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
</child>
<child>
- <widget class="GtkImage" id="EasterEggImage">
+ <widget class="GtkScrolledWindow" id="scrolledwindow11">
<property name="visible">True</property>
- <property name="xalign">0.5</property>
- <property name="yalign">0.5</property>
- <property name="xpad">0</property>
- <property name="ypad">0</property>
+ <property name="can_focus">True</property>
+ <property name="hscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
+ <property name="vscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
+ <property name="shadow_type">GTK_SHADOW_NONE</property>
+ <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
+
+ <child>
+ <widget class="GtkViewport" id="viewport2">
+ <property name="visible">True</property>
+ <property name="shadow_type">GTK_SHADOW_NONE</property>
+
+ <child>
+ <widget class="GtkImage" id="BrowserImage">
+ <property name="visible">True</property>
+ <property name="xalign">0.5</property>
+ <property name="yalign">0.5</property>
+ <property name="xpad">0</property>
+ <property name="ypad">0</property>
+ </widget>
+ </child>
+ </widget>
+ </child>
</widget>
<packing>
<property name="tab_expand">False</property>
| 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
(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"
let tab_label meta_markup =
let rec aux =
function
- | `Current m -> sprintf "<b>%s</b>" (aux m)
| `Closed m -> sprintf "<s>%s</s>" (aux m)
+ | `Current m -> sprintf "<b>%s</b>" (aux m)
| `Shift (pos, m) -> sprintf "|<sub>%d</sub>: %s" pos (aux m)
| `Meta n -> sprintf "?%d" n
in
~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
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
* @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
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
[ `Blank
| `Current_proof
| `Us
+ | `Coercions
]
type mathViewer_entry =
| `About `Blank -> "about:blank"
| `About `Current_proof -> "about:proof"
| `About `Us -> "about:us"
+ | `About `Coercions -> "about:coercions"
| `Check _ -> "check:"
| `Cic (_, _) -> "term:"
| `Dir uri -> uri
| "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")
exception Cancel
-type abouts = [ `Blank | `Current_proof | `Us ]
+type abouts = [ `Blank | `Current_proof | `Us | `Coercions]
type mathViewer_entry =
[ `About of abouts
(**************************************************************************)
set "baseuri" "cic:/matita/tests/coercions/".
-include "legacy/coq.ma".
+include "nat/nat.ma".
inductive pos: Set \def
| one : pos
\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.
+
+
apply H;
[assumption
|3,5:assumption;
- 4:assumption
+ |4:assumption
|*:assumption
]
qed.
\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.
projects / helm.git / commitdiff