X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fhelena%2Fsrc%2Fautomath%2FautCrg.ml;h=5ed896306dfcf0558d6858ad499f57398b3f94f0;hb=f7d7f2459b3b0409be5f168822be3b836ccc929b;hp=69a8c072d2282921b958e0a96f516c1d93c761a9;hpb=39cf453a20e35416d0fd932cc5bf14733e918587;p=helm.git

diff --git a/helm/software/helena/src/automath/autCrg.ml b/helm/software/helena/src/automath/autCrg.ml
index 69a8c072d..5ed896306 100644
--- a/helm/software/helena/src/automath/autCrg.ml
+++ b/helm/software/helena/src/automath/autCrg.ml
@@ -9,16 +9,14 @@
      \ /   This software is distributed as is, NO WARRANTY.              
       V_______________________________________________________________ *)
 
-module U = NUri
-module K = U.UriHash
-module C = Cps
-module J = Marks
-module N = Level
-module E = Entity
-module G = Options
-module S = Status
-module A = Aut
-module D = Crg
+module U  = NUri
+module UH = U.UriHash
+module C  = Cps
+module G  = Options
+module N  = Layer
+module E  = Entity
+module A  = Aut
+module D  = Crg
 
 (* qualified identifier: uri, name, qualifiers *)
 type qid = D.uri * D.id * D.id list
@@ -35,21 +33,35 @@ type status = {
 
 let henv_size, hcnt_size = 7000, 4300 (* hash tables initial sizes *)
 
-let henv = K.create henv_size (* optimized global environment *)
+let henv = UH.create henv_size (* optimized global environment *)
 
-let hcnt = K.create hcnt_size (* optimized context *)
+let hcnt = UH.create hcnt_size (* optimized context *)
 
 (* Internal functions *******************************************************)
 
-let empty_cnt = D.ESort
+let empty_cnt = D.empty_lenv
 
-let add_abst cnt id d w =
-   let a = E.node_attrs ~name:(id, true) ~degr:(succ d) () in 
-   D.EBind (cnt, a, D.Abst (N.two, w)) 
+let alpha id =
+   if id.[0] >= '0' && id.[0] <= '9' then !G.alpha ^ id else id
 
-let mk_lref f a i = f a.E.n_degr (D.TLRef (E.empty_node, i))
+let attrs_for_abst id aw =
+   let id = if !G.alpha <> "" then alpha id else id in
+   let main = E.succ aw.E.b_main in
+   E.bind_attrs ~name:(id, true) ~side:aw.E.b_main ~main ()
 
-let id_of_name (id, _, _) = id
+let attrs_for_decl aw =
+   let main = E.succ aw.E.b_main in
+   E.bind_attrs ~side:aw.E.b_main ~main ()
+
+let add_abst cnt id aw w =
+   let y = attrs_for_abst id aw in
+   let l = if !G.infinity then N.infinity else N.two in
+   D.EBind (cnt, E.empty_node, y, D.Abst (false, l, w))
+
+let mk_lref f _ y i = f y (D.TLRef (E.empty_node, i))
+
+let id_of_name (id, _, _) =
+   if !G.alpha <> "" then alpha id else id
 
 let mk_qid f lst id path =
    let str = String.concat "/" path in
@@ -80,7 +92,7 @@ let relax_opt_qid f lst = function
    | Some qid -> let f qid = f (Some qid) in relax_qid f lst qid
 
 let resolve_gref err f lst qid =
-   try let a, cnt = K.find henv (uri_of_qid qid) in f qid a cnt
+   try let y, cnt = UH.find henv (uri_of_qid qid) in f qid y cnt
    with Not_found -> err qid
 
 let resolve_gref_relaxed f lst qid =
@@ -91,7 +103,7 @@ let resolve_gref_relaxed f lst qid =
 let get_cnt err f lst = function
    | None             -> f empty_cnt
    | Some qid as node ->
-      try let cnt = K.find hcnt (uri_of_qid qid) in f cnt
+      try let cnt = UH.find hcnt (uri_of_qid qid) in f cnt
       with Not_found -> err node
 
 let get_cnt_relaxed f lst =
@@ -99,55 +111,68 @@ let get_cnt_relaxed f lst =
    let rec err node = relax_opt_qid (get_cnt err f lst) lst node in
    get_cnt err f lst lst.node
 
-let push_abst f a w lenv =
-   let bw = D.Abst (N.infinite, w) in
-   D.push_bind f a bw lenv
-
-let add_proj e t = match e with
-   | D.ESort                 -> t
-   | D.EBind (D.ESort, a, b) -> D.TBind (a, b, t) 
-   | _                       -> D.TProj (E.empty_node, e, t)
+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 *)
-let rec xlate_term f st lst y lenv = function
+let rec xlate_term f st lst z 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 k = if s then 0 else 1 in
+      let y = E.bind_attrs ~main:(k, 0) () in
+      f y (D.TSort k)
    | A.Appl (v, t)       ->
-      let f vv d tt = f d (D.TAppl (E.empty_node, vv, tt)) in
-      let f _ vv = xlate_term (f vv) st lst y lenv t in
+      let f vv yt tt =
+         f yt (D.TAppl (!G.extended, vv, tt))
+      in
+      let f _ vv = xlate_term (f vv) st lst z lenv t in
       xlate_term f st lst false lenv v
    | A.Abst (name, w, t) ->
-      let f d ww = 
-         let a = E.node_attrs ~name:(name, true) () in
-	 let f d tt =
-            let l = if !G.cc then match y, d with
-               | true, _ -> N.one
-               | _   , 0 -> N.one
-               | _   , 1 -> N.unknown st.S.lenv (J.new_mark ())
-               | _   , 2 -> N.two
-               | _       -> assert false
-               else N.infinite
+      let f yw ww =
+         let yw = attrs_for_abst name yw in
+         let f yt tt =
+	    let yt = E.compose yw yt in
+            let l = 
+               if !G.cc then match z, snd yt.E.b_main with
+                  | true, _ -> N.one
+                  | _   , 0 -> N.one
+                  | _   , 1 -> N.unknown st
+                  | _   , 2 -> N.two
+                  | _       -> assert false
+               else N.infinity
             in
-	    let b = D.Abst (l, ww) in
-	    f d (D.TBind (a, b, tt))
+	    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 y lenv t in
-	 push_abst f {a with E.n_degr = succ d} ww lenv
+         let f lenv = xlate_term f st lst z lenv t in
+	 push_abst f yw ww lenv
       in
       xlate_term f st lst true lenv w
    | A.GRef (name, args) ->
       let map1 args (id, _) = A.GRef ((id, true, []), []) :: args in
       let map2 f arg args = 
-         let f _ arg = f (D.EAppl (args, E.empty_node, arg)) in 
+         let f _ v = f (D.EAppl (args, !G.extended, v)) in 
          xlate_term f st lst false lenv arg
       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
+      let g qid y cnt =
+         let gref = D.TGRef (E.empty_node, uri_of_qid qid) in
+	 if cnt = D.ESort then f y gref else
 	 let f = function 
-            | D.EAppl (D.ESort, a, v) -> f a.E.n_degr (D.TAppl (a, v, gref))
-            | args                    -> f a.E.n_degr (D.TProj (E.empty_node, args, gref))
+            | D.EAppl (D.ESort, x, v) -> f y (D.TAppl (x, v, gref))
+            | args                    -> f y (D.TProj (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
@@ -173,11 +198,11 @@ let xlate_entity err f st lst = function
    | A.Block (name, w)         ->
       let f qid = 
          let f cnt =
-	    let f d ww = 
-	       K.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
@@ -185,36 +210,40 @@ 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
-               K.add henv (uri_of_qid qid) (a, 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 f yw ww =
+               let y = attrs_for_decl yw in
+               UH.add henv (uri_of_qid qid) (y, lenv);
+	       let t = add_proj yw lenv ww in
+               let na = E.node_attrs ~apix:lst.line () in
+	       let entity = E.empty_root, na, uri_of_qid qid, E.Abst t in
+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
 	 in
          complete_qid f lst (name, true, [])
       in
+      let f = if !G.infinity then f else D.set_layer f N.one in 
       get_cnt_relaxed f lst
    | A.Def (name, w, trans, v) ->
       let f lenv =
          let f qid = 
-            let f _ ww =
-	       let f d vv =
-                  let na = E.node_attrs ~apix:lst.line ~degr:d () in
-                  K.add henv (uri_of_qid qid) (na, lenv);
-                  let t = add_proj lenv (D.TCast (E.empty_node, ww, vv)) in
+            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 b = E.Abbr t 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, b in
+	          let entity = ra, na, uri_of_qid qid, E.Abbr t in
+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
@@ -228,12 +257,10 @@ let xlate_entity err f st lst = function
 (* Interface functions ******************************************************)
 
 let initial_status () =
-   K.clear henv; K.clear hcnt; {
+   UH.clear henv; UH.clear hcnt; {
    path = []; node = None; nodes = []; line = 1; mk_uri = G.get_mk_uri ();
 }
 
-let refresh_status lst = {lst with
-   mk_uri = G.get_mk_uri ()
-}
+let refresh_status lst = initial_status ()
 
 let crg_of_aut = xlate_entity