remove weakTypeOfWeakExpr and replaceWeakTypeVar, no longer required

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

diff --git a/src/HaskWeakTypes.v b/src/HaskWeakTypes.v
index b295cf1..593bccf 100644 (file)
--- a/src/HaskWeakTypes.v
+++ b/src/HaskWeakTypes.v
@@ -13,6 +13,13 @@ 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.
@@ -26,7 +33,7 @@ Inductive WeakTypeVar := weakTypeVar : CoreVar -> Kind -> WeakTypeVar.
 Inductive WeakType :=
 | WTyVarTy  : WeakTypeVar                                      -> WeakType
 | WAppTy    : WeakType            ->                  WeakType -> WeakType
-| WTyFunApp : TyCon               ->             list WeakType -> WeakType
+| WTyFunApp : TyFun               ->             list WeakType -> WeakType
 | WTyCon    : TyCon                                            -> WeakType
 | WFunTyCon :                                                     WeakType    (* never use (WTyCon ArrowCon);    always use this! *)
 | WCodeTy   : WeakTypeVar         ->                  WeakType -> WeakType    (* never use the raw tycon *)
@@ -60,42 +67,19 @@ 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.
 
 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 tc lt                 => TyConApp tc (map weakTypeToCoreType' lt)
+    | 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)
@@ -113,9 +97,7 @@ Definition compare_weakTypes (w1 w2:WeakType) :=
     then true
     else false.
 
-(* Coq's "decide equality" can't cope here; we have to cheat for now *)
-Axiom compare_weakTypes_axiom : forall w1 w2, if compare_weakTypes w1 w2 then w1=w2 else not (w1=w2).
-
+(*
 Instance EqDecidableWeakType : EqDecidable WeakType.
   apply Build_EqDecidable.
   intros.
@@ -126,7 +108,8 @@ Instance EqDecidableWeakType : EqDecidable WeakType.
   left; auto.
   right; auto.
   Defined.
+*)
 
-Definition weakTypeToString : WeakType -> string :=
-  coreTypeToString ○ weakTypeToCoreType.
+Instance WeakTypeToString : ToString WeakType :=
+  { toString := coreTypeToString ○ weakTypeToCoreType }.