From 948156df0a5071924ba2a2b6090596ceb0cba74f Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 28 Jan 2003 18:38:45 +0000 Subject: [PATCH] Decompose now has a new parameter which is the callback to call to select the uris that must be used for the decomposition. --- helm/gTopLevel/gTopLevel.ml | 24 ++++++++++++++++++++---- helm/gTopLevel/proofEngine.ml | 3 ++- helm/gTopLevel/proofEngine.mli | 6 +++++- 3 files changed, 27 insertions(+), 6 deletions(-) diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index 9d1b3e982..396c968fd 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -352,9 +352,6 @@ let raise NoChoice ;; -EliminationTactics.interactive_user_uri_choice := - (fun ~selection_mode -> interactive_user_uri_choice ~selection_mode:selection_mode);; - let interactive_interpretation_choice interpretations = let chosen = ref None in let window = @@ -1814,6 +1811,23 @@ let check scratch_window () = ("

" ^ Printexc.to_string e ^ "

") ; ;; +let decompose_uris_choice_callback uris = +(* N.B.: in questo passaggio perdo l'informazione su exp_named_subst !!!! *) + let module U = UriManager in + List.map + (function uri -> + match Disambiguate.cic_textual_parser_uri_of_string uri with + CicTextualParser0.IndTyUri (uri,typeno) -> (uri,typeno,[]) + | _ -> assert false) + (interactive_user_uri_choice + ~selection_mode:`EXTENDED ~ok:"Ok" ~enable_button_for_non_vars:false + ~title:"Decompose" ~msg:"Please, select the Inductive Types to decompose" + (List.map + (function (uri,typeno,_) -> + U.string_of_uri uri ^ "#1/" ^ string_of_int (typeno+1) + ) uris) + ) +;; (***********************) (* TACTICS *) @@ -2156,7 +2170,9 @@ let assumption = call_tactic ProofEngine.assumption;; let generalize = call_tactic_with_goal_input ProofEngine.generalize;; let absurd = call_tactic_with_input ProofEngine.absurd;; let contradiction = call_tactic ProofEngine.contradiction;; -let decompose = call_tactic_with_input ProofEngine.decompose;; +let decompose = + call_tactic_with_input + (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 diff --git a/helm/gTopLevel/proofEngine.ml b/helm/gTopLevel/proofEngine.ml index 379007021..e333ec3b8 100644 --- a/helm/gTopLevel/proofEngine.ml +++ b/helm/gTopLevel/proofEngine.ml @@ -231,7 +231,8 @@ let generalize term = apply_tactic (VariousTactics.generalize_tac ~term) let absurd term = apply_tactic (NegationTactics.absurd_tac ~term) let contradiction () = apply_tactic NegationTactics.contradiction_tac -let decompose term = apply_tactic (EliminationTactics.decompose_tac ~term) +let decompose ~uris_choice_callback term = + apply_tactic (EliminationTactics.decompose_tac ~term ~uris_choice_callback) (* let decide_equality () = apply_tactic VariousTactics.decide_equality_tac diff --git a/helm/gTopLevel/proofEngine.mli b/helm/gTopLevel/proofEngine.mli index 0263fd1e7..deb8483ac 100644 --- a/helm/gTopLevel/proofEngine.mli +++ b/helm/gTopLevel/proofEngine.mli @@ -81,7 +81,11 @@ val generalize : Cic.term -> unit val absurd : Cic.term -> unit val contradiction : unit -> unit -val decompose : Cic.term -> unit +val decompose : + uris_choice_callback: + ((UriManager.uri * int * (UriManager.uri * Cic.term) list) list -> + (UriManager.uri * int * (UriManager.uri * Cic.term) list) list) -> + Cic.term -> unit (* val decide_equality : unit -> unit -- 2.39.2