lcc/exe/eval/Main.hs

   1 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
   2 {-# LANGUAGE GADTs #-}
   3 {-# LANGUAGE NoMonomorphismRestriction #-}
   4 {-# LANGUAGE ScopedTypeVariables #-}
   5 {-# LANGUAGE UndecidableInstances #-}
   6 {-# LANGUAGE ViewPatterns #-}
   7 {-# OPTIONS_GHC -fno-warn-orphans #-}
   8 module Main where
   9
  10 import Control.Arrow (left)
  11 import Control.Applicative (Applicative(..))
  12 import Control.Monad (Monad(..), void, when)
  13 import Control.Monad.IO.Class (MonadIO(..))
  14 import Control.Monad.Trans.Class as MT (MonadTrans(..))
  15 import Data.Bool (Bool(..))
  16 import Data.Char (Char)
  17 import Data.Either (Either(..))
  18 import Data.Eq (Eq(..))
  19 import Data.Function (($), (.), id)
  20 import Data.Functor (Functor(..), (<$>))
  21 import Data.Maybe (Maybe(..), maybe)
  22 import Data.Monoid (Monoid(..))
  23 import Data.Semigroup ((<>))
  24 import Data.String (String)
  25 import Data.Text (Text)
  26 import Prelude (error, succ, Integer, undefined)
  27 import System.Console.Haskeline as HL
  28 import System.IO (IO, putStr, putStrLn, print)
  29 import Text.Show (Show(..))
  30 import qualified Control.Monad.Classes as MC
  31 import qualified Control.Monad.Classes.Run as MC
  32 import qualified Control.Monad.Trans.State.Strict as SS
  33 import qualified Data.Char as Char
  34 import qualified Data.List as L
  35 import qualified Data.Map.Strict as Map
  36 import qualified Data.Text as T
  37 import qualified Data.Text as Text
  38 import qualified Data.Text.IO as Text
  39 import qualified System.Console.Haskeline.History as HL
  40 import qualified System.IO as IO
  41 import qualified Text.Megaparsec as P
  42
  43 import Language.Symantic as Sym
  44 import qualified Language.Symantic.Document as D
  45 import qualified Language.Symantic.Grammar as G
  46 import qualified Language.Symantic.Lib as Sym
  47
  48 import qualified Hcompta.LCC.Sym as LCC.Sym
  49 import qualified Hcompta.LCC as LCC
  50 import qualified Hcompta.LCC.Lib.Strict as S
  51 import Hcompta.LCC.Read ()
  52 import Hcompta.LCC.Write (Writeable(..), context_write)
  53
  54 -- dbg :: Show a => String -> a -> a
  55 -- dbg msg x = trace (msg ++ " = " ++ show x) x
  56
  57 main :: IO ()
  58 main = do
  59         runInputT defaultSettings
  60          { historyFile    = Just ".hcompta.history"
  61          , autoAddHistory = False
  62          } $
  63                 MC.evalStateStrict evalTeUnit $
  64                 S.evalState (LCC.state_sym @LCC.Sym.SRC @(Proxy Eval ': LCC.Sym.SS)) $
  65                 unREPL $ loop True 0
  66         where
  67         loop :: forall src ss.
  68          Show src =>
  69          Syms ss Eval =>
  70          -- Syms ss View =>
  71          -- Syms ss (BetaT View) =>
  72          SymInj ss Eval =>
  73          ReadTe src ss =>
  74          Gram_Term src ss (G src ss (SS.StateT (TermVT src ss '[]) (InputT IO))) =>
  75          Bool -> Integer -> REPL src ss ()
  76         loop ok i = do
  77                 let prompt =
  78                         "\SOH\ESC["
  79                          <> (if ok then "32" else "31")
  80                          <> ";1m\STX"
  81                          <> show i
  82                          <> "\SOH\ESC[34;1m\STX>\SOH\ESC[0;48;05;233m\STX "
  83                 -- Σ
  84                 line <- readLine prompt
  85                 case line of
  86                  Nothing -> loop ok i
  87                  Just l -> do
  88                         void $ REPL $ lift $ lift $
  89                                 HL.modifyHistory $
  90                                 HL.addHistoryRemovingAllDupes l
  91                         REPL (parseTe $ Text.pack l) >>= \case
  92                          Left err -> do
  93                                 liftIO $ putStr $ P.parseErrorPretty err
  94                                 loop False (succ i)
  95                          Right expr ->
  96                                 case expr of
  97                                  Command_Def  nam ast -> runTe nam ast
  98                                  Command_Bind nam ast -> runTe nam ast
  99                                  Command_Eval     ast -> runTe "ans" ast
 100                 where
 101                 runTe nam ast =
 102                         case readTe ast of
 103                          Left err -> do
 104                                 liftIO $ print err
 105                                 loop False (succ i)
 106                          Right te -> do
 107                                 REPL $ do
 108                                         MC.modify $ \(imps::Imports NameTe, mods) ->
 109                                                 (imps, insTerm nam te mods)
 110                                         lr_r <- evalTe te
 111                                         case lr_r of
 112                                          Right r ->
 113                                                 when (nam == NameTe "base") $ MC.put r
 114                                          Left (Error_Eval_Cannot_prove_Constraint (TypeVT q)) ->
 115                                                 printTy q >>= ansiIO . ("Cannot prove Constraint: " <>)
 116                                 loop True (succ i)
 117                 insTerm ::
 118                  Sym.NameTe ->
 119                  Sym.TermVT src ss '[] ->
 120                  Sym.Modules src ss ->
 121                  Sym.Modules src ss
 122                 insTerm n t =
 123                         Sym.insertTermVT ([] `Sym.Mod` t) n $
 124                         Sym.Fixity2 Sym.infixN5
 125
 126 type instance MC.CanDo (S.StateT (LCC.State_Sym src ss) m) (MC.EffState (TermVT src ss '[])) = 'False
 127 -- type instance MC.CanDo (S.StateT (LCC.State_Sym src ss) m) (MC.EffState (EvalVT src)) = 'False
 128
 129 -- * Type 'G'
 130 type G src ss m =
 131  P.ParsecT P.Dec Text
 132            (S.StateT (LCC.State_Sym src ss) m)
 133
 134 -- * Type 'Command'
 135 data Command src ss
 136  =   Command_Eval (AST_Term src ss)
 137  |   Command_Def  NameTe (AST_Term src ss)
 138  |   Command_Bind NameTe (AST_Term src ss)
 139  deriving (Eq, Show)
 140
 141 parseTe ::
 142  forall ss src m.
 143  Monad m =>
 144  Gram_Term src ss (G src ss m) =>
 145  Text ->
 146  S.StateT (LCC.State_Sym src ss) m
 147           (Either (P.ParseError Char P.Dec) (Command src ss))
 148 parseTe = P.runParserT g ""
 149         where
 150         g :: G src ss m (Command src ss)
 151         g = G.unCF $
 152                 G.try gCmdLet G.<+>
 153                 G.try gCmdBind G.<+>
 154                 gCmdEval
 155         gCmdLet =
 156                 Command_Def
 157                  <$  G.optional (G.try $ G.symbol "let")
 158                  <*> Sym.g_NameTe
 159                  <*  G.symbol "="
 160                  <*> Sym.g_term
 161                  <*  G.eoi
 162         gCmdEval =
 163                 Command_Eval
 164                  <$> Sym.g_term
 165                  <*  G.eoi
 166         gCmdBind =
 167                 Command_Bind
 168                  <$> Sym.g_NameTe
 169                  <*  G.symbol "<-"
 170                  <*> Sym.g_term
 171                  <*  G.eoi
 172
 173 -- * Type 'ReadTe'
 174 type ReadTe src ss =
 175  ( SourceInj (TypeVT src)    src
 176  , SourceInj (KindK src)     src
 177  , SourceInj (AST_Type src)  src
 178  )
 179
 180 readTe ::
 181  forall src ss.
 182  ( Syms ss Eval
 183  -- , Syms ss View
 184  -- , Syms ss (BetaT View)
 185  , ReadTe src ss
 186  ) =>
 187  AST_Term src ss ->
 188  Either (Error_Term src) (TermVT src ss '[])
 189 readTe = Sym.readTerm CtxTyZ
 190
 191 -- | Lifted 'D.ansiIO' on 'IO.stdout'. Helper.
 192 ansiIO :: MonadIO m => D.ANSI_IO -> m ()
 193 ansiIO = liftIO . (`D.ansiIO` IO.stdout)
 194
 195 -- * Type 'Error_Eval'
 196 data Error_Eval src
 197  =   Error_Eval_Cannot_prove_Constraint (TypeVT src)
 198  deriving (Eq, Show)
 199
 200 evalTe ::
 201  forall src ss m.
 202  Source src =>
 203  Syms ss Eval =>
 204  -- Syms ss View =>
 205  -- Syms ss (BetaT View) =>
 206  SymInj ss Eval =>
 207  SourceInj (TypeVT src) src =>
 208  MonadIO m =>
 209  TermVT src ss '[] ->
 210  S.StateT (LCC.State_Sym src ss)
 211           (SS.StateT (TermVT src ss '[]) m)
 212           (Either (Error_Eval src) (TermVT src ss '[]))
 213 evalTe te@(TermVT (Term q t (TeSym sym))) = do
 214         printTy (q #> t) >>= ansiIO . ("Type: " <>)
 215         -- liftIO $ Text.putStrLn $ "View: " <> view (betaT $ sym CtxTeZ)
 216         case t of
 217          io:@aTy | Just HRefl <- proj_ConstKiTy @_ @IO io -> do
 218                 case proveConstraint q of
 219                  Nothing -> return $ Left $ Error_Eval_Cannot_prove_Constraint $ TypeVT q
 220                  Just Dict -> do
 221                         a <- liftIO $ eval $ sym CtxTeZ
 222                         let r = TermVT $ teEval_uneval aTy a
 223                         printTe aTy a
 224                         return $ Right r
 225          _ -> do
 226                 r@(TermVT (Term q' t' (TeSym sym'))) <- completeTe te
 227                 printTy (q' #> t') >>= ansiIO . ("Type: Completed: " <>)
 228                 case proveConstraint q' of
 229                  Nothing -> return $ Left $ Error_Eval_Cannot_prove_Constraint $ TypeVT q'
 230                  Just Dict -> do
 231                         let a = eval $ sym' CtxTeZ
 232                         printTe t' a
 233                         return $ Right r
 234
 235 completeTe ::
 236  forall src ss m.
 237  Source src =>
 238  Syms ss Eval =>
 239  -- Syms ss View =>
 240  -- Syms ss (BetaT View) =>
 241  SourceInj (TypeVT src) src =>
 242  MonadIO m =>
 243  TermVT src ss '[] ->
 244  S.StateT (LCC.State_Sym src ss)
 245           (SS.StateT (TermVT src ss '[]) m)
 246           (TermVT src ss '[])
 247 completeTe t = do
 248         liftIO $ putStrLn "completeTe"
 249         st :: TermVT src ss '[] <- MC.get
 250         case betaTerms $ G.BinTree0 t `G.BinTree2` G.BinTree0 st of
 251          Left _  -> do
 252                 liftIO $ putStrLn "completeTe: Left"
 253                 return t
 254          Right s -> do
 255                 liftIO $ putStrLn "completeTe: Right"
 256                 return s
 257
 258 printTy ::
 259  forall src ss m vs t d.
 260  Source src =>
 261  D.Doc_Text d =>
 262  D.Doc_Color d =>
 263  MonadIO m =>
 264  Type src vs t ->
 265  S.StateT (LCC.State_Sym src ss) m d
 266 printTy ty = do
 267         (impsTy, _ :: Sym.ModulesTy src) <- MC.get
 268         return $ Sym.docType
 269                 Sym.config_Doc_Type
 270                  { config_Doc_Type_vars_numbering = False
 271                  , config_Doc_Type_imports        = impsTy
 272                  } 0 ty <> D.eol
 273
 274 printTe :: Source src => MonadIO m => Type src vs a -> a -> m ()
 275 printTe aTy a =
 276         case proveConstraint $ LCC.Sym.tyWriteable
 277          (allocVarsR (lenVars aTy) $ LCC.Sym.tyContext_Write @_ @'[] ~> LCC.Sym.tyANSI_IO) aTy of
 278          Just Dict -> ansiIO $ write a context_write
 279          Nothing -> liftIO $
 280                 case proveConstraint $ Sym.tyShow aTy of
 281                  Nothing -> putStrLn $ "No Show instance for type: " <> show aTy
 282                  Just Dict -> do
 283                         putStrLn "Show:"
 284                         print a
 285
 286
 287 -- * Type 'REPL'
 288 -- /Read Eval Print Loop/ monad.
 289 newtype REPL src ss a
 290  =      REPL
 291  {    unREPL :: S.StateT (LCC.State_Sym src ss)
 292                          (SS.StateT (TermVT src ss '[])
 293                                     (InputT IO))
 294                          a }
 295  deriving ( Functor
 296           , Applicative
 297           , Monad
 298           , MonadIO
 299           -- , MonadState State_REPL
 300           )
 301 {-
 302 instance MonadTrans (REPL src ss) where
 303         lift = REPL . lift . lift
 304 -}
 305 type instance MC.CanDo (REPL src ss) (MC.EffState (LCC.State_Sym src ss))               = 'False
 306 type instance MC.CanDo (REPL src ss) (MC.EffState (Sym.Imports ns, Sym.Modules src ss)) = 'False
 307 type instance MC.CanDo (REPL src ss) (MC.EffState (Sym.Imports ns, Sym.ModulesTy src))  = 'False
 308 type instance MC.CanDo (REPL src ss) (MC.EffState (Sym.TermVT src ss '[]))              = 'False
 309 -- type instance MC.CanDo (REPL src ss) (MC.EffState (EvalVT src))                       = 'False
 310
 311 {-
 312 -- * Type 'State_REPL'
 313 data State_REPL src ss
 314  =   State_REPL
 315  {   state_repl_terms :: LCC.State_Sym src ss
 316  ,   state_repl_db    :: db
 317  }
 318
 319 -- State_REPL src ss db
 320 type instance MC.CanDo (S.StateT (State_REPL src ss db) m) (MC.EffState (State_REPL src ss db)) = 'True
 321 instance Monad m => MC.MonadStateN 'MC.Zero (State_REPL src ss db) (S.StateT (State_REPL src ss db) m) where
 322         stateN _px = S.StateT . SS.state
 323
 324 -- LCC.State_Sym src ss
 325 type instance MC.CanDo (S.StateT (State_REPL src ss db) m) (MC.EffState (State_REPL src ss db)) = 'True
 326 instance Monad m => MC.MonadStateN 'MC.Zero (State_REPL src ss db) (S.StateT (LCC.State_Sym src ss) m) where
 327         stateN _px f = S.StateT $ SS.state $ \st ->
 328                 (\a -> st{state_repl_terms=a}) <$> f (state_repl_terms st)
 329 -}
 330
 331
 332 readLine :: String -> REPL src ss (Maybe String)
 333 readLine prompt = do
 334         line <- REPL . lift . lift $ getInputLine prompt
 335         case line of
 336          Just l@(':':_) -> return $ Just l
 337          Just l@(_:_) | L.last l == ' ' -> readLines l
 338          Just l  -> return $ Just l
 339          Nothing -> return Nothing
 340         where
 341         readLines :: String -> REPL src ss (Maybe String)
 342         readLines acc = do
 343                 line <- REPL . lift . lift $ getInputLine ""
 344                 case line of
 345                  Just l@(_:_) | L.last l == ' ' -> readLines $ acc <> l
 346                  Just l  -> return $ Just $ acc <> l
 347                  Nothing -> return $ Just acc
 348
 349
 350
 351
 352 docModules ::
 353  Source src =>
 354  D.Doc_Text d =>
 355  D.Doc_Color d =>
 356  D.Doc_Decoration d =>
 357  ReadTe src ss =>
 358  Sym.Imports Sym.NameTy ->
 359  Sym.Modules src ss -> d
 360 docModules imps (Sym.Modules mods) =
 361         Map.foldrWithKey
 362          (\p m doc -> docModule imps p m <> doc)
 363          D.empty
 364          mods
 365
 366 docModule ::
 367  forall src ss d.
 368  Source src =>
 369  D.Doc_Text d =>
 370  D.Doc_Color d =>
 371  D.Doc_Decoration d =>
 372  ReadTe src ss =>
 373  Sym.Imports Sym.NameTy ->
 374  Sym.PathMod -> Sym.Module src ss -> d
 375 docModule imps m Sym.ByFixity
 376  { Sym.byPrefix
 377  , Sym.byInfix
 378  , Sym.byPostfix
 379  } =
 380         go docFixityInfix   byInfix <>
 381         go docFixityPrefix  byPrefix <>
 382         go docFixityPostfix byPostfix
 383         where
 384         go :: (fixy -> d) -> ModuleFixy src ss fixy -> d
 385         go docFixy =
 386                 Map.foldrWithKey
 387                  (\n Sym.Tokenizer
 388                          { Sym.token_fixity
 389                          , Sym.token_term = t
 390                          } doc ->
 391                         docPathTe m n <>
 392                         docFixy token_fixity <>
 393                         D.space <> D.bold (D.yellower "::") <> D.space <>
 394                         docTokenTerm imps (t Sym.noSource) <>
 395                         D.eol <> doc)
 396                  D.empty
 397
 398 docTokenTerm ::
 399  forall src ss d.
 400  Source src =>
 401  D.Doc_Text d =>
 402  D.Doc_Color d =>
 403  ReadTe src ss =>
 404  Sym.Imports Sym.NameTy ->
 405  Sym.Token_Term src ss -> d
 406 docTokenTerm imps t =
 407         case Sym.readTerm CtxTyZ (G.BinTree0 t) of
 408          Left{} -> error "[BUG] docTokenTerm: readTerm failed"
 409          Right (Sym.TermVT te) ->
 410                 Sym.docType Sym.config_Doc_Type
 411                  { config_Doc_Type_vars_numbering = False
 412                  , config_Doc_Type_imports        = imps
 413                  } 0 $ Sym.typeOfTerm te
 414
 415 docFixityInfix :: (D.Doc_Decoration t, D.Doc_Color t, D.Doc_Text t) => Infix -> t
 416 docFixityInfix = \case
 417          Sym.Infix Nothing 5 -> D.empty
 418          Sym.Infix a p ->
 419                 let docAssoc = \case
 420                          Sym.AssocL -> "l"
 421                          Sym.AssocR -> "r"
 422                          Sym.AssocB Sym.SideL -> "l"
 423                          Sym.AssocB Sym.SideR -> "r" in
 424                 D.magenta $ " infix" <> maybe D.empty docAssoc a <>
 425                 D.space <> D.bold (D.bluer (D.int p))
 426 docFixityPrefix :: (D.Doc_Decoration t, D.Doc_Color t, D.Doc_Text t) => Unifix -> t
 427 docFixityPrefix p = D.magenta $ " prefix "  <> D.bold (D.bluer (D.int $ Sym.unifix_prece p))
 428 docFixityPostfix :: (D.Doc_Decoration t, D.Doc_Color t, D.Doc_Text t) => Unifix -> t
 429 docFixityPostfix p = D.magenta $ " postfix " <> D.bold (D.bluer (D.int $ Sym.unifix_prece p))
 430
 431 docPathTe ::
 432  D.Doc_Text d =>
 433  D.Doc_Color d =>
 434  PathMod -> NameTe -> d
 435 docPathTe ms (NameTe n) =
 436         D.catH $
 437         L.intersperse (D.charH '.') $
 438         ((\(NameMod m) -> D.textH m) <$> ms) <>
 439         [(if isOp n then id else D.yellower) $ D.text n]
 440         where
 441         isOp = T.all $ \case '_' -> True; '\'' -> True; c -> Char.isAlphaNum c
 442
 443
 444 {-
 445 mainSym :: IO ()
 446 mainSym = do
 447         args <- Env.getArgs
 448         let sym@(LCC.State_Sym (impsTy,_modsTy) (_impsTe,patchModsTe -> modsTe)) =
 449                 LCC.state_sym @LCC.Sym.SRC @LCC.Sym.SS
 450         (`D.ansiIO` IO.stderr) $ docModules impsTy modsTe
 451         let arg = Text.unwords $ Text.pack <$> args
 452         ast <- printError $ parseTe sym arg
 453         {-
 454         ast <- (foldr1 G.BinTree2 <$>) $ forM args $ \arg -> do
 455                 printError $ parseTe sym $ Text.pack arg
 456         -}
 457         _te <- printError $ readTe ast
 458         return ()
 459         {-
 460         evalTe impsTy te
 461         forM_ args $ \arg -> do
 462                 ast <- printError $ parseTe (impsTy, modsTy) (impsTe, modsTe) $ Text.pack arg
 463                 te  <- printError $ readTe ast
 464                 evalTe impsTy te
 465         -}
 466         where
 467         patchModsTe = Sym.deleteDefTermInfix ([] `Mod` "$")
 468
 469 printError :: Show err => MonadIO m => Either err a -> m a
 470 printError (Left err) = liftIO $ error $ show err
 471 printError (Right a)  = return a
 472
 473 parseTe ::
 474  forall ss src m.
 475  m ~ Identity =>
 476  Show src =>
 477  G.Gram_Source src (G src ss m) =>
 478  Gram_Term src ss (G src ss m) =>
 479  LCC.State_Sym src ss ->
 480  Text -> Either (P.ParseError Char P.Dec) (Command src ss)
 481 parseTe sym inp =
 482         runIdentity $
 483         S.evalState sym $
 484         P.runParserT g "" inp
 485         where
 486         g :: G src ss Identity (Command src ss)
 487         g = G.unCF $
 488                 G.try (Command_Def <$> Sym.g_NameTe <* G.lexeme (G.char '=') <*> Sym.g_term <* G.eoi) G.<+>
 489                 (Command_Eval <$> Sym.g_term <* G.eoi)
 490 -}
 491
 492
 493 evalTeUnit :: Source src => SymInj ss () => TermVT src ss '[]
 494 evalTeUnit = TermVT $ Sym.teUnit -- Term noConstraint Sym.tyUnit $ teSym @() $ Sym.unit
 495
 496 {-
 497 evalTeUnit :: Source src => EvalVT src
 498 evalTeUnit = EvalVT (Sym.tyUnit @_ @'[]) $ eval Sym.unit
 499
 500 -- * Type 'EvalVT'
 501 data EvalVT src = forall vs t. EvalVT (Type src vs t) t
 502
 503 appEvalVT ::
 504  SourceInj (TypeVT src) src =>
 505  Constable (->) =>
 506  EvalVT src ->
 507  EvalVT src ->
 508  Either (Error_Beta src) (EvalVT src)
 509 appEvalVT (EvalVT tf te_fun) (EvalVT ta te_arg) =
 510         let (tf',ta') = appendVars tf ta in
 511         case unTyFun tf' of
 512          Nothing -> Left $ Error_Beta_Term_not_a_function $ TypeVT tf'
 513          Just (af,_rf) -> do
 514                 mgu <-
 515                         (Error_Beta_Unify `left`) $
 516                         case (unQualsTy af, unQualsTy ta') of
 517                          (TypeK af', TypeK ta'') -> unifyType mempty af' ta''
 518                 let tf'' = subst mgu tf'
 519                 let ta'' = subst mgu ta'
 520                 appEval tf'' te_fun ta'' te_arg $ \tr te_res ->
 521                         normalizeVarsTy tr $ \tr' ->
 522                                 EvalVT tr' te_res
 523
 524 appEval ::
 525  forall src vs fun arg ret.
 526  SourceInj (TypeVT src) src =>
 527  Constable (->) =>
 528  Type src vs fun -> fun ->
 529  Type src vs arg -> arg ->
 530  (forall res. Type src vs res -> res -> ret) ->
 531  Either (Error_Beta src) ret
 532 appEval tf fun ta arg k =
 533         case tf of
 534          a2b :@ a2b_a :@ a2b_b
 535                 | Just HRefl <- proj_ConstKiTy @(K (->)) @(->) a2b ->
 536                 case a2b_a `eqType` ta of
 537                  Nothing   -> Left $ Error_Beta_Type_mismatch (TypeVT a2b_a) (TypeVT ta)
 538                  Just Refl -> Right $ k a2b_b $ fun arg
 539          _ -> Left $ Error_Beta_Term_not_a_function $ TypeVT tf
 540 -}
 541
 542
 543
 544 -- * Class 'Sym_Eval'
 545 type instance Sym Eval = Sym_Eval
 546 class Sym_Eval term where
 547         uneval :: a -> term a
 548         default uneval :: Sym_Eval (UnT term) => Trans term => a -> term a
 549         uneval = trans . uneval
 550
 551 -- Interpreting
 552 instance Sym_Eval Eval where
 553         uneval a = Eval a
 554 {-
 555 instance Sym_Eval View where
 556         uneval = View $ \_p _v -> "()"
 557 instance (Sym_Eval r1, Sym_Eval r2) => Sym_Eval (Dup r1 r2) where
 558         uneval = uneval `Dup` uneval
 559 -}
 560
 561 -- Transforming
 562 instance (Sym_Eval term, Sym_Lambda term) => Sym_Eval (BetaT term)
 563
 564 -- Typing
 565 instance NameTyOf Eval where
 566         nameTyOf _c = [] `Mod` "Eval"
 567 instance ClassInstancesFor Eval where
 568 instance TypeInstancesFor Eval
 569 instance FixityOf Eval
 570
 571 -- Compiling
 572 instance
 573  ( SymInj ss Eval
 574  ) => Gram_Term_AtomsFor src ss g Eval where
 575 instance ModuleFor src ss Eval
 576
 577 -- ** 'Type's
 578 tyEval :: Source src => LenInj vs => Type src vs Eval
 579 tyEval = tyConst @(K Eval) @Eval
 580
 581 -- ** 'Term's
 582 teEval_uneval ::
 583  Source src => SymInj ss Eval =>
 584  Type src vs a -> a ->
 585  Term src ss ts vs (() #> a)
 586 teEval_uneval ty a =
 587         Term (noConstraintLen $ lenVars ty) ty $
 588         symInj @Eval $
 589         TeSym $ \_c -> uneval a