split HaskLiteralsAndTyCons into two files

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

diff --git a/src/HaskFlattener.v b/src/HaskFlattener.v
index 5e16f56..ae99605 100644 (file)
--- a/src/HaskFlattener.v
+++ b/src/HaskFlattener.v
@@ -17,7 +17,8 @@ Require Import HaskCoreTypes.
 Require Import HaskCoreVars.
 Require Import HaskWeakTypes.
 Require Import HaskWeakVars.
-Require Import HaskLiteralsAndTyCons.
+Require Import HaskLiterals.
+Require Import HaskTyCons.
 Require Import HaskStrongTypes.
 Require Import HaskProof.
 Require Import NaturalDeduction.
@@ -199,6 +200,7 @@ 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 ★ }.
@@ -914,6 +916,13 @@ Section HaskFlattener.
           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").