-exception MetaSubstFailure of string
-exception Uncertain of string
-exception AssertFailure of string
+exception MetaSubstFailure of string Lazy.t
+exception Uncertain of string Lazy.t
+exception AssertFailure of string Lazy.t
exception DeliftingARelWouldCaptureAFreeVariable;;
let debug_print = fun _ -> ()
(more @ more_to_be_restricted @ more_to_be_restricted',
metasenv')
with Occur ->
- raise (MetaSubstFailure (sprintf
+ raise (MetaSubstFailure (lazy (sprintf
"Cannot restrict the context of the metavariable ?%d over the hypotheses %s since metavariable's type depends on at least one of them"
- n (names_of_context_indexes context to_be_restricted))))
- metasenv ([], [])
+ n (names_of_context_indexes context to_be_restricted)))))
+ metasenv ([], [])
in
let (more_to_be_restricted', subst) = (* restrict subst *)
List.fold_right
@ more_to_be_restricted'@more_to_be_restricted'' in
(more, subst')
with Occur ->
- let error_msg = sprintf
+ let error_msg = lazy (sprintf
"Cannot restrict the context of the metavariable ?%d over the hypotheses %s since ?%d is already instantiated with %s and at least one of the hypotheses occurs in the substituted term"
n (names_of_context_indexes context to_be_restricted) n
- (ppterm subst term)
+ (ppterm subst term))
in
(* DEBUG
debug_print (lazy error_msg);
deliftaux k (S.lift m t)
| Some (_,C.Decl t) ->
C.Rel ((position (m-k) l) + k)
- | None -> raise (MetaSubstFailure "RelToHiddenHypothesis")
+ | None -> raise (MetaSubstFailure (lazy "RelToHiddenHypothesis"))
with
Failure _ ->
- raise (MetaSubstFailure "Unbound variable found in deliftaux")
+ raise (MetaSubstFailure (lazy "Unbound variable found in deliftaux"))
)
| C.Var (uri,exp_named_subst) ->
let exp_named_subst' =
with CicUtil.Subst_not_found _ ->
(* see the top level invariant *)
if (i = n) then
- raise (MetaSubstFailure (sprintf
+ raise (MetaSubstFailure (lazy (sprintf
"Cannot unify the metavariable ?%d with a term that has as subterm %s in which the same metavariable occurs (occur check)"
- i (ppterm subst t)))
+ i (ppterm subst t))))
else
begin
(* I do not consider the term associated to ?i in subst since *)
(List.map
(function Some t -> ppterm subst t | None -> "_") l
)))); *)
- raise (Uncertain (sprintf
+ raise (Uncertain (lazy (sprintf
"Error trying to abstract %s over [%s]: the algorithm only tried to abstract over bound variables"
(ppterm subst t)
(String.concat "; "
(List.map
(function Some t -> ppterm subst t | None -> "_")
- l))))
+ l)))))
in
let (metasenv, subst) = restrict subst !to_be_restricted metasenv in
res, metasenv, subst