diff --git a/CEFP/Examples/CodeApplication.hs b/CEFP/Examples/CodeApplication.hs deleted file mode 100644 --- a/CEFP/Examples/CodeApplication.hs +++ /dev/null @@ -1,175 +0,0 @@ -module Main where - -import qualified Prelude -import MuFeldspar.Prelude - -import MuFeldspar.Core -import MuFeldspar.Frontend -import MuFeldspar.Vector - -import Imperative.Imperative -import Imperative.Compiler - -import Data.Word -import Data.Bits (Bits) - - -type VecBool = Vector (Data Bool) - -type VecInt = Vector (Data Int) - --- Primitive Functions (and tuples) - -prog0 :: Data Int -> Data Int -prog0 = (*2) - -prog1 :: (Data Int, Data Int) -> (Data Int, Data Int, Data Int) -prog1 (a,b) = (min a b, a + b, a ^ b) - -prog2 :: Data Int -> Data Int -> (Data Int, Data Int, Data Int) -prog2 a b = (min a b, a + b, a ^ b) - -isEven :: (Type a, Integral a) => Data a -> Data Bool -isEven i = i `mod` 2 == 0 - -swap (a,b) = (b,a) - - --- Conditional - -f :: Data Int -> Data Int -f i = (isEven i) ? (2*i, i) - -t1 = eval (f 3) - -t2 = eval (f 4) - - --- Arrays - -prog3 :: Data [Int] -prog3 = parallel 10 (*2) - -tst1 = eval prog3 - -tst1a = drawFeld prog3 - -tst1b = printFeld prog3 - -tst1c = compile prog3 - -prog4 :: Data [Int] -prog4 = parallel 10 (`mod` 5) - -prog5 :: Data [Int] -prog5 = parallel 10 f - -prog6 :: Data [Int] -prog6 = parallel 10 (<< 3) - -prog7 :: Data [Int] -prog7 = parallel 10 (>> 1) - -prog8 :: Data [Int] -prog8 = parallel 12 (`xor` 3) - - - - -perm f arr = parallel (getLength arr) (\i -> getIx arr (f i)) - -rot arr = perm f arr - where - f i = (i+1) `mod` (getLength arr) - -prog9 :: Data [[Int]] -prog9 = parallel 8 (\i -> parallel i id) - --- Sequential Arrays - -prog10 :: Data [Int] -prog10 = sequential 10 1 g - where - g ix st = (j,j) - where j = (ix + 1) * st - --- for Loop - -prog11 :: Data Int -> Data Int -prog11 k = forLoop k 1 g - where - g ix st = (ix + 1) * st - -composeN :: (Syntax st) => (st -> st) -> Data Length -> st -> st -composeN f l i0 = forLoop l i0 g - where - g _ i = f i - -ccn = compile (composeN ((*2) :: Data Int -> Data Int)) - - - - - --- Vectors - -prog12 :: Vector (Data Int) -prog12 = Indexed 10 (*2) - -tst2 = eval prog11 - -prog13 :: Data Int -prog13 = sum $ Indexed 10 (*2) - - -prog14 :: Vector (Data Int) -prog14 = map (*5) $ Indexed 10 (*2) - -prog15 :: Vector (Data Int) -prog15 = map (*5) . map (+1) $ Indexed 10 (*2) - -scalarProduct :: (Type a, Num a) => Vector (Data a) -> Vector (Data a) -> Data a -scalarProduct as bs = sum $ zipWith (*) as bs - - -forceEx as bs = (sum . force) $ zipWith (*) as bs - -prog16 :: Data Int -> Data Int -prog16 a = sum $ (isEven a) ? (prog14, prog15) - - - - - -sumEven :: VecInt -> Data Int -sumEven = sum . map zeroOutOdd - where - zeroOutOdd x = (testBit x 0) ? (0,x) - -{-- -*Main> eval $ sumEven (value [1..10]) -30 ---} - - - - - -testBit :: (Type a, Bits a) => Data a -> Data Index -> Data Bool -testBit l i = not ((l .&. (1< Data Int -> VecBool -int2BLN n v = reverse $ indexed n (testBit v) - -int2BL :: (Type a, Bits a) => Data a -> VecBool -int2BL l = reverse $ indexed (bitSize l) (testBit l) - - - -dft :: Vector (Data Complex) -> Vector (Data Complex) -dft v = Indexed l ixf - where - l = length v - ixf i = scalarProduct v (ts i) - ts k = indexed l f - where f i = cis $ (-2 * (value pi) * (i2n i) * (i2n k)) / (i2n l) diff --git a/CEFP/Examples/ExProg.hs b/CEFP/Examples/ExProg.hs deleted file mode 100644 --- a/CEFP/Examples/ExProg.hs +++ /dev/null @@ -1,894 +0,0 @@ -module Main where - -import qualified Prelude -import MuFeldspar.Prelude - -import MuFeldspar.Core -import MuFeldspar.Frontend -import MuFeldspar.Vector - -import Imperative.Imperative -import Imperative.Compiler - -import Data.Word -import Data.Bits (Bits) - - -type VecBool = Vector (Data Bool) - -type VecInt = Vector (Data Int) - --- Primitive Functions (and tuples) - -prog0 :: Data Int -> Data Int -prog0 = (*2) - -prog1 :: (Data Int, Data Int) -> (Data Int, Data Int, Data Int) -prog1 (a,b) = (min a b, a + b, a ^ b) - -prog2 :: Data Int -> Data Int -> (Data Int, Data Int, Data Int) -prog2 a b = (min a b, a + b, a ^ b) - -isEven :: (Type a, Integral a) => Data a -> Data Bool -isEven i = i `mod` 2 == 0 - -swap (a,b) = (b,a) - - --- Conditional - -f :: Data Int -> Data Int -f i = (isEven i) ? (2*i, i) - -t1 = eval (f 3) - -t2 = eval (f 4) - - --- Arrays - -prog3 :: Data [Int] -prog3 = parallel 10 (*2) - -tst1 = eval prog3 - -tst1a = drawFeld prog3 - -tst1b = printFeld prog3 - -tst1c = compile prog3 - -prog4 :: Data [Int] -prog4 = parallel 10 (`mod` 5) - -prog5 :: Data [Int] -prog5 = parallel 10 f - -prog6 :: Data [Int] -prog6 = parallel 10 (<< 3) - -prog7 :: Data [Int] -prog7 = parallel 10 (>> 1) - -prog8 :: Data [Int] -prog8 = parallel 12 (`xor` 3) - - - - -perm f arr = parallel (getLength arr) (\i -> getIx arr (f i)) - -rot arr = perm f arr - where - f i = (i+1) `mod` (getLength arr) - -prog9 :: Data [[Int]] -prog9 = parallel 8 (\i -> parallel i id) - --- Sequential Arrays - -prog10 :: Data [Int] -prog10 = sequential 10 1 g - where - g ix st = (j,j) - where j = (ix + 1) * st - --- for Loop - -prog11 :: Data Int -> Data Int -prog11 k = forLoop k 1 g - where - g ix st = (ix + 1) * st - -composeN :: (Syntax st) => (st -> st) -> Data Length -> st -> st -composeN f l i0 = forLoop l i0 g - where - g _ i = f i - -ccn = compile (composeN ((*2) :: Data Int -> Data Int)) - - - - - --- Vectors - -prog12 :: Vector (Data Int) -prog12 = Indexed 10 (*2) - -tst2 = eval prog11 - -prog13 :: Data Int -prog13 = sum $ Indexed 10 (*2) - - -prog14 :: Vector (Data Int) -prog14 = map (*5) $ Indexed 10 (*2) - -prog15 :: Vector (Data Int) -prog15 = map (*5) . map (+1) $ Indexed 10 (*2) - -scalarProduct :: (Type a, Num a) => Vector (Data a) -> Vector (Data a) -> Data a -scalarProduct as bs = sum $ zipWith (*) as bs - - -forceEx as bs = (sum . force) $ zipWith (*) as bs - -prog16 :: Data Int -> Data Int -prog16 a = sum $ (isEven a) ? (prog14, prog15) - - - - - -sumEven :: VecInt -> Data Int -sumEven = sum . map zeroOutOdd - where - zeroOutOdd x = (testBit x 0) ? (0,x) - -{-- -*Main> eval $ sumEven (value [1..10]) -30 ---} - - - - -tri :: (Syntax a) => (a -> a) -> Vector a -> Vector a -tri f (Indexed len ixf) = (indexed len ixf') - where - ixf' i = composeN f i (ixf i) - -ctri = compile (tri ((*2) :: Data Int -> Data Int)) - - -testBit :: (Type a, Bits a) => Data a -> Data Index -> Data Bool -testBit l i = not ((l .&. (1< Data a -> VecBool -int2BL l = reverse $ indexed (bitSize l) (testBit l) - - -int2BLN :: Data Length -> Data Int -> VecBool -int2BLN n v = reverse $ indexed n (testBit v) - - -pows2 :: Data Length -> Vector (Data Index) -pows2 k = Indexed k (1<<) - -bL2Int :: VecBool -> Data Int -bL2Int bs = scalarProduct (reverse (map b2i bs)) (pows2 (length bs)) - -bL2Int' :: VecBool -> Data Int -bL2Int' = sum . tri (*2) . map b2i - -oneBitsN :: Data Index -> Data Index -oneBitsN = complement . zeroBitsN - -zeroBitsN :: Data Index -> Data Index -zeroBitsN = shiftL allOnes - -allOnes :: Data Index -allOnes = complement 0 - - - -xorBool :: Data Bool -> Data Bool -> Data Bool -xorBool a b = not (a == b) - -pad :: Data Length -> VecBool -> VecBool -pad l v = (replicate (l - length v) false) ++ v - -crcAdd :: VecBool -> VecBool -> VecBool -crcAdd as bs = zipWith xorBool (pad m as) (pad m bs) - where - m = max (length as) (length bs) - - - - -simpleCRC :: VecBool -> VecBool -> VecBool -simpleCRC poly msg = fst $ composeN step (l+w) (fw, msg ++ fw) - where - w = length poly - fw = replicate w false - l = length msg - step (reg,ms) = (reg',tlms) - where - reg' = (index reg 0) ? (zipWith xorBool poly r1, r1) - (hms,tlms) = splitAt 1 ms - r1 = drop 1 reg ++ hms - -simpleCRC1 :: VecBool -> VecBool -> VecBool -simpleCRC1 poly msg = fst $ composeN step (length augmsg) (fw,0) - where - w = length poly - fw = replicate w false - augmsg = msg ++ fw - step (reg,i) = (reg',i+1) - where - reg' = (index reg 0) ? (zipWith xorBool poly r1, r1) - r1 = drop 1 reg ++ replicate 1 (index augmsg i) - -simpleCRC2 :: VecBool -> VecBool -> VecBool -simpleCRC2 poly msg = forLoop (length augmsg) fw step - where - w = length poly - fw = replicate w false - augmsg = msg ++ fw - step i reg = reg' - where - reg' = (index reg 0) ? (zipWith xorBool poly r1, r1) - r1 = drop 1 reg ++ replicate 1 (index augmsg i) - - -crc16ccitt :: Data Word16 -crc16ccitt = value 0x1021 - -crc32ieee :: Data Word32 -crc32ieee = value 0x04C11DB7 - -tst4 = eval $ int2BL crc16ccitt - -tstSimpleCRC = eval $ simpleCRC2 (int2BL crc16ccitt) (int2BL (8856 :: Data Word64)) - -{-- -*Main> tstSimpleCRC -[False,True,True,False,False,False,True,False,False,False,True,True,False,True,False,True] ---} - -tstSimpleCRCAgain = eval $ simpleCRC2 (int2BL crc16ccitt) (int2BL (8856 :: Data Word64) ++ value [False,True,True,False,False,False,True,False,False,False,True,True,False,True,False,True]) - -{-- -*Main> tstSimpleCRCAgain -[False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False] ---} - -table :: (Bits a, Type a) => Data a -> Data Index -> Data [a] -table poly size = parallel (2^size) (calc poly size) - - -calc :: (Bits a, Type a) => Data a -> Data Index -> Data Index -> Data a -calc poly size i = i2n $ bL2Int $ simpleCRC1 (int2BL poly) (int2BLN size i) - - -mTable :: (Type a, Bits a) => Data a -> Data Index -> Data Index -> Data [a] -mTable poly size i = parallel (2^size) (\j -> calc poly (j `shiftL` (8*i)) size) - -calc1 :: Data Index -> Data [Word32] -calc1 i = parallel 256 (\j -> tableCRCModCh (bytesR (j `shiftL` (8*i)))) - -table32 :: Data [Word32] -table32 = table crc32ieee 8 - -table16 :: Data [Word16] -table16 = table crc16ccitt 8 - -tstTab16 = eval $ table16 - -{-- -*Main> tstTab16 -[0,4129,8258,12387,16516,20645,24774,28903,33032,37161,41290,45419,49548,53677,5 -7806,61935,4657,528,12915,8786,21173,17044,29431,25302,37689,33560,45947,41818,5 -4205,50076,62463,58334,9314,13379,1056,5121,25830,29895,17572,21637,42346,46411, -34088,38153,58862,62927,50604,54669,13907,9842,5649,1584,30423,26358,22165,18100 -,46939,42874,38681,34616,63455,59390,55197,51132,18628,22757,26758,30887,2112,62 -41,10242,14371,51660,55789,59790,63919,35144,39273,43274,47403,23285,19156,31415 -,27286,6769,2640,14899,10770,56317,52188,64447,60318,39801,35672,47931,43802,278 -14,31879,19684,23749,11298,15363,3168,7233,60846,64911,52716,56781,44330,48395,3 -6200,40265,32407,28342,24277,20212,15891,11826,7761,3696,65439,61374,57309,53244 -,48923,44858,40793,36728,37256,33193,45514,41451,53516,49453,61774,57711,4224,16 -1,12482,8419,20484,16421,28742,24679,33721,37784,41979,46042,49981,54044,58239,6 -2302,689,4752,8947,13010,16949,21012,25207,29270,46570,42443,38312,34185,62830,5 -8703,54572,50445,13538,9411,5280,1153,29798,25671,21540,17413,42971,47098,34713, -38840,59231,63358,50973,55100,9939,14066,1681,5808,26199,30326,17941,22068,55628 -,51565,63758,59695,39368,35305,47498,43435,22596,18533,30726,26663,6336,2273,144 -66,10403,52093,56156,60223,64286,35833,39896,43963,48026,19061,23124,27191,31254 -,2801,6864,10931,14994,64814,60687,56684,52557,48554,44427,40424,36297,31782,276 -55,23652,19525,15522,11395,7392,3265,61215,65342,53085,57212,44955,49082,36825,4 -0952,28183,32310,20053,24180,11923,16050,3793,7920] ---} - -tab16 = value [0,4129,8258,12387,16516,20645,24774,28903,33032,37161,41290,45419,49548,53677,57806,61935,4657,528,12915,8786,21173,17044,29431,25302,37689,33560,45947,41818,54205,50076,62463,58334,9314,13379,1056,5121,25830,29895,17572,21637,42346,46411,34088,38153,58862,62927,50604,54669,13907,9842,5649,1584,30423,26358,22165,18100,46939,42874,38681,34616,63455,59390,55197,51132,18628,22757,26758,30887,2112,6241,10242,14371,51660,55789,59790,63919,35144,39273,43274,47403,23285,19156,31415,27286,6769,2640,14899,10770,56317,52188,64447,60318,39801,35672,47931,43802,27814,31879,19684,23749,11298,15363,3168,7233,60846,64911,52716,56781,44330,48395,36200,40265,32407,28342,24277,20212,15891,11826,7761,3696,65439,61374,57309,53244,48923,44858,40793,36728,37256,33193,45514,41451,53516,49453,61774,57711,4224,161,12482,8419,20484,16421,28742,24679,33721,37784,41979,46042,49981,54044,58239,62302,689,4752,8947,13010,16949,21012,25207,29270,46570,42443,38312,34185,62830,58703,54572,50445,13538,9411,5280,1153,29798,25671,21540,17413,42971,47098,34713,38840,59231,63358,50973,55100,9939,14066,1681,5808,26199,30326,17941,22068,55628,51565,63758,59695,39368,35305,47498,43435,22596,18533,30726,26663,6336,2273,14466,10403,52093,56156,60223,64286,35833,39896,43963,48026,19061,23124,27191,31254,2801,6864,10931,14994,64814,60687,56684,52557,48554,44427,40424,36297,31782,27655,23652,19525,15522,11395,7392,3265,61215,65342,53085,57212,44955,49082,36825,40952,28183,32310,20053,24180,11923,16050,3793,7920] :: Data [Word16] - -tstTab32 = eval $ table32 - -{-- -*Main> tstTab32 -[0,79764919,159529838,222504665,319059676,398814059,445009330,507990021,63811935 -2,583659535,797628118,726387553,890018660,835552979,1015980042,944750013,1276238 -704,1221641927,1167319070,1095957929,1595256236,1540665371,1452775106,1381403509 -,1780037320,1859660671,1671105958,1733955601,2031960084,2111593891,1889500026,19 -52343757,2552477408,2632100695,2443283854,2506133561,2334638140,2414271883,21919 -15858,2254759653,3190512472,3135915759,3081330742,3009969537,2905550212,28509594 -11,2762807018,2691435357,3560074640,3505614887,3719321342,3648080713,3342211916, -3287746299,3467911202,3396681109,4063920168,4143685023,4223187782,4286162673,377 -9000052,3858754371,3904687514,3967668269,881225847,809987520,1023691545,96923409 -4,662832811,591600412,771767749,717299826,311336399,374308984,453813921,53357647 -0,25881363,88864420,134795389,214552010,2023205639,2086057648,1897238633,1976864 -222,1804852699,1867694188,1645340341,1724971778,1587496639,1516133128,1461550545 -,1406951526,1302016099,1230646740,1142491917,1087903418,2896545431,2825181984,27 -70861561,2716262478,3215044683,3143675388,3055782693,3001194130,2326604591,23894 -56536,2200899649,2280525302,2578013683,2640855108,2418763421,2498394922,37699005 -19,3832873040,3912640137,3992402750,4088425275,4151408268,4197601365,4277358050, -3334271071,3263032808,3476998961,3422541446,3585640067,3514407732,3694837229,364 -0369242,1762451694,1842216281,1619975040,1682949687,2047383090,2127137669,193846 -8188,2001449195,1325665622,1271206113,1183200824,1111960463,1543535498,148906962 -9,1434599652,1363369299,622672798,568075817,748617968,677256519,907627842,853037 -301,1067152940,995781531,51762726,131386257,177728840,240578815,269590778,349224 -269,429104020,491947555,4046411278,4126034873,4172115296,4234965207,3794477266,3 -874110821,3953728444,4016571915,3609705398,3555108353,3735388376,3664026991,3290 -680682,3236090077,3449943556,3378572211,3174993278,3120533705,3032266256,2961025 -959,2923101090,2868635157,2813903052,2742672763,2604032198,2683796849,2461293480 -,2524268063,2284983834,2364738477,2175806836,2238787779,1569362073,1498123566,14 -09854455,1355396672,1317987909,1246755826,1192025387,1137557660,2072149281,21351 -22070,1912620623,1992383480,1753615357,1816598090,1627664531,1707420964,29539018 -5,358241886,404320391,483945776,43990325,106832002,186451547,266083308,932423249 -,861060070,1041341759,986742920,613929101,542559546,756411363,701822548,33161969 -85,3244833742,3425377559,3370778784,3601682597,3530312978,3744426955,3689838204, -3819031489,3881883254,3928223919,4007849240,4037393693,4100235434,4180117107,425 -9748804,2310601993,2373574846,2151335527,2231098320,2596047829,2659030626,247035 -9227,2550115596,2947551409,2876312838,2788305887,2733848168,3165939309,309470716 -2,3040238851,2985771188] ---} - -tab32 = value [0,79764919,159529838,222504665,319059676,398814059,445009330,507990021,638119352,583659535,797628118,726387553,890018660,835552979,1015980042,944750013,1276238704,1221641927,1167319070,1095957929,1595256236,1540665371,1452775106,1381403509,1780037320,1859660671,1671105958,1733955601,2031960084,2111593891,1889500026,1952343757,2552477408,2632100695,2443283854,2506133561,2334638140,2414271883,2191915858,2254759653,3190512472,3135915759,3081330742,3009969537,2905550212,2850959411,2762807018,2691435357,3560074640,3505614887,3719321342,3648080713,3342211916,3287746299,3467911202,3396681109,4063920168,4143685023,4223187782,4286162673,3779000052,3858754371,3904687514,3967668269,881225847,809987520,1023691545,969234094,662832811,591600412,771767749,717299826,311336399,374308984,453813921,533576470,25881363,88864420,134795389,214552010,2023205639,2086057648,1897238633,1976864222,1804852699,1867694188,1645340341,1724971778,1587496639,1516133128,1461550545,1406951526,1302016099,1230646740,1142491917,1087903418,2896545431,2825181984,2770861561,2716262478,3215044683,3143675388,3055782693,3001194130,2326604591,2389456536,2200899649,2280525302,2578013683,2640855108,2418763421,2498394922,3769900519,3832873040,3912640137,3992402750,4088425275,4151408268,4197601365,4277358050,3334271071,3263032808,3476998961,3422541446,3585640067,3514407732,3694837229,3640369242,1762451694,1842216281,1619975040,1682949687,2047383090,2127137669,1938468188,2001449195,1325665622,1271206113,1183200824,1111960463,1543535498,1489069629,1434599652,1363369299,622672798,568075817,748617968,677256519,907627842,853037301,1067152940,995781531,51762726,131386257,177728840,240578815,269590778,349224269,429104020,491947555,4046411278,4126034873,4172115296,4234965207,3794477266,3874110821,3953728444,4016571915,3609705398,3555108353,3735388376,3664026991,3290680682,3236090077,3449943556,3378572211,3174993278,3120533705,3032266256,2961025959,2923101090,2868635157,2813903052,2742672763,2604032198,2683796849,2461293480,2524268063,2284983834,2364738477,2175806836,2238787779,1569362073,1498123566,1409854455,1355396672,1317987909,1246755826,1192025387,1137557660,2072149281,2135122070,1912620623,1992383480,1753615357,1816598090,1627664531,1707420964,295390185,358241886,404320391,483945776,43990325,106832002,186451547,266083308,932423249,861060070,1041341759,986742920,613929101,542559546,756411363,701822548,3316196985,3244833742,3425377559,3370778784,3601682597,3530312978,3744426955,3689838204,3819031489,3881883254,3928223919,4007849240,4037393693,4100235434,4180117107,4259748804,2310601993,2373574846,2151335527,2231098320,2596047829,2659030626,2470359227,2550115596,2947551409,2876312838,2788305887,2733848168,3165939309,3094707162,3040238851,2985771188] :: Data [Word32] - -leftByte :: (Bits a, Type a, Integral a) => Data a -> Data Index -leftByte a = i2n $ (a `shiftR` (bitSize a - 8)) .&. 0xFF - -byteIn :: (Bits a, Type a, Integral a) => Data Word8 -> Data a -> Data a -byteIn b w = w `shiftL` 8 .|. i2n b - - -tableCRC :: (Bits a, Type a, Integral a) => - Data a -> Vector (Data Word8) -> Data a -tableCRC poly msg = forLoop (length augmsg) 0 step - where - augmsg = msg ++ replicate ((bitSize poly) `div` 8) 0 - step i reg - = byteIn (index augmsg i) reg `xor` getIx (table poly 8) (leftByte reg) - - -tableCRC1 :: (Bits a, Type a, Integral a) => - Data a -> Vector (Data Word8) -> Data a -tableCRC1 poly msg = share (value (eval (table poly 8))) $ \tab -> - forLoop (length augmsg) 0 (step tab) - where - augmsg = msg ++ replicate ((bitSize poly) `div` 8) 0 - step tab i reg - = byteIn (index augmsg i) reg `xor` getIx tab (leftByte reg) - -tstTabCRC = compile $ tableCRC1 crc16ccitt - -{-- -main (v0) - v1 := [0,4129,8258,12387,16516,20645,24774,28903,33032,37161,41290,45419,49548 -,53677,57806,61935,4657,528,12915,8786,21173,17044,29431,25302,37689,33560,45947 -,41818,54205,50076,62463,58334,9314,13379,1056,5121,25830,29895,17572,21637,4234 -6,46411,34088,38153,58862,62927,50604,54669,13907,9842,5649,1584,30423,26358,221 -65,18100,46939,42874,38681,34616,63455,59390,55197,51132,18628,22757,26758,30887 -,2112,6241,10242,14371,51660,55789,59790,63919,35144,39273,43274,47403,23285,191 -56,31415,27286,6769,2640,14899,10770,56317,52188,64447,60318,39801,35672,47931,4 -3802,27814,31879,19684,23749,11298,15363,3168,7233,60846,64911,52716,56781,44330 -,48395,36200,40265,32407,28342,24277,20212,15891,11826,7761,3696,65439,61374,573 -09,53244,48923,44858,40793,36728,37256,33193,45514,41451,53516,49453,61774,57711 -,4224,161,12482,8419,20484,16421,28742,24679,33721,37784,41979,46042,49981,54044 -,58239,62302,689,4752,8947,13010,16949,21012,25207,29270,46570,42443,38312,34185 -,62830,58703,54572,50445,13538,9411,5280,1153,29798,25671,21540,17413,42971,4709 -8,34713,38840,59231,63358,50973,55100,9939,14066,1681,5808,26199,30326,17941,220 -68,55628,51565,63758,59695,39368,35305,47498,43435,22596,18533,30726,26663,6336, -2273,14466,10403,52093,56156,60223,64286,35833,39896,43963,48026,19061,23124,271 -91,31254,2801,6864,10931,14994,64814,60687,56684,52557,48554,44427,40424,36297,3 -1782,27655,23652,19525,15522,11395,7392,3265,61215,65342,53085,57212,44955,49082 -,36825,40952,28183,32310,20053,24180,11923,16050,3793,7920] :: [Word16] - x3 := v0 - x2 := (arrLength x3) - x6 := 4129 :: Word16 - x5 := (bitSize x6) - x7 := 8 :: Int - x4 := (div x5 x7) - x1 := (x2 + x4) - x8 := 0 :: Word16 - x9 := 0 :: Int - v3 := (tup2 x8 x9) - - for v2 in 0 .. (x1-1) do - x14 := v3 - x13 := (sel1 x14) - x15 := 8 :: Int - x12 := (shiftL x13 x15) - x20 := v3 - x19 := (sel2 x20) - x22 := v0 - x21 := (arrLength x22) - x18 := (x19 < x21) - - if x18 then - x23 := v0 - x25 := v3 - x24 := (sel2 x25) - x17 := (getIx x23 x24) - else - x17 := 0 :: Word8 - x16 := (i2n x17) - x11 := (x12 .|. x16) - x27 := v1 - x32 := v3 - x31 := (sel1 x32) - x36 := v3 - x35 := (sel1 x36) - x34 := (bitSize x35) - x37 := 8 :: Int - x33 := (x34 - x37) - x30 := (shiftR x31 x33) - x38 := 255 :: Word16 - x29 := (x30 .&. x38) - x28 := (i2n x29) - x26 := (getIx x27 x28) - x10 := (xor x11 x26) - x41 := v3 - x40 := (sel2 x41) - x42 := 1 :: Int - x39 := (x40 + x42) - v3 := (tup2 x10 x39) - x0 := v3 - out := (sel1 x0) ---} - - -tableCRC2 :: Vector (Data Word8) -> Data Word16 -tableCRC2 msg = share tab16 $ \tab -> fst (composeN (step tab) (length augmsg) (0,0)) - where - augmsg = msg ++ replicate 2 0 - step tab (reg, i) = (byteIn (index augmsg i) reg `xor` getIx tab (leftByte reg), i+1) - - -tstFastTab = compile tableCRC2 - -tableCRC3 :: Vector (Data Word8) -> Data Word32 -tableCRC3 msg = share tab32 $ \tab -> fst (composeN (step tab) (length augmsg) (0,0)) - where - augmsg = msg ++ replicate 4 0 - step tab (reg, i) = (byteIn (index augmsg i) reg `xor` getIx tab (leftByte reg), i+1) - - -tableCRCMod :: (Bits a, Type a, Integral a) => - Data a -> Vector (Data Word8) -> Data a -tableCRCMod poly msg = share (value (eval (table poly 8))) $ \tab -> - forLoop (length msg) 0 (step tab) - where - step tab i reg - = reg `shiftL` 8 `xor` getIx tab (leftByte reg `xor` i2n (index msg i)) - -tableCRCModCh :: Vector (Data Word8) -> Data Word32 -tableCRCModCh msg = share tab32 $ \tab -> forLoop (length msg) 0 (step tab) - where - step tab i reg - = reg `shiftL` 8 `xor` getIx tab (leftByte reg `xor` i2n (index msg i)) - -tstModTab = compile $ tableCRCMod crc16ccitt - -{-- -main (v0) - v1 := [0,4129,8258,12387,16516,20645,24774,28903,33032,37161,41290,45419,49548 -,53677,57806,61935,4657,528,12915,8786,21173,17044,29431,25302,37689,33560,45947 -,41818,54205,50076,62463,58334,9314,13379,1056,5121,25830,29895,17572,21637,4234 -6,46411,34088,38153,58862,62927,50604,54669,13907,9842,5649,1584,30423,26358,221 -65,18100,46939,42874,38681,34616,63455,59390,55197,51132,18628,22757,26758,30887 -,2112,6241,10242,14371,51660,55789,59790,63919,35144,39273,43274,47403,23285,191 -56,31415,27286,6769,2640,14899,10770,56317,52188,64447,60318,39801,35672,47931,4 -3802,27814,31879,19684,23749,11298,15363,3168,7233,60846,64911,52716,56781,44330 -,48395,36200,40265,32407,28342,24277,20212,15891,11826,7761,3696,65439,61374,573 -09,53244,48923,44858,40793,36728,37256,33193,45514,41451,53516,49453,61774,57711 -,4224,161,12482,8419,20484,16421,28742,24679,33721,37784,41979,46042,49981,54044 -,58239,62302,689,4752,8947,13010,16949,21012,25207,29270,46570,42443,38312,34185 -,62830,58703,54572,50445,13538,9411,5280,1153,29798,25671,21540,17413,42971,4709 -8,34713,38840,59231,63358,50973,55100,9939,14066,1681,5808,26199,30326,17941,220 -68,55628,51565,63758,59695,39368,35305,47498,43435,22596,18533,30726,26663,6336, -2273,14466,10403,52093,56156,60223,64286,35833,39896,43963,48026,19061,23124,271 -91,31254,2801,6864,10931,14994,64814,60687,56684,52557,48554,44427,40424,36297,3 -1782,27655,23652,19525,15522,11395,7392,3265,61215,65342,53085,57212,44955,49082 -,36825,40952,28183,32310,20053,24180,11923,16050,3793,7920] :: [Word16] - x1 := v0 - x0 := (arrLength x1) - v3 := 0 :: Word16 - - for v2 in 0 .. (x0-1) do - x3 := v3 - x4 := 8 :: Int - x2 := (shiftL x3 x4) - x6 := v1 - x11 := v3 - x14 := v3 - x13 := (bitSize x14) - x15 := 8 :: Int - x12 := (x13 - x15) - x10 := (shiftR x11 x12) - x16 := 255 :: Word16 - x9 := (x10 .&. x16) - x8 := (i2n x9) - x19 := v0 - x20 := v2 - x18 := (getIx x19 x20) - x17 := (i2n x18) - x7 := (xor x8 x17) - x5 := (getIx x6 x7) - v3 := (xor x2 x5) - out := v3 ---} - -bytes :: (Bits t, Type t, Integral t) => Data t -> Vector (Data Word8) -bytes w = map i2n (Indexed l ixf) - where - ixf k = (w `shiftR` (8*k)) .&. 0xFF - l = numBytes w - - -bytesR :: (Bits t, Type t, Integral t) => Data t -> Vector (Data Word8) -bytesR w = map i2n (Indexed l ixf) - where - ixf k = (w `shiftR` (8*(l-1-k))) .&. 0xFF - l = numBytes w - -numBytes :: (Bits t, Type t, Integral t) => Data t -> Data Index -numBytes a = (bitSize a) `div` 8 - - -m1 = eval $ tableCRCMod crc32ieee (value [1..20]) - -{-- -*Main> m1 -3245827117 ---} - -m2 = eval $ tableCRCMod crc32ieee (value [1..20] ++ bytesR (3245827117 :: Data Word32)) - -{-- -*Main> m2 -0 ---} - -sliceCRC :: (Type a, Bits a, Integral a) => - Data a -> Vector (Data a) -> Data a -sliceCRC poly msg = share (value (eval (parallel n (mTable poly 8)))) $ \tab -> - forLoop (length msg) 0 (step tab) - where - n = numBytes poly - step tab i reg = fold xor 0 $ g . bytes $ reg `xor` w1 - where - w1 = index msg i - g (Indexed len ixf) = Indexed len ixf' - where - ixf' j = getIx (getIx tab j) (i2n (ixf j)) - - - - -m3 = eval $ sliceCRC crc16ccitt (value [1..5]) - - -sliceCRC' :: Vector (Data Word32) -> Data Word32 -sliceCRC' msg = share (value (eval (parallel 4 calc1))) $ \tab -> - forLoop (length msg) 0 (step tab) - where - step tab i reg = fold xor 0 $ g . bytes $ reg `xor` w1 - where - w1 = index msg i - g (Indexed len ixf) = Indexed len ixf' - where - ixf' j = getIx (getIx tab j) (i2n (ixf j)) - - -fold1 :: (Syntax a) => (a -> a -> a) -> Vector a -> a -fold1 f as = fold f (index as 0) (drop 1 as) - -m4 = eval $ sliceCRC' (value [1..100]) -{-- -*Main> m4 -3886779157 ---} - -m5 = eval $ sliceCRC' (value [1..5] ++ replicate 1 3886779157) - -m6 = eval $ sliceCRC' (value [1..100] ++ replicate 1 4076606085) - -{-- -main (v0) - v1 := [[0,79764919,159529838,222504665,319059676,398814059,445009330,507990021 -,638119352,583659535,797628118,726387553,890018660,835552979,1015980042,94475001 -3,1276238704,1221641927,1167319070,1095957929,1595256236,1540665371,1452775106,1 -381403509,1780037320,1859660671,1671105958,1733955601,2031960084,2111593891,1889 -500026,1952343757,2552477408,2632100695,2443283854,2506133561,2334638140,2414271 -883,2191915858,2254759653,3190512472,3135915759,3081330742,3009969537,2905550212 -,2850959411,2762807018,2691435357,3560074640,3505614887,3719321342,3648080713,33 -42211916,3287746299,3467911202,3396681109,4063920168,4143685023,4223187782,42861 -62673,3779000052,3858754371,3904687514,3967668269,881225847,809987520,1023691545 -,969234094,662832811,591600412,771767749,717299826,311336399,374308984,453813921 -,533576470,25881363,88864420,134795389,214552010,2023205639,2086057648,189723863 -3,1976864222,1804852699,1867694188,1645340341,1724971778,1587496639,1516133128,1 -461550545,1406951526,1302016099,1230646740,1142491917,1087903418,2896545431,2825 -181984,2770861561,2716262478,3215044683,3143675388,3055782693,3001194130,2326604 -591,2389456536,2200899649,2280525302,2578013683,2640855108,2418763421,2498394922 -,3769900519,3832873040,3912640137,3992402750,4088425275,4151408268,4197601365,42 -77358050,3334271071,3263032808,3476998961,3422541446,3585640067,3514407732,36948 -37229,3640369242,1762451694,1842216281,1619975040,1682949687,2047383090,21271376 -69,1938468188,2001449195,1325665622,1271206113,1183200824,1111960463,1543535498, -1489069629,1434599652,1363369299,622672798,568075817,748617968,677256519,9076278 -42,853037301,1067152940,995781531,51762726,131386257,177728840,240578815,2695907 -78,349224269,429104020,491947555,4046411278,4126034873,4172115296,4234965207,379 -4477266,3874110821,3953728444,4016571915,3609705398,3555108353,3735388376,366402 -6991,3290680682,3236090077,3449943556,3378572211,3174993278,3120533705,303226625 -6,2961025959,2923101090,2868635157,2813903052,2742672763,2604032198,2683796849,2 -461293480,2524268063,2284983834,2364738477,2175806836,2238787779,1569362073,1498 -123566,1409854455,1355396672,1317987909,1246755826,1192025387,1137557660,2072149 -281,2135122070,1912620623,1992383480,1753615357,1816598090,1627664531,1707420964 -,295390185,358241886,404320391,483945776,43990325,106832002,186451547,266083308, -932423249,861060070,1041341759,986742920,613929101,542559546,756411363,701822548 -,3316196985,3244833742,3425377559,3370778784,3601682597,3530312978,3744426955,36 -89838204,3819031489,3881883254,3928223919,4007849240,4037393693,4100235434,41801 -17107,4259748804,2310601993,2373574846,2151335527,2231098320,2596047829,26590306 -26,2470359227,2550115596,2947551409,2876312838,2788305887,2733848168,3165939309, -3094707162,3040238851,2985771188],[0,3524903388,2700254735,1928028115,1159995817 -,2537414773,3856056230,936345210,2319991634,1481736846,716889437,4171439233,3479 -986939,494248743,1872690420,3179756840,273783571,3259521743,2963473692,165640723 -2,1433778874,2272033638,4119274677,664724841,2585385025,1207966109,988497486,390 -8208530,3745380840,220477492,2144298983,2916525627,547567142,4072339450,21528351 -13,1380477429,1703352207,3080640083,3312814464,392972380,2867557748,2029171880,1 -69470843,3623889575,4023342301,1037473025,1329449682,2636385038,821210421,380707 -9657,2415932218,1108996838,1976994972,2815380800,3575911059,121492303,3132812903 -,1755525051,440954984,3360797108,4288597966,763825682,1600934337,2373292061,1095 -134284,2472521104,3786732099,866988959,73551333,3598421049,2760954858,1988694582 -,3406704414,420998850,1811722513,3118821581,2385120951,1546899307,785944760,4240 -527716,1360525151,2198746755,4058343760,603760780,338941686,3324647210,303256600 -9,1725466917,3680482317,155612625,2074946050,2847206366,2658899364,1281512568,10 -49168811,3968911991,1642420842,3019676598,3239560293,319686073,616659907,4141398 -559,2217993676,1445602320,3953989944,968153316,1264551735,2571519723,2928228497, -2089875789,242984606,3697436482,1907671417,2746024101,3511050102,56598186,881909 -968,3867746572,2489482975,1182514947,4227629611,702890999,1527651364,2300042744, -3201868674,1824612958,506084749,3425958993,2190268568,1351948612,578700951,40333 -16683,3349739825,363935981,1733977918,3041109730,147102666,3671939606,2822112709 -,2049950745,1306573411,2683927487,3977389164,1057744304,2463974283,1086620247,84 -1997700,3761642584,3623445026,98608126,1997274157,2769436145,412418265,339822208 -5,3093798614,1786666762,1571889520,2410209452,4249075583,794459811,2721050302,18 -82599266,48066737,3502551405,3876310807,890375883,1207521560,2514522308,67788337 -2,4202589232,2291479523,1519186495,1833143365,3210366361,3450933834,531157910,29 -94632109,1617409137,311225250,3231001214,4149892100,625186264,1470679563,2242972 -631,943077119,3929012003,2563025136,1256024364,2098337622,2936788618,3722479961, -267995269,3284841684,299070728,1664625371,2971790087,2263782781,1425495201,63937 -2146,4094020270,1233319814,2610640474,3916458377,996780117,212260399,3737065459, -2891204640,2119010812,3550162887,25357851,1936306632,2708500500,2529103470,11517 -82834,911052897,3830731197,1507028117,2345315657,4179751578,725103430,485969212, -3471740128,3154498355,1847333615,3815342834,829440814,1134238973,2441272609,2790 -105947,1951687303,113196372,3567713416,1763819936,3141009532,3386073007,46626366 -7,738582537,4263256533,2365029894,1592704986,4080540129,555866173,1405781998,217 -8106930,3055302728,1678113172,384738887,3304548251,2037406387,2875825007,3649225 -916,194708832,1012169498,3998071494,2628183317,1321149641],[0,30977159,61954318, -40498569,123908636,112860827,80997138,84625301,247817272,253610175,225721654,212 -636081,161994276,142572195,169250602,198058925,495634544,475161847,507220350,534 -986233,451443308,456185579,425272162,411144165,323988552,311886031,285144390,287 -726017,338501204,368423635,396117850,373615581,991269088,986528871,950323694,964 -453737,1014440700,1034915451,1069972466,1042208629,902886616,872962143,912371158 -,934871377,850544324,862644803,822288330,819704653,647977104,659026967,623772062 -,620145945,570288780,539313675,575452034,596909829,677002408,696422447,736847270 -,708036897,792235700,786440755,747231162,760314685,1982538176,2012450119,1973057 -742,1950536777,1900647388,1888567131,1928907474,1931503189,2028881400,2033641855 -,2069830902,2055712881,2139944932,2119457635,2084417258,2112160365,1805773232,17 -86332471,1745924286,1774722105,1824742316,1830549291,1869742754,1856679461,17010 -88648,1690050831,1725289606,1728935937,1644576660,1675531027,1639409306,16179389 -73,1295954208,1290149287,1318053934,1331119273,1247544124,1266986939,1240291890, -1211496117,1140577560,1109621151,1078627350,1100095633,1150904068,1161939843,119 -3819658,1190171277,1354004816,1366087127,1392844894,1390251225,1473694540,144378 -4651,1416073794,1438596805,1584471400,1604956655,1572881510,1545136353,149446232 -4,1489699827,1520629370,1534745341,3965076352,3985567495,4024900238,3997152777,3 -946115484,3941358875,3901073554,3915187221,3801294776,3813378879,3777134262,3774 -534193,3857814948,3827906851,3863006378,3885522989,4057762800,4026804087,4067283 -710,4088757881,4139661804,4150695275,4111425762,4107783269,4279889864,4274078543 -,4238915270,4251982401,4168834516,4188270931,4224320730,4195526749,3611546464,36 -00515047,3572664942,3576309481,3491848572,3522809339,3549444210,3527972085,36494 -84632,3630046175,3661098582,3689890513,3739485508,3745294787,3713358922,37002897 -41,3402177296,3406935959,3380101662,3365990041,3450579212,3430090123,3457871874, -3485621381,3289153320,3319059375,3351062054,3328543393,3278818612,3266732467,323 -5877946,3238475965,2591908416,2611334855,2580298574,2551486409,2636107868,263031 -9323,2662238546,2675320277,2495088248,2506140415,2533973878,2530341873,248058378 -0,2449610979,2422992234,2444444141,2281155120,2251228855,2219242302,2241748921,2 -157254700,2169353387,2200191266,2197613989,2301808136,2297062031,2323879686,2338 -012033,2387639316,2408108179,2380342554,2352581021,2708009632,2695912999,2732174 -254,2734753577,2785689788,2815618107,2780502450,2757997877,2947389080,2926918175 -,2887569302,2915328785,2832147588,2836891651,2877193610,2863059213,3168942800,31 -74733399,3209913310,3196833625,3145763020,3126338635,3090272706,3119086917,29889 -24648,3019895407,2979399654,2957945697,3041258740,3030204531,3069490682,30731206 -37],[0,3698170551,3155831001,1618457198,2096450565,2694370994,3236914396,4783468 -59,4192901130,629605053,1173401811,2577214052,2233455631,1500663480,956693718,38 -48824417,4145294755,729397012,1259210106,2539888589,2346803622,1468857105,939215 -231,3952530376,251573673,3532861214,3001326960,1854474183,1913387436,2925945627, -3457274229,310135746,3941156593,914676806,1458794024,2325673119,2518420212,12489 -56483,705045037,4134254746,319020795,3480110156,2937714210,1937009813,1878430462 -,3013281865,3555506727,260120720,503147346,3247501797,2716287883,2106251580,1627 -924311,3177561568,3708948366,25138489,3826774872,947546607,1477303169,2220900662 -,2564996957,1150232042,620271492,4170517811,3507720277,226364130,1829353612,2976 -129595,2917588048,1904953063,301790345,3448860222,687409247,4103377640,249791296 -6,1217313329,1410090074,2288115437,3893783683,880539188,638041590,4201260865,258 -5629999,1181749144,1525871091,2258594628,3874019626,981812125,3756860924,5876922 -7,1677135141,3214579602,2736286201,2138436430,520241440,3278887831,1006294692,38 -85452307,2279669373,1535993034,1192204961,2606891030,4212503160,662186191,325584 -8622,511562777,2114610807,2724723904,3202679467,1653119004,50276978,3734155461,3 -438213895,277045680,1895093214,2895726953,2954606338,1819684277,201433051,349674 -0204,889479949,3916036538,2300464084,1433653603,1240542984,2510075327,4125820881 -,696687974,2800106781,2055972778,452728260,3331428211,3658707224,108981167,17118 -88833,3127165814,1594664215,2204188576,3809906126,1065031545,603580690,428791901 -3,2682503627,1133403004,1374818494,2376043017,3991418983,830841552,755457211,405 -0306572,2434626658,1299246805,2820180148,1953829379,335716461,3362732762,3572352 -177,142630406,1761078376,3030021855,1276083180,2422399323,4027929397,746113410,8 -21704681,3969363294,2363498288,1351452039,3051742182,1770551633,167758655,358313 -6136,3373314019,360527188,1963624250,2842107277,3139130959,1735838968,117538454, -3681346593,3354270282,461603069,2079601299,2811865124,1123143237,2661045490,4276 -872860,579238955,1040482880,3798538487,2183047833,1584607278,2012589384,28788797 -43,3421472145,394403622,184607053,3614276602,3071986068,1802982179,2384409922,13 -83247861,839196059,3999827756,4075452743,780657648,1324372382,2459814697,2162262 -251,1552685660,1023125554,3767939717,4229221614,544822873,1074717751,2623766144, -2030770401,2774958678,3306238008,427600527,100553956,3650342483,3118758973,17035 -36266,2635918265,1097953550,554091360,4251670999,3790186428,1032076555,157624304 -5,2174621138,1693873075,3097225476,3639368554,75612637,402866102,3295585537,2753 -107823,2020904408,1778959898,3060096173,3591564995,176125044,385714719,339843908 -0,2867307206,1988769905,2481085968,1334822055,804812489,4086688894,4011266581,86 -3668386,1393375948,2405474427]] :: [[Word32]] - x2 := v0 - x1 := (arrLength x2) - x3 := 0 :: Word32 - x4 := 0 :: Int - v3 := (tup2 x3 x4) - - for v2 in 0 .. (x1-1) do - x10 := 3 :: Int - x11 := 0 :: Int - x9 := (x10 - x11) - x12 := 1 :: Int - x8 := (x9 + x12) - x7 := (i2n x8) - x17 := v3 - x16 := (sel1 x17) - x19 := v0 - x21 := v3 - x20 := (sel2 x21) - x18 := (getIx x19 x20) - x15 := (xor x16 x18) - x14 := (bitSize x15) - x22 := 8 :: Int - x13 := (div x14 x22) - x6 := (min x7 x13) - v5 := 0 :: Word32 - - for v4 in 0 .. (x6-1) do - x23 := v5 - x26 := v1 - x29 := v4 - x28 := (i2n x29) - x30 := 0 :: Int - x27 := (x28 + x30) - x25 := (getIx x26 x27) - x37 := v3 - x36 := (sel1 x37) - x39 := v0 - x41 := v3 - x40 := (sel2 x41) - x38 := (getIx x39 x40) - x35 := (xor x36 x38) - x43 := 8 :: Int - x50 := v3 - x49 := (sel1 x50) - x52 := v0 - x54 := v3 - x53 := (sel2 x54) - x51 := (getIx x52 x53) - x48 := (xor x49 x51) - x47 := (bitSize x48) - x55 := 8 :: Int - x46 := (div x47 x55) - x56 := 1 :: Int - x45 := (x46 - x56) - x63 := v3 - x62 := (sel1 x63) - x65 := v0 - x67 := v3 - x66 := (sel2 x67) - x64 := (getIx x65 x66) - x61 := (xor x62 x64) - x60 := (bitSize x61) - x68 := 8 :: Int - x59 := (div x60 x68) - x69 := v4 - x58 := (x59 - x69) - x70 := 1 :: Int - x57 := (x58 - x70) - x44 := (x45 - x57) - x42 := (x43 * x44) - x34 := (shiftR x35 x42) - x71 := 255 :: Word32 - x33 := (x34 .&. x71) - x32 := (i2n x33) - x31 := (i2n x32) - x24 := (getIx x25 x31) - v5 := (xor x23 x24) - x5 := v5 - x74 := v3 - x73 := (sel2 x74) - x75 := 1 :: Int - x72 := (x73 + x75) - v3 := (tup2 x5 x72) - x0 := v3 - out := (sel1 x0) ---} - - -onCond :: Data Bool -> Data Int -> Data Int -onCond b m = m .&. (- (b2i b)) - -sumEven1 :: Vector (Data Int) -> Data Int -sumEven1 = sum . map (\i -> onCond (i .&. 1 == 0) i) - -swapOE1 :: (Syntax a) => Vector a -> Vector a -swapOE1 v = Indexed (length v) ixf - where - ixf i = (i `mod` 2 == 0) ? (index v (i+1), index v (i-1)) - --- same as above -swapOE2 :: Vector a -> Vector a -swapOE2 = premap (\i -> (i `mod` 2 == 0) ? (i+1,i-1)) - -swapOE3 :: Vector a -> Vector a -swapOE3 = premap (`xor` 1) - -premap :: (Data Index -> Data Index) -> Vector a -> Vector a -premap f (Indexed l ixf) = Indexed l (ixf . f) - - -bitr :: Data Index -> Data Index -> Data Index -bitr n a = - share (oneBitsN n) $ \mask -> (complement mask .&. a) .|. rev mask - where - rev mask = rotateL (reverseBits (mask .&. a)) n - -bitRev :: Data Index -> Vector a -> Vector a -bitRev = premap . bitr - -countUp :: Data Length -> Vector (Data Index) -countUp n = Indexed n id - -pipe :: Syntax a => (Data Index -> a -> a) -> Vector (Data Index) -> a -> a -pipe = flip . fold . flip - -specbr m n v = bL2Int (l ++ r') - where - iv = int2BLN m v - (l,r) = splitAt (m-n) iv - r' = reverse r - - - - -{-- -checkCRC :: (VecBool -> VecBool -> VecBool) -> VecBool -> VecBool -> Data Bool -checkCRC crc poly msg = fold && true (map not (crc poly (msg ++ (crc poly msg)))) ---} diff --git a/CEFP/Examples/Exercise10.hs b/CEFP/Examples/Exercise10.hs deleted file mode 100644 --- a/CEFP/Examples/Exercise10.hs +++ /dev/null @@ -1,109 +0,0 @@ -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE GADTs #-} -{-# LANGUAGE TypeOperators #-} -{-# LANGUAGE ViewPatterns #-} - -import Language.Syntactic - - - ----------------------------------------- --- a) ----------------------------------------- - -data Circ a - where - Const :: Bool -> Circ Bool - Inv :: Circ Bool -> Circ Bool - And :: Circ Bool -> Circ Bool -> Circ Bool - -data ConstSym a where Const' :: Bool -> ConstSym (Full Bool) -data InvSym a where Inv' :: InvSym (Bool :-> Full Bool) -data AndSym a where And' :: AndSym (Bool :-> Bool :-> Full Bool) - -type CircDom = InvSym :+: AndSym :+: ConstSym - - - ----------------------------------------- --- b) ----------------------------------------- - -consT :: (ConstSym :<: dom) => Bool -> ASTF dom Bool -consT a = inject (Const' a) - -inv :: (InvSym :<: dom) => ASTF dom Bool -> ASTF dom Bool -inv a = inject Inv' :$: a - -anD :: (AndSym :<: dom) => - ASTF dom Bool -> ASTF dom Bool -> ASTF dom Bool -anD a b = inject And' :$: a :$: b - - - ----------------------------------------- --- c) ----------------------------------------- - -circ1 :: Circ Bool -circ1 = And (Const False) (And (Const True) (Inv (Const False))) - -circ2 :: ASTF CircDom Bool -circ2 = anD (consT False) (anD (consT True) (inv (consT False))) - - - ----------------------------------------- --- d) ----------------------------------------- - -fromCirc :: Circ a -> ASTF CircDom a -fromCirc (Const a) = inject (Const' a) -fromCirc (Inv a) = inject Inv' :$: fromCirc a -fromCirc (And a b) = inject And' :$: fromCirc a :$: fromCirc b - -toCirc :: ASTF CircDom a -> Circ a -toCirc (project -> Just (Const' a)) = Const a -toCirc ((project -> Just Inv') :$: a) = Inv (toCirc a) -toCirc ((project -> Just And') :$: a :$: b) = And (toCirc a) (toCirc b) - - - ----------------------------------------- --- e) ----------------------------------------- - -instance Render ConstSym where render (Const' a) = show a -instance Render InvSym where render Inv' = "inv" -instance Render AndSym where render And' = "and" - -instance Eval ConstSym where evaluate (Const' a) = fromEval a -instance Eval InvSym where evaluate Inv' = fromEval not -instance Eval AndSym where evaluate And' = fromEval (&&) - - - ----------------------------------------- --- f) ----------------------------------------- - -data NandSym a where Nand :: NandSym (Bool :-> Bool :-> Full Bool) - -instance Render NandSym where render Nand = "nand" - -instance Eval NandSym where evaluate Nand = fromEval $ \a b -> not (a && b) - -nandify' :: AST (InvSym :+: AndSym :+: dom) a -> AST (NandSym :+: dom) a -nandify' ((project -> Just Inv') :$: a) = inject Nand :$: a' :$: a' - where - a' = nandify a -nandify' ((project -> Just And') :$: a :$: b) = inject Nand :$: ab :$: ab - where - ab = inject Nand :$: nandify a :$: nandify b -nandify' (c :$: a) = nandify' c :$: nandify a -nandify' (Symbol (InjectR (InjectR a))) = Symbol (InjectR a) - -nandify :: - ASTF (InvSym :+: AndSym :+: dom) a -> ASTF (NandSym :+: dom) a -nandify = nandify' - diff --git a/CEFP/Examples/Exercise12.hs b/CEFP/Examples/Exercise12.hs deleted file mode 100644 --- a/CEFP/Examples/Exercise12.hs +++ /dev/null @@ -1,26 +0,0 @@ -{-# LANGUAGE GADTs #-} -{-# LANGUAGE TypeOperators #-} - -import Language.Syntactic -import Language.Syntactic.Constructs.Symbol - -import MuFeldspar.Core - - - -data ForLoop' a - where - ForLoop' :: Type st => - ForLoop' (Length :-> st :-> (Index -> st -> st) :-> Full st) - -instance IsSymbol ForLoop' - where - toSym ForLoop' = Sym "forLoop" forLoop - where - forLoop len init body = foldl (flip body) init (reverse [0 .. len-1]) - -instance ExprEq ForLoop' where exprEq = exprEqSym -instance Render ForLoop' where renderPart = renderPartSym -instance Eval ForLoop' where evaluate = evaluateSym -instance ToTree ForLoop' - diff --git a/CEFP/Examples/Exercise14.hs b/CEFP/Examples/Exercise14.hs deleted file mode 100644 --- a/CEFP/Examples/Exercise14.hs +++ /dev/null @@ -1,61 +0,0 @@ -{-# LANGUAGE MultiParamTypeClasses #-} -{-# LANGUAGE TypeFamilies #-} -{-# LANGUAGE TypeSynonymInstances #-} -{-# LANGUAGE ViewPatterns #-} - -module Option where - - - -import Language.Syntactic - -import MuFeldspar.Core -import MuFeldspar.Frontend - - - -data Option a = Option { isSome :: Data Bool, fromSome :: a } - -instance Syntax a => Syntactic (Option a) FeldDomainAll - where - type Internal (Option a) = (Bool, Internal a) - desugar = desugar . freezeOption . fmap resugar - sugar = fmap resugar . unfreezeOption . sugar - -instance Functor Option - where - fmap f opt = opt {fromSome = f (fromSome opt)} - -instance Monad Option - where - return = some - a >>= f = b { isSome = isSome a ? (isSome b, false) } - where - b = f (fromSome a) - - - -freezeOption :: Type a => Option (Data a) -> Data (Bool,a) -freezeOption a = resugar (isSome a, fromSome a) - -unfreezeOption :: Type a => Data (Bool,a) -> Option (Data a) -unfreezeOption (resugar -> (valid,a)) = Option valid a - -undef :: Syntax a => a -undef = resugar $ getIx (value []) 0 - -some :: a -> Option a -some = Option true - -none :: Syntax a => Option a -none = Option false undef - -option :: Syntax b => b -> (a -> b) -> Option a -> b -option noneCase someCase opt = isSome opt ? - ( someCase (fromSome opt) - , noneCase - ) - -oplus :: Syntax a => Option a -> Option a -> Option a -oplus a b = isSome a ? (a,b) - diff --git a/CEFP/Examples/SolutionsSec2.hs b/CEFP/Examples/SolutionsSec2.hs deleted file mode 100644 --- a/CEFP/Examples/SolutionsSec2.hs +++ /dev/null @@ -1,370 +0,0 @@ -module Main where - -import qualified Prelude - -import MuFeldspar.Prelude - - -import MuFeldspar.Core ---import MuFeldspar.Tuple -import MuFeldspar.Frontend -import MuFeldspar.Vector - - -import Imperative.Imperative -import Imperative.Compiler - -import Data.Word -import Data.Bits (Bits) - -type VecBool = Vector (Data Bool) - -type VecInt = Vector (Data Int) - - - --- Exercise 1 - -composeN :: (Syntax st) => (st -> st) -> Data Length -> st -> st -composeN f l i0 = forLoop l i0 g - where - g _ st = f st - -tri :: (Syntax a) => (a -> a) -> Vector a -> Vector a -tri f (Indexed len ixf) = indexed len ixf' - where - ixf' i = composeN f i (ixf i) - - -tri1 :: (Syntax a) => (a -> a) -> Vector a -> Vector a -tri1 f (Indexed len ixf) = indexed len ixf' - where - ixf' i = forLoop i (ixf i) (\_ -> f) - - -{-- -*Main> eval $ tri (*2) (1...6) -[1,4,12,32,80,192] -*Main> eval $ tri1 (*2) (1...6) -[1,4,12,32,80,192] ---} - - --- Exercise 2 - -swapOE1 :: (Syntax a) => Vector a -> Vector a -swapOE1 v = Indexed (length v) ixf - where - ixf i = (i `mod` 2 == 0) ? (index v (i+1), index v (i-1)) - --- same as above -swapOE2 :: Vector a -> Vector a -swapOE2 = premap (\i -> (i `mod` 2 == 0) ? (i+1,i-1)) - -swapOE3 :: Vector a -> Vector a -swapOE3 = premap (`xor` 1) - -premap :: (Data Index -> Data Index) -> Vector a -> Vector a -premap f (Indexed l ixf) = Indexed l (ixf . f) - - - --- Exercise 3 - -pows2 :: Data Int -> Vector (Data Int) -pows2 k = Indexed k (2^) - - - -pow2 :: Data Index -> Data Index -pow2 k = 1 << k -- or 2^k - -pows21 :: Data Length -> Vector (Data Index) -pows21 k = Indexed k pow2 - - - - - --- Exercise 4 - -pad :: Data Length -> VecBool -> VecBool -pad l v = (replicate (l - length v) false) ++ v - -xorBool :: Data Bool -> Data Bool -> Data Bool -xorBool a b = not (a == b) - -crcAdd :: VecBool -> VecBool -> VecBool -crcAdd as bs = zipWith xorBool (pad m as) (pad m bs) - where - m = max (length as) (length bs) - - - - - - --- Exercise 5 - --- direct implementation using reverseBits -bitr :: Data Index -> Data Index -> Data Index -bitr n a = - share (oneBitsN n) $ \mask -> (complement mask .&. a) .|. rev mask - where - rev mask = rotateL (reverseBits (mask .&. a)) n - -bitRev :: Data Index -> Vector a -> Vector a -bitRev n = premap (bitr n) - -oneBitsN :: Data Index -> Data Index -oneBitsN = complement . zeroBitsN - -zeroBitsN :: Data Index -> Data Index -zeroBitsN = shiftL allOnes - -allOnes :: Data Index -allOnes = complement 0 - - - -bitrH :: Index -> Data Index -> Data Index -bitrH n a = - share (oneBitsN vn) $ \mask -> (complement mask .&. a) .|. rev mask - where - rev mask = rotateL (reverseBits (mask .&. a)) vn - vn = value n - - - - - --- transliteration of solution from bithacks -bitr1 :: Data Index -> Data Index -> Data Index -bitr1 n i = snd (pipe stage (countUp n) (i, i >> n)) - where - stage _ (i,r) = (i>>1, (i .&. 1) .|. (r<<1)) - -bitRev1 :: Data Index -> Vector a -> Vector a -bitRev1 n = premap (bitr1 n) - -countUp :: Data Length -> Vector (Data Index) -countUp n = Indexed n id - -pipe :: Syntax a => (Data Index -> a -> a) -> Vector (Data Index) -> a -> a -pipe = flip . fold . flip - - - --- A version of composeN that depends on a *Haskell* value - -composeNH :: Index -> (a -> a) -> a -> a -composeNH 0 f = id -composeNH n f = (composeNH (n-1) f) . f - - --- Now use this to make bitr. Note the type. - -bitr1H :: Index -> Data Index -> Data Index -bitr1H n i = snd (composeNH n stage (i, i >> vn)) - where - stage (i,r) = (i>>1, (i .&. 1) .|. (r<<1)) - vn = value n - - --- Now we must provide the n parameter at compile time --- and the recursion gets unwound - -{-- - -main (v0) - x3 := v0 - x4 := 1 :: Int - x2 := (shiftR x3 x4) - x5 := 1 :: Int - x1 := (shiftR x2 x5) - x6 := 1 :: Int - x0 := (x1 .&. x6) - x11 := v0 - x12 := 1 :: Int - x10 := (shiftR x11 x12) - x13 := 1 :: Int - x9 := (x10 .&. x13) - x17 := v0 - x18 := 1 :: Int - x16 := (x17 .&. x18) - x21 := v0 - x22 := 3 :: Int - x20 := (shiftR x21 x22) - x23 := 1 :: Int - x19 := (shiftL x20 x23) - x15 := (x16 .|. x19) - x24 := 1 :: Int - x14 := (shiftL x15 x24) - x8 := (x9 .|. x14) - x25 := 1 :: Int - x7 := (shiftL x8 x25) - out := (x0 .|. x7) - - -Compare with printMain $ bitr1 -which gives the expected for loop - -main (v0,v1) - x1 := v0 - x2 := v1 - x4 := v1 - x5 := v0 - x3 := (shiftR x4 x5) - v3 := (tup2 x2 x3) - - for v2 in 0 .. (x1-1) do - x8 := v3 - x7 := (sel1 x8) - x9 := 1 :: Int - x6 := (shiftR x7 x9) - x13 := v3 - x12 := (sel1 x13) - x14 := 1 :: Int - x11 := (x12 .&. x14) - x17 := v3 - x16 := (sel2 x17) - x18 := 1 :: Int - x15 := (shiftL x16 x18) - x10 := (x11 .|. x15) - v3 := (tup2 x6 x10) - x0 := v3 - out := (sel2 x0) - ---} - - - - - - -specbr m n v = bL2Int (l ++ r') - where - iv = int2BLN m v - (l,r) = splitAt (m-n) iv - r' = reverse r - -testBit :: (Type a, Bits a) => Data a -> Data Index -> Data Bool -testBit l i = not ((l .&. (1< Data a -> VecBool -int2BL l = reverse $ indexed (bitSize l) (testBit l) - - -int2BLN :: Data Length -> Data Int -> VecBool -int2BLN n v = reverse $ indexed n (testBit v) - - -bL2Int :: VecBool -> Data Int -bL2Int bs = scalarProduct (reverse (map b2i bs)) (pows2 (length bs)) - -bL2Int' :: VecBool -> Data Int -bL2Int' = sum . tri (*2) . map b2i - -scalarProduct :: (Type a, Num a) => Vector (Data a) -> Vector (Data a) -> Data a -scalarProduct as bs = sum (zipWith (*) as bs) - - - - - --- Exercise 6 (See slides) - --- 2^n input FFT. Applies to sub-parts of input vector --- of length 2^(n+i). --- There is currently no check that the input vector is at least of length 2^n - - -countDown n = reverse (indexed n id) - -fft :: Data Index -> Vector (Data Complex) -> Vector (Data Complex) -fft n = bitRev n . lin stage (countDown n) - where - stage k = combx f g (bitZero k) (flipBit k) twid - where - f a b _ = a + b - g a b t = t * (a-b) - twid i = cis ((-(value pi)*(i2n (lsbsN k i)))/ i2n (pow2 k)) - - - -combx f g c p x (Indexed l ixf) = Indexed l ixf' - where - ixf' i = (c i) ? (f ai pi xi, g pi ai xi) - where - ai = ixf i - pi = ixf (p i) - xi = x i - - - - -lin :: Syntax a => (b -> a -> a) -> Vector b -> a -> a -lin f (Indexed len ixf) a = forLoop len a (\i st -> f (ixf i) st) - -lsbsN :: Data Index -> Data Index -> Data Index -lsbsN k i = i .&. oneBitsN k - -bitZero :: Data Index -> Data Index -> Data Bool -bitZero k i = (i .&. (1< Data Index -> Data Index -flipBit k = (`xor` (1< - (t -> t -> a) -> (t -> t -> a) - -> (Data Index -> Data Bool) -> (Data Index -> Data Index) - -> Vector t - -> Vector a -comb f g c p (Indexed l ixf) = Indexed l ixf' - where - ixf' i = (c i) ? (f a b, g a b) - where - a = ixf i - b = ixf (p i) - -apart :: (Syntax a) => - (t -> t -> a) -> (t -> t -> a) - -> Data Index - -> Vector t - -> Vector a -apart f g k = comb f g (bitZero k) (flipBit k) - - - - - - -bMerge :: Data Index -> Vector (Data Int) -> Vector (Data Int) -bMerge n = lin (apart min max) (countDown n) - - --- now we'd like to be able to reverse half of each 2^n length sub-vector - -halfRev :: Data Index -> Vector (Data a) -> Vector (Data a) -halfRev n = premap (\i -> (bitZero n' i) ? (i ,i `xor` oneBitsN n')) - where - n' = n-1 - - -merge :: Data Index -> Vector (Data Int) -> Vector (Data Int) -merge n = bMerge n . halfRev n - -bsort :: Data Index -> Vector (Data Int) -> Vector (Data Int) -bsort n = lin merge (1...n) - - - - diff --git a/CEFP/Examples/Test.hs b/CEFP/Examples/Test.hs deleted file mode 100644 --- a/CEFP/Examples/Test.hs +++ /dev/null @@ -1,46 +0,0 @@ -import qualified Prelude - -import MuFeldspar.Prelude -import MuFeldspar.Core -import MuFeldspar.Frontend -import MuFeldspar.Vector - -import Imperative.Imperative -import Imperative.Compiler - - - -prog1 :: Data Int -prog1 = 23 + min 45 2 - -test1_1 = eval prog1 -test1_2 = printMain $ compile prog1 - -prog2 = (prog1==3) ? (prog1*3, prog1*4) - -test2_1 = eval prog2 -test2_2 = printMain $ compile prog2 - -- Note how prog1 is only computed once - -prog3 :: Vector (Vector (Data Int)) -> Vector (Vector (Data Int)) -prog3 = map reverse . map reverse - -test3_1 = eval prog3 [[1,2,3],[4,5],[6]] -test3_2 = printMain $ compile prog3 - -prog4 :: Vector (Vector (Data Int)) -> Data Int -prog4 = sum . map sum . map reverse . map reverse - -test4_1 = eval prog4 [[1,2,3],[4,5],[6]] -test4_2 = printMain $ compile prog4 - -prog5 = sequential 10 1 $ \i st -> (i+st, (i+1)*st) - -test5_1 = eval prog5 -test5_2 = printMain $ compile prog5 - -prog6 as bs = sum (zipWith (*) as bs) :: Data Index - -test6_1 = eval prog6 [10..19] [20..29] -test6_2 = printMain $ compile prog6 - diff --git a/CEFP/Imperative/Compiler.hs b/CEFP/Imperative/Compiler.hs deleted file mode 100644 --- a/CEFP/Imperative/Compiler.hs +++ /dev/null @@ -1,204 +0,0 @@ -{-# OPTIONS_GHC -fcontext-stack=25 #-} - -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE GADTs #-} -{-# LANGUAGE MultiParamTypeClasses #-} -{-# LANGUAGE TypeOperators #-} -{-# LANGUAGE UndecidableInstances #-} -{-# LANGUAGE ViewPatterns #-} - -module Imperative.Compiler where - - - -import Prelude as P - -import Control.Monad.State - -import Language.Syntactic -import Language.Syntactic.Constructs.Symbol -import Language.Syntactic.Constructs.Literal -import Language.Syntactic.Constructs.Condition -import Language.Syntactic.Constructs.Tuple -import Language.Syntactic.Constructs.Binding -import Language.Syntactic.Constructs.Binding.HigherOrder -import Language.Syntactic.Sharing.SimpleCodeMotion - -import MuFeldspar.Core -import Imperative.Imperative - - - --------------------------------------------------------------------------------- --- * Misc. --------------------------------------------------------------------------------- - -type Result = Ident - -ident :: String -> VarId -> Ident -ident base i = base ++ show i - -freshVar :: State VarId String -freshVar = do - v <- get; put (v+1) - return (ident "x" v) - -viewInfix :: String -> Maybe String -viewInfix name - | head name P.== '(' && last name P.== ')' = Just (tail $ init name) - | otherwise = Nothing - -projLambda :: (Lambda Poly :<: dom) => AST dom a -> Maybe VarId -projLambda = liftM getVar . project - where - getVar :: Lambda Poly a -> VarId - getVar (Lambda var) = var - - - --------------------------------------------------------------------------------- --- * Generic machinery --------------------------------------------------------------------------------- - -class Compile sub dom - where - compileSym :: sub a -> Result -> HList (AST dom) a -> State VarId Prog - -instance (Compile sub1 dom, Compile sub2 dom) => Compile (sub1 :+: sub2) dom - where - compileSym (InjectL a) = compileSym a - compileSym (InjectR a) = compileSym a - -compileM :: Compile dom dom => Result -> ASTF dom a -> State VarId Prog -compileM result = queryNodeSimple (flip compileSym result) - -compileFresh :: Compile dom dom => ASTF dom a -> State VarId (Result,Prog) -compileFresh arg = do - var <- freshVar - prog <- compileM var arg - return (var,prog) - -compileTop :: (Compile dom dom, Lambda Poly :<: dom) => - [Ident] -> ASTF dom a -> Main -compileTop params ((projLambda -> Just inp) :$: body) = - compileTop (ident "v" inp:params) body -compileTop params a = Main (reverse params) prog - where - prog = flip evalState 0 $ compileM "out" a - -compile :: Syntactic a FeldDomainAll => a -> Main -compile = compileTop [] . reifySmart poly - - - -instance Compile dom dom => Compile (Sym ctx) dom - where - compileSym (Sym name _) result args = do - (varArgs,progs) <- liftM unzip $ listHListM compileFresh args - return $ concat progs ++ [result := expr varArgs] - where - expr [a,b] - | Just op <- viewInfix name = Op op (Var a) (Var b) - expr args = App name (map Var args) - -compileSymb :: (IsSymbol expr, Compile dom dom) => - expr a -> Result -> HList (AST dom) a -> State VarId Prog -compileSymb = compileSym . toSym - - - --------------------------------------------------------------------------------- --- * Compilation of sub-domains --------------------------------------------------------------------------------- - -instance Compile (Variable Poly) dom - where - compileSym (Variable i) result _ = return [result := Var (ident "v" i)] - -instance Compile (Lambda Poly) dom - where - compileSym = error "Can only compile top-level Lambda" - -instance Compile (Literal Poly) dom - where - compileSym (Literal a) result _ = return [result := Lit (show a)] - -instance Compile dom dom => Compile NUM dom where compileSym = compileSymb -instance Compile dom dom => Compile INTEGRAL dom where compileSym = compileSymb -instance Compile dom dom => Compile FRACTIONAL dom where compileSym = compileSymb -instance Compile dom dom => Compile Conversion dom where compileSym = compileSymb -instance Compile dom dom => Compile COMPLEX dom where compileSym = compileSymb -instance Compile dom dom => Compile BITS dom where compileSym = compileSymb -instance Compile dom dom => Compile Logic dom where compileSym = compileSymb -instance Compile dom dom => Compile ORD dom where compileSym = compileSymb -instance Compile dom dom => Compile Array dom where compileSym = compileSymb - -instance Compile dom dom => Compile (Condition Poly) dom - where - compileSym Condition result (cond :*: tHEN :*: eLSE :*: Nil) = do - (condVar,condProg) <- compileFresh cond - thenProg <- compileM result tHEN - elseProg <- compileM result eLSE - return $ condProg ++ [Cond (Var condVar) thenProg elseProg] - -instance Compile dom dom => Compile (Tuple Poly) dom where compileSym = compileSymb -instance Compile dom dom => Compile (Select Poly) dom where compileSym = compileSymb - -instance (Compile dom dom, Lambda Poly :<: dom) => Compile (Let Poly Poly) dom - where - compileSym Let result (a :*: ((projLambda -> Just var) :$: body) :*: Nil) = - liftM2 (++) - (compileM (ident "v" var) a) - (compileM result body) - -instance (Compile dom dom, Lambda Poly :<: dom) => Compile Parallel dom - where - compileSym par@Parallel result (len :*: (lamIx :$: body) :*: Nil) - | Just ix <- projLambda lamIx - = do (lenVar,lenProg) <- compileFresh len - (elemVar,bodyProg) <- compileFresh body - let ixVar = ident "v" ix - emptyProg = result := Lit "[]" - assignProg = result := App "updateArr" [Var result, Var ixVar, Var elemVar] - let fullBody = bodyProg ++ [assignProg] - return - $ lenProg - ++ [emptyProg, For True (Var lenVar) ixVar fullBody] - -instance (Compile dom dom, Lambda Poly :<: dom) => Compile Sequential dom - where - compileSym seq@Sequential result (len :*: init :*: (lamIx :$: (lamSt :$: body)) :*: Nil) - | Just ix <- projLambda lamIx - , Just st <- projLambda lamSt - = do (lenVar,lenProg) <- compileFresh len - let ixVar = ident "v" ix - stVar = ident "v" st - initProg <- compileM stVar init - (bodyVar,bodyProg) <- compileFresh body - elemVar <- freshVar - let fstProg = elemVar := App "sel1" [Var bodyVar] - sndProg = stVar := App "sel2" [Var bodyVar] - emptyProg = result := Lit "[]" - assignProg = result := App "setIx" [Var result, Var ixVar, Var elemVar] - let fullBody = bodyProg ++ [fstProg,sndProg,assignProg] - return - $ lenProg - ++ initProg - ++ [emptyProg, For False (Var lenVar) ixVar fullBody] - -instance (Compile dom dom, Lambda Poly :<: dom) => Compile ForLoop dom - where - compileSym ForLoop result (len :*: init :*: (lamIx :$: (lamSt :$: body)) :*: Nil) - | Just ix <- projLambda lamIx - , Just st <- projLambda lamSt - = do (lenVar,lenProg) <- compileFresh len - let ixVar = ident "v" ix - stVar = ident "v" st - initProg <- compileM stVar init - bodyProg <- compileM stVar body - return - $ lenProg - ++ initProg - ++ [For False (Var lenVar) ixVar bodyProg, result := Var stVar] - diff --git a/CEFP/Imperative/Imperative.hs b/CEFP/Imperative/Imperative.hs deleted file mode 100644 --- a/CEFP/Imperative/Imperative.hs +++ /dev/null @@ -1,98 +0,0 @@ -module Imperative.Imperative where - - - -import Data.List - - - -type Ident = String - -data Expr - = Lit String -- Literal - | Var Ident -- Variable - | App String [Expr] -- Function call - | Op String Expr Expr -- Binary operator - -type IsPar = Bool -- Parallel or sequential loop? - -data Stmt - = Nop -- No-op - | Ident := Expr -- Assignment - | Cond Expr Prog Prog -- Conditional - | For IsPar Expr Ident Prog -- For loop - -type Prog = [Stmt] - -data Main = Main - { mainInp :: [Ident] - , mainBody :: Prog - } - -instance Show Main - where - show = renderMain - - - -paren :: String -> String -paren = ("(" ++) . (++ ")") - --- | Like 'unlines', but without the final newline -unLines :: [String] -> String -unLines = concat . intersperse "\n" - -indent :: Int -> String -> String -indent n = unLines . map move . lines - where - move = (replicate n ' ' ++) - -renderExpr :: Expr -> String -renderExpr (Lit a) = a -renderExpr (Var ident) = ident -renderExpr (App str args) = paren $ unwords (str : map renderExpr args) -renderExpr (Op str a b) = paren $ unwords [renderExpr a, str, renderExpr b] - -mkNop :: Prog -> Prog -mkNop [] = [Nop] -mkNop prog = prog - -renderStmt :: Stmt -> String -renderStmt Nop = "nop" -renderStmt (ident := expr) = ident ++ " := " ++ renderExpr expr -renderStmt (Cond cond tHEN eLSE) - | isSmall = - ("if " ++ renderExpr cond ++ " then " ++ tRend ++ " else " ++ eRend) - | otherwise = - ("\nif " ++ renderExpr cond ++ " then\n") - ++ - indent 2 tRend - ++ - "\nelse\n" - ++ - indent 2 eRend - where - t = mkNop tHEN - e = mkNop eLSE - tRend = renderProg t - eRend = renderProg e - isSmall = length (lines tRend) <= 1 && length (lines eRend) <= 1 -renderStmt (For isPar len index body) = - (loop ++ index ++ " in 0 .. (" ++ renderExpr len ++ "-1) do\n") - ++ - indent 2 (renderProg body) - where - loop = if isPar then "\npar " else "\nfor " - -renderProg :: Prog -> String -renderProg = unLines . map renderStmt - -renderMain :: Main -> String -renderMain (Main params prog) = - ("main (" ++ concat (intersperse "," params) ++ ")\n") - ++ - indent 2 (renderProg prog) - -printMain :: Main -> IO () -printMain = putStrLn . (++"\n") . renderMain - diff --git a/CEFP/MuFeldspar/Core.hs b/CEFP/MuFeldspar/Core.hs deleted file mode 100644 --- a/CEFP/MuFeldspar/Core.hs +++ /dev/null @@ -1,460 +0,0 @@ -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE GADTs #-} -{-# LANGUAGE MultiParamTypeClasses #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE TypeFamilies #-} -{-# LANGUAGE TypeOperators #-} -{-# LANGUAGE TypeSynonymInstances #-} -{-# LANGUAGE UndecidableInstances #-} - -module MuFeldspar.Core where - - - -import Data.Bits (Bits) -import qualified Data.Bits as Bits -import Data.Complex hiding (Complex) -import qualified Data.Complex as C -import Data.List -import Data.Typeable - -import Language.Syntactic -import Language.Syntactic.Constructs.Symbol -import Language.Syntactic.Constructs.Literal -import Language.Syntactic.Constructs.Condition -import Language.Syntactic.Constructs.Tuple -import Language.Syntactic.Constructs.Binding -import Language.Syntactic.Constructs.Binding.HigherOrder - - - --------------------------------------------------------------------------------- --- * Types --------------------------------------------------------------------------------- - --- | Set of supported types -class (Eq a, Show a, Typeable a) => Type a -instance (Eq a, Show a, Typeable a) => Type a - -type Length = Int -type Index = Int - - - --------------------------------------------------------------------------------- --- * Numeric functions --------------------------------------------------------------------------------- - -data NUM a - where - Abs :: (Type a, Num a) => NUM (a :-> Full a) - Sign :: (Type a, Num a) => NUM (a :-> Full a) - Add :: (Type a, Num a) => NUM (a :-> a :-> Full a) - Sub :: (Type a, Num a) => NUM (a :-> a :-> Full a) - Mul :: (Type a, Num a) => NUM (a :-> a :-> Full a) - -instance IsSymbol NUM - where - toSym Abs = Sym "abs" abs - toSym Sign = Sym "signum" signum - toSym Add = Sym "(+)" (+) - toSym Sub = Sym "(-)" (-) - toSym Mul = Sym "(*)" (*) - -instance ExprEq NUM where exprEq = exprEqSym; exprHash = exprHashSym -instance Render NUM where renderPart = renderPartSym -instance Eval NUM where evaluate = evaluateSym -instance ToTree NUM -instance EvalBind NUM where evalBindSym = evalBindSymDefault - -instance MaybeWitnessSat Poly NUM where maybeWitnessSat _ _ = Just SatWit - - - --------------------------------------------------------------------------------- --- * Integral functions --------------------------------------------------------------------------------- - -data INTEGRAL a - where - Div :: (Type a, Integral a) => INTEGRAL (a :-> a :-> Full a) - Mod :: (Type a, Integral a) => INTEGRAL (a :-> a :-> Full a) - Exp :: (Type a, Integral a) => INTEGRAL (a :-> a :-> Full a) - -instance IsSymbol INTEGRAL - where - toSym Div = Sym "div" div - toSym Mod = Sym "mod" mod - toSym Exp = Sym "(^)" (^) - -instance ExprEq INTEGRAL where exprEq = exprEqSym; exprHash = exprHashSym -instance Render INTEGRAL where renderPart = renderPartSym -instance Eval INTEGRAL where evaluate = evaluateSym -instance ToTree INTEGRAL -instance EvalBind INTEGRAL where evalBindSym = evalBindSymDefault - -instance MaybeWitnessSat Poly INTEGRAL where maybeWitnessSat _ _ = Just SatWit - - - --------------------------------------------------------------------------------- --- * Fractional functions --------------------------------------------------------------------------------- - -data FRACTIONAL a - where - FDiv :: (Type a, Fractional a) => FRACTIONAL (a :-> a :-> Full a) - -instance IsSymbol FRACTIONAL - where - toSym FDiv = Sym "(/)" (/) - -instance ExprEq FRACTIONAL where exprEq = exprEqSym; exprHash = exprHashSym -instance Render FRACTIONAL where renderPart = renderPartSym -instance Eval FRACTIONAL where evaluate = evaluateSym -instance ToTree FRACTIONAL -instance EvalBind FRACTIONAL where evalBindSym = evalBindSymDefault - -instance MaybeWitnessSat Poly FRACTIONAL where maybeWitnessSat _ _ = Just SatWit - - - --------------------------------------------------------------------------------- --- * Conversion functions --------------------------------------------------------------------------------- - -data Conversion a - where - I2N :: (Type a, Integral a, Type b, Num b) => Conversion (a :-> Full b) - F2I :: (Type a, Integral a) => Conversion (Float :-> Full a) - B2I :: (Type a, Integral a) => Conversion (Bool :-> Full a) - -instance IsSymbol Conversion - where - toSym I2N = Sym "i2n" (fromInteger.toInteger) - toSym F2I = Sym "f2i" truncate - toSym B2I = Sym "b2i" (\b -> if b then 1 else 0) - -instance ExprEq Conversion where exprEq = exprEqSym; exprHash = exprHashSym -instance Render Conversion where renderPart = renderPartSym -instance Eval Conversion where evaluate = evaluateSym -instance ToTree Conversion -instance EvalBind Conversion where evalBindSym = evalBindSymDefault - -instance MaybeWitnessSat Poly Conversion where maybeWitnessSat _ _ = Just SatWit - - - --------------------------------------------------------------------------------- --- * Complex numbers --------------------------------------------------------------------------------- - -type Complex = C.Complex Float - -data COMPLEX a - where - Complex :: COMPLEX (Float :-> Float :-> Full Complex) - RealPart :: COMPLEX (Complex :-> Full Float) - ImagPart :: COMPLEX (Complex :-> Full Float) - MkPolar :: COMPLEX (Float :-> Float :-> Full Complex) - Magnitude :: COMPLEX (Complex :-> Full Float) - Phase :: COMPLEX (Complex :-> Full Float) - -instance IsSymbol COMPLEX - where - toSym Complex = Sym "complex" (:+) - toSym RealPart = Sym "realPart" realPart - toSym ImagPart = Sym "imagPart" imagPart - toSym MkPolar = Sym "mkPolar" mkPolar - toSym Magnitude = Sym "magnitude" magnitude - toSym Phase = Sym "phase" phase - -instance ExprEq COMPLEX where exprEq = exprEqSym; exprHash = exprHashSym -instance Render COMPLEX where renderPart = renderPartSym -instance Eval COMPLEX where evaluate = evaluateSym -instance ToTree COMPLEX -instance EvalBind COMPLEX where evalBindSym = evalBindSymDefault - -instance MaybeWitnessSat Poly COMPLEX where maybeWitnessSat _ _ = Just SatWit - - - --------------------------------------------------------------------------------- --- * Bit manipulation --------------------------------------------------------------------------------- - -data BITS a - where - Complement :: (Type a, Bits a) => BITS (a :-> Full a) - BitAnd :: (Type a, Bits a) => BITS (a :-> a :-> Full a) - BitOr :: (Type a, Bits a) => BITS (a :-> a :-> Full a) - Xor :: (Type a, Bits a) => BITS (a :-> a :-> Full a) - ShiftL :: (Type a, Bits a) => BITS (a :-> Index :-> Full a) - ShiftR :: (Type a, Bits a) => BITS (a :-> Index :-> Full a) - RotateL :: (Type a, Bits a) => BITS (a :-> Index :-> Full a) - RotateR :: (Type a, Bits a) => BITS (a :-> Index :-> Full a) - BitSize :: (Type a, Bits a) => BITS (a :-> Full Index) - ReverseBits :: (Type a, Bits a) => BITS (a :-> Full a) - -instance IsSymbol BITS - where - toSym Complement = Sym "complement" Bits.complement - toSym BitAnd = Sym "(.&.)" (Bits..&.) - toSym BitOr = Sym "(.|.)" (Bits..|.) - toSym Xor = Sym "xor" Bits.xor - toSym ShiftL = Sym "shiftL" Bits.shiftL - toSym ShiftR = Sym "shiftR" Bits.shiftR - toSym RotateL = Sym "rotateL" Bits.rotateL - toSym RotateR = Sym "rotateR" Bits.rotateR - toSym BitSize = Sym "bitSize" Bits.bitSize - toSym ReverseBits = Sym "reverseBits" reverseBits - where - reverseBits :: Bits.Bits b => b -> b - reverseBits b = revLoop b 0 (0 `asTypeOf` b) - where - bitSize = Bits.bitSize b - revLoop b i n - | i Prelude.>= bitSize = n - | Bits.testBit b i = - revLoop b (i+1) (Bits.setBit n (bitSize - i - 1)) - | otherwise = revLoop b (i+1) n - - - -instance ExprEq BITS where exprEq = exprEqSym; exprHash = exprHashSym -instance Render BITS where renderPart = renderPartSym -instance Eval BITS where evaluate = evaluateSym -instance ToTree BITS -instance EvalBind BITS where evalBindSym = evalBindSymDefault - -instance MaybeWitnessSat Poly BITS where maybeWitnessSat _ _ = Just SatWit - - - --------------------------------------------------------------------------------- --- * Logic operations --------------------------------------------------------------------------------- - -data Logic a - where - Eq :: Type a => Logic (a :-> a :-> Full Bool) - Not :: Logic (Bool :-> Full Bool) - And :: Logic (Bool :-> Bool :-> Full Bool) - Or :: Logic (Bool :-> Bool :-> Full Bool) - -instance IsSymbol Logic - where - toSym Eq = Sym "(==)" (==) - toSym Not = Sym "not" not - toSym And = Sym "(&&)" (&&) - toSym Or = Sym "(||)" (||) - -instance ExprEq Logic where exprEq = exprEqSym; exprHash = exprHashSym -instance Render Logic where renderPart = renderPartSym -instance Eval Logic where evaluate = evaluateSym -instance ToTree Logic -instance EvalBind Logic where evalBindSym = evalBindSymDefault - -instance MaybeWitnessSat Poly Logic where maybeWitnessSat _ _ = Just SatWit - - - --------------------------------------------------------------------------------- --- * Functions on ordered types --------------------------------------------------------------------------------- - -data ORD a - where - Less :: (Type a, Ord a) => ORD (a :-> a :-> Full Bool) - LEQ :: (Type a, Ord a) => ORD (a :-> a :-> Full Bool) - Greater :: (Type a, Ord a) => ORD (a :-> a :-> Full Bool) - GEQ :: (Type a, Ord a) => ORD (a :-> a :-> Full Bool) - Min :: (Type a, Ord a) => ORD (a :-> a :-> Full a) - Max :: (Type a, Ord a) => ORD (a :-> a :-> Full a) - -instance IsSymbol ORD - where - toSym Less = Sym "(<)" (<) - toSym LEQ = Sym "(<=)" (<=) - toSym Greater = Sym "(>)" (>) - toSym GEQ = Sym "(>=)" (>=) - toSym Min = Sym "min" min - toSym Max = Sym "max" max - -instance ExprEq ORD where exprEq = exprEqSym; exprHash = exprHashSym -instance Render ORD where renderPart = renderPartSym -instance Eval ORD where evaluate = evaluateSym -instance ToTree ORD -instance EvalBind ORD where evalBindSym = evalBindSymDefault - -instance MaybeWitnessSat Poly ORD where maybeWitnessSat _ _ = Just SatWit - - - --------------------------------------------------------------------------------- --- * Array functions --------------------------------------------------------------------------------- - -data Array a - where - GetLength :: Type a => Array ([a] :-> Full Length) - SetLength :: Type a => Array (Length :-> [a] :-> Full [a]) - GetIx :: Type a => Array ([a] :-> Index :-> Full a) - -instance IsSymbol Array - where - toSym GetLength = Sym "getLength" length - toSym SetLength = Sym "setLength" take - toSym GetIx = Sym "getIx" getIx - where - getIx as i - | (i >= length as) || (i < 0) = error "getIx: index out of bounds" - | otherwise = as !! i - -instance ExprEq Array where exprEq = exprEqSym; exprHash = exprHashSym -instance Render Array where renderPart = renderPartSym -instance Eval Array where evaluate = evaluateSym -instance ToTree Array -instance EvalBind Array where evalBindSym = evalBindSymDefault - -instance MaybeWitnessSat Poly Array where maybeWitnessSat _ _ = Just SatWit - - - --------------------------------------------------------------------------------- --- * Parallel arrays --------------------------------------------------------------------------------- - -data Parallel a - where - Parallel :: Type a => Parallel (Length :-> (Index -> a) :-> Full [a]) - -instance IsSymbol Parallel - where - toSym Parallel = Sym "parallel" parallelEval - where - parallelEval len ixf = map ixf [0 .. len-1] - -instance ExprEq Parallel where exprEq = exprEqSym; exprHash = exprHashSym -instance Render Parallel where renderPart = renderPartSym -instance Eval Parallel where evaluate = evaluateSym -instance ToTree Parallel -instance EvalBind Parallel where evalBindSym = evalBindSymDefault - -instance MaybeWitnessSat Poly Parallel where maybeWitnessSat _ _ = Just SatWit - - - --------------------------------------------------------------------------------- --- * Sequential arrays --------------------------------------------------------------------------------- - -data Sequential a - where - Sequential :: (Type st, Type a) => - Sequential (Length :-> st :-> (Index -> st -> (a,st)) :-> Full [a]) - -instance IsSymbol Sequential - where - toSym Sequential = Sym "sequential" sequentialEval - where - sequentialEval l init step = snd $ mapAccumL evalStep init [0 .. l-1] - where - evalStep st i = (st',a) where (a,st') = step i st - -instance ExprEq Sequential where exprEq = exprEqSym; exprHash = exprHashSym -instance Render Sequential where renderPart = renderPartSym -instance Eval Sequential where evaluate = evaluateSym -instance ToTree Sequential -instance EvalBind Sequential where evalBindSym = evalBindSymDefault - -instance MaybeWitnessSat Poly Sequential where maybeWitnessSat _ _ = Just SatWit - - - --------------------------------------------------------------------------------- --- * For loops --------------------------------------------------------------------------------- - -data ForLoop a - where - ForLoop :: Type st => - ForLoop (Length :-> st :-> (Index -> st -> st) :-> Full st) - -instance IsSymbol ForLoop - where - toSym ForLoop = Sym "forLoop" forLoopEval - where - forLoopEval len init body = foldl (flip body) init [0 .. len-1] - -instance ExprEq ForLoop where exprEq = exprEqSym; exprHash = exprHashSym -instance Render ForLoop where renderPart = renderPartSym -instance Eval ForLoop where evaluate = evaluateSym -instance ToTree ForLoop -instance EvalBind ForLoop where evalBindSym = evalBindSymDefault - -instance MaybeWitnessSat Poly ForLoop where maybeWitnessSat _ _ = Just SatWit - - - --------------------------------------------------------------------------------- --- * Feldspar domain --------------------------------------------------------------------------------- - -type FeldDomain - = Literal Poly - :+: Condition Poly - :+: Tuple Poly - :+: Select Poly - :+: Let Poly Poly - :+: NUM - :+: INTEGRAL - :+: FRACTIONAL - :+: Conversion - :+: COMPLEX - :+: BITS - :+: Logic - :+: ORD - :+: Array - :+: Parallel - :+: Sequential - :+: ForLoop - -type FeldDomainAll = HODomain Poly FeldDomain - -newtype Data a = Data { unData :: ASTF FeldDomainAll a } - -instance Type a => Syntactic (Data a) FeldDomainAll - where - type Internal (Data a) = a - desugar = unData - sugar = Data - --- | Specialization of the 'Syntactic' class for the Feldspar domain -class (Syntactic a FeldDomainAll, Type (Internal a)) => Syntax a -instance (Syntactic a FeldDomainAll, Type (Internal a)) => Syntax a - -instance Type a => Eq (Data a) - where - Data a == Data b = alphaEq poly (reify poly a) (reify poly b) - -instance Type a => Show (Data a) - where - show (Data a) = render $ reify poly a - - - --------------------------------------------------------------------------------- --- * Back ends --------------------------------------------------------------------------------- - -printFeld :: Syntactic a FeldDomainAll => a -> IO () -printFeld = printExpr . reify poly - -drawFeld :: Syntactic a FeldDomainAll => a -> IO () -drawFeld = drawAST . reify poly - -eval :: Syntactic a FeldDomainAll => a -> Internal a -eval = evalBind . reify poly - diff --git a/CEFP/MuFeldspar/Frontend.hs b/CEFP/MuFeldspar/Frontend.hs deleted file mode 100644 --- a/CEFP/MuFeldspar/Frontend.hs +++ /dev/null @@ -1,218 +0,0 @@ -{-# OPTIONS_GHC -fcontext-stack=30 #-} - -{-# LANGUAGE GADTs #-} -{-# LANGUAGE ViewPatterns #-} - -module MuFeldspar.Frontend where - - - -import Data.Bits (Bits) - -import Language.Syntactic -import Language.Syntactic.Constructs.Symbol -import Language.Syntactic.Constructs.Literal -import Language.Syntactic.Constructs.Condition -import Language.Syntactic.Constructs.TupleSyntacticPoly -import Language.Syntactic.Constructs.Binding -import Language.Syntactic.Constructs.Binding.HigherOrder - -import MuFeldspar.Core - - - -value :: Syntax a => Internal a -> a -value = sugarSymCtx poly . Literal - -false :: Data Bool -false = value False - -true :: Data Bool -true = value True - --- | For types containing some kind of \"thunk\", this function can be used to --- force computation -force :: Syntax a => a -> a -force = resugar - -desugarD :: Syntax a => a -> Data (Internal a) -desugarD = resugar - -sugarD :: Syntax a => Data (Internal a) -> a -sugarD = resugar - -share :: (Syntax a, Syntax b) => a -> (a -> b) -> b -share = sugarSym (letBind poly) - -instance (Type a, Num a) => Num (Data a) - where - fromInteger = value . fromInteger - abs = sugarSym Abs - signum = sugarSym Sign - (+) = sugarSym Add - (-) = sugarSym Sub - (*) = sugarSym Mul - -div :: (Type a, Integral a) => Data a -> Data a -> Data a -div = sugarSym Div - -mod :: (Type a, Integral a) => Data a -> Data a -> Data a -mod = sugarSym Mod - -(^) :: (Type a, Integral a) => Data a -> Data a -> Data a -(^) = sugarSym Exp - -instance (Type a, Fractional a) => Fractional (Data a) - where - fromRational = value . fromRational - (/) = sugarSym FDiv - -i2n :: (Type a, Integral a, Type b, Num b) => Data a -> Data b -i2n = sugarSym I2N - -f2i :: (Type a, Integral a) => Data Float -> Data a -f2i = sugarSym F2I - -b2i :: (Type a, Integral a) => Data Bool -> Data a -b2i = sugarSym B2I - -complex :: Data Float -> Data Float -> Data Complex -complex = sugarSym Complex - -realPart :: Data Complex -> Data Float -realPart = sugarSym RealPart - -imagPart :: Data Complex -> Data Float -imagPart = sugarSym ImagPart - -mkPolar :: Data Float -> Data Float -> Data Complex -mkPolar = sugarSym MkPolar - -magnitude :: Data Complex -> Data Float -magnitude = sugarSym Magnitude - -phase :: Data Complex -> Data Float -phase = sugarSym Phase - -polar :: Data Complex -> (Data Float, Data Float) -polar a = (magnitude a, phase a) - -cis :: Data Float -> Data Complex -cis = mkPolar 1 - - - -complement :: (Type a, Bits a) => Data a -> Data a -complement = sugarSym Complement - -(.&.) :: (Type a, Bits a) => Data a -> Data a -> Data a -(.&.) = sugarSym BitAnd - -(.|.) :: (Type a, Bits a) => Data a -> Data a -> Data a -(.|.) = sugarSym BitOr - -xor :: (Type a, Bits a) => Data a -> Data a -> Data a -xor = sugarSym Xor - -shiftL :: (Type a, Bits a) => Data a -> Data Index -> Data a -shiftL = sugarSym ShiftL - -shiftR :: (Type a, Bits a) => Data a -> Data Index -> Data a -shiftR = sugarSym ShiftR - -(<<), (>>) :: (Type a, Bits a) => Data a -> Data Index -> Data a -(<<) = shiftL -(>>) = shiftR - -infixl 5 <<, >> - -rotateL :: (Type a, Bits a) => Data a -> Data Index -> Data a -rotateL = sugarSym RotateL - -rotateR :: (Type a, Bits a) => Data a -> Data Index -> Data a -rotateR = sugarSym RotateR - -bitSize :: (Type a, Bits a) => Data a -> Data Index -bitSize = sugarSym BitSize - -reverseBits :: (Type a, Bits a) => Data a -> Data a -reverseBits = sugarSym ReverseBits - -(==) :: Type a => Data a -> Data a -> Data Bool -(==) = sugarSym Eq - -not :: Data Bool -> Data Bool -not = sugarSym Not - -(&&) :: Data Bool -> Data Bool -> Data Bool -(&&) = sugarSym And - -(||) :: Data Bool -> Data Bool -> Data Bool -(||) = sugarSym Or - -(<) :: (Type a, Ord a) => Data a -> Data a -> Data Bool -(<) = sugarSym Less - -(<=) :: (Type a, Ord a) => Data a -> Data a -> Data Bool -(<=) = sugarSym LEQ - -(>) :: (Type a, Ord a) => Data a -> Data a -> Data Bool -(>) = sugarSym Greater - -(>=) :: (Type a, Ord a) => Data a -> Data a -> Data Bool -(>=) = sugarSym GEQ - -max :: (Type a, Ord a) => Data a -> Data a -> Data a -max = sugarSym Max - -min :: (Type a, Ord a) => Data a -> Data a -> Data a -min = sugarSym Min - -(?) :: Syntax a => Data Bool -> (a,a) -> a -cond ? (t,e) = sugarSymCtx poly Condition cond t e - - - -parallel :: Type a => Data Length -> (Data Index -> Data a) -> Data [a] - -parallel len ixf - | getIx :$: arr :$: var0 <- body - , Just GetIx <- project getIx - , Just (Variable 0) <- prjCtx poly var0 - = setLength len $ Data arr - where - body = unData $ ixf $ Data $ inject (Variable 0 `withContext` poly) - -- This case is an optimization that's included because it has a great effect - -- on the size of the generated code. - -parallel len ixf = sugarSym Parallel len ixf - - - -sequential :: (Type a, Syntax st) => - Data Length -> st -> (Data Index -> st -> (Data a, st)) -> Data [a] -sequential = sugarSym Sequential - -forLoop :: Syntax st => Data Length -> st -> (Data Index -> st -> st) -> st -forLoop = sugarSym ForLoop - -getLength :: Type a => Data [a] -> Data Length -getLength = sugarSym GetLength - - - -setLength :: Type a => Data Length -> Data [a] -> Data [a] - -setLength (desugar -> ((project -> Just GetLength) :$: arr')) arr - | alphaEq poly (reify poly arr') (reify poly $ unData arr) - = arr - -- This case is an optimization that's needed for the optimization of - -- 'parallel' to work properly. - -setLength arr len = sugarSym SetLength arr len - - - -getIx :: Type a => Data [a] -> Data Index -> Data a -getIx = sugarSym GetIx - diff --git a/CEFP/MuFeldspar/Prelude.hs b/CEFP/MuFeldspar/Prelude.hs deleted file mode 100644 --- a/CEFP/MuFeldspar/Prelude.hs +++ /dev/null @@ -1,11 +0,0 @@ -module MuFeldspar.Prelude - ( module Prelude - ) where - -import Prelude hiding - ( (==), (&&), (||), (<), (<=), (>), (>=), (^), (++), (>>) - , div, max, min, mod, not - , concat, drop, length, map, replicate, reverse, splitAt, sum, take, unzip, zip - , zipWith - ) - diff --git a/CEFP/MuFeldspar/Vector.hs b/CEFP/MuFeldspar/Vector.hs deleted file mode 100644 --- a/CEFP/MuFeldspar/Vector.hs +++ /dev/null @@ -1,96 +0,0 @@ -{-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE GADTs #-} -{-# LANGUAGE MultiParamTypeClasses #-} -{-# LANGUAGE TypeFamilies #-} -{-# LANGUAGE TypeOperators #-} -{-# LANGUAGE TypeSynonymInstances #-} - -module MuFeldspar.Vector where - - - -import qualified Prelude - -import Language.Syntactic -import Language.Syntactic.Constructs.Binding.HigherOrder - -import MuFeldspar.Prelude -import MuFeldspar.Core -import MuFeldspar.Frontend - - - -data Vector a - where - Indexed :: {length :: Data Length, index :: Data Index -> a } -> Vector a - -instance Syntax a => Syntactic (Vector a) FeldDomainAll - where - type Internal (Vector a) = [Internal a] - desugar = desugar . freezeVector . map resugar - sugar = map resugar . unfreezeVector . sugar - -instance Functor Vector - where - fmap = map - - - -indexed :: Data Length -> (Data Index -> a) -> Vector a -indexed = Indexed - -freezeVector :: Type a => Vector (Data a) -> Data [a] -freezeVector vec = parallel (length vec) (index vec) - -unfreezeVector :: Type a => Data [a] -> Vector (Data a) -unfreezeVector arr = Indexed (getLength arr) (getIx arr) - -take :: Data Length -> Vector a -> Vector a -take n (Indexed l ixf) = indexed (min n l) ixf - -drop :: Data Length -> Vector a -> Vector a -drop n (Indexed l ixf) = indexed (max (l-n) 0) (ixf . (+n)) - -splitAt :: Data Index -> Vector a -> (Vector a, Vector a) -splitAt n vec = (take n vec, drop n vec) - -zip :: Vector a -> Vector b -> Vector (a,b) -zip a b = indexed (length a `min` length b) (\i -> (index a i, index b i)) - -unzip :: Vector (a,b) -> (Vector a, Vector b) -unzip ab = (indexed len (fst . index ab), indexed len (snd . index ab)) - where - len = length ab - -permute :: (Data Length -> Data Index -> Data Index) -> (Vector a -> Vector a) -permute perm vec = indexed len (index vec . perm len) - where - len = length vec - -reverse :: Vector a -> Vector a -reverse = permute $ \len i -> len-i-1 - -(...) :: (Type a, Integral a) => Data a -> Data a -> Vector (Data a) -l ... h = indexed (i2n $ h-l+1) ((+l) . i2n) - -replicate :: Data Index -> a -> Vector a -replicate len a = indexed len (const a) - -(++) :: Syntax a => Vector a -> Vector a -> Vector a -vec1 ++ vec2 = indexed len ixf - where - len = length vec1 + length vec2 - ixf i = i < length vec1 ? (index vec1 i, index vec2 (i-length vec1)) - -map :: (a -> b) -> Vector a -> Vector b -map f (Indexed len ixf) = indexed len (f . ixf) - -zipWith :: (a -> b -> c) -> Vector a -> Vector b -> Vector c -zipWith f a b = map (uncurry f) $ zip a b - -fold :: Syntax a => (a -> b -> a) -> a -> Vector b -> a -fold f a (Indexed len ixf) = forLoop len a (\i st -> f st (ixf i)) - -sum :: (Type a, Num a) => Vector (Data a) -> Data a -sum = fold (+) 0 - diff --git a/Examples/ALaCarte.hs b/Examples/ALaCarte.hs --- a/Examples/ALaCarte.hs +++ b/Examples/ALaCarte.hs @@ -56,20 +56,20 @@ -- Manual injection: addExample :: ASTF (Val :+: Add) Int -addExample = Symbol (InjectR Add) :$: Symbol (InjectL (Val 118)) :$: Symbol (InjectL (Val 1219)) +addExample = Sym (InjR Add) :$ Sym (InjL (Val 118)) :$ Sym (InjL (Val 1219)) -- Automatic injection: val :: (Val :<: expr) => Int -> ASTF expr Int -val = inject . Val +val = inj . Val (<+>) :: (Add :<: expr) => ASTF expr Int -> ASTF expr Int -> ASTF expr Int -a <+> b = inject Add :$: a :$: b +a <+> b = inj Add :$ a :$ b (<*>) :: (Mul :<: expr) => ASTF expr Int -> ASTF expr Int -> ASTF expr Int -a <*> b = inject Mul :$: a :$: b +a <*> b = inj Mul :$ a :$ b infixl 6 <+> infixl 7 <*> @@ -98,14 +98,14 @@ -- Pattern matching: -distr :: (Add :<: expr, Mul :<: expr, ConsType a) => AST expr a -> AST expr a -distr ((project -> Just Mul) :$: a :$: b) = case distr b of - (project -> Just Add) :$: c :$: d -> a' <*> c <+> a' <*> d +distr :: (Add :<: expr, Mul :<: expr) => AST expr a -> AST expr a +distr ((prj -> Just Mul) :$ a :$ b) = case distr b of + (prj -> Just Add) :$ c :$ d -> a' <*> c <+> a' <*> d b' -> a' <*> b' where a' = distr a -distr (f :$: a) = distr f :$: distr a -distr a = a +distr (f :$ a) = distr f :$ distr a +distr a = a -- Note the use of direct recursion instead of a fold combinator example5 :: ASTF (Val :+: Add :+: Mul) Int diff --git a/Examples/NanoFeldspar/Core.hs b/Examples/NanoFeldspar/Core.hs --- a/Examples/NanoFeldspar/Core.hs +++ b/Examples/NanoFeldspar/Core.hs @@ -15,8 +15,8 @@ -- types at which constructors operate. Currently, all general constructs (such -- as 'Literal' and 'Tuple') use a 'SimpleCtx' context, which means that the -- types are quite unrestricted. A real implementation would also probably use --- custom types for primitive functions, since the 'Sym' construct is quite --- unsafe (uses only a 'String' to distinguish between functions). +-- custom types for primitive functions, since 'Construct' is quite unsafe (uses +-- only a 'String' to distinguish between functions). module NanoFeldspar.Core where @@ -25,12 +25,13 @@ import Data.Typeable import Language.Syntactic -import Language.Syntactic.Constructs.Symbol -import Language.Syntactic.Constructs.Literal -import Language.Syntactic.Constructs.Condition -import Language.Syntactic.Constructs.Tuple +import Language.Syntactic.Interpretation.Semantics import Language.Syntactic.Constructs.Binding import Language.Syntactic.Constructs.Binding.HigherOrder +import Language.Syntactic.Constructs.Condition +import Language.Syntactic.Constructs.Construct +import Language.Syntactic.Constructs.Literal +import Language.Syntactic.Constructs.Tuple import Language.Syntactic.Sharing.SimpleCodeMotion @@ -69,20 +70,26 @@ where maybeWitnessSat = maybeWitnessSatDefault -instance IsSymbol Parallel +instance Semantic Parallel where - toSym Parallel = Sym "parallel" parallel - where - parallel len ixf = map ixf [0 .. len-1] + semantics Parallel = Sem + { semanticName = "parallel" + , semanticEval = \len ixf -> map ixf [0 .. len-1] + } -instance ExprEq Parallel where exprEq = exprEqSym; exprHash = exprHashSym -instance Render Parallel where renderPart = renderPartSym -instance Eval Parallel where evaluate = evaluateSym +instance ExprEq Parallel where exprEq = exprEqSem; exprHash = exprHashSem +instance Render Parallel where renderPart = renderPartSem +instance Eval Parallel where evaluate = evaluateSem instance ToTree Parallel instance EvalBind Parallel where evalBindSym = evalBindSymDefault +instance (AlphaEq dom dom dom env, Parallel :<: dom) => + AlphaEq Parallel Parallel dom env + where + alphaEqSym = alphaEqSymDefault + -------------------------------------------------------------------------------- -- * For loops -------------------------------------------------------------------------------- @@ -105,27 +112,34 @@ where maybeWitnessSat = maybeWitnessSatDefault -instance IsSymbol ForLoop +instance Semantic ForLoop where - toSym ForLoop = Sym "forLoop" forLoop - where - forLoop len init body = foldl (flip body) init [0 .. len-1] + semantics ForLoop = Sem + { semanticName = "forLoop" + , semanticEval = \len init body -> foldl (flip body) init [0 .. len-1] + } -instance ExprEq ForLoop where exprEq = exprEqSym; exprHash = exprHashSym -instance Render ForLoop where renderPart = renderPartSym -instance Eval ForLoop where evaluate = evaluateSym + +instance ExprEq ForLoop where exprEq = exprEqSem; exprHash = exprHashSem +instance Render ForLoop where renderPart = renderPartSem +instance Eval ForLoop where evaluate = evaluateSem instance ToTree ForLoop instance EvalBind ForLoop where evalBindSym = evalBindSymDefault +instance (AlphaEq dom dom dom env, ForLoop :<: dom) => + AlphaEq ForLoop ForLoop dom env + where + alphaEqSym = alphaEqSymDefault + -------------------------------------------------------------------------------- -- * Feldspar domain -------------------------------------------------------------------------------- -- | The Feldspar domain type FeldDomain - = Sym SimpleCtx + = Construct SimpleCtx :+: Literal SimpleCtx :+: Condition SimpleCtx :+: Tuple SimpleCtx @@ -157,15 +171,15 @@ -- | Print the expression printFeld :: Syntactic a FeldDomainAll => a -> IO () -printFeld = printExpr . reifySmart simpleCtx +printFeld = printExpr . reifySmart (const True) -- | Draw the syntax tree drawFeld :: Syntactic a FeldDomainAll => a -> IO () -drawFeld = drawAST . reifySmart simpleCtx +drawFeld = drawAST . reifySmart (const True) -- | Evaluation eval :: Syntactic a FeldDomainAll => a -> Internal a -eval = evalBind . reifySmart simpleCtx +eval = evalBind . reifySmart (const True) @@ -195,21 +209,20 @@ -- | Alpha equivalence instance Type a => Eq (Data a) where - Data a == Data b = - alphaEq simpleCtx (reify simpleCtx a) (reify simpleCtx b) + Data a == Data b = alphaEq (reify a) (reify b) instance Type a => Show (Data a) where - show (Data a) = render $ reify simpleCtx a + show (Data a) = render $ reify a instance (Type a, Num a) => Num (Data a) where fromInteger = value . fromInteger - abs = sugarSymCtx simpleCtx $ Sym "abs" abs - signum = sugarSymCtx simpleCtx $ Sym "signum" signum - (+) = sugarSymCtx simpleCtx $ Sym "(+)" (+) - (-) = sugarSymCtx simpleCtx $ Sym "(-)" (-) - (*) = sugarSymCtx simpleCtx $ Sym "(*)" (*) + abs = sugarSymCtx simpleCtx $ Construct "abs" abs + signum = sugarSymCtx simpleCtx $ Construct "signum" signum + (+) = sugarSymCtx simpleCtx $ Construct "(+)" (+) + (-) = sugarSymCtx simpleCtx $ Construct "(-)" (-) + (*) = sugarSymCtx simpleCtx $ Construct "(*)" (*) (?) :: Syntax a => Data Bool -> (a,a) -> a cond ? (t,e) = sugarSymCtx simpleCtx Condition cond t e @@ -222,11 +235,11 @@ forLoop = sugarSym ForLoop arrLength :: Type a => Data [a] -> Data Length -arrLength = sugarSymCtx simpleCtx $ Sym "arrLength" Prelude.length +arrLength = sugarSymCtx simpleCtx $ Construct "arrLength" Prelude.length -- | Array indexing getIx :: Type a => Data [a] -> Data Index -> Data a -getIx = sugarSymCtx simpleCtx $ Sym "getIx" eval +getIx = sugarSymCtx simpleCtx $ Construct "getIx" eval where eval as i | i >= len || i < 0 = error "getIx: index out of bounds" @@ -235,14 +248,14 @@ len = Prelude.length as not :: Data Bool -> Data Bool -not = sugarSymCtx simpleCtx $ Sym "not" Prelude.not +not = sugarSymCtx simpleCtx $ Construct "not" Prelude.not (==) :: Type a => Data a -> Data a -> Data Bool -(==) = sugarSymCtx simpleCtx $ Sym "(==)" (Prelude.==) +(==) = sugarSymCtx simpleCtx $ Construct "(==)" (Prelude.==) max :: Type a => Data a -> Data a -> Data a -max = sugarSymCtx simpleCtx $ Sym "max" Prelude.max +max = sugarSymCtx simpleCtx $ Construct "max" Prelude.max min :: Type a => Data a -> Data a -> Data a -min = sugarSymCtx simpleCtx $ Sym "min" Prelude.min +min = sugarSymCtx simpleCtx $ Construct "min" Prelude.min diff --git a/Examples/NanoFeldspar/Extra.hs b/Examples/NanoFeldspar/Extra.hs --- a/Examples/NanoFeldspar/Extra.hs +++ b/Examples/NanoFeldspar/Extra.hs @@ -1,3 +1,5 @@ +{-# OPTIONS_GHC -fcontext-stack=100 #-} + {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-} @@ -12,11 +14,11 @@ import Language.Syntactic -import Language.Syntactic.Constructs.Symbol -import Language.Syntactic.Constructs.Literal import Language.Syntactic.Constructs.Binding import Language.Syntactic.Constructs.Binding.HigherOrder import Language.Syntactic.Constructs.Binding.Optimize +import Language.Syntactic.Constructs.Construct +import Language.Syntactic.Constructs.Literal import Language.Syntactic.Sharing.Graph import Language.Syntactic.Sharing.ReifyHO @@ -79,5 +81,5 @@ _ -> expr drawFeldPart :: Syntactic a FeldDomainAll => a -> IO () -drawFeldPart = drawAST . optimize simpleCtx constFold . reify simpleCtx +drawFeldPart = drawAST . optimize simpleCtx constFold . reify diff --git a/Language/Syntactic.hs b/Language/Syntactic.hs --- a/Language/Syntactic.hs +++ b/Language/Syntactic.hs @@ -8,7 +8,6 @@ , module Language.Syntactic.Interpretation.Equality , module Language.Syntactic.Interpretation.Render , module Language.Syntactic.Interpretation.Evaluation - , module Language.Syntactic.Constructs.Annotate ) where @@ -17,5 +16,4 @@ import Language.Syntactic.Interpretation.Equality import Language.Syntactic.Interpretation.Render import Language.Syntactic.Interpretation.Evaluation -import Language.Syntactic.Constructs.Annotate diff --git a/Language/Syntactic/Constructs/Annotate.hs b/Language/Syntactic/Constructs/Annotate.hs deleted file mode 100644 --- a/Language/Syntactic/Constructs/Annotate.hs +++ /dev/null @@ -1,123 +0,0 @@ --- | Annotations for syntax trees - -module Language.Syntactic.Constructs.Annotate where - - - -import Data.Tree - -import Language.Syntactic.Syntax -import Language.Syntactic.Interpretation.Equality -import Language.Syntactic.Interpretation.Render -import Language.Syntactic.Interpretation.Evaluation - - - --- | Annotating an expression with arbitrary information. --- --- This can be used to annotate every node of a syntax tree, which is done by --- changing --- --- > AST dom a --- --- to --- --- > AST (Ann info dom) a --- --- Injection/projection of an annotated tree is done using --- 'injectAnn' / 'projectAnn'. -data Ann info expr a - where - Ann - :: { annInfo :: info (EvalResult a) - , annExpr :: expr a - } - -> Ann info expr a - -type AnnSTF info dom a = ASTF (Ann info dom) a - - - -instance WitnessCons dom => WitnessCons (Ann info dom) - where - witnessCons (Ann _ a) = witnessCons a - -instance WitnessSat expr => WitnessSat (Ann info expr) - where - type SatContext (Ann info expr) = SatContext expr - witnessSat (Ann _ a) = witnessSat a - -instance MaybeWitnessSat ctx dom => MaybeWitnessSat ctx (Ann info dom) - where - maybeWitnessSat ctx (Ann _ a) = maybeWitnessSat ctx a - -instance ExprEq expr => ExprEq (Ann info expr) - where - exprEq a b = annExpr a `exprEq` annExpr b - exprHash = exprHash . annExpr - -instance Render expr => Render (Ann info expr) - where - render = render . annExpr - -instance ToTree expr => ToTree (Ann info expr) - where - toTreePart args = toTreePart args . annExpr - -instance Eval expr => Eval (Ann info expr) - where - evaluate = evaluate . annExpr - - - -injectAnn :: (sub :<: sup, ConsType a) => - info (EvalResult a) -> sub a -> AST (Ann info sup) a -injectAnn info = Symbol . Ann info . inject - -projectAnn :: (sub :<: sup) => - AST (Ann info sup) a -> Maybe (info (EvalResult a), sub a) -projectAnn a = do - Symbol (Ann info b) <- return a - c <- project b - return (info, c) - --- | Get the annotation of the top-level node -getInfo :: AST (Ann info dom) a -> info (EvalResult a) -getInfo (Symbol (Ann info _)) = info -getInfo (f :$: _) = getInfo f - --- | Lift a function that operates on expressions with associated information to --- operate on an 'Ann' expression. This function is convenient to use together --- with e.g. 'queryNodeSimple' when the domain has the form @(`Ann` info dom)@. -liftAnn :: (expr a -> info (EvalResult a) -> b) -> (Ann info expr a -> b) -liftAnn f (Ann info a) = f a info - --- | Collect the annotations of all nodes -collectInfo :: (forall a . info a -> b) -> AST (Ann info dom) a -> [b] -collectInfo coll (Symbol (Ann info _)) = [coll info] -collectInfo coll (f :$: a) = collectInfo coll f ++ collectInfo coll a - --- | Rendering of annotated syntax trees -toTreeAnn :: forall info dom a . (Render info, ToTree dom) => - ASTF (Ann info dom) a -> Tree String -toTreeAnn a = mkTree [] a - where - mkTree :: [Tree String] -> AST (Ann info dom) b -> Tree String - mkTree args (Symbol (Ann info expr)) = Node infoStr [toTreePart args expr] - where - infoStr = "<<" ++ render info ++ ">>" - mkTree args (f :$: a) = mkTree (mkTree [] a : args) f - --- | Show an annotated syntax tree using ASCII art -showAnn :: (Render info, ToTree dom) => ASTF (Ann info dom) a -> String -showAnn = drawTree . toTreeAnn - --- | Print an annotated syntax tree using ASCII art -drawAnn :: (Render info, ToTree dom) => ASTF (Ann info dom) a -> IO () -drawAnn = putStrLn . showAnn - --- | Strip annotations from an 'AST' -stripAnn :: AST (Ann info dom) a -> AST dom a -stripAnn (Symbol (Ann _ a)) = Symbol a -stripAnn (f :$: a) = stripAnn f :$: stripAnn a - diff --git a/Language/Syntactic/Constructs/Binding.hs b/Language/Syntactic/Constructs/Binding.hs --- a/Language/Syntactic/Constructs/Binding.hs +++ b/Language/Syntactic/Constructs/Binding.hs @@ -1,4 +1,5 @@ {-# LANGUAGE OverlappingInstances #-} +{-# LANGUAGE UndecidableInstances #-} -- | General binding constructs @@ -6,7 +7,7 @@ -import Control.Monad.Identity +import qualified Control.Monad.Identity as Monad import Control.Monad.Reader import Data.Dynamic import Data.Ix @@ -16,11 +17,13 @@ import Data.Proxy import Language.Syntactic -import Language.Syntactic.Constructs.Symbol -import Language.Syntactic.Constructs.Literal import Language.Syntactic.Constructs.Condition -import Language.Syntactic.Constructs.Tuple +import Language.Syntactic.Constructs.Construct +import Language.Syntactic.Constructs.Decoration +import Language.Syntactic.Constructs.Identity +import Language.Syntactic.Constructs.Literal import Language.Syntactic.Constructs.Monad +import Language.Syntactic.Constructs.Tuple @@ -186,7 +189,7 @@ -- | Partial `Let` projection with explicit context prjLet :: (Let ctxa ctxb :<: sup) => Proxy ctxa -> Proxy ctxb -> sup a -> Maybe (Let ctxa ctxb a) -prjLet _ _ = project +prjLet _ _ = prj @@ -194,58 +197,50 @@ -- * Interpretation -------------------------------------------------------------------------------- --- | Alpha equivalence in an environment of variable equivalences. The supplied --- equivalence function gets called when the argument expressions are not both --- 'Variable's, both 'Lambda's or both ':$:'. -alphaEqM :: (Lambda ctx :<: dom, Variable ctx :<: dom) +-- | Capture-avoiding substitution +subst :: forall ctx dom a b + . (Lambda ctx :<: dom, Variable ctx :<: dom, Typeable a) => Proxy ctx - -> (forall a b . AST dom a -> AST dom b -> Reader [(VarId,VarId)] Bool) - -> (forall a b . AST dom a -> AST dom b -> Reader [(VarId,VarId)] Bool) - --- TODO This function is not ideal, since the type says nothing about which --- cases have been handled when calling 'eq'. - -alphaEqM ctx eq - ((prjCtx ctx -> Just (Lambda v1)) :$: a1) - ((prjCtx ctx -> Just (Lambda v2)) :$: a2) = - local ((v1,v2):) $ alphaEqM ctx eq a1 a2 - -alphaEqM ctx eq - (prjCtx ctx -> Just (Variable v1)) - (prjCtx ctx -> Just (Variable v2)) = do - env <- ask - case lookup v1 env of - Nothing -> return (v1==v2) -- Free variables - Just v2' -> return (v2==v2') - -alphaEqM ctx eq (f1 :$: a1) (f2 :$: a2) = do - e <- alphaEqM ctx eq f1 f2 - if e then alphaEqM ctx eq a1 a2 else return False - -alphaEqM _ eq a b = eq a b - - + -> VarId -- ^ Variable to be substituted + -> ASTF dom a -- ^ Expression to substitute for + -> ASTF dom b -- ^ Expression to substitute in + -> ASTF dom b +subst ctx v new a = go a + where + go :: AST dom c -> AST dom c + go a@((prjCtx ctx -> Just (Lambda w)) :$ _) + | v==w = a -- Capture + go (f :$ a) = go f :$ go a + go (prjCtx ctx -> Just (Variable w)) + | v==w + , Just new' <- gcast new + = new' + go a = a --- | Alpha-equivalence on lambda expressions. Free variables are taken to be --- equivalent if they have the same identifier. -alphaEq :: (Lambda ctx :<: dom, Variable ctx :<: dom, ExprEq dom) => - Proxy ctx -> AST dom a -> AST dom b -> Bool -alphaEq ctx a b = runReader (alphaEqM ctx (\a b -> return $ exprEq a b) a b) [] +-- | Beta-reduction of an expression. The expression to be reduced is assumed to +-- be a `Lambda`. +betaReduce :: forall ctx dom a b . (Lambda ctx :<: dom, Variable ctx :<: dom) + => Proxy ctx + -> ASTF dom a -- ^ Argument + -> ASTF dom (a -> b) -- ^ Function to be reduced + -> ASTF dom b +betaReduce ctx new ((prjCtx ctx -> Just (Lambda v)) :$ body) = + subst ctx v new body class EvalBind sub where evalBindSym - :: (EvalBind dom, ConsType a) + :: (EvalBind dom, Signature a) => sub a - -> HList (AST dom) a - -> Reader [(VarId,Dynamic)] (EvalResult a) + -> Args (AST dom) a + -> Reader [(VarId,Dynamic)] (DenResult a) instance (EvalBind sub1, EvalBind sub2) => EvalBind (sub1 :+: sub2) where - evalBindSym (InjectL a) = evalBindSym a - evalBindSym (InjectR a) = evalBindSym a + evalBindSym (InjL a) = evalBindSym a + evalBindSym (InjR a) = evalBindSym a -- | Evaluation of possibly open expressions evalBindM :: EvalBind dom => ASTF dom a -> Reader [(VarId,Dynamic)] a @@ -256,15 +251,16 @@ evalBind = flip runReader [] . evalBindM -- | Convenient default implementation of 'evalBindSym' -evalBindSymDefault :: (Eval sub, ConsType a, EvalBind dom) +evalBindSymDefault :: (Eval sub, Signature a, EvalBind dom) => sub a - -> HList (AST dom) a - -> Reader [(VarId,Dynamic)] (EvalResult a) + -> Args (AST dom) a + -> Reader [(VarId,Dynamic)] (DenResult a) evalBindSymDefault sym args = do - args' <- mapHListM (liftM (Identity . Full) . evalBindM) args - return $ appEvalHList (toEval $ evaluate sym) args' + args' <- mapArgsM (liftM (Monad.Identity . Full) . evalBindM) args + return $ appEvalArgs (toEval $ evaluate sym) args' -instance EvalBind (Sym ctx) where evalBindSym = evalBindSymDefault +instance EvalBind (Identity ctx) where evalBindSym = evalBindSymDefault +instance EvalBind (Construct ctx) where evalBindSym = evalBindSymDefault instance EvalBind (Literal ctx) where evalBindSym = evalBindSymDefault instance EvalBind (Condition ctx) where evalBindSym = evalBindSymDefault instance EvalBind (Tuple ctx) where evalBindSym = evalBindSymDefault @@ -272,13 +268,13 @@ instance EvalBind (Let ctxa ctxb) where evalBindSym = evalBindSymDefault instance Monad m => EvalBind (MONAD m) where evalBindSym = evalBindSymDefault -instance EvalBind dom => EvalBind (Ann info dom) +instance EvalBind dom => EvalBind (Decor info dom) where - evalBindSym (Ann _ a) args = evalBindSym a args + evalBindSym a args = evalBindSym (decorExpr a) args instance EvalBind (Lambda ctx) where - evalBindSym (Lambda v) (body :*: Nil) = do + evalBindSym (Lambda v) (body :* Nil) = do env <- ask return $ \a -> flip runReader ((v,toDyn a):env) @@ -293,4 +289,111 @@ Just a -> case fromDynamic a of Just a -> return a _ -> return $ error "evalBind: internal type error" + + + +-------------------------------------------------------------------------------- +-- * Alpha equivalence +-------------------------------------------------------------------------------- + +-- | Environments containing a list of variable equivalences +class VarEqEnv a + where + prjVarEqEnv :: a -> [(VarId,VarId)] + modVarEqEnv :: ([(VarId,VarId)] -> [(VarId,VarId)]) -> (a -> a) + +instance VarEqEnv [(VarId,VarId)] + where + prjVarEqEnv = id + modVarEqEnv = id + +class VarEqEnv env => AlphaEq sub1 sub2 dom env + where + alphaEqSym + :: (Signature a, Signature b) + => sub1 a + -> Args (AST dom) a + -> sub2 b + -> Args (AST dom) b + -> Reader env Bool + +instance (AlphaEq subA1 subB1 dom env, AlphaEq subA2 subB2 dom env) => + AlphaEq (subA1 :+: subA2) (subB1 :+: subB2) dom env + where + alphaEqSym (InjL a) aArgs (InjL b) bArgs = alphaEqSym a aArgs b bArgs + alphaEqSym (InjR a) aArgs (InjR b) bArgs = alphaEqSym a aArgs b bArgs + alphaEqSym (InjL a) aArgs (InjR b) bArgs = return False + alphaEqSym (InjR a) aArgs (InjL b) bArgs = return False + +alphaEqM :: AlphaEq dom dom dom env => + ASTF dom a -> ASTF dom b -> Reader env Bool +alphaEqM a b = queryNodeSimple (alphaEqM2 b) a + +alphaEqM2 :: (AlphaEq dom dom dom env, Signature a) => + ASTF dom b -> dom a -> Args (AST dom) a -> Reader env Bool +alphaEqM2 b a aArgs = queryNodeSimple (alphaEqSym a aArgs) b + +-- | Alpha-equivalence on lambda expressions. Free variables are taken to be +-- equivalent if they have the same identifier. +alphaEq :: AlphaEq dom dom dom [(VarId,VarId)] => + ASTF dom a -> ASTF dom b -> Bool +alphaEq a b = flip runReader ([] :: [(VarId,VarId)]) $ alphaEqM a b + +alphaEqSymDefault + :: ( ExprEq sub + , AlphaEq dom dom dom env + , Signature a + , Signature b + ) + => sub a + -> Args (AST dom) a + -> sub b + -> Args (AST dom) b + -> Reader env Bool +alphaEqSymDefault a aArgs b bArgs + | exprEq a b = alphaEqChildren a' b' + | otherwise = return False + where + a' = appArgs (Sym (undefined :: dom a)) aArgs + b' = appArgs (Sym (undefined :: dom b)) bArgs + +alphaEqChildren :: AlphaEq dom dom dom env => + AST dom a -> AST dom b -> Reader env Bool +alphaEqChildren (Sym _) (Sym _) = return True +alphaEqChildren (f :$ a) (g :$ b) = liftM2 (&&) + (alphaEqChildren f g) + (alphaEqM a b) +alphaEqChildren _ _ = return False + +instance AlphaEq dom dom dom env => AlphaEq (Identity ctx) (Identity ctx) dom env where alphaEqSym = alphaEqSymDefault +instance AlphaEq dom dom dom env => AlphaEq (Construct ctx) (Construct ctx) dom env where alphaEqSym = alphaEqSymDefault +instance AlphaEq dom dom dom env => AlphaEq (Literal ctx) (Literal ctx) dom env where alphaEqSym = alphaEqSymDefault +instance AlphaEq dom dom dom env => AlphaEq (Condition ctx) (Condition ctx) dom env where alphaEqSym = alphaEqSymDefault +instance AlphaEq dom dom dom env => AlphaEq (Tuple ctx) (Tuple ctx) dom env where alphaEqSym = alphaEqSymDefault +instance AlphaEq dom dom dom env => AlphaEq (Select ctx) (Select ctx) dom env where alphaEqSym = alphaEqSymDefault +instance AlphaEq dom dom dom env => AlphaEq (Let ctxa ctxb) (Let ctxa ctxb) dom env where alphaEqSym = alphaEqSymDefault + +instance (AlphaEq dom dom dom env, Monad m) => AlphaEq (MONAD m) (MONAD m) dom env + where + alphaEqSym = alphaEqSymDefault + +instance AlphaEq dom dom (Decor info dom) env => + AlphaEq (Decor info dom) (Decor info dom) (Decor info dom) env + where + alphaEqSym a aArgs b bArgs = + alphaEqSym (decorExpr a) aArgs (decorExpr b) bArgs + +instance AlphaEq dom dom dom env => AlphaEq (Lambda ctx) (Lambda ctx) dom env + where + alphaEqSym (Lambda v1) (body1 :* Nil) (Lambda v2) (body2 :* Nil) = + local (modVarEqEnv ((v1,v2):)) $ alphaEqM body1 body2 + +instance AlphaEq dom dom dom env => + AlphaEq (Variable ctx) (Variable ctx) dom env + where + alphaEqSym (Variable v1) Nil (Variable v2) Nil = do + env <- asks prjVarEqEnv + case lookup v1 env of + Nothing -> return (v1==v2) -- Free variables + Just v2' -> return (v2==v2') diff --git a/Language/Syntactic/Constructs/Binding/HigherOrder.hs b/Language/Syntactic/Constructs/Binding/HigherOrder.hs --- a/Language/Syntactic/Constructs/Binding/HigherOrder.hs +++ b/Language/Syntactic/Constructs/Binding/HigherOrder.hs @@ -50,7 +50,7 @@ lambda :: (Typeable a, Typeable b, Sat ctx a) => (ASTF (HODomain ctx dom) a -> ASTF (HODomain ctx dom) b) -> ASTF (HODomain ctx dom) (a -> b) -lambda = inject . HOLambda +lambda = inj . HOLambda instance ( Syntactic a (HODomain ctx dom) @@ -70,12 +70,12 @@ reifyM :: forall ctx dom a . Typeable a => AST (HODomain ctx dom) a -> State VarId (AST (Lambda ctx :+: Variable ctx :+: dom) a) -reifyM (f :$: a) = liftM2 (:$:) (reifyM f) (reifyM a) -reifyM (Symbol (InjectR a)) = return $ Symbol $ InjectR a -reifyM (Symbol (InjectL (HOLambda f))) = do +reifyM (f :$ a) = liftM2 (:$) (reifyM f) (reifyM a) +reifyM (Sym (InjR a)) = return $ Sym $ InjR a +reifyM (Sym (InjL (HOLambda f))) = do v <- get; put (v+1) - body <- reifyM $ f $ inject $ (Variable v `withContext` ctx) - return $ inject (Lambda v `withContext` ctx) :$: body + body <- reifyM $ f $ inj $ (Variable v `withContext` ctx) + return $ inj (Lambda v `withContext` ctx) :$ body where ctx = Proxy :: Proxy ctx @@ -89,8 +89,7 @@ -- | Reifying an n-ary syntactic function reify :: Syntactic a (HODomain ctx dom) - => Proxy ctx - -> a + => a -> ASTF (Lambda ctx :+: Variable ctx :+: dom) (Internal a) -reify _ = reifyTop . desugar +reify = reifyTop . desugar diff --git a/Language/Syntactic/Constructs/Binding/Optimize.hs b/Language/Syntactic/Constructs/Binding/Optimize.hs --- a/Language/Syntactic/Constructs/Binding/Optimize.hs +++ b/Language/Syntactic/Constructs/Binding/Optimize.hs @@ -11,11 +11,12 @@ import Data.Proxy import Language.Syntactic -import Language.Syntactic.Constructs.Symbol -import Language.Syntactic.Constructs.Literal +import Language.Syntactic.Constructs.Binding import Language.Syntactic.Constructs.Condition +import Language.Syntactic.Constructs.Construct +import Language.Syntactic.Constructs.Identity +import Language.Syntactic.Constructs.Literal import Language.Syntactic.Constructs.Tuple -import Language.Syntactic.Constructs.Binding @@ -48,8 +49,8 @@ :: Proxy ctx -> ConstFolder dom -> sub a - -> HList (AST dom) a - -> Writer (Set VarId) (ASTF dom (EvalResult a)) + -> Args (AST dom) a + -> Writer (Set VarId) (ASTF dom (DenResult a)) -- The reason for having @dom@ as a class parameter is that many instances -- require the constraint @(sub :<: dom)@. If @dom@ was forall-quantified in @@ -60,8 +61,8 @@ instance (Optimize sub1 ctx dom, Optimize sub2 ctx dom) => Optimize (sub1 :+: sub2) ctx dom where - optimizeSym ctx constFold (InjectL a) = optimizeSym ctx constFold a - optimizeSym ctx constFold (InjectR a) = optimizeSym ctx constFold a + optimizeSym ctx constFold (InjL a) = optimizeSym ctx constFold a + optimizeSym ctx constFold (InjR a) = optimizeSym ctx constFold a optimizeM :: Optimize dom ctx dom => Proxy ctx @@ -85,35 +86,36 @@ => Proxy ctx -> ConstFolder dom -> sub a - -> HList (AST dom) a - -> Writer (Set VarId) (ASTF dom (EvalResult a)) + -> Args (AST dom) a + -> Writer (Set VarId) (ASTF dom (DenResult a)) optimizeSymDefault ctx constFold sym@(witnessCons -> ConsWit) args = do - (args',vars) <- listen $ mapHListM (optimizeM ctx constFold) args - let result = appHList (Symbol $ inject sym) args' + (args',vars) <- listen $ mapArgsM (optimizeM ctx constFold) args + let result = appArgs (Sym $ inj sym) args' value = evalBind result if Set.null vars then return $ constFold result value else return result -instance (Sym ctx' :<: dom, Optimize dom ctx dom) => Optimize (Sym ctx') ctx dom where optimizeSym = optimizeSymDefault -instance (Literal ctx' :<: dom, Optimize dom ctx dom) => Optimize (Literal ctx') ctx dom where optimizeSym = optimizeSymDefault -instance (Tuple ctx' :<: dom, Optimize dom ctx dom) => Optimize (Tuple ctx') ctx dom where optimizeSym = optimizeSymDefault -instance (Select ctx' :<: dom, Optimize dom ctx dom) => Optimize (Select ctx') ctx dom where optimizeSym = optimizeSymDefault -instance (Let ctxa ctxb :<: dom, Optimize dom ctx dom) => Optimize (Let ctxa ctxb) ctx dom where optimizeSym = optimizeSymDefault +instance (Identity ctx' :<: dom, Optimize dom ctx dom) => Optimize (Identity ctx') ctx dom where optimizeSym = optimizeSymDefault +instance (Construct ctx' :<: dom, Optimize dom ctx dom) => Optimize (Construct ctx') ctx dom where optimizeSym = optimizeSymDefault +instance (Literal ctx' :<: dom, Optimize dom ctx dom) => Optimize (Literal ctx') ctx dom where optimizeSym = optimizeSymDefault +instance (Tuple ctx' :<: dom, Optimize dom ctx dom) => Optimize (Tuple ctx') ctx dom where optimizeSym = optimizeSymDefault +instance (Select ctx' :<: dom, Optimize dom ctx dom) => Optimize (Select ctx') ctx dom where optimizeSym = optimizeSymDefault +instance (Let ctxa ctxb :<: dom, Optimize dom ctx dom) => Optimize (Let ctxa ctxb) ctx dom where optimizeSym = optimizeSymDefault instance ( Condition ctx' :<: dom , Lambda ctx :<: dom , Variable ctx :<: dom - , ExprEq dom + , AlphaEq dom dom dom [(VarId,VarId)] , Optimize dom ctx dom ) => Optimize (Condition ctx') ctx dom where - optimizeSym ctx constFold cond@Condition args@(c :*: t :*: e :*: Nil) - | Set.null cVars = optimizeM ctx constFold t_or_e - | alphaEq ctx t e = optimizeM ctx constFold t - | otherwise = optimizeSymDefault ctx constFold cond args + optimizeSym ctx constFold cond@Condition args@(c :* t :* e :* Nil) + | Set.null cVars = optimizeM ctx constFold t_or_e + | alphaEq t e = optimizeM ctx constFold t + | otherwise = optimizeSymDefault ctx constFold cond args where (c',cVars) = runWriter $ optimizeM ctx constFold c t_or_e = if evalBind c' then t else e @@ -123,12 +125,12 @@ where optimizeSym _ _ var@(Variable v) Nil = do tell (singleton v) - return (inject var) + return (inj var) instance (Lambda ctx :<: dom, Optimize dom ctx dom) => Optimize (Lambda ctx) ctx dom where - optimizeSym ctx constFold lam@(Lambda v) (body :*: Nil) = do + optimizeSym ctx constFold lam@(Lambda v) (body :* Nil) = do body' <- censor (delete v) $ optimizeM ctx constFold body - return $ inject lam :$: body' + return $ inj lam :$ body' diff --git a/Language/Syntactic/Constructs/Condition.hs b/Language/Syntactic/Constructs/Condition.hs --- a/Language/Syntactic/Constructs/Condition.hs +++ b/Language/Syntactic/Constructs/Condition.hs @@ -6,12 +6,11 @@ -import Data.Hash import Data.Proxy import Data.Typeable import Language.Syntactic -import Language.Syntactic.Constructs.Symbol +import Language.Syntactic.Interpretation.Semantics @@ -36,12 +35,12 @@ where maybeWitnessSat _ _ = Nothing -instance IsSymbol (Condition ctx) +instance Semantic (Condition ctx) where - toSym Condition = Sym "condition" (\c t e -> if c then t else e) + semantics Condition = Sem "condition" (\c t e -> if c then t else e) -instance ExprEq (Condition ctx) where exprEq = exprEqSym; exprHash = exprHashSym -instance Render (Condition ctx) where renderPart = renderPartSym -instance Eval (Condition ctx) where evaluate = evaluateSym +instance ExprEq (Condition ctx) where exprEq = exprEqSem; exprHash = exprHashSem +instance Render (Condition ctx) where renderPart = renderPartSem +instance Eval (Condition ctx) where evaluate = evaluateSem instance ToTree (Condition ctx) diff --git a/Language/Syntactic/Constructs/Construct.hs b/Language/Syntactic/Constructs/Construct.hs new file mode 100644 --- /dev/null +++ b/Language/Syntactic/Constructs/Construct.hs @@ -0,0 +1,68 @@ +{-# LANGUAGE OverlappingInstances #-} + +-- | Provides a simple way to make syntactic constructs for prototyping. Note +-- that 'Construct' is quite unsafe as it only uses 'String' to distinguish +-- between different constructs. Also, 'Construct' has a very free type that +-- allows any number of arguments. + +module Language.Syntactic.Constructs.Construct where + + + +import Data.Typeable + +import Data.Hash +import Data.Proxy + +import Language.Syntactic + + + +data Construct ctx a + where + Construct :: (Signature a, Sat ctx (DenResult a)) => + String -> Denotation a -> Construct ctx a + +instance WitnessCons (Construct ctx) + where + witnessCons (Construct _ _) = ConsWit + +instance WitnessSat (Construct ctx) + where + type SatContext (Construct ctx) = ctx + witnessSat (Construct _ _) = SatWit + +instance MaybeWitnessSat ctx (Construct ctx) + where + maybeWitnessSat = maybeWitnessSatDefault + +instance MaybeWitnessSat ctx1 (Construct ctx2) + where + maybeWitnessSat _ _ = Nothing + +instance ExprEq (Construct ctx) + where + exprEq (Construct a _) (Construct b _) = a==b + exprHash (Construct name _) = hash name + +instance Render (Construct ctx) + where + renderPart [] (Construct name _) = name + renderPart args (Construct name _) + | isInfix = "(" ++ unwords [a,op,b] ++ ")" + | otherwise = "(" ++ unwords (name : args) ++ ")" + where + [a,b] = args + op = init $ tail name + isInfix + = not (null name) + && head name == '(' + && last name == ')' + && length args == 2 + +instance ToTree (Construct ctx) + +instance Eval (Construct ctx) + where + evaluate (Construct _ a) = fromEval a + diff --git a/Language/Syntactic/Constructs/Decoration.hs b/Language/Syntactic/Constructs/Decoration.hs new file mode 100644 --- /dev/null +++ b/Language/Syntactic/Constructs/Decoration.hs @@ -0,0 +1,158 @@ +-- | Construct for decorating expressions with additional information + +module Language.Syntactic.Constructs.Decoration where + + + +import Control.Monad.Identity +import Data.Tree + +import Data.Proxy + +import Language.Syntactic.Syntax +import Language.Syntactic.Interpretation.Equality +import Language.Syntactic.Interpretation.Evaluation +import Language.Syntactic.Interpretation.Render + + + +-------------------------------------------------------------------------------- +-- * Decoration +-------------------------------------------------------------------------------- + +-- | Decorating an expression with additional information +-- +-- One usage of 'Decor' is to decorate every node of a syntax tree. This is done +-- simply by changing +-- +-- > AST dom a +-- +-- to +-- +-- > AST (Decor info dom) a +-- +-- Injection\/projection of an decorated tree is done using 'injDecor' \/ +-- 'prjDecor'. +data Decor info expr a + where + Decor + :: { decorInfo :: info (DenResult a) + , decorExpr :: expr a + } + -> Decor info expr a + + + +instance WitnessCons dom => WitnessCons (Decor info dom) + where + witnessCons (Decor _ a) = witnessCons a + +instance WitnessSat expr => WitnessSat (Decor info expr) + where + type SatContext (Decor info expr) = SatContext expr + witnessSat (Decor _ a) = witnessSat a + +instance MaybeWitnessSat ctx dom => MaybeWitnessSat ctx (Decor info dom) + where + maybeWitnessSat ctx (Decor _ a) = maybeWitnessSat ctx a + +instance ExprEq expr => ExprEq (Decor info expr) + where + exprEq a b = decorExpr a `exprEq` decorExpr b + exprHash = exprHash . decorExpr + +instance Render expr => Render (Decor info expr) + where + renderPart args = renderPart args . decorExpr + render = render . decorExpr + +instance ToTree expr => ToTree (Decor info expr) + where + toTreePart args = toTreePart args . decorExpr + +instance Eval expr => Eval (Decor info expr) + where + evaluate = evaluate . decorExpr + + + +injDecor :: (sub :<: sup, Signature a) => + info (DenResult a) -> sub a -> AST (Decor info sup) a +injDecor info = Sym . Decor info . inj + +prjDecor :: (sub :<: sup) => + AST (Decor info sup) a -> Maybe (info (DenResult a), sub a) +prjDecor a = do + Sym (Decor info b) <- return a + c <- prj b + return (info, c) + +-- | 'injDecor' with explicit context +injDecorCtx :: (sub ctx :<: sup, Signature a) => + Proxy ctx -> info (DenResult a) -> sub ctx a -> AST (Decor info sup) a +injDecorCtx ctx info = Sym . Decor info . injCtx ctx + +-- | 'prjDecor' with explicit context +prjDecorCtx :: (sub ctx :<: sup) + => Proxy ctx -> AST (Decor info sup) a + -> Maybe (info (DenResult a), sub ctx a) +prjDecorCtx ctx a = do + Sym (Decor info b) <- return a + c <- prjCtx ctx b + return (info, c) + +-- | Get the decoration of the top-level node +getInfo :: AST (Decor info dom) a -> info (DenResult a) +getInfo (Sym (Decor info _)) = info +getInfo (f :$ _) = getInfo f + +-- | Update the decoration of the top-level node +updateDecor :: forall info dom a . + (info a -> info a) -> ASTF (Decor info dom) a -> ASTF (Decor info dom) a +updateDecor f = runIdentity . transformNode update + where + update + :: (Signature b, a ~ DenResult b) + => Decor info dom b + -> Args (AST (Decor info dom)) b + -> Identity (ASTF (Decor info dom) a) + update (Decor info a) args = Identity $ appArgs (Sym sym) args + where + sym = Decor (f info) a + +-- | Lift a function that operates on expressions with associated information to +-- operate on an 'Decor' expression. This function is convenient to use together +-- with e.g. 'queryNodeSimple' when the domain has the form +-- @(`Decor` info dom)@. +liftDecor :: (expr a -> info (DenResult a) -> b) -> (Decor info expr a -> b) +liftDecor f (Decor info a) = f a info + +-- | Collect the decorations of all nodes +collectInfo :: (forall a . info a -> b) -> AST (Decor info dom) a -> [b] +collectInfo coll (Sym (Decor info _)) = [coll info] +collectInfo coll (f :$ a) = collectInfo coll f ++ collectInfo coll a + +-- | Rendering of decorated syntax trees +toTreeDecor :: forall info dom a . (Render info, ToTree dom) => + ASTF (Decor info dom) a -> Tree String +toTreeDecor a = mkTree [] a + where + mkTree :: [Tree String] -> AST (Decor info dom) b -> Tree String + mkTree args (Sym (Decor info expr)) = Node infoStr [toTreePart args expr] + where + infoStr = "<<" ++ render info ++ ">>" + mkTree args (f :$ a) = mkTree (mkTree [] a : args) f + +-- | Show an decorated syntax tree using ASCII art +showDecor :: (Render info, ToTree dom) => ASTF (Decor info dom) a -> String +showDecor = drawTree . toTreeDecor + +-- | Print an decorated syntax tree using ASCII art +drawDecor :: (Render info, ToTree dom) => ASTF (Decor info dom) a -> IO () +drawDecor = putStrLn . showDecor + +-- | Strip decorations from an 'AST' +stripDecor :: AST (Decor info dom) a -> AST dom a +stripDecor (Sym (Decor _ a)) = Sym a +stripDecor (f :$ a) = stripDecor f :$ stripDecor a + diff --git a/Language/Syntactic/Constructs/Identity.hs b/Language/Syntactic/Constructs/Identity.hs new file mode 100644 --- /dev/null +++ b/Language/Syntactic/Constructs/Identity.hs @@ -0,0 +1,47 @@ +{-# LANGUAGE OverlappingInstances #-} + +-- | Identity function + +module Language.Syntactic.Constructs.Identity where + + + +import Data.Proxy +import Data.Typeable + +import Language.Syntactic +import Language.Syntactic.Interpretation.Semantics + + + +-- | Identity function +data Identity ctx a + where + Id :: Sat ctx a => Identity ctx (a :-> Full a) + +instance WitnessCons (Identity ctx) + where + witnessCons Id = ConsWit + +instance WitnessSat (Identity ctx) + where + type SatContext (Identity ctx) = ctx + witnessSat Id = SatWit + +instance MaybeWitnessSat ctx (Identity ctx) + where + maybeWitnessSat = maybeWitnessSatDefault + +instance MaybeWitnessSat ctx1 (Identity ctx2) + where + maybeWitnessSat _ _ = Nothing + +instance Semantic (Identity ctx) + where + semantics Id = Sem "id" id + +instance ExprEq (Identity ctx) where exprEq = exprEqSem; exprHash = exprHashSem +instance Render (Identity ctx) where renderPart = renderPartSem +instance Eval (Identity ctx) where evaluate = evaluateSem +instance ToTree (Identity ctx) + diff --git a/Language/Syntactic/Constructs/Monad.hs b/Language/Syntactic/Constructs/Monad.hs --- a/Language/Syntactic/Constructs/Monad.hs +++ b/Language/Syntactic/Constructs/Monad.hs @@ -7,7 +7,7 @@ import Control.Monad import Language.Syntactic -import Language.Syntactic.Constructs.Symbol +import Language.Syntactic.Interpretation.Semantics import Data.Proxy @@ -31,19 +31,19 @@ where maybeWitnessSat _ _ = Nothing -instance Monad m => IsSymbol (MONAD m) +instance Monad m => Semantic (MONAD m) where - toSym Return = Sym "return" return - toSym Bind = Sym "bind" (>>=) - toSym Then = Sym "then" (>>) - toSym When = Sym "when" when + semantics Return = Sem "return" return + semantics Bind = Sem "bind" (>>=) + semantics Then = Sem "then" (>>) + semantics When = Sem "when" when -instance Monad m => ExprEq (MONAD m) where exprEq = exprEqSym; exprHash = exprHashSym -instance Monad m => Render (MONAD m) where renderPart = renderPartSym -instance Monad m => Eval (MONAD m) where evaluate = evaluateSym +instance Monad m => ExprEq (MONAD m) where exprEq = exprEqSem; exprHash = exprHashSem +instance Monad m => Render (MONAD m) where renderPart = renderPartSem +instance Monad m => Eval (MONAD m) where evaluate = evaluateSem instance Monad m => ToTree (MONAD m) -- | Projection with explicit monad type prjMonad :: (MONAD m :<: sup) => Proxy (m ()) -> sup a -> Maybe (MONAD m a) -prjMonad _ = project +prjMonad _ = prj diff --git a/Language/Syntactic/Constructs/Symbol.hs b/Language/Syntactic/Constructs/Symbol.hs deleted file mode 100644 --- a/Language/Syntactic/Constructs/Symbol.hs +++ /dev/null @@ -1,93 +0,0 @@ -{-# LANGUAGE OverlappingInstances #-} - --- | Generic symbols --- --- 'Sym' provides a simple way to make syntactic symbols for prototyping. --- However, note that 'Sym' is quite unsafe as it only uses 'String' to --- distinguish between different symbols. Also, 'Sym' has a very free type that --- allows any number of arguments. - -module Language.Syntactic.Constructs.Symbol where - - - -import Data.Typeable - -import Data.Hash -import Data.Proxy - -import Language.Syntactic - - - -data Sym ctx a - where - Sym :: (ConsType a, Sat ctx (EvalResult a)) => - String -> ConsEval a -> Sym ctx a - -instance WitnessCons (Sym ctx) - where - witnessCons (Sym _ _) = ConsWit - -instance WitnessSat (Sym ctx) - where - type SatContext (Sym ctx) = ctx - witnessSat (Sym _ _) = SatWit - -instance MaybeWitnessSat ctx (Sym ctx) - where - maybeWitnessSat = maybeWitnessSatDefault - -instance MaybeWitnessSat ctx1 (Sym ctx2) - where - maybeWitnessSat _ _ = Nothing - -instance ExprEq (Sym ctx) - where - exprEq (Sym a _) (Sym b _) = a==b - exprHash (Sym name _) = hash name - -instance Render (Sym ctx) - where - renderPart [] (Sym name _) = name - renderPart args (Sym name _) - | isInfix = "(" ++ unwords [a,op,b] ++ ")" - | otherwise = "(" ++ unwords (name : args) ++ ")" - where - [a,b] = args - op = init $ tail name - isInfix - = not (null name) - && head name == '(' - && last name == ')' - && length args == 2 - -instance ToTree (Sym ctx) - -instance Eval (Sym ctx) - where - evaluate (Sym _ a) = fromEval a - - - --- | Class of expressions that can be treated as symbols -class IsSymbol expr - where - toSym :: expr a -> Sym Poly a - --- | Default implementation of 'exprEq' -exprEqSym :: IsSymbol expr => expr a -> expr b -> Bool -exprEqSym a b = exprEq (toSym a) (toSym b) - --- | Default implementation of 'exprHash' -exprHashSym :: IsSymbol expr => expr a -> Hash -exprHashSym = exprHash . toSym - --- | Default implementation of 'renderPart' -renderPartSym :: IsSymbol expr => [String] -> expr a -> String -renderPartSym args = renderPart args . toSym - --- | Default implementation of 'evaluate' -evaluateSym :: IsSymbol expr => expr a -> a -evaluateSym = evaluate . toSym - diff --git a/Language/Syntactic/Constructs/Tuple.hs b/Language/Syntactic/Constructs/Tuple.hs --- a/Language/Syntactic/Constructs/Tuple.hs +++ b/Language/Syntactic/Constructs/Tuple.hs @@ -17,13 +17,12 @@ -import Data.Hash import Data.Proxy import Data.Tuple.Curry import Data.Tuple.Select import Language.Syntactic -import Language.Syntactic.Constructs.Symbol +import Language.Syntactic.Interpretation.Semantics @@ -68,18 +67,18 @@ where maybeWitnessSat _ _ = Nothing -instance IsSymbol (Tuple ctx) +instance Semantic (Tuple ctx) where - toSym Tup2 = Sym "tup2" (,) - toSym Tup3 = Sym "tup3" (,,) - toSym Tup4 = Sym "tup4" (,,,) - toSym Tup5 = Sym "tup5" (,,,,) - toSym Tup6 = Sym "tup6" (,,,,,) - toSym Tup7 = Sym "tup7" (,,,,,,) + semantics Tup2 = Sem "tup2" (,) + semantics Tup3 = Sem "tup3" (,,) + semantics Tup4 = Sem "tup4" (,,,) + semantics Tup5 = Sem "tup5" (,,,,) + semantics Tup6 = Sem "tup6" (,,,,,) + semantics Tup7 = Sem "tup7" (,,,,,,) -instance ExprEq (Tuple ctx) where exprEq = exprEqSym; exprHash = exprHashSym -instance Render (Tuple ctx) where renderPart = renderPartSym -instance Eval (Tuple ctx) where evaluate = evaluateSym +instance ExprEq (Tuple ctx) where exprEq = exprEqSem; exprHash = exprHashSem +instance Render (Tuple ctx) where renderPart = renderPartSem +instance Eval (Tuple ctx) where evaluate = evaluateSem instance ToTree (Tuple ctx) @@ -256,19 +255,19 @@ where maybeWitnessSat _ _ = Nothing -instance IsSymbol (Select ctx) +instance Semantic (Select ctx) where - toSym Sel1 = Sym "sel1" sel1 - toSym Sel2 = Sym "sel2" sel2 - toSym Sel3 = Sym "sel3" sel3 - toSym Sel4 = Sym "sel4" sel4 - toSym Sel5 = Sym "sel5" sel5 - toSym Sel6 = Sym "sel6" sel6 - toSym Sel7 = Sym "sel7" sel7 + semantics Sel1 = Sem "sel1" sel1 + semantics Sel2 = Sem "sel2" sel2 + semantics Sel3 = Sem "sel3" sel3 + semantics Sel4 = Sem "sel4" sel4 + semantics Sel5 = Sem "sel5" sel5 + semantics Sel6 = Sem "sel6" sel6 + semantics Sel7 = Sem "sel7" sel7 -instance ExprEq (Select ctx) where exprEq = exprEqSym; exprHash = exprHashSym -instance Render (Select ctx) where renderPart = renderPartSym -instance Eval (Select ctx) where evaluate = evaluateSym +instance ExprEq (Select ctx) where exprEq = exprEqSem; exprHash = exprHashSem +instance Render (Select ctx) where renderPart = renderPartSem +instance Eval (Select ctx) where evaluate = evaluateSem instance ToTree (Select ctx) -- | Return the selected position, e.g. diff --git a/Language/Syntactic/Interpretation/Equality.hs b/Language/Syntactic/Interpretation/Equality.hs --- a/Language/Syntactic/Interpretation/Equality.hs +++ b/Language/Syntactic/Interpretation/Equality.hs @@ -26,12 +26,12 @@ instance ExprEq dom => ExprEq (AST dom) where - exprEq (Symbol a) (Symbol b) = exprEq a b - exprEq (f1 :$: a1) (f2 :$: a2) = exprEq f1 f2 && exprEq a1 a2 + exprEq (Sym a) (Sym b) = exprEq a b + exprEq (f1 :$ a1) (f2 :$ a2) = exprEq f1 f2 && exprEq a1 a2 exprEq _ _ = False - exprHash (Symbol a) = hashInt 0 `combine` exprHash a - exprHash (f :$: a) = hashInt 1 `combine` exprHash f `combine` exprHash a + exprHash (Sym a) = hashInt 0 `combine` exprHash a + exprHash (f :$ a) = hashInt 1 `combine` exprHash f `combine` exprHash a instance ExprEq dom => Eq (AST dom a) where @@ -39,12 +39,12 @@ instance (ExprEq expr1, ExprEq expr2) => ExprEq (expr1 :+: expr2) where - exprEq (InjectL a) (InjectL b) = exprEq a b - exprEq (InjectR a) (InjectR b) = exprEq a b + exprEq (InjL a) (InjL b) = exprEq a b + exprEq (InjR a) (InjR b) = exprEq a b exprEq _ _ = False - exprHash (InjectL a) = hashInt 0 `combine` exprHash a - exprHash (InjectR a) = hashInt 1 `combine` exprHash a + exprHash (InjL a) = hashInt 0 `combine` exprHash a + exprHash (InjR a) = hashInt 1 `combine` exprHash a instance (ExprEq expr1, ExprEq expr2) => Eq ((expr1 :+: expr2) a) where diff --git a/Language/Syntactic/Interpretation/Evaluation.hs b/Language/Syntactic/Interpretation/Evaluation.hs --- a/Language/Syntactic/Interpretation/Evaluation.hs +++ b/Language/Syntactic/Interpretation/Evaluation.hs @@ -13,13 +13,13 @@ instance Eval dom => Eval (AST dom) where - evaluate (Symbol a) = evaluate a - evaluate (f :$: a) = evaluate f $: result (evaluate a) + evaluate (Sym a) = evaluate a + evaluate (f :$ a) = evaluate f $: result (evaluate a) instance (Eval expr1, Eval expr2) => Eval (expr1 :+: expr2) where - evaluate (InjectL a) = evaluate a - evaluate (InjectR a) = evaluate a + evaluate (InjL a) = evaluate a + evaluate (InjR a) = evaluate a evalFull :: Eval dom => ASTF dom a -> a evalFull = result . evaluate diff --git a/Language/Syntactic/Interpretation/Render.hs b/Language/Syntactic/Interpretation/Render.hs --- a/Language/Syntactic/Interpretation/Render.hs +++ b/Language/Syntactic/Interpretation/Render.hs @@ -30,8 +30,8 @@ instance Render dom => Render (AST dom) where - renderPart args (Symbol a) = renderPart args a - renderPart args (f :$: a) = renderPart (render a : args) f + renderPart args (Sym a) = renderPart args a + renderPart args (f :$ a) = renderPart (render a : args) f instance Render dom => Show (AST dom a) where @@ -39,8 +39,8 @@ instance (Render expr1, Render expr2) => Render (expr1 :+: expr2) where - renderPart args (InjectL a) = renderPart args a - renderPart args (InjectR a) = renderPart args a + renderPart args (InjL a) = renderPart args a + renderPart args (InjR a) = renderPart args a instance (Render expr1, Render expr2) => Show ((expr1 :+: expr2) a) where @@ -61,13 +61,13 @@ instance ToTree dom => ToTree (AST dom) where - toTreePart args (Symbol a) = toTreePart args a - toTreePart args (f :$: a) = toTreePart (toTree a : args) f + toTreePart args (Sym a) = toTreePart args a + toTreePart args (f :$ a) = toTreePart (toTree a : args) f instance (ToTree expr1, ToTree expr2) => ToTree (expr1 :+: expr2) where - toTreePart args (InjectL a) = toTreePart args a - toTreePart args (InjectR a) = toTreePart args a + toTreePart args (InjL a) = toTreePart args a + toTreePart args (InjR a) = toTreePart args a -- | Convert an expression to a syntax tree toTree :: ToTree expr => expr a -> Tree String diff --git a/Language/Syntactic/Interpretation/Semantics.hs b/Language/Syntactic/Interpretation/Semantics.hs new file mode 100644 --- /dev/null +++ b/Language/Syntactic/Interpretation/Semantics.hs @@ -0,0 +1,76 @@ +-- | Default implementations of some interpretation functions + +module Language.Syntactic.Interpretation.Semantics where + + + +import Data.Typeable + +import Data.Hash +import Data.Proxy + +import Language.Syntactic + + + +-- | A representation of a syntactic construct as a 'String' and an evaluation +-- function. It is not meant to be used as a syntactic symbol in an 'AST'. Its +-- only purpose is to provide the default implementations of functions like +-- `exprEq` via the `Semantic` class. +data Semantics a + where + Sem :: Signature a + => { semanticName :: String + , semanticEval :: Denotation a + } + -> Semantics a + + + +instance ExprEq Semantics + where + exprEq (Sem a _) (Sem b _) = a==b + exprHash (Sem name _) = hash name + +instance Render Semantics + where + renderPart [] (Sem name _) = name + renderPart args (Sem name _) + | isInfix = "(" ++ unwords [a,op,b] ++ ")" + | otherwise = "(" ++ unwords (name : args) ++ ")" + where + [a,b] = args + op = init $ tail name + isInfix + = not (null name) + && head name == '(' + && last name == ')' + && length args == 2 + +instance Eval Semantics + where + evaluate (Sem _ a) = fromEval a + + + +-- | Class of expressions that can be treated as constructs +class Semantic expr + where + semantics :: expr a -> Semantics a + +-- | Default implementation of 'exprEq' +exprEqSem :: Semantic expr => expr a -> expr b -> Bool +exprEqSem a b = exprEq (semantics a) (semantics b) + +-- | Default implementation of 'exprHash' +exprHashSem :: Semantic expr => expr a -> Hash +exprHashSem = exprHash . semantics + +-- | Default implementation of 'renderPart' +renderPartSem :: Semantic expr => [String] -> expr a -> String +renderPartSem args = renderPart args . semantics + +-- | Default implementation of 'evaluate' +evaluateSem :: Semantic expr => expr a -> a +evaluateSem = evaluate . semantics + diff --git a/Language/Syntactic/Sharing/Graph.hs b/Language/Syntactic/Sharing/Graph.hs --- a/Language/Syntactic/Sharing/Graph.hs +++ b/Language/Syntactic/Sharing/Graph.hs @@ -1,3 +1,5 @@ +{-# LANGUAGE UndecidableInstances #-} + -- | Representation and manipulation of abstract syntax graphs module Language.Syntactic.Sharing.Graph where @@ -63,6 +65,52 @@ +-- | Environment for alpha-equivalence +class NodeEqEnv dom a + where + prjNodeEqEnv :: a -> NodeEnv dom + modNodeEqEnv :: (NodeEnv dom -> NodeEnv dom) -> (a -> a) + +type EqEnv dom = ([(VarId,VarId)], NodeEnv dom) + +type NodeEnv dom = + ( Array NodeId Hash + , Array NodeId (SomeAST dom) + ) + +instance NodeEqEnv dom (EqEnv dom) + where + prjNodeEqEnv = snd + modNodeEqEnv f = (id *** f) + +instance VarEqEnv (EqEnv dom) + where + prjVarEqEnv = fst + modVarEqEnv f = (f *** id) + +instance (AlphaEq dom dom dom env, NodeEqEnv dom env) => + AlphaEq (Node ctx) (Node ctx) dom env + where + alphaEqSym (Node n1) Nil (Node n2) Nil + | n1 == n2 = return True + | otherwise = do + (hTab,nTab) :: NodeEnv dom <- asks prjNodeEqEnv + if hTab!n1 /= hTab!n2 + then return False + else case (nTab!n1, nTab!n2) of + (SomeAST a, SomeAST b) -> alphaEqM a b + -- TODO The result could be memoized in a + -- @Map (NodeId,NodeId) Bool@ + + -- TODO With only this instance, the result will be 'False' when one argument + -- is a 'Node' and the other one isn't. This is not really correct since + -- 'Node's are just meta-variables and shouldn't be part of the + -- comparison. But as long as equivalent expressions always have 'Node's + -- at the same position, it doesn't matter. This could probably be fixed + -- by adding two overlapping instances. + + + -- | \"Abstract Syntax Graph\" -- -- A representation of a syntax tree with explicit sharing. An 'ASG' is valid if @@ -97,10 +145,8 @@ -- function reindexNodesAST :: (NodeId -> NodeId) -> AST (Node ctx :+: dom) a -> AST (Node ctx :+: dom) a -reindexNodesAST reix (Symbol (InjectL (Node n))) = - Symbol (InjectL (Node $ reix n)) -reindexNodesAST reix (f :$: a) = - reindexNodesAST reix f :$: reindexNodesAST reix a +reindexNodesAST reix (Sym (InjL (Node n))) = Sym (InjL (Node $ reix n)) +reindexNodesAST reix (f :$ a) = reindexNodesAST reix f :$ reindexNodesAST reix a reindexNodesAST reix a = a -- | Reindex the nodes according to the given index mapping. The number of nodes @@ -175,10 +221,10 @@ nodes = [(n, g expr) | (n, SomeAST expr) <- ns] arr = array (0, nn-1) nodes - g :: ConsType c => AST (Node ctx :+: dom) c -> b - g (h :$: a) = alg $ AppPF (g h) (g a) - g (Symbol (InjectL (Node n)) ) = alg $ NodePF n (arr!n) - g (Symbol (InjectR a)) = alg $ DomPF a + g :: Signature c => AST (Node ctx :+: dom) c -> b + g (h :$ a) = alg $ AppPF (g h) (g a) + g (Sym (InjL (Node n)) ) = alg $ NodePF n (arr!n) + g (Sym (InjR a)) = alg $ DomPF a @@ -192,14 +238,14 @@ where nodeMap = array (0, n-1) nodes - inline :: forall b. (Typeable b, ConsType b) => + inline :: forall b. (Typeable b, Signature b) => AST (Node ctx :+: dom) b -> AST dom b - inline (f :$: a) = inline f :$: inline a - inline (Symbol (InjectL (Node n))) = case nodeMap ! n of + inline (f :$ a) = inline f :$ inline a + inline (Sym (InjL (Node n))) = case nodeMap ! n of SomeAST a -> case gcast a of Nothing -> error "inlineAll: type mismatch" Just a -> inline a - inline (Symbol (InjectR a)) = Symbol a + inline (Sym (InjR a)) = Sym a @@ -231,16 +277,16 @@ nodes' = [(n, SomeAST (inline a)) | (n, SomeAST a) <- nodes, occs!n > 1] n' = genericLength nodes' - inline :: forall b. (Typeable b, ConsType b) => + inline :: forall b. (Typeable b, Signature b) => AST (Node ctx :+: dom) b -> AST (Node ctx :+: dom) b - inline (f :$: a) = inline f :$: inline a - inline (Symbol (InjectL (Node n))) - | occs!n > 1 = Symbol (InjectL (Node n)) + inline (f :$ a) = inline f :$ inline a + inline (Sym (InjL (Node n))) + | occs!n > 1 = Sym (InjL (Node n)) | otherwise = case nodeTab ! n of SomeAST a -> case gcast a of Nothing -> error "inlineSingle: type mismatch" Just a -> inline a - inline (Symbol (InjectR a)) = Symbol (InjectR a) + inline (Sym (InjR a)) = Sym (InjR a) @@ -263,7 +309,9 @@ -- | Partitions the nodes such that two nodes are in the same sub-list if and -- only if they are alpha-equivalent. partitionNodes :: forall ctx dom a - . (Lambda ctx :<: dom, Variable ctx :<: dom, ExprEq dom) + . ( ExprEq dom + , AlphaEq dom dom (Node ctx :+: dom) (EqEnv (Node ctx :+: dom)) + ) => ASG ctx dom a -> [[NodeId]] partitionNodes graph = concatMap (fullPartition nodeEq) approxPartitioning where @@ -274,45 +322,24 @@ -- are guaranteed to be inequivalent, while nodes in the same partition -- might be equivalent. approxPartitioning - = map (map fst) - $ groupBy ((==) `on` snd) - $ sortBy (compare `on` snd) - $ hashes - - eqNode :: forall a b . ExprEq dom - => AST (Node ctx :+: dom) a - -> AST (Node ctx :+: dom) b - -> Reader [(VarId,VarId)] Bool - eqNode (Symbol (InjectL (Node n1))) (Symbol (InjectL (Node n2))) - | n1 == n2 = return True - | hTab!n1 /= hTab!n2 = return False - | otherwise = case (nTab!n1, nTab!n2) of - (SomeAST a, SomeAST b) -> eqNodeAlpha a b - -- TODO The result could be memoized in a - -- @Map (NodeId,NodeId) Bool@ - eqNode (Symbol (InjectR a)) (Symbol (InjectR b)) = return (exprEq a b) - eqNode _ _ = return False - -- Returns 'False' when one argument is a 'Node' and the other one isn't. - -- This is not really correct since 'Node's are just meta-variables and - -- shouldn't be part of the comparison. But as long as equivalent - -- expressions always have 'Node's at the same position, it doesn't matter. - -- This is just for simplicity; it would be easy to fix. - - -- | Alpha-equivalence for expressions with 'Node's - eqNodeAlpha :: forall a b - . AST (Node ctx :+: dom) a - -> AST (Node ctx :+: dom) b - -> Reader [(VarId,VarId)] Bool - eqNodeAlpha a b = alphaEqM (Proxy::Proxy ctx) eqNode a b + = map (map fst) + $ groupBy ((==) `on` snd) + $ sortBy (compare `on` snd) + $ hashes nodeEq :: NodeId -> NodeId -> Bool - nodeEq n1 n2 = runReader (liftSome2 eqNodeAlpha (nTab!n1) (nTab!n2)) [] + nodeEq n1 n2 = runReader + (liftSome2 alphaEqM (nTab!n1) (nTab!n2)) + (([],(hTab,nTab)) :: EqEnv (Node ctx :+: dom)) -- | Common sub-expression elimination based on alpha-equivalence -cse :: (Lambda ctx :<: dom, Variable ctx :<: dom, ExprEq dom) => - ASG ctx dom a -> ASG ctx dom a +cse + :: ( ExprEq dom + , AlphaEq dom dom (Node ctx :+: dom) (EqEnv (Node ctx :+: dom)) + ) + => ASG ctx dom a -> ASG ctx dom a cse graph@(ASG top nodes n) = nubNodes $ reindexNodes (reixTab!) graph where parts = partitionNodes graph diff --git a/Language/Syntactic/Sharing/Reify.hs b/Language/Syntactic/Sharing/Reify.hs --- a/Language/Syntactic/Sharing/Reify.hs +++ b/Language/Syntactic/Sharing/Reify.hs @@ -47,17 +47,17 @@ st <- liftIO $ makeStableName a hist <- liftIO $ readIORef history case lookHistory hist (StName st) of - Just n -> return $ Symbol $ InjectL $ Node n + Just n -> return $ Sym $ InjL $ Node n _ -> do n <- fresh nSupp liftIO $ modifyIORef history $ remember (StName st) n a' <- reifyRec a tell [(n, SomeAST a')] - return $ Symbol $ InjectL $ Node n + return $ Sym $ InjL $ Node n reifyRec :: AST dom b -> GraphMonad ctx dom b - reifyRec (f :$: a) = liftM2 (:$:) (reifyRec f) (reifyNode a) - reifyRec (Symbol a) = return $ Symbol (InjectR a) + reifyRec (f :$ a) = liftM2 (:$) (reifyRec f) (reifyNode a) + reifyRec (Sym a) = return $ Sym (InjR a) diff --git a/Language/Syntactic/Sharing/ReifyHO.hs b/Language/Syntactic/Sharing/ReifyHO.hs --- a/Language/Syntactic/Sharing/ReifyHO.hs +++ b/Language/Syntactic/Sharing/ReifyHO.hs @@ -63,21 +63,21 @@ st <- liftIO $ makeStableName a hist <- liftIO $ readIORef history case lookHistory hist (StName st) of - Just n -> return $ Symbol $ InjectL $ Node n + Just n -> return $ Sym $ InjL $ Node n _ -> do n <- fresh nSupp liftIO $ modifyIORef history $ remember (StName st) n a' <- reifyRec a tell [(n, SomeAST a')] - return $ Symbol $ InjectL $ Node n + return $ Sym $ InjL $ Node n reifyRec :: AST (HODomain ctx dom) b -> GraphMonad ctx dom b - reifyRec (f :$: a) = liftM2 (:$:) (reifyRec f) (reifyNode a) - reifyRec (Symbol (InjectR a)) = return $ Symbol (InjectR (InjectR a)) - reifyRec (Symbol (InjectL (HOLambda f))) = do + reifyRec (f :$ a) = liftM2 (:$) (reifyRec f) (reifyNode a) + reifyRec (Sym (InjR a)) = return $ Sym (InjR (InjR a)) + reifyRec (Sym (InjL (HOLambda f))) = do v <- fresh vSupp - body <- reifyNode $ f $ inject $ (Variable v `withContext` ctx) - return $ inject (Lambda v `withContext` ctx) :$: body + body <- reifyNode $ f $ inj $ (Variable v `withContext` ctx) + return $ inj (Lambda v `withContext` ctx) :$ body where ctx = Proxy :: Proxy ctx diff --git a/Language/Syntactic/Sharing/SimpleCodeMotion.hs b/Language/Syntactic/Sharing/SimpleCodeMotion.hs --- a/Language/Syntactic/Sharing/SimpleCodeMotion.hs +++ b/Language/Syntactic/Sharing/SimpleCodeMotion.hs @@ -5,7 +5,9 @@ -- The code is based on an implementation by Gergely Dévai. module Language.Syntactic.Sharing.SimpleCodeMotion - ( codeMotion + ( BindDict (..) + , codeMotion + , defaultBindDict , reifySmart ) where @@ -23,40 +25,51 @@ --- | Substituting a sub-expression -substitute :: forall ctx dom a b - . ( Typeable a - , Typeable b - , Variable ctx :<: dom - , Lambda ctx :<: dom - , ExprEq dom - ) - => Proxy ctx - -> ASTF dom a -- ^ Sub-expression to be replaced +-- | Interface for binding constructs +data BindDict ctx dom = BindDict + { prjVariable :: forall a . dom a -> Maybe VarId + , prjLambda :: forall a . dom a -> Maybe VarId + , injVariable :: forall a . (Sat ctx a, Typeable a) => ASTF dom a -> VarId -> dom (Full a) + , injLambda :: forall a b . (Sat ctx a, Typeable a, Sat ctx b) => ASTF dom b -> VarId -> dom (b :-> Full (a -> b)) + , injLet :: forall a b . (Sat ctx a, Sat ctx b) => ASTF dom b -> dom (a :-> (a -> b) :-> Full b) + } + -- TODO `injLambda` has more constraints than the `Lambda` constructor. This + -- is demanded by the Feldspar implementation. One way to make things + -- more consistent would be to add an extra `ctx` parameter to `Lambda` + -- (like `Let`). + +-- | Substituting a sub-expression. Assumes no variable capturing in the +-- expressions involved. +substitute :: forall dom a b + . (Typeable a, Typeable b, AlphaEq dom dom dom [(VarId,VarId)]) + => ASTF dom a -- ^ Sub-expression to be replaced -> ASTF dom a -- ^ Replacing sub-expression -> ASTF dom b -- ^ Whole expression -> ASTF dom b -substitute ctx x y a = subst a +substitute x y a + | Just y' <- gcast y, alphaEq x a = y' + | otherwise = subst a where subst :: Typeable c => AST dom c -> AST dom c - subst a | Just y' <- gcast y, alphaEq ctx x a = y' - subst (f :$: a) = subst f :$: subst a + subst (f :$ a) = subst f :$ substitute x y a subst a = a -- | Count the number of occurrences of a sub-expression -count :: (Variable ctx :<: dom, Lambda ctx :<: dom, ExprEq dom) - => Proxy ctx - -> AST dom a -- ^ Expression to count - -> AST dom b -- ^ Expression to count in - -> VarId -count ctx a b - | alphaEq ctx a b = 1 -count ctx a (f :$: b) = count ctx a f + count ctx a b -count ctx a _ = 0 +count :: forall dom a b . AlphaEq dom dom dom [(VarId,VarId)] + => ASTF dom a -- ^ Expression to count + -> ASTF dom b -- ^ Expression to count in + -> Int +count a b + | alphaEq a b = 1 + | otherwise = cnt b + where + cnt :: AST dom c -> Int + cnt (f :$ b) = cnt f + count a b + cnt _ = 0 nonTerminal :: AST dom a -> Bool -nonTerminal (_ :$: _) = True -nonTerminal _ = False +nonTerminal (_ :$ _) = True +nonTerminal _ = False data SomeAST ctx dom where @@ -64,9 +77,10 @@ -- | Environment for the expression in the 'choose' function data Env ctx dom = Env - { context :: Proxy ctx - , inLambda :: Bool -- ^ Whether the current expression is inside a lambda - , counter :: SomeAST ctx dom -> VarId + { inLambda :: Bool -- ^ Whether the current expression is inside a lambda + , canShare :: forall a . dom a -> Bool + -- ^ Whether a given symbol can be shared + , counter :: SomeAST ctx dom -> Int -- ^ Counting the number of occurrences of an expression in the -- environment , dependencies :: Set VarId @@ -74,117 +88,140 @@ -- expression } -independent :: (Variable ctx :<: dom) => Env ctx dom -> AST dom a -> Bool -independent env (prjCtx (context env) -> Just (Variable v)) = +independent :: BindDict ctx dom -> Env ctx dom -> AST dom a -> Bool +independent bindDict env (Sym (prjVariable bindDict -> Just v)) = not (v `member` dependencies env) -independent env (f :$: a) = independent env f && independent env a -independent _ _ = True +independent bindDict env (f :$ a) = + independent bindDict env f && independent bindDict env a +independent _ _ _ = True -- | Checks whether a sub-expression in a given environment can be lifted out -liftable :: (Variable ctx :<: dom, Lambda ctx :<: dom, Sat ctx a, Typeable a) => - Env ctx dom -> ASTF dom a -> Bool -liftable env a = independent env a && heuristic +liftable :: (Sat ctx a, Typeable a) => + BindDict ctx dom -> Env ctx dom -> ASTF dom a -> Bool +liftable bindDict env a = independent bindDict env a && heuristic -- Lifting dependent expressions is semantically incorrect where - heuristic = nonTerminal a && (inLambda env || (counter env (SomeAST a) > 1)) + heuristic + = queryNodeSimple (const . canShare env) a + && nonTerminal a + && (inLambda env || (counter env (SomeAST a) > 1)) -- | Choose a sub-expression to share -choose :: forall ctx dom a - . ( Variable ctx :<: dom - , Lambda ctx :<: dom - , ExprEq dom +choose + :: ( AlphaEq dom dom dom [(VarId,VarId)] , MaybeWitnessSat ctx dom , Typeable a ) - => ASTF dom a -> Maybe (SomeAST ctx dom) -choose a = chooseEnv env a + => BindDict ctx dom + -> (forall a . dom a -> Bool) + -> ASTF dom a + -> Maybe (SomeAST ctx dom) +choose bindDict canShr a = chooseEnv bindDict env a where - ctx = Proxy :: Proxy ctx - - env :: Env ctx dom env = Env { inLambda = False - , counter = \(SomeAST b) -> count ctx b a + , canShare = canShr + , counter = \(SomeAST b) -> count b a , dependencies = empty - , context = ctx } -- | Choose a sub-expression to share in an 'Env' environment -chooseEnv - :: ( Variable ctx :<: dom - , Lambda ctx :<: dom - , MaybeWitnessSat ctx dom - , Typeable a - ) - => Env ctx dom -> ASTF dom a -> Maybe (SomeAST ctx dom) -chooseEnv env a - | Just SatWit <- maybeWitnessSat (context env) a - , liftable env a +chooseEnv :: forall ctx dom a . (MaybeWitnessSat ctx dom, Typeable a) => + BindDict ctx dom -> Env ctx dom -> ASTF dom a -> Maybe (SomeAST ctx dom) +chooseEnv bindDict env a + | Just SatWit <- maybeWitnessSat (Proxy :: Proxy ctx) a + , liftable bindDict env a = Just (SomeAST a) - | otherwise = chooseEnvSub env a + | otherwise = chooseEnvSub bindDict env a -- | Like 'chooseEnv', but does not consider the top expression for sharing -chooseEnvSub - :: (Variable ctx :<: dom, Lambda ctx :<: dom, MaybeWitnessSat ctx dom) - => Env ctx dom -> AST dom a -> Maybe (SomeAST ctx dom) -chooseEnvSub env ((prjCtx (context env) -> Just (Lambda v)) :$: a) = - chooseEnv env' a +chooseEnvSub :: MaybeWitnessSat ctx dom => + BindDict ctx dom -> Env ctx dom -> AST dom a -> Maybe (SomeAST ctx dom) +chooseEnvSub bindDict env (Sym (prjLambda bindDict -> Just v) :$ a) = + chooseEnv bindDict env' a where env' = env { inLambda = True , dependencies = insert v (dependencies env) } -chooseEnvSub env (f :$: a) = chooseEnvSub env f `mplus` chooseEnv env a -chooseEnvSub _ _ = Nothing +chooseEnvSub bindDict env (f :$ a) = + chooseEnvSub bindDict env f `mplus` chooseEnv bindDict env a +chooseEnvSub _ _ _ = Nothing + + -- | Perform common sub-expression elimination and variable hoisting codeMotion :: forall ctx dom a - . ( Variable ctx :<: dom - , Lambda ctx :<: dom - , Let ctx ctx :<: dom - , ExprEq dom + . ( AlphaEq dom dom dom [(VarId,VarId)] , MaybeWitnessSat ctx dom , Typeable a ) - => Proxy ctx -> ASTF dom a -> State VarId (ASTF dom a) -codeMotion ctx a + => BindDict ctx dom + -> (forall a . dom a -> Bool) + -> ASTF dom a + -> State VarId (ASTF dom a) +codeMotion bindDict canShr a | Just SatWit <- maybeWitnessSat ctx a - , Just b <- choose a + , Just b <- choose bindDict canShr a = share b - | otherwise = descend ctx a + | otherwise = descend a where + ctx = Proxy :: Proxy ctx + share :: Sat ctx a => SomeAST ctx dom -> State VarId (ASTF dom a) share (SomeAST b) = do - b' <- codeMotion ctx b + b' <- codeMotion bindDict canShr b v <- get; put (v+1) - let x = inject (Variable v `withContext` ctx) - body <- codeMotion ctx $ substitute ctx b x a + let x = Sym (injVariable bindDict b v) + body <- codeMotion bindDict canShr $ substitute b x a return - $ inject (letBind ctx) - :$: b' - :$: (inject (Lambda v `withContext` ctx) :$: body) + $ Sym (injLet bindDict body) + :$ b' + :$ (Sym (injLambda bindDict body v) :$ body) -descend - :: ( Variable ctx :<: dom - , Lambda ctx :<: dom - , Let ctx ctx :<: dom - , ExprEq dom - , MaybeWitnessSat ctx dom + descend :: AST dom b -> State VarId (AST dom b) + descend (f :$ a) = liftM2 (:$) (descend f) (codeMotion bindDict canShr a) + descend a = return a + + + +defaultBindDict :: forall ctx dom + . ( Variable ctx :<: dom + , Lambda ctx :<: dom + , Let ctx ctx :<: dom ) - => Proxy ctx -> AST dom a -> State VarId (AST dom a) -descend ctx (f :$: a) = liftM2 (:$:) (descend ctx f) (codeMotion ctx a) -descend _ a = return a + => BindDict ctx dom +defaultBindDict = BindDict + { prjVariable = \a -> do + Variable v <- prjCtx ctx a + return v + , prjLambda = \a -> do + Lambda v <- prjCtx ctx a + return v + + , injVariable = \_ v -> inj (Variable v `withContext` ctx) + , injLambda = \_ v -> inj (Lambda v `withContext` ctx) + , injLet = \_ -> inj (letBind ctx) + } + where + ctx = Proxy :: Proxy ctx + + + -- | Like 'reify' but with common sub-expression elimination and variable -- hoisting -reifySmart - :: ( Let ctx ctx :<: dom - , ExprEq dom +reifySmart :: forall ctx dom a + . ( Let ctx ctx :<: dom + , AlphaEq dom dom (Lambda ctx :+: Variable ctx :+: dom) [(VarId,VarId)] , MaybeWitnessSat ctx dom , Syntactic a (HODomain ctx dom) ) - => Proxy ctx + => (forall a . (Lambda ctx :+: Variable ctx :+: dom) a -> Bool) -> a -> ASTF (Lambda ctx :+: Variable ctx :+: dom) (Internal a) -reifySmart ctx = flip evalState 0 . (codeMotion ctx <=< reifyM) . desugar +reifySmart canShr = flip evalState 0 . + (codeMotion dict canShr <=< reifyM . desugar) + where + dict = defaultBindDict :: BindDict ctx (Lambda ctx :+: Variable ctx :+: dom) diff --git a/Language/Syntactic/Syntax.hs b/Language/Syntactic/Syntax.hs --- a/Language/Syntactic/Syntax.hs +++ b/Language/Syntactic/Syntax.hs @@ -23,12 +23,12 @@ -- following conversions: -- -- > conv12 :: Expr1 a -> Expr2 a --- > conv12 (Num1 n) = inject (Num2 n) --- > conv12 (Add1 a b) = inject Add2 :$: conv12 a :$: conv12 b +-- > conv12 (Num1 n) = inj (Num2 n) +-- > conv12 (Add1 a b) = inj Add2 :$ conv12 a :$ conv12 b -- > -- > conv21 :: Expr2 a -> Expr1 a --- > conv21 (project -> Just (Num2 n)) = Num1 n --- > conv21 ((project -> Just Add2) :$: a :$: b) = Add1 (conv21 a) (conv21 b) +-- > conv21 (prj -> Just (Num2 n)) = Num1 n +-- > conv21 ((prj -> Just Add2) :$ a :$ b) = Add1 (conv21 a) (conv21 b) -- -- A key property here is that the patterns in @conv21@ are actually complete. -- @@ -39,8 +39,8 @@ -- > countNodes = count -- > where -- > count :: AST domain a -> Int --- > count (Symbol _) = 1 --- > count (a :$: b) = count a + count b +-- > count (Sym _) = 1 +-- > count (a :$ b) = count a + count b -- -- Furthermore, although @Expr2@ was defined to use exactly the constructors -- 'Num2' and 'Add2', it is possible to leave the set of constructors open, @@ -59,21 +59,20 @@ ( -- * Syntax trees Full (..) , (:->) (..) - , HList (..) + , Args (..) , WrapFull (..) - , ConsType - , ConsEval - , EvalResult + , Signature + , Denotation + , DenResult , ConsWit (..) , WitnessCons (..) , fromEval , toEval - , listHList - , listHListM - , mapHList - , mapHListM - , appHList - , appEvalHList + , listArgs + , mapArgs + , mapArgsM + , appArgs + , appEvalArgs , ($:) , AST (..) , ASTF @@ -140,25 +139,25 @@ newtype a :-> b = Partial (a -> b) deriving (Typeable) --- | Heterogeneous list, indexed by a container type and a 'ConsType' -data family HList (c :: * -> *) a +-- | Heterogeneous list, indexed by a container type and a 'Signature' +data family Args (c :: * -> *) a -data instance HList c (Full a) = Nil -data instance HList c (a :-> b) = Typeable a => c (Full a) :*: HList c b +data instance Args c (Full a) = Nil +data instance Args c (a :-> b) = Typeable a => c (Full a) :* Args c b -- The 'Typeable' constraint is needed in order to be able to rebuild an 'AST' - -- from an 'HList' (since '(:$:)' has a `Typeable` constraint). + -- from an 'Args' (since '(:$)' has a `Typeable` constraint). -infixr :->, :*: +infixr :->, :* -- | Can be used to turn a type constructor indexed by @a@ to a type constructor --- indexed by @(`Full` a)@. This is useful together with 'HList', which assumes +-- indexed by @(`Full` a)@. This is useful together with 'Args', which assumes -- its constructor to be indexed by @(`Full` a)@. That is, use -- --- > HList (WrapFull c) ... +-- > Args (WrapFull c) ... -- -- instead of -- --- > HList c ... +-- > Args c ... -- -- if @c@ is not indexed by @(`Full` a)@. data WrapFull c a @@ -175,117 +174,112 @@ -- > a1 :-> a2 :-> ... :-> Full an -- -- The closed class also has the property: --- @ConsType' (a :-> b)@ iff. @ConsType' b@. -class ConsType' a +-- @Signature' (a :-> b)@ iff. @Signature' b@. +class Signature' a where - type ConsEval' a - type EvalResult' a + type Denotation' a + type DenResult' a - fromEval' :: ConsEval' a -> a - toEval' :: a -> ConsEval' a - listHList' :: (forall a . c (Full a) -> b) -> HList c a -> [b] - listHListM' :: Monad m => (forall a . c (Full a) -> m b) -> HList c a -> m [b] - mapHList' :: (forall a . c1 (Full a) -> c2 (Full a)) -> HList c1 a -> HList c2 a - mapHListM' :: Monad m => (forall a . c1 (Full a) -> m (c2 (Full a))) -> HList c1 a -> m (HList c2 a) - appHList' :: AST dom a -> HList (AST dom) a -> ASTF dom (EvalResult a) - appEvalHList' :: ConsEval a -> HList Identity a -> EvalResult a + fromEval' :: Denotation' a -> a + toEval' :: a -> Denotation' a + listArgs' :: (forall a . c (Full a) -> b) -> Args c a -> [b] + mapArgs' :: (forall a . c1 (Full a) -> c2 (Full a)) -> Args c1 a -> Args c2 a + mapArgsM' :: Monad m => (forall a . c1 (Full a) -> m (c2 (Full a))) -> Args c1 a -> m (Args c2 a) + appArgs' :: AST dom a -> Args (AST dom) a -> ASTF dom (DenResult a) + appEvalArgs' :: Denotation a -> Args Identity a -> DenResult a -instance ConsType' (Full a) +instance Signature' (Full a) where - type ConsEval' (Full a) = a - type EvalResult' (Full a) = a + type Denotation' (Full a) = a + type DenResult' (Full a) = a - fromEval' = Full - toEval' = result - listHList' f Nil = [] - listHListM' f Nil = return [] - mapHList' f Nil = Nil - mapHListM' f Nil = return Nil - appHList' a Nil = a - appEvalHList' a Nil = a + fromEval' = Full + toEval' = result + listArgs' f Nil = [] + mapArgs' f Nil = Nil + mapArgsM' f Nil = return Nil + appArgs' a Nil = a + appEvalArgs' a Nil = a -instance ConsType' b => ConsType' (a :-> b) +instance Signature' b => Signature' (a :-> b) where - type ConsEval' (a :-> b) = a -> ConsEval' b - type EvalResult' (a :-> b) = EvalResult' b + type Denotation' (a :-> b) = a -> Denotation' b + type DenResult' (a :-> b) = DenResult' b - fromEval' = Partial . (fromEval' .) - toEval' (Partial f) = toEval' . f - listHList' f (a :*: as) = f a : listHList' f as - listHListM' f (a :*: as) = sequence (f a : listHList' f as) - mapHList' f (a :*: as) = f a :*: mapHList' f as - mapHListM' f (a :*: as) = liftM2 (:*:) (f a) (mapHListM' f as) - appHList' c (a :*: as) = appHList' (c :$: a) as - appEvalHList' f (a :*: as) = appEvalHList' (f $ result $ runIdentity a) as + fromEval' = Partial . (fromEval' .) + toEval' (Partial f) = toEval' . f + listArgs' f (a :* as) = f a : listArgs' f as + mapArgs' f (a :* as) = f a :* mapArgs' f as + mapArgsM' f (a :* as) = liftM2 (:*) (f a) (mapArgsM' f as) + appArgs' c (a :* as) = appArgs' (c :$ a) as + appEvalArgs' f (a :* as) = appEvalArgs' (f $ result $ runIdentity a) as -- | Fully or partially applied constructor -- --- This is a public alias for the hidden class 'ConsType''. The only instances +-- This is a public alias for the hidden class 'Signature''. The only instances -- are: -- --- > instance ConsType' (Full a) --- > instance ConsType' b => ConsType' (a :-> b) -class ConsType' a => ConsType a -instance ConsType' a => ConsType a +-- > instance Signature' (Full a) +-- > instance Signature' b => Signature' (a :-> b) +class Signature' a => Signature a +instance Signature' a => Signature a --- | Maps a 'ConsType' to a simpler form where ':->' has been replaced by @->@, +-- | Maps a 'Signature' to a simpler form where ':->' has been replaced by @->@, -- and 'Full' has been removed. This is a public alias for the hidden type --- 'ConsEval''. -type ConsEval a = ConsEval' a +-- 'Denotation''. +type Denotation a = Denotation' a --- | Returns the result type ('Full' removed) of a 'ConsType'. This is a public --- alias for the hidden type 'EvalResult''. -type EvalResult a = EvalResult' a +-- | Returns the result type ('Full' removed) of a 'Signature'. This is a public +-- alias for the hidden type 'DenResult''. +type DenResult a = DenResult' a --- | A witness of @(`ConsType` a)@ +-- | A witness of @(`Signature` a)@ data ConsWit a where - ConsWit :: ConsType a => ConsWit a + ConsWit :: Signature a => ConsWit a -- | Expressions in syntactic are supposed to have the form --- @(`ConsType` a => expr a)@. This class lets us witness the 'ConsType' +-- @(`Signature` a => expr a)@. This class lets us witness the 'Signature' -- constraint of an expression without examining the expression. class WitnessCons expr where witnessCons :: expr a -> ConsWit a --- | Make a constructor evaluation from a 'ConsEval' representation -fromEval :: ConsType a => ConsEval a -> a +instance (WitnessCons sub1, WitnessCons sub2) => WitnessCons (sub1 :+: sub2) + where + witnessCons (InjL a) = witnessCons a + witnessCons (InjR a) = witnessCons a + +-- | Make a constructor evaluation from a 'Denotation' representation +fromEval :: Signature a => Denotation a -> a fromEval = fromEval' -toEval :: ConsType a => a -> ConsEval a +toEval :: Signature a => a -> Denotation a toEval = toEval' -- | Convert a heterogeneous list to a normal list -listHList :: ConsType a => - (forall a . c (Full a) -> b) -> HList c a -> [b] -listHList = listHList' - --- | Convert a heterogeneous list to a normal list -listHListM :: (Monad m, ConsType a) => - (forall a . c (Full a) -> m b) -> HList c a -> m [b] -listHListM = listHListM' +listArgs :: Signature a => (forall a . c (Full a) -> b) -> Args c a -> [b] +listArgs = listArgs' -- | Change the container of each element in a heterogeneous list -mapHList :: ConsType a => - (forall a . c1 (Full a) -> c2 (Full a)) -> HList c1 a -> HList c2 a -mapHList = mapHList' +mapArgs :: Signature a => + (forall a . c1 (Full a) -> c2 (Full a)) -> Args c1 a -> Args c2 a +mapArgs = mapArgs' -- | Change the container of each element in a heterogeneous list, monadic -- version -mapHListM :: (Monad m, ConsType a) => - (forall a . c1 (Full a) -> m (c2 (Full a))) -> HList c1 a -> m (HList c2 a) -mapHListM = mapHListM' +mapArgsM :: (Monad m, Signature a) => + (forall a . c1 (Full a) -> m (c2 (Full a))) -> Args c1 a -> m (Args c2 a) +mapArgsM = mapArgsM' -- | Apply the syntax tree to the listed arguments -appHList :: ConsType a => - AST dom a -> HList (AST dom) a -> ASTF dom (EvalResult a) -appHList = appHList' +appArgs :: Signature a => + AST dom a -> Args (AST dom) a -> ASTF dom (DenResult a) +appArgs = appArgs' -- | Apply the evaluation function to the listed arguments -appEvalHList :: ConsType a => - ConsEval a -> HList Identity a -> EvalResult a -appEvalHList = appEvalHList' +appEvalArgs :: Signature a => Denotation a -> Args Identity a -> DenResult a +appEvalArgs = appEvalArgs' -- | Semantic constructor application ($:) :: (a :-> b) -> a -> b @@ -300,14 +294,14 @@ -- @(`AST` dom (`Full` a))@ represents a fully applied constructor, i.e. a -- complete syntax tree. -- It is not possible to construct a total value of type @(`AST` dom a)@ that --- does not fulfill the constraint @(`ConsType` a)@. +-- does not fulfill the constraint @(`Signature` a)@. -- --- Note that the hidden class 'ConsType'' mentioned in the type of 'Symbol' is --- interchangeable with 'ConsType'. +-- Note that the hidden class 'Signature'' mentioned in the type of 'Sym' is +-- interchangeable with 'Signature'. data AST dom a where - Symbol :: ConsType' a => dom a -> AST dom a - (:$:) :: Typeable a => AST dom (a :-> b) -> ASTF dom a -> AST dom b + Sym :: Signature' a => dom a -> AST dom a + (:$) :: Typeable a => AST dom (a :-> b) -> ASTF dom a -> AST dom b -- | Fully applied abstract syntax tree type ASTF dom a = AST dom (Full a) @@ -315,10 +309,10 @@ -- | Co-product of two symbol domains data dom1 :+: dom2 :: * -> * where - InjectL :: dom1 a -> (dom1 :+: dom2) a - InjectR :: dom2 a -> (dom1 :+: dom2) a + InjL :: dom1 a -> (dom1 :+: dom2) a + InjR :: dom2 a -> (dom1 :+: dom2) a -infixl 1 :$: +infixl 1 :$ infixr :+: @@ -335,7 +329,7 @@ instance (Typeable a, ApplySym b f' dom) => ApplySym (a :-> b) (ASTF dom a -> f') dom where - appSym' sym a = appSym' (sym :$: a) + appSym' sym a = appSym' (sym :$ a) -- | Generic symbol application -- @@ -344,11 +338,11 @@ -- > appSym :: (expr :<: AST dom, Typeable a, Typeable b, ..., Typeable x) -- > => expr (a :-> b :-> ... :-> Full x) -- > -> (ASTF dom a -> ASTF dom b -> ... -> ASTF dom x) -appSym :: (ApplySym a f dom, ConsType a, sym :<: AST dom) => sym a -> f -appSym sym = appSym' (inject sym) +appSym :: (ApplySym a f dom, Signature a, sym :<: AST dom) => sym a -> f +appSym sym = appSym' (inj sym) -- | Generic symbol application with explicit context -appSymCtx :: (ApplySym a f dom, ConsType a, sym ctx :<: dom) => +appSymCtx :: (ApplySym a f dom, Signature a, sym ctx :<: dom) => Proxy ctx -> sym ctx a -> f appSymCtx _ = appSym @@ -361,47 +355,47 @@ class sub :<: sup where -- | Injection from @sub@ to @sup@ - inject :: ConsType a => sub a -> sup a + inj :: Signature a => sub a -> sup a -- | Partial projection from @sup@ to @sub@ - project :: sup a -> Maybe (sub a) + prj :: sup a -> Maybe (sub a) instance (sub :<: sup) => ((:<:) sub (AST sup)) -- GHC 6.12 requires prefix syntax here where - inject = Symbol . inject + inj = Sym . inj - project (Symbol a) = project a - project _ = Nothing + prj (Sym a) = prj a + prj _ = Nothing instance ((:<:) expr expr) where - inject = id - project = Just + inj = id + prj = Just instance ((:<:) expr1 (expr1 :+: expr2)) where - inject = InjectL + inj = InjL - project (InjectL a) = Just a - project _ = Nothing + prj (InjL a) = Just a + prj _ = Nothing instance (expr1 :<: expr3) => ((:<:) expr1 (expr2 :+: expr3)) where - inject = InjectR . inject + inj = InjR . inj - project (InjectR a) = project a - project _ = Nothing + prj (InjR a) = prj a + prj _ = Nothing --- | 'inject' with explicit context -injCtx :: (sub ctx :<: sup, ConsType a) => Proxy ctx -> sub ctx a -> sup a -injCtx _ = inject +-- | 'inj' with explicit context +injCtx :: (sub ctx :<: sup, Signature a) => Proxy ctx -> sub ctx a -> sup a +injCtx _ = inj --- | 'project' with explicit context +-- | 'prj' with explicit context prjCtx :: (sub ctx :<: sup) => Proxy ctx -> sup a -> Maybe (sub ctx a) -prjCtx _ = project +prjCtx _ = prj @@ -485,13 +479,13 @@ -- > ) => expr (Internal a :-> Internal b :-> ... :-> Full (Internal x)) -- > -> (a -> b -> ... -> x) sugarSym - :: (ConsType a, expr :<: AST dom, ApplySym a b dom, SyntacticN c b) - => expr a -> c + :: (Signature a, sym :<: AST dom, ApplySym a b dom, SyntacticN c b) + => sym a -> c sugarSym = sugarN . appSym -- | \"Sugared\" symbol application with explicit context sugarSymCtx - :: (ConsType a, sym ctx :<: dom, ApplySym a b dom, SyntacticN c b) + :: (Signature a, sym ctx :<: dom, ApplySym a b dom, SyntacticN c b) => Proxy ctx -> sym ctx a -> c sugarSymCtx _ = sugarSym @@ -514,19 +508,19 @@ -- following type, which shows that 'queryNode' can be directly used to -- transform syntax trees (see also 'transformNode'): -- --- > (forall a . ConsType a => dom a -> HList (AST dom) a -> ASTF dom' (EvalResult a)) +-- > (forall b . (Signature b, a ~ DenResult b) => dom b -> Args (AST dom) b -> ASTF dom' a) -- > -> ASTF dom a -- > -> ASTF dom' a -queryNode :: forall dom a c - . (forall a . ConsType a => - dom a -> HList (AST dom) a -> c (Full (EvalResult a))) +queryNode :: forall dom c a + . (forall b . (Signature b, a ~ DenResult b) => + dom b -> Args (AST dom) b -> c (Full a)) -> ASTF dom a -> c (Full a) queryNode f a = query a Nil where - query :: AST dom b -> HList (AST dom) b -> c (Full (EvalResult b)) - query (Symbol a) args = f a args - query (c :$: a) args = query c (a :*: args) + query :: (a ~ DenResult b) => AST dom b -> Args (AST dom) b -> c (Full a) + query (Sym a) args = f a args + query (c :$ a) args = query c (a :* args) -- | A simpler version of 'queryNode' -- @@ -535,12 +529,12 @@ -- -- > class Count subDomain -- > where --- > count' :: Count domain => subDomain a -> HList (AST domain) a -> Int +-- > count' :: Count domain => subDomain a -> Args (AST domain) a -> Int -- > -- > instance (Count sub1, Count sub2) => Count (sub1 :+: sub2) -- > where --- > count' (InjectL a) args = count' a args --- > count' (InjectR a) args = count' a args +-- > count' (InjL a) args = count' a args +-- > count' (InjR a) args = count' a args -- > -- > count :: Count dom => ASTF dom a -> Int -- > count = queryNodeSimple count' @@ -561,18 +555,19 @@ -- -- > instance Count Add -- > where --- > count' Add (a :*: b :*: Nil) = 1 + count a + count b -queryNodeSimple :: forall dom a b - . (forall a . ConsType a => dom a -> HList (AST dom) a -> b) +-- > count' Add (a :* b :* Nil) = 1 + count a + count b +queryNodeSimple :: forall dom a c + . (forall b . (Signature b, a ~ DenResult b) => + dom b -> Args (AST dom) b -> c) -> ASTF dom a - -> b + -> c queryNodeSimple f a = unConst $ queryNode (\c -> Const . f c) a -- | A version of 'queryNode' where the result is a transformed syntax tree, -- wrapped in a type constructor @c@ transformNode :: forall dom dom' c a - . ( forall a . ConsType a - => dom a -> HList (AST dom) a -> c (ASTF dom' (EvalResult a)) + . ( forall b . (Signature b, a ~ DenResult b) + => dom b -> Args (AST dom) b -> c (ASTF dom' a) ) -> ASTF dom a -> c (ASTF dom' a) @@ -606,6 +601,11 @@ where data Witness ctx a witness :: Witness ctx a + -- TODO Could probably use a one-parameter class instead, see + -- + -- http://www.haskell.org/pipermail/glasgow-haskell-users/2011-December/021292.html + -- + -- (but without the Super type family). Or even better, use ConstraintKinds. witnessByProxy :: Sat ctx a => Proxy ctx -> Proxy a -> Witness ctx a witnessByProxy _ _ = witness @@ -625,29 +625,29 @@ class WitnessSat expr where type SatContext expr - witnessSat :: expr a -> SatWit (SatContext expr) (EvalResult a) + witnessSat :: expr a -> SatWit (SatContext expr) (DenResult a) -- | Expressions that act as witnesses of their result type class MaybeWitnessSat ctx expr where - maybeWitnessSat :: Proxy ctx -> expr a -> Maybe (SatWit ctx (EvalResult a)) + maybeWitnessSat :: Proxy ctx -> expr a -> Maybe (SatWit ctx (DenResult a)) instance MaybeWitnessSat ctx dom => MaybeWitnessSat ctx (AST dom) where - maybeWitnessSat ctx (Symbol a) = maybeWitnessSat ctx a - maybeWitnessSat ctx (f :$: _) = maybeWitnessSat ctx f + maybeWitnessSat ctx (Sym a) = maybeWitnessSat ctx a + maybeWitnessSat ctx (f :$ _) = maybeWitnessSat ctx f instance (MaybeWitnessSat ctx sub1, MaybeWitnessSat ctx sub2) => MaybeWitnessSat ctx (sub1 :+: sub2) where - maybeWitnessSat ctx (InjectL a) = maybeWitnessSat ctx a - maybeWitnessSat ctx (InjectR a) = maybeWitnessSat ctx a + maybeWitnessSat ctx (InjL a) = maybeWitnessSat ctx a + maybeWitnessSat ctx (InjR a) = maybeWitnessSat ctx a -- | Convenient default implementation of 'maybeWitnessSat' maybeWitnessSatDefault :: WitnessSat expr => Proxy (SatContext expr) -> expr a - -> Maybe (SatWit (SatContext expr) (EvalResult a)) + -> Maybe (SatWit (SatContext expr) (DenResult a)) maybeWitnessSatDefault _ = Just . witnessSat -- | Type application for constraining the @ctx@ type of a parameterized symbol diff --git a/syntactic.cabal b/syntactic.cabal --- a/syntactic.cabal +++ b/syntactic.cabal @@ -1,5 +1,5 @@ Name: syntactic -Version: 0.7 +Version: 0.8 Synopsis: Generic abstract syntax, and utilities for embedded languages Description: This library provides: . @@ -45,19 +45,6 @@ Examples/NanoFeldspar/Extra.hs Examples/NanoFeldspar/Vector.hs Examples/NanoFeldspar/Test.hs - CEFP/MuFeldspar/Core.hs - CEFP/MuFeldspar/Frontend.hs - CEFP/MuFeldspar/Prelude.hs - CEFP/MuFeldspar/Vector.hs - CEFP/Imperative/Compiler.hs - CEFP/Imperative/Imperative.hs - CEFP/Examples/CodeApplication.hs - CEFP/Examples/Exercise10.hs - CEFP/Examples/Exercise12.hs - CEFP/Examples/Exercise14.hs - CEFP/Examples/ExProg.hs - CEFP/Examples/SolutionsSec2.hs - CEFP/Examples/Test.hs source-repository head type: darcs @@ -68,19 +55,21 @@ Language.Syntactic Language.Syntactic.Syntax Language.Syntactic.Interpretation.Equality - Language.Syntactic.Interpretation.Render Language.Syntactic.Interpretation.Evaluation - Language.Syntactic.Constructs.Annotate - Language.Syntactic.Constructs.Symbol - Language.Syntactic.Constructs.Literal - Language.Syntactic.Constructs.Condition - Language.Syntactic.Constructs.Tuple - Language.Syntactic.Constructs.TupleSyntacticPoly - Language.Syntactic.Constructs.TupleSyntacticSimple + Language.Syntactic.Interpretation.Render + Language.Syntactic.Interpretation.Semantics Language.Syntactic.Constructs.Binding Language.Syntactic.Constructs.Binding.HigherOrder Language.Syntactic.Constructs.Binding.Optimize + Language.Syntactic.Constructs.Condition + Language.Syntactic.Constructs.Construct + Language.Syntactic.Constructs.Decoration + Language.Syntactic.Constructs.Identity + Language.Syntactic.Constructs.Literal Language.Syntactic.Constructs.Monad + Language.Syntactic.Constructs.Tuple + Language.Syntactic.Constructs.TupleSyntacticPoly + Language.Syntactic.Constructs.TupleSyntacticSimple Language.Syntactic.Frontend.Monad Language.Syntactic.Sharing.SimpleCodeMotion Language.Syntactic.Sharing.Utils @@ -93,10 +82,11 @@ Build-depends: array, - base >= 4 && < 4.4, + base >= 4.0 && < 4.6, containers, data-hash, - mtl >= 1.1 && < 3, + mtl >= 2 && < 3, + QuickCheck >= 2.4, tagged, transformers >= 0.2, tuple >= 0.2