From: Adam Megacz Date: Sat, 28 May 2011 20:54:31 +0000 (-0700) Subject: rename constructors of Arrange to start with A instead of R X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=commitdiff_plain;h=1a2754d2e135ef3c5fd7ef817e1129af93b533a5 rename constructors of Arrange to start with A instead of R --- diff --git a/src/ExtractionMain.v b/src/ExtractionMain.v index d500e79..df7896b 100644 --- a/src/ExtractionMain.v +++ b/src/ExtractionMain.v @@ -237,7 +237,7 @@ Section core2proof. ND Rule [ Γ > Δ > Σ |- [a ---> s ]@lev ] [ Γ > Δ > [a @@ lev],,Σ |- [ s ]@lev ]. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ]. eapply nd_comp; [ idtac | eapply nd_rule; eapply RApp ]. eapply nd_comp; [ apply nd_rlecnac | idtac ]. apply nd_prod. @@ -252,7 +252,7 @@ Section core2proof. intro pf. eapply nd_comp. apply pf. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RCanR ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply ACanR ]. apply curry. Defined. @@ -268,8 +268,8 @@ Section core2proof. eapply nd_comp. eapply nd_rule. eapply RArrange. - eapply RCanR. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ]. + eapply ACanR. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ]. apply curry. Defined. diff --git a/src/HaskFlattener.v b/src/HaskFlattener.v index 51fd784..1bb35c6 100644 --- a/src/HaskFlattener.v +++ b/src/HaskFlattener.v @@ -287,7 +287,7 @@ Section HaskFlattener. ND Rule [] [ Γ > Δ > [x@@lev] |- [y]@lev ] -> ND Rule [ Γ > Δ > ant |- [x]@lev ] [ Γ > Δ > ant |- [y]@lev ]. intros. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanR ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanR ]. eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ]. eapply nd_comp; [ apply nd_rlecnac | idtac ]. apply nd_prod. @@ -296,7 +296,7 @@ Section HaskFlattener. apply X. eapply nd_rule. eapply RArrange. - apply RuCanR. + apply AuCanR. Defined. Definition precompose Γ Δ ec : forall a x y z lev, @@ -308,7 +308,7 @@ Section HaskFlattener. eapply nd_comp; [ apply nd_rlecnac | idtac ]. apply nd_prod. apply nd_id. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ]. apply ga_comp. Defined. @@ -317,8 +317,8 @@ Section HaskFlattener. [ Γ > Δ > a,,b |- [@ga_mk _ ec y z ]@lev ] [ Γ > Δ > a,,([@ga_mk _ ec x y @@ lev],,b) |- [@ga_mk _ ec x z ]@lev ]. intros. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RLeft; eapply RExch ]. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCossa ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ALeft; eapply AExch ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AuAssoc ]. apply precompose. Defined. @@ -338,7 +338,7 @@ Section HaskFlattener. ND Rule [] [ Γ > Δ > [] |- [@ga_mk _ ec x y ]@lev ] -> ND Rule [] [ Γ > Δ > [@ga_mk _ ec y z @@ lev] |- [@ga_mk _ ec x z ]@lev ]. intros. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanL ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanL ]. eapply nd_comp; [ idtac | eapply postcompose_ ]. apply X. Defined. @@ -347,12 +347,12 @@ Section HaskFlattener. ND Rule [ Γ > Δ > Σ |- [@ga_mk Γ ec a b ]@lev ] [ Γ > Δ > Σ |- [@ga_mk Γ ec (a,,c) (b,,c) ]@lev ]. intros. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanR ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanR ]. eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ]. eapply nd_comp; [ apply nd_rlecnac | idtac ]. apply nd_prod. apply nd_id. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RuCanR ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AuCanR ]. apply ga_first. Defined. @@ -370,12 +370,12 @@ Section HaskFlattener. [ Γ > Δ > Σ |- [@ga_mk Γ ec a b ]@lev ] [ Γ > Δ > Σ |- [@ga_mk Γ ec (c,,a) (c,,b) ]@lev ]. intros. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanR ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanR ]. eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ]. eapply nd_comp; [ apply nd_rlecnac | idtac ]. apply nd_prod. apply nd_id. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RuCanR ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AuCanR ]. apply ga_second. Defined. @@ -393,7 +393,7 @@ Section HaskFlattener. [Γ > Δ > Σ |- [@ga_mk Γ ec (a,,x) b ]@l ] [Γ > Δ > Σ,,[@ga_mk Γ ec [] a @@ l] |- [@ga_mk Γ ec x b ]@l ]. intros. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ]. eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ]. eapply nd_comp; [ apply nd_llecnac | idtac ]. apply nd_prod. @@ -404,7 +404,7 @@ Section HaskFlattener. apply nd_prod. apply postcompose. apply ga_uncancell. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ]. apply precompose. Defined. @@ -430,38 +430,38 @@ Section HaskFlattener. (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) B)) (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) A)) ]@nil] with - | RId a => let case_RId := tt in ga_id _ _ _ _ _ - | RCanL a => let case_RCanL := tt in ga_uncancell _ _ _ _ _ - | RCanR a => let case_RCanR := tt in ga_uncancelr _ _ _ _ _ - | RuCanL a => let case_RuCanL := tt in ga_cancell _ _ _ _ _ - | RuCanR a => let case_RuCanR := tt in ga_cancelr _ _ _ _ _ - | RAssoc a b c => let case_RAssoc := tt in ga_assoc _ _ _ _ _ _ _ - | RCossa a b c => let case_RCossa := tt in ga_unassoc _ _ _ _ _ _ _ - | RExch a b => let case_RExch := tt in ga_swap _ _ _ _ _ _ - | RWeak a => let case_RWeak := tt in ga_drop _ _ _ _ _ - | RCont a => let case_RCont := tt in ga_copy _ _ _ _ _ - | RLeft a b c r' => let case_RLeft := tt in flatten _ _ r' ;; boost _ _ _ _ _ (ga_second _ _ _ _ _ _ _) - | RRight a b c r' => let case_RRight := tt in flatten _ _ r' ;; boost _ _ _ _ _ (ga_first _ _ _ _ _ _ _) - | RComp c b a r1 r2 => let case_RComp := tt in (fun r1' r2' => _) (flatten _ _ r1) (flatten _ _ r2) + | AId a => let case_AId := tt in ga_id _ _ _ _ _ + | ACanL a => let case_ACanL := tt in ga_uncancell _ _ _ _ _ + | ACanR a => let case_ACanR := tt in ga_uncancelr _ _ _ _ _ + | AuCanL a => let case_AuCanL := tt in ga_cancell _ _ _ _ _ + | AuCanR a => let case_AuCanR := tt in ga_cancelr _ _ _ _ _ + | AAssoc a b c => let case_AAssoc := tt in ga_assoc _ _ _ _ _ _ _ + | AuAssoc a b c => let case_AuAssoc := tt in ga_unassoc _ _ _ _ _ _ _ + | AExch a b => let case_AExch := tt in ga_swap _ _ _ _ _ _ + | AWeak a => let case_AWeak := tt in ga_drop _ _ _ _ _ + | ACont a => let case_ACont := tt in ga_copy _ _ _ _ _ + | ALeft a b c r' => let case_ALeft := tt in flatten _ _ r' ;; boost _ _ _ _ _ (ga_second _ _ _ _ _ _ _) + | ARight a b c r' => let case_ARight := tt in flatten _ _ r' ;; boost _ _ _ _ _ (ga_first _ _ _ _ _ _ _) + | AComp c b a r1 r2 => let case_AComp := tt in (fun r1' r2' => _) (flatten _ _ r1) (flatten _ _ r2) end); clear flatten; repeat take_simplify; repeat drop_simplify; intros. - destruct case_RComp. + destruct case_AComp. set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) a)) as a' in *. set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) b)) as b' in *. set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) c)) as c' in *. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RCanL ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply ACanL ]. eapply nd_comp; [ idtac | eapply nd_rule; apply (@RLet Γ Δ [] [] (@ga_mk _ (v2t ec) a' b') (@ga_mk _ (v2t ec) a' c')) ]. eapply nd_comp; [ apply nd_llecnac | idtac ]. apply nd_prod. apply r2'. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RuCanR ]. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RCanL ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply AuCanR ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply ACanL ]. eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ]. eapply nd_comp; [ apply nd_llecnac | idtac ]. eapply nd_prod. apply r1'. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ]. apply ga_comp. Defined. @@ -485,19 +485,19 @@ Section HaskFlattener. match r as R in Arrange A B return Arrange (mapOptionTree (flatten_leveled_type ) (drop_lev _ A)) (mapOptionTree (flatten_leveled_type ) (drop_lev _ B)) with - | RId a => let case_RId := tt in RId _ - | RCanL a => let case_RCanL := tt in RCanL _ - | RCanR a => let case_RCanR := tt in RCanR _ - | RuCanL a => let case_RuCanL := tt in RuCanL _ - | RuCanR a => let case_RuCanR := tt in RuCanR _ - | RAssoc a b c => let case_RAssoc := tt in RAssoc _ _ _ - | RCossa a b c => let case_RCossa := tt in RCossa _ _ _ - | RExch a b => let case_RExch := tt in RExch _ _ - | RWeak a => let case_RWeak := tt in RWeak _ - | RCont a => let case_RCont := tt in RCont _ - | RLeft a b c r' => let case_RLeft := tt in RLeft _ (flatten _ _ r') - | RRight a b c r' => let case_RRight := tt in RRight _ (flatten _ _ r') - | RComp a b c r1 r2 => let case_RComp := tt in RComp (flatten _ _ r1) (flatten _ _ r2) + | AId a => let case_AId := tt in AId _ + | ACanL a => let case_ACanL := tt in ACanL _ + | ACanR a => let case_ACanR := tt in ACanR _ + | AuCanL a => let case_AuCanL := tt in AuCanL _ + | AuCanR a => let case_AuCanR := tt in AuCanR _ + | AAssoc a b c => let case_AAssoc := tt in AAssoc _ _ _ + | AuAssoc a b c => let case_AuAssoc := tt in AuAssoc _ _ _ + | AExch a b => let case_AExch := tt in AExch _ _ + | AWeak a => let case_AWeak := tt in AWeak _ + | ACont a => let case_ACont := tt in ACont _ + | ALeft a b c r' => let case_ALeft := tt in ALeft _ (flatten _ _ r') + | ARight a b c r' => let case_ARight := tt in ARight _ (flatten _ _ r') + | AComp a b c r1 r2 => let case_AComp := tt in AComp (flatten _ _ r1) (flatten _ _ r2) end) ant1 ant2 r); clear flatten; repeat take_simplify; repeat drop_simplify; intros. Defined. @@ -511,19 +511,19 @@ Section HaskFlattener. apply nd_rule. apply RArrange. induction r; simpl. - apply RId. - apply RCanL. - apply RCanR. - apply RuCanL. - apply RuCanR. - apply RAssoc. - apply RCossa. - apply RExch. (* TO DO: check for all-leaf trees here *) - apply RWeak. - apply RCont. - apply RLeft; auto. - apply RRight; auto. - eapply RComp; [ apply IHr1 | apply IHr2 ]. + apply AId. + apply ACanL. + apply ACanR. + apply AuCanL. + apply AuCanR. + apply AAssoc. + apply AuAssoc. + apply AExch. (* TO DO: check for all-leaf trees here *) + apply AWeak. + apply ACont. + apply ALeft; auto. + apply ARight; auto. + eapply AComp; [ apply IHr1 | apply IHr2 ]. apply flatten_arrangement. apply r. @@ -546,11 +546,11 @@ Section HaskFlattener. eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ]. eapply nd_comp; [ apply nd_llecnac | idtac ]. apply nd_prod. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanL ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanL ]. eapply nd_comp; [ idtac | eapply postcompose_ ]. apply ga_uncancelr. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ]. eapply nd_comp; [ idtac | eapply precompose ]. apply pfb. Defined. @@ -573,7 +573,7 @@ Section HaskFlattener. apply y. idtac. clear y q. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ]. simpl. eapply nd_comp; [ apply nd_llecnac | idtac ]. eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ]. @@ -641,7 +641,7 @@ Section HaskFlattener. destruct s. simpl. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RExch ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply AExch ]. set (fun z z' => @RLet Γ Δ z (mapOptionTree flatten_leveled_type q') t z' nil) as q''. eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ]. clear q''. @@ -649,8 +649,8 @@ Section HaskFlattener. apply nd_prod. apply nd_rule. apply RArrange. - eapply RComp; [ idtac | apply RCanR ]. - apply RLeft. + eapply AComp; [ idtac | apply ACanR ]. + apply ALeft. apply (@arrangeCancelEmptyTree _ _ _ _ e). eapply nd_comp. @@ -658,10 +658,10 @@ Section HaskFlattener. eapply (@RVar Γ Δ t nil). apply nd_rule. apply RArrange. - eapply RComp. - apply RuCanR. - apply RLeft. - apply RWeak. + eapply AComp. + apply AuCanR. + apply ALeft. + apply AWeak. (* eapply decide_tree_empty. @@ -685,15 +685,15 @@ Section HaskFlattener. simpl. apply nd_rule. apply RArrange. - apply RLeft. - apply RWeak. + apply ALeft. + apply AWeak. simpl. apply nd_rule. unfold take_lev. simpl. apply RArrange. - apply RLeft. - apply RWeak. + apply ALeft. + apply AWeak. apply (Prelude_error "escapifying code with multi-leaf antecedents is not supported"). *) Defined. @@ -714,17 +714,17 @@ Section HaskFlattener. simpl. drop_simplify. simpl. - apply RId. + apply AId. simpl. - apply RId. - eapply RComp; [ idtac | apply RCanL ]. - eapply RComp; [ idtac | eapply RLeft; apply IHt2 ]. + apply AId. + eapply AComp; [ idtac | apply ACanL ]. + eapply AComp; [ idtac | eapply ALeft; apply IHt2 ]. Opaque drop_lev. simpl. Transparent drop_lev. idtac. drop_simplify. - apply RRight. + apply ARight. apply IHt1. Defined. @@ -735,17 +735,17 @@ Section HaskFlattener. simpl. drop_simplify. simpl. - apply RId. + apply AId. simpl. - apply RId. - eapply RComp; [ apply RuCanL | idtac ]. - eapply RComp; [ eapply RRight; apply IHt1 | idtac ]. + apply AId. + eapply AComp; [ apply AuCanL | idtac ]. + eapply AComp; [ eapply ARight; apply IHt1 | idtac ]. Opaque drop_lev. simpl. Transparent drop_lev. idtac. drop_simplify. - apply RLeft. + apply ALeft. apply IHt2. Defined. @@ -901,7 +901,7 @@ Section HaskFlattener. eapply nd_rule. eapply RArrange. simpl. - apply RCanR. + apply ACanR. apply boost. simpl. apply ga_curry. @@ -967,8 +967,8 @@ Section HaskFlattener. eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ]. apply nd_prod. apply nd_id. - eapply nd_comp; [ eapply nd_rule; eapply RArrange; eapply RCanL | idtac ]. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch (* okay *)]. + eapply nd_comp; [ eapply nd_rule; eapply RArrange; eapply ACanL | idtac ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch (* okay *)]. apply precompose. destruct case_RWhere. @@ -997,8 +997,8 @@ Section HaskFlattener. eapply nd_comp; [ idtac | eapply precompose' ]. apply nd_rule. apply RArrange. - apply RLeft. - apply RCanL. + apply ALeft. + apply ACanL. destruct case_RVoid. simpl. @@ -1100,15 +1100,15 @@ Section HaskFlattener. set (mapOptionTree (flatten_type ○ unlev)(take_lev (ec :: nil) succ)) as succ_guest. set (mapOptionTree flatten_type (take_arg_types_as_tree t)) as succ_args. unfold empty_tree. - eapply nd_comp; [ eapply nd_rule; eapply RArrange; eapply RLeft; apply tree_of_nothing | idtac ]. - eapply nd_comp; [ eapply nd_rule; eapply RArrange; eapply RCanR | idtac ]. + eapply nd_comp; [ eapply nd_rule; eapply RArrange; eapply ALeft; apply tree_of_nothing | idtac ]. + eapply nd_comp; [ eapply nd_rule; eapply RArrange; eapply ACanR | idtac ]. refine (ga_unkappa Γ Δ (v2t ec) nil _ _ _ _ ;; _). eapply nd_comp; [ idtac | eapply arrange_brak ]. unfold succ_host. unfold succ_guest. eapply nd_rule. eapply RArrange. - apply RExch. + apply AExch. apply (Prelude_error "found Brak at depth >0 indicating 3-level code; only two-level code is currently supported"). destruct case_SEsc. @@ -1122,8 +1122,8 @@ Section HaskFlattener. take_simplify. drop_simplify. simpl. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RLeft; apply tree_of_nothing' ]. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanR ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ALeft; apply tree_of_nothing' ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanR ]. simpl. rewrite take_lemma'. rewrite unlev_relev. @@ -1139,15 +1139,15 @@ Section HaskFlattener. set (mapOptionTree flatten_leveled_type (drop_lev (ec :: nil) succ)) as succ_host. set (mapOptionTree flatten_type (take_arg_types_as_tree t)) as succ_args. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RuCanR ]. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RuCanR ]. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RCanL ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply AuCanR ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply AuCanR ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply ACanL ]. eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ]. eapply nd_comp; [ apply nd_llecnac | idtac ]. apply nd_prod; [ idtac | eapply boost ]. induction x. apply ga_id. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanL ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanL ]. simpl. apply ga_join. apply IHx1. diff --git a/src/HaskProgrammingLanguage.v b/src/HaskProgrammingLanguage.v index 8aba304..30a0ae8 100644 --- a/src/HaskProgrammingLanguage.v +++ b/src/HaskProgrammingLanguage.v @@ -73,10 +73,10 @@ Section HaskProgrammingLanguage. apply nd_id. eapply nd_rule. set (@org_fc) as ofc. - set (RArrange Γ Δ _ _ _ (RuCanL [l0])) as rule. - apply org_fc with (r:=RArrange _ _ _ _ _ (RuCanL [_])). + set (RArrange Γ Δ _ _ _ (AuCanL [l0])) as rule. + apply org_fc with (r:=RArrange _ _ _ _ _ (AuCanL [_])). auto. - eapply nd_comp; [ idtac | eapply nd_rule; apply org_fc with (r:=RArrange _ _ _ _ _ (RCanL _)) ]. + eapply nd_comp; [ idtac | eapply nd_rule; apply org_fc with (r:=RArrange _ _ _ _ _ (ACanL _)) ]. apply nd_rule. destruct l. destruct l0. @@ -148,23 +148,23 @@ Section HaskProgrammingLanguage. ; cnd_expand_right := fun a b c => SystemFCa_right c a b }. (* intros; apply nd_rule. simpl. - apply (org_fc _ _ _ _ ((RArrange _ _ _ _ _ (RCossa _ _ _)))). + apply (org_fc _ _ _ _ ((RArrange _ _ _ _ _ (AuAssoc _ _ _)))). auto. intros; apply nd_rule. simpl. - apply (org_fc _ _ _ _ (RArrange _ _ _ _ _ (RAssoc _ _ _))); auto. + apply (org_fc _ _ _ _ (RArrange _ _ _ _ _ (AAssoc _ _ _))); auto. intros; apply nd_rule. simpl. - apply (org_fc _ _ _ _ (RArrange _ _ _ _ _ (RCanL _))); auto. + apply (org_fc _ _ _ _ (RArrange _ _ _ _ _ (ACanL _))); auto. intros; apply nd_rule. simpl. - apply (org_fc _ _ _ _ (RArrange _ _ _ _ _ (RCanR _))); auto. + apply (org_fc _ _ _ _ (RArrange _ _ _ _ _ (ACanR _))); auto. intros; apply nd_rule. simpl. - apply (org_fc _ _ _ _ (RArrange _ _ _ _ _ (RuCanL _))); auto. + apply (org_fc _ _ _ _ (RArrange _ _ _ _ _ (AuCanL _))); auto. intros; apply nd_rule. simpl. - apply (org_fc _ _ _ _ (RArrange _ _ _ _ _ (RuCanR _))); auto. + apply (org_fc _ _ _ _ (RArrange _ _ _ _ _ (AuCanR _))); auto. *) admit. admit. diff --git a/src/HaskProof.v b/src/HaskProof.v index c887b8a..9787c62 100644 --- a/src/HaskProof.v +++ b/src/HaskProof.v @@ -67,7 +67,7 @@ Inductive Rule : Tree ??Judg -> Tree ??Judg -> Type := | RJoin : ∀ Γ Δ Σ₁ Σ₂ τ₁ τ₂ l, Rule ([Γ > Δ > Σ₁ |- τ₁ @l],,[Γ > Δ > Σ₂ |- τ₂ @l]) [Γ>Δ> Σ₁,,Σ₂ |- τ₁,,τ₂ @l ] -(* order is important here; we want to be able to skolemize without introducing new RExch'es *) +(* order is important here; we want to be able to skolemize without introducing new AExch'es *) | RApp : ∀ Γ Δ Σ₁ Σ₂ tx te l, Rule ([Γ>Δ> Σ₁ |- [tx--->te]@l],,[Γ>Δ> Σ₂ |- [tx]@l]) [Γ>Δ> Σ₁,,Σ₂ |- [te]@l] | RLet : ∀ Γ Δ Σ₁ Σ₂ σ₁ σ₂ l, Rule ([Γ>Δ> Σ₁ |- [σ₁]@l],,[Γ>Δ> [σ₁@@l],,Σ₂ |- [σ₂]@l ]) [Γ>Δ> Σ₁,,Σ₂ |- [σ₂ ]@l] diff --git a/src/HaskProofToLatex.v b/src/HaskProofToLatex.v index 9d88e79..99af119 100644 --- a/src/HaskProofToLatex.v +++ b/src/HaskProofToLatex.v @@ -160,19 +160,19 @@ Instance ToLatexMathJudgment : ToLatexMath Judg := Fixpoint nd_uruleToRawLatexMath {T}{h}{c}(r:@Arrange T h c) : string := match r with - | RLeft _ _ _ r => nd_uruleToRawLatexMath r - | RRight _ _ _ r => nd_uruleToRawLatexMath r - | RId _ => "Id" - | RCanL _ => "CanL" - | RCanR _ => "CanR" - | RuCanL _ => "uCanL" - | RuCanR _ => "uCanR" - | RAssoc _ _ _ => "Assoc" - | RCossa _ _ _ => "Cossa" - | RExch _ _ => "Exch" - | RWeak _ => "Weak" - | RCont _ => "Cont" - | RComp _ _ _ _ _ => "Comp" (* FIXME: do a better job here *) + | ALeft _ _ _ r => nd_uruleToRawLatexMath r + | ARight _ _ _ r => nd_uruleToRawLatexMath r + | AId _ => "Id" + | ACanL _ => "CanL" + | ACanR _ => "CanR" + | AuCanL _ => "uCanL" + | AuCanR _ => "uCanR" + | AAssoc _ _ _ => "Assoc" + | AuAssoc _ _ _ => "Cossa" + | AExch _ _ => "Exch" + | AWeak _ => "Weak" + | ACont _ => "Cont" + | AComp _ _ _ _ _ => "Comp" (* FIXME: do a better job here *) end. Fixpoint nd_ruleToRawLatexMath {h}{c}(r:Rule h c) : string := @@ -201,19 +201,19 @@ end. Fixpoint nd_hideURule {T}{h}{c}(r:@Arrange T h c) : bool := match r with - | RLeft _ _ _ r => nd_hideURule r - | RRight _ _ _ r => nd_hideURule r - | RCanL _ => true - | RCanR _ => true - | RuCanL _ => true - | RuCanR _ => true - | RAssoc _ _ _ => true - | RCossa _ _ _ => true - | RExch (T_Leaf None) b => true - | RExch a (T_Leaf None) => true - | RWeak (T_Leaf None) => true - | RCont (T_Leaf None) => true - | RComp _ _ _ _ _ => false (* FIXME: do better *) + | ALeft _ _ _ r => nd_hideURule r + | ARight _ _ _ r => nd_hideURule r + | ACanL _ => true + | ACanR _ => true + | AuCanL _ => true + | AuCanR _ => true + | AAssoc _ _ _ => true + | AuAssoc _ _ _ => true + | AExch (T_Leaf None) b => true + | AExch a (T_Leaf None) => true + | AWeak (T_Leaf None) => true + | ACont (T_Leaf None) => true + | AComp _ _ _ _ _ => false (* FIXME: do better *) | _ => false end. Fixpoint nd_hideRule {h}{c}(r:Rule h c) : bool := diff --git a/src/HaskProofToStrong.v b/src/HaskProofToStrong.v index e70322e..299a83b 100644 --- a/src/HaskProofToStrong.v +++ b/src/HaskProofToStrong.v @@ -238,49 +238,49 @@ Section HaskProofToStrong. ujudg2exprType Γ ξ Δ H t l -> ujudg2exprType Γ ξ Δ C t l with - | RLeft h c ctx r => let case_RLeft := tt in (fun e => _) (urule2expr _ _ _ _ r) - | RRight h c ctx r => let case_RRight := tt in (fun e => _) (urule2expr _ _ _ _ r) - | RId a => let case_RId := tt in _ - | RCanL a => let case_RCanL := tt in _ - | RCanR a => let case_RCanR := tt in _ - | RuCanL a => let case_RuCanL := tt in _ - | RuCanR a => let case_RuCanR := tt in _ - | RAssoc a b c => let case_RAssoc := tt in _ - | RCossa a b c => let case_RCossa := tt in _ - | RExch a b => let case_RExch := tt in _ - | RWeak a => let case_RWeak := tt in _ - | RCont a => let case_RCont := tt in _ - | RComp a b c f g => let case_RComp := tt in (fun e1 e2 => _) (urule2expr _ _ _ _ f) (urule2expr _ _ _ _ g) + | ALeft h c ctx r => let case_ALeft := tt in (fun e => _) (urule2expr _ _ _ _ r) + | ARight h c ctx r => let case_ARight := tt in (fun e => _) (urule2expr _ _ _ _ r) + | AId a => let case_AId := tt in _ + | ACanL a => let case_ACanL := tt in _ + | ACanR a => let case_ACanR := tt in _ + | AuCanL a => let case_AuCanL := tt in _ + | AuCanR a => let case_AuCanR := tt in _ + | AAssoc a b c => let case_AAssoc := tt in _ + | AuAssoc a b c => let case_AuAssoc := tt in _ + | AExch a b => let case_AExch := tt in _ + | AWeak a => let case_AWeak := tt in _ + | ACont a => let case_ACont := tt in _ + | AComp a b c f g => let case_AComp := tt in (fun e1 e2 => _) (urule2expr _ _ _ _ f) (urule2expr _ _ _ _ g) end); clear urule2expr; intros. - destruct case_RId. + destruct case_AId. apply X. - destruct case_RCanL. + destruct case_ACanL. simpl; unfold ujudg2exprType; intros. simpl in X. apply (X ([],,vars)). simpl; rewrite <- H; auto. - destruct case_RCanR. + destruct case_ACanR. simpl; unfold ujudg2exprType; intros. simpl in X. apply (X (vars,,[])). simpl; rewrite <- H; auto. - destruct case_RuCanL. + destruct case_AuCanL. simpl; unfold ujudg2exprType; intros. destruct vars; try destruct o; inversion H. simpl in X. apply (X vars2); auto. - destruct case_RuCanR. + destruct case_AuCanR. simpl; unfold ujudg2exprType; intros. destruct vars; try destruct o; inversion H. simpl in X. apply (X vars1); auto. - destruct case_RAssoc. + destruct case_AAssoc. simpl; unfold ujudg2exprType; intros. simpl in X. destruct vars; try destruct o; inversion H. @@ -288,7 +288,7 @@ Section HaskProofToStrong. apply (X (vars1_1,,(vars1_2,,vars2))). subst; auto. - destruct case_RCossa. + destruct case_AuAssoc. simpl; unfold ujudg2exprType; intros. simpl in X. destruct vars; try destruct o; inversion H. @@ -296,20 +296,20 @@ Section HaskProofToStrong. apply (X ((vars1,,vars2_1),,vars2_2)). subst; auto. - destruct case_RExch. + destruct case_AExch. simpl; unfold ujudg2exprType ; intros. simpl in X. destruct vars; try destruct o; inversion H. apply (X (vars2,,vars1)). inversion H; subst; auto. - destruct case_RWeak. + destruct case_AWeak. simpl; unfold ujudg2exprType; intros. simpl in X. apply (X []). auto. - destruct case_RCont. + destruct case_ACont. simpl; unfold ujudg2exprType ; intros. simpl in X. apply (X (vars,,vars)). @@ -317,7 +317,7 @@ Section HaskProofToStrong. rewrite <- H. auto. - destruct case_RLeft. + destruct case_ALeft. intro vars; unfold ujudg2exprType; intro H. destruct vars; try destruct o; inversion H. apply (fun q => e ξ q vars2 H2). @@ -332,7 +332,7 @@ Section HaskProofToStrong. simpl. reflexivity. - destruct case_RRight. + destruct case_ARight. intro vars; unfold ujudg2exprType; intro H. destruct vars; try destruct o; inversion H. apply (fun q => e ξ q vars1 H1). @@ -347,7 +347,7 @@ Section HaskProofToStrong. simpl. reflexivity. - destruct case_RComp. + destruct case_AComp. apply e2. apply e1. apply X. diff --git a/src/HaskSkolemizer.v b/src/HaskSkolemizer.v index 76e1bdb..259d24e 100644 --- a/src/HaskSkolemizer.v +++ b/src/HaskSkolemizer.v @@ -125,14 +125,14 @@ Section HaskSkolemizer. destruct (eqd_dec ([tx],,take_arg_types_as_tree te) (take_arg_types_as_tree (tx ---> te))). rewrite <- e. simpl. - apply RId. + apply AId. unfold take_arg_types_as_tree. Opaque take_arg_types_as_tree. simpl. destruct (count_arg_types (te (fun _ : Kind => unit) (ite_unit Γ))). simpl. replace (tx) with (fun (TV : Kind → Type) (ite : InstantiatedTypeEnv TV Γ) => tx TV ite). - apply RCanR. + apply ACanR. apply phoas_extensionality. reflexivity. apply (Prelude_error "should not be possible"). @@ -146,14 +146,14 @@ Section HaskSkolemizer. destruct (eqd_dec ([tx],,take_arg_types_as_tree te) (take_arg_types_as_tree (tx ---> te))). rewrite <- e. simpl. - apply RId. + apply AId. unfold take_arg_types_as_tree. Opaque take_arg_types_as_tree. simpl. destruct (count_arg_types (te (fun _ : Kind => unit) (ite_unit Γ))). simpl. replace (tx) with (fun (TV : Kind → Type) (ite : InstantiatedTypeEnv TV Γ) => tx TV ite). - apply RuCanR. + apply AuCanR. apply phoas_extensionality. reflexivity. apply (Prelude_error "should not be possible"). @@ -251,7 +251,7 @@ Section HaskSkolemizer. apply nd_rule. apply SFlat. apply RArrange. - apply RRight. + apply ARight. apply d. destruct case_RBrak. @@ -288,7 +288,7 @@ Section HaskSkolemizer. rewrite H. rewrite H0. simpl. - eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; apply RuCanL ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; apply AuCanL ]. apply nd_rule. apply SFlat. apply RLit. @@ -303,7 +303,7 @@ Section HaskSkolemizer. rewrite H. rewrite H0. simpl. - eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply RuCanR ]. + eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply AuCanR ]. apply nd_rule. apply SFlat. apply RVar. @@ -318,7 +318,7 @@ Section HaskSkolemizer. rewrite H. rewrite H0. simpl. - eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply RuCanR ]. + eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply AuCanR ]. apply nd_rule. apply SFlat. apply RGlobal. @@ -334,9 +334,9 @@ Section HaskSkolemizer. apply nd_rule. apply SFlat. apply RArrange. - eapply RComp. - eapply RCossa. - eapply RLeft. + eapply AComp. + eapply AuAssoc. + eapply ALeft. apply take_arrange. destruct case_RCast. @@ -370,14 +370,14 @@ Section HaskSkolemizer. rewrite H0. simpl. eapply nd_comp. - eapply nd_prod; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply RCanR ]. + eapply nd_prod; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply ACanR ]. eapply nd_rule. eapply SFlat. eapply RArrange. - eapply RLeft. + eapply ALeft. eapply take_unarrange. - eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply RAssoc ]. + eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply AAssoc ]. eapply nd_rule; eapply SFlat; apply RWhere. destruct case_RLet. @@ -393,17 +393,17 @@ Section HaskSkolemizer. rewrite H0. eapply nd_comp. - eapply nd_prod; [ eapply nd_rule; eapply SFlat; eapply RArrange; eapply RCanR | eapply nd_id ]. + 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 RAssoc ]. + 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 RCossa. + eapply AuAssoc. destruct case_RWhere. simpl. @@ -418,16 +418,16 @@ Section HaskSkolemizer. rewrite H0. eapply nd_comp. - eapply nd_prod; [ apply nd_id | eapply nd_rule; eapply SFlat; eapply RArrange; eapply RCanR ]. - eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply RAssoc ]. - eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply RLeft; eapply RAssoc ]. + 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 RComp. - eapply RCossa. - apply RLeft. - eapply RCossa. + eapply AComp. + eapply AuAssoc. + apply ALeft. + eapply AuAssoc. destruct case_RVoid. simpl. @@ -435,7 +435,7 @@ Section HaskSkolemizer. apply nd_rule. apply SFlat. apply RVoid. - eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply RuCanL ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply AuCanL ]. apply nd_rule. apply SFlat. apply RVoid. diff --git a/src/HaskStrongToProof.v b/src/HaskStrongToProof.v index 8aa4005..1b9f6af 100644 --- a/src/HaskStrongToProof.v +++ b/src/HaskStrongToProof.v @@ -621,16 +621,16 @@ Definition factorContextLeft (* where the leaf is v *) apply inr. subst. - apply RuCanR. + apply AuCanR. (* where the leaf is NOT v *) apply inl. - apply RuCanL. + apply AuCanL. (* empty leaf *) destruct case_None. apply inl; simpl in *. - apply RuCanR. + apply AuCanR. (* branch *) refine ( @@ -650,45 +650,45 @@ Definition factorContextLeft destruct case_Neither. apply inl. simpl. - eapply RComp; [idtac | apply RuCanL ]. - exact (RComp + eapply AComp; [idtac | apply AuCanL ]. + exact (AComp (* order will not matter because these are central as morphisms *) - (RRight _ (RComp lpf (RCanL _))) - (RLeft _ (RComp rpf (RCanL _)))). + (ARight _ (AComp lpf (ACanL _))) + (ALeft _ (AComp rpf (ACanL _)))). destruct case_Right. apply inr. unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *. fold (stripOutVars (v::nil)). - eapply RComp; [ idtac | eapply pivotContext' ]. - eapply RComp. - eapply RRight. - eapply RComp. + eapply AComp; [ idtac | eapply pivotContext' ]. + eapply AComp. + eapply ARight. + eapply AComp. apply lpf. - apply RCanL. - eapply RLeft. + apply ACanL. + eapply ALeft. apply rpf. destruct case_Left. apply inr. fold (stripOutVars (v::nil)). simpl. - eapply RComp. - eapply RLeft. - eapply RComp. + eapply AComp. + eapply ALeft. + eapply AComp. apply rpf. simpl. - eapply RCanL. - eapply RComp; [ idtac | eapply RCossa ]. - eapply RRight. + eapply ACanL. + eapply AComp; [ idtac | eapply AuAssoc ]. + eapply ARight. apply lpf. destruct case_Both. apply inr. simpl. - eapply RComp; [ idtac | eapply RRight; eapply RCont ]. - eapply RComp; [ eapply RRight; eapply lpf | idtac ]. - eapply RComp; [ eapply RLeft; eapply rpf | idtac ]. + eapply AComp; [ idtac | eapply ARight; eapply ACont ]. + eapply AComp; [ eapply ARight; eapply lpf | idtac ]. + eapply AComp; [ eapply ALeft; eapply rpf | idtac ]. clear lpf rpf. simpl. apply arrangeSwapMiddle. @@ -726,16 +726,16 @@ Definition factorContextRight (* where the leaf is v *) apply inr. subst. - apply RuCanL. + apply AuCanL. (* where the leaf is NOT v *) apply inl. - apply RuCanR. + apply AuCanR. (* empty leaf *) destruct case_None. apply inl; simpl in *. - apply RuCanR. + apply AuCanR. (* branch *) refine ( @@ -754,51 +754,51 @@ Definition factorContextRight destruct case_Neither. apply inl. - eapply RComp; [idtac | apply RuCanR ]. - exact (RComp + eapply AComp; [idtac | apply AuCanR ]. + exact (AComp (* order will not matter because these are central as morphisms *) - (RRight _ (RComp lpf (RCanR _))) - (RLeft _ (RComp rpf (RCanR _)))). + (ARight _ (AComp lpf (ACanR _))) + (ALeft _ (AComp rpf (ACanR _)))). destruct case_Right. apply inr. fold (stripOutVars (v::nil)). - set (RRight (mapOptionTree ξ ctx2) (RComp lpf ((RCanR _)))) as q. + set (ARight (mapOptionTree ξ ctx2) (AComp lpf ((ACanR _)))) as q. simpl in *. - eapply RComp. + eapply AComp. apply q. clear q. clear lpf. unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *. - eapply RComp; [ idtac | apply RAssoc ]. - apply RLeft. + eapply AComp; [ idtac | apply AAssoc ]. + apply ALeft. apply rpf. destruct case_Left. apply inr. unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *. fold (stripOutVars (v::nil)). - eapply RComp; [ idtac | eapply pivotContext ]. - set (RComp rpf (RCanR _ )) as rpf'. - set (RLeft ((mapOptionTree ξ (stripOutVars (v :: nil) ctx1),, [ξ v])) rpf') as qq. + eapply AComp; [ idtac | eapply pivotContext ]. + set (AComp rpf (ACanR _ )) as rpf'. + set (ALeft ((mapOptionTree ξ (stripOutVars (v :: nil) ctx1),, [ξ v])) rpf') as qq. simpl in *. - eapply RComp; [ idtac | apply qq ]. + eapply AComp; [ idtac | apply qq ]. clear qq rpf' rpf. - apply (RRight (mapOptionTree ξ ctx2)). + apply (ARight (mapOptionTree ξ ctx2)). apply lpf. destruct case_Both. apply inr. unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *. fold (stripOutVars (v::nil)). - eapply RComp; [ idtac | eapply copyAndPivotContext ]. + eapply AComp; [ idtac | eapply copyAndPivotContext ]. (* order will not matter because these are central as morphisms *) - exact (RComp (RRight _ lpf) (RLeft _ rpf)). + exact (AComp (ARight _ lpf) (ALeft _ rpf)). Defined. -(* same as before, but use RWeak if necessary *) +(* same as before, but use AWeak if necessary *) Definition factorContextLeftAndWeaken (Γ:TypeEnv)(Δ:CoercionEnv Γ) v (* variable to be pivoted, if found *) @@ -809,8 +809,8 @@ Definition factorContextLeftAndWeaken (mapOptionTree ξ ([v],,(stripOutVars (v::nil) ctx)) ). set (factorContextLeft Γ Δ v ctx ξ) as q. destruct q; auto. - eapply RComp; [ apply a | idtac ]. - refine (RRight _ (RWeak _)). + eapply AComp; [ apply a | idtac ]. + refine (ARight _ (AWeak _)). Defined. Definition factorContextLeftAndWeaken'' @@ -836,7 +836,7 @@ Definition factorContextLeftAndWeaken'' unfold mapOptionTree; simpl in *. intros. rewrite (@stripping_nothing_is_inert Γ); auto. - apply RuCanL. + apply AuCanL. intros. unfold mapOptionTree in *. simpl in *. @@ -855,15 +855,15 @@ Definition factorContextLeftAndWeaken'' unfold stripOutVars in q. rewrite q in IHv1'. clear q. - eapply RComp; [ idtac | eapply RAssoc ]. - eapply RComp; [ idtac | eapply IHv1' ]. + eapply AComp; [ idtac | eapply AAssoc ]. + eapply AComp; [ idtac | eapply IHv1' ]. clear IHv1'. apply IHv2; auto. auto. auto. Defined. -(* same as before, but use RWeak if necessary *) +(* same as before, but use AWeak if necessary *) Definition factorContextRightAndWeaken (Γ:TypeEnv)(Δ:CoercionEnv Γ) v (* variable to be pivoted, if found *) @@ -874,8 +874,8 @@ Definition factorContextRightAndWeaken (mapOptionTree ξ ((stripOutVars (v::nil) ctx),,[v]) ). set (factorContextRight Γ Δ v ctx ξ) as q. destruct q; auto. - eapply RComp; [ apply a | idtac ]. - refine (RLeft _ (RWeak _)). + eapply AComp; [ apply a | idtac ]. + refine (ALeft _ (AWeak _)). Defined. Definition factorContextRightAndWeaken'' @@ -899,7 +899,7 @@ Definition factorContextRightAndWeaken'' unfold mapOptionTree; simpl in *. intros. rewrite (@stripping_nothing_is_inert Γ); auto. - apply RuCanR. + apply AuCanR. intros. unfold mapOptionTree in *. simpl in *. @@ -918,14 +918,14 @@ Definition factorContextRightAndWeaken'' fold X in IHv2'. set (distinct_app _ _ _ H) as H'. destruct H' as [H1 H2]. - set (RComp (IHv1 _ H1) (IHv2' H2)) as qq. - eapply RComp. + set (AComp (IHv1 _ H1) (IHv2' H2)) as qq. + eapply AComp. apply qq. clear qq IHv2' IHv2 IHv1. rewrite strip_swap_lemma. rewrite strip_twice_lemma. rewrite (notin_strip_inert' v1 (leaves v2)). - apply RCossa. + apply AuAssoc. apply distinct_swap. auto. Defined. diff --git a/src/HaskWeak.v b/src/HaskWeak.v index 670d8bd..077f7b5 100644 --- a/src/HaskWeak.v +++ b/src/HaskWeak.v @@ -108,4 +108,4 @@ Fixpoint simplifyWeakExpr (me:WeakExpr) : WeakExpr := (* un-letrec-ify multi branch letrecs *) | WELetRec mlr e => WELetRec mlr (simplifyWeakExpr e ) end. -*) \ No newline at end of file +*) diff --git a/src/NaturalDeductionContext.v b/src/NaturalDeductionContext.v index 03fc704..57dfdb8 100644 --- a/src/NaturalDeductionContext.v +++ b/src/NaturalDeductionContext.v @@ -14,19 +14,19 @@ Section NaturalDeductionContext. (* Figure 3, production $\vdash_E$, Uniform rules *) Inductive Arrange {T} : Tree ??T -> Tree ??T -> Type := - | RId : forall a , Arrange a a - | RCanL : forall a , Arrange ( [],,a ) ( a ) - | RCanR : forall a , Arrange ( a,,[] ) ( a ) - | RuCanL : forall a , Arrange ( a ) ( [],,a ) - | RuCanR : forall a , Arrange ( a ) ( a,,[] ) - | RAssoc : forall a b c , Arrange (a,,(b,,c) ) ((a,,b),,c ) - | RCossa : forall a b c , Arrange ((a,,b),,c ) ( a,,(b,,c) ) - | RExch : forall a b , Arrange ( (b,,a) ) ( (a,,b) ) - | RWeak : forall a , Arrange ( [] ) ( a ) - | RCont : forall a , Arrange ( (a,,a) ) ( a ) - | RLeft : forall {h}{c} x , Arrange h c -> Arrange ( x,,h ) ( x,,c) - | RRight : forall {h}{c} x , Arrange h c -> Arrange ( h,,x ) ( c,,x) - | RComp : forall {a}{b}{c}, Arrange a b -> Arrange b c -> Arrange a c + | AId : forall a , Arrange a a + | ACanL : forall a , Arrange ( [],,a ) ( a ) + | ACanR : forall a , Arrange ( a,,[] ) ( a ) + | AuCanL : forall a , Arrange ( a ) ( [],,a ) + | AuCanR : forall a , Arrange ( a ) ( a,,[] ) + | AAssoc : forall a b c , Arrange (a,,(b,,c) ) ((a,,b),,c ) + | AuAssoc : forall a b c , Arrange ((a,,b),,c ) ( a,,(b,,c) ) + | AExch : forall a b , Arrange ( (b,,a) ) ( (a,,b) ) + | AWeak : forall a , Arrange ( [] ) ( a ) + | ACont : forall a , Arrange ( (a,,a) ) ( a ) + | ALeft : forall {h}{c} x , Arrange h c -> Arrange ( x,,h ) ( x,,c) + | ARight : forall {h}{c} x , Arrange h c -> Arrange ( h,,x ) ( c,,x) + | AComp : forall {a}{b}{c}, Arrange a b -> Arrange b c -> Arrange a c . (* "Arrange" objects are parametric in the type of the leaves of the tree *) @@ -36,51 +36,51 @@ Section NaturalDeductionContext. Arrange (mapOptionTree f Σ₁) (mapOptionTree f Σ₂). intros. induction X; simpl. - apply RId. - apply RCanL. - apply RCanR. - apply RuCanL. - apply RuCanR. - apply RAssoc. - apply RCossa. - apply RExch. - apply RWeak. - apply RCont. - apply RLeft; auto. - apply RRight; auto. - eapply RComp; [ apply IHX1 | apply IHX2 ]. + apply AId. + apply ACanL. + apply ACanR. + apply AuCanL. + apply AuCanR. + apply AAssoc. + apply AuAssoc. + apply AExch. + apply AWeak. + apply ACont. + apply ALeft; auto. + apply ARight; auto. + eapply AComp; [ apply IHX1 | apply IHX2 ]. Defined. (* a frequently-used Arrange - swap the middle two elements of a four-element sequence *) Definition arrangeSwapMiddle {T} (a b c d:Tree ??T) : Arrange ((a,,b),,(c,,d)) ((a,,c),,(b,,d)). - eapply RComp. - apply RCossa. - eapply RComp. - eapply RLeft. - eapply RComp. - eapply RAssoc. - eapply RRight. - apply RExch. - eapply RComp. - eapply RLeft. - eapply RCossa. - eapply RAssoc. + eapply AComp. + apply AuAssoc. + eapply AComp. + eapply ALeft. + eapply AComp. + eapply AAssoc. + eapply ARight. + apply AExch. + eapply AComp. + eapply ALeft. + eapply AuAssoc. + eapply AAssoc. Defined. - (* like RExch, but works on nodes which are an Assoc away from being adjacent *) + (* like AExch, but works on nodes which are an Assoc away from being adjacent *) Definition pivotContext {T} a b c : @Arrange T ((a,,b),,c) ((a,,c),,b) := - RComp (RComp (RCossa _ _ _) (RLeft a (RExch c b))) (RAssoc _ _ _). + AComp (AComp (AuAssoc _ _ _) (ALeft a (AExch c b))) (AAssoc _ _ _). - (* like RExch, but works on nodes which are an Assoc away from being adjacent *) + (* like AExch, but works on nodes which are an Assoc away from being adjacent *) Definition pivotContext' {T} a b c : @Arrange T (a,,(b,,c)) (b,,(a,,c)) := - RComp (RComp (RAssoc _ _ _) (RRight c (RExch b a))) (RCossa _ _ _). + AComp (AComp (AAssoc _ _ _) (ARight c (AExch b a))) (AuAssoc _ _ _). Definition copyAndPivotContext {T} a b c : @Arrange T ((a,,b),,(c,,b)) ((a,,c),,b). - eapply RComp; [ idtac | apply (RLeft (a,,c) (RCont b)) ]. - eapply RComp; [ idtac | apply RCossa ]. - eapply RComp; [ idtac | apply (RRight b (pivotContext a b c)) ]. - apply RAssoc. + eapply AComp; [ idtac | apply (ALeft (a,,c) (ACont b)) ]. + eapply AComp; [ idtac | apply AuAssoc ]. + eapply AComp; [ idtac | apply (ARight b (pivotContext a b c)) ]. + apply AAssoc. Defined. (* given any set of TreeFlags on a tree, we can Arrange all of the flagged nodes into the left subtree *) @@ -93,16 +93,16 @@ Section NaturalDeductionContext. destruct a. simpl. destruct (f t); simpl. - apply RuCanL. - apply RuCanR. + apply AuCanL. + apply AuCanR. simpl. - apply RuCanL. + apply AuCanL. simpl in *. - eapply RComp; [ idtac | apply arrangeSwapMiddle ]. - eapply RComp. - eapply RLeft. + eapply AComp; [ idtac | apply arrangeSwapMiddle ]. + eapply AComp. + eapply ALeft. apply IHΣ2. - eapply RRight. + eapply ARight. apply IHΣ1. Defined. @@ -116,16 +116,16 @@ Section NaturalDeductionContext. destruct a. simpl. destruct (f t); simpl. - apply RCanL. - apply RCanR. + apply ACanL. + apply ACanR. simpl. - apply RCanL. + apply ACanL. simpl in *. - eapply RComp; [ apply arrangeSwapMiddle | idtac ]. - eapply RComp. - eapply RLeft. + eapply AComp; [ apply arrangeSwapMiddle | idtac ]. + eapply AComp. + eapply ALeft. apply IHΣ2. - eapply RRight. + eapply ARight. apply IHΣ1. Defined. @@ -164,17 +164,17 @@ Section NaturalDeductionContext. induction q; intros. simpl in H. rewrite H. - apply RId. + apply AId. simpl in *. destruct t; try destruct o; inversion H. set (IHq1 _ H1) as x1. set (IHq2 _ H2) as x2. - eapply RComp. - eapply RRight. + eapply AComp. + eapply ARight. rewrite <- H1. apply x1. - eapply RComp. - apply RCanL. + eapply AComp. + apply ACanL. rewrite <- H2. apply x2. Defined. @@ -187,21 +187,21 @@ Section NaturalDeductionContext. induction q; intros. simpl in H. rewrite H. - apply RId. + apply AId. simpl in *. destruct t; try destruct o; inversion H. set (IHq1 _ H1) as x1. set (IHq2 _ H2) as x2. - eapply RComp. - apply RuCanL. - eapply RComp. - eapply RRight. + eapply AComp. + apply AuCanL. + eapply AComp. + eapply ARight. apply x1. - eapply RComp. - eapply RLeft. + eapply AComp. + eapply ALeft. apply x2. rewrite H. - apply RId. + apply AId. Defined. (* given an Arrange from Σ₁ to Σ₂ and any predicate on tree nodes, we can construct an Arrange from (dropT Σ₁) to (dropT Σ₂) *) @@ -210,38 +210,38 @@ Section NaturalDeductionContext. refine ((fix arrangeTake t1 t2 (arr:Arrange t1 t2) := match arr as R in Arrange A B return Arrange (dropT (mkFlags pred A)) (dropT (mkFlags pred B)) with - | RId a => let case_RId := tt in RId _ - | RCanL a => let case_RCanL := tt in _ - | RCanR a => let case_RCanR := tt in _ - | RuCanL a => let case_RuCanL := tt in _ - | RuCanR a => let case_RuCanR := tt in _ - | RAssoc a b c => let case_RAssoc := tt in RAssoc _ _ _ - | RCossa a b c => let case_RCossa := tt in RCossa _ _ _ - | RExch a b => let case_RExch := tt in RExch _ _ - | RWeak a => let case_RWeak := tt in _ - | RCont a => let case_RCont := tt in _ - | RLeft a b c r' => let case_RLeft := tt in RLeft _ (arrangeTake _ _ r') - | RRight a b c r' => let case_RRight := tt in RRight _ (arrangeTake _ _ r') - | RComp a b c r1 r2 => let case_RComp := tt in RComp (arrangeTake _ _ r1) (arrangeTake _ _ r2) + | AId a => let case_AId := tt in AId _ + | ACanL a => let case_ACanL := tt in _ + | ACanR a => let case_ACanR := tt in _ + | AuCanL a => let case_AuCanL := tt in _ + | AuCanR a => let case_AuCanR := tt in _ + | AAssoc a b c => let case_AAssoc := tt in AAssoc _ _ _ + | AuAssoc a b c => let case_AuAssoc := tt in AuAssoc _ _ _ + | AExch a b => let case_AExch := tt in AExch _ _ + | AWeak a => let case_AWeak := tt in _ + | ACont a => let case_ACont := tt in _ + | ALeft a b c r' => let case_ALeft := tt in ALeft _ (arrangeTake _ _ r') + | ARight a b c r' => let case_ARight := tt in ARight _ (arrangeTake _ _ r') + | AComp a b c r1 r2 => let case_AComp := tt in AComp (arrangeTake _ _ r1) (arrangeTake _ _ r2) end)); clear arrangeTake; intros. - destruct case_RCanL. - simpl; destruct (pred None); simpl; apply RCanL. + destruct case_ACanL. + simpl; destruct (pred None); simpl; apply ACanL. - destruct case_RCanR. - simpl; destruct (pred None); simpl; apply RCanR. + destruct case_ACanR. + simpl; destruct (pred None); simpl; apply ACanR. - destruct case_RuCanL. - simpl; destruct (pred None); simpl; apply RuCanL. + destruct case_AuCanL. + simpl; destruct (pred None); simpl; apply AuCanL. - destruct case_RuCanR. - simpl; destruct (pred None); simpl; apply RuCanR. + destruct case_AuCanR. + simpl; destruct (pred None); simpl; apply AuCanR. - destruct case_RWeak. - simpl; destruct (pred None); simpl; apply RWeak. + destruct case_AWeak. + simpl; destruct (pred None); simpl; apply AWeak. - destruct case_RCont. - simpl; destruct (pred None); simpl; apply RCont. + destruct case_ACont. + simpl; destruct (pred None); simpl; apply ACont. Defined. diff --git a/src/PCF.v b/src/PCF.v index 5caf2dc..373519b 100644 --- a/src/PCF.v +++ b/src/PCF.v @@ -183,8 +183,8 @@ Section PCF. eapply nd_prod. apply nd_id. apply (PCF_Arrange [h] ([],,[h]) [h0]). - apply RuCanL. - eapply nd_comp; [ idtac | apply (PCF_Arrange ([],,a) a [h0]); apply RCanL ]. + apply AuCanL. + eapply nd_comp; [ idtac | apply (PCF_Arrange ([],,a) a [h0]); apply ACanL ]. apply nd_rule. (* set (@RLet Γ Δ [] (a@@@(ec::nil)) h0 h (ec::nil)) as q. @@ -241,27 +241,27 @@ Section PCF. ; cnd_expand_right := fun a b c => PCF_right Γ Δ lev c a b }. intros; apply nd_rule. unfold PCFRule. simpl. - exists (RArrange _ _ _ _ _ (RCossa _ _ _)). + exists (RArrange _ _ _ _ _ (AuAssoc _ _ _)). apply (PCF_RArrange _ _ lev ((a,,b),,c) (a,,(b,,c)) x). intros; apply nd_rule. unfold PCFRule. simpl. - exists (RArrange _ _ _ _ _ (RAssoc _ _ _)). + exists (RArrange _ _ _ _ _ (AAssoc _ _ _)). apply (PCF_RArrange _ _ lev (a,,(b,,c)) ((a,,b),,c) x). intros; apply nd_rule. unfold PCFRule. simpl. - exists (RArrange _ _ _ _ _ (RCanL _)). + exists (RArrange _ _ _ _ _ (ACanL _)). apply (PCF_RArrange _ _ lev ([],,a) _ _). intros; apply nd_rule. unfold PCFRule. simpl. - exists (RArrange _ _ _ _ _ (RCanR _)). + exists (RArrange _ _ _ _ _ (ACanR _)). apply (PCF_RArrange _ _ lev (a,,[]) _ _). intros; apply nd_rule. unfold PCFRule. simpl. - exists (RArrange _ _ _ _ _ (RuCanL _)). + exists (RArrange _ _ _ _ _ (AuCanL _)). apply (PCF_RArrange _ _ lev _ ([],,a) _). intros; apply nd_rule. unfold PCFRule. simpl. - exists (RArrange _ _ _ _ _ (RuCanR _)). + exists (RArrange _ _ _ _ _ (AuCanR _)). apply (PCF_RArrange _ _ lev _ (a,,[]) _). Defined.