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