module Presyntax where

import Data.Text (Text)
import Syntax (Plicity)

data RawExpr
  = Rvar  Text
  | Rapp  Plicity RawExpr RawExpr
  | Rlam  Plicity Text    RawExpr
  | Rpi   Plicity Text    RawExpr RawExpr
  | Rlet  Text    RawExpr RawExpr RawExpr
  | Rtype
  | Rhole

  | Rtop | Runit
  | Rbot
  | Req RawExpr RawExpr
  | Rrefl
  | Rcoe
  | Rcong
  | Rsym

  | Rsigma Text RawExpr RawExpr
  | Rpair RawExpr RawExpr
  | Rproj1 RawExpr
  | Rproj2 RawExpr

  | RSrcPos (Int, Int) (Int, Int) RawExpr
  deriving (Eq, Show, Ord)