remove weakTypeOfWeakExpr and replaceWeakTypeVar, no longer required

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

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 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".

@@ -74,6 +75,9 @@ 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