From 4c157ac5c58f34fffc98289c2d2e71032d584a83 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Mon, 22 Feb 2010 18:53:10 +0000 Subject: [PATCH 1/1] - we completed the text parser fixing the syntactic shortcuts - we can now parse several files without loosing the status - some imperative variables refactored --- helm/software/lambda-delta/.depend.opt | 115 +++++++++--------- helm/software/lambda-delta/Make | 2 +- helm/software/lambda-delta/Makefile | 4 +- .../lambda-delta/automath/autLexer.mll | 5 +- .../lambda-delta/automath/autProcess.ml | 2 +- .../lambda-delta/automath/autProcess.mli | 2 +- .../lambda-delta/basic_ag/bagOutput.ml | 2 +- .../lambda-delta/basic_rg/brgOutput.ml | 2 +- helm/software/lambda-delta/common/Make | 2 +- helm/software/lambda-delta/common/entity.ml | 12 +- .../software/lambda-delta/common/hierarchy.ml | 3 + .../lambda-delta/common/hierarchy.mli | 2 + helm/software/lambda-delta/common/options.ml | 37 ++++++ helm/software/lambda-delta/common/output.ml | 7 +- helm/software/lambda-delta/common/output.mli | 4 - .../lambda-delta/complete_rg/crgAut.ml | 18 +-- .../lambda-delta/complete_rg/crgAut.mli | 4 +- .../lambda-delta/complete_rg/crgTxt.ml | 45 ++++--- .../lambda-delta/complete_rg/crgTxt.mli | 4 +- .../lambda-delta/examples/exp_math/L.hln | 43 +++---- .../lambda-delta/examples/exp_math/Make | 2 +- .../lambda-delta/examples/exp_math/Makefile | 4 +- .../lambda-delta/examples/exp_math/T0.hln | 35 ++++++ .../examples/exp_math/preamble.hln | 8 ++ helm/software/lambda-delta/lib/log.ml | 3 + helm/software/lambda-delta/lib/log.mli | 2 + helm/software/lambda-delta/text/txt.ml | 3 +- helm/software/lambda-delta/text/txtLexer.mll | 61 +++++----- helm/software/lambda-delta/text/txtParser.mly | 50 ++++---- helm/software/lambda-delta/text/txtTxt.ml | 1 - .../software/lambda-delta/toplevel/metaAut.ml | 16 +-- .../lambda-delta/toplevel/metaAut.mli | 4 +- helm/software/lambda-delta/toplevel/top.ml | 67 ++++++---- 33 files changed, 346 insertions(+), 225 deletions(-) create mode 100644 helm/software/lambda-delta/common/options.ml create mode 100644 helm/software/lambda-delta/examples/exp_math/T0.hln create mode 100644 helm/software/lambda-delta/examples/exp_math/preamble.hln diff --git a/helm/software/lambda-delta/.depend.opt b/helm/software/lambda-delta/.depend.opt index c299acf63..d85664986 100644 --- a/helm/software/lambda-delta/.depend.opt +++ b/helm/software/lambda-delta/.depend.opt @@ -10,6 +10,21 @@ 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 +common/options.cmo: lib/cps.cmx +common/options.cmx: lib/cps.cmx +common/hierarchy.cmi: +common/hierarchy.cmo: lib/cps.cmx common/hierarchy.cmi +common/hierarchy.cmx: lib/cps.cmx common/hierarchy.cmi +common/output.cmi: +common/output.cmo: common/options.cmx lib/log.cmi common/output.cmi +common/output.cmx: common/options.cmx lib/log.cmx common/output.cmi +common/entity.cmo: common/options.cmx lib/nUri.cmi automath/aut.cmx +common/entity.cmx: common/options.cmx lib/nUri.cmx automath/aut.cmx +common/library.cmi: common/entity.cmx +common/library.cmo: lib/nUri.cmi common/hierarchy.cmi common/entity.cmx \ + lib/cps.cmx common/library.cmi +common/library.cmx: lib/nUri.cmx common/hierarchy.cmx common/entity.cmx \ + lib/cps.cmx common/library.cmi text/txt.cmo: text/txt.cmx: text/txtParser.cmi: text/txt.cmx @@ -33,28 +48,15 @@ automath/autOutput.cmx: lib/log.cmx lib/cps.cmx automath/autProcess.cmx \ automath/autParser.cmi: automath/aut.cmx automath/autParser.cmo: automath/aut.cmx automath/autParser.cmi automath/autParser.cmx: automath/aut.cmx automath/autParser.cmi -automath/autLexer.cmo: lib/log.cmi automath/autParser.cmi -automath/autLexer.cmx: lib/log.cmx automath/autParser.cmx -common/hierarchy.cmi: -common/hierarchy.cmo: lib/cps.cmx common/hierarchy.cmi -common/hierarchy.cmx: lib/cps.cmx common/hierarchy.cmi -common/output.cmi: -common/output.cmo: lib/log.cmi common/output.cmi -common/output.cmx: lib/log.cmx common/output.cmi -common/entity.cmo: lib/nUri.cmi automath/aut.cmx -common/entity.cmx: lib/nUri.cmx automath/aut.cmx -common/library.cmi: common/entity.cmx -common/library.cmo: lib/nUri.cmi common/hierarchy.cmi common/entity.cmx \ - lib/cps.cmx common/library.cmi -common/library.cmx: lib/nUri.cmx common/hierarchy.cmx common/entity.cmx \ - lib/cps.cmx common/library.cmi +automath/autLexer.cmo: common/options.cmx lib/log.cmi automath/autParser.cmi +automath/autLexer.cmx: common/options.cmx lib/log.cmx automath/autParser.cmx basic_ag/bag.cmo: lib/log.cmi common/entity.cmx lib/cps.cmx basic_ag/bag.cmx: lib/log.cmx common/entity.cmx lib/cps.cmx basic_ag/bagOutput.cmi: lib/log.cmi basic_ag/bag.cmx -basic_ag/bagOutput.cmo: common/output.cmi lib/nUri.cmi lib/log.cmi \ +basic_ag/bagOutput.cmo: common/options.cmx lib/nUri.cmi lib/log.cmi \ common/hierarchy.cmi common/entity.cmx basic_ag/bag.cmx \ basic_ag/bagOutput.cmi -basic_ag/bagOutput.cmx: common/output.cmx lib/nUri.cmx lib/log.cmx \ +basic_ag/bagOutput.cmx: common/options.cmx lib/nUri.cmx lib/log.cmx \ common/hierarchy.cmx common/entity.cmx basic_ag/bag.cmx \ basic_ag/bagOutput.cmi basic_ag/bagEnvironment.cmi: basic_ag/bag.cmx @@ -93,10 +95,10 @@ basic_ag/bagUntrusted.cmx: lib/nUri.cmx lib/log.cmx common/entity.cmx \ basic_rg/brg.cmo: common/entity.cmx basic_rg/brg.cmx: common/entity.cmx basic_rg/brgOutput.cmi: lib/log.cmi common/library.cmi basic_rg/brg.cmx -basic_rg/brgOutput.cmo: common/output.cmi lib/nUri.cmi lib/log.cmi \ +basic_rg/brgOutput.cmo: common/options.cmx lib/nUri.cmi lib/log.cmi \ common/library.cmi common/hierarchy.cmi common/entity.cmx lib/cps.cmx \ basic_rg/brg.cmx basic_rg/brgOutput.cmi -basic_rg/brgOutput.cmx: common/output.cmx lib/nUri.cmx lib/log.cmx \ +basic_rg/brgOutput.cmx: common/options.cmx lib/nUri.cmx lib/log.cmx \ common/library.cmx common/hierarchy.cmx common/entity.cmx lib/cps.cmx \ basic_rg/brg.cmx basic_rg/brgOutput.cmi basic_rg/brgEnvironment.cmi: basic_rg/brg.cmx @@ -143,19 +145,18 @@ complete_rg/crgOutput.cmo: lib/nUri.cmi common/library.cmi \ complete_rg/crgOutput.cmx: lib/nUri.cmx common/library.cmx \ common/hierarchy.cmx common/entity.cmx complete_rg/crg.cmx lib/cps.cmx \ complete_rg/crgOutput.cmi -complete_rg/crgTxt.cmi: text/txt.cmx common/entity.cmx complete_rg/crg.cmx -complete_rg/crgTxt.cmo: text/txtTxt.cmi text/txt.cmx lib/nUri.cmi \ - common/hierarchy.cmi common/entity.cmx complete_rg/crg.cmx lib/cps.cmx \ - complete_rg/crgTxt.cmi -complete_rg/crgTxt.cmx: text/txtTxt.cmx text/txt.cmx lib/nUri.cmx \ - common/hierarchy.cmx common/entity.cmx complete_rg/crg.cmx lib/cps.cmx \ - complete_rg/crgTxt.cmi -complete_rg/crgAut.cmi: common/entity.cmx complete_rg/crg.cmx \ - automath/aut.cmx -complete_rg/crgAut.cmo: lib/nUri.cmi common/entity.cmx complete_rg/crg.cmx \ - lib/cps.cmx automath/aut.cmx complete_rg/crgAut.cmi -complete_rg/crgAut.cmx: lib/nUri.cmx common/entity.cmx complete_rg/crg.cmx \ - lib/cps.cmx automath/aut.cmx complete_rg/crgAut.cmi +complete_rg/crgTxt.cmi: text/txt.cmx complete_rg/crg.cmx +complete_rg/crgTxt.cmo: text/txtTxt.cmi text/txt.cmx common/options.cmx \ + lib/nUri.cmi common/hierarchy.cmi common/entity.cmx complete_rg/crg.cmx \ + lib/cps.cmx complete_rg/crgTxt.cmi +complete_rg/crgTxt.cmx: text/txtTxt.cmx text/txt.cmx common/options.cmx \ + lib/nUri.cmx common/hierarchy.cmx common/entity.cmx complete_rg/crg.cmx \ + lib/cps.cmx complete_rg/crgTxt.cmi +complete_rg/crgAut.cmi: complete_rg/crg.cmx automath/aut.cmx +complete_rg/crgAut.cmo: common/options.cmx lib/nUri.cmi common/entity.cmx \ + complete_rg/crg.cmx lib/cps.cmx automath/aut.cmx complete_rg/crgAut.cmi +complete_rg/crgAut.cmx: common/options.cmx lib/nUri.cmx common/entity.cmx \ + complete_rg/crg.cmx lib/cps.cmx automath/aut.cmx complete_rg/crgAut.cmi complete_rg/crgBrg.cmi: complete_rg/crg.cmx basic_rg/brg.cmx complete_rg/crgBrg.cmo: common/entity.cmx complete_rg/crg.cmx lib/cps.cmx \ basic_rg/brg.cmx complete_rg/crgBrg.cmi @@ -172,10 +173,10 @@ toplevel/metaLibrary.cmi: toplevel/meta.cmx toplevel/metaLibrary.cmo: toplevel/metaOutput.cmi toplevel/metaLibrary.cmi toplevel/metaLibrary.cmx: toplevel/metaOutput.cmx toplevel/metaLibrary.cmi toplevel/metaAut.cmi: toplevel/meta.cmx automath/aut.cmx -toplevel/metaAut.cmo: lib/nUri.cmi toplevel/meta.cmx common/entity.cmx \ - lib/cps.cmx automath/aut.cmx toplevel/metaAut.cmi -toplevel/metaAut.cmx: lib/nUri.cmx toplevel/meta.cmx common/entity.cmx \ - lib/cps.cmx automath/aut.cmx toplevel/metaAut.cmi +toplevel/metaAut.cmo: common/options.cmx lib/nUri.cmi toplevel/meta.cmx \ + common/entity.cmx lib/cps.cmx automath/aut.cmx toplevel/metaAut.cmi +toplevel/metaAut.cmx: common/options.cmx lib/nUri.cmx toplevel/meta.cmx \ + common/entity.cmx lib/cps.cmx automath/aut.cmx toplevel/metaAut.cmi toplevel/metaBag.cmi: toplevel/meta.cmx basic_ag/bag.cmx toplevel/metaBag.cmo: toplevel/meta.cmx lib/cps.cmx basic_ag/bag.cmx \ toplevel/metaBag.cmi @@ -187,24 +188,26 @@ toplevel/metaBrg.cmo: toplevel/meta.cmx common/entity.cmx lib/cps.cmx \ toplevel/metaBrg.cmx: toplevel/meta.cmx common/entity.cmx lib/cps.cmx \ basic_rg/brg.cmx toplevel/metaBrg.cmi toplevel/top.cmo: text/txtParser.cmi text/txtLexer.cmx text/txt.cmx \ - lib/time.cmx common/output.cmi lib/nUri.cmi toplevel/metaOutput.cmi \ - toplevel/metaLibrary.cmi toplevel/metaBrg.cmi toplevel/metaBag.cmi \ - toplevel/metaAut.cmi toplevel/meta.cmx lib/log.cmi common/library.cmi \ - common/hierarchy.cmi common/entity.cmx complete_rg/crgTxt.cmi \ - complete_rg/crgOutput.cmi complete_rg/crgBrg.cmi complete_rg/crgAut.cmi \ - complete_rg/crg.cmx lib/cps.cmx basic_rg/brgUntrusted.cmi \ - basic_rg/brgReduction.cmi basic_rg/brgOutput.cmi basic_rg/brg.cmx \ - basic_ag/bagUntrusted.cmi basic_ag/bagType.cmi basic_ag/bagOutput.cmi \ - basic_ag/bag.cmx automath/autProcess.cmi automath/autParser.cmi \ - automath/autOutput.cmi automath/autLexer.cmx automath/aut.cmx + lib/time.cmx common/output.cmi common/options.cmx lib/nUri.cmi \ + toplevel/metaOutput.cmi toplevel/metaLibrary.cmi toplevel/metaBrg.cmi \ + toplevel/metaBag.cmi toplevel/metaAut.cmi toplevel/meta.cmx lib/log.cmi \ + common/library.cmi common/hierarchy.cmi common/entity.cmx \ + complete_rg/crgTxt.cmi complete_rg/crgOutput.cmi complete_rg/crgBrg.cmi \ + complete_rg/crgAut.cmi complete_rg/crg.cmx lib/cps.cmx \ + basic_rg/brgUntrusted.cmi basic_rg/brgReduction.cmi \ + basic_rg/brgOutput.cmi basic_rg/brg.cmx basic_ag/bagUntrusted.cmi \ + basic_ag/bagType.cmi basic_ag/bagOutput.cmi basic_ag/bag.cmx \ + automath/autProcess.cmi automath/autParser.cmi automath/autOutput.cmi \ + automath/autLexer.cmx automath/aut.cmx toplevel/top.cmx: text/txtParser.cmx text/txtLexer.cmx text/txt.cmx \ - lib/time.cmx common/output.cmx lib/nUri.cmx toplevel/metaOutput.cmx \ - toplevel/metaLibrary.cmx toplevel/metaBrg.cmx toplevel/metaBag.cmx \ - toplevel/metaAut.cmx toplevel/meta.cmx lib/log.cmx common/library.cmx \ - common/hierarchy.cmx common/entity.cmx complete_rg/crgTxt.cmx \ - complete_rg/crgOutput.cmx complete_rg/crgBrg.cmx complete_rg/crgAut.cmx \ - complete_rg/crg.cmx lib/cps.cmx basic_rg/brgUntrusted.cmx \ - basic_rg/brgReduction.cmx basic_rg/brgOutput.cmx basic_rg/brg.cmx \ - basic_ag/bagUntrusted.cmx basic_ag/bagType.cmx basic_ag/bagOutput.cmx \ - basic_ag/bag.cmx automath/autProcess.cmx automath/autParser.cmx \ - automath/autOutput.cmx automath/autLexer.cmx automath/aut.cmx + lib/time.cmx common/output.cmx common/options.cmx lib/nUri.cmx \ + toplevel/metaOutput.cmx toplevel/metaLibrary.cmx toplevel/metaBrg.cmx \ + toplevel/metaBag.cmx toplevel/metaAut.cmx toplevel/meta.cmx lib/log.cmx \ + common/library.cmx common/hierarchy.cmx common/entity.cmx \ + complete_rg/crgTxt.cmx complete_rg/crgOutput.cmx complete_rg/crgBrg.cmx \ + complete_rg/crgAut.cmx complete_rg/crg.cmx lib/cps.cmx \ + basic_rg/brgUntrusted.cmx basic_rg/brgReduction.cmx \ + basic_rg/brgOutput.cmx basic_rg/brg.cmx basic_ag/bagUntrusted.cmx \ + basic_ag/bagType.cmx basic_ag/bagOutput.cmx basic_ag/bag.cmx \ + automath/autProcess.cmx automath/autParser.cmx automath/autOutput.cmx \ + automath/autLexer.cmx automath/aut.cmx diff --git a/helm/software/lambda-delta/Make b/helm/software/lambda-delta/Make index ed00c8bbc..8e332c33b 100644 --- a/helm/software/lambda-delta/Make +++ b/helm/software/lambda-delta/Make @@ -1 +1 @@ -lib text automath common basic_ag basic_rg complete_rg toplevel +lib common text automath basic_ag basic_rg complete_rg toplevel diff --git a/helm/software/lambda-delta/Makefile b/helm/software/lambda-delta/Makefile index cb895593f..aeb161c90 100644 --- a/helm/software/lambda-delta/Makefile +++ b/helm/software/lambda-delta/Makefile @@ -6,7 +6,7 @@ KEEP = README automath/*.aut CLEAN = etc/log.txt -TAGS = test-si test-si-fast hal xml-si-drg xml-si profile +TAGS = test-si test-si-fast hal xml-si-crg xml-si profile XMLS = xml/brg-si/grundlagen/l/not.ld.xml \ xml/brg-si/grundlagen/l/et.ld.xml \ @@ -38,7 +38,7 @@ xml-si: $(MAIN).opt @echo " HELENA -u -x -s 2 $(INPUT)" $(H)./$(MAIN).opt -u -x -s 2 -S 1 $(INPUT) > etc/log.txt -xml-si-drg: $(MAIN).opt +xml-si-crg: $(MAIN).opt @echo " HELENA -u -x -s 1 $(INPUT)" $(H)./$(MAIN).opt -u -x -s 1 -S 1 $(INPUT) > etc/log.txt diff --git a/helm/software/lambda-delta/automath/autLexer.mll b/helm/software/lambda-delta/automath/autLexer.mll index b7009f924..51f1e7cb9 100644 --- a/helm/software/lambda-delta/automath/autLexer.mll +++ b/helm/software/lambda-delta/automath/autLexer.mll @@ -11,13 +11,12 @@ { module L = Log + module O = Options module P = AutParser let debug = false let out s = if debug then L.warn s else () - let unquote = ref false - (* This turns an Automath identifier into an XML nmtoken *) let quote id = let l = String.length id in @@ -69,7 +68,7 @@ and token = parse | "'type'" { out "TYPE"; P.TYPE } | ID { out "ID"; let s = Lexing.lexeme lexbuf in - if !unquote then P.IDENT s else P.IDENT (quote s) + if !O.unquote then P.IDENT s else P.IDENT (quote s) } | ":=" { out "DEF"; P.DEF } | "(" { out "OP"; P.OP } diff --git a/helm/software/lambda-delta/automath/autProcess.ml b/helm/software/lambda-delta/automath/autProcess.ml index b9751b2f5..405952ff5 100644 --- a/helm/software/lambda-delta/automath/autProcess.ml +++ b/helm/software/lambda-delta/automath/autProcess.ml @@ -66,7 +66,7 @@ let proc_command f st command = match command with (* interface functions ******************************************************) -let initial_status = { +let initial_status () = { opening = false; reopening = false; closing = false; explicit = false; block = false; iao = 0; iar = 0; iac = 0; iag = 0 diff --git a/helm/software/lambda-delta/automath/autProcess.mli b/helm/software/lambda-delta/automath/autProcess.mli index 91280101a..4145ff946 100644 --- a/helm/software/lambda-delta/automath/autProcess.mli +++ b/helm/software/lambda-delta/automath/autProcess.mli @@ -11,7 +11,7 @@ type status -val initial_status: status +val initial_status: unit -> status val process_command: (status -> Aut.command -> 'a) -> status -> Aut.command -> 'a diff --git a/helm/software/lambda-delta/basic_ag/bagOutput.ml b/helm/software/lambda-delta/basic_ag/bagOutput.ml index 829ee82f8..0bfc13ee6 100644 --- a/helm/software/lambda-delta/basic_ag/bagOutput.ml +++ b/helm/software/lambda-delta/basic_ag/bagOutput.ml @@ -13,9 +13,9 @@ module P = Printf module F = Format module U = NUri module L = Log +module O = Options module Y = Entity module H = Hierarchy -module O = Output module B = Bag type counters = { diff --git a/helm/software/lambda-delta/basic_rg/brgOutput.ml b/helm/software/lambda-delta/basic_rg/brgOutput.ml index 124f98974..186349a1c 100644 --- a/helm/software/lambda-delta/basic_rg/brgOutput.ml +++ b/helm/software/lambda-delta/basic_rg/brgOutput.ml @@ -14,10 +14,10 @@ module F = Format module C = Cps module U = NUri module L = Log +module O = Options module Y = Entity module X = Library module H = Hierarchy -module O = Output module B = Brg (* nodes count **************************************************************) diff --git a/helm/software/lambda-delta/common/Make b/helm/software/lambda-delta/common/Make index 8085aa65b..1ec685637 100644 --- a/helm/software/lambda-delta/common/Make +++ b/helm/software/lambda-delta/common/Make @@ -1 +1 @@ -hierarchy output entity library +options hierarchy output entity library diff --git a/helm/software/lambda-delta/common/entity.ml b/helm/software/lambda-delta/common/entity.ml index d0e049d23..de06f2924 100644 --- a/helm/software/lambda-delta/common/entity.ml +++ b/helm/software/lambda-delta/common/entity.ml @@ -9,6 +9,8 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) +module O = Options + type uri = NUri.uri type id = Aut.id @@ -26,8 +28,6 @@ type 'term bind = Abst of 'term (* declaration: domain *) type 'term entity = attrs * uri * 'term bind (* attrs, name, binder *) -type uri_generator = string -> string - type status = { delta: bool; (* global delta-expansion *) rt: bool; (* reference typing *) @@ -104,6 +104,10 @@ let xlate f xlate_term = function | _, _, Void -> assert false -let initial_status expand si = { - delta = false; rt = false; si = si; expand = expand +let initial_status () = { + delta = false; rt = false; si = !O.si; expand = !O.expand +} + +let refresh_status st = {st with + si = !O.si; expand = !O.expand } diff --git a/helm/software/lambda-delta/common/hierarchy.ml b/helm/software/lambda-delta/common/hierarchy.ml index 23c8109bf..b7d428353 100644 --- a/helm/software/lambda-delta/common/hierarchy.ml +++ b/helm/software/lambda-delta/common/hierarchy.ml @@ -59,3 +59,6 @@ let set_graph s = let err () = false in let f g = graph := g; true in graph_of_string err f s + +let clear () = + H.clear sort; graph := graph_of_string C.err C.start default_graph diff --git a/helm/software/lambda-delta/common/hierarchy.mli b/helm/software/lambda-delta/common/hierarchy.mli index a0bd1862e..04feaf929 100644 --- a/helm/software/lambda-delta/common/hierarchy.mli +++ b/helm/software/lambda-delta/common/hierarchy.mli @@ -20,3 +20,5 @@ val set_graph: string -> bool val string_of_graph: unit -> string val apply: int -> int + +val clear: unit -> unit diff --git a/helm/software/lambda-delta/common/options.ml b/helm/software/lambda-delta/common/options.ml new file mode 100644 index 000000000..53693174b --- /dev/null +++ b/helm/software/lambda-delta/common/options.ml @@ -0,0 +1,37 @@ +(* + ||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 C = Cps + +type uri_generator = string -> string + +(* interface functions ******************************************************) + +let indexes = ref false (* show de Bruijn indexes *) + +let expand = ref false (* always expand global definitions *) + +let si = ref false (* use sort inclusion *) + +let unquote = ref false (* do not quote identifiers when lexing *) + +let icm = ref 0 (* complexity measure of relocated terms *) + +let cover = ref "" (* initial uri segment *) + +let mk_uri = ref (fun _ _ -> C.err : bool -> string -> uri_generator) + +let get_mk_uri () = + !mk_uri !si !cover + +let clear () = + expand := false; si := false; cover := ""; indexes := false; icm := 0; + mk_uri := fun _ _ -> C.err diff --git a/helm/software/lambda-delta/common/output.ml b/helm/software/lambda-delta/common/output.ml index c2e43d460..8270c5d97 100644 --- a/helm/software/lambda-delta/common/output.ml +++ b/helm/software/lambda-delta/common/output.ml @@ -11,8 +11,7 @@ module P = Printf module L = Log - -let icm = ref 0 +module O = Options type reductions = { beta : int; @@ -70,6 +69,4 @@ let print_reductions () = L.warn (P.sprintf " Local: %7u" r.lrt); L.warn (P.sprintf " Global: %7u" r.grt); L.warn (P.sprintf " Sort inclusion: %7u" r.si); - L.warn (P.sprintf " Relocated nodes (icm): %7u" !icm) - -let indexes = ref false + L.warn (P.sprintf " Relocated nodes (icm): %7u" !O.icm) diff --git a/helm/software/lambda-delta/common/output.mli b/helm/software/lambda-delta/common/output.mli index 679346a19..20b83f0fc 100644 --- a/helm/software/lambda-delta/common/output.mli +++ b/helm/software/lambda-delta/common/output.mli @@ -9,10 +9,6 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) -val indexes: bool ref - -val icm: int ref - val clear_reductions: unit -> unit val add: diff --git a/helm/software/lambda-delta/complete_rg/crgAut.ml b/helm/software/lambda-delta/complete_rg/crgAut.ml index 8420cbea7..0b95adf41 100644 --- a/helm/software/lambda-delta/complete_rg/crgAut.ml +++ b/helm/software/lambda-delta/complete_rg/crgAut.ml @@ -12,6 +12,7 @@ module U = NUri module H = U.UriHash module C = Cps +module O = Options module Y = Entity module A = Aut module D = Crg @@ -28,7 +29,7 @@ type status = { node: context_node; (* current context node *) nodes: context_node list; (* context node list *) line: int; (* line number *) - mk_uri:Y.uri_generator (* uri generator *) + mk_uri:O.uri_generator (* uri generator *) } type resolver = Local of int @@ -42,11 +43,6 @@ let hcnt = H.create hcnt_size (* optimized context *) (* Internal functions *******************************************************) -let initial_status mk_uri = - H.clear henv; H.clear hcnt; { - path = []; node = None; nodes = []; line = 1; mk_uri = mk_uri -} - let empty_cnt = [], [] let add_abst (a, ws) id w = @@ -216,7 +212,13 @@ let xlate_entity err f st = function (* Interface functions ******************************************************) -let initial_status mk_uri = - initial_status mk_uri +let initial_status () = + H.clear henv; H.clear hcnt; { + path = []; node = None; nodes = []; line = 1; mk_uri = O.get_mk_uri () +} + +let refresh_status st = {st with + mk_uri = O.get_mk_uri () +} let crg_of_aut = xlate_entity diff --git a/helm/software/lambda-delta/complete_rg/crgAut.mli b/helm/software/lambda-delta/complete_rg/crgAut.mli index b48145d0f..c7d93d3ce 100644 --- a/helm/software/lambda-delta/complete_rg/crgAut.mli +++ b/helm/software/lambda-delta/complete_rg/crgAut.mli @@ -11,7 +11,9 @@ type status -val initial_status: Entity.uri_generator -> status +val initial_status: unit -> status + +val refresh_status: status -> status val crg_of_aut: (status -> 'a) -> (status -> Crg.entity -> 'a) -> status -> Aut.command -> 'a diff --git a/helm/software/lambda-delta/complete_rg/crgTxt.ml b/helm/software/lambda-delta/complete_rg/crgTxt.ml index 267ef384f..8089c79e2 100644 --- a/helm/software/lambda-delta/complete_rg/crgTxt.ml +++ b/helm/software/lambda-delta/complete_rg/crgTxt.ml @@ -12,16 +12,17 @@ module U = NUri module H = Hierarchy module C = Cps +module O = Options module Y = Entity module T = Txt module TT = TxtTxt module D = Crg type status = { - path: T.id list; (* current section path *) - line: int; (* line number *) - sort: int; (* first default sort index *) - mk_uri:Y.uri_generator (* uri generator *) + path : T.id list; (* current section path *) + line : int; (* line number *) + sort : int; (* first default sort index *) + mk_uri: O.uri_generator (* uri generator *) } let henv_size = 7000 (* hash tables initial size *) @@ -30,10 +31,6 @@ let henv = Hashtbl.create henv_size (* optimized global environment *) (* Internal functions *******************************************************) -let initial_status mk_uri = { - path = []; line = 1; sort = 0; mk_uri = mk_uri -} - let name_of_id ?(r=true) id = Y.Name (id, r) let mk_lref f i j k = f (D.TLRef ([Y.Apix k], i, j)) @@ -114,14 +111,10 @@ let mk_contents tt = function | T.Th -> [], Y.Abbr tt let xlate_entity err f st = function - | T.Section (Some name) -> - err {st with path = name :: st.path} - | T.Section None -> - begin match st.path with - | _ :: ptl -> - err {st with path = ptl} - | _ -> assert false - end + | T.Require _ -> + err st + | T.Graph id -> + assert (H.set_graph id); err st | T.Sorts sorts -> let map st (xix, s) = let ix = match xix with @@ -131,8 +124,14 @@ let xlate_entity err f st = function {st with sort = H.set_sorts ix [s]} in err (List.fold_left map st sorts) - | T.Graph id -> - assert (H.set_graph id); err st + | T.Section (Some name) -> + err {st with path = name :: st.path} + | T.Section None -> + begin match st.path with + | _ :: ptl -> + err {st with path = ptl} + | _ -> assert false + end | T.Entity (kind, id, meta, t) -> let uri = uri_of_id st id st.path in Hashtbl.add henv id uri; @@ -147,7 +146,13 @@ let xlate_entity err f st = function (* Interface functions ******************************************************) -let initial_status mk_uri = - initial_status mk_uri +let initial_status () = + Hashtbl.clear henv; { + path = []; line = 1; sort = 0; mk_uri = O.get_mk_uri () +} + +let refresh_status st = {st with + mk_uri = O.get_mk_uri () +} let crg_of_txt = xlate_entity diff --git a/helm/software/lambda-delta/complete_rg/crgTxt.mli b/helm/software/lambda-delta/complete_rg/crgTxt.mli index 5edaabedd..90105b57f 100644 --- a/helm/software/lambda-delta/complete_rg/crgTxt.mli +++ b/helm/software/lambda-delta/complete_rg/crgTxt.mli @@ -11,7 +11,9 @@ type status -val initial_status: Entity.uri_generator -> status +val initial_status: unit -> status + +val refresh_status: status -> status val crg_of_txt: (status -> 'a) -> (status -> Crg.entity -> 'a) -> status -> Txt.command -> 'a diff --git a/helm/software/lambda-delta/examples/exp_math/L.hln b/helm/software/lambda-delta/examples/exp_math/L.hln index fbcf44adf..28f3bff23 100644 --- a/helm/software/lambda-delta/examples/exp_math/L.hln +++ b/helm/software/lambda-delta/examples/exp_math/L.hln @@ -1,8 +1,8 @@ -\graph Z3 +\require preamble -\sorts Prop, Set, Term +\* Intuitionistic Predicate Logic with Equality *\ -\open syntax \* [1] 2.1. *\ +\open elements \* [1] 2.1. 2.2. *\ \decl "logical false" False: *Prop @@ -10,34 +10,31 @@ \decl "logical disjunction" Or: *Prop => *Prop -> *Prop - \decl "logical implication" Imp: *Prop => *Prop -> *Prop +\* implication and non-dependent abstraction are isomorphic *\ + \def "logical implication" + Imp = [p:*Prop, q:*Prop] p -> q : *Prop => *Prop -> *Prop - \decl "logical comprehension" All: [~:*Set->*Prop] *Prop + \decl "logical comprehension" All: (*Obj -> *Prop) -> *Prop - \decl "logical existence" Ex: [~:*Set->*Prop] *Prop + \decl "logical existence" Ex: (*Obj -> *Prop) -> *Prop - \decl "syntactical identity" Id: *Set => *Set -> *Prop - - \decl "rule application" App: *Set => *Set => *Set -> *Prop - - \decl "classification predicate" Cl: *Set -> *Prop - - \decl "classification membership" Eta: *Set => *Set -> *Prop - - \decl "object-to-term-coercion" T: *Set -> *Term - - \decl "term application" At: *Term => *Term -> *Term - - \decl "term-object equivalence" E: *Term => *Set -> *Prop + \decl "syntactical identity" Id: *Obj => *Obj -> *Prop \close -\open non_logical_axioms +\open abbreviations \* [1] 2.3. *\ + + \def "logical negation" + Not = [p:*Prop] p -> False : *Prop -> *Prop - \ax e_refl: [x:*Set] E(T(x), x) + \def "logical equivalence" + Iff = [p:*Prop, q:*Prop] And(p -> q, q -> p) : *Prop => *Prop -> *Prop - \ax e_at_in: [f:*Set][x:*Set][y:*Set] App(f,x,y) -> E(At(T(f), T(x)), y) + \def "logical strict existence" + EX = [p:*Obj->*Prop] Ex([x:*Obj] And(p(x), [y:*Obj] p(y) -> Id(x, y))) + : (*Obj -> *Prop) -> *Prop - \ax e_at_out: [f:*Set][x:*Set][y:*Set] E(At(T(f), T(x)), y) -> App(f,x,y) + \def "negated syntactical identity" + NId = [x:*Obj, y:*Obj] Not(Id(x, y)) : *Obj => *Obj -> *Prop \close diff --git a/helm/software/lambda-delta/examples/exp_math/Make b/helm/software/lambda-delta/examples/exp_math/Make index f1f020178..138243141 100644 --- a/helm/software/lambda-delta/examples/exp_math/Make +++ b/helm/software/lambda-delta/examples/exp_math/Make @@ -1 +1 @@ -L.hln +preamble.hln L.hln T0.hln diff --git a/helm/software/lambda-delta/examples/exp_math/Makefile b/helm/software/lambda-delta/examples/exp_math/Makefile index ffc3343a0..93ea22279 100644 --- a/helm/software/lambda-delta/examples/exp_math/Makefile +++ b/helm/software/lambda-delta/examples/exp_math/Makefile @@ -8,11 +8,11 @@ HLNS = $(shell cat Make) all: $(HLNS) @echo " HELENA -r $(ROOT)" - $(H)$(HELENA) -r $(ROOT) $^ + $(H)$(HELENA) -r $(ROOT) -u $^ progress: $(HLNS) @echo " HELENA -r $(ROOT) -j" - $(H)$(HELENA) -r $(ROOT) -j $^ + $(H)$(HELENA) -r $(ROOT) -j -u $^ xml: $(HLNS) @echo " HELENA -r $(ROOT) -x" diff --git a/helm/software/lambda-delta/examples/exp_math/T0.hln b/helm/software/lambda-delta/examples/exp_math/T0.hln new file mode 100644 index 000000000..a1366dc7d --- /dev/null +++ b/helm/software/lambda-delta/examples/exp_math/T0.hln @@ -0,0 +1,35 @@ +\require L + +\* Feferman's system T0 *\ + +\open elements \* [1] 2.1. 2.2. 2.4. *\ + + \decl "rule application" App: *Obj => *Obj => *Obj -> *Prop + + \decl "classification predicate" Cl: *Obj -> *Prop + + \decl "classification membership" Eta: *Obj => *Obj -> *Prop + +\* we must make an explicit coercion from *Obj to *Term *\ + \decl "object-to-term-coercion" T: *Obj -> *Term + + \decl "term application" At: *Term => *Term -> *Term + + \decl "term-object equivalence" E: *Term => *Obj -> *Prop + +\close + +\open logical_abbreviations \* [1] 2.3. *\ + +\close + +\open non_logical_axioms \* [1] 2.4. *\ + +\* we axiomatize E because *Term is not inductively generated *\ + \ax e_refl: [y:*Obj] E(T(y), y) +\* + \ax e_at_in: [f:*Obj][x:*Obj][y:*Obj] App(f,x,y) -> E(At(T(f), T(x)), y) + + \ax e_at_out: [f:*Obj][x:*Obj][y:*Obj] E(At(T(f), T(x)), y) -> App(f,x,y) +*\ +\close diff --git a/helm/software/lambda-delta/examples/exp_math/preamble.hln b/helm/software/lambda-delta/examples/exp_math/preamble.hln new file mode 100644 index 000000000..7d80ba4fa --- /dev/null +++ b/helm/software/lambda-delta/examples/exp_math/preamble.hln @@ -0,0 +1,8 @@ +\* Systematic Explicit Mathematics *\ +\* [1] F. Feferman: *\ + +\* Development started: 2010 Feb 20 *\ + +\graph Z3 + +\sorts Prop, Obj, Term diff --git a/helm/software/lambda-delta/lib/log.ml b/helm/software/lambda-delta/lib/log.ml index 3b93ccedb..03e7b5b95 100644 --- a/helm/software/lambda-delta/lib/log.ml +++ b/helm/software/lambda-delta/lib/log.ml @@ -32,6 +32,9 @@ let loc = ref "unknown location" (* Internal functions *******************************************************) +let clear () = + level := 0; loc := "unknown location" + let std = F.std_formatter let err = F.err_formatter diff --git a/helm/software/lambda-delta/lib/log.mli b/helm/software/lambda-delta/lib/log.mli index 956f91fd8..9e0f054e1 100644 --- a/helm/software/lambda-delta/lib/log.mli +++ b/helm/software/lambda-delta/lib/log.mli @@ -26,6 +26,8 @@ val loc: string ref val level: int ref +val clear: unit -> unit + val warn: string -> unit val box: int -> unit diff --git a/helm/software/lambda-delta/text/txt.ml b/helm/software/lambda-delta/text/txt.ml index 81c210852..ca32a9150 100644 --- a/helm/software/lambda-delta/text/txt.ml +++ b/helm/software/lambda-delta/text/txt.ml @@ -34,7 +34,8 @@ and term = Sort of ix (* level *) | Inst of term * term list (* function, arguments *) | Impl of bool * id * term * term (* strong?, label, source, target *) -type command = Graph of id (* hierarchy graph: name *) +type command = Require of id list (* required files: names *) + | Graph of id (* hierarchy graph: name *) | Sorts of (int option * id) list (* sorts: index, name *) | Section of id option (* section: Some id = open, None = close last *) | Entity of kind * id * desc * term (* entity: class, name, description, contents *) diff --git a/helm/software/lambda-delta/text/txtLexer.mll b/helm/software/lambda-delta/text/txtLexer.mll index fc00064e5..d42629713 100644 --- a/helm/software/lambda-delta/text/txtLexer.mll +++ b/helm/software/lambda-delta/text/txtLexer.mll @@ -38,33 +38,34 @@ and qstring = parse | BS QT { "\"" ^ qstring lexbuf } | _ { Lexing.lexeme lexbuf ^ qstring lexbuf } and token = parse - | SPC { token lexbuf } - | OC { block_comment lexbuf; token lexbuf } - | ID as id { out "ID"; P.ID id } - | IX as ix { out "IX"; P.IX (int_of_string ix) } - | QT { let s = qstring lexbuf in out "STR"; P.STR s } - | "\\graph" { out "GRAPH"; P.GRAPH } - | "\\decl" { out "DECL"; P.DECL } - | "\\ax" { out "AX"; P.AX } - | "\\def" { out "DEF"; P.DEF } - | "\\th" { out "TH"; P.TH } - | "\\open" { out "OPEN"; P.OPEN } - | "\\close" { out "CLOSE"; P.CLOSE } - | "\\sorts" { out "SORTS"; P.SORTS } - | "(" { out "OP"; P.OP } - | ")" { out "CP"; P.CP } - | "[" { out "OB"; P.OB } - | "]" { out "CB"; P.CB } - | "<" { out "OA"; P.OA } - | ">" { out "CA"; P.CA } - | "." { out "FS"; P.FS } - | ":" { out "CN"; P.CN } - | "," { out "CM"; P.CM } - | "=" { out "EQ"; P.EQ } - | "*" { out "STAR"; P.STAR } - | "#" { out "HASH"; P.HASH } - | "+" { out "PLUS"; P.PLUS } - | "~" { out "TE"; P.TE } - | "->" { out "WTO"; P.WTO } - | "=>" { out "STO"; P.STO } - | eof { out "EOF"; P.EOF } + | SPC { token lexbuf } + | OC { block_comment lexbuf; token lexbuf } + | ID as id { out "ID"; P.ID id } + | IX as ix { out "IX"; P.IX (int_of_string ix) } + | QT { let s = qstring lexbuf in out "STR"; P.STR s } + | "\\require" { out "REQUIRE"; P.REQUIRE } + | "\\graph" { out "GRAPH"; P.GRAPH } + | "\\decl" { out "DECL"; P.DECL } + | "\\ax" { out "AX"; P.AX } + | "\\def" { out "DEF"; P.DEF } + | "\\th" { out "TH"; P.TH } + | "\\open" { out "OPEN"; P.OPEN } + | "\\close" { out "CLOSE"; P.CLOSE } + | "\\sorts" { out "SORTS"; P.SORTS } + | "(" { out "OP"; P.OP } + | ")" { out "CP"; P.CP } + | "[" { out "OB"; P.OB } + | "]" { out "CB"; P.CB } + | "<" { out "OA"; P.OA } + | ">" { out "CA"; P.CA } + | "." { out "FS"; P.FS } + | ":" { out "CN"; P.CN } + | "," { out "CM"; P.CM } + | "=" { out "EQ"; P.EQ } + | "*" { out "STAR"; P.STAR } + | "#" { out "HASH"; P.HASH } + | "+" { out "PLUS"; P.PLUS } + | "~" { out "TE"; P.TE } + | "->" { out "WTO"; P.WTO } + | "=>" { out "STO"; P.STO } + | eof { out "EOF"; P.EOF } diff --git a/helm/software/lambda-delta/text/txtParser.mly b/helm/software/lambda-delta/text/txtParser.mly index ee995aa2d..05af001e7 100644 --- a/helm/software/lambda-delta/text/txtParser.mly +++ b/helm/software/lambda-delta/text/txtParser.mly @@ -33,12 +33,12 @@ %token IX %token ID STR %token OP CP OB CB OA CA FS CN CM EQ STAR HASH PLUS TE WTO STO - %token GRAPH DECL AX DEF TH OPEN CLOSE SORTS EOF + %token REQUIRE GRAPH DECL AX DEF TH OPEN CLOSE SORTS EOF %start entry %type entry - %nonassoc CP CB CA + %nonassoc CP CB CA %right WTO STO %% hash: @@ -67,9 +67,9 @@ ; abst: - | ID CN term { $1, true, $3 } - | TE CN term { "", false, $3 } - | TE ID CN term { $2, false, $4 } + | ID CN term { $1, true, $3 } + | TE term { "", false, $2 } + | ID TE term { $1, false, $3 } ; abbr: | ID EQ term { $1, $3 } @@ -88,27 +88,29 @@ | ids { T.Void $1 } ; atom: - | STAR IX { T.Sort $2 } - | STAR ID { T.NSrt $2 } - | hash IX { T.LRef ($2, 0) } - | hash IX PLUS IX { T.LRef ($2, $4) } - | hash ID { T.NRef $2 } + | STAR IX { T.Sort $2 } + | STAR ID { T.NSrt $2 } + | hash IX { T.LRef ($2, 0) } + | hash IX PLUS IX { T.LRef ($2, $4) } + | ID { T.NRef $1 } + | HASH ID { T.NRef $2 } + | atom OP term CP { T.Inst ($1, [$3]) } + | atom OP terms CP { T.Inst ($1, $3) } ; term: - | atom { $1 } - | OA term CA fs term { T.Cast ($2, $5) } - | OP terms CP fs term { T.Appl ($2, $5) } - | atom OP terms CP { T.Inst ($1, $3) } - | OB binder CB fs term { T.Bind ($2, $5) } - | term WTO term { T.Impl (false, "", $1, $3) } - | TE CN term WTO term { T.Impl (false, "", $3, $5) } - | TE ID CN term WTO term { T.Impl (false, $2, $4, $6) } - | term STO term { T.Impl (true, "", $1, $3) } - | TE CN term STO term { T.Impl (true, "", $3, $5) } - | TE ID CN term STO term { T.Impl (true, $2, $4, $6) } + | atom { $1 } + | OA term CA fs term { T.Cast ($2, $5) } + | OP term CP fs term { T.Appl ([$2], $5) } + | OP terms CP fs term { T.Appl ($2, $5) } + | OB binder CB fs term { T.Bind ($2, $5) } + | term WTO term { T.Impl (false, "", $1, $3) } + | ID TE term WTO term { T.Impl (false, $1, $3, $5) } + | term STO term { T.Impl (true, "", $1, $3) } + | ID TE term STO term { T.Impl (true, $1, $3, $5) } + | OP term CP { $2 } ; terms: - | term { [$1] } + | term CM term { [$1; $3] } | term CM terms { $1 :: $3 } ; @@ -121,6 +123,8 @@ | TH { T.Th } ; xentity: + | REQUIRE ids + { Some (T.Require $2) } | GRAPH ID { Some (T.Graph $2) } | decl comment ID CN term @@ -140,7 +144,7 @@ ; start: | GRAPH {} | decl {} | def {} - | OPEN {} | CLOSE {} | SORTS {} | EOF {} + | REQUIRE {} | OPEN {} | CLOSE {} | SORTS {} | EOF {} ; entry: | xentity { $1, false } diff --git a/helm/software/lambda-delta/text/txtTxt.ml b/helm/software/lambda-delta/text/txtTxt.ml index 4564adca4..1d501fe0d 100644 --- a/helm/software/lambda-delta/text/txtTxt.ml +++ b/helm/software/lambda-delta/text/txtTxt.ml @@ -60,4 +60,3 @@ and contract_binder f = function in let f xwws = f (T.Abst xwws) in C.list_map f map xws - diff --git a/helm/software/lambda-delta/toplevel/metaAut.ml b/helm/software/lambda-delta/toplevel/metaAut.ml index d686c0f2c..dd6c4a6f6 100644 --- a/helm/software/lambda-delta/toplevel/metaAut.ml +++ b/helm/software/lambda-delta/toplevel/metaAut.ml @@ -12,6 +12,7 @@ module U = NUri module H = U.UriHash module C = Cps +module O = Options module Y = Entity module M = Meta module A = Aut @@ -40,11 +41,6 @@ let hcnt = H.create hcnt_size (* optimized context *) (* Internal functions *******************************************************) -let initial_status cover = - H.clear henv; H.clear hcnt; { - path = []; node = None; nodes = []; line = 1; cover = cover; -} - let id_of_name (id, _, _) = id let mk_qid st id path = @@ -210,7 +206,13 @@ let xlate_entity err f st = function (* Interface functions ******************************************************) -let initial_status ?(cover="") () = - initial_status cover +let initial_status () = + H.clear henv; H.clear hcnt; { + path = []; node = None; nodes = []; line = 1; cover = !O.cover +} + +let refresh_status st = {st with + cover = !O.cover +} let meta_of_aut = xlate_entity diff --git a/helm/software/lambda-delta/toplevel/metaAut.mli b/helm/software/lambda-delta/toplevel/metaAut.mli index 9277dbe5b..a1210c527 100644 --- a/helm/software/lambda-delta/toplevel/metaAut.mli +++ b/helm/software/lambda-delta/toplevel/metaAut.mli @@ -11,7 +11,9 @@ type status -val initial_status: ?cover:string -> unit -> status +val initial_status: unit -> status + +val refresh_status: status -> status val meta_of_aut: (status -> 'a) -> (status -> Meta.entity -> 'a) -> diff --git a/helm/software/lambda-delta/toplevel/top.ml b/helm/software/lambda-delta/toplevel/top.ml index 6c6691354..865271a4a 100644 --- a/helm/software/lambda-delta/toplevel/top.ml +++ b/helm/software/lambda-delta/toplevel/top.ml @@ -15,8 +15,9 @@ module U = NUri module C = Cps module L = Log module T = Time +module O = Options module H = Hierarchy -module O = Output +module Op = Output module Y = Entity module X = Library module AL = AutLexer @@ -58,16 +59,23 @@ let bag_error s msg = let brg_error s msg = L.error BrgR.specs (L.Warn s :: L.Loc :: msg); flush_all () -let initial_status mk_uri cover expand si = { +let initial_status () = { ac = AO.initial_counters; mc = MO.initial_counters; brgc = BrgO.initial_counters; bagc = BagO.initial_counters; - mst = MA.initial_status ~cover (); - dst = DA.initial_status (mk_uri si cover); - tst = DT.initial_status (mk_uri si cover); - ast = AP.initial_status; - kst = Y.initial_status expand si + mst = MA.initial_status (); + dst = DA.initial_status (); + tst = DT.initial_status (); + ast = AP.initial_status (); + kst = Y.initial_status () +} + +let refresh_status st = {st with + mst = MA.refresh_status st.mst; + dst = DA.refresh_status st.dst; + tst = DT.refresh_status st.tst; + kst = Y.refresh_status st.kst } (* kernel related ***********************************************************) @@ -202,21 +210,20 @@ let meta = ref false let progress = ref false let preprocess = ref false let root = ref "" -let si = ref false -let expand = ref false let cc = ref false let export = ref false let old = ref false +let st = ref (initial_status ()) let process_2 st entity = let st = if !L.level > 2 then count_entity st entity else st in - if !export then export_entity !si !moch entity; + if !export then export_entity !O.si !moch entity; if !stage > 2 then type_check st entity else st let process_1 st entity = if !progress then pp_progress entity; let st = if !L.level > 2 then count_entity st entity else st in - if !export && !stage = 1 then export_entity !si !moch entity; + if !export && !stage = 1 then export_entity !O.si !moch entity; if !stage > 1 then process_2 st (xlate_entity entity) else st let process_0 st entity = @@ -273,6 +280,12 @@ try | None -> () | Some och -> ML.close_out C.start och in + let clear_options () = + stage := 3; moch := None; meta := false; progress := false; + preprocess := false; root := ""; cc := false; export := false; + old := false; kernel := Brg; st := initial_status (); + L.clear (); O.clear (); H.clear (); Op.clear_reductions () + in let process_file name = if !L.level > 0 then T.gmtime version_string; if !L.level > 1 then @@ -280,7 +293,6 @@ try if !L.level > 0 then T.utime_stamp "started"; let base_name = Filename.chop_extension (Filename.basename name) in if !meta then set_meta_file base_name; - O.clear_reductions (); let mk_uri = if !stage < 2 then Crg.mk_uri else match !kernel with @@ -288,15 +300,16 @@ try | Bag -> Bag.mk_uri in let cover = F.concat !root base_name in - let st = initial_status mk_uri cover !expand !si in - let st, input = process st name in + O.mk_uri := mk_uri; O.cover := cover; + let sst, input = process (refresh_status !st) name in + st := sst; if !L.level > 0 then T.utime_stamp "processed"; if !L.level > 2 then begin - AO.print_counters C.start st.ac; - if !preprocess then AO.print_process_counters C.start st.ast; - if !stage > 0 then MO.print_counters C.start st.mc; - if !stage > 1 then print_counters st; - if !stage > 2 then O.print_reductions () + AO.print_counters C.start !st.ac; + if !preprocess then AO.print_process_counters C.start !st.ast; + if !stage > 0 then MO.print_counters C.start !st.mc; + if !stage > 1 then print_counters !st; + if !stage > 2 then Op.print_reductions () end in let exit () = @@ -305,14 +318,15 @@ try flush_all () in let help = - "Usage: helena [ -Vcgijmopqux | -Ss | -hkr ] ...\n\n" ^ + "Usage: helena [ -VXcgijmopqux | -Ss | -hkr ] ...\n\n" ^ "Summary levels: 0 just errors (default), 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 (default)\n" in let help_S = " set summary level (see above)" in - let help_V = " show version information" in - + let help_V = " show version information" in + let help_X = " clear options" in + let help_c = " output conversion constraints" in let help_g = " always expand global definitions" in let help_h = " set type hierarchy (default: Z1)" in @@ -321,7 +335,7 @@ try let help_k = " set kernel version (default: brg)" in let help_m = " output intermediate representation (HAL)" in let help_o = " use old abstract language instead of crg" in - let help_p = " preprocess Automath source" in + let help_p = " preprocess source" in let help_q = " disable quotation of identifiers" in let help_r = " set initial segment of URI hierarchy" in let help_s = " set translation stage (see above)" in @@ -332,8 +346,9 @@ try Arg.parse [ ("-S", Arg.Int set_summary, help_S); ("-V", Arg.Unit print_version, help_V); + ("-X", Arg.Unit clear_options, help_X); ("-c", Arg.Set cc, help_c); - ("-g", Arg.Set expand, help_g); + ("-g", Arg.Set O.expand, help_g); ("-h", Arg.String set_hierarchy, help_h); ("-i", Arg.Set O.indexes, help_i); ("-j", Arg.Set progress, help_j); @@ -341,10 +356,10 @@ try ("-m", Arg.Set meta, help_m); ("-o", Arg.Set old, help_o); ("-p", Arg.Set preprocess, help_p); - ("-q", Arg.Set AL.unquote, help_q); + ("-q", Arg.Set O.unquote, help_q); ("-r", Arg.String set_root, help_r); ("-s", Arg.Int set_stage, help_s); - ("-u", Arg.Set si, help_u); + ("-u", Arg.Set O.si, help_u); ("-x", Arg.Set export, help_x) ] process_file help; with BagT.TypeError msg -> bag_error "Type Error" msg -- 2.39.2