quox/lib/Quox/Definition.idr
2023-03-13 19:33:09 +01:00

107 lines
2.6 KiB
Idris

module Quox.Definition
import public Quox.No
import public Quox.Syntax
import public Data.SortedMap
import public Control.Monad.Reader
import Decidable.Decidable
public export
record AnyTerm q where
constructor T
get : forall d, n. Term q d n
public export
data DefBody q =
Concrete (AnyTerm q)
| Postulate
public export
record Definition' q (isGlobal : Pred q) where
constructor MkDef
qty : q
type : AnyTerm q
body : DefBody q
{auto 0 qtyGlobal : isGlobal qty}
public export
0 Definition : (q : Type) -> IsQty q => Type
Definition q = Definition' q IsGlobal
public export %inline
mkDef : IsQty q => (qty : q) -> (0 _ : IsGlobal qty) =>
(type, term : forall d, n. Term q d n) -> Definition q
mkDef qty type term = MkDef {qty, type = T type, body = Concrete (T term)}
public export %inline
mkPostulate : IsQty q => (qty : q) -> (0 _ : IsGlobal qty) =>
(type : forall d, n. Term q d n) -> Definition q
mkPostulate qty type = MkDef {qty, type = T type, body = Postulate}
public export %inline
mkDef0 : IsQty q => (qty : q) -> (0 _ : IsGlobal qty) =>
(type, term : Term q 0 0) -> Definition q
mkDef0 qty type term = mkDef qty (inject type) (inject term)
public export %inline
(.get0) : AnyTerm q -> Term q 0 0
t.get0 = t.get
public export %inline
(.type0) : Definition' q _ -> Term q 0 0
g.type0 = g.type.get
public export %inline
(.term) : Definition' q _ -> Maybe (AnyTerm q)
g.term = case g.body of
Concrete t => Just t
Postulate => Nothing
public export %inline
(.term0) : Definition' q _ -> Maybe (Term q 0 0)
g.term0 = map (\x => x.get) g.term
public export %inline
(.qtyP) : forall q, isGlobal. Definition' q isGlobal -> Subset q isGlobal
g.qtyP = Element g.qty g.qtyGlobal
public export %inline
toElim : Definition' q _ -> Maybe $ Elim q d n
toElim def = pure $ (!def.term).get :# def.type.get
public export
0 IsZero : IsQty q => Pred $ Definition q
IsZero g = IsZero g.qty
public export %inline
isZero : (p : IsQty q) => Dec1 $ Definition.IsZero @{p}
isZero g = isZero g.qty
public export
0 Definitions' : (q : Type) -> Pred q -> Type
Definitions' q isGlobal = SortedMap Name $ Definition' q isGlobal
public export
0 Definitions : (q : Type) -> IsQty q => Type
Definitions q = Definitions' q IsGlobal
public export
0 HasDefs' : (q : Type) -> (q -> Type) -> (Type -> Type) -> Type
HasDefs' q isGlobal = MonadReader (Definitions' q isGlobal)
public export
0 HasDefs : (q : Type) -> IsQty q => (Type -> Type) -> Type
HasDefs q = HasDefs' q IsGlobal
public export %inline
lookupElim : forall isGlobal.
Name -> Definitions' q isGlobal -> Maybe (Elim q d n)
lookupElim x defs = toElim !(lookup x defs)