- helena: the improved attribute system allows to export the sorts of Pi's

[helm.git] / helm / software / helena / src / automath / autCrg.ml

diff --git a/helm/software/helena/src/automath/autCrg.ml b/helm/software/helena/src/automath/autCrg.ml
index fe562480d68db7be0d5721b55865eebe45f8310a..1c2759d15d7cdfa06f1ef55239e8d11013ebd6ab 100644 (file)
--- a/helm/software/helena/src/automath/autCrg.ml
+++ b/helm/software/helena/src/automath/autCrg.ml
@@ -45,12 +45,12 @@ let empty_cnt = D.empty_lenv
 let alpha id =
    if id.[0] >= '0' && id.[0] <= '9' then !G.alpha ^ id else id
 
-let add_abst cnt id d w =
+let add_abst cnt id aw w =
    let id = if !G.alpha <> "" then alpha id else id in
-   let a = E.node_attrs ~name:(id, true) ~degr:(succ d) () in 
-   D.EBind (cnt, a, D.Abst (N.two, w)) 
+   let aw = {aw with E.n_name = Some (id, true); E.n_degr = succ aw.E.n_degr} in 
+   D.EBind (cnt, aw, D.Abst (N.two, w))
 
-let mk_lref f a i = f a.E.n_degr (D.TLRef (E.empty_node, i))
+let mk_lref f a i = f a (D.TLRef (a, i))
 
 let id_of_name (id, _, _) =
    if !G.alpha <> "" then alpha id else id
@@ -115,19 +115,19 @@ let add_proj e t = match e with
 (* this is not tail recursive in the GRef branch *)
 let rec xlate_term f st lst y lenv = function
    | A.Sort s            ->
-      let f h = f 0 (D.TSort (E.empty_node, h)) in
-      if s then f 0 else f 1
+      let h = if s then 0 else 1 in
+      let a = E.node_attrs ~sort:h () in
+      f a (D.TSort (a, h))
    | A.Appl (v, t)       ->
-      let f vv d tt = f d (D.TAppl (E.empty_node, vv, tt)) in
+      let f vv at tt = f at (D.TAppl (at, vv, tt)) in
       let f _ vv = xlate_term (f vv) st lst y lenv t in
       xlate_term f st lst false lenv v
    | A.Abst (name, w, t) ->
       let name = if !G.alpha <> "" then alpha name else name in
-      let f dw ww = 
-         let a = E.node_attrs ~name:(name, true) () in
-         let f dt tt =
-(*         let a = {a with E.n_degr = dt} in *)
-            let l = if !G.cc then match y, dt with
+      let name = Some (name, true) in
+      let f aw ww = 
+         let f at tt =
+            let l = if !G.cc then match y, at.E.n_degr with
                | true, _ -> N.one
                | _   , 0 -> N.one
                | _   , 1 -> N.unknown st.S.lenv
@@ -136,10 +136,11 @@ let rec xlate_term f st lst y lenv = function
                else N.infinite
             in
            let b = D.Abst (l, ww) in
-           f dt (D.TBind (a, b, tt))
+           let at = {at with E.n_name = name} in
+           f at (D.TBind (at, b, tt))
         in
          let f lenv = xlate_term f st lst y lenv t in
-        push_abst f {a with E.n_degr = succ dw} ww lenv
+        push_abst f {aw with E.n_name = name; E.n_degr = succ aw.E.n_degr} ww lenv
       in
       xlate_term f st lst true lenv w
    | A.GRef (name, args) ->
@@ -150,10 +151,10 @@ let rec xlate_term f st lst y lenv = function
       in
       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
+        if cnt = D.ESort then f a gref else
         let f = function 
-            | D.EAppl (D.ESort, b, v) -> f a.E.n_degr (D.TAppl (b, v, gref))
-            | args                    -> f a.E.n_degr (D.TProj (E.empty_node, args, gref))
+            | D.EAppl (D.ESort, _, v) -> f a (D.TAppl (a, v, gref))
+            | args                    -> f a (D.TProj (a, args, gref))
          in
         let f args = C.list_fold_right f map2 args D.ESort in
         D.sub_list_strict (D.fold_names f map1 args) cnt args
@@ -179,11 +180,11 @@ let xlate_entity err f st lst = function
    | A.Block (name, w)         ->
       let f qid = 
          let f cnt =
-           let f d ww = 
-              UH.add hcnt (uri_of_qid qid) (add_abst cnt name d ww);
+           let f aw ww = 
+              UH.add hcnt (uri_of_qid qid) (add_abst cnt name aw ww);
               err {lst with node = Some qid}
            in
-           xlate_term f st lst true cnt w
+            xlate_term f st lst true cnt w
         in
          get_cnt_relaxed f lst
       in
@@ -191,15 +192,15 @@ let xlate_entity err f st lst = function
    | A.Decl (name, w)          ->
       let f lenv =
         let f qid = 
-            let f d ww =
-               let a = E.node_attrs ~apix:lst.line ~degr:(succ d) () in
-               UH.add henv (uri_of_qid qid) (a, lenv);
+            let f aw ww =
+               let aw = {aw with E.n_apix = lst.line; E.n_degr = succ aw.E.n_degr} in
+               UH.add henv (uri_of_qid qid) (aw, lenv);
               let t = add_proj lenv ww in
 (*
            print_newline (); CrgOutput.pp_term print_string t;
 *)
               let b = E.Abst t in
-              let entity = E.empty_root, a, uri_of_qid qid, b in
+              let entity = E.empty_root, aw, uri_of_qid qid, b in
               f {lst with line = succ lst.line} entity
            in
            xlate_term f st lst true lenv w
@@ -211,10 +212,10 @@ let xlate_entity err f st lst = function
       let f lenv =
          let f qid = 
             let f _ ww =
-              let f d vv =
-                  let na = E.node_attrs ~apix:lst.line ~degr:d () in
+              let f av vv =
+                  let na = {av with E.n_apix = lst.line} in
                   UH.add henv (uri_of_qid qid) (na, lenv);
-                  let t = add_proj lenv (D.TCast (E.empty_node, ww, vv)) in
+                  let t = add_proj lenv (D.TCast (na, ww, vv)) in
 (*
            print_newline (); CrgOutput.pp_term print_string t;
 *)