X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskSkolemizer.v;h=eaf134141a8a7b8162c3ccccf35a4a4c781bd874;hp=435b687968922e3066467e7a89b2ddba38b51785;hb=3161a8a65cb0190e83d32bde613c3b64dfe31739;hpb=af41ffb1692ae207554342ccdc3bf73abaa75a01

diff --git a/src/HaskSkolemizer.v b/src/HaskSkolemizer.v
index 435b687..eaf1341 100644
--- a/src/HaskSkolemizer.v
+++ b/src/HaskSkolemizer.v
@@ -492,11 +492,43 @@ Section HaskSkolemizer.
         apply nd_rule.
         apply SFlat.
         apply (@RLetRec Γ Δ lri x y nil).
-        apply (Prelude_error "RLetRec at depth>0").
+        destruct (decide_tree_empty (mapOptionTreeAndFlatten take_arg_types_as_tree y @@@ (h :: t)));
+          [ idtac | apply (Prelude_error "used LetRec on a set of bindings involving a function type") ].
+        destruct (eqd_dec y (mapOptionTree drop_arg_types_as_tree y));
+          [ idtac | apply (Prelude_error "used LetRec on a set of bindings involving a function type") ].
+        rewrite <- e.
+        clear e.
+        eapply nd_comp.
+          eapply nd_rule.
+          eapply SFlat.
+          eapply RArrange.
+          eapply ALeft.
+          eapply AComp.
+          eapply ARight.
+          destruct s.
+          apply (arrangeCancelEmptyTree _ _ e).
+          apply ACanL.
+        eapply nd_comp.
+          eapply nd_rule.
+          eapply SFlat.
+          eapply RArrange.
+          eapply AuAssoc.
+        eapply nd_rule.
+          eapply SFlat.
+          eapply RLetRec.
 
       destruct case_RCase.
-        simpl.
-        apply (Prelude_error "CASE: BIG FIXME").
+        destruct lev; [ idtac | apply (Prelude_error "case at depth >0") ]; simpl.
+        apply nd_rule.
+        apply SFlat.
+        rewrite <- mapOptionTree_compose.
+        assert
+          ((mapOptionTree (fun x => skolemize_judgment (@pcb_judg tc Γ Δ nil tbranches avars (fst x) (snd x))) alts) =
+           (mapOptionTree (fun x => (@pcb_judg tc Γ Δ nil tbranches avars (fst x) (snd x))) alts)).
+           admit.
+           rewrite H.
+        set (@RCase Γ Δ nil tc Σ avars tbranches alts) as q.
+        apply q.
         Defined.
 
   Transparent take_arg_types_as_tree.