add support for hetmet_flatten casting variable

diff --git a/src/ExtractionMain.v b/src/ExtractionMain.v
index 350506e..ebf4e77 100644 (file)
--- a/src/ExtractionMain.v
+++ b/src/ExtractionMain.v
@@ -164,9 +164,11 @@ Section core2proof.
     Definition mkWeakExprVar (u:Unique)(t:WeakType)             : WeakExprVar :=
       weakExprVar (mkExVar (mkSystemName u "ev" O) (weakTypeToCoreType t)) t.
 
     Definition mkWeakExprVar (u:Unique)(t:WeakType)             : WeakExprVar :=
       weakExprVar (mkExVar (mkSystemName u "ev" O) (weakTypeToCoreType t)) t.
 

-    Context (hetmet_brak  : WeakExprVar).
-    Context (hetmet_esc   : WeakExprVar).
-    Context (uniqueSupply : UniqSupply).
+    Context (hetmet_brak    : WeakExprVar).
+    Context (hetmet_esc     : WeakExprVar).
+    Context (hetmet_flatten : WeakExprVar).
+    Context (hetmet_flattened_id : WeakExprVar).
+    Context (uniqueSupply   : UniqSupply).

 
     Definition useUniqueSupply {T}(ut:UniqM T) : ???T :=
       match ut with
 
     Definition useUniqueSupply {T}(ut:UniqM T) : ???T :=
       match ut with

@@ -270,6 +272,8 @@ Section core2proof.
     Context
     (hetmet_brak  : CoreVar)
     (hetmet_esc   : CoreVar)
     Context
     (hetmet_brak  : CoreVar)
     (hetmet_esc   : CoreVar)

+    (hetmet_flatten : CoreVar)
+    (hetmet_flattened_id : CoreVar)

     (uniqueSupply : UniqSupply)
     (lbinds:list (@CoreBind CoreVar))
     (hetmet_PGArrowTyCon : TyFun)
     (uniqueSupply : UniqSupply)
     (lbinds:list (@CoreBind CoreVar))
     (hetmet_PGArrowTyCon : TyFun)

@@ -391,6 +395,8 @@ Section core2proof.
 
     Definition hetmet_brak' := coreVarToWeakExprVarOrError hetmet_brak.
     Definition hetmet_esc'  := coreVarToWeakExprVarOrError hetmet_esc.
 
     Definition hetmet_brak' := coreVarToWeakExprVarOrError hetmet_brak.
     Definition hetmet_esc'  := coreVarToWeakExprVarOrError hetmet_esc.

+    Definition hetmet_flatten'  := coreVarToWeakExprVarOrError hetmet_flatten.
+    Definition hetmet_flattened_id'  := coreVarToWeakExprVarOrError hetmet_flattened_id.

 
     Definition coreToCoreExpr' (ce:@CoreExpr CoreVar) : ???(@CoreExpr CoreVar) :=
       addErrorMessage ("input CoreSyn: " +++ toString ce)
 
     Definition coreToCoreExpr' (ce:@CoreExpr CoreVar) : ???(@CoreExpr CoreVar) :=
       addErrorMessage ("input CoreSyn: " +++ toString ce)

@@ -405,12 +411,13 @@ Section core2proof.
                     ((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => true) τ nil we) >>= fun e =>
 
                       (addErrorMessage ("HaskStrong...")
                     ((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => true) τ nil we) >>= fun e =>
 
                       (addErrorMessage ("HaskStrong...")

-                        (let haskProof := flatten_proof my_ga (@expr2proof _ _ _ _ _ _ e)
+                        (let haskProof := flatten_proof hetmet_flatten' hetmet_flattened_id' my_ga (@expr2proof _ _ _ _ _ _ e)

                          in (* insert HaskProof-to-HaskProof manipulations here *)
                          OK ((@proof2expr nat _ FreshNat _ _ _ _ (fun _ => Prelude_error "unbound unique") _ haskProof) O)
                          >>= fun e' =>
                            (snd e') >>= fun e'' =>
                          in (* insert HaskProof-to-HaskProof manipulations here *)
                          OK ((@proof2expr nat _ FreshNat _ _ _ _ (fun _ => Prelude_error "unbound unique") _ haskProof) O)
                          >>= fun e' =>
                            (snd e') >>= fun e'' =>

-                         strongExprToWeakExpr hetmet_brak' hetmet_esc' mkWeakTypeVar mkWeakCoerVar mkWeakExprVar uniqueSupply
+                         strongExprToWeakExpr hetmet_brak' hetmet_esc'
+                           mkWeakTypeVar mkWeakCoerVar mkWeakExprVar uniqueSupply

                            (projT2 e'') INil
                          >>= fun q =>
                            OK (weakExprToCoreExpr q)
                            (projT2 e'') INil
                          >>= fun q =>
                            OK (weakExprToCoreExpr q)

@@ -446,6 +453,8 @@ Section core2proof.
     Definition coqPassCoreToCore 
     (hetmet_brak  : CoreVar)
     (hetmet_esc   : CoreVar)
     Definition coqPassCoreToCore 
     (hetmet_brak  : CoreVar)
     (hetmet_esc   : CoreVar)

+    (hetmet_flatten   : CoreVar)
+    (hetmet_flattened_id   : CoreVar)

     (uniqueSupply : UniqSupply)
     (lbinds:list (@CoreBind CoreVar))
     (hetmet_PGArrowTyCon : TyFun)
     (uniqueSupply : UniqSupply)
     (lbinds:list (@CoreBind CoreVar))
     (hetmet_PGArrowTyCon : TyFun)

@@ -469,6 +478,8 @@ Section core2proof.
     coqPassCoreToCore'
        hetmet_brak  
        hetmet_esc   
     coqPassCoreToCore'
        hetmet_brak  
        hetmet_esc   

+       hetmet_flatten
+       hetmet_flattened_id

        uniqueSupply 
        hetmet_PGArrowTyCon
        hetmet_pga_id 
        uniqueSupply 
        hetmet_PGArrowTyCon
        hetmet_pga_id 

diff --git a/src/HaskFlattener.v b/src/HaskFlattener.v
index 60a205f..5e16f56 100644 (file)
--- a/src/HaskFlattener.v
+++ b/src/HaskFlattener.v
@@ -14,6 +14,9 @@ Require Import Coq.Lists.List.
 
 Require Import HaskKinds.
 Require Import HaskCoreTypes.
 
 Require Import HaskKinds.
 Require Import HaskCoreTypes.

+Require Import HaskCoreVars.
+Require Import HaskWeakTypes.
+Require Import HaskWeakVars.

 Require Import HaskLiteralsAndTyCons.
 Require Import HaskStrongTypes.
 Require Import HaskProof.
 Require Import HaskLiteralsAndTyCons.
 Require Import HaskStrongTypes.
 Require Import HaskProof.

@@ -24,6 +27,7 @@ Require Import HaskStrong.
 Require Import HaskProof.
 Require Import HaskStrongToProof.
 Require Import HaskProofToStrong.
 Require Import HaskProof.
 Require Import HaskStrongToProof.
 Require Import HaskProofToStrong.

+Require Import HaskWeakToStrong.

 
 Open Scope nd_scope.
 
 
 Open Scope nd_scope.
 

@@ -194,6 +198,8 @@ Section HaskFlattener.
 
   Set Printing Width 130.
 
 
   Set Printing Width 130.
 

+  Context (hetmet_flatten : WeakExprVar).
+  Context (hetmet_id      : WeakExprVar).

   Context {unitTy : forall TV, RawHaskType TV ★                                          }.
   Context {prodTy : forall TV, RawHaskType TV ★  -> RawHaskType TV ★ -> RawHaskType TV ★ }.
   Context {gaTy   : forall TV, RawHaskType TV ECKind  -> RawHaskType TV ★ -> RawHaskType TV ★  -> RawHaskType TV ★ }.
   Context {unitTy : forall TV, RawHaskType TV ★                                          }.
   Context {prodTy : forall TV, RawHaskType TV ★  -> RawHaskType TV ★ -> RawHaskType TV ★ }.
   Context {gaTy   : forall TV, RawHaskType TV ECKind  -> RawHaskType TV ★ -> RawHaskType TV ★  -> RawHaskType TV ★ }.

@@ -900,7 +906,16 @@ Section HaskFlattener.
       simpl.
       rename l into g.
       rename σ into l.
       simpl.
       rename l into g.
       rename σ into l.

-      destruct l as [|ec lev]; simpl; [ apply nd_rule; rewrite globals_do_not_have_code_types; apply RGlobal; auto | idtac ].
+      destruct l as [|ec lev]; simpl. 
+        destruct (eqd_dec (g:CoreVar) (hetmet_flatten:CoreVar)).
+          set (garrowfy_code_types (g wev)) as t.
+          set (RGlobal _ Δ nil (mkGlobal Γ t hetmet_id)) as q.
+          simpl in q.
+          apply nd_rule.
+          apply q.
+          apply INil.
+        apply nd_rule; rewrite globals_do_not_have_code_types.
+          apply RGlobal.

       apply (Prelude_error "found RGlobal at depth >0").
 
     destruct case_RLam.
       apply (Prelude_error "found RGlobal at depth >0").
 
     destruct case_RLam.