From a0e5816092e0d90329602192c89d6f320d5fb882 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 3 Dec 2002 14:34:05 +0000 Subject: [PATCH] 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). --- .../cic_proof_checking/cicTypeChecker.ml | 92 ++++++++++--------- .../cic_proof_checking/cicTypeChecker.mli | 8 +- 2 files changed, 57 insertions(+), 43 deletions(-) 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 -- 2.39.2