Decompose now has a new parameter which is the callback to call to select the

uris that must be used for the decomposition.

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 9d1b3e982969625da635f395361938b5f5be9500..396c968fd99e170eb100854f0bd3c0f341bc41bd 100644 (file)
--- 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 () =
       ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
 ;;
 
+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 379007021595618f5edaec3142fe9638918aed9c..e333ec3b8ec9e5d741a2c856164ddfbbe0c32f66 100644 (file)
--- 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 0263fd1e7c31e8e07fb5bc23335905fb051ba1cd..deb8483ac0348e7b3cc31ea85e858edb79b4968b 100644 (file)
--- 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