From ef05c795559108c1d33cfa048531849807867a81 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sun, 5 Apr 2009 23:38:16 +0000 Subject: [PATCH] - Procedural: now we generate the exact tactic (in place of some apply tactics) and we do not perform conversion steps before it (1104 change tactics omitted in the lambda-delta devel) - new target for the PREDICATIVE-TOPOLOGY devel: now is "limits" --- .../components/acic_procedural/procedural1.ml | 23 ++++++++++--------- .../acic_procedural/proceduralTeX.ml | 2 ++ .../acic_procedural/proceduralTypes.ml | 8 +++++++ .../acic_procedural/proceduralTypes.mli | 1 + .../{PREDICATIVE-TOPOLOGY => limits}/Makefile | 0 .../class_defs.ma | 0 .../class_eq.ma | 0 .../coa_defs.ma | 0 .../coa_props.ma | 0 .../{PREDICATIVE-TOPOLOGY => limits}/depends | 0 .../domain_data.ma | 0 .../domain_defs.ma | 0 .../{PREDICATIVE-TOPOLOGY => limits}/iff.ma | 0 .../{PREDICATIVE-TOPOLOGY => limits}/root | 0 .../subset_defs.ma | 0 15 files changed, 23 insertions(+), 11 deletions(-) rename helm/software/matita/contribs/{PREDICATIVE-TOPOLOGY => limits}/Makefile (100%) rename helm/software/matita/contribs/{PREDICATIVE-TOPOLOGY => limits}/class_defs.ma (100%) rename helm/software/matita/contribs/{PREDICATIVE-TOPOLOGY => limits}/class_eq.ma (100%) rename helm/software/matita/contribs/{PREDICATIVE-TOPOLOGY => limits}/coa_defs.ma (100%) rename helm/software/matita/contribs/{PREDICATIVE-TOPOLOGY => limits}/coa_props.ma (100%) rename helm/software/matita/contribs/{PREDICATIVE-TOPOLOGY => limits}/depends (100%) rename helm/software/matita/contribs/{PREDICATIVE-TOPOLOGY => limits}/domain_data.ma (100%) rename helm/software/matita/contribs/{PREDICATIVE-TOPOLOGY => limits}/domain_defs.ma (100%) rename helm/software/matita/contribs/{PREDICATIVE-TOPOLOGY => limits}/iff.ma (100%) rename helm/software/matita/contribs/{PREDICATIVE-TOPOLOGY => limits}/root (100%) rename helm/software/matita/contribs/{PREDICATIVE-TOPOLOGY => limits}/subset_defs.ma (100%) diff --git a/helm/software/components/acic_procedural/procedural1.ml b/helm/software/components/acic_procedural/procedural1.ml index 4b9127002..ad3152530 100644 --- a/helm/software/components/acic_procedural/procedural1.ml +++ b/helm/software/components/acic_procedural/procedural1.ml @@ -241,8 +241,9 @@ let get_intro = function | C.Anonymous -> None | C.Name s -> Some s -let mk_preamble st what script = - convert st what @ script +let mk_preamble st what script = match script with + | T.Exact _ :: _ -> script + | _ -> convert st what @ script let mk_arg st = function | C.ARel (_, _, i, name) as what -> convert st ~name:(name, i) what @@ -270,7 +271,7 @@ let mk_fwd_rewrite st dtext name tl direction v t ity = assert (Ut.is_sober st.context (H.cic ity)); let ity = H.acic_bc st.context ity in let br1 = [T.Id ""] in - let br2 = List.rev (T.Apply (w, "assumption") :: script None) in + let br2 = List.rev (T.Exact (w, "assumption") :: script None) in let text = "non-linear rewrite" in st, [T.Branch ([br2; br1], ""); T.Cut (name, ity, text)] end @@ -320,24 +321,24 @@ and proc_letin st what name v w t = let qt = proc_proof (next (add st entry)) t in List.rev_append rqv qt else - [T.Apply (what, dtext)] + [T.Exact (what, dtext)] in mk_preamble st what script and proc_rel st what = let _, dtext = test_depth st in let text = "assumption" in - let script = [T.Apply (what, dtext ^ text)] in + let script = [T.Exact (what, dtext ^ text)] in mk_preamble st what script and proc_mutconstruct st what = let _, dtext = test_depth st in - let script = [T.Apply (what, dtext)] in + let script = [T.Exact (what, dtext)] in mk_preamble st what script and proc_const st what = let _, dtext = test_depth st in - let script = [T.Apply (what, dtext)] in + let script = [T.Exact (what, dtext)] in mk_preamble st what script and proc_appl st what hd tl = @@ -391,7 +392,7 @@ and proc_appl st what hd tl = let hd = mk_exp_args hd tl classes synth in script @ [T.Apply (hd, dtext ^ text); T.Branch (qs, "")] else - [T.Apply (what, dtext)] + [T.Exact (what, dtext)] in mk_preamble st what script @@ -411,14 +412,14 @@ and proc_case st what uri tyno u v ts = let script = List.rev (mk_arg st v) in script @ [T.Cases (v, e, dtext ^ text); T.Branch (qs, "")] else - [T.Apply (what, dtext)] + [T.Exact (what, dtext)] in mk_preamble st what script and proc_other st what = let _, dtext = test_depth st in let text = Printf.sprintf "%s: %s" "UNEXPANDED" (string_of_head what) in - let script = [T.Apply (what, dtext ^ text)] in + let script = [T.Exact (what, dtext ^ text)] in mk_preamble st what script and proc_proof st t = @@ -458,7 +459,7 @@ try let aux (inv, _) v = if I.overlaps synth inv then None else if I.S.is_empty inv then Some (get_note (fun st -> proc_proof st v)) else - Some (get_note (fun _ -> [T.Apply (v, dtext ^ "dependent")])) + Some (get_note (fun _ -> [T.Exact (v, dtext ^ "dependent")])) in let ps = T.list_map2_filter aux classes ts in let b = List.length ps > 1 in diff --git a/helm/software/components/acic_procedural/proceduralTeX.ml b/helm/software/components/acic_procedural/proceduralTeX.ml index 55be4ddb3..279ebecb9 100644 --- a/helm/software/components/acic_procedural/proceduralTeX.ml +++ b/helm/software/components/acic_procedural/proceduralTeX.ml @@ -194,6 +194,8 @@ let rec xl frm = function | T.Statement _ :: l | T.Qed _ :: l -> xl frm l + | T.Exact (t, _) :: l -> + F.fprintf frm "\\Exact{%a}" xat t; xl frm l | T.Intros (_, [r], _) :: l -> F.fprintf frm "\\Intro{%a}{%a}" xx r xl l | T.LetIn (r, v, _) :: l -> diff --git a/helm/software/components/acic_procedural/proceduralTypes.ml b/helm/software/components/acic_procedural/proceduralTypes.ml index cb4c11d2e..75ce2ee64 100644 --- a/helm/software/components/acic_procedural/proceduralTypes.ml +++ b/helm/software/components/acic_procedural/proceduralTypes.ml @@ -74,6 +74,7 @@ type step = Note of note | Statement of flavour * name * what * body * note | Qed of note | Id of note + | Exact of what * note | Intros of count option * name list * note | Cut of name * what * note | LetIn of name * what * note @@ -166,6 +167,10 @@ let mk_id punctation = let tactic = G.IdTac floc in mk_tactic tactic punctation +let mk_exact t punctation = + let tactic = G.Exact (floc, t) in + mk_tactic tactic punctation + let mk_intros xi xids punctation = let tactic = G.Intros (floc, (xi, xids)) in mk_tactic tactic punctation @@ -239,6 +244,7 @@ let rec render_step sep a = function | Statement (f, n, t, v, s) -> mk_statement f n t v :: mk_thnote s a | Inductive (lps, ts, s) -> mk_inductive lps ts :: mk_thnote s a | Qed s -> mk_qed :: mk_tacnote s a + | Exact (t, s) -> mk_exact t sep :: mk_tacnote s a | Id s -> mk_id sep :: mk_tacnote s a | Intros (c, ns, s) -> mk_intros c ns sep :: mk_tacnote s a | Cut (n, t, s) -> mk_cut n t sep :: mk_tacnote s a @@ -275,6 +281,7 @@ let rec count_step a = function | Note _ | Statement _ | Id _ + | Exact _ | Qed _ -> a | Branch (pps, _) -> List.fold_left count_steps a pps | _ -> succ a @@ -292,6 +299,7 @@ let rec count_node a = function | Intros _ | Clear _ | ClearBody _ -> a + | Exact (t, _) | Cut (_, t, _) | LetIn (_, t, _) | Apply (t, _) -> count a (H.cic t) diff --git a/helm/software/components/acic_procedural/proceduralTypes.mli b/helm/software/components/acic_procedural/proceduralTypes.mli index aa6ad3aa5..13161daad 100644 --- a/helm/software/components/acic_procedural/proceduralTypes.mli +++ b/helm/software/components/acic_procedural/proceduralTypes.mli @@ -53,6 +53,7 @@ type step = Note of note | Statement of flavour * name * what * body * note | Qed of note | Id of note + | Exact of what * note | Intros of count option * name list * note | Cut of name * what * note | LetIn of name * what * note diff --git a/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/Makefile b/helm/software/matita/contribs/limits/Makefile similarity index 100% rename from helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/Makefile rename to helm/software/matita/contribs/limits/Makefile diff --git a/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/class_defs.ma b/helm/software/matita/contribs/limits/class_defs.ma similarity index 100% rename from helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/class_defs.ma rename to helm/software/matita/contribs/limits/class_defs.ma diff --git a/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/class_eq.ma b/helm/software/matita/contribs/limits/class_eq.ma similarity index 100% rename from helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/class_eq.ma rename to helm/software/matita/contribs/limits/class_eq.ma diff --git a/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/coa_defs.ma b/helm/software/matita/contribs/limits/coa_defs.ma similarity index 100% rename from helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/coa_defs.ma rename to helm/software/matita/contribs/limits/coa_defs.ma diff --git a/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/coa_props.ma b/helm/software/matita/contribs/limits/coa_props.ma similarity index 100% rename from helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/coa_props.ma rename to helm/software/matita/contribs/limits/coa_props.ma diff --git a/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/depends b/helm/software/matita/contribs/limits/depends similarity index 100% rename from helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/depends rename to helm/software/matita/contribs/limits/depends diff --git a/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/domain_data.ma b/helm/software/matita/contribs/limits/domain_data.ma similarity index 100% rename from helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/domain_data.ma rename to helm/software/matita/contribs/limits/domain_data.ma diff --git a/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/domain_defs.ma b/helm/software/matita/contribs/limits/domain_defs.ma similarity index 100% rename from helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/domain_defs.ma rename to helm/software/matita/contribs/limits/domain_defs.ma diff --git a/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/iff.ma b/helm/software/matita/contribs/limits/iff.ma similarity index 100% rename from helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/iff.ma rename to helm/software/matita/contribs/limits/iff.ma diff --git a/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/root b/helm/software/matita/contribs/limits/root similarity index 100% rename from helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/root rename to helm/software/matita/contribs/limits/root diff --git a/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/subset_defs.ma b/helm/software/matita/contribs/limits/subset_defs.ma similarity index 100% rename from helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/subset_defs.ma rename to helm/software/matita/contribs/limits/subset_defs.ma -- 2.39.2