-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathphys.psoa
243 lines (206 loc) · 12.7 KB
/
phys.psoa
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
Document
(
Prefix(: <http://psoa.ruleml.org/lib/phys#>)
Prefix(xsb: <http://xsb.sourceforge.net/manual1/manual1.pdf#>)
Prefix(pred: <http://www.w3.org/2007/rif-builtin-predicate#>)
Prefix(func: <http://www.w3.org/2007/rif-builtin-function#>)
Group
(
% Wellformedness-checking (Yes/error-yielding) predicates
Forall ?x (
:tryInteger(?x) :-
? = External(func:numeric-integer-divide(?x 1)) % Workaround for raising an exception for non-integers
)
Forall ?year ?month ?day (
:tryDate(:date(?year ?month ?day)) :- And(:tryYear(?year) :tryMonth(?month) :tryDay(?day))
)
Forall ?hour ?minute ?second (
:tryTime(:time(?hour ?minute ?second)) :- And(:tryHour(?hour) :tryMinute(?minute) :trySecond(?second))
)
Forall ?year ?month ?day ?hour ?minute ?second (
:tryDatetime(:datetime(?year ?month ?day ?hour ?minute ?second)) :- And(:tryDate(:date(?year ?month ?day)) :tryTime(:time(?hour ?minute ?second)))
)
Forall ?year (
:tryYear(?year) :- :tryInteger(?year)
)
Forall ?month (
:tryMonth(?month) :- :tryInteger(?month)
)
Forall ?day (
:tryDay(?day) :- :tryInteger(?day)
)
Forall ?hour (
:tryHour(?hour) :- :tryInteger(?hour)
)
Forall ?minute (
:tryMinute(?minute) :- :tryInteger(?minute)
)
Forall ?second (
:trySecond(?second) :- :tryInteger(?second)
)
% Date/Time-yielding predicates
Forall ?year ?month ?day ?hour ?minute ?second (
:currentDatetime(:datetime(?year ?month ?day ?hour ?minute ?second)) :-
External(xsb:local_datime(xsb:datime(?year ?month ?day ?hour ?minute ?second)))
)
Forall ?year ?month ?day ?hour ?minute ?second (
:currentDatetimeUTC(:datetime(?year ?month ?day ?hour ?minute ?second)) :-
External(xsb:datime(xsb:datime(?year ?month ?day ?hour ?minute ?second)))
)
Forall ?year ?month ?day ?hour ?minute ?second (
:currentDate(:date(?year ?month ?day)) :-
:currentDatetime(:datetime(?year ?month ?day ?hour ?minute ?second))
)
Forall ?year ?month ?day ?hour ?minute ?second (
:currentDateUTC(:date(?year ?month ?day)) :-
:currentDatetimeUTC(:datetime(?year ?month ?day ?hour ?minute ?second))
)
Forall ?year ?month ?day ?hour ?minute ?second (
:currentTime(:time(?hour ?minute ?second)) :-
:currentDatetime(:datetime(?year ?month ?day ?hour ?minute ?second))
)
Forall ?year ?month ?day ?hour ?minute ?second (
:currentTimeUTC(:time(?hour ?minute ?second)) :-
:currentDatetimeUTC(:datetime(?year ?month ?day ?hour ?minute ?second))
)
% Date-comparison predicates
Forall ?year1 ?month1 ?day1 ?year2 ?month2 ?day2 (
:lessThanDate(:date(?year1 ?month1 ?day1) :date(?year2 ?month2 ?day2)) :-
And(:tryDate(:date(?year1 ?month1 ?day1))
:tryDate(:date(?year2 ?month2 ?day2))
Or(External(pred:numeric-less-than(?year1 ?year2))
And(External(pred:numeric-equal(?year1 ?year2))
Or(External(pred:numeric-less-than(?month1 ?month2))
And(External(pred:numeric-equal(?month1 ?month2))
External(pred:numeric-less-than(?day1 ?day2)))))))
)
Forall ?year1 ?month1 ?day1 ?year2 ?month2 ?day2 (
:lessEqDate(:date(?year1 ?month1 ?day1) :date(?year2 ?month2 ?day2)) :-
And(:tryDate(:date(?year1 ?month1 ?day1))
:tryDate(:date(?year2 ?month2 ?day2))
Or(External(pred:numeric-less-than(?year1 ?year2)) % numeric-less-than, without -or-equal, since, for -equal, ...
And(External(pred:numeric-equal(?year1 ?year2))
Or(External(pred:numeric-less-than(?month1 ?month2)) % ... ?month1/?day1 could be numeric-greater-than ?month2/?day2
And(External(pred:numeric-equal(?month1 ?month2))
External(pred:numeric-less-than-or-equal(?day1 ?day2)))))))
)
Forall ?year1 ?month1 ?day1 ?year2 ?month2 ?day2 (
:greaterThanDate(:date(?year1 ?month1 ?day1) :date(?year2 ?month2 ?day2)) :-
And(:tryDate(:date(?year1 ?month1 ?day1))
:tryDate(:date(?year2 ?month2 ?day2))
Or(External(pred:numeric-greater-than(?year1 ?year2))
And(External(pred:numeric-equal(?year1 ?year2))
Or(External(pred:numeric-greater-than(?month1 ?month2))
And(External(pred:numeric-equal(?month1 ?month2))
External(pred:numeric-greater-than(?day1 ?day2)))))))
)
Forall ?year1 ?month1 ?day1 ?year2 ?month2 ?day2 (
:greaterEqDate(:date(?year1 ?month1 ?day1) :date(?year2 ?month2 ?day2)) :-
And(:tryDate(:date(?year1 ?month1 ?day1))
:tryDate(:date(?year2 ?month2 ?day2))
Or(External(pred:numeric-greater-than(?year1 ?year2)) % numeric-greater-than, without -or-equal, since, for -equal, ...
And(External(pred:numeric-equal(?year1 ?year2))
Or(External(pred:numeric-greater-than(?month1 ?month2)) % ... ?month1/?day1 could be numeric-less-than ?month2/?day2
And(External(pred:numeric-equal(?month1 ?month2))
External(pred:numeric-greater-than-or-equal(?day1 ?day2)))))))
)
Forall ?year1 ?month1 ?day1 ?year2 ?month2 ?day2 (
:eqDate(:date(?year1 ?month1 ?day1) :date(?year2 ?month2 ?day2)) :-
And(:tryDate(:date(?year1 ?month1 ?day1))
:tryDate(:date(?year2 ?month2 ?day2))
External(pred:numeric-equal(?year1 ?year2))
External(pred:numeric-equal(?month1 ?month2))
External(pred:numeric-equal(?day1 ?day2)))
)
% Time-comparison predicates
Forall ?hour1 ?minute1 ?second1 ?hour2 ?minute2 ?second2 (
:lessThanTime(:time(?hour1 ?minute1 ?second1) :time(?hour2 ?minute2 ?second2)) :-
And(:tryTime(:time(?hour1 ?minute1 ?second1))
:tryTime(:time(?hour2 ?minute2 ?second2))
Or(External(pred:numeric-less-than(?hour1 ?hour2))
And(External(pred:numeric-equal(?hour1 ?hour2))
Or(External(pred:numeric-less-than(?minute1 ?minute2))
And(External(pred:numeric-equal(?minute1 ?minute2))
External(pred:numeric-less-than(?second1 ?second2)))))))
)
Forall ?hour1 ?minute1 ?second1 ?hour2 ?minute2 ?second2 (
:lessEqTime(:time(?hour1 ?minute1 ?second1) :time(?hour2 ?minute2 ?second2)) :-
And(:tryTime(:time(?hour1 ?minute1 ?second1))
:tryTime(:time(?hour2 ?minute2 ?second2))
Or(External(pred:numeric-less-than(?hour1 ?hour2)) % numeric-less-than, without -or-equal, since, for -equal, ...
And(External(pred:numeric-equal(?hour1 ?hour2))
Or(External(pred:numeric-less-than(?minute1 ?minute2)) % ... ?minute1/?second1 could be numeric-greater-than ?minute2/?second2
And(External(pred:numeric-equal(?minute1 ?minute2))
External(pred:numeric-less-than-or-equal(?second1 ?second2)))))))
)
Forall ?hour1 ?minute1 ?second1 ?hour2 ?minute2 ?second2 (
:greaterThanTime(:time(?hour1 ?minute1 ?second1) :time(?hour2 ?minute2 ?second2)) :-
And(:tryTime(:time(?hour1 ?minute1 ?second1))
:tryTime(:time(?hour2 ?minute2 ?second2))
Or(External(pred:numeric-greater-than(?hour1 ?hour2))
And(External(pred:numeric-equal(?hour1 ?hour2))
Or(External(pred:numeric-greater-than(?minute1 ?minute2))
And(External(pred:numeric-equal(?minute1 ?minute2))
External(pred:numeric-greater-than(?second1 ?second2)))))))
)
Forall ?hour1 ?minute1 ?second1 ?hour2 ?minute2 ?second2 (
:greaterEqTime(:time(?hour1 ?minute1 ?second1) :time(?hour2 ?minute2 ?second2)) :-
And(:tryTime(:time(?hour1 ?minute1 ?second1))
:tryTime(:time(?hour2 ?minute2 ?second2))
Or(External(pred:numeric-greater-than(?hour1 ?hour2)) % numeric-greater-than, without -or-equal, since, for -equal, ...
And(External(pred:numeric-equal(?hour1 ?hour2))
Or(External(pred:numeric-greater-than(?minute1 ?minute2)) % ... ?minute1/?second1 could be numeric-less-than ?minute2/?second2
And(External(pred:numeric-equal(?minute1 ?minute2))
External(pred:numeric-greater-than-or-equal(?second1 ?second2)))))))
)
Forall ?hour1 ?minute1 ?second1 ?hour2 ?minute2 ?second2 (
:eqTime(:time(?hour1 ?minute1 ?second1) :time(?hour2 ?minute2 ?second2)) :-
And(:tryTime(:time(?hour1 ?minute1 ?second1))
:tryTime(:time(?hour2 ?minute2 ?second2))
External(pred:numeric-equal(?hour1 ?hour2))
External(pred:numeric-equal(?minute1 ?minute2))
External(pred:numeric-equal(?second1 ?second2)))
)
% Datetime-comparison predicates
% Top-level wellformedness checks with :tryDatetime for early detection of type/format violation
Forall ?year1 ?month1 ?day1 ?hour1 ?minute1 ?second1 ?year2 ?month2 ?day2 ?hour2 ?minute2 ?second2 (
:lessThanDatetime(:datetime(?year1 ?month1 ?day1 ?hour1 ?minute1 ?second1) :datetime(?year2 ?month2 ?day2 ?hour2 ?minute2 ?second2)) :-
And(:tryDatetime(:datetime(?year1 ?month1 ?day1 ?hour1 ?minute1 ?second1))
:tryDatetime(:datetime(?year2 ?month2 ?day2 ?hour2 ?minute2 ?second2))
Or(:lessThanDate(:date(?year1 ?month1 ?day1) :date(?year2 ?month2 ?day2))
And(:eqDate(:date(?year1 ?month1 ?day1) :date(?year2 ?month2 ?day2))
:lessThanTime(:time(?hour1 ?minute1 ?second1) :time(?hour2 ?minute2 ?second2)))))
)
Forall ?year1 ?month1 ?day1 ?hour1 ?minute1 ?second1 ?year2 ?month2 ?day2 ?hour2 ?minute2 ?second2 (
:lessEqDatetime(:datetime(?year1 ?month1 ?day1 ?hour1 ?minute1 ?second1) :datetime(?year2 ?month2 ?day2 ?hour2 ?minute2 ?second2)) :-
And(:tryDatetime(:datetime(?year1 ?month1 ?day1 ?hour1 ?minute1 ?second1))
:tryDatetime(:datetime(?year2 ?month2 ?day2 ?hour2 ?minute2 ?second2))
Or(:lessThanDate(:date(?year1 ?month1 ?day1) :date(?year2 ?month2 ?day2))
And(:eqDate(:date(?year1 ?month1 ?day1) :date(?year2 ?month2 ?day2))
:lessEqTime(:time(?hour1 ?minute1 ?second1) :time(?hour2 ?minute2 ?second2)))))
)
Forall ?year1 ?month1 ?day1 ?hour1 ?minute1 ?second1 ?year2 ?month2 ?day2 ?hour2 ?minute2 ?second2 (
:greaterThanDatetime(:datetime(?year1 ?month1 ?day1 ?hour1 ?minute1 ?second1) :datetime(?year2 ?month2 ?day2 ?hour2 ?minute2 ?second2)) :-
And(:tryDatetime(:datetime(?year1 ?month1 ?day1 ?hour1 ?minute1 ?second1))
:tryDatetime(:datetime(?year2 ?month2 ?day2 ?hour2 ?minute2 ?second2))
Or(:greaterThanDate(:date(?year1 ?month1 ?day1) :date(?year2 ?month2 ?day2))
And(:eqDate(:date(?year1 ?month1 ?day1) :date(?year2 ?month2 ?day2))
:greaterThanTime(:time(?hour1 ?minute1 ?second1) :time(?hour2 ?minute2 ?second2)))))
)
Forall ?year1 ?month1 ?day1 ?hour1 ?minute1 ?second1 ?year2 ?month2 ?day2 ?hour2 ?minute2 ?second2 (
:greaterEqDatetime(:datetime(?year1 ?month1 ?day1 ?hour1 ?minute1 ?second1) :datetime(?year2 ?month2 ?day2 ?hour2 ?minute2 ?second2)) :-
And(:tryDatetime(:datetime(?year1 ?month1 ?day1 ?hour1 ?minute1 ?second1))
:tryDatetime(:datetime(?year2 ?month2 ?day2 ?hour2 ?minute2 ?second2))
Or(:greaterThanDate(:date(?year1 ?month1 ?day1) :date(?year2 ?month2 ?day2))
And(:eqDate(:date(?year1 ?month1 ?day1) :date(?year2 ?month2 ?day2))
:greaterEqTime(:time(?hour1 ?minute1 ?second1) :time(?hour2 ?minute2 ?second2)))))
)
Forall ?year1 ?month1 ?day1 ?hour1 ?minute1 ?second1 ?year2 ?month2 ?day2 ?hour2 ?minute2 ?second2 (
:eqDatetime(:datetime(?year1 ?month1 ?day1 ?hour1 ?minute1 ?second1) :datetime(?year2 ?month2 ?day2 ?hour2 ?minute2 ?second2)) :-
And(:tryDatetime(:datetime(?year1 ?month1 ?day1 ?hour1 ?minute1 ?second1))
:tryDatetime(:datetime(?year2 ?month2 ?day2 ?hour2 ?minute2 ?second2))
:eqDate(:date(?year1 ?month1 ?day1) :date(?year2 ?month2 ?day2))
:eqTime(:time(?hour1 ?minute1 ?second1) :time(?hour2 ?minute2 ?second2)))
)
)
)