diff options
| -rw-r--r-- | kernel/reduction.ml | 10 | ||||
| -rw-r--r-- | kernel/retypeops.ml | 30 | ||||
| -rw-r--r-- | kernel/retypeops.mli | 4 | ||||
| -rw-r--r-- | pretyping/retyping.ml | 13 |
4 files changed, 28 insertions, 29 deletions
diff --git a/kernel/reduction.ml b/kernel/reduction.ml index f2cb9a8aec..b7bd4eef9a 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -302,7 +302,7 @@ let unfold_ref_with_args infos tab fl v = type conv_tab = { cnv_inf : clos_infos; - relevances : Sorts.relevance list; + relevances : Sorts.relevance Range.t; lft_tab : clos_tab; rgt_tab : clos_tab; } @@ -313,16 +313,16 @@ type conv_tab = { passed to each respective side of the conversion function below. *) let push_relevance infos r = - { infos with relevances = r.Context.binder_relevance :: infos.relevances } + { infos with relevances = Range.cons r.Context.binder_relevance infos.relevances } let push_relevances infos nas = - { infos with relevances = Array.fold_left (fun l x -> x.Context.binder_relevance :: l) infos.relevances nas } + { infos with relevances = Array.fold_left (fun l x -> Range.cons x.Context.binder_relevance l) infos.relevances nas } let rec skip_pattern infos relevances n c1 c2 = if Int.equal n 0 then {infos with relevances}, c1, c2 else match kind c1, kind c2 with | Lambda (x, _, c1), Lambda (_, _, c2) -> - skip_pattern infos (x.Context.binder_relevance :: relevances) (pred n) c1 c2 + skip_pattern infos (Range.cons x.Context.binder_relevance relevances) (pred n) c1 c2 | _ -> raise IrregularPatternShape let skip_pattern infos n c1 c2 = @@ -705,7 +705,7 @@ let clos_gen_conv trans cv_pb l2r evars env univs t1 t2 = let infos = create_clos_infos ~evars reds env in let infos = { cnv_inf = infos; - relevances = List.map Context.Rel.Declaration.get_relevance (rel_context env); + relevances = Range.empty; lft_tab = create_tab (); rgt_tab = create_tab (); } in diff --git a/kernel/retypeops.ml b/kernel/retypeops.ml index 5c15257511..6a1b36ea94 100644 --- a/kernel/retypeops.ml +++ b/kernel/retypeops.ml @@ -39,16 +39,10 @@ let relevance_of_projection env p = let mib = lookup_mind mind env in Declareops.relevance_of_projection_repr mib (Projection.repr p) -let rec relevance_of_rel_extra env extra n = - match extra with - | [] -> relevance_of_rel env n - | r :: _ when Int.equal n 1 -> r - | _ :: extra -> relevance_of_rel_extra env extra (n-1) - -let relevance_of_flex env extra lft = function +let relevance_of_flex env = function | ConstKey (c,_) -> relevance_of_constant env c | VarKey x -> relevance_of_var env x - | RelKey p -> relevance_of_rel_extra env extra (Esubst.reloc_rel p lft) + | RelKey p -> relevance_of_rel env p let rec relevance_of_fterm env extra lft f = let open CClosure in @@ -57,9 +51,9 @@ let rec relevance_of_fterm env extra lft f = | KnownI -> Sorts.Irrelevant | Unknown -> let r = match fterm_of f with - | FRel n -> relevance_of_rel_extra env extra (Esubst.reloc_rel n lft) + | FRel n -> Range.get extra (Esubst.reloc_rel n lft - 1) | FAtom c -> relevance_of_term_extra env extra lft (Esubst.subs_id 0) c - | FFlex key -> relevance_of_flex env extra lft key + | FFlex key -> relevance_of_flex env key | FInt _ | FFloat _ -> Sorts.Relevant | FInd _ | FProd _ -> Sorts.Relevant (* types are always relevant *) | FConstruct (c,_) -> relevance_of_constructor env c @@ -69,12 +63,12 @@ let rec relevance_of_fterm env extra lft f = | FCoFix ((i,(lna,_,_)), _) -> (lna.(i)).binder_relevance | FCaseT (ci, _, _, _, _) -> ci.ci_relevance | FLambda (len, tys, bdy, e) -> - let extra = List.rev_append (List.map (fun (x,_) -> binder_relevance x) tys) extra in + let extra = List.fold_left (fun accu (x, _) -> Range.cons (binder_relevance x) accu) extra tys in let lft = Esubst.el_liftn len lft in let e = Esubst.subs_liftn len e in relevance_of_term_extra env extra lft e bdy | FLetIn (x, _, _, bdy, e) -> - relevance_of_term_extra env (x.binder_relevance :: extra) + relevance_of_term_extra env (Range.cons x.binder_relevance extra) (Esubst.el_lift lft) (Esubst.subs_lift e) bdy | FLIFT (k, f) -> relevance_of_fterm env extra (Esubst.el_shft k lft) f | FCLOS (c, e) -> relevance_of_term_extra env extra lft e c @@ -88,16 +82,18 @@ let rec relevance_of_fterm env extra lft f = and relevance_of_term_extra env extra lft subs c = match kind c with | Rel n -> - (match Esubst.expand_rel n subs with + begin match Esubst.expand_rel n subs with | Inl (k, f) -> relevance_of_fterm env extra (Esubst.el_liftn k lft) f - | Inr (n, _) -> relevance_of_rel_extra env extra (Esubst.reloc_rel n lft)) + | Inr (n, None) -> Range.get extra (Esubst.reloc_rel n lft - 1) + | Inr (_, Some p) -> relevance_of_rel env p + end | Var x -> relevance_of_var env x | Sort _ | Ind _ | Prod _ -> Sorts.Relevant (* types are always relevant *) | Cast (c, _, _) -> relevance_of_term_extra env extra lft subs c | Lambda ({binder_relevance=r;_}, _, bdy) -> - relevance_of_term_extra env (r::extra) (Esubst.el_lift lft) (Esubst.subs_lift subs) bdy + relevance_of_term_extra env (Range.cons r extra) (Esubst.el_lift lft) (Esubst.subs_lift subs) bdy | LetIn ({binder_relevance=r;_}, _, _, bdy) -> - relevance_of_term_extra env (r::extra) (Esubst.el_lift lft) (Esubst.subs_lift subs) bdy + relevance_of_term_extra env (Range.cons r extra) (Esubst.el_lift lft) (Esubst.subs_lift subs) bdy | App (c, _) -> relevance_of_term_extra env extra lft subs c | Const (c,_) -> relevance_of_constant env c | Construct (c,_) -> relevance_of_constructor env c @@ -115,5 +111,5 @@ let relevance_of_fterm env extra lft c = let relevance_of_term env c = if Environ.sprop_allowed env - then relevance_of_term_extra env [] Esubst.el_id (Esubst.subs_id 0) c + then relevance_of_term_extra env Range.empty Esubst.el_id (Esubst.subs_id 0) c else Sorts.Relevant diff --git a/kernel/retypeops.mli b/kernel/retypeops.mli index f4497be44b..dd4513959f 100644 --- a/kernel/retypeops.mli +++ b/kernel/retypeops.mli @@ -14,14 +14,14 @@ val relevance_of_term : Environ.env -> Constr.constr -> Sorts.relevance -val relevance_of_fterm : Environ.env -> Sorts.relevance list -> +val relevance_of_fterm : Environ.env -> Sorts.relevance Range.t -> Esubst.lift -> CClosure.fconstr -> Sorts.relevance (** Helpers *) open Names -val relevance_of_rel_extra : Environ.env -> Sorts.relevance list -> int -> Sorts.relevance +val relevance_of_rel : Environ.env -> int -> Sorts.relevance val relevance_of_var : Environ.env -> Id.t -> Sorts.relevance val relevance_of_constant : Environ.env -> Constant.t -> Sorts.relevance val relevance_of_constructor : Environ.env -> constructor -> Sorts.relevance diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index f089b242a2..d2af957b54 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -264,16 +264,19 @@ let relevance_of_term env sigma c = if Environ.sprop_allowed env then let rec aux rels c = match kind sigma c with - | Rel n -> Retypeops.relevance_of_rel_extra env rels n + | Rel n -> + let len = Range.length rels in + if n <= len then Range.get rels (n - 1) + else Retypeops.relevance_of_rel env (n - len) | Var x -> Retypeops.relevance_of_var env x | Sort _ -> Sorts.Relevant | Cast (c, _, _) -> aux rels c | Prod ({binder_relevance=r}, _, codom) -> - aux (r::rels) codom + aux (Range.cons r rels) codom | Lambda ({binder_relevance=r}, _, bdy) -> - aux (r::rels) bdy + aux (Range.cons r rels) bdy | LetIn ({binder_relevance=r}, _, _, bdy) -> - aux (r::rels) bdy + aux (Range.cons r rels) bdy | App (c, _) -> aux rels c | Const (c,_) -> Retypeops.relevance_of_constant env c | Ind _ -> Sorts.Relevant @@ -287,7 +290,7 @@ let relevance_of_term env sigma c = | Meta _ | Evar _ -> Sorts.Relevant in - aux [] c + aux Range.empty c else Sorts.Relevant let relevance_of_type env sigma t = |