CicPp.ppobj (C.Variable ("DEBUG", None, t, [], [])) ^ "\n" ^ i
in
if !fdebug = 0 then
- debug_print (s ^ "\n" ^ List.fold_right debug_aux (t::env) "")
+ debug_print (lazy (s ^ "\n" ^ List.fold_right debug_aux (t::env) ""))
;;
module type Strategy =
)
| C.Var (uri,exp_named_subst) ->
(*
-debug_print ("%%%%%UWVAR " ^ String.concat " ; " (List.map (function (uri,t) -> UriManager.string_of_uri uri ^ " := " ^ CicPp.ppterm t) ens)) ;
+debug_print (lazy ("%%%%%UWVAR " ^ String.concat " ; " (List.map (function (uri,t) -> UriManager.string_of_uri uri ^ " := " ^ CicPp.ppterm t) ens))) ;
*)
if List.exists (function (uri',_) -> UriManager.eq uri' uri) ens then
CicSubstitution.lift m (RS.from_ens (List.assq uri ens))
| _::tl -> filter_and_lift already_instantiated tl
(*
| (uri,_)::tl ->
-debug_print ("---- SKIPPO " ^ UriManager.string_of_uri uri) ;
+debug_print (lazy ("---- SKIPPO " ^ UriManager.string_of_uri uri)) ;
if List.for_all (function (uri',_) -> not (UriManager.eq uri uri'))
-exp_named_subst' then debug_print "---- OK1" ;
-debug_print ("++++ uri " ^ UriManager.string_of_uri uri ^ " not in " ^ String.concat " ; " (List.map UriManager.string_of_uri params)) ;
-if List.mem uri params then debug_print "---- OK2" ;
+exp_named_subst' then debug_print (lazy "---- OK1") ;
+debug_print (lazy ("++++ uri " ^ UriManager.string_of_uri uri ^ " not in " ^ String.concat " ; " (List.map UriManager.string_of_uri params))) ;
+if List.mem uri params then debug_print (lazy "---- OK2") ;
filter_and_lift tl
*)
in
try
reduce context (0, [], [], t, [])
with Not_found ->
- debug_print (CicPp.ppterm t) ;
+ debug_print (lazy (CicPp.ppterm t)) ;
raise Not_found
;;
*)
let rescsc = CicReductionNaif.whd context t in
if not (CicReductionNaif.are_convertible context res rescsc) then
begin
- debug_print ("PRIMA: " ^ CicPp.ppterm t) ;
+ debug_print (lazy ("PRIMA: " ^ CicPp.ppterm t)) ;
flush stderr ;
- debug_print ("DOPO: " ^ CicPp.ppterm res) ;
+ debug_print (lazy ("DOPO: " ^ CicPp.ppterm res)) ;
flush stderr ;
- debug_print ("CSC: " ^ CicPp.ppterm rescsc) ;
+ debug_print (lazy ("CSC: " ^ CicPp.ppterm rescsc)) ;
flush stderr ;
CicReductionNaif.fdebug := 0 ;
let _ = CicReductionNaif.are_convertible context res rescsc in
(*
(match t1 with
Cic.Meta _ ->
- debug_print (CicPp.ppterm t1);
- debug_print (CicPp.ppterm (whd ~subst context t1));
- debug_print (CicPp.ppterm t2);
- debug_print (CicPp.ppterm (whd ~subst context t2))
+ debug_print (lazy (CicPp.ppterm t1));
+ debug_print (lazy (CicPp.ppterm (whd ~subst context t1)));
+ debug_print (lazy (CicPp.ppterm t2));
+ debug_print (lazy (CicPp.ppterm (whd ~subst context t2)))
| _ -> ()); *)
let t1' = whd ~subst context t1 in
let t2' = whd ~subst context t2 in
let s' = aux ctx s in
C.Lambda (n, s', aux ((decl n s')::ctx) t)
| C.LetIn (n,s,t) ->
- let s' = aux ctx s in
- C.LetIn (n, s, aux ((def n s')::ctx) t)
+ (* the term is already in weak head normal form *)
+ assert false
| C.Appl (h::l) -> C.Appl (h::(List.map (aux ctx) l))
| C.Appl [] -> assert false
| C.Const (uri,exp_named_subst) ->
List.map (fun (n,t) -> n,aux ctx t) exp_named_subst)
| C.MutCase (sp,i,outt,t,pl) ->
C.MutCase (sp,i, aux ctx outt, aux ctx t, List.map (aux ctx) pl)
+(*CSC: to be completed, I suppose *)
| C.Fix _ -> t
| C.CoFix _ -> t