quox/lib/Quox/Syntax/Qty.idr

module Quox.Syntax.Qty

import Quox.Pretty
import Quox.Name
import public Quox.Decidable
import Data.DPair

%default total


private
commas : List (Doc HL) -> List (Doc HL)
commas []      = []
commas [x]     = [x]
commas (x::xs) = (x <+> hl Delim ",") :: commas xs

private %inline
blobD : Pretty.HasEnv m => m (Doc HL)
blobD = hlF Delim $ ifUnicode "·" "@"

export %inline
prettyQtyBinds : Pretty.HasEnv m => PrettyHL q => PrettyHL a =>
                 List q -> a -> m (Doc HL)
prettyQtyBinds []   x = pretty0M x
prettyQtyBinds qtys x = pure $
  hang 2 $ sep [aseparate comma !(traverse pretty0M qtys) <++> !blobD,
                !(pretty0M x)]


public export
interface Eq q => IsQty q where
  zero, one : q
  (+),  (*) : q -> q -> q

  ||| true if bindings of this quantity will be erased
  ||| and must not be runtime relevant
  IsZero : Pred q
  isZero : Dec1 IsZero
  zeroIsZero : IsZero zero

  ||| ``p `Compat` q`` if it is ok for a binding of
  ||| quantity `q` to be used exactly `p` times.
  ||| e.g. ``1 `Compat` 1``, ``1 `Compat` ω``
  Compat : Rel q
  compat : Dec2 Compat

  ||| true if it is ok for this quantity to appear for the
  ||| subject of a typing judgement [@qtt, §2.3].
  IsSubj : Pred q
  isSubj : Dec1 IsSubj
  zeroIsSubj : forall pi. IsZero pi -> IsSubj pi
  oneIsSubj  : IsSubj one
  timesSubj  : forall pi, rh. IsSubj pi -> IsSubj rh -> IsSubj (pi * rh)

  ||| true if it is ok for a global definition to have this
  ||| quantity. so not exact usage counts, maybe.
  IsGlobal : Pred q
  isGlobal : Dec1 IsGlobal
  zeroIsGlobal : forall pi. IsZero pi -> IsGlobal zero

public export
0 SQty : (q : Type) -> IsQty q => Type
SQty q = Subset q IsSubj

public export %inline
szero : IsQty q => SQty q
szero = Element zero $ zeroIsSubj zeroIsZero

public export %inline
sone : IsQty q => SQty q
sone = Element one oneIsSubj

||| "σ ⨴ π"
|||
||| ``sg `subjMult` pi`` is equal to `pi` if it is zero, otherwise it
||| is equal to `sg`.
public export %inline
subjMult : IsQty q => SQty q -> q -> SQty q
subjMult sg pi = case isZero pi of
  Yes y => Element pi $ zeroIsSubj y
  No  _ => sg


public export
0 GQty : (q : Type) -> IsQty q => Type
GQty q = Subset q IsGlobal

public export %inline
gzero : IsQty q => GQty q
gzero = Element zero $ zeroIsGlobal zeroIsZero

export %inline
globalToSubj : IsQty q => GQty q -> SQty q
globalToSubj q = if isYes $ isZero q.fst then szero else sone