store the magic CoreVar for hetmet brak/esc in WeakExpr Esc/Brak

diff --git a/src/HaskCoreToWeak.v b/src/HaskCoreToWeak.v
index b538417..6fc5b43 100644 (file)
--- a/src/HaskCoreToWeak.v
+++ b/src/HaskCoreToWeak.v
@@ -75,24 +75,24 @@ Variable coreViewDeep : CoreType -> CoreType.  Extract Inlined Constant coreView
 Definition coreTypeToWeakType t := coreTypeToWeakType' (coreViewDeep t).
 
 (* detects our crude Core-encoding of modal type introduction/elimination forms *)
-Definition isBrak (ce:@CoreExpr CoreVar) : ??(WeakTypeVar * CoreType) :=
+Definition isBrak (ce:@CoreExpr CoreVar) : ??(CoreVar * WeakTypeVar * CoreType) :=
 match ce with
   | (CoreEApp (CoreEApp (CoreEVar v) (CoreEType (TyVarTy ec))) (CoreEType tbody))
     => if coreName_eq hetmet_brak_name (coreVarCoreName v) then
-      match coreVarToWeakVar v with
+      match coreVarToWeakVar ec with
         | WExprVar _  => None
-        | WTypeVar tv => Some (tv,tbody)
+        | WTypeVar tv => Some (v,tv,tbody)
         | WCoerVar _  => None
       end else None
   | _ => None
 end.
-Definition isEsc (ce:@CoreExpr CoreVar) : ??(WeakTypeVar * CoreType) :=
+Definition isEsc (ce:@CoreExpr CoreVar) : ??(CoreVar * WeakTypeVar * CoreType) :=
 match ce with
   | (CoreEApp (CoreEApp (CoreEVar v) (CoreEType (TyVarTy ec))) (CoreEType tbody))
     => if coreName_eq hetmet_esc_name (coreVarCoreName v) then
-      match coreVarToWeakVar v with
+      match coreVarToWeakVar ec with
         | WExprVar _  => None
-        | WTypeVar tv => Some (tv,tbody)
+        | WTypeVar tv => Some (v,tv,tbody)
         | WCoerVar _  => None
       end else None
   | _ => None
@@ -120,15 +120,15 @@ Fixpoint coreExprToWeakExpr (ce:@CoreExpr CoreVar) : ???WeakExpr :=
                           end
 
     | CoreEApp   e1 e2 => match isBrak e1 with
-                            | Some (tv,t) =>
+                            | Some (v,tv,t) =>
                               coreExprToWeakExpr e2 >>= fun e' =>
                                 coreTypeToWeakType t >>= fun t' =>
-                                OK (WEBrak tv e' t')
+                                OK (WEBrak v tv e' t')
                             | None    => match isEsc e1 with
-                                           | Some (tv,t) =>
+                                           | Some (v,tv,t) =>
                                              coreExprToWeakExpr e2 >>= fun e' =>
                                                coreTypeToWeakType t >>= fun t' =>
-                                                 OK (WEEsc tv e' t')
+                                                 OK (WEEsc v tv e' t')
                                            | None    => coreExprToWeakExpr e1 >>= fun e1' =>
                                              match e2 with
                                                | CoreEType t => 

diff --git a/src/HaskStrongToWeak.v b/src/HaskStrongToWeak.v
index a7f6b77..ea76856 100644 (file)
--- a/src/HaskStrongToWeak.v
+++ b/src/HaskStrongToWeak.v
@@ -72,6 +72,12 @@ Definition reindexStrongExpr {VV}{HH}{eqVV:EqDecidable VV}{eqHH:EqDecidable HH}
 Definition updateITE {Γ:TypeEnv}{TV:Kind->Type}{κ}(tv:TV κ)(ite:InstantiatedTypeEnv TV Γ) : InstantiatedTypeEnv TV (κ::Γ)
   := tv::::ite.
 
+Section strongExprToWeakExpr.
+
+  Context (hetmet_brak : CoreVar).
+  Context (hetmet_esc  : CoreVar).
+Axiom FIXME : forall {t}, t.
+
 Fixpoint strongExprToWeakExpr {Γ}{Δ}{ξ}{τ}
   (ftv:Fresh Kind                (fun _ => WeakTypeVar))
   (fcv:Fresh (WeakType*WeakType) (fun _ => WeakCoerVar))
@@ -83,8 +89,8 @@ match exp as E in @Expr _ _ G D X L return InstantiatedTypeEnv (fun _ => WeakTyp
 | EApp  Γ' _ _ _ _ _ e1 e2      => fun ite => WEApp (strongExprToWeakExpr ftv fcv e1 ite) (strongExprToWeakExpr ftv fcv e2 ite)
 | ELam  Γ'   _ _ _ t _ cv e     => fun ite => WELam (weakExprVar cv (typeToWeakType ftv t ite)) (strongExprToWeakExpr ftv fcv e ite)
 | ELet  Γ' _ _ t _ _ ev e1 e2   => fun ite => WELet (weakExprVar ev (typeToWeakType ftv t ite)) (strongExprToWeakExpr ftv fcv e1 ite) (strongExprToWeakExpr ftv fcv e2 ite)
-| EEsc  Γ' _ _ ec t _ e         => fun ite => WEEsc  (ec _ ite) (strongExprToWeakExpr ftv fcv e ite) (typeToWeakType ftv t ite)
-| EBrak Γ' _ _ ec t _ e         => fun ite => WEBrak (ec _ ite) (strongExprToWeakExpr ftv fcv e ite) (typeToWeakType ftv t ite)
+| EEsc  Γ' _ _ ec t _ e         => fun ite => WEEsc  hetmet_esc (ec _ ite) (strongExprToWeakExpr ftv fcv e ite) (typeToWeakType ftv t ite)
+| EBrak Γ' _ _ ec t _ e         => fun ite => WEBrak hetmet_brak (ec _ ite) (strongExprToWeakExpr ftv fcv e ite) (typeToWeakType ftv t ite)
 | ECast Γ Δ ξ t1 t2 γ l e       => fun ite => WECast (strongExprToWeakExpr ftv fcv e ite) (strongCoercionToWeakCoercion γ ite)
 | ENote _ _ _ _ n e             => fun ite => WENote n (strongExprToWeakExpr ftv fcv e ite)
 | ETyApp  Γ Δ κ σ τ ξ l       e => fun ite => WETyApp (strongExprToWeakExpr ftv fcv e ite) (typeToWeakType ftv τ ite)
@@ -137,3 +143,4 @@ match elrb as E in ELetRecBindings G D X L V
 | ELR_leaf   _ _ ξ' cv v e    => fun ite => [((weakExprVar v (typeToWeakType ftv (unlev (ξ' v)) ite)),(strongExprToWeakExpr ftv fcv e ite))]
 | ELR_branch _ _ _ _ _ _ b1 b2 => fun ite => (exprLetRec2WeakExprLetRec ftv fcv b1 ite),, (exprLetRec2WeakExprLetRec ftv fcv b2 ite)
 end.
+End strongExprToWeakExpr.
\ No newline at end of file

diff --git a/src/HaskWeak.v b/src/HaskWeak.v
index f177e1f..e5a2bfb 100644 (file)
--- a/src/HaskWeak.v
+++ b/src/HaskWeak.v
@@ -28,11 +28,12 @@ Inductive WeakExpr :=
 | WETyLam     : WeakTypeVar                     -> WeakExpr                  -> WeakExpr
 | WECoLam     : WeakCoerVar                     -> WeakExpr                  -> WeakExpr
 
-(* the WeakType argument in WEBrak/WEEsc is used only when going back    *)
-(* from Weak to Core; it lets us dodge a possibly-failing type           *)
-(* calculation                                                           *)
-| WEBrak      : WeakTypeVar                     -> WeakExpr  -> WeakType     -> WeakExpr
-| WEEsc       : WeakTypeVar                     -> WeakExpr  -> WeakType     -> WeakExpr
+(* The WeakType argument in WEBrak/WEEsc is used only when going back      *)
+(* from Weak to Core; it lets us dodge a possibly-failing type             *)
+(* calculation.  The CoreVar argument is the GlobalVar for the hetmet_brak *)
+(* or hetmet_esc identifier                                                *)
+| WEBrak      : CoreVar -> WeakTypeVar          -> WeakExpr  -> WeakType     -> WeakExpr
+| WEEsc       : CoreVar -> WeakTypeVar          -> WeakExpr  -> WeakType     -> WeakExpr
 
 (* note that HaskWeak "Case" does not bind a variable; coreExprToWeakExpr adds a let-binder *)
 | WECase      : forall (scrutinee:WeakExpr)
@@ -127,8 +128,8 @@ Fixpoint weakTypeOfWeakExpr (ce:WeakExpr) : ???WeakType :=
     | WECase  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' =>
+    | 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''

diff --git a/src/HaskWeakToCore.v b/src/HaskWeakToCore.v
index cfaf65e..24eedc6 100644 (file)
--- a/src/HaskWeakToCore.v
+++ b/src/HaskWeakToCore.v
@@ -53,10 +53,18 @@ Section HaskWeakToCore.
   | WETyLam (weakTypeVar tv _  ) e       => CoreELam  tv (weakExprToCoreExpr f e )
   | WECoLam (weakCoerVar cv _ _ _) e     => CoreELam  cv (weakExprToCoreExpr f e )
   | WECast  e co                         => CoreECast    (weakExprToCoreExpr f e ) (weakCoercionToCoreCoercion co)
-  | WEBrak  (weakTypeVar ec _) e t       => CoreEApp  (CoreEApp (CoreEVar hetmet_brak_var)
-                                                           (CoreEType (TyVarTy ec))) (CoreEType (weakTypeToCoreType t))
-  | WEEsc   (weakTypeVar ec _) e t       => CoreEApp  (CoreEApp (CoreEVar hetmet_esc_var)
-                                                           (CoreEType (TyVarTy ec))) (CoreEType (weakTypeToCoreType t))
+  | WEBrak  v (weakTypeVar ec _) e t     => fold_left CoreEApp
+                                                   ((CoreEType (TyVarTy ec))::
+                                                     (CoreEType (weakTypeToCoreType t))::
+                                                     (weakExprToCoreExpr f e)::
+                                                     nil)
+                                                   (CoreEVar v)
+  | WEEsc   v (weakTypeVar ec _) e t     => fold_left CoreEApp
+                                                   ((CoreEType (TyVarTy ec))::
+                                                     (CoreEType (weakTypeToCoreType t))::
+                                                     (weakExprToCoreExpr f e)::
+                                                     nil)
+                                                   (CoreEVar v)
   | WELet   (weakExprVar v _) ve e       => mkCoreLet      (CoreNonRec v (weakExprToCoreExpr f ve))  (weakExprToCoreExpr f e)
   | WECase  e tbranches tc types alts    => let (v,f') := next _ _ f tt  in
                                             CoreECase (weakExprToCoreExpr f' e) v (weakTypeToCoreType tbranches)

diff --git a/src/HaskWeakToStrong.v b/src/HaskWeakToStrong.v
index 3317445..cd4b17b 100644 (file)
--- a/src/HaskWeakToStrong.v
+++ b/src/HaskWeakToStrong.v
@@ -465,10 +465,10 @@ Definition weakExprToStrongExpr : forall
                                                     τ' _ e >>= fun e' =>
                                                    castExpr "WELam" _ (ELam Γ Δ ξ tv _ _ ev e')
 
-    | WEBrak  ec e tbody                => weakExprToStrongExpr Γ Δ φ ψ ξ τ ((φ (`ec))::lev) e >>= fun e' =>
+    | WEBrak  _ ec e tbody              => weakExprToStrongExpr Γ Δ φ ψ ξ τ ((φ (`ec))::lev) e >>= fun e' =>
                                              castExpr "WEBrak" _ (EBrak _ _ _ (φ (`ec)) _ lev e')
 
-    | WEEsc   ec e tbody                => weakTypeToType'' φ tbody ★ >>= fun tbody' =>
+    | WEEsc   _ ec e tbody              => weakTypeToType'' φ tbody ★ >>= fun tbody' =>
                                            match lev with
                                              | nil       => Error "ill-leveled escapification"
                                              | ec'::lev' => weakExprToStrongExpr Γ Δ φ ψ ξ (<[ φ (`ec) |- tbody' ]>) lev e