{-# 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
data Condition tyname name uni fun a where
Typechecks :: (PLC.Typecheckable uni fun, PLC.GEq uni)
=> TC.PirTCConfig uni fun -> Condition TyName Name uni fun a
GloballyUniqueNames :: (HasUnique tyname TypeUnique, HasUnique name TermUnique, Ord a)
=> Condition tyname name uni fun a
Custom :: (Term tyname name uni fun a -> Maybe (a, Text))
-> Condition tyname name uni fun a
data BiCondition tyname name uni fun a where
ConstCondition :: Condition tyname name uni fun a -> BiCondition tyname name uni fun a
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
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 ()
data Pass m tyname name uni fun a =
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
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)]
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]
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