From cc709075c62d5d1136384af8579a53f985038f8f Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Fri, 23 Jun 2023 14:55:07 +0200 Subject: [PATCH] Enhancements --- engine/backends/fstar/fstar_backend.ml | 17 +- engine/lib/concrete_ident/concrete_ident.ml | 16 + engine/lib/concrete_ident/concrete_ident.mli | 2 + engine/lib/import_thir.ml | 1311 ++++++++++-------- frontend/exporter/src/all.rs | 22 +- 5 files changed, 777 insertions(+), 591 deletions(-) diff --git a/engine/backends/fstar/fstar_backend.ml b/engine/backends/fstar/fstar_backend.ml index 9fdc47eb6..5b6cef958 100644 --- a/engine/backends/fstar/fstar_backend.ml +++ b/engine/backends/fstar/fstar_backend.ml @@ -327,7 +327,7 @@ struct @@ F.AST.Project (pexpr arg, F.lid [ "_" ^ string_of_int (n + 1) ]) | App { f = { e = GlobalVar (`Projector (`Concrete cid)) }; args = [ arg ] } -> - F.term @@ F.AST.Project (pexpr arg, pfield_concrete_ident cid) + F.term @@ F.AST.Project (pexpr arg, pconcrete_ident cid) | App { f = { e = GlobalVar x }; args } when Map.mem operators x -> let arity, op = Map.find_exn operators x in if List.length args <> arity then @@ -343,7 +343,20 @@ struct None, pexpr then_, Option.value_map else_ ~default:F.unit ~f:pexpr ) - | Array l -> F.AST.mkConsList F.dummyRange (List.map ~f:pexpr l) + | Array l -> + let len = List.length l in + let body = F.AST.mkConsList F.dummyRange (List.map ~f:pexpr l) in + let array_of_list = + let id = + Concrete_ident.of_name Value Rust_primitives__hax__array_of_list + in + F.term @@ F.AST.Name (pconcrete_ident id) + in + F.term_of_string + ("(let l = " ^ term_to_string body + ^ " in assert_norm (List.Tot.length l == " ^ Int.to_string len ^ "); " + ^ term_to_string array_of_list + ^ " l)") | Let { lhs; rhs; body; monadic = Some monad } -> let p = F.pat @@ F.AST.PatAscribed (ppat lhs, (pty lhs.span lhs.typ, None)) diff --git a/engine/lib/concrete_ident/concrete_ident.ml b/engine/lib/concrete_ident/concrete_ident.ml index addbb274c..0d49157b1 100644 --- a/engine/lib/concrete_ident/concrete_ident.ml +++ b/engine/lib/concrete_ident/concrete_ident.ml @@ -61,6 +61,17 @@ module Imported = struct | Some path, Some { data = Ctor; _ } -> path | _ -> path); } + + let map_path_strings ~(f : string -> string) (did : def_id) : def_id = + let f : def_path_item -> def_path_item = function + | TypeNs s -> TypeNs (f s) + | ValueNs s -> ValueNs (f s) + | MacroNs s -> MacroNs (f s) + | LifetimeNs s -> LifetimeNs (f s) + | other -> other + in + let f x = { x with data = f x.data } in + { did with path = List.map ~f did.path } end module Kind = struct @@ -85,6 +96,9 @@ end type t = { def_id : Imported.def_id; kind : Kind.t } [@@deriving show, yojson, sexp] +let map_path_strings ~(f : string -> string) (cid : t) : t = + { cid with def_id = Imported.map_path_strings ~f cid.def_id } + (* [kind] is really a metadata, it is not relevant, `def_id`s are unique *) let equal x y = [%equal: Imported.def_id] x.def_id y.def_id let compare x y = [%compare: Imported.def_id] x.def_id y.def_id @@ -219,6 +233,8 @@ let rec to_view ({ def_id; kind } : t) : view = and to_definition_name (x : t) : string = (to_view x).definition +let to_crate_name (x : t) : string = (to_view x).crate + let to_namespace x = let View.{ crate; path; _ } = to_view x in (crate, path) diff --git a/engine/lib/concrete_ident/concrete_ident.mli b/engine/lib/concrete_ident/concrete_ident.mli index 2d64012f2..fffc693f6 100644 --- a/engine/lib/concrete_ident/concrete_ident.mli +++ b/engine/lib/concrete_ident/concrete_ident.mli @@ -22,4 +22,6 @@ type view = { crate : string; path : string list; definition : string } val to_view : t -> view val to_definition_name : t -> string +val to_crate_name : t -> string val to_namespace : t -> string * string list +val map_path_strings : f:(string -> string) -> t -> t diff --git a/engine/lib/import_thir.ml b/engine/lib/import_thir.ml index 68c92ee0e..86693a754 100644 --- a/engine/lib/import_thir.ml +++ b/engine/lib/import_thir.ml @@ -120,17 +120,11 @@ module Exn = struct | And -> And | Or -> Or - let c_lit_type span (t : Thir.lit_int_type) : int_kind = - match t with - | Unsuffixed -> - assertion_failure span - "Got an untyped int literal which is `Unsuffixed`" - | Signed ty -> { size = int_ty_to_size ty; signedness = Signed } - | Unsigned ty -> { size = uint_ty_to_size ty; signedness = Unsigned } - - type extended_literal = EL_Lit of literal | EL_Array of literal list + type extended_literal = + | EL_Lit of literal + | EL_U8Array of literal list (* EL_U8Array only encodes arrays of [u8]s *) - let c_lit' span (lit : Thir.lit_kind) (ty : ty option) : extended_literal = + let c_lit' span (lit : Thir.lit_kind) (ty : ty) : extended_literal = let mk l = EL_Lit l in let mku8 n = let kind = { size = S8; signedness = Unsigned } in @@ -149,10 +143,10 @@ module Exn = struct "[import_thir:literal] got an error literal: this means the Rust \ compiler or Hax's frontend probably reported errors above." | Str (str, _) -> mk @@ String str - | CStr (l, _) | ByteStr (l, _) -> EL_Array (List.map ~f:mku8 l) + | CStr (l, _) | ByteStr (l, _) -> EL_U8Array (List.map ~f:mku8 l) | Byte n -> mk @@ mku8 n | Char s -> mk @@ Char s - | Int (i, _t) -> + | Int (value, _kind) -> mk @@ Int { @@ -166,11 +160,9 @@ module Exn = struct value; kind = (match ty with TFloat k -> k | ty -> error "float"); } - | Float _ -> unimplemented span "todo float" | Bool b -> mk @@ Bool b - let c_lit span (lit : Thir.spanned_for__lit_kind) : - ty option -> extended_literal = + let c_lit span (lit : Thir.spanned_for__lit_kind) : ty -> extended_literal = c_lit' span lit.node let resugar_index_mut (e : expr) : (expr * expr) option = @@ -187,605 +179,752 @@ module Exn = struct Some (x, index) | _ -> None - let rec c_expr (e : Thir.decorated_for__expr_kind) : expr = - try c_expr_unwrapped e - with Diagnostics.SpanFreeError report -> - let typ : ty = - try c_ty e.span e.ty - with Diagnostics.SpanFreeError _ -> U.hax_failure_typ - in - let span = c_span e.span in - U.hax_failure_expr' span typ report - ([%show: Thir.decorated_for__expr_kind] e) + module type EXPR = sig + val c_expr : Thir.decorated_for__expr_kind -> expr + val c_ty : Thir.span -> Thir.ty -> ty + val c_generic_value : Thir.span -> Thir.generic_arg -> generic_value + val c_generics : Thir.generics -> generics + val c_param : Thir.span -> Thir.param -> param + val c_trait_item' : Thir.span -> Thir.trait_item_kind -> trait_item' + end - and c_binop (op : Thir.bin_op) lhs rhs span typ = - U.call - (match op with - | Add -> Core__ops__arith__Add__add - | Sub -> Core__ops__arith__Sub__sub - | Mul -> Core__ops__arith__Mul__mul - | Div -> Core__ops__arith__Div__div - | Rem -> Core__ops__arith__Rem__rem - | BitXor -> Core__ops__bit__BitXor__bitxor - | BitAnd -> Core__ops__bit__BitAnd__bitand - | BitOr -> Core__ops__bit__BitOr__bitor - | Shl -> Core__ops__bit__Shl__shl - | Shr -> Core__ops__bit__Shr__shr - | Eq -> Core__cmp__PartialEq__eq - | Lt -> Core__cmp__PartialOrd__lt - | Le -> Core__cmp__PartialOrd__le - | Ne -> Core__cmp__PartialEq__ne - | Ge -> Core__cmp__PartialOrd__ge - | Gt -> Core__cmp__PartialOrd__gt - | Offset -> Core__ptr__const_ptr__Impl__offset) - [ lhs; rhs ] span typ + (* BinOp to [core::ops::*] overloaded functions *) - and c_expr_unwrapped (e : Thir.decorated_for__expr_kind) : expr = - let call f args = App { f; args = List.map ~f:c_expr args } in - let typ = c_ty e.span e.ty in - let span = c_span e.span in - let mk_global typ v : expr = { span; typ; e = GlobalVar v } in - let ( ->. ) a b = TArrow (a, b) in - let (v : expr') = - match e.contents with - | MacroInvokation { argument; macro_ident; _ } -> - MacroInvokation - { - args = argument; - macro = def_id Macro macro_ident; - witness = W.macro; - } - | If - { - cond = { contents = Let { expr = scrutinee; pat }; _ }; - else_opt; - then'; - _; - } -> - let scrutinee = c_expr scrutinee in - let arm_pat = c_pat pat in - let then_ = c_expr then' in - let else_ = - Option.value ~default:(U.unit_expr span) - @@ Option.map ~f:c_expr else_opt - in - let arm_then = - { arm = { arm_pat; body = then_ }; span = then_.span } - in - let arm_else = - let arm_pat = { arm_pat with p = PWild } in - { arm = { arm_pat; body = else_ }; span = else_.span } - in - Match { scrutinee; arms = [ arm_then; arm_else ] } - | If { cond; else_opt; then'; _ } -> - let cond = c_expr cond in - let then_ = c_expr then' in - let else_ = Option.map ~f:c_expr else_opt in - If { cond; else_; then_ } - | Call { args; fn_span = _; from_hir_call = _; fun'; ty = _ } -> - let args = List.map ~f:c_expr args in - let f = c_expr fun' in - App { f; args } - | Deref { arg } -> - let inner_typ = c_ty arg.span arg.ty in - call (mk_global ([ inner_typ ] ->. typ) @@ `Primitive Deref) [ arg ] - | Binary { lhs; rhs; op } -> - (c_binop op (c_expr lhs) (c_expr rhs) span typ).e - | LogicalOp { lhs; rhs; op } -> - let lhs_type = c_ty lhs.span lhs.ty in - let rhs_type = c_ty rhs.span rhs.ty in - call - (mk_global ([ lhs_type; rhs_type ] ->. typ) - @@ `Primitive (LogicalOp (c_logical_op op))) - [ lhs; rhs ] - | Unary { arg; op } -> - (U.call - (match op with - | Not -> Core__ops__bit__Not__not - | Neg -> Core__ops__arith__Neg__neg) - [ c_expr arg ] - span typ) - .e - | Cast { source } -> - let source_type = c_ty source.span source.ty in - call - (mk_global ([ source_type ] ->. typ) @@ `Primitive Cast) - [ source ] - | Use { source } -> (c_expr source).e - | NeverToAny { source } -> (c_expr source).e - (* TODO: this is incorrect (NeverToAny) *) - | Pointer { cast; source } -> c_pointer e typ span cast source - | Loop { body } -> - let body = c_expr body in - Loop - { - body; - kind = UnconditionalLoop; - state = None; - label = None; - witness = W.loop; - } - | Match { scrutinee; arms } -> - let scrutinee = c_expr scrutinee in - let arms = List.map ~f:c_arm arms in - Match { scrutinee; arms } - | Let _ -> unimplemented e.span "Let" - | Block { safety_mode = BuiltinUnsafe | ExplicitUnsafe; _ } -> - raise e.span UnsafeBlock - | Block o -> - (* if there is no expression & the last expression is ⊥, just use that *) - let lift_last_statement_as_expr_if_possible expr stmts (ty : Thir.ty) - = - match (ty, expr, List.drop_last stmts, List.last stmts) with - | ( Thir.Never, - None, - Some stmts, - Some ({ kind = Thir.Expr { expr; _ }; _ } : Thir.stmt) ) -> - (stmts, Some expr) - | _ -> (stmts, expr) - in - let o_stmts, o_expr = - lift_last_statement_as_expr_if_possible o.expr o.stmts e.ty - in - let init = - Option.map ~f:c_expr o_expr - |> Option.value ~default:(unit_expr span) + module Make (CTX : sig + val is_core_item : bool + end) : EXPR = struct + let c_binop (op : Thir.bin_op) (lhs : expr) (rhs : expr) (span : span) + (typ : ty) = + let overloaded_names_of_binop : Thir.bin_op -> Concrete_ident.name = + function + | Add -> Core__ops__arith__Add__add + | Sub -> Core__ops__arith__Sub__sub + | Mul -> Core__ops__arith__Mul__mul + | Div -> Core__ops__arith__Div__div + | Rem -> Core__ops__arith__Rem__rem + | BitXor -> Core__ops__bit__BitXor__bitxor + | BitAnd -> Core__ops__bit__BitAnd__bitand + | BitOr -> Core__ops__bit__BitOr__bitor + | Shl -> Core__ops__bit__Shl__shl + | Shr -> Core__ops__bit__Shr__shr + | Lt -> Core__cmp__PartialOrd__lt + | Le -> Core__cmp__PartialOrd__le + | Ne -> Core__cmp__PartialEq__ne + | Ge -> Core__cmp__PartialOrd__ge + | Gt -> Core__cmp__PartialOrd__gt + | Eq -> Core__cmp__PartialEq__eq + | Offset -> Core__ptr__const_ptr__Impl__offset + in + let primitive_names_of_binop : Thir.bin_op -> Concrete_ident.name = + function + | Add -> Rust_primitives__u128__add + | Sub -> Rust_primitives__u128__sub + | Mul -> Rust_primitives__u128__mul + | Div -> Rust_primitives__u128__div + | Rem -> Rust_primitives__u128__rem + | BitXor -> Rust_primitives__u128__bit_xor + | BitAnd -> Rust_primitives__u128__bit_and + | BitOr -> Rust_primitives__u128__bit_or + | Shl -> Rust_primitives__u128__shl + | Shr -> Rust_primitives__u128__shr + | Lt -> Rust_primitives__u128__lt + | Le -> Rust_primitives__u128__le + | Ne -> Rust_primitives__u128__ne + | Ge -> Rust_primitives__u128__ge + | Gt -> Rust_primitives__u128__gt + | Eq -> Rust_primitives__u128__eq + | Offset -> Rust_primitives__offset + in + let name = + if CTX.is_core_item then + let assert_type_eq t1 t2 = + if not (U.ty_equality t1 t2) then + assertion_failure + (Diagnostics.to_thir_span span) + ("Binary operation: expected LHS and RHS to have the same \ + type, instead LHS has type [" + ^ [%show: ty] t1 + ^ "] while RHS has type [" + ^ [%show: ty] t2 + ^ "]") in - let { e; _ } = - List.fold_right o_stmts ~init ~f:(fun { kind; _ } body -> - match kind with - | Expr { expr = rhs; _ } -> - let rhs = c_expr rhs in - let e = - Let - { - monadic = None; - lhs = wild_pat rhs.span rhs.typ; - rhs; - body; - } - in - let span = union_span rhs.span body.span in - { e; typ; span } - | Let { else_block = Some _; _ } -> raise e.span LetElse - | Let { initializer' = None; _ } -> raise e.span LetWithoutInit - | Let { pattern = lhs; initializer' = Some rhs; _ } -> - let lhs = c_pat lhs in - let rhs = c_expr rhs in - let e = Let { monadic = None; lhs; rhs; body } in - let span = union_span rhs.span body.span in - { e; typ; span }) + let int = + ("int", function TInt k -> Some (show_int_kind k) | _ -> None) in - e - | Assign { lhs; rhs } -> - let lhs = c_expr lhs in - let rhs = c_expr rhs in - c_expr_assign lhs rhs - | AssignOp { lhs; op; rhs } -> - let lhs = c_expr lhs in - c_expr_assign lhs @@ c_binop op lhs (c_expr rhs) span typ - | VarRef { id } -> LocalVar (local_ident id) - | Field { lhs; field } -> - let lhs = c_expr lhs in - let projector = - GlobalVar - (`Projector (`Concrete (Concrete_ident.of_def_id Field field))) + let float = + ( "float", + function TFloat k -> Some (show_float_kind k) | _ -> None ) in - let span = c_span e.span in - App - { - f = { e = projector; typ = TArrow ([ lhs.typ ], typ); span }; - args = [ lhs ]; - } - | TupleField { lhs; field } -> - (* TODO: refactor *) - let tuple_len = 0 (* todo, lookup type *) in - let lhs = c_expr lhs in - let projector = - GlobalVar (`Projector (`TupleField (field, tuple_len))) + let bool = ("bool", function TBool -> Some "bool" | _ -> None) in + let concat_tup sep (x, y) = x ^ sep ^ y in + let ( <*> ) (x, f) (y, g) = + ( x ^ "*" ^ y, + f *** g >> uncurry Option.both >> Option.map ~f:(concat_tup "_") + ) in - let span = c_span e.span in - App - { - f = { e = projector; typ = TArrow ([ lhs.typ ], typ); span }; - args = [ lhs ]; - } - | GlobalName { id } -> GlobalVar (def_id Value id) - | UpvarRef { var_hir_id = id; _ } -> LocalVar (local_ident id) - | Borrow { arg; borrow_kind = kind } -> - let e' = c_expr arg in - let kind = c_borrow_kind e.span kind in - Borrow { kind; e = e'; witness = W.reference } - | AddressOf { arg; mutability = mut } -> - let e = c_expr arg in - AddressOf - { - e; - mut = c_mutability W.mutable_pointer mut; - witness = W.raw_pointer; - } - | Break { value; _ } -> - (* TODO: labels! *) - let e = Option.map ~f:c_expr value in - let e = Option.value ~default:(unit_expr span) e in - Break { e; label = None; witness = W.loop } - | Continue _ -> - Continue { e = None; label = None; witness = (W.continue, W.loop) } - | Return { value } -> - let e = Option.map ~f:c_expr value in - let e = Option.value ~default:(unit_expr span) e in - Return { e; witness = W.early_exit } - | ConstBlock _ -> unimplemented e.span "ConstBlock" - | ConstParam { param = id } (* TODO: shadowing? *) | ConstRef { id } -> - LocalVar { name = id.name; id = LocalIdent.const_id_of_int id.index } - | Repeat { value; count } -> - let value = c_expr value in - let count = c_expr count in - let inner = U.call Hax__Array__repeat [ value; count ] span typ in - (U.call Alloc__boxed__Impl__new [ inner ] span typ).e - | Tuple { fields } -> - (U.make_tuple_expr' ~span @@ List.map ~f:c_expr fields).e - | Array { fields } -> Array (List.map ~f:c_expr fields) - | Adt { info; base; fields; _ } -> - let constructor = - def_id (Constructor { is_struct = info.typ_is_struct }) info.variant + let both (e, f) = + ( e ^ "*" ^ e, + fun (t1, t2) -> + assert_type_eq t1 t2; + f t1 ) in - let base = - Option.map - ~f:(fun base -> (c_expr base.base, W.construct_base)) - base + let ( <|> ) (x, f) (y, g) = + (x ^ " or" ^ y, fun v -> match f v with None -> g v | v -> v) in - let fields = - List.map - ~f:(fun f -> - let field = def_id Field f.field in - let value = c_expr f.value in - (field, value)) - fields + let name = primitive_names_of_binop op in + let expected, f = + match op with + | Add | Sub | Mul | Div -> both int <|> both float + | Rem -> both int + | BitXor | BitAnd | BitOr -> both int <|> both bool + | Shl | Shr -> int <*> int + | Lt | Le | Ne | Ge | Gt -> both int <|> both float + | Eq -> both int <|> both float <|> both bool + | Offset -> ("", fun _ -> Some "") in - Construct + match f (lhs.typ, rhs.typ) with + | Some with_ -> + Concrete_ident.of_name Value name + |> Concrete_ident.map_path_strings ~f:(function + | "u128" -> with_ + | s -> s) + | None -> + assertion_failure + (Diagnostics.to_thir_span span) + ("Binary operation: expected " ^ expected ^ " type, got " + ^ [%show: ty] lhs.typ) + else Concrete_ident.of_name Value @@ overloaded_names_of_binop op + in + U.call' (`Concrete name) [ lhs; rhs ] span typ + + let rec c_expr (e : Thir.decorated_for__expr_kind) : expr = + try c_expr_unwrapped e + with Diagnostics.SpanFreeError report -> + let typ : ty = + try c_ty e.span e.ty + with Diagnostics.SpanFreeError _ -> U.hax_failure_typ + in + let span = c_span e.span in + U.hax_failure_expr' span typ report + ([%show: Thir.decorated_for__expr_kind] e) + + and c_expr_unwrapped (e : Thir.decorated_for__expr_kind) : expr = + let call f args = App { f; args = List.map ~f:c_expr args } in + let typ = c_ty e.span e.ty in + let span = c_span e.span in + let mk_global typ v : expr = { span; typ; e = GlobalVar v } in + let ( ->. ) a b = TArrow (a, b) in + let (v : expr') = + match e.contents with + | MacroInvokation { argument; macro_ident; _ } -> + MacroInvokation + { + args = argument; + macro = def_id Macro macro_ident; + witness = W.macro; + } + | If { - is_record = info.variant_is_record; - is_struct = info.typ_is_struct; - constructor; - fields; - base; - } - | Literal { lit; _ } -> ( - match c_lit e.span lit @@ Some typ with - | EL_Lit lit -> Literal lit - | EL_Array l -> - Array - (List.map - ~f:(fun lit -> - { - e = Literal lit; - span; - typ = TInt { size = S8; signedness = Unsigned }; - }) - l)) - | NamedConst { def_id = id; _ } -> GlobalVar (def_id Value id) - | Closure { body; params; upvars; _ } -> - let params = - List.filter_map ~f:(fun p -> Option.map ~f:c_pat p.pat) params - in - let body = c_expr body in - let upvars = List.map ~f:c_expr upvars in - Closure { body; params; captures = upvars } - | Index { index; lhs } -> - let index_type = c_ty index.span index.ty in - let lhs_type = c_ty lhs.span lhs.ty in - call - (mk_global ([ lhs_type; index_type ] ->. typ) - @@ Global_ident.of_name Value Core__ops__index__Index__index) - [ lhs; index ] - | StaticRef { def_id = id; _ } -> GlobalVar (def_id Value id) - | PlaceTypeAscription _ -> - unimplemented e.span "expression PlaceTypeAscription" - | ValueTypeAscription _ -> - unimplemented e.span "expression ValueTypeAscription" - | ZstLiteral _ -> unimplemented e.span "expression ZstLiteral" - | Yield _ -> unimplemented e.span "expression Yield" - | Todo _ -> unimplemented e.span "expression Todo" - in - { e = v; span; typ } + cond = { contents = Let { expr = scrutinee; pat }; _ }; + else_opt; + then'; + _; + } -> + let scrutinee = c_expr scrutinee in + let arm_pat = c_pat pat in + let then_ = c_expr then' in + let else_ = + Option.value ~default:(U.unit_expr span) + @@ Option.map ~f:c_expr else_opt + in + let arm_then = + { arm = { arm_pat; body = then_ }; span = then_.span } + in + let arm_else = + let arm_pat = { arm_pat with p = PWild } in + { arm = { arm_pat; body = else_ }; span = else_.span } + in + Match { scrutinee; arms = [ arm_then; arm_else ] } + | If { cond; else_opt; then'; _ } -> + let cond = c_expr cond in + let then_ = c_expr then' in + let else_ = Option.map ~f:c_expr else_opt in + If { cond; else_; then_ } + | Call { args; fn_span = _; from_hir_call = _; fun'; ty = _ } -> + let args = List.map ~f:c_expr args in + let f = c_expr fun' in + App { f; args } + | Deref { arg } -> + let inner_typ = c_ty arg.span arg.ty in + call (mk_global ([ inner_typ ] ->. typ) @@ `Primitive Deref) [ arg ] + | Binary { lhs; rhs; op } -> + (c_binop op (c_expr lhs) (c_expr rhs) span typ).e + | LogicalOp { lhs; rhs; op } -> + let lhs_type = c_ty lhs.span lhs.ty in + let rhs_type = c_ty rhs.span rhs.ty in + call + (mk_global ([ lhs_type; rhs_type ] ->. typ) + @@ `Primitive (LogicalOp (c_logical_op op))) + [ lhs; rhs ] + | Unary { arg; op } -> + (U.call + (match op with + | Not -> Core__ops__bit__Not__not + | Neg -> Core__ops__arith__Neg__neg) + [ c_expr arg ] + span typ) + .e + | Cast { source } -> + let source_type = c_ty source.span source.ty in + call + (mk_global ([ source_type ] ->. typ) @@ `Primitive Cast) + [ source ] + | Use { source } -> (c_expr source).e + | NeverToAny { source } -> (c_expr source).e + (* TODO: this is incorrect (NeverToAny) *) + | Pointer { cast; source } -> c_pointer e typ span cast source + | Loop { body } -> + let body = c_expr body in + Loop + { + body; + kind = UnconditionalLoop; + state = None; + label = None; + witness = W.loop; + } + | Match { scrutinee; arms } -> + let scrutinee = c_expr scrutinee in + let arms = List.map ~f:c_arm arms in + Match { scrutinee; arms } + | Let _ -> unimplemented e.span "Let" + | Block { safety_mode = BuiltinUnsafe | ExplicitUnsafe; _ } -> + unsafe_block e.span + | Block o -> + (* if there is no expression & the last expression is ⊥, just use that *) + let lift_last_statement_as_expr_if_possible expr stmts + (ty : Thir.ty) = + match (ty, expr, List.drop_last stmts, List.last stmts) with + | ( Thir.Never, + None, + Some stmts, + Some ({ kind = Thir.Expr { expr; _ }; _ } : Thir.stmt) ) -> + (stmts, Some expr) + | _ -> (stmts, expr) + in + let o_stmts, o_expr = + lift_last_statement_as_expr_if_possible o.expr o.stmts e.ty + in + let init = + Option.map ~f:c_expr o_expr + |> Option.value ~default:(unit_expr span) + in + let { e; _ } = + List.fold_right o_stmts ~init ~f:(fun { kind; _ } body -> + match kind with + | Expr { expr = rhs; _ } -> + let rhs = c_expr rhs in + let e = + Let + { + monadic = None; + lhs = wild_pat rhs.span rhs.typ; + rhs; + body; + } + in + let span = union_span rhs.span body.span in + { e; typ; span } + | Let { else_block = Some _; _ } -> + unimplemented ~issue_id:155 e.span + "Sorry, Hax does not support [let-else] (see \ + https://doc.rust-lang.org/rust-by-example/flow_control/let_else.html) \ + for now." + | Let { initializer' = None; _ } -> + unimplemented ~issue_id:156 e.span + "Sorry, Hax does not support declare-first let \ + bindings (see \ + https://doc.rust-lang.org/rust-by-example/variable_bindings/declare.html) \ + for now." + | Let { pattern = lhs; initializer' = Some rhs; _ } -> + let lhs = c_pat lhs in + let rhs = c_expr rhs in + let e = Let { monadic = None; lhs; rhs; body } in + let span = union_span rhs.span body.span in + { e; typ; span }) + in + e + | Assign { lhs; rhs } -> + let lhs = c_expr lhs in + let rhs = c_expr rhs in + c_expr_assign lhs rhs + | AssignOp { lhs; op; rhs } -> + let lhs = c_expr lhs in + c_expr_assign lhs @@ c_binop op lhs (c_expr rhs) span typ + | VarRef { id } -> LocalVar (local_ident id) + | Field { lhs; field } -> + let lhs = c_expr lhs in + let projector = + GlobalVar + (`Projector (`Concrete (Concrete_ident.of_def_id Field field))) + in + let span = c_span e.span in + App + { + f = { e = projector; typ = TArrow ([ lhs.typ ], typ); span }; + args = [ lhs ]; + } + | TupleField { lhs; field } -> + (* TODO: refactor *) + let tuple_len = 0 (* todo, lookup type *) in + let lhs = c_expr lhs in + let projector = + GlobalVar (`Projector (`TupleField (field, tuple_len))) + in + let span = c_span e.span in + App + { + f = { e = projector; typ = TArrow ([ lhs.typ ], typ); span }; + args = [ lhs ]; + } + | GlobalName { id } -> GlobalVar (def_id Value id) + | UpvarRef { var_hir_id = id; _ } -> LocalVar (local_ident id) + | Borrow { arg; borrow_kind = kind } -> + let e' = c_expr arg in + let kind = c_borrow_kind e.span kind in + Borrow { kind; e = e'; witness = W.reference } + | AddressOf { arg; mutability = mut } -> + let e = c_expr arg in + AddressOf + { + e; + mut = c_mutability W.mutable_pointer mut; + witness = W.raw_pointer; + } + | Break { value; _ } -> + (* TODO: labels! *) + let e = Option.map ~f:c_expr value in + let e = Option.value ~default:(unit_expr span) e in + Break { e; label = None; witness = W.loop } + | Continue _ -> + Continue { e = None; label = None; witness = (W.continue, W.loop) } + | Return { value } -> + let e = Option.map ~f:c_expr value in + let e = Option.value ~default:(unit_expr span) e in + Return { e; witness = W.early_exit } + | ConstBlock _ -> unimplemented e.span "ConstBlock" + | ConstParam { param = id } (* TODO: shadowing? *) | ConstRef { id } -> + LocalVar + { name = id.name; id = LocalIdent.const_id_of_int id.index } + | Repeat { value; count } -> + let value = c_expr value in + let count = c_expr count in + let inner = + U.call Rust_primitives__hax__repeat [ value; count ] span typ + in + (U.call Alloc__boxed__Impl__new [ inner ] span typ).e + | Tuple { fields } -> + (U.make_tuple_expr' ~span @@ List.map ~f:c_expr fields).e + | Array { fields } -> Array (List.map ~f:c_expr fields) + | Adt { info; base; fields; _ } -> + let constructor = + def_id + (Constructor { is_struct = info.typ_is_struct }) + info.variant + in + let base = + Option.map + ~f:(fun base -> (c_expr base.base, W.construct_base)) + base + in + let fields = + List.map + ~f:(fun f -> + let field = def_id Field f.field in + let value = c_expr f.value in + (field, value)) + fields + in + Construct + { + is_record = info.variant_is_record; + is_struct = info.typ_is_struct; + constructor; + fields; + base; + } + | Literal { lit; _ } -> ( + match c_lit e.span lit typ with + | EL_Lit lit -> Literal lit + | EL_U8Array l -> + Array + (List.map + ~f:(fun lit -> + { + e = Literal lit; + span; + typ = TInt { size = S8; signedness = Unsigned }; + }) + l)) + | NamedConst { def_id = id; _ } -> GlobalVar (def_id Value id) + | Closure { body; params; upvars; _ } -> + let params = + List.filter_map ~f:(fun p -> Option.map ~f:c_pat p.pat) params + in + let body = c_expr body in + let upvars = List.map ~f:c_expr upvars in + Closure { body; params; captures = upvars } + | Index { index; lhs } -> + let index_type = c_ty index.span index.ty in + let lhs_type = c_ty lhs.span lhs.ty in + call + (mk_global ([ lhs_type; index_type ] ->. typ) + @@ Global_ident.of_name Value Core__ops__index__Index__index) + [ lhs; index ] + | StaticRef { def_id = id; _ } -> GlobalVar (def_id Value id) + | PlaceTypeAscription _ -> + unimplemented e.span "expression PlaceTypeAscription" + | ValueTypeAscription _ -> + unimplemented e.span "expression ValueTypeAscription" + | ZstLiteral _ -> unimplemented e.span "expression ZstLiteral" + | Yield _ -> unimplemented e.span "expression Yield" + | Todo _ -> unimplemented e.span "expression Todo" + in + { e = v; span; typ } - and c_expr_assign lhs rhs = - let rec mk_lhs lhs = - match lhs.e with - | LocalVar var -> LhsLocalVar { var; typ = lhs.typ } - | _ -> ( - match resugar_index_mut lhs with - | Some (e, index) -> - LhsArrayAccessor - { - e = mk_lhs e; - typ = lhs.typ; - index; - witness = W.nontrivial_lhs; - } - | None -> ( - match (U.unbox_underef_expr lhs).e with - | App + and c_expr_assign lhs rhs = + let rec mk_lhs lhs = + match lhs.e with + | LocalVar var -> LhsLocalVar { var; typ = lhs.typ } + | _ -> ( + match resugar_index_mut lhs with + | Some (e, index) -> + LhsArrayAccessor { - f = - { - e = GlobalVar (`Projector _ as field); - typ = TArrow ([ _ ], _); - span = _; - }; - args = [ e ]; - } -> - LhsFieldAccessor + e = mk_lhs e; + typ = lhs.typ; + index; + witness = W.nontrivial_lhs; + } + | None -> ( + match (U.unbox_underef_expr lhs).e with + | App { - e = mk_lhs e; - typ = lhs.typ; - field; - witness = W.nontrivial_lhs; - } - | _ -> LhsArbitraryExpr { e = lhs; witness = W.arbitrary_lhs })) - in + f = + { + e = GlobalVar (`Projector _ as field); + typ = TArrow ([ _ ], _); + span = _; + }; + args = [ e ]; + } -> + LhsFieldAccessor + { + e = mk_lhs e; + typ = lhs.typ; + field; + witness = W.nontrivial_lhs; + } + | _ -> LhsArbitraryExpr { e = lhs; witness = W.arbitrary_lhs })) + in - Assign { lhs = mk_lhs lhs; e = rhs; witness = W.mutable_variable } + Assign { lhs = mk_lhs lhs; e = rhs; witness = W.mutable_variable } - and c_pat (pat : Thir.decorated_for__pat_kind) : pat = - let span = c_span pat.span in - let typ = c_ty pat.span pat.ty in - let v = - match pat.contents with - | Wild -> PWild - | AscribeUserType { ascription = { annotation; _ }; subpattern } -> - let typ, typ_span = c_canonical_user_type_annotation annotation in - let pat = c_pat subpattern in - PAscription { typ; typ_span; pat } - | Binding { mode; mutability; subpattern; ty; var; _ } -> - let mut = c_mutability W.mutable_variable mutability in - let subpat = - Option.map ~f:(c_pat &&& Fn.const W.as_pattern) subpattern - in - let typ = c_ty pat.span ty in - let mode = c_binding_mode pat.span mode in - let var = local_ident var in - PBinding { mut; mode; var; typ; subpat } - | Variant { info; subpatterns; _ } -> - let name = - def_id (Constructor { is_struct = info.typ_is_struct }) info.variant - in - let args = List.map ~f:(c_field_pat info) subpatterns in - PConstruct - { - name; - args; - is_record = info.variant_is_record; - is_struct = info.typ_is_struct; - } - | Tuple { subpatterns } -> - (List.map ~f:c_pat subpatterns |> U.make_tuple_pat').p - | Deref { subpattern } -> - PDeref { subpat = c_pat subpattern; witness = W.reference } - | Constant { value } -> ( - match c_constant_kind pat.span value with - | EL_Lit lit -> PConstant { lit } - | EL_Array l -> - PArray - { - args = - List.map - ~f:(fun lit -> - { - p = PConstant { lit }; - span; - typ = TInt { size = S8; signedness = Unsigned }; - }) - l; - }) - | Array _ -> unimplemented pat.span "Pat:Array" - | Or _ -> - unimplemented pat.span ~issue_id:161 - "Or patterns (see \ - https://rust-lang.github.io/rfcs/2535-or-patterns.html)" - | Slice _ -> unimplemented pat.span "Slice" - | Range _ -> unimplemented pat.span "Range" - in - { p = v; span; typ } + and c_pat (pat : Thir.decorated_for__pat_kind) : pat = + let span = c_span pat.span in + let typ = c_ty pat.span pat.ty in + let v = + match pat.contents with + | Wild -> PWild + | AscribeUserType { ascription = { annotation; _ }; subpattern } -> + let typ, typ_span = c_canonical_user_type_annotation annotation in + let pat = c_pat subpattern in + PAscription { typ; typ_span; pat } + | Binding { mode; mutability; subpattern; ty; var; _ } -> + let mut = c_mutability W.mutable_variable mutability in + let subpat = + Option.map ~f:(c_pat &&& Fn.const W.as_pattern) subpattern + in + let typ = c_ty pat.span ty in + let mode = c_binding_mode pat.span mode in + let var = local_ident var in + PBinding { mut; mode; var; typ; subpat } + | Variant { info; subpatterns; _ } -> + let name = + def_id + (Constructor { is_struct = info.typ_is_struct }) + info.variant + in + let args = List.map ~f:(c_field_pat info) subpatterns in + PConstruct + { + name; + args; + is_record = info.variant_is_record; + is_struct = info.typ_is_struct; + } + | Tuple { subpatterns } -> + (List.map ~f:c_pat subpatterns |> U.make_tuple_pat').p + | Deref { subpattern } -> + PDeref { subpat = c_pat subpattern; witness = W.reference } + | Constant { value } -> ( + match c_typed_constant_kind pat.span value with + | EL_Lit lit -> PConstant { lit } + | EL_U8Array l -> + PArray + { + args = + List.map + ~f:(fun lit -> + { + p = PConstant { lit }; + span; + typ = TInt { size = S8; signedness = Unsigned }; + }) + l; + }) + | Array _ -> unimplemented pat.span "Pat:Array" + | Or _ -> + unimplemented pat.span ~issue_id:161 + "Or patterns (see \ + https://rust-lang.github.io/rfcs/2535-or-patterns.html)" + | Slice _ -> unimplemented pat.span "Slice" + | Range _ -> unimplemented pat.span "Range" + in + { p = v; span; typ } - and c_field_pat info (field_pat : Thir.field_pat) : field_pat = - { field = def_id Field field_pat.field; pat = c_pat field_pat.pattern } + and c_field_pat info (field_pat : Thir.field_pat) : field_pat = + { field = def_id Field field_pat.field; pat = c_pat field_pat.pattern } - and c_constant_kind span (k : Thir.constant_kind) : extended_literal = - match k with - | Ty _ -> raise span GotTypeInLitPat - | Lit lit -> c_lit' span lit None - | Todo s -> unimplemented span ("TODO node: " ^ s) + and extended_literal_of_expr (e : expr) : extended_literal = + let not_a_literal () = + assertion_failure + (Diagnostics.to_thir_span e.span) + ("expected a literal, got " ^ [%show: expr] e) + in + match e.e with + | Literal lit -> EL_Lit lit + | Array lits -> + EL_U8Array + (List.map + ~f:(function + | { + e = + Literal + (Int { kind = { size = S8; signedness = Unsigned }; _ } + as lit); + } -> + lit + | _ -> not_a_literal ()) + lits) + | _ -> not_a_literal () - and c_canonical_user_type_annotation - (annotation : Thir.canonical_user_type_annotation) : ty * span = - (c_ty annotation.span annotation.inferred_ty, c_span annotation.span) + and c_typed_constant_kind span (k : Thir.typed_constant_kind) : + extended_literal = + match k.constant_kind with + | Ty e -> extended_literal_of_expr (c_expr e) + | Lit lit -> c_lit' span lit (c_ty span k.typ) + | Todo s -> unimplemented span ("TODO node: " ^ s) - and c_pointer e typ span cast source = - match cast with - | ReifyFnPointer -> - (* we have arrow types, we do not distinguish between top-level functions and closures *) - (c_expr source).e - | Unsize -> - (* https://doc.rust-lang.org/std/marker/trait.Unsize.html *) - (U.call Hax__CoerceUnsize__unsize [ c_expr source ] span typ).e - (* let source = c_expr source in *) - (* let from_typ = source.typ in *) - (* let to_typ = typ in *) - (* match (U.Box.Ty.destruct from_typ, U.Box.Ty.destruct to_typ) with *) - (* | Some _from_typ, Some to_typ -> ( *) - (* match U.Box.Expr.destruct source with *) - (* | Some source -> *) - (* (U.Box.Expr.make *) - (* @@ U.call "dummy" "unsize_cast" [] [ source ] span to_typ) *) - (* .e *) - (* | _ -> *) - (* unimplemented e.span *) - (* "[Pointer(Unsize)] cast from not directly boxed expression") *) - (* | _ -> *) - (* unimplemented e.span *) - (* ("[Pointer(Unsize)] cast\n • from type [" *) - (* ^ [%show: ty] from_typ *) - (* ^ "]\n • to type [" *) - (* ^ [%show: ty] to_typ *) - (* ^ "]\n\nThe expression is: " *) - (* ^ [%show: expr] source)) *) - | _ -> - unimplemented e.span - ("Pointer, with [cast] being " ^ [%show: Thir.pointer_cast] cast) + and c_canonical_user_type_annotation + (annotation : Thir.canonical_user_type_annotation) : ty * span = + (c_ty annotation.span annotation.inferred_ty, c_span annotation.span) - and c_ty (span : Thir.span) (ty : Thir.ty) : ty = - match ty with - | Bool -> TBool - | Char -> TChar - | Int k -> TInt (c_int_ty k) - | Uint k -> TInt (c_uint_ty k) - | Float _k -> TFloat - | Arrow { params; ret } -> - TArrow (List.map ~f:(c_ty span) params, c_ty span ret) - | NamedType { def_id = id; generic_args } -> - let ident = def_id Type id in - let args = List.map ~f:(c_generic_value span) generic_args in - TApp { ident; args } - | Foreign _ -> unimplemented span "Foreign" - | Str -> TStr - | Array (ty, len) -> TArray { typ = c_ty span ty; length = c_expr len } - | Slice ty -> - let ty = c_ty span ty in - TSlice { ty; witness = W.slice } - | RawPtr _ -> TRawPointer { witness = W.raw_pointer } - | Ref (_region, ty, mut) -> - let typ = c_ty span ty in - let mut = c_mutability W.mutable_reference mut in - TRef { witness = W.reference; region = "todo"; typ; mut } - | Never -> TFalse - | Tuple types -> - let types = List.map ~f:(fun ty -> GType (c_ty span ty)) types in - TApp { ident = `TupleType (List.length types); args = types } - | Alias _ -> TProjectedAssociatedType (Thir.show_ty ty) - (* | Opaque _ -> unimplemented span "type Opaque" *) - | Param { index; name } -> - (* TODO: [id] might not unique *) - TParam { name; id = LocalIdent.ty_param_id_of_int index } - | Error -> unimplemented span "type Error" - | Dynamic _ -> unimplemented span "type Dynamic" - | Generator _ -> unimplemented span "type Generator" - | Placeholder _ -> unimplemented span "type Placeholder" - | Bound _ -> unimplemented span "type Bound" - | Infer _ -> unimplemented span "type Infer" - | Todo _ -> unimplemented span "type Todo" - (* fun _ -> Ok Bool *) + and c_pointer e typ span cast source = + match cast with + | ReifyFnPointer -> + (* we have arrow types, we do not distinguish between top-level functions and closures *) + (c_expr source).e + | Unsize -> + (* https://doc.rust-lang.org/std/marker/trait.Unsize.html *) + (U.call Rust_primitives__unsize [ c_expr source ] span typ).e + (* let source = c_expr source in *) + (* let from_typ = source.typ in *) + (* let to_typ = typ in *) + (* match (U.Box.Ty.destruct from_typ, U.Box.Ty.destruct to_typ) with *) + (* | Some _from_typ, Some to_typ -> ( *) + (* match U.Box.Expr.destruct source with *) + (* | Some source -> *) + (* (U.Box.Expr.make *) + (* @@ U.call "dummy" "unsize_cast" [] [ source ] span to_typ) *) + (* .e *) + (* | _ -> *) + (* unimplemented e.span *) + (* "[Pointer(Unsize)] cast from not directly boxed expression") *) + (* | _ -> *) + (* unimplemented e.span *) + (* ("[Pointer(Unsize)] cast\n • from type [" *) + (* ^ [%show: ty] from_typ *) + (* ^ "]\n • to type [" *) + (* ^ [%show: ty] to_typ *) + (* ^ "]\n\nThe expression is: " *) + (* ^ [%show: expr] source)) *) + | _ -> + unimplemented e.span + ("Pointer, with [cast] being " ^ [%show: Thir.pointer_cast] cast) - and c_generic_value (span : Thir.span) (ty : Thir.generic_arg) : generic_value - = - match ty with - | Type ty -> GType (c_ty span ty) - | Const _e -> unimplemented span "c_generic_value:Const" - | _ -> GLifetime { lt = "todo generics"; witness = W.lifetime } + and c_ty (span : Thir.span) (ty : Thir.ty) : ty = + match ty with + | Bool -> TBool + | Char -> TChar + | Int k -> TInt (c_int_ty k) + | Uint k -> TInt (c_uint_ty k) + | Float k -> TFloat (match k with F32 -> F32 | F64 -> F64) + | Arrow { params; ret } -> + TArrow (List.map ~f:(c_ty span) params, c_ty span ret) + | NamedType { def_id = id; generic_args } -> + let ident = def_id Type id in + let args = List.map ~f:(c_generic_value span) generic_args in + TApp { ident; args } + | Foreign _ -> unimplemented span "Foreign" + | Str -> TStr + | Array (ty, len) -> TArray { typ = c_ty span ty; length = c_expr len } + | Slice ty -> + let ty = c_ty span ty in + TSlice { ty; witness = W.slice } + | RawPtr _ -> TRawPointer { witness = W.raw_pointer } + | Ref (_region, ty, mut) -> + let typ = c_ty span ty in + let mut = c_mutability W.mutable_reference mut in + TRef { witness = W.reference; region = "todo"; typ; mut } + | Never -> TFalse + | Tuple types -> + let types = List.map ~f:(fun ty -> GType (c_ty span ty)) types in + TApp { ident = `TupleType (List.length types); args = types } + | Alias _ -> TProjectedAssociatedType (Thir.show_ty ty) + (* | Opaque _ -> unimplemented span "type Opaque" *) + | Param { index; name } -> + (* TODO: [id] might not unique *) + TParam { name; id = LocalIdent.ty_param_id_of_int index } + | Error -> unimplemented span "type Error" + | Dynamic _ -> unimplemented span "type Dynamic" + | Generator _ -> unimplemented span "type Generator" + | Placeholder _ -> unimplemented span "type Placeholder" + | Bound _ -> unimplemented span "type Bound" + | Infer _ -> unimplemented span "type Infer" + | Todo _ -> unimplemented span "type Todo" + (* fun _ -> Ok Bool *) - and c_arm (arm : Thir.arm) : arm = - let arm_pat = c_pat arm.pattern in - let body = c_expr arm.body in - let span = c_span arm.span in - { arm = { arm_pat; body }; span } + and c_generic_value (span : Thir.span) (ty : Thir.generic_arg) : + generic_value = + match ty with + | Type ty -> GType (c_ty span ty) + | Const _e -> unimplemented span "c_generic_value:Const" + | _ -> GLifetime { lt = "todo generics"; witness = W.lifetime } - and c_param span (param : Thir.param) : param = - { - typ_span = Option.map ~f:c_span param.ty_span; - typ = c_ty (Option.value ~default:span param.ty_span) param.ty; - pat = c_pat (Option.value_exn param.pat); - } + and c_arm (arm : Thir.arm) : arm = + let arm_pat = c_pat arm.pattern in + let body = c_expr arm.body in + let span = c_span arm.span in + { arm = { arm_pat; body }; span } - let c_generic_param (param : Thir.generic_param) : generic_param = - let ident = - match param.name with - | Fresh -> - (* fail with ("[Fresh] ident? " ^ Thir.show_generic_param param) *) - (* TODO might be wrong to just have a wildcard here *) - ({ name = "_"; id = LocalIdent.ty_param_id_of_int 123 } : local_ident) - | Error -> assertion_failure param.span "[Error] ident" - | Plain n -> local_ident n - in - match (param.kind : Thir.generic_param_kind) with - | Lifetime _ -> GPLifetime { ident; witness = W.lifetime } - | Type { default; _ } -> - let default = Option.map ~f:(c_ty param.span) default in - GPType { ident; default } - | Const { default = Some _; _ } -> - unimplemented param.span "c_generic_param:Const with a default" - | Const { default = None; ty } -> - GPConst { ident; typ = c_ty param.span ty } + and c_param span (param : Thir.param) : param = + { + typ_span = Option.map ~f:c_span param.ty_span; + typ = c_ty (Option.value ~default:span param.ty_span) param.ty; + pat = c_pat (Option.value_exn param.pat); + } - let c_predicate_kind span (p : Thir.predicate_kind) : trait_ref option = - match p with - | Clause (Trait { is_positive = true; is_const = _; trait_ref }) -> - let args = List.map ~f:(c_generic_value span) trait_ref.generic_args in - Some - { - trait = Concrete_ident.of_def_id Trait trait_ref.def_id; - args; - bindings = []; - } - | _ -> None + let c_generic_param (param : Thir.generic_param) : generic_param = + let ident = + match param.name with + | Fresh -> + (* fail with ("[Fresh] ident? " ^ Thir.show_generic_param param) *) + (* TODO might be wrong to just have a wildcard here *) + ({ name = "_"; id = LocalIdent.ty_param_id_of_int 123 } + : local_ident) + | Error -> assertion_failure param.span "[Error] ident" + | Plain n -> local_ident n + in + match (param.kind : Thir.generic_param_kind) with + | Lifetime _ -> GPLifetime { ident; witness = W.lifetime } + | Type { default; _ } -> + let default = Option.map ~f:(c_ty param.span) default in + GPType { ident; default } + | Const { default = Some _; _ } -> + unimplemented param.span "c_generic_param:Const with a default" + | Const { default = None; ty } -> + GPConst { ident; typ = c_ty param.span ty } + + let c_predicate_kind span (p : Thir.predicate_kind) : trait_ref option = + match p with + | Clause (Trait { is_positive = true; is_const = _; trait_ref }) -> + let args = + List.map ~f:(c_generic_value span) trait_ref.generic_args + in + Some + { + trait = Concrete_ident.of_def_id Trait trait_ref.def_id; + args; + bindings = []; + } + | _ -> None - let c_constraint span (c : Thir.where_predicate) : generic_constraint list = - match c with - | BoundPredicate { bounded_ty; bounds; span; _ } -> - let typ = c_ty span bounded_ty in - let traits = List.map ~f:(c_predicate_kind span) bounds in - let traits = List.filter_map ~f:Fn.id traits in - List.map - ~f:(fun trait : generic_constraint -> - GCType { typ; implements = trait }) - traits - | RegionPredicate _ -> unimplemented span "region prediate" - | EqPredicate _ -> unimplemented span "EqPredicate" + let c_constraint span (c : Thir.where_predicate) : generic_constraint list = + match c with + | BoundPredicate { bounded_ty; bounds; span; _ } -> + let typ = c_ty span bounded_ty in + let traits = List.map ~f:(c_predicate_kind span) bounds in + let traits = List.filter_map ~f:Fn.id traits in + List.map + ~f:(fun trait : generic_constraint -> + GCType { typ; implements = trait }) + traits + | RegionPredicate _ -> unimplemented span "region prediate" + | EqPredicate _ -> unimplemented span "EqPredicate" - let list_dedup (equal : 'a -> 'a -> bool) : 'a list -> 'a list = - let rec aux (seen : 'a list) (todo : 'a list) : 'a list = - match todo with - | hd :: tl -> - if List.mem ~equal seen hd then aux seen tl - else hd :: aux (hd :: seen) tl - | _ -> todo - in - aux [] + let list_dedup (equal : 'a -> 'a -> bool) : 'a list -> 'a list = + let rec aux (seen : 'a list) (todo : 'a list) : 'a list = + match todo with + | hd :: tl -> + if List.mem ~equal seen hd then aux seen tl + else hd :: aux (hd :: seen) tl + | _ -> todo + in + aux [] - let c_generics (generics : Thir.generics) : generics = - { - params = List.map ~f:c_generic_param generics.params; - constraints = - List.concat_map ~f:(c_constraint generics.span) generics.predicates - |> list_dedup equal_generic_constraint; - } + let c_generics (generics : Thir.generics) : generics = + { + params = List.map ~f:c_generic_param generics.params; + constraints = + List.concat_map ~f:(c_constraint generics.span) generics.predicates + |> list_dedup equal_generic_constraint; + } - let c_trait_item' span (item : Thir.trait_item_kind) : trait_item' = - match item with - | Const (_, Some _) -> - unimplemented span - "TODO: traits: no support for defaults in traits for now" - | Const (ty, None) -> TIFn (c_ty span ty) - | ProvidedFn _ -> - unimplemented span - "TODO: traits: no support for defaults in funcitons for now" - | RequiredFn (sg, _) -> - let Thir.{ inputs; output; _ } = sg.decl in - let output = - match output with - | DefaultReturn _span -> unit_typ - | Return ty -> c_ty span ty - in - TIFn (TArrow (List.map ~f:(c_ty span) inputs, output)) - | Type (bounds, None) -> - let bounds = List.filter_map ~f:(c_predicate_kind span) bounds in - TIType bounds - | Type (_, Some _) -> - unimplemented span - "TODO: traits: no support for defaults in type for now" + let c_trait_item' span (item : Thir.trait_item_kind) : trait_item' = + match item with + | Const (_, Some _) -> + unimplemented span + "TODO: traits: no support for defaults in traits for now" + | Const (ty, None) -> TIFn (c_ty span ty) + | ProvidedFn _ -> + unimplemented span + "TODO: traits: no support for defaults in funcitons for now" + | RequiredFn (sg, _) -> + let Thir.{ inputs; output; _ } = sg.decl in + let output = + match output with + | DefaultReturn _span -> unit_typ + | Return ty -> c_ty span ty + in + TIFn (TArrow (List.map ~f:(c_ty span) inputs, output)) + | Type (bounds, None) -> + let bounds = List.filter_map ~f:(c_predicate_kind span) bounds in + TIType bounds + | Type (_, Some _) -> + unimplemented span + "TODO: traits: no support for defaults in type for now" + end + + let make ~krate : (module EXPR) = + let is_core_item = String.(krate = "core" || krate = "core_hax_model") in + let module M : EXPR = Make (struct + let is_core_item = is_core_item + end) in + (module M) let c_trait_item (item : Thir.trait_item) : trait_item = - (* Types.Param { index = 0; name = "Self" } *) + let open (val make ~krate:item.owner_id.krate : EXPR) in let { params; constraints } = c_generics item.generics in { ti_span = c_span item.span; @@ -798,6 +937,7 @@ module Exn = struct try c_item_unwrapped item with Diagnostics.SpanFreeError _kind -> [] and c_item_unwrapped (item : Thir.item) : item list = + let open (val make ~krate:item.owner_id.krate : EXPR) in if (* We need something better here, see issue #108 *) List.exists @@ -1005,7 +1145,7 @@ module Exn = struct in (* ident is supposed to always be an actual item, thus here we need to cheat a bit *) let def_id = item.owner_id in - let def_id = + let def_id : Types.def_id = { def_id with path = @@ -1020,5 +1160,4 @@ module Exn = struct end let c_item (item : Thir.item) : (item list, error) Result.t = - try Exn.c_item item |> Result.return - with Exn.ImportError error -> Error error + Exn.c_item item |> Result.return diff --git a/frontend/exporter/src/all.rs b/frontend/exporter/src/all.rs index 010bbbfc6..b0358ebfa 100644 --- a/frontend/exporter/src/all.rs +++ b/frontend/exporter/src/all.rs @@ -268,6 +268,22 @@ impl<'tcx, S: BaseState<'tcx> + HasThir<'tcx>> SInto } } +impl<'tcx, S: BaseState<'tcx> + HasThir<'tcx>> SInto + for rustc_middle::mir::ConstantKind<'tcx> +{ + fn sinto(&self, s: &S) -> TypedConstantKind { + TypedConstantKind { + typ: self.ty().sinto(s), + constant_kind: self.sinto(s), + } + } +} +#[derive(Clone, Debug, Serialize, Deserialize, JsonSchema)] +pub struct TypedConstantKind { + typ: Ty, + constant_kind: ConstantKind, +} + #[derive(Clone, Debug, Serialize, Deserialize, JsonSchema)] pub enum ConstantKind { Ty(Const), @@ -1947,8 +1963,8 @@ pub enum RangeEnd { #[args(<'tcx, S: BaseState<'tcx> + HasThir<'tcx>>, from: rustc_middle::thir::PatRange<'tcx>, state: S as state)] #[derive(Clone, Debug, Serialize, Deserialize, JsonSchema)] pub struct PatRange { - pub lo: ConstantKind, - pub hi: ConstantKind, + pub lo: TypedConstantKind, + pub hi: TypedConstantKind, pub end: RangeEnd, } @@ -2102,7 +2118,7 @@ pub enum PatKind { /// * Opaque constants, that must not be matched structurally. So anything that does not derive /// `PartialEq` and `Eq`. Constant { - value: ConstantKind, + value: TypedConstantKind, }, Range(PatRange),