path : T.id list; (* current section path *)
line : int; (* line number *)
sort : int; (* first default sort index *)
+ rest : bool; (* restricted applications *)
mk_uri: G.uri_generator (* uri generator *)
}
(* Internal functions *******************************************************)
-let mk_lref f a i = f a (D.TLRef (a, i))
+let mk_lref f a y i = f y (D.TLRef (a, i))
-let mk_gref f a uri = f a (D.TGRef (a, uri))
+let mk_gref f y uri = f y (D.TGRef (E.empty_node, uri))
let get err f e i = match D.get e i with
- | _, _, D.Void -> err ()
- | _, a, _ -> mk_lref f a i
+ | _, _, _, D.Void -> err ()
+ | _, a, y, _ -> mk_lref f a y i
let resolve_gref err f st id =
try
- let a, uri = KH.find henv id in f a uri
+ let y, uri = KH.find henv id in f y uri
with Not_found -> err ()
let name_of_id ?(r=true) id =
CrgOutput.pp_lenv print_string (Layer.initial_status ()) lenv;
Printf.printf "\n";
*)
- | T.Sort h ->
- let a = E.node_attrs ~sort:h () in
- f a (D.TSort (a, h))
+ | T.Sort k ->
+ let y = E.bind_attrs ~main:(k, 0) () in
+ f y (D.TSort k)
| T.NSrt id ->
let f h = xlate_term f st lenv (T.Sort h) in
H.sort_of_string (xerr "sort not found") f id
let err () = resolve_gref (xerr "global constant not found") (mk_gref f) st id in
D.resolve_lref err (mk_lref f) id lenv
| T.Cast (u, t) ->
- let f uu a tt = f a (D.TCast (a, uu, tt)) in
+ let f uu y tt = f y (D.TCast (uu, tt)) in
let f _ uu = xlate_term (f uu) st lenv t in
xlate_term f st lenv u
| T.Appl (v, t) ->
- let f vv a tt = f a (D.TAppl (a, vv, tt)) in
+ let f vv y tt = f y (D.TAppl (E.appl_attrs st.rest, vv, tt)) in
let f _ vv = xlate_term (f vv) st lenv t in
xlate_term f st lenv v
| T.Proj (bs, t) ->
- let f e a tt = f a (D.TProj (a, e, tt)) in
+ let f e y tt = f y (D.TProj (e, tt)) in
let f (lenv, e) = xlate_term (f e) st lenv t in
C.list_fold_left f (xlate_bind st) (lenv, D.empty_lenv) bs
| T.Inst (t, vs) ->
let map f v e =
- let f _ vv = D.push_appl f E.empty_node vv e in
+ let f _ vv = D.push_appl f (E.appl_attrs st.rest) vv e in
xlate_term f st lenv v
in
- let f e a tt = f a (D.TProj (a, e, tt)) in
+ let f e y tt = f y (D.TProj (e, tt)) in
let f e = xlate_term (f e) st lenv t in
C.list_fold_right f map vs D.empty_lenv
and xlate_bind st f (lenv, e) b =
let f lenv e = f (lenv, e) in
- let f a b lenv = D.push_bind (f lenv) a b e in
- let f a b = D.push_bind (f a b) a b lenv in
+ let f y b lenv = D.push_bind (f lenv) E.empty_node y b e in
+ let f y b = D.push_bind (f y b) E.empty_node y b lenv in
match b with
| T.Abst (n, id, r, w) ->
- let f a ww =
- let a = {a with E.n_name = name_of_id ~r id} in
- f a (D.Abst (n, ww))
+ let f y ww =
+ let y = E.bind_attrs ?name:(name_of_id id) () in
+ f y (D.Abst (false, n, ww))
in
xlate_term f st lenv w
| T.Abbr (id, v) ->
- let f a vv =
- let a = {a with E.n_name = name_of_id id} in
- f a (D.Abbr vv)
+ let f y vv =
+ let y = E.bind_attrs ?name:(name_of_id id) () in
+ f y (D.Abbr vv)
in
xlate_term f st lenv v
| T.Void id ->
- let a = E.node_attrs ?name:(name_of_id id) ~sort:st.sort () in
- f a D.Void
+ let y = E.bind_attrs ?name:(name_of_id id) ~main:(st.sort, 0) () in
+ f y D.Void
let mk_contents main kind tt =
let ms, b = match kind with
- | T.Decl -> [] , E.Abst tt
- | T.Ax -> [E.InProp] , E.Abst tt
- | T.Cong -> [E.InProp; E.Progress], E.Abst tt
- | T.Def -> [] , E.Abbr tt
- | T.Th -> [E.InProp] , E.Abbr tt
+ | T.Decl -> [] , E.abst E.empty_env tt
+ | T.Ax -> [E.InProp] , E.abst E.empty_env tt
+ | T.Cong -> [E.InProp; E.Progress], E.abst E.empty_env tt
+ | T.Def -> [] , E.abbr E.empty_env tt
+ | T.Th -> [E.InProp] , E.abbr E.empty_env tt
in
if main then E.Main :: ms, b else ms, b
assert (H.set_graph id); err st
| T.Constant (main, kind, id, info, t) ->
let uri = uri_of_id st id st.path in
- let g na tt =
+ let g ya tt =
+ KH.add henv id (ya, uri);
(*
print_newline (); CrgOutput.pp_term print_string tt;
*)
- let na = {na with E.n_apix = st.line} in
- KH.add henv id (na, uri);
let meta, b = mk_contents main kind tt in
+ let na = E.node_attrs ~apix:st.line () in
let ra = E.root_attrs ~meta ~info () in
let entity = ra, na, uri, b in
f {st with line = succ st.line} entity
-
in
xlate_term g st D.empty_lenv t
| T.Generate _ ->
let initial_status () =
KH.clear henv; {
- path = []; line = 1; sort = 0; mk_uri = G.get_mk_uri ()
+ path = []; line = 1; sort = 0; rest = true; mk_uri = G.get_mk_uri ()
}
let refresh_status st = {st with