Code

Add states natively to execution monad#3

Code

Draft

Nils-Lauermann wants to merge 17 commits intomainrems-project/archsem:mainfrom stateful_execrems-project/archsem:stateful_execCopy head branch name to clipboard

Commits

Commits on Mar 17, 2025

• Modify Exec to include a state (especially also in the errors)

  Nils-Lauermann

  committed
  f99f44a

  Copy full SHA for f99f44a

• Adapt more definitions

  Nils-Lauermann

  committed
  5dcee7d

  Copy full SHA for 5dcee7d

• Introduce monadic instances for res with state unit

  Nils-Lauermann

  committed
  27a273b

  Copy full SHA for 27a273b

• Finish redefinition of Exec monad with states

  Nils-Lauermann

  committed
  d5b7150

  Copy full SHA for d5b7150

• Improve definitions and proofs

  Nils-Lauermann

  committed
  877934d

  Copy full SHA for 877934d

• Fix small issues

  Nils-Lauermann

  committed
  27e1c0b

  Copy full SHA for 27e1c0b

• Fix GenModels

  Nils-Lauermann

  committed
  8c678b8

  Copy full SHA for 8c678b8

• Try to adapt promising

  Nils-Lauermann

  committed
  4d0ffcd

  Copy full SHA for 4d0ffcd

• WIP stateful_exec_promising

  

  tperami

  authored and

  Nils-Lauermann

  committed
  c63274a

  Copy full SHA for c63274a

• Remove obligatory state from res record

  Nils-Lauermann

  committed
  1ae991c

  Copy full SHA for 1ae991c

Commits on Mar 20, 2025

• Add unfold instances

  Nils-Lauermann

  committed
  5df0e65

  Copy full SHA for 5df0e65

Commits on Mar 21, 2025

• Use new getter notation

  Nils-Lauermann

  committed
  b94a01f

  Copy full SHA for b94a01f

• Make Exec.t transparent and add useful CDestrSimpl instances

  Nils-Lauermann

  committed
  b57dd42

  Copy full SHA for b57dd42

• Add CDestruct instances

  Nils-Lauermann

  committed
  0bbdae4

  Copy full SHA for 0bbdae4

• Slight improvements

  Nils-Lauermann

  committed
  36959f8

  Copy full SHA for 36959f8

• Add infrastructure

  Nils-Lauermann

  committed
  1858263

  Copy full SHA for 1858263

• Remove leftover Program

  Nils-Lauermann

  committed
  cfac084

  Copy full SHA for cfac084