content: {-# LANGUAGE ViewPatterns #-}
  -- This file is part of the Haskell debugger Hoed.
  --
  -- Copyright (c) Maarten Faddegon 2015-2016
  
  {-# LANGUAGE OverloadedLists, DefaultSignatures, TypeOperators, FlexibleContexts, FlexibleInstances, StandaloneDeriving, CPP, DeriveGeneric #-}
  
  module Debug.Hoed.Prop where
  -- ( judge
  -- , Propositions(..)
  -- ) where
  import qualified Data.Vector.Generic as VG
  import Debug.Hoed.Observe(EventWithId(..), Observable(..),Trace(..),UID,Event(..),Change(..),ourCatchAllIO,evaluate,eventParent,parentPosition)
  import Debug.Hoed.Render(CompStmt(..),noNewlines)
  import Debug.Hoed.CompTree(CompTree,Vertex(..),Graph(..),vertexUID,vertexRes,replaceVertex,getJudgement,setJudgement)
  import Debug.Hoed.EventForest(EventForest,mkEventForest,dfsChildren)
  import Debug.Hoed.Serialize
  import qualified Data.IntMap as M
  import qualified Data.Text as T
  import Prelude hiding (Right)
  import Data.Graph.Libgraph(Judgement(..),AssistedMessage(..),mapGraph)
  import System.Directory(createDirectoryIfMissing)
  import System.Process(system)
  import System.Exit(ExitCode(..))
  import System.IO(hPutStrLn,stderr)
  import System.IO.Unsafe(unsafePerformIO)
  import Data.Char(isAlpha)
  import Data.Maybe(isNothing,fromJust,isJust)
  import Data.List(intersperse,isInfixOf,foldl1)
  import GHC.Generics hiding (moduleName) --(Generic(..),Rep(..),from,(:+:)(..),(:*:)(..),U1(..),K1(..),M1(..))
  import Control.Monad(foldM)
  
  ------------------------------------------------------------------------------------------------------------------------
  
  data Propositions = Propositions { propositions :: [Proposition]
                                   , propType :: PropType
                                   , funName :: String
                                   , extraModules :: [Module]
                                   }
  
  data PropType = Specify | PropertiesOf deriving Eq
  
  data Signature 
    = Argument Int
    | SubjectFunction
    | Random
    deriving (Show,Eq)
  
  data TestGen = TestGenQuickCheck | TestGenLegacyQuickCheck -- TestGenSmallCheck
    deriving Show
  
  data Proposition = Proposition { propositionType :: PropositionType
                                 , propModule      :: Module
                                 , propName        :: String
                                 , signature       :: [Signature]
                                 , maxSize         :: Maybe Int
                                 , testgen         :: TestGen
                                 } deriving Show
  
  mkProposition :: Module -> String -> Proposition
  mkProposition m f = Proposition { propositionType = BoolProposition
                                  , propModule      = m
                                  , propName        = f
                                  , signature       = [SubjectFunction,Argument 0]
                                  , maxSize         = Nothing
                                  , testgen         = TestGenQuickCheck
                                  }
  
  ofType :: Proposition -> PropositionType -> Proposition
  ofType p t = p{propositionType = t}
  
  withSignature :: Proposition -> [Signature] -> Proposition
  withSignature p s = p{signature = s}
  
  sizeHint :: Proposition -> Int -> Proposition
  sizeHint p n = p{maxSize = Just n}
  
  withTestGen :: Proposition -> TestGen -> Proposition
  withTestGen p f = p{testgen=f}
  
  data PropositionType 
    = IOProposition
    | BoolProposition
    | LegacyQuickCheckProposition
    | QuickCheckProposition 
    deriving Show
  
  data Module = Module {moduleName :: String, searchPath :: String} 
    deriving Show
  
  data PropRes 
    = Error Proposition String 
    | Hold Proposition 
    | HoldWeak Proposition
    | Disprove Proposition
    | DisproveBy Proposition [String] 
    deriving Show
  
  ------------------------------------------------------------------------------------------------------------------------
  
  sourceFile   = ".Hoed/exe/Main.hs"
  buildFiles   = ".Hoed/exe/Main.o .Hoed/exe/Main.hi"
  exeFile      = ".Hoed/exe/Main"
  outFile      = ".Hoed/exe/Main.out"
  errFile      = ".Hoed/exe/Main.compilerMessages"
  treeFilePath = ".Hoed/savedCompTree."
  traceFilePath = ".Hoed/savedTrace."
  
  ------------------------------------------------------------------------------------------------------------------------
  
  lookupPropositions :: [Propositions] -> Vertex -> Maybe Propositions
  lookupPropositions _ RootVertex = Nothing
  lookupPropositions ps v = lookupWith funName lbl ps
    where lbl = (T.unpack . stmtLabel . vertexStmt) v
  
  lookupWith :: Eq a => (b->a) -> a -> [b] -> Maybe b
  lookupWith f x ys = case filter (\y -> f y == x) ys of
    []    -> Nothing
    (y:_) -> Just y
  
  ------------------------------------------------------------------------------------------------------------------------
  
  
  data Judge 
    = Judge Judgement
      -- ^ Returns a Judgement (see Libgraph library).
    | AlternativeTree CompTree Trace
      -- ^ Found counter example with simpler computation tree.
  
  -- TODO: review this function, not sure if complexity suggestion actually makes sense there...
  judgeAll :: UnevalHandler -> (CompTree -> Int) -> Trace -> [Propositions] -> CompTree -> IO CompTree
  judgeAll handler complexity trc ps compTree = foldM f compTree (vertices compTree)
    where
    c = complexity compTree
    f :: CompTree -> Vertex -> IO CompTree
    f curTree v = do
      putStrLn $ take 50 (cycle "-")
      putStrLn $ "Evaluating properties to judge statement: " ++ vertexRes v
      putStrLn $ take 50 (cycle "-")
      case lookupPropositions ps v of
        Nothing  -> do
          putStrLn "*** no propositions"
          return curTree
        (Just p) -> do
          j <- judge' handler trc p v complexity curTree
          case j of
            (Judge jmt)            -> do
              putStrLn $ "*** judgement is " ++ show jmt
              return $ replaceVertex curTree (setJudgement v jmt)
            (AlternativeTree t' _) -> do
               let msg = "Simpler tree suggested with complexity " ++ show (complexity t') 
                         ++ "(current tree has complexity of " ++ show c ++ ")"
               putStrLn $ "*** " ++ msg
               return $ replaceVertex curTree (setJudgement v (Assisted [InconclusiveProperty msg]))
  
  
  -- |Use propositions to judge a computation statement.
  -- First tries restricted and bottom for unevaluated expressions,
  -- then unrestricted, and finally with randomly generated values 
  -- for unevaluated expressions.
  judge :: Trace -> Propositions -> Vertex -> (CompTree -> Int) -> CompTree -> IO Judge
  judge trc p v complexity curTree = do
    putStrLn $ take 50 (cycle "-")
    putStrLn $ "Evaluating properties to judge statement: " ++ vertexRes v
    putStrLn $ take 50 (cycle "-")
    putStrLn "### ATTEMPT 1: with a restricted subject function\n"
    res1 <- judge' RestrictedBottom trc p v complexity curTree
    case res1 of
      (Judge (Assisted _)) -> do 
        putStrLn "### ATTEMPT 2: with an unrestricted subject function\n"
        res2 <- judge' Bottom trc p v complexity curTree
        case res2 of
          (Judge (Assisted _)) -> do 
            putStrLn "### ATTEMPT 3: with randomly generated values\n"
            judge' Forall trc p v complexity curTree
          _                    -> return res2
      (Judge _) -> return res1
    return res1
  
  judge' RestrictedBottom trc p v complexity curTree = do
    pas <- evalPropositions RestrictedBottom trc p v
    let j | propType p == Specify && all holds pas  = (Judge Right)
          | any disproves pas                       = (Judge Wrong)
          | otherwise                               = advice pas
    return j
  
  judge' handler trc p v complexity curTree = do
    pas <- evalPropositions handler trc p v
    let j | propType p == Specify && all holds pas  = return (Judge Right)
          | any disproves pas                       = do 
              let curComplexity = complexity curTree
              (bestComplexity,bestTree,bestTrace) <- simplestTree complexity (extraModules p) pas (curComplexity,curTree,[]) trc v
              if bestComplexity == curComplexity
                then return $ Judge $ Assisted $ [InconclusiveProperty $ "We found values for the unevaluated "
                                                  ++ "expressions in the current statement that falsify\n"
                                                  ++ "a property, however the resulting tree is not simpler."]
                else return (AlternativeTree bestTree bestTrace)
          | otherwise = return (advice pas)
    j
  
  holds :: PropRes -> Bool
  holds (Hold _) = True
  holds (HoldWeak _) = True
  holds _         = False
  
  disproves :: PropRes -> Bool
  disproves (Disprove _)     = True
  disproves (DisproveBy _ _) = True
  disproves _                = False
  
  disprovesBy :: PropRes -> Bool
  disprovesBy (DisproveBy _ _) = True
  disprovesBy _                = False
  
  -- Using the given complexity function, compare the computation trees of the list of
  -- property results and select the simplest tree.
  simplestTree :: (CompTree -> Int) -> [Module] -> [PropRes] -> (Int,CompTree,Trace) -> Trace -> Vertex -> IO (Int,CompTree,Trace)
  simplestTree complexity ms rs cur trc v = foldM (simple2 complexity trc v ms) cur (filter disproves rs)
  
  -- Using the given complexity function, read the computation tree of the given property
  -- into memory and compare its complexity with the complexity of the currently best tree.
  -- Return whichever of these two trees is simplest.
  simple2 :: (CompTree -> Int)  -> Trace -> Vertex -> [Module] -> (Int,CompTree,Trace) -> PropRes -> IO (Int,CompTree,Trace)
  simple2 complexity trc v ms (curComplexity,curTree,curTrace) propRes = do
    reEvalProposition propRes trc v ms
    maybeCandTree  <- restoreTree  $ treeFilePath  ++ resOf propRes
    maybeCandTrace <- restoreTrace $ traceFilePath ++ resOf propRes
    case (maybeCandTree,maybeCandTrace) of
      (Just candTree, Just candTrace) -> do 
        let candComplexity = complexity candTree
        putStrLn $ "Discovered new tree with complexity " ++ show candComplexity 
                   ++ " (current tree is " ++ show curComplexity ++ ")"
        return $ if candComplexity < curComplexity 
                   then (candComplexity,candTree,candTrace)
                   else (curComplexity,curTree,curTrace)
      _ -> do
        putStrLn $ "FAILED to to restore computation tree of " ++ resOf propRes
        return (curComplexity,curTree,curTrace)
  
  advice :: [PropRes] -> Judge
  advice rs' = case filter holds rs' of
    [] -> Judge $ Assisted $ errorMessages rs'
    rs -> Judge $ Assisted $ PassingProperty (commas (map resOf rs)) : errorMessages rs'
  
  commas :: [String] -> String
  commas = concat . (intersperse ", ")
  
  errorMessages :: [PropRes] -> [AssistedMessage]
  errorMessages = foldl (\acc (Error prop msg) -> InconclusiveProperty ("\n---\n\nApplying property " ++ propName prop ++ " gives inconclusive result:\n\n" ++ msg) : acc) [] . filter isError
  
  isError (Error _ _) = True
  isError _           = False
  
  data UnevalHandler = RestrictedBottom | Bottom | Forall | FromList [String] deriving (Eq, Show)
  
  unevalHandler :: UnevalHandler -> PropVarGen String
  unevalHandler RestrictedBottom = propVarError
  unevalHandler Bottom           = propVarError
  unevalHandler Forall           = propVarFresh
  unevalHandler (FromList _)     = propVarFresh
  
  unevalState :: UnevalHandler -> PropVars
  unevalState RestrictedBottom  = propVars0
  unevalState Bottom            = propVars0
  unevalState Forall            = propVars0
  -- unevalState (FromList _)      = propVars0
  -- Replace last line with 
  unevalState (FromList values) = ([],values)
  -- to directly substitute unevaluated expressions with the FromList values.
  -- This is only valid when all randomly generated values are actually substituting
  -- unevaluated expressions (this is not always the case, consider e.g. testing f in
  -- quickCheck p where p f x y = f x == g x y)
  
  resOf :: PropRes -> String
  resOf (Error p _)      = propName p
  resOf (Hold p)         = propName p
  resOf (HoldWeak p)     = propName p
  resOf (Disprove p)     = propName p
  resOf (DisproveBy p _) = propName p
  
  evalPropositions :: UnevalHandler -> Trace -> Propositions -> Vertex -> IO [PropRes]
  evalPropositions _ _ _ RootVertex = return []
  evalPropositions handler trc p v = mapM (evalProposition handler trc v (extraModules p)) (propositions p)
  
  evalProposition :: UnevalHandler -> Trace -> Vertex -> [Module] -> Proposition -> IO PropRes
  evalProposition RestrictedBottom trc v ms prop | not (SubjectFunction `elem` (signature prop)) = do
    putStrLn $ "property " ++ propName prop ++ ": Cannot restrict subject function!"
    return $ Error prop "Cannot restrict subject function!"
  evalProposition handler trc v ms prop = do
    putStrLn $ "property " ++ propName prop
    createDirectoryIfMissing True ".Hoed/exe"
    clean
    prgm <- generateCode handler trc v prop ms
    compile prop
    exit <- compile prop
    case exit of 
      (ExitFailure _) -> do
          err  <- readFile errFile
          putStrLn $ "failed to compile: " ++ err
          return $ Error prop $ "Compilation of {{{\n" ++ prgm ++ "\n}}} failed with:\n" ++ err
      ExitSuccess     -> do 
        exit <- run
        out <- readFile outFile
        putStrLn $ "evaluated to: " ++ out
        return $ mkPropRes prop exit (backspaces out)
  
  
  reEvalProposition :: PropRes -> Trace -> Vertex -> [Module] -> IO PropRes
  reEvalProposition (Disprove prop) _ _ _ = return (Disprove prop) -- no need to re-evaluate
  reEvalProposition (DisproveBy prop values) trc v ms = do
    putStrLn $ "RE-EVALUATE with " ++ concat valuesInBrackets ++ " {"
    (Disprove p) <- evalProposition (FromList valuesInBrackets) trc v ms prop
    putStrLn $ "} RE-EVALUATE"
    return (Disprove p)
    where
    valuesInBrackets = map (\s -> " (" ++ s ++ ") ") values
  
  clean = system $ "rm -f " ++ sourceFile ++ " " ++ exeFile ++ " " ++ buildFiles
  
  compile prop = do
    putStrLn cmd
    system cmd
    where cmd = "ghc -dynamic -i" ++ (searchPath . propModule) prop ++ " -o " ++ exeFile ++ " " ++ sourceFile ++ " > " ++ errFile ++ " 2>&1"
  
  run = system $ exeFile ++ " > " ++ outFile ++ " 2>&1"
  
  generateCode :: UnevalHandler -> Trace -> Vertex -> Proposition -> [Module] -> IO String
  generateCode handler trc v prop ms = do 
    -- Uncomment the next line to dump generated program on screen
    -- hPutStrLn stderr $ "Generated the following program ***\n" ++ prgm ++ "\n***" 
    writeFile sourceFile prgm
    return prgm
    where 
    prgm = generate handler prop ms trc (\i -> EventWithId i (trc VG.! i)) i f
    i    = (stmtIdentifier . vertexStmt) v
    f    = (T.unpack . stmtLabel . vertexStmt) v
  
  mkPropRes :: Proposition -> ExitCode -> String -> PropRes
  mkPropRes prop (ExitFailure _) out        = Error prop out
  mkPropRes prop ExitSuccess out
    | out == "True\n"                       = Hold prop
    | out == "+++ OK, passed 100 tests.\n"  = HoldWeak prop
    | out == "False\n"                      = Disprove prop
    | "Falsifiable" `isInfixOf` out         = DisproveBy prop (reverse . tail . lines $ out)
    | otherwise                             = Error prop out
  
  shorten s
    | length s < 120 = s
    | otherwise    = (take 117 s) ++ "..."
  
  backspaces :: String -> String
  backspaces s = reverse (backspaces' [] s)
    where
    backspaces' s []    = s
    backspaces' s (c:t)
      | c == '\b'       = backspaces' (safeTail s) t
      | otherwise       = backspaces' (c:s)        t
  
    safeTail []    = []
    safeTail (c:s) = s
  
  ------------------------------------------------------------------------------------------------------------------------
  
  type PropVars = ([String],[String]) -- A tuple of used variables, and a supply of fresh variables
  type PropVarGen a = PropVars -> (a,PropVars)
  
  comp :: PropVarGen a -> PropVarGen b -> (a -> b -> c) -> PropVarGen c
  comp x y f vs = let (x', vs')  = x vs
                      (y', vs'') = y vs'
                  in  (f x' y', vs'')
  
  -- MF TODO: this is exactly like liftM2
  liftPV :: (a -> b -> c) -> PropVarGen a -> PropVarGen b -> PropVarGen c
  liftPV f x y = comp x y f
  
  propVars0 :: PropVars
  propVars0 = ([], map show [1..])
  
  propVarError :: PropVarGen String
  -- propVarError = propVarReturn "(error \"Request of value that was unevaluated in original program.\")"
  propVarError (bvs,v:fvs) = (x, (bvs,fvs)) 
   where x = "(error \"Request of value that was unevaluated in original program (underscore " ++ v ++ " in computation statement).\")"
  
  propVarFresh :: PropVarGen String
  propVarFresh (bvs,v:fvs) = (x, (x:bvs,fvs)) where x = 'x':v
  
  propVarReturn :: String -> PropVarGen String
  propVarReturn s vs = (s,vs)
  
  propVarBind :: UnevalHandler -> (String,PropVars) -> Proposition -> String
  propVarBind (FromList _) (propApp,_)       prop = generatePrint prop ++ propApp
  propVarBind _            (propApp,([],_))  prop = generatePrint prop ++ propApp
  propVarBind _            (propApp,(bvs,_)) prop = qc ++ " (\\" ++ bvs' ++ " -> " ++ propApp ++ ")"
    where
    bvs' = concat (intersperse " " bvs)
    qc = case (testgen prop, maxSize prop) of
           (TestGenQuickCheck, Nothing) 
             -> "quickCheckWith stdArgs{maxDiscardRatio=50}"
           (TestGenQuickCheck, Just n)
             -> "quickCheckWith stdArgs{maxDiscardRatio=50,maxSize=" ++ show n ++ "}"
           (TestGenLegacyQuickCheck, Nothing)
             ->  "check defaultConfig{configMaxFail=5000}"
           (TestGenLegacyQuickCheck, Just n)
             -> "check defaultConfig{configMaxFail=5000,configSize=(+" ++ show n ++ ") . (`div` 2)}"
  
  generatePrint :: Proposition -> String
  generatePrint p = case propositionType p of
    IOProposition         -> ""
    BoolProposition       -> "print $ "
    QuickCheckProposition -> "(\\q -> do MkRose res ts <- reduceRose .  unProp . (\\p->unGen p  (mkQCGen 1) 1) . unProperty $ q; print . fromJust . ok $ res) $ "
    LegacyQuickCheckProposition -> "do g <- newStdGen; print . fromJust . ok . (generate 1 g) . evaluate $ "
  
  ------------------------------------------------------------------------------------------------------------------------
  
  generate :: UnevalHandler -> Proposition -> [Module ] -> Trace -> (UID->EventWithId) -> UID -> String -> String
  generate handler prop ms trc getEvent i f = generateHeading prop ms ++ generateMain handler prop trc getEvent i f
  
  generateHeading :: Proposition -> [Module] -> String
  generateHeading prop ms =
    "-- This file is generated by the Haskell debugger Hoed\n"
    ++ generateImport (propModule prop)
    ++ generateImport (Module "qualified Debug.Hoed as Hoed" [])
    ++ qcImports
    ++ foldl (\acc m -> acc ++ generateImport m) "" ms
    where
    qcImports = case propositionType prop of
          BoolProposition -> generateImport (Module "Test.QuickCheck" [])
          IOProposition   -> generateImport (Module "Test.QuickCheck" [])
          LegacyQuickCheckProposition -> qcImports'
          QuickCheckProposition -> qcImports'
                                   ++ generateImport (Module "Test.QuickCheck.Property" [])
                                   ++ generateImport (Module "Test.QuickCheck.Gen" [])
                                   ++ generateImport (Module "Test.QuickCheck.Random" [])
    qcImports'
      = generateImport (Module "System.Random" [])             -- newStdGen
        ++ generateImport (Module "Data.Maybe" [])             -- fromJust
        ++ generateImport (Module "Test.QuickCheck" [])
  
  generateImport :: Module -> String
  generateImport m =  "import " ++ (moduleName m) ++ "\n"
  
  generateMain :: UnevalHandler -> Proposition -> Trace -> (UID->EventWithId) -> UID -> String -> String
  generateMain handler prop trc getEvent i f
    = "main = Hoed.runOstore \"" ++ (propName prop) ++"\" $ "
              ++ propVarBind handler (foldl accSig ((propName prop) ++ " ",unevalState handler) (signature prop)) prop
              -- ++ appValues handler
              ++ "\n"
      where 
      -- appValues (FromList values) = concat (map (" "++) values)
      -- appValues _                 = ""
      accSig :: (String,PropVars) -> Signature -> (String,PropVars)
      accSig (acc,propVars) x = let (s,propVars') = getSig x propVars in (acc ++ " " ++ s, propVars')
      getSig :: Signature -> PropVarGen String
      getSig SubjectFunction = cf
      getSig (Argument i) | i < length args = args !! i
      -- MF TODO: should we do something better when user gives index that is out of bounds?
      getSig Random = propVarFresh
      getSig _ = propVarError
  
      args :: [PropVarGen String]
      args = generateArgs (unevalHandler handler) trc getEvent i
  
      cf :: PropVarGen String
      cf | handler == RestrictedBottom 
             = foldl1 (liftPV $ \acc c -> acc ++ " " ++ c)
               ([ propVarReturn $ "(" ++ genConAp (length args) f
               , generateRes (unevalHandler handler) trc getEvent i
               , propVarReturn $ ")"
               ] :: [PropVarGen String])
         | otherwise = propVarReturn f
  
  generateRes :: (PropVarGen String) -> Trace -> (UID -> EventWithId) -> UID -> PropVarGen String
  generateRes unevalGen trc getEvent i
   | areFun mres = (propVarReturn " {- generateRes -} ") `pvCat`
                   (generateRes unevalGen trc getEvent (eventUID . head . justFuns $ mres)) -- (*)
   | otherwise   = case mres of [_,mr] -> generateRes' unevalGen trc getEvent mr
   --
   -- (*) MF TODO: can there be multiple funs in mres? what then?
   --
   where
   mres = filter isJustRes children
   mr = case mres of [_,e] -> e; _ -> Nothing
   children = dfsChildren frt e
   frt = (mkEventForest trc)
   e   = getEvent i
  
  generateRes' :: PropVarGen String -> Trace -> (UID->EventWithId) -> Maybe EventWithId -> PropVarGen String
  generateRes' unevalGen trc getEvent Nothing = unevalGen
  generateRes' unevalGen trc getEvent (Just e)
   | change (event e) == Fun = 
    case dfsChildren frt e of 
     [_,_    ,_,mr] -> 
      generateRes' unevalGen trc getEvent mr
     [Nothing,_,mr] -> 
      generateRes' unevalGen trc getEvent mr
     as  -> 
      error $ "generateRes': event " ++ show (eventUID e) 
       ++ ":FUN has " ++ show (length as) ++ " children!\nnamely: " ++ commas (map show as)
   | otherwise       = generateExpr unevalGen trc getEvent frt (Just e)
   where
   frt = (mkEventForest trc)
  
  generateArgs :: (PropVarGen String) -> Trace -> (UID -> EventWithId) -> UID -> [PropVarGen String]
  generateArgs unevalGen trc getEvent i =
   (propVarReturn " {- generateArgs -} ") `pvCat`
   pvArg `pvCat` (propVarReturn $ " {- more: " ++ show mres ++ " -} ") 
   : moreArgs unevalGen trc getEvent mr
   where
   pvArg | areFun marg = generateFunMap unevalGen trc getEvent (justFuns marg)
         | otherwise   = case marg of
           [Nothing] -> unevalGen
           [_,ma]    -> generateExpr unevalGen trc getEvent frt ma
   e   = getEvent i
   marg = filter nothingOrArg children
   mres = filter isJustRes children
   mr = case mres of [_,e] -> e; _ -> Nothing
   children = dfsChildren frt e
   frt = (mkEventForest trc)
  
  nothingOrArg Nothing = True
  nothingOrArg (Just e) = isArg e
  
  noArg :: [Maybe a] -> Bool
  noArg [Nothing] = True
  noArg _         = False
  
  areFun :: [Maybe EventWithId] -> Bool
  areFun (_:e:_) = isJustFun e
  areFun _       = False
  
  justFuns :: [Maybe EventWithId] -> [EventWithId]
  justFuns = map fromJust . filter isJustFun
  
  isJustFun :: Maybe EventWithId -> Bool
  isJustFun (Just e) = change (event e) == Fun
  isJustFun Nothing  = False
  
  generateFunMap :: (PropVarGen String) -> Trace -> (UID -> EventWithId) -> [EventWithId] -> PropVarGen String
  generateFunMap unevalGen trc getEvent funs 
   | length funs > 0 = caseOf `pvCat` (pvConcat cases') `pvCat` esac
   | otherwise       = propVarReturn "{- a fun without applications? -}"
   where 
   caseOf = propVarReturn $ " {- funmap with " ++ (show . length $ funs ) ++ " cases -} " 
                            ++ "(\\y -> case y of "
   esac   = propVarReturn ")"
   cases, cases' :: [PropVarGen String]
   cases  = map (\fun -> generateCase unevalGen trc getEvent fun) funs
   cases' = intersperse (propVarReturn "; ") cases
  
  generateCase :: (PropVarGen String) -> Trace -> (UID -> EventWithId) -> EventWithId -> PropVarGen String
  generateCase unevalGen trc getEvent fun =
   (propVarReturn $ " {- CASE " ++ show fun ++ " -} ") `pvCat`
   case args of 
    [] -> (propVarReturn "{- catchall -} _") --> res
    _  -> (foldl1 (liftPV $ \acc c -> acc ++ " " ++ c) args) --> res
   where
   args :: [PropVarGen String]
   args  = map (generateExpr (propVarReturn "_") trc getEvent frt)
           . filter (\(Just e) -> isArg e) . filter isJust . dfsChildren frt $ fun
   res :: PropVarGen String
   res  = generateRes unevalGen trc getEvent (eventUID fun)
   (-->) :: PropVarGen String -> PropVarGen String -> PropVarGen String 
   (-->) = liftPV $ \x y -> x ++ " -> " ++ y
   frt = mkEventForest trc -- MF TODO: create just once and share?
  
  isArg = hasParentPos 0
  
  isRes = hasParentPos 1
  
  isJustRes (Just e) = isRes e
  isJustRes Nothing  = False
  
  hasParentPos i = (==i) . parentPosition . eventParent . event
  
  pvCat :: PropVarGen String -> PropVarGen String -> PropVarGen String
  pvCat = liftPV (++)
  
  pvConcat :: [PropVarGen String] -> PropVarGen String
  pvConcat = foldl pvCat (propVarReturn "")
  
  moreArgs :: PropVarGen String -> Trace -> (UID->EventWithId) -> Maybe EventWithId -> [PropVarGen String]
  moreArgs _ trc getEvent Nothing = []
  moreArgs unevalGen trc getEvent (Just e)
    | change (event e) == Fun = generateArgs unevalGen trc getEvent (eventUID e)
    | otherwise       = []
  
  generateExpr :: PropVarGen String -> Trace -> (UID -> EventWithId) -> EventForest -> Maybe EventWithId -> PropVarGen String
  generateExpr unevalGen _ _ _ Nothing    = unevalGen
  generateExpr unevalGen trc getEvent frt (Just e) = 
    -- (propVarReturn $ "{- generateExpr " ++ show e ++ "-}") `pvCat` 
    case change (event e) of
    (Cons _ (T.unpack -> s)) -> let s' = if isAlpha (head s) then s else "(" ++ s ++ ")"
                  in liftPV (++) ( foldl (liftPV $ \acc c -> acc ++ " " ++ c)
                                   (propVarReturn ("(" ++ s')) cs
                                 ) 
                                 ( propVarReturn ") "
                                 )
    Enter      -> propVarReturn ""
    -- Fun        -> generateFunMap unevalGen trc getEvent (justFuns xs)
    evnt       -> propVarReturn $ "error \"cannot represent: " ++ show evnt ++ "\""
  
   where cs :: [PropVarGen String]
         cs = map (generateExpr unevalGen trc getEvent frt) xs
         xs = (dfsChildren frt e)
  
  
  -- only works if there is 1 argument
  conAp :: Observable b => (a -> b) -> b -> a -> b
  conAp f r x = constrain (f x) r
  
  genConAp :: Int -> String -> String
  genConAp n f | n > 0 = "(\\r " ++ args ++ " -> Hoed.constrain (" ++ f ++ " " ++ args ++ ") r)"
    where args = foldl1 (\a x -> a ++ " " ++ x) xs
          xs = map (\i -> "x" ++ show i) [1..n]
  
  --------------------------------------------------------------------------------
  -- MF TODO: this should probably be part of the Observable class ...
  
  
  (===) :: ParEq a => a -> a -> Bool
  x === y = case parEq x y of (Just b) -> b
                              Nothing  -> error "might be equal"
  
  class ParEq a where
    parEq :: a -> a -> Maybe Bool
    default parEq :: (Generic a, GParEq (Rep a)) => a -> a -> Maybe Bool
    parEq x y = gParEq (from x) (from y)
  
  class GParEq rep where
    gParEq :: rep a -> rep a -> Maybe Bool
  
  orNothing :: IO (Maybe Bool) -> Maybe Bool
  orNothing mb = unsafePerformIO $ ourCatchAllIO mb (\_ -> return Nothing)
  
  catchEq :: Eq a => a -> a -> Maybe Bool
  catchEq x y = orNothing $ do mb <- evaluate (x == y); return (Just mb)
  
  catchGEq :: GParEq rep => rep a -> rep a -> Maybe Bool
  catchGEq x y = orNothing $ x `seq` y `seq` (evaluate $ gParEq x y)
  
  -- Sums: encode choice between constructors
  instance (GParEq a, GParEq b) => GParEq (a :+: b) where
    gParEq x y = let r = gParEq_ x y in r
      where gParEq_ (L1 x) (L1 y) = x `catchGEq` y
            gParEq_ (R1 x) (R1 y) = x `catchGEq` y
            gParEq_ _      _      = Just False
  
  -- Products: encode multiple arguments to constructors
  instance (GParEq a, GParEq b) => GParEq (a :*: b) where
    gParEq x y = let r = gParEq_ x y in r
      where gParEq_ (x :*: x') (y :*: y')
              | any (== (Just False)) mbs = Just False
              | all (== (Just True))  mbs = Just True
              | otherwise                 = Nothing
              where mbs = [(catchGEq x y) `seq` (catchGEq x y), (catchGEq x' y') `seq` (catchGEq x' y')] :: [Maybe Bool]
  
  -- Unit: used for constructors without arguments
  instance GParEq U1 where
  #if __GLASGOW_HASKELL__ >= 710
    gParEq x y = catchEq x y
  #else
    gParEq _ _ = Nothing
  #endif
  
  -- Constants: additional parameters and recursion of kind *
  instance (ParEq a) => GParEq (K1 i a) where
    gParEq x y = let r = gParEq_ x y in r
      where gParEq_ (K1 x) (K1 y) = x `parEq` y
  
  -- Meta: data types
  instance (GParEq a) => GParEq (M1 D d a) where
    gParEq x y = let r = gParEq_ x y in r
      where gParEq_ (M1 x) (M1 y) = x `catchGEq` y
  
  -- Meta: Selectors
  instance (GParEq a, Selector s) => GParEq (M1 S s a) where
    gParEq x y = let r = gParEq_ x y in r
      where gParEq_ (M1 x) (M1 y) = x `catchGEq` y
          
  -- Meta: Constructors
  instance (GParEq a, Constructor c) => GParEq (M1 C c a) where
    gParEq x y = let r = gParEq_ x y in r
      where gParEq_ (M1 x) (M1 y) = x `catchGEq` y
  
  instance (ParEq a)          => ParEq [a]
  instance (ParEq a, ParEq b) => ParEq (a,b)
  instance (ParEq a)          => ParEq (Maybe a)
  instance ParEq Int          where parEq x y = Just (x == y)
  instance ParEq Bool         where parEq x y = Just (x == y)
  instance ParEq Integer      where parEq x y = Just (x == y)
  instance ParEq Float        where parEq x y = Just (x == y)
  instance ParEq Double       where parEq x y = Just (x == y)
  instance ParEq Char         where parEq x y = Just (x == y)
  