parameter sintax added to axiom statement

[helm.git] / helm / software / components / cic_proof_checking / cicReduction.ml

diff --git a/helm/software/components/cic_proof_checking/cicReduction.ml b/helm/software/components/cic_proof_checking/cicReduction.ml
index 5e02fdbaaa391d00705586a0df49d61d60b79a2a..5c5db75b4bb88f93ef54640b0952e77067338567 100644 (file)
--- a/helm/software/components/cic_proof_checking/cicReduction.ml
+++ b/helm/software/components/cic_proof_checking/cicReduction.ml
@@ -34,6 +34,37 @@ exception ReferenceToVariable;;
 exception ReferenceToCurrentProof;;
 exception ReferenceToInductiveDefinition;;
 
+let ndebug = ref false;;
+let indent = ref "";;
+let times = ref [];;
+let pp s =
+ if !ndebug then
+  prerr_endline (Printf.sprintf "%-20s" !indent ^ " " ^ Lazy.force s)
+;;
+let inside c =
+ if !ndebug then
+  begin
+   let time1 = Unix.gettimeofday () in
+   indent := !indent ^ String.make 1 c;
+   times := time1 :: !times;
+   prerr_endline ("{{{" ^ !indent ^ " ")
+  end
+;;
+let outside ok =
+ if !ndebug then
+  begin
+   let time2 = Unix.gettimeofday () in
+   let time1 =
+    match !times with time1::tl -> times := tl; time1 | [] -> assert false in
+   prerr_endline ("}}} " ^ string_of_float (time2 -. time1));
+   if not ok then prerr_endline "exception raised!";
+   try
+    indent := String.sub !indent 0 (String.length !indent -1)
+   with
+    Invalid_argument _ -> indent := "??"; ()
+ end
+;;
+
 let debug = false
 let profile = false
 let debug_print s = if debug then prerr_endline (Lazy.force s)
@@ -805,6 +836,8 @@ let (===) x y =
 let are_convertible whd ?(subst=[]) ?(metasenv=[])  =
  let heuristic = ref true in
  let rec aux test_equality_only context t1 t2 ugraph =
+ (*D*)inside 'B'; try let rc = 
+  pp (lazy (CicPp.ppterm t1 ^ " vs " ^ CicPp.ppterm t2));
   let rec aux2 test_equality_only t1 t2 ugraph =
 
    (* this trivial euristic cuts down the total time of about five times ;-) *)
@@ -869,19 +902,16 @@ prerr_endline ("%%%%%%: " ^ CicPp.ppterm term' ^ " <==> " ^ CicPp.ppterm t1);
 *)
                aux test_equality_only context t1 term' ugraph
             with  CicUtil.Subst_not_found _ -> false,ugraph)
-          (* TASSI: CONSTRAINTS *)
-        | (C.Sort (C.Type t1), C.Sort (C.Type t2)) when test_equality_only ->
-            (try
-              true,(CicUniv.add_eq t2 t1 ugraph)
-             with CicUniv.UniverseInconsistency _ -> false,ugraph)
-          (* TASSI: CONSTRAINTS *)
-        | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
-            (try
-              true,(CicUniv.add_ge t2 t1 ugraph)
-             with CicUniv.UniverseInconsistency _ -> false,ugraph)
-          (* TASSI: CONSTRAINTS *)
-        | (C.Sort s1, C.Sort (C.Type _)) -> (not test_equality_only),ugraph
-          (* TASSI: CONSTRAINTS *)
+        | (C.Sort (C.CProp t1|C.Type t1), C.Sort (C.CProp t2|C.Type t2)) 
+          when test_equality_only ->
+            (try true,(CicUniv.add_eq t2 t1 ugraph)
+            with CicUniv.UniverseInconsistency _ -> false,ugraph)
+        | (C.Sort (C.CProp t1|C.Type t1), C.Sort (C.CProp t2|C.Type t2))
+          when not test_equality_only ->
+            (try true,(CicUniv.add_ge t2 t1 ugraph)
+            with CicUniv.UniverseInconsistency _ -> false,ugraph)
+        | (C.Sort s1, C.Sort (C.Type _))
+        | (C.Sort s1, C.Sort (C.CProp _)) -> (not test_equality_only),ugraph
         | (C.Sort s1, C.Sort s2) -> (s1 = s2),ugraph
         | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) ->
             let b',ugraph' = aux true context s1 s2 ugraph in
@@ -909,13 +939,18 @@ prerr_endline ("%%%%%%: " ^ CicPp.ppterm term' ^ " <==> " ^ CicPp.ppterm t1);
            else
              false,ugraph
         | (C.Appl l1, C.Appl l2) ->
+           let b, ugraph = 
+             aux test_equality_only context (List.hd l1) (List.hd l2) ugraph
+           in
+           if not b then false, ugraph
+           else
            (try
              List.fold_right2
                (fun  x y (b,ugraph) -> 
                  if b then
-                   aux test_equality_only context x y ugraph
+                   aux true context x y ugraph
                  else
-                   false,ugraph) l1 l2 (true,ugraph)
+                   false,ugraph) (List.tl l1) (List.tl l2) (true,ugraph)
             with
              Invalid_argument _ -> false,ugraph
            )
@@ -978,7 +1013,7 @@ prerr_endline ("%%%%%%: " ^ CicPp.ppterm term' ^ " <==> " ^ CicPp.ppterm t1);
              let b'',ugraph''=aux test_equality_only context 
                  outtype1 outtype2 ugraph in
              if b'' then 
-               let b''',ugraph'''= aux test_equality_only context 
+               let b''',ugraph'''= aux true context 
                    term1 term2 ugraph'' in
                List.fold_right2
                  (fun x y (b,ugraph) -> 
@@ -1063,7 +1098,7 @@ prerr_endline ("PREWHD: " ^ CicPp.ppterm t1 ^ " <===> " ^ CicPp.ppterm t2);
    let t2' = whd ?delta:(Some true) ?subst:(Some subst) context t2 in
     debug t1' [t2'] "POSTWHD";
 *)
-let rec convert_machines ugraph =
+let rec convert_machines test_equality_only ugraph =
  function
     [] -> true,ugraph
   | ((k1,env1,ens1,h1,s1),(k2,env2,ens2,h2,s2))::tl ->
@@ -1088,11 +1123,11 @@ let rec convert_machines ugraph =
        in
         match problems with
            None -> false,ugraph
-         | Some problems -> convert_machines ugraph problems
+         | Some problems -> convert_machines true ugraph problems
       else
        res
 in
- convert_machines ugraph
+ convert_machines test_equality_only ugraph
   [R.reduce ~delta:true ~subst context (0,[],[],t1,[]),
    R.reduce ~delta:true ~subst context (0,[],[],t2,[])]
 (*prerr_endline ("POSTWH: " ^ CicPp.ppterm t1' ^ " <===> " ^ CicPp.ppterm t2');*)
@@ -1100,6 +1135,7 @@ in
     aux2 test_equality_only t1' t2' ugraph
 *)
 end
+ (*D*)in outside true; rc with exc -> outside false; raise exc
  in
   aux false (*c t1 t2 ugraph *)
 ;;