module Website

import Data.String
import System

-- This is Molly's website.
--
-- This webpage is the source code for an Idris program which prints a
-- summary of the information presented below. This program is also a
-- quine -- it can print its own source code -- and is also a quine
-- generator (which is how I wrote it in the first place).


{- Information about me -}

||| My name.
name : String
name = "Molly Miller"

||| Types of link I have on my website.
data Link : Type where
  Blog : (url : String) -> Link
  GitHub : (username : String) -> Link
  Irc : (net : String) -> (nick : String) -> Link
  Email : (user_part : String) -> (domain_part : String) -> Link

||| Links to other places.
links : List Link
links = [ Blog "https://www.mollymiller.net/blog",
          GitHub "@sysvinit",
          Irc "Freenode" "sysvinit",
          Irc "Hackint" "sysvinit",
          Email "interwebs" "m-squa.red" ]

||| I have things in which I'm interested.
Interest : Type
Interest = String

||| I have the following general interests.
interests : List Interest
interests = [ "Unix systems", "network engineering",
              "functional programming" ]

||| I spend time doing things in places.
data Occupation : Type where
  OccupiedWith : (what : String) -> (where_ : String) -> Occupation

||| I spend most of my time doing this thing.
mainOccupation : Occupation
mainOccupation = OccupiedWith "Computer Science"
                 "the University of St Andrews"

||| But I do other things as well.
otherOccupations : List Occupation
otherOccupations = [
  OccupiedWith "internet routing" "AS207480"
]


{- Some meta things -}

||| The type of a copyright declaration.
data Copyright : Type where
  C : (year : Int) -> (holder : String) -> Copyright

||| This program carries the following copyright.
copyright : Copyright
copyright = C 2020 name

||| This program source code is released under the following licence.
spdxLicenseIdentifier : String
spdxLicenseIdentifier = "ISC"

||| This site was made using the following tools.
madeWith : List String
madeWith = ["Idris", "Pygments", "Dracula"]


{- The main program, which does the heavy lifting -}

-- Some useful interface implementations.

implementation Show Link where
  show (GitHub username) = username ++ " on GitHub"
  show (Irc net nick) = nick ++ " on " ++ net ++ " IRC"
  show (Email user domain) = "email " ++ user ++ " AT " ++ domain
  show (Blog url) = url

implementation Show Copyright where
  show (C year holder) = "Copyright (C) " ++ show year ++ " " ++ holder

implementation Show Occupation where
  show (OccupiedWith thing place) =
    thing ++ " at " ++ place

-- Some utility functions.

||| Exit with an error message.
errmsg : String -> IO a
errmsg msg = do fPutStrLn stderr msg
                exitFailure

||| Left-pad a string by some number of spaces.
indent : Nat -> String -> String
indent lvl msg = (pack $ replicate lvl ' ') ++ msg

||| Split a list of strings onto separate lines so that no line is
||| longer than `len` characters long.
wrapLines : Nat -> List String -> List (List String)
wrapLines len ss = wrapLines' 0 ss []
  where
    wrapLines' : Nat -> List String ->
                 List (List String) -> List (List String)
    wrapLines' v [] yss = yss
    wrapLines' v (x :: xs) [] = wrapLines' (length x) xs (pure (pure x))
    wrapLines' v (x :: xs) acc@(ys :: yss) =
      let newlen = length x + v
      in if newlen > len
         then wrapLines' 0 xs (pure x :: acc)
         else wrapLines' newlen xs ((x :: ys) :: yss)

||| Format and concatenate items in a line.
formatLines : Nat -> List (List String) -> List String
formatLines spcs =
  map (indent spcs . pack . intercalate [' ', '|', ' '] . map unpack)

||| Display the information presented at the top of this file.
displayInfo : IO ()
displayInfo =
  do putStrLn ""
     putStrLn (indent 30 name)
     putStrLn ""
     traverse_ putStrLn
               ((formatLines 8 . wrapLines 56 . reverse) interests)
     putStrLn ""
     traverse_ putStrLn
               ((formatLines 10 . wrapLines 44 . map show) links)
     putStrLn ""
     traverse_ (putStrLn . indent 12 . show)
               (mainOccupation :: otherOccupations)
     putStrLn ""
     putStr (indent 6 (show copyright))
     putStr "; SPDX-License-Identifier: "
     putStrLn spdxLicenseIdentifier
     putStrLn ""


||| Convert a Maybe to an Either, mapping Just to Right, and
||| Nothing to Left, with some default value specified for the
||| Left.
toEither : Maybe a -> Lazy b -> Either b a
toEither (Just v)  e = Right v
toEither (Nothing) e = Left e

-- Forward declarations, for functions which are used before they are
-- defined.

||| This program's own source code in encoded form
ownSource : (List String, List String)

||| Encoded magic numbers
magic : List String

-- Functions which perform quine encoding and decoding.

||| Convert a list of strings containing the encoded program
||| source into a list of decoded integers.
decode : List String -> Maybe (List Int)
decode xs = do xs' <- traverse (traverse parse . split isSpace) xs
               pure (concat xs')
  where
    parse : String -> Maybe Int
    parse s = do i <- parseInteger s
                 if i < 0
                   then Nothing
                   else Just i

||| Concatenate a list of strings containing encoded data, with
||| appropriate delimiters and indentation for printing.
catStrings : List String -> String
catStrings = foldr (++) "\n" . intersperse ",\n" .
             map (("  \"" ++) . (++ "\""))

||| Convert a list of integers into a string containing their
||| stringified values in a form which can be passed back into the
||| Idris compiler.
encode : List Int -> String
encode = catStrings . map concatLine . splitIntoLines
  where
    splitIntoLines : List a -> List (List a)
    splitIntoLines [] = []
    splitIntoLines xs = let (start, rest) = splitAt 17 xs
                        in start :: splitIntoLines rest

    concatLine : List Int -> String
    concatLine = pack . intercalate (pure ' ') . map (unpack . cast)

||| Turn a list of integers into a string whose characters have
||| the ASCII/Unicode values of the corresponding integer in the
||| input list.
render : List Int -> String
render = pack . map cast

||| Decode and render the magic numbers.
makeMagic : Maybe String
makeMagic = decode magic >>= (pure . render)

||| Decode and render the magic numbers and return them in an IO
||| context.
makeMagicIO : IO String
makeMagicIO = maybe (errmsg "Could not construct secret magic")
              pure makeMagic

||| Attempt to split an arbitrary program's input around a fixed point.
splitOnFixedPoint : String -> Either String (String, String)
splitOnFixedPoint str =
  let lines = (newlines . split (== '\n')) str
  in do mag <- toEither makeMagic "Could not construct secret magic"
        case split (== mag) lines of
          start :: end :: Nil => Right (concat start, concat end)
          _ => Left "Secret magic not found"
  where
    newlines : List String -> List String
    newlines [] = []
    newlines (x :: Nil) = pure x
    newlines (x :: xs) = (x ++ "\n") :: newlines xs

||| Load a file and attempt to split its contents around the
||| quine's fixed point.
loadFile : String -> IO (String, String)
loadFile file =
  do res <- readFile file

     content <- the (IO String)
       (case res of
         Right v => pure v
         Left err => errmsg ("Could not read " ++ file))

     case splitOnFixedPoint content of
       Right v => pure v
       Left err => errmsg err

-- Putting everything together...

||| Load this program's source from the named file and insert the
||| encoded sections necessary to turn it into a printable quine.
renderExternal : String -> IO String
renderExternal file =
  do (top, bottom) <- loadFile file
     middle <- makeMagicIO
     let enctop = (encode . map ord . unpack) top
     let encbot = (encode . map ord . unpack) bottom
     pure (top ++ enctop ++ middle ++ encbot ++ bottom)

||| Render this program's embedded encoded source into a printable
||| quine.
renderInternal : IO String
renderInternal =
  let enctop = catStrings (fst ownSource)
      encbot = catStrings (snd ownSource)
  in do middle <- makeMagicIO
        top <- maybe (errmsg "Could not decode source")
               (pure . render) (decode $ fst ownSource)
        bottom <- maybe (errmsg "Could not decode source")
                  (pure . render) (decode $ snd ownSource)
        pure (top ++ enctop ++ middle ++ encbot ++ bottom)

-- And the main program

||| The main entry point into the program
mainProg : IO ()
mainProg =
  do args <- getArgs
     case args of
       argv0 :: "source" :: Nil =>
             renderInternal >>= putStr
       argv0 :: "make-quine" :: filename :: Nil =>
             renderExternal filename >>= putStr
       _ => displayInfo



ownSource = ([
  "109 111 100 117 108 101 32 87 101 98 115 105 116 101 10 10 105",
  "109 112 111 114 116 32 68 97 116 97 46 83 116 114 105 110 103",
  "10 105 109 112 111 114 116 32 83 121 115 116 101 109 10 10 45",
  "45 32 84 104 105 115 32 105 115 32 77 111 108 108 121 39 115",
  "32 119 101 98 115 105 116 101 46 10 45 45 10 45 45 32 84",
  "104 105 115 32 119 101 98 112 97 103 101 32 105 115 32 116 104",
  "101 32 115 111 117 114 99 101 32 99 111 100 101 32 102 111 114",
  "32 97 110 32 73 100 114 105 115 32 112 114 111 103 114 97 109",
  "32 119 104 105 99 104 32 112 114 105 110 116 115 32 97 10 45",
  "45 32 115 117 109 109 97 114 121 32 111 102 32 116 104 101 32",
  "105 110 102 111 114 109 97 116 105 111 110 32 112 114 101 115 101",
  "110 116 101 100 32 98 101 108 111 119 46 32 84 104 105 115 32",
  "112 114 111 103 114 97 109 32 105 115 32 97 108 115 111 32 97",
  "10 45 45 32 113 117 105 110 101 32 45 45 32 105 116 32 99",
  "97 110 32 112 114 105 110 116 32 105 116 115 32 111 119 110 32",
  "115 111 117 114 99 101 32 99 111 100 101 32 45 45 32 97 110",
  "100 32 105 115 32 97 108 115 111 32 97 32 113 117 105 110 101",
  "10 45 45 32 103 101 110 101 114 97 116 111 114 32 40 119 104",
  "105 99 104 32 105 115 32 104 111 119 32 73 32 119 114 111 116",
  "101 32 105 116 32 105 110 32 116 104 101 32 102 105 114 115 116",
  "32 112 108 97 99 101 41 46 10 10 10 123 45 32 73 110 102",
  "111 114 109 97 116 105 111 110 32 97 98 111 117 116 32 109 101",
  "32 45 125 10 10 124 124 124 32 77 121 32 110 97 109 101 46",
  "10 110 97 109 101 32 58 32 83 116 114 105 110 103 10 110 97",
  "109 101 32 61 32 34 77 111 108 108 121 32 77 105 108 108 101",
  "114 34 10 10 124 124 124 32 84 121 112 101 115 32 111 102 32",
  "108 105 110 107 32 73 32 104 97 118 101 32 111 110 32 109 121",
  "32 119 101 98 115 105 116 101 46 10 100 97 116 97 32 76 105",
  "110 107 32 58 32 84 121 112 101 32 119 104 101 114 101 10 32",
  "32 66 108 111 103 32 58 32 40 117 114 108 32 58 32 83 116",
  "114 105 110 103 41 32 45 62 32 76 105 110 107 10 32 32 71",
  "105 116 72 117 98 32 58 32 40 117 115 101 114 110 97 109 101",
  "32 58 32 83 116 114 105 110 103 41 32 45 62 32 76 105 110",
  "107 10 32 32 73 114 99 32 58 32 40 110 101 116 32 58 32",
  "83 116 114 105 110 103 41 32 45 62 32 40 110 105 99 107 32",
  "58 32 83 116 114 105 110 103 41 32 45 62 32 76 105 110 107",
  "10 32 32 69 109 97 105 108 32 58 32 40 117 115 101 114 95",
  "112 97 114 116 32 58 32 83 116 114 105 110 103 41 32 45 62",
  "32 40 100 111 109 97 105 110 95 112 97 114 116 32 58 32 83",
  "116 114 105 110 103 41 32 45 62 32 76 105 110 107 10 10 124",
  "124 124 32 76 105 110 107 115 32 116 111 32 111 116 104 101 114",
  "32 112 108 97 99 101 115 46 10 108 105 110 107 115 32 58 32",
  "76 105 115 116 32 76 105 110 107 10 108 105 110 107 115 32 61",
  "32 91 32 66 108 111 103 32 34 104 116 116 112 115 58 47 47",
  "119 119 119 46 109 111 108 108 121 109 105 108 108 101 114 46 110",
  "101 116 47 98 108 111 103 34 44 10 32 32 32 32 32 32 32",
  "32 32 32 71 105 116 72 117 98 32 34 64 115 121 115 118 105",
  "110 105 116 34 44 10 32 32 32 32 32 32 32 32 32 32 73",
  "114 99 32 34 70 114 101 101 110 111 100 101 34 32 34 115 121",
  "115 118 105 110 105 116 34 44 10 32 32 32 32 32 32 32 32",
  "32 32 73 114 99 32 34 72 97 99 107 105 110 116 34 32 34",
  "115 121 115 118 105 110 105 116 34 44 10 32 32 32 32 32 32",
  "32 32 32 32 69 109 97 105 108 32 34 105 110 116 101 114 119",
  "101 98 115 34 32 34 109 45 115 113 117 97 46 114 101 100 34",
  "32 93 10 10 124 124 124 32 73 32 104 97 118 101 32 116 104",
  "105 110 103 115 32 105 110 32 119 104 105 99 104 32 73 39 109",
  "32 105 110 116 101 114 101 115 116 101 100 46 10 73 110 116 101",
  "114 101 115 116 32 58 32 84 121 112 101 10 73 110 116 101 114",
  "101 115 116 32 61 32 83 116 114 105 110 103 10 10 124 124 124",
  "32 73 32 104 97 118 101 32 116 104 101 32 102 111 108 108 111",
  "119 105 110 103 32 103 101 110 101 114 97 108 32 105 110 116 101",
  "114 101 115 116 115 46 10 105 110 116 101 114 101 115 116 115 32",
  "58 32 76 105 115 116 32 73 110 116 101 114 101 115 116 10 105",
  "110 116 101 114 101 115 116 115 32 61 32 91 32 34 85 110 105",
  "120 32 115 121 115 116 101 109 115 34 44 32 34 110 101 116 119",
  "111 114 107 32 101 110 103 105 110 101 101 114 105 110 103 34 44",
  "10 32 32 32 32 32 32 32 32 32 32 32 32 32 32 34 102",
  "117 110 99 116 105 111 110 97 108 32 112 114 111 103 114 97 109",
  "109 105 110 103 34 32 93 10 10 124 124 124 32 73 32 115 112",
  "101 110 100 32 116 105 109 101 32 100 111 105 110 103 32 116 104",
  "105 110 103 115 32 105 110 32 112 108 97 99 101 115 46 10 100",
  "97 116 97 32 79 99 99 117 112 97 116 105 111 110 32 58 32",
  "84 121 112 101 32 119 104 101 114 101 10 32 32 79 99 99 117",
  "112 105 101 100 87 105 116 104 32 58 32 40 119 104 97 116 32",
  "58 32 83 116 114 105 110 103 41 32 45 62 32 40 119 104 101",
  "114 101 95 32 58 32 83 116 114 105 110 103 41 32 45 62 32",
  "79 99 99 117 112 97 116 105 111 110 10 10 124 124 124 32 73",
  "32 115 112 101 110 100 32 109 111 115 116 32 111 102 32 109 121",
  "32 116 105 109 101 32 100 111 105 110 103 32 116 104 105 115 32",
  "116 104 105 110 103 46 10 109 97 105 110 79 99 99 117 112 97",
  "116 105 111 110 32 58 32 79 99 99 117 112 97 116 105 111 110",
  "10 109 97 105 110 79 99 99 117 112 97 116 105 111 110 32 61",
  "32 79 99 99 117 112 105 101 100 87 105 116 104 32 34 67 111",
  "109 112 117 116 101 114 32 83 99 105 101 110 99 101 34 10 32",
  "32 32 32 32 32 32 32 32 32 32 32 32 32 32 32 32 34",
  "116 104 101 32 85 110 105 118 101 114 115 105 116 121 32 111 102",
  "32 83 116 32 65 110 100 114 101 119 115 34 10 10 124 124 124",
  "32 66 117 116 32 73 32 100 111 32 111 116 104 101 114 32 116",
  "104 105 110 103 115 32 97 115 32 119 101 108 108 46 10 111 116",
  "104 101 114 79 99 99 117 112 97 116 105 111 110 115 32 58 32",
  "76 105 115 116 32 79 99 99 117 112 97 116 105 111 110 10 111",
  "116 104 101 114 79 99 99 117 112 97 116 105 111 110 115 32 61",
  "32 91 10 32 32 79 99 99 117 112 105 101 100 87 105 116 104",
  "32 34 105 110 116 101 114 110 101 116 32 114 111 117 116 105 110",
  "103 34 32 34 65 83 50 48 55 52 56 48 34 10 93 10 10",
  "10 123 45 32 83 111 109 101 32 109 101 116 97 32 116 104 105",
  "110 103 115 32 45 125 10 10 124 124 124 32 84 104 101 32 116",
  "121 112 101 32 111 102 32 97 32 99 111 112 121 114 105 103 104",
  "116 32 100 101 99 108 97 114 97 116 105 111 110 46 10 100 97",
  "116 97 32 67 111 112 121 114 105 103 104 116 32 58 32 84 121",
  "112 101 32 119 104 101 114 101 10 32 32 67 32 58 32 40 121",
  "101 97 114 32 58 32 73 110 116 41 32 45 62 32 40 104 111",
  "108 100 101 114 32 58 32 83 116 114 105 110 103 41 32 45 62",
  "32 67 111 112 121 114 105 103 104 116 10 10 124 124 124 32 84",
  "104 105 115 32 112 114 111 103 114 97 109 32 99 97 114 114 105",
  "101 115 32 116 104 101 32 102 111 108 108 111 119 105 110 103 32",
  "99 111 112 121 114 105 103 104 116 46 10 99 111 112 121 114 105",
  "103 104 116 32 58 32 67 111 112 121 114 105 103 104 116 10 99",
  "111 112 121 114 105 103 104 116 32 61 32 67 32 50 48 50 48",
  "32 110 97 109 101 10 10 124 124 124 32 84 104 105 115 32 112",
  "114 111 103 114 97 109 32 115 111 117 114 99 101 32 99 111 100",
  "101 32 105 115 32 114 101 108 101 97 115 101 100 32 117 110 100",
  "101 114 32 116 104 101 32 102 111 108 108 111 119 105 110 103 32",
  "108 105 99 101 110 99 101 46 10 115 112 100 120 76 105 99 101",
  "110 115 101 73 100 101 110 116 105 102 105 101 114 32 58 32 83",
  "116 114 105 110 103 10 115 112 100 120 76 105 99 101 110 115 101",
  "73 100 101 110 116 105 102 105 101 114 32 61 32 34 73 83 67",
  "34 10 10 124 124 124 32 84 104 105 115 32 115 105 116 101 32",
  "119 97 115 32 109 97 100 101 32 117 115 105 110 103 32 116 104",
  "101 32 102 111 108 108 111 119 105 110 103 32 116 111 111 108 115",
  "46 10 109 97 100 101 87 105 116 104 32 58 32 76 105 115 116",
  "32 83 116 114 105 110 103 10 109 97 100 101 87 105 116 104 32",
  "61 32 91 34 73 100 114 105 115 34 44 32 34 80 121 103 109",
  "101 110 116 115 34 44 32 34 68 114 97 99 117 108 97 34 93",
  "10 10 10 123 45 32 84 104 101 32 109 97 105 110 32 112 114",
  "111 103 114 97 109 44 32 119 104 105 99 104 32 100 111 101 115",
  "32 116 104 101 32 104 101 97 118 121 32 108 105 102 116 105 110",
  "103 32 45 125 10 10 45 45 32 83 111 109 101 32 117 115 101",
  "102 117 108 32 105 110 116 101 114 102 97 99 101 32 105 109 112",
  "108 101 109 101 110 116 97 116 105 111 110 115 46 10 10 105 109",
  "112 108 101 109 101 110 116 97 116 105 111 110 32 83 104 111 119",
  "32 76 105 110 107 32 119 104 101 114 101 10 32 32 115 104 111",
  "119 32 40 71 105 116 72 117 98 32 117 115 101 114 110 97 109",
  "101 41 32 61 32 117 115 101 114 110 97 109 101 32 43 43 32",
  "34 32 111 110 32 71 105 116 72 117 98 34 10 32 32 115 104",
  "111 119 32 40 73 114 99 32 110 101 116 32 110 105 99 107 41",
  "32 61 32 110 105 99 107 32 43 43 32 34 32 111 110 32 34",
  "32 43 43 32 110 101 116 32 43 43 32 34 32 73 82 67 34",
  "10 32 32 115 104 111 119 32 40 69 109 97 105 108 32 117 115",
  "101 114 32 100 111 109 97 105 110 41 32 61 32 34 101 109 97",
  "105 108 32 34 32 43 43 32 117 115 101 114 32 43 43 32 34",
  "32 65 84 32 34 32 43 43 32 100 111 109 97 105 110 10 32",
  "32 115 104 111 119 32 40 66 108 111 103 32 117 114 108 41 32",
  "61 32 117 114 108 10 10 105 109 112 108 101 109 101 110 116 97",
  "116 105 111 110 32 83 104 111 119 32 67 111 112 121 114 105 103",
  "104 116 32 119 104 101 114 101 10 32 32 115 104 111 119 32 40",
  "67 32 121 101 97 114 32 104 111 108 100 101 114 41 32 61 32",
  "34 67 111 112 121 114 105 103 104 116 32 40 67 41 32 34 32",
  "43 43 32 115 104 111 119 32 121 101 97 114 32 43 43 32 34",
  "32 34 32 43 43 32 104 111 108 100 101 114 10 10 105 109 112",
  "108 101 109 101 110 116 97 116 105 111 110 32 83 104 111 119 32",
  "79 99 99 117 112 97 116 105 111 110 32 119 104 101 114 101 10",
  "32 32 115 104 111 119 32 40 79 99 99 117 112 105 101 100 87",
  "105 116 104 32 116 104 105 110 103 32 112 108 97 99 101 41 32",
  "61 10 32 32 32 32 116 104 105 110 103 32 43 43 32 34 32",
  "97 116 32 34 32 43 43 32 112 108 97 99 101 10 10 45 45",
  "32 83 111 109 101 32 117 116 105 108 105 116 121 32 102 117 110",
  "99 116 105 111 110 115 46 10 10 124 124 124 32 69 120 105 116",
  "32 119 105 116 104 32 97 110 32 101 114 114 111 114 32 109 101",
  "115 115 97 103 101 46 10 101 114 114 109 115 103 32 58 32 83",
  "116 114 105 110 103 32 45 62 32 73 79 32 97 10 101 114 114",
  "109 115 103 32 109 115 103 32 61 32 100 111 32 102 80 117 116",
  "83 116 114 76 110 32 115 116 100 101 114 114 32 109 115 103 10",
  "32 32 32 32 32 32 32 32 32 32 32 32 32 32 32 32 101",
  "120 105 116 70 97 105 108 117 114 101 10 10 124 124 124 32 76",
  "101 102 116 45 112 97 100 32 97 32 115 116 114 105 110 103 32",
  "98 121 32 115 111 109 101 32 110 117 109 98 101 114 32 111 102",
  "32 115 112 97 99 101 115 46 10 105 110 100 101 110 116 32 58",
  "32 78 97 116 32 45 62 32 83 116 114 105 110 103 32 45 62",
  "32 83 116 114 105 110 103 10 105 110 100 101 110 116 32 108 118",
  "108 32 109 115 103 32 61 32 40 112 97 99 107 32 36 32 114",
  "101 112 108 105 99 97 116 101 32 108 118 108 32 39 32 39 41",
  "32 43 43 32 109 115 103 10 10 124 124 124 32 83 112 108 105",
  "116 32 97 32 108 105 115 116 32 111 102 32 115 116 114 105 110",
  "103 115 32 111 110 116 111 32 115 101 112 97 114 97 116 101 32",
  "108 105 110 101 115 32 115 111 32 116 104 97 116 32 110 111 32",
  "108 105 110 101 32 105 115 10 124 124 124 32 108 111 110 103 101",
  "114 32 116 104 97 110 32 96 108 101 110 96 32 99 104 97 114",
  "97 99 116 101 114 115 32 108 111 110 103 46 10 119 114 97 112",
  "76 105 110 101 115 32 58 32 78 97 116 32 45 62 32 76 105",
  "115 116 32 83 116 114 105 110 103 32 45 62 32 76 105 115 116",
  "32 40 76 105 115 116 32 83 116 114 105 110 103 41 10 119 114",
  "97 112 76 105 110 101 115 32 108 101 110 32 115 115 32 61 32",
  "119 114 97 112 76 105 110 101 115 39 32 48 32 115 115 32 91",
  "93 10 32 32 119 104 101 114 101 10 32 32 32 32 119 114 97",
  "112 76 105 110 101 115 39 32 58 32 78 97 116 32 45 62 32",
  "76 105 115 116 32 83 116 114 105 110 103 32 45 62 10 32 32",
  "32 32 32 32 32 32 32 32 32 32 32 32 32 32 32 76 105",
  "115 116 32 40 76 105 115 116 32 83 116 114 105 110 103 41 32",
  "45 62 32 76 105 115 116 32 40 76 105 115 116 32 83 116 114",
  "105 110 103 41 10 32 32 32 32 119 114 97 112 76 105 110 101",
  "115 39 32 118 32 91 93 32 121 115 115 32 61 32 121 115 115",
  "10 32 32 32 32 119 114 97 112 76 105 110 101 115 39 32 118",
  "32 40 120 32 58 58 32 120 115 41 32 91 93 32 61 32 119",
  "114 97 112 76 105 110 101 115 39 32 40 108 101 110 103 116 104",
  "32 120 41 32 120 115 32 40 112 117 114 101 32 40 112 117 114",
  "101 32 120 41 41 10 32 32 32 32 119 114 97 112 76 105 110",
  "101 115 39 32 118 32 40 120 32 58 58 32 120 115 41 32 97",
  "99 99 64 40 121 115 32 58 58 32 121 115 115 41 32 61 10",
  "32 32 32 32 32 32 108 101 116 32 110 101 119 108 101 110 32",
  "61 32 108 101 110 103 116 104 32 120 32 43 32 118 10 32 32",
  "32 32 32 32 105 110 32 105 102 32 110 101 119 108 101 110 32",
  "62 32 108 101 110 10 32 32 32 32 32 32 32 32 32 116 104",
  "101 110 32 119 114 97 112 76 105 110 101 115 39 32 48 32 120",
  "115 32 40 112 117 114 101 32 120 32 58 58 32 97 99 99 41",
  "10 32 32 32 32 32 32 32 32 32 101 108 115 101 32 119 114",
  "97 112 76 105 110 101 115 39 32 110 101 119 108 101 110 32 120",
  "115 32 40 40 120 32 58 58 32 121 115 41 32 58 58 32 121",
  "115 115 41 10 10 124 124 124 32 70 111 114 109 97 116 32 97",
  "110 100 32 99 111 110 99 97 116 101 110 97 116 101 32 105 116",
  "101 109 115 32 105 110 32 97 32 108 105 110 101 46 10 102 111",
  "114 109 97 116 76 105 110 101 115 32 58 32 78 97 116 32 45",
  "62 32 76 105 115 116 32 40 76 105 115 116 32 83 116 114 105",
  "110 103 41 32 45 62 32 76 105 115 116 32 83 116 114 105 110",
  "103 10 102 111 114 109 97 116 76 105 110 101 115 32 115 112 99",
  "115 32 61 10 32 32 109 97 112 32 40 105 110 100 101 110 116",
  "32 115 112 99 115 32 46 32 112 97 99 107 32 46 32 105 110",
  "116 101 114 99 97 108 97 116 101 32 91 39 32 39 44 32 39",
  "124 39 44 32 39 32 39 93 32 46 32 109 97 112 32 117 110",
  "112 97 99 107 41 10 10 124 124 124 32 68 105 115 112 108 97",
  "121 32 116 104 101 32 105 110 102 111 114 109 97 116 105 111 110",
  "32 112 114 101 115 101 110 116 101 100 32 97 116 32 116 104 101",
  "32 116 111 112 32 111 102 32 116 104 105 115 32 102 105 108 101",
  "46 10 100 105 115 112 108 97 121 73 110 102 111 32 58 32 73",
  "79 32 40 41 10 100 105 115 112 108 97 121 73 110 102 111 32",
  "61 10 32 32 100 111 32 112 117 116 83 116 114 76 110 32 34",
  "34 10 32 32 32 32 32 112 117 116 83 116 114 76 110 32 40",
  "105 110 100 101 110 116 32 51 48 32 110 97 109 101 41 10 32",
  "32 32 32 32 112 117 116 83 116 114 76 110 32 34 34 10 32",
  "32 32 32 32 116 114 97 118 101 114 115 101 95 32 112 117 116",
  "83 116 114 76 110 10 32 32 32 32 32 32 32 32 32 32 32",
  "32 32 32 32 40 40 102 111 114 109 97 116 76 105 110 101 115",
  "32 56 32 46 32 119 114 97 112 76 105 110 101 115 32 53 54",
  "32 46 32 114 101 118 101 114 115 101 41 32 105 110 116 101 114",
  "101 115 116 115 41 10 32 32 32 32 32 112 117 116 83 116 114",
  "76 110 32 34 34 10 32 32 32 32 32 116 114 97 118 101 114",
  "115 101 95 32 112 117 116 83 116 114 76 110 10 32 32 32 32",
  "32 32 32 32 32 32 32 32 32 32 32 40 40 102 111 114 109",
  "97 116 76 105 110 101 115 32 49 48 32 46 32 119 114 97 112",
  "76 105 110 101 115 32 52 52 32 46 32 109 97 112 32 115 104",
  "111 119 41 32 108 105 110 107 115 41 10 32 32 32 32 32 112",
  "117 116 83 116 114 76 110 32 34 34 10 32 32 32 32 32 116",
  "114 97 118 101 114 115 101 95 32 40 112 117 116 83 116 114 76",
  "110 32 46 32 105 110 100 101 110 116 32 49 50 32 46 32 115",
  "104 111 119 41 10 32 32 32 32 32 32 32 32 32 32 32 32",
  "32 32 32 40 109 97 105 110 79 99 99 117 112 97 116 105 111",
  "110 32 58 58 32 111 116 104 101 114 79 99 99 117 112 97 116",
  "105 111 110 115 41 10 32 32 32 32 32 112 117 116 83 116 114",
  "76 110 32 34 34 10 32 32 32 32 32 112 117 116 83 116 114",
  "32 40 105 110 100 101 110 116 32 54 32 40 115 104 111 119 32",
  "99 111 112 121 114 105 103 104 116 41 41 10 32 32 32 32 32",
  "112 117 116 83 116 114 32 34 59 32 83 80 68 88 45 76 105",
  "99 101 110 115 101 45 73 100 101 110 116 105 102 105 101 114 58",
  "32 34 10 32 32 32 32 32 112 117 116 83 116 114 76 110 32",
  "115 112 100 120 76 105 99 101 110 115 101 73 100 101 110 116 105",
  "102 105 101 114 10 32 32 32 32 32 112 117 116 83 116 114 76",
  "110 32 34 34 10 10 10 124 124 124 32 67 111 110 118 101 114",
  "116 32 97 32 77 97 121 98 101 32 116 111 32 97 110 32 69",
  "105 116 104 101 114 44 32 109 97 112 112 105 110 103 32 74 117",
  "115 116 32 116 111 32 82 105 103 104 116 44 32 97 110 100 10",
  "124 124 124 32 78 111 116 104 105 110 103 32 116 111 32 76 101",
  "102 116 44 32 119 105 116 104 32 115 111 109 101 32 100 101 102",
  "97 117 108 116 32 118 97 108 117 101 32 115 112 101 99 105 102",
  "105 101 100 32 102 111 114 32 116 104 101 10 124 124 124 32 76",
  "101 102 116 46 10 116 111 69 105 116 104 101 114 32 58 32 77",
  "97 121 98 101 32 97 32 45 62 32 76 97 122 121 32 98 32",
  "45 62 32 69 105 116 104 101 114 32 98 32 97 10 116 111 69",
  "105 116 104 101 114 32 40 74 117 115 116 32 118 41 32 32 101",
  "32 61 32 82 105 103 104 116 32 118 10 116 111 69 105 116 104",
  "101 114 32 40 78 111 116 104 105 110 103 41 32 101 32 61 32",
  "76 101 102 116 32 101 10 10 45 45 32 70 111 114 119 97 114",
  "100 32 100 101 99 108 97 114 97 116 105 111 110 115 44 32 102",
  "111 114 32 102 117 110 99 116 105 111 110 115 32 119 104 105 99",
  "104 32 97 114 101 32 117 115 101 100 32 98 101 102 111 114 101",
  "32 116 104 101 121 32 97 114 101 10 45 45 32 100 101 102 105",
  "110 101 100 46 10 10 124 124 124 32 84 104 105 115 32 112 114",
  "111 103 114 97 109 39 115 32 111 119 110 32 115 111 117 114 99",
  "101 32 99 111 100 101 32 105 110 32 101 110 99 111 100 101 100",
  "32 102 111 114 109 10 111 119 110 83 111 117 114 99 101 32 58",
  "32 40 76 105 115 116 32 83 116 114 105 110 103 44 32 76 105",
  "115 116 32 83 116 114 105 110 103 41 10 10 124 124 124 32 69",
  "110 99 111 100 101 100 32 109 97 103 105 99 32 110 117 109 98",
  "101 114 115 10 109 97 103 105 99 32 58 32 76 105 115 116 32",
  "83 116 114 105 110 103 10 10 45 45 32 70 117 110 99 116 105",
  "111 110 115 32 119 104 105 99 104 32 112 101 114 102 111 114 109",
  "32 113 117 105 110 101 32 101 110 99 111 100 105 110 103 32 97",
  "110 100 32 100 101 99 111 100 105 110 103 46 10 10 124 124 124",
  "32 67 111 110 118 101 114 116 32 97 32 108 105 115 116 32 111",
  "102 32 115 116 114 105 110 103 115 32 99 111 110 116 97 105 110",
  "105 110 103 32 116 104 101 32 101 110 99 111 100 101 100 32 112",
  "114 111 103 114 97 109 10 124 124 124 32 115 111 117 114 99 101",
  "32 105 110 116 111 32 97 32 108 105 115 116 32 111 102 32 100",
  "101 99 111 100 101 100 32 105 110 116 101 103 101 114 115 46 10",
  "100 101 99 111 100 101 32 58 32 76 105 115 116 32 83 116 114",
  "105 110 103 32 45 62 32 77 97 121 98 101 32 40 76 105 115",
  "116 32 73 110 116 41 10 100 101 99 111 100 101 32 120 115 32",
  "61 32 100 111 32 120 115 39 32 60 45 32 116 114 97 118 101",
  "114 115 101 32 40 116 114 97 118 101 114 115 101 32 112 97 114",
  "115 101 32 46 32 115 112 108 105 116 32 105 115 83 112 97 99",
  "101 41 32 120 115 10 32 32 32 32 32 32 32 32 32 32 32",
  "32 32 32 32 112 117 114 101 32 40 99 111 110 99 97 116 32",
  "120 115 39 41 10 32 32 119 104 101 114 101 10 32 32 32 32",
  "112 97 114 115 101 32 58 32 83 116 114 105 110 103 32 45 62",
  "32 77 97 121 98 101 32 73 110 116 10 32 32 32 32 112 97",
  "114 115 101 32 115 32 61 32 100 111 32 105 32 60 45 32 112",
  "97 114 115 101 73 110 116 101 103 101 114 32 115 10 32 32 32",
  "32 32 32 32 32 32 32 32 32 32 32 32 32 32 105 102 32",
  "105 32 60 32 48 10 32 32 32 32 32 32 32 32 32 32 32",
  "32 32 32 32 32 32 32 32 116 104 101 110 32 78 111 116 104",
  "105 110 103 10 32 32 32 32 32 32 32 32 32 32 32 32 32",
  "32 32 32 32 32 32 101 108 115 101 32 74 117 115 116 32 105",
  "10 10 124 124 124 32 67 111 110 99 97 116 101 110 97 116 101",
  "32 97 32 108 105 115 116 32 111 102 32 115 116 114 105 110 103",
  "115 32 99 111 110 116 97 105 110 105 110 103 32 101 110 99 111",
  "100 101 100 32 100 97 116 97 44 32 119 105 116 104 10 124 124",
  "124 32 97 112 112 114 111 112 114 105 97 116 101 32 100 101 108",
  "105 109 105 116 101 114 115 32 97 110 100 32 105 110 100 101 110",
  "116 97 116 105 111 110 32 102 111 114 32 112 114 105 110 116 105",
  "110 103 46 10 99 97 116 83 116 114 105 110 103 115 32 58 32",
  "76 105 115 116 32 83 116 114 105 110 103 32 45 62 32 83 116",
  "114 105 110 103 10 99 97 116 83 116 114 105 110 103 115 32 61",
  "32 102 111 108 100 114 32 40 43 43 41 32 34 92 110 34 32",
  "46 32 105 110 116 101 114 115 112 101 114 115 101 32 34 44 92",
  "110 34 32 46 10 32 32 32 32 32 32 32 32 32 32 32 32",
  "32 109 97 112 32 40 40 34 32 32 92 34 34 32 43 43 41",
  "32 46 32 40 43 43 32 34 92 34 34 41 41 10 10 124 124",
  "124 32 67 111 110 118 101 114 116 32 97 32 108 105 115 116 32",
  "111 102 32 105 110 116 101 103 101 114 115 32 105 110 116 111 32",
  "97 32 115 116 114 105 110 103 32 99 111 110 116 97 105 110 105",
  "110 103 32 116 104 101 105 114 10 124 124 124 32 115 116 114 105",
  "110 103 105 102 105 101 100 32 118 97 108 117 101 115 32 105 110",
  "32 97 32 102 111 114 109 32 119 104 105 99 104 32 99 97 110",
  "32 98 101 32 112 97 115 115 101 100 32 98 97 99 107 32 105",
  "110 116 111 32 116 104 101 10 124 124 124 32 73 100 114 105 115",
  "32 99 111 109 112 105 108 101 114 46 10 101 110 99 111 100 101",
  "32 58 32 76 105 115 116 32 73 110 116 32 45 62 32 83 116",
  "114 105 110 103 10 101 110 99 111 100 101 32 61 32 99 97 116",
  "83 116 114 105 110 103 115 32 46 32 109 97 112 32 99 111 110",
  "99 97 116 76 105 110 101 32 46 32 115 112 108 105 116 73 110",
  "116 111 76 105 110 101 115 10 32 32 119 104 101 114 101 10 32",
  "32 32 32 115 112 108 105 116 73 110 116 111 76 105 110 101 115",
  "32 58 32 76 105 115 116 32 97 32 45 62 32 76 105 115 116",
  "32 40 76 105 115 116 32 97 41 10 32 32 32 32 115 112 108",
  "105 116 73 110 116 111 76 105 110 101 115 32 91 93 32 61 32",
  "91 93 10 32 32 32 32 115 112 108 105 116 73 110 116 111 76",
  "105 110 101 115 32 120 115 32 61 32 108 101 116 32 40 115 116",
  "97 114 116 44 32 114 101 115 116 41 32 61 32 115 112 108 105",
  "116 65 116 32 49 55 32 120 115 10 32 32 32 32 32 32 32",
  "32 32 32 32 32 32 32 32 32 32 32 32 32 32 32 32 32",
  "105 110 32 115 116 97 114 116 32 58 58 32 115 112 108 105 116",
  "73 110 116 111 76 105 110 101 115 32 114 101 115 116 10 10 32",
  "32 32 32 99 111 110 99 97 116 76 105 110 101 32 58 32 76",
  "105 115 116 32 73 110 116 32 45 62 32 83 116 114 105 110 103",
  "10 32 32 32 32 99 111 110 99 97 116 76 105 110 101 32 61",
  "32 112 97 99 107 32 46 32 105 110 116 101 114 99 97 108 97",
  "116 101 32 40 112 117 114 101 32 39 32 39 41 32 46 32 109",
  "97 112 32 40 117 110 112 97 99 107 32 46 32 99 97 115 116",
  "41 10 10 124 124 124 32 84 117 114 110 32 97 32 108 105 115",
  "116 32 111 102 32 105 110 116 101 103 101 114 115 32 105 110 116",
  "111 32 97 32 115 116 114 105 110 103 32 119 104 111 115 101 32",
  "99 104 97 114 97 99 116 101 114 115 32 104 97 118 101 10 124",
  "124 124 32 116 104 101 32 65 83 67 73 73 47 85 110 105 99",
  "111 100 101 32 118 97 108 117 101 115 32 111 102 32 116 104 101",
  "32 99 111 114 114 101 115 112 111 110 100 105 110 103 32 105 110",
  "116 101 103 101 114 32 105 110 32 116 104 101 10 124 124 124 32",
  "105 110 112 117 116 32 108 105 115 116 46 10 114 101 110 100 101",
  "114 32 58 32 76 105 115 116 32 73 110 116 32 45 62 32 83",
  "116 114 105 110 103 10 114 101 110 100 101 114 32 61 32 112 97",
  "99 107 32 46 32 109 97 112 32 99 97 115 116 10 10 124 124",
  "124 32 68 101 99 111 100 101 32 97 110 100 32 114 101 110 100",
  "101 114 32 116 104 101 32 109 97 103 105 99 32 110 117 109 98",
  "101 114 115 46 10 109 97 107 101 77 97 103 105 99 32 58 32",
  "77 97 121 98 101 32 83 116 114 105 110 103 10 109 97 107 101",
  "77 97 103 105 99 32 61 32 100 101 99 111 100 101 32 109 97",
  "103 105 99 32 62 62 61 32 40 112 117 114 101 32 46 32 114",
  "101 110 100 101 114 41 10 10 124 124 124 32 68 101 99 111 100",
  "101 32 97 110 100 32 114 101 110 100 101 114 32 116 104 101 32",
  "109 97 103 105 99 32 110 117 109 98 101 114 115 32 97 110 100",
  "32 114 101 116 117 114 110 32 116 104 101 109 32 105 110 32 97",
  "110 32 73 79 10 124 124 124 32 99 111 110 116 101 120 116 46",
  "10 109 97 107 101 77 97 103 105 99 73 79 32 58 32 73 79",
  "32 83 116 114 105 110 103 10 109 97 107 101 77 97 103 105 99",
  "73 79 32 61 32 109 97 121 98 101 32 40 101 114 114 109 115",
  "103 32 34 67 111 117 108 100 32 110 111 116 32 99 111 110 115",
  "116 114 117 99 116 32 115 101 99 114 101 116 32 109 97 103 105",
  "99 34 41 10 32 32 32 32 32 32 32 32 32 32 32 32 32",
  "32 112 117 114 101 32 109 97 107 101 77 97 103 105 99 10 10",
  "124 124 124 32 65 116 116 101 109 112 116 32 116 111 32 115 112",
  "108 105 116 32 97 110 32 97 114 98 105 116 114 97 114 121 32",
  "112 114 111 103 114 97 109 39 115 32 105 110 112 117 116 32 97",
  "114 111 117 110 100 32 97 32 102 105 120 101 100 32 112 111 105",
  "110 116 46 10 115 112 108 105 116 79 110 70 105 120 101 100 80",
  "111 105 110 116 32 58 32 83 116 114 105 110 103 32 45 62 32",
  "69 105 116 104 101 114 32 83 116 114 105 110 103 32 40 83 116",
  "114 105 110 103 44 32 83 116 114 105 110 103 41 10 115 112 108",
  "105 116 79 110 70 105 120 101 100 80 111 105 110 116 32 115 116",
  "114 32 61 10 32 32 108 101 116 32 108 105 110 101 115 32 61",
  "32 40 110 101 119 108 105 110 101 115 32 46 32 115 112 108 105",
  "116 32 40 61 61 32 39 92 110 39 41 41 32 115 116 114 10",
  "32 32 105 110 32 100 111 32 109 97 103 32 60 45 32 116 111",
  "69 105 116 104 101 114 32 109 97 107 101 77 97 103 105 99 32",
  "34 67 111 117 108 100 32 110 111 116 32 99 111 110 115 116 114",
  "117 99 116 32 115 101 99 114 101 116 32 109 97 103 105 99 34",
  "10 32 32 32 32 32 32 32 32 99 97 115 101 32 115 112 108",
  "105 116 32 40 61 61 32 109 97 103 41 32 108 105 110 101 115",
  "32 111 102 10 32 32 32 32 32 32 32 32 32 32 115 116 97",
  "114 116 32 58 58 32 101 110 100 32 58 58 32 78 105 108 32",
  "61 62 32 82 105 103 104 116 32 40 99 111 110 99 97 116 32",
  "115 116 97 114 116 44 32 99 111 110 99 97 116 32 101 110 100",
  "41 10 32 32 32 32 32 32 32 32 32 32 95 32 61 62 32",
  "76 101 102 116 32 34 83 101 99 114 101 116 32 109 97 103 105",
  "99 32 110 111 116 32 102 111 117 110 100 34 10 32 32 119 104",
  "101 114 101 10 32 32 32 32 110 101 119 108 105 110 101 115 32",
  "58 32 76 105 115 116 32 83 116 114 105 110 103 32 45 62 32",
  "76 105 115 116 32 83 116 114 105 110 103 10 32 32 32 32 110",
  "101 119 108 105 110 101 115 32 91 93 32 61 32 91 93 10 32",
  "32 32 32 110 101 119 108 105 110 101 115 32 40 120 32 58 58",
  "32 78 105 108 41 32 61 32 112 117 114 101 32 120 10 32 32",
  "32 32 110 101 119 108 105 110 101 115 32 40 120 32 58 58 32",
  "120 115 41 32 61 32 40 120 32 43 43 32 34 92 110 34 41",
  "32 58 58 32 110 101 119 108 105 110 101 115 32 120 115 10 10",
  "124 124 124 32 76 111 97 100 32 97 32 102 105 108 101 32 97",
  "110 100 32 97 116 116 101 109 112 116 32 116 111 32 115 112 108",
  "105 116 32 105 116 115 32 99 111 110 116 101 110 116 115 32 97",
  "114 111 117 110 100 32 116 104 101 10 124 124 124 32 113 117 105",
  "110 101 39 115 32 102 105 120 101 100 32 112 111 105 110 116 46",
  "10 108 111 97 100 70 105 108 101 32 58 32 83 116 114 105 110",
  "103 32 45 62 32 73 79 32 40 83 116 114 105 110 103 44 32",
  "83 116 114 105 110 103 41 10 108 111 97 100 70 105 108 101 32",
  "102 105 108 101 32 61 10 32 32 100 111 32 114 101 115 32 60",
  "45 32 114 101 97 100 70 105 108 101 32 102 105 108 101 10 10",
  "32 32 32 32 32 99 111 110 116 101 110 116 32 60 45 32 116",
  "104 101 32 40 73 79 32 83 116 114 105 110 103 41 10 32 32",
  "32 32 32 32 32 40 99 97 115 101 32 114 101 115 32 111 102",
  "10 32 32 32 32 32 32 32 32 32 82 105 103 104 116 32 118",
  "32 61 62 32 112 117 114 101 32 118 10 32 32 32 32 32 32",
  "32 32 32 76 101 102 116 32 101 114 114 32 61 62 32 101 114",
  "114 109 115 103 32 40 34 67 111 117 108 100 32 110 111 116 32",
  "114 101 97 100 32 34 32 43 43 32 102 105 108 101 41 41 10",
  "10 32 32 32 32 32 99 97 115 101 32 115 112 108 105 116 79",
  "110 70 105 120 101 100 80 111 105 110 116 32 99 111 110 116 101",
  "110 116 32 111 102 10 32 32 32 32 32 32 32 82 105 103 104",
  "116 32 118 32 61 62 32 112 117 114 101 32 118 10 32 32 32",
  "32 32 32 32 76 101 102 116 32 101 114 114 32 61 62 32 101",
  "114 114 109 115 103 32 101 114 114 10 10 45 45 32 80 117 116",
  "116 105 110 103 32 101 118 101 114 121 116 104 105 110 103 32 116",
  "111 103 101 116 104 101 114 46 46 46 10 10 124 124 124 32 76",
  "111 97 100 32 116 104 105 115 32 112 114 111 103 114 97 109 39",
  "115 32 115 111 117 114 99 101 32 102 114 111 109 32 116 104 101",
  "32 110 97 109 101 100 32 102 105 108 101 32 97 110 100 32 105",
  "110 115 101 114 116 32 116 104 101 10 124 124 124 32 101 110 99",
  "111 100 101 100 32 115 101 99 116 105 111 110 115 32 110 101 99",
  "101 115 115 97 114 121 32 116 111 32 116 117 114 110 32 105 116",
  "32 105 110 116 111 32 97 32 112 114 105 110 116 97 98 108 101",
  "32 113 117 105 110 101 46 10 114 101 110 100 101 114 69 120 116",
  "101 114 110 97 108 32 58 32 83 116 114 105 110 103 32 45 62",
  "32 73 79 32 83 116 114 105 110 103 10 114 101 110 100 101 114",
  "69 120 116 101 114 110 97 108 32 102 105 108 101 32 61 10 32",
  "32 100 111 32 40 116 111 112 44 32 98 111 116 116 111 109 41",
  "32 60 45 32 108 111 97 100 70 105 108 101 32 102 105 108 101",
  "10 32 32 32 32 32 109 105 100 100 108 101 32 60 45 32 109",
  "97 107 101 77 97 103 105 99 73 79 10 32 32 32 32 32 108",
  "101 116 32 101 110 99 116 111 112 32 61 32 40 101 110 99 111",
  "100 101 32 46 32 109 97 112 32 111 114 100 32 46 32 117 110",
  "112 97 99 107 41 32 116 111 112 10 32 32 32 32 32 108 101",
  "116 32 101 110 99 98 111 116 32 61 32 40 101 110 99 111 100",
  "101 32 46 32 109 97 112 32 111 114 100 32 46 32 117 110 112",
  "97 99 107 41 32 98 111 116 116 111 109 10 32 32 32 32 32",
  "112 117 114 101 32 40 116 111 112 32 43 43 32 101 110 99 116",
  "111 112 32 43 43 32 109 105 100 100 108 101 32 43 43 32 101",
  "110 99 98 111 116 32 43 43 32 98 111 116 116 111 109 41 10",
  "10 124 124 124 32 82 101 110 100 101 114 32 116 104 105 115 32",
  "112 114 111 103 114 97 109 39 115 32 101 109 98 101 100 100 101",
  "100 32 101 110 99 111 100 101 100 32 115 111 117 114 99 101 32",
  "105 110 116 111 32 97 32 112 114 105 110 116 97 98 108 101 10",
  "124 124 124 32 113 117 105 110 101 46 10 114 101 110 100 101 114",
  "73 110 116 101 114 110 97 108 32 58 32 73 79 32 83 116 114",
  "105 110 103 10 114 101 110 100 101 114 73 110 116 101 114 110 97",
  "108 32 61 10 32 32 108 101 116 32 101 110 99 116 111 112 32",
  "61 32 99 97 116 83 116 114 105 110 103 115 32 40 102 115 116",
  "32 111 119 110 83 111 117 114 99 101 41 10 32 32 32 32 32",
  "32 101 110 99 98 111 116 32 61 32 99 97 116 83 116 114 105",
  "110 103 115 32 40 115 110 100 32 111 119 110 83 111 117 114 99",
  "101 41 10 32 32 105 110 32 100 111 32 109 105 100 100 108 101",
  "32 60 45 32 109 97 107 101 77 97 103 105 99 73 79 10 32",
  "32 32 32 32 32 32 32 116 111 112 32 60 45 32 109 97 121",
  "98 101 32 40 101 114 114 109 115 103 32 34 67 111 117 108 100",
  "32 110 111 116 32 100 101 99 111 100 101 32 115 111 117 114 99",
  "101 34 41 10 32 32 32 32 32 32 32 32 32 32 32 32 32",
  "32 32 40 112 117 114 101 32 46 32 114 101 110 100 101 114 41",
  "32 40 100 101 99 111 100 101 32 36 32 102 115 116 32 111 119",
  "110 83 111 117 114 99 101 41 10 32 32 32 32 32 32 32 32",
  "98 111 116 116 111 109 32 60 45 32 109 97 121 98 101 32 40",
  "101 114 114 109 115 103 32 34 67 111 117 108 100 32 110 111 116",
  "32 100 101 99 111 100 101 32 115 111 117 114 99 101 34 41 10",
  "32 32 32 32 32 32 32 32 32 32 32 32 32 32 32 32 32",
  "32 40 112 117 114 101 32 46 32 114 101 110 100 101 114 41 32",
  "40 100 101 99 111 100 101 32 36 32 115 110 100 32 111 119 110",
  "83 111 117 114 99 101 41 10 32 32 32 32 32 32 32 32 112",
  "117 114 101 32 40 116 111 112 32 43 43 32 101 110 99 116 111",
  "112 32 43 43 32 109 105 100 100 108 101 32 43 43 32 101 110",
  "99 98 111 116 32 43 43 32 98 111 116 116 111 109 41 10 10",
  "45 45 32 65 110 100 32 116 104 101 32 109 97 105 110 32 112",
  "114 111 103 114 97 109 10 10 124 124 124 32 84 104 101 32 109",
  "97 105 110 32 101 110 116 114 121 32 112 111 105 110 116 32 105",
  "110 116 111 32 116 104 101 32 112 114 111 103 114 97 109 10 109",
  "97 105 110 80 114 111 103 32 58 32 73 79 32 40 41 10 109",
  "97 105 110 80 114 111 103 32 61 10 32 32 100 111 32 97 114",
  "103 115 32 60 45 32 103 101 116 65 114 103 115 10 32 32 32",
  "32 32 99 97 115 101 32 97 114 103 115 32 111 102 10 32 32",
  "32 32 32 32 32 97 114 103 118 48 32 58 58 32 34 115 111",
  "117 114 99 101 34 32 58 58 32 78 105 108 32 61 62 10 32",
  "32 32 32 32 32 32 32 32 32 32 32 32 114 101 110 100 101",
  "114 73 110 116 101 114 110 97 108 32 62 62 61 32 112 117 116",
  "83 116 114 10 32 32 32 32 32 32 32 97 114 103 118 48 32",
  "58 58 32 34 109 97 107 101 45 113 117 105 110 101 34 32 58",
  "58 32 102 105 108 101 110 97 109 101 32 58 58 32 78 105 108",
  "32 61 62 10 32 32 32 32 32 32 32 32 32 32 32 32 32",
  "114 101 110 100 101 114 69 120 116 101 114 110 97 108 32 102 105",
  "108 101 110 97 109 101 32 62 62 61 32 112 117 116 83 116 114",
  "10 32 32 32 32 32 32 32 95 32 61 62 32 100 105 115 112",
  "108 97 121 73 110 102 111 10 10 10 10 111 119 110 83 111 117",
  "114 99 101 32 61 32 40 91 10"
],[ -- this is a MAGIC COMMENT
  "93 41 10 10 109 97 103 105 99 32 61 32 91 10 32 32 34",
  "57 51 32 52 52 32 57 49 32 51 50 32 52 53 32 52 53",
  "32 51 50 32 49 49 54 32 49 48 52 32 49 48 53 32 49",
  "49 53 32 51 50 32 49 48 53 32 49 49 53 32 51 50 32",
  "57 55 32 51 50 32 55 55 32 54 53 32 55 49 34 44 10",
  "32 32 34 55 51 32 54 55 32 51 50 32 54 55 32 55 57",
  "32 55 55 32 55 55 32 54 57 32 55 56 32 56 52 32 49",
  "48 34 10 93 10 10 110 97 109 101 115 112 97 99 101 32 77",
  "97 105 110 10 32 32 124 124 124 32 84 104 101 32 73 100 114",
  "105 115 32 49 32 99 111 109 112 105 108 101 114 32 114 101 113",
  "117 105 114 101 115 32 116 104 101 32 109 97 105 110 32 102 117",
  "110 99 116 105 111 110 32 116 111 32 98 101 32 119 105 116 104",
  "105 110 32 97 10 32 32 124 124 124 32 77 97 105 110 32 110",
  "97 109 101 115 112 97 99 101 46 10 32 32 109 97 105 110 32",
  "58 32 73 79 32 40 41 10 32 32 109 97 105 110 32 61 32",
  "109 97 105 110 80 114 111 103 10"
])

magic = [
  "93 44 91 32 45 45 32 116 104 105 115 32 105 115 32 97 32 77 65 71",
  "73 67 32 67 79 77 77 69 78 84 10"
]

namespace Main
  ||| The Idris 1 compiler requires the main function to be within a
  ||| Main namespace.
  main : IO ()
  main = mainProg