* Pure2 -- An Interpreter for Functional Pure Type Systems
*
* Copyright 2008, K.D.P.Ross <kyle@osl.iu.edu>

* Here is the syntax of Pure2.

where `<X>` denotes nonterminal `X`
  and `<X> .. <X>` denotes a sequence of one or more `<X>`'s
  and `load`, `reset`, `dump`, `START`, `STOP`, `CHECKS`, `sort`, `axiom`, `rule`, `assume`, `let`, and `in` are reserved keywords
  and `<Id>` is an identifier beginning with a capital letter (and not equal to any of the keywords)
  and `<id>` is an identifier beginning with a miniscule letter (and not equal to any of the keywords)

Nonterm   Productions                      Intuition                      Example / Clarification
--------  -------------------------------- ------------------------------ ---------------------------------------------------------------------------------------------------------------------------------------------------
cmd     ::= load <filename>                [load a file]                  `load Foo` reads definitions in file `Foo.type`
          | reset                          [reset interpreter state]
          | dump                           [show interpreter state]       (prints the sorts, axioms, rules, and abbreviations currently defined)

          | START                          [resume processing input]      (use this and `STOP` in files to determine which bits of the code are interpreted / ignored)
          | STOP                           [suspend processing input]
          | CHECKS                         [enable typechecks]            (only needed in files)

          | sort <Id> .. <Id> .            [declare sorts]                `sort A B C D.` declares sorts `A`, `B`, `C`, and `D`
          | axiom <Id> .. <Id> : <Id> .    [declare axioms]               `axiom A B C : D.` declares axioms `A : D`, `B : D`, and `C : D`
          | rule <Id> -> <Id> .            [declare rule]                 `rule A -> B.` declares rule `A -> B : B`
          | rule <Id> -> <Id> : <Id> .                                    `rule A -> B : C.` declares rule `A -> B : C`

          | assume <Id> .. <Id> : <term> . [posit constants]              `assume A B : Nat -> Nat.` posits constants `A : Nat -> Nat` and `B : Nat -> Nat`
          | <Id> = <term> .                [define abbreviation]          `id = \ x : Nat -> x.` defines a "macro" `id` whose use is precisely equivalent to `\ x : Nat -> x`

          | <term> .                       [typecheck and normalise term] `\ (x : Nat) -> F x.` typechecks and then normalises term `\ (x : Nat) -> F x`
          | <term> : <term> .              [check typing of term]         `\ (x : Nat) -> x : Nat -> Nat` checks that the furnished term has the required type then normalises the term

          | <term> ===a <term> .           [decide alpha equivalence]     `\ (x : Nat) -> x ===a \ (y : Nat) -> y.` checks terms `\ (x : Nat) -> x` and `\ (y : Nat) -> y` for alpha equivalence
          | <term> === <term> .            [decide convertibility]        `\ (x : Nat) -> F x === (\ (f : Nat -> Nat) -> f) F.` compares terms `\ (x : Nat) -> F x` and `(\ (f : Nat -> Nat) -> f) F` for beta convertibility

term    ::= <hterm>                        [application term]             (series of simple terms)
          | <sterm>                        [simple term]                  (identifier or parenthesised term)
          | <params> <term>                [dependent product]            `(a : Set) a -> List a` equivalent of Martin-Lof's `(Pi a in Set)(a -> List a)`
          | \ <params> -> <term>           [abstraction]                  `\ (a : Set)(anA : a) -> anA` (syntactic sugar for `\ (a : Set) -> \ (anA : a) -> a`)

          | <hterm> -> <term>              [arrow type]                   `Foo -> Bar` (syntactic sugar for `(g : Foo) Bar` where, in general, `g` does not occur in the range type)
          | let <id> = <term> in <term>    [let binding]                  `let x : Nat = Zro in x` (syntactic sugar for `(\ (x : Nat) -> x) Zro`)

hterm   ::= <sterm> .. <sterm>

sterm   ::= <Id>
          | <id>
          | ( <term> )

params  ::= <binders> .. <binders>         [parameter-group list]         `(a b : Set)(x y : A -> B)` (syntactic sugar for `(a : Set)(b : Set)(x : A -> B)(y : A -> B)`)

binders ::= ( <id> .. <id> : <term> )      [parameter group]