diff --git a/Cargo.toml b/Cargo.toml index c2fb1a0..f706626 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -4,6 +4,7 @@ members = [ "lice", "lice-scope", "lice-macros", + "lice-egraph", ] [workspace.package] diff --git a/lice-egraph/Cargo.toml b/lice-egraph/Cargo.toml new file mode 100644 index 0000000..f4e4af0 --- /dev/null +++ b/lice-egraph/Cargo.toml @@ -0,0 +1,16 @@ +[package] +name = "lice-egraph" +description = "Equality Saturation for MicroHs programs" +authors.workspace = true +version.workspace = true +edition.workspace = true +license.workspace = true + +[dependencies] +lice = { path = "../lice", features = [ "graph" ] } +egg = "0.9.5" +lice-macros = { path = "../lice-macros" } +parse-display = { version = "0.9" } +ordered-float = "4.2.0" +log = "0.4.21" +clap = { verison = "4.5.4", features = [ "derive" ] } diff --git a/lice-egraph/dots/foo.svg b/lice-egraph/dots/foo.svg new file mode 100644 index 0000000..7d209ab --- /dev/null +++ b/lice-egraph/dots/foo.svg @@ -0,0 +1,153 @@ + + + + + + +egraph + + +cluster_0 + + + +cluster_4 + + + +cluster_5 + + + +cluster_2 + + + +cluster_3 + + + + +0.0 + +A + + + +0.1 + +0 + + + +4.0 + +@ + + + +4.0:sw->0.0 + + + + + +3.0 + +I + + + +4.0:se->3.0 + + + + + +4.1 + +4 + + + +5.0 + +@ + + + +2.0 + +IO.return + + + +5.0:sw->2.0 + + + + + +5.0:se->3.0 + + + + + +5.1 + +@ + + + +5.1:sw->4.0 + + + + + +5.1:se->5.1:n + + + + + +5.2 + +5 + + + +5.3 + +6 + + + +2.1 + +2 + + + +3.1 + +0 + + + +3.2 + +1 + + + +3.3 + +3 + + + diff --git a/lice-egraph/dots/main.svg b/lice-egraph/dots/main.svg new file mode 100644 index 0000000..b58463c --- /dev/null +++ b/lice-egraph/dots/main.svg @@ -0,0 +1,10292 @@ + + + + + + +egraph + + +cluster_0 + + + +cluster_378 + + + +cluster_110 + + + +cluster_299 + + + +cluster_31 + + + +cluster_787 + + + +cluster_330 + + + +cluster_172 + + + +cluster_282 + + + +cluster_14 + + + +cluster_124 + + + +cluster_45 + + + +cluster_801 + + + +cluster_76 + + + +cluster_186 + + + +cluster_753 + + + +cluster_107 + + + +cluster_863 + + + +cluster_28 + + + +cluster_138 + + + +cluster_327 + + + +cluster_815 + + + +cluster_90 + + + +cluster_846 + + + +cluster_11 + + + +cluster_121 + + + +cluster_310 + + + +cluster_42 + + + +cluster_231 + + + +cluster_152 + + + +cluster_73 + + + +cluster_293 + + + +cluster_25 + + + +cluster_781 + + + +cluster_135 + + + +cluster_56 + + + +cluster_166 + + + +cluster_733 + + + +cluster_8 + + + +cluster_764 + + + +cluster_39 + + + +cluster_228 + + + +cluster_149 + + + +cluster_180 + + + +cluster_747 + + + +cluster_101 + + + +cluster_22 + + + +cluster_400 + + + +cluster_53 + + + +cluster_242 + + + +cluster_809 + + + +cluster_163 + + + +cluster_304 + + + +cluster_36 + + + +cluster_146 + + + +cluster_713 + + + +cluster_67 + + + +cluster_823 + + + +cluster_98 + + + +cluster_19 + + + +cluster_208 + + + +cluster_775 + + + +cluster_129 + + + +cluster_50 + + + +cluster_239 + + + +cluster_160 + + + +cluster_349 + + + +cluster_727 + + + +cluster_81 + + + +cluster_837 + + + +cluster_2 + + + +cluster_191 + + + +cluster_33 + + + +cluster_222 + + + +cluster_174 + + + +cluster_741 + + + +cluster_284 + + + +cluster_16 + + + +cluster_803 + + + +cluster_157 + + + +cluster_724 + + + +cluster_188 + + + +cluster_755 + + + +cluster_30 + + + +cluster_140 + + + +cluster_61 + + + +cluster_817 + + + +cluster_171 + + + +cluster_92 + + + +cluster_848 + + + +cluster_13 + + + +cluster_879 + + + +cluster_44 + + + +cluster_233 + + + +cluster_154 + + + +cluster_721 + + + +cluster_264 + + + +cluster_831 + + + +cluster_374 + + + +cluster_106 + + + +cluster_295 + + + +cluster_27 + + + +cluster_783 + + + +cluster_137 + + + +cluster_168 + + + +cluster_735 + + + +cluster_89 + + + +cluster_766 + + + +cluster_120 + + + +cluster_151 + + + +cluster_72 + + + +cluster_749 + + + +cluster_859 + + + +cluster_402 + + + +cluster_134 + + + +cluster_244 + + + +cluster_811 + + + +cluster_275 + + + +cluster_763 + + + +cluster_117 + + + +cluster_306 + + + +cluster_794 + + + +cluster_148 + + + +cluster_715 + + + +cluster_69 + + + +cluster_258 + + + +cluster_825 + + + +cluster_856 + + + +cluster_210 + + + +cluster_777 + + + +cluster_241 + + + +cluster_351 + + + +cluster_839 + + + +cluster_4 + + + +cluster_193 + + + +cluster_760 + + + +cluster_114 + + + +cluster_303 + + + +cluster_870 + + + +cluster_224 + + + +cluster_791 + + + +cluster_145 + + + +cluster_66 + + + +cluster_176 + + + +cluster_207 + + + +cluster_884 + + + +cluster_49 + + + +cluster_805 + + + +cluster_159 + + + +cluster_348 + + + +cluster_1 + + + +cluster_190 + + + +cluster_757 + + + +cluster_111 + + + +cluster_300 + + + +cluster_32 + + + +cluster_221 + + + +cluster_709 + + + +cluster_63 + + + +cluster_252 + + + +cluster_819 + + + +cluster_204 + + + +cluster_125 + + + +cluster_314 + + + +cluster_881 + + + +cluster_46 + + + +cluster_723 + + + +cluster_833 + + + +cluster_187 + + + +cluster_376 + + + +cluster_29 + + + +cluster_785 + + + +cluster_249 + + + +cluster_170 + + + +cluster_201 + + + +cluster_122 + + + +cluster_74 + + + +cluster_751 + + + +cluster_105 + + + +cluster_861 + + + +cluster_26 + + + +cluster_136 + + + +cluster_813 + + + +cluster_167 + + + +cluster_88 + + + +cluster_277 + + + +cluster_844 + + + +cluster_9 + + + +cluster_119 + + + +cluster_308 + + + +cluster_796 + + + +cluster_150 + + + +cluster_339 + + + +cluster_717 + + + +cluster_71 + + + +cluster_260 + + + +cluster_827 + + + +cluster_291 + + + +cluster_23 + + + +cluster_779 + + + +cluster_133 + + + +cluster_322 + + + +cluster_432 + + + +cluster_164 + + + +cluster_85 + + + +cluster_274 + + + +cluster_841 + + + +cluster_6 + + + +cluster_195 + + + +cluster_762 + + + +cluster_116 + + + +cluster_305 + + + +cluster_226 + + + +cluster_793 + + + +cluster_147 + + + +cluster_336 + + + +cluster_68 + + + +cluster_178 + + + +cluster_130 + + + +cluster_319 + + + +cluster_886 + + + +cluster_51 + + + +cluster_240 + + + +cluster_807 + + + +cluster_161 + + + +cluster_350 + + + +cluster_728 + + + +cluster_82 + + + +cluster_271 + + + +cluster_3 + + + +cluster_192 + + + +cluster_34 + + + +cluster_790 + + + +cluster_333 + + + +cluster_821 + + + +cluster_175 + + + +cluster_852 + + + +cluster_206 + + + +cluster_395 + + + +cluster_316 + + + +cluster_48 + + + +cluster_725 + + + +cluster_79 + + + + +0.0 + +A + + + +0.1 + +0 + + + +0.2 + +7 + + + +0.3 + +12 + + + +0.4 + +17 + + + +0.5 + +20 + + + +0.6 + +37 + + + +0.7 + +40 + + + +0.8 + +43 + + + +0.9 + +54 + + + +0.10 + +57 + + + +0.11 + +60 + + + +0.12 + +77 + + + +0.13 + +86 + + + +0.14 + +93 + + + +0.15 + +96 + + + +0.16 + +99 + + + +0.17 + +102 + + + +0.18 + +141 + + + +0.19 + +144 + + + +0.20 + +155 + + + +0.21 + +158 + + + +0.22 + +181 + + + +0.23 + +196 + + + +0.24 + +211 + + + +0.25 + +214 + + + +0.26 + +229 + + + +0.27 + +232 + + + +0.28 + +245 + + + +0.29 + +247 + + + +0.30 + +250 + + + +0.31 + +261 + + + +0.32 + +278 + + + +0.33 + +281 + + + +0.34 + +285 + + + +0.35 + +294 + + + +0.36 + +311 + + + +0.37 + +320 + + + +0.38 + +323 + + + +0.39 + +328 + + + +0.40 + +331 + + + +0.41 + +334 + + + +0.42 + +337 + + + +0.43 + +340 + + + +0.44 + +379 + + + +0.45 + +396 + + + +378.0 + +@ + + + +378.0:sw->0.0 + + + + + +159.0 + +@ + + + +378.0:se->159.0 + + + + + +378.1 + +378 + + + +110.0 + +@ + + + +61.0 + +S' + + + +110.0:sw->61.0 + + + + + +44.0 + +B + + + +110.0:se->44.0 + + + + + +110.1 + +110 + + + +110.2 + +184 + + + +110.3 + +199 + + + +110.4 + +217 + + + +299.0 + +@ + + + +45.0 + +C + + + +299.0:sw->45.0 + + + + + +148.0 + +IO.>>= + + + +299.0:se->148.0 + + + + + +299.1 + +299 + + + +31.0 + +@ + + + +30.0 + +36 + + + +31.0:se->30.0 + + + + + +29.0 + +@ + + + +31.0:sw->29.0 + + + + + +31.1 + +31 + + + +787.0 + +@ + + + +14.0 + +IO.stdout + + + +787.0:se->14.0 + + + + + +32.0 + +37 + + + +787.0:sw->32.0 + + + + + +330.0 + +@ + + + +330.0:sw->0.0 + + + + + +330.0:se->44.0 + + + + + +330.1 + +330 + + + +172.0 + +@ + + + +208.0 + +@ + + + +172.0:se->208.0 + + + + + +201.0 + +@ + + + +172.0:sw->201.0 + + + + + +172.1 + +20 + + + +172.2 + +172 + + + +172.3 + +209 + + + +282.0 + +@ + + + +282.0:se->0.0 + + + + + +252.0 + +K2 + + + +282.0:sw->252.0 + + + + + +282.1 + +282 + + + +14.1 + +39 + + + +14.2 + +14 + + + +14.3 + +18 + + + +124.0 + +C'B + + + +124.1 + +124 + + + +124.2 + +128 + + + +124.3 + +263 + + + +124.4 + +268 + + + +45.1 + +45 + + + +45.2 + +70 + + + +45.3 + +115 + + + +45.4 + +297 + + + +45.5 + +346 + + + +45.6 + +356 + + + +45.7 + +364 + + + +45.8 + +370 + + + +45.9 + +383 + + + +45.10 + +389 + + + +801.0 + +@ + + + +801.0:sw->45.0 + + + + + +819.0 + +@ + + + +801.0:se->819.0 + + + + + +801.1 + +@ + + + +166.0 + +@ + + + +801.1:se->166.0 + + + + + +777.0 + +@ + + + +801.1:sw->777.0 + + + + + +76.0 + +@ + + + +76.0:sw->0.0 + + + + + +8.0 + +@ + + + +76.0:se->8.0 + + + + + +76.1 + +76 + + + +186.0 + +@ + + + +233.0 + +U + + + +186.0:sw->233.0 + + + + + +258.0 + +@ + + + +186.0:se->258.0 + + + + + +186.1 + +14 + + + +186.2 + +186 + + + +186.3 + +200 + + + +186.4 + +218 + + + +186.5 + +259 + + + +753.0 + +@ + + + +753.0:se->777.0 + + + + + +348.0 + +@ + + + +753.0:sw->348.0 + + + + + +753.1 + +@ + + + +152.0 + +IO.return + + + +753.1:se->152.0 + + + + + +715.0 + +@ + + + +753.1:sw->715.0 + + + + + +107.0 + +@ + + + +107.0:sw->44.0 + + + + + +106.0 + +@ + + + +107.0:se->106.0 + + + + + +107.1 + +107 + + + +863.0 + +@ + + + +242.0 + +@ + + + +863.0:sw->242.0 + + + + + +160.0 + +@ + + + +863.0:se->160.0 + + + + + +28.0 + +@ + + + +28.0:se->152.0 + + + + + +151.0 + +@ + + + +28.0:sw->151.0 + + + + + +28.1 + +24 + + + +28.2 + +28 + + + +28.3 + +64 + + + +28.4 + +80 + + + +28.5 + +153 + + + +28.6 + +165 + + + +138.0 + +@ + + + +137.0 + +@ + + + +138.0:se->137.0 + + + + + +122.0 + +@ + + + +138.0:sw->122.0 + + + + + +138.1 + +138 + + + +327.0 + +@ + + + +327.0:sw->0.0 + + + + + +190.0 + +@ + + + +327.0:se->190.0 + + + + + +327.1 + +213 + + + +327.2 + +327 + + + +815.0 + +@ + + + +207.0 + +K + + + +815.0:sw->207.0 + + + + + +150.0 + +IO.>> + + + +815.0:se->150.0 + + + + + +815.1 + +@ + + + +400.0 + +@ + + + +815.1:se->400.0 + + + + + +785.0 + +@ + + + +815.1:sw->785.0 + + + + + +90.0 + +ord + + + +90.1 + +28 + + + +90.2 + +29 + + + +90.3 + +90 + + + +90.4 + +94 + + + +90.5 + +97 + + + +846.0 + +@ + + + +846.0:se->166.0 + + + + + +240.0 + +@ + + + +846.0:sw->240.0 + + + + + +846.1 + +@ + + + +846.1:se->258.0 + + + + + +846.1:sw->819.0 + + + + + +11.0 + +@ + + + +11.0:sw->0.0 + + + + + +1.0 + +@ + + + +11.0:se->1.0 + + + + + +11.1 + +11 + + + +121.0 + +@ + + + +120.0 + +@ + + + +121.0:se->120.0 + + + + + +111.0 + +B' + + + +121.0:sw->111.0 + + + + + +121.1 + +121 + + + +310.0 + +@ + + + +310.0:sw->0.0 + + + + + +310.0:se->160.0 + + + + + +310.1 + +310 + + + +42.0 + +@ + + + +42.0:sw->0.0 + + + + + +42.0:se->30.0 + + + + + +42.1 + +42 + + + +231.0 + +@ + + + +231.0:sw->0.0 + + + + + +22.0 + +I + + + +231.0:se->22.0 + + + + + +231.1 + +59 + + + +231.2 + +143 + + + +231.3 + +231 + + + +152.1 + +5 + + + +152.2 + +152 + + + +152.3 + +162 + + + +152.4 + +302 + + + +152.5 + +332 + + + +73.0 + +10 + + + +73.1 + +73 + + + +293.0 + +@ + + + +293.0:sw->0.0 + + + + + +50.0 + +@ + + + +293.0:se->50.0 + + + + + +293.1 + +293 + + + +25.0 + +IO.performIO + + + +25.1 + +34 + + + +25.2 + +25 + + + +25.3 + +55 + + + +781.0 + +@ + + + +755.0 + +@ + + + +781.0:sw->755.0 + + + + + +781.0:se->148.0 + + + + + +135.0 + +@ + + + +134.0 + +@ + + + +135.0:se->134.0 + + + + + +125.0 + +@ + + + +135.0:sw->125.0 + + + + + +135.1 + +135 + + + +56.0 + +@ + + + +56.0:sw->0.0 + + + + + +56.0:se->25.0 + + + + + +56.1 + +56 + + + +146.0 + +@ + + + +166.0:sw->146.0 + + + + + +166.0:se->258.0 + + + + + +166.1 + +@ + + + +166.1:se->28.0 + + + + + +164.0 + +@ + + + +166.1:sw->164.0 + + + + + +166.2 + +@ + + + +166.2:sw->186.0 + + + + + +166.2:se->146.0 + + + + + +166.3 + +@ + + + +833.0 + +@ + + + +166.3:sw->833.0 + + + + + +178.0 + +@ + + + +166.3:se->178.0 + + + + + +166.4 + +@ + + + +733.0 + +@ + + + +166.4:se->733.0 + + + + + +856.0 + +@ + + + +166.4:sw->856.0 + + + + + +166.5 + +166 + + + +733.0:se->28.0 + + + + + +275.0 + +@ + + + +733.0:sw->275.0 + + + + + +733.1 + +@ + + + +733.1:sw->856.0 + + + + + +760.0 + +@ + + + +733.1:se->760.0 + + + + + +69.0 + +@ + + + +8.0:sw->69.0 + + + + + +74.0 + +@ + + + +8.0:se->74.0 + + + + + +8.1 + +32 + + + +8.2 + +8 + + + +8.3 + +75 + + + +764.0 + +@ + + + +764.0:se->28.0 + + + + + +764.0:sw->137.0 + + + + + +764.1 + +@ + + + +791.0 + +@ + + + +764.1:sw->791.0 + + + + + +136.0 + +Z + + + +764.1:se->136.0 + + + + + +39.0 + +@ + + + +39.0:sw->0.0 + + + + + +39.0:se->32.0 + + + + + +39.1 + +39 + + + +228.0 + +@ + + + +228.0:sw->0.0 + + + + + +168.0 + +@ + + + +228.0:se->168.0 + + + + + +228.1 + +228 + + + +149.0 + +@ + + + +747.0 + +@ + + + +149.0:se->747.0 + + + + + +46.0 + +@ + + + +149.0:sw->46.0 + + + + + +149.1 + +@ + + + +149.1:se->148.0 + + + + + +147.0 + +@ + + + +149.1:sw->147.0 + + + + + +149.2 + +149 + + + +180.0 + +@ + + + +180.0:sw->0.0 + + + + + +180.0:se->146.0 + + + + + +180.1 + +180 + + + +747.0:sw->45.0 + + + + + +747.0:se->781.0 + + + + + +747.1 + +@ + + + +713.0 + +@ + + + +747.1:sw->713.0 + + + + + +747.1:se->148.0 + + + + + +101.0 + +@ + + + +101.0:sw->0.0 + + + + + +88.0 + +27 + + + +101.0:se->88.0 + + + + + +101.1 + +101 + + + +22.1 + +17 + + + +22.2 + +25 + + + +22.3 + +33 + + + +22.4 + +22 + + + +22.5 + +58 + + + +22.6 + +118 + + + +22.7 + +142 + + + +22.8 + +225 + + + +22.9 + +230 + + + +400.0:se->207.0 + + + + + +400.0:sw->252.0 + + + + + +400.1 + +400 + + + +53.0 + +@ + + + +53.0:sw->0.0 + + + + + +27.0 + +@ + + + +53.0:se->27.0 + + + + + +53.1 + +53 + + + +241.0 + +@ + + + +242.0:se->241.0 + + + + + +242.0:sw->136.0 + + + + + +242.1 + +242 + + + +809.0 + +@ + + + +809.0:sw->764.0 + + + + + +749.0 + +@ + + + +809.0:se->749.0 + + + + + +163.0 + +@ + + + +163.0:se->152.0 + + + + + +161.0 + +@ + + + +163.0:sw->161.0 + + + + + +163.1 + +@ + + + +163.1:se->753.0 + + + + + +349.0 + +@ + + + +163.1:sw->349.0 + + + + + +163.2 + +163 + + + +304.0 + +@ + + + +304.0:sw->160.0 + + + + + +304.0:se->207.0 + + + + + +304.1 + +@ + + + +304.1:se->160.0 + + + + + +304.1:sw->190.0 + + + + + +304.2 + +@ + + + +304.2:se->146.0 + + + + + +193.0 + +@ + + + +304.2:sw->193.0 + + + + + +304.3 + +@ + + + +303.0 + +@ + + + +304.3:se->303.0 + + + + + +300.0 + +@ + + + +304.3:sw->300.0 + + + + + +304.4 + +@ + + + +308.0 + +@ + + + +304.4:se->308.0 + + + + + +796.0 + +@ + + + +304.4:sw->796.0 + + + + + +304.5 + +304 + + + +36.0 + +@ + + + +36.0:sw->0.0 + + + + + +13.0 + +@ + + + +36.0:se->13.0 + + + + + +36.1 + +36 + + + +146.0:se->178.0 + + + + + +175.0 + +@ + + + +146.0:sw->175.0 + + + + + +146.1 + +22 + + + +146.2 + +146 + + + +146.3 + +169 + + + +146.4 + +173 + + + +146.5 + +177 + + + +146.6 + +179 + + + +713.0:se->755.0 + + + + + +713.0:sw->46.0 + + + + + +713.1 + +@ + + + +713.1:se->146.0 + + + + + +374.0 + +@ + + + +713.1:sw->374.0 + + + + + +67.0 + +@ + + + +67.0:sw->61.0 + + + + + +66.0 + +@ + + + +67.0:se->66.0 + + + + + +67.1 + +67 + + + +823.0 + +@ + + + +823.0:sw->801.0 + + + + + +170.0 + +@ + + + +823.0:se->170.0 + + + + + +98.0 + +@ + + + +98.0:sw->0.0 + + + + + +98.0:se->90.0 + + + + + +98.1 + +95 + + + +98.2 + +98 + + + +19.0 + +@ + + + +19.0:sw->0.0 + + + + + +19.0:se->14.0 + + + + + +19.1 + +19 + + + +208.0:se->207.0 + + + + + +206.0 + +@ + + + +208.0:sw->206.0 + + + + + +208.1 + +208 + + + +775.0 + +@ + + + +775.0:se->801.0 + + + + + +775.0:sw->46.0 + + + + + +775.1 + +@ + + + +775.1:sw->753.0 + + + + + +775.1:se->166.0 + + + + + +129.0 + +@ + + + +129.0:se->124.0 + + + + + +129.0:sw->44.0 + + + + + +129.1 + +129 + + + +50.0:sw->233.0 + + + + + +291.0 + +@ + + + +50.0:se->291.0 + + + + + +50.1 + +11 + + + +50.2 + +50 + + + +50.3 + +132 + + + +50.4 + +265 + + + +50.5 + +270 + + + +50.6 + +292 + + + +239.0 + +@ + + + +239.0:se->207.0 + + + + + +239.0:sw->136.0 + + + + + +239.1 + +@ + + + +239.1:se->146.0 + + + + + +239.1:sw->291.0 + + + + + +239.2 + +239 + + + +239.3 + +256 + + + +239.4 + +290 + + + +160.0:se->242.0 + + + + + +160.0:sw->146.0 + + + + + +160.1 + +@ + + + +160.1:se->146.0 + + + + + +192.0 + +@ + + + +160.1:sw->192.0 + + + + + +160.2 + +@ + + + +160.2:se->308.0 + + + + + +305.0 + +@ + + + +160.2:sw->305.0 + + + + + +160.3 + +@ + + + +831.0 + +@ + + + +160.3:sw->831.0 + + + + + +160.3:se->178.0 + + + + + +160.4 + +10 + + + +160.5 + +160 + + + +160.6 + +307 + + + +160.7 + +309 + + + +349.0:sw->44.0 + + + + + +349.0:se->348.0 + + + + + +349.1 + +349 + + + +349.2 + +359 + + + +349.3 + +367 + + + +349.4 + +386 + + + +727.0 + +@ + + + +727.0:se->146.0 + + + + + +187.0 + +@ + + + +727.0:sw->187.0 + + + + + +81.0 + +@ + + + +81.0:se->28.0 + + + + + +79.0 + +@ + + + +81.0:sw->79.0 + + + + + +81.1 + +@ + + + +81.1:sw->106.0 + + + + + +709.0 + +@ + + + +81.1:se->709.0 + + + + + +81.2 + +81 + + + +837.0 + +@ + + + +837.0:sw->400.0 + + + + + +837.0:se->146.0 + + + + + +2.0 + +fromUTF8 + + + +2.1 + +2 + + + +191.0 + +@ + + + +191.0:sw->44.0 + + + + + +191.0:se->190.0 + + + + + +191.1 + +191 + + + +33.0 + +@ + + + +33.0:sw->31.0 + + + + + +33.0:se->32.0 + + + + + +33.1 + +@ + + + +33.1:se->30.0 + + + + + +757.0 + +@ + + + +33.1:sw->757.0 + + + + + +33.2 + +33 + + + +222.0 + +@ + + + +221.0 + +@ + + + +222.0:se->221.0 + + + + + +48.0 + +C' + + + +222.0:sw->48.0 + + + + + +222.1 + +222 + + + +174.0 + +@ + + + +174.0:sw->172.0 + + + + + +174.0:se->146.0 + + + + + +174.1 + +@ + + + +721.0 + +@ + + + +174.1:se->721.0 + + + + + +870.0 + +@ + + + +174.1:sw->870.0 + + + + + +174.2 + +174 + + + +741.0 + +@ + + + +741.0:se->160.0 + + + + + +145.0 + +@ + + + +741.0:sw->145.0 + + + + + +741.1 + +@ + + + +741.1:sw->348.0 + + + + + +779.0 + +@ + + + +741.1:se->779.0 + + + + + +284.0 + +@ + + + +284.0:sw->0.0 + + + + + +116.0 + +@ + + + +284.0:se->116.0 + + + + + +284.1 + +284 + + + +16.0 + +@ + + + +16.0:sw->0.0 + + + + + +9.0 + +@ + + + +16.0:se->9.0 + + + + + +16.1 + +16 + + + +803.0 + +@ + + + +803.0:sw->45.0 + + + + + +821.0 + +@ + + + +803.0:se->821.0 + + + + + +803.1 + +@ + + + +803.1:se->152.0 + + + + + +803.1:sw->779.0 + + + + + +157.0 + +@ + + + +157.0:sw->0.0 + + + + + +157.0:se->150.0 + + + + + +157.1 + +157 + + + +724.0 + +@ + + + +724.0:sw->66.0 + + + + + +723.0 + +@ + + + +724.0:se->723.0 + + + + + +188.0 + +@ + + + +188.0:sw->110.0 + + + + + +188.0:se->187.0 + + + + + +188.1 + +188 + + + +755.0:se->146.0 + + + + + +295.0 + +P + + + +755.0:sw->295.0 + + + + + +30.1 + +add_utf8 + + + +30.2 + +30 + + + +30.3 + +41 + + + +140.0 + +@ + + + +140.0:sw->0.0 + + + + + +140.0:se->79.0 + + + + + +140.1 + +140 + + + +61.1 + +61 + + + +61.2 + +108 + + + +61.3 + +182 + + + +61.4 + +197 + + + +61.5 + +215 + + + +61.6 + +262 + + + +61.7 + +267 + + + +817.0 + +@ + + + +817.0:se->304.0 + + + + + +817.0:sw->44.0 + + + + + +171.0 + +@ + + + +171.0:sw->46.0 + + + + + +807.0 + +@ + + + +171.0:se->807.0 + + + + + +171.1 + +@ + + + +171.1:se->170.0 + + + + + +167.0 + +@ + + + +171.1:sw->167.0 + + + + + +171.2 + +171 + + + +92.0 + +@ + + + +92.0:sw->0.0 + + + + + +71.0 + +@ + + + +92.0:se->71.0 + + + + + +92.1 + +92 + + + +848.0 + +@ + + + +766.0 + +@ + + + +848.0:se->766.0 + + + + + +848.0:sw->150.0 + + + + + +23.0 + +@ + + + +13.0:sw->23.0 + + + + + +34.0 + +@ + + + +13.0:se->34.0 + + + + + +13.1 + +38 + + + +13.2 + +13 + + + +13.3 + +35 + + + +879.0 + +@ + + + +879.0:sw->303.0 + + + + + +879.0:se->207.0 + + + + + +44.1 + +6 + + + +44.2 + +21 + + + +44.3 + +24 + + + +44.4 + +44 + + + +44.5 + +47 + + + +44.6 + +78 + + + +44.7 + +103 + + + +44.8 + +104 + + + +44.9 + +109 + + + +44.10 + +112 + + + +44.11 + +126 + + + +44.12 + +127 + + + +44.13 + +183 + + + +44.14 + +189 + + + +44.15 + +198 + + + +44.16 + +216 + + + +44.17 + +296 + + + +44.18 + +301 + + + +44.19 + +313 + + + +44.20 + +329 + + + +44.21 + +341 + + + +44.22 + +342 + + + +44.23 + +343 + + + +44.24 + +344 + + + +44.25 + +345 + + + +44.26 + +352 + + + +44.27 + +353 + + + +44.28 + +354 + + + +44.29 + +355 + + + +44.30 + +361 + + + +44.31 + +362 + + + +44.32 + +363 + + + +44.33 + +368 + + + +44.34 + +369 + + + +44.35 + +380 + + + +44.36 + +381 + + + +44.37 + +382 + + + +44.38 + +387 + + + +44.39 + +388 + + + +233.1 + +233 + + + +233.2 + +246 + + + +233.3 + +251 + + + +233.4 + +279 + + + +233.5 + +286 + + + +233.6 + +324 + + + +233.7 + +397 + + + +154.0 + +@ + + + +154.0:sw->0.0 + + + + + +154.0:se->28.0 + + + + + +154.1 + +154 + + + +721.0:se->146.0 + + + + + +721.0:sw->208.0 + + + + + +721.1 + +@ + + + +721.1:sw->299.0 + + + + + +721.1:se->879.0 + + + + + +721.2 + +@ + + + +721.2:sw->304.0 + + + + + +721.2:se->207.0 + + + + + +264.0 + +@ + + + +264.0:se->124.0 + + + + + +264.0:sw->61.0 + + + + + +264.1 + +264 + + + +264.2 + +269 + + + +831.0:se->160.0 + + + + + +831.0:sw->207.0 + + + + + +831.1 + +@ + + + +831.1:se->242.0 + + + + + +825.0 + +@ + + + +831.1:sw->825.0 + + + + + +831.2 + +@ + + + +831.2:se->174.0 + + + + + +839.0 + +@ + + + +831.2:sw->839.0 + + + + + +374.0:se->295.0 + + + + + +374.0:sw->348.0 + + + + + +374.1 + +374 + + + +374.2 + +393 + + + +106.0:sw->44.0 + + + + + +105.0 + +Y + + + +106.0:se->105.0 + + + + + +106.1 + +106 + + + +295.1 + +3 + + + +295.2 + +113 + + + +295.3 + +295 + + + +295.4 + +338 + + + +295.5 + +373 + + + +295.6 + +392 + + + +27.0:sw->46.0 + + + + + +51.0 + +@ + + + +27.0:se->51.0 + + + + + +27.1 + +35 + + + +27.2 + +27 + + + +27.3 + +52 + + + +783.0 + +@ + + + +783.0:se->749.0 + + + + + +783.0:sw->709.0 + + + + + +783.1 + +@ + + + +783.1:se->809.0 + + + + + +762.0 + +@ + + + +783.1:sw->762.0 + + + + + +137.0:sw->135.0 + + + + + +137.0:se->136.0 + + + + + +137.1 + +137 + + + +168.0:sw->201.0 + + + + + +226.0 + +@ + + + +168.0:se->226.0 + + + + + +168.1 + +18 + + + +168.2 + +168 + + + +168.3 + +227 + + + +735.0 + +@ + + + +735.0:se->146.0 + + + + + +735.0:sw->226.0 + + + + + +735.1 + +@ + + + +735.1:sw->299.0 + + + + + +886.0 + +@ + + + +735.1:se->886.0 + + + + + +735.2 + +@ + + + +735.2:sw->304.0 + + + + + +884.0 + +@ + + + +735.2:se->884.0 + + + + + +735.3 + +@ + + + +735.3:se->22.0 + + + + + +735.3:sw->308.0 + + + + + +89.0 + +@ + + + +89.0:se->88.0 + + + + + +89.0:sw->48.0 + + + + + +89.1 + +89 + + + +4.0 + +@ + + + +766.0:se->4.0 + + + + + +766.0:sw->723.0 + + + + + +114.0 + +@ + + + +120.0:sw->114.0 + + + + + +119.0 + +@ + + + +120.0:se->119.0 + + + + + +120.1 + +120 + + + +151.0:sw->45.0 + + + + + +151.0:se->785.0 + + + + + +151.1 + +@ + + + +151.1:sw->149.0 + + + + + +151.1:se->150.0 + + + + + +151.2 + +151 + + + +72.0 + +@ + + + +72.0:sw->45.0 + + + + + +72.0:se->71.0 + + + + + +72.1 + +72 + + + +749.0:se->9.0 + + + + + +749.0:sw->71.0 + + + + + +859.0 + +@ + + + +859.0:se->787.0 + + + + + +859.0:sw->148.0 + + + + + +402.0 + +@ + + + +402.0:sw->0.0 + + + + + +63.0 + +@ + + + +402.0:se->63.0 + + + + + +402.1 + +402 + + + +133.0 + +@ + + + +134.0:se->133.0 + + + + + +130.0 + +@ + + + +134.0:sw->130.0 + + + + + +134.1 + +134 + + + +244.0 + +@ + + + +244.0:sw->0.0 + + + + + +244.0:se->192.0 + + + + + +244.1 + +244 + + + +811.0 + +@ + + + +811.0:se->28.0 + + + + + +811.0:sw->133.0 + + + + + +274.0 + +@ + + + +275.0:se->274.0 + + + + + +271.0 + +@ + + + +275.0:sw->271.0 + + + + + +275.1 + +275 + + + +763.0 + +@ + + + +763.0:sw->44.0 + + + + + +763.0:se->762.0 + + + + + +117.0 + +@ + + + +117.0:sw->45.0 + + + + + +117.0:se->116.0 + + + + + +117.1 + +117 + + + +306.0 + +@ + + + +306.0:se->207.0 + + + + + +316.0 + +@ + + + +306.0:sw->316.0 + + + + + +306.1 + +9 + + + +306.2 + +306 + + + +306.3 + +318 + + + +794.0 + +@ + + + +794.0:sw->88.0 + + + + + +793.0 + +@ + + + +794.0:se->793.0 + + + + + +148.1 + +@ + + + +148.1:sw->28.0 + + + + + +148.1:se->291.0 + + + + + +148.2 + +@ + + + +148.2:se->28.0 + + + + + +148.2:sw->50.0 + + + + + +148.3 + +@ + + + +148.3:se->152.0 + + + + + +813.0 + +@ + + + +148.3:sw->813.0 + + + + + +148.4 + +4 + + + +148.5 + +148 + + + +148.6 + +298 + + + +148.7 + +335 + + + +715.0:sw->349.0 + + + + + +715.0:se->741.0 + + + + + +715.1 + +@ + + + +715.1:se->160.0 + + + + + +376.0 + +@ + + + +715.1:sw->376.0 + + + + + +69.0:sw->67.0 + + + + + +68.0 + +@ + + + +69.0:se->68.0 + + + + + +69.1 + +69 + + + +258.0:sw->252.0 + + + + + +258.0:se->240.0 + + + + + +258.1 + +258 + + + +825.0:se->174.0 + + + + + +825.0:sw->807.0 + + + + + +856.0:sw->124.0 + + + + + +856.0:se->148.0 + + + + + +210.0 + +@ + + + +210.0:sw->0.0 + + + + + +210.0:se->172.0 + + + + + +210.1 + +210 + + + +777.0:se->803.0 + + + + + +777.0:sw->46.0 + + + + + +777.1 + +@ + + + +777.1:se->152.0 + + + + + +777.1:sw->741.0 + + + + + +241.0:sw->136.0 + + + + + +241.0:se->240.0 + + + + + +241.1 + +241 + + + +351.0 + +@ + + + +351.0:sw->44.0 + + + + + +350.0 + +@ + + + +351.0:se->350.0 + + + + + +351.1 + +351 + + + +839.0:sw->239.0 + + + + + +839.0:se->160.0 + + + + + +839.1 + +@ + + + +839.1:se->242.0 + + + + + +839.1:sw->823.0 + + + + + +839.2 + +@ + + + +839.2:se->170.0 + + + + + +844.0 + +@ + + + +839.2:sw->844.0 + + + + + +4.0:sw->2.0 + + + + + +3.0 + +hello, world +& + + + +4.0:se->3.0 + + + + + +4.1 + +4 + + + +193.0:sw->191.0 + + + + + +193.0:se->192.0 + + + + + +193.1 + +193 + + + +760.0:se->28.0 + + + + + +760.0:sw->274.0 + + + + + +114.0:sw->44.0 + + + + + +114.0:se->295.0 + + + + + +114.1 + +114 + + + +303.0:se->152.0 + + + + + +303.0:sw->44.0 + + + + + +303.1 + +303 + + + +870.0:se->166.0 + + + + + +870.0:sw->44.0 + + + + + +224.0 + +@ + + + +224.0:sw->222.0 + + + + + +224.0:se->192.0 + + + + + +224.1 + +224 + + + +791.0:sw->124.0 + + + + + +790.0 + +@ + + + +791.0:se->790.0 + + + + + +145.0:sw->349.0 + + + + + +145.0:se->374.0 + + + + + +145.1 + +1 + + + +145.2 + +145 + + + +145.3 + +375 + + + +145.4 + +394 + + + +66.0:se->150.0 + + + + + +66.0:sw->48.0 + + + + + +66.1 + +66 + + + +176.0 + +@ + + + +176.0:sw->188.0 + + + + + +176.0:se->193.0 + + + + + +176.1 + +21 + + + +176.2 + +176 + + + +176.3 + +194 + + + +207.1 + +@ + + + +207.1:sw->781.0 + + + + + +207.1:se->400.0 + + + + + +207.2 + +@ + + + +207.2:sw->837.0 + + + + + +207.2:se->148.0 + + + + + +207.3 + +8 + + + +207.4 + +207 + + + +207.5 + +238 + + + +207.6 + +255 + + + +207.7 + +287 + + + +207.8 + +289 + + + +207.9 + +317 + + + +207.10 + +321 + + + +207.11 + +325 + + + +207.12 + +399 + + + +884.0:se->22.0 + + + + + +884.0:sw->207.0 + + + + + +49.0 + +@ + + + +49.0:sw->44.0 + + + + + +49.0:se->48.0 + + + + + +49.1 + +49 + + + +805.0 + +@ + + + +805.0:se->160.0 + + + + + +805.0:sw->295.0 + + + + + +159.0:sw->351.0 + + + + + +159.0:se->376.0 + + + + + +159.1 + +2 + + + +159.2 + +159 + + + +159.3 + +377 + + + +348.0:sw->44.0 + + + + + +348.0:se->46.0 + + + + + +348.1 + +348 + + + +348.2 + +358 + + + +348.3 + +366 + + + +348.4 + +372 + + + +348.5 + +385 + + + +348.6 + +391 + + + +1.0:sw->8.0 + + + + + +1.0:se->9.0 + + + + + +1.1 + +@ + + + +1.1:sw->724.0 + + + + + +725.0 + +@ + + + +1.1:se->725.0 + + + + + +1.2 + +41 + + + +1.3 + +1 + + + +1.4 + +10 + + + +190.0:sw->233.0 + + + + + +190.0:se->207.0 + + + + + +190.1 + +7 + + + +190.2 + +19 + + + +190.3 + +190 + + + +190.4 + +203 + + + +190.5 + +212 + + + +190.6 + +315 + + + +190.7 + +326 + + + +757.0:se->32.0 + + + + + +717.0 + +@ + + + +757.0:sw->717.0 + + + + + +111.1 + +111 + + + +111.2 + +131 + + + +111.3 + +185 + + + +111.4 + +272 + + + +300.0:se->299.0 + + + + + +300.0:sw->44.0 + + + + + +300.1 + +300 + + + +32.1 + +add_FILE + + + +32.2 + +32 + + + +32.3 + +38 + + + +221.0:se->0.0 + + + + + +221.0:sw->233.0 + + + + + +221.1 + +15 + + + +221.2 + +221 + + + +221.3 + +248 + + + +709.0:se->28.0 + + + + + +709.0:sw->138.0 + + + + + +709.1 + +@ + + + +709.1:se->764.0 + + + + + +709.1:sw->763.0 + + + + + +63.0:se->400.0 + + + + + +63.0:sw->233.0 + + + + + +63.1 + +0 + + + +63.2 + +63 + + + +63.3 + +401 + + + +252.1 + +252 + + + +252.2 + +280 + + + +252.3 + +398 + + + +819.0:se->166.0 + + + + + +819.0:sw->803.0 + + + + + +204.0 + +@ + + + +204.0:se->190.0 + + + + + +204.0:sw->48.0 + + + + + +204.1 + +204 + + + +125.0:se->124.0 + + + + + +125.0:sw->48.0 + + + + + +125.1 + +125 + + + +314.0 + +@ + + + +314.0:se->44.0 + + + + + +314.0:sw->48.0 + + + + + +314.1 + +314 + + + +881.0 + +@ + + + +881.0:sw->0.0 + + + + + +881.0:se->304.0 + + + + + +46.0:se->45.0 + + + + + +46.0:sw->44.0 + + + + + +46.1 + +46 + + + +46.2 + +347 + + + +46.3 + +357 + + + +46.4 + +365 + + + +46.5 + +371 + + + +46.6 + +384 + + + +46.7 + +390 + + + +723.0:se->9.0 + + + + + +723.0:sw->68.0 + + + + + +723.1 + +@ + + + +723.1:sw->81.0 + + + + + +723.1:se->749.0 + + + + + +723.2 + +@ + + + +723.2:se->783.0 + + + + + +723.2:sw->105.0 + + + + + +833.0:se->166.0 + + + + + +833.0:sw->207.0 + + + + + +833.1 + +@ + + + +833.1:se->258.0 + + + + + +833.1:sw->825.0 + + + + + +833.2 + +@ + + + +833.2:se->174.0 + + + + + +841.0 + +@ + + + +833.2:sw->841.0 + + + + + +187.0:se->186.0 + + + + + +187.0:sw->111.0 + + + + + +187.1 + +187 + + + +376.0:se->145.0 + + + + + +376.0:sw->350.0 + + + + + +376.1 + +376 + + + +29.0:se->28.0 + + + + + +29.0:sw->27.0 + + + + + +29.1 + +@ + + + +29.1:sw->45.0 + + + + + +29.1:se->717.0 + + + + + +29.2 + +29 + + + +785.0:sw->747.0 + + + + + +785.0:se->150.0 + + + + + +249.0 + +@ + + + +249.0:sw->0.0 + + + + + +249.0:se->221.0 + + + + + +249.1 + +249 + + + +170.0:se->146.0 + + + + + +170.0:sw->168.0 + + + + + +170.1 + +@ + + + +170.1:se->735.0 + + + + + +170.1:sw->870.0 + + + + + +170.2 + +170 + + + +201.0:sw->110.0 + + + + + +201.0:se->186.0 + + + + + +201.1 + +201 + + + +201.2 + +219 + + + +122.0:sw->110.0 + + + + + +122.0:se->121.0 + + + + + +122.1 + +122 + + + +74.0:se->73.0 + + + + + +74.0:sw->72.0 + + + + + +74.1 + +74 + + + +751.0 + +@ + + + +751.0:se->14.0 + + + + + +751.0:sw->33.0 + + + + + +751.1 + +@ + + + +751.1:se->30.0 + + + + + +751.1:sw->859.0 + + + + + +105.1 + +105 + + + +861.0 + +@ + + + +861.0:se->160.0 + + + + + +861.0:sw->258.0 + + + + + +26.0 + +@ + + + +26.0:se->25.0 + + + + + +26.0:sw->44.0 + + + + + +26.1 + +26 + + + +136.1 + +136 + + + +136.2 + +234 + + + +136.3 + +235 + + + +136.4 + +236 + + + +136.5 + +237 + + + +136.6 + +253 + + + +136.7 + +254 + + + +136.8 + +288 + + + +813.0:se->148.0 + + + + + +813.0:sw->207.0 + + + + + +813.1 + +@ + + + +813.1:sw->785.0 + + + + + +813.1:se->291.0 + + + + + +813.2 + +@ + + + +813.2:se->150.0 + + + + + +827.0 + +@ + + + +813.2:sw->827.0 + + + + + +167.0:se->166.0 + + + + + +167.0:sw->163.0 + + + + + +167.1 + +@ + + + +167.1:se->775.0 + + + + + +167.1:sw->348.0 + + + + + +167.2 + +167 + + + +88.1 + +putb + + + +88.2 + +88 + + + +88.3 + +100 + + + +277.0 + +@ + + + +277.0:sw->0.0 + + + + + +277.0:se->164.0 + + + + + +277.1 + +277 + + + +844.0:se->160.0 + + + + + +844.0:sw->240.0 + + + + + +844.1 + +@ + + + +844.1:se->242.0 + + + + + +844.1:sw->819.0 + + + + + +844.2 + +@ + + + +844.2:se->166.0 + + + + + +852.0 + +@ + + + +844.2:sw->852.0 + + + + + +9.0:se->14.0 + + + + + +9.0:sw->13.0 + + + + + +9.1 + +@ + + + +9.1:sw->22.0 + + + + + +9.1:se->9.1:n + + + + + +9.2 + +@ + + + +9.2:sw->25.0 + + + + + +9.2:se->751.0 + + + + + +9.3 + +@ + + + +9.3:se->14.0 + + + + + +9.3:sw->34.0 + + + + + +9.4 + +40 + + + +9.5 + +9 + + + +9.6 + +15 + + + +119.0:se->22.0 + + + + + +119.0:sw->117.0 + + + + + +119.1 + +119 + + + +308.0:se->0.0 + + + + + +308.0:sw->160.0 + + + + + +308.1 + +@ + + + +308.1:se->160.0 + + + + + +308.1:sw->221.0 + + + + + +308.2 + +@ + + + +308.2:se->160.0 + + + + + +308.2:sw->306.0 + + + + + +308.3 + +@ + + + +308.3:sw->817.0 + + + + + +308.3:se->207.0 + + + + + +308.4 + +@ + + + +308.4:sw->881.0 + + + + + +308.4:se->308.4:n + + + + + +308.5 + +308 + + + +796.0:se->304.0 + + + + + +796.0:sw->207.0 + + + + + +150.1 + +@ + + + +150.1:sw->28.0 + + + + + +150.1:se->400.0 + + + + + +150.2 + +@ + + + +150.2:se->28.0 + + + + + +150.2:sw->63.0 + + + + + +150.3 + +@ + + + +150.3:sw->815.0 + + + + + +150.3:se->152.0 + + + + + +150.4 + +23 + + + +150.5 + +65 + + + +150.6 + +150 + + + +150.7 + +156 + + + +339.0 + +@ + + + +339.0:sw->0.0 + + + + + +339.0:se->295.0 + + + + + +339.1 + +339 + + + +717.0:se->148.0 + + + + + +717.0:sw->48.0 + + + + + +717.1 + +@ + + + +717.1:se->28.0 + + + + + +717.1:sw->51.0 + + + + + +71.0:se->90.0 + + + + + +71.0:sw->89.0 + + + + + +71.1 + +30 + + + +71.2 + +71 + + + +71.3 + +83 + + + +71.4 + +91 + + + +260.0 + +@ + + + +260.0:sw->0.0 + + + + + +260.0:se->186.0 + + + + + +260.1 + +260 + + + +827.0:sw->239.0 + + + + + +827.0:se->148.0 + + + + + +827.1 + +@ + + + +827.1:sw->781.0 + + + + + +827.1:se->291.0 + + + + + +291.0:se->239.0 + + + + + +291.0:sw->207.0 + + + + + +291.1 + +291 + + + +23.0:se->22.0 + + + + + +23.0:sw->44.0 + + + + + +23.1 + +23 + + + +779.0:se->805.0 + + + + + +779.0:sw->46.0 + + + + + +779.1 + +@ + + + +779.1:se->160.0 + + + + + +779.1:sw->374.0 + + + + + +133.0:se->50.0 + + + + + +133.0:sw->111.0 + + + + + +133.1 + +133 + + + +322.0 + +@ + + + +322.0:sw->0.0 + + + + + +322.0:se->207.0 + + + + + +322.1 + +322 + + + +432.0 + +@ + + + +432.0:se->4.0 + + + + + +432.0:sw->1.0 + + + + + +432.1 + +@ + + + +432.1:se->432.1:n + + + + + +6.0 + +@ + + + +432.1:sw->6.0 + + + + + +432.2 + +@ + + + +432.2:sw->11.0 + + + + + +432.2:se->432.2:n + + + + + +432.3 + +@ + + + +432.3:sw->16.0 + + + + + +432.3:se->432.3:n + + + + + +432.4 + +@ + + + +432.4:sw->19.0 + + + + + +432.4:se->432.4:n + + + + + +432.5 + +@ + + + +432.5:sw->36.0 + + + + + +432.5:se->432.5:n + + + + + +432.6 + +@ + + + +432.6:sw->39.0 + + + + + +432.6:se->432.6:n + + + + + +432.7 + +@ + + + +432.7:sw->42.0 + + + + + +432.7:se->432.7:n + + + + + +432.8 + +@ + + + +432.8:sw->53.0 + + + + + +432.8:se->432.8:n + + + + + +432.9 + +@ + + + +432.9:sw->56.0 + + + + + +432.9:se->432.9:n + + + + + +432.10 + +@ + + + +432.10:sw->76.0 + + + + + +432.10:se->432.10:n + + + + + +432.11 + +@ + + + +432.11:se->432.11:n + + + + + +85.0 + +@ + + + +432.11:sw->85.0 + + + + + +432.12 + +@ + + + +432.12:sw->92.0 + + + + + +432.12:se->432.12:n + + + + + +432.13 + +@ + + + +432.13:sw->98.0 + + + + + +432.13:se->432.13:n + + + + + +432.14 + +@ + + + +432.14:sw->101.0 + + + + + +432.14:se->432.14:n + + + + + +432.15 + +@ + + + +432.15:sw->140.0 + + + + + +432.15:se->432.15:n + + + + + +432.16 + +@ + + + +432.16:sw->154.0 + + + + + +432.16:se->432.16:n + + + + + +432.17 + +@ + + + +432.17:sw->157.0 + + + + + +432.17:se->432.17:n + + + + + +432.18 + +@ + + + +432.18:sw->180.0 + + + + + +432.18:se->432.18:n + + + + + +432.19 + +@ + + + +432.19:se->432.19:n + + + + + +195.0 + +@ + + + +432.19:sw->195.0 + + + + + +432.20 + +@ + + + +432.20:sw->210.0 + + + + + +432.20:se->432.20:n + + + + + +432.21 + +@ + + + +432.21:sw->228.0 + + + + + +432.21:se->432.21:n + + + + + +432.22 + +@ + + + +432.22:sw->231.0 + + + + + +432.22:se->432.22:n + + + + + +432.23 + +@ + + + +432.23:sw->244.0 + + + + + +432.23:se->432.23:n + + + + + +432.24 + +@ + + + +432.24:sw->249.0 + + + + + +432.24:se->432.24:n + + + + + +432.25 + +@ + + + +432.25:sw->260.0 + + + + + +432.25:se->432.25:n + + + + + +432.26 + +@ + + + +432.26:sw->277.0 + + + + + +432.26:se->432.26:n + + + + + +432.27 + +@ + + + +432.27:sw->284.0 + + + + + +432.27:se->432.27:n + + + + + +432.28 + +@ + + + +432.28:sw->293.0 + + + + + +432.28:se->432.28:n + + + + + +432.29 + +@ + + + +432.29:sw->310.0 + + + + + +432.29:se->432.29:n + + + + + +432.30 + +@ + + + +432.30:se->432.30:n + + + + + +319.0 + +@ + + + +432.30:sw->319.0 + + + + + +432.31 + +@ + + + +432.31:sw->322.0 + + + + + +432.31:se->432.31:n + + + + + +432.32 + +@ + + + +432.32:sw->327.0 + + + + + +432.32:se->432.32:n + + + + + +432.33 + +@ + + + +432.33:sw->330.0 + + + + + +432.33:se->432.33:n + + + + + +432.34 + +@ + + + +432.34:se->432.34:n + + + + + +333.0 + +@ + + + +432.34:sw->333.0 + + + + + +432.35 + +@ + + + +432.35:se->432.35:n + + + + + +336.0 + +@ + + + +432.35:sw->336.0 + + + + + +432.36 + +@ + + + +432.36:sw->339.0 + + + + + +432.36:se->432.36:n + + + + + +432.37 + +@ + + + +432.37:sw->378.0 + + + + + +432.37:se->432.37:n + + + + + +432.38 + +@ + + + +432.38:se->432.38:n + + + + + +395.0 + +@ + + + +432.38:sw->395.0 + + + + + +432.39 + +@ + + + +432.39:sw->402.0 + + + + + +432.39:se->432.39:n + + + + + +432.40 + +@ + + + +432.40:sw->848.0 + + + + + +432.40:se->725.0 + + + + + +432.41 + +42 + + + +432.42 + +5 + + + +432.43 + +403 + + + +432.44 + +404 + + + +432.45 + +405 + + + +432.46 + +406 + + + +432.47 + +407 + + + +432.48 + +408 + + + +432.49 + +409 + + + +432.50 + +410 + + + +432.51 + +411 + + + +432.52 + +412 + + + +432.53 + +413 + + + +432.54 + +414 + + + +432.55 + +415 + + + +432.56 + +416 + + + +432.57 + +417 + + + +432.58 + +418 + + + +432.59 + +419 + + + +432.60 + +420 + + + +432.61 + +421 + + + +432.62 + +422 + + + +432.63 + +423 + + + +432.64 + +424 + + + +432.65 + +425 + + + +432.66 + +426 + + + +432.67 + +427 + + + +432.68 + +428 + + + +432.69 + +429 + + + +432.70 + +430 + + + +432.71 + +431 + + + +432.72 + +432 + + + +432.73 + +433 + + + +432.74 + +434 + + + +432.75 + +435 + + + +432.76 + +436 + + + +432.77 + +437 + + + +432.78 + +438 + + + +432.79 + +439 + + + +432.80 + +440 + + + +432.81 + +441 + + + +432.82 + +442 + + + +432.83 + +443 + + + +432.84 + +444 + + + +432.85 + +445 + + + +432.86 + +446 + + + +164.0:se->275.0 + + + + + +164.0:sw->271.0 + + + + + +164.1 + +13 + + + +164.2 + +164 + + + +164.3 + +276 + + + +85.0:sw->0.0 + + + + + +85.0:se->68.0 + + + + + +85.1 + +85 + + + +274.0:sw->111.0 + + + + + +274.0:se->116.0 + + + + + +274.1 + +274 + + + +841.0:se->166.0 + + + + + +841.0:sw->239.0 + + + + + +841.1 + +@ + + + +841.1:sw->823.0 + + + + + +841.1:se->258.0 + + + + + +841.2 + +@ + + + +841.2:sw->846.0 + + + + + +841.2:se->170.0 + + + + + +6.0:sw->0.0 + + + + + +6.0:se->432.0 + + + + + +6.1 + +6 + + + +195.0:sw->0.0 + + + + + +195.0:se->176.0 + + + + + +195.1 + +195 + + + +762.0:se->28.0 + + + + + +762.0:sw->121.0 + + + + + +116.0:se->282.0 + + + + + +116.0:sw->233.0 + + + + + +116.1 + +12 + + + +116.2 + +116 + + + +116.3 + +273 + + + +116.4 + +283 + + + +305.0:se->304.0 + + + + + +305.0:sw->295.0 + + + + + +305.1 + +305 + + + +226.0:se->22.0 + + + + + +226.0:sw->224.0 + + + + + +226.1 + +226 + + + +793.0:sw->90.0 + + + + + +793.0:se->73.0 + + + + + +147.0:se->146.0 + + + + + +147.0:sw->145.0 + + + + + +147.1 + +@ + + + +147.1:se->713.0 + + + + + +147.1:sw->348.0 + + + + + +147.2 + +147 + + + +336.0:sw->0.0 + + + + + +336.0:se->148.0 + + + + + +336.1 + +336 + + + +68.0:se->71.0 + + + + + +82.0 + +@ + + + +68.0:sw->82.0 + + + + + +68.1 + +31 + + + +68.2 + +68 + + + +68.3 + +84 + + + +178.0:se->146.0 + + + + + +178.0:sw->176.0 + + + + + +178.1 + +@ + + + +178.1:se->304.0 + + + + + +728.0 + +@ + + + +178.1:sw->728.0 + + + + + +178.2 + +178 + + + +130.0:se->129.0 + + + + + +130.0:sw->44.0 + + + + + +130.1 + +130 + + + +319.0:sw->0.0 + + + + + +319.0:se->306.0 + + + + + +319.1 + +319 + + + +886.0:sw->303.0 + + + + + +886.0:se->884.0 + + + + + +51.0:se->50.0 + + + + + +51.0:sw->49.0 + + + + + +51.1 + +51 + + + +240.0:se->239.0 + + + + + +240.0:sw->136.0 + + + + + +240.1 + +@ + + + +240.1:se->258.0 + + + + + +240.1:sw->821.0 + + + + + +240.2 + +@ + + + +240.2:se->152.0 + + + + + +240.2:sw->861.0 + + + + + +240.3 + +240 + + + +240.4 + +257 + + + +807.0:sw->45.0 + + + + + +807.0:se->823.0 + + + + + +807.1 + +@ + + + +807.1:sw->775.0 + + + + + +807.1:se->170.0 + + + + + +161.0:se->160.0 + + + + + +161.0:sw->159.0 + + + + + +161.1 + +@ + + + +161.1:se->715.0 + + + + + +161.1:sw->350.0 + + + + + +161.2 + +161 + + + +350.0:se->349.0 + + + + + +350.0:sw->44.0 + + + + + +350.1 + +350 + + + +350.2 + +360 + + + +728.0:se->727.0 + + + + + +728.0:sw->44.0 + + + + + +82.0:se->81.0 + + + + + +82.0:sw->44.0 + + + + + +82.1 + +82 + + + +271.0:se->50.0 + + + + + +271.0:sw->264.0 + + + + + +271.1 + +266 + + + +271.2 + +271 + + + +3.1 + +3 + + + +192.0:se->242.0 + + + + + +192.0:sw->233.0 + + + + + +192.1 + +16 + + + +192.2 + +192 + + + +192.3 + +205 + + + +192.4 + +223 + + + +192.5 + +243 + + + +34.0:se->33.0 + + + + + +34.0:sw->26.0 + + + + + +34.1 + +34 + + + +790.0:sw->129.0 + + + + + +790.0:se->811.0 + + + + + +790.1 + +@ + + + +790.1:se->28.0 + + + + + +790.1:sw->134.0 + + + + + +333.0:sw->0.0 + + + + + +333.0:se->152.0 + + + + + +333.1 + +333 + + + +821.0:se->152.0 + + + + + +821.0:sw->805.0 + + + + + +175.0:sw->45.0 + + + + + +175.0:se->825.0 + + + + + +175.1 + +@ + + + +175.1:se->174.0 + + + + + +175.1:sw->171.0 + + + + + +175.2 + +175 + + + +852.0:se->160.0 + + + + + +852.0:sw->241.0 + + + + + +852.1 + +@ + + + +852.1:se->242.0 + + + + + +852.1:sw->821.0 + + + + + +852.2 + +@ + + + +852.2:sw->863.0 + + + + + +852.2:se->152.0 + + + + + +206.0:sw->204.0 + + + + + +206.0:se->192.0 + + + + + +206.1 + +206 + + + +395.0:sw->0.0 + + + + + +395.0:se->145.0 + + + + + +395.1 + +395 + + + +316.0:se->190.0 + + + + + +316.0:sw->314.0 + + + + + +316.1 + +316 + + + +48.1 + +48 + + + +48.2 + +62 + + + +48.3 + +87 + + + +48.4 + +123 + + + +48.5 + +202 + + + +48.6 + +220 + + + +48.7 + +312 + + + +725.0:sw->74.0 + + + + + +725.0:se->9.0 + + + + + +725.1 + +@ + + + +725.1:se->73.0 + + + + + +725.1:sw->749.0 + + + + + +725.2 + +@ + + + +725.2:sw->794.0 + + + + + +725.2:se->9.0 + + + + + +79.0:sw->107.0 + + + + + +79.0:se->138.0 + + + + + +79.1 + +26 + + + +79.2 + +79 + + + +79.3 + +139 + + + diff --git a/lice-egraph/dots/test4.svg b/lice-egraph/dots/test4.svg new file mode 100644 index 0000000..7d209ab --- /dev/null +++ b/lice-egraph/dots/test4.svg @@ -0,0 +1,153 @@ + + + + + + +egraph + + +cluster_0 + + + +cluster_4 + + + +cluster_5 + + + +cluster_2 + + + +cluster_3 + + + + +0.0 + +A + + + +0.1 + +0 + + + +4.0 + +@ + + + +4.0:sw->0.0 + + + + + +3.0 + +I + + + +4.0:se->3.0 + + + + + +4.1 + +4 + + + +5.0 + +@ + + + +2.0 + +IO.return + + + +5.0:sw->2.0 + + + + + +5.0:se->3.0 + + + + + +5.1 + +@ + + + +5.1:sw->4.0 + + + + + +5.1:se->5.1:n + + + + + +5.2 + +5 + + + +5.3 + +6 + + + +2.1 + +2 + + + +3.1 + +0 + + + +3.2 + +1 + + + +3.3 + +3 + + + diff --git a/lice-egraph/dots/test5.svg b/lice-egraph/dots/test5.svg new file mode 100644 index 0000000..67eabc7 --- /dev/null +++ b/lice-egraph/dots/test5.svg @@ -0,0 +1,301 @@ + + + + + + +egraph + + +cluster_0 + + + +cluster_8 + + + +cluster_5 + + + +cluster_2 + + + +cluster_10 + + + +cluster_4 + + + +cluster_12 + + + +cluster_9 + + + +cluster_3 + + + + +0.0 + +A + + + +0.1 + +0 + + + +8.0 + +IO.return + + + +8.1 + +8 + + + +5.0 + +@ + + + +2.0 + +@ + + + +5.0:se->2.0 + + + + + +12.0 + +K + + + +5.0:sw->12.0 + + + + + +5.1 + +5 + + + +2.0:se->2.0:n + + + + + +4.0 + +@ + + + +2.0:sw->4.0 + + + + + +2.1 + +@ + + + +2.1:sw->5.0 + + + + + +3.0 + +2 + + + +2.1:se->3.0 + + + + + +2.2 + +1 + + + +2.3 + +1 + + + +2.4 + +2 + + + +2.5 + +6 + + + +2.6 + +7 + + + +2.7 + +13 + + + +10.0 + +@ + + + +10.0:sw->8.0 + + + + + +10.0:se->2.0 + + + + + +10.1 + +@ + + + +10.1:se->10.1:n + + + + + +9.0 + +@ + + + +10.1:sw->9.0 + + + + + +10.2 + +10 + + + +10.3 + +11 + + + +4.0:sw->0.0 + + + + + +4.0:se->12.0 + + + + + +4.1 + +4 + + + +12.1 + +0 + + + +12.2 + +1 + + + +12.3 + +12 + + + +9.0:sw->0.0 + + + + + +9.0:se->2.0 + + + + + +9.1 + +9 + + + +3.1 + +3 + + + diff --git a/lice-egraph/src/lib.rs b/lice-egraph/src/lib.rs new file mode 100644 index 0000000..5f05846 --- /dev/null +++ b/lice-egraph/src/lib.rs @@ -0,0 +1,495 @@ +use egg::*; +use lice::combinator::Combinator; +use lice::file::{Expr, Index, Program}; +use ordered_float::OrderedFloat; +use std::collections::{HashMap}; +use std::cmp::Ordering; + + +pub struct MyAstSize; + +#[derive(Clone, Copy, PartialEq, Eq, Debug)] +pub enum MyCost { + Finite(usize), + Infinite(isize), +} + +fn add(a: MyCost, b: MyCost) -> MyCost { + use MyCost::*; + match (a, b) { + (Infinite(wtv), _) => Infinite(wtv), + (_, Infinite(wtv)) => Infinite(wtv), + (Finite(x), Finite(y)) => Finite(x + y), + } +} + +fn add1(a: MyCost, b: MyCost) -> MyCost { + add(add(a, b), MyCost::Finite(1)) +} + +impl PartialOrd for MyCost { + fn partial_cmp(&self, other: &Self) -> Option { + use MyCost::*; + match (self, other) { + (Finite(x), Finite(y)) => x.partial_cmp(y), + (Infinite(_), Infinite(_)) => Some(Ordering::Equal), + (Infinite(_), Finite(_)) => Some(Ordering::Greater), + (Finite(_), Infinite(_)) => Some(Ordering::Less), + } + } +} + +impl CostFunction for MyAstSize { + type Cost = MyCost; + + fn cost(&mut self, t: &SKI, mut costs: C) -> MyCost where C: FnMut(Id) -> MyCost { + match t { + SKI::App([f, a]) => { + let cf = costs(*f); + let ca = costs(*a); + let cost = add1(cf, ca); + // println!("App ({cost:?}): {f:?} ({cf:?}) @ {a:?} ({ca:?})"); + cost + } + SKI::Placeholder(id) => MyCost::Infinite(*id as isize), + SKI::Ref([id]) => { + add(MyCost::Finite(1), costs(*id)) + } + _ => { + // println!("{t:?}: 1"); + MyCost::Finite(1) + } + } + } +} + +#[derive(Clone, Hash, PartialEq, Eq, PartialOrd, Ord, Debug)] +struct PlaceHolderNum(usize); + +impl core::str::FromStr for PlaceHolderNum { + type Err = &'static str; + + fn from_str(_s: &str) -> Result { + Err("Cannot parse PlaceholderNum") + } +} + +impl core::fmt::Display for PlaceHolderNum { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + f.debug_tuple("PlaceHolder").field(&self.0).finish() + } +} + +impl From for PlaceHolderNum { + fn from(value: usize) -> Self { + Self(value) + } +} + +#[derive(Clone, Hash, PartialEq, Eq, PartialOrd, Ord)] +struct MyStr(String); + +impl core::str::FromStr for MyStr { + type Err = &'static str; + + fn from_str(_s: &str) -> Result { + Err("Cannot parse MyStr") + } +} + +impl core::fmt::Display for MyStr { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + let s = &self.0; + write!(f, "{}", s.as_str()) + } +} + +impl core::fmt::Debug for MyStr { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + let s = &self.0; + write!(f, "{}", s.as_str()) + } +} + +impl From for MyStr { + fn from(value: String) -> Self { + Self(value) + } +} + +define_language! { + pub enum SKI { + Prim(Combinator), + "@" = App([Id; 2]), + Int(i64), + Float(OrderedFloat), + Array(usize, Vec), + "*" = Ref([Id; 1]), // usize), + String(MyStr), + Tick(MyStr), + Ffi(MyStr), + Unknown(String), + Placeholder(usize), + } +} + +struct AstSizeHi; +impl CostFunction for AstSizeHi { + type Cost = usize; + fn cost(&mut self, enode: &SKI, mut costs: C) -> Self::Cost + where + C: FnMut(Id) -> Self::Cost, + { + let node_cost = match enode { + SKI::Placeholder(_) => usize::MAX, + SKI::Ref(_) => usize::MAX, + _ => 1, + }; + + enode.fold(node_cost, |sum, id| { + sum.saturating_add(costs(id)) + }) + } +} + +fn ski_reductions() -> Vec> { + vec![ + rewrite!("S"; "(@ (@ (@ S ?f) ?g) ?x)" => "(@ (@ ?f ?x) (@ ?g ?x))"), + rewrite!("K";"(@ (@ K ?f) ?g)" => "?f"), + rewrite!("I"; "(@ I ?x)" => "?x"), + rewrite!("B"; "(@ (@ (@ B ?f) ?g) ?x)" => "(@ ?f (@ ?g ?x))"), + rewrite!("C"; "(@ (@ (@ C ?f) ?x) ?y)" => "(@ (@ ?f ?y) ?x)"), + rewrite!("A"; "(@ (@ A ?x) ?y)" => "?y"), + rewrite!("S'"; "(@ (@ (@ (@ S' ?c) ?f) ?g) ?x)" => "(@ (@ ?c (@ ?f ?x)) (@ ?g ?x))"), + rewrite!("B'"; "(@ (@ (@ (@ B' ?c) ?f) ?g) ?x)" => "(@ (@ ?c ?f) (@ ?g ?x))"), + rewrite!("C'"; "(@ (@ (@ (@ C' ?c) ?f) ?x) ?y)" => "(@ (@ ?c (@ ?f ?y)) ?x)"), + rewrite!("P"; "(@ (@ (@ P ?x) ?y) ?f)" => "(@ (@ ?f ?x) ?y)"), + rewrite!("R"; "(@ (@ (@ R ?y) ?f) ?x)" => "(@ (@ ?f ?x) ?y)"), + rewrite!("O"; "(@ (@ (@ (@ O ?x) ?y) ?z) ?f)" => "(@ (@ ?f ?x) ?y)"), + rewrite!("U"; "(@ (@ U ?x) ?f)" => "(@ ?f ?x)"), + rewrite!("Z"; "(@ (@ (@ Z ?f) ?x) ?y)" => "(@ ?f ?x)"), + rewrite!("K2"; "(@ (@ (@ K2 ?x) ?y) ?z)" => "?x"), + rewrite!("K3"; "(@ (@ (@ (@ K3 ?x) ?y) ?z) ?w)" => "?x"), + rewrite!("K4"; "(@ (@ (@ (@ (@ K4 ?x) ?y) ?z) ?w) ?v)" => "?x"), + rewrite!("C'B"; "(@ (@ (@ (@ C'B ?f) ?g) ?x) ?y)" => "(@ (@ ?f ?x) (@ ?g ?y))"), + ] +} + +pub fn program_to_egraph(program: &Program) -> (Id, HashMap, EGraph) { + let mut egraph = EGraph::::default(); + let mut idx_eid_map = HashMap::::new(); + add_placeholders(program, &mut idx_eid_map, &mut egraph); + fill_placeholders(program, &mut idx_eid_map, &mut egraph); + + let root = match idx_eid_map.get(&program.root) { + Some(eid) => *eid, + None => panic!("missing root"), + }; + + eclasses_check(&egraph); + (root, idx_eid_map, egraph) +} + +pub fn optimize(egraph: EGraph, root: Id, fname: &str) -> String { + let runner = Runner::::default() + .with_egraph(egraph) + .run(&ski_reductions()); + + runner.egraph.dot().to_svg(fname).unwrap(); + eclasses_check(&runner.egraph); + + let extractor = Extractor::new(&runner.egraph, MyAstSize); + let (cost, best) = extractor.find_best(root); + + + println!("best: {best:?}"); + println!("expr: {:#?} \n cost: {:#?}", best.to_string(), cost); + + let mut i = true; + // println!("{{ "); + for ec in runner.egraph.classes() { + if !i { + // print!(", "); + } + i = false; + + // print!("\"eclass {:04}\": {{ ", ec.id); + + // print!("\"nodes\": ["); + let mut j = true; + for node in &ec.nodes { + if !j { + // print!(", "); + } + j = false; + // print!("\"{node:?}\""); + } + // print!(" ], "); + // print!("\"best cost\": \"{:?}\", ", extractor.find_best_cost(ec.id)); + // print!("\"Best node\": \"{:?}\" ", extractor.find_best_node(ec.id)); + // println!("}}"); + } + // println!("\n\n"); + + best.to_string() +} + +pub fn noop(egraph: EGraph, root: Id) -> String { + let runner = Runner::::default() + .with_egraph(egraph) + .run(&vec![]); + + let extractor = Extractor::new(&runner.egraph, AstSizeHi); + let (_, best) = extractor.find_best(root); + + runner.egraph.dot().to_svg("dots/foo.svg").unwrap(); + println!("best: {:#?}", best); + + best.to_string() +} + +fn add_placeholders( + program: &Program, + idx_eid_map: &mut HashMap, + egraph: &mut EGraph, +) { + program.body.iter().enumerate().for_each(|(idx, _)| { + let eid = egraph.add(SKI::Placeholder(idx.into())); + idx_eid_map.insert(idx, eid); + }) +} + +fn fill_placeholders( + program: &Program, + idx_eid_map: &mut HashMap, + egraph: &mut EGraph, +) { + program.body.iter().enumerate().for_each(|(idx, expr)| { + let eid = match expr { + Expr::Prim(comb) => egraph.add(SKI::Prim(*comb)), + Expr::Int(i) => egraph.add(SKI::Int(*i)), + Expr::Float(flt) => egraph.add(SKI::Float(OrderedFloat(*flt))), + Expr::String(s) => egraph.add(SKI::String(MyStr(s.to_string()))), + Expr::Tick(s) => egraph.add(SKI::Tick(MyStr(s.to_string()))), + Expr::Ffi(s) => egraph.add(SKI::Ffi(MyStr(s.to_string()))), + Expr::Ref(lbl) => { + let ref_idx = program.defs[*lbl]; + let ref_eid = match idx_eid_map.get(&ref_idx) { + Some(x) => *x, + None => panic!("missing ref"), + }; + let new_eid = egraph.add(SKI::Ref([ref_eid])); + egraph.union(new_eid, ref_eid); + new_eid + } + Expr::App(f, a) => { + let func_eid = match idx_eid_map.get(f) { + Some(eid) => *eid, + None => panic!("missing placeholder: {:#?}", f), + }; + let arg_eid = match idx_eid_map.get(a) { + Some(eid) => *eid, + None => panic!("missing placeholder: {:#?}", f), + }; + egraph.add(SKI::App([func_eid, arg_eid])) + } + Expr::Array(u, arr) => { + let e_arr: Vec = arr + .iter() + .map(|i| { + let elmt_eid = match idx_eid_map.get(i) { + Some(eid) => *eid, + None => panic!("missing placeholder: {:#?}", i), + }; + elmt_eid + }) + .collect(); + egraph.add(SKI::Array(*u, e_arr)) + } + _ => panic!("unknown expr: {:#?}", expr), + }; + + let placeholder = match idx_eid_map.get(&idx) { + Some(x) => *x, + None => panic!("missing placeholder eclass"), + }; + + egraph.union(placeholder, eid); + }) +} + +fn eclasses_check(egraph: &EGraph) { + egraph.classes().for_each(|ec| { + let not_ref_or_placeholder: Vec<&SKI> = ec + .nodes + .iter() + .filter(|en| !matches!(en, SKI::Placeholder(_) | SKI::Ref(_))) + .collect(); + assert!(!not_ref_or_placeholder.is_empty()) + }) +} + +#[cfg(test)] +mod tests { + use super::*; + + #[test] + fn reduce_skk_to_id() { + let mut egraph = EGraph::::default(); + let root = egraph.add_expr(&"(@ (@ (@ S K) K) 1)".parse().unwrap()); + let runner = Runner::::default() + .with_egraph(egraph) + .run(&ski_reductions()); + + let extractor = Extractor::new(&runner.egraph, AstSize); + let (_, best) = extractor.find_best(root); + assert!(best.to_string() == "1"); + } + + #[test] + fn program_to_egraph_then_reduce() { + let p = Program { + root: 5, + body: vec![ + /* 0 */ Expr::Prim(Combinator::S), + /* 1 */ Expr::Prim(Combinator::K), + /* 2 */ Expr::Int(1), + /* 3 */ Expr::App(0, 1), + /* 4 */ Expr::App(3, 1), + /* 5 */ Expr::App(4, 2), + ], + defs: vec![0], + }; + assert_eq!(p.to_string(), "S K :0 @ _0 @ #1 @ }"); + println!("expr: {:#?}\n", p.to_string()); + let (root, _, egraph) = program_to_egraph(&p); + let optimized = optimize(egraph, root, "dots/test1.svg"); + println!("optimized: {:#?}\n", optimized); + assert!(optimized == "1"); + } + + #[test] + fn ref_handling() { + let p = Program { + root: 5, + body: vec![ + /* 0 */ Expr::Prim(Combinator::S), + /* 1 */ Expr::Prim(Combinator::K), + /* 2 */ Expr::Int(1), + /* 3 */ Expr::App(0, 6), + /* 4 */ Expr::App(3, 6), + /* 5 */ Expr::App(4, 2), + /* 6 */ Expr::Ref(0), + ], + defs: vec![1], + }; + // println!("------- refs\n {:#?}", p.to_string()); + let (root, _m, egraph) = program_to_egraph(&p); + // println!("root: {:#?}", root); + // egraph.classes().for_each(|ec| { println!("{:#?}", ec)}); + let optimized = optimize(egraph, root, "dots/test2.svg"); + // println!("{:#?}\n", optimized); + assert!(optimized == "1"); + // println!("refs --------") + } + + #[test] + fn small() { + let p = Program { + root: 7, + body: vec![ + /* 0 */ Expr::Prim(Combinator::A), + /* 1 */ Expr::Prim(Combinator::K), + /* 2 */ Expr::Int(1), + /* 3 */ Expr::Int(2), + /* 4 */ Expr::App(0, 1), + /* 5 */ Expr::App(8, 2), + /* 6 */ Expr::App(5, 3), + /* 7 */ Expr::App(4, 6), + /* 8 */ Expr::Ref(0), + ], + defs: vec![1], + }; + println!("expr: {:#?}", p.to_string()); + let (root, _m, egraph) = program_to_egraph(&p); + // println!("root: {:#?}", root); + // egraph.classes().for_each(|ec| { println!("{:#?}", ec)}); + let optimized = optimize(egraph, root, "dots/test3.svg"); + println!("optimized: {:#?}\n", optimized); + } + + #[test] + fn small2() { + let p = Program { + root: 6, + body: vec![ + /* 0 */ Expr::Prim(Combinator::A), + /* 1 */ Expr::Prim(Combinator::I), + /* 2 */ Expr::Prim(Combinator::Return), + /* 3 */ Expr::Ref(0), + /* 4 */ Expr::App(0, 1), + /* 5 */ Expr::App(2, 3), + /* 6 */ Expr::App(4, 5), + ], + defs: vec![1], + }; + println!("expr: {:#?}", p.to_string()); + let (root, _m, egraph) = program_to_egraph(&p); + // println!("root: {:#?}", root); + // egraph.classes().for_each(|ec| { println!("{:#?}", ec)}); + let optimized = optimize(egraph, root, "dots/test4.svg"); + println!("optimized: {:#?}\n", optimized); + } + + #[test] + fn small3() { + let p = Program { + root: 11, + body: vec![ + /* 0 */ Expr::Prim(Combinator::A), + /* 1 */ Expr::Prim(Combinator::K), + /* 2 */ Expr::Int(1), + /* 3 */ Expr::Int(2), + /* 4 */ Expr::App(0, 1), + /* 5 */ Expr::App(12, 2), + /* 6 */ Expr::App(5, 3), + /* 7 */ Expr::App(4, 6), + /* 8 */ Expr::Prim(Combinator::Return), + /* 9 */ Expr::App(0, 7), + /* 10 */ Expr::App(8, 13), + /* 11 */ Expr::App(9, 10), + /* 12 */ Expr::Ref(0), + /* 13 */ Expr::Ref(1), + ], + defs: vec![1, 7], + }; + println!("expr: {:#?}", p.to_string()); + let (root, _m, egraph) = program_to_egraph(&p); + println!("root: {:#?}", root); + // egraph.classes().for_each(|ec| { println!("{:#?}", ec)}); + let optimized = optimize(egraph, root, "dots/test5.svg"); + println!("optimized: {:#?}\n", optimized); + } + + #[test] + fn cyclic() { + let p = Program { + root: 3, + body: vec![ + /* 0 */ Expr::Prim(Combinator::K), + /* 1 */ Expr::String("hi".to_string()), + /* 2 */ Expr::Ref(0), + /* 3 */ Expr::App(4, 1), + /* 4 */ Expr::App(0, 2), + ], + defs: vec![3], + }; + + println!("expr: {:#?}", p.to_string()); + let (root, _m, egraph) = program_to_egraph(&p); + println!("root: {:#?}", root); + // egraph.classes().for_each(|ec| { println!("{:#?}", ec)}); + let optimized = optimize(egraph, root, "dots/test6.svg"); + println!("optimized: {:#?}\n", optimized); + } +} diff --git a/lice-egraph/src/main.rs b/lice-egraph/src/main.rs new file mode 100644 index 0000000..1673d0b --- /dev/null +++ b/lice-egraph/src/main.rs @@ -0,0 +1,36 @@ +use clap::Parser; +use lice::file::CombFile; +use lice::combinator::Combinator; +use lice::file::{Expr, Index, Program}; +use lice_egraph::{noop, optimize, program_to_egraph}; +use log::error; +use std::{fs::File, io::Read, path::PathBuf, process, str::FromStr}; + +#[derive(Parser, Debug)] +struct Cli { + filename: PathBuf, +} + +fn main() { + let args = Cli::parse(); + + let Ok(mut f) = File::open(&args.filename) else { + error!( + "No such file or directory: {}", + args.filename.to_string_lossy() + ); + process::exit(1); + }; + let mut buf = String::new(); + f.read_to_string(&mut buf).unwrap_or_else(|e| { + error!("{e}"); + process::exit(1); + }); + let c = CombFile::from_str(&buf).unwrap_or_else(|e| { + error!("{e}"); + process::exit(1); + }); + + let (root, mp, egraph) = program_to_egraph(&c.program); + let optimized = optimize(egraph, root, "dots/main.svg"); +} diff --git a/lice/src/combinator.rs b/lice/src/combinator.rs index ac483e3..13487ec 100644 --- a/lice/src/combinator.rs +++ b/lice/src/combinator.rs @@ -38,6 +38,9 @@ pub enum ReduxCode { Copy, PartialEq, Eq, + Hash, + PartialOrd, + Ord, lice_macros::Reduce, parse_display::Display, num_enum::IntoPrimitive,