(* Copyright (C) 2002, HELM Team. * * This file is part of HELM, an Hypertextual, Electronic * Library of Mathematics, developed at the Computer Science * Department, University of Bologna, Italy. * * HELM is free software; you can redistribute it and/or * modify it under the terms of the GNU General Public License * as published by the Free Software Foundation; either version 2 * of the License, or (at your option) any later version. * * HELM is distributed in the hope that it will be useful, * but WITHOUT ANY WARRANTY; without even the implied warranty of * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the * GNU General Public License for more details. * * You should have received a copy of the GNU General Public License * along with HELM; if not, write to the Free Software * Foundation, Inc., 59 Temple Place - Suite 330, Boston, * MA 02111-1307, USA. * * For details, see the HELM World-Wide-Web page, * 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 = let (proof, goal) = status in let module C = Cic in let module R = CicReduction in let module P = PrimitiveTactics in let module T = Tacticals in let module S = ProofEngineStructuralRules in let module U = UriManager in let (_,metasenv,_,_) = proof in let _,context,ty = CicUtil.lookup_meta goal metasenv in let termty = CicTypeChecker.type_of_aux' metasenv context term in (* per ora non serve *) T.then_ ~start:(T.repeat_tactic ~tactic:(T.then_ ~start:(VariousTactics.generalize_tac ~term) (* chissa' se cosi' funziona? *) ~continuation:(P.intros)) ~continuation:(P.elim_intros_simpl ~term) status ;; *) let elim_type_tac ~term = let elim_type_tac ~term status = let module C = Cic in let module P = PrimitiveTactics in let module T = Tacticals in ProofEngineTypes.apply_tactic (T.thens ~start: (P.cut_tac term) ~continuations:[ P.elim_intros_simpl_tac ~term:(C.Rel 1) ; T.id_tac ]) status in ProofEngineTypes.mk_tactic (elim_type_tac ~term) ;; (* Decompose related stuff *) 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' = try (* Constant *) if String.sub uri' (String.length uri' - 4) 4 = ".con" then CicTextualParser0.ConUri (UriManager.uri_of_string uri') else if String.sub uri' (String.length uri' - 4) 4 = ".var" then CicTextualParser0.VarUri (UriManager.uri_of_string uri') else (try (* Inductive Type *) let uri'',typeno = CicTextualLexer.indtyuri_of_uri uri' in CicTextualParser0.IndTyUri (uri'',typeno) with _ -> (* Constructor of an Inductive Type *) let uri'',typeno,consno = CicTextualLexer.indconuri_of_uri uri' in CicTextualParser0.IndConUri (uri'',typeno,consno) ) with _ -> 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.: 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 = let decompose_tac uris_choice_callback term status = let (proof, goal) = status in let module C = Cic in let module R = CicReduction in let module P = PrimitiveTactics in let module T = Tacticals in let module S = ProofEngineStructuralRules in let _,metasenv,_,_ = proof in let _,context,ty = CicUtil.lookup_meta goal metasenv in let old_context_len = List.length context in let termty = CicTypeChecker.type_of_aux' metasenv context term in let rec make_list termty = (* 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 (C.MutInd (uri,typeno,exp_named_subst)) (* when (not (List.mem (uri,typeno,exp_named_subst) urilist)) *) -> (uri,typeno,exp_named_subst)::urilist | (C.Appl ((C.MutInd (uri,typeno,exp_named_subst))::applist)) (* when (not (List.mem (uri,typeno,exp_named_subst) urilist)) *) -> (uri,typeno,exp_named_subst)::(List.fold_left search_inductive_types urilist applist) | _ -> urilist (* N.B: in un caso tipo (and A !C:Prop.(or B C)) l'or *non* viene selezionato! *) in let rec purge_duplicates urilist = let rec aux triple urilist = match urilist with [] -> [] | hd::tl -> if (hd = triple) then aux triple tl else hd::(aux triple tl) in match urilist with [] -> [] | hd::tl -> hd::(purge_duplicates (aux hd tl)) in purge_duplicates (search_inductive_types [] termty) in 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 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 = let (proof, goal) = status in 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,_ = CicUtil.lookup_meta goal metasenv in let old_context_len = List.length context in let termty = CicTypeChecker.type_of_aux' metasenv context term' in 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) -> warn ("elim " ^ CicPp.ppterm termty); ProofEngineTypes.apply_tactic (T.then_ ~start:(P.elim_intros_simpl_tac ~term:term') ~continuation:( (* clear the hyp that has just been eliminated *) ProofEngineTypes.mk_tactic (fun status -> let (proof, goal) = status in let _,metasenv,_,_ = proof in let _,context,_ = CicUtil.lookup_meta goal metasenv in let new_context_len = List.length context in 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 ProofEngineTypes.apply_tactic (T.then_ ~start:( 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:(ProofEngineTypes.mk_tactic (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 ))) status | _ -> let new_nr_of_hyp_still_to_elim = nr_of_hyp_still_to_elim - 1 in 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 (* no hyp to elim left in this goal *) ProofEngineTypes.apply_tactic T.id_tac status in elim_clear_tac ~term':term ~nr_of_hyp_still_to_elim:1 status in ProofEngineTypes.mk_tactic (decompose_tac uris_choice_callback term) ;;