X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicTypeChecker.ml;h=8403f5f0c082e295da72e48c1764cd27adc24ea2;hb=b38de2d3fa8bbe346c59c18bbeb889f29e493f63;hp=2ba10d7426926dcb1ccbd095ac3188394e6f4260;hpb=dc9e2d7251f23bce441aa19a13f70d309a7c35fd;p=helm.git

diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
index 2ba10d742..8403f5f0c 100644
--- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
@@ -66,7 +66,7 @@ let debrujin_constructor uri number_of_types =
         C.Var (uri,exp_named_subst')
     | C.Meta _ -> assert false
     | C.Sort _
-    | C.Implicit as t -> t
+    | C.Implicit _ as t -> t
     | C.Cast (te,ty) -> C.Cast (aux k te, aux k ty)
     | C.Prod (n,s,t) -> C.Prod (n, aux k s, aux (k+1) t)
     | C.Lambda (n,s,t) -> C.Lambda (n, aux k s, aux (k+1) t)
@@ -205,7 +205,7 @@ and does_not_occur context n nn te =
     | C.Rel _
     | C.Meta _
     | C.Sort _
-    | C.Implicit -> true
+    | C.Implicit _ -> true
     | C.Cast (te,ty) ->
        does_not_occur context n nn te && does_not_occur context n nn ty
     | C.Prod (name,so,dest) ->
@@ -567,7 +567,7 @@ and recursive_args context n nn te =
    | C.Var _
    | C.Meta _
    | C.Sort _
-   | C.Implicit
+   | C.Implicit _
    | C.Cast _ (*CSC ??? *) ->
       raise (AssertFailure "3") (* due to type-checking *)
    | C.Prod (name,so,de) ->
@@ -631,7 +631,8 @@ and eat_lambdas context n te =
        eat_lambdas ((Some (name,(C.Decl so)))::context) (n - 1) ta
       in
        (te, k + 1, context')
-   | (_, _) -> raise (AssertFailure "9")
+   | (n, te) ->
+       raise (AssertFailure (sprintf "9 (%d, %s)" n (CicPp.ppterm te)))
 
 (*CSC: Tutto quello che segue e' l'intuzione di luca ;-) *)
 and check_is_really_smaller_arg context n nn kl x safes te =
@@ -645,7 +646,7 @@ and check_is_really_smaller_arg context n nn kl x safes te =
    | C.Var _
    | C.Meta _
    | C.Sort _
-   | C.Implicit 
+   | C.Implicit _
    | C.Cast _
 (*   | C.Cast (te,ty) ->
       check_is_really_smaller_arg n nn kl x safes te &&
@@ -798,7 +799,7 @@ and guarded_by_destructors context n nn kl x safes =
       )
    | C.Meta _
    | C.Sort _
-   | C.Implicit -> true
+   | C.Implicit _ -> true
    | C.Cast (te,ty) ->
       guarded_by_destructors context n nn kl x safes te &&
        guarded_by_destructors context n nn kl x safes ty
@@ -976,7 +977,7 @@ and guarded_by_constructors context n nn h te args coInductiveTypeURI =
    | C.Rel _ -> true
    | C.Meta _
    | C.Sort _
-   | C.Implicit
+   | C.Implicit _
    | C.Cast _
    | C.Prod _
    | C.LetIn _ ->
@@ -1007,7 +1008,7 @@ and guarded_by_constructors context n nn h te args coInductiveTypeURI =
          | C.Var _
          | C.Sort _ ->
             does_not_occur context n nn te
-         | C.Implicit
+         | C.Implicit _
          | C.Cast _ ->
             raise (AssertFailure "24")(* due to type-checking *)
          | C.Prod (name,so,de) ->
@@ -1041,7 +1042,7 @@ and guarded_by_constructors context n nn h te args coInductiveTypeURI =
          | C.Var _
          | C.Meta _
          | C.Sort _
-         | C.Implicit
+         | C.Implicit _
          | C.Cast _ -> raise (AssertFailure "29")(* due to type-checking *)
          | C.Prod (name,so,de) ->
             begin
@@ -1348,13 +1349,11 @@ and type_of_aux' metasenv context t =
        decr fdebug ;
        ty
     | C.Meta (n,l) -> 
-       let (_,canonical_context,ty) =
-        List.find (function (m,_,_) -> n = m) metasenv
-       in
+       let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
         check_metasenv_consistency metasenv context canonical_context l;
         CicSubstitution.lift_meta l ty
     | C.Sort s -> C.Sort C.Type (*CSC manca la gestione degli universi!!! *)
-    | C.Implicit -> raise (AssertFailure "21")
+    | C.Implicit _ -> raise (AssertFailure "21")
     | C.Cast (te,ty) as t ->
        let _ = type_of_aux context ty in
         if R.are_convertible context (type_of_aux context te) ty then
@@ -1638,8 +1637,10 @@ in if not res then debug_print ("#### " ^ CicPp.ppterm (type_of_aux context p) ^
         when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> (* different from Coq manual!!! *)
          C.Sort s2
     | (C.Sort s1, C.Sort s2) -> C.Sort C.Type (*CSC manca la gestione degli universi!!! *)
-    | (_,_) ->
-      raise (TypeCheckerFailure (sprintf
+    | (C.Meta _, C.Sort _) -> t2'
+    | (C.Meta _, C.Meta (_,[]))
+    | (C.Sort _, C.Meta (_,[])) -> t2'
+    | (_,_) -> raise (TypeCheckerFailure (sprintf
         "Prod: expected two sorts, found = %s, %s" (CicPp.ppterm t1')
           (CicPp.ppterm t2')))