X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fhelena%2Fsrc%2Ftext%2FtxtCrg.ml;h=4580d2d867eb7b29ec5dbf4de2e5b3da5129deae;hb=88977b2d546e547e23b046792fe2ad8f6ff192a4;hp=21af0f5116b804aa2e4cc92e18dcca3ae5ba8eaf;hpb=34e6104ef149e3776d0ab7f0930ae73f0e8de157;p=helm.git

diff --git a/helm/software/helena/src/text/txtCrg.ml b/helm/software/helena/src/text/txtCrg.ml
index 21af0f511..4580d2d86 100644
--- a/helm/software/helena/src/text/txtCrg.ml
+++ b/helm/software/helena/src/text/txtCrg.ml
@@ -9,120 +9,137 @@
      \ /   This software is distributed as is, NO WARRANTY.              
       V_______________________________________________________________ *)
 
+module KF = Filename
+module KH = Hashtbl
+module KL = List
+
 module U  = NUri
 module C  = Cps
 module G  = Options
 module H  = Hierarchy
 module E  = 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 *)
+   rest  : bool;           (* restricted applications *) 
    mk_uri: G.uri_generator (* uri generator *) 
 }
 
 let henv_size = 7000 (* hash tables initial size *)
 
-let henv = Hashtbl.create henv_size (* optimized global environment *)
+let henv = KH.create henv_size (* optimized global environment *)
+
+let xerr s () = 
+   Printf.printf "%s\n%!" s; C.err ()
 
 (* Internal functions *******************************************************)
-(*
-let name_of_id ?(r=true) id = E.Name (id, r)
 
-let mk_lref f i j k = f (D.TLRef ([E.Apix k], i, j))
+let mk_lref f a y i = f y (D.TLRef (a, i))
 
-let mk_gref f uri = f (D.TGRef ([], uri))
+let mk_gref f y uri = f y (D.TGRef (E.empty_node, uri))
+
+let get err f e i = match D.get e i with
+   | _, _, _, D.Void -> err ()
+   | _, a, y, _      -> mk_lref f a y i
+
+let resolve_gref err f st id =
+   try 
+      let y, uri = KH.find henv id in f y uri
+   with Not_found -> err ()
+
+let name_of_id ?(r=true) id =
+   if id = "" then None else Some (id, r)
 
 let uri_of_id st id path =
    let str = String.concat "/" path in
-   let str = Filename.concat str id in 
+   let str = KF.concat str id in 
    let str = st.mk_uri str in
    U.uri_of_string str
 
-let resolve_gref err f st id =
-   try f (Hashtbl.find henv id)
-   with Not_found -> err ()
-
 let rec xlate_term f st lenv = function
-   | T.Inst _
-   | T.Impl _         -> assert false
-   | T.Sort h         -> 
-      f (D.TSort ([], h))
-   | T.NSrt id        -> 
-      let f h = f (D.TSort ([], h)) in
-      H.sort_of_string C.err f id
-   | T.LRef (i, j)    ->    
-      D.get_index C.err (mk_lref f i j) i j lenv
+(*
+   CrgOutput.pp_lenv print_string (Layer.initial_status ()) lenv;
+   Printf.printf "\n";
+*)
+   | T.Sort k         ->
+      let y = E.bind_attrs ~main:(k, 0) () in 
+      f y (D.TSort k)
+   | T.NSrt id        ->
+      let f h = xlate_term f st lenv (T.Sort h) in
+      H.sort_of_string (xerr "sort not found") f id
+   | T.LRef i         ->
+      get (xerr "index out of bounds") f lenv i
    | T.NRef id        ->
-      let err () = resolve_gref C.err (mk_gref f) st id in
+      let err () = resolve_gref (xerr "global constant not found") (mk_gref f) st id in
       D.resolve_lref err (mk_lref f) id lenv
    | 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
+      let f uu y tt = f y (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)   ->
-      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 (n, 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
+   | T.Appl (v, t)    ->
+      let f vv y tt = f y (D.TAppl (E.appl_attrs st.rest, vv, tt)) in
+      let f _ vv = xlate_term (f vv) st lenv t in
+      xlate_term f st lenv v
+   | T.Proj (bs, t)   ->
+      let f e y tt = f y (D.TProj (e, tt)) in
+      let f (lenv, e) = xlate_term (f e) st lenv t in
+      C.list_fold_left f (xlate_bind st) (lenv, D.empty_lenv) bs
+   | T.Inst (t, vs)   ->
+      let map f v e =
+         let f _ vv = D.push_appl f (E.appl_attrs st.rest) vv e in
+         xlate_term f st lenv v
       in
-      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 (n, [])) in
-	    let lenv, aa, wws = List.fold_left abst_map (lenv, [], []) xws in
-	    lenv, aa, D.Abst (n, wws)
-         | T.Abbr xvs ->
-	    let lenv = D.push_bind C.start lenv [] (D.Abbr []) 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 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 n tt = function
-   | T.Decl -> []                    , E.Abst (n, tt)
-   | T.Ax   -> [E.InProp]            , E.Abst (n, tt)
-   | T.Cong -> [E.InProp; E.Progress], E.Abst (n, tt)   
-   | T.Def  -> []                    , E.Abbr tt
-   | T.Th   -> [E.InProp]            , E.Abbr tt
+      let f e y tt = f y (D.TProj (e, tt)) in
+      let f e = xlate_term (f e) st lenv t in
+      C.list_fold_right f map vs D.empty_lenv
+
+and xlate_bind st f (lenv, e) b =
+   let f lenv e = f (lenv, e) in
+   let f y b lenv = D.push_bind (f lenv) E.empty_node y b e in
+   let f y b = D.push_bind (f y b) E.empty_node y b lenv in
+   match b with
+      | T.Abst (n, id, r, w) ->
+         let f y ww =
+            let y = E.bind_attrs ?name:(name_of_id id) () in
+            f y (D.Abst (false, n, ww))
+         in
+         xlate_term f st lenv w
+      | T.Abbr (id, v)       ->
+         let f y vv =
+            let y = E.bind_attrs ?name:(name_of_id id) () in
+            f y (D.Abbr vv)
+         in
+         xlate_term f st lenv v
+      | T.Void id           ->
+         let y = E.bind_attrs ?name:(name_of_id id) ~main:(st.sort, 0) () in
+         f y D.Void
+
+let mk_contents main kind tt =
+   let ms, b = match kind with
+      | T.Decl -> []                    , E.abst E.empty_env tt
+      | T.Ax   -> [E.InProp]            , E.abst E.empty_env tt
+      | T.Cong -> [E.InProp; E.Progress], E.abst E.empty_env tt   
+      | T.Def  -> []                    , E.abbr E.empty_env tt
+      | T.Th   -> [E.InProp]            , E.abbr E.empty_env tt
+   in
+   if main then E.Main :: ms, b else ms, b
 
 let xlate_entity err f gen st = function
-   | T.Require _                           ->
+   | T.Require _                          ->
       err st
-   | T.Section (Some name)                 ->
+   | T.Section (Some name)                ->
       err {st with path = name :: st.path}
-   | T.Section None                        ->
+   | T.Section None                       ->
       begin match st.path with
 	 | _ :: ptl -> 
 	    err {st with path = ptl}
          | _        -> assert false
       end
-   | T.Sorts sorts                         ->
+   | T.Sorts sorts                        ->
       let map st (xix, s) =
          let ix = match xix with 
 	    | None    -> st.sort
@@ -130,35 +147,35 @@ let xlate_entity err f gen st = function
 	 in
          {st with sort = H.set_sorts ix [s]}
       in
-      err (List.fold_left map st sorts)
-   | T.Graph id                            ->
+      err (KL.fold_left map st sorts)
+   | T.Graph id                           ->
       assert (H.set_graph id); err st
-   | T.Entity (main, kind, n, id, info, t) ->
+   | T.Constant (main, kind, id, info, t) ->
       let uri = uri_of_id st id st.path in
-      Hashtbl.add henv id uri;
-      let tt = xlate_term C.start st D.empty_lenv t in
+      let g ya tt =
+         KH.add henv id (ya, uri);
 (*
-      print_newline (); CrgOutput.pp_term print_string tt;
-*)
-      let a = [] in
-      let ms, b = mk_contents n tt kind in 
-      let ms = if main then E.Main :: ms else ms in 
-      let a = if ms <> [] then E.Meta ms :: a else a in
-      let a = if info <> ("", "") then E.Info info :: a else a in
-      let entity = E.Mark st.line :: a, uri, b in
-      f {st with line = succ st.line} entity
-   | T.Generate _                          ->
+         print_newline (); CrgOutput.pp_term print_string tt;
+*)   
+         let meta, b = mk_contents main kind tt in 
+         let na = E.node_attrs ~apix:st.line () in
+         let ra = E.root_attrs ~meta ~info () in
+         let entity = ra, na, uri, b in
+         f {st with line = succ st.line} entity
+      in
+      xlate_term g st D.empty_lenv t
+   | T.Generate _                         ->
       err st
 
 (* Interface functions ******************************************************)
-*)
+
 let initial_status () =
-   Hashtbl.clear henv; {
-   path = []; line = 1; sort = 0; mk_uri = G.get_mk_uri ()
+   KH.clear henv; {
+   path = []; line = 1; sort = 0; rest = true; mk_uri = G.get_mk_uri ()
 }
 
 let refresh_status st = {st with
    mk_uri = G.get_mk_uri ()
 }
 
-let crg_of_txt _ _ = assert false (* xlate_entity *)
+let crg_of_txt = xlate_entity