remove weakTypeOfWeakExpr and replaceWeakTypeVar, no longer required

diff --git a/src/HaskCoreToWeak.v b/src/HaskCoreToWeak.v
index a812483..1734637 100644 (file)
--- a/src/HaskCoreToWeak.v
+++ b/src/HaskCoreToWeak.v
@@ -14,6 +14,7 @@ Require Import HaskCore.
 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".
@@ -74,6 +75,9 @@ Fixpoint coreTypeToWeakType' (ct:CoreType) : ???WeakType :=
 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

diff --git a/src/HaskWeak.v b/src/HaskWeak.v
index 013c62a..8f2a526 100644 (file)
--- a/src/HaskWeak.v
+++ b/src/HaskWeak.v
@@ -8,6 +8,7 @@ Require Import General.
 Require Import Coq.Lists.List.
 Require Import HaskKinds.
 Require Import HaskCoreLiterals.
+Require Import HaskCore.
 Require Import HaskCoreVars.
 Require Import HaskCoreTypes.
 Require Import HaskCoreTypes.
@@ -98,43 +99,5 @@ Definition makeClosedExpression : WeakExpr -> WeakExpr :=
 Definition weakTypeOfLiteral (lit:HaskLiteral) : WeakType :=
   (WTyCon (haskLiteralToTyCon lit)).
 
-(* calculate the CoreType of a WeakExpr *)
-Fixpoint weakTypeOfWeakExpr (ce:WeakExpr) : ???WeakType :=
-  match ce with
-    | WEVar   (weakExprVar v t) => OK t
-    | WELit   lit   => OK (weakTypeOfLiteral lit)
-    | WEApp   e1 e2 => weakTypeOfWeakExpr e1 >>= fun t' =>
-                       match t' with
-                         | (WAppTy (WAppTy WFunTyCon t1) t2) => OK t2
-                         | _ => Error ("found non-function type "+++t'+++" in EApp")
-                       end
-    | WETyApp e t    => weakTypeOfWeakExpr e >>= fun te =>
-                        match te with
-                          | WForAllTy v ct => OK (replaceWeakTypeVar ct v t)
-                          | _ => Error ("found non-forall type "+++te+++" in ETyApp")
-                        end
-    | WECoApp e co   => weakTypeOfWeakExpr e >>= fun te =>
-                        match te with
-                          | WCoFunTy t1 t2 t => OK t
-                          | _ => Error ("found non-coercion type "+++te+++" in ETyApp")
-                        end
-    | WELam   (weakExprVar ev vt) e => weakTypeOfWeakExpr e >>= fun t' => OK (WAppTy (WAppTy WFunTyCon vt) t')
-    | WETyLam tv e => weakTypeOfWeakExpr e >>= fun t' => OK (WForAllTy tv t')
-    | WECoLam (weakCoerVar cv _ φ₁ φ₂) e => weakTypeOfWeakExpr e >>= fun t' => OK (WCoFunTy φ₁ φ₂ t')
-    | WELet   ev ve e            => weakTypeOfWeakExpr e
-    | WELetRec rb e              => weakTypeOfWeakExpr e
-    | WENote  n e                => weakTypeOfWeakExpr e
-    | WECast  e (weakCoercion _ t1 t2 _) => OK t2
-    | WECase  vscrut scrutinee tbranches tc type_params alts => OK tbranches
-
-    (* note that we willfully ignore the type stashed in WEBrak/WEEsc here *)
-    | WEBrak _ ec e _ => weakTypeOfWeakExpr e >>= fun t' => OK (WCodeTy ec t')
-    | WEEsc  _ ec e _ => weakTypeOfWeakExpr e >>= fun t' =>
-      match t' with
-        | (WAppTy (WAppTy WCodeTyCon (WTyVarTy ec')) t'') =>
-          if eqd_dec ec ec' then OK t''
-            else Error "level mismatch in escapification"
-        | _ => Error "ill-typed escapification"
-      end
-  end.
-
+Variable coreTypeOfCoreExpr    : @CoreExpr CoreVar -> CoreType.
+  Extract Inlined Constant coreTypeOfCoreExpr => "CoreUtils.exprType".

diff --git a/src/HaskWeakToCore.v b/src/HaskWeakToCore.v
index cb3d7a3..7d0fac4 100644 (file)
--- a/src/HaskWeakToCore.v
+++ b/src/HaskWeakToCore.v
@@ -15,7 +15,6 @@ Require Import HaskCore.
 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".

diff --git a/src/HaskWeakToStrong.v b/src/HaskWeakToStrong.v
index a15b81d..3d8137f 100644 (file)
--- a/src/HaskWeakToStrong.v
+++ b/src/HaskWeakToStrong.v
@@ -18,6 +18,7 @@ Require Import HaskStrongTypes.
 Require Import HaskStrong.
 Require Import HaskCoreTypes.
 Require Import HaskCoreVars.
+Require Import HaskCoreToWeak.
 
 Open Scope string_scope.
 Definition TyVarResolver Γ   := forall wt:WeakTypeVar, HaskTyVar Γ wt.

diff --git a/src/HaskWeakTypes.v b/src/HaskWeakTypes.v
index 6b6b61e..593bccf 100644 (file)
--- a/src/HaskWeakTypes.v
+++ b/src/HaskWeakTypes.v
@@ -67,30 +67,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.