|
|
- {-# 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
|