content: {-# LANGUAGE OverloadedStrings #-}
  
  module UndoANFTests(tests) where
  
  import Language.Fixpoint.Types (SortedReft(..), Symbol,
                                  isPrefixOfSym, anfPrefix, syms)
  import Language.Fixpoint.Solver.EnvironmentReduction (undoANFSimplifyingWith)
  import Arbitrary
  import qualified Data.HashMap.Strict as M
  import Test.Tasty (TestTree, testGroup, adjustOption)
  import Test.Tasty.HUnit ((@?=))
  import qualified Test.Tasty.HUnit as H
  import Test.Tasty.QuickCheck ((===))
  import qualified Test.Tasty.QuickCheck as Q
  
  
  tests :: TestTree
  tests =
    withOptions $
      testGroup
        "undoANFSimplifyingWith id id"
        [ H.testCase "id on empty env" $
            simpleUndoANF [] @?= M.empty
        , Q.testProperty "id when env contains no lq_anf$* bindings" $
            prop_no_change (M.fromList . unEnv . unNoAnfEnv) simpleUndoANFNoAnfEnv
        , testGroup
            "zero anf vars left afterwards, starting with:"
            [ Q.testProperty "no anf vars" $
                prop_no_anfs simpleUndoANFNoAnfEnv
            , Q.testProperty "single-level anf vars" $
                prop_no_anfs simpleUndoANFFlatAnfEnv
            , Q.testProperty "chained anf vars" $
                prop_no_anfs simpleUndoANFChainedAnfEnv
            ]
        ]
    where
      withOptions = adjustOption (min (Q.QuickCheckMaxSize 8))   -- adjustOption . min because we don't want to default to the enormous value.
                    . adjustOption (max (Q.QuickCheckTests 500)) -- adjustOption . max because we may want larger on the command line.
  
  -- | 5 seconds (in microseconds).
  timeout :: Int
  timeout = 5000000
  
  prop_no_change :: (Q.Arbitrary e, Eq e, Show e) => (e -> M.HashMap Symbol SortedReft) -> (e -> M.HashMap Symbol SortedReft) -> e -> Q.Property
  prop_no_change toHashMap f e = Q.within timeout $ f e === toHashMap e
  
  prop_no_anfs :: (Q.Arbitrary e, Eq e, Show e) => (e -> M.HashMap Symbol SortedReft) -> e -> Q.Property
  prop_no_anfs f e = Q.within timeout . checkNoAnfs . f $ e
    where
      checkNoAnfs m = M.filter (any isAnfVar . syms) m === M.empty
      isAnfVar = isPrefixOfSym anfPrefix
  
  -- | We perform tests with only trivial lenses (i.e. id)
  simpleUndoANF :: [(Symbol, SortedReft)] -> M.HashMap Symbol SortedReft
  simpleUndoANF = undoANFSimplifyingWith id id . M.fromList
  
  ----------------------------------------------------
  -- | simpleUndoANF conjugated with various newtypes
  ----------------------------------------------------
  
  simpleUndoANFEnv :: Env -> M.HashMap Symbol SortedReft
  simpleUndoANFEnv = simpleUndoANF . unEnv
  
  simpleUndoANFNoAnfEnv :: NoAnfEnv -> M.HashMap Symbol SortedReft
  simpleUndoANFNoAnfEnv = simpleUndoANFEnv . unNoAnfEnv
  
  simpleUndoANFFlatAnfEnv :: FlatAnfEnv -> M.HashMap Symbol SortedReft
  simpleUndoANFFlatAnfEnv = simpleUndoANFEnv . unFlatAnfEnv
  
  simpleUndoANFChainedAnfEnv :: ChainedAnfEnv -> M.HashMap Symbol SortedReft
  simpleUndoANFChainedAnfEnv = simpleUndoANFEnv . unChainedAnfEnv
  