PairExtension.xstw

module PairExtension;

extension {
  context-free syntax
    "Pair" Type -> Type {cons("TyPair")}

  desugarings
    { Pair T ~~~> (T->T->T) -> T }

  context-free syntax
    Term "." "1"          -> Term {cons("Fst")}
    Term "." "2"          -> Term {cons("Snd")}
    "(" Term "," Term ")" -> Term {cons("Pair")}

  context-free priorities
      Term Term     -> Term >
    { Term "." "1"  -> Term
      Term "." "2"  -> Term } >
      Term "+" Term -> Term

  inductive definitions
    T-Fst:
      C |- t : Pair T
      ---------------
      C |- t.1 : T
    T-Snd:
      C |- t : Pair T
      ---------------
      C |- t.2 : T
    T-Pair:
      (C |- t1 : T) (C |- t2 : T)
      ---------------------------
      C |- (t1,t2) : Pair T

  desugarings
    { (C |- t : S)
      ----------------
      C |- [ t.1 ] : T
      ~~~~~~~~~~~~~~~~>
      t (\a:T.\y:T.a)
      where y = fresh(C,a:T) }
    { C |- t : S
      ----------------
      C |- [ t.2 ] : T
      ~~~~~~~~~~~~~~~~>
      t (\a:T.\b:T.b) }
    { (C |- t1 : T) (C |- t2 : T)
      ---------------------------
      C |- [ (t1,t2) ] : S
      ~~~~~~~~~~~~~~~~~~~~~~~~~~~>
      (\y:T->T->T. (y t1 t2))
      where y = fresh(C) }
}