let push_abst f y w lenv =
let bw = D.Abst (false, N.infinity, w) in
D.push_bind f E.empty_node y bw lenv
-
+(*
+let rec set_name_y f = function
+ | D.ESort -> f D.ESort
+ | D.EBind (e, a, y, b) -> set_name_y (D.push_bind f a {y with E.b_name = Some ("Y", true)} b) e
+ | D.EAppl (e, x, v) -> set_name_y (D.push_appl f x v) e
+ | D.EProj (e, d) -> let f d = set_name_y (D.push_proj f d) e in set_name_y f d
+*)
let add_proj yt e t = match e with
| D.ESort -> t
| D.EBind (D.ESort, _, y, b) -> D.TBind (E.compose y yt, b, t)
- | _ ->
+ | e ->
D.TProj (D.set_attrs C.start yt e, t)
(* this is not tail recursive in the GRef branch *)
else N.infinity
in
let b = D.Abst (false, l, ww) in
+(* let yt = {yt with E.b_name = Some ("P", true)} in *)
f yt (D.TBind (yt, b, tt))
in
let f lenv = xlate_term f st lst z lenv t in
let y = attrs_for_decl yw in
UH.add henv (uri_of_qid qid) (y, lenv);
let t = add_proj yw lenv ww in
-(*
- print_newline (); CrgOutput.pp_term print_string t;
-*)
let na = E.node_attrs ~apix:lst.line () in
let entity = E.empty_root, na, uri_of_qid qid, E.Abst t in
- G.set_current_trace lst.line;
+IFDEF TRACE THEN
+ G.set_current_trace lst.line
+ELSE () END;
f {lst with line = succ lst.line} entity
in
xlate_term f st lst true lenv w
| A.Def (name, w, trans, v) ->
let f lenv =
let f qid =
- let f _ ww =
+ let f yw ww =
let f yv vv =
UH.add henv (uri_of_qid qid) (yv, lenv);
let t = add_proj yv lenv (D.TCast (ww, vv)) in
(*
- print_newline (); CrgOutput.pp_term print_string t;
+ let lenv0 = D.set_layer C.start N.one lenv in
+ let t = D.TCast (add_proj yw lenv0 ww, add_proj yv lenv vv) in
*)
let na = E.node_attrs ~apix:lst.line () 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, E.Abbr t in
- G.set_current_trace lst.line;
+IFDEF TRACE THEN
+ G.set_current_trace lst.line
+ELSE () END;
f {lst with line = succ lst.line} entity
in
xlate_term f st lst false lenv v