X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FproofEngineHelpers.ml;h=fa5c77d7170928091cbd50a29917b9fc40ec883c;hb=3a96f145e913a11cf64db491b001b4fdfc71b57a;hp=c3e6f04aa8286d56c8aa31bc5129eb99edbfd346;hpb=e31bb143e3a303321e509f415764338849b7e516;p=helm.git diff --git a/helm/software/components/tactics/proofEngineHelpers.ml b/helm/software/components/tactics/proofEngineHelpers.ml index c3e6f04aa..fa5c77d71 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, _, _) = +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 + 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 @@ -62,7 +62,7 @@ let subst_meta_in_proof proof meta term newmetasenv = * 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,8 +77,9 @@ 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 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 (* Metavariables can appear also in the *statement* of the theorem * since the parser does not reject as statements terms with @@ -104,7 +105,9 @@ let subst_meta_and_metasenv_in_proof proof meta subst_in newmetasenv = | _ -> 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 = @@ -483,17 +486,33 @@ exception Fail of string Lazy.t 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 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 -> @@ -504,7 +523,7 @@ exception Fail of string Lazy.t 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 subst,metasenv,ugraph,((Some (`Def ([],selected_ty)))::res), @@ -525,7 +544,7 @@ exception Fail of string Lazy.t 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 @@ -613,69 +632,6 @@ let locate_in_conjecture ?(equality=fun _ -> (==)) what (_,context,ty) = 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 @@ -689,19 +645,65 @@ let lookup_type metasenv context hyp = (* FG: **********************************************************************) -let list_rev_map_filter f l = - let rec aux a = function - | [] -> a - | hd :: tl -> - begin match f hd with - | None -> aux a tl - | Some b -> aux (b :: a) tl - end - in - aux [] l - let get_name context index = try match List.nth context (pred index) with | Some (Cic.Name name, _) -> Some name | _ -> None with Invalid_argument "List.nth" -> None + +let get_rel context name = + let rec aux i = function + | [] -> None + | Some (Cic.Name s, _) :: _ when s = name -> Some (Cic.Rel i) + | _ :: 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) + | Some (_,Cic.Def (t,None)) -> + List.map fst (CicUtil.metas_of_term ty) + | Some (_,Cic.Def (t,Some 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) +;; +