X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicReductionNaif.ml;h=04067ccbfdfbb27663920b6ca3c2e46c9309f3b5;hb=4cb4d286a1fdcb150c2848a9d21ac3486906c317;hp=4362006447266b1fea7578adca00e4c7e59fa4c4;hpb=e626927b4c1c77bdcd6b545203a0a9c17a9ff136;p=helm.git

diff --git a/helm/ocaml/cic_proof_checking/cicReductionNaif.ml b/helm/ocaml/cic_proof_checking/cicReductionNaif.ml
index 436200644..04067ccbf 100644
--- a/helm/ocaml/cic_proof_checking/cicReductionNaif.ml
+++ b/helm/ocaml/cic_proof_checking/cicReductionNaif.ml
@@ -31,7 +31,7 @@ let debug t env s =
  let rec debug_aux t i =
   let module C = Cic in
   let module U = UriManager in
-   CicPp.ppobj (C.Variable ("DEBUG", None, t, [])) ^ "\n" ^ i
+   CicPp.ppobj (C.Variable ("DEBUG", None, t, [], [])) ^ "\n" ^ i
  in
   if !fdebug = 0 then
    prerr_endline (s ^ "\n" ^ List.fold_right debug_aux (t::env) "")
@@ -57,12 +57,15 @@ let whd context =
 	  | None -> raise RelToHiddenHypothesis
        )
     | C.Var (uri,exp_named_subst) as t ->
-       (match CicEnvironment.get_cooked_obj ~trust:false uri with
+	let o,_ = 
+	  CicEnvironment.get_cooked_obj ~trust:false CicUniv.empty_ugraph uri
+	in
+       (match o with
            C.Constant _ -> raise ReferenceToConstant
          | C.CurrentProof _ -> raise ReferenceToCurrentProof
          | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
-         | C.Variable (_,None,_,_) -> if l = [] then t else C.Appl (t::l)
-         | C.Variable (_,Some body,_,_) ->
+         | C.Variable (_,None,_,_,_) -> if l = [] then t else C.Appl (t::l)
+         | C.Variable (_,Some body,_,_,_) ->
             whdaux l (CicSubstitution.subst_vars exp_named_subst body)
        )
     | C.Meta _ as t -> if l = [] then t else C.Appl (t::l)
@@ -80,12 +83,15 @@ let whd context =
     | C.Appl (he::tl) -> whdaux (tl@l) he
     | C.Appl [] -> raise (Impossible 1)
     | C.Const (uri,exp_named_subst) as t ->
-       (match CicEnvironment.get_cooked_obj ~trust:false uri with
-           C.Constant (_,Some body,_,_) ->
+	let o,_ = 
+	  CicEnvironment.get_cooked_obj ~trust:false CicUniv.empty_ugraph uri
+	in
+       (match o with
+           C.Constant (_,Some body,_,_,_) ->
             whdaux l (CicSubstitution.subst_vars exp_named_subst body)
          | C.Constant _ -> if l = [] then t else C.Appl (t::l)
          | C.Variable _ -> raise ReferenceToVariable
-         | C.CurrentProof (_,_,body,_,_) ->
+         | C.CurrentProof (_,_,body,_,_,_) ->
             whdaux l (CicSubstitution.subst_vars exp_named_subst body)
          | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
        )
@@ -120,8 +126,9 @@ let whd context =
             C.MutConstruct (_,_,j,_) -> whdaux l (List.nth pl (j-1))
           | C.Appl (C.MutConstruct (_,_,j,_) :: tl) ->
              let (arity, r) =
-              match CicEnvironment.get_obj mutind with
-                 C.InductiveDefinition (tl,ingredients,r) ->
+	       let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph mutind in
+              match o with
+                 C.InductiveDefinition (tl,ingredients,r,_) ->
                    let (_,_,arity,_) = List.nth tl i in
                     (arity,r)
                | _ -> raise WrongUriToInductiveDefinition
@@ -182,128 +189,219 @@ t in prerr_endline "DOPO WHD" ; flush stderr ; res
 ;;
 
 (* t1, t2 must be well-typed *)
-let are_convertible =
+let are_convertible c t1 t2 ugraph =
  let module U = UriManager in
- let rec aux context t1 t2 =
-  let aux2 t1 t2 =
+ let rec aux test_equality_only context t1 t2 ugraph =
+  let aux2 test_equality_only t1 t2 ugraph =
    (* this trivial euristic cuts down the total time of about five times ;-) *)
    (* this because most of the time t1 and t2 are "sintactically" the same   *)
    if t1 = t2 then
-    true
+    true,ugraph
    else
     begin
      let module C = Cic in
        match (t1,t2) with
-          (C.Rel n1, C.Rel n2) -> n1 = n2
+          (C.Rel n1, C.Rel n2) -> (n1 = n2),ugraph
         | (C.Var (uri1,exp_named_subst1), C.Var (uri2,exp_named_subst2)) ->
-            U.eq uri1 uri2 &&
+            let b = U.eq uri1 uri2 in
+	    if b then
              (try
                List.fold_right2
-                (fun (uri1,x) (uri2,y) b ->
-                  U.eq uri1 uri2 && aux context x y && b
-                ) exp_named_subst1 exp_named_subst2 true 
+                (fun (uri1,x) (uri2,y) (b,ugraph) ->
+                  (* FIXME: lazy! *)
+                  let b',ugraph' = aux test_equality_only context x y ugraph in
+                  (U.eq uri1 uri2 && b' && b),ugraph'
+                ) exp_named_subst1 exp_named_subst2 (true,ugraph) 
               with
-               Invalid_argument _ -> false
+               Invalid_argument _ -> false,ugraph
              )
+	    else
+	      false,ugraph
         | (C.Meta (n1,l1), C.Meta (n2,l2)) -> 
-            n1 = n2 &&
+            let b = n1 = n2 in
+	    if b then
              List.fold_left2
-              (fun b t1 t2 ->
-                b &&
-                 match t1,t2 with
+              (fun (b,ugraph) t1 t2 ->
+		if b then 
+                  match t1,t2 with
                     None,_
-                  | _,None  -> true
-                  | Some t1',Some t2' -> aux context t1' t2'
-              ) true l1 l2
-        | (C.Sort s1, C.Sort s2) -> true (*CSC da finire con gli universi *)
+                  | _,None  -> true,ugraph
+                  | Some t1',Some t2' -> 
+		      aux test_equality_only context t1' t2' ugraph
+		else
+		  false,ugraph
+              ) (true,ugraph) l1 l2
+	    else
+	      false,ugraph
+          (* TASSI: CONSTRAINTS *)
+	| (C.Sort (C.Type t1), C.Sort (C.Type t2)) when test_equality_only ->
+	    true,(CicUniv.add_eq t2 t1 ugraph)
+	  (* TASSI: CONSTRAINTS *)
+	| (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
+	    true,(CicUniv.add_ge t2 t1 ugraph)
+	  (* TASSI: CONSTRAINTS *)
+	| (C.Sort s1, C.Sort (C.Type _)) -> (not test_equality_only),ugraph
+	  (* TASSI: CONSTRAINTS *)
+        | (C.Sort s1, C.Sort s2) -> (s1 = s2),ugraph
         | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) ->
-           aux context s1 s2 &&
-            aux ((Some (name1, (C.Decl s1)))::context) t1 t2
+	    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.Lambda (name1,s1,t1), C.Lambda(_,s2,t2)) ->
-           aux context s1 s2 &&
-            aux ((Some (name1, (C.Decl s1)))::context) t1 t2
+           let b',ugraph' = aux test_equality_only 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)) ->
-           aux context s1 s2 &&
-            aux ((Some (name1, (C.Def (s1,None))))::context) t1 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'
+	   else
+	     false,ugraph
         | (C.Appl l1, C.Appl l2) ->
            (try
-             List.fold_right2 (fun  x y b -> aux context x y && b) l1 l2 true 
+             List.fold_right2
+               (fun  x y (b,ugraph) -> 
+		 if b then
+		   aux test_equality_only context x y ugraph
+	         else
+	           false,ugraph) l1 l2 (true,ugraph)
             with
-             Invalid_argument _ -> false
+             Invalid_argument _ -> false,ugraph
            )
         | (C.Const (uri1,exp_named_subst1), C.Const (uri2,exp_named_subst2)) ->
-            U.eq uri1 uri2 &&
+            let b' = U.eq uri1 uri2 in
+	    if b' then
              (try
                List.fold_right2
-                (fun (uri1,x) (uri2,y) b ->
-                  U.eq uri1 uri2 && aux context x y && b
-                ) exp_named_subst1 exp_named_subst2 true 
+                (fun (uri1,x) (uri2,y) (b,ugraph) ->
+		  if b && U.eq uri1 uri2 then
+		    aux test_equality_only context x y ugraph 
+		  else
+		    false,ugraph
+                ) exp_named_subst1 exp_named_subst2 (true,ugraph)
               with
-               Invalid_argument _ -> false
+               Invalid_argument _ -> false,ugraph
              )
+	    else
+	      false,ugraph
         | (C.MutInd (uri1,i1,exp_named_subst1),
            C.MutInd (uri2,i2,exp_named_subst2)
           ) ->
-            U.eq uri1 uri2 && i1 = i2 &&
+            let b' = U.eq uri1 uri2 && i1 = i2 in
+	    if b' then
              (try
                List.fold_right2
-                (fun (uri1,x) (uri2,y) b ->
-                  U.eq uri1 uri2 && aux context x y && b
-                ) exp_named_subst1 exp_named_subst2 true 
+                (fun (uri1,x) (uri2,y) (b,ugraph) ->
+                  if b && U.eq uri1 uri2 then
+		    aux test_equality_only context x y ugraph
+		  else
+		   false,ugraph
+                ) exp_named_subst1 exp_named_subst2 (true,ugraph)
               with
-               Invalid_argument _ -> false
+               Invalid_argument _ -> false,ugraph
              )
+	    else 
+	      false,ugraph
         | (C.MutConstruct (uri1,i1,j1,exp_named_subst1),
            C.MutConstruct (uri2,i2,j2,exp_named_subst2)
           ) ->
-            U.eq uri1 uri2 && i1 = i2 && j1 = j2 &&
+            let b' = U.eq uri1 uri2 && i1 = i2 && j1 = j2 in
+	    if b' then
              (try
                List.fold_right2
-                (fun (uri1,x) (uri2,y) b ->
-                  U.eq uri1 uri2 && aux context x y && b
-                ) exp_named_subst1 exp_named_subst2 true 
+                (fun (uri1,x) (uri2,y) (b,ugraph) ->
+		  if b && U.eq uri1 uri2 then
+		    aux test_equality_only context x y ugraph
+		  else
+		    false,ugraph
+                ) exp_named_subst1 exp_named_subst2 (true,ugraph)
               with
-               Invalid_argument _ -> false
+               Invalid_argument _ -> false,ugraph
              )
+	    else
+	      false,ugraph
         | (C.MutCase (uri1,i1,outtype1,term1,pl1),
            C.MutCase (uri2,i2,outtype2,term2,pl2)) -> 
-            U.eq uri1 uri2 && i1 = i2 && aux context outtype1 outtype2 &&
-             aux context term1 term2 &&
-             List.fold_right2 (fun x y b -> b && aux context x y) pl1 pl2 true
+            let b' = U.eq uri1 uri2 && i1 = i2 in
+	    if b' then
+             let b'',ugraph''=aux test_equality_only context 
+		 outtype1 outtype2 ugraph in
+	     if b'' then 
+	       let b''',ugraph'''= aux test_equality_only context 
+		   term1 term2 ugraph'' in
+	       List.fold_right2
+		 (fun x y (b,ugraph) -> 
+		   if b then
+		     aux test_equality_only context x y ugraph 
+		   else 
+		     false,ugraph)
+		 pl1 pl2 (true,ugraph''')
+	     else
+	       false,ugraph
+	    else
+	      false,ugraph
         | (C.Fix (i1,fl1), C.Fix (i2,fl2)) ->
            let tys =
             List.map (function (n,_,ty,_) -> Some (C.Name n,(C.Decl ty))) fl1
            in
-            i1 = i2 &&
+            if i1 = i2 then
              List.fold_right2
-              (fun (_,recindex1,ty1,bo1) (_,recindex2,ty2,bo2) b ->
-                b && recindex1 = recindex2 && aux context ty1 ty2 &&
-                 aux (tys@context) bo1 bo2)
-              fl1 fl2 true
+              (fun (_,recindex1,ty1,bo1) (_,recindex2,ty2,bo2) (b,ugraph) ->
+                if b && recindex1 = recindex2 then
+		  let b',ugraph' = aux test_equality_only context ty1 ty2 
+		      ugraph in
+		  if b' then
+		    aux test_equality_only (tys@context) bo1 bo2 ugraph'
+	          else
+	            false,ugraph
+	        else
+	          false,ugraph)
+	     fl1 fl2 (true,ugraph)
+	    else
+	      false,ugraph
         | (C.CoFix (i1,fl1), C.CoFix (i2,fl2)) ->
            let tys =
             List.map (function (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl1
            in
-            i1 = i2 &&
-             List.fold_right2
-              (fun (_,ty1,bo1) (_,ty2,bo2) b ->
-                b && aux context ty1 ty2 && aux (tys@context) bo1 bo2)
-              fl1 fl2 true
+            if i1 = i2 then
+              List.fold_right2
+              (fun (_,ty1,bo1) (_,ty2,bo2) (b,ugraph) ->
+		if b then
+		  let b',ugraph' = aux test_equality_only context ty1 ty2 
+		      ugraph in
+		  if b' then
+		    aux test_equality_only (tys@context) bo1 bo2 ugraph'
+	          else
+	            false,ugraph
+	        else
+	          false,ugraph)
+	     fl1 fl2 (true,ugraph)
+	    else
+	      false,ugraph
         | (C.Cast _, _) | (_, C.Cast _)
         | (C.Implicit _, _) | (_, C.Implicit _) ->
-           raise (Impossible 3) (* we don't trust our whd ;-) *)
-        | (_,_) -> false
+            assert false
+        | (_,_) -> false,ugraph
     end
   in
-   if aux2 t1 t2 then true
+   let b,ugraph' = aux2 test_equality_only t1 t2 ugraph in
+   if b then
+     b,ugraph'
    else
     begin
      debug t1 [t2] "PREWHD";
-     let t1' = whd context t1 
-     and t2' = whd context t2 in
+     let t1' = whd context t1 in
+     let t2' = whd context t2 in
       debug t1' [t2'] "POSTWHD";
-      aux2 t1' t2'
+      aux2 test_equality_only t1' t2' ugraph
     end
  in
-  aux
+  aux false c t1 t2 ugraph
 ;;