- the text model now supports invocations of the entity generator (to

[helm.git] / helm / software / lambda-delta / complete_rg / crgTxt.ml

diff --git a/helm/software/lambda-delta/complete_rg/crgTxt.ml b/helm/software/lambda-delta/complete_rg/crgTxt.ml
index 1cb2b3ee90cde40bddfd7319928a2c9b895908d9..e0f5feb1a17182964cecab652fd12c5b3286626d 100644 (file)
--- a/helm/software/lambda-delta/complete_rg/crgTxt.ml
+++ b/helm/software/lambda-delta/complete_rg/crgTxt.ml
@@ -9,18 +9,20 @@
      \ /   This software is distributed as is, NO WARRANTY.              
       V_______________________________________________________________ *)
 
-module U = NUri
-module H = Hierarchy
-module C = Cps
-module Y = Entity
-module T = Txt
-module D = Crg
+module U  = NUri
+module H  = Hierarchy
+module C  = Cps
+module O  = Options
+module Y  = Entity
+module T  = Txt
+module TT = TxtTxt
+module D  = Crg
 
 type status = {
-   path: T.id list;          (* current section path *)
-   line: int;                (* line number *)
-   sort: int;                (* first default sort index *)
-   mk_uri:Y.uri_generator    (* uri generator *) 
+   path  : T.id list;      (* current section path *)
+   line  : int;            (* line number *)
+   sort  : int;            (* first default sort index *)
+   mk_uri: O.uri_generator (* uri generator *) 
 }
 
 let henv_size = 7000 (* hash tables initial size *)
@@ -29,11 +31,7 @@ let henv = Hashtbl.create henv_size (* optimized global environment *)
 
 (* Internal functions *******************************************************)
 
-let initial_status mk_uri = {
-   path = []; line = 1; sort = 0; mk_uri = mk_uri
-}
-
-let name_of_id id = Y.Name (id, true)
+let name_of_id ?(r=true) id = Y.Name (id, r)
 
 let mk_lref f i j k = f (D.TLRef ([Y.Apix k], i, j))
 
@@ -50,52 +48,62 @@ let resolve_gref err f st id =
    with Not_found -> err ()
 
 let rec xlate_term f st lenv = function
-   | T.Sort h            -> 
+   | T.Inst _
+   | T.Impl _       -> assert false
+   | T.Sort h       -> 
       f (D.TSort ([], h))
-   | T.NSrt id           -> 
+   | T.NSrt id      -> 
       let f h = f (D.TSort ([], h)) in
       H.sort_of_string C.err f id
-   | T.LRef (i, j)       ->    
+   | T.LRef (i, j)  ->    
       D.get_index C.err (mk_lref f i j) i j lenv
-   | T.NRef id           ->
+   | T.NRef id      ->
       let err () = resolve_gref C.err (mk_gref f) st id in
       D.resolve_lref err (mk_lref f) id lenv
-   | T.Cast (u, t)       ->
+   | T.Cast (u, t)  ->
       let f uu tt = f (D.TCast ([], uu, tt)) in
       let f uu = xlate_term (f uu) st lenv t in
       xlate_term f st lenv u
-   | T.Appl (vs, t)      ->
+   | T.Appl (vs, t) ->
       let map f = xlate_term f st lenv in
       let f vvs tt = f (D.TAppl ([], vvs, tt)) in
       let f vvs = xlate_term (f vvs) st lenv t in
       C.list_map f map vs
-   | T.Bind (b, t)       ->
-      let map1 (lenv, a, wws) (id, w) = 
+   | T.Bind (b, t)  ->
+      let abst_map (lenv, a, wws) (id, r, w) = 
+         let attr = name_of_id ~r id in
+        let ww = xlate_term C.start st lenv w in
+        D.push2 C.err C.start lenv attr ~t:ww (), attr :: a, ww :: wws
+      in
+      let abbr_map (lenv, a, wws) (id, w) = 
          let attr = name_of_id id in
         let ww = xlate_term C.start st lenv w in
         D.push2 C.err C.start lenv attr ~t:ww (), attr :: a, ww :: wws
       in
-      let map2 (lenv, a, n) id = 
+      let void_map (lenv, a, n) id = 
         let attr = name_of_id id in
         D.push2 C.err C.start lenv attr (), attr :: a, succ n
       in
       let lenv, aa, bb = match b with
          | T.Abst xws ->
            let lenv = D.push_bind C.start lenv [] (D.Abst []) in
-           let lenv, aa, wws = List.fold_left map1 (lenv, [], []) xws in
+           let lenv, aa, wws = List.fold_left abst_map (lenv, [], []) xws in
            lenv, aa, D.Abst wws
          | T.Abbr xvs ->
            let lenv = D.push_bind C.start lenv [] (D.Abbr []) in
-           let lenv, aa, vvs = List.fold_left map1 (lenv, [], []) xvs in
+           let lenv, aa, vvs = List.fold_left abbr_map (lenv, [], []) xvs in
            lenv, aa, D.Abbr vvs
          | T.Void ids ->
            let lenv = D.push_bind C.start lenv [] (D.Void 0) in
-           let lenv, aa, n = List.fold_left map2 (lenv, [], 0) ids in
+           let lenv, aa, n = List.fold_left void_map (lenv, [], 0) ids in
            lenv, aa, D.Void n
       in
       let f tt = f (D.TBind (aa, bb, tt)) in
       xlate_term f st lenv t
 
+let xlate_term f st lenv t =
+   TT.contract (xlate_term f st lenv) t
+
 let mk_contents tt = function
    | T.Decl -> [], Y.Abst tt
    | T.Ax   -> [], Y.Abst tt
@@ -103,6 +111,8 @@ let mk_contents tt = function
    | T.Th   -> [], Y.Abbr tt
 
 let xlate_entity err f st = function
+   | T.Require _                  ->
+      err st
    | T.Section (Some name)        ->
       err {st with path = name :: st.path}
    | T.Section None               ->
@@ -133,10 +143,18 @@ let xlate_entity err f st = function
       let a = if meta <> "" then Y.Meta meta :: a else a in
       let entity = Y.Mark st.line :: a, uri, b in
       f {st with line = succ st.line} entity
+   | T.Generate _                 ->
+      err st
 
 (* Interface functions ******************************************************)
 
-let initial_status mk_uri =
-   initial_status mk_uri
+let initial_status () =
+   Hashtbl.clear henv; {
+   path = []; line = 1; sort = 0; mk_uri = O.get_mk_uri ()
+}
+
+let refresh_status st = {st with
+   mk_uri = O.get_mk_uri ()
+}
 
 let crg_of_txt = xlate_entity