Something went wrong. Try again.
dependent-types proof-assistant
Something went wrong. Try again.
2.2 kB · 115 lines
Haskell
at main
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116
module Core.Syntax where
import Core.Infoimport Common
data LetBind = LetBind { letBindName :: Name , letBindTy :: Ty , letBindBody :: Tm }
data PiBind = PiBind { piBindName :: Name , piBindInfo :: PiDomKind , piBindDomTy :: Ty , piBindBody :: Ty }
data LamBind = LamBind { lamBindName :: Name , lamBindInfo :: PiDomKind , lamBindDomTy :: Ty , lamBindBody :: Tm }
instance Show PiBind where show (PiBind x i a b) = show (x, i, a, b)
instance Show LamBind where show (LamBind x i a t) = show (x, i, a, t)
instance Show LetBind where show (LetBind x a t) = show (x, a, t)
data Sub = SNil -- ^ Sub Γ ∙ | SExt Sub Tm -- ^ vanilla extension | SDef Sub Tm -- ^ extend codomain with a definition deriving Show
{- σ : Sub Γ Δ t : Tm Δ A ─────────────────────────────── SDef σ t : Sub Γ (Δ, x : A = t)-}
data MetaSub = MSId | MSSub Sub deriving Show
data Level = ZeroPlus Tm | OmegaPlus Integer | OmegaPlusOmega deriving Show
data Tm = Var Ix | TopDef {-# nounpack #-} DefInfo | Meta MetaVar MetaSub | Let Tm LetBind | App Tm Tm PiDomKind | Lam LamBind | LZero | LSuc Tm | LMax Tm Tm | Wk Tm | Code Level Ty | Cast Ty Ty Tm deriving Show
data Ty = TYPE Level | Pi PiBind | FinLevel | Decode Level Tm deriving Show
data Locals = LNil | LLet Locals Name Tm Ty | LBind Locals Name ~Ty deriving Show
instance Sized Locals where size = go 0 where go acc LNil = acc go acc (LLet ls _ _ _) = go (acc + 1) ls go acc (LBind ls _ _) = go (acc + 1) ls
localsToNames :: Locals -> NameslocalsToNames = \case LNil -> Nil LLet ls x _ _ -> Cons x (localsToNames ls) LBind ls x _ -> Cons x (localsToNames ls)
type LocalsArg = (?locals :: Locals)
data RevLocals = RLNil | RLLet Name Tm Ty RevLocals | RLBind Name ~Ty RevLocals deriving Show
reverseLocals :: Locals -> RevLocalsreverseLocals = go RLNil where go acc = \case LNil -> acc LLet ls x t a -> go (RLLet x t a acc) ls LBind ls x a -> go (RLBind x a acc) ls
makeFields ''PiBindmakeFields ''LetBind