{-# OPTIONS_HADDOCK hide #-}

{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE UndecidableInstances #-}

-- | 

module Cubix.Language.Solidity.IPS.Types where

import Data.List ( (\\) )

import Language.Haskell.TH ( mkName )

import Data.Comp.Multi ( Term,  project', CxtS, AnnCxtS )
import Data.Comp.Trans ( runCompTrans, makeSumType )

import Cubix.Language.Solidity.Modularized.Names
import Cubix.Language.Solidity.Modularized.Types as Solidity
import Cubix.Language.Info
import Cubix.Language.Parametric.Derive
import Cubix.Language.Parametric.InjF
import Cubix.Language.Parametric.Syntax qualified as P

-----------------------------------------------------------------------------------
---------------       Variable declarations and blocks     ------------------------
-----------------------------------------------------------------------------------

data LValue e l where
  IndexLValue        :: e P.ExpressionL -> e P.ExpressionL              -> LValue e P.LhsL
  IdentifierLValue   :: e P.IdentL                                      -> LValue e P.LhsL
  MemberAccessLValue :: e P.ExpressionL -> e Solidity.MemberAccessTypeL -> LValue e P.LhsL
  TupleLValue        :: e [Maybe P.ExpressionL]                         -> LValue e P.LhsL

deriveAll [''LValue]

-----------------------------------------------------------------------------------
---------------------     Identifiers and assignments      ------------------------
-----------------------------------------------------------------------------------

createSortInclusionTypes
  [''P.IdentL,    ''P.AssignL,     ''P.ExpressionL ]
  [''IdentifierL, ''P.ExpressionL, ''P.RhsL        ]
deriveAllButSortInjection
  [ ''IdentIsIdentifier, ''AssignIsExpression, ''ExpressionIsRhs ]
createSortInclusionInfers
  [''P.IdentL,    ''P.AssignL,     ''P.ExpressionL ]
  [''IdentifierL, ''P.ExpressionL, ''P.RhsL        ]

-----------------------------------------------------------------------------------
---------------               Expressions                  ------------------------
-----------------------------------------------------------------------------------

createSortInclusionType' ''P.ExpressionL ''ExpressionL (mkName "ExpressionIsSolExp")
createSortInclusionType' ''ExpressionL ''P.ExpressionL (mkName "SolExpIsExpression")
deriveAllButSortInjection [''ExpressionIsSolExp]
deriveAllButSortInjection [''SolExpIsExpression]
createSortInclusionInfer' ''P.ExpressionL ''ExpressionL (mkName "ExpressionIsSolExp")
createSortInclusionInfer' ''ExpressionL ''P.ExpressionL (mkName "SolExpIsExpression")

-----------------------------------------------------------------------------------
----------------------         Declaring the IPS           ------------------------
-----------------------------------------------------------------------------------

do let soliditySortInjections =
         [ ''IdentIsIdentifier
         , ''AssignIsExpression
         , ''ExpressionIsRhs
         , ''ExpressionIsSolExp, ''SolExpIsExpression
         ]
       solidityNewNodes = [ ''LValue ]
       names =
         (soliditySigNames \\ [mkName "Identifier"]) ++
         soliditySortInjections ++
         solidityNewNodes ++
         [ ''P.Ident, ''P.Assign, ''P.AssignOpEquals
         , ''P.AssignOpAdd, ''P.AssignOpSub, ''P.AssignOpMul, ''P.AssignOpDiv, ''P.AssignOpMod
         , ''P.AssignOpBitAnd, ''P.AssignOpBitOr, ''P.AssignOpBitXor
         , ''P.AssignOpArithShr, ''P.AssignOpLogicShr, ''P.AssignOpShl
         , ''P.UnaryMinusOp, ''P.ComplementOp, ''P.LogicalNegationOp
         , ''P.ArithBinOp, ''P.DivOp, ''P.ModOp, ''P.ExpOp
         , ''P.BitwiseBinOp, ''P.LogicalBinOp, ''P.ShlOp, ''P.LogicalShrOp, ''P.ArithShrOp
         , ''P.RelationalBinOp
         , ''P.CondTernaryOp
         , ''P.Operator
         , ''P.SeqOp
         ]
   runCompTrans $ makeSumType "MSoliditySig" names


-- TODO 2023.11.02: I don't remember what this is for
--type instance InjectableSorts MCSig MultiLocalVarDeclL = '[CCompoundBlockItemL]

type MSolidityTerm = Term MSoliditySig
type MSolidityTermLab = TermLab MSoliditySig

type MSolidityCxt h a = CxtS h MSoliditySig a
type MSolidityCxtA h a p = AnnCxtS p h MSoliditySig a


-----------------------------------------------------------------------------------
----------------------         Sort injections             ------------------------
-----------------------------------------------------------------------------------

instance {-# OVERLAPPING #-} InjF MSoliditySig P.IdentL P.LhsL where
    injF :: forall h (a :: * -> *).
CxtS h MSoliditySig a IdentL -> CxtS h MSoliditySig a LhsL
injF = CxtS h MSoliditySig a IdentL -> CxtS h MSoliditySig a LhsL
forall h (fs :: Signature) (a :: * -> *) j.
(LValue :-<: fs, InjF fs LhsL j) =>
CxtS h fs a IdentL -> CxtS h fs a j
iIdentifierLValue

    projF' :: forall h p (a :: * -> *).
Cxt h (Sum MSoliditySig :&: p) a LhsL
-> Maybe (Cxt h (Sum MSoliditySig :&: p) a IdentL)
projF' Cxt h (Sum MSoliditySig :&: p) a LhsL
e
      | Just (IdentifierLValue Cxt h (Sum MSoliditySig :&: p) a IdentL
ident) <- Cxt h (Sum MSoliditySig :&: p) a LhsL
-> Maybe (LValue (Cxt h (Sum MSoliditySig :&: p) a) LhsL)
forall (f :: (* -> *) -> * -> *) (f' :: (* -> *) -> * -> *)
       (s :: (* -> *) -> * -> *) h (a :: * -> *) i.
(RemA f f', s :<: f') =>
Cxt h f a i -> Maybe (s (Cxt h f a) i)
project' Cxt h (Sum MSoliditySig :&: p) a LhsL
e
      = Cxt h (Sum MSoliditySig :&: p) a IdentL
-> Maybe (Cxt h (Sum MSoliditySig :&: p) a IdentL)
forall a. a -> Maybe a
Just Cxt h (Sum MSoliditySig :&: p) a IdentL
ident
    projF' Cxt h (Sum MSoliditySig :&: p) a LhsL
_ = Maybe (Cxt h (Sum MSoliditySig :&: p) a IdentL)
forall a. Maybe a
Nothing

instance {-# OVERLAPPING #-} InjF MSoliditySig P.IdentL ExpressionL where
    injF :: forall h (a :: * -> *).
CxtS h MSoliditySig a IdentL -> CxtS h MSoliditySig a ExpressionL
injF = CxtS h MSoliditySig a IdentifierL
-> CxtS h MSoliditySig a ExpressionL
forall h (fs :: Signature) (a :: * -> *) j.
(Expression :-<: fs, InjF fs ExpressionL j) =>
CxtS h fs a IdentifierL -> CxtS h fs a j
iIdentifierExpression (CxtS h MSoliditySig a IdentifierL
 -> CxtS h MSoliditySig a ExpressionL)
-> (CxtS h MSoliditySig a IdentL
    -> CxtS h MSoliditySig a IdentifierL)
-> CxtS h MSoliditySig a IdentL
-> CxtS h MSoliditySig a ExpressionL
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CxtS h MSoliditySig a IdentL -> CxtS h MSoliditySig a IdentifierL
forall (fs :: Signature) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l -> CxtS h fs a l'
forall h (a :: * -> *).
CxtS h MSoliditySig a IdentL -> CxtS h MSoliditySig a IdentifierL
injF

    projF' :: forall h p (a :: * -> *).
Cxt h (Sum MSoliditySig :&: p) a ExpressionL
-> Maybe (Cxt h (Sum MSoliditySig :&: p) a IdentL)
projF' Cxt h (Sum MSoliditySig :&: p) a ExpressionL
e
     | Just (IdentifierExpression Cxt h (Sum MSoliditySig :&: p) a IdentifierL
i) <- Cxt h (Sum MSoliditySig :&: p) a ExpressionL
-> Maybe
     (Expression (Cxt h (Sum MSoliditySig :&: p) a) ExpressionL)
forall (f :: (* -> *) -> * -> *) (f' :: (* -> *) -> * -> *)
       (s :: (* -> *) -> * -> *) h (a :: * -> *) i.
(RemA f f', s :<: f') =>
Cxt h f a i -> Maybe (s (Cxt h f a) i)
project' Cxt h (Sum MSoliditySig :&: p) a ExpressionL
e
     , Just (IdentIsIdentifier Cxt h (Sum MSoliditySig :&: p) a IdentL
j) <- Cxt h (Sum MSoliditySig :&: p) a IdentifierL
-> Maybe
     (IdentIsIdentifier (Cxt h (Sum MSoliditySig :&: p) a) IdentifierL)
forall (f :: (* -> *) -> * -> *) (f' :: (* -> *) -> * -> *)
       (s :: (* -> *) -> * -> *) h (a :: * -> *) i.
(RemA f f', s :<: f') =>
Cxt h f a i -> Maybe (s (Cxt h f a) i)
project' Cxt h (Sum MSoliditySig :&: p) a IdentifierL
i
     = Cxt h (Sum MSoliditySig :&: p) a IdentL
-> Maybe (Cxt h (Sum MSoliditySig :&: p) a IdentL)
forall a. a -> Maybe a
Just Cxt h (Sum MSoliditySig :&: p) a IdentL
j
    projF' Cxt h (Sum MSoliditySig :&: p) a ExpressionL
_ = Maybe (Cxt h (Sum MSoliditySig :&: p) a IdentL)
forall a. Maybe a
Nothing

instance {-# OVERLAPPING #-} InjF MSoliditySig P.IdentL P.ExpressionL where
    injF :: forall h (a :: * -> *).
CxtS h MSoliditySig a IdentL -> CxtS h MSoliditySig a ExpressionL
injF = Cxt h (Sum MSoliditySig) a ExpressionL
-> Cxt h (Sum MSoliditySig) a ExpressionL
forall {k} h (f :: (* -> *) -> * -> *) (a :: * -> *) (j :: k).
(SolExpIsExpression :<: f) =>
Cxt h f a ExpressionL -> Cxt h f a ExpressionL
SolExpIsExpression' (Cxt h (Sum MSoliditySig) a ExpressionL
 -> Cxt h (Sum MSoliditySig) a ExpressionL)
-> (CxtS h MSoliditySig a IdentL
    -> Cxt h (Sum MSoliditySig) a ExpressionL)
-> CxtS h MSoliditySig a IdentL
-> Cxt h (Sum MSoliditySig) a ExpressionL
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CxtS h MSoliditySig a IdentL
-> Cxt h (Sum MSoliditySig) a ExpressionL
forall (fs :: Signature) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l -> CxtS h fs a l'
forall h (a :: * -> *).
CxtS h MSoliditySig a IdentL -> CxtS h MSoliditySig a ExpressionL
injF

    projF' :: forall h p (a :: * -> *).
Cxt h (Sum MSoliditySig :&: p) a ExpressionL
-> Maybe (Cxt h (Sum MSoliditySig :&: p) a IdentL)
projF' Cxt h (Sum MSoliditySig :&: p) a ExpressionL
e
      | Just (SolExpIsExpression Cxt h (Sum MSoliditySig :&: p) a ExpressionL
exp) <- Cxt h (Sum MSoliditySig :&: p) a ExpressionL
-> Maybe
     (SolExpIsExpression (Cxt h (Sum MSoliditySig :&: p) a) ExpressionL)
forall (f :: (* -> *) -> * -> *) (f' :: (* -> *) -> * -> *)
       (s :: (* -> *) -> * -> *) h (a :: * -> *) i.
(RemA f f', s :<: f') =>
Cxt h f a i -> Maybe (s (Cxt h f a) i)
project' Cxt h (Sum MSoliditySig :&: p) a ExpressionL
e
      = Cxt h (Sum MSoliditySig :&: p) a ExpressionL
-> Maybe (Cxt h (Sum MSoliditySig :&: p) a IdentL)
forall (fs :: Signature) l l' h p (a :: * -> *).
InjF fs l l' =>
Cxt h (Sum fs :&: p) a l' -> Maybe (Cxt h (Sum fs :&: p) a l)
forall h p (a :: * -> *).
Cxt h (Sum MSoliditySig :&: p) a ExpressionL
-> Maybe (Cxt h (Sum MSoliditySig :&: p) a IdentL)
projF' Cxt h (Sum MSoliditySig :&: p) a ExpressionL
exp
    projF' Cxt h (Sum MSoliditySig :&: p) a ExpressionL
_ = Maybe (Cxt h (Sum MSoliditySig :&: p) a IdentL)
forall a. Maybe a
Nothing

instance InjF MSoliditySig P.AssignL ExpressionL where
  injF :: forall h (a :: * -> *).
CxtS h MSoliditySig a AssignL -> CxtS h MSoliditySig a ExpressionL
injF = Cxt h (Sum MSoliditySig) a ExpressionL
-> Cxt h (Sum MSoliditySig) a ExpressionL
forall {k} h (f :: (* -> *) -> * -> *) (a :: * -> *) (j :: k).
(ExpressionIsSolExp :<: f) =>
Cxt h f a ExpressionL -> Cxt h f a ExpressionL
ExpressionIsSolExp' (Cxt h (Sum MSoliditySig) a ExpressionL
 -> Cxt h (Sum MSoliditySig) a ExpressionL)
-> (CxtS h MSoliditySig a AssignL
    -> Cxt h (Sum MSoliditySig) a ExpressionL)
-> CxtS h MSoliditySig a AssignL
-> Cxt h (Sum MSoliditySig) a ExpressionL
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CxtS h MSoliditySig a AssignL
-> Cxt h (Sum MSoliditySig) a ExpressionL
forall (fs :: Signature) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l -> CxtS h fs a l'
forall h (a :: * -> *).
CxtS h MSoliditySig a AssignL -> CxtS h MSoliditySig a ExpressionL
injF

  projF' :: forall h p (a :: * -> *).
Cxt h (Sum MSoliditySig :&: p) a ExpressionL
-> Maybe (Cxt h (Sum MSoliditySig :&: p) a AssignL)
projF' Cxt h (Sum MSoliditySig :&: p) a ExpressionL
e
    | Just (ExpressionIsSolExp Cxt h (Sum MSoliditySig :&: p) a ExpressionL
exp) <- Cxt h (Sum MSoliditySig :&: p) a ExpressionL
-> Maybe
     (ExpressionIsSolExp (Cxt h (Sum MSoliditySig :&: p) a) ExpressionL)
forall (f :: (* -> *) -> * -> *) (f' :: (* -> *) -> * -> *)
       (s :: (* -> *) -> * -> *) h (a :: * -> *) i.
(RemA f f', s :<: f') =>
Cxt h f a i -> Maybe (s (Cxt h f a) i)
project' Cxt h (Sum MSoliditySig :&: p) a ExpressionL
e
    = Cxt h (Sum MSoliditySig :&: p) a ExpressionL
-> Maybe (Cxt h (Sum MSoliditySig :&: p) a AssignL)
forall (fs :: Signature) l l' h p (a :: * -> *).
InjF fs l l' =>
Cxt h (Sum fs :&: p) a l' -> Maybe (Cxt h (Sum fs :&: p) a l)
forall h p (a :: * -> *).
Cxt h (Sum MSoliditySig :&: p) a ExpressionL
-> Maybe (Cxt h (Sum MSoliditySig :&: p) a AssignL)
projF' Cxt h (Sum MSoliditySig :&: p) a ExpressionL
exp
  projF' Cxt h (Sum MSoliditySig :&: p) a ExpressionL
_ = Maybe (Cxt h (Sum MSoliditySig :&: p) a AssignL)
forall a. Maybe a
Nothing

instance InjF MSoliditySig ExpressionL P.RhsL where
  injF :: forall h (a :: * -> *).
CxtS h MSoliditySig a ExpressionL -> CxtS h MSoliditySig a RhsL
injF = CxtS h MSoliditySig a ExpressionL -> CxtS h MSoliditySig a RhsL
forall (fs :: Signature) l l' h (a :: * -> *).
InjF fs l l' =>
CxtS h fs a l -> CxtS h fs a l'
forall h (a :: * -> *).
CxtS h MSoliditySig a ExpressionL -> CxtS h MSoliditySig a RhsL
injF (CxtS h MSoliditySig a ExpressionL -> CxtS h MSoliditySig a RhsL)
-> (CxtS h MSoliditySig a ExpressionL
    -> CxtS h MSoliditySig a ExpressionL)
-> CxtS h MSoliditySig a ExpressionL
-> CxtS h MSoliditySig a RhsL
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CxtS h MSoliditySig a ExpressionL
-> CxtS h MSoliditySig a ExpressionL
forall {k} h (f :: (* -> *) -> * -> *) (a :: * -> *) (j :: k).
(SolExpIsExpression :<: f) =>
Cxt h f a ExpressionL -> Cxt h f a ExpressionL
SolExpIsExpression'

  projF' :: forall h p (a :: * -> *).
Cxt h (Sum MSoliditySig :&: p) a RhsL
-> Maybe (Cxt h (Sum MSoliditySig :&: p) a ExpressionL)
projF' Cxt h (Sum MSoliditySig :&: p) a RhsL
e
    | Just (ExpressionIsRhs Cxt h (Sum MSoliditySig :&: p) a ExpressionL
rhs) <- Cxt h (Sum MSoliditySig :&: p) a RhsL
-> Maybe (ExpressionIsRhs (Cxt h (Sum MSoliditySig :&: p) a) RhsL)
forall (f :: (* -> *) -> * -> *) (f' :: (* -> *) -> * -> *)
       (s :: (* -> *) -> * -> *) h (a :: * -> *) i.
(RemA f f', s :<: f') =>
Cxt h f a i -> Maybe (s (Cxt h f a) i)
project' Cxt h (Sum MSoliditySig :&: p) a RhsL
e
    = Cxt h (Sum MSoliditySig :&: p) a ExpressionL
-> Maybe (Cxt h (Sum MSoliditySig :&: p) a ExpressionL)
forall (fs :: Signature) l l' h p (a :: * -> *).
InjF fs l l' =>
Cxt h (Sum fs :&: p) a l' -> Maybe (Cxt h (Sum fs :&: p) a l)
forall h p (a :: * -> *).
Cxt h (Sum MSoliditySig :&: p) a ExpressionL
-> Maybe (Cxt h (Sum MSoliditySig :&: p) a ExpressionL)
projF' Cxt h (Sum MSoliditySig :&: p) a ExpressionL
rhs
  projF' Cxt h (Sum MSoliditySig :&: p) a RhsL
_ = Maybe (Cxt h (Sum MSoliditySig :&: p) a ExpressionL)
forall a. Maybe a
Nothing