53 lines
1.2 KiB
Idris
53 lines
1.2 KiB
Idris
|
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
|