quox/lib/Quox/Definition.idr

131 lines
3.3 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
import public Data.SortedMap
2023-01-08 14:44:25 -05:00
import public Control.Monad.Reader
import Decidable.Decidable
2022-08-22 04:17:08 -04:00
public export
2023-01-08 14:44:25 -05:00
record AnyTerm q where
2022-08-22 04:17:08 -04:00
constructor T
2023-01-08 14:44:25 -05:00
get : forall d, n. Term q d n
2022-08-22 04:17:08 -04:00
public export
2023-01-20 19:41:21 -05:00
record Definition' q (isGlobal : Pred q) where
2022-08-22 04:17:08 -04:00
constructor MkDef'
2023-01-08 14:44:25 -05:00
qty : q
type : AnyTerm q
term : Maybe $ AnyTerm q
{auto 0 qtyGlobal : isGlobal qty}
public export
0 Definition : (q : Type) -> IsQty q => Type
Definition q = Definition' q IsGlobal
2022-08-22 04:17:08 -04:00
public export %inline
2023-01-08 14:44:25 -05:00
mkDef : IsQty q => (qty : q) -> (0 _ : IsGlobal qty) =>
(type, term : forall d, n. Term q d n) -> Definition q
2023-01-08 09:44:20 -05:00
mkDef qty type term = MkDef' {qty, type = T type, term = Just (T term)}
2022-08-22 04:17:08 -04:00
public export %inline
2023-01-08 14:44:25 -05:00
mkAbstract : IsQty q => (qty : q) -> (0 _ : IsGlobal qty) =>
(type : forall d, n. Term q d n) -> Definition q
2023-01-08 09:44:20 -05:00
mkAbstract qty type = MkDef' {qty, type = T type, term = Nothing}
2022-08-22 04:17:08 -04:00
2023-02-10 15:40:44 -05:00
public export %inline
(.get0) : AnyTerm q -> Term q 0 0
t.get0 = t.get
2022-08-22 04:17:08 -04:00
public export %inline
2023-01-08 14:44:25 -05:00
(.type0) : Definition' q _ -> Term q 0 0
2023-01-08 09:07:01 -05:00
g.type0 = g.type.get
2022-08-22 04:17:08 -04:00
public export %inline
2023-01-08 14:44:25 -05:00
(.term0) : Definition' q _ -> Maybe (Term q 0 0)
2023-01-08 09:07:01 -05:00
g.term0 = map (\t => t.get) g.term
2022-08-22 04:17:08 -04:00
public export %inline
2023-01-08 14:44:25 -05:00
(.qtyP) : forall q, isGlobal. Definition' q isGlobal -> Subset q isGlobal
2022-08-22 04:17:08 -04:00
g.qtyP = Element g.qty g.qtyGlobal
2023-01-20 19:41:21 -05:00
public export %inline
toElim : Definition' q _ -> Maybe $ Elim q d n
toElim def = pure $ (!def.term).get :# def.type.get
2023-01-20 19:41:21 -05:00
public export
0 IsZero : IsQty q => Pred $ Definition q
IsZero g = IsZero g.qty
2022-08-22 04:17:08 -04:00
public export %inline
2023-01-20 19:41:21 -05:00
isZero : (p : IsQty q) => Dec1 $ Definition.IsZero @{p}
isZero g = isZero g.qty
2023-01-08 14:44:25 -05:00
public export
2023-01-20 19:41:21 -05:00
0 Definitions' : (q : Type) -> Pred q -> Type
2023-01-08 14:44:25 -05:00
Definitions' q isGlobal = SortedMap Name $ Definition' q isGlobal
2022-08-22 04:17:08 -04:00
public export
2023-01-08 14:44:25 -05:00
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)
2023-01-20 19:41:30 -05:00
public export
2023-01-08 14:44:25 -05:00
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)
parameters {0 isGlobal : _} (defs : Definitions' q isGlobal)
namespace Term
public export %inline
isRedex : Term q d n -> Bool
isRedex = isRedex $ \x => lookupElim x defs
public export
0 IsRedex, NotRedex : Pred $ Term q d n
IsRedex = So . isRedex
NotRedex = No . isRedex
namespace Elim
public export %inline
isRedex : Elim q d n -> Bool
isRedex = isRedex $ \x => lookupElim x defs
public export
0 IsRedex, NotRedex : Pred $ Elim q d n
IsRedex = So . isRedex
NotRedex = No . isRedex
public export
0 NonRedexElim, NonRedexTerm :
(q : Type) -> (d, n : Nat) -> {isGlobal : Pred q} ->
Definitions' q isGlobal -> Type
NonRedexElim q d n defs = Subset (Elim q d n) (NotRedex defs)
NonRedexTerm q d n defs = Subset (Term q d n) (NotRedex defs)
parameters {0 isGlobal : _} (defs : Definitions' q isGlobal)
namespace Term
export %inline
2023-02-10 15:40:44 -05:00
whnfD : Term q d n -> NonRedexTerm q d n defs
whnfD = whnf $ \x => lookupElim x defs
namespace Elim
export %inline
2023-02-10 15:40:44 -05:00
whnfD : Elim q d n -> NonRedexElim q d n defs
whnfD = whnf $ \x => lookupElim x defs