From cf13b7adf17ce23342d8d5f26df6517aa222e21a Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 29 Jan 2003 13:20:55 +0000 Subject: [PATCH] 1. All the reduction tactics have been modified to reduce several (sub)terms at once. 2. To reduce several (sub)terms at once you can use the new multiple selection feature. --- helm/gTopLevel/gTopLevel.ml | 111 +++++++++++++++++++++++++++++++-- helm/gTopLevel/proofEngine.ml | 20 +++--- helm/gTopLevel/proofEngine.mli | 12 ++-- 3 files changed, 121 insertions(+), 22 deletions(-) diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index f00261d8e..5626600f7 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -1990,6 +1990,65 @@ let call_tactic_with_goal_input tactic () = ("

Many terms selected

") ;; +let call_tactic_with_goal_inputs tactic () = + let module L = LogicalOperations in + let module G = Gdome in + let notebook = (rendering_window ())#notebook in + let output = + ((rendering_window ())#output : GMathViewAux.single_selection_math_view) in + let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in + let savedproof = !ProofEngine.proof in + let savedgoal = !ProofEngine.goal in + try + let term_of_node 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 + match !current_goal_infos with + Some (ids_to_terms, ids_to_father_ids,_) -> + let id = xpath in + (Hashtbl.find ids_to_terms id) + | None -> assert false (* "ERROR: No current term!!!" *) + in + match notebook#proofw#get_selections with + [] -> + output_html outputhtml + ("

No term selected

") + | l -> + let terms = List.map term_of_node l in + match !current_goal_infos with + Some (ids_to_terms, ids_to_father_ids,_) -> + tactic terms ; + refresh_sequent notebook ; + refresh_proof output + | None -> assert false (* "ERROR: No current term!!!" *) + with + RefreshSequentException e -> + output_html outputhtml + ("

Exception raised during the refresh of the " ^ + "sequent: " ^ Printexc.to_string e ^ "

") ; + ProofEngine.proof := savedproof ; + ProofEngine.goal := savedgoal ; + refresh_sequent notebook + | RefreshProofException e -> + output_html outputhtml + ("

Exception raised during the refresh of the " ^ + "proof: " ^ Printexc.to_string e ^ "

") ; + ProofEngine.proof := savedproof ; + ProofEngine.goal := savedgoal ; + refresh_sequent notebook ; + refresh_proof output + | e -> + output_html outputhtml + ("

" ^ Printexc.to_string e ^ "

") ; + ProofEngine.proof := savedproof ; + ProofEngine.goal := savedgoal +;; + let call_tactic_with_input_and_goal_input tactic () = let module L = LogicalOperations in let module G = Gdome in @@ -2107,6 +2166,46 @@ let call_tactic_with_goal_input_in_scratch tactic scratch_window () = ("

Many terms selected

") ;; +let call_tactic_with_goal_inputs_in_scratch tactic scratch_window () = + let module L = LogicalOperations in + let module G = Gdome in + let mmlwidget = + (scratch_window#mmlwidget : GMathViewAux.multi_selection_math_view) in + let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in + let savedproof = !ProofEngine.proof in + let savedgoal = !ProofEngine.goal in + match mmlwidget#get_selections with + [] -> + output_html outputhtml + ("

No term selected

") + | l -> + 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 term_of_node 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 + 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 = mml_of_cic_term 111 expr in + scratch_window#show () ; + scratch_window#mmlwidget#load_doc ~dom:mml + | None -> assert false (* "ERROR: No current term!!!" *) + with + e -> + output_html outputhtml + ("

" ^ Printexc.to_string e ^ "

") +;; + let call_tactic_with_hypothesis_input tactic () = let module L = LogicalOperations in let module G = Gdome in @@ -2169,9 +2268,9 @@ let exact = call_tactic_with_input ProofEngine.exact;; let apply = call_tactic_with_input ProofEngine.apply;; 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_input ProofEngine.whd;; -let reduce = call_tactic_with_goal_input ProofEngine.reduce;; -let simpl = call_tactic_with_goal_input ProofEngine.simpl;; +let whd = call_tactic_with_goal_inputs ProofEngine.whd;; +let reduce = call_tactic_with_goal_inputs ProofEngine.reduce;; +let simpl = call_tactic_with_goal_inputs ProofEngine.simpl;; let fold_whd = call_tactic_with_input ProofEngine.fold_whd;; let fold_reduce = call_tactic_with_input ProofEngine.fold_reduce;; let fold_simpl = call_tactic_with_input ProofEngine.fold_simpl;; @@ -2201,15 +2300,15 @@ let decompose = (ProofEngine.decompose ~uris_choice_callback:decompose_uris_choice_callback);; let whd_in_scratch scratch_window = - call_tactic_with_goal_input_in_scratch ProofEngine.whd_in_scratch + call_tactic_with_goal_inputs_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 + call_tactic_with_goal_inputs_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 + call_tactic_with_goal_inputs_in_scratch ProofEngine.simpl_in_scratch scratch_window ;; diff --git a/helm/gTopLevel/proofEngine.ml b/helm/gTopLevel/proofEngine.ml index 99e6a081c..4751cb23f 100644 --- a/helm/gTopLevel/proofEngine.ml +++ b/helm/gTopLevel/proofEngine.ml @@ -116,7 +116,7 @@ let perforate context term ty = let irl = identity_relocation_list_for_metavariable context in (*CSC: Bug: se ci sono due term uguali nella prova dovrei bucarne uno solo!!!*) let bo' = - ProofEngineReduction.replace (==) term (C.Meta (newmeta,irl)) bo + ProofEngineReduction.replace (==) [term] [C.Meta (newmeta,irl)] bo in (* It may be possible that some metavariables occurred only in *) (* the term we are perforating and they now occurs no more. We *) @@ -137,7 +137,7 @@ let perforate context term ty = (************************************************************) (* Reduces [term] using [reduction_function] in the current scratch goal [ty] *) -let reduction_tactic_in_scratch reduction_function term ty = +let reduction_tactic_in_scratch reduction_function terms ty = let metasenv = match !proof with None -> [] @@ -148,9 +148,9 @@ let reduction_tactic_in_scratch reduction_function term ty = None -> assert false | Some metano -> List.find (function (m,_,_) -> m=metano) metasenv in - let term' = reduction_function context term in + let terms' = List.map (reduction_function context) terms in ProofEngineReduction.replace - ~equality:(==) ~what:term ~with_what:term' ~where:ty + ~equality:(==) ~what:terms ~with_what:terms' ~where:ty ;; let whd_in_scratch = reduction_tactic_in_scratch CicReduction.whd @@ -184,15 +184,15 @@ let clear hyp = apply_tactic (ProofEngineStructuralRules.clear ~hyp) (* reduction tactics *) -let whd term = +let whd terms = apply_tactic - (ReductionTactics.whd_tac ~also_in_hypotheses:true ~term:(Some term)) -let reduce term = + (ReductionTactics.whd_tac ~also_in_hypotheses:true ~terms:(Some terms)) +let reduce terms = apply_tactic - (ReductionTactics.reduce_tac ~also_in_hypotheses:true ~term:(Some term)) -let simpl term = + (ReductionTactics.reduce_tac ~also_in_hypotheses:true ~terms:(Some terms)) +let simpl terms = apply_tactic - (ReductionTactics.simpl_tac ~also_in_hypotheses:true ~term:(Some term)) + (ReductionTactics.simpl_tac ~also_in_hypotheses:true ~terms:(Some terms)) let fold_whd term = apply_tactic diff --git a/helm/gTopLevel/proofEngine.mli b/helm/gTopLevel/proofEngine.mli index c845c2b1e..8f8b1261d 100644 --- a/helm/gTopLevel/proofEngine.mli +++ b/helm/gTopLevel/proofEngine.mli @@ -31,17 +31,17 @@ val goal : ProofEngineTypes.goal option ref val perforate : Cic.context -> Cic.term -> Cic.term -> unit (* reduction tactics *) -val whd : Cic.term -> unit -val reduce : Cic.term -> unit -val simpl : Cic.term -> unit +val whd : Cic.term list -> unit +val reduce : Cic.term list -> unit +val simpl : Cic.term list -> unit val fold_whd : Cic.term -> unit val fold_reduce : Cic.term -> unit val fold_simpl : Cic.term -> unit (* scratch area reduction tactics *) -val whd_in_scratch : Cic.term -> Cic.term -> Cic.term -val reduce_in_scratch : Cic.term -> Cic.term -> Cic.term -val simpl_in_scratch : Cic.term -> Cic.term -> Cic.term +val whd_in_scratch : Cic.term list -> Cic.term -> Cic.term +val reduce_in_scratch : Cic.term list -> Cic.term -> Cic.term +val simpl_in_scratch : Cic.term list -> Cic.term -> Cic.term (* "primitive" tactics *) val can_apply : Cic.term -> bool -- 2.39.2