-- SPDX-FileCopyrightText: 2021 Oxhead Alpha
-- SPDX-License-Identifier: LicenseRef-MIT-OA

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

import Prelude qualified 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 = a
forall a. Default a => a
def

  lIsDef :: a : s :-> Bool : s
  default lIsDef
    :: (NiceConstant a, NiceComparable a) => a : s :-> Bool : s
  lIsDef = a -> (a : s) :-> (a : a : s)
forall t (s :: [*]). NiceConstant t => t -> s :-> (t : s)
push a
forall a. LDefault a => a
ldef ((a : s) :-> (a : a : s))
-> ((a : a : s) :-> (Bool : s)) -> (a : s) :-> (Bool : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (a : a : s) :-> (Bool : s)
forall n (s :: [*]). NiceComparable n => (n : n : s) :-> (Bool : s)
eq

instance LDefault Integer
instance LDefault Natural

instance LDefault [a] where
  lIsDef :: forall (s :: [*]). ([a] : s) :-> (Bool : s)
lIsDef = ([a] : s) :-> (Bool : s)
forall c (s :: [*]). SizeOpHs c => (c : s) :-> (Bool : s)
isEmpty
instance LDefault (Set k) where
  lIsDef :: forall (s :: [*]). (Set k : s) :-> (Bool : s)
lIsDef = (Set k : s) :-> (Bool : s)
forall c (s :: [*]). SizeOpHs c => (c : s) :-> (Bool : s)
isEmpty
instance LDefault (Map k v) where
  lIsDef :: forall (s :: [*]). (Map k v : s) :-> (Bool : s)
lIsDef = (Map k v : s) :-> (Bool : s)
forall c (s :: [*]). SizeOpHs c => (c : s) :-> (Bool : s)
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 :: NamedF Identity a n
ldef = forall (x :: Symbol) a. IsLabel x a => a
P.fromLabel @n Name n -> a -> NamedF Identity a n
forall (name :: Symbol) a. Name name -> a -> NamedF Identity a name
:! a
forall a. LDefault a => a
ldef
  lIsDef :: forall (s :: [*]). (NamedF Identity a n : s) :-> (Bool : s)
lIsDef = Label n -> (NamedF Identity a n : s) :-> (a : s)
forall (name :: Symbol) a (s :: [*]).
Label name -> ((name :! a) : s) :-> (a : s)
fromNamed (forall (x :: Symbol) a. IsLabel x a => a
P.fromLabel @n) ((NamedF Identity a n : s) :-> (a : s))
-> ((a : s) :-> (Bool : s))
-> (NamedF Identity a n : s) :-> (Bool : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (a : s) :-> (Bool : s)
forall a (s :: [*]). LDefault a => (a : s) :-> (Bool : s)
lIsDef

instance (LDefault a, LDefault b) => LDefault (a, b) where
  ldef :: (a, b)
ldef = (a
forall a. LDefault a => a
ldef, b
forall a. LDefault a => a
ldef)
  lIsDef :: forall (s :: [*]). ((a, b) : s) :-> (Bool : s)
lIsDef = ((a, b) : s) :-> (a : b : s)
forall a b (s :: [*]). ((a, b) : s) :-> (a : b : s)
unpair (((a, b) : s) :-> (a : b : s))
-> ((a : b : s) :-> (a : Bool : s))
-> ((a, b) : s) :-> (a : Bool : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# ((b : s) :-> (Bool : s)) -> (a : b : s) :-> (a : Bool : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip (b : s) :-> (Bool : s)
forall a (s :: [*]). LDefault a => (a : s) :-> (Bool : s)
lIsDef (((a, b) : s) :-> (a : Bool : s))
-> ((a : Bool : s) :-> (Bool : Bool : s))
-> ((a, b) : s) :-> (Bool : Bool : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (a : Bool : s) :-> (Bool : Bool : s)
forall a (s :: [*]). LDefault a => (a : s) :-> (Bool : s)
lIsDef (((a, b) : s) :-> (Bool : Bool : s))
-> ((Bool : Bool : s) :-> (Bool : s))
-> ((a, b) : s) :-> (Bool : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Bool : Bool : s) :-> (Bool : s)
forall n m r (s :: [*]).
ArithOpHs And n m r =>
(n : m : s) :-> (r : s)
and