content: 
  module Syntax where
  
  import Common
  
  --------------------------------------------------------------------------------
  
  type Ty = Tm
  
  -- | A `Pruning` represents a spine of variables, which contains a subsequence
  --   of all variables in scope. A `Just` represents application to a var, a
  --   `Nothing` skips over a var.
  type Pruning = [Maybe Icit]
  
  -- | A reversed pruning. Used for pruning Pi domains, where we have to iterate
  --   inside-out.
  newtype RevPruning = RevPruning Pruning
  
  revPruning :: Pruning -> RevPruning
  revPruning = RevPruning . reverse
  
  -- | Information about the local binders, used for efficiently creating types for
  --   fresh metas.
  data Locals
    = LHere
    | LDefine Locals Name ~Ty ~Tm
    | LBind Locals Name ~Ty
    deriving Show
  
  -- | Convert type in context to a closed iterated Pi type.  Note: we need `Tm`
  --   and `Ty` in `Locals` in order to make this operation efficient. With this, we
  --   can simply move things over from `Locals` without having to rename or quote
  --   anything.
  closeTy :: Locals -> Ty -> Ty
  closeTy mcl b = case mcl of
    LHere             -> b
    LBind mcl x a     -> closeTy mcl (Pi x Expl a b)
    LDefine mcl x a t -> closeTy mcl (Let x a t b)
  
  -- | Convert a term in context to a closed term by wrapping it in lambdas and
  --   let-definitions. The type of the result is given by `closeTy`.
  closeTm :: Locals -> Tm -> Tm
  closeTm mcl t = case mcl of
    LHere             -> t
    LBind mcl x a     -> closeTm mcl (Lam x Expl t)
    LDefine mcl x a u -> closeTm mcl (Let x a u t)
  
  data Tm
    = Var Ix
    | Lam Name Icit Tm
    | App Tm Tm Icit
    | AppPruning Tm Pruning
    | U
    | Pi Name Icit Ty Ty
    | Let Name Ty Tm Tm
    | Meta MetaVar
    | PostponedCheck CheckVar
    | Open [Name] Tm Tm
  
    | Box
    | Quote Tm
    | Splice Tm (Maybe String) -- displayed location of the splice
  
    | Eff
    | Return
    | Bind Name Tm Tm
    | Seq Tm Tm
  
    | Ref
    | New
    | Write
    | Read
    | Erased String
  
    | Nat
    | NatLit Integer
    | Suc
    | NatElim
  
    | RecTy [(Name, Tm)]
    | Rec [(Name, Tm)]
    | Proj Tm Name
  
    | ReadNat
    | PrintNat
    | Log String
    deriving Show
  
  pattern LamI x t = Lam x Impl t
  pattern LamE x t = Lam x Expl t
  pattern AppE t u = App t u Expl
  pattern AppI t u = App t u Impl
  pattern NatElim' p s z n = NatElim `AppI` p `AppE` s `AppE` z `AppE` n
  pattern Eff' t = Eff `AppE` t
  pattern Return' a t = Return `AppI` a `AppE` t
  pattern Ref' a = Ref `AppE` a
  pattern New' a t = New `AppI` a `AppE` t
  pattern Write' a t u = Write `AppI` a `AppE` t `AppE` u
  pattern Read' a t = Read `AppI` a `AppE` t
  pattern Suc' t = Suc `AppE` t
  pattern Box' t = Box `AppE` t
  pattern PrintNat' t = PrintNat `AppE` t
  
  
  -- | Unfold `AppPruning` to an iterated application to vars. This applies a term to all de Bruijn indices
  --   which are `Just` in the mask.
  appPruning :: Tm -> Pruning -> Tm
  appPruning t pr = go 0 pr where
    go x []              = t
    go x (pr :> Just i)  = App (go (x + 1) pr) (Var x) i
    go x (pr :> Nothing) = go (x + 1) pr
  