diff --git a/engine/lib/analyses/function_dependency.ml b/engine/lib/analyses/function_dependency.ml index 8a42ee869..fbc4d8de5 100644 --- a/engine/lib/analyses/function_dependency.ml +++ b/engine/lib/analyses/function_dependency.ml @@ -14,7 +14,7 @@ module%inlined_contents Make (F : Features.T) = struct Ast_utils.MakeWithNamePolicy (F) (Concrete_ident.DefaultNamePolicy) let analyse (items : A.item list) : analysis_data = - let temp_list = List.concat_map ~f:U.functions_of_item items in + let temp_list = List.concat_map ~f:U.Destruct.Item.functions items in List.fold_left ~init:(Map.empty (module String)) ~f:(fun y (name, body) -> diff --git a/engine/lib/analyses/mutable_variables.ml b/engine/lib/analyses/mutable_variables.ml index 340167179..ddf9acad8 100644 --- a/engine/lib/analyses/mutable_variables.ml +++ b/engine/lib/analyses/mutable_variables.ml @@ -164,7 +164,7 @@ module%inlined_contents Make (F : Features.T) = struct ~f:(fun (y, count) (name, body) -> let items, count = analyse_function_body body count in (y @ [ (name, items) ], count)) - (List.concat_map ~f:U.functions_of_item items) + (List.concat_map ~f:U.Destruct.Item.functions items) in let mut_map (* Concrete_ident *) : (Local_ident.t list * (U.TypedLocalIdent.t * id_order) list) diff --git a/engine/lib/ast.ml b/engine/lib/ast.ml index bc14ddfd2..76aaa7b3c 100644 --- a/engine/lib/ast.ml +++ b/engine/lib/ast.ml @@ -631,7 +631,7 @@ functor (s : string) : item = { v = HaxError s; span; ident; attrs = [] } - module F = F + (* module F = F *) end module type T = sig diff --git a/engine/lib/ast_utils.ml b/engine/lib/ast_utils.ml deleted file mode 100644 index a2486af98..000000000 --- a/engine/lib/ast_utils.ml +++ /dev/null @@ -1,1084 +0,0 @@ -open! Prelude -open Ast - -type visit_level = ExprLevel | TypeLevel - -module TypedLocalIdent (Ty : sig - type ty [@@deriving show, yojson] -end) = -struct - module T = struct - type t = Local_ident.t * Ty.ty [@@deriving show, yojson] - - let sexp_of_t : t -> _ = fst >> Local_ident.sexp_of_t - let compare (a : t) (b : t) = [%compare: Local_ident.t] (fst a) (fst b) - let equal (a : t) (b : t) = [%eq: Local_ident.t] (fst a) (fst b) - end - - include Base.Comparator.Make (T) - include T -end - -module UniqueList (T : sig - type t [@@deriving eq, show, yojson] - type comparator_witness -end) : sig - type t [@@deriving eq, show, yojson] - - val without : T.t -> t -> t - val cons : T.t -> t -> t - val to_list : t -> T.t list - val from_set : (T.t, T.comparator_witness) Set.t -> t - val empty : t - val is_empty : t -> bool - val singleton : T.t -> t -end = struct - type t = T.t list [@@deriving eq, show, yojson] - - let without x = List.filter ~f:([%eq: T.t] x >> not) - let cons hd tl = hd :: tl - let to_list = Fn.id - let from_set s = Set.to_list s - let empty = [] - let is_empty = List.is_empty - let singleton x = [ x ] -end - -module Make (F : Features.T) = struct - module AST = Ast.Make (F) - open AST - module TypedLocalIdent = TypedLocalIdent (AST) - - module Expect = struct - let mut_borrow (e : expr) : expr option = - match e.e with Borrow { kind = Mut _; e; _ } -> Some e | _ -> None - - let deref (e : expr) : expr option = - match e.e with - | App { f = { e = GlobalVar (`Primitive Deref); _ }; args = [ e ]; _ } -> - Some e - | _ -> None - - let concrete_app1 (f : Concrete_ident.name) (e : expr) : expr option = - match e.e with - | App - { - f = { e = GlobalVar (`Concrete f'); _ }; - args = [ e ]; - generic_args = _; - impl = _; - (* TODO: see issue #328 *) - } - when Concrete_ident.eq_name f f' -> - Some e - | _ -> None - - let deref_mut_app = concrete_app1 Core__ops__deref__DerefMut__deref_mut - - let local_var (e : expr) : expr option = - match e.e with LocalVar _ -> Some e | _ -> None - - let arrow (typ : ty) : (ty list * ty) option = - match typ with - | TArrow (inputs, output) -> Some (inputs, output) - | _ -> None - - let mut_ref (typ : ty) : ty option = - match typ with TRef { mut = Mutable _; typ; _ } -> Some typ | _ -> None - - let concrete_app' : expr' -> concrete_ident option = function - | App { f = { e = GlobalVar (`Concrete c); _ }; _ } -> Some c - | _ -> None - end - - module Sets = struct - module Global_ident = struct - include Set.M (Global_ident) - - class ['s] monoid = - object - inherit ['s] VisitorsRuntime.monoid - method private zero = Set.empty (module Global_ident) - method private plus = Set.union - end - end - - module Concrete_ident = struct - include Set.M (Concrete_ident) - - class ['s] monoid = - object - inherit ['s] VisitorsRuntime.monoid - method private zero = Set.empty (module Concrete_ident) - method private plus = Set.union - end - end - - module Local_ident = struct - include Set.M (Local_ident) - - class ['s] monoid = - object - inherit ['s] VisitorsRuntime.monoid - method private zero = Set.empty (module Local_ident) - method private plus = Set.union - end - end - - module TypedLocalIdent = struct - include Set.M (TypedLocalIdent) - - let show (x : t) : string = - [%show: TypedLocalIdent.t list] @@ Set.to_list x - - let pp (fmt : Stdlib.Format.formatter) (s : t) : unit = - Stdlib.Format.pp_print_string fmt @@ show s - - class ['s] monoid = - object - inherit ['s] VisitorsRuntime.monoid - method private zero = Set.empty (module TypedLocalIdent) - method private plus = Set.union - end - end - end - - let functions_of_item (x : item) : (concrete_ident * expr) list = - match x.v with - | Fn { name; generics = _; body; params = _ } -> [ (name, body) ] - | Impl { items; _ } -> - List.filter_map - ~f:(fun w -> - match w.ii_v with - | IIFn { body; params = _ } -> Some (w.ii_ident, body) - | _ -> None) - items - | _ -> [] - - module Mappers = struct - let regenerate_span_ids = - object - inherit [_] item_map - method visit_t () x = x - method visit_mutability _ () m = m - method visit_span = Fn.const Span.refresh_id - end - - let normalize_borrow_mut = - object - inherit [_] expr_map as super - method visit_t () x = x - method visit_mutability _ () m = m - - method! visit_expr s e = - let rec expr e = - match e.e with - | App - { - f = { e = GlobalVar (`Primitive Deref); _ }; - args = [ { e = Borrow { e = sub; _ }; _ } ]; - generic_args = _; - impl = _; - (* TODO: see issue #328 *) - } -> - expr sub - | _ -> super#visit_expr s e - in - expr e - end - - let rename_generic_constraints = - object - inherit [_] item_map as _super - method visit_t _ x = x - method visit_mutability _ _ m = m - - method! visit_GCType (s : (string, string) Hashtbl.t) bound id = - let data = "i" ^ Int.to_string (Hashtbl.length s) in - let _ = Hashtbl.add s ~key:id ~data in - GCType { bound; id = data } - - method! visit_LocalBound s id = - LocalBound { id = Hashtbl.find s id |> Option.value ~default:id } - end - - let rename_local_idents (f : local_ident -> local_ident) = - object - inherit [_] item_map as _super - method visit_t () x = x - method visit_mutability _ () m = m - method! visit_local_ident () ident = f ident - end - - let rename_global_idents (f : visit_level -> global_ident -> global_ident) = - object - inherit [_] item_map as super - method visit_t (_lvl : visit_level) x = x - method visit_mutability _ (_lvl : visit_level) m = m - method! visit_global_ident (lvl : visit_level) ident = f lvl ident - method! visit_ty _ t = super#visit_ty TypeLevel t - (* method visit_GlobalVar (lvl : level) i = GlobalVar (f lvl i) *) - end - - let rename_concrete_idents - (f : visit_level -> Concrete_ident.t -> Concrete_ident.t) = - object - inherit [_] item_map as super - method visit_t (_lvl : visit_level) x = x - method visit_mutability _ (_lvl : visit_level) m = m - method! visit_concrete_ident (lvl : visit_level) ident = f lvl ident - - method! visit_global_ident lvl (x : Global_ident.t) = - match x with - | `Concrete x -> `Concrete (f lvl x) - | _ -> super#visit_global_ident lvl x - - method! visit_ty _ t = super#visit_ty TypeLevel t - end - - let rename_global_idents_item - (f : visit_level -> global_ident -> global_ident) : item -> item = - (rename_global_idents f)#visit_item ExprLevel - - (** Add type ascription nodes in nested function calls. This helps - type inference in the presence of associated types in backends - that don't support them well (F* for instance). *) - let add_typ_ascription = - let is_app = Expect.concrete_app' >> Option.is_some in - let o = - object - inherit [_] item_map as super - method visit_t (_ascribe_app : bool) x = x - method visit_mutability _ (_ascribe_app : bool) m = m - - method! visit_expr' (ascribe_app : bool) e = - (* Enable type ascription of underlying function - application. In the F* backend, we're annotating every - [Let] bindings, thus if we're facing a [Let], we turn - off application ascription. Similarly, if we're facing - an Ascription, we turn off application ascription. *) - let ascribe_app = - (ascribe_app || is_app e) - && not ([%matches? Let _ | Ascription _] e) - in - super#visit_expr' ascribe_app e - - method! visit_expr (ascribe_app : bool) e = - let e = super#visit_expr ascribe_app e in - let ascribe (e : expr) = - if [%matches? Ascription _] e.e then e - else { e with e = Ascription { e; typ = e.typ } } - in - match e.e with - | App - { - f = { e = GlobalVar (`Primitive Cast); _ } as f; - args = [ arg ]; - generic_args; - impl; - } -> - ascribe - { - e with - e = App { f; args = [ ascribe arg ]; generic_args; impl }; - } - | _ -> - (* Ascribe the return type of a function application & constructors *) - if (ascribe_app && is_app e.e) || [%matches? Construct _] e.e - then ascribe e - else e - end - in - o#visit_item false - end - - module Reducers = struct - let collect_local_idents = - object - inherit [_] item_reduce as _super - inherit [_] Sets.Local_ident.monoid as m - method visit_t _ _ = m#zero - method visit_mutability (_f : unit -> _ -> _) () _ = m#zero - method! visit_local_ident _ x = Set.singleton (module Local_ident) x - end - - include struct - open struct - type env = Local_ident.t list - - let id_shadows ~(env : env) (id : Local_ident.t) = - List.find env ~f:(fun x -> String.equal x.name id.name) - |> Option.value ~default:id - |> [%equal: Local_ident.t] id - |> not - - let ( ++ ) = Set.union - - let shadows' (type a) ~env vars (x : a) next = - (* account for shadowing within `vars` *) - List.filter ~f:(id_shadows ~env:vars) (List.rev vars) - |> Set.of_list (module Local_ident) - |> Set.union (next (vars @ env) x) - - let shadows (type a) ~(env : env) (pats : pat list) (x : a) - (next : env -> a -> Sets.Local_ident.t) = - let vars = - List.map pats ~f:(collect_local_idents#visit_pat ()) - |> Set.(union_list (module Local_ident) >> to_list) - in - shadows' ~env vars x next - end - - let collect_ambiguous_local_idents = - object (self) - inherit [_] item_reduce as super - inherit [_] Sets.Local_ident.monoid as m - method visit_t (_ : env) _ = m#zero - method visit_mutability (_f : env -> _ -> _) _ _ = m#zero - - method visit_arm' env { arm_pat; body } = - shadows ~env [ arm_pat ] body super#visit_expr - - method visit_expr' env e = - match e with - | Let { monadic = _; lhs; rhs; body } -> - super#visit_expr env rhs - ++ shadows ~env [ lhs ] body super#visit_expr - | Loop { kind; state; body; _ } -> - let empty = Set.empty (module Local_ident) |> Fn.(id &&& id) in - let ikind, ukind = - match kind with - | UnconditionalLoop -> empty - | ForLoop { pat; it; _ } -> - ( collect_local_idents#visit_pat () pat, - super#visit_expr env it ) - | ForIndexLoop { start; end_; var; _ } -> - ( Set.singleton (module Local_ident) var, - super#visit_expr (var :: env) start - ++ super#visit_expr (var :: env) end_ ) - in - let istate, ustate = - match state with - | Some { init; bpat; _ } -> - ( collect_local_idents#visit_pat () bpat, - super#visit_expr (Set.to_list ikind @ env) init ) - | _ -> empty - in - let intro = ikind ++ istate |> Set.to_list in - ukind ++ ustate ++ shadows' ~env intro body super#visit_expr - | Closure { params; body; _ } -> - shadows ~env params body super#visit_expr - | _ -> super#visit_expr' env e - - method visit_IIFn = self#visit_function_like - method visit_Fn env _ _ = self#visit_function_like env - - method visit_function_like env body params = - let f p = p.pat in - shadows ~env (List.map ~f params) body super#visit_expr - - method visit_local_ident env id = - Set.(if id_shadows ~env id then Fn.flip singleton id else empty) - (module Local_ident) - end - - let disambiguate_local_idents (item : item) = - let ambiguous = collect_ambiguous_local_idents#visit_item [] item in - let local_vars = collect_local_idents#visit_item () item |> ref in - let refresh env (id : Local_ident.t) : string = - let extract_suffix (id' : Local_ident.t) = - String.chop_prefix ~prefix:(id.name ^ "_") id'.name - |> Option.bind ~f:string_to_int - in - let suffix = - Set.filter_map (module Int) env ~f:extract_suffix - |> Set.max_elt |> Option.value ~default:0 |> ( + ) 1 - in - id.name ^ "_" ^ Int.to_string suffix - in - let new_names = - ambiguous |> Set.to_list - |> List.map ~f:(fun (var : Local_ident.t) -> - let var' = { var with name = refresh !local_vars var } in - local_vars := Set.add !local_vars var'; - (var, var')) - |> Map.of_alist_exn (module Local_ident) - in - let rename var = Map.find new_names var |> Option.value ~default:var in - (Mappers.rename_local_idents rename)#visit_item () item - end - - let collect_global_idents = - object - inherit ['self] item_reduce as _super - inherit [_] Sets.Global_ident.monoid as m - method visit_t _ _ = m#zero - method visit_mutability (_f : unit -> _ -> _) () _ = m#zero - - method! visit_global_ident (_env : unit) (x : Global_ident.t) = - Set.singleton (module Global_ident) x - end - - let collect_concrete_idents = - object - inherit ['self] item_reduce as super - inherit [_] Sets.Concrete_ident.monoid as m - method visit_t _ _ = m#zero - method visit_mutability (_f : unit -> _ -> _) () _ = m#zero - - method! visit_global_ident (_env : unit) (x : Global_ident.t) = - match x with - | `Concrete x -> Set.singleton (module Concrete_ident) x - | _ -> super#visit_global_ident () x - - method! visit_concrete_ident (_env : unit) (x : Concrete_ident.t) = - Set.singleton (module Concrete_ident) x - end - - let variables_of_pat (p : pat) : Sets.Local_ident.t = - (object - inherit [_] expr_reduce as super - inherit [_] Sets.Local_ident.monoid as m - method visit_t _ _ = m#zero - method visit_mutability (_f : unit -> _ -> _) () _ = m#zero - - method! visit_PBinding env _ _ var _ subpat = - m#plus - (Set.singleton (module Local_ident) var) - (Option.value_map subpat ~default:m#zero - ~f:(fst >> super#visit_pat env)) - end) - #visit_pat - () p - - let variables_of_param (p : param) : Local_ident.t list = - variables_of_pat p.pat |> Set.to_list - - let variables_of_pats : pat list -> Sets.Local_ident.t = - List.map ~f:variables_of_pat >> Set.union_list (module Local_ident) - - let without_vars (mut_vars : Sets.TypedLocalIdent.t) - (vars : Sets.Local_ident.t) = - Set.filter mut_vars ~f:(fst >> Set.mem vars >> not) - - let without_pats_vars (mut_vars : Sets.TypedLocalIdent.t) : - pat list -> Sets.TypedLocalIdent.t = - variables_of_pats >> without_vars mut_vars - - let without_pat_vars (mut_vars : Sets.TypedLocalIdent.t) (pat : pat) : - Sets.TypedLocalIdent.t = - without_pats_vars mut_vars [ pat ] - - let free_assigned_variables - (fv_of_arbitrary_lhs : - F.arbitrary_lhs -> expr -> Sets.TypedLocalIdent.t) = - object - inherit [_] expr_reduce as super - inherit [_] Sets.TypedLocalIdent.monoid as m - method visit_t _ _ = m#zero - method visit_mutability (_f : unit -> _ -> _) () _ = m#zero - - (* TODO: loop state *) - - method visit_Assign _env lhs e _wit = - let rec visit_lhs lhs = - match lhs with - | LhsLocalVar { var; _ } -> - Set.singleton (module TypedLocalIdent) (var, e.typ) - | LhsFieldAccessor { e; _ } -> visit_lhs e - | LhsArrayAccessor { e; index; _ } -> - Set.union (super#visit_expr () index) (visit_lhs e) - | LhsArbitraryExpr { witness; e } -> fv_of_arbitrary_lhs witness e - in - visit_lhs lhs - - method visit_Match env scrut arms = - List.fold_left ~init:(super#visit_expr env scrut) ~f:Set.union - @@ List.map ~f:(fun arm -> super#visit_arm env arm) arms - - method visit_Let env _monadic pat expr body = - Set.union (super#visit_expr env expr) - @@ without_pat_vars (super#visit_expr env body) pat - - method visit_Closure env params body _captures = - without_pats_vars (super#visit_expr env body) params - - method visit_Loop env body kind state _label _witness = - let vars = - (match kind with - | UnconditionalLoop -> [] - | ForLoop { pat = _not_mutable; _ } -> [] - | ForIndexLoop { var = _not_mutable; _ } -> []) - @ (state - |> Option.map ~f:(fun { bpat; _ } -> variables_of_pat bpat) - |> Option.to_list) - |> Set.union_list (module Local_ident) - in - m#plus - (super#visit_loop_kind env kind) - (m#plus - (Option.map ~f:(super#visit_loop_state env) state - |> Option.value ~default:m#zero) - (without_vars (super#visit_expr env body) vars)) - - method visit_arm' env { arm_pat; body } = - without_pat_vars (super#visit_expr env body) arm_pat - end - - class ['s] expr_list_monoid = - object - inherit ['s] VisitorsRuntime.monoid - method private zero = [] - method private plus = List.append - end - - let collect_break_payloads = - object - inherit [_] expr_reduce as super - inherit [_] expr_list_monoid as m - method visit_t _ _ = m#zero - method visit_mutability (_f : unit -> _ -> _) () _ = m#zero - method visit_Break _ e _ _ = m#plus (super#visit_expr () e) [ e ] - - method visit_Loop _ _ _ _ _ _ = (* Do *NOT* visit sub nodes *) - m#zero - end - end - - (** Produces a local identifier which is locally fresh **with respect - to expressions {exprs}**. *) - let fresh_local_ident_in_expr (exprs : expr list) (prefix : string) : - Local_ident.t = - let free_suffix = - List.map ~f:(Reducers.collect_local_idents#visit_expr ()) exprs - |> Set.union_list (module Local_ident) - |> Set.to_list - |> List.filter_map ~f:(fun ({ name; _ } : local_ident) -> - String.chop_prefix ~prefix name) - |> List.map ~f:(function "" -> "0" | s -> s) - |> List.filter_map ~f:Stdlib.int_of_string_opt - |> List.fold ~init:(-1) ~f:Int.max - |> ( + ) 1 - |> function - | 0 -> "" - | n -> Int.to_string n - in - { - name = prefix ^ free_suffix; - id = - (* TODO: freshness is local and name-only here... *) - Local_ident.mk_id Expr (-1); - } - - let never_typ : ty = - let ident = - `Concrete (Concrete_ident.of_name Type Rust_primitives__hax__Never) - in - TApp { ident; args = [] } - - let is_never_typ : ty -> bool = function - | TApp { ident; _ } -> - Global_ident.eq_name Rust_primitives__hax__Never ident - | _ -> false - - let unit_typ : ty = TApp { ident = `TupleType 0; args = [] } - - let unit_expr span : expr = - { typ = unit_typ; span; e = GlobalVar (`TupleCons 0) } - - (* TODO: Those tuple1 things are wrong! Tuples of size one exists in Rust! e.g. `(123,)` *) - let rec remove_tuple1_pat (p : pat) : pat = - match p.p with - | PConstruct { name = `TupleType 1; args = [ { pat; _ } ]; _ } -> - remove_tuple1_pat pat - | _ -> p - - let rec remove_tuple1 (t : ty) : ty = - match t with - | TApp { ident = `TupleType 1; args = [ GType t ] } -> remove_tuple1 t - | _ -> t - - let remove_unsize (e : expr) : expr = - match e.e with - | App { f = { e = GlobalVar f; _ }; args = [ e ]; _ } - when Global_ident.eq_name Rust_primitives__unsize f -> - e - | _ -> e - - (* let rec remove_empty_tap *) - - let is_unit_typ : ty -> bool = - remove_tuple1 >> [%matches? TApp { ident = `TupleType 0; _ }] - - let rec pat_is_expr (p : pat) (e : expr) = - match (p.p, e.e) with - | _, Construct { constructor = `TupleCons 1; fields = [ (_, e) ]; _ } -> - pat_is_expr p e - | PBinding { subpat = None; var = pv; _ }, LocalVar ev -> - [%eq: local_ident] pv ev - | ( PConstruct { name = pn; args = pargs; _ }, - Construct { constructor = en; fields = eargs; base = None; _ } ) - when [%eq: global_ident] pn en -> ( - match List.zip pargs eargs with - | Ok zip -> - List.for_all - ~f:(fun (x, y) -> - [%eq: global_ident] x.field (fst y) && pat_is_expr x.pat (snd y)) - zip - | Unequal_lengths -> false) - | _ -> false - - let make_let (lhs : pat) (rhs : expr) (body : expr) = - if pat_is_expr lhs body then rhs - else { body with e = Let { monadic = None; lhs; rhs; body } } - - let make_var_pat (var : local_ident) (typ : ty) (span : span) : pat = - { - p = PBinding { mut = Immutable; mode = ByValue; var; typ; subpat = None }; - span; - typ; - } - - let ty_equality (a : ty) (b : ty) : bool = - let replace_spans = - object - inherit [_] item_map - method visit_t () x = x - method visit_mutability _ () m = m - method! visit_span _ = function _ -> Span.default - end - in - let a = replace_spans#visit_ty () a in - let b = replace_spans#visit_ty () b in - [%eq: ty] a b - - let let_of_binding ((var, rhs) : local_ident * expr) (body : expr) : expr = - make_let (make_var_pat var rhs.typ rhs.span) rhs body - - let lets_of_bindings (bindings : (local_ident * expr) list) (body : expr) : - expr = - List.fold_right ~init:body ~f:let_of_binding bindings - - let make_tuple_typ' (tuple : ty list) : ty = - TApp - { - ident = `TupleType (List.length tuple); - args = List.map ~f:(fun typ -> GType typ) tuple; - } - - 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_unit_param (span : span) : param = - let typ = unit_typ in - let pat = make_wild_pat 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 - - let make_tuple_field_pat (len : int) (nth : int) (pat : pat) : field_pat = - { field = `TupleField (nth + 1, len); pat } - - let make_tuple_pat'' span (tuple : field_pat list) : pat = - match tuple with - | [ { pat; _ } ] -> pat - | _ -> - let len = List.length tuple in - { - p = - PConstruct - { - name = `TupleCons len; - args = tuple; - is_record = false; - is_struct = true; - }; - typ = make_tuple_typ @@ List.map ~f:(fun { pat; _ } -> pat.typ) tuple; - span; - } - - let make_tuple_pat' (pats : pat list) : pat = - let len = List.length pats in - let span = Span.union_list @@ List.map ~f:(fun p -> p.span) pats in - List.mapi ~f:(fun i pat -> { field = `TupleField (i, len); pat }) pats - |> make_tuple_pat'' span - - let make_tuple_pat : pat list -> pat = function - | [ pat ] -> pat - | pats -> make_tuple_pat' pats - - let make_tuple_expr' ~(span : span) (tuple : expr list) : expr = - let len = List.length tuple in - { - e = - Construct - { - constructor = `TupleCons len; - is_record = false; - is_struct = true; - fields = - List.mapi ~f:(fun i x -> (`TupleField (i, len), x)) @@ tuple; - base = None; - }; - typ = make_tuple_typ @@ List.map ~f:(fun { typ; _ } -> typ) tuple; - span; - } - - let make_tuple_expr ~(span : span) : expr list -> expr = function - | [ e ] -> e - | es -> make_tuple_expr' ~span es - - (* maybe we should just drop Construct in favor of a - [Record] thing, and put everything which is not a Record - into an App. This would simplify stuff quite much. Maybe not - for LHS things. *) - let call_Constructor' (constructor : global_ident) is_struct - (args : expr list) span ret_typ = - let mk_field = - let len = List.length args in - fun n -> `TupleField (len, n) - in - let fields = List.mapi ~f:(fun i arg -> (mk_field i, arg)) args in - { - e = - Construct - { constructor; is_record = false; is_struct; fields; base = None }; - typ = ret_typ; - span; - } - - let call_Constructor (constructor_name : Concrete_ident.name) - (is_struct : bool) (args : expr list) span ret_typ = - call_Constructor' - (`Concrete - (Concrete_ident.of_name (Constructor { is_struct }) constructor_name)) - is_struct args span ret_typ - - let call' f (args : expr list) span ret_typ = - let typ = TArrow (List.map ~f:(fun arg -> arg.typ) args, ret_typ) in - let e = GlobalVar f in - { - e = - App - { - f = { e; typ; span }; - args; - generic_args = []; - impl = - None - (* TODO: see issue #328, and check that for evrey call to `call'` *); - }; - typ = ret_typ; - span; - } - - let call ?(kind : Concrete_ident.Kind.t = Value) - (f_name : Concrete_ident.name) (args : expr list) span ret_typ = - call' (`Concrete (Concrete_ident.of_name kind f_name)) args span ret_typ - - let string_lit span (s : string) : expr = - { span; typ = TStr; e = Literal (String s) } - - let hax_failure_expr' span (typ : ty) (context, kind) (ast : string) = - let error = Diagnostics.pretty_print_context_kind context kind in - let args = List.map ~f:(string_lit span) [ error; ast ] in - call Rust_primitives__hax__failure args span typ - - let hax_failure_expr span (typ : ty) (context, kind) (expr0 : Ast.Full.expr) = - hax_failure_expr' span typ (context, kind) (Print_rust.pexpr_str expr0) - - let hax_failure_typ = - let ident = - `Concrete (Concrete_ident.of_name Type Rust_primitives__hax__failure) - in - TApp { ident; args = [] } - - module LiftToFullAst = struct - let expr : AST.expr -> Ast.Full.expr = Stdlib.Obj.magic - let item : AST.item -> Ast.Full.item = Stdlib.Obj.magic - end - - let unbox_expr' (next : expr -> expr) (e : expr) : expr = - match e.e with - | App { f = { e = GlobalVar f; _ }; args = [ e ]; _ } - when Global_ident.eq_name Alloc__boxed__Impl__new f -> - next e - | _ -> e - - let underef_expr' (next : expr -> expr) (e : expr) : expr = - match e.e with - | App - { - f = { e = GlobalVar (`Primitive Ast.Deref); _ }; - args = [ e ]; - generic_args = _; - impl = _; - } -> - next e - | _ -> e - - let rec unbox_expr e = unbox_expr' unbox_expr e - let underef_expr e = underef_expr' unbox_expr e - - let rec unbox_underef_expr e = - (unbox_expr' unbox_underef_expr >> underef_expr' unbox_underef_expr) e - - (* extracts a `param` out of a `generic_param` if it's a const - generic, otherwise returns `None`` *) - let param_of_generic_const_param (g : generic_param) : param option = - let* typ = match g.kind with GPConst { typ } -> Some typ | _ -> None in - let ({ span; ident = var; _ } : generic_param) = g in - let pat = - let mode, mut, subpat = (ByValue, Immutable, None) in - { p = PBinding { mut; mode; var; typ; subpat }; span; typ } - in - Some { pat; typ; typ_span = Some span; attrs = [] } - - let rec expr_of_lhs (span : span) (lhs : lhs) : expr = - match lhs with - | LhsLocalVar { var; typ } -> { e = LocalVar var; typ; span } - | LhsFieldAccessor { e; typ; field; _ } -> - let e = expr_of_lhs span e in - let f = { e = GlobalVar field; typ = TArrow ([ e.typ ], typ); span } in - { - e = - App - { - f; - args = [ e ]; - generic_args = []; - impl = None (* TODO: see issue #328 *); - }; - typ; - span; - } - | LhsArrayAccessor { e; typ; index; _ } -> - let args = [ expr_of_lhs span e; index ] in - call Core__ops__index__Index__index args span typ - | LhsArbitraryExpr { e; _ } -> e - - (* module Box = struct *) - (* module Ty = struct *) - (* let destruct (t : ty) : ty option = *) - (* match t with *) - (* | TApp { ident = `Concrete box; args = [ GType sub; _alloc ] } *) - (* when Concrete_ident.eq_name Alloc__boxed__Box box -> *) - (* Some sub *) - (* | _ -> None *) - - (* let alloc_ty = *) - (* TApp *) - (* { *) - (* ident = `Concrete (Concrete_ident.of_name Type Alloc__alloc__Global); *) - (* args = []; *) - (* } *) - - (* let make (t : ty) : ty = *) - (* let ident = `Concrete (Concrete_ident.of_name Type Alloc__boxed__Box) in *) - (* TApp { ident; args = [ GType t; GType alloc_ty ] } *) - (* end *) - - (* module Expr = struct *) - (* let destruct (e : expr) : expr option = *) - (* match e.e with *) - (* | App { f = { e = GlobalVar (`Primitive Box); _ }; args = [ arg ] } -> *) - (* Some arg *) - (* | _ -> None *) - - (* let make (e : expr) : expr = *) - (* let boxed_ty = Ty.make e.typ in *) - (* let f_ty = TArrow ([ e.typ ], boxed_ty) in *) - (* let f = { e with typ = f_ty; e = GlobalVar (`Primitive Box) } in *) - (* { e with typ = boxed_ty; e = App { f; args = [ e ] } } *) - (* end *) - (* end *) - - let rec collect_let_bindings' (e : expr) : (pat * expr * ty) list * expr = - match e.e with - | Let { monadic = _; lhs; rhs; body } -> - let bindings, body = collect_let_bindings' body in - ((lhs, rhs, e.typ) :: bindings, body) - | _ -> ([], e) - - let collect_let_bindings (e : expr) : (pat * expr) list * expr = - let bindings, body = collect_let_bindings' e in - let types = List.map ~f:thd3 bindings in - assert ( - match (List.drop_last types, types) with - | Some init, _ :: tl -> - List.zip_exn init tl |> List.for_all ~f:(uncurry [%eq: ty]) - | _ -> true); - (* TODO: injecting the type of the lets in the body is bad. - We should stay closer to Rust's inference. - Here, we lose a bit of information. - *) - let body = - { body with typ = List.hd types |> Option.value ~default:body.typ } - in - (List.map ~f:(fun (p, e, _) -> (p, e)) bindings, body) - - let rec map_body_of_nested_lets (f : expr -> expr) (e : expr) : expr = - match e.e with - | Let { monadic; lhs; rhs; body } -> - { - e with - e = Let { monadic; lhs; rhs; body = map_body_of_nested_lets f body }; - } - | _ -> f e - - let tuple_projector span (tuple_typ : ty) (len : int) (nth : int) - (type_at_nth : ty) : expr = - { - span; - (* TODO: require a span here *) - typ = TArrow ([ tuple_typ ], type_at_nth); - e = GlobalVar (`Projector (`TupleField (nth, len))); - } - - let project_tuple (tuple : expr) (len : int) (nth : int) (type_at_nth : ty) : - expr = - { - span = tuple.span; - typ = type_at_nth; - e = - App - { - f = tuple_projector tuple.span tuple.typ len nth type_at_nth; - args = [ tuple ]; - generic_args = [] (* TODO: see issue #328 *); - impl = None (* TODO: see issue #328 *); - }; - } - - module Place = struct - type t = { place : place'; span : span; typ : ty } - - and place' = - | LocalVar of Local_ident.t - | Deref of expr - | IndexProjection of { place : t; index : expr } - | FieldProjection of { place : t; projector : global_ident } - [@@deriving show] - - let deref_mut_allowed (t : ty) : bool = - match t with - | TApp { ident; _ } -> Global_ident.eq_name Alloc__vec__Vec ident - | _ -> false - - let rec of_expr (e : expr) : t option = - let wrap place = Some { place; span = e.span; typ = e.typ } in - match e.e with - | App { f = { e = GlobalVar (`Primitive Deref); _ }; args = [ e ]; _ } - -> ( - match of_expr e with - | Some { place = IndexProjection _; _ } as value -> value - | _ -> wrap @@ Deref e) - | LocalVar i -> wrap @@ LocalVar i - | App - { - f = { e = GlobalVar (`Projector _ as projector); _ }; - args = [ place ]; - generic_args = _; - impl = _; - (* TODO: see issue #328 *) - } -> - let* place = of_expr place in - wrap @@ FieldProjection { place; projector } - | App - { - f = { e = GlobalVar f; _ }; - args = [ place; index ]; - generic_args = _; - impl = _; - (* TODO: see issue #328 *) - } - when Global_ident.eq_name Core__ops__index__Index__index f -> - let* place = of_expr place in - let place = IndexProjection { place; index } in - Some { place; span = e.span; typ = e.typ } - | App - { - f = { e = GlobalVar f; _ }; - args = [ place; index ]; - generic_args = _; - impl = _; - (* TODO: see issue #328 *) - } - when Global_ident.eq_name Core__ops__index__IndexMut__index_mut f -> - (* Note that here, we allow any type to be `index_mut`ed: - Hax translates that to `Rust_primitives.Hax.update_at`. - This will typecheck IFF there is an implementation. - *) - let* typ = Expect.mut_ref e.typ in - let* place = Expect.mut_borrow place in - let* place = of_expr place in - let place = IndexProjection { place; index } in - Some { place; span = e.span; typ } - | _ -> None - - let rec to_expr (p : t) : expr = - match p.place with - | LocalVar v -> - let e : expr' = LocalVar v in - { e; typ = p.typ; span = p.span } - | Deref e -> call' (`Primitive Deref) [ e ] p.span p.typ - | FieldProjection { place; projector } -> - let e = to_expr place in - call' projector [ e ] p.span p.typ - | IndexProjection { place; index } -> - let e = to_expr place in - call Core__ops__index__Index__index [ e; index ] p.span p.typ - - let expect_deref_mut (p : t) : t option = - match p.place with - | Deref e -> - let* e = Expect.deref_mut_app e in - let* e = Expect.mut_borrow e in - of_expr e - | _ -> None - - let expect_allowed_deref_mut (p : t) : t option = - let* p = expect_deref_mut p in - if deref_mut_allowed p.typ then Some p else None - - let skip_allowed_deref_mut (p : t) : t = - Option.value ~default:p (expect_deref_mut p) - end - - module StringList = struct - module U = struct - module T = struct - type t = string * string list - [@@deriving show, yojson, compare, sexp, eq, hash] - end - - include T - module C = Base.Comparator.Make (T) - include C - end - - include U - module Map = Map.M (U) - end -end - -module MakeWithNamePolicy (F : Features.T) (NP : Concrete_ident.NAME_POLICY) = -struct - include Make (F) - open AST - module Concrete_ident_view = Concrete_ident.MakeViewAPI (NP) - - let group_items_by_namespace (items : item list) : item list StringList.Map.t - = - let h = Hashtbl.create (module StringList) in - List.iter items ~f:(fun item -> - let ns = Concrete_ident_view.to_namespace item.ident in - let items = Hashtbl.find_or_add h ns ~default:(fun _ -> ref []) in - items := !items @ [ item ]); - Map.of_iteri_exn - (module StringList) - ~iteri:(Hashtbl.map h ~f:( ! ) |> Hashtbl.iteri) -end diff --git a/engine/lib/ast_utils/ast_utils.ml b/engine/lib/ast_utils/ast_utils.ml new file mode 100644 index 000000000..35611901f --- /dev/null +++ b/engine/lib/ast_utils/ast_utils.ml @@ -0,0 +1,229 @@ +open! Prelude +open Ast + +(* module TypedLocalIdent = Ast_utils_sets.TypedLocalIdent *) + +module Make (F : Features.T) = struct + module AST = Ast.Make (F) + open AST + module TypedLocalIdent = Typed_local_ident.Make (F) + module Reducers = Ast_utils_browse.Reducers (F) + module Mappers = Ast_utils_browse.Mappers (F) + module Construct = Ast_utils_syntax.Construct (F) + module Destruct = Ast_utils_syntax.Destruct (F) + module Place = Place.Make(F) + + module Sets = struct + include Ast_utils_sets + module TypedLocalIdent = M (TypedLocalIdent) + end + + (** Produces a local identifier which is locally fresh **with respect + to expressions {exprs}**. *) + let fresh_local_ident_in_expr (exprs : expr list) (prefix : string) : + Local_ident.t = + let free_suffix = + List.map ~f:(Reducers.collect_local_idents#visit_expr ()) exprs + |> Set.union_list (module Local_ident) + |> Set.to_list + |> List.filter_map ~f:(fun ({ name; _ } : local_ident) -> + String.chop_prefix ~prefix name) + |> List.map ~f:(function "" -> "0" | s -> s) + |> List.filter_map ~f:Stdlib.int_of_string_opt + |> List.fold ~init:(-1) ~f:Int.max + |> ( + ) 1 + |> function + | 0 -> "" + | n -> Int.to_string n + in + { + name = prefix ^ free_suffix; + id = + (* TODO: freshness is local and name-only here... *) + Local_ident.mk_id Expr (-1); + } + + (* TODO: Those tuple1 things are wrong! Tuples of size one exists in Rust! e.g. `(123,)` *) + let rec remove_tuple1_pat (p : pat) : pat = + match p.p with + | PConstruct { name = `TupleType 1; args = [ { pat; _ } ]; _ } -> + remove_tuple1_pat pat + | _ -> p + + let rec remove_tuple1 (t : ty) : ty = + match t with + | TApp { ident = `TupleType 1; args = [ GType t ] } -> remove_tuple1 t + | _ -> t + + let remove_unsize (e : expr) : expr = + match e.e with + | App { f = { e = GlobalVar f; _ }; args = [ e ]; _ } + when Global_ident.eq_name Rust_primitives__unsize f -> + e + | _ -> e + + let rec pat_is_expr (p : pat) (e : expr) = + match (p.p, e.e) with + | _, Construct { constructor = `TupleCons 1; fields = [ (_, e) ]; _ } -> + pat_is_expr p e + | PBinding { subpat = None; var = pv; _ }, LocalVar ev -> + [%eq: local_ident] pv ev + | ( PConstruct { name = pn; args = pargs; _ }, + Construct { constructor = en; fields = eargs; base = None; _ } ) + when [%eq: global_ident] pn en -> ( + match List.zip pargs eargs with + | Ok zip -> + List.for_all + ~f:(fun (x, y) -> + [%eq: global_ident] x.field (fst y) && pat_is_expr x.pat (snd y)) + zip + | Unequal_lengths -> false) + | _ -> false + + let ty_equality (a : ty) (b : ty) : bool = + let replace_spans = + object + inherit [_] item_map + method visit_t () x = x + method visit_mutability _ () m = m + method! visit_span _ = function _ -> Span.default + end + in + let a = replace_spans#visit_ty () a in + let b = replace_spans#visit_ty () b in + [%eq: ty] a b + + (* maybe we should just drop Construct in favor of a + [Record] thing, and put everything which is not a Record + into an App. This would simplify stuff quite much. Maybe not + for LHS things. *) + let call_Constructor' (constructor : global_ident) is_struct + (args : expr list) span ret_typ = + let mk_field = + let len = List.length args in + fun n -> `TupleField (len, n) + in + let fields = List.mapi ~f:(fun i arg -> (mk_field i, arg)) args in + { + e = + Construct + { constructor; is_record = false; is_struct; fields; base = None }; + typ = ret_typ; + span; + } + + let call_Constructor (constructor_name : Concrete_ident.name) + (is_struct : bool) (args : expr list) span ret_typ = + call_Constructor' + (`Concrete + (Concrete_ident.of_name (Constructor { is_struct }) constructor_name)) + is_struct args span ret_typ + + module LiftToFullAst = struct + let expr : AST.expr -> Ast.Full.expr = Stdlib.Obj.magic + let item : AST.item -> Ast.Full.item = Stdlib.Obj.magic + end + + let unbox_expr' (next : expr -> expr) (e : expr) : expr = + match e.e with + | App { f = { e = GlobalVar f; _ }; args = [ e ]; _ } + when Global_ident.eq_name Alloc__boxed__Impl__new f -> + next e + | _ -> e + + let underef_expr' (next : expr -> expr) (e : expr) : expr = + match e.e with + | App + { + f = { e = GlobalVar (`Primitive Ast.Deref); _ }; + args = [ e ]; + generic_args = _; + impl = _; + } -> + next e + | _ -> e + + let rec unbox_expr e = unbox_expr' unbox_expr e + let underef_expr e = underef_expr' unbox_expr e + + let rec unbox_underef_expr e = + (unbox_expr' unbox_underef_expr >> underef_expr' unbox_underef_expr) e + + (* extracts a `param` out of a `generic_param` if it's a const + generic, otherwise returns `None`` *) + let param_of_generic_const_param (g : generic_param) : param option = + let* typ = match g.kind with GPConst { typ } -> Some typ | _ -> None in + let ({ span; ident = var; _ } : generic_param) = g in + let pat = + let mode, mut, subpat = (ByValue, Immutable, None) in + { p = PBinding { mut; mode; var; typ; subpat }; span; typ } + in + Some { pat; typ; typ_span = Some span; attrs = [] } + + let rec expr_of_lhs (span : span) (lhs : lhs) : expr = + match lhs with + | LhsLocalVar { var; typ } -> { e = LocalVar var; typ; span } + | LhsFieldAccessor { e; typ; field; _ } -> + let e = expr_of_lhs span e in + let f = { e = GlobalVar field; typ = TArrow ([ e.typ ], typ); span } in + { + e = + App + { + f; + args = [ e ]; + generic_args = []; + impl = None (* TODO: see issue #328 *); + }; + typ; + span; + } + | LhsArrayAccessor { e; typ; index; _ } -> + let args = [ expr_of_lhs span e; index ] in + Construct.Expr.app Core__ops__index__Index__index args span typ + | LhsArbitraryExpr { e; _ } -> e + + let rec map_body_of_nested_lets (f : expr -> expr) (e : expr) : expr = + match e.e with + | Let { monadic; lhs; rhs; body } -> + { + e with + e = Let { monadic; lhs; rhs; body = map_body_of_nested_lets f body }; + } + | _ -> f e + + + module StringList = struct + module U = struct + module T = struct + type t = string * string list + [@@deriving show, yojson, compare, sexp, eq, hash] + end + + include T + module C = Base.Comparator.Make (T) + include C + end + + include U + module Map = Map.M (U) + end +end + +module MakeWithNamePolicy (F : Features.T) (NP : Concrete_ident.NAME_POLICY) = +struct + include Make (F) + open AST + module Concrete_ident_view = Concrete_ident.MakeViewAPI (NP) + + let group_items_by_namespace (items : item list) : item list StringList.Map.t + = + let h = Hashtbl.create (module StringList) in + List.iter items ~f:(fun item -> + let ns = Concrete_ident_view.to_namespace item.ident in + let items = Hashtbl.find_or_add h ns ~default:(fun _ -> ref []) in + items := !items @ [ item ]); + Map.of_iteri_exn + (module StringList) + ~iteri:(Hashtbl.map h ~f:( ! ) |> Hashtbl.iteri) +end diff --git a/engine/lib/ast_utils/ast_utils_browse.ml b/engine/lib/ast_utils/ast_utils_browse.ml new file mode 100644 index 000000000..41308747c --- /dev/null +++ b/engine/lib/ast_utils/ast_utils_browse.ml @@ -0,0 +1,410 @@ +open! Prelude +open Ast + +type visit_level = ExprLevel | TypeLevel + +module Mappers (F : Features.T) = struct + module AST = Ast.Make (F) + open AST + + let regenerate_span_ids = + object + inherit [_] item_map + method visit_t () x = x + method visit_mutability _ () m = m + method visit_span = Fn.const Span.refresh_id + end + + let normalize_borrow_mut = + object + inherit [_] expr_map as super + method visit_t () x = x + method visit_mutability _ () m = m + + method! visit_expr s e = + let rec expr e = + match e.e with + | App + { + f = { e = GlobalVar (`Primitive Deref); _ }; + args = [ { e = Borrow { e = sub; _ }; _ } ]; + generic_args = _; + impl = _; + (* TODO: see issue #328 *) + } -> + expr sub + | _ -> super#visit_expr s e + in + expr e + end + + let rename_generic_constraints = + object + inherit [_] item_map as _super + method visit_t _ x = x + method visit_mutability _ _ m = m + + method! visit_GCType (s : (string, string) Hashtbl.t) bound id = + let data = "i" ^ Int.to_string (Hashtbl.length s) in + let _ = Hashtbl.add s ~key:id ~data in + GCType { bound; id = data } + + method! visit_LocalBound s id = + LocalBound { id = Hashtbl.find s id |> Option.value ~default:id } + end + + let rename_local_idents (f : local_ident -> local_ident) = + object + inherit [_] item_map as _super + method visit_t () x = x + method visit_mutability _ () m = m + method! visit_local_ident () ident = f ident + end + + let rename_global_idents (f : visit_level -> global_ident -> global_ident) = + object + inherit [_] item_map as super + method visit_t (_lvl : visit_level) x = x + method visit_mutability _ (_lvl : visit_level) m = m + method! visit_global_ident (lvl : visit_level) ident = f lvl ident + method! visit_ty _ t = super#visit_ty TypeLevel t + (* method visit_GlobalVar (lvl : level) i = GlobalVar (f lvl i) *) + end + + let rename_concrete_idents + (f : visit_level -> Concrete_ident.t -> Concrete_ident.t) = + object + inherit [_] item_map as super + method visit_t (_lvl : visit_level) x = x + method visit_mutability _ (_lvl : visit_level) m = m + method! visit_concrete_ident (lvl : visit_level) ident = f lvl ident + + method! visit_global_ident lvl (x : Global_ident.t) = + match x with + | `Concrete x -> `Concrete (f lvl x) + | _ -> super#visit_global_ident lvl x + + method! visit_ty _ t = super#visit_ty TypeLevel t + end + + let rename_global_idents_item + (f : visit_level -> global_ident -> global_ident) : item -> item = + (rename_global_idents f)#visit_item ExprLevel + + module Destruct = Ast_utils_syntax.Destruct (F) + + (** Add type ascription nodes in nested function calls. This helps + type inference in the presence of associated types in backends + that don't support them well (F* for instance). *) + let add_typ_ascription = + let is_app = Destruct.Expr.concrete_app' >> Option.is_some in + let o = + object + inherit [_] item_map as super + method visit_t (_ascribe_app : bool) x = x + method visit_mutability _ (_ascribe_app : bool) m = m + + method! visit_expr' (ascribe_app : bool) e = + (* Enable type ascription of underlying function + application. In the F* backend, we're annotating every + [Let] bindings, thus if we're facing a [Let], we turn + off application ascription. Similarly, if we're facing + an Ascription, we turn off application ascription. *) + let ascribe_app = + (ascribe_app || is_app e) + && not ([%matches? Let _ | Ascription _] e) + in + super#visit_expr' ascribe_app e + + method! visit_expr (ascribe_app : bool) e = + let e = super#visit_expr ascribe_app e in + let ascribe (e : expr) = + if [%matches? Ascription _] e.e then e + else { e with e = Ascription { e; typ = e.typ } } + in + match e.e with + | App + { + f = { e = GlobalVar (`Primitive Cast); _ } as f; + args = [ arg ]; + generic_args; + impl; + } -> + ascribe + { + e with + e = App { f; args = [ ascribe arg ]; generic_args; impl }; + } + | _ -> + (* Ascribe the return type of a function application & constructors *) + if (ascribe_app && is_app e.e) || [%matches? Construct _] e.e then + ascribe e + else e + end + in + o#visit_item false +end + +module Reducers (F : Features.T) = struct + module AST = Ast.Make (F) + open AST + module TypedLocalIdent = Typed_local_ident.Make (F) + + module Sets = struct + include Ast_utils_sets + module TypedLocalIdent = M (TypedLocalIdent) + end + + module Mappers = Mappers (F) + + let collect_local_idents = + object + inherit [_] item_reduce as _super + inherit [_] Sets.Local_ident.monoid as m + method visit_t _ _ = m#zero + method visit_mutability (_f : unit -> _ -> _) () _ = m#zero + method! visit_local_ident _ x = Set.singleton (module Local_ident) x + end + + include struct + open struct + type env = Local_ident.t list + + let id_shadows ~(env : env) (id : Local_ident.t) = + List.find env ~f:(fun x -> String.equal x.name id.name) + |> Option.value ~default:id + |> [%equal: Local_ident.t] id + |> not + + let ( ++ ) = Set.union + + let shadows' (type a) ~env vars (x : a) next = + (* account for shadowing within `vars` *) + List.filter ~f:(id_shadows ~env:vars) (List.rev vars) + |> Set.of_list (module Local_ident) + |> Set.union (next (vars @ env) x) + + let shadows (type a) ~(env : env) (pats : pat list) (x : a) + (next : env -> a -> Sets.Local_ident.t) = + let vars = + List.map pats ~f:(collect_local_idents#visit_pat ()) + |> Set.(union_list (module Local_ident) >> to_list) + in + shadows' ~env vars x next + end + + let collect_ambiguous_local_idents = + object (self) + inherit [_] item_reduce as super + inherit [_] Sets.Local_ident.monoid as m + method visit_t (_ : env) _ = m#zero + method visit_mutability (_f : env -> _ -> _) _ _ = m#zero + + method visit_arm' env { arm_pat; body } = + shadows ~env [ arm_pat ] body super#visit_expr + + method visit_expr' env e = + match e with + | Let { monadic = _; lhs; rhs; body } -> + super#visit_expr env rhs + ++ shadows ~env [ lhs ] body super#visit_expr + | Loop { kind; state; body; _ } -> + let empty = Set.empty (module Local_ident) |> Fn.(id &&& id) in + let ikind, ukind = + match kind with + | UnconditionalLoop -> empty + | ForLoop { pat; it; _ } -> + ( collect_local_idents#visit_pat () pat, + super#visit_expr env it ) + | ForIndexLoop { start; end_; var; _ } -> + ( Set.singleton (module Local_ident) var, + super#visit_expr (var :: env) start + ++ super#visit_expr (var :: env) end_ ) + in + let istate, ustate = + match state with + | Some { init; bpat; _ } -> + ( collect_local_idents#visit_pat () bpat, + super#visit_expr (Set.to_list ikind @ env) init ) + | _ -> empty + in + let intro = ikind ++ istate |> Set.to_list in + ukind ++ ustate ++ shadows' ~env intro body super#visit_expr + | Closure { params; body; _ } -> + shadows ~env params body super#visit_expr + | _ -> super#visit_expr' env e + + method visit_IIFn = self#visit_function_like + method visit_Fn env _ _ = self#visit_function_like env + + method visit_function_like env body params = + let f p = p.pat in + shadows ~env (List.map ~f params) body super#visit_expr + + method visit_local_ident env id = + Set.(if id_shadows ~env id then Fn.flip singleton id else empty) + (module Local_ident) + end + + let disambiguate_local_idents (item : item) = + let ambiguous = collect_ambiguous_local_idents#visit_item [] item in + let local_vars = collect_local_idents#visit_item () item |> ref in + let refresh env (id : Local_ident.t) : string = + let extract_suffix (id' : Local_ident.t) = + String.chop_prefix ~prefix:(id.name ^ "_") id'.name + |> Option.bind ~f:string_to_int + in + let suffix = + Set.filter_map (module Int) env ~f:extract_suffix + |> Set.max_elt |> Option.value ~default:0 |> ( + ) 1 + in + id.name ^ "_" ^ Int.to_string suffix + in + let new_names = + ambiguous |> Set.to_list + |> List.map ~f:(fun (var : Local_ident.t) -> + let var' = { var with name = refresh !local_vars var } in + local_vars := Set.add !local_vars var'; + (var, var')) + |> Map.of_alist_exn (module Local_ident) + in + let rename var = Map.find new_names var |> Option.value ~default:var in + (Mappers.rename_local_idents rename)#visit_item () item + end + + let collect_global_idents = + object + inherit ['self] item_reduce as _super + inherit [_] Sets.Global_ident.monoid as m + method visit_t _ _ = m#zero + method visit_mutability (_f : unit -> _ -> _) () _ = m#zero + + method! visit_global_ident (_env : unit) (x : Global_ident.t) = + Set.singleton (module Global_ident) x + end + + let collect_concrete_idents = + object + inherit ['self] item_reduce as super + inherit [_] Sets.Concrete_ident.monoid as m + method visit_t _ _ = m#zero + method visit_mutability (_f : unit -> _ -> _) () _ = m#zero + + method! visit_global_ident (_env : unit) (x : Global_ident.t) = + match x with + | `Concrete x -> Set.singleton (module Concrete_ident) x + | _ -> super#visit_global_ident () x + + method! visit_concrete_ident (_env : unit) (x : Concrete_ident.t) = + Set.singleton (module Concrete_ident) x + end + + let variables_of_pat (p : pat) : Sets.Local_ident.t = + (object + inherit [_] expr_reduce as super + inherit [_] Sets.Local_ident.monoid as m + method visit_t _ _ = m#zero + method visit_mutability (_f : unit -> _ -> _) () _ = m#zero + + method! visit_PBinding env _ _ var _ subpat = + m#plus + (Set.singleton (module Local_ident) var) + (Option.value_map subpat ~default:m#zero + ~f:(fst >> super#visit_pat env)) + end) + #visit_pat + () p + + let variables_of_param (p : param) : Local_ident.t list = + variables_of_pat p.pat |> Set.to_list + + let variables_of_pats : pat list -> Sets.Local_ident.t = + List.map ~f:variables_of_pat >> Set.union_list (module Local_ident) + + let without_vars (mut_vars : Sets.TypedLocalIdent.t) + (vars : Sets.Local_ident.t) = + Set.filter mut_vars ~f:(fst >> Set.mem vars >> not) + + let without_pats_vars (mut_vars : Sets.TypedLocalIdent.t) : + pat list -> Sets.TypedLocalIdent.t = + variables_of_pats >> without_vars mut_vars + + let without_pat_vars (mut_vars : Sets.TypedLocalIdent.t) (pat : pat) : + Sets.TypedLocalIdent.t = + without_pats_vars mut_vars [ pat ] + + let free_assigned_variables + (fv_of_arbitrary_lhs : F.arbitrary_lhs -> expr -> Sets.TypedLocalIdent.t) + = + object + inherit [_] expr_reduce as super + inherit [_] Sets.TypedLocalIdent.monoid as m + method visit_t _ _ = m#zero + method visit_mutability (_f : unit -> _ -> _) () _ = m#zero + + (* TODO: loop state *) + + method visit_Assign _env lhs e _wit = + let rec visit_lhs lhs = + match lhs with + | LhsLocalVar { var; _ } -> + Set.singleton (module TypedLocalIdent) (var, e.typ) + | LhsFieldAccessor { e; _ } -> visit_lhs e + | LhsArrayAccessor { e; index; _ } -> + Set.union (super#visit_expr () index) (visit_lhs e) + | LhsArbitraryExpr { witness; e } -> fv_of_arbitrary_lhs witness e + in + visit_lhs lhs + + method visit_Match env scrut arms = + List.fold_left ~init:(super#visit_expr env scrut) ~f:Set.union + @@ List.map ~f:(fun arm -> super#visit_arm env arm) arms + + method visit_Let env _monadic pat expr body = + Set.union (super#visit_expr env expr) + @@ without_pat_vars (super#visit_expr env body) pat + + method visit_Closure env params body _captures = + without_pats_vars (super#visit_expr env body) params + + method visit_Loop env body kind state _label _witness = + let vars = + (match kind with + | UnconditionalLoop -> [] + | ForLoop { pat = _not_mutable; _ } -> [] + | ForIndexLoop { var = _not_mutable; _ } -> []) + @ (state + |> Option.map ~f:(fun { bpat; _ } -> variables_of_pat bpat) + |> Option.to_list) + |> Set.union_list (module Local_ident) + in + m#plus + (super#visit_loop_kind env kind) + (m#plus + (Option.map ~f:(super#visit_loop_state env) state + |> Option.value ~default:m#zero) + (without_vars (super#visit_expr env body) vars)) + + method visit_arm' env { arm_pat; body } = + without_pat_vars (super#visit_expr env body) arm_pat + end + + class ['s] expr_list_monoid = + object + inherit ['s] VisitorsRuntime.monoid + method private zero = [] + method private plus = List.append + end + + let collect_break_payloads = + object + inherit [_] expr_reduce as super + inherit [_] expr_list_monoid as m + method visit_t _ _ = m#zero + method visit_mutability (_f : unit -> _ -> _) () _ = m#zero + method visit_Break _ e _ _ = m#plus (super#visit_expr () e) [ e ] + + method visit_Loop _ _ _ _ _ _ = (* Do *NOT* visit sub nodes *) + m#zero + end +end diff --git a/engine/lib/ast_utils/ast_utils_sets.ml b/engine/lib/ast_utils/ast_utils_sets.ml new file mode 100644 index 000000000..3ecc5bfd6 --- /dev/null +++ b/engine/lib/ast_utils/ast_utils_sets.ml @@ -0,0 +1,28 @@ +open! Prelude +open Ast + +module M (T : sig + type t [@@deriving show] + type comparator_witness + + val comparator : (t, comparator_witness) Base.Comparator.comparator +end) = +struct + include Set.M (T) + + let show (x : t) : string = [%show: T.t list] @@ Set.to_list x + + let pp (fmt : Stdlib.Format.formatter) (s : t) : unit = + Stdlib.Format.pp_print_string fmt @@ show s + + class ['s] monoid = + object + inherit ['s] VisitorsRuntime.monoid + method private zero = Set.empty (module T) + method private plus = Set.union + end +end + +module Global_ident = M (Global_ident) +module Concrete_ident = M (Concrete_ident) +module Local_ident = M (Local_ident) diff --git a/engine/lib/ast_utils/ast_utils_syntax.ml b/engine/lib/ast_utils/ast_utils_syntax.ml new file mode 100644 index 000000000..4bb141e24 --- /dev/null +++ b/engine/lib/ast_utils/ast_utils_syntax.ml @@ -0,0 +1,233 @@ +open! Prelude +open Ast + +module Misc (F : Features.T) = struct + module AST = Ast.Make (F) + open AST + + let rec pat_is_expr (p : pat) (e : expr) = + match (p.p, e.e) with + | _, Construct { constructor = `TupleCons 1; fields = [ (_, e) ]; _ } -> + pat_is_expr p e + | PBinding { subpat = None; var = pv; _ }, LocalVar ev -> + [%eq: local_ident] pv ev + | ( PConstruct { name = pn; args = pargs; _ }, + Construct { constructor = en; fields = eargs; base = None; _ } ) + when [%eq: global_ident] pn en -> ( + match List.zip pargs eargs with + | Ok zip -> + List.for_all + ~f:(fun (x, y) -> + [%eq: global_ident] x.field (fst y) && pat_is_expr x.pat (snd y)) + zip + | Unequal_lengths -> false) + | _ -> false +end + +module Construct (F : Features.T) = struct + module AST = Ast.Make (F) + open AST + open Misc (F) + + let tuple_field_pat (len : int) (nth : int) (pat : pat) : field_pat = + { field = `TupleField (nth, len); pat } + + module Ty = struct + let never : ty = + let ident = + `Concrete (Concrete_ident.of_name Type Rust_primitives__hax__Never) + in + TApp { ident; args = [] } + + let unit : ty = TApp { ident = `TupleType 0; args = [] } + + let tuple' (tuple : ty list) : ty = + let args = List.map ~f:(fun typ -> GType typ) tuple in + TApp { ident = `TupleType (List.length tuple); args } + + let tuple : ty list -> ty = function [ ty ] -> ty | l -> tuple' l + + let hax_failure : ty = + let ident = Concrete_ident.of_name Type Rust_primitives__hax__failure in + TApp { ident = `Concrete ident; args = [] } + end + + module Pat = struct + let var (var : local_ident) (typ : ty) (span : span) : pat = + let mut, mode = (Immutable, ByValue) in + { p = PBinding { mut; mode; var; typ; subpat = None }; span; typ } + + let wild (typ : ty) (span : span) : pat = { p = PWild; span; typ } + + let tuple' ?(drop_tuple_1=true) span : field_pat list -> pat = function + | [ { pat; _ } ] when drop_tuple_1 -> pat + | args -> + let is_record, is_struct = (false, true) in + let name = `TupleCons (List.length args) in + let p = PConstruct { name; args; is_record; is_struct } in + { p; typ = Ty.tuple @@ List.map ~f:(fun p -> p.pat.typ) args; span } + + let tuple ?(drop_tuple_1=true) ?span (pats : pat list) : pat = + let len = List.length pats in + let span = + let default () = Span.union_list @@ List.map ~f:(fun p -> p.span) pats in + Option.value_or_thunk span ~default + in + List.mapi ~f:(tuple_field_pat len) pats |> tuple' ~drop_tuple_1 span + end + + module Expr = struct + let unit span : expr = { typ = Ty.unit; span; e = GlobalVar (`TupleCons 0) } + let string_lit span s : expr = { span; typ = TStr; e = Literal (String s) } + + let let_ (lhs : pat) (rhs : expr) (body : expr) = + if pat_is_expr lhs body then rhs + else { body with e = Let { monadic = None; lhs; rhs; body } } + + let let_uncurried ((var, rhs) : local_ident * expr) (body : expr) : expr = + let_ (Pat.var var rhs.typ rhs.span) rhs body + + let multiple_lets (bindings : (local_ident * expr) list) (body : expr) : + expr = + List.fold_right ~init:body ~f:let_uncurried bindings + + let seq (e1 : expr) (e2 : expr) : expr = + let_ (Pat.wild e1.typ e1.span) e1 e2 + + let tuple' ~(span : span) (args : expr list) : expr = + let len = List.length args in + let is_record, is_struct = (false, true) in + let fields = List.mapi ~f:(fun i x -> (`TupleField (i, len), x)) args in + let constructor = `TupleCons len in + { + e = Construct { constructor; fields; is_record; is_struct; base = None }; + typ = List.map ~f:(fun { typ; _ } -> typ) args |> Ty.tuple; + span; + } + + let tuple ~(span : span) : expr list -> expr = function + | [ e ] -> e + | args -> tuple' ~span args + + let app' ?impl f (args : expr list) span ret_typ = + let typ = TArrow (List.map ~f:(fun arg -> arg.typ) args, ret_typ) in + let e = GlobalVar f in + let e = App { f = { e; typ; span }; args; generic_args = []; impl } in + { e; typ = ret_typ; span } + + let app ?impl ?(kind : Concrete_ident.Kind.t = Value) + (f_name : Concrete_ident.name) (args : expr list) span ret_typ = + let f = `Concrete (Concrete_ident.of_name kind f_name) in + app' ?impl f args span ret_typ + + let hax_failure' span (typ : ty) (context, kind) (ast : string) = + let error = Diagnostics.pretty_print_context_kind context kind in + let args = List.map ~f:(string_lit span) [ error; ast ] in + app Rust_primitives__hax__failure args span typ + + let hax_failure span (typ : ty) (context, kind) (expr0 : Ast.Full.expr) = + hax_failure' span typ (context, kind) (Print_rust.pexpr_str expr0) + + let tuple_projector span (tuple_typ : ty) (len : int) (nth : int) + (type_at_nth : ty) : expr = + let e = GlobalVar (`Projector (`TupleField (nth, len))) in + { span; typ = TArrow ([ tuple_typ ], type_at_nth); e } + end + + let unit_param (span : span) : param = + let typ = Ty.unit in + { pat = Pat.wild typ span; typ; typ_span = None; attrs = [] } +end + +module Destruct (F : Features.T) = struct + module AST = Ast.Make (F) + open AST + + module Item = struct + let functions (x : item) : (concrete_ident * expr) list = + match x.v with + | Fn { name; generics = _; body; params = _ } -> [ (name, body) ] + | Impl { items; _ } -> + List.filter_map + ~f:(fun w -> + match w.ii_v with + | IIFn { body; params = _ } -> Some (w.ii_ident, body) + | _ -> None) + items + | _ -> [] + end + + module Expr = struct + let mut_borrow (e : expr) : expr option = + match e.e with Borrow { kind = Mut _; e; _ } -> Some e | _ -> None + + let deref (e : expr) : expr option = + match e.e with + | App { f = { e = GlobalVar (`Primitive Deref); _ }; args = [ e ]; _ } -> + Some e + | _ -> None + + let concrete_app1 (f : Concrete_ident.name) (e : expr) : expr option = + match e.e with + | App + { + f = { e = GlobalVar (`Concrete f'); _ }; + args = [ e ]; + generic_args = _; + impl = _; + (* TODO: see issue #328 *) + } + when Concrete_ident.eq_name f f' -> + Some e + | _ -> None + + let concrete_app' : expr' -> concrete_ident option = function + | App { f = { e = GlobalVar (`Concrete c); _ }; _ } -> Some c + | _ -> None + + let deref_mut_app : expr -> expr option = + concrete_app1 Core__ops__deref__DerefMut__deref_mut + + let local_var (e : expr) : expr option = + match e.e with LocalVar _ -> Some e | _ -> None + + let rec let_bindings' (e : expr) : (pat * expr * ty) list * expr = + match e.e with + | Let { monadic = _; lhs; rhs; body } -> + let bindings, body = let_bindings' body in + ((lhs, rhs, e.typ) :: bindings, body) + | _ -> ([], e) + + let let_bindings (e : expr) : (pat * expr) list * expr = + let bindings, body = let_bindings' e in + let types = List.map ~f:thd3 bindings in + assert ( + match (List.drop_last types, types) with + | Some init, _ :: tl -> + List.zip_exn init tl |> List.for_all ~f:(uncurry [%eq: ty]) + | _ -> true); + (* TODO: injecting the type of the lets in the body is bad. + We should stay closer to Rust's inference. + Here, we lose a bit of information. + *) + let typ = List.hd types |> Option.value ~default:body.typ in + (List.map ~f:(fun (p, e, _) -> (p, e)) bindings, { body with typ }) + end + + module Ty = struct + let arrow (typ : ty) : (ty list * ty) option = + match typ with + | TArrow (inputs, output) -> Some (inputs, output) + | _ -> None + + let mut_ref (typ : ty) : ty option = + match typ with TRef { mut = Mutable _; typ; _ } -> Some typ | _ -> None + + let never : ty -> bool = function + | TApp { ident; _ } -> + Global_ident.eq_name Rust_primitives__hax__Never ident + | _ -> false + + let unit = [%matches? TApp { ident = `TupleType 0; _ }] + end +end diff --git a/engine/lib/ast_utils/ast_utils_syntax.mli b/engine/lib/ast_utils/ast_utils_syntax.mli new file mode 100644 index 000000000..7277afea1 --- /dev/null +++ b/engine/lib/ast_utils/ast_utils_syntax.mli @@ -0,0 +1,91 @@ +open! Prelude +open Ast + +module Misc (F : Features.T) : sig + module AST : module type of Ast.Make (F) + open AST + + val pat_is_expr : pat -> expr -> bool +end + +module Construct (F : Features.T) : sig + module AST : module type of Ast.Make (F) + open AST + + val tuple_field_pat : int -> int -> pat -> field_pat + + module Ty : sig + val never : ty + val unit : ty + val tuple' : ty list -> ty + val tuple : ty list -> ty + val hax_failure : ty + end + + module Pat : sig + val var : local_ident -> ty -> span -> pat + val wild : ty -> span -> pat + val tuple' : ?drop_tuple_1:bool -> span -> field_pat list -> pat + val tuple : ?drop_tuple_1:bool -> ?span:span -> pat list -> pat + end + + module Expr : sig + val unit : span -> expr + val string_lit : span -> string -> expr + val let_ : pat -> expr -> expr -> expr + val let_uncurried : local_ident * expr -> expr -> expr + val multiple_lets : (local_ident * expr) list -> expr -> expr + val seq : expr -> expr -> expr + val tuple' : span:span -> expr list -> expr + val tuple : span:span -> expr list -> expr + + val app' : + ?impl:impl_expr -> Global_ident.t -> expr list -> span -> ty -> expr + + val app : + ?impl:impl_expr -> + ?kind:Concrete_ident.Kind.t -> + Concrete_ident.name -> + expr list -> + span -> + ty -> + expr + + val hax_failure' : + span -> ty -> Diagnostics.Context.t * Types.kind -> string -> expr + + val hax_failure : + span -> ty -> Diagnostics.Context.t * Types.kind -> Ast.Full.expr -> expr + + val tuple_projector : span -> ty -> int -> int -> ty -> expr + end + + val unit_param : span -> param +end + +module Destruct (F : Features.T) : sig + module AST : module type of Ast.Make (F) + open AST + + module Item : sig + val functions : item -> (concrete_ident * expr) list + end + + module Expr : sig + val mut_borrow : expr -> expr option + val deref : expr -> expr option + val concrete_app1 : Concrete_ident.name -> expr -> expr option + val concrete_app' : expr' -> concrete_ident option + val deref_mut_app : expr -> expr option + val local_var : expr -> expr option + val let_bindings' : expr -> (pat * expr * ty) list * expr + val let_bindings : expr -> (pat * expr) list * expr + end + + module Ty : sig + val arrow : ty -> (ty list * ty) option + val mut_ref : ty -> ty option + val never : ty -> bool + val unit : ty -> bool + end +end diff --git a/engine/lib/ast_utils/place.ml b/engine/lib/ast_utils/place.ml new file mode 100644 index 000000000..bbd8aba0e --- /dev/null +++ b/engine/lib/ast_utils/place.ml @@ -0,0 +1,106 @@ +(** Quoting the {{: https://doc.rust-lang.org/reference/expressions.html#place-expressions-and-value-expressions }Rust Reference}, "a place expression is an expression that represents a memory location". + +This module represent places and provides helpers around them. *) + +open! Prelude +open Ast + +module Make (F : Features.T) = struct + module AST = Ast.Make (F) + open AST + module Destruct = Ast_utils_syntax.Destruct (F) + module Construct = Ast_utils_syntax.Construct (F) + + type t = { place : place; span : span; typ : ty } + + and place = + | LocalVar of Local_ident.t + | Deref of expr + | IndexProjection of { place : t; index : expr } + | FieldProjection of { place : t; projector : global_ident } + [@@deriving show] + + let deref_mut_allowed (t : ty) : bool = + match t with + | TApp { ident; _ } -> Global_ident.eq_name Alloc__vec__Vec ident + | _ -> false + + let rec of_expr (e : expr) : t option = + let wrap place = Some { place; span = e.span; typ = e.typ } in + match e.e with + | App { f = { e = GlobalVar (`Primitive Deref); _ }; args = [ e ]; _ } -> ( + match of_expr e with + | Some { place = IndexProjection _; _ } as value -> value + | _ -> wrap @@ Deref e) + | LocalVar i -> wrap @@ LocalVar i + | App + { + f = { e = GlobalVar (`Projector _ as projector); _ }; + args = [ place ]; + generic_args = _; + impl = _; + (* TODO: see issue #328 *) + } -> + let* place = of_expr place in + wrap @@ FieldProjection { place; projector } + | App + { + f = { e = GlobalVar f; _ }; + args = [ place; index ]; + generic_args = _; + impl = _; + (* TODO: see issue #328 *) + } + when Global_ident.eq_name Core__ops__index__Index__index f -> + let* place = of_expr place in + let place = IndexProjection { place; index } in + Some { place; span = e.span; typ = e.typ } + | App + { + f = { e = GlobalVar f; _ }; + args = [ place; index ]; + generic_args = _; + impl = _; + (* TODO: see issue #328 *) + } + when Global_ident.eq_name Core__ops__index__IndexMut__index_mut f -> + (* Note that here, we allow any type to be `index_mut`ed: + Hax translates that to `Rust_primitives.Hax.update_at`. + This will typecheck IFF there is an implementation. + *) + let* typ = Destruct.Ty.mut_ref e.typ in + let* place = Destruct.Expr.mut_borrow place in + let* place = of_expr place in + let place = IndexProjection { place; index } in + Some { place; span = e.span; typ } + | _ -> None + + let rec to_expr (p : t) : expr = + match p.place with + | LocalVar v -> + let e : expr' = LocalVar v in + { e; typ = p.typ; span = p.span } + | Deref e -> Construct.Expr.app' (`Primitive Deref) [ e ] p.span p.typ + | FieldProjection { place; projector } -> + let e = to_expr place in + Construct.Expr.app' projector [ e ] p.span p.typ + | IndexProjection { place; index } -> + let e = to_expr place in + Construct.Expr.app Core__ops__index__Index__index [ e; index ] p.span + p.typ + + let expect_deref_mut (p : t) : t option = + match p.place with + | Deref e -> + let* e = Destruct.Expr.deref_mut_app e in + let* e = Destruct.Expr.mut_borrow e in + of_expr e + | _ -> None + + let expect_allowed_deref_mut (p : t) : t option = + let* p = expect_deref_mut p in + if deref_mut_allowed p.typ then Some p else None + + let skip_allowed_deref_mut (p : t) : t = + Option.value ~default:p (expect_deref_mut p) +end diff --git a/engine/lib/ast_utils/typed_local_ident.ml b/engine/lib/ast_utils/typed_local_ident.ml new file mode 100644 index 000000000..596381dc4 --- /dev/null +++ b/engine/lib/ast_utils/typed_local_ident.ml @@ -0,0 +1,16 @@ +open! Prelude + +module Make (F : Features.T) = struct + module AST = Ast.Make (F) + + module T = struct + type t = Local_ident.t * AST.ty [@@deriving show, yojson] + + let sexp_of_t : t -> _ = fst >> Local_ident.sexp_of_t + let compare (a : t) (b : t) = [%compare: Local_ident.t] (fst a) (fst b) + let equal (a : t) (b : t) = [%eq: Local_ident.t] (fst a) (fst b) + end + + include Base.Comparator.Make (T) + include T +end diff --git a/engine/lib/backend.ml b/engine/lib/backend.ml index 83007df16..543eb483a 100644 --- a/engine/lib/backend.ml +++ b/engine/lib/backend.ml @@ -16,7 +16,7 @@ module type T = sig module U : sig module Mappers : sig val rename_global_idents_item : - (Ast_utils.visit_level -> global_ident -> global_ident) -> + (Ast_utils_browse.visit_level -> global_ident -> global_ident) -> AST.item -> AST.item end diff --git a/engine/lib/generic_printer/generic_printer_base.ml b/engine/lib/generic_printer/generic_printer_base.ml index e9d6d8ad1..9390248cb 100644 --- a/engine/lib/generic_printer/generic_printer_base.ml +++ b/engine/lib/generic_printer/generic_printer_base.ml @@ -234,7 +234,7 @@ module Make (F : Features.T) = struct print#with_span ~span (fun _ -> try print#expr_unwrapped ctx e with Diagnostics.SpanFreeError.Exn (Data (context, kind)) -> - U.hax_failure_expr span e.typ (context, kind) + U.Construct.Expr.hax_failure span e.typ (context, kind) (U.LiftToFullAst.expr e) (* TODO: if the printer is extremely broken, this results in a stack overflow *) |> print#expr ctx) diff --git a/engine/lib/import_thir.ml b/engine/lib/import_thir.ml index 1db362c78..1a94b0021 100644 --- a/engine/lib/import_thir.ml +++ b/engine/lib/import_thir.ml @@ -87,11 +87,6 @@ let c_binding_mode span : Thir.binding_mode -> binding_mode = function | ByValue -> ByValue | ByRef k -> ByRef (c_borrow_kind span k, W.reference) -let unit_typ : ty = TApp { ident = `TupleType 0; args = [] } - -let unit_expr span : expr = - { typ = unit_typ; span; e = Ast.GlobalVar (`TupleCons 0) } - let wild_pat span : ty -> pat = fun typ -> { typ; span; p = PWild } let c_logical_op : Thir.logical_op -> logical_op = function @@ -307,17 +302,17 @@ end) : EXPR = struct ^ [%show: ty] lhs.typ) else Concrete_ident.of_name Value @@ overloaded_names_of_binop op in - U.call' (`Concrete name) [ lhs; rhs ] span typ + U.Construct.Expr.app' (`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.Exn (Data (ctx, kind)) -> let typ : ty = try c_ty e.span e.ty - with Diagnostics.SpanFreeError.Exn _ -> U.hax_failure_typ + with Diagnostics.SpanFreeError.Exn _ -> U.Construct.Ty.hax_failure in let span = Span.of_thir e.span in - U.hax_failure_expr' span typ (ctx, kind) + U.Construct.Expr.hax_failure' span typ (ctx, kind) ([%show: Thir.decorated_for__expr_kind] e) and c_expr_unwrapped (e : Thir.decorated_for__expr_kind) : expr = @@ -349,7 +344,7 @@ end) : EXPR = struct let arm_pat = c_pat pat in let then_ = c_expr then' in let else_ = - Option.value ~default:(U.unit_expr span) + Option.value ~default:(U.Construct.Expr.unit span) @@ Option.map ~f:c_expr else_opt in let arm_then = @@ -386,7 +381,7 @@ end) : EXPR = struct { f with e = GlobalVar (def_id (AssociatedItem Value) id) } | _ -> f in - let args = if List.is_empty args then [ unit_expr span ] else args in + let args = if List.is_empty args then [ U.Construct.Expr.unit span ] else args in App { f; @@ -395,7 +390,7 @@ end) : EXPR = struct impl = Option.map ~f:(c_impl_expr e.span) impl; } | Box { value } -> - (U.call Rust_primitives__hax__box_new [ c_expr value ] span typ).e + (U.Construct.Expr.app Rust_primitives__hax__box_new [ c_expr value ] span typ).e | Deref { arg } -> let inner_typ = c_ty arg.span arg.ty in call (mk_global ([ inner_typ ] ->. typ) @@ `Primitive Deref) [ arg ] @@ -409,7 +404,7 @@ end) : EXPR = struct @@ `Primitive (LogicalOp (c_logical_op op))) [ lhs; rhs ] | Unary { arg; op } -> - (U.call + (U.Construct.Expr.app (match op with | Not -> Core__ops__bit__Not__not | Neg -> Core__ops__arith__Neg__neg) @@ -423,7 +418,7 @@ end) : EXPR = struct [ source ] | Use { source } -> (c_expr source).e | NeverToAny { source } -> - (U.call Rust_primitives__hax__never_to_any [ c_expr source ] span typ) + (U.Construct.Expr.app Rust_primitives__hax__never_to_any [ c_expr source ] span typ) .e (* TODO: this is incorrect (NeverToAny) *) | Pointer { cast; source } -> c_pointer e typ span cast source @@ -465,7 +460,7 @@ end) : EXPR = struct let e = c_expr e in { e with e = Block (e, W.block) }) o_expr - |> Option.value ~default:(unit_expr span) + |> Option.value ~default:(U.Construct.Expr.unit span) in let { e; _ } = List.fold_right o_stmts ~init ~f:(fun { kind; _ } body -> @@ -555,13 +550,13 @@ end) : EXPR = struct | Break { value; _ } -> (* TODO: labels! *) let e = Option.map ~f:c_expr value in - let e = Option.value ~default:(unit_expr span) e in + let e = Option.value ~default:(U.Construct.Expr.unit span) e in Break { e; label = None; witness = (W.break, 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 + let e = Option.value ~default:(U.Construct.Expr.unit span) e in Return { e; witness = W.early_exit } | ConstBlock _ -> unimplemented [ e.span ] "ConstBlock" | ConstParam { param = id; _ } (* TODO: shadowing? *) | ConstRef { id } -> @@ -574,11 +569,11 @@ end) : EXPR = struct let value = c_expr value in let count = c_constant_expr count in let inner = - U.call Rust_primitives__hax__repeat [ value; count ] span typ + U.Construct.Expr.app Rust_primitives__hax__repeat [ value; count ] span typ in - (U.call Alloc__boxed__Impl__new [ inner ] span typ).e + (U.Construct.Expr.app Alloc__boxed__Impl__new [ inner ] span typ).e | Tuple { fields } -> - (U.make_tuple_expr' ~span @@ List.map ~f:c_expr fields).e + (U.Construct.Expr.tuple' ~span @@ List.map ~f:c_expr fields).e | Array { fields } -> Array (List.map ~f:c_expr fields) | Adt { info; base; fields; _ } -> let constructor = @@ -628,7 +623,7 @@ 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.Construct.Pat.wild U.Construct.Ty.unit span ] else params in let body = c_expr body in @@ -763,7 +758,7 @@ end) : EXPR = struct is_struct = info.typ_is_struct; } | Tuple { subpatterns } -> - (List.map ~f:c_pat subpatterns |> U.make_tuple_pat').p + (List.map ~f:c_pat subpatterns |> U.Construct.Pat.tuple ~drop_tuple_1:false ~span).p | Deref { subpattern } -> PDeref { subpat = c_pat subpattern; witness = W.reference } | Constant { value } -> @@ -824,7 +819,7 @@ end) : EXPR = struct (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 + (U.Construct.Expr.app 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 *) @@ -860,7 +855,7 @@ end) : EXPR = struct | Arrow value -> let ({ inputs; output; _ } : Thir.ty_fn_sig) = value.value in let inputs = - if List.is_empty inputs then [ U.unit_typ ] + if List.is_empty inputs then [ U.Construct.Ty.unit ] else List.map ~f:(c_ty span) inputs in TArrow (inputs, c_ty span output) @@ -880,7 +875,7 @@ end) : EXPR = struct 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 -> U.never_typ + | Never -> U.Construct.Ty.never | Tuple types -> let types = List.map ~f:(fun ty -> GType (c_ty span ty)) types in TApp { ident = `TupleType (List.length types); args = types } @@ -1040,11 +1035,11 @@ end) : EXPR = struct let (Thir.{ inputs; output; _ } : Thir.fn_decl) = sg.decl in let output = match output with - | DefaultReturn _span -> unit_typ + | DefaultReturn _span -> U.Construct.Ty.unit | Return ty -> c_ty span ty in let inputs = - if List.is_empty inputs then [ U.unit_typ ] + if List.is_empty inputs then [ U.Construct.Ty.unit ] else List.map ~f:(c_ty span) inputs in TIFn (TArrow (inputs, output)) @@ -1152,7 +1147,7 @@ and c_item_unwrapped ~ident (item : Thir.item) : item list = } | Fn (generics, { body; params; _ }) -> let params = - if List.is_empty params then [ U.make_unit_param span ] + if List.is_empty params then [ U.Construct.unit_param span ] else List.map ~f:(c_param item.span) params in mk @@ -1263,7 +1258,7 @@ and c_item_unwrapped ~ident (item : Thir.item) : item list = match (item.kind : Thir.impl_item_kind) with | Fn { body; params; _ } -> let params = - if List.is_empty params then [ U.make_unit_param span ] + if List.is_empty params then [ U.Construct.unit_param span ] else List.map ~f:(c_param item.span) params in Fn diff --git a/engine/lib/phases/phase_and_mut_defsite.ml b/engine/lib/phases/phase_and_mut_defsite.ml index 0437e3068..22cd9dd3b 100644 --- a/engine/lib/phases/phase_and_mut_defsite.ml +++ b/engine/lib/phases/phase_and_mut_defsite.ml @@ -47,7 +47,7 @@ struct let expect_mut_ref_param (param : param) : (local_ident * ty * span) option = - let* typ = Expect.mut_ref param.typ in + let* typ = Destruct.Ty.mut_ref param.typ in match param.pat.p with | PBinding { mut = Immutable; mode = ByValue; var; typ = _; subpat = None } -> @@ -78,9 +78,9 @@ struct in let output_components = List.map ~f:snd3 and_muts - @ if UB.is_unit_typ output then [] else [ output ] + @ if UB.Destruct.Ty.unit output then [] else [ output ] in - let output = UB.make_tuple_typ output_components in + let output = UB.Construct.Ty.tuple output_components in Some (params, output, and_muts) (* visit an expression and replace all `Return e` nodes by `Return (f e)` *) @@ -105,7 +105,7 @@ struct match e.e with | GlobalVar (`TupleCons 0) -> e | _ -> - let lhs = UB.make_var_pat var e.typ e.span in + let lhs = UB.Construct.Pat.var var e.typ e.span in let rhs = e in let body = { e with e = LocalVar var } in { body with e = Let { monadic = None; lhs; rhs; body } } @@ -124,10 +124,10 @@ struct let* var = expect_in_vars_local_var e in (* var is supposed to be typed `&mut _` *) let typ = - Expect.mut_ref e.typ + Destruct.Ty.mut_ref e.typ |> Option.value_or_thunk ~default:(fun () -> Error.assertion_failure e.span - @@ "Expect.mut_ref: got `None`") + @@ "Destruct.Ty.mut_ref: got `None`") in (* we reconstruct `e` to type it correctly *) Some { e = LocalVar var; typ; span = e.span } @@ -139,7 +139,7 @@ struct method visit_mutability _ () m = m method visit_expr () e = - (let* e = Expect.deref e in + (let* e = Destruct.Expr.deref e in retyped_local_var_in_vars e) <|?> (fun _ -> retyped_local_var_in_vars e) |> Option.value_or_thunk ~default:(fun _ -> super#visit_expr () e) @@ -180,7 +180,7 @@ struct method visit_expr () e = try super#visit_expr () e with Diagnostics.SpanFreeError.Exn (Data (context, kind)) -> - UB.hax_failure_expr e.span e.typ (context, kind) + UB.Construct.Expr.hax_failure e.span e.typ (context, kind) (UB.LiftToFullAst.expr e) method visit_Assign () lhs e witness = @@ -209,8 +209,8 @@ struct vars in let f (e : B.expr) : B.expr = - UB.make_tuple_expr ~span:e.span - (vars @ if UB.is_unit_typ e.typ then [] else [ e ]) + UB.Construct.Expr.tuple ~span:e.span + (vars @ if UB.Destruct.Ty.unit e.typ then [] else [ e ]) in let body = body |> mutref_to_mut_expr idents |> convert_lhs |> map_returns ~f @@ -250,7 +250,7 @@ struct let params = List.map ~f:(fun typ -> - let pat = UB.make_var_pat var typ span in + let pat = UB.Construct.Pat.var var typ span in (* let pat : B.pat = { typ; p; span } in *) B.{ pat; typ; typ_span = None; attrs = [] }) inputs @@ -261,7 +261,7 @@ struct e = (* this is wrongly typed, though it's fine, we throw this away before returning *) - (UB.unit_expr span).e; + (UB.Construct.Expr.unit span).e; typ = output; span; } diff --git a/engine/lib/phases/phase_cf_into_monads.ml b/engine/lib/phases/phase_cf_into_monads.ml index 6a194dab8..8d31732ec 100644 --- a/engine/lib/phases/phase_cf_into_monads.ml +++ b/engine/lib/phases/phase_cf_into_monads.ml @@ -184,7 +184,7 @@ struct arms in let typ = - match arms with [] -> UB.never_typ | hd :: _ -> hd.arm.body.typ + match arms with [] -> UB.Construct.Ty.never | hd :: _ -> hd.arm.body.typ in { e = Match { scrutinee = dexpr scrutinee; arms }; span; typ } | If { cond; then_; else_ } -> @@ -218,12 +218,12 @@ struct let converted_typ = dty span converted_typ in if [%equal: B.ty] converted_typ e.typ then e else - UB.call Core__ops__try_trait__FromResidual__from_residual [ e ] span + UB.Construct.Expr.app Core__ops__try_trait__FromResidual__from_residual [ e ] span converted_typ | Return { e; _ } -> let open KnownMonads in let e = dexpr e in - UB.call Core__ops__control_flow__ControlFlow__Break [ e ] span + UB.Construct.Expr.app Core__ops__control_flow__ControlFlow__Break [ e ] span (to_typ @@ { monad = Some (MException e.typ); typ }) | [%inline_arms "dexpr'.*" - Let - Match - If - Continue - Break - QuestionMark @@ -233,7 +233,7 @@ struct and lift_if_necessary (e : B.expr) (target_type : B.ty) = if B.equal_ty e.typ target_type then e else - UB.call Rust_primitives__hax__control_flow_monad__ControlFlowMonad__lift + UB.Construct.Expr.app Rust_primitives__hax__control_flow_monad__ControlFlowMonad__lift [ e ] e.span target_type [@@inline_ands bindings_of dexpr - dexpr'] @@ -243,7 +243,7 @@ struct let e' = dexpr e in match KnownMonads.from_typ dty e.typ e'.typ with | { monad = Some m; typ } -> - UB.call + UB.Construct.Expr.app (match m with | MException _ -> Rust_primitives__hax__control_flow_monad__mexception__run diff --git a/engine/lib/phases/phase_direct_and_mut.ml b/engine/lib/phases/phase_direct_and_mut.ml index e85745d02..fa3d8a1a6 100644 --- a/engine/lib/phases/phase_direct_and_mut.ml +++ b/engine/lib/phases/phase_direct_and_mut.ml @@ -46,7 +46,7 @@ struct (Place.t, A.expr) Either.t option = let e = UA.Mappers.normalize_borrow_mut#visit_expr () e in let e = UA.remove_unsize e in - let* e = UA.Expect.mut_borrow e in + let* e = UA.Destruct.Expr.mut_borrow e in Option.some @@ match @@ -103,7 +103,7 @@ struct type, but sometimes `_otype` is less precise (i.e. an associated type while a concrete type is available) *) let arg_types, _otype = - UA.Expect.arrow f.typ + UA.Destruct.Ty.arrow f.typ |> Option.value_or_thunk ~default:(fun _ -> Error.assertion_failure span "expected an arrow type here") in @@ -116,7 +116,7 @@ struct | Ok inputs -> inputs | _ -> Error.assertion_failure span "application: bad arity") |> List.map ~f:(fun (typ, (arg : A.expr)) -> - if UA.Expect.mut_ref typ |> Option.is_some then + if UA.Destruct.Ty.mut_ref typ |> Option.is_some then (* the argument of the function is mutable *) let v = expect_mut_borrow_of_place_or_pure_expr arg @@ -181,16 +181,16 @@ struct let otype = dty f.span otype in let pat = let out = - if UB.is_unit_typ otype then [] - else [ UB.make_var_pat out_var otype f.span ] + if UB.Destruct.Ty.unit otype then [] + else [ UB.Construct.Pat.var out_var otype f.span ] in List.map ~f:(function - | Some (var, _), (ty, span) -> UB.make_var_pat var ty span - | None, (ty, span) -> UB.make_wild_pat ty span) + | Some (var, _), (ty, span) -> UB.Construct.Pat.var var ty span + | None, (ty, span) -> UB.Construct.Pat.wild ty span) mutargs @ out - |> UB.make_tuple_pat + |> UB.Construct.Pat.tuple in let f_call = let f : B.expr = @@ -222,22 +222,22 @@ struct |> List.map ~f:(fun ((var, lhs), (typ, span)) -> let e = B.{ e = LocalVar var; span; typ } in let witness = Features.On.mutable_variable in - B.{ e = Assign { lhs; e; witness }; span; typ = UB.unit_typ }) + B.{ e = Assign { lhs; e; witness }; span; typ = UB.Construct.Ty.unit }) in (* TODO: this should be greatly simplified when `lhs` type will accept tuples (issue #222) *) match assigns with | [ { e = Assign { lhs; witness; _ }; span; typ } ] - when UB.is_unit_typ otype -> + when UB.Destruct.Ty.unit otype -> { e = Assign { lhs; e = f_call; witness }; span; typ } | _ -> let body = let init = - if UB.is_unit_typ otype then UB.unit_expr f.span + if UB.Destruct.Ty.unit otype then UB.Construct.Expr.unit f.span else B.{ typ = otype; span = f.span; e = LocalVar out_var } in - List.fold_right ~init ~f:UB.make_seq assigns + List.fold_right ~init ~f:UB.Construct.Expr.seq assigns in - UB.make_let pat f_call body) + UB.Construct.Expr.let_ pat f_call body) and dexpr' (span : span) (e : A.expr') : B.expr' = match e with diff --git a/engine/lib/phases/phase_drop_blocks.ml b/engine/lib/phases/phase_drop_blocks.ml index b9edf72dd..b74fe2824 100644 --- a/engine/lib/phases/phase_drop_blocks.ml +++ b/engine/lib/phases/phase_drop_blocks.ml @@ -27,7 +27,7 @@ module%inlined_contents Make (F : Features.T) = struct [%%inline_defs dmutability] let rec dexpr' (span : span) (e : A.expr') : B.expr' = - match (UA.unbox_underef_expr { e; span; typ = UA.never_typ }).e with + match (UA.unbox_underef_expr { e; span; typ = UA.Construct.Ty.never }).e with | [%inline_arms "dexpr'.*" - Block] -> auto | Block (inner, _) -> (dexpr inner).e [@@inline_ands bindings_of dexpr - dexpr'] diff --git a/engine/lib/phases/phase_drop_references.ml b/engine/lib/phases/phase_drop_references.ml index 48daa26b3..49d9493a5 100644 --- a/engine/lib/phases/phase_drop_references.ml +++ b/engine/lib/phases/phase_drop_references.ml @@ -68,7 +68,7 @@ struct | PDeref { subpat; _ } -> (dpat subpat).p and dexpr' (span : span) (e : A.expr') : B.expr' = - match (UA.unbox_underef_expr { e; span; typ = UA.never_typ }).e with + match (UA.unbox_underef_expr { e; span; typ = UA.Construct.Ty.never }).e with | [%inline_arms If + Literal + Array + Block] -> auto | Construct { constructor; is_record; is_struct; fields; base } -> Construct diff --git a/engine/lib/phases/phase_functionalize_loops.ml b/engine/lib/phases/phase_functionalize_loops.ml index f0d216441..9240d1d93 100644 --- a/engine/lib/phases/phase_functionalize_loops.ml +++ b/engine/lib/phases/phase_functionalize_loops.ml @@ -58,7 +58,7 @@ struct span = body.span; } in - UB.call ~kind:(AssociatedItem Value) + UB.Construct.Expr.app ~kind:(AssociatedItem Value) Core__iter__traits__iterator__Iterator__fold [ it; dexpr init; fn ] span (dty span expr.typ) diff --git a/engine/lib/phases/phase_local_mutation.ml b/engine/lib/phases/phase_local_mutation.ml index 06dc1ff9c..4ef7f205d 100644 --- a/engine/lib/phases/phase_local_mutation.ml +++ b/engine/lib/phases/phase_local_mutation.ml @@ -102,10 +102,10 @@ struct { monadic = None; lhs = - h UB.make_tuple_pat (dpat lhs) - (UB.make_var_pat var (dty span typ) span); + h UB.Construct.Pat.tuple (dpat lhs) + (UB.Construct.Pat.var var (dty span typ) span); rhs = - h (UB.make_tuple_expr ~span) (UB.unit_expr span) + h (UB.Construct.Expr.tuple ~span) (UB.Construct.Expr.unit span) (dexpr_s { s with expr_level = []; drop_expr = false } value); @@ -123,14 +123,14 @@ struct |> List.map ~f:(fun (i, t) -> (i, dty span t)) in let vars_pat = - List.map ~f:(fun (i, t) -> UB.make_var_pat i t span) rhs_vars - |> UB.make_tuple_pat + List.map ~f:(fun (i, t) -> UB.Construct.Pat.var i t span) rhs_vars + |> UB.Construct.Pat.tuple in let lhs = dpat lhs in let lhs' = if List.is_empty rhs_vars then lhs else if drop_expr then vars_pat - else UB.make_tuple_pat [ vars_pat; lhs ] + else UB.Construct.Pat.tuple [ vars_pat; lhs ] in let body = dexpr_same body in { @@ -155,10 +155,10 @@ struct s.expr_level in let vars = - match vars with [ v ] -> v | _ -> UB.make_tuple_expr ~span vars + match vars with [ v ] -> v | _ -> UB.Construct.Expr.tuple ~span vars in if s.drop_expr then vars - else UB.make_tuple_expr ~span [ vars; UB.unit_expr span ] + else UB.Construct.Expr.tuple ~span [ vars; UB.Construct.Expr.unit span ] | Assign _ -> . | Closure { params; body; captures } -> let observable_mutations = @@ -208,7 +208,7 @@ struct | If { cond; then_; else_ } -> let then_ = dexpr_same then_ in let else_ = - Option.value ~default:(UA.unit_expr expr.span) else_ + Option.value ~default:(UA.Construct.Expr.unit expr.span) else_ |> dexpr_same |> Option.some in let cond = @@ -223,7 +223,7 @@ struct List.map ~f:darm arms in let typ = - match arms with [] -> UB.never_typ | hd :: _ -> hd.arm.body.typ + match arms with [] -> UB.Construct.Ty.never | hd :: _ -> hd.arm.body.typ in let scrutinee = dexpr_s { s with expr_level = []; drop_expr = false } scrutinee @@ -265,15 +265,15 @@ struct Some (let bpat' = List.map - ~f:(fun (i, t) -> UB.make_var_pat i t span) + ~f:(fun (i, t) -> UB.Construct.Pat.var i t span) observable_mutations - |> UB.make_tuple_pat + |> UB.Construct.Pat.tuple in let init' = List.map ~f:(fun (i, typ) : B.expr -> { e = LocalVar i; typ; span }) observable_mutations - |> UB.make_tuple_expr ~span + |> UB.Construct.Expr.tuple ~span in let witness = Features.On.state_passing_loop in match state with @@ -281,9 +281,9 @@ struct | Some { init; bpat; _ } -> { init = - UB.make_tuple_expr ~span + UB.Construct.Expr.tuple ~span [ init'; dexpr_s empty_s init ]; - bpat = UB.make_tuple_pat [ bpat'; dpat bpat ]; + bpat = UB.Construct.Pat.tuple [ bpat'; dpat bpat ]; witness; }) in @@ -293,22 +293,22 @@ struct in let body = dexpr_s s body in (* we deal with a for loop: this is always a unit expression (i.e. no [break foo] with [foo] non-unit allowed) *) - let typ = List.map ~f:snd observable_mutations |> UB.make_tuple_typ in + let typ = List.map ~f:snd observable_mutations |> UB.Construct.Ty.tuple in let loop : B.expr = { e = Loop { body; kind; state; label; witness }; typ; span } in if adapt && not (List.is_empty variables_to_output) then (* here, we need to introduce the shadowings as bindings *) let out = - UB.make_tuple_expr ~span + UB.Construct.Expr.tuple ~span @@ List.map ~f:(fun (ident, typ) -> B.{ e = LocalVar ident; typ; span }) variables_to_output in let lhs = - UB.make_tuple_pat + UB.Construct.Pat.tuple @@ List.map - ~f:(fun (ident, typ) -> UB.make_var_pat ident typ span) + ~f:(fun (ident, typ) -> UB.Construct.Pat.var ident typ span) observable_mutations in B. @@ -333,7 +333,7 @@ struct ~f:(fun (i, typ) : B.expr -> { e = LocalVar i; typ; span }) s.expr_level - |> UB.make_tuple_expr ~span + |> UB.Construct.Expr.tuple ~span in if s.drop_expr then let effect_e' = @@ -347,12 +347,12 @@ struct Let { monadic = None; - lhs = UB.make_wild_pat e'.typ e'.span; + lhs = UB.Construct.Pat.wild e'.typ e'.span; rhs = e'; body = vars; }; } - else UB.make_tuple_expr ~span [ vars; e' ]) + else UB.Construct.Expr.tuple ~span [ vars; e' ]) and dexpr_unwrapped e = dexpr_s Instructions.zero e [@@inline_ands bindings_of dexpr - dexpr'] diff --git a/engine/lib/phases/phase_reconstruct_for_loops.ml b/engine/lib/phases/phase_reconstruct_for_loops.ml index 745246ca3..956f23127 100644 --- a/engine/lib/phases/phase_reconstruct_for_loops.ml +++ b/engine/lib/phases/phase_reconstruct_for_loops.ml @@ -224,7 +224,7 @@ struct rhs; body = { e = GlobalVar (`TupleCons 0) }; } - when UA.is_unit_typ rhs.typ -> + when UA.Destruct.Ty.unit rhs.typ -> rhs | _ -> body in @@ -257,7 +257,7 @@ struct witness = S.loop expr.span witness; }; span = expr.span; - typ = UB.unit_typ; + typ = UB.Construct.Ty.unit; } | None -> h expr [@@inline_ands bindings_of dexpr] diff --git a/engine/lib/phases/phase_trivialize_assign_lhs.ml b/engine/lib/phases/phase_trivialize_assign_lhs.ml index 079e83276..32841f23d 100644 --- a/engine/lib/phases/phase_trivialize_assign_lhs.ml +++ b/engine/lib/phases/phase_trivialize_assign_lhs.ml @@ -73,7 +73,7 @@ module%inlined_contents Make (F : Features.T) = struct Rust_primitives__hax__monomorphized_update_at__update_at_range_full | _ -> Rust_primitives__hax__update_at in - let rhs = UB.call update_at [ lhs; dexpr index; rhs ] span lhs.typ in + let rhs = UB.Construct.Expr.app update_at [ lhs; dexpr index; rhs ] span lhs.typ in updater_of_lhs e rhs span | LhsArbitraryExpr _ -> Error.raise { kind = ArbitraryLHS; span } @@ -86,7 +86,7 @@ module%inlined_contents Make (F : Features.T) = struct { e = Assign { lhs; e; witness }; span = expr.span; - typ = UB.unit_typ; + typ = UB.Construct.Ty.unit; } | [%inline_arms "dexpr'.*" - Assign] -> map (fun e -> B.{ e; typ = dty expr.span expr.typ; span = expr.span }) diff --git a/engine/lib/side_effect_utils.ml b/engine/lib/side_effect_utils.ml index 2690b09b8..5fe9d321f 100644 --- a/engine/lib/side_effect_utils.ml +++ b/engine/lib/side_effect_utils.ml @@ -180,12 +180,12 @@ struct let var = (* if the body is a local variable, use that, otherwise get a fresh one *) - match snd @@ U.collect_let_bindings expr with + match snd @@ U.Destruct.Expr.let_bindings expr with (* TODO: this optimization is disabled because it fails in cases like f(x, {x = 3; x}) *) | { e = LocalVar var; _ } when false -> var | _ -> fresh () in - ( lbs @ [ (U.make_var_pat var expr.typ expr.span, expr) ], + ( lbs @ [ (U.Construct.Pat.var var expr.typ expr.span, expr) ], { expr with e = LocalVar var } )) :: l )) in @@ -209,7 +209,7 @@ struct end let let_of_binding ((pat, rhs) : pat * expr) (body : expr) : expr = - U.make_let pat rhs body + U.Construct.Expr.let_ pat rhs body let lets_of_bindings (bindings : (pat * expr) list) (body : expr) : expr = List.fold_right ~init:body ~f:let_of_binding bindings diff --git a/engine/lib/subtype.ml b/engine/lib/subtype.ml index 2f7383d8e..b57505b4e 100644 --- a/engine/lib/subtype.ml +++ b/engine/lib/subtype.ml @@ -138,9 +138,9 @@ struct let typ : B.ty = try dty e.span e.typ with Diagnostics.SpanFreeError.Exn (Data (_context, _kind)) -> - UB.hax_failure_typ + UB.Construct.Ty.hax_failure in - UB.hax_failure_expr e.span typ (context, kind) (UA.LiftToFullAst.expr e) + UB.Construct.Expr.hax_failure e.span typ (context, kind) (UA.LiftToFullAst.expr e) and dexpr_unwrapped (e : A.expr) : B.expr = { e = dexpr' e.span e.e; span = e.span; typ = dty e.span e.typ }