Skip to content

Commit

Permalink
Merge pull request #958 from hacspec/ast_builder
Browse files Browse the repository at this point in the history
feat(engine): add module `ast_builder`
  • Loading branch information
maximebuyse authored Oct 3, 2024
2 parents 4a023d0 + b5ada80 commit 2a2445f
Show file tree
Hide file tree
Showing 19 changed files with 302 additions and 148 deletions.
64 changes: 64 additions & 0 deletions engine/lib/ast_builder.ml
Original file line number Diff line number Diff line change
@@ -0,0 +1,64 @@
open! Prelude
open! Ast

module Make (F : Features.T) = struct
module AST = Ast.Make (F)
open AST

open struct
module Gen = Ast_builder_generated.Make (F)
end

module type SPAN = Gen.SPAN

include Gen.Explicit

module NoSpan = struct
let ty_tuple (types : ty list) : ty =
let ident = `TupleType (List.length types) in
let args = List.map ~f:(fun typ -> GType typ) types in
TApp { ident; args }

let ty_tuple_or_id : ty list -> ty = function
| [ ty ] -> ty
| types -> ty_tuple types
end

include NoSpan

module Explicit = struct
let ty_unit : ty = TApp { ident = `TupleType 0; args = [] }
let expr_unit = expr_GlobalVar (`TupleCons 0) ~typ:ty_unit
let pat_PBinding ~typ = pat_PBinding ~inner_typ:typ ~typ

let arm ~span arm_pat ?(guard = None) body =
{ arm = { arm_pat; body; guard }; span }
end

include Explicit

module Make0 (Span : Gen.SPAN) = struct
open! Span
include Gen.Make (Span)
include NoSpan

let pat_PBinding = Explicit.pat_PBinding ~span
let expr_unit = expr_unit ~span
let arm ?(guard = None) = arm ~span ?guard
end

module type S = module type of Make0 (struct
let span = failwith "dummy"
end)

module Make (Span : sig
val span : span
end) : S =
Make0 (Span)

let make : span -> (module S) =
fun span : (module S) ->
(module Make0 (struct
let span = span
end))
end
15 changes: 6 additions & 9 deletions engine/lib/ast_utils.ml
Original file line number Diff line number Diff line change
Expand Up @@ -49,6 +49,7 @@ module Make (F : Features.T) = struct
open AST
module TypedLocalIdent = TypedLocalIdent (AST)
module Visitors = Ast_visitors.Make (F)
module M = Ast_builder.Make (F)

module Expect = struct
let mut_borrow (e : expr) : expr option =
Expand Down Expand Up @@ -801,19 +802,13 @@ module Make (F : Features.T) = struct
let make_tuple_typ (tuple : ty list) : ty =
match tuple with [ ty ] -> ty | _ -> make_tuple_typ' tuple

let make_wild_pat (typ : ty) (span : span) : pat = { p = PWild; span; typ }

let make_arm (arm_pat : pat) (body : expr) ?(guard : guard option = None)
(span : span) : arm =
{ arm = { arm_pat; body; guard }; span }

let make_unit_param (span : span) : param =
let typ = unit_typ in
let pat = make_wild_pat typ span in
let pat = M.pat_PWild ~typ ~span in
{ pat; typ; typ_span = None; attrs = [] }

let make_seq (e1 : expr) (e2 : expr) : expr =
make_let (make_wild_pat e1.typ e1.span) e1 e2
make_let (M.pat_PWild ~typ:e1.typ ~span:e1.span) e1 e2

let make_tuple_field_pat (len : int) (nth : int) (pat : pat) : field_pat =
{ field = `TupleField (nth + 1, len); pat }
Expand Down Expand Up @@ -918,7 +913,9 @@ module Make (F : Features.T) = struct

let make_closure (params : pat list) (body : expr) (span : span) : expr =
let params =
match params with [] -> [ make_wild_pat unit_typ span ] | _ -> params
match params with
| [] -> [ M.pat_PWild ~typ:unit_typ ~span ]
| _ -> params
in
let e = Closure { params; body; captures = [] } in
{ e; typ = TArrow (List.map ~f:(fun p -> p.typ) params, body.typ); span }
Expand Down
13 changes: 12 additions & 1 deletion engine/lib/dune
Original file line number Diff line number Diff line change
Expand Up @@ -55,7 +55,18 @@
ast_visitors.ml
(with-stdin-from
%{ast}
(run generate_visitors)))))
(run generate_from_ast visitors)))))

(rule
(target ast_builder_generated.ml)
(deps
(:ast ast.ml))
(action
(with-stdout-to
ast_builder_generated.ml
(with-stdin-from
%{ast}
(run generate_from_ast ast_builder)))))

(rule
(target concrete_ident_generated.ml)
Expand Down
13 changes: 7 additions & 6 deletions engine/lib/import_thir.ml
Original file line number Diff line number Diff line change
Expand Up @@ -428,11 +428,11 @@ end) : EXPR = struct
{
arms =
[
U.make_arm lhs body lhs_body_span;
U.make_arm
U.M.arm lhs body ~span:lhs_body_span;
U.M.arm
{ p = PWild; span = else_block.span; typ = lhs.typ }
{ else_block with typ = body.typ }
else_block.span;
~span:else_block.span;
];
scrutinee = rhs;
}
Expand Down Expand Up @@ -488,10 +488,10 @@ end) : EXPR = struct
Option.value ~default:(U.unit_expr span)
@@ Option.map ~f:c_expr else_opt
in
let arm_then = U.make_arm arm_pat then_ then_.span in
let arm_then = U.M.arm arm_pat then_ ~span:then_.span in
let arm_else =
let arm_pat = { arm_pat with p = PWild } in
U.make_arm arm_pat else_ else_.span
U.M.arm arm_pat else_ ~span:else_.span
in
Match { scrutinee; arms = [ arm_then; arm_else ] }
| If { cond; else_opt; then'; _ } ->
Expand Down Expand Up @@ -726,7 +726,8 @@ end) : EXPR = struct
List.filter_map ~f:(fun p -> Option.map ~f:c_pat p.pat) params
in
let params =
if List.is_empty params then [ U.make_wild_pat U.unit_typ span ]
if List.is_empty params then
[ U.M.pat_PWild ~typ:U.M.ty_unit ~span ]
else params
in
let body = c_expr body in
Expand Down
2 changes: 1 addition & 1 deletion engine/lib/phases/phase_direct_and_mut.ml
Original file line number Diff line number Diff line change
Expand Up @@ -196,7 +196,7 @@ struct
List.map
~f:(function
| Some (var, _), (ty, span) -> UB.make_var_pat var ty span
| None, (ty, span) -> UB.make_wild_pat ty span)
| None, (typ, span) -> UB.M.pat_PWild ~typ ~span)
mutargs
@ out
|> UB.make_tuple_pat
Expand Down
139 changes: 45 additions & 94 deletions engine/lib/phases/phase_drop_match_guards.ml
Original file line number Diff line number Diff line change
Expand Up @@ -84,7 +84,7 @@ module%inlined_contents Make (F : Features.T) = struct
match remaining with
| [] -> treated
| { arm = { arm_pat; body; guard = None }; span } :: remaining ->
let new_arm : B.arm = UB.make_arm (dpat arm_pat) (dexpr body) span in
let new_arm : B.arm = UB.M.arm (dpat arm_pat) (dexpr body) ~span in
transform_arms scrutinee remaining (new_arm :: treated)
(* Matches an arm `arm_pat if let lhs = rhs => body` *)
(* And rewrites to `_ => match <option_match> {Some(x) => x, None => match scrutinee {<treated>} }` *)
Expand All @@ -101,6 +101,7 @@ module%inlined_contents Make (F : Features.T) = struct
span;
}
:: remaining ->
let module MS = (val UB.M.make guard_span) in
let result_typ = dty span body.typ in
let opt_result_typ : B.ty =
TApp
Expand All @@ -126,115 +127,65 @@ module%inlined_contents Make (F : Features.T) = struct
[ { field = `TupleField (0, 1); pat = b } ] )
| None -> (Core__option__Option__None, [])
in
{
p =
PConstruct
{
name =
Global_ident.of_name
(Constructor { is_struct = false })
name;
args;
is_record = false;
is_struct = false;
};
span = guard_span;
typ = opt_result_typ;
}
MS.pat_PConstruct
~name:
(Global_ident.of_name (Constructor { is_struct = false }) name)
~args ~is_record:false ~is_struct:false ~typ:opt_result_typ
in

let expr_none = mk_opt_expr None in

(* This is the nested pattern matching equivalent to the guard *)
(* Example: .. if let pat = rhs => body *)
(* Rewrites with match rhs { pat => Some(body), _ => None }*)
let guard_match : B.expr' =
Match
{
scrutinee = dexpr rhs;
arms =
[
UB.make_arm (dpat lhs)
(mk_opt_expr (Some (dexpr body)))
span;
UB.make_arm
(UB.make_wild_pat (dty guard_span lhs.typ) guard_span)
expr_none guard_span;
];
}
let guard_match : B.expr =
MS.expr_Match ~scrutinee:(dexpr rhs)
~arms:
[
UB.M.arm (dpat lhs) (mk_opt_expr (Some (dexpr body))) ~span;
MS.arm (MS.pat_PWild ~typ:(dty guard_span lhs.typ)) expr_none;
]
~typ:opt_result_typ
in

(* `r` corresponds to `option_match` in the example above *)
let r : B.expr =
{
e =
Match
{
scrutinee;
arms =
[
UB.make_arm (dpat arm_pat)
{
e = guard_match;
span = guard_span;
typ = opt_result_typ;
}
guard_span;
UB.make_arm
(UB.make_wild_pat
(dty guard_span arm_pat.typ)
guard_span)
expr_none guard_span;
];
};
span = guard_span;
typ = opt_result_typ;
}
MS.expr_Match ~scrutinee
~arms:
[
MS.arm (dpat arm_pat) guard_match;
MS.arm
(UB.M.pat_PWild
~typ:(dty guard_span arm_pat.typ)
~span:guard_span)
expr_none;
]
~typ:opt_result_typ
in
let id = UB.fresh_local_ident_in [] "x" in
let new_body : B.expr =
{
e =
Match
{
scrutinee = r;
arms =
[
UB.make_arm
(mk_opt_pattern
(Some
{
p =
PBinding
{
mut = Immutable;
mode = ByValue;
var = id;
typ = result_typ;
subpat = None;
};
span;
typ = result_typ;
}))
{ e = LocalVar id; span; typ = result_typ }
guard_span;
UB.make_arm (mk_opt_pattern None)
{
e = maybe_simplified_match scrutinee treated;
span = guard_span;
typ = result_typ;
}
guard_span;
];
};
span = guard_span;
typ = result_typ;
}
MS.expr_Match ~scrutinee:r
~arms:
[
MS.arm
(mk_opt_pattern
(Some
(MS.pat_PBinding ~mut:Immutable ~mode:ByValue ~var:id
~typ:result_typ ~subpat:None)))
{ e = LocalVar id; span; typ = result_typ };
MS.arm (mk_opt_pattern None)
{
e = maybe_simplified_match scrutinee treated;
span = guard_span;
typ = result_typ;
};
]
~typ:result_typ
in
let new_arm : B.arm =
UB.make_arm
(UB.make_wild_pat (dty span arm_pat.typ) span)
new_body span
UB.M.arm
(UB.M.pat_PWild ~typ:(dty span arm_pat.typ) ~span)
new_body ~span
in
transform_arms scrutinee remaining [ new_arm ]
[@@inline_ands
Expand Down
25 changes: 10 additions & 15 deletions engine/lib/phases/phase_functionalize_loops.ml
Original file line number Diff line number Diff line change
Expand Up @@ -158,6 +158,8 @@ struct

let rec dexpr_unwrapped (expr : A.expr) : B.expr =
let span = expr.span in
let module M = UB.M in
let module MS = (val M.make span) in
match expr.e with
| Loop
{
Expand All @@ -178,9 +180,8 @@ struct
| Some (f, args, typ) ->
let invariant : B.expr =
let default =
let span = expr.span in
let pat = UB.make_wild_pat typ span in
(pat, B.{ e = Literal (Bool true); typ = TBool; span })
let pat = MS.pat_PWild ~typ in
(pat, MS.expr_Literal ~typ:TBool (Bool true))
in
let pat, invariant = Option.value ~default invariant in
UB.make_closure [ bpat; pat ] invariant invariant.span
Expand All @@ -204,20 +205,14 @@ struct
let bpat = dpat bpat in
let init = dexpr init in
let condition : B.expr =
let e : B.expr' =
Closure { params = [ bpat ]; body = condition; captures = [] }
in
let typ : B.ty = TArrow ([ bpat.typ ], condition.typ) in
let span = condition.span in
{ e; typ; span }
M.expr_Closure ~params:[ bpat ] ~body:condition ~captures:[]
~span:condition.span
~typ:(TArrow ([ bpat.typ ], condition.typ))
in
let body : B.expr =
let e : B.expr' =
Closure { params = [ bpat ]; body; captures = [] }
in
let typ : B.ty = TArrow ([ bpat.typ ], body.typ) in
let span = body.span in
{ e; typ; span }
M.expr_Closure ~params:[ bpat ] ~body ~captures:[]
~typ:(TArrow ([ bpat.typ ], body.typ))
~span:body.span
in
UB.call ~kind:(AssociatedItem Value) Rust_primitives__hax__while_loop
[ condition; init; body ] span (dty span expr.typ)
Expand Down
Loading

0 comments on commit 2a2445f

Please sign in to comment.