quox/lib/Quox/Syntax/Qty.idr

90 lines
2.2 KiB
Idris
Raw Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

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