-
Notifications
You must be signed in to change notification settings - Fork 1
/
sorts.mm1
29 lines (24 loc) · 1.27 KB
/
sorts.mm1
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
import "sorts.mm0";
import "13-fixedpoints.mm1";
do {
(def (is_function symbol input_sorts output_sort) @ foldri
0
input_sorts
'(s_exists ,output_sort y (_eq (eVar y) ,(foldli 0 input_sorts symbol (fn (i phi s) '(app ,phi (eVar ,(string->atom @ string-append "x" i)))))))
(fn (i s phi) '(s_forall ,s ,(string->atom @ string-append "x" i) ,phi)))
(def (is_partial_function symbol input_sorts output_sort) @ foldri
0
input_sorts
'(s_exists ,output_sort y (_subset ,(foldli 0 input_sorts symbol (fn (i phi s) '(app ,phi (eVar ,(string->atom @ string-append "x" i))))) (eVar y)))
(fn (i s phi) '(s_forall ,s ,(string->atom @ string-append "x" i) ,phi)))
(def (is_multi_function symbol input_sorts output_sort) @ foldri
0
input_sorts
'(_subset ,(foldli 0 input_sorts symbol (fn (i phi s) '(app ,phi (eVar ,(string->atom @ string-append "x" i))))) (dom output_sort))
(fn (i s phi) '(s_forall ,s ,(string->atom @ string-append "x" i) ,phi)))
(def (is_rel symbol input_sorts output_sort) @ foldri
0
input_sorts
'(is_sorted_pred ,(dom 'output_sort) ,(foldli 0 input_sorts symbol (fn (i phi s) '(app ,phi (eVar ,(string->atom @ string-append "x" i))))))
(fn (i s phi) '(s_forall ,s ,(string->atom @ string-append "x" i) ,phi)))
};