MagicHaskeller 0.8.6.1 → 0.8.6.2
raw patch · 28 files changed
+431/−507 lines, 28 files
Files
- Control/Monad/Search/Best.hs +53/−0
- Control/Monad/Search/Combinatorial.lhs +1/−1
- ExperimIOP.hs +151/−13
- MagicHaskeller.cabal +7/−6
- MagicHaskeller.lhs +2/−21
- MagicHaskeller/Analytical.hs +17/−8
- MagicHaskeller/Analytical/FMExpr.hs +11/−2
- MagicHaskeller/Analytical/Parser.hs +11/−9
- MagicHaskeller/Analytical/Syntax.hs +1/−1
- MagicHaskeller/Analytical/Synthesize.hs +51/−22
- MagicHaskeller/Classify.hs +3/−2
- MagicHaskeller/ClassifyDM.hs +2/−2
- MagicHaskeller/CoreLang.lhs +20/−11
- MagicHaskeller/DebMT.lhs +1/−2
- MagicHaskeller/ExecuteAPI610.hs +3/−3
- MagicHaskeller/Instantiate.hs +4/−2
- MagicHaskeller/LibTH.hs +7/−7
- MagicHaskeller/MHTH.lhs +6/−2
- MagicHaskeller/Options.hs +10/−1
- MagicHaskeller/PriorSubsts.lhs +4/−0
- MagicHaskeller/ProgGenSF.lhs +5/−7
- MagicHaskeller/ProgGenXF.lhs +0/−322
- MagicHaskeller/ProgramGenerator.lhs +8/−3
- MagicHaskeller/ReadDynamic.hs +13/−9
- MagicHaskeller/RunAnalytical.hs +20/−11
- MagicHaskeller/TimeOut.hs +9/−5
- MagicHaskeller/TyConLib.hs +0/−23
- MagicHaskeller/Types.lhs +11/−12
+ Control/Monad/Search/Best.hs view
@@ -0,0 +1,53 @@+-- +-- (c) Susumu Katayama+--++-- best¤Î¤ä¤Ä¤À¤±keep¤¹¤ë¤ä¤Ä¡¥analytical¤ËŬÍѤ¹¤ë¤ÈIgorII¤ÈƱ¤¸¤Ë¤Ê¤ë¤·¡¤exhaustive¤ËŬÍѤ¹¤ë¤ÈDjinn¤ß¤¿¤¤¤Ê´¶¤¸¤Ë¤Ê¤ë¡¥+{-# LANGUAGE MultiParamTypeClasses #-}+module Control.Monad.Search.Best where+import Control.Monad+import Control.Monad.Search.Combinatorial++-- | Unlike 'Matrix', 'Recomp', etc., the 'Best' monad only keeps the best set of results.+-- This makes the analytical synthesis like IgorII, and the exhaustive synthesis like Djinn,+-- i.e., the resulting algorithms are more efficient, but cannot be used for (analytically-)generate-and-test.+data Best a = Result [a] | Delay (Best a) deriving (Show, Read)++-- Note that getBests zero = _|_+getBests :: Best a -> [a]+getBests (Result xs) = xs+getBests (Delay b) = getBests b++zero = Delay zero++instance Functor Best where+ fmap f (Result xs) = Result $ map f xs+ fmap f (Delay b) = Delay $ fmap f b+instance Monad Best where+ return x = Result [x]+ Result xs >>= f = msum $ map f xs+ Delay b >>= f = Delay $ b >>= f+instance MonadPlus Best where+ mzero = zero+ Result xs `mplus` Result ys = Result $ xs++ys+ b@(Result _) `mplus` Delay _ = b+ Delay _ `mplus` b@(Result _) = b+ Delay b `mplus` Delay c = Delay $ b `mplus` c+instance Delay Best where+ delay = Delay++instance Search Best where+ fromRc = fromMx . toMx+ toRc = toRc . toMx+ fromMx (Mx xss) = fromLists xss+ toMx (Result xs) = Mx $ xs : unMx mzero+ toMx (Delay b) = let Mx xss = toMx b in Mx $ []:xss+ fromDF = Result++fromLists :: [[a]] -> Best a+fromLists ([]:xss) = Delay (fromLists xss)+fromLists (xs:_) = Result xs++instance Memoable Best Best where+ tabulate = id+ applyMemo = id
Control/Monad/Search/Combinatorial.lhs view
@@ -171,7 +171,7 @@ zipDepthRc :: (Int -> Bag a -> Bag b) -> Recomp a -> Recomp b zipDepthRc f (Rc g) = Rc (\d -> f d (g d)) --- $B8+3]$1>e$N?<$5$r;H$&<BAu(B+-- $B8+3]$1>e$N?<$5$r;H$&<BAu(B NB: This is confusing. zipDepthDB :: (Int -> Bag (a,Int) -> Bag (b,Int)) -> DBound a -> DBound b zipDepthDB f (DB g) = DB (\d -> f d (g d))
ExperimIOP.hs view
@@ -2,7 +2,7 @@ -- (C) Susumu Katayama -- -- (Typed)IOPairs¾å¤Ç¥Ç¡¼¥¿¤ò¤È¤ë¡¥ghci¾å¤Ç :cmd ¤ò»È¤¤¤Þ¤¯¤ë´¶¤¸¡¥-{-# LANGUAGE RankNTypes, CPP #-}+{-# LANGUAGE RankNTypes, CPP, TemplateHaskell #-} module ExperimIOP(module ExperimIOP, module MagicHaskeller.RunAnalytical) where import MagicHaskeller.Analytical@@ -78,7 +78,7 @@ ++ filtGetOne "eq9" "eqPred" ++ filtGetOne "evenpos7" "evenposPred" -- ++ filtGetOne "evens21" "(\\evens -> evens [4,6,9,2,3,8,8] == [4,6,2,8,8])"--- ++ filtGetOne "fib6" "(\\fib -> fib 1 == 1 && fib 2 == 1 && fib 4 == 3 && fib 6 == 8 && fib 8 == 21)"+-- ++ filtGetOneBK "fib6" "add''" "(\\fib -> fib 1 == 1 && fib 2 == 1 && fib 4 == 3 && fib 6 == 8 && fib 8 == 21)" ++ filtGetOne "iniT" "initPred" ++ filtGetOne "oddpos6" "oddposPred" ++ filtGetOne "lasT" "lastPred"@@ -129,6 +129,7 @@ add'2 = [d| f :: Int->Int->Int; f 0 x = x; f x 0 = x |] -- dame ¤É¤¦¤âoverlap¤·¤Æ¤¤¤ë¤Î¤¬¤Þ¤º¤¤¤Î¤Ç¤Ï? ¼«Æ°Åª¤Ëcaseʬ¤±¤¹¤ë¤è¤¦¤Ë¤¹¤ì¤Ð¤è¤¤¡¥ add'1 = [d| f :: Int->Int->Int; f 0 x = x |] add'' = [d| f :: Int->Int->Int; f 0 x = x; f 1 0 = 1; f 2 0 = 2; f 1 1 = 2; f 1 2 = 3; f 2 1 = 3; f 2 2 = 4; f 2 3 = 5 |]+add'''= [d| f :: Int->Int->Int; f 0 0 = 0; f 0 1 = 1; f 0 2 = 2; f 1 0 = 1; f 2 0 = 2; f 1 1 = 2; f 1 2 = 3; f 2 1 = 3; f 2 2 = 4; f 2 3 = 5 |] addArgss = ["3 5"] -- :cmd run $ filtGetOne "addN" "longAddNPred"@@ -298,6 +299,13 @@ appenD [a,b,c,d][e] = [a,b,c,d,e] appenD [a,b,c,d,e][] = [a,b,c,d,e] |] -- ¤¤¤±¤ë+{-+take 2: 0+take 4: 0+take 7: 0+take 11:0.39+take 16: >300+-} appendPred (++) = "foo" ++ "bar" == "foobar" -- :cmd run $ filtGetOne "concat12" "(\\concat -> concat [\"abc\",\"\",\"de\",\"fghi\"] == \"abcdefghi\")" concat12 = [d|@@ -340,7 +348,8 @@ allOddArgss = ["[3,1,5]", "[1,3,2]"] -- ¤³¤Ã¤Á¤¬tuned-drop12 = [d| droP :: Int -> [a] -> [a]+tunedDrop12 = [d| + droP :: Int -> [a] -> [a] droP 0 [] = [] droP 0 [a] = [a] droP 0 [a,b] = [a,b]@@ -353,11 +362,35 @@ droP 2 [a] = [] droP 2 [a,b] = [] droP 2 [a,b,c] = [c]- --droP (S (S 1)) [] = []- --droP (S (S 1)) [a] = []- --droP (S (S 1)) [a,b] = []- --droP (S (S 1)) [a,b,c] = []- |] -- ¤¤¤±¤ë¡¥+ |] -- 0.20sec+tunedDrop9 = [d|+ droP :: Int -> [a] -> [a]+ droP 0 [] = []+ droP 0 [a] = [a]+ droP 0 [a,b] = [a,b]+ droP 1 [] = []+ droP 1 [a] = []+ droP 1 [a,b] = [b]+ droP 2 [] = []+ droP 2 [a] = []+ droP 2 [a,b] = []+ |] -- 0.08sec+tunedDrop6 = [d|+ droP :: Int -> [a] -> [a]+ droP 0 [] = []+ droP 0 [a] = [a]+ droP 0 [a,b] = [a,b]+ droP 1 [] = []+ droP 1 [a] = []+ droP 1 [a,b] = [b]+ |] -- 0.07sec+tunedDrop4 = [d|+ droP :: Int -> [a] -> [a]+ droP 0 [] = []+ droP 0 [a] = [a]+ droP 1 [] = []+ droP 1 [a] = []+ |] -- 0.10 sec -- :cmd run $ filtGetOne "drop'9" "dropPred" drop'9 = [d| droP :: Int -> [a] -> [a] droP 0 x = x@@ -389,6 +422,15 @@ even6 = [d| f :: Int -> Bool; f 0 = True; f 1 = False; f 2 = True; f 3 = False; f 4 = True; f 5 = False |] evenArgss = ["8", "9"] +tunedEvenpos n = fmap (takeFunD n) evenpos7+{-+take 2 : >300 sec+take 3 : 0.03 sec+take 4 : 0.02 sec+take 5 : 0.01 sec+take 6 : 0.01 sec+take 7 : 0.04 sec+-} -- :cmd run $ filtGetOne "evenpos7" "evenposPred" evenpos7 = [d| evenpos :: [a] -> [a] evenpos [] = []@@ -424,7 +466,7 @@ evens [3, 1] = [] evens [3, 2] = [2] evens [3, 3] = []- |]+ |] -- >300 evens13 = [d| evens :: [Int] -> [Int] evens [] = []@@ -440,13 +482,41 @@ evens [2, 0] = [2,0] evens [2, 1] = [2] evens [2, 2] = [2,2]- |]+ |] -- >300+evens10 = [d|+ evens :: [Int] -> [Int]+ evens [] = []+ evens [0] = [0]+ evens [1] = []+ evens [2] = [2]+ evens [0,0] = [0,0]+ evens [0,1] = [0]+ evens [0,2] = [0,2]+ evens [1, 0] = [0]+ evens [1, 1] = []+ evens [1, 2] = [2]+ |] -- >300+evens7 = [d|+ evens :: [Int] -> [Int]+ evens [] = []+ evens [0] = [0]+ evens [1] = []+ evens [0,0] = [0,0]+ evens [0,1] = [0]+ evens [1, 0] = [0]+ evens [1, 1] = []+ |] -- >300 evensArgss = ["[1,2,3,4,5]"] evensPred evens = evens [4,6,9,2,3,8,8] == [4,6,2,8,8] -- :cmd run $ filtGetOne "eq9" "eqPred"-eq9 = [d| f :: Int->Int->Bool; f 0 0 = True; f 0 1 = False; f 0 2 = False; f 1 0 = False; f 1 1 = True; f 1 2 = False; f 2 0 = False; f 2 1 = False; f 2 2 = True |] -- Examples.hs¤ÈƱ¤¸¤â¤Î-eq16 = [d| f :: Int->Int->Bool; f 0 0 = True; f 0 1 = False; f 0 2 = False; f 0 3 = False; f 1 0 = False; f 1 1 = True; f 1 2 = False; f 1 3 = False; f 2 0 = False; f 2 1 = False; f 2 2 = True; f 2 3 = False; f 3 0 = False; f 3 1 = False; f 3 2 = False; f 3 3 = True |] -- dame ... too slow....+eq9 = [d| f :: Int->Int->Bool; f 0 0 = True; f 0 1 = False; f 0 2 = False; f 1 0 = False; f 1 1 = True; f 1 2 = False; f 2 0 = False; f 2 1 = False; f 2 2 = True |] -- Examples.hs¤ÈƱ¤¸¤â¤Î 0.04sec++eq6 = fmap (takeFunD 6) eq9 -- 0.07 sec+eq4 = [d| f :: Int->Int->Bool; f 0 0 = True; f 0 1 = False; f 1 0 = False; f 1 1 = True |] -- 0.08 sec+eq3 = fmap (takeFunD 3) eq4++eq16 = [d| f :: Int->Int->Bool; f 0 0 = True; f 0 1 = False; f 0 2 = False; f 0 3 = False; f 1 0 = False; f 1 1 = True; f 1 2 = False; f 1 3 = False; f 2 0 = False; f 2 1 = False; f 2 2 = True; f 2 3 = False; f 3 0 = False; f 3 1 = False; f 3 2 = False; f 3 3 = True |] -- >300 eqArgss = ["4 4", "5 7"] eqPred :: (Int->Int->Bool) -> Bool eqPred (==) = 3==3 && not (4==6) && 0==0 && not (2==0) && not (0==2) && not (3==5)@@ -497,6 +567,10 @@ fib 8 = 21 fib 9 = 34 |]++tunedFib n = fmap (takeFunD n) fib10+-- add'''¤ò»È¤¦¾ì¹ç¡¤¼ÂºÝ¤Ë¤Ïfib6¤¬¸Â³¦+ fibPred fib = fib 1 == 1 && fib 2 == 1 && fib 4 == 3 && fib 6 == 8 && fib 8 == 21 -- :cmd run $ filtGetOne "heaD" "headPred" heaD = [d|@@ -506,6 +580,7 @@ heaD [a,b,c] = a heaD [a,b,c,d] = a |]+tunedHead n = fmap (takeFunD n) heaD -- 1¤«¤é4Á´¤Æ0.01 sec headPred head = head "abcde" == 'a' -- :cmd run $ filtGetOne "incr" "incrPred" incr = [d|@@ -547,6 +622,13 @@ iniT [a,b,c] = [a,b] iniT [a,b,c,d] = [a,b,c] |] -- ¤ª¤Ê¤¸¤ä¤Ä+tunedInit n = fmap (takeFunD n) iniT+{-+take 4: 0.01 sec+take 3: 0.01 sec+take 2: 0.02 sec+take 1: >300+-} initPred init = init "foobar" == "fooba" -- taken from Examples.hs in igor2-0.7.1.3, but equivalence over Ints has to be defined in order to work with igor2, because equivalence over Ints are not defined.@@ -648,6 +730,15 @@ oddpos [a,b,c,d,e] = [a,c,e] |] oddposPred oddpos = oddpos "abcdef" == "ace" && oddpos "abc" == "ac"+{-+take 6: 0 sec+take 5: 0 sec+take 4: 0 sec+take 3: 0 sec+take 2: >300+take 1: +-}+tunedOddpos n = fmap (takeFunD n) oddpos6 -- 1¤«¤é4Á´¤Æ0.01 sec -- :cmd run $ filtGetOne "lasT" "lastPred" lasT = [d|@@ -657,6 +748,13 @@ lasT [a,b,c] = c lasT [a,b,c,d] = d |]+{-+take 4: 0.04 sec+take 3: 0.01 sec+take 2: 0.01 sec+take 1: >300+-}+tunedLast n = fmap (takeFunD n) lasT lastPred last = last "abcde" == 'e' lastM = [d|@@ -681,6 +779,14 @@ lasts [[c],[d,e],[f]] = [c,e,f] lasts [[c,d],[e,f],[g]] = [d,f,g] |]+-- not actually tuned+tunedLasts n = fmap (takeFunD n) lasts+{- +take 1: >300+take 4: 0.06+take 8: 0.10+take 10: 1.2 sec -- ÏÀʸ¤À¤È»Í¼Î¸ÞÆþ¤Ç0ÉäÀ¤±¤É¡¤¤¢¤Î»þ¤ÏbatchWriteFile¤Ç¤ä¤Ã¤¿¤Î¤Ç¥ª¡¼¥Ð¥Ø¥Ã¥É¤¬¤Ê¤«¤Ã¤¿¡¥+-} lasts' = [d| lasts :: [[a]] -> [a] lasts [] = []@@ -710,8 +816,33 @@ lengths [[],[a]] = [0,1] lengths [[],[b,a]] = [0,2] |]+tunedLens n = fmap (takeFunD n) [d|+ lengths :: [[a]] -> [Int]+ lengths [] = []+ lengths [[]] = [0]+ lengths [[a]] = [1]+ lengths [[b,a]] = [2]+ lengths [[],[]] = [0, 0]+ lengths [[],[a]] = [0,1]+ lengths [[],[b,a]] = [0,2]+ lengths [[x],[]] = [1, 0]+ lengths [[x],[a]] = [1,1]+ lengths [[x],[b,a]] = [1,2]+ lengths [[x,y],[]] = [2, 0]+ lengths [[x,y],[a]] = [2,1]+ lengths [[x,y],[b,a]] = [2,2]+ lengths [[],[],[]] = [0,0,0]+ |] lengthsPred :: ([String] -> [Int]) -> Bool lengthsPred lengths = lengths ["abcdef", "abc", "abcde"] == [6,3,5]+{-+take 4: 0.02+take 7: 0.03+take 10: 0.15 secs+take 13: 6.60 secs+take 14: 17.15 secs+-}+-- ¤·¤«¤·¡¤IgorIIH¤Ç¤³¤ì¤òÁ´Éô¥¿¥¤¥à¥¢¥¦¥È¤Þ¤Ç¤ä¤ë¤È¹Í¤¨¤ë¤Èµ¤¤¬±ó¤¯¤Ê¤ë¡¥¤¿¤È¤¨¤Ð¡¤¾åµ¤Îlengths¤ÎÎã¤Ç¤Ï¡¤Äó°Æ¼êË¡¤Ç¤¹¤Ù¤Æ¤¦¤Þ¤¯¤¤¤Ã¤Æ¤¤¤ë¤Î¤À¤«¤é¡¤1¤Ä¤ÎÎã¤ÇIgorIIH¤ËÀ¸À®¤Ç¤¤Ê¤±¤ì¤ÐÄó°Æ¼êË¡¤¬Í¥¤Ã¤Æ¤¤¤ë¤Î¤ÏÌÀÇò¤Ê¤Î¤Ç¤ä¤á¤Æ¤·¤Þ¤Ã¤Æ¤¤¤¤¤Î¤Ç¤Ï¤Ê¤«¤í¤¦¤«¡© -- :cmd run $ filtGetOne "multFst" "multFstPred" multFst = [d|@@ -724,7 +855,14 @@ --multfst [a,b,c,d,e] = [a,a,a,a,a] --multfst [a,b,c,d,e,f] = [a,a,a,a,a,a] |]+{-+take 2: >300+take 3: 0+take 4: 0+take 5: 0+-} multFstPred multfst = multfst "abcdef" == "aaaaaa"+tunedMultFst n = fmap (takeFunD n) multFst -- :cmd run $ filtGetOne "multLst" "multLstPred" multLst = [d|@@ -738,6 +876,7 @@ --multlst [a,b,c,d,e,f] = [f,f,f,f,f,f] |] multLstPred multlst = multlst "abcdef" == "ffffff"+tunedMultLst n = fmap (takeFunD n) multLst -- :cmd run $ filtGetOne "negateall" "negateAllPred" negateall = [d|@@ -845,7 +984,6 @@ sumR = [d| sum [] = 0; sum [x] = x; sum [x,y] = x+y; sum [x,y,z] = x+(y+z); sum [x,y,z,w] = x+(y+(z+w)) |] tunedSum n = fmap (takeFunD n) suM- sumPred sum = sum [7,3,8,5] == 23 -- :cmd run $ filtGetOne "swap" "swapPred"
MagicHaskeller.cabal view
@@ -1,11 +1,12 @@ Name: MagicHaskeller-Version: 0.8.6.1+Version: 0.8.6.2 Cabal-Version: >= 1.2 License: BSD3 Author: Susumu Katayama Maintainer: Susumu Katayama <skata@cs.miyazaki-u.ac.jp> Stability: experimental Homepage: http://nautilus.cs.miyazaki-u.ac.jp/~skata/MagicHaskeller.html+bug-reports: mailto:skata@cs.miyazaki-u.ac.jp Synopsis: Automatic inductive functional programmer by systematic search Build-Type: Simple Category: Language@@ -30,10 +31,10 @@ Library Build-depends: template-haskell, base >= 4 && < 5, syb, containers, array, random, directory, bytestring, mtl- Exposed-modules: MagicHaskeller, Control.Monad.Search.Combinatorial, MagicHaskeller.ProgGen, MagicHaskeller.ProgGenSF, MagicHaskeller.ProgGenXF,- MagicHaskeller.Expression, MagicHaskeller.LibTH, MagicHaskeller.Analytical, MagicHaskeller.Options- Other-modules: MagicHaskeller.MemoToFiles, MagicHaskeller.ShortString, MagicHaskeller.GetTime,- MagicHaskeller.Types, MagicHaskeller.PriorSubsts, Data.Memo, MagicHaskeller.ClassifyTr, MagicHaskeller.Classification, + Exposed-modules: MagicHaskeller, Control.Monad.Search.Combinatorial, Control.Monad.Search.Best, MagicHaskeller.ProgGen, MagicHaskeller.ProgGenSF,+ MagicHaskeller.Expression, MagicHaskeller.LibTH, MagicHaskeller.Analytical, MagicHaskeller.Options, MagicHaskeller.Classification, MagicHaskeller.GetTime+ Other-modules: MagicHaskeller.MemoToFiles, MagicHaskeller.ShortString, + MagicHaskeller.Types, MagicHaskeller.PriorSubsts, Data.Memo, MagicHaskeller.ClassifyTr, MagicHaskeller.CoreLang, MagicHaskeller.DebMT, MagicHaskeller.TyConLib, MagicHaskeller.FakeDynamic, MagicHaskeller.PolyDynamic, MagicHaskeller.ReadTypeRep, MagicHaskeller.ReadTHType, MagicHaskeller.TimeOut, MagicHaskeller.Execute, MagicHaskeller.T10,@@ -45,7 +46,7 @@ GHC-options: -O2 -fvia-C cpp-options: -DCHTO - if flag(GHCAPI)+ if flag(GHCAPI) && !os(windows) Build-depends: ghc >= 6.10, old-time, ghc-paths Exposed-modules: MagicHaskeller.RunAnalytical, MagicHaskeller.ExecuteAPI610
MagicHaskeller.lhs view
@@ -12,11 +12,6 @@ -- Please refer to their documentations on types from them --- in this documentation, types from TH are all qualified and the only type used from @module Typeable@ is Typeable.Typeable. Other types you had never seen should be our internal representation. module TH, module Typeable, -{- x ²¼¤ÎÊý¤ËThe program generators¤Ã¤Æ¤Î¤¬¤¢¤ë¤¿¤á¡¤confusing¤Ê¤Î¤Ç¡¥- -- * Program generators- ProgramGenerator, ProgGen, ProgGenSF, {- ProgGenSFIF, -} CutFree, CutFreeSF, ConstrL, ConstrLSF,--}- -- * Setting up your synthesis -- | Before synthesis, you have to define at least one program generator algorithm (or you may define one once and reuse it for later syntheses). -- Other parameters are memoization depth and time out interval, which have default values.@@ -25,7 +20,7 @@ -- ** Class for program generator algorithms -- | Please note that @ConstrL@ and @ConstrLSF@ are obsoleted and users are expected to use the 'constrL' option in 'Option'. ProgramGenerator,- ProgGen, ProgGenSF, ProgGenXF,+ ProgGen, ProgGenSF, -- ** Functions for creating your program generator algorithm -- | You can set your primitives like, e.g., @'setPrimitives' $('p' [| ( (+) :: Int->Int->Int, 0 :: Int, \'A\', [] :: [a] ) |])@,@@ -136,7 +131,7 @@ import MagicHaskeller.ProgGen(ProgGen(PG)) import MagicHaskeller.ProgGenSF(ProgGenSF, PGSF) -- import MagicHaskeller.ProgGenLF(ProgGenLF)-import MagicHaskeller.ProgGenXF(ProgGenXF)+-- import MagicHaskeller.ProgGenXF(ProgGenXF) import MagicHaskeller.ProgramGenerator import MagicHaskeller.Options(Opt(..), options) import Control.Monad.Search.Combinatorial -- This should all be exposed?@@ -293,20 +288,6 @@ where primsOpt = case primopt opt of Nothing -> prims Just po -> po --- this can be moved to somewhere near Common is defined (currently ProgramGenerator.lhs), when 'Primitive' is moved to some more adequate place.--- ¼ÂºÝProgramGenerator.lhs¤ÇPrimitive¤ò°·¤¨¤ì¤Ð¤â¤Ã¤Èñ½ã²½¤Ç¤¤ë¤Ï¤º¡¥-mkCommon :: Options -> [Primitive] -> Common-mkCommon opts prims = let- tyconlib = primitivesToTCL prims- optunit = forget opts- in Cmn {opt = optunit, tcl = tyconlib, vl = primitivesToVL tyconlib prims, rt = mkRandTrie (nrands opts) tyconlib (stdgen opts)}---- | options for limiting the hypothesis space.-type Options = Opt [Primitive]--forget :: Opt a -> Opt ()-forget opt = case primopt opt of Nothing -> opt{primopt = Nothing}- Just _ -> opt{primopt = Just ()} setPG :: ProgGen -> IO () setPG = writeIORef refmemodeb
MagicHaskeller/Analytical.hs view
@@ -11,9 +11,9 @@ -- In order to generate-and-test over the result of this module, use "MagicHaskeller.RunAnalytical". -- ** Synthesizers which can be used with any types. - get1, getMany, getManyTyped, noBK, c, SplicedPrims,+ get1, getMany, getManyM, getManyTyped, noBK, c, SplicedPrims, -- ** Synthesizers which are easier to use that can be used only with types appearing 'MagicHaskeller.CoreLang.defaultPrimitives'- getOne, synth, synthTyped+ getOne, synth, synthM, synthTyped ) where import Data.Char(ord,chr)@@ -23,6 +23,7 @@ import Language.Haskell.TH import Control.Monad.Search.Combinatorial+import Control.Monad.Search.Best import MagicHaskeller.TyConLib import MagicHaskeller.CoreLang hiding (C) import MagicHaskeller.PriorSubsts@@ -50,15 +51,21 @@ get1 :: SplicedPrims -- ^ target function definition by example -> SplicedPrims -- ^ background knowledge function definitions by example -> Exp+-- get1 target bk = head $ getBests $ getManyM target bk -- This uses Control.Monad.Search.Best. get1 target bk = head $ concat $ getMany target bk -- | getMany does what you expect from its name. getMany :: SplicedPrims -- ^ target function definition by example -> SplicedPrims -- ^ background knowledge function definitions by example -> [[Exp]]-getMany (tgt,pt) (bk,pb) = let ps = pt++pb- tcl = primitivesToTCL ps- vl = primitivesToVL tcl ps- in map (map (exprToTHExp vl)) $ unMx $ toMx (analyticSynth tcl vl tgt bk :: Strategy CoreExpr)+getMany tgt bk = unMx $ toMx (getManyM tgt bk :: Strategy Exp)+getManyM :: (Search m) =>+ SplicedPrims -- ^ target function definition by example+ -> SplicedPrims -- ^ background knowledge function definitions by example+ -> m Exp+getManyM (tgt,pt) (bk,pb) = let ps = pt++pb+ tcl = primitivesToTCL ps+ vl = primitivesToVL tcl ps+ in fmap (exprToTHExp vl) (analyticSynth tcl vl tgt bk) -- | getManyTyped is a variant of 'getMany' that generates typed expressions. -- This alone is not very useful, but the type info is required when compiling the expression and is used in "MagicHaskeller.RunAnalytical". getManyTyped :: SplicedPrims -- ^ target function definition by example@@ -99,9 +106,11 @@ -- > fa (b@(_ : d)) = succ (fa d) -- > in fa a getOne iops bk = head $ concat $ synth iops bk+-- getOne iops bk = head $ getBests $ synthM iops bk -- This uses Control.Monad.Search.Best. synth :: [Dec] -> [Dec] -> [[Exp]]-synth iops bk- = map (map (exprToTHExp defaultVarLib)) $ unMx $ toMx (analyticSynth defaultTCL defaultVarLib iops bk :: Strategy CoreExpr)+synth iops bk = unMx $ toMx (synthM iops bk :: Strategy Exp)+synthM :: Search m => [Dec] -> [Dec] -> m Exp+synthM iops bk = fmap (exprToTHExp defaultVarLib) (analyticSynth defaultTCL defaultVarLib iops bk) -- | 'synthTyped' is like synth, but adds the infered type signature to each expression. This is useful for executing the expression at runtime using GHC API. synthTyped :: [Dec] -> [Dec] -> [[Exp]]
MagicHaskeller/Analytical/FMExpr.hs view
@@ -60,7 +60,8 @@ --unifyFME = matchFME unifyFME' :: Expr -> FMExpr a -> Subst -> [(a,Subst)] unifyFME' x EmptyFME s = []-unifyFME' x@(E i) fme s = error "cannot happen for now"+-- unifyFME' (E i) fme s = error "cannot happen for now"+unifyFME' (E i) fme s = [ (x, s) | x <- valsFME fme ] -- ¤¿¤À¤·¡¤unifyFME (E _) fme¤Î¾ì¹ç¡ÊÁ´ÂΤ¬existential¤Î¾ì¹ç¡Ë¤Ï¤½¤â¤½¤âintroBK¤»¤º¤Ëundefined¤Ê°ú¿ô¤Ë¤·¤Æ¤·¤Þ¤¦¤Ù¤¡¥¤É¤¦¤»¤½¤Î°ú¿ô¤Ï»È¤ï¤ì¤Ê¤¤¤Ã¤Æ¤³¤È¤À¤«¤é¡¥ {- unifyFME' x@(E i) fme s o = case lookup i s of Nothing -> [ (x, [(i,e')] `plusSubst` s) | (e,x) <- assocsFME fme, let e' = fresh (o+) e ] -- assocsFME :: FMExpr a -> [(Expr,a)]¤À¤±¤É¡¤FMExpr¤Ë¾ðÊó¤ò»Ä¤·¤Æ¤ª¤±¤Ð̵Â̤ʷ׻»¤¬¤Ê¤¯¤Ê¤ë¤«¡¥¤Æ¤æ¡¼¤«¡¤Typed Constr¤ÎType¤ÎÉôʬ¤Î¤¿¤á¤Ë¤½¤¦¤¹¤ëɬÍפ¬¤¢¤ë¡¥ Just e -> unifyFME' e fme s o@@ -93,13 +94,21 @@ assocsFMEs EmptyFMEs = [] assocsFMEs fmes = ([], nilFMEs fmes) : [ (x:xs, v) | (x,fmes') <- assocsFME (consFMEs fmes), (xs, v) <- assocsFMEs fmes ] +-- valsFME = map snd . assocsFME+valsFME :: FMExpr a -> [a]+valsFME EmptyFME = []+valsFME fme = IntMap.elems (existentialFME fme) ++ universalFME fme+ ++ [ v | fmes <- IntMap.elems (conApFME fme), v <- valsFMEs fmes ]+valsFMEs :: FMExprs a -> [a]+valsFMEs EmptyFMEs = []+valsFMEs fmes = nilFMEs fmes : [ v | fmes' <- valsFME (consFMEs fmes), v <- valsFMEs fmes' ] -- û¤¯¤·¤¿Êª¡¥¸úΨ¤Ï³Îǧ¤·¤Æ¤Ê¤¤¡¥ matchFME :: Expr -> FMExpr a -> [(a,Subst)] matchFME x fme = matchFME' x fme emptySubst matchFME' :: Expr -> FMExpr a -> Subst -> [(a,Subst)] matchFME' x EmptyFME s = []-matchFME' x@(E i) fme s = error "cannot happen"+matchFME' (E i) fme s = [ (x, s) | x <- valsFME fme ] -- ¤¿¤À¤·¡¤matchFME (E _) fme¤Î¾ì¹ç¡ÊÁ´ÂΤ¬existential¤Î¾ì¹ç¡Ë¤Ï¤½¤â¤½¤âintroBK¤»¤º¤Ëundefined¤Ê°ú¿ô¤Ë¤·¤Æ¤·¤Þ¤¦¤Ù¤¡¥¤É¤¦¤»¤½¤Î°ú¿ô¤Ï»È¤ï¤ì¤Ê¤¤¤Ã¤Æ¤³¤È¤À¤«¤é¡¥ -- Universal variables only match to existentials matchFME' x@(U _) fme s = matchExistential x fme s -- Constractor applications can match to both existentials and constructor applications with the same constructor.
MagicHaskeller/Analytical/Parser.hs view
@@ -43,7 +43,7 @@ inferTypedIOPairss ((name, (Just ty, Just (iops Types.::: infty))):ts) = do apinfty <- applyPS infty mguPS apinfty $ Types.quantify ty- updateSubstPS (return . unquantifySubst)+-- updateSubstPS (return . unquantifySubst) s <- getSubst let hd = (name, map (tapplyIOP s) iops Types.:::ty)@@ -51,7 +51,7 @@ return (hd:tl) inferTypedIOPairss ((name, (Nothing, Just (iops Types.::: infty))):ts) = do s <- getSubst- let hd = (name, map (tapplyIOP s) iops Types.::: Types.apply s infty)+ let hd = (name, map (tapplyIOP $ quantifySubst s) iops Types.::: Types.apply s infty) tl <- inferTypedIOPairss ts return (hd:tl) inferTypedIOPairss ((_nam, (Just _t, Nothing)):ts) = inferTypedIOPairss ts -- pattern including only a type signature. This is still useful when incorporating with MagicHaskeller, but MagH has its own parser, so let's ignore the pattern silently.@@ -103,6 +103,7 @@ matchType :: MonadPlus m => [Types.Type] -> Types.Type -> Types.Type -> PriorSubsts m () matchType argtys retty ty = mguType argtys retty (Types.quantify ty) >> updateSubstPS (return . unquantifySubst) unquantifySubst = map (\(v,t) -> (v, Types.unquantify t))+quantifySubst = map (\(v,t) -> (v, Types.quantify t)) mguType (t:ts) r (u Types.:->v) = do mguPS t u s <- getSubst mguType (map (Types.apply s) ts) (Types.apply s r) v@@ -161,12 +162,14 @@ getMbTypedConstr :: XVarLib -> Name -> Maybe (Types.Typed Constr) getMbTypedConstr xvl name = fmap (mkTypedConstr xvl) $ Map.lookup (nameBase name) (invVarLib xvl) getTypedConstr :: XVarLib -> Name -> Types.Typed Constr-getTypedConstr xvl name = let c = invVarLib xvl Map.! (nameBase name) in mkTypedConstr xvl c+getTypedConstr xvl name = case Map.lookup (nameBase name) $ invVarLib xvl of Just c -> mkTypedConstr xvl c+ Nothing -> error ("could not find "++show name) mkTypedConstr xvl c = c Types.::: PD.dynType (varLib xvl!c)-patToExp ivl (LitP (IntegerL i)) | i>=0 = natToConExp ivl i- | otherwise = cap (mkTypedConstr ivl (negateID ivl)) [natToConExp ivl (-i)]--- patToExp tcl (LitP (CharL c)) = C (Ctor (ord c) (c¤ËÁêÅö¤¹¤ëÅÛ. ¤¢¤ëÌõ¤Ê¤¤?)) []--- patToExp tcl (LitP (StringL str)) = strToConExp tcl str+litToExp ivl (IntegerL i) | i>=0 = natToConExp ivl i+ | otherwise = cap (mkTypedConstr ivl (negateID ivl)) [natToConExp ivl (-i)]+-- litToExp tcl (CharL c) = C (Ctor (ord c) (c¤ËÁêÅö¤¹¤ëÅÛ. ¤¢¤ëÌõ¤Ê¤¤?)) [] ¤Æ¤æ¡¼¤«¡¤constructor°·¤¤¤Ë¤¹¤ì¤Ð¤¤¤¤¤Î¤À¤¬¡¥+-- litToExp tcl (StringL str) = strToConExp tcl str+patToExp ivl (LitP l) = litToExp ivl l patToExp ivl (VarP name) = U (strToInt $ nameBase name) patToExp ivl (TupP pats) = cap (getTypedConstr ivl (tupleDataName (length pats))) (map (patToExp ivl) pats) patToExp ivl (ConP name pats) = cap (getTypedConstr ivl name) (map (patToExp ivl) pats)@@ -194,8 +197,7 @@ thExpToExpr ivl (VarE name) = case getMbTypedConstr ivl name of Nothing -> U (strToInt $ nameBase name) Just x -> C 1 x [] thExpToExpr ivl (ConE name) = C 1 (getTypedConstr ivl name) []-thExpToExpr ivl (LitE (IntegerL i)) | i >= 0 = natToConExp ivl i- | otherwise = cap (mkTypedConstr ivl (negateID ivl)) [natToConExp ivl (-i)]+thExpToExpr ivl (LitE l) = litToExp ivl l thExpToExpr ivl (AppE f x) = case thExpToExpr ivl f of C sz c xs -> let thx = thExpToExpr ivl x in C (sz + size thx) c (xs ++ [thx]) -- O(n^2) U _ -> error "Only constructor applications are permitted in IO examples."
MagicHaskeller/Analytical/Syntax.hs view
@@ -50,7 +50,7 @@ type Subst = [(Int,Expr)] -unify (C _ i xs) (C _ j ys) | i==j = unifyList xs ys+unify (C _ i xs) (C _ j ys) | Types.typee i == Types.typee j = unifyList xs ys | otherwise = mzero unify e f | e==f = return [] unify (E i) e = bind i e
MagicHaskeller/Analytical/Synthesize.hs view
@@ -49,13 +49,37 @@ aritar = length $ inputs iop bk = reverse $ zipWith (Types.:::) (map mkBKFun $ bkiopss) bktypes in (fmap (\e -> napply (length bktups) FunLambda $ napply aritar Lambda (Fix e aritar [aritar-1, aritar-2..0])) $ -- $ Fix e $ map X [arity-1, arity-2 .. 0]) $ -- ËÜÅö¤Ï¤³¤Î·ë²Ì¤Î¤½¤ì¤¾¤ì¤Ë bknames¤òŬÍѤ·¤¿¤¤¤Î¤À¤¬¡¤bknames¤ÊHValue¤¬¤Ê¤¤¤Î¤Ç.... ¤Æ¤æ¡¼¤«¡¤Exp¤Ê¤éºî¤ì¤ë¡¥CoreExpr¤â¡¤BK¤¬Á´ÉôVarLib¤Ë¤Ï¤¤¤Ã¤Æ¤¤¤ì¤Ðºî¤ì¤ë¡¥- analSynthm {- analSynthNoUniT ¤³¤Ã¤Á¤À¤È¤Á¤ç¤Ã¤È¤¤¤¤²Ã¸º¤Ç¤Á¤ç¤Ã¤È®¤¤ -} bk (target Types.:::ty)+ fastAnalSynthNoUniT bk (target Types.::: ty) ,foldr (Types.:->) ty bktypes) _ -> error "TypedIOPairs.analyticSynth*: More than one I/O pairs are defined as the target." where xvl = mkXVarLib vl -analSynth, analSynthm :: Search m => BK -> Types.Typed Fun -> m CoreExpr+fastAnalSynthNoUniT bk tfun@(fun Types.::: _) | any hasExistential $ map output $ iopairs fun = analSynthNoUniT bk tfun+ | otherwise = fastAnalSynthmNoUniT bk tfun++--fastAnalSynthNoUniT = fastAnalSynthmNoUniT+fastAnalSynthmNoUniT bk tfun+ = others `mplus` delay bkRelated+ where newbk = tfun : bk+ bkRelated = headSpine analSynthNoUniT introBKm newbk tfun + others = headSpine fastAnalSynthNoUniT (introConstr +++ introVarm +++ ndelayIntro 2 introCase) newbk tfun++analSynthNoUniT bk tfun+ = headSpine analSynthNoUniT (introConstr +++ introVarm' +++ ndelayIntro 2 introCase +++ ndelayIntro 1 introBKm) (tfun:bk) tfun++{-+The following definition of analSynth should work even if +- existential variables are included in BK or in Fun, e.g. a function binding + f a = b+ is included+ or+- the same variable name appear multiple times in the LHS (input examples) of an I/O example in BK or in Fun, E.g. a function binding+ f a a = 1+ is included.+Those bindings are not valid Haskell, nor accepted by Template Haskell, so a library like haskell-src has to be used for parsing them.+-}+analSynth, analSynthm, fastAnalSynthNoUniT :: Search m => BK -> Types.Typed Fun -> m CoreExpr analSynth bk tfun@(fun Types.::: _) | any hasExistential $ map output $ iopairs fun = fmap fst $ runStateT (analSynthUTm bk tfun) emptySt | otherwise = analSynthm bk tfun analSynthm bk tfun@@ -104,9 +128,6 @@ ) _ -> error "TypedIOPairs.analyticSynth*: More than one I/O pairs are defined as the target." where xvl = mkXVarLib vl--- analSynthNoUniT is inaccurate, but should work in most cases. This can be used in place of analSynthm-analSynthNoUniT bk tfun- = headSpine analSynthNoUniT (introConstr +++ introVarm +++ ndelayIntro 2 introCase +++ ndelayIntro 1 introBKm) (tfun:bk) tfun analSynthNoUniT_debug (Br intro trs) bk tfun = headSpine_debug analSynthNoUniT_debug trs intro (tfun:bk) tfun @@ -169,7 +190,7 @@ liftList :: MonadPlus m => StateT s [] a -> StateT s m a liftList = mapStateT (msum . map return) -introVarm, introConstr, introCase :: (Functor m, MonadPlus m) => Introducer m -- introConstr¤Ç¤Ï¡¤¼ÂºÝ¤Ë¤ÏCoreExpr¤ÏConstr¤Ç¤è¤¤¡¥+introVarm, introVarm', introConstr, introCase :: (Functor m, MonadPlus m) => Introducer m -- introConstr¤Ç¤Ï¡¤¼ÂºÝ¤Ë¤ÏCoreExpr¤ÏConstr¤Ç¤è¤¤¡¥ introBKm :: (Search m) => Introducer m -- introConstr¤Ç¤Ï¡¤¼ÂºÝ¤Ë¤ÏCoreExpr¤ÏConstr¤Ç¤è¤¤¡¥ introVarUTm, introBKUTm :: MonadPlus m => IntroUniT m -- introVarUTm¤Ï°ìÏ¢¤ÎIgor´Ø·¸¤ÎÏÀʸ¤Ë¤Ï¤Ê¤¤¤â¤Î¤Î¡¤introBK¤¬Í¸ú¤ËƯ¤¯¤Ë¤ÏɬÍס¥¤³¤ì¤¬¤Ê¤¤¤È¡¤f¤òºî¤ë¤Î¤ËBK¤È¤·¤Æf¤ò»È¤Ã¤Æ¤â¡¤introBK¤À¤±¤Ç½ª¤ï¤Ã¤Æ¤¯¤ì¤º¡¤À¸À®¤µ¤ì¤Ê¤¤¡¥@@ -182,6 +203,8 @@ -- introVarm b f = introVar (zipWithM_ unify) b f *************************************** ¤³¤ì¤Ï¥Ç¥Ð¥Ã¥°»þ¤ËÍÍѤʤ³¤È¤â¡¥ introVarm = introVar (\a b -> guard $ a==b) +introVarm' = introVar (zipWithM_ unify)+ introVar :: MonadPlus m => ([Expr] -> [Expr] -> m ()) -> Introducer m introVar cmp _ (fun Types.::: ty) = do let (argtys, retty) = Types.splitArgs ty@@ -189,7 +212,7 @@ arifun = arity fun let trins = transpose $ map inputs iops -- (ix,inps Types.::: argty) <- msum $ map return $ zip [0..] trins- (ix,argty,inps) <- msum [ return t | t@(_,aty,_) <- zip3 [0..] argtys $ visibles (toBeSought fun) trins, aty == retty ]+ (ix,argty,inps) <- msum [ return t | t@(_,aty,_) <- zip3 [0..] argtys $ visibles (toBeSought fun) trins, Types.mgu aty retty /= Nothing] -- The following four lines should be equivalent to cmp (map output iops) inps@@ -281,7 +304,7 @@ let (bkargtys, bkretty) = Types.splitArgs bkty substy <- Types.match bkretty retty iopss <- case bkfun of BKF{maxNumBVs=addendum} -> subBK (-addendum) (iopairs fun) bkfun- Rec{maxNumBVs=addendum} -> sub (-addendum) initTS (iopairs fun) bkfun+ Rec{maxNumBVs=addendum} -> sub (-addendum) initTS fun bkfun return (foldl (:$) (FunX ix), [ setIOPairs iops fun Types.::: tys | iops Types.::: tys <- reverse $ @@ -316,16 +339,18 @@ apbkf = applyIOPs s $ iopairs bkf bkiop <- msum $ map return apbkf subtractIOPairUTm aptgt bkiop-subtractIOPairsFromIOPairsUTm :: MonadPlus m => TermStat -> [IOPair] -> Fun -> UniT m [[IOPair]]+subtractIOPairsFromIOPairsUTm :: MonadPlus m => TermStat -> Fun -> Fun -> UniT m [[IOPair]]+subtractIOPairsFromIOPairsUTm ts tgt bkf = subtractIOPairsFromIOPairsUTm' ts (iopairs tgt) bkf+subtractIOPairsFromIOPairsUTm' :: MonadPlus m => TermStat -> [IOPair] -> Fun -> UniT m [[IOPair]] {- subtractIOPairsFromIOPairs funs bks = foldr (\fun rest -> do iops <- subtractIOPairs fun bks iopss <- rest return (iops:iopss)) (return []) funs -}-subtractIOPairsFromIOPairsUTm ts [] bkf = return []-subtractIOPairsFromIOPairsUTm ts (fun:funs) bkf = do+subtractIOPairsFromIOPairsUTm' ts [] bkf = return []+subtractIOPairsFromIOPairsUTm' ts (fun:funs) bkf = do (iops,newts) <- subtractIOPairsUTm ts fun bkf- iopss <- subtractIOPairsFromIOPairsUTm newts funs bkf -- iops¤Ï¡¤subfunction¤¬Ê£¿ô¤¢¤Ã¤Æ¡¤¤½¤ì¤ésubfunctions¤Î¤½¤ì¤¾¤ì¤Ë´Ø¤·¤ÆIOPair1¸Ä¤º¤Ä¤Ë²á¤®¤Ê¤¤¡¥+ iopss <- subtractIOPairsFromIOPairsUTm' newts funs bkf -- iops¤Ï¡¤subfunction¤¬Ê£¿ô¤¢¤Ã¤Æ¡¤¤½¤ì¤ésubfunctions¤Î¤½¤ì¤¾¤ì¤Ë´Ø¤·¤ÆIOPair1¸Ä¤º¤Ä¤Ë²á¤®¤Ê¤¤¡¥ return (iops:iopss) subtractIOPairsUTm :: MonadPlus m => TermStat -> IOPair -> Fun -> UniT m ([IOPair], TermStat) -- Æ⦥ꥹ¥È¤Î´ð¿ô¤Ïfun¤Îarity, ³°Â¦¤Ïbk¤ÎIO pair¤Î¤¦¤Ámatch¤¹¤ë¤Î¤Ï¤¤¤¯¤Ä¤¢¤ë¤« -- ¤Æ¤æ¡¼¤«¡¤Æ⦤Ïbk¤Îarity¤Ç¤Ï¡©@@ -357,23 +382,27 @@ return [ fun{output=apply s o} | o <- inputs frbkiop ] -- This @apply@ is necessary here because introBKm will soon forget the substitution. subtractIOPairsFromIOPairsm :: Int -- maxNumBVs¤Ç¥²¥Ã¥È¤Ç¤¤ëÃÍ¡¥- -> TermStat -> [IOPair] -> Fun -> [] [[IOPair]]-subtractIOPairsFromIOPairsm addendum ts tgt bkf = subtractIOPairsFromIOPairsmFME addendum ts tgt bkf addendum-subtractIOPairsFromIOPairsmFME :: Int -> TermStat -> [IOPair] -> Fun -> Int -> [] [[IOPair]]+ -> TermStat -> Fun -> Fun -> [] [[IOPair]]+subtractIOPairsFromIOPairsm addendum ts tgt bkf+ = subtractIOPairsFromIOPairsmFME addendum ts (length $ filter id $ toBeSought tgt) -- the actual arity+ (iopairs tgt) bkf addendum+subtractIOPairsFromIOPairsmFME :: Int -> TermStat -> Int -> [IOPair] -> Fun -> Int -> [] [[IOPair]] {- subtractIOPairsFromIOPairsBK funs bks = foldr (liftM2 (:)) (return []) $ map (flip subtractIOPairs bks) funs -}-subtractIOPairsFromIOPairsmFME addendum ts [] bkf offset = return []-subtractIOPairsFromIOPairsmFME addendum ts (fun:funs) bkf offset = do - (iops,newts) <- subtractIOPairsmFME ts fun bkf offset- iopss <- subtractIOPairsFromIOPairsmFME addendum newts funs bkf (offset+addendum) -- iops¤Ï¡¤subfunction¤¬Ê£¿ô¤¢¤Ã¤Æ¡¤¤½¤ì¤ésubfunctions¤Î¤½¤ì¤¾¤ì¤Ë´Ø¤·¤ÆIOPair1¸Ä¤º¤Ä¤Ë²á¤®¤Ê¤¤¡¥+subtractIOPairsFromIOPairsmFME addendum ts ary [] bkf offset = return []+subtractIOPairsFromIOPairsmFME addendum ts ary (fun:funs) bkf offset = do + (iops,newts) <- subtractIOPairsmFME ts ary fun bkf offset+ iopss <- subtractIOPairsFromIOPairsmFME addendum newts ary funs bkf (offset+addendum) -- iops¤Ï¡¤subfunction¤¬Ê£¿ô¤¢¤Ã¤Æ¡¤¤½¤ì¤ésubfunctions¤Î¤½¤ì¤¾¤ì¤Ë´Ø¤·¤ÆIOPair1¸Ä¤º¤Ä¤Ë²á¤®¤Ê¤¤¡¥ return (iops:iopss) -- Applying substitutions to funs is not currently necessary (because funs does not include existential variables), but that will be useful in future versions which fill gaps of input examples. -subtractIOPairsmFME :: TermStat -> IOPair -> Fun -> Int -> [([IOPair], TermStat)] -- ÊÖ¤êÃͤÎ[IOPair]¤Ï³Æ°ú¿ô¤ËÂбþ-subtractIOPairsmFME ts tgtiop bkf offset = do +subtractIOPairsmFME :: TermStat -> Int -> IOPair -> Fun -> Int -> [([IOPair], TermStat)] -- ÊÖ¤êÃͤÎ[IOPair]¤Ï³Æ°ú¿ô¤ËÂбþ+subtractIOPairsmFME ts ary tgtiop bkf offset + = case output tgtiop of E{} -> [(replicate (arity bkf) tgtiop, ts)] -- target¤ÎÊÖ¤êÃͤ¬Ã±¤Ëexistential variable¤Î¾ì¹ç¡¤»È¤ï¤ì¤Ê¤¤¤Î¤Ç¤Ê¤ó¤Ç¤â¤è¤¤¡¥¤¬¡¤arity¤ò·¤¨¤ëɬÍפ¬¤¢¤ë¡¥+ tgto -> do let vistgt = reverse $ visibles (reverse $ toBeSought bkf) $ reverse $ inputs tgtiop- visbkis <- unifyingIOPairs (output tgtiop) (fmexpr bkf) offset+ visbkis <- unifyingIOPairs tgto (fmexpr bkf) offset let iops = [ tgtiop{output=o} | o <- visbkis ] let newts = updateTS visbkis vistgt ts -- This makes sure that the generated program does not go into a loop. guard $ evalTS newts
MagicHaskeller/Classify.hs view
@@ -57,7 +57,7 @@ Just ([], op) -> fmap snd . ofilter (op,pto) . fmap opreexecute -- Just (rnds,op) -> unscanl . fmap snd . repEqClsBy_simple op . fmap (spreexecute rnds) -- Feb. 10, 2007¤Înotes¤ÎºÇ¸å¤ÎÊդ껲¾È¡¥Matrix¤Î¾ì¹ç¤Í¡¥ Just (rnds,op) -> fmap snd . sfilter (op,pto) . fmap (spreexecute (uncurryDyn (mkUncurry tcl) typ) rnds)-spreexecute uncurrier rnds e@(AE _ dyn) = let f = uncurrier dyn in (map (dynApp f) rnds, e)+spreexecute uncurrier rnds e@(AE _ dyn) = let f = uncurrier dyn in (map (dynAppErr "in Classify.spreexecute" f) rnds, e) opreexecute :: AnnExpr -> (Dynamic, AnnExpr) opreexecute e@(AE _ dyn) = (dyn, e)@@ -187,7 +187,8 @@ Just EQ -> diffSortedByBot op cs ds Just LT -> c : diffSortedByBot op cs ws Just GT -> diffSortedByBot op vs ds- Nothing -> c : diffSortedByBot op cs ds -- I just do not know what is the best solution here, but when timeout happens, I temporarily believe @c@, and skip d.+-- Nothing -> c : diffSortedByBot op cs ds -- I just do not know what is the best solution here, but when timeout happens, I temporarily believe @c@, and skip d.+ Nothing -> diffSortedByBot op cs ds -- The above turned out to be not a good solution, because when an error (or a timeout) happens, the expression repeatedly appears at each depth. See newnotes on Dec. 18, 2011 {-
MagicHaskeller/ClassifyDM.hs view
@@ -30,7 +30,7 @@ select = zipDepthDB $ \d -> map (\((xss,ae),i) -> (((xss!!d), ae),i)) spreexecuteDM :: (Dynamic->Dynamic) -> [[Dynamic]] -> AnnExpr -> ([[Dynamic]], AnnExpr)-spreexecuteDM uncurrier rnds e@(AE _ dyn) = let f = uncurrier dyn in (map ({- forceList . -} map (dynApp f)) rnds, e)+spreexecuteDM uncurrier rnds e@(AE _ dyn) = let f = uncurrier dyn in (map ({- forceList . -} map (dynAppErr "in ClassifyDM.spreexecuteDM" f)) rnds, e) sprDM :: (Dynamic->Dynamic) -> [[Dynamic]] -> AnnExpr -> Int -> ([Dynamic], AnnExpr) sprDM unc rnds e db = case spreexecuteDM unc rnds e of (xss, ae) -> (xss!!db, ae)@@ -91,7 +91,7 @@ #ifdef CHTO listCmpBot len (cmp,pto) xs ys = unsafeWithPTOOpt pto $ listCmp len cmp xs ys #else-listCmpBot len cmp xs ys = Just $ listCmp len cmp xs ys+listCmpBot len (cmp,_) xs ys = Just $ listCmp len cmp xs ys #endif
MagicHaskeller/CoreLang.lhs view
@@ -286,27 +286,36 @@ primitivesToVL :: TyConLib -> [Primitive] -> VarLib primitivesToVL tcl ps- = listArray (0, length ps + 7) (map (\ (HV x, e, ty) -> PD.unsafeToDyn tcl (thTypeToType tcl ty) x e) ps+ = listArray (0, length ps + (lenDefaultPrimitives-1)) (map (\ (HV x, e, ty) -> PD.unsafeToDyn tcl (thTypeToType tcl ty) x e) ps ++ defaultPrimitives) --- | 'defaultVarLib' can be used as a VarLib for testing and debugging.+-- | 'defaultVarLib' can be used as a VarLib for testing and debugging. Currently this is used only by the analytical synthesizer. defaultVarLib :: VarLib-defaultVarLib = listArray (0, length defaultPrimitives - 1) defaultPrimitives----- ¤Ç¤â¡¤¥Ç¥Ð¥Ã¥°ÌÜŪ¤Ç¡¤Int¤À¤±¤¸¤ã¤Ê¤¯¤Æ¥ê¥¹¥È¤È¤«¤âdefaultVarLib¤Ë´Þ¤á¤¿¤¤¡¥-----+defaultVarLib = listArray (0, lenDefaultPrimitives-1) defaultPrimitives +lenDefaultPrimitives = length defaultPrimitives -- | @defaultPrimitives@ is the set of primitives that we want to make sure to appear in VarLib but may not appear in the primitive set with which to synthesize. -- In other words, it is the set of primitives we want to make sure to assign IDs to. defaultPrimitives :: [PD.Dynamic] defaultPrimitives = [+ $(PD.dynamic [|defaultTCL|] [|()::()|]),+ $(PD.dynamic [|defaultTCL|] [|(,) ::a->b->(a,b)|]),+ $(PD.dynamic [|defaultTCL|] [|(,,) ::a->b->c->(a,b,c)|]),+ $(PD.dynamic [|defaultTCL|] [|(,,,) ::a->b->c->d->(a,b,c,d)|]),+ $(PD.dynamic [|defaultTCL|] [|(,,,,) ::a->b->c->d->e->(a,b,c,d,e)|]),+ $(PD.dynamic [|defaultTCL|] [|(,,,,,) ::a->b->c->d->e->f->(a,b,c,d,e,f)|]),+ $(PD.dynamic [|defaultTCL|] [|(,,,,,,)::a->b->c->d->e->f->g->(a,b,c,d,e,f,g)|]),++ $(PD.dynamic [|defaultTCL|] [|Left :: a -> Either a b|]),+ $(PD.dynamic [|defaultTCL|] [|Right :: b -> Either a b|]),+ $(PD.dynamic [|defaultTCL|] [|Nothing :: Maybe a|]),+ $(PD.dynamic [|defaultTCL|] [|Just :: a -> Maybe a|]),+ $(PD.dynamic [|defaultTCL|] [|LT :: Ordering|]),+ $(PD.dynamic [|defaultTCL|] [|EQ :: Ordering|]),+ $(PD.dynamic [|defaultTCL|] [|GT :: Ordering|]),+ $(PD.dynamic [|defaultTCL|] [|(+)::Int->Int->Int|]), $(PD.dynamic [|defaultTCL|] [|False::Bool|]), $(PD.dynamic [|defaultTCL|] [|True::Bool|]),
MagicHaskeller/DebMT.lhs view
@@ -36,8 +36,6 @@ lookupMT mt (t0:->t1) = lookupMT (lookupMT (funMT mt) t0) t1 -encode :: Type -> Int -> (Type, Decoder)- retrieve :: Decoder -> Subst -> Subst -- retrieve deco sub = let news = [ (decodeVar deco i, decode deco ty) | (i, ty) <- sub ] in trace ("sub = " ++ show sub ++ " and news = " ++ show news ++ " and deco = " ++ show deco) news retrieve deco sub = [ (decodeVar deco i, decode deco ty) | (i, ty) <- sub ]@@ -47,6 +45,7 @@ decodeVar (Dec tvs margin) tv = case tvs !? tv of Nothing -> tv+margin Just ntv -> ntv +encode :: Type -> Int -> (Type, Decoder) encode = Types.normalizeVarIDs
MagicHaskeller/ExecuteAPI610.hs view
@@ -136,7 +136,7 @@ case sf of Succeeded -> return () Failed -> error "failed to load modules" - -- liftIO $ hPutStrLn stderr "setting up modules********************************************************"+ -- liftIO $ hPutStrLn stderr "setting up modules" #ifdef GHC7 modules <- mapM (\fs -> fmap (\x -> (x,Nothing)) $ findModule (mkModuleName fs) Nothing) ("Prelude":fss) #else@@ -242,8 +242,6 @@ stmtToCore hscEnv pst = do let dfs = hsc_dflags hscEnv icxt = hsc_IC hscEnv- -- hPutStrLn stderr "*************************************"- -- hPutStrLn stderr $ showSDoc $ ppr pst (tcmsgs, mbtc) <- tcRnStmt hscEnv icxt pst case mbtc of Nothing -> perror dfs tcmsgs Just (ids, tc_expr) -> do -- desugar@@ -329,6 +327,7 @@ directExecuteAPI hscEnv gm ce = runCoreExpr hscEnv $ ceToCSCE gm ce + -- Note: MagicHaskeller.Primitive = (HValue, TH.Exp, TH.Type) -- Use -- typeToTHType :: TyConLib -> Types.Type -> TH.Type@@ -355,6 +354,7 @@ -- data CoreExpr a = ... ¤ß¤¿¤¤¤Ë¤·¤Æ¡¤CoreExpr CoreSyn.CoreExpr¤ß¤¿¤¤¤Ë»È¤¦¡¥ mkGlobalMap hscEnv tups = do ces <- mapM (compileVar hscEnv) tups return $ Map.fromList $ zip (map (\(_,b,_) -> thToBaseString b) tups) ces+ {- -- See Linker.linkDependencies
MagicHaskeller/Instantiate.hs view
@@ -20,7 +20,7 @@ import Control.Monad import qualified Data.IntMap as IntMap -import MagicHaskeller.MyDynamic+import MagicHaskeller.MyDynamic hiding (dynApp) -- import Data.Typeable import MagicHaskeller.ReadDynamic(dynI)@@ -34,6 +34,8 @@ -- import Debug.Trace trace _ e = e +dynApp = dynAppErr "in MagicHaskeller.Instantiate"+ type Order = Maybe ([Dynamic], PackedOrd) type ExpResult = ([Dynamic],CoreExpr)@@ -93,7 +95,7 @@ dynToCompare :: TyConLib -> Dynamic -> (Dynamic -> Dynamic -> Ordering)-dynToCompare tcl dyn d0 d1 = fromDyn tcl (dynApp (dynApp dyn d0) d1) (error "dynToCompare: type mismatch")+dynToCompare tcl dyn d0 d1 = fromDyn tcl (dynAppErr "in dynToCompare (1)" (dynAppErr "in dynToCompare (2)" dyn d0) d1) (error "dynToCompare: type mismatch") --dynToCompare tcl dyn d0 d1 = aLittleSafeFromDyn (readType' tcl "Ordering") (dynApp (dynApp dyn d0) d1) -- °ú¿ô¤Î·¿¤¬³ÎÄꤷ¤Æ¤âÊÖ¤êÃͤη¿¤¬³ÎÄꤷ¤Ê¤¤¾ì¹ç¡§¤¿¤È¤¨¤Ðundefined¤äerror¤È¤«¡¥¤³¤Î¤Ø¤ó¤ò¤Á¤ã¤ó¤Ètake care¤·¤È¤«¤Ê¤¤¤È¡¤¤à¤ê¤ä¤êInt¤ËÊÑ´¹¤¹¤ë¤³¤È¤Ë¤Ê¤ë¡¥...¤Þ¤¢¤¤¤Ã¤«¡©
MagicHaskeller/LibTH.hs view
@@ -12,7 +12,7 @@ import System.Random(mkStdGen) import Control.Monad(liftM2) -initialize, init075 :: IO ()+initialize, init075, inittv1 :: IO () initialize = do setPrimitives (list ++ nat ++ natural ++ mb ++ bool ++ $(p [| (hd :: (->) [a] (Maybe a), (+) :: Int -> Int -> Int, (+) :: Integer -> Integer -> Integer) |])) setDepth 10 -- MagicHaskeller version 0.8 ignores the setDepth value and always memoizes.@@ -69,7 +69,7 @@ np i = let i' = i-1 in f i' (np i') -list' = $(p [| ([], (:), foldr :: (b -> a -> a) -> a -> (->) [b] a) |] )+list' = $(p [| ([], (:), foldr :: (b -> a -> a) -> a -> (->) [b] a, tail :: [a] -> [a]) |] ) -- foldr's argument order makes the synthesis slower:) list = $(p [| ([], (:), list_para :: (->) [b] (a -> (b -> [b] -> a -> a) -> a)) |] ) -- List paramorphism@@ -185,10 +185,10 @@ (list++bool) rich -rich = (list ++ bool ++- -- nat ++- -- mb ++ bool ++ $(p [| (hd :: [a] -> Maybe a, (+) :: Int -> Int -> Int) |]) ++- boolean ++ eq ++ -- intinst +++rich = (list' +++ nat +++ mb ++ bool ++ $(p [| (hd :: [a] -> Maybe a, (+) :: Int -> Int -> Int) |]) +++ boolean ++ eq ++ intinst ++ list1 ++ list2 ++ list3) @@ -200,7 +200,7 @@ -- just for debugging ra :: ProgramGenerator pg => pg ra = mkPG rich'-rich' = (list++bool++boolean+++rich' = (list'++bool++boolean++ list1 ++ list3) mx :: ProgramGenerator pg => pg
MagicHaskeller/MHTH.lhs view
@@ -38,9 +38,9 @@ expToExpExp (InfixE (Just e0) e Nothing) = [| InfixE (Just $(expToExpExp e0)) $(expToExpExp e) Nothing |] expToExpExp (InfixE Nothing e (Just e1)) = [| InfixE Nothing $(expToExpExp e) (Just $(expToExpExp e1)) |] expToExpExp (InfixE (Just e0) e (Just e1)) = [| InfixE (Just $(expToExpExp e0)) $(expToExpExp e) (Just $(expToExpExp e1)) |]-expToExpExp (TupE es) = [| (return . AppE . TupE) =<< $((return . ListE) =<< mapM expToExpExp es) |]+expToExpExp (TupE es) = [| TupE $((return . ListE) =<< mapM expToExpExp es) |] expToExpExp (CondE e0 e1 e2) = [| CondE $(expToExpExp e0) $(expToExpExp e1) $(expToExpExp e2) |]-expToExpExp (ListE es) = [| (return . AppE . ListE) =<< $((return . ListE) =<< mapM expToExpExp es) |]+expToExpExp (ListE es) = [| ListE $((return . ListE) =<< mapM expToExpExp es) |] expToExpExp e@(LitE (CharL c)) = [| LitE (CharL $(return e)) |] expToExpExp e@(LitE (StringL s)) = [| LitE (StringL $(return e)) |] expToExpExp e@(LitE (IntegerL c)) = [| LitE (IntegerL $(return e)) |]@@ -74,6 +74,10 @@ patToExpPat WildP = [| WildP |] patToExpPat (ListP ps) = [| ListP $(liftM ListE $ mapM patToExpPat ps) |] patToExpPat (SigP p t) = [| SigP $(patToExpPat p) $(typeToExpType t) |]+patToExpPat (LitP (IntegerL i)) = [| LitP (IntegerL $(return $ LitE (IntegerL i))) |]+patToExpPat (LitP (CharL c)) = [| LitP (CharL $(return $ LitE (CharL c))) |]+patToExpPat (LitP (StringL cs)) = [| LitP (StringL $(return $ LitE (StringL cs))) |]+patToExpPat (LitP (RationalL r)) = [| LitP (RationalL $(return $ LitE (RationalL r))) |] decsToExpDecs ds = fmap ListE $ mapM decToExpDec ds decToExpDec (FunD name clauses) = [| FunD (mkName $(nameToNameStr showTypeName name)) $(liftM ListE $ mapM clauseToExpClause clauses) |]
MagicHaskeller/Options.hs view
@@ -18,7 +18,12 @@ , 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.- , 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.+ , 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'. , 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.@@ -118,6 +123,10 @@ -- reducer (opt,_,_,_,_) = execute opt ++forget :: Opt a -> Opt ()+forget opt = case primopt opt of Nothing -> opt{primopt = Nothing}+ Just _ -> opt{primopt = Just ()} nrnds = map fnrnds [0..]
MagicHaskeller/PriorSubsts.lhs view
@@ -1,6 +1,10 @@ -- -- (c) Susumu Katayama --++Everything written in this module can be rewritten using StateT.+When I wrote this first (around 2003?) I did not know the term `Monad Transformer' and I reinvented it....+ \begin{code} {-# OPTIONS -cpp -fglasgow-exts #-} module MagicHaskeller.PriorSubsts where
MagicHaskeller/ProgGenSF.lhs view
@@ -60,7 +60,7 @@ type ExpTip e = Matrix e type ExpTrie e = MapType (ExpTip e)-type TypeTrie e = MapType (Matrix (ExpTip e, Subst, Int))+type TypeTrie e = MapType (Matrix ([e], Subst, Int)) type MemoTrie e = (TypeTrie e, ExpTrie e) @@ -156,10 +156,10 @@ = let mxty = maxVarID ty -- `max` maximum (map maxVarID avail) in Mx $ map (tokoro10ap ty) $ scanl1 (++) $ unMx $ toMx $ unPS ps emptySubst (mxty+1) -}-freezePS :: Type -> PriorSubsts DBound (ExpTip e) -> Matrix (ExpTip e,Subst,Int)+freezePS :: Type -> PriorSubsts DBound (ExpTip e) -> Matrix ([e],Subst,Int) freezePS ty ps = let mxty = maxVarID ty -- `max` maximum (map maxVarID avail)- in mapDepth (tokoro10ap ty) $ toMx $ fmap fst $ Rc $ unDB $ unPS ps emptySubst (mxty+1)+ in zipDepthMx (\d tups -> map (\(Mx xss, s, i)->(xss!!d, s, i)) $ tokoro10ap ty tups) $ toMx $ fmap fst $ Rc $ unDB $ unPS ps emptySubst (mxty+1) -- MemoStingy.tokoro10 is different from T10.tokoro10, in that duplicates will be removed. -- (Note that the type can be specialized to [(Type,k,i)] -> [(Type,k,i)])@@ -199,7 +199,7 @@ | memocond depth = lookupUniExprs memodeb avail t depth >> return () | otherwise = makeUniExprs memodeb avail t depth >> return () -lookupUniExprs :: Expression e => MemoDeb e -> [Type] -> Type -> Int -> PriorSubsts [] (ExpTip e)+lookupUniExprs :: Expression e => MemoDeb e -> [Type] -> Type -> Int -> PriorSubsts [] [e] lookupUniExprs memodeb@((mt,_),_,_) avail t depth = lookupNormalized (\tn -> unMx (lmtty mt tn) !! depth) avail t @@ -270,9 +270,7 @@ lookupTypeTrie :: Expression e => MemoDeb e -> Type -> Recomp ([e], Subst, Int) lookupTypeTrie ((mt,_), _, _) t- = Rc $ - \depth -> let Mx xss = lmtty mt t- in [ (yss!!depth, s, i) | (Mx yss, s, i) <- xss !! depth ]+ = toRc $ lmtty mt t lookupNormalized :: MonadPlus m => (Type -> m (e, Subst, Int)) -> [Type] -> Type -> PriorSubsts m e
− MagicHaskeller/ProgGenXF.lhs
@@ -1,322 +0,0 @@--- --- (c) Susumu Katayama-----\begin{code}-{-# OPTIONS -cpp -XRelaxedPolyRec #-}-module MagicHaskeller.ProgGenXF(ProgGenXF) where-import MagicHaskeller.Types-import MagicHaskeller.TyConLib-import Control.Monad-import MagicHaskeller.CoreLang-import Control.Monad.Search.Combinatorial-import MagicHaskeller.PriorSubsts-import Data.List(partition, sortBy, sort, nub, (\\))-import Data.Ix(inRange)--import MagicHaskeller.ClassifyDM--import System.Random(mkStdGen, StdGen)-import MagicHaskeller.Instantiate--import MagicHaskeller.ProgramGenerator-import MagicHaskeller.Options(Opt(..))--import MagicHaskeller.Expression--import MagicHaskeller.ClassifyTr-import MagicHaskeller.MyDynamic--import MagicHaskeller.T10(mergesortWithBy)--import MagicHaskeller.DebMT--import Debug.Trace--- trace str = id--reorganize_ = reorganizer_--- reorganize_ = id--classify = True-traceExpTy _ = id--- traceExpTy fty = trace ("lookupexp "++ show fty)-traceTy _ = id--- traceTy fty = trace ("lookup "++ show fty)---- Memoization table, created from primitive components-newtype ProgGenXF = PGXF MemoDeb -- internal data representation.--- ^ Program generator with experimental leveraged filtration, experimental variant of ProgGenSF. The following is explanation of ProgGenSF.--- This program generator employs filtration by random testing, and rarely generate semantically equivalent expressions more than once, while different expressions will eventually appear (for most of the types, represented with Prelude types, whose arguments are instance of Arbitrary and which return instance of Ord).--- The idea is to apply random numbers to the generated expressions, compute the quotient set of the resulting values at each depth of the search tree, and adopt the complete system of representatives for the depth and push the remaining expressions to one step deeper in the search tree.--- (Thus, adoption of expressions that may be equivalent to another already-generated-expression will be postponed until their \"uniqueness\" is proved.)--- As a result, (unlike "ProgGen",) expressions with size N may not appear at depth N but some deeper place.------ "ProgGenSF" is more efficient along with a middle-sized primitive set (like @reallyall@ found in LibTH.hs),--- but is slower than "ProgGen" for a small-sized one.------ Also note that "ProgGenSF" depends on hard use of unsafe* stuff, so if there is a bug, it may segfault....--type ExpTip = (Stream (Forest ([Dynamic], AnnExpr)), Stream (Forest ([Dynamic], AnnExpr)), Matrix AnnExpr)--type ExpTrie = MapType ExpTip-type TypeTrie = MapType (Matrix (Matrix AnnExpr, Subst, Int))--type MemoTrie = (TypeTrie, ExpTrie)---lmt :: MemoDeb -> Type -> Matrix AnnExpr-lmt memoDeb@((_,mt),_,cmn) fty =- let (_,_,x) = traceExpTy fty $- lookupMT mt fty -- ¤³¤Ã¤Á¤À¤Èlookup--- filtBF cmn fty $ matchFunctions memoDeb fty -- ¤³¤Ã¤Á¤À¤Èrecompute- in x--- filtBF ty = fmap fromAnnExpr . filterBF tcl rtrie ty . fmap (toAnnExprWind (execute opt) ty) . tabulate-filtBF cmn ty | classify = filterTr cmn ty . fmap (toAnnExprWind (execute (opt cmn) (vl cmn)) ty) -- . mapDepth aUS- | otherwise = \bf -> (undefined, undefined, toMx $ mapDepth aUS bf)--lmtty mt fty = traceTy fty $- lookupMT mt fty----memocond i = 3<i--- memocond i = i<10-memocond i = True---- memocond ty = size ty < 10 -- popArgs avail t¤·¤Æ¤«¤é¤ä¤ë¤Î¤Ï¤Á¤ç¤Ã¤È̵ÂÌ¡¥¤È»×¤Ã¤¿¤±¤É¡¤¼ÂºÝ¤Ï´Ø·¸¤Ê¤¤¤ß¤¿¤¤¡¥--- memocond av ty = size ty + sum (map size av) < 10---instance ProgramGenerator ProgGenXF where- mkTrieOpt cmn tcesopt tces = PGXF (mkTrieOptSF cmn tcesopt tces)- matchingPrograms ty (PGXF x) = fromMx $ matchProgs x ty- unifyingPrograms ty px@(PGXF x) = fromRc $ catBags $ fmap (\ (es,_,_) -> map (toAnnExpr $ reducer px) es) $ unifyingPossibilities ty x- extractCommon (PGXF (_,_,cmn)) = cmn--unifyingPossibilities ty memodeb = unPS (unifyableExprs memodeb [] ty) emptySubst 0---- quantify¤µ¤ì¤¿¤ä¤Ä¤¬memoize¤µ¤ì¤Æ¤¤¤ëÌõ¤À¤«¤é¡¤query¤Îentry¤Ç¤Ïquantify¤¹¤ëɬÍפϤʤ¤--- entry for query--- ¤Æ¤æ¡¼¤«¡¤quantify¤·¤Á¤ã¤¦¤Ê¤éMemoDeb.mguPrograms¤«¤Ê¤ó¤«¤½¤Î¤Þ¤Þ»È¤¨¤Ð¤¤¤¤¤Ã¤ÆÏä⤢¤ë¡¥¤Þ¤¢¡¤recursive¤Ë¤Ï¾åµ¤ÎunifyableExprs¤ò¸Æ¤Ð¤Ê¤¤ã¥À¥á¤À¤±¤É¡¥--- ¤Ê¤ª¡¤¸·Ì©¤Ê°ÕÌ£¤Çmatch¤Ë¤¹¤ë¤Ë¤Ï¤É¤¦¤âquantify¤ÏɬÍפäݤ¤¡¥---matchProgs :: (Int, Memo) -> Type -> BF AnnExpr-matchProgs :: MemoDeb -> Type -> Matrix AnnExpr-matchProgs memodeb ty = fmap (toAnnExprWindWind (reducer $ PGXF memodeb) ty) $ -- fmap meToAE $ -- koko- lmt memodeb $ normalize $ unquantify ty -- ¤³¤Ã¤Á¤À¤Èlookup-{--matchProgs memodeb ty = fmap toAnnExpr $ wind (fmap (mapCE Lambda)) (lookupFuns memodeb) [] (quantify ty) -- ¤³¤Ã¤Á¤À¤Èrecompute ¤È¤¤¤¦¤È¸ìÊÀ¤¬¤¢¤ë¡¥recompute¤·¤¿¤¤ãlmt¤Î¤È¤³¤í¤òÊѤ¨¤ë¤Ù¤·¡¥---- matchProgs¤Î¤ß¤Î²¼ÀÁ¤±¡¤matchFuns¤È¸ò´¹²Äǽ-lookupFuns :: (Expression e, Ord e) => (Int, MemoDeb e) -> [Type] -> Type -> BF e-lookupFuns memodeb@(memodepth,((_,mt),_,tcl,rtrie)) avail reqret =-{--#ifdef CLASSIFY- fmap fromAnnExpr $ toRc $ filterDM tcl rtrie ty $ fromRc $ fmap (toAnnExprWind ty) $-#endif--}--- mapDepth uniqSort $- matchFuns memodeb avail reqret- where ty = popArgs avail reqret--}--specializedPossibleTypes :: Type -> MemoDeb -> Recomp Type-specializedPossibleTypes ty memodeb = runPS (fmap (\(av,t) -> popArgs av t) $ specializedTypes memodeb [] ty)--- specializedPossibleTypes ty memodeb@(_,((mt,_),_,_,_)) = fmap (\(_,s,_) -> apply s ty) $ toRc $ lmtty mt ty---type MemoDeb = (MemoTrie, (([Prim],[Prim]),([Prim],[Prim])), Common)--mkTrieOptSF :: Common -> [Typed [CoreExpr]] -> [Typed [CoreExpr]] -> MemoDeb-mkTrieOptSF cmn txsopt txs- = let- memoDeb = (memoTrie, (qtlopt,qtl), cmn)- -- memoTrie :: MemoTrie- memoTrie = (typeTrie,expTrie)- typeTrie = mkMTty (tcl cmn) (\ty -> freezePS ty (specTypes memoDeb ty))- expTrie = mkMTexp (tcl cmn) (\ty -> -- fmap (aeToME (tcl cmn) (rt cmn) ty) $- filtBF cmn ty $ toMx $ matchFunctions memoDeb ty)- in memoDeb- where qtlopt = splitPrims txsopt- qtl = splitPrims txs--mkMTty = mkMT-mkMTexp = mkMT--mondepth = zipDepthRc (\d xs -> trace ("depth="++show d++", and the length is "++show (length xs)) xs) -- depth¤Èɽ¼¨¤¹¤ë¤Ê¤é+1¤¹¤ë¤Ù¤¤Ç¤¢¤Ã¤¿¡¥(0¤«¤é»Ï¤Þ¤ë¤Î¤Ç)---type BFT = Recomp-unBFM = unMx---{--freezePS :: (Search m, Expression e) => Type -> PriorSubsts m (ExpTip e) -> Matrix (ExpTip e,Subst,Int)-freezePS ty ps- = let mxty = maxVarID ty -- `max` maximum (map maxVarID avail)- in Mx $ map (tokoro10ap ty) $ scanl1 (++) $ unMx $ toMx $ unPS ps emptySubst (mxty+1)--}-freezePS :: Type -> PriorSubsts Recomp e -> Matrix (e,Subst,Int)-freezePS ty ps- = let mxty = maxVarID ty -- `max` maximum (map maxVarID avail)- in mapDepth (tokoro10ap ty) $ toMx $ unPS ps emptySubst (mxty+1)---- MemoStingy.tokoro10 is different from T10.tokoro10, in that duplicates will be removed.--- (Note that the type can be specialized to [(Type,k,i)] -> [(Type,k,i)])-tokoro10 :: (Eq k, Ord k) => [(a,k,i)] -> [(a,k,i)]-tokoro10 = mergesortWithBy const (\ (_,k,_) (_,l,_) -> k `compare` l)---- tokoro10fstfst = mergesortWithBy const (\ ((k,_),_,_) ((l,_),_,_) -> k `compare` l)--tokoro10ap :: Type -> [(a,Subst,i)] -> [(a,Subst,i)]-tokoro10ap ty = mergesortWithBy const (\ (_,k,_) (_,l,_) -> normalize (apply k ty) `compare` normalize (apply l ty))----specializedTypes :: (Search m) => MemoDeb -> [Type] -> Type -> PriorSubsts m ([Type],Type)-specializedTypes memodeb avail t = do specializedCases memodeb avail t- subst <- getSubst- return (map (apply subst) avail, apply subst t)--- specializedCases is the same as unifyableExprs, except that the latter returns PriorSubsts BF [CoreExpr], and that the latter considers memodepth.-specializedCases, specCases, specCases' :: (Search m) => MemoDeb -> [Type] -> Type -> PriorSubsts m ()-specializedCases memodeb = applyDo (specCases memodeb)-specCases memodeb = wind_ (\avail reqret -> reorganize_ (\newavail -> uniExprs_ memodeb newavail reqret) avail)-{- ¤É¤Ã¤Á¤¬¤ï¤«¤ê¤ä¤¹¤¤¤«¤ÏÉÔÌÀ-specCases memodeb avail (t0:->t1) = specCases memodeb (t0 : avail) t1-specCases memodeb avail reqret = reorganize_ (\newavail -> uniExprs_ memodeb newavail reqret) avail--}------uniExprs_ :: (Search m) => MemoDeb -> [Type] -> Type -> PriorSubsts m ()-uniExprs_ memodeb avail t- = convertPS fromRc $ psListToPSRecomp lfp- where lfp depth- | memocond depth = lookupUniExprs memodeb avail t depth >> return ()- | otherwise = makeUniExprs memodeb avail t depth >> return ()--lookupUniExprs :: MemoDeb -> [Type] -> Type -> Int -> PriorSubsts [] (Matrix AnnExpr)-lookupUniExprs ((mt,_),_,_) avail t depth- = lookupNormalized (\tn -> unMx (lmtty mt tn) !! depth) avail t--makeUniExprs :: MemoDeb -> [Type] -> Type -> Int -> PriorSubsts [] Type-makeUniExprs memodeb avail t depth- = convertPS tokoro10fst $- do psRecompToPSList (reorganize_ (\av -> specCases' memodeb av t) avail) depth- sub <- getSubst- return $ quantify (apply sub $ popArgs avail t)----- entry point for memoization-specTypes :: (Search m) => MemoDeb -> Type -> PriorSubsts m (Matrix AnnExpr)-specTypes memodeb@((_,mt),_,_) ty- = do let (avail,t) = splitArgs ty- reorganize_ (\av -> specCases' memodeb av t) avail--- quantify¤ÏmemoÀè¤Ç´û¤Ë¤ä¤é¤ì¤Æ¤¤¤ë¤Î¤ÇÉÔÍ×- typ <- applyPS ty- return (lmt memodeb $ normalize $ unquantify typ)---funApSub_ :: Search m => (Type -> PriorSubsts m ()) -> (Type -> PriorSubsts m ()) -> Type -> PriorSubsts m ()-funApSub_ lltbehalf behalf (t:>ts) = do lltbehalf t- funApSub_ lltbehalf behalf ts-funApSub_ lltbehalf behalf (t:->ts) = do behalf t- funApSub_ lltbehalf behalf ts-funApSub_ lltbehalf behalf _t = return ()--funApSub_spec behalf = funApSub_ behalf behalf---- specCases' trie prims@(primgen,primmono) avail reqret = msum (map (retMono.fromPrim) primmono) `mplus` msum (map retMono fromAvail ++ map retGen primgen)-specCases' memodeb@((ttrie,etrie), (prims@(primgen,primmono),_),cmn) avail reqret- = msum (map retPrimMono primmono ++ map retMono avail ++ map retGen primgen)- where fas | constrL $ opt cmn = funApSub_ lltbehalf behalf- | otherwise = funApSub_spec behalf- where behalf = specializedCases memodeb avail- lltbehalf = flip mguAssumptions_ avail- -- retPrimMono :: (Int, Type, Int, Typed [CoreExpr]) -> PriorSubsts BFT ()- retPrimMono (arity, retty, numtvs, _xs:::ty)- = napply arity delayPS $- do tvid <- reserveTVars numtvs- mguPS reqret (mapTV (tvid+) retty)- fas (mapTV (tvid+) ty)- -- retMono :: Type -> PriorSubsts BFT ()- retMono ty = napply (getArity ty) delayPS $- do mguPS reqret (getRet ty)- fas ty- -- retGen :: (Int, Type, Int, Typed [CoreExpr]) -> PriorSubsts BFT ()- retGen (arity, _r, numtvs, _s:::ty) = napply arity delayPS $- do tvid <- reserveTVars numtvs -- ¤³¤Î¡ÊºÇ½é¤Î¡ËID¤½¤Î¤â¤Î¡Ê¤Ä¤Þ¤êÊÖ¤êÃͤÎtvID¡Ë¤Ï¤¹¤°¤Ë»È¤ï¤ì¤Ê¤¯¤Ê¤ë- -- let typ = apply (unitSubst tvid reqret) (mapTV (tvid+) ty) -- mapTV¤Èapply¤Ïhylo-fusion¤Ç¤¤ë¤Ï¤º¤À¤¬¡¤¾¡¼ê¤Ë¤µ¤ì¤ë¡©- -- -- unitSubst¤òinline¤Ë¤·¤Ê¤¤¤ÈÂÌÌܤ«- mkSubsts (tvndelay $ opt cmn) tvid reqret- fas (mapTV (tvid+) ty)-- gentvar <- applyPS (TV tvid)-- guard (orderedAndUsedArgs gentvar)- fas gentvar--type Generator m e = MemoDeb -> [Type] -> Type -> PriorSubsts m [e]--unifyableExprs :: Generator Recomp AnnExpr-unifyableExprs memodeb avails ty = unifyableExprs' memodeb avails ty-unifyableExprs' :: Generator Recomp AnnExpr-unifyableExprs' memodeb = applyDo (wind (fmap (map (mapCE Lambda))) (lookupNormalized (lookupTypeTrie memodeb)))---lookupTypeTrie :: MemoDeb -> Type -> Recomp ([AnnExpr], Subst, Int)-lookupTypeTrie memodeb@((mt,_), _, _) t- = Rc $ - \depth -> let Mx xss = lmtty mt t- in [ ({-map meToAE-} (yss!!depth), s, i) | (Mx yss, s, i) <- xss !! depth ]---lookupNormalized :: MonadPlus m => (Type -> m (e, Subst, Int)) -> [Type] -> Type -> PriorSubsts m e-lookupNormalized fun avail t- = do mx <- getMx- let typ = popArgs avail t- (tn, decoder) = encode typ mx- (es, sub, m) <- mkPS (fun tn)- updatePS (retrieve decoder sub)- updateMx (m+)- return es--tokoro10fst :: (Eq k, Ord k) => [(k,s,i)] -> [(k,s,i)]-tokoro10fst = mergesortWithBy const (\ (k,_,_) (l,_,_) -> k `compare` l)---- entry for memoization-matchFunctions :: MemoDeb -> Type -> Recomp AnnExpr-matchFunctions memodeb ty = case splitArgs (quantify ty) of (avail,t) -> matchFuns memodeb avail t--matchFuns :: MemoDeb -> [Type] -> Type -> Recomp AnnExpr-matchFuns memodeb avail reqret = catBags $ runPS (-- trace "matchFuns'" $ - matchFuns' unifyableExprs memodeb avail reqret)--matchFuns' :: Generator Recomp AnnExpr -> Generator Recomp AnnExpr--- matchFuns' = generateFuns matchPS filtExprs lookupListrie -- MemoDeb¤Î·¿¤Î°ã¤¤¤Ç¤³¤ì¤Ï¤¦¤Þ¤¯¤¤¤«¤Ê¤ó¤À¡¥-matchFuns' rec md@(_, (_,(primgen,primmono)),cmn) avail reqret- = let behalf = rec md avail- lltbehalf = lookupListrie lenavails rec md avail -- heuristic filtration- lenavails = length avail--- fe :: Type -> Type -> [CoreExpr] -> [CoreExpr] -- ^ heuristic filtration- fe = filtExprs (guess $ opt cmn)- in fromAssumptions (PGXF md) lenavails behalf matchPS reqret avail `mplus`- msum (map (retPrimMono (PGXF md) lenavails lltbehalf behalf matchPS reqret) primmono- ++ map (( if tv0 $ opt cmn then retGenTV0 else- if tv1 $ opt cmn then retGenTV1- else retGenOrd) (PGXF md) lenavails fe lltbehalf behalf reqret) primgen)--lookupListrie :: (Search m) => Int -> Generator m AnnExpr -> Generator m AnnExpr-lookupListrie lenavails rec memodeb@(_,_,cmn) avail t- | constrL opts = matchAssumptions (PGXF memodeb) lenavails t avail- | guess opts = do- args <- rec memodeb avail t- let args' = filter (not.isClosed.toCE) args- when (null args') mzero- return args'- | otherwise = rec memodeb avail t- where opts = opt cmn-filtExprs :: Expression e => Bool -> Type -> Type -> [e] -> [e]-filtExprs g a b | g = filterExprs a b- | otherwise = id--\end{code}
MagicHaskeller/ProgramGenerator.lhs view
@@ -65,15 +65,20 @@ data Common = Cmn {opt :: Opt (), tcl :: TyConLib, vl :: VarLib, rt :: RTrie} +mkCommon :: Options -> [Primitive] -> Common+mkCommon opts prims = let+ tyconlib = primitivesToTCL prims+ optunit = forget opts+ in Cmn {opt = optunit, tcl = tyconlib, vl = primitivesToVL tyconlib prims, rt = mkRandTrie (nrands opts) tyconlib (stdgen opts)} +-- | options for limiting the hypothesis space.+type Options = Opt [Primitive]+ 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)---- avail$B$K$7$m(BType$B$K$7$m(Bapply$B$5$l$F$$$k!%(B--- $B$@$+$i$3$=!$(BrunAnotherPS$BE*$K(BemptySubst$B$KBP$7$F<B9T$7$?J}$,8zN(E*$J$O$:!)(B $B$G$b!$(BSubstitution$B$C$F$=$s$J$K$G$+$/$J$i$J$+$C$?$N$G$O!)(BFiniteMap$B$G$b(Bassoc list$B$G$bJQ$o$i$J$+$C$?5$$,!%(B applyDo :: Monad m => ([Type] -> Type -> PriorSubsts m a) -> [Type] -> Type -> PriorSubsts m a
MagicHaskeller/ReadDynamic.hs view
@@ -7,16 +7,20 @@ -- import ReadType import MagicHaskeller.MyDynamic import Language.Haskell.TH-dynS = $(dynamic [|undefined|] [| s :: (b->c->a) -> (b->c) -> b -> a |])-dynK = $(dynamic [|undefined|] [| const :: a->b->a |])-dynI = $(dynamic [|undefined|] [| id :: a->a |])-dynB = $(dynamic [|undefined|] [| (.) :: (c->a) -> (b->c) -> b -> a |])-dynC = $(dynamic [|undefined|] [| flip :: (b->c->a) -> c -> b -> a |])-dynS' = $(dynamic [|undefined|] [| sprime :: (a->b->c)->(d->a)->(d->b)->d->c |])-dynB' = $(dynamic [|undefined|] [| bprime :: (a->b->c)->a->(d->b)->d->c |])-dynC' = $(dynamic [|undefined|] [| cprime :: (a->b->c)->(d->a)->b->d->c |])--- readType assumes the tcl is undefined, so it cannot be used when type constructors other than -> are used.+import MagicHaskeller.TyConLib(defaultTCL)+dynS = $(dynamic [|undefTCL|] [| s :: (b->c->a) -> (b->c) -> b -> a |])+dynK = $(dynamic [|undefTCL|] [| const :: a->b->a |])+dynI = $(dynamic [|undefTCL|] [| id :: a->a |])+dynB = $(dynamic [|undefTCL|] [| (.) :: (c->a) -> (b->c) -> b -> a |])+dynC = $(dynamic [|undefTCL|] [| flip :: (b->c->a) -> c -> b -> a |])+dynS' = $(dynamic [|undefTCL|] [| sprime :: (a->b->c)->(d->a)->(d->b)->d->c |])+dynB' = $(dynamic [|undefTCL|] [| bprime :: (a->b->c)->a->(d->b)->d->c |])+dynC' = $(dynamic [|undefTCL|] [| cprime :: (a->b->c)->(d->a)->b->d->c |])+-- readType assumes the tcl is undefTCL, so it cannot be used when type constructors other than -> are used. s = \f g x -> f x (g x) sprime = (\f g h x -> f (g x) (h x)) bprime = (\f g h x -> f g (h x)) cprime = (\f g h x -> f (g x) h)++-- undefTCL = error "undefTCL" -- This is bad, actually, because we cannot expect laziness to work here, because the tcl is spliced.+undefTCL = defaultTCL
MagicHaskeller/RunAnalytical.hs view
@@ -3,15 +3,20 @@ -- module MagicHaskeller.RunAnalytical(- -- | This module provides with analytical generate-and-test synthesis, i.e. synthesis by filtration of analytically generated (many) expressions.+ -- | This module provides analytically-generate-and-test synthesis, i.e. synthesis by filtration of analytically generated (many) expressions. -- Actions whose name ends with F use random testing filter (like 'MagicHaskeller.filterThenF') in order to reduce the number of expressions.+ --+ -- ATTENTION: This module is supposed to be used under GHCi environment. Currently it is known not to work when executed as an a.out.+ -- Also, this module is tested only on Linux, and does not work with Windows. Another point is that currently functions in this module only+ -- work with known types appearing in 'MagicHaskeller.CoreLang.defaultPrimitives'.+ -- ** Re-exported modules module MagicHaskeller, module MagicHaskeller.ExecuteAPI610, module MagicHaskeller.Analytical, - -- ** Synthesizers which can be used with any types.- - -- | 'filterGet1' and its friends can be used to synthesize one expression satisfying the given condition. For example,+ {-+ -- ** Synthesizers which will be able to be used with any types but currently do not work with unknown types. -- *** All in one actions quickStartC, quickStartCF, + -- | 'filterGet1' and its friends can be used to synthesize one expression satisfying the given condition. For example, -- >>> session <- prepareAPI [] -- >>> filterGet1_ session $(c [d| f [] = 0; f [a] = 1; f [a,b] = 2 |]) (\f -> f "foobar" == 6) -- > \a -> let fa (b@([])) = 0@@ -19,16 +24,20 @@ -- > in fa a filterGet1_, filterGet1, filterGet1BK, -- | Unlike 'filterGet1' and its friends, the following three functions do not print anything but only return results silently.- getFilt, getFiltF, getAll,- -- ** Synthesizers which are easier to use that can be used only with types appearing 'MagicHaskeller.CoreLang.defaultPrimitives'- -- *** All in one actions+ getFilt, getFiltF, getAll, + -}+ + {- -- ** Synthesizers which are easier to use that can be used only with types appearing in 'MagicHaskeller.CoreLang.defaultPrimitives' -}+ -- | All in one actions quickStart, quickStartF, - -- *** counterparts to 'filterGet1_', 'filterGet1', and 'filterGet1BK'+ -- | 'filterGet1' and its friends can be used to synthesize one expression satisfying the given condition. For example,+ {- -- *** counterparts to 'filterGet1_', 'filterGet1', and 'filterGet1BK' -} filterGetOne_, filterGetOne, filterGetOneBK, - -- *** counterparts to 'getFilt', 'getFiltF', and 'getAll'- + -- | Unlike 'filterGetOne' and its friends, the following three functions do not print anything but only return results silently.+ {- -- *** counterparts to 'getFilt', 'getFiltF', and 'getAll' -} synthFilt, synthFiltF, synthAll,- -- *** counterpart to 'noBK'+ {- -- *** counterpart to 'noBK' -}+ -- | 'noBKQ' can be used as the background knowledge for showing that no background knowledge functions are used. noBKQ ) where import MagicHaskeller
MagicHaskeller/TimeOut.hs view
@@ -40,6 +40,9 @@ unsafeWithPTO pto a = unsafePerformIO $ wrapExecution ( maybeWithTO seq pto (return a) )+maybeWithTO :: (a -> IO () -> IO ()) -- ^ seq or deepSeq(=Control.Parallel.Strategies.sforce). For our purposes seq is enough, because @a@ is either 'Bool' or 'Ordering'.+ -> Maybe Int -> IO a -> IO (Maybe a)+maybeWithTO sq mbt action = maybeWithTO' sq mbt (const action) newPTO t = return t #else unsafeWithPTO _ = Just@@ -60,10 +63,6 @@ unsafeEvaluate t e = unsafePerformIO (withTO t (return e)) -- Should I use Control.OldException.evaluate? I do not want to evaluate long lists deeply. -} -maybeWithTO :: (a -> IO () -> IO ()) -- ^ seq or deepSeq(=Control.Parallel.Strategies.sforce). For our purposes seq is enough, because @a@ is either 'Bool' or 'Ordering'.- -> Maybe Int -> IO a -> IO (Maybe a)-maybeWithTO sq mbt action = maybeWithTO' sq mbt (const action)- maybeWithTO' :: (a -> IO () -> IO ()) -> Maybe Int -> ((IO b -> IO b) -> IO a) -> IO (Maybe a) maybeWithTO' _ Nothing action = do a <- action id return (Just a)@@ -103,15 +102,20 @@ -- Catch exceptions such as stack space overflow catchIt :: (SampleVar (Maybe a)) -> IO () -> IO ()+#ifdef SHOWEXCEPTIONS+catchIt sv act = act -- disable+#else catchIt sv act = Control.Exception.catch act (handler sv)--- catchIt sv act = act -- disable+#endif handler sv err = Control.Exception.catch (realHandler sv (err::SomeException)) (handler sv) -- realHandler sv (AsyncException ThreadKilled) = return () -- If the thread is killed by ^C (i.e. not by another thread), sv is left empty. So, the parent thread can catch ^C while waiting.+{- #ifdef REALDYNAMIC -- realHandler sv err = trace (show err) $ writeSampleVar sv Nothing realHandler sv (ErrorCall str) = trace str $ writeSampleVar sv Nothing #endif+-} realHandler sv err = writeSampleVar sv Nothing catchYield tid sv action = Control.Exception.catch (yield >> action) (childHandler tid sv)
MagicHaskeller/TyConLib.hs view
@@ -41,30 +41,7 @@ tupleMax = 0 -} -{--defaultTyCons :: [(TypeName, Kind)]-defaultTyCons = [("()",Star), ("[]",Star::->Star)] ++ [ (tuplename i, intToRank1Kind i) | i<-[2..7] ] ++ [("Char",Star), ("Integer",Star), ("Int",Star), ("Double",Star), ("Float",Star), ("IO",Star::->Star), ("Bool",Star)] -- $B$3$3$K=P$F$/$kE[$,(BVirtual.hs$B$G$b=P$F$/$k$H%(%i!<$K$J$k$N$GCm0U!%(B--- defaultTyCons = [("*","()"), ("* -> *","[]"), --}- tuplename i = '(':replicate (i-1) ',' ++")"-{--intToRank1Kind :: Int -> Kind-intToRank1Kind 0 = Star-intToRank1Kind i = Star ::-> intToRank1Kind (i-1)--- $B$J$k$Y$/$3$$$D$i$r;H$&!%>J%9%Z!<%9$N$?$a!%(Btuples$B$C$F(Blist$B$r:n$k$Y$-(B?--- first-order kind $B$N$[$&$,$?$@$7$+$C$?$h$&$J!#(B-unit = Con 0 "()" Star-list = Con 1 "[]" (Star::->Star)-tuple n = Con (fromIntegral n) (tuplename n) (intToRank1Kind n)--- arrow = Con 2 "(->)" 2--- tuple n = Con (n+1) (tuplename n) n--}-{--unit = Con 0 0-list = Con 1 0-tuple n = Con n 0--} unit tcl = nameToTyCon tcl "()" list tcl = nameToTyCon tcl "[]"
MagicHaskeller/Types.lhs view
@@ -1,18 +1,15 @@ -- -- (c) Susumu Katayama ---Types.lhs: renamed to avoid name clash with package ghc -Oct. 1, 2003; bruteForce/Type.lhs- \begin{code} {-# OPTIONS -cpp -funbox-strict-fields #-} module MagicHaskeller.Types(Type(..), Kind, TyCon, TyVar, TypeName, Class(..), Typed(..), tyvars, Subst, plusSubst, emptySubst, apply, mgu, varBind, match, maxVarID, normalizeVarIDs, normalize, - Decoder(..), typer, typee, negateTVIDs, limitType, quantify, unquantify, lookupSubst, unifyFunAp,- alltyvars, mapTV, size, unitSubst, applyCheck, assertsubst, substOK, eqType, getRet, getArity, splitArgs, getArgs, pushArgs, popArgs, mguFunAp, strToVarType, revSplitArgs, splitArgsCPS, bakaHash+ Decoder(..), typer, typee, negateTVIDs, limitType, quantify, quantify', unquantify, lookupSubst, unifyFunAp,+ alltyvars, mapTV, size, unitSubst, applyCheck, assertsubst, substOK, eqType, getRet, getArity, splitArgs, getArgs, pushArgs, popArgs, mguFunAp, strToVarType, revSplitArgs, revGetArgs, splitArgsCPS, bakaHash ) where import Data.List import Control.Monad@@ -175,7 +172,7 @@ eqType t0 t1 = normalize t0 == normalize t1 --- quantify freezes tyvars into tycons whose tcID's are -tvID, like Tina Yu's approach to synthesis of polymorphic functions.+-- quantify freezes tyvars into tycons whose IDs are negative. quantify, quantify', unquantify :: Type -> Type quantify ty = quantify' (normalize ty) quantify' (TV iD) = TC (-iD-1)@@ -219,7 +216,6 @@ --- moved from MemoStingy.lhs and MemoDeb.lhs pushArgsCPS :: (Int -> [Type] -> Type -> a) -> [Type] -> Type -> a pushArgsCPS f = pa 0 where @@ -245,6 +241,9 @@ revSplitArgs (t0:->t1) = case revSplitArgs t1 of (n,args,ret) -> (n+1, t0:args, ret) revSplitArgs t = (0, [], t) +revGetArgs :: Type -> [Type]+revGetArgs ty = case revSplitArgs ty of (_,ts,_) -> ts+ popArgs :: [Type] -> Type -> Type popArgs = flip (foldl (flip (:->))) @@ -265,6 +264,9 @@ typee (a ::: _) = a typer (_ ::: t) = t +instance Functor Typed where+ fmap f (a ::: t) = f a ::: t+ \end{code} \section{Type inference tools}@@ -283,7 +285,6 @@ -- subst$B$K$/$o$($k$H$-$O(B:>$B$r(B:->$B$K$;$M$P$J$i$J$$$,!"(Bapply s (a:>b)$B$O(Bapply s a :> apply s b match, mgu :: MonadPlus m => Type -> Type -> m Subst --- $B4pK\E*$K!$(BTHIH.match$B$O(Bmerge$B$r;H$C$F$k$N$G?.MQ$7$F$J$$!%(B match (l :-> r) (l' :-> r') = match2Ap l r l' r' {- match (l :-> r) (l' :> r') = match2Ap l r l' r'@@ -320,10 +321,8 @@ varBind :: MonadPlus m => TyVar -> Type -> m Subst varBind u t | t == TV u = return emptySubst- | u `elem` (tyvars t) = mzero -- infinite type--- | u `elementOf` (tyvars t) = mzero -- infinite type -- The above list implementation seems faster.--- | not (t `satisfies` classes u) = mzero -- applyCl is necessary for multi-param classes, but how can I do it?- | otherwise = return (unitSubst u t) -- $B$[$s$H$&$O(Bvar$B$I$&$7(Bbind$B$9$k$H$-$O(Bcontext$B$b$4$&$;$$$;$M$P$J$i$L!#(B+ | u `elem` (tyvars t) = mzero+ | otherwise = return (unitSubst u t) substOK :: Subst -> Bool substOK = all (\ (i,ty) -> not (i `elem` (tyvars ty)))