X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskFlattener.v;h=ae9960559b5e305fe0006142cdc247b9c5d2a3f2;hp=60a205fa94a0e2797bd10c134d111765f1f9ae30;hb=1c1cdb9014f409248ca96b677503719916b2b477;hpb=b4857a6f575dffd5c9c9d5decbc21ff63a338270

diff --git a/src/HaskFlattener.v b/src/HaskFlattener.v
index 60a205f..ae99605 100644
--- a/src/HaskFlattener.v
+++ b/src/HaskFlattener.v
@@ -14,7 +14,11 @@ Require Import Coq.Lists.List.
 
 Require Import HaskKinds.
 Require Import HaskCoreTypes.
-Require Import HaskLiteralsAndTyCons.
+Require Import HaskCoreVars.
+Require Import HaskWeakTypes.
+Require Import HaskWeakVars.
+Require Import HaskLiterals.
+Require Import HaskTyCons.
 Require Import HaskStrongTypes.
 Require Import HaskProof.
 Require Import NaturalDeduction.
@@ -24,6 +28,7 @@ Require Import HaskStrong.
 Require Import HaskProof.
 Require Import HaskStrongToProof.
 Require Import HaskProofToStrong.
+Require Import HaskWeakToStrong.
 
 Open Scope nd_scope.
 
@@ -194,6 +199,9 @@ 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 ECKind  -> RawHaskType TV ★ -> RawHaskType TV ★  -> RawHaskType TV ★ }.
@@ -900,7 +908,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.