diff options
Diffstat (limited to 'kernel/inductive.ml')
| -rw-r--r-- | kernel/inductive.ml | 50 |
1 files changed, 26 insertions, 24 deletions
diff --git a/kernel/inductive.ml b/kernel/inductive.ml index dd49c4a1b..ca29d83f6 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -17,6 +17,7 @@ open Declareops open Environ open Reduction open Type_errors +open Context.Rel.Declaration type mind_specif = mutual_inductive_body * one_inductive_body @@ -77,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) = Context.Rel.fold_outside - (fun (_,copt,_) (largs,subs,ty) -> - match (copt, largs, kind_of_term ty) with - | (None, a::args, Prod(_,_,t)) -> (args, a::subs, t) - | (Some b,_,LetIn(_,_,_,t)) -> + (fun decl (largs,subs,ty) -> + match (decl, largs, kind_of_term 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 ()) @@ -152,7 +153,7 @@ let remember_subst u subst = (* Propagate the new levels in the signature *) let 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 @@ -165,7 +166,7 @@ let make_subst env = (* a useless extra constraint *) let s = sort_as_univ (snd (dest_arity env (Lazy.force 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 *) @@ -314,14 +315,14 @@ let is_correct_arity env c pj ind specif params = let rec srec env pt ar = let pt' = whd_betadeltaiota env pt in match kind_of_term pt', ar with - | Prod (na1,a1,t), (_,None,a1')::ar' -> + | Prod (na1,a1,t), (LocalAssum (_,a1'))::ar' -> let () = try conv env a1 a1' with NotConvertible -> raise (LocalArity None) in - srec (push_rel (na1,None,a1) env) t ar' + srec (push_rel (LocalAssum (na1,a1)) env) t ar' (* The last Prod domain is the type of the scrutinee *) | Prod (na1,a1,a2), [] -> (* whnf of t was not needed here! *) - let env' = push_rel (na1,None,a1) env in + let env' = push_rel (LocalAssum (na1,a1)) env in let ksort = match kind_of_term (whd_betadeltaiota env' a2) with | Sort s -> family_of_sort s | _ -> raise (LocalArity None) in @@ -330,7 +331,7 @@ let is_correct_arity env c pj ind specif params = try conv env a1 dep_ind with NotConvertible -> raise (LocalArity None) in check_allowed_sort ksort specif - | _, (_,Some _,_ as d)::ar' -> + | _, (LocalDef _ as d)::ar' -> srec (push_rel d env) (lift 1 pt') ar' | _ -> raise (LocalArity None) @@ -482,7 +483,7 @@ let make_renv env recarg tree = genv = [Lazy.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 } @@ -568,14 +569,14 @@ let check_inductive_codomain env p = (* 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 @@ -848,7 +849,7 @@ let filter_stack_domain env ci p stack = let t = whd_betadeltaiota env ar in match stack, kind_of_term t with | elt :: stack', Prod (n,a,c0) -> - let d = (n,None,a) in + let d = LocalAssum (n,a) in let ty, args = decompose_app (whd_betadeltaiota env a) in let elt = match kind_of_term ty with | Ind ind -> @@ -905,10 +906,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)) @@ -983,10 +984,11 @@ let check_one_fix renv recpos trees def = | Var id -> begin - match pi2 (lookup_named id renv.env) with - | None -> + let open Context.Named.Declaration in + match lookup_named id 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(c,l)) @@ -1040,7 +1042,7 @@ let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) = match kind_of_term (whd_betadeltaiota 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 Int.equal n (k + 1) then (* get the inductive type of the fixpoint *) let (mind, _) = @@ -1090,7 +1092,7 @@ let rec codomain_is_coind env c = let b = whd_betadeltaiota env c in match kind_of_term 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 -> @@ -1131,7 +1133,7 @@ let check_one_cofix env nbfix def deftype = | Lambda (x,a,b) -> let () = assert (List.is_empty args) in 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)) |