aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/inferCumulativity.ml
blob: a4097237ff4ef0957ba66f07e03ebdb2483c27e0 (plain)
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
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017     *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

open Reduction
open Declarations
open Constr
open Univ
open Util

(** Throughout this module we modify a map [variances] from local
   universes to [Variance.t]. It starts as a trivial mapping to
   [Irrelevant] and every time we encounter a local universe we
   restrict it accordingly. *)

let infer_level_eq u variances =
  if LMap.mem u variances
  then LMap.set u Variance.Invariant variances
  else variances

let infer_level_leq u variances =
  match LMap.find u variances with
  | exception Not_found -> variances
  | varu -> LMap.set u (Variance.sup varu Variance.Covariant) variances

let infer_generic_instance_eq variances u =
  Array.fold_left (fun variances u -> infer_level_eq u variances)
    variances (Instance.to_array u)

let variance_pb cv_pb var =
  let open Variance in
  match cv_pb, var with
  | _, Irrelevant -> Irrelevant
  | _, Invariant -> Invariant
  | CONV, Covariant -> Invariant
  | CUMUL, Covariant -> Covariant

let infer_cumulative_ind_instance cv_pb cumi variances u =
  Array.fold_left2 (fun variances varu u ->
      match LMap.find u variances with
      | exception Not_found -> variances
      | varu' ->
        LMap.set u (Variance.sup varu' (variance_pb cv_pb varu)) variances)
    variances (ACumulativityInfo.variance cumi) (Instance.to_array u)

let infer_inductive_instance cv_pb env variances ind nargs u =
  let mind = Environ.lookup_mind (fst ind) env in
  match mind.mind_universes with
  | Monomorphic_ind _ -> assert (Instance.is_empty u); variances
  | Polymorphic_ind _ -> infer_generic_instance_eq variances u
  | Cumulative_ind cumi ->
    if not (Int.equal (inductive_cumulativity_arguments (mind,snd ind)) nargs)
    then infer_generic_instance_eq variances u
    else infer_cumulative_ind_instance cv_pb cumi variances u

let infer_constructor_instance_eq env variances ((mi,ind),ctor) nargs u =
  let mind = Environ.lookup_mind mi env in
  match mind.mind_universes with
  | Monomorphic_ind _ -> assert (Instance.is_empty u); variances
  | Polymorphic_ind _ -> infer_generic_instance_eq variances u
  | Cumulative_ind cumi ->
    if not (Int.equal (constructor_cumulativity_arguments (mind,ind,ctor)) nargs)
    then infer_generic_instance_eq variances u
    else infer_cumulative_ind_instance CONV cumi variances u

let infer_sort cv_pb variances s =
  match cv_pb with
  | CONV ->
    LSet.fold infer_level_eq (Universe.levels (Sorts.univ_of_sort s)) variances
  | CUMUL ->
    LSet.fold infer_level_leq (Universe.levels (Sorts.univ_of_sort s)) variances

let infer_table_key infos variances c =
  let open Names in
  match c with
  | ConstKey (_, u) ->
    infer_generic_instance_eq variances u
  | VarKey _ | RelKey _ -> variances

let rec infer_fterm cv_pb infos variances hd stk =
  Control.check_for_interrupt ();
  let open CClosure in
  let hd,stk = whd_stack infos hd stk in
  match fterm_of hd with
  | FAtom a ->
    begin match kind a with
      | Sort s -> infer_sort cv_pb variances s
      | Meta _ -> infer_stack infos variances stk
      | _ -> assert false
    end
  | FEvar ((_,args),e) ->
    let variances = infer_stack infos variances stk in
    infer_vect infos variances (Array.map (mk_clos e) args)
  | FRel _ -> variances
  | FFlex fl ->
    let variances = infer_table_key infos variances fl in
    infer_stack infos variances stk
  | FProj (_,c) ->
    let variances = infer_fterm CONV infos variances c [] in
    infer_stack infos variances stk
  | FLambda _ ->
    let (_,ty,bd) = destFLambda mk_clos hd in
    let variances = infer_fterm CONV infos variances ty [] in
    infer_fterm CONV infos variances bd []
  | FProd (_,dom,codom) ->
    let variances = infer_fterm CONV infos variances dom [] in
    infer_fterm cv_pb infos variances codom []
  | FInd (ind, u) ->
    let variances =
      if Instance.is_empty u then variances
      else
        let nargs = stack_args_size stk in
        infer_inductive_instance cv_pb (info_env infos) variances ind nargs u
    in
    infer_stack infos variances stk
  | FConstruct (ctor,u) ->
    let variances =
      if Instance.is_empty u then variances
      else
        let nargs = stack_args_size stk in
        infer_constructor_instance_eq (info_env infos) variances ctor nargs u
    in
    infer_stack infos variances stk
  | FFix ((_,(_,tys,cl)),e) | FCoFix ((_,(_,tys,cl)),e) ->
    let n = Array.length cl in
    let variances = infer_vect infos variances (Array.map (mk_clos e) tys) in
    let le = Esubst.subs_liftn n e in
    let variances = infer_vect infos variances (Array.map (mk_clos le) cl) in
    infer_stack infos variances stk

  (* Removed by whnf *)
  | FLOCKED | FCaseT _ | FCast _ | FLetIn _ | FApp _ | FLIFT _ | FCLOS _ -> assert false

and infer_stack infos variances (stk:CClosure.stack) =
  match stk with
  | [] -> variances
  | z :: stk ->
    let open CClosure in
    let variances = match z with
      | Zapp v -> infer_vect infos variances v
      | Zproj _ -> variances
      | Zfix (fx,a) ->
        let variances = infer_fterm CONV infos variances fx [] in
        infer_stack infos variances a
      | ZcaseT (ci,p,br,e) ->
        let variances = infer_fterm CONV infos variances (mk_clos e p) [] in
        infer_vect infos variances (Array.map (mk_clos e) br)
      | Zshift _ -> variances
      | Zupdate _ -> variances
    in
    infer_stack infos variances stk

and infer_vect infos variances v =
  Array.fold_left (fun variances c -> infer_fterm CONV infos variances c []) variances v

let infer_term cv_pb env variances c =
  let open CClosure in
  let infos = create_clos_infos all env in
  infer_fterm cv_pb infos variances (CClosure.inject c) []

let infer_arity_constructor is_arity env variances arcn =
  let infer_typ typ (env,variances) =
    match typ with
    | Context.Rel.Declaration.LocalAssum (_, typ') ->
      (Environ.push_rel typ env, infer_term CUMUL env variances typ')
    | Context.Rel.Declaration.LocalDef _ -> assert false
  in
  let typs, codom = Reduction.dest_prod env arcn in
  let env, variances = Context.Rel.fold_outside infer_typ typs ~init:(env, variances) in
  (* If we have Inductive foo@{i j} : ... -> Type@{i} := C : ... -> foo Type@{j}
     i is irrelevant, j is invariant. *)
  if not is_arity then infer_term CUMUL env variances codom else variances

let infer_inductive env mie =
  let open Entries in
  let { mind_entry_params = params;
        mind_entry_inds = entries; } = mie
  in
  let univs =
    match mie.mind_entry_universes with
    | Monomorphic_ind_entry _
    | Polymorphic_ind_entry _ as univs -> univs
    | Cumulative_ind_entry cumi ->
      let uctx = CumulativityInfo.univ_context cumi in
      let uarray = Instance.to_array @@ UContext.instance uctx in
      let env = Environ.push_context uctx env in
      let variances =
        Array.fold_left (fun variances u -> LMap.add u Variance.Irrelevant variances)
          LMap.empty uarray
      in
      let env, _ = Typeops.infer_local_decls env params in
      let variances = List.fold_left (fun variances entry ->
          let variances = infer_arity_constructor true
              env variances entry.mind_entry_arity
          in
          List.fold_left (infer_arity_constructor false env)
            variances entry.mind_entry_lc)
          variances
          entries
      in
      let variances = Array.map (fun u -> LMap.find u variances) uarray in
      Cumulative_ind_entry (CumulativityInfo.make (uctx, variances))
  in
  { mie with mind_entry_universes = univs }