\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
+module KF = Filename
+module KH = Hashtbl
+module KL = List
+
module U = NUri
-module H = Hierarchy
module C = Cps
module G = Options
+module H = Hierarchy
module E = Entity
module T = Txt
-module TT = TxtTxt
module D = Crg
type status = {
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 *)
}
let henv_size = 7000 (* hash tables initial size *)
-let henv = Hashtbl.create henv_size (* optimized global environment *)
+let henv = KH.create henv_size (* optimized global environment *)
+
+let xerr s () =
+ Printf.printf "%s\n%!" s; C.err ()
(* Internal functions *******************************************************)
-(*
-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_lref f a y i = f y (D.TLRef (a, i))
+
+let mk_gref f y uri = f y (D.TGRef (E.empty_node, uri))
-let mk_gref f uri = f (D.TGRef ([], uri))
+let get err f e i = match D.get e i with
+ | _, _, _, D.Void -> err ()
+ | _, a, y, _ -> mk_lref f a y i
+
+let resolve_gref err f st id =
+ try
+ let y, uri = KH.find henv id in f y uri
+ with Not_found -> err ()
+
+let name_of_id ?(r=true) id =
+ if id = "" then None else Some (id, r)
let uri_of_id st id path =
let str = String.concat "/" path in
- let str = Filename.concat str id in
+ let str = KF.concat str id in
let str = st.mk_uri str in
U.uri_of_string str
-let resolve_gref err f st id =
- try f (Hashtbl.find henv id)
- with Not_found -> err ()
-
let rec xlate_term f st lenv = function
- | T.Inst _
- | T.Impl _ -> assert false
- | T.Sort h ->
- f (D.TSort ([], h))
- | T.NSrt id ->
- let f h = f (D.TSort ([], h)) in
- H.sort_of_string C.err f id
- | T.LRef (i, j) ->
- D.get_index C.err (mk_lref f i j) i j lenv
+(*
+ CrgOutput.pp_lenv print_string (Layer.initial_status ()) lenv;
+ Printf.printf "\n";
+*)
+ | 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
+ | T.LRef i ->
+ get (xerr "index out of bounds") f lenv i
| T.NRef id ->
- let err () = resolve_gref C.err (mk_gref f) st id in
+ 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 tt = f (D.TCast ([], uu, tt)) in
- let f uu = xlate_term (f uu) st lenv t 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 (vs, t) ->
- let map f = xlate_term f st lenv in
- let f vvs tt = f (D.TAppl ([], vvs, tt)) in
- let f vvs = xlate_term (f vvs) st lenv t in
- C.list_map f map vs
- | T.Bind (n, b, t) ->
- let abst_map (lenv, a, wws) (id, r, w) =
- let attr = name_of_id ~r id in
- let ww = xlate_term C.start st lenv w in
- D.push2 C.err C.start lenv ~attr ~t:ww (), attr :: a, ww :: wws
- in
- let abbr_map (lenv, a, wws) (id, w) =
- let attr = name_of_id id in
- let ww = xlate_term C.start st lenv w in
- D.push2 C.err C.start lenv ~attr ~t:ww (), attr :: a, ww :: wws
- in
- let void_map (lenv, a, n) id =
- let attr = name_of_id id in
- D.push2 C.err C.start lenv ~attr (), attr :: a, succ n
- in
- let lenv, aa, bb = match b with
- | T.Abst xws ->
- let lenv = D.push_bind C.start lenv [] (D.Abst (n, [])) in
- let lenv, aa, wws = List.fold_left abst_map (lenv, [], []) xws in
- lenv, aa, D.Abst (n, wws)
- | T.Abbr xvs ->
- let lenv = D.push_bind C.start lenv [] (D.Abbr []) in
- let lenv, aa, vvs = List.fold_left abbr_map (lenv, [], []) xvs in
- lenv, aa, D.Abbr vvs
- | T.Void ids ->
- let lenv = D.push_bind C.start lenv [] (D.Void 0) in
- let lenv, aa, n = List.fold_left void_map (lenv, [], 0) ids in
- lenv, aa, D.Void n
+ | T.Appl (v, t) ->
+ 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 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.appl_attrs st.rest) vv e in
+ xlate_term f st lenv v
in
- let f tt = f (D.TBind (aa, bb, tt)) in
- xlate_term f st lenv t
-
-let xlate_term f st lenv t =
- TT.contract (xlate_term f st lenv) t
-
-let mk_contents n tt = function
- | T.Decl -> [] , E.Abst (n, tt)
- | T.Ax -> [E.InProp] , E.Abst (n, tt)
- | T.Cong -> [E.InProp; E.Progress], E.Abst (n, tt)
- | T.Def -> [] , E.Abbr tt
- | T.Th -> [E.InProp] , E.Abbr tt
+ 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 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 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 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 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 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
let xlate_entity err f gen st = function
- | T.Require _ ->
+ | T.Require _ ->
err st
- | T.Section (Some name) ->
+ | T.Section (Some name) ->
err {st with path = name :: st.path}
- | T.Section None ->
+ | T.Section None ->
begin match st.path with
| _ :: ptl ->
err {st with path = ptl}
| _ -> assert false
end
- | T.Sorts sorts ->
+ | T.Sorts sorts ->
let map st (xix, s) =
let ix = match xix with
| None -> st.sort
in
{st with sort = H.set_sorts ix [s]}
in
- err (List.fold_left map st sorts)
- | T.Graph id ->
+ err (KL.fold_left map st sorts)
+ | T.Graph id ->
assert (H.set_graph id); err st
- | T.Entity (main, kind, n, id, info, t) ->
+ | T.Constant (main, kind, id, info, t) ->
let uri = uri_of_id st id st.path in
- Hashtbl.add henv id uri;
- let tt = xlate_term C.start st D.empty_lenv t in
+ let g ya tt =
+ KH.add henv id (ya, uri);
(*
- print_newline (); CrgOutput.pp_term print_string tt;
-*)
- let a = [] in
- let ms, b = mk_contents n tt kind in
- let ms = if main then E.Main :: ms else ms in
- let a = if ms <> [] then E.Meta ms :: a else a in
- let a = if info <> ("", "") then E.Info info :: a else a in
- let entity = E.Mark st.line :: a, uri, b in
- f {st with line = succ st.line} entity
- | T.Generate _ ->
+ print_newline (); CrgOutput.pp_term print_string tt;
+*)
+ 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 _ ->
err st
(* Interface functions ******************************************************)
-*)
+
let initial_status () =
- Hashtbl.clear henv; {
- path = []; line = 1; sort = 0; mk_uri = G.get_mk_uri ()
+ KH.clear henv; {
+ path = []; line = 1; sort = 0; rest = true; mk_uri = G.get_mk_uri ()
}
let refresh_status st = {st with
mk_uri = G.get_mk_uri ()
}
-let crg_of_txt _ _ = assert false (* xlate_entity *)
+let crg_of_txt = xlate_entity
projects / helm.git / blobdiff