Presyntax.hs

module Presyntax where

import Common

data Tm
  = Var Name                                  -- x
  | Lam Name (Either Name Icit) (Maybe Tm) Tm -- \x. t | \{x}. t | \{x = y}. t |
                                              -- \(x : A). t | \{x : A}. t
  | App Tm Tm (Either Name Icit)              -- t u  | t {u} | t {x = u}
  | U                                         -- U
  | Pi Name Icit Tm Tm                        -- (x : A) -> B | {x : A} -> B
  | Let Name (Maybe Tm) Tm Tm                 -- let x : A = t; u
  | SrcPos SourcePos Tm                       -- source position for error reporting

  | Box                                       -- □
  | Quote Tm                                  -- <t>
  | Splice Tm SourcePos                       -- ~t

  | Eff                                       -- Eff
  | Return                                    -- return
  | Bind Name Tm Tm                           -- do x <- t; u
  | Seq Tm Tm                                 -- do t; u

  | Ref                                       -- Ref t
  | New                                       -- new t
  | Write                                     -- write t u
  | Read                                      -- read t

  | Nat                                       -- ℕ | Nat
  | Zero                                      -- zero
  | Suc                                       -- suc
  | NatLit Integer                            -- numeral
  | NatElim                                   -- NatElim | ℕElim

  | RecTy [(Name, Tm)]                        -- Σ(a : A, b : B ...) <|> Rec(a : A, b : B ...)
  | Rec [(Maybe Name, Tm)]                    -- (a = t, b = u, v, ...)
  | Proj Tm Name                              -- t.field

  | Open Tm Tm                                -- open t; u

  | ReadNat                                   -- readℕ | readNat
  | PrintNat                                  -- printℕ | printℕ
  | Log String                                -- log "t"

  | Hole                                      -- _
  deriving Show

pattern AppE t u = App t u (Right Expl)
pattern AppI t u = App t u (Right Impl)

-- | Get rid of source positions, for better debug printing.
stripPos :: Tm -> Tm
stripPos = \case
  Var x         -> Var x
  Lam x i ma t  -> Lam x i (stripPos <$> ma) (stripPos t)
  App t u i     -> App (stripPos t) (stripPos u) i
  U             -> U
  Pi x i a b    -> Pi x i (stripPos a) (stripPos b)
  Let x a t u   -> Let x (stripPos <$> a) (stripPos t) (stripPos u)
  SrcPos _ t    -> stripPos t
  Hole          -> Hole
  Box           -> Box
  Quote t       -> Quote (stripPos t)
  Splice t p    -> Splice (stripPos t) p
  Eff           -> Eff
  Return        -> Return
  Bind x t u    -> Bind x (stripPos t) (stripPos u)
  Seq t u       -> Seq (stripPos t) (stripPos u)
  Ref           -> Ref
  New           -> New
  Write         -> Write
  Read          -> Read
  Nat           -> Nat
  Zero          -> Zero
  Suc           -> Suc
  NatLit n      -> NatLit n
  NatElim       -> NatElim
  RecTy fs      -> RecTy ((stripPos <$>) <$> fs)
  Rec fs        -> Rec   ((stripPos <$>) <$> fs)
  Proj t x      -> Proj (stripPos t) x
  Open t u      -> Open (stripPos t) (stripPos u)
  ReadNat       -> ReadNat
  PrintNat      -> PrintNat
  Log s         -> Log s


--------------------------------------------------------------------------------