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

simplify isEmpty and isSubSing

This commit is contained in:
rhiannon morris 2023-09-30 18:32:26 +02:00
parent da2278e390
commit d15ce34164
1 changed files with 4 additions and 16 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

20
lib/Quox/Equal.idr
View File

@ -74,6 +74,8 @@ isEmpty : {n : Nat} -> Definitions -> EqContext n -> SQty -> Term 0 n ->
Eff EqualInner Bool Eff EqualInner Bool
isEmpty defs ctx sg ty0 = do isEmpty defs ctx sg ty0 = do
Element ty0 nc <- whnf defs ctx sg ty0.loc ty0 Element ty0 nc <- whnf defs ctx sg ty0.loc ty0
let Left y = choose $ isTyConE ty0
| Right n => pure False
case ty0 of case ty0 of
TYPE {} => pure False TYPE {} => pure False
Pi {arg, res, _} => pure False Pi {arg, res, _} => pure False
@ -85,15 +87,7 @@ isEmpty defs ctx sg ty0 = do
Eq {} => pure False Eq {} => pure False
Nat {} => pure False Nat {} => pure False
BOX {ty, _} => isEmpty defs ctx sg ty BOX {ty, _} => isEmpty defs ctx sg ty
E (Ann {tm, _}) => isEmpty defs ctx sg tm
E _ => pure False E _ => pure False
Lam {} => pure False
Pair {} => pure False
Tag {} => pure False
DLam {} => pure False
Zero {} => pure False
Succ {} => pure False
Box {} => pure False
||| true if a type is known to be a subsingleton purely by its form. ||| true if a type is known to be a subsingleton purely by its form.
||| a subsingleton is a type with only zero or one possible values. ||| a subsingleton is a type with only zero or one possible values.
@ -110,6 +104,8 @@ isSubSing : {n : Nat} -> Definitions -> EqContext n -> SQty -> Term 0 n ->
Eff EqualInner Bool Eff EqualInner Bool
isSubSing defs ctx sg ty0 = do isSubSing defs ctx sg ty0 = do
Element ty0 nc <- whnf defs ctx sg ty0.loc ty0 Element ty0 nc <- whnf defs ctx sg ty0.loc ty0
let Left y = choose $ isTyConE ty0
| Right n => pure False
case ty0 of case ty0 of
TYPE {} => pure False TYPE {} => pure False
Pi {arg, res, _} => Pi {arg, res, _} =>
@ -123,15 +119,7 @@ isSubSing defs ctx sg ty0 = do
Eq {} => pure True Eq {} => pure True
Nat {} => pure False Nat {} => pure False
BOX {ty, _} => isSubSing defs ctx sg ty BOX {ty, _} => isSubSing defs ctx sg ty
E (Ann {tm, _}) => isSubSing defs ctx sg tm
E _ => pure False E _ => pure False
Lam {} => pure False
Pair {} => pure False
Tag {} => pure False
DLam {} => pure False
Zero {} => pure False
Succ {} => pure False
Box {} => pure False
||| the left argument if the current mode is `Super`; otherwise the right one. ||| the left argument if the current mode is `Super`; otherwise the right one.