<commit_before>Dijkstra Monads for Free
------------------------

A basic, complete example:

```
fstar FStar.DM4F.Test.Fst
```

To see more debug output, and see the generated combinators:

```
fstar --trace_error --debug_level ED --debug FStar.DM4F.Test FStar.DM4F.Test.fst --prn --print_implicits --print_universes --print_bound_var_types
```

Current status:
- `repr`, `bind` and `return` are *-transformed and _-elaborated;
- same goes for the actions.

The code is in `src/tc/dmff.fs`.
- `star_type_definition` is the *-transformation from the paper for types;
- `star_expr_definition` performs the *-transformation and the _-elaboration at
  the same time; it relies on the bidirectional inference / synthesis engine
  (`infer` and `check`); details currently in a .txt note in our private
  repository.
- `trans_F` and `trans_G` are the `F_C(wp)` and `G^\epsilon_H` helpers from the
  paper
- `gen_wps_for_free` uses "stronger than" to generate more combinators;
  specifically, it generates `if_then_else`, `assert`, `assume`, `close`; it
  also generates `trivial` but the term is (at the time of this writing)
  ill-formed.

The output of the *-transformation and the _-elaboration is re-checked (the
generated terms are well-formed in F*); the effect definition is lifted from DM
to F*; missing WPs are generated, and everything is sent off to the "regular"
effect checking code.

Items left:
- fill out various TODOs in `dmff.fs` to faithfully check everything (right now,
  most checks are fairly lax);
- generate the missing WP combinators (`ite_wp`, `null_wp`)
- try out more things in the definition language; try out with a parameterized
  `STATE (h: heap)` effect; etc
- figure out how to properly type-check actions (right now, the code is
  suboptimal);
- * and elaboration of lifts
- inserting "return" on the fly when reflecting Tot computations
- more examples!
- figure out the impact of freshen_bv and merge this back into master
- extraction!<commit_msg>Update the README following this morning's progress<commit_after>Dijkstra Monads for Free
------------------------

A basic, complete example:

```
fstar FStar.DM4F.Test.Fst
```

To see the generated combinators (look for top-level definitions starting with
`FStar.DM4F.Test.STINT_`):

```
fstar --dump_module FStar.DM4F.Test FStar.DM4F.Test.fst
```

To see more debug output related to the DMFF elaboration and star
transformations:

```
fstar --trace_error --debug_level ED --debug FStar.DM4F.Test FStar.DM4F.Test.fst --prn --print_implicits --print_universes --print_bound_var_types
```

Current status:
- `repr`, `bind` and `return` are *-transformed and _-elaborated;
- same goes for the actions;
- all the remaining combinators are generated.

The code is in `src/tc/dmff.fs`.
- `star_type_definition` is the *-transformation from the paper for types;
- `star_expr_definition` performs the *-transformation and the _-elaboration at
  the same time; it relies on the bidirectional inference / synthesis engine
  (`infer` and `check`); details currently in a .txt note in our private
  repository.
- `trans_F` and `trans_G` are the `F_C(wp)` and `G^\epsilon_H` helpers from the
  paper
- `gen_wps_for_free` uses "stronger than" to generate more combinators;
  specifically, it generates `if_then_else`, `assert`, `assume`, `close`; it
  also generates `trivial` but the term is (at the time of this writing)
  ill-formed.

The output of the *-transformation and the _-elaboration is re-checked (the
generated terms are well-formed in F*); the effect definition is lifted from DM
to F*; missing WPs are generated, and everything is sent off to the "regular"
effect checking code.

Items left:
- fill out various TODOs in `dmff.fs` to faithfully check everything (right now,
  most checks are fairly lax);
- try out more things in the definition language; try out with a parameterized
  `STATE (h: heap)` effect; etc
- figure out how to properly type-check actions (right now, the code is
  suboptimal);
- * and elaboration of lifts
- inserting "return" on the fly when reflecting Tot computations
- more examples!
- figure out the impact of freshen_bv and merge this back into master
- extraction!

{'fraction_non_alphanumeric': 0.10090865614538498, 'fraction_numerical': 0.002152080344332855, 'mean_word_length': 4.058041112454656, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 3, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '3485032', 'n_tokens_mistral': 1295, 'n_tokens_neox': 1252, 'n_words': 543}