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 p.env (p sect)) or (sym in init_scope).

;

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