From: Ferruccio Guidi Date: Fri, 3 Jul 2009 15:28:01 +0000 (+0000) Subject: we now do some static analysis on the Automath text to possibly clear some language... X-Git-Tag: make_still_working~3753 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=2b821e608cc1fceebc13e85867a244fe02edf71e we now do some static analysis on the Automath text to possibly clear some language ambiguities --- diff --git a/helm/software/lambda-delta/.depend.opt b/helm/software/lambda-delta/.depend.opt index b68ea6dd8..b102e20ae 100644 --- a/helm/software/lambda-delta/.depend.opt +++ b/helm/software/lambda-delta/.depend.opt @@ -1,28 +1,21 @@ -lib/nUri.cmi: lib/nUri.cmo: lib/nUri.cmi lib/nUri.cmx: lib/nUri.cmi -lib/cps.cmo: -lib/cps.cmx: -lib/share.cmo: -lib/share.cmx: -lib/log.cmi: lib/log.cmo: lib/cps.cmx lib/log.cmi lib/log.cmx: lib/cps.cmx lib/log.cmi lib/time.cmo: lib/log.cmi lib/time.cmx: lib/log.cmx -lib/hierarchy.cmi: lib/hierarchy.cmo: lib/cps.cmx lib/hierarchy.cmi lib/hierarchy.cmx: lib/cps.cmx lib/hierarchy.cmi -lib/output.cmi: lib/output.cmo: lib/log.cmi lib/output.cmi lib/output.cmx: lib/log.cmx lib/output.cmi -automath/aut.cmo: -automath/aut.cmx: -automath/autOutput.cmi: automath/aut.cmx -automath/autOutput.cmo: lib/log.cmi lib/cps.cmx automath/aut.cmx \ - automath/autOutput.cmi -automath/autOutput.cmx: lib/log.cmx lib/cps.cmx automath/aut.cmx \ - automath/autOutput.cmi +automath/autProcess.cmi: automath/aut.cmx +automath/autProcess.cmo: automath/aut.cmx automath/autProcess.cmi +automath/autProcess.cmx: automath/aut.cmx automath/autProcess.cmi +automath/autOutput.cmi: automath/autProcess.cmi automath/aut.cmx +automath/autOutput.cmo: lib/log.cmi lib/cps.cmx automath/autProcess.cmi \ + automath/aut.cmx automath/autOutput.cmi +automath/autOutput.cmx: lib/log.cmx lib/cps.cmx automath/autProcess.cmx \ + automath/aut.cmx automath/autOutput.cmi automath/autParser.cmi: automath/aut.cmx automath/autParser.cmo: automath/aut.cmx automath/autParser.cmi automath/autParser.cmx: automath/aut.cmx automath/autParser.cmi @@ -130,11 +123,13 @@ toplevel/top.cmo: lib/time.cmx lib/output.cmi lib/nUri.cmi \ basic_rg/brgUntrusted.cmi basic_rg/brgType.cmi basic_rg/brgOutput.cmi \ basic_rg/brg.cmx basic_ag/bagUntrusted.cmi basic_ag/bagType.cmi \ basic_ag/bagReduction.cmi basic_ag/bagOutput.cmi basic_ag/bag.cmx \ - automath/autParser.cmi automath/autOutput.cmi automath/autLexer.cmx + automath/autProcess.cmi automath/autParser.cmi automath/autOutput.cmi \ + automath/autLexer.cmx toplevel/top.cmx: lib/time.cmx lib/output.cmx lib/nUri.cmx \ toplevel/metaOutput.cmx toplevel/metaBrg.cmx toplevel/metaBag.cmx \ toplevel/metaAut.cmx lib/log.cmx lib/hierarchy.cmx lib/cps.cmx \ basic_rg/brgUntrusted.cmx basic_rg/brgType.cmx basic_rg/brgOutput.cmx \ basic_rg/brg.cmx basic_ag/bagUntrusted.cmx basic_ag/bagType.cmx \ basic_ag/bagReduction.cmx basic_ag/bagOutput.cmx basic_ag/bag.cmx \ - automath/autParser.cmx automath/autOutput.cmx automath/autLexer.cmx + automath/autProcess.cmx automath/autParser.cmx automath/autOutput.cmx \ + automath/autLexer.cmx diff --git a/helm/software/lambda-delta/Makefile b/helm/software/lambda-delta/Makefile index 24807817e..c5f715d74 100644 --- a/helm/software/lambda-delta/Makefile +++ b/helm/software/lambda-delta/Makefile @@ -17,8 +17,8 @@ test: $(MAIN).opt $(H)./$(MAIN).opt -S 3 $(O) $(INPUT) > log.txt test-si: $(MAIN).opt - @echo " HELENA -u $(INPUT-ORIG)" - $(H)./$(MAIN).opt -u -S 3 $(O) $(INPUT-ORIG) > log.txt + @echo " HELENA -c -u $(INPUT)" + $(H)./$(MAIN).opt -c -u -S 3 $(O) $(INPUT) > log.txt meta: $(MAIN).opt @echo " HELENA -m meta.txt $(INPUT)" diff --git a/helm/software/lambda-delta/README b/helm/software/lambda-delta/README index 91e936067..8087dec9d 100644 --- a/helm/software/lambda-delta/README +++ b/helm/software/lambda-delta/README @@ -2,7 +2,7 @@ Helena Checker 0.8.0 M (June 2008) * type "make" or "make opt" to compile the native executable -* type "make test" to parse the grundlagen +* type "make test-si" to parse the grundlagen it generates a log.txt with the grundlagen contents statistics * type "make clean" to remove the products of compilation diff --git a/helm/software/lambda-delta/automath/Make b/helm/software/lambda-delta/automath/Make index 9a773e0fc..29d237864 100644 --- a/helm/software/lambda-delta/automath/Make +++ b/helm/software/lambda-delta/automath/Make @@ -1 +1 @@ -aut autOutput autParser autLexer +aut autProcess autOutput autParser autLexer diff --git a/helm/software/lambda-delta/automath/aut.ml b/helm/software/lambda-delta/automath/aut.ml index dc938821e..4b1dffd9e 100644 --- a/helm/software/lambda-delta/automath/aut.ml +++ b/helm/software/lambda-delta/automath/aut.ml @@ -18,7 +18,7 @@ type term = Sort of bool (* sorts: true = TYPE, false = PROP *) | Appl of term * term (* application: argument, function *) | Abst of id * term * term (* abstraction: name, type, body *) -type item = Section of id option (* section: Some = open/reopen, None = close last *) +type item = Section of (bool * id) option (* section: Some true = open, Some false = reopen, None = close last *) | Context of qid option (* context: Some = last node, None = root *) | Block of id * term (* block opener: name, type *) | Decl of id * term (* declaration: name, type *) diff --git a/helm/software/lambda-delta/automath/autOutput.ml b/helm/software/lambda-delta/automath/autOutput.ml index ffbdfdb20..6ca42e6c6 100644 --- a/helm/software/lambda-delta/automath/autOutput.ml +++ b/helm/software/lambda-delta/automath/autOutput.ml @@ -12,6 +12,7 @@ module P = Printf module L = Log module A = Aut +module R = AutProcess type counters = { sections: int; @@ -85,3 +86,13 @@ let print_counters f c = L.warn (P.sprintf " Global Int. Complexity: unknown"); L.warn (P.sprintf " + Abbreviation nodes: %7u" c.xnodes); f () + +let print_process_counters f c = + let f iao iar iac = + L.warn (P.sprintf " Automath process summary"); + L.warn (P.sprintf " Implicit after opening: %7u" iao); + L.warn (P.sprintf " Implicit after reopening: %7u" iar); + L.warn (P.sprintf " Implicit after closing: %7u" iac); + f () + in + R.get_counters f c diff --git a/helm/software/lambda-delta/automath/autOutput.mli b/helm/software/lambda-delta/automath/autOutput.mli index a73697418..9d293a97f 100644 --- a/helm/software/lambda-delta/automath/autOutput.mli +++ b/helm/software/lambda-delta/automath/autOutput.mli @@ -1,27 +1,13 @@ -(* Copyright (C) 2000, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department, University of Bologna, Italy. + ||I|| + ||T|| HELM is free software; you can redistribute it and/or + ||A|| modify it under the terms of the GNU General Public License + \ / version 2 or (at your option) any later version. + \ / This software is distributed as is, NO WARRANTY. + V_______________________________________________________________ *) type counters @@ -30,3 +16,5 @@ val initial_counters: counters val count_item: (counters -> 'a) -> counters -> Aut.item -> 'a val print_counters: (unit -> 'a) -> counters -> 'a + +val print_process_counters: (unit -> 'a) -> AutProcess.status -> 'a diff --git a/helm/software/lambda-delta/automath/autParser.mly b/helm/software/lambda-delta/automath/autParser.mly index 3bf5f3d00..c8e836e79 100644 --- a/helm/software/lambda-delta/automath/autParser.mly +++ b/helm/software/lambda-delta/automath/autParser.mly @@ -72,19 +72,19 @@ | term CM terms { $1 :: $3 } ; item: - | PLUS IDENT { A.Section (Some $2) } - | PLUS TIMES IDENT { A.Section (Some $3) } - | MINUS IDENT { A.Section None } - | EXIT { A.Section None } - | star { A.Context None } - | qid star { A.Context (Some $1) } - | IDENT DEF EB sc term { A.Block ($1, $5) } - | IDENT sc term DEF EB { A.Block ($1, $3) } - | OB IDENT oftype term CB { A.Block ($2, $4) } - | IDENT DEF PN sc term { A.Decl ($1, $5) } - | IDENT sc term DEF PN { A.Decl ($1, $3) } - | IDENT DEF expand term sc term { A.Def ($1, $6, $3, $4) } - | IDENT sc term DEF expand term { A.Def ($1, $3, $5, $6) } + | PLUS IDENT { A.Section (Some (true, $2)) } + | PLUS TIMES IDENT { A.Section (Some (false, $3)) } + | MINUS IDENT { A.Section None } + | EXIT { A.Section None } + | star { A.Context None } + | qid star { A.Context (Some $1) } + | IDENT DEF EB sc term { A.Block ($1, $5) } + | IDENT sc term DEF EB { A.Block ($1, $3) } + | OB IDENT oftype term CB { A.Block ($2, $4) } + | IDENT DEF PN sc term { A.Decl ($1, $5) } + | IDENT sc term DEF PN { A.Decl ($1, $3) } + | IDENT DEF expand term sc term { A.Def ($1, $6, $3, $4) } + | IDENT sc term DEF expand term { A.Def ($1, $3, $5, $6) } ; items: | { [] } diff --git a/helm/software/lambda-delta/automath/autProcess.ml b/helm/software/lambda-delta/automath/autProcess.ml new file mode 100644 index 000000000..c6ef561f0 --- /dev/null +++ b/helm/software/lambda-delta/automath/autProcess.ml @@ -0,0 +1,53 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department, University of Bologna, Italy. + ||I|| + ||T|| HELM is free software; you can redistribute it and/or + ||A|| modify it under the terms of the GNU General Public License + \ / version 2 or (at your option) any later version. + \ / This software is distributed as is, NO WARRANTY. + V_______________________________________________________________ *) + +module A = Aut + +type status = { + opening : bool; (* just opened section *) + reopening: bool; (* just reopened section *) + closing : bool; (* just closed section *) + iao : int; (* implicit context after opening section *) + iar : int; (* implicit context after reopening section *) + iac : int (* implicit context after closing section *) +} + +(* internal functions *******************************************************) + +let proc_section f st = function + | Some (true, _) -> f {st with opening = true} + | Some (false, _) -> f {st with reopening = true} + | None -> f {st with closing = true} + +let proc_context f st = + f {st with opening = false; reopening = false; closing = false} + +let proc_proper f st = + let st = if st.opening then {st with iao = succ st.iao} else st in + let st = if st.reopening then {st with iar = succ st.iar} else st in + let st = if st.closing then {st with iac = succ st.iac} else st in + proc_context f st + +let proc_item f st item = match item with + | A.Section section -> proc_section f st section item + | A.Context _ -> proc_context f st item + | _ -> proc_proper f st item + +(* interface functions ******************************************************) + +let initial_status = { + opening = false; reopening = false; closing = false; + iao = 0; iar = 0; iac = 0 +} + +let process_item = proc_item + +let get_counters f st = f st.iao st.iar st.iac diff --git a/helm/software/lambda-delta/automath/autProcess.mli b/helm/software/lambda-delta/automath/autProcess.mli new file mode 100644 index 000000000..61cd61d05 --- /dev/null +++ b/helm/software/lambda-delta/automath/autProcess.mli @@ -0,0 +1,18 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department, University of Bologna, Italy. + ||I|| + ||T|| HELM is free software; you can redistribute it and/or + ||A|| modify it under the terms of the GNU General Public License + \ / version 2 or (at your option) any later version. + \ / This software is distributed as is, NO WARRANTY. + V_______________________________________________________________ *) + +type status + +val initial_status: status + +val process_item: (status -> Aut.item -> 'a) -> status -> Aut.item -> 'a + +val get_counters: (int -> int -> int -> 'a) -> status -> 'a diff --git a/helm/software/lambda-delta/basic_ag/bagReduction.mli b/helm/software/lambda-delta/basic_ag/bagReduction.mli index ead9d5118..28c29e7f2 100644 --- a/helm/software/lambda-delta/basic_ag/bagReduction.mli +++ b/helm/software/lambda-delta/basic_ag/bagReduction.mli @@ -9,7 +9,6 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) - exception LRefNotFound of Bag.message type ho_whd_result = diff --git a/helm/software/lambda-delta/toplevel/metaAut.ml b/helm/software/lambda-delta/toplevel/metaAut.ml index 7e18bd1e5..48628b2bb 100644 --- a/helm/software/lambda-delta/toplevel/metaAut.ml +++ b/helm/software/lambda-delta/toplevel/metaAut.ml @@ -28,7 +28,7 @@ type status = { node: context_node; (* current context node *) nodes: context_node list; (* context node list *) line: int; (* line number *) - explicit: bool (* need explicit context root? *) + cover: string (* initial segment of URI hierarchy *) } type resolver = Local of int @@ -38,22 +38,23 @@ let hsize = 7000 (* hash tables initial size *) (* Internal functions *******************************************************) -let initial_status size = { - path = []; node = None; nodes = []; line = 1; explicit = true; +let initial_status size cover = { + path = []; node = None; nodes = []; line = 1; cover = cover; henv = H.create size; hcnt = H.create size } let id_of_name (id, _, _) = id -let mk_qid id path = - let str = String.concat "/" path in - let str = Filename.concat str id in +let mk_qid st id path = + let uripath = if st.cover = "" then path else st.cover :: path in + let str = String.concat "/" uripath in + let str = Filename.concat str id in U.uri_of_string ("ld:/" ^ str), id, path let uri_of_qid (uri, _, _) = uri let complete_qid f st (id, is_local, qs) = - let f qs = f (mk_qid id qs) in + let f qs = f (mk_qid st id qs) in let f path = Cps.list_rev_append f path ~tail:qs in let rec skip f = function | phd :: ptl, qshd :: _ when phd = qshd -> f ptl @@ -62,17 +63,17 @@ let complete_qid f st (id, is_local, qs) = in if is_local then f st.path else skip f (st.path, qs) -let relax_qid f (_, id, path) = - let f path = f (mk_qid id path) in +let relax_qid f st (_, id, path) = + let f path = f (mk_qid st id path) in let f = function | _ :: tl -> Cps.list_rev f tl | [] -> assert false in Cps.list_rev f path -let relax_opt_qid f = function +let relax_opt_qid f st = function | None -> f None - | Some qid -> let f qid = f (Some qid) in relax_qid f qid + | Some qid -> let f qid = f (Some qid) in relax_qid f st qid let resolve_lref f st l lenv id = let rec aux f i = function @@ -95,7 +96,7 @@ let resolve_gref f st qid = let resolve_gref_relaxed f st qid = let rec g qid = function - | None -> relax_qid (resolve_gref g st) qid + | None -> relax_qid (resolve_gref g st) st qid | Some args -> f qid args in resolve_gref g st qid @@ -109,7 +110,7 @@ let get_pars f st = function let get_pars_relaxed f st = let rec g pars = function | None -> f pars - | Some node -> relax_opt_qid (get_pars g st) node + | Some node -> relax_opt_qid (get_pars g st) st node in get_pars g st st.node @@ -145,7 +146,7 @@ let rec xlate_term f st lenv = function resolve_lref f st l lenv (id_of_name name) let xlate_item f st = function - | A.Section (Some name) -> + | A.Section (Some (_, name)) -> f {st with path = name :: st.path; nodes = st.node :: st.nodes} None | A.Section None -> begin match st.path, st.nodes with @@ -200,6 +201,7 @@ let xlate_item f st = function (* Interface functions ******************************************************) -let initial_status = initial_status hsize +let initial_status ?(cover="") () = + initial_status hsize cover let meta_of_aut = xlate_item diff --git a/helm/software/lambda-delta/toplevel/metaAut.mli b/helm/software/lambda-delta/toplevel/metaAut.mli index 128215cc4..b5c7e0b69 100644 --- a/helm/software/lambda-delta/toplevel/metaAut.mli +++ b/helm/software/lambda-delta/toplevel/metaAut.mli @@ -1,30 +1,16 @@ -(* Copyright (C) 2000, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department, University of Bologna, Italy. + ||I|| + ||T|| HELM is free software; you can redistribute it and/or + ||A|| modify it under the terms of the GNU General Public License + \ / version 2 or (at your option) any later version. + \ / This software is distributed as is, NO WARRANTY. + V_______________________________________________________________ *) type status -val initial_status: status +val initial_status: ?cover:string -> unit -> status val meta_of_aut: (status -> Meta.item -> 'a) -> status -> Aut.item -> 'a diff --git a/helm/software/lambda-delta/toplevel/top.ml b/helm/software/lambda-delta/toplevel/top.ml index 842f02b2d..873d5c590 100644 --- a/helm/software/lambda-delta/toplevel/top.ml +++ b/helm/software/lambda-delta/toplevel/top.ml @@ -15,6 +15,7 @@ module C = Cps module L = Log module H = Hierarchy module O = Output +module AP = AutProcess module AO = AutOutput module MA = MetaAut module MO = MetaOutput @@ -28,6 +29,7 @@ module BagR = BagReduction module BagU = BagUntrusted type status = { + ast : AP.status; mst : MA.status; ac : AO.counters; mc : MO.counters; @@ -35,12 +37,13 @@ type status = { bagc: BagO.counters } -let initial_status = { +let initial_status cover = { ac = AO.initial_counters; mc = MO.initial_counters; brgc = BrgO.initial_counters; bagc = BagO.initial_counters; - mst = MA.initial_status + mst = MA.initial_status ~cover (); + ast = AP.initial_status } let count count_fun c item = @@ -54,6 +57,10 @@ let bag_error s msg = let brg_error s msg = L.error BrgO.specs (L.Warn s :: L.Loc :: msg); flush () +let process_item f st = + let f ast = f {st with ast = ast} in + AP.process_item f st.ast + (* kernel related ***********************************************************) type kernel = Brg | Bag @@ -101,10 +108,11 @@ let si () = match !kernel with let main = try - let version_string = "Helena 0.8.0 M - June 2009" in + let version_string = "Helena 0.8.0 M - July 2009" in let stage = ref 3 in let meta_file = ref None in let progress = ref false in + let use_cover = ref true in let set_hierarchy s = let f = function | Some g -> H.graph := g @@ -170,27 +178,36 @@ try in (* stage 0 *) let st = {st with ac = count AO.count_item st.ac item} in - let st = - if !stage > 0 then MA.meta_of_aut (f st) st.mst item else st + let f st item = + let st = + if !stage > 0 then MA.meta_of_aut (f st) st.mst item else st + in + aux st tl in - aux st tl - in + process_item f st item + in O.clear_reductions (); - let st = aux initial_status book in + let cover = + if !use_cover then Filename.chop_extension (Filename.basename name) + else "" + in + let st = aux (initial_status cover) book in if !L.level > 0 then Time.utime_stamp "processed"; if !L.level > 2 then AO.print_counters C.start st.ac; + if !L.level > 2 then AO.print_process_counters C.start st.ast; if !L.level > 2 && !stage > 0 then MO.print_counters C.start st.mc; if !L.level > 2 && !stage > 1 then print_counters st; if !L.level > 2 && !stage > 1 then O.print_reductions () in let help = - "Usage: helena [ -Vipu | -Ss | -m | -hk ] ...\n\n" ^ + "Usage: helena [ -Vcipu | -Ss | -m | -hk ] ...\n\n" ^ "Summary levels: 0 just errors, 1 time stamps, 2 processed file names, \ 3 data information, 4 typing information, 5 reduction information\n\n" ^ "Stages: 0 parsing, 1 to intermediate, 2 to untrusted, 3 to trusted\n" in let help_S = " set summary level" in let help_V = " show version information" in + let help_c = " disable initial segment of URI hierarchy" in let help_h = " set type hierarchy" in let help_i = " show local references by index" in let help_k = " set kernel version" in @@ -203,6 +220,7 @@ try Arg.parse [ ("-S", Arg.Int set_summary, help_S); ("-V", Arg.Unit print_version, help_V); + ("-c", Arg.Clear use_cover, help_c); ("-h", Arg.String set_hierarchy, help_h); ("-i", Arg.Set O.indexes, help_i); ("-k", Arg.String set_kernel, help_k);