-(* 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)))
-