package rocq-runtime

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

Source file typeclasses.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
(************************************************************************)
(*         *      The Rocq Prover / The Rocq Development Team           *)
(*  v      *         Copyright INRIA, CNRS and contributors             *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(*   \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)         *)
(************************************************************************)

(*i*)
open Names
open Constr
open Vars
open Evd
open Util
open Typeclasses_errors
open Context.Rel.Declaration

(*i*)

(* Core typeclasses hints *)
type 'a hint_info_gen =
    { hint_priority : int option;
      hint_pattern : 'a option }

type hint_info = (Id.Set.t * Pattern.constr_pattern) hint_info_gen

let { Goptions.get = get_typeclasses_unique_solutions } =
  Goptions.declare_bool_option_and_ref
    ~key:["Typeclasses";"Unique";"Solutions"]
    ~value:false
    ()

type class_method = {
  meth_name : Name.t;
  meth_info : hint_info option;
  meth_const : Constant.t option;
}

(* This module defines type-classes *)
type typeclass = {
  (* Universe quantification *)
  cl_univs : UVars.AbstractContext.t;

  (* The class implementation *)
  cl_impl : GlobRef.t;

  (* Context in which the definitions are typed. Includes both typeclass parameters and superclasses. *)
  cl_context : Constr.rel_context;

  (* Context of definitions and properties on defs, will not be shared *)
  cl_props : Constr.rel_context;

  (* The method implementations as projections. *)
  cl_projs : class_method list;

  cl_strict : bool;

  cl_unique : bool;
}

type typeclasses = typeclass GlobRef.Map.t
(* Invariant: for any pair (gr, tc) in the map, gr and tc.cl_impl are equal *)

type instance = {
  is_class: GlobRef.t;
  is_info: hint_info;
  is_impl: GlobRef.t;
}

type instances = (instance GlobRef.Map.t) GlobRef.Map.t

let instance_impl is = is.is_impl

let hint_priority is = is.is_info.hint_priority

(*
 * states management
 *)

let classes : typeclasses ref = Summary.ref GlobRef.Map.empty ~name:"classes"
let instances : instances ref = Summary.ref GlobRef.Map.empty ~name:"instances"

let typeclass_univ_instance (cl, u) =
  assert (UVars.eq_sizes (UVars.AbstractContext.size cl.cl_univs) (UVars.Instance.length u));
  let subst_ctx c = Context.Rel.map (subst_instance_constr u) c in
    { cl with cl_context = subst_ctx cl.cl_context;
      cl_props = subst_ctx cl.cl_props}

let class_info c = GlobRef.Map.find_opt c !classes

let class_info_exn env sigma r =
  match class_info r with
  | Some v -> v
  | None ->
    let sigma, c = Evd.fresh_global env sigma r in
    not_a_class env sigma c

let global_class_of_constr env sigma c =
  try let gr, u = EConstr.destRef sigma c in
    GlobRef.Map.find gr !classes, u
  with DestKO | Not_found -> not_a_class env sigma c

let decompose_class_app env sigma c =
  let hd, args = EConstr.decompose_app_list sigma c in
  match EConstr.kind sigma hd with
  | Proj (p, _, c) ->
    let expp = Retyping.expand_projection env sigma p c args in
    EConstr.decompose_app_list sigma expp
  | _ -> hd, args

let dest_class_app env sigma c =
  let cl, args = decompose_class_app env sigma c in
    global_class_of_constr env sigma cl, (List.map EConstr.Unsafe.to_constr args)

let dest_class_arity env sigma c =
  let open EConstr in
  let rels, c = decompose_prod_decls sigma c in
    rels, dest_class_app (push_rel_context rels env) sigma c

let class_of_constr env sigma c =
  try Some (dest_class_arity env sigma c)
  with e when CErrors.noncritical e -> None

let is_class_constr sigma c =
  try let gr, u = EConstr.destRef sigma c in
    GlobRef.Map.mem gr !classes
  with DestKO | Not_found -> false

let rec is_class_type evd c =
  let c, _ = EConstr.decompose_app evd c in
    match EConstr.kind evd c with
    | Prod (_, _, t) -> is_class_type evd t
    | Cast (t, _, _) -> is_class_type evd t
    | Proj (p, _, c) -> GlobRef.(Map.mem (ConstRef (Projection.constant p))) !classes
    | _ -> is_class_constr evd c

let is_class_evar evd evi =
  is_class_type evd (Evd.evar_concl evi)

let rec is_maybe_class_type evd c =
  let c, _ = EConstr.decompose_app evd c in
    match EConstr.kind evd c with
    | Prod (_, _, t) -> is_maybe_class_type evd t
    | Cast (t, _, _) -> is_maybe_class_type evd t
    | Evar _ -> true
    | Proj (p, _, c) -> GlobRef.(Map.mem (ConstRef (Projection.constant p))) !classes
    | _ -> is_class_constr evd c

let () = Hook.set Evd.is_maybe_typeclass_hook (fun evd c -> is_maybe_class_type evd (EConstr.of_constr c))

let load_class cl =
  classes := GlobRef.Map.add cl.cl_impl cl !classes

(** Build the subinstances hints. *)

(*
 * interface functions
 *)

let load_instance inst =
  let insts =
    try GlobRef.Map.find inst.is_class !instances
    with Not_found -> GlobRef.Map.empty in
  let insts = GlobRef.Map.add inst.is_impl inst insts in
  instances := GlobRef.Map.add inst.is_class insts !instances

let remove_instance inst =
  let insts =
    try GlobRef.Map.find inst.is_class !instances
    with Not_found -> assert false in
  let insts = GlobRef.Map.remove inst.is_impl insts in
  instances := GlobRef.Map.add inst.is_class insts !instances


let instance_constructor (cl,u) args =
  let lenpars = List.count is_local_assum cl.cl_context in
  let open EConstr in
  let pars = fst (List.chop lenpars args) in
    match cl.cl_impl with
      | GlobRef.IndRef ind ->
        let ind = ind, u in
          (Some (applist (mkConstructUi (ind, 1), args)),
           applist (mkIndU ind, pars))
      | GlobRef.ConstRef cst ->
        let cst = cst, u in
        let term = match args with
          | [] -> None
          | _ -> Some (List.last args)
        in
          (term, applist (mkConstU cst, pars))
      | _ -> assert false

let typeclasses () = GlobRef.Map.fold (fun _ l c -> l :: c) !classes []

let cmap_elements c = GlobRef.Map.fold (fun k v acc -> v :: acc) c []

let instances_of c =
  try cmap_elements (GlobRef.Map.find c.cl_impl !instances) with Not_found -> []

let all_instances () =
  GlobRef.Map.fold (fun k v acc ->
    GlobRef.Map.fold (fun k v acc -> v :: acc) v acc)
    !instances []

let instances r =
  Option.map instances_of (class_info r)

let instances_exn env sigma r =
  match instances r with
  | Some v -> v
  | None ->
    let sigma, c = Evd.fresh_global env sigma r in
    not_a_class env sigma c

let is_class gr =
  GlobRef.Map.mem gr !classes

open Evar_kinds
type evar_filter = Evar.t -> Evar_kinds.t Lazy.t -> bool

let make_unresolvables filter evd =
  let tcs = Evd.get_typeclass_evars evd in
  Evd.set_typeclass_evars evd (Evar.Set.filter (fun x -> not (filter x)) tcs)

let all_evars _ _ = true
let all_goals _ source =
  match Lazy.force source with
  | VarInstance _ | GoalEvar -> true
  | _ -> false

let no_goals ev evi = not (all_goals ev evi)
let no_goals_or_obligations _ source =
  match Lazy.force source with
  | VarInstance _ | GoalEvar | QuestionMark _ -> false
  | _ -> true

let has_typeclasses filter evd =
  let tcs = get_typeclass_evars evd in
  let check ev = filter ev (lazy (snd (Evd.evar_source (Evd.find_undefined evd ev)))) in
  Evar.Set.exists check tcs

let get_filtered_typeclass_evars filter evd =
  let tcs = get_typeclass_evars evd in
  let check ev = filter ev (lazy (snd (Evd.evar_source (Evd.find_undefined evd ev)))) in
  Evar.Set.filter check tcs

let solve_all_instances_hook = ref (fun env evd filter unique fail -> assert false)

let solve_all_instances env evd filter unique fail =
  !solve_all_instances_hook env evd filter unique fail

let set_solve_all_instances f = solve_all_instances_hook := f

let resolve_typeclasses ?(filter=no_goals) ?(unique=get_typeclasses_unique_solutions ())
    ?(fail=true) env evd =
  if not (has_typeclasses filter evd) then evd
  else solve_all_instances env evd filter unique fail

(** In case of unsatisfiable constraints, build a nice error message *)

let error_unresolvable env evd comp =
  let exception MultipleFound in
  let fold ev accu =
    match Evd.find_undefined evd ev with
    | exception Not_found -> None
    | evi ->
      let ev_class = class_of_constr env evd (Evd.evar_concl evi) in
      if Option.is_empty ev_class then accu
      else (* focus on one instance if only one was searched for *)
      if Option.has_some accu then raise MultipleFound
      else (Some ev)
  in
  let ev = try Evar.Set.fold fold comp None with MultipleFound -> None in
  Pretype_errors.unsatisfiable_constraints env evd ev comp

(** Deprecated *)

let solve_one_instance = ref (fun env evm t -> assert false)

let resolve_one_typeclass ?unique:_ env evm t =
  !solve_one_instance env evm t

let set_solve_one_instance f = solve_one_instance := f
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