diff options
Diffstat (limited to 'kernel/inductive.ml')
| -rw-r--r-- | kernel/inductive.ml | 76 |
1 files changed, 34 insertions, 42 deletions
diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 9bed598bb7..9bbcf07f7e 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -130,11 +130,6 @@ where Remark: Set (predicative) is encoded as Type(0) *) -let sort_as_univ = let open Sorts in function -| Type u -> u -| Prop Null -> Universe.type0m -| Prop Pos -> Universe.type0 - (* Template polymorphism *) (* cons_subst add the mapping [u |-> su] in subst if [u] is not *) @@ -159,18 +154,18 @@ let make_subst env = let rec make subst = function | LocalDef _ :: sign, exp, args -> make subst (sign, exp, args) - | d::sign, None::exp, args -> + | _d::sign, None::exp, args -> let args = match args with _::args -> args | [] -> [] in make subst (sign, exp, args) - | d::sign, Some u::exp, a::args -> + | _d::sign, Some u::exp, a::args -> (* We recover the level of the argument, but we don't change the *) (* level in the corresponding type in the arity; this level in the *) (* arity is a global level which, at typing time, will be enforce *) (* to be greater than the level of the argument; this is probably *) (* a useless extra constraint *) - let s = sort_as_univ (snd (dest_arity env (Lazy.force a))) in + let s = Sorts.univ_of_sort (snd (dest_arity env (Lazy.force a))) in make (cons_subst u s subst) (sign, exp, args) - | LocalAssum (na,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 *) @@ -178,7 +173,7 @@ let make_subst env = (* update its image [x] by [sup x u] in order not to forget the *) (* dependency in [u] that remains to be fullfilled. *) make (remember_subst u subst) (sign, exp, []) - | sign, [], _ -> + | _sign, [], _ -> (* Uniform parameters are exhausted *) subst | [], _, _ -> @@ -204,7 +199,7 @@ let instantiate_universes env ctx ar argsorts = (* Type of an inductive type *) -let type_of_inductive_gen ?(polyprop=true) env ((mib,mip),u) paramtyps = +let type_of_inductive_gen ?(polyprop=true) env ((_mib,mip),u) paramtyps = match mip.mind_arity with | RegularArity a -> subst_instance_constr u a.mind_user_arity | TemplateArity ar -> @@ -220,12 +215,12 @@ let type_of_inductive_gen ?(polyprop=true) env ((mib,mip),u) paramtyps = let type_of_inductive env pind = type_of_inductive_gen env pind [||] -let constrained_type_of_inductive env ((mib,mip),u as pind) = +let constrained_type_of_inductive env ((mib,_mip),u as pind) = let ty = type_of_inductive 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 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) @@ -236,8 +231,8 @@ let type_of_inductive_knowing_parameters env ?(polyprop=true) mip args = (* The max of an array of universes *) let cumulate_constructor_univ u = let open Sorts in function - | Prop Null -> u - | Prop Pos -> Universe.sup Universe.type0 u + | Prop -> u + | Set -> Universe.sup Universe.type0 u | Type u' -> Universe.sup u u' let max_inductive_sort = @@ -254,7 +249,7 @@ let type_of_constructor (cstr, u) (mib,mip) = if i > nconstr then user_err Pp.(str "Not enough constructors in the type."); constructor_instantiate (fst ind) u mib specif.(i-1) -let constrained_type_of_constructor (cstr,u as cstru) (mib,mip as ind) = +let constrained_type_of_constructor (_cstr,u as cstru) (mib,_mip as ind) = let ty = type_of_constructor cstru ind in let cst = instantiate_inductive_constraints mib u in (ty, cst) @@ -284,7 +279,7 @@ let inductive_sort_family mip = let mind_arity mip = mip.mind_arity_ctxt, inductive_sort_family mip -let get_instantiated_arity (ind,u) (mib,mip) params = +let get_instantiated_arity (_ind,u) (mib,mip) params = let sign, s = mind_arity mip in full_inductive_instantiate mib u params sign, s @@ -293,8 +288,8 @@ let elim_sorts (_,mip) = mip.mind_kelim let is_private (mib,_) = mib.mind_private = Some true let is_primitive_record (mib,_) = match mib.mind_record with - | Some (Some _) -> true - | _ -> false + | PrimRecord _ -> true + | NotRecord | FakeRecord -> false let build_dependent_inductive ind (_,mip) params = let realargs,_ = List.chop mip.mind_nrealdecls mip.mind_arity_ctxt in @@ -568,7 +563,7 @@ 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_all env s) in + let i,_l' = decompose_app (whd_all env s) in isInd i (* The following functions are almost duplicated from indtypes.ml, except @@ -640,10 +635,10 @@ let get_recargs_approx env tree ind args = build_recargs_nested ienv tree (ind_kn, largs) | _ -> mk_norec end - | err -> + | _err -> mk_norec - and build_recargs_nested (env,ra_env as ienv) tree (((mind,i),u), largs) = + and build_recargs_nested (env,_ra_env as ienv) tree (((mind,i),u), largs) = (* If the inferred tree already disallows recursion, no need to go further *) if eq_wf_paths tree mk_norec then tree else @@ -681,7 +676,7 @@ let get_recargs_approx env tree ind args = (Rtree.mk_rec irecargs).(i) and build_recargs_constructors ienv trees c = - let rec recargs_constr_rec (env,ra_env as ienv) trees lrec c = + let rec recargs_constr_rec (env,_ra_env as ienv) trees lrec c = let x,largs = decompose_app (whd_all env c) in match kind x with @@ -690,7 +685,7 @@ let get_recargs_approx env tree ind args = let recarg = build_recargs ienv (List.hd trees) b in let ienv' = ienv_push_var ienv (na,b,mk_norec) in recargs_constr_rec ienv' (List.tl trees) (recarg::lrec) d - | hd -> + | _hd -> List.rev lrec in recargs_constr_rec ienv trees [] c @@ -790,7 +785,7 @@ let rec subterm_specif renv stack t = | Lambda (x,a,b) -> let () = assert (List.is_empty l) in - let spec,stack' = extract_stack renv a stack in + let spec,stack' = extract_stack stack in subterm_specif (push_var renv (x,a,spec)) stack' b (* Metas and evars are considered OK *) @@ -799,14 +794,11 @@ let rec subterm_specif renv stack t = | Proj (p, c) -> let subt = subterm_specif renv stack c in (match subt with - | Subterm (s, wf) -> + | Subterm (_s, wf) -> (* We take the subterm specs of the constructor of the record *) let wf_args = (dest_subterms wf).(0) in (* We extract the tree of the projected argument *) - let kn = Projection.constant p in - let cb = lookup_constant kn renv.env in - let pb = Option.get cb.const_proj in - let n = pb.proj_arg in + let n = Projection.arg p in spec_of_tree (List.nth wf_args n) | Dead_code -> Dead_code | Not_subterm -> Not_subterm) @@ -824,7 +816,7 @@ and stack_element_specif = function |SClosure (h_renv,h) -> lazy_subterm_specif h_renv [] h |SArg x -> x -and extract_stack renv a = function +and extract_stack = function | [] -> Lazy.from_val Not_subterm , [] | h::t -> stack_element_specif h, t @@ -855,7 +847,7 @@ let error_illegal_rec_call renv fx (arg_renv,arg) = let error_partial_apply renv fx = raise (FixGuardError (renv.env,NotEnoughArgumentsForFixCall fx)) -let filter_stack_domain env ci p stack = +let filter_stack_domain env p stack = let absctx, ar = dest_lam_assum env p in (* Optimization: if the predicate is not dependent, no restriction is needed and we avoid building the recargs tree. *) @@ -940,7 +932,7 @@ let check_one_fix renv recpos trees def = let case_spec = branches_specif renv (lazy_subterm_specif renv [] c_0) ci in let stack' = push_stack_closures renv l stack in - let stack' = filter_stack_domain renv.env ci p stack' in + let stack' = filter_stack_domain renv.env p stack' in Array.iteri (fun k br' -> let stack_br = push_stack_args case_spec.(k) stack' in check_rec_call renv stack_br br') lrest @@ -972,7 +964,7 @@ let check_one_fix renv recpos trees def = else check_rec_call renv' [] body) bodies - | Const (kn,u as cu) -> + | Const (kn,_u as cu) -> if evaluable_constant kn renv.env then try List.iter (check_rec_call renv []) l with (FixGuardError _ ) -> @@ -983,7 +975,7 @@ let check_one_fix renv recpos trees def = | Lambda (x,a,b) -> let () = assert (List.is_empty l) in check_rec_call renv [] a ; - let spec, stack' = extract_stack renv a stack in + let spec, stack' = extract_stack stack in check_rec_call (push_var renv (x,a,spec)) stack' b | Prod (x,a,b) -> @@ -991,7 +983,7 @@ let check_one_fix renv recpos trees def = check_rec_call renv [] a; check_rec_call (push_var_renv renv (x,a)) [] b - | CoFix (i,(_,typarray,bodies as recdef)) -> + | CoFix (_i,(_,typarray,bodies as recdef)) -> List.iter (check_rec_call renv []) l; Array.iter (check_rec_call renv []) typarray; let renv' = push_fix_renv renv recdef in @@ -1000,13 +992,13 @@ let check_one_fix renv recpos trees def = | (Ind _ | Construct _) -> List.iter (check_rec_call renv []) l - | Proj (p, c) -> + | Proj (_p, c) -> List.iter (check_rec_call renv []) l; check_rec_call renv [] c | Var id -> begin - let open Context.Named.Declaration in + let open! Context.Named.Declaration in match lookup_named id renv.env with | LocalAssum _ -> List.iter (check_rec_call renv []) l @@ -1137,10 +1129,10 @@ let check_one_cofix env nbfix def deftype = raise (CoFixGuardError (env,UnguardedRecursiveCall t)) else if not(List.for_all (noccur_with_meta n nbfix) args) then raise (CoFixGuardError (env,NestedRecursiveOccurrences)) - | Construct ((_,i as cstr_kn),u) -> + | Construct ((_,i as cstr_kn),_u) -> let lra = vlra.(i-1) in let mI = inductive_of_constructor cstr_kn in - let (mib,mip) = lookup_mind_specif env mI in + let (mib,_mip) = lookup_mind_specif env mI in let realargs = List.skipn mib.mind_nparams args in let rec process_args_of_constr = function | (t::lr), (rar::lrar) -> @@ -1165,7 +1157,7 @@ let check_one_cofix env nbfix def deftype = else raise (CoFixGuardError (env,RecCallInTypeOfAbstraction a)) - | CoFix (j,(_,varit,vdefs as recdef)) -> + | CoFix (_j,(_,varit,vdefs as recdef)) -> if List.for_all (noccur_with_meta n nbfix) args then if Array.for_all (noccur_with_meta n nbfix) varit then @@ -1211,7 +1203,7 @@ let check_one_cofix env nbfix def deftype = (* The function which checks that the whole block of definitions satisfies the guarded condition *) -let check_cofix env (bodynum,(names,types,bodies as recdef)) = +let check_cofix env (_bodynum,(names,types,bodies as recdef)) = let flags = Environ.typing_flags env in if flags.check_guarded then let nbfix = Array.length bodies in |