X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskSkolemizer.v;h=0d1cecbf1ffc86359a2f39c02bc999d0edaa241b;hp=259d24e70bc0c603c27a0bd40e5c99bc31f7c8bf;hb=refs%2Fheads%2Fcoq-extraction-baked-in;hpb=1a2754d2e135ef3c5fd7ef817e1129af93b533a5 diff --git a/src/HaskSkolemizer.v b/src/HaskSkolemizer.v index 259d24e..0d1cecb 100644 --- a/src/HaskSkolemizer.v +++ b/src/HaskSkolemizer.v @@ -226,14 +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 _ - | 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 _ @@ -348,14 +348,6 @@ Section HaskSkolemizer. 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. @@ -378,56 +370,89 @@ 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; [ 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. @@ -447,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. @@ -467,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.