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
|
module
imports
statix/section/section
statix/name
statix/type
statix/sort_cons
statix/symbol
statix/production
statix/attribute
signature // Section
constructors
TemplateSection : list(TemplateProduction) -> Section
sorts constructors
TemplateProduction : SymbolDef * Template * Attributes -> TemplateProduction
TemplateProductionWithCons : SortCons * Template * Attributes -> TemplateProduction
sorts constructors
Template : list(TemplateLine) -> Template
TemplateSquare : list(TemplateLine) -> Template
: list(TemplatePart) -> Template
sorts constructors
: list(TemplatePart) -> TemplateLine
sorts constructors
Angled : Placeholder -> TemplatePart
Squared : Placeholder -> TemplatePart
BreakAngled : TemplatePart
BreakSquared : TemplatePart
String : string -> TemplatePart
Escape : string -> TemplatePart
Layout : string -> TemplatePart
sorts constructors
Placeholder : Symbol * PlaceholderOptions -> Placeholder
sorts PlaceholderOptions
rules
sectionOK(s, TemplateSection(templateProductions)) :- typeOfTemplateProductions(s, templateProductions) == _.
: scope * TemplateProduction -> TYPE
typeOfTemplateProduction(, TemplateProduction(, , attrs)) = :- { }
typeOfSymbolDef(s, symbolDef) == Tsort,
new sProd, sProd -P-> s,
typeOfTemplate(sProd, template) == Tsymbols,
Tprod == INJ(Tsymbols, Tsort),
injectionProductionOK(Tprod, attrs, symbolDef),
@template.type := Tprod.
typeOfTemplateProduction(, TemplateProductionWithCons(sortCons, , _)) = :- { Tsort}
declareSortCons(s, Tsymbols, sortCons) == Tprod,
new sProd, sProd -P-> s,
typeOfTemplate(sProd, template) == Tsymbols,
@template.type := Tprod.
typeOfTemplateProductions maps typeOfTemplateProduction(*, list(*)) = list(*)
: scope * Template -> list(TYPE)
typeOfTemplate(s, Template(lines)) = flattenTypes(typeOfTemplateLines(s, lines)). /* Flatten nested list */
typeOfTemplate(s, TemplateSquare(lines)) = flattenTypes(typeOfTemplateLines(s, lines)). /* Flatten nested list */
typeOfTemplate(, SingleLineTemplate([p|ps])) = appendTypes(TmaybePart, Trest) /* Append maybe-list */ :-
maybeTypeOfTemplatePart(s, p) == TmaybePart,
typeOfTemplate(s, SingleLineTemplate(ps)) == Trest.
typeOfTemplate(s, SingleLineTemplate([])) = [].
// Returns nested lists of types, as a template has multiple lines, with multiple parts.
: scope * list(TemplateLine) -> list(list(TYPE))
typeOfTemplateLines(, [l|ls]) = [Tline|Tlines] :-
typeOfTemplateLine(s, l) == Tline,
typeOfTemplateLines(s, ls) == Tlines.
typeOfTemplateLines(s, [ ]) = [].
: scope * TemplateLine -> list(TYPE)
typeOfTemplateLine(, Line([p|ps])) = appendTypes(TmaybePart, Trest) /* Append maybe-list */ :-
maybeTypeOfTemplatePart(s, p) == TmaybePart,
typeOfTemplateLine(s, Line(ps)) == Trest.
typeOfTemplateLine(s, Line([ ])) = [].
// Emulate option type: returns list of one type for sorts, and empty list for others.
: scope * TemplatePart -> list(TYPE)
maybeTypeOfTemplatePart(s, Angled(placeholder)) = [typeOfPlaceholder(s, placeholder)].
maybeTypeOfTemplatePart(s, Squared(placeholder)) = [typeOfPlaceholder(s, placeholder)].
maybeTypeOfTemplatePart(s, _) = [].
: scope * Placeholder -> TYPE
typeOfPlaceholder(s, Placeholder(symbol, _)) = typeOfSymbol(s, symbol).
signature // Options
constructors
TemplateOptions : list(TemplateOption) -> Section
sorts constructors
KeywordAttributes : SymbolDef * Attributes -> TemplateOption
rules
sectionOK(s, TemplateOptions(templateOptions)) :- templateOptionsOK(s, templateOptions).
: scope * TemplateOption
templateOptionOK(s, KeywordAttributes(symbolDef, _)) :- typeOfSymbolDef(s, symbolDef) == _.
templateOptionOK(s, _).
templateOptionsOK maps templateOptionOK(*, list(*))
|