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
|
module
imports
statix/name
statix/type
statix/sort
statix/cons
statix/symbol
statix/util
signature
sorts constructors
SortCons : SymbolDef * Constructor -> SortCons
sorts constructors
: string -> Constructor
sorts constructors
SortDef : string -> SymbolDef
SymbolDefCf : SymbolDef -> SymbolDef
SymbolDefLex : SymbolDef -> SymbolDef
SymbolDefVar : SymbolDef -> SymbolDef
SymbolDef_Symbol : Symbol -> SymbolDef
sorts constructors
SortConsRef : Symbol * Constructor -> SortConsRef
rules
: scope * list(TYPE) * SortCons -> TYPE
declareSortCons(, Tsymbols, SortCons(symbolDef, Constructor(constructorName))) = Tprod :- {}
typeOfSymbolDef(s, symbolDef) == Tsort,
declareConstructor(s, Tsymbols, Tsort, constructorName) == Tprod.
: scope * SymbolDef -> TYPE
typeOfSymbolDef(s, SortDef(name)) = Tsort :- typeOfSort(s, name) == Tsort.
typeOfSymbolDef(s, SymbolDefCf(symbolDef)) = T :- typeOfSymbolDef(s, symbolDef) == T.
typeOfSymbolDef(s, SymbolDefLex(symbolDef)) = T :- typeOfSymbolDef(s, symbolDef) == T.
typeOfSymbolDef(s, SymbolDefVar(symbolDef)) = T :- typeOfSymbolDef(s, symbolDef) == T.
typeOfSymbolDef(s, SymbolDef_Symbol(symbol)) = T :- typeOfSymbol(s, symbol) == T.
: scope * SortConsRef -> TYPE
typeOfSortConsRef(, SortConsRef(symbol, Constructor(constructorName))) = Tprod :- {}
typeOfSymbol(s, symbol) == Tsort,
typeOfConstructorInSort(s, constructorName, Tsort) == Tprod.
maps typeOfSortConsRef(*, list(*)) = list(*)
|