X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Ftoplevel%2FmetaAut.ml;h=5b85e46cbea703dd21fafe6f53b7242c6b5025b5;hb=299f571083fa9cc38060c0d6b2ec81eefeaa1050;hp=ac481a21d0f2b0ab95979b74aca7d73da411eadd;hpb=98d596e4a26c596ef17b3c7ed48c86f1cf4d4061;p=helm.git

diff --git a/helm/software/lambda-delta/toplevel/metaAut.ml b/helm/software/lambda-delta/toplevel/metaAut.ml
index ac481a21d..5b85e46cb 100644
--- a/helm/software/lambda-delta/toplevel/metaAut.ml
+++ b/helm/software/lambda-delta/toplevel/metaAut.ml
@@ -24,53 +24,97 @@
  *)
 
 module H = Hashtbl
+
 module M = Meta
 module A = Aut
 
-type context_node = M.qid option (* context node: None = root *)
+type environment = (M.qid, M.pars) H.t
 
-type context = (M.qid, M.term * context_node) H.t (* context: son, parent *)
+type context_node = M.qid option (* context node: None = root *)
 
 type status = {
-   genv: M.environment; (* global environment *)
-   path: M.id list;     (* current section path *) 
-   cnt: context;        (* context *)
-   node: context_node;  (* current context node *)
-   explicit: bool       (* need explicit context root? *)
+   genv: M.environment;      (* global environment *)
+   henv: environment;        (* optimized global environment *)
+   path: M.id list;          (* current section path *) 
+   hcnt: environment;        (* optimized context *)   
+   node: context_node;       (* current context node *)
+   nodes: context_node list; (* context node list *)
+   line: int;                (* line number *)
+   explicit: bool            (* need explicit context root? *)
 }
 
 type resolver = Local of int
               | Global of M.pars
-	      | Unresolved
 
-let initial_status = {
-   genv = []; path = []; cnt = H.create 11; node = None; explicit = true
+let hsize = 11 (* hash tables initial size *)
+
+let initial_status size = {
+   genv = []; path = []; node = None; nodes = []; line = 1; explicit = true;
+   henv = H.create size; hcnt = H.create size
 }
 
 let complete_qid f st (id, is_local, qs) =
    let f qs = f (id, qs) in
-   if is_local then Cps.list_rev_append f st.path ~tail:qs else f qs
+   let f path = Cps.list_rev_append f 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)
 
-let resolve_gref f st lenv gref =
+let relax_qid f (id, path) =
+   let f path = f (id, path) in
+   let f = function
+      | _ :: tl -> Cps.list_rev f tl
+      | []      -> assert false
+   in
+   Cps.list_rev f path
+
+let relax_opt_qid f = function
+   | None     -> f None
+   | Some qid -> let f qid = f (Some qid) in relax_qid f qid
+
+let resolve_gref f st local lenv gref =
   let rec get_local f i = function
-     | []                              -> f None
-     | (name, _) :: _ when name = gref -> f (Some i)
-     | _ :: tl                         -> get_local f (succ i) tl
+     | []                                      -> f None
+     | (name, _) :: _ when fst name = fst gref -> f (Some i)
+     | _ :: tl                                 -> get_local f (succ i) tl
   in
-  let rec get_global f = function
-     | []                                       -> f None
-     | (args, name, _, _) :: _ when name = gref -> f (Some args)
-     | _ :: tl                                  -> get_global f tl
+  let get_global f =
+     try 
+        let args = H.find st.henv gref in f (Some args)
+     with Not_found -> f None
   in
   let g = function
-      | Some args -> f (Global args)
-      | None      -> f Unresolved
+      | Some args -> f gref (Some (Global args))
+      | None      -> f gref None
   in
   let f = function
-      | Some i -> f (Local i)
-      | None   -> get_global g st.genv
+      | Some i -> f gref (Some (Local i))
+      | None   -> get_global g
   in
-  get_local f 0 lenv
+  if local then get_local f 0 lenv else f None
+
+let resolve_gref_relaxed f st lenv gref =
+   let rec g gref = function
+      | None          -> relax_qid (resolve_gref g st false lenv) gref
+      | Some resolved -> f gref resolved
+   in
+   resolve_gref g st true lenv gref
+
+let get_pars f st = function
+   | None              -> f [] None
+   | Some name as node ->
+      try let pars = H.find st.hcnt name in f pars None
+      with Not_found -> f [] (Some node)
+
+let get_pars_relaxed f st =
+   let rec g pars = function
+      | None      -> f pars 
+      | Some node -> relax_opt_qid (get_pars g st) node
+   in
+   get_pars g st st.node
 
 let rec xlate_term f st lenv = function
    | A.Sort sort         -> f (M.Sort sort)
@@ -90,26 +134,27 @@ let rec xlate_term f st lenv = function
       let f name = function
 	 | Local i     -> f (M.LRef i)
          | Global defs -> 
-            let map1 f = xlate_term f st lenv in
-	    let map2 f (name, _) = f (M.GRef (name, [])) in
+            let l = List.length lenv in
+	    let map1 f = xlate_term f st lenv in
+	    let map2 f (name, _) = f (M.GRef (l, name, [])) in
             let f tail =  	   
-	       let f args = f (M.GRef (name, args)) in
+	       let f args = f (M.GRef (l, name, args)) in
                let f defs = Cps.list_rev_map_append f map2 defs ~tail in
 	       Cps.list_sub_strict f defs args
 	    in
 	    Cps.list_map f map1 args
-	 | Unresolved  -> assert false
       in
-      let f name = resolve_gref (f name) st lenv name in
+      let f name = resolve_gref_relaxed f st lenv name in
       complete_qid f st name
 
 let xlate_item f st = function
    | A.Section (Some name)     ->
-      f {st with path = name :: st.path}
+      f {st with path = name :: st.path; nodes = st.node :: st.nodes}
    | A.Section None            ->
-      begin match st.path with
-         | []      -> assert false
-	 | _ :: tl -> f {st with path = tl}
+      begin match st.path, st.nodes with
+	 | _ :: ptl, nhd :: ntl -> 
+	    f {st with path = ptl; node = nhd; nodes = ntl}
+         | _                    -> assert false
       end
    | A.Context None            ->
       f {st with node = None}
@@ -117,12 +162,45 @@ let xlate_item f st = function
       let f name = f {st with node = Some name} in
       complete_qid f st name
    | A.Block (name, w)         ->
-      let f name ww = H.add st.cnt name (ww, st.node); f st in
-      let f name = xlate_term (f name) st [] w in
-      complete_qid f st (name, true, [])   
-   | A.Decl (name, w)          -> f st 
-   | A.Def (name, w, trans, v) -> f st
+      let f name = 
+         let f pars =
+	    let f ww = 
+	       H.add st.hcnt name ((name, ww) :: pars);
+	       f {st with node = Some name}
+	    in
+            xlate_term f st pars w
+	 in
+         get_pars_relaxed f st
+      in
+      complete_qid f st (name, true, [])
+   | A.Decl (name, w)          ->
+      let f pars = 
+         let f name = 
+            let f ww =
+	       let entry = (st.line, pars, name, ww, None) in
+	       H.add st.henv name pars;
+	       f {st with genv = entry :: st.genv; line = succ st.line}
+	    in
+	    xlate_term f st pars w
+	 in
+         complete_qid f st (name, true, [])
+      in
+      get_pars_relaxed f st
+   | A.Def (name, w, trans, v) ->
+      let f pars = 
+         let f name = 
+            let f ww vv = 
+	       let entry = (st.line, pars, name, ww, Some (trans, vv)) in
+	       H.add st.henv name pars;
+	       f {st with genv = entry :: st.genv; line = succ st.line}
+	    in
+	    let f ww = xlate_term (f ww) st pars v in
+	    xlate_term f st pars w
+	 in
+         complete_qid f st (name, true, [])
+      in
+      get_pars_relaxed f st
 
 let meta_of_aut f book =
    let f st = f st.genv in
-   Cps.list_fold_left f xlate_item initial_status book
+   Cps.list_fold_left f xlate_item (initial_status hsize) book