add support for hetmet_unflatten

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

diff --git a/src/HaskFlattener.v b/src/HaskFlattener.v
index 6d9d7a6..e8aceb1 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 HaskCoreVars.
+Require Import HaskWeakTypes.
+Require Import HaskWeakVars.
 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 HaskWeakToStrong.
 
 Open Scope nd_scope.
 
@@ -194,14 +198,17 @@ Section HaskFlattener.
 
   Set Printing Width 130.
 
+  Context (hetmet_flatten : WeakExprVar).
+  Context (hetmet_unflatten : 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 ★  -> RawHaskType TV ★ -> RawHaskType TV ★  -> RawHaskType TV ★ }.
+  Context {gaTy   : forall TV, RawHaskType TV ECKind  -> RawHaskType TV ★ -> RawHaskType TV ★  -> RawHaskType TV ★ }.
 
   Definition ga_mk_tree {Γ} (tr:Tree ??(HaskType Γ ★)) : HaskType Γ ★ :=
     fun TV ite => reduceTree (unitTy TV) (prodTy TV) (mapOptionTree (fun x => x TV ite) tr).
 
-  Definition ga_mk {Γ}(ec:HaskType Γ ★ )(ant suc:Tree ??(HaskType Γ ★)) : HaskType Γ ★ :=
+  Definition ga_mk {Γ}(ec:HaskType Γ ECKind )(ant suc:Tree ??(HaskType Γ ★)) : HaskType Γ ★ :=
     fun TV ite => gaTy TV (ec TV ite) (ga_mk_tree ant TV ite) (ga_mk_tree suc TV ite).
 
   Class garrow :=
@@ -257,7 +264,7 @@ Section HaskFlattener.
     fun TV ite =>
       garrowfy_raw_codetypes (ht TV ite).
 
-  Definition v2t {Γ}(ec:HaskTyVar Γ ★) := fun TV ite => TVar (ec TV ite).
+  Definition v2t {Γ}(ec:HaskTyVar Γ ECKind) := fun TV ite => TVar (ec TV ite).
 
   Fixpoint garrowfy_leveled_code_types' {Γ}(ht:HaskType Γ ★)(lev:HaskLevel Γ) : HaskType Γ ★ :=
     match lev with
@@ -509,7 +516,7 @@ Section HaskFlattener.
 *)
   Definition garrowfy_arrangement' :
     forall Γ (Δ:CoercionEnv Γ)
-      (ec:HaskTyVar Γ ★) (lev:HaskLevel Γ) (ant1 ant2:Tree ??(LeveledHaskType Γ ★)) (r:Arrange ant1 ant2),
+      (ec:HaskTyVar Γ ECKind) (lev:HaskLevel Γ) (ant1 ant2:Tree ??(LeveledHaskType Γ ★)) (r:Arrange ant1 ant2),
       ND Rule [] [Γ > Δ > [] |- [@ga_mk _ (v2t ec) (take_lev (ec :: lev) ant2) (take_lev (ec :: lev) ant1) @@ nil] ].
 
       intros Γ Δ ec lev.
@@ -554,7 +561,7 @@ Section HaskFlattener.
 
   Definition garrowfy_arrangement :
     forall Γ (Δ:CoercionEnv Γ) n
-      (ec:HaskTyVar Γ ★) (lev:HaskLevel Γ) (ant1 ant2:Tree ??(LeveledHaskType Γ ★)) (r:Arrange ant1 ant2) succ,
+      (ec:HaskTyVar Γ ECKind) (lev:HaskLevel Γ) (ant1 ant2:Tree ??(LeveledHaskType Γ ★)) (r:Arrange ant1 ant2) succ,
       ND Rule
       [Γ > Δ > mapOptionTree (garrowfy_leveled_code_types ) (drop_lev n ant1)
         |- [@ga_mk _ (v2t ec) (take_lev (ec :: lev) ant1) (mapOptionTree (unlev' ) succ) @@ nil]]
@@ -900,7 +907,23 @@ Section HaskFlattener.
       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.
+        destruct (eqd_dec (g:CoreVar) (hetmet_unflatten: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.