Joachim’s Haskell and lean4 experiments #2
Conversation
nomeata
changed the title
|
Done. |
|
As the IL is still changing a lot, would you mind going through the non-draft PRs and merge what can be merged (and say why something can’t be merged), so that I don’t have to spend that much time on merge conflicts? |
There was a problem hiding this comment.
Do we all agree that the changes to the spec are temporary hacks? If so, that's okay with me, but we should clearly mark them as such, and we need to have a plan for resolving them quickly. Once other backends start depending on them it could become much more difficult to fix them.
|
I guess it's sensible if the backends wait a bit until these are decided since it might have non-trivial impact on the actual implementation. Update: oops, I accidentally clicked on 'Close with comment'. This is reopened. |
this is a pass that takes care of the problem with `MUT?`, which is a
non-functional expression (denotes multiple values), and thus cannot be
compiled like this to functional backends (proof backends).
Here is its effect:
```diff
relation Global_ok: `%|-%:%`(context, global, globaltype)
;; 3-typing.watsup:414.1-418.40
- rule _ {C : context, expr : expr, gt : globaltype, t : valtype}:
+ rule _ {C : context, expr : expr, gt : globaltype, t : valtype, w0 : ()?}:
`%|-%:%`(C, GLOBAL(gt, expr), gt)
-- Globaltype_ok: `|-%:OK`(gt)
- -- if (gt = `MUT%?%`(()?{}, t))
+ -- if (gt = `MUT%?%`(w0, t))
-- Expr_ok_const: `%|-%:%CONST`(C, expr, t)
```
Not to be merged, just for visibility.
This large branch contains (or contained) the following changes
Spec changes: None! (Since fd25f77)
Il changes:
TheEconstructor (Il-to-Il Totalization pass, adding TheE constructor #4)Il.Apart: A check for whether two (open) expression definitely cannot denote the same expression. (IL: A conservative apartness checker #16)Il.Eq:eq_idandeq_prem(Il.Eq improvements #5)Il-to-Il passes (the “middlend”):
ElsePr/otherwiseelimination passSubEelimination pass, synthesizing injection functions. (Il-to-Il pass: Make SubE explicit #10)otherwiseelimination pass (Il-to-Il: General otherwise elimination [archival branch] #17)Also needs the
NegPrconstructor (Add negated premises #7)This one is not acceptable, it seems, so someone needs to write an acceptable else elimination pass.
A Haskell backend.
Preview: https://github.com/Wasm-DSL/spectec/blob/joachim/spectec/test-haskell/SpecTec.hs
Supports data type definitions and function definitions.
A Lean4 backend.
Preview: https://github.com/Wasm-DSL/spectec/blob/joachim/spectec/test-lean4/SpecTec.lean
Supports the full current spec, but:
otherwisepass needs to be found.The main executable can run selected passes and/or backends (watsup exe: Flags to run middlend passes and different backends #6)
Tests for the middlend passes and the new backends.
CI