{-# LANGUAGE LambdaCase #-}
module Presyntax where

data Exp
  = Var String
  | App Exp Exp
  | Lam String  Exp
  | Let String Exp Exp Exp

  | Sigma String Exp Exp
  | Pair Exp Exp
  | Proj1 Exp
  | Proj2 Exp

  | Pi  String Exp Exp
  | Type
  | Typeω

  | I
  | I0 | I1
  | IAnd Exp Exp
  | IOr  Exp Exp
  | INot Exp

  | Path

  | Cut Exp Exp
  | Span (Int, Int) (Int, Int) Exp

  -- Formulas, partial elements, and the type of formulas
  | Partial [(Formula, Exp)]
  | PartialT
  | PartialP

  -- Compositions
  | Comp

  -- Cubical subtypes
  | SubT

  -- Glueing
  | GlueTy
  | Glue
  | Unglue

  -- Bools
  | Bool
  | Tt
  | Ff
  | If
  deriving (Eq, Show, Ord)

data Formula
  = Is0 String
  | Is1 String
  | And Formula Formula
  | Or Formula Formula
  | Top | Bot
  deriving (Eq, Ord)

instance Show Formula where
  showsPrec p =
    \case
      Is1 i -> showString i
      Is0 i -> showString ('~':i)
      And x y -> showParen (p > and_prec) $
        showsPrec or_prec x
        . showString " && "
        . showsPrec or_prec y
      Or x y -> showParen (p > or_prec) $
        showsPrec or_prec x
        . showString " || "
        . showsPrec or_prec y
      Top -> showString "i1"
      Bot -> showString "i0"
    where
      and_prec = 2
      or_prec = 1


data Statement
  = Assume [(String, Exp)]
  | Declare String Exp Exp
  | Eval Exp