X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicReductionMachine.ml;h=0610504c4faeaa389c8c65e6ea804acb1542d6fe;hb=4cb4d286a1fdcb150c2848a9d21ac3486906c317;hp=e963ddce9b5062a941a45ff2b6e3cf44c89b8707;hpb=c5d5bf37b1e4c4b9b499ed2cbfe27cf2ec181944;p=helm.git

diff --git a/helm/ocaml/cic_proof_checking/cicReductionMachine.ml b/helm/ocaml/cic_proof_checking/cicReductionMachine.ml
index e963ddce9..0610504c4 100644
--- a/helm/ocaml/cic_proof_checking/cicReductionMachine.ml
+++ b/helm/ocaml/cic_proof_checking/cicReductionMachine.ml
@@ -38,7 +38,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) "")
@@ -353,9 +353,12 @@ prerr_endline ("%%%%%UWVAR " ^ String.concat " ; " (List.map (function (uri,t) -
           CicSubstitution.lift m (RS.from_ens (List.assq uri ens))
          else
           let params =
-           (match CicEnvironment.get_obj uri with
+	    let o,_ = 
+	      CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
+	    in
+           (match o with
                C.Constant _ -> raise ReferenceToConstant
-             | C.Variable (_,_,_,params) -> params
+             | C.Variable (_,_,_,params,_) -> params
              | C.CurrentProof _ -> raise ReferenceToCurrentProof
              | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
            )
@@ -382,10 +385,13 @@ prerr_endline ("%%%%%UWVAR " ^ String.concat " ; " (List.map (function (uri,t) -
        | C.Appl l -> C.Appl (List.map (unwind_aux m) l)
        | C.Const (uri,exp_named_subst) ->
           let params =
-           (match CicEnvironment.get_obj uri with
-               C.Constant (_,_,_,params) -> params
+	    let o,_ = 
+	      CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
+	    in
+           (match o with
+               C.Constant (_,_,_,params,_) -> params
              | C.Variable _ -> raise ReferenceToVariable
-             | C.CurrentProof (_,_,_,_,params) -> params
+             | C.CurrentProof (_,_,_,_,params,_) -> params
              | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
            )
           in
@@ -395,11 +401,14 @@ prerr_endline ("%%%%%UWVAR " ^ String.concat " ; " (List.map (function (uri,t) -
             C.Const (uri,exp_named_subst')
        | C.MutInd (uri,i,exp_named_subst) ->
           let params =
-           (match CicEnvironment.get_obj uri with
+	    let o,_ = 
+	      CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
+	    in
+           (match o with
                C.Constant _ -> raise ReferenceToConstant
              | C.Variable _ -> raise ReferenceToVariable
              | C.CurrentProof _ -> raise ReferenceToCurrentProof
-             | C.InductiveDefinition (_,params,_) -> params
+             | C.InductiveDefinition (_,params,_,_) -> params
            )
           in
            let exp_named_subst' =
@@ -408,11 +417,14 @@ prerr_endline ("%%%%%UWVAR " ^ String.concat " ; " (List.map (function (uri,t) -
             C.MutInd (uri,i,exp_named_subst')
        | C.MutConstruct (uri,i,j,exp_named_subst) ->
           let params =
-           (match CicEnvironment.get_obj uri with
+	    let o,_ = 
+	      CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
+	    in
+           (match o with
                C.Constant _ -> raise ReferenceToConstant
              | C.Variable _ -> raise ReferenceToVariable
              | C.CurrentProof _ -> raise ReferenceToCurrentProof
-             | C.InductiveDefinition (_,params,_) -> params
+             | C.InductiveDefinition (_,params,_,_) -> params
            )
           in
            let exp_named_subst' =
@@ -498,7 +510,7 @@ if List.mem uri params then prerr_endline "---- OK2" ;
    unwind' 0 
   ;;
   
-  let reduce context : config -> Cic.term = 
+  let reduce ?(subst = []) context : config -> Cic.term = 
    let module C = Cic in
    let module S = CicSubstitution in 
    let rec reduce =
@@ -530,21 +542,28 @@ if List.mem uri params then prerr_endline "---- OK2" ;
          if List.exists (function (uri',_) -> UriManager.eq uri' uri) ens then
           reduce (0, [], [], RS.from_ens (List.assq uri ens), s)
          else
-          (match CicEnvironment.get_obj uri with
+          ( let o,_ = 
+	      CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
+	    in
+            match o with
               C.Constant _ -> raise ReferenceToConstant
             | C.CurrentProof _ -> raise ReferenceToCurrentProof
             | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
-            | C.Variable (_,None,_,_) ->
+            | C.Variable (_,None,_,_,_) ->
                let t' = unwind k e ens t in
                 if s = [] then t' else
                  C.Appl (t'::(RS.from_stack_list ~unwind s))
-            | C.Variable (_,Some body,_,_) ->
+            | C.Variable (_,Some body,_,_,_) ->
                let ens' = push_exp_named_subst k e ens exp_named_subst in
                 reduce (0, [], ens', body, s)
           )
-     | (k, e, ens, (C.Meta _ as t), s) ->
-        let t' = unwind k e ens t in
-         if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s))
+     | (k, e, ens, (C.Meta (n,l) as t), s) ->
+        (try 
+	   let (_, term,_) = CicUtil.lookup_subst n subst in
+           reduce (k, e, ens,CicSubstitution.lift_meta l term,s)
+	 with  CicUtil.Subst_not_found _ ->
+           let t' = unwind k e ens t 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) ->
@@ -581,16 +600,19 @@ if List.mem uri params then prerr_endline "---- OK2" ;
          C.Appl (List.append (List.map (unwind k e ens) l) s)
   *)
      | (k, e, ens, (C.Const (uri,exp_named_subst) as t), s) ->
-        (match CicEnvironment.get_obj uri with
-            C.Constant (_,Some body,_,_) ->
+        (let o,_ = 
+	   CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
+	 in
+	  match o with
+            C.Constant (_,Some body,_,_,_) ->
              let ens' = push_exp_named_subst k e ens exp_named_subst in
               (* constants are closed *)
               reduce (0, [], ens', body, s) 
-          | C.Constant (_,None,_,_) ->
+          | C.Constant (_,None,_,_,_) ->
              let t' = unwind k e ens t in
               if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s))
           | C.Variable _ -> raise ReferenceToVariable
-          | C.CurrentProof (_,_,body,_,_) ->
+          | C.CurrentProof (_,_,body,_,_,_) ->
              let ens' = push_exp_named_subst k e ens exp_named_subst in
               (* constants are closed *)
               reduce (0, [], ens', body, s)
@@ -636,11 +658,14 @@ if List.mem uri params then prerr_endline "---- OK2" ;
               reduce (k, e, ens, (List.nth pl (j-1)), s)
            | C.Appl (C.MutConstruct (_,_,j,_) :: tl) ->
               let (arity, r) =
-               match CicEnvironment.get_obj mutind with
-                  C.InductiveDefinition (tl,ingredients,r) ->
-                    let (_,_,arity,_) = List.nth tl i in
-                     (arity,r)
-                | _ -> raise WrongUriToInductiveDefinition
+		let o,_ = 
+		  CicEnvironment.get_cooked_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
               in
                let ts =
                 let num_to_eat = r in
@@ -722,10 +747,22 @@ if List.mem uri params then prerr_endline "---- OK2" ;
      | (uri,t)::tl ->
          push_exp_named_subst k e ((uri,RS.to_ens (unwind k e ens t))::ens) tl
    in
-    reduce
+     reduce 
   ;;
-  
-  let rec whd context t = reduce context (0, [], [], t, []);;
+  (*
+  let rec whd context t = 
+    try 
+      reduce context (0, [], [], t, [])
+    with Not_found -> 
+      prerr_endline (CicPp.ppterm t) ; 
+      raise Not_found
+  ;;
+  *)
+
+  let rec whd ?(subst=[]) context t = 
+    reduce ~subst context (0, [], [], t, [])
+  ;;
+
   
 (* DEBUGGING ONLY
 let whd context t =
@@ -765,148 +802,235 @@ module R = Reduction
  ClosuresOnStackByValueFromEnvOrEnsByNameOnConstantsStrategy;;
 *)
 module R = Reduction(ClosuresOnStackByValueFromEnvOrEnsStrategy);;
+module U = UriManager;;
 
 let whd = R.whd;;
 
+  (* mimic ocaml (<< 3.08) "=" behaviour. Tests physical equality first then
+    * fallbacks to structural equality *)
+let (===) x y = (Pervasives.compare x y = 0)
+
 (* t1, t2 must be well-typed *)
-let are_convertible =
- let module U = UriManager in
- let rec aux test_equality_only context t1 t2 =
-  let aux2 test_equality_only t1 t2 =
+let are_convertible ?(subst=[]) ?(metasenv=[])  =
+ 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
+   if t1 === t2 then
+     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 &&
+            if U.eq uri1 uri2 then
              (try
                List.fold_right2
-                (fun (uri1,x) (uri2,y) b ->
-                  U.eq uri1 uri2 && aux test_equality_only context x y && b
-                ) exp_named_subst1 exp_named_subst2 true 
+                (fun (uri1,x) (uri2,y) (b,ugraph) ->
+                  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
              )
-        | (C.Meta (n1,l1), C.Meta (n2,l2)) -> 
-            n1 = n2 &&
-             List.fold_left2
-              (fun b t1 t2 ->
-                b &&
-                 match t1,t2 with
-                    None,_
-                  | _,None  -> true
-                  | Some t1',Some t2' -> aux test_equality_only context t1' t2'
-              ) true l1 l2
-	  (* TASSI: CONSTRAINTS *)
+	    else
+	      false,ugraph
+        | (C.Meta (n1,l1), C.Meta (n2,l2)) ->
+	    if n1 = n2 then
+	      let b2, ugraph1 = 
+		let l1 = CicUtil.clean_up_local_context subst metasenv n1 l1 in
+		let l2 = CicUtil.clean_up_local_context subst metasenv n2 l2 in
+		  List.fold_left2
+		    (fun (b,ugraph) t1 t2 ->
+		       if b then 
+			 match t1,t2 with
+			     None,_
+			   | _,None  -> true,ugraph
+			   | Some t1',Some t2' -> 
+			       aux test_equality_only context t1' t2' ugraph
+		       else
+			 false,ugraph
+		    ) (true,ugraph) l1 l2
+	      in
+		if b2 then true,ugraph1 else false,ugraph 
+	    else
+	      false,ugraph
+          (* TASSI: CONSTRAINTS *)
 	| (C.Sort (C.Type t1), C.Sort (C.Type t2)) when test_equality_only ->
-	    CicUniv.add_eq t2 t1
+	    true,(CicUniv.add_eq t2 t1 ugraph)
 	  (* TASSI: CONSTRAINTS *)
 	| (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
-	    CicUniv.add_ge t2 t1
+	    true,(CicUniv.add_ge t2 t1 ugraph)
 	  (* TASSI: CONSTRAINTS *)
-	| (C.Sort s1, C.Sort (C.Type _)) -> not test_equality_only
+	| (C.Sort s1, C.Sort (C.Type _)) -> (not test_equality_only),ugraph
 	  (* TASSI: CONSTRAINTS *)
-        | (C.Sort s1, C.Sort s2) -> s1 = s2
-	| (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) ->
-           aux true context s1 s2 &&
-            aux test_equality_only ((Some (name1, (C.Decl s1)))::context) t1 t2
+        | (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
+	    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 test_equality_only context s1 s2 &&
-            aux test_equality_only ((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 test_equality_only context s1 s2 &&
+           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
+             ((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 test_equality_only context x y && b) l1 l2 true
+               (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 test_equality_only 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 test_equality_only 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 test_equality_only 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 test_equality_only context outtype1 outtype2 &&
-             aux test_equality_only context term1 term2 &&
-             List.fold_right2
-              (fun x y b -> b && aux test_equality_only 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 &&
+            let tys =
+              List.map (function (n,_,ty,_) -> Some (C.Name n,(C.Decl ty))) fl1
+            in
+            if i1 = i2 then
              List.fold_right2
-              (fun (_,recindex1,ty1,bo1) (_,recindex2,ty2,bo2) b ->
-                b && recindex1 = recindex2 &&
-                 aux test_equality_only context ty1 ty2 &&
-                 aux test_equality_only (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 test_equality_only context ty1 ty2 &&
-                 aux test_equality_only (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 _) ->
             assert false
-        | (_,_) -> false
+        | (_,_) -> false,ugraph
     end
   in
-   if aux2 test_equality_only t1 t2 then true
-   else
-    begin
+     begin
      debug t1 [t2] "PREWHD";
-     let t1' = whd context t1 in
-     let t2' = whd context t2 in
+     (* 
+     (match t1 with 
+	 Cic.Meta _ -> 
+	   prerr_endline (CicPp.ppterm t1);
+	   prerr_endline (CicPp.ppterm (whd ~subst context t1));
+	   prerr_endline (CicPp.ppterm t2);
+	   prerr_endline (CicPp.ppterm (whd ~subst context t2))
+       | _ -> ()); *)
+     let t1' = whd ~subst context t1 in
+     let t2' = whd ~subst context t2 in
       debug t1' [t2'] "POSTWHD";
-      aux2 test_equality_only t1' t2'
+      aux2 test_equality_only t1' t2' ugraph
     end
  in
-  aux false
+  aux false (*c t1 t2 ugraph *)
 ;;
+