Skip to content
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.

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

Add Grisette.Unified #210

Merged
merged 23 commits into from
Jun 20, 2024
Merged

Add Grisette.Unified #210

merged 23 commits into from
Jun 20, 2024

Conversation

lsrcz
Copy link
Owner

@lsrcz lsrcz commented Jun 13, 2024

This pull request adds a unified interface to symbolic and concrete code. With this pull request, the user can write code like:

finteger :: forall mode. (IsMode mode) => GetInteger mode -> GetInteger mode -> GetInteger mode
finteger l r =
  mrgIte @mode
    (l .== r)
    (l + r)
    (symIte @mode (l .< r) l r)

finteger (1 :: Integer) 2        -- under 'Con mode
finteger ("a" :: SymInteger) "b" -- under 'Sym mode

All the operations are introduced with a single IsMode mode constraint.

Data types are also supported. Here GetData resolves to A 'Con when mode is 'Con, and resolves to UnionM (A 'Sym) when mode is 'Sym.

data A mode = A (GetIntN mode 8) | AT (GetData mode (A mode))
  deriving (Generic)
deriving via (Default (A mode)) instance (IsMode mode) => (Mergeable (A mode))

fdata ::
  forall mode m.
  (FDataConstraint mode m) =>
  GetData mode (A mode) ->
  m (GetIntN mode 8)
fdata d = do
  a :: A mode <- extractData @mode d
  case a of
    A v -> mrgModifyError id $ safeDiv v (v - 1)
    AT v -> fdata v

@lsrcz lsrcz self-assigned this Jun 13, 2024
@lsrcz lsrcz force-pushed the feat-unified branch 2 times, most recently from a815f91 to ac4aa27 Compare June 13, 2024 09:42
Copy link

codecov bot commented Jun 13, 2024

Codecov Report

Attention: Patch coverage is 87.64045% with 44 lines in your changes missing coverage. Please review.

Project coverage is 55.37%. Comparing base (f5d4d03) to head (34e35a9).
Report is 1 commits behind head on main.

Files Patch % Lines
...risette/Unified/Internal/Class/UnifiedBranching.hs 48.00% 12 Missing and 1 partial ⚠️
src/Grisette/Unified/Internal/Class/UnifiedSOrd.hs 37.50% 10 Missing ⚠️
.../Grisette/Internal/Core/Data/Class/SafeDivision.hs 42.85% 2 Missing and 2 partials ⚠️
src/Grisette/Unified/Lib/Data/Foldable.hs 94.59% 4 Missing ⚠️
...Grisette/Internal/Core/Data/Class/SafeSymRotate.hs 80.00% 0 Missing and 2 partials ⚠️
src/Grisette/Lib/Control/Monad.hs 94.87% 2 Missing ⚠️
src/Grisette/Unified/Internal/Class/UnifiedSEq.hs 50.00% 2 Missing ⚠️
src/Grisette/Unified/Lib/Control/Monad.hs 96.96% 0 Missing and 2 partials ⚠️
src/Grisette/Lib/Control/Applicative.hs 93.33% 1 Missing ⚠️
...rc/Grisette/Unified/Internal/Class/UnifiedITEOp.hs 80.00% 1 Missing ⚠️
... and 3 more
Additional details and impacted files
@@            Coverage Diff             @@
##             main     #210      +/-   ##
==========================================
+ Coverage   54.86%   55.37%   +0.51%     
==========================================
  Files          85       97      +12     
  Lines        7385     7548     +163     
  Branches      643      645       +2     
==========================================
+ Hits         4052     4180     +128     
- Misses       2690     2723      +33     
- Partials      643      645       +2     

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

@lsrcz lsrcz force-pushed the feat-unified branch 3 times, most recently from f24a192 to 9f09e39 Compare June 13, 2024 19:54
@lsrcz
Copy link
Owner Author

lsrcz commented Jun 20, 2024

I will just merge this into the core, and subsequent refactoring and new features will be in different pull requests.

Tasks to do:

  • Reorganize some core type classes that may also need to be unified.
  • Reorganize the Template Haskell code
  • Add unification support for other unified type classes.

@lsrcz lsrcz merged commit ac0934b into main Jun 20, 2024
20 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

1 participant