]> matita.cs.unibo.it Git - helm.git/commitdiff
ugly coerc db print
authorEnrico Tassi <enrico.tassi@inria.fr>
Tue, 29 Sep 2009 16:53:28 +0000 (16:53 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Tue, 29 Sep 2009 16:53:28 +0000 (16:53 +0000)
helm/software/components/ng_refiner/nCicUnifHint.ml
helm/software/components/ng_refiner/nCicUnifHint.mli
helm/software/matita/lablGraphviz.ml
helm/software/matita/matita.glade
helm/software/matita/matitaGui.ml
helm/software/matita/matitaMathView.ml
helm/software/matita/matitaTypes.ml
helm/software/matita/matitaTypes.mli

index ce88085521c2ddabda8d96069f9fba79bb90a876..bdd5b080b87bc2cdb2e45b44c39b18bccfb186b9 100644 (file)
 let debug s = prerr_endline (Lazy.force s);;
 let debug _ = ();;
 
-module COT : Set.OrderedType with type t = int * NCic.term = 
+module HOT : Set.OrderedType 
+with type t = int * NCic.term  * NCic.term * NCic.term = 
   struct
-        type t = int * NCic.term
+        (* precedence, skel1, skel2, term *)
+        type t = int * NCic.term * NCic.term * NCic.term
         let compare = Pervasives.compare
   end
 
-module HintSet = Set.Make(COT)
+module EOT : Set.OrderedType 
+with type t = int * NCic.term =
+  struct
+        type t = int * NCic.term 
+        let compare = Pervasives.compare
+  end
+
+module HintSet = Set.Make(HOT)
+module EqSet = Set.Make(EOT)
 
 module HDB = 
   Discrimination_tree.Make(NDiscriminationTree.NCicIndexable)(HintSet)
 
 module EQDB = 
-  Discrimination_tree.Make(NDiscriminationTree.NCicIndexable)(HintSet)
+  Discrimination_tree.Make(NDiscriminationTree.NCicIndexable)(EqSet)
 
 type db =
   HDB.t * (* hint database: (dummy A B)[?] |-> \forall X.(summy a b)[X] *)
@@ -86,16 +96,19 @@ let index_hint hdb context t1 t2 precedence =
         | NCic.Def (b,ty) -> NCic.LetIn (n,ty,b,t))
       t context 
   in
-  let data_hint = ctx2abstractions context (pair t1 t2) in
+  let data_hint = 
+    precedence, t1_skeleton, t2_skeleton, ctx2abstractions context (pair t1 t2)
+  in
   let data_t1 = t2_skeleton in
   let data_t2 = t1_skeleton in
 
   debug(lazy ("INDEXING: " ^ 
     NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] src ^ " |==> " ^
-    NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] data_hint));
+    NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] 
+      (let _,x,_,_ = data_hint in x)));
 
   hdb#set_uhint_db (
-      HDB.index (fst (hdb#uhint_db)) src (precedence, data_hint),
+      HDB.index (fst (hdb#uhint_db)) src data_hint,
       EQDB.index  
         (EQDB.index (snd (hdb#uhint_db)) t2_skeleton (precedence, data_t2))
         t1_skeleton (precedence, data_t1))
@@ -222,7 +235,7 @@ let eq_class_of hdb t1 =
           it sould retulr the whole content of the trie *)
   else
     let candidates = EQDB.retrieve_unifiables (snd hdb#uhint_db) t1 in
-    let candidates = HintSet.elements candidates in
+    let candidates = EqSet.elements candidates in
     let candidates = List.sort (fun (x,_) (y,_) -> compare x y) candidates in
     List.map snd candidates
  in
@@ -246,12 +259,12 @@ let look_for_hint hdb metasenv subst context t1 t2 =
   let candidates1 = HDB.retrieve_unifiables (fst hdb#uhint_db) (pair t1 t2) in
   let candidates2 = HDB.retrieve_unifiables (fst hdb#uhint_db) (pair t2 t1) in
   let candidates1 = 
-    List.map (fun (prec,ty) -> 
+    List.map (fun (prec,_,_,ty) -> 
        prec,true,saturate ~delta:max_int metasenv subst context ty 0) 
     (HintSet.elements candidates1) 
   in
   let candidates2 = 
-    List.map (fun (prec,ty) -> 
+    List.map (fun (prec,_,_,ty) -> 
        prec,false,saturate ~delta:max_int metasenv subst context ty 0) 
     (HintSet.elements candidates2) 
   in
@@ -300,3 +313,47 @@ let look_for_hint hdb metasenv subst context t1 t2 =
 
   rc
 ;;
+
+
+let generate_dot_file status fmt =
+  let module Pp = GraphvizPp.Dot in
+  let h_db, _ = status#uhint_db in
+  let names = ref [] in
+  let id = ref 0 in
+  let mangle l =
+    try List.assoc l !names
+    with Not_found ->
+      incr id;
+      names := (l,"node"^string_of_int!id) :: !names;
+      List.assoc l !names
+  in
+  let nodes = ref [] in
+  let edges = ref [] in
+  HDB.iter h_db (fun _key dataset -> 
+      List.iter
+        (fun (precedence, l,r, hint) ->
+            let l = 
+              Str.global_substitute (Str.regexp "\n") (fun _ -> "")
+               (NCicPp.ppterm 
+                ~margin:max_int ~metasenv:[] ~context:[] ~subst:[] l) 
+            in
+            let r = 
+              Str.global_substitute (Str.regexp "\n") (fun _ -> "")
+               (NCicPp.ppterm 
+                ~margin:max_int ~metasenv:[] ~context:[] ~subst:[] r)
+            in
+            let hint = 
+              string_of_int precedence ^ "..." ^
+              Str.global_substitute (Str.regexp "\n") (fun _ -> "")
+               (NCicPp.ppterm 
+                ~margin:max_int ~metasenv:[] ~context:[] ~subst:[] hint)
+            in
+            nodes := (mangle l,l) :: (mangle r,r) :: !nodes;
+            edges := (mangle l, mangle r, hint) :: !edges)
+        (HintSet.elements dataset);
+    );
+  List.iter (fun x, l -> Pp.node x ~attrs:["label",l] fmt) !nodes;
+  List.iter (fun x, y, l -> 
+      Pp.raw (Printf.sprintf "%s -- %s [ label=\"%s\" ];\n" x y "?") fmt)
+  !edges;
+;;
index 862c9808efc0193b00d78257cfd1f48f5ecbd2b7..421ef9ffb66e0d48672e3b2e01a4ecd1ab24d147 100644 (file)
@@ -42,3 +42,5 @@ val look_for_hint:
 
 val eq_class_of:
       #status -> NCic.term -> NCic.term list
+
+val generate_dot_file: #status -> Format.formatter -> unit
index d67584c8c99d4f700d99f39afa625c654a0c311b..ab817e2940394c19a197810fecd79d6d825711f9 100644 (file)
@@ -114,7 +114,8 @@ class graphviz_impl ?packing () =
           "coords", min_x^","^min_y^" "^max_x^","^max_y
          | x -> x) l
       in
-      let p =
+      try
+       let p =
         XmlPushParser.create_parser
           { XmlPushParser.default_callbacks with
             XmlPushParser.start_element =
@@ -123,8 +124,9 @@ class graphviz_impl ?packing () =
                 | "area" when is_rect attrs -> areas := attrs :: !areas
                 | "area" when is_poly attrs -> areas := rectify attrs :: !areas
                 | _ -> ()) } in
-      XmlPushParser.parse p (`File fname);
-      map <- !areas
+       XmlPushParser.parse p (`File fname);
+       map <- !areas  
+      with XmlPushParser.Parse_error _ -> ()
 
     method private find_href x y =
       List.find
index 75783e6ab0dc16099c6f9fd73b5ce95d72150932..0d80fe22c933960827789de606e3c3601b392610 100644 (file)
                                 <property name="use_underline">True</property>
                               </widget>
                             </child>
+                            <child>
+                              <widget class="GtkMenuItem" id="showHintsDbMenuItem">
+                                <property name="visible">True</property>
+                                <property name="tooltip" translatable="yes">Displays the database of hints</property>
+                                <property name="label" translatable="yes">Hints database</property>
+                                <property name="use_underline">True</property>
+                              </widget>
+                            </child>
                             <child>
                               <widget class="GtkImageMenuItem" id="showAutoGuiMenuItem">
                                 <property name="visible">True</property>
index 8b38950bb67d6b6ef6922e04cfbcef3b51a2c9c2..b6bba823f035893c481d4eaf3f4f9316bb270046 100644 (file)
@@ -995,6 +995,10 @@ class gui () =
         (fun _ -> 
           let c = MatitaMathView.cicBrowser () in
           c#load (`About `Coercions));
+      connect_menu_item main#showHintsDbMenuItem 
+        (fun _ -> 
+          let c = MatitaMathView.cicBrowser () in
+          c#load (`About `Hints));
       connect_menu_item main#showAutoGuiMenuItem 
         (fun _ -> MatitaAutoGui.auto_dialog Auto.get_auto_status);
       connect_menu_item main#showTermGrammarMenuItem 
index c666a34f7d7fe5f06efe5827e3660a5900e7bfc2..e76c659a4cb42ab194754060e36ca392fb76192e 100644 (file)
@@ -1035,6 +1035,25 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
   let load_easter_egg = lazy (
     win#browserImage#set_file (MatitaMisc.image_path "meegg.png"))
   in
+  let load_hints () =
+      let module Pp = GraphvizPp.Dot in
+      let filename, oc = Filename.open_temp_file "matita" ".dot" in
+      let fmt = Format.formatter_of_out_channel oc in
+      let status = (MatitaScript.current ())#grafite_status in
+      Pp.header 
+        ~name:"Hints"
+        ~graph_type:"graph"
+        ~graph_attrs:["overlap", "false"]
+        ~node_attrs:["fontsize", "9"; "width", ".4"; 
+            "height", ".4"; "shape", "box"]
+        ~edge_attrs:["fontsize", "10"; "len", "2"] fmt;
+      NCicUnifHint.generate_dot_file status fmt;
+      Pp.trailer fmt;
+      Pp.raw "@." fmt;
+      close_out oc;
+      gviz#load_graph_from_file ~gviz_cmd:"neato -Tpng" filename;
+      (*HExtlib.safe_remove filename*)
+  in
   let load_coerchgraph tred () = 
       let module Pp = GraphvizPp.Dot in
       let filename, oc = Filename.open_temp_file "matita" ".dot" in
@@ -1261,6 +1280,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
           | `About `Us -> self#egg ()
           | `About `CoercionsFull -> self#coerchgraph false ()
           | `About `Coercions -> self#coerchgraph true ()
+          | `About `Hints -> self#hints ()
           | `About `TeX -> self#tex ()
           | `About `Grammar -> self#grammar () 
           | `Check term -> self#_loadCheck term
@@ -1324,6 +1344,10 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
       load_coerchgraph tred ();
       self#_showGviz
 
+    method private hints () =
+      load_hints ();
+      self#_showGviz
+
     method private tex () =
       let b = Buffer.create 1000 in
       Printf.bprintf b "UTF-8 equivalence classes (rotate with ALT-L):\n\n";
index 7468bedfadfaafe84ef7edb1bdb0cec7ae973f85..30e64892cc2ede541a3313994e52325c170a4fbf 100644 (file)
@@ -39,6 +39,7 @@ type abouts =
   | `CoercionsFull
   | `TeX
   | `Grammar
+  | `Hints
   ]
   
 type mathViewer_entry =
@@ -63,6 +64,7 @@ let string_of_entry = function
   | `About `CoercionsFull -> "about:coercions"
   | `About `TeX -> "about:tex"
   | `About `Grammar -> "about:grammar"
+  | `About `Hints -> "about:hints"
   | `Check _ -> "check:"
   | `Cic (_, _) -> "term:"
   | `NCic (_, _, _, _) -> "nterm:"
@@ -87,6 +89,7 @@ let entry_of_string = function
   | "about:blank" -> `About `Blank
   | "about:proof" -> `About `Current_proof
   | "about:us"    -> `About `Us
+  | "about:hints"    -> `About `Hints
   | "about:coercions?tred=true"    -> `About `Coercions
   | "about:coercions"    -> `About `CoercionsFull
   | "about:tex"    -> `About `TeX
index a1e2fa9aab2844c06e54e084681413d5a7e05327..6d672a1238a01217b45142b4dc18cbc567308b94 100644 (file)
@@ -26,7 +26,7 @@
 exception Cancel
 
 type abouts = [ `Blank | `Current_proof | `Us | `Coercions 
- | `CoercionsFull | `TeX | `Grammar]
+ | `CoercionsFull | `TeX | `Grammar | `Hints]
 
 type mathViewer_entry =
   [ `About of abouts