X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicReductionNaif.ml;h=987f4b6edbd8bc932207aeee2f493b2ea8135986;hb=1c7fb836e2af4f2f3d18afd0396701f2094265ff;hp=e0ad91f59b2414c3c855fb07287edc0f0e341c88;hpb=0054d117ebed7924a96bcaadc9bcbbef9d372938;p=helm.git

diff --git a/helm/ocaml/cic_proof_checking/cicReductionNaif.ml b/helm/ocaml/cic_proof_checking/cicReductionNaif.ml
index e0ad91f59..987f4b6ed 100644
--- a/helm/ocaml/cic_proof_checking/cicReductionNaif.ml
+++ b/helm/ocaml/cic_proof_checking/cicReductionNaif.ml
@@ -31,37 +31,39 @@ 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
-   begin
-    print_endline (s ^ "\n" ^ List.fold_right debug_aux (t::env) "") ;
-    flush stdout
-   end
+   prerr_endline (s ^ "\n" ^ List.fold_right debug_aux (t::env) "")
 ;;
 
 exception Impossible of int;;
-exception ReferenceToDefinition;;
-exception ReferenceToAxiom;;
+exception ReferenceToConstant;;
 exception ReferenceToVariable;;
 exception ReferenceToCurrentProof;;
 exception ReferenceToInductiveDefinition;;
+exception RelToHiddenHypothesis;;
 
 (* takes a well-typed term *)
-let whd =
+let whd context =
  let rec whdaux l =
   let module C = Cic in
   let module S = CicSubstitution in
    function
-      C.Rel _ as t -> if l = [] then t else C.Appl (t::l)
-    | C.Var uri as t ->
-       (match CicEnvironment.get_cooked_obj uri 0 with
-           C.Definition _ -> raise ReferenceToDefinition
-         | C.Axiom _ -> raise ReferenceToAxiom
+      C.Rel n as t ->
+       (match List.nth context (n-1) with
+           Some (_, C.Decl _) -> if l = [] then t else C.Appl (t::l)
+         | Some (_, C.Def bo) -> whdaux l (S.lift n bo)
+	  | None -> raise RelToHiddenHypothesis
+       )
+    | C.Var (uri,exp_named_subst) as t ->
+       (match CicEnvironment.get_cooked_obj ~trust:false uri 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,_) -> whdaux l 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)
     | C.Sort _ as t -> t (* l should be empty *)
@@ -77,18 +79,19 @@ let whd =
     | C.LetIn (n,s,t) -> whdaux l (S.subst (whdaux [] s) t)
     | C.Appl (he::tl) -> whdaux (tl@l) he
     | C.Appl [] -> raise (Impossible 1)
-    | C.Const (uri,cookingsno) as t ->
-       (match CicEnvironment.get_cooked_obj uri cookingsno with
-           C.Definition (_,body,_,_) -> whdaux l body
-         | C.Axiom _ -> if l = [] then t else C.Appl (t::l)
+    | C.Const (uri,exp_named_subst) as t ->
+       (match CicEnvironment.get_cooked_obj ~trust:false uri 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,_) -> whdaux l body
+         | C.CurrentProof (_,_,body,_,_) ->
+            whdaux l (CicSubstitution.subst_vars exp_named_subst body)
          | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
        )
-    | C.Abst _ as t -> t (*CSC l should be empty ????? *)
-    | C.MutInd (uri,_,_) as t -> if l = [] then t else C.Appl (t::l)
-    | C.MutConstruct (uri,_,_,_) as t -> if l = [] then t else C.Appl (t::l)
-    | C.MutCase (mutind,cookingsno,i,_,term,pl) as t ->
+    | C.MutInd _ as t -> if l = [] then t else C.Appl (t::l)
+    | C.MutConstruct _ as t -> if l = [] then t else C.Appl (t::l)
+    | C.MutCase (mutind,i,_,term,pl) as t->
        let decofix =
         function
            C.CoFix (i,fl) as t ->
@@ -114,35 +117,28 @@ let whd =
          | t -> t
        in
         (match decofix (whdaux [] term) with
-            C.MutConstruct (_,_,_,j) -> whdaux l (List.nth pl (j-1))
-          | C.Appl (C.MutConstruct (_,_,_,j) :: tl) ->
-             let (arity, r, num_ingredients) =
+            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 (_,_,arity,_) = List.nth tl i
-                   and num_ingredients =
-                    List.fold_right
-                     (fun (k,l) i ->
-                       if k < cookingsno then i + List.length l else i
-                     ) ingredients 0
-                   in
-                    (arity,r,num_ingredients)
+                   let (_,_,arity,_) = List.nth tl i in
+                    (arity,r)
                | _ -> raise WrongUriToInductiveDefinition
              in
               let ts =
-               let num_to_eat = r + num_ingredients in
-                let rec eat_first =
-                 function
-                    (0,l) -> l
-                  | (n,he::tl) when n > 0 -> eat_first (n - 1, tl)
-                  | _ -> raise (Impossible 5)
-                in
-                 eat_first (num_to_eat,tl)
+               let rec eat_first =
+                function
+                   (0,l) -> l
+                 | (n,he::tl) when n > 0 -> eat_first (n - 1, tl)
+                 | _ -> raise (Impossible 5)
+               in
+                eat_first (r,tl)
               in
                whdaux (ts@l) (List.nth pl (j-1))
-         | C.Abst _| C.Cast _ | C.Implicit ->
-            raise (Impossible 2) (* we don't trust our whd ;-) *)
-         | _ -> t
+          | C.Cast _ | C.Implicit ->
+             raise (Impossible 2) (* we don't trust our whd ;-) *)
+          | _ -> if l = [] then t else C.Appl (t::l)
        )
     | C.Fix (i,fl) as t ->
        let (_,recindex,_,body) = List.nth fl i in
@@ -171,98 +167,140 @@ let whd =
           | None -> if l = [] then t else C.Appl (t::l)
          )
     | C.CoFix (i,fl) as t ->
-       (*CSC vecchio codice
-       let (_,_,body) = List.nth fl i in
-        let body' =
-         let counter = ref (List.length fl) in
-          List.fold_right
-           (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
-           fl
-           body
-        in
-         whdaux l body'
-       *)
        if l = [] then t else C.Appl (t::l)
  in
+(*CSC
+function t ->
+prerr_endline ("PRIMA WHD" ^ CicPp.ppterm t) ; flush stderr ;
+List.iter (function (Cic.Decl t) -> prerr_endline ("Context: " ^ CicPp.ppterm t) | (Cic.Def t) -> prerr_endline ("Context:= " ^ CicPp.ppterm t)) context ; flush stderr ; prerr_endline "<PRIMA WHD" ; flush stderr ;
+let res =
+*)
   whdaux []
+(*CSC
+t in prerr_endline "DOPO WHD" ; flush stderr ; res
+*)
 ;;
 
 (* t1, t2 must be well-typed *)
-let are_convertible t1 t2 =
+let are_convertible =
  let module U = UriManager in
- let rec aux t1 t2 =
-  debug t1 [t2] "PREWHD";
-  (* 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
-  else
-   begin
-    let module C = Cic in
-     let t1' = whd t1 
-     and t2' = whd t2 in
-     debug t1' [t2'] "POSTWHD";
-     (*if !fdebug = 0 then ignore(Unix.system "read" );*)
-      match (t1',t2') with
-         (C.Rel n1, C.Rel n2) -> n1 = n2
-       | (C.Var uri1, C.Var uri2) -> U.eq uri1 uri2
-       | (C.Meta n1, C.Meta n2) -> n1 = n2
-       | (C.Sort s1, C.Sort s2) -> true (*CSC da finire con gli universi *)
-       | (C.Prod (_,s1,t1), C.Prod(_,s2,t2)) ->
-          aux s1 s2 && aux t1 t2
-       | (C.Lambda (_,s1,t1), C.Lambda(_,s2,t2)) ->
-          aux s1 s2 && aux t1 t2
-       | (C.Appl l1, C.Appl l2) ->
-          (try
-            List.fold_right2 (fun  x y b -> aux x y && b) l1 l2 true 
-           with
-            Invalid_argument _ -> false
-          )
-       | (C.Const (uri1,_), C.Const (uri2,_)) ->
-           (*CSC: questo commento e' chiaro o delirante? Io lo sto scrivendo *)
-           (*CSC: mentre sono delirante, quindi ...                          *)
-           (* WARNING: it is really important that the two cookingsno are not *)
-           (* checked for equality. This allows not to cook an object with no *)
-           (* ingredients only to update the cookingsno. E.g: if a term t has *)
-           (* a reference to a term t1 which does not depend on any variable  *)
-           (* and t1 depends on a term t2 (that can't depend on any variable  *)
-           (* because of t1), then t1 cooked at every level could be the same *)
-           (* as t1 cooked at level 0. Doing so, t2 will be extended in t     *)
-           (* with cookingsno 0 and not 2. But this will not cause any trouble*)
-           (* if here we don't check that the two cookingsno are equal.       *)
-           U.eq uri1 uri2
-       | (C.MutInd (uri1,k1,i1), C.MutInd (uri2,k2,i2)) ->
-           (* WARNIG: see the previous warning *)
-           U.eq uri1 uri2 && i1 = i2
-       | (C.MutConstruct (uri1,_,i1,j1), C.MutConstruct (uri2,_,i2,j2)) ->
-           (* WARNIG: see the previous warning *)
-           U.eq uri1 uri2 && i1 = i2 && j1 = j2
-       | (C.MutCase (uri1,_,i1,outtype1,term1,pl1),
-          C.MutCase (uri2,_,i2,outtype2,term2,pl2)) -> 
-           (* WARNIG: see the previous warning *)
-           (* aux outtype1 outtype2 should be true if aux pl1 pl2 *)
-           U.eq uri1 uri2 && i1 = i2 && aux outtype1 outtype2 &&
-            aux term1 term2 &&
-            List.fold_right2 (fun x y b -> b && aux x y) pl1 pl2 true
-       | (C.Fix (i1,fl1), C.Fix (i2,fl2)) ->
-          i1 = i2 &&
-           List.fold_right2
-            (fun (_,recindex1,ty1,bo1) (_,recindex2,ty2,bo2) b ->
-              b && recindex1 = recindex2 && aux ty1 ty2 && aux bo1 bo2)
-            fl1 fl2 true
-       | (C.CoFix (i1,fl1), C.CoFix (i2,fl2)) ->
-          i1 = i2 &&
-           List.fold_right2
-            (fun (_,ty1,bo1) (_,ty2,bo2) b ->
-              b && aux ty1 ty2 && aux bo1 bo2)
-            fl1 fl2 true
-       | (C.Abst _, _) | (_, C.Abst _) | (C.Cast _, _) | (_, C.Cast _)
-       | (C.Implicit, _) | (_, C.Implicit) ->
-          raise (Impossible 3) (* we don't trust our whd ;-) *)
-       | (_,_) ->
-          debug t1' [t2'] "NOT-CONVERTIBLE" ;
-          false
-   end
+ let rec aux context t1 t2 =
+  let aux2 t1 t2 =
+   (* 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
+   else
+    begin
+     let module C = Cic in
+       match (t1,t2) with
+          (C.Rel n1, C.Rel n2) -> n1 = n2
+        | (C.Var (uri1,exp_named_subst1), C.Var (uri2,exp_named_subst2)) ->
+            U.eq uri1 uri2 &&
+             (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 
+              with
+               Invalid_argument _ -> false
+             )
+        | (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 context t1' t2'
+              ) true l1 l2
+        | (C.Sort s1, C.Sort s2) -> true (*CSC da finire con gli universi *)
+        | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) ->
+           aux context s1 s2 && aux ((Some (name1, (C.Decl s1)))::context) t1 t2
+        | (C.Lambda (name1,s1,t1), C.Lambda(_,s2,t2)) ->
+           aux context s1 s2 && aux ((Some (name1, (C.Decl s1)))::context) t1 t2
+        | (C.LetIn (name1,s1,t1), C.LetIn(_,s2,t2)) ->
+           aux context s1 s2 && aux ((Some (name1, (C.Def s1)))::context) t1 t2
+        | (C.Appl l1, C.Appl l2) ->
+           (try
+             List.fold_right2 (fun  x y b -> aux context x y && b) l1 l2 true 
+            with
+             Invalid_argument _ -> false
+           )
+        | (C.Const (uri1,exp_named_subst1), C.Const (uri2,exp_named_subst2)) ->
+            U.eq uri1 uri2 &&
+             (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 
+              with
+               Invalid_argument _ -> false
+             )
+        | (C.MutInd (uri1,i1,exp_named_subst1),
+           C.MutInd (uri2,i2,exp_named_subst2)
+          ) ->
+            U.eq uri1 uri2 && i1 = i2 &&
+             (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 
+              with
+               Invalid_argument _ -> false
+             )
+        | (C.MutConstruct (uri1,i1,j1,exp_named_subst1),
+           C.MutConstruct (uri2,i2,j2,exp_named_subst2)
+          ) ->
+            U.eq uri1 uri2 && i1 = i2 && j1 = j2 &&
+             (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 
+              with
+               Invalid_argument _ -> false
+             )
+        | (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
+        | (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 &&
+             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
+        | (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
+        | (C.Cast _, _) | (_, C.Cast _)
+        | (C.Implicit, _) | (_, C.Implicit) ->
+           raise (Impossible 3) (* we don't trust our whd ;-) *)
+        | (_,_) -> false
+    end
+  in
+   if aux2 t1 t2 then true
+   else
+    begin
+     debug t1 [t2] "PREWHD";
+     let t1' = whd context t1 
+     and t2' = whd context t2 in
+      debug t1' [t2'] "POSTWHD";
+      aux2 t1' t2'
+    end
  in
-  aux t1 t2
+  aux
 ;;