(* *)
(******************************************************************************)
+open Printf
+
exception RefreshSequentException of exn;;
exception RefreshProofException of exn;;
set_metasenv : Cic.metasenv -> unit ;
context: Cic.context ;
set_context : Cic.context -> unit >
- (* output messages *)
- val output_html : string -> unit
(* GUI refresh functions *)
val refresh_proof : unit -> unit
val refresh_goals : unit -> unit
val decompose_uris_choice_callback :
(UriManager.uri * int * 'a) list ->
(UriManager.uri * int * 'b list) list
- val mk_fresh_name_callback :
- Cic.context -> Cic.name -> typ:Cic.term -> Cic.name
+ val mk_fresh_name_callback : ProofEngineTypes.mk_fresh_name_type
+ val mqi_handle : MQIConn.handle
+ val dbd:Mysql.dbd
end
;;
val whd_in_scratch : unit -> unit
val reduce_in_scratch : unit -> unit
val simpl_in_scratch : unit -> unit
+ val auto : unit -> unit
end
module Make (C: Callbacks) : Tactics =
struct
+ let print_uncaught_exception e =
+ HelmLogger.log (`Error (`T (sprintf "Uncaught exception: %s"
+ (Printexc.to_string e))))
+
+ let handle_refresh_exception f savedproof savedgoal =
+ try
+ f ()
+ with
+ | RefreshSequentException e ->
+ HelmLogger.log (`Error (`T
+ (sprintf "Exception raised during the refresh of the sequent: %s"
+ (Printexc.to_string e))));
+ ProofEngine.set_proof savedproof ;
+ ProofEngine.goal := savedgoal ;
+ C.refresh_goals ()
+ | RefreshProofException e ->
+ HelmLogger.log (`Error (`T
+ (sprintf "Exception raised during the refresh of the proof: %s"
+ (Printexc.to_string e))));
+ ProofEngine.set_proof savedproof ;
+ ProofEngine.goal := savedgoal ;
+ C.refresh_goals () ;
+ C.refresh_proof ()
+ | e ->
+ print_uncaught_exception e;
+ ProofEngine.set_proof savedproof ;
+ ProofEngine.goal := savedgoal
+
let call_tactic tactic () =
- let savedproof = !ProofEngine.proof in
+ let savedproof = ProofEngine.get_proof () in
let savedgoal = !ProofEngine.goal in
- begin
- try
- tactic () ;
- C.refresh_goals () ;
- C.refresh_proof ()
- with
- RefreshSequentException e ->
- C.output_html
- ("<h1 color=\"red\">Exception raised during the refresh of the " ^
- "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
- ProofEngine.proof := savedproof ;
- ProofEngine.goal := savedgoal ;
- C.refresh_goals ()
- | RefreshProofException e ->
- C.output_html
- ("<h1 color=\"red\">Exception raised during the refresh of the " ^
- "proof: " ^ Printexc.to_string e ^ "</h1>") ;
- ProofEngine.proof := savedproof ;
- ProofEngine.goal := savedgoal ;
- C.refresh_goals () ;
- C.refresh_proof ()
- | e ->
- C.output_html
- ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
- ProofEngine.proof := savedproof ;
- ProofEngine.goal := savedgoal
- end
+ handle_refresh_exception
+ (fun () ->
+ tactic ();
+ C.refresh_goals ();
+ C.refresh_proof ())
+ savedproof savedgoal
let call_tactic_with_input tactic ?term () =
- let savedproof = !ProofEngine.proof in
+ let savedproof = ProofEngine.get_proof () in
let savedgoal = !ProofEngine.goal in
let uri,metasenv,bo,ty =
- match !ProofEngine.proof with
+ match ProofEngine.get_proof () with
None -> assert false
| Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty
in
in
canonical_context
in
- try
- let metasenv',expr =
- (match term with
- | None -> ()
- | Some t -> (C.term_editor ())#set_term t);
- (C.term_editor ())#get_metasenv_and_term canonical_context metasenv
- in
- ProofEngine.proof := Some (uri,metasenv',bo,ty) ;
- tactic expr ;
- C.refresh_goals () ;
- C.refresh_proof () ;
- (C.term_editor ())#reset
- with
- RefreshSequentException e ->
- C.output_html
- ("<h1 color=\"red\">Exception raised during the refresh of the " ^
- "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
- ProofEngine.proof := savedproof ;
- ProofEngine.goal := savedgoal ;
- C.refresh_goals ()
- | RefreshProofException e ->
- C.output_html
- ("<h1 color=\"red\">Exception raised during the refresh of the " ^
- "proof: " ^ Printexc.to_string e ^ "</h1>") ;
- ProofEngine.proof := savedproof ;
- ProofEngine.goal := savedgoal ;
+ handle_refresh_exception
+ (fun () ->
+ let metasenv',expr,ugraph = (*TASSI: FIX THIS*)
+ (match term with
+ | None -> ()
+ | Some t -> (C.term_editor ())#set_term t);
+ (C.term_editor ())#get_metasenv_and_term canonical_context metasenv
+ in
+ ProofEngine.set_proof (Some (uri,metasenv',bo,ty)) ;
+ tactic expr ;
C.refresh_goals () ;
- C.refresh_proof ()
- | e ->
- C.output_html
- ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
- ProofEngine.proof := savedproof ;
- ProofEngine.goal := savedgoal
+ C.refresh_proof () ;
+ (C.term_editor ())#reset)
+ savedproof savedgoal
let call_tactic_with_goal_input tactic () =
let module L = LogicalOperations in
let module G = Gdome in
- let savedproof = !ProofEngine.proof in
+ let savedproof = ProofEngine.get_proof () in
let savedgoal = !ProofEngine.goal in
match (C.sequent_viewer ())#get_selected_terms with
- [term] ->
- begin
- try
- tactic term ;
- C.refresh_goals () ;
- C.refresh_proof ()
- with
- RefreshSequentException e ->
- C.output_html
- ("<h1 color=\"red\">Exception raised during the refresh of " ^
- "the sequent: " ^ Printexc.to_string e ^ "</h1>") ;
- ProofEngine.proof := savedproof ;
- ProofEngine.goal := savedgoal ;
- C.refresh_goals ()
- | RefreshProofException e ->
- C.output_html
- ("<h1 color=\"red\">Exception raised during the refresh of " ^
- "the proof: " ^ Printexc.to_string e ^ "</h1>") ;
- ProofEngine.proof := savedproof ;
- ProofEngine.goal := savedgoal ;
- C.refresh_goals () ;
- C.refresh_proof ()
- | e ->
- C.output_html
- ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
- ProofEngine.proof := savedproof ;
- ProofEngine.goal := savedgoal ;
- end
- | [] ->
- C.output_html
- ("<h1 color=\"red\">No term selected</h1>")
- | _ ->
- C.output_html
- ("<h1 color=\"red\">Many terms selected</h1>")
+ | [term] ->
+ handle_refresh_exception
+ (fun () ->
+ tactic term ;
+ C.refresh_goals () ;
+ C.refresh_proof ())
+ savedproof savedgoal
+ | [] -> HelmLogger.log (`Error (`T "No term selected"))
+ | _ -> HelmLogger.log (`Error (`T "Too many terms selected"))
let call_tactic_with_goal_inputs tactic () =
let module L = LogicalOperations in
let module G = Gdome in
- let savedproof = !ProofEngine.proof in
+ let savedproof = ProofEngine.get_proof () in
let savedgoal = !ProofEngine.goal in
- try
- match (C.sequent_viewer ())#get_selected_terms with
- [] ->
- C.output_html
- ("<h1 color=\"red\">No term selected</h1>")
- | terms ->
- tactic terms ;
- C.refresh_goals () ;
- C.refresh_proof () ;
- with
- RefreshSequentException e ->
- C.output_html
- ("<h1 color=\"red\">Exception raised during the refresh of the " ^
- "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
- ProofEngine.proof := savedproof ;
- ProofEngine.goal := savedgoal ;
- C.refresh_goals ()
- | RefreshProofException e ->
- C.output_html
- ("<h1 color=\"red\">Exception raised during the refresh of the " ^
- "proof: " ^ Printexc.to_string e ^ "</h1>") ;
- ProofEngine.proof := savedproof ;
- ProofEngine.goal := savedgoal ;
- C.refresh_goals () ;
- C.refresh_proof ()
- | e ->
- C.output_html
- ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
- ProofEngine.proof := savedproof ;
- ProofEngine.goal := savedgoal
+ handle_refresh_exception
+ (fun () ->
+ match (C.sequent_viewer ())#get_selected_terms with
+ | [] -> HelmLogger.log (`Error (`T "No term selected"))
+ | terms ->
+ tactic terms ;
+ C.refresh_goals () ;
+ C.refresh_proof ())
+ savedproof savedgoal
let call_tactic_with_input_and_goal_input tactic () =
let module L = LogicalOperations in
let module G = Gdome in
- let savedproof = !ProofEngine.proof in
+ let savedproof = ProofEngine.get_proof () in
let savedgoal = !ProofEngine.goal in
match (C.sequent_viewer ())#get_selected_terms with
[term] ->
- begin
- try
- 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 (metasenv',expr) =
- (C.term_editor ())#get_metasenv_and_term canonical_context metasenv
- in
- ProofEngine.proof := Some (uri,metasenv',bo,ty) ;
- tactic ~goal_input:term ~input:expr ;
- C.refresh_goals () ;
- C.refresh_proof () ;
- (C.term_editor ())#reset
- with
- RefreshSequentException e ->
- C.output_html
- ("<h1 color=\"red\">Exception raised during the refresh of " ^
- "the sequent: " ^ Printexc.to_string e ^ "</h1>") ;
- ProofEngine.proof := savedproof ;
- ProofEngine.goal := savedgoal ;
- C.refresh_goals ()
- | RefreshProofException e ->
- C.output_html
- ("<h1 color=\"red\">Exception raised during the refresh of " ^
- "the proof: " ^ Printexc.to_string e ^ "</h1>") ;
- ProofEngine.proof := savedproof ;
- ProofEngine.goal := savedgoal ;
- C.refresh_goals () ;
- C.refresh_proof ()
- | e ->
- C.output_html
- ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
- ProofEngine.proof := savedproof ;
- ProofEngine.goal := savedgoal ;
- end
- | [] ->
- C.output_html
- ("<h1 color=\"red\">No term selected</h1>")
- | _ ->
- C.output_html
- ("<h1 color=\"red\">Many terms selected</h1>")
+ handle_refresh_exception
+ (fun () ->
+ let uri,metasenv,bo,ty =
+ match ProofEngine.get_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 (metasenv',expr,ugraph) =(* FIX THIS AND *)
+ (C.term_editor ())#get_metasenv_and_term
+ canonical_context metasenv
+ in
+ ProofEngine.set_proof (Some (uri,metasenv',bo,ty)) ;
+ tactic ~goal_input:term ~input:expr ;
+ C.refresh_goals () ;
+ C.refresh_proof () ;
+ (C.term_editor ())#reset)
+ savedproof savedgoal
+ | [] -> HelmLogger.log (`Error (`T "No term selected"))
+ | _ -> HelmLogger.log (`Error (`T "Too many terms selected"))
let call_tactic_with_goal_input_in_scratch tactic () =
let module L = LogicalOperations in
let module G = Gdome in
let scratch_window = C.scratch_window () in
match scratch_window#sequent_viewer#get_selected_terms with
- [term] ->
+ | [term] ->
begin
try
let expr = tactic term scratch_window#term in
scratch_window#set_term expr ;
scratch_window#show () ;
with
- e ->
- C.output_html
- ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
+ e -> print_uncaught_exception e
end
- | [] ->
- C.output_html
- ("<h1 color=\"red\">No term selected</h1>")
- | _ ->
- C.output_html
- ("<h1 color=\"red\">Many terms selected</h1>")
+ | [] -> HelmLogger.log (`Error (`T "No term selected"))
+ | _ -> HelmLogger.log (`Error (`T "Too many terms selected"))
let call_tactic_with_goal_inputs_in_scratch tactic () =
let module L = LogicalOperations in
let module G = Gdome in
let scratch_window = C.scratch_window () in
match scratch_window#sequent_viewer#get_selected_terms with
- [] ->
- C.output_html
- ("<h1 color=\"red\">No terms selected</h1>")
+ | [] -> HelmLogger.log (`Error (`T "No term selected"))
| terms ->
try
let expr = tactic terms scratch_window#term in
scratch_window#set_term expr ;
scratch_window#show () ;
with
- e ->
- C.output_html
- ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
+ e -> print_uncaught_exception e
let call_tactic_with_hypothesis_input tactic () =
let module L = LogicalOperations in
let module G = Gdome in
- let savedproof = !ProofEngine.proof in
+ let savedproof = ProofEngine.get_proof () in
let savedgoal = !ProofEngine.goal in
match (C.sequent_viewer ())#get_selected_hypotheses with
- [hypothesis] ->
- begin
- try
- tactic hypothesis ;
- C.refresh_goals () ;
- C.refresh_proof ()
- with
- RefreshSequentException e ->
- C.output_html
- ("<h1 color=\"red\">Exception raised during the refresh of " ^
- "the sequent: " ^ Printexc.to_string e ^ "</h1>") ;
- ProofEngine.proof := savedproof ;
- ProofEngine.goal := savedgoal ;
- C.refresh_goals ()
- | RefreshProofException e ->
- C.output_html
- ("<h1 color=\"red\">Exception raised during the refresh of " ^
- "the proof: " ^ Printexc.to_string e ^ "</h1>") ;
- ProofEngine.proof := savedproof ;
- ProofEngine.goal := savedgoal ;
- C.refresh_goals () ;
- C.refresh_proof ()
- | e ->
- C.output_html
- ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
- ProofEngine.proof := savedproof ;
- ProofEngine.goal := savedgoal ;
- end
- | [] ->
- C.output_html
- ("<h1 color=\"red\">No hypothesis selected</h1>")
- | _ ->
- C.output_html
- ("<h1 color=\"red\">Many hypothesis selected</h1>")
+ | [hypothesis] ->
+ handle_refresh_exception
+ (fun () ->
+ tactic hypothesis ;
+ C.refresh_goals () ;
+ C.refresh_proof ())
+ savedproof savedgoal
+ | [] -> HelmLogger.log (`Error (`T "No hypothesis selected"))
+ | _ -> HelmLogger.log (`Error (`T "Too many hypotheses selected"))
+
let intros =
(ProofEngine.intros ~mk_fresh_name_callback:C.mk_fresh_name_callback)
let exact = call_tactic_with_input ProofEngine.exact
let apply = call_tactic_with_input ProofEngine.apply
+ let auto = call_tactic (ProofEngine.auto ~dbd:C.dbd)
let elimintrossimpl = call_tactic_with_input ProofEngine.elim_intros_simpl
let elimtype = call_tactic_with_input ProofEngine.elim_type
let whd = call_tactic_with_goal_inputs ProofEngine.whd
projects / helm.git / blobdiff