after embedding

plutus-core/executables/plutus/AnyProgram/Apply.hs

@@ -13,12 +13,11 @@ import Control.Monad.Except
 
 -- | Given a singleton witness and two programs of that type witness, apply them together.
 --
--- This could alternatively be achieved by
--- using an "Appliable" typeclass + withAppliable hasomorphism
 applyProgram :: (MonadError PLC.ApplyProgramError m)
              => SLang s -> FromLang s -> FromLang s -> m (FromLang s)
 applyProgram sng p1 p2 = withSemigroupA (_sann sng) $
     case sng of
         SPir{} -> PIR.applyProgram p1 p2
         SPlc{} -> PLC.applyProgram p1 p2
         SUplc{} -> UPLC.UnrestrictedProgram <$> UPLC.applyProgram (UPLC.unUnrestrictedProgram p1) (UPLC.unUnrestrictedProgram p2)
+        SData{} -> error "FIXME: not implemented yet"

plutus-core/executables/plutus/AnyProgram/Compile.hs

@@ -1,10 +1,8 @@
 {-# LANGUAGE LambdaCase #-}
-{-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE ViewPatterns #-}
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE ImplicitParams #-}
-{-# LANGUAGE MultiParamTypeClasses #-}
 module AnyProgram.Compile
     ( compileProgram
     ) where
@@ -14,12 +12,10 @@ import GetOpt
 import AnyProgram.With
 
 import PlutusCore.Default
-import PlutusCore.Builtin qualified as PLC
 import PlutusCore qualified as PLC
 import PlutusCore.Error as PLC
 import PlutusCore.MkPlc
 import PlutusCore.DeBruijn qualified as PLC
-import PlutusCore.DeBruijn qualified as PLC
 import PlutusCore.Compiler qualified as PLC
 import PlutusIR qualified as PIR
 import PlutusIR.TypeCheck qualified as PIR
@@ -34,11 +30,13 @@ import Control.Monad.Reader
 import Control.Lens hiding ((%~))
 import Control.Monad.Except
 import Control.Monad.Error.Lens
-import Unsafe.Coerce
 
 compileProgram :: (?opts :: Opts, e ~ (PIR.Provenance (FromAnn (US_ann s1))), -- Here we use the erroring of the original term's annotation
                   MonadError (PIR.Error DefaultUni DefaultFun e) m)
-               => SLang s1 -> SLang s2 -> FromLang s1 -> m (FromLang s2)
+               => SLang s1
+               -> SLang s2
+               -> FromLang s1
+               -> m (FromLang s2)
 compileProgram = curry $ \case
     -- exclude all pir-debruijn input&output combinations
     ----------------------------------------
@@ -49,7 +47,7 @@ compileProgram = curry $ \case
 
     -- pir to plc
     ----------------------------------------
-    (sng1@(SPir n1@SName a1), SPlc n2 a2@SUnit) ->
+    (SPir n1@SName a1, SPlc n2 SUnit) ->
         -- Note: PIR.compileProgram subsumes pir typechecking
         -- prove that a1 has Ord,Pretty
         withOrdPrettyA a1 $
@@ -60,6 +58,14 @@ compileProgram = curry $ \case
             -- >=> toOutAnn a1 a2
     (SPir SName _, SPlc _ _) -> const $ throwing PIR._Error $ PIR.OptionsError "only support unit-ann output for now"
 
+    -- plc to pir (a special case of embedding, since plc is subset of pir)
+    ----------------------------------------
+    (SPlc n1 a1, SPir n2 a2) ->
+           -- MAYBE: perhaps first plc-typecheck?
+           plcToOutName n1 n2
+        >=> pure . embedProgram
+        >=> toOutAnn a1 a2
+
     -- pir to uplc
     ----------------------------------------
     (sng1@(SPir n1 a1), sng2@(SUplc n2 a2)) ->
@@ -82,10 +88,11 @@ compileProgram = curry $ \case
     ----------------------------------------
     (SPir n1@SName a1, SPir n2@SName a2) ->
         through (modifyError (fmap PIR.Original) . pirTypecheck a1)
+        -- TODO: optimise
         >=> pirToOutName n1 n2
         >=> toOutAnn a1 a2
     (SPlc n1@SName a1, SPlc n2@SName a2) ->
-        through (modifyError (fmap PIR.Original . PIR.PLCTypeError . embedPLCTypeError) . plcTypecheck a1)
+        through (modifyError (fmap PIR.Original . PIR.PLCError) . plcTypecheck n1 a1)
         >=> plcToOutName n1 n2
         >=> toOutAnn a1 a2
     (SUplc n1 a1, SUplc n2 a2) ->
@@ -96,12 +103,8 @@ compileProgram = curry $ \case
 
     (_, _) -> const $ throwing PIR._Error $ PIR.OptionsError "not implemented yet"
 
-
-embedPLCTypeError :: PLC.TypeError
-                    (PLC.Term tyname name uni1 fun1 ann1) uni2 fun2 ann2
-                  -> PLC.TypeError (PIR.Term tyname name uni1 fun1 ann1) uni2 fun2 ann2
-embedPLCTypeError (PLC.TypeMismatch arg1 t2 arg3 arg4) = TypeMismatch arg1 (embed t2) arg3 arg4
-embedPLCTypeError e = unsafeCoerce e -- FIXME: have to explicitly write all down because of semi-phantom typevar term
+embedProgram :: PLC.Program tyname name uni fun ann -> PIR.Program tyname name uni fun ann
+embedProgram (PLC.Program a v t) = PIR.Program a v $ embed t
 
 toOutAnn :: (Functor f, PIR.AsError e uni fun a, MonadError e m)
          => SAnn s1
@@ -124,49 +127,78 @@ pirTypecheck sngA p = PLC.runQuoteT $ do
     tcConfig <- withMonoidA sngA $ PIR.getDefTypeCheckConfig mempty
     void $ PIR.inferTypeOfProgram tcConfig p
 
+plcViaName :: (PLC.MonadQuote m, PLC.AsFreeVariableError e, MonadError e m)
+            => (PLC.Program PLC.TyName PLC.Name uni fun a -> m (PLC.Program PLC.TyName PLC.Name uni fun a))
+            -> SNaming n
+            -> PLC.Program (FromNameTy n) (FromName n) uni fun a
+            -> m (PLC.Program (FromNameTy n) (FromName n) uni fun a)
+plcViaName act sngN = case sngN of
+    SName -> act
+    SNamedDeBruijn -> PLC.progTerm PLC.unDeBruijnTerm
+                     >=> act
+                     >=> PLC.progTerm PLC.deBruijnTerm
+    SDeBruijn -> pure . PLC.programMapNames PLC.fakeTyNameDeBruijn PLC.fakeNameDeBruijn
+                >=> plcViaName act SNamedDeBruijn
+                >=> pure . PLC.programMapNames PLC.unNameTyDeBruijn PLC.unNameDeBruijn
+
+plcToName :: (PLC.MonadQuote m, PLC.AsFreeVariableError e, MonadError e m)
+          => (PLC.Program PLC.TyName PLC.Name uni fun a -> m x)
+          -> SNaming n
+          -> (PLC.Program (FromNameTy n) (FromName n) uni fun a -> m x)
+plcToName act sngN = case sngN of
+    SName -> act
+    SNamedDeBruijn -> PLC.progTerm PLC.unDeBruijnTerm
+                      >=> act
+    SDeBruijn -> pure . PLC.programMapNames PLC.fakeTyNameDeBruijn PLC.fakeNameDeBruijn
+                >=> plcToName act SNamedDeBruijn
+
+uplcViaName :: (PLC.MonadQuote m, PLC.AsFreeVariableError e, MonadError e m)
+            => (UPLC.Program PLC.Name uni fun a -> m (UPLC.Program PLC.Name uni fun a))
+            -> SNaming n
+            -> UPLC.Program (FromName n) uni fun a
+            -> m (UPLC.Program (FromName n) uni fun a)
+uplcViaName act sngN = case sngN of
+    SName -> act
+    SNamedDeBruijn -> UPLC.progTerm UPLC.unDeBruijnTerm
+                    >=> act
+                    >=> UPLC.progTerm UPLC.deBruijnTerm
+    SDeBruijn -> pure . UPLC.programMapNames UPLC.fakeNameDeBruijn
+                >=> uplcViaName act SNamedDeBruijn
+                >=> pure . UPLC.programMapNames UPLC.unNameDeBruijn
+
 plcTypecheck :: (PLC.AsTypeError
                           e
-                          (PLC.Term UPLC.TyName UPLC.Name DefaultUni DefaultFun ())
+                          -- errors remain with names
+                          (PLC.Term PLC.TyName PLC.Name DefaultUni DefaultFun ())
                           DefaultUni
                           DefaultFun
-                          (FromAnn a), MonadError e m)
-             => SAnn a
-             -> PLC.Program PLC.TyName PLC.Name DefaultUni DefaultFun (FromAnn a)
+                          (FromAnn a)
+               , PLC.AsFreeVariableError e
+               , MonadError e m
+               )
+             => SNaming n
+             -> SAnn a
+             -> PLC.Program (FromNameTy n) (FromName n) DefaultUni DefaultFun (FromAnn a)
              -> m ()
-plcTypecheck sngA p = PLC.runQuoteT $ do
+plcTypecheck sngN sngA p = PLC.runQuoteT $ do
     tcConfig <- withMonoidA sngA $ PLC.getDefTypeCheckConfig mempty
-    void $ PLC.inferTypeOfProgram tcConfig p
+    void $ plcToName (PLC.inferTypeOfProgram tcConfig) sngN p
 
 uplcOptimise :: (?opts :: Opts, PLC.AsFreeVariableError e, MonadError e m)
              => SNaming n1
              -> UPLC.UnrestrictedProgram (FromName n1) DefaultUni DefaultFun a
              -> m (UPLC.UnrestrictedProgram (FromName n1) DefaultUni DefaultFun a)
-uplcOptimise sngN =
+uplcOptimise =
     case _optimiseLvl ?opts of
-        -- short-circuit to avoid renaming
-        NoOptimise -> pure
+        NoOptimise -> const pure -- short-circuit to avoid renaming
         safeOrUnsafe ->
                 let sOpts = UPLC.defaultSimplifyOpts &
                                 case safeOrUnsafe of
                                   SafeOptimise -> set UPLC.soConservativeOpts True
                                   UnsafeOptimise -> id
-                in PLC.runQuoteT . (_Wrapped $ uplcOptimiseWith sOpts sngN)
-
--- | Optimise using given `UPLC.SimplifyOpts`
-uplcOptimiseWith :: (PLC.AsFreeVariableError e, MonadError e m, PLC.MonadQuote m)
-                 => UPLC.SimplifyOpts PLC.Name a
-                 -> SNaming n1
-                 -> UPLC.Program (FromName n1) DefaultUni DefaultFun a
-                 -> m (UPLC.Program (FromName n1) DefaultUni DefaultFun a)
-uplcOptimiseWith sOpts = \case
-    SName ->  UPLC.simplifyProgram sOpts
-    SNamedDeBruijn ->
-                UPLC.progTerm UPLC.unDeBruijnTerm
-            >=> uplcOptimiseWith sOpts SName
-            >=> UPLC.progTerm UPLC.deBruijnTerm
-    SDeBruijn -> pure . UPLC.programMapNames UPLC.fakeNameDeBruijn
-                >=> uplcOptimiseWith sOpts SNamedDeBruijn
-                >=> pure . UPLC.programMapNames UPLC.unNameDeBruijn
+                in fmap PLC.runQuoteT
+                   . _Wrapped
+                   . uplcViaName (UPLC.simplifyProgram sOpts)
 
 -- | We do not have a typechecker for uplc, but we could pretend that scopecheck is a "typechecker"
 uplcTypecheck :: forall sN sA uni fun e m

plutus-core/executables/plutus/AnyProgram/IO.hs

@@ -56,12 +56,12 @@ prettyWithStyle = \case
 
 readFileName :: FileName -> IO BS.ByteString
 readFileName = \case
-    StdOut -> fail "should not happen"
+    StdOut -> failE "should not happen"
     StdIn -> BS.hGetContents stdin
     AbsolutePath fp -> BS.readFile fp
 
 writeFileName :: FileName -> BS.ByteString -> IO ()
 writeFileName fn bs = case fn of
-    StdIn -> fail "should not happen"
+    StdIn -> failE "should not happen"
     StdOut -> BS.hPutStr stdout bs
     AbsolutePath fp -> BS.writeFile fp bs

plutus-core/executables/plutus/AnyProgram/Parse.hs

@@ -5,6 +5,7 @@ module AnyProgram.Parse
 
 import PlutusPrelude hiding ((%~))
 import Types
+import Common
 
 import PlutusCore.Error as PLC
 import PlutusCore.Quote as PLC
@@ -32,15 +33,16 @@ parseProgram s bs =
                           SPir{} -> PIR.parseProgram bs
                           SPlc{} -> PLC.parseProgram bs
                           SUplc{} -> UPLC.UnrestrictedProgram <$> UPLC.parseProgram bs
+                          SData{} -> error "FIXME: not implemented yet"
             SUnit ->
                 -- TODO: deduplicate
                 pure $ unsafeFromRight @PLC.ParserErrorBundle $ PLC.runQuoteT $
                       case s of
                           SPir{} -> void <$> PIR.parseProgram bs
                           SPlc{} -> void <$> PLC.parseProgram bs
                           SUplc{} -> void <$> UPLC.UnrestrictedProgram <$> UPLC.parseProgram bs
-
-            SCoverage -> fail "cannot parse coverage"
-        _ -> fail "cannot parse non name"
+                          SData{} -> error "FIXME: not implemented yet"
+            SCoverage -> failE "cannot parse coverage"
+        _ -> failE "cannot parse non name"
 
 

plutus-core/executables/plutus/AnyProgram/With.hs

@@ -1,5 +1,3 @@
-{-# LANGUAGE TypeSynonymInstances #-}
-{-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE RankNTypes #-}
 -- | BOILERPLATE needed to support Hasochism.
 module AnyProgram.With where
@@ -11,7 +9,6 @@ import PlutusCore.Pretty qualified as PLC
 import Types
 import Prettyprinter
 import Flat
-import PlutusPrelude
 
 withShowL :: forall s r. SLang s ->  (Show (FromLang s) => r) -> r
 withShowL s r = case s of

plutus-core/executables/plutus/Common.hs

@@ -9,7 +9,7 @@ import System.Exit
 printE :: Show a => a -> IO ()
 printE = hPutStrLn stderr . show
 
--- like fail , just no wrtap it with user error
+-- like fail , just no wrap it with the text "user error"
 failE :: Show a => a -> IO b
 failE a = do
     printE a

plutus-core/executables/plutus/GetOpt.hs

@@ -12,6 +12,7 @@ module GetOpt
     ) where
 
 import Types
+import Common
 
 import PlutusPrelude
 import Control.Monad
@@ -36,7 +37,7 @@ parseArgs :: [String] -> IO Opts
 parseArgs args = do
     let (getOptRes, _, getOptErrMsgs) = GetOpt.getOpt (GetOpt.ReturnInOrder fromNonDash) optDescrs args
 
-    when (not $ null getOptErrMsgs) $ fail $ fold getOptErrMsgs
+    when (not $ null getOptErrMsgs) $ failE $ fold getOptErrMsgs
 
     -- MAYBE: I could make --stdout completely implicit when getOptRes.output==Nothing
     -- MAYBE: I could make --stdin sometimes implicit, when getOptRes.inputs=[], and allow it explicitly

plutus-core/executables/plutus/Main.hs

@@ -1,5 +1,5 @@
-{-# LANGUAGE RecordWildCards #-}
 {-# LANGUAGE ImplicitParams #-}
+module Main where
 
 import Types
 import GetOpt

plutus-core/executables/plutus/Mode/Compile.hs

@@ -21,8 +21,8 @@ import Prettyprinter
 runCompile :: (?opts :: Opts)
            => IO SomeAst
 runCompile = case ?opts of
-    Opts {_inputs = []} -> fail "No input file given. Use --stdin if you want to read program from stdin. See also --help"
-    Opts {_output = Nothing} -> fail "No output file given. Use --stdout to write program to stdout"
+    Opts {_inputs = []} -> failE "No input file given. Use --stdin if you want to read program from stdin. See also --help"
+    Opts {_output = Nothing} -> failE "No output file given. Use --stdout to write program to stdout"
     Opts {_inputs = (hd:tl), _output = Just (SomeFile sngT fileT)} -> do
         hdT <- readCompile hd sngT
         astT <- foldlM (readCompileApply sngT) hdT tl

plutus-core/executables/plutus/Mode/PrintSamples.hs

@@ -2,5 +2,7 @@ module Mode.PrintSamples
     ( runPrintSamples
     ) where
 
+import Common
+
 runPrintSamples :: IO ()
-runPrintSamples = fail "not implemented"
+runPrintSamples = failE "not implemented"

plutus-core/executables/plutus/Mode/PrintUni.hs

@@ -2,5 +2,7 @@ module Mode.PrintUni
     ( runPrintUni
     ) where
 
+import Common
+
 runPrintUni :: IO ()
-runPrintUni = fail "not implemented"
+runPrintUni = failE "not implemented"

plutus-core/executables/plutus/Types.hs

@@ -1,5 +1,4 @@
 {-# LANGUAGE TypeFamilyDependencies #-}
-{-# LANGUAGE OverloadedStrings #-}
 {-# OPTIONS_GHC -fno-warn-redundant-constraints #-}
 
 -- all following needed for singletons-th
@@ -61,7 +60,7 @@ data FileName = AbsolutePath FilePath
               | StdOut
               deriving stock (Eq, Show)
 
--- indexed by the lang
+-- tagged by the lang
 data File (l :: Lang) = File
     { _fType :: FileType
     , _fName :: FileName