update in helena

[helm.git] / helm / software / helena / src / text / txtCrg.ml

diff --git a/helm/software/helena/src/text/txtCrg.ml b/helm/software/helena/src/text/txtCrg.ml
index b2d0c99e1630aa54641e6cbeb1561e41ebb573ca..4580d2d867eb7b29ec5dbf4de2e5b3da5129deae 100644 (file)
--- a/helm/software/helena/src/text/txtCrg.ml
+++ b/helm/software/helena/src/text/txtCrg.ml
@@ -25,7 +25,7 @@ type status = {
    path  : T.id list;      (* current section path *)
    line  : int;            (* line number *)
    sort  : int;            (* first default sort index *)
-   ext   : bool;           (* extended applications *) 
+   rest  : bool;           (* restricted applications *) 
    mk_uri: G.uri_generator (* uri generator *) 
 }
 
@@ -38,17 +38,17 @@ let xerr s () =
 
 (* 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 =
@@ -65,9 +65,9 @@ let rec xlate_term f st lenv = function
    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
@@ -77,54 +77,54 @@ let rec xlate_term f st lenv = function
       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, st.ext, 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 st.ext 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 (false, 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
 
@@ -152,17 +152,16 @@ let xlate_entity err f gen st = function
       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 _                         ->
@@ -172,7 +171,7 @@ let xlate_entity err f gen st = function
 
 let initial_status () =
    KH.clear henv; {
-   path = []; line = 1; sort = 0; ext = false; 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