From 94d7c55025f5df750ce213172c5d2441b5a210e1 Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Fri, 25 Mar 2011 11:09:10 -0700 Subject: [PATCH] move ModalBoxTyCon, ArrowTyCon to HaskLiteralsAndTyCons --- src/HaskCoreToWeak.v | 3 --- src/HaskLiteralsAndTyCons.v | 3 +++ src/HaskWeakToCore.v | 3 --- 3 files changed, 3 insertions(+), 6 deletions(-) diff --git a/src/HaskCoreToWeak.v b/src/HaskCoreToWeak.v index 055d588..36399a0 100644 --- a/src/HaskCoreToWeak.v +++ b/src/HaskCoreToWeak.v @@ -15,9 +15,6 @@ Require Import HaskWeakVars. Require Import HaskWeakTypes. Require Import HaskWeak. -Variable ModalBoxTyCon : TyCon. Extract Inlined Constant ModalBoxTyCon => "TysWiredIn.hetMetCodeTypeTyCon". -Variable ArrowTyCon : TyCon. Extract Constant ArrowTyCon => "Type.funTyCon". - Variable tyConOrTyFun : CoreTyCon -> sum TyCon TyFun. Extract Inlined Constant tyConOrTyFun => "tyConOrTyFun". Variable coreViewDeep : CoreType -> CoreType. Extract Inlined Constant coreViewDeep => "coreViewDeep". Variable coreCoercionToWeakCoercion : CoreCoercion -> WeakCoercion. diff --git a/src/HaskLiteralsAndTyCons.v b/src/HaskLiteralsAndTyCons.v index 24fc00f..0592f3a 100644 --- a/src/HaskLiteralsAndTyCons.v +++ b/src/HaskLiteralsAndTyCons.v @@ -86,3 +86,6 @@ Variable tyConToString : TyCon -> string. Extract Inlined Constant tyCon Variable tyFunToString : TyFun -> string. Extract Inlined Constant tyFunToString => "outputableToString". Instance TyConToString : ToString TyCon := { toString := tyConToString }. Instance TyFunToString : ToString TyFun := { toString := tyFunToString }. + +Variable ModalBoxTyCon : TyCon. Extract Inlined Constant ModalBoxTyCon => "TysWiredIn.hetMetCodeTypeTyCon". +Variable ArrowTyCon : TyCon. Extract Constant ArrowTyCon => "Type.funTyCon". diff --git a/src/HaskWeakToCore.v b/src/HaskWeakToCore.v index 51e61dd..290d634 100644 --- a/src/HaskWeakToCore.v +++ b/src/HaskWeakToCore.v @@ -31,9 +31,6 @@ Variable mkUnsafeCoercion : CoreType -> CoreType -> CoreCoercion. Variable coreCoercionsAreReallyTypes : CoreCoercion -> CoreType. Extract Inlined Constant coreCoercionsAreReallyTypes => "(\x -> x)". -Variable ModalBoxTyCon : TyCon. Extract Inlined Constant ModalBoxTyCon => "TysWiredIn.hetMetCodeTypeTyCon". -Variable ArrowTyCon : TyCon. Extract Constant ArrowTyCon => "Type.funTyCon". - Definition weakAltConToCoreAltCon (wa:WeakAltCon) : CoreAltCon := match wa with | WeakDataAlt cdc => DataAlt cdc -- 1.7.10.4