subst, menv
with CicUtil.Meta_not_found m ->
let names = names_of_context context in
- debug_print (
+ debug_print (lazy (
Printf.sprintf "Meta_not_found %d!: %s %s\n%s\n\n%s" m
(CicPp.pp t1 names) (CicPp.pp t2 names)
- (print_metasenv menv) (print_metasenv metasenv));
+ (print_metasenv menv) (print_metasenv metasenv)));
assert false
)
| _, C.Meta _ -> unif subst menv t s
(* Printf.printf "| unification %s %s\n" (CicPp.ppterm t1) (CicPp.ppterm t2); *)
let subst, menv, ug =
if not (is_simple_term t1) || not (is_simple_term t2) then (
- debug_print (
+ debug_print (lazy (
Printf.sprintf "NOT SIMPLE TERMS: %s %s"
- (CicPp.ppterm t1) (CicPp.ppterm t2));
+ (CicPp.ppterm t1) (CicPp.ppterm t2)));
CicUnification.fo_unif metasenv context t1 t2 ugraph
) else
unification_simple metasenv context t1 t2 ugraph
match head with
| C.Appl [C.MutInd (uri, _, _); ty; t1; t2]
when (UriManager.eq uri eq_uri) && (ok_types ty newmetas) ->
- debug_print (
- Printf.sprintf "OK: %s" (CicPp.ppterm term));
-(* debug_print ( *)
+ debug_print (lazy (
+ Printf.sprintf "OK: %s" (CicPp.ppterm term)));
+(* debug_print (lazy ( *)
(* Printf.sprintf "args: %s\n" *)
-(* (String.concat ", " (List.map CicPp.ppterm args))); *)
-(* debug_print ( *)
+(* (String.concat ", " (List.map CicPp.ppterm args)))); *)
+(* debug_print (lazy ( *)
(* Printf.sprintf "newmetas:\n%s\n" *)
-(* (print_metasenv newmetas)); *)
+(* (print_metasenv newmetas))); *)
let o = !Utils.compare_terms t1 t2 in
let w = compute_equality_weight ty t1 t2 in
let proof = BasicProof p in
let rec aux newmeta = function
| [] -> [], newmeta
| (term, termty)::tl ->
- debug_print (
+ debug_print (lazy (
Printf.sprintf "Examining: %s (%s)"
- (UriManager.string_of_uri (CicUtil.uri_of_term term))(* (CicPp.ppterm term) *) (CicPp.ppterm termty));
+ (UriManager.string_of_uri (CicUtil.uri_of_term term))(* (CicPp.ppterm term) *) (CicPp.ppterm termty)));
let res, newmeta =
match termty with
| C.Prod (name, s, t) ->
match head with
| C.Appl [C.MutInd (uri, _, _); ty; t1; t2]
when (iseq uri) && (ok_types ty newmetas) ->
- debug_print (
- Printf.sprintf "OK: %s" (CicPp.ppterm term));
+ debug_print (lazy (
+ Printf.sprintf "OK: %s" (CicPp.ppterm term)));
let o = !Utils.compare_terms t1 t2 in
let w = compute_equality_weight ty t1 t2 in
let proof = BasicProof p in
(List.fold_left
(fun l e ->
if List.exists (meta_convertibility_eq e) l then (
- debug_print (
- Printf.sprintf "NO!! %s already there!" (string_of_equality e));
+ debug_print (lazy (
+ Printf.sprintf "NO!! %s already there!" (string_of_equality e)));
l
)
else e::l)