rhi/quox
rhi/quox
1
0
Fork 0
Code Issues 15 Pull requests 1 Releases Wiki Activity

AnyTerm.(.def) => (.get)

Browse source
This commit is contained in:
rhiannon morris 2023-01-08 15:07:01 +01:00
parent 98fa8d9967
commit 9dbd0b066c
3 changed files with 5 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
lib/Quox/Definition.idr
View file

@ -8,7 +8,7 @@ import public Control.Monad.State
public export public export
record AnyTerm where record AnyTerm where
constructor T constructor T
def : forall d, n. Term d n get : forall d, n. Term d n
public export public export
record Definition where record Definition where
@ -33,11 +33,11 @@ MkAbstract {qty, type} =
public export %inline public export %inline
(.type0) : Definition -> Term 0 0 (.type0) : Definition -> Term 0 0
g.type0 = g.type.def g.type0 = g.type.get
public export %inline public export %inline
(.term0) : Definition -> Maybe (Term 0 0) (.term0) : Definition -> Maybe (Term 0 0)
g.term0 = map (\t => t.def) g.term g.term0 = map (\t => t.get) g.term
public export %inline public export %inline
(.qtyP) : Definition -> Subset Qty IsGlobal (.qtyP) : Definition -> Subset Qty IsGlobal

2
lib/Quox/Equal.idr
View file

@ -37,7 +37,7 @@ parameters {auto _ : MonadError Error m} {auto _ : MonadReader Env m}
defE : Name -> m (Maybe (Elim d n)) defE : Name -> m (Maybe (Elim d n))
defE x = asks $ \env => do defE x = asks $ \env => do
g <- lookup x env.defs g <- lookup x env.defs
pure $ (!g.term).def :# g.type.def pure $ (!g.term).get :# g.type.get
private %inline private %inline
defT : Name -> m (Maybe (Term d n)) defT : Name -> m (Maybe (Term d n))

2
lib/Quox/Typechecker.idr
View file

@ -129,7 +129,7 @@ parameters {auto _ : CanTC m}
infer' ctx sg (Element (F x) _) = do infer' ctx sg (Element (F x) _) = do
Just g <- asks $ lookup x | Nothing => throwError $ NotInScope x Just g <- asks $ lookup x | Nothing => throwError $ NotInScope x
when (isZero g) $ expectEqualQ sg Zero when (isZero g) $ expectEqualQ sg Zero
pure $ InfRes {type = g.type.def, qout = zero} pure $ InfRes {type = g.type.get, qout = zero}
infer' ctx sg (Element (B i) _) = infer' ctx sg (Element (B i) _) =
pure $ lookupBound sg i ctx pure $ lookupBound sg i ctx