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
|
module
imports
statix/section/grammar
statix/section/template
statix/name
statix/type
statix/sort_cons
statix/symbol
statix/production
statix/attribute
signature
constructors
Syntax : list(Production) -> Grammar
Lexical : list(Production) -> Grammar
Contextfree : list(Production) -> Grammar
Variables : list(Production) -> Grammar
LexVariables : list(Production) -> Grammar
VariablesProductive : list(SdfProduction) -> Grammar
LexVariablesProductive : list(SdfProduction) -> Grammar
Kernel : list(SdfProduction) -> Grammar
LexicalSyntax : list(SdfProduction) -> Grammar
ContextFreeSyntax : list(GeneralProduction) -> Grammar
sorts constructors // Kernel-style productions
Prod : list(Symbol) * Symbol * Attributes -> Production
sorts constructors // General productions (explicated injection)
GeneralProduction_SdfProduction : SdfProduction -> GeneralProduction
GeneralProduction_TemplateProduction : TemplateProduction -> GeneralProduction
sorts constructors // SDF2-style productions
SdfProduction : SymbolDef * RHS * Attributes -> SdfProduction
SdfProductionWithCons : SortCons * RHS * Attributes -> SdfProduction
sorts constructors
: list(Symbol) -> RHS
rules
grammarOK(s, Syntax(productions)) :- productionsOK(s, productions).
grammarOK(s, Lexical(productions)) :- productionsOK(s, productions).
grammarOK(s, Contextfree(productions)) :- productionsOK(s, productions).
grammarOK(s, Variables(productions)) :- productionsOK(s, productions).
grammarOK(s, LexVariables(productions)) :- productionsOK(s, productions).
grammarOK(s, VariablesProductive(sdfProductions)) :- typeOfSdfProductions(s, sdfProductions) == _.
grammarOK(s, LexVariablesProductive(sdfProductions)) :- typeOfSdfProductions(s, sdfProductions) == _.
grammarOK(s, Kernel(sdfProductions)) :- typeOfSdfProductions(s, sdfProductions) == _.
grammarOK(s, LexicalSyntax(sdfProductions)) :- typeOfSdfProductions(s, sdfProductions) == _.
grammarOK(s, ContextFreeSyntax(generalProductions)) :- generalProductionsOK(s, generalProductions).
: scope * Production
productionOK(s, Prod(symbols, symbol, _)) :- {}
new sProd, sProd -P-> s,
typesOfSymbols(sProd, symbols) == _,
typeOfSymbol(sProd, symbol) == _.
maps productionOK(*, list(*))
: scope * GeneralProduction
generalProductionOK(s, GeneralProduction_SdfProduction(sdfProduction)) :-
typeOfSdfProduction(s, sdfProduction) == _.
generalProductionOK(s, GeneralProduction_TemplateProduction(templateProduction)) :-
typeOfTemplateProduction(s, templateProduction) == _.
generalProductionsOK maps generalProductionOK(*, list(*))
: scope * SdfProduction -> TYPE
typeOfSdfProduction(, SdfProduction(, rhs@Rhs(symbols), attrs)) = :- { }
typeOfSymbolDef(s, symbolDef) == Tsort,
new sProd, sProd -P-> s,
typesOfSymbols(sProd, symbols) == Tsymbols,
Tprod == INJ(Tsymbols, Tsort),
injectionProductionOK(Tprod, attrs, symbolDef),
@rhs.type := Tprod.
typeOfSdfProduction(, SdfProductionWithCons(sortCons, rhs@Rhs(symbols), _)) = :- { Tsort}
declareSortCons(s, Tsymbols, sortCons) == Tprod,
new sProd, sProd -P-> s,
typesOfSymbols(sProd, symbols) == Tsymbols,
@rhs.type := Tprod.
maps typeOfSdfProduction(*, list(*)) = list(*)
|