Remove lingering references to Sally

The `what4-transition-system-tests` test suite in particular will be moved to `language-sally`.
GaloisInc · Apr 11, 2022 · 87b360b · 87b360b
1 parent 5901b36
commit 87b360b
Show file tree

Hide file tree

Showing 6 changed files with 5 additions and 258 deletions.
diff --git a/.gitmodules b/.gitmodules
@@ -7,7 +7,3 @@
 [submodule "dependencies/blt"]
 	path = dependencies/blt
 	url = https://github.com/GaloisInc/blt
-[submodule "dependencies/language-sally"]
-	path = dependencies/language-sally
-	url = https://github.com/GaloisInc/language-sally.git
-
diff --git a/cabal.project b/cabal.project
@@ -9,9 +9,8 @@ packages:
   what4-abc/
   what4-blt/
   what4-transition-system/
-  
+
 optional-packages:
   dependencies/abcBridge/
   dependencies/aig/
   dependencies/blt/
-  dependencies/language-sally/
diff --git a/dependencies/language-sally b/dependencies/language-sally
diff --git a/what4-transition-system/src/What4/TransitionSystem.hs b/what4-transition-system/src/What4/TransitionSystem.hs
@@ -81,9 +81,10 @@ createStateStruct sym namespace stateType =
 type CtxState state = Ctx.EmptyCtx Ctx.::> BaseTypes.BaseStructType state
 
 -- | Computes a set of side conditions we must add to state formulas to account
--- for the mismatch between What4 types and sally types.  For instance, a What4
--- @Nat@ must be translated as a Sally @Int@ (since Sally does not have natural
--- numbers), with a side condition of positivity.
+-- for the mismatch between What4 types and types found in transition systems
+-- such as MCMT and Sally.  For instance, a What4 @Nat@ must be translated as
+-- an MCMT @Int@ (since MCMT does not have natural numbers), with a side
+-- condition of positivity.
 sideConditions ::
   forall sym t st fs state.
   sym ~ ExprBuilder t st fs =>

diff --git a/what4-transition-system/test/Main.hs b/what4-transition-system/test/Main.hs
diff --git a/what4-transition-system/what4-transition-system.cabal b/what4-transition-system/what4-transition-system.cabal
@@ -35,16 +35,3 @@ library
     -Werror=overlapping-patterns
 
   default-language: Haskell2010
-
-test-suite what4-transition-system-tests
-  import:           dependencies
-  type:             exitcode-stdio-1.0
-  main-is:          Main.hs
-  other-modules:    Paths_what4_transition_system
-  hs-source-dirs:   test
-  ghc-options:
-    -Wall -Werror=incomplete-patterns -Werror=missing-methods
-    -Werror=overlapping-patterns
-
-  build-depends:    what4-transition-system
-  default-language: Haskell2010