+let call_tactic_with_goal_input tactic () =
+ let module L = LogicalOperations in
+ let module G = Gdome in
+ let notebook = (rendering_window ())#notebook in
+ let output = ((rendering_window ())#output : GMathView.math_view) in
+ let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
+ let savedproof = !ProofEngine.proof in
+ let savedgoal = !ProofEngine.goal in
+ match notebook#proofw#get_selection with
+ Some node ->
+ let xpath =
+ ((node : Gdome.element)#getAttributeNS
+ ~namespaceURI:helmns
+ ~localName:(G.domString "xref"))#to_string
+ in
+ if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
+ else
+ begin
+ try
+ match !current_goal_infos with
+ Some (ids_to_terms, ids_to_father_ids,_) ->
+ let id = xpath in
+ tactic (Hashtbl.find ids_to_terms id) ;
+ refresh_sequent notebook ;
+ refresh_proof output
+ | None -> assert false (* "ERROR: No current term!!!" *)
+ with
+ RefreshSequentException e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+ "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
+ ProofEngine.proof := savedproof ;
+ ProofEngine.goal := savedgoal ;
+ refresh_sequent notebook
+ | RefreshProofException e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+ "proof: " ^ Printexc.to_string e ^ "</h1>") ;
+ ProofEngine.proof := savedproof ;
+ ProofEngine.goal := savedgoal ;
+ refresh_sequent notebook ;
+ refresh_proof output
+ | e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+ ProofEngine.proof := savedproof ;
+ ProofEngine.goal := savedgoal ;
+ end
+ | None ->
+ output_html outputhtml
+ ("<h1 color=\"red\">No term selected</h1>")
+;;
+
+let call_tactic_with_input_and_goal_input tactic () =
+ let module L = LogicalOperations in
+ let module G = Gdome in
+ let notebook = (rendering_window ())#notebook in
+ let output = ((rendering_window ())#output : GMathView.math_view) in
+ let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
+ let inputt = ((rendering_window ())#inputt : term_editor) in
+ let savedproof = !ProofEngine.proof in
+ let savedgoal = !ProofEngine.goal in
+ match notebook#proofw#get_selection with
+ Some node ->
+ let xpath =
+ ((node : Gdome.element)#getAttributeNS
+ ~namespaceURI:helmns
+ ~localName:(G.domString "xref"))#to_string
+ in
+ if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
+ else
+ begin
+ try
+ match !current_goal_infos with
+ Some (ids_to_terms, ids_to_father_ids,_) ->
+ let id = xpath in
+ let uri,metasenv,bo,ty =
+ match !ProofEngine.proof with
+ None -> assert false
+ | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty
+ in
+ let canonical_context =
+ match !ProofEngine.goal with
+ None -> assert false
+ | Some metano ->
+ let (_,canonical_context,_) =
+ List.find (function (m,_,_) -> m=metano) metasenv
+ in
+ canonical_context in
+ let context =
+ List.map
+ (function
+ Some (n,_) -> Some n
+ | None -> None
+ ) canonical_context
+ in
+ let dom,mk_metasenv_and_expr = inputt#get_term context metasenv
+ in
+ let (metasenv',expr) =
+ disambiguate_input canonical_context metasenv dom
+ mk_metasenv_and_expr
+ in
+ ProofEngine.proof := Some (uri,metasenv',bo,ty) ;
+ tactic ~goal_input:(Hashtbl.find ids_to_terms id)
+ ~input:expr ;
+ refresh_sequent notebook ;
+ refresh_proof output ;
+ inputt#reset
+ | None -> assert false (* "ERROR: No current term!!!" *)
+ with
+ RefreshSequentException e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+ "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
+ ProofEngine.proof := savedproof ;
+ ProofEngine.goal := savedgoal ;
+ refresh_sequent notebook
+ | RefreshProofException e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+ "proof: " ^ Printexc.to_string e ^ "</h1>") ;
+ ProofEngine.proof := savedproof ;
+ ProofEngine.goal := savedgoal ;
+ refresh_sequent notebook ;
+ refresh_proof output
+ | e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+ ProofEngine.proof := savedproof ;
+ ProofEngine.goal := savedgoal ;
+ end
+ | None ->
+ output_html outputhtml
+ ("<h1 color=\"red\">No term selected</h1>")
+;;
+
+let call_tactic_with_goal_input_in_scratch tactic scratch_window () =
+ let module L = LogicalOperations in
+ let module G = Gdome in
+ let mmlwidget = (scratch_window#mmlwidget : GMathView.math_view) in
+ let outputhtml = (scratch_window#outputhtml : GHtml.xmhtml) in
+ let savedproof = !ProofEngine.proof in
+ let savedgoal = !ProofEngine.goal in
+ match mmlwidget#get_selection with
+ Some node ->
+ let xpath =
+ ((node : Gdome.element)#getAttributeNS
+ ~namespaceURI:helmns
+ ~localName:(G.domString "xref"))#to_string
+ in
+ if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
+ else
+ begin
+ try
+ match !current_scratch_infos with
+ (* term is the whole goal in the scratch_area *)
+ Some (term,ids_to_terms, ids_to_father_ids,_) ->
+ let id = xpath in
+ let expr = tactic term (Hashtbl.find ids_to_terms id) in
+ let mml = mml_of_cic_term 111 expr in
+ scratch_window#show () ;
+ scratch_window#mmlwidget#load_tree ~dom:mml
+ | None -> assert false (* "ERROR: No current term!!!" *)
+ with
+ e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
+ end
+ | None ->
+ output_html outputhtml
+ ("<h1 color=\"red\">No term selected</h1>")
+;;
+
+let call_tactic_with_hypothesis_input tactic () =
+ let module L = LogicalOperations in
+ let module G = Gdome in
+ let notebook = (rendering_window ())#notebook in
+ let output = ((rendering_window ())#output : GMathView.math_view) in
+ let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
+ let savedproof = !ProofEngine.proof in
+ let savedgoal = !ProofEngine.goal in
+ match notebook#proofw#get_selection with
+ Some node ->
+ let xpath =
+ ((node : Gdome.element)#getAttributeNS
+ ~namespaceURI:helmns
+ ~localName:(G.domString "xref"))#to_string
+ in
+ if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
+ else
+ begin
+ try
+ match !current_goal_infos with
+ Some (_,_,ids_to_hypotheses) ->
+ let id = xpath in
+ tactic (Hashtbl.find ids_to_hypotheses id) ;
+ refresh_sequent notebook ;
+ refresh_proof output
+ | None -> assert false (* "ERROR: No current term!!!" *)
+ with
+ RefreshSequentException e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+ "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
+ ProofEngine.proof := savedproof ;
+ ProofEngine.goal := savedgoal ;
+ refresh_sequent notebook
+ | RefreshProofException e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+ "proof: " ^ Printexc.to_string e ^ "</h1>") ;
+ ProofEngine.proof := savedproof ;
+ ProofEngine.goal := savedgoal ;
+ refresh_sequent notebook ;
+ refresh_proof output
+ | e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+ ProofEngine.proof := savedproof ;
+ ProofEngine.goal := savedgoal ;
+ end
+ | None ->
+ output_html outputhtml
+ ("<h1 color=\"red\">No term selected</h1>")
+;;
+
+
+let intros = call_tactic ProofEngine.intros;;
+let exact = call_tactic_with_input ProofEngine.exact;;
+let apply = call_tactic_with_input ProofEngine.apply;;
+let elimsimplintros = call_tactic_with_input ProofEngine.elim_simpl_intros;;
+let elimtype = call_tactic_with_input ProofEngine.elim_type;;
+let whd = call_tactic_with_goal_input ProofEngine.whd;;
+let reduce = call_tactic_with_goal_input ProofEngine.reduce;;
+let simpl = call_tactic_with_goal_input ProofEngine.simpl;;
+let fold = call_tactic_with_input ProofEngine.fold;;
+let cut = call_tactic_with_input ProofEngine.cut;;
+let change = call_tactic_with_input_and_goal_input ProofEngine.change;;
+let letin = call_tactic_with_input ProofEngine.letin;;
+let ring = call_tactic ProofEngine.ring;;
+let clearbody = call_tactic_with_hypothesis_input ProofEngine.clearbody;;
+let clear = call_tactic_with_hypothesis_input ProofEngine.clear;;
+let fourier = call_tactic ProofEngine.fourier;;
+let rewritesimpl = call_tactic_with_input ProofEngine.rewrite_simpl;;
+let reflexivity = call_tactic ProofEngine.reflexivity;;
+let symmetry = call_tactic ProofEngine.symmetry;;
+let transitivity = call_tactic_with_input ProofEngine.transitivity;;
+let left = call_tactic ProofEngine.left;;
+let right = call_tactic ProofEngine.right;;
+let assumption = call_tactic ProofEngine.assumption;;
+
+let whd_in_scratch scratch_window =
+ call_tactic_with_goal_input_in_scratch ProofEngine.whd_in_scratch
+ scratch_window
+;;
+let reduce_in_scratch scratch_window =
+ call_tactic_with_goal_input_in_scratch ProofEngine.reduce_in_scratch
+ scratch_window
+;;
+let simpl_in_scratch scratch_window =
+ call_tactic_with_goal_input_in_scratch ProofEngine.simpl_in_scratch
+ scratch_window
+;;
+
+
+
+(**********************)
+(* END OF TACTICS *)
+(**********************)
+
+
+let show () =
+ let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
+ try
+ show_in_show_window (input_or_locate_uri ~title:"Show")
+ with
+ e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+;;
+
+exception NotADefinition;;
+
+let open_ () =
+ let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
+ let output = ((rendering_window ())#output : GMathView.math_view) in
+ let notebook = (rendering_window ())#notebook in
+ try
+ let uri = input_or_locate_uri ~title:"Open" in
+ CicTypeChecker.typecheck uri ;
+ let metasenv,bo,ty =
+ match CicEnvironment.get_cooked_obj uri with
+ Cic.Constant (_,Some bo,ty,_) -> [],bo,ty
+ | Cic.CurrentProof (_,metasenv,bo,ty,_) -> metasenv,bo,ty
+ | Cic.Constant _
+ | Cic.Variable _
+ | Cic.InductiveDefinition _ -> raise NotADefinition
+ in
+ ProofEngine.proof :=
+ Some (uri, metasenv, bo, ty) ;
+ ProofEngine.goal := None ;
+ refresh_sequent notebook ;
+ refresh_proof output
+ with
+ RefreshSequentException e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+ "sequent: " ^ Printexc.to_string e ^ "</h1>")
+ | RefreshProofException e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+ "proof: " ^ Printexc.to_string e ^ "</h1>")
+ | e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+;;
+
+
+let searchPattern () =
+ let inputt = ((rendering_window ())#inputt : term_editor) in
+ let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
+ try
+ let rec get_level ?(last_invalid=false) () =
+ match
+ GToolbox.input_string
+ ~title:"Insert the strictness parameter for the query:"
+ ((if last_invalid then
+ "Invalid input (must be a non-negative natural number). Insert again "
+ else
+ "Insert "
+ ) ^ "the strictness parameter for the query:")
+ with
+ None -> raise NoChoice
+ | Some n ->
+ try
+ int_of_string n
+ with
+ _ -> get_level ~last_invalid:true ()
+ in
+ let level = get_level () in
+ let metasenv =
+ match !ProofEngine.proof with
+ None -> assert false
+ | Some (_,metasenv,_,_) -> metasenv
+ in
+ match !ProofEngine.goal with
+ None -> ()
+ | Some metano ->
+ let (_, ey ,ty) = List.find (function (m,_,_) -> m=metano) metasenv in
+ let result = MQueryGenerator.searchPattern metasenv ey ty level in
+ let uris =
+ List.map
+ (function uri,_ ->
+ wrong_xpointer_format_from_wrong_xpointer_format' uri
+ ) result in
+ let html =
+ " <h1>Backward Query: </h1>" ^
+ " <h2>Levels: </h2> " ^
+ MQueryGenerator.string_of_levels
+ (MQueryGenerator.levels_of_term metasenv ey ty) "<br>" ^
+ " <pre>" ^ get_last_query result ^ "</pre>"
+ in
+ output_html outputhtml html ;
+ let uris',exc =
+ let rec filter_out =
+ function
+ [] -> [],""
+ | uri::tl ->
+ let tl',exc = filter_out tl in
+ try
+ if
+ ProofEngine.can_apply
+ (term_of_cic_textual_parser_uri
+ (cic_textual_parser_uri_of_string uri))
+ then
+ uri::tl',exc
+ else
+ tl',exc
+ with
+ e ->
+ let exc' =
+ "<h1 color=\"red\"> ^ Exception raised trying to apply " ^
+ uri ^ ": " ^ Printexc.to_string e ^ " </h1>" ^ exc
+ in
+ tl',exc'
+ in
+ filter_out uris
+ in
+ let html' =
+ " <h1>Objects that can actually be applied: </h1> " ^
+ String.concat "<br>" uris' ^ exc ^
+ " <h1>Number of false matches: " ^
+ string_of_int (List.length uris - List.length uris') ^ "</h1>" ^
+ " <h1>Number of good matches: " ^
+ string_of_int (List.length uris') ^ "</h1>"
+ in
+ output_html outputhtml html' ;
+ let uri' =
+ user_uri_choice ~title:"Ambiguous input."
+ ~msg:
+ "Many lemmas can be successfully applied. Please, choose one:"
+ uris'
+ in
+ inputt#set_term uri' ;
+ apply ()
+ with
+ e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
+;;
+