From c5ff3bf7bda01b5194e502aef5e9e47a49ecf1ad Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Thu, 20 Feb 2003 17:24:43 +0000 Subject: [PATCH] - added HBugs notification after tactic application - bugfix: removed some useless status save - defined module type "Tactics", module type returned by Make functor --- helm/gTopLevel/invokeTactics.ml | 73 ++++++++++++++++++++++++++------ helm/gTopLevel/invokeTactics.mli | 38 +++++++++-------- 2 files changed, 82 insertions(+), 29 deletions(-) diff --git a/helm/gTopLevel/invokeTactics.ml b/helm/gTopLevel/invokeTactics.ml index 96f306cdf..775d6a468 100644 --- a/helm/gTopLevel/invokeTactics.ml +++ b/helm/gTopLevel/invokeTactics.ml @@ -62,10 +62,54 @@ module type Callbacks = (UriManager.uri * int * 'b list) list val mk_fresh_name_callback : Cic.context -> Cic.name -> typ:Cic.term -> Cic.name + (* 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 () = @@ -75,7 +119,8 @@ module Make(C:Callbacks) = try tactic () ; C.refresh_goals () ; - C.refresh_proof () + C.refresh_proof () ; + C.notify_hbugs () with RefreshSequentException e -> C.output_html @@ -99,7 +144,7 @@ module Make(C:Callbacks) = 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 = @@ -118,13 +163,17 @@ module Make(C:Callbacks) = 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 @@ -158,7 +207,8 @@ module Make(C:Callbacks) = try tactic term ; C.refresh_goals () ; - C.refresh_proof () + C.refresh_proof () ; + C.notify_hbugs () with RefreshSequentException e -> C.output_html @@ -201,7 +251,8 @@ module Make(C:Callbacks) = | terms -> tactic terms ; C.refresh_goals () ; - C.refresh_proof () + C.refresh_proof () ; + C.notify_hbugs () with RefreshSequentException e -> C.output_html @@ -253,7 +304,8 @@ module Make(C:Callbacks) = 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 @@ -286,8 +338,6 @@ module Make(C:Callbacks) = let call_tactic_with_goal_input_in_scratch tactic () = let module L = LogicalOperations in let module G = Gdome in - let savedproof = !ProofEngine.proof in - let savedgoal = !ProofEngine.goal in let scratch_window = C.scratch_window () in match scratch_window#sequent_viewer#get_selected_terms with [term] -> @@ -314,8 +364,6 @@ module Make(C:Callbacks) = let module L = LogicalOperations in let module G = Gdome in let scratch_window = C.scratch_window () in - let savedproof = !ProofEngine.proof in - let savedgoal = !ProofEngine.goal in match scratch_window#sequent_viewer#get_selected_terms with [] -> C.output_html @@ -343,7 +391,8 @@ module Make(C:Callbacks) = try tactic hypothesis ; C.refresh_goals () ; - C.refresh_proof () + C.refresh_proof () ; + C.notify_hbugs () with RefreshSequentException e -> C.output_html diff --git a/helm/gTopLevel/invokeTactics.mli b/helm/gTopLevel/invokeTactics.mli index 313991ced..11b8ecf72 100644 --- a/helm/gTopLevel/invokeTactics.mli +++ b/helm/gTopLevel/invokeTactics.mli @@ -62,46 +62,50 @@ module type Callbacks = (UriManager.uri * int * 'b list) list val mk_fresh_name_callback : Cic.context -> Cic.name -> typ:Cic.term -> Cic.name + val notify_hbugs : unit -> unit end -module Make (C : Callbacks) : +module type Tactics = sig val intros : unit -> unit - val exact : unit -> unit - val apply : unit -> unit - val elimintrossimpl : unit -> unit - val elimtype : 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 : unit -> unit - val fold_reduce : unit -> unit - val fold_simpl : unit -> unit - val cut : 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 : 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 : unit -> unit - val rewritebacksimpl : 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 : 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 : unit -> unit + val absurd : ?term:string -> unit -> unit val contradiction : unit -> unit - val decompose : unit -> unit - val injection : unit -> unit - val discriminate : 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 + -- 2.39.2