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
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
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
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
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
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
-lib text automath common basic_ag basic_rg complete_rg toplevel
+lib common text automath basic_ag basic_rg complete_rg toplevel
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 \
@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
{
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
| "'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 }
(* 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
type status
-val initial_status: status
+val initial_status: unit -> status
val process_command:
(status -> Aut.command -> 'a) -> status -> Aut.command -> 'a
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 = {
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 **************************************************************)
-hierarchy output entity library
+options hierarchy output entity library
\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
+module O = Options
+
type uri = NUri.uri
type id = Aut.id
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 *)
| _, _, 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
}
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
val string_of_graph: unit -> string
val apply: int -> int
+
+val clear: unit -> unit
--- /dev/null
+(*
+ ||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
module P = Printf
module L = Log
-
-let icm = ref 0
+module O = Options
type reductions = {
beta : int;
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)
\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
-val indexes: bool ref
-
-val icm: int ref
-
val clear_reductions: unit -> unit
val add:
module U = NUri
module H = U.UriHash
module C = Cps
+module O = Options
module Y = Entity
module A = Aut
module D = Crg
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
(* 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 =
(* 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
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
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 *)
(* 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))
| 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
{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;
(* 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
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
-\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
\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
-L.hln
+preamble.hln L.hln T0.hln
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"
--- /dev/null
+\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
--- /dev/null
+\* Systematic Explicit Mathematics *\
+\* [1] F. Feferman: *\
+
+\* Development started: 2010 Feb 20 *\
+
+\graph Z3
+
+\sorts Prop, Obj, Term
(* Internal functions *******************************************************)
+let clear () =
+ level := 0; loc := "unknown location"
+
let std = F.std_formatter
let err = F.err_formatter
val level: int ref
+val clear: unit -> unit
+
val warn: string -> unit
val box: int -> unit
| 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 *)
| 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 }
%token <int> IX
%token <string> 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 <Txt.command option * bool> entry
- %nonassoc CP CB CA
+ %nonassoc CP CB CA
%right WTO STO
%%
hash:
;
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 }
| 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 }
;
| TH { T.Th }
;
xentity:
+ | REQUIRE ids
+ { Some (T.Require $2) }
| GRAPH ID
{ Some (T.Graph $2) }
| decl comment ID CN term
;
start:
| GRAPH {} | decl {} | def {}
- | OPEN {} | CLOSE {} | SORTS {} | EOF {}
+ | REQUIRE {} | OPEN {} | CLOSE {} | SORTS {} | EOF {}
;
entry:
| xentity { $1, false }
in
let f xwws = f (T.Abst xwws) in
C.list_map f map xws
-
module U = NUri
module H = U.UriHash
module C = Cps
+module O = Options
module Y = Entity
module M = Meta
module A = Aut
(* 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 =
(* 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
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) ->
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
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 ***********************************************************)
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 =
| 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
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
| 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 () =
flush_all ()
in
let help =
- "Usage: helena [ -Vcgijmopqux | -Ss <number> | -hkr <string> ] <file> ...\n\n" ^
+ "Usage: helena [ -VXcgijmopqux | -Ss <number> | -hkr <string> ] <file> ...\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 = "<number> 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 = "<string> set type hierarchy (default: Z1)" in
let help_k = "<string> 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 = "<string> set initial segment of URI hierarchy" in
let help_s = "<number> set translation stage (see above)" in
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);
("-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
projects / helm.git / commitdiff