pantagruel

eval p: Program :: Bool
Program <= [Section]

" A section head must have at least one statement; a section body can be empty.

section head: Head, body: Body, #head > 0 => Section

Head <= [Comment, Declaration, Alias]
Body <= [Comment, Expression]
Comment, Declaration, Alias, Expression <= [String]
---

eval p <- all sect : p \ is_bound? sect

;

is_bound? sect: Section :: Bool
---

" All variables referred to in a section head must be defined by the
" end of that section head. All the variables in a section body, however,
" must be defined by the end of the *next* section body.

is_bound? sect <-                                           ...
    (all h : sect.head \ all sym : h \ is_bound? sym) ...
    and                                                     ...
    (all b : (p ((p sect) - 1)).body \ all sym : b \ is_bound? sym)

;

is_bound sym: String :: Bool
---
is_bound sym <- (sym in env p (p sect)) or (sym in init_scope)

;

env p: Program :: [Scope]
init_scope :: Scope
Scope <= {String}