X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftactics%2FproofEngineHelpers.ml;h=c2d0d15e171586b339f2fa32cd695cac1d063c54;hb=e55c40ddebaa3664f294a8dd8df162e8c1fa5020;hp=cf7df2d58a197ca9895837e784aa0a94e4b47294;hpb=7f2444c2670cadafddd8785b687ef312158376b0;p=helm.git diff --git a/components/tactics/proofEngineHelpers.ml b/components/tactics/proofEngineHelpers.ml index cf7df2d58..c2d0d15e1 100644 --- a/components/tactics/proofEngineHelpers.ml +++ b/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,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'',bo',ty', attrs in (newproof, metasenv'') (*CSC: commento vecchio *) @@ -78,7 +78,7 @@ let subst_meta_in_proof proof meta term newmetasenv = (*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 (uri,_,bo,ty, attrs) = 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 @@ -104,7 +104,7 @@ let subst_meta_and_metasenv_in_proof proof meta subst_in newmetasenv = | _ -> i ) newmetasenv [] in - let newproof = uri,metasenv',bo',ty' in + let newproof = uri,metasenv',bo',ty', attrs in (newproof, metasenv') let compare_metasenvs ~oldmetasenv ~newmetasenv = @@ -613,69 +613,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 @@ -686,3 +623,19 @@ let lookup_type metasenv context hyp = | [] -> raise (ProofEngineTypes.Fail (lazy "lookup_type: not premise in the current goal")) in aux 1 context + +(* FG: **********************************************************************) + +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