first pass at proper handling of coercions in HaskWeak

[coq-hetmet.git] / src / HaskWeakTypes.v

diff --git a/src/HaskWeakTypes.v b/src/HaskWeakTypes.v
index 6b6b61e..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.
 
+(* 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".
@@ -67,30 +100,6 @@ Fixpoint isTyConApp (wt:WeakType)(acc:list WeakType) : ??(TyCon * list WeakType)
     | _            => None
   end.
 
-(* messy first-order NON-CAPTURE-AVOIDING substitution on WeakType's *)
-Fixpoint replaceWeakTypeVar (te:WeakType)(tv:WeakTypeVar)(tsubst:WeakType) : WeakType :=
-  match te with
-    | WTyVarTy  tv'            => if eqd_dec tv tv' then tsubst else te
-    | WAppTy  t1 t2            => WAppTy (replaceWeakTypeVar t1 tv tsubst) (replaceWeakTypeVar t2 tv tsubst)
-    | WForAllTy  tv' t         => if eqd_dec tv tv' then te else WForAllTy tv' (replaceWeakTypeVar t tv tsubst)
-    | WCoFunTy t1 t2 t         => WCoFunTy (replaceWeakTypeVar t1 tv tsubst)
-                                      (replaceWeakTypeVar t2 tv tsubst) (replaceWeakTypeVar t tv tsubst)
-    | WIParam ip ty  => WIParam ip (replaceWeakTypeVar ty tv tsubst)
-    | WClassP  c lt => WClassP c ((fix replaceCoreDistinctList (lt:list WeakType) :=
-      match lt with
-        | nil => nil
-        | h::t => (replaceWeakTypeVar h tv tsubst)::(replaceCoreDistinctList t)
-      end) lt)
-    | WTyFunApp tc lt => WTyFunApp tc ((fix replaceCoreDistinctList (lt:list WeakType) :=
-      match lt with
-        | nil => nil
-        | h::t => (replaceWeakTypeVar h tv tsubst)::(replaceCoreDistinctList t)
-      end) lt)
-    | WTyCon tc                => WTyCon tc
-    | WFunTyCon                => WFunTyCon
-    | WModalBoxTyCon           => WModalBoxTyCon
-  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.