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