Code

Cek#16

Code

Merged

denismerigoux merged 42 commits intomainCatalaLang/catala-formalization:mainfrom cekCatalaLang/catala-formalization:cekCopy head branch name to clipboardJan 7, 2025

+2,525-1,332

Commits

Commits on Jan 6, 2025

• implementation of the cek abstract machine with ite

  adelaett

  committed
  ab93f2f

  Copy full SHA for ab93f2f

• notations

  adelaett

  committed
  33a9bf7

  Copy full SHA for 33a9bf7

• gitignore

  adelaett

  committed
  1ee8f4d

  Copy full SHA for 1ee8f4d

• documentation

  adelaett

  committed
  3557f42

  Copy full SHA for 3557f42

• modifications to miniml

  adelaett

  committed
  96d9a95

  Copy full SHA for 96d9a95

• fixing typing

  adelaett

  committed
  01e4039

  Copy full SHA for 01e4039

• fixing ife too

  adelaett

  committed
  f342bb5

  Copy full SHA for f342bb5

• moving to cek for catala.

  adelaett

  committed
  837521f

  Copy full SHA for 837521f

• fixing the cek ite

  adelaett

  committed
  401cb7b

  Copy full SHA for 401cb7b

• typing corrected.

  adelaett

  committed
  e2f29de

  Copy full SHA for e2f29de

• translation requires to have the environement in each continuations

  adelaett

  committed
  b84b9e7

  Copy full SHA for b84b9e7

• modification to the cred -> sred simulation

  adelaett

  committed
  a2acb9f

  Copy full SHA for a2acb9f

• correcting sred -> cred

  adelaett

  committed
  8e783bc

  Copy full SHA for 8e783bc

• writing about what i did

  adelaett

  committed
  15700f0

  Copy full SHA for 15700f0

• congruence definition for if-then-else

  adelaett

  committed
  7c5a018

  Copy full SHA for 7c5a018

• tactic examples

  adelaett

  committed
  9f99d49

  Copy full SHA for 9f99d49

• new tentative

  adelaett

  committed
  ed0bf0b

  Copy full SHA for ed0bf0b

• other tentatives

  adelaett

  committed
  d8ebdcc

  Copy full SHA for d8ebdcc

• working technique. Let's see if it continues.

  adelaett

  committed
  34a175d

  Copy full SHA for 34a175d

• seems to continue working!

  adelaett

  committed
  2371dd7

  Copy full SHA for 2371dd7

• adjusted "megatactic" to handle more cases.

  adelaett

  committed
  ae6a27c

  Copy full SHA for ae6a27c

• keeps working!!!

  adelaett

  committed
  df94c71

  Copy full SHA for df94c71

• keeps working. Need to have subtile (not-hammer) rewriting sometime

  adelaett

  committed
  766e299

  Copy full SHA for 766e299

• keep working.

  adelaett

  committed
  c74483a

  Copy full SHA for c74483a

• every cases but the ones that depends on a better decompose tactic.

  adelaett

  committed
  27ab894

  Copy full SHA for 27ab894

• found one case that does not work as expected.

  adelaett

  committed
  5249255

  Copy full SHA for 5249255

• proof finished, but too cases remains. Let's see what we can do.

  adelaett

  committed
  a53de01

  Copy full SHA for a53de01

• automation

  adelaett

  committed
  62b8cb6

  Copy full SHA for 62b8cb6

• removing debug logs.

  adelaett

  committed
  f72affa

  Copy full SHA for f72affa

• partial automisation

  adelaett

  committed
  381ea59

  Copy full SHA for 381ea59

• continuing the automation

  adelaett

  committed
  e831897

  Copy full SHA for e831897

• new diagram

  adelaett

  committed
  d8c7b2d

  Copy full SHA for d8c7b2d

• finally found a working diagram. Checking the remaining cases.

  adelaett

  committed
  1b5bd1a

  Copy full SHA for 1b5bd1a

• all but the nontrivial list handling is done.

  adelaett

  committed
  2445450

  Copy full SHA for 2445450

• working diagram

  adelaett

  committed
  a32806d

  Copy full SHA for a32806d

• removing automation and getting the correct diagram's proof.

  adelaett

  committed
  3e39019

  Copy full SHA for 3e39019

• cleanup

  adelaett

  committed
  620d82d

  Copy full SHA for 620d82d

• deadcode elim

  adelaett

  committed
  7a02ff9

  Copy full SHA for 7a02ff9

• remove equations from deps

  adelaett

  committed
  90c29f7

  Copy full SHA for 90c29f7

• commenting away one tactic test

  adelaett

  committed
  7ed41bc

  Copy full SHA for 7ed41bc

Commits on Jan 7, 2025

• iteration on tactics.

  adelaett

  committed
  bdb00ab

  Copy full SHA for bdb00ab

• switching to coq 8.20

  adelaett

  committed
  3fffcfe

  Copy full SHA for 3fffcfe