X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fcontent_pres%2FtermContentPres.ml;h=4a65e6ec9595099b3ab2f8fc6e05a4e7648f2923;hb=56fb3c39cc9186ad2700b0ee8ca37f8d759c2376;hp=28bcbe314a2e3db6b279160c3c56a776b7c51908;hpb=8a660ee06d72cfee52c707bb1d8d8be3bab0d682;p=helm.git

diff --git a/matita/components/content_pres/termContentPres.ml b/matita/components/content_pres/termContentPres.ml
index 28bcbe314..4a65e6ec9 100644
--- a/matita/components/content_pres/termContentPres.ml
+++ b/matita/components/content_pres/termContentPres.ml
@@ -81,7 +81,7 @@ let ident_w_href href i =
   match href with
   | None -> ident i
   | Some href ->
-      let href = UriManager.string_of_uri href in
+      let href = NReference.string_of_reference href in
       add_xml_attrs [Some "xlink", "href", href] (ident i)
 
 let binder_symbol s =
@@ -109,7 +109,7 @@ let map_space f l =
   ~sep:[space] (List.map (fun x -> [f x]) l)
 ;;
 
-let pp_ast0 t k =
+let pp_ast0 status t k =
   let rec aux =
     function
     | Ast.Appl ts ->
@@ -143,7 +143,7 @@ let pp_ast0 t k =
         in
         let match_box =
           hvbox false false [
-           hvbox false true [
+           hvbox false false [
             hvbox false true [keyword "match"; space; break; top_pos (k what)];
             break;
             hvbox false true indty_box;
@@ -210,8 +210,8 @@ let pp_ast0 t k =
               keyword "let"; space;
               hvbox false true [
                 aux_var var; space;
-                builtin_symbol "\\def"; break; top_pos (k s) ];
-              break; space; keyword "in"; space ];
+                builtin_symbol "\\def"; break; top_pos (k s); space; keyword "in"; space ];
+              ];
             break;
             k t ])
     | Ast.LetRec (rec_kind, funs, where) ->
@@ -289,46 +289,51 @@ let pp_ast0 t k =
   and special_k = function
     | Ast.AttributedTerm (attrs, t) -> Ast.AttributedTerm (attrs, k t)
     | t ->
-        prerr_endline ("unexpected special: " ^ NotationPp.pp_term t);
+        prerr_endline ("unexpected special: " ^ NotationPp.pp_term status t);
         assert false
   in
   aux t
 
   (* persistent state *)
 
-let initial_level1_patterns21 () = Hashtbl.create 211
-let level1_patterns21 = ref (initial_level1_patterns21 ())
-let compiled21 = ref None
-let pattern21_matrix = ref []
-let counter = ref ~-1 
-
-let stack = ref [];;
-
-let push () =
-  stack := (!counter,!level1_patterns21,!compiled21,!pattern21_matrix)::!stack;
-  counter := ~-1;
-  level1_patterns21 := initial_level1_patterns21 ();
-  compiled21 := None;
-  pattern21_matrix := []
-;;
-
-let pop () =
- match !stack with
-    [] -> assert false
-  | (ocounter,olevel1_patterns21,ocompiled21,opatterns21_matrix)::old ->
-     stack := old;
-     counter := ocounter;
-     level1_patterns21 := olevel1_patterns21;
-     compiled21 := ocompiled21;
-     pattern21_matrix := opatterns21_matrix
-;;
-
-let get_compiled21 () =
-  match !compiled21 with
-  | None -> assert false
-  | Some f -> Lazy.force f
-
-let set_compiled21 f = compiled21 := Some f
+module IntMap = Map.Make(struct type t = int let compare = compare end);;
+
+type db = {
+ level1_patterns21: NotationPt.term IntMap.t;
+ compiled21: ((NotationPt.term -> (NotationEnv.t * NotationPt.term list * int) option)) Lazy.t;
+ pattern21_matrix: (NotationPt.term * pattern_id) list;
+ counter: pattern_id
+}
+
+let initial_db = {
+ level1_patterns21 = IntMap.empty;
+ compiled21 = lazy (Content2presMatcher.Matcher21.compiler []);
+ pattern21_matrix = [];
+ counter = ~-1 
+}
+
+class type g_status =
+  object
+    method content_pres_db: db
+  end
+ 
+class virtual status =
+ object
+   inherit NCic.status
+   val content_pres_db = initial_db  
+   method content_pres_db = content_pres_db
+   method set_content_pres_db v = {< content_pres_db = v >}
+   method set_content_pres_status
+    : 'status. #g_status as 'status -> 'self
+    = fun o -> {< content_pres_db = o#content_pres_db >}
+ end
+
+let get_compiled21 status =
+  Lazy.force status#content_pres_db.compiled21
+
+let set_compiled21 status f =
+ status#set_content_pres_db
+  { status#content_pres_db with compiled21 = f }
 
 let add_idrefs =
   List.fold_right (fun idref t -> Ast.AttributedTerm (`IdRef idref, t))
@@ -449,12 +454,12 @@ let instantiate21 idrefs env l1 =
   in
     subst_singleton `Left env l1
 
-let rec pp_ast1 term = 
+let rec pp_ast1 status term = 
   let rec pp_value = function
     | NotationEnv.NumValue _ as v -> v
     | NotationEnv.StringValue _ as v -> v
-(*     | NotationEnv.TermValue t when t == term -> NotationEnv.TermValue (pp_ast0 t pp_ast1) *)
-    | NotationEnv.TermValue t -> NotationEnv.TermValue (pp_ast1 t)
+(*     | NotationEnv.TermValue t when t == term -> NotationEnv.TermValue (pp_ast0 status t pp_ast1) *)
+    | NotationEnv.TermValue t -> NotationEnv.TermValue (pp_ast1 status t)
     | NotationEnv.OptValue None as v -> v
     | NotationEnv.OptValue (Some v) -> 
         NotationEnv.OptValue (Some (pp_value v))
@@ -467,32 +472,30 @@ let rec pp_ast1 term =
 (* prerr_endline ("pattern matching from 2 to 1 on term " ^ NotationPp.pp_term term); *)
   match term with
   | Ast.AttributedTerm (attrs, term') ->
-      Ast.AttributedTerm (attrs, pp_ast1 term')
+      Ast.AttributedTerm (attrs, pp_ast1 status term')
   | _ ->
-      (match (get_compiled21 ()) term with
-      | None -> pp_ast0 term pp_ast1
+      (match get_compiled21 status term with
+      | None -> pp_ast0 status term (pp_ast1 status)
       | Some (env, ctors, pid) ->
           let idrefs =
             List.flatten (List.map NotationUtil.get_idrefs ctors)
           in
           let l1 =
             try
-              Hashtbl.find !level1_patterns21 pid
+              IntMap.find pid status#content_pres_db.level1_patterns21
             with Not_found -> assert false
           in
           instantiate21 idrefs (ast_env_of_env env) l1)
 
-let load_patterns21 t =
-  set_compiled21 (lazy (Content2presMatcher.Matcher21.compiler t))
+let load_patterns21 status t =
+  set_compiled21 status (lazy (Content2presMatcher.Matcher21.compiler t))
 
-let pp_ast ast =
+let pp_ast status ast =
   debug_print (lazy "pp_ast <-");
-  let ast' = pp_ast1 ast in
-  debug_print (lazy ("pp_ast -> " ^ NotationPp.pp_term ast'));
+  let ast' = pp_ast1 status ast in
+  debug_print (lazy ("pp_ast -> " ^ NotationPp.pp_term status ast'));
   ast'
 
-exception Pretty_printer_not_found
-
 let fill_pos_info l1_pattern = l1_pattern
 (*   let rec aux toplevel pos =
     function
@@ -506,26 +509,21 @@ let fill_pos_info l1_pattern = l1_pattern
   in
   aux true l1_pattern *)
 
-let fresh_id =
-  fun () ->
-    incr counter;
-    !counter
+let fresh_id status =
+  let counter = status#content_pres_db.counter+1 in
+   status#set_content_pres_db ({ status#content_pres_db with counter = counter  }), counter
 
-let add_pretty_printer l2 (CicNotationParser.CL1P (l1,precedence)) =
-  let id = fresh_id () in
+let add_pretty_printer status l2 (CicNotationParser.CL1P (l1,precedence)) =
+  let status,id = fresh_id status in
   let l1' = add_level_info precedence (fill_pos_info l1) in
   let l2' = NotationUtil.strip_attributes l2 in
-  Hashtbl.add !level1_patterns21 id l1';
-  pattern21_matrix := (l2', id) :: !pattern21_matrix;
-  load_patterns21 !pattern21_matrix;
-  id
-
-let remove_pretty_printer id =
-  (try
-    Hashtbl.remove !level1_patterns21 id;
-  with Not_found -> raise Pretty_printer_not_found);
-  pattern21_matrix := List.filter (fun (_, id') -> id <> id') !pattern21_matrix;
-  load_patterns21 !pattern21_matrix
+  let status =
+   status#set_content_pres_db
+    { status#content_pres_db with
+       level1_patterns21 =
+        IntMap.add id l1' status#content_pres_db.level1_patterns21;
+       pattern21_matrix = (l2',id)::status#content_pres_db.pattern21_matrix } in
+  load_patterns21 status status#content_pres_db.pattern21_matrix 
 
   (* presentation -> content *)
 
@@ -574,7 +572,7 @@ let tail_names names env =
   in
   aux [] env
 
-let instantiate_level2 env term =
+let instantiate_level2 status env term =
 (*   prerr_endline ("istanzio: " ^ NotationPp.pp_term term); *)
   let fresh_env = ref [] in
   let lookup_fresh_name n =
@@ -586,7 +584,6 @@ let instantiate_level2 env term =
       new_name
   in
   let rec aux env term =
-(*    prerr_endline ("ENV " ^ NotationPp.pp_env env); *)
     match term with
     | Ast.AttributedTerm (a, term) -> (*Ast.AttributedTerm (a, *)aux env term
     | Ast.Appl terms -> Ast.Appl (List.map (aux env) terms)
@@ -638,7 +635,10 @@ let instantiate_level2 env term =
   and aux_meta_substs env meta_substs = List.map (aux_opt env) meta_substs
   and aux_variable env = function
     | Ast.NumVar name -> Ast.Num (Env.lookup_num env name, 0)
-    | Ast.IdentVar name -> Ast.Ident (Env.lookup_string env name, None)
+    | Ast.IdentVar name ->
+       (match Env.lookup_string env name with
+           Env.Ident x -> Ast.Ident (x, None)
+         | Env.Var x -> Ast.Variable (Ast.IdentVar x))
     | Ast.TermVar (name,(Ast.Level l|Ast.Self l)) -> 
         Ast.AttributedTerm (`Level l,Env.lookup_term env name)
     | Ast.FreshVar name -> Ast.Ident (lookup_fresh_name name, None)
@@ -665,7 +665,7 @@ let instantiate_level2 env term =
             | _ ->
                 prerr_endline (sprintf
                   "lookup of %s in env %s did not return an optional value"
-                  name (NotationPp.pp_env env));
+                  name (NotationPp.pp_env status env));
                 assert false))
     | Ast.Fold (`Left, base_pattern, names, rec_pattern) ->
         let acc_name = List.hd names in (* names can't be empty, cfr. parser *)
@@ -716,10 +716,3 @@ let instantiate_level2 env term =
     | _ -> assert false
   in
   aux env term
-
-  (* initialization *)
-
-let _ = load_patterns21 []
-
-
-