content: {-
  A narrowing-based Evaluator for Formulas in Prefix Normal Form based on the compilation technique of LazySmallCheck
  -}
  module Narrowing_Engine where
  
  import Control.Monad
  import Control.Exception
  import System.IO
  import System.Exit
  import Data.Maybe
  import Data.List (partition, findIndex)
  import qualified Generated_Code
  import qualified Typerep
  
  type Pos = [Int]
  
  --  Refinement Tree
  
  data Quantifier = Existential | Universal
  
  data Truth = Eval Bool | Unevaluated | Unknown deriving Eq
  
  conj :: Truth -> Truth -> Truth
  conj (Eval True) b = b
  conj (Eval False) _ = Eval False
  conj b (Eval True) = b
  conj _ (Eval False) = Eval False
  conj Unevaluated _ = Unevaluated
  conj _ Unevaluated = Unevaluated
  conj Unknown Unknown = Unknown
  
  disj :: Truth -> Truth -> Truth
  disj (Eval True) _ = Eval True
  disj (Eval False) b = b
  disj _ (Eval True) = Eval True
  disj b (Eval False) = b
  disj Unknown _ = Unknown
  disj _ Unknown = Unknown
  disj Unevaluated Unevaluated = Unevaluated
  
  ball ts = foldl (\s t -> conj s (value_of t)) (Eval True) ts
  bexists ts = foldl (\s t -> disj s (value_of t)) (Eval False) ts
  
  data Tree = Leaf Truth
    | Variable Quantifier Truth Pos Generated_Code.Narrowing_type Tree
    | Constructor Quantifier Truth Pos [Tree]
  
  value_of :: Tree -> Truth
  value_of (Leaf r) = r
  value_of (Variable _ r _ _ _) = r
  value_of (Constructor _ r _ _) = r
  
  data Edge = V Pos Generated_Code.Narrowing_type | C Pos Int
  type Path = [Edge]
  
  position_of :: Edge -> Pos
  position_of (V pos _) = pos
  position_of (C pos _) = pos
  
  -- Operation find: finds first relevant unevaluated node and returns its path
  
  find :: Tree -> Path
  find (Leaf Unevaluated) = []
  find (Variable _ _ pos ty t) = V pos ty : (find t)
  find (Constructor _ _ pos ts) = C pos i : find (ts !! i)
    where  
      Just i = findIndex (\t -> value_of t == Unevaluated) ts
  
  -- Operation update: updates the leaf and the cached truth values results along the path
  
  update :: Path -> Truth -> Tree -> Tree
  update [] v (Leaf _) = Leaf v
  update (V _ _ : es) v (Variable q r p ty t) = Variable q (value_of t') p ty t'
    where
      t' = update es v t    
  update (C _ i : es) v (Constructor q r pos ts) = Constructor q r' pos ts' 
    where
      (xs, y : ys) = splitAt i ts
      y' = update es v y
      ts' = xs ++ (y' : ys)
      r' = valueOf ts'
      valueOf = case q of { Universal -> ball; Existential -> bexists}
   
  -- Operation: refineTree
  
  replace :: (Tree -> Tree) -> Path -> Tree -> Tree
  replace f [] t = (f t)
  replace f (V _ _ : es) (Variable q r pos ty t) = Variable q r pos ty (replace f es t)
  replace f (C _ i : es) (Constructor q r pos ts) = Constructor q r pos (xs ++ (replace f es y : ys))
     where
       (xs, y : ys) = splitAt i ts
  
  refine_tree :: [Edge] -> Pos -> Tree -> Tree
  refine_tree es p t = replace refine (path_of_position p es) t
    where
      path_of_position p es = takeWhile (\e -> position_of e /= p) es  
      refine (Variable q r p (Generated_Code.Narrowing_sum_of_products ps) t) =
        Constructor q r p [ foldr (\(i,ty) t -> Variable q r (p++[i]) ty t) t (zip [0..] ts) | ts <- ps ]
  
  -- refute
  
  refute :: ([Generated_Code.Narrowing_term] -> Bool) -> Bool -> Int -> Tree -> IO Tree
  refute exec genuine_only d t = ref t
    where
      ref t =
        let path = find t in
          do
            t' <- answer genuine_only (exec (terms_of [] path)) (\b -> return (update path (Eval b) t))
              (\p -> return (if length p < d then refine_tree path p t else update path Unknown t));
            case value_of t' of
              Unevaluated -> ref t'
              _ -> return t'
  
  depthCheck :: Bool -> Int -> Generated_Code.Property -> IO ()
  depthCheck genuine_only d p = refute (checkOf p) genuine_only d (treeOf 0 p) >>= (\t -> 
    case value_of t of
     Eval False -> putStrLn ("SOME (" ++ show (counterexampleOf (reifysOf p) (exampleOf 0 t)) ++ ")")  
     _ -> putStrLn ("NONE"))
  
  -- Term refinement
  
  -- Operation: termOf
  
  term_of :: Pos -> Path -> Generated_Code.Narrowing_term
  term_of p (C [] i : es) = Generated_Code.Narrowing_constructor i (terms_of p es)
  term_of p [V [] ty] = Generated_Code.Narrowing_variable p ty
  
  terms_of :: Pos -> Path -> [Generated_Code.Narrowing_term]
  terms_of p es = terms_of' 0 es
    where
      terms_of' i [] = []
      terms_of' i (e : es) = (t : terms_of' (i + 1) rs) 
        where
          (ts, rs) = Data.List.partition (\e -> head (position_of e) == i) (e : es)
          t = term_of (p ++ [i]) (map (map_pos tail) ts)
          map_pos f (V p ty) = V (f p) ty
          map_pos f (C p ts) = C (f p) ts
  
  -- Answers
  
  data Answer = Known Bool | Refine Pos;
  
  answeri :: a -> (a -> IO b) -> (Pos -> IO b) -> IO b;
  answeri a known unknown =
    do res <- try (evaluate a)
       case res of
         Right b -> known b
         Left (ErrorCall ('\0':p)) -> unknown (map fromEnum p)
         Left e -> throw e
  
  answer :: Bool -> Bool -> (Bool -> IO b) -> (Pos -> IO b) -> IO b;
  answer genuine_only a known unknown =
    Control.Exception.catch (answeri a known unknown) 
      (\ (PatternMatchFail _) -> known genuine_only)
  
  
  -- presentation of counterexample
  
  
  instance Show Typerep.Typerep where {
    show (Typerep.Typerep c ts) = "Type (\"" ++ c ++ "\", " ++ show ts ++ ")";
  };
  
  instance Show Generated_Code.Term where {
    show (Generated_Code.Const c t) = "Const (\"" ++ c ++ "\", " ++ show t ++ ")";
    show (Generated_Code.App s t) = "(" ++ show s ++ ") $ (" ++ show t ++ ")";
    show (Generated_Code.Abs s ty t) = "Abs (\"" ++ s ++ "\", " ++ show ty ++ ", " ++ show t ++ ")";
    show (Generated_Code.Free s ty) = "Free (\"" ++ s ++  "\", " ++ show ty ++ ")";
  };
  {-
  posOf :: Edge -> Pos
  posOf (VN pos _) = pos
  posOf (CtrB pos _) = pos
  
  tailPosEdge :: Edge -> Edge
  tailPosEdge (VN pos ty) = VN (tail pos) ty
  tailPosEdge (CtrB pos ts) = CtrB (tail pos) ts
  
  termOf :: Pos -> Tree -> (Narrowing_term, Tree)
  termOf pos = if Ctr i (termListOf (pos ++ [i]) )
  termOf pos [VN [] ty] = Var pos ty
  
  termListOf :: Pos -> [Narrowing_term]
  termListOf pos es = termListOf' 0 es
    where
      termListOf' i [] = []
      termListOf' i (e : es) =
        let
          (ts, rs) = List.partition (\e -> head (posOf e) == i) (e : es)
          t = termOf (pos ++ [i]) (map tailPosEdge ts)
        in
          (t : termListOf' (i + 1) rs) 
  
  termlist_of :: Pos -> QuantTree -> ([Term], QuantTree)
  
  termlist_of p' (Node r)
  
  term_of p' (VarNode _ _ p ty t) = if p == p' then
      (Some (Var ty), t)
    else
      (None, t)
  term_of p' (CtrBranch q _ p ts) =
    if p == p' then
      let
        i = findindex (\t -> evalOf t == Eval False)        
      in
        Ctr i (termlist_of (p ++ [i])  (ts ! i) [])
    else
      error ""
  -}
  termlist_of :: Pos -> ([Generated_Code.Narrowing_term], Tree) -> ([Generated_Code.Narrowing_term], Tree)
  termlist_of p' (terms, Leaf b) = (terms, Leaf b) 
  termlist_of p' (terms, Variable q r p ty t) = if p' == take (length p') p then
      termlist_of p' (terms ++ [Generated_Code.Narrowing_variable p ty], t)
    else
      (terms, Variable q r p ty t)
  termlist_of p' (terms, Constructor q r p ts) = if p' == take (length p') p then
      let
        Just i = findIndex (\t -> value_of t == Eval False) ts
        (subterms, t') = fixp (\j -> termlist_of (p ++ [j])) 0 ([], ts !! i)
      in
        (terms ++ [Generated_Code.Narrowing_constructor i subterms], t')
    else
      (terms, Constructor q r p ts)
    where
      fixp f j s = if length (fst (f j s)) == length (fst s) then s else fixp f (j + 1) (f j s)
  
  
  alltermlist_of :: Pos -> ([Generated_Code.Narrowing_term], Tree) -> [([Generated_Code.Narrowing_term], Tree)]
  alltermlist_of p' (terms, Leaf b) = [(terms, Leaf b)] 
  alltermlist_of p' (terms, Variable q r p ty t) = if p' == take (length p') p then
      alltermlist_of p' (terms ++ [Generated_Code.Narrowing_variable p ty], t)
    else
      [(terms, Variable q r p ty t)]
  alltermlist_of p' (terms, Constructor q r p ts) =
    if p' == take (length p') p then
      let
        its = filter (\(i, t) -> value_of t == Eval False) (zip [0..] ts)
      in
        concatMap
          (\(i, t) -> map (\(subterms, t') -> (terms ++ [Generated_Code.Narrowing_constructor i subterms], t'))
             (fixp (\j -> alltermlist_of (p ++ [j])) 0 ([], t))) its
    else
      [(terms, Constructor q r p ts)]
    where
      fixp f j s = case (f j s) of
        [s'] -> if length (fst s') == length (fst s) then [s'] else concatMap (fixp f (j + 1)) (f j s)
        _ -> concatMap (fixp f (j + 1)) (f j s)
  
  data Example = UnivExample Generated_Code.Narrowing_term Example | ExExample [(Generated_Code.Narrowing_term, Example)] | EmptyExample
  
  quantifierOf (Variable q _ _ _ _) = q
  quantifierOf (Constructor q _ _ _) = q
  
  exampleOf :: Int -> Tree -> Example
  exampleOf _ (Leaf _) = EmptyExample
  exampleOf p t =
     case quantifierOf t of
       Universal ->
         let
           ([term], rt) = termlist_of [p] ([], t)
         in UnivExample term (exampleOf (p + 1) rt)
       Existential ->
         ExExample (map (\([term], rt) -> (term, exampleOf (p + 1) rt)) (alltermlist_of [p] ([], t)))
  
  data Counterexample = Universal_Counterexample (Generated_Code.Term, Counterexample)
    | Existential_Counterexample [(Generated_Code.Term, Counterexample)] | Empty_Assignment
    
  instance Show Counterexample where {
  show Empty_Assignment = "Narrowing_Generators.Empty_Assignment";
  show (Universal_Counterexample x) = "Narrowing_Generators.Universal_Counterexample" ++ show x;
  show (Existential_Counterexample x) = "Narrowing_Generators.Existential_Counterexample" ++ show x;
  };
  
  counterexampleOf :: [Generated_Code.Narrowing_term -> Generated_Code.Term] -> Example -> Counterexample
  counterexampleOf [] EmptyExample = Empty_Assignment
  counterexampleOf (reify : reifys) (UnivExample t ex) = Universal_Counterexample (reify t, counterexampleOf reifys ex)
  counterexampleOf (reify : reifys) (ExExample exs) = Existential_Counterexample (map (\(t, ex) -> (reify t, counterexampleOf reifys ex)) exs)
  
  checkOf :: Generated_Code.Property -> [Generated_Code.Narrowing_term] -> Bool
  checkOf (Generated_Code.Property b) = (\[] -> b)
  checkOf (Generated_Code.Universal _ f _) = (\(t : ts) -> checkOf (f t) ts)
  checkOf (Generated_Code.Existential _ f _) = (\(t : ts) -> checkOf (f t) ts)
  
  treeOf :: Int -> Generated_Code.Property -> Tree
  treeOf n (Generated_Code.Property _) = Leaf Unevaluated
  treeOf n (Generated_Code.Universal ty f _)  = Variable Universal Unevaluated [n] ty (treeOf (n + 1) (f undefined)) 
  treeOf n (Generated_Code.Existential ty f _) = Variable Existential Unevaluated [n] ty (treeOf (n + 1) (f undefined))
  
  reifysOf :: Generated_Code.Property -> [Generated_Code.Narrowing_term -> Generated_Code.Term]
  reifysOf (Generated_Code.Property _) = []
  reifysOf (Generated_Code.Universal _ f r)  = (r : (reifysOf (f undefined)))
  reifysOf (Generated_Code.Existential _ f r) = (r : (reifysOf (f undefined)))
  
  