X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskWeakTypes.v;h=9ec126eb69607f52924330adbc336a62133d5870;hp=593bccf77b5d2de3a138cc61f0facefea7d2dfef;hb=18a60d7a8ae87aa64c73f9ac03c785b12f8bd25a;hpb=5cfd103cffd56381262b2d280cbba88e0932f78a

diff --git a/src/HaskWeakTypes.v b/src/HaskWeakTypes.v
index 593bccf..9ec126e 100644
--- a/src/HaskWeakTypes.v
+++ b/src/HaskWeakTypes.v
@@ -8,18 +8,9 @@ Require Import General.
 Require Import Coq.Strings.String.
 Require Import Coq.Lists.List.
 Require Import HaskKinds.
-Require Import HaskCoreLiterals.
+Require Import HaskLiterals.
+Require Import HaskTyCons.
 Require Import HaskCoreVars.
-Require Import HaskCoreTypes.
-
-(* TO DO: mark the TyCon used for hetmet as a "type family" so GHC keeps it fully-applied-at-all-times *)
-Variable tyConToCoreTyCon : TyCon -> CoreTyCon.           Extract Inlined Constant tyConToCoreTyCon  => "(\x -> x)".
-Variable tyFunToCoreTyCon : TyFun -> CoreTyCon.           Extract Inlined Constant tyFunToCoreTyCon  => "(\x -> x)".
-Coercion tyConToCoreTyCon : TyCon >-> CoreTyCon.
-Coercion tyFunToCoreTyCon : TyFun >-> CoreTyCon.
-
-Instance TyConToString : ToString TyCon := { toString := tyConToString }.
-Instance TyFunToString : ToString TyFun := { toString := tyConToString }.
 
 (* a WeakTypeVar merely wraps a CoreVar and includes its Kind *)
 Inductive WeakTypeVar := weakTypeVar : CoreVar -> Kind -> WeakTypeVar.
@@ -55,61 +46,45 @@ Instance WeakTypeVarEqDecidable : EqDecidable WeakTypeVar.
     right; intro; apply n; inversion H; subst; auto.
     Defined.
 
-(* 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".
-
-(* if this is a (WAppTy (WAppTy ... (WTyCon tc) .. ) .. ), return (tc,[...]) *)
-Fixpoint isTyConApp (wt:WeakType)(acc:list WeakType) : ??(TyCon * list WeakType) :=
-  match wt with
-    | WTyCon tc    => Some (tc,acc)
-    | WAppTy t1 t2 => isTyConApp t1 (t2::acc)
-    | _            => None
-  end.
-
-(* we try to normalize the representation of a type as much as possible before feeding it back to GHCs type-comparison function *)
-Definition normalizeWeakType (wt:WeakType) : WeakType := wt.
+(* a WeakCoerVar just wraps a CoreVar and tags it with the pair of types amongst which it coerces *)
+Inductive WeakCoerVar := weakCoerVar : CoreVar -> WeakType -> WeakType -> WeakCoerVar.
 
-Fixpoint weakTypeToCoreType' (wt:WeakType) : CoreType :=
-  match wt with
-    | WTyVarTy  (weakTypeVar v _)     => TyVarTy v
-    | WAppTy (WAppTy WFunTyCon t1) t2 => FunTy (weakTypeToCoreType' t1) (weakTypeToCoreType' t2)
-    | WAppTy  t1 t2                   => match (weakTypeToCoreType' t1) with
-                                           | TyConApp tc tys => TyConApp tc (app tys ((weakTypeToCoreType' t2)::nil))
-                                           | t1'             => AppTy t1' (weakTypeToCoreType' t2)
-                                         end
-    | WTyCon    tc                    => TyConApp tc nil
-    | WTyFunApp tf lt                 => TyConApp tf (map weakTypeToCoreType' lt)
-    | WClassP c lt                    => PredTy (ClassP c (map weakTypeToCoreType' lt))
-    | WIParam n ty                    => PredTy (IParam n (weakTypeToCoreType' ty))
-    | WForAllTy (weakTypeVar wtv _) t => ForAllTy wtv (weakTypeToCoreType' t)
-    | WFunTyCon                       => TyConApp ArrowTyCon nil
-    | WCodeTy  (weakTypeVar ec _) t   => TyConApp ModalBoxTyCon ((TyVarTy ec)::(weakTypeToCoreType' t)::nil)
-    | WCoFunTy t1 t2 t3               => FunTy (PredTy (EqPred (weakTypeToCoreType' t1) (weakTypeToCoreType' t2)))
-                                            (weakTypeToCoreType' t3)
-  end.
+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 γⁿ *)*)
+.
 
-Definition weakTypeToCoreType (wt:WeakType) :=
-  weakTypeToCoreType' (normalizeWeakType wt).
+Fixpoint weakCoercionTypes (wc:WeakCoercion) : WeakType * WeakType :=
+match wc with
+| WCoVar     (weakCoerVar _ t1 t2)   => (WFunTyCon,WFunTyCon)   (* FIXME!!! *)
+| WCoType    t                       => (WFunTyCon,WFunTyCon)   (* FIXME!!! *)
+| WCoApp     c1 c2                   => (WFunTyCon,WFunTyCon)   (* FIXME!!! *)
+| WCoAppT    c t                     => (WFunTyCon,WFunTyCon)   (* FIXME!!! *)
+| WCoAll     k f                     => (WFunTyCon,WFunTyCon)   (* FIXME!!! *)
+| WCoSym     c                       => let (t2,t1) := weakCoercionTypes c in (t1,t2)
+| WCoComp    c1 c2                   => (WFunTyCon,WFunTyCon)   (* FIXME!!! *)
+| WCoLeft    c                       => (WFunTyCon,WFunTyCon)   (* FIXME!!! *)
+| WCoRight   c                       => (WFunTyCon,WFunTyCon)   (* FIXME!!! *)
+| WCoUnsafe  t1 t2                   => (t1,t2)
+end.
 
-Definition compare_weakTypes (w1 w2:WeakType) :=
-  if coretype_eq_dec (weakTypeToCoreType w1) (weakTypeToCoreType w2)
-    then true
-    else false.
 
-(*
-Instance EqDecidableWeakType : EqDecidable WeakType.
-  apply Build_EqDecidable.
-  intros.
-  set (compare_weakTypes_axiom v1 v2) as x.
-  set (compare_weakTypes v1 v2) as y.
-  assert (y=compare_weakTypes v1 v2). reflexivity.
-  destruct y; rewrite <- H in x.
-  left; auto.
-  right; auto.
-  Defined.
-*)
-
-Instance WeakTypeToString : ToString WeakType :=
-  { toString := coreTypeToString ○ weakTypeToCoreType }.
+(* this is a trick to allow circular definitions, post-extraction *)
+Variable weakTypeToString : WeakType -> string.
+    Extract Inlined Constant weakTypeToString => "(coreTypeToString . weakTypeToCoreType)".
+Instance WeakTypeToString : ToString WeakType := { toString := weakTypeToString }.
 
+Variable tyConToCoreTyCon : TyCon  -> CoreTyCon.           Extract Inlined Constant tyConToCoreTyCon  => "(\x -> x)".
+Variable tyFunToCoreTyCon : TyFun  -> CoreTyCon.           Extract Inlined Constant tyFunToCoreTyCon  => "(\x -> x)".
+Coercion tyConToCoreTyCon : TyCon >-> CoreTyCon.
+Coercion tyFunToCoreTyCon : TyFun >-> CoreTyCon.