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

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

module Lorentz.ADT
  ( HasField
  , HasFieldOfType
  , HasFieldsOfType
  , NamedField (..)
  , (:=)
  , HasDupableGetters
  , 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 (..)
  , (:!)
  , (:?)

    -- * Advanced methods
  , getFieldOpen
  , setFieldOpen
  ) 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.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)

-- | This marker typeclass is a requirement for the 'getField'
-- (where it is imposed on the /datatype/), and it is supposed to be satisfied
-- in two cases:
--
-- 1. The entire datatype is 'Dupable';
-- 2. When the datatype has non-dupable fields, they are located so that
-- 'getField' remains efficient.
--
-- The problem we are trying to solve here: without special care, 'getField'
-- may become multiple times more costly, see 'instrGetField' for the
-- explanation.
-- And this typeclass imposes an invariant: if we ever use 'getField' on a
-- datatype, then we have to pay attention to the datatype's Michelson
-- representation and ensure 'getField' remains optimal.
--
-- When you are developing a contract:
-- "Lorentz.Layouts.NonDupable" module contains utilities to help you
-- provide the necessary Michelson layout. In case you want to use your
-- custom layout but still allow 'getField' for it, you can define an instance
-- for your type manually as an assurance that Michelson layout is optimal enough
-- to use 'getField' on this type.
--
-- When you are developing a library:
-- Note that 'HasDupableGetters' resolves to 'Dupable' by default, and when
-- propagating this constraint you can switch to 'Dupable' anytime but this
-- will also make your code unusable in the presence of 'Ticket's and other
-- non-dupable types.
class HasDupableGetters a
instance {-# OVERLAPPABLE #-} Dupable a => HasDupableGetters a

-- | 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 :: forall dt (name :: Symbol) (st :: [*]).
InstrGetFieldC dt name =>
Label name -> (dt : st) :-> (GetFieldType dt name : st)
toField = Instr
  (GValueType (Rep dt) : ToTs st)
  (ToT
     (LnrFieldType
        (LNRequireFound name dt (GLookupNamed name (Rep dt))))
     : ToTs st)
-> (dt : st)
   :-> (LnrFieldType
          (LNRequireFound name dt (GLookupNamed name (Rep dt)))
          : st)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I (Instr
   (GValueType (Rep dt) : ToTs st)
   (ToT
      (LnrFieldType
         (LNRequireFound name dt (GLookupNamed name (Rep dt))))
      : ToTs st)
 -> (dt : st)
    :-> (LnrFieldType
           (LNRequireFound name dt (GLookupNamed name (Rep dt)))
           : st))
-> (Label name
    -> Instr
         (GValueType (Rep dt) : ToTs st)
         (ToT
            (LnrFieldType
               (LNRequireFound name dt (GLookupNamed name (Rep dt))))
            : ToTs st))
-> Label name
-> (dt : st)
   :-> (LnrFieldType
          (LNRequireFound name dt (GLookupNamed name (Rep dt)))
          : 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)
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 :: forall dt (name :: Symbol) (st :: [*]).
InstrGetFieldC dt name =>
Label name -> (dt : st) :-> ((name :! GetFieldType dt name) : st)
toFieldNamed Label name
l = Label name
-> (dt : st)
   :-> (LnrFieldType
          (LNRequireFound name dt (GLookupNamed name (Rep dt)))
          : st)
forall dt (name :: Symbol) (st :: [*]).
InstrGetFieldC dt name =>
Label name -> (dt : st) :-> (GetFieldType dt name : st)
toField Label name
l ((dt : st)
 :-> (LnrFieldType
        (LNRequireFound name dt (GLookupNamed name (Rep dt)))
        : st))
-> ((LnrFieldType
       (LNRequireFound name dt (GLookupNamed name (Rep dt)))
       : st)
    :-> (NamedF
           Identity
           (LnrFieldType
              (LNRequireFound name dt (GLookupNamed name (Rep dt))))
           name
           : st))
-> (dt : st)
   :-> (NamedF
          Identity
          (LnrFieldType
             (LNRequireFound name dt (GLookupNamed name (Rep dt))))
          name
          : st)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# Label name
-> (LnrFieldType
      (LNRequireFound name dt (GLookupNamed name (Rep dt)))
      : st)
   :-> (NamedF
          Identity
          (LnrFieldType
             (LNRequireFound name dt (GLookupNamed name (Rep 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.
getField
  :: forall dt name st.
     (InstrGetFieldC dt name, Dupable (GetFieldType dt name), HasDupableGetters dt)
  => Label name -> dt : st :-> GetFieldType dt name : dt ': st
getField :: forall dt (name :: Symbol) (st :: [*]).
(InstrGetFieldC dt name, Dupable (GetFieldType dt name),
 HasDupableGetters dt) =>
Label name -> (dt : st) :-> (GetFieldType dt name : dt : st)
getField = Instr
  (GValueType (Rep dt) : ToTs st)
  (ToT (GetFieldType dt name) : GValueType (Rep dt) : ToTs st)
-> (dt : st) :-> (GetFieldType dt name : dt : st)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I (Instr
   (GValueType (Rep dt) : ToTs st)
   (ToT (GetFieldType dt name) : GValueType (Rep dt) : ToTs st)
 -> (dt : st) :-> (GetFieldType dt name : dt : st))
-> (Label name
    -> Instr
         (GValueType (Rep dt) : ToTs st)
         (ToT (GetFieldType dt name) : GValueType (Rep dt) : ToTs st))
-> Label name
-> (dt : st) :-> (GetFieldType dt name : dt : st)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall dt (name :: Symbol) (st :: [T]).
(InstrGetFieldC dt name,
 DupableScope (ToT (GetFieldType dt name))) =>
Label name
-> Instr (ToT dt : st) (ToT (GetFieldType dt name) : ToT dt : st)
instrGetField @dt
  (DupableScope (ToT (GetFieldType dt name)) =>
 Label name -> (dt : st) :-> (GetFieldType dt name : dt : st))
-> (Dupable (GetFieldType dt name)
    :- DupableScope (ToT (GetFieldType dt name)))
-> Label name
-> (dt : st) :-> (GetFieldType dt name : dt : st)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall a. Dupable a :- DupableScope (ToT a)
dupableEvi @(GetFieldType dt name)
  where
    _needHasDupableGetters :: Dict (HasDupableGetters dt)
_needHasDupableGetters = forall (a :: Constraint). a => Dict a
Dict @(HasDupableGetters dt)

-- | Like 'getField', but leaves field named.
getFieldNamed
  :: forall dt name st.
     (InstrGetFieldC dt name, Dupable (GetFieldType dt name), HasDupableGetters dt)
  => Label name -> dt : st :-> (name :! GetFieldType dt name) : dt ': st
getFieldNamed :: forall dt (name :: Symbol) (st :: [*]).
(InstrGetFieldC dt name, Dupable (GetFieldType dt name),
 HasDupableGetters dt) =>
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 (GetFieldType dt name),
 HasDupableGetters 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 :: forall dt (name :: Symbol) (st :: [*]).
InstrSetFieldC dt name =>
Label name -> (GetFieldType dt name : dt : st) :-> (dt : st)
setField = Instr
  (ToT
     (LnrFieldType
        (LNRequireFound name dt (GLookupNamed name (Rep dt))))
     : GValueType (Rep dt) : ToTs st)
  (GValueType (Rep dt) : ToTs st)
-> (LnrFieldType
      (LNRequireFound name dt (GLookupNamed name (Rep dt)))
      : dt : st)
   :-> (dt : st)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I (Instr
   (ToT
      (LnrFieldType
         (LNRequireFound name dt (GLookupNamed name (Rep dt))))
      : GValueType (Rep dt) : ToTs st)
   (GValueType (Rep dt) : ToTs st)
 -> (LnrFieldType
       (LNRequireFound name dt (GLookupNamed name (Rep dt)))
       : dt : st)
    :-> (dt : st))
-> (Label name
    -> Instr
         (ToT
            (LnrFieldType
               (LNRequireFound name dt (GLookupNamed name (Rep dt))))
            : GValueType (Rep dt) : ToTs st)
         (GValueType (Rep dt) : ToTs st))
-> Label name
-> (LnrFieldType
      (LNRequireFound name dt (GLookupNamed name (Rep dt)))
      : 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)
instrSetField @dt

-- | Apply given modifier to a datatype field.
modifyField
  :: forall dt name st.
     ( InstrGetFieldC dt name
     , InstrSetFieldC dt name
     , Dupable (GetFieldType dt name)
     , HasDupableGetters dt
     )
  => Label name
  -> (forall st0. (GetFieldType dt name ': st0) :-> (GetFieldType dt name ': st0))
  -> dt : st :-> dt : st
modifyField :: forall dt (name :: Symbol) (st :: [*]).
(InstrGetFieldC dt name, InstrSetFieldC dt name,
 Dupable (GetFieldType dt name), HasDupableGetters dt) =>
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 = forall dt (name :: Symbol) (st :: [*]).
(InstrGetFieldC dt name, Dupable (GetFieldType dt name),
 HasDupableGetters 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
# forall dt (name :: Symbol) (st :: [*]).
InstrSetFieldC dt name =>
Label name -> (GetFieldType dt name : dt : st) :-> (dt : st)
setField @dt Label name
l

-- | \"Open\" version of 'getField', an advanced method suitable for chaining
-- getters.
--
-- It accepts two continuations accepting the extracted field, one that
-- leaves the field on stack (and does a duplication of @res@ inside)
-- and another one that consumes the field. Normally these are just @getField@
-- and @toField@ for some nested field.
--
-- Unlike the straightforward chaining of 'getField'/'toField' methods,
-- @getFieldOpen@ does not require the immediate field to be dupable; rather,
-- in the best case only @res@ has to be dupable.
getFieldOpen
  :: forall dt name res st.
     (InstrGetFieldC dt name, HasDupableGetters dt)
  => '[GetFieldType dt name] :-> '[res, GetFieldType dt name]
  -> '[GetFieldType dt name] :-> '[res]
  -> Label name
  -> dt : st :-> res : dt ': st
getFieldOpen :: forall dt (name :: Symbol) res (st :: [*]).
(InstrGetFieldC dt name, HasDupableGetters dt) =>
('[GetFieldType dt name] :-> '[res, GetFieldType dt name])
-> ('[GetFieldType dt name] :-> '[res])
-> Label name
-> (dt : st) :-> (res : dt : st)
getFieldOpen '[LnrFieldType
    (LNRequireFound name dt (GLookupNamed name (Rep dt)))]
:-> '[res,
      LnrFieldType (LNRequireFound name dt (GLookupNamed name (Rep dt)))]
contWDup '[LnrFieldType
    (LNRequireFound name dt (GLookupNamed name (Rep dt)))]
:-> '[res]
contWoDup =
  Instr
  (GValueType (Rep dt) : ToTs st)
  (ToT res : GValueType (Rep dt) : ToTs st)
-> (dt : st) :-> (res : dt : st)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I (Instr
   (GValueType (Rep dt) : ToTs st)
   (ToT res : GValueType (Rep dt) : ToTs st)
 -> (dt : st) :-> (res : dt : st))
-> (Label name
    -> Instr
         (GValueType (Rep dt) : ToTs st)
         (ToT res : GValueType (Rep dt) : ToTs st))
-> Label name
-> (dt : st) :-> (res : dt : st)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall dt (name :: Symbol) (res :: T) (st :: [T]).
InstrGetFieldC dt name =>
Instr
  '[ToT (GetFieldType dt name)] '[res, ToT (GetFieldType dt name)]
-> Instr '[ToT (GetFieldType dt name)] '[res]
-> Label name
-> Instr (ToT dt : st) (res : ToT dt : st)
instrGetFieldOpen @dt (('[LnrFieldType
     (LNRequireFound name dt (GLookupNamed name (Rep dt)))]
 :-> '[res,
       LnrFieldType
         (LNRequireFound name dt (GLookupNamed name (Rep dt)))])
-> Instr
     (ToTs
        '[LnrFieldType
            (LNRequireFound name dt (GLookupNamed name (Rep dt)))])
     (ToTs
        '[res,
          LnrFieldType
            (LNRequireFound name dt (GLookupNamed name (Rep dt)))])
forall (inp :: [*]) (out :: [*]).
HasCallStack =>
(inp :-> out) -> Instr (ToTs inp) (ToTs out)
iNonFailingCode '[LnrFieldType
    (LNRequireFound name dt (GLookupNamed name (Rep dt)))]
:-> '[res,
      LnrFieldType (LNRequireFound name dt (GLookupNamed name (Rep dt)))]
contWDup) (('[LnrFieldType
     (LNRequireFound name dt (GLookupNamed name (Rep dt)))]
 :-> '[res])
-> Instr
     (ToTs
        '[LnrFieldType
            (LNRequireFound name dt (GLookupNamed name (Rep dt)))])
     (ToTs '[res])
forall (inp :: [*]) (out :: [*]).
HasCallStack =>
(inp :-> out) -> Instr (ToTs inp) (ToTs out)
iNonFailingCode '[LnrFieldType
    (LNRequireFound name dt (GLookupNamed name (Rep dt)))]
:-> '[res]
contWoDup)
  where
    _needHasDupableGetters :: Dict (HasDupableGetters dt)
_needHasDupableGetters = forall (a :: Constraint). a => Dict a
Dict @(HasDupableGetters dt)

-- | \"Open\" version of 'setField', an advanced method suitable for chaining
-- setters.
--
-- It accepts a continuation accepting the field extracted for the update and
-- the new value that is being set. Normally this continuation is just @setField@
-- for some nested field.
setFieldOpen
  :: forall dt name new st.
     InstrSetFieldC dt name
  => '[new, GetFieldType dt name] :-> '[GetFieldType dt name]
  -> Label name
  -> (new ': dt ': st) :-> (dt ': st)
setFieldOpen :: forall dt (name :: Symbol) new (st :: [*]).
InstrSetFieldC dt name =>
('[new, GetFieldType dt name] :-> '[GetFieldType dt name])
-> Label name -> (new : dt : st) :-> (dt : st)
setFieldOpen '[new,
  LnrFieldType (LNRequireFound name dt (GLookupNamed name (Rep dt)))]
:-> '[LnrFieldType
        (LNRequireFound name dt (GLookupNamed name (Rep dt)))]
cont =
  Instr
  (ToT new : GValueType (Rep dt) : ToTs st)
  (GValueType (Rep dt) : ToTs st)
-> (new : dt : st) :-> (dt : st)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I (Instr
   (ToT new : GValueType (Rep dt) : ToTs st)
   (GValueType (Rep dt) : ToTs st)
 -> (new : dt : st) :-> (dt : st))
-> (Label name
    -> Instr
         (ToT new : GValueType (Rep dt) : ToTs st)
         (GValueType (Rep dt) : ToTs st))
-> Label name
-> (new : dt : st) :-> (dt : st)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall dt (name :: Symbol) (new :: T) (st :: [T]).
InstrSetFieldC dt name =>
Instr
  '[new, ToT (GetFieldType dt name)] '[ToT (GetFieldType dt name)]
-> Label name -> Instr (new : ToT dt : st) (ToT dt : st)
instrSetFieldOpen @dt (('[new,
   LnrFieldType (LNRequireFound name dt (GLookupNamed name (Rep dt)))]
 :-> '[LnrFieldType
         (LNRequireFound name dt (GLookupNamed name (Rep dt)))])
-> Instr
     (ToTs
        '[new,
          LnrFieldType
            (LNRequireFound name dt (GLookupNamed name (Rep dt)))])
     (ToTs
        '[LnrFieldType
            (LNRequireFound name dt (GLookupNamed name (Rep dt)))])
forall (inp :: [*]) (out :: [*]).
HasCallStack =>
(inp :-> out) -> Instr (ToTs inp) (ToTs out)
iNonFailingCode '[new,
  LnrFieldType (LNRequireFound name dt (GLookupNamed name (Rep dt)))]
:-> '[LnrFieldType
        (LNRequireFound name dt (GLookupNamed name (Rep dt)))]
cont)

-- | 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 :: forall dt (st :: [*]).
(InstrConstructC dt, RMap (ConstructorFieldTypes dt)) =>
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 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 Instr (ToTs' st) (ToT x : ToTs' st)
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 :: forall dt fctors (st :: [*]).
(InstrConstructC dt, RMap (ConstructorFieldTypes dt),
 fctors ~ Rec (FieldConstructor st) (ConstructorFieldTypes dt),
 RecFromTuple fctors) =>
IsoRecTuple fctors -> st :-> (dt : st)
constructT = Rec (FieldConstructor st) (ConstructorFieldTypes dt)
-> st :-> (dt : st)
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))
-> (IsoRecTuple
      (Rec (FieldConstructor st) (ConstructorFieldTypes dt))
    -> Rec (FieldConstructor st) (ConstructorFieldTypes dt))
-> IsoRecTuple
     (Rec (FieldConstructor st) (ConstructorFieldTypes dt))
-> st :-> (dt : st)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IsoRecTuple (Rec (FieldConstructor st) (ConstructorFieldTypes dt))
-> Rec (FieldConstructor st) (ConstructorFieldTypes 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 :: forall dt (fields :: [*]) (st :: [*]).
(InstrConstructC dt, fields ~ ConstructorFieldTypes dt,
 KnownList fields) =>
(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 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
\\ 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
\\ 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 :: forall dt (fields :: [*]) (st :: [*]).
(InstrDeconstructC dt, KnownList fields,
 fields ~ ConstructorFieldTypes dt) =>
(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 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
\\ 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
\\ 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 :: forall (st :: [*]) f.
HasCallStack =>
(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_ :: forall dt (name :: Symbol) (st :: [*]).
InstrWrapC dt name =>
Label name
-> AppendCtorField (GetCtorField dt name) st :-> (dt : st)
wrap_ =
  case forall (cf :: CtorField) (st :: [*]).
(AppendCtorFieldAxiom ('OneField Word) '[Int],
 AppendCtorFieldAxiom 'NoFields '[Int]) =>
Dict (AppendCtorFieldAxiom cf st)
appendCtorFieldAxiom @(GetCtorField dt name) @st of
    Dict
  (AppendCtorFieldAxiom
     (LnrFieldType
        (LNRequireFound name dt (GLookupNamed name (Rep dt))))
     st)
Dict -> Instr
  (ToTs
     (AppendCtorField
        (LnrFieldType
           (LNRequireFound name dt (GLookupNamed name (Rep dt))))
        st))
  (GValueType (Rep dt) : ToTs st)
-> AppendCtorField
     (LnrFieldType
        (LNRequireFound name dt (GLookupNamed name (Rep dt))))
     st
   :-> (dt : st)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I (Instr
   (ToTs
      (AppendCtorField
         (LnrFieldType
            (LNRequireFound name dt (GLookupNamed name (Rep dt))))
         st))
   (GValueType (Rep dt) : ToTs st)
 -> AppendCtorField
      (LnrFieldType
         (LNRequireFound name dt (GLookupNamed name (Rep dt))))
      st
    :-> (dt : st))
-> (Label name
    -> Instr
         (ToTs
            (AppendCtorField
               (LnrFieldType
                  (LNRequireFound name dt (GLookupNamed name (Rep dt))))
               st))
         (GValueType (Rep dt) : ToTs st))
-> Label name
-> AppendCtorField
     (LnrFieldType
        (LNRequireFound name dt (GLookupNamed name (Rep dt))))
     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)
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 :: forall dt (name :: Symbol) (st :: [*]).
InstrWrapOneC dt name =>
Label name -> (CtorOnlyField name dt : st) :-> (dt : st)
wrapOne = case 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)
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_ :: forall dt (out :: [*]) (inp :: [*]).
(InstrCaseC dt, RMap (CaseClauses dt)) =>
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 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 :: forall (x :: CaseClauseParam).
CaseClauseL inp out x -> CaseClause (ToTs inp) (ToTs out) x
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 forall {k} (t :: k). Proxy t
forall {t :: CaseClauseParam}. Proxy t
Proxy @clauses of
        (Proxy ('CaseClauseParam ctor x)
_ :: Proxy ('CaseClauseParam ctor cc)) ->
          case 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 :: forall dt (out :: [*]) (inp :: [*]) clauses.
CaseTC dt out inp clauses =>
IsoRecTuple clauses -> (dt : inp) :-> out
caseT = forall dt (out :: [*]) (inp :: [*]).
(InstrCaseC dt, RMap (CaseClauses dt)) =>
Rec (CaseClauseL inp out) (CaseClauses dt) -> (dt : inp) :-> out
case_ @dt (Rec (CaseClauseL inp out) (CaseClauses dt) -> (dt : inp) :-> out)
-> (IsoRecTuple (Rec (CaseClauseL inp out) (CaseClauses dt))
    -> Rec (CaseClauseL inp out) (CaseClauses dt))
-> IsoRecTuple (Rec (CaseClauseL inp out) (CaseClauses dt))
-> (dt : inp) :-> out
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IsoRecTuple (Rec (CaseClauseL inp out) (CaseClauses dt))
-> Rec (CaseClauseL inp out) (CaseClauses 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_ :: forall dt (name :: Symbol) (st :: [*]).
InstrUnwrapC dt name =>
Label name -> (dt : st) :-> (CtorOnlyField name dt : st)
unsafeUnwrap_ =
  case forall (cf :: CtorField) (st :: [*]).
(AppendCtorFieldAxiom ('OneField Word) '[Int],
 AppendCtorFieldAxiom 'NoFields '[Int]) =>
Dict (AppendCtorFieldAxiom cf st)
appendCtorFieldAxiom @(GetCtorField dt name) @st of
    Dict
  (AppendCtorFieldAxiom
     (LnrFieldType
        (LNRequireFound name dt (GLookupNamed name (Rep dt))))
     st)
Dict -> Instr
  (GValueType (Rep dt) : ToTs st)
  (ToT
     (RequireOneField
        name
        (LnrFieldType
           (LNRequireFound name dt (GLookupNamed name (Rep dt)))))
     : ToTs st)
-> (dt : st)
   :-> (RequireOneField
          name
          (LnrFieldType
             (LNRequireFound name dt (GLookupNamed name (Rep dt))))
          : st)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I (Instr
   (GValueType (Rep dt) : ToTs st)
   (ToT
      (RequireOneField
         name
         (LnrFieldType
            (LNRequireFound name dt (GLookupNamed name (Rep dt)))))
      : ToTs st)
 -> (dt : st)
    :-> (RequireOneField
           name
           (LnrFieldType
              (LNRequireFound name dt (GLookupNamed name (Rep dt))))
           : st))
-> (Label name
    -> Instr
         (GValueType (Rep dt) : ToTs st)
         (ToT
            (RequireOneField
               name
               (LnrFieldType
                  (LNRequireFound name dt (GLookupNamed name (Rep dt)))))
            : ToTs st))
-> Label name
-> (dt : st)
   :-> (RequireOneField
          name
          (LnrFieldType
             (LNRequireFound name dt (GLookupNamed name (Rep 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)
unsafeInstrUnwrap @dt