package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Source file retrieveObl.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
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
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <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 Names

(**
   - Get types of existentials ;
   - Flatten dependency tree (prefix order) ;
   - Replace existentials by de Bruijn indices in term, applied to the right arguments ;
   - Apply term prefixed by quantification on "existentials".
*)

let check_evars env evm =
  Evar.Map.iter
    (fun key evi ->
      if Evd.is_obligation_evar evm key then ()
      else
        let loc, k = Evd.evar_source evi in
        Pretype_errors.error_unsolvable_implicit ?loc env evm key None)
    (Evd.undefined_map evm)

type obligation_info =
  ( Names.Id.t
  * Constr.types
  * Evar_kinds.t Loc.located
  * (bool * Evar_kinds.obligation_definition_status)
  * Int.Set.t
  * unit Proofview.tactic option )
  array

type oblinfo =
  { ev_name : int * Id.t
  ; ev_hyps : EConstr.named_context
  ; ev_status : bool * Evar_kinds.obligation_definition_status
  ; ev_chop : int option
  ; ev_src : Evar_kinds.t Loc.located
  ; ev_typ : Constr.types
  ; ev_tac : unit Proofview.tactic option
  ; ev_deps : Int.Set.t }

(** Substitute evar references in t using de Bruijn indices,
  where n binders were passed through. *)

let succfix (depth, fixrels) = (succ depth, List.map succ fixrels)

let subst_evar_constr evm evs n idf t =
  let seen = ref Int.Set.empty in
  let transparent = ref Id.Set.empty in
  let evar_info id = CList.assoc_f Evar.equal id evs in
  let rec substrec (depth, fixrels) c =
    match EConstr.kind evm c with
    | Constr.Evar (k, args) ->
      let {ev_name = id, idstr; ev_hyps = hyps; ev_chop = chop} =
        try evar_info k
        with Not_found ->
          CErrors.anomaly ~label:"eterm"
            Pp.(
              str "existential variable "
              ++ int (Evar.repr k)
              ++ str " not found.")
      in
      seen := Int.Set.add id !seen;
      (* Evar arguments are created in inverse order,
         and we must not apply to defined ones (i.e. LetIn's)
      *)
      let args =
        let args = Evd.expand_existential evm (k, args) in
        let n = match chop with None -> 0 | Some c -> c in
        let l, r = CList.chop n (List.rev args) in
        List.rev r
      in
      let args =
        let rec aux hyps args acc =
          let open Context.Named.Declaration in
          match (hyps, args) with
          | LocalAssum _ :: tlh, c :: tla ->
            aux tlh tla (substrec (depth, fixrels) c :: acc)
          | LocalDef _ :: tlh, _ :: tla -> aux tlh tla acc
          | [], [] -> acc
          | _, _ -> acc
          (*failwith "subst_evars: invalid argument"*)
        in
        aux hyps args []
      in
      if
        List.exists
          (fun x ->
            match EConstr.kind evm x with
            | Constr.Rel n -> Int.List.mem n fixrels
            | _ -> false)
          args
      then transparent := Id.Set.add idstr !transparent;
      EConstr.mkApp (idf idstr, Array.of_list args)
    | Constr.Fix _ ->
      EConstr.map_with_binders evm succfix substrec (depth, 1 :: fixrels) c
    | _ -> EConstr.map_with_binders evm succfix substrec (depth, fixrels) c
  in
  let t' = substrec (0, []) t in
  (EConstr.to_constr evm t', !seen, !transparent)

(** Substitute variable references in t using de Bruijn indices,
  where n binders were passed through. *)
let subst_vars acc n t =
  let var_index id = Util.List.index Id.equal id acc in
  let rec substrec depth c =
    match Constr.kind c with
    | Constr.Var v -> (
      try Constr.mkRel (depth + var_index v) with Not_found -> c )
    | _ -> Constr.map_with_binders succ substrec depth c
  in
  substrec 0 t

(** Rewrite type of an evar ([ H1 : t1, ... Hn : tn |- concl ])
    to a product : forall H1 : t1, ..., forall Hn : tn, concl.
    Changes evars and hypothesis references to variable references.
*)
let etype_of_evar evm evs hyps concl =
  let open Context.Named.Declaration in
  let rec aux acc n = function
    | decl :: tl -> (
      let t', s, trans =
        subst_evar_constr evm evs n EConstr.mkVar
          (Context.Named.Declaration.get_type decl)
      in
      let t'' = subst_vars acc 0 t' in
      let rest, s', trans' =
        aux (Context.Named.Declaration.get_id decl :: acc) (succ n) tl
      in
      let s' = Int.Set.union s s' in
      let trans' = Id.Set.union trans trans' in
      match decl with
      | LocalDef (id, c, _) ->
        let c', s'', trans'' = subst_evar_constr evm evs n EConstr.mkVar c in
        let c' = subst_vars acc 0 c' in
        ( Term.mkNamedProd_or_LetIn (LocalDef (id, c', t'')) rest
        , Int.Set.union s'' s'
        , Id.Set.union trans'' trans' )
      | LocalAssum (id, _) ->
        (Term.mkNamedProd_or_LetIn (LocalAssum (id, t'')) rest, s', trans') )
    | [] ->
      let t', s, trans = subst_evar_constr evm evs n EConstr.mkVar concl in
      (subst_vars acc 0 t', s, trans)
  in
  aux [] 0 (List.rev hyps)

let trunc_named_context n ctx =
  let len = List.length ctx in
  CList.firstn (len - n) ctx

let rec chop_product n t =
  let pop t = Vars.lift (-1) t in
  if Int.equal n 0 then Some t
  else
    match Constr.kind t with
    | Constr.Prod (_, _, b) ->
      if Vars.noccurn 1 b then chop_product (pred n) (pop b) else None
    | _ -> None

let evar_dependencies evm oev =
  let one_step deps =
    Evar.Set.fold
      (fun ev s ->
        let evi = Evd.find evm ev in
        let deps' = Evd.evars_of_filtered_evar_info evm evi in
        if Evar.Set.mem oev deps' then
          invalid_arg
            ( "Ill-formed evar map: cycle detected for evar "
            ^ Pp.string_of_ppcmds @@ Evar.print oev )
        else Evar.Set.union deps' s)
      deps deps
  in
  let rec aux deps =
    let deps' = one_step deps in
    if Evar.Set.equal deps deps' then deps else aux deps'
  in
  aux (Evar.Set.singleton oev)

let move_after ((id, ev, deps) as obl) l =
  let rec aux restdeps = function
    | ((id', _, _) as obl') :: tl ->
      let restdeps' = Evar.Set.remove id' restdeps in
      if Evar.Set.is_empty restdeps' then obl' :: obl :: tl
      else obl' :: aux restdeps' tl
    | [] -> [obl]
  in
  aux (Evar.Set.remove id deps) l

let sort_dependencies evl =
  let rec aux l found list =
    match l with
    | ((id, ev, deps) as obl) :: tl ->
      let found' = Evar.Set.union found (Evar.Set.singleton id) in
      if Evar.Set.subset deps found' then aux tl found' (obl :: list)
      else aux (move_after obl tl) found list
    | [] -> List.rev list
  in
  aux evl Evar.Set.empty []

let retrieve_obligations env name evm fs ?deps ?status t ty =
  (* 'Serialize' the evars *)
  let nc = Environ.named_context env in
  let nc_len = Context.Named.length nc in
  let evm = Evarutil.nf_evar_map_undefined evm in
  let evl = Evd.undefined_map evm in
  let evl = match deps with
  | None -> evl
  | Some deps -> Evar.Map.filter (fun ev _ -> Evar.Set.mem ev deps) evl
  in
  let evl = Evar.Map.bindings evl in
  let evl = List.map (fun (id, ev) -> (id, ev, evar_dependencies evm id)) evl in
  let sevl = sort_dependencies evl in
  let evl = List.map (fun (id, ev, _) -> (id, ev)) sevl in
  let evn =
    let i = ref (-1) in
    List.rev_map
      (fun (id, ev) ->
        incr i;
        ( id
        , ( !i
          , Id.of_string
              (Id.to_string name ^ "_obligation_" ^ string_of_int (succ !i)) )
        , ev ))
      evl
  in
  let evts =
    (* Remove existential variables in types and build the corresponding products *)
    List.fold_right
      (fun (id, (n, nstr), ev) l ->
        let hyps = Evd.evar_filtered_context ev in
        let hyps = trunc_named_context nc_len hyps in
        let evtyp, deps, transp = etype_of_evar evm l hyps (Evd.evar_concl ev) in
        let evtyp, hyps, chop =
          match chop_product fs evtyp with
          | Some t -> (t, trunc_named_context fs hyps, fs)
          | None -> (evtyp, hyps, 0)
        in
        let loc, k = Evd.evar_source (Evd.find evm id) in
        let status =
          match k with
          | Evar_kinds.QuestionMark {Evar_kinds.qm_obligation = o} -> o
          | _ -> (
            match status with
            | Some o -> o
            | None ->
              Evar_kinds.Define (not (Program.get_proofs_transparency ())) )
        in
        let force_status, status, chop =
          match status with
          | Evar_kinds.Define true as stat ->
            if not (Int.equal chop fs) then (true, Evar_kinds.Define false, None)
            else (false, stat, Some chop)
          | s -> (false, s, None)
        in
        let info =
          { ev_name = (n, nstr)
          ; ev_hyps = hyps
          ; ev_status = (force_status, status)
          ; ev_chop = chop
          ; ev_src = (loc, k)
          ; ev_typ = evtyp
          ; ev_deps = deps
          ; ev_tac = None }
        in
        (id, info) :: l)
      evn []
  in
  let t', _, transparent =
    (* Substitute evar refs in the term by variables *)
    subst_evar_constr evm evts 0 EConstr.mkVar t
  in
  let ty, _, _ = subst_evar_constr evm evts 0 EConstr.mkVar ty in
  let evars =
    List.map
      (fun (ev, info) ->
        let { ev_name = _, name
            ; ev_status = force_status, status
            ; ev_src = src
            ; ev_typ = typ
            ; ev_deps = deps
            ; ev_tac = tac } =
          info
        in
        let force_status, status =
          match status with
          | Evar_kinds.Define true when Id.Set.mem name transparent ->
            (true, Evar_kinds.Define false)
          | _ -> (force_status, status)
        in
        (name, typ, src, (force_status, status), deps, tac))
      evts
  in
  let evnames = List.map (fun (ev, info) -> (ev, snd info.ev_name)) evts in
  let evmap f c = Util.pi1 (subst_evar_constr evm evts 0 f c) in
  (Array.of_list (List.rev evars), (evnames, evmap), t', ty)
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct