kernel/retypeops.ml

  1
  2
  3
  4
  5
  6
  7
  8
  9
 10
 11
 12
 13
 14
 15
 16
 17
 18
 19
 20
 21
 22
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119

(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

open Util
open Names
open Constr
open Declarations
open Environ
open Context

module RelDecl = Context.Rel.Declaration

let relevance_of_rel env n =
  let decl = lookup_rel n env in
  RelDecl.get_relevance decl

let relevance_of_var env x =
  let decl = lookup_named x env in
  Context.Named.Declaration.get_relevance decl

let relevance_of_constant env c =
  let decl = lookup_constant c env in
  decl.const_relevance

let relevance_of_constructor env ((mi,i),_) =
  let decl = lookup_mind mi env in
  let packet = decl.mind_packets.(i) in
  packet.mind_relevance

let relevance_of_projection env p =
  let mind = Projection.mind p in
  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
  | 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)

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 -> relevance_of_rel_extra env extra (Esubst.reloc_rel n lft)
      | FAtom c -> relevance_of_term_extra env extra lft (Esubst.subs_id 0) c
      | FFlex key -> relevance_of_flex env extra lft key
      | FInt _ -> 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.rev_append (List.map (fun (x,_) -> binder_relevance x) tys) extra 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)
          (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 ->
    (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))
  | 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
  | LetIn ({binder_relevance=r;_}, _, _, bdy) ->
    relevance_of_term_extra env (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 _ -> 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 [] Esubst.el_id (Esubst.subs_id 0) c
  else Sorts.Relevant