(* 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/. *) (* TODO se ce n'e' piu' di una, prende la prima che trova... sarebbe meglio chiedere *) let assumption_tac ~status:((proof,goal) as status) = let module C = Cic in let module R = CicReduction in let module S = CicSubstitution in let _,metasenv,_,_ = proof in let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in let rec find n = function hd::tl -> (match hd with (Some (_, C.Decl t)) when (R.are_convertible context (S.lift n t) ty) -> n | (Some (_, C.Def t)) when (R.are_convertible context (CicTypeChecker.type_of_aux' metasenv context (S.lift n t)) ty) -> n | _ -> find (n+1) tl ) | [] -> raise (ProofEngineTypes.Fail "Assumption: No such assumption") in PrimitiveTactics.apply_tac ~status ~term:(C.Rel (find 1 context)) ;; (* Questa invece era in fourierR.ml let assumption_tac ~status:(proof,goal)= let curi,metasenv,pbo,pty = proof in let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in let num = ref 0 in let tac_list = List.map ( fun x -> num := !num + 1; match x with Some(Cic.Name(nm),t) -> (nm,exact ~term:(Cic.Rel(!num))) | _ -> ("fake",tcl_fail 1) ) context in Tacticals.try_tactics ~tactics:tac_list ~status:(proof,goal) ;; *) (* ANCORA DA DEBUGGARE *) (* IN FASE DI IMPLEMENTAZIONE *) let generalize_tac ~term ~status:((proof,goal) as status) = let module C = Cic in let module P = PrimitiveTactics in let module T = Tacticals in let _,metasenv,_,_ = proof in let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in (* let uno = (C.Appl [ C.MutConstruct (UriManager.uri_of_string "cic:/Coq/Init/Datatypes/nat.ind", 0, 2, []) ; C.MutConstruct (UriManager.uri_of_string "cic:/Coq/Init/Datatypes/nat.ind", 0, 1, [])]) in let tuno = CicTypeChecker.type_of_aux' metasenv context uno in prerr_endline ("#### uno: " ^ CicPp.ppterm uno); prerr_endline ("#### tuno: " ^ CicPp.ppterm tuno); *) prerr_endline ("#### dummy: " ^ (CicPp.ppterm (CicTypeChecker.type_of_aux' metasenv context term))); prerr_endline ("#### with_what: " ^ CicPp.ppterm (C.Rel 1)); prerr_endline ("#### term: " ^ CicPp.ppterm term); prerr_endline ("#### ty: " ^ CicPp.ppterm ty); T.thens ~start:(P.cut_tac ~term:( C.Prod ( (C.Name "dummy_for_gen"), (CicTypeChecker.type_of_aux' metasenv context term), (ProofEngineReduction.replace_lifting ~equality:(==) ~with_what:(C.Rel 1) (* C.Name "dummy_for_gen" *) ~what:term ~where:ty)))) ~continuations: [T.id_tac ; (P.apply_tac ~term:(C.Appl [(C.Rel 1); term]))] (* in quest'ordine o viceversa? provare *) (* [(P.apply_tac ~term:(C.Appl [(C.Rel 1); term])) ; T.id_tac] (* in quest'ordine o viceversa? provare *)*) ~status ;; (* let generalize_tac ~term ~status:((proof,goal) as status) = let module C = Cic in let module H = ProofEngineHelpers in let module P = PrimitiveTactics in let module T = Tacticals in let _,metasenv,_,_ = proof in let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in let add_decl_tac ~term ~status:(proof, goal) = let module C = Cic in let curi,metasenv,pbo,pty = proof in let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in let _ = CicTypeChecker.type_of_aux' metasenv context term in let newmeta = H.new_meta ~proof in let context_for_newmeta = (Some (C.Name "dummy_for_gen",C.Decl term))::context in let irl = H.identity_relocation_list_for_metavariable context_for_newmeta in let newmetaty = CicSubstitution.lift 1 ty in let bo' = C.LetIn (C.Name "dummy_for_gen" , term , C.Meta (newmeta,irl)) in let (newproof, _) = H.subst_meta_in_proof proof metano bo'[newmeta,context_for_newmeta,newmetaty] in (newproof, [newmeta]) in T.then_ ~start:(add_decl_tac ~term:(CicTypeChecker.type_of_aux' metasenv context term)) ~continuation:( T.id_tac) (* T.thens ~start:(P.cut_tac ~term:(ProofEngineReduction.replace ~equality:(==) ~with_what:(C.Rel 1) (* dummy_for_gen *) ~what:term ~where:ty)) ~continuations: [T.id_tac ; (P.apply_tac ~term:(C.Appl [term ; (C.Rel 1)]))]) (* in quest'ordine o viceversa? provare *) (* [(P.apply_tac ~term:(C.Appl [term ; (C.Rel 1)])) ; T.id_tac]) in quest'ordine o viceversa? provare *) *) ~status ;; *) let decide_equality_tac = Tacticals.id_tac ;; (* let compare_tac ~term1 ~term2 ~status:((proof, goal) as status) = let module C = Cic in let module U = UriManager in let module P = PrimitiveTactics in let module T = Tacticals in let _,metasenv,_,_ = proof in let _,context,gty = List.find (function (m,_,_) -> m=goal) metasenv in if ((CicTypeChecker.type_of_aux' metasenv context term1) = (CicTypeChecker.type_of_aux' metasenv context term2)) (* controllo che i due termini siano comparabili *) then T.thens ~start:P.cut_tac ~term:(* term1=term2->gty/\~term1=term2->gty *) ~continuations:[split_tac ; P.intros_tac ~name:"FOO"] else raise (ProofEngineTypes.Fail "Compare: Comparing terms of different types") ;; *) (*** DOMANDE *** - come faccio clear di un ipotesi di cui non so il nome? - differenza tra elim e induction ...e inversion? - come passo a decompose la lista di termini? - ma la rewrite funzionava? - come implemento la generalize? *)