quox/lib/Quox/Syntax/Qty.idr

154 lines
4 KiB
Idris
Raw Normal View History

2023-04-01 13:16:43 -04:00
||| 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
2021-07-20 16:05:19 -04:00
module Quox.Syntax.Qty
import Quox.Pretty
2023-04-01 13:16:43 -04:00
import Quox.Decidable
2023-01-08 14:44:25 -05:00
import Data.DPair
2023-04-01 13:16:43 -04:00
import Derive.Prelude
2021-07-20 16:05:19 -04:00
2022-05-02 16:38:37 -04:00
%default total
2023-04-01 13:16:43 -04:00
%language ElabReflection
2021-07-20 16:05:19 -04:00
2023-04-01 13:16:43 -04:00
||| 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
2021-07-20 16:05:19 -04:00
public export
2023-04-01 13:16:43 -04:00
data Qty = Zero | One | Any
%runElab derive "Qty" [Eq, Ord, Show]
2023-05-14 13:58:46 -04:00
%name Qty.Qty pi, rh
2023-04-01 13:16:43 -04:00
2023-04-01 13:16:43 -04:00
export
2023-05-14 13:58:46 -04:00
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 "#")
2023-04-01 13:16:43 -04:00
||| prints in a form that can be a suffix of "case"
public export
2023-05-14 13:58:46 -04:00
prettySuffix : {opts : _} -> Qty -> Eff Pretty (Doc opts)
prettySuffix = prettyQty
2023-04-01 13:16:43 -04:00
||| 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
2023-04-17 15:41:10 -04:00
||| "π ρ"
2023-04-01 13:16:43 -04:00
|||
2023-05-12 11:28:29 -04:00
||| returns a quantity τ with π ≤ τ and ρ ≤ τ.
||| if π = ρ, then it's that, otherwise it's ω.
2023-04-01 13:16:43 -04:00
public export
2023-05-12 11:28:29 -04:00
lub : Qty -> Qty -> Qty
lub p q = if p == q then p else Any
2023-04-01 13:16:43 -04:00
||| 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]
%name Qty.SQty sg
2022-08-22 04:07:46 -04:00
||| "σ ⨴ π"
|||
||| σ ⨴ π is 0 if either of σ or π are, otherwise it is σ.
2023-04-01 13:16:43 -04:00
public export
subjMult : SQty -> Qty -> SQty
subjMult _ Zero = SZero
2023-04-01 13:16:43 -04:00
subjMult sg _ = sg
2023-04-01 13:16:43 -04:00
||| 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]
%name GQty rh
2023-01-08 14:44:25 -05:00
2023-04-01 13:16:43 -04:00
public export
toGlobal : Qty -> Maybe GQty
toGlobal Zero = Just GZero
toGlobal Any = Just GAny
toGlobal One = Nothing
2023-04-01 10:01:53 -04:00
2023-04-01 13:16:43 -04:00
||| 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