{-# LANGUAGE GADTs      #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE RankNTypes #-}

module PlutusIR.Pass where

import PlutusIR.Check.Uniques qualified as Uniques
import PlutusIR.Core.Type
import PlutusIR.Error
import PlutusIR.TypeCheck qualified as TC

import PlutusCore qualified as PLC
import PlutusCore.Name.Unique

import Control.Monad (void, when)
import Control.Monad.Except
import Control.Monad.Trans.Class (lift)
import Data.Foldable
import Data.Text (Text)
import PlutusCore.Quote

-- | A condition on a 'Term'.
data Condition tyname name uni fun a where
  -- | The 'Term' typechecks.
  Typechecks :: (PLC.Typecheckable uni fun, PLC.GEq uni)
    => TC.PirTCConfig uni fun -> Condition TyName Name uni fun a
  -- | The 'Term' has globally unique names.
  GloballyUniqueNames :: (HasUnique tyname TypeUnique, HasUnique name TermUnique, Ord a)
    => Condition tyname name uni fun a
  -- | A custom condition. 'Nothing' indicates success, 'Just' indicates a failure at
  -- a location with a message.
  Custom :: (Term tyname name uni fun a -> Maybe (a, Text))
    -> Condition tyname name uni fun a

-- | A condition on a pair of 'Term's.
data BiCondition tyname name uni fun a where
  -- | A condition on the second 'Term'.
  ConstCondition :: Condition tyname name uni fun a -> BiCondition tyname name uni fun a
  -- | A custom condition. 'Nothing' indicates success, 'Just' indicates a failure at
  -- a location with a message.
  CustomBi :: (Term tyname name uni fun a -> Term tyname name uni fun a -> Maybe (a, Text))
    -> BiCondition tyname name uni fun a

checkCondition
  :: MonadError (Error uni fun a) m
  => Condition tyname name uni fun a
  -> Term tyname name uni fun a
  -> m ()
checkCondition :: forall (uni :: * -> *) fun a (m :: * -> *) tyname name.
MonadError (Error uni fun a) m =>
Condition tyname name uni fun a
-> Term tyname name uni fun a -> m ()
checkCondition Condition tyname name uni fun a
c Term tyname name uni fun a
t = case Condition tyname name uni fun a
c of
  Typechecks PirTCConfig uni fun
tcconfig -> m (Normalized (Type TyName uni ())) -> m ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (m (Normalized (Type TyName uni ())) -> m ())
-> m (Normalized (Type TyName uni ())) -> m ()
forall a b. (a -> b) -> a -> b
$ QuoteT m (Normalized (Type TyName uni ()))
-> m (Normalized (Type TyName uni ()))
forall (m :: * -> *) a. Monad m => QuoteT m a -> m a
runQuoteT (QuoteT m (Normalized (Type TyName uni ()))
 -> m (Normalized (Type TyName uni ())))
-> QuoteT m (Normalized (Type TyName uni ()))
-> m (Normalized (Type TyName uni ()))
forall a b. (a -> b) -> a -> b
$ do
    -- Typechecking requires globally unique names
    Term tyname name uni fun a
renamed <- Term tyname name uni fun a -> QuoteT m (Term tyname name uni fun a)
forall a (m :: * -> *). (Rename a, MonadQuote m) => a -> m a
forall (m :: * -> *).
MonadQuote m =>
Term tyname name uni fun a -> m (Term tyname name uni fun a)
PLC.rename Term tyname name uni fun a
t
    PirTCConfig uni fun
-> Term TyName Name uni fun a
-> QuoteT m (Normalized (Type TyName uni ()))
forall err (uni :: * -> *) fun ann (m :: * -> *).
MonadTypeCheckPir err uni fun ann m =>
PirTCConfig uni fun
-> Term TyName Name uni fun ann
-> m (Normalized (Type TyName uni ()))
TC.inferType PirTCConfig uni fun
tcconfig Term tyname name uni fun a
Term TyName Name uni fun a
renamed
  Condition tyname name uni fun a
GloballyUniqueNames -> m () -> m ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ (UniqueError a -> Bool) -> Term tyname name uni fun a -> m ()
forall ann name tyname e (m :: * -> *) (uni :: * -> *) fun.
(Ord ann, HasUnique name TermUnique, HasUnique tyname TypeUnique,
 AsUniqueError e ann, MonadError e m) =>
(UniqueError ann -> Bool) -> Term tyname name uni fun ann -> m ()
Uniques.checkTerm (Bool -> UniqueError a -> Bool
forall a b. a -> b -> a
const Bool
True) Term tyname name uni fun a
t
  Custom Term tyname name uni fun a -> Maybe (a, Text)
f -> case Term tyname name uni fun a -> Maybe (a, Text)
f Term tyname name uni fun a
t of
    Just (a
a, Text
e) -> Error uni fun a -> m ()
forall a. Error uni fun a -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Error uni fun a -> m ()) -> Error uni fun a -> m ()
forall a b. (a -> b) -> a -> b
$ a -> Text -> Error uni fun a
forall (uni :: * -> *) fun a. a -> Text -> Error uni fun a
CompilationError a
a Text
e
    Maybe (a, Text)
Nothing     -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

checkBiCondition
  :: MonadError (Error uni fun a) m
  => BiCondition tyname name uni fun a
  -> Term tyname name uni fun a
  -> Term tyname name uni fun a
  -> m ()
checkBiCondition :: forall (uni :: * -> *) fun a (m :: * -> *) tyname name.
MonadError (Error uni fun a) m =>
BiCondition tyname name uni fun a
-> Term tyname name uni fun a -> Term tyname name uni fun a -> m ()
checkBiCondition BiCondition tyname name uni fun a
c Term tyname name uni fun a
t1 Term tyname name uni fun a
t2 = case BiCondition tyname name uni fun a
c of
  ConstCondition Condition tyname name uni fun a
c' -> Condition tyname name uni fun a
-> Term tyname name uni fun a -> m ()
forall (uni :: * -> *) fun a (m :: * -> *) tyname name.
MonadError (Error uni fun a) m =>
Condition tyname name uni fun a
-> Term tyname name uni fun a -> m ()
checkCondition Condition tyname name uni fun a
c' Term tyname name uni fun a
t2
  CustomBi Term tyname name uni fun a
-> Term tyname name uni fun a -> Maybe (a, Text)
f -> case Term tyname name uni fun a
-> Term tyname name uni fun a -> Maybe (a, Text)
f Term tyname name uni fun a
t1 Term tyname name uni fun a
t2 of
    Just (a
a, Text
e) -> Error uni fun a -> m ()
forall a. Error uni fun a -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Error uni fun a -> m ()) -> Error uni fun a -> m ()
forall a b. (a -> b) -> a -> b
$ a -> Text -> Error uni fun a
forall (uni :: * -> *) fun a. a -> Text -> Error uni fun a
CompilationError a
a Text
e
    Maybe (a, Text)
Nothing     -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

-- | A pass over a term, with pre- and post-conditions.
data Pass m tyname name uni fun a =
  -- | A basic pass. Has a function, which is the pass itself, a set of pre-conditions
  -- which are run on the input term, and a set of post-conditions which are run on the
  -- input and output terms (so can compare them).
  Pass
    (Term tyname name uni fun a -> m (Term tyname name uni fun a))
    [Condition tyname name uni fun a]
    [BiCondition tyname name uni fun a]
  | CompoundPass (Pass m tyname name uni fun a) (Pass m tyname name uni fun a)
  | NoOpPass
  | NamedPass String (Pass m tyname name uni fun a)

instance Semigroup (Pass m tyname name uni fun a) where
  Pass m tyname name uni fun a
p1 <> :: Pass m tyname name uni fun a
-> Pass m tyname name uni fun a -> Pass m tyname name uni fun a
<> Pass m tyname name uni fun a
p2 = Pass m tyname name uni fun a
-> Pass m tyname name uni fun a -> Pass m tyname name uni fun a
forall (m :: * -> *) tyname name (uni :: * -> *) fun a.
Pass m tyname name uni fun a
-> Pass m tyname name uni fun a -> Pass m tyname name uni fun a
CompoundPass Pass m tyname name uni fun a
p1 Pass m tyname name uni fun a
p2

instance Monoid (Pass m tyname name uni fun a) where
  mempty :: Pass m tyname name uni fun a
mempty = Pass m tyname name uni fun a
forall (m :: * -> *) tyname name (uni :: * -> *) fun a.
Pass m tyname name uni fun a
NoOpPass

hoistPass :: (forall v . m v -> n v) -> Pass m tyname name uni fun a -> Pass n tyname name uni fun a
hoistPass :: forall (m :: * -> *) (n :: * -> *) tyname name (uni :: * -> *) fun
       a.
(forall v. m v -> n v)
-> Pass m tyname name uni fun a -> Pass n tyname name uni fun a
hoistPass forall v. m v -> n v
f Pass m tyname name uni fun a
p = case Pass m tyname name uni fun a
p of
  Pass Term tyname name uni fun a -> m (Term tyname name uni fun a)
mainPass [Condition tyname name uni fun a]
pre [BiCondition tyname name uni fun a]
post -> (Term tyname name uni fun a -> n (Term tyname name uni fun a))
-> [Condition tyname name uni fun a]
-> [BiCondition tyname name uni fun a]
-> Pass n tyname name uni fun a
forall (m :: * -> *) tyname name (uni :: * -> *) fun a.
(Term tyname name uni fun a -> m (Term tyname name uni fun a))
-> [Condition tyname name uni fun a]
-> [BiCondition tyname name uni fun a]
-> Pass m tyname name uni fun a
Pass (m (Term tyname name uni fun a) -> n (Term tyname name uni fun a)
forall v. m v -> n v
f (m (Term tyname name uni fun a) -> n (Term tyname name uni fun a))
-> (Term tyname name uni fun a -> m (Term tyname name uni fun a))
-> Term tyname name uni fun a
-> n (Term tyname name uni fun a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term tyname name uni fun a -> m (Term tyname name uni fun a)
mainPass) [Condition tyname name uni fun a]
pre [BiCondition tyname name uni fun a]
post
  CompoundPass Pass m tyname name uni fun a
p1 Pass m tyname name uni fun a
p2     -> Pass n tyname name uni fun a
-> Pass n tyname name uni fun a -> Pass n tyname name uni fun a
forall (m :: * -> *) tyname name (uni :: * -> *) fun a.
Pass m tyname name uni fun a
-> Pass m tyname name uni fun a -> Pass m tyname name uni fun a
CompoundPass ((forall v. m v -> n v)
-> Pass m tyname name uni fun a -> Pass n tyname name uni fun a
forall (m :: * -> *) (n :: * -> *) tyname name (uni :: * -> *) fun
       a.
(forall v. m v -> n v)
-> Pass m tyname name uni fun a -> Pass n tyname name uni fun a
hoistPass m v -> n v
forall v. m v -> n v
f Pass m tyname name uni fun a
p1) ((forall v. m v -> n v)
-> Pass m tyname name uni fun a -> Pass n tyname name uni fun a
forall (m :: * -> *) (n :: * -> *) tyname name (uni :: * -> *) fun
       a.
(forall v. m v -> n v)
-> Pass m tyname name uni fun a -> Pass n tyname name uni fun a
hoistPass m v -> n v
forall v. m v -> n v
f Pass m tyname name uni fun a
p2)
  NamedPass String
n Pass m tyname name uni fun a
pass       -> String
-> Pass n tyname name uni fun a -> Pass n tyname name uni fun a
forall (m :: * -> *) tyname name (uni :: * -> *) fun a.
String
-> Pass m tyname name uni fun a -> Pass m tyname name uni fun a
NamedPass String
n ((forall v. m v -> n v)
-> Pass m tyname name uni fun a -> Pass n tyname name uni fun a
forall (m :: * -> *) (n :: * -> *) tyname name (uni :: * -> *) fun
       a.
(forall v. m v -> n v)
-> Pass m tyname name uni fun a -> Pass n tyname name uni fun a
hoistPass m v -> n v
forall v. m v -> n v
f Pass m tyname name uni fun a
pass)
  Pass m tyname name uni fun a
NoOpPass               -> Pass n tyname name uni fun a
forall (m :: * -> *) tyname name (uni :: * -> *) fun a.
Pass m tyname name uni fun a
NoOpPass

runPass
  :: Monad m
  => (String -> m ())
  -> Bool
  -> Pass m tyname name uni fun a
  -> Term tyname name uni fun a
  -> ExceptT (Error uni fun a) m (Term tyname name uni fun a)
runPass :: forall (m :: * -> *) tyname name (uni :: * -> *) fun a.
Monad m =>
(String -> m ())
-> Bool
-> Pass m tyname name uni fun a
-> Term tyname name uni fun a
-> ExceptT (Error uni fun a) m (Term tyname name uni fun a)
runPass String -> m ()
logger Bool
checkConditions (Pass Term tyname name uni fun a -> m (Term tyname name uni fun a)
mainPass [Condition tyname name uni fun a]
pre [BiCondition tyname name uni fun a]
post) Term tyname name uni fun a
t = do
  Bool
-> ExceptT (Error uni fun a) m () -> ExceptT (Error uni fun a) m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
checkConditions (ExceptT (Error uni fun a) m () -> ExceptT (Error uni fun a) m ())
-> ExceptT (Error uni fun a) m () -> ExceptT (Error uni fun a) m ()
forall a b. (a -> b) -> a -> b
$ do
    m () -> ExceptT (Error uni fun a) m ()
forall (m :: * -> *) a.
Monad m =>
m a -> ExceptT (Error uni fun a) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> ExceptT (Error uni fun a) m ())
-> m () -> ExceptT (Error uni fun a) m ()
forall a b. (a -> b) -> a -> b
$ String -> m ()
logger String
"checking preconditions"
    [Condition tyname name uni fun a]
-> (Condition tyname name uni fun a
    -> ExceptT (Error uni fun a) m ())
-> ExceptT (Error uni fun a) m ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
t a -> (a -> f b) -> f ()
for_ [Condition tyname name uni fun a]
pre ((Condition tyname name uni fun a
  -> ExceptT (Error uni fun a) m ())
 -> ExceptT (Error uni fun a) m ())
-> (Condition tyname name uni fun a
    -> ExceptT (Error uni fun a) m ())
-> ExceptT (Error uni fun a) m ()
forall a b. (a -> b) -> a -> b
$ \Condition tyname name uni fun a
c -> Condition tyname name uni fun a
-> Term tyname name uni fun a -> ExceptT (Error uni fun a) m ()
forall (uni :: * -> *) fun a (m :: * -> *) tyname name.
MonadError (Error uni fun a) m =>
Condition tyname name uni fun a
-> Term tyname name uni fun a -> m ()
checkCondition Condition tyname name uni fun a
c Term tyname name uni fun a
t
  Term tyname name uni fun a
t' <- m (Term tyname name uni fun a)
-> ExceptT (Error uni fun a) m (Term tyname name uni fun a)
forall (m :: * -> *) a.
Monad m =>
m a -> ExceptT (Error uni fun a) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m (Term tyname name uni fun a)
 -> ExceptT (Error uni fun a) m (Term tyname name uni fun a))
-> m (Term tyname name uni fun a)
-> ExceptT (Error uni fun a) m (Term tyname name uni fun a)
forall a b. (a -> b) -> a -> b
$ Term tyname name uni fun a -> m (Term tyname name uni fun a)
mainPass Term tyname name uni fun a
t
  Bool
-> ExceptT (Error uni fun a) m () -> ExceptT (Error uni fun a) m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
checkConditions (ExceptT (Error uni fun a) m () -> ExceptT (Error uni fun a) m ())
-> ExceptT (Error uni fun a) m () -> ExceptT (Error uni fun a) m ()
forall a b. (a -> b) -> a -> b
$ do
    m () -> ExceptT (Error uni fun a) m ()
forall (m :: * -> *) a.
Monad m =>
m a -> ExceptT (Error uni fun a) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> ExceptT (Error uni fun a) m ())
-> m () -> ExceptT (Error uni fun a) m ()
forall a b. (a -> b) -> a -> b
$ String -> m ()
logger String
"checking postconditions"
    [BiCondition tyname name uni fun a]
-> (BiCondition tyname name uni fun a
    -> ExceptT (Error uni fun a) m ())
-> ExceptT (Error uni fun a) m ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
t a -> (a -> f b) -> f ()
for_ [BiCondition tyname name uni fun a]
post ((BiCondition tyname name uni fun a
  -> ExceptT (Error uni fun a) m ())
 -> ExceptT (Error uni fun a) m ())
-> (BiCondition tyname name uni fun a
    -> ExceptT (Error uni fun a) m ())
-> ExceptT (Error uni fun a) m ()
forall a b. (a -> b) -> a -> b
$ \BiCondition tyname name uni fun a
c -> BiCondition tyname name uni fun a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
-> ExceptT (Error uni fun a) m ()
forall (uni :: * -> *) fun a (m :: * -> *) tyname name.
MonadError (Error uni fun a) m =>
BiCondition tyname name uni fun a
-> Term tyname name uni fun a -> Term tyname name uni fun a -> m ()
checkBiCondition BiCondition tyname name uni fun a
c Term tyname name uni fun a
t Term tyname name uni fun a
t'
  Term tyname name uni fun a
-> ExceptT (Error uni fun a) m (Term tyname name uni fun a)
forall a. a -> ExceptT (Error uni fun a) m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term tyname name uni fun a
t'
runPass String -> m ()
logger Bool
checkConditions (CompoundPass Pass m tyname name uni fun a
p1 Pass m tyname name uni fun a
p2) Term tyname name uni fun a
t = do
  Term tyname name uni fun a
t' <- (String -> m ())
-> Bool
-> Pass m tyname name uni fun a
-> Term tyname name uni fun a
-> ExceptT (Error uni fun a) m (Term tyname name uni fun a)
forall (m :: * -> *) tyname name (uni :: * -> *) fun a.
Monad m =>
(String -> m ())
-> Bool
-> Pass m tyname name uni fun a
-> Term tyname name uni fun a
-> ExceptT (Error uni fun a) m (Term tyname name uni fun a)
runPass String -> m ()
logger Bool
checkConditions Pass m tyname name uni fun a
p1 Term tyname name uni fun a
t
  (String -> m ())
-> Bool
-> Pass m tyname name uni fun a
-> Term tyname name uni fun a
-> ExceptT (Error uni fun a) m (Term tyname name uni fun a)
forall (m :: * -> *) tyname name (uni :: * -> *) fun a.
Monad m =>
(String -> m ())
-> Bool
-> Pass m tyname name uni fun a
-> Term tyname name uni fun a
-> ExceptT (Error uni fun a) m (Term tyname name uni fun a)
runPass String -> m ()
logger Bool
checkConditions Pass m tyname name uni fun a
p2 Term tyname name uni fun a
t'
runPass String -> m ()
logger Bool
checkConditions (NamedPass String
n Pass m tyname name uni fun a
pass) Term tyname name uni fun a
t = do
  m () -> ExceptT (Error uni fun a) m ()
forall (m :: * -> *) a.
Monad m =>
m a -> ExceptT (Error uni fun a) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> ExceptT (Error uni fun a) m ())
-> m () -> ExceptT (Error uni fun a) m ()
forall a b. (a -> b) -> a -> b
$ String -> m ()
logger (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ String
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
": running pass"
  Term tyname name uni fun a
t' <- (String -> m ())
-> Bool
-> Pass m tyname name uni fun a
-> Term tyname name uni fun a
-> ExceptT (Error uni fun a) m (Term tyname name uni fun a)
forall (m :: * -> *) tyname name (uni :: * -> *) fun a.
Monad m =>
(String -> m ())
-> Bool
-> Pass m tyname name uni fun a
-> Term tyname name uni fun a
-> ExceptT (Error uni fun a) m (Term tyname name uni fun a)
runPass String -> m ()
logger Bool
checkConditions Pass m tyname name uni fun a
pass Term tyname name uni fun a
t
  m () -> ExceptT (Error uni fun a) m ()
forall (m :: * -> *) a.
Monad m =>
m a -> ExceptT (Error uni fun a) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> ExceptT (Error uni fun a) m ())
-> m () -> ExceptT (Error uni fun a) m ()
forall a b. (a -> b) -> a -> b
$ String -> m ()
logger (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ String
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
": finished pass"
  Term tyname name uni fun a
-> ExceptT (Error uni fun a) m (Term tyname name uni fun a)
forall a. a -> ExceptT (Error uni fun a) m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term tyname name uni fun a
t'
runPass String -> m ()
_ Bool
_ Pass m tyname name uni fun a
NoOpPass Term tyname name uni fun a
t = Term tyname name uni fun a
-> ExceptT (Error uni fun a) m (Term tyname name uni fun a)
forall a. a -> ExceptT (Error uni fun a) m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term tyname name uni fun a
t

-- | A simple, non-monadic pass that should typecheck.
simplePass
  :: (PLC.Typecheckable uni fun, PLC.GEq uni, Applicative m)
  => String
  -> TC.PirTCConfig uni fun
  -> (Term TyName Name uni fun a -> Term TyName Name uni fun a)
  -> Pass m TyName Name uni fun a
simplePass :: forall (uni :: * -> *) fun (m :: * -> *) a.
(Typecheckable uni fun, GEq uni, Applicative m) =>
String
-> PirTCConfig uni fun
-> (Term TyName Name uni fun a -> Term TyName Name uni fun a)
-> Pass m TyName Name uni fun a
simplePass String
name PirTCConfig uni fun
tcConfig Term TyName Name uni fun a -> Term TyName Name uni fun a
f =
  String
-> Pass m TyName Name uni fun a -> Pass m TyName Name uni fun a
forall (m :: * -> *) tyname name (uni :: * -> *) fun a.
String
-> Pass m tyname name uni fun a -> Pass m tyname name uni fun a
NamedPass String
name (Pass m TyName Name uni fun a -> Pass m TyName Name uni fun a)
-> Pass m TyName Name uni fun a -> Pass m TyName Name uni fun a
forall a b. (a -> b) -> a -> b
$
    (Term TyName Name uni fun a -> m (Term TyName Name uni fun a))
-> [Condition TyName Name uni fun a]
-> [BiCondition TyName Name uni fun a]
-> Pass m TyName Name uni fun a
forall (m :: * -> *) tyname name (uni :: * -> *) fun a.
(Term tyname name uni fun a -> m (Term tyname name uni fun a))
-> [Condition tyname name uni fun a]
-> [BiCondition tyname name uni fun a]
-> Pass m tyname name uni fun a
Pass (Term TyName Name uni fun a -> m (Term TyName Name uni fun a)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term TyName Name uni fun a -> m (Term TyName Name uni fun a))
-> (Term TyName Name uni fun a -> Term TyName Name uni fun a)
-> Term TyName Name uni fun a
-> m (Term TyName Name uni fun a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term TyName Name uni fun a -> Term TyName Name uni fun a
f) [PirTCConfig uni fun -> Condition TyName Name uni fun a
forall (uni :: * -> *) fun a.
(Typecheckable uni fun, GEq uni) =>
PirTCConfig uni fun -> Condition TyName Name uni fun a
Typechecks PirTCConfig uni fun
tcConfig] [Condition TyName Name uni fun a
-> BiCondition TyName Name uni fun a
forall tyname name (uni :: * -> *) fun a.
Condition tyname name uni fun a
-> BiCondition tyname name uni fun a
ConstCondition (PirTCConfig uni fun -> Condition TyName Name uni fun a
forall (uni :: * -> *) fun a.
(Typecheckable uni fun, GEq uni) =>
PirTCConfig uni fun -> Condition TyName Name uni fun a
Typechecks PirTCConfig uni fun
tcConfig)]

-- | A pass that does renaming.
renamePass
  :: (HasUnique name TermUnique, HasUnique tyname TypeUnique, MonadQuote m, Ord a)
  => Pass m tyname name uni fun a
renamePass :: forall name tyname (m :: * -> *) a (uni :: * -> *) fun.
(HasUnique name TermUnique, HasUnique tyname TypeUnique,
 MonadQuote m, Ord a) =>
Pass m tyname name uni fun a
renamePass =
  String
-> Pass m tyname name uni fun a -> Pass m tyname name uni fun a
forall (m :: * -> *) tyname name (uni :: * -> *) fun a.
String
-> Pass m tyname name uni fun a -> Pass m tyname name uni fun a
NamedPass String
"renaming" (Pass m tyname name uni fun a -> Pass m tyname name uni fun a)
-> Pass m tyname name uni fun a -> Pass m tyname name uni fun a
forall a b. (a -> b) -> a -> b
$
    (Term tyname name uni fun a -> m (Term tyname name uni fun a))
-> [Condition tyname name uni fun a]
-> [BiCondition tyname name uni fun a]
-> Pass m tyname name uni fun a
forall (m :: * -> *) tyname name (uni :: * -> *) fun a.
(Term tyname name uni fun a -> m (Term tyname name uni fun a))
-> [Condition tyname name uni fun a]
-> [BiCondition tyname name uni fun a]
-> Pass m tyname name uni fun a
Pass Term tyname name uni fun a -> m (Term tyname name uni fun a)
forall a (m :: * -> *). (Rename a, MonadQuote m) => a -> m a
forall (m :: * -> *).
MonadQuote m =>
Term tyname name uni fun a -> m (Term tyname name uni fun a)
PLC.rename [] [Condition tyname name uni fun a
-> BiCondition tyname name uni fun a
forall tyname name (uni :: * -> *) fun a.
Condition tyname name uni fun a
-> BiCondition tyname name uni fun a
ConstCondition Condition tyname name uni fun a
forall tyname name a (uni :: * -> *) fun.
(HasUnique tyname TypeUnique, HasUnique name TermUnique, Ord a) =>
Condition tyname name uni fun a
GloballyUniqueNames]

-- | A pass that does typechecking, useful when you want to do it explicitly
-- and not as part of a precondition check.
typecheckPass
  :: (TC.MonadTypeCheckPir err uni fun a m, Ord a)
  => TC.PirTCConfig uni fun
  -> Pass m TyName Name uni fun a
typecheckPass :: forall err (uni :: * -> *) fun a (m :: * -> *).
(MonadTypeCheckPir err uni fun a m, Ord a) =>
PirTCConfig uni fun -> Pass m TyName Name uni fun a
typecheckPass PirTCConfig uni fun
tcconfig = String
-> Pass m TyName Name uni fun a -> Pass m TyName Name uni fun a
forall (m :: * -> *) tyname name (uni :: * -> *) fun a.
String
-> Pass m tyname name uni fun a -> Pass m tyname name uni fun a
NamedPass String
"typechecking" (Pass m TyName Name uni fun a -> Pass m TyName Name uni fun a)
-> Pass m TyName Name uni fun a -> Pass m TyName Name uni fun a
forall a b. (a -> b) -> a -> b
$ (Term TyName Name uni fun a -> m (Term TyName Name uni fun a))
-> [Condition TyName Name uni fun a]
-> [BiCondition TyName Name uni fun a]
-> Pass m TyName Name uni fun a
forall (m :: * -> *) tyname name (uni :: * -> *) fun a.
(Term tyname name uni fun a -> m (Term tyname name uni fun a))
-> [Condition tyname name uni fun a]
-> [BiCondition tyname name uni fun a]
-> Pass m tyname name uni fun a
Pass Term TyName Name uni fun a -> m (Term TyName Name uni fun a)
run [Condition TyName Name uni fun a
forall tyname name a (uni :: * -> *) fun.
(HasUnique tyname TypeUnique, HasUnique name TermUnique, Ord a) =>
Condition tyname name uni fun a
GloballyUniqueNames] []
  where
    run :: Term TyName Name uni fun a -> m (Term TyName Name uni fun a)
run Term TyName Name uni fun a
t = do
      Normalized (Type TyName uni ())
_ <- PirTCConfig uni fun
-> Term TyName Name uni fun a
-> m (Normalized (Type TyName uni ()))
forall err (uni :: * -> *) fun ann (m :: * -> *).
MonadTypeCheckPir err uni fun ann m =>
PirTCConfig uni fun
-> Term TyName Name uni fun ann
-> m (Normalized (Type TyName uni ()))
TC.inferType PirTCConfig uni fun
tcconfig Term TyName Name uni fun a
t
      Term TyName Name uni fun a -> m (Term TyName Name uni fun a)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term TyName Name uni fun a
t