| 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 _
- | RWhere Γ Δ Σ₁ Σ₂ Σ₃ σ₁ σ₂ lev => let case_RWhere := tt in _
- | RJoin Γ p lri m x q l => let case_RJoin := tt in _
+ | RCut Γ Δ Σ Σ₁ Σ₁₂ Σ₂ Σ₃ l => let case_RCut := tt in _
+ | RLeft Γ Δ Σ₁ Σ₂ Σ l => let case_RLeft := tt in _
+ | RRight Γ Δ Σ₁ Σ₂ Σ l => let case_RRight := 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 _
apply γ.
apply (Prelude_error "found RCast at level >0").
- destruct case_RJoin.
- simpl.
- destruct l.
- apply nd_rule.
- apply SFlat.
- apply RJoin.
- apply (Prelude_error "found RJoin at level >0").
-
destruct case_RApp.
simpl.
destruct lev.
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; [ 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 ].
+ set (mapOptionTreeAndFlatten take_arg_types_as_tree Σ₃) as Σ₃''.
+ set (mapOptionTree drop_arg_types_as_tree Σ₃) as Σ₃'''.
+ set (mapOptionTreeAndFlatten take_arg_types_as_tree Σ₁₂) as Σ₁₂''.
+ set (mapOptionTree drop_arg_types_as_tree Σ₁₂) as Σ₁₂'''.
+ destruct (decide_tree_empty (Σ₁₂'' @@@ (h::l)));
+ [ idtac | apply (Prelude_error "used RCut on a variable with function type") ].
+ destruct (eqd_dec Σ₁₂ Σ₁₂'''); [ idtac | apply (Prelude_error "used RCut on a variable with function type") ].
+ rewrite <- e.
+ clear e.
+ destruct s.
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.
+ eapply nd_prod.
+ eapply nd_rule.
+ eapply SFlat.
+ eapply RArrange.
+ eapply AComp.
+ eapply ALeft.
+ eapply arrangeCancelEmptyTree with (q:=x).
+ apply e.
+ apply ACanR.
apply nd_id.
- apply nd_rule.
+ 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 RCut ].
+ apply nd_prod.
+ apply nd_id.
+ eapply nd_rule.
eapply SFlat.
eapply RArrange.
+ eapply AComp.
eapply AuAssoc.
-
- destruct case_RWhere.
- simpl.
- destruct lev.
+ eapply ALeft.
+ eapply AComp.
+ eapply AuAssoc.
+ eapply ALeft.
+ eapply AId.
+
+ destruct case_RLeft.
+ simpl; destruct l; [ apply nd_rule; apply SFlat; apply RLeft | idtac ].
+ set (mapOptionTreeAndFlatten take_arg_types_as_tree Σ₂) as Σ₂'.
+ set (mapOptionTreeAndFlatten take_arg_types_as_tree Σ) as Σ'.
+ set (mapOptionTree drop_arg_types_as_tree Σ₂) as Σ₂''.
+ set (mapOptionTree drop_arg_types_as_tree Σ) as Σ''.
+ destruct (decide_tree_empty (Σ' @@@ (h::l)));
+ [ idtac | apply (Prelude_error "used RLeft on a variable with function type") ].
+ destruct (eqd_dec Σ Σ''); [ idtac | apply (Prelude_error "used RLeft on a variable with function type") ].
+ rewrite <- e.
+ clear Σ'' e.
+ destruct s.
+ set (arrangeUnCancelEmptyTree _ _ e) as q.
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply ALeft; eapply ARight; eapply q ].
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply ALeft; eapply AuCanL; eapply q ].
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply AAssoc ].
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 SFlat.
+ eapply RLeft.
+
+ destruct case_RRight.
+ simpl; destruct l; [ apply nd_rule; apply SFlat; apply RRight | idtac ].
+ set (mapOptionTreeAndFlatten take_arg_types_as_tree Σ₂) as Σ₂'.
+ set (mapOptionTreeAndFlatten take_arg_types_as_tree Σ) as Σ'.
+ set (mapOptionTree drop_arg_types_as_tree Σ₂) as Σ₂''.
+ set (mapOptionTree drop_arg_types_as_tree Σ) as Σ''.
+ destruct (decide_tree_empty (Σ' @@@ (h::l)));
+ [ idtac | apply (Prelude_error "used RRight on a variable with function type") ].
+ destruct (eqd_dec Σ Σ''); [ idtac | apply (Prelude_error "used RRight on a variable with function type") ].
+ rewrite <- e.
+ clear Σ'' e.
+ destruct s.
+ set (arrangeUnCancelEmptyTree _ _ e) as q.
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply ALeft; eapply ALeft; eapply q ].
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply ALeft; eapply AuCanR ].
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; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply ALeft; eapply AExch ]. (* yuck *)
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply AuAssoc ].
+ eapply nd_rule.
+ eapply SFlat.
+ apply RRight.
destruct case_RVoid.
simpl.
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.