(* 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/. *) exception Bad_pattern of string let new_meta_of_proof ~proof:(_, metasenv, _, _) = CicMkImplicit.new_meta metasenv [] let subst_meta_in_proof proof meta term newmetasenv = let uri,metasenv,bo,ty = proof in (* empty context is ok for term since it wont be used by apply_subst *) (* hack: since we do not know the context and the type of term, we create a substitution with cc =[] and type = Implicit; they will be in any case dropped by apply_subst, but it would be better to rewrite the code. Cannot we just use apply_subst_metasenv, etc. ?? *) let subst_in = CicMetaSubst.apply_subst [meta,([], term,Cic.Implicit None)] in let metasenv' = newmetasenv @ (List.filter (function (m,_,_) -> m <> meta) metasenv) in let metasenv'' = List.map (function i,canonical_context,ty -> let canonical_context' = List.map (function Some (n,Cic.Decl s) -> Some (n,Cic.Decl (subst_in s)) | Some (n,Cic.Def (s,None)) -> Some (n,Cic.Def ((subst_in s),None)) | None -> None | Some (_,Cic.Def (_,Some _)) -> assert false ) canonical_context in i,canonical_context',(subst_in ty) ) metasenv' in let bo' = subst_in bo in (* Metavariables can appear also in the *statement* of the theorem * since the parser does not reject as statements terms with * metavariable therein *) let ty' = subst_in ty in let newproof = uri,metasenv'',bo',ty' in (newproof, metasenv'') (*CSC: commento vecchio *) (* refine_meta_with_brand_new_metasenv meta term subst_in newmetasenv *) (* This (heavy) function must be called when a tactic can instantiate old *) (* metavariables (i.e. existential variables). It substitues the metasenv *) (* of the proof with the result of removing [meta] from the domain of *) (* [newmetasenv]. Then it replaces Cic.Meta [meta] with [term] everywhere *) (* in the current proof. Finally it applies [apply_subst_replacing] to *) (* current proof. *) (*CSC: A questo punto perche' passare un bo' gia' istantiato, se tanto poi *) (*CSC: ci ripasso sopra apply_subst!!! *) (*CSC: Attenzione! Ora questa funzione applica anche [subst_in] a *) (*CSC: [newmetasenv]. *) let subst_meta_and_metasenv_in_proof proof meta subst_in newmetasenv = let (uri,_,bo,ty) = proof in let bo' = subst_in bo in (* Metavariables can appear also in the *statement* of the theorem * since the parser does not reject as statements terms with * metavariable therein *) let ty' = subst_in ty in let metasenv' = List.fold_right (fun metasenv_entry i -> match metasenv_entry with (m,canonical_context,ty) when m <> meta -> let canonical_context' = List.map (function None -> None | Some (i,Cic.Decl t) -> Some (i,Cic.Decl (subst_in t)) | Some (i,Cic.Def (t,None)) -> Some (i,Cic.Def ((subst_in t),None)) | Some (_,Cic.Def (_,Some _)) -> assert false ) canonical_context in (m,canonical_context',subst_in ty)::i | _ -> i ) newmetasenv [] in let newproof = uri,metasenv',bo',ty' in (newproof, metasenv') let compare_metasenvs ~oldmetasenv ~newmetasenv = List.map (function (i,_,_) -> i) (List.filter (function (i,_,_) -> not (List.exists (fun (j,_,_) -> i=j) oldmetasenv)) newmetasenv) ;; (** finds the _pointers_ to subterms that are alpha-equivalent to wanted in t *) let find_subterms ~wanted ~context t = let rec find context w t = if ProofEngineReduction.alpha_equivalence w t then [context,t] else match t with | Cic.Sort _ | Cic.Rel _ -> [] | Cic.Meta (_, ctx) -> List.fold_left ( fun acc e -> match e with | None -> acc | Some t -> find context w t @ acc ) [] ctx | Cic.Lambda (name, t1, t2) | Cic.Prod (name, t1, t2) -> find context w t1 @ find (Some (name, Cic.Decl t1)::context) (CicSubstitution.lift 1 w) t2 | Cic.LetIn (name, t1, t2) -> find context w t1 @ find (Some (name, Cic.Def (t1,None))::context) (CicSubstitution.lift 1 w) t2 | Cic.Appl l -> List.fold_left (fun acc t -> find context w t @ acc) [] l | Cic.Cast (t, ty) -> find context w t @ find context w ty | Cic.Implicit _ -> assert false | Cic.Const (_, esubst) | Cic.Var (_, esubst) | Cic.MutInd (_, _, esubst) | Cic.MutConstruct (_, _, _, esubst) -> List.fold_left (fun acc (_, t) -> find context w t @ acc) [] esubst | Cic.MutCase (_, _, outty, indterm, patterns) -> find context w outty @ find context w indterm @ List.fold_left (fun acc p -> find context w p @ acc) [] patterns | Cic.Fix (_, funl) -> let tys = List.map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) funl in List.fold_left ( fun acc (_, _, ty, bo) -> find context w ty @ find (tys @ context) w bo @ acc ) [] funl | Cic.CoFix (_, funl) -> let tys = List.map (fun (n,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) funl in List.fold_left ( fun acc (_, ty, bo) -> find context w ty @ find (tys @ context) w bo @ acc ) [] funl in find context wanted t let select_in_term ~context ~term ~pattern:(wanted,where) = let add_ctx context name entry = (Some (name, entry)) :: context in let rec aux context where term = match (where, term) with | Cic.Implicit (Some `Hole), t -> [context,t] | Cic.Implicit (Some `Type), t -> [] | Cic.Implicit None,_ -> [] | Cic.Meta (_, ctxt1), Cic.Meta (_, ctxt2) -> List.concat (List.map2 (fun t1 t2 -> (match (t1, t2) with Some t1, Some t2 -> aux context t1 t2 | _ -> [])) ctxt1 ctxt2) | Cic.Cast (te1, ty1), Cic.Cast (te2, ty2) -> aux context te1 te2 @ aux context ty1 ty2 | Cic.Prod (Cic.Anonymous, s1, t1), Cic.Prod (name, s2, t2) | Cic.Lambda (Cic.Anonymous, s1, t1), Cic.Lambda (name, s2, t2) -> aux context s1 s2 @ aux (add_ctx context name (Cic.Decl s2)) t1 t2 | Cic.Prod (Cic.Name n1, s1, t1), Cic.Prod ((Cic.Name n2) as name , s2, t2) | Cic.Lambda (Cic.Name n1, s1, t1), Cic.Lambda ((Cic.Name n2) as name, s2, t2) when n1 = n2-> aux context s1 s2 @ aux (add_ctx context name (Cic.Decl s2)) t1 t2 | Cic.Prod (name1, s1, t1), Cic.Prod (name2, s2, t2) | Cic.Lambda (name1, s1, t1), Cic.Lambda (name2, s2, t2) -> [] | Cic.LetIn (Cic.Anonymous, s1, t1), Cic.LetIn (name, s2, t2) -> aux context s1 s2 @ aux (add_ctx context name (Cic.Def (s2,None))) t1 t2 | Cic.LetIn (Cic.Name n1, s1, t1), Cic.LetIn ((Cic.Name n2) as name, s2, t2) when n1 = n2-> aux context s1 s2 @ aux (add_ctx context name (Cic.Def (s2,None))) t1 t2 | Cic.LetIn (name1, s1, t1), Cic.LetIn (name2, s2, t2) -> [] | Cic.Appl terms1, Cic.Appl terms2 -> auxs context terms1 terms2 | Cic.Var (_, subst1), Cic.Var (_, subst2) | Cic.Const (_, subst1), Cic.Const (_, subst2) | Cic.MutInd (_, _, subst1), Cic.MutInd (_, _, subst2) | Cic.MutConstruct (_, _, _, subst1), Cic.MutConstruct (_, _, _, subst2) -> auxs context (List.map snd subst1) (List.map snd subst2) | Cic.MutCase (_, _, out1, t1, pat1), Cic.MutCase (_ , _, out2, t2, pat2) -> aux context out1 out2 @ aux context t1 t2 @ auxs context pat1 pat2 | Cic.Fix (_, funs1), Cic.Fix (_, funs2) -> let tys = List.map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) funs2 in List.concat (List.map2 (fun (_, _, ty1, bo1) (_, _, ty2, bo2) -> aux context ty1 ty2 @ aux (tys @ context) bo1 bo2) funs1 funs2) | Cic.CoFix (_, funs1), Cic.CoFix (_, funs2) -> let tys = List.map (fun (n,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) funs2 in List.concat (List.map2 (fun (_, ty1, bo1) (_, ty2, bo2) -> aux context ty1 ty2 @ aux (tys @ context) bo1 bo2) funs1 funs2) | x,y -> raise (Bad_pattern (Printf.sprintf "Pattern %s versus term %s" (CicPp.ppterm x) (CicPp.ppterm y))) and auxs context terms1 terms2 = (* as aux for list of terms *) List.concat (List.map2 (fun t1 t2 -> aux context t1 t2) terms1 terms2) in let roots = aux context where term in match wanted with None -> roots | Some wanted -> let rec find_in_roots = function [] -> [] | (context,where)::tl -> let tl' = find_in_roots tl in let found = let wanted = CicSubstitution.lift (List.length context) wanted in find_subterms ~wanted ~context where in found @ tl' in find_in_roots roots exception Fail of string (** select metasenv conjecture pattern * select all subterms of [conjecture] matching [pattern]. * It returns the set of matched terms (that can be compared using physical * equality to the subterms of [conjecture]) together with their contexts. * The representation of the set mimics the ProofEngineTypes.pattern type: * a list of hypothesis (names of) together with the list of its matched * subterms (and their contexts) + the list of matched subterms of the * with their context conclusion. Note: in the result the list of hypothesis * has an entry for each entry in the context and in the same order. * Of course the list of terms (with their context) associated to the * hypothesis name may be empty. *) let select ~metasenv ~conjecture:(_,context,ty) ~pattern:(what,hyp_patterns,goal_pattern) = let find_pattern_for name = try Some (snd (List.find (fun (n, pat) -> Cic.Name n = name) hyp_patterns)) with Not_found -> None in let ty_terms = select_in_term ~context ~term:ty ~pattern:(what,goal_pattern) in let context_len = List.length context in let context_terms = fst (List.fold_right (fun entry (res,context) -> match entry with None -> (None::res),(None::context) | Some (name,Cic.Decl term) -> (match find_pattern_for name with | None -> ((Some (`Decl []))::res),(entry::context) | Some pat -> try let what = match what with None -> None | Some what -> let what,subst',metasenv' = CicMetaSubst.delift_rels [] metasenv (context_len - List.length context) what in assert (subst' = []); assert (metasenv' = metasenv); Some what in let terms = select_in_term ~context ~term ~pattern:(what,pat) in ((Some (`Decl terms))::res),(entry::context) with CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable -> raise (Fail ("The term the user wants to convert is not closed " ^ "in the context of the position of the substitution."))) | Some (name,Cic.Def (bo, ty)) -> (match find_pattern_for name with | None -> let selected_ty= match ty with None -> None | Some _ -> Some [] in ((Some (`Def ([],selected_ty)))::res),(entry::context) | Some pat -> try let what = match what with None -> None | Some what -> let what,subst',metasenv' = CicMetaSubst.delift_rels [] metasenv (context_len - List.length context) what in assert (subst' = []); assert (metasenv' = metasenv); Some what in let terms_bo = select_in_term ~context ~term:bo ~pattern:(what,pat) in let terms_ty = match ty with None -> None | Some ty -> Some (select_in_term ~context ~term:ty ~pattern:(what,pat)) in ((Some (`Def (terms_bo,terms_ty)))::res),(entry::context) with CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable -> raise (Fail ("The term the user wants to convert is not closed " ^ "in the context of the position of the substitution."))) ) context ([],[])) in context_terms, ty_terms