quox/src/Quox/Syntax/Qty.idr

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