X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fhelena%2Fsrc%2Fautomath%2FautCrg.ml;h=d1a72518b2d053636bbc639eb30d434854322950;hb=88977b2d546e547e23b046792fe2ad8f6ff192a4;hp=548e1ec73ad7094f60d9455d3cf960ab5ae75db1;hpb=95872555aaa040a22ad2d93cb1278f79e20da70c;p=helm.git

diff --git a/helm/software/helena/src/automath/autCrg.ml b/helm/software/helena/src/automath/autCrg.ml
index 548e1ec73..d1a72518b 100644
--- a/helm/software/helena/src/automath/autCrg.ml
+++ b/helm/software/helena/src/automath/autCrg.ml
@@ -9,235 +9,260 @@
      \ /   This software is distributed as is, NO WARRANTY.              
       V_______________________________________________________________ *)
 
-module U = NUri
-module K = U.UriHash
-module C = Cps
-module G = Options
-module E = Entity
-module N = Level
-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
 
-type context = E.attrs * D.term list
-
 type context_node = qid option (* context node: None = root *)
 
 type status = {
-   path: D.id list;          (* current section path *) 
+   path: D.id list;          (* current section path *)
    node: context_node;       (* current context node *)
    nodes: context_node list; (* context node list *)
    line: int;                (* line number *)
-   mk_uri:G.uri_generator    (* uri generator *) 
+   mk_uri: G.uri_generator;  (* uri generator *)
 }
 
-type resolver = Local of int
-              | Global of context
-
 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 = [], []
+let empty_cnt = D.empty_lenv
+
+let alpha id =
+   if id.[0] >= '0' && id.[0] <= '9' then !G.alpha ^ id else id
+
+let attrs_for_appl yv yt =
+   E.appl_attrs ~side:yv ~main:yt !G.restricted
+
+let attrs_for_abst id yw =
+   let id = if !G.alpha <> "" then alpha id else id in
+   E.bind_attrs ~name:(id, true) ~side:yw ~main:(E.succ yw) ()
 
-let add_abst (a, ws) id w = 
-   E.Name (id, true) :: a, w :: ws 
+let attrs_for_env y =
+   E.env_attrs ~side:y ()
 
-let mk_lref f i j k = f (D.TLRef ([E.Apix k], i, j))
+let add_abst cnt id yw w =
+   let a = attrs_for_abst id yw in
+   let l = if !G.infinity then N.infinity else N.two in
+   D.EBind (cnt, E.empty_node, a, D.Abst (false, l, w))
 
-let id_of_name (id, _, _) = id
+let mk_lref f _ a i = f a.E.b_main (D.TLRef (E.empty_node, i))
 
-let mk_qid f st id path =
+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
-   let str = Filename.concat str id in 
-   let str = st.mk_uri str in
+   let str = Filename.concat str id in
+   let str = lst.mk_uri str in
    f (U.uri_of_string str, id, path)
 
 let uri_of_qid (uri, _, _) = uri
 
-let complete_qid f st (id, is_local, qs) =
-   let f path = C.list_rev_append (mk_qid f st id) path ~tail:qs in
+let complete_qid f lst (id, is_local, qs) =
+   let f path = C.list_rev_append (mk_qid f lst id) path ~tail:qs in
    let rec skip f = function
       | phd :: ptl, qshd :: _ when phd = qshd -> f ptl
       | _ :: ptl, _ :: _                      -> skip f (ptl, qs)
       | _                                     -> f []
    in
-   if is_local then f st.path else skip f (st.path, qs)
+   if is_local then f lst.path else skip f (lst.path, qs)
 
-let relax_qid f st (_, id, path) =
+let relax_qid f lst (_, id, path) =
    let f = function
-      | _ :: tl -> C.list_rev (mk_qid f st id) tl
+      | _ :: tl -> C.list_rev (mk_qid f lst id) tl
       | []      -> assert false
    in
    C.list_rev f path
 
-let relax_opt_qid f st = function
+let relax_opt_qid f lst = function
    | None     -> f None
-   | Some qid -> let f qid = f (Some qid) in relax_qid f st qid
+   | Some qid -> let f qid = f (Some qid) in relax_qid f lst qid
 
-let resolve_gref err f st qid =
-   try let cnt = K.find henv (uri_of_qid qid) in f qid cnt
-   with Not_found -> err qid 
+let resolve_gref err f lst qid =
+   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 st qid =
-(* this is not tail recursive *)   
-   let rec err qid = relax_qid (resolve_gref err f st) st qid in
-   resolve_gref err f st qid
+let resolve_gref_relaxed f lst qid =
+(* this is not tail recursive *)
+   let rec err qid = relax_qid (resolve_gref err f lst) lst qid in
+   resolve_gref err f lst qid
 
-let get_cnt err f st = function
+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 st =
-(* this is not tail recursive *)   
-   let rec err node = relax_opt_qid (get_cnt err f st) st node in
-   get_cnt err f st st.node
-
-(****************************************************************************)
+let get_cnt_relaxed f lst =
+(* this is not tail recursive *)
+   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 lenv a w =
-   let bw = D.Abst (N.infinite, [w]) in
-   let f lenv = f lenv in
-   D.push_bind f lenv a bw
-
-let lenv_of_cnt (a, ws) = 
-   D.push_bind C.start D.empty_lenv a (D.Abst (N.infinite, ws))
+let push_abst f a w lenv =
+   let bw = D.Abst (false, N.infinity, w) in
+   D.push_bind f E.empty_node a 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, a, v)    -> set_name_y (D.push_appl f a 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, _, a, b) -> D.TBind (E.compose a 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 lenv = function
-   | A.Sort s            -> 
-      let f h = f (D.TSort ([], h)) in
-      if s then f 0 else f 1
+let rec xlate_term f st lst z lenv = function
+   | A.Sort s            ->
+      let k = if s then 0 else 1 in
+      f (k, 0) (D.TSort k)
    | A.Appl (v, t)       ->
-      let f vv tt = f (D.TAppl ([], [vv], tt)) in
-      let f vv = xlate_term (f vv) st lenv t in
-      xlate_term f st lenv v
+      let f yv vv yt tt =
+         f yt (D.TAppl (attrs_for_appl yv yt, vv, tt))
+      in
+      let f yv vv = xlate_term (f yv vv) st lst z lenv t in
+      xlate_term f st lst false lenv v
    | A.Abst (name, w, t) ->
-      let f ww = 
-         let a = [E.Name (name, true)] in
-	 let f tt =
-	    let b = D.Abst (N.infinite, [ww]) in
-	    f (D.TBind (a, b, tt))
+      let f yw ww =
+         let a = attrs_for_abst name yw in
+         let f yt tt =
+            let l =
+               if !G.cc then match z, snd yt with
+                  | true, _ -> N.one
+                  | _   , 0 -> N.one
+                  | _   , 1 -> N.unknown st
+                  | _   , 2 -> N.two
+                  | _       -> assert false
+               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 (E.compose a yt, b, tt))
 	 in
-         let f lenv = xlate_term f st lenv t in
-	 push_abst f lenv a ww
+         let f lenv = xlate_term f st lst z lenv t in
+	 push_abst f a ww lenv
       in
-      xlate_term f st lenv w
+      xlate_term f st lst true lenv w
    | A.GRef (name, args) ->
-      let map1 f = function
-	    | E.Name (id, _) -> f (A.GRef ((id, true, []), []))
-	    | _              -> C.err ()
+      let map1 args (id, _) = A.GRef ((id, true, []), []) :: args in
+      let map2 y f arg args =
+         let f yv v = f (D.EAppl (args, attrs_for_appl yv y, v)) in
+         xlate_term f st lst false lenv arg
       in
-      let map2 f t = xlate_term f st lenv t in
-      let g qid (a, _) =
-         let gref = D.TGRef ([], uri_of_qid qid) in
-	 match args, a with
-	    | [], [] -> f gref
-	    | _      ->
-	       let f args = f (D.TAppl ([], args, gref)) in
-	       let f args = C.list_rev_map f map2 args in
-	       let f a = C.list_rev_map_append f map1 a ~tail:args in
-	       C.list_sub_strict f a args
+      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 y (D.TAppl (a, v, gref))
+            | args                    -> f y (D.TProj (args, gref))
+         in
+	 let f args = C.list_fold_right f (map2 y) args D.ESort in
+	 D.sub_list_strict (D.fold_names f map1 args) cnt args
       in
-      let g qid = resolve_gref_relaxed g st qid in
-      let err () = complete_qid g st name in
+      let g qid = resolve_gref_relaxed g lst qid in
+      let err () = complete_qid g lst name in
       D.resolve_lref err (mk_lref f) (id_of_name name) lenv
 
-let xlate_entity err f st = function
+let xlate_entity err f st lst = function
    | A.Section (Some (_, name))     ->
-      err {st with path = name :: st.path; nodes = st.node :: st.nodes}
+      err {lst with path = name :: lst.path; nodes = lst.node :: lst.nodes}
    | A.Section None            ->
-      begin match st.path, st.nodes with
-	 | _ :: ptl, nhd :: ntl -> 
-	    err {st with path = ptl; node = nhd; nodes = ntl}
+      begin match lst.path, lst.nodes with
+	 | _ :: ptl, nhd :: ntl ->
+	    err {lst with path = ptl; node = nhd; nodes = ntl}
          | _                    -> assert false
       end
    | A.Context None            ->
-      err {st with node = None}
+      err {lst with node = None}
    | A.Context (Some name)     ->
-      let f name = err {st with node = Some name} in
-      complete_qid f st name 
+      let f name = err {lst with node = Some name} in
+      complete_qid f lst name
    | A.Block (name, w)         ->
-      let f qid = 
+      let f qid =
          let f cnt =
-	    let lenv = lenv_of_cnt cnt in
-	    let f ww = 
-	       K.add hcnt (uri_of_qid qid) (add_abst cnt name ww);
-	       err {st with node = Some qid}
+	    let f yw ww =
+	       UH.add hcnt (uri_of_qid qid) (add_abst cnt name yw ww);
+	       err {lst with node = Some qid}
 	    in
-	    xlate_term f st lenv w
+            xlate_term f st lst true cnt w
 	 in
-         get_cnt_relaxed f st
+         get_cnt_relaxed f lst
       in
-      complete_qid f st (name, true, [])
+      complete_qid f lst (name, true, [])
    | A.Decl (name, w)          ->
-      let f cnt =
-         let a, ws = cnt in
-         let lenv = lenv_of_cnt cnt in
-	 let f qid = 
-            let f ww =
-               K.add henv (uri_of_qid qid) cnt;
-	       let t = match ws with
-	          | [] -> ww
-	          | _  -> D.TBind (a, D.Abst (N.infinite, ws), ww)
-	       in
-(*
-	    print_newline (); CrgOutput.pp_term print_string t;
-*)
-	       let b = E.Abst (N.infinite, t) in
-	       let entity = [E.Mark st.line], uri_of_qid qid, b in
-	       f {st with line = succ st.line} entity
+      let f lenv =
+	 let f qid =
+            let f yw ww =
+               let yv = E.succ yw in
+               let a = attrs_for_env yv in
+               UH.add henv (uri_of_qid qid) (yv, 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 a 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 lenv w
+	    xlate_term f st lst true lenv w
 	 in
-         complete_qid f st (name, true, [])
+         complete_qid f lst (name, true, [])
       in
-      get_cnt_relaxed f st
+      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 cnt = 
-	 let a, ws = cnt in
-	 let lenv = lenv_of_cnt cnt in
-         let f qid = 
-            let f ww =
-	       let f vv =
-                  K.add henv (uri_of_qid qid) cnt;
-                  let t = match ws with
-	             | [] -> D.TCast ([], ww, vv)
-	             | _  -> D.TBind (a, D.Abst (N.infinite, ws), D.TCast ([], ww, vv))
-	          in
-(*
-	    print_newline (); CrgOutput.pp_term print_string t;
-*)
-	          let b = E.Abbr t in
-	          let a = E.Mark st.line :: if trans then [] else [E.Meta [E.Private]] in
-	          let entity = a, uri_of_qid qid, b in
-	          f {st with line = succ st.line} entity
+      let f lenv =
+         let f qid =
+            let f yw ww =
+	       let f yv vv =
+                  let a = attrs_for_env yv in
+                  UH.add henv (uri_of_qid qid) (yv, lenv);
+                  let t = if !G.cast then
+                     let f e = D.TCast (add_proj yw e ww, add_proj yv lenv vv) in
+                     if !G.infinity then f lenv else D.set_layer f N.one lenv
+                  else
+                     add_proj yv lenv (D.TCast (ww, 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 a 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 lenv v
+	       xlate_term f st lst false lenv v
 	    in
-            xlate_term f st lenv w
+            xlate_term f st lst true lenv w
 	 in
-         complete_qid f st (name, true, [])
+         complete_qid f lst (name, true, [])
       in
-      get_cnt_relaxed f st
+      get_cnt_relaxed f lst
 
 (* Interface functions ******************************************************)
 
 let initial_status () =
-   K.clear henv; K.clear hcnt; {
-   path = []; node = None; nodes = []; line = 1; mk_uri = G.get_mk_uri ()
+   UH.clear henv; UH.clear hcnt; {
+   path = []; node = None; nodes = []; line = 1; mk_uri = G.get_mk_uri ();
 }
 
-let refresh_status st = {st with
-   mk_uri = G.get_mk_uri ()
-}
+let refresh_status lst = initial_status ()
 
 let crg_of_aut = xlate_entity