== Concrete syntax for the IL ==


Conventions:

  x     metavaraible for identifiers; identifiers are
          sequences of alphanumeric characters
  i     metavariable for decimal integers

  k     metavariable for kinds
  ty    metavariable for types
  t     metavariable for terms

  p     metavariable for primitives
  pf    metavariable for primitive function symbols
  pt    metavariable for primitive types

  ...   n-ary syntax abbreviation; has the
        usual meaning

  ( )   grouping symbols; can appear surrounding
          any legal kind, type, or term to override
          default precedence and/or associtaivity

  Whitespace between lexemes is not significant,
  except that at least one whitespace character must
  appear after keywords and product projection forms (#i, ##i).


Kinds:

  *                    base kind
  k => k               arrow kind (right associative)
  <<| k1, ... , kn |>> type-product kind
  !!i                  i-ary product kind

Types:

  `x                   type variable
  $`x                  top-level type definition
  \`x :: k. ty         type-level abstraction
  ty ty                type-level application (left associative)
  << ty1, ..., tyn >>  n-ary type-product (product of types)
  ##i ty               type product projection
  ty -> ty             arrow type (right associative)
  forall `x :: k. ty   universal type
  mu `x :: k. ty       recursive type
  @{| pt |}            primitive type
  <| ty1, ..., tyn |>  n-ary product type
  {| ty1, ..., tyn |}  n-ary sum type


Terms:

  ^x                   term variable
  %x                   let-bound variable
  $x                   top-level identifier
  \^x :: ty. t         term abstraction
  t t                  term application (left associative)
  /\`x :: k. t         type abstraction
  t [ ty ]             type application
  error [t] "message"  noisy bottom
  seq t t              the infamous seq
  @{ p }               primitive
  @f{ pf | t1, .. tn } primitive function
  < t1, ..., tn >      n-ary (unlifted) product
  #i t                 product projection
  &x~i
    {| ty1, ... tyn |}
    t                  data constructor
  roll [ty] t          recursive roll
  unroll t             recursive unroll

  case t default t of
    { i_1 : arm1;
        ...    ;
      i_n : armn; }     case

  primcase t default f of
    { i_1 : arm_1;
        ...    ;
      i_n : arm_n }     primitive case

  let
    { %x1 :: ty1 = t1;
        ...   ;
      %xn :: tyn = tn; }
   in t                recursive let