add support for CSP in HaskCore+HaskWeak

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

diff --git a/src/HaskWeakToCore.v b/src/HaskWeakToCore.v
index 88c6830..9607d5f 100644 (file)
--- a/src/HaskWeakToCore.v
+++ b/src/HaskWeakToCore.v
@@ -15,6 +15,7 @@ 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".
@@ -23,18 +24,17 @@ Variable sortAlts  : forall {a}{b}, list (@triple AltCon a b) -> list (@triple A
   Extract Inlined Constant sortAlts => "sortAlts".
   Implicit Arguments sortAlts [[a][b]].
 
-Variable trustMeCoercion           : CoreCoercion.
-  Extract Inlined Constant trustMeCoercion => "Coercion.unsafeCoerce".
+Variable mkUnsafeCoercion : CoreType -> CoreType -> CoreCoercion.
+    Extract Inlined Constant mkUnsafeCoercion => "Coercion.mkUnsafeCoercion".
 
 (* Coercion and Type are actually the same thing in GHC, but we don't tell Coq about that.  This lets us get around it. *)
 Variable coreCoercionsAreReallyTypes : CoreCoercion -> CoreType.
   Extract Inlined Constant coreCoercionsAreReallyTypes => "(\x -> x)".
 
-Definition weakCoercionToCoreCoercion : WeakCoercion -> CoreCoercion :=
-   fun _ => trustMeCoercion.
+Definition weakCoercionToCoreCoercion (wc:WeakCoercion) : CoreCoercion :=
+  mkUnsafeCoercion (weakTypeToCoreType (fst (weakCoercionTypes wc))) (weakTypeToCoreType (snd (weakCoercionTypes wc))).
 
-
-  Fixpoint weakExprToCoreExpr (me:WeakExpr) : @CoreExpr CoreVar :=
+Fixpoint weakExprToCoreExpr (me:WeakExpr) : @CoreExpr CoreVar :=
   match me with
   | WEVar   (weakExprVar v _)            => CoreEVar  v
   | WELit   lit                          => CoreELit  lit
@@ -59,6 +59,12 @@ Definition weakCoercionToCoreCoercion : WeakCoercion -> CoreCoercion :=
                                                      (weakExprToCoreExpr e)::
                                                      nil)
                                                    (CoreEVar v)
+  | WECSP   v (weakTypeVar ec _) e t     => fold_left CoreEApp
+                                                   ((CoreEType (TyVarTy ec))::
+                                                     (CoreEType (weakTypeToCoreType t))::
+                                                     (weakExprToCoreExpr e)::
+                                                     nil)
+                                                   (CoreEVar v)
   | WELet   (weakExprVar v _) ve e       => mkCoreLet      (CoreNonRec v (weakExprToCoreExpr ve))  (weakExprToCoreExpr e)
   | WECase  vscrut e tbranches tc types alts  =>
                                             CoreECase (weakExprToCoreExpr e) vscrut (weakTypeToCoreType tbranches)
@@ -87,8 +93,9 @@ Definition weakCoercionToCoreCoercion : WeakCoercion -> CoreCoercion :=
                                                (weakExprToCoreExpr e)
   end.
 
+Definition weakTypeOfWeakExpr (we:WeakExpr) : ???WeakType :=
+  coreTypeToWeakType (coreTypeOfCoreExpr (weakExprToCoreExpr we)).
 
 Instance weakExprToString : ToString WeakExpr  :=
   { toString := fun we => toString (weakExprToCoreExpr we) }.
 
-