From f3cddcf163b36101158ea33b3fad368ac8c62d75 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 15 Sep 2009 10:23:45 +0000 Subject: [PATCH] some renaming. final commit for version 0.8.0 --- helm/software/lambda-delta/.depend.opt | 20 +++--- helm/software/lambda-delta/automath/Omega.aut | 2 +- helm/software/lambda-delta/automath/aut.ml | 12 ++-- .../lambda-delta/automath/autOutput.ml | 16 ++--- .../lambda-delta/automath/autOutput.mli | 2 +- .../lambda-delta/automath/autParser.mly | 12 ++-- .../lambda-delta/automath/autProcess.ml | 14 ++-- .../lambda-delta/automath/autProcess.mli | 2 +- helm/software/lambda-delta/basic_ag/bag.ml | 10 +-- .../lambda-delta/basic_ag/bagOutput.ml | 2 +- .../lambda-delta/basic_ag/bagOutput.mli | 2 +- .../lambda-delta/basic_ag/bagUntrusted.mli | 4 +- helm/software/lambda-delta/basic_rg/brg.ml | 8 +-- .../lambda-delta/basic_rg/brgOutput.ml | 2 +- .../lambda-delta/basic_rg/brgOutput.mli | 4 +- .../lambda-delta/basic_rg/brgUntrusted.mli | 4 +- helm/software/lambda-delta/common/Make | 2 +- .../common/{unit.ml => entity.ml} | 2 +- helm/software/lambda-delta/common/library.ml | 2 +- helm/software/lambda-delta/common/library.mli | 6 +- helm/software/lambda-delta/toplevel/meta.ml | 10 +-- .../software/lambda-delta/toplevel/metaAut.ml | 4 +- .../lambda-delta/toplevel/metaAut.mli | 2 +- .../software/lambda-delta/toplevel/metaBag.ml | 4 +- .../lambda-delta/toplevel/metaBag.mli | 2 +- .../software/lambda-delta/toplevel/metaBrg.ml | 4 +- .../lambda-delta/toplevel/metaBrg.mli | 2 +- .../lambda-delta/toplevel/metaLibrary.ml | 4 +- .../lambda-delta/toplevel/metaLibrary.mli | 2 +- .../lambda-delta/toplevel/metaOutput.ml | 4 +- .../lambda-delta/toplevel/metaOutput.mli | 4 +- helm/software/lambda-delta/toplevel/top.ml | 64 +++++++++---------- 32 files changed, 117 insertions(+), 117 deletions(-) rename helm/software/lambda-delta/common/{unit.ml => entity.ml} (95%) diff --git a/helm/software/lambda-delta/.depend.opt b/helm/software/lambda-delta/.depend.opt index 9e2f23a6f..8ee2db5d8 100644 --- a/helm/software/lambda-delta/.depend.opt +++ b/helm/software/lambda-delta/.depend.opt @@ -21,14 +21,14 @@ common/hierarchy.cmo: lib/cps.cmx common/hierarchy.cmi common/hierarchy.cmx: lib/cps.cmx common/hierarchy.cmi common/output.cmo: lib/log.cmi common/output.cmi common/output.cmx: lib/log.cmx common/output.cmi -common/unit.cmo: lib/nUri.cmi automath/aut.cmx -common/unit.cmx: lib/nUri.cmx automath/aut.cmx -common/library.cmi: common/unit.cmx common/hierarchy.cmi +common/entity.cmo: lib/nUri.cmi automath/aut.cmx +common/entity.cmx: lib/nUri.cmx automath/aut.cmx +common/library.cmi: common/hierarchy.cmi common/entity.cmx common/library.cmo: lib/nUri.cmi common/hierarchy.cmi common/library.cmi common/library.cmx: lib/nUri.cmx common/hierarchy.cmx common/library.cmi -basic_rg/brg.cmo: common/unit.cmx -basic_rg/brg.cmx: common/unit.cmx -basic_rg/brgOutput.cmi: common/unit.cmx lib/log.cmi basic_rg/brg.cmx +basic_rg/brg.cmo: common/entity.cmx +basic_rg/brg.cmx: common/entity.cmx +basic_rg/brgOutput.cmi: lib/log.cmi common/entity.cmx basic_rg/brg.cmx basic_rg/brgOutput.cmo: common/output.cmi lib/nUri.cmi lib/log.cmi \ common/hierarchy.cmi lib/cps.cmx basic_rg/brg.cmx basic_rg/brgOutput.cmi basic_rg/brgOutput.cmx: common/output.cmx lib/nUri.cmx lib/log.cmx \ @@ -66,8 +66,8 @@ basic_rg/brgUntrusted.cmo: lib/log.cmi basic_rg/brgType.cmi \ basic_rg/brgUntrusted.cmx: lib/log.cmx basic_rg/brgType.cmx \ basic_rg/brgReduction.cmx basic_rg/brgEnvironment.cmx basic_rg/brg.cmx \ basic_rg/brgUntrusted.cmi -basic_ag/bag.cmo: common/unit.cmx lib/log.cmi lib/cps.cmx -basic_ag/bag.cmx: common/unit.cmx lib/log.cmx lib/cps.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 \ common/hierarchy.cmi basic_ag/bag.cmx basic_ag/bagOutput.cmi @@ -104,8 +104,8 @@ basic_ag/bagUntrusted.cmo: lib/log.cmi basic_ag/bagType.cmi \ basic_ag/bagEnvironment.cmi basic_ag/bag.cmx basic_ag/bagUntrusted.cmi basic_ag/bagUntrusted.cmx: lib/log.cmx basic_ag/bagType.cmx \ basic_ag/bagEnvironment.cmx basic_ag/bag.cmx basic_ag/bagUntrusted.cmi -toplevel/meta.cmo: common/unit.cmx -toplevel/meta.cmx: common/unit.cmx +toplevel/meta.cmo: common/entity.cmx +toplevel/meta.cmx: common/entity.cmx toplevel/metaOutput.cmi: toplevel/meta.cmx toplevel/metaOutput.cmo: lib/nUri.cmi toplevel/meta.cmx lib/log.cmi \ lib/cps.cmx toplevel/metaOutput.cmi diff --git a/helm/software/lambda-delta/automath/Omega.aut b/helm/software/lambda-delta/automath/Omega.aut index 661154db9..2466a606e 100644 --- a/helm/software/lambda-delta/automath/Omega.aut +++ b/helm/software/lambda-delta/automath/Omega.aut @@ -2,7 +2,7 @@ # This book is not accepted in AUT-QE because [y:'type'] is not allowed # This book is accepted in lambda-delta with sort inclusion but Omega is not # valid if sort inclusion is allowed on the term backbone only -# This book is valid in lambda-delta with sort inclusion allowed everywhere +# This book is valid in lambda-delta with unrestricted sort inclusion +l @ Delta := [x:[y:'type']'type']x : [x:[y:'type']'type']'type' diff --git a/helm/software/lambda-delta/automath/aut.ml b/helm/software/lambda-delta/automath/aut.ml index d05e53d03..513bd4a47 100644 --- a/helm/software/lambda-delta/automath/aut.ml +++ b/helm/software/lambda-delta/automath/aut.ml @@ -16,10 +16,10 @@ type qid = id * bool * id list (* qualified identifier: name, local?, path *) type term = Sort of bool (* sorts: true = TYPE, false = PROP *) | GRef of qid * term list (* reference: name, arguments *) | Appl of term * term (* application: argument, function *) - | Abst of id * term * term (* abstraction: name, type, body *) + | Abst of id * term * term (* abstraction: name, domain, scope *) -type unit = 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 *) - | Def of id * term * bool * term (* definition: name, type, transparent?, body *) +type entity = 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, domain *) + | Decl of id * term (* declaration: name, domain *) + | Def of id * term * bool * term (* definition: name, domain, transparent?, body *) diff --git a/helm/software/lambda-delta/automath/autOutput.ml b/helm/software/lambda-delta/automath/autOutput.ml index f9467d63e..5b415ff0b 100644 --- a/helm/software/lambda-delta/automath/autOutput.ml +++ b/helm/software/lambda-delta/automath/autOutput.ml @@ -50,7 +50,7 @@ let rec count_term f c = function let f c = count_term f c t in count_term f c w -let count_unit f c = function +let count_entity f c = function | A.Section _ -> f {c with sections = succ c.sections} | A.Context _ -> @@ -68,14 +68,14 @@ let count_unit f c = function let print_counters f c = let terms = c.sorts + c.grefs + c.appls + c.absts in - let units = c.sections + c.contexts + c.blocks + c.decls + c.defs in + let entities = c.sections + c.contexts + c.blocks + c.decls + c.defs in L.warn (P.sprintf " Automath representation summary"); - L.warn (P.sprintf " Total book units: %7u" units); - L.warn (P.sprintf " Section units: %7u" c.sections); - L.warn (P.sprintf " Context units: %7u" c.contexts); - L.warn (P.sprintf " Block units: %7u" c.blocks); - L.warn (P.sprintf " Declaration units: %7u" c.decls); - L.warn (P.sprintf " Definition units: %7u" c.defs); + L.warn (P.sprintf " Total book entities: %7u" entities); + L.warn (P.sprintf " Section entities: %7u" c.sections); + L.warn (P.sprintf " Context entities: %7u" c.contexts); + L.warn (P.sprintf " Block entities: %7u" c.blocks); + L.warn (P.sprintf " Declaration entities: %7u" c.decls); + L.warn (P.sprintf " Definition entities: %7u" c.defs); L.warn (P.sprintf " Total Parameter items: %7u" c.pars); L.warn (P.sprintf " Application items: %7u" c.pars); L.warn (P.sprintf " Total term items: %7u" terms); diff --git a/helm/software/lambda-delta/automath/autOutput.mli b/helm/software/lambda-delta/automath/autOutput.mli index fb02ed2d8..611c1bf6b 100644 --- a/helm/software/lambda-delta/automath/autOutput.mli +++ b/helm/software/lambda-delta/automath/autOutput.mli @@ -13,7 +13,7 @@ type counters val initial_counters: counters -val count_unit: (counters -> 'a) -> counters -> Aut.unit -> 'a +val count_entity: (counters -> 'a) -> counters -> Aut.entity -> 'a val print_counters: (unit -> 'a) -> counters -> 'a diff --git a/helm/software/lambda-delta/automath/autParser.mly b/helm/software/lambda-delta/automath/autParser.mly index f974b9808..c772837b3 100644 --- a/helm/software/lambda-delta/automath/autParser.mly +++ b/helm/software/lambda-delta/automath/autParser.mly @@ -32,7 +32,7 @@ %token TYPE PROP DEF EB E PN EXIT %start book - %type book + %type book %% path: MINUS {} | FS {} ; oftype: CN {} | CM {} ; @@ -71,7 +71,7 @@ | term { [$1] } | term CM terms { $1 :: $3 } ; - unit: + entity: | PLUS IDENT { A.Section (Some (true, $2)) } | PLUS TIMES IDENT { A.Section (Some (false, $3)) } | MINUS IDENT { A.Section None } @@ -86,10 +86,10 @@ | IDENT DEF expand term sc term { A.Def ($1, $6, $3, $4) } | IDENT sc term DEF expand term { A.Def ($1, $3, $5, $6) } ; - units: - | { [] } - | unit units { $1 :: $2 } + entities: + | { [] } + | entity entities { $1 :: $2 } ; book: - | units eof { $1 } + | entities eof { $1 } ; diff --git a/helm/software/lambda-delta/automath/autProcess.ml b/helm/software/lambda-delta/automath/autProcess.ml index 56ecd4ca4..0009e021e 100644 --- a/helm/software/lambda-delta/automath/autProcess.ml +++ b/helm/software/lambda-delta/automath/autProcess.ml @@ -57,12 +57,12 @@ let proc_global f st = in exp_count f st -let proc_unit f st unit = match unit with - | A.Section section -> proc_section f st section unit - | A.Context _ -> proc_context f st unit - | A.Block _ -> proc_block f st unit - | A.Decl _ -> proc_global f st unit - | A.Def _ -> proc_global f st unit +let proc_entity f st entity = match entity with + | A.Section section -> proc_section f st section entity + | A.Context _ -> proc_context f st entity + | A.Block _ -> proc_block f st entity + | A.Decl _ -> proc_global f st entity + | A.Def _ -> proc_global f st entity (* interface functions ******************************************************) @@ -72,6 +72,6 @@ let initial_status = { iao = 0; iar = 0; iac = 0; iag = 0 } -let process_unit = proc_unit +let process_entity = proc_entity let get_counters f st = f st.iao st.iar st.iac st.iag diff --git a/helm/software/lambda-delta/automath/autProcess.mli b/helm/software/lambda-delta/automath/autProcess.mli index e84f91aee..8f10b653e 100644 --- a/helm/software/lambda-delta/automath/autProcess.mli +++ b/helm/software/lambda-delta/automath/autProcess.mli @@ -13,6 +13,6 @@ type status val initial_status: status -val process_unit: (status -> Aut.unit -> 'a) -> status -> Aut.unit -> 'a +val process_entity: (status -> Aut.entity -> 'a) -> status -> Aut.entity -> 'a val get_counters: (int -> int -> int -> int -> 'a) -> status -> 'a diff --git a/helm/software/lambda-delta/basic_ag/bag.ml b/helm/software/lambda-delta/basic_ag/bag.ml index 3fa4568d1..79e7a0421 100644 --- a/helm/software/lambda-delta/basic_ag/bag.ml +++ b/helm/software/lambda-delta/basic_ag/bag.ml @@ -12,8 +12,8 @@ (* kernel version: basic, absolute, global *) (* note : experimental *) -type uri = Unit.uri -type id = Unit.id +type uri = Entity.uri +type id = Entity.id type bind = Void (* exclusion *) | Abst of term (* abstraction *) @@ -22,13 +22,13 @@ type bind = Void (* exclusion *) and term = Sort of int (* hierarchy index *) | LRef of int (* location *) | GRef of uri (* reference *) - | Cast of term * term (* type, term *) + | Cast of term * term (* domain, element *) | Appl of term * term (* argument, function *) | Bind of int * id * bind * term (* location, name, binder, scope *) -type entry = bind Unit.entry (* age, uri, binder *) +type entry = bind Entity.entry (* age, uri, binder *) -type unit = bind Unit.unit +type entity = bind Entity.entity type lenv = (int * id * bind) list (* location, name, binder *) diff --git a/helm/software/lambda-delta/basic_ag/bagOutput.ml b/helm/software/lambda-delta/basic_ag/bagOutput.ml index eb3bf05d9..400ffc55e 100644 --- a/helm/software/lambda-delta/basic_ag/bagOutput.ml +++ b/helm/software/lambda-delta/basic_ag/bagOutput.ml @@ -74,7 +74,7 @@ let count_entry_binder f c = function let count_entry f c (_, _, b) = count_entry_binder f c b -let count_unit f c = function +let count_entity f c = function | Some entry -> count_entry f c entry | None -> f c diff --git a/helm/software/lambda-delta/basic_ag/bagOutput.mli b/helm/software/lambda-delta/basic_ag/bagOutput.mli index f3761ac1a..daa07a6d1 100644 --- a/helm/software/lambda-delta/basic_ag/bagOutput.mli +++ b/helm/software/lambda-delta/basic_ag/bagOutput.mli @@ -13,7 +13,7 @@ type counters val initial_counters: counters -val count_unit: (counters -> 'a) -> counters -> Bag.unit -> 'a +val count_entity: (counters -> 'a) -> counters -> Bag.entity -> 'a val print_counters: (unit -> 'a) -> counters -> 'a diff --git a/helm/software/lambda-delta/basic_ag/bagUntrusted.mli b/helm/software/lambda-delta/basic_ag/bagUntrusted.mli index 76ba89918..9aa4ec575 100644 --- a/helm/software/lambda-delta/basic_ag/bagUntrusted.mli +++ b/helm/software/lambda-delta/basic_ag/bagUntrusted.mli @@ -10,5 +10,5 @@ V_______________________________________________________________ *) val type_check: - (Bag.term option -> Bag.unit -> 'a) -> ?si:bool -> - Hierarchy.graph -> Bag.unit -> 'a + (Bag.term option -> Bag.entity -> 'a) -> ?si:bool -> + Hierarchy.graph -> Bag.entity -> 'a diff --git a/helm/software/lambda-delta/basic_rg/brg.ml b/helm/software/lambda-delta/basic_rg/brg.ml index d0a442807..e3c586681 100644 --- a/helm/software/lambda-delta/basic_rg/brg.ml +++ b/helm/software/lambda-delta/basic_rg/brg.ml @@ -12,8 +12,8 @@ (* kernel version: basic, relative, global *) (* note : ufficial basic lambda-delta *) -type uri = Unit.uri -type id = Unit.id +type uri = Entity.uri +type id = Entity.id type attr = Name of bool * id (* real?, name *) | Apix of int (* additional position index *) @@ -31,9 +31,9 @@ and term = Sort of attrs * int (* attrs, hierarchy index *) | Appl of attrs * term * term (* attrs, argument, function *) | Bind of bind * term (* binder, scope *) -type entry = bind Unit.entry (* age, uri, binder *) +type entry = bind Entity.entry (* age, uri, binder *) -type unit = bind Unit.unit +type entity = bind Entity.entity type lenv = Null (* Cons: tail, relative local environment, binder *) diff --git a/helm/software/lambda-delta/basic_rg/brgOutput.ml b/helm/software/lambda-delta/basic_rg/brgOutput.ml index 1a0b0650e..662a71988 100644 --- a/helm/software/lambda-delta/basic_rg/brgOutput.ml +++ b/helm/software/lambda-delta/basic_rg/brgOutput.ml @@ -103,7 +103,7 @@ let count_entry f c = function } in f c -let count_unit f c = function +let count_entity f c = function | Some entry -> count_entry f c entry | None -> f c diff --git a/helm/software/lambda-delta/basic_rg/brgOutput.mli b/helm/software/lambda-delta/basic_rg/brgOutput.mli index b9acfd302..0af895dd4 100644 --- a/helm/software/lambda-delta/basic_rg/brgOutput.mli +++ b/helm/software/lambda-delta/basic_rg/brgOutput.mli @@ -13,10 +13,10 @@ type counters val initial_counters: counters -val count_unit: (counters -> 'a) -> counters -> Brg.unit -> 'a +val count_entity: (counters -> 'a) -> counters -> Brg.entity -> 'a val print_counters: (unit -> 'a) -> counters -> 'a val specs: (Brg.lenv, Brg.term) Log.specs -val export_entry: Format.formatter -> Brg.bind Unit.entry -> unit +val export_entry: Format.formatter -> Brg.bind Entity.entry -> unit diff --git a/helm/software/lambda-delta/basic_rg/brgUntrusted.mli b/helm/software/lambda-delta/basic_rg/brgUntrusted.mli index 80f9b2eee..bab64303e 100644 --- a/helm/software/lambda-delta/basic_rg/brgUntrusted.mli +++ b/helm/software/lambda-delta/basic_rg/brgUntrusted.mli @@ -10,5 +10,5 @@ V_______________________________________________________________ *) val type_check: - (BrgType.message -> 'a) -> (Brg.term option -> Brg.unit -> 'a) -> - ?si:bool -> Hierarchy.graph -> Brg.unit -> 'a + (BrgType.message -> 'a) -> (Brg.term option -> Brg.entity -> 'a) -> + ?si:bool -> Hierarchy.graph -> Brg.entity -> 'a diff --git a/helm/software/lambda-delta/common/Make b/helm/software/lambda-delta/common/Make index ccf9cfd65..8085aa65b 100644 --- a/helm/software/lambda-delta/common/Make +++ b/helm/software/lambda-delta/common/Make @@ -1 +1 @@ -hierarchy output unit library +hierarchy output entity library diff --git a/helm/software/lambda-delta/common/unit.ml b/helm/software/lambda-delta/common/entity.ml similarity index 95% rename from helm/software/lambda-delta/common/unit.ml rename to helm/software/lambda-delta/common/entity.ml index d76b9d9fe..78d7c3ace 100644 --- a/helm/software/lambda-delta/common/unit.ml +++ b/helm/software/lambda-delta/common/entity.ml @@ -14,4 +14,4 @@ type id = Aut.id type 'bind entry = int * uri * 'bind (* age, uri, binder *) -type 'bind unit = 'bind entry option +type 'bind entity = 'bind entry option diff --git a/helm/software/lambda-delta/common/library.ml b/helm/software/lambda-delta/common/library.ml index c60a227e7..8ef875ce7 100644 --- a/helm/software/lambda-delta/common/library.ml +++ b/helm/software/lambda-delta/common/library.ml @@ -42,7 +42,7 @@ let close_entry frm = (* interface functions ******************************************************) -let export_unit export_entry si g = function +let export_entity export_entry si g = function | Some entry -> let _, uri, bind = entry in let path = path_of_uri uri in diff --git a/helm/software/lambda-delta/common/library.mli b/helm/software/lambda-delta/common/library.mli index 1a10b6e9d..68325f3d9 100644 --- a/helm/software/lambda-delta/common/library.mli +++ b/helm/software/lambda-delta/common/library.mli @@ -9,6 +9,6 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) -val export_unit: - (Format.formatter -> 'bind Unit.entry -> unit) -> - bool -> Hierarchy.graph -> 'bind Unit.unit -> unit +val export_entity: + (Format.formatter -> 'bind Entity.entry -> unit) -> + bool -> Hierarchy.graph -> 'bind Entity.entity -> unit diff --git a/helm/software/lambda-delta/toplevel/meta.ml b/helm/software/lambda-delta/toplevel/meta.ml index a3cb08585..563e19b99 100644 --- a/helm/software/lambda-delta/toplevel/meta.ml +++ b/helm/software/lambda-delta/toplevel/meta.ml @@ -9,19 +9,19 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) -type uri = Unit.uri +type uri = Entity.uri -type id = Unit.id +type id = Entity.id type term = Sort of bool (* sorts: true = TYPE, false = PROP *) | LRef of int * int (* local reference: local environment length, de bruijn index *) | GRef of int * uri * term list (* global reference: local environment length, name, arguments *) | Appl of term * term (* application: argument, function *) - | Abst of id * term * term (* abstraction: name, type, scope *) + | Abst of id * term * term (* abstraction: name, domain, scope *) type pars = (id * term) list (* parameter declarations: name, type *) -(* entry: line number, parameters, name, type, (transparent?, body) *) +(* entry: line number, parameters, name, domain, (transparent?, body) *) type entry = int * pars * uri * term * (bool * term) option -type unit = entry option +type entity = entry option diff --git a/helm/software/lambda-delta/toplevel/metaAut.ml b/helm/software/lambda-delta/toplevel/metaAut.ml index 335f57fc0..db18ade47 100644 --- a/helm/software/lambda-delta/toplevel/metaAut.ml +++ b/helm/software/lambda-delta/toplevel/metaAut.ml @@ -145,7 +145,7 @@ let rec xlate_term f st lenv = function in resolve_lref f st l lenv (id_of_name name) -let xlate_unit f st = function +let xlate_entity f st = function | A.Section (Some (_, name)) -> f {st with path = name :: st.path; nodes = st.node :: st.nodes} None | A.Section None -> @@ -204,4 +204,4 @@ let xlate_unit f st = function let initial_status ?(cover="") () = initial_status hsize cover -let meta_of_aut = xlate_unit +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 79c8fb22b..cfcb49d0b 100644 --- a/helm/software/lambda-delta/toplevel/metaAut.mli +++ b/helm/software/lambda-delta/toplevel/metaAut.mli @@ -13,4 +13,4 @@ type status val initial_status: ?cover:string -> unit -> status -val meta_of_aut: (status -> Meta.unit -> 'a) -> status -> Aut.unit -> 'a +val meta_of_aut: (status -> Meta.entity -> 'a) -> status -> Aut.entity -> 'a diff --git a/helm/software/lambda-delta/toplevel/metaBag.ml b/helm/software/lambda-delta/toplevel/metaBag.ml index 89c1527c8..67c938df0 100644 --- a/helm/software/lambda-delta/toplevel/metaBag.ml +++ b/helm/software/lambda-delta/toplevel/metaBag.ml @@ -63,10 +63,10 @@ let xlate_entry f = function let f c = unwind_to_xlate_term (f c) c u in xlate_pars f pars -let xlate_unit f = function +let xlate_entity f = function | None -> f None | Some e -> let f e = f (Some e) in xlate_entry f e (* Interface functions ******************************************************) -let bag_of_meta = xlate_unit +let bag_of_meta = xlate_entity diff --git a/helm/software/lambda-delta/toplevel/metaBag.mli b/helm/software/lambda-delta/toplevel/metaBag.mli index f19f6dd76..b8e41be04 100644 --- a/helm/software/lambda-delta/toplevel/metaBag.mli +++ b/helm/software/lambda-delta/toplevel/metaBag.mli @@ -9,4 +9,4 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) -val bag_of_meta: (Bag.unit -> 'a) -> Meta.unit -> 'a +val bag_of_meta: (Bag.entity -> 'a) -> Meta.entity -> 'a diff --git a/helm/software/lambda-delta/toplevel/metaBrg.ml b/helm/software/lambda-delta/toplevel/metaBrg.ml index eff9e9c55..2fb17262e 100644 --- a/helm/software/lambda-delta/toplevel/metaBrg.ml +++ b/helm/software/lambda-delta/toplevel/metaBrg.ml @@ -62,10 +62,10 @@ let xlate_entry f = function let f c = unwind_to_xlate_term (f c) c u in xlate_pars f pars -let xlate_unit f = function +let xlate_entity f = function | None -> f None | Some e -> let f e = f (Some e) in xlate_entry f e (* Interface functions ******************************************************) -let brg_of_meta = xlate_unit +let brg_of_meta = xlate_entity diff --git a/helm/software/lambda-delta/toplevel/metaBrg.mli b/helm/software/lambda-delta/toplevel/metaBrg.mli index b07ed1253..6a4a7bd2b 100644 --- a/helm/software/lambda-delta/toplevel/metaBrg.mli +++ b/helm/software/lambda-delta/toplevel/metaBrg.mli @@ -9,4 +9,4 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) -val brg_of_meta: (Brg.unit -> 'a) -> Meta.unit -> 'a +val brg_of_meta: (Brg.entity -> 'a) -> Meta.entity -> 'a diff --git a/helm/software/lambda-delta/toplevel/metaLibrary.ml b/helm/software/lambda-delta/toplevel/metaLibrary.ml index a6e780a5f..3ae116d96 100644 --- a/helm/software/lambda-delta/toplevel/metaLibrary.ml +++ b/helm/software/lambda-delta/toplevel/metaLibrary.ml @@ -29,8 +29,8 @@ let open_out f name = F.pp_set_margin frm max_int; f (och, frm) -let write_unit f (_, frm) unit = - O.pp_unit f frm unit +let write_entity f (_, frm) entity = + O.pp_entity f frm entity let close_out f (och, _) = close_out och; f () diff --git a/helm/software/lambda-delta/toplevel/metaLibrary.mli b/helm/software/lambda-delta/toplevel/metaLibrary.mli index 26172e46c..2f6e41b80 100644 --- a/helm/software/lambda-delta/toplevel/metaLibrary.mli +++ b/helm/software/lambda-delta/toplevel/metaLibrary.mli @@ -13,6 +13,6 @@ type out_channel val open_out: (out_channel -> 'a) -> string -> 'a -val write_unit: (unit -> 'a) -> out_channel -> Meta.unit -> 'a +val write_entity: (unit -> 'a) -> out_channel -> Meta.entity -> 'a val close_out: (unit -> 'a) -> out_channel -> 'a diff --git a/helm/software/lambda-delta/toplevel/metaOutput.ml b/helm/software/lambda-delta/toplevel/metaOutput.ml index a8560ab18..7f62c8abc 100644 --- a/helm/software/lambda-delta/toplevel/metaOutput.ml +++ b/helm/software/lambda-delta/toplevel/metaOutput.ml @@ -77,7 +77,7 @@ let count_entry f c = function let f c = count_term f c w in Cps.list_fold_left f count_par c pars -let count_unit f c = function +let count_entity f c = function | Some e -> count_entry f c e | None -> f c @@ -150,6 +150,6 @@ let pp_entry frm (l, pars, uri, u, body) = F.fprintf frm "@[%u@@%s%a%a:%a@]@\n%!" l (U.string_of_uri uri) pp_pars pars pp_body body pp_term u -let pp_unit f frm = function +let pp_entity f frm = function | Some entry -> pp_entry frm entry; f () | None -> f () diff --git a/helm/software/lambda-delta/toplevel/metaOutput.mli b/helm/software/lambda-delta/toplevel/metaOutput.mli index 611e12139..1a7b119ce 100644 --- a/helm/software/lambda-delta/toplevel/metaOutput.mli +++ b/helm/software/lambda-delta/toplevel/metaOutput.mli @@ -13,8 +13,8 @@ type counters val initial_counters: counters -val count_unit: (counters -> 'a) -> counters -> Meta.unit -> 'a +val count_entity: (counters -> 'a) -> counters -> Meta.entity -> 'a val print_counters: (unit -> 'a) -> counters -> 'a -val pp_unit: (unit -> 'a) -> Format.formatter -> Meta.unit -> 'a +val pp_entity: (unit -> 'a) -> Format.formatter -> Meta.entity -> 'a diff --git a/helm/software/lambda-delta/toplevel/top.ml b/helm/software/lambda-delta/toplevel/top.ml index e87bf8a07..c3923b387 100644 --- a/helm/software/lambda-delta/toplevel/top.ml +++ b/helm/software/lambda-delta/toplevel/top.ml @@ -49,8 +49,8 @@ let initial_status cover = { ast = AP.initial_status } -let count count_fun c unit = - if !L.level > 2 then count_fun C.start c unit else c +let count count_fun c entity = + if !L.level > 2 then count_fun C.start c entity else c let flush () = L.flush 0; L.flush_err () @@ -60,16 +60,16 @@ let bag_error s msg = let brg_error s msg = L.error BrgR.specs (L.Warn s :: L.Loc :: msg); flush () -let process_unit f st = +let process_entity f st = let f ast = f {st with ast = ast} in - AP.process_unit f st.ast + AP.process_entity f st.ast (* kernel related ***********************************************************) type kernel = Brg | Bag -type kernel_unit = Brgunit of Brg.unit - | Bagunit of Bag.unit +type kernel_entity = BrgEntity of Brg.entity + | BagEntity of Bag.entity let kernel = ref Brg @@ -77,21 +77,21 @@ let print_counters st = match !kernel with | Brg -> BrgO.print_counters C.start st.brgc | Bag -> BagO.print_counters C.start st.bagc -let kernel_of_meta f st unit = match !kernel with +let kernel_of_meta f st entity = match !kernel with | Brg -> - let f unit = f st (Brgunit unit) in - MBrg.brg_of_meta f unit + let f entity = f st (BrgEntity entity) in + MBrg.brg_of_meta f entity | Bag -> - let f unit = f st (Bagunit unit) in - MBag.bag_of_meta f unit + let f entity = f st (BagEntity entity) in + MBag.bag_of_meta f entity -let count_unit st = function - | Brgunit unit -> {st with brgc = count BrgO.count_unit st.brgc unit} - | Bagunit unit -> {st with bagc = count BagO.count_unit st.bagc unit} +let count_entity st = function + | BrgEntity entity -> {st with brgc = count BrgO.count_entity st.brgc entity} + | BagEntity entity -> {st with bagc = count BagO.count_entity st.bagc entity} -let export_unit si g = function - | Brgunit unit -> G.export_unit BrgO.export_entry si g unit - | Bagunit _ -> () +let export_entity si g = function + | BrgEntity entity -> G.export_entity BrgO.export_entry si g entity + | BagEntity _ -> () let type_check f st si g k = let brg_err msg = brg_error "Type Error" msg; failwith "Interrupted" in @@ -100,8 +100,8 @@ let type_check f st si g k = | Some (i, u, _) -> f st (Some (i, u)) in match k with - | Brgunit unit -> BrgU.type_check brg_err f ~si g unit - | Bagunit unit -> BagU.type_check f ~si g unit + | BrgEntity entity -> BrgU.type_check brg_err f ~si g entity + | BagEntity entity -> BagU.type_check f ~si g entity (****************************************************************************) @@ -152,7 +152,7 @@ try if !L.level > 0 then T.utime_stamp "parsed"; let rec aux st = function | [] -> st - | unit :: tl -> + | entity :: tl -> (* stage 3 *) let f st = function | None -> st @@ -162,31 +162,31 @@ try st in (* stage 2 *) - let f st unit = - let st = count_unit st unit in - if !export then export_unit !si !graph unit; - if !stage > 2 then type_check f st !si !graph unit else st + let f st entity = + let st = count_entity st entity in + if !export then export_entity !si !graph entity; + if !stage > 2 then type_check f st !si !graph entity else st in (* stage 1 *) - let f st mst unit = + let f st mst entity = let st = {st with - mst = mst; mc = count MO.count_unit st.mc unit + mst = mst; mc = count MO.count_entity st.mc entity } in begin match !moch with | None -> () - | Some och -> ML.write_unit C.start och unit + | Some och -> ML.write_entity C.start och entity end; - if !stage > 1 then kernel_of_meta f st unit else st + if !stage > 1 then kernel_of_meta f st entity else st in (* stage 0 *) - let st = {st with ac = count AO.count_unit st.ac unit} in - let f st unit = + let st = {st with ac = count AO.count_entity st.ac entity} in + let f st entity = let st = - if !stage > 0 then MA.meta_of_aut (f st) st.mst unit else st + if !stage > 0 then MA.meta_of_aut (f st) st.mst entity else st in aux st tl in - if !process then process_unit f st unit else f st unit + if !process then process_entity f st entity else f st entity in O.clear_reductions (); let cover = if !use_cover then base_name else "" in -- 2.39.2