(* 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/. *) open ProofEngineTypes (* Note: this code is almost identical to change_tac and * it could be unified by making the change function a callback *) let reduction_tac ~reduction ~pattern (proof,goal) = let curi,metasenv,pbo,pty = proof in let (metano,context,ty) as conjecture = CicUtil.lookup_meta goal metasenv in let change where terms = if terms = [] then where else let terms, terms' = List.split (List.map (fun (context, t) -> t, reduction context t) terms) in ProofEngineReduction.replace ~equality:(==) ~what:terms ~with_what:terms' ~where:where in let (selected_context,selected_ty) = ProofEngineHelpers.select ~metasenv ~conjecture ~pattern in let ty' = change ty selected_ty in let context' = List.fold_right2 (fun entry selected_entry context' -> match entry,selected_entry with None,None -> None::context' | Some (name,Cic.Decl ty),Some (`Decl selected_ty) -> let ty' = change ty selected_ty in Some (name,Cic.Decl ty')::context' | Some (name,Cic.Def (bo,ty)),Some (`Def (selected_bo,selected_ty)) -> let bo' = change bo selected_bo in let ty' = match ty,selected_ty with None,None -> None | Some ty,Some selected_ty -> Some (change ty selected_ty) | _,_ -> assert false in Some (name,Cic.Def (bo',ty'))::context' | _,_ -> assert false ) context selected_context [] in let metasenv' = List.map (function | (n,_,_) when n = metano -> (metano,context',ty') | _ as t -> t ) metasenv in (curi,metasenv',pbo,pty), [metano] ;; let simpl_tac ~pattern = mk_tactic (reduction_tac ~reduction:ProofEngineReduction.simpl ~pattern);; let reduce_tac ~pattern = mk_tactic (reduction_tac ~reduction:ProofEngineReduction.reduce ~pattern);; let whd_tac ~pattern = mk_tactic (reduction_tac ~reduction:CicReduction.whd ~pattern);; let normalize_tac ~pattern = mk_tactic (reduction_tac ~reduction:CicReduction.normalize ~pattern);; exception NotConvertible (* Note: this code is almost identical to reduction_tac and * it could be unified by making the change function a callback *) (* CSC: with_what is parsed in the context of the goal, but it should replace something that lives in a completely different context. Thus we perform a delift + lift phase to move it in the right context. However, in this way the tactic is less powerful than expected: with_what cannot reference variables that are local to the term that is going to be replaced. To fix this we should parse with_what in the context of the term(s) to be replaced. *) let change_tac ~pattern with_what = let change_tac ~pattern ~with_what (proof, goal) = let curi,metasenv,pbo,pty = proof in let (metano,context,ty) as conjecture = CicUtil.lookup_meta goal metasenv in let context_len = List.length context in let change context'_len where terms = if terms = [] then where else let terms, terms' = List.split (List.map (fun (context_of_t, t) -> let context_of_t_len = List.length context_of_t in let with_what_in_context' = if context_len > context'_len then begin let with_what,subst,metasenv' = CicMetaSubst.delift_rels [] metasenv (context_len - context'_len) with_what in assert (subst = []); assert (metasenv = metasenv'); with_what end else with_what in let with_what_in_context_of_t = if context_of_t_len > context'_len then CicSubstitution.lift (context_of_t_len - context'_len) with_what_in_context' else with_what in let _,u = CicTypeChecker.type_of_aux' metasenv context_of_t with_what CicUniv.empty_ugraph in let b,_ = CicReduction.are_convertible ~metasenv context_of_t t with_what u in if b then t, with_what_in_context_of_t else raise NotConvertible) terms) in ProofEngineReduction.replace ~equality:(==) ~what:terms ~with_what:terms' ~where:where in let (selected_context,selected_ty) = ProofEngineHelpers.select ~metasenv ~conjecture ~pattern in let ty' = change context_len ty selected_ty in let context' = List.fold_right2 (fun entry selected_entry context' -> let context'_len = List.length context' in match entry,selected_entry with None,None -> None::context' | Some (name,Cic.Decl ty),Some (`Decl selected_ty) -> let ty' = change context'_len ty selected_ty in Some (name,Cic.Decl ty')::context' | Some (name,Cic.Def (bo,ty)),Some (`Def (selected_bo,selected_ty)) -> let bo' = change context'_len bo selected_bo in let ty' = match ty,selected_ty with None,None -> None | Some ty,Some selected_ty -> Some (change context'_len ty selected_ty) | _,_ -> assert false in Some (name,Cic.Def (bo',ty'))::context' | _,_ -> assert false ) context selected_context [] in let metasenv' = List.map (function | (n,_,_) when n = metano -> (metano,context',ty') | _ as t -> t ) metasenv in (curi,metasenv',pbo,pty), [metano] in mk_tactic (change_tac ~pattern ~with_what) let fold_tac ~reduction ~term ~pattern = let fold_tac ~reduction ~term ~pattern:(wanted,hyps_pat,concl_pat) status = assert (wanted = None); (* this should be checked syntactically *) let proof,goal = status in let _,metasenv,_,_ = proof in let _,context,_ = CicUtil.lookup_meta goal metasenv in let reduced_term = reduction context term in apply_tactic (change_tac ~pattern:(Some reduced_term,hyps_pat,concl_pat) term) status in mk_tactic (fold_tac ~reduction ~term ~pattern) ;;