*** empty log message ***

[helm.git] / helm / ocaml / cic_unification / cicMetaSubst.ml

diff --git a/helm/ocaml/cic_unification/cicMetaSubst.ml b/helm/ocaml/cic_unification/cicMetaSubst.ml
index 768255a1493db265c087ecad4355b934d8354b19..614faf6df15f50d6af219ac90ccacf502afd04fb 100644 (file)
--- a/helm/ocaml/cic_unification/cicMetaSubst.ml
+++ b/helm/ocaml/cic_unification/cicMetaSubst.ml
@@ -47,7 +47,7 @@ let reset_counters () =
  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
@@ -64,7 +64,7 @@ context length: %d (avg = %.2f)
   ((float !metasenv_length) /. (float !apply_subst_metasenv_counter))
   !context_length
   ((float !context_length) /. (float !apply_subst_context_counter))
-  )*)
+  ))*)
 
 
 
@@ -232,17 +232,6 @@ let apply_subst_gen ~appl_fun subst term =
 ;;
 
 let apply_subst =
-(* CSC: old code that never performs beta reduction
-  let appl_fun um_aux he tl =
-    let tl' = List.map um_aux tl in
-      begin
-       match um_aux he with
-          Cic.Appl l -> Cic.Appl (l@tl')
-        | he' -> Cic.Appl (he'::tl')
-      end
-  in
-  apply_subst_gen ~appl_fun
-*)
   let appl_fun um_aux he tl =
     let tl' = List.map um_aux tl in
     let t' =
@@ -252,18 +241,7 @@ let apply_subst =
     in
      begin
       match he with
-         Cic.Meta (m,_) ->
-          let rec beta_reduce =
-           function
-              (Cic.Appl (Cic.Lambda (_,_,t)::he'::tl')) ->
-                let he'' = CicSubstitution.subst he' t in
-                 if tl' = [] then
-                  he''
-                 else
-                  beta_reduce (Cic.Appl(he''::tl'))
-            | t -> t
-          in
-           beta_reduce t'
+         Cic.Meta (m,_) -> CicReduction.head_beta_reduce t'
        | _ -> t'
      end
   in
@@ -356,7 +334,7 @@ let ppsubst subst =
 
 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) ->
@@ -595,10 +573,10 @@ let rec restrict subst to_be_restricted metasenv =
             (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
@@ -614,8 +592,8 @@ let delift n subst context metasenv l t =
    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
@@ -738,14 +716,14 @@ let delift n subst context metasenv l t =
       (* 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)
@@ -908,5 +886,5 @@ let fpp_gen ppf s =
 
 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)