coercGraph.ml* moved from cic_unification to library

[helm.git] / helm / ocaml / cic_proof_checking / cicReduction.ml

diff --git a/helm/ocaml/cic_proof_checking/cicReduction.ml b/helm/ocaml/cic_proof_checking/cicReduction.ml
index 0229f23386bf39d0d0ed3a5cee7b8f1919c05760..7ba2cffbcfaa76298770ed8c19c5a5c369badadc 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicReduction.ml
+++ b/helm/ocaml/cic_proof_checking/cicReduction.ml
@@ -34,6 +34,7 @@ exception ReferenceToCurrentProof;;
 exception ReferenceToInductiveDefinition;;
 
 let debug = false
+let profile = false
 let debug_print s = if debug then prerr_endline (Lazy.force s)
 
 let fdebug = ref 1;;
@@ -510,20 +511,22 @@ if List.mem uri params then debug_print (lazy "---- OK2") ;
       unwind_aux m t          
   ;;
   
-let profiler_unwind = HExtlib.profile "are_convertible.unwind"
-  let unwind k e ens t =
-let foo () =
-   unwind' 0  k e ens t
-in
- profiler_unwind.HExtlib.profile foo ()
+  let unwind = unwind' 0;;
+
+(*
+  let unwind =
+   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
    let module S = CicSubstitution in 
    let rec reduce =
     function
-       (k, e, _, (C.Rel n as t), s) ->
+       (k, e, _, C.Rel n, s) ->
         let d =
          try
           Some (RS.from_env (List.nth e (n-1)))
@@ -574,14 +577,14 @@ in
            if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s)))
      | (k, e, _, (C.Sort _ as t), s) -> t (* s should be empty *)
      | (k, e, _, (C.Implicit _ as t), s) -> t (* s should be empty *)
-     | (k, e, ens, (C.Cast (te,ty) as t), s) ->
+     | (k, e, ens, C.Cast (te,ty), s) ->
         reduce (k, e, ens, te, s) (* s should be empty *)
      | (k, e, ens, (C.Prod _ as t), s) ->
          unwind k e ens t (* s should be empty *)
      | (k, e, ens, (C.Lambda (_,_,t) as t'), []) -> unwind k e ens t' 
      | (k, e, ens, C.Lambda (_,_,t), p::s) ->
          reduce (k+1, (RS.stack_to_env ~reduce ~unwind p)::e, ens, t,s)
-     | (k, e, ens, (C.LetIn (_,m,t) as t'), s) ->
+     | (k, e, ens, C.LetIn (_,m,t), s) ->
         let m' = RS.compute_to_env ~reduce ~unwind k e ens m in
          reduce (k+1, m'::e, ens, t, s)
      | (_, _, _, C.Appl [], _) -> assert false
@@ -638,7 +641,7 @@ in
      | (k, e, ens, (C.MutCase (mutind,i,_,term,pl) as t),s) ->
         let decofix =
          function
-            C.CoFix (i,fl) as t ->
+            C.CoFix (i,fl) ->
              let (_,_,body) = List.nth fl i in
               let body' =
                let counter = ref (List.length fl) in
@@ -798,9 +801,15 @@ module R = Reduction(ClosuresOnStackByValueFromEnvOrEnsStrategy);; OK 58.127s
 module R = Reduction(ClosuresOnStackByValueFromEnvOrEnsStrategy);;
 module U = UriManager;;
 
-let profiler_whd = HExtlib.profile "are_convertible.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 =
@@ -1006,8 +1015,7 @@ let are_convertible whd ?(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
@@ -1021,18 +1029,8 @@ let are_convertible whd ?(subst=[]) ?(metasenv=[])  =
            debug_print (lazy (CicPp.ppterm t2));
            debug_print (lazy (CicPp.ppterm (whd ~subst context t2)))
        | _ -> ()); *)
-     let t1' =
- let foo () =
-whd ?delta:(Some true) ?subst:(Some subst) context t1
- in
-  profiler_whd.HExtlib.profile foo ()
-in
-     let t2' =
- let foo () =
-whd ?delta:(Some true) ?subst:(Some subst) context t2
- in
-  profiler_whd.HExtlib.profile foo ()
-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
@@ -1063,19 +1061,23 @@ let _ =  are_convertible CicReductionNaif.whd ~subst context res rescsc CicUniv.
 
 let are_convertible = are_convertible whd
 
-let profiler_other_whd = HExtlib.profile "~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
   let t = whd ~delta ~subst ctx term in
   let aux = normalize ~delta ~subst in
   let decl name t = Some (name, C.Decl t) in
-  let def  name t = Some (name, C.Def (t,None)) in
+  let def name t = Some (name, C.Def (t,None)) in
   match t with
   | C.Rel n -> t
   | C.Var (uri,exp_named_subst) ->