summaryrefslogtreecommitdiff
path: root/checker/inductive.ml
diff options
context:
space:
mode:
Diffstat (limited to 'checker/inductive.ml')
-rw-r--r--checker/inductive.ml147
1 files changed, 53 insertions, 94 deletions
diff --git a/checker/inductive.ml b/checker/inductive.ml
index 79dba4fa..c4ffc141 100644
--- a/checker/inductive.ml
+++ b/checker/inductive.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Errors
+open CErrors
open Util
open Names
open Cic
@@ -31,20 +31,20 @@ let lookup_mind_specif env (kn,tyi) =
(mib, mib.mind_packets.(tyi))
let find_rectype env c =
- let (t, l) = decompose_app (whd_betadeltaiota env c) in
+ let (t, l) = decompose_app (whd_all env c) in
match t with
| Ind ind -> (ind, l)
| _ -> raise Not_found
let find_inductive env c =
- let (t, l) = decompose_app (whd_betadeltaiota env c) in
+ let (t, l) = decompose_app (whd_all env c) in
match t with
| Ind (ind,_)
when (fst (lookup_mind_specif env ind)).mind_finite != CoFinite -> (ind, l)
| _ -> raise Not_found
let find_coinductive env c =
- let (t, l) = decompose_app (whd_betadeltaiota env c) in
+ let (t, l) = decompose_app (whd_all env c) in
match t with
| Ind (ind,_)
when (fst (lookup_mind_specif env ind)).mind_finite == CoFinite -> (ind, l)
@@ -59,16 +59,6 @@ let inductive_instance mib =
UContext.instance mib.mind_universes
else Instance.empty
-let inductive_context mib =
- if mib.mind_polymorphic then
- instantiate_univ_context mib.mind_universes
- else UContext.empty
-
-let instantiate_inductive_constraints mib u =
- if mib.mind_polymorphic then
- subst_instance_constraints u (UContext.constraints mib.mind_universes)
- else Constraint.empty
-
(************************************************************************)
(* Build the substitution that replaces Rels by the appropriate *)
@@ -88,10 +78,10 @@ let instantiate_params full t u args sign =
anomaly ~label:"instantiate_params" (Pp.str "type, ctxt and args mismatch") in
let (rem_args, subs, ty) =
fold_rel_context
- (fun (_,copt,_) (largs,subs,ty) ->
- match (copt, largs, ty) with
- | (None, a::args, Prod(_,_,t)) -> (args, a::subs, t)
- | (Some b,_,LetIn(_,_,_,t)) ->
+ (fun decl (largs,subs,ty) ->
+ match (decl, largs, ty) with
+ | (LocalAssum _, a::args, Prod(_,_,t)) -> (args, a::subs, t)
+ | (LocalDef (_,b,_),_,LetIn(_,_,_,t)) ->
(largs, (substl subs (subst_instance_constr u b))::subs, t)
| (_,[],_) -> if full then fail() else ([], subs, ty)
| _ -> fail ())
@@ -161,7 +151,7 @@ let remember_subst u subst =
(* Propagate the new levels in the signature *)
let rec make_subst env =
let rec make subst = function
- | (_,Some _,_)::sign, exp, args ->
+ | LocalDef _ :: sign, exp, args ->
make subst (sign, exp, args)
| d::sign, None::exp, args ->
let args = match args with _::args -> args | [] -> [] in
@@ -174,7 +164,7 @@ let rec make_subst env =
(* a useless extra constraint *)
let s = sort_as_univ (snd (dest_arity env a)) in
make (cons_subst u s subst) (sign, exp, args)
- | (na,None,t)::sign, Some u::exp, [] ->
+ | LocalAssum (na,t) :: sign, Some u::exp, [] ->
(* No more argument here: we add the remaining universes to the *)
(* substitution (when [u] is distinct from all other universes in the *)
(* template, it is identity substitution otherwise (ie. when u is *)
@@ -190,8 +180,6 @@ let rec make_subst env =
in
make Univ.LMap.empty
-exception SingletonInductiveBecomesProp of Id.t
-
let instantiate_universes env ctx ar argsorts =
let args = Array.to_list argsorts in
let subst = make_subst env (ctx,ar.template_param_levels,args) in
@@ -208,11 +196,7 @@ let instantiate_universes env ctx ar argsorts =
(* Type of an inductive type *)
-let is_prop_sort = function
- | Prop Null -> true
- | _ -> false
-
-let type_of_inductive_gen ?(polyprop=true) env ((mib,mip),u) paramtyps =
+let type_of_inductive_gen env ((mib,mip),u) paramtyps =
match mip.mind_arity with
| RegularArity a ->
if not mib.mind_polymorphic then a.mind_user_arity
@@ -220,25 +204,7 @@ let type_of_inductive_gen ?(polyprop=true) env ((mib,mip),u) paramtyps =
| TemplateArity ar ->
let ctx = List.rev mip.mind_arity_ctxt in
let ctx,s = instantiate_universes env ctx ar paramtyps in
- (* The Ocaml extraction cannot handle (yet?) "Prop-polymorphism", i.e.
- the situation where a non-Prop singleton inductive becomes Prop
- when applied to Prop params *)
- if not polyprop && not (Univ.is_type0m_univ ar.template_level) && is_prop_sort s
- then raise (SingletonInductiveBecomesProp mip.mind_typename);
- mkArity (List.rev ctx,s)
-
-let type_of_inductive env pind =
- type_of_inductive_gen env pind [||]
-
-let constrained_type_of_inductive env ((mib,mip),u as pind) =
- let ty = type_of_inductive_gen env pind [||] in
- let cst = instantiate_inductive_constraints mib u in
- (ty, cst)
-
-let constrained_type_of_inductive_knowing_parameters env ((mib,mip),u as pind) args =
- let ty = type_of_inductive_gen env pind args in
- let cst = instantiate_inductive_constraints mib u in
- (ty, cst)
+ mkArity (List.rev ctx,s)
let type_of_inductive_knowing_parameters env mip args =
type_of_inductive_gen env mip args
@@ -275,16 +241,6 @@ let type_of_constructor_gen (cstr,u) (mib,mip as mspec) =
let type_of_constructor cstru mspec =
type_of_constructor_gen cstru mspec
-let type_of_constructor_in_ctx cstr (mib,mip as mspec) =
- let u = Univ.UContext.instance mib.mind_universes in
- let c = type_of_constructor_gen (cstr, u) mspec in
- (c, mib.mind_universes)
-
-let constrained_type_of_constructor (cstr,u as cstru) (mib,mip as ind) =
- let ty = type_of_constructor_gen cstru ind in
- let cst = instantiate_inductive_constraints mib u in
- (ty, cst)
-
let arities_of_specif (kn,u) (mib,mip) =
let specif = mip.mind_nf_lc in
Array.map (constructor_instantiate kn u mib) specif
@@ -319,8 +275,8 @@ let elim_sorts (_,mip) = mip.mind_kelim
let extended_rel_list n hyps =
let rec reln l p = function
- | (_,None,_) :: hyps -> reln (Rel (n+p) :: l) (p+1) hyps
- | (_,Some _,_) :: hyps -> reln l (p+1) hyps
+ | LocalAssum _ :: hyps -> reln (Rel (n+p) :: l) (p+1) hyps
+ | LocalDef _ :: hyps -> reln l (p+1) hyps
| [] -> l
in
reln [] 1 hyps
@@ -343,15 +299,15 @@ let check_allowed_sort ksort specif =
let is_correct_arity env c (p,pj) ind specif params =
let arsign,_ = get_instantiated_arity ind specif params in
let rec srec env pt ar =
- let pt' = whd_betadeltaiota env pt in
+ let pt' = whd_all env pt in
match pt', ar with
- | Prod (na1,a1,t), (_,None,a1')::ar' ->
+ | Prod (na1,a1,t), LocalAssum (_,a1')::ar' ->
(try conv env a1 a1'
with NotConvertible -> raise (LocalArity None));
- srec (push_rel (na1,None,a1) env) t ar'
+ srec (push_rel (LocalAssum (na1,a1)) env) t ar'
| Prod (na1,a1,a2), [] -> (* whnf of t was not needed here! *)
- let env' = push_rel (na1,None,a1) env in
- let ksort = match (whd_betadeltaiota env' a2) with
+ let env' = push_rel (LocalAssum (na1,a1)) env in
+ let ksort = match (whd_all env' a2) with
| Sort s -> family_of_sort s
| _ -> raise (LocalArity None) in
let dep_ind = build_dependent_inductive ind specif params in
@@ -362,8 +318,8 @@ let is_correct_arity env c (p,pj) ind specif params =
| Sort s', [] ->
check_allowed_sort (family_of_sort s') specif;
false
- | _, (_,Some _,_ as d)::ar' ->
- srec (push_rel d env) (lift 1 pt') ar'
+ | _, (LocalDef _ as d)::ar' ->
+ srec (push_rel d env) (lift 1 pt') ar'
| _ ->
raise (LocalArity None)
in
@@ -527,10 +483,10 @@ type guard_env =
let make_renv env recarg tree =
{ env = env;
rel_min = recarg+2; (* recarg = 0 ==> Rel 1 -> recarg; Rel 2 -> fix *)
- genv = [Lazy.lazy_from_val(Subterm(Large,tree))] }
+ genv = [Lazy.from_val(Subterm(Large,tree))] }
let push_var renv (x,ty,spec) =
- { env = push_rel (x,None,ty) renv.env;
+ { env = push_rel (LocalAssum (x,ty)) renv.env;
rel_min = renv.rel_min+1;
genv = spec:: renv.genv }
@@ -538,7 +494,7 @@ let assign_var_spec renv (i,spec) =
{ renv with genv = List.assign renv.genv (i-1) spec }
let push_var_renv renv (x,ty) =
- push_var renv (x,ty,Lazy.lazy_from_val Not_subterm)
+ push_var renv (x,ty,Lazy.from_val Not_subterm)
(* Fetch recursive information about a variable p *)
let subterm_var p renv =
@@ -549,13 +505,13 @@ let push_ctxt_renv renv ctxt =
let n = rel_context_length ctxt in
{ env = push_rel_context ctxt renv.env;
rel_min = renv.rel_min+n;
- genv = iterate (fun ge -> Lazy.lazy_from_val Not_subterm::ge) n renv.genv }
+ genv = iterate (fun ge -> Lazy.from_val Not_subterm::ge) n renv.genv }
let push_fix_renv renv (_,v,_ as recdef) =
let n = Array.length v in
{ env = push_rec_types recdef renv.env;
rel_min = renv.rel_min+n;
- genv = iterate (fun ge -> Lazy.lazy_from_val Not_subterm::ge) n renv.genv }
+ genv = iterate (fun ge -> Lazy.from_val Not_subterm::ge) n renv.genv }
(* Definition and manipulation of the stack *)
@@ -622,20 +578,21 @@ let check_inductive_codomain env p =
let env = push_rel_context absctx env in
let arctx, s = dest_prod_assum env ar in
let env = push_rel_context arctx env in
- let i,l' = decompose_app (whd_betadeltaiota env s) in
+ let i,l' = decompose_app (whd_all env s) in
match i with Ind _ -> true | _ -> false
(* The following functions are almost duplicated from indtypes.ml, except
that they carry here a poorer environment (containing less information). *)
let ienv_push_var (env, lra) (x,a,ra) =
-(push_rel (x,None,a) env, (Norec,ra)::lra)
+(push_rel (LocalAssum (x,a)) env, (Norec,ra)::lra)
let ienv_push_inductive (env, ra_env) ((mind,u),lpar) =
let mib = Environ.lookup_mind mind env in
let ntypes = mib.mind_ntypes in
let push_ind specif env =
- push_rel (Anonymous,None,
- hnf_prod_applist env (type_of_inductive env ((mib,specif),u)) lpar) env
+ let decl = LocalAssum (Anonymous,
+ hnf_prod_applist env (type_of_inductive env ((mib,specif),u)) lpar) in
+ push_rel decl env
in
let env = Array.fold_right push_ind mib.mind_packets env in
let rc = Array.mapi (fun j t -> (Imbr (mind,j),t)) (Rtree.mk_rec_calls ntypes) in
@@ -645,7 +602,7 @@ let ienv_push_inductive (env, ra_env) ((mind,u),lpar) =
let rec ienv_decompose_prod (env,_ as ienv) n c =
if Int.equal n 0 then (ienv,c) else
- let c' = whd_betadeltaiota env c in
+ let c' = whd_all env c in
match c' with
Prod(na,a,b) ->
let ienv' = ienv_push_var ienv (na,a,mk_norec) in
@@ -675,7 +632,7 @@ close to check_positive in indtypes.ml, but does no positivy check and does not
compute the number of recursive arguments. *)
let get_recargs_approx env tree ind args =
let rec build_recargs (env, ra_env as ienv) tree c =
- let x,largs = decompose_app (whd_betadeltaiota env c) in
+ let x,largs = decompose_app (whd_all env c) in
match x with
| Prod (na,b,d) ->
assert (List.is_empty largs);
@@ -734,7 +691,7 @@ let get_recargs_approx env tree ind args =
and build_recargs_constructors ienv trees c =
let rec recargs_constr_rec (env,ra_env as ienv) trees lrec c =
- let x,largs = decompose_app (whd_betadeltaiota env c) in
+ let x,largs = decompose_app (whd_all env c) in
match x with
| Prod (na,b,d) ->
@@ -763,7 +720,7 @@ let restrict_spec env spec p =
let env = push_rel_context absctx env in
let arctx, s = dest_prod_assum env ar in
let env = push_rel_context arctx env in
- let i,args = decompose_app (whd_betadeltaiota env s) in
+ let i,args = decompose_app (whd_all env s) in
match i with
| Ind i ->
begin match spec with
@@ -785,7 +742,7 @@ let restrict_spec env spec p =
let rec subterm_specif renv stack t =
(* maybe reduction is not always necessary! *)
- let f,l = decompose_app (whd_betadeltaiota renv.env t) in
+ let f,l = decompose_app (whd_all renv.env t) in
match f with
| Rel k -> subterm_var k renv
@@ -861,7 +818,7 @@ and stack_element_specif = function
|SArg x -> x
and extract_stack renv a = function
- | [] -> Lazy.lazy_from_val Not_subterm , []
+ | [] -> Lazy.from_val Not_subterm , []
| h::t -> stack_element_specif h, t
@@ -899,11 +856,11 @@ let filter_stack_domain env ci p stack =
if noccur_with_meta 1 (rel_context_length absctx) ar then stack
else let env = push_rel_context absctx env in
let rec filter_stack env ar stack =
- let t = whd_betadeltaiota env ar in
+ let t = whd_all env ar in
match stack, t with
| elt :: stack', Prod (n,a,c0) ->
- let d = (n,None,a) in
- let ty, args = decompose_app (whd_betadeltaiota env a) in
+ let d = LocalAssum (n,a) in
+ let ty, args = decompose_app (whd_all env a) in
let elt = match ty with
| Ind ind ->
let spec' = stack_element_specif elt in
@@ -956,10 +913,10 @@ let check_one_fix renv recpos trees def =
end
else
begin
- match pi2 (lookup_rel p renv.env) with
- | None ->
+ match lookup_rel p renv.env with
+ | LocalAssum _ ->
List.iter (check_rec_call renv []) l
- | Some c ->
+ | LocalDef (_,c,_) ->
try List.iter (check_rec_call renv []) l
with FixGuardError _ ->
check_rec_call renv stack (applist(lift p c,l))
@@ -1032,6 +989,10 @@ let check_one_fix renv recpos trees def =
| (Ind _ | Construct _) ->
List.iter (check_rec_call renv []) l
+ | Proj (p, c) ->
+ List.iter (check_rec_call renv []) l;
+ check_rec_call renv [] c
+
| Var _ -> anomaly (Pp.str "Section variable in Coqchk !")
| Sort _ -> assert (l = [])
@@ -1041,8 +1002,6 @@ let check_one_fix renv recpos trees def =
| (App _ | LetIn _ | Cast _) -> assert false (* beta zeta reduction *)
- | Proj (p, c) -> check_rec_call renv [] c
-
and check_nested_fix_body renv decr recArgsDecrArg body =
if decr = 0 then
check_rec_call (assign_var_spec renv (1,recArgsDecrArg)) [] body
@@ -1075,10 +1034,10 @@ let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) =
(* check fi does not appear in the k+1 first abstractions,
gives the type of the k+1-eme abstraction (must be an inductive) *)
let rec check_occur env n def =
- match (whd_betadeltaiota env def) with
+ match (whd_all env def) with
| Lambda (x,a,b) ->
if noccur_with_meta n nbfix a then
- let env' = push_rel (x, None, a) env in
+ let env' = push_rel (LocalAssum (x,a)) env in
if n = k+1 then
(* get the inductive type of the fixpoint *)
let (mind, _) =
@@ -1124,10 +1083,10 @@ let anomaly_ill_typed () =
anomaly ~label:"check_one_cofix" (Pp.str "too many arguments applied to constructor")
let rec codomain_is_coind env c =
- let b = whd_betadeltaiota env c in
+ let b = whd_all env c in
match b with
| Prod (x,a,b) ->
- codomain_is_coind (push_rel (x, None, a) env) b
+ codomain_is_coind (push_rel (LocalAssum (x,a)) env) b
| _ ->
(try find_coinductive env b
with Not_found ->
@@ -1136,7 +1095,7 @@ let rec codomain_is_coind env c =
let check_one_cofix env nbfix def deftype =
let rec check_rec_call env alreadygrd n tree vlra t =
if not (noccur_with_meta n nbfix t) then
- let c,args = decompose_app (whd_betadeltaiota env t) in
+ let c,args = decompose_app (whd_all env t) in
match c with
| Rel p when n <= p && p < n+nbfix ->
(* recursive call: must be guarded and no nested recursive
@@ -1168,7 +1127,7 @@ let check_one_cofix env nbfix def deftype =
| Lambda (x,a,b) ->
assert (args = []);
if noccur_with_meta n nbfix a then
- let env' = push_rel (x, None, a) env in
+ let env' = push_rel (LocalAssum (x,a)) env in
check_rec_call env' alreadygrd (n+1) tree vlra b
else
raise (CoFixGuardError (env,RecCallInTypeOfAbstraction a))
generated by cgit v1.2.3 (git 2.39.1) at 2024-10-31 10:50:48 +0000