* http://cs.unibo.it/helm/.
*)
-exception Bad_pattern of string
+(* $Id$ *)
+
+exception Bad_pattern of string Lazy.t
let new_meta_of_proof ~proof:(_, metasenv, _, _) =
CicMkImplicit.new_meta metasenv []
List.map
(function
Some (n,Cic.Decl s) -> Some (n,Cic.Decl (subst_in s))
- | Some (n,Cic.Def (s,None)) -> Some (n,Cic.Def ((subst_in s),None))
+ | Some (n,Cic.Def (s,None)) -> Some (n,Cic.Def (subst_in s,None))
| None -> None
- | Some (_,Cic.Def (_,Some _)) -> assert false
+ | Some (n,Cic.Def (bo,Some ty)) ->
+ Some (n,Cic.Def (subst_in bo,Some (subst_in ty)))
) canonical_context
in
i,canonical_context',(subst_in ty)
None -> None
| Some (i,Cic.Decl t) -> Some (i,Cic.Decl (subst_in t))
| Some (i,Cic.Def (t,None)) ->
- Some (i,Cic.Def ((subst_in t),None))
- | Some (_,Cic.Def (_,Some _)) -> assert false
+ Some (i,Cic.Def (subst_in t,None))
+ | Some (i,Cic.Def (bo,Some ty)) ->
+ Some (i,Cic.Def (subst_in bo,Some (subst_in ty)))
) canonical_context
in
(m,canonical_context',subst_in ty)::i
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
with
- | Invalid_argument _ -> raise (Bad_pattern error_msg)
+ | Invalid_argument _ -> raise (Bad_pattern (lazy error_msg))
in
let rec aux context where term =
match (where, term) with
funs1 funs2)
| x,y ->
raise (Bad_pattern
- (Printf.sprintf "Pattern %s versus term %s"
+ (lazy (Printf.sprintf "Pattern %s versus term %s"
(CicPp.ppterm x)
- (CicPp.ppterm y)))
+ (CicPp.ppterm y))))
and auxs context terms1 terms2 = (* as aux for list of terms *)
List.concat (map2 "wrong number of arguments in application"
(fun t1 t2 -> aux context t1 t2) terms1 terms2)
in
- let context_len = List.length context 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 ->
in
snd (aux term)
-exception Fail of string
+exception Fail of string Lazy.t
(** select metasenv conjecture pattern
* select all subterms of [conjecture] matching [pattern].
* @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
let subst,metasenv,ugraph,ty_terms =
select_in_term ~metasenv ~context ~ugraph ~term:ty
~pattern:(what,goal_pattern) in
- let context_len = List.length context in
let subst,metasenv,ugraph,context_terms =
let subst,metasenv,ugraph,res,_ =
(List.fold_right
| 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
| Some (Cic.Name name, Cic.Def (u, _)) :: tail when name = hyp ->
p, fst (CicTypeChecker.type_of_aux' metasenv tail u CicUniv.empty_ugraph)
| _ :: tail -> aux (succ p) tail
- | [] -> raise (ProofEngineTypes.Fail "lookup_type: not premise in the current goal")
+ | [] -> raise (ProofEngineTypes.Fail (lazy "lookup_type: not premise in the current goal"))
in
aux 1 context