X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fcomponents%2Fcontent%2Finterpretations.ml;h=aaa87d0838fa946746e8a5db2b7c7cebfbda2866;hb=f3f6b451707a3feb8245717e3fa7ca25df0ce8ef;hp=c7bfa576804b19621429f46f9556a4158b1db350;hpb=8a660ee06d72cfee52c707bb1d8d8be3bab0d682;p=helm.git

diff --git a/matita/components/content/interpretations.ml b/matita/components/content/interpretations.ml
index c7bfa5768..aaa87d083 100644
--- a/matita/components/content/interpretations.ml
+++ b/matita/components/content/interpretations.ml
@@ -28,52 +28,58 @@
 open Printf
 
 module Ast = NotationPt
-module Obj = LibraryObjects
 
 let debug = false
 let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
 
-type interpretation_id = int
+let load_patterns32 = ref (fun _ -> assert false);;
+let set_load_patterns32 f = load_patterns32 := f;;
 
 let idref id t = Ast.AttributedTerm (`IdRef id, t)
 
+type cic_id = string
+
 type term_info =
-  { sort: (Cic.id, Ast.sort_kind) Hashtbl.t;
-    uri: (Cic.id, UriManager.uri) Hashtbl.t;
+  { sort: (cic_id, Ast.sort_kind) Hashtbl.t;
+    uri: (cic_id, NReference.reference) Hashtbl.t;
   }
 
-  (* persistent state *)
-
-let initial_level2_patterns32 () = Hashtbl.create 211
-let initial_interpretations () = Hashtbl.create 211
-
-let level2_patterns32 = ref (initial_level2_patterns32 ())
-(* symb -> id list ref *)
-let interpretations = ref (initial_interpretations ())
-let pattern32_matrix = ref []
-let counter = ref ~-1 
-let find_level2_patterns32 pid = Hashtbl.find !level2_patterns32 pid;;
-
-let stack = ref []
-
-let push () =
- stack := (!counter,!level2_patterns32,!interpretations,!pattern32_matrix)::!stack;
- counter := ~-1;
- level2_patterns32 := initial_level2_patterns32 ();
- interpretations := initial_interpretations ();
- pattern32_matrix := []
-;;
-
-let pop () =
- match !stack with
-    [] -> assert false
-  | (ocounter,olevel2_patterns32,ointerpretations,opattern32_matrix)::old ->
-   stack := old;
-   counter := ocounter;
-   level2_patterns32 := olevel2_patterns32;
-   interpretations := ointerpretations;
-   pattern32_matrix := opattern32_matrix
-;;
+module IntMap = Map.Make(struct type t = int let compare = compare end);;
+module StringMap = Map.Make(String);;
+
+type db = {
+  counter: int;
+  pattern32_matrix: (bool * NotationPt.cic_appl_pattern * int) list;
+  level2_patterns32:
+   (string * string * NotationPt.argument_pattern list *
+     NotationPt.cic_appl_pattern) IntMap.t;
+  interpretations: int list StringMap.t; (* symb -> id list *)
+}
+
+let initial_db = {
+   counter = -1; 
+   pattern32_matrix = [];
+   level2_patterns32 = IntMap.empty;
+   interpretations = StringMap.empty
+}
+
+class type g_status =
+  object
+    method interp_db: db
+  end
+ 
+class status =
+ object
+   val interp_db = initial_db  
+   method interp_db = interp_db
+   method set_interp_db v = {< interp_db = v >}
+   method set_interp_status
+    : 'status. #g_status as 'status -> 'self
+    = fun o -> {< interp_db = o#interp_db >}
+ end
+
+let find_level2_patterns32 status pid =
+ IntMap.find pid status#interp_db.level2_patterns32
 
 let add_idrefs =
   List.fold_right (fun idref t -> Ast.AttributedTerm (`IdRef idref, t))
@@ -108,86 +114,53 @@ let instantiate32 term_info idrefs env symbol args =
   if args = [] then head
   else Ast.Appl (head :: List.map instantiate_arg args)
 
-let load_patterns32s = ref [];;
-
-let add_load_patterns32 f = load_patterns32s := f :: !load_patterns32s;;
-let fresh_id =
-  fun () ->
-    incr counter;
-    !counter
-
-let add_interpretation dsc (symbol, args) appl_pattern =
-  let id = fresh_id () in
-  Hashtbl.add !level2_patterns32 id (dsc, symbol, args, appl_pattern);
-  pattern32_matrix := (true, appl_pattern, id) :: !pattern32_matrix;
-  List.iter (fun f -> f !pattern32_matrix) !load_patterns32s;
-  (try
-    let ids = Hashtbl.find !interpretations symbol in
-    ids := id :: !ids
-  with Not_found -> Hashtbl.add !interpretations symbol (ref [id]));
-  id
-
-let get_all_interpretations () =
-  List.map
-    (function (_, _, id) ->
-      let (dsc, _, _, _) =
-        try
-          Hashtbl.find !level2_patterns32 id
-        with Not_found -> assert false
-      in
-      (id, dsc))
-    !pattern32_matrix
-
-let get_active_interpretations () =
-  HExtlib.filter_map (function (true, _, id) -> Some id | _ -> None)
-    !pattern32_matrix
-
-let set_active_interpretations ids =
-  let pattern32_matrix' =
-    List.map
-      (function 
-        | (_, ap, id) when List.mem id ids -> (true, ap, id)
-        | (_, ap, id) -> (false, ap, id))
-      !pattern32_matrix
+let fresh_id status =
+  let counter = status#interp_db.counter+1 in
+   status#set_interp_db ({ status#interp_db with counter = counter  }), counter
+
+let add_interpretation (status : #status) dsc (symbol, args) appl_pattern =
+  let status,id = fresh_id status in
+  let ids =
+   try
+    StringMap.find symbol status#interp_db.interpretations
+   with Not_found -> [id] in
+  let status =
+   status#set_interp_db { status#interp_db with
+    level2_patterns32 =
+      IntMap.add id (dsc, symbol, args, appl_pattern)
+       status#interp_db.level2_patterns32;
+    pattern32_matrix = (true,appl_pattern,id)::status#interp_db.pattern32_matrix;
+    interpretations = StringMap.add symbol ids status#interp_db.interpretations
+   }
   in
-  pattern32_matrix := pattern32_matrix';
-  List.iter (fun f -> f !pattern32_matrix) !load_patterns32s
+   !load_patterns32 status#interp_db.pattern32_matrix;
+   status
+
+let toggle_active_interpretations status b =
+  status#set_interp_db { status#interp_db with
+   pattern32_matrix =
+     List.map (fun (_,ap,id) -> b,ap,id) status#interp_db.pattern32_matrix }
 
 exception Interpretation_not_found
 
-let lookup_interpretations ?(sorted=true) symbol =
+let lookup_interpretations status ?(sorted=true) symbol =
   try
     let raw = 
       List.map (
         fun id ->
           let (dsc, _, args, appl_pattern) =
-            try
-              Hashtbl.find !level2_patterns32 id
+            try IntMap.find id status#interp_db.level2_patterns32
             with Not_found -> assert false 
           in
           dsc, args, appl_pattern
-      )
-      !(Hashtbl.find !interpretations symbol)
+      ) (StringMap.find symbol status#interp_db.interpretations)
     in
     if sorted then HExtlib.list_uniq (List.sort Pervasives.compare raw)
               else raw
   with Not_found -> raise Interpretation_not_found
 
-let remove_interpretation id =
-  (try
-    let dsc, symbol, _, _ = Hashtbl.find !level2_patterns32 id in
-    let ids = Hashtbl.find !interpretations symbol in
-    ids := List.filter ((<>) id) !ids;
-    Hashtbl.remove !level2_patterns32 id;
-  with Not_found -> raise Interpretation_not_found);
-  pattern32_matrix :=
-    List.filter (fun (_, _, id') -> id <> id') !pattern32_matrix;
-  List.iter (fun f -> f !pattern32_matrix) !load_patterns32s
-
-let init () = List.iter (fun f -> f []) !load_patterns32s
-
 let instantiate_appl_pattern 
-  ~mk_appl ~mk_implicit ~term_of_uri ~term_of_nref env appl_pattern 
+  ~mk_appl ~mk_implicit ~term_of_nref env appl_pattern 
 =
   let lookup name =
     try List.assoc name env
@@ -196,11 +169,9 @@ let instantiate_appl_pattern
       assert false
   in
   let rec aux = function
-    | Ast.UriPattern uri -> term_of_uri uri
     | Ast.NRefPattern nref -> term_of_nref nref
     | Ast.ImplicitPattern -> mk_implicit false
     | Ast.VarPattern name -> lookup name
     | Ast.ApplPattern terms -> mk_appl (List.map aux terms)
   in
   aux appl_pattern
-