store the scrutinee CoreVar in WeakExpr Case to simplify WeakExprToCoreExpr

diff --git a/src/HaskCoreToWeak.v b/src/HaskCoreToWeak.v
index 6fc5b43..a812483 100644 (file)
--- a/src/HaskCoreToWeak.v
+++ b/src/HaskCoreToWeak.v
@@ -200,7 +200,10 @@ Fixpoint coreExprToWeakExpr (ce:@CoreExpr CoreVar) : ???WeakExpr :=
           >>= fun branches =>
             coreExprToWeakExpr e >>= fun scrutinee =>
               coreTypeToWeakType tbranches >>= fun tbranches' =>
-                  OK (WELet ev scrutinee (WECase (WEVar ev) tbranches' tc lt (unleaves branches)))
+                  OK (WECase ev scrutinee tbranches' tc lt (unleaves branches))
       end
   end.
 
+
+
+

diff --git a/src/HaskStrongToWeak.v b/src/HaskStrongToWeak.v
index ea76856..7fcea20 100644 (file)
--- a/src/HaskStrongToWeak.v
+++ b/src/HaskStrongToWeak.v
@@ -98,6 +98,7 @@ match exp as E in @Expr _ _ G D X L return InstantiatedTypeEnv (fun _ => WeakTyp
 | ECoApp Γ Δ κ σ₁ σ₂ γ σ ξ l e  => fun ite => WECoApp (strongExprToWeakExpr ftv fcv e ite) (strongCoercionToWeakCoercion γ ite)
 | ECase Γ Δ ξ l tc tbranches atypes e alts =>
   fun ite => WECase
+    FIXME
     (strongExprToWeakExpr ftv fcv e ite)
     (@typeToWeakType ftv Γ _ tbranches ite)
     tc

diff --git a/src/HaskWeak.v b/src/HaskWeak.v
index e5a2bfb..013c62a 100644 (file)
--- a/src/HaskWeak.v
+++ b/src/HaskWeak.v
@@ -35,8 +35,8 @@ Inductive WeakExpr :=
 | 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)
+| WECase      : forall (vscrut:WeakExprVar)
+                       (scrutinee:WeakExpr)
                        (tbranches:WeakType)
                        (tc:TyCon)
                        (type_params:list WeakType)
@@ -125,7 +125,7 @@ Fixpoint weakTypeOfWeakExpr (ce:WeakExpr) : ???WeakType :=
     | WELetRec rb e              => weakTypeOfWeakExpr e
     | WENote  n e                => weakTypeOfWeakExpr e
     | WECast  e (weakCoercion _ t1 t2 _) => OK t2
-    | WECase  scrutinee tbranches tc type_params alts => OK tbranches
+    | 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')

diff --git a/src/HaskWeakToCore.v b/src/HaskWeakToCore.v
index 24eedc6..cb3d7a3 100644 (file)
--- a/src/HaskWeakToCore.v
+++ b/src/HaskWeakToCore.v
@@ -31,43 +31,38 @@ Variable trustMeCoercion           : CoreCoercion.
 Variable coreCoercionsAreReallyTypes : CoreCoercion -> CoreType.
   Extract Inlined Constant coreCoercionsAreReallyTypes => "(\x -> x)".
 
-Section HaskWeakToCore.
+Definition weakCoercionToCoreCoercion : WeakCoercion -> CoreCoercion :=
+   fun _ => trustMeCoercion.
 
-  (* the CoreVar for the "magic" bracket/escape identifiers must be created from within one of the monads *)
-  Context (hetmet_brak_var : CoreVar).
-  Context (hetmet_esc_var  : CoreVar).
 
-  Definition weakCoercionToCoreCoercion : WeakCoercion -> CoreCoercion :=
-    fun _ => trustMeCoercion.
-
-  Fixpoint weakExprToCoreExpr (f:Fresh unit (fun _ => WeakExprVar)) (me:WeakExpr) : @CoreExpr CoreVar :=
+  Fixpoint weakExprToCoreExpr (me:WeakExpr) : @CoreExpr CoreVar :=
   match me with
   | WEVar   (weakExprVar v _)            => CoreEVar  v
   | WELit   lit                          => CoreELit  lit
-  | WEApp   e1 e2                        => CoreEApp     (weakExprToCoreExpr f e1) (weakExprToCoreExpr f e2)
-  | WETyApp e t                          => CoreEApp     (weakExprToCoreExpr f e ) (CoreEType (weakTypeToCoreType t))
-  | WECoApp e co                         => CoreEApp     (weakExprToCoreExpr f e )
+  | WEApp   e1 e2                        => CoreEApp     (weakExprToCoreExpr e1) (weakExprToCoreExpr e2)
+  | WETyApp e t                          => CoreEApp     (weakExprToCoreExpr e ) (CoreEType (weakTypeToCoreType t))
+  | WECoApp e co                         => CoreEApp     (weakExprToCoreExpr e )
                                                            (CoreEType (coreCoercionsAreReallyTypes (weakCoercionToCoreCoercion co)))
-  | WENote  n e                          => CoreENote n  (weakExprToCoreExpr f e )
-  | WELam   (weakExprVar ev _  ) e       => CoreELam  ev (weakExprToCoreExpr f e )
-  | 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)
+  | WENote  n e                          => CoreENote n  (weakExprToCoreExpr e )
+  | WELam   (weakExprVar ev _  ) e       => CoreELam  ev (weakExprToCoreExpr e )
+  | WETyLam (weakTypeVar tv _  ) e       => CoreELam  tv (weakExprToCoreExpr e )
+  | WECoLam (weakCoerVar cv _ _ _) e     => CoreELam  cv (weakExprToCoreExpr e )
+  | WECast  e co                         => CoreECast    (weakExprToCoreExpr e ) (weakCoercionToCoreCoercion co)
   | WEBrak  v (weakTypeVar ec _) e t     => fold_left CoreEApp
                                                    ((CoreEType (TyVarTy ec))::
                                                      (CoreEType (weakTypeToCoreType t))::
-                                                     (weakExprToCoreExpr f e)::
+                                                     (weakExprToCoreExpr e)::
                                                      nil)
                                                    (CoreEVar v)
   | WEEsc   v (weakTypeVar ec _) e t     => fold_left CoreEApp
                                                    ((CoreEType (TyVarTy ec))::
                                                      (CoreEType (weakTypeToCoreType t))::
-                                                     (weakExprToCoreExpr f e)::
+                                                     (weakExprToCoreExpr 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)
+  | 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)
                                               (sortAlts ((
                                                 fix mkCaseBranches (alts:Tree 
                                                   ??(AltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) :=
@@ -80,19 +75,19 @@ Section HaskWeakToCore.
                                                         (map (fun v:WeakTypeVar => weakVarToCoreVar v) tvars)
                                                         (map (fun v:WeakCoerVar => weakVarToCoreVar v) cvars))
                                                       (map (fun v:WeakExprVar => weakVarToCoreVar v) evars))
-                                                      (weakExprToCoreExpr f' e))::nil
+                                                      (weakExprToCoreExpr e))::nil
                                                 end
                                               ) alts))
   | WELetRec mlr e                       => CoreELet (CoreRec
                                                ((fix mkLetBindings (mlr:Tree ??(WeakExprVar * WeakExpr)) :=
                                                  match mlr with
                                                    | T_Leaf None                        => nil
-                                                   | T_Leaf (Some (weakExprVar cv _,e)) => (cv,(weakExprToCoreExpr f e))::nil
+                                                   | T_Leaf (Some (weakExprVar cv _,e)) => (cv,(weakExprToCoreExpr e))::nil
                                                    | T_Branch b1 b2                     => app (mkLetBindings b1) (mkLetBindings b2)
                                                  end) mlr))
-                                               (weakExprToCoreExpr f e)
+                                               (weakExprToCoreExpr e)
   end.
 
-End HaskWeakToCore.
+
 
 

diff --git a/src/HaskWeakToStrong.v b/src/HaskWeakToStrong.v
index cd4b17b..a15b81d 100644 (file)
--- a/src/HaskWeakToStrong.v
+++ b/src/HaskWeakToStrong.v
@@ -558,16 +558,16 @@ Definition weakExprToStrongExpr : forall
            weakExprToStrongExpr Γ Δ φ ψ ξ' τ lev e >>= fun e' =>       
              OK (ELetRec Γ Δ ξ lev τ _ binds' e')
 
-    | WECase  e tbranches tc avars alts =>
+    | WECase vscrut e tbranches tc avars alts =>
       mkAvars avars (tyConKind tc) φ >>= fun avars' =>
       weakTypeToType'' φ tbranches ★  >>= fun tbranches' =>
-        weakExprToStrongExpr Γ Δ φ ψ ξ (caseType tc avars') lev e >>= fun e' =>
+          let ξ' := update_ξ ξ (((vscrut:CoreVar), _ @@lev)::nil) in
 (fix mkTree (t:Tree ??(AltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) : ???(Tree
      ??{scb
        : StrongCaseBranchWithVVs CoreVar CoreVarEqDecidable tc avars'
        &
        Expr (sac_Γ scb Γ) (sac_Δ scb Γ avars' (weakCK'' Δ))
-         (scbwv_ξ scb ξ lev) (weakLT' (tbranches' @@  lev))}) := 
+         (scbwv_ξ scb ξ' lev) (weakLT' (tbranches' @@  lev))}) := 
         match t with
           | T_Leaf None           => OK []
           | T_Leaf (Some (ac,extyvars,coervars,exprvars,ebranch)) => 
@@ -575,7 +575,7 @@ Definition weakExprToStrongExpr : forall
               list2vecOrFail (map (fun ev:WeakExprVar => ev:CoreVar) exprvars) _ (fun _ _ => "WECase") >>= fun exprvars' =>
                 let scb := @Build_StrongCaseBranchWithVVs CoreVar CoreVarEqDecidable tc Γ avars' sac exprvars' in
                   weakExprToStrongExpr (sac_Γ scb Γ) (sac_Δ scb Γ avars' (weakCK'' Δ)) (sacpj_φ sac _ φ) (sacpj_ψ sac _ _ avars' ψ)
-            (scbwv_ξ scb ξ lev) (weakT' tbranches') (weakL' lev) ebranch >>= fun ebranch' =>
+            (scbwv_ξ scb ξ' lev) (weakT' tbranches') (weakL' lev) ebranch >>= fun ebranch' =>
             let case_case := tt in OK [ _ ]
           | T_Branch b1 b2        =>
             mkTree b1 >>= fun b1' =>
@@ -583,7 +583,10 @@ Definition weakExprToStrongExpr : forall
                 OK (b1',,b2')
         end
 ) alts >>= fun tree =>
-          castExpr "ECase" _ (ECase Γ Δ ξ lev tc tbranches' avars' e' tree)
+        weakExprToStrongExpr Γ Δ φ ψ ξ (caseType tc avars') lev e >>= fun e' =>
+          castExpr "ECaseScrut" _ (EVar Γ Δ ξ' vscrut) >>= fun evar =>
+            castExpr "ECase" _ (ECase Γ Δ ξ' lev tc tbranches' avars' evar tree) >>= fun ecase' =>
+              OK (ELet _ _ _ _ _ lev (vscrut:CoreVar) e' ecase')
     end)).
 
     destruct case_some.
@@ -600,7 +603,7 @@ Definition weakExprToStrongExpr : forall
       apply e1.
 
     destruct case_case.
-      clear mkTree t o e' p e p0 p1 p2 alts weakExprToStrongExpr ebranch.
+      clear mkTree t o p e p0 p1 p2 alts weakExprToStrongExpr ebranch.
       exists scb.
       apply ebranch'.
     Defined.