From 394177fef9a7a158a527077b69928b0a9818bce8 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sat, 25 Nov 2006 11:23:02 +0000 Subject: [PATCH] added a test for the pullback stuff and the possibility to get the coercion graph printed without closures --- matita/matita.ml | 19 ++++++++++++++++++ matita/matitaMathView.ml | 16 +++++++++------ matita/matitaTypes.ml | 7 +++++-- matita/matitaTypes.mli | 2 +- matita/tests/pullback.ma | 42 ++++++++++++++++++++++++++++++++++++++++ 5 files changed, 77 insertions(+), 9 deletions(-) create mode 100644 matita/tests/pullback.ma diff --git a/matita/matita.ml b/matita/matita.ml index 609a014d0..783b8c023 100644 --- a/matita/matita.ml +++ b/matita/matita.ml @@ -198,6 +198,22 @@ let _ = let nb = gui#main#hintNotebook in nb#goto_page ((nb#current_page + 1) mod 3)); *) addDebugSeparator (); +(* + addDebugItem "meets between L and R" + (fun _ -> + let l = CoercDb.coerc_carr_of_term (CicUtil.term_of_uri + (UriManager.uri_of_string "cic:/matita/test/L.ind#xpointer(1/1)" )) + in + let r = CoercDb.coerc_carr_of_term (CicUtil.term_of_uri + (UriManager.uri_of_string "cic:/matita/test/R.ind#xpointer(1/1)" )) + in + let meets = CoercGraph.meets l r in + prerr_endline "MEETS:"; + List.iter (fun carr -> prerr_endline (CicPp.ppterm (CoercDb.term_of_carr + carr))) meets + ); + addDebugSeparator (); +*) addDebugItem "disable all (pretty printing) notations" (fun _ -> CicNotation.set_active_notations []); addDebugItem "enable all (pretty printing) notations" @@ -217,6 +233,9 @@ let _ = addDebugItem "show coercions graph" (fun _ -> let c = MatitaMathView.cicBrowser () in c#load (`About `Coercions)); + addDebugItem "show coercions graph (full)" (fun _ -> + let c = MatitaMathView.cicBrowser () in + c#load (`About `CoercionsFull)); addDebugItem "dump coercions Db" (fun _ -> List.iter (fun (s,t,ul) -> diff --git a/matita/matitaMathView.ml b/matita/matitaMathView.ml index 5ae8baab6..ee49267fe 100644 --- a/matita/matitaMathView.ml +++ b/matita/matitaMathView.ml @@ -844,12 +844,15 @@ 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_coerchgraph () = + let load_coerchgraph tred () = let str = CoercGraph.generate_dot_file () in let filename, oc = Filename.open_temp_file "matita" ".dot" in output_string oc str; close_out oc; - gviz#load_graph_from_file filename; + if tred then + gviz#load_graph_from_file ~gviz_cmd:"tred|dot" filename + else + gviz#load_graph_from_file filename; HExtlib.safe_remove filename in object (self) @@ -1024,13 +1027,14 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) method private _load ?(force=false) entry = handle_error (fun () -> if entry <> current_entry || entry = `About `Current_proof || entry = - `About `Coercions || force then + `About `Coercions || entry = `About `CoercionsFull || force then begin (match entry with | `About `Current_proof -> self#home () | `About `Blank -> self#blank () | `About `Us -> self#egg () - | `About `Coercions -> self#coerchgraph () + | `About `CoercionsFull -> self#coerchgraph false () + | `About `Coercions -> self#coerchgraph true () | `Check term -> self#_loadCheck term | `Cic (term, metasenv) -> self#_loadTermCic term metasenv | `Development d -> self#_showDevelDeps d @@ -1079,8 +1083,8 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) self#redraw_gviz ~center_on:uri (); self#_showGviz - method private coerchgraph () = - load_coerchgraph (); + method private coerchgraph tred () = + load_coerchgraph tred (); self#_showGviz method private home () = diff --git a/matita/matitaTypes.ml b/matita/matitaTypes.ml index 791713e56..23d0d832f 100644 --- a/matita/matitaTypes.ml +++ b/matita/matitaTypes.ml @@ -36,6 +36,7 @@ type abouts = | `Current_proof | `Us | `Coercions + | `CoercionsFull ] type mathViewer_entry = @@ -54,7 +55,8 @@ let string_of_entry = function | `About `Blank -> "about:blank" | `About `Current_proof -> "about:proof" | `About `Us -> "about:us" - | `About `Coercions -> "about:coercions" + | `About `Coercions -> "about:coercions?tred=true" + | `About `CoercionsFull -> "about:coercions" | `Check _ -> "check:" | `Cic (_, _) -> "term:" | `Development d -> "devel:/" ^ d @@ -77,7 +79,8 @@ let entry_of_string = function | "about:blank" -> `About `Blank | "about:proof" -> `About `Current_proof | "about:us" -> `About `Us - | "about:coercions" -> `About `Coercions + | "about:coercions?tred=true" -> `About `Coercions + | "about:coercions" -> `About `CoercionsFull | _ -> (* only about entries supported ATM *) raise (Invalid_argument "entry_of_string") diff --git a/matita/matitaTypes.mli b/matita/matitaTypes.mli index c2e3f40ed..c71c99dcc 100644 --- a/matita/matitaTypes.mli +++ b/matita/matitaTypes.mli @@ -25,7 +25,7 @@ exception Cancel -type abouts = [ `Blank | `Current_proof | `Us | `Coercions] +type abouts = [ `Blank | `Current_proof | `Us | `Coercions | `CoercionsFull] type mathViewer_entry = [ `About of abouts diff --git a/matita/tests/pullback.ma b/matita/tests/pullback.ma new file mode 100644 index 000000000..228d27d47 --- /dev/null +++ b/matita/tests/pullback.ma @@ -0,0 +1,42 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +set "baseuri" "cic:/matita/test/". + +inductive T : Type \def t : T. +inductive L : Type \def l : L. +inductive R : Type \def r : R. +inductive R1 : Type \def r1 : R1. +inductive P1 : Type \def p1 : P1. +inductive P2 : Type \def p2 : P2. + +definition L_to_T : L \to T \def \lambda x.t. +definition R_to_T : R \to T \def \lambda x.t. +definition P1_to_L : P1 \to L \def \lambda x.l. +definition P1_to_R1 : P1 \to R1 \def \lambda x.r1. +definition R1_to_P2 : R1 \to P2 \def \lambda x.p2. +definition R1_to_R : R1 \to R \def \lambda x.r. +definition P2_to_L : P2 \to L \def \lambda x.l. +definition P2_to_R : P2 \to R \def \lambda x.r. +definition P1_to_P1 : P1 \to P1 \def \lambda x.p1. + +coercion cic:/matita/test/L_to_T.con. +coercion cic:/matita/test/R_to_T.con. +coercion cic:/matita/test/P1_to_L.con. +coercion cic:/matita/test/P1_to_R1.con. +coercion cic:/matita/test/R1_to_R.con. +coercion cic:/matita/test/R1_to_P2.con. +coercion cic:/matita/test/P2_to_L.con. +coercion cic:/matita/test/P2_to_R.con. +coercion cic:/matita/test/P1_to_P1.con. -- 2.39.2