-
Notifications
You must be signed in to change notification settings - Fork 0
/
answer.ml
168 lines (156 loc) · 7.44 KB
/
answer.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
open Ast
open Ast_utils
type reason =
| TYPES_EQ of Typ.t * Typ.t
| TYPES_SUB of Typ.t * Typ.t
| TYPES_MISSING_FIELD of Label.t * Typ.t
| KINDS_EQ of Kind.t * Kind.t
| KINDS_SUB of Kind.t * Kind.t
| KINDS_MISSING_FIELD of Label.t * Kind.t
| WF_TYPE of Typ.t * Kind.t
| E_TYP_VAR_PURE of Typ.Var.free Location.located
| TERM_VAR_DISAGREE_TYP of
Typ.t * Typ.t * Term.Var.free
| TYP_VAR_DISAGREE_KIND of
Kind.t Location.located * Kind.t Location.located * Typ.Var.free
| TYP_VAR_DISAGREE_EE of
Mode.mode Location.located * Mode.mode Location.located * Typ.Var.free
| TYP_VAR_DISAGREE_UE of
Mode.mode Location.located * Mode.mode Location.located * Typ.Var.free
| TYP_VAR_DISAGREE_EEQ of
Mode.mode Location.located * Mode.mode Location.located * Typ.Var.free
| TYP_VAR_DISAGREE_EQE of
Mode.mode Location.located * Mode.mode Location.located * Typ.Var.free
| TYP_VAR_DISAGREE_UEQ of
Mode.mode Location.located * Mode.mode Location.located * Typ.Var.free
| TYP_VAR_DISAGREE_EQU of
Mode.mode Location.located * Mode.mode Location.located * Typ.Var.free
| TYP_VAR_DISAGREE_EQEQ of
Mode.mode Location.located * Mode.mode Location.located * Typ.Var.free
type t = Yes | No of reason list
let ( &*& ) r1 r2 = match r1 with
| Yes -> r2 ()
| No _ -> r1
let from_bool b = if b then Yes else No []
let to_bool = function Yes -> true | No _ -> false
let rec error_msg = function
| [] -> assert false
| [ KINDS_EQ (k1, k2)] ->
Printf.sprintf "%s\nis not a kind that is equivalent to\n%s\n%!"
(PPrint.Kind.string k1) (PPrint.Kind.string k2)
| [ KINDS_SUB (k1, k2)] ->
Printf.sprintf "%s\nis not a subkind of\n%s\n%!"
(PPrint.Kind.string k1) (PPrint.Kind.string k2)
| [ KINDS_MISSING_FIELD (lab, k)] ->
Printf.sprintf "The field\n %s :: %s\nis required but not provided.\n%!"
lab (PPrint.Kind.string k)
| [ TYPES_EQ (t1, t2)] ->
Printf.sprintf "%s\nis not a type that is equivalent to\n%s\n%!"
(PPrint.Typ.string t1) (PPrint.Typ.string t2)
| [ TYPES_SUB (t1, t2)] ->
Printf.sprintf "%s\nis not a subtype of\n%s\n%!"
(PPrint.Typ.string t1) (PPrint.Typ.string t2)
| [ TYPES_MISSING_FIELD (lab, t)] ->
Printf.sprintf "The field\n %s : %s\nis required but not provided.\n%!"
lab (PPrint.Typ.string t)
| [ WF_TYPE (t, k)] ->
Printf.sprintf "%s\n cannot be given the kind\n%s\n%!"
(PPrint.Typ.string t) (PPrint.Kind.string k)
| [ E_TYP_VAR_PURE a] ->
Printf.sprintf "The existential type variable %s is not closed nor restricted.\nIt was used in %s.\n%!"
(Typ.Var.to_string a.Location.content) (Location.location_msg a)
| [ TERM_VAR_DISAGREE_TYP (t1, t2, x) ] ->
Printf.sprintf "The term variable %s is assigned two different types while zipping environments.\nIn %s, it has type\n%s\nwhereas in %s, it has type\n%s\n%!"
(Term.Var.to_string x)
(Location.location_msg t1)
(Ast_utils.PPrint.Typ.string t1)
(Location.location_msg t2)
(Ast_utils.PPrint.Typ.string t2)
| [ TYP_VAR_DISAGREE_KIND (k1, k2, x) ] ->
Printf.sprintf "The type variable %s is assigned two different kinds while zipping environments.\nIn %s, it has kind\n%s\nwhereas in %s, it has kind\n%s\n%!"
(Typ.Var.to_string x)
(Location.location_msg k1)
(Ast_utils.PPrint.Kind.string k1.Location.content)
(Location.location_msg k2)
(Ast_utils.PPrint.Kind.string k2.Location.content)
| [ TYP_VAR_DISAGREE_EE (loc1, loc2, x) ] ->
Printf.sprintf "The type variable %s is used twice to create existential types in %s, and in %s.\n%!"
(Typ.Var.to_string x)
(Location.location_msg loc1)
(Location.location_msg loc2)
| [ TYP_VAR_DISAGREE_UE (loc1, loc2, x) ] ->
Printf.sprintf "The existential type variable %s is used before its witness has been defined. It is introduced in %s, then used, and defined later in %s.\n%!"
(Typ.Var.to_string x)
(Location.location_msg loc1)
(Location.location_msg loc2)
| [ TYP_VAR_DISAGREE_EQEQ
(mode1, mode2, x) ] ->
begin
match (mode1.Location.content, mode2.Location.content) with
| (Mode.EQ t1, Mode.EQ t2) ->
Printf.sprintf "The type variable %s is assigned two different equations while zipping environments.\nIn %s, it is said to be equal to the type\n%s\nwhereas in %s, it is said to be equal to the type\n%s\n%!"
(Typ.Var.to_string x)
(Location.location_msg mode1)
(Ast_utils.PPrint.Typ.string t1)
(Location.location_msg mode2)
(Ast_utils.PPrint.Typ.string t2)
| ((Mode.U | Mode.E | Mode.EQ _), _) -> assert false
end
| [ TYP_VAR_DISAGREE_EEQ (loc1, loc2, x) ] ->
Printf.sprintf "The existential type variable %s is used to create an existential type in %s, whereas it holds an equation in %s.\n%!"
(Typ.Var.to_string x)
(Location.location_msg loc1)
(Location.location_msg loc2)
| [ TYP_VAR_DISAGREE_EQE (loc1, loc2, x) ] ->
Printf.sprintf "The existential type variable %s holds an equation in %s, whereas it is used to create an existential type in %s.\n%!"
(Typ.Var.to_string x)
(Location.location_msg loc1)
(Location.location_msg loc2)
| [ TYP_VAR_DISAGREE_UEQ (loc1, loc2, x) ] ->
Printf.sprintf "The type variable %s does not hold an equation in %s, whereas it holds an equation in %s.\n%!"
(Typ.Var.to_string x)
(Location.location_msg loc1)
(Location.location_msg loc2)
| [ TYP_VAR_DISAGREE_EQU (loc1, loc2, x) ] ->
Printf.sprintf "The type variable %s holds an equation in %s, whereas it does not hold an equation in %s.\n%!"
(Typ.Var.to_string x)
(Location.location_msg loc1)
(Location.location_msg loc2)
| (KINDS_EQ (k1, k2)) :: l ->
Printf.sprintf "%s\nis not a kind that is equivalent to\n%s\nbecause\n%a"
(PPrint.Kind.string k1) (PPrint.Kind.string k2)
(fun _ -> error_msg) l
| (KINDS_SUB (k1, k2)) :: l ->
Printf.sprintf "%s\nis not a subkind of\n%s\nbecause\n%a"
(PPrint.Kind.string k1) (PPrint.Kind.string k2)
(fun _ -> error_msg) l
| (TYPES_EQ (t1, t2)) :: l ->
Printf.sprintf "%s\nis not a type that is equivalent to\n%s\nbecause\n%a"
(PPrint.Typ.string t1) (PPrint.Typ.string t2)
(fun _ -> error_msg) l
| (TYPES_SUB (t1, t2)) :: l ->
Printf.sprintf "%s\nis not a subtype of\n%s\nbecause\n%a"
(PPrint.Typ.string t1) (PPrint.Typ.string t2)
(fun _ -> error_msg) l
| (WF_TYPE (t, k)) :: l ->
Printf.sprintf "%s\n cannot be given the kind\n%s\nbecause\n%a"
(PPrint.Typ.string t) (PPrint.Kind.string k)
(fun _ -> error_msg) l
| (E_TYP_VAR_PURE _ | TERM_VAR_DISAGREE_TYP _ |
TYP_VAR_DISAGREE_KIND _ | TYP_VAR_DISAGREE_EQU _ |
TYP_VAR_DISAGREE_UEQ _ | TYP_VAR_DISAGREE_EQE _ |
TYP_VAR_DISAGREE_EEQ _ | TYP_VAR_DISAGREE_EQEQ _ |
TYP_VAR_DISAGREE_UE _ | TYP_VAR_DISAGREE_EE _ |
TYPES_MISSING_FIELD _ | KINDS_MISSING_FIELD _) :: _ ->
assert false
module WithValue = struct
type 'a t = Yes of 'a | No of reason list
let ( &*& ) (r1: 'a t) r2 = match r1 with
| Yes _ -> r2 ()
| No _ -> r1
let to_bool : 'a t -> bool = function Yes _ -> true | No _ -> false
let map (f: 'a -> 'b) : 'a t -> 'b t = function
| Yes x -> Yes (f x)
| No r -> No r
let error_msg = error_msg
end