module Main

import SSG.Djot.Lines

import Control.Eff
import Data.String
import Hedgehog

lines' : Eff [Lines] (List String)
lines' = do
  Just next <- take
    | _ => pure []
  map (next ::) lines'

propLinesEquiv : Property
propLinesEquiv = property $ do
  str <- forAll $ string (linear 0 256) ascii
  let std_lines = lines str
  let (our_lines, rest) = extract $ runLines str lines'
  our_lines === std_lines

main : IO ()
main = test $
  [ MkGroup
      "Lines effect"
      [ ("Lines effect equivalent to lines", propLinesEquiv)
      ]
  ]