From: Adam Megacz <megacz@cs.berkeley.edu>
Date: Fri, 27 May 2011 02:39:42 +0000 (-0700)
Subject: partial support for LetRec in flattener
X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=commitdiff_plain;h=a9a60dc234f76a4740b32c0f62aa0fe3a89fea83;ds=sidebyside

partial support for LetRec in flattener
---

diff --git a/src/HaskFlattener.v b/src/HaskFlattener.v
index 308e669..08485a1 100644
--- a/src/HaskFlattener.v
+++ b/src/HaskFlattener.v
@@ -1220,8 +1220,29 @@ Section HaskFlattener.
 
     destruct case_RLetRec.
       rename t into lev.
+      simpl. destruct lev; simpl.
+      replace (getjlev (y @@@ nil)) with (nil: (HaskLevel Γ)).
+      replace (mapOptionTree flatten_leveled_type (y @@@ nil))
+        with  ((mapOptionTree flatten_type y) @@@ nil).
+      unfold flatten_leveled_type at 2.
       simpl.
-      apply (Prelude_error "LetRec not supported (FIXME)").
+      unfold flatten_leveled_type at 3.
+      simpl.
+      apply nd_rule.
+      set (@RLetRec Γ Δ (mapOptionTree flatten_leveled_type lri) (flatten_type x) (mapOptionTree flatten_type y) nil) as q.
+      simpl in q.
+      apply q.
+        induction y; try destruct a; auto.
+        simpl.
+        rewrite IHy1.
+        rewrite IHy2.
+        reflexivity.
+        induction y; try destruct a; auto.
+        simpl.
+        rewrite <- IHy1.
+        rewrite <- IHy2.
+        reflexivity.
+      apply (Prelude_error "LetRec not supported inside brackets yet (FIXME)").
 
     destruct case_RCase.
       simpl.