* http://cs.unibo.it/helm/.
*)
+(* $Id$ *)
+
exception Bad_pattern of string Lazy.t
let new_meta_of_proof ~proof:(_, metasenv, _, _) =
find subst metasenv ugraph context wanted t
let select_in_term ~metasenv ~context ~ugraph ~term ~pattern:(wanted,where) =
- let add_ctx context name entry =
- (Some (name, entry)) :: context
- in
+ let add_ctx context name entry = (Some (name, entry)) :: context in
let map2 error_msg f l1 l2 =
try
List.map2 f l1 l2
List.concat (map2 "wrong number of arguments in application"
(fun t1 t2 -> aux context t1 t2) terms1 terms2)
in
- let roots = aux context where term in
+ let roots =
+ match where with
+ | None -> []
+ | Some where -> aux context where term
+ in
match wanted with
None -> [],metasenv,ugraph,roots
| Some wanted ->
* @raise Bad_pattern
* *)
let select ~metasenv ~ugraph ~conjecture:(_,context,ty)
- ~pattern:(what,hyp_patterns,goal_pattern)
+ ~(pattern: (Cic.term, Cic.lazy_term) ProofEngineTypes.pattern)
=
+ let what, hyp_patterns, goal_pattern = pattern in
let find_pattern_for name =
try Some (snd (List.find (fun (n, pat) -> Cic.Name n = name) hyp_patterns))
with Not_found -> None in
| Some pat ->
let subst,metasenv,ugraph,terms =
select_in_term ~metasenv ~context ~ugraph ~term
- ~pattern:(what,pat)
+ ~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
- ~pattern:(what,pat) in
+ ~pattern:(what, Some pat) in
let subst,metasenv,ugraph,terms_ty =
match ty with
None -> subst,metasenv,ugraph,None
| Some ty ->
let subst,metasenv,ugraph,res =
select_in_term ~metasenv ~context ~ugraph ~term:ty
- ~pattern:(what,pat)
+ ~pattern:(what, Some pat)
in
subst,metasenv,ugraph,Some res
in