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

-- This module provides data types for representing partially typed
-- instructions.
module Morley.Michelson.TypeCheck.TypeCheckedOp
  ( TypeCheckedInstr
  , TypeCheckedOp(..)
  , IllTypedInstr(..)
  , Nesting
  , SomeSingInstr(..)
  , someInstrToOp
  , someViewToOp
  , withSomeTcInstr
  ) where

import Data.Singletons (SingI)
import Fmt (Doc)
import Prettyprinter (enclose)

import Morley.Michelson.Printer.Util
  (RenderDoc(..), doesntNeedParens, renderOpsList, renderOpsListNoBraces)
import Morley.Michelson.TypeCheck.Types (HST(..), SomeTcInstr(..), SomeTcInstrOut(..))
import Morley.Michelson.Typed.Aliases
import Morley.Michelson.Typed.Annotation
import Morley.Michelson.Typed.Convert (instrToOps)
import Morley.Michelson.Typed.Instr (Instr, castInstr)
import Morley.Michelson.Typed.View (SomeView'(..), View'(..))
import Morley.Michelson.Untyped qualified as U
import Morley.Michelson.Untyped.Instr (InstrAbstract(..))

-- | Represents a root of a partially typed operation tree.
type TypeCheckedInstr op = InstrAbstract [] (TypeCheckedOp op)

newtype Nesting = Nesting Word
  deriving newtype (Nesting -> Nesting -> Bool
(Nesting -> Nesting -> Bool)
-> (Nesting -> Nesting -> Bool) -> Eq Nesting
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Nesting -> Nesting -> Bool
== :: Nesting -> Nesting -> Bool
$c/= :: Nesting -> Nesting -> Bool
/= :: Nesting -> Nesting -> Bool
Eq, Eq Nesting
Eq Nesting
-> (Nesting -> Nesting -> Ordering)
-> (Nesting -> Nesting -> Bool)
-> (Nesting -> Nesting -> Bool)
-> (Nesting -> Nesting -> Bool)
-> (Nesting -> Nesting -> Bool)
-> (Nesting -> Nesting -> Nesting)
-> (Nesting -> Nesting -> Nesting)
-> Ord Nesting
Nesting -> Nesting -> Bool
Nesting -> Nesting -> Ordering
Nesting -> Nesting -> Nesting
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Nesting -> Nesting -> Ordering
compare :: Nesting -> Nesting -> Ordering
$c< :: Nesting -> Nesting -> Bool
< :: Nesting -> Nesting -> Bool
$c<= :: Nesting -> Nesting -> Bool
<= :: Nesting -> Nesting -> Bool
$c> :: Nesting -> Nesting -> Bool
> :: Nesting -> Nesting -> Bool
$c>= :: Nesting -> Nesting -> Bool
>= :: Nesting -> Nesting -> Bool
$cmax :: Nesting -> Nesting -> Nesting
max :: Nesting -> Nesting -> Nesting
$cmin :: Nesting -> Nesting -> Nesting
min :: Nesting -> Nesting -> Nesting
Ord, Int -> Nesting
Nesting -> Int
Nesting -> [Nesting]
Nesting -> Nesting
Nesting -> Nesting -> [Nesting]
Nesting -> Nesting -> Nesting -> [Nesting]
(Nesting -> Nesting)
-> (Nesting -> Nesting)
-> (Int -> Nesting)
-> (Nesting -> Int)
-> (Nesting -> [Nesting])
-> (Nesting -> Nesting -> [Nesting])
-> (Nesting -> Nesting -> [Nesting])
-> (Nesting -> Nesting -> Nesting -> [Nesting])
-> Enum Nesting
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
$csucc :: Nesting -> Nesting
succ :: Nesting -> Nesting
$cpred :: Nesting -> Nesting
pred :: Nesting -> Nesting
$ctoEnum :: Int -> Nesting
toEnum :: Int -> Nesting
$cfromEnum :: Nesting -> Int
fromEnum :: Nesting -> Int
$cenumFrom :: Nesting -> [Nesting]
enumFrom :: Nesting -> [Nesting]
$cenumFromThen :: Nesting -> Nesting -> [Nesting]
enumFromThen :: Nesting -> Nesting -> [Nesting]
$cenumFromTo :: Nesting -> Nesting -> [Nesting]
enumFromTo :: Nesting -> Nesting -> [Nesting]
$cenumFromThenTo :: Nesting -> Nesting -> Nesting -> [Nesting]
enumFromThenTo :: Nesting -> Nesting -> Nesting -> [Nesting]
Enum, Nesting
Nesting -> Nesting -> Bounded Nesting
forall a. a -> a -> Bounded a
$cminBound :: Nesting
minBound :: Nesting
$cmaxBound :: Nesting
maxBound :: Nesting
Bounded, Integer -> Nesting
Nesting -> Nesting
Nesting -> Nesting -> Nesting
(Nesting -> Nesting -> Nesting)
-> (Nesting -> Nesting -> Nesting)
-> (Nesting -> Nesting -> Nesting)
-> (Nesting -> Nesting)
-> (Nesting -> Nesting)
-> (Nesting -> Nesting)
-> (Integer -> Nesting)
-> Num Nesting
forall a.
(a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a)
-> (a -> a)
-> (a -> a)
-> (Integer -> a)
-> Num a
$c+ :: Nesting -> Nesting -> Nesting
+ :: Nesting -> Nesting -> Nesting
$c- :: Nesting -> Nesting -> Nesting
- :: Nesting -> Nesting -> Nesting
$c* :: Nesting -> Nesting -> Nesting
* :: Nesting -> Nesting -> Nesting
$cnegate :: Nesting -> Nesting
negate :: Nesting -> Nesting
$cabs :: Nesting -> Nesting
abs :: Nesting -> Nesting
$csignum :: Nesting -> Nesting
signum :: Nesting -> Nesting
$cfromInteger :: Integer -> Nesting
fromInteger :: Integer -> Nesting
Num, Nesting -> ()
(Nesting -> ()) -> NFData Nesting
forall a. (a -> ()) -> NFData a
$crnf :: Nesting -> ()
rnf :: Nesting -> ()
NFData)
  deriving stock Int -> Nesting -> ShowS
[Nesting] -> ShowS
Nesting -> String
(Int -> Nesting -> ShowS)
-> (Nesting -> String) -> ([Nesting] -> ShowS) -> Show Nesting
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Nesting -> ShowS
showsPrec :: Int -> Nesting -> ShowS
$cshow :: Nesting -> String
show :: Nesting -> String
$cshowList :: [Nesting] -> ShowS
showList :: [Nesting] -> ShowS
Show

data SomeSingInstr where
  SomeSingInstr :: (SingI inp, SingI out) => Instr inp out -> SomeSingInstr

deriving stock instance Show SomeSingInstr

instance Eq SomeSingInstr where
  SomeSingInstr Instr inp out
i1 == :: SomeSingInstr -> SomeSingInstr -> Bool
== SomeSingInstr Instr inp out
i2 = Instr inp out -> Maybe (Instr inp out)
forall (inp1 :: [T]) (out1 :: [T]) (inp2 :: [T]) (out2 :: [T]).
(SingI inp1, SingI out1, SingI inp2, SingI out2) =>
Instr inp1 out1 -> Maybe (Instr inp2 out2)
castInstr Instr inp out
i1 Maybe (Instr inp out) -> Maybe (Instr inp out) -> Bool
forall a. Eq a => a -> a -> Bool
== Instr inp out -> Maybe (Instr inp out)
forall a. a -> Maybe a
Just Instr inp out
i2

instance NFData SomeSingInstr where
  rnf :: SomeSingInstr -> ()
rnf (SomeSingInstr Instr inp out
x) = Instr inp out -> ()
forall a. NFData a => a -> ()
rnf Instr inp out
x

-- | Represents nodes of a partially typed operation tree.
data TypeCheckedOp op where
  -- | Constructs well-typed node.
  WellTypedOp :: SomeSingInstr -> TypeCheckedOp op
  -- | Constructs ill-typed node which might in turn contain well-typed and
  -- non-typed operations.
  IllTypedOp :: [IllTypedInstr op] -> TypeCheckedOp op
  -- | Partially typed sequence of operations. Used exclusively for error-reporting.
  -- 'Nesting' argument exists because we can't mix typed and untyped
  -- instructions, so we need a way to represent brace nesting of @{ <typed
  -- seq>; <untyped seq> }@
  MixedOp :: Nesting -> SomeSingInstr -> [IllTypedInstr op] -> TypeCheckedOp op
  deriving stock (TypeCheckedOp op -> TypeCheckedOp op -> Bool
(TypeCheckedOp op -> TypeCheckedOp op -> Bool)
-> (TypeCheckedOp op -> TypeCheckedOp op -> Bool)
-> Eq (TypeCheckedOp op)
forall op. Eq op => TypeCheckedOp op -> TypeCheckedOp op -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall op. Eq op => TypeCheckedOp op -> TypeCheckedOp op -> Bool
== :: TypeCheckedOp op -> TypeCheckedOp op -> Bool
$c/= :: forall op. Eq op => TypeCheckedOp op -> TypeCheckedOp op -> Bool
/= :: TypeCheckedOp op -> TypeCheckedOp op -> Bool
Eq, (forall a b. (a -> b) -> TypeCheckedOp a -> TypeCheckedOp b)
-> (forall a b. a -> TypeCheckedOp b -> TypeCheckedOp a)
-> Functor TypeCheckedOp
forall a b. a -> TypeCheckedOp b -> TypeCheckedOp a
forall a b. (a -> b) -> TypeCheckedOp a -> TypeCheckedOp b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> TypeCheckedOp a -> TypeCheckedOp b
fmap :: forall a b. (a -> b) -> TypeCheckedOp a -> TypeCheckedOp b
$c<$ :: forall a b. a -> TypeCheckedOp b -> TypeCheckedOp a
<$ :: forall a b. a -> TypeCheckedOp b -> TypeCheckedOp a
Functor, Int -> TypeCheckedOp op -> ShowS
[TypeCheckedOp op] -> ShowS
TypeCheckedOp op -> String
(Int -> TypeCheckedOp op -> ShowS)
-> (TypeCheckedOp op -> String)
-> ([TypeCheckedOp op] -> ShowS)
-> Show (TypeCheckedOp op)
forall op. Show op => Int -> TypeCheckedOp op -> ShowS
forall op. Show op => [TypeCheckedOp op] -> ShowS
forall op. Show op => TypeCheckedOp op -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall op. Show op => Int -> TypeCheckedOp op -> ShowS
showsPrec :: Int -> TypeCheckedOp op -> ShowS
$cshow :: forall op. Show op => TypeCheckedOp op -> String
show :: TypeCheckedOp op -> String
$cshowList :: forall op. Show op => [TypeCheckedOp op] -> ShowS
showList :: [TypeCheckedOp op] -> ShowS
Show)

-- | Represents a non-well-typed operation
data IllTypedInstr op
  = SemiTypedInstr (TypeCheckedInstr op) -- ^ Constructs a partially typed operation.
  | NonTypedInstr op  -- ^ Constructs a completely untyped operation.
  | IllTypedNest [IllTypedInstr op] -- ^ Nested sequence of ill-typed operations.
  deriving stock (Int -> IllTypedInstr op -> ShowS
[IllTypedInstr op] -> ShowS
IllTypedInstr op -> String
(Int -> IllTypedInstr op -> ShowS)
-> (IllTypedInstr op -> String)
-> ([IllTypedInstr op] -> ShowS)
-> Show (IllTypedInstr op)
forall op. Show op => Int -> IllTypedInstr op -> ShowS
forall op. Show op => [IllTypedInstr op] -> ShowS
forall op. Show op => IllTypedInstr op -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall op. Show op => Int -> IllTypedInstr op -> ShowS
showsPrec :: Int -> IllTypedInstr op -> ShowS
$cshow :: forall op. Show op => IllTypedInstr op -> String
show :: IllTypedInstr op -> String
$cshowList :: forall op. Show op => [IllTypedInstr op] -> ShowS
showList :: [IllTypedInstr op] -> ShowS
Show, IllTypedInstr op -> IllTypedInstr op -> Bool
(IllTypedInstr op -> IllTypedInstr op -> Bool)
-> (IllTypedInstr op -> IllTypedInstr op -> Bool)
-> Eq (IllTypedInstr op)
forall op. Eq op => IllTypedInstr op -> IllTypedInstr op -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall op. Eq op => IllTypedInstr op -> IllTypedInstr op -> Bool
== :: IllTypedInstr op -> IllTypedInstr op -> Bool
$c/= :: forall op. Eq op => IllTypedInstr op -> IllTypedInstr op -> Bool
/= :: IllTypedInstr op -> IllTypedInstr op -> Bool
Eq, (forall x. IllTypedInstr op -> Rep (IllTypedInstr op) x)
-> (forall x. Rep (IllTypedInstr op) x -> IllTypedInstr op)
-> Generic (IllTypedInstr op)
forall x. Rep (IllTypedInstr op) x -> IllTypedInstr op
forall x. IllTypedInstr op -> Rep (IllTypedInstr op) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall op x. Rep (IllTypedInstr op) x -> IllTypedInstr op
forall op x. IllTypedInstr op -> Rep (IllTypedInstr op) x
$cfrom :: forall op x. IllTypedInstr op -> Rep (IllTypedInstr op) x
from :: forall x. IllTypedInstr op -> Rep (IllTypedInstr op) x
$cto :: forall op x. Rep (IllTypedInstr op) x -> IllTypedInstr op
to :: forall x. Rep (IllTypedInstr op) x -> IllTypedInstr op
Generic, (forall a b. (a -> b) -> IllTypedInstr a -> IllTypedInstr b)
-> (forall a b. a -> IllTypedInstr b -> IllTypedInstr a)
-> Functor IllTypedInstr
forall a b. a -> IllTypedInstr b -> IllTypedInstr a
forall a b. (a -> b) -> IllTypedInstr a -> IllTypedInstr b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> IllTypedInstr a -> IllTypedInstr b
fmap :: forall a b. (a -> b) -> IllTypedInstr a -> IllTypedInstr b
$c<$ :: forall a b. a -> IllTypedInstr b -> IllTypedInstr a
<$ :: forall a b. a -> IllTypedInstr b -> IllTypedInstr a
Functor)

instance RenderDoc op => RenderDoc (IllTypedInstr op) where
  renderDoc :: RenderContext -> IllTypedInstr op -> Doc ()
renderDoc RenderContext
pn = \case
    SemiTypedInstr TypeCheckedInstr op
instr -> RenderContext -> TypeCheckedInstr op -> Doc ()
forall a. RenderDoc a => RenderContext -> a -> Doc ()
renderDoc RenderContext
pn TypeCheckedInstr op
instr
    NonTypedInstr op
op -> RenderContext -> op -> Doc ()
forall a. RenderDoc a => RenderContext -> a -> Doc ()
renderDoc RenderContext
pn op
op
    IllTypedNest [IllTypedInstr op]
ops -> Bool -> [IllTypedInstr op] -> Doc ()
forall op (f :: * -> *).
(RenderDoc op, Foldable f) =>
Bool -> f op -> Doc ()
renderOpsList Bool
False [IllTypedInstr op]
ops

deriving anyclass instance (NFData (TypeCheckedOp op), NFData op) => NFData (IllTypedInstr op)

instance RenderDoc op => RenderDoc (TypeCheckedOp op) where
  renderDoc :: RenderContext -> TypeCheckedOp op -> Doc ()
renderDoc RenderContext
_ (WellTypedOp (SomeSingInstr Instr inp out
instr)) = Bool -> [ExpandedOp] -> Doc ()
forall op (f :: * -> *).
(RenderDoc op, Foldable f) =>
Bool -> f op -> Doc ()
renderOpsListNoBraces Bool
False (Instr inp out -> [ExpandedOp]
forall (inp :: [T]) (out :: [T]).
HasCallStack =>
Instr inp out -> [ExpandedOp]
instrToOps Instr inp out
instr)
  renderDoc RenderContext
_ (MixedOp Nesting
nesting (SomeSingInstr Instr inp out
instr) [IllTypedInstr op]
rest) =
    Nesting -> Doc () -> Doc ()
nestBraces Nesting
nesting (Doc () -> Doc ()) -> Doc () -> Doc ()
forall a b. (a -> b) -> a -> b
$ Bool -> [Doc ()] -> Doc ()
forall op (f :: * -> *).
(RenderDoc op, Foldable f) =>
Bool -> f op -> Doc ()
renderOpsListNoBraces Bool
False ([Doc ()] -> Doc ()) -> [Doc ()] -> Doc ()
forall a b. (a -> b) -> a -> b
$ [ExpandedOp] -> [Doc ()]
forall a. RenderDoc a => [a] -> [Doc ()]
doRender (Instr inp out -> [ExpandedOp]
forall (inp :: [T]) (out :: [T]).
HasCallStack =>
Instr inp out -> [ExpandedOp]
instrToOps Instr inp out
instr) [Doc ()] -> [Doc ()] -> [Doc ()]
forall a. Semigroup a => a -> a -> a
<> [IllTypedInstr op] -> [Doc ()]
forall a. RenderDoc a => [a] -> [Doc ()]
doRender [IllTypedInstr op]
rest
    where
      doRender :: RenderDoc a => [a] -> [Doc]
      doRender :: forall a. RenderDoc a => [a] -> [Doc ()]
doRender = (a -> Doc ()) -> [a] -> [Doc ()]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (RenderContext -> a -> Doc ()
forall a. RenderDoc a => RenderContext -> a -> Doc ()
renderDoc RenderContext
doesntNeedParens) ([a] -> [Doc ()]) -> ([a] -> [a]) -> [a] -> [Doc ()]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Bool) -> [a] -> [a]
forall a. (a -> Bool) -> [a] -> [a]
filter a -> Bool
forall a. RenderDoc a => a -> Bool
isRenderable
  renderDoc RenderContext
_ (IllTypedOp [IllTypedInstr op]
ops) = Bool -> [IllTypedInstr op] -> Doc ()
forall op (f :: * -> *).
(RenderDoc op, Foldable f) =>
Bool -> f op -> Doc ()
renderOpsListNoBraces Bool
False [IllTypedInstr op]
ops

nestBraces :: Nesting -> Doc -> Doc
nestBraces :: Nesting -> Doc () -> Doc ()
nestBraces Nesting
0 = Doc () -> Doc ()
forall a. a -> a
id
nestBraces Nesting
n = Doc () -> Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann -> Doc ann
enclose Doc ()
"{ " Doc ()
" }" (Doc () -> Doc ()) -> (Doc () -> Doc ()) -> Doc () -> Doc ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Nesting -> Doc () -> Doc ()
nestBraces (Nesting -> Nesting
forall a. Enum a => a -> a
pred Nesting
n)

-- | Makes a well-typed node out of `SomeTcInstr`
someInstrToOp :: SomeTcInstr inp -> TypeCheckedOp op
someInstrToOp :: forall (inp :: [T]) op. SomeTcInstr inp -> TypeCheckedOp op
someInstrToOp SomeTcInstr inp
hst = SomeTcInstr inp
-> (forall (out :: [T]).
    (SingI inp, SingI out) =>
    Instr inp out -> TypeCheckedOp op)
-> TypeCheckedOp op
forall (inp :: [T]) r.
SomeTcInstr inp
-> (forall (out :: [T]).
    (SingI inp, SingI out) =>
    Instr inp out -> r)
-> r
withSomeTcInstr SomeTcInstr inp
hst ((forall (out :: [T]).
  (SingI inp, SingI out) =>
  Instr inp out -> TypeCheckedOp op)
 -> TypeCheckedOp op)
-> (forall (out :: [T]).
    (SingI inp, SingI out) =>
    Instr inp out -> TypeCheckedOp op)
-> TypeCheckedOp op
forall a b. (a -> b) -> a -> b
$ SomeSingInstr -> TypeCheckedOp op
forall op. SomeSingInstr -> TypeCheckedOp op
WellTypedOp (SomeSingInstr -> TypeCheckedOp op)
-> (Instr inp out -> SomeSingInstr)
-> Instr inp out
-> TypeCheckedOp op
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Instr inp out -> SomeSingInstr
forall (inp :: [T]) (out :: [T]).
(SingI inp, SingI out) =>
Instr inp out -> SomeSingInstr
SomeSingInstr

-- | Extracts 'Instr' from 'SomeTcInstr' and passes it to a continuation.
withSomeTcInstr
  :: SomeTcInstr inp
  -> (forall out. (SingI inp, SingI out) => Instr inp out -> r)
  -> r
withSomeTcInstr :: forall (inp :: [T]) r.
SomeTcInstr inp
-> (forall (out :: [T]).
    (SingI inp, SingI out) =>
    Instr inp out -> r)
-> r
withSomeTcInstr (HST inp
hst :/ SomeTcInstrOut inp
rest) = case HST inp
hst of
  HST inp
SNil -> SomeTcInstrOut inp
-> (forall (out :: [T]).
    (SingI inp, SingI out) =>
    Instr inp out -> r)
-> r
forall (inp :: [T]) r.
SingI inp =>
SomeTcInstrOut inp
-> (forall (out :: [T]).
    (SingI inp, SingI out) =>
    Instr inp out -> r)
-> r
go SomeTcInstrOut inp
rest
  (::&){} -> SomeTcInstrOut inp
-> (forall (out :: [T]).
    (SingI inp, SingI out) =>
    Instr inp out -> r)
-> r
forall (inp :: [T]) r.
SingI inp =>
SomeTcInstrOut inp
-> (forall (out :: [T]).
    (SingI inp, SingI out) =>
    Instr inp out -> r)
-> r
go SomeTcInstrOut inp
rest
  where
    go :: SingI inp => SomeTcInstrOut inp
       -> (forall out. (SingI inp, SingI out) => Instr inp out -> r)
       -> r
    go :: forall (inp :: [T]) r.
SingI inp =>
SomeTcInstrOut inp
-> (forall (out :: [T]).
    (SingI inp, SingI out) =>
    Instr inp out -> r)
-> r
go (Instr inp out
i ::: HST out
_) forall (out :: [T]). (SingI inp, SingI out) => Instr inp out -> r
cont = Instr inp out -> r
forall (out :: [T]). (SingI inp, SingI out) => Instr inp out -> r
cont Instr inp out
i
    go (AnyOutInstr forall (out :: [T]). Instr inp out
i) forall (out :: [T]). (SingI inp, SingI out) => Instr inp out -> r
cont = Instr inp '[] -> r
forall (out :: [T]). (SingI inp, SingI out) => Instr inp out -> r
cont (forall (out :: [T]). Instr inp out
i @'[])

-- | Makes takes a typed view and converts it into an untyped one with
-- typechecked code.
someViewToOp :: SomeView st -> U.View' (TypeCheckedOp op)
someViewToOp :: forall (st :: T) op. SomeView st -> View' (TypeCheckedOp op)
someViewToOp (SomeView View{ViewName
Notes arg
Notes ret
ViewCode' Instr arg st ret
vName :: ViewName
vArgument :: Notes arg
vReturn :: Notes ret
vCode :: ViewCode' Instr arg st ret
vName :: forall (instr :: [T] -> [T] -> *) (arg :: T) (st :: T) (ret :: T).
View' instr arg st ret -> ViewName
vArgument :: forall (instr :: [T] -> [T] -> *) (arg :: T) (st :: T) (ret :: T).
View' instr arg st ret -> Notes arg
vReturn :: forall (instr :: [T] -> [T] -> *) (arg :: T) (st :: T) (ret :: T).
View' instr arg st ret -> Notes ret
vCode :: forall (instr :: [T] -> [T] -> *) (arg :: T) (st :: T) (ret :: T).
View' instr arg st ret -> ViewCode' instr arg st ret
..}) = U.View
  { viewCode :: TypeCheckedOp op
U.viewCode = SomeSingInstr -> TypeCheckedOp op
forall op. SomeSingInstr -> TypeCheckedOp op
WellTypedOp (SomeSingInstr -> TypeCheckedOp op)
-> SomeSingInstr -> TypeCheckedOp op
forall a b. (a -> b) -> a -> b
$ ViewCode' Instr arg st ret -> SomeSingInstr
forall (inp :: [T]) (out :: [T]).
(SingI inp, SingI out) =>
Instr inp out -> SomeSingInstr
SomeSingInstr ViewCode' Instr arg st ret
vCode
  , viewName :: ViewName
U.viewName = ViewName
vName
  , viewArgument :: Ty
U.viewArgument = Notes arg -> Ty
forall (x :: T). Notes x -> Ty
mkUType Notes arg
vArgument
  , viewReturn :: Ty
U.viewReturn = Notes ret -> Ty
forall (x :: T). Notes x -> Ty
mkUType Notes ret
vReturn
  }

instance NFData op => NFData (TypeCheckedOp op) where
  rnf :: TypeCheckedOp op -> ()
rnf = \case
    WellTypedOp SomeSingInstr
x -> SomeSingInstr -> ()
forall a. NFData a => a -> ()
rnf SomeSingInstr
x
    IllTypedOp [IllTypedInstr op]
x -> [IllTypedInstr op] -> ()
forall a. NFData a => a -> ()
rnf [IllTypedInstr op]
x
    MixedOp Nesting
x SomeSingInstr
y [IllTypedInstr op]
z -> Nesting -> ()
forall a. NFData a => a -> ()
rnf Nesting
x () -> () -> ()
forall a b. a -> b -> b
`seq` SomeSingInstr -> ()
forall a. NFData a => a -> ()
rnf SomeSingInstr
y () -> () -> ()
forall a b. a -> b -> b
`seq` [IllTypedInstr op] -> ()
forall a. NFData a => a -> ()
rnf [IllTypedInstr op]
z