+let rec eat_lambdas ~subst ~metasenv context n te =
+ match (n, R.whd ~subst context te) with
+ | (0, _) -> (te, context)
+ | (n, C.Lambda (name,so,ta)) when n > 0 ->
+ eat_lambdas ~subst ~metasenv ((name,(C.Decl so))::context) (n - 1) ta
+ | (n, te) ->
+ raise (AssertFailure (lazy (Printf.sprintf "eat_lambdas (%d, %s)" n
+ (PP.ppterm ~subst ~metasenv ~context te))))
+;;
+
+let rec eat_or_subst_lambdas
+ ~subst ~metasenv n te to_be_subst args (context,_,_ as k)
+=
+ match n, R.whd ~subst context te, to_be_subst, args with
+ | (n, C.Lambda (_,_,ta),true::to_be_subst,arg::args) when n > 0 ->
+ eat_or_subst_lambdas ~subst ~metasenv (n - 1) (S.subst arg ta)
+ to_be_subst args k
+ | (n, C.Lambda (name,so,ta),false::to_be_subst,_::args) when n > 0 ->
+ eat_or_subst_lambdas ~subst ~metasenv (n - 1) ta to_be_subst args
+ (shift_k (name,(C.Decl so)) k)
+ | (_, te, _, _) -> te, k
+;;
+
+let check_homogeneous_call ~subst context indparamsno n uri reduct tl =
+ let last =
+ List.fold_left
+ (fun k x ->
+ if k = 0 then 0
+ else
+ match R.whd ~subst context x with
+ | C.Rel m when m = n - (indparamsno - k) -> k - 1
+ | _ -> raise (TypeCheckerFailure (lazy
+ ("Argument "^string_of_int (indparamsno - k + 1) ^ " (of " ^
+ string_of_int indparamsno ^ " fixed) is not homogeneous in "^
+ "appl:\n"^ PP.ppterm ~context ~subst ~metasenv:[] reduct))))
+ indparamsno tl
+ in
+ if last <> 0 then
+ raise (TypeCheckerFailure
+ (lazy ("Non-positive occurence in mutual inductive definition(s) [2]"^
+ NUri.string_of_uri uri)))
+;;
+
+(* Inductive types being checked for positivity have *)
+(* indexes x s.t. n < x <= nn. *)
+let rec weakly_positive ~subst context n nn uri indparamsno posuri te =
+ (*CSC: Not very nice. *)
+ let dummy = C.Sort C.Prop in
+ (*CSC: to be moved in cicSubstitution? *)
+ let rec subst_inductive_type_with_dummy _ = function
+ | C.Meta (_,(_,C.Irl _)) as x -> x
+ | C.Meta (i,(lift,C.Ctx ls)) ->
+ C.Meta (i,(lift,C.Ctx
+ (List.map (subst_inductive_type_with_dummy ()) ls)))
+ | C.Const (Ref.Ref (uri',Ref.Ind (true,0,_))) when NUri.eq uri' uri -> dummy
+ | C.Appl ((C.Const (Ref.Ref (uri',Ref.Ind (true,0,lno))))::tl)
+ when NUri.eq uri' uri ->
+ let _, rargs = HExtlib.split_nth lno tl in
+ if rargs = [] then dummy else C.Appl (dummy :: rargs)
+ | t -> U.map (fun _ x->x) () subst_inductive_type_with_dummy t
+ in
+ (* this function has the same semantics of are_all_occurrences_positive
+ but the i-th context entry role is played by dummy and some checks
+ are skipped because we already know that are_all_occurrences_positive
+ of uri in te. *)
+ let rec aux context n nn te =
+ match R.whd ~subst context te with
+ | t when t = dummy -> true
+ | C.Meta (i,lc) ->
+ (try
+ let _,_,term,_ = U.lookup_subst i subst in
+ let t = S.subst_meta lc term in
+ weakly_positive ~subst context n nn uri indparamsno posuri t
+ with U.Subst_not_found _ -> true)
+ | C.Appl (te::rargs) when te = dummy ->
+ List.for_all (does_not_occur ~subst context n nn) rargs
+ | C.Prod (name,source,dest) when
+ does_not_occur ~subst ((name,C.Decl source)::context) 0 1 dest ->
+ (* dummy abstraction, so we behave as in the anonimous case *)
+ strictly_positive ~subst context n nn indparamsno posuri source &&
+ aux ((name,C.Decl source)::context) (n + 1) (nn + 1) dest
+ | C.Prod (name,source,dest) ->
+ does_not_occur ~subst context n nn source &&
+ aux ((name,C.Decl source)::context) (n + 1) (nn + 1) dest
+ | _ ->
+ raise (TypeCheckerFailure (lazy "Malformed inductive constructor type"))
+ in
+ aux context n nn (subst_inductive_type_with_dummy () te)
+
+and strictly_positive ~subst context n nn indparamsno posuri te =
+ match R.whd ~subst context te with
+ | t when does_not_occur ~subst context n nn t -> true
+ | C.Meta (i,lc) ->
+ (try
+ let _,_,term,_ = U.lookup_subst i subst in
+ let t = S.subst_meta lc term in
+ strictly_positive ~subst context n nn indparamsno posuri t
+ with U.Subst_not_found _ -> true)
+ | C.Rel _ when indparamsno = 0 -> true
+ | C.Appl ((C.Rel m)::tl) as reduct when m > n && m <= nn ->
+ check_homogeneous_call ~subst context indparamsno n posuri reduct tl;
+ List.for_all (does_not_occur ~subst context n nn) tl
+ | C.Prod (name,so,ta) ->
+ does_not_occur ~subst context n nn so &&
+ strictly_positive ~subst ((name,C.Decl so)::context) (n+1) (nn+1)
+ indparamsno posuri ta
+ | C.Appl (C.Const (Ref.Ref (uri,Ref.Ind _) as r)::tl) ->
+ let _,paramsno,tyl,_,i = E.get_checked_indtys r in
+ let _,name,ity,cl = List.nth tyl i in
+ let ok = List.length tyl = 1 in
+ let params, arguments = HExtlib.split_nth paramsno tl in
+ let lifted_params = List.map (S.lift 1) params in
+ let cl =
+ List.map (fun (_,_,te) -> instantiate_parameters lifted_params te) cl
+ in
+ ok &&
+ List.for_all (does_not_occur ~subst context n nn) arguments &&
+ List.for_all
+ (weakly_positive ~subst ((name,C.Decl ity)::context) (n+1) (nn+1)
+ uri indparamsno posuri) cl
+ | _ -> false
+
+(* the inductive type indexes are s.t. n < x <= nn *)
+and are_all_occurrences_positive ~subst context uri indparamsno i n nn te =
+ match R.whd ~subst context te with
+ | C.Appl ((C.Rel m)::tl) as reduct when m = i ->
+ check_homogeneous_call ~subst context indparamsno n uri reduct tl;
+ List.for_all (does_not_occur ~subst context n nn) tl
+ | C.Rel m when m = i ->
+ if indparamsno = 0 then
+ true
+ else
+ raise (TypeCheckerFailure
+ (lazy ("Non-positive occurence in mutual inductive definition(s) [3]"^
+ NUri.string_of_uri uri)))
+ | C.Prod (name,source,dest) when
+ does_not_occur ~subst ((name,C.Decl source)::context) 0 1 dest ->
+ strictly_positive ~subst context n nn indparamsno uri source &&
+ are_all_occurrences_positive ~subst
+ ((name,C.Decl source)::context) uri indparamsno
+ (i+1) (n + 1) (nn + 1) dest
+ | C.Prod (name,source,dest) ->
+ if not (does_not_occur ~subst context n nn source) then
+ raise (TypeCheckerFailure (lazy ("Non-positive occurrence in "^
+ PP.ppterm ~context ~metasenv:[] ~subst te)));
+ are_all_occurrences_positive ~subst ((name,C.Decl source)::context)
+ uri indparamsno (i+1) (n + 1) (nn + 1) dest
+ | _ ->
+ raise
+ (TypeCheckerFailure (lazy ("Malformed inductive constructor type " ^
+ (NUri.string_of_uri uri))))
+;;
+