- Grammar for all obj commands ported to NG (let recs and inductives still need

[helm.git] / helm / software / components / ng_kernel / nCicTypeChecker.ml

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index da130c55574c07a501db14f6cd73ef0d676f0588..3459c8dd246b34e48848b367491465d324bd0b7c 100644 (file)
--- a/helm/software/components/ng_kernel/nCicTypeChecker.ml
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml
@@ -126,7 +126,8 @@ let sort_of_prod ~metasenv ~subst context (name,s) t (t1, t2) =
    let t2 = R.whd ~subst ((name,C.Decl s)::context) t2 in
    match t1, t2 with
    | C.Sort _, C.Sort C.Prop -> t2
-   | C.Sort (C.Type u1), C.Sort (C.Type u2) -> C.Sort (C.Type (u1@u2)) 
+   | C.Sort (C.Type u1), C.Sort (C.Type u2) ->
+      C.Sort (C.Type (NCicEnvironment.max u1 u2))
    | C.Sort C.Prop,C.Sort (C.Type _) -> t2
    | C.Meta (_,(_,(C.Irl 0 | C.Ctx []))), C.Sort _ -> t2
    | C.Meta (_,(_,(C.Irl 0 | C.Ctx []))), C.Meta (i,(_,(C.Irl 0 | C.Ctx [])))
@@ -235,7 +236,7 @@ let check_homogeneous_call ~subst context indparamsno n uri reduct tl =
    (fun k x ->
      if k = 0 then 0
      else
-      match R.whd context x with
+      match R.whd ~subst context x with
       | C.Rel m when m = n - (indparamsno - k) -> k - 1
       | _ -> raise (TypeCheckerFailure (lazy 
          ("Argument "^string_of_int (indparamsno - k + 1) ^ " (of " ^
@@ -268,7 +269,7 @@ let rec weakly_positive ~subst context n nn uri indparamsno posuri te =
      are skipped because we already know that are_all_occurrences_positive
      of uri in te. *)
   let rec aux context n nn te =
-    match R.whd context te with
+    match R.whd ~subst context te with
      | t when t = dummy -> true
      | C.Appl (te::rargs) when te = dummy ->
         List.for_all (does_not_occur ~subst context n nn) rargs
@@ -286,7 +287,7 @@ let rec weakly_positive ~subst context n nn uri indparamsno posuri te =
      aux context n nn (subst_inductive_type_with_dummy () te)
 
 and strictly_positive ~subst context n nn indparamsno posuri te =
-  match R.whd context te with
+  match R.whd ~subst context te with
    | t when does_not_occur ~subst context n nn t -> true
    | C.Rel _ when indparamsno = 0 -> true
    | C.Appl ((C.Rel m)::tl) as reduct when m > n && m <= nn ->
@@ -314,7 +315,7 @@ and strictly_positive ~subst context n nn indparamsno posuri te =
        
 (* the inductive type indexes are s.t. n < x <= nn *)
 and are_all_occurrences_positive ~subst context uri indparamsno i n nn te =
-  match R.whd context te with
+  match R.whd ~subst context te with
   |  C.Appl ((C.Rel m)::tl) as reduct when m = i ->
       check_homogeneous_call ~subst context indparamsno n uri reduct tl;
       List.for_all (does_not_occur ~subst context n nn) tl
@@ -374,7 +375,9 @@ let rec typeof ~subst ~metasenv context term =
          match List.nth context (n - 1) with
          | (_,C.Decl ty) -> S.lift n ty
          | (_,C.Def (_,ty)) -> S.lift n ty
-        with Failure _ -> raise (TypeCheckerFailure (lazy "unbound variable")))
+        with Failure _ -> 
+          raise (TypeCheckerFailure (lazy ("unbound variable " ^ string_of_int n
+            ^" under: " ^ NCicPp.ppcontext ~metasenv ~subst context))))
     | C.Sort (C.Type [false,u]) -> C.Sort (C.Type [true, u])
     | C.Sort (C.Type _) -> 
         raise (AssertFailure (lazy ("Cannot type an inferred type: "^
@@ -677,7 +680,7 @@ and eat_prods ~subst ~metasenv context he ty_he args_with_ty =
             raise 
               (TypeCheckerFailure 
                 (lazy (Printf.sprintf
-                  ("Appl: wrong application of %s: the parameter %s has type"^^
+                  ("Appl: wrong application of %s: the argument %s has type"^^
                    "\n%s\nbut it should have type \n%s\nContext:\n%s\n")
                   (PP.ppterm ~subst ~metasenv ~context he)
                   (PP.ppterm ~subst ~metasenv ~context arg)
@@ -714,7 +717,7 @@ and is_non_recursive_singleton ~subst (Ref.Ref (uri,_)) iname ity cty =
 
 and is_non_informative ~metasenv ~subst paramsno c =
  let rec aux context c =
-   match R.whd context c with
+   match R.whd ~subst context c with
     | C.Prod (n,so,de) ->
        let s = typeof ~metasenv ~subst context so in
        s = C.Sort C.Prop && aux ((n,(C.Decl so))::context) de
@@ -1001,7 +1004,7 @@ and guarded_by_constructors ~subst ~metasenv context t indURI indlen nn =
    aux context 0 nn false t
                                                                       
 and recursive_args ~subst ~metasenv context n nn te =
-  match R.whd context te with
+  match R.whd ~subst context te with
   | C.Rel _ | C.Appl _ | C.Const _ -> []
   | C.Prod (name,so,de) ->
      (not (does_not_occur ~subst context n nn so)) ::
@@ -1302,4 +1305,31 @@ E.set_typecheck_obj
 
 let _ = NCicReduction.set_get_relevance get_relevance;;
 
+
+let indent = ref 0;;
+let debug = true;;
+let logger =
+    let do_indent () = String.make !indent ' ' in  
+    (function 
+      | `Start_type_checking s ->
+          if debug then
+           prerr_endline (do_indent () ^ "Start: " ^ NUri.string_of_uri s); 
+          incr indent
+      | `Type_checking_completed s ->
+          decr indent;
+          if debug then
+           prerr_endline (do_indent () ^ "End: " ^ NUri.string_of_uri s)
+      | `Type_checking_interrupted s ->
+          decr indent;
+          if debug then
+           prerr_endline (do_indent () ^ "Break: " ^ NUri.string_of_uri s)
+      | `Type_checking_failed s ->
+          decr indent;
+          if debug then
+           prerr_endline (do_indent () ^ "Fail: " ^ NUri.string_of_uri s)
+      | `Trust_obj s ->
+          if debug then
+           prerr_endline (do_indent () ^ "Trust: " ^ NUri.string_of_uri s))
+;;
+(* let _ = set_logger logger ;; *)
 (* EOF *)