X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FproofEngineHelpers.ml;h=d95d37d8ca53090771a8f10a7f1068d0eb0f3677;hb=af805d8cb199ea2c532983e29b064cf9861454f4;hp=b4e9a4e94dda77e472926710485393c45799811f;hpb=438a29376390222b94c1fe9772917c3aad50d42e;p=helm.git diff --git a/helm/software/components/tactics/proofEngineHelpers.ml b/helm/software/components/tactics/proofEngineHelpers.ml index b4e9a4e94..d95d37d8c 100644 --- a/helm/software/components/tactics/proofEngineHelpers.ml +++ b/helm/software/components/tactics/proofEngineHelpers.ml @@ -27,11 +27,11 @@ exception Bad_pattern of string Lazy.t -let new_meta_of_proof ~proof:(_, metasenv, _, _) = - CicMkImplicit.new_meta metasenv [] +let new_meta_of_proof ~proof:(_, metasenv, subst, _, _, _) = + CicMkImplicit.new_meta metasenv subst let subst_meta_in_proof proof meta term newmetasenv = - let uri,metasenv,bo,ty = proof in + let uri,metasenv,initial_subst,bo,ty, attrs = 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 @@ -48,21 +48,20 @@ let subst_meta_in_proof proof meta term newmetasenv = 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 (n,Cic.Def (bo,Some ty)) -> - Some (n,Cic.Def (subst_in bo,Some (subst_in ty))) + | Some (n,Cic.Def (bo,ty)) -> + Some (n,Cic.Def (subst_in bo,subst_in ty)) ) canonical_context in i,canonical_context',(subst_in ty) ) metasenv' in - let bo' = subst_in bo in + let bo' = lazy (subst_in (Lazy.force 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 + let newproof = uri,metasenv'',initial_subst,bo',ty', attrs in (newproof, metasenv'') (*CSC: commento vecchio *) @@ -77,9 +76,10 @@ let subst_meta_in_proof proof meta term newmetasenv = (*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 +let subst_meta_and_metasenv_in_proof proof meta subst newmetasenv = + let (uri,_,initial_subst,bo,ty, attrs) = proof in + let subst_in = CicMetaSubst.apply_subst subst in + let bo' = lazy (subst_in (Lazy.force bo)) in (* Metavariables can appear also in the *statement* of the theorem * since the parser does not reject as statements terms with * metavariable therein *) @@ -94,17 +94,17 @@ let subst_meta_and_metasenv_in_proof proof meta subst_in newmetasenv = (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 (i,Cic.Def (bo,Some ty)) -> - Some (i,Cic.Def (subst_in bo,Some (subst_in ty))) + | Some (i,Cic.Def (bo,ty)) -> + Some (i,Cic.Def (subst_in bo,subst_in ty)) ) canonical_context in (m,canonical_context',subst_in ty)::i | _ -> i ) newmetasenv [] in - let newproof = uri,metasenv',bo',ty' in + (* qui da capire se per la fase transitoria si fa initial_subst @ subst + * oppure subst *) + let newproof = uri,metasenv',subst,bo',ty', attrs in (newproof, metasenv') let compare_metasenvs ~oldmetasenv ~newmetasenv = @@ -148,14 +148,16 @@ let find_subterms ~subst ~metasenv ~ugraph ~wanted ~context t = (CicSubstitution.lift 1 w) t2 in subst,metasenv,ugraph,rest1 @ rest2 - | Cic.LetIn (name, t1, t2) -> + | Cic.LetIn (name, t1, t2, t3) -> let subst,metasenv,ugraph,rest1 = find subst metasenv ugraph context w t1 in let subst,metasenv,ugraph,rest2 = - find subst metasenv ugraph (Some (name, Cic.Def (t1,None))::context) - (CicSubstitution.lift 1 w) t2 + find subst metasenv ugraph context w t2 in + let subst,metasenv,ugraph,rest3 = + find subst metasenv ugraph (Some (name, Cic.Def (t1,t2))::context) + (CicSubstitution.lift 1 w) t3 in - subst,metasenv,ugraph,rest1 @ rest2 + subst,metasenv,ugraph,rest1 @ rest2 @ rest3 | Cic.Appl l -> List.fold_left (fun (subst,metasenv,ugraph,acc) t -> @@ -227,7 +229,9 @@ let find_subterms ~subst ~metasenv ~ugraph ~wanted ~context t = in find subst metasenv ugraph context wanted t -let select_in_term ~metasenv ~context ~ugraph ~term ~pattern:(wanted,where) = +let select_in_term + ~metasenv ~subst ~context ~ugraph ~term ~pattern:(wanted,where) += let add_ctx context name entry = (Some (name, entry)) :: context in let map2 error_msg f l1 l2 = try @@ -260,12 +264,16 @@ let select_in_term ~metasenv ~context ~ugraph ~term ~pattern:(wanted,where) = 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.LetIn (Cic.Anonymous, s1, ty1, t1), Cic.LetIn (name, s2, ty2, t2) -> + aux context s1 s2 @ + aux context ty1 ty2 @ + aux (add_ctx context name (Cic.Def (s2,ty2))) t1 t2 + | Cic.LetIn (Cic.Name n1, s1, ty1, t1), + Cic.LetIn ((Cic.Name n2) as name, s2, ty2, t2) when n1 = n2-> + aux context s1 s2 @ + aux context ty1 ty2 @ + aux (add_ctx context name (Cic.Def (s2,ty2))) t1 t2 + | Cic.LetIn (name1, s1, ty1, t1), Cic.LetIn (name2, s2, ty2, t2) -> [] | Cic.Appl terms1, Cic.Appl terms2 -> auxs context terms1 terms2 | Cic.Var (_, subst1), Cic.Var (_, subst2) | Cic.Const (_, subst1), Cic.Const (_, subst2) @@ -307,13 +315,13 @@ let select_in_term ~metasenv ~context ~ugraph ~term ~pattern:(wanted,where) = | Some where -> aux context where term in match wanted with - None -> [],metasenv,ugraph,roots + None -> subst,metasenv,ugraph,roots | Some wanted -> - let rec find_in_roots = + let rec find_in_roots subst = function - [] -> [],metasenv,ugraph,[] + [] -> subst,metasenv,ugraph,[] | (context',where)::tl -> - let subst,metasenv,ugraph,tl' = find_in_roots tl in + let subst,metasenv,ugraph,tl' = find_in_roots subst tl in let subst,metasenv,ugraph,found = let wanted, metasenv, ugraph = wanted context' metasenv ugraph in find_subterms ~subst ~metasenv ~ugraph ~wanted ~context:context' @@ -321,7 +329,8 @@ let select_in_term ~metasenv ~context ~ugraph ~term ~pattern:(wanted,where) = in subst,metasenv,ugraph,found @ tl' in - find_in_roots roots + find_in_roots subst roots +;; (** create a pattern from a term and a list of subterms. * the pattern is granted to have a ? for every subterm that has no selected @@ -360,25 +369,26 @@ let pattern_of ?(equality=(==)) ~term terms = if b1||b2 then true,Cic.Cast (te, ty) else not_found - | Cic.Prod (name, s, t) -> + | Cic.Prod (_, s, t) -> let b1,s = aux s in let b2,t = aux t in if b1||b2 then - true, Cic.Prod (name, s, t) + true, Cic.Prod (Cic.Anonymous, s, t) else not_found - | Cic.Lambda (name, s, t) -> + | Cic.Lambda (_, s, t) -> let b1,s = aux s in let b2,t = aux t in if b1||b2 then - true, Cic.Lambda (name, s, t) + true, Cic.Lambda (Cic.Anonymous, s, t) else not_found - | Cic.LetIn (name, s, t) -> + | Cic.LetIn (_, s, ty, t) -> let b1,s = aux s in - let b2,t = aux t in - if b1||b2 then - true, Cic.LetIn (name, s, t) + let b2,ty = aux ty in + let b3,t = aux t in + if b1||b2||b3 then + true, Cic.LetIn (Cic.Anonymous, s, ty, t) else not_found | Cic.Appl terms -> @@ -476,60 +486,75 @@ exception Fail of string Lazy.t * * @raise Bad_pattern * *) - let select ~metasenv ~ugraph ~conjecture:(_,context,ty) + let select ~metasenv ~subst ~ugraph ~conjecture:(_,context,ty) ~(pattern: (Cic.term, Cic.lazy_term) ProofEngineTypes.pattern) = let what, hyp_patterns, goal_pattern = pattern in let find_pattern_for name = try Some (snd (List.find (fun (n, pat) -> Cic.Name n = name) hyp_patterns)) with Not_found -> None in + (* Multiple hypotheses with the same name can be in the context. + In this case we need to pick the last one, but we will perform + a fold_right on the context. Thus we pre-process hyp_patterns. *) + let full_hyp_pattern = + let rec aux blacklist = + function + [] -> [] + | None::tl -> None::aux blacklist tl + | Some (name,_)::tl -> + if List.mem name blacklist then + None::aux blacklist tl + else + find_pattern_for name::aux (name::blacklist) tl + in + aux [] context + in let subst,metasenv,ugraph,ty_terms = - select_in_term ~metasenv ~context ~ugraph ~term:ty - ~pattern:(what,goal_pattern) in + select_in_term ~metasenv ~subst ~context ~ugraph ~term:ty + ~pattern:(what,goal_pattern) + in let subst,metasenv,ugraph,context_terms = let subst,metasenv,ugraph,res,_ = (List.fold_right - (fun entry (subst,metasenv,ugraph,res,context) -> + (fun (pattern,entry) (subst,metasenv,ugraph,res,context) -> match entry with - None -> subst,metasenv,ugraph,(None::res),(None::context) + None -> subst,metasenv,ugraph,None::res,None::context | Some (name,Cic.Decl term) -> - (match find_pattern_for name with + (match pattern with | None -> subst,metasenv,ugraph,((Some (`Decl []))::res),(entry::context) | Some pat -> let subst,metasenv,ugraph,terms = - select_in_term ~metasenv ~context ~ugraph ~term + select_in_term ~subst ~metasenv ~context ~ugraph ~term ~pattern:(what, Some pat) in subst,metasenv,ugraph,((Some (`Decl terms))::res), (entry::context)) | Some (name,Cic.Def (bo, ty)) -> - (match find_pattern_for name with + (match pattern with | None -> - let selected_ty=match ty with None -> None | Some _ -> Some [] in + let selected_ty = [] in subst,metasenv,ugraph,((Some (`Def ([],selected_ty)))::res), (entry::context) | Some pat -> let subst,metasenv,ugraph,terms_bo = - select_in_term ~metasenv ~context ~ugraph ~term:bo + select_in_term ~subst ~metasenv ~context ~ugraph ~term:bo ~pattern:(what, Some pat) in let subst,metasenv,ugraph,terms_ty = - match ty with - None -> subst,metasenv,ugraph,None - | Some ty -> - let subst,metasenv,ugraph,res = - select_in_term ~metasenv ~context ~ugraph ~term:ty - ~pattern:(what, Some pat) - in - subst,metasenv,ugraph,Some res + let subst,metasenv,ugraph,res = + select_in_term ~subst ~metasenv ~context ~ugraph ~term:ty + ~pattern:(what, Some pat) + in + subst,metasenv,ugraph,res in subst,metasenv,ugraph,((Some (`Def (terms_bo,terms_ty)))::res), (entry::context)) - ) context (subst,metasenv,ugraph,[],[])) + ) (List.combine full_hyp_pattern context) (subst,metasenv,ugraph,[],[])) in subst,metasenv,ugraph,res in subst,metasenv,ugraph,context_terms, ty_terms +;; (** locate_in_term equality what where context * [what] must match a subterm of [where] according to [equality] @@ -556,8 +581,10 @@ let locate_in_term ?(equality=(fun _ -> (==))) what ~where context = | Cic.Prod (name, s, t) | Cic.Lambda (name, s, t) -> aux context s @ aux (add_ctx context name (Cic.Decl s)) t - | Cic.LetIn (name, s, t) -> - aux context s @ aux (add_ctx context name (Cic.Def (s,None))) t + | Cic.LetIn (name, s, ty, t) -> + aux context s @ + aux context ty @ + aux (add_ctx context name (Cic.Def (s,ty))) t | Cic.Appl tl -> auxs context tl | Cic.MutCase (_, _, out, t, pat) -> aux context out @ aux context t @ auxs context pat @@ -602,91 +629,48 @@ let locate_in_conjecture ?(equality=fun _ -> (==)) what (_,context,ty) = context',res | Some (_, Cic.Def (bo,ty)) -> let res = res @ locate_in_term what ~where:bo context in - let res = - match ty with - None -> res - | Some ty -> - res @ locate_in_term what ~where:ty context in + let res = res @ locate_in_term what ~where:ty context in let context' = entry::context in context',res ) context ([],[]) in res @ locate_in_term what ~where:ty context -(* saturate_term newmeta metasenv context ty goal_arity *) -(* Given a type [ty] (a backbone), it returns its suffix of length *) -(* [goal_arity] head and a new metasenv in which there is new a META for each *) -(* hypothesis, a list of arguments for the new applications and the index of *) -(* the last new META introduced. The nth argument in the list of arguments is *) -(* just the nth new META. *) -let saturate_term newmeta metasenv context ty goal_arity = - let module C = Cic in - let module S = CicSubstitution in - assert (goal_arity >= 0); - let rec aux newmeta ty = - match ty with - C.Cast (he,_) -> aux newmeta he -(* CSC: patch to generate ?1 : ?2 : Type in place of ?1 : Type to simulate ?1 :< Type - (* If the expected type is a Type, then also Set is OK ==> - * we accept any term of type Type *) - (*CSC: BUG HERE: in this way it is possible for the term of - * type Type to be different from a Sort!!! *) - | C.Prod (name,(C.Sort (C.Type _) as s),t) -> - (* TASSI: ask CSC if BUG HERE refers to the C.Cast or C.Propd case *) - let irl = - CicMkImplicit.identity_relocation_list_for_metavariable context - in - let newargument = C.Meta (newmeta+1,irl) in - let (res,newmetasenv,arguments,lastmeta) = - aux (newmeta + 2) (S.subst newargument t) - in - res, - (newmeta,[],s)::(newmeta+1,context,C.Meta (newmeta,[]))::newmetasenv, - newargument::arguments,lastmeta -*) - | C.Prod (name,s,t) -> - let irl = - CicMkImplicit.identity_relocation_list_for_metavariable context - in - let newargument = C.Meta (newmeta,irl) in - let res,newmetasenv,arguments,lastmeta,prod_no = - aux (newmeta + 1) (S.subst newargument t) - in - if prod_no + 1 = goal_arity then - let head = CicReduction.normalize ~delta:false context ty in - head,[],[],lastmeta,goal_arity + 1 - else - (** NORMALIZE RATIONALE - * we normalize the target only NOW since we may be in this case: - * A1 -> A2 -> T where T = (\lambda x.A3 -> P) k - * and we want a mesasenv with ?1:A1 and ?2:A2 and not - * ?1, ?2, ?3 (that is the one we whould get if we start from the - * beta-normalized A1 -> A2 -> A3 -> P **) - let s' = CicReduction.normalize ~delta:false context s in - res,(newmeta,context,s')::newmetasenv,newargument::arguments, - lastmeta,prod_no + 1 - | t -> - let head = CicReduction.normalize ~delta:false context t in - match CicReduction.whd context head with - C.Prod _ as head' -> aux newmeta head' - | _ -> head,[],[],newmeta,0 - in - (* WARNING: here we are using the invariant that above the most *) - (* recente new_meta() there are no used metas. *) - let res,newmetasenv,arguments,lastmeta,_ = aux newmeta ty in - res,metasenv @ newmetasenv,arguments,lastmeta - let lookup_type metasenv context hyp = let rec aux p = function | Some (Cic.Name name, Cic.Decl t) :: _ when name = hyp -> p, t - | Some (Cic.Name name, Cic.Def (_, Some t)) :: _ when name = hyp -> p, t - | Some (Cic.Name name, Cic.Def (u, _)) :: tail when name = hyp -> - p, fst (CicTypeChecker.type_of_aux' metasenv tail u CicUniv.empty_ugraph) + | Some (Cic.Name name, Cic.Def (_,t)) :: _ when name = hyp -> p, t | _ :: tail -> aux (succ p) tail | [] -> raise (ProofEngineTypes.Fail (lazy "lookup_type: not premise in the current goal")) in aux 1 context +let find_hyp name = + let rec find_hyp n = + function + [] -> assert false + | Some (Cic.Name s,Cic.Decl ty)::_ when name = s -> + Cic.Rel n, CicSubstitution.lift n ty + | Some (Cic.Name s,Cic.Def _)::_ when name = s -> assert false (*CSC: not implemented yet! But does this make any sense?*) + | _::tl -> find_hyp (n+1) tl + in + find_hyp 1 +;; + +(* sort pattern hypotheses from the smallest to the highest Rel *) +let sort_pattern_hyps context (t,hpatterns,cpattern) = + let hpatterns = + List.sort + (fun (id1,_) (id2,_) -> + let t1,_ = find_hyp id1 context in + let t2,_ = find_hyp id2 context in + match t1,t2 with + Cic.Rel n1, Cic.Rel n2 -> compare n1 n2 + | _,_ -> assert false) hpatterns + in + t,hpatterns,cpattern +;; + (* FG: **********************************************************************) let get_name context index = @@ -702,3 +686,50 @@ let get_rel context name = | _ :: tl -> aux (succ i) tl in aux 1 context + +let split_with_whd (c, t) = + let add s v c = Some (s, Cic.Decl v) :: c in + let rec aux whd a n c = function + | Cic.Prod (s, v, t) -> aux false ((c, v) :: a) (succ n) (add s v c) t + | v when whd -> (c, v) :: a, n + | v -> aux true a n c (CicReduction.whd c v) + in + aux false [] 0 c t + +let split_with_normalize (c, t) = + let add s v c = Some (s, Cic.Decl v) :: c in + let rec aux a n c = function + | Cic.Prod (s, v, t) -> aux ((c, v) :: a) (succ n) (add s v c) t + | v -> (c, v) :: a, n + in + aux [] 0 c (CicReduction.normalize c t) + + (* menv sorting *) +module OT = + struct + type t = Cic.conjecture + let compare (i,_,_) (j,_,_) = Pervasives.compare i j + end +module MS = HTopoSort.Make(OT) +let relations_of_menv m c = + let i, ctx, ty = c in + let m = List.filter (fun (j,_,_) -> j <> i) m in + let m_ty = List.map fst (CicUtil.metas_of_term ty) in + let m_ctx = + List.flatten + (List.map + (function + | None -> [] + | Some (_,Cic.Decl t) -> + List.map fst (CicUtil.metas_of_term ty) + | Some (_,Cic.Def (t,ty)) -> + List.map fst (CicUtil.metas_of_term ty) @ + List.map fst (CicUtil.metas_of_term t)) + ctx) + in + let metas = HExtlib.list_uniq (List.sort compare (m_ty @ m_ctx)) in + List.filter (fun (i,_,_) -> List.exists ((=) i) metas) m +;; +let sort_metasenv (m : Cic.metasenv) = + (MS.topological_sort m (relations_of_menv m) : Cic.metasenv) +;;