calculus/Calculus/Lambda/Omega/Explicit/REPL.hs

   1 {-# LANGUAGE ExistentialQuantification #-}
   2 {-# LANGUAGE FlexibleContexts #-}
   3 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
   4 {-# LANGUAGE NamedFieldPuns #-}
   5 {-# LANGUAGE NoImplicitPrelude #-}
   6 {-# LANGUAGE OverloadedStrings #-}
   7 {-# LANGUAGE Rank2Types #-}
   8 {-# LANGUAGE ScopedTypeVariables #-}
   9 {-# LANGUAGE StandaloneDeriving #-}
  10 {-# LANGUAGE TupleSections #-}
  11 {-# LANGUAGE ViewPatterns #-}
  12 {-# OPTIONS_GHC -fno-warn-tabs #-}
  13 module Calculus.Lambda.Omega.Explicit.REPL where
  14
  15 import Control.Applicative (Applicative(..), (<$>))
  16 import Control.Exception
  17 import Control.Monad
  18 import Control.Monad.State
  19 import Data.Bool
  20 import qualified Data.Char as Char
  21 import Data.Either (Either(..))
  22 import Data.Eq (Eq(..))
  23 import Data.Foldable (Foldable(..))
  24 import Data.Function (($), (.), const, flip)
  25 import Data.Functor.Identity
  26 import Data.List ((++), break, concat, dropWhile, last, reverse)
  27 import Data.List (isPrefixOf, find)
  28 import qualified Data.List as List
  29 import Data.Map.Strict (Map)
  30 import qualified Data.Map.Strict as Map
  31 import Data.Maybe (Maybe(..))
  32 import Data.Monoid ((<>))
  33 import Data.Monoid (Monoid(..))
  34 import Data.Ord (Ord(..))
  35 import Data.String (String)
  36 import Data.Text (Text)
  37 import qualified Data.Text as Text
  38 import Data.Text.Buildable (Buildable(..))
  39 import qualified Data.Text.Lazy as TL
  40 import qualified Data.Text.Lazy.Builder as Builder
  41 import Data.Tuple (fst)
  42 import Data.Typeable as Typeable
  43 import Prelude (Integer, Num(..), div, error)
  44 import System.Console.Haskeline
  45 import System.Directory
  46 import System.FilePath
  47 import System.IO (IO, readFile)
  48 import qualified Text.Parsec as R
  49 import Text.Show (Show(..))
  50
  51 -- import Debug.Trace
  52
  53 import Calculus.Abstraction.DeBruijn.Generalized
  54 import Calculus.Lambda.Omega.Explicit
  55 import Calculus.Lambda.Omega.Explicit.Read
  56
  57 -- * Type 'REPL'
  58
  59 -- | /Read Eval Print Loop/ monad.
  60 newtype REPL a
  61  =      REPL
  62  {    unREPL :: StateT REPL_State (InputT IO) a }
  63  deriving ( Functor
  64           , Applicative
  65           , Monad
  66           , MonadIO
  67           , MonadState REPL_State )
  68
  69 data REPL_State
  70  =   REPL_State
  71  {   repl_state_env       :: Env
  72  ,   repl_state_load_dir  :: FilePath
  73  ,   repl_state_load_done :: Map FilePath ()
  74  }
  75
  76 main :: IO ()
  77 main = do
  78         cwd <- getCurrentDirectory
  79         runInputT defaultSettings $
  80                 evalStateT (unREPL main_loop) $
  81                 REPL_State
  82                  { repl_state_env       = prelude axioms
  83                  , repl_state_load_dir  = cwd
  84                  , repl_state_load_done = mempty
  85                  }
  86         where
  87         main_loop :: REPL ()
  88         main_loop = do
  89                 let prompt = "> "
  90                 line <- repl_read_command prompt
  91                 case slice <$> line of
  92                  Just (cmd, input) | (not (length cmd > 1 && cmd `isPrefixOf` "quit")) ->
  93                         dispatch cmd input
  94                  _ -> return ()
  95                 main_loop
  96
  97 slice :: String -> (String, String)
  98 slice (':':str) = break Char.isSpace str
  99 slice str       = ("", str)
 100
 101
 102 -- ** I/O
 103 print :: Buildable a => a -> TL.Text
 104 print = Builder.toLazyText . build
 105
 106 repl_write_string_ln :: String -> REPL ()
 107 repl_write_string_ln = REPL . lift . outputStrLn
 108
 109 repl_write_string :: String -> REPL ()
 110 repl_write_string = REPL . lift . outputStr
 111
 112 repl_show :: Show a => a -> REPL ()
 113 repl_show = repl_write_string_ln . show
 114
 115 repl_print :: Buildable a => a -> REPL ()
 116 repl_print = repl_write_string . TL.unpack . print
 117
 118 repl_print_ln :: Buildable a => a -> REPL ()
 119 repl_print_ln = repl_write_string_ln . TL.unpack . print
 120
 121 repl_read :: Parser Identity x -> String -> (x -> REPL ()) ->  REPL ()
 122 repl_read _p [] _k = return ()
 123 repl_read p s k =
 124         case runIdentity $ read p s of
 125          Right x -> k x
 126          Left err -> do
 127                 repl_write_string_ln "Parsing error:"
 128                 repl_show err
 129                 repl_write_string " Command_Input: "
 130                 repl_write_string_ln s
 131
 132 -- ** Commands
 133 repl_read_command :: String -> REPL (Maybe String)
 134 repl_read_command prompt = do
 135         line <- REPL . lift $ getInputLine prompt
 136         case line of
 137          Just s@(':':_) -> return $ Just s
 138          Just l@(_:_) | last l == ' ' -> parse_block l
 139          Just s -> return $ Just s
 140          Nothing -> return Nothing
 141         where
 142         parse_block :: String -> REPL (Maybe String)
 143         parse_block s = do
 144                 line <- REPL . lift $ getInputLine ""
 145                 case line of
 146                  Just l@(_:_) | last l == ' ' -> parse_block (s ++ '\n' : l)
 147                  _ -> return $ Just s
 148
 149 type Command_Name = String
 150 type Command = Command_Input -> IO Command_Output
 151
 152 command :: Command_Name -> Command
 153 command "" = command "let"
 154 command cmd =
 155         case find (\p -> cmd `isPrefixOf` fst p) commands of
 156          Nothing -> (\_ -> return $ Left $ Error_Command cmd)
 157          Just (_, c) -> c
 158         where
 159         commands :: [(String, Command)]
 160         commands =
 161          [ ("assume", command_assume) -- Type -> IO ()
 162          , ("code" , command_code) -- Var -> Term
 163          , ("dump" , command_dump) -- Term -> Text
 164          , ("equiv", command_equiv) -- Term -> Term -> Bool
 165          -- , ("echo" , command_echo) -- Term -> Term
 166          , ("let"  , command_let) -- Var -> Term -> IO ()
 167          , ("load" , command_load) -- FilePath -> IO ()
 168          , ("nf"   , command_normalize normalize) -- Term -> Term
 169          , ("nf_dump", command_normalize_dump normalize) -- Term -> Term
 170          , ("reset", command_reset) -- () -> IO ()
 171          , ("type" , command_type) -- Term -> Type
 172          , ("type_dump", command_type_dump) -- Term -> Text
 173          , ("whnf" , command_normalize whnf) -- Term -> Term
 174          ]
 175 command_run :: Command_Name -> Command
 176 command_run cmd (Command_Input i st) = do
 177         command cmd $
 178                 Command_Input (strip_spaces i) st
 179         where
 180         strip_spaces =
 181                 reverse . dropWhile Char.isSpace .
 182                 reverse . dropWhile Char.isSpace
 183
 184 dispatch :: Command_Name -> String -> REPL ()
 185 dispatch cmd i = do
 186         st <- get
 187         output <- liftIO $ command_run cmd (Command_Input i st)
 188         case output of
 189          Left (err::Error) ->
 190                 repl_print err
 191          Right (Command_Result msg new_st) -> do
 192                 case TL.unpack $ print msg of
 193                  [] -> return ()
 194                  o -> repl_write_string_ln o
 195                 put new_st
 196
 197 data Command_Input
 198  =   Command_Input String REPL_State
 199 type Command_Output
 200  = Either Error Command_Result
 201 data Error
 202  =   Error_Parse String R.ParseError
 203  |   Error_Type Type_Error
 204  |   Error_Let  Var_Name Type_Error
 205  |   Error_Code Var_Name
 206  |   Error_Command Command_Name
 207  |   Error_IO IOException
 208  |   Error_Load FilePath Error
 209  deriving (Show)
 210 instance Buildable Error where
 211         build err =
 212                 case err of
 213                  Error_Parse s e -> "Error: parsing: " <> build s <> "\n" <> build (show e) <> "\n"
 214                  Error_Type e -> build e
 215                  Error_Let var e -> "Error: in let: " <> build var <> "\n " <> build e
 216                  Error_Code var -> "Error: no such variable in environment: " <> build var
 217                  Error_Command cmd -> "Error: unrecognized command: " <> build cmd <> "\n"
 218                  Error_IO e -> "Error: " <> build (show e) <> "\n"
 219                  Error_Load file e ->
 220                         "Error: loading: " <> build file <> "\n"
 221                         <> build e
 222 data Command_Result
 223  =   forall msg.
 224      ( Buildable msg
 225      ) => Command_Result msg REPL_State
 226
 227 command_assume :: Command
 228 command_assume (Command_Input str st) =
 229         return $
 230         let ctx = context_from_env $ repl_state_env st in
 231         case runIdentity $ read parse_assume str of
 232          Left err -> Left $ Error_Parse str err
 233          Right (v, ty) ->
 234                 case type_of ctx ty of
 235                         Left err -> Left $ Error_Type err
 236                         Right _ty_ty -> Right $
 237                                 Command_Result (""::Text) $
 238                                         st{repl_state_env = env_insert v
 239                                                  (TeTy_Axiom (Axiom_Type_Assume ty)) ty $
 240                                                 repl_state_env st
 241                                          }
 242
 243 command_code :: Command
 244 command_code (Command_Input str st) =
 245         return $
 246         let env = repl_state_env st in
 247         case runIdentity $ read parse_var_name str of
 248          Left err -> Left $ Error_Parse str err
 249          Right var ->
 250                 case Map.lookup var env of
 251                  Nothing -> Left $ Error_Code var
 252                  Just item -> Right $ Command_Result
 253                          (form_given $ env_item_term item)
 254                          st
 255
 256 command_dump :: Command
 257 command_dump (Command_Input str st) =
 258         return $
 259                 case runIdentity $ read parse_term str of
 260                  Left err -> Left $ Error_Parse str err
 261                  Right te -> Right $ Command_Result (show te) st
 262
 263 command_let :: Command
 264 command_let (Command_Input [] st) =
 265         return $ Right $ Command_Result (""::Text) st
 266 command_let (Command_Input str st) =
 267         let toks_or_err = runIdentity $ lex lex_all str in
 268         case toks_or_err of
 269          Left err -> return $ Left $ Error_Parse str err
 270          Right [] -> return $ Right $ Command_Result (""::Text) st
 271          Right toks ->
 272                 case runIdentity $ parse parse_let_or_term toks of
 273                  Left err -> return $ Left $ Error_Parse str err
 274                  Right let_or_term -> do
 275                         let ctx = context_from_env $ repl_state_env st
 276                         case let_or_term of
 277                          Left (v, mty, te) ->
 278                                 let ety = case mty of
 279                                          Nothing -> type_of ctx te
 280                                          Just ty -> do
 281                                                 _ty_ty <- type_of ctx ty
 282                                                 const ty <$> check ctx (context_apply ctx ty) te
 283                                  in
 284                                 return $
 285                                 case ety of
 286                                  Left err -> Left $ Error_Let v err
 287                                  Right ty -> do
 288                                         Right $ Command_Result (build v <> " : " <> build ty) $
 289                                                 st{repl_state_env = env_insert v te ty $ repl_state_env st}
 290                          Right let_te ->
 291                                 case type_of ctx let_te of
 292                                  Left err -> return $ Left $ Error_Type err
 293                                  Right _ty ->
 294                                         let norm_te = normalize ctx let_te in
 295                                         case norm_te of
 296                                          TeTy_Axiom (axiom_cast -> Just (Axiom_Term (io::IO (Term Var_Name)) _o_ty)) -> do
 297                                                 io_te <- io
 298                                                 return $ Right $ Command_Result io_te st
 299                                          _ ->
 300                                                 return $ Right $ Command_Result norm_te st
 301
 302 command_load :: Command
 303 command_load (Command_Input file input_st) = do
 304         err_or_io <- try $ do
 305                 path <- canonicalizePath (repl_state_load_dir input_st </> file)
 306                 content <- readFile path
 307                 return (path, content)
 308         case err_or_io of
 309          Left (err::IOException) -> return $ Left $ Error_IO err
 310          Right (modul, content) -> do
 311                 case Map.lookup modul $ repl_state_load_done input_st of
 312                  Just _ -> return $ Right $
 313                         Command_Result ("Module already loaded: " ++ modul) input_st
 314                  _ ->
 315                         case runIdentity $ R.runParserT (parse_commands <* R.eof) () modul content of
 316                          Left err -> return $ Left $ Error_Load modul $ Error_Parse content err
 317                          Right cmds -> do
 318                                 let old_dir = repl_state_load_dir input_st
 319                                 err_or_st <-
 320                                         foldM (\err_or_st (cmd, i) ->
 321                                                 case err_or_st of
 322                                                  Left _ -> return $ err_or_st
 323                                                  Right (Command_Result last_msg last_st) -> do
 324                                                         o <- command_run cmd (Command_Input i last_st)
 325                                                         case o of
 326                                                          Left _ -> return o
 327                                                          Right (Command_Result msg running_st) ->
 328                                                                 return $ Right $
 329                                                                         Command_Result (build last_msg <> "\n" <> build msg) running_st
 330                                          )
 331                                          (Right $ Command_Result ("Loading: " <> modul)
 332                                                  input_st{repl_state_load_dir = takeDirectory modul})
 333                                          ({-trace ("cmds: " ++ show cmds)-} cmds)
 334                                 return $
 335                                         case err_or_st of
 336                                          Left err -> Left $ Error_Load modul $ err
 337                                          Right (Command_Result msg result_st) ->
 338                                                 Right $ Command_Result msg $ result_st
 339                                                  { repl_state_load_dir  = old_dir
 340                                                  , repl_state_load_done =
 341                                                         Map.insert modul () $
 342                                                         repl_state_load_done result_st
 343                                                  }
 344
 345 command_normalize
 346  :: (Context Var_Name -> Term Var_Name -> Term Var_Name)
 347  -> Command
 348 command_normalize norm (Command_Input str st) = do
 349         let ctx = context_from_env $ repl_state_env st
 350         case runIdentity $ read parse_term str of
 351          Left err -> return $ Left $ Error_Parse str err
 352          Right (te::Term Var_Name) ->
 353                 let n_te = norm ctx te in
 354                 case n_te of
 355                  TeTy_Axiom (axiom_cast -> Just (Axiom_Term (o::IO (Term Var_Name)) _o_ty)) -> do
 356                         r <- o
 357                         return $ Right $ Command_Result r st
 358                  TeTy_Axiom (axiom_cast -> Just (Axiom_Term (o::IO Text) _o_ty)) -> do
 359                         r <- o
 360                         return $ Right $ Command_Result r st
 361                  _ ->
 362                         return $ Right $ Command_Result n_te st
 363
 364 command_equiv :: Command
 365 command_equiv (Command_Input str st) = do
 366         let ctx = context_from_env $ repl_state_env st
 367         return $
 368                 case runIdentity $ read ((,) <$> parse_term <* (parse_token Token_Equal >> parse_token Token_Equal) <*> parse_term) str of
 369                  Left err -> Left $ Error_Parse str err
 370                  Right (x_te, y_te) -> Right $
 371                         Command_Result (if equiv ctx x_te y_te then "True" else "False"::Text) st
 372
 373 command_normalize_dump
 374  :: (Context Var_Name -> Term Var_Name -> Term Var_Name)
 375  -> Command
 376 command_normalize_dump norm (Command_Input str st) = do
 377         let ctx = context_from_env $ repl_state_env st
 378         return $
 379                 case runIdentity $ read parse_term str of
 380                  Left err -> Left $ Error_Parse str err
 381                  Right te -> Right $ Command_Result (show $ norm ctx te) st
 382
 383 command_reset :: Command
 384 command_reset (Command_Input _ st) =
 385         return $ Right $
 386                 Command_Result (""::Text) st{repl_state_env = mempty}
 387
 388 command_type :: Command
 389 command_type (Command_Input [] st) = do
 390         let env = repl_state_env st
 391         return $
 392                 Right $ Command_Result
 393                  (
 394                         foldr (flip (<>)) "" $
 395                         List.intersperse "\n" $
 396                          (\(name, item) ->
 397                                 build name <> " : "
 398                                  <> build (form_given $ env_item_type item))
 399                          <$> (Map.toList env)
 400                  )
 401                  st
 402 command_type (Command_Input str st) = do
 403         let ctx = context_from_env $ repl_state_env st
 404         return $
 405                 case runIdentity $ read parse_term str of
 406                  Left err -> Left $ Error_Parse str err
 407                  Right te ->
 408                         case type_of ctx te of
 409                          Left err -> Left $ Error_Type err
 410                          Right ty -> Right $ Command_Result (normalize ctx ty) st
 411
 412 command_type_dump :: Command
 413 command_type_dump (Command_Input [] st) = do
 414         let env = repl_state_env st
 415         return $
 416                 Right $ Command_Result
 417                  (
 418                         foldr (flip (<>)) "" $
 419                         List.intersperse "\n" $
 420                          (\(name, item) ->
 421                                 build name <> " : "
 422                                  <> build (show $ form_given $ env_item_type item))
 423                          <$> (Map.toList env)
 424                  )
 425                  st
 426 command_type_dump (Command_Input str st) = do
 427         let ctx = context_from_env $ repl_state_env st
 428         return $
 429                 case runIdentity $ read parse_term str of
 430                  Left err -> Left $ Error_Parse str err
 431                  Right te ->
 432                         case type_of ctx te of
 433                          Left err -> Left $ Error_Type err
 434                          Right ty -> Right $ Command_Result (show $ normalize ctx ty) st
 435
 436 {-
 437 command_echo :: String -> REPL ()
 438 command_echo str =
 439         repl_read parse_term str repl_print_ln
 440 -}
 441
 442 -- * Builtins
 443
 444 builtin :: Axioms -> [Text] -> Env
 445 builtin =
 446         foldl $ \env str ->
 447                 let ctx = context_from_env env in
 448                 read_string parse_let str $ \(v, mty, te) ->
 449                         let ety = case mty of
 450                                  Just ty -> do
 451                                         _ty_ty <- type_of ctx ty
 452                                         const ty <$> check ctx (context_apply ctx ty) te
 453                                  Nothing -> type_of ctx te in
 454                         case ety of
 455                          Left err -> error $ show err
 456                          Right ty -> env_insert v te ty env
 457         where
 458         read_string p s k =
 459                 case runIdentity $ read p s of
 460                  Right x -> k x
 461                  Left err -> error $
 462                          "Parsing_error:\n" ++ show err
 463                          ++ " Input: " ++ Text.unpack s
 464
 465 axioms :: Axioms
 466 axioms =
 467         (axioms_monopoly <>) $
 468         (Map.fromList axioms_io <>) $
 469         (Map.fromList axioms_int <>) $
 470         (Map.fromList axioms_text <>) $
 471         Map.fromList
 472          [ ("Unit", item $ Axiom_Type_Unit)
 473          ]
 474         where
 475         item :: (Axiomable (Axiom ax), Typeable ax) => Axiom ax -> Env_Item
 476         item = env_item_from_axiom context
 477         {-
 478         axioms_arr =
 479          [ -- ("Arr", item $ Axiom_Term_Abst)
 480          ]
 481         -}
 482         axioms_text =
 483          [ ("Text"      , item $ Axiom_Type_Text)
 484          , ("text_empty", item $ axiom_term (""::Text))
 485          , ("text_hello", item $ axiom_term ("Hello World!"::Text))
 486          ]
 487         axioms_int =
 488          [ ("Int"      , item $ Axiom_Type_Integer)
 489          , ("int_zero" , item $ axiom_term (0::Integer))
 490          , ("int_one"  , item $ axiom_term (1::Integer))
 491          , ("int_add"  , item $ axiom_term ((+)::Integer -> Integer -> Integer))
 492          , ("int_neg"  , item $ axiom_term (negate::Integer -> Integer))
 493          , ("int_sub"  , item $ axiom_term ((-)::Integer -> Integer -> Integer))
 494          , ("int_mul"  , item $ axiom_term ((*)::Integer -> Integer -> Integer))
 495          , ("int_div"  , item $ axiom_term (div::Integer -> Integer -> Integer))
 496          ]
 497         axioms_io =
 498          [ ("IO"       , item $ (Axiom_Type_IO::Axiom (IO A)))
 499          , ("return_io", item $ return_io)
 500          , ("bind_io"  , item $ bind_io)
 501          , ("join_io"  , item $ join_io)
 502          -- , ("return_io_text", item $ axiom_term $ (return::Text -> IO Text))
 503          -- , ("return_io_int", item $ Axiom_Term $ (return::Int -> IO Int))
 504          ]
 505                 where
 506                 -- | @return_io : ∀(A:*) -> A -> IO A@
 507                 return_io :: Axiom (Axiom_Type_Abst)
 508                 return_io =
 509                         Axiom_Type_Abst "A" (TeTy_Axiom . ax_te) ax_ty
 510                         where
 511                                 ax_te :: Type Var_Name
 512                                  -> Axiom (Axiom_Term (Term Var_Name -> IO (Term Var_Name)))
 513                                 ax_te ty = Axiom_Term return (\ctx -> context_lift ctx <$> ty)
 514                                 ax_ty :: Abstraction (Suggest Var_Name) Type Var_Name
 515                                 ax_ty =
 516                                         (("A" =?) `abstract`) $
 517                                         axiom_type_of context $
 518                                         axiom_term (return::A -> IO A)
 519
 520                 -- | @bind_io : ∀(A:*) -> ∀(B:*) -> IO A -> (A -> IO B) -> IO B@
 521                 bind_io :: Axiom Axiom_Type_Abst
 522                 bind_io = ax1_te
 523                         where
 524                                 ax1_te :: Axiom Axiom_Type_Abst
 525                                 ax1_te =
 526                                         Axiom_Type_Abst "A"
 527                                          (\(Type_Abst _ _ ty_a_abst) ->
 528                                                 TeTy_Axiom $
 529                                                 Axiom_Type_Abst "B"
 530                                                  (TeTy_Axiom . ax0_te)
 531                                                  ty_a_abst)
 532                                          ax1_ty
 533                                 ax1_ty =
 534                                         (("A" =?) `abstract`) $
 535                                         Type_Abst "B"
 536                                          (Type_Sort (Type_Level_0, Type_Morphism_Mono)) $
 537                                          ax0_ty
 538
 539                                 ax0_te
 540                                  :: Type Var_Name
 541                                  -> Axiom (Axiom_Term
 542                                          (  IO (Term Var_Name)
 543                                          -> (Term Var_Name -> IO (Term Var_Name))
 544                                          -> IO (Term Var_Name)
 545                                          ))
 546                                 ax0_te ty =
 547                                         Axiom_Term (>>=) (\ctx -> context_lift ctx <$> ty)
 548                                 ax0_ty =
 549                                         (("B" =?) `abstract`) $
 550                                         axiom_type_of context $
 551                                         axiom_term ((>>=)::IO A -> (A -> IO B) -> IO B)
 552
 553                 -- | @join_io : ∀(A:*) -> IO (IO A) -> IO A@
 554                 join_io :: Axiom Axiom_Type_Abst
 555                 join_io = ax1_te
 556                         where
 557                                 ax1_te :: Axiom Axiom_Type_Abst
 558                                 ax1_te =
 559                                         Axiom_Type_Abst "A"
 560                                          (\ty_a ->
 561                                                 TeTy_Axiom $
 562                                                 Axiom_Term
 563                                                  (join::IO (IO (Term Var_Name)) -> IO (Term Var_Name))
 564                                                  (\ctx -> context_lift ctx <$> ty_a))
 565                                          ax1_ty
 566                                 ax1_ty =
 567                                         (("A" =?) `abstract`) $
 568                                         axiom_type_of context $
 569                                         axiom_term (join::IO (IO A) -> IO A)
 570
 571 prelude :: Axioms -> Env
 572 prelude axs =
 573         builtin axs $ concat $ (Text.unlines <$>) <$>
 574          [ prelude_bool
 575          , prelude_either
 576          ]
 577         where
 578         prelude_bool :: [[Text]]
 579         prelude_bool =
 580          [ ["Bool_Polytype : *p = (R:*) -> R -> R -> R"]
 581          , ["Bool  : *m   = Monotype Bool_Polytype"]
 582          , ["True  : Bool = monotype Bool_Polytype (λ(R:*) (True:R) (False:R) -> True)"]
 583          , ["False : Bool = monotype Bool_Polytype (λ(R:*) (True:R) (False:R) -> False)"]
 584          , [ "eq (x:Bool) (y:Bool) : Bool"
 585            , "  = monotype Bool_Polytype"
 586            , "    (λ(R:*) (True:R) (False:R) ->"
 587            , "      polytype Bool_Polytype x R"
 588            , "       (polytype Bool_Polytype y R True  False)"
 589            , "       (polytype Bool_Polytype y R False True)"
 590            , "    )"
 591            ]
 592          , [ "and (x:Bool) (y:Bool) : Bool"
 593            , " = monotype Bool_Polytype"
 594            , "   (λ(R:*) (True:R) (False:R) ->"
 595            , "     polytype Bool_Polytype x R"
 596            , "      (polytype Bool_Polytype y R True  False)"
 597            , "      (polytype Bool_Polytype y R False False)"
 598            , "   )"
 599            ]
 600          , [ "or (x:Bool) (y:Bool) : Bool"
 601            , " = monotype Bool_Polytype"
 602            , "   (λ(R:*) (True:R) (False:R) ->"
 603            , "     polytype Bool_Polytype x R"
 604            , "      (polytype Bool_Polytype y R True  True)"
 605            , "      (polytype Bool_Polytype y R True False)"
 606            , "   )"
 607            ]
 608          , [ "xor (x:Bool) (y:Bool) : Bool"
 609            , " = monotype Bool_Polytype"
 610            , "   (λ(R:*) (True:R) (False:R) ->"
 611            , "     polytype Bool_Polytype x R"
 612            , "      (polytype Bool_Polytype y R False  True)"
 613            , "      (polytype Bool_Polytype y R True False)"
 614            , "   )"
 615            ]
 616          , [ "not (x:Bool) : Bool"
 617            , " = monotype Bool_Polytype"
 618            , "   (λ(R:*) (True:R) (False:R) ->"
 619            , "     polytype Bool_Polytype x R False True)"
 620            ]
 621          ]
 622         prelude_either :: [[Text]]
 623         prelude_either =
 624          [ ["Either_Polytype (A:*) (B:*) : *p = (R:*) -> (A -> R) -> (B -> R) -> R"]
 625          , ["Either  (A:*) (B:*) : *m = Monotype (Either_Polytype A B)"]
 626          , [ "Left (A:*) (B:*) (x:A)"
 627            , "     : Either A B"
 628            , "     = monotype (Either_Polytype A B)"
 629            , "       (λ(R:*) (Left:A -> R) (Right:B -> R) -> Left x)"
 630            ]
 631          , [ "Right (A:*) (B:*) (x:B)"
 632            , "       : Either A B"
 633            , "       = monotype (Either_Polytype A B)"
 634            , "         (λ(R:*) (Left:A -> R) (Right:B -> R) -> Right x)"
 635            ]
 636          , [ "either (A:*) (B:*) (R:*) (l:A -> R) (r:B -> R) (e:Either A B) : R"
 637            , "   = polytype (Either_Polytype A B) e R l r"
 638            ]
 639          ]