content: module E.Arbitrary where
  
  --import Test.QuickCheck
  import Data.Monoid
  import Doc.DocLike()
  import Doc.PPrint
  import Doc.Pretty (putDoc, Doc)
  import E.E
  import E.Show
  import E.TypeCheck()
  import GenUtil()
  import Name.Id
  import Name.VConsts
  import System.Random
  import Support.CanType
  import Support.FreeVars()
  -- import qualified Data.Map as Map
  import qualified Data.Set as Set
  
  data EP = EP {
      canDiverge :: Bool,
      usedVars :: Set.Set TVr
      }
  
  choose :: [IO a] -> IO a
  choose [] = fail "nothing to choose from"
  choose as = do
      x <- randomRIO (0,length as - 1)
      as !! x
  
  value t
      | t == tInteger = choose [return $ ELit $ LitInt 1 tInteger]
      | t == tChar = choose [return $ ELit $ LitInt (fromIntegral (fromEnum 'x')) tChar]
      | t == eStar = choose $ map return [tChar, tInteger]
      | otherwise = fail "not support value"
  
  var t = do
      x <- randomRIO (1,100)
      return $ TVr (anonymous x) t mempty
  
  complicate :: Set.Set TVr -> E -> IO E
  complicate fvs e = do
      let re = if Set.null fvs then (replicate 1 (return e) ++ ) else id
      e <- choose  $ re  (replicate 2 $ complicate' fvs e >>= complicate fvs )
      return e
  
  complicate' fvs e
      | EPi (TVr _ a1 _) a2 <- te = choose [ do v <- value a1; return (EAp e v), f e  ]
      | otherwise = f e
      where
      te = getType e
      f (EAp a b) = choose [do
          a' <- complicate fvs a
          b' <- complicate fvs b
          return (EAp a b), g e]
      f (ELam v e) = choose [do
              e' <- complicate fvs e
              return (ELam v e'),
              g e]
      f e = g e
      g e = do
          t <- value eStar
          v <- var t
          return (ELam v e)
  
  genE = do
      v <- value tInteger
      complicate mempty v
  
  ge = do
      e <- genE
      print e
      putStrLn (render $ (ePretty e :: Doc))
      putDoc (pprint (getType e))
  
  testE = do
      putStrLn "Testing E"
      ge
      ge
  
  {-
  
  typeSet env = Map.keys env
  typeCnt env a
      | Just x <- Map.lookup a env = x
      | otherwise = 0
  typeCntInc env a = Map.insert a (typeCnt env a + 1) env
  
  countTerm :: E -> Map.Map E Int -> Int -> Int
  countTerm _t _env 0 = 0
  countTerm t env 1 = typeCnt env t
  countTerm t@(EPi (TVr _ a1 _) a2) env s = countTerm a2 (typeCntInc env a1) (s - 1) + countHeadVarTerm t env s
  countTerm t env s = countHeadVarTerm t env s
  
  countHeadVarTerm t env s = sum [ countHeadVarArgTerms bs env s | bs <- validHeadVarTypeSet t env]
  
  countHeadVarArgTerms (b,bs) env s
      | numVarWithTypeInEnv <= 0 = 0    -- multiplication is too strict here
      | otherwise = numVarWithTypeInEnv * numTerms where
          numVarWithTypeInEnv = typeCnt env b
          m = length bs
          numTerms = sum [ product [ countTerm b env s | s <- ss | b <- bs ] | ss <- ndk (s - 1 - m) m]
  
  validHeadVarTypeSet  a env = concat (map (f []) (Map.keys env)) where
      f rs b | b == a = return (a,reverse rs)
      f rs (EPi (TVr _ b1 _) b2) = f (b1:rs) b2
      f _ _ = fail "not valid head var type set"
  
  ndk :: Int -> Int -> [[Int]]
  ndk n m | n < 0 = error "ndk: n < 0"
  ndk n m | m < 0 = error "ndk: m < 0"
  ndk n m | n < m = error "ndk: n < m"
  ndk 0 m = []
  ndk n m | n == m = [replicate m 1]
  ndk n m = snub $ concat [ f ss | ss <- ndk (n - 1) m] where
      f ss = [ [ if i == i' then s + 1 else s | s <- ss | i' <- [0 :: Int ..] ] | _ <- ss | i <- [0 :: Int ..] ]
  
  testE = do
      putStrLn "Testing E"
      let f x i = do
          putStrLn $ "countTerm" <+> show x <+> show i <+> "=" <+> show (countTerm x (Map.singleton eStar 1) i)
      f eStar 2
      f eStar 4
      f eStar 1
      f (ePi (TVr 0 eStar mempty) eStar) 7
      let prop_ndk n m = abs n >= abs m ==> let ss = ndk (abs n) (abs m) in and [ sum s == (abs n) |s <- ss] && unique mempty ss where
          unique _ [] = True
          unique ss (x:xs) | x `Set.member` ss = False
          unique ss (x:xs) = unique (Set.insert x ss) xs
      --quickCheck prop_ndk
  
      print (ndk 4 2)
      --print (ndk 10 4)
  
  gen a s = genTerm a mempty s
  
  genTerm _a _env s | s < 1 = return Nothing
  genTerm a env 1
      | typeCnt env a > 0 = genVarTerm env a
      | otherwise = return Nothing
  genTerm (EPi (TVr _ a1) a2) env s = do
      let totalNumTerm = countTerm a env s
          numLamTerm = countTerm a2 (typeCntInc env a1 (s - 1))
      x <- randomRIO (0,totalNumTerm)
      if x <= numLamTerm then
          genLamTerm a1 a2 env s
        else genAppTerm a env s (totalNumTerm  - numLamTerm)
  genTerm a env s = genAppTerm a env s (countTerm a env s)
  
  genVarTerm a env | typeCnt env a == 0 = return Nothing
  
  -}
  