Decompose now has a new parameter that is the callback function to call

to select the uris that must be decomposed.

diff --git a/helm/ocaml/tactics/eliminationTactics.ml b/helm/ocaml/tactics/eliminationTactics.ml
index fc6906cbc9c9662e655c3ba324b008747ed47949..ae947f5ec4bd35759702588c95790410d10d07ee 100644 (file)
--- a/helm/ocaml/tactics/eliminationTactics.ml
+++ b/helm/ocaml/tactics/eliminationTactics.ml
@@ -69,16 +69,6 @@ lista e ritornando la lista di termini che l'utente vuole decomporre;
 decomporre. *)
 
 
-exception InteractiveUserUriChoiceNotRegistered
-
-let interactive_user_uri_choice =
- (ref (fun ~selection_mode -> raise InteractiveUserUriChoiceNotRegistered) :
-  (selection_mode:[`SINGLE | `EXTENDED] ->
-      ?ok:string ->
-      ?enable_button_for_non_vars:bool ->
-      title:string -> msg:string -> string list -> string list) ref)
-;;
-
 exception IllFormedUri of string
 
 let cic_textual_parser_uri_of_string uri' =
@@ -106,28 +96,7 @@ let cic_textual_parser_uri_of_string uri' =
   _ -> raise (IllFormedUri uri')
 ;;
 
-let constructor_uri_of_string uri = 
-  match cic_textual_parser_uri_of_string uri with
-     CicTextualParser0.IndTyUri (uri,typeno) -> (uri,typeno,[])
-   | _ -> assert false
-;;
-
-let call_back uris = 
-(* N.B.: in questo passaggio perdo l'informazione su exp_named_subst !!!! *)
-  let module U = UriManager in 
-   List.map 
-    (constructor_uri_of_string)
-    (!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)
-    ) 
-;;
-
-
-let decompose_tac ~term ~status:((proof,goal) as status) =
+let decompose_tac ~term ~uris_choice_callback ~status:((proof,goal) as status) =
   let module C = Cic in
   let module R = CicReduction in
   let module P = PrimitiveTactics in
@@ -169,8 +138,8 @@ let decompose_tac ~term ~status:((proof,goal) as status) =
 
        let urilist =  
           (* list of triples (uri,typeno,exp_named_subst) of Inductive Types found in term and chosen by the user *)
-          (* N.B.: due to a bug in call_back exp_named_subst are not significant (they all are []) *)
-         call_back (make_list termty) in
+          (* N.B.: due to a bug in uris_choice_callback exp_named_subst are not significant (they all are []) *)
+         uris_choice_callback (make_list termty) in
 
         let rec elim_clear_tac ~term' ~nr_of_hyp_still_to_elim ~status:((proof,goal) as status) =
 prerr_endline ("%%%%%%% nr_of_hyp_still_to_elim=" ^ (string_of_int nr_of_hyp_still_to_elim));

diff --git a/helm/ocaml/tactics/eliminationTactics.mli b/helm/ocaml/tactics/eliminationTactics.mli
index a49c771585dee99989e0a910f64869c18b742d28..5e132c4966366860cad1e3cefa44b881e7aa1c2b 100644 (file)
--- a/helm/ocaml/tactics/eliminationTactics.mli
+++ b/helm/ocaml/tactics/eliminationTactics.mli
@@ -25,9 +25,9 @@
 
 val elim_type_tac: term:Cic.term -> ProofEngineTypes.tactic
 
-val interactive_user_uri_choice: ( selection_mode:[`SINGLE | `EXTENDED] ->
-      ?ok:string ->
-      ?enable_button_for_non_vars:bool ->
-      title:string -> msg:string -> string list -> string list) ref
-
-val decompose_tac: term:Cic.term -> ProofEngineTypes.tactic
+val decompose_tac:
+ term:Cic.term ->
+ uris_choice_callback:
+  ((UriManager.uri * int * (UriManager.uri * Cic.term) list) list ->
+   (UriManager.uri * int * (UriManager.uri * Cic.term) list) list) ->
+   ProofEngineTypes.tactic