pantagruel

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

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

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

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

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
Scope <= {String}