From 39b42ed90bc74c8b6293842f1ac4aca60fc0c37e Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Fri, 6 Aug 2010 18:23:25 +0000 Subject: [PATCH] we renamed the module abbreviations according to src/modules.ml ld.dtd: now is more strict Makefiles: some refactoring crg: bug fix in name/indexes translation xmlLibrary: bug fix in the rendering of the "name" attribute: ^ is forbidden in a NMTOKEN brgOutput: new xml exportation via xmlCrg --- helm/software/lambda-delta/.depend.opt | 26 +-- helm/software/lambda-delta/Makefile.common | 2 +- .../software/lambda-delta/src/automath/aut.ml | 4 +- .../lambda-delta/src/automath/autLexer.mll | 78 ++++----- .../lambda-delta/src/automath/autOutput.ml | 12 +- .../lambda-delta/src/automath/autParser.mly | 4 +- .../software/lambda-delta/src/basic_ag/bag.ml | 8 +- .../src/basic_ag/bagEnvironment.ml | 16 +- .../lambda-delta/src/basic_ag/bagOutput.ml | 66 +++---- .../lambda-delta/src/basic_ag/bagReduction.ml | 110 ++++++------ .../src/basic_ag/bagSubstitution.ml | 32 ++-- .../lambda-delta/src/basic_ag/bagType.ml | 96 +++++------ .../lambda-delta/src/basic_ag/bagUntrusted.ml | 26 +-- .../software/lambda-delta/src/basic_rg/brg.ml | 10 +- .../lambda-delta/src/basic_rg/brgCrg.ml | 10 +- .../src/basic_rg/brgEnvironment.ml | 12 +- .../lambda-delta/src/basic_rg/brgOutput.ml | 86 +++------- .../lambda-delta/src/basic_rg/brgReduction.ml | 84 ++++----- .../lambda-delta/src/basic_rg/brgType.ml | 63 ++++--- .../lambda-delta/src/basic_rg/brgUntrusted.ml | 28 +-- .../software/lambda-delta/src/common/alpha.ml | 8 +- .../lambda-delta/src/common/entity.ml | 13 +- .../lambda-delta/src/common/hierarchy.ml | 18 +- .../software/lambda-delta/src/common/marks.ml | 4 +- .../lambda-delta/src/common/output.ml | 4 +- .../lambda-delta/src/complete_rg/crg.ml | 29 ++-- .../lambda-delta/src/complete_rg/crgAut.ml | 46 ++--- .../lambda-delta/src/complete_rg/crgOutput.ml | 14 +- .../lambda-delta/src/complete_rg/crgTxt.ml | 26 +-- helm/software/lambda-delta/src/modules.ml | 62 +++++++ helm/software/lambda-delta/src/text/txt.ml | 1 - .../lambda-delta/src/text/txtLexer.mll | 72 ++++---- .../lambda-delta/src/text/txtParser.mly | 4 +- .../lambda-delta/src/toplevel/meta.ml | 8 +- .../lambda-delta/src/toplevel/metaAut.ml | 34 ++-- .../lambda-delta/src/toplevel/metaBag.ml | 28 +-- .../lambda-delta/src/toplevel/metaBrg.ml | 6 +- .../lambda-delta/src/toplevel/metaLibrary.ml | 6 +- .../lambda-delta/src/toplevel/metaOutput.ml | 18 +- .../software/lambda-delta/src/toplevel/top.ml | 161 +++++++++--------- helm/software/lambda-delta/src/xml/xmlCrg.ml | 53 +++--- .../lambda-delta/src/xml/xmlLibrary.ml | 18 +- helm/software/lambda-delta/xml/ld.dtd | 66 ++++--- 43 files changed, 752 insertions(+), 720 deletions(-) create mode 100644 helm/software/lambda-delta/src/modules.ml diff --git a/helm/software/lambda-delta/.depend.opt b/helm/software/lambda-delta/.depend.opt index bc920f171..dcd6c9354 100644 --- a/helm/software/lambda-delta/.depend.opt +++ b/helm/software/lambda-delta/.depend.opt @@ -17,8 +17,8 @@ src/common/output.cmo: src/common/options.cmx src/lib/log.cmi \ src/common/output.cmi src/common/output.cmx: src/common/options.cmx src/lib/log.cmx \ src/common/output.cmi -src/common/entity.cmo: src/common/options.cmx src/automath/aut.cmx -src/common/entity.cmx: src/common/options.cmx src/automath/aut.cmx +src/common/entity.cmo: src/common/options.cmx +src/common/entity.cmx: src/common/options.cmx src/common/marks.cmo: src/common/entity.cmx src/common/marks.cmx: src/common/entity.cmx src/common/alpha.cmi: src/common/entity.cmx @@ -38,8 +38,8 @@ src/text/txtLexer.cmx: src/text/txtParser.cmx src/common/options.cmx \ src/text/txtTxt.cmi: src/text/txt.cmx src/text/txtTxt.cmo: src/text/txt.cmx src/lib/cps.cmx src/text/txtTxt.cmi src/text/txtTxt.cmx: src/text/txt.cmx src/lib/cps.cmx src/text/txtTxt.cmi -src/automath/aut.cmo: -src/automath/aut.cmx: +src/automath/aut.cmo: src/common/entity.cmx +src/automath/aut.cmx: src/common/entity.cmx src/automath/autProcess.cmi: src/automath/aut.cmx src/automath/autProcess.cmo: src/automath/aut.cmx src/automath/autProcess.cmi src/automath/autProcess.cmx: src/automath/aut.cmx src/automath/autProcess.cmi @@ -149,12 +149,14 @@ src/basic_rg/brgCrg.cmx: src/common/marks.cmx src/common/entity.cmx \ src/basic_rg/brgCrg.cmi src/basic_rg/brgOutput.cmi: src/xml/xmlLibrary.cmi src/lib/log.cmi \ src/basic_rg/brg.cmx -src/basic_rg/brgOutput.cmo: src/xml/xmlLibrary.cmi src/common/options.cmx \ +src/basic_rg/brgOutput.cmo: src/xml/xmlCrg.cmi src/common/options.cmx \ src/lib/log.cmi src/common/hierarchy.cmi src/common/entity.cmx \ - src/lib/cps.cmx src/basic_rg/brg.cmx src/basic_rg/brgOutput.cmi -src/basic_rg/brgOutput.cmx: src/xml/xmlLibrary.cmx src/common/options.cmx \ + src/lib/cps.cmx src/basic_rg/brgCrg.cmi src/basic_rg/brg.cmx \ + src/basic_rg/brgOutput.cmi +src/basic_rg/brgOutput.cmx: src/xml/xmlCrg.cmx src/common/options.cmx \ src/lib/log.cmx src/common/hierarchy.cmx src/common/entity.cmx \ - src/lib/cps.cmx src/basic_rg/brg.cmx src/basic_rg/brgOutput.cmi + src/lib/cps.cmx src/basic_rg/brgCrg.cmx src/basic_rg/brg.cmx \ + src/basic_rg/brgOutput.cmi src/basic_rg/brgEnvironment.cmi: src/basic_rg/brg.cmx src/basic_rg/brgEnvironment.cmo: src/common/entity.cmx src/basic_rg/brg.cmx \ src/basic_rg/brgEnvironment.cmi @@ -180,13 +182,13 @@ src/basic_rg/brgType.cmi: src/lib/log.cmi src/common/entity.cmx \ src/basic_rg/brgType.cmo: src/lib/share.cmx src/lib/log.cmi \ src/common/hierarchy.cmi src/common/entity.cmx src/lib/cps.cmx \ src/basic_rg/brgSubstitution.cmi src/basic_rg/brgReduction.cmi \ - src/basic_rg/brgOutput.cmi src/basic_rg/brgEnvironment.cmi \ - src/basic_rg/brg.cmx src/basic_rg/brgType.cmi + src/basic_rg/brgEnvironment.cmi src/basic_rg/brg.cmx \ + src/basic_rg/brgType.cmi src/basic_rg/brgType.cmx: src/lib/share.cmx src/lib/log.cmx \ src/common/hierarchy.cmx src/common/entity.cmx src/lib/cps.cmx \ src/basic_rg/brgSubstitution.cmx src/basic_rg/brgReduction.cmx \ - src/basic_rg/brgOutput.cmx src/basic_rg/brgEnvironment.cmx \ - src/basic_rg/brg.cmx src/basic_rg/brgType.cmi + src/basic_rg/brgEnvironment.cmx src/basic_rg/brg.cmx \ + src/basic_rg/brgType.cmi src/basic_rg/brgUntrusted.cmi: src/common/entity.cmx src/basic_rg/brgType.cmi \ src/basic_rg/brg.cmx src/basic_rg/brgUntrusted.cmo: src/lib/log.cmi src/common/entity.cmx \ diff --git a/helm/software/lambda-delta/Makefile.common b/helm/software/lambda-delta/Makefile.common index c47540bea..e3b12db51 100644 --- a/helm/software/lambda-delta/Makefile.common +++ b/helm/software/lambda-delta/Makefile.common @@ -63,7 +63,7 @@ $(MAIN).opt: $(OBJECTS) $(H)$(OCAMLDEP) $^ > .depend.opt clean: - @echo " CLEAN" + @echo " CLEAN . $(SRC)" $(H)find -name "*~" | xargs $(RM) $(CLEAN) lint: $(XMLS) diff --git a/helm/software/lambda-delta/src/automath/aut.ml b/helm/software/lambda-delta/src/automath/aut.ml index 00213b4b3..7f2ed3cc7 100644 --- a/helm/software/lambda-delta/src/automath/aut.ml +++ b/helm/software/lambda-delta/src/automath/aut.ml @@ -9,7 +9,9 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) -type id = string (* identifier *) +module E = Entity + +type id = E.id type qid = id * bool * id list (* qualified identifier: name, local?, path *) diff --git a/helm/software/lambda-delta/src/automath/autLexer.mll b/helm/software/lambda-delta/src/automath/autLexer.mll index cb33d0c3f..c0bc55afd 100644 --- a/helm/software/lambda-delta/src/automath/autLexer.mll +++ b/helm/software/lambda-delta/src/automath/autLexer.mll @@ -10,11 +10,11 @@ V_______________________________________________________________ *) { - module L = Log - module O = Options - module P = AutParser + module L = Log + module G = Options + module AP = AutParser - let out s = if !O.debug_lexer then L.warn s else () + let out s = if !G.debug_lexer then L.warn s else () (* This turns an Automath identifier into an XML nmtoken *) let quote id = @@ -50,41 +50,41 @@ and token = parse | SPC { token lexbuf } | LC { line_comment lexbuf; token lexbuf } | OC { block_comment lexbuf; token lexbuf } - | "_E" { out "E"; P.E } - | "'_E'" { out "E"; P.E } - | "---" { out "EB"; P.EB } - | "'eb'" { out "EB"; P.EB } - | "EB" { out "EB"; P.EB } - | "--" { out "EXIT"; P.EXIT } - | "PN" { out "PN"; P.PN } - | "'pn'" { out "PN"; P.PN } - | "PRIM" { out "PN"; P.PN } - | "'prim'" { out "PN"; P.PN } - | "???" { out "PN"; P.PN } - | "PROP" { out "PROP"; P.PROP } - | "'prop'" { out "PROP"; P.PROP } - | "TYPE" { out "TYPE"; P.TYPE } - | "'type'" { out "TYPE"; P.TYPE } + | "_E" { out "E"; AP.E } + | "'_E'" { out "E"; AP.E } + | "---" { out "EB"; AP.EB } + | "'eb'" { out "EB"; AP.EB } + | "EB" { out "EB"; AP.EB } + | "--" { out "EXIT"; AP.EXIT } + | "PN" { out "PN"; AP.PN } + | "'pn'" { out "PN"; AP.PN } + | "PRIM" { out "PN"; AP.PN } + | "'prim'" { out "PN"; AP.PN } + | "???" { out "PN"; AP.PN } + | "PROP" { out "PROP"; AP.PROP } + | "'prop'" { out "PROP"; AP.PROP } + | "TYPE" { out "TYPE"; AP.TYPE } + | "'type'" { out "TYPE"; AP.TYPE } | ID { out "ID"; let s = Lexing.lexeme lexbuf in - if !O.unquote then P.IDENT s else P.IDENT (quote s) + if !G.unquote then AP.IDENT s else AP.IDENT (quote s) } - | ":=" { out "DEF"; P.DEF } - | "(" { 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 "AT"; P.AT } - | "~" { out "TD"; P.TD } - | "\"" { out "QT"; P.QT } - | ":" { out "CN"; P.CN } - | "," { out "CM"; P.CM } - | ";" { out "SC"; P.SC } - | "." { out "FS"; P.FS } - | "+" { out "PLUS"; P.PLUS } - | "-" { out "MINUS"; P.MINUS } - | "*" { out "TIMES"; P.TIMES } - | "=" { out "DEF"; P.DEF } - | eof { out "EOF"; P.EOF } + | ":=" { out "DEF"; AP.DEF } + | "(" { out "OP"; AP.OP } + | ")" { out "CP"; AP.CP } + | "[" { out "OB"; AP.OB } + | "]" { out "CB"; AP.CB } + | "<" { out "OA"; AP.OA } + | ">" { out "CA"; AP.CA } + | "@" { out "AT"; AP.AT } + | "~" { out "TD"; AP.TD } + | "\"" { out "QT"; AP.QT } + | ":" { out "CN"; AP.CN } + | "," { out "CM"; AP.CM } + | ";" { out "SC"; AP.SC } + | "." { out "FS"; AP.FS } + | "+" { out "PLUS"; AP.PLUS } + | "-" { out "MINUS"; AP.MINUS } + | "*" { out "TIMES"; AP.TIMES } + | "=" { out "DEF"; AP.DEF } + | eof { out "EOF"; AP.EOF } diff --git a/helm/software/lambda-delta/src/automath/autOutput.ml b/helm/software/lambda-delta/src/automath/autOutput.ml index d692005bd..ddf2f30ed 100644 --- a/helm/software/lambda-delta/src/automath/autOutput.ml +++ b/helm/software/lambda-delta/src/automath/autOutput.ml @@ -9,11 +9,11 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) -module P = Printf -module C = Cps -module L = Log -module A = Aut -module R = AutProcess +module P = Printf +module C = Cps +module L = Log +module A = Aut +module AA = AutProcess type counters = { sections: int; @@ -97,4 +97,4 @@ let print_process_counters f c = L.warn (P.sprintf " Implicit after global: %7u" iag); f () in - R.get_counters f c + AA.get_counters f c diff --git a/helm/software/lambda-delta/src/automath/autParser.mly b/helm/software/lambda-delta/src/automath/autParser.mly index e90ba3b7c..31f2c643c 100644 --- a/helm/software/lambda-delta/src/automath/autParser.mly +++ b/helm/software/lambda-delta/src/automath/autParser.mly @@ -24,10 +24,10 @@ */ %{ - module O = Options + module G = Options module A = Aut - let _ = Parsing.set_trace !O.debug_parser + let _ = Parsing.set_trace !G.debug_parser %} %token NUM %token IDENT diff --git a/helm/software/lambda-delta/src/basic_ag/bag.ml b/helm/software/lambda-delta/src/basic_ag/bag.ml index 1aa9b62e7..d3ac2c8ee 100644 --- a/helm/software/lambda-delta/src/basic_ag/bag.ml +++ b/helm/software/lambda-delta/src/basic_ag/bag.ml @@ -12,8 +12,10 @@ (* kernel version: basic, absolute, global *) (* note : experimental *) -type uri = Entity.uri -type id = Entity.id +module E = Entity + +type uri = E.uri +type id = E.id type bind = Void (* exclusion *) | Abst of term (* abstraction *) @@ -26,7 +28,7 @@ and term = Sort of int (* hierarchy index *) | Appl of term * term (* argument, function *) | Bind of int * id * bind * term (* location, name, binder, scope *) -type entity = term Entity.entity (* attrs, uri, binder *) +type entity = term E.entity (* attrs, uri, binder *) type lenv = (int * id * bind) list (* location, name, binder *) diff --git a/helm/software/lambda-delta/src/basic_ag/bagEnvironment.ml b/helm/software/lambda-delta/src/basic_ag/bagEnvironment.ml index 04681cfee..30e3e992f 100644 --- a/helm/software/lambda-delta/src/basic_ag/bagEnvironment.ml +++ b/helm/software/lambda-delta/src/basic_ag/bagEnvironment.ml @@ -11,14 +11,14 @@ module U = NUri module L = Log -module H = U.UriHash -module Y = Entity -module B = Bag +module K = U.UriHash +module E = Entity +module Z = Bag -exception ObjectNotFound of B.message +exception ObjectNotFound of Z.message let hsize = 7000 -let env = H.create hsize +let env = K.create hsize (* Internal functions *******************************************************) @@ -32,8 +32,8 @@ let error uri = raise (ObjectNotFound (L.items1 (U.string_of_uri uri))) let set_entity f (a, uri, b) = let age = get_age () in - let entry = (Y.Apix age :: a), uri, b in - H.add env uri entry; f entry + let entry = (E.Apix age :: a), uri, b in + K.add env uri entry; f entry let get_entity f uri = - try f (H.find env uri) with Not_found -> error uri + try f (K.find env uri) with Not_found -> error uri diff --git a/helm/software/lambda-delta/src/basic_ag/bagOutput.ml b/helm/software/lambda-delta/src/basic_ag/bagOutput.ml index 0bfc13ee6..de954ed56 100644 --- a/helm/software/lambda-delta/src/basic_ag/bagOutput.ml +++ b/helm/software/lambda-delta/src/basic_ag/bagOutput.ml @@ -13,10 +13,10 @@ module P = Printf module F = Format module U = NUri module L = Log -module O = Options -module Y = Entity +module G = Options +module E = Entity module H = Hierarchy -module B = Bag +module Z = Bag type counters = { eabsts: int; @@ -36,41 +36,41 @@ let initial_counters = { } let rec count_term_binder f c = function - | B.Abst w -> + | Z.Abst w -> let c = {c with tabsts = succ c.tabsts} in count_term f c w - | B.Abbr v -> + | Z.Abbr v -> let c = {c with tabbrs = succ c.tabbrs} in count_term f c v - | B.Void -> f c + | Z.Void -> f c and count_term f c = function - | B.Sort _ -> + | Z.Sort _ -> f {c with tsorts = succ c.tsorts} - | B.LRef _ -> + | Z.LRef _ -> f {c with tlrefs = succ c.tlrefs} - | B.GRef _ -> + | Z.GRef _ -> f {c with tgrefs = succ c.tgrefs} - | B.Cast (v, t) -> + | Z.Cast (v, t) -> let c = {c with tcasts = succ c.tcasts} in let f c = count_term f c t in count_term f c v - | B.Appl (v, t) -> + | Z.Appl (v, t) -> let c = {c with tappls = succ c.tappls} in let f c = count_term f c t in count_term f c v - | B.Bind (_, _, b, t) -> + | Z.Bind (_, _, b, t) -> let f c = count_term_binder f c b in count_term f c t let count_entity f c = function - | _, _, Y.Abst w -> + | _, _, E.Abst w -> let c = {c with eabsts = succ c.eabsts} in count_term f c w - | _, _, Y.Abbr v -> + | _, _, E.Abbr v -> let c = {c with eabbrs = succ c.eabbrs} in count_term f c v - | _, _, Y.Void -> assert false + | _, _, E.Void -> assert false let print_counters f c = let terms = @@ -78,7 +78,7 @@ let print_counters f c = c.tabbrs in let items = c.eabsts + c.eabbrs in - let locations = B.locations () in + let locations = Z.locations () in L.warn (P.sprintf " Kernel representation summary (basic_ag)"); L.warn (P.sprintf " Total entry items: %7u" items); L.warn (P.sprintf " Declaration items: %7u" c.eabsts); @@ -95,50 +95,50 @@ let print_counters f c = f () let res l id = - if !O.indexes then P.sprintf "#%u" l else id + if !G.indexes then P.sprintf "#%u" l else id let rec pp_term c frm = function - | B.Sort h -> + | Z.Sort h -> let err () = F.fprintf frm "@[*%u@]" h in let f s = F.fprintf frm "@[%s@]" s in H.string_of_sort err f h - | B.LRef i -> + | Z.LRef i -> let f = function | Some (id, _) -> F.fprintf frm "@[%s@]" id | None -> F.fprintf frm "@[#%u@]" i in - if !O.indexes then f None else B.get f c i - | B.GRef s -> F.fprintf frm "@[$%s@]" (U.string_of_uri s) - | B.Cast (u, t) -> + if !G.indexes then f None else Z.get f c i + | Z.GRef s -> F.fprintf frm "@[$%s@]" (U.string_of_uri s) + | Z.Cast (u, t) -> F.fprintf frm "@[{%a}.%a@]" (pp_term c) u (pp_term c) t - | B.Appl (v, t) -> + | Z.Appl (v, t) -> F.fprintf frm "@[(%a).%a@]" (pp_term c) v (pp_term c) t - | B.Bind (l, id, B.Abst w, t) -> + | Z.Bind (l, id, Z.Abst w, t) -> let f cc = F.fprintf frm "@[[%s:%a].%a@]" (res l id) (pp_term c) w (pp_term cc) t in - B.push "output abst" f c l id (B.Abst w) - | B.Bind (l, id, B.Abbr v, t) -> + Z.push "output abst" f c l id (Z.Abst w) + | Z.Bind (l, id, Z.Abbr v, t) -> let f cc = F.fprintf frm "@[[%s=%a].%a@]" (res l id) (pp_term c) v (pp_term cc) t in - B.push "output abbr" f c l id (B.Abbr v) - | B.Bind (l, id, B.Void, t) -> + Z.push "output abbr" f c l id (Z.Abbr v) + | Z.Bind (l, id, Z.Void, t) -> let f cc = F.fprintf frm "@[[%s].%a@]" (res l id) (pp_term cc) t in - B.push "output void" f c l id B.Void + Z.push "output void" f c l id Z.Void let pp_lenv frm c = let pp_entry frm = function - | l, id, B.Abst w -> + | l, id, Z.Abst w -> F.fprintf frm "@,@[%s : %a@]" (res l id) (pp_term c) w - | l, id, B.Abbr v -> + | l, id, Z.Abbr v -> F.fprintf frm "@,@[%s = %a@]" (res l id) (pp_term c) v - | l, id, B.Void -> + | l, id, Z.Void -> F.fprintf frm "@,%s" (res l id) in let iter map frm l = List.iter (map frm) l in let f es = F.fprintf frm "%a" (iter pp_entry) (List.rev es) in - B.contents f c + Z.contents f c let specs = { L.pp_term = pp_term; L.pp_lenv = pp_lenv diff --git a/helm/software/lambda-delta/src/basic_ag/bagReduction.ml b/helm/software/lambda-delta/src/basic_ag/bagReduction.ml index b7eb88f63..e2e00e39b 100644 --- a/helm/software/lambda-delta/src/basic_ag/bagReduction.ml +++ b/helm/software/lambda-delta/src/basic_ag/bagReduction.ml @@ -9,57 +9,57 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) -module U = NUri -module C = Cps -module L = Log -module Y = Entity -module B = Bag -module O = BagOutput -module E = BagEnvironment -module S = BagSubstitution +module U = NUri +module C = Cps +module L = Log +module E = Entity +module Z = Bag +module ZO = BagOutput +module ZE = BagEnvironment +module ZS = BagSubstitution type machine = { i: int; - c: B.lenv; - s: B.term list + c: Z.lenv; + s: Z.term list } type whd_result = | Sort_ of int - | LRef_ of int * B.term option - | GRef_ of B.entity - | Bind_ of int * B.id * B.term * B.term + | LRef_ of int * Z.term option + | GRef_ of Z.entity + | Bind_ of int * Z.id * Z.term * Z.term type ho_whd_result = | Sort of int - | Abst of B.term + | Abst of Z.term (* Internal functions *******************************************************) let term_of_whdr = function - | Sort_ h -> B.Sort h - | LRef_ (i, _) -> B.LRef i - | GRef_ (_, uri, _) -> B.GRef uri - | Bind_ (l, id, w, t) -> B.bind_abst l id w t + | Sort_ h -> Z.Sort h + | LRef_ (i, _) -> Z.LRef i + | GRef_ (_, uri, _) -> Z.GRef uri + | Bind_ (l, id, w, t) -> Z.bind_abst l id w t let level = 5 let log1 s c t = let sc, st = s ^ " in the environment", "the term" in - L.log O.specs level (L.et_items1 sc c st t) + L.log ZO.specs level (L.et_items1 sc c st t) let log2 s cu u ct t = let s1, s2, s3 = s ^ " in the environment", "the term", "and in the environment" in - L.log O.specs level (L.et_items2 s1 cu s2 u ~sc2:s3 ~c2:ct s2 t) + L.log ZO.specs level (L.et_items2 s1 cu s2 u ~sc2:s3 ~c2:ct s2 t) -let empty_machine = {i = 0; c = B.empty_lenv; s = []} +let empty_machine = {i = 0; c = Z.empty_lenv; s = []} let inc m = {m with i = succ m.i} let unwind_to_term f m t = - let map f t (l, id, b) = f (B.Bind (l, id, b, t)) in + let map f t (l, id, b) = f (Z.Bind (l, id, b, t)) in let f mc = C.list_fold_left f map t mc in - B.contents f m.c + Z.contents f m.c let unwind_stack f m = let map f v = unwind_to_term f m v in @@ -70,43 +70,43 @@ let get f c m i = | Some (_, b) -> f b | None -> assert false in - let f c = B.get f c i in - B.append f c m.c + let f c = Z.get f c i in + Z.append f c m.c let push msg f c m l id w = assert (m.s = []); - let f w = B.push msg f c l id (B.Abst w) in + let f w = Z.push msg f c l id (Z.Abst w) in unwind_to_term f m w (* to share *) let rec whd f c m x = (* L.warn "entering R.whd"; *) match x with - | B.Sort h -> f m (Sort_ h) - | B.GRef uri -> + | Z.Sort h -> f m (Sort_ h) + | Z.GRef uri -> let f entry = f m (GRef_ entry) in - E.get_entity f uri - | B.LRef i -> + ZE.get_entity f uri + | Z.LRef i -> let f = function - | B.Void -> f m (LRef_ (i, None)) - | B.Abst t -> f m (LRef_ (i, Some t)) - | B.Abbr t -> whd f c m t + | Z.Void -> f m (LRef_ (i, None)) + | Z.Abst t -> f m (LRef_ (i, Some t)) + | Z.Abbr t -> whd f c m t in get f c m i - | B.Cast (_, t) -> whd f c m t - | B.Appl (v, t) -> whd f c {m with s = v :: m.s} t - | B.Bind (l, id, B.Abst w, t) -> + | Z.Cast (_, t) -> whd f c m t + | Z.Appl (v, t) -> whd f c {m with s = v :: m.s} t + | Z.Bind (l, id, Z.Abst w, t) -> begin match m.s with | [] -> f m (Bind_ (l, id, w, t)) | v :: tl -> - let nl = B.new_location () in - let f mc = S.subst (whd f c {m with c = mc; s = tl}) nl l t in - B.push "!" f m.c nl id (B.Abbr (B.Cast (w, v))) + let nl = Z.new_location () in + let f mc = ZS.subst (whd f c {m with c = mc; s = tl}) nl l t in + Z.push "!" f m.c nl id (Z.Abbr (Z.Cast (w, v))) end - | B.Bind (l, id, b, t) -> - let nl = B.new_location () in - let f mc = S.subst (whd f c {m with c = mc}) nl l t in - B.push "!" f m.c nl id b + | Z.Bind (l, id, b, t) -> + let nl = Z.new_location () in + let f mc = ZS.subst (whd f c {m with c = mc}) nl l t in + Z.push "!" f m.c nl id b (* Interface functions ******************************************************) @@ -117,10 +117,10 @@ let rec ho_whd f c m x = | Bind_ (_, _, w, _) -> let f w = f (Abst w) in unwind_to_term f m w | LRef_ (_, Some w) -> ho_whd f c m w - | GRef_ (_, _, Y.Abst w) -> ho_whd f c m w - | GRef_ (_, _, Y.Abbr v) -> ho_whd f c m v + | GRef_ (_, _, E.Abst w) -> ho_whd f c m w + | GRef_ (_, _, E.Abbr v) -> ho_whd f c m v | LRef_ (_, None) -> assert false - | GRef_ (_, _, Y.Void) -> assert false + | GRef_ (_, _, E.Void) -> assert false in whd aux c m x @@ -140,11 +140,11 @@ let rec are_convertible f ~si a c m1 t1 m2 t2 = if h1 = h2 then f a else f false | LRef_ (i1, _), LRef_ (i2, _) -> if i1 = i2 then are_convertible_stacks f ~si a c m1 m2 else f false - | GRef_ ((Y.Apix a1 :: _), _, Y.Abst _), - GRef_ ((Y.Apix a2 :: _), _, Y.Abst _) -> + | GRef_ ((E.Apix a1 :: _), _, E.Abst _), + GRef_ ((E.Apix a2 :: _), _, E.Abst _) -> if a1 = a2 then are_convertible_stacks f ~si a c m1 m2 else f false - | GRef_ ((Y.Apix a1 :: _), _, Y.Abbr v1), - GRef_ ((Y.Apix a2 :: _), _, Y.Abbr v2) -> + | GRef_ ((E.Apix a1 :: _), _, E.Abbr v1), + GRef_ ((E.Apix a2 :: _), _, E.Abbr v2) -> if a1 = a2 then let f a = if a then f a else are_convertible f ~si true c m1 v1 m2 v2 @@ -153,16 +153,16 @@ let rec are_convertible f ~si a c m1 t1 m2 t2 = else if a1 < a2 then whd (aux m1 r1) c m2 v2 else whd (aux_rev m2 r2) c m1 v1 - | _, GRef_ (_, _, Y.Abbr v2) -> + | _, GRef_ (_, _, E.Abbr v2) -> whd (aux m1 r1) c m2 v2 - | GRef_ (_, _, Y.Abbr v1), _ -> + | GRef_ (_, _, E.Abbr v1), _ -> whd (aux_rev m2 r2) c m1 v1 | Bind_ (l1, id1, w1, t1), Bind_ (l2, id2, w2, t2) -> - let l = B.new_location () in + let l = Z.new_location () in let h c = let m1, m2 = inc m1, inc m2 in - let f t1 = S.subst (are_convertible f ~si a c m1 t1 m2) l l2 t2 in - S.subst f l l1 t1 + let f t1 = ZS.subst (are_convertible f ~si a c m1 t1 m2) l l2 t2 in + ZS.subst f l l1 t1 in let f r = if r then push "!" h c m1 l id1 w1 else f false in are_convertible f ~si a c m1 w1 m2 w2 diff --git a/helm/software/lambda-delta/src/basic_ag/bagSubstitution.ml b/helm/software/lambda-delta/src/basic_ag/bagSubstitution.ml index ad75d63b8..46cd95c14 100644 --- a/helm/software/lambda-delta/src/basic_ag/bagSubstitution.ml +++ b/helm/software/lambda-delta/src/basic_ag/bagSubstitution.ml @@ -10,34 +10,34 @@ V_______________________________________________________________ *) module S = Share -module B = Bag +module Z = Bag (* Internal functions *******************************************************) let rec lref_map_bind f map b = match b with - | B.Abbr v -> - let f v' = f (S.sh1 v v' b B.abbr) in + | Z.Abbr v -> + let f v' = f (S.sh1 v v' b Z.abbr) in lref_map f map v - | B.Abst w -> - let f w' = f (S.sh1 w w' b B.abst) in + | Z.Abst w -> + let f w' = f (S.sh1 w w' b Z.abst) in lref_map f map w - | B.Void -> f b + | Z.Void -> f b and lref_map f map t = match t with - | B.LRef i -> - let ii = map i in f (S.sh1 i ii t B.lref) - | B.GRef _ -> f t - | B.Sort _ -> f t - | B.Cast (w, u) -> - let f w' u' = f (S.sh2 w w' u u' t B.cast) in + | Z.LRef i -> + let ii = map i in f (S.sh1 i ii t Z.lref) + | Z.GRef _ -> f t + | Z.Sort _ -> f t + | Z.Cast (w, u) -> + let f w' u' = f (S.sh2 w w' u u' t Z.cast) in let f w' = lref_map (f w') map u in lref_map f map w - | B.Appl (w, u) -> - let f w' u' = f (S.sh2 w w' u u' t B.appl) in + | Z.Appl (w, u) -> + let f w' u' = f (S.sh2 w w' u u' t Z.appl) in let f w' = lref_map (f w') map u in lref_map f map w - | B.Bind (l, id, b, u) -> - let f b' u' = f (S.sh2 b b' u u' t (B.bind l id)) in + | Z.Bind (l, id, b, u) -> + let f b' u' = f (S.sh2 b b' u u' t (Z.bind l id)) in let f b' = lref_map (f b') map u in lref_map_bind f map b diff --git a/helm/software/lambda-delta/src/basic_ag/bagType.ml b/helm/software/lambda-delta/src/basic_ag/bagType.ml index bb4ee83d4..d92e23272 100644 --- a/helm/software/lambda-delta/src/basic_ag/bagType.ml +++ b/helm/software/lambda-delta/src/basic_ag/bagType.ml @@ -9,18 +9,18 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) -module U = NUri -module C = Cps -module S = Share -module L = Log -module Y = Entity -module H = Hierarchy -module B = Bag -module O = BagOutput -module E = BagEnvironment -module R = BagReduction +module U = NUri +module C = Cps +module S = Share +module L = Log +module E = Entity +module H = Hierarchy +module Z = Bag +module ZO = BagOutput +module ZE = BagEnvironment +module ZR = BagReduction -exception TypeError of B.message +exception TypeError of Z.message (* Internal functions *******************************************************) @@ -28,7 +28,7 @@ let level = 4 let log1 s c t = let sc, st = s ^ " in the envireonment", "the term" in - L.log O.specs level (L.et_items1 sc c st t) + L.log ZO.specs level (L.et_items1 sc c st t) let error1 st c t = let sc = "In the envireonment" in @@ -41,8 +41,8 @@ let error3 c t1 t2 t3 = raise (TypeError (L.et_items3 sc c st1 t1 st2 t2 st3 t3)) let mk_gref u l = - let map t v = B.Appl (v, t) in - List.fold_left map (B.GRef u) l + let map t v = Z.Appl (v, t) in + List.fold_left map (Z.GRef u) l (* Interface functions ******************************************************) @@ -50,75 +50,75 @@ let rec b_type_of f st c x = (* L.warn "Entering T.b_type_of"; *) log1 "Now checking" c x; match x with - | B.Sort h -> - let h = H.apply h in f x (B.Sort h) - | B.LRef i -> + | Z.Sort h -> + let h = H.apply h in f x (Z.Sort h) + | Z.LRef i -> let f = function - | Some (_, B.Abst w) -> f x w - | Some (_, B.Abbr (B.Cast (w, v))) -> f x w - | Some (_, B.Abbr _) -> assert false - | Some (_, B.Void) -> + | Some (_, Z.Abst w) -> f x w + | Some (_, Z.Abbr (Z.Cast (w, v))) -> f x w + | Some (_, Z.Abbr _) -> assert false + | Some (_, Z.Void) -> error1 "reference to excluded variable" c x | None -> error1 "variable not found" c x in - B.get f c i - | B.GRef uri -> + Z.get f c i + | Z.GRef uri -> let f = function - | _, _, Y.Abst w -> f x w - | _, _, Y.Abbr (B.Cast (w, v)) -> f x w - | _, _, Y.Abbr _ -> assert false - | _, _, Y.Void -> assert false + | _, _, E.Abst w -> f x w + | _, _, E.Abbr (Z.Cast (w, v)) -> f x w + | _, _, E.Abbr _ -> assert false + | _, _, E.Void -> assert false in - E.get_entity f uri - | B.Bind (l, id, B.Abbr v, t) -> + ZE.get_entity f uri + | Z.Bind (l, id, Z.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) + f (S.sh2 v xv t xt x (Z.bind_abbr l id)) (Z.bind_abbr l id xv tt) in let f xv cc = b_type_of (f xv) st cc t in - let f xv = B.push "type abbr" (f xv) c l id (B.Abbr xv) in + let f xv = Z.push "type abbr" (f xv) c l id (Z.Abbr xv) in let f xv vv = match xv with - | B.Cast _ -> f xv - | _ -> f (B.Cast (vv, xv)) + | Z.Cast _ -> f xv + | _ -> f (Z.Cast (vv, xv)) in type_of f st c v - | B.Bind (l, id, B.Abst u, t) -> + | Z.Bind (l, id, Z.Abst u, t) -> let f xu xt tt = - f (S.sh2 u xu t xt x (B.bind_abst l id)) (B.bind_abst l id xu tt) + f (S.sh2 u xu t xt x (Z.bind_abst l id)) (Z.bind_abst l id xu tt) in let f xu cc = b_type_of (f xu) st cc t in - let f xu _ = B.push "type abst" (f xu) c l id (B.Abst xu) in + let f xu _ = Z.push "type abst" (f xu) c l id (Z.Abst xu) in type_of f st c u - | B.Bind (l, id, B.Void, t) -> + | Z.Bind (l, id, Z.Void, t) -> let f xt tt = - f (S.sh1 t xt x (B.bind l id B.Void)) (B.bind l id B.Void tt) + f (S.sh1 t xt x (Z.bind l id Z.Void)) (Z.bind l id Z.Void tt) in let f cc = b_type_of f st cc t in - B.push "type void" f c l id B.Void - | B.Appl (v, t) -> + Z.push "type void" f c l id Z.Void + | Z.Appl (v, t) -> let f xv vv xt tt = function - | R.Abst w -> + | ZR.Abst w -> L.box (succ level); - L.log O.specs (succ level) (L.t_items1 "Just scanned" c w); + L.log ZO.specs (succ level) (L.t_items1 "Just scanned" c w); L.unbox (succ level); let f a = (* L.warn (Printf.sprintf "Convertible: %b" a); *) - if a then f (S.sh2 v xv t xt x B.appl) (B.appl xv tt) + if a then f (S.sh2 v xv t xt x Z.appl) (Z.appl xv tt) else error3 c xv vv w in - R.are_convertible f ~si:st.Y.si c w vv + ZR.are_convertible f ~si:st.E.si c w vv | _ -> error1 "not a function" c xt in - let f xv vv xt tt = R.ho_whd (f xv vv xt tt) c tt in + let f xv vv xt tt = ZR.ho_whd (f xv vv xt tt) c tt in let f xv vv = b_type_of (f xv vv) st c t in type_of f st c v - | B.Cast (u, t) -> + | Z.Cast (u, t) -> let f xu xt tt a = (* L.warn (Printf.sprintf "Convertible: %b" a); *) - if a then f (S.sh2 u xu t xt x B.cast) xu else error3 c xt tt xu + if a then f (S.sh2 u xu t xt x Z.cast) xu else error3 c xt tt xu in - let f xu xt tt = R.are_convertible (f xu xt tt) ~si:st.Y.si c xu tt in + let f xu xt tt = ZR.are_convertible (f xu xt tt) ~si:st.E.si c xu tt in let f xu _ = b_type_of (f xu) st c t in type_of f st c u diff --git a/helm/software/lambda-delta/src/basic_ag/bagUntrusted.ml b/helm/software/lambda-delta/src/basic_ag/bagUntrusted.ml index 33d6a5fbd..72223f778 100644 --- a/helm/software/lambda-delta/src/basic_ag/bagUntrusted.ml +++ b/helm/software/lambda-delta/src/basic_ag/bagUntrusted.ml @@ -9,21 +9,21 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) -module U = NUri -module L = Log -module Y = Entity -module B = Bag -module E = BagEnvironment -module T = BagType +module U = NUri +module L = Log +module E = Entity +module Z = Bag +module ZE = BagEnvironment +module ZT = BagType (* Interface functions ******************************************************) (* to share *) let type_check f st = function - | a, uri, Y.Abst t -> - let f xt tt = E.set_entity (f tt) (a, uri, Y.Abst xt) in - L.loc := U.string_of_uri uri; T.type_of f st B.empty_lenv t - | a, uri, Y.Abbr t -> - let f xt tt = E.set_entity (f tt) (a, uri, Y.Abbr xt) in - L.loc := U.string_of_uri uri; T.type_of f st B.empty_lenv t - | _, _, Y.Void -> assert false + | a, uri, E.Abst t -> + let f xt tt = ZE.set_entity (f tt) (a, uri, E.Abst xt) in + L.loc := U.string_of_uri uri; ZT.type_of f st Z.empty_lenv t + | a, uri, E.Abbr t -> + let f xt tt = ZE.set_entity (f tt) (a, uri, E.Abbr xt) in + L.loc := U.string_of_uri uri; ZT.type_of f st Z.empty_lenv t + | _, _, E.Void -> assert false diff --git a/helm/software/lambda-delta/src/basic_rg/brg.ml b/helm/software/lambda-delta/src/basic_rg/brg.ml index efc5d7556..d2a0b9987 100644 --- a/helm/software/lambda-delta/src/basic_rg/brg.ml +++ b/helm/software/lambda-delta/src/basic_rg/brg.ml @@ -12,9 +12,11 @@ (* kernel version: basic, relative, global *) (* note : ufficial basic lambda-delta *) -type uri = Entity.uri -type id = Entity.id -type attrs = Entity.attrs +module E = Entity + +type uri = E.uri +type id = E.id +type attrs = E.attrs type bind = Void (* *) | Abst of term (* type *) @@ -27,7 +29,7 @@ and term = Sort of attrs * int (* attrs, hierarchy index *) | Appl of attrs * term * term (* attrs, argument, function *) | Bind of attrs * bind * term (* attrs, binder, scope *) -type entity = term Entity.entity (* attrs, uri, binder *) +type entity = term E.entity (* attrs, uri, binder *) type lenv = Null (* Cons: tail, relative local environment, attrs, binder *) diff --git a/helm/software/lambda-delta/src/basic_rg/brgCrg.ml b/helm/software/lambda-delta/src/basic_rg/brgCrg.ml index 2b3129339..32950e1cf 100644 --- a/helm/software/lambda-delta/src/basic_rg/brgCrg.ml +++ b/helm/software/lambda-delta/src/basic_rg/brgCrg.ml @@ -10,8 +10,8 @@ V_______________________________________________________________ *) module C = Cps -module Y = Entity -module M = Marks +module E = Entity +module J = Marks module D = Crg module B = Brg @@ -25,7 +25,7 @@ let rec lenv_fold_left map1 map2 x = function let rec xlate_term f = function | D.TSort (a, l) -> f (B.Sort (a, l)) | D.TGRef (a, n) -> f (B.GRef (a, n)) - | D.TLRef (a, _, _) -> let f i = f (B.LRef (a, i)) in Y.apix C.err f a + | D.TLRef (a, _, _) -> let f i = f (B.LRef (a, i)) in E.apix C.err f a | D.TCast (a, u, t) -> let f uu tt = f (B.Cast (a, uu, tt)) in let f uu = xlate_term (f uu) t in @@ -44,11 +44,11 @@ let rec xlate_term f = function and xlate_bind x a b = let f a ns = a, ns in - let a, ns = Y.get_names f a in + let a, ns = E.get_names f a in match b with | D.Abst ws -> let map x n w = - let f ww = B.Bind (n :: M.new_mark () :: a, B.Abst ww, x) in + let f ww = B.Bind (n :: J.new_mark () :: a, B.Abst ww, x) in xlate_term f w in List.fold_left2 map x ns ws diff --git a/helm/software/lambda-delta/src/basic_rg/brgEnvironment.ml b/helm/software/lambda-delta/src/basic_rg/brgEnvironment.ml index 121da88da..0b1f1da17 100644 --- a/helm/software/lambda-delta/src/basic_rg/brgEnvironment.ml +++ b/helm/software/lambda-delta/src/basic_rg/brgEnvironment.ml @@ -10,12 +10,12 @@ V_______________________________________________________________ *) module U = NUri -module H = U.UriHash -module Y = Entity +module K = U.UriHash +module E = Entity module B = Brg let hsize = 7000 -let env = H.create hsize +let env = K.create hsize (* Internal functions *******************************************************) @@ -28,8 +28,8 @@ let get_age = (* decps *) let set_entity (a, uri, b) = let age = get_age () in - let entity = (Y.Apix age :: a), uri, b in - H.add env uri entity; entity + let entity = (E.Apix age :: a), uri, b in + K.add env uri entity; entity let get_entity uri = - try H.find env uri with Not_found -> [], uri, Y.Void + try K.find env uri with Not_found -> [], uri, E.Void diff --git a/helm/software/lambda-delta/src/basic_rg/brgOutput.ml b/helm/software/lambda-delta/src/basic_rg/brgOutput.ml index c70bbfec7..d4b851b76 100644 --- a/helm/software/lambda-delta/src/basic_rg/brgOutput.ml +++ b/helm/software/lambda-delta/src/basic_rg/brgOutput.ml @@ -9,16 +9,17 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) -module P = Printf -module F = Format -module C = Cps -module U = NUri -module L = Log -module O = Options -module Y = Entity -module X = XmlLibrary -module H = Hierarchy -module B = Brg +module P = Printf +module F = Format +module C = Cps +module U = NUri +module L = Log +module G = Options +module E = Entity +module H = Hierarchy +module XD = XmlCrg +module B = Brg +module BD = BrgCrg (* nodes count **************************************************************) @@ -88,15 +89,15 @@ and count_term f c e = function count_term_binder f c e b let count_entity f c = function - | _, u, Y.Abst w -> + | _, u, E.Abst w -> let c = {c with eabsts = succ c.eabsts; nodes = succ c.nodes; uris = u :: c.uris } in count_term f c B.empty w - | _, _, Y.Abbr v -> + | _, _, E.Abbr v -> let c = {c with eabbrs = succ c.eabbrs; xnodes = succ c.xnodes} in count_term f c B.empty v - | _, _, Y.Void -> assert false + | _, _, E.Void -> assert false let print_counters f c = let terms = @@ -129,7 +130,7 @@ let rec does_not_occur f n r = function let f n1 r1 = if n1 = n && r1 = r then f false else does_not_occur f n r e in - Y.name C.err f a + E.name C.err f a let rename f e a = let rec aux f e n r = @@ -140,10 +141,10 @@ let rename f e a = does_not_occur f n r e in let f n0 r0 = - let f n r = if n = n0 && r = r0 then f a else f (Y.Name (n, r) :: a) in + let f n r = if n = n0 && r = r0 then f a else f (E.Name (n, r) :: a) in aux f e n0 r0 in - Y.name C.err f a + E.name C.err f a (* lenv/term pretty printing ************************************************) @@ -152,7 +153,7 @@ let name err frm a = | true -> F.fprintf frm "%s" n | false -> F.fprintf frm "^%s" n in - Y.name err f a + E.name err f a let rec pp_term e frm = function | B.Sort (_, h) -> @@ -161,7 +162,7 @@ let rec pp_term e frm = function H.string_of_sort err f h | B.LRef (_, i) -> let err _ = F.fprintf frm "@[#%u@]" i in - if !O.indexes then err () else + if !G.indexes then err () else let _, _, a, b = B.get e i in F.fprintf frm "@[%a@]" (name err) a | B.GRef (_, s) -> @@ -209,50 +210,5 @@ let specs = { (* term xml printing ********************************************************) -let rec exp_term e t out tab = match t with - | B.Sort (a, l) -> - let a = - let err _ = a in - let f s = Y.Name (s, true) :: a in - H.string_of_sort err f l - in - let attrs = [X.position l; X.name a] in - X.tag X.sort attrs out tab - | B.LRef (a, i) -> - let a = - let err _ = a in - let f n r = Y.Name (n, r) :: a in - let _, _, a, b = B.get e i in - Y.name err f a - in - let attrs = [X.position i; X.name a] in - X.tag X.lref attrs out tab - | B.GRef (a, n) -> - let a = Y.Name (U.name_of_uri n, true) :: a in - let attrs = [X.uri n; X.name a] in - X.tag X.gref attrs out tab - | B.Cast (a, u, t) -> - let attrs = [] in - X.tag X.cast attrs ~contents:(exp_term e u) out tab; - exp_term e t out tab - | B.Appl (a, v, t) -> - let attrs = [] in - X.tag X.appl attrs ~contents:(exp_term e v) out tab; - exp_term e t out tab - | B.Bind (a, b, t) -> - let a = rename C.start e a in - exp_bind e a b out tab; - exp_term (B.push e B.empty a b) t out tab - -and exp_bind e a b out tab = match b with - | B.Abst w -> - let attrs = [X.name a; X.mark a] in - X.tag X.abst attrs ~contents:(exp_term e w) out tab - | B.Abbr v -> - let attrs = [X.name a; X.mark a] in - X.tag X.abbr attrs ~contents:(exp_term e v) out tab - | B.Void -> - let attrs = [X.name a; X.mark a] in - X.tag X.void attrs out tab - -let export_term = exp_term B.empty +let export_term = + BD.crg_of_brg XD.export_term diff --git a/helm/software/lambda-delta/src/basic_rg/brgReduction.ml b/helm/software/lambda-delta/src/basic_rg/brgReduction.ml index 03ed05b05..bd78edc26 100644 --- a/helm/software/lambda-delta/src/basic_rg/brgReduction.ml +++ b/helm/software/lambda-delta/src/basic_rg/brgReduction.ml @@ -9,15 +9,15 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) -module U = NUri -module C = Cps -module S = Share -module L = Log -module Y = Entity -module P = Output -module B = Brg -module O = BrgOutput -module E = BrgEnvironment +module U = NUri +module C = Cps +module S = Share +module L = Log +module E = Entity +module O = Output +module B = Brg +module BO = BrgOutput +module BE = BrgEnvironment type kam = { e: B.lenv; (* environment *) @@ -31,11 +31,11 @@ let level = 5 let log1 s c t = let sc, st = s ^ " in the environment", "the term" in - L.log O.specs level (L.et_items1 sc c st t) + L.log BO.specs level (L.et_items1 sc c st t) let log2 s cu u ct t = let s1, s2, s3 = s ^ " in the environment", "the term", "and in the environment" in - L.log O.specs level (L.et_items2 s1 cu s2 u ~sc2:s3 ~c2:ct s2 t) + L.log BO.specs level (L.et_items2 s1 cu s2 u ~sc2:s3 ~c2:ct s2 t) let rec list_and map = function | hd1 :: tl1, hd2 :: tl2 -> @@ -75,35 +75,35 @@ let rec step st m x = match x with | B.Sort _ -> m, None, x | B.GRef (_, uri) -> - begin match E.get_entity uri with - | _, _, Y.Abbr v when st.Y.delta -> - P.add ~gdelta:1 (); step st m v - | _, _, Y.Abst w when st.Y.rt -> - P.add ~grt:1 (); step st m w - | a, _, Y.Abbr v -> - let e = Y.apix C.err C.start a in + begin match BE.get_entity uri with + | _, _, E.Abbr v when st.E.delta -> + O.add ~gdelta:1 (); step st m v + | _, _, E.Abst w when st.E.rt -> + O.add ~grt:1 (); step st m w + | a, _, E.Abbr v -> + let e = E.apix C.err C.start a in m, Some (e, a, B.Abbr v), x - | a, _, Y.Abst w -> - let e = Y.apix C.err C.start a in + | a, _, E.Abst w -> + let e = E.apix C.err C.start a in m, Some (e, a, B.Abst w), x - | _, _, Y.Void -> assert false + | _, _, E.Void -> assert false end | B.LRef (_, i) -> begin match get m i with | c, _, B.Abbr v -> - P.add ~ldelta:1 (); + O.add ~ldelta:1 (); step st {m with e = c} v - | c, _, B.Abst w when st.Y.rt -> - P.add ~lrt:1 (); + | c, _, B.Abst w when st.E.rt -> + O.add ~lrt:1 (); step st {m with e = c} w | c, _, B.Void -> assert false | c, a, (B.Abst _ as b) -> - let e = Y.apix C.err C.start a in + let e = E.apix C.err C.start a in {m with e = c}, Some (e, a, b), x end | B.Cast (_, _, t) -> - P.add ~tau:1 (); + O.add ~tau:1 (); step st m t | B.Appl (_, v, t) -> step st {m with s = (m.e, v) :: m.s} t @@ -111,19 +111,19 @@ let rec step st m x = begin match m.s with | [] -> m, None, x | (c, v) :: s -> - P.add ~beta:1 ~upsilon:(List.length s) (); + O.add ~beta:1 ~upsilon:(List.length s) (); let e = B.push m.e c a (B.abbr v) (* (B.Cast ([], w, v)) *) in step st {m with e = e; s = s} t end | B.Bind (a, b, t) -> - P.add ~upsilon:(List.length m.s) (); + O.add ~upsilon:(List.length m.s) (); let e = B.push m.e m.e a b in step st {m with e = e} t let push m a b = assert (m.s = []); let a, d = match b with - | B.Abst _ -> Y.Apix m.d :: a, succ m.d + | B.Abst _ -> E.Apix m.d :: a, succ m.d | b -> a, m.d in let e = B.push m.e m.e a b in @@ -139,28 +139,28 @@ let rec ac_nfs st (m1, r1, u) (m2, r2, t) = | Some (e1, _, B.Abbr v1), _, Some (e2, _, B.Abbr v2), _ -> if e1 = e2 then if ac_stacks st m1 m2 then true else begin - P.add ~gdelta:2 (); ac st m1 v1 m2 v2 + O.add ~gdelta:2 (); ac st m1 v1 m2 v2 end else if e1 < e2 then begin - P.add ~gdelta:1 (); + O.add ~gdelta:1 (); ac_nfs st (m1, r1, u) (step st m2 v2) end else begin - P.add ~gdelta:1 (); + O.add ~gdelta:1 (); ac_nfs st (step st m1 v1) (m2, r2, t) end | _, _, Some (_, _, B.Abbr v2), _ -> - P.add ~gdelta:1 (); + O.add ~gdelta:1 (); ac_nfs st (m1, r1, u) (step st m2 v2) | Some (_, _, B.Abbr v1), _, _, _ -> - P.add ~gdelta:1 (); + O.add ~gdelta:1 (); ac_nfs st (step st m1 v1) (m2, r2, t) | _, B.Bind (a1, (B.Abst w1 as b1), t1), _, B.Bind (a2, (B.Abst w2 as b2), t2) -> - if ac {st with Y.si = false} m1 w1 m2 w2 then + if ac {st with E.si = false} m1 w1 m2 w2 then ac st (push m1 a1 b1) t1 (push m2 a2 b2) t2 else false - | _, B.Sort _, _, B.Bind (a, b, t) when st.Y.si -> - P.add ~si:1 (); + | _, B.Sort _, _, B.Bind (a, b, t) when st.E.si -> + O.add ~si:1 (); ac st (push m1 a b) u (push m2 a b) t | _ -> false @@ -173,7 +173,7 @@ and ac_stacks st m1 m2 = if List.length m1.s <> List.length m2.s then false else let map (c1, v1) (c2, v2) = let m1, m2 = {m1 with e = c1; s = []}, {m2 with e = c2; s = []} in - ac {st with Y.si = false} m1 v1 m2 v2 + ac {st with E.si = false} m1 v1 m2 v2 in list_and map (m1.s, m2.s) @@ -189,21 +189,21 @@ let get m i = let xwhd st m t = L.box level; log1 "Now scanning" m.e t; - let m, _, t = step {st with Y.delta = true; Y.rt = true} m t in + let m, _, t = step {st with E.delta = true; E.rt = true} m t in L.unbox level; m, t let are_convertible st mu u mw w = L.box level; log2 "Now converting" mu.e u mw.e w; - let r = ac {st with Y.delta = st.Y.expand; Y.rt = false} mu u mw w in + let r = ac {st with E.delta = st.E.expand; E.rt = false} mu u mw w in L.unbox level; r (* let err _ = in if S.eq mu mw then are_alpha_convertible err f u w else err () *) (* error reporting **********************************************************) -let pp_term m frm t = O.specs.L.pp_term m.e frm t +let pp_term m frm t = BO.specs.L.pp_term m.e frm t -let pp_lenv frm m = O.specs.L.pp_lenv frm m.e +let pp_lenv frm m = BO.specs.L.pp_lenv frm m.e let specs = { L.pp_term = pp_term; L.pp_lenv = pp_lenv diff --git a/helm/software/lambda-delta/src/basic_rg/brgType.ml b/helm/software/lambda-delta/src/basic_rg/brgType.ml index 8b119e5e2..5515e4404 100644 --- a/helm/software/lambda-delta/src/basic_rg/brgType.ml +++ b/helm/software/lambda-delta/src/basic_rg/brgType.ml @@ -9,19 +9,18 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) -module U = NUri -module C = Cps -module A = Share -module L = Log -module H = Hierarchy -module Y = Entity -module B = Brg -module O = BrgOutput -module E = BrgEnvironment -module S = BrgSubstitution -module R = BrgReduction +module U = NUri +module C = Cps +module S = Share +module L = Log +module H = Hierarchy +module E = Entity +module B = Brg +module BE = BrgEnvironment +module BS = BrgSubstitution +module BR = BrgReduction -type message = (R.kam, B.term) Log.message +type message = (BR.kam, B.term) Log.message (* Internal functions *******************************************************) @@ -32,7 +31,7 @@ let message1 st1 m t1 = let log1 s m t = let s = s ^ " the term" in - L.log R.specs level (message1 s m t) + L.log BR.specs level (message1 s m t) let error1 err s m t = err (message1 s m t) @@ -51,14 +50,14 @@ let error3 err m t1 t2 ?mu t3 = err (message3 m t1 t2 ?mu t3) let assert_convertibility err f st m u w v = - if R.are_convertible st m u m w then f () else + if BR.are_convertible st m u m w then f () else error3 err m v w u let assert_applicability err f st m u w v = - match R.xwhd st m u with + match BR.xwhd st m u with | _, B.Sort _ -> error1 err "not a function type" m u | mu, B.Bind (_, B.Abst u, _) -> - if R.are_convertible st mu u m w then f () else + if BR.are_convertible st mu u m w then f () else error3 err m v w ~mu u | _ -> assert false (**) @@ -68,29 +67,29 @@ let rec b_type_of err f st m x = | B.Sort (a, h) -> let h = H.apply h in f x (B.Sort (a, h)) | B.LRef (_, i) -> - begin match R.get m i with + begin match BR.get m i with | B.Abst w -> - f x (S.lift (succ i) (0) w) + f x (BS.lift (succ i) (0) w) | B.Abbr (B.Cast (_, w, _)) -> - f x (S.lift (succ i) (0) w) + f x (BS.lift (succ i) (0) w) | B.Abbr _ -> assert false | B.Void -> error1 err "reference to excluded variable" m x end | B.GRef (_, uri) -> - begin match E.get_entity uri with - | _, _, Y.Abst w -> f x w - | _, _, Y.Abbr (B.Cast (_, w, _)) -> f x w - | _, _, Y.Abbr _ -> assert false - | _, _, Y.Void -> + begin match BE.get_entity uri with + | _, _, E.Abst w -> f x w + | _, _, E.Abbr (B.Cast (_, w, _)) -> f x w + | _, _, E.Abbr _ -> assert false + | _, _, E.Void -> error1 err "reference to unknown entry" m x end | B.Bind (a, B.Abbr 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) + f (S.sh2 v xv t xt x (B.bind_abbr a)) (B.bind_abbr a xv tt) in let f xv m = b_type_of err (f xv) st m t in - let f xv = f xv (R.push m a (B.abbr xv)) in + let f xv = f xv (BR.push m a (B.abbr xv)) in let f xv vv = match xv with | B.Cast _ -> f xv | _ -> f (B.Cast ([], vv, xv)) @@ -98,27 +97,27 @@ let rec b_type_of err f st m x = type_of err f st m v | B.Bind (a, B.Abst 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) + f (S.sh2 u xu t xt x (B.bind_abst a)) (B.bind_abst a xu tt) in let f xu m = b_type_of err (f xu) st m t in - let f xu _ = f xu (R.push m a (B.abst xu)) in + let f xu _ = f xu (BR.push m a (B.abst xu)) in type_of err f st m u | B.Bind (a, B.Void, t) -> let f xt tt = - f (A.sh1 t xt x (B.bind_void a)) (B.bind_void a tt) + f (S.sh1 t xt x (B.bind_void a)) (B.bind_void a tt) in - b_type_of err f st (R.push m a B.Void) t + b_type_of err f st (BR.push m a B.Void) t | 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 + let f _ = f (S.sh2 v xv t xt x (B.appl a)) (B.appl a xv tt) in assert_applicability err f st m tt vv xv in let f xv vv = b_type_of err (f xv vv) st m t in type_of err f st 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 + let f _ = f (S.sh2 u xu t xt x (B.cast a)) xu in assert_convertibility err f st m xu tt xt in let f xu _ = b_type_of err (f xu) st m t in diff --git a/helm/software/lambda-delta/src/basic_rg/brgUntrusted.ml b/helm/software/lambda-delta/src/basic_rg/brgUntrusted.ml index 4c1ae61db..160206198 100644 --- a/helm/software/lambda-delta/src/basic_rg/brgUntrusted.ml +++ b/helm/software/lambda-delta/src/basic_rg/brgUntrusted.ml @@ -9,30 +9,30 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) -module U = NUri -module L = Log -module Y = Entity -module B = Brg -module E = BrgEnvironment -module R = BrgReduction -module T = BrgType +module U = NUri +module L = Log +module E = Entity +module B = Brg +module BE = BrgEnvironment +module BR = BrgReduction +module BT = BrgType (* Interface functions ******************************************************) (* to share *) let type_check err f st = function - | a, uri, Y.Abst t -> + | a, uri, E.Abst t -> let f xt tt = - let e = E.set_entity (a, uri, Y.Abst xt) in f tt e + let e = BE.set_entity (a, uri, E.Abst xt) in f tt e in - L.loc := U.string_of_uri uri; T.type_of err f st R.empty_kam t - | a, uri, Y.Abbr t -> + L.loc := U.string_of_uri uri; BT.type_of err f st BR.empty_kam t + | a, uri, E.Abbr t -> let f xt tt = let xt = match xt with | B.Cast _ -> xt | _ -> B.Cast ([], tt, xt) in - let e = E.set_entity (a, uri, Y.Abbr xt) in f tt e + let e = BE.set_entity (a, uri, E.Abbr xt) in f tt e in - L.loc := U.string_of_uri uri; T.type_of err f st R.empty_kam t - | _, _, Y.Void -> assert false + L.loc := U.string_of_uri uri; BT.type_of err f st BR.empty_kam t + | _, _, E.Void -> assert false diff --git a/helm/software/lambda-delta/src/common/alpha.ml b/helm/software/lambda-delta/src/common/alpha.ml index 01c2aafe8..1eb6b1063 100644 --- a/helm/software/lambda-delta/src/common/alpha.ml +++ b/helm/software/lambda-delta/src/common/alpha.ml @@ -9,7 +9,7 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) -module Y = Entity +module E = Entity (* internal functions *******************************************************) @@ -21,10 +21,10 @@ let rec rename ns n = let alpha_name acc attr = let ns, a = acc in match attr with - | Y.Name n -> + | E.Name n -> if List.mem n ns then let n = rename ns n in - n :: ns, Y.Name n :: a + n :: ns, E.Name n :: a else n :: ns, attr :: a | _ -> assert false @@ -36,4 +36,4 @@ let alpha ns a = let _, names = List.fold_left alpha_name (ns, []) (List.rev names) in List.rev_append a names in - Y.get_names f a + E.get_names f a diff --git a/helm/software/lambda-delta/src/common/entity.ml b/helm/software/lambda-delta/src/common/entity.ml index e32b347a8..6da0b3aeb 100644 --- a/helm/software/lambda-delta/src/common/entity.ml +++ b/helm/software/lambda-delta/src/common/entity.ml @@ -9,10 +9,13 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) -module O = Options +module U = NUri +module G = Options + +type uri = U.uri + +type id = string (* identifier *) -type uri = NUri.uri -type id = Aut.id type name = id * bool (* token, real? *) type names = name list @@ -118,10 +121,10 @@ let xlate f xlate_term = function assert false let initial_status () = { - delta = false; rt = false; si = !O.si; expand = !O.expand + delta = false; rt = false; si = !G.si; expand = !G.expand } let refresh_status st = {st with - si = !O.si; expand = !O.expand + si = !G.si; expand = !G.expand } diff --git a/helm/software/lambda-delta/src/common/hierarchy.ml b/helm/software/lambda-delta/src/common/hierarchy.ml index b7d428353..28d95cc82 100644 --- a/helm/software/lambda-delta/src/common/hierarchy.ml +++ b/helm/software/lambda-delta/src/common/hierarchy.ml @@ -9,28 +9,28 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) -module H = Hashtbl -module S = Scanf +module K = Hashtbl +module P = Scanf module C = Cps type graph = string * (int -> int) let sorts = 3 -let sort = H.create sorts +let sort = K.create sorts let default_graph = "Z1" (* Internal functions *******************************************************) let set_sort h s = - H.add sort h s; succ h + K.add sort h s; succ h let graph_of_string err f s = try - let x = S.sscanf s "Z%u" C.start in + let x = P.sscanf s "Z%u" C.start in if x > 0 then f (s, fun h -> x + h) else err () with - S.Scan_failure _ | Failure _ | End_of_file -> err () + P.Scan_failure _ | Failure _ | End_of_file -> err () let graph = ref (graph_of_string C.err C.start default_graph) @@ -40,14 +40,14 @@ let set_sorts i ss = List.fold_left set_sort i ss let string_of_sort err f h = - try f (H.find sort h) with Not_found -> err () + try f (K.find sort h) with Not_found -> err () let sort_of_string err f s = let map h n = function | None when n = s -> Some h | xh -> xh in - match H.fold map sort None with + match K.fold map sort None with | None -> err () | Some h -> f h @@ -61,4 +61,4 @@ let set_graph s = graph_of_string err f s let clear () = - H.clear sort; graph := graph_of_string C.err C.start default_graph + K.clear sort; graph := graph_of_string C.err C.start default_graph diff --git a/helm/software/lambda-delta/src/common/marks.ml b/helm/software/lambda-delta/src/common/marks.ml index 026414e2a..a9b78762a 100644 --- a/helm/software/lambda-delta/src/common/marks.ml +++ b/helm/software/lambda-delta/src/common/marks.ml @@ -9,7 +9,7 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) -module Y = Entity +module E = Entity (* interface functions ******************************************************) @@ -18,4 +18,4 @@ let new_location = fun () -> incr location; !location let new_mark () = - Y.Mark (new_location ()) + E.Mark (new_location ()) diff --git a/helm/software/lambda-delta/src/common/output.ml b/helm/software/lambda-delta/src/common/output.ml index 8270c5d97..38ebf8a34 100644 --- a/helm/software/lambda-delta/src/common/output.ml +++ b/helm/software/lambda-delta/src/common/output.ml @@ -11,7 +11,7 @@ module P = Printf module L = Log -module O = Options +module G = Options type reductions = { beta : int; @@ -69,4 +69,4 @@ let print_reductions () = L.warn (P.sprintf " Local: %7u" r.lrt); L.warn (P.sprintf " Global: %7u" r.grt); L.warn (P.sprintf " Sort inclusion: %7u" r.si); - L.warn (P.sprintf " Relocated nodes (icm): %7u" !O.icm) + L.warn (P.sprintf " Relocated nodes (icm): %7u" !G.icm) diff --git a/helm/software/lambda-delta/src/complete_rg/crg.ml b/helm/software/lambda-delta/src/complete_rg/crg.ml index 07a4cb3ee..cc93d6dc3 100644 --- a/helm/software/lambda-delta/src/complete_rg/crg.ml +++ b/helm/software/lambda-delta/src/complete_rg/crg.ml @@ -12,11 +12,11 @@ (* kernel version: complete, relative, global *) (* note : fragment of complete lambda-delta serving as abstract layer *) -module Y = Entity +module E = Entity -type uri = Y.uri -type id = Y.id -type attrs = Y.attrs +type uri = E.uri +type id = E.id +type attrs = E.attrs type bind = Abst of term list (* domains *) | Abbr of term list (* bodies *) @@ -34,7 +34,7 @@ and lenv = ESort (* top *) | EProj of lenv * attrs * lenv (* environment, attrs, closure *) | EBind of lenv * attrs * bind (* environment, attrs, binder *) -type entity = term Y.entity +type entity = term E.entity (* helpers ******************************************************************) @@ -58,19 +58,25 @@ let push2 err f lenv attr ?t () = match lenv, t with let resolve_lref err f id lenv = let rec aux f i k = function | ESort -> err () + | EBind (tl, _, Abst []) + | EBind (tl, _, Abbr []) + | EBind (tl, _, Void 0) -> aux f i k tl | EBind (tl, a, _) -> let err kk = aux f (succ i) (k + kk) tl in let f j = f i j (k + j) in - Y.resolve err f id a + E.resolve err f id a | EProj _ -> assert false (* TODO *) in aux f 0 0 lenv let rec get_name err f i j = function | ESort -> err i + | EBind (tl, _, Abst []) + | EBind (tl, _, Abbr []) + | EBind (tl, _, Void 0) -> get_name err f i j tl | EBind (_, a, _) when i = 0 -> let err () = err i in - Y.get_name err f j a + E.get_name err f j a | EBind (tl, _, _) -> get_name err f (pred i) j tl | EProj (tl, _, e) -> @@ -80,15 +86,18 @@ let rec get_name err f i j = function let get_index err f i j lenv = let rec aux f i k = function | ESort -> err i + | EBind (tl, _, Abst []) + | EBind (tl, _, Abbr []) + | EBind (tl, _, Void 0) -> aux f i k tl | EBind (_, a, _) when i = 0 -> - if Y.count_names a > j then f (k + j) else err i + if E.count_names a > j then f (k + j) else err i | EBind (tl, a, _) -> - aux f (pred i) (k + Y.count_names a) tl + aux f (pred i) (k + E.count_names a) tl | EProj _ -> assert false (* TODO *) in aux f i 0 lenv let rec names_of_lenv ns = function | ESort -> ns - | EBind (tl, a, _) -> names_of_lenv (Y.rev_append_names ns a) tl + | EBind (tl, a, _) -> names_of_lenv (E.rev_append_names ns a) tl | EProj (tl, _, e) -> names_of_lenv (names_of_lenv ns e) tl diff --git a/helm/software/lambda-delta/src/complete_rg/crgAut.ml b/helm/software/lambda-delta/src/complete_rg/crgAut.ml index 0b95adf41..2221c3c06 100644 --- a/helm/software/lambda-delta/src/complete_rg/crgAut.ml +++ b/helm/software/lambda-delta/src/complete_rg/crgAut.ml @@ -10,17 +10,17 @@ V_______________________________________________________________ *) module U = NUri -module H = U.UriHash +module K = U.UriHash module C = Cps -module O = Options -module Y = Entity +module G = Options +module E = Entity module A = Aut module D = Crg (* qualified identifier: uri, name, qualifiers *) type qid = D.uri * D.id * D.id list -type context = Y.attrs * D.term list +type context = E.attrs * D.term list type context_node = qid option (* context node: None = root *) @@ -29,7 +29,7 @@ type status = { node: context_node; (* current context node *) nodes: context_node list; (* context node list *) line: int; (* line number *) - mk_uri:O.uri_generator (* uri generator *) + mk_uri:G.uri_generator (* uri generator *) } type resolver = Local of int @@ -37,21 +37,21 @@ type resolver = Local of int let henv_size, hcnt_size = 7000, 4300 (* hash tables initial sizes *) -let henv = H.create henv_size (* optimized global environment *) +let henv = K.create henv_size (* optimized global environment *) -let hcnt = H.create hcnt_size (* optimized context *) +let hcnt = K.create hcnt_size (* optimized context *) (* Internal functions *******************************************************) let empty_cnt = [], [] let add_abst (a, ws) id w = - Y.Name (id, true) :: a, w :: ws + E.Name (id, true) :: a, w :: ws let lenv_of_cnt (a, ws) = D.push_bind C.start D.empty_lenv a (D.Abst ws) -let mk_lref f i j k = f (D.TLRef ([Y.Apix k], i, j)) +let mk_lref f i j k = f (D.TLRef ([E.Apix k], i, j)) let id_of_name (id, _, _) = id @@ -84,7 +84,7 @@ let relax_opt_qid f st = function | Some qid -> let f qid = f (Some qid) in relax_qid f st qid let resolve_gref err f st qid = - try let cnt = H.find henv (uri_of_qid qid) in f qid cnt + try let cnt = K.find henv (uri_of_qid qid) in f qid cnt with Not_found -> err qid let resolve_gref_relaxed f st qid = @@ -95,7 +95,7 @@ let resolve_gref_relaxed f st qid = let get_cnt err f st = function | None -> f empty_cnt | Some qid as node -> - try let cnt = H.find hcnt (uri_of_qid qid) in f cnt + try let cnt = K.find hcnt (uri_of_qid qid) in f cnt with Not_found -> err node let get_cnt_relaxed f st = @@ -114,7 +114,7 @@ let rec xlate_term f st lenv = function xlate_term f st lenv v | A.Abst (name, w, t) -> let f ww = - let a, b = [Y.Name (name, true)], (D.Abst [ww]) in + let a, b = [E.Name (name, true)], (D.Abst [ww]) in let f tt = f (D.TBind (a, b, tt)) in let f lenv = xlate_term f st lenv t in D.push_bind f lenv a b @@ -122,7 +122,7 @@ let rec xlate_term f st lenv = function xlate_term f st lenv w | A.GRef (name, args) -> let map1 f = function - | Y.Name (id, _) -> f (A.GRef ((id, true, []), [])) + | E.Name (id, _) -> f (A.GRef ((id, true, []), [])) | _ -> C.err () in let map2 f = xlate_term f st lenv in @@ -159,7 +159,7 @@ let xlate_entity err f st = function let f cnt = let lenv = lenv_of_cnt cnt in let ww = xlate_term C.start st lenv w in - H.add hcnt (uri_of_qid qid) (add_abst cnt name ww); + K.add hcnt (uri_of_qid qid) (add_abst cnt name ww); err {st with node = Some qid} in get_cnt_relaxed f st @@ -171,7 +171,7 @@ let xlate_entity err f st = function let lenv = lenv_of_cnt cnt in let f qid = let ww = xlate_term C.start st lenv w in - H.add henv (uri_of_qid qid) cnt; + K.add henv (uri_of_qid qid) cnt; let t = match ws with | [] -> ww | _ -> D.TBind (a, D.Abst ws, ww) @@ -179,8 +179,8 @@ let xlate_entity err f st = function (* print_newline (); CrgOutput.pp_term print_string t; *) - let b = Y.Abst t in - let entity = [Y.Mark st.line], uri_of_qid qid, b in + let b = E.Abst t in + let entity = [E.Mark st.line], uri_of_qid qid, b in f {st with line = succ st.line} entity in complete_qid f st (name, true, []) @@ -193,7 +193,7 @@ let xlate_entity err f st = function let f qid = let ww = xlate_term C.start st lenv w in let vv = xlate_term C.start st lenv v in - H.add henv (uri_of_qid qid) cnt; + K.add henv (uri_of_qid qid) cnt; let t = match ws with | [] -> D.TCast ([], ww, vv) | _ -> D.TBind (a, D.Abst ws, D.TCast ([], ww, vv)) @@ -201,8 +201,8 @@ let xlate_entity err f st = function (* print_newline (); CrgOutput.pp_term print_string t; *) - let b = Y.Abbr t in - let a = Y.Mark st.line :: if trans then [] else [Y.Priv] in + let b = E.Abbr t in + let a = E.Mark st.line :: if trans then [] else [E.Priv] in let entity = a, uri_of_qid qid, b in f {st with line = succ st.line} entity in @@ -213,12 +213,12 @@ let xlate_entity err f st = function (* Interface functions ******************************************************) let initial_status () = - H.clear henv; H.clear hcnt; { - path = []; node = None; nodes = []; line = 1; mk_uri = O.get_mk_uri () + K.clear henv; K.clear hcnt; { + path = []; node = None; nodes = []; line = 1; mk_uri = G.get_mk_uri () } let refresh_status st = {st with - mk_uri = O.get_mk_uri () + mk_uri = G.get_mk_uri () } let crg_of_aut = xlate_entity diff --git a/helm/software/lambda-delta/src/complete_rg/crgOutput.ml b/helm/software/lambda-delta/src/complete_rg/crgOutput.ml index 6da54cbc3..efa39eec6 100644 --- a/helm/software/lambda-delta/src/complete_rg/crgOutput.ml +++ b/helm/software/lambda-delta/src/complete_rg/crgOutput.ml @@ -13,19 +13,19 @@ module P = Printf module U = NUri module C = Cps module H = Hierarchy -module Y = Entity +module E = Entity module D = Crg (****************************************************************************) let pp_attrs out a = let map = function - | Y.Name (s, true) -> out (P.sprintf "%s;" s) - | Y.Name (s, false) -> out (P.sprintf "~%s;" s) - | Y.Apix i -> out (P.sprintf "+%i;" i) - | Y.Mark i -> out (P.sprintf "@%i;" i) - | Y.Meta s -> out (P.sprintf "\"%s\";" s) - | Y.Priv -> out (P.sprintf "%s;" "~") + | E.Name (s, true) -> out (P.sprintf "%s;" s) + | E.Name (s, false) -> out (P.sprintf "~%s;" s) + | E.Apix i -> out (P.sprintf "+%i;" i) + | E.Mark i -> out (P.sprintf "@%i;" i) + | E.Meta s -> out (P.sprintf "\"%s\";" s) + | E.Priv -> out (P.sprintf "%s;" "~") in List.iter map a diff --git a/helm/software/lambda-delta/src/complete_rg/crgTxt.ml b/helm/software/lambda-delta/src/complete_rg/crgTxt.ml index 34727aff9..75aef2ae1 100644 --- a/helm/software/lambda-delta/src/complete_rg/crgTxt.ml +++ b/helm/software/lambda-delta/src/complete_rg/crgTxt.ml @@ -12,8 +12,8 @@ module U = NUri module H = Hierarchy module C = Cps -module O = Options -module Y = Entity +module G = Options +module E = Entity module T = Txt module TT = TxtTxt module D = Crg @@ -22,7 +22,7 @@ type status = { path : T.id list; (* current section path *) line : int; (* line number *) sort : int; (* first default sort index *) - mk_uri: O.uri_generator (* uri generator *) + mk_uri: G.uri_generator (* uri generator *) } let henv_size = 7000 (* hash tables initial size *) @@ -31,9 +31,9 @@ let henv = Hashtbl.create henv_size (* optimized global environment *) (* Internal functions *******************************************************) -let name_of_id ?(r=true) id = Y.Name (id, r) +let name_of_id ?(r=true) id = E.Name (id, r) -let mk_lref f i j k = f (D.TLRef ([Y.Apix k], i, j)) +let mk_lref f i j k = f (D.TLRef ([E.Apix k], i, j)) let mk_gref f uri = f (D.TGRef ([], uri)) @@ -105,10 +105,10 @@ let xlate_term f st lenv t = TT.contract (xlate_term f st lenv) t let mk_contents tt = function - | T.Decl -> [], Y.Abst tt - | T.Ax -> [], Y.Abst tt - | T.Def -> [], Y.Abbr tt - | T.Th -> [], Y.Abbr tt + | T.Decl -> [], E.Abst tt + | T.Ax -> [], E.Abst tt + | T.Def -> [], E.Abbr tt + | T.Th -> [], E.Abbr tt let xlate_entity err f gen st = function | T.Require _ -> @@ -140,8 +140,8 @@ let xlate_entity err f gen st = function print_newline (); CrgOutput.pp_term print_string tt; *) let a, b = mk_contents tt kind in - let a = if meta <> "" then Y.Meta meta :: a else a in - let entity = Y.Mark st.line :: a, uri, b in + let a = if meta <> "" then E.Meta meta :: a else a in + let entity = E.Mark st.line :: a, uri, b in f {st with line = succ st.line} entity | T.Generate _ -> err st @@ -150,11 +150,11 @@ let xlate_entity err f gen st = function let initial_status () = Hashtbl.clear henv; { - path = []; line = 1; sort = 0; mk_uri = O.get_mk_uri () + path = []; line = 1; sort = 0; mk_uri = G.get_mk_uri () } let refresh_status st = {st with - mk_uri = O.get_mk_uri () + mk_uri = G.get_mk_uri () } let crg_of_txt = xlate_entity diff --git a/helm/software/lambda-delta/src/modules.ml b/helm/software/lambda-delta/src/modules.ml new file mode 100644 index 000000000..f48cf6ffc --- /dev/null +++ b/helm/software/lambda-delta/src/modules.ml @@ -0,0 +1,62 @@ +(* free = F I N P Q U V W *) + +module U = NUri +module K = NUri.UriHash + +module C = cps +module S = share +module L = log +module Y = time (**) + +module G = options +module H = hierarchy +module O = output +module E = entity +module J = marks (**) +module R = alpha + +module T = txt +module TP = txtParser +module TL = txtLexer +module TT = txtTxt + +module A = aut +module AA = autProcess +module AO = autOutput +module AP = autParser +module AL = autLexer + +module Z = bag +module ZO = bagOutput +module ZE = bagEnvironment +module ZS = bagSubstitution +module ZR = bagReduction +module ZT = bagType +module ZU = bagUntrusted + +module D = crg +module DO = crgOutput +module TD = crgTxt +module AD = crgAut + +module XL = xmlLibrary +module XD = xmlCrg + +module B = brg +module BD = brgCrg +module BO = brgOutput +module BE = brgEnvironment +module BS = brgSubstitution +module BR = brgReduction +module BT = brgType +module BU = brgUntrusted + +module M = meta +module MO = metaOutput +module ML = metaLibrary +module MA = metaAut +module MZ = metaBag +module MB = metaBrg +(* + top +*) diff --git a/helm/software/lambda-delta/src/text/txt.ml b/helm/software/lambda-delta/src/text/txt.ml index dbcc0675c..a2140585a 100644 --- a/helm/software/lambda-delta/src/text/txt.ml +++ b/helm/software/lambda-delta/src/text/txt.ml @@ -40,4 +40,3 @@ type command = Require of id list (* required files: names *) | Section of id option (* section: Some id = open, None = close last *) | Entity of kind * id * desc * term (* entity: class, name, description, contents *) | Generate of term list (* predefined generated entity: arguments *) - diff --git a/helm/software/lambda-delta/src/text/txtLexer.mll b/helm/software/lambda-delta/src/text/txtLexer.mll index dc293bdcf..e5ced3806 100644 --- a/helm/software/lambda-delta/src/text/txtLexer.mll +++ b/helm/software/lambda-delta/src/text/txtLexer.mll @@ -10,11 +10,11 @@ V_______________________________________________________________ *) { - module L = Log - module O = Options - module P = TxtParser + module L = Log + module G = Options + module TP = TxtParser - let out s = if !O.debug_lexer then L.warn s else () + let out s = if !G.debug_lexer then L.warn s else () } let BS = "\\" @@ -38,35 +38,35 @@ and qstring = parse | BS QT { "\"" ^ qstring lexbuf } | _ as c { String.make 1 c ^ qstring lexbuf } and token = parse - | SPC { token lexbuf } - | OC { block_comment lexbuf; token lexbuf } - | ID as id { out ("ID " ^ id); P.ID id } - | IX as ix { out ("IX " ^ ix); P.IX (int_of_string ix) } - | QT { let s = qstring lexbuf in out ("STR " ^ s); 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 } - | "\\generate" { out "GEN"; P.GEN } - | "\\require" { out "REQ"; P.REQ } - | "\\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 " ^ id); TP.ID id } + | IX as ix { out ("IX " ^ ix); TP.IX (int_of_string ix) } + | QT { let s = qstring lexbuf in out ("STR " ^ s); TP.STR s } + | "\\graph" { out "GRAPH"; TP.GRAPH } + | "\\decl" { out "DECL"; TP.DECL } + | "\\ax" { out "AX"; TP.AX } + | "\\def" { out "DEF"; TP.DEF } + | "\\th" { out "TH"; TP.TH } + | "\\generate" { out "GEN"; TP.GEN } + | "\\require" { out "REQ"; TP.REQ } + | "\\open" { out "OPEN"; TP.OPEN } + | "\\close" { out "CLOSE"; TP.CLOSE } + | "\\sorts" { out "SORTS"; TP.SORTS } + | "(" { out "OP"; TP.OP } + | ")" { out "CP"; TP.CP } + | "[" { out "OB"; TP.OB } + | "]" { out "CB"; TP.CB } + | "<" { out "OA"; TP.OA } + | ">" { out "CA"; TP.CA } + | "." { out "FS"; TP.FS } + | ":" { out "CN"; TP.CN } + | "," { out "CM"; TP.CM } + | "=" { out "EQ"; TP.EQ } + | "*" { out "STAR"; TP.STAR } + | "#" { out "HASH"; TP.HASH } + | "+" { out "PLUS"; TP.PLUS } + | "~" { out "TE"; TP.TE } + | "->" { out "WTO"; TP.WTO } + | "=>" { out "STO"; TP.STO } + | eof { out "EOF"; TP.EOF } diff --git a/helm/software/lambda-delta/src/text/txtParser.mly b/helm/software/lambda-delta/src/text/txtParser.mly index 694e30891..415b594ca 100644 --- a/helm/software/lambda-delta/src/text/txtParser.mly +++ b/helm/software/lambda-delta/src/text/txtParser.mly @@ -24,10 +24,10 @@ */ %{ - module O = Options + module G = Options module T = Txt - let _ = Parsing.set_trace !O.debug_parser + let _ = Parsing.set_trace !G.debug_parser %} %token IX %token ID STR diff --git a/helm/software/lambda-delta/src/toplevel/meta.ml b/helm/software/lambda-delta/src/toplevel/meta.ml index 553977251..1a710278e 100644 --- a/helm/software/lambda-delta/src/toplevel/meta.ml +++ b/helm/software/lambda-delta/src/toplevel/meta.ml @@ -9,8 +9,10 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) -type uri = Entity.uri -type id = Entity.id +module E = Entity + +type uri = E.uri +type id = E.id type term = Sort of bool (* sorts: true = TYPE, false = PROP *) | LRef of int * int (* local reference: local environment length, de bruijn index *) @@ -22,4 +24,4 @@ type pars = (id * term) list (* parameter declarations: name, type *) type entry = pars * term * term option (* parameters, domain, body *) -type entity = entry Entity.entity +type entity = entry E.entity diff --git a/helm/software/lambda-delta/src/toplevel/metaAut.ml b/helm/software/lambda-delta/src/toplevel/metaAut.ml index dd6c4a6f6..6a45518b5 100644 --- a/helm/software/lambda-delta/src/toplevel/metaAut.ml +++ b/helm/software/lambda-delta/src/toplevel/metaAut.ml @@ -10,10 +10,10 @@ V_______________________________________________________________ *) module U = NUri -module H = U.UriHash +module K = U.UriHash module C = Cps -module O = Options -module Y = Entity +module G = Options +module E = Entity module M = Meta module A = Aut @@ -35,9 +35,9 @@ type resolver = Local of int let henv_size, hcnt_size = 7000, 4300 (* hash tables initial sizes *) -let henv = H.create henv_size (* optimized global environment *) +let henv = K.create henv_size (* optimized global environment *) -let hcnt = H.create hcnt_size (* optimized context *) +let hcnt = K.create hcnt_size (* optimized context *) (* Internal functions *******************************************************) @@ -89,7 +89,7 @@ let resolve_lref_strict f st l lenv id = resolve_lref f st l lenv id let resolve_gref f st qid = - try let args = H.find henv (uri_of_qid qid) in f qid (Some args) + try let args = K.find henv (uri_of_qid qid) in f qid (Some args) with Not_found -> f qid None let resolve_gref_relaxed f st qid = @@ -103,7 +103,7 @@ let resolve_gref_relaxed f st qid = let get_pars f st = function | None -> f [] None | Some qid as node -> - try let pars = H.find hcnt (uri_of_qid qid) in f pars None + try let pars = K.find hcnt (uri_of_qid qid) in f pars None with Not_found -> f [] (Some node) let get_pars_relaxed f st = @@ -164,7 +164,7 @@ let xlate_entity err f st = function let f qid = let f pars = let f ww = - H.add hcnt (uri_of_qid qid) ((name, ww) :: pars); + K.add hcnt (uri_of_qid qid) ((name, ww) :: pars); err {st with node = Some qid} in xlate_term f st pars w @@ -176,10 +176,10 @@ let xlate_entity err f st = function let f pars = let f qid = let f ww = - H.add henv (uri_of_qid qid) pars; - let a = [Y.Mark st.line] in + K.add henv (uri_of_qid qid) pars; + let a = [E.Mark st.line] in let entry = pars, ww, None in - let entity = a, uri_of_qid qid, Y.Abst entry in + let entity = a, uri_of_qid qid, E.Abst entry in f {st with line = succ st.line} entity in xlate_term f st pars w @@ -191,10 +191,10 @@ let xlate_entity err f st = function let f pars = let f qid = let f ww vv = - H.add henv (uri_of_qid qid) pars; - let a = Y.Mark st.line :: if trans then [] else [Y.Priv] in + K.add henv (uri_of_qid qid) pars; + let a = E.Mark st.line :: if trans then [] else [E.Priv] in let entry = pars, ww, Some vv in - let entity = a, uri_of_qid qid, Y.Abbr entry in + let entity = a, uri_of_qid qid, E.Abbr entry in f {st with line = succ st.line} entity in let f ww = xlate_term (f ww) st pars v in @@ -207,12 +207,12 @@ let xlate_entity err f st = function (* Interface functions ******************************************************) let initial_status () = - H.clear henv; H.clear hcnt; { - path = []; node = None; nodes = []; line = 1; cover = !O.cover + K.clear henv; K.clear hcnt; { + path = []; node = None; nodes = []; line = 1; cover = !G.cover } let refresh_status st = {st with - cover = !O.cover + cover = !G.cover } let meta_of_aut = xlate_entity diff --git a/helm/software/lambda-delta/src/toplevel/metaBag.ml b/helm/software/lambda-delta/src/toplevel/metaBag.ml index 991d7e8c2..97148c737 100644 --- a/helm/software/lambda-delta/src/toplevel/metaBag.ml +++ b/helm/software/lambda-delta/src/toplevel/metaBag.ml @@ -10,45 +10,45 @@ V_______________________________________________________________ *) module C = Cps -module B = Bag +module Z = Bag module M = Meta (* Internal functions *******************************************************) let rec xlate_term c f = function | M.Sort s -> - let f h = f (B.Sort h) in + let f h = f (Z.Sort h) in if s then f 0 else f 1 | M.LRef (_, i) -> let l, _, _ = List.nth c i in - f (B.LRef l) + f (Z.LRef l) | M.GRef (_, uri, vs) -> - let map f t v = f (B.appl v t) in - let f vs = C.list_fold_left f map (B.GRef uri) vs in + let map f t v = f (Z.appl v t) in + let f vs = C.list_fold_left f map (Z.GRef uri) vs in C.list_map f (xlate_term c) vs | M.Appl (v, t) -> - let f v t = f (B.Appl (v, t)) in + let f v t = f (Z.Appl (v, t)) in let f v = xlate_term c (f v) t in xlate_term c f v | M.Abst (id, w, t) -> let f w = - let l = B.new_location () in - let f t = f (B.Bind (l, id, B.Abst w, t)) in + let l = Z.new_location () in + let f t = f (Z.Bind (l, id, Z.Abst w, t)) in let f c = xlate_term c f t in - B.push "meta" f c l id (B.Abst w) + Z.push "meta" f c l id (Z.Abst w) in xlate_term c f w let xlate_pars f pars = let map f (id, w) c = - let l = B.new_location () in - let f w = B.push "meta" f c l id (B.Abst w) in + let l = Z.new_location () in + let f w = Z.push "meta" f c l id (Z.Abst w) in xlate_term c f w in - C.list_fold_right f map pars B.empty_lenv + C.list_fold_right f map pars Z.empty_lenv let unwind_to_xlate_term f c t = - let map f t (l, id, b) = f (B.bind l id b t) in + let map f t (l, id, b) = f (Z.bind l id b t) in let f t = C.list_fold_left f map t c in xlate_term c f t @@ -57,7 +57,7 @@ let xlate_entry f = function let f c = unwind_to_xlate_term f c u in xlate_pars f pars | pars, u, Some t -> - let f u t = f (B.Cast (u, t)) in + let f u t = f (Z.Cast (u, t)) in let f c u = unwind_to_xlate_term (f u) c t in let f c = unwind_to_xlate_term (f c) c u in xlate_pars f pars diff --git a/helm/software/lambda-delta/src/toplevel/metaBrg.ml b/helm/software/lambda-delta/src/toplevel/metaBrg.ml index cde4daa13..72298dd13 100644 --- a/helm/software/lambda-delta/src/toplevel/metaBrg.ml +++ b/helm/software/lambda-delta/src/toplevel/metaBrg.ml @@ -10,7 +10,7 @@ V_______________________________________________________________ *) module C = Cps -module Y = Entity +module E = Entity module B = Brg module M = Meta @@ -32,7 +32,7 @@ let rec xlate_term c f = function xlate_term c f v | M.Abst (id, w, t) -> let f w = - let a = [Y.Name (id, true)] in + let a = [E.Name (id, true)] in let f t = f (B.Bind (a, B.Abst w, t)) in xlate_term (B.push c B.empty a (B.Abst w)) f t in @@ -40,7 +40,7 @@ let rec xlate_term c f = function let xlate_pars f pars = let map f (id, w) c = - let a = [Y.Name (id, true)] in + let a = [E.Name (id, true)] in let f w = f (B.push c B.empty a (B.Abst w)) in xlate_term c f w in diff --git a/helm/software/lambda-delta/src/toplevel/metaLibrary.ml b/helm/software/lambda-delta/src/toplevel/metaLibrary.ml index 3ae116d96..ca0fd9792 100644 --- a/helm/software/lambda-delta/src/toplevel/metaLibrary.ml +++ b/helm/software/lambda-delta/src/toplevel/metaLibrary.ml @@ -9,8 +9,8 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) -module F = Format -module O = MetaOutput +module F = Format +module MO = MetaOutput type out_channel = Pervasives.out_channel * F.formatter @@ -30,7 +30,7 @@ let open_out f name = f (och, frm) let write_entity f (_, frm) entity = - O.pp_entity f frm entity + MO.pp_entity f frm entity let close_out f (och, _) = close_out och; f () diff --git a/helm/software/lambda-delta/src/toplevel/metaOutput.ml b/helm/software/lambda-delta/src/toplevel/metaOutput.ml index 21d735d0e..859857ebe 100644 --- a/helm/software/lambda-delta/src/toplevel/metaOutput.ml +++ b/helm/software/lambda-delta/src/toplevel/metaOutput.ml @@ -14,7 +14,7 @@ module F = Format module U = NUri module C = Cps module L = Log -module Y = Entity +module E = Entity module M = Meta type counters = { @@ -69,21 +69,21 @@ let count_xterm f c = function | Some v -> count_term f c v let count_entity f c = function - | _, u, Y.Abst (pars, w, xv) -> + | _, u, E.Abst (pars, w, xv) -> let c = {c with eabsts = succ c.eabsts} in let c = {c with pabsts = c.pabsts + List.length pars} in let c = {c with uris = u :: c.uris; nodes = succ c.nodes + List.length pars} in let f c = count_xterm f c xv in let f c = count_term f c w in Cps.list_fold_left f count_par c pars - | _, _, Y.Abbr (pars, w, xv) -> + | _, _, E.Abbr (pars, w, xv) -> let c = {c with eabbrs = succ c.eabbrs; xnodes = succ c.xnodes} in let c = {c with pabsts = c.pabsts + List.length pars} in let c = {c with nodes = c.nodes + List.length pars} in let f c = count_xterm f c xv in let f c = count_term f c w in Cps.list_fold_left f count_par c pars - | _, _, Y.Void -> assert false + | _, _, E.Void -> assert false let print_counters f c = let terms = c.tsorts + c.tlrefs + c.tgrefs + c.tappls + c.tabsts in @@ -114,7 +114,7 @@ let string_of_sort = function let pp_transparent frm a = let err () = F.fprintf frm "%s" "=" in let f () = F.fprintf frm "%s" "~" in - Y.priv err f a + E.priv err f a let pp_list pp opend sep closed frm l = let rec aux frm = function @@ -151,12 +151,12 @@ let pp_body a frm = function | Some t -> F.fprintf frm "%a%a" pp_transparent a pp_term t let pp_entity frm = function - | a, uri, Y.Abst (pars, u, body) - | a, uri, Y.Abbr (pars, u, body) -> + | a, uri, E.Abst (pars, u, body) + | a, uri, E.Abbr (pars, u, body) -> F.fprintf frm "@[%u@@%s%a%a:%a@]@\n%!" - (Y.mark C.err C.start a) (U.string_of_uri uri) + (E.mark C.err C.start a) (U.string_of_uri uri) pp_pars pars (pp_body a) body pp_term u - | _, _, Y.Void -> assert false + | _, _, E.Void -> assert false let pp_entity f frm entity = pp_entity frm entity; f () diff --git a/helm/software/lambda-delta/src/toplevel/top.ml b/helm/software/lambda-delta/src/toplevel/top.ml index d45bcf98e..f69c4b8df 100644 --- a/helm/software/lambda-delta/src/toplevel/top.ml +++ b/helm/software/lambda-delta/src/toplevel/top.ml @@ -9,73 +9,72 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) -module F = Filename -module P = Printf -module U = NUri -module C = Cps -module L = Log -module T = Time -module O = Options -module H = Hierarchy -module Op = Output -module Y = Entity -module XL = XmlLibrary -module XCrg = XmlCrg -module AL = AutLexer -module AP = AutProcess -module AO = AutOutput -module DT = CrgTxt -module DA = CrgAut -module MA = MetaAut -module MO = MetaOutput -module ML = MetaLibrary -module MBrg = MetaBrg -module BrgC = BrgCrg -module BrgO = BrgOutput -module BrgR = BrgReduction -module BrgU = BrgUntrusted -module MBag = MetaBag -module BagO = BagOutput -module BagT = BagType -module BagU = BagUntrusted +module F = Filename +module P = Printf +module U = NUri +module C = Cps +module L = Log +module Y = Time +module G = Options +module H = Hierarchy +module O = Output +module E = Entity +module XL = XmlLibrary +module XD = XmlCrg +module AA = AutProcess +module AO = AutOutput +module TD = CrgTxt +module AD = CrgAut +module MA = MetaAut +module MO = MetaOutput +module ML = MetaLibrary +module MB = MetaBrg +module BD = BrgCrg +module BO = BrgOutput +module BR = BrgReduction +module BU = BrgUntrusted +module MZ = MetaBag +module ZO = BagOutput +module ZT = BagType +module ZU = BagUntrusted type status = { - ast : AP.status; - dst : DA.status; + ast : AA.status; + dst : AD.status; mst : MA.status; - tst : DT.status; + tst : TD.status; ac : AO.counters; mc : MO.counters; - brgc: BrgO.counters; - bagc: BagO.counters; - kst : Y.status + brgc: BO.counters; + bagc: ZO.counters; + kst : E.status } let flush_all () = L.flush 0; L.flush_err () let bag_error s msg = - L.error BagO.specs (L.Warn s :: L.Loc :: msg); flush_all () + L.error ZO.specs (L.Warn s :: L.Loc :: msg); flush_all () let brg_error s msg = - L.error BrgR.specs (L.Warn s :: L.Loc :: msg); flush_all () + L.error BR.specs (L.Warn s :: L.Loc :: msg); flush_all () let initial_status () = { ac = AO.initial_counters; mc = MO.initial_counters; - brgc = BrgO.initial_counters; - bagc = BagO.initial_counters; + brgc = BO.initial_counters; + bagc = ZO.initial_counters; mst = MA.initial_status (); - dst = DA.initial_status (); - tst = DT.initial_status (); - ast = AP.initial_status (); - kst = Y.initial_status () + dst = AD.initial_status (); + tst = TD.initial_status (); + ast = AA.initial_status (); + kst = E.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 + dst = AD.refresh_status st.dst; + tst = TD.refresh_status st.tst; + kst = E.refresh_status st.kst } (* kernel related ***********************************************************) @@ -90,16 +89,16 @@ type kernel_entity = BrgEntity of Brg.entity let kernel = ref Brg let print_counters st = match !kernel with - | Brg -> BrgO.print_counters C.start st.brgc - | Bag -> BagO.print_counters C.start st.bagc + | Brg -> BO.print_counters C.start st.brgc + | Bag -> ZO.print_counters C.start st.bagc let xlate_entity entity = match !kernel, entity with | Brg, CrgEntity e -> - let f e = (BrgEntity e) in Y.xlate f BrgC.brg_of_crg e + let f e = (BrgEntity e) in E.xlate f BD.brg_of_crg e | Brg, MetaEntity e -> - let f e = (BrgEntity e) in Y.xlate f MBrg.brg_of_meta e + let f e = (BrgEntity e) in E.xlate f MB.brg_of_meta e | Bag, MetaEntity e -> - let f e = (BagEntity e) in Y.xlate f MBag.bag_of_meta e + let f e = (BagEntity e) in E.xlate f MZ.bag_of_meta e | _, entity -> entity let pp_progress e = @@ -107,23 +106,23 @@ let pp_progress e = let s = U.string_of_uri u in let err () = L.warn (P.sprintf "%s" s) in let f i = L.warn (P.sprintf "[%u] %s" i s) in - Y.mark err f a + E.mark err f a in match e with - | CrgEntity e -> Y.common f e - | BrgEntity e -> Y.common f e - | BagEntity e -> Y.common f e - | MetaEntity e -> Y.common f e + | CrgEntity e -> E.common f e + | BrgEntity e -> E.common f e + | BagEntity e -> E.common f e + | MetaEntity e -> E.common f e let count_entity st = function | MetaEntity e -> {st with mc = MO.count_entity C.start st.mc e} - | BrgEntity e -> {st with brgc = BrgO.count_entity C.start st.brgc e} - | BagEntity e -> {st with bagc = BagO.count_entity C.start st.bagc e} + | BrgEntity e -> {st with brgc = BO.count_entity C.start st.brgc e} + | BagEntity e -> {st with bagc = ZO.count_entity C.start st.bagc e} | _ -> st let export_entity si xdir moch = function - | CrgEntity e -> XL.export_entity XCrg.export_term si xdir e - | BrgEntity e -> XL.export_entity BrgO.export_term si xdir e + | CrgEntity e -> XL.export_entity XD.export_term si xdir e + | BrgEntity e -> XL.export_entity BO.export_term si xdir e | MetaEntity e -> begin match moch with | None -> () @@ -135,8 +134,8 @@ let type_check st k = let brg_err msg = brg_error "Type Error" msg; failwith "Interrupted" in let ok _ _ = st in match k with - | BrgEntity entity -> BrgU.type_check brg_err ok st.kst entity - | BagEntity entity -> BagU.type_check ok st.kst entity + | BrgEntity entity -> BU.type_check brg_err ok st.kst entity + | BagEntity entity -> ZU.type_check ok st.kst entity | CrgEntity _ | MetaEntity _ -> st @@ -203,7 +202,7 @@ let entity_of_input lexbuf i = match i, !parbuf with let process_input f st = function | AutEntity e -> let f ast e = f {st with ast = ast} (AutEntity e) in - AP.process_command f st.ast e + AA.process_command f st.ast e | xe -> f st xe let count_input st = function @@ -226,13 +225,13 @@ let streaming = ref false (* parsing style (temporary) *) let process_2 st entity = let st = if !L.level > 2 then count_entity st entity else st in - if !export <> "" then export_entity !O.si !export !moch entity; + if !export <> "" then export_entity !G.si !export !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 !O.si !export !moch entity; + if !export <> "" && !stage = 1 then export_entity !G.si !export !moch entity; if !stage > 1 then process_2 st (xlate_entity entity) else st let process_0 st entity = @@ -246,11 +245,11 @@ let process_0 st entity = | AutEntity e, false -> let err dst = {st with dst = dst} in let g dst e = process_1 {st with dst = dst} (CrgEntity e) in - DA.crg_of_aut err g st.dst e + AD.crg_of_aut err g st.dst e | TxtEntity e, _ -> let crr tst = {st with tst = tst} in let d tst e = process_1 {st with tst = tst} (CrgEntity e) in - DT.crg_of_txt crr d gen_text st.tst e + TD.crg_of_txt crr d gen_text st.tst e | NoEntity, _ -> assert false in let st = if !L.level > 2 then count_input st entity else st in @@ -310,14 +309,14 @@ try stage := 3; moch := None; meta := false; progress := false; preprocess := false; root := ""; cc := false; export := ""; old := false; kernel := Brg; st := initial_status (); - L.clear (); O.clear (); H.clear (); Op.clear_reductions (); + L.clear (); G.clear (); H.clear (); O.clear_reductions (); streaming := false; in let process_file name = - if !L.level > 0 then T.gmtime version_string; + if !L.level > 0 then Y.gmtime version_string; if !L.level > 1 then L.warn (P.sprintf "Processing file: %s" name); - if !L.level > 0 then T.utime_stamp "started"; + if !L.level > 0 then Y.utime_stamp "started"; let base_name = Filename.chop_extension (Filename.basename name) in if !meta then set_meta_file base_name; let mk_uri = @@ -327,21 +326,21 @@ try | Bag -> Bag.mk_uri in let cover = F.concat !root base_name in - O.mk_uri := mk_uri; O.cover := cover; + G.mk_uri := mk_uri; G.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 > 0 then Y.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 Op.print_reductions () + if !stage > 2 then O.print_reductions () end in let exit () = close !moch; - if !L.level > 0 then T.utime_stamp "at exit"; + if !L.level > 0 then Y.utime_stamp "at exit"; flush_all () in let help = @@ -375,25 +374,25 @@ try L.box 0; L.box_err (); at_exit exit; Arg.parse [ - ("-L", Arg.Set O.debug_lexer, help_L); - ("-P", Arg.Set O.debug_parser, help_P); + ("-L", Arg.Set G.debug_lexer, help_L); + ("-P", Arg.Set G.debug_parser, help_P); ("-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 O.expand, help_g); + ("-g", Arg.Set G.expand, help_g); ("-h", Arg.String set_hierarchy, help_h); - ("-i", Arg.Set O.indexes, help_i); + ("-i", Arg.Set G.indexes, help_i); ("-j", Arg.Set progress, help_j); ("-k", Arg.String set_kernel, help_k); ("-m", Arg.Set meta, help_m); ("-o", Arg.Set old, help_o); ("-p", Arg.Set preprocess, help_p); - ("-q", Arg.Set O.unquote, help_q); + ("-q", Arg.Set G.unquote, help_q); ("-r", Arg.String set_root, help_r); ("-s", Arg.Int set_stage, help_s); - ("-u", Arg.Set O.si, help_u); + ("-u", Arg.Set G.si, help_u); ("-x", Arg.String set_xdir, help_x); ("-1", Arg.Set streaming, help_1); ] process_file help; -with BagT.TypeError msg -> bag_error "Type Error" msg +with ZT.TypeError msg -> bag_error "Type Error" msg diff --git a/helm/software/lambda-delta/src/xml/xmlCrg.ml b/helm/software/lambda-delta/src/xml/xmlCrg.ml index 62f0654bd..a0b5a7f1a 100644 --- a/helm/software/lambda-delta/src/xml/xmlCrg.ml +++ b/helm/software/lambda-delta/src/xml/xmlCrg.ml @@ -9,13 +9,13 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) -module U = NUri -module C = Cps -module H = Hierarchy -module Y = Entity -module A = Alpha -module X = XmlLibrary -module D = Crg +module U = NUri +module C = Cps +module H = Hierarchy +module Y = Entity +module R = Alpha +module XL = XmlLibrary +module D = Crg (* internal functions *******************************************************) @@ -54,38 +54,35 @@ let rec exp_term e t out tab = match t with let f s = Y.Name (s, true) :: a in H.string_of_sort err f l in - let attrs = [X.position l; X.name a] in - X.tag X.sort attrs out tab + let attrs = [XL.position l; XL.name a] in + XL.tag XL.sort attrs out tab | D.TLRef (a, i, j) -> let a = let err _ = a in let f n r = Y.Name (n, r) :: a in D.get_name err f i j e in - let attrs = [X.position i; X.offset j; X.name a] in - X.tag X.lref attrs out tab + let attrs = [XL.position i; XL.offset j; XL.name a] in + XL.tag XL.lref attrs out tab | D.TGRef (a, n) -> let a = Y.Name (U.name_of_uri n, true) :: a in - let attrs = [X.uri n; X.name a] in - X.tag X.gref attrs out tab + let attrs = [XL.uri n; XL.name a] in + XL.tag XL.gref attrs out tab | D.TCast (a, u, t) -> let attrs = [] in - X.tag X.cast attrs ~contents:(exp_term e u) out tab; + XL.tag XL.cast attrs ~contents:(exp_term e u) out tab; exp_term e t out tab | D.TAppl (a, vs, t) -> - let attrs = [X.arity (List.length vs)] in - X.tag X.appl attrs ~contents:(list_iter (exp_term e) vs) out tab; + let attrs = [XL.arity (List.length vs)] in + XL.tag XL.appl attrs ~contents:(list_iter (exp_term e) vs) out tab; exp_term e t out tab | D.TProj (a, lenv, t) -> let attrs = [] in - X.tag X.proj attrs ~contents:(lenv_iter (exp_bind e) (exp_eproj e) lenv) out tab; + XL.tag XL.proj attrs ~contents:(lenv_iter (exp_bind e) (exp_eproj e) lenv) out tab; exp_term (D.push_proj C.start e a lenv) t out tab | D.TBind (a, b, t) -> (* NOTE: the inner binders are alpha-converted first *) -(* so undesirable renamings might occur *) -(* EX: we rename [x][x]x to [x][x_]x_ *) -(* whereas [x_][x]x would be more desirable *) - let a = A.alpha (D.names_of_lenv [] e) a in + let a = R.alpha (D.names_of_lenv [] e) a in exp_bind e a b out tab; exp_term (D.push_bind C.start e a b) t out tab @@ -95,19 +92,19 @@ and exp_bind e a b out tab = match b with | D.Abst ws -> let e = D.push_bind C.start e a (D.Abst []) in - let attrs = [X.name ns; X.mark a; X.arity (List.length ws)] in - X.tag X.abst attrs ~contents:(list_rev_iter exp_term e ns ws) out tab + let attrs = [XL.name ns; XL.mark a; XL.arity (List.length ws)] in + XL.tag XL.abst attrs ~contents:(list_rev_iter exp_term e ns ws) out tab | D.Abbr vs -> let e = D.push_bind C.start e a (D.Abbr []) in - let attrs = [X.name ns; X.mark a; X.arity (List.length vs)] in - X.tag X.abbr attrs ~contents:(list_rev_iter exp_term e ns vs) out tab + let attrs = [XL.name ns; XL.mark a; XL.arity (List.length vs)] in + XL.tag XL.abbr attrs ~contents:(list_rev_iter exp_term e ns vs) out tab | D.Void n -> - let attrs = [X.name a; X.mark a; X.arity n] in - X.tag X.void attrs out tab + let attrs = [XL.name a; XL.mark a; XL.arity n] in + XL.tag XL.void attrs out tab and exp_eproj e a lenv out tab = let attrs = [] in - X.tag X.proj attrs ~contents:(lenv_iter (exp_bind e) (exp_eproj e) lenv) out tab + XL.tag XL.proj attrs ~contents:(lenv_iter (exp_bind e) (exp_eproj e) lenv) out tab (* interface functions ******************************************************) diff --git a/helm/software/lambda-delta/src/xml/xmlLibrary.ml b/helm/software/lambda-delta/src/xml/xmlLibrary.ml index 8a6801159..a9b1e5a1c 100644 --- a/helm/software/lambda-delta/src/xml/xmlLibrary.ml +++ b/helm/software/lambda-delta/src/xml/xmlLibrary.ml @@ -13,7 +13,7 @@ module F = Filename module U = NUri module C = Cps module H = Hierarchy -module Y = Entity +module E = Entity (* internal functions *******************************************************) @@ -94,23 +94,23 @@ let arity n = let name a = let map f i n r s = - let n = if r then n else "^" ^ n in + let n = if r then n else "-" ^ n in let spc = if i then "" else " " in f (s ^ n ^ spc) in let f s = "name", s in - Y.names f map a "" + E.names f map a "" let mark a = let err () = "mark", "" in let f i = "mark", string_of_int i in - Y.mark err f a + E.mark err f a (* TODO: the string s must be quoted *) let meta a = let err () = "meta", "" in let f s = "meta", s in - Y.meta err f a + E.meta err f a let export_entity pp_term si xdir (a, u, b) = let path = path_of_uri xdir u in @@ -118,12 +118,12 @@ let export_entity pp_term si xdir (a, u, b) = let och = open_out (path ^ obj_ext) in let out = output_string och in xml out "1.0" "UTF-8"; doctype out root system; - let a = Y.Name (U.name_of_uri u, true) :: a in + let a = E.Name (U.name_of_uri u, true) :: a in let attrs = [uri u; name a; mark a; meta a] in let contents = match b with - | Y.Abst w -> tag "ABST" attrs ~contents:(pp_term w) - | Y.Abbr v -> tag "ABBR" attrs ~contents:(pp_term v) - | Y.Void -> assert false + | E.Abst w -> tag "ABST" attrs ~contents:(pp_term w) + | E.Abbr v -> tag "ABBR" attrs ~contents:(pp_term v) + | E.Void -> assert false in let opts = if si then "si" else "" in let shp = H.string_of_graph () in diff --git a/helm/software/lambda-delta/xml/ld.dtd b/helm/software/lambda-delta/xml/ld.dtd index c16764021..1a3103c2a 100644 --- a/helm/software/lambda-delta/xml/ld.dtd +++ b/helm/software/lambda-delta/xml/ld.dtd @@ -12,65 +12,63 @@ @@ -80,18 +78,18 @@ -- 2.39.2