module type Callbacks =
sig
+ (* input widgets *)
val sequent_viewer : unit -> TermViewer.sequent_viewer
val term_editor : unit -> TermEditor.term_editor
- val get_current_scratch_infos :
+ val scratch_window :
unit ->
- (Cic.term *
- (Cic.id, Cic.term) Hashtbl.t *
- (Cic.id, Cic.id option) Hashtbl.t *
- (string, Cic.hypothesis) Hashtbl.t
- ) option
- val set_current_scratch_infos :
- (Cic.term *
- (Cic.id, Cic.term) Hashtbl.t *
- (Cic.id, Cic.id option) Hashtbl.t *
- (string, Cic.hypothesis) Hashtbl.t
- ) option -> unit
+ < sequent_viewer: TermViewer.sequent_viewer ;
+ show: unit -> unit ;
+ term: Cic.term ;
+ set_term : Cic.term -> unit ;
+ metasenv: Cic.metasenv ;
+ 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
+ (* callbacks for user-tactics interaction *)
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 output_html : string -> unit
+ (* invoked when the proof assistant's status has changed to notify Hbugs *)
+ val notify_hbugs : unit -> unit
end
;;
-module Make(C:Callbacks) =
+module type Tactics =
+ sig
+ val intros : unit -> unit
+ val exact : ?term:string -> unit -> unit
+ val apply : ?term:string -> unit -> unit
+ val elimintrossimpl : ?term:string -> unit -> unit
+ val elimtype : ?term:string -> unit -> unit
+ val whd : unit -> unit
+ val reduce : unit -> unit
+ val simpl : unit -> unit
+ val fold_whd : ?term:string -> unit -> unit
+ val fold_reduce : ?term:string -> unit -> unit
+ val fold_simpl : ?term:string -> unit -> unit
+ val cut : ?term:string -> unit -> unit
+ val change : unit -> unit
+ val letin : ?term:string -> unit -> unit
+ val ring : unit -> unit
+ val clearbody : unit -> unit
+ val clear : unit -> unit
+ val fourier : unit -> unit
+ val rewritesimpl : ?term:string -> unit -> unit
+ val rewritebacksimpl : ?term:string -> unit -> unit
+ val replace : unit -> unit
+ val reflexivity : unit -> unit
+ val symmetry : unit -> unit
+ val transitivity : ?term:string -> unit -> unit
+ val exists : unit -> unit
+ val split : unit -> unit
+ val left : unit -> unit
+ val right : unit -> unit
+ val assumption : unit -> unit
+ val generalize : unit -> unit
+ val absurd : ?term:string -> unit -> unit
+ val contradiction : unit -> unit
+ val decompose : ?term:string -> unit -> unit
+ val injection : ?term:string -> unit -> unit
+ val discriminate : ?term:string -> unit -> unit
+ val whd_in_scratch : unit -> unit
+ val reduce_in_scratch : unit -> unit
+ val simpl_in_scratch : unit -> unit
+ end
+
+module Make (C: Callbacks) : Tactics =
struct
let call_tactic tactic () =
try
tactic () ;
C.refresh_goals () ;
- C.refresh_proof ()
+ C.refresh_proof () ;
+ C.notify_hbugs ()
with
RefreshSequentException e ->
C.output_html
ProofEngine.goal := savedgoal
end
- let call_tactic_with_input tactic () =
+ let call_tactic_with_input tactic ?term () =
let savedproof = !ProofEngine.proof in
let savedgoal = !ProofEngine.goal in
let uri,metasenv,bo,ty =
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
+ (C.term_editor ())#reset ;
+ C.notify_hbugs ()
with
RefreshSequentException e ->
C.output_html
try
tactic term ;
C.refresh_goals () ;
- C.refresh_proof ()
+ C.refresh_proof () ;
+ C.notify_hbugs ()
with
RefreshSequentException e ->
C.output_html
| terms ->
tactic terms ;
C.refresh_goals () ;
- C.refresh_proof ()
+ C.refresh_proof () ;
+ C.notify_hbugs ()
with
RefreshSequentException e ->
C.output_html
tactic ~goal_input:term ~input:expr ;
C.refresh_goals () ;
C.refresh_proof () ;
- (C.term_editor ())#reset
+ (C.term_editor ())#reset ;
+ C.notify_hbugs ()
with
RefreshSequentException e ->
C.output_html
C.output_html
("<h1 color=\"red\">Many terms selected</h1>")
- let call_tactic_with_goal_input_in_scratch tactic scratch_window () =
+ let call_tactic_with_goal_input_in_scratch tactic () =
let module L = LogicalOperations in
let module G = Gdome in
- let mmlwidget =
- (scratch_window#mmlwidget : GMathViewAux.multi_selection_math_view) in
- let savedproof = !ProofEngine.proof in
- let savedgoal = !ProofEngine.goal in
- match mmlwidget#get_selections with
- [node] ->
- let xpath =
- ((node : Gdome.element)#getAttributeNS
- ~namespaceURI:Misc.helmns
- ~localName:(G.domString "xref"))#to_string
- in
- if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
- else
- begin
- try
- match C.get_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,scratch_infos =
- ApplyStylesheets.mml_of_cic_term 111 expr
- in
- C.set_current_scratch_infos (Some scratch_infos) ;
- scratch_window#show () ;
- scratch_window#mmlwidget#load_doc ~dom:mml
- | None -> assert false (* "ERROR: No current term!!!" *)
- with
- e ->
- C.output_html
- ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
- end
+ let scratch_window = C.scratch_window () in
+ match scratch_window#sequent_viewer#get_selected_terms with
+ [term] ->
+ begin
+ try
+ let expr = tactic term scratch_window#term in
+ scratch_window#sequent_viewer#load_sequent
+ scratch_window#metasenv (111,scratch_window#context,expr) ;
+ scratch_window#set_term expr ;
+ scratch_window#show () ;
+ with
+ e ->
+ C.output_html
+ ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
+ end
| [] ->
C.output_html
("<h1 color=\"red\">No term selected</h1>")
C.output_html
("<h1 color=\"red\">Many terms selected</h1>")
- let call_tactic_with_goal_inputs_in_scratch tactic scratch_window () =
+ let call_tactic_with_goal_inputs_in_scratch tactic () =
let module L = LogicalOperations in
let module G = Gdome in
- let mmlwidget =
- (scratch_window#mmlwidget : GMathViewAux.multi_selection_math_view) in
- let savedproof = !ProofEngine.proof in
- let savedgoal = !ProofEngine.goal in
- match mmlwidget#get_selections with
+ let scratch_window = C.scratch_window () in
+ match scratch_window#sequent_viewer#get_selected_terms with
[] ->
C.output_html
- ("<h1 color=\"red\">No term selected</h1>")
- | l ->
+ ("<h1 color=\"red\">No terms selected</h1>")
+ | terms ->
try
- match C.get_current_scratch_infos () with
- (* term is the whole goal in the scratch_area *)
- Some (term,ids_to_terms, ids_to_father_ids,_) ->
- let term_of_node node =
- let xpath =
- ((node : Gdome.element)#getAttributeNS
- ~namespaceURI:Misc.helmns
- ~localName:(G.domString "xref"))#to_string
- in
- if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
- else
- let id = xpath in
- Hashtbl.find ids_to_terms id
- in
- let terms = List.map term_of_node l in
- let expr = tactic terms term in
- let mml,scratch_infos =
- ApplyStylesheets.mml_of_cic_term 111 expr
- in
- C.set_current_scratch_infos (Some scratch_infos) ;
- scratch_window#show () ;
- scratch_window#mmlwidget#load_doc ~dom:mml
- | None -> assert false (* "ERROR: No current term!!!" *)
+ let expr = tactic terms scratch_window#term in
+ scratch_window#sequent_viewer#load_sequent
+ scratch_window#metasenv (111,scratch_window#context,expr) ;
+ scratch_window#set_term expr ;
+ scratch_window#show () ;
with
e ->
C.output_html
try
tactic hypothesis ;
C.refresh_goals () ;
- C.refresh_proof ()
+ C.refresh_proof () ;
+ C.notify_hbugs ()
with
RefreshSequentException e ->
C.output_html
let left = call_tactic ProofEngine.left
let right = call_tactic ProofEngine.right
let assumption = call_tactic ProofEngine.assumption
+ let injection = call_tactic_with_input ProofEngine.injection
+ let discriminate = call_tactic_with_input ProofEngine.discriminate
let generalize =
call_tactic_with_goal_inputs
(ProofEngine.generalize ~mk_fresh_name_callback:C.mk_fresh_name_callback)
call_tactic_with_input
(ProofEngine.decompose
~uris_choice_callback:C.decompose_uris_choice_callback)
- let whd_in_scratch scratch_window =
+ let whd_in_scratch =
call_tactic_with_goal_inputs_in_scratch ProofEngine.whd_in_scratch
- scratch_window
- let reduce_in_scratch scratch_window =
+ let reduce_in_scratch =
call_tactic_with_goal_inputs_in_scratch ProofEngine.reduce_in_scratch
- scratch_window
- let simpl_in_scratch scratch_window =
+ let simpl_in_scratch =
call_tactic_with_goal_inputs_in_scratch ProofEngine.simpl_in_scratch
- scratch_window
end
;;
projects / helm.git / blobdiff