module AST where

import Numeric.Natural

import Data.Map.Strict (Map)


type Name = String

data Term
  = TSet Term            -- ^ The n-th universe (n : Level)
  | TSetw Natural        -- ^ The n-th ω-universe
  | TVar Name            -- ^ variable
  | TPi Name Term Term   -- ^ Pi: (x : A) -> B
  | TLam Name Term Term  -- ^ λ(x : A). B
  | TApp Term Term       -- ^ application

  | TLift Term           -- ^ Γ |- t : Set i  ~>  Γ |- lift t : Set (Succ i)
  | TLevel               -- ^ The Level type
  | TLevelUniv           -- ^ The LevelUniv type: the type of Level
  | TIZero               -- ^ Level zero
  | TIMax Term Term      -- ^ Maximum of two levels
  | TISucc Term          -- ^ Level + 1

  | TAnnot (OfType Term Term)  -- ^ term : type

  -- Temporary stuff until we have proper inductive types:
  | TOne                   -- ^ The unit type
  | TUnit                  -- ^ The element of the unit type
  | TSigma Name Term Term  -- ^ Sigma: (x : A) × B
  | TPair Term Term        -- ^ Dependent pair
  | TProj1 Term            -- ^ First projection of a dependent pair
  | TProj2 Term            -- ^ Second projection of a dependent pair
  deriving (Show)

data Definition = Definition Name (OfType Term Term)
  deriving (Show)

type Env = Map Name (OfType (Maybe Term) Term)

data OfType a b = a :| b
  deriving (Show)
infix 1 :|