]> matita.cs.unibo.it Git - helm.git/commitdiff
- new attributes system
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Sun, 23 Nov 2014 19:36:06 +0000 (19:36 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Sun, 23 Nov 2014 19:36:06 +0000 (19:36 +0000)
- 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

39 files changed:
helm/software/helena/.depend.opt
helm/software/helena/Makefile
helm/software/helena/src/automath/autCrg.ml
helm/software/helena/src/basic_ag/bag.ml
helm/software/helena/src/basic_ag/bagCrg.ml
helm/software/helena/src/basic_ag/bagEnvironment.ml
helm/software/helena/src/basic_ag/bagOutput.ml
helm/software/helena/src/basic_ag/bagReduction.ml
helm/software/helena/src/basic_ag/bagSubstitution.mli
helm/software/helena/src/basic_ag/bagType.ml
helm/software/helena/src/basic_ag/bagUntrusted.ml
helm/software/helena/src/basic_rg/brg.ml
helm/software/helena/src/basic_rg/brgCrg.ml
helm/software/helena/src/basic_rg/brgEnvironment.ml
helm/software/helena/src/basic_rg/brgOutput.ml
helm/software/helena/src/basic_rg/brgReduction.ml
helm/software/helena/src/basic_rg/brgReduction.mli
helm/software/helena/src/basic_rg/brgType.ml
helm/software/helena/src/basic_rg/brgUntrusted.ml
helm/software/helena/src/basic_rg/brgValidity.ml
helm/software/helena/src/common/Make
helm/software/helena/src/common/alpha.ml
helm/software/helena/src/common/alpha.mli
helm/software/helena/src/common/ccs.ml
helm/software/helena/src/common/ccs.mli
helm/software/helena/src/common/entity.ml
helm/software/helena/src/common/level.ml
helm/software/helena/src/common/level.mli
helm/software/helena/src/common/marks.ml
helm/software/helena/src/common/marks.mli
helm/software/helena/src/common/status.ml
helm/software/helena/src/complete_rg/crg.ml
helm/software/helena/src/complete_rg/crgOutput.ml
helm/software/helena/src/modules.ml
helm/software/helena/src/text/txtCrg.ml
helm/software/helena/src/toplevel/top.ml
helm/software/helena/src/xml/xmlCrg.ml
helm/software/helena/src/xml/xmlLibrary.ml
helm/software/helena/src/xml/xmlLibrary.mli

index 22608ffa0782343bcde9f1df57242a675daa227d..abec726080093d6ef5418e7d95cd8da042dce969 100644 (file)
@@ -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 \
index 690c8c93532643abe8878f7ffa13160e65bbbf85..48e34b90fbf7429469cdee88ca0da753891d4779 100644 (file)
@@ -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
 
index 025459d2e6df9c9595064ed356c585b5a6ccfce1..9093ffbb213e9f38f7d6ffcc81a7dbcf984afb0f 100644 (file)
@@ -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 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 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
index 5e7c07b5b3238d4da9ebbd233712128a94ae74c6..74c305156ecb3c609b06a563ed95b2828d6e83fd 100644 (file)
 (* 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
 
index 1bd5945031249fb9aaa208677b6f7fec016ad02c..9724290f930fae807383420ba90713a658ba5ec9 100644 (file)
@@ -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) ->
index 30e3e992f2ed4f00e8375f0fdfd9c7ff4798545d..24c2126199c5f5a568a4e4944fffb33f6d18ab91 100644 (file)
@@ -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 =
index 4d0a1c07b1b2e834fed3861c84535459ab4a202e..0fbc039b20a228821108cc86d911c806fc1ca06a 100644 (file)
@@ -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)
index c7d89bc84736abc69b1bf345155e807b1ffedaf8..2f4b5a2c7e75af941bf2e9880625a53136a704f2 100644 (file)
@@ -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
index b48c056df33fea395c16c2dec01f29f3f619516d..45325ab4412f29fc325a397f8e2dd6e15d65d862 100644 (file)
@@ -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
index aa4b821a8c1942b3f49e3cba927741e2ab5de983..4a3d37eccdbcf32e111b3cc9d826a15a40b0d19f 100644 (file)
@@ -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) ->
index c27ec5ed1d94e1c8f0f51fa6f4db44009b798cc8..9efbf91824979cdbbd75d3d8a5b8f1d4bb8b27ee 100644 (file)
@@ -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
index c9b5ee41573edfaa56f9a6cd7384ace307aab9d6..eeb9f56d61bdb00ae4d2aab5b0bfa5216659566d 100644 (file)
@@ -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
 
index f646145ed65c2047f66bc3d5f64845fdf2afbc3e..a392afe93b708178be8a727a0444d3092e0c9ab9 100644 (file)
@@ -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 
index d2daed49a26fc96820331ea5416ebf5de3082a5b..a3123caf393bcd839431f743c9f8444a1e1e294e 100644 (file)
@@ -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
index 978658caa0cd6fbf87d144a1275b3e1e877dccbe..aa3cce9524c9719d516dd27e6dad5e0d60db00ab 100644 (file)
@@ -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)           -> 
index 09e262d12eb900caa58f02e4e825df3e4d6c69c2..f397c1c6f5c10ceac594ed4617ff6a164757b836 100644 (file)
@@ -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
index e73d2df8a8508d793a80182e938c13398d6cabeb..56fbf772343cdffc2aa6efbbeb37db44b0f3a299 100644 (file)
@@ -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 
 
index 29b73beeb587c85bc58f2918e7ec652132c3648c..5ba07c876355a1e63e8ec3b4c1c6f93873b1285f 100644 (file)
@@ -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
index 88edd46d8dee15f0a559da19014ac33653fdd6e6..87a3f60cfff3942573016435c7466cc5597235f2 100644 (file)
@@ -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
index e358d5a1909304faea2c84187ac0c9ed71ca14a0..c83c5e87f12fa4602b18f46541479e5120280ff7 100644 (file)
@@ -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) ->
index 7be0f01c2d5ab26f367a7f40c5d517f26e06868a..71d85f4f3c3138293b2dde216689de3fcbe94751 100644 (file)
@@ -1 +1 @@
-hierarchy level entity options output marks alpha ccs status 
+marks hierarchy level entity options output alpha ccs status 
index 1eb6b106383c0a1623a2a47430ac11dbe62bb61f..8da7e563b970eedd2a16efb3162476c0b63f2e6f 100644 (file)
 
 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
index a08e98e5963ca40ea05a96fac71fc23819912b02..cf0fafd05b77cc0d69003b1aef1e73b5a307603b 100644 (file)
@@ -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
index 5364d1e079b61402d8d6a89231bc087c0afaaa5a..d003d805ce6a87cd21d09b46b511efb4a0eb74e0 100644 (file)
@@ -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 ()
+*)
index f263d8a089542eaf121d7e0e0bf31a1bc8649695..83061e6e5e1361f6a6b0507a852d6b78db98a0ab 100644 (file)
@@ -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
+*)
index 9915dd3c37b385ef42b6cebf992feebf228ddb34..c447190501854daee08e11455956be0ae1477105 100644 (file)
@@ -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
index b10dda06a4b83f30618790322dd2e5459c3bf49f..60f7ac4381b6d2c0e2ccaefde91229d0a6cb231d 100644 (file)
@@ -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
index 9b4955248726eaffd5689491ee31e6af2af79227..4bae584fa8843ead6401d1d4260b9e54a207ebad 100644 (file)
@@ -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
 
index fba716b37494560fc7d9063e437a821191fafff9..5b45cc79f24a8cb8657e918b34ce938c7dff964a 100644 (file)
@@ -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
index ff5a681093d790adeafa7a01f7916d9fd0895e78..b4bafe680eb692c03914ade7437caf0de56ecf99 100644 (file)
@@ -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
index 3ae3136089d6ae9239bf571217c14df9dd80c01f..a076a9aae69e35dffee8b0cf570c9c8209346f12 100644 (file)
@@ -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 () *)
 }
index 7ba80ddfb39a7c01156f656b75fc41f7b37c31c0..0acd43336d090ee42a3c096d300287623036c296 100644 (file)
@@ -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 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
index d5f639b392d6721e45c2cee02f1b1764b9040389..529a293e1a79d737d8775a9ec96f51e83330dcc9 100644 (file)
@@ -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 "[]"
 
index 6f795219f271605536fca588af7e9f29859fe824..b0524922446194002ee7e1b3e4fbce5b402db7dc 100644 (file)
@@ -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
index a6839b89cc747e5c55a78f8437ce3995e0ff8322..63b7725b25d2f1521a3e4662c1126ff88001e14c 100644 (file)
@@ -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))
index afa62555dfb68bcc04d6df64172c0d5f511963d1..d64857d324cc878c4b216522e8ccbbf0ff7861f6 100644 (file)
@@ -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 = 
index ce14855e0abd4b21bd68ea20116d255a545f6e9f..2e10553cb25e3f76841387afbf2aeaae6d0afbc0 100644 (file)
@@ -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
index e182ab9a39d20d45fac636194f42267b7eee3c44..1e2bd4de4d5e015ff100fcc6f09e3c5794a89059 100644 (file)
@@ -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
+*)
index 9db373c4724a76cae9f8a391833478e1eb20fc01..19ce4cfe3564357aca2e74695807f847f46e0fdc 100644 (file)
@@ -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