forked from ocaml/ocaml
/
dyntypes.mli
142 lines (105 loc) · 3.4 KB
/
dyntypes.mli
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
(***********************************************************************)
(* *)
(* Objective Caml *)
(* *)
(* Xavier Leroy, projet Cristal, INRIA Rocquencourt *)
(* *)
(* Copyright 1996 Institut National de Recherche en Informatique et *)
(* en Automatique. All rights reserved. This file is distributed *)
(* under the terms of the GNU Library General Public License, with *)
(* the special exception on linking described in file ../LICENSE. *)
(* *)
(***********************************************************************)
(* $Id$ *)
(** Dynamic representation of types. *)
type 'a ttype
(** {2 Structure of types.} *)
type stype =
| DT_tuple of stype list
| DT_node of node * stype list
| DT_var of int
and record_representation =
| Record_regular
| Record_float
and mutable_flag =
| Mutable
| Immutable
and node = {
node_id: string;
node_definition: node_definition;
}
and node_definition =
| DT_record of record_definition
| DT_variant of variant_definition
| DT_abstract
| DT_builtin
and record_definition = {
record_representation: record_representation;
record_fields: (string * mutable_flag * stype) list;
}
and variant_definition = {
variant_constructors: (string * stype list) list;
}
val stype_of_ttype: 'a ttype -> stype
(** {2 Equality.} *)
module TypEq : sig
type ('a, 'b) t
(** A value of type [('a, 'b) t] is a witness that the two types ['a] and ['b] are equal. *)
val refl: ('a, 'a) t
val trans: ('a, 'b) t -> ('b, 'c) t -> ('a, 'c) t
val sym: ('a, 'b) t -> ('b, 'a) t
val app: ('a, 'b) t -> 'a -> 'b
end
val stype_equality: stype -> stype -> bool
val equal: 'a ttype -> 'b ttype -> ('a, 'b) TypEq.t option
(** {2 Dynamic values.} *)
module type DYN = sig
type t
val x: t
val t: t ttype
end
type dyn = (module DYN)
val dyn: 'a ttype -> 'a -> dyn
val tuple: dyn list -> dyn
(** {2 Inspection of values.} *)
type head =
| DV_tuple of dyn list
| DV_record of (string * dyn) list
| DV_constructor of string * dyn list
exception AbstractValue of node
val inspect: dyn -> head
(** {2 Abstract types.} *)
module type TYPE0 = sig
type t
val node: node
val ttype: t ttype
val inspect: dyn -> t option
end
module type TYPE1 = sig
type 'a t
module type T = sig
type a
type b
val b: b ttype
val eq: (a, b t) TypEq.t
end
val node: node
val ttype: 'a ttype -> 'a t ttype
val decompose: 'a t ttype -> 'a ttype
val check: 'a ttype -> (module T with type a = 'a) option
module type V = sig
type b
val b: b ttype
val x: b t
end
val inspect: dyn -> (module V) option
end
module Abstract0(X : sig val name: string type t end) : TYPE0 with type t = X.t
module Abstract1(X : sig val name: string type 'a t end) : TYPE1 with type 'a t = 'a X.t
module DList: TYPE1 with type 'a t = 'a list
module DOption: TYPE1 with type 'a t = 'a option
module DArray: TYPE1 with type 'a t = 'a array
module DInt: TYPE0 with type t = int
module DString: TYPE0 with type t = string
module DFloat: TYPE0 with type t = float
module DBool: TYPE0 with type t = bool