- C.Appl ((C.MutInd (uri',_,_))::tl) when UriManager.eq uri' uri -> true
- | C.MutInd (uri',0,_) when UriManager.eq uri' uri -> true
- | C.Prod (C.Anonymous,source,dest) ->
- strictly_positive context n nn
- (subst_inductive_type_with_dummy_mutind source) &&
- weakly_positive ((Some (C.Anonymous,(C.Decl source)))::context)
- (n + 1) (nn + 1) uri dest
- | C.Prod (name,source,dest) when
- does_not_occur ((Some (name,(C.Decl source)))::context) 0 n dest ->
- (* dummy abstraction, so we behave as in the anonimous case *)
- strictly_positive context n nn
- (subst_inductive_type_with_dummy_mutind source) &&
- weakly_positive ((Some (name,(C.Decl source)))::context)
- (n + 1) (nn + 1) uri dest
- | C.Prod (name,source,dest) ->
- does_not_occur context n nn
- (subst_inductive_type_with_dummy_mutind source)&&
- weakly_positive ((Some (name,(C.Decl source)))::context)
- (n + 1) (nn + 1) uri dest
- | _ ->
- raise (TypeCheckerFailure (lazy "Malformed inductive constructor type"))
-
-(* instantiate_parameters ps (x1:T1)...(xn:Tn)C *)
-(* returns ((x_|ps|:T_|ps|)...(xn:Tn)C){ps_1 / x1 ; ... ; ps_|ps| / x_|ps|} *)
-and instantiate_parameters params c =
- let module C = Cic in
- match (c,params) with
- (c,[]) -> c
- | (C.Prod (_,_,ta), he::tl) ->
- instantiate_parameters tl
- (CicSubstitution.subst he ta)
- | (C.Cast (te,_), _) -> instantiate_parameters params te
- | (t,l) -> raise (AssertFailure (lazy "1"))
-
-and strictly_positive context n nn te =
- let module C = Cic in
- let module U = UriManager in
- match CicReduction.whd context te with
- | t when does_not_occur context n nn t -> true
- | C.Rel _ -> true
- | C.Cast (te,ty) ->
- (*CSC: bisogna controllare ty????*)
- strictly_positive context n nn te
- | C.Prod (name,so,ta) ->
- does_not_occur context n nn so &&
- strictly_positive ((Some (name,(C.Decl so)))::context) (n+1) (nn+1) ta
- | C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
- List.fold_right (fun x i -> i && does_not_occur context n nn x) tl true
- | C.Appl ((C.MutInd (uri,i,exp_named_subst))::tl) ->
- let (ok,paramsno,ity,cl,name) =
- let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
- match o with
- C.InductiveDefinition (tl,_,paramsno,_) ->
- let (name,_,ity,cl) = List.nth tl i in
- (List.length tl = 1, paramsno, ity, cl, name)
- (* (true, paramsno, ity, cl, name) *)
- | _ ->
- raise
- (TypeCheckerFailure
- (lazy ("Unknown inductive type:" ^ U.string_of_uri uri)))
- in
- let (params,arguments) = split tl paramsno in
- let lifted_params = List.map (CicSubstitution.lift 1) params in
- let cl' =
- List.map
- (fun (_,te) ->
- instantiate_parameters lifted_params
- (CicSubstitution.subst_vars exp_named_subst te)
- ) cl
- in
- ok &&
- List.fold_right
- (fun x i -> i && does_not_occur context n nn x)
- arguments true &&
- (*CSC: MEGAPATCH3 (sara' quella giusta?)*)
- List.fold_right
- (fun x i ->
- i &&
- weakly_positive
- ((Some (C.Name name,(Cic.Decl ity)))::context) (n+1) (nn+1) uri
- x
- ) cl' true
- | t -> false
-
-(* the inductive type indexes are s.t. n < x <= nn *)
-and are_all_occurrences_positive context uri indparamsno i n nn te =
- let module C = Cic in
- match CicReduction.whd context te with
- C.Appl ((C.Rel m)::tl) when m = i ->
- (*CSC: riscrivere fermandosi a 0 *)
- (* let's check if the inductive type is applied at least to *)
- (* indparamsno parameters *)
- let last =
- List.fold_left
- (fun k x ->
- if k = 0 then 0
- else
- match CicReduction.whd context x with
- C.Rel m when m = n - (indparamsno - k) -> k - 1
- | _ ->
- raise (TypeCheckerFailure
- (lazy
- ("Non-positive occurence in mutual inductive definition(s) [1]" ^
- UriManager.string_of_uri uri)))
- ) indparamsno tl
- in
- if last = 0 then
- List.fold_right (fun x i -> i && does_not_occur context n nn x) tl true
- else
- raise (TypeCheckerFailure
- (lazy ("Non-positive occurence in mutual inductive definition(s) [2]"^
- UriManager.string_of_uri uri)))
- | C.Rel m when m = i ->
- if indparamsno = 0 then
- true
- else
- raise (TypeCheckerFailure
- (lazy ("Non-positive occurence in mutual inductive definition(s) [3]"^
- UriManager.string_of_uri uri)))
- | C.Prod (C.Anonymous,source,dest) ->
- let b = strictly_positive context n nn source in
- b &&
- are_all_occurrences_positive
- ((Some (C.Anonymous,(C.Decl source)))::context) uri indparamsno
- (i+1) (n + 1) (nn + 1) dest
- | C.Prod (name,source,dest) when
- does_not_occur ((Some (name,(C.Decl source)))::context) 0 n dest ->
- (* dummy abstraction, so we behave as in the anonimous case *)
- strictly_positive context n nn source &&
- are_all_occurrences_positive
- ((Some (name,(C.Decl source)))::context) uri indparamsno
- (i+1) (n + 1) (nn + 1) dest
- | C.Prod (name,source,dest) ->
- does_not_occur context n nn source &&
- are_all_occurrences_positive ((Some (name,(C.Decl source)))::context)
- uri indparamsno (i+1) (n + 1) (nn + 1) dest
- | _ ->
- raise
- (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