Bring more structure to Dcalc #164
Conversation
denismerigoux
added
✨ enhancement
| type scope_body = { | ||
| scope_body_lets : scope_let list; | ||
| scope_body_result : expr Pos.marked Bindlib.box; | ||
| scope_body_arg : expr Bindlib.var; |
There was a problem hiding this comment.
why scope_let_var is Pos.marked and scope_body_arg is not ?
| | SubScopeVarDefinition (** [let s.x = fun _ -> e] *) | ||
| | CallingSubScope (** [let result = s ({ x = s.x; y = s.x; ...}) ]*) | ||
| | DestructuringSubScopeResults (** [let s.x = result.x ]**) | ||
| | Assertion (** [let _ = assert e]*) |
There was a problem hiding this comment.
thanks for the comments! :)
There was a problem hiding this comment.
after reading the scope to dcalc transformation, it might be a good idea here to put
[let x = e, where e = error_on_empty e' for some e']
to emphasis the fact that structural invariant are not kept by the ocaml type system.
There was a problem hiding this comment.
or we could use gadts, but that's more complicated
| let make_multiple_let_in (xs : Var.t array) (taus : typ Pos.marked list) | ||
| (e1 : expr Pos.marked Bindlib.box list) (e2 : expr Pos.marked Bindlib.box) (pos : Pos.t) : | ||
| expr Pos.marked Bindlib.box = | ||
| make_app (make_abs xs e2 pos taus pos) e1 pos |
There was a problem hiding this comment.
why did you removed this function ? It could still be useful (for instance lines 194 and following)
|
|
||
| open Ast | ||
|
|
||
| val optimize_program : program -> program |
There was a problem hiding this comment.
Could you explain why did you removed the optimization on the Dcalc ?
|
|
||
| type program = { decl_ctx : decl_ctx; scopes : (ScopeName.t * Var.t * expr Pos.marked) list } | ||
| val build_whole_program_expr : program -> ScopeName.t -> expr Pos.marked Bindlib.box |
There was a problem hiding this comment.
Why does the result is boxed ? It seems everywhere this function is used, its results is immediately unboxed.
Motivation
To complete #158, we need to minimize the amount of option transformations happening when compiling the scopes body. In general, this amount cannot really be minimized; but here we may leverage the invariants coming from the Scopelang -> Dcalc translation to "optionize" just the minimal amount of terms for the Dcalc -> Lcalc translation without exceptions.
Changes
This PR mainly changes the scope bodies in Dcalc from being just an expression that wraps an
EAbsto a list of explicit let-bindings that are annotated with a kind, coming from the Scopelang -> Dcalc translations. The changes incompiler/dcalc/ast.ml*ripple into other files, but this is mostly straightforward refactorings that add some boilerplate in order to traverse the now irregular structure of the scope bodies.