Default.hs

-- SPDX-FileCopyrightText: 2020 Tocqueville Group
--
-- SPDX-License-Identifier: LicenseRef-MIT-TQ

-- | Default values for Lorentz.
module Lorentz.Default
  ( LDefault (..)
  ) where

import qualified Prelude as P

import Lorentz.Base
import Lorentz.Coercions
import Lorentz.Constraints
import Lorentz.Instr
import Lorentz.Macro
import Lorentz.Value
import Morley.Util.Named
import Morley.Util.TypeLits

-- | Lorentz version of 'Default'.
class LDefault a where
  ldef :: a
  default ldef :: Default a => a
  ldef = def

  lIsDef :: a : s :-> Bool : s
  default lIsDef
    :: (NiceConstant a, NiceComparable a) => a : s :-> Bool : s
  lIsDef = push ldef # eq

instance LDefault Integer
instance LDefault Natural

instance LDefault [a] where
  lIsDef = isEmpty
instance LDefault (Set k) where
  lIsDef = isEmpty
instance LDefault (Map k v) where
  lIsDef = isEmpty
-- We do not provide an instance for 'BigMap' since
-- it cannot be checked on emptiness

instance (LDefault a, KnownSymbol n) => LDefault (NamedF P.Identity a n) where
  ldef = P.fromLabel :! ldef
  lIsDef = fromNamed P.fromLabel # lIsDef

instance (LDefault a, LDefault b) => LDefault (a, b) where
  ldef = (ldef, ldef)
  lIsDef = unpair # dip lIsDef # lIsDef # and