* http://cs.unibo.it/helm/.
*)
-exception Bad_pattern of string
+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
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
snd (aux term)
-exception Fail of string
+exception Fail of string Lazy.t
(** select metasenv conjecture pattern
* select all subterms of [conjecture] matching [pattern].
| 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