summaryrefslogtreecommitdiff
path: root/checker/indtypes.ml
diff options
context:
space:
mode:
Diffstat (limited to 'checker/indtypes.ml')
-rw-r--r--checker/indtypes.ml47
1 files changed, 24 insertions, 23 deletions
diff --git a/checker/indtypes.ml b/checker/indtypes.ml
index 2865f5bd..27f79e79 100644
--- a/checker/indtypes.ml
+++ b/checker/indtypes.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Errors
+open CErrors
open Util
open Names
open Cic
@@ -32,11 +32,11 @@ let string_of_mp mp =
if !Flags.debug then debug_string_of_mp mp else string_of_mp mp
let prkn kn =
- let (mp,_,l) = repr_kn kn in
+ let (mp,_,l) = KerName.repr kn in
str(string_of_mp mp ^ "." ^ Label.to_string l)
let prcon c =
- let ck = canonical_con c in
- let uk = user_con c in
+ let ck = Constant.canonical c in
+ let uk = Constant.user c in
if KerName.equal ck uk then prkn uk else (prkn uk ++str"(="++prkn ck++str")")
(* Same as noccur_between but may perform reductions.
@@ -44,7 +44,7 @@ let prcon c =
let weaker_noccur_between env x nvars t =
if noccur_between x nvars t then Some t
else
- let t' = whd_betadeltaiota env t in
+ let t' = whd_all env t in
if noccur_between x nvars t' then Some t'
else None
@@ -56,10 +56,10 @@ let is_constructor_head t =
let conv_ctxt_prefix env (ctx1:rel_context) ctx2 =
let rec chk env rctx1 rctx2 =
match rctx1, rctx2 with
- (_,None,ty1 as d1)::rctx1', (_,None,ty2)::rctx2' ->
+ (LocalAssum (_,ty1) as d1)::rctx1', LocalAssum (_,ty2)::rctx2' ->
conv env ty1 ty2;
chk (push_rel d1 env) rctx1' rctx2'
- | (_,Some bd1,ty1 as d1)::rctx1', (_,Some bd2,ty2)::rctx2' ->
+ | (LocalDef (_,bd1,ty1) as d1)::rctx1', LocalDef (_,bd2,ty2)::rctx2' ->
conv env ty1 ty2;
conv env bd1 bd2;
chk (push_rel d1 env) rctx1' rctx2'
@@ -90,14 +90,14 @@ exception InductiveError of inductive_error
(* Typing the arities and constructor types *)
let rec sorts_of_constr_args env t =
- let t = whd_betadeltaiota_nolet env t in
+ let t = whd_allnolet env t in
match t with
| Prod (name,c1,c2) ->
let varj = infer_type env c1 in
- let env1 = push_rel (name,None,c1) env in
+ let env1 = push_rel (LocalAssum (name,c1)) env in
varj :: sorts_of_constr_args env1 c2
| LetIn (name,def,ty,c) ->
- let env1 = push_rel (name,Some def,ty) env in
+ let env1 = push_rel (LocalDef (name,def,ty)) env in
sorts_of_constr_args env1 c
| _ when is_constructor_head t -> []
| _ -> anomaly ~label:"infos_and_sort" (Pp.str "not a positive constructor")
@@ -167,7 +167,7 @@ let typecheck_arity env params inds =
full_arity is used as argument or subject to cast, an
upper universe will be generated *)
let id = ind.mind_typename in
- let env_ar' = push_rel (Name id, None, arity) env_ar in
+ let env_ar' = push_rel (LocalAssum (Name id, arity)) env_ar in
env_ar')
env
inds in
@@ -176,7 +176,7 @@ let typecheck_arity env params inds =
(* Allowed eliminations *)
let check_predicativity env s small level =
- match s, fst (engagement env) with
+ match s, engagement env with
Type u, _ ->
(* let u' = fresh_local_univ () in *)
(* let cst = *)
@@ -319,9 +319,9 @@ let check_correct_par (env,n,ntypes,_) hyps l largs =
let nhyps = List.length hyps in
let rec check k index = function
| [] -> ()
- | (_,Some _,_)::hyps -> check k (index+1) hyps
+ | LocalDef _ :: hyps -> check k (index+1) hyps
| _::hyps ->
- match whd_betadeltaiota env lpar.(k) with
+ match whd_all env lpar.(k) with
| Rel w when w = index -> check (k-1) (index+1) hyps
| _ -> raise (IllFormedInd (LocalNonPar (k+1,index,l)))
in check (nparams-1) (n-nhyps) hyps;
@@ -340,9 +340,9 @@ let check_rec_par (env,n,_,_) hyps nrecp largs =
| ([],_) -> ()
| (_,[]) ->
failwith "number of recursive parameters cannot be greater than the number of parameters."
- | (lp,(_,Some _,_)::hyps) -> find (index-1) (lp,hyps)
+ | (lp,LocalDef _ :: hyps) -> find (index-1) (lp,hyps)
| (p::lp,_::hyps) ->
- (match whd_betadeltaiota env p with
+ (match whd_all env p with
| Rel w when w = index -> find (index-1) (lp,hyps)
| _ -> failwith "bad number of recursive parameters")
in find (n-1) (lpar,List.rev hyps)
@@ -370,14 +370,15 @@ let abstract_mind_lc env ntyps npars lc =
[lra] is the list of recursive tree of each variable
*)
let ienv_push_var (env, n, ntypes, lra) (x,a,ra) =
- (push_rel (x,None,a) env, n+1, ntypes, (Norec,ra)::lra)
+ (push_rel (LocalAssum (x,a)) env, n+1, ntypes, (Norec,ra)::lra)
let ienv_push_inductive (env, n, ntypes, ra_env) ((mi,u),lpar) =
let auxntyp = 1 in
let specif = lookup_mind_specif env mi in
let env' =
- push_rel (Anonymous,None,
- hnf_prod_applist env (type_of_inductive env (specif,u)) lpar) env in
+ let decl = LocalAssum (Anonymous,
+ hnf_prod_applist env (type_of_inductive env (specif,u)) lpar) in
+ push_rel decl env in
let ra_env' =
(Imbr mi,(Rtree.mk_rec_calls 1).(0)) ::
List.map (fun (r,t) -> (r,Rtree.lift 1 t)) ra_env in
@@ -387,7 +388,7 @@ let ienv_push_inductive (env, n, ntypes, ra_env) ((mi,u),lpar) =
let rec ienv_decompose_prod (env,_,_,_ as ienv) n c =
if 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
@@ -400,7 +401,7 @@ let check_positivity_one (env, _,ntypes,_ as ienv) hyps nrecp (_,i as ind) indlc
let lparams = rel_context_length hyps in
(* check the inductive types occur positively in [c] *)
let rec check_pos (env, n, ntypes, ra_env as ienv) 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);
@@ -469,7 +470,7 @@ let check_positivity_one (env, _,ntypes,_ as ienv) hyps nrecp (_,i as ind) indlc
and check_constructors ienv check_head c =
let rec check_constr_rec (env,n,ntypes,ra_env as ienv) 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) ->
assert (List.is_empty largs);
@@ -527,7 +528,7 @@ let check_positivity env_ar mind params nrecp inds =
(************************************************************************)
let check_inductive env kn mib =
- Flags.if_verbose ppnl (str " checking ind: " ++ pr_mind kn); pp_flush ();
+ Flags.if_verbose Feedback.msg_notice (str " checking ind: " ++ MutInd.print kn);
(* check mind_constraints: should be consistent with env *)
let env = add_constraints (Univ.UContext.constraints mib.mind_universes) env in
(* check mind_record : TODO ? check #constructor = 1 ? *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-06 00:09:37 +0000