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 = {
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 *)
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
| 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 *)
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
| 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
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
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
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
projects / helm.git / blobdiff