154 lines
4 KiB
Idris
154 lines
4 KiB
Idris
||| quantities count how many times a bound variable is used [@nuttin; @qtt].
|
||
|||
|
||
||| i tried grtt [@grtt] for a bit but i think it was more complex than
|
||
||| it's worth in a language that has other stuff going on too
|
||
module Quox.Syntax.Qty
|
||
|
||
import Quox.Pretty
|
||
import Quox.Decidable
|
||
import Quox.PrettyValExtra
|
||
import Data.DPair
|
||
import Derive.Prelude
|
||
|
||
%default total
|
||
%language ElabReflection
|
||
|
||
|
||
||| the possibilities we care about are:
|
||
|||
|
||
||| - 0: a variable is used only at compile time, not run time
|
||
||| - 1: a variable is used exactly once at run time
|
||
||| - ω (or #): don't care. an ω variable *can* also be used 0/1 time
|
||
public export
|
||
data Qty = Zero | One | Any
|
||
%runElab derive "Qty" [Eq, Ord, Show, PrettyVal]
|
||
%name Qty.Qty pi, rh
|
||
|
||
|
||
export
|
||
prettyQty : {opts : _} -> Qty -> Eff Pretty (Doc opts)
|
||
prettyQty Zero = hl Qty $ text "0"
|
||
prettyQty One = hl Qty $ text "1"
|
||
prettyQty Any = hl Qty =<< ifUnicode (text "ω") (text "#")
|
||
|
||
||| prints in a form that can be a suffix of "case"
|
||
public export
|
||
prettySuffix : {opts : _} -> Qty -> Eff Pretty (Doc opts)
|
||
prettySuffix = prettyQty
|
||
|
||
|
||
||| e.g. if in the expression `(s, t)`, the variable `x` is
|
||
||| used π times in `s` and ρ times in `t`, then it's used
|
||
||| (π + ρ) times in the whole expression
|
||
public export
|
||
(+) : Qty -> Qty -> Qty
|
||
Zero + rh = rh
|
||
pi + Zero = pi
|
||
_ + _ = Any
|
||
|
||
||| e.g. if a function `f` uses its argument π times,
|
||
||| and `f x` occurs in a σ context, then `x` is used `πσ` times overall
|
||
public export
|
||
(*) : Qty -> Qty -> Qty
|
||
Zero * _ = Zero
|
||
_ * Zero = Zero
|
||
One * rh = rh
|
||
pi * One = pi
|
||
Any * Any = Any
|
||
|
||
||| "π ≤ ρ"
|
||
|||
|
||
||| if a variable is bound with quantity ρ, then it can be used with a total
|
||
||| quantity π as long as π ≤ ρ. for example, an ω variable can be used any
|
||
||| number of times, so π ≤ ω for any π.
|
||
public export
|
||
compat : Qty -> Qty -> Bool
|
||
compat pi Any = True
|
||
compat pi rh = pi == rh
|
||
|
||
|
||
||| "π ∨ ρ"
|
||
|||
|
||
||| returns a quantity τ with π ≤ τ and ρ ≤ τ.
|
||
||| if π = ρ, then it's that, otherwise it's ω.
|
||
public export
|
||
lub : Qty -> Qty -> Qty
|
||
lub p q = if p == q then p else Any
|
||
|
||
|
||
||| to maintain subject reduction, only 0 or 1 can occur
|
||
||| for the subject of a typing judgment. see @qtt, §2.3 for more detail
|
||
public export
|
||
data SQty = SZero | SOne
|
||
%runElab derive "SQty" [Eq, Ord, Show, PrettyVal]
|
||
%name Qty.SQty sg
|
||
|
||
||| "σ ⨴ π"
|
||
|||
|
||
||| σ ⨴ π is 0 if either of σ or π are, otherwise it is σ.
|
||
public export
|
||
subjMult : SQty -> Qty -> SQty
|
||
subjMult _ Zero = SZero
|
||
subjMult sg _ = sg
|
||
|
||
|
||
||| it doesn't make much sense for a top level declaration to have a
|
||
||| quantity of 1, so the only distinction is whether it is present
|
||
||| at runtime at all or not
|
||
public export
|
||
data GQty = GZero | GAny
|
||
%runElab derive "GQty" [Eq, Ord, Show, PrettyVal]
|
||
%name GQty rh
|
||
|
||
public export
|
||
toGlobal : Qty -> Maybe GQty
|
||
toGlobal Zero = Just GZero
|
||
toGlobal Any = Just GAny
|
||
toGlobal One = Nothing
|
||
|
||
||| when checking a definition, a 0 definition is checked at 0,
|
||
||| but an ω definition is checked at 1 since ω isn't a subject quantity
|
||
public export %inline
|
||
globalToSubj : GQty -> SQty
|
||
globalToSubj GZero = SZero
|
||
globalToSubj GAny = SOne
|
||
|
||
|
||
public export
|
||
DecEq Qty where
|
||
decEq Zero Zero = Yes Refl
|
||
decEq Zero One = No $ \case _ impossible
|
||
decEq Zero Any = No $ \case _ impossible
|
||
decEq One Zero = No $ \case _ impossible
|
||
decEq One One = Yes Refl
|
||
decEq One Any = No $ \case _ impossible
|
||
decEq Any Zero = No $ \case _ impossible
|
||
decEq Any One = No $ \case _ impossible
|
||
decEq Any Any = Yes Refl
|
||
|
||
public export
|
||
DecEq SQty where
|
||
decEq SZero SZero = Yes Refl
|
||
decEq SZero SOne = No $ \case _ impossible
|
||
decEq SOne SZero = No $ \case _ impossible
|
||
decEq SOne SOne = Yes Refl
|
||
|
||
public export
|
||
DecEq GQty where
|
||
decEq GZero GZero = Yes Refl
|
||
decEq GZero GAny = No $ \case _ impossible
|
||
decEq GAny GZero = No $ \case _ impossible
|
||
decEq GAny GAny = Yes Refl
|
||
|
||
|
||
namespace SQty
|
||
public export %inline
|
||
(.qty) : SQty -> Qty
|
||
(SZero).qty = Zero
|
||
(SOne).qty = One
|
||
|
||
namespace GQty
|
||
public export %inline
|
||
(.qty) : GQty -> Qty
|
||
(GZero).qty = Zero
|
||
(GAny).qty = Any
|