diff --git a/CEFP/Examples/CodeApplication.hs b/CEFP/Examples/CodeApplication.hs new file mode 100644 --- /dev/null +++ b/CEFP/Examples/CodeApplication.hs @@ -0,0 +1,175 @@ +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 new file mode 100644 --- /dev/null +++ b/CEFP/Examples/ExProg.hs @@ -0,0 +1,894 @@ +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 new file mode 100644 --- /dev/null +++ b/CEFP/Examples/Exercise10.hs @@ -0,0 +1,109 @@ +{-# 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 new file mode 100644 --- /dev/null +++ b/CEFP/Examples/Exercise12.hs @@ -0,0 +1,26 @@ +{-# 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 new file mode 100644 --- /dev/null +++ b/CEFP/Examples/Exercise14.hs @@ -0,0 +1,61 @@ +{-# 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 new file mode 100644 --- /dev/null +++ b/CEFP/Examples/SolutionsSec2.hs @@ -0,0 +1,370 @@ +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 new file mode 100644 --- /dev/null +++ b/CEFP/Examples/Test.hs @@ -0,0 +1,46 @@ +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 new file mode 100644 --- /dev/null +++ b/CEFP/Imperative/Compiler.hs @@ -0,0 +1,204 @@ +{-# 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 new file mode 100644 --- /dev/null +++ b/CEFP/Imperative/Imperative.hs @@ -0,0 +1,98 @@ +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 new file mode 100644 --- /dev/null +++ b/CEFP/MuFeldspar/Core.hs @@ -0,0 +1,460 @@ +{-# 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 new file mode 100644 --- /dev/null +++ b/CEFP/MuFeldspar/Frontend.hs @@ -0,0 +1,218 @@ +{-# 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 new file mode 100644 --- /dev/null +++ b/CEFP/MuFeldspar/Prelude.hs @@ -0,0 +1,11 @@ +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 new file mode 100644 --- /dev/null +++ b/CEFP/MuFeldspar/Vector.hs @@ -0,0 +1,96 @@ +{-# 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/NanoFeldspar/Core.hs b/Examples/NanoFeldspar/Core.hs --- a/Examples/NanoFeldspar/Core.hs +++ b/Examples/NanoFeldspar/Core.hs @@ -12,27 +12,26 @@ -- syntactic. -- -- A more realistic implementation would use custom contexts to restrict the --- types at which constructors operate. Currently, all general features (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' feature is quite unsafe (uses --- only a 'String' to distinguish between functions). +-- 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). module NanoFeldspar.Core where -import Prelude hiding (max, min) -import qualified Prelude import Data.Typeable import Language.Syntactic -import Language.Syntactic.Features.Symbol -import Language.Syntactic.Features.Literal -import Language.Syntactic.Features.Condition -import Language.Syntactic.Features.Tuple -import Language.Syntactic.Features.Binding -import Language.Syntactic.Features.Binding.HigherOrder +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 @@ -61,16 +60,26 @@ where witnessCons Parallel = ConsWit +instance WitnessSat Parallel + where + type SatContext Parallel = SimpleCtx + witnessSat Parallel = SatWit + +instance MaybeWitnessSat SimpleCtx Parallel + where + maybeWitnessSat = maybeWitnessSatDefault + instance IsSymbol Parallel where toSym Parallel = Sym "parallel" parallel where parallel 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 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 @@ -87,16 +96,26 @@ where witnessCons ForLoop = ConsWit +instance WitnessSat ForLoop + where + type SatContext ForLoop = SimpleCtx + witnessSat ForLoop = SatWit + +instance MaybeWitnessSat SimpleCtx ForLoop + where + maybeWitnessSat = maybeWitnessSatDefault + instance IsSymbol ForLoop where toSym ForLoop = Sym "forLoop" forLoop where forLoop 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 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 @@ -106,8 +125,8 @@ -- | The Feldspar domain type FeldDomain - = Literal SimpleCtx - :+: Sym SimpleCtx + = Sym SimpleCtx + :+: Literal SimpleCtx :+: Condition SimpleCtx :+: Tuple SimpleCtx :+: Select SimpleCtx @@ -115,10 +134,9 @@ :+: Parallel :+: ForLoop -data Data a = Type a => Data { unData :: HOAST SimpleCtx FeldDomain (Full a) } +type FeldDomainAll = HODomain SimpleCtx FeldDomain -type FeldDomainAll = - HOLambda SimpleCtx FeldDomain :+: Variable SimpleCtx :+: FeldDomain +newtype Data a = Data { unData :: ASTF FeldDomainAll a } -- | Declaring 'Data' as syntactic sugar instance Type a => Syntactic (Data a) FeldDomainAll @@ -128,19 +146,8 @@ sugar = Data -- | Specialization of the 'Syntactic' class for the Feldspar domain -class - ( Syntactic a FeldDomainAll - , Type (Internal a) - , SyntacticN a (ASTF FeldDomainAll (Internal a)) - ) => - Syntax a - -instance - ( Syntactic a FeldDomainAll - , Type (Internal a) - , SyntacticN a (ASTF FeldDomainAll (Internal a)) - ) => - Syntax a +class (Syntactic a FeldDomainAll, Type (Internal a)) => Syntax a +instance (Syntactic a FeldDomainAll, Type (Internal a)) => Syntax a @@ -149,16 +156,16 @@ -------------------------------------------------------------------------------- -- | Print the expression -printFeld :: Reifiable SimpleCtx a FeldDomain internal => a -> IO () -printFeld = printExpr . reifyCtx simpleCtx +printFeld :: Syntactic a FeldDomainAll => a -> IO () +printFeld = printExpr . reifySmart simpleCtx -- | Draw the syntax tree -drawFeld :: Reifiable SimpleCtx a FeldDomain internal => a -> IO () -drawFeld = drawAST . reifyCtx simpleCtx +drawFeld :: Syntactic a FeldDomainAll => a -> IO () +drawFeld = drawAST . reifySmart simpleCtx -- | Evaluation -eval :: Reifiable SimpleCtx a FeldDomain internal => a -> NAryEval internal -eval = evalLambda . reifyCtx simpleCtx +eval :: Syntactic a FeldDomainAll => a -> Internal a +eval = evalBind . reifySmart simpleCtx @@ -168,8 +175,14 @@ -- | Literal value :: Syntax a => Internal a -> a -value = sugar . litCtx simpleCtx +value = sugarSymCtx simpleCtx . 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 @@ -177,53 +190,43 @@ -- | Share a value using let binding share :: (Syntax a, Syntax b) => a -> (a -> b) -> b -share a f = sugar $ letBindCtx simpleCtx (desugar a) (desugarN f) +share = sugarSym (letBind simpleCtx) -- | Alpha equivalence -instance Eq (Data a) +instance Type a => Eq (Data a) where Data a == Data b = - alphaEq simpleCtx (reifyCtx simpleCtx a) (reifyCtx simpleCtx b) + alphaEq simpleCtx (reify simpleCtx a) (reify simpleCtx b) -instance Show (Data a) +instance Type a => Show (Data a) where - show (Data a) = render $ reifyCtx simpleCtx a + show (Data a) = render $ reify simpleCtx a instance (Type a, Num a) => Num (Data a) where fromInteger = value . fromInteger - abs = sugarN $ sym1 simpleCtx "abs" abs - signum = sugarN $ sym1 simpleCtx "signum" signum - (+) = sugarN $ sym2 simpleCtx "(+)" (+) - (-) = sugarN $ sym2 simpleCtx "(-)" (-) - (*) = sugarN $ sym2 simpleCtx "(*)" (*) + abs = sugarSymCtx simpleCtx $ Sym "abs" abs + signum = sugarSymCtx simpleCtx $ Sym "signum" signum + (+) = sugarSymCtx simpleCtx $ Sym "(+)" (+) + (-) = sugarSymCtx simpleCtx $ Sym "(-)" (-) + (*) = sugarSymCtx simpleCtx $ Sym "(*)" (*) (?) :: Syntax a => Data Bool -> (a,a) -> a -cond ? (t,e) = sugar $ - conditionCtx simpleCtx (desugar cond) (desugar t) (desugar e) +cond ? (t,e) = sugarSymCtx simpleCtx Condition cond t e -- | Parallel array parallel :: Type a => Data Length -> (Data Index -> Data a) -> Data [a] -parallel len ixf - = sugar - $ inject Parallel - :$: desugar len - :$: lambda (desugarN ixf) +parallel = sugarSym Parallel forLoop :: Syntax st => Data Length -> st -> (Data Index -> st -> st) -> st -forLoop len init body - = sugar - $ inject ForLoop - :$: desugar len - :$: desugar init - :$: lambdaN (desugarN body) +forLoop = sugarSym ForLoop arrLength :: Type a => Data [a] -> Data Length -arrLength = sugarN $ sym1 simpleCtx "arrLength" Prelude.length +arrLength = sugarSymCtx simpleCtx $ Sym "arrLength" Prelude.length -- | Array indexing getIx :: Type a => Data [a] -> Data Index -> Data a -getIx = sugarN $ sym2 simpleCtx "getIx" eval +getIx = sugarSymCtx simpleCtx $ Sym "getIx" eval where eval as i | i >= len || i < 0 = error "getIx: index out of bounds" @@ -231,9 +234,15 @@ where len = Prelude.length as +not :: Data Bool -> Data Bool +not = sugarSymCtx simpleCtx $ Sym "not" Prelude.not + +(==) :: Type a => Data a -> Data a -> Data Bool +(==) = sugarSymCtx simpleCtx $ Sym "(==)" (Prelude.==) + max :: Type a => Data a -> Data a -> Data a -max = sugarN $ sym2 simpleCtx "max" Prelude.max +max = sugarSymCtx simpleCtx $ Sym "max" Prelude.max min :: Type a => Data a -> Data a -> Data a -min = sugarN $ sym2 simpleCtx "min" Prelude.min +min = sugarSymCtx simpleCtx $ Sym "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 @@ -12,11 +12,11 @@ import Language.Syntactic -import Language.Syntactic.Features.Symbol -import Language.Syntactic.Features.Literal -import Language.Syntactic.Features.Binding -import Language.Syntactic.Features.Binding.HigherOrder -import Language.Syntactic.Features.Binding.PartialEval +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.Sharing.Graph import Language.Syntactic.Sharing.ReifyHO @@ -24,24 +24,21 @@ --- | A predicate deciding which constructs can be shared. Variables and literals --- are not shared. -mkSimpleWit :: (Sym SimpleCtx :<: dom, Parallel :<: dom, ForLoop :<: dom) => - ASTF dom a -> Maybe (Witness' SimpleCtx a) -mkSimpleWit ((project -> Just Parallel) :$: _ :$: _) = Just Witness' -mkSimpleWit ((project -> Just ForLoop) :$: _ :$: _ :$: _) = Just Witness' -mkSimpleWit expr = witnessSatSym simpleCtx expr - - - -------------------------------------------------------------------------------- -- * Graph reification -------------------------------------------------------------------------------- +-- | A predicate deciding which constructs can be shared. Literals and variables +-- are not shared. +canShare :: ASTF FeldDomainAll a -> Maybe (SatWit SimpleCtx a) +canShare (prjCtx simpleCtx -> Just (Literal _)) = Nothing +canShare (prjCtx simpleCtx -> Just (Variable _)) = Nothing +canShare a = maybeWitnessSat simpleCtx a + -- | Draw the syntax graph after common sub-expression elimination -drawFeldCSE :: Reifiable SimpleCtx a FeldDomain internal => a -> IO () +drawFeldCSE :: Syntactic a FeldDomainAll => a -> IO () drawFeldCSE a = do - (g,_) <- reifyGraph mkSimpleWit a + (g,_) <- reifyGraph canShare a drawASG $ reindexNodesFrom0 $ inlineSingle @@ -49,39 +46,38 @@ $ g -- | Draw the syntax graph after observing sharing -drawFeldObs :: Reifiable SimpleCtx a FeldDomain internal => a -> IO () +drawFeldObs :: Syntactic a FeldDomainAll => a -> IO () drawFeldObs a = do - (g,_) <- reifyGraph mkSimpleWit a + (g,_) <- reifyGraph canShare a drawASG $ reindexNodesFrom0 $ inlineSingle $ g + + -------------------------------------------------------------------------------- -- * Partial evaluation -------------------------------------------------------------------------------- -instance (ForLoop :<: dom, PartialEval dom ctx dom) => - PartialEval ForLoop ctx dom +instance (ForLoop :<: dom, Optimize dom ctx dom) => + Optimize ForLoop ctx dom where - partEvalFeat = partEvalFeatDefault + optimizeSym = optimizeSymDefault -instance (Parallel :<: dom, PartialEval dom ctx dom) => - PartialEval Parallel ctx dom +instance (Parallel :<: dom, Optimize dom ctx dom) => + Optimize Parallel ctx dom where - partEvalFeat = partEvalFeatDefault - - + optimizeSym = optimizeSymDefault constFold :: forall a . ASTF (Lambda SimpleCtx :+: Variable SimpleCtx :+: FeldDomain) a -> a -> ASTF (Lambda SimpleCtx :+: Variable SimpleCtx :+: FeldDomain) a -constFold expr a = case mkSimpleWit expr of - Just Witness' -> case witness :: Witness SimpleCtx a of - SimpleWit -> litCtx simpleCtx a +constFold expr a = case fmap fromSatWit (maybeWitnessSat simpleCtx expr) of + Just SimpleWit -> appSymCtx simpleCtx $ Literal a _ -> expr -drawFeldPart :: Reifiable SimpleCtx a FeldDomain internal => a -> IO () -drawFeldPart = drawAST . partialEval simpleCtx constFold . reifyCtx simpleCtx +drawFeldPart :: Syntactic a FeldDomainAll => a -> IO () +drawFeldPart = drawAST . optimize simpleCtx constFold . reify simpleCtx diff --git a/Examples/NanoFeldspar/Test.hs b/Examples/NanoFeldspar/Test.hs --- a/Examples/NanoFeldspar/Test.hs +++ b/Examples/NanoFeldspar/Test.hs @@ -1,6 +1,6 @@ -import Prelude hiding (length, map, max, min, reverse, sum, unzip, zip, zipWith) +import Prelude hiding (length, map, (==), max, min, reverse, sum, unzip, zip, zipWith) -import Language.Syntactic.Features.TupleSyntacticSimple +import Language.Syntactic.Constructs.TupleSyntacticSimple import NanoFeldspar.Core import NanoFeldspar.Extra @@ -16,7 +16,7 @@ test1_3 = eval prog1 0 10 prog2 :: Data Int -> Data Int -prog2 a = share (min a a) $ \b -> max b b +prog2 a = let b = min a a in max b b test2_1 = drawFeld prog2 test2_2 = printFeld prog2 @@ -63,7 +63,7 @@ as = map (*2) $ force (1...20) test7_1 = drawFeld prog7 - -- Draws a tree with a lot of duplication + -- Draws a tree with no duplication test7_2 = drawFeldCSE prog7 -- Draws a graph with no duplication @@ -74,6 +74,20 @@ -- 'parallel' introduced by 'force' is shared, because 'force' only appears -- once. --- Note that we're still missing a way to rebuild an expression with let --- bindings from the graph. This is ongoing work. + + +-------------------------------------------------------------------------------- +-- Demonstration of partial evaluation +-------------------------------------------------------------------------------- + +prog8 :: Data Int -> Data Int +prog8 a = (a==10) ? (max 5 (6+7), max 5 (6+7)) + +test8 = drawFeldPart prog8 + +prog9 a = expensiveCond ? (parallel a (+a), parallel a (+a)) + where + expensiveCond = getIx (parallel (a*a*a*a) (+a)) 10 == 23 + +test9 = drawFeldPart prog9 diff --git a/Examples/NanoFeldspar/Vector.hs b/Examples/NanoFeldspar/Vector.hs --- a/Examples/NanoFeldspar/Vector.hs +++ b/Examples/NanoFeldspar/Vector.hs @@ -19,7 +19,7 @@ -import Prelude hiding (length, map, max, min, reverse, sum, unzip, zip, zipWith) +import Prelude hiding (length, map, (==), max, min, reverse, sum, unzip, zip, zipWith) import Language.Syntactic diff --git a/Language/Syntactic.hs b/Language/Syntactic.hs --- a/Language/Syntactic.hs +++ b/Language/Syntactic.hs @@ -8,7 +8,7 @@ , module Language.Syntactic.Interpretation.Equality , module Language.Syntactic.Interpretation.Render , module Language.Syntactic.Interpretation.Evaluation - , module Language.Syntactic.Features.Annotate + , module Language.Syntactic.Constructs.Annotate ) where @@ -17,5 +17,5 @@ import Language.Syntactic.Interpretation.Equality import Language.Syntactic.Interpretation.Render import Language.Syntactic.Interpretation.Evaluation -import Language.Syntactic.Features.Annotate +import Language.Syntactic.Constructs.Annotate diff --git a/Language/Syntactic/Constructs/Annotate.hs b/Language/Syntactic/Constructs/Annotate.hs new file mode 100644 --- /dev/null +++ b/Language/Syntactic/Constructs/Annotate.hs @@ -0,0 +1,123 @@ +-- | 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 new file mode 100644 --- /dev/null +++ b/Language/Syntactic/Constructs/Binding.hs @@ -0,0 +1,296 @@ +{-# LANGUAGE OverlappingInstances #-} + +-- | General binding constructs + +module Language.Syntactic.Constructs.Binding where + + + +import Control.Monad.Identity +import Control.Monad.Reader +import Data.Dynamic +import Data.Ix +import Data.Tree + +import Data.Hash +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.Monad + + + +-------------------------------------------------------------------------------- +-- * Variables +-------------------------------------------------------------------------------- + +-- | Variable identifier +newtype VarId = VarId { varInteger :: Integer } + deriving (Eq, Ord, Num, Real, Integral, Enum, Ix) + +instance Show VarId + where + show (VarId i) = show i + +showVar :: VarId -> String +showVar v = "var" ++ show v + + + +-- | Variables +data Variable ctx a + where + Variable :: (Typeable a, Sat ctx a) => VarId -> Variable ctx (Full a) + -- 'Typeable' needed by the dynamic types in 'evalBind'. + +instance WitnessCons (Variable ctx) + where + witnessCons (Variable _) = ConsWit + +instance WitnessSat (Variable ctx) + where + type SatContext (Variable ctx) = ctx + witnessSat (Variable _) = SatWit + +instance MaybeWitnessSat ctx (Variable ctx) + where + maybeWitnessSat = maybeWitnessSatDefault + +instance MaybeWitnessSat ctx1 (Variable ctx2) + where + maybeWitnessSat _ _ = Nothing + +-- | 'exprEq' does strict identifier comparison; i.e. no alpha equivalence. +-- +-- 'exprHash' assigns the same hash to all variables. This is a valid +-- over-approximation that enables the following property: +-- +-- @`alphaEq` a b ==> `exprHash` a == `exprHash` b@ +instance ExprEq (Variable ctx) + where + exprEq (Variable v1) (Variable v2) = v1==v2 + exprHash (Variable _) = hashInt 0 + +instance Render (Variable ctx) + where + render (Variable v) = showVar v + +instance ToTree (Variable ctx) + where + toTreePart [] (Variable v) = Node ("var:" ++ show v) [] + + + +-------------------------------------------------------------------------------- +-- * Lambda binding +-------------------------------------------------------------------------------- + +-- | Lambda binding +data Lambda ctx a + where + Lambda :: (Typeable a, Sat ctx a) => + VarId -> Lambda ctx (b :-> Full (a -> b)) + -- 'Typeable' needed by the dynamic types in 'evalBind'. + +instance WitnessCons (Lambda ctx) + where + witnessCons (Lambda _) = ConsWit + +instance MaybeWitnessSat ctx1 (Lambda ctx2) + where + maybeWitnessSat _ _ = Nothing + +-- | 'exprEq' does strict identifier comparison; i.e. no alpha equivalence. +-- +-- 'exprHash' assigns the same hash to all 'Lambda' bindings. This is a valid +-- over-approximation that enables the following property: +-- +-- @`alphaEq` a b ==> `exprHash` a == `exprHash` b@ +instance ExprEq (Lambda ctx) + where + exprEq (Lambda v1) (Lambda v2) = v1==v2 + exprHash (Lambda _) = hashInt 0 + +instance Render (Lambda ctx) + where + renderPart [body] (Lambda v) = "(\\" ++ showVar v ++ " -> " ++ body ++ ")" + +instance ToTree (Lambda ctx) + where + toTreePart [body] (Lambda v) = Node ("Lambda " ++ show v) [body] + + + +-------------------------------------------------------------------------------- +-- * Let binding +-------------------------------------------------------------------------------- + +-- | Let binding +-- +-- A 'Let' expression is really just an application of a lambda binding (the +-- argument @(a -> b)@ is preferably constructed by 'Lambda'). +data Let ctxa ctxb a + where + Let :: (Sat ctxa a, Sat ctxb b) => Let ctxa ctxb (a :-> (a -> b) :-> Full b) + +instance WitnessCons (Let ctxa ctxb) + where + witnessCons Let = ConsWit + +instance WitnessSat (Let ctxa ctxb) + where + type SatContext (Let ctxa ctxb) = ctxb + witnessSat Let = SatWit + +instance MaybeWitnessSat ctxb (Let ctxa ctxb) + where + maybeWitnessSat = maybeWitnessSatDefault + +instance MaybeWitnessSat ctx (Let ctxa ctxb) + where + maybeWitnessSat _ _ = Nothing + +instance ExprEq (Let ctxa ctxb) + where + exprEq Let Let = True + + exprHash Let = hashInt 0 + +instance Render (Let ctxa ctxb) + where + renderPart [] Let = "Let" + renderPart [f,a] Let = "(" ++ unwords ["letBind",f,a] ++ ")" + +instance ToTree (Let ctxa ctxb) + where + toTreePart [a,body] Let = case splitAt 7 node of + ("Lambda ", var) -> Node ("Let " ++ var) [a,body'] + _ -> Node "Let" [a,body] + where + Node node [body'] = body + var = drop 7 node -- Drop the "Lambda " prefix + +instance Eval (Let ctxa ctxb) + where + evaluate Let = fromEval (flip ($)) + +-- | Let binding with explicit context +letBind :: (Sat ctx a, Sat ctx b) => + Proxy ctx -> Let ctx ctx (a :-> (a -> b) :-> Full b) +letBind _ = Let + +-- | Partial `Let` projection with explicit context +prjLet :: (Let ctxa ctxb :<: sup) => + Proxy ctxa -> Proxy ctxb -> sup a -> Maybe (Let ctxa ctxb a) +prjLet _ _ = project + + + +-------------------------------------------------------------------------------- +-- * 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) + => 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 + + + +-- | 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) [] + + + +class EvalBind sub + where + evalBindSym + :: (EvalBind dom, ConsType a) + => sub a + -> HList (AST dom) a + -> Reader [(VarId,Dynamic)] (EvalResult a) + +instance (EvalBind sub1, EvalBind sub2) => EvalBind (sub1 :+: sub2) + where + evalBindSym (InjectL a) = evalBindSym a + evalBindSym (InjectR a) = evalBindSym a + +-- | Evaluation of possibly open expressions +evalBindM :: EvalBind dom => ASTF dom a -> Reader [(VarId,Dynamic)] a +evalBindM = liftM result . queryNode (\a -> liftM Full . evalBindSym a) + +-- | Evaluation of closed expressions +evalBind :: EvalBind dom => ASTF dom a -> a +evalBind = flip runReader [] . evalBindM + +-- | Convenient default implementation of 'evalBindSym' +evalBindSymDefault :: (Eval sub, ConsType a, EvalBind dom) + => sub a + -> HList (AST dom) a + -> Reader [(VarId,Dynamic)] (EvalResult a) +evalBindSymDefault sym args = do + args' <- mapHListM (liftM (Identity . Full) . evalBindM) args + return $ appEvalHList (toEval $ evaluate sym) args' + +instance EvalBind (Sym 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 +instance EvalBind (Select ctx) where evalBindSym = evalBindSymDefault +instance EvalBind (Let ctxa ctxb) where evalBindSym = evalBindSymDefault +instance Monad m => EvalBind (MONAD m) where evalBindSym = evalBindSymDefault + +instance EvalBind dom => EvalBind (Ann info dom) + where + evalBindSym (Ann _ a) args = evalBindSym a args + +instance EvalBind (Lambda ctx) + where + evalBindSym (Lambda v) (body :*: Nil) = do + env <- ask + return + $ \a -> flip runReader ((v,toDyn a):env) + $ evalBindM body + +instance EvalBind (Variable ctx) + where + evalBindSym (Variable v) Nil = do + env <- ask + case lookup v env of + Nothing -> return $ error "evalBind: evaluating free variable" + Just a -> case fromDynamic a of + Just a -> return a + _ -> return $ error "evalBind: internal type error" + diff --git a/Language/Syntactic/Constructs/Binding/HigherOrder.hs b/Language/Syntactic/Constructs/Binding/HigherOrder.hs new file mode 100644 --- /dev/null +++ b/Language/Syntactic/Constructs/Binding/HigherOrder.hs @@ -0,0 +1,96 @@ +{-# LANGUAGE UndecidableInstances #-} + +-- | This module provides binding constructs using higher-order syntax and a +-- function for translating to first-order syntax. Expressions constructed using +-- the exported interface are guaranteed to have a well-behaved translation. + +module Language.Syntactic.Constructs.Binding.HigherOrder + ( Variable + , Let (..) + , HOLambda (..) + , HODomain + , lambda + , reifyM + , reifyTop + , reify + ) where + + + +import Control.Monad.State +import Data.Typeable + +import Data.Proxy + +import Language.Syntactic +import Language.Syntactic.Constructs.Binding + + + +-- | Higher-order lambda binding +data HOLambda ctx dom a + where + HOLambda :: (Typeable a, Typeable b, Sat ctx a) + => (ASTF (HODomain ctx dom) a -> ASTF (HODomain ctx dom) b) + -> HOLambda ctx dom (Full (a -> b)) + +type HODomain ctx dom = HOLambda ctx dom :+: Variable ctx :+: dom + +instance WitnessCons (HOLambda ctx dom) + where + witnessCons (HOLambda _) = ConsWit + +instance MaybeWitnessSat ctx1 (HOLambda ctx2 dom) + where + maybeWitnessSat _ _ = Nothing + + + +-- | Lambda binding +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 + +instance + ( Syntactic a (HODomain ctx dom) + , Syntactic b (HODomain ctx dom) + , Sat ctx (Internal a) + ) => + Syntactic (a -> b) (HODomain ctx dom) + where + type Internal (a -> b) = Internal a -> Internal b + desugar f = lambda (desugar . f . sugar) + sugar = error "sugar not implemented for (a -> b)" + -- TODO An implementation of sugar would require dom to have some kind of + -- application. Perhaps use Let for this? + + + +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 + v <- get; put (v+1) + body <- reifyM $ f $ inject $ (Variable v `withContext` ctx) + return $ inject (Lambda v `withContext` ctx) :$: body + where + ctx = Proxy :: Proxy ctx + +-- | Translating expressions with higher-order binding to corresponding +-- expressions using first-order binding +reifyTop :: Typeable a => + AST (HODomain ctx dom) a -> AST (Lambda ctx :+: Variable ctx :+: dom) a +reifyTop = flip evalState 0 . reifyM + -- It is assumed that there are no 'Variable' constructors (i.e. no free + -- variables) in the argument. This is guaranteed by the exported interface. + +-- | Reifying an n-ary syntactic function +reify :: Syntactic a (HODomain ctx dom) + => Proxy ctx + -> a + -> ASTF (Lambda ctx :+: Variable ctx :+: dom) (Internal a) +reify _ = reifyTop . desugar + diff --git a/Language/Syntactic/Constructs/Binding/Optimize.hs b/Language/Syntactic/Constructs/Binding/Optimize.hs new file mode 100644 --- /dev/null +++ b/Language/Syntactic/Constructs/Binding/Optimize.hs @@ -0,0 +1,134 @@ +{-# LANGUAGE UndecidableInstances #-} + +-- | Basic optimization of expressions +module Language.Syntactic.Constructs.Binding.Optimize where + + + +import Control.Monad.Writer +import Data.Set as Set + +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.Binding + + + +-- | Constant folder +-- +-- Given an expression and the statically known value of that expression, +-- returns a (possibly) new expression with the same meaning as the original. +-- Typically, the result will be a 'Literal', if the relevant type constraints +-- are satisfied. +type ConstFolder dom = forall a . ASTF dom a -> a -> ASTF dom a + +-- | Basic optimization of a sub-domain +class EvalBind dom => Optimize sub ctx dom + where + -- | Bottom-up optimization of a sub-domain. The optimization performed is + -- up to each instance, but the intention is to provide a sensible set of + -- \"always-appropriate\" optimizations. The default implementation + -- 'optimizeSymDefault' does only constant folding. This constant folding + -- uses the set of free variables to know when it's static evaluation is + -- possible. Thus it is possible to help constant folding of other + -- constructs by pruning away parts of the syntax tree that are known not to + -- be needed. For example, by replacing (using ordinary Haskell as an + -- example) + -- + -- > if True then a else b + -- + -- with @a@, we don't need to report the free variables in @b@. This, in + -- turn, can lead to more constant folding higher up in the syntax tree. + optimizeSym + :: Proxy ctx + -> ConstFolder dom + -> sub a + -> HList (AST dom) a + -> Writer (Set VarId) (ASTF dom (EvalResult 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 + -- 'optimizeSym', this constraint would not be allowed. On the other hand, it + -- is not possible to add the constraint @(sub :<: dom)@ to 'optimizeSym', + -- because the instance for '(:+:)' doesn't satisfy it. + +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 + +optimizeM :: Optimize dom ctx dom + => Proxy ctx + -> ConstFolder dom + -> ASTF dom a + -> Writer (Set VarId) (ASTF dom a) +optimizeM ctx constFold = transformNode (optimizeSym ctx constFold) + +-- | Optimize an expression +optimize :: Optimize dom ctx dom => + Proxy ctx -> ConstFolder dom -> ASTF dom a -> ASTF dom a +optimize ctx constFold = fst . runWriter . optimizeM ctx constFold + +-- | Convenient default implementation of 'optimizeSym' (uses 'evalBind' to +-- partially evaluate) +optimizeSymDefault + :: ( sub :<: dom + , WitnessCons sub + , Optimize dom ctx dom + ) + => Proxy ctx + -> ConstFolder dom + -> sub a + -> HList (AST dom) a + -> Writer (Set VarId) (ASTF dom (EvalResult a)) +optimizeSymDefault ctx constFold sym@(witnessCons -> ConsWit) args = do + (args',vars) <- listen $ mapHListM (optimizeM ctx constFold) args + let result = appHList (Symbol $ inject 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 + ( Condition ctx' :<: dom + , Lambda ctx :<: dom + , Variable ctx :<: dom + , ExprEq dom + , 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 + where + (c',cVars) = runWriter $ optimizeM ctx constFold c + t_or_e = if evalBind c' then t else e + +instance (Variable ctx :<: dom, Optimize dom ctx dom) => + Optimize (Variable ctx) ctx dom + where + optimizeSym _ _ var@(Variable v) Nil = do + tell (singleton v) + return (inject var) + +instance (Lambda ctx :<: dom, Optimize dom ctx dom) => + Optimize (Lambda ctx) ctx dom + where + optimizeSym ctx constFold lam@(Lambda v) (body :*: Nil) = do + body' <- censor (delete v) $ optimizeM ctx constFold body + return $ inject lam :$: body' + diff --git a/Language/Syntactic/Constructs/Condition.hs b/Language/Syntactic/Constructs/Condition.hs new file mode 100644 --- /dev/null +++ b/Language/Syntactic/Constructs/Condition.hs @@ -0,0 +1,47 @@ +{-# LANGUAGE OverlappingInstances #-} + +-- | Conditional expressions + +module Language.Syntactic.Constructs.Condition where + + + +import Data.Hash +import Data.Proxy +import Data.Typeable + +import Language.Syntactic +import Language.Syntactic.Constructs.Symbol + + + +data Condition ctx a + where + Condition :: Sat ctx a => Condition ctx (Bool :-> a :-> a :-> Full a) + +instance WitnessCons (Condition ctx) + where + witnessCons Condition = ConsWit + +instance WitnessSat (Condition ctx) + where + type SatContext (Condition ctx) = ctx + witnessSat Condition = SatWit + +instance MaybeWitnessSat ctx (Condition ctx) + where + maybeWitnessSat = maybeWitnessSatDefault + +instance MaybeWitnessSat ctx1 (Condition ctx2) + where + maybeWitnessSat _ _ = Nothing + +instance IsSymbol (Condition ctx) + where + toSym Condition = Sym "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 ToTree (Condition ctx) + diff --git a/Language/Syntactic/Constructs/Literal.hs b/Language/Syntactic/Constructs/Literal.hs new file mode 100644 --- /dev/null +++ b/Language/Syntactic/Constructs/Literal.hs @@ -0,0 +1,57 @@ +{-# LANGUAGE OverlappingInstances #-} + +-- | Literal expressions + +module Language.Syntactic.Constructs.Literal where + + + +import Data.Typeable + +import Data.Hash +import Data.Proxy + +import Language.Syntactic + + + +data Literal ctx a + where + Literal :: (Eq a, Show a, Typeable a, Sat ctx a) => + a -> Literal ctx (Full a) + +instance WitnessCons (Literal ctx) + where + witnessCons (Literal _) = ConsWit + +instance WitnessSat (Literal ctx) + where + type SatContext (Literal ctx) = ctx + witnessSat (Literal _) = SatWit + +instance MaybeWitnessSat ctx (Literal ctx) + where + maybeWitnessSat = maybeWitnessSatDefault + +instance MaybeWitnessSat ctx1 (Literal ctx2) + where + maybeWitnessSat _ _ = Nothing + +instance ExprEq (Literal ctx) + where + Literal a `exprEq` Literal b = case cast a of + Just a' -> a'==b + Nothing -> False + + exprHash (Literal a) = hash (show a) + +instance Render (Literal ctx) + where + render (Literal a) = show a + +instance ToTree (Literal ctx) + +instance Eval (Literal ctx) + where + evaluate (Literal a) = fromEval a + diff --git a/Language/Syntactic/Constructs/Monad.hs b/Language/Syntactic/Constructs/Monad.hs new file mode 100644 --- /dev/null +++ b/Language/Syntactic/Constructs/Monad.hs @@ -0,0 +1,49 @@ +-- | Monadic constructs + +module Language.Syntactic.Constructs.Monad where + + + +import Control.Monad + +import Language.Syntactic +import Language.Syntactic.Constructs.Symbol + +import Data.Proxy + + + +data MONAD m a + where + Return :: MONAD m (a :-> Full (m a)) + Bind :: MONAD m (m a :-> (a -> m b) :-> Full (m b)) + Then :: MONAD m (m a :-> m b :-> Full (m b)) + When :: MONAD m (Bool :-> m () :-> Full (m ())) + +instance WitnessCons (MONAD m) + where + witnessCons Return = ConsWit + witnessCons Bind = ConsWit + witnessCons Then = ConsWit + witnessCons When = ConsWit + +instance MaybeWitnessSat ctx (MONAD m) + where + maybeWitnessSat _ _ = Nothing + +instance Monad m => IsSymbol (MONAD m) + where + toSym Return = Sym "return" return + toSym Bind = Sym "bind" (>>=) + toSym Then = Sym "then" (>>) + toSym When = Sym "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 => ToTree (MONAD m) + +-- | Projection with explicit monad type +prjMonad :: (MONAD m :<: sup) => Proxy (m ()) -> sup a -> Maybe (MONAD m a) +prjMonad _ = project + diff --git a/Language/Syntactic/Constructs/Symbol.hs b/Language/Syntactic/Constructs/Symbol.hs new file mode 100644 --- /dev/null +++ b/Language/Syntactic/Constructs/Symbol.hs @@ -0,0 +1,93 @@ +{-# 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 new file mode 100644 --- /dev/null +++ b/Language/Syntactic/Constructs/Tuple.hs @@ -0,0 +1,422 @@ +{-# OPTIONS_GHC -fcontext-stack=30 #-} + +{-# LANGUAGE OverlappingInstances #-} + +-- | Construction and projection of tuples in the object language +-- +-- The function pairs @desugarTupX@/@sugarTupX@ could be used directly in +-- 'Syntactic' instances if it wasn't for the extra @(`Proxy` ctx)@ arguments. +-- For this reason, 'Syntactic' instances have to be written manually for each +-- context. The module "Language.Syntactic.Constructs.TupleSyntacticPoly" +-- provides instances for a 'Poly' context. The exact same code can be used to +-- make instances for other contexts -- just copy/paste and replace 'Poly' and +-- 'poly' with the desired context (and probably add an extra constraint in the +-- class contexts). + +module Language.Syntactic.Constructs.Tuple where + + + +import Data.Hash +import Data.Proxy +import Data.Tuple.Curry +import Data.Tuple.Select + +import Language.Syntactic +import Language.Syntactic.Constructs.Symbol + + + +-------------------------------------------------------------------------------- +-- * Construction +-------------------------------------------------------------------------------- + +-- | Expressions for constructing tuples +data Tuple ctx a + where + Tup2 :: Sat ctx (a,b) => Tuple ctx (a :-> b :-> Full (a,b)) + Tup3 :: Sat ctx (a,b,c) => Tuple ctx (a :-> b :-> c :-> Full (a,b,c)) + Tup4 :: Sat ctx (a,b,c,d) => Tuple ctx (a :-> b :-> c :-> d :-> Full (a,b,c,d)) + Tup5 :: Sat ctx (a,b,c,d,e) => Tuple ctx (a :-> b :-> c :-> d :-> e :-> Full (a,b,c,d,e)) + Tup6 :: Sat ctx (a,b,c,d,e,f) => Tuple ctx (a :-> b :-> c :-> d :-> e :-> f :-> Full (a,b,c,d,e,f)) + Tup7 :: Sat ctx (a,b,c,d,e,f,g) => Tuple ctx (a :-> b :-> c :-> d :-> e :-> f :-> g :-> Full (a,b,c,d,e,f,g)) + +instance WitnessCons (Tuple ctx) + where + witnessCons Tup2 = ConsWit + witnessCons Tup3 = ConsWit + witnessCons Tup4 = ConsWit + witnessCons Tup5 = ConsWit + witnessCons Tup6 = ConsWit + witnessCons Tup7 = ConsWit + +instance WitnessSat (Tuple ctx) + where + type SatContext (Tuple ctx) = ctx + witnessSat Tup2 = SatWit + witnessSat Tup3 = SatWit + witnessSat Tup4 = SatWit + witnessSat Tup5 = SatWit + witnessSat Tup6 = SatWit + witnessSat Tup7 = SatWit + +instance MaybeWitnessSat ctx (Tuple ctx) + where + maybeWitnessSat = maybeWitnessSatDefault + +instance MaybeWitnessSat ctx1 (Tuple ctx2) + where + maybeWitnessSat _ _ = Nothing + +instance IsSymbol (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" (,,,,,,) + +instance ExprEq (Tuple ctx) where exprEq = exprEqSym; exprHash = exprHashSym +instance Render (Tuple ctx) where renderPart = renderPartSym +instance Eval (Tuple ctx) where evaluate = evaluateSym +instance ToTree (Tuple ctx) + + + +desugarTup2 + :: ( Syntactic a dom + , Syntactic b dom + , Sat ctx (Internal a, Internal b) + , Tuple ctx :<: dom + ) + => Proxy ctx + -> (a,b) + -> ASTF dom (Internal a, Internal b) +desugarTup2 ctx = uncurryN $ sugarSymCtx ctx Tup2 + +desugarTup3 + :: ( Syntactic a dom + , Syntactic b dom + , Syntactic c dom + , Sat ctx (Internal a, Internal b, Internal c) + , Tuple ctx :<: dom + ) + => Proxy ctx + -> (a,b,c) + -> ASTF dom (Internal a, Internal b, Internal c) +desugarTup3 ctx = uncurryN $ sugarSymCtx ctx Tup3 + +desugarTup4 + :: ( Syntactic a dom + , Syntactic b dom + , Syntactic c dom + , Syntactic d dom + , Sat ctx (Internal a, Internal b, Internal c, Internal d) + , Tuple ctx :<: dom + ) + => Proxy ctx + -> (a,b,c,d) + -> ASTF dom (Internal a, Internal b, Internal c, Internal d) +desugarTup4 ctx = uncurryN $ sugarSymCtx ctx Tup4 + +desugarTup5 + :: ( Syntactic a dom + , Syntactic b dom + , Syntactic c dom + , Syntactic d dom + , Syntactic e dom + , Sat ctx (Internal a, Internal b, Internal c, Internal d, Internal e) + , Tuple ctx :<: dom + ) + => Proxy ctx + -> (a,b,c,d,e) + -> ASTF dom (Internal a, Internal b, Internal c, Internal d, Internal e) +desugarTup5 ctx = uncurryN $ sugarSymCtx ctx Tup5 + +desugarTup6 + :: ( Syntactic a dom + , Syntactic b dom + , Syntactic c dom + , Syntactic d dom + , Syntactic e dom + , Syntactic f dom + , Sat ctx (Internal a, Internal b, Internal c, Internal d, Internal e, Internal f) + , Tuple ctx :<: dom + ) + => Proxy ctx + -> (a,b,c,d,e,f) + -> ASTF dom (Internal a, Internal b, Internal c, Internal d, Internal e, Internal f) +desugarTup6 ctx = uncurryN $ sugarSymCtx ctx Tup6 + +desugarTup7 + :: ( Syntactic a dom + , Syntactic b dom + , Syntactic c dom + , Syntactic d dom + , Syntactic e dom + , Syntactic f dom + , Syntactic g dom + , Sat ctx (Internal a, Internal b, Internal c, Internal d, Internal e, Internal f, Internal g) + , Tuple ctx :<: dom + ) + => Proxy ctx + -> (a,b,c,d,e,f,g) + -> ASTF dom (Internal a, Internal b, Internal c, Internal d, Internal e, Internal f, Internal g) +desugarTup7 ctx = uncurryN $ sugarSymCtx ctx Tup7 + + + +-------------------------------------------------------------------------------- +-- * Projection +-------------------------------------------------------------------------------- + +-- | These families ('Sel1'' - 'Sel7'') are needed because of the problem +-- described in: +-- +-- +type family Sel1' a +type instance Sel1' (a,b) = a +type instance Sel1' (a,b,c) = a +type instance Sel1' (a,b,c,d) = a +type instance Sel1' (a,b,c,d,e) = a +type instance Sel1' (a,b,c,d,e,f) = a +type instance Sel1' (a,b,c,d,e,f,g) = a + +type family Sel2' a +type instance Sel2' (a,b) = b +type instance Sel2' (a,b,c) = b +type instance Sel2' (a,b,c,d) = b +type instance Sel2' (a,b,c,d,e) = b +type instance Sel2' (a,b,c,d,e,f) = b +type instance Sel2' (a,b,c,d,e,f,g) = b + +type family Sel3' a +type instance Sel3' (a,b,c) = c +type instance Sel3' (a,b,c,d) = c +type instance Sel3' (a,b,c,d,e) = c +type instance Sel3' (a,b,c,d,e,f) = c +type instance Sel3' (a,b,c,d,e,f,g) = c + +type family Sel4' a +type instance Sel4' (a,b,c,d) = d +type instance Sel4' (a,b,c,d,e) = d +type instance Sel4' (a,b,c,d,e,f) = d +type instance Sel4' (a,b,c,d,e,f,g) = d + +type family Sel5' a +type instance Sel5' (a,b,c,d,e) = e +type instance Sel5' (a,b,c,d,e,f) = e +type instance Sel5' (a,b,c,d,e,f,g) = e + +type family Sel6' a +type instance Sel6' (a,b,c,d,e,f) = f +type instance Sel6' (a,b,c,d,e,f,g) = f + +type family Sel7' a +type instance Sel7' (a,b,c,d,e,f,g) = g + +-- | Expressions for selecting elements of a tuple +data Select ctx a + where + Sel1 :: (Sel1 a b, Sel1' a ~ b, Sat ctx b) => Select ctx (a :-> Full b) + Sel2 :: (Sel2 a b, Sel2' a ~ b, Sat ctx b) => Select ctx (a :-> Full b) + Sel3 :: (Sel3 a b, Sel3' a ~ b, Sat ctx b) => Select ctx (a :-> Full b) + Sel4 :: (Sel4 a b, Sel4' a ~ b, Sat ctx b) => Select ctx (a :-> Full b) + Sel5 :: (Sel5 a b, Sel5' a ~ b, Sat ctx b) => Select ctx (a :-> Full b) + Sel6 :: (Sel6 a b, Sel6' a ~ b, Sat ctx b) => Select ctx (a :-> Full b) + Sel7 :: (Sel7 a b, Sel7' a ~ b, Sat ctx b) => Select ctx (a :-> Full b) + +instance WitnessCons (Select ctx) + where + witnessCons Sel1 = ConsWit + witnessCons Sel2 = ConsWit + witnessCons Sel3 = ConsWit + witnessCons Sel4 = ConsWit + witnessCons Sel5 = ConsWit + witnessCons Sel6 = ConsWit + witnessCons Sel7 = ConsWit + +instance WitnessSat (Select ctx) + where + type SatContext (Select ctx) = ctx + witnessSat Sel1 = SatWit + witnessSat Sel2 = SatWit + witnessSat Sel3 = SatWit + witnessSat Sel4 = SatWit + witnessSat Sel5 = SatWit + witnessSat Sel6 = SatWit + witnessSat Sel7 = SatWit + +instance MaybeWitnessSat ctx (Select ctx) + where + maybeWitnessSat = maybeWitnessSatDefault + +instance MaybeWitnessSat ctx1 (Select ctx2) + where + maybeWitnessSat _ _ = Nothing + +instance IsSymbol (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 + +instance ExprEq (Select ctx) where exprEq = exprEqSym; exprHash = exprHashSym +instance Render (Select ctx) where renderPart = renderPartSym +instance Eval (Select ctx) where evaluate = evaluateSym +instance ToTree (Select ctx) + +-- | Return the selected position, e.g. +-- +-- > selectPos (Sel3 poly :: Select Poly ((Int,Int,Int,Int) :-> Full Int)) = 3 +selectPos :: Select ctx a -> Int +selectPos Sel1 = 1 +selectPos Sel2 = 2 +selectPos Sel3 = 3 +selectPos Sel4 = 4 +selectPos Sel5 = 5 +selectPos Sel6 = 6 +selectPos Sel7 = 7 + + + +sugarTup2 + :: ( Syntactic a dom + , Syntactic b dom + , Sat ctx (Internal a) + , Sat ctx (Internal b) + , Select ctx :<: dom + ) + => Proxy ctx + -> ASTF dom (Internal a, Internal b) + -> (a,b) +sugarTup2 ctx a = + ( sugarSymCtx ctx Sel1 a + , sugarSymCtx ctx Sel2 a + ) + +sugarTup3 + :: ( Syntactic a dom + , Syntactic b dom + , Syntactic c dom + , Sat ctx (Internal a) + , Sat ctx (Internal b) + , Sat ctx (Internal c) + , Select ctx :<: dom + ) + => Proxy ctx + -> ASTF dom (Internal a, Internal b, Internal c) + -> (a,b,c) +sugarTup3 ctx a = + ( sugarSymCtx ctx Sel1 a + , sugarSymCtx ctx Sel2 a + , sugarSymCtx ctx Sel3 a + ) + +sugarTup4 + :: ( Syntactic a dom + , Syntactic b dom + , Syntactic c dom + , Syntactic d dom + , Sat ctx (Internal a) + , Sat ctx (Internal b) + , Sat ctx (Internal c) + , Sat ctx (Internal d) + , Select ctx :<: dom + ) + => Proxy ctx + -> ASTF dom (Internal a, Internal b, Internal c, Internal d) + -> (a,b,c,d) +sugarTup4 ctx a = + ( sugarSymCtx ctx Sel1 a + , sugarSymCtx ctx Sel2 a + , sugarSymCtx ctx Sel3 a + , sugarSymCtx ctx Sel4 a + ) + +sugarTup5 + :: ( Syntactic a dom + , Syntactic b dom + , Syntactic c dom + , Syntactic d dom + , Syntactic e dom + , Sat ctx (Internal a) + , Sat ctx (Internal b) + , Sat ctx (Internal c) + , Sat ctx (Internal d) + , Sat ctx (Internal e) + , Select ctx :<: dom + ) + => Proxy ctx + -> ASTF dom (Internal a, Internal b, Internal c, Internal d, Internal e) + -> (a,b,c,d,e) +sugarTup5 ctx a = + ( sugarSymCtx ctx Sel1 a + , sugarSymCtx ctx Sel2 a + , sugarSymCtx ctx Sel3 a + , sugarSymCtx ctx Sel4 a + , sugarSymCtx ctx Sel5 a + ) + +sugarTup6 + :: ( Syntactic a dom + , Syntactic b dom + , Syntactic c dom + , Syntactic d dom + , Syntactic e dom + , Syntactic f dom + , Sat ctx (Internal a) + , Sat ctx (Internal b) + , Sat ctx (Internal c) + , Sat ctx (Internal d) + , Sat ctx (Internal e) + , Sat ctx (Internal f) + , Select ctx :<: dom + ) + => Proxy ctx + -> ASTF dom (Internal a, Internal b, Internal c, Internal d, Internal e, Internal f) + -> (a,b,c,d,e,f) +sugarTup6 ctx a = + ( sugarSymCtx ctx Sel1 a + , sugarSymCtx ctx Sel2 a + , sugarSymCtx ctx Sel3 a + , sugarSymCtx ctx Sel4 a + , sugarSymCtx ctx Sel5 a + , sugarSymCtx ctx Sel6 a + ) + +sugarTup7 + :: ( Syntactic a dom + , Syntactic b dom + , Syntactic c dom + , Syntactic d dom + , Syntactic e dom + , Syntactic f dom + , Syntactic g dom + , Sat ctx (Internal a) + , Sat ctx (Internal b) + , Sat ctx (Internal c) + , Sat ctx (Internal d) + , Sat ctx (Internal e) + , Sat ctx (Internal f) + , Sat ctx (Internal g) + , Select ctx :<: dom + ) + => Proxy ctx + -> ASTF dom (Internal a, Internal b, Internal c, Internal d, Internal e, Internal f, Internal g) + -> (a,b,c,d,e,f,g) +sugarTup7 ctx a = + ( sugarSymCtx ctx Sel1 a + , sugarSymCtx ctx Sel2 a + , sugarSymCtx ctx Sel3 a + , sugarSymCtx ctx Sel4 a + , sugarSymCtx ctx Sel5 a + , sugarSymCtx ctx Sel6 a + , sugarSymCtx ctx Sel7 a + ) + diff --git a/Language/Syntactic/Constructs/TupleSyntacticPoly.hs b/Language/Syntactic/Constructs/TupleSyntacticPoly.hs new file mode 100644 --- /dev/null +++ b/Language/Syntactic/Constructs/TupleSyntacticPoly.hs @@ -0,0 +1,138 @@ +{-# LANGUAGE UndecidableInstances #-} + +-- | 'Syntactic' instances for tuples with 'Poly' context +module Language.Syntactic.Constructs.TupleSyntacticPoly where + + + +import Language.Syntactic.Syntax +import Language.Syntactic.Constructs.Tuple + + + +instance + ( Syntactic a dom + , Syntactic b dom + , Tuple Poly :<: dom + , Select Poly :<: dom + ) => + Syntactic (a,b) dom + where + type Internal (a,b) = + ( Internal a + , Internal b + ) + + desugar = desugarTup2 poly + sugar = sugarTup2 poly + +instance + ( Syntactic a dom + , Syntactic b dom + , Syntactic c dom + , Tuple Poly :<: dom + , Select Poly :<: dom + ) => + Syntactic (a,b,c) dom + where + type Internal (a,b,c) = + ( Internal a + , Internal b + , Internal c + ) + + desugar = desugarTup3 poly + sugar = sugarTup3 poly + +instance + ( Syntactic a dom + , Syntactic b dom + , Syntactic c dom + , Syntactic d dom + , Tuple Poly :<: dom + , Select Poly :<: dom + ) => + Syntactic (a,b,c,d) dom + where + type Internal (a,b,c,d) = + ( Internal a + , Internal b + , Internal c + , Internal d + ) + + desugar = desugarTup4 poly + sugar = sugarTup4 poly + +instance + ( Syntactic a dom + , Syntactic b dom + , Syntactic c dom + , Syntactic d dom + , Syntactic e dom + , Tuple Poly :<: dom + , Select Poly :<: dom + ) => + Syntactic (a,b,c,d,e) dom + where + type Internal (a,b,c,d,e) = + ( Internal a + , Internal b + , Internal c + , Internal d + , Internal e + ) + + desugar = desugarTup5 poly + sugar = sugarTup5 poly + +instance + ( Syntactic a dom + , Syntactic b dom + , Syntactic c dom + , Syntactic d dom + , Syntactic e dom + , Syntactic f dom + , Tuple Poly :<: dom + , Select Poly :<: dom + ) => + Syntactic (a,b,c,d,e,f) dom + where + type Internal (a,b,c,d,e,f) = + ( Internal a + , Internal b + , Internal c + , Internal d + , Internal e + , Internal f + ) + + desugar = desugarTup6 poly + sugar = sugarTup6 poly + +instance + ( Syntactic a dom + , Syntactic b dom + , Syntactic c dom + , Syntactic d dom + , Syntactic e dom + , Syntactic f dom + , Syntactic g dom + , Tuple Poly :<: dom + , Select Poly :<: dom + ) => + Syntactic (a,b,c,d,e,f,g) dom + where + type Internal (a,b,c,d,e,f,g) = + ( Internal a + , Internal b + , Internal c + , Internal d + , Internal e + , Internal f + , Internal g + ) + + desugar = desugarTup7 poly + sugar = sugarTup7 poly + diff --git a/Language/Syntactic/Constructs/TupleSyntacticSimple.hs b/Language/Syntactic/Constructs/TupleSyntacticSimple.hs new file mode 100644 --- /dev/null +++ b/Language/Syntactic/Constructs/TupleSyntacticSimple.hs @@ -0,0 +1,138 @@ +{-# LANGUAGE UndecidableInstances #-} + +-- | 'Syntactic' instances for tuples with 'SimpleCtx' context +module Language.Syntactic.Constructs.TupleSyntacticSimple where + + + +import Language.Syntactic.Syntax +import Language.Syntactic.Constructs.Tuple + + + +instance + ( Syntactic a dom, Eq (Internal a), Show (Internal a) + , Syntactic b dom, Eq (Internal b), Show (Internal b) + , Tuple SimpleCtx :<: dom + , Select SimpleCtx :<: dom + ) => + Syntactic (a,b) dom + where + type Internal (a,b) = + ( Internal a + , Internal b + ) + + desugar = desugarTup2 simpleCtx + sugar = sugarTup2 simpleCtx + +instance + ( Syntactic a dom, Eq (Internal a), Show (Internal a) + , Syntactic b dom, Eq (Internal b), Show (Internal b) + , Syntactic c dom, Eq (Internal c), Show (Internal c) + , Tuple SimpleCtx :<: dom + , Select SimpleCtx :<: dom + ) => + Syntactic (a,b,c) dom + where + type Internal (a,b,c) = + ( Internal a + , Internal b + , Internal c + ) + + desugar = desugarTup3 simpleCtx + sugar = sugarTup3 simpleCtx + +instance + ( Syntactic a dom, Eq (Internal a), Show (Internal a) + , Syntactic b dom, Eq (Internal b), Show (Internal b) + , Syntactic c dom, Eq (Internal c), Show (Internal c) + , Syntactic d dom, Eq (Internal d), Show (Internal d) + , Tuple SimpleCtx :<: dom + , Select SimpleCtx :<: dom + ) => + Syntactic (a,b,c,d) dom + where + type Internal (a,b,c,d) = + ( Internal a + , Internal b + , Internal c + , Internal d + ) + + desugar = desugarTup4 simpleCtx + sugar = sugarTup4 simpleCtx + +instance + ( Syntactic a dom, Eq (Internal a), Show (Internal a) + , Syntactic b dom, Eq (Internal b), Show (Internal b) + , Syntactic c dom, Eq (Internal c), Show (Internal c) + , Syntactic d dom, Eq (Internal d), Show (Internal d) + , Syntactic e dom, Eq (Internal e), Show (Internal e) + , Tuple SimpleCtx :<: dom + , Select SimpleCtx :<: dom + ) => + Syntactic (a,b,c,d,e) dom + where + type Internal (a,b,c,d,e) = + ( Internal a + , Internal b + , Internal c + , Internal d + , Internal e + ) + + desugar = desugarTup5 simpleCtx + sugar = sugarTup5 simpleCtx + +instance + ( Syntactic a dom, Eq (Internal a), Show (Internal a) + , Syntactic b dom, Eq (Internal b), Show (Internal b) + , Syntactic c dom, Eq (Internal c), Show (Internal c) + , Syntactic d dom, Eq (Internal d), Show (Internal d) + , Syntactic e dom, Eq (Internal e), Show (Internal e) + , Syntactic f dom, Eq (Internal f), Show (Internal f) + , Tuple SimpleCtx :<: dom + , Select SimpleCtx :<: dom + ) => + Syntactic (a,b,c,d,e,f) dom + where + type Internal (a,b,c,d,e,f) = + ( Internal a + , Internal b + , Internal c + , Internal d + , Internal e + , Internal f + ) + + desugar = desugarTup6 simpleCtx + sugar = sugarTup6 simpleCtx + +instance + ( Syntactic a dom, Eq (Internal a), Show (Internal a) + , Syntactic b dom, Eq (Internal b), Show (Internal b) + , Syntactic c dom, Eq (Internal c), Show (Internal c) + , Syntactic d dom, Eq (Internal d), Show (Internal d) + , Syntactic e dom, Eq (Internal e), Show (Internal e) + , Syntactic f dom, Eq (Internal f), Show (Internal f) + , Syntactic g dom, Eq (Internal g), Show (Internal g) + , Tuple SimpleCtx :<: dom + , Select SimpleCtx :<: dom + ) => + Syntactic (a,b,c,d,e,f,g) dom + where + type Internal (a,b,c,d,e,f,g) = + ( Internal a + , Internal b + , Internal c + , Internal d + , Internal e + , Internal f + , Internal g + ) + + desugar = desugarTup7 simpleCtx + sugar = sugarTup7 simpleCtx + diff --git a/Language/Syntactic/Features/Annotate.hs b/Language/Syntactic/Features/Annotate.hs deleted file mode 100644 --- a/Language/Syntactic/Features/Annotate.hs +++ /dev/null @@ -1,99 +0,0 @@ --- | Annotations for syntax trees - -module Language.Syntactic.Features.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 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 - --- | 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 - diff --git a/Language/Syntactic/Features/Binding.hs b/Language/Syntactic/Features/Binding.hs deleted file mode 100644 --- a/Language/Syntactic/Features/Binding.hs +++ /dev/null @@ -1,276 +0,0 @@ --- | General binding constructs - -module Language.Syntactic.Features.Binding where - - - -import Control.Monad.Reader -import Data.Dynamic -import Data.Ix -import Data.Tree - -import Data.Hash -import Data.Proxy - -import Language.Syntactic - - - --------------------------------------------------------------------------------- --- * Variables --------------------------------------------------------------------------------- - --- | Variable identifier -newtype VarId = VarId { varInteger :: Integer } - deriving (Eq, Ord, Num, Real, Integral, Enum, Ix) - -instance Show VarId - where - show (VarId i) = show i - -showVar :: VarId -> String -showVar v = "var" ++ show v - - - --- | Variables -data Variable ctx a - where - Variable :: (Typeable a, Sat ctx a) => VarId -> Variable ctx (Full a) - -- 'Typeable' needed by the dynamic types in 'evalLambda'. - -instance WitnessCons (Variable ctx) - where - witnessCons (Variable _) = ConsWit - -instance WitnessSat (Variable ctx) - where - type Context (Variable ctx) = ctx - witnessSat (Variable _) = Witness' - --- | 'exprEq' does strict identifier comparison; i.e. no alpha equivalence. --- --- 'exprHash' assigns the same hash to all variables. This is a valid --- over-approximation that enables the following property: --- --- @`alphaEq` a b ==> `exprHash` a == `exprHash` b@ -instance ExprEq (Variable ctx) - where - exprEq (Variable v1) (Variable v2) = v1==v2 - exprHash (Variable _) = hashInt 0 - -instance Render (Variable ctx) - where - render (Variable v) = showVar v - -instance ToTree (Variable ctx) - where - toTreePart [] (Variable v) = Node ("var:" ++ show v) [] - --- | Partial `Variable` projection with explicit context -prjVariable :: (Variable ctx :<: sup) => - Proxy ctx -> sup a -> Maybe (Variable ctx a) -prjVariable _ = project - - - --------------------------------------------------------------------------------- --- * Lambda binding --------------------------------------------------------------------------------- - --- | Lambda binding -data Lambda ctx a - where - Lambda :: (Typeable a, Sat ctx a) => - VarId -> Lambda ctx (b :-> Full (a -> b)) - -- 'Typeable' needed by the dynamic types in 'evalLambda'. - -instance WitnessCons (Lambda ctx) - where - witnessCons (Lambda _) = ConsWit - --- | 'exprEq' does strict identifier comparison; i.e. no alpha equivalence. --- --- 'exprHash' assigns the same hash to all 'Lambda' bindings. This is a valid --- over-approximation that enables the following property: --- --- @`alphaEq` a b ==> `exprHash` a == `exprHash` b@ -instance ExprEq (Lambda ctx) - where - exprEq (Lambda v1) (Lambda v2) = v1==v2 - exprHash (Lambda _) = hashInt 0 - -instance Render (Lambda ctx) - where - renderPart [body] (Lambda v) = "(\\" ++ showVar v ++ " -> " ++ body ++ ")" - -instance ToTree (Lambda ctx) - where - toTreePart [body] (Lambda v) = Node ("Lambda " ++ show v) [body] - --- | Partial `Lambda` projection with explicit context -prjLambda :: (Lambda ctx :<: sup) => Proxy ctx -> sup a -> Maybe (Lambda ctx a) -prjLambda _ = project - - - --- | The class of n-ary binding functions -class NAry ctx a dom | a -> dom - -- Note: using a functional dependency rather than an associated type, - -- because this makes it possible to make a class alias constraining dom. - -- GHC doesn't yet handle equality super classes. - where - type NAryEval a - - -- | N-ary binding by nested use of the supplied binder - bindN - :: Proxy ctx - -> ( forall b c . (Typeable b, Typeable c, Sat ctx b) - => (ASTF dom b -> ASTF dom c) - -> ASTF dom (b -> c) - ) - -> a -> ASTF dom (NAryEval a) - -instance Sat ctx a => NAry ctx (ASTF dom a) dom - where - type NAryEval (ASTF dom a) = a - bindN _ _ = id - -instance (Typeable a, Sat ctx a, NAry ctx b dom, Typeable (NAryEval b)) => - NAry ctx (ASTF dom a -> b) dom - where - type NAryEval (ASTF dom a -> b) = a -> NAryEval b - bindN ctx lambda = lambda . (bindN ctx lambda .) - - - --------------------------------------------------------------------------------- --- * Let binding --------------------------------------------------------------------------------- - --- | Let binding --- --- A 'Let' expression is really just an application of a lambda binding (the --- argument @(a -> b)@ is preferably constructed by 'Lambda'). -data Let ctxa ctxb a - where - Let :: (Sat ctxa a, Sat ctxb b) => Let ctxa ctxb (a :-> (a -> b) :-> Full b) - -instance WitnessCons (Let ctxa ctxb) - where - witnessCons Let = ConsWit - -instance WitnessSat (Let ctxa ctxb) - where - type Context (Let ctxa ctxb) = ctxb - witnessSat Let = Witness' - -instance ExprEq (Let ctxa ctxb) - where - exprEq Let Let = True - - exprHash Let = hashInt 0 - -instance Render (Let ctxa ctxb) - where - renderPart [] Let = "Let" - renderPart [f,a] Let = "(" ++ unwords ["letBind",f,a] ++ ")" - -instance ToTree (Let ctxa ctxb) - where - toTreePart [a,body] Let = Node ("Let " ++ var) [a,body'] - where - Node node [body'] = body - var = drop 7 node -- Drop the "Lambda " prefix - -instance Eval (Let ctxa ctxb) - where - evaluate Let = fromEval (flip ($)) - --- | Partial `Let` projection with explicit context -prjLet :: (Let ctxa ctxb :<: sup) => - Proxy ctxa -> Proxy ctxb -> sup a -> Maybe (Let ctxa ctxb a) -prjLet _ _ = project - - - --------------------------------------------------------------------------------- --- * 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) - => 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 - ((prjLambda ctx -> Just (Lambda v1)) :$: a1) - ((prjLambda ctx -> Just (Lambda v2)) :$: a2) = - local ((v1,v2):) $ alphaEqM ctx eq a1 a2 - -alphaEqM ctx eq - (prjVariable ctx -> Just (Variable v1)) - (prjVariable 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 - - - --- | 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) [] - - - --- | Evaluation of possibly open lambda expressions -evalLambdaM :: (Eval dom, MonadReader [(VarId,Dynamic)] m) => - ASTF (Lambda ctx :+: Variable ctx :+: dom) a -> m a -evalLambdaM = liftM result . eval - where - eval :: (Eval dom, MonadReader [(VarId,Dynamic)] m) => - AST (Lambda ctx :+: Variable ctx :+: dom) a -> m a - eval (Symbol (InjectR (InjectL (Variable v)))) = do - env <- ask - case lookup v env of - Nothing -> return $ error "eval: evaluating free variable" - Just a -> case fromDynamic a of - Just a -> return (Full a) - _ -> return $ error "eval: internal type error" - - eval (Symbol (InjectL (Lambda v)) :$: body) = do - env <- ask - return - $ Full - $ \a -> flip runReader ((v,toDyn a):env) - $ liftM result - $ eval body - - eval (f :$: a) = do - f' <- eval f - a' <- eval a - return (f' $: result a') - - eval (Symbol (InjectR (InjectR a))) = return (evaluate a) - - - --- | Evaluation of closed lambda expressions -evalLambda :: Eval dom => ASTF (Lambda ctx :+: Variable ctx :+: dom) a -> a -evalLambda = flip runReader [] . evalLambdaM - diff --git a/Language/Syntactic/Features/Binding/HigherOrder.hs b/Language/Syntactic/Features/Binding/HigherOrder.hs deleted file mode 100644 --- a/Language/Syntactic/Features/Binding/HigherOrder.hs +++ /dev/null @@ -1,134 +0,0 @@ -{-# LANGUAGE UndecidableInstances #-} - --- | This module provides binding constructs using higher-order syntax and a --- function for translating to first-order syntax. Expressions constructed using --- the exported interface are guaranteed to have a well-behaved translation. - -module Language.Syntactic.Features.Binding.HigherOrder - ( Variable - , evalLambda - , Let (..) - , HOLambda (..) - , HOAST - , HOASTF - , lambda - , lambdaN - , letBindCtx - , letBind - , reifyM - , reifyTop - , Reifiable - , reifyCtx - , reify - ) where - - - -import Control.Monad.State -import Data.Typeable - -import Data.Proxy - -import Language.Syntactic -import Language.Syntactic.Features.Binding - - - --- | Higher-order lambda binding -data HOLambda ctx dom a - where - HOLambda :: (Typeable a, Typeable b, Sat ctx a) - => (HOASTF ctx dom a -> HOASTF ctx dom b) - -> HOLambda ctx dom (Full (a -> b)) - -type HOAST ctx dom = AST (HOLambda ctx dom :+: Variable ctx :+: dom) -type HOASTF ctx dom a = HOAST ctx dom (Full a) - -instance WitnessCons (HOLambda ctx dom) - where - witnessCons (HOLambda _) = ConsWit - - - --- | Lambda binding -lambda :: (Typeable a, Typeable b, Sat ctx a) => - (HOASTF ctx dom a -> HOASTF ctx dom b) -> HOASTF ctx dom (a -> b) -lambda = inject . HOLambda - --- | N-ary lambda binding -lambdaN :: forall ctx dom a - . NAry ctx a (HOLambda ctx dom :+: Variable ctx :+: dom) - => a -> HOASTF ctx dom (NAryEval a) -lambdaN = bindN (Proxy :: Proxy ctx) lambda - --- | Let binding with explicit context -letBindCtx :: forall ctxa ctxb dom a b - . (Typeable a, Typeable b, Let ctxa ctxb :<: dom, Sat ctxa a, Sat ctxb b) - => Proxy ctxb - -> HOASTF ctxa dom a - -> (HOASTF ctxa dom a -> HOASTF ctxa dom b) - -> HOASTF ctxa dom b -letBindCtx _ a f = inject let' :$: a :$: lambda f - where - let' :: Let ctxa ctxb (a :-> (a -> b) :-> Full b) - let' = Let - --- | Let binding -letBind :: (Typeable a, Typeable b, Let Poly Poly :<: dom) - => HOASTF Poly dom a - -> (HOASTF Poly dom a -> HOASTF Poly dom b) - -> HOASTF Poly dom b -letBind = letBindCtx poly - - - -reifyM :: forall ctx dom a . Typeable a - => HOAST 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 - v <- get; put (v+1) - body <- reifyM $ f $ inject $ (Variable v `withContext` ctx) - return $ inject (Lambda v `withContext` ctx) :$: body - where - ctx = Proxy :: Proxy ctx - - --- | Translating expressions with higher-order binding to corresponding --- expressions using first-order binding -reifyTop :: Typeable a => - HOAST ctx dom a -> AST (Lambda ctx :+: Variable ctx :+: dom) a -reifyTop = flip evalState 0 . reifyM - -- It is assumed that there are no 'Variable' constructors (i.e. no free - -- variables) in the argument. This is guaranteed by the exported interface. - - - --- | Convenient class alias for n-ary syntactic functions -class - ( SyntacticN a internal - , NAry ctx internal (HOLambda ctx dom :+: Variable ctx :+: dom) - , Typeable (NAryEval internal) - ) => - Reifiable ctx a dom internal | a -> dom internal - -instance - ( SyntacticN a internal - , NAry ctx internal (HOLambda ctx dom :+: Variable ctx :+: dom) - , Typeable (NAryEval internal) - ) => - Reifiable ctx a dom internal - --- | Reifying an n-ary syntactic function with explicit context -reifyCtx :: Reifiable ctx a dom internal - => Proxy ctx - -> a - -> ASTF (Lambda ctx :+: Variable ctx :+: dom) (NAryEval internal) -reifyCtx _ = reifyTop . lambdaN . desugarN - --- | Reifying an n-ary syntactic function -reify :: Reifiable Poly a dom internal => - a -> ASTF (Lambda Poly :+: Variable Poly :+: dom) (NAryEval internal) -reify = reifyCtx poly - diff --git a/Language/Syntactic/Features/Binding/PartialEval.hs b/Language/Syntactic/Features/Binding/PartialEval.hs deleted file mode 100644 --- a/Language/Syntactic/Features/Binding/PartialEval.hs +++ /dev/null @@ -1,144 +0,0 @@ -{-# LANGUAGE UndecidableInstances #-} - --- | Partial evaluation - -module Language.Syntactic.Features.Binding.PartialEval where - - - -import Control.Monad.Writer -import Data.Set as Set - -import Data.Proxy - -import Language.Syntactic -import Language.Syntactic.Features.Symbol -import Language.Syntactic.Features.Literal -import Language.Syntactic.Features.Condition -import Language.Syntactic.Features.Tuple -import Language.Syntactic.Features.Binding - - - --- | Constant folder --- --- Given an expression and the statically known value of that expression, --- returns a (possibly) new expression with the same meaning as the original. --- Typically, the result will be a 'Literal', if the relevant type constraints --- are satisfied. -type ConstFolder ctx dom = forall a - . ASTF (Lambda ctx :+: Variable ctx :+: dom) a - -> a - -> ASTF (Lambda ctx :+: Variable ctx :+: dom) a - --- | Partial evaluation -class Eval dom => PartialEval feature ctx dom - where - -- | Partial evaluation of a feature. The @(`Set` `VarId`)@ returned is the - -- set of free variables of the expression. However, free variables are - -- counted in a \"lazy\" sense: free variables from sub-expressions that are - -- never evaluated may not be counted. (The instance for 'Conditional' will - -- throw away the free variables of the pruned branch when the condition is - -- statically known. This is one reason why partial evaluation and free - -- variable calculation have to be done simultaneously.) - partEvalFeat - :: Proxy ctx - -> ConstFolder ctx dom - -> feature a - -> HList (AST (Lambda ctx :+: Variable ctx :+: dom)) a - -> Writer - (Set VarId) - (ASTF (Lambda ctx :+: Variable ctx :+: dom) (EvalResult a)) - -instance (PartialEval sub1 ctx dom, PartialEval sub2 ctx dom) => - PartialEval (sub1 :+: sub2) ctx dom - where - partEvalFeat ctx constFold (InjectL a) = partEvalFeat ctx constFold a - partEvalFeat ctx constFold (InjectR a) = partEvalFeat ctx constFold a - -partialEvalM :: PartialEval dom ctx dom - => Proxy ctx - -> ConstFolder ctx dom - -> ASTF (Lambda ctx :+: Variable ctx :+: dom) a - -> Writer (Set VarId) (ASTF (Lambda ctx :+: Variable ctx :+: dom) a) -partialEvalM ctx constFold = transformNodeC (partEvalFeat ctx constFold) - --- | Partially evaluate an expression -partialEval :: PartialEval dom ctx dom - => Proxy ctx - -> ConstFolder ctx dom - -> ASTF (Lambda ctx :+: Variable ctx :+: dom) a - -> ASTF (Lambda ctx :+: Variable ctx :+: dom) a -partialEval ctx constFold = fst . runWriter . partialEvalM ctx constFold - - - --- | Convenient default implementation of 'partEvalFeat' (uses 'evalLambda' to --- evaluate) -partEvalFeatDefault - :: ( feature :<: dom - , WitnessCons feature - , PartialEval dom ctx dom - ) - => Proxy ctx - -> ConstFolder ctx dom - -> feature a - -> HList (AST (Lambda ctx :+: Variable ctx :+: dom)) a - -> Writer - (Set VarId) - (ASTF (Lambda ctx :+: Variable ctx :+: dom) (EvalResult a)) -partEvalFeatDefault ctx constFold feat@(witnessCons -> ConsWit) args = do - (args',vars) <- listen $ mapHListM (partialEvalM ctx constFold) args - let result = appHList (Symbol $ InjectR $ InjectR $ inject feat) args' - value = evalLambda result - if Set.null vars - then return $ constFold result value - else return result - -instance (Sym ctx' :<: dom, PartialEval dom ctx dom) => - PartialEval (Sym ctx') ctx dom - where - partEvalFeat = partEvalFeatDefault - -instance (Literal ctx' :<: dom, PartialEval dom ctx dom) => - PartialEval (Literal ctx') ctx dom - where - partEvalFeat = partEvalFeatDefault - -instance (Condition ctx' :<: dom, PartialEval dom ctx dom) => - PartialEval (Condition ctx') ctx dom - where - partEvalFeat ctx constFold cond@Condition args@(c :*: t :*: e :*: Nil) - | Set.null cVars = partialEvalM ctx constFold t_or_e - | otherwise = partEvalFeatDefault ctx constFold cond args - where - (c',cVars) = runWriter $ partialEvalM ctx constFold c - t_or_e = if evalLambda c' then t else e - -instance (Tuple ctx' :<: dom, PartialEval dom ctx dom) => - PartialEval (Tuple ctx') ctx dom - where - partEvalFeat = partEvalFeatDefault - -instance (Select ctx' :<: dom, PartialEval dom ctx dom) => - PartialEval (Select ctx') ctx dom - where - partEvalFeat = partEvalFeatDefault - -instance PartialEval dom ctx dom => PartialEval (Variable ctx) ctx dom - where - partEvalFeat _ _ var@(Variable v) Nil = do - tell (singleton v) - return (inject var) - -instance PartialEval dom ctx dom => PartialEval (Lambda ctx) ctx dom - where - partEvalFeat ctx constFold lam@(Lambda v) (body :*: Nil) = do - body' <- censor (delete v) $ partialEvalM ctx constFold body - return $ inject lam :$: body' - -instance (Let ctxa ctxb :<: dom, PartialEval dom ctx dom) => - PartialEval (Let ctxa ctxb) ctx dom - where - partEvalFeat = partEvalFeatDefault - diff --git a/Language/Syntactic/Features/Condition.hs b/Language/Syntactic/Features/Condition.hs deleted file mode 100644 --- a/Language/Syntactic/Features/Condition.hs +++ /dev/null @@ -1,57 +0,0 @@ --- | Conditional expressions - -module Language.Syntactic.Features.Condition where - - - -import Data.Hash -import Data.Proxy - -import Language.Syntactic -import Language.Syntactic.Features.Symbol - - - -data Condition ctx a - where - Condition :: Sat ctx a => Condition ctx (Bool :-> a :-> a :-> Full a) - -instance WitnessCons (Condition ctx) - where - witnessCons Condition = ConsWit - -instance WitnessSat (Condition ctx) - where - type Context (Condition ctx) = ctx - witnessSat Condition = Witness' - -instance IsSymbol (Condition ctx) - where - toSym Condition = Sym "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 ToTree (Condition ctx) - - - --- | Conditional expression with explicit context -conditionCtx - :: (Sat ctx (Internal a), Syntactic a dom, Condition ctx :<: dom) - => Proxy ctx -> ASTF dom Bool -> a -> a -> a -conditionCtx ctx cond tHEN eLSE = sugar $ inject (Condition `withContext` ctx) - :$: cond - :$: desugar tHEN - :$: desugar eLSE - --- | Conditional expression -condition :: (Condition Poly :<: dom, Syntactic a dom) => - ASTF dom Bool -> a -> a -> a -condition = conditionCtx poly - --- | Partial `Condition` projection with explicit context -prjCondition :: (Condition ctx :<: sup) => - Proxy ctx -> sup a -> Maybe (Condition ctx a) -prjCondition _ = project - diff --git a/Language/Syntactic/Features/Literal.hs b/Language/Syntactic/Features/Literal.hs deleted file mode 100644 --- a/Language/Syntactic/Features/Literal.hs +++ /dev/null @@ -1,63 +0,0 @@ --- | Literal expressions - -module Language.Syntactic.Features.Literal where - - - -import Data.Typeable - -import Data.Hash -import Data.Proxy - -import Language.Syntactic - - - -data Literal ctx a - where - Literal :: (Eq a, Show a, Typeable a, Sat ctx a) => - a -> Literal ctx (Full a) - -instance WitnessCons (Literal ctx) - where - witnessCons (Literal _) = ConsWit - -instance WitnessSat (Literal ctx) - where - type Context (Literal ctx) = ctx - witnessSat (Literal _) = Witness' - -instance ExprEq (Literal ctx) - where - Literal a `exprEq` Literal b = case cast a of - Just a' -> a'==b - Nothing -> False - - exprHash (Literal a) = hash (show a) - -instance Render (Literal ctx) - where - render (Literal a) = show a - -instance ToTree (Literal ctx) - -instance Eval (Literal ctx) - where - evaluate (Literal a) = fromEval a - - - --- | Literal with explicit context -litCtx :: (Eq a, Show a, Typeable a, Sat ctx a, Literal ctx :<: dom) => - Proxy ctx -> a -> ASTF dom a -litCtx ctx = inject . (`withContext` ctx) . Literal - --- | Literal -lit :: (Eq a, Show a, Typeable a, Literal Poly :<: dom) => a -> ASTF dom a -lit = litCtx poly - --- | Partial literal projection with explicit context -prjLiteral :: (Literal ctx :<: sup) => - Proxy ctx -> sup a -> Maybe (Literal ctx a) -prjLiteral _ = project - diff --git a/Language/Syntactic/Features/Symbol.hs b/Language/Syntactic/Features/Symbol.hs deleted file mode 100644 --- a/Language/Syntactic/Features/Symbol.hs +++ /dev/null @@ -1,179 +0,0 @@ --- | Simple 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.Features.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 Context (Sym ctx) = ctx - witnessSat (Sym _ _) = Witness' - -witnessSatSym :: forall ctx dom a . (Sym ctx :<: dom) - => Proxy ctx - -> ASTF dom a - -> Maybe (Witness' ctx a) -witnessSatSym ctx = witSym - where - witSym :: (EvalResult b ~ a) => AST dom b -> Maybe (Witness' ctx a) - witSym (prjSym ctx -> Just (Sym _ _)) = Just Witness' - witSym (f :$: _) = witSym f - witSym _ = 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 - - - --- | A zero-argument symbol -sym0 - :: ( Sat ctx a - , Sym ctx :<: dom - ) - => Proxy ctx - -> String - -> a - -> ASTF dom a -sym0 ctx name a = inject (Sym name a `withContext` ctx) - --- | A one-argument symbol -sym1 - :: ( Typeable a - , Sat ctx b - , Sym ctx :<: dom - ) - => Proxy ctx - -> String - -> (a -> b) - -> ASTF dom a - -> ASTF dom b -sym1 ctx name f a = inject (Sym name f `withContext` ctx) :$: a - --- | A two-argument symbol -sym2 - :: ( Typeable a - , Typeable b - , Sat ctx c - , Sym ctx :<: dom - ) - => Proxy ctx - -> String - -> (a -> b -> c) - -> ASTF dom a - -> ASTF dom b - -> ASTF dom c -sym2 ctx name f a b = inject (Sym name f `withContext` ctx) :$: a :$: b - --- | A three-argument symbol -sym3 - :: ( Typeable a - , Typeable b - , Typeable c - , Sat ctx d - , Sym ctx :<: dom - ) - => Proxy ctx - -> String - -> (a -> b -> c -> d) - -> ASTF dom a - -> ASTF dom b - -> ASTF dom c - -> ASTF dom d -sym3 ctx name f a b c = inject (Sym name f `withContext` ctx) :$: a :$: b :$: c - --- | A four-argument symbol -sym4 - :: ( Typeable a - , Typeable b - , Typeable c - , Typeable d - , Sat ctx e - , Sym ctx :<: dom - ) - => Proxy ctx - -> String - -> (a -> b -> c -> d -> e) - -> ASTF dom a - -> ASTF dom b - -> ASTF dom c - -> ASTF dom d - -> ASTF dom e -sym4 ctx name f a b c d = - inject (Sym name f `withContext` ctx) :$: a :$: b :$: c :$: d - - - --- | Partial symbol projection with explicit context -prjSym :: (Sym ctx :<: sup) => - Proxy ctx -> sup a -> Maybe (Sym ctx a) -prjSym _ = project - - - --- | 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/Features/Tuple.hs b/Language/Syntactic/Features/Tuple.hs deleted file mode 100644 --- a/Language/Syntactic/Features/Tuple.hs +++ /dev/null @@ -1,391 +0,0 @@ --- | Construction and projection of tuples in the object language --- --- The function pairs @desugarTupX@/@sugarTupX@ could be used directly in --- 'Syntactic' instances if it wasn't for the extra @(`Proxy` ctx)@ arguments. --- For this reason, 'Syntactic' instances have to be written manually for each --- context. The module "Language.Syntactic.Features.TupleSyntacticPoly" provides --- instances for a 'Poly' context. The exact same code can be used to make --- instances for other contexts -- just copy/paste and replace 'Poly' and 'poly' --- with the desired context (and probably add an extra constraint in the class --- contexts). - -module Language.Syntactic.Features.Tuple where - - - -import Data.Hash -import Data.Proxy -import Data.Tuple.Select - -import Language.Syntactic -import Language.Syntactic.Features.Symbol - - - --------------------------------------------------------------------------------- --- * Construction --------------------------------------------------------------------------------- - --- | Expressions for constructing tuples -data Tuple ctx a - where - Tup2 :: Sat ctx (a,b) => Tuple ctx (a :-> b :-> Full (a,b)) - Tup3 :: Sat ctx (a,b,c) => Tuple ctx (a :-> b :-> c :-> Full (a,b,c)) - Tup4 :: Sat ctx (a,b,c,d) => Tuple ctx (a :-> b :-> c :-> d :-> Full (a,b,c,d)) - Tup5 :: Sat ctx (a,b,c,d,e) => Tuple ctx (a :-> b :-> c :-> d :-> e :-> Full (a,b,c,d,e)) - Tup6 :: Sat ctx (a,b,c,d,e,f) => Tuple ctx (a :-> b :-> c :-> d :-> e :-> f :-> Full (a,b,c,d,e,f)) - Tup7 :: Sat ctx (a,b,c,d,e,f,g) => Tuple ctx (a :-> b :-> c :-> d :-> e :-> f :-> g :-> Full (a,b,c,d,e,f,g)) - -instance WitnessCons (Tuple ctx) - where - witnessCons Tup2 = ConsWit - witnessCons Tup3 = ConsWit - witnessCons Tup4 = ConsWit - witnessCons Tup5 = ConsWit - witnessCons Tup6 = ConsWit - witnessCons Tup7 = ConsWit - -instance WitnessSat (Tuple ctx) - where - type Context (Tuple ctx) = ctx - witnessSat Tup2 = Witness' - witnessSat Tup3 = Witness' - witnessSat Tup4 = Witness' - witnessSat Tup5 = Witness' - witnessSat Tup6 = Witness' - witnessSat Tup7 = Witness' - -instance IsSymbol (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" (,,,,,,) - -instance ExprEq (Tuple ctx) where exprEq = exprEqSym; exprHash = exprHashSym -instance Render (Tuple ctx) where renderPart = renderPartSym -instance Eval (Tuple ctx) where evaluate = evaluateSym -instance ToTree (Tuple ctx) - --- | Partial `Tuple` projection with explicit context -prjTuple :: (Tuple ctx :<: sup) => Proxy ctx -> sup a -> Maybe (Tuple ctx a) -prjTuple _ = project - - - -desugarTup2 - :: ( Syntactic a dom - , Syntactic b dom - , Sat ctx (Internal a, Internal b) - , Tuple ctx :<: dom - ) - => Proxy ctx - -> (a,b) - -> ASTF dom (Internal a, Internal b) -desugarTup2 ctx (a,b) = inject (Tup2 `withContext` ctx) - :$: desugar a - :$: desugar b - -desugarTup3 - :: ( Syntactic a dom - , Syntactic b dom - , Syntactic c dom - , Sat ctx (Internal a, Internal b, Internal c) - , Tuple ctx :<: dom - ) - => Proxy ctx - -> (a,b,c) - -> ASTF dom (Internal a, Internal b, Internal c) -desugarTup3 ctx (a,b,c) = inject (Tup3 `withContext` ctx) - :$: desugar a - :$: desugar b - :$: desugar c - -desugarTup4 - :: ( Syntactic a dom - , Syntactic b dom - , Syntactic c dom - , Syntactic d dom - , Sat ctx (Internal a, Internal b, Internal c, Internal d) - , Tuple ctx :<: dom - ) - => Proxy ctx - -> (a,b,c,d) - -> ASTF dom (Internal a, Internal b, Internal c, Internal d) -desugarTup4 ctx (a,b,c,d) = inject (Tup4 `withContext` ctx) - :$: desugar a - :$: desugar b - :$: desugar c - :$: desugar d - -desugarTup5 - :: ( Syntactic a dom - , Syntactic b dom - , Syntactic c dom - , Syntactic d dom - , Syntactic e dom - , Sat ctx (Internal a, Internal b, Internal c, Internal d, Internal e) - , Tuple ctx :<: dom - ) - => Proxy ctx - -> (a,b,c,d,e) - -> ASTF dom (Internal a, Internal b, Internal c, Internal d, Internal e) -desugarTup5 ctx (a,b,c,d,e) = inject (Tup5 `withContext` ctx) - :$: desugar a - :$: desugar b - :$: desugar c - :$: desugar d - :$: desugar e - -desugarTup6 - :: ( Syntactic a dom - , Syntactic b dom - , Syntactic c dom - , Syntactic d dom - , Syntactic e dom - , Syntactic f dom - , Sat ctx (Internal a, Internal b, Internal c, Internal d, Internal e, Internal f) - , Tuple ctx :<: dom - ) - => Proxy ctx - -> (a,b,c,d,e,f) - -> ASTF dom (Internal a, Internal b, Internal c, Internal d, Internal e, Internal f) -desugarTup6 ctx (a,b,c,d,e,f) = inject (Tup6 `withContext` ctx) - :$: desugar a - :$: desugar b - :$: desugar c - :$: desugar d - :$: desugar e - :$: desugar f - -desugarTup7 - :: ( Syntactic a dom - , Syntactic b dom - , Syntactic c dom - , Syntactic d dom - , Syntactic e dom - , Syntactic f dom - , Syntactic g dom - , Sat ctx (Internal a, Internal b, Internal c, Internal d, Internal e, Internal f, Internal g) - , Tuple ctx :<: dom - ) - => Proxy ctx - -> (a,b,c,d,e,f,g) - -> ASTF dom (Internal a, Internal b, Internal c, Internal d, Internal e, Internal f, Internal g) -desugarTup7 ctx (a,b,c,d,e,f,g) = inject (Tup7 `withContext` ctx) - :$: desugar a - :$: desugar b - :$: desugar c - :$: desugar d - :$: desugar e - :$: desugar f - :$: desugar g - - - --------------------------------------------------------------------------------- --- * Projection --------------------------------------------------------------------------------- - --- | Expressions for selecting elements of a tuple -data Select ctx a - where - Sel1 :: (Sel1 a b, Sat ctx b) => Select ctx (a :-> Full b) - Sel2 :: (Sel2 a b, Sat ctx b) => Select ctx (a :-> Full b) - Sel3 :: (Sel3 a b, Sat ctx b) => Select ctx (a :-> Full b) - Sel4 :: (Sel4 a b, Sat ctx b) => Select ctx (a :-> Full b) - Sel5 :: (Sel5 a b, Sat ctx b) => Select ctx (a :-> Full b) - Sel6 :: (Sel6 a b, Sat ctx b) => Select ctx (a :-> Full b) - Sel7 :: (Sel7 a b, Sat ctx b) => Select ctx (a :-> Full b) - -instance WitnessCons (Select ctx) - where - witnessCons Sel1 = ConsWit - witnessCons Sel2 = ConsWit - witnessCons Sel3 = ConsWit - witnessCons Sel4 = ConsWit - witnessCons Sel5 = ConsWit - witnessCons Sel6 = ConsWit - witnessCons Sel7 = ConsWit - -instance WitnessSat (Select ctx) - where - type Context (Select ctx) = ctx - witnessSat Sel1 = Witness' - witnessSat Sel2 = Witness' - witnessSat Sel3 = Witness' - witnessSat Sel4 = Witness' - witnessSat Sel5 = Witness' - witnessSat Sel6 = Witness' - witnessSat Sel7 = Witness' - -instance IsSymbol (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 - -instance ExprEq (Select ctx) where exprEq = exprEqSym; exprHash = exprHashSym -instance Render (Select ctx) where renderPart = renderPartSym -instance Eval (Select ctx) where evaluate = evaluateSym -instance ToTree (Select ctx) - --- | Partial `Select` projection with explicit context -prjSelect :: (Select ctx :<: sup) => Proxy ctx -> sup a -> Maybe (Select ctx a) -prjSelect _ = project - --- | Return the selected position, e.g. --- --- > selectPos (Sel3 poly :: Select Poly ((Int,Int,Int,Int) :-> Full Int)) = 3 -selectPos :: Select ctx a -> Int -selectPos Sel1 = 1 -selectPos Sel2 = 2 -selectPos Sel3 = 3 -selectPos Sel4 = 4 -selectPos Sel5 = 5 -selectPos Sel6 = 6 -selectPos Sel7 = 7 - - - -sugarTup2 - :: ( Syntactic a dom - , Syntactic b dom - , Sat ctx (Internal a) - , Sat ctx (Internal b) - , Select ctx :<: dom - ) - => Proxy ctx - -> ASTF dom (Internal a, Internal b) - -> (a,b) -sugarTup2 ctx a = - ( sugar $ inject (Sel1 `withContext` ctx) :$: a - , sugar $ inject (Sel2 `withContext` ctx) :$: a - ) - -sugarTup3 - :: ( Syntactic a dom - , Syntactic b dom - , Syntactic c dom - , Sat ctx (Internal a) - , Sat ctx (Internal b) - , Sat ctx (Internal c) - , Select ctx :<: dom - ) - => Proxy ctx - -> ASTF dom (Internal a, Internal b, Internal c) - -> (a,b,c) -sugarTup3 ctx a = - ( sugar $ inject (Sel1 `withContext` ctx) :$: a - , sugar $ inject (Sel2 `withContext` ctx) :$: a - , sugar $ inject (Sel3 `withContext` ctx) :$: a - ) - -sugarTup4 - :: ( Syntactic a dom - , Syntactic b dom - , Syntactic c dom - , Syntactic d dom - , Sat ctx (Internal a) - , Sat ctx (Internal b) - , Sat ctx (Internal c) - , Sat ctx (Internal d) - , Select ctx :<: dom - ) - => Proxy ctx - -> ASTF dom (Internal a, Internal b, Internal c, Internal d) - -> (a,b,c,d) -sugarTup4 ctx a = - ( sugar $ inject (Sel1 `withContext` ctx) :$: a - , sugar $ inject (Sel2 `withContext` ctx) :$: a - , sugar $ inject (Sel3 `withContext` ctx) :$: a - , sugar $ inject (Sel4 `withContext` ctx) :$: a - ) - -sugarTup5 - :: ( Syntactic a dom - , Syntactic b dom - , Syntactic c dom - , Syntactic d dom - , Syntactic e dom - , Sat ctx (Internal a) - , Sat ctx (Internal b) - , Sat ctx (Internal c) - , Sat ctx (Internal d) - , Sat ctx (Internal e) - , Select ctx :<: dom - ) - => Proxy ctx - -> ASTF dom (Internal a, Internal b, Internal c, Internal d, Internal e) - -> (a,b,c,d,e) -sugarTup5 ctx a = - ( sugar $ inject (Sel1 `withContext` ctx) :$: a - , sugar $ inject (Sel2 `withContext` ctx) :$: a - , sugar $ inject (Sel3 `withContext` ctx) :$: a - , sugar $ inject (Sel4 `withContext` ctx) :$: a - , sugar $ inject (Sel5 `withContext` ctx) :$: a - ) - -sugarTup6 - :: ( Syntactic a dom - , Syntactic b dom - , Syntactic c dom - , Syntactic d dom - , Syntactic e dom - , Syntactic f dom - , Sat ctx (Internal a) - , Sat ctx (Internal b) - , Sat ctx (Internal c) - , Sat ctx (Internal d) - , Sat ctx (Internal e) - , Sat ctx (Internal f) - , Select ctx :<: dom - ) - => Proxy ctx - -> ASTF dom (Internal a, Internal b, Internal c, Internal d, Internal e, Internal f) - -> (a,b,c,d,e,f) -sugarTup6 ctx a = - ( sugar $ inject (Sel1 `withContext` ctx) :$: a - , sugar $ inject (Sel2 `withContext` ctx) :$: a - , sugar $ inject (Sel3 `withContext` ctx) :$: a - , sugar $ inject (Sel4 `withContext` ctx) :$: a - , sugar $ inject (Sel5 `withContext` ctx) :$: a - , sugar $ inject (Sel6 `withContext` ctx) :$: a - ) - -sugarTup7 - :: ( Syntactic a dom - , Syntactic b dom - , Syntactic c dom - , Syntactic d dom - , Syntactic e dom - , Syntactic f dom - , Syntactic g dom - , Sat ctx (Internal a) - , Sat ctx (Internal b) - , Sat ctx (Internal c) - , Sat ctx (Internal d) - , Sat ctx (Internal e) - , Sat ctx (Internal f) - , Sat ctx (Internal g) - , Select ctx :<: dom - ) - => Proxy ctx - -> ASTF dom (Internal a, Internal b, Internal c, Internal d, Internal e, Internal f, Internal g) - -> (a,b,c,d,e,f,g) -sugarTup7 ctx a = - ( sugar $ inject (Sel1 `withContext` ctx) :$: a - , sugar $ inject (Sel2 `withContext` ctx) :$: a - , sugar $ inject (Sel3 `withContext` ctx) :$: a - , sugar $ inject (Sel4 `withContext` ctx) :$: a - , sugar $ inject (Sel5 `withContext` ctx) :$: a - , sugar $ inject (Sel6 `withContext` ctx) :$: a - , sugar $ inject (Sel7 `withContext` ctx) :$: a - ) - diff --git a/Language/Syntactic/Features/TupleSyntacticPoly.hs b/Language/Syntactic/Features/TupleSyntacticPoly.hs deleted file mode 100644 --- a/Language/Syntactic/Features/TupleSyntacticPoly.hs +++ /dev/null @@ -1,138 +0,0 @@ -{-# LANGUAGE UndecidableInstances #-} - --- | 'Syntactic' instances for tuples with 'Poly' context -module Language.Syntactic.Features.TupleSyntacticPoly where - - - -import Language.Syntactic.Syntax -import Language.Syntactic.Features.Tuple - - - -instance - ( Syntactic a dom - , Syntactic b dom - , Tuple Poly :<: dom - , Select Poly :<: dom - ) => - Syntactic (a,b) dom - where - type Internal (a,b) = - ( Internal a - , Internal b - ) - - desugar = desugarTup2 poly - sugar = sugarTup2 poly - -instance - ( Syntactic a dom - , Syntactic b dom - , Syntactic c dom - , Tuple Poly :<: dom - , Select Poly :<: dom - ) => - Syntactic (a,b,c) dom - where - type Internal (a,b,c) = - ( Internal a - , Internal b - , Internal c - ) - - desugar = desugarTup3 poly - sugar = sugarTup3 poly - -instance - ( Syntactic a dom - , Syntactic b dom - , Syntactic c dom - , Syntactic d dom - , Tuple Poly :<: dom - , Select Poly :<: dom - ) => - Syntactic (a,b,c,d) dom - where - type Internal (a,b,c,d) = - ( Internal a - , Internal b - , Internal c - , Internal d - ) - - desugar = desugarTup4 poly - sugar = sugarTup4 poly - -instance - ( Syntactic a dom - , Syntactic b dom - , Syntactic c dom - , Syntactic d dom - , Syntactic e dom - , Tuple Poly :<: dom - , Select Poly :<: dom - ) => - Syntactic (a,b,c,d,e) dom - where - type Internal (a,b,c,d,e) = - ( Internal a - , Internal b - , Internal c - , Internal d - , Internal e - ) - - desugar = desugarTup5 poly - sugar = sugarTup5 poly - -instance - ( Syntactic a dom - , Syntactic b dom - , Syntactic c dom - , Syntactic d dom - , Syntactic e dom - , Syntactic f dom - , Tuple Poly :<: dom - , Select Poly :<: dom - ) => - Syntactic (a,b,c,d,e,f) dom - where - type Internal (a,b,c,d,e,f) = - ( Internal a - , Internal b - , Internal c - , Internal d - , Internal e - , Internal f - ) - - desugar = desugarTup6 poly - sugar = sugarTup6 poly - -instance - ( Syntactic a dom - , Syntactic b dom - , Syntactic c dom - , Syntactic d dom - , Syntactic e dom - , Syntactic f dom - , Syntactic g dom - , Tuple Poly :<: dom - , Select Poly :<: dom - ) => - Syntactic (a,b,c,d,e,f,g) dom - where - type Internal (a,b,c,d,e,f,g) = - ( Internal a - , Internal b - , Internal c - , Internal d - , Internal e - , Internal f - , Internal g - ) - - desugar = desugarTup7 poly - sugar = sugarTup7 poly - diff --git a/Language/Syntactic/Features/TupleSyntacticSimple.hs b/Language/Syntactic/Features/TupleSyntacticSimple.hs deleted file mode 100644 --- a/Language/Syntactic/Features/TupleSyntacticSimple.hs +++ /dev/null @@ -1,138 +0,0 @@ -{-# LANGUAGE UndecidableInstances #-} - --- | 'Syntactic' instances for tuples with 'SimpleCtx' context -module Language.Syntactic.Features.TupleSyntacticSimple where - - - -import Language.Syntactic.Syntax -import Language.Syntactic.Features.Tuple - - - -instance - ( Syntactic a dom, Eq (Internal a), Show (Internal a) - , Syntactic b dom, Eq (Internal b), Show (Internal b) - , Tuple SimpleCtx :<: dom - , Select SimpleCtx :<: dom - ) => - Syntactic (a,b) dom - where - type Internal (a,b) = - ( Internal a - , Internal b - ) - - desugar = desugarTup2 simpleCtx - sugar = sugarTup2 simpleCtx - -instance - ( Syntactic a dom, Eq (Internal a), Show (Internal a) - , Syntactic b dom, Eq (Internal b), Show (Internal b) - , Syntactic c dom, Eq (Internal c), Show (Internal c) - , Tuple SimpleCtx :<: dom - , Select SimpleCtx :<: dom - ) => - Syntactic (a,b,c) dom - where - type Internal (a,b,c) = - ( Internal a - , Internal b - , Internal c - ) - - desugar = desugarTup3 simpleCtx - sugar = sugarTup3 simpleCtx - -instance - ( Syntactic a dom, Eq (Internal a), Show (Internal a) - , Syntactic b dom, Eq (Internal b), Show (Internal b) - , Syntactic c dom, Eq (Internal c), Show (Internal c) - , Syntactic d dom, Eq (Internal d), Show (Internal d) - , Tuple SimpleCtx :<: dom - , Select SimpleCtx :<: dom - ) => - Syntactic (a,b,c,d) dom - where - type Internal (a,b,c,d) = - ( Internal a - , Internal b - , Internal c - , Internal d - ) - - desugar = desugarTup4 simpleCtx - sugar = sugarTup4 simpleCtx - -instance - ( Syntactic a dom, Eq (Internal a), Show (Internal a) - , Syntactic b dom, Eq (Internal b), Show (Internal b) - , Syntactic c dom, Eq (Internal c), Show (Internal c) - , Syntactic d dom, Eq (Internal d), Show (Internal d) - , Syntactic e dom, Eq (Internal e), Show (Internal e) - , Tuple SimpleCtx :<: dom - , Select SimpleCtx :<: dom - ) => - Syntactic (a,b,c,d,e) dom - where - type Internal (a,b,c,d,e) = - ( Internal a - , Internal b - , Internal c - , Internal d - , Internal e - ) - - desugar = desugarTup5 simpleCtx - sugar = sugarTup5 simpleCtx - -instance - ( Syntactic a dom, Eq (Internal a), Show (Internal a) - , Syntactic b dom, Eq (Internal b), Show (Internal b) - , Syntactic c dom, Eq (Internal c), Show (Internal c) - , Syntactic d dom, Eq (Internal d), Show (Internal d) - , Syntactic e dom, Eq (Internal e), Show (Internal e) - , Syntactic f dom, Eq (Internal f), Show (Internal f) - , Tuple SimpleCtx :<: dom - , Select SimpleCtx :<: dom - ) => - Syntactic (a,b,c,d,e,f) dom - where - type Internal (a,b,c,d,e,f) = - ( Internal a - , Internal b - , Internal c - , Internal d - , Internal e - , Internal f - ) - - desugar = desugarTup6 simpleCtx - sugar = sugarTup6 simpleCtx - -instance - ( Syntactic a dom, Eq (Internal a), Show (Internal a) - , Syntactic b dom, Eq (Internal b), Show (Internal b) - , Syntactic c dom, Eq (Internal c), Show (Internal c) - , Syntactic d dom, Eq (Internal d), Show (Internal d) - , Syntactic e dom, Eq (Internal e), Show (Internal e) - , Syntactic f dom, Eq (Internal f), Show (Internal f) - , Syntactic g dom, Eq (Internal g), Show (Internal g) - , Tuple SimpleCtx :<: dom - , Select SimpleCtx :<: dom - ) => - Syntactic (a,b,c,d,e,f,g) dom - where - type Internal (a,b,c,d,e,f,g) = - ( Internal a - , Internal b - , Internal c - , Internal d - , Internal e - , Internal f - , Internal g - ) - - desugar = desugarTup7 simpleCtx - sugar = sugarTup7 simpleCtx - diff --git a/Language/Syntactic/Frontend/Monad.hs b/Language/Syntactic/Frontend/Monad.hs new file mode 100644 --- /dev/null +++ b/Language/Syntactic/Frontend/Monad.hs @@ -0,0 +1,64 @@ +module Language.Syntactic.Frontend.Monad where + + + +import Control.Monad.Cont +import Data.Typeable + +import Language.Syntactic +import Language.Syntactic.Constructs.Binding.HigherOrder +import Language.Syntactic.Constructs.Monad + + + +-- | User interface to embedded monadic programs +newtype Mon ctx dom m a + where + Mon + :: { unMon :: forall r . (Monad m, Typeable r) => + Cont (ASTF (HODomain ctx dom) (m r)) a + } + -> Mon ctx dom m a + +deriving instance Functor (Mon ctx dom m) + +instance (Monad m) => Monad (Mon ctx dom m) + where + return a = Mon $ return a + ma >>= f = Mon $ unMon ma >>= unMon . f + +-- | One-layer desugaring of monadic actions +desugarMonad + :: ( MONAD m :<: dom + , Monad m + , Typeable1 m + , Typeable a + , Sat ctx a + ) + => Mon ctx dom m (ASTF (HODomain ctx dom) a) + -> ASTF (HODomain ctx dom) (m a) +desugarMonad = flip runCont (sugarSym Return) . unMon + +-- | One-layer sugaring of monadic actions +sugarMonad + :: ( MONAD m :<: dom + , Monad m + , Typeable1 m + , Typeable a + , Sat ctx a + ) + => ASTF (HODomain ctx dom) (m a) + -> Mon ctx dom m (ASTF (HODomain ctx dom) a) +sugarMonad ma = Mon $ cont $ sugarSym Bind ma + +instance ( MONAD m :<: dom + , Syntactic a (HODomain ctx dom) + , Monad m, Typeable1 m + , Sat ctx (Internal a) + ) => + Syntactic (Mon ctx dom m a) (HODomain ctx dom) + where + type Internal (Mon ctx dom m a) = m (Internal a) + desugar = desugarMonad . fmap desugar + sugar = fmap sugar . sugarMonad + 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 @@ -15,7 +15,7 @@ import Data.Proxy import Language.Syntactic -import Language.Syntactic.Features.Binding +import Language.Syntactic.Constructs.Binding import Language.Syntactic.Sharing.Utils @@ -53,10 +53,6 @@ render (Node a) = showNode a instance ToTree (Node ctx) - --- | Partial `Node` projection with explicit context -prjNode :: (Node ctx :<: sup) => Proxy ctx -> sup a -> Maybe (Node ctx a) -prjNode _ = project 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 @@ -32,7 +32,7 @@ reifyGraphM :: forall ctx dom a . Typeable a - => (forall a . ASTF dom a -> Maybe (Witness' ctx a)) + => (forall a . ASTF dom a -> Maybe (SatWit ctx a)) -> IORef NodeId -> IORef (History (AST dom)) -> ASTF dom a @@ -43,7 +43,7 @@ reifyNode :: Typeable b => ASTF dom b -> GraphMonad ctx dom (Full b) reifyNode a = case canShare a of Nothing -> reifyRec a - Just Witness' | a `seq` True -> do + Just SatWit | a `seq` True -> do st <- liftIO $ makeStableName a hist <- liftIO $ readIORef history case lookHistory hist (StName st) of @@ -67,11 +67,11 @@ -- is well-behaved in the sense that the worst thing that could happen is that -- sharing is lost. It is not possible to get false sharing. reifyGraph :: Typeable a - => (forall a . ASTF dom a -> Maybe (Witness' ctx a)) + => (forall a . ASTF dom a -> Maybe (SatWit ctx a)) -- ^ A function that decides whether a given node can be shared. -- 'Nothing' means \"don't share\"; 'Just' means \"share\". Nodes whose -- result type fulfills @(`Sat` ctx a)@ can be shared, which is why the - -- function returns a 'Witness''. + -- function returns a 'SatWit'. -> ASTF dom a -> IO (ASG ctx dom a) reifyGraph canShare a = do 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 @@ -1,8 +1,9 @@ -- | This module is similar to "Language.Syntactic.Sharing.Reify", but operates --- on 'HOAST' rather than a general 'AST'. The reason for having this module is --- that when using 'HOAST', it is important to do simultaneous sharing analysis --- and 'HOLambda' reification. Obviously we cannot do sharing analysis first --- (using 'Language.Syntactic.Sharing.Reify.reifyGraph' from +-- on @`AST` (`HODomain` ctx dom)@ rather than a general 'AST'. The reason for +-- having this module is that when using 'HODomain', it is important to do +-- simultaneous sharing analysis and 'HOLambda' reification. Obviously we cannot +-- do sharing analysis first (using +-- 'Language.Syntactic.Sharing.Reify.reifyGraph' from -- "Language.Syntactic.Sharing.Reify"), since it needs to be able to look inside -- 'HOLambda'. On the other hand, if we did 'HOLambda' reification first (using -- 'reify'), we would destroy the sharing. @@ -26,8 +27,8 @@ import Data.Proxy import Language.Syntactic -import Language.Syntactic.Features.Binding -import Language.Syntactic.Features.Binding.HigherOrder +import Language.Syntactic.Constructs.Binding +import Language.Syntactic.Constructs.Binding.HigherOrder import Language.Syntactic.Sharing.Graph import Language.Syntactic.Sharing.StableName import qualified Language.Syntactic.Sharing.Reify -- For Haddock @@ -45,19 +46,20 @@ reifyGraphM :: forall ctx dom a . Typeable a - => (forall a . HOASTF ctx dom a -> Maybe (Witness' ctx a)) + => (forall a . ASTF (HODomain ctx dom) a -> Maybe (SatWit ctx a)) -> IORef VarId -> IORef NodeId - -> IORef (History (HOAST ctx dom)) - -> HOASTF ctx dom a + -> IORef (History (AST (HODomain ctx dom))) + -> ASTF (HODomain ctx dom) a -> GraphMonad ctx dom (Full a) reifyGraphM canShare vSupp nSupp history = reifyNode where - reifyNode :: Typeable b => HOASTF ctx dom b -> GraphMonad ctx dom (Full b) + reifyNode :: Typeable b => + ASTF (HODomain ctx dom) b -> GraphMonad ctx dom (Full b) reifyNode a = case canShare a of Nothing -> reifyRec a - Just Witness' | a `seq` True -> do + Just SatWit | a `seq` True -> do st <- liftIO $ makeStableName a hist <- liftIO $ readIORef history case lookHistory hist (StName st) of @@ -69,7 +71,7 @@ tell [(n, SomeAST a')] return $ Symbol $ InjectL $ Node n - reifyRec :: HOAST ctx dom b -> GraphMonad ctx dom b + 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 @@ -83,8 +85,8 @@ -- | Convert a syntax tree to a sharing-preserving graph reifyGraphTop :: Typeable a - => (forall a . HOASTF ctx dom a -> Maybe (Witness' ctx a)) - -> HOASTF ctx dom a + => (forall a . ASTF (HODomain ctx dom) a -> Maybe (SatWit ctx a)) + -> ASTF (HODomain ctx dom) a -> IO (ASG ctx (Lambda ctx :+: Variable ctx :+: dom) a, VarId) reifyGraphTop canShare a = do vSupp <- newIORef 0 @@ -100,16 +102,16 @@ -- This function is not referentially transparent (hence the 'IO'). However, it -- is well-behaved in the sense that the worst thing that could happen is that -- sharing is lost. It is not possible to get false sharing. -reifyGraph :: Reifiable ctx a dom internal - => (forall a . HOASTF ctx dom a -> Maybe (Witness' ctx a)) +reifyGraph :: Syntactic a (HODomain ctx dom) + => (forall a . ASTF (HODomain ctx dom) a -> Maybe (SatWit ctx a)) -- ^ A function that decides whether a given node can be shared. -- 'Nothing' means \"don't share\"; 'Just' means \"share\". Nodes whose -- result type fulfills @(`Sat` ctx a)@ can be shared, which is why the - -- function returns a 'Witness''. + -- function returns a 'SatWit'. -> a -> IO - ( ASG ctx (Lambda ctx :+: Variable ctx :+: dom) (NAryEval internal) + ( ASG ctx (Lambda ctx :+: Variable ctx :+: dom) (Internal a) , VarId ) -reifyGraph canShare = reifyGraphTop canShare . lambdaN . desugarN +reifyGraph canShare = reifyGraphTop canShare . desugar diff --git a/Language/Syntactic/Sharing/SimpleCodeMotion.hs b/Language/Syntactic/Sharing/SimpleCodeMotion.hs new file mode 100644 --- /dev/null +++ b/Language/Syntactic/Sharing/SimpleCodeMotion.hs @@ -0,0 +1,190 @@ +-- | Simple code motion transformation performing common sub-expression +-- elimination and variable hoisting. Note that the implementation is very +-- inefficient. +-- +-- The code is based on an implementation by Gergely Dévai. + +module Language.Syntactic.Sharing.SimpleCodeMotion + ( codeMotion + , reifySmart + ) where + + + +import Control.Monad.State +import Data.Set as Set +import Data.Typeable + +import Data.Proxy + +import Language.Syntactic +import Language.Syntactic.Constructs.Binding +import Language.Syntactic.Constructs.Binding.HigherOrder + + + +-- | 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 + -> ASTF dom a -- ^ Replacing sub-expression + -> ASTF dom b -- ^ Whole expression + -> ASTF dom b +substitute ctx x y a = 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 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 + +nonTerminal :: AST dom a -> Bool +nonTerminal (_ :$: _) = True +nonTerminal _ = False + +data SomeAST ctx dom + where + SomeAST :: (Sat ctx a, Typeable a) => ASTF dom a -> SomeAST ctx dom + +-- | 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 + -- ^ Counting the number of occurrences of an expression in the + -- environment + , dependencies :: Set VarId + -- ^ The set of variables that are not allowed to occur in the chosen + -- expression + } + +independent :: (Variable ctx :<: dom) => Env ctx dom -> AST dom a -> Bool +independent env (prjCtx (context env) -> Just (Variable v)) = + not (v `member` dependencies env) +independent env (f :$: a) = independent env f && independent 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 + -- Lifting dependent expressions is semantically incorrect + where + heuristic = 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 + , MaybeWitnessSat ctx dom + , Typeable a + ) + => ASTF dom a -> Maybe (SomeAST ctx dom) +choose a = chooseEnv env a + where + ctx = Proxy :: Proxy ctx + + env :: Env ctx dom + env = Env + { inLambda = False + , counter = \(SomeAST b) -> count ctx 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 + = Just (SomeAST a) + | otherwise = chooseEnvSub 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 + where + env' = env + { inLambda = True + , dependencies = insert v (dependencies env) + } +chooseEnvSub env (f :$: a) = chooseEnvSub env f `mplus` chooseEnv 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 + , MaybeWitnessSat ctx dom + , Typeable a + ) + => Proxy ctx -> ASTF dom a -> State VarId (ASTF dom a) +codeMotion ctx a + | Just SatWit <- maybeWitnessSat ctx a + , Just b <- choose a + = share b + | otherwise = descend ctx a + where + share :: Sat ctx a => SomeAST ctx dom -> State VarId (ASTF dom a) + share (SomeAST b) = do + b' <- codeMotion ctx b + v <- get; put (v+1) + let x = inject (Variable v `withContext` ctx) + body <- codeMotion ctx $ substitute ctx b x a + return + $ inject (letBind ctx) + :$: b' + :$: (inject (Lambda v `withContext` ctx) :$: body) + +descend + :: ( Variable ctx :<: dom + , Lambda ctx :<: dom + , Let ctx ctx :<: dom + , ExprEq dom + , MaybeWitnessSat 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 + +-- | Like 'reify' but with common sub-expression elimination and variable +-- hoisting +reifySmart + :: ( Let ctx ctx :<: dom + , ExprEq dom + , MaybeWitnessSat ctx dom + , Syntactic a (HODomain ctx dom) + ) + => Proxy ctx + -> a + -> ASTF (Lambda ctx :+: Variable ctx :+: dom) (Internal a) +reifySmart ctx = flip evalState 0 . (codeMotion ctx <=< reifyM) . desugar + diff --git a/Language/Syntactic/Syntax.hs b/Language/Syntactic/Syntax.hs --- a/Language/Syntactic/Syntax.hs +++ b/Language/Syntactic/Syntax.hs @@ -60,6 +60,7 @@ Full (..) , (:->) (..) , HList (..) + , WrapFull (..) , ConsType , ConsEval , EvalResult @@ -72,20 +73,27 @@ , mapHList , mapHListM , appHList + , appEvalHList , ($:) , AST (..) , ASTF , (:+:) (..) + , ApplySym + , appSym + , appSymCtx -- * Subsumption , (:<:) (..) + , injCtx + , prjCtx -- * Syntactic sugar , Syntactic (..) , resugar , SyntacticN (..) + , sugarSym + , sugarSymCtx -- * AST processing - , queryNodeI , queryNode - , transformNodeC + , queryNodeSimple , transformNode -- * Restricted syntax trees , Sat (..) @@ -98,9 +106,12 @@ -- -- I don't know if the fix just removes the warning, or if it means -- that 'Sat (..)' is enough. - , Witness' (..) - , witness' + , witnessByProxy + , SatWit (..) + , fromSatWit , WitnessSat (..) + , MaybeWitnessSat (..) + , maybeWitnessSatDefault , withContext , Poly , poly @@ -139,6 +150,21 @@ 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 +-- its constructor to be indexed by @(`Full` a)@. That is, use +-- +-- > HList (WrapFull c) ... +-- +-- instead of +-- +-- > HList c ... +-- +-- if @c@ is not indexed by @(`Full` a)@. +data WrapFull c a + where + WrapFull :: { unwrapFull :: c a } -> WrapFull c (Full a) + -- | Fully or partially applied constructor -- -- This class is private to the module to guarantee that all members of the @@ -155,40 +181,42 @@ type ConsEval' a type EvalResult' 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) - + 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 instance ConsType' (Full a) where type ConsEval' (Full a) = a type EvalResult' (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 + 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 instance ConsType' b => ConsType' (a :-> b) where type ConsEval' (a :-> b) = a -> ConsEval' b type EvalResult' (a :-> b) = EvalResult' 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 + 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 -- | Fully or partially applied constructor -- @@ -249,11 +277,16 @@ (forall a . c1 (Full a) -> m (c2 (Full a))) -> HList c1 a -> m (HList c2 a) mapHListM = mapHListM' --- | Apply the syntax tree to listed arguments +-- | Apply the syntax tree to the listed arguments appHList :: ConsType a => AST dom a -> HList (AST dom) a -> ASTF dom (EvalResult a) appHList = appHList' +-- | Apply the evaluation function to the listed arguments +appEvalHList :: ConsType a => + ConsEval a -> HList Identity a -> EvalResult a +appEvalHList = appEvalHList' + -- | Semantic constructor application ($:) :: (a :-> b) -> a -> b Partial f $: a = f a @@ -290,6 +323,37 @@ +-- | Class that performs the type-level recursion needed by 'appSym' +class ApplySym a f dom | a dom -> f, f -> a dom + where + appSym' :: AST dom a -> f + +instance ApplySym (Full a) (ASTF dom a) dom + where + appSym' = id + +instance (Typeable a, ApplySym b f' dom) => + ApplySym (a :-> b) (ASTF dom a -> f') dom + where + appSym' sym a = appSym' (sym :$: a) + +-- | Generic symbol application +-- +-- 'appSym' has any type of the form: +-- +-- > 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) + +-- | Generic symbol application with explicit context +appSymCtx :: (ApplySym a f dom, ConsType a, sym ctx :<: dom) => + Proxy ctx -> sym ctx a -> f +appSymCtx _ = appSym + + + -------------------------------------------------------------------------------- -- * Subsumption -------------------------------------------------------------------------------- @@ -331,6 +395,16 @@ +-- | 'inject' with explicit context +injCtx :: (sub ctx :<: sup, ConsType a) => Proxy ctx -> sub ctx a -> sup a +injCtx _ = inject + +-- | 'project' with explicit context +prjCtx :: (sub ctx :<: sup) => Proxy ctx -> sup a -> Maybe (sub ctx a) +prjCtx _ = project + + + -------------------------------------------------------------------------------- -- * Syntactic sugar -------------------------------------------------------------------------------- @@ -398,26 +472,63 @@ +-- | \"Sugared\" symbol application +-- +-- 'sugarSym' has any type of the form: +-- +-- > sugarSym :: +-- > ( expr :<: AST dom +-- > , Syntactic a dom +-- > , Syntactic b dom +-- > , ... +-- > , Syntactic x dom +-- > ) => 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 +sugarSym = sugarN . appSym + +-- | \"Sugared\" symbol application with explicit context +sugarSymCtx + :: (ConsType a, sym ctx :<: dom, ApplySym a b dom, SyntacticN c b) + => Proxy ctx -> sym ctx a -> c +sugarSymCtx _ = sugarSym + + + -------------------------------------------------------------------------------- -- * AST processing -------------------------------------------------------------------------------- -newtype Wrap a b = Wrap {unWrap :: a} - -- Only used in the definition of 'queryNode' +newtype Const a b = Const {unConst :: a} + -- Only used in the definition of 'queryNodeSimple' --- | Like 'queryNode' but with the result indexed by the constructor's result --- type -queryNodeI :: forall dom a b - . (forall a . ConsType a => dom a -> HList (AST dom) a -> b (EvalResult a)) - -> ASTF dom a -> b a -queryNodeI f a = query a Nil +newtype WrapAST c dom a = WrapAST { unWrapAST :: c (AST dom a) } + -- Only used in the definition of 'transformNode' + +-- | Query an 'AST' using a function that gets direct access to the top-most +-- constructor and its sub-trees +-- +-- Note that, by instantiating the type @c@ with @`AST` dom'@, we get the +-- 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)) +-- > -> 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))) + -> ASTF dom a + -> c (Full a) +queryNode f a = query a Nil where - query :: AST dom c -> HList (AST dom) c -> b (EvalResult c) + 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 an 'AST' using a function that gets direct access to the top-most --- constructor and its sub-trees +-- | A simpler version of 'queryNode' -- -- This function can be used to create 'AST' traversal functions indexed by the -- symbol types, for example: @@ -432,7 +543,7 @@ -- > count' (InjectR a) args = count' a args -- > -- > count :: Count dom => ASTF dom a -> Int --- > count = queryNode count' +-- > count = queryNodeSimple count' -- -- Here, @count@ represents some static analysis on an 'AST'. Each constructor -- in the tree will be queried by @count'@ indexed by the corresponding symbol @@ -451,36 +562,21 @@ -- > instance Count Add -- > where -- > count' Add (a :*: b :*: Nil) = 1 + count a + count b -queryNode :: forall dom a b +queryNodeSimple :: forall dom a b . (forall a . ConsType a => dom a -> HList (AST dom) a -> b) - -> ASTF dom a -> b -queryNode f a = unWrap $ queryNodeI (\c -> Wrap . f c) a - - + -> ASTF dom a + -> b +queryNodeSimple f a = unConst $ queryNode (\c -> Const . f c) a --- | Like 'transformNode' but with the result wrapped in a type constructor @c@ -transformNodeC :: forall dom dom' 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)) ) -> ASTF dom a -> c (ASTF dom' a) -transformNodeC f a = transform a Nil - where - transform :: AST dom b -> HList (AST dom) b -> c (ASTF dom' (EvalResult b)) - transform (Symbol a) args = f a args - transform (c :$: a) args = transform c (a :*: args) - --- | Transform an 'AST' using a function that gets direct access to the top-most --- constructor and its sub-trees. This function is similar to 'queryNode', but --- returns a transformed 'AST' rather than abstract interpretation. -transformNode :: forall dom dom' a - . ( forall a . ConsType a - => dom a -> HList (AST dom) a -> ASTF dom' (EvalResult a) - ) - -> ASTF dom a - -> ASTF dom' a -transformNode f a = runIdentity $ transformNodeC (\c -> Identity . f c) a +transformNode f a = unWrapAST $ queryNode (\a args -> WrapAST (f a args)) a @@ -511,22 +607,48 @@ data Witness ctx a witness :: Witness ctx a +witnessByProxy :: Sat ctx a => Proxy ctx -> Proxy a -> Witness ctx a +witnessByProxy _ _ = witness + -- | Witness of a @(`Sat` ctx a)@ constraint. This is different from -- @(`Witness` ctx a)@, which witnesses the class encoded by @ctx@. 'Witness'' -- has a single constructor for all contexts, while 'Witness' has different -- constructors for different contexts. -data Witness' ctx a +data SatWit ctx a where - Witness' :: Sat ctx a => Witness' ctx a + SatWit :: Sat ctx a => SatWit ctx a -witness' :: Witness' ctx a -> Witness ctx a -witness' Witness' = witness +fromSatWit :: SatWit ctx a -> Witness ctx a +fromSatWit SatWit = witness --- | Symbols that act as witnesses of their result type -class WitnessSat sym +-- | Expressions that act as witnesses of their result type +class WitnessSat expr where - type Context sym - witnessSat :: sym a -> Witness' (Context sym) (EvalResult a) + type SatContext expr + witnessSat :: expr a -> SatWit (SatContext expr) (EvalResult 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)) + +instance MaybeWitnessSat ctx dom => MaybeWitnessSat ctx (AST dom) + where + maybeWitnessSat ctx (Symbol 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 + +-- | Convenient default implementation of 'maybeWitnessSat' +maybeWitnessSatDefault :: WitnessSat expr + => Proxy (SatContext expr) + -> expr a + -> Maybe (SatWit (SatContext expr) (EvalResult a)) +maybeWitnessSatDefault _ = Just . witnessSat -- | Type application for constraining the @ctx@ type of a parameterized symbol withContext :: sym ctx a -> Proxy ctx -> sym ctx a diff --git a/syntactic.cabal b/syntactic.cabal --- a/syntactic.cabal +++ b/syntactic.cabal @@ -1,5 +1,5 @@ Name: syntactic -Version: 0.6 +Version: 0.7 Synopsis: Generic abstract syntax, and utilities for embedded languages Description: This library provides: . @@ -21,6 +21,10 @@ object languages, such as Feldspar. Currently, it does not support cyclic programs. . + The following people have contributed to Syntactic: + . + * Anders Persson + . \[1\] /Data types à la carte/, by Wouter Swierstra, in /Journal of Functional Programming/, 2008 . @@ -41,6 +45,19 @@ 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 @@ -53,16 +70,19 @@ Language.Syntactic.Interpretation.Equality Language.Syntactic.Interpretation.Render Language.Syntactic.Interpretation.Evaluation - Language.Syntactic.Features.Annotate - Language.Syntactic.Features.Symbol - Language.Syntactic.Features.Literal - Language.Syntactic.Features.Condition - Language.Syntactic.Features.Tuple - Language.Syntactic.Features.TupleSyntacticPoly - Language.Syntactic.Features.TupleSyntacticSimple - Language.Syntactic.Features.Binding - Language.Syntactic.Features.Binding.HigherOrder - Language.Syntactic.Features.Binding.PartialEval + 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.Constructs.Binding + Language.Syntactic.Constructs.Binding.HigherOrder + Language.Syntactic.Constructs.Binding.Optimize + Language.Syntactic.Constructs.Monad + Language.Syntactic.Frontend.Monad + Language.Syntactic.Sharing.SimpleCodeMotion Language.Syntactic.Sharing.Utils Language.Syntactic.Sharing.Graph Language.Syntactic.Sharing.StableName @@ -83,19 +103,20 @@ Extensions: DeriveDataTypeable + DeriveFunctor + EmptyDataDecls FlexibleContexts FlexibleInstances FunctionalDependencies GADTs GeneralizedNewtypeDeriving MultiParamTypeClasses + PatternGuards Rank2Types ScopedTypeVariables + StandaloneDeriving TypeFamilies TypeOperators TypeSynonymInstances ViewPatterns - -- Required by GHC-6.12: - EmptyDataDecls - PatternGuards