CicRefine.type_of_aux' metasenv context term ugraph in
(Ok (term', metasenv')),ugraph1
with
- | CicRefine.Uncertain _ ->
- debug_print ("UNCERTAIN!!! " ^ CicPp.ppterm term) ;
+ | CicRefine.Uncertain s ->
+ debug_print ("UNCERTAIN!!! [" ^ s ^ "] " ^ CicPp.ppterm term) ;
Uncertain,ugraph
| CicRefine.RefineFailure msg ->
debug_print (sprintf "PRUNED!!!\nterm%s\nmessage:%s"
Cic.MutConstruct (uri, i, j, mk_subst uris)
| Cic.Meta _ | Cic.Implicit _ as t ->
(*
- prerr_endline (sprintf
+ debug_print (sprintf
"Warning: %s must be instantiated with _[%s] but we do not enforce it"
(CicPp.ppterm t)
(String.concat "; "
CicEnvironment.CircularDependency _ ->
raise DisambiguateChoices.Invalid_choice))
| CicAst.Implicit -> Cic.Implicit None
+ | CicAst.UserInput -> Cic.Implicit (Some `Hole)
+(* | CicAst.UserInput -> assert false*)
| CicAst.Num (num, i) -> resolve env (Num i) ~num ()
| CicAst.Meta (index, subst) ->
let cic_subst =
| CicAst.Sort `CProp -> Cic.Sort Cic.CProp
| CicAst.Symbol (symbol, instance) ->
resolve env (Symbol (symbol, instance)) ()
- | CicAst.UserInput -> assert false
and aux_option loc context = function
| None -> Cic.Implicit (Some `Type)
| Some term -> aux loc context term
try
CicUtil.term_of_uri uri
with exn ->
- prerr_endline uri;
- prerr_endline (Printexc.to_string exn);
+ debug_print uri;
+ debug_print (Printexc.to_string exn);
assert false
in
fun _ _ _ -> term))
(fun dom_item ->
try
let len = List.length (lookup_choices dom_item) in
- prerr_endline (sprintf "BENCHMARK %s: %d"
+ debug_print (sprintf "BENCHMARK %s: %d"
(string_of_domain_item dom_item) len);
len
with No_choices _ -> 0)
(*
(if benchmark then
let res_size = List.length res in
- prerr_endline (sprintf
+ debug_print (sprintf
("BENCHMARK: %d/%d refinements performed, domain size %d, interps %d, k %.2f\n" ^^
"BENCHMARK: estimated %.2f")
!actual_refinements !max_refinements !domain_size res_size