-
Notifications
You must be signed in to change notification settings - Fork 53
/
Copy pathcoq-lib-common.elpi
170 lines (146 loc) · 6.81 KB
/
coq-lib-common.elpi
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
/* coq-elpi: Helpers common to synterp and interp */
/* license: GNU Lesser General Public License Version 2.1 or later */
/* ------------------------------------------------------------------------- */
shorten std.{fatal-error, fatal-error-w-data, debug-print}.
:before "default-fatal-error"
fatal-error M :- !, stop M.
:before "default-fatal-error-w-data"
fatal-error-w-data Msg Data :- !,
term_to_string Data DataS,
M is Msg ^ ": " ^ DataS, stop M.
:before "default-debug-print"
debug-print M Data :- !, coq.debug M Data.
% HACK: elpi's stop has no argument
type stop string -> prop.
:name "stop:begin"
stop S :- coq.error S. % halt S
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
pred coq.parse-attributes i:list attribute, i:list attribute-signature, o:list prop.
% Coq attribute parser, eg [#[attribute=value] Command]
%
% Usage:
% main _ :-
% attributes A, % fetch
% coq.parse-attributes A Spec Opts, % parse/validate
% Opts => (mycode, get-option "foo" V, mycode). % use
%
% where [Opts] is a list of clauses [get-option StringName Value], where value
% can have any type and [Spec] is a list of [attribute-sigmature].
% Example of an attribute signature:
% [
% att "this" bool,
% att "that.thing" int,
% att "algebraic" (oneof ["foo" `-> foo-thing, "bar" `-> barbar]),
% ]
%
% Env variable COQ_ELPI_ATTRIBUTES can be used to pass attributes to all
% commands. These attributes names are prefixed by 'elpi.' and are of type
% string.
%
% Eg.
% COQ_ELPI_ATTRIBUTES=test=yes,str="some-string" coqc foo.v
% results in commands in foo.v to receive
% [ attribute "elpi.test" (leaf "yes") ,
% attribute "elpi.str" (leaf "some-string") | ...]
% which are automatically accepted and give rise to
% get-option "elpi.test" "yes"
% get-option "elpi.str" "some-string"
kind attribute-signature type.
type att string -> attribute-type -> attribute-signature.
type att-ignore-unknown attribute-signature.
type supported-attribute attribute-signature -> prop.
supported-attribute (att "elpi.loc" loc).
supported-attribute (att Name string) :- rex_match "^elpi\\." Name.
kind attribute-type type.
type int attribute-type.
type string attribute-type.
type bool attribute-type.
type oneof list attribute-mapping -> attribute-type.
type attmap attribute-type. % #[map(k1="v1",k2="v2")]
type attlist attribute-type. % #[set(b1,b2,b3)]
type attlabel attribute-type. % #[label( a(..), b, .. )] if #[label(a, b), a(..), ..]
type loc attribute-type.
kind attribute-mapping type.
type (`->) string -> any -> attribute-mapping.
pred coq.valid-str-attribute i:string, i:string, o:option any, o:diagnostic.
coq.valid-str-attribute Name Value V Diag :-
if (supported-attribute (att Name Type))
(coq.typecheck-attribute Name Type Value LPV Diag, V = some LPV)
(if (supported-attribute att-ignore-unknown) (V = none, Diag = ok)
(Diag = error {calc ( "Attribute " ^ Name ^ " is not supported")})).
pred coq.valid-loc-attribute i:string, i:loc, o:diagnostic.
coq.valid-loc-attribute Name Loc Diag :-
if (supported-attribute (att Name loc))
(if (primitive? Loc "loc") (Diag = ok) (Diag = error {calc ( "Attribute " ^ Name ^ " takes a loc, got " ^ {std.any->string Loc} ) } ))
(if (supported-attribute att-ignore-unknown) (Diag = ok)
(Diag = error {calc ( "Attribute " ^ Name ^ " is not supported")})).
:index (_ 1 1)
pred coq.typecheck-attribute i:string, o:attribute-type, i:string, o:any, o:diagnostic.
coq.typecheck-attribute _ int Value V ok :- V is string_to_int Value, !.
coq.typecheck-attribute N int Value _ (error Msg) :-
Msg is "Attribute " ^ N ^ " takes an integer, got: " ^ Value.
coq.typecheck-attribute _ string V V ok.
coq.typecheck-attribute _ bool "true" tt ok.
coq.typecheck-attribute _ bool "tt" tt ok.
coq.typecheck-attribute _ bool "True" tt ok.
coq.typecheck-attribute _ bool "on" tt ok.
coq.typecheck-attribute _ bool "yes" tt ok.
coq.typecheck-attribute _ bool "" tt ok.
coq.typecheck-attribute _ bool "false" ff ok.
coq.typecheck-attribute _ bool "False" ff ok.
coq.typecheck-attribute _ bool "off" ff ok.
coq.typecheck-attribute _ bool "ff" ff ok.
coq.typecheck-attribute _ bool "no" ff ok.
coq.typecheck-attribute N bool Value _ (error Msg) :-
Msg is "Attribute " ^ N ^ " takes an boolean, got: " ^ Value.
pred coq.is-one-of i:string, o:any, i:attribute-mapping.
coq.is-one-of K V (K `-> V).
coq.typecheck-attribute _ (oneof L) K V ok :- std.exists L (coq.is-one-of K V), !.
coq.typecheck-attribute N (oneof L) K _ (error Msg) :-
std.map L (x\r\ sigma tmp\ x = r `-> tmp) S,
std.fold S "" (s\ a\ calc (a ^ " " ^ s)) OneOf,
Msg is "Attribute " ^ N ^ " takes one of " ^ OneOf ^ ", got: " ^ K.
pred append-string i:string, i:string, o:string.
append-string "" A A :- !.
append-string A B R :- R is A ^ "." ^ B.
pred keep-only-label i:attribute, o:attribute.
keep-only-label (attribute L _) (attribute L (leaf-str "")).
coq.parse-attributes L S O :-
std.map S (x\r\ r = supported-attribute x) CS,
CS => parse-attributes.aux L "" O, !.
pred parse-attributes.aux i:list attribute, i:string, o:list prop.
parse-attributes.aux [] _ [].
parse-attributes.aux [attribute S (node L)|AS] Prefix R :-
append-string Prefix S PS, supported-attribute (att PS attlist), !,
parse-attributes.aux AS Prefix R1,
((pi x\ supported-attribute (att x bool) :- !) ==> parse-attributes.aux L "" Map),
std.append R1 [get-option PS Map] R.
parse-attributes.aux [attribute S (node L)|AS] Prefix R :-
append-string Prefix S PS, supported-attribute (att PS attmap), !,
parse-attributes.aux AS Prefix R1,
((pi x\ supported-attribute (att x string) :- !) ==> parse-attributes.aux L "" Map),
std.append R1 [get-option PS Map] R.
parse-attributes.aux [attribute S (node L)|AS] Prefix R :-
append-string Prefix S PS, supported-attribute (att PS attlabel), !,
parse-attributes.aux AS Prefix R1,
std.map L keep-only-label Ll,
((pi x\ supported-attribute (att x bool) :- !) ==> parse-attributes.aux Ll "" Map),
parse-attributes.aux L Prefix R2,
std.append R1 [get-option PS Map|R2] R.
parse-attributes.aux [attribute S (node L)|AS] Prefix R :- !,
parse-attributes.aux AS Prefix R1,
append-string Prefix S PS,
parse-attributes.aux L PS R2,
std.append R1 R2 R.
parse-attributes.aux [attribute S (leaf-str V)|AS] Prefix CLS :- !,
append-string Prefix S PS,
coq.valid-str-attribute PS V V1 Diag,
if (Diag = error Msg) (coq.error Msg) true,
if (V1 = some Val) (CLS = [get-option PS Val|R]) (CLS = R), % ignored
parse-attributes.aux AS Prefix R.
parse-attributes.aux [attribute S (leaf-loc V)|AS] Prefix CLS :- !,
append-string Prefix S PS,
coq.valid-loc-attribute PS V Diag,
if (Diag = error Msg) (coq.error Msg) true,
CLS = [get-option PS V|R],
parse-attributes.aux AS Prefix R.