universes are written with the URI inside objects, this allows

[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 af5564d0754c32c39a594bdef0ad2ba6552dd298..11fd5123560b1f411bd8a77832c30a6db7150f01 100644 (file)
--- a/helm/software/components/cic_proof_checking/cicReduction.ml
+++ b/helm/software/components/cic_proof_checking/cicReduction.ml
@@ -451,7 +451,8 @@ debug_print (lazy ("%%%%%UWVAR " ^ String.concat " ; " (List.map (function (uri,
        | C.Cast (te,ty) -> C.Cast (unwind_aux m te, unwind_aux m ty) (*CSC ???*)
        | C.Prod (n,s,t) -> C.Prod (n, unwind_aux m s, unwind_aux (m + 1) t)
        | C.Lambda (n,s,t) -> C.Lambda (n, unwind_aux m s, unwind_aux (m + 1) t)
-       | C.LetIn (n,s,t) -> C.LetIn (n, unwind_aux m s, unwind_aux (m + 1) t)
+       | C.LetIn (n,s,ty,t) ->
+          C.LetIn (n, unwind_aux m s, unwind_aux m ty, unwind_aux (m + 1) t)
        | C.Appl l -> C.Appl (List.map (unwind_aux m) l)
        | C.Const (uri,exp_named_subst) ->
           let params =
@@ -596,19 +597,21 @@ if List.mem uri params then debug_print (lazy "---- OK2") ;
     function
        (k, e, _, C.Rel n, s) as config ->
         let config' =
-         try
-          Some (RS.from_env (List.nth e (n-1)))
-         with
-          Failure _ ->
-           try
-            begin
-             match List.nth context (n - 1 - k) with
-                None -> assert false
-              | Some (_,C.Decl _) -> None
-              | Some (_,C.Def (x,_)) -> Some (0,[],[],S.lift (n - k) x,[])
-            end
-           with
-            Failure _ -> None
+         if not delta then None
+         else
+          try
+           Some (RS.from_env (List.nth e (n-1)))
+          with
+           Failure _ ->
+            try
+             begin
+              match List.nth context (n - 1 - k) with
+                 None -> assert false
+               | Some (_,C.Decl _) -> None
+               | Some (_,C.Def (x,_)) -> Some (0,[],[],S.lift (n - k) x,[])
+             end
+            with
+             Failure _ -> None
         in
          (match config' with 
              Some (k',e',ens',t',s') -> reduce (k',e',ens',t',s'@s)
@@ -643,7 +646,7 @@ if List.mem uri params then debug_print (lazy "---- OK2") ;
      | (_, _, _, C.Lambda _, []) as config -> config
      | (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), 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
@@ -796,9 +799,10 @@ module R = Reduction
 module R = Reduction(ClosuresOnStackByValueFromEnvOrEnsStrategy);; OK 58.127s
 *)
 (*module R = Reduction(CallByValueByNameForUnwind);;*)
-module R = Reduction(CallByValueByNameForUnwind');;
+module RS = CallByValueByNameForUnwind';;
 (*module R = Reduction(CallByNameStrategy);;*)
 (*module R = Reduction(ClosuresOnStackByValueFromEnvOrEnsStrategy);;*)
+module R = Reduction(RS);;
 module U = UriManager;;
 
 let whd = R.whd
@@ -905,17 +909,21 @@ prerr_endline ("%%%%%%: " ^ CicPp.ppterm term' ^ " <==> " ^ CicPp.ppterm t1);
             else
               false,ugraph
         | (C.Lambda (name1,s1,t1), C.Lambda(_,s2,t2)) ->
-           let b',ugraph' = aux test_equality_only context s1 s2 ugraph in
+           let b',ugraph' = aux true context s1 s2 ugraph in
            if b' then
              aux test_equality_only ((Some (name1, (C.Decl s1)))::context) 
                t1 t2 ugraph'
            else
              false,ugraph
-        | (C.LetIn (name1,s1,t1), C.LetIn(_,s2,t2)) ->
+        | (C.LetIn (name1,s1,ty1,t1), C.LetIn(_,s2,ty2,t2)) ->
            let b',ugraph' = aux test_equality_only context s1 s2 ugraph in
            if b' then
-            aux test_equality_only
-             ((Some (name1, (C.Def (s1,None))))::context) t1 t2 ugraph'
+            let b',ugraph = aux test_equality_only context ty1 ty2 ugraph in
+            if b' then
+             aux test_equality_only
+              ((Some (name1, (C.Def (s1,ty1))))::context) t1 t2 ugraph'
+            else
+              false,ugraph
            else
              false,ugraph
         | (C.Appl l1, C.Appl l2) ->
@@ -1067,11 +1075,48 @@ begin
    (* heuristic := false; *)
    debug t1 [t2] "PREWHD";
 (*prerr_endline ("PREWHD: " ^ CicPp.ppterm t1 ^ " <===> " ^ CicPp.ppterm t2);*)
+(*
+prerr_endline ("PREWHD: " ^ CicPp.ppterm t1 ^ " <===> " ^ CicPp.ppterm t2);
    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";
+*)
+let rec convert_machines ugraph =
+ function
+    [] -> true,ugraph
+  | ((k1,env1,ens1,h1,s1),(k2,env2,ens2,h2,s2))::tl ->
+     let (b,ugraph) as res =
+      aux2 test_equality_only
+       (R.unwind (k1,env1,ens1,h1,[])) (R.unwind (k2,env2,ens2,h2,[])) ugraph
+     in
+      if b then
+       let problems =
+        try
+         Some
+          (List.combine
+            (List.map
+              (fun si-> R.reduce ~delta:false ~subst context(RS.from_stack si))
+              s1)
+            (List.map
+              (fun si-> R.reduce ~delta:false ~subst context(RS.from_stack si))
+              s2)
+          @ tl)
+        with
+         Invalid_argument _ -> None
+       in
+        match problems with
+           None -> false,ugraph
+         | Some problems -> convert_machines ugraph problems
+      else
+       res
+in
+ convert_machines 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');*)
+(*
     aux2 test_equality_only t1' t2' ugraph
+*)
 end
  in
   aux false (*c t1 t2 ugraph *)
@@ -1131,7 +1176,7 @@ let rec normalize ?(delta=true) ?(subst=[]) ctx term =
   | C.Lambda (n,s,t) -> 
       let s' = aux ctx s in
       C.Lambda (n, s', aux ((decl n s')::ctx) t)
-  | C.LetIn (n,s,t) ->
+  | C.LetIn (n,s,_,t) ->
       (* the term is already in weak head normal form *)
       assert false
   | C.Appl (h::l) -> C.Appl (h::(List.map (aux ctx) l))