From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 3 Dec 2002 14:34:05 +0000 (+0000)
Subject: typecheck_mutual_inductive_defs exposed.
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a0e5816092e0d90329602192c89d6f320d5fb882;p=helm.git

typecheck_mutual_inductive_defs exposed.
It is used to type-check and inductive definition which has no URI associated
to it (i.e. it is not managed by the getter; e.g. when it is not saved yet
since we do not know if it is well-typed).
---

diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
index a494c4a69..b07c6e4a0 100644
--- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
@@ -58,7 +58,9 @@ let debrujin_constructor uri number_of_types =
  let rec aux k =
   let module C = Cic in
    function
-      C.Rel _ as t -> t
+      C.Rel n as t when n <= k -> t
+    | C.Rel _ ->
+        raise (NotWellTyped ("Debrujin: open term found"))
     | C.Var (uri,exp_named_subst) ->
        let exp_named_subst' = 
         List.map (function (uri,t) -> (uri,aux k t)) exp_named_subst
@@ -428,49 +430,55 @@ and are_all_occurrences_positive context uri indparamsno i n nn te =
    | _ -> raise (NotWellFormedTypeOfInductiveConstructor (UriManager.string_of_uri uri))
 
 (* Main function to checks the correctness of a mutual *)
-(* inductive block definition.                         *)
-and check_mutual_inductive_defs uri =
+(* inductive block definition. This is the function    *)
+(* exported to the proof-engine.                       *)
+and typecheck_mutual_inductive_defs uri (itl,_,indparamsno) =
  let module U = UriManager in
-  function
-     Cic.InductiveDefinition (itl, _, indparamsno) ->
-      (* let's check if the arity of the inductive types are well *)
-      (* formed                                                   *)
-      List.iter (fun (_,_,x,_) -> let _ = type_of x in ()) itl ;
+  (* let's check if the arity of the inductive types are well *)
+  (* formed                                                   *)
+  List.iter (fun (_,_,x,_) -> let _ = type_of x in ()) itl ;
 
-      (* 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 _ =
-        List.fold_right
-         (fun (_,_,_,cl) i ->
-           List.iter
-            (fun (name,te) -> 
-              let debrujinedte = debrujin_constructor uri len te in
-              let augmented_term =
-               List.fold_right
-                (fun (name,_,ty,_) i -> Cic.Prod (Cic.Name name, ty, i))
-                itl debrujinedte
-              in
-               let _ = type_of augmented_term in
-                (* let's check also the positivity conditions *)
-                if
-                 not
-                  (are_all_occurrences_positive tys uri indparamsno i 0 len
-                    debrujinedte)
-                then
-                 raise (NotPositiveOccurrences (U.string_of_uri uri))
-            ) cl ;
-           (i + 1)
-        ) itl 1
-       in
-        ()
-   | _ ->
-     raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
+  (* 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 _ =
+    List.fold_right
+     (fun (_,_,_,cl) i ->
+       List.iter
+        (fun (name,te) -> 
+          let debrujinedte = debrujin_constructor uri len te in
+          let augmented_term =
+           List.fold_right
+            (fun (name,_,ty,_) i -> Cic.Prod (Cic.Name name, ty, i))
+            itl debrujinedte
+          in
+           let _ = type_of augmented_term in
+            (* let's check also the positivity conditions *)
+            if
+             not
+              (are_all_occurrences_positive tys uri indparamsno i 0 len
+                debrujinedte)
+            then
+             raise (NotPositiveOccurrences (U.string_of_uri uri))
+        ) cl ;
+       (i + 1)
+    ) itl 1
+   in
+    ()
+
+(* Main function to checks the correctness of a mutual *)
+(* inductive block definition.                         *)
+and check_mutual_inductive_defs uri =
+ function
+    Cic.InductiveDefinition (itl, params, indparamsno) ->
+     typecheck_mutual_inductive_defs uri (itl,params,indparamsno)
+  | _ ->
+    raise (WrongUriToMutualInductiveDefinitions (UriManager.string_of_uri uri))
 
 and type_of_mutual_inductive_defs uri i =
  let module C = Cic in
diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.mli b/helm/ocaml/cic_proof_checking/cicTypeChecker.mli
index a18d651f6..4a7fe8db0 100644
--- a/helm/ocaml/cic_proof_checking/cicTypeChecker.mli
+++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.mli
@@ -31,9 +31,15 @@ exception ListTooShort
 exception NotPositiveOccurrences of string
 exception NotWellFormedTypeOfInductiveConstructor of string
 exception WrongRequiredArgument of string
+
 val typecheck : UriManager.uri -> unit
 
-(* used only in the toplevel *)
+(* FUNCTIONS USED ONLY IN THE TOPLEVEL *)
+
 (* type_of_aux' metasenv context term *)
 val type_of_aux':
  Cic.metasenv -> Cic.context -> Cic.term -> Cic.term
+
+(* typecheck_mutual_inductive_defs uri (itl,params,indparamsno) *)
+val typecheck_mutual_inductive_defs :
+ UriManager.uri -> Cic.inductiveType list * UriManager.uri list * int -> unit