Skip to content

Commit a1dc976

Browse files
authored
Merge branch 'main' into main
2 parents 0902dc8 + 75184e1 commit a1dc976

File tree

17 files changed

+456
-434
lines changed

17 files changed

+456
-434
lines changed

engine/lib/concrete_ident/concrete_ident.ml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -485,7 +485,7 @@ module MakeRenderAPI (NP : NAME_POLICY) : RENDER_API = struct
485485
let*? _no_generics = List.is_empty impl_infos.generics.params in
486486
match impl_infos.trait_ref with
487487
| None -> Some ty
488-
| Some { def_id = trait; generic_args = [ _self ]; _ } ->
488+
| Some { value = { def_id = trait; generic_args = [ _self ]; _ }; _ } ->
489489
let* trait = Explicit_def_id.of_def_id trait in
490490
let trait = View.of_def_id trait in
491491
let*? _same_ns = [%eq: View.ModPath.t] namespace trait.mod_path in

engine/lib/concrete_ident/thir_simple_types.ml

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -58,15 +58,16 @@ let to_string ~(namespace : View.ModPath.t) :
5858
| Float F32 -> Some "f32"
5959
| Float F64 -> Some "f64"
6060
| Tuple [] -> Some "unit"
61-
| Adt { def_id; generic_args = []; _ } -> Option.map ~f:escape (adt def_id)
61+
| Adt { value = { def_id; generic_args = []; _ }; _ } ->
62+
Option.map ~f:escape (adt def_id)
6263
| _ -> None
6364
in
6465
let apply left right = left ^ "_of_" ^ right in
6566
let rec arity1 (ty : Types.node_for__ty_kind) =
6667
match ty.value with
6768
| Slice sub -> arity1 sub |> Option.map ~f:(apply "slice")
6869
| Ref (_, sub, _) -> arity1 sub |> Option.map ~f:(apply "ref")
69-
| Adt { def_id; generic_args = [ Type arg ]; _ } ->
70+
| Adt { value = { def_id; generic_args = [ Type arg ]; _ }; _ } ->
7071
let* adt = adt def_id in
7172
let* arg = arity1 arg in
7273
Some (apply adt arg)

engine/lib/import_thir.ml

Lines changed: 76 additions & 66 deletions
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,8 @@ module Thir = struct
1111
type generic_param_kind = generic_param_kind_for__decorated_for__expr_kind
1212
type trait_item = trait_item_for__decorated_for__expr_kind
1313
type ty = node_for__ty_kind
14+
type item_ref = node_for__item_ref_contents
15+
type trait_ref = item_ref
1416
end
1517

1618
open! Prelude
@@ -244,16 +246,16 @@ end) : EXPR = struct
244246
(typ : ty) =
245247
let overloaded_names_of_binop : Thir.bin_op -> Concrete_ident.name =
246248
function
247-
| Add -> Core__ops__arith__Add__add
248-
| Sub -> Core__ops__arith__Sub__sub
249-
| Mul -> Core__ops__arith__Mul__mul
249+
| Add | AddUnchecked -> Core__ops__arith__Add__add
250+
| Sub | SubUnchecked -> Core__ops__arith__Sub__sub
251+
| Mul | MulUnchecked -> Core__ops__arith__Mul__mul
250252
| Div -> Core__ops__arith__Div__div
251253
| Rem -> Core__ops__arith__Rem__rem
252254
| BitXor -> Core__ops__bit__BitXor__bitxor
253255
| BitAnd -> Core__ops__bit__BitAnd__bitand
254256
| BitOr -> Core__ops__bit__BitOr__bitor
255-
| Shl -> Core__ops__bit__Shl__shl
256-
| Shr -> Core__ops__bit__Shr__shr
257+
| Shl | ShlUnchecked -> Core__ops__bit__Shl__shl
258+
| Shr | ShrUnchecked -> Core__ops__bit__Shr__shr
257259
| Lt -> Core__cmp__PartialOrd__lt
258260
| Le -> Core__cmp__PartialOrd__le
259261
| Ne -> Core__cmp__PartialEq__ne
@@ -269,16 +271,16 @@ end) : EXPR = struct
269271
| Offset -> Core__ptr__const_ptr__Impl__offset
270272
in
271273
let primitive_names_of_binop : Thir.bin_op -> Concrete_ident.name = function
272-
| Add -> Rust_primitives__u128__add
273-
| Sub -> Rust_primitives__u128__sub
274-
| Mul -> Rust_primitives__u128__mul
274+
| Add | AddUnchecked -> Rust_primitives__u128__add
275+
| Sub | SubUnchecked -> Rust_primitives__u128__sub
276+
| Mul | MulUnchecked -> Rust_primitives__u128__mul
275277
| Div -> Rust_primitives__u128__div
276278
| Rem -> Rust_primitives__u128__rem
277279
| BitXor -> Rust_primitives__u128__bit_xor
278280
| BitAnd -> Rust_primitives__u128__bit_and
279281
| BitOr -> Rust_primitives__u128__bit_or
280-
| Shl -> Rust_primitives__u128__shl
281-
| Shr -> Rust_primitives__u128__shr
282+
| Shl | ShlUnchecked -> Rust_primitives__u128__shl
283+
| Shr | ShrUnchecked -> Rust_primitives__u128__shr
282284
| Lt -> Rust_primitives__u128__lt
283285
| Le -> Rust_primitives__u128__le
284286
| Ne -> Rust_primitives__u128__ne
@@ -330,11 +332,12 @@ end) : EXPR = struct
330332
let expected, f =
331333
match op with
332334
| Add | Sub | Mul | AddWithOverflow | SubWithOverflow
333-
| MulWithOverflow | Div ->
335+
| MulWithOverflow | AddUnchecked | SubUnchecked | MulUnchecked | Div
336+
->
334337
both int <|> both float
335338
| Rem | Cmp -> both int
336339
| BitXor | BitAnd | BitOr -> both int <|> both bool
337-
| Shl | Shr -> int <*> int
340+
| Shl | Shr | ShlUnchecked | ShrUnchecked -> int <*> int
338341
| Lt | Le | Ne | Ge | Gt -> both int <|> both float
339342
| Eq -> both int <|> both float <|> both bool
340343
| Offset -> ("", fun _ -> Some "")
@@ -504,38 +507,35 @@ end) : EXPR = struct
504507
let then_ = c_expr then' in
505508
let else_ = Option.map ~f:c_expr else_opt in
506509
If { cond; else_; then_ }
507-
| Call
508-
{
509-
args;
510-
fn_span = _;
511-
trait;
512-
from_hir_call = _;
513-
fun';
514-
ty = _;
515-
generic_args;
516-
bounds_impls;
517-
} ->
518-
let args = List.map ~f:c_expr args in
519-
let bounds_impls = List.map ~f:(c_impl_expr e.span) bounds_impls in
520-
let c_generic_values = List.map ~f:(c_generic_value e.span) in
521-
let generic_args = c_generic_values generic_args in
522-
let f =
523-
let f = c_expr fun' in
524-
match (trait, fun'.contents) with
525-
| Some _, GlobalName { id; _ } ->
526-
{ f with e = GlobalVar (def_id ~value:true id) }
527-
| _ -> f
510+
| Call { args; fn_span = _; from_hir_call = _; fun'; ty = _ } -> (
511+
let args =
512+
if List.is_empty args then [ unit_expr span ]
513+
else List.map ~f:c_expr args
528514
in
529-
let args = if List.is_empty args then [ unit_expr span ] else args in
530-
App
531-
{
532-
f;
533-
args;
534-
generic_args;
535-
bounds_impls;
536-
trait =
537-
Option.map ~f:(c_impl_expr e.span *** c_generic_values) trait;
538-
}
515+
let f = c_expr fun' in
516+
match fun'.contents with
517+
| GlobalName
518+
{
519+
item =
520+
{
521+
value = { def_id = id; generic_args; impl_exprs; in_trait };
522+
_;
523+
};
524+
_;
525+
} ->
526+
let f = { f with e = GlobalVar (def_id ~value:true id) } in
527+
let bounds_impls = List.map ~f:(c_impl_expr e.span) impl_exprs in
528+
let generic_args =
529+
List.map ~f:(c_generic_value e.span) generic_args
530+
in
531+
let in_trait = Option.map ~f:(c_impl_expr e.span) in_trait in
532+
let trait =
533+
Option.map ~f:(fun ie -> (ie, ie.goal.args)) in_trait
534+
in
535+
App { f; args; generic_args; bounds_impls; trait }
536+
| _ ->
537+
App
538+
{ f; args; generic_args = []; bounds_impls = []; trait = None })
539539
| Box { value } ->
540540
(U.call Rust_primitives__hax__box_new [ c_expr value ] span typ).e
541541
| Deref { arg } ->
@@ -644,7 +644,9 @@ end) : EXPR = struct
644644
trait = None (* TODO: see issue #328 *);
645645
bounds_impls = [];
646646
}
647-
| GlobalName { id; constructor = _ } -> GlobalVar (def_id ~value:true id)
647+
| GlobalName { item = { value = { def_id = id; _ }; _ }; constructor = _ }
648+
->
649+
GlobalVar (def_id ~value:true id)
648650
| UpvarRef { var_hir_id = id; _ } -> LocalVar (local_ident Expr id)
649651
| Borrow { arg; borrow_kind = kind } ->
650652
let e' = c_expr arg in
@@ -731,9 +733,14 @@ end) : EXPR = struct
731733
typ = TInt { size = S8; signedness = Unsigned };
732734
})
733735
l))
734-
| NamedConst { def_id = id; impl; args; _ } ->
736+
| NamedConst
737+
{
738+
item =
739+
{ value = { def_id = id; generic_args; in_trait = impl; _ }; _ };
740+
_;
741+
} ->
735742
let f = GlobalVar (def_id ~value:true id) in
736-
let args = List.map ~f:(c_generic_value e.span) args in
743+
let args = List.map ~f:(c_generic_value e.span) generic_args in
737744
let const_args =
738745
List.filter_map args ~f:(function GConst e -> Some e | _ -> None)
739746
in
@@ -853,7 +860,7 @@ end) : EXPR = struct
853860
Array { fields = List.map ~f:constant_expr_to_expr fields }
854861
| Tuple { fields } ->
855862
Tuple { fields = List.map ~f:constant_expr_to_expr fields }
856-
| GlobalName { id; _ } -> GlobalName { id; constructor = None }
863+
| GlobalName item -> GlobalName { item; constructor = None }
857864
| Borrow arg ->
858865
Borrow { arg = constant_expr_to_expr arg; borrow_kind = Thir.Shared }
859866
| ConstRef { id } -> ConstRef { id }
@@ -1023,16 +1030,14 @@ end) : EXPR = struct
10231030
| Float k ->
10241031
TFloat
10251032
(match k with F16 -> F16 | F32 -> F32 | F64 -> F64 | F128 -> F128)
1026-
| Arrow signature
1027-
| Closure (_, { untupled_sig = signature; _ })
1028-
| FnDef { fn_sig = signature; _ } ->
1029-
let ({ inputs; output; _ } : Thir.ty_fn_sig) = signature.value in
1033+
| Arrow fn_sig | Closure { fn_sig; _ } | FnDef { fn_sig; _ } ->
1034+
let ({ inputs; output; _ } : Thir.ty_fn_sig) = fn_sig.value in
10301035
let inputs =
10311036
if List.is_empty inputs then [ U.unit_typ ]
10321037
else List.map ~f:(c_ty span) inputs
10331038
in
10341039
TArrow (inputs, c_ty span output)
1035-
| Adt { def_id = id; generic_args; _ } ->
1040+
| Adt { value = { def_id = id; generic_args; _ }; _ } ->
10361041
let ident = def_id ~value:false id in
10371042
let args = List.map ~f:(c_generic_value span) generic_args in
10381043
TApp { ident; args }
@@ -1117,15 +1122,15 @@ end) : EXPR = struct
11171122
let goal = c_trait_ref span ie.trait.value in
11181123
let impl = { kind = c_impl_expr_atom span ie.impl; goal } in
11191124
match ie.impl with
1120-
| Concrete { impl_exprs = []; _ } -> impl
1121-
| Concrete { impl_exprs; _ } ->
1125+
| Concrete { value = { impl_exprs = []; _ }; _ } -> impl
1126+
| Concrete { value = { impl_exprs; _ }; _ } ->
11221127
let args = List.map ~f:(c_impl_expr span) impl_exprs in
11231128
{ kind = ImplApp { impl; args }; goal }
11241129
| _ -> impl
11251130

11261131
and c_trait_ref span (tr : Thir.trait_ref) : trait_goal =
1127-
let trait = Concrete_ident.of_def_id ~value:false tr.def_id in
1128-
let args = List.map ~f:(c_generic_value span) tr.generic_args in
1132+
let trait = Concrete_ident.of_def_id ~value:false tr.value.def_id in
1133+
let args = List.map ~f:(c_generic_value span) tr.value.generic_args in
11291134
{ trait; args }
11301135

11311136
and c_impl_expr_atom (span : Thir.span) (ie : Thir.impl_expr_atom) :
@@ -1139,7 +1144,7 @@ end) : EXPR = struct
11391144
let ident =
11401145
{ goal = c_trait_ref span trait_ref; name = predicate_id }
11411146
in
1142-
let item = Concrete_ident.of_def_id ~value:false item.def_id in
1147+
let item = Concrete_ident.of_def_id ~value:false item.value.def_id in
11431148
let trait_ref = c_trait_ref span trait_ref in
11441149
Projection
11451150
{ impl = { kind = item_kind; goal = trait_ref }; ident; item }
@@ -1152,9 +1157,9 @@ end) : EXPR = struct
11521157
Parent { impl = { kind = item_kind; goal = trait_ref }; ident }
11531158
in
11541159
match ie with
1155-
| Concrete { id; generics; _ } ->
1156-
let trait = Concrete_ident.of_def_id ~value:false id in
1157-
let args = List.map ~f:(c_generic_value span) generics in
1160+
| Concrete { value = { def_id; generic_args; _ }; _ } ->
1161+
let trait = Concrete_ident.of_def_id ~value:false def_id in
1162+
let args = List.map ~f:(c_generic_value span) generic_args in
11581163
Concrete { trait; args }
11591164
| LocalBound { predicate_id; path; _ } ->
11601165
let init = LocalBound { id = predicate_id } in
@@ -1249,8 +1254,12 @@ end) : EXPR = struct
12491254
generic_constraint option =
12501255
match kind with
12511256
| Trait { is_positive = true; trait_ref } ->
1252-
let args = List.map ~f:(c_generic_value span) trait_ref.generic_args in
1253-
let trait = Concrete_ident.of_def_id ~value:false trait_ref.def_id in
1257+
let args =
1258+
List.map ~f:(c_generic_value span) trait_ref.value.generic_args
1259+
in
1260+
let trait =
1261+
Concrete_ident.of_def_id ~value:false trait_ref.value.def_id
1262+
in
12541263
Some (GCType { goal = { trait; args }; name = id })
12551264
| Projection { impl_expr; assoc_item; ty } ->
12561265
let impl = c_impl_expr span impl_expr in
@@ -1329,7 +1338,7 @@ include struct
13291338

13301339
let import_ty : Types.span -> Types.node_for__ty_kind -> Ast.Rust.ty = c_ty
13311340

1332-
let import_trait_ref : Types.span -> Types.trait_ref -> Ast.Rust.trait_goal =
1341+
let import_trait_ref : Types.span -> Thir.trait_ref -> Ast.Rust.trait_goal =
13331342
c_trait_ref
13341343

13351344
let import_clause :
@@ -1777,9 +1786,10 @@ and c_item_unwrapped ~ident ~type_only (item : Thir.item) : item list =
17771786
generics = c_generics generics;
17781787
self_ty = c_ty item.span self_ty;
17791788
of_trait =
1780-
( Concrete_ident.of_def_id ~value:false of_trait.def_id,
1781-
List.map ~f:(c_generic_value item.span) of_trait.generic_args
1782-
);
1789+
( Concrete_ident.of_def_id ~value:false of_trait.value.def_id,
1790+
List.map
1791+
~f:(c_generic_value item.span)
1792+
of_trait.value.generic_args );
17831793
items;
17841794
parent_bounds =
17851795
List.filter_map

engine/lib/import_thir.mli

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,7 @@
11
val import_ty : Types.span -> Types.node_for__ty_kind -> Ast.Rust.ty
2-
val import_trait_ref : Types.span -> Types.trait_ref -> Ast.Rust.trait_goal
2+
3+
val import_trait_ref :
4+
Types.span -> Types.node_for__item_ref_contents -> Ast.Rust.trait_goal
35

46
val import_clause :
57
Types.span -> Types.clause -> Ast.Rust.generic_constraint option

engine/utils/ocaml_of_json_schema/ocaml_of_json_schema.js

Lines changed: 13 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -576,6 +576,7 @@ end
576576
let items = Object.entries(definitions)
577577
.map(([name, def]) => ['Node_for_TyKind' == name ? 'node_for_ty_kind_generated' : name, def])
578578
.map(([name, def]) => ['Node_for_DefIdContents' == name ? 'node_for_def_id_contents_generated' : name, def])
579+
.map(([name, def]) => ['Node_for_ItemRefContents' == name ? 'node_for_item_ref_contents_generated' : name, def])
579580
.map(
580581
([name, def]) => export_definition(name, def)
581582
).filter(x => x instanceof Object);
@@ -611,9 +612,10 @@ open ParseError
611612
impl += `
612613
and node_for__ty_kind = node_for_ty_kind_generated
613614
and node_for__def_id_contents = node_for_def_id_contents_generated
615+
and node_for__item_ref_contents = node_for_item_ref_contents_generated
614616
615617
616-
type map_types = ${"[`TyKind of ty_kind | `DefIdContents of def_id_contents]"}
618+
type map_types = ${"[`TyKind of ty_kind | `DefIdContents of def_id_contents | `ItemRefContents of item_ref_contents]"}
617619
let cache_map: (int64, ${"[ `Value of map_types | `JSON of Yojson.Safe.t ]"}) Base.Hashtbl.t = Base.Hashtbl.create (module Base.Int64)
618620
619621
module Exn = struct
@@ -667,6 +669,15 @@ and node_for__def_id_contents_of_yojson (o: Yojson.Safe.t): node_for__def_id_con
667669
o
668670
in
669671
{value; id = Base.Int64.zero}
672+
and node_for__item_ref_contents_of_yojson (o: Yojson.Safe.t): node_for__item_ref_contents =
673+
let (value, _id) =
674+
table_id_node_of_yojson "ItemRefContents"
675+
(fun value -> \`ItemRefContents value)
676+
(function | \`ItemRefContents value -> Some value | _ -> None)
677+
item_ref_contents_of_yojson
678+
o
679+
in
680+
{value; id = Base.Int64.zero}
670681
`;
671682
impl += ('');
672683
impl += ('let rec ' + items.map(({ name, type, parse, to_json }) =>
@@ -675,6 +686,7 @@ and node_for__def_id_contents_of_yojson (o: Yojson.Safe.t): node_for__def_id_con
675686
impl += `
676687
and yojson_of_node_for__ty_kind {value; id} = yojson_of_node_for_ty_kind_generated {value; id}
677688
and yojson_of_node_for__def_id_contents {value; id} = yojson_of_node_for_def_id_contents_generated {value; id}
689+
and yojson_of_node_for__item_ref_contents {value; id} = yojson_of_node_for_item_ref_contents_generated {value; id}
678690
end
679691
680692
open struct

0 commit comments

Comments
 (0)