quox/lib/Quox/Definition.idr

118 lines
2.9 KiB
Idris
Raw Normal View History

2022-08-22 04:17:08 -04:00
module Quox.Definition
import public Quox.No
2022-08-22 04:17:08 -04:00
import public Quox.Syntax
2023-08-28 13:59:36 -04:00
import Quox.Displace
2022-08-22 04:17:08 -04:00
import public Data.SortedMap
2023-05-01 21:06:25 -04:00
import public Quox.Loc
2023-10-15 10:12:43 -04:00
import Quox.Pretty
2023-03-31 13:23:30 -04:00
import Control.Eff
2023-10-15 10:23:38 -04:00
import Data.Singleton
2023-01-08 14:44:25 -05:00
import Decidable.Decidable
2022-08-22 04:17:08 -04:00
public export
2023-04-01 13:16:43 -04:00
data DefBody =
Concrete (Term 0 0)
| Postulate
namespace DefBody
public export
2023-04-01 13:16:43 -04:00
(.term0) : DefBody -> Maybe (Term 0 0)
(Concrete t).term0 = Just t
(Postulate).term0 = Nothing
2022-08-22 04:17:08 -04:00
public export
2023-04-01 13:16:43 -04:00
record Definition where
constructor MkDef
2023-04-01 13:16:43 -04:00
qty : GQty
type0 : Term 0 0
body0 : DefBody
2023-05-01 21:06:25 -04:00
loc_ : Loc
2022-08-22 04:17:08 -04:00
public export %inline
2023-05-01 21:06:25 -04:00
mkPostulate : GQty -> (type0 : Term 0 0) -> Loc -> Definition
mkPostulate qty type0 loc_ = MkDef {qty, type0, body0 = Postulate, loc_}
2022-08-22 04:17:08 -04:00
2023-03-13 14:33:09 -04:00
public export %inline
2023-05-01 21:06:25 -04:00
mkDef : GQty -> (type0, term0 : Term 0 0) -> Loc -> Definition
mkDef qty type0 term0 loc_ = MkDef {qty, type0, body0 = Concrete term0, loc_}
export Located Definition where def.loc = def.loc_
export Relocatable Definition where setLoc loc = {loc_ := loc}
2022-08-22 04:17:08 -04:00
parameters {d, n : Nat}
public export %inline
2023-04-01 13:16:43 -04:00
(.type) : Definition -> Term d n
g.type = g.type0 // shift0 d // shift0 n
2023-01-20 19:41:21 -05:00
2023-08-28 13:59:36 -04:00
public export %inline
(.typeAt) : Definition -> Universe -> Term d n
g.typeAt u = displace u g.type
public export %inline
2023-04-01 13:16:43 -04:00
(.term) : Definition -> Maybe (Term d n)
g.term = g.body0.term0 <&> \t => t // shift0 d // shift0 n
public export %inline
2023-08-28 13:59:36 -04:00
(.termAt) : Definition -> Universe -> Maybe (Term d n)
g.termAt u = displace u <$> g.term
public export %inline
toElim : Definition -> Universe -> Maybe $ Elim d n
toElim def u = pure $ Ann !(def.termAt u) (def.typeAt u) def.loc
2023-10-15 10:23:38 -04:00
public export
(.typeWith) : Definition -> Singleton d -> Singleton n -> Term d n
g.typeWith (Val d) (Val n) = g.type
public export
(.typeWithAt) : Definition -> Singleton d -> Singleton n -> Universe -> Term d n
g.typeWithAt d n u = displace u $ g.typeWith d n
public export
(.termWith) : Definition -> Singleton d -> Singleton n -> Maybe (Term d n)
g.termWith (Val d) (Val n) = g.term
2022-08-22 04:17:08 -04:00
public export %inline
2023-04-01 13:16:43 -04:00
isZero : Definition -> Bool
isZero g = g.qty == GZero
2023-01-08 14:44:25 -05:00
2023-04-17 17:58:24 -04:00
public export
data DefEnvTag = DEFS
2023-04-17 17:58:24 -04:00
2023-01-08 14:44:25 -05:00
public export
2023-04-01 13:16:43 -04:00
Definitions : Type
Definitions = SortedMap Name Definition
2023-01-08 14:44:25 -05:00
2023-01-20 19:41:30 -05:00
public export
2023-05-01 21:06:25 -04:00
DefsReader : Type -> Type
2023-04-17 17:58:24 -04:00
DefsReader = ReaderL DEFS Definitions
2023-05-01 21:06:25 -04:00
public export
DefsState : Type -> Type
DefsState = StateL DEFS Definitions
public export %inline
2023-08-28 13:59:36 -04:00
lookupElim : {d, n : Nat} -> Name -> Universe -> Definitions -> Maybe (Elim d n)
lookupElim x u defs = toElim !(lookup x defs) u
2023-10-15 10:12:43 -04:00
2023-10-15 10:23:38 -04:00
public export %inline
lookupElim0 : Name -> Universe -> Definitions -> Maybe (Elim 0 0)
lookupElim0 = lookupElim
2023-10-15 10:12:43 -04:00
export
prettyDef : {opts : LayoutOpts} -> Name -> Definition -> Eff Pretty (Doc opts)
prettyDef name (MkDef qty type _ _) = withPrec Outer $ do
qty <- prettyQty qty.qty
dot <- dotD
name <- prettyFree name
colon <- colonD
type <- prettyTerm [<] [<] type
2023-11-03 12:47:01 -04:00
hangDSingle (hsep [hcat [qty, dot, name], colon]) type