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

"WhnfErr" ⇒ "WhnfError"

Browse source
This commit is contained in:
rhiannon morris 2023-03-13 19:39:29 +01:00
parent 765c62866a
commit ecd3be8bda
3 changed files with 8 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
lib/Quox/Reduce.idr
View file

@ -13,7 +13,7 @@ import Data.List
||| errors that might happen if you pass an ill typed expression into ||| errors that might happen if you pass an ill typed expression into
||| whnf. don't do that please ||| whnf. don't do that please
public export public export
data WhnfErr = MissingEnumArm TagVal (List TagVal) data WhnfError = MissingEnumArm TagVal (List TagVal)
public export public export
@ -21,9 +21,7 @@ public export
RedexTest tm = forall q, d, n, g. Definitions' q g -> tm q d n -> Bool RedexTest tm = forall q, d, n, g. Definitions' q g -> tm q d n -> Bool
public export public export
interface Whnf (0 tm : TermLike) interface Whnf (0 tm : TermLike) (0 isRedex : RedexTest tm) (0 err : Type) | tm
(0 isRedex : RedexTest tm)
(0 err : Type) | tm
where where
whnf : (defs : Definitions' q g) -> whnf : (defs : Definitions' q g) ->
tm q d n -> Either err (Subset (tm q d n) (No . isRedex defs)) tm q d n -> Either err (Subset (tm q d n) (No . isRedex defs))
@ -107,7 +105,7 @@ mutual
mutual mutual
export covering export covering
Whnf Elim Reduce.isRedexE WhnfErr where Whnf Elim Reduce.isRedexE WhnfError where
whnf defs (F x) with (lookupElim x defs) proof eq whnf defs (F x) with (lookupElim x defs) proof eq
_ | Just y = whnf defs y _ | Just y = whnf defs y
_ | Nothing = pure $ Element (F x) $ rewrite eq in Ah _ | Nothing = pure $ Element (F x) $ rewrite eq in Ah
@ -173,7 +171,7 @@ mutual
whnf defs (DCloE el th) = whnf defs $ pushSubstsWith' th id el whnf defs (DCloE el th) = whnf defs $ pushSubstsWith' th id el
export covering export covering
Whnf Term Reduce.isRedexT WhnfErr where Whnf Term Reduce.isRedexT WhnfError where
whnf _ t@(TYPE {}) = pure $ nred t whnf _ t@(TYPE {}) = pure $ nred t
whnf _ t@(Pi {}) = pure $ nred t whnf _ t@(Pi {}) = pure $ nred t
whnf _ t@(Lam {}) = pure $ nred t whnf _ t@(Lam {}) = pure $ nred t

4
lib/Quox/Typing.idr
View file

@ -152,7 +152,7 @@ data Error q
(Elim q d n) (Elim q d n) (Elim q d n) (Elim q d n)
(Error q) (Error q)
| WhnfError WhnfErr | WhnfError WhnfError
public export public export
@ -215,7 +215,7 @@ substCasePairRet dty retty =
parameters {auto _ : HasErr q m} (defs : Definitions' q _) parameters {auto _ : HasErr q m} (defs : Definitions' q _)
export covering %inline export covering %inline
whnfT : {0 isRedex : RedexTest tm} -> Whnf tm isRedex WhnfErr => whnfT : {0 isRedex : RedexTest tm} -> Whnf tm isRedex WhnfError =>
tm q d n -> m (NonRedex tm q d n defs) tm q d n -> m (NonRedex tm q d n defs)
whnfT = either (throwError . WhnfError) pure . whnf defs whnfT = either (throwError . WhnfError) pure . whnf defs

4
tests/TypingImpls.idr
View file

@ -9,7 +9,7 @@ import Derive.Prelude
%language ElabReflection %language ElabReflection
%runElab derive "WhnfErr" [Show] %runElab derive "Reduce.WhnfError" [Show]
%runElab deriveIndexed "DimEq" [Show] %runElab deriveIndexed "DimEq" [Show]
@ -22,7 +22,7 @@ showTypingError : (PrettyHL q, Show q) => Show (Error q)
showTypingError = deriveShow showTypingError = deriveShow
export export
ToInfo WhnfErr where ToInfo WhnfError where
toInfo (MissingEnumArm t ts) = toInfo (MissingEnumArm t ts) =
[("type", "MissingEnumArm"), [("type", "MissingEnumArm"),
("tag", show t), ("tag", show t),