PatternLowering.hs (9828B)
1 -- Opt-in candidate controls. Built through Nix by pattern_lowering.py. 2 -- The reference compiler constructs independent authored oracles, never candidate expectations. 3 module Main where 4 import Runtime 5 import Wire 6 import TreeObservation 7 import qualified Data.ByteString as BS 8 import qualified Data.Text as Text 9 import qualified Data.Vector as V 10 import qualified Data.Map as Map 11 import qualified Data.Aeson as JSON 12 import Control.Monad 13 import Control.Exception 14 import System.Directory 15 import Data.List (isSuffixOf,isPrefixOf) 16 import System.Environment 17 import System.Timeout (timeout) 18 19 load path = do 20 bytes <- BS.readFile path 21 bundle <- either error pure (decodeBundle bytes) 22 either error pure (verifyBundle bundle) 23 let nodes = reconstructBundleTerms(bundleNodes bundle) 24 pure $ Map.fromList [(Text.unpack(exportName ex),nodes V.! fromIntegral(exportRoot ex))|ex<-manifestExports(bundleManifest bundle)] 25 bindings (Fork (Stem Leaf) (Fork value _)) = case toList value of 26 Right rows -> Map.fromList [(either error id (toString name),term)|Fork name term<-rows] 27 _ -> error "invalid definition list" 28 bindings (Fork Leaf (Fork diagnostic _)) = error ("compile failure: "++formatT Decode diagnostic) 29 bindings other = error ("invalid compiler reply: "++show other) 30 compile unit env source = apply (apply unit env) (ofString source) 31 selected reply = case reply of 32 Fork (Stem Leaf) (Fork _ _) -> Fork (Stem Leaf) (Fork (bindings reply Map.! "main") Leaf) 33 Fork Leaf (Fork problem _) -> Fork Leaf (Fork problem Leaf) 34 _ -> error "invalid compiler reply" 35 36 main = do 37 [directory] <- getArgs 38 candidate <- load(directory++"/source_unit.arboricx") 39 reference <- load "test/fixtures/compiler-library.arboricx" 40 retained <- load(directory++"/reference-unit.arboricx") 41 let unit = candidate Map.! "compileStableModuleDefinitions" 42 old = retained Map.! "compileStableModuleDefinitions" 43 helpers = ofList [Fork (ofString (drop (length prefix) name)) term | (name,term)<-Map.toList reference, prefix<-["prelude.","parser."],prefix `isPrefixOf` name] 44 oracle source = bindings (compile old helpers ("main = "++source)) Map.! "main" 45 corpusBytes <- BS.readFile(directory++"/equations.json") 46 corpus <- either error pure (JSON.eitherDecodeStrict' corpusBytes :: Either String [(String,String,String,String,Bool)]) 47 forM_ corpus $ \(label,source,expected,environment,truth) -> do 48 let actual = selected(compile unit (oracle environment) source) 49 wanted = oracle expected 50 unless ((actual==wanted)==truth) $ error (label++": wrong result\n"++show actual++"\nexpected\n"++show wanted) 51 putStrLn ("equation "++label++": passed") 52 let output=directory++"/programs" 53 baseline=directory++"/reference-programs" 54 createDirectoryIfMissing True output 55 createDirectoryIfMissing True baseline 56 files <- filter (isSuffixOf ".tri") <$> listDirectory (directory++"/program-sources") 57 forM_ files $ \file -> do 58 source <- unlines . filter (not . isPrefixOf "!export") . lines <$> readFile (directory++"/program-sources/"++file) 59 let code=bindings(compile unit Leaf source) 60 get name=code Map.! name 61 function=get "main" 62 poison=error "ignored subtree forced" :: T 63 check label actual expected=unless(actual==expected)(error(file++": "++label)) 64 trees 0=[Leaf] 65 trees n=let cs=trees(n-1) in Leaf:map Stem cs++[Fork a b|a<-cs,b<-cs] 66 inputs=trees(2::Int) 67 forceTreeShared function 68 if "eq-" `isPrefixOf` file then do 69 let eq=apply(get "y")(get "worker") 70 forM_ inputs $ \a -> forM_ inputs $ \b -> check "finite equality" (apply(apply eq a)b) (if a==b then Stem Leaf else Leaf) 71 check "root mismatch" (apply(apply eq Leaf)(Stem poison)) Leaf 72 check "early mismatch" (apply(apply eq(Fork Leaf poison))(Fork(Stem Leaf)poison)) Leaf 73 let partial=Fork Leaf poison 74 failure<-try(evaluate(apply(apply eq partial)partial))::IO(Either SomeException T) 75 case failure of Left _->pure();Right _->error "partial reflexivity" 76 else if "copy-" `isPrefixOf` file then do 77 let oracle (Fork h r)=Fork(Stem h)(oracle r) 78 oracle _=Leaf 79 forM_ inputs $ \x -> check "finite copy" (apply function x)(oracle x) 80 check "malformed root" (apply function(Stem poison)) Leaf 81 case apply function(Fork poison Leaf) of 82 Fork(Stem _)rest->check "ignored head" rest Leaf 83 _->error "copy head" 84 case apply function(Fork Leaf poison) of 85 Fork first _->check "ignored tail" first(Stem Leaf) 86 _->error "copy tail" 87 else do 88 let pick Leaf=Leaf 89 pick(Stem _)=Stem Leaf 90 pick(Fork _ _)=Fork Leaf Leaf 91 oracle(Fork h r)=Fork(pick h)(oracle r) 92 oracle _=Leaf 93 forM_ inputs $ \x -> check "finite classifier" (apply function x)(oracle x) 94 check "ignored stem" (apply function(Fork(Stem poison)Leaf))(Fork(Stem Leaf)Leaf) 95 check "ignored fork" (apply function(Fork(Fork poison poison)Leaf))(Fork(Fork Leaf Leaf)Leaf) 96 forM_ [(output,code),(baseline,bindings(compile old Leaf source))] $ \(destination,terms) -> do 97 bundle<-buildBundleShared [(Text.pack name,terms Map.! name)|name<-["main","worker","y"]] 98 BS.writeFile(destination++"/"++take(length file-4)file++".arboricx")(encodeBundle bundle) 99 putStrLn("program "++file++": finite/demand controls passed") 100 101 -- Independent code-generation targets: ordinary readable equations must now 102 -- construct the same tree as the hand-written direct dispatcher. The retained 103 -- compiler must fail that target, rather than being a vacuous semantic control. 104 let canonical tree = encodeBundle <$> buildBundleShared [("root",tree)] 105 forM_ [("copy-equations","copy-triage"),("pick-equations","pick-triage")] $ \(authored,manual) -> do 106 fresh <- load(output++"/"++authored++".arboricx") >>= canonical . (Map.! "main") 107 wanted <- load(baseline++"/"++manual++".arboricx") >>= canonical . (Map.! "main") 108 previous <- load(baseline++"/"++authored++".arboricx") >>= canonical . (Map.! "main") 109 unless(fresh==wanted && previous/=wanted)(error("code-generation target: "++authored)) 110 forM_ ["copy-triage","pick-triage","eq-triage-explicit"] $ \name -> do 111 fresh <- load(output++"/"++name++".arboricx") >>= canonical . (Map.! "main") 112 previous <- load(baseline++"/"++name++".arboricx") >>= canonical . (Map.! "main") 113 unless(fresh==previous)(error("non-pattern control changed: "++name)) 114 putStrLn "exact direct-dispatch targets, wrong-compiler and unchanged-control checks passed" 115 let function source = do 116 let term=bindings(compile unit Leaf source) Map.! "main" 117 forceTreeShared term 118 pure term 119 poison=error "split moved an unreached test" :: T 120 check source input expected = do 121 term<-function source 122 unless(apply term input==expected)(error("demand/order: "++source)) 123 check "f _ t = 23\nf (t _) _ = 24\nf _ _ = 25\nmain input = f input t" poison (ofNumber 23) 124 check "f (t _) t = 23\nf _ _ = 24\nmain input = f t input" poison (ofNumber 24) 125 check "f (t t (t x)) = x\nf _ = 24\nmain input = f (t (t t) input)" poison (ofNumber 24) 126 check "f (t (t x) y) = y\nf (t x y) = x\nf _ = t\nmain input = f input" 127 (Fork (ofNumber 23) poison) (ofNumber 23) 128 check "main input = (wanted : let\n f t ^wanted = 23\n f _ _ = 24\n in f (t t) t) input" poison (ofNumber 24) 129 preserve<-function "f (t _) = t\nf original = original\nmain input = f input" 130 case apply preserve(Fork(ofNumber 23)poison) of 131 Fork first _ | first==ofNumber 23 -> pure () 132 _->error "fallback lost original subject" 133 whole<-function "main (t original{_} rest) = t original rest\nmain _ = t" 134 case apply whole(Fork(ofNumber 23)poison) of 135 Fork first _ | first==ofNumber 23 -> pure () 136 _->error "known constructor lost whole-child capture" 137 putStrLn "split-column, nested-failure, pin and whole-capture demand controls passed" 138 139 -- Ineligible splits must retain the old sequential representation exactly. 140 forM_ ["wanted = t\nmain ^wanted = t t\nmain _ = t", 141 "main whole{t} = t t\nmain _ = t", 142 "main 23 = t t\nmain _ = t", 143 "main _ t = t\nmain (t _) _ = t t\nmain _ _ = t t t"] $ \source -> do 144 fresh <- canonical (bindings(compile unit Leaf source) Map.! "main") 145 previous <- canonical (bindings(compile old Leaf source) Map.! "main") 146 unless(fresh==previous)(error "sequential fallback representation changed") 147 putStrLn "sequential fallback identity controls passed" 148 -- Stable-only change: ordinary optimized lowering retains exact function 149 -- trees. Avoid its known closed-recursion construction hazard in this control. 150 forM_ ["main t = t\nmain (t _) = t t\nmain _ = t t t", 151 "main x = case x of\n (t a b) = a\n _ = t", 152 "main x = let\n f t = x\n f _ = t\n in f x"] $ \source -> do 153 let fresh = bindings(compile (candidate Map.! "compileModuleDefinitions") Leaf source) Map.! "main" 154 previous = bindings(compile (retained Map.! "compileModuleDefinitions") Leaf source) Map.! "main" 155 a <- canonical fresh 156 b <- canonical previous 157 unless(a==b)(error "optimized representation changed") 158 -- Fully publishing a function must not execute a closed divergent branch. 159 -- Both direct top-level matching and a local case exercise stable routing. 160 forM_ ["spin x = spin x\nmain t = spin t\nmain other = other", 161 "spin x = spin x\nmain input = case input of\n t = spin t\n other = other", 162 "spin x = spin x\nmain input = let\n f t = spin t\n f other = other\n in f input"] $ \source -> do 163 term <- function source 164 unless(apply term (Stem Leaf)==Stem Leaf)(error "unselected closed divergence") 165 case apply term (Stem poison) of 166 Stem _ -> pure () 167 _ -> error "guard inspected ignored child" 168 negative <- timeout 200000 (evaluate (apply term Leaf)) 169 case negative of 170 Nothing -> pure () 171 Just _ -> error "demanded divergent branch returned" 172 putStrLn "optimized identity and stable closed-divergence construction controls passed"