X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicReductionNaif.ml;h=f569e75cd451f196a83ef95e86db8a735e07e206;hb=b1fb6b8e1767d775bc452303629e95941d142bea;hp=089906b6d6628472b05c5342b31795a631e0b35b;hpb=37f08b2aba9f17d9d609ca0f57d607f437a3d3fc;p=helm.git

diff --git a/helm/ocaml/cic_proof_checking/cicReductionNaif.ml b/helm/ocaml/cic_proof_checking/cicReductionNaif.ml
index 089906b6d..f569e75cd 100644
--- a/helm/ocaml/cic_proof_checking/cicReductionNaif.ml
+++ b/helm/ocaml/cic_proof_checking/cicReductionNaif.ml
@@ -56,8 +56,8 @@ let whd context =
    function
       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)
+           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 as t ->
@@ -91,7 +91,6 @@ let whd context =
          | C.CurrentProof (_,_,body,_) -> whdaux l 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->
@@ -146,7 +145,7 @@ let whd context =
                  eat_first (num_to_eat,tl)
               in
                whdaux (ts@l) (List.nth pl (j-1))
-         | C.Abst _| C.Cast _ | C.Implicit ->
+         | C.Cast _ | C.Implicit ->
             raise (Impossible 2) (* we don't trust our whd ;-) *)
          | _ -> if l = [] then t else C.Appl (t::l)
        )
@@ -207,14 +206,22 @@ let are_convertible =
           (C.Rel n1, C.Rel n2) -> n1 = n2
         | (C.Var uri1, C.Var uri2) -> U.eq uri1 uri2
         | (C.Meta (n1,l1), C.Meta (n2,l2)) -> 
-	    if n1 = n2 then (assert (l1=l2);true) else false
+            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 (_,s1,t1), C.Prod(_,s2,t2)) ->
-           aux context s1 s2 && aux ((Some (C.Decl s1))::context) t1 t2
-        | (C.Lambda (_,s1,t1), C.Lambda(_,s2,t2)) ->
-           aux context s1 s2 && aux ((Some (C.Decl s1))::context) t1 t2
-        | (C.LetIn (_,s1,t1), C.LetIn(_,s2,t2)) ->
-           aux context s1 s2 && aux ((Some (C.Def s1))::context) t1 t2
+        | (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 
@@ -250,7 +257,9 @@ let are_convertible =
              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 (_,_,ty,_) -> Some (C.Decl ty)) fl1 in
+           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 ->
@@ -258,13 +267,15 @@ let are_convertible =
                  aux (tys@context) bo1 bo2)
               fl1 fl2 true
         | (C.CoFix (i1,fl1), C.CoFix (i2,fl2)) ->
-           let tys = List.map (function (_,ty,_) -> Some (C.Decl ty)) fl1 in
+           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.Abst _, _) | (_, C.Abst _) | (C.Cast _, _) | (_, C.Cast _)
+        | (C.Cast _, _) | (_, C.Cast _)
         | (C.Implicit, _) | (_, C.Implicit) ->
            raise (Impossible 3) (* we don't trust our whd ;-) *)
         | (_,_) -> false