X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskSkolemizer.v;h=0d1cecbf1ffc86359a2f39c02bc999d0edaa241b;hp=b1d65e6ebb3f766b9e1c000062cf1299747cd160;hb=489b12c6c491b96c37839610d33fbdf666ee527f;hpb=cd81fca459c551077b485b1c1b297b3be1c43f3a

diff --git a/src/HaskSkolemizer.v b/src/HaskSkolemizer.v
index b1d65e6..0d1cecb 100644
--- a/src/HaskSkolemizer.v
+++ b/src/HaskSkolemizer.v
@@ -226,16 +226,14 @@ Section HaskSkolemizer.
       | RGlobal  Γ Δ σ l wev           => let case_RGlobal := tt       in _
       | RLam     Γ Δ Σ tx te     lev   => let case_RLam := tt          in _
       | RCast    Γ Δ Σ σ τ lev γ       => let case_RCast := tt         in _
-      | RAbsT    Γ Δ Σ κ σ lev         => let case_RAbsT := tt         in _
+      | RAbsT    Γ Δ Σ κ σ lev n       => let case_RAbsT := tt         in _
       | RAppT    Γ Δ Σ κ σ τ     lev   => let case_RAppT := tt         in _
       | RAppCo   Γ Δ Σ κ σ₁ σ₂ γ σ lev => let case_RAppCo := tt        in _
       | RAbsCo   Γ Δ Σ κ σ  σ₁ σ₂  lev => let case_RAbsCo := tt        in _
       | RApp     Γ Δ Σ₁ Σ₂ tx te lev   => let case_RApp := tt          in _
-      | RLet     Γ Δ Σ₁ Σ₂ σ₁ σ₂ lev   => let case_RLet := tt          in _
       | RCut     Γ Δ Σ Σ₁ Σ₁₂ Σ₂ Σ₃ l  => let case_RCut := tt          in _
       | RLeft    Γ Δ Σ₁ Σ₂  Σ     l    => let case_RLeft := tt in _
       | RRight   Γ Δ Σ₁ Σ₂  Σ     l    => let case_RRight := tt in _
-      | RWhere   Γ Δ Σ₁ Σ₂ Σ₃ σ₁ σ₂ lev => let case_RWhere := tt          in _
       | RVoid    _ _           l       => let case_RVoid := tt   in _
       | RBrak    Γ Δ t ec succ lev     => let case_RBrak := tt         in _
       | REsc     Γ Δ t ec succ lev     => let case_REsc := tt          in _
@@ -372,56 +370,8 @@ Section HaskSkolemizer.
         eapply take_unarrange.
 
         eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply AAssoc ].
-        eapply nd_rule; eapply SFlat; apply RWhere.
-
-      destruct case_RLet.
-        simpl.
-        destruct lev.
-        apply nd_rule.
-        apply SFlat.
-        apply RLet.
-        set (check_hof σ₁) as hof_tx.
-        destruct hof_tx; [ apply (Prelude_error "attempt to let-bind a higher-order function at depth>0") | idtac ].
-        destruct a.
-        rewrite H.
-        rewrite H0.
-
-        eapply nd_comp.
-        eapply nd_prod; [ eapply nd_rule; eapply SFlat; eapply RArrange; eapply ACanR | eapply nd_id ].
-
-        set (@RLet Γ Δ Σ₁ (Σ₂,,(take_arg_types_as_tree σ₂ @@@ (h::lev))) σ₁ (drop_arg_types_as_tree σ₂) (h::lev)) as q.
-        eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply AAssoc ].
-        eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply q ].
-        apply nd_prod.
-          apply nd_id.
-          apply nd_rule.
-          eapply SFlat.
-          eapply RArrange.
-          eapply AuAssoc.
-
-      destruct case_RWhere.
-        simpl.
-        destruct lev.
-        apply nd_rule.
-        apply SFlat.
-        apply RWhere.
-        set (check_hof σ₁) as hof_tx.
-        destruct hof_tx; [ apply (Prelude_error "attempt to let-bind a higher-order function at depth>0") | idtac ].
-        destruct a.
-        rewrite H.
-        rewrite H0.
-
-        eapply nd_comp.
-        eapply nd_prod; [ apply nd_id | eapply nd_rule; eapply SFlat; eapply RArrange; eapply ACanR ].
-        eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply AAssoc ].
-        eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply ALeft; eapply AAssoc ].
-        eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RWhere ].
-        apply nd_prod; [ idtac | eapply nd_id ].
-        eapply nd_rule; apply SFlat; eapply RArrange.
-        eapply AComp.
-        eapply AuAssoc.
-        apply ALeft.
-        eapply AuAssoc.
+        eapply nd_comp; [ apply nd_exch | idtac ].
+        eapply nd_rule; eapply SFlat; eapply RCut.
 
       destruct case_RCut.
         simpl; destruct l; [ apply nd_rule; apply SFlat; apply RCut | idtac ].
@@ -522,7 +472,10 @@ Section HaskSkolemizer.
 
       destruct case_RAbsT.
         simpl.
-        destruct lev; simpl; [ apply nd_rule; apply SFlat; apply (@RAbsT _ _ _ _ _ nil) | idtac ].
+        destruct lev; simpl.
+          apply nd_rule.
+          apply SFlat.
+          apply (@RAbsT Γ Δ Σ κ σ nil n).
         apply (Prelude_error "RAbsT at depth>0").
 
       destruct case_RAppCo.
@@ -542,11 +495,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.