first pass at proper handling of coercions in HaskWeak

diff --git a/src/Extraction-prefix.hs b/src/Extraction-prefix.hs
index 4abbf69..d0b6ffa 100644 (file)
--- a/src/Extraction-prefix.hs
+++ b/src/Extraction-prefix.hs
@@ -19,10 +19,12 @@ import qualified FastString
 import qualified BasicTypes
 import qualified DataCon
 import qualified CoreSyn
 import qualified BasicTypes
 import qualified DataCon
 import qualified CoreSyn

+import qualified CoreUtils

 import qualified Class
 import qualified Data.Char 
 import qualified Class
 import qualified Data.Char 

+import qualified Data.Typeable

 import Data.Bits ((.&.), shiftL, (.|.))
 import Data.Bits ((.&.), shiftL, (.|.))

-import Prelude ( (++), (+), (==), Show, show, Char )
+import Prelude ( (++), (+), (==), Show, show, Char, (.) )

 import qualified Prelude
 import qualified GHC.Base
 
 import qualified Prelude
 import qualified GHC.Base
 

@@ -44,11 +46,15 @@ errOrFail (Error s) = Prelude.error s
 getTyConTyVars :: TyCon.TyCon -> [Var.TyVar]
 getTyConTyVars tc = if TyCon.isFunTyCon tc then [] else if TyCon.isPrimTyCon tc then [] else TyCon.tyConTyVars tc
 
 getTyConTyVars :: TyCon.TyCon -> [Var.TyVar]
 getTyConTyVars tc = if TyCon.isFunTyCon tc then [] else if TyCon.isPrimTyCon tc then [] else TyCon.tyConTyVars tc
 

+sortAlts :: [(CoreSyn.AltCon,a,b)] -> [(CoreSyn.AltCon,a,b)]
+sortAlts x = x -- FIXME
+

 -- to do: this could be moved into Coq
 coreVarToWeakVar :: Var.Var -> WeakVar
 coreVarToWeakVar v | Id.isId     v = WExprVar (WeakExprVar v (errOrFail (coreTypeToWeakType (Var.varType v))))
 coreVarToWeakVar v | Var.isTyVar v = WTypeVar (WeakTypeVar v (coreKindToKind (Var.varType v)))
 -- to do: this could be moved into Coq
 coreVarToWeakVar :: Var.Var -> WeakVar
 coreVarToWeakVar v | Id.isId     v = WExprVar (WeakExprVar v (errOrFail (coreTypeToWeakType (Var.varType v))))
 coreVarToWeakVar v | Var.isTyVar v = WTypeVar (WeakTypeVar v (coreKindToKind (Var.varType v)))

-coreVarToWeakVar v | Var.isCoVar v = WCoerVar (WeakCoerVar v (Prelude.error "FIXME") (Prelude.error "FIXME"))
+coreVarToWeakVar v | Var.isCoVar v = WCoerVar (WeakCoerVar v (Prelude.error "FIXME") 
+                                                             (Prelude.error "FIXME") (Prelude.error "FIXME"))

 coreVarToWeakVar _                 =
    Prelude.error "Var.Var that is neither an expression variable, type variable, nor coercion variable!"
 
 coreVarToWeakVar _                 =
    Prelude.error "Var.Var that is neither an expression variable, type variable, nor coercion variable!"
 

@@ -80,7 +86,7 @@ coreKindToKind k =
   case Coercion.splitKindFunTy_maybe k of
       Prelude.Just (k1,k2) -> KindTypeFunction (coreKindToKind k1) (coreKindToKind k2)
       Prelude.Nothing -> 
   case Coercion.splitKindFunTy_maybe k of
       Prelude.Just (k1,k2) -> KindTypeFunction (coreKindToKind k1) (coreKindToKind k2)
       Prelude.Nothing -> 

-                      if      (Coercion.isLiftedTypeKind k)   then KindType
+                      if (Coercion.isLiftedTypeKind k)   then KindType

                  else if (Coercion.isUnliftedTypeKind k) then KindUnliftedType
                  else if (Coercion.isOpenTypeKind k)     then KindOpenType
                  else if (Coercion.isArgTypeKind k)      then KindArgType
                  else if (Coercion.isUnliftedTypeKind k) then KindUnliftedType
                  else if (Coercion.isOpenTypeKind k)     then KindOpenType
                  else if (Coercion.isArgTypeKind k)      then KindArgType

@@ -113,3 +119,45 @@ coreViewDeep t =
       TypeRep.PredTy p         -> case Type.coreView t of
                                Prelude.Nothing     -> TypeRep.PredTy p
                                Prelude.Just    t'  -> t'
       TypeRep.PredTy p         -> case Type.coreView t of
                                Prelude.Nothing     -> TypeRep.PredTy p
                                Prelude.Just    t'  -> t'

+
+-- FIXME: cotycon applications may be oversaturated
+coreCoercionToWeakCoercion :: Type.Type -> WeakCoercion
+coreCoercionToWeakCoercion c =
+ case c of
+  TypeRep.TyVarTy  v     -> WCoVar (WeakCoerVar v (Prelude.error "FIXME") (Prelude.error "FIXME") (Prelude.error "FIXME"))
+  TypeRep.AppTy    t1 t2 -> WCoApp   (coreCoercionToWeakCoercion t1) (coreCoercionToWeakCoercion t2)
+  TypeRep.TyConApp tc t  ->
+      case TyCon.isCoercionTyCon_maybe tc of
+        Prelude.Nothing -> Prelude.error ((Prelude.++) "coreCoercionToWeakCoercion got " (outputableToString c))
+        Prelude.Just (_, ctcd) ->
+            case (ctcd,t) of
+              (TyCon.CoTrans , [x,y]     ) -> WCoComp   (coreCoercionToWeakCoercion x) (coreCoercionToWeakCoercion y)
+              (TyCon.CoSym   , [x]       ) -> WCoSym    (coreCoercionToWeakCoercion x)
+              (TyCon.CoLeft  , [x]       ) -> WCoLeft   (coreCoercionToWeakCoercion x)
+              (TyCon.CoRight , [x]       ) -> WCoLeft   (coreCoercionToWeakCoercion x)
+-- FIXME      (TyCon.CoUnsafe, [t1, t2 ] ) -> WCoUnsafe (coreTypeToWeakType t1) (coreTypeToWeakType t2)
+              (TyCon.CoTrans , []        ) -> Prelude.error "CoTrans is not in post-publication-appendix SystemFC1"
+              (TyCon.CoCsel1 , []        ) -> Prelude.error "CoCsel1 is not in post-publication-appendix SystemFC1"
+              (TyCon.CoCsel2 , []        ) -> Prelude.error "CoCsel2 is not in post-publication-appendix SystemFC1"
+              (TyCon.CoCselR , []        ) -> Prelude.error "CoCselR is not in post-publication-appendix SystemFC1"
+              (TyCon.CoInst  , []        ) -> Prelude.error "CoInst  is not in post-publication-appendix SystemFC1"
+--              (TyCon.CoAxiom , []        ) -> Prelude.error "CoAxiom is not yet implemented (FIXME)"
+              _ -> Prelude.error ((Prelude.++) "coreCoercionToWeakCoercion got " (outputableToString c))
+  _ -> Prelude.error ((Prelude.++) "coreCoercionToWeakCoercion got " (outputableToString c))
+--  TypeRep.ForAllTy v t   -> WCoAll  (Prelude.error "FIXME") (coreTypeToWeakType t)
+-- FIXME   x y                                  -> WCoAppT    (coreCoercionToWeakCoercion x) (coreCoercionToWeakType y)
+--  CoreSyn.Type t                            -> WCoType   (coreTypeToWeakType t)
+
+{-
+weakCoercionToCoreCoercion :: CoreCoercion -> Type.Type
+| WCoVar     (weakCoerVar _ _ t1 t2) => (t1,t2)
+| WCoType    t                       => Prelude_error "FIXME WCoType"
+| WCoApp     c1 c2                   => Prelude_error "FIXME WCoApp"
+| WCoAppT    c t                     => Prelude_error "FIXME WCoAppT"
+| WCoAll     k f                     => Prelude_error "FIXME WCoAll"
+| WCoSym     c                       => let (t2,t1) := weakCoercionTypes c in (t1,t2)
+| WCoComp    c1 c2                   => Prelude_error "FIXME WCoComp"
+| WCoLeft    c                       => Prelude_error "FIXME WCoLeft"
+| WCoRight   c                       => Prelude_error "FIXME WCoRight"
+| WCoUnsafe  t1 t2                   => (t1,t2)
+-}
\ No newline at end of file

diff --git a/src/HaskCoreToWeak.v b/src/HaskCoreToWeak.v
index 1734637..1cbaf22 100644 (file)
--- a/src/HaskCoreToWeak.v
+++ b/src/HaskCoreToWeak.v
@@ -14,7 +14,6 @@ Require Import HaskCore.
 Require Import HaskWeakVars.
 Require Import HaskWeakTypes.
 Require Import HaskWeak.
 Require Import HaskWeakVars.
 Require Import HaskWeakTypes.
 Require Import HaskWeak.

-Require Import HaskWeakToCore.

 
 Axiom    tycons_distinct       : ~(ArrowTyCon=ModalBoxTyCon).
 Variable tyConOrTyFun          : CoreTyCon -> sum TyCon TyFun. Extract Inlined Constant tyConOrTyFun      => "tyConOrTyFun".
 
 Axiom    tycons_distinct       : ~(ArrowTyCon=ModalBoxTyCon).
 Variable tyConOrTyFun          : CoreTyCon -> sum TyCon TyFun. Extract Inlined Constant tyConOrTyFun      => "tyConOrTyFun".

@@ -44,7 +43,7 @@ Fixpoint coreTypeToWeakType' (ct:CoreType) : ???WeakType :=
                                     | WExprVar _  => Error "encountered expression variable in a modal box type"
                                     | WCoerVar _  => Error "encountered coercion variable in a modal box type"
                                   end
                                     | WExprVar _  => Error "encountered expression variable in a modal box type"
                                     | WCoerVar _  => Error "encountered coercion variable in a modal box type"
                                   end

-                                | _                           => Error "mis-applied modal box tycon"
+                                | _                           => Error ("mis-applied modal box tycon: " +++ ct)

                               end
                          else let tc' := if eqd_dec tc ArrowTyCon
                                          then WFunTyCon
                               end
                          else let tc' := if eqd_dec tc ArrowTyCon
                                          then WFunTyCon

@@ -75,9 +74,6 @@ Fixpoint coreTypeToWeakType' (ct:CoreType) : ???WeakType :=
 Variable coreViewDeep : CoreType -> CoreType.  Extract Inlined Constant coreViewDeep => "coreViewDeep".
 Definition coreTypeToWeakType t := coreTypeToWeakType' (coreViewDeep t).
 
 Variable coreViewDeep : CoreType -> CoreType.  Extract Inlined Constant coreViewDeep => "coreViewDeep".
 Definition coreTypeToWeakType t := coreTypeToWeakType' (coreViewDeep t).
 

-Definition weakTypeOfWeakExpr (we:WeakExpr) : ???WeakType :=
-  coreTypeToWeakType (coreTypeOfCoreExpr (weakExprToCoreExpr we)).
-

 (* detects our crude Core-encoding of modal type introduction/elimination forms *)
 Definition isBrak (ce:@CoreExpr CoreVar) : ??(CoreVar * WeakTypeVar * CoreType) :=
 match ce with
 (* detects our crude Core-encoding of modal type introduction/elimination forms *)
 Definition isBrak (ce:@CoreExpr CoreVar) : ??(CoreVar * WeakTypeVar * CoreType) :=
 match ce with

@@ -102,11 +98,14 @@ match ce with
   | _ => None
 end.
 
   | _ => None
 end.
 

-Definition coreCoercionToWeakCoercion (cc:CoreCoercion) : ???WeakCoercion :=
+Variable coreCoercionToWeakCoercion : CoreCoercion -> WeakCoercion.
+  Extract Inlined Constant coreCoercionToWeakCoercion => "coreCoercionToWeakCoercion".
+(*

   let (t1,t2) := coreCoercionKind cc
   in  coreTypeToWeakType t1 >>= fun t1' =>
   let (t1,t2) := coreCoercionKind cc
   in  coreTypeToWeakType t1 >>= fun t1' =>

-    coreTypeToWeakType t2 >>= fun t2' =>
-    OK (weakCoercion (kindOfCoreType t1) t1' t2' cc).
+        coreTypeToWeakType t2 >>= fun t2' =>
+          OK (WCoUnsafe t1' t2').
+*)

 
 Fixpoint coreExprToWeakExpr (ce:@CoreExpr CoreVar) : ???WeakExpr :=
   match ce with
 
 Fixpoint coreExprToWeakExpr (ce:@CoreExpr CoreVar) : ???WeakExpr :=
   match ce with

@@ -114,8 +113,7 @@ Fixpoint coreExprToWeakExpr (ce:@CoreExpr CoreVar) : ???WeakExpr :=
     | CoreENote  n e   => coreExprToWeakExpr e >>= fun e' => OK (WENote n e')
     | CoreEType  t     => Error "encountered CoreEType in a position where an Expr should have been"
     | CoreECast  e co  => coreExprToWeakExpr e >>= fun e' =>
     | CoreENote  n e   => coreExprToWeakExpr e >>= fun e' => OK (WENote n e')
     | CoreEType  t     => Error "encountered CoreEType in a position where an Expr should have been"
     | CoreECast  e co  => coreExprToWeakExpr e >>= fun e' =>

-                            coreCoercionToWeakCoercion co >>= fun co' =>
-                              OK (WECast e' co')
+                              OK (WECast e' (coreCoercionToWeakCoercion co))

 
     | CoreEVar   v     => match coreVarToWeakVar v with
                             | WExprVar ev => OK (WEVar ev)
 
     | CoreEVar   v     => match coreVarToWeakVar v with
                             | WExprVar ev => OK (WEVar ev)

@@ -178,8 +176,8 @@ Fixpoint coreExprToWeakExpr (ce:@CoreExpr CoreVar) : ???WeakExpr :=
         | WTypeVar _  => Error "found a type variable in a case"
         | WCoerVar _  => Error "found a coercion variable in a case"
         | WExprVar ev => 
         | WTypeVar _  => Error "found a type variable in a case"
         | WCoerVar _  => Error "found a coercion variable in a case"
         | WExprVar ev => 

-      coreExprToWeakExpr e >>= fun e' =>
-        weakTypeOfWeakExpr e' >>= fun te' =>
+        coreTypeToWeakType (coreTypeOfCoreExpr e) >>= fun te' =>
+        coreExprToWeakExpr e >>= fun e' =>

           (match isTyConApp te' nil with None => Error "expectTyConApp encountered strange type" | Some x => OK x end)
              >>= fun tca =>
             let (tc,lt) := tca in
           (match isTyConApp te' nil with None => Error "expectTyConApp encountered strange type" | Some x => OK x end)
              >>= fun tca =>
             let (tc,lt) := tca in

diff --git a/src/HaskStrongTypes.v b/src/HaskStrongTypes.v
index 81beb65..e79927a 100644 (file)
--- a/src/HaskStrongTypes.v
+++ b/src/HaskStrongTypes.v
@@ -13,6 +13,7 @@ Require Import HaskCoreTypes.
 Require Import HaskCoreVars.
 Require Import HaskWeakTypes.
 Require Import HaskWeakVars.
 Require Import HaskCoreVars.
 Require Import HaskWeakTypes.
 Require Import HaskWeakVars.

+Require Import HaskWeak.

 Require Import HaskCoreToWeak.
 
 Variable dataConTyCon      : CoreDataCon -> TyCon.         Extract Inlined Constant dataConTyCon      => "DataCon.dataConTyCon".
 Require Import HaskCoreToWeak.
 
 Variable dataConTyCon      : CoreDataCon -> TyCon.         Extract Inlined Constant dataConTyCon      => "DataCon.dataConTyCon".

diff --git a/src/HaskWeakToCore.v b/src/HaskWeakToCore.v
index 88c6830..e4a4d1f 100644 (file)
--- a/src/HaskWeakToCore.v
+++ b/src/HaskWeakToCore.v
@@ -15,6 +15,7 @@ Require Import HaskCore.
 Require Import HaskWeakVars.
 Require Import HaskWeakTypes.
 Require Import HaskWeak.
 Require Import HaskWeakVars.
 Require Import HaskWeakTypes.
 Require Import HaskWeak.

+Require Import HaskCoreToWeak.

 
 Variable mkCoreLet : @CoreBind CoreVar -> @CoreExpr CoreVar -> @CoreExpr CoreVar.
   Extract Inlined Constant mkCoreLet => "MkCore.mkCoreLet".
 
 Variable mkCoreLet : @CoreBind CoreVar -> @CoreExpr CoreVar -> @CoreExpr CoreVar.
   Extract Inlined Constant mkCoreLet => "MkCore.mkCoreLet".

@@ -23,16 +24,15 @@ Variable sortAlts  : forall {a}{b}, list (@triple AltCon a b) -> list (@triple A
   Extract Inlined Constant sortAlts => "sortAlts".
   Implicit Arguments sortAlts [[a][b]].
 
   Extract Inlined Constant sortAlts => "sortAlts".
   Implicit Arguments sortAlts [[a][b]].
 

-Variable trustMeCoercion           : CoreCoercion.
-  Extract Inlined Constant trustMeCoercion => "Coercion.unsafeCoerce".
+Variable mkUnsafeCoercion : CoreType -> CoreType -> CoreCoercion.
+    Extract Inlined Constant mkUnsafeCoercion => "Coercion.mkUnsafeCoercion".

 
 (* Coercion and Type are actually the same thing in GHC, but we don't tell Coq about that.  This lets us get around it. *)
 Variable coreCoercionsAreReallyTypes : CoreCoercion -> CoreType.
   Extract Inlined Constant coreCoercionsAreReallyTypes => "(\x -> x)".
 
 
 (* Coercion and Type are actually the same thing in GHC, but we don't tell Coq about that.  This lets us get around it. *)
 Variable coreCoercionsAreReallyTypes : CoreCoercion -> CoreType.
   Extract Inlined Constant coreCoercionsAreReallyTypes => "(\x -> x)".
 

-Definition weakCoercionToCoreCoercion : WeakCoercion -> CoreCoercion :=
-   fun _ => trustMeCoercion.
-
+  Definition weakCoercionToCoreCoercion (wc:WeakCoercion) : CoreCoercion :=
+    mkUnsafeCoercion (weakTypeToCoreType (fst (weakCoercionTypes wc))) (weakTypeToCoreType (snd (weakCoercionTypes wc))).

 
   Fixpoint weakExprToCoreExpr (me:WeakExpr) : @CoreExpr CoreVar :=
   match me with
 
   Fixpoint weakExprToCoreExpr (me:WeakExpr) : @CoreExpr CoreVar :=
   match me with

@@ -87,8 +87,9 @@ Definition weakCoercionToCoreCoercion : WeakCoercion -> CoreCoercion :=
                                                (weakExprToCoreExpr e)
   end.
 
                                                (weakExprToCoreExpr e)
   end.
 

+Definition weakTypeOfWeakExpr (we:WeakExpr) : ???WeakType :=
+  coreTypeToWeakType (coreTypeOfCoreExpr (weakExprToCoreExpr we)).

 
 Instance weakExprToString : ToString WeakExpr  :=
   { toString := fun we => toString (weakExprToCoreExpr we) }.
 
 
 Instance weakExprToString : ToString WeakExpr  :=
   { toString := fun we => toString (weakExprToCoreExpr we) }.
 

-

diff --git a/src/HaskWeakToStrong.v b/src/HaskWeakToStrong.v
index d765f0f..e5c88f8 100644 (file)
--- a/src/HaskWeakToStrong.v
+++ b/src/HaskWeakToStrong.v
@@ -19,7 +19,6 @@ Require Import HaskStrongTypes.
 Require Import HaskStrong.
 Require Import HaskCoreTypes.
 Require Import HaskCoreVars.
 Require Import HaskStrong.
 Require Import HaskCoreTypes.
 Require Import HaskCoreVars.

-Require Import HaskCoreToWeak.

 
 Open Scope string_scope.
 Definition TyVarResolver Γ   := forall wt:WeakTypeVar, ???(HaskTyVar Γ wt).
 
 Open Scope string_scope.
 Definition TyVarResolver Γ   := forall wt:WeakTypeVar, ???(HaskTyVar Γ wt).

@@ -559,7 +558,7 @@ Definition weakExprToStrongExpr : forall
                                                    weakExprToStrongExpr Γ (_ :: Δ) φ (weakψ ψ) ξ te' lev e >>= fun e' =>
                                                      castExpr we "WECoLam" _ (ECoLam Γ Δ cv te' t1' t2' ξ lev e')
 
                                                    weakExprToStrongExpr Γ (_ :: Δ) φ (weakψ ψ) ξ te' lev e >>= fun e' =>
                                                      castExpr we "WECoLam" _ (ECoLam Γ Δ cv te' t1' t2' ξ lev e')
 

-    | WECast  e co                      => let (_,t1,t2,_) := co in
+    | WECast  e co                      => let (t1,t2) := weakCoercionTypes co in

                                              weakTypeToType'' φ t1 ★ >>= fun t1' =>
                                                weakTypeToType'' φ t2 ★ >>= fun t2' =>
                                                    weakExprToStrongExpr Γ Δ φ ψ ξ t1' lev e >>= fun e' =>
                                              weakTypeToType'' φ t1 ★ >>= fun t1' =>
                                                weakTypeToType'' φ t2 ★ >>= fun t2' =>
                                                    weakExprToStrongExpr Γ Δ φ ψ ξ t1' lev e >>= fun e' =>

diff --git a/src/HaskWeakTypes.v b/src/HaskWeakTypes.v
index 593bccf..cdbc9e7 100644 (file)
--- a/src/HaskWeakTypes.v
+++ b/src/HaskWeakTypes.v
@@ -55,6 +55,39 @@ Instance WeakTypeVarEqDecidable : EqDecidable WeakTypeVar.
     right; intro; apply n; inversion H; subst; auto.
     Defined.
 
     right; intro; apply n; inversion H; subst; auto.
     Defined.
 

+(* a WeakCoerVar just wraps a CoreVar and tags it with the pair of types amongst which it coerces *)
+Inductive WeakCoerVar := weakCoerVar : CoreVar -> Kind -> WeakType -> WeakType -> WeakCoerVar.
+
+Inductive WeakCoercion : Type :=
+| WCoVar          : WeakCoerVar                                   -> WeakCoercion (* g      *)
+| WCoType         : WeakType                                      -> WeakCoercion (* τ      *)
+| WCoApp          : WeakCoercion -> WeakCoercion                  -> WeakCoercion (* γ γ    *)
+| WCoAppT         : WeakCoercion -> WeakType                      -> WeakCoercion (* γ@v    *)
+| WCoAll          : Kind  -> (WeakTypeVar -> WeakCoercion)        -> WeakCoercion (* ∀a:κ.γ *)
+| WCoSym          : WeakCoercion                                  -> WeakCoercion (* sym    *)
+| WCoComp         : WeakCoercion -> WeakCoercion                  -> WeakCoercion (* ◯      *)
+| WCoLeft         : WeakCoercion                                  -> WeakCoercion (* left   *)
+| WCoRight        : WeakCoercion                                  -> WeakCoercion (* right  *)
+| WCoUnsafe       : WeakType -> WeakType                          -> WeakCoercion (* unsafe *)
+(*| WCoCFApp        : ∀ n, CoFunConst n -> vec WeakCoercion n       -> WeakCoercion (* C   γⁿ *)*)
+(*| WCoTFApp        : ∀ n, TyFunConst n -> vec WeakCoercion n       -> WeakCoercion (* S_n γⁿ *)*)
+.
+
+Variable Prelude_error : forall {A}, string -> A.   Extract Inlined Constant Prelude_error => "Prelude.error".
+Fixpoint weakCoercionTypes (wc:WeakCoercion) : WeakType * WeakType :=
+match wc with
+| WCoVar     (weakCoerVar _ _ t1 t2) => (t1,t2)
+| WCoType    t                       => Prelude_error "FIXME WCoType"
+| WCoApp     c1 c2                   => Prelude_error "FIXME WCoApp"
+| WCoAppT    c t                     => Prelude_error "FIXME WCoAppT"
+| WCoAll     k f                     => Prelude_error "FIXME WCoAll"
+| WCoSym     c                       => let (t2,t1) := weakCoercionTypes c in (t1,t2)
+| WCoComp    c1 c2                   => Prelude_error "FIXME WCoComp"
+| WCoLeft    c                       => Prelude_error "FIXME WCoLeft"
+| WCoRight   c                       => Prelude_error "FIXME WCoRight"
+| WCoUnsafe  t1 t2                   => (t1,t2)
+end.
+

 (* TO DO: write a proper EqDecidable instance for WeakType and then move the rest of this into HaskWeakToCore *)
 Variable ModalBoxTyCon   : TyCon.        Extract Inlined Constant ModalBoxTyCon => "TysWiredIn.hetMetCodeTypeTyCon".
 Variable ArrowTyCon      : TyCon.        Extract Constant ArrowTyCon    => "Type.funTyCon".
 (* TO DO: write a proper EqDecidable instance for WeakType and then move the rest of this into HaskWeakToCore *)
 Variable ModalBoxTyCon   : TyCon.        Extract Inlined Constant ModalBoxTyCon => "TysWiredIn.hetMetCodeTypeTyCon".
 Variable ArrowTyCon      : TyCon.        Extract Constant ArrowTyCon    => "Type.funTyCon".

diff --git a/src/HaskWeakVars.v b/src/HaskWeakVars.v
index 8a77e09..f174563 100644 (file)
--- a/src/HaskWeakVars.v
+++ b/src/HaskWeakVars.v
@@ -13,12 +13,6 @@ Require Import HaskCoreVars.
 Require Import HaskCoreTypes.
 Require Import HaskWeakTypes.
 
 Require Import HaskCoreTypes.
 Require Import HaskWeakTypes.
 

-(* TO DO: finish this *)
-Inductive WeakCoercion : Type := weakCoercion : Kind -> WeakType -> WeakType -> CoreCoercion -> WeakCoercion.
-
-(* a WeakCoerVar just wraps a CoreVar and tags it with the pair of types amongst which it coerces *)
-Inductive WeakCoerVar := weakCoerVar : CoreVar -> Kind -> WeakType -> WeakType -> WeakCoerVar.
-

 (* a WeakExprVar just wraps a CoreVar and tags it with the type of its value *)
 Inductive WeakExprVar := weakExprVar : CoreVar -> WeakType -> WeakExprVar.
 
 (* a WeakExprVar just wraps a CoreVar and tags it with the type of its value *)
 Inductive WeakExprVar := weakExprVar : CoreVar -> WeakType -> WeakExprVar.