55 lines
997 B
Idris
55 lines
997 B
Idris
module Quox.Syntax.Qty
|
||
|
||
import Quox.Pretty
|
||
|
||
import Data.Fin
|
||
|
||
|
||
public export
|
||
data Qty = Zero | One | Any
|
||
%name Qty.Qty pi, rh
|
||
|
||
private Repr : Type
|
||
Repr = Fin 3
|
||
|
||
private %inline repr : Qty -> Repr
|
||
repr pi = case pi of Zero => 0; One => 1; Any => 2
|
||
|
||
export Eq Qty where (==) = (==) `on` repr
|
||
export Ord Qty where compare = compare `on` repr
|
||
|
||
|
||
export
|
||
PrettyHL Qty where
|
||
prettyM pi = hl Qty <$>
|
||
case pi of
|
||
Zero => ifUnicode "𝟬" "0"
|
||
One => ifUnicode "𝟭" "1"
|
||
Any => ifUnicode "𝛚" "*"
|
||
|
||
export %inline
|
||
prettyQtyBinds : Pretty.HasEnv m => List Qty -> m (Doc HL)
|
||
prettyQtyBinds =
|
||
map (align . sep) .
|
||
traverse (\pi => [|pretty0M pi <++> pure (hl Delim "|")|])
|
||
|
||
|
||
public export
|
||
(+) : Qty -> Qty -> Qty
|
||
Zero + rh = rh
|
||
pi + Zero = pi
|
||
_ + _ = Any
|
||
|
||
public export
|
||
(*) : Qty -> Qty -> Qty
|
||
Zero * _ = Zero
|
||
_ * Zero = Zero
|
||
One * rh = rh
|
||
pi * One = pi
|
||
Any * Any = Any
|
||
|
||
infix 6 <=.
|
||
public export
|
||
(<=.) : Qty -> Qty -> Bool
|
||
pi <=. rh = rh == Any || pi == rh
|