module Website

import Data.List
import Data.List1
import Data.Strings
import System
import System.File

-- This is Molly's website.
--
-- This webpage is the source code for an Idris 2 program (tested with version
-- 0.3.0). It prints a summary of the information presented below, and it's also
-- a quine, as it can print its own source code. (It's 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
  GitHub : (username : String) -> Link
  Irc : (net : String) -> (nick : String) -> Link
  Email : (user_part : String) -> (domain_part : String) -> Link
  Other : (desc : String) -> (url : String) -> Link

||| Relative links on my website.
slash : String -> String
slash = ("https://www.mollymiller.net/" ++)

||| Links to other places.
links : List Link
links = [
    Other "blog" (slash "blog"),
    GitHub "@sysvinit",
    Irc "Freenode" "sysvinit",
    Irc "Hackint" "sysvinit",
    Email "interwebs" "m-squa.red",
    Other "music feed" (slash "nowplaying")
]

||| 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 2021 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 2", "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 (Other desc url) = desc ++ " at " ++ 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 = wrap (map makePair ss) []
  where
    makePair : String -> (String, Nat)
    makePair s = (s, length s)

    wrap : List (String, Nat) -> List (List String, Nat) ->
           List (List String)
    wrap []        acc = reverse $ map (reverse . fst) acc
    wrap (x :: xs) []  = wrap xs $ pure (pure $ fst x, snd x)
    wrap (x :: xs) acc@(y :: ys) =
      if snd x >= len
        then wrap xs $ (pure $ fst x, snd x) :: acc
        else if snd x + snd y >= len
          then wrap xs $ (pure $ fst x, snd x) :: acc
          else wrap xs $ (fst x :: fst y, snd x + snd y) :: ys


||| 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) interests)
     putStrLn ""
     traverse_ putStrLn
               ((formatLines 9 . wrapLines 54 . map show) links)
     putStrLn ""
     traverse_ (putStrLn . indent 12 . show)
               (Prelude.(::) mainOccupation otherOccupations)
     putStrLn ""
     putStr (indent 6 (show copyright))
     putStr "; SPDX-License-Identifier: "
     putStrLn spdxLicenseIdentifier
     putStrLn ""

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

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

||| Encoded magic numbers.
magic : List Int

-- Functions which perform quine encoding and decoding.

||| Convert a list of integers into a stringified form which can be passed
||| back into the Idris compiler.
encode : List Int -> String
encode = foldr (++) "\n" . intersperse ",\n" .
         map concatLine . splitIntoLines
  where
    splitIntoLines : List a -> List (List a)
    splitIntoLines [] = []
    splitIntoLines xs = let (start, rest) = splitAt 15 xs
                        in start :: splitIntoLines rest

    concatLine : List Int -> String
    concatLine = ("  " ++) . pack . intercalate [',', ' '] .
                 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

||| Render the magic numbers.
renderedMagic : String
renderedMagic = render magic

||| Attempt to split an arbitrary program's input around a fixed point.
splitOnFixedPoint : String -> Either String (String, String)
splitOnFixedPoint str =
  let lines = (newlines . toList . split (== '\n')) str
  in case (toList . split (== renderedMagic)) 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 <- 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
     let enctop = (encode . map ord . unpack) top
     let encbot = (encode . map ord . unpack) bottom
     pure (top ++ enctop ++ renderedMagic ++ encbot ++ bottom)

||| Render this program's embedded encoded source into a printable
||| quine.
renderInternal : String
renderInternal =
  let top    = (render . fst) ownSource
      bottom = (render . snd) ownSource
      enctop = (encode . fst) ownSource
      encbot = (encode . snd) ownSource
  in top ++ enctop ++ renderedMagic ++ encbot ++ bottom

-- And the main program.

||| The main entry point into the program.
main : IO ()
main =
  do args <- getArgs
     case args of
       argv0 :: "source" :: Nil => putStr renderInternal
       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, 76, 105,
  115, 116, 10, 105, 109, 112, 111, 114, 116, 32, 68, 97, 116, 97, 46,
  76, 105, 115, 116, 49, 10, 105, 109, 112, 111, 114, 116, 32, 68, 97,
  116, 97, 46, 83, 116, 114, 105, 110, 103, 115, 10, 105, 109, 112, 111,
  114, 116, 32, 83, 121, 115, 116, 101, 109, 10, 105, 109, 112, 111, 114,
  116, 32, 83, 121, 115, 116, 101, 109, 46, 70, 105, 108, 101, 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, 50, 32, 112, 114, 111, 103, 114, 97, 109, 32, 40,
  116, 101, 115, 116, 101, 100, 32, 119, 105, 116, 104, 32, 118, 101, 114,
  115, 105, 111, 110, 10, 45, 45, 32, 48, 46, 51, 46, 48, 41, 46,
  32, 73, 116, 32, 112, 114, 105, 110, 116, 115, 32, 97, 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, 44, 32, 97, 110, 100,
  32, 105, 116, 39, 115, 32, 97, 108, 115, 111, 10, 45, 45, 32, 97,
  32, 113, 117, 105, 110, 101, 44, 32, 97, 115, 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, 46, 32,
  40, 73, 116, 39, 115, 32, 97, 108, 115, 111, 32, 97, 32, 113, 117,
  105, 110, 101, 32, 103, 101, 110, 101, 114, 97, 116, 111, 114, 44, 10,
  45, 45, 32, 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,
  46, 41, 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, 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,
  32, 32, 79, 116, 104, 101, 114, 32, 58, 32, 40, 100, 101, 115, 99,
  32, 58, 32, 83, 116, 114, 105, 110, 103, 41, 32, 45, 62, 32, 40,
  117, 114, 108, 32, 58, 32, 83, 116, 114, 105, 110, 103, 41, 32, 45,
  62, 32, 76, 105, 110, 107, 10, 10, 124, 124, 124, 32, 82, 101, 108,
  97, 116, 105, 118, 101, 32, 108, 105, 110, 107, 115, 32, 111, 110, 32,
  109, 121, 32, 119, 101, 98, 115, 105, 116, 101, 46, 10, 115, 108, 97,
  115, 104, 32, 58, 32, 83, 116, 114, 105, 110, 103, 32, 45, 62, 32,
  83, 116, 114, 105, 110, 103, 10, 115, 108, 97, 115, 104, 32, 61, 32,
  40, 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,
  34, 32, 43, 43, 41, 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, 10, 32, 32, 32, 32, 79, 116, 104, 101, 114, 32, 34, 98, 108,
  111, 103, 34, 32, 40, 115, 108, 97, 115, 104, 32, 34, 98, 108, 111,
  103, 34, 41, 44, 10, 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, 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, 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, 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, 44, 10, 32, 32, 32, 32, 79, 116, 104, 101, 114,
  32, 34, 109, 117, 115, 105, 99, 32, 102, 101, 101, 100, 34, 32, 40,
  115, 108, 97, 115, 104, 32, 34, 110, 111, 119, 112, 108, 97, 121, 105,
  110, 103, 34, 41, 10, 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, 49, 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, 32,
  50, 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,
  58, 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, 79, 116, 104, 101, 114,
  32, 100, 101, 115, 99, 32, 117, 114, 108, 41, 32, 61, 32, 100, 101,
  115, 99, 32, 43, 43, 32, 34, 32, 97, 116, 32, 34, 32, 43, 43,
  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, 32, 40, 109, 97, 112, 32, 109,
  97, 107, 101, 80, 97, 105, 114, 32, 115, 115, 41, 32, 91, 93, 10,
  32, 32, 119, 104, 101, 114, 101, 10, 32, 32, 32, 32, 109, 97, 107,
  101, 80, 97, 105, 114, 32, 58, 32, 83, 116, 114, 105, 110, 103, 32,
  45, 62, 32, 40, 83, 116, 114, 105, 110, 103, 44, 32, 78, 97, 116,
  41, 10, 32, 32, 32, 32, 109, 97, 107, 101, 80, 97, 105, 114, 32,
  115, 32, 61, 32, 40, 115, 44, 32, 108, 101, 110, 103, 116, 104, 32,
  115, 41, 10, 10, 32, 32, 32, 32, 119, 114, 97, 112, 32, 58, 32,
  76, 105, 115, 116, 32, 40, 83, 116, 114, 105, 110, 103, 44, 32, 78,
  97, 116, 41, 32, 45, 62, 32, 76, 105, 115, 116, 32, 40, 76, 105,
  115, 116, 32, 83, 116, 114, 105, 110, 103, 44, 32, 78, 97, 116, 41,
  32, 45, 62, 10, 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, 10, 32, 32, 32, 32, 119, 114, 97, 112, 32, 91, 93,
  32, 32, 32, 32, 32, 32, 32, 32, 97, 99, 99, 32, 61, 32, 114,
  101, 118, 101, 114, 115, 101, 32, 36, 32, 109, 97, 112, 32, 40, 114,
  101, 118, 101, 114, 115, 101, 32, 46, 32, 102, 115, 116, 41, 32, 97,
  99, 99, 10, 32, 32, 32, 32, 119, 114, 97, 112, 32, 40, 120, 32,
  58, 58, 32, 120, 115, 41, 32, 91, 93, 32, 32, 61, 32, 119, 114,
  97, 112, 32, 120, 115, 32, 36, 32, 112, 117, 114, 101, 32, 40, 112,
  117, 114, 101, 32, 36, 32, 102, 115, 116, 32, 120, 44, 32, 115, 110,
  100, 32, 120, 41, 10, 32, 32, 32, 32, 119, 114, 97, 112, 32, 40,
  120, 32, 58, 58, 32, 120, 115, 41, 32, 97, 99, 99, 64, 40, 121,
  32, 58, 58, 32, 121, 115, 41, 32, 61, 10, 32, 32, 32, 32, 32,
  32, 105, 102, 32, 115, 110, 100, 32, 120, 32, 62, 61, 32, 108, 101,
  110, 10, 32, 32, 32, 32, 32, 32, 32, 32, 116, 104, 101, 110, 32,
  119, 114, 97, 112, 32, 120, 115, 32, 36, 32, 40, 112, 117, 114, 101,
  32, 36, 32, 102, 115, 116, 32, 120, 44, 32, 115, 110, 100, 32, 120,
  41, 32, 58, 58, 32, 97, 99, 99, 10, 32, 32, 32, 32, 32, 32,
  32, 32, 101, 108, 115, 101, 32, 105, 102, 32, 115, 110, 100, 32, 120,
  32, 43, 32, 115, 110, 100, 32, 121, 32, 62, 61, 32, 108, 101, 110,
  10, 32, 32, 32, 32, 32, 32, 32, 32, 32, 32, 116, 104, 101, 110,
  32, 119, 114, 97, 112, 32, 120, 115, 32, 36, 32, 40, 112, 117, 114,
  101, 32, 36, 32, 102, 115, 116, 32, 120, 44, 32, 115, 110, 100, 32,
  120, 41, 32, 58, 58, 32, 97, 99, 99, 10, 32, 32, 32, 32, 32,
  32, 32, 32, 32, 32, 101, 108, 115, 101, 32, 119, 114, 97, 112, 32,
  120, 115, 32, 36, 32, 40, 102, 115, 116, 32, 120, 32, 58, 58, 32,
  102, 115, 116, 32, 121, 44, 32, 115, 110, 100, 32, 120, 32, 43, 32,
  115, 110, 100, 32, 121, 41, 32, 58, 58, 32, 121, 115, 10, 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,
  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, 57, 32, 46, 32, 119, 114, 97,
  112, 76, 105, 110, 101, 115, 32, 53, 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, 80, 114, 101, 108, 117, 100, 101, 46, 40, 58, 58, 41, 32,
  109, 97, 105, 110, 79, 99, 99, 117, 112, 97, 116, 105, 111, 110, 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, 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, 46, 10, 111, 119, 110, 83, 111, 117, 114, 99, 101,
  32, 58, 32, 40, 76, 105, 115, 116, 32, 73, 110, 116, 44, 32, 76,
  105, 115, 116, 32, 73, 110, 116, 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, 46, 10, 109, 97, 103, 105, 99, 32, 58, 32,
  76, 105, 115, 116, 32, 73, 110, 116, 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, 105,
  110, 116, 101, 103, 101, 114, 115, 32, 105, 110, 116, 111, 32, 97, 32,
  115, 116, 114, 105, 110, 103, 105, 102, 105, 101, 100, 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, 10, 124, 124, 124, 32, 98, 97, 99, 107,
  32, 105, 110, 116, 111, 32, 116, 104, 101, 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, 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, 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, 53, 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,
  40, 34, 32, 32, 34, 32, 43, 43, 41, 32, 46, 32, 112, 97, 99,
  107, 32, 46, 32, 105, 110, 116, 101, 114, 99, 97, 108, 97, 116, 101,
  32, 91, 39, 44, 39, 44, 32, 39, 32, 39, 93, 32, 46, 10, 32,
  32, 32, 32, 32, 32, 32, 32, 32, 32, 32, 32, 32, 32, 32, 32,
  32, 109, 97, 112, 32, 40, 117, 110, 112, 97, 99, 107, 32, 46, 32,
  99, 97, 115, 116, 41, 10, 32, 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, 82, 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, 114, 101, 110,
  100, 101, 114, 101, 100, 77, 97, 103, 105, 99, 32, 58, 32, 83, 116,
  114, 105, 110, 103, 10, 114, 101, 110, 100, 101, 114, 101, 100, 77, 97,
  103, 105, 99, 32, 61, 32, 114, 101, 110, 100, 101, 114, 32, 109, 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, 116, 111, 76, 105, 115, 116, 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, 99, 97,
  115, 101, 32, 40, 116, 111, 76, 105, 115, 116, 32, 46, 32, 115, 112,
  108, 105, 116, 32, 40, 61, 61, 32, 114, 101, 110, 100, 101, 114, 101,
  100, 77, 97, 103, 105, 99, 41, 41, 32, 108, 105, 110, 101, 115, 32,
  111, 102, 10, 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, 95, 32, 32, 32, 32, 32, 32, 32,
  32, 32, 32, 32, 32, 32, 32, 32, 32, 32, 32, 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, 99, 97,
  115, 101, 32, 114, 101, 115, 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, 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, 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, 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, 114, 101, 110, 100, 101, 114, 101,
  100, 77, 97, 103, 105, 99, 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, 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, 116, 111, 112, 32, 32, 32, 32, 61, 32, 40, 114,
  101, 110, 100, 101, 114, 32, 46, 32, 102, 115, 116, 41, 32, 111, 119,
  110, 83, 111, 117, 114, 99, 101, 10, 32, 32, 32, 32, 32, 32, 98,
  111, 116, 116, 111, 109, 32, 61, 32, 40, 114, 101, 110, 100, 101, 114,
  32, 46, 32, 115, 110, 100, 41, 32, 111, 119, 110, 83, 111, 117, 114,
  99, 101, 10, 32, 32, 32, 32, 32, 32, 101, 110, 99, 116, 111, 112,
  32, 61, 32, 40, 101, 110, 99, 111, 100, 101, 32, 46, 32, 102, 115,
  116, 41, 32, 111, 119, 110, 83, 111, 117, 114, 99, 101, 10, 32, 32,
  32, 32, 32, 32, 101, 110, 99, 98, 111, 116, 32, 61, 32, 40, 101,
  110, 99, 111, 100, 101, 32, 46, 32, 115, 110, 100, 41, 32, 111, 119,
  110, 83, 111, 117, 114, 99, 101, 10, 32, 32, 105, 110, 32, 116, 111,
  112, 32, 43, 43, 32, 101, 110, 99, 116, 111, 112, 32, 43, 43, 32,
  114, 101, 110, 100, 101, 114, 101, 100, 77, 97, 103, 105, 99, 32, 43,
  43, 32, 101, 110, 99, 98, 111, 116, 32, 43, 43, 32, 98, 111, 116,
  116, 111, 109, 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, 46, 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, 46, 10, 109,
  97, 105, 110, 32, 58, 32, 73, 79, 32, 40, 41, 10, 109, 97, 105,
  110, 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, 32, 112, 117, 116, 83, 116, 114, 32, 114, 101, 110, 100, 101,
  114, 73, 110, 116, 101, 114, 110, 97, 108, 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, 57, 51, 44, 32, 52, 52, 44, 32, 57, 49, 44, 32, 51, 50,
  44, 32, 52, 53, 44, 32, 52, 53, 44, 32, 51, 50, 44, 32, 49,
  49, 54, 44, 32, 49, 48, 52, 44, 32, 49, 48, 53, 44, 32, 49,
  49, 53, 44, 32, 51, 50, 44, 32, 49, 48, 53, 44, 32, 49, 49,
  53, 44, 32, 51, 50, 44, 32, 57, 55, 44, 10, 32, 32, 51, 50,
  44, 32, 55, 55, 44, 32, 54, 53, 44, 32, 55, 49, 44, 32, 55,
  51, 44, 32, 54, 55, 44, 32, 51, 50, 44, 32, 54, 55, 44, 32,
  55, 57, 44, 32, 55, 55, 44, 32, 55, 55, 44, 32, 54, 57, 44,
  32, 55, 56, 44, 32, 56, 52, 44, 32, 49, 48, 10, 93, 10, 10,
  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
]