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
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
|
module
imports
static-semantics/actions/functions
static-semantics/entities/annotations
static-semantics/types/built-ins
static-semantics/ui/template-calls
static-semantics/webdsl-actions
static-semantics/webdsl-types
static-semantics/webdsl-ui
static-semantics/webdsl
rules // var decls in templates and pages
templateElementOk(s, s_decl, _, TEVarDecl(varDecl)) :- templateVarDeclOk(s, s_decl, varDecl).
templateElementOk(s, s_decl, _, RequestScopeTemplate(varDecl)) :- templateVarDeclOk(s, s_decl, varDecl).
templateElementOk(s, s_decl, _, LocalScopeTemplate(varDecl)) :- templateVarDeclOk(s, s_decl, varDecl).
: scope * scope * VarDecl
templateVarDeclOk(s, s_decl, TemplateVarDecl(, )) :- { }
t == typeOfSort(s, sort),
inequalType(t, UNTYPED()) | error $[Unknown type [sort]] @sort,
declareVar(s_decl, x, t),
@x.type := t.
templateVarDeclOk(, s_decl, TemplateVarDeclInit(, , )) :- { }
t == typeOfSort(s, sort),
expType == typeOfExp(s, exp),
typeCompatible(expType, t) | error $[Expression [exp] is not of type [sort], got type [expType]] @exp,
declareVar(s_decl, x, t),
@x.type := t.
templateVarDeclOk(s, s_decl, TemplateVarDeclInitInferred(, )) :- { }
t == typeOfExp(s, exp),
inequalType(t, UNTYPED()) | error $[Unable to infer type of [exp]] @exp,
declareVar(s_decl, x, t),
@x.type := t.
rules // action definitions
: scope * scope * string * list(FormalArg) * list(Statement) * BOOL
templateActionOk(, s_pha, a, , stmts, declare) :- { }
new s_fun, s_fun -P-> s, // TO-DO: possibly create different label for edges out of actions, abusing P label here
argTypes == typesOfArgs(s, args),
declareParameters(s_fun, zipArgTypes(args, argTypes)),
new s_fun_body, s_fun_body -P-> s_fun,
optionallyDeclareAction(s_pha, a, args, argTypes, declare),
stmtsOk(s_fun_body, stmts, PAGE(_, _)).
: scope * string * list(FormalArg) * list(TYPE) * BOOL
optionallyDeclareAction(_, _, _, _, FALSE()).
optionallyDeclareAction(s, a, args, ts, TRUE()) :- declareAction(s, a, FUNCTION_ORIGIN(args), ts).
defOk(_, Action2Definition(Action(_, a, _, _))) :- false | error $[Actions are only allowed in pages and templates] @a.
rules // action calls
templateElementOk(s, _, s_pha, Action2TemplateElement(Action(_, a, FormalArgs(args), Block(stmts)))) :-
templateActionOk(s, s_pha, a, args, stmts, TRUE()).
: scope * ActionCallOrInlineOrExp
actionCallOrInlineOrExpOk(s, ActionCallOrInline(a)) :- actionCallOrInlineOk(s, a).
actionCallOrInlineOrExpOk(, ActionCallOrInlineExp(PropertySubmitExp(e))) :-
typeCompatible(typeOfExp(s, e), string(s)) | error $[Expression must be compatible with type String].
: scope * ActionCallOrInline
actionCallOrInlineOk(, ActionCall(ThisCall(, ))) :- { }
argTypes == typesOfExps(s, args),
resolveAction(s, a) == [(_, (a', ACTION(_, ts))) | _] | error $[Action [a] not defined] @a,
typesCompatible(argTypes, ts) == TRUE() | error $[Given argument types not compatible with action definition. Got [argTypes] but expected [ts]] @args,
@a.ref := a'.
actionCallOrInlineOk(, InlineAction(Block(stmts))) :-
templateActionOk(s, s, "", [], stmts, FALSE()).
rules // action blocks in templates
templateElementOk(s, _, _, Init(Block(stmts))) :-
stmtsOk(s, stmts, PAGE(_, _)).
templateElementOk(s, _, _, DataBindAction(Block(stmts))) :-
stmtsOk(s, stmts, UNTYPED()).
templateElementOk(s, _, _, RenderAction(Block(stmts))) :-
stmtsOk(s, stmts, UNTYPED()).
templateElementOk(s, _, _, AllPhasesAction(Block(stmts))) :-
stmtsOk(s, stmts, UNTYPED()).
templateElementOk(s, _, _, ValidateAction(Block(stmts))) :-
stmtsOk(s, stmts, UNTYPED()).
rules // statements
stmtOk(s, _, r@Return(_), PAGE(_, _)) :- false | error $[Expected page call in return statement].
stmtOk(s, _, r@Return(ThisCall2Exp(ThisCall(p, exps))), PAGE(_, _)) :-
pageCallOk_internal(s, p, exps).
stmtOk(_, _, GoTo(pc), _) :- try { false } | warning $[This statement is not yet implemented].
rules // expressions
// pass new scope as placeholder and action scope because passing `s`
// would introduce a CloseLabel exception in the concurrent solver.
// this causes any actions/placeholders references and declarations to fail
// but this is not a big deal since there's no use case for working with
// actions/placeholders in rendertemplate(...) and validatetemplate(...) calls
typeOfExp(s, RenderTemplateFunctionCall(tc)) = string(s) :-
templateCallOk(s, new, tc).
typeOfExp(s, ValidateTemplateFunctionCall(tc)) = string(s) :-
templateCallOk(s, new, tc).
rules // template var arg exp
typeOfExp(s, e@TemplateVarArgExp(expVarArgs)) = LIST() :-
t == typeOfExpVarArgList(s, expVarArgs),
@e.type := t.
: scope * list(ExpVarArg) -> TYPE
typeOfExpVarArgList(s, []) = UNTYPED() :- false | error $[Cannot infer the type of an empty list of ExpVarArgs].
typeOfExpVarArgList(, [hd | tl]) = :-
t == typeOfExpVarArg(s, hd),
expVarArgsCompatible(s, tl, t).
: scope * list(ExpVarArg) * TYPE
expVarArgsCompatible(_, [], _).
expVarArgsCompatible(, [ | tl], ) :- { }
T2 == typeOfExpVarArg(s, hd),
typeCompatible(T2, T1) | error $[Type of [hd] must be compatible [T1], [T2] given]@hd,
expVarArgsCompatible(s, tl, T1).
: scope * ExpVarArg -> TYPE
typeOfExpVarArg(s, ExpVarArg(expsOrTemplateArgs)) = TEMPLATEVARARG(ts, new) :-
ts == typesOfExpOrTemplateArgs(s, expsOrTemplateArgs).
typeOfExpVarArg(, ExpVarArgFor(, srt, , OptFilterSome(f), expVarArgs)) = t :- { }
typeOfSort == typeOfSort(s, srt),
typeOfExp == typeOfExp(s, exp),
or(
equalTypeB(LIST(typeOfSort), typeOfExp),
equalTypeB(SET(typeOfSort), typeOfExp)
) | error $[Must be a list or set of type [typeOfSort], [typeOfExp] given] @exp,
new s_for, s_for -P-> s,
forLoopFilterOk(s_for, f),
declareVar(s_for, x, typeOfSort),
declareAnnotation(s_for, x, DERIVED()), // abuse derived annotation to declare immutability of x
t == typeOfExpVarArgList(s_for, expVarArgs),
@x.type := typeOfSort.
typeOfExpVarArg(, ExpVarArgForInferred(, exp, OptFilterSome(f), expVarArgs)) = t :- { }
typeOfExp == typeOfExp(s, exp),
typeOfSort == stripGenericType(typeOfExp),
new s_for, s_for -P-> s,
forLoopFilterOk(s_for, f),
declareVar(s_for, x, typeOfSort),
declareAnnotation(s_for, x, DERIVED()), // abuse derived annotation to declare immutability of x
t == typeOfExpVarArgList(s_for, expVarArgs),
@x.type := typeOfSort.
typeOfExpVarArg(, ExpVarArgForAll(, srt, OptFilterSome(f), expVarArgs)) = t :- { }
typeOfSort == typeOfSort(s, srt),
new s_for, s_for -P-> s,
forLoopFilterOk(s_for, f),
declareVar(s_for, x, typeOfSort),
declareAnnotation(s_for, x, DERIVED()), // abuse derived annotation to declare immutability of x
t == typeOfExpVarArgList(s_for, expVarArgs),
@x.type := typeOfSort.
typeOfExpVarArg(, ExpVarArgForCount(, , , expVarArgs)) = t :- { t1 t2 }
int == int(s),
typeCompatible(typeOfExp(s, e1), int) | error $[Expression must be compatible with type Int] @e1,
typeCompatible(typeOfExp(s, e2), int) | error $[Expression must be compatible with type Int] @e2,
new s_for, s_for -P-> s,
declareVar(s_for, x, int),
declareAnnotation(s_for, x, DERIVED()), // abuse derived annotation to declare immutability of x
t == typeOfExpVarArgList(s_for, expVarArgs),
@x.type := int.
rules // exp or template arg
typesOfExpOrTemplateArgs maps typeOfExpOrTemplateArg(*, list(*)) = list(*)
: scope * ExpOrTemplateArg -> TYPE
typeOfExpOrTemplateArg(s, ExpVarArgExp(exp)) = t :-
t == typeOfExp(s, exp).
typeOfExpOrTemplateArg(s, ExpVarArgElements(elems)) = TEMPLATEELEMENTS() :- { }
new s_eval, s_eval -P-> s,
templateElementsOk(s_eval, new, elems).
|