-- -- (c) Susumu Katayama 2009 -- ProgramGenerator.lhs; split from MemoDeb.lhs DeBruijn.lhs; FMTypeDeb (FMTypeDSをいじったもの)から，FMTypeをやめてavailを全部listにしたもの． revision1.36から，FIXとOLD/FILTRECを削除． FMTypeDS.lhs FMType.lhsでPASSRENAMER2なやつを出発点とする． revision 1.1（FMType.lhsをPASSRENAMER2に限定したのと同じ）をcommitするときにコメントで「テストしていない」と書いたが，直後にテストした． FMType.lhs revision 1.41くらいから大幅にsimplifyした．特に，Memoizationを止めた． 以前のはFMType.withMemoTrie.lhsに残しておく． Memoizationをやってたおそらく最後の動く奴にはlastMemoTrieというタグを打ってある． \begin{code} {-# OPTIONS -fglasgow-exts -cpp #-} module MagicHaskeller.ProgramGenerator where import MagicHaskeller.Types import MagicHaskeller.TyConLib import Control.Monad import Data.Monoid import MagicHaskeller.CoreLang import Control.Monad.Search.Combinatorial import MagicHaskeller.PriorSubsts import Data.List(partition, sortBy) import Data.Ix(inRange) import System.Random(mkStdGen) import MagicHaskeller.Instantiate import MagicHaskeller.Expression import MagicHaskeller.T10 import qualified Data.Map as Map import Debug.Trace import Data.Monoid import System.Random import MagicHaskeller.MyDynamic import MagicHaskeller.Execute(unsafeExecute) -- replacement of LISTENER. Now replaced further with |guess| -- listen = False type Prim = (Int, Type, Int, Typed [CoreExpr]) -- | ProgramGenerator is a generalization of the old @Memo@ type. class ProgramGenerator a where -- | |mkTrie| creates the generator with the default parameters. mkTrie :: Common -> [Typed [CoreExpr]] -> a mkTrie cmn t = mkTrieOpt cmn t t mkTrieOpt :: Common -> [Typed [CoreExpr]] -> [Typed [CoreExpr]] -> a mkTrieOpt cmn _ t = mkTrie cmn t -- error "This program generator does not take an optional primitive set." matchingPrograms, unifyingPrograms :: Search m => Type -> (Int,a) -> m AnnExpr matchingPrograms ty memodeb = unifyingPrograms (quantify ty) memodeb extractCommon :: a -> Common extractTCL :: ProgramGenerator a => a -> TyConLib extractTCL = tcl . extractCommon extractVL :: ProgramGenerator a => a -> VarLib extractVL = vl . extractCommon extractRTrie :: ProgramGenerator a => a -> RTrie extractRTrie = rt . extractCommon reducer :: ProgramGenerator a => a -> CoreExpr -> Dynamic reducer pg = execute (opt $ extractCommon pg) (extractVL pg) data Common = Cmn {opt :: Opt (), tcl :: TyConLib, vl :: VarLib, rt :: RTrie} -- | options that limit the hypothesis space. data Opt a = Opt{ 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. , execute :: VarLib -> CoreExpr -> Dynamic -- timeout はこの中でやるべき．IO Dynamicの場合にunsafePerformIOを2回やると変なことになりそうなので． , 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. , 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. , 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.) , 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. , 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. , tv0 :: Bool , stdgen :: StdGen -- ^ The random seed. , nrands :: [Int] -- ^ number of random samples at each depth, for each type. } -- | default options -- -- > options = Opt{ primopt = Nothing -- > , execute = unsafeExecute -- > , timeout = Just 20000 -- > , guess = False -- > , contain = True -- > , constrL = False -- > , tv1 = False -- > , stdgen = mkStdGen 123456 -- > , nrands = repeat 5 -- > } options :: Opt a options = Opt{ primopt = Nothing , execute = unsafeExecute , timeout = Just 20000 , guess = False , contain = True , constrL = False , tv1 = False , tv0 = False , stdgen = mkStdGen 123456 , nrands = nrnds } -- reducer (opt,_,_,_,_) = execute opt nrnds = map fnrnds [0..] chopRnds :: [[a]] -> [[a]] chopRnds = zipWith take nrnds {- fnrnds n | n <= 5 = 5 | n < 10 = 10-n | otherwise = 1 -} fnrnds _ = 5 {- fnrnds n | n < 13 = 13-n | otherwise = 1 -} retsTVar (_, TV tv, _, _) = True retsTVar _ = False splitPrims :: [Typed [CoreExpr]] -> ([Prim],[Prim]) splitPrims = partition retsTVar . map (\ tx@(_:::t) -> (getArity t, getRet t, maxVarID t + 1, tx)) . mergesortWithBy (\(x:::t) (y:::_) -> (x++y):::t) (\(_:::t) (_:::u) -> compare t u) applyDo :: Monad m => ([Type] -> Type -> PriorSubsts m a) -> [Type] -> Type -> PriorSubsts m a applyDo fun avail ty = do subst <- getSubst fun (map (apply subst) avail) (apply subst ty) wind :: (a->a) -> ([Type] -> Type -> a) -> [Type] -> Type -> a wind g f avail (t0 :-> t1) = g $ wind g f (t0 : avail) t1 wind _ f avail reqret = f avail reqret wind_ :: ([Type] -> Type -> a) -> [Type] -> Type -> a wind_ = wind id {-# SPECIALIZE fromAssumptions :: (Search m, ProgramGenerator pg) => pg -> Int -> (Type -> PriorSubsts m [CoreExpr]) -> (Type -> Type -> PriorSubsts m ()) -> Type -> [Type] -> PriorSubsts m [CoreExpr] #-} fromAssumptions :: (Search m, Expression e, ProgramGenerator pg) => pg -> Int -> (Type -> PriorSubsts m [e]) -> (Type -> Type -> PriorSubsts m ()) -> Type -> [Type] -> PriorSubsts m [e] fromAssumptions pg lenavails behalf mps reqret avail = msum $ map (retMono pg lenavails behalf (flip mps reqret)) (fromAvail avail) retMono :: (Search m, Expression e, ProgramGenerator pg) => pg -> Int -> (Type -> PriorSubsts m [e]) -> (Type -> PriorSubsts m ()) -> ([CoreExpr], (Int,[Type],Type)) -> PriorSubsts m [e] retMono pg lenavails behalf tok fromBlah = do let (es, (arity,args,retty)) = fromBlah tok retty convertPS (ndelay arity) $ fap behalf args (map (fromCE (reducer pg) lenavails arity) es) fromAvail :: [Type] -> [([CoreExpr], (Int,[Type],Type))] fromAvail = zipWith (\ n t -> ([X n], revSplitArgs t)) [0..] -- ConstrLではmatchではダメ．理由はDec. 2, 2007のnotesを参照． mguAssumptions :: (MonadPlus m) => Type -> [Type] -> PriorSubsts m [CoreExpr] mguAssumptions patty assumptions = applyDo mguAssumptions' assumptions patty mguAssumptions' assumptions patty = msum $ zipWith (\n t -> mguPS patty t >> return [X n]) [0..] assumptions {-# SPECIALIZE matchAssumptions :: (MonadPlus m, ProgramGenerator pg) => pg -> Int -> Type -> [Type] -> PriorSubsts m [CoreExpr] #-} matchAssumptions :: (MonadPlus m, Expression e, ProgramGenerator pg) => pg -> Int -> Type -> [Type] -> PriorSubsts m [e] matchAssumptions pg lenavails reqty assumptions = do s <- getSubst let newty = apply s reqty msum $ zipWith (\n t -> matchPS newty t >> return [fromCE (reducer pg) lenavails (getArity newty) (X n)]) [0..] assumptions -- match の場合，通常はreqtyの方だけapply substすればよい． -- not sure if this is more efficient than doing mguAssumptions and returning (). mguAssumptions_ :: (MonadPlus m) => Type -> [Type] -> PriorSubsts m () mguAssumptions_ patty assumptions = applyDo mguAssumptions_' assumptions patty mguAssumptions_' assumptions patty = msum $ map (mguPS patty) assumptions {-# SPECIALIZE retPrimMono :: (Search m, ProgramGenerator pg) => pg -> Int -> (Type -> PriorSubsts m [CoreExpr]) -> (Type -> PriorSubsts m [CoreExpr]) -> (Type -> Type -> PriorSubsts m ()) -> Type -> Prim -> PriorSubsts m [CoreExpr] #-} retPrimMono :: (Search m, Expression e, ProgramGenerator pg) => pg -> Int -> (Type -> PriorSubsts m [e]) -> (Type -> PriorSubsts m [e]) -> (Type -> Type -> PriorSubsts m ()) -> Type -> Prim -> PriorSubsts m [e] retPrimMono pg lenavails lltbehalf behalf mps reqret (arity, retty, numtvs, xs:::ty) = do tvid <- reserveTVars numtvs mps (mapTV (tvid+) retty) reqret convertPS (ndelay arity) $ funApSub lltbehalf behalf (mapTV (tvid+) ty) (map (fromCE (reducer pg) lenavails arity) xs) funApSub :: (Search m, Expression e) => (Type -> PriorSubsts m [e]) -> (Type -> PriorSubsts m [e]) -> Type -> [e] -> PriorSubsts m [e] funApSub = funApSubOp (<$>) funApSubOp op lltbehalf behalf (t:> ts) funs = do args <- lltbehalf t funApSubOp op lltbehalf behalf ts (liftM2 op funs args) -- original. funApSubOp op lltbehalf behalf (t:->ts) funs = do args <- behalf t funApSubOp op lltbehalf behalf ts (liftM2 op funs args) funApSubOp _ _ _ _ funs = return funs -- originalでrevGetArgs経由にすると，foldMを使った場合と同じ効率になる． {- funApSub behalf t funs = fap behalf (revGetArgs t) funs revGetArgs (t:->u) = t : revGetArgs u revGetArgs _ = [] -} {- fap behalf (t:ts) funs = do args <- behalf t fap behalf ts (liftM2 (<$>) funs args) fap _ _ funs = return funs -} {- mapMを使う 一番遅い． fap behalf ts funs = do args <- mapM behalf ts return (foldl (liftM2 (<$>)) funs args) -} -- foldMを使う．なぜかこれが一番速い fap behalf ts funs = foldM (\fs t -> do args <- behalf t return $ liftM2 (<$>) fs args) funs ts -- fap behalf ts funs = mapAndFoldM (liftM2 (<$>)) funs behalf ts mapAndFoldM op n f [] = return n mapAndFoldM op n f (x:xs) = do y <- f x mapAndFoldM op (n `op` y) f xs {-# SPECIALIZE retGen :: (Search m, ProgramGenerator pg) => pg -> Int -> (Type -> Type -> [CoreExpr] -> [CoreExpr]) -> (Type -> PriorSubsts m [CoreExpr]) -> (Type -> PriorSubsts m [CoreExpr]) -> Type -> Prim -> PriorSubsts m [CoreExpr] #-} retGen, retGenOrd, retGenTV1 :: (Search m, Expression e, ProgramGenerator pg) => pg -> Int -> (Type -> Type -> [e] -> [e]) -> (Type -> PriorSubsts m [e]) -> (Type -> PriorSubsts m [e]) -> Type -> Prim -> PriorSubsts m [e] retGen pg lenavails fe lltbehalf behalf = retGen' (funApSub lltbehalf behalf) pg lenavails fe lltbehalf behalf retGen' fas pg lenavails fe lltbehalf behalf reqret (arity, _retty, numtvs, xs:::ty) = convertPS (ndelay arity) $ do tvid <- reserveTVars numtvs -- この（最初の）IDそのもの（つまり返り値のtvID）はすぐに使われなくなる -- let typ = apply (unitSubst tvid reqret) (mapTV (tvid+) ty) -- mapTVとapplyはhylo-fusionできるはずだが，勝手にされる？ -- -- unitSubstをinlineにしないと駄目か a <- mkSubsts tvid reqret exprs <- funApSub lltbehalf behalf (mapTV (tvid+) ty) (map (fromCE (reducer pg) lenavails (arity+a)) xs) gentvar <- applyPS (TV tvid) guard (orderedAndUsedArgs gentvar) -- この辺のcheckをTVnに入る前の早い段階にやるのは1つの考え方だが，TVn中にreplaceされたりはしないのか? fas gentvar (fe gentvar ty exprs) -- retGenOrd can be used instead of retGen, when not reorganizing. retGenOrd pg lenavails fe lltbehalf behalf = retGen' (funApSub'' False) pg lenavails fe lltbehalf behalf where -- funApSub'' filtexp (TV _ :-> _) funs = mzero -- mkSubstsで導入されたtyvarsが使われていないケース．replaceされた結果TVってケースはとりあえず無視.... funApSub'' filtexp (t:->ts@(u:->_)) funs -- | t > u = mzero | otherwise = do args <- behalf t funApSub'' (t==u) ts (if filtexp then [ f <$> e | f <- funs, e <- args, let _:$d = toCE f, d <= toCE e ] else liftM2 (<$>) funs args) -- てゆーかtとuが同じならばもっといろんなことができそう． funApSub'' filtexp (t:->ts) funs = do args <- behalf t return (if filtexp then [ f <$> e | f <- funs, e <- args, let _:$d = toCE f, d <= toCE e] else liftM2 (<$>) funs args) funApSub'' _fe _t funs = return funs orderedAndUsedArgs (TV _ :-> _) = False -- mkSubstsで導入されたtyvarsが使われていないケース．replaceされた結果TVってケースはとりあえず無視.... orderedAndUsedArgs (t:->ts@(u:->_)) | t > u = False | otherwise = orderedAndUsedArgs ts orderedAndUsedArgs _ = True usedArg n (TV m :-> _) = n /= m usedArg _ _ = True retGenTV1 pg lenavails fe lltbehalf behalf reqret (arity, _retty, numtvs, xs:::ty) = convertPS (ndelay arity) $ do tvid <- reserveTVars numtvs -- この（最初の）IDそのもの（つまり返り値のtvID）はすぐに使われなくなる -- let typ = apply (unitSubst tvid reqret) (mapTV (tvid+) ty) -- mapTVとapplyはhylo-fusionできるはずだが，勝手にされる？ -- -- unitSubstをinlineにしないと駄目か a <- mkSubst tvid reqret exprs <- funApSub lltbehalf behalf (mapTV (tvid+) ty) (map (fromCE (reducer pg) lenavails (arity+a)) xs) gentvar <- applyPS (TV tvid) guard (usedArg (tvid+1) gentvar) funApSub lltbehalf behalf gentvar (fe gentvar ty exprs) retGenTV0 pg lenavails fe lltbehalf behalf reqret (arity, _retty, numtvs, xs:::ty) = convertPS (ndelay arity) $ do tvid <- reserveTVars numtvs -- この（最初の）IDそのもの（つまり返り値のtvID）はすぐに使われなくなる -- let typ = apply (unitSubst tvid reqret) (mapTV (tvid+) ty) -- mapTVとapplyはhylo-fusionできるはずだが，勝手にされる？ -- -- unitSubstをinlineにしないと駄目か updatePS (unitSubst tvid reqret) exprs <- funApSub lltbehalf behalf (mapTV (tvid+) ty) (map (fromCE (reducer pg) lenavails arity) xs) gentvar <- applyPS (TV tvid) return $ fe gentvar ty exprs -- LISTENERかDESTRUCTIVEがdefineされているときの，各ケースのoptimization filterExprs :: Expression e => Type -> Type -> [e] -> [e] filterExprs gentvar ty = filter (cond . getArgExprs . toCE) where cond es = case gentvar of _:->_ -> not (retSameVal ty es) && not (includesStrictArg es) && anyRec ty es && not (constEq ty es) _ -> not (retSameVal ty es) && not (includesStrictArg es) getArgExprs e = gae e [] gae (f:$e) es = gae f (e:es) gae _ es = es -- forall w x y. list_para w (\_ -> x) (\c d e f -> e (blah)) = \_ -> x 的なもの. constEq (t:->u) (e@(Lambda d):es) | returnsAtoA t = recHead t e && constEq u es | otherwise = not (isUsed 0 d) && ceq e u es constEq (t:->u) (_:_) = False -- not case/cata/para, so should pass. constEq (_:> u) (_ :es) = constEq u es constEq _ [] = True ceq d (t:->u) (e@(Lambda _):es) | returnsAtoA t = recHead t e && ceq d u es | otherwise = d == e && ceq d u es ceq d (t:->u) (_:_) = False -- not case/cata/para, so should pass. ceq d (_:> u) (_ :es) = ceq d u es ceq _ _ [] = True recHead (t:->u@(_:->_)) (Lambda e) = recHead u e recHead (TV tv0 :-> TV tv1) (Lambda (Lambda (X 1 :$ _))) = tv0 == 0 && tv1 == 0 -- 複数recがある場合，最後の奴だけrecとして認めることになっちゃうので，最適化の意味ではちょっとだけザル recHead _u _e = False -- windUntilRecってのがあれば共有可能 (CPSな感じ) retSameVal (_:>u) (_:es) = retSameVal u es retSameVal (t:->u) (e:es) = (returnsId t e && rsv u es) || rsv' (retVal t e) u es retSameVal _ _ = False rsv (_:>u) (_:es) = rsv u es rsv (t:->u) (e:es) = (returnsId t e && rsv u es) || rsv' (retVal t e) u es rsv _ _ = True rsv' rve (_:>u) (_:es) = rsv' rve u es rsv' rve (t:->u) (e:es) = (returnsId t e || retVal t e == rve) && rsv' rve u es rsv' _ _ _ = True \end{code} typeをひっくり返す場合 {- -- :>なargumentをdropするのを忘れてた． -- :>を再び実装する時は，CoreExprの方のspineのlistを持つ．で，:>の場所をskipする． -- あと，返り値が関数にunifyすることもあるので，必ず引数ではなく型の方を数えること ... てゆーかそれだったら後ろから数えちゃダメじゃん． これは結構ややこしい話だが， ・returnsIdに関しては，replaceする前の型のarityで数えてidを返す場合しか当てはまらない． ・retValに関しては，いっちゃん最後が等しければOK．とはいえ， - returnsIdが交じっていれば，結局replaceする前の型のarityで数えることになるだろう，また， - returnsIdが交じっていない，つまりrecursionがない場合は，そもそもcase expansionでfilter outされる（予定） というわけで，実際にはどちらのケースでもreplaceする前の型のarityで数えればよい．つまり前から数えろってことやね． てゆーか，前から数えるとかいうのは各argumentの話． -} {- 上記の理由から，これは間違い． retSameVal (hd:tl@(_:_)) (f:$e) = -- trace ("t = "++show t ++ ", and f:$e = " ++ show (f:$e)) $ (returnsId hd e && returnsAtoA hd && retSameVal tl f) || retSameVal' rve tl f where rve = retVal e retSameVal _ _ = True retSameVal' e (hd:tl@(_:_)) (f:$d) = ((returnsId hd d && returnsAtoA hd) || rvd==e) && retSameVal' e tl f -- retSameVal' e t (f:$d) = (d == X 0 && returnsAtoA (head t) && retSameVal' e tailt f) || (d==e) && retSameVal' e tailt f where rvd = retVal d retSameVal' _ _ _ = True -} retSameVal (hd:tl@(_:_)) (f:$e) = -- trace ("t = "++show t ++ ", and f:$e = " ++ show (f:$e)) $ (returnsId hd e && retSameVal tl f) || retSameVal' (retVal hd e) tl f retSameVal _ _ = True retSameVal' rve (hd:tl@(_:_)) (f:$d) = (returnsId hd d || retVal hd d == rve) && retSameVal' rve tl f retSameVal' _ _ _ = True \begin{code} -- returnsAtoA is True when the type returns a->a, where the tvID of a is 0. returnsAtoA (TV tv0 :-> TV tv1) = tv0 == 0 && tv1 == 0 returnsAtoA (t :-> u) = returnsAtoA u returnsAtoA _ = False -- 同時にreturnsAtoAもチェックしてるのもポイント． returnsId (t:->u@(_:->_)) (Lambda e) = returnsId u e returnsId (TV tv0 :-> TV tv1) e = tv0 == 0 && tv1 == 0 && isId e returnsId _u _e = False -- ここで(_u,_e)が(TV _, Lambda _)ってこともあり得る．_uがt:->uなのに_eがLambdaでないってのはありえないか． {- これだと，結果として最後の引数と返り値の型が同じだけどもともとのPrim上では違う，という可能性があり得る． returnsId (t:->u) (Lambda e) = returnsId u e returnsId (_:->_) _ = error "returnsId: impossible" returnsId (TV tv) (X 0) = tvID tv == 0 returnsId _u _e = False -- ここで(_u,_e)が(TV _, Lambda _)ってこともあり得る．_uがt:->uなのに_eがLambdaでないってのはありえないか． -} -- isId checks if the argument is eta-equivalent to id, i.e. (Lambda (X 0)). Note that expressions are eta-expanded. -- for example, isId (Lambda (Lambda (Lambda ((X 2 :$ X 1) :$ X 0)))) is True. -- There is no need to tell that isId (Lambda ((Lambda (X 0)) :$ X 0)) is True, because this beta-reducible expression would not be synthesized. isId e = isId' 0 e isId' n (Lambda e) = isId' (n+1) e isId' n e = isId'' n 0 e isId'' n m (e :$ X i) = i==m && isId'' n (m+1) e isId'' n m (X i) = i==m && n == m+1 isId'' _ _ _ = False retVal t e = rv t 0 e rv (_:->t) n (Lambda e) = rv t (n+1) e rv (_:->_) _ _ = error "rv: impossible" rv _ n e = mapsub n e -- mapsub n ~= gmap (subtract n), but I will have to rewrite the definition of CoreExpr to prevent gmap from updating other Ints. mapsub n (X m) = X (m-n) mapsub n (a :$ b) = mapsub n a :$ mapsub n b mapsub n (Lambda e) = Lambda (mapsub n e) mapsub n e = e isClosed = isClosed' 0 isClosed' dep (X n) = n < dep isClosed' dep (Lambda e) = isClosed' (dep+1) e isClosed' dep (f :$ e) = isClosed' dep f && isClosed' dep e isClosed' _ _ = True -- 効率のことを考えると，strictArgは最初に持ってくることになる．（将来的には，最初になるように並べ変えてgenerateし，終ってから元に戻すことになる） -- （少なくとも，最初にexpandする．制限が多いので分岐しにくいから．） includesStrictArg (X n : es) = any (isUsed n) es -- caseのデータなのでLambdaは来ない．あと，Quantifyは最初からexcludeされている．というわけで，ここには実際には((_:$_):_)か[]しか来ない． -- 関数適用の場合はめんどくさいしチェックもコストがかかるので素通しにする． includesStrictArg _ = False {- includesStrictArg [] = False includesStrictArg es = case last es of X n -> any (isUsed n) (init es) _:$_ -> False -- 関数適用の場合はめんどくさいしチェックもコストがかかるので素通しにする． -- caseのデータなのでLambdaは来ない．あと，Quantifyは最初からexcludeされている． -} anyRec (_:>t) (_:es) = anyRec t es anyRec (t:->u) (e:es) = -- trace ("ar: t = "++show t++" and u = "++ show u) $ recursive t e || anyRec u es anyRec (_:->_) _ = error "hoge" anyRec _ [] = False {- typeの方をひっくり返す場合 anyRec (hd:tl@(_:_)) (f:$e) = recursive hd e || anyRec tl f anyRec _ _ = False -} recursive (t:->u@(_:->_)) (Lambda e) = recursive u e recursive (TV tv0 :-> TV tv1) (Lambda e) = tv0 == 0 && tv1 == 0 && isUsed 0 e && not (constRec 0 e) -- これだと，recursiveのやつとnot const.recのやつが同じでなくてはならないが，その条件は必要か？ （listでやっている限りは気にしなくていいって話もあるけど） recursive _ _ = False constRec dep (Lambda e) = constRec (dep+1) e constRec dep (X n :$ e) | n == dep = not (belowIsUsed n e) constRec _ _ = False belowIsUsed dep (X n) = dep > n belowIsUsed dep (Lambda e) = belowIsUsed (dep+1) e belowIsUsed dep (f :$ e) = belowIsUsed dep f || belowIsUsed dep e belowIsUsed _ _ = False {- lastarg (_:->t@(_:->_)) = let Just (la,n) = lastarg t in Just (la, n+1) lastarg (t:->_) = Just (t, 1) lastarg _ = Nothing isRec n expr = isUsed (-n) expr -} isUsed dep (X n) = dep==n isUsed dep (Lambda e) = isUsed (dep+1) e isUsed dep (f :$ e) = isUsed dep f || isUsed dep e isUsed _ _ = False mkSubsts :: Search m => Int -> Type -> PriorSubsts m Int mkSubsts tvid reqret = base `mplus` delayPS recurse where base = do updatePS (unitSubst tvid reqret) -- ここをsetSubstにして，mguProgsを呼び出すたびに結果のSubstをplusSubstするようにした方が，無駄にSubstが大きくならない． -- めんどくさいからこうしてるけど，もしlookupSubstが時間を食い過ぎるなら考える． return 0 recurse = do v <- newTVar arity <- mkSubsts tvid (TV v :-> reqret) return (arity+1) mkSubst :: Search m => Int -> Type -> PriorSubsts m Int mkSubst tvid reqret = base `mplus` delayPS first where base = do updatePS (unitSubst tvid reqret) -- ここをsetSubstにして，mguProgsを呼び出すたびに結果のSubstをplusSubstするようにした方が，無駄にSubstが大きくならない． -- めんどくさいからこうしてるけど，もしlookupSubstが時間を食い過ぎるなら考える． return 0 first = do v <- newTVar updatePS (unitSubst tvid (TV v :-> reqret)) return 1 mkRetty t = (getRet t, t) -- getRet (t0:->t1) = getRet t1 -- getRet t = t -- MemoStingyとかでは -- reorganize_ :: ([Type] -> PriorSubsts BF ()) -> [Type] -> PriorSubsts BF () -- として使われるのだが，G4ipでは下記の型じゃないと． reorganizer_ :: ([Type] -> a) -> [Type] -> a reorganizer_ fun avail = fun $ uniqSort avail -- moved from T10.hs to make T10 independent of Types -- hit decides whether to memoize or not. hit :: Type -> [Type] -> Bool -- hit ty tys = True -- always memo -- hit ty tys = areMono (ty:tys) -- memo only tycons ... Substいらないし，availsToReplacerなしで（newavailなしで）判定できる．あとそもそも，MapTypeにtvやevalがいらないし，encode/decodeもいらなくなる．ただ，monomorphicしからやないのって，ちょっと少な過ぎる気もする． -- hit ty tys = sum (map size (ty:tys)) < 7 -- hit ty tys = sum (map size (ty:tys)) < 2 -- hit ty tys = sum (map size (ty:tys)) < 5 -- hit ty tys = sum (map size (ty:tys)) < 12 hit ty tys = sum (map size (ty:tys)) < 10 areMono = all (null.tyvars) \end{code}