* http://cs.unibo.it/helm/.
*)
+(** DEBUGGING *)
+
+ (** perform debugging output? *)
+let debug = false
+
+ (** debugging print *)
+let warn s =
+ if debug then
+ prerr_endline ("DECOMPOSE: " ^ s)
+
+
+
(*
let induction_tac ~term ~status:((proof,goal) as status) =
let module C = Cic in
~status
;;
-(* Questa era gia' in ring.ml!!!! NB: adesso in ring non c'e' piu' :-)
-let elim_type_tac ~term ~status =
- warn "in Ring.elim_type_tac";
- Tacticals.thens ~start:(cut_tac ~term)
- ~continuations:[elim_simpl_intros_tac ~term:(Cic.Rel 1) ; Tacticals.id_tac] ~status
-*)
+(* Decompose related stuff *)
-(* PROVE DI DECOMPOSE *)
-(* guardare quali sono i tipi induttivi decomponibili presenti in
-profondita' nel term; chiamare una funzione di call-back passando questa
-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
_ -> raise (IllFormedUri uri')
;;
-let decompose_tac ?(uris_choice_callback=(function l -> l)) term
- ~status:((proof,goal) as status)
-=
+(*
+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.: nella finestra c'e' un campo "nessuno deei precedenti, prova questo" che non ha senso? *)
+(* N.B.: in questo passaggio perdo l'informazione su exp_named_subst !!!! *)
+(* domanda: due triple possono essere diverse solo per avere exp_named_subst diverse?? *)
+ 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 ?(uris_choice_callback=(function l -> l)) term ~status:((proof,goal) as status) =
let module C = Cic in
let module R = CicReduction in
let module P = PrimitiveTactics in
let _,metasenv,_,_ = proof in
let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
let old_context_len = List.length context in
-(* let nr_of_hyp_still_to_elim = ref 1 in *)
let termty = CicTypeChecker.type_of_aux' metasenv context term in
let rec make_list termty =
-(* altamente inefficente? *)
+ (* N.B.: altamente inefficente? *)
let rec search_inductive_types urilist termty =
(* search in term the Inductive Types and return a list of uris as triples like this: (uri,typeno,exp_named_subst) *)
match termty with
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));
+ warn ("nr_of_hyp_still_to_elim=" ^ (string_of_int nr_of_hyp_still_to_elim));
if nr_of_hyp_still_to_elim <> 0 then
let _,metasenv,_,_ = proof in
let _,context,_ = List.find (function (m,_,_) -> m=goal) metasenv in
let old_context_len = List.length context in
let termty = CicTypeChecker.type_of_aux' metasenv context term' in
-prerr_endline ("%%%%%%% elim_clear termty= " ^ CicPp.ppterm termty);
+ warn ("elim_clear termty= " ^ CicPp.ppterm termty);
match termty with
C.MutInd (uri,typeno,exp_named_subst)
| C.Appl((C.MutInd (uri,typeno,exp_named_subst))::_)
when (List.mem (uri,typeno,exp_named_subst) urilist) ->
-prerr_endline ("%%%%%%% elim " ^ CicPp.ppterm termty);
+ warn ("elim " ^ CicPp.ppterm termty);
T.then_
~start:(P.elim_intros_simpl_tac ~term:term')
~continuation:(
let _,metasenv,_,_ = proof in
let _,context,_ = List.find (function (m,_,_) -> m=goal) metasenv in
let new_context_len = List.length context in
-prerr_endline ("%%%%%%% newcon=" ^ (string_of_int new_context_len) ^ " & oldcon=" ^ (string_of_int old_context_len) ^ " & old_nr_of_hyp=" ^ (string_of_int nr_of_hyp_still_to_elim));
+ warn ("newcon=" ^ (string_of_int new_context_len) ^ " & oldcon=" ^ (string_of_int old_context_len) ^ " & old_nr_of_hyp=" ^ (string_of_int nr_of_hyp_still_to_elim));
let new_nr_of_hyp_still_to_elim = nr_of_hyp_still_to_elim + (new_context_len - old_context_len) - 1 in
T.then_
~start:(
- if (term'==term) (* this is the first application of elim: there's no need to clear the hyp *)
+ if (term'==term) (* if it's the first application of elim, there's no need to clear the hyp *)
then begin prerr_endline ("%%%%%%% no clear"); T.id_tac end
else begin prerr_endline ("%%%%%%% clear " ^ (string_of_int (new_nr_of_hyp_still_to_elim))); (S.clear ~hyp:(List.nth context (new_nr_of_hyp_still_to_elim))) end)
~continuation:(elim_clear_tac ~term':(C.Rel new_nr_of_hyp_still_to_elim) ~nr_of_hyp_still_to_elim:new_nr_of_hyp_still_to_elim)
~status
| _ ->
let new_nr_of_hyp_still_to_elim = nr_of_hyp_still_to_elim - 1 in
-prerr_endline ("%%%%%%% fail; hyp=" ^ (string_of_int new_nr_of_hyp_still_to_elim));
+ warn ("fail; hyp=" ^ (string_of_int new_nr_of_hyp_still_to_elim));
elim_clear_tac ~term':(C.Rel new_nr_of_hyp_still_to_elim) ~nr_of_hyp_still_to_elim:new_nr_of_hyp_still_to_elim ~status
- else (* raise (ProofEngineTypes.Fail "Decomopse: finished decomposing"); *) T.id_tac ~status
+ else (* no hyp to elim left in this goal *)
+ T.id_tac ~status
in
-(* T.repeat_tactic ~tactic: *)
- (elim_clear_tac ~term':term ~nr_of_hyp_still_to_elim:1)
- ~status
+ elim_clear_tac ~term':term ~nr_of_hyp_still_to_elim:1 ~status
;;
-
projects / helm.git / blobdiff