pantagruel

eval |p: Program| :: Bool
[Section] => Program
" A section head must have at least one statement; a section body can be empty.
section |head, body: Head, Body . #head > 0 | => Section
[Comment, Declaration, Alias] => Head
[Comment, Expression] => Body
[String] => Comment, Declaration, Alias, Expression

eval p <- all sect from 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 from sect.head . all sym from h . is_bound? sym) ...
    and                                                     ...
    (all b from (p (p sect) - 1).body . all sym from b . is_bound? sym)

;

is_bound |sym: String| :: Bool

is_bound sym <- sym from (env p) (p sect) or sym from init_scope

;

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