{-# LANGUAGE CPP #-} module MagicHaskeller.Options where #ifdef TFRANDOM import System.Random.TF(seedTFGen, TFGen) #else import System.Random(mkStdGen, StdGen) #endif import MagicHaskeller.Execute(unsafeExecute) import MagicHaskeller.MemoToFiles(MemoCond, MemoType(..)) import MagicHaskeller.CoreLang import MagicHaskeller.MyDynamic import MagicHaskeller.Types(Type) -- | options that limit the hypothesis space. data Opt a = Opt{ Opt a -> Maybe a primopt :: Maybe a -- ^ Use this option if you want to use a different component library for the stage of solving the inhabitation problem. -- @Nothing@ means using the same one. -- This option makes sense only when using *SF style generators, because otherwise the program generation is not staged. -- Using a minimal set for solving the inhabitation and a redundant library for the real program generation can be a good bet. , Opt a -> Int memodepth :: Int -- ^ memoization depth. (Sub)expressions within this size are memoized, while greater expressions will be recomputed (to save the heap space). Only effective when using 'ProgGen' and unless using the 'everythingIO' family. , Opt a -> Type -> Int -> Bool memoCondPure :: Type -> Int -> Bool -- ^ This represents when to memoize. It takes the query type and the query depth, and returns @True@ if the corresponding entry should be looked up from the lazy memo table. Currently this only works for ProgGenSF. , Opt a -> MemoCond memoCond :: MemoCond -- ^ This represents which memoization table to be used based on the query type and the search depth, when using the 'everythingIO' family. , Opt a -> VarLib -> CoreExpr -> Dynamic execute :: VarLib -> CoreExpr -> Dynamic -- timeout はこの中でやるべき．IO Dynamicの場合にunsafePerformIOを2回やると変なことになりそうなので． , Opt a -> Maybe Int timeout :: Maybe Int -- ^ @Just ms@ sets the timeout to @ms@ microseconds. Also, my implementation of timeout also catches inevitable exceptions like stack space overflow. Note that setting timeout makes the library referentially untransparent. (But currently @Just 20000@ is the default!) Setting this option to @Nothing@ disables both timeout and capturing exceptions. , Opt a -> Bool forcibleTimeout :: Bool -- ^ If this option is @True@, 'System.Posix.Process.forkProcess' instead of 'Control.Concurrent.forkIO' is used for timeout. -- The former is much heavier than the latter, but is more preemptive and thus is necessary for interrupting some infinite loops. -- This record is ignored if FORCIBLETO is not defined. , Opt a -> Bool guess :: Bool -- ^ If this option is @True@, the program guesses whether each function is a case/catamorphism/paramorphism or not. -- This information is used to filter out some duplicate expressions. -- (History: I once abandoned this guessing strategy around the time I moved to the library implementation, because -- I could not formally prove the exhaustiveness of the resulting algorithm. -- For this reason, the old standalone version of MagicHaskeller uses this strategy, but almost the same effect -- can be obtained by setting this option to True, or using 'MagicHaskeller.init075' instead of 'MagicHaskeller.initialize'. , Opt a -> Bool contain :: Bool -- ^ This option is now obsolete, and we always assume True now. -- If this option was @False@, data structures might not contain functions, and thus types like @[Int->Int]@, @(Int->Bool, Char)@, etc. were not permitted. -- (NB: recently I noticed that making this @False@ might not improve the efficiency of generating lambda terms at all, though when I generated combinatory expressions it WAS necessary. -- In fact, I mistakenly turned this limitation off, and my code always regarded this as True, but I did not notice that, so this option can be obsoleted.) , Opt a -> Bool constrL :: Bool -- ^ If this option is @True@, matching at the antecedent of induction rules may occur, which constrains generation of existential types. -- You need to use prefixed @(->)@ to show that some parameter can be matched at the antecedent, e.g., -- @'p' [| ( []::[a], (:)::a->[a]->[a], foldr :: (a->b->b) -> b -> (->) [a] b ) |]@ -- See LibTH.hs for examples. , Opt a -> Int tvndelay:: Int -- ^ Each time the type variable which appears in the return type of a function (e.g. @b@ in @foldr::(a->b->b)->b->[a]->b@) -- is expanded to a function type, the search priority of the current computation is lowered by this number. -- It's default value is 1, which means there is nothing special, and the priority for each expression corresponds -- to the number of function applications in the expression. -- -- Example: when tvndelay = 1, -- -- The priority of -- -- > \xs -> foldr (\x y -> x+y) 0 xs -- -- is 5, -- because there are five @$@'s in -- -- > \xs -> ((foldr $ (\x y -> ((+) $ x) $ y)) $ 0) xs -- -- -- The priority of -- -- > \xs ys -> foldr (\x y zs -> x : y zs) (\ws->ws) xs ys -- -- is 7, -- because there are seven @$@'s in -- -- > \xs ys -> (((foldr $ (\x y zs -> (((:) $ x) $ y) $ zs)) $ (\ws->ws)) $ xs) $ ys -- -- -- Example: when tvndelay = 2, -- -- The priority of -- -- > \xs -> foldr (\x y -> x+y) 0 xs -- -- is 5, -- because there are five @$@'s in -- -- > \xs -> ((foldr $ (\x y -> ((+) $ x) $ y)) $ 0) xs -- -- The priority of -- -- > \xs ys -> foldr (\x y zs -> x : y zs) (\ws->ws) xs ys -- -- is 8, -- because there are eight @$@'s in -- -- > \xs ys -> (((foldr $ (\x y zs -> (((:) $ x) $ y) $ zs)) $ (\ws->ws)) $ xs) $$ ys -- -- where @$$@ denotes the function application caused by expanding a type variable into a function type. , Opt a -> Bool tv1 :: Bool -- ^ If this option is @True@, the return type of functions returning a type variable (e.g. @b@ in @foldr::(a->b->b)->b->[a]->b@) -- can only be replaced with @Eval t => t@ and @Eval t => u -> t@, while if @False@ with @Eval t => t@, @Eval t => u->t@, @Eval t => u->v->t@, etc., where @Eval t@ means t cannot be replaced with a function. -- The restriction can be amended if the tuple constructor and destructors are available. , Opt a -> Bool tv0 :: Bool #ifdef TFRANDOM , stdgen :: TFGen -- ^ The random seed. #else , Opt a -> StdGen stdgen :: StdGen -- ^ The random seed. #endif , Opt a -> [Int] nrands :: [Int] -- ^ number of random samples at each depth, for each type, for the filter applied during synthesis (used by ProgGenSF, &c.). , Opt a -> Int -> Int fcnrand :: Int -> Int -- ^ number of random samples at each depth, for each type, for the filter applied after synthesis (used by filterThenF, &c.). } -- | default options -- -- > options = Opt{ primopt = Nothing -- > , memodepth = 10 -- > , memoCondPure = \ _type depth -> 0<depth -- > , memoCond = \ _type depth -> return $ if depth < 10 then Ram else Recompute -- > , execute = unsafeExecute -- > , timeout = Just 20000 -- > , forcibleTimeout = False -- > , guess = False -- > , contain = True -- > , constrL = False -- > , tv1 = False #ifdef TFRANDOM -- > , stdgen = seedTFGen (3497676378205993723,16020016691208771845,6545968067796471226,2770936286170065919) #else -- > , stdgen = mkStdGen 123456 #endif -- > , nrands = repeat 5 -- > , fcnrand = (6+) -- > } options :: Opt a options :: Opt a options = Opt :: forall a. Maybe a -> Int -> (Type -> Int -> Bool) -> MemoCond -> (VarLib -> CoreExpr -> Dynamic) -> Maybe Int -> Bool -> Bool -> Bool -> Bool -> Int -> Bool -> Bool -> StdGen -> [Int] -> (Int -> Int) -> Opt a Opt{ primopt :: Maybe a primopt = Maybe a forall a. Maybe a Nothing , memodepth :: Int memodepth = Int 10 , memoCondPure :: Type -> Int -> Bool memoCondPure = \ Type _type Int depth -> Int 0Int -> Int -> Bool forall a. Ord a => a -> a -> Bool <Int depth , memoCond :: MemoCond memoCond = \ Type _ty Int d -> MemoType -> IO MemoType forall (m :: * -> *) a. Monad m => a -> m a return (MemoType -> IO MemoType) -> MemoType -> IO MemoType forall a b. (a -> b) -> a -> b $ if Int dInt -> Int -> Bool forall a. Ord a => a -> a -> Bool <Int 10 then MemoType Ram else MemoType Recompute , execute :: VarLib -> CoreExpr -> Dynamic execute = VarLib -> CoreExpr -> Dynamic unsafeExecute , timeout :: Maybe Int timeout = Int -> Maybe Int forall a. a -> Maybe a Just Int 20000 , forcibleTimeout :: Bool forcibleTimeout = Bool False , guess :: Bool guess = Bool False , contain :: Bool contain = Bool True , constrL :: Bool constrL = Bool False , tvndelay :: Int tvndelay = Int 1 , tv1 :: Bool tv1 = Bool False , tv0 :: Bool tv0 = Bool False #ifdef TFRANDOM , stdgen = seedTFGen (3497676378205993723,16020016691208771845,6545968067796471226,2770936286170065919) #else , stdgen :: StdGen stdgen = Int -> StdGen mkStdGen Int 123456 #endif , nrands :: [Int] nrands = [Int] nrnds , fcnrand :: Int -> Int fcnrand = (Int 6Int -> Int -> Int forall a. Num a => a -> a -> a +) } -- reducer (opt,_,_,_,_) = execute opt forget :: Opt a -> Opt () forget :: Opt a -> Opt () forget Opt a opt = case Opt a -> Maybe a forall a. Opt a -> Maybe a primopt Opt a opt of Maybe a Nothing -> Opt a opt{primopt :: Maybe () primopt = Maybe () forall a. Maybe a Nothing} Just a _ -> Opt a opt{primopt :: Maybe () primopt = () -> Maybe () forall a. a -> Maybe a Just ()} nrnds :: [Int] nrnds = (Integer -> Int) -> [Integer] -> [Int] forall a b. (a -> b) -> [a] -> [b] map Integer -> Int forall p p. Num p => p -> p fnrnds [Integer 0..] chopRnds :: [[a]] -> [[a]] chopRnds :: [[a]] -> [[a]] chopRnds = (Int -> [a] -> [a]) -> [Int] -> [[a]] -> [[a]] forall a b c. (a -> b -> c) -> [a] -> [b] -> [c] zipWith Int -> [a] -> [a] forall a. Int -> [a] -> [a] take [Int] nrnds {- fnrnds n | n <= 5 = 5 | n < 10 = 10-n | otherwise = 1 -} fnrnds :: p -> p fnrnds p _ = p 5 {- fnrnds n | n < 13 = 13-n | otherwise = 1 -}