metasenv_length := 0;
context_length := 0
let print_counters () =
- debug_print (Printf.sprintf
+ debug_print (lazy (Printf.sprintf
"apply_subst: %d
apply_subst_context: %d
apply_subst_metasenv: %d
((float !metasenv_length) /. (float !apply_subst_metasenv_counter))
!context_length
((float !context_length) /. (float !apply_subst_context_counter))
- )*)
+ ))*)
let ppcontext ?sep subst context = fst (ppcontext' ?sep subst context)
-let ppmetasenv ?(sep = "\n") metasenv subst =
+let ppmetasenv ?(sep = "\n") subst metasenv =
String.concat sep
(List.map
(fun (i, c, t) ->
(ppterm subst term)
in
(* DEBUG
- debug_print error_msg;
- debug_print ("metasenv = \n" ^ (ppmetasenv metasenv subst));
- debug_print ("subst = \n" ^ (ppsubst subst));
- debug_print ("context = \n" ^ (ppcontext subst context)); *)
+ debug_print (lazy error_msg);
+ debug_print (lazy ("metasenv = \n" ^ (ppmetasenv metasenv subst)));
+ debug_print (lazy ("subst = \n" ^ (ppsubst subst)));
+ debug_print (lazy ("context = \n" ^ (ppcontext subst context))); *)
raise (MetaSubstFailure error_msg)))
subst ([], [])
in
otherwise the occur check does not make sense *)
(*
- debug_print ("sto deliftando il termine " ^ (CicPp.ppterm t) ^ " rispetto
- al contesto locale " ^ (CicPp.ppterm (Cic.Meta(0,l))));
+ debug_print (lazy ("sto deliftando il termine " ^ (CicPp.ppterm t) ^ " rispetto
+ al contesto locale " ^ (CicPp.ppterm (Cic.Meta(0,l)))));
*)
let module S = CicSubstitution in
(* The reason is that our delift function is weaker than first *)
(* order (in the sense of alpha-conversion). See comment above *)
(* related to the delift function. *)
-(* debug_print "First Order UnificationFailure during delift" ;
-debug_print(sprintf
+(* debug_print (lazy "First Order UnificationFailure during delift") ;
+debug_print(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
- ))); *)
+ )))); *)
raise (Uncertain (sprintf
"Error trying to abstract %s over [%s]: the algorithm only tried to abstract over bound variables"
(ppterm subst t)
let fppsubst ppf subst = fpp_gen ppf (ppsubst subst)
let fppterm ppf term = fpp_gen ppf (CicPp.ppterm term)
-let fppmetasenv ppf metasenv = fpp_gen ppf (ppmetasenv metasenv [])
+let fppmetasenv ppf metasenv = fpp_gen ppf (ppmetasenv [] metasenv)