split into two major parts:

[helm.git] / helm / ocaml / cic_proof_checking / cicTypeChecker.ml

diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
index 19ee778f56d25aaf1e94e404935177bcdd53b67f..8403f5f0c082e295da72e48c1764cd27adc24ea2 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
@@ -30,7 +30,6 @@ open Printf
 
 exception AssertFailure of string;;
 exception TypeCheckerFailure of string;;
-exception SortExpectedMetaFound of string;;   (* TODO temp *)
 
 let fdebug = ref 0;;
 let debug t context =
@@ -67,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)
@@ -206,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) ->
@@ -568,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) ->
@@ -647,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 &&
@@ -800,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
@@ -978,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 _ ->
@@ -1009,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) ->
@@ -1043,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
@@ -1354,7 +1353,7 @@ and type_of_aux' metasenv context t =
         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,10 +1637,12 @@ 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 (SortExpectedMetaFound (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')))
-(*       raise (TypeCheckerFailure (sprintf *)
 
  and eat_prods context hetype =
   (*CSC: siamo sicuri che le are_convertible non lavorino con termini non *)