Skip to content

Improvement to 'Embeddable' typeclass through 'Embedding' GADT #21

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
RobinWebbers merged 7 commits into from
Jul 31, 2026
Merged

Improvement to 'Embeddable' typeclass through 'Embedding' GADT #21

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
7 commits
Select commit Hold shift + click to select a range
2ef46c0
Stub for heterogeneous embedding using 'Embed'
RobinWebbers Jul 20, 2026
74cd929
WIP embeddings. This implements the improved API for type embeddings.…
RobinWebbers Jul 24, 2026
f6f6259
Changed type embeddings interface to allow for a type alias that we s…
RobinWebbers Jul 24, 2026
bf5f4a4
Added some comments to changes in expression subsumption.
RobinWebbers Jul 27, 2026
cb002b2
Adjusted fresh variable instantiation to use the new embeddings. Bugf…
RobinWebbers Jul 29, 2026
2297f5f
Adjusted fresh variable generation to work with the InstEnvs. Fixed b…
RobinWebbers Jul 30, 2026
0a83fe0
Typo in commit
RobinWebbers Jul 30, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions package.yaml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -81,6 +81,7 @@ library:
- hashable
- deepseq
- bytestring
- syb

tests:
pantomime-test:
Expand Down
1 change: 1 addition & 0 deletions pantomime.cabal
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -106,6 +106,7 @@ library
, microlens
, mtl
, primitive
, syb
, template-haskell
, text
, transformers
Expand Down
2 changes: 1 addition & 1 deletion src/Pantomime.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ module Pantomime
( plugin

, Theory (..)
, PluginAxioms (..)
, Embeddings (..)
, pantomime
, pantomimeMarker
, pantomimeNothing
Expand Down
4 changes: 2 additions & 2 deletions src/Pantomime/Annotation.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,13 +6,13 @@ module Pantomime.Annotation
) where

import Data.Data (Data)
import Pantomime.Axiom (PluginAxioms)
import Pantomime.Axiom (Embeddings)
import GHC.Utils.Outputable (Outputable (..), hang)

-- TODO: Not sure I like the name. This checks whether an expression whose
-- result is of type Bool is valid. That is, whether it will always return True.
data Theory where
Theory :: PluginAxioms -> Theory
Theory :: Embeddings -> Theory
deriving (Show, Data)

instance Outputable Theory where
Expand Down
Loading
Loading