From cb9413483bcd2a6bc91fb439343550bb6f425e5b Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Wed, 18 Mar 2020 17:57:12 +0100 Subject: Rename Retypeops -> Relevanceops This module used to do retyping for the kernel in prototypes of SProp, but was switched to only relevance inference before the merge. --- kernel/kernel.mllib | 2 +- kernel/reduction.ml | 2 +- kernel/relevanceops.ml | 115 ++++++++++++++++++++++++++++++++++++++++++++++++ kernel/relevanceops.mli | 28 ++++++++++++ kernel/retypeops.ml | 115 ------------------------------------------------ kernel/retypeops.mli | 28 ------------ kernel/term_typing.ml | 2 +- 7 files changed, 146 insertions(+), 146 deletions(-) create mode 100644 kernel/relevanceops.ml create mode 100644 kernel/relevanceops.mli delete mode 100644 kernel/retypeops.ml delete mode 100644 kernel/retypeops.mli (limited to 'kernel') diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib index f1e994b337..cc9da3a2ce 100644 --- a/kernel/kernel.mllib +++ b/kernel/kernel.mllib @@ -27,7 +27,7 @@ Conv_oracle Environ Primred CClosure -Retypeops +Relevanceops Reduction Clambda Nativelambda diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 5fbe501169..469d5ccaa2 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -331,7 +331,7 @@ let skip_pattern infos n c1 c2 = let is_irrelevant infos lft c = let env = info_env infos.cnv_inf in - try Retypeops.relevance_of_fterm env infos.relevances lft c == Sorts.Irrelevant with _ -> false + try Relevanceops.relevance_of_fterm env infos.relevances lft c == Sorts.Irrelevant with _ -> false (* Conversion between [lft1]term1 and [lft2]term2 *) let rec ccnv cv_pb l2r infos lft1 lft2 term1 term2 cuniv = diff --git a/kernel/relevanceops.ml b/kernel/relevanceops.ml new file mode 100644 index 0000000000..3f3e722245 --- /dev/null +++ b/kernel/relevanceops.ml @@ -0,0 +1,115 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* relevance_of_constant env c + | VarKey x -> relevance_of_var env x + | RelKey p -> relevance_of_rel env p + +let rec relevance_of_fterm env extra lft f = + let open CClosure in + match CClosure.relevance_of f with + | KnownR -> Sorts.Relevant + | KnownI -> Sorts.Irrelevant + | Unknown -> + let r = match fterm_of f with + | 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 key + | FInt _ | FFloat _ -> Sorts.Relevant + | FInd _ | FProd _ -> Sorts.Relevant (* types are always relevant *) + | FConstruct (c,_) -> relevance_of_constructor env c + | FApp (f, _) -> relevance_of_fterm env extra lft f + | FProj (p, _) -> relevance_of_projection env p + | FFix (((_,i),(lna,_,_)), _) -> (lna.(i)).binder_relevance + | FCoFix ((i,(lna,_,_)), _) -> (lna.(i)).binder_relevance + | FCaseT (ci, _, _, _, _) -> ci.ci_relevance + | FLambda (len, tys, bdy, e) -> + 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 (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 + + | FEvar (_, _) -> Sorts.Relevant (* let's assume evars are relevant for now *) + | FLOCKED -> assert false + in + CClosure.set_relevance r f; + r + +and relevance_of_term_extra env extra lft subs c = + match kind c with + | Rel n -> + begin match Esubst.expand_rel n subs with + | Inl (k, f) -> relevance_of_fterm env extra (Esubst.el_liftn k lft) f + | 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 (Range.cons r extra) (Esubst.el_lift lft) (Esubst.subs_lift subs) bdy + | LetIn ({binder_relevance=r;_}, _, _, 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 + | Case (ci, _, _, _) -> ci.ci_relevance + | Fix ((_,i),(lna,_,_)) -> (lna.(i)).binder_relevance + | CoFix (i,(lna,_,_)) -> (lna.(i)).binder_relevance + | Proj (p, _) -> relevance_of_projection env p + | Int _ | Float _ -> Sorts.Relevant + + | Meta _ | Evar _ -> Sorts.Relevant (* let's assume metas and evars are relevant for now *) + +let relevance_of_fterm env extra lft c = + if Environ.sprop_allowed env then relevance_of_fterm env extra lft c + else Sorts.Relevant + +let relevance_of_term env c = + if Environ.sprop_allowed env + then relevance_of_term_extra env Range.empty Esubst.el_id (Esubst.subs_id 0) c + else Sorts.Relevant diff --git a/kernel/relevanceops.mli b/kernel/relevanceops.mli new file mode 100644 index 0000000000..86734e747e --- /dev/null +++ b/kernel/relevanceops.mli @@ -0,0 +1,28 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* Constr.constr -> Sorts.relevance + +val relevance_of_fterm : Environ.env -> Sorts.relevance Range.t -> + Esubst.lift -> CClosure.fconstr -> + Sorts.relevance + + +(** Helpers *) +open Names +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 +val relevance_of_projection : Environ.env -> Projection.t -> Sorts.relevance diff --git a/kernel/retypeops.ml b/kernel/retypeops.ml deleted file mode 100644 index 3f3e722245..0000000000 --- a/kernel/retypeops.ml +++ /dev/null @@ -1,115 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* relevance_of_constant env c - | VarKey x -> relevance_of_var env x - | RelKey p -> relevance_of_rel env p - -let rec relevance_of_fterm env extra lft f = - let open CClosure in - match CClosure.relevance_of f with - | KnownR -> Sorts.Relevant - | KnownI -> Sorts.Irrelevant - | Unknown -> - let r = match fterm_of f with - | 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 key - | FInt _ | FFloat _ -> Sorts.Relevant - | FInd _ | FProd _ -> Sorts.Relevant (* types are always relevant *) - | FConstruct (c,_) -> relevance_of_constructor env c - | FApp (f, _) -> relevance_of_fterm env extra lft f - | FProj (p, _) -> relevance_of_projection env p - | FFix (((_,i),(lna,_,_)), _) -> (lna.(i)).binder_relevance - | FCoFix ((i,(lna,_,_)), _) -> (lna.(i)).binder_relevance - | FCaseT (ci, _, _, _, _) -> ci.ci_relevance - | FLambda (len, tys, bdy, e) -> - 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 (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 - - | FEvar (_, _) -> Sorts.Relevant (* let's assume evars are relevant for now *) - | FLOCKED -> assert false - in - CClosure.set_relevance r f; - r - -and relevance_of_term_extra env extra lft subs c = - match kind c with - | Rel n -> - begin match Esubst.expand_rel n subs with - | Inl (k, f) -> relevance_of_fterm env extra (Esubst.el_liftn k lft) f - | 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 (Range.cons r extra) (Esubst.el_lift lft) (Esubst.subs_lift subs) bdy - | LetIn ({binder_relevance=r;_}, _, _, 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 - | Case (ci, _, _, _) -> ci.ci_relevance - | Fix ((_,i),(lna,_,_)) -> (lna.(i)).binder_relevance - | CoFix (i,(lna,_,_)) -> (lna.(i)).binder_relevance - | Proj (p, _) -> relevance_of_projection env p - | Int _ | Float _ -> Sorts.Relevant - - | Meta _ | Evar _ -> Sorts.Relevant (* let's assume metas and evars are relevant for now *) - -let relevance_of_fterm env extra lft c = - if Environ.sprop_allowed env then relevance_of_fterm env extra lft c - else Sorts.Relevant - -let relevance_of_term env c = - if Environ.sprop_allowed env - 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 deleted file mode 100644 index 86734e747e..0000000000 --- a/kernel/retypeops.mli +++ /dev/null @@ -1,28 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* Constr.constr -> Sorts.relevance - -val relevance_of_fterm : Environ.env -> Sorts.relevance Range.t -> - Esubst.lift -> CClosure.fconstr -> - Sorts.relevance - - -(** Helpers *) -open Names -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 -val relevance_of_projection : Environ.env -> Projection.t -> Sorts.relevance diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 0c89d51033..c8c2301171 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -143,7 +143,7 @@ let infer_declaration env (dcl : constant_entry) = Cooking.cook_body = def; cook_type = typ; cook_universes = univs; - cook_relevance = Retypeops.relevance_of_term env j.uj_val; + cook_relevance = Relevanceops.relevance_of_term env j.uj_val; cook_inline = c.const_entry_inline_code; cook_context = c.const_entry_secctx; } -- cgit v1.2.3