Code

Opaque extensions#1134

Code

Merged

maximebuyse merged 17 commits intomaincryspen/hax:mainfrom opaque-extensionscryspen/hax:opaque-extensionsCopy head branch name to clipboardDec 12, 2024

+511-150

Commits

Commits on Dec 5, 2024

• Unify (an extended version of) opaque and interface-only in a single erasure mechanism.

  maximebuyse

  committed
  e2aa8b8

  Copy full SHA for e2aa8b8

• Add tests for opaque attribute.

  maximebuyse

  committed
  1af618e

  Copy full SHA for 1af618e

• Tests snapshots.

  maximebuyse

  committed
  f3fb4d5

  Copy full SHA for f3fb4d5

• Update documentation of -i flag.

  maximebuyse

  committed
  3282b7e

  Copy full SHA for 3282b7e

• Allow to make opaque (and drop body) of selected (non-trait) impl methods.

  maximebuyse

  committed
  ef18a4f

  Copy full SHA for ef18a4f

• Document and correct.

  maximebuyse

  committed
  5574e81

  Copy full SHA for 5574e81

• Allow opaque types even without interface mode.

  maximebuyse

  committed
  ed3ef5c

  Copy full SHA for ed3ef5c

• Add function signature only in interface mode.

  maximebuyse

  committed
  30ec986

  Copy full SHA for 30ec986

• New tests snapshots.

  maximebuyse

  committed
  cdcd4fb

  Copy full SHA for cdcd4fb

• Remove body of methods inside impls in type-only mode.

  maximebuyse

  committed
  f300ff8

  Copy full SHA for f300ff8

• Pass generic arguments to erased impls.

  maximebuyse

  committed
  a9f56d8

  Copy full SHA for a9f56d8

• Remove the implementation without FStarBinder of erased_impl.

  maximebuyse

  committed
  cc2a7f9

  Copy full SHA for cc2a7f9

• Rename NeverDropBody to NeverErased.

  maximebuyse

  committed
  b9f31e4

  Copy full SHA for b9f31e4

• Updated tests.

  maximebuyse

  committed
  c5dc718

  Copy full SHA for c5dc718

Commits on Dec 12, 2024

• Merge branch 'main' into opaque-extensions

  W95Psp

  authored
  769f700

  Copy full SHA for 769f700

• Add more cases in opaque tests.

  maximebuyse

  committed
  b3de817

  Copy full SHA for b3de817

• Go back to previous behaviour for val interfaces in the fsti for impls with assoc type.

  maximebuyse

  committed
  7629b15

  Copy full SHA for 7629b15