From 916c558005ed665c62699a7a4c5347870c8a3efb Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Thu, 16 Apr 2009 21:50:52 +0000 Subject: [PATCH] Procedural: we corrected two errors about the handling of mutcase (the "cases" tactic is now disabled because it does not work well with the current kernel) transcript: we immplemented uri substitution in Verbatim items matitaInit: new option -no-default-includes for omitting the devels included by default (this is to compile procedural/library :) ) procedural/library: bug fix --- .../components/acic_procedural/.depend | 14 +++--- .../components/acic_procedural/.depend.opt | 14 +++--- .../components/acic_procedural/Makefile | 2 +- .../acic_procedural/acic2Procedural.ml | 16 +++---- .../{procedural1.ml => procedural2.ml} | 22 ++------- .../{procedural1.mli => procedural2.mli} | 0 .../acic_procedural/proceduralConversion.ml | 5 +- .../acic_procedural/proceduralOptimizer.ml | 4 ++ .../acic_procedural/proceduralTypes.ml | 2 +- .../components/binaries/transcript/engine.ml | 3 ++ .../contribs/procedural/Makefile.common | 6 +-- .../contribs/procedural/library/Makefile | 1 + .../contribs/procedural/library/preamble.ma | 47 ++++++------------- .../matita/library/logic/connectives.ma | 1 - helm/software/matita/matitaInit.ml | 8 +++- 15 files changed, 63 insertions(+), 82 deletions(-) rename helm/software/components/acic_procedural/{procedural1.ml => procedural2.ml} (96%) rename helm/software/components/acic_procedural/{procedural1.mli => procedural2.mli} (100%) diff --git a/helm/software/components/acic_procedural/.depend b/helm/software/components/acic_procedural/.depend index 122ed1938..189d36ff1 100644 --- a/helm/software/components/acic_procedural/.depend +++ b/helm/software/components/acic_procedural/.depend @@ -1,4 +1,4 @@ -procedural1.cmi: proceduralTypes.cmi +procedural2.cmi: proceduralTypes.cmi proceduralTeX.cmi: proceduralTypes.cmi proceduralHelpers.cmo: proceduralHelpers.cmi proceduralHelpers.cmx: proceduralHelpers.cmi @@ -14,15 +14,15 @@ proceduralMode.cmo: proceduralClassify.cmi proceduralMode.cmi proceduralMode.cmx: proceduralClassify.cmx proceduralMode.cmi proceduralConversion.cmo: proceduralHelpers.cmi proceduralConversion.cmi proceduralConversion.cmx: proceduralHelpers.cmx proceduralConversion.cmi -procedural1.cmo: proceduralTypes.cmi proceduralHelpers.cmi \ - proceduralConversion.cmi proceduralClassify.cmi procedural1.cmi -procedural1.cmx: proceduralTypes.cmx proceduralHelpers.cmx \ - proceduralConversion.cmx proceduralClassify.cmx procedural1.cmi +procedural2.cmo: proceduralTypes.cmi proceduralHelpers.cmi \ + proceduralConversion.cmi proceduralClassify.cmi procedural2.cmi +procedural2.cmx: proceduralTypes.cmx proceduralHelpers.cmx \ + proceduralConversion.cmx proceduralClassify.cmx procedural2.cmi proceduralTeX.cmo: proceduralTypes.cmi proceduralHelpers.cmi \ proceduralTeX.cmi proceduralTeX.cmx: proceduralTypes.cmx proceduralHelpers.cmx \ proceduralTeX.cmi -acic2Procedural.cmo: proceduralTypes.cmi proceduralTeX.cmi procedural1.cmi \ +acic2Procedural.cmo: proceduralTypes.cmi proceduralTeX.cmi procedural2.cmi \ acic2Procedural.cmi -acic2Procedural.cmx: proceduralTypes.cmx proceduralTeX.cmx procedural1.cmx \ +acic2Procedural.cmx: proceduralTypes.cmx proceduralTeX.cmx procedural2.cmx \ acic2Procedural.cmi diff --git a/helm/software/components/acic_procedural/.depend.opt b/helm/software/components/acic_procedural/.depend.opt index 122ed1938..189d36ff1 100644 --- a/helm/software/components/acic_procedural/.depend.opt +++ b/helm/software/components/acic_procedural/.depend.opt @@ -1,4 +1,4 @@ -procedural1.cmi: proceduralTypes.cmi +procedural2.cmi: proceduralTypes.cmi proceduralTeX.cmi: proceduralTypes.cmi proceduralHelpers.cmo: proceduralHelpers.cmi proceduralHelpers.cmx: proceduralHelpers.cmi @@ -14,15 +14,15 @@ proceduralMode.cmo: proceduralClassify.cmi proceduralMode.cmi proceduralMode.cmx: proceduralClassify.cmx proceduralMode.cmi proceduralConversion.cmo: proceduralHelpers.cmi proceduralConversion.cmi proceduralConversion.cmx: proceduralHelpers.cmx proceduralConversion.cmi -procedural1.cmo: proceduralTypes.cmi proceduralHelpers.cmi \ - proceduralConversion.cmi proceduralClassify.cmi procedural1.cmi -procedural1.cmx: proceduralTypes.cmx proceduralHelpers.cmx \ - proceduralConversion.cmx proceduralClassify.cmx procedural1.cmi +procedural2.cmo: proceduralTypes.cmi proceduralHelpers.cmi \ + proceduralConversion.cmi proceduralClassify.cmi procedural2.cmi +procedural2.cmx: proceduralTypes.cmx proceduralHelpers.cmx \ + proceduralConversion.cmx proceduralClassify.cmx procedural2.cmi proceduralTeX.cmo: proceduralTypes.cmi proceduralHelpers.cmi \ proceduralTeX.cmi proceduralTeX.cmx: proceduralTypes.cmx proceduralHelpers.cmx \ proceduralTeX.cmi -acic2Procedural.cmo: proceduralTypes.cmi proceduralTeX.cmi procedural1.cmi \ +acic2Procedural.cmo: proceduralTypes.cmi proceduralTeX.cmi procedural2.cmi \ acic2Procedural.cmi -acic2Procedural.cmx: proceduralTypes.cmx proceduralTeX.cmx procedural1.cmx \ +acic2Procedural.cmx: proceduralTypes.cmx proceduralTeX.cmx procedural2.cmx \ acic2Procedural.cmi diff --git a/helm/software/components/acic_procedural/Makefile b/helm/software/components/acic_procedural/Makefile index d0304111f..5acd1d21d 100644 --- a/helm/software/components/acic_procedural/Makefile +++ b/helm/software/components/acic_procedural/Makefile @@ -8,7 +8,7 @@ INTERFACE_FILES = \ proceduralTypes.mli \ proceduralMode.mli \ proceduralConversion.mli \ - procedural1.mli \ + procedural2.mli \ proceduralTeX.mli \ acic2Procedural.mli \ $(NULL) diff --git a/helm/software/components/acic_procedural/acic2Procedural.ml b/helm/software/components/acic_procedural/acic2Procedural.ml index f749ce8d2..0eb8d8efb 100644 --- a/helm/software/components/acic_procedural/acic2Procedural.ml +++ b/helm/software/components/acic_procedural/acic2Procedural.ml @@ -26,7 +26,7 @@ module L = Librarian module T = ProceduralTypes -module P1 = Procedural1 +module P2 = Procedural2 module X = ProceduralTeX let tex_formatter = ref None @@ -35,10 +35,10 @@ let tex_formatter = ref None let procedural_of_acic_object ~ids_to_inner_sorts ~ids_to_inner_types ?info ?depth ?flavour prefix anobj = - let st = P1.init ~ids_to_inner_sorts ~ids_to_inner_types ?depth [] in - L.time_stamp "P : LEVEL 1 "; - HLog.debug "Procedural: level 1 transformation"; - let steps = P1.proc_obj st ?flavour ?info anobj in + let st = P2.init ~ids_to_inner_sorts ~ids_to_inner_types ?depth [] in + L.time_stamp "P : LEVEL 2 "; + HLog.debug "Procedural: level 2 transformation"; + let steps = P2.proc_obj st ?flavour ?info anobj in let _ = match !tex_formatter with | None -> () | Some frm -> X.tex_of_steps frm ids_to_inner_sorts steps @@ -50,9 +50,9 @@ let procedural_of_acic_object ~ids_to_inner_sorts ~ids_to_inner_types let procedural_of_acic_term ~ids_to_inner_sorts ~ids_to_inner_types ?depth prefix context annterm = - let st = P1.init ~ids_to_inner_sorts ~ids_to_inner_types ?depth context in - HLog.debug "Procedural: level 1 transformation"; - let steps = P1.proc_proof st annterm in + let st = P2.init ~ids_to_inner_sorts ~ids_to_inner_types ?depth context in + HLog.debug "Procedural: level 2 transformation"; + let steps = P2.proc_proof st annterm in let _ = match !tex_formatter with | None -> () | Some frm -> X.tex_of_steps frm ids_to_inner_sorts steps diff --git a/helm/software/components/acic_procedural/procedural1.ml b/helm/software/components/acic_procedural/procedural2.ml similarity index 96% rename from helm/software/components/acic_procedural/procedural1.ml rename to helm/software/components/acic_procedural/procedural2.ml index a0c0331f3..9dcd20304 100644 --- a/helm/software/components/acic_procedural/procedural1.ml +++ b/helm/software/components/acic_procedural/procedural2.ml @@ -176,19 +176,6 @@ let get_sub_names head l = let get_type msg st t = H.get_type msg st.context (H.cic t) -let clear_absts m = - let rec aux k n = function - | C.ALambda (id, s, v, t) when k > 0 -> - C.ALambda (id, s, v, aux (pred k) n t) - | C.ALambda (_, _, _, t) when n > 0 -> - aux 0 (pred n) (Cn.lift 1 (-1) t) - | t when n > 0 -> - Printf.eprintf "A2P.clear_absts: %u %s\n" n (Pp.ppterm (H.cic t)); - assert false - | t -> t - in - aux m - (* proof construction *******************************************************) let anonymous_premise = C.Name "UNNAMED" @@ -405,11 +392,10 @@ and proc_case st what uri tyno u v ts = let names = H.get_ind_names uri tyno in let qs = proc_bkd_proofs (next st) synth names classes ts in let lpsno, _ = H.get_ind_type uri tyno in - let ps, sort_disp = H.get_ind_parameters st.context (H.cic v) in + let ps, _ = H.get_ind_parameters st.context (H.cic v) in let _, rps = HEL.split_nth lpsno ps in - let rpsno = List.length rps in - let predicate = clear_absts rpsno (1 - sort_disp) u in - let e = Cn.mk_pattern rpsno predicate in + let rpsno = List.length rps in + let e = Cn.mk_pattern rpsno u in let text = "" in let script = List.rev (mk_arg st v) in script @ [T.Cases (v, e, dtext ^ text); T.Branch (qs, "")] @@ -442,7 +428,9 @@ and proc_proof st t = | C.AMutConstruct _ as what -> proc_mutconstruct (f st) what | C.AConst _ as what -> proc_const (f st) what | C.AAppl (_, hd :: tl) as what -> proc_appl (f st) what hd tl +(* FG: we deactivate the tactic "cases" because it does not work properly | C.AMutCase (_, uri, i, u, v, ts) as what -> proc_case (f st) what uri i u v ts +*) | what -> proc_other (f st) what and proc_bkd_proofs st synth names classes ts = diff --git a/helm/software/components/acic_procedural/procedural1.mli b/helm/software/components/acic_procedural/procedural2.mli similarity index 100% rename from helm/software/components/acic_procedural/procedural1.mli rename to helm/software/components/acic_procedural/procedural2.mli diff --git a/helm/software/components/acic_procedural/proceduralConversion.ml b/helm/software/components/acic_procedural/proceduralConversion.ml index 3eadc2fcf..97e32b94a 100644 --- a/helm/software/components/acic_procedural/proceduralConversion.ml +++ b/helm/software/components/acic_procedural/proceduralConversion.ml @@ -59,7 +59,10 @@ let lift k n = | C.ARel (id, rid, m, b) as t -> if m < k then t else if m + n > 0 then C.ARel (id, rid, m + n, b) else - assert false + begin + HLog.error (Printf.sprintf "ProceduralConversion.lift: %i %i" m n); + assert false + end | C.AConst (id, uri, xnss) -> C.AConst (id, uri, List.map (lift_xns k) xnss) | C.AVar (id, uri, xnss) -> C.AVar (id, uri, List.map (lift_xns k) xnss) | C.AMutInd (id, uri, tyno, xnss) -> C.AMutInd (id, uri, tyno, List.map (lift_xns k) xnss) diff --git a/helm/software/components/acic_procedural/proceduralOptimizer.ml b/helm/software/components/acic_procedural/proceduralOptimizer.ml index 6910613d2..c27966a4a 100644 --- a/helm/software/components/acic_procedural/proceduralOptimizer.ml +++ b/helm/software/components/acic_procedural/proceduralOptimizer.ml @@ -185,6 +185,10 @@ and opt_mutcase_critical g st es c uri tyno outty arg cases = let ps, sort_disp = H.get_ind_parameters c arg in let lps, rps = HEL.split_nth lpsno ps in let rpsno = List.length rps in + if rpsno = 0 && sort_disp = 0 then +(* FG: the transformation is not possible, we fall back into the plain case *) + opt_mutcase_plain g st es c uri tyno outty arg cases + else let predicate = clear_absts rpsno (1 - sort_disp) outty in let is_recursive t = I.S.mem tyno (I.get_mutinds_of_uri uri t) diff --git a/helm/software/components/acic_procedural/proceduralTypes.ml b/helm/software/components/acic_procedural/proceduralTypes.ml index b30d6e862..ed198d99b 100644 --- a/helm/software/components/acic_procedural/proceduralTypes.ml +++ b/helm/software/components/acic_procedural/proceduralTypes.ml @@ -206,7 +206,7 @@ let mk_cases what pattern punctation = mk_tactic tactic punctation let mk_apply t punctation = - let tactic = G.ApplyP (floc, t) in + let tactic = G.Apply (floc, t) in mk_tactic tactic punctation let mk_change t where pattern punctation = diff --git a/helm/software/components/binaries/transcript/engine.ml b/helm/software/components/binaries/transcript/engine.ml index 091987b65..027b03575 100644 --- a/helm/software/components/binaries/transcript/engine.ml +++ b/helm/software/components/binaries/transcript/engine.ml @@ -234,6 +234,9 @@ let produce st = | T.Section (b, id, _) as item -> let path = if b then id :: path else List.tl path in path, Some item + | T.Verbatim s -> + let pat, templ = st.input_base_uri, st.output_base_uri in + path, Some (T.Verbatim (Pcre.replace ~pat ~templ s)) | item -> path, Some item in let set_includes st name = diff --git a/helm/software/matita/contribs/procedural/Makefile.common b/helm/software/matita/contribs/procedural/Makefile.common index a6bc20571..7fdf63830 100644 --- a/helm/software/matita/contribs/procedural/Makefile.common +++ b/helm/software/matita/contribs/procedural/Makefile.common @@ -4,12 +4,8 @@ DIR = $(shell basename $$PWD) H = @ -MATITAOPTIONS = - TRANSCRIPT = $(BIN)../components/binaries/transcript/transcript.opt -OPTIONS = - LOG = log.txt MMAS = $(shell find -name "*.mma") @@ -42,4 +38,4 @@ clean.ma: endif mma: $(DEVEL).conf.xml clean.ma - $(H)$(TRANSCRIPT) $(OPTIONS) -C $(BIN) $(DEVEL) + $(H)$(TRANSCRIPT) $(TRANSCRIPTOPTIONS) -C $(BIN) $(DEVEL) diff --git a/helm/software/matita/contribs/procedural/library/Makefile b/helm/software/matita/contribs/procedural/library/Makefile index bd75dbd6d..0fa53112e 100644 --- a/helm/software/matita/contribs/procedural/library/Makefile +++ b/helm/software/matita/contribs/procedural/library/Makefile @@ -1,3 +1,4 @@ DEVEL = library +MATITAOPTIONS = -no-default-includes -onepass include ../Makefile.common diff --git a/helm/software/matita/contribs/procedural/library/preamble.ma b/helm/software/matita/contribs/procedural/library/preamble.ma index 89ee1a360..5bad82685 100644 --- a/helm/software/matita/contribs/procedural/library/preamble.ma +++ b/helm/software/matita/contribs/procedural/library/preamble.ma @@ -12,38 +12,21 @@ (* *) (**************************************************************************) -(* +default "true" cic:/matita/logic/connectives/True.ind. -default "equality" - cic:/Coq/Init/Logic/eq.ind - cic:/Coq/Init/Logic/sym_eq.con - cic:/Coq/Init/Logic/trans_eq.con - cic:/Coq/Init/Logic/eq_ind.con - cic:/Coq/Init/Logic/eq_ind_r.con - cic:/Coq/Init/Logic/eq_rec.con - cic:/Coq/Init/Logic/eq_rec_r.con - cic:/Coq/Init/Logic/eq_rect.con - cic:/Coq/Init/Logic/eq_rect_r.con - cic:/Coq/Init/Logic/f_equal.con - cic:/matita/procedural/Coq/preamble/f_equal1.con. - -default "true" - cic:/Coq/Init/Logic/True.ind. -default "false" - cic:/Coq/Init/Logic/False.ind. -default "absurd" - cic:/Coq/Init/Logic/absurd.con. - -interpretation "Coq's leibnitz's equality" 'eq x y = (cic:/Coq/Init/Logic/eq.ind#xpointer(1/1) _ x y). +default "false" cic:/matita/logic/connectives/False.ind. -theorem f_equal1 : \forall A,B:Type.\forall f:A\to B.\forall x,y:A. - x = y \to (f y) = (f x). - intros. - symmetry. - apply cic:/Coq/Init/Logic/f_equal.con. - assumption. -qed. +default "absurd" cic:/matita/logic/connectives/absurd.con. -alias id "land" = "cic:/matita/procedural/Coq/Init/Logic/and.ind#xpointer(1/1)". - -*) +default "equality" + cic:/matita/logic/equality/eq.ind + cic:/matita/logic/equality/sym_eq.con + cic:/matita/logic/equality/transitive_eq.con + cic:/matita/logic/equality/eq_ind.con + cic:/matita/logic/equality/eq_elim_r.con + cic:/matita/logic/equality/eq_rec.con + cic:/matita/logic/equality/eq_elim_r'.con + cic:/matita/logic/equality/eq_rect.con + cic:/matita/logic/equality/eq_elim_r''.con + cic:/matita/logic/equality/eq_f.con + cic:/matita/logic/equality/eq_OF_eq.con. diff --git a/helm/software/matita/library/logic/connectives.ma b/helm/software/matita/library/logic/connectives.ma index 6a20bc897..832d1a531 100644 --- a/helm/software/matita/library/logic/connectives.ma +++ b/helm/software/matita/library/logic/connectives.ma @@ -49,7 +49,6 @@ inductive Or (A,B:Prop) : Prop \def or_introl : A \to (Or A B) | or_intror : B \to (Or A B). -(*CSC: the URI must disappear: there is a bug now *) interpretation "logical or" 'or x y = (Or x y). theorem Or_ind': diff --git a/helm/software/matita/matitaInit.ml b/helm/software/matita/matitaInit.ml index f75cbcf48..aee55d60d 100644 --- a/helm/software/matita/matitaInit.ml +++ b/helm/software/matita/matitaInit.ml @@ -192,6 +192,7 @@ let parse_cmdline init_status = (HExtlib.normalize_path (absolutize path)^" "^uri) | _ -> raise (Failure "bad baseuri, use -b 'path::uri'") in + let no_default_includes = ref false in let arg_spec = let std_arg_spec = [ "-b", Arg.String set_baseuri, " forces the baseuri of path"; @@ -217,10 +218,12 @@ let parse_cmdline init_status = Helm_registry.set_bool "matita.system" true), ("Act on the system library instead of the user one" ^ "\n WARNING: not for the casual user"); - "-v", + "-no-default-includes", Arg.Set no_default_includes, + "Do not include the default searched paths for the include command"; + "-v", Arg.Unit (fun () -> Helm_registry.set_bool "matita.verbose" true), "Verbose mode"; - "--version", Arg.Unit print_version, "Prints version"; + "--version", Arg.Unit print_version, "Prints version" ] in let debug_arg_spec = if BuildTimeConf.debug then @@ -240,6 +243,7 @@ let parse_cmdline init_status = Helm_registry.set_list Helm_registry.of_string ~key ~value:l in Arg.parse arg_spec (add_l args) (usage ()); + let default_includes = if !no_default_includes then [] else default_includes in let includes = List.map (fun x -> HExtlib.normalize_path (absolutize x)) ((List.rev !includes) @ default_includes) -- 2.39.2