Scopelang to dcalc done [skip ci]

This commit is contained in:
Denis Merigoux 2021-12-09 18:42:36 +01:00
parent fcf7c31279
commit 3a21bec4b1
No known key found for this signature in database
GPG Key ID: EE99DCFA365C3EE3
3 changed files with 46 additions and 28 deletions

View File

@ -131,8 +131,8 @@ type scope_let_kind =
| ScopeVarDefinition
| SubScopeVarDefinition
| CallingSubScope
| Assertion
| DestructuringSubScopeResults
| Assertion
type scope_let = {
scope_let_var : expr Bindlib.var Pos.marked;

View File

@ -133,13 +133,15 @@ type decl_ctx = { ctx_enums : enum_ctx; ctx_structs : struct_ctx }
type binder = (expr, expr Pos.marked) Bindlib.binder
(** This kind annotation signals that the let-binding respects a structural invariant. These
invariants concern the shape of the expression in the let-binding, and are documented below. *)
type scope_let_kind =
| DestructuringInputStruct
| ScopeVarDefinition
| SubScopeVarDefinition
| CallingSubScope
| Assertion
| DestructuringSubScopeResults
| DestructuringInputStruct (** [let x = input.field]*)
| ScopeVarDefinition (** [let x = error_on_empty e]*)
| 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]*)
type scope_let = {
scope_let_var : expr Bindlib.var Pos.marked;
@ -147,8 +149,14 @@ type scope_let = {
scope_let_typ : typ Pos.marked;
scope_let_expr : expr Pos.marked;
}
(** A scope let-binding has all the information necessary to make a proper let-binding expression,
plus an annotation for the kind of the let-binding that comes from the compilation of a
{!module: Scopelang.Ast} statement. *)
type scope_body = { scope_body_lets : scope_let list; scope_result : expr Pos.marked }
(** Instead of being a single expression, we give a little more ad-hoc structure to the scope body
by decomposing it in an ordered list of let-bindings, and a result expression that uses the
let-binded variables. *)
type program = { decl_ctx : decl_ctx; scopes : (ScopeName.t * expr Bindlib.var * scope_body) list }

View File

@ -425,34 +425,44 @@ let translate_rule (ctx : ctx) (rule : Ast.rule)
Ast.ScopeName.get_info subname;
]
in
let result_tuple_var = Dcalc.Ast.Var.make ("result", pos_sigma) in
let results_bindings_xs = List.map (fun (_, _, v) -> v) all_subscope_vars_dcalc in
let results_bindings_taus =
List.map (fun (_, tau, _) -> (tau, pos_sigma)) all_subscope_vars_dcalc
in
let results_bindings_e1s =
List.mapi
(fun i _ ->
Bindlib.box_apply
(fun r ->
( Dcalc.Ast.ETupleAccess
( r,
i,
Some called_scope_return_struct,
List.map (fun (_, t, _) -> (t, pos_sigma)) all_subscope_vars_dcalc ),
pos_sigma ))
(Dcalc.Ast.make_var (result_tuple_var, pos_sigma)))
all_subscope_vars_dcalc
in
let result_tuple_typ =
( Dcalc.Ast.TTuple
( List.map (fun (_, tau, _) -> (tau, pos_sigma)) all_subscope_vars_dcalc,
Some called_scope_return_struct ),
pos_sigma )
in
( [ ([ result_tuple_var ], pos_sigma); (results_bindings_xs, pos_sigma) ],
[ [ result_tuple_typ ]; results_bindings_taus ],
[ [ call_expr ]; results_bindings_e1s ],
let call_scope_let =
{
Dcalc.Ast.scope_let_var = (result_tuple_var, pos_sigma);
Dcalc.Ast.scope_let_kind = Dcalc.Ast.CallingSubScope;
Dcalc.Ast.scope_let_typ = result_tuple_typ;
Dcalc.Ast.scope_let_expr = Bindlib.unbox call_expr;
}
in
let result_bindings_lets =
List.mapi
(fun i (_, tau, v) ->
{
Dcalc.Ast.scope_let_var = (v, pos_sigma);
Dcalc.Ast.scope_let_typ = (tau, pos_sigma);
Dcalc.Ast.scope_let_kind = Dcalc.Ast.DestructuringSubScopeResults;
Dcalc.Ast.scope_let_expr =
Bindlib.unbox
(Bindlib.box_apply
(fun r ->
( Dcalc.Ast.ETupleAccess
( r,
i,
Some called_scope_return_struct,
List.map (fun (_, t, _) -> (t, pos_sigma)) all_subscope_vars_dcalc ),
pos_sigma ))
(Dcalc.Ast.make_var (result_tuple_var, pos_sigma)));
})
all_subscope_vars_dcalc
in
( call_scope_let :: result_bindings_lets,
{
ctx with
subscope_vars =