Istari

Term syntax

Istari employs two types for terms: Term.term is the internal representation of terms, and ETerm.eterm is the external representation. We usually refer to both of them as just terms, except when the context requires us to distinguish them.

The main difference between internal and external terms is that internal terms represent variables using de Bruijn indices, while external terms use explicit names. (Istari’s de Bruijn indices count from zero.) External terms are converted to internal ones by supplying a data structure (called a directory) that maps names onto indices.

The term grammar

The default grammar for terms is as follows. Capitalized words are nonterminals; lower case words are keywords. (Exception: U and Kind are keywords.)

Forms are listed in increasing order of precedence. Grouped forms have the same precedence. A subterm at the same level of precedence is given in brackets. For example, [Term] + Term indicates that addition is left associative, while Term :: [Term] indicates that cons is right associative.

Term ::=
  fn Bindingsn . [Term]                                          (lambda)
  forall Bindings . [Term]                                       (dependent product)  
  exists Bindings . [Term]                                       (strong dependent sum)
  iforall Bindings . [Term]                                      (impredicative universal)
  iexists Bindings . [Term]                                      (impredicative existential)
  intersect Bindings . [Term]                                    (intersection type)
  foralltp OIdents . [Term]                                      (impredicative polymorphism)
  rec Ident . [Term]                                             (recursive type)
  mu Ident . [Term]                                              (inductive type)
  wtype ( Ident : [Term] ) . [Term]                              (W type)
  iset ( Ident : [Term] ) . [Term]                               (intensional set type)
  quotient ( Ident Ident : [Term] ) . [Term]                     (quotient type)
  Term -> [Term]                                                 (ordinary arrow)
  Term -t> [Term]                                                (tarrow kind)
  Term -k> [Term]                                                (karrow kind)
  Term -g> [Term]                                                (guard)
  let Ident = Term in [Term]                                     (let)
  let next Ident = Term in [Term]                                (scoped future elim)
  case Term of | inl OIdent . [Term] | inr OIdent . [Term]       (sum elim)
  Term : [Term]                                                  (typing)
  Term : type                                                    (type formation)
  fnind ... inductive function ...                               (inductive function)

  if [Term] then [Term] else [Term]                              (if-then-else)

  Term <-> Term                                                  (if-and-only-if)

  Term % [Term]                                                  (sum type)

  Term & [Term]                                                  (product type)

  Term = Term : Term                                             (equality)
  Term = Term : type                                             (type equality)
  Term <: Term                                                   (subtyping)
  Term <:> Term                                                  (extensional type equivalence)
  Term != Term : Term                                            (inequality)
  Term <= Term                                                   (natural number inequality)
  Term < Term                                                    (natural number inequality)
  Term <l= Term                                                  (level inequality)
  Term <z= Term                                                  (integer inequality)
  Term <z Term                                                   (integer inequality)

  Term :: [Term]                                                 (cons)

  [Term] + Term                                                  (natural number plus)
  [Term] - Term                                                  (natural number minus)
  [Term] +z Term                                                 (integer plus)
  [Term] -z Term                                                 (integer minus)

  [Term] * Term                                                  (natural number times)
  [Term] *z Term                                                 (integer times)

  [Term] Term                                                    (application)
  [Term] #1                                                      (first projection)
  [Term] #2                                                      (second projection)
  [Term] #prev                                                   (unscoped future elim)
  [Term] ## Number                                               (#2 ... #2 #1)
  pi1 Term                                                       (first projection)
  pi2 Term                                                       (second projection)
  prev Term                                                      (unscoped future elim)
  next Term                                                      (future intro)
  inl Term                                                       (sum intro)
  inr Term                                                       (sum intro)
  ~z Term                                                        (integer negation)
  U Level                                                        (universe)
  Kind Level                                                     (kind)
  [Term] :> Term                                                 (type annotation)
  [Term] ap Term                                                 (visibilized application)
  [Term] _# Number                                               (application to multiple evars)
  [Term] __# Number                                              (application to multiple holes)

  ( Term )
  ()                                                             (unit)
  ( Term , ... , Term )                                          (tuple, length at least 2)
  { Ident : Term | Term }                                        (set type)
  { Term }                                                       (squashed type)
  Longident                                                      (identifier)
  Number                                                         (natural number literal)
  _                                                              (evar)
  __                                                             (hole)
  \ ... antiquoted internal term ... \
  ` Longident
  l` LTerm                                                       (literal term)
  level` Level                                                   (level expression)
  z` Number                                                      (integer literal)

OIdent ::=
  Ident
  _                                                              (anonymous argument)

OIdents ::=
  OIdent ... OIdent                                              (length can be zero)

Binding ::=
  OIdent                                                         (unannotated binding)
  (OIdents : Term)                                               (binding with type supplied)

Bindings ::=       
  Binding ... Binding                                            (length at least 0)

Bindingsn ::=       
  Binding ... Binding                                            (length at least 1)

Level ::=
  Number + [Level]                                               (level plus)

  ( Level )
  Number                                                         (level literal)
  [ Level ... Level ]                                            (level max, length at least 1)
  Ident                                                          (identifier)
  \ ... antiquoted internal term ... \

Notes:

Literal terms

The LTerm (“literal term”) grammar represents internal terms directly. It uses de Bruijn indices rather than names and offers very few conveniences. It also provides a notation for explicit substitution.

LTerm ::=
  fn . [LTerm]                                                   (lambda)

  LTerm = LTerm : LTerm                                          (equality)
  LTerm = LTerm : type                                           (type equality)

  [LTerm] LTerm                                                  (application)
  [LTerm] #1                                                     (first projection)
  [LTerm] #2                                                     (second projection)
  [LTerm] #prev                                                  (unscoped future elim)
  next LTerm                                                     (future intro)

  [LTerm] [ Sub ]                                                (substitution)

  ( LTerm )
  ()                                                             (unit)
  ( LTerm, LTerm )                                               (pair)
  U                                                              (universe w/o argument)
  Number                                                         (de Bruijn index)
  \ ... antiquoted internal term ... \
  ` Longident
  z` Number                                                      (integer literal)

Sub ::=
  [Sub] o Sub                                                    (composition)

  LTerm . [Sub]                                                  (substitution cons)
  Number . [Sub]                                                 (special case of cons)
  ^ Number                                                       (shift)
  id                                                             (identity, same as ^0)
  ( Sub )

Notes:

Parsing functions

Most of the nonterminals above can be parsed by various pervasive functions: parseIdent, parseIdents, parseLongident, parseOIdent, parseOIdents, parseBinding, parseBindings, parseLTerm, parseSub.

These functions are all actually the identity function, but IML is instructed to parse their argument using the indicated nonterminal.

Opacity

Constants have one of four levels of opacity: soft, firm, hard, or opaque:

A constant’s opacity can be altered using the function setOpacity. Since opacities can be altered, an opaque constant is not entirely abstract. To make a constant abstract, one may delete a constant’s definition, thereby rendering it permanently opaque, using the function abstract.

(* abbreviated *)
signature CONSTANT =
   sig
      ...

      datatype opacity = SOFT | FIRM | HARD | OPAQUE

      (* returns the constant's definition if the constant is not OPAQUE *)
      val definition : constant -> term option

      val opacity : constant -> opacity
      val setOpacity : constant -> opacity -> unit

      (* sets opacity to OPAQUE and deletes the definition (cannot be reversed) *)
      val abstract : constant -> unit
   end

structure Constant : CONSTANT