Extend cryptol-saw-core tests to include SuiteB.cry and PrimeEC.cry.

GaloisInc · Jun 16, 2021 · 7190cf4 · 7190cf4
1 parent ebf2832
commit 7190cf4
Showing 1 changed file with 9 additions and 3 deletions.
diff --git a/cryptol-saw-core/test/CryptolVerifierTC.hs b/cryptol-saw-core/test/CryptolVerifierTC.hs
@@ -31,11 +31,17 @@ main =
      putStrLn "Translated Float.cry!"
      cenv2 <- CEnv.importModule sc cenv1 (Right N.arrayName) Nothing CEnv.OnlyPublic Nothing
      putStrLn "Translated Array.cry!"
-     cenv3 <- CEnv.parseDecls sc cenv2 (CEnv.InputText superclassContents "superclass.cry" 1 1)
+     cenv3 <- CEnv.importModule sc cenv2 (Right N.suiteBName) Nothing CEnv.OnlyPublic Nothing
+     putStrLn "Translated SuiteB.cry!"
+     cenv4 <- CEnv.importModule sc cenv3 (Right N.primeECName) Nothing CEnv.OnlyPublic Nothing
+     putStrLn "Translated PrimeEC.cry!"
+     cenv5 <- CEnv.importModule sc cenv4 (Right N.preludeReferenceName) Nothing CEnv.OnlyPublic Nothing
+     putStrLn "Translated Reference.cry!"
+     cenv6 <- CEnv.parseDecls sc cenv5 (CEnv.InputText superclassContents "superclass.cry" 1 1)
      putStrLn "Translated superclass.cry!"
-     cenv4 <- CEnv.parseDecls sc cenv3 (CEnv.InputText instanceContents "instance.cry" 1 1)
+     cenv7 <- CEnv.parseDecls sc cenv6 (CEnv.InputText instanceContents "instance.cry" 1 1)
      putStrLn "Translated instance.cry!"
-     mapM_ (checkTranslation sc) $ Map.assocs (CEnv.eTermEnv cenv4)
+     mapM_ (checkTranslation sc) $ Map.assocs (CEnv.eTermEnv cenv7)
      putStrLn "Checked all terms!"
 
 checkTranslation :: SharedContext -> (N.Name, Term) -> IO ()