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
|
module
imports
statix/name
statix/type
statix/util
signature
sorts constructors
CONTEXTFREE : SORT_KIND
LEXICAL : SORT_KIND
VAR : SORT_KIND
relations
: occurrence -> SORT_KIND
rules
: scope * string * SORT_KIND -> TYPE
declareSort(, , kind) = :-
Tsort == SORT(Sort{name}),
s -> Sort{name} with typeOfDecl Tsort and kindOfSort kind,
Sort{name} in s |-> [(_, (_))] | error $[Sort [name] is already defined],
@name.type := Tsort.
: scope * string -> TYPE
typeOfSort(s, ) = :- {}
typeOfDecl of Sort{name} in s |-> paths,
resolveTypeOfSorts(name, paths, NON_EMPTY()) == Tsort,
@name.type := Tsort.
: string * list((path * (occurrence * TYPE))) * EMPTINESS -> TYPE
resolveTypeOfSorts(, [(_, (Sort{name'}, Tsort))|paths], _) = Tsort :-
@name.ref += name',
resolveTypeOfSorts(name, paths, MAYBE_EMPTY()) == Tsort.
resolveTypeOfSorts(, [], NON_EMPTY()) = _ :- false | error $[Sort [name] is not defined]@name.
resolveTypeOfSorts(name, [], MAYBE_EMPTY()) = _.
kindOfSort : scope * string -> SORT_KIND
kindOfSort(s, ) = :- {}
kindOfSort of Sort{name} in s |-> paths,
resolveKindOfSorts(name, paths, NON_EMPTY()) == Tsort,
@name.type := Tsort.
: string * list((path * (occurrence * SORT_KIND))) * EMPTINESS -> SORT_KIND
resolveKindOfSorts(, [(_, (Sort{name'}, Tsort))|paths], _) = Tsort :-
@name.ref += name',
resolveKindOfSorts(name, paths, MAYBE_EMPTY()) == Tsort.
resolveKindOfSorts(, [], NON_EMPTY()) = _ :- false | error $[Sort [name] is not defined]@name.
resolveKindOfSorts(name, [], MAYBE_EMPTY()) = _.
|