@@ -9,29 +9,42 @@ DSL розглядається як frontend до формальної моде
99Ключова ідея:
1010
1111``` text
12- DSL text
13- -> Lexer
14- -> Parser
15- -> CST
16- -> Surface AST
17- -> Normalize / Desugar
18- -> Compile
19- -> Program IR
20- -> Interpreter over Kernel
21- -> Judgments / checks
12+ OCaml model:
13+ Kernel
14+ Typed AST (ручне конструювання)
15+ Tests
16+
17+ Elixir compiler:
18+ DSL text
19+ -> Lexer
20+ -> Parser
21+ -> Surface AST
22+ -> Normalize / Desugar
23+ -> Compile
24+ -> Erlang AST
25+ -> BEAM
26+ -> Execution over Kernel
27+ -> Judgments / checks
2228```
2329
2430---
2531
2632## Загальний підхід
2733
28- DSL не виконується напряму. Замість цього він:
34+ Важливо: формальна модель системи реалізується в OCaml без використання DSL-синтаксису.
2935
30- 1 . Парситься у синтаксичне дерево
31- 2 . Нормалізується
32- 3 . Компілюється у проміжне представлення (Program IR)
33- 4 . Інтерпретується поверх формального kernel
34- 5 . Перевіряється через систему semantic judgments
36+ Усі сценарії на цьому рівні задаються безпосередньо через типізований AST kernel-моделі.
37+
38+ Синтаксис DSL (lexer, parser) з’являється лише в Elixir-реалізації компілятора.
39+
40+ DSL не виконується напряму. Замість цього Elixir-реалізація:
41+
42+ 1 . Парсить DSL у синтаксичне дерево
43+ 2 . Нормалізує surface form
44+ 3 . Компілює сценарій у Erlang AST
45+ 4 . Компілює Erlang AST у BEAM
46+ 5 . Виконує код поверх формального kernel
47+ 6 . Перевіряє результат через semantic judgments
3548
3649Таким чином система має чітке розділення між:
3750
@@ -110,17 +123,17 @@ Parser не виконує semantic resolution.
110123
111124- resolution alias-ів
112125- роботу з контекстом сесії
113- - перетворення resource references
126+ - перетворення feed references
114127- інтерпретацію symbolic boundary (` snapshot ` , ` continue ` )
115128- перевірку базової коректності
116129
117- Результатом є ** Program IR ** — компільована програма сценарію.
130+ Результатом є Erlang AST — компільована програма сценарію у форматі, що напряму компілюється у BEAM .
118131
119132---
120133
121- ## Program IR
134+ ## Erlang AST
122135
123- Program IR — це проміжне представлення сценарію як програми з ефектами.
136+ Erlang AST — це представлення сценарію як програми з ефектами у форматі, що напряму відповідає BEAM execution model .
124137
125138Основна ідея:
126139
@@ -129,6 +142,10 @@ Program IR — це проміжне представлення сценарію
129142- ` expect ` — assertion
130143- сценарій — композиція таких операцій
131144
145+ У OCaml-моделі ці операції задаються безпосередньо через типізований AST, без використання текстового синтаксису DSL.
146+
147+ В Elixir-компіляторі вони мають бути скомпільовані не у власний IR, а в Erlang AST як цільове представлення BEAM.
148+
132149### Приклад структури
133150
134151``` ocaml
@@ -152,7 +169,7 @@ type _ program =
152169 | Op : 'a op -> 'a program
153170```
154171
155- Program IR є строго типізованим і визначає порядок виконання ефектів .
172+ Ця структура описує типізований AST моделі; у цільовій Elixir-реалізації сценарій має компілюватися в Erlang AST .
156173
157174---
158175
@@ -175,9 +192,9 @@ Kernel не містить DSL-специфічного синтаксису.
175192
176193---
177194
178- ## Interpreter
195+ ## Execution over Kernel
179196
180- Interpreter виконує Program IR поверх kernel.
197+ Execution layer виконує скомпільований Erlang AST поверх kernel.
181198
182199Він:
183200
@@ -192,7 +209,7 @@ Interpreter виконує Program IR поверх kernel.
192209run : program -> state -> result
193210```
194211
195- Interpreter є єдиною точкою, де відбувається execution semantics.
212+ Execution over Kernel є точкою, де Erlang AST зв’язується з формальною моделлю та runtime semantics.
196213
197214---
198215
@@ -226,12 +243,12 @@ Interpreter є єдиною точкою, де відбувається executio
226243
227244- env.ml
228245- compile.ml
229- - program .ml
246+ - erlang_ast .ml
230247
231248### Semantic core
232249
233250- kernel.ml
234- - interpreter .ml
251+ - execution .ml
235252- judgment.ml
236253- typecheck.ml
237254- world_check.ml
@@ -246,10 +263,11 @@ Interpreter є єдиною точкою, де відбувається executio
246263
247264Архітектура розділяє:
248265
249- - синтаксис (DSL)
250- - програму сценарію (Program IR)
266+ - синтаксис DSL (тільки в Elixir)
267+ - типізований AST моделі (в OCaml)
268+ - цільове Erlang AST (для BEAM)
251269- семантику (Kernel)
252- - виконання (Interpreter )
270+ - виконання (Execution over Kernel )
253271- перевірку (Judgments)
254272
255273Це дозволяє:
@@ -262,10 +280,26 @@ Interpreter є єдиною точкою, де відбувається executio
262280Ключова формула:
263281
264282``` text
265- DSL = frontend
266- Program IR = compiled scenario program
283+ OCaml model = kernel + typed AST + tests
284+ Elixir compiler = syntax + compile to Erlang AST
285+ Erlang AST = compiled scenario program
267286Kernel = canonical semantic model
268- Interpreter = semantics
287+ Execution over Kernel = semantics
269288Judgments = verification layer
270289```
271290
291+
292+
293+ Розділення відповідальностей:
294+
295+ - OCaml модель:
296+ - Kernel
297+ - Типізований AST
298+ - Формальні перевірки
299+ - Без DSL-синтаксису
300+
301+ - Elixir компілятор:
302+ - DSL синтаксис
303+ - Парсер і токенайзер
304+ - Компіляція у Erlang AST
305+ - Генерація BEAM коду
0 commit comments