let refine_term metasenv context uri term ugraph =
(* if benchmark then incr actual_refinements; *)
assert (uri=None);
- let metasenv, term =
- CicMkImplicit.expand_implicits metasenv [] context term in
debug_print (lazy (sprintf "TEST_INTERPRETATION: %s" (CicPp.ppterm term)));
try
let term', _, metasenv',ugraph1 =
(Ok (term', metasenv')),ugraph1
with
| CicRefine.Uncertain s ->
- debug_print (lazy ("UNCERTAIN!!! [" ^ s ^ "] " ^ CicPp.ppterm term)) ;
+ debug_print (lazy ("UNCERTAIN!!! [" ^ (Lazy.force s) ^ "] " ^ CicPp.ppterm term)) ;
Uncertain,ugraph
| CicRefine.RefineFailure msg ->
debug_print (lazy (sprintf "PRUNED!!!\nterm%s\nmessage:%s"
- (CicPp.ppterm term) (CicRefine.explain_error msg)));
+ (CicPp.ppterm term) (Lazy.force msg)));
Ko,ugraph
let refine_obj metasenv context uri obj ugraph =
assert (context = []);
- let metasenv, obj = CicMkImplicit.expand_implicits_in_obj metasenv [] obj in
debug_print (lazy (sprintf "TEST_INTERPRETATION: %s" (CicPp.ppobj obj))) ;
try
let obj', metasenv,ugraph = CicRefine.typecheck metasenv uri obj in
(Ok (obj', metasenv)),ugraph
with
| CicRefine.Uncertain s ->
- debug_print (lazy ("UNCERTAIN!!! [" ^ s ^ "] " ^ CicPp.ppobj obj)) ;
+ debug_print (lazy ("UNCERTAIN!!! [" ^ (Lazy.force s) ^ "] " ^ CicPp.ppobj obj)) ;
Uncertain,ugraph
| CicRefine.RefineFailure msg ->
debug_print (lazy (sprintf "PRUNED!!!\nterm%s\nmessage:%s"
- (CicPp.ppobj obj) (CicRefine.explain_error msg))) ;
+ (CicPp.ppobj obj) (Lazy.force msg))) ;
Ko,ugraph
let resolve (env: codomain_item Environment.t) (item: domain_item) ?(num = "") ?(args = []) () =
module Trivial =
struct
- exception Ambiguous_term of string
+ exception Ambiguous_term of string Lazy.t
exception Exit
module Callbacks =
struct
try
fst (Disambiguator.disambiguate_term ~dbd ~context ~metasenv ast
?initial_ugraph ~aliases ~universe:None)
- with Exit -> raise (Ambiguous_term term)
+ with Exit -> raise (Ambiguous_term (lazy term))
end