add support for CSP in HaskCore+HaskWeak

diff --git a/src/HaskCoreToWeak.v b/src/HaskCoreToWeak.v
index d47ab0c..1be33fd 100644 (file)
--- a/src/HaskCoreToWeak.v
+++ b/src/HaskCoreToWeak.v
@@ -23,11 +23,10 @@ Variable coreCoercionToWeakCoercion : CoreCoercion -> WeakCoercion.
 (* extracts the Name from a CoreVar *)
 Variable coreVarCoreName    : CoreVar -> CoreName.   Extract Inlined Constant coreVarCoreName  => "Var.varName".
 
-(* the magic wired-in name for the modal type introduction form *)
+(* the magic wired-in name for the modal type introduction/elimination forms *)
 Variable hetmet_brak_name   : CoreName.              Extract Inlined Constant hetmet_brak_name => "PrelNames.hetmet_brak_name".
-
-(* the magic wired-in name for the modal type elimination form *)
 Variable hetmet_esc_name    : CoreName.              Extract Inlined Constant hetmet_esc_name  => "PrelNames.hetmet_esc_name".
+Variable hetmet_csp_name    : CoreName.              Extract Inlined Constant hetmet_csp_name  => "PrelNames.hetmet_csp_name".
 
 Fixpoint coreTypeToWeakType' (ct:CoreType) : ???WeakType :=
   match ct with
@@ -109,6 +108,18 @@ match ce with
   | _ => None
 end.
 
+Definition isCSP (ce:@CoreExpr CoreVar) : ??(CoreVar * WeakTypeVar * CoreType) :=
+match ce with
+  | (CoreEApp (CoreEApp (CoreEVar v) (CoreEType (TyVarTy ec))) (CoreEType tbody))
+    => if coreName_eq hetmet_csp_name (coreVarCoreName v) then
+      match coreVarToWeakVar ec with
+        | WExprVar _  => None
+        | WTypeVar tv => Some (v,tv,tbody)
+        | WCoerVar _  => None
+      end else None
+  | _ => None
+end.
+
 (* if this is a (WAppTy (WAppTy ... (WTyCon tc) .. ) .. ), return (tc,[...]) *)
 Fixpoint expectTyConApp (wt:WeakType)(acc:list WeakType) : ???(TyCon * list WeakType) :=
   match wt with
@@ -142,13 +153,20 @@ Fixpoint coreExprToWeakExpr (ce:@CoreExpr CoreVar) : ???WeakExpr :=
                                              coreExprToWeakExpr e2 >>= fun e' =>
                                                coreTypeToWeakType t >>= fun t' =>
                                                  OK (WEEsc v tv e' t')
-                                           | None    => coreExprToWeakExpr e1 >>= fun e1' =>
-                                             match e2 with
-                                               | CoreEType t => 
-                                                 coreTypeToWeakType t >>= fun t' =>
-                                                   OK (WETyApp e1' t')
-                                               | _           => coreExprToWeakExpr e2 >>= fun e2' => OK (WEApp e1' e2')
-                                             end
+                                           | None    => match isCSP e1 with
+                                                          | Some (v,tv,t) =>
+                                                            coreExprToWeakExpr e2 >>= fun e' =>
+                                                              coreTypeToWeakType t >>= fun t' =>
+                                                                OK (WECSP v tv e' t')
+                                                          | None    => coreExprToWeakExpr e1 >>= fun e1' =>
+                                                            match e2 with
+                                                              | CoreEType t => 
+                                                                coreTypeToWeakType t >>= fun t' =>
+                                                                  OK (WETyApp e1' t')
+                                                              | _           => coreExprToWeakExpr e2
+                                                                >>= fun e2' => OK (WEApp e1' e2')
+                                                            end
+                                                        end
                                          end
                           end
 

diff --git a/src/HaskWeak.v b/src/HaskWeak.v
index 3c7b69c..60b7d04 100644 (file)
--- a/src/HaskWeak.v
+++ b/src/HaskWeak.v
@@ -35,6 +35,7 @@ Inductive WeakExpr :=
 (* or hetmet_esc identifier                                                *)
 | WEBrak      : CoreVar -> WeakTypeVar          -> WeakExpr  -> WeakType     -> WeakExpr
 | WEEsc       : CoreVar -> WeakTypeVar          -> WeakExpr  -> WeakType     -> WeakExpr
+| WECSP       : CoreVar -> WeakTypeVar          -> WeakExpr  -> WeakType     -> WeakExpr
 
 | WECase      : forall (vscrut:WeakExprVar)
                        (scrutinee:WeakExpr)

diff --git a/src/HaskWeakToCore.v b/src/HaskWeakToCore.v
index b6add94..9607d5f 100644 (file)
--- a/src/HaskWeakToCore.v
+++ b/src/HaskWeakToCore.v
@@ -59,6 +59,12 @@ Fixpoint weakExprToCoreExpr (me:WeakExpr) : @CoreExpr CoreVar :=
                                                      (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)

diff --git a/src/HaskWeakToStrong.v b/src/HaskWeakToStrong.v
index 1c3ba70..04e1055 100644 (file)
--- a/src/HaskWeakToStrong.v
+++ b/src/HaskWeakToStrong.v
@@ -501,6 +501,8 @@ Definition weakExprToStrongExpr : forall
                                                >>= fun e' => castExpr we "WEEsc" (τ@@lev) (EEsc Γ Δ ξ ec' tbody' lev' e')
                                            end
 
+    | WECSP   _ ec e tbody              => Error "FIXME: CSP not supported beyond HaskWeak stage"
+
     | WENote  n e                       => weakExprToStrongExpr Γ Δ φ ψ ξ τ lev e >>= fun e' => OK (ENote _ _ _ _ n e')
 
     | WELet   v ve  ebody               => weakTypeToTypeOfKind φ v ★  >>= fun tv =>