Symbolic evaluator overhaul

package.yaml

@@ -24,8 +24,10 @@ default-extensions:
 - BlockArguments
 - ConstraintKinds
 - DataKinds
+- DeriveGeneric
 - DeriveDataTypeable
 - DeriveTraversable
+- DerivingVia
 - FlexibleContexts
 - FlexibleInstances
 - GADTs
@@ -35,8 +37,11 @@ default-extensions:
 - MultiParamTypeClasses
 - MultiWayIf
 - NamedFieldPuns
+- OverloadedStrings
+- PatternSynonyms
 - RankNTypes
 - RecordWildCards
+- RecursiveDo
 # TODO: Perhaps it would be better to fade out any use of 'ScopedTypeVariables'
 # in favor of only using 'TypeAbstractions'. It is a lot less cursed.
 - ScopedTypeVariables
@@ -77,11 +82,14 @@ library:
   - template-haskell
   - microlens
   - effectful-core >= 2.5.1.0
+  - effectful
   - text
   - hashable
   - deepseq
   - bytestring
   - syb
+  - data-fix
+  - recursion-schemes
 
 tests:
   pantomime-test:
@@ -91,7 +99,6 @@ tests:
     - -threaded
     - -rtsopts
     - -with-rtsopts=-N
-    - -dynamic
     dependencies:
     - pantomime
     - hspec

pantomime.cabal

@@ -1,6 +1,6 @@
 cabal-version: 2.2
 
--- This file has been generated from package.yaml by hpack version 0.38.1.
+-- This file has been generated from package.yaml by hpack version 0.39.6.
 --
 -- see: https://github.com/sol/hpack
 
@@ -39,27 +39,20 @@ library
       Effectful.Grisette.Solver
       Pantomime
       Pantomime.Annotation
-      Pantomime.Axiom
-      Pantomime.Binding
       Pantomime.BuiltIn
-      Pantomime.Defer
       Pantomime.Embed
-      Pantomime.Expr
-      Pantomime.Fresh
-      Pantomime.Grisette.Mergeable
-      Pantomime.Grisette.UnionT
       Pantomime.Literal
       Pantomime.Marker
       Pantomime.Orphan.GHC
       Pantomime.Orphan.Grisette
       Pantomime.Passes
-      Pantomime.PrimOps
+      Pantomime.PrimOp
       Pantomime.Solve
-      Pantomime.Subst
-      Pantomime.Symbolise
       Pantomime.TH
+      Pantomime.Tsil
       Pantomime.Unification
       Pantomime.Util
+      Pantomime.WHNF
   other-modules:
       Paths_pantomime
   autogen-modules:
@@ -71,8 +64,10 @@ library
       BlockArguments
       ConstraintKinds
       DataKinds
+      DeriveGeneric
       DeriveDataTypeable
       DeriveTraversable
+      DerivingVia
       FlexibleContexts
       FlexibleInstances
       GADTs
@@ -82,8 +77,11 @@ library
       MultiParamTypeClasses
       MultiWayIf
       NamedFieldPuns
+      OverloadedStrings
+      PatternSynonyms
       RankNTypes
       RecordWildCards
+      RecursiveDo
       ScopedTypeVariables
       TemplateHaskell
       TupleSections
@@ -98,14 +96,17 @@ library
     , composition
     , constraints >=0.14.2
     , containers
+    , data-fix
     , deepseq
+    , effectful
     , effectful-core >=2.5.1.0
     , ghc >=9.12.2
     , grisette >=0.13.0.0
     , hashable
     , microlens
     , mtl
     , primitive
+    , recursion-schemes
     , syb
     , template-haskell
     , text
@@ -127,8 +128,10 @@ test-suite pantomime-test
       BlockArguments
       ConstraintKinds
       DataKinds
+      DeriveGeneric
       DeriveDataTypeable
       DeriveTraversable
+      DerivingVia
       FlexibleContexts
       FlexibleInstances
       GADTs
@@ -138,16 +141,19 @@ test-suite pantomime-test
       MultiParamTypeClasses
       MultiWayIf
       NamedFieldPuns
+      OverloadedStrings
+      PatternSynonyms
       RankNTypes
       RecordWildCards
+      RecursiveDo
       ScopedTypeVariables
       TemplateHaskell
       TupleSections
       TypeAbstractions
       TypeApplications
       TypeFamilies
       TypeOperators
-  ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-export-lists -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -Wprepositive-qualified-module -threaded -rtsopts -with-rtsopts=-N -dynamic
+  ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-export-lists -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -Wprepositive-qualified-module -threaded -rtsopts -with-rtsopts=-N
   build-depends:
       HUnit
     , base >=4.7 && <5

src/Effectful/GHC/TyThing.hs

@@ -1,10 +1,8 @@
 {-# LANGUAGE GADTs #-}
-{-# LANGUAGE KindSignatures #-}
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE UndecidableInstances #-}
-{-# LANGUAGE OverloadedStrings #-}
 {-# OPTIONS_GHC -Wno-orphans #-}
 
 module Effectful.GHC.TyThing
@@ -85,6 +83,7 @@ instance (Error (LookupError Name) :> es, HasThings :> es) => MonadThings (Eff e
       ATyCon tyCon -> pure tyCon
       _ -> throwError_ $ LookupError name
 
+-- | Lookup a class.
 lookupClass
   :: HasCallStack
   => Error (LookupError Name) :> es

src/Pantomime.hs

@@ -14,7 +14,7 @@ module Pantomime
 import GHC.Plugins hiding (empty, (<>))
 
 import Pantomime.Annotation
-import Pantomime.Axiom
+import Pantomime.Embed
 import Pantomime.Passes
 import Pantomime.TH (pantomime)
 import Pantomime.Marker

src/Pantomime/Annotation.hs

@@ -6,7 +6,7 @@ module Pantomime.Annotation
   ) where
 
 import Data.Data (Data)
-import Pantomime.Axiom (Embeddings)
+import Pantomime.Embed (Embeddings)
 import GHC.Utils.Outputable (Outputable (..), hang)
 
 -- TODO: Not sure I like the name. This checks whether an expression whose