From ad8d37cce3b39565861014d870b91b1add0ec0e3 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 29 Sep 2009 16:53:28 +0000 Subject: [PATCH] ugly coerc db print --- .../components/ng_refiner/nCicUnifHint.ml | 77 ++++++++++++++++--- .../components/ng_refiner/nCicUnifHint.mli | 2 + helm/software/matita/lablGraphviz.ml | 8 +- helm/software/matita/matita.glade | 8 ++ helm/software/matita/matitaGui.ml | 4 + helm/software/matita/matitaMathView.ml | 24 ++++++ helm/software/matita/matitaTypes.ml | 3 + helm/software/matita/matitaTypes.mli | 2 +- 8 files changed, 114 insertions(+), 14 deletions(-) diff --git a/helm/software/components/ng_refiner/nCicUnifHint.ml b/helm/software/components/ng_refiner/nCicUnifHint.ml index ce8808552..bdd5b080b 100644 --- a/helm/software/components/ng_refiner/nCicUnifHint.ml +++ b/helm/software/components/ng_refiner/nCicUnifHint.ml @@ -14,19 +14,29 @@ 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; +;; diff --git a/helm/software/components/ng_refiner/nCicUnifHint.mli b/helm/software/components/ng_refiner/nCicUnifHint.mli index 862c9808e..421ef9ffb 100644 --- a/helm/software/components/ng_refiner/nCicUnifHint.mli +++ b/helm/software/components/ng_refiner/nCicUnifHint.mli @@ -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 diff --git a/helm/software/matita/lablGraphviz.ml b/helm/software/matita/lablGraphviz.ml index d67584c8c..ab817e294 100644 --- a/helm/software/matita/lablGraphviz.ml +++ b/helm/software/matita/lablGraphviz.ml @@ -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 diff --git a/helm/software/matita/matita.glade b/helm/software/matita/matita.glade index 75783e6ab..0d80fe22c 100644 --- a/helm/software/matita/matita.glade +++ b/helm/software/matita/matita.glade @@ -1283,6 +1283,14 @@ True + + + True + Displays the database of hints + Hints database + True + + True diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml index 8b38950bb..b6bba823f 100644 --- a/helm/software/matita/matitaGui.ml +++ b/helm/software/matita/matitaGui.ml @@ -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 diff --git a/helm/software/matita/matitaMathView.ml b/helm/software/matita/matitaMathView.ml index c666a34f7..e76c659a4 100644 --- a/helm/software/matita/matitaMathView.ml +++ b/helm/software/matita/matitaMathView.ml @@ -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"; diff --git a/helm/software/matita/matitaTypes.ml b/helm/software/matita/matitaTypes.ml index 7468bedfa..30e64892c 100644 --- a/helm/software/matita/matitaTypes.ml +++ b/helm/software/matita/matitaTypes.ml @@ -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 diff --git a/helm/software/matita/matitaTypes.mli b/helm/software/matita/matitaTypes.mli index a1e2fa9aa..6d672a123 100644 --- a/helm/software/matita/matitaTypes.mli +++ b/helm/software/matita/matitaTypes.mli @@ -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 -- 2.39.2