|
module Narrowing_Engine where {
import Control.Monad;
import Control.Exception;
import System.IO;
import System.Exit;
import qualified Typerep;
import qualified Generated_Code;
type Pos = [Int];
-- Term refinement
new :: Pos -> [[Generated_Code.Narrowing_type]] -> [Generated_Code.Narrowing_term];
new p ps = [ Generated_Code.Narrowing_constructor c (zipWith (\i t -> Generated_Code.Narrowing_variable (p++[i]) t) [0..] ts)
| (c, ts) <- zip [0..] ps ];
refine :: Generated_Code.Narrowing_term -> Pos -> [Generated_Code.Narrowing_term];
refine (Generated_Code.Narrowing_variable p (Generated_Code.Narrowing_sum_of_products ss)) [] = new p ss;
refine (Generated_Code.Narrowing_constructor c xs) p = map (Generated_Code.Narrowing_constructor c) (refineList xs p);
refineList :: [Generated_Code.Narrowing_term] -> Pos -> [[Generated_Code.Narrowing_term]];
refineList xs (i:is) = let (ls, x:rs) = splitAt i xs in [ls ++ y:rs | y <- refine x is];
-- Find total instantiations of a partial value
total :: Generated_Code.Narrowing_term -> [Generated_Code.Narrowing_term];
total (Generated_Code.Narrowing_constructor c xs) = [Generated_Code.Narrowing_constructor c ys | ys <- mapM total xs];
total (Generated_Code.Narrowing_variable p (Generated_Code.Narrowing_sum_of_products ss)) = [y | x <- new p ss, y <- total x];
-- Answers
answeri :: a -> (Bool -> a -> IO b) -> (Pos -> IO b) -> IO b;
answeri a known unknown =
try (evaluate a) >>= (\res ->
case res of
Right b -> known True b
Left (ErrorCall ('\0':p)) -> unknown (map fromEnum p)
Left e -> throw e);
answer :: Bool -> 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 False genuine_only);
-- Refute
str_of_list [] = "[]";
str_of_list (x:xs) = "(" ++ x ++ " :: " ++ str_of_list xs ++ ")";
report :: Bool -> Result -> [Generated_Code.Narrowing_term] -> IO Int;
report genuine r xs = putStrLn ("SOME (" ++ (if genuine then "true" else "false") ++
", " ++ (str_of_list $ zipWith ($) (showArgs r) xs) ++ ")") >> hFlush stdout >> exitWith ExitSuccess;
eval :: Bool -> Bool -> (Bool -> Bool -> IO a) -> (Pos -> IO a) -> IO a;
eval genuine_only p k u = answer genuine_only p k u;
ref :: Bool -> Result -> [Generated_Code.Narrowing_term] -> IO Int;
ref genuine_only r xs = eval genuine_only (apply_fun r xs) (\genuine res -> if res then return 1 else report genuine r xs)
(\p -> sumMapM (ref genuine_only r) 1 (refineList xs p));
refute :: Bool -> Result -> IO Int;
refute genuine_only r = ref genuine_only r (args r);
sumMapM :: (a -> IO Int) -> Int -> [a] -> IO Int;
sumMapM f n [] = return n;
sumMapM f n (a:as) = seq n (do m <- f a ; sumMapM f (n+m) as);
-- Testable
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 ++ ")";
};
data Result =
Result { args :: [Generated_Code.Narrowing_term]
, showArgs :: [Generated_Code.Narrowing_term -> String]
, apply_fun :: [Generated_Code.Narrowing_term] -> Bool
};
data P = P (Int -> Int -> Result);
run :: Testable a => ([Generated_Code.Narrowing_term] -> a) -> Int -> Int -> Result;
run a = let P f = property a in f;
class Testable a where {
property :: ([Generated_Code.Narrowing_term] -> a) -> P;
};
instance Testable Bool where {
property app = P $ \n d -> Result [] [] (app . reverse);
};
instance (Generated_Code.Partial_term_of a, Generated_Code.Narrowing a, Testable b) => Testable (a -> b) where {
property f = P $ \n d ->
let Generated_Code.Narrowing_cons t c = Generated_Code.narrowing d
c' = Generated_Code.conv c
r = run (\(x:xs) -> f xs (c' x)) (n+1) d
in r { args = Generated_Code.Narrowing_variable [n] t : args r,
showArgs = (show . Generated_Code.partial_term_of (Generated_Code.Type :: Generated_Code.Itself a)) : showArgs r };
};
-- Top-level interface
depthCheck :: Testable a => Bool -> Int -> a -> IO ();
depthCheck genuine_only d p =
(refute genuine_only $ run (const p) 0 d) >> putStrLn ("NONE") >> hFlush stdout;
smallCheck :: Testable a => Bool -> Int -> a -> IO ();
smallCheck genuine_only d p = mapM_ (\d -> depthCheck genuine_only d p) [0..d] >> putStrLn ("NONE") >> hFlush stdout;
}
¤ Dauer der Verarbeitung: 0.1 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
