From: Ferruccio Guidi Date: Sun, 23 Nov 2014 19:36:06 +0000 (+0000) Subject: - new attributes system X-Git-Tag: make_still_working~795 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=977faf4820cd8ff5e2f0a5249161bbb92ae4b097;p=helm.git - new attributes system - new constraints system (starts) - static disambiguation of Automath unified binders by degree heuristics (C.E. Brown) [ grundlagen_2: just 1960 binders out of 47115 remain ambiguous ] - Makefile: XNLDIR is now relative --- diff --git a/helm/software/helena/.depend.opt b/helm/software/helena/.depend.opt index 22608ffa0..abec72608 100644 --- a/helm/software/helena/.depend.opt +++ b/helm/software/helena/.depend.opt @@ -7,12 +7,15 @@ src/lib/log.cmo: src/lib/log.cmi src/lib/log.cmx: src/lib/log.cmi src/lib/time.cmo: src/lib/log.cmi src/lib/time.cmx: src/lib/log.cmx +src/common/marks.cmi: +src/common/marks.cmo: src/common/marks.cmi +src/common/marks.cmx: src/common/marks.cmi src/common/hierarchy.cmi: src/common/hierarchy.cmo: src/lib/cps.cmx src/common/hierarchy.cmi src/common/hierarchy.cmx: src/lib/cps.cmx src/common/hierarchy.cmi -src/common/level.cmi: -src/common/level.cmo: src/common/level.cmi -src/common/level.cmx: src/common/level.cmi +src/common/level.cmi: src/common/marks.cmi +src/common/level.cmo: src/common/marks.cmi src/common/level.cmi +src/common/level.cmx: src/common/marks.cmx src/common/level.cmi src/common/entity.cmo: src/common/level.cmi src/common/entity.cmx: src/common/level.cmx src/common/options.cmo: src/lib/cps.cmx @@ -22,13 +25,10 @@ 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/marks.cmi: src/common/entity.cmx -src/common/marks.cmo: src/common/entity.cmx src/common/marks.cmi -src/common/marks.cmx: src/common/entity.cmx src/common/marks.cmi src/common/alpha.cmi: src/common/entity.cmx src/common/alpha.cmo: src/common/entity.cmx src/common/alpha.cmi src/common/alpha.cmx: src/common/entity.cmx src/common/alpha.cmi -src/common/ccs.cmi: src/common/entity.cmx +src/common/ccs.cmi: src/common/ccs.cmo: src/common/options.cmx src/common/entity.cmx \ src/lib/cps.cmx src/common/ccs.cmi src/common/ccs.cmx: src/common/options.cmx src/common/entity.cmx \ @@ -40,12 +40,12 @@ src/complete_rg/crg.cmo: src/common/level.cmi src/common/entity.cmx \ src/complete_rg/crg.cmx: src/common/level.cmx src/common/entity.cmx \ src/lib/cps.cmx src/complete_rg/crgOutput.cmi: src/complete_rg/crg.cmx -src/complete_rg/crgOutput.cmo: src/lib/log.cmi src/common/level.cmi \ - src/common/entity.cmx src/complete_rg/crg.cmx src/lib/cps.cmx \ - src/complete_rg/crgOutput.cmi -src/complete_rg/crgOutput.cmx: src/lib/log.cmx src/common/level.cmx \ - src/common/entity.cmx src/complete_rg/crg.cmx src/lib/cps.cmx \ - src/complete_rg/crgOutput.cmi +src/complete_rg/crgOutput.cmo: src/common/marks.cmi src/lib/log.cmi \ + src/common/level.cmi src/common/entity.cmx src/complete_rg/crg.cmx \ + src/lib/cps.cmx src/complete_rg/crgOutput.cmi +src/complete_rg/crgOutput.cmx: src/common/marks.cmx src/lib/log.cmx \ + src/common/level.cmx src/common/entity.cmx src/complete_rg/crg.cmx \ + src/lib/cps.cmx src/complete_rg/crgOutput.cmi src/text/txt.cmo: src/common/level.cmi src/text/txt.cmx: src/common/level.cmx src/text/txtParser.cmi: src/text/txt.cmx @@ -89,14 +89,13 @@ src/automath/autLexer.cmo: src/common/options.cmx src/lib/log.cmi \ src/automath/autLexer.cmx: src/common/options.cmx src/lib/log.cmx \ src/automath/autParser.cmx src/automath/autCrg.cmi: src/complete_rg/crg.cmx src/automath/aut.cmx -src/automath/autCrg.cmo: src/common/options.cmx src/common/level.cmi \ - src/common/entity.cmx src/complete_rg/crg.cmx src/lib/cps.cmx \ - src/automath/aut.cmx src/automath/autCrg.cmi -src/automath/autCrg.cmx: src/common/options.cmx src/common/level.cmx \ - src/common/entity.cmx src/complete_rg/crg.cmx src/lib/cps.cmx \ - src/automath/aut.cmx src/automath/autCrg.cmi -src/xml/xmlLibrary.cmi: src/common/level.cmi src/common/entity.cmx \ - src/common/ccs.cmi +src/automath/autCrg.cmo: src/common/options.cmx src/common/marks.cmi \ + src/common/level.cmi src/common/entity.cmx src/complete_rg/crg.cmx \ + src/lib/cps.cmx src/automath/aut.cmx src/automath/autCrg.cmi +src/automath/autCrg.cmx: src/common/options.cmx src/common/marks.cmx \ + src/common/level.cmx src/common/entity.cmx src/complete_rg/crg.cmx \ + src/lib/cps.cmx src/automath/aut.cmx src/automath/autCrg.cmi +src/xml/xmlLibrary.cmi: src/common/level.cmi src/common/entity.cmx src/xml/xmlLibrary.cmo: src/common/options.cmx src/common/level.cmi \ src/common/hierarchy.cmi src/common/entity.cmx src/lib/cps.cmx \ src/common/ccs.cmi src/xml/xmlLibrary.cmi @@ -113,12 +112,12 @@ src/xml/xmlCrg.cmx: src/xml/xmlLibrary.cmx src/common/hierarchy.cmx \ src/basic_rg/brg.cmo: src/common/level.cmi src/common/entity.cmx src/basic_rg/brg.cmx: src/common/level.cmx src/common/entity.cmx src/basic_rg/brgCrg.cmi: src/complete_rg/crg.cmx src/basic_rg/brg.cmx -src/basic_rg/brgCrg.cmo: src/common/marks.cmi src/common/level.cmi \ - src/common/entity.cmx src/complete_rg/crg.cmx src/lib/cps.cmx \ - src/basic_rg/brg.cmx src/basic_rg/brgCrg.cmi -src/basic_rg/brgCrg.cmx: src/common/marks.cmx src/common/level.cmx \ - src/common/entity.cmx src/complete_rg/crg.cmx src/lib/cps.cmx \ - src/basic_rg/brg.cmx src/basic_rg/brgCrg.cmi +src/basic_rg/brgCrg.cmo: src/common/level.cmi src/common/entity.cmx \ + src/complete_rg/crg.cmx src/lib/cps.cmx src/basic_rg/brg.cmx \ + src/basic_rg/brgCrg.cmi +src/basic_rg/brgCrg.cmx: src/common/level.cmx src/common/entity.cmx \ + src/complete_rg/crg.cmx src/lib/cps.cmx src/basic_rg/brg.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/xmlCrg.cmi src/common/options.cmx \ @@ -144,13 +143,13 @@ src/basic_rg/brgReduction.cmi: src/common/status.cmx src/lib/log.cmi \ src/basic_rg/brgReduction.cmo: src/common/status.cmx src/lib/share.cmx \ src/common/output.cmi src/common/options.cmx src/lib/log.cmi \ src/common/level.cmi src/common/hierarchy.cmi src/common/entity.cmx \ - src/lib/cps.cmx src/common/ccs.cmi src/basic_rg/brgOutput.cmi \ + src/common/ccs.cmi src/basic_rg/brgOutput.cmi \ src/basic_rg/brgEnvironment.cmi src/basic_rg/brg.cmx \ src/basic_rg/brgReduction.cmi src/basic_rg/brgReduction.cmx: src/common/status.cmx src/lib/share.cmx \ src/common/output.cmx src/common/options.cmx src/lib/log.cmx \ src/common/level.cmx src/common/hierarchy.cmx src/common/entity.cmx \ - src/lib/cps.cmx src/common/ccs.cmx src/basic_rg/brgOutput.cmx \ + src/common/ccs.cmx src/basic_rg/brgOutput.cmx \ src/basic_rg/brgEnvironment.cmx src/basic_rg/brg.cmx \ src/basic_rg/brgReduction.cmi src/basic_rg/brgValidity.cmi: src/common/status.cmx \ @@ -187,8 +186,10 @@ src/basic_rg/brgUntrusted.cmx: src/lib/log.cmx src/common/entity.cmx \ src/basic_rg/brgValidity.cmx src/basic_rg/brgType.cmx \ src/basic_rg/brgReduction.cmx src/basic_rg/brgEnvironment.cmx \ src/basic_rg/brg.cmx src/basic_rg/brgUntrusted.cmi -src/basic_ag/bag.cmo: src/lib/log.cmi src/common/entity.cmx src/lib/cps.cmx -src/basic_ag/bag.cmx: src/lib/log.cmx src/common/entity.cmx src/lib/cps.cmx +src/basic_ag/bag.cmo: src/common/marks.cmi src/lib/log.cmi \ + src/common/entity.cmx src/lib/cps.cmx +src/basic_ag/bag.cmx: src/common/marks.cmx src/lib/log.cmx \ + src/common/entity.cmx src/lib/cps.cmx src/basic_ag/bagCrg.cmi: src/complete_rg/crg.cmx src/basic_ag/bag.cmx src/basic_ag/bagCrg.cmo: src/common/marks.cmi src/common/level.cmi \ src/common/entity.cmx src/complete_rg/crg.cmx src/lib/cps.cmx \ @@ -211,7 +212,7 @@ src/basic_ag/bagEnvironment.cmo: src/lib/log.cmi src/common/entity.cmx \ src/basic_ag/bag.cmx src/basic_ag/bagEnvironment.cmi src/basic_ag/bagEnvironment.cmx: src/lib/log.cmx src/common/entity.cmx \ src/basic_ag/bag.cmx src/basic_ag/bagEnvironment.cmi -src/basic_ag/bagSubstitution.cmi: src/basic_ag/bag.cmx +src/basic_ag/bagSubstitution.cmi: src/common/marks.cmi src/basic_ag/bag.cmx src/basic_ag/bagSubstitution.cmo: src/lib/share.cmx src/basic_ag/bag.cmx \ src/basic_ag/bagSubstitution.cmi src/basic_ag/bagSubstitution.cmx: src/lib/share.cmx src/basic_ag/bag.cmx \ diff --git a/helm/software/helena/Makefile b/helm/software/helena/Makefile index 690c8c935..48e34b90f 100644 --- a/helm/software/helena/Makefile +++ b/helm/software/helena/Makefile @@ -14,7 +14,7 @@ TAGS = test-si test-si-fast profile xml-si xml-si-crg include Makefile.common -XMLDIR = $(HOME)/svn/helm_stable/www/lambdadelta +XMLDIR = ../../www/lambdadelta INPUT = examples/grundlagen/grundlagen_2.aut diff --git a/helm/software/helena/src/automath/autCrg.ml b/helm/software/helena/src/automath/autCrg.ml index 025459d2e..9093ffbb2 100644 --- a/helm/software/helena/src/automath/autCrg.ml +++ b/helm/software/helena/src/automath/autCrg.ml @@ -13,16 +13,15 @@ module U = NUri module K = U.UriHash module C = Cps module G = Options -module E = Entity +module J = Marks module N = Level +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 = E.attrs * D.term list - type context_node = qid option (* context node: None = root *) type status = { @@ -30,12 +29,10 @@ type status = { node: context_node; (* current context node *) nodes: context_node list; (* context node list *) line: int; (* line number *) - mk_uri: G.uri_generator; (* uri generator *) + mk_uri: G.uri_generator; (* uri generator *) + lenv: N.status; (* level environment *) } -type resolver = Local of int - | Global of context - let henv_size, hcnt_size = 7000, 4300 (* hash tables initial sizes *) let henv = K.create henv_size (* optimized global environment *) @@ -47,9 +44,9 @@ let hcnt = K.create hcnt_size (* optimized context *) let empty_cnt = D.ESort let add_abst cnt id w = - D.EBind (cnt, [E.Name (id, true)], D.Abst (N.infinite, w)) + D.EBind (cnt, E.node_attrs ~name:(id, true) (), D.Abst (N.two, w)) -let mk_lref f i = f (D.TLRef ([], i)) +let mk_lref f a i = f a.E.n_degr (D.TLRef (E.empty_node, i)) let id_of_name (id, _, _) = id @@ -82,8 +79,8 @@ 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 age, cnt = K.find henv (uri_of_qid qid) in f qid age cnt - with Not_found -> err qid + try let a, cnt = K.find henv (uri_of_qid qid) in f qid a cnt + with Not_found -> err qid let resolve_gref_relaxed f st qid = (* this is not tail recursive *) @@ -108,48 +105,49 @@ let push_abst f a w lenv = let add_proj e t = match e with | D.ESort -> t | D.EBind (D.ESort, a, b) -> D.TBind (a, b, t) - | _ -> D.TProj ([], e, t) - -let lenv_of_cnt cnt = cnt + | _ -> D.TProj (E.empty_node, e, t) (* this is not tail recursive in the GRef branch *) let rec xlate_term f st lenv = function - | A.Sort s -> - let f h = f (D.TSort ([], h)) in + | A.Sort s -> + let f h = f 0 (D.TSort (E.empty_node, h)) in if s then f 0 else f 1 | A.Appl (v, t) -> - let f vv tt = f (D.TAppl ([], vv, tt)) in - let f vv = xlate_term (f vv) st lenv t in + let f vv d tt = f d (D.TAppl (E.empty_node, vv, tt)) in + let f _ vv = xlate_term (f vv) st lenv t in xlate_term f st lenv v | A.Abst (name, w, t) -> - let f ww = - let a = [E.Name (name, true)] in - let f tt = - let b = D.Abst (N.infinite, ww) in - f (D.TBind (a, b, tt)) + let f d ww = + let a = E.node_attrs ~name:(name, true) () in + let f d tt = + let l = match d with + | 0 -> N.one + | 1 -> N.unknown st.lenv (J.new_mark ()) + | 2 -> N.two + | _ -> assert false + in + let b = D.Abst (l, ww) in + f d (D.TBind (a, b, tt)) in let f lenv = xlate_term f st lenv t in - push_abst f a ww lenv + push_abst f {a with E.n_degr = succ d} ww lenv in xlate_term f st lenv w | A.GRef (name, args) -> - let map1 args a = - let f id _ = A.GRef ((id, true, []), []) :: args in - E.name C.err f a - in + let map1 args (id, _) = A.GRef ((id, true, []), []) :: args in let map2 f arg args = - let f arg = f (D.EAppl (args, [], arg)) in + let f _ arg = f (D.EAppl (args, E.empty_node, arg)) in xlate_term f st lenv arg in - let g qid age cnt = - let gref = D.TGRef ([age], uri_of_qid qid) in - if cnt = D.ESort then f gref else + let g qid a cnt = + let gref = D.TGRef (a, uri_of_qid qid) in + if cnt = D.ESort then f a.E.n_degr gref else let f = function - | D.EAppl (D.ESort, a, v) -> f (D.TAppl (a, v, gref)) - | args -> f (D.TProj ([], args, gref)) + | D.EAppl (D.ESort, a, v) -> f a.E.n_degr (D.TAppl (a, v, gref)) + | args -> f a.E.n_degr (D.TProj (E.empty_node, args, gref)) in let f args = C.list_fold_right f map2 args D.ESort in - D.sub_list_strict (D.fold_attrs f map1 args) cnt args + D.sub_list_strict (D.fold_names f map1 args) cnt args in let g qid = resolve_gref_relaxed g st qid in let err () = complete_qid g st name in @@ -172,7 +170,7 @@ let xlate_entity err f st = function | A.Block (name, w) -> let f qid = let f cnt = - let f ww = + let f _ ww = K.add hcnt (uri_of_qid qid) (add_abst cnt name ww); err {st with node = Some qid} in @@ -182,18 +180,17 @@ let xlate_entity err f st = function in complete_qid f st (name, true, []) | A.Decl (name, w) -> - let f cnt = - let lenv = lenv_of_cnt cnt in + let f lenv = let f qid = - let f ww = - let age = E.Apix st.line in - K.add henv (uri_of_qid qid) (age, cnt); + let f d ww = + let a = E.node_attrs ~apix:st.line ~degr:(succ d) () in + K.add henv (uri_of_qid qid) (a, lenv); let t = add_proj lenv ww in (* print_newline (); CrgOutput.pp_term print_string t; *) - let b = E.Abst (N.infinite, t) in - let entity = [age], uri_of_qid qid, b in + let b = E.Abst t in + let entity = E.empty_root, a, uri_of_qid qid, b in f {st with line = succ st.line} entity in xlate_term f st lenv w @@ -202,20 +199,19 @@ let xlate_entity err f st = function in get_cnt_relaxed f st | A.Def (name, w, trans, v) -> - let f cnt = - let lenv = lenv_of_cnt cnt in + let f lenv = let f qid = - let f ww = - let f vv = - let age = E.Apix st.line in - K.add henv (uri_of_qid qid) (age, cnt); - let t = add_proj lenv (D.TCast ([], ww, vv)) in + let f _ ww = + let f d vv = + let na = E.node_attrs ~apix:st.line ~degr:d () in + K.add henv (uri_of_qid qid) (na, lenv); + let t = add_proj lenv (D.TCast (E.empty_node, ww, vv)) in (* print_newline (); CrgOutput.pp_term print_string t; *) let b = E.Abbr t in - let a = age :: if trans then [] else [E.Meta [E.Private]] in - let entity = a, uri_of_qid qid, b in + let ra = if trans then E.empty_root else E.root_attrs ~meta:[E.Private] () in + let entity = ra, na, uri_of_qid qid, b in f {st with line = succ st.line} entity in xlate_term f st lenv v @@ -230,7 +226,8 @@ let xlate_entity err f st = function let initial_status () = K.clear henv; K.clear hcnt; { - path = []; node = None; nodes = []; line = 1; mk_uri = G.get_mk_uri () + path = []; node = None; nodes = []; line = 1; mk_uri = G.get_mk_uri (); + lenv = N.initial_status (); } let refresh_status st = {st with diff --git a/helm/software/helena/src/basic_ag/bag.ml b/helm/software/helena/src/basic_ag/bag.ml index 5e7c07b5b..74c305156 100644 --- a/helm/software/helena/src/basic_ag/bag.ml +++ b/helm/software/helena/src/basic_ag/bag.ml @@ -12,25 +12,26 @@ (* kernel version: basic, absolute, global *) (* note : experimental *) +module J = Marks module E = Entity type uri = E.uri -type attrs = E.attrs +type attrs = E.node_attrs type bind = Void (* exclusion *) | Abst of term (* abstraction *) | Abbr of term (* abbreviation *) -and term = Sort of int (* hierarchy index *) - | LRef of int (* location *) - | GRef of uri (* reference *) - | Cast of term * term (* domain, element *) - | Appl of term * term (* argument, function *) - | Bind of attrs * int * bind * term (* name, location, binder, scope *) +and term = Sort of int (* hierarchy index *) + | LRef of J.mark (* location *) + | GRef of uri (* reference *) + | Cast of term * term (* domain, element *) + | Appl of term * term (* argument, function *) + | Bind of attrs * J.mark * bind * term (* name, location, binder, scope *) type entity = term E.entity (* attrs, uri, binder *) -type lenv = (attrs * int * bind) list (* name, location, binder *) +type lenv = (attrs * J.mark * bind) list (* name, location, binder *) type message = (lenv, term) Log.item list diff --git a/helm/software/helena/src/basic_ag/bagCrg.ml b/helm/software/helena/src/basic_ag/bagCrg.ml index 1bd594503..9724290f9 100644 --- a/helm/software/helena/src/basic_ag/bagCrg.ml +++ b/helm/software/helena/src/basic_ag/bagCrg.ml @@ -35,7 +35,7 @@ let rec xlate_term f c = function D.shift (xlate_term f c) e t (* this case should be removed by improving alpha-conversion *) | D.TBind (ab, D.Abst (n, ws), D.TCast (ac, u, t)) -> - xlate_term f c (D.TCast (ac, D.TBind (ab, D.Abst (N.pred n, ws), u), D.TBind (ab, D.Abst (n, ws), t))) + xlate_term f c (D.TCast (ac, D.TBind (ab, D.Abst (N.minus n 1, ws), u), D.TBind (ab, D.Abst (n, ws), t))) | D.TBind (a, b, t) -> let f cc = let a, l, b = List.hd cc in @@ -46,28 +46,28 @@ let rec xlate_term f c = function and xlate_bind f c a = function | D.Abst (_, w) -> - let f ww = Z.push "xlate_bind" f c a (J.new_location ()) (Z.Abst ww) in + let f ww = Z.push "xlate_bind" f c a (J.new_mark ()) (Z.Abst ww) in xlate_term f c w | D.Abbr v -> - let f vv = Z.push "xlate_bind" f c a (J.new_location ()) (Z.Abbr vv) in + let f vv = Z.push "xlate_bind" f c a (J.new_mark ()) (Z.Abbr vv) in xlate_term f c v | D.Void -> - Z.push "xlate_bind" f c a (J.new_location ()) Z.Void + Z.push "xlate_bind" f c a (J.new_mark ()) Z.Void (* internal functions: bag to crg term **************************************) let rec xlate_bk_term f c = function - | Z.Sort h -> f (D.TSort ([], h)) - | Z.GRef s -> f (D.TGRef ([], s)) + | Z.Sort h -> f (D.TSort (E.empty_node, h)) + | Z.GRef s -> f (D.TGRef (E.empty_node, s)) | Z.LRef l -> - let f i = f (D.TLRef ([], i)) in + let f i = f (D.TLRef (E.empty_node, i)) in Z.nth C.err f l c | Z.Cast (u, t) -> - let f tt uu = f (D.TCast ([], uu, tt)) in + let f tt uu = f (D.TCast (E.empty_node, uu, tt)) in let f tt = xlate_bk_term (f tt) c u in xlate_bk_term f c t | Z.Appl (u, t) -> - let f tt uu = f (D.TAppl ([], uu, tt)) in + let f tt uu = f (D.TAppl (E.empty_node, uu, tt)) in let f tt = xlate_bk_term (f tt) c u in xlate_bk_term f c t | Z.Bind (a, l, b, t) -> diff --git a/helm/software/helena/src/basic_ag/bagEnvironment.ml b/helm/software/helena/src/basic_ag/bagEnvironment.ml index 30e3e992f..24c212619 100644 --- a/helm/software/helena/src/basic_ag/bagEnvironment.ml +++ b/helm/software/helena/src/basic_ag/bagEnvironment.ml @@ -30,9 +30,9 @@ let error uri = raise (ObjectNotFound (L.items1 (U.string_of_uri uri))) (* Interface functions ******************************************************) -let set_entity f (a, uri, b) = +let set_entity f (ra, na, uri, b) = let age = get_age () in - let entry = (E.Apix age :: a), uri, b in + let entry = ra, {na with E.n_apix = Some age}, uri, b in K.add env uri entry; f entry let get_entity f uri = diff --git a/helm/software/helena/src/basic_ag/bagOutput.ml b/helm/software/helena/src/basic_ag/bagOutput.ml index 4d0a1c07b..0fbc039b2 100644 --- a/helm/software/helena/src/basic_ag/bagOutput.ml +++ b/helm/software/helena/src/basic_ag/bagOutput.ml @@ -68,13 +68,13 @@ and count_term f c = function count_term f c t let count_entity f c = function - | _, _, E.Abst (_, w) -> + | _, _, _, E.Abst w -> let c = {c with eabsts = succ c.eabsts} in count_term f c w - | _, _, E.Abbr v -> + | _, _, _, E.Abbr v -> let c = {c with eabbrs = succ c.eabbrs} in count_term f c v - | _, _, E.Void -> assert false + | _, _, _, E.Void -> assert false let print_counters f c = let terms = @@ -82,7 +82,7 @@ let print_counters f c = c.tabbrs in let items = c.eabsts + c.eabbrs in - let locations = J.locations () in + let locations = J.marks () in L.warn level (P.sprintf "Kernel representation summary (basic_ag)"); L.warn level (P.sprintf " Total entry items: %7u" items); L.warn level (P.sprintf " Declaration items: %7u" c.eabsts); @@ -106,7 +106,7 @@ let name err och a = E.name err f a let res a l och = - let err () = P.fprintf och "#%u" l in + let err () = P.fprintf och "#%s" (J.to_string l) in if !G.indexes then err () else name err och a let rec pp_term c och = function @@ -115,7 +115,7 @@ let rec pp_term c och = function let f s = P.fprintf och "%s" s in H.string_of_sort err f h | Z.LRef i -> - let err () = P.fprintf och "#%u" i in + let err () = P.fprintf och "#%s" (J.to_string i) in let f a _ = name err och a in if !G.indexes then err () else Z.get err f c i | Z.GRef s -> P.fprintf och "$%s" (U.string_of_uri s) diff --git a/helm/software/helena/src/basic_ag/bagReduction.ml b/helm/software/helena/src/basic_ag/bagReduction.ml index c7d89bc84..2f4b5a2c7 100644 --- a/helm/software/helena/src/basic_ag/bagReduction.ml +++ b/helm/software/helena/src/basic_ag/bagReduction.ml @@ -29,9 +29,9 @@ type machine = { type whd_result = | Sort_ of int - | LRef_ of int * Z.term option + | LRef_ of J.mark * Z.term option | GRef_ of Z.entity - | Bind_ of Z.attrs * int * Z.term * Z.term + | Bind_ of Z.attrs * J.mark * Z.term * Z.term type ho_whd_result = | Sort of int @@ -42,10 +42,10 @@ type ho_whd_result = let level = 4 let term_of_whdr = function - | Sort_ h -> Z.Sort h - | LRef_ (i, _) -> Z.LRef i - | GRef_ (_, uri, _) -> Z.GRef uri - | Bind_ (a, l, w, t) -> Z.bind_abst a l w t + | Sort_ h -> Z.Sort h + | LRef_ (i, _) -> Z.LRef i + | GRef_ (_, _, uri, _) -> Z.GRef uri + | Bind_ (a, l, w, t) -> Z.bind_abst a l w t let log1 s c t = let sc, st = s ^ " in the environment", "the term" in @@ -99,12 +99,12 @@ let rec whd f c m x = begin match m.s with | [] -> f m (Bind_ (a, l, w, t)) | v :: tl -> - let nl = J.new_location () in + let nl = J.new_mark () in let f mc = ZS.subst (whd f c {m with c = mc; s = tl}) nl l t in Z.push "!" f m.c a nl (Z.Abbr (Z.Cast (w, v))) end | Z.Bind (a, l, b, t) -> - let nl = J.new_location () in + let nl = J.new_mark () in let f mc = ZS.subst (whd f c {m with c = mc}) nl l t in Z.push "!" f m.c a nl b @@ -113,14 +113,14 @@ let rec whd f c m x = let rec ho_whd f c m x = (* L.warn "entering R.ho_whd"; *) let aux m = function - | Sort_ h -> f (Sort h) - | Bind_ (_, _, w, _) -> + | Sort_ h -> f (Sort h) + | 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_ (_, _, E.Abst (_, w)) -> ho_whd f c m w - | GRef_ (_, _, E.Abbr v) -> ho_whd f c m v - | LRef_ (_, None) -> assert false - | GRef_ (_, _, E.Void) -> assert false + | LRef_ (_, Some w) -> ho_whd f c m w + | 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_ (_, _, _, E.Void) -> assert false in whd aux c m x @@ -139,11 +139,11 @@ let rec are_convertible f st 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 st a c m1 m2 else f false - | GRef_ ((E.Apix a1 :: _), _, E.Abst _), - GRef_ ((E.Apix a2 :: _), _, E.Abst _) -> + | GRef_ (_, {E.n_apix = Some a1}, _, E.Abst _), + GRef_ (_, {E.n_apix = Some a2}, _, E.Abst _) -> if a1 = a2 then are_convertible_stacks f st a c m1 m2 else f false - | GRef_ ((E.Apix a1 :: _), _, E.Abbr v1), - GRef_ ((E.Apix a2 :: _), _, E.Abbr v2) -> + | GRef_ (_, {E.n_apix = Some a1}, _, E.Abbr v1), + GRef_ (_, {E.n_apix = Some a2}, _, E.Abbr v2) -> if a1 = a2 then let f a = if a then f a else are_convertible f st true c m1 v1 m2 v2 @@ -152,12 +152,12 @@ let rec are_convertible f st 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_ (_, _, E.Abbr v2) -> + | _, GRef_ (_, _, _, E.Abbr v2) -> whd (aux m1 r1) c m2 v2 - | GRef_ (_, _, E.Abbr v1), _ -> + | GRef_ (_, _, _, E.Abbr v1), _ -> whd (aux_rev m2 r2) c m1 v1 | Bind_ (a1, l1, w1, t1), Bind_ (a2, l2, w2, t2) -> - let l = J.new_location () in + let l = J.new_mark () in let h c = let m1, m2 = inc m1, inc m2 in let f t1 = ZS.subst (are_convertible f st a c m1 t1 m2) l l2 t2 in diff --git a/helm/software/helena/src/basic_ag/bagSubstitution.mli b/helm/software/helena/src/basic_ag/bagSubstitution.mli index b48c056df..45325ab44 100644 --- a/helm/software/helena/src/basic_ag/bagSubstitution.mli +++ b/helm/software/helena/src/basic_ag/bagSubstitution.mli @@ -9,4 +9,4 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) -val subst: (Bag.term -> 'a) -> int -> int -> Bag.term -> 'a +val subst: (Bag.term -> 'a) -> Marks.mark -> Marks.mark -> Bag.term -> 'a diff --git a/helm/software/helena/src/basic_ag/bagType.ml b/helm/software/helena/src/basic_ag/bagType.ml index aa4b821a8..4a3d37ecc 100644 --- a/helm/software/helena/src/basic_ag/bagType.ml +++ b/helm/software/helena/src/basic_ag/bagType.ml @@ -61,10 +61,10 @@ let rec b_type_of err f st c x = Z.get err0 f c i | Z.GRef uri -> let f = function - | _, _, E.Abst (_, w) -> f x w - | _, _, E.Abbr (Z.Cast (w, v)) -> f x w - | _, _, E.Abbr _ -> assert false - | _, _, E.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 ZE.get_entity f uri | Z.Bind (a, l, Z.Abbr v, t) -> diff --git a/helm/software/helena/src/basic_ag/bagUntrusted.ml b/helm/software/helena/src/basic_ag/bagUntrusted.ml index c27ec5ed1..9efbf9182 100644 --- a/helm/software/helena/src/basic_ag/bagUntrusted.ml +++ b/helm/software/helena/src/basic_ag/bagUntrusted.ml @@ -20,12 +20,12 @@ module ZT = BagType (* to share *) let type_check err f st = function - | a, uri, E.Abst (n, t) -> + | ra, na, uri, E.Abst t -> let err msg = err (L.Uri uri :: msg) in - let f xt tt = ZE.set_entity (f tt) (a, uri, E.Abst (n, xt)) in + let f xt tt = ZE.set_entity (f tt) (ra, na, uri, E.Abst xt) in ZT.type_of err f st Z.empty_lenv t - | a, uri, E.Abbr t -> + | ra, na, uri, E.Abbr t -> let err msg = err (L.Uri uri :: msg) in - let f xt tt = ZE.set_entity (f tt) (a, uri, E.Abbr xt) in + let f xt tt = ZE.set_entity (f tt) (ra, na, uri, E.Abbr xt) in ZT.type_of err f st Z.empty_lenv t - | _, _, E.Void -> assert false + | _, _, _, E.Void -> assert false diff --git a/helm/software/helena/src/basic_rg/brg.ml b/helm/software/helena/src/basic_rg/brg.ml index c9b5ee415..eeb9f56d6 100644 --- a/helm/software/helena/src/basic_rg/brg.ml +++ b/helm/software/helena/src/basic_rg/brg.ml @@ -16,7 +16,7 @@ module E = Entity module N = Level type uri = E.uri -type attrs = E.attrs +type attrs = E.node_attrs type bind = Void (* *) | Abst of N.level * term (* level, type *) @@ -62,7 +62,7 @@ let empty = Null let push e c a b = Cons (e, c, a, b) let rec get i = function - | Null -> Null, Null, [], Void + | Null -> Null, Null, E.empty_node, Void | Cons (e, c, a, b) when i = 0 -> e, c, a, b | Cons (e, _, _, _) -> get (pred i) e diff --git a/helm/software/helena/src/basic_rg/brgCrg.ml b/helm/software/helena/src/basic_rg/brgCrg.ml index f646145ed..a392afe93 100644 --- a/helm/software/helena/src/basic_rg/brgCrg.ml +++ b/helm/software/helena/src/basic_rg/brgCrg.ml @@ -11,7 +11,6 @@ module C = Cps module E = Entity -module J = Marks module N = Level module D = Crg module B = Brg @@ -37,7 +36,7 @@ let rec xlate_term f = function and xlate_bind f a b x = match b with | D.Abst (n, w) -> - let f ww = f (B.Bind (J.new_mark () :: a, B.Abst (n, ww), x)) in + let f ww = f (B.Bind (a, B.Abst (n, ww), x)) in xlate_term f w | D.Abbr v -> let f vv = f (B.Bind (a, B.Abbr vv, x)) in diff --git a/helm/software/helena/src/basic_rg/brgEnvironment.ml b/helm/software/helena/src/basic_rg/brgEnvironment.ml index d2daed49a..a3123caf3 100644 --- a/helm/software/helena/src/basic_rg/brgEnvironment.ml +++ b/helm/software/helena/src/basic_rg/brgEnvironment.ml @@ -20,8 +20,8 @@ let env = K.create hsize (* decps *) let set_entity entity = - let _, uri, _ = entity in + let _, _, uri, _ = entity in K.add env uri entity; entity let get_entity uri = - try K.find env uri with Not_found -> [], uri, E.Void + try K.find env uri with Not_found -> E.empty_root, E.empty_node, uri, E.Void diff --git a/helm/software/helena/src/basic_rg/brgOutput.ml b/helm/software/helena/src/basic_rg/brgOutput.ml index 978658caa..aa3cce952 100644 --- a/helm/software/helena/src/basic_rg/brgOutput.ml +++ b/helm/software/helena/src/basic_rg/brgOutput.ml @@ -91,15 +91,15 @@ and count_term f c e = function count_term_binder f c e b let count_entity f c = function - | _, u, E.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 - | _, _, E.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 - | _, _, E.Void -> assert false + | _, _, _, E.Void -> assert false let print_counters f c = let terms = @@ -143,7 +143,7 @@ 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 (E.Name (n, r) :: a) in + let f n r = if n = n0 && r = r0 then f a else f {a with E.n_name = Some (n, r)} in aux f e n0 r0 in E.name C.err f a @@ -158,7 +158,7 @@ let name err och a = E.name err f a let pp_level och n = - if N.is_infinite n then () else P.fprintf och "^%s" (N.to_string n) + P.fprintf och "%s" (N.to_string n) let rec pp_term e och = function | B.Sort (_, h) -> diff --git a/helm/software/helena/src/basic_rg/brgReduction.ml b/helm/software/helena/src/basic_rg/brgReduction.ml index 09e262d12..f397c1c6f 100644 --- a/helm/software/helena/src/basic_rg/brgReduction.ml +++ b/helm/software/helena/src/basic_rg/brgReduction.ml @@ -10,7 +10,6 @@ V_______________________________________________________________ *) module U = NUri -module C = Cps module W = Share module L = Log module H = Hierarchy @@ -98,19 +97,19 @@ let rec step st m x = else m, x, None | B.GRef (_, uri) -> begin match BE.get_entity uri with - | _, _, E.Abbr v -> + | _, _, _, E.Abbr v -> if st.S.delta then begin if !G.summary then O.add ~gdelta:1 (); step st m v end else m, x, Some v - | _, _, E.Abst (_, w) -> + | _, _, _, E.Abst w -> if assert_tstep m true then begin if !G.summary then O.add ~grt:1 (); step st (tstep m) w end else m, x, None - | _, _, E.Void -> + | _, _, _, E.Void -> assert false end | B.LRef (_, i) -> @@ -144,9 +143,9 @@ let rec step st m x = let n = N.minus n m.d in m, B.Bind (a, B.Abst (n, w), t), None | (c, v) :: s -> - if N.is_zero n then Q.add_nonzero st.S.cc a; +(* if N.is_zero n then Q.add_nonzero st.S.cc a; *) if !G.summary then O.add ~beta:1 ~theta:(List.length s) (); - let v = if assert_tstep m false then B.Cast ([], w, v) else v in + let v = if assert_tstep m false then B.Cast (E.empty_node, w, v) else v in let e = B.push m.e c a (B.abbr v) in step st {m with e = e; s = s} t end @@ -163,9 +162,8 @@ let assert_iterations m1 m2 = match m1.n, m2.n with | _ -> false let push m a b = - assert (m.s = []); let a, l = match b with - | B.Abst _ -> E.Apix m.l :: a, succ m.l + | B.Abst _ -> {a with E.n_apix = Some m.l}, succ m.l | b -> a, m.l in let e = B.push m.e m.e a b in @@ -176,15 +174,13 @@ let rec ac_nfs st (m1, t1, r1) (m2, t2, r2) = match t1, r1, t2, r2 with | B.Sort (_, h1), _, B.Sort (_, h2), _ -> h1 = h2 - | B.LRef (a1, _), _, B.LRef (a2, _), _ -> - let e1 = E.apix C.err C.start a1 in - let e2 = E.apix C.err C.start a2 in + | B.LRef ({E.n_apix = Some e1}, _), _, + B.LRef ({E.n_apix = Some e2}, _), _ -> if e1 = e2 then ac_stacks st m1 m2 else false | B.GRef (_, u1), None, B.GRef (_, u2), None -> if U.eq u1 u2 && assert_iterations m1 m2 then ac_stacks st m1 m2 else false - | B.GRef (a1, u1), Some v1, B.GRef (a2, u2), Some v2 -> - let e1 = E.apix C.err C.start a1 in - let e2 = E.apix C.err C.start a2 in + | B.GRef ({E.n_apix = Some e1}, u1), Some v1, + B.GRef ({E.n_apix = Some e2}, u2), Some v2 -> if e1 < e2 then begin if !G.summary then O.add ~gdelta:1 (); ac_nfs st (m1, t1, r1) (step st m2 v2) @@ -204,12 +200,12 @@ let rec ac_nfs st (m1, t1, r1) (m2, t2, r2) = ac_nfs st (step st m1 v1) (m2, t2, r2) | B.Bind (a1, (B.Abst (n1, w1) as b1), t1), _, B.Bind (a2, (B.Abst (n2, w2) as b2), t2), _ -> - if n1 = n2 then () else Q.add_equal st.S.cc a1 a2; +(* if n1 = n2 then () else Q.add_equal st.S.cc a1 a2; *) if ac {st with S.si = false} (reset m1 zero) w1 (reset m2 zero) w2 then ac st (push m1 a1 b1) t1 (push m2 a2 b2) t2 else false | B.Sort _, _, B.Bind (a, (B.Abst (n, _) as b), t), _ -> - if N.is_zero n then () else Q.add_zero st.S.cc a; +(* if N.is_zero n then () else Q.add_zero st.S.cc a; *) if !G.summary then O.add ~si:1 (); ac st (push m1 a b) t1 (push m2 a b) t | _ -> false diff --git a/helm/software/helena/src/basic_rg/brgReduction.mli b/helm/software/helena/src/basic_rg/brgReduction.mli index e73d2df8a..56fbf7723 100644 --- a/helm/software/helena/src/basic_rg/brgReduction.mli +++ b/helm/software/helena/src/basic_rg/brgReduction.mli @@ -17,7 +17,7 @@ val empty_kam: kam val get: kam -> int -> Brg.bind -val push: kam -> Entity.attrs -> Brg.bind -> kam +val push: kam -> Entity.node_attrs -> Brg.bind -> kam val xwhd: Status.status -> kam -> int option -> Brg.term -> kam * Brg.term diff --git a/helm/software/helena/src/basic_rg/brgType.ml b/helm/software/helena/src/basic_rg/brgType.ml index 29b73beeb..5ba07c876 100644 --- a/helm/software/helena/src/basic_rg/brgType.ml +++ b/helm/software/helena/src/basic_rg/brgType.ml @@ -82,10 +82,10 @@ let rec b_type_of err f st m x = end | B.GRef (_, uri) -> 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 -> + | _, _, _, 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) -> @@ -96,12 +96,12 @@ let rec b_type_of err f st m x = 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)) + | _ -> f (B.Cast (E.empty_node, vv, xv)) in type_of err f st m v | B.Bind (a, B.Abst (n, u), t) -> let f xu xt tt = - f (W.sh2 u xu t xt x (B.bind_abst n a)) (B.bind_abst (N.pred n) a xu tt) + f (W.sh2 u xu t xt x (B.bind_abst n a)) (B.bind_abst (N.minus n 1) a xu tt) in let f xu m = b_type_of err (f xu) st m t in let f xu _ = f xu (BR.push m a (B.abst n xu)) in diff --git a/helm/software/helena/src/basic_rg/brgUntrusted.ml b/helm/software/helena/src/basic_rg/brgUntrusted.ml index 88edd46d8..87a3f60cf 100644 --- a/helm/software/helena/src/basic_rg/brgUntrusted.ml +++ b/helm/software/helena/src/basic_rg/brgUntrusted.ml @@ -22,29 +22,29 @@ module BV = BrgValidity (* to share *) let type_check err f st = function - | a, uri, E.Abst (n, t) -> + | ra, na, uri, E.Abst t -> let err msg = err (L.Uri uri :: msg) in let f xt tt = - let e = BE.set_entity (a, uri, E.Abst (n, xt)) in f tt e + let e = BE.set_entity (ra, na, uri, E.Abst xt) in f tt e in BT.type_of err f st BR.empty_kam t - | a, uri, E.Abbr t -> + | ra, na, uri, E.Abbr t -> let err msg = err (L.Uri uri :: msg) in let f xt tt = let xt = match xt with | B.Cast _ -> xt - | _ -> B.Cast ([], tt, xt) + | _ -> B.Cast (E.empty_node, tt, xt) in - let e = BE.set_entity (a, uri, E.Abbr xt) in f tt e + let e = BE.set_entity (ra, na, uri, E.Abbr xt) in f tt e in BT.type_of err f st BR.empty_kam t - | _, _, E.Void -> assert false + | _, _, _, E.Void -> assert false let validate err f st e = let uri, t = match e with - | _, uri, E.Abst (_, t) -> uri, t - | _, uri, E.Abbr t -> uri, t - | _, _, E.Void -> assert false + | _, _, uri, E.Abst t -> uri, t + | _, _, uri, E.Abbr t -> uri, t + | _, _, _, E.Void -> assert false in let err msg = err (L.Uri uri :: msg) in let f () = let _ = BE.set_entity e in f () in diff --git a/helm/software/helena/src/basic_rg/brgValidity.ml b/helm/software/helena/src/basic_rg/brgValidity.ml index e358d5a19..c83c5e87f 100644 --- a/helm/software/helena/src/basic_rg/brgValidity.ml +++ b/helm/software/helena/src/basic_rg/brgValidity.ml @@ -69,9 +69,9 @@ let rec b_validate err f st m x = end | B.GRef (_, uri) -> begin match BE.get_entity uri with - | _, _, E.Abst _ - | _, _, E.Abbr _ -> f () - | _, _, E.Void -> + | _, _, _, E.Abst _ + | _, _, _, E.Abbr _ -> f () + | _, _, _, E.Void -> error1 err "reference to unknown entry" m x end | B.Bind (a, b, t) -> diff --git a/helm/software/helena/src/common/Make b/helm/software/helena/src/common/Make index 7be0f01c2..71d85f4f3 100644 --- a/helm/software/helena/src/common/Make +++ b/helm/software/helena/src/common/Make @@ -1 +1 @@ -hierarchy level entity options output marks alpha ccs status +marks hierarchy level entity options output alpha ccs status diff --git a/helm/software/helena/src/common/alpha.ml b/helm/software/helena/src/common/alpha.ml index 1eb6b1063..8da7e563b 100644 --- a/helm/software/helena/src/common/alpha.ml +++ b/helm/software/helena/src/common/alpha.ml @@ -11,29 +11,12 @@ module E = Entity -(* internal functions *******************************************************) - -let rec rename ns n = - let token, mode = n in - let n = token ^ "_", mode in - if List.mem n ns then rename ns n else n - -let alpha_name acc attr = - let ns, a = acc in - match attr with - | E.Name n -> - if List.mem n ns then - let n = rename ns n in - n :: ns, E.Name n :: a - else - n :: ns, attr :: a - | _ -> assert false - (* interface functions ******************************************************) -let alpha ns a = - let f a names = - let _, names = List.fold_left alpha_name (ns, []) (List.rev names) in - List.rev_append a names +let rec alpha mem x a = + let err () = a in + let f () = match a.E.n_name with + | None -> assert false + | Some (token, mode) -> alpha mem x {a with E.n_name = Some (token ^ "_", mode)} in - E.get_names f a + mem err f x a diff --git a/helm/software/helena/src/common/alpha.mli b/helm/software/helena/src/common/alpha.mli index a08e98e59..cf0fafd05 100644 --- a/helm/software/helena/src/common/alpha.mli +++ b/helm/software/helena/src/common/alpha.mli @@ -9,4 +9,7 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) -val alpha: Entity.names -> Entity.attrs -> Entity.attrs +val alpha: ((unit -> Entity.node_attrs) -> (unit -> Entity.node_attrs) -> + 'a -> Entity.node_attrs -> Entity.node_attrs + ) -> + 'a -> Entity.node_attrs -> Entity.node_attrs diff --git a/helm/software/helena/src/common/ccs.ml b/helm/software/helena/src/common/ccs.ml index 5364d1e07..d003d805c 100644 --- a/helm/software/helena/src/common/ccs.ml +++ b/helm/software/helena/src/common/ccs.ml @@ -14,7 +14,7 @@ module U = NUri module C = Cps module E = Entity module G = Options - +(* type csys = { buri: E.uri; mutable tp : int list; @@ -48,3 +48,4 @@ let add_equal s xa ia = let i = abs (mark xa), abs (mark ia) in if L.mem i s.tn then () else s.tn <- i :: s.tn else () +*) diff --git a/helm/software/helena/src/common/ccs.mli b/helm/software/helena/src/common/ccs.mli index f263d8a08..83061e6e5 100644 --- a/helm/software/helena/src/common/ccs.mli +++ b/helm/software/helena/src/common/ccs.mli @@ -8,7 +8,7 @@ \ / version 2 or (at your option) any later version. \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) - +(* type csys = { buri: Entity.uri; mutable tp : int list; @@ -23,3 +23,4 @@ val add_nonzero: csys -> Entity.attrs -> unit val add_zero: csys -> Entity.attrs -> unit val add_equal: csys -> Entity.attrs -> Entity.attrs -> unit +*) diff --git a/helm/software/helena/src/common/entity.ml b/helm/software/helena/src/common/entity.ml index 9915dd3c3..c44719050 100644 --- a/helm/software/helena/src/common/entity.ml +++ b/helm/software/helena/src/common/entity.ml @@ -18,102 +18,61 @@ type id = string (* identifier *) type name = id * bool (* token, real? *) -type names = name list - type meta = Main (* main object *) | InProp (* inhabitant of a proposition *) | Progress (* uncompleted object *) | Private (* private global definition *) -type attr = Name of name (* name *) - | Apix of int (* additional position index *) - | Mark of int (* node marker *) - | Meta of meta list (* metaliguistic classification *) - | Info of (string * string) (* metaliguistic annotation: language (defaults to "en-US"), text *) +type node_attrs = { + n_name: name option; (* name *) + n_apix: int option; (* additional position index *) + n_degr: int; (* degree *) + n_real: bool; (* real node? (not generated) *) +} -type attrs = attr list (* attributes *) +type root_attrs = { + r_meta: meta list; (* metaliguistic classification *) + r_info: (string * string) option; (* metaliguistic annotation: language (defaults to "en-US"), text *) +} -type 'term bind = Abst of N.level * 'term (* declaration: level, domain *) - | Abbr of 'term (* definition: body *) - | Void (* exclusion *) +type 'term bind = Abst of 'term (* declaration: domain *) + | Abbr of 'term (* definition: body *) + | Void (* exclusion *) -type 'term entity = attrs * uri * 'term bind (* attrs, name, binder *) +type 'term entity = root_attrs * node_attrs * uri * 'term bind (* attrs, uri, binder *) (* helpers ******************************************************************) -let common f (a, u, _) = f a u - -let rec name err f = function - | Name (n, r) :: _ -> f n r - | _ :: tl -> name err f tl - | [] -> err () - -let names f map l a = - let rec aux f i a = function - | [] -> f a - | Name (n, r) :: tl -> aux (map f i n r) false a tl - | _ :: tl -> aux f i a tl - in - aux f true a l - -let rec get_name err f j = function - | [] -> err () - | Name (n, r) :: _ when j = 0 -> f n r - | Name _ :: tl -> get_name err f (pred j) tl - | _ :: tl -> get_name err f j tl - -let rec get_names f = function - | [] -> f [] [] - | Name _ as n :: tl -> - let f a ns = f a (n :: ns) in get_names f tl - | e :: tl -> - let f a = f (e :: a) in get_names f tl - -let count_names a = - let rec aux k = function - | [] -> k - | Name _ :: tl -> aux (succ k) tl - | _ :: tl -> aux k tl - in - aux 0 a - -let rec apix err f = function - | Apix i :: _ -> f i - | _ :: tl -> apix err f tl - | [] -> err () - -let rec mark err f = function - | Mark i :: _ -> f i - | _ :: tl -> mark err f tl - | [] -> err () - -let rec meta err f = function - | Meta ms :: _ -> f ms - | _ :: tl -> meta err f tl - | [] -> err () - -let rec info err f = function - | Info (lg, tx) :: _ -> f lg tx - | _ :: tl -> info err f tl - | [] -> err () - -let resolve err f name a = - let rec aux i = function - | Name (n, true) :: _ when n = name -> f i - | _ :: tl -> aux (succ i) tl - | [] -> err i - in - aux 0 a - -let rec rev_append_names ns = function - | [] -> ns - | Name n :: tl -> rev_append_names (n :: ns) tl - | _ :: tl -> rev_append_names ns tl +let node_attrs ?(real=true) ?apix ?name ?(degr=0) () = { + n_real = real; n_apix = apix; n_name = name; n_degr = degr; +} + +let root_attrs ?(meta=[]) ?info () = { + r_meta = meta; r_info = info; +} + +let empty_node = node_attrs () + +let empty_root = root_attrs () + +let common f (ra, na, u, _) = f ra na u + +let rec name err f a = match a.n_name with + | Some (n, r) -> f n r + | None -> err () + +let rec apix err f a = match a.n_apix with + | Some i -> f i + | None -> err () + +let rec info err f a = match a.r_info with + | Some (lg, tx) -> f lg tx + | None -> err () let xlate f xlate_term = function - | a, uri, Abst (n, t) -> - let f t = f (a, uri, Abst (n, t)) in xlate_term f t - | a, uri, Abbr t -> - let f t = f (a, uri, Abbr t) in xlate_term f t - | _, _, Void -> + | ra, na, uri, Abst t -> + let f t = f (ra, na, uri, Abst t) in xlate_term f t + | ra, na, uri, Abbr t -> + let f t = f (ra, na, uri, Abbr t) in xlate_term f t + | _, _, _, Void -> assert false diff --git a/helm/software/helena/src/common/level.ml b/helm/software/helena/src/common/level.ml index b10dda06a..60f7ac438 100644 --- a/helm/software/helena/src/common/level.ml +++ b/helm/software/helena/src/common/level.ml @@ -9,34 +9,63 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) -type level = int option +module H = Hashtbl + +module J = Marks + +type level = Inf (* infinite *) + | Fin of int (* finite *) + | Ref of J.mark (* unknown *) + +type const = NotZero (* not zero: beta and whnf allowed *) + +type contents = Value of level (* defined with this level *) + | Const of const list (* undefined with these constraints *) + +type status = (J.mark, contents) H.t (* environment for level variables *) + +(* Internal functions *******************************************************) + +let env_size = 2000 + +let empty_ref = Const [] + +let find st k = + try H.find st k with Not_found -> H.add st k empty_ref; empty_ref + +let rec resolve st k = match find st k with + | Value (Ref k) -> resolve st k + | cell -> k, cell (* Interface functions ******************************************************) -let infinite = None +let initial_status () = + H.create env_size + +let infinite = Inf + +let zero = Fin 0 -let finite i = Some i +let one = Fin 1 -let is_zero xi = - xi = (Some 0) +let two = Fin 2 -let is_infinite xi = - xi = None +let finite i = Fin i -let succ = function - | None -> None - | Some i -> Some (succ i) +let unknown st k = match resolve st k with + | _, Value l -> l + | k, Const _ -> Ref k -let pred = function - | None -> None - | Some i when i > 1 -> Some (pred i) - | _ -> Some 0 +let is_zero l = + l = zero let minus n j = match n with - | None -> None - | Some i when i > j -> Some (i - j) - | _ -> Some 0 + | Inf -> Inf + | Fin i when i > j -> Fin (i - j) + | Fin _ -> zero + | Ref i -> Inf (* assert false *) let to_string = function - | None -> "" - | Some i -> string_of_int i + | Inf -> "" + | Fin i -> string_of_int i + | Ref k -> "-" ^ J.to_string k diff --git a/helm/software/helena/src/common/level.mli b/helm/software/helena/src/common/level.mli index 9b4955248..4bae584fa 100644 --- a/helm/software/helena/src/common/level.mli +++ b/helm/software/helena/src/common/level.mli @@ -9,19 +9,23 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) +type status + type level +val initial_status: unit -> status + val infinite: level val finite: int -> level -val is_zero: level -> bool +val one: level -val is_infinite: level -> bool +val two: level -val succ: level -> level +val unknown: status -> Marks.mark -> level -val pred: level -> level +val is_zero: level -> bool val minus: level -> int -> level diff --git a/helm/software/helena/src/common/marks.ml b/helm/software/helena/src/common/marks.ml index fba716b37..5b45cc79f 100644 --- a/helm/software/helena/src/common/marks.ml +++ b/helm/software/helena/src/common/marks.ml @@ -9,16 +9,15 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) -module E = Entity +type mark = int -let location = ref 0 +let mark = ref 1 (* interface functions ******************************************************) -let locations () = !location - -let new_location () = - incr location; !location +let marks () = !mark let new_mark () = - E.Mark (new_location ()) + incr mark; !mark + +let to_string i = string_of_int i diff --git a/helm/software/helena/src/common/marks.mli b/helm/software/helena/src/common/marks.mli index ff5a68109..b4bafe680 100644 --- a/helm/software/helena/src/common/marks.mli +++ b/helm/software/helena/src/common/marks.mli @@ -9,8 +9,10 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) -val locations: unit -> int +type mark -val new_location: unit -> int +val marks: unit -> int -val new_mark: unit -> Entity.attr +val new_mark: unit -> mark + +val to_string: mark -> string diff --git a/helm/software/helena/src/common/status.ml b/helm/software/helena/src/common/status.ml index 3ae313608..a076a9aae 100644 --- a/helm/software/helena/src/common/status.ml +++ b/helm/software/helena/src/common/status.ml @@ -15,16 +15,16 @@ module Q = Ccs type status = { delta: bool; (* global delta-expansion *) si: bool; (* sort inclusion *) - cc: Q.csys; (* conversion constraints *) +(* cc: Q.csys; (* conversion constraints *) *) } (* helpers ******************************************************************) let initial_status () = { delta = false; - si = !G.si; cc = Q.init () + si = !G.si; (* cc = Q.init () *) } let refresh_status st = {st with - si = !G.si; cc = Q.init () + si = !G.si; (* cc = Q.init () *) } diff --git a/helm/software/helena/src/complete_rg/crg.ml b/helm/software/helena/src/complete_rg/crg.ml index 7ba80ddfb..0acd43336 100644 --- a/helm/software/helena/src/complete_rg/crg.ml +++ b/helm/software/helena/src/complete_rg/crg.ml @@ -18,7 +18,7 @@ module N = Level type uri = E.uri type id = E.id -type attrs = E.attrs +type attrs = E.node_attrs type bind = Abst of N.level * term (* level, type *) | Abbr of term (* body *) @@ -72,7 +72,7 @@ let resolve_lref err f id lenv = | ESort -> err () | EAppl (tl, _, _) -> aux i tl | EBind (tl, a, _) -> - let f id0 _ = if id0 = id then f i else aux (succ i) tl in + let f id0 _ = if id0 = id then f a i else aux (succ i) tl in E.name err f a | EProj (tl, _, d) -> append (aux i) tl d in @@ -89,44 +89,8 @@ let rec get_name err f i = function let err i = get_name err f i tl in get_name err f i e -(* -let push2 err f lenv ?attr ?t () = match lenv, attr, t with - | EBind (e, a, Abst (n, ws)), Some attr, Some t -> - f (EBind (e, (attr :: a), Abst (n, t :: ws))) - | EBind (e, a, Abst (n, ws)), None, Some t -> - f (EBind (e, a, Abst (n, t :: ws))) - | EBind (e, a, Abbr vs), Some attr, Some t -> - f (EBind (e, (attr :: a), Abbr (t :: vs))) - | EBind (e, a, Abbr vs), None, Some t -> - f (EBind (e, a, Abbr (t :: vs))) - | EBind (e, a, Void n), Some attr, None -> - f (EBind (e, (attr :: a), Void (succ n))) - | EBind (e, a, Void n), None, None -> - f (EBind (e, a, Void (succ n))) - | _ -> err () - -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 E.count_names a > j then f (k + j) else err i - | EBind (tl, a, _) -> - aux f (pred i) (k + E.count_names a) tl - | EProj (tl, _, d) -> aux f i k (eshift C.start tl d) - in - aux f i 0 lenv -*) -let rec names_of_lenv ns = function - | ESort -> ns - | EBind (tl, a, _) -> names_of_lenv (E.rev_append_names ns a) tl - | EAppl (tl, _, _) -> names_of_lenv ns tl - | EProj (tl, _, e) -> names_of_lenv (names_of_lenv ns e) tl - let rec get e i = match e with - | ESort -> ESort, [], Void + | ESort -> ESort, E.empty_node, Void | EBind (e, a, b) when i = 0 -> e, a, b | EBind (e, _, _) -> get e (pred i) | EAppl (e, _, _) -> get e i @@ -137,7 +101,15 @@ let rec sub_list_strict f e l = match e, l with | EBind (e, _, Abst _), _ :: tl -> sub_list_strict f e tl | _ -> assert false -let rec fold_attrs f map a0 = function - | ESort -> f a0 - | EBind (e, a, Abst _) -> fold_attrs f map (map a0 a) e - | _ -> assert false +let rec fold_names f map x = function + | ESort -> f x + | EBind (e, {E.n_name = Some n}, Abst _) -> fold_names f map (map x n) e + | _ -> assert false + +let rec mem err f e b = match e with + | ESort -> err () + | EBind (e, a, _) -> + if a.E.n_name = b.E.n_name then f () else mem err f e b + | EAppl (e, _, _) -> mem err f e b + | EProj (e, _, d) -> + let err () = mem err f e b in mem err f d b diff --git a/helm/software/helena/src/complete_rg/crgOutput.ml b/helm/software/helena/src/complete_rg/crgOutput.ml index d5f639b39..529a293e1 100644 --- a/helm/software/helena/src/complete_rg/crgOutput.ml +++ b/helm/software/helena/src/complete_rg/crgOutput.ml @@ -13,8 +13,9 @@ module P = Printf module U = NUri module C = Cps module L = Log -module E = Entity +module J = Marks module N = Level +module E = Entity module D = Crg (* nodes count **************************************************************) @@ -90,15 +91,15 @@ and count_binder f c e a b = match b with D.push_bind (f c) a b e let count_entity f c = function - | _, u, E.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 D.ESort w - | _, _, E.Abbr v -> + | _, _, _, E.Abbr v -> let c = {c with eabbrs = succ c.eabbrs; xnodes = succ c.xnodes} in count_term f c D.ESort v - | _, _, E.Void -> assert false + | _, _, _, E.Void -> assert false let print_counters f c = let terms = @@ -107,6 +108,7 @@ let print_counters f c = in let items = c.eabsts + c.eabbrs in let nodes = c.nodes + c.xnodes in + let marks = J.marks () in L.warn level (P.sprintf "Intermediate representation summary (complete_rg)"); L.warn level (P.sprintf " Total entry items: %7u" items); L.warn level (P.sprintf " Declaration items: %7u" c.eabsts); @@ -119,6 +121,7 @@ let print_counters f c = L.warn level (P.sprintf " Application items: %7u" c.tappls); L.warn level (P.sprintf " Abstraction items: %7u" c.tabsts); L.warn level (P.sprintf " Abbreviation items: %7u" c.tabbrs); + L.warn level (P.sprintf " Ambiguous abstractions: %7u" marks); L.warn level (P.sprintf " Global Int. Complexity: %7u" c.nodes); L.warn level (P.sprintf " + Abbreviation nodes: %7u" nodes); f () @@ -126,15 +129,10 @@ let print_counters f c = (* term/environment pretty printer ******************************************) let pp_attrs out a = - let map = function - | 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 _ -> () - | E.Info _ -> () - in - List.iter map a + let f s b = if b then out (P.sprintf "%s;" s) else out (P.sprintf "~%s;" s) in + E.name ignore f a; + let f i = out (P.sprintf "+%i;" i) in + E.apix ignore f a let rec pp_term out = function | D.TSort (a, l) -> pp_attrs out a; out (P.sprintf "*%u" l) @@ -147,8 +145,7 @@ let rec pp_term out = function and pp_bind out = function | D.Abst (n, x) -> - out "[:"; pp_term out x; out "]"; - if N.is_infinite n then () else out (N.to_string n) + out "[:"; pp_term out x; out "]"; out (N.to_string n) | D.Abbr x -> out "[="; pp_term out x; out "]"; | D.Void -> out "[]" diff --git a/helm/software/helena/src/modules.ml b/helm/software/helena/src/modules.ml index 6f795219f..b05249224 100644 --- a/helm/software/helena/src/modules.ml +++ b/helm/software/helena/src/modules.ml @@ -8,12 +8,12 @@ module W = Share (**) module L = Log module Y = Time (**) +module J = Marks (**) module H = Hierarchy module N = Level module E = Entity module G = Options module O = Output -module J = Marks (**) module R = Alpha module Q = Ccs module S = Status diff --git a/helm/software/helena/src/text/txtCrg.ml b/helm/software/helena/src/text/txtCrg.ml index a6839b89c..63b7725b2 100644 --- a/helm/software/helena/src/text/txtCrg.ml +++ b/helm/software/helena/src/text/txtCrg.ml @@ -30,9 +30,9 @@ let henv_size = 7000 (* hash tables initial size *) let henv = Hashtbl.create henv_size (* optimized global environment *) (* Internal functions *******************************************************) - -let name_of_id ?(r=true) id = E.Name (id, r) (* +let name_of_id ?(r=true) id = E.Name (id, r) + let mk_lref f i j k = f (D.TLRef ([E.Apix k], i, j)) let mk_gref f uri = f (D.TGRef ([], uri)) diff --git a/helm/software/helena/src/toplevel/top.ml b/helm/software/helena/src/toplevel/top.ml index afa62555d..d64857d32 100644 --- a/helm/software/helena/src/toplevel/top.ml +++ b/helm/software/helena/src/toplevel/top.ml @@ -91,11 +91,11 @@ let xlate_entity entity = match !G.kernel, entity with | _, entity -> entity let pp_progress e = - let f a u = + let f _ na u = let s = U.string_of_uri u in let err () = L.warn 2 (P.sprintf "<%s>" s) in let f i = L.warn 2 (P.sprintf "[%u] <%s>" i s) in - E.apix err f a + E.apix err f na in match e with | CrgEntity e -> E.common f e @@ -267,7 +267,7 @@ let process st name = let lexbuf = Lexing.from_channel ich in let st = process st lexbuf input in close_in ich; - if !G.cc then XL.export_csys st.kst.S.cc; +(* if !G.cc then XL.export_csys st.kst.S.cc; *) st, input let main = diff --git a/helm/software/helena/src/xml/xmlCrg.ml b/helm/software/helena/src/xml/xmlCrg.ml index ce14855e0..2e10553cb 100644 --- a/helm/software/helena/src/xml/xmlCrg.ml +++ b/helm/software/helena/src/xml/xmlCrg.ml @@ -12,7 +12,7 @@ module U = NUri module C = Cps module H = Hierarchy -module Y = Entity +module E = Entity module R = Alpha module XL = XmlLibrary module D = Crg @@ -24,6 +24,8 @@ let lenv_iter map_bind map_appl map_proj e lenv out tab = | D.ESort -> e | D.EBind (e, a, b) -> let e = aux e in +(* NOTE: the inner binders are alpha-converted first *) + let a = R.alpha D.mem e a in map_bind e a b out tab; D.EBind (e, a, b) | D.EAppl (e, a, v) -> let e = aux e in @@ -38,7 +40,7 @@ let rec exp_term e t out tab = match t with | D.TSort (a, l) -> let a = let err _ = a in - let f s = Y.Name (s, true) :: a in + let f s = {a with E.n_name = Some (s, true)} in H.string_of_sort err f l in let attrs = [XL.position l; XL.name a] in @@ -46,13 +48,13 @@ let rec exp_term e t out tab = match t with | D.TLRef (a, i) -> let a = let err _ = a in - let f n r = Y.Name (n, r) :: a in + let f n r = {a with E.n_name = Some (n, r)} in D.get_name err f i e in let attrs = [XL.position i; 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 a = {a with E.n_name = Some (U.name_of_uri n, true)} in let attrs = [XL.uri n; XL.name a; XL.apix a] in XL.tag XL.gref attrs out tab | D.TCast (a, u, t) -> @@ -69,7 +71,7 @@ let rec exp_term e t out tab = match t with exp_term (D.push_proj C.start a lenv e) t out tab | D.TBind (a, b, t) -> (* NOTE: the inner binders are alpha-converted first *) - let a = R.alpha (D.names_of_lenv [] e) a in + let a = R.alpha D.mem e a in exp_bind e a b out tab; exp_term (D.push_bind C.start a b e) t out tab @@ -79,7 +81,7 @@ and exp_appl e a v out tab = and exp_bind e a b out tab = match b with | D.Abst (n, w) -> - let attrs = [XL.level n; XL.name a; XL.mark a] in + let attrs = [XL.level n; XL.name a] in XL.tag XL.abst attrs ~contents:(exp_term e w) out tab | D.Abbr v -> let attrs = [XL.name a] in diff --git a/helm/software/helena/src/xml/xmlLibrary.ml b/helm/software/helena/src/xml/xmlLibrary.ml index e182ab9a3..1e2bd4de4 100644 --- a/helm/software/helena/src/xml/xmlLibrary.ml +++ b/helm/software/helena/src/xml/xmlLibrary.ml @@ -96,24 +96,15 @@ let uri u = "uri", U.string_of_uri u let name a = - let map f i n r s = - 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 - E.names f map a "" + let err () = "name", "" in + let f n r = "name", if r then n else "-" ^ n in + E.name err f a let apix a = let err () = "age", "" in let f i = "age", string_of_int i in E.apix err f a -let mark a = - let err () = "mark", "" in - let f i = "mark", string_of_int i in - E.mark err f a - let level n = "level", N.to_string n @@ -124,9 +115,7 @@ let meta a = | E.Progress -> "Progress" | E.Private -> "Private" in - let err () = "meta", "" in - let f ms = "meta", String.concat " " (List.rev_map map ms) in - E.meta err f a + "meta", String.concat " " (List.rev_map map a.E.r_meta) let arity l = "arity", string_of_int (List.length l) @@ -137,18 +126,18 @@ let info a = let f lg tx = ["lang", lg; "info", tx] in E.info err f a -let export_entity pp_term (a, u, b) = +let export_entity pp_term (ra, na, u, b) = let path = path_of_uri !G.xdir u in let _ = Sys.command (Printf.sprintf "mkdir -p %s" (F.dirname path)) in let och = open_out (path ^ ext) in let out = output_string och in xml out "1.0" "UTF-8"; doctype out obj_root system; - let a = E.Name (U.name_of_uri u, true) :: a in - let attrs = uri u :: name a :: apix a :: meta a :: info a in + let na = {na with E.n_name = Some (U.name_of_uri u, true)} in + let attrs = uri u :: name na :: apix na :: meta ra :: info ra in let contents = match b with - | E.Abst (n, w) -> tag "GDec" (level n :: attrs) ~contents:(pp_term w) - | E.Abbr v -> tag "GDef" attrs ~contents:(pp_term v) - | E.Void -> assert false + | E.Abst w -> tag "GDec" attrs ~contents:(pp_term w) + | E.Abbr v -> tag "GDef" attrs ~contents:(pp_term v) + | E.Void -> assert false in let opts = if !G.si then "si" else "" in let shp = H.string_of_graph () in @@ -171,7 +160,7 @@ let precs = function let nexts = function | [] -> "next", "" | l -> "next", String.concat " " (List.rev_map next_map l) - +(* let export_csys s = let path = path_of_uri !G.xdir s.Q.buri in let _ = Sys.command (Printf.sprintf "mkdir -p %s" path) in @@ -187,3 +176,4 @@ let export_csys s = in tag ccs_root attrs ~contents out 0; close_out och +*) diff --git a/helm/software/helena/src/xml/xmlLibrary.mli b/helm/software/helena/src/xml/xmlLibrary.mli index 9db373c47..19ce4cfe3 100644 --- a/helm/software/helena/src/xml/xmlLibrary.mli +++ b/helm/software/helena/src/xml/xmlLibrary.mli @@ -16,9 +16,9 @@ type attr = string * string type pp = och -> int -> unit val export_entity: ('term -> pp) -> 'term Entity.entity -> unit - +(* val export_csys: Ccs.csys -> unit - +*) val tag: string -> attr list -> ?contents:pp -> pp val sort: string @@ -45,12 +45,10 @@ val uri: Entity.uri -> attr val level: Level.level -> attr -val name: Entity.attrs -> attr - -val apix: Entity.attrs -> attr +val name: Entity.node_attrs -> attr -val mark: Entity.attrs -> attr +val apix: Entity.node_attrs -> attr -val meta: Entity.attrs -> attr +val meta: Entity.root_attrs -> attr -val info: Entity.attrs -> attr list +val info: Entity.root_attrs -> attr list