X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FproofEngineHelpers.ml;h=d95d37d8ca53090771a8f10a7f1068d0eb0f3677;hb=b68e52f889215ce2c21c3d771f59b2d2057d53c1;hp=7d223a4437b4d9fe232032315b9ec8c933a17a6a;hpb=cc23f034c9419186602d9250456241f2eba90d7c;p=helm.git diff --git a/helm/software/components/tactics/proofEngineHelpers.ml b/helm/software/components/tactics/proofEngineHelpers.ml index 7d223a443..d95d37d8c 100644 --- a/helm/software/components/tactics/proofEngineHelpers.ml +++ b/helm/software/components/tactics/proofEngineHelpers.ml @@ -27,8 +27,8 @@ 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,initial_subst,bo,ty, attrs = proof in @@ -56,7 +56,7 @@ let subst_meta_in_proof proof meta term newmetasenv = 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 *) @@ -79,7 +79,7 @@ let subst_meta_in_proof proof meta term newmetasenv = 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' = 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 *) @@ -229,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 @@ -313,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' @@ -327,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 @@ -483,7 +486,7 @@ 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 @@ -507,8 +510,9 @@ exception Fail of string Lazy.t 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 @@ -521,7 +525,7 @@ exception Fail of string Lazy.t 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), @@ -534,11 +538,11 @@ exception Fail of string Lazy.t (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 = let subst,metasenv,ugraph,res = - select_in_term ~metasenv ~context ~ugraph ~term:ty + select_in_term ~subst ~metasenv ~context ~ugraph ~term:ty ~pattern:(what, Some pat) in subst,metasenv,ugraph,res @@ -550,6 +554,7 @@ exception Fail of string Lazy.t 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] @@ -640,6 +645,32 @@ let lookup_type metasenv context hyp = 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 =