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
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 :: ([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 :: (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 :: (Map k v : s) :-> (Bool : s)
lIsDef = (Map k v : s) :-> (Bool : s)
forall c (s :: [*]). SizeOpHs c => (c : s) :-> (Bool : s)
isEmpty
instance (LDefault a, KnownSymbol n) => LDefault (NamedF P.Identity a n) where
ldef :: NamedF Identity a n
ldef = forall a. IsLabel n a => a
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 :: (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 a. IsLabel n a => a
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 :: ((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