Skip to content

Conversation

@joom
Copy link
Member

@joom joom commented Jan 26, 2026

This PR introduces first-class support for Rocq type classes (though incomplete for complex ones w.r.t. indices), restructures the testing infrastructure, and fixes several code generation bugs.

  • Type Classes: Type classes are now extracted to C++ concepts with requires clauses, and type class instances become template structs with static methods. (closes Compilation of Rocq type classes to C++ concepts and structs #2)

  • Testing: The test infrastructure was modernized with dune-based test rules replacing shell scripts. Also added new tests for records and type classes.

Test results:

Running Crane Tests
━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━

basics/
  ack                       ✓ pass
  add_one                   ✓ pass
  binom                     ✓ pass
  colist                    ✗ fail
  eqordshow                 ✓ pass
  graph                     ✗ fail
  ind_param                 ✗ fail
  isort                     ✗ fail
  levenshtein               ✗ fail
  list                      ✓ pass
  map                       ✓ pass
  module                    ✓ pass
  msort                     ✗ fail
  multi_ind_functor         ✓ pass
  mutual_functor            ✓ pass
  mutual_mod                ✓ pass
  nat_bde                   ✓ pass
  nat                       ✓ pass
  nested_mod                ✗ fail
  nested_tree               ✗ fail
  psort                     ✗ fail
  pstring                   ✗ fail
  qsort                     ✗ fail
  rapply                    ✓ pass
  regexp                    ✗ fail
  rev                       ✗ fail
  rmatch                    ✓ pass
  tokenizer                 ✓ pass
  top_bde                   ✓ pass
  top                       ✓ pass
  tree                      ✓ pass
  vec                       ✗ fail
  zip                       ✗ fail

monadic/
  experiment                ✗ fail
  free_monad                ✗ fail
  hash_bde                  ✓ pass
  hash                      ✓ pass
  io                        ✓ pass
  par                       ✗ fail
  simple_io                 ✗ fail
  stm                       ✗ fail
  thread                    ✗ fail
  vector                    ✗ fail

━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━
Results: 21 passed, 22 failed, 43 total

@joom joom requested a review from mzweav January 26, 2026 20:53
@mzweav mzweav merged commit cc3a09e into main Jan 27, 2026
2 checks passed
@mzweav mzweav deleted the joomy/typeclasses branch January 27, 2026 14:34
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Compilation of Rocq type classes to C++ concepts and structs

3 participants