cut --> hoist

binded representation

few doc
This commit is contained in:
Alain 2022-02-11 11:38:18 +01:00
parent 8834034094
commit cf28a58342
No known key found for this signature in database
GPG Key ID: D4C746AED35E1D17
2 changed files with 162 additions and 138 deletions

View File

@ -0,0 +1,135 @@
open Utils
module D = Ast
(** Alternative representation of the Dcalc Ast. It is currently used in the transformation without exceptions. We make heavy use of bindlib, binding each scope-let-variable and each scope explicitly. *)
(** In [Ast], [Ast.scope_lets] is defined as a list of kind, var, and boxed expression. This representation binds using bindlib the tail of the list with the variable defined in the let. *)
type scope_lets =
| Result of D.expr Pos.marked
| ScopeLet of {
scope_let_kind : D.scope_let_kind;
scope_let_typ : D.typ Pos.marked;
scope_let_expr : D.expr Pos.marked;
scope_let_next : (D.expr, scope_lets) Bindlib.binder;
scope_let_pos : Pos.t;
}
(** As a consequence, the scope_body contains only a result and input/output signature, as the other elements are stored inside the scope_let. The binder present is the argument of type [scope_body_input_struct]. *)
type scope_body = {
scope_body_input_struct : D.StructName.t;
scope_body_output_struct : D.StructName.t;
scope_body_result : (D.expr, scope_lets) Bindlib.binder;
}
(* finally, we do the same transformation for the whole program for the kinded lets. This permit us to use bindlib variables for scopes names. *)
type scopes =
| Nil
| ScopeDef of {
scope_name : D.ScopeName.t;
scope_body : scope_body;
scope_next : (D.expr, scopes) Bindlib.binder;
}
let union = D.VarMap.union (fun _ _ _ -> Some ())
(** free variables. For each construction, we define two free variables functions. The first one generates [unit D.VarMap.t], since there is no [D.VarSet.t]. And the second returns a list. The second one is better from pretty printing in debug. *)
let rec fv_scope_lets scope_lets =
match scope_lets with
| Result e -> D.fv e
| ScopeLet { scope_let_expr = e; scope_let_next = next; _ } ->
let v, body = Bindlib.unbind next in
union (D.fv e) (D.VarMap.remove v (fv_scope_lets body))
let fv_scope_body { scope_body_result = binder; _ } =
let v, body = Bindlib.unbind binder in
D.VarMap.remove v (fv_scope_lets body)
let rec fv_scopes scopes =
match scopes with
| Nil -> D.VarMap.empty
| ScopeDef { scope_body = body; scope_next = next; _ } ->
let v, next = Bindlib.unbind next in
union (D.VarMap.remove v (fv_scopes next)) (fv_scope_body body)
let _free_vars_scope_lets scope_lets = fv_scope_lets scope_lets |> D.VarMap.bindings |> List.map fst
let _free_vars_scope_body scope_body = fv_scope_body scope_body |> D.VarMap.bindings |> List.map fst
let free_vars_scopes scopes = fv_scopes scopes |> D.VarMap.bindings |> List.map fst
(** Actual transformation for scopes. It simply *)
let bind_scope_lets (acc : scope_lets Bindlib.box) (scope_let : D.scope_let) :
scope_lets Bindlib.box =
let pos = snd scope_let.D.scope_let_var in
Cli.debug_print
@@ Format.asprintf "binding let %a. Variable occurs = %b" Print.format_var
(fst scope_let.D.scope_let_var)
(Bindlib.occur (fst scope_let.D.scope_let_var) acc);
let binder = Bindlib.bind_var (fst scope_let.D.scope_let_var) acc in
Bindlib.box_apply2
(fun expr binder ->
Cli.debug_print
@@ Format.asprintf "free variables in expression: %a"
(Format.pp_print_list Print.format_var)
(D.free_vars expr);
ScopeLet
{
scope_let_kind = scope_let.D.scope_let_kind;
scope_let_typ = scope_let.D.scope_let_typ;
scope_let_expr = expr;
scope_let_next = binder;
scope_let_pos = pos;
})
scope_let.D.scope_let_expr binder
let bind_scope_body (body : D.scope_body) : scope_body Bindlib.box =
(* it is a fold_right and not a fold_left. *)
let body_result =
ListLabels.fold_right body.D.scope_body_lets
~init:(Bindlib.box_apply (fun e -> Result e) body.D.scope_body_result)
~f:(Fun.flip bind_scope_lets)
in
Cli.debug_print @@ Format.asprintf "binding arg %a" Print.format_var body.D.scope_body_arg;
let scope_body_result = Bindlib.bind_var body.D.scope_body_arg body_result in
Cli.debug_print
@@ Format.asprintf "isfinal term is closed: %b" (Bindlib.is_closed scope_body_result);
Bindlib.box_apply
(fun scope_body_result ->
Cli.debug_print
@@ Format.asprintf "rank of the final term: %i" (Bindlib.binder_rank scope_body_result);
{
scope_body_output_struct = body.D.scope_body_output_struct;
scope_body_input_struct = body.D.scope_body_input_struct;
scope_body_result;
})
scope_body_result
let bind_scope
((scope_name, scope_var, scope_body) : D.ScopeName.t * D.expr Bindlib.var * D.scope_body)
(acc : scopes Bindlib.box) : scopes Bindlib.box =
Bindlib.box_apply2
(fun scope_body scope_next -> ScopeDef { scope_name; scope_body; scope_next })
(bind_scope_body scope_body) (Bindlib.bind_var scope_var acc)
let bind_scopes (scopes : (D.ScopeName.t * D.expr Bindlib.var * D.scope_body) list) :
scopes Bindlib.box =
let result = ListLabels.fold_right scopes ~init:(Bindlib.box Nil) ~f:bind_scope in
Cli.debug_print
@@ Format.asprintf "free variable in the program : [%a]"
(Format.pp_print_list Print.format_var)
(free_vars_scopes (Bindlib.unbox result));
result

View File

@ -2,7 +2,7 @@ open Utils
module D = Dcalc.Ast
module A = Ast
(** hoisting *)
(*** hoisting *)
(** The main idea around this pass is to compile Dcalc to Lcalc without using [raise EmptyError] nor
[try _ with EmptyError -> _]. To do so, we use the same technique as in rust or erlang to handle
@ -10,41 +10,49 @@ module A = Ast
[try e1 with EmtpyError -> e2] as [match e1 with | None -> e2 | Some x -> x].
When doing this naively, this requires to add matches and Some constructor everywhere. We apply
here an other technique where we generate what we call `cuts`. Cuts are expression whom could
minimally [raise EmptyError]. For instance
here an other technique where we generate what we call `hoists`. Hoists are expression whom could
minimally [raise EmptyError]. For instance in
[let x = <e1, e2, ..., en| e_just :- e_cons> * 3 in x + 1], the sub-expression
[<e1, e2, ..., en| e_just :- e_cons>] can produce an empty error. So we make a cut with a new
[<e1, e2, ..., en| e_just :- e_cons>] can produce an empty error. So we make a hoist with a new
variable [y] linked to the Dcalc expression [<e1, e2, ..., en| e_just :- e_cons>], and we return
as the translated expression [let x = y * 3 in x + 1].
The compilation of expressions is found in the functions [translate_and_cut ctx e] and
[translate_expr ctx e]. Every option-generating expresion when calling [translate_and_cut] will
be cutted and later handled by the [translate_expr] function. Every other cases is found in the
translate_and_cut function. *)
The compilation of expressions is found in the functions [translate_and_hoist ctx e] and
[translate_expr ctx e]. Every option-generating expression when calling [translate_and_hoist] will
be hoisted and later handled by the [translate_expr] function. Every other cases is found in the
translate_and_hoist function. *)
type cuts = D.expr Pos.marked A.VarMap.t
(** cuts *)
type info = { expr : A.expr Pos.marked Bindlib.box; var : A.expr Bindlib.var; is_pure : bool }
(** information about the Dcalc variable : what is the corresponding LCalc variable; an expression
(** Hoists definition. It represent bindings between [A.Var.t] and [D.expr]. *)
type hoists = D.expr Pos.marked A.VarMap.t
(** Information about each encontered Dcalc variable is stored inside a context : what is the corresponding LCalc variable; an expression corresponding to the variable
build correctly using Bindlib, and a boolean `is_pure` indicating whenever the variable can be
an EmptyError and hence should be matched (false) or if it never can be EmptyError (true). *)
type ctx = info D.VarMap.t
(** information context about variables in the current scope *)
type info = { expr : A.expr Pos.marked Bindlib.box; var : A.expr Bindlib.var; is_pure : bool }
let pp_info (fmt : Format.formatter) (info : info) =
Format.fprintf fmt "{var: %a; is_pure: %b}" Print.format_var info.var info.is_pure
let pp_binding (fmt : Format.formatter) ((v, info) : D.Var.t * info) =
Format.fprintf fmt "%a:%a" Dcalc.Print.format_var v pp_info info
(** information context about variables in the current scope *)
type ctx = info D.VarMap.t
let pp_ctx (fmt : Format.formatter) (ctx : ctx) =
let pp_binding (fmt : Format.formatter) ((v, info) : D.Var.t * info) =
Format.fprintf fmt "%a: %a" Dcalc.Print.format_var v pp_info info
in
let pp_bindings =
Format.pp_print_list ~pp_sep:(fun fmt () -> Format.pp_print_string fmt "; ") pp_binding
in
Format.fprintf fmt "@[<2>[%a]@]" pp_bindings (D.VarMap.bindings ctx)
(** [find ~info n ctx] is a warpper to ocaml's Map.find that handle errors in a slightly better way. *)
let find ?(info : string = "none") (n : D.Var.t) (ctx : ctx) : info =
let _ =
@ -61,6 +69,7 @@ let find ?(info : string = "none") (n : D.Var.t) (ctx : ctx) : info =
Dcalc.Print.format_var n info)
Pos.no_pos
(** [add_var pos var is_pure ctx] add to the context [ctx] the Dcalc variable var, creating a unique corresponding variable in Lcalc, with the corresponding expression, and the boolean is_pure. It is usefull for debuging purposes as it printing each of the Dcalc/Lcalc variable pairs. *)
let add_var (pos : Pos.t) (var : D.Var.t) (is_pure : bool) (ctx : ctx) : ctx =
let new_var = A.Var.make (Bindlib.name_of var, pos) in
let expr = A.make_var (new_var, pos) in
@ -70,126 +79,6 @@ let add_var (pos : Pos.t) (var : D.Var.t) (is_pure : bool) (ctx : ctx) : ctx =
D.VarMap.update var (fun _ -> Some { expr; var = new_var; is_pure }) ctx
(* internal representation of scopes. We make here heavy use of bindlib. *)
type scope_lets =
| Result of D.expr Pos.marked
| ScopeLet of {
scope_let_kind : D.scope_let_kind;
scope_let_typ : D.typ Pos.marked;
scope_let_expr : D.expr Pos.marked;
scope_let_next : (D.expr, scope_lets) Bindlib.binder;
scope_let_pos : Pos.t;
}
type scope_body = {
scope_body_input_struct : D.StructName.t;
scope_body_output_struct : D.StructName.t;
scope_body_result : (D.expr, scope_lets) Bindlib.binder;
}
type scopes =
| Nil
| ScopeDef of {
scope_name : D.ScopeName.t;
scope_body : scope_body;
scope_next : (D.expr, scopes) Bindlib.binder;
}
let union = D.VarMap.union (fun _ _ _ -> Some ())
let rec fv_scope_lets scope_lets =
match scope_lets with
| Result e -> D.fv e
| ScopeLet { scope_let_expr = e; scope_let_next = next; _ } ->
let v, body = Bindlib.unbind next in
union (D.fv e) (D.VarMap.remove v (fv_scope_lets body))
let fv_scope_body { scope_body_result = binder; _ } =
let v, body = Bindlib.unbind binder in
D.VarMap.remove v (fv_scope_lets body)
let rec fv_scopes scopes =
match scopes with
| Nil -> D.VarMap.empty
| ScopeDef { scope_body = body; scope_next = next; _ } ->
let v, next = Bindlib.unbind next in
union (D.VarMap.remove v (fv_scopes next)) (fv_scope_body body)
let _free_vars_scope_lets scope_lets = fv_scope_lets scope_lets |> D.VarMap.bindings |> List.map fst
let _free_vars_scope_body scope_body = fv_scope_body scope_body |> D.VarMap.bindings |> List.map fst
let free_vars_scopes scopes = fv_scopes scopes |> D.VarMap.bindings |> List.map fst
let bind_scope_lets (acc : scope_lets Bindlib.box) (scope_let : D.scope_let) :
scope_lets Bindlib.box =
let pos = snd scope_let.D.scope_let_var in
Cli.debug_print
@@ Format.asprintf "binding let %a. Variable occurs = %b" Dcalc.Print.format_var
(fst scope_let.D.scope_let_var)
(Bindlib.occur (fst scope_let.D.scope_let_var) acc);
let binder = Bindlib.bind_var (fst scope_let.D.scope_let_var) acc in
Bindlib.box_apply2
(fun expr binder ->
Cli.debug_print
@@ Format.asprintf "free variables in expression: %a"
(Format.pp_print_list Dcalc.Print.format_var)
(D.free_vars expr);
ScopeLet
{
scope_let_kind = scope_let.D.scope_let_kind;
scope_let_typ = scope_let.D.scope_let_typ;
scope_let_expr = expr;
scope_let_next = binder;
scope_let_pos = pos;
})
scope_let.D.scope_let_expr binder
let bind_scope_body (body : D.scope_body) : scope_body Bindlib.box =
let body_result =
ListLabels.fold_right body.D.scope_body_lets
~init:(Bindlib.box_apply (fun e -> Result e) body.D.scope_body_result)
~f:(Fun.flip bind_scope_lets)
in
Cli.debug_print @@ Format.asprintf "binding arg %a" Dcalc.Print.format_var body.D.scope_body_arg;
let scope_body_result = Bindlib.bind_var body.D.scope_body_arg body_result in
Cli.debug_print
@@ Format.asprintf "isfinal term is closed: %b" (Bindlib.is_closed scope_body_result);
Bindlib.box_apply
(fun scope_body_result ->
Cli.debug_print
@@ Format.asprintf "rank of the final term: %i" (Bindlib.binder_rank scope_body_result);
{
scope_body_output_struct = body.D.scope_body_output_struct;
scope_body_input_struct = body.D.scope_body_input_struct;
scope_body_result;
})
scope_body_result
let bind_scope
((scope_name, scope_var, scope_body) : D.ScopeName.t * D.expr Bindlib.var * D.scope_body)
(acc : scopes Bindlib.box) : scopes Bindlib.box =
Bindlib.box_apply2
(fun scope_body scope_next -> ScopeDef { scope_name; scope_body; scope_next })
(bind_scope_body scope_body) (Bindlib.bind_var scope_var acc)
let bind_scopes (scopes : (D.ScopeName.t * D.expr Bindlib.var * D.scope_body) list) :
scopes Bindlib.box =
let result = ListLabels.fold_right scopes ~init:(Bindlib.box Nil) ~f:bind_scope in
Cli.debug_print
@@ Format.asprintf "free variable in the program : [%a]"
(Format.pp_print_list Dcalc.Print.format_var)
(free_vars_scopes (Bindlib.unbox result));
result
(** [tau' = translate_typ tau] translate the a dcalc type into a lcalc type.
Since positions where there is thunked expressions is exactly where we will put option