Start to refactor Lcalc AST (WIP) [skip ci]

This commit is contained in:
Denis Merigoux 2022-04-15 12:16:44 +02:00
parent 88a522d120
commit 8ce81fedaa
No known key found for this signature in database
GPG Key ID: EE99DCFA365C3EE3
5 changed files with 214 additions and 27 deletions

View File

@ -50,13 +50,91 @@ type expr =
| ERaise of except
| ECatch of expr Pos.marked * except * expr Pos.marked
type scope_body = {
scope_body_name : Dcalc.Ast.ScopeName.t;
scope_body_var : expr Bindlib.var;
scope_body_expr : expr Pos.marked;
}
type program = { decl_ctx : Dcalc.Ast.decl_ctx; scopes : expr Dcalc.Ast.scopes }
type program = { decl_ctx : Dcalc.Ast.decl_ctx; scopes : scope_body list }
let evar (v : expr Bindlib.var) (pos : Pos.t) : expr Pos.marked Bindlib.box =
Bindlib.box_apply (fun v' -> (v', pos)) (Bindlib.box_var v)
let etuple
(args : expr Pos.marked Bindlib.box list)
(s : Dcalc.Ast.StructName.t option)
(pos : Pos.t) : expr Pos.marked Bindlib.box =
Bindlib.box_apply
(fun args -> (ETuple (args, s), pos))
(Bindlib.box_list args)
let etupleaccess
(e1 : expr Pos.marked Bindlib.box)
(i : int)
(s : Dcalc.Ast.StructName.t option)
(typs : Dcalc.Ast.typ Pos.marked list)
(pos : Pos.t) : expr Pos.marked Bindlib.box =
Bindlib.box_apply (fun e1 -> (ETupleAccess (e1, i, s, typs), pos)) e1
let einj
(e1 : expr Pos.marked Bindlib.box)
(i : int)
(e_name : Dcalc.Ast.EnumName.t)
(typs : Dcalc.Ast.typ Pos.marked list)
(pos : Pos.t) : expr Pos.marked Bindlib.box =
Bindlib.box_apply (fun e1 -> (EInj (e1, i, e_name, typs), pos)) e1
let ematch
(arg : expr Pos.marked Bindlib.box)
(arms : expr Pos.marked Bindlib.box list)
(e_name : Dcalc.Ast.EnumName.t)
(pos : Pos.t) : expr Pos.marked Bindlib.box =
Bindlib.box_apply2
(fun arg arms -> (EMatch (arg, arms, e_name), pos))
arg (Bindlib.box_list arms)
let earray (args : expr Pos.marked Bindlib.box list) (pos : Pos.t) :
expr Pos.marked Bindlib.box =
Bindlib.box_apply (fun args -> (EArray args, pos)) (Bindlib.box_list args)
let elit (l : lit) (pos : Pos.t) : expr Pos.marked Bindlib.box =
Bindlib.box (ELit l, pos)
let eabs
(binder : (expr, expr Pos.marked) Bindlib.mbinder Bindlib.box)
(pos_binder : Pos.t)
(typs : Dcalc.Ast.typ Pos.marked list)
(pos : Pos.t) : expr Pos.marked Bindlib.box =
Bindlib.box_apply
(fun binder -> (EAbs ((binder, pos_binder), typs), pos))
binder
let eapp
(e1 : expr Pos.marked Bindlib.box)
(args : expr Pos.marked Bindlib.box list)
(pos : Pos.t) : expr Pos.marked Bindlib.box =
Bindlib.box_apply2
(fun e1 args -> (EApp (e1, args), pos))
e1 (Bindlib.box_list args)
let eassert (e1 : expr Pos.marked Bindlib.box) (pos : Pos.t) :
expr Pos.marked Bindlib.box =
Bindlib.box_apply (fun e1 -> (EAssert e1, pos)) e1
let eop (op : Dcalc.Ast.operator) (pos : Pos.t) : expr Pos.marked Bindlib.box =
Bindlib.box (EOp op, pos)
let eraise (e1 : except) (pos : Pos.t) : expr Pos.marked Bindlib.box =
Bindlib.box (ERaise e1, pos)
let ecatch
(e1 : expr Pos.marked Bindlib.box)
(exn : except)
(e2 : expr Pos.marked Bindlib.box)
(pos : Pos.t) : expr Pos.marked Bindlib.box =
Bindlib.box_apply2 (fun e1 e2 -> (ECatch (e1, exn, e2), pos)) e1 e2
let eifthenelse
(e1 : expr Pos.marked Bindlib.box)
(e2 : expr Pos.marked Bindlib.box)
(e3 : expr Pos.marked Bindlib.box)
(pos : Pos.t) : expr Pos.marked Bindlib.box =
Bindlib.box_apply3 (fun e1 e2 e3 -> (EIfThenElse (e1, e2, e3), pos)) e1 e2 e3
module Var = struct
type t = expr Bindlib.var
@ -74,6 +152,40 @@ module VarSet = Set.Make (Var)
type vars = expr Bindlib.mvar
let map_expr
(ctx : 'a)
~(f : 'a -> expr Pos.marked -> expr Pos.marked Bindlib.box)
(e : expr Pos.marked) : expr Pos.marked Bindlib.box =
match Pos.unmark e with
| EVar (v, _pos) -> evar v (Pos.get_position e)
| EApp (e1, args) ->
eapp (f ctx e1) (List.map (f ctx) args) (Pos.get_position e)
| EAbs ((binder, binder_pos), typs) ->
eabs
(Bindlib.box_mbinder (f ctx) binder)
binder_pos typs (Pos.get_position e)
| ETuple (args, s) -> etuple (List.map (f ctx) args) s (Pos.get_position e)
| ETupleAccess (e1, n, s_name, typs) ->
etupleaccess ((f ctx) e1) n s_name typs (Pos.get_position e)
| EInj (e1, i, e_name, typs) ->
einj ((f ctx) e1) i e_name typs (Pos.get_position e)
| EMatch (arg, arms, e_name) ->
ematch ((f ctx) arg) (List.map (f ctx) arms) e_name (Pos.get_position e)
| EArray args -> earray (List.map (f ctx) args) (Pos.get_position e)
| ELit l -> elit l (Pos.get_position e)
| EAssert e1 -> eassert ((f ctx) e1) (Pos.get_position e)
| EOp op -> Bindlib.box (EOp op, Pos.get_position e)
| ERaise exn -> eraise exn (Pos.get_position e)
| EIfThenElse (e1, e2, e3) ->
eifthenelse ((f ctx) e1) ((f ctx) e2) ((f ctx) e3) (Pos.get_position e)
| ECatch (e1, exn, e2) ->
ecatch (f ctx e1) exn (f ctx e2) (Pos.get_position e)
(** See [Bindlib.box_term] documentation for why we are doing that. *)
let box_expr (e : expr Pos.marked) : expr Pos.marked Bindlib.box =
let rec id_t () e = map_expr () ~f:id_t e in
id_t () e
let make_var ((x, pos) : Var.t Pos.marked) : expr Pos.marked Bindlib.box =
Bindlib.box_apply (fun x -> (x, pos)) (Bindlib.box_var x)
@ -97,8 +209,8 @@ let make_let_in
(x : Var.t)
(tau : D.typ Pos.marked)
(e1 : expr Pos.marked Bindlib.box)
(e2 : expr Pos.marked Bindlib.box) : expr Pos.marked Bindlib.box =
let pos = Pos.get_position (Bindlib.unbox e2) in
(e2 : expr Pos.marked Bindlib.box)
(pos : Pos.t) : expr Pos.marked Bindlib.box =
make_app (make_abs (Array.of_list [ x ]) e2 pos [ tau ] pos) [ e1 ] pos
let make_multiple_let_in

View File

@ -64,13 +64,7 @@ type expr =
| ERaise of except
| ECatch of expr Pos.marked * except * expr Pos.marked
type scope_body = {
scope_body_name : Dcalc.Ast.ScopeName.t;
scope_body_var : expr Bindlib.var;
scope_body_expr : expr Pos.marked;
}
type program = { decl_ctx : Dcalc.Ast.decl_ctx; scopes : scope_body list }
type program = { decl_ctx : Dcalc.Ast.decl_ctx; scopes : expr Dcalc.Ast.scopes }
(** {1 Variable helpers} *)
@ -87,6 +81,78 @@ module VarSet : Set.S with type elt = Var.t
type vars = expr Bindlib.mvar
type binder = (expr, expr Pos.marked) Bindlib.binder
(** {1 Boxed constructors}*)
val evar : expr Bindlib.var -> Pos.t -> expr Pos.marked Bindlib.box
val etuple :
expr Pos.marked Bindlib.box list ->
Dcalc.Ast.StructName.t option ->
Pos.t ->
expr Pos.marked Bindlib.box
val etupleaccess :
expr Pos.marked Bindlib.box ->
int ->
Dcalc.Ast.StructName.t option ->
Dcalc.Ast.typ Pos.marked list ->
Pos.t ->
expr Pos.marked Bindlib.box
val einj :
expr Pos.marked Bindlib.box ->
int ->
Dcalc.Ast.EnumName.t ->
Dcalc.Ast.typ Pos.marked list ->
Pos.t ->
expr Pos.marked Bindlib.box
val ematch :
expr Pos.marked Bindlib.box ->
expr Pos.marked Bindlib.box list ->
Dcalc.Ast.EnumName.t ->
Pos.t ->
expr Pos.marked Bindlib.box
val earray :
expr Pos.marked Bindlib.box list -> Pos.t -> expr Pos.marked Bindlib.box
val elit : lit -> Pos.t -> expr Pos.marked Bindlib.box
val eabs :
(expr, expr Pos.marked) Bindlib.mbinder Bindlib.box ->
Pos.t ->
Dcalc.Ast.typ Pos.marked list ->
Pos.t ->
expr Pos.marked Bindlib.box
val eapp :
expr Pos.marked Bindlib.box ->
expr Pos.marked Bindlib.box list ->
Pos.t ->
expr Pos.marked Bindlib.box
val eassert :
expr Pos.marked Bindlib.box -> Pos.t -> expr Pos.marked Bindlib.box
val eop : Dcalc.Ast.operator -> Pos.t -> expr Pos.marked Bindlib.box
val eifthenelse :
expr Pos.marked Bindlib.box ->
expr Pos.marked Bindlib.box ->
expr Pos.marked Bindlib.box ->
Pos.t ->
expr Pos.marked Bindlib.box
val ecatch :
expr Pos.marked Bindlib.box ->
except ->
expr Pos.marked Bindlib.box ->
Pos.t ->
expr Pos.marked Bindlib.box
val eraise : except -> Pos.t -> expr Pos.marked Bindlib.box
(** {1 Language terms construction}*)
val make_var : Var.t Pos.marked -> expr Pos.marked Bindlib.box
@ -110,6 +176,7 @@ val make_let_in :
Dcalc.Ast.typ Pos.marked ->
expr Pos.marked Bindlib.box ->
expr Pos.marked Bindlib.box ->
Pos.t ->
expr Pos.marked Bindlib.box
val make_multiple_let_in :
@ -147,6 +214,8 @@ val make_matchopt :
(** [e' = make_matchopt'' pos v e e_none e_some] Builds the term corresponding
to [match e with | None -> fun () -> e_none |Some -> fun v -> e_some]. *)
val box_expr : expr Pos.marked -> expr Pos.marked Bindlib.box
(** {1 Special symbols}*)
val handle_default : Var.t

View File

@ -181,7 +181,8 @@ let rec closure_conversion_expr (ctx : ctx) (e : expr Pos.marked) :
(Bindlib.box_list
(List.map
(fun extra_var -> Bindlib.box_var extra_var)
extra_vars_list))),
extra_vars_list)))
(Pos.get_position e),
extra_vars )
| EApp ((EOp op, pos_op), args) ->
(* This corresponds to an operator call, which we don't want to
@ -241,8 +242,11 @@ let rec closure_conversion_expr (ctx : ctx) (e : expr Pos.marked) :
Pos.get_position e ))
(Bindlib.box_var code_var) (Bindlib.box_var env_var)
(Bindlib.box_list new_args))
(Pos.get_position e)
in
( make_let_in env_var (Dcalc.Ast.TAny, Pos.get_position e) new_e1 call_expr,
( make_let_in env_var
(Dcalc.Ast.TAny, Pos.get_position e)
new_e1 call_expr (Pos.get_position e),
free_vars )
| EAssert e1 ->
let new_e1, free_vars = closure_conversion_expr ctx e1 in

View File

@ -74,8 +74,8 @@ let format_var (fmt : Format.formatter) (v : Var.t) : unit =
Format.fprintf fmt "%s_%d" (Bindlib.name_of v) (Bindlib.uid_of v)
let rec format_expr
(ctx : Dcalc.Ast.decl_ctx)
?(debug : bool = false)
(ctx : Dcalc.Ast.decl_ctx)
(fmt : Format.formatter)
(e : expr Pos.marked) : unit =
let format_expr = format_expr ctx ~debug in
@ -204,11 +204,13 @@ let rec format_expr
format_punctuation "(" format_expr e' format_punctuation ")"
let format_scope
(decl_ctx : Dcalc.Ast.decl_ctx)
?(debug : bool = false)
(ctx : Dcalc.Ast.decl_ctx)
(fmt : Format.formatter)
(body : scope_body) : unit =
Format.fprintf fmt "@[<hov 2>%a %a %a@ %a@]" format_keyword "let" format_var
body.scope_body_var format_punctuation "="
(format_expr decl_ctx ~debug)
body.scope_body_expr
((n, s) : Dcalc.Ast.ScopeName.t * Ast.expr Dcalc.Ast.scope_body) : unit =
Format.fprintf fmt "@[<hov 2>%a %a =@ %a@]" format_keyword "let"
Dcalc.Ast.ScopeName.format_t n (format_expr ctx ~debug)
(Bindlib.unbox
(Dcalc.Ast.build_whole_scope_expr ~make_abs:Ast.make_abs
~make_let_in:Ast.make_let_in ~box_expr:Ast.box_expr ctx s
(Pos.get_position (Dcalc.Ast.ScopeName.get_info n))))

View File

@ -28,15 +28,15 @@ val format_var : Format.formatter -> Ast.Var.t -> unit
val format_exception : Format.formatter -> Ast.except -> unit
val format_expr :
Dcalc.Ast.decl_ctx ->
?debug:bool ->
Dcalc.Ast.decl_ctx ->
Format.formatter ->
Ast.expr Pos.marked ->
unit
val format_scope :
Dcalc.Ast.decl_ctx ->
?debug:bool ->
Dcalc.Ast.decl_ctx ->
Format.formatter ->
Ast.scope_body ->
Dcalc.Ast.ScopeName.t * Ast.expr Dcalc.Ast.scope_body ->
unit