added preliminary checks for indtys

typecheck the explicit type of letins

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index 63eacd93169afe311b071174d2a3f519e15de197..907dd8b6cf3c8e8254f5adb165980d86b37904d6 100644 (file)
--- a/helm/software/components/ng_kernel/nCicTypeChecker.ml
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml
@@ -239,70 +239,6 @@ and are_all_occurrences_positive context uri indparamsno i n nn te =
       (TypeCheckerFailure (lazy ("Malformed inductive constructor type " ^
         (UriManager.string_of_uri uri))))
 
-(* Main function to checks the correctness of a mutual *)
-(* inductive block definition. This is the function    *)
-(* exported to the proof-engine.                       *)
-and typecheck_mutual_inductive_defs ~logger uri (itl,_,indparamsno) ugraph =
- let module U = UriManager in
-  (* let's check if the arity of the inductive types are well *)
-  (* formed                                                   *)
-  let ugrap1 = List.fold_left 
-   (fun ugraph (_,_,x,_) -> let _,ugraph' = 
-      type_of ~logger x ugraph in ugraph') 
-   ugraph itl in
-
-  (* let's check if the types of the inductive constructors  *)
-  (* are well formed.                                        *)
-  (* In order not to use type_of_aux we put the types of the *)
-  (* mutual inductive types at the head of the types of the  *)
-  (* constructors using Prods                                *)
-  let len = List.length itl in
-  let tys =
-    List.map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) itl in
-  let _,ugraph2 =
-    List.fold_right
-      (fun (_,_,_,cl) (i,ugraph) ->
-        let ugraph'' = 
-          List.fold_left
-            (fun ugraph (name,te) -> 
-              let debruijnedte = debruijn uri len te in
-              let augmented_term =
-                List.fold_right
-                  (fun (name,_,ty,_) i -> Cic.Prod (Cic.Name name, ty, i))
-                  itl debruijnedte
-              in
-              let _,ugraph' = type_of ~logger augmented_term ugraph in
-              (* let's check also the positivity conditions *)
-              if
-                not
-                  (are_all_occurrences_positive tys uri indparamsno i 0 len
-                     debruijnedte)
-              then
-                begin
-                prerr_endline (UriManager.string_of_uri uri);
-                prerr_endline (string_of_int (List.length tys));
-                raise
-                  (TypeCheckerFailure
-                    (lazy ("Non positive occurence in " ^ U.string_of_uri uri)))                end 
-              else
-                ugraph'
-            ) ugraph cl in
-        (i + 1),ugraph''
-      ) itl (1,ugrap1)
-  in
-  ugraph2
-
-(* Main function to checks the correctness of a mutual *)
-(* inductive block definition.                         *)
-and check_mutual_inductive_defs uri obj ugraph =
-  match obj with
-      Cic.InductiveDefinition (itl, params, indparamsno, _) ->
-        typecheck_mutual_inductive_defs uri (itl,params,indparamsno) ugraph 
-    | _ ->
-        raise (TypeCheckerFailure (
-                lazy ("Unknown mutual inductive definition:" ^
-                 UriManager.string_of_uri uri)))
-
 (* the boolean h means already protected *)
 (* args is the list of arguments the type of the constructor that may be *)
 (* found in head position must be applied to.                            *)
@@ -610,9 +546,10 @@ let eat_prods ~subst ~metasenv context ty_he args_with_ty =
       (match R.whd ~subst context ty_he with 
       | C.Prod (n,s,t) ->
 (*
-          prerr_endline (NCicPp.ppterm ~context s ^ " - Vs - " ^ NCicPp.ppterm
+          prerr_endline (NCicPp.ppterm ~subst ~metasenv ~context s ^ " - Vs - "
+          ^ NCicPp.ppterm ~subst ~metasenv
           ~context ty_arg);
-          prerr_endline (NCicPp.ppterm ~context (S.subst ~avoid_beta_redexes:true arg t));
+          prerr_endline (NCicPp.ppterm ~subst ~metasenv ~context (S.subst ~avoid_beta_redexes:true arg t));
 *)
           if R.are_convertible ~subst ~metasenv context ty_arg s then
             aux (S.subst ~avoid_beta_redexes:true arg t) tl
@@ -718,6 +655,7 @@ let rec typeof ~subst ~metasenv context term =
          C.Prod (n,s,ty)
     | C.LetIn (n,ty,t,bo) ->
        let ty_t = typeof_aux context t in
+       let _ = typeof_aux context ty in
        if not (R.are_convertible ~subst ~metasenv context ty ty_t) then
          raise 
           (TypeCheckerFailure 
@@ -986,7 +924,31 @@ let rec typeof ~subst ~metasenv context term =
  in 
    typeof_aux context term
 
-and check_mutual_inductive_defs _ = ()
+and check_mutual_inductive_defs uri ~metasenv ~subst is_ind leftno tyl = 
+  (* let's check if the arity of the inductive types are well formed *)
+  List.iter (fun (_,_,x,_) -> ignore (typeof ~subst ~metasenv [] x)) tyl;
+  (* let's check if the types of the inductive constructors are well formed. *)
+  let len = List.length tyl in
+  let tys = List.map (fun (_,n,ty,_) -> (n,(C.Decl ty))) tyl in
+  ignore
+   (List.fold_right
+    (fun (_,_,_,cl) i ->
+       List.iter
+         (fun (_,name,te) -> 
+           let debruijnedte = debruijn uri len te in
+           ignore (typeof ~subst ~metasenv tys debruijnedte);
+           (* let's check also the positivity conditions *)
+           if false (*
+             not
+               (are_all_occurrences_positive tys uri indparamsno i 0 len
+                  debruijnedte) *)
+           then
+             raise
+               (TypeCheckerFailure
+                 (lazy ("Non positive occurence in "^NUri.string_of_uri uri))))
+         cl;
+        i + 1)
+    tyl 1)
 
 and eat_lambdas ~subst ~metasenv context n te =
   match (n, R.whd ~subst context te) with
@@ -1218,7 +1180,8 @@ and check_obj_well_typed (uri,height,metasenv,subst,kind) =
         (NCicPp.ppterm ~subst ~metasenv ~context:[] ty_te) 
         (NCicPp.ppterm ~subst ~metasenv ~context:[] ty))))
    | C.Constant (_,_,None,ty,_) -> ignore (typeof ~subst ~metasenv [] ty)
-   | C.Inductive _ as obj -> check_mutual_inductive_defs obj
+   | C.Inductive (is_ind, leftno, tyl, _) -> 
+       check_mutual_inductive_defs uri ~metasenv ~subst is_ind leftno tyl
    | C.Fixpoint (inductive,fl,_) ->
       let types,kl,len =
         List.fold_left