You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
84 lines
1.3 KiB
84 lines
1.3 KiB
{-# 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
|