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
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 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 *)
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
| 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'
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
*
* @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
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
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 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
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]