From a9a60dc234f76a4740b32c0f62aa0fe3a89fea83 Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Thu, 26 May 2011 19:39:42 -0700 Subject: [PATCH] partial support for LetRec in flattener --- src/HaskFlattener.v | 23 ++++++++++++++++++++++- 1 file changed, 22 insertions(+), 1 deletion(-) 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. -- 1.7.10.4