From 79684e8bd0f54b5c88fff981366bd8c78dd0fbe9 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Thu, 10 Sep 2009 13:14:48 +0000 Subject: [PATCH] some interfaces improved --- helm/software/lambda-delta/.depend.opt | 53 ++++++-------- helm/software/lambda-delta/automath/aut.ml | 2 +- .../lambda-delta/automath/autOutput.ml | 16 ++--- .../lambda-delta/automath/autOutput.mli | 2 +- .../lambda-delta/automath/autParser.mly | 10 +-- .../lambda-delta/automath/autProcess.ml | 14 ++-- .../lambda-delta/automath/autProcess.mli | 2 +- helm/software/lambda-delta/basic_ag/bag.ml | 8 +-- .../lambda-delta/basic_ag/bagEnvironment.ml | 12 ++-- .../lambda-delta/basic_ag/bagEnvironment.mli | 4 +- .../lambda-delta/basic_ag/bagOutput.ml | 10 +-- .../lambda-delta/basic_ag/bagOutput.mli | 2 +- .../lambda-delta/basic_ag/bagReduction.ml | 6 +- .../software/lambda-delta/basic_ag/bagType.ml | 4 +- .../lambda-delta/basic_ag/bagUntrusted.ml | 12 ++-- .../lambda-delta/basic_ag/bagUntrusted.mli | 4 +- helm/software/lambda-delta/basic_rg/brg.ml | 8 +-- .../lambda-delta/basic_rg/brgEnvironment.ml | 12 ++-- .../lambda-delta/basic_rg/brgEnvironment.mli | 4 +- .../lambda-delta/basic_rg/brgOutput.ml | 12 ++-- .../lambda-delta/basic_rg/brgOutput.mli | 4 +- .../lambda-delta/basic_rg/brgReduction.ml | 6 +- .../lambda-delta/basic_rg/brgReduction.mli | 14 ++-- .../lambda-delta/basic_rg/brgSubstitution.mli | 3 +- .../software/lambda-delta/basic_rg/brgType.ml | 61 ++++++++-------- .../lambda-delta/basic_rg/brgType.mli | 8 +-- .../lambda-delta/basic_rg/brgUntrusted.ml | 18 ++--- .../lambda-delta/basic_rg/brgUntrusted.mli | 4 +- helm/software/lambda-delta/common/Make | 2 +- .../software/lambda-delta/common/hierarchy.ml | 8 +-- .../lambda-delta/common/hierarchy.mli | 2 +- helm/software/lambda-delta/common/library.ml | 8 +-- helm/software/lambda-delta/common/library.mli | 6 +- .../lambda-delta/common/{item.ml => unit.ml} | 4 +- helm/software/lambda-delta/toplevel/meta.ml | 6 +- .../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 | 8 +-- .../lambda-delta/toplevel/metaOutput.mli | 4 +- helm/software/lambda-delta/toplevel/top.ml | 71 +++++++++---------- 46 files changed, 222 insertions(+), 236 deletions(-) rename helm/software/lambda-delta/common/{item.ml => unit.ml} (87%) diff --git a/helm/software/lambda-delta/.depend.opt b/helm/software/lambda-delta/.depend.opt index 692e237c6..9e2f23a6f 100644 --- a/helm/software/lambda-delta/.depend.opt +++ b/helm/software/lambda-delta/.depend.opt @@ -1,17 +1,9 @@ -lib/nUri.cmi: lib/nUri.cmo: lib/nUri.cmi lib/nUri.cmx: lib/nUri.cmi -lib/cps.cmo: -lib/cps.cmx: -lib/share.cmo: -lib/share.cmx: -lib/log.cmi: lib/log.cmo: lib/cps.cmx lib/log.cmi lib/log.cmx: lib/cps.cmx lib/log.cmi lib/time.cmo: lib/log.cmi lib/time.cmx: lib/log.cmx -automath/aut.cmo: -automath/aut.cmx: automath/autProcess.cmi: automath/aut.cmx automath/autProcess.cmo: automath/aut.cmx automath/autProcess.cmi automath/autProcess.cmx: automath/aut.cmx automath/autProcess.cmi @@ -25,25 +17,23 @@ 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/item.cmo: lib/nUri.cmi automath/aut.cmx -common/item.cmx: lib/nUri.cmx automath/aut.cmx -common/library.cmi: common/item.cmx common/hierarchy.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/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/item.cmx -basic_rg/brg.cmx: common/item.cmx -basic_rg/brgOutput.cmi: lib/log.cmi common/item.cmx basic_rg/brg.cmx +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/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 \ common/hierarchy.cmx lib/cps.cmx basic_rg/brg.cmx basic_rg/brgOutput.cmi -basic_rg/brgEnvironment.cmi: lib/nUri.cmi basic_rg/brg.cmx +basic_rg/brgEnvironment.cmi: basic_rg/brg.cmx basic_rg/brgEnvironment.cmo: lib/nUri.cmi basic_rg/brg.cmx \ basic_rg/brgEnvironment.cmi basic_rg/brgEnvironment.cmx: lib/nUri.cmx basic_rg/brg.cmx \ @@ -68,21 +58,22 @@ basic_rg/brgType.cmx: lib/share.cmx lib/nUri.cmx lib/log.cmx \ common/hierarchy.cmx lib/cps.cmx basic_rg/brgSubstitution.cmx \ basic_rg/brgReduction.cmx basic_rg/brgOutput.cmx \ basic_rg/brgEnvironment.cmx basic_rg/brg.cmx basic_rg/brgType.cmi -basic_rg/brgUntrusted.cmi: common/hierarchy.cmi basic_rg/brg.cmx +basic_rg/brgUntrusted.cmi: common/hierarchy.cmi basic_rg/brgType.cmi \ + basic_rg/brg.cmx basic_rg/brgUntrusted.cmo: lib/log.cmi basic_rg/brgType.cmi \ basic_rg/brgReduction.cmi basic_rg/brgEnvironment.cmi basic_rg/brg.cmx \ basic_rg/brgUntrusted.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: lib/log.cmi common/item.cmx lib/cps.cmx -basic_ag/bag.cmx: lib/log.cmx common/item.cmx lib/cps.cmx +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/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 basic_ag/bagOutput.cmx: common/output.cmx lib/nUri.cmx lib/log.cmx \ common/hierarchy.cmx basic_ag/bag.cmx basic_ag/bagOutput.cmi -basic_ag/bagEnvironment.cmi: lib/nUri.cmi basic_ag/bag.cmx +basic_ag/bagEnvironment.cmi: basic_ag/bag.cmx basic_ag/bagEnvironment.cmo: lib/nUri.cmi lib/log.cmi basic_ag/bag.cmx \ basic_ag/bagEnvironment.cmi basic_ag/bagEnvironment.cmx: lib/nUri.cmx lib/log.cmx basic_ag/bag.cmx \ @@ -113,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/item.cmx -toplevel/meta.cmx: common/item.cmx +toplevel/meta.cmo: common/unit.cmx +toplevel/meta.cmx: common/unit.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 @@ -142,15 +133,15 @@ toplevel/top.cmo: lib/time.cmx common/output.cmi lib/nUri.cmi \ toplevel/metaOutput.cmi toplevel/metaLibrary.cmi toplevel/metaBrg.cmi \ toplevel/metaBag.cmi toplevel/metaAut.cmi lib/log.cmi common/library.cmi \ common/hierarchy.cmi lib/cps.cmx basic_rg/brgUntrusted.cmi \ - basic_rg/brgType.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 + 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 toplevel/top.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 lib/log.cmx common/library.cmx \ common/hierarchy.cmx lib/cps.cmx basic_rg/brgUntrusted.cmx \ - basic_rg/brgType.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 + 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 diff --git a/helm/software/lambda-delta/automath/aut.ml b/helm/software/lambda-delta/automath/aut.ml index 4b1dffd9e..d05e53d03 100644 --- a/helm/software/lambda-delta/automath/aut.ml +++ b/helm/software/lambda-delta/automath/aut.ml @@ -18,7 +18,7 @@ type term = Sort of bool (* sorts: true = TYPE, false = PROP *) | Appl of term * term (* application: argument, function *) | Abst of id * term * term (* abstraction: name, type, body *) -type item = Section of (bool * id) option (* section: Some true = open, Some false = reopen, None = close last *) +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 *) diff --git a/helm/software/lambda-delta/automath/autOutput.ml b/helm/software/lambda-delta/automath/autOutput.ml index 2f1a4d91c..f9467d63e 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_item f c = function +let count_unit f c = function | A.Section _ -> f {c with sections = succ c.sections} | A.Context _ -> @@ -68,14 +68,14 @@ let count_item f c = function let print_counters f c = let terms = c.sorts + c.grefs + c.appls + c.absts in - let items = c.sections + c.contexts + c.blocks + c.decls + c.defs in + let units = c.sections + c.contexts + c.blocks + c.decls + c.defs in L.warn (P.sprintf " Automath representation summary"); - L.warn (P.sprintf " Total book items: %7u" items); - L.warn (P.sprintf " Section items: %7u" c.sections); - L.warn (P.sprintf " Context items: %7u" c.contexts); - L.warn (P.sprintf " Block items: %7u" c.blocks); - L.warn (P.sprintf " Declaration items: %7u" c.decls); - L.warn (P.sprintf " Definition items: %7u" c.defs); + 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 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 9d293a97f..fb02ed2d8 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_item: (counters -> 'a) -> counters -> Aut.item -> 'a +val count_unit: (counters -> 'a) -> counters -> Aut.unit -> '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 c8e836e79..f974b9808 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 } ; - item: + unit: | 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) } ; - items: + units: | { [] } - | item items { $1 :: $2 } + | unit units { $1 :: $2 } ; book: - | items eof { $1 } + | units eof { $1 } ; diff --git a/helm/software/lambda-delta/automath/autProcess.ml b/helm/software/lambda-delta/automath/autProcess.ml index 87fe41865..56ecd4ca4 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_item f st item = match item with - | A.Section section -> proc_section f st section item - | A.Context _ -> proc_context f st item - | A.Block _ -> proc_block f st item - | A.Decl _ -> proc_global f st item - | A.Def _ -> proc_global f st item +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 (* interface functions ******************************************************) @@ -72,6 +72,6 @@ let initial_status = { iao = 0; iar = 0; iac = 0; iag = 0 } -let process_item = proc_item +let process_unit = proc_unit 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 373935e9e..e84f91aee 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_item: (status -> Aut.item -> 'a) -> status -> Aut.item -> 'a +val process_unit: (status -> Aut.unit -> 'a) -> status -> Aut.unit -> '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 32a9b0c5b..3fa4568d1 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 = Item.uri -type id = Item.id +type uri = Unit.uri +type id = Unit.id type bind = Void (* exclusion *) | Abst of term (* abstraction *) @@ -26,9 +26,9 @@ and term = Sort of int (* hierarchy index *) | Appl of term * term (* argument, function *) | Bind of int * id * bind * term (* location, name, binder, scope *) -type obj = bind Item.obj (* age, uri, binder *) +type entry = bind Unit.entry (* age, uri, binder *) -type item = bind Item.item +type unit = bind Unit.unit type lenv = (int * id * bind) list (* location, name, binder *) diff --git a/helm/software/lambda-delta/basic_ag/bagEnvironment.ml b/helm/software/lambda-delta/basic_ag/bagEnvironment.ml index f14566172..35fab4db3 100644 --- a/helm/software/lambda-delta/basic_ag/bagEnvironment.ml +++ b/helm/software/lambda-delta/basic_ag/bagEnvironment.ml @@ -18,7 +18,7 @@ exception ObjectNotFound of B.message let hsize = 7000 let env = H.create hsize -let entry = ref 1 +let age = ref 1 (* Internal functions *******************************************************) @@ -26,10 +26,10 @@ let error uri = raise (ObjectNotFound (L.items1 (U.string_of_uri uri))) (* Interface functions ******************************************************) -let set_obj f obj = - let _, uri, b = obj in - let obj = !entry, uri, b in - incr entry; H.add env uri obj; f obj +let set_entry f entry = + let _, uri, b = entry in + let entry = !age, uri, b in + incr age; H.add env uri entry; f entry -let get_obj f uri = +let get_entry f uri = try f (H.find env uri) with Not_found -> error uri diff --git a/helm/software/lambda-delta/basic_ag/bagEnvironment.mli b/helm/software/lambda-delta/basic_ag/bagEnvironment.mli index 6dc2330c1..ed94f4e8b 100644 --- a/helm/software/lambda-delta/basic_ag/bagEnvironment.mli +++ b/helm/software/lambda-delta/basic_ag/bagEnvironment.mli @@ -11,6 +11,6 @@ exception ObjectNotFound of Bag.message -val set_obj: (Bag.obj -> 'a) -> Bag.obj -> 'a +val set_entry: (Bag.entry -> 'a) -> Bag.entry -> 'a -val get_obj: (Bag.obj -> 'a) -> NUri.uri -> 'a +val get_entry: (Bag.entry -> 'a) -> Bag.uri -> 'a diff --git a/helm/software/lambda-delta/basic_ag/bagOutput.ml b/helm/software/lambda-delta/basic_ag/bagOutput.ml index d6633bcd8..eb3bf05d9 100644 --- a/helm/software/lambda-delta/basic_ag/bagOutput.ml +++ b/helm/software/lambda-delta/basic_ag/bagOutput.ml @@ -62,7 +62,7 @@ and count_term f c = function let f c = count_term_binder f c b in count_term f c t -let count_obj_binder f c = function +let count_entry_binder f c = function | B.Abst w -> let c = {c with eabsts = succ c.eabsts} in count_term f c w @@ -71,11 +71,11 @@ let count_obj_binder f c = function count_term f c v | B.Void -> f c -let count_obj f c (_, _, b) = - count_obj_binder f c b +let count_entry f c (_, _, b) = + count_entry_binder f c b -let count_item f c = function - | Some obj -> count_obj f c obj +let count_unit f c = function + | Some entry -> count_entry f c entry | None -> f c let print_counters f c = diff --git a/helm/software/lambda-delta/basic_ag/bagOutput.mli b/helm/software/lambda-delta/basic_ag/bagOutput.mli index 58c63f110..f3761ac1a 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_item: (counters -> 'a) -> counters -> Bag.item -> 'a +val count_unit: (counters -> 'a) -> counters -> Bag.unit -> 'a val print_counters: (unit -> 'a) -> counters -> 'a diff --git a/helm/software/lambda-delta/basic_ag/bagReduction.ml b/helm/software/lambda-delta/basic_ag/bagReduction.ml index 3aa576a86..628968bef 100644 --- a/helm/software/lambda-delta/basic_ag/bagReduction.ml +++ b/helm/software/lambda-delta/basic_ag/bagReduction.ml @@ -26,7 +26,7 @@ type machine = { type whd_result = | Sort_ of int | LRef_ of int * B.term option - | GRef_ of B.obj + | GRef_ of B.entry | Bind_ of int * B.id * B.term * B.term type ho_whd_result = @@ -83,8 +83,8 @@ let rec whd f c m x = match x with | B.Sort h -> f m (Sort_ h) | B.GRef uri -> - let f obj = f m (GRef_ obj) in - E.get_obj f uri + let f entry = f m (GRef_ entry) in + E.get_entry f uri | B.LRef i -> let f = function | B.Void -> f m (LRef_ (i, None)) diff --git a/helm/software/lambda-delta/basic_ag/bagType.ml b/helm/software/lambda-delta/basic_ag/bagType.ml index 6adcc4087..da808cd45 100644 --- a/helm/software/lambda-delta/basic_ag/bagType.ml +++ b/helm/software/lambda-delta/basic_ag/bagType.ml @@ -68,9 +68,9 @@ let rec b_type_of f ~si g c x = | _, _, B.Abbr (B.Cast (w, v)) -> f x w | _, _, B.Abbr _ -> assert false | _, _, B.Void -> - error1 "reference to excluded object" c x + error1 "reference to excluded entry" c x in - E.get_obj f uri + E.get_entry f uri | B.Bind (l, id, B.Abbr v, t) -> let f xv xt tt = f (S.sh2 v xv t xt x (B.bind_abbr l id)) (B.bind_abbr l id xv tt) diff --git a/helm/software/lambda-delta/basic_ag/bagUntrusted.ml b/helm/software/lambda-delta/basic_ag/bagUntrusted.ml index 69112d2ff..ff5478d9f 100644 --- a/helm/software/lambda-delta/basic_ag/bagUntrusted.ml +++ b/helm/software/lambda-delta/basic_ag/bagUntrusted.ml @@ -20,13 +20,13 @@ module T = BagType let type_check f ?(si=false) g = function | None -> f None None | Some (a, uri, B.Abst t) -> - let f tt obj = f (Some tt) (Some obj) in - let f xt tt = E.set_obj (f tt) (a, uri, B.Abst xt) in + let f tt entry = f (Some tt) (Some entry) in + let f xt tt = E.set_entry (f tt) (a, uri, B.Abst xt) in L.loc := a; T.type_of f ~si g B.empty_lenv t | Some (a, uri, B.Abbr t) -> - let f tt obj = f (Some tt) (Some obj) in - let f xt tt = E.set_obj (f tt) (a, uri, B.Abbr xt) in + let f tt entry = f (Some tt) (Some entry) in + let f xt tt = E.set_entry (f tt) (a, uri, B.Abbr xt) in L.loc := a; T.type_of f ~si g B.empty_lenv t | Some (a, uri, B.Void) -> - let f obj = f None (Some obj) in - L.loc := a; E.set_obj f (a, uri, B.Void) + let f entry = f None (Some entry) in + L.loc := a; E.set_entry f (a, uri, B.Void) diff --git a/helm/software/lambda-delta/basic_ag/bagUntrusted.mli b/helm/software/lambda-delta/basic_ag/bagUntrusted.mli index 3ecd2f0d8..76ba89918 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.item -> 'a) -> ?si:bool -> - Hierarchy.graph -> Bag.item -> 'a + (Bag.term option -> Bag.unit -> 'a) -> ?si:bool -> + Hierarchy.graph -> Bag.unit -> 'a diff --git a/helm/software/lambda-delta/basic_rg/brg.ml b/helm/software/lambda-delta/basic_rg/brg.ml index 52ec4728f..d0a442807 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 = Item.uri -type id = Item.id +type uri = Unit.uri +type id = Unit.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 obj = bind Item.obj (* age, uri, binder *) +type entry = bind Unit.entry (* age, uri, binder *) -type item = bind Item.item +type unit = bind Unit.unit type lenv = Null (* Cons: tail, relative local environment, binder *) diff --git a/helm/software/lambda-delta/basic_rg/brgEnvironment.ml b/helm/software/lambda-delta/basic_rg/brgEnvironment.ml index 29c6dd475..1017092d7 100644 --- a/helm/software/lambda-delta/basic_rg/brgEnvironment.ml +++ b/helm/software/lambda-delta/basic_rg/brgEnvironment.ml @@ -15,16 +15,16 @@ module B = Brg let hsize = 7000 let env = H.create hsize -let entry = ref 1 +let age = ref 1 (* Internal functions *******************************************************) (* Interface functions ******************************************************) -let set_obj f obj = - let _, uri, b = obj in - let obj = !entry, uri, b in - incr entry; H.add env uri obj; f obj +let set_entry f entry = + let _, uri, b = entry in + let entry = !age, uri, b in + incr age; H.add env uri entry; f entry -let get_obj err f uri = +let get_entry err f uri = try f (H.find env uri) with Not_found -> err () diff --git a/helm/software/lambda-delta/basic_rg/brgEnvironment.mli b/helm/software/lambda-delta/basic_rg/brgEnvironment.mli index ee59f37d3..96d6522d9 100644 --- a/helm/software/lambda-delta/basic_rg/brgEnvironment.mli +++ b/helm/software/lambda-delta/basic_rg/brgEnvironment.mli @@ -9,6 +9,6 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) -val set_obj: (Brg.obj -> 'a) -> Brg.obj -> 'a +val set_entry: (Brg.entry -> 'a) -> Brg.entry -> 'a -val get_obj: (unit -> 'a) -> (Brg.obj -> 'a) -> NUri.uri -> 'a +val get_entry: (unit -> 'a) -> (Brg.entry -> 'a) -> Brg.uri -> 'a diff --git a/helm/software/lambda-delta/basic_rg/brgOutput.ml b/helm/software/lambda-delta/basic_rg/brgOutput.ml index 47005ec6d..1a0b0650e 100644 --- a/helm/software/lambda-delta/basic_rg/brgOutput.ml +++ b/helm/software/lambda-delta/basic_rg/brgOutput.ml @@ -88,7 +88,7 @@ and count_term f c e = function let f c = B.push (f c) e b in count_term_binder f c e b -let count_obj f c = function +let count_entry f c = function | (_, u, B.Abst (_, w)) -> let c = {c with eabsts = succ c.eabsts; nodes = succ c.nodes; uris = u :: c.uris @@ -103,8 +103,8 @@ let count_obj f c = function } in f c -let count_item f c = function - | Some obj -> count_obj f c obj +let count_unit f c = function + | Some entry -> count_entry f c entry | None -> f c let print_counters f c = @@ -275,7 +275,7 @@ and exp_bind c frm = function | B.Void a -> F.fprintf frm "" id a -let exp_obj c frm = function +let exp_entry c frm = function | _, u, B.Abst (a, w) -> let str = U.string_of_uri u in let a = B.Name (true, U.name_of_uri u) :: a in @@ -289,5 +289,5 @@ let exp_obj c frm = function let a = B.Name (true, U.name_of_uri u) :: a in F.fprintf frm "" str id a -let export_obj frm obj = - F.fprintf frm "@,@[ %a@]@," (exp_obj B.empty_lenv) obj +let export_entry frm entry = + F.fprintf frm "@,@[ %a@]@," (exp_entry B.empty_lenv) entry diff --git a/helm/software/lambda-delta/basic_rg/brgOutput.mli b/helm/software/lambda-delta/basic_rg/brgOutput.mli index 9a3b58b4a..b9acfd302 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_item: (counters -> 'a) -> counters -> Brg.item -> 'a +val count_unit: (counters -> 'a) -> counters -> Brg.unit -> 'a val print_counters: (unit -> 'a) -> counters -> 'a val specs: (Brg.lenv, Brg.term) Log.specs -val export_obj: Format.formatter -> Brg.bind Item.obj -> unit +val export_entry: Format.formatter -> Brg.bind Unit.entry -> unit diff --git a/helm/software/lambda-delta/basic_rg/brgReduction.ml b/helm/software/lambda-delta/basic_rg/brgReduction.ml index 71a0d1639..e6ea50142 100644 --- a/helm/software/lambda-delta/basic_rg/brgReduction.ml +++ b/helm/software/lambda-delta/basic_rg/brgReduction.ml @@ -18,7 +18,7 @@ module B = Brg module O = BrgOutput module E = BrgEnvironment -type machine = { +type kam = { c: B.lenv; s: (B.lenv * B.term) list; i: int @@ -78,7 +78,7 @@ let rec step f ?(delta=false) ?(rt=false) m x = | e, _, b -> f m (Some (e, b)) x in - E.get_obj C.err f uri + E.get_entry C.err f uri | B.LRef (_, i) -> let f c = function | B.Abbr (_, v) -> @@ -176,7 +176,7 @@ and ac_stacks err f m1 m2 = (* Interface functions ******************************************************) -let empty_machine = { +let empty_kam = { c = B.empty_lenv; s = []; i = 0 } diff --git a/helm/software/lambda-delta/basic_rg/brgReduction.mli b/helm/software/lambda-delta/basic_rg/brgReduction.mli index 2ad3bc522..94f6543e0 100644 --- a/helm/software/lambda-delta/basic_rg/brgReduction.mli +++ b/helm/software/lambda-delta/basic_rg/brgReduction.mli @@ -9,19 +9,19 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) -type machine +type kam -val empty_machine: machine +val empty_kam: kam -val get: (unit -> 'a) -> (Brg.bind -> 'a) -> machine -> int -> 'a +val get: (unit -> 'a) -> (Brg.bind -> 'a) -> kam -> int -> 'a -val push: (machine -> 'a) -> machine -> Brg.bind -> 'a +val push: (kam -> 'a) -> kam -> Brg.bind -> 'a -val xwhd: (machine -> Brg.term -> 'a) -> machine -> Brg.term -> 'a +val xwhd: (kam -> Brg.term -> 'a) -> kam -> Brg.term -> 'a (* arguments: expected type, inferred type *) val are_convertible: (unit -> 'a) -> (unit -> 'a) -> - ?si:bool -> machine -> Brg.term -> machine -> Brg.term -> 'a + ?si:bool -> kam -> Brg.term -> kam -> Brg.term -> 'a -val specs: (machine, Brg.term) Log.specs +val specs: (kam, Brg.term) Log.specs diff --git a/helm/software/lambda-delta/basic_rg/brgSubstitution.mli b/helm/software/lambda-delta/basic_rg/brgSubstitution.mli index 4c5c9c8a7..f20350af6 100644 --- a/helm/software/lambda-delta/basic_rg/brgSubstitution.mli +++ b/helm/software/lambda-delta/basic_rg/brgSubstitution.mli @@ -10,5 +10,6 @@ V_______________________________________________________________ *) val lift: (Brg.term -> 'a) -> int -> int -> Brg.term -> 'a - +(* val lift_bind: (Brg.bind -> 'a) -> int -> int -> Brg.bind -> 'a +*) diff --git a/helm/software/lambda-delta/basic_rg/brgType.ml b/helm/software/lambda-delta/basic_rg/brgType.ml index b26d1b439..cf997e473 100644 --- a/helm/software/lambda-delta/basic_rg/brgType.ml +++ b/helm/software/lambda-delta/basic_rg/brgType.ml @@ -20,9 +20,7 @@ module E = BrgEnvironment module S = BrgSubstitution module R = BrgReduction -type message = (R.machine, B.term) Log.item list - -exception TypeError of message +type message = (R.kam, B.term) Log.message (* Internal functions *******************************************************) @@ -35,8 +33,8 @@ let log1 s m t = let s = s ^ " the term" in L.log R.specs level (message1 s m t) -let error1 s m t = - raise (TypeError (message1 s m t)) +let error1 err s m t = + err (message1 s m t) let message3 m t1 t2 ?mu t3 = let sm, st1, st2 = "In the environment", "the term", "is of type" in @@ -48,23 +46,24 @@ let message3 m t1 t2 ?mu t3 = let st3 = "but it must be of type" in L.et_items3 sm m st1 t1 st2 t2 st3 t3 -let error3 m t1 t2 ?mu t3 = - raise (TypeError (message3 m t1 t2 ?mu t3)) +let error3 err m t1 t2 ?mu t3 = + err (message3 m t1 t2 ?mu t3) -let assert_convertibility f ~si m u w v = - let err _ = error3 m v w u in +let assert_convertibility err f ~si m u w v = + let err _ = error3 err m v w u in R.are_convertible err f ~si m u m w -let assert_applicability f ~si m u w v = +let assert_applicability err f ~si m u w v = let f mu = function + | B.Sort _ -> error1 err "not a function type" m u | B.Bind (B.Abst (_, u), _) -> - let err _ = error3 m v w ~mu u in + let err _ = error3 err m v w ~mu u in R.are_convertible err f ~si mu u m w - | _ -> error1 "not a function type" m u + | _ -> assert false in R.xwhd f m u -let rec b_type_of f ~si g m x = +let rec b_type_of err f ~si g m x = log1 "Now checking" m x; match x with | B.Sort (a, h) -> @@ -77,9 +76,9 @@ let rec b_type_of f ~si g m x = S.lift (f x) (succ i) (0) w | B.Abbr _ -> assert false | B.Void _ -> - error1 "reference to excluded variable" m x + error1 err "reference to excluded variable" m x in - let err _ = error1 "reference to unknown variable" m x in + let err _ = error1 err "reference to unknown variable" m x in R.get err f m i | B.GRef (_, uri) -> let f = function @@ -87,51 +86,51 @@ let rec b_type_of f ~si g m x = | _, _, B.Abbr (_, B.Cast (_, w, _)) -> f x w | _, _, B.Abbr _ -> assert false | _, _, B.Void _ -> - error1 "reference to excluded object" m x + error1 err "reference to excluded entry" m x in - let err _ = error1 "reference to unknown object" m x in - E.get_obj err f uri + let err _ = error1 err "reference to unknown entry" m x in + E.get_entry err f uri | B.Bind (B.Abbr (a, v), t) -> let f xv xt tt = f (A.sh2 v xv t xt x (B.bind_abbr a)) (B.bind_abbr a xv tt) in - let f xv m = b_type_of (f xv) ~si g m t in + let f xv m = b_type_of err (f xv) ~si g m t in let f xv = R.push (f xv) m (B.abbr a xv) in let f xv vv = match xv with | B.Cast _ -> f xv | _ -> f (B.Cast ([], vv, xv)) in - type_of f ~si g m v + type_of err f ~si g m v | B.Bind (B.Abst (a, u), t) -> let f xu xt tt = f (A.sh2 u xu t xt x (B.bind_abst a)) (B.bind_abst a xu tt) in - let f xu m = b_type_of (f xu) ~si g m t in + let f xu m = b_type_of err (f xu) ~si g m t in let f xu _ = R.push (f xu) m (B.abst a xu) in - type_of f ~si g m u + type_of err f ~si g m u | B.Bind (B.Void a as b, t) -> let f xt tt = f (A.sh1 t xt x (B.bind b)) (B.bind b tt) in - let f m = b_type_of f ~si g m t in + let f m = b_type_of err f ~si g m t in R.push f m b | B.Appl (a, v, t) -> let f xv vv xt tt = let f _ = f (A.sh2 v xv t xt x (B.appl a)) (B.appl a xv tt) in - assert_applicability f ~si m tt vv xv + assert_applicability err f ~si m tt vv xv in - let f xv vv = b_type_of (f xv vv) ~si g m t in - type_of f ~si g m v + let f xv vv = b_type_of err (f xv vv) ~si g m t in + type_of err f ~si g m v | B.Cast (a, u, t) -> let f xu xt tt = let f _ = f (A.sh2 u xu t xt x (B.cast a)) xu in - assert_convertibility f ~si m xu tt xt + assert_convertibility err f ~si m xu tt xt in - let f xu _ = b_type_of (f xu) ~si g m t in - type_of f ~si g m u + let f xu _ = b_type_of err (f xu) ~si g m t in + type_of err f ~si g m u (* Interface functions ******************************************************) -and type_of f ?(si=false) g m x = +and type_of err f ?(si=false) g m x = let f t u = L.unbox level; f t u in - L.box level; b_type_of f ~si g m x + L.box level; b_type_of err f ~si g m x diff --git a/helm/software/lambda-delta/basic_rg/brgType.mli b/helm/software/lambda-delta/basic_rg/brgType.mli index 6ee5d57ed..2d7a14663 100644 --- a/helm/software/lambda-delta/basic_rg/brgType.mli +++ b/helm/software/lambda-delta/basic_rg/brgType.mli @@ -9,10 +9,8 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) -type message = (BrgReduction.machine, Brg.term) Log.item list - -exception TypeError of message +type message = (BrgReduction.kam, Brg.term) Log.message val type_of: - (Brg.term -> Brg.term -> 'a) -> ?si:bool -> - Hierarchy.graph -> BrgReduction.machine -> Brg.term -> 'a + (message -> 'a) -> (Brg.term -> Brg.term -> 'a) -> + ?si:bool -> Hierarchy.graph -> BrgReduction.kam -> Brg.term -> 'a diff --git a/helm/software/lambda-delta/basic_rg/brgUntrusted.ml b/helm/software/lambda-delta/basic_rg/brgUntrusted.ml index 67c756b46..20b9a5cf1 100644 --- a/helm/software/lambda-delta/basic_rg/brgUntrusted.ml +++ b/helm/software/lambda-delta/basic_rg/brgUntrusted.ml @@ -18,16 +18,16 @@ module T = BrgType (* Interface functions ******************************************************) (* to share *) -let type_check f ?(si=false) g = function +let type_check err f ?(si=false) g = function | None -> f None None | Some (e, uri, B.Abst (a, t)) -> - let f tt obj = f (Some tt) (Some obj) in - let f xt tt = E.set_obj (f tt) (e, uri, B.abst a xt) in - L.loc := e; T.type_of f ~si g R.empty_machine t + let f tt entry = f (Some tt) (Some entry) in + let f xt tt = E.set_entry (f tt) (e, uri, B.abst a xt) in + L.loc := e; T.type_of err f ~si g R.empty_kam t | Some (e, uri, B.Abbr (a, t)) -> - let f tt obj = f (Some tt) (Some obj) in - let f xt tt = E.set_obj (f tt) (e, uri, B.abbr a xt) in - L.loc := e; T.type_of f ~si g R.empty_machine t + let f tt entry = f (Some tt) (Some entry) in + let f xt tt = E.set_entry (f tt) (e, uri, B.abbr a xt) in + L.loc := e; T.type_of err f ~si g R.empty_kam t | Some (e, uri, (B.Void _ as b)) -> - let f obj = f None (Some obj) in - L.loc := e; E.set_obj f (e, uri, b) + let f entry = f None (Some entry) in + L.loc := e; E.set_entry f (e, uri, b) diff --git a/helm/software/lambda-delta/basic_rg/brgUntrusted.mli b/helm/software/lambda-delta/basic_rg/brgUntrusted.mli index e2066f998..80f9b2eee 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: - (Brg.term option -> Brg.item -> 'a) -> ?si:bool -> - Hierarchy.graph -> Brg.item -> 'a + (BrgType.message -> 'a) -> (Brg.term option -> Brg.unit -> 'a) -> + ?si:bool -> Hierarchy.graph -> Brg.unit -> 'a diff --git a/helm/software/lambda-delta/common/Make b/helm/software/lambda-delta/common/Make index 801c1a84f..ccf9cfd65 100644 --- a/helm/software/lambda-delta/common/Make +++ b/helm/software/lambda-delta/common/Make @@ -1 +1 @@ -hierarchy output item library +hierarchy output unit library diff --git a/helm/software/lambda-delta/common/hierarchy.ml b/helm/software/lambda-delta/common/hierarchy.ml index abe23e10a..375390bdc 100644 --- a/helm/software/lambda-delta/common/hierarchy.ml +++ b/helm/software/lambda-delta/common/hierarchy.ml @@ -16,8 +16,7 @@ module C = Cps type graph = string * (int -> int) let sorts = 2 -let sort = H.create sorts -let index = ref 0 +let sort = H.create sorts (* Internal functions *******************************************************) @@ -26,9 +25,8 @@ let set_sort f (h:int) (s:string) = (* Interface functions ******************************************************) -let set_new_sorts f ss = - let f i = index := i; f i in - C.list_fold_left f set_sort !index ss +let set_sorts f ss i = + C.list_fold_left f set_sort i ss let get_sort err f h = try f (H.find sort h) with Not_found -> err () diff --git a/helm/software/lambda-delta/common/hierarchy.mli b/helm/software/lambda-delta/common/hierarchy.mli index 5bebd28df..a0790321c 100644 --- a/helm/software/lambda-delta/common/hierarchy.mli +++ b/helm/software/lambda-delta/common/hierarchy.mli @@ -11,7 +11,7 @@ type graph -val set_new_sorts: (int -> 'a) -> string list -> 'a +val set_sorts: (int -> 'a) -> string list -> int -> 'a val get_sort: (unit -> 'a) -> (string -> 'a) -> int -> 'a diff --git a/helm/software/lambda-delta/common/library.ml b/helm/software/lambda-delta/common/library.ml index 8dec0dd5d..c60a227e7 100644 --- a/helm/software/lambda-delta/common/library.ml +++ b/helm/software/lambda-delta/common/library.ml @@ -42,15 +42,15 @@ let close_entry frm = (* interface functions ******************************************************) -let export_item export_obj si g = function - | Some obj -> - let _, uri, bind = obj in +let export_unit export_entry si g = function + | Some entry -> + let _, uri, bind = entry in let path = path_of_uri uri in let _ = Sys.command (Printf.sprintf "mkdir -p %s" (F.dirname path)) in let och = open_out (path ^ obj_ext) in let frm = Format.formatter_of_out_channel och in Format.pp_set_margin frm max_int; Format.fprintf frm "@[%t%t%t%a%t@]@." - pp_head pp_doctype (open_entry si g) export_obj obj close_entry; + pp_head pp_doctype (open_entry si g) export_entry entry close_entry; close_out och | None -> () diff --git a/helm/software/lambda-delta/common/library.mli b/helm/software/lambda-delta/common/library.mli index 7e3ee1b82..1a10b6e9d 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_item: - (Format.formatter -> 'bind Item.obj -> unit) -> - bool -> Hierarchy.graph -> 'bind Item.item -> unit +val export_unit: + (Format.formatter -> 'bind Unit.entry -> unit) -> + bool -> Hierarchy.graph -> 'bind Unit.unit -> unit diff --git a/helm/software/lambda-delta/common/item.ml b/helm/software/lambda-delta/common/unit.ml similarity index 87% rename from helm/software/lambda-delta/common/item.ml rename to helm/software/lambda-delta/common/unit.ml index 7e9b7cea8..d76b9d9fe 100644 --- a/helm/software/lambda-delta/common/item.ml +++ b/helm/software/lambda-delta/common/unit.ml @@ -12,6 +12,6 @@ type uri = NUri.uri type id = Aut.id -type 'bind obj = int * uri * 'bind (* age, uri, binder *) +type 'bind entry = int * uri * 'bind (* age, uri, binder *) -type 'bind item = 'bind obj option +type 'bind unit = 'bind entry option diff --git a/helm/software/lambda-delta/toplevel/meta.ml b/helm/software/lambda-delta/toplevel/meta.ml index a7af17273..a3cb08585 100644 --- a/helm/software/lambda-delta/toplevel/meta.ml +++ b/helm/software/lambda-delta/toplevel/meta.ml @@ -9,9 +9,9 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) -type uri = Item.uri +type uri = Unit.uri -type id = Item.id +type id = Unit.id type term = Sort of bool (* sorts: true = TYPE, false = PROP *) | LRef of int * int (* local reference: local environment length, de bruijn index *) @@ -24,4 +24,4 @@ type pars = (id * term) list (* parameter declarations: name, type *) (* entry: line number, parameters, name, type, (transparent?, body) *) type entry = int * pars * uri * term * (bool * term) option -type item = entry option +type unit = entry option diff --git a/helm/software/lambda-delta/toplevel/metaAut.ml b/helm/software/lambda-delta/toplevel/metaAut.ml index 2ef3ec737..335f57fc0 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_item f st = function +let xlate_unit 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_item f st = function let initial_status ?(cover="") () = initial_status hsize cover -let meta_of_aut = xlate_item +let meta_of_aut = xlate_unit diff --git a/helm/software/lambda-delta/toplevel/metaAut.mli b/helm/software/lambda-delta/toplevel/metaAut.mli index b5c7e0b69..79c8fb22b 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.item -> 'a) -> status -> Aut.item -> 'a +val meta_of_aut: (status -> Meta.unit -> 'a) -> status -> Aut.unit -> 'a diff --git a/helm/software/lambda-delta/toplevel/metaBag.ml b/helm/software/lambda-delta/toplevel/metaBag.ml index e0dbf53ae..89c1527c8 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_item f = function +let xlate_unit 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_item +let bag_of_meta = xlate_unit diff --git a/helm/software/lambda-delta/toplevel/metaBag.mli b/helm/software/lambda-delta/toplevel/metaBag.mli index 87e341692..f19f6dd76 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.item -> 'a) -> Meta.item -> 'a +val bag_of_meta: (Bag.unit -> 'a) -> Meta.unit -> 'a diff --git a/helm/software/lambda-delta/toplevel/metaBrg.ml b/helm/software/lambda-delta/toplevel/metaBrg.ml index 9b0ae73db..eff9e9c55 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_item f = function +let xlate_unit 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_item +let brg_of_meta = xlate_unit diff --git a/helm/software/lambda-delta/toplevel/metaBrg.mli b/helm/software/lambda-delta/toplevel/metaBrg.mli index cb47bc9c1..b07ed1253 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.item -> 'a) -> Meta.item -> 'a +val brg_of_meta: (Brg.unit -> 'a) -> Meta.unit -> 'a diff --git a/helm/software/lambda-delta/toplevel/metaLibrary.ml b/helm/software/lambda-delta/toplevel/metaLibrary.ml index e9192f598..a6e780a5f 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_item f (_, frm) item = - O.pp_item f frm item +let write_unit f (_, frm) unit = + O.pp_unit f frm unit 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 d1c723436..26172e46c 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_item: (unit -> 'a) -> out_channel -> Meta.item -> 'a +val write_unit: (unit -> 'a) -> out_channel -> Meta.unit -> '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 4cec084b6..a8560ab18 100644 --- a/helm/software/lambda-delta/toplevel/metaOutput.ml +++ b/helm/software/lambda-delta/toplevel/metaOutput.ml @@ -77,17 +77,17 @@ 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_item f c = function +let count_unit f c = function | Some e -> count_entry f c e | None -> f c let print_counters f c = let terms = c.tsorts + c.tlrefs + c.tgrefs + c.tappls + c.tabsts in let pars = c.pabsts + c.pappls in - let items = c.eabsts + c.eabbrs in + let entries = c.eabsts + c.eabbrs in let nodes = c.nodes + c.xnodes in L.warn (P.sprintf " Intermediate representation summary"); - L.warn (P.sprintf " Total entry items: %7u" items); + L.warn (P.sprintf " Total entries: %7u" entries); L.warn (P.sprintf " Declaration items: %7u" c.eabsts); L.warn (P.sprintf " Definition items: %7u" c.eabbrs); L.warn (P.sprintf " Total parameter items: %7u" pars); @@ -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_item f frm = function +let pp_unit 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 aefb43bef..611e12139 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_item: (counters -> 'a) -> counters -> Meta.item -> 'a +val count_unit: (counters -> 'a) -> counters -> Meta.unit -> 'a val print_counters: (unit -> 'a) -> counters -> 'a -val pp_item: (unit -> 'a) -> Format.formatter -> Meta.item -> 'a +val pp_unit: (unit -> 'a) -> Format.formatter -> Meta.unit -> 'a diff --git a/helm/software/lambda-delta/toplevel/top.ml b/helm/software/lambda-delta/toplevel/top.ml index 13887c6ef..e87bf8a07 100644 --- a/helm/software/lambda-delta/toplevel/top.ml +++ b/helm/software/lambda-delta/toplevel/top.ml @@ -25,7 +25,6 @@ module MBrg = MetaBrg module G = Library module BrgO = BrgOutput module BrgR = BrgReduction -module BrgT = BrgType module BrgU = BrgUntrusted module MBag = MetaBag module BagO = BagOutput @@ -50,8 +49,8 @@ let initial_status cover = { ast = AP.initial_status } -let count count_fun c item = - if !L.level > 2 then count_fun C.start c item else c +let count count_fun c unit = + if !L.level > 2 then count_fun C.start c unit else c let flush () = L.flush 0; L.flush_err () @@ -61,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_item f st = +let process_unit f st = let f ast = f {st with ast = ast} in - AP.process_item f st.ast + AP.process_unit f st.ast (* kernel related ***********************************************************) type kernel = Brg | Bag -type kernel_item = BrgItem of Brg.item - | BagItem of Bag.item +type kernel_unit = Brgunit of Brg.unit + | Bagunit of Bag.unit let kernel = ref Brg @@ -78,30 +77,31 @@ 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 item = match !kernel with +let kernel_of_meta f st unit = match !kernel with | Brg -> - let f item = f st (BrgItem item) in - MBrg.brg_of_meta f item + let f unit = f st (Brgunit unit) in + MBrg.brg_of_meta f unit | Bag -> - let f item = f st (BagItem item) in - MBag.bag_of_meta f item + let f unit = f st (Bagunit unit) in + MBag.bag_of_meta f unit -let count_item st = function - | BrgItem item -> {st with brgc = count BrgO.count_item st.brgc item} - | BagItem item -> {st with bagc = count BagO.count_item st.bagc item} +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 export_item si g = function - | BrgItem item -> G.export_item BrgO.export_obj si g item - | BagItem _ -> () +let export_unit si g = function + | Brgunit unit -> G.export_unit BrgO.export_entry si g unit + | Bagunit _ -> () let type_check f st si g k = + let brg_err msg = brg_error "Type Error" msg; failwith "Interrupted" in let f _ = function - | None -> f st None + | None -> f st None | Some (i, u, _) -> f st (Some (i, u)) in match k with - | BrgItem item -> BrgU.type_check f ~si g item - | BagItem item -> BagU.type_check f ~si g item + | Brgunit unit -> BrgU.type_check brg_err f ~si g unit + | Bagunit unit -> BagU.type_check f ~si g unit (****************************************************************************) @@ -152,7 +152,7 @@ try if !L.level > 0 then T.utime_stamp "parsed"; let rec aux st = function | [] -> st - | item :: tl -> + | unit :: tl -> (* stage 3 *) let f st = function | None -> st @@ -162,31 +162,31 @@ try st in (* stage 2 *) - let f st item = - let st = count_item st item in - if !export then export_item !si !graph item; - if !stage > 2 then type_check f st !si !graph item else st + 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 in (* stage 1 *) - let f st mst item = + let f st mst unit = let st = {st with - mst = mst; mc = count MO.count_item st.mc item + mst = mst; mc = count MO.count_unit st.mc unit } in begin match !moch with | None -> () - | Some och -> ML.write_item C.start och item + | Some och -> ML.write_unit C.start och unit end; - if !stage > 1 then kernel_of_meta f st item else st + if !stage > 1 then kernel_of_meta f st unit else st in (* stage 0 *) - let st = {st with ac = count AO.count_item st.ac item} in - let f st item = + let st = {st with ac = count AO.count_unit st.ac unit} in + let f st unit = let st = - if !stage > 0 then MA.meta_of_aut (f st) st.mst item else st + if !stage > 0 then MA.meta_of_aut (f st) st.mst unit else st in aux st tl in - if !process then process_item f st item else f st item + if !process then process_unit f st unit else f st unit in O.clear_reductions (); let cover = if !use_cover then base_name else "" in @@ -223,7 +223,7 @@ try let help_s = " set translation stage (see above)" in let help_x = " export kernel objects (XML)" in L.box 0; L.box_err (); - H.set_new_sorts ignore ["Set"; "Prop"]; + H.set_sorts ignore ["Set"; "Prop"] 0; at_exit exit; Arg.parse [ ("-S", Arg.Int set_summary, help_S); @@ -240,4 +240,3 @@ try ("-x", Arg.Set export, help_x) ] read_file help; with BagT.TypeError msg -> bag_error "Type Error" msg - | BrgT.TypeError msg -> brg_error "Type Error" msg -- 2.39.2