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
|
module
imports
statix/section/section
statix/name
statix/type
statix/symbol
signature // Declarations
sorts constructors
Module : ModuleName * list(ImpSection) * list(Section) -> Module
sorts constructors
Unparameterized : ModuleId -> ModuleName
: ModuleId * list(Symbol) -> ModuleName
sorts // Use module identifiers as-is.
rules
: scope * Module
moduleOK(, Module(, importSections, sections)) :- {}
new sMod, sMod -P-> sGlobal,
declareModule(sGlobal, sMod, name),
moduleNameOK(sMod, name),
importSectionsOK(sMod, importSections),
sectionsOK(sMod, sections).
: scope * ModuleName
moduleNameOK(s, Parameterized(_, symbols)) :- typesOfSymbols(s, symbols) == _.
moduleNameOK(s, _).
rules
: scope * scope * ModuleName
declareModule(, sMod, name) :- {}
idOfModuleName(name) == id,
sGlobal -> Module{id} with typeOfDecl MOD(sMod),
Module{id} in sGlobal |-> [(_, (_))] | error $[Duplicate definition of module [id]]@id.
: scope * ModuleName -> TYPE
typeOfModule(s, name) = Tmod :- { }
idOfModuleName(name) == id,
typeOfDecl of Module{id} in s |-> paths,
resolveModules(id, paths, NON_EMPTY()) == Tmod.
: ModuleId * list((path * (occurrence * TYPE))) * EMPTINESS -> TYPE
resolveModules(, [(_, (Module{id'}, Tmod))|paths], _) = Tmod :-
@id.ref += id',
resolveModules(id, paths, MAYBE_EMPTY()) == Tmod.
resolveModules(, [], NON_EMPTY()) = _ :- false | error $[Module [id] is not defined]@id.
resolveModules(id, [], MAYBE_EMPTY()) = _.
: ModuleName -> ModuleId
idOfModuleName(Unparameterized(id)) = id.
idOfModuleName(Parameterized(id, _)) = id.
signature // Imports
sorts constructors
Imports : list(Import) -> ImpSection
sorts constructors
Module : ModuleName -> Import
rules
: scope * ImpSection
importSectionOK(s, Imports(imports)) :- importsOK(s, imports).
importSectionsOK maps importSectionOK(*, list(*))
: scope * Import
importOK(, Module(name)) :- {}
typeOfModule(s, name) == MOD(sMod),
s -I-> sMod.
importsOK maps importOK(*, list(*))
|