aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/genarg.ml
blob: a3bfb405c8d5eec28b33b7db8ed8f7f87e4e72df (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
(************************************************************************)
(*  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 Pp
open Util

module ArgT =
struct
  module DYN = Dyn.Make ()
  module Map = DYN.Map
  type ('a, 'b, 'c) tag = ('a * 'b * 'c) DYN.tag
  type any = Any : ('a, 'b, 'c) tag -> any
  let eq = DYN.eq
  let repr = DYN.repr
  let create = DYN.create
  let name s = match DYN.name s with
  | None -> None
  | Some (DYN.Any t) ->
    Some (Any (Obj.magic t)) (** All created tags are made of triples *)
end

type (_, _, _) genarg_type =
| ExtraArg : ('a, 'b, 'c) ArgT.tag -> ('a, 'b, 'c) genarg_type
| ListArg : ('a, 'b, 'c) genarg_type -> ('a list, 'b list, 'c list) genarg_type
| OptArg : ('a, 'b, 'c) genarg_type -> ('a option, 'b option, 'c option) genarg_type
| PairArg : ('a1, 'b1, 'c1) genarg_type * ('a2, 'b2, 'c2) genarg_type ->
  ('a1 * 'a2, 'b1 * 'b2, 'c1 * 'c2) genarg_type

type argument_type = ArgumentType : ('a, 'b, 'c) genarg_type -> argument_type

let rec genarg_type_eq : type a1 a2 b1 b2 c1 c2.
  (a1, b1, c1) genarg_type -> (a2, b2, c2) genarg_type ->
  (a1 * b1 * c1, a2 * b2 * c2) CSig.eq option =
fun t1 t2 -> match t1, t2 with
| ExtraArg t1, ExtraArg t2 -> ArgT.eq t1 t2
| ListArg t1, ListArg t2 ->
  begin match genarg_type_eq t1 t2 with
  | None -> None
  | Some Refl -> Some Refl
  end
| OptArg t1, OptArg t2 ->
  begin match genarg_type_eq t1 t2 with
  | None -> None
  | Some Refl -> Some Refl
  end
| PairArg (t1, u1), PairArg (t2, u2) ->
  begin match genarg_type_eq t1 t2 with
  | None -> None
  | Some Refl ->
    match genarg_type_eq u1 u2 with
    | None -> None
    | Some Refl -> Some Refl
  end
| _ -> None

let rec pr_genarg_type : type a b c. (a, b, c) genarg_type -> Pp.t = function
| ListArg t -> pr_genarg_type t ++ spc () ++ str "list"
| OptArg t -> pr_genarg_type t ++ spc () ++ str "opt"
| PairArg (t1, t2) ->
    str "("++ pr_genarg_type t1 ++ spc () ++
    str "*" ++ spc () ++ pr_genarg_type t2 ++ str ")"
| ExtraArg s -> str (ArgT.repr s)

let argument_type_eq arg1 arg2 = match arg1, arg2 with
| ArgumentType t1, ArgumentType t2 ->
  match genarg_type_eq t1 t2 with
  | None -> false
  | Some Refl -> true

let pr_argument_type (ArgumentType t) = pr_genarg_type t

type 'a uniform_genarg_type = ('a, 'a, 'a) genarg_type
(** Alias for concision *)

(* Dynamics but tagged by a type expression *)

type rlevel = [ `rlevel ]
type glevel = [ `glevel ]
type tlevel = [ `tlevel ]

type (_, _) abstract_argument_type =
| Rawwit : ('a, 'b, 'c) genarg_type -> ('a, rlevel) abstract_argument_type
| Glbwit : ('a, 'b, 'c) genarg_type -> ('b, glevel) abstract_argument_type
| Topwit : ('a, 'b, 'c) genarg_type -> ('c, tlevel) abstract_argument_type

type 'l generic_argument = GenArg : ('a, 'l) abstract_argument_type * 'a -> 'l generic_argument

type raw_generic_argument = rlevel generic_argument
type glob_generic_argument = glevel generic_argument
type typed_generic_argument = tlevel generic_argument

let rawwit t = Rawwit t
let glbwit t = Glbwit t
let topwit t = Topwit t

let wit_list t = ListArg t

let wit_opt t = OptArg t

let wit_pair t1 t2 = PairArg (t1, t2)

let in_gen t o = GenArg (t, o)

let abstract_argument_type_eq :
  type a b l. (a, l) abstract_argument_type -> (b, l) abstract_argument_type -> (a, b) CSig.eq option =
  fun t1 t2 -> match t1, t2 with
  | Rawwit t1, Rawwit t2 ->
    begin match genarg_type_eq t1 t2 with
    | None -> None
    | Some Refl -> Some Refl
    end
  | Glbwit t1, Glbwit t2 ->
    begin match genarg_type_eq t1 t2 with
    | None -> None
    | Some Refl -> Some Refl
    end
  | Topwit t1, Topwit t2 ->
    begin match genarg_type_eq t1 t2 with
    | None -> None
    | Some Refl -> Some Refl
    end

let out_gen (type a) (type l) (t : (a, l) abstract_argument_type) (o : l generic_argument) : a =
  let GenArg (t', v) = o in
  match abstract_argument_type_eq t t' with
  | None -> failwith "out_gen"
  | Some Refl -> v

let has_type (GenArg (t, v)) u = match abstract_argument_type_eq t u with
| None -> false
| Some _ -> true

let unquote : type l. (_, l) abstract_argument_type -> _ = function
| Rawwit t -> ArgumentType t
| Glbwit t -> ArgumentType t
| Topwit t -> ArgumentType t

let genarg_tag (GenArg (t, _)) = unquote t

type 'a raw_abstract_argument_type = ('a,rlevel) abstract_argument_type
type 'a glob_abstract_argument_type = ('a,glevel) abstract_argument_type
type 'a typed_abstract_argument_type = ('a,tlevel) abstract_argument_type

(** Creating args *)

module type Param = sig type ('raw, 'glb, 'top) t end
module ArgMap(M : Param) =
struct
  type _ pack = Pack : ('raw, 'glb, 'top) M.t -> ('raw * 'glb * 'top) pack
  include ArgT.Map(struct type 'a t = 'a pack end)
end

let create_arg name =
  match ArgT.name name with
  | None -> ExtraArg (ArgT.create name)
  | Some _ ->
    CErrors.anomaly (str "generic argument already declared: " ++ str name ++ str ".")

let make0 = create_arg

(** Registering genarg-manipulating functions *)

module type GenObj =
sig
  type ('raw, 'glb, 'top) obj
  val name : string
  val default : ('raw, 'glb, 'top) genarg_type -> ('raw, 'glb, 'top) obj option
end

module Register (M : GenObj) =
struct
  module GenMap = ArgMap(struct type ('r, 'g, 't) t = ('r, 'g, 't) M.obj end)
  let arg0_map = ref GenMap.empty

  let register0 arg f = match arg with
  | ExtraArg s ->
    if GenMap.mem s !arg0_map then
      let msg = str M.name ++ str " function already registered: " ++ str (ArgT.repr s) ++ str "." in
      CErrors.anomaly msg
    else
      arg0_map := GenMap.add s (GenMap.Pack f) !arg0_map
  | _ -> assert false

  let get_obj0 name =
    try
      let GenMap.Pack obj = GenMap.find name !arg0_map in obj
    with Not_found ->
      match M.default (ExtraArg name) with
      | None ->
        CErrors.anomaly (str M.name ++ str " function not found: " ++ str (ArgT.repr name) ++ str ".")
      | Some obj -> obj

  (** For now, the following function is quite dummy and should only be applied
      to an extra argument type, otherwise, it will badly fail. *)
  let obj t = match t with
  | ExtraArg s -> get_obj0 s
  | _ -> assert false

end