bulwahn@41933: module Narrowing_Engine where {
bulwahn@41905: 
bulwahn@41905: import Monad;
bulwahn@41905: import Control.Exception;
bulwahn@41905: import System.IO;
bulwahn@41905: import System.Exit;
bulwahn@44751: import Generated_Code;
bulwahn@41905: 
bulwahn@41908: type Pos = [Int];
bulwahn@41905: 
bulwahn@41905: -- Term refinement
bulwahn@41905: 
bulwahn@43047: new :: Pos -> [[Narrowing_type]] -> [Narrowing_term];
bulwahn@41905: new p ps = [ Ctr c (zipWith (\i t -> Var (p++[i]) t) [0..] ts)
bulwahn@41905:            | (c, ts) <- zip [0..] ps ];
bulwahn@41905: 
bulwahn@43047: refine :: Narrowing_term -> Pos -> [Narrowing_term];
bulwahn@41905: refine (Var p (SumOfProd ss)) [] = new p ss;
bulwahn@41905: refine (Ctr c xs) p = map (Ctr c) (refineList xs p);
bulwahn@41905: 
bulwahn@43047: refineList :: [Narrowing_term] -> Pos -> [[Narrowing_term]];
bulwahn@41908: refineList xs (i:is) = let (ls, x:rs) = splitAt i xs in [ls ++ y:rs | y <- refine x is];
bulwahn@41905: 
bulwahn@41905: -- Find total instantiations of a partial value
bulwahn@41905: 
bulwahn@43047: total :: Narrowing_term -> [Narrowing_term];
bulwahn@41905: total (Ctr c xs) = [Ctr c ys | ys <- mapM total xs];
bulwahn@41905: total (Var p (SumOfProd ss)) = [y | x <- new p ss, y <- total x];
bulwahn@41905: 
bulwahn@41905: -- Answers
bulwahn@41905: 
bulwahn@45003: answeri :: a -> (a -> IO b) -> (Pos -> IO b) -> IO b;
bulwahn@45003: answeri a known unknown =
bulwahn@41905:   try (evaluate a) >>= (\res ->
bulwahn@41905:      case res of
bulwahn@41905:        Right b -> known b
bulwahn@41908:        Left (ErrorCall ('\0':p)) -> unknown (map fromEnum p)
bulwahn@41905:        Left e -> throw e);
bulwahn@41905: 
bulwahn@45003: answer :: Bool -> (Bool -> IO b) -> (Pos -> IO b) -> IO b;
bulwahn@45003: answer a known unknown =
bulwahn@45003:   Control.Exception.catch (answeri a known unknown) 
bulwahn@45003:     (\ (PatternMatchFail _) -> known True);
bulwahn@45003: 
bulwahn@41905: -- Refute
bulwahn@41905: 
bulwahn@41905: str_of_list [] = "[]";
bulwahn@41905: str_of_list (x:xs) = "(" ++ x ++ " :: " ++ str_of_list xs ++ ")";
bulwahn@41905: 
bulwahn@43047: report :: Result -> [Narrowing_term] -> IO Int;
bulwahn@43079: report r xs = putStrLn ("SOME (" ++ (str_of_list $ zipWith ($) (showArgs r) xs) ++ ")") >> hFlush stdout >> exitWith ExitSuccess;
bulwahn@41905: 
bulwahn@41905: eval :: Bool -> (Bool -> IO a) -> (Pos -> IO a) -> IO a;
bulwahn@41905: eval p k u = answer p (\p -> answer p k u) u;
bulwahn@41905: 
bulwahn@43047: ref :: Result -> [Narrowing_term] -> IO Int;
bulwahn@41905: ref r xs = eval (apply_fun r xs) (\res -> if res then return 1 else report r xs) (\p -> sumMapM (ref r) 1 (refineList xs p));
bulwahn@41905:           
bulwahn@41908: refute :: Result -> IO Int;
bulwahn@41905: refute r = ref r (args r);
bulwahn@41905: 
bulwahn@41908: sumMapM :: (a -> IO Int) -> Int -> [a] -> IO Int;
bulwahn@41905: sumMapM f n [] = return n;
bulwahn@41905: sumMapM f n (a:as) = seq n (do m <- f a ; sumMapM f (n+m) as);
bulwahn@41905: 
bulwahn@41905: -- Testable
bulwahn@41905: 
bulwahn@41905: instance Show Typerep where {
bulwahn@41908:   show (Typerep c ts) = "Type (\"" ++ c ++ "\", " ++ show ts ++ ")";
bulwahn@41905: };
bulwahn@41905: 
bulwahn@41933: instance Show Term where {
bulwahn@41905:   show (Const c t) = "Const (\"" ++ c ++ "\", " ++ show t ++ ")";
bulwahn@41905:   show (App s t) = "(" ++ show s ++ ") $ (" ++ show t ++ ")";
bulwahn@43079:   show (Abs s ty t) = "Abs (\"" ++ s ++ "\", " ++ show ty ++ ", " ++ show t ++ ")";
bulwahn@43079:   show (Free s ty) = "Free (\"" ++ s ++  "\", " ++ show ty ++ ")";
bulwahn@41905: };
bulwahn@41905: 
bulwahn@41905: data Result =
bulwahn@43047:   Result { args     :: [Narrowing_term]
bulwahn@43047:          , showArgs :: [Narrowing_term -> String]
bulwahn@43047:          , apply_fun    :: [Narrowing_term] -> Bool
bulwahn@41905:          };
bulwahn@41905: 
bulwahn@41908: data P = P (Int -> Int -> Result);
bulwahn@41905: 
bulwahn@43047: run :: Testable a => ([Narrowing_term] -> a) -> Int -> Int -> Result;
bulwahn@41905: run a = let P f = property a in f;
bulwahn@41905: 
bulwahn@41905: class Testable a where {
bulwahn@43047:   property :: ([Narrowing_term] -> a) -> P;
bulwahn@41905: };
bulwahn@41905: 
bulwahn@41905: instance Testable Bool where {
bulwahn@41905:   property app = P $ \n d -> Result [] [] (app . reverse);
bulwahn@41905: };
bulwahn@41905: 
bulwahn@43079: instance (Partial_term_of a, Narrowing a, Testable b) => Testable (a -> b) where {
bulwahn@41905:   property f = P $ \n d ->
bulwahn@41962:     let C t c = narrowing d
bulwahn@41905:         c' = conv c
bulwahn@41905:         r = run (\(x:xs) -> f xs (c' x)) (n+1) d
bulwahn@43079:     in  r { args = Var [n] t : args r, showArgs = (show . partial_term_of (Type :: Itself a)) : showArgs r };
bulwahn@41905: };
bulwahn@41905: 
bulwahn@41905: -- Top-level interface
bulwahn@41905: 
bulwahn@41908: depthCheck :: Testable a => Int -> a -> IO ();
bulwahn@41905: depthCheck d p =
bulwahn@42090:   (refute $ run (const p) 0 d) >> putStrLn ("NONE") >> hFlush stdout;
bulwahn@41905: 
bulwahn@41908: smallCheck :: Testable a => Int -> a -> IO ();
bulwahn@42090: smallCheck d p = mapM_ (`depthCheck` p) [0..d] >> putStrLn ("NONE") >> hFlush stdout;
bulwahn@41905: 
bulwahn@41905: }
bulwahn@41905: