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

{-# LANGUAGE FunctionalDependencies #-}
{-# OPTIONS_GHC -Wno-unticked-promoted-constructors #-}

module Lorentz.ADT
  ( HasField
  , HasFieldOfType
  , HasFieldsOfType
  , NamedField (..)
  , (:=)
  , toField
  , toFieldNamed
  , getField
  , getFieldNamed
  , setField
  , modifyField
  , construct
  , constructT
  , constructStack
  , deconstruct
  , fieldCtor
  , wrap_
  , wrapOne
  , case_
  , caseT
  , unsafeUnwrap_
  , CaseTC
  , CaseArrow (..)
  , CaseClauseL (..)
  , InstrConstructC
  , ConstructorFieldTypes

    -- * Useful re-exports
  , Rec (..)
  , (:!)
  , (:?)
  ) where

import Data.Constraint ((\\))
import Data.Vinyl.Core (RMap(..), Rec(..))
import GHC.TypeLits (AppendSymbol, Symbol)

import Lorentz.Base
import Lorentz.Coercions
import Lorentz.Constraints
import Morley.Michelson.Typed.Haskell.Instr
import Morley.Michelson.Typed.Haskell.Value
import Morley.Michelson.Typed.Instr
import Morley.Util.Label (Label)
import Morley.Util.Named
import Morley.Util.Type (KnownList, type (++))
import Morley.Util.TypeTuple

-- | Allows field access and modification.
type HasField dt fname =
  ( InstrGetFieldC dt fname
  , InstrSetFieldC dt fname
  )

-- | Like 'HasField', but allows constrainting field type.
type HasFieldOfType dt fname fieldTy =
  ( HasField dt fname
  , GetFieldType dt fname ~ fieldTy
  )

-- | A pair of field name and type.
data NamedField = NamedField Symbol Type
type n := ty = 'NamedField n ty
infixr 0 :=

-- | Shortcut for multiple 'HasFieldOfType' constraints.
type family HasFieldsOfType (dt :: Type) (fs :: [NamedField])
             :: Constraint where
  HasFieldsOfType _ '[] = ()
  HasFieldsOfType dt ((n := ty) ': fs) =
    (HasFieldOfType dt n ty, HasFieldsOfType dt fs)

-- | Extract a field of a datatype replacing the value of this
-- datatype with the extracted field.
--
-- For this and the following functions you have to specify field name
-- which is either record name or name attached with @(:!)@ operator.
toField
  :: forall dt name st.
     InstrGetFieldC dt name
  => Label name -> dt : st :-> GetFieldType dt name : st
toField :: Label name -> (dt : st) :-> (GetFieldType dt name : st)
toField = Instr
  (GValueType (Rep dt) : ToTs st)
  (ToT (GetFieldType dt name) : ToTs st)
-> (dt : st) :-> (GetFieldType dt name : st)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I (Instr
   (GValueType (Rep dt) : ToTs st)
   (ToT (GetFieldType dt name) : ToTs st)
 -> (dt : st) :-> (GetFieldType dt name : st))
-> (Label name
    -> Instr
         (GValueType (Rep dt) : ToTs st)
         (ToT (GetFieldType dt name) : ToTs st))
-> Label name
-> (dt : st) :-> (GetFieldType dt name : st)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall dt (name :: Symbol) (st :: [T]).
InstrGetFieldC dt name =>
Label name -> Instr (ToT dt : st) (ToT (GetFieldType dt name) : st)
forall (name :: Symbol) (st :: [T]).
InstrGetFieldC dt name =>
Label name -> Instr (ToT dt : st) (ToT (GetFieldType dt name) : st)
instrToField @dt

-- | Like 'toField', but leaves field named.
toFieldNamed
  :: forall dt name st.
     InstrGetFieldC dt name
  => Label name -> dt : st :-> (name :! GetFieldType dt name) : st
toFieldNamed :: Label name -> (dt : st) :-> ((name :! GetFieldType dt name) : st)
toFieldNamed Label name
l = Label name -> (dt : st) :-> (GetFieldType dt name : st)
forall dt (name :: Symbol) (st :: [*]).
InstrGetFieldC dt name =>
Label name -> (dt : st) :-> (GetFieldType dt name : st)
toField Label name
l ((dt : st) :-> (GetFieldType dt name : st))
-> ((GetFieldType dt name : st)
    :-> ((name :! GetFieldType dt name) : st))
-> (dt : st) :-> ((name :! GetFieldType dt name) : st)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# Label name
-> (GetFieldType dt name : st)
   :-> ((name :! GetFieldType dt name) : st)
forall (name :: Symbol) a (s :: [*]).
Label name -> (a : s) :-> ((name :! a) : s)
toNamed Label name
l

-- | Extract a field of a datatype, leaving the original datatype on stack.
--
-- TODO: [#585] Make this and all depending functions require only
-- @Dupable (GetFieldType dt name)@
getField
  :: forall dt name st.
     (InstrGetFieldC dt name, Dupable dt)
  => Label name -> dt : st :-> GetFieldType dt name : dt ': st
getField :: Label name -> (dt : st) :-> (GetFieldType dt name : dt : st)
getField Label name
l = (dt : st) :-> (dt : dt : st)
forall a (s :: [*]). Dupable a => (a : s) :-> (a : a : s)
dup ((dt : st) :-> (dt : dt : st))
-> ((dt : dt : st) :-> (GetFieldType dt name : dt : st))
-> (dt : st) :-> (GetFieldType dt name : dt : st)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# Label name -> (dt : dt : st) :-> (GetFieldType dt name : dt : st)
forall dt (name :: Symbol) (st :: [*]).
InstrGetFieldC dt name =>
Label name -> (dt : st) :-> (GetFieldType dt name : st)
toField Label name
l
  where
    dup :: forall a s. Dupable a => a : s :-> a : a : s
    dup :: (a : s) :-> (a : a : s)
dup = Instr (ToTs (a : s)) (ToTs (a : a : s)) -> (a : s) :-> (a : a : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I Instr (ToTs (a : s)) (ToTs (a : a : s))
forall (a :: T) (s :: [T]).
DupableScope a =>
Instr (a : s) (a : a : s)
DUP (DupableScope (ToT a) => (a : s) :-> (a : a : s))
-> (((SingI (ToT a), FailOnTicketFound (ContainsTicket (ToT a))),
     KnownValue a)
    :- DupableScope (ToT a))
-> (a : s) :-> (a : a : s)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ ((SingI (ToT a), FailOnTicketFound (ContainsTicket (ToT a))),
 KnownValue a)
:- DupableScope (ToT a)
forall a. Dupable a :- DupableScope (ToT a)
dupableEvi @a

-- | Like 'getField', but leaves field named.
getFieldNamed
  :: forall dt name st.
     (InstrGetFieldC dt name, Dupable dt)
  => Label name -> dt : st :-> (name :! GetFieldType dt name) : dt ': st
getFieldNamed :: Label name
-> (dt : st) :-> ((name :! GetFieldType dt name) : dt : st)
getFieldNamed Label name
l = Label name -> (dt : st) :-> (GetFieldType dt name : dt : st)
forall dt (name :: Symbol) (st :: [*]).
(InstrGetFieldC dt name, Dupable dt) =>
Label name -> (dt : st) :-> (GetFieldType dt name : dt : st)
getField Label name
l ((dt : st) :-> (GetFieldType dt name : dt : st))
-> ((GetFieldType dt name : dt : st)
    :-> ((name :! GetFieldType dt name) : dt : st))
-> (dt : st) :-> ((name :! GetFieldType dt name) : dt : st)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (GetFieldType dt name : dt : st)
:-> ((name :! GetFieldType dt name) : dt : st)
forall a (s :: [*]).
Wrappable a =>
(Unwrappabled a : s) :-> (a : s)
coerceWrap

-- | Set a field of a datatype.
setField
  :: forall dt name st.
     InstrSetFieldC dt name
  => Label name -> (GetFieldType dt name ': dt ': st) :-> (dt ': st)
setField :: Label name -> (GetFieldType dt name : dt : st) :-> (dt : st)
setField = Instr
  (ToT (GetFieldType dt name) : GValueType (Rep dt) : ToTs st)
  (GValueType (Rep dt) : ToTs st)
-> (GetFieldType dt name : dt : st) :-> (dt : st)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I (Instr
   (ToT (GetFieldType dt name) : GValueType (Rep dt) : ToTs st)
   (GValueType (Rep dt) : ToTs st)
 -> (GetFieldType dt name : dt : st) :-> (dt : st))
-> (Label name
    -> Instr
         (ToT (GetFieldType dt name) : GValueType (Rep dt) : ToTs st)
         (GValueType (Rep dt) : ToTs st))
-> Label name
-> (GetFieldType dt name : dt : st) :-> (dt : st)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall dt (name :: Symbol) (st :: [T]).
InstrSetFieldC dt name =>
Label name
-> Instr (ToT (GetFieldType dt name) : ToT dt : st) (ToT dt : st)
forall (name :: Symbol) (st :: [T]).
InstrSetFieldC dt name =>
Label name
-> Instr (ToT (GetFieldType dt name) : ToT dt : st) (ToT dt : st)
instrSetField @dt

-- | Apply given modifier to a datatype field.
modifyField
  :: forall dt name st.
     ( InstrGetFieldC dt name
     , InstrSetFieldC dt name
     , Dupable dt
     )
  => Label name
  -> (forall st0. (GetFieldType dt name ': st0) :-> (GetFieldType dt name ': st0))
  -> dt : st :-> dt : st
modifyField :: Label name
-> (forall (st0 :: [*]).
    (GetFieldType dt name : st0) :-> (GetFieldType dt name : st0))
-> (dt : st) :-> (dt : st)
modifyField Label name
l forall (st0 :: [*]).
(GetFieldType dt name : st0) :-> (GetFieldType dt name : st0)
i = Label name -> (dt : st) :-> (GetFieldType dt name : dt : st)
forall dt (name :: Symbol) (st :: [*]).
(InstrGetFieldC dt name, Dupable dt) =>
Label name -> (dt : st) :-> (GetFieldType dt name : dt : st)
getField @dt Label name
l ((dt : st) :-> (GetFieldType dt name : dt : st))
-> ((GetFieldType dt name : dt : st)
    :-> (GetFieldType dt name : dt : st))
-> (dt : st) :-> (GetFieldType dt name : dt : st)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (GetFieldType dt name : dt : st)
:-> (GetFieldType dt name : dt : st)
forall (st0 :: [*]).
(GetFieldType dt name : st0) :-> (GetFieldType dt name : st0)
i ((dt : st) :-> (GetFieldType dt name : dt : st))
-> ((GetFieldType dt name : dt : st) :-> (dt : st))
-> (dt : st) :-> (dt : st)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# Label name -> (GetFieldType dt name : dt : st) :-> (dt : st)
forall dt (name :: Symbol) (st :: [*]).
InstrSetFieldC dt name =>
Label name -> (GetFieldType dt name : dt : st) :-> (dt : st)
setField @dt Label name
l

-- | Make up a datatype. You provide a pack of individual fields constructors.
--
-- Each element of the accepted record should be an instruction wrapped with
-- 'fieldCtor' function. This instruction will have access to the stack at
-- the moment of calling @construct@.
-- Instructions have to output fields of the built datatype, one per instruction;
-- instructions order is expected to correspond to the order of fields in the
-- datatype.
construct
  :: forall dt st.
     ( InstrConstructC dt
     , RMap (ConstructorFieldTypes dt)
     )
  => Rec (FieldConstructor st) (ConstructorFieldTypes dt)
  -> st :-> dt : st
construct :: Rec (FieldConstructor st) (ConstructorFieldTypes dt)
-> st :-> (dt : st)
construct Rec (FieldConstructor st) (ConstructorFieldTypes dt)
fctors =
  Instr (ToTs st) (ToTs (dt : st)) -> st :-> (dt : st)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I (Instr (ToTs st) (ToTs (dt : st)) -> st :-> (dt : st))
-> Instr (ToTs st) (ToTs (dt : st)) -> st :-> (dt : st)
forall a b. (a -> b) -> a -> b
$ forall (st :: [T]).
InstrConstructC dt =>
Rec (FieldConstructor st) (ConstructorFieldTypes dt)
-> Instr st (ToT dt : st)
forall dt (st :: [T]).
InstrConstructC dt =>
Rec (FieldConstructor st) (ConstructorFieldTypes dt)
-> Instr st (ToT dt : st)
instrConstruct @dt (Rec (FieldConstructor (ToTs st)) (ConstructorFieldTypes dt)
 -> Instr (ToTs st) (ToT dt : ToTs st))
-> Rec (FieldConstructor (ToTs st)) (ConstructorFieldTypes dt)
-> Instr (ToTs st) (ToT dt : ToTs st)
forall a b. (a -> b) -> a -> b
$
  (forall x. FieldConstructor st x -> FieldConstructor (ToTs st) x)
-> Rec (FieldConstructor st) (ConstructorFieldTypes dt)
-> Rec (FieldConstructor (ToTs st)) (ConstructorFieldTypes dt)
forall u (rs :: [u]) (f :: u -> *) (g :: u -> *).
RMap rs =>
(forall (x :: u). f x -> g x) -> Rec f rs -> Rec g rs
rmap (\(FieldConstructor i) -> Instr (ToTs' (ToTs st)) (ToT x : ToTs' (ToTs st))
-> FieldConstructor (ToTs st) x
forall k (st :: [k]) field.
Instr (ToTs' st) (ToT field : ToTs' st)
-> FieldConstructor st field
FieldConstructor Instr (ToTs' st) (ToT x : ToTs' st)
Instr (ToTs' (ToTs st)) (ToT x : ToTs' (ToTs st))
i) Rec (FieldConstructor st) (ConstructorFieldTypes dt)
fctors

-- | Version of 'construct' which accepts tuple of field constructors.
constructT
  :: forall dt fctors st.
     ( InstrConstructC dt
     , RMap (ConstructorFieldTypes dt)
     , fctors ~ Rec (FieldConstructor st) (ConstructorFieldTypes dt)
     , RecFromTuple fctors
     )
  => IsoRecTuple fctors
  -> st :-> dt : st
constructT :: IsoRecTuple fctors -> st :-> (dt : st)
constructT = Rec (FieldConstructor st) (GFieldTypes (Rep dt))
-> st :-> (dt : st)
forall dt (st :: [*]).
(InstrConstructC dt, RMap (ConstructorFieldTypes dt)) =>
Rec (FieldConstructor st) (ConstructorFieldTypes dt)
-> st :-> (dt : st)
construct (Rec (FieldConstructor st) (GFieldTypes (Rep dt))
 -> st :-> (dt : st))
-> (IsoRecTuple (Rec (FieldConstructor st) (GFieldTypes (Rep dt)))
    -> Rec (FieldConstructor st) (GFieldTypes (Rep dt)))
-> IsoRecTuple (Rec (FieldConstructor st) (GFieldTypes (Rep dt)))
-> st :-> (dt : st)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IsoRecTuple (Rec (FieldConstructor st) (GFieldTypes (Rep dt)))
-> Rec (FieldConstructor st) (GFieldTypes (Rep dt))
forall r. RecFromTuple r => IsoRecTuple r -> r
recFromTuple

-- | Construct an object from fields on the stack.
constructStack
  :: forall dt fields st .
  ( InstrConstructC dt
  , fields ~ ConstructorFieldTypes dt
  , KnownList fields
  )
  => (fields ++ st) :-> dt : st
constructStack :: (fields ++ st) :-> (dt : st)
constructStack =
  Instr (ToTs (fields ++ st)) (ToTs (dt : st))
-> (fields ++ st) :-> (dt : st)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I (forall (st :: [T]).
(InstrConstructC dt, ToTs fields ~ ToTs (ConstructorFieldTypes dt),
 KnownList (ToTs fields)) =>
Instr (ToTs fields ++ st) (ToT dt : st)
forall dt (stack :: [T]) (st :: [T]).
(InstrConstructC dt, stack ~ ToTs (ConstructorFieldTypes dt),
 KnownList stack) =>
Instr (stack ++ st) (ToT dt : st)
instrConstructStack @dt @(ToTs fields))
      (KnownList (ToTs fields) => (fields ++ st) :-> (dt : st))
-> (KnownList fields :- KnownList (ToTs fields))
-> (fields ++ st) :-> (dt : st)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ KnownList fields :- KnownList (ToTs fields)
forall (s :: [*]). KnownList s :- KnownList (ToTs s)
totsKnownLemma @fields
      ((ToTs (fields ++ st) ~ (ToTs fields ++ ToTs st)) =>
 (fields ++ st) :-> (dt : st))
-> Dict (ToTs (fields ++ st) ~ (ToTs fields ++ ToTs st))
-> (fields ++ st) :-> (dt : st)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ KnownList fields =>
Dict (ToTs (fields ++ st) ~ (ToTs fields ++ ToTs st))
forall (a :: [*]) (b :: [*]).
KnownList a =>
Dict (ToTs (a ++ b) ~ (ToTs a ++ ToTs b))
totsAppendLemma @fields @st

-- | Decompose a complex object into its fields
deconstruct
  :: forall dt fields st .
  ( InstrDeconstructC dt
  , KnownList fields
  , fields ~ ConstructorFieldTypes dt
  )
  => dt : st :-> (fields ++ st)
deconstruct :: (dt : st) :-> (fields ++ st)
deconstruct =
  Instr (ToTs (dt : st)) (ToTs (fields ++ st))
-> (dt : st) :-> (fields ++ st)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I (forall (st :: [T]).
(InstrDeconstructC dt,
 ToTs fields ~ ToTs (ConstructorFieldTypes dt),
 KnownList (ToTs fields)) =>
Instr (ToT dt : st) (ToTs fields ++ st)
forall dt (stack :: [T]) (st :: [T]).
(InstrDeconstructC dt, stack ~ ToTs (ConstructorFieldTypes dt),
 KnownList stack) =>
Instr (ToT dt : st) (stack ++ st)
instrDeconstruct @dt @(ToTs fields))
    (KnownList (ToTs fields) => (dt : st) :-> (fields ++ st))
-> (KnownList fields :- KnownList (ToTs fields))
-> (dt : st) :-> (fields ++ st)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ KnownList fields :- KnownList (ToTs fields)
forall (s :: [*]). KnownList s :- KnownList (ToTs s)
totsKnownLemma @fields
    ((ToTs (fields ++ st) ~ (ToTs fields ++ ToTs st)) =>
 (dt : st) :-> (fields ++ st))
-> Dict (ToTs (fields ++ st) ~ (ToTs fields ++ ToTs st))
-> (dt : st) :-> (fields ++ st)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ KnownList fields =>
Dict (ToTs (fields ++ st) ~ (ToTs fields ++ ToTs st))
forall (a :: [*]) (b :: [*]).
KnownList a =>
Dict (ToTs (a ++ b) ~ (ToTs a ++ ToTs b))
totsAppendLemma @fields @st

-- | Lift an instruction to field constructor.
fieldCtor :: HasCallStack => (st :-> f : st) -> FieldConstructor st f
fieldCtor :: (st :-> (f : st)) -> FieldConstructor st f
fieldCtor = \case
  I Instr (ToTs st) (ToTs (f : st))
i -> Instr (ToTs' st) (ToT f : ToTs' st) -> FieldConstructor st f
forall k (st :: [k]) field.
Instr (ToTs' st) (ToT field : ToTs' st)
-> FieldConstructor st field
FieldConstructor Instr (ToTs st) (ToTs (f : st))
Instr (ToTs' st) (ToT f : ToTs' st)
i
  FI forall (out' :: [T]). Instr (ToTs st) out'
_ -> Text -> FieldConstructor st f
forall a. HasCallStack => Text -> a
error Text
"Field constructor always fails"

-- | Wrap entry in constructor. Useful for sum types.
wrap_
  :: forall dt name st.
     InstrWrapC dt name
  => Label name -> (AppendCtorField (GetCtorField dt name) st) :-> dt : st
wrap_ :: Label name
-> AppendCtorField (GetCtorField dt name) st :-> (dt : st)
wrap_ =
  case (AppendCtorFieldAxiom ('OneField Word) '[Int],
 AppendCtorFieldAxiom 'NoFields '[Int]) =>
Dict (AppendCtorFieldAxiom (GetCtorField dt name) st)
forall (cf :: CtorField) (st :: [*]).
(AppendCtorFieldAxiom ('OneField Word) '[Int],
 AppendCtorFieldAxiom 'NoFields '[Int]) =>
Dict (AppendCtorFieldAxiom cf st)
appendCtorFieldAxiom @(GetCtorField dt name) @st of
    Dict (AppendCtorFieldAxiom (GetCtorField dt name) st)
Dict -> Instr
  (ToTs (AppendCtorField (GetCtorField dt name) st))
  (GValueType (Rep dt) : ToTs st)
-> AppendCtorField (GetCtorField dt name) st :-> (dt : st)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I (Instr
   (ToTs (AppendCtorField (GetCtorField dt name) st))
   (GValueType (Rep dt) : ToTs st)
 -> AppendCtorField (GetCtorField dt name) st :-> (dt : st))
-> (Label name
    -> Instr
         (ToTs (AppendCtorField (GetCtorField dt name) st))
         (GValueType (Rep dt) : ToTs st))
-> Label name
-> AppendCtorField (GetCtorField dt name) st :-> (dt : st)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall dt (name :: Symbol) (st :: [T]).
InstrWrapC dt name =>
Label name
-> Instr (AppendCtorField (GetCtorField dt name) st) (ToT dt : st)
forall (name :: Symbol) (st :: [T]).
InstrWrapC dt name =>
Label name
-> Instr (AppendCtorField (GetCtorField dt name) st) (ToT dt : st)
instrWrap @dt

-- | Wrap entry in single-field constructor. Useful for sum types.
wrapOne
  :: forall dt name st.
     InstrWrapOneC dt name
  => Label name -> (CtorOnlyField name dt ': st) :-> dt : st
wrapOne :: Label name -> (CtorOnlyField name dt : st) :-> (dt : st)
wrapOne = case (AppendCtorFieldAxiom ('OneField Word) '[Int],
 AppendCtorFieldAxiom 'NoFields '[Int]) =>
Dict (AppendCtorFieldAxiom (GetCtorField dt name) st)
forall (cf :: CtorField) (st :: [*]).
(AppendCtorFieldAxiom ('OneField Word) '[Int],
 AppendCtorFieldAxiom 'NoFields '[Int]) =>
Dict (AppendCtorFieldAxiom cf st)
appendCtorFieldAxiom @(GetCtorField dt name) @st of
  Dict (AppendCtorFieldAxiom (GetCtorField dt name) st)
Dict -> Instr
  (ToT (CtorOnlyField name dt) : ToTs st)
  (GValueType (Rep dt) : ToTs st)
-> (CtorOnlyField name dt : st) :-> (dt : st)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I (Instr
   (ToT (CtorOnlyField name dt) : ToTs st)
   (GValueType (Rep dt) : ToTs st)
 -> (CtorOnlyField name dt : st) :-> (dt : st))
-> (Label name
    -> Instr
         (ToT (CtorOnlyField name dt) : ToTs st)
         (GValueType (Rep dt) : ToTs st))
-> Label name
-> (CtorOnlyField name dt : st) :-> (dt : st)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall dt (name :: Symbol) (st :: [T]).
InstrWrapOneC dt name =>
Label name
-> Instr (ToT (CtorOnlyField name dt) : st) (ToT dt : st)
forall (name :: Symbol) (st :: [T]).
InstrWrapOneC dt name =>
Label name
-> Instr (ToT (CtorOnlyField name dt) : st) (ToT dt : st)
instrWrapOne @dt

-- | Lorentz analogy of 'CaseClause', it works on plain 'Type' types.
data CaseClauseL (inp :: [Type]) (out :: [Type]) (param :: CaseClauseParam) where
  CaseClauseL :: AppendCtorField x inp :-> out -> CaseClauseL inp out ('CaseClauseParam ctor x)

-- | Provides "case" arrow which works on different wrappers for clauses.
class CaseArrow name body clause | clause -> name, clause -> body where
  -- | Lift an instruction to case clause.
  --
  -- You should write out constructor name corresponding to the clause
  -- explicitly. Prefix constructor name with "c" letter, otherwise
  -- your label will not be recognized by Haskell parser.
  -- Passing constructor name can be circumvented but doing so is not recomended
  -- as mentioning contructor name improves readability and allows avoiding
  -- some mistakes.
  (/->) :: Label name -> body -> clause
  infixr 0 /->

instance ( name ~ ("c" `AppendSymbol` ctor)
         , body ~ (AppendCtorField x inp :-> out)
         ) => CaseArrow name body
                (CaseClauseL inp out ('CaseClauseParam ctor x)) where
  /-> :: Label name -> body -> CaseClauseL inp out ('CaseClauseParam ctor x)
(/->) Label name
_ = body -> CaseClauseL inp out ('CaseClauseParam ctor x)
forall (x :: CtorField) (inp :: [*]) (out :: [*]) (ctor :: Symbol).
(AppendCtorField x inp :-> out)
-> CaseClauseL inp out ('CaseClauseParam ctor x)
CaseClauseL

-- | Pattern match on the given sum type.
--
-- You have to provide a 'Rec' containing case branches.
-- To construct a case branch use '/->' operator.
case_
  :: forall dt out inp.
     ( InstrCaseC dt
     , RMap (CaseClauses dt)
     )
  => Rec (CaseClauseL inp out) (CaseClauses dt) -> dt : inp :-> out
case_ :: Rec (CaseClauseL inp out) (CaseClauses dt) -> (dt : inp) :-> out
case_ = RemFail Instr (GValueType (Rep dt) : ToTs inp) (ToTs out)
-> (dt : inp) :-> out
forall (inp :: [*]) (out :: [*]).
RemFail Instr (ToTs inp) (ToTs out) -> inp :-> out
LorentzInstr (RemFail Instr (GValueType (Rep dt) : ToTs inp) (ToTs out)
 -> (dt : inp) :-> out)
-> (Rec (CaseClauseL inp out) (CaseClauses dt)
    -> RemFail Instr (GValueType (Rep dt) : ToTs inp) (ToTs out))
-> Rec (CaseClauseL inp out) (CaseClauses dt)
-> (dt : inp) :-> out
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (out :: [T]) (inp :: [T]).
InstrCaseC dt =>
Rec (CaseClause inp out) (CaseClauses dt)
-> RemFail Instr (ToT dt : inp) out
forall dt (out :: [T]) (inp :: [T]).
InstrCaseC dt =>
Rec (CaseClause inp out) (CaseClauses dt)
-> RemFail Instr (ToT dt : inp) out
instrCase @dt (Rec (CaseClause (ToTs inp) (ToTs out)) (CaseClauses dt)
 -> RemFail Instr (GValueType (Rep dt) : ToTs inp) (ToTs out))
-> (Rec (CaseClauseL inp out) (CaseClauses dt)
    -> Rec (CaseClause (ToTs inp) (ToTs out)) (CaseClauses dt))
-> Rec (CaseClauseL inp out) (CaseClauses dt)
-> RemFail Instr (GValueType (Rep dt) : ToTs inp) (ToTs out)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (x :: CaseClauseParam).
 CaseClauseL inp out x -> CaseClause (ToTs inp) (ToTs out) x)
-> Rec (CaseClauseL inp out) (CaseClauses dt)
-> Rec (CaseClause (ToTs inp) (ToTs out)) (CaseClauses dt)
forall u (rs :: [u]) (f :: u -> *) (g :: u -> *).
RMap rs =>
(forall (x :: u). f x -> g x) -> Rec f rs -> Rec g rs
rmap forall (x :: CaseClauseParam).
CaseClauseL inp out x -> CaseClause (ToTs inp) (ToTs out) x
coerceCaseClause
  where
    coerceCaseClause
      :: forall clauses.
         CaseClauseL inp out clauses -> CaseClause (ToTs inp) (ToTs out) clauses
    coerceCaseClause :: CaseClauseL inp out clauses
-> CaseClause (ToTs inp) (ToTs out) clauses
coerceCaseClause (CaseClauseL (LorentzInstr RemFail Instr (ToTs (AppendCtorField x inp)) (ToTs out)
cc)) =
      RemFail Instr (AppendCtorField x (ToTs inp)) (ToTs out)
-> CaseClause (ToTs inp) (ToTs out) ('CaseClauseParam ctor x)
forall (x :: CtorField) (inp :: [T]) (out :: [T]) (ctor :: Symbol).
RemFail Instr (AppendCtorField x inp) out
-> CaseClause inp out ('CaseClauseParam ctor x)
CaseClause (RemFail Instr (AppendCtorField x (ToTs inp)) (ToTs out)
 -> CaseClause (ToTs inp) (ToTs out) ('CaseClauseParam ctor x))
-> RemFail Instr (AppendCtorField x (ToTs inp)) (ToTs out)
-> CaseClause (ToTs inp) (ToTs out) ('CaseClauseParam ctor x)
forall a b. (a -> b) -> a -> b
$ case Proxy clauses
forall k (t :: k). Proxy t
Proxy @clauses of
        (_ :: Proxy ('CaseClauseParam ctor cc)) ->
          case (AppendCtorFieldAxiom ('OneField Word) '[Int],
 AppendCtorFieldAxiom 'NoFields '[Int]) =>
Dict (AppendCtorFieldAxiom x inp)
forall (cf :: CtorField) (st :: [*]).
(AppendCtorFieldAxiom ('OneField Word) '[Int],
 AppendCtorFieldAxiom 'NoFields '[Int]) =>
Dict (AppendCtorFieldAxiom cf st)
appendCtorFieldAxiom @cc @inp of Dict (AppendCtorFieldAxiom x inp)
Dict -> RemFail Instr (AppendCtorField x (ToTs inp)) (ToTs out)
RemFail Instr (ToTs (AppendCtorField x inp)) (ToTs out)
cc

-- | Like 'case_', accepts a tuple of clauses, which may be more convenient.
--
-- If user is experiencing problems with wierd errors about tuples while using
-- this function, he should take look at "Morley.Util.TypeTuple.Instances" and ensure
-- that his tuple isn't bigger than generated instances, if so, he should probably
-- extend number of generated instances.
caseT
  :: forall dt out inp clauses.
     CaseTC dt out inp clauses
  => IsoRecTuple clauses -> dt : inp :-> out
caseT :: IsoRecTuple clauses -> (dt : inp) :-> out
caseT = forall (out :: [*]) (inp :: [*]).
(InstrCaseC dt, RMap (GCaseClauses (Rep dt))) =>
Rec (CaseClauseL inp out) (GCaseClauses (Rep dt))
-> (dt : inp) :-> out
forall dt (out :: [*]) (inp :: [*]).
(InstrCaseC dt, RMap (CaseClauses dt)) =>
Rec (CaseClauseL inp out) (CaseClauses dt) -> (dt : inp) :-> out
case_ @dt (Rec (CaseClauseL inp out) (GCaseClauses (Rep dt))
 -> (dt : inp) :-> out)
-> (IsoRecTuple (Rec (CaseClauseL inp out) (GCaseClauses (Rep dt)))
    -> Rec (CaseClauseL inp out) (GCaseClauses (Rep dt)))
-> IsoRecTuple (Rec (CaseClauseL inp out) (GCaseClauses (Rep dt)))
-> (dt : inp) :-> out
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IsoRecTuple (Rec (CaseClauseL inp out) (GCaseClauses (Rep dt)))
-> Rec (CaseClauseL inp out) (GCaseClauses (Rep dt))
forall r. RecFromTuple r => IsoRecTuple r -> r
recFromTuple

type CaseTC dt out inp clauses =
  ( InstrCaseC dt
  , RMap (CaseClauses dt)
  , RecFromTuple clauses
  , clauses ~ Rec (CaseClauseL inp out) (CaseClauses dt)
  )

-- | Unwrap a constructor with the given name. Useful for sum types.
unsafeUnwrap_
  :: forall dt name st.
     InstrUnwrapC dt name
  => Label name -> dt : st :-> (CtorOnlyField name dt ': st)
unsafeUnwrap_ :: Label name -> (dt : st) :-> (CtorOnlyField name dt : st)
unsafeUnwrap_ =
  case (AppendCtorFieldAxiom ('OneField Word) '[Int],
 AppendCtorFieldAxiom 'NoFields '[Int]) =>
Dict (AppendCtorFieldAxiom (GetCtorField dt name) st)
forall (cf :: CtorField) (st :: [*]).
(AppendCtorFieldAxiom ('OneField Word) '[Int],
 AppendCtorFieldAxiom 'NoFields '[Int]) =>
Dict (AppendCtorFieldAxiom cf st)
appendCtorFieldAxiom @(GetCtorField dt name) @st of
    Dict (AppendCtorFieldAxiom (GetCtorField dt name) st)
Dict -> Instr
  (GValueType (Rep dt) : ToTs st)
  (ToT (CtorOnlyField name dt) : ToTs st)
-> (dt : st) :-> (CtorOnlyField name dt : st)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I (Instr
   (GValueType (Rep dt) : ToTs st)
   (ToT (CtorOnlyField name dt) : ToTs st)
 -> (dt : st) :-> (CtorOnlyField name dt : st))
-> (Label name
    -> Instr
         (GValueType (Rep dt) : ToTs st)
         (ToT (CtorOnlyField name dt) : ToTs st))
-> Label name
-> (dt : st) :-> (CtorOnlyField name dt : st)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall dt (name :: Symbol) (st :: [T]).
InstrUnwrapC dt name =>
Label name
-> Instr (ToT dt : st) (ToT (CtorOnlyField name dt) : st)
forall (name :: Symbol) (st :: [T]).
InstrUnwrapC dt name =>
Label name
-> Instr (ToT dt : st) (ToT (CtorOnlyField name dt) : st)
unsafeInstrUnwrap @dt