module Quox.Syntax.Qty

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

%default total


public export
interface Eq q => IsQty q where
  zero, one, any : q

  (+), (*) : q -> q -> q
  lub      : q -> q -> Maybe 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

  ||| true if bindings of this quantity can be used any number of times.
  ||| this is needed for natural elimination
  IsAny : Pred q
  isAny : Dec1 IsAny
  anyIsAny : IsAny any

  ||| ``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` ω``.
  ||| if ``π `lub` ρ`` exists, then both `π` and `ρ` must be compatible with it
  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 pi
  anyIsGlobal : forall pi. IsAny pi -> IsGlobal pi

  ||| prints in a form that can be a suffix of "case"
  prettySuffix : Pretty.HasEnv m => q -> m (Doc HL)

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

public export %inline
gany : IsQty q => GQty q
gany = Element any $ anyIsGlobal anyIsAny

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