content: {-# LANGUAGE ConstraintKinds #-}
  {-# LANGUAGE DataKinds #-}
  {-# LANGUAGE DeriveFoldable #-}
  {-# LANGUAGE FlexibleContexts #-}
  {-# LANGUAGE FlexibleInstances #-}
  {-# LANGUAGE GADTs #-}
  {-# LANGUAGE MultiParamTypeClasses #-}
  {-# LANGUAGE OverloadedStrings #-}
  {-# LANGUAGE ScopedTypeVariables #-}
  {-# LANGUAGE StandaloneDeriving #-}
  {-# LANGUAGE GeneralizedNewtypeDeriving #-}
  {-# LANGUAGE TypeApplications #-}
  {-# LANGUAGE TypeFamilies #-}
  {-# LANGUAGE TupleSections #-}
  {-# LANGUAGE UndecidableInstances #-}
  {-# LANGUAGE ViewPatterns #-}
  
  {-# OPTIONS_GHC -Wall #-}
  {-# OPTIONS_GHC -Wno-missing-methods #-}
  {-# OPTIONS_GHC -Wno-name-shadowing #-}
  {-# OPTIONS_GHC -Wno-type-defaults #-}
  {-# OPTIONS_GHC -Wno-incomplete-patterns #-}
  {-# OPTIONS_GHC -Wno-orphans #-}
  
  module Main where
  
  import Control.Applicative
  import Test.QuickCheck.Monadic
  import Test.Tasty
  import Test.Tasty.QuickCheck as QC hiding ((.&.))
  import Test.QuickCheck.Unicode
  import System.Environment
  import qualified Data.Text (null, pack, unpack)
  import Data.Maybe
  import Data.Bool (bool)
  import Data.Proxy
  import GHC.Natural
  import GHC.TypeLits hiding (Text)
  import qualified Data.Word
  import qualified Data.Int
  import Data.Bits (Bits(..), FiniteBits(..))
  import Numeric
  import Data.List (intercalate)
  
  import Turtle
  import Embedder
  -- import Debug.Trace (traceShowId, traceShow)
  
  
  main :: IO ()
  main = do
    putStrLn "Probing embedders..."
    good <- isHealthy embedder
    goodDrun <- isHealthy Drun
    putStrLn . ("Found " <>) . (<> ".") . intercalate " and " . map embedderCommand
                 $ [ embedder | good ] <> [ Drun | goodDrun ]
    let tests :: TestTree
        tests = testGroup "Motoko tests" . concat
                 $ [ [arithProps, conversionProps, utf8Props, matchingProps] | good ]
                 <> [ [encodingProps] | goodDrun ]
  
    if not (good || goodDrun)
    then putStrLn "No embedder available for testing. Done..."
    else setEnv "TASTY_NUM_THREADS" "1" >> defaultMain tests
  
  arithProps :: TestTree
  arithProps = testGroup "Arithmetic/logic"
    [ QC.testProperty "expected failures" $ prop_rejects
    , QC.testProperty "expected successes" $ prop_verifies
    ]
  
  conversionProps :: TestTree
  conversionProps = testGroup "Numeric conversions"
    [ QC.testProperty "roundtrip Nat64 Nat Nat64 " $ prop_roundtripNatWNW @64
    , QC.testProperty "roundtrip Nat32 Nat Nat32 " $ prop_roundtripNatWNW @32
    , QC.testProperty "roundtrip Nat16 Nat Nat16 " $ prop_roundtripNatWNW @16
    , QC.testProperty "roundtrip Nat8 Nat Nat8 " $ prop_roundtripNatWNW @8
    , QC.testProperty "roundtrip Int64 Nat Nat64 " $ prop_roundtripIntWNW @64
    , QC.testProperty "roundtrip Int32 Nat Nat32 " $ prop_roundtripIntWNW @32
    , QC.testProperty "roundtrip Int16 Nat Nat16 " $ prop_roundtripIntWNW @16
    , QC.testProperty "roundtrip Int8 Nat Nat8 " $ prop_roundtripIntWNW @8
    , QC.testProperty "modulo Nat Nat64 Nat" $ prop_moduloNWN @64
    , QC.testProperty "modulo Nat Nat32 Nat" $ prop_moduloNWN @32
    , QC.testProperty "modulo Nat Nat16 Nat" $ prop_moduloNWN @16
    , QC.testProperty "modulo Nat Nat8 Nat" $ prop_moduloNWN @8
    ]
  
  utf8Props :: TestTree
  utf8Props = testGroup "UTF-8 coding"
    [ QC.testProperty "explode >>> concat roundtrips" $ prop_explodeConcat
    , QC.testProperty "charToText >>> head roundtrips" $ prop_charToText
    , QC.testProperty "length computation" $ prop_textLength
    , QC.testProperty "chunky concat (ropes)" $ prop_ropeConcat
    , QC.testProperty "chunky length (ropes)" $ prop_ropeLength
    , QC.testProperty "chunky iterator (ropes)" $ prop_ropeIterator
    ]
  
  matchingProps :: TestTree
  matchingProps = testGroup "Pattern matching" $
    [ QC.testProperty "intra-actor" $ prop_matchStructured ]
  
  
  -- these require messaging
  encodingProps :: TestTree
  encodingProps = testGroup "Encoding" $
    [ QC.testProperty "inter-actor" $ withMaxSuccess 20 prop_matchInActor
    , QC.testProperty "encoded-Nat" $ withMaxSuccess 10 prop_matchActorNat
    , QC.testProperty "encoded-Int" $ withMaxSuccess 10 prop_matchActorInt
    , QC.testProperty "encoded-Text" $ withMaxSuccess 10 prop_matchActorText
    ]
  
  
  withPrim :: Line -> Line
  withPrim = (fromString "import Prim \"mo:⛔\";" <>)
  
  runner :: Embedder -> ExitCode -> (Bool -> Bool) -> Turtle.FilePath -> String -> PropertyM IO ()
  runner embedder reqOutcome relevant name testCase =
      let as = name <.> "mo"
          wasm = name <.> "wasm"
          fileArg = fromString . encodeString
          script = do Turtle.output as $ withPrim <$> fromString testCase
                      res@(exitCode, _, _) <- procStrictWithErr "moc"
                        (addCompilerArgs embedder ["--legacy-actors", "-no-check-ir", fileArg as]) empty
                      if ExitSuccess == exitCode
                      then (True,) <$> invokeEmbedder embedder wasm
                      else pure (False, res)
      in run script >>= assertOutcomeCheckingFuzz reqOutcome relevant
  
  runScriptNoFuzz    :: Turtle.FilePath -> String -> PropertyM IO ()
  runScriptWantFuzz  :: Turtle.FilePath -> String -> PropertyM IO ()
  drunScriptNoFuzz   :: Turtle.FilePath -> String -> PropertyM IO ()
  drunScriptWantFuzz :: Turtle.FilePath -> String -> PropertyM IO ()
  
  (runScriptNoFuzz, runScriptWantFuzz) = (runEmbedder ExitSuccess id, runEmbedder (ExitFailure 134) not)
      where runEmbedder = runner embedder
  (drunScriptNoFuzz, drunScriptWantFuzz) = (runEmbedder ExitSuccess id, runEmbedder (ExitFailure 1) not)
      where runEmbedder = runner Drun
  
  prop_explodeConcat :: UTF8 String -> Property
  prop_explodeConcat (UTF8 str) = monadicIO $ do
    let testCase :: String
        testCase = "do { var str = \"\"; for (c in \""
                   <> s <> "\".chars()) { str #= Prim.charToText c }; assert (str == \"" <> s <> "\") }"
  
        s = concatMap escape str
    runScriptNoFuzz "explodeConcat" testCase
  
  -- TODO: why can't we use Test.QuickCheck.Unicode.Unicode? (see https://github.com/bos/quickcheck-unicode/issues/5)
  newtype UTF8 a = UTF8 a deriving Show
  
  instance Arbitrary (UTF8 String) where
    arbitrary = UTF8 <$> string1
  
  instance Arbitrary (UTF8 Char) where
    arbitrary = UTF8 <$> Test.QuickCheck.Unicode.char
  
  hex :: Int -> String
  hex = (`showHex` "")
  
  escape :: Char -> String
  escape ch | '\\' `elem` show ch = "\\u{" <> hex (fromEnum ch) <> "}"
  escape '"' = "\\\""
  escape ch = pure ch
  
  prop_charToText :: UTF8 Char -> Property
  prop_charToText (UTF8 char) = monadicIO $ do
    let testCase = "assert (switch ((Prim.charToText '"
                   <> c <> "').chars().next()) { case (?'" <> c <> "') true; case _ false })"
  
        c = escape char
    runScriptNoFuzz "charToText" testCase
  
  prop_textLength :: UTF8 [Char] -> Property
  prop_textLength (UTF8 text) = monadicIO $ do
    let testCase = "assert(\"" <> (text >>= escape) <> "\".size() == " <> show (length text) <> ")"
    runScriptNoFuzz "textLength" testCase
  
  data Rope a = EmptyChunk | Chunk a | UTF8Chunk a | LongChunk a | Rope a `Rope` Rope a deriving (Eq, Show, Foldable)
  
  instance Semigroup (Rope a) where
    (<>) = Rope
  
  instance Monoid (Rope a) where
    mempty = EmptyChunk
  
  instance Arbitrary (Rope String) where
    arbitrary = frequency [ (2, pure mempty)
                          , (4, Chunk <$> arbitrary)
                          , (5, elements [ UTF8Chunk "Медве́ди хо́дят по у́лицам. Коне́чно, э́то непра́вда!"
                                         , UTF8Chunk "Boci, boci tarka, se füle, se farka, oda megyünk lakni, ahol tejet kapni."
                                         , UTF8Chunk "十年树木，百年树人" ])
                          , (7, pure $ LongChunk "The quick brown fox jumps over the lazy dog")
                          , (3, Rope <$> arbitrary <*> arbitrary) ]
  
  instance Semigroup (MOTerm String) where
    (<>) = Concat
  
  instance Monoid (MOTerm String) where
    mempty = Text mempty
  
  asString :: Rope String -> String
  asString = foldMap id
  
  asMot :: Rope String -> MOTerm String
  asMot = foldMap Text
  
  prop_ropeConcat :: Rope String -> Property
  prop_ropeConcat rope = monadicIO $ do
    let testCase = "assert (" <> ropeMot <> " == " <> string <> ")"
        string = unparseMO (Text (asString rope))
        ropeMot = unparseMO (asMot rope)
    runScriptNoFuzz "ropeConcat" testCase
  
  prop_ropeLength :: Rope String -> Property
  prop_ropeLength rope = monadicIO $ do
    let testCase = "assert (" <> ropeMot <> ".size() == " <> show len <> ")"
        len = length (asString rope)
        ropeMot = unparseMO (asMot rope)
    runScriptNoFuzz "ropeLength" testCase
  
  prop_ropeIterator :: Rope String -> Property
  prop_ropeIterator rope = monadicIO $ do
    let testCase = "func same(c : ?Char, d : Char) : Bool = switch c { case (?cc) { cc == d }; case null false };"
                <> "let i = (" <> ropeMot <> ").chars();"
                <> concatMap testStep string
                <> "assert (switch (i.next()) { case null true; case _ false })"
        testStep c = "assert (same(i.next(), '" <> escape c <> "'));"
        string = asString rope
        ropeMot = unparseMO (asMot rope)
    runScriptNoFuzz "ropeLength" testCase
  
  
  assertOutcomeCheckingFuzz ::
      ExitCode -> (Bool -> Bool) -> (Bool, (ExitCode, Text, Text)) -> PropertyM IO ()
  assertOutcomeCheckingFuzz outcome relevant (compiled, (exitCode, out, err)) = do
    let fuzzErr = not $ Data.Text.null err
        fuzzErrRelevant = relevant fuzzErr
    when (fuzzErr && fuzzErrRelevant) $ do
      monitor (counterexample "STDERR:")
      monitor (counterexample . Data.Text.unpack $ err)
    let fuzzOut = not $ Data.Text.null out
    when fuzzOut $ do
      monitor (counterexample "STDOUT:")
      monitor (counterexample . Data.Text.unpack $ out)
    assert (not $ outcome /= exitCode || (if compiled then fuzzErrRelevant else fuzzErr) || fuzzOut)
  
  assertSuccessNoFuzz :: (Bool, (ExitCode, Text, Text)) -> PropertyM IO ()
  assertSuccessNoFuzz = assertOutcomeCheckingFuzz ExitSuccess id
  
  newtype Failing = Failing (MOTerm Integer)
  
  instance Arbitrary Failing where
    arbitrary = Failing <$> suchThat (resize 5 arbitrary) (\(evaluate @Integer -> res) -> null res)
    shrink (Failing term) = do
      term' <- shrink term
      Nothing <- pure $ evaluate term'
      pure $ Failing term'
  
  unparseFailing :: Failing -> String
  unparseFailing (Failing t) = "let _ = " ++ unparseMO t ++ ";"
  
  instance Show Failing where
      show = unparseFailing
  
  prop_rejects :: Failing -> Property
  prop_rejects f = monadicIO $ runScriptWantFuzz "fails" (unparseFailing f)
  
  newtype TestCase = TestCase (MOTerm Integer)
  
  unparseTestCase :: TestCase -> String
  unparseTestCase (TestCase t) =
    let actual = unparseMO t in
    let Just expected = evaluate @Integer t in
    "assert (" ++ actual ++ " == " ++ show expected ++ ");"
  
  instance Show TestCase where show = unparseTestCase
  
  instance Arbitrary TestCase where
    arbitrary = TestCase <$> suchThat (resize 5 arbitrary) (isJust . evaluate @Integer)
    shrink (TestCase term) = do
      term' <- shrink term
      Just _ <- pure $ evaluate term'
      pure $ TestCase term'
  
  newtype TestCases = TestCases [TestCase]
  
  instance Show TestCases where
    show (TestCases tcs) = unlines $ map unparseTestCase tcs
  
  instance Arbitrary TestCases where
    arbitrary = TestCases <$> vector 10
    shrink (TestCases tcs) = TestCases <$> shrink tcs
  
  prop_verifies :: TestCases -> Property
  prop_verifies (TestCases tcs) = monadicIO $ do
    Turtle.output "tests.mo" $ msum $ pure (withPrim mempty) : [ fromString (unparseTestCase tc) | tc <- tcs ]
    res@(exitCode, _, _) <- procStrictWithErr "moc"
             (addCompilerArgs embedder ["--legacy-actors", "-no-check-ir", "tests.mo"]) empty
    res' <- if exitCode == ExitSuccess
            then (True,) <$> procStrictWithErr (embedderCommand embedder) (addEmbedderArgs embedder ["tests.wasm"]) empty
            else pure (False, res)
    assertSuccessNoFuzz res'
  
  
  newtype ConversionTestNat n = ConversionTestNat (Neuralgic (BitLimited n Natural)) deriving (Show, Arbitrary)
  newtype ConversionTestInt n = ConversionTestInt (Neuralgic (BitLimited n Integer)) deriving (Show, Arbitrary)
  
  prop_roundtripNatWNW :: WordLike n => ConversionTestNat n -> Property
  prop_roundtripNatWNW (ConversionTestNat n) = do
      let expected = Neuralgic n
      let actual = ConvertNatToNatN (ConvertNatNToNat expected)
      let testCase = "assert(" <> unparseMO (actual `Equals` expected) <> ")"
      monadicIO $ runScriptNoFuzz "roundtripWNW" testCase
  prop_roundtripIntWNW :: WordLike n => ConversionTestInt n -> Property
  prop_roundtripIntWNW (ConversionTestInt n) = do
      let expected = Neuralgic n
      let actual = ConvertIntToIntN (ConvertIntNToInt expected)
      let testCase = "assert(" <> unparseMO (actual `Equals` expected) <> ")"
      monadicIO $ runScriptNoFuzz "roundtripWNW" testCase
  
  
  newtype ModuloTest (n :: Nat) = ModuloTest (MOTerm (BitLimited n Natural)) deriving Show
  
  instance WordLike n => Arbitrary (ModuloTest n) where
    arbitrary = ModuloTest . ConvertNatToNatN @n . Neuralgic <$> (arbitrary :: Gen (Neuralgic Natural))
  
  prop_moduloNWN :: forall n . KnownNat n => ModuloTest n -> Property
  prop_moduloNWN (ModuloTest term@(ConvertNatToNatN (Neuralgic m))) = monadicIO $ runScriptNoFuzz "moduloNWN" testCase
    where m' = evalN m .&. maskFor term
          testCase = "assert(" <> unparseMO (ConvertNatNToNat term)
                  <> " == " <> show m' <> ")"
  
  data Matching where
    Matching :: (AnnotLit t, MOValue t, Show t, Evaluatable t, Arbitrary (MOTerm t)) => (MOTerm t, t) -> Matching
  
  deriving instance Show Matching
  
  
  instance Arbitrary Matching where
    arbitrary = oneof [ realise Matching <$> gen @Bool
                      , realise Matching <$> gen @(Bool, Bool)
                      , realise Matching <$> gen @(Bool, Integer)
                      , realise Matching <$> gen @((Bool, Natural), Integer)
                      , realise Matching <$> gen @(BitLimited 8 Natural, BitLimited 8 Integer)
                      , realise Matching <$> gen @(Maybe Integer)
                      ]
      where gen :: (Arbitrary (MOTerm a), Evaluatable a) => Gen (MOTerm a, Maybe a)
            gen = (do term <- arbitrary
                      let val = evaluate term
                      pure (term, val)) `suchThat` (isJust . snd)
            realise f (tm, Just v) = f (tm, v)
    shrink (Matching (term, _val)) = do
      term' <- shrink term
      Just val' <- pure $ evaluate term'
      pure $ Matching (term', val')
  
  prop_matchStructured :: Matching -> Property
  prop_matchStructured (Matching a) = locally a
  
  locally :: (AnnotLit t, MOValue t) => (MOTerm t, t) -> Property
  locally (tm, v) = monadicIO $ do
    let testCase = "assert (switch (" <> expr <> ") { case (" <> eval'd <> ") true; case _ false })"
  
        eval'd = unparse v
        expr = unparseMO tm
    runScriptNoFuzz "matchLocally" testCase
  
  prop_matchInActor :: Matching -> Property
  prop_matchInActor (Matching a) = mobile a
  
  mobile :: (AnnotLit t, MOValue t) => (MOTerm t, t) -> Property
  mobile (tm, v) = monadicIO $ do
    let testCase = "actor { public func match (b : " <> typed <> ") : async () { assert (switch b { case (" <> eval'd <> ") true; case _ false }) }; public func go () : async () { let res = await match (" <> expr <> " : " <> typed <> "); return res } };"
  
        eval'd = unparse v
        typed = unparseType v
        expr = unparseMO tm
    drunScriptNoFuzz "matchMobile" testCase
  
  
  prop_matchActorNat :: Neuralgic Natural -> Property
  prop_matchActorNat nat = monadicIO $ do
      let testCase = format ("actor { public func match (n : Nat) : async () { assert (switch n { case ("%d%") true; case _ false }) }; public func go () : async () { let res = await match ("%d%" : Nat); return res } };") eval'd eval'd
          eval'd = evalN nat
      drunScriptNoFuzz "matchActorNat" (Data.Text.unpack testCase)
  
  prop_matchActorInt :: Neuralgic Integer -> Property
  prop_matchActorInt int = monadicIO $ do
      let testCase = format ("actor { public func match (i : Int) : async () { assert (switch i { case ("%d%") true; case _ false }) }; public func go () : async () { let res = await match ("%d%" : Int); return res } };") eval'd eval'd
          eval'd = evalN int
      drunScriptNoFuzz "matchActorInt" (Data.Text.unpack testCase)
  
  prop_matchActorText :: UTF8 String -> Property
  prop_matchActorText (UTF8 text) = monadicIO $ do
      let testCase = format ("actor { public func match (i : Text) : async () { assert (switch i { case (\""%s%"\") true; case _ false }) }; public func go () : async () { let res = await match (\""%s%"\" : Text); return res } };") eval'd eval'd
          eval'd = Data.Text.pack $ text >>= escape
      drunScriptNoFuzz "matchActorText" (Data.Text.unpack testCase)
  
  -- instances of MOValue describe "ground values" in
  -- Motoko. These can appear in patterns and have
  -- well-defined Motoko type.
  --
  class MOValue a where
    unparseType :: a -> String
    unparse :: a -> String
  
  instance MOValue Bool where
    unparseType _ = "Bool"
    unparse = unparseMO . Bool
  
  instance MOValue Integer where
    unparseType _ = "Int"
    unparse = show
  
  instance MOValue Natural where
    unparseType _ = "Nat"
    unparse = show
  
  instance KnownNat n => MOValue (BitLimited n Natural) where
    unparseType _ = "Nat" <> bitWidth (Proxy @n)
    unparse (NatN a) = annot (Five @(BitLimited n Natural)) (show a)
  
  instance KnownNat n => MOValue (BitLimited n Integer) where
    unparseType _ = "Int" <> bitWidth (Proxy @n)
    unparse (IntN a) = annot (Five @(BitLimited n Integer)) (show a)
  
  instance (MOValue a, MOValue b) => MOValue (a, b) where
    unparseType (a, b) = "(" <> unparseType a <> ", " <> unparseType b <> ")"
    unparse (a, b) = "(" <> unparse a <> ", " <> unparse b <> ")"
  
  instance (MOValue a, MOValue b, MOValue c) => MOValue (a, b, c) where
    unparseType (a, b, c) = "(" <> unparseType a <> ", " <> unparseType b <> ", " <> unparseType c <> ")"
    unparse (a, b, c) = "(" <> unparse a <> ", " <> unparse b <> ", " <> unparse c <> ")"
  
  instance MOValue a => MOValue (Maybe a) where
    unparseType Nothing = "Null"
    unparseType (Just a) = "?" <> unparseType a
    unparse Nothing = "null"
    unparse (Just a) = "?" <> unparse a
  
  -- wiggle room around an *important value*
  -- think of it as a "fuzz"
  --
  data Off = TwoLess | OneLess | OneMore | TwoMore
   deriving (Enum, Eq, Ord, Show)
  
  instance Arbitrary Off where
    arbitrary = elements [TwoLess .. TwoMore]
  
  -- Below data structure tries to focus test case generation of
  -- numeric values to *neuralgic points* of the numeric line, namely
  -- areas where (from our white-box knowledge of Motoko's inner
  -- workings) representation changes are expected to happen. These
  -- are mostly at a power-of-two boundary and around it, e.g. we have
  -- signed 30 bit numbers (`Int` and `Nat`) that have a compact representation
  -- and out of this range the number gets heap-allocated.
  --
  data Neuralgic t
    = LargeNeg
    | AroundNeg Integer
    | Around0
    | AroundPos Integer
    | LargePos
    | Offset (Neuralgic t) Off
   deriving (Eq, Ord, Show)
  
  instance Arbitrary (Neuralgic Integer) where
    arbitrary = frequency [ (5, elements [LargeNeg, AroundNeg 63, AroundNeg 30, Around0, AroundPos 30, AroundPos 63, LargePos])
                          , (8, Offset <$> arbitrary <*> arbitrary)]
  
  
  guardedFrom :: (Arbitrary (Neuralgic a), Integral a) =>
                (Integer -> Maybe a) -> [Neuralgic a] -> Gen (Neuralgic a)
  pred `guardedFrom` set = frequency [ (5, elements set)
                                     , (3, Offset <$> arbitrary <*> arbitrary)]
                           `suchThat` (isJust . guardedEvalN pred)
  infix 1 `guardedFrom`
  
  instance Arbitrary (Neuralgic Natural) where
    arbitrary =  (\n -> if n >= 0 then pure (fromIntegral n) else Nothing)
                 `guardedFrom` [Around0, AroundPos 30, AroundPos 63, LargePos, AroundPos 77]
  
  instance KnownNat n => Arbitrary (Neuralgic (BitLimited n Natural)) where
    arbitrary = fmap NatN <$> trapNat bits `guardedFrom` menu bits
      where bits = natVal (Proxy @n)
            menu 8 = [Around0, AroundPos 3, AroundPos 5, AroundPos 8]
            menu 16 = [Around0, AroundPos 3, AroundPos 5, AroundPos 8, AroundPos 13, AroundPos 16]
            menu 32 = [Around0, AroundPos 8, AroundPos 13, AroundPos 16, AroundPos 23, AroundPos 32]
            menu 64 = [Around0, AroundPos 8, AroundPos 13, AroundPos 23, AroundPos 31, AroundPos 47, AroundPos 64]
  
  
  instance KnownNat n => Arbitrary (Neuralgic (BitLimited n Integer)) where
    arbitrary = fmap IntN <$> trapInt bits `guardedFrom` menu bits
      where bits = natVal (Proxy @n)
            menu 8 = [Around0, AroundNeg 3, AroundNeg 5, AroundNeg 7, AroundPos 3, AroundPos 5, AroundPos 7]
            menu 16 = [Around0, AroundNeg 3, AroundNeg 7, AroundNeg 10, AroundNeg 15, AroundPos 3, AroundPos 8, AroundPos 10, AroundPos 15]
            menu 32 = [Around0, AroundNeg 3, AroundNeg 17, AroundNeg 27, AroundNeg 31, AroundPos 3, AroundPos 18, AroundPos 25, AroundPos 31]
            menu 64 = [Around0, AroundNeg 9, AroundNeg 27, AroundNeg 51, AroundNeg 63, AroundPos 10, AroundPos 28, AroundPos 55, AroundPos 63]
  
  
  data MOTerm :: * -> * where
    -- Comparisons
    NotEqual, Equals, GreaterEqual, Greater, LessEqual, Less
      :: (AnnotLit a, Evaluatable a, Arbitrary (MOTerm a)) =>
         MOTerm a -> MOTerm a -> MOTerm Bool
    -- Short-circuit
    ShortAnd, ShortOr
      :: MOTerm Bool -> MOTerm Bool -> MOTerm Bool
    -- Boolean
    Not :: MOTerm Bool -> MOTerm Bool
    Bool :: Bool -> MOTerm Bool
    -- Bitwise
    Complement :: MOTerm (BitLimited n a) -> MOTerm (BitLimited n a)
    Or, And, Xor, RotL, RotR, ShiftL, ShiftR
      :: MOTerm (BitLimited n a) -> MOTerm (BitLimited n a) -> MOTerm (BitLimited n a)
    PopCnt, Clz, Ctz :: MOTerm (BitLimited n a) -> MOTerm (BitLimited n a)
    -- Arithmetic
    Pos, Neg, Abs :: MOTerm a -> MOTerm a
    Add, Sub, Mul, Div, Mod, Pow :: MOTerm a -> MOTerm a -> MOTerm a
    -- Wrapping Arithmetic
    WrapAdd, WrapSub, WrapMul, WrapPow
      :: MOTerm (BitLimited n a) -> MOTerm (BitLimited n a) -> MOTerm (BitLimited n a)
    -- Numeric
    Lit :: Integer -> MOTerm a
    Neuralgic :: Neuralgic a -> MOTerm a
    Five :: MOTerm a
    -- Text
    Text :: String -> MOTerm String
    Concat :: MOTerm String -> MOTerm String -> MOTerm String
    -- Conditional
    IfThenElse :: MOTerm a -> MOTerm a -> MOTerm Bool -> MOTerm a
    -- Conversion
    ConvertNatural :: MOTerm Natural -> MOTerm Integer
    ConvertNatToNatN :: WordLike n => MOTerm Natural -> MOTerm (BitLimited n Natural)
    ConvertNatNToNat :: WordLike n => MOTerm (BitLimited n Natural) -> MOTerm Natural
    ConvertIntToIntN :: WordLike n => MOTerm Integer -> MOTerm (BitLimited n Integer)
    ConvertIntNToInt :: WordLike n => MOTerm (BitLimited n Integer) -> MOTerm Integer
    -- Constructors (intro forms)
    Pair ::
      ( AnnotLit a, AnnotLit b
      , Evaluatable a, Evaluatable b
      , Arbitrary (MOTerm a), Arbitrary (MOTerm b)
      ) => MOTerm a -> MOTerm b -> MOTerm (a, b)
    Triple ::
      ( AnnotLit a, AnnotLit b, AnnotLit c
      , Evaluatable a, Evaluatable b, Evaluatable c
      , Arbitrary (MOTerm a), Arbitrary (MOTerm b), Arbitrary (MOTerm c)
      ) => MOTerm a -> MOTerm b -> MOTerm c -> MOTerm (a, b, c)
    Array :: MOTerm a -> MOTerm [a] -- not matchable!
    Null :: MOTerm (Maybe a)
    Some :: (AnnotLit a, Evaluatable a, Arbitrary (MOTerm a)) => MOTerm a -> MOTerm (Maybe a)
    -- Variants, Objects (TODO)
  
  shrinkRel2 :: (Arbitrary a, Arbitrary b) => (a -> b -> c) -> a -> b -> [c]
  shrinkRel2 f a b = concat
      [ (\a -> f a b) <$> shrink a
      , (\b -> f a b) <$> shrink b
      ]
  
  shrinkRel3 :: (Arbitrary a, Arbitrary b, Arbitrary c) => (a -> b -> c -> d) -> a -> b -> c -> [d]
  shrinkRel3 f a b c = concat
      [ (\a -> f a b c) <$> shrink a
      , (\b -> f a b c) <$> shrink b
      , (\c -> f a b c) <$> shrink c
      ]
  
  shrinkOp2 :: Arbitrary a => (a -> a -> a) -> a -> a -> [a]
  shrinkOp2 f a b = a : b : shrinkRel2 f a b
  
  shrinkOp1 :: Arbitrary a => (a -> a) -> a -> [a]
  shrinkOp1 f a = a : (f <$> shrink a)
  
  subShrink :: Arbitrary (MOTerm t) => MOTerm t -> [MOTerm t]
  subShrink Five = []
  subShrink (Lit _) = []
  subShrink (Neuralgic _) = []
  subShrink (Pos n) = shrinkOp1 Pos n
  subShrink (Neg n) = shrinkOp1 Neg n
  subShrink (Abs n) = shrinkOp1 Abs n
  subShrink (a `Add` b) = shrinkOp2 Add a b
  subShrink (a `Sub` b) = shrinkOp2 Sub a b
  subShrink (a `Mul` b) = shrinkOp2 Mul a b
  subShrink (a `Div` b) = shrinkOp2 Div a b
  subShrink (a `Mod` b) = shrinkOp2 Mod a b
  subShrink (a `Or` b) = shrinkOp2 Or a b
  subShrink (a `And` b) = shrinkOp2 And a b
  subShrink (a `Xor` b) = shrinkOp2 Xor a b
  subShrink (a `RotL` b) = shrinkOp2 RotL a b
  subShrink (a `RotR` b) = shrinkOp2 RotR a b
  subShrink (a `ShiftL` b) = shrinkOp2 ShiftL a b
  subShrink (a `ShiftR` b) = shrinkOp2 ShiftR a b
  subShrink (a `WrapAdd` b) = shrinkOp2 WrapAdd a b
  subShrink (a `WrapSub` b) = shrinkOp2 WrapSub a b
  subShrink (a `WrapMul` b) = shrinkOp2 WrapMul a b
  subShrink (a `WrapPow` b) = shrinkOp2 WrapPow a b
  subShrink (PopCnt n) = shrinkOp1 PopCnt n
  subShrink (Clz n) = shrinkOp1 Clz n
  subShrink (Ctz n) = shrinkOp1 Ctz n
  subShrink (Complement n) = shrinkOp1 Complement n
  subShrink (ConvertNatural a) = ConvertNatural <$> shrink a
  subShrink (ConvertNatNToNat a) = ConvertNatNToNat <$> shrink a
  subShrink (ConvertNatToNatN a) = ConvertNatToNatN <$> shrink a
  subShrink (ConvertIntNToInt a) = ConvertIntNToInt <$> shrink a
  subShrink (ConvertIntToIntN a) = ConvertIntToIntN <$> shrink a
  subShrink (IfThenElse a _ (Bool True)) = [a]
  subShrink (IfThenElse _ b (Bool False)) = [b]
  subShrink (IfThenElse a b c) = [a, b] <> shrinkRel3 IfThenElse a b c
  subShrink (a `NotEqual` b) = shrinkRel2 NotEqual a b
  subShrink (a `Equals` b) = shrinkRel2 Equals a b
  subShrink (a `GreaterEqual` b) = shrinkRel2 GreaterEqual a b
  subShrink (a `Greater` b) = shrinkRel2 Greater a b
  subShrink (a `LessEqual` b) = shrinkRel2 LessEqual a b
  subShrink (a `Less` b) = shrinkRel2 Less a b
  subShrink (a `ShortAnd` b) = shrinkRel2 ShortAnd a b
  subShrink (a `ShortOr` b) = shrinkRel2 ShortOr a b
  subShrink (Not a) = Not <$> shrink a
  subShrink (Bool False) = []
  subShrink (Bool True) = []
  subShrink (a `Pair` b) = shrinkRel2 Pair a b
  subShrink (Triple a b c) = shrinkRel3 Triple a b c
  subShrink Null = []
  subShrink (Some a) = Null : (Some <$> shrink a)
  subShrink (Text a) = Text <$> shrink a
  subShrink (a `Concat` b) = shrinkOp2 Concat a b
  
  deriving instance Show (MOTerm t)
  
  
  arithTerm :: Arbitrary (MOTerm t) =>
      Int -> [(Int, Gen (MOTerm t))]
  arithTerm n =
      [ (n, resize (n `div` 3) $ Add <$> arbitrary <*> arbitrary)
      , (n, resize (n `div` 3) $ Sub <$> arbitrary <*> arbitrary)
      , (n, resize (n `div` 3) $ Mul <$> arbitrary <*> arbitrary)
      , (n, resize (n `div` 3) $ Div <$> arbitrary <*> arbitrary)
      , (n, resize (n `div` 3) $ Mod <$> arbitrary <*> arbitrary)
      , (n, resize (n `div` 4) $ IfThenElse <$> arbitrary <*> arbitrary <*> arbitrary)
      , (n `div` 5 , resize (n `div` 3) $ Pow <$> arbitrary <*> ((`Mod` Five) <$> arbitrary))
      ]
  
  bitwiseTerm :: WordLike n => Arbitrary (MOTerm (BitLimited n i)) => Int -> [(Int, Gen (MOTerm (BitLimited n i)))]
  bitwiseTerm n =
      [ (n `div` 5, resize (n `div` 3) $ Or <$> arbitrary <*> arbitrary)
      , (n `div` 5, resize (n `div` 3) $ And <$> arbitrary <*> arbitrary)
      , (n `div` 5, resize (n `div` 3) $ Xor <$> arbitrary <*> arbitrary)
      , (n `div` 5, resize (n `div` 3) $ RotL <$> arbitrary <*> arbitrary)
      , (n `div` 5, resize (n `div` 3) $ RotR <$> arbitrary <*> arbitrary)
      , (n `div` 5, resize (n `div` 3) $ ShiftL <$> arbitrary <*> arbitrary)
      , (n `div` 5, resize (n `div` 3) $ ShiftR <$> arbitrary <*> arbitrary)
      , (n `div` 5, resize (n `div` 3) $ WrapAdd <$> arbitrary <*> arbitrary)
      , (n `div` 5, resize (n `div` 3) $ WrapSub <$> arbitrary <*> arbitrary)
      , (n `div` 5, resize (n `div` 3) $ WrapMul <$> arbitrary <*> arbitrary)
      , (n `div` 5, resize (n `div` 3) $ WrapPow <$> arbitrary <*> ((`Mod` Five) <$> arbitrary))
      , (n `div` 5, PopCnt <$> arbitrary)
      , (n `div` 5, Clz <$> arbitrary)
      , (n `div` 5, Ctz <$> arbitrary)
      , (n `div` 5, Complement <$> arbitrary)
      ]
  
  -- generate reasonably formed trees from smaller subterms
  --
  reasonablyShaped :: (Arbitrary (Neuralgic a), AnnotLit a, Evaluatable a)
                   => (Int -> [(Int, Gen (MOTerm a))])
                   -> Gen (MOTerm a)
  reasonablyShaped sub = sized $ \(succ -> n) -> frequency $
                         (30 `div` n, Neuralgic <$> arbitrary)
                         : if n > 1 then sub n else []
  
  instance WordLike n => Arbitrary (MOTerm (BitLimited n Natural)) where
    arbitrary = reasonablyShaped $ \n ->
      arithTerm n <>
      bitwiseTerm n
    shrink (Lit _) = []
    shrink x = [ Lit (fromIntegral x) | Just x <- pure $ evaluate x ] <> subShrink x
  
  instance WordLike n => Arbitrary (MOTerm (BitLimited n Integer)) where
    arbitrary = reasonablyShaped $ \n ->
      arithTerm n <>
      bitwiseTerm n
    shrink (Lit _) = []
    shrink x = [ Lit (fromIntegral x) | Just x <- pure $ evaluate x ] <> subShrink x
  
  instance (AnnotLit a, AnnotLit b, Evaluatable a, Evaluatable b, Arbitrary (MOTerm a), Arbitrary (MOTerm b)) => Arbitrary (MOTerm (a, b)) where
    arbitrary = scale (`quot` 2) $ Pair <$> arbitrary <*> arbitrary
    shrink (Pair x y) = shrinkRel2 Pair x y
  
  instance (AnnotLit a, AnnotLit b, AnnotLit c, Evaluatable a, Evaluatable b, Evaluatable c, Arbitrary (MOTerm a), Arbitrary (MOTerm b), Arbitrary (MOTerm c))
      => Arbitrary (MOTerm (a, b, c)) where
    arbitrary = scale (`quot` 3) $ Triple <$> arbitrary <*> arbitrary <*> arbitrary
    shrink (Triple x y z) = shrinkRel3 Triple x y z
  
  instance (AnnotLit a, Evaluatable a, Arbitrary (MOTerm a)) => Arbitrary (MOTerm (Maybe a)) where
    arbitrary = frequency [(1, pure Null), (10, Some <$> arbitrary)]
    shrink Null = []
    shrink (Some t) = Null : [ Some t' | t' <- shrink t ]
  
  instance Arbitrary (MOTerm Bool) where
    arbitrary = sized $ \(succ -> n) -> -- TODO: use frequency?
      oneof $ (Bool <$> arbitrary) : if n <= 1 then [] else
      [ resize (n `div` 3) $ elements [NotEqual @Integer, Equals, GreaterEqual, Greater, LessEqual, Less] <*> arbitrary <*> arbitrary
      , resize (n `div` 5) $ elements [ShortAnd, ShortOr] <*> arbitrary <*> arbitrary
      , resize (n `div` 2) $ Not <$> arbitrary
      ]
    shrink (Bool _) = []
    shrink x = [ Bool x | Just x <- pure $ evaluate x ] <> subShrink x
  
  instance Arbitrary (MOTerm Natural) where
    arbitrary = reasonablyShaped $ \n ->
      arithTerm n <>
      [ (n `div` 2, ConvertNatNToNat <$> (arbitrary @(MOTerm Nat8)))
      , (n `div` 2, ConvertNatNToNat <$> (arbitrary @(MOTerm Nat16)))
      , (n `div` 2, ConvertNatNToNat <$> (arbitrary @(MOTerm Nat32)))
      , (n `div` 2, ConvertNatNToNat <$> (arbitrary @(MOTerm Nat64)))
      ]
    shrink (Lit _) = []
    shrink x = [ Lit (fromIntegral x) | Just x <- pure $ evaluate x ] <> subShrink x
  
  instance Arbitrary (MOTerm Integer) where
    arbitrary = reasonablyShaped $ \n ->
      arithTerm n <>
      [ (n, resize (n `div` 2) $ Pos <$> arbitrary)
      , (n, resize (n `div` 2) $ Neg <$> arbitrary)
      , (n, resize (n `div` 2) $ Abs <$> arbitrary)
      , (5*n, ConvertNatural <$> arbitrary)
      , (n `div` 3, ConvertIntNToInt <$> (arbitrary @(MOTerm Int8)))
      , (n `div` 3, ConvertIntNToInt <$> (arbitrary @(MOTerm Int16)))
      , (n `div` 3, ConvertIntNToInt <$> (arbitrary @(MOTerm Int32)))
      , (n `div` 3, ConvertIntNToInt <$> (arbitrary @(MOTerm Int64)))
      ]
    shrink (Lit _) = []
    shrink x = [ Lit (fromIntegral x) | Just x <- pure $ evaluate x ] <> subShrink x
  
  instance Num a => Num (Maybe a) where
    (+) = liftA2 (+)
    (-) = liftA2 (-)
    (*) = liftA2 (*)
    abs = liftA abs
    signum = liftA signum
    fromInteger = pure . fromInteger
  
  instance Real a => Real (Maybe a) where
    toRational = undefined
  
  instance Enum a => Enum (Maybe a)
  
  instance (Enum (Maybe a), Eq a, Integral a) => Integral (Maybe a) where
    _ `quotRem` Just 0 = (Nothing, Nothing)
    a `quotRem` b = case liftA2 quotRem a b of
                      Just (pure -> x, pure -> y) -> (x, y)
                      _ -> (Nothing, Nothing)
  
  
  evalO :: Num a => Off -> a -> a
  evalO TwoLess = \n -> n - 2
  evalO OneLess = \n -> n - 1
  evalO OneMore = (+1)
  evalO TwoMore = (+2)
  
  evalN :: Num a => Neuralgic t -> a
  evalN LargeNeg = fromIntegral (minBound :: Int) - 111
  evalN (AroundNeg n) = - 2 ^ n
  evalN Around0 = 0
  evalN (AroundPos n) = 2 ^ n - 1
  evalN LargePos = fromIntegral (maxBound :: Int) + 333
  evalN (Offset (evalN -> n) (evalO -> o)) = o n
  
  
  guardedEvalN :: Integral a => (Integer -> Maybe a) -> Neuralgic a -> Maybe a
  guardedEvalN g (Offset (guardedEvalN g -> n) (evalO -> o)) = g =<< (o . toInteger) <$> n
  guardedEvalN g (g . evalN -> res) = res
  
  noExponentRestriction, nonNegativeExponentRestriction, defaultExponentRestriction :: (Ord a, Num a) => a -> Maybe ()
  noExponentRestriction _ = pure ()
  nonNegativeExponentRestriction = guard . (>= 0)
  defaultExponentRestriction = guard . ((&&) <$> (>= 0) <*> (< 5))
  
  class Restricted a where
    substractable :: Maybe a -> Maybe a -> Bool
    exponentiable :: (Num a, Ord a) => a -> Maybe ()
    exponentiable = defaultExponentRestriction
  
  instance Restricted Integer where substractable _ _ = True
  instance Restricted Natural where substractable a b = isJust $ do m <- a; n <- b; guard $ m >= n
  instance KnownNat n => Restricted (BitLimited n Natural) where
    substractable a b = isJust $ do NatN m <- a; NatN n <- b; guard $ m >= n
    exponentiable = if natVal (Proxy @n) <= 8
                    then noExponentRestriction
                    else defaultExponentRestriction
  instance KnownNat n => Restricted (BitLimited n Integer) where
    exponentiable = if natVal (Proxy @n) <= 8
                    then nonNegativeExponentRestriction
                    else defaultExponentRestriction
  
  class Ord a => Evaluatable a where
    evaluate :: MOTerm a -> Maybe a
  
  
  data BitLimited (n :: Nat) (a :: *) where
    NatN :: KnownNat n => Natural -> BitLimited n Natural
    IntN :: KnownNat n => Integer -> BitLimited n Integer
  
  deriving instance Show (BitLimited n a)
  deriving instance Eq (BitLimited n a)
  deriving instance Ord (BitLimited n a)
  
  
  -- for a BitLimited n Word, the instances of WordView provide the
  -- change of perspective to the built-in Word types' semantics
  --
  class WordView a where
    type WordType a :: *
    toWord :: a -> WordType a
    fromWord :: WordType a -> a
    lift1 :: (WordType a -> WordType a) -> a -> a
    lift1 f (fromWord . f . toWord -> res) = res
    lift1b :: (WordType a -> b) -> a -> b
    lift1b f (f . toWord -> res) = res
    lift2 :: (WordType a -> WordType a -> WordType a) -> a -> a -> a
    lift2 f (toWord -> a) (toWord -> b) = fromWord (a `f` b)
    {-# MINIMAL toWord, fromWord #-}
  
  
  type family WordTypeForBits a where
    WordTypeForBits 8 = Data.Word.Word8
    WordTypeForBits 16 = Data.Word.Word16
    WordTypeForBits 32 = Data.Word.Word32
    WordTypeForBits 64 = Data.Word.Word64
  
  instance (Integral (WordTypeForBits n), FiniteBits (WordTypeForBits n), KnownNat n) => WordView (BitLimited n Natural) where
    type WordType (BitLimited n Natural) = WordTypeForBits n
    toWord (NatN n) = fromIntegral n
    fromWord = NatN . fromIntegral
  
  type family IntTypeForBits a where
    IntTypeForBits 8 = Data.Int.Int8
    IntTypeForBits 16 = Data.Int.Int16
    IntTypeForBits 32 = Data.Int.Int32
    IntTypeForBits 64 = Data.Int.Int64
  
  instance (Integral (IntTypeForBits n), FiniteBits (IntTypeForBits n), KnownNat n) => WordView (BitLimited n Integer) where
    type WordType (BitLimited n Integer) = IntTypeForBits n
    toWord (IntN n) = fromIntegral n
    fromWord = IntN . fromIntegral
  
  type WordLike n = ( Integral (WordTypeForBits n)
                    , FiniteBits (WordTypeForBits n)
                    , Integral (IntTypeForBits n)
                    , FiniteBits (IntTypeForBits n)
                    , KnownNat n
                    , WordView (BitLimited n Natural)
                    , WordView (BitLimited n Integer)
                    )
  
  type Nat8 = BitLimited 8 Natural
  type Nat16 = BitLimited 16 Natural
  type Nat32 = BitLimited 32 Natural
  type Nat64 = BitLimited 64 Natural
  type Int8 = BitLimited 8 Integer
  type Int16 = BitLimited 16 Integer
  type Int32 = BitLimited 32 Integer
  type Int64 = BitLimited 64 Integer
  
  instance ToBitLimited bits a => Num (BitLimited bits a) where
    NatN m + NatN n = NatN . fromJust $ trapNat (natVal (Proxy @bits)) (toInteger m + toInteger n)
    IntN m + IntN n = IntN . fromJust $ trapInt (natVal (Proxy @bits)) (m + n)
    NatN m - NatN n = NatN . fromJust $ trapNat (natVal (Proxy @bits)) (toInteger m - toInteger n)
    IntN m - IntN n = IntN . fromJust $ trapInt (natVal (Proxy @bits)) (m - n)
    NatN m * NatN n = NatN . fromJust $ trapNat (natVal (Proxy @bits)) (toInteger m * toInteger n)
    IntN m * IntN n = IntN . fromJust $ trapInt (natVal (Proxy @bits)) (m * n)
  
    abs (NatN m) = NatN (abs m)
    abs (IntN m) = IntN . fromJust $ trapInt (natVal (Proxy @bits)) (abs m)
  
    signum (NatN m) = NatN (signum m)
    signum (IntN m) = IntN (signum m)
  
    fromInteger = toBitLimited . fromInteger
  
  -- Helper class ToBitLimited, to build correct BitLimited variant
  class KnownNat bits => ToBitLimited bits a where toBitLimited :: Integer -> BitLimited bits a
  
  instance KnownNat bits => ToBitLimited bits Natural where
    toBitLimited = NatN @bits . fromJust . trapNat (natVal (Proxy @bits)) . fromIntegral
  instance KnownNat bits => ToBitLimited bits Integer where
    toBitLimited = IntN @bits . fromJust . trapInt (natVal (Proxy @bits))
  
  instance ToBitLimited n a => Real (BitLimited n a)
  instance Enum (BitLimited n a)
  instance ToBitLimited n a => Integral (BitLimited n a) where
    toInteger (NatN n) = toInteger n
    toInteger (IntN n) = n
  
  trapNat :: Integer -> Integer -> Maybe Natural
  trapNat n v = do guard (v >= 0 && v < 2 ^ n); pure (fromIntegral v)
  
  trapInt :: Integer -> Integer -> Maybe Integer
  trapInt n v = do guard (v < 2 ^ (n-1) && v >= - 2 ^ (n-1)); pure v
  
  instance WordLike bits => Evaluatable (BitLimited bits Natural) where
    evaluate Five = pure $ NatN 5
    evaluate (Lit n) = NatN <$> trapNat (natVal (Proxy @bits)) n
    evaluate (Neuralgic n) = NatN <$> trapNat (natVal (Proxy @bits)) (evalN n)
    evaluate ab =
        case ab of
          a `Add` b -> go (+) a b
          a `Sub` b -> go (-) a b
          a `Mul` b -> go (*) a b
          _ `Div` (evaluate -> Just 0) -> Nothing
          a `Div` b -> go quot a b
          _ `Mod` (evaluate -> Just 0) -> Nothing
          a `Mod` b -> go rem a b
          a `Pow` b -> do b' <- evaluate b; exponentiable b'; go (^) a b
            -- NB: The use of exponentiable means that evaluate t = Nothing
            -- can mean "traps" or "too big, should not evaluate"
            -- This is kinda ok, because the generators only produce small
            -- exponents, but could be revisited for better test coverage.
          IfThenElse a b c -> do c <- evaluate c
                                 evaluate $ if c then a else b
  
          a `Or` b -> goWrap (.|.) a b
          a `And` b -> goWrap (.&.) a b
          a `Xor` b -> goWrap xor a b
          a `RotL` b -> goWrapMod rotateL a b
          a `RotR` b -> goWrapMod rotateR a b
          a `ShiftL` b -> goWrapMod shiftL a b
          a `ShiftR` b -> goWrapMod shiftR a b
  
          Complement a -> fromWord . complement . toWord <$> evaluate a
          PopCnt a -> NatN . fromIntegral . popCount . toWord <$> evaluate a
          Clz a -> NatN . fromIntegral . countLeadingZeros . toWord <$> evaluate a
          Ctz a -> NatN . fromIntegral . countTrailingZeros . toWord <$> evaluate a
  
          a `WrapAdd` b -> goWrap (+) a b
          a `WrapSub` b -> goWrap (-) a b
          a `WrapMul` b -> goWrap (*) a b
          a `WrapPow` b -> goWrap (^) a b
  
          _ -> error $ show ab
      where
          bitcount = natVal (Proxy @bits)
          go op a b = do NatN a <- evaluate a; NatN b <- evaluate b; NatN <$> trapNat (natVal (Proxy @bits)) (toInteger a `op` toInteger b)
          goWrap op a b = do
              a <- toWord <$> evaluate a
              b <- toWord <$> evaluate b
              pure $ fromWord $ a `op` b
          goWrapMod op a b = do
              a <- toWord <$> evaluate a
              b <- fromIntegral . (`mod` bitcount) . fromIntegral <$> evaluate b
              pure $ fromWord $ a `op` b
  
  instance WordLike bits => Evaluatable (BitLimited bits Integer) where
    evaluate Five = pure $ IntN 5
    evaluate (Lit n) = IntN <$> trapInt (natVal (Proxy @bits)) n
    evaluate (Neuralgic n) = IntN <$> trapInt (natVal (Proxy @bits)) (evalN n)
    evaluate ab =
        case ab of
          a `Add` b -> go (+) a b
          a `Sub` b -> go (-) a b
          a `Mul` b -> go (*) a b
          _ `Div` (evaluate -> Just 0) -> Nothing
          a `Div` b -> go quot a b
          _ `Mod` (evaluate -> Just 0) -> Nothing
          a `Mod` b -> go rem a b
          a `Pow` b -> do b' <- evaluate b; exponentiable b'; go (^) a b
          IfThenElse a b c -> do c <- evaluate c
                                 evaluate $ if c then a else b
  
          a `Or` b -> goWrap (.|.) a b
          a `And` b -> goWrap (.&.) a b
          a `Xor` b -> goWrap xor a b
          a `RotL` b -> goWrapMod rotateL a b
          a `RotR` b -> goWrapMod rotateR a b
          a `ShiftL` b -> goWrapMod shiftL a b
          a `ShiftR` b -> goWrapMod shiftR a b
  
          Complement a -> fromWord . complement . toWord <$> evaluate a
          PopCnt a -> IntN . fromIntegral . popCount . toWord <$> evaluate a
          Clz a -> IntN . fromIntegral . countLeadingZeros . toWord <$> evaluate a
          Ctz a -> IntN . fromIntegral . countTrailingZeros . toWord <$> evaluate a
  
          a `WrapAdd` b -> goWrap (+) a b
          a `WrapSub` b -> goWrap (-) a b
          a `WrapMul` b -> goWrap (*) a b
          a `WrapPow` b -> do b' <- evaluate b; exponentiable b'; goWrap (^) a b
  
          _ -> error $ show ab
      where
          bitcount = natVal (Proxy @bits)
          go op a b = do IntN a <- evaluate a; IntN b <- evaluate b; IntN <$> trapInt (natVal (Proxy @bits)) (toInteger a `op` toInteger b)
          goWrap op a b = do
              a <- toWord <$> evaluate a
              b <- toWord <$> evaluate b
              pure $ fromWord $ a `op` b
          goWrapMod op a b = do
              a <- toWord <$> evaluate a
              b <- fromIntegral . (`mod` bitcount) . fromIntegral <$> evaluate b
              pure $ fromWord $ a `op` b
  
  instance Evaluatable Integer where
    evaluate = eval
  instance Evaluatable Natural where
    evaluate = eval
  
  instance (Evaluatable a, Evaluatable b) => Evaluatable (a, b) where
    evaluate (Pair a b) = (,) <$> evaluate a <*> evaluate b
  
  instance (Evaluatable a, Evaluatable b, Evaluatable c) => Evaluatable (a, b, c) where
    evaluate (Triple a b c) = (,,) <$> evaluate a <*> evaluate b <*> evaluate c
  
  instance Evaluatable a => Evaluatable (Maybe a) where
    evaluate Null = pure Nothing
    evaluate (Some a) = Just <$> evaluate a
  
  maskFor :: forall n a . (WordLike n, Num a) => MOTerm (BitLimited n a) -> a
  maskFor _ = fromIntegral $ 2 ^ natVal (Proxy @n) - 1
  
  
  eval :: (Restricted a, Integral a) => MOTerm a -> Maybe a
  eval Five = pure 5
  eval (Neuralgic n) = evalN n
  eval (Lit n) = pure (fromIntegral n)
  eval (Pos n) = eval n
  eval (Neg n) = - eval n
  eval (Abs n) = abs $ eval n
  eval (a `Add` b) = eval a + eval b
  eval ((eval -> a) `Sub` (eval -> b)) = do guard $ substractable a b; a - b
  eval (a `Mul` b) = eval a * eval b
  eval (a `Div` b) = eval a `quot` eval b
  eval (a `Mod` b) = eval a `rem` eval b
  eval (a `Pow` (eval -> b)) = do b' <- b; exponentiable b'; (^) <$> eval a <*> b
  eval (ConvertNatural t) = fromIntegral <$> evaluate t
  eval c@(ConvertNatToNatN t) = fromIntegral . (.&. maskFor c) <$> evaluate t
  eval (ConvertNatNToNat t) = fromIntegral <$> evaluate t
  eval c@(ConvertIntToIntN t) = fromIntegral . (.&. maskFor c) <$> evaluate t
  eval (ConvertIntNToInt t) = fromIntegral <$> evaluate t
  eval (IfThenElse a b c) = do c <- evaluate c
                               eval $ if c then a else b
  --eval _ = Nothing
  
  
  instance Evaluatable Bool where
    evaluate (a `NotEqual` b) = (/=) <$> evaluate a <*> evaluate b
    evaluate (a `Equals` b) = (==) <$> evaluate a <*> evaluate b
    evaluate (a `GreaterEqual` b) = (>=) <$> evaluate a <*> evaluate b
    evaluate (a `Greater` b) = (>) <$> evaluate a <*> evaluate b
    evaluate (a `LessEqual` b) = (<=) <$> evaluate a <*> evaluate b
    evaluate (a `Less` b) = (<) <$> evaluate a <*> evaluate b
    evaluate (a `ShortAnd` b) = evaluate a >>= bool (pure False) (evaluate b)
    evaluate (a `ShortOr` b) = evaluate a >>= bool (evaluate b) (pure True)
    evaluate (Not a) = not <$> evaluate a
    evaluate (Bool b) = pure b
  
  instance Evaluatable String where
    evaluate (Text a) = pure a
    evaluate (a `Concat` b) = (<>) <$> evaluate a <*> evaluate b
  
  type AnnotLit t = (Annot t, Literal t)
  
  class Annot t where
    annot :: MOTerm t -> String -> String
    sizeSuffix :: MOTerm t -> String -> String
    sizeSuffix _ = id
    typSuffix :: MOTerm t -> String -> String
    typSuffix _ = id
  
  instance Annot (a, b) where
    annot _ = id
  
  instance Annot (a, b, c) where
    annot _ = id
  
  instance Annot (Maybe a) where
    annot _ = id
  
  instance Annot Integer where
    annot _ s = "((" <> s <> ") : Int)"
  
  instance Annot Natural where
    annot _ s = "((" <> s <> ") : Nat)"
  
  instance Annot String where
    annot _ = id
  
  bitWidth :: KnownNat n => Proxy n -> String
  bitWidth p = show (natVal p)
  
  instance KnownNat n => Annot (BitLimited n Natural) where
    annot _ s = "((" <> s <> ") : Nat" <> bitWidth (Proxy @n) <> ")"
    sizeSuffix _ = (<> bitWidth (Proxy @n))
    typSuffix _ = (<> "Nat" <> bitWidth (Proxy @n))
  
  instance KnownNat n => Annot (BitLimited n Integer) where
    annot _ s = "((" <> s <> ") : Int" <> bitWidth (Proxy @n) <> ")"
    sizeSuffix _ = (<> bitWidth (Proxy @n))
    typSuffix _ = (<> "Int" <> bitWidth (Proxy @n))
  
  instance Annot Bool where
    annot _ = id
  
  class Literal a where
    literal :: Neuralgic a -> String
    literal (evalN -> n) = if n < 0 then "(" <> show n <> ")" else show n
  
  instance Literal (a, b) where
    literal _ = error "Literal (a, b) makes no sense"
  
  instance Literal (a, b, c) where
    literal _ = error "Literal (a, b, c) makes no sense"
  
  instance Literal (Maybe a) where
    literal _ = error "Literal (Maybe a) makes no sense"
  
  instance Literal String where
    literal _ = error "Literal String makes no sense"
  
  instance Literal Integer
  instance Literal Natural
  instance Literal (BitLimited n Natural)
  instance KnownNat bits => Literal (BitLimited bits Integer) where
    literal (evalN -> n) = if n < 0
                           then "(" <> show n <> ")"
                           else show n
  
  instance Literal Bool where
    literal _ = error "Literal Bool makes no sense"
  
  inParens :: (a -> String) -> String -> a -> a -> String
  inParens to op lhs rhs = "(" <> to lhs <> " " <> op <> " " <> to rhs <> ")"
  
  unparseMO :: AnnotLit a => MOTerm a -> String
  unparseMO f@Five = annot f "5"
  unparseMO a@(Lit n) = annot a $ show n
  unparseMO a@(Neuralgic n) = annot a $ literal n
  unparseMO (Pos n) = "(+" <> unparseMO n <> ")"
  unparseMO (Neg n) = "(-" <> unparseMO n <> ")"
  unparseMO (Abs n) = "(Prim.abs " <> unparseMO n <> ")"
  unparseMO (a `Add` b) = inParens unparseMO "+" a b
  unparseMO (a `Sub` b) = annot a $ inParens unparseMO "-" a b
  unparseMO (a `Mul` b) = inParens unparseMO "*" a b
  unparseMO (a `Div` b) = inParens unparseMO "/" a b
  unparseMO (a `Mod` b) = inParens unparseMO "%" a b
  unparseMO (a `Pow` b) = inParens unparseMO "**" a b
  unparseMO (a `Or` b) = inParens unparseMO "|" a b
  unparseMO (a `And` b) = inParens unparseMO "&" a b
  unparseMO (a `Xor` b) = inParens unparseMO "^" a b
  unparseMO (a `RotL` b) = inParens unparseMO "<<>" a b
  unparseMO (a `RotR` b) = inParens unparseMO "<>>" a b
  unparseMO (a `ShiftL` b) = inParens unparseMO "<<" a b
  unparseMO (a `ShiftR` b) = inParens unparseMO ">>" a b
  unparseMO (a `WrapAdd` b) = inParens unparseMO "+%" a b
  unparseMO (a `WrapSub` b) = inParens unparseMO "-%" a b
  unparseMO (a `WrapMul` b) = inParens unparseMO "*%" a b
  unparseMO (a `WrapPow` b) = inParens unparseMO "**%" a b
  unparseMO t@(PopCnt n) = typSuffix t "(Prim.popcnt" <> " " <> unparseMO n <> ")"
  unparseMO t@(Clz n) = typSuffix t "(Prim.clz" <> " " <> unparseMO n <> ")"
  unparseMO t@(Ctz n) = typSuffix t "(Prim.ctz" <> " " <> unparseMO n <> ")"
  unparseMO (Complement a) = "(^ " <> unparseMO a <> ")"
  unparseMO (ConvertNatural a) = "(++++(" <> unparseMO a <> "))"
  unparseMO (ConvertNatNToNat a) = sizeSuffix a "(Prim.nat" <> "ToNat " <> unparseMO a <> ")"
  unparseMO t@(ConvertNatToNatN a) = sizeSuffix t "(Prim.intToNat" <> "Wrap " <> unparseMO a <> ")"
  unparseMO (ConvertIntNToInt a) = sizeSuffix a "(Prim.int" <> "ToInt " <> unparseMO a <> ")"
  unparseMO t@(ConvertIntToIntN a) = sizeSuffix t "(Prim.intToInt" <> "Wrap " <> unparseMO a <> ")"
  unparseMO (IfThenElse a b c) = "(if (" <> unparseMO c <> ") " <> unparseMO a <> " else " <> unparseMO b <> ")"
  unparseMO (a `NotEqual` b) = inParens unparseMO "!=" a b
  unparseMO (a `Equals` b) = inParens unparseMO "==" a b
  unparseMO (a `GreaterEqual` b) = inParens unparseMO ">=" a b
  unparseMO (a `Greater` b) = inParens unparseMO ">" a b
  unparseMO (a `LessEqual` b) = inParens unparseMO "<=" a b
  unparseMO (a `Less` b) = inParens unparseMO "<" a b
  unparseMO (a `ShortAnd` b) = inParens unparseMO "and" a b
  unparseMO (a `ShortOr` b) = inParens unparseMO "or" a b
  unparseMO (Not a) = "(not " <> unparseMO a <> ")"
  unparseMO (Bool False) = "false"
  unparseMO (Bool True) = "true"
  unparseMO (a `Pair` b) = "(" <> unparseMO a <> ", " <> unparseMO b <> ")"
  unparseMO (Triple a b c) = "(" <> unparseMO a <> ", " <> unparseMO b <> ", " <> unparseMO c <> ")"
  unparseMO Null = "null"
  unparseMO (Some a) = '?' : unparseMO a
  unparseMO (Text a) = '"' : concatMap escape a <> "\""
  unparseMO (a `Concat` b) = "(" <> unparseMO a <> " # " <> unparseMO b <> ")"
  unparseMO (Array _ ) = error "not yet implemented"
  
  
  -- TODOs:
  --   - wordToInt
  --   - natToNat64/intToWord64 (and round-trips)
  --       Done: natToWordN/wordNToNat
  --   - bitwise ops (btst?)
  --   - pattern matches (over numeric, bool, structured)
  --   - trapping flavour-preserving conversions Nat -> NatN
  --   - bitsize-preserving conversions
  --   - data MOTerm (p :: {Term, Pattern}) where ... Pattern :: MOValue a => a -> MOTerm (Pattern/both) a
  --   - Text and Concat tests (partly covered by rope tests)
  