X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskSkolemizer.v;h=0d1cecbf1ffc86359a2f39c02bc999d0edaa241b;hp=9d8dd4d970816458b0e4e6125c8d0cb9fc59f234;hb=refs%2Fheads%2Fcoq-extraction-baked-in;hpb=171beb27508a340b24ab14837e72451d0b500805 diff --git a/src/HaskSkolemizer.v b/src/HaskSkolemizer.v index 9d8dd4d..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 _ + | 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 _ @@ -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 ]. @@ -429,24 +379,38 @@ Section HaskSkolemizer. 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 Σ₁₂''); [ idtac | apply (Prelude_error "used RCut on a variable with function type") ]. + 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; [ apply nd_id | eapply nd_rule; eapply SFlat; eapply RArrange; eapply AuAssoc ]. + 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. 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. - eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply ACanR ]. - apply nd_rule. - apply SFlat. - apply RArrange. - apply ALeft. - destruct s. - eapply arrangeCancelEmptyTree with (q:=x). - rewrite e0. - admit. (* FIXME, but not serious *) apply nd_id. + eapply nd_rule. + eapply SFlat. + eapply RArrange. + eapply AComp. + eapply AuAssoc. + eapply ALeft. + eapply AComp. + eapply AuAssoc. + eapply ALeft. + eapply AId. destruct case_RLeft. simpl; destruct l; [ apply nd_rule; apply SFlat; apply RLeft | idtac ]. @@ -508,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. @@ -528,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.