From 9f49495f5f1e54ccacb8142043cba65ca55b7125 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 10 Jul 2006 17:09:21 +0000 Subject: [PATCH] - cheanges for the new coercion stuff (including the generated graph) - new test for coercions - new test for tinycals --- helm/software/matita/applyTransformation.ml | 2 +- helm/software/matita/matita.glade | 28 ++++++++++++++--- helm/software/matita/matita.ml | 35 ++++++++++++--------- helm/software/matita/matitaMathView.ml | 26 ++++++++++++--- helm/software/matita/matitaTypes.ml | 3 ++ helm/software/matita/matitaTypes.mli | 2 +- helm/software/matita/tests/coercions.ma | 26 +++++++++++++-- helm/software/matita/tests/tinycals.ma | 16 +++++----- 8 files changed, 104 insertions(+), 34 deletions(-) diff --git a/helm/software/matita/applyTransformation.ml b/helm/software/matita/applyTransformation.ml index fe8d9e569..6e92cfa95 100644 --- a/helm/software/matita/applyTransformation.ml +++ b/helm/software/matita/applyTransformation.ml @@ -78,7 +78,7 @@ let txt_of_cic_sequent_conclusion size metasenv sequent = let t, ids_to_uris = TermAcicContent.ast_of_acic ids_to_inner_sorts t in let t = TermContentPres.pp_ast t in let t = CicNotationPres.render ids_to_uris t in - BoxPp.render_to_string size t + BoxPp.render_to_string (function x::_ -> x | _ -> assert false) size t let txt_of_cic_term size metasenv context t = let fake_sequent = (-1,context,t) in diff --git a/helm/software/matita/matita.glade b/helm/software/matita/matita.glade index a756e4042..8fc50338f 100644 --- a/helm/software/matita/matita.glade +++ b/helm/software/matita/matita.glade @@ -412,12 +412,30 @@ - + True - 0.5 - 0.5 - 0 - 0 + True + GTK_POLICY_AUTOMATIC + GTK_POLICY_AUTOMATIC + GTK_SHADOW_NONE + GTK_CORNER_TOP_LEFT + + + + True + GTK_SHADOW_NONE + + + + True + 0.5 + 0.5 + 0 + 0 + + + + False diff --git a/helm/software/matita/matita.ml b/helm/software/matita/matita.ml index 3c5bf8441..164518426 100644 --- a/helm/software/matita/matita.ml +++ b/helm/software/matita/matita.ml @@ -160,6 +160,20 @@ let _ = | Incomplete_proof i -> let _,_,p,_ = i.GrafiteTypes.proof in p | Proof p -> let _,_,p,_ = p in p | Intermediate _ -> assert false))); + addDebugItem "Print current proof (natural language) to stderr" + (fun _ -> + prerr_endline + (ObjPp.obj_to_string 120 + (match + (MatitaScript.current ())#grafite_status.GrafiteTypes.proof_status + with + | GrafiteTypes.No_proof -> assert false + | Incomplete_proof i -> + let _,m,p,ty = i.GrafiteTypes.proof in + Cic.CurrentProof ("current (incomplete) proof",m,p,ty,[],[]) + | Proof (_,m,p,ty) -> + Cic.CurrentProof ("current proof",m,p,ty,[],[]) + | Intermediate _ -> assert false))); (* addDebugItem "ask record choice" (fun _ -> HLog.debug (string_of_int @@ -187,26 +201,19 @@ let _ = (fun _ -> GrafiteDisambiguator.only_one_pass := true); addDebugSeparator (); addDebugItem "enable coercions hiding" - (fun _ -> TermAcicContent.hide_coercions := true); + (fun _ -> Acic2content.hide_coercions := true); addDebugItem "disable coercions hiding" - (fun _ -> TermAcicContent.hide_coercions := false); + (fun _ -> Acic2content.hide_coercions := false); + addDebugItem "show coercions graph" (fun _ -> + let c = MatitaMathView.cicBrowser () in + c#load (`About `Coercions)); addDebugItem "dump coercions Db" (fun _ -> List.iter - (fun (s,t,u) -> + (fun (s,t,ul) -> HLog.debug - (UriManager.name_of_uri u ^ ":" + ((String.concat "," (List.map UriManager.name_of_uri ul)) ^ ":" ^ CoercDb.name_of_carr s ^ " -> " ^ CoercDb.name_of_carr t)) (CoercDb.to_list ())); - addDebugItem "show coercions graph" (fun _ -> - let str = CoercGraph.generate_dot_file () in - let filename, oc = Filename.open_temp_file "xx" ".dot" in - output_string oc str; - close_out oc; - let ps = Filename.temp_file "yy" ".png" in - ignore (Unix.system ("/usr/bin/dot -Tpng -o" ^ ps ^ " " ^ filename)); - ignore (Unix.system ("/usr/bin/display " ^ ps)); - Sys.remove ps; - Sys.remove filename); addDebugSeparator (); let mview () = (MatitaMathView.sequentsViewer_instance ())#cicMathView in (* addDebugItem "save (sequent) MathML to matita.xml" diff --git a/helm/software/matita/matitaMathView.ml b/helm/software/matita/matitaMathView.ml index 5de25e45b..486866013 100644 --- a/helm/software/matita/matitaMathView.ml +++ b/helm/software/matita/matitaMathView.ml @@ -571,8 +571,8 @@ end let tab_label meta_markup = let rec aux = function - | `Current m -> sprintf "%s" (aux m) | `Closed m -> sprintf "%s" (aux m) + | `Current m -> sprintf "%s" (aux m) | `Shift (pos, m) -> sprintf "|%d: %s" pos (aux m) | `Meta n -> sprintf "?%d" n in @@ -694,7 +694,8 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () = ~env:(fun depth tag (pos, sw) -> let markup = match depth, pos with - | 0, _ -> `Current (render_switch sw) + | 0, 0 -> `Current (render_switch sw) + | 0, _ -> `Shift (pos, `Current (render_switch sw)) | 1, pos when Stack.head_tag stack = `BranchTag -> `Shift (pos, render_switch sw) | _ -> render_switch sw @@ -824,7 +825,18 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) in let handle_error' f = (fun () -> handle_error (fun () -> f ())) in let load_easter_egg = lazy ( - win#easterEggImage#set_file (MatitaMisc.image_path "meegg.png")) + win#browserImage#set_file (MatitaMisc.image_path "meegg.png")) + in + let load_coerchgraph () = + let str = CoercGraph.generate_dot_file () in + let filename, oc = Filename.open_temp_file "xx" ".dot" in + output_string oc str; + close_out oc; + let ps = Filename.temp_file "yy" ".png" in + ignore (Unix.system ("/usr/bin/dot -Tpng -o" ^ ps ^ " " ^ filename)); + Sys.remove filename; + at_exit (fun _ -> Sys.remove ps); + win#browserImage#set_file ps in object (self) inherit scriptAccessor @@ -940,12 +952,14 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) * @param uri string *) method private _load ?(force=false) entry = handle_error (fun () -> - if entry <> current_entry || entry = `About `Current_proof || force then + if entry <> current_entry || entry = `About `Current_proof || entry = + `About `Coercions || force then begin (match entry with | `About `Current_proof -> self#home () | `About `Blank -> self#blank () | `About `Us -> self#egg () + | `About `Coercions -> self#coerchgraph () | `Check term -> self#_loadCheck term | `Cic (term, metasenv) -> self#_loadTermCic term metasenv | `Dir dir -> self#_loadDir dir @@ -969,6 +983,10 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) win#mathOrListNotebook#goto_page 2; Lazy.force load_easter_egg + method private coerchgraph () = + win#mathOrListNotebook#goto_page 2; + load_coerchgraph () + method private home () = self#_showMath; match self#script#grafite_status.proof_status with diff --git a/helm/software/matita/matitaTypes.ml b/helm/software/matita/matitaTypes.ml index 13543dbb6..5e2e98062 100644 --- a/helm/software/matita/matitaTypes.ml +++ b/helm/software/matita/matitaTypes.ml @@ -35,6 +35,7 @@ type abouts = [ `Blank | `Current_proof | `Us + | `Coercions ] type mathViewer_entry = @@ -50,6 +51,7 @@ let string_of_entry = function | `About `Blank -> "about:blank" | `About `Current_proof -> "about:proof" | `About `Us -> "about:us" + | `About `Coercions -> "about:coercions" | `Check _ -> "check:" | `Cic (_, _) -> "term:" | `Dir uri -> uri @@ -60,6 +62,7 @@ let entry_of_string = function | "about:blank" -> `About `Blank | "about:proof" -> `About `Current_proof | "about:us" -> `About `Us + | "about:coercions" -> `About `Coercions | _ -> (* only about entries supported ATM *) raise (Invalid_argument "entry_of_string") diff --git a/helm/software/matita/matitaTypes.mli b/helm/software/matita/matitaTypes.mli index be77c4435..78e0c2541 100644 --- a/helm/software/matita/matitaTypes.mli +++ b/helm/software/matita/matitaTypes.mli @@ -25,7 +25,7 @@ exception Cancel -type abouts = [ `Blank | `Current_proof | `Us ] +type abouts = [ `Blank | `Current_proof | `Us | `Coercions] type mathViewer_entry = [ `About of abouts diff --git a/helm/software/matita/tests/coercions.ma b/helm/software/matita/tests/coercions.ma index 20b15cd26..914126de2 100644 --- a/helm/software/matita/tests/coercions.ma +++ b/helm/software/matita/tests/coercions.ma @@ -13,7 +13,7 @@ (**************************************************************************) set "baseuri" "cic:/matita/tests/coercions/". -include "legacy/coq.ma". +include "nat/nat.ma". inductive pos: Set \def | one : pos @@ -61,4 +61,26 @@ definition double2: \def \lambda f:int \to int. \lambda x : pos .f (nat2int (pos2nat x)). - +coercion cic:/matita/logic/equality/eq_f.con. +coercion cic:/matita/logic/equality/eq_f1.con. +variant xxx : ? \def eq_f. +coercion cic:/matita/tests/coercions/xxx.con. + +theorem coercion_svelta : \forall T,S:Type.\forall f:T \to S.\forall x,y:T.x=y \to f y = f x. + intros. + apply ((\lambda h:f y = f x.h) H). +qed. + +variant pos2nat' : ? \def pos2nat. + +coercion cic:/matita/tests/coercions/xxx.con. + +inductive initial: Set \def iii : initial. + +definition i2pos: ? \def \lambda x:initial.one. + +coercion cic:/matita/tests/coercions/i2pos.con. + +coercion cic:/matita/tests/coercions/pos2nat'.con. + + diff --git a/helm/software/matita/tests/tinycals.ma b/helm/software/matita/tests/tinycals.ma index 5cd2548a8..7bc189261 100644 --- a/helm/software/matita/tests/tinycals.ma +++ b/helm/software/matita/tests/tinycals.ma @@ -21,7 +21,7 @@ intros. apply H; [assumption |3,5:assumption; - 4:assumption + |4:assumption |*:assumption ] qed. @@ -31,19 +31,21 @@ theorem prova1: \forall H:A \to A \to A \to A \to A \to B.A \to B. intros. apply H; - [*:assumption - ] + [*:assumption] qed. +include "logic/connectives.ma". + theorem prova2: \forall A,B:Prop. - \forall H:A \to A \to A \to A \to A \to B.A \to B. + \forall H:A \to A \to A \to (A \land A) \to A \to B.A \to B. intros. apply H; [2:assumption - |assumption - 3,5:assumption - *:assumption + |4:split.assumption + |3,5:assumption + |*:assumption ] +assumption. qed. -- 2.39.2