Adding an interpreter to lcalc #432
Conversation
|
I've implemented the correct behavior. @AltGr could you take a look to the typing errors? |
Lcalc for some reason
I made some changes in the meantime, and had to factorise e.g. the handling of the `EEmptyError` case, but this is the simple approach type-wise of making the function type for `∀ 'a. 'a —> 'a` (with `assert false` match cases), then restricting its type do `dcalc` or `lcalc` in the `.mli`.
AltGr
force-pushed
the
adelaett-lcalc-interpret
branch
from
1acdab0
to
0098f00
Compare
It would probably be simpler to just add a toplevel |
| @@ -58,6 +60,7 @@ let backend_option_to_string = function | |||
| let backend_option_of_string backend = | |||
| match String.lowercase_ascii backend with | |||
| | "interpret" -> `Interpret | |||
| | "interpret_lcalc" -> `Interpret_Lcalc | |||
There was a problem hiding this comment.
This new backend should be documented in the info variable in this file (around line ~300).
There was a problem hiding this comment.
I've added a docstring. Can you confirm it is ok?
| Expr.map_raw ~fop:Operator.translate | ||
| ~floc:(function _ -> .) | ||
| ~f:(translate_expr ctx) (Marked.mark m e) | ||
| | EOp { op; tys } -> Expr.eop (Operator.translate op) tys m |
There was a problem hiding this comment.
You're changing the behavior of your compilation pass here, is this wanted?
There was a problem hiding this comment.
We now have a different Expr.map function that don't required anymore the fop and floc functions. Hence, the behavior is the same for the lines you underlined.
| "Expected a boolean literal for the result of this assertion \ | ||
| (should not happen if the term was well-typed)") | ||
|
|
||
| let interpret_program_lcalc p s : (Uid.MarkedString.info * ('a, 'm) gexpr) list |
There was a problem hiding this comment.
Do you really have to duplicate the code for interpret_program_lcalc and interpret_program_dcalc ?
There was a problem hiding this comment.
yes there is typing issues. From the discussion with @AltGr, we concluded we need two differents functions.
|
Perfect, we can merge once CI is green on my side. |
work in progress: I have some issues with GADT