quox/lib/Quox/Definition.idr

53 lines
1.2 KiB
Idris
Raw Permalink Normal View History

2022-08-22 04:17:08 -04:00
module Quox.Definition
import public Quox.Syntax
import public Data.SortedMap
import public Control.Monad.State
public export
record AnyTerm where
constructor T
def : forall d, n. Term d n
public export
record Definition where
constructor MkDef'
qty : Qty
0 qtyGlobal : IsGlobal qty
type : AnyTerm
term : Maybe AnyTerm
public export %inline
MkDef : (qty : Qty) -> (0 qtyGlobal : IsGlobal qty) =>
(type, term : forall d, n. Term d n) -> Definition
MkDef {qty, type, term} =
MkDef' {qty, qtyGlobal = %search, type = T type, term = Just (T term)}
public export %inline
MkAbstract : (qty : Qty) -> (0 qtyGlobal : IsGlobal qty) =>
(type : forall d, n. Term d n) -> Definition
MkAbstract {qty, type} =
MkDef' {qty, qtyGlobal = %search, type = T type, term = Nothing}
public export %inline
(.type0) : Definition -> Term 0 0
g.type0 = g.type.def
public export %inline
(.term0) : Definition -> Maybe (Term 0 0)
g.term0 = map (\t => t.def) g.term
public export %inline
(.qtyP) : Definition -> Subset Qty IsGlobal
g.qtyP = Element g.qty g.qtyGlobal
public export %inline
isZero : Definition -> Bool
isZero g = g.qty == Zero
public export
Definitions : Type
Definitions = SortedMap Name Definition