*)
let new_meta_of_proof ~proof:(_, metasenv, _, _) =
- CicMkImplicit.new_meta metasenv
+ CicMkImplicit.new_meta metasenv []
let subst_meta_in_proof proof meta term newmetasenv =
let uri,metasenv,bo,ty = proof in
- let subst_in = CicMetaSubst.apply_subst [meta,term] 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 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 ~eq ~wanted t =
+ let rec find wanted t =
+ if eq wanted t then
+ [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 wanted t @ acc
+ ) [] ctx
+ | Cic.Lambda (_, t1, t2)
+ | Cic.Prod (_, t1, t2)
+ | Cic.LetIn (_, t1, t2) ->
+ find wanted t1 @ find (CicSubstitution.lift 1 wanted) t2
+ | Cic.Appl l ->
+ List.fold_left (fun acc t -> find wanted t @ acc) [] l
+ | Cic.Cast (t, ty) -> find wanted t @ find wanted ty
+ | Cic.Implicit _ -> assert false
+ | Cic.Const (_, esubst)
+ | Cic.Var (_, esubst)
+ | Cic.MutInd (_, _, esubst)
+ | Cic.MutConstruct (_, _, _, esubst) ->
+ List.fold_left (fun acc (_, t) -> find wanted t @ acc) [] esubst
+ | Cic.MutCase (_, _, outty, indterm, patterns) ->
+ find wanted outty @ find wanted indterm @
+ List.fold_left (fun acc p -> find wanted p @ acc) [] patterns
+ | Cic.Fix (_, funl) ->
+ List.fold_left (
+ fun acc (_, _, ty, bo) -> find wanted ty @ find wanted bo @ acc
+ ) [] funl
+ | Cic.CoFix (_, funl) ->
+ List.fold_left (
+ fun acc (_, ty, bo) -> find wanted ty @ find wanted bo @ acc
+ ) [] funl
+ in
+ find wanted t