diff --git a/engine/utils/ppx_functor_application/README.md b/engine/utils/ppx_functor_application/README.md index fb852d344..3a59a7558 100644 --- a/engine/utils/ppx_functor_application/README.md +++ b/engine/utils/ppx_functor_application/README.md @@ -1,65 +1,82 @@ -# `ppx_inline` +# `ppx_functor_application` -Inlines chunks of OCaml AST in place. +## Motivation +The engine consists of numerous phases, implemented as OCaml functors +parametrized over "AST features" (see the book). Two phases can be +binded (sequenced) via `Phase_utils.BindPhase` functor. -Rewrite `[%%inline_defs L]`, `[%%inline_arms L]`, `[%%inline_body PATH]` inside nodes `[%%inlined_contents NODE]`, where: - - `L` is a (`+`/`-`-separated) list of path specifying which chunk of AST we should inline; - - `PATH` is a `.`-separated list of strings, possibly containing the `*` glob. +Since OCaml define (or let users define) infix notations for functor +application, combining many phases (functors) results in the following +christmas tree looking kinds of code: -## Example: -File `some_module.ml`: ```ocaml -let f x = x + 1 -let g x = x + 2 -let f' x = x + 3 - -module M = struct - let w = 0 - let x = 1 - let y = 2 - let z = 3 +struct + module ARG0 = (Phases.Reject.RawOrMutPointer)(Features.Rust) + module ARG1 = (Phases.Transform_hax_lib_inline)(ARG0.FB) + module ARG2 = (Phases.Specialize)(ARG1.FB) + module ARG3 = (Phases.Drop_sized_trait)(ARG2.FB) + module ARG4 = (Phases.Simplify_question_marks)(ARG3.FB) + module ARG5 = (Phases.And_mut_defsite)(ARG4.FB) + module ARG6 = (Phases.Reconstruct_for_loops)(ARG5.FB) + module ARG7 = (Phases.Reconstruct_while_loops)(ARG6.FB) + module ARG8 = (Phases.Direct_and_mut)(ARG7.FB) + module ARG9 = (Phases.Reject.Arbitrary_lhs)(ARG8.FB) + module ARG10 = (Phases.Drop_blocks)(ARG9.FB) + module ARG11 = (Phases.Drop_references)(ARG10.FB) + module ARG12 = (Phases.Trivialize_assign_lhs)(ARG11.FB) + module ARG13 = (Side_effect_utils.Hoist)(ARG12.FB) + module ARG14 = (Phases.Simplify_match_return)(ARG13.FB) + module ARG15 = (Phases.Drop_needless_returns)(ARG14.FB) + module ARG16 = (Phases.Local_mutation)(ARG15.FB) + module ARG17 = (Phases.Reject.Continue)(ARG16.FB) + module ARG18 = (Phases.Cf_into_monads)(ARG17.FB) + module ARG19 = (Phases.Reject.EarlyExit)(ARG18.FB) + module ARG20 = (Phases.Functionalize_loops)(ARG19.FB) + module ARG21 = (Phases.Reject.As_pattern)(ARG20.FB) + module ARG22 = (Phases.Traits_specs)(ARG21.FB) + module ARG23 = (Phases.Simplify_hoisting)(ARG22.FB) + module ARG24 = (Phases.Newtype_as_refinement)(ARG23.FB) + module ARG25 = (SubtypeToInputLanguage)(ARG24.FB) + module ARG26 = (Identity)(ARG25.FB) + include + ((BindPhase)(((BindPhase)(((BindPhase)(((BindPhase)(((BindPhase)(((BindPhase)(((BindPhase)(((BindPhase)(((BindPhase)(((BindPhase)(((BindPhase)(((BindPhase)(((BindPhase)(((BindPhase)(((BindPhase)(((BindPhase)(((BindPhase)(((BindPhase)(((BindPhase)(((BindPhase)(((BindPhase)(((BindPhase)(((BindPhase)(((BindPhase)(((BindPhase)(((BindPhase)(ARG0))(ARG1)))(ARG2)))(ARG3)))(ARG4)))(ARG5)))(ARG6)))(ARG7)))(ARG8)))(ARG9)))(ARG10)))(ARG11)))(ARG12)))(ARG13)))(ARG14)))(ARG15)))(ARG16)))(ARG17)))(ARG18)))(ARG19)))(ARG20)))(ARG21)))(ARG22)))(ARG23)))(ARG24)))(ARG25)))(ARG26) end - -let h x = "" -type foo = | A | B -let i (x: foo) = - match x with - | A -> 0 - | B -> 1 ``` -The module: -```ocaml -module%inlined_contents [@@add "some_module.ml"] Test = struct - [%%inline_defs f + g + foo] - [%%inline_defs "M.*" - z - y] - - let h: int -> string = [%%inline_body h] - let i: foo -> int = - match i with - | [%%inline_arms "i.*" - B] -> dummy - | B -> 123 -end -``` +The system of phases is supposed to let backends opt-in or out easily +for phases. This syntactic limitation was a major issue for that. + +## Solution +This PPX defines a small DSL that embeds in the OCaml syntax of +expressions to provide a nice way of binding phases functors via a +`|>` infix operator. -Will be rewritten into: +Example: ```ocaml -module%inlined_contents [@@add "some_module.ml"] Test = struct - - (* [%%inline_defs f + g + foo] *) - let f x = x + 1 - let g x = x + 2 - type foo = | A | B - - (* [%%inline_defs "M.*" - z - y] *) - let w = 0 - let x = 1 - - let h: int -> string = (fun x -> "") - let i: foo -> int = - match i with - | A -> 0 - | B -> 123 -end +module TransformToInputLanguage = + [%functor_application + Phases.Reject.RawOrMutPointer(Features.Rust) + |> Phases.Transform_hax_lib_inline + |> Phases.Specialize + |> Phases.Drop_sized_trait + |> Phases.Simplify_question_marks + |> Phases.And_mut_defsite + |> Phases.Reconstruct_for_loops + |> Phases.Reconstruct_while_loops + |> SubtypeToInputLanguage + |> Identity + ] + [@ocamlformat "disable"] ``` +Note: the `[@ocamlformat "disable"]` annotation is important, +otherwise `ocamlformat` tries to format those PPX invokations with its +rules for expressions, yielding rather ugly looking code... + +### Syntax + - `Name`: a module `Name` + - `Name(X, Y, Z)`: the application of the functor `Name` with three arguments `X`, `Y` and `Z` + - `(module )`: the arbitary OCaml module expression `` + - ` `: the application of the module described by `` and the module described by `` + - `(fun X -> )`: a "functor" from `X` to `` + - ` |> `: `` binded with `` diff --git a/engine/utils/ppx_functor_application/ppx_functor_application.ml b/engine/utils/ppx_functor_application/ppx_functor_application.ml index c49ff7bd9..f53344de7 100644 --- a/engine/utils/ppx_functor_application/ppx_functor_application.ml +++ b/engine/utils/ppx_functor_application/ppx_functor_application.ml @@ -30,6 +30,7 @@ let show_module_expr = string_of_module_expr let pp_module_expr (fmt : Format.formatter) (s : module_expr) : unit = Format.pp_print_string fmt @@ string_of_module_expr s +(** Defines a DSL for functor application. *) type module_dsl = | Var of longident | App of module_dsl * module_dsl @@ -41,6 +42,7 @@ type module_dsl = let var_of_string s = Var (Longident.Lident s) +(** Elaborate a OCaml module expression from a `module_dsl` *) let rec elab ~loc (t : module_dsl) : module_expr = let (module E) = Ast_builder.make loc in let h = elab ~loc in @@ -92,6 +94,7 @@ let rec collect_pipes (t : module_dsl) : module_dsl list = | Meta (Pipe l, _) | Pipe l -> List.concat_map ~f:collect_pipes l | _ -> [ t ] +(** Get rid of extra `Pipe` nodes *) let rec normalize (t : module_dsl) : module_dsl = match t with | App (f, x) -> App (normalize f, normalize x) @@ -104,16 +107,28 @@ let rec normalize (t : module_dsl) : module_dsl = | [ t ] -> t | l -> Pipe l) +(** Recognize a small language embedded in OCaml syntax for applying +functors in chain. *) let rec parse expr = let r = match expr with - | { pexp_desc = Pexp_construct ({ txt; _ }, None); _ } -> Var txt + | { pexp_desc = Pexp_construct ({ txt; _ }, None); _ } -> + (* Parses variables (module names are uppercase, since we are looking at OCaml expressions, so we match on constructors) *) + Var txt | { pexp_desc = Pexp_construct ({ txt; _ }, Some arg); _ } -> + (* Parses module applcations (same as above: in expressions, module applications are parsed as constructor applications) *) App (Var txt, parse arg) - | [%expr [%e? m1] |> [%e? m2]] -> Pipe [ parse m1; parse m2 ] - | [%expr (module [%m? m])] -> ModExpr m - | [%expr [%e? f] [%e? x]] -> App (parse f, parse x) + | [%expr [%e? m1] |> [%e? m2]] -> + (* Parses `... |> ...` infix module application *) + Pipe [ parse m1; parse m2 ] + | [%expr (module [%m? m])] -> + (* Parses module expressions (in this case, that corresponds to OCaml module expression) *) + ModExpr m + | [%expr [%e? f] [%e? x]] -> + (* Parses module applications (e.g. `(fun x -> ...) (module YXZ)`) *) + App (parse f, parse x) | [%expr fun [%p? x] -> [%e? body]] -> ( + (* Parses module abstractions (e.g. `fun X -> Z(X)`) *) match x with | { ppat_desc = Ppat_construct ({ txt = Lident x; _ }, None); _ } -> Abs (x, parse body) diff --git a/frontend/exporter/src/types/copied.rs b/frontend/exporter/src/types/copied.rs index 527507362..8fd350c83 100644 --- a/frontend/exporter/src/types/copied.rs +++ b/frontend/exporter/src/types/copied.rs @@ -2412,66 +2412,50 @@ pub enum ExprKind { #[map({ let e = gstate.thir().exprs[*fun].unroll_scope(gstate); let (generic_args, r#trait, bounds_impls); - let fun = match &e.kind { - /* TODO: see whether [user_ty] below is relevant or not */ - rustc_middle::thir::ExprKind::ZstLiteral {user_ty: _ } => { - match ty.kind() { - rustc_middle::ty::TyKind::FnDef(def_id, generics) => { - let (hir_id, attributes) = e.hir_id_and_attributes(gstate); - let hir_id = hir_id.map(|hir_id| hir_id.index()); - let contents = Box::new(ExprKind::GlobalName { - id: def_id.sinto(gstate) - }); - let mut translated_generics = generics.sinto(gstate); - let tcx = gstate.base().tcx; - r#trait = (|| { - let assoc_item = tcx.opt_associated_item(*def_id)?; - let assoc_trait = tcx.trait_of_item(assoc_item.def_id)?; - let trait_ref = ty::TraitRef::new(tcx, assoc_trait, generics.iter()); - let impl_expr = { - // TODO: we should not wrap into a dummy binder - let poly_trait_ref = ty::Binder::dummy(trait_ref); - poly_trait_ref.impl_expr(gstate, gstate.param_env()) - }; - let assoc_generics = tcx.generics_of(assoc_item.def_id); - let assoc_generics = translated_generics.drain(0..assoc_generics.parent_count); - Some((impl_expr, assoc_generics.collect())) - })(); - generic_args = translated_generics; - bounds_impls = solve_item_traits(gstate, gstate.param_env(), *def_id, generics, None); - Expr { - contents, - span: e.span.sinto(gstate), - ty: e.ty.sinto(gstate), - hir_id, - attributes, - } - }, - ty_kind => supposely_unreachable_fatal!( - gstate[e.span], - "CallNotTyFnDef"; - {e, ty_kind} - ) + // A function is any expression whose type is something callable + let fun = match ty.kind() { + rustc_middle::ty::TyKind::FnDef(def_id, generics) => { + let (hir_id, attributes) = e.hir_id_and_attributes(gstate); + let hir_id = hir_id.map(|hir_id| hir_id.index()); + let contents = Box::new(ExprKind::GlobalName { + id: def_id.sinto(gstate) + }); + let mut translated_generics = generics.sinto(gstate); + let tcx = gstate.base().tcx; + r#trait = (|| { + let assoc_item = tcx.opt_associated_item(*def_id)?; + let assoc_trait = tcx.trait_of_item(assoc_item.def_id)?; + let trait_ref = ty::TraitRef::new(tcx, assoc_trait, generics.iter()); + let impl_expr = { + // TODO: we should not wrap into a dummy binder + let poly_trait_ref = ty::Binder::dummy(trait_ref); + poly_trait_ref.impl_expr(gstate, gstate.param_env()) + }; + let assoc_generics = tcx.generics_of(assoc_item.def_id); + let assoc_generics = translated_generics.drain(0..assoc_generics.parent_count); + Some((impl_expr, assoc_generics.collect())) + })(); + generic_args = translated_generics; + bounds_impls = solve_item_traits(gstate, gstate.param_env(), *def_id, generics, None); + Expr { + contents, + span: e.span.sinto(gstate), + ty: e.ty.sinto(gstate), + hir_id, + attributes, } }, - kind => { - match ty.kind() { - rustc_middle::ty::TyKind::FnPtr(..) => { - generic_args = vec![]; // A function pointer has no generics - bounds_impls = vec![]; // A function pointer has no bounds - r#trait = None; // A function pointer is not a method - e.sinto(gstate) - }, - ty_kind => { - supposely_unreachable!( - gstate[e.span], - "CallNotTyFnDef"; - {e, kind, ty_kind} - ); - fatal!(gstate, "RefCallNotTyFnPtr") - } - } - } + rustc_middle::ty::TyKind::FnPtr(..) => { + generic_args = vec![]; // A function pointer has no generics + bounds_impls = vec![]; // A function pointer has no bounds + r#trait = None; // A function pointer is not a method + e.sinto(gstate) + }, + ty_kind => supposely_unreachable_fatal!( + gstate[e.span], + "CallNotTyFnDef"; + {e, ty_kind} + ) }; TO_TYPE::Call { ty: ty.sinto(gstate), diff --git a/tests/Cargo.lock b/tests/Cargo.lock index 9d18936a6..fe5e3ca74 100644 --- a/tests/Cargo.lock +++ b/tests/Cargo.lock @@ -235,6 +235,13 @@ version = "0.0.1" name = "fn-to-letfun" version = "0.1.0" +[[package]] +name = "functions" +version = "0.1.0" +dependencies = [ + "hax-lib", +] + [[package]] name = "generics" version = "0.1.0" diff --git a/tests/Cargo.toml b/tests/Cargo.toml index 68ec5ef04..8142bf4a4 100644 --- a/tests/Cargo.toml +++ b/tests/Cargo.toml @@ -28,5 +28,6 @@ members = [ "cli/include-flag", "cli/interface-only", "recursion", + "functions", ] resolver = "2" diff --git a/tests/functions/Cargo.toml b/tests/functions/Cargo.toml new file mode 100644 index 000000000..215bd726c --- /dev/null +++ b/tests/functions/Cargo.toml @@ -0,0 +1,10 @@ +[package] +name = "functions" +version = "0.1.0" +edition = "2021" + +[dependencies] +hax-lib = { path = "../../hax-lib" } + +[package.metadata.hax-tests] +into."fstar+coq" = { snapshot = "stdout" } diff --git a/tests/functions/src/lib.rs b/tests/functions/src/lib.rs new file mode 100644 index 000000000..f3c4b4801 --- /dev/null +++ b/tests/functions/src/lib.rs @@ -0,0 +1,6 @@ +/// Issue #757 +fn calling_function_pointer() { + fn f() {} + let f_ptr = f::; + f_ptr(); +}