X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicReduction.ml;h=813a589d603d7c2025d9cfb97686d10573e5064c;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=8b9a0d22e35bc4d2b7d36d70cb4a6291a2178604;hpb=219fb7c39077e9c82b3657ab067c176bb5b222ef;p=helm.git

diff --git a/helm/ocaml/cic_proof_checking/cicReduction.ml b/helm/ocaml/cic_proof_checking/cicReduction.ml
index 8b9a0d22e..813a589d6 100644
--- a/helm/ocaml/cic_proof_checking/cicReduction.ml
+++ b/helm/ocaml/cic_proof_checking/cicReduction.ml
@@ -33,7 +33,9 @@ exception ReferenceToVariable;;
 exception ReferenceToCurrentProof;;
 exception ReferenceToInductiveDefinition;;
 
-let debug_print = fun _ -> ()
+let debug = false
+let profile = false
+let debug_print s = if debug then prerr_endline (Lazy.force s)
 
 let fdebug = ref 1;;
 let debug t env s =
@@ -43,7 +45,7 @@ let debug t env s =
    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 =
@@ -349,7 +351,7 @@ module Reduction(RS : 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))
@@ -495,11 +497,11 @@ debug_print ("%%%%%UWVAR " ^ String.concat " ; " (List.map (function (uri,t) ->
         | _::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
@@ -509,9 +511,15 @@ if List.mem uri params then debug_print "---- OK2" ;
       unwind_aux m t          
   ;;
   
+  let unwind = unwind' 0;;
+
+(*
   let unwind =
-   unwind' 0 
+   let profiler_unwind = HExtlib.profile ~enable:profile "are_convertible.unwind" in
+    fun k e ens t ->
+     profiler_unwind.HExtlib.profile (unwind k e ens) t
   ;;
+*)
   
   let reduce ~delta ?(subst = []) context : config -> Cic.term = 
    let module C = Cic in
@@ -760,7 +768,7 @@ if List.mem uri params then debug_print "---- OK2" ;
     try 
       reduce context (0, [], [], t, [])
     with Not_found -> 
-      debug_print (CicPp.ppterm t) ; 
+      debug_print (lazy (CicPp.ppterm t)) ; 
       raise Not_found
   ;;
   *)
@@ -770,54 +778,45 @@ if List.mem uri params then debug_print "---- OK2" ;
   ;;
 
   
-(* DEBUGGING ONLY
-let whd context t =
- let res = whd context t in
- let rescsc = CicReductionNaif.whd context t in
-  if not (CicReductionNaif.are_convertible context res rescsc) then
-   begin
-    debug_print ("PRIMA: " ^ CicPp.ppterm t) ;
-    flush stderr ;
-    debug_print ("DOPO: " ^ CicPp.ppterm res) ;
-    flush stderr ;
-    debug_print ("CSC: " ^ CicPp.ppterm rescsc) ;
-    flush stderr ;
-CicReductionNaif.fdebug := 0 ;
-let _ =  CicReductionNaif.are_convertible context res rescsc in
-    assert false ;
-   end
-  else 
-   res
-;;
-*)
  end
 ;;
 
 
-(*
-module R = Reduction CallByNameStrategy;;
-module R = Reduction CallByValueStrategy;;
-module R = Reduction CallByValueStrategyByNameOnConstants;;
-module R = Reduction LazyCallByValueStrategy;;
-module R = Reduction LazyCallByValueStrategyByNameOnConstants;;
-module R = Reduction LazyCallByNameStrategy;;
+(* ROTTO = rompe l'unificazione poiche' riduce gli argomenti di un'applicazione
+           senza ridurre la testa
+module R = Reduction CallByNameStrategy;; OK 56.368s
+module R = Reduction CallByValueStrategy;; ROTTO
+module R = Reduction CallByValueStrategyByNameOnConstants;; ROTTO
+module R = Reduction LazyCallByValueStrategy;; ROTTO
+module R = Reduction LazyCallByValueStrategyByNameOnConstants;; ROTTO
+module R = Reduction LazyCallByNameStrategy;; OK 0m56.398s
 module R = Reduction
  LazyCallByValueByNameOnConstantsWhenFromStack_ByNameStrategyWhenFromEnvOrEns;;
-module R = Reduction ClosuresOnStackByValueFromEnvOrEnsStrategy;;
+ OK 59.058s
+module R = Reduction ClosuresOnStackByValueFromEnvOrEnsStrategy;; OK 58.583s
 module R = Reduction
- ClosuresOnStackByValueFromEnvOrEnsByNameOnConstantsStrategy;;
+ ClosuresOnStackByValueFromEnvOrEnsByNameOnConstantsStrategy;; OK 58.094s
+module R = Reduction(ClosuresOnStackByValueFromEnvOrEnsStrategy);; OK 58.127s
 *)
 module R = Reduction(ClosuresOnStackByValueFromEnvOrEnsStrategy);;
 module U = UriManager;;
 
-let whd = R.whd;;
+let whd = R.whd
+
+(*
+let whd =
+ let profiler_whd = HExtlib.profile ~enable:profile "are_convertible.whd" in
+  fun ?(delta=true) ?(subst=[]) context t ->
+   profiler_whd.HExtlib.profile (whd ~delta ~subst context) t
+*)
 
   (* mimic ocaml (<< 3.08) "=" behaviour. Tests physical equality first then
     * fallbacks to structural equality *)
-let (===) x y = (Pervasives.compare x y = 0)
+let (===) x y =
+  Pervasives.compare x y = 0
 
 (* t1, t2 must be well-typed *)
-let are_convertible ?(subst=[]) ?(metasenv=[])  =
+let are_convertible whd ?(subst=[]) ?(metasenv=[])  =
  let rec aux test_equality_only context t1 t2 ugraph =
   let aux2 test_equality_only t1 t2 ugraph =
 
@@ -1016,8 +1015,7 @@ let are_convertible ?(subst=[]) ?(metasenv=[])  =
             else
               false,ugraph
         | (C.Cast _, _) | (_, C.Cast _)
-        | (C.Implicit _, _) | (_, C.Implicit _) ->
-            assert false
+        | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
         | (_,_) -> false,ugraph
     end
   in
@@ -1026,13 +1024,13 @@ let are_convertible ?(subst=[]) ?(metasenv=[])  =
      (* 
      (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 t1' = whd ?delta:(Some true) ?subst:(Some subst) context t1 in
+     let t2' = whd ?delta:(Some true) ?subst:(Some subst) context t2 in
       debug t1' [t2'] "POSTWHD";
       aux2 test_equality_only t1' t2' ugraph
     end
@@ -1040,6 +1038,39 @@ let are_convertible ?(subst=[]) ?(metasenv=[])  =
   aux false (*c t1 t2 ugraph *)
 ;;
 
+(* DEBUGGING ONLY
+let whd ?(delta=true) ?(subst=[]) context t = 
+ let res = whd ~delta ~subst context t in
+ let rescsc = CicReductionNaif.whd ~delta ~subst context t in
+  if not (fst (are_convertible CicReductionNaif.whd ~subst context res rescsc CicUniv.empty_ugraph)) then
+   begin
+    debug_print (lazy ("PRIMA: " ^ CicPp.ppterm t)) ;
+    flush stderr ;
+    debug_print (lazy ("DOPO: " ^ CicPp.ppterm res)) ;
+    flush stderr ;
+    debug_print (lazy ("CSC: " ^ CicPp.ppterm rescsc)) ;
+    flush stderr ;
+fdebug := 0 ;
+let _ =  are_convertible CicReductionNaif.whd ~subst context res rescsc CicUniv.empty_ugraph in
+    assert false ;
+   end
+  else 
+   res
+;;
+*)
+
+let are_convertible = are_convertible whd
+
+let whd = R.whd
+
+(*
+let profiler_other_whd = HExtlib.profile ~enable:profile "~are_convertible.whd"
+let whd ?(delta=true) ?(subst=[]) context t = 
+ let foo () =
+  whd ~delta ~subst context t
+ in
+  profiler_other_whd.HExtlib.profile foo ()
+*)
 
 let rec normalize ?(delta=true) ?(subst=[]) ctx term =
   let module C = Cic in
@@ -1063,8 +1094,8 @@ let rec normalize ?(delta=true) ?(subst=[]) ctx term =
       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) ->
@@ -1076,6 +1107,7 @@ let rec normalize ?(delta=true) ?(subst=[]) ctx term =
         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