From 26b440d88a6ff9efb7bd0adee13738337a8b0e26 Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Mon, 26 Feb 2024 14:45:20 +0100 Subject: [PATCH] wip --- .envrc | 1 + cli/driver/src/exporter.rs | 20 +- cli/options/engine/src/lib.rs | 30 + engine/backends/coq/coq/coq_backend.ml | 1 + .../fstar/fstar-surface-ast/FStar_String.ml | 4 +- engine/backends/fstar/fstar_backend.ml | 18 +- engine/backends/proverif/proverif_backend.ml | 994 +++++++++--------- engine/default.nix | 2 + engine/lib/dune | 1 + engine/lib/generic_printer/generic_printer.ml | 436 -------- .../lib/generic_printer/generic_printer.mli | 6 - .../generic_printer/generic_printer_api.ml | 89 ++ .../generic_printer/generic_printer_base.ml | 460 +++----- .../generic_printer/generic_printer_base.mli | 23 + .../generic_printer_base_sig.ml | 348 ++++++ .../generic_printer_template.ml | 64 ++ engine/lib/generic_printer/rust_printer.ml | 170 +++ engine/lib/generic_printer/rust_printer.mli | 4 + engine/profile.dump | 0 flake.lock | 58 +- flake.nix | 30 +- tests/attributes/src/lib.rs | 43 +- 22 files changed, 1474 insertions(+), 1328 deletions(-) create mode 100644 .envrc delete mode 100644 engine/lib/generic_printer/generic_printer.ml delete mode 100644 engine/lib/generic_printer/generic_printer.mli create mode 100644 engine/lib/generic_printer/generic_printer_api.ml create mode 100644 engine/lib/generic_printer/generic_printer_base.mli create mode 100644 engine/lib/generic_printer/generic_printer_base_sig.ml create mode 100644 engine/lib/generic_printer/generic_printer_template.ml create mode 100644 engine/lib/generic_printer/rust_printer.ml create mode 100644 engine/lib/generic_printer/rust_printer.mli create mode 100644 engine/profile.dump diff --git a/.envrc b/.envrc new file mode 100644 index 000000000..3550a30f2 --- /dev/null +++ b/.envrc @@ -0,0 +1 @@ +use flake diff --git a/cli/driver/src/exporter.rs b/cli/driver/src/exporter.rs index 802363231..abccf53bf 100644 --- a/cli/driver/src/exporter.rs +++ b/cli/driver/src/exporter.rs @@ -47,9 +47,24 @@ fn write_files( std::fs::write(&path, file.contents).unwrap_or_else(|e| { session.fatal(format!( "Unable to write to file {:#?}. Error: {:#?}", - path, e + &path, e )) - }) + }); + if let Some(mut sourcemap) = file.sourcemap { + sourcemap.inline_sources_content(); + sourcemap.sourceRoot = manifest_dir.display().to_string(); + let sourcemap = serde_json::to_string_pretty(&sourcemap).unwrap(); + let path = path.with_extension(format!( + "{}.map", + path.extension().unwrap().to_str().unwrap() + )); + std::fs::write(&path, sourcemap).unwrap_or_else(|e| { + session.fatal(format!( + "Unable to write to file {:#?}. Error: {:#?}", + path, e + )) + }); + } } } @@ -403,6 +418,7 @@ impl Callbacks for ExtractionCallbacks { let engine_options = hax_cli_options_engine::EngineOptions { backend: backend.clone(), input: converted_items, + manifest_dir: std::env::var("CARGO_MANIFEST_DIR").unwrap().into(), impl_infos, }; let mut engine_subprocess = find_hax_engine() diff --git a/cli/options/engine/src/lib.rs b/cli/options/engine/src/lib.rs index d48cc1e8c..dd6590e9f 100644 --- a/cli/options/engine/src/lib.rs +++ b/cli/options/engine/src/lib.rs @@ -8,16 +8,46 @@ type ThirBody = hax_frontend_exporter::ThirBody; pub struct EngineOptions { pub backend: BackendOptions, pub input: Vec>, + pub manifest_dir: String, pub impl_infos: Vec<( hax_frontend_exporter::DefId, hax_frontend_exporter::ImplInfos, )>, } +#[allow(non_snake_case)] +#[derive(JsonSchema, Debug, Clone, Serialize, Deserialize)] +pub struct SourceMap { + pub mappings: String, + pub sourceRoot: String, + pub sources: Vec, + pub sourcesContent: Vec>, + pub names: Vec, + pub version: u8, + pub file: String, +} + +impl SourceMap { + pub fn inline_sources_content(&mut self) { + self.sourcesContent = vec![]; + for source in &self.sources { + let path = if self.sourceRoot.is_empty() { + source.clone() + } else { + format!("{}/{}", &self.sourceRoot, source) + }; + eprintln!("path={path}"); + let contents = Some(std::fs::read_to_string(path).unwrap()); + self.sourcesContent.push(contents); + } + } +} + #[derive(JsonSchema, Debug, Clone, Serialize, Deserialize)] pub struct File { pub path: String, pub contents: String, + pub sourcemap: Option, } #[derive(JsonSchema, Debug, Clone, Serialize, Deserialize)] diff --git a/engine/backends/coq/coq/coq_backend.ml b/engine/backends/coq/coq/coq_backend.ml index c90877015..5425e4599 100644 --- a/engine/backends/coq/coq/coq_backend.ml +++ b/engine/backends/coq/coq/coq_backend.ml @@ -690,6 +690,7 @@ let translate _ (_bo : BackendOptions.t) (items : AST.item list) : path = mod_name ^ ".v"; contents = hardcoded_coq_headers ^ "\n" ^ string_of_items items ^ "\n"; + sourcemap = None; }) open Phase_utils diff --git a/engine/backends/fstar/fstar-surface-ast/FStar_String.ml b/engine/backends/fstar/fstar-surface-ast/FStar_String.ml index 45c7ba415..4cbd870bd 100644 --- a/engine/backends/fstar/fstar-surface-ast/FStar_String.ml +++ b/engine/backends/fstar/fstar-surface-ast/FStar_String.ml @@ -29,8 +29,8 @@ let get s i = BatUChar.code (BatUTF8.get s (Z.to_int i)) let collect f s = let r = ref "" in BatUTF8.iter (fun c -> r := !r ^ f (BatUChar.code c)) s; !r -let lowercase = BatString.lowercase -let uppercase = BatString.uppercase +let lowercase = String.lowercase_ascii +let uppercase = String.uppercase_ascii let escaped = BatString.escaped let index = get exception Found of int diff --git a/engine/backends/fstar/fstar_backend.ml b/engine/backends/fstar/fstar_backend.ml index 7cdb90db4..65e3a7d8d 100644 --- a/engine/backends/fstar/fstar_backend.ml +++ b/engine/backends/fstar/fstar_backend.ml @@ -1213,6 +1213,8 @@ let fstar_headers (bo : BackendOptions.t) = in [ opts; "open Core"; "open FStar.Mul" ] |> String.concat ~sep:"\n" +module GG = Rust_printer.Make (InputLanguage) + let translate m (bo : BackendOptions.t) (items : AST.item list) : Types.file list = let show_view Concrete_ident.{ crate; path; definition } = @@ -1227,17 +1229,25 @@ let translate m (bo : BackendOptions.t) (items : AST.item list) : ~f:(map_first_letter String.uppercase) (fst ns :: snd ns)) in + let string_of_items _ _ items = + let r = GG.items () items in + let str = Generic_printer_api.AnnotatedString.to_string r in + let sm = Generic_printer_api.AnnotatedString.to_sourcemap r in + let r = (str, sm) in + (r, r) + in let impl, intf = string_of_items bo m items in - let make ~ext body = + let make ~ext (body, sourcemap) = if String.is_empty body then None else Some Types. { path = mod_name ^ "." ^ ext; - contents = - "module " ^ mod_name ^ "\n" ^ fstar_headers bo ^ "\n\n" - ^ body ^ "\n"; + contents = body; + (* "module " ^ mod_name ^ "\n" ^ fstar_headers bo ^ "\n\n" *) + (* ^ body ^ "\n"; *) + sourcemap = Some sourcemap; } in List.filter_map ~f:Fn.id diff --git a/engine/backends/proverif/proverif_backend.ml b/engine/backends/proverif/proverif_backend.ml index 1397f18d5..3818e5a2f 100644 --- a/engine/backends/proverif/proverif_backend.ml +++ b/engine/backends/proverif/proverif_backend.ml @@ -103,478 +103,478 @@ end module U = Ast_utils.MakeWithNamePolicy (InputLanguage) (ProVerifNamePolicy) open AST -module Print = struct - module GenericPrint = - Generic_printer.Make (InputLanguage) (U.Concrete_ident_view) - - open Generic_printer_base.Make (InputLanguage) - open PPrint - - let iblock f = group >> jump 2 0 >> terminate (break 0) >> f >> group - - (* TODO: Give definitions for core / known library functions, cf issues #447, #448 *) - let library_functions : - (Concrete_ident_generated.name * (AST.expr list -> document)) list = - [ (* (\* Core dependencies *\) *) - (* (Alloc__vec__from_elem, fun args -> string "PLACEHOLDER_library_function"); *) - (* ( Alloc__slice__Impl__to_vec, *) - (* fun args -> string "PLACEHOLDER_library_function" ); *) - (* (Core__slice__Impl__len, fun args -> string "PLACEHOLDER_library_function"); *) - (* ( Core__ops__deref__Deref__deref, *) - (* fun args -> string "PLACEHOLDER_library_function" ); *) - (* ( Core__ops__index__Index__index, *) - (* fun args -> string "PLACEHOLDER_library_function" ); *) - (* ( Rust_primitives__unsize, *) - (* fun args -> string "PLACEHOLDER_library_function" ); *) - (* ( Core__num__Impl_9__to_le_bytes, *) - (* fun args -> string "PLACEHOLDER_library_function" ); *) - (* ( Alloc__slice__Impl__into_vec, *) - (* fun args -> string "PLACEHOLDER_library_function" ); *) - (* ( Alloc__vec__Impl_1__truncate, *) - (* fun args -> string "PLACEHOLDER_library_function" ); *) - (* ( Alloc__vec__Impl_2__extend_from_slice, *) - (* fun args -> string "PLACEHOLDER_library_function" ); *) - (* ( Alloc__slice__Impl__concat, *) - (* fun args -> string "PLACEHOLDER_library_function" ); *) - (* ( Core__option__Impl__is_some, *) - (* fun args -> string "PLACEHOLDER_library_function" ); *) - (* (\* core::clone::Clone_f_clone *\) *) - (* ( Core__clone__Clone__clone, *) - (* fun args -> string "PLACEHOLDER_library_function" ); *) - (* (\* core::cmp::PartialEq::eq *\) *) - (* ( Core__cmp__PartialEq__eq, *) - (* fun args -> string "PLACEHOLDER_library_function" ); *) - (* (\* core::cmp::PartialEq_f_ne *\) *) - (* ( Core__cmp__PartialEq__ne, *) - (* fun args -> string "PLACEHOLDER_library_function" ); *) - (* (\* core::cmp::PartialOrd::lt *\) *) - (* ( Core__cmp__PartialOrd__lt, *) - (* fun args -> string "PLACEHOLDER_library_function" ); *) - (* (\* core::ops::arith::Add::add *\) *) - (* ( Core__ops__arith__Add__add, *) - (* fun args -> string "PLACEHOLDER_library_function" ); *) - (* (\* core::ops::arith::Sub::sub *\) *) - (* ( Core__ops__arith__Sub__sub, *) - (* fun args -> string "PLACEHOLDER_library_function" ); *) - (* (\* core::option::Option_Option_None_c *\) *) - (* ( Core__option__Option__None, *) - (* fun args -> string "PLACEHOLDER_library_function" ); *) - (* (\* core::option::Option_Option_Some_c *\) *) - (* ( Core__option__Option__Some, *) - (* fun args -> string "PLACEHOLDER_library_function" ); *) - (* (\* core::result::impl__map_err *\) *) - (* ( Core__result__Impl__map_err, *) - (* fun args -> string "PLACEHOLDER_library_function" ); *) - (* (\* Crypto dependencies *\) *) - (* (\* hax_lib_protocol::cal::hash *\) *) - (* ( Hax_lib_protocol__crypto__hash, *) - (* fun args -> string "PLACEHOLDER_library_function" ); *) - (* (\* hax_lib_protocol::cal::hmac *\) *) - (* ( Hax_lib_protocol__crypto__hmac, *) - (* fun args -> string "PLACEHOLDER_library_function" ); *) - (* (\* hax_lib_protocol::cal::aead_decrypt *\) *) - (* ( Hax_lib_protocol__crypto__aead_decrypt, *) - (* fun args -> string "PLACEHOLDER_library_function" ); *) - (* (\* hax_lib_protocol::cal::aead_encrypt *\) *) - (* ( Hax_lib_protocol__crypto__aead_encrypt, *) - (* fun args -> string "PLACEHOLDER_library_function" ); *) - (* (\* hax_lib_protocol::cal::dh_scalar_multiply *\) *) - (* ( Hax_lib_protocol__crypto__dh_scalar_multiply, *) - (* fun args -> string "PLACEHOLDER_library_function" ); *) - (* (\* hax_lib_protocol::cal::dh_scalar_multiply_base *\) *) - (* ( Hax_lib_protocol__crypto__dh_scalar_multiply_base, *) - (* fun args -> string "PLACEHOLDER_library_function" ); *) - (* (\* hax_lib_protocol::cal::impl__DHScalar__from_bytes *\) *) - (* ( Hax_lib_protocol__crypto__Impl__from_bytes, *) - (* fun args -> string "PLACEHOLDER_library_function" ); *) - (* (\* hax_lib_protocol::cal::impl__DHElement__from_bytes *\) *) - (* ( Hax_lib_protocol__crypto__Impl_1__from_bytes, *) - (* fun args -> string "PLACEHOLDER_library_function" ); *) - (* (\* hax_lib_protocol::cal::impl__AEADKey__from_bytes *\) *) - (* ( Hax_lib_protocol__crypto__Impl_4__from_bytes, *) - (* fun args -> string "PLACEHOLDER_library_function" ); *) - (* (\* hax_lib_protocol::cal::impl__AEADIV__from_bytes *\) *) - (* ( Hax_lib_protocol__crypto__Impl_5__from_bytes, *) - (* fun args -> string "PLACEHOLDER_library_function" ); *) - (* (\* hax_lib_protocol::cal::impl__AEADTag__from_bytes *\) *) - (* ( Hax_lib_protocol__crypto__Impl_6__from_bytes, *) - (* fun args -> string "PLACEHOLDER_library_function" ); *) ] - - let library_constructors : - (Concrete_ident_generated.name - * ((global_ident * AST.expr) list -> document)) - list = - [ (* ( Core__option__Option__Some, *) - (* fun args -> string "PLACEHOLDER_library_constructor" ); *) - (* ( Core__option__Option__None, *) - (* fun args -> string "PLACEHOLDER_library_constructor" ); *) - (* ( Core__ops__range__Range, *) - (* fun args -> string "PLACEHOLDER_library_constructor" ); *) - (* (\* hax_lib_protocol::cal::(HashAlgorithm_HashAlgorithm_Sha256_c *\) *) - (* ( Hax_lib_protocol__crypto__HashAlgorithm__Sha256, *) - (* fun args -> string "PLACEHOLDER_library_constructor" ); *) - (* (\* hax_lib_protocol::cal::DHGroup_DHGroup_X25519_c *\) *) - (* ( Hax_lib_protocol__crypto__DHGroup__X25519, *) - (* fun args -> string "PLACEHOLDER_library_constructor" ); *) - (* (\* hax_lib_protocol::cal::AEADAlgorithm_AEADAlgorithm_Chacha20Poly1305_c *\) *) - (* ( Hax_lib_protocol__crypto__AEADAlgorithm__Chacha20Poly1305, *) - (* fun args -> string "PLACEHOLDER_library_constructor" ); *) - (* (\* hax_lib_protocol::cal::HMACAlgorithm_HMACAlgorithm_Sha256_c *\) *) - (* ( Hax_lib_protocol__crypto__HMACAlgorithm__Sha256, *) - (* fun args -> string "PLACEHOLDER_library_constructor" ); *) ] - - let library_constructor_patterns : - (Concrete_ident_generated.name * (field_pat list -> document)) list = - [ (* ( Core__option__Option__Some, *) - (* fun args -> string "PLACEHOLDER_library_constructor" ); *) - (* ( Core__option__Option__None, *) - (* fun args -> string "PLACEHOLDER_library_constructor" ); *) - (* ( Core__ops__range__Range, *) - (* fun args -> string "PLACEHOLDER_library_constructor" ); *) - (* (\* hax_lib_protocol::cal::(HashAlgorithm_HashAlgorithm_Sha256_c *\) *) - (* ( Hax_lib_protocol__crypto__HashAlgorithm__Sha256, *) - (* fun args -> string "PLACEHOLDER_library_constructor" ); *) - (* (\* hax_lib_protocol::cal::DHGroup_DHGroup_X25519_c *\) *) - (* ( Hax_lib_protocol__crypto__DHGroup__X25519, *) - (* fun args -> string "PLACEHOLDER_library_constructor" ); *) - (* (\* hax_lib_protocol::cal::AEADAlgorithm_AEADAlgorithm_Chacha20Poly1305_c *\) *) - (* ( Hax_lib_protocol__crypto__AEADAlgorithm__Chacha20Poly1305, *) - (* fun args -> string "PLACEHOLDER_library_constructor" ); *) - (* (\* hax_lib_protocol::cal::HMACAlgorithm_HMACAlgorithm_Sha256_c *\) *) - (* ( Hax_lib_protocol__crypto__HMACAlgorithm__Sha256, *) - (* fun args -> string "PLACEHOLDER_library_constructor" ); *) ] - - let library_types : (Concrete_ident_generated.name * document) list = - [ (* (\* hax_lib_protocol::cal::(t_DHScalar *\) *) - (* (Hax_lib_protocol__crypto__DHScalar, string "PLACEHOLDER_library_type"); *) - (* (Core__option__Option, string "PLACEHOLDER_library_type"); *) - (* (Alloc__vec__Vec, string "PLACEHOLDER_library_type"); *) ] - - let assoc_known_name name (known_name, _) = - Global_ident.eq_name known_name name - - let translate_known_name name ~dict = - List.find ~f:(assoc_known_name name) dict - - class print aux = - object (print) - inherit GenericPrint.print as super - - method field_accessor field_name = - string "accessor" ^^ underscore ^^ print#concrete_ident field_name - - method match_arm scrutinee { arm_pat; body } = - let body = print#expr_at Arm_body body in - match arm_pat with - | { p = PWild; _ } -> body - | _ -> - let scrutinee = print#expr_at Expr_Match_scrutinee scrutinee in - let pat = print#pat_at Arm_pat arm_pat |> group in - string "let" ^^ space ^^ pat ^^ string " = " ^^ scrutinee - ^^ string " in " ^^ body - - method ty_bool = string "bool" - method ty_int _ = string "nat" - - method pat' : Generic_printer_base.par_state -> pat' fn = - fun ctx -> - let wrap_parens = - group - >> match ctx with AlreadyPar -> Fn.id | NeedsPar -> iblock braces - in - fun pat -> - match pat with - | PConstruct { name; args } -> ( - match - translate_known_name name ~dict:library_constructor_patterns - with - | Some (_, translation) -> translation args - | None -> super#pat' ctx pat) - | _ -> super#pat' ctx pat - - method tuple_elem_pat' : Generic_printer_base.par_state -> pat' fn = - fun ctx -> - let wrap_parens = - group - >> match ctx with AlreadyPar -> Fn.id | NeedsPar -> iblock braces - in - function - | PBinding { mut; mode; var; typ; subpat } -> - let p = print#local_ident var in - p ^^ colon ^^ space ^^ print#ty ctx typ - | p -> print#pat' ctx p - - method tuple_elem_pat : Generic_printer_base.par_state -> pat fn = - fun ctx { p; span; _ } -> - print#with_span ~span (fun _ -> print#tuple_elem_pat' ctx p) - - method tuple_elem_pat_at = print#par_state >> print#tuple_elem_pat - - method! pat_construct_tuple : pat list fn = - List.map ~f:(print#tuple_elem_pat_at Pat_ConstructTuple) - >> print#doc_construct_tuple - - method! expr_app f args _generic_args = - let args = - separate_map - (comma ^^ break 1) - (print#expr_at Expr_App_arg >> group) - args - in - let f = - match f with - | { e = GlobalVar name; _ } -> ( - match name with - | `Projector (`Concrete i) | `Concrete i -> - print#concrete_ident i |> group - | _ -> super#expr_at Expr_App_f f |> group) - in - f ^^ iblock parens args - - method! expr' : Generic_printer_base.par_state -> expr' fn = - fun ctx e -> - let wrap_parens = - group - >> match ctx with AlreadyPar -> Fn.id | NeedsPar -> iblock braces - in - match e with - (* Translate known functions *) - | App { f = { e = GlobalVar name; _ }; args } -> ( - match translate_known_name name ~dict:library_functions with - | Some (name, translation) -> translation args - | None -> ( - match name with - | `Projector (`Concrete name) -> - print#field_accessor name - ^^ iblock parens - (separate_map - (comma ^^ break 1) - (fun arg -> print#expr AlreadyPar arg) - args) - | _ -> super#expr' ctx e)) - | Construct { constructor; fields; _ } - when Global_ident.eq_name Core__result__Result__Ok constructor -> - super#expr' ctx (snd (Option.value_exn (List.hd fields))).e - | Construct { constructor; _ } - when Global_ident.eq_name Core__result__Result__Err constructor -> - string "construct_fail()" - (* Translate known constructors *) - | Construct { constructor; fields } -> ( - match - translate_known_name constructor ~dict:library_constructors - with - | Some (name, translation) -> translation fields - | None -> super#expr' ctx e) - (* Desugared `?` operator *) - | Match - { - scrutinee = - { e = App { f = { e = GlobalVar n; _ }; args = [ expr ] }; _ }; - arms = _; - } - (*[@ocamlformat "disable"]*) - when Global_ident.eq_name Core__ops__try_trait__Try__branch n -> - super#expr' ctx expr.e - | Match { scrutinee; arms } -> - separate_map - (hardline ^^ string "else ") - (fun { arm; span } -> print#match_arm scrutinee arm) - arms - | If { cond; then_; else_ } -> - let if_then = - (string "if" ^//^ nest 2 (print#expr_at Expr_If_cond cond)) - ^/^ string "then" - ^//^ (print#expr_at Expr_If_then then_ |> parens |> nest 1) - in - (match else_ with - | None -> if_then - | Some else_ -> - if_then ^^ break 1 ^^ string "else" ^^ space - ^^ (print#expr_at Expr_If_else else_ |> iblock parens)) - |> wrap_parens - | _ -> super#expr' ctx e - - method concrete_ident = print#concrete_ident' ~under_current_ns:false - - method! item' item = - let fun_and_reduc base_name constructor = - let field_prefix = - if constructor.is_record then empty - else print#concrete_ident base_name - in - let fun_args = constructor.arguments in - let fun_args_full = - separate_map - (comma ^^ break 1) - (fun (x, y, _z) -> - print#concrete_ident x ^^ string ": " ^^ print#ty_at Param_typ y) - fun_args - in - let fun_args_names = - separate_map - (comma ^^ break 1) - (fst3 >> fun x -> print#concrete_ident x) - fun_args - in - let fun_args_types = - separate_map - (comma ^^ break 1) - (snd3 >> print#ty_at Param_typ) - fun_args - in - let constructor_name = print#concrete_ident constructor.name in - - let fun_line = - string "fun" ^^ space ^^ constructor_name - ^^ iblock parens fun_args_types - ^^ string ": " - ^^ print#concrete_ident base_name - ^^ space ^^ string "[data]" ^^ dot - in - let reduc_line = - string "reduc forall " ^^ iblock Fn.id fun_args_full ^^ semi - in - let build_accessor (ident, ty, attr) = - print#field_accessor ident - ^^ iblock parens (constructor_name ^^ iblock parens fun_args_names) - ^^ blank 1 ^^ equals ^^ blank 1 ^^ print#concrete_ident ident - in - let reduc_lines = - separate_map (dot ^^ hardline) - (fun arg -> reduc_line ^^ nest 4 (hardline ^^ build_accessor arg)) - fun_args - in - fun_line ^^ hardline ^^ reduc_lines - ^^ if reduc_lines == empty then empty else dot - in - match item with - (* `fn`s are transformed into `letfun` process macros. *) - | Fn { name; generics; body; params } -> - let params_string = - iblock parens (separate_map (comma ^^ break 1) print#param params) - in - string "letfun" ^^ space - ^^ align - (print#concrete_ident name ^^ params_string ^^ space ^^ equals - ^^ hardline - ^^ print#expr_at Item_Fn_body body - ^^ dot) - (* `struct` definitions are transformed into simple constructors and `reduc`s for accessing fields. *) - | Type { name; generics; variants; is_struct } -> - let type_line = - string "type " ^^ print#concrete_ident name ^^ dot - in - let type_converter_line = - string "fun " ^^ print#concrete_ident name - ^^ string "_to_bitstring" - ^^ iblock parens (print#concrete_ident name) - ^^ string ": bitstring [typeConverter]." - in - if is_struct then - let struct_constructor = List.hd variants in - match struct_constructor with - | None -> empty - | Some constructor -> - type_line ^^ hardline ^^ type_converter_line ^^ hardline - ^^ fun_and_reduc name constructor - else - type_line ^^ hardline ^^ type_converter_line ^^ hardline - ^^ separate_map (hardline ^^ hardline) - (fun variant -> fun_and_reduc name variant) - variants - | _ -> empty - - method! expr_let : lhs:pat -> rhs:expr -> expr fn = - fun ~lhs ~rhs body -> - string "let" ^^ space - ^^ iblock Fn.id (print#pat_at Expr_Let_lhs lhs) - ^^ space ^^ equals ^^ space - ^^ iblock Fn.id (print#expr_at Expr_Let_rhs rhs) - ^^ space ^^ string "in" ^^ hardline - ^^ (print#expr_at Expr_Let_body body |> group) - - method concrete_ident' ~(under_current_ns : bool) : concrete_ident fn = - fun id -> - if under_current_ns then print#name_of_concrete_ident id - else - let crate, path = print#namespace_of_concrete_ident id in - let full_path = crate :: path in - separate_map (underscore ^^ underscore) utf8string full_path - ^^ underscore ^^ underscore - ^^ print#name_of_concrete_ident id - - method! doc_construct_inductive - : is_record:bool -> - is_struct:bool -> - constructor:concrete_ident -> - base:document option -> - (global_ident * document) list fn = - fun ~is_record ~is_struct:_ ~constructor ~base:_ args -> - if is_record then - print#concrete_ident constructor - ^^ iblock parens - (separate_map - (break 0 ^^ comma) - (fun (field, body) -> iblock Fn.id body |> group) - args) - else - print#concrete_ident constructor - ^^ iblock parens (separate_map (comma ^^ break 1) snd args) - - method generic_values : generic_value list fn = - function - | [] -> empty - | values -> - string "_of" ^^ underscore - ^^ separate_map underscore print#generic_value values - - method ty_app f args = print#concrete_ident f ^^ print#generic_values args - - method ty : Generic_printer_base.par_state -> ty fn = - fun ctx ty -> - match ty with - | TBool -> print#ty_bool - | TParam i -> print#local_ident i - | TInt kind -> print#ty_int kind - (* Translate known types, no args at the moment *) - | TApp { ident; args } -> super#ty ctx ty - (*( - match translate_known_name ident ~dict:library_types with - | Some (_, translation) -> translation - | None -> super#ty ctx ty)*) - | _ -> string "bitstring" - end - - type proverif_aux_info = CrateFns of AST.item list | NoAuxInfo - - include Api (struct - type aux_info = proverif_aux_info - - let new_print aux = (new print aux :> print_object) - end) -end - -let filter_crate_functions (items : AST.item list) = - List.filter ~f:(fun item -> [%matches? Fn _] item.v) items - -let is_process_read : attrs -> bool = - Attr_payloads.payloads >> List.exists ~f:(fst >> [%matches? Types.ProcessRead]) - -let is_process_write : attrs -> bool = - Attr_payloads.payloads - >> List.exists ~f:(fst >> [%matches? Types.ProcessWrite]) - -let is_process_init : attrs -> bool = - Attr_payloads.payloads >> List.exists ~f:(fst >> [%matches? Types.ProcessInit]) - -let is_process item = - is_process_read item.attrs - || is_process_write item.attrs - || is_process_init item.attrs - -module type Subprinter = sig - val print : AST.item list -> string -end +(* module Print = struct *) +(* module GenericPrint = *) +(* Generic_printer.Make (InputLanguage) (U.Concrete_ident_view) *) + +(* open Generic_printer_base.Make (InputLanguage) *) +(* open PPrint *) + +(* let iblock f = group >> jump 2 0 >> terminate (break 0) >> f >> group *) + +(* (\* TODO: Give definitions for core / known library functions, cf issues #447, #448 *\) *) +(* let library_functions : *) +(* (Concrete_ident_generated.name * (AST.expr list -> document)) list = *) +(* [ (\* (\\* Core dependencies *\\) *\) *) +(* (\* (Alloc__vec__from_elem, fun args -> string "PLACEHOLDER_library_function"); *\) *) +(* (\* ( Alloc__slice__Impl__to_vec, *\) *) +(* (\* fun args -> string "PLACEHOLDER_library_function" ); *\) *) +(* (\* (Core__slice__Impl__len, fun args -> string "PLACEHOLDER_library_function"); *\) *) +(* (\* ( Core__ops__deref__Deref__deref, *\) *) +(* (\* fun args -> string "PLACEHOLDER_library_function" ); *\) *) +(* (\* ( Core__ops__index__Index__index, *\) *) +(* (\* fun args -> string "PLACEHOLDER_library_function" ); *\) *) +(* (\* ( Rust_primitives__unsize, *\) *) +(* (\* fun args -> string "PLACEHOLDER_library_function" ); *\) *) +(* (\* ( Core__num__Impl_9__to_le_bytes, *\) *) +(* (\* fun args -> string "PLACEHOLDER_library_function" ); *\) *) +(* (\* ( Alloc__slice__Impl__into_vec, *\) *) +(* (\* fun args -> string "PLACEHOLDER_library_function" ); *\) *) +(* (\* ( Alloc__vec__Impl_1__truncate, *\) *) +(* (\* fun args -> string "PLACEHOLDER_library_function" ); *\) *) +(* (\* ( Alloc__vec__Impl_2__extend_from_slice, *\) *) +(* (\* fun args -> string "PLACEHOLDER_library_function" ); *\) *) +(* (\* ( Alloc__slice__Impl__concat, *\) *) +(* (\* fun args -> string "PLACEHOLDER_library_function" ); *\) *) +(* (\* ( Core__option__Impl__is_some, *\) *) +(* (\* fun args -> string "PLACEHOLDER_library_function" ); *\) *) +(* (\* (\\* core::clone::Clone_f_clone *\\) *\) *) +(* (\* ( Core__clone__Clone__clone, *\) *) +(* (\* fun args -> string "PLACEHOLDER_library_function" ); *\) *) +(* (\* (\\* core::cmp::PartialEq::eq *\\) *\) *) +(* (\* ( Core__cmp__PartialEq__eq, *\) *) +(* (\* fun args -> string "PLACEHOLDER_library_function" ); *\) *) +(* (\* (\\* core::cmp::PartialEq_f_ne *\\) *\) *) +(* (\* ( Core__cmp__PartialEq__ne, *\) *) +(* (\* fun args -> string "PLACEHOLDER_library_function" ); *\) *) +(* (\* (\\* core::cmp::PartialOrd::lt *\\) *\) *) +(* (\* ( Core__cmp__PartialOrd__lt, *\) *) +(* (\* fun args -> string "PLACEHOLDER_library_function" ); *\) *) +(* (\* (\\* core::ops::arith::Add::add *\\) *\) *) +(* (\* ( Core__ops__arith__Add__add, *\) *) +(* (\* fun args -> string "PLACEHOLDER_library_function" ); *\) *) +(* (\* (\\* core::ops::arith::Sub::sub *\\) *\) *) +(* (\* ( Core__ops__arith__Sub__sub, *\) *) +(* (\* fun args -> string "PLACEHOLDER_library_function" ); *\) *) +(* (\* (\\* core::option::Option_Option_None_c *\\) *\) *) +(* (\* ( Core__option__Option__None, *\) *) +(* (\* fun args -> string "PLACEHOLDER_library_function" ); *\) *) +(* (\* (\\* core::option::Option_Option_Some_c *\\) *\) *) +(* (\* ( Core__option__Option__Some, *\) *) +(* (\* fun args -> string "PLACEHOLDER_library_function" ); *\) *) +(* (\* (\\* core::result::impl__map_err *\\) *\) *) +(* (\* ( Core__result__Impl__map_err, *\) *) +(* (\* fun args -> string "PLACEHOLDER_library_function" ); *\) *) +(* (\* (\\* Crypto dependencies *\\) *\) *) +(* (\* (\\* hax_lib_protocol::cal::hash *\\) *\) *) +(* (\* ( Hax_lib_protocol__crypto__hash, *\) *) +(* (\* fun args -> string "PLACEHOLDER_library_function" ); *\) *) +(* (\* (\\* hax_lib_protocol::cal::hmac *\\) *\) *) +(* (\* ( Hax_lib_protocol__crypto__hmac, *\) *) +(* (\* fun args -> string "PLACEHOLDER_library_function" ); *\) *) +(* (\* (\\* hax_lib_protocol::cal::aead_decrypt *\\) *\) *) +(* (\* ( Hax_lib_protocol__crypto__aead_decrypt, *\) *) +(* (\* fun args -> string "PLACEHOLDER_library_function" ); *\) *) +(* (\* (\\* hax_lib_protocol::cal::aead_encrypt *\\) *\) *) +(* (\* ( Hax_lib_protocol__crypto__aead_encrypt, *\) *) +(* (\* fun args -> string "PLACEHOLDER_library_function" ); *\) *) +(* (\* (\\* hax_lib_protocol::cal::dh_scalar_multiply *\\) *\) *) +(* (\* ( Hax_lib_protocol__crypto__dh_scalar_multiply, *\) *) +(* (\* fun args -> string "PLACEHOLDER_library_function" ); *\) *) +(* (\* (\\* hax_lib_protocol::cal::dh_scalar_multiply_base *\\) *\) *) +(* (\* ( Hax_lib_protocol__crypto__dh_scalar_multiply_base, *\) *) +(* (\* fun args -> string "PLACEHOLDER_library_function" ); *\) *) +(* (\* (\\* hax_lib_protocol::cal::impl__DHScalar__from_bytes *\\) *\) *) +(* (\* ( Hax_lib_protocol__crypto__Impl__from_bytes, *\) *) +(* (\* fun args -> string "PLACEHOLDER_library_function" ); *\) *) +(* (\* (\\* hax_lib_protocol::cal::impl__DHElement__from_bytes *\\) *\) *) +(* (\* ( Hax_lib_protocol__crypto__Impl_1__from_bytes, *\) *) +(* (\* fun args -> string "PLACEHOLDER_library_function" ); *\) *) +(* (\* (\\* hax_lib_protocol::cal::impl__AEADKey__from_bytes *\\) *\) *) +(* (\* ( Hax_lib_protocol__crypto__Impl_4__from_bytes, *\) *) +(* (\* fun args -> string "PLACEHOLDER_library_function" ); *\) *) +(* (\* (\\* hax_lib_protocol::cal::impl__AEADIV__from_bytes *\\) *\) *) +(* (\* ( Hax_lib_protocol__crypto__Impl_5__from_bytes, *\) *) +(* (\* fun args -> string "PLACEHOLDER_library_function" ); *\) *) +(* (\* (\\* hax_lib_protocol::cal::impl__AEADTag__from_bytes *\\) *\) *) +(* (\* ( Hax_lib_protocol__crypto__Impl_6__from_bytes, *\) *) +(* (\* fun args -> string "PLACEHOLDER_library_function" ); *\) ] *) + +(* let library_constructors : *) +(* (Concrete_ident_generated.name *) +(* * ((global_ident * AST.expr) list -> document)) *) +(* list = *) +(* [ (\* ( Core__option__Option__Some, *\) *) +(* (\* fun args -> string "PLACEHOLDER_library_constructor" ); *\) *) +(* (\* ( Core__option__Option__None, *\) *) +(* (\* fun args -> string "PLACEHOLDER_library_constructor" ); *\) *) +(* (\* ( Core__ops__range__Range, *\) *) +(* (\* fun args -> string "PLACEHOLDER_library_constructor" ); *\) *) +(* (\* (\\* hax_lib_protocol::cal::(HashAlgorithm_HashAlgorithm_Sha256_c *\\) *\) *) +(* (\* ( Hax_lib_protocol__crypto__HashAlgorithm__Sha256, *\) *) +(* (\* fun args -> string "PLACEHOLDER_library_constructor" ); *\) *) +(* (\* (\\* hax_lib_protocol::cal::DHGroup_DHGroup_X25519_c *\\) *\) *) +(* (\* ( Hax_lib_protocol__crypto__DHGroup__X25519, *\) *) +(* (\* fun args -> string "PLACEHOLDER_library_constructor" ); *\) *) +(* (\* (\\* hax_lib_protocol::cal::AEADAlgorithm_AEADAlgorithm_Chacha20Poly1305_c *\\) *\) *) +(* (\* ( Hax_lib_protocol__crypto__AEADAlgorithm__Chacha20Poly1305, *\) *) +(* (\* fun args -> string "PLACEHOLDER_library_constructor" ); *\) *) +(* (\* (\\* hax_lib_protocol::cal::HMACAlgorithm_HMACAlgorithm_Sha256_c *\\) *\) *) +(* (\* ( Hax_lib_protocol__crypto__HMACAlgorithm__Sha256, *\) *) +(* (\* fun args -> string "PLACEHOLDER_library_constructor" ); *\) ] *) + +(* let library_constructor_patterns : *) +(* (Concrete_ident_generated.name * (field_pat list -> document)) list = *) +(* [ (\* ( Core__option__Option__Some, *\) *) +(* (\* fun args -> string "PLACEHOLDER_library_constructor" ); *\) *) +(* (\* ( Core__option__Option__None, *\) *) +(* (\* fun args -> string "PLACEHOLDER_library_constructor" ); *\) *) +(* (\* ( Core__ops__range__Range, *\) *) +(* (\* fun args -> string "PLACEHOLDER_library_constructor" ); *\) *) +(* (\* (\\* hax_lib_protocol::cal::(HashAlgorithm_HashAlgorithm_Sha256_c *\\) *\) *) +(* (\* ( Hax_lib_protocol__crypto__HashAlgorithm__Sha256, *\) *) +(* (\* fun args -> string "PLACEHOLDER_library_constructor" ); *\) *) +(* (\* (\\* hax_lib_protocol::cal::DHGroup_DHGroup_X25519_c *\\) *\) *) +(* (\* ( Hax_lib_protocol__crypto__DHGroup__X25519, *\) *) +(* (\* fun args -> string "PLACEHOLDER_library_constructor" ); *\) *) +(* (\* (\\* hax_lib_protocol::cal::AEADAlgorithm_AEADAlgorithm_Chacha20Poly1305_c *\\) *\) *) +(* (\* ( Hax_lib_protocol__crypto__AEADAlgorithm__Chacha20Poly1305, *\) *) +(* (\* fun args -> string "PLACEHOLDER_library_constructor" ); *\) *) +(* (\* (\\* hax_lib_protocol::cal::HMACAlgorithm_HMACAlgorithm_Sha256_c *\\) *\) *) +(* (\* ( Hax_lib_protocol__crypto__HMACAlgorithm__Sha256, *\) *) +(* (\* fun args -> string "PLACEHOLDER_library_constructor" ); *\) ] *) + +(* let library_types : (Concrete_ident_generated.name * document) list = *) +(* [ (\* (\\* hax_lib_protocol::cal::(t_DHScalar *\\) *\) *) +(* (\* (Hax_lib_protocol__crypto__DHScalar, string "PLACEHOLDER_library_type"); *\) *) +(* (\* (Core__option__Option, string "PLACEHOLDER_library_type"); *\) *) +(* (\* (Alloc__vec__Vec, string "PLACEHOLDER_library_type"); *\) ] *) + +(* let assoc_known_name name (known_name, _) = *) +(* Global_ident.eq_name known_name name *) + +(* let translate_known_name name ~dict = *) +(* List.find ~f:(assoc_known_name name) dict *) + +(* class print aux = *) +(* object (print) *) +(* inherit GenericPrint.print as super *) + +(* method field_accessor field_name = *) +(* string "accessor" ^^ underscore ^^ print#concrete_ident field_name *) + +(* method match_arm scrutinee { arm_pat; body } = *) +(* let body = print#expr_at Arm_body body in *) +(* match arm_pat with *) +(* | { p = PWild; _ } -> body *) +(* | _ -> *) +(* let scrutinee = print#expr_at Expr_Match_scrutinee scrutinee in *) +(* let pat = print#pat_at Arm_pat arm_pat |> group in *) +(* string "let" ^^ space ^^ pat ^^ string " = " ^^ scrutinee *) +(* ^^ string " in " ^^ body *) + +(* method ty_bool = string "bool" *) +(* method ty_int _ = string "nat" *) + +(* method pat' : Generic_printer_base.par_state -> pat' fn = *) +(* fun ctx -> *) +(* let wrap_parens = *) +(* group *) +(* >> match ctx with AlreadyPar -> Fn.id | NeedsPar -> iblock braces *) +(* in *) +(* fun pat -> *) +(* match pat with *) +(* | PConstruct { name; args } -> ( *) +(* match *) +(* translate_known_name name ~dict:library_constructor_patterns *) +(* with *) +(* | Some (_, translation) -> translation args *) +(* | None -> super#pat' ctx pat) *) +(* | _ -> super#pat' ctx pat *) + +(* method tuple_elem_pat' : Generic_printer_base.par_state -> pat' fn = *) +(* fun ctx -> *) +(* let wrap_parens = *) +(* group *) +(* >> match ctx with AlreadyPar -> Fn.id | NeedsPar -> iblock braces *) +(* in *) +(* function *) +(* | PBinding { mut; mode; var; typ; subpat } -> *) +(* let p = print#local_ident var in *) +(* p ^^ colon ^^ space ^^ print#ty ctx typ *) +(* | p -> print#pat' ctx p *) + +(* method tuple_elem_pat : Generic_printer_base.par_state -> pat fn = *) +(* fun ctx { p; span; _ } -> *) +(* print#with_span ~span (fun _ -> print#tuple_elem_pat' ctx p) *) + +(* method tuple_elem_pat_at = print#par_state >> print#tuple_elem_pat *) + +(* method! pat_construct_tuple : pat list fn = *) +(* List.map ~f:(print#tuple_elem_pat_at Pat_ConstructTuple) *) +(* >> print#doc_construct_tuple *) + +(* method! expr_app f args _generic_args = *) +(* let args = *) +(* separate_map *) +(* (comma ^^ break 1) *) +(* (print#expr_at Expr_App_arg >> group) *) +(* args *) +(* in *) +(* let f = *) +(* match f with *) +(* | { e = GlobalVar name; _ } -> ( *) +(* match name with *) +(* | `Projector (`Concrete i) | `Concrete i -> *) +(* print#concrete_ident i |> group *) +(* | _ -> super#expr_at Expr_App_f f |> group) *) +(* in *) +(* f ^^ iblock parens args *) + +(* method! expr' : Generic_printer_base.par_state -> expr' fn = *) +(* fun ctx e -> *) +(* let wrap_parens = *) +(* group *) +(* >> match ctx with AlreadyPar -> Fn.id | NeedsPar -> iblock braces *) +(* in *) +(* match e with *) +(* (\* Translate known functions *\) *) +(* | App { f = { e = GlobalVar name; _ }; args } -> ( *) +(* match translate_known_name name ~dict:library_functions with *) +(* | Some (name, translation) -> translation args *) +(* | None -> ( *) +(* match name with *) +(* | `Projector (`Concrete name) -> *) +(* print#field_accessor name *) +(* ^^ iblock parens *) +(* (separate_map *) +(* (comma ^^ break 1) *) +(* (fun arg -> print#expr AlreadyPar arg) *) +(* args) *) +(* | _ -> super#expr' ctx e)) *) +(* | Construct { constructor; fields; _ } *) +(* when Global_ident.eq_name Core__result__Result__Ok constructor -> *) +(* super#expr' ctx (snd (Option.value_exn (List.hd fields))).e *) +(* | Construct { constructor; _ } *) +(* when Global_ident.eq_name Core__result__Result__Err constructor -> *) +(* string "construct_fail()" *) +(* (\* Translate known constructors *\) *) +(* | Construct { constructor; fields } -> ( *) +(* match *) +(* translate_known_name constructor ~dict:library_constructors *) +(* with *) +(* | Some (name, translation) -> translation fields *) +(* | None -> super#expr' ctx e) *) +(* (\* Desugared `?` operator *\) *) +(* | Match *) +(* { *) +(* scrutinee = *) +(* { e = App { f = { e = GlobalVar n; _ }; args = [ expr ] }; _ }; *) +(* arms = _; *) +(* } *) +(* (\*[@ocamlformat "disable"]*\) *) +(* when Global_ident.eq_name Core__ops__try_trait__Try__branch n -> *) +(* super#expr' ctx expr.e *) +(* | Match { scrutinee; arms } -> *) +(* separate_map *) +(* (hardline ^^ string "else ") *) +(* (fun { arm; span } -> print#match_arm scrutinee arm) *) +(* arms *) +(* | If { cond; then_; else_ } -> *) +(* let if_then = *) +(* (string "if" ^//^ nest 2 (print#expr_at Expr_If_cond cond)) *) +(* ^/^ string "then" *) +(* ^//^ (print#expr_at Expr_If_then then_ |> parens |> nest 1) *) +(* in *) +(* (match else_ with *) +(* | None -> if_then *) +(* | Some else_ -> *) +(* if_then ^^ break 1 ^^ string "else" ^^ space *) +(* ^^ (print#expr_at Expr_If_else else_ |> iblock parens)) *) +(* |> wrap_parens *) +(* | _ -> super#expr' ctx e *) + +(* method concrete_ident = print#concrete_ident' ~under_current_ns:false *) + +(* method! item' item = *) +(* let fun_and_reduc base_name constructor = *) +(* let field_prefix = *) +(* if constructor.is_record then empty *) +(* else print#concrete_ident base_name *) +(* in *) +(* let fun_args = constructor.arguments in *) +(* let fun_args_full = *) +(* separate_map *) +(* (comma ^^ break 1) *) +(* (fun (x, y, _z) -> *) +(* print#concrete_ident x ^^ string ": " ^^ print#ty_at Param_typ y) *) +(* fun_args *) +(* in *) +(* let fun_args_names = *) +(* separate_map *) +(* (comma ^^ break 1) *) +(* (fst3 >> fun x -> print#concrete_ident x) *) +(* fun_args *) +(* in *) +(* let fun_args_types = *) +(* separate_map *) +(* (comma ^^ break 1) *) +(* (snd3 >> print#ty_at Param_typ) *) +(* fun_args *) +(* in *) +(* let constructor_name = print#concrete_ident constructor.name in *) + +(* let fun_line = *) +(* string "fun" ^^ space ^^ constructor_name *) +(* ^^ iblock parens fun_args_types *) +(* ^^ string ": " *) +(* ^^ print#concrete_ident base_name *) +(* ^^ space ^^ string "[data]" ^^ dot *) +(* in *) +(* let reduc_line = *) +(* string "reduc forall " ^^ iblock Fn.id fun_args_full ^^ semi *) +(* in *) +(* let build_accessor (ident, ty, attr) = *) +(* print#field_accessor ident *) +(* ^^ iblock parens (constructor_name ^^ iblock parens fun_args_names) *) +(* ^^ blank 1 ^^ equals ^^ blank 1 ^^ print#concrete_ident ident *) +(* in *) +(* let reduc_lines = *) +(* separate_map (dot ^^ hardline) *) +(* (fun arg -> reduc_line ^^ nest 4 (hardline ^^ build_accessor arg)) *) +(* fun_args *) +(* in *) +(* fun_line ^^ hardline ^^ reduc_lines *) +(* ^^ if reduc_lines == empty then empty else dot *) +(* in *) +(* match item with *) +(* (\* `fn`s are transformed into `letfun` process macros. *\) *) +(* | Fn { name; generics; body; params } -> *) +(* let params_string = *) +(* iblock parens (separate_map (comma ^^ break 1) print#param params) *) +(* in *) +(* string "letfun" ^^ space *) +(* ^^ align *) +(* (print#concrete_ident name ^^ params_string ^^ space ^^ equals *) +(* ^^ hardline *) +(* ^^ print#expr_at Item_Fn_body body *) +(* ^^ dot) *) +(* (\* `struct` definitions are transformed into simple constructors and `reduc`s for accessing fields. *\) *) +(* | Type { name; generics; variants; is_struct } -> *) +(* let type_line = *) +(* string "type " ^^ print#concrete_ident name ^^ dot *) +(* in *) +(* let type_converter_line = *) +(* string "fun " ^^ print#concrete_ident name *) +(* ^^ string "_to_bitstring" *) +(* ^^ iblock parens (print#concrete_ident name) *) +(* ^^ string ": bitstring [typeConverter]." *) +(* in *) +(* if is_struct then *) +(* let struct_constructor = List.hd variants in *) +(* match struct_constructor with *) +(* | None -> empty *) +(* | Some constructor -> *) +(* type_line ^^ hardline ^^ type_converter_line ^^ hardline *) +(* ^^ fun_and_reduc name constructor *) +(* else *) +(* type_line ^^ hardline ^^ type_converter_line ^^ hardline *) +(* ^^ separate_map (hardline ^^ hardline) *) +(* (fun variant -> fun_and_reduc name variant) *) +(* variants *) +(* | _ -> empty *) + +(* method! expr_let : lhs:pat -> rhs:expr -> expr fn = *) +(* fun ~lhs ~rhs body -> *) +(* string "let" ^^ space *) +(* ^^ iblock Fn.id (print#pat_at Expr_Let_lhs lhs) *) +(* ^^ space ^^ equals ^^ space *) +(* ^^ iblock Fn.id (print#expr_at Expr_Let_rhs rhs) *) +(* ^^ space ^^ string "in" ^^ hardline *) +(* ^^ (print#expr_at Expr_Let_body body |> group) *) + +(* method concrete_ident' ~(under_current_ns : bool) : concrete_ident fn = *) +(* fun id -> *) +(* if under_current_ns then print#name_of_concrete_ident id *) +(* else *) +(* let crate, path = print#namespace_of_concrete_ident id in *) +(* let full_path = crate :: path in *) +(* separate_map (underscore ^^ underscore) utf8string full_path *) +(* ^^ underscore ^^ underscore *) +(* ^^ print#name_of_concrete_ident id *) + +(* method! doc_construct_inductive *) +(* : is_record:bool -> *) +(* is_struct:bool -> *) +(* constructor:concrete_ident -> *) +(* base:document option -> *) +(* (global_ident * document) list fn = *) +(* fun ~is_record ~is_struct:_ ~constructor ~base:_ args -> *) +(* if is_record then *) +(* print#concrete_ident constructor *) +(* ^^ iblock parens *) +(* (separate_map *) +(* (break 0 ^^ comma) *) +(* (fun (field, body) -> iblock Fn.id body |> group) *) +(* args) *) +(* else *) +(* print#concrete_ident constructor *) +(* ^^ iblock parens (separate_map (comma ^^ break 1) snd args) *) + +(* method generic_values : generic_value list fn = *) +(* function *) +(* | [] -> empty *) +(* | values -> *) +(* string "_of" ^^ underscore *) +(* ^^ separate_map underscore print#generic_value values *) + +(* method ty_app f args = print#concrete_ident f ^^ print#generic_values args *) + +(* method ty : Generic_printer_base.par_state -> ty fn = *) +(* fun ctx ty -> *) +(* match ty with *) +(* | TBool -> print#ty_bool *) +(* | TParam i -> print#local_ident i *) +(* | TInt kind -> print#ty_int kind *) +(* (\* Translate known types, no args at the moment *\) *) +(* | TApp { ident; args } -> super#ty ctx ty *) +(* (\*( *) +(* match translate_known_name ident ~dict:library_types with *) +(* | Some (_, translation) -> translation *) +(* | None -> super#ty ctx ty)*\) *) +(* | _ -> string "bitstring" *) +(* end *) + +(* type proverif_aux_info = CrateFns of AST.item list | NoAuxInfo *) + +(* include Api (struct *) +(* type aux_info = proverif_aux_info *) + +(* let new_print aux = (new print aux :> print_object) *) +(* end) *) +(* end *) + +(* let filter_crate_functions (items : AST.item list) = *) +(* List.filter ~f:(fun item -> [%matches? Fn _] item.v) items *) + +(* let is_process_read : attrs -> bool = *) +(* Attr_payloads.payloads >> List.exists ~f:(fst >> [%matches? Types.ProcessRead]) *) + +(* let is_process_write : attrs -> bool = *) +(* Attr_payloads.payloads *) +(* >> List.exists ~f:(fst >> [%matches? Types.ProcessWrite]) *) + +(* let is_process_init : attrs -> bool = *) +(* Attr_payloads.payloads >> List.exists ~f:(fst >> [%matches? Types.ProcessInit]) *) + +(* let is_process item = *) +(* is_process_read item.attrs *) +(* || is_process_write item.attrs *) +(* || is_process_init item.attrs *) + +(* module type Subprinter = sig *) +(* val print : AST.item list -> string *) +(* end *) module MkSubprinter (Section : sig val banner : string @@ -610,37 +610,38 @@ module DataTypes = MkSubprinter (struct List.filter ~f:(fun item -> [%matches? Type _] item.v) items let contents items = - let contents, _ = Print.items NoAuxInfo (filter_data_types items) in - contents + (* let contents, _ = Print.items NoAuxInfo (filter_data_types items) in *) + (* contents *) + failwith "x" end) module Letfuns = MkSubprinter (struct let banner = "Functions" let preamble items = "" - - let contents items = - let process_letfuns, pure_letfuns = - List.partition_tf ~f:is_process (filter_crate_functions items) - in - let pure_letfuns_print, _ = - Print.items (CrateFns (filter_crate_functions items)) pure_letfuns - in - let process_letfuns_print, _ = - Print.items (CrateFns (filter_crate_functions items)) process_letfuns - in - pure_letfuns_print ^ process_letfuns_print + let contents items = failwith "x" + (* let process_letfuns, pure_letfuns = *) + (* List.partition_tf ~f:is_process (filter_crate_functions items) *) + (* in *) + (* let pure_letfuns_print, _ = *) + (* Print.items (CrateFns (filter_crate_functions items)) pure_letfuns *) + (* in *) + (* let process_letfuns_print, _ = *) + (* Print.items (CrateFns (filter_crate_functions items)) process_letfuns *) + (* in *) + (* pure_letfuns_print ^ process_letfuns_print *) end) module Processes = MkSubprinter (struct let banner = "Processes" let preamble items = "" - let process_filter item = [%matches? Fn _] item.v && is_process item - - let contents items = - let contents, _ = - Print.items NoAuxInfo (List.filter ~f:process_filter items) - in - contents + let process_filter item = failwith "x" + (* [%matches? Fn _] item.v && is_process item *) + + let contents items = failwith "x" + (* let contents, _ = *) + (* Print.items NoAuxInfo (List.filter ~f:process_filter items) *) + (* in *) + (* contents *) end) module Toplevel = MkSubprinter (struct @@ -656,9 +657,12 @@ let translate m (bo : BackendOptions.t) (items : AST.item list) : ^ Processes.print items in let analysis_contents = Toplevel.print items in - let lib_file = Types.{ path = "lib.pvl"; contents = lib_contents } in + let lib_file = + Types.{ path = "lib.pvl"; contents = lib_contents; sourcemap = None } + in let analysis_file = - Types.{ path = "analysis.pv"; contents = analysis_contents } + Types. + { path = "analysis.pv"; contents = analysis_contents; sourcemap = None } in [ lib_file; analysis_file ] diff --git a/engine/default.nix b/engine/default.nix index a9d6c7b3b..c54c1f5af 100644 --- a/engine/default.nix +++ b/engine/default.nix @@ -10,6 +10,7 @@ gnused, lib, removeReferencesTo, + ocaml-sourcemaps, }: let non_empty_list = ocamlPackages.buildDunePackage rec { pname = "non_empty_list"; @@ -67,6 +68,7 @@ re js_of_ocaml ocamlgraph + ocaml-sourcemaps ] ++ # F* dependencies diff --git a/engine/lib/dune b/engine/lib/dune index a6b068a3e..8b4763d6c 100644 --- a/engine/lib/dune +++ b/engine/lib/dune @@ -12,6 +12,7 @@ core logs re + sourcemaps ocamlgraph) (preprocessor_deps ; `ppx_inline` is used on the `Subtype` module, thus we need it at PPX time diff --git a/engine/lib/generic_printer/generic_printer.ml b/engine/lib/generic_printer/generic_printer.ml deleted file mode 100644 index 0c8ff1d65..000000000 --- a/engine/lib/generic_printer/generic_printer.ml +++ /dev/null @@ -1,436 +0,0 @@ -open! Prelude -open! Ast - -module Make (F : Features.T) (View : Concrete_ident.VIEW_API) = struct - open Generic_printer_base - open Generic_printer_base.Make (F) - - module Class = struct - module U = Ast_utils.Make (F) - open! AST - open PPrint - - let iblock f = group >> jump 2 0 >> terminate (break 0) >> f >> group - - class print = - object (print) - inherit print_base as super - method printer_name = "Generic" - - method par_state : ast_position -> par_state = - function - | Lhs_LhsArrayAccessor | Ty_Tuple | Ty_TSlice | Ty_TArray_length - | Expr_If_cond | Expr_If_then | Expr_If_else | Expr_Array - | Expr_Assign | Expr_Closure_param | Expr_Closure_body - | Expr_Ascription_e | Expr_Let_lhs | Expr_Let_rhs | Expr_Let_body - | Expr_App_arg | Expr_ConstructTuple | Pat_ConstructTuple | Pat_PArray - | Pat_Ascription_pat | Param_pat | Item_Fn_body | GenericParam_GPConst - -> - AlreadyPar - | _ -> NeedsPar - - method namespace_of_concrete_ident - : concrete_ident -> string * string list = - fun i -> View.to_namespace i - - method concrete_ident' ~(under_current_ns : bool) : concrete_ident fn = - fun id -> - let id = View.to_view id in - let chunks = - if under_current_ns then [ id.definition ] - else id.crate :: (id.path @ [ id.definition ]) - in - separate_map (colon ^^ colon) utf8string chunks - - method name_of_concrete_ident : concrete_ident fn = - View.to_definition_name >> utf8string - - method mutability : 'a. 'a mutability fn = fun _ -> empty - - method primitive_ident : primitive_ident fn = - function - | Deref -> string "deref" - | Cast -> string "cast" - | LogicalOp And -> string "and" - | LogicalOp Or -> string "or" - - method local_ident : local_ident fn = View.local_ident >> utf8string - - method literal : literal_ctx -> literal fn = - (* TODO : escape *) - fun _ctx -> function - | String s -> utf8string s |> dquotes - | Char c -> char c |> bquotes - | Int { value; negative; _ } -> - string value |> precede (if negative then minus else empty) - | Float { value; kind; negative } -> - string value - |> precede (if negative then minus else empty) - |> terminate - (string (match kind with F32 -> "f32" | F64 -> "f64")) - | Bool b -> OCaml.bool b - - method generic_value : generic_value fn = - function - | GLifetime _ -> string "Lifetime" - | GType ty -> print#ty_at GenericValue_GType ty - | GConst expr -> print#expr_at GenericValue_GConst expr - - method lhs : lhs fn = - function - | LhsLocalVar { var; _ } -> print#local_ident var - | LhsArbitraryExpr { e; _ } -> print#expr_at Lhs_LhsArbitraryExpr e - | LhsFieldAccessor { e; field; _ } -> - print#lhs e |> parens - |> terminate (dot ^^ print#global_ident_projector field) - | LhsArrayAccessor { e; index; _ } -> - print#lhs e |> parens - |> terminate (print#expr_at Lhs_LhsArrayAccessor index |> brackets) - - method ty_bool : document = string "bool" - method ty_char : document = string "char" - method ty_str : document = string "str" - - method ty_int : int_kind fn = - fun { size; signedness } -> - let signedness = match signedness with Signed -> "i" | _ -> "u" in - let size = - match int_of_size size with - | Some n -> OCaml.int n - | None -> string "size" - in - string signedness ^^ size - - method ty_float : float_kind fn = - (function F32 -> "f32" | F64 -> "f64") >> string - - method generic_values : generic_value list fn = - function - | [] -> empty - | values -> separate_map comma print#generic_value values |> angles - - method ty_app : concrete_ident -> generic_value list fn = - fun f args -> print#concrete_ident f ^^ print#generic_values args - - method ty_tuple : int -> ty list fn = - fun _n -> - separate_map (comma ^^ break 1) (print#ty_at Ty_Tuple) - >> iblock parens - - method! ty : par_state -> ty fn = - fun ctx ty -> - match ty with - | TBool -> string "bool" - | TChar -> string "char" - | TInt kind -> print#ty_int kind - | TFloat kind -> print#ty_float kind - | TStr -> string "String" - | TArrow (inputs, output) -> - separate_map (string "->") (print#ty_at Ty_TArrow) - (inputs @ [ output ]) - |> parens - |> precede (string "arrow!") - | TRef { typ; mut; _ } -> - ampersand ^^ print#mutability mut ^^ print#ty_at Ty_TRef typ - | TParam i -> print#local_ident i - | TSlice { ty; _ } -> print#ty_at Ty_TSlice ty |> brackets - | TRawPointer _ -> string "raw_pointer!()" - | TArray { typ; length } -> - print#ty_at Ty_TArray_length typ - ^/^ semi - ^/^ print#expr_at Ty_TArray_length length - |> brackets - | TAssociatedType _ -> string "assoc_type!()" - | TOpaque _ -> string "opaque_type!()" - | TApp _ -> super#ty ctx ty - - method! expr' : par_state -> expr' fn = - fun ctx e -> - let wrap_parens = - group - >> - match ctx with AlreadyPar -> Fn.id | NeedsPar -> iblock braces - in - match e with - | If { cond; then_; else_ } -> - let if_then = - (string "if" ^//^ nest 2 (print#expr_at Expr_If_cond cond)) - ^/^ string "then" - ^//^ (print#expr_at Expr_If_then then_ |> braces |> nest 1) - in - (match else_ with - | None -> if_then - | Some else_ -> - if_then ^^ break 1 ^^ string "else" ^^ space - ^^ (print#expr_at Expr_If_else else_ |> iblock braces)) - |> wrap_parens - | Match { scrutinee; arms } -> - let header = - string "match" ^^ space - ^^ (print#expr_at Expr_Match_scrutinee scrutinee - |> terminate space |> iblock Fn.id) - |> group - in - let arms = - separate_map hardline - (print#arm >> group >> nest 2 - >> precede (bar ^^ space) - >> group) - arms - in - header ^^ iblock braces arms - | Let { monadic; lhs; rhs; body } -> - (Option.map - ~f:(fun monad -> print#expr_monadic_let ~monad) - monadic - |> Option.value ~default:print#expr_let) - ~lhs ~rhs body - |> wrap_parens - | Literal l -> print#literal Expr l - | Block (e, _) -> print#expr ctx e - | Array l -> - separate_map comma (print#expr_at Expr_Array) l - |> group |> brackets - | LocalVar i -> print#local_ident i - | GlobalVar (`Concrete i) -> print#concrete_ident i - | GlobalVar (`Primitive p) -> print#primitive_ident p - | GlobalVar (`TupleCons 0) -> print#expr_construct_tuple [] - | GlobalVar - (`TupleType _ | `TupleField _ | `Projector _ | `TupleCons _) -> - print#assertion_failure "GlobalVar" - | Assign { lhs; e; _ } -> - group (print#lhs lhs) - ^^ space ^^ equals - ^/^ group (print#expr_at Expr_Assign e) - ^^ semi - | Loop _ -> string "todo loop;" - | Break _ -> string "todo break;" - | Return _ -> string "todo return;" - | Continue _ -> string "todo continue;" - | QuestionMark { e; _ } -> - print#expr_at Expr_QuestionMark e |> terminate qmark - | Borrow { kind; e; _ } -> - string (match kind with Mut _ -> "&mut " | _ -> "&") - ^^ print#expr_at Expr_Borrow e - | AddressOf _ -> string "todo address of;" - | Closure { params; body; _ } -> - separate_map comma (print#pat_at Expr_Closure_param) params - |> group |> enclose bar bar - |> terminate (print#expr_at Expr_Closure_body body |> group) - |> wrap_parens - | Ascription { e; typ } -> - print#expr_at Expr_Ascription_e e - ^^ string "as" - ^/^ print#ty_at Expr_Ascription_typ typ - |> wrap_parens - | MacroInvokation _ -> print#assertion_failure "MacroInvokation" - | EffectAction _ -> print#assertion_failure "EffectAction" - | App _ | Construct _ -> super#expr' ctx e - - method expr_monadic_let - : monad:supported_monads * F.monadic_binding -> - lhs:pat -> - rhs:expr -> - expr fn = - fun ~monad:_ ~lhs ~rhs body -> print#expr_let ~lhs ~rhs body - - method expr_let : lhs:pat -> rhs:expr -> expr fn = - fun ~lhs ~rhs body -> - string "let" - ^/^ iblock Fn.id (print#pat_at Expr_Let_lhs lhs) - ^/^ equals - ^/^ iblock Fn.id (print#expr_at Expr_Let_rhs rhs) - ^^ semi - ^/^ (print#expr_at Expr_Let_body body |> group) - - method tuple_projection : size:int -> nth:int -> expr fn = - fun ~size:_ ~nth e -> - print#expr_at Expr_TupleProjection e - |> terminate (dot ^^ OCaml.int nth) - - method field_projection : concrete_ident -> expr fn = - fun i e -> - print#expr_at Expr_FieldProjection e - |> terminate (dot ^^ print#name_of_concrete_ident i) - - method expr_app : expr -> expr list -> generic_value list fn = - fun f args _generic_args -> - let args = - separate_map - (comma ^^ break 1) - (print#expr_at Expr_App_arg >> group) - args - in - let f = print#expr_at Expr_App_f f |> group in - f ^^ iblock parens args - - method doc_construct_tuple : document list fn = - separate (comma ^^ break 1) >> iblock parens - - method expr_construct_tuple : expr list fn = - List.map ~f:(print#expr_at Expr_ConstructTuple) - >> print#doc_construct_tuple - - method pat_construct_tuple : pat list fn = - List.map ~f:(print#pat_at Pat_ConstructTuple) - >> print#doc_construct_tuple - - method global_ident_projector : global_ident fn = - function - | `Projector (`Concrete i) | `Concrete i -> print#concrete_ident i - | _ -> - print#assertion_failure "global_ident_projector: not a projector" - - method doc_construct_inductive - : is_record:bool -> - is_struct:bool -> - constructor:concrete_ident -> - base:document option -> - (global_ident * document) list fn = - fun ~is_record ~is_struct:_ ~constructor ~base:_ args -> - if is_record then - print#concrete_ident constructor - ^^ space - ^^ iblock parens - (separate_map (break 0) - (fun (field, body) -> - (print#global_ident_projector field - |> terminate comma |> group) - ^^ colon ^^ space ^^ iblock Fn.id body) - args) - else - print#concrete_ident constructor - ^^ space - ^^ iblock parens (separate_map (break 0) snd args) - - method expr_construct_inductive - : is_record:bool -> - is_struct:bool -> - constructor:concrete_ident -> - base:(expr * F.construct_base) option -> - (global_ident * expr) list fn = - fun ~is_record ~is_struct ~constructor ~base -> - let base = - Option.map - ~f:(fst >> print#expr_at Expr_ConcreteInductive_base) - base - in - List.map ~f:(print#expr_at Expr_ConcreteInductive_field |> map_snd) - >> print#doc_construct_inductive ~is_record ~is_struct ~constructor - ~base - - method attr : attr fn = fun _ -> empty - - method! pat' : par_state -> pat' fn = - fun ctx -> - let wrap_parens = - group - >> - match ctx with AlreadyPar -> Fn.id | NeedsPar -> iblock braces - in - function - | PWild -> underscore - | PAscription { typ; typ_span; pat } -> - print#pat_ascription ~typ ~typ_span pat |> wrap_parens - | PBinding { mut; mode; var; typ = _; subpat } -> ( - let p = - (match mode with ByRef _ -> string "&" | _ -> empty) - ^^ (match mut with Mutable _ -> string "mut " | _ -> empty) - ^^ print#local_ident var - in - match subpat with - | Some (subpat, _) -> - p ^^ space ^^ at ^^ space - ^^ print#pat_at Pat_PBinding_subpat subpat - |> wrap_parens - | None -> p) - | PArray { args } -> - separate_map (break 0) - (print#pat_at Pat_PArray >> terminate comma >> group) - args - |> iblock brackets - | PDeref { subpat; _ } -> - ampersand ^^ print#pat_at Pat_PDeref subpat - | (PConstruct _ | PConstant _) as pat -> super#pat' ctx pat - | POr { subpats } -> - separate_map (bar ^^ break 1) (print#pat_at Pat_Or) subpats - - method pat_ascription : typ:ty -> typ_span:span -> pat fn = - fun ~typ ~typ_span pat -> - print#pat_at Pat_Ascription_pat pat - ^^ colon - ^^ print#with_span ~span:typ_span (fun () -> - print#ty_at Pat_Ascription_typ typ) - - method expr_unwrapped : par_state -> expr fn = - fun ctx { e; _ } -> print#expr' ctx e - - method param : param fn = - fun { pat; typ; typ_span; attrs } -> - let typ = - match typ_span with - | Some span -> - print#with_span ~span (fun _ -> print#ty_at Param_typ typ) - | None -> print#ty_at Param_typ typ - in - print#attrs attrs ^^ print#pat_at Param_pat pat ^^ space ^^ colon - ^^ space ^^ typ - - method item' : item' fn = - function - | Fn { name; generics; body; params } -> - let params = - iblock parens - (separate_map (comma ^^ break 1) print#param params) - in - let generics = print#generic_params generics.params in - string "fn" ^^ space ^^ print#concrete_ident name ^^ generics - ^^ params - ^^ iblock braces (print#expr_at Item_Fn_body body) - | _ -> string "item not implemented" - - method generic_param' : generic_param fn = - fun { ident; attrs; kind; _ } -> - let suffix = - match kind with - | GPLifetime _ -> space ^^ colon ^^ space ^^ string "'unk" - | GPType { default = None } -> empty - | GPType { default = Some default } -> - space ^^ equals ^^ space - ^^ print#ty_at GenericParam_GPType default - | GPConst { typ } -> - space ^^ colon ^^ space - ^^ print#ty_at GenericParam_GPConst typ - in - let prefix = - match kind with - | GPConst _ -> string "const" ^^ space - | _ -> empty - in - let ident = - let name = - if String.(ident.name = "_") then "Anonymous" else ident.name - in - { ident with name } - in - prefix ^^ print#attrs attrs ^^ print#local_ident ident ^^ suffix - - method generic_params : generic_param list fn = - separate_map comma print#generic_param >> group >> angles - - method arm' : arm' fn = - fun { arm_pat; body } -> - let pat = print#pat_at Arm_pat arm_pat |> group in - let body = print#expr_at Arm_body body in - pat ^^ string " => " ^^ body ^^ comma - end - end - - include Class - - include Api (struct - type aux_info = unit - - let new_print () = (new Class.print :> print_object) - end) -end diff --git a/engine/lib/generic_printer/generic_printer.mli b/engine/lib/generic_printer/generic_printer.mli deleted file mode 100644 index ccd471cc3..000000000 --- a/engine/lib/generic_printer/generic_printer.mli +++ /dev/null @@ -1,6 +0,0 @@ -module Make (F : Features.T) (View : Concrete_ident.VIEW_API) : sig - open Generic_printer_base.Make(F) - include API - - class print : print_class -end diff --git a/engine/lib/generic_printer/generic_printer_api.ml b/engine/lib/generic_printer/generic_printer_api.ml new file mode 100644 index 000000000..8e914e8cc --- /dev/null +++ b/engine/lib/generic_printer/generic_printer_api.ml @@ -0,0 +1,89 @@ +open! Prelude +open Generic_printer_base + +module AnnotatedString = struct + type t = string * Annotation.t list [@@deriving show, yojson, eq] + + let to_string = fst + + let to_sourcemap : t -> Types.source_map = + snd >> List.filter_map ~f:Annotation.to_mapping >> Sourcemaps.Source_maps.mk + >> fun ({ + mappings; + sourceRoot; + sources; + sourcesContent; + names; + version; + file; + } : + Sourcemaps.Source_maps.t) -> + Types. + { mappings; sourceRoot; sources; sourcesContent; names; version; file } +end + +module Make (F : Features.T) = struct + module AST = Ast.Make (F) + open Ast.Make (F) + open SecretTypes + + type print_object = + < printer_name : string + ; get_span_data : unit -> Annotation.t list + ; ty : (par_state -> ty fn) no_override + ; pat : (par_state -> pat fn) no_override + ; arm : arm fn no_override + ; expr : (par_state -> expr fn) no_override + ; item : item fn no_override + ; items : item list fn > + (** In the end, an printer *object* should be of the type {!print_object}. *) + + module type API = sig + type aux_info + + val items : aux_info -> item list -> AnnotatedString.t + val item : aux_info -> item -> AnnotatedString.t + val expr : aux_info -> expr -> AnnotatedString.t + val pat : aux_info -> pat -> AnnotatedString.t + val ty : aux_info -> ty -> AnnotatedString.t + end + + module Api (NewPrint : sig + type aux_info + + val new_print : aux_info -> print_object + end) = + struct + open NewPrint + + let mk' (f : print_object -> 'a -> PPrint.document) (aux : aux_info) + (x : 'a) : AnnotatedString.t = + let printer = new_print aux in + let doc = f printer x in + let buf = Buffer.create 0 in + PPrint.ToBuffer.pretty 1.0 80 buf doc; + (Buffer.contents buf, printer#get_span_data ()) + + let mk (f : print_object -> 'a fn no_override) = + mk' (fun (po : print_object) -> + let f : 'a fn no_override = f po in + let f = !:f in + f) + + type aux_info = NewPrint.aux_info + + let items : aux_info -> item list -> AnnotatedString.t = + mk' (fun p -> p#items) + + let item : aux_info -> item -> AnnotatedString.t = mk (fun p -> p#item) + + let expr : aux_info -> expr -> AnnotatedString.t = + mk' (fun p -> !:(p#expr) AlreadyPar) + + let pat : aux_info -> pat -> AnnotatedString.t = + mk' (fun p -> !:(p#pat) AlreadyPar) + + let ty : aux_info -> ty -> AnnotatedString.t = + mk' (fun p -> !:(p#ty) AlreadyPar) + end +end diff --git a/engine/lib/generic_printer/generic_printer_base.ml b/engine/lib/generic_printer/generic_printer_base.ml index 164442ec8..09a694a95 100644 --- a/engine/lib/generic_printer/generic_printer_base.ml +++ b/engine/lib/generic_printer/generic_printer_base.ml @@ -2,92 +2,29 @@ open! Prelude open! Ast open PPrint -(** Generic printer for the {!module:Ast} ASTs. It uses the [PPrint] -library, and additionaly computes {!Annotation.t}. *) - -(** Identifies a position in the AST. This is useful for figuring out -wether we should wrap a chunk of AST in parenthesis. or not *) -type ast_position = - | GenericValue_GType - | GenericValue_GConst - | Lhs_LhsArbitraryExpr - | Lhs_LhsArrayAccessor - | Ty_TArrow - | Ty_TRef - | Ty_Tuple - | Ty_TSlice - | Ty_TArray_typ - | Ty_TArray_length - | Expr_If_cond - | Expr_If_then - | Expr_If_else - | Expr_Array - | Expr_Assign - | Expr_Closure_param - | Expr_Closure_body - | Expr_Ascription_e - | Expr_Ascription_typ - | Expr_Let_lhs - | Expr_Let_rhs - | Expr_Let_body - | Expr_Match_scrutinee - | Expr_QuestionMark - | Expr_Borrow - | Expr_TupleProjection - | Expr_ConstructTuple - | Expr_FieldProjection - | Expr_App_f - | Expr_App_arg - | Expr_ConcreteInductive_base - | Expr_ConcreteInductive_field - | Pat_PBinding_subpat - | Pat_PDeref - | Pat_PArray - | Pat_ConstructTuple - | Pat_ConcreteInductive - | Pat_Ascription_pat - | Pat_Ascription_typ - | Pat_Or - | Param_pat - | Param_typ - | GenericParam_GPType - | GenericParam_GPConst - | Arm_pat - | Arm_body - | Item_Fn_body -[@@warning "-37"] - -module Annotation = struct - type loc = { line : int; col : int } [@@deriving show, yojson, eq] - type t = loc * span [@@deriving show, yojson, eq] +module SecretTypes = struct + type 't no_override = 't + type 'location no_direct_call = unit end -type annot_str = string * Annotation.t list [@@deriving show, yojson, eq] - -(** When printing a chunk of AST, should we wrap parenthesis -({!NeedsPar}) or not ({!AlreadyPar})? *) -type par_state = NeedsPar | AlreadyPar +let ( !: ) (type a) (f : a SecretTypes.no_override) : a = f -type literal_ctx = Pat | Expr +include Generic_printer_base_sig.Types module Make (F : Features.T) = struct module AST = Ast.Make (F) module U = Ast_utils.Make (F) open Ast.Make (F) + open Generic_printer_base_sig.Make (F) (SecretTypes) - type 't fn = 't -> document - - (** Raw generic printers base class. Those are useful for building a - printer, not for consuming printers. Consumers should use - the {!module:Api} functor. *) - class virtual print_base = + class virtual base : print_base_type = object (print) val mutable current_span = Span.default val mutable span_data : Annotation.t list = [] val mutable current_namespace : (string * string list) option = None method get_span_data () = span_data - method with_span ~span f = + method with_span ~(span : span) (f : unit -> document) : document = let prev_span = current_span in current_span <- span; let doc = f () |> print#spanned_doc |> custom in @@ -108,14 +45,126 @@ module Make (F : Features.T) = struct method compact : output -> unit = fun o -> compact o doc end - method concrete_ident : concrete_ident fn = - fun id -> - let current_ns = print#get_current_namespace () in - let id_ns = print#namespace_of_concrete_ident id in - print#concrete_ident' - ~under_current_ns: - ([%equal: (string * string list) option] current_ns (Some id_ns)) - id + method expr_at = print#par_state >> print#expr + method ty_at = print#par_state >> print#ty + method pat_at = print#par_state >> print#pat + + method expr ctx (e : expr) = + let span = e.span in + print#with_span ~span (fun _ -> + try print#__expr ctx e + with Diagnostics.SpanFreeError.Exn (Data (context, kind)) -> + U.hax_failure_expr 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) + + method ty ctx full = + match full with + | TApp { ident = `Concrete ident; args } -> + print#ty_TApp_application ~full ident args |> group + | TApp + { + ident = `Primitive _ | `TupleCons _ | `TupleField _ | `Projector _; + _; + } -> + print#assertion_failure "TApp not concrete" + | TApp { ident = `TupleType size; args } -> + let args = + List.filter_map ~f:(function GType t -> Some t | _ -> None) args + in + if [%equal: int] (List.length args) size |> not then + print#assertion_failure "malformed [ty.TApp] tuple"; + print#ty_TApp_tuple ~full args + | TApp _ -> . + | _ -> print#ty_ () ctx full + + method pat ctx (full : pat) = + print#with_span ~span:full.span (fun _ -> print#pat_ () ctx full) + + method item i = + print#set_current_namespace + (print#namespace_of_concrete_ident i.ident |> Option.some); + print#with_span ~span:i.span (fun _ -> + try print#item_ () i + with Diagnostics.SpanFreeError.Exn (Data (context, kind)) -> + let error = Diagnostics.pretty_print_context_kind context kind in + let cast_item : item -> Ast.Full.item = Stdlib.Obj.magic in + let ast = cast_item i |> Print_rust.pitem_str in + let msg = + error ^ "\nLast available AST for this item:\n\n" ^ ast + in + (* TODO: if the printer is extremely broken, this results in a stack overflow *) + make_hax_error_item i.span i.ident msg |> print#item) + + method private __expr ctx full = + match full.e with + | App { f = { e = GlobalVar i; _ } as f; args; generic_args; impl = _ } + -> ( + let expect_one_arg where = + match args with + | [ arg ] -> arg + | _ -> print#assertion_failure @@ "Expected one arg at " ^ where + in + match i with + | `Concrete _ | `Primitive _ -> ( + match (args, i) with + | [], `Concrete i -> + print#expr_App_constant ~full i generic_args + | [], _ -> print#assertion_failure "Primitive app of arity 0" + | _ -> print#expr_App_application ~full f args generic_args) + | `TupleType _ | `TupleCons _ | `TupleField _ -> + print#assertion_failure "App: unexpected tuple" + | `Projector (`TupleField (nth, size)) -> + let arg = expect_one_arg "projector tuple field" in + print#expr_App_tuple_projection ~full ~size ~nth arg + | `Projector (`Concrete i) -> + let arg = expect_one_arg "projector concrete" in + print#expr_App_field_projection ~full i arg) + | App { f; args; generic_args; _ } -> + print#expr_App_application ~full f args generic_args + | Construct { constructor; fields; base; is_record; is_struct } -> ( + match constructor with + | `Concrete constructor -> + print#expr_Construct_inductive ~full ~is_record ~is_struct + ~constructor ~base fields + | `TupleCons _ -> + List.map ~f:snd fields |> print#expr_Construct_tuple ~full + | `Primitive _ | `TupleType _ | `TupleField _ | `Projector _ -> + print#assertion_failure "Construct unexpected constructors") + | App _ | Construct _ -> . + | _ -> print#expr_ () ctx full + + method arm (full : arm) = + print#with_span ~span:full.span (fun _ -> print#arm_ () full) + + method generic_param (full : generic_param) = + print#with_span ~span:full.span (fun _ -> print#generic_param_ () full) + + method param_ty (full : param) = + match full.typ_span with + | Some span -> print#with_span ~span (fun _ -> print#param_ty_ () full) + | None -> print#param_ty_ () full + + method impl_item (full : impl_item) = + print#with_span ~span:full.ii_span (fun _ -> print#impl_item_ () full) + + method trait_item (full : trait_item) = + print#with_span ~span:full.ti_span (fun _ -> print#trait_item_ () full) + + method attr (full : attr) = + print#with_span ~span:full.span (fun _ -> print#attr_ () full) + + method concrete_ident id = + let current_ns = print#get_current_namespace () in + let id_ns = print#namespace_of_concrete_ident id in + print#concrete_ident_ () + ~under_current_ns: + ([%equal: (string * string list) option] current_ns (Some id_ns)) + id + + method items = separate_map (twice hardline) print#item + method attrs = separate_map hardline print#attr method assertion_failure : 'any. string -> 'any = fun details -> @@ -126,257 +175,6 @@ module Make (F : Features.T) = struct method set_current_namespace ns = current_namespace <- ns method get_current_namespace () = current_namespace - - (* `*_at` variants *) - method expr_at : ast_position -> expr fn = print#par_state >> print#expr - method ty_at : ast_position -> ty fn = print#par_state >> print#ty - method pat_at : ast_position -> pat fn = print#par_state >> print#pat - - method pat : par_state -> pat fn = - fun ctx { p; span; _ } -> - print#with_span ~span (fun _ -> print#pat' ctx p) - - method item_unwrapped : item fn = fun { v; _ } -> print#item' v - - method generic_param : generic_param fn = - fun ({ span; _ } as p) -> - print#with_span ~span (fun _ -> print#generic_param' p) - - method arm : arm fn = - fun { arm; span } -> print#with_span ~span (fun _ -> print#arm' arm) - - method ty : par_state -> ty fn = - fun _ctx ty -> - match ty with - | TApp { ident = `Concrete ident; args } -> - print#ty_app ident args |> group - | TApp - { - ident = - `Primitive _ | `TupleCons _ | `TupleField _ | `Projector _; - _; - } -> - print#assertion_failure "TApp not concrete" - | TApp { ident = `TupleType n; args } -> - let args = - List.filter_map - ~f:(function GType t -> Some t | _ -> None) - args - in - if [%equal: int] (List.length args) n |> not then - print#assertion_failure "malformed ty app tuple"; - print#ty_tuple n args - | TApp _ -> . - | _ -> - print#assertion_failure "default ty is only implemented for TApp" - - method expr' : par_state -> expr' fn = - fun _ctx e -> - match e with - | App - { f = { e = GlobalVar i; _ } as f; args; generic_args; impl = _ } - -> ( - let expect_one_arg where = - match args with - | [ arg ] -> arg - | _ -> print#assertion_failure @@ "Expected one arg at " ^ where - in - match i with - | `Concrete _ | `Primitive _ -> print#expr_app f args generic_args - | `TupleType _ | `TupleCons _ | `TupleField _ -> - print#assertion_failure "App: unexpected tuple" - | `Projector (`TupleField (nth, size)) -> - let arg = expect_one_arg "projector tuple field" in - print#tuple_projection ~size ~nth arg - | `Projector (`Concrete i) -> - let arg = expect_one_arg "projector concrete" in - print#field_projection i arg) - | App { f; args; generic_args; _ } -> - print#expr_app f args generic_args - | Construct { constructor; fields; base; is_record; is_struct } -> ( - match constructor with - | `Concrete constructor -> - print#expr_construct_inductive ~is_record ~is_struct - ~constructor ~base fields - | `TupleCons _ -> - List.map ~f:snd fields |> print#expr_construct_tuple - | `Primitive _ | `TupleType _ | `TupleField _ | `Projector _ -> - print#assertion_failure "Construct unexpected constructors") - | App _ | Construct _ -> . - | _ -> - print#assertion_failure - "default expr' is only implemented for App and Construct" - - method pat' : par_state -> pat' fn = - fun _ -> function - | PConstant { lit } -> print#literal Pat lit - | PConstruct { name; args; is_record; is_struct } -> ( - match name with - | `Concrete constructor -> - print#doc_construct_inductive ~is_record ~is_struct - ~constructor ~base:None - (List.map - ~f:(fun fp -> - (fp.field, print#pat_at Pat_ConcreteInductive fp.pat)) - args) - | `TupleCons _ -> - List.map ~f:(fun fp -> fp.pat) args - |> print#pat_construct_tuple - | `Primitive _ | `TupleType _ | `TupleField _ | `Projector _ -> - print#assertion_failure "todo err") - | _ -> - print#assertion_failure - "default pat' is only implemented for PConstant and PConstruct" - - method expr : par_state -> expr fn = - fun ctx e -> - let span = e.span in - 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.LiftToFullAst.expr e) - (* TODO: if the printer is extremely broken, this results in a stack overflow *) - |> print#expr ctx) - - method item : item fn = - fun i -> - print#set_current_namespace - (print#namespace_of_concrete_ident i.ident |> Option.some); - try print#item_unwrapped i - with Diagnostics.SpanFreeError.Exn (Data (context, kind)) -> - let error = Diagnostics.pretty_print_context_kind context kind in - let cast_item : item -> Ast.Full.item = Stdlib.Obj.magic in - let ast = cast_item i |> Print_rust.pitem_str in - let msg = error ^ "\nLast available AST for this item:\n\n" ^ ast in - (* TODO: if the printer is extremely broken, this results in a stack overflow *) - make_hax_error_item i.span i.ident msg |> print#item - - method items : item list fn = separate_map (twice hardline) print#item - method attrs : attrs fn = separate_map hardline print#attr + method unreachable : 'any. unit -> 'any = fun _ -> failwith "x" end - - type print_object = - < printer_name : string - ; get_span_data : unit -> Annotation.t list - ; ty : par_state -> ty fn - ; pat : par_state -> pat fn - ; arm : arm fn - ; expr : par_state -> expr fn - ; item : item fn - ; items : item list fn > - (** In the end, an printer *object* should be of the type {!print_object}. *) - - class type print_class = - object - inherit print_base - method printer_name : string - method get_span_data : unit -> Annotation.t list - - method namespace_of_concrete_ident : - concrete_ident -> string * string list - - method par_state : ast_position -> par_state - method concrete_ident' : under_current_ns:bool -> concrete_ident fn - method concrete_ident : concrete_ident fn - method name_of_concrete_ident : concrete_ident fn - method mutability : 'a. 'a mutability fn - method primitive_ident : primitive_ident fn - method local_ident : local_ident fn - method literal : literal_ctx -> literal fn - method generic_value : generic_value fn - method lhs : lhs fn - method ty_bool : document - method ty_char : document - method ty_str : document - method ty_int : int_kind fn - method ty_float : float_kind fn - method generic_values : generic_value list fn - method ty_app : concrete_ident -> generic_value list fn - method ty_tuple : int -> ty list fn - method ty : par_state -> ty fn - method expr' : par_state -> expr' fn - - method expr_monadic_let : - monad:supported_monads * F.monadic_binding -> - lhs:pat -> - rhs:expr -> - expr fn - - method expr_let : lhs:pat -> rhs:expr -> expr fn - method tuple_projection : size:int -> nth:int -> expr fn - method field_projection : concrete_ident -> expr fn - method expr_app : expr -> expr list -> generic_value list fn - method doc_construct_tuple : document list fn - method expr_construct_tuple : expr list fn - method pat_construct_tuple : pat list fn - method global_ident_projector : global_ident fn - - method doc_construct_inductive : - is_record:bool -> - is_struct:bool -> - constructor:concrete_ident -> - base:document option -> - (global_ident * document) list fn - - method expr_construct_inductive : - is_record:bool -> - is_struct:bool -> - constructor:concrete_ident -> - base:(expr * F.construct_base) option -> - (global_ident * expr) list fn - - method attr : attr fn - method attrs : attrs fn - method pat' : par_state -> pat' fn - method pat_ascription : typ:ty -> typ_span:span -> pat fn - method pat : par_state -> pat fn - method expr_unwrapped : par_state -> expr fn - method param : param fn - method item' : item' fn - method item_unwrapped : item fn - method generic_param' : generic_param fn - method generic_param : generic_param fn - method generic_params : generic_param list fn - method arm' : arm' fn - method arm : arm fn - method expr : par_state -> expr fn - method item : item fn - method items : item list fn - end - - module type API = sig - type aux_info - - val items : aux_info -> item list -> annot_str - val item : aux_info -> item -> annot_str - val expr : aux_info -> expr -> annot_str - val pat : aux_info -> pat -> annot_str - val ty : aux_info -> ty -> annot_str - end - - module Api (NewPrint : sig - type aux_info - - val new_print : aux_info -> print_object - end) = - struct - open NewPrint - - let mk (f : print_object -> 'a -> PPrint.document) (aux : aux_info) (x : 'a) - : annot_str = - let printer = new_print aux in - let doc = f printer x in - let buf = Buffer.create 0 in - PPrint.ToBuffer.pretty 1.0 80 buf doc; - (Buffer.contents buf, printer#get_span_data ()) - - type aux_info = NewPrint.aux_info - - let items : aux_info -> item list -> annot_str = mk (fun p -> p#items) - let item : aux_info -> item -> annot_str = mk (fun p -> p#item) - let expr : aux_info -> expr -> annot_str = mk (fun p -> p#expr AlreadyPar) - let pat : aux_info -> pat -> annot_str = mk (fun p -> p#pat AlreadyPar) - let ty : aux_info -> ty -> annot_str = mk (fun p -> p#ty AlreadyPar) - end end diff --git a/engine/lib/generic_printer/generic_printer_base.mli b/engine/lib/generic_printer/generic_printer_base.mli new file mode 100644 index 000000000..fb97d5f63 --- /dev/null +++ b/engine/lib/generic_printer/generic_printer_base.mli @@ -0,0 +1,23 @@ +open! Prelude +open! Ast + +include module type of struct + (** Protects some methods from being called or overrided. *) + module SecretTypes = struct + type 't no_override = private 't + (** Hello *) + + type 'location no_direct_call = private unit + (** Hello *) + end + + include Generic_printer_base_sig.Types +end + +val ( !: ) : 'a. 'a SecretTypes.no_override -> 'a + +module Make (F : Features.T) : sig + open Generic_printer_base_sig.Make(F)(SecretTypes) + + class virtual base : print_base_type +end diff --git a/engine/lib/generic_printer/generic_printer_base_sig.ml b/engine/lib/generic_printer/generic_printer_base_sig.ml new file mode 100644 index 000000000..2ffb68f4a --- /dev/null +++ b/engine/lib/generic_printer/generic_printer_base_sig.ml @@ -0,0 +1,348 @@ +[@@@warning "-37-34-27"] + +open! Prelude +open! Ast +open PPrint + +module Types = struct + (** Generic printer for the {!module:Ast} ASTs. It uses the [PPrint] +library, and additionaly computes {!Annotation.t}. *) + + (** Identifies a position in the AST. This is useful for figuring out +wether we should wrap a chunk of AST in parenthesis. or not *) + type ast_position = + | GenericValue_GType + | GenericValue_GConst + | Lhs_LhsArbitraryExpr + | Lhs_LhsArrayAccessor + | Ty_TArrow + | Ty_TRef + | Ty_Tuple + | Ty_TSlice + | Ty_TArray_typ + | Ty_TArray_length + | Expr_If_cond + | Expr_If_then + | Expr_If_else + | Expr_Array + | Expr_Assign + | Expr_Closure_param + | Expr_Closure_body + | Expr_Ascription_e + | Expr_Ascription_typ + | Expr_Let_lhs + | Expr_Let_rhs + | Expr_Let_body + | Expr_Match_scrutinee + | Expr_QuestionMark + | Expr_Borrow + | Expr_TupleProjection + | Expr_ConstructTuple + | Expr_FieldProjection + | Expr_App_f + | Expr_App_arg + | Expr_ConcreteInductive_base + | Expr_ConcreteInductive_field + | Pat_PBinding_subpat + | Pat_PDeref + | Pat_PArray + | Pat_ConstructTuple + | Pat_ConcreteInductive + | Pat_Ascription_pat + | Pat_Ascription_typ + | Pat_Or + | Param_pat + | Param_typ + | GenericParam_GPType + | GenericParam_GPConst + | Arm_pat + | Arm_body + | Item_Fn_body + [@@warning "-37"] + + module Annotation = struct + type loc = { line : int; col : int } [@@deriving show, yojson, eq] + type t = loc * span [@@deriving show, yojson, eq] + + let to_mapping ((loc, span) : t) : Sourcemaps.Source_maps.mapping option = + let real_path (x : Types.file_name) = + match x with + | Real (LocalPath p) | Real (Remapped { local_path = Some p; _ }) -> + Some p + | _ -> None + in + let loc_to_loc ({ line; col } : loc) : Sourcemaps.Location.t = + { line; col } + in + let to_loc ({ col; line } : Types.loc) : loc = + { col = Int.of_string col; line = Int.of_string line - 1 } + in + let* span = + Span.to_thir span + |> List.find ~f:(fun (s : Types.span) -> + real_path s.filename |> Option.is_some) + in + let* src_filename = real_path span.filename in + let src_start = to_loc span.lo |> loc_to_loc in + let src_end = to_loc span.hi |> loc_to_loc in + let dst_start = loc_to_loc loc in + Some + Sourcemaps.Source_maps. + { + src = { start = src_start; end_ = Some src_end }; + gen = { start = dst_start; end_ = None }; + source = src_filename; + name = None; + } + end + + type annot_str = string * Annotation.t list [@@deriving show, yojson, eq] + + (** When printing a chunk of AST, should we wrap parenthesis +({!NeedsPar}) or not ({!AlreadyPar})? *) + type par_state = NeedsPar | AlreadyPar + + type 't fn = 't -> document +end + +open Types + +module Make + (F : Features.T) (SecretTypes : sig + type 't no_override + type 'location no_direct_call + end) = +struct + module AST = Ast.Make (F) + module U = Ast_utils.Make (F) + open Ast.Make (F) + open SecretTypes + + (** Raw generic printers base class. Those are useful for building a + printer, not for consuming printers. Consumers should use + the {!module:Api} functor. *) + class type virtual print_base_type = + object + + (** {1 Span handling} *) + + (** Every piece of string rendered is contextualized with span information automatically. *) + + method get_span_data : unit -> Annotation.t list + (** Retreive the mapping between locations in the rendered + string and Rust locations. *) + + method with_span : span:span -> (unit -> document) -> document + (** [with_span ~span f] runs `f` in the context of [span]. *) + + method spanned_doc : document -> custom + (** [spanned_doc doc] constructs a custom wrapping document for + [doc]. Rendering this document in [pretty] mode has a + side-effect: we push a [Annotation.t] to internal state. An + annotation maps a location within the rendered string to a Rust + span (that is, a location in the original Rust source code). *) + + (** {1 [*_at] methods} *) + + (** Always use [_at] methods rather than [] + ones. The former takes an [ast_position], that contextualizes + from where we are printing something. Printing the body of a + [let .. = ..;] expression (position [Expr_Let_body]) and + printing a function argument (position [Expr_App_arg]) will + probably require different parenthesizing: [ast_position] gives + contextual information upon which such parenthesizing decisions + can be taken. *) + + method expr_at : ast_position -> expr fn + (** Renders an [expr] at some [ast_position]. *) + + method ty_at : ast_position -> ty fn + (** Renders a [ty] at some [ast_position]. *) + + method pat_at : ast_position -> pat fn + (** Renders a [pat] at some [ast_position]. *) + + (** {1 Driver methods} *) + + (** The methods in this section are defined in two flavors: + `` and `_`. `` methods are not + overridable. Indeed, they take care of various things for + you: + + {ul {- catch exceptions and translate them as + pretty-printed errors with the original Rust AST;} + {- set contextual span information in a systematic way;} + {- disambiguate certain variant of the AST (see {!section-"specialized-printers"}).}} + + Your can override `_` methods. + *) + + (** {2 Expressions} *) + method expr : (par_state -> expr fn) no_override + (** Prints an expression. Pre-handles the variants [App] and + [Construct]: see {!section-"specialize-expr"}. *) + + method virtual expr_ : [ `Expr ] no_direct_call -> par_state -> expr fn + (** Overridable printer for expressions. Please mark the cases + [App] and [Construct] as unreachable. *) + + (** {2 Types} *) + method ty : (par_state -> ty fn) no_override + (** Prints a type. Pre-handles [TApp]. *) + + method virtual ty_ : [ `Ty ] no_direct_call -> par_state -> ty fn + (** Overridable printer for types. Please mark the case [TApp] + as unreachable. *) + + (** {2 Patterns} *) + method pat : (par_state -> pat fn) no_override + (** Prints a pattern. *) + + method virtual pat_ : [ `Pat ] no_direct_call -> par_state -> pat fn + (** Overridable printer for patterns. *) + + (** {2 Items} *) + method item : item fn no_override + (** Prints a item. *) + + method virtual item_ : [ `Item ] no_direct_call -> item fn + (** Overridable printer for items. *) + + (** {2 Arms} *) + method arm : arm fn no_override + (** Prints an arm (in a match). *) + + method virtual arm_ : [ `Arm ] no_direct_call -> arm fn + (** Overridable printer for arms (in matches).*) + + (** {2 Generic parameters} *) + method generic_param : generic_param fn no_override + (** Prints a generic parameter. *) + + method virtual generic_param_ : [ `GP ] no_direct_call -> generic_param fn + (** Overridable printer for generic parameters. *) + + (** {2 Parameters} *) + method param_ty : param fn no_override + (** Prints the type of a parameter. This is special because of `typ_span`. *) + + method virtual param_ty_ : [ `Param ] no_direct_call -> param fn + (** Overridable printer for parameter types. *) + + (** {2 Impl items} *) + method impl_item : impl_item fn no_override + (** Prints an impl item. *) + + method virtual impl_item_ : [ `II ] no_direct_call -> impl_item fn + (** Overridable printer for impl items. *) + + (** {2 Trait items} *) + method trait_item : trait_item fn no_override + (** Prints an trait item. *) + + method virtual trait_item_ : [ `TI ] no_direct_call -> trait_item fn + (** Overridable printer for trait items. *) + + (** {2 Attributes} *) + + method attr : attr fn no_override + (** Prints an attribute. *) + + method virtual attr_ : [ `Attr ] no_direct_call -> attr fn + (** Overridable printer for attributes. *) + + (** {2 Concrete idents} *) + + method concrete_ident : concrete_ident fn no_override + (** Prints a concrete ident. *) + + method virtual concrete_ident_ : + [ `CIdent ] no_direct_call -> under_current_ns:bool -> concrete_ident fn + (** Overridable printer for concrete idents. *) + + (** {1:specialized-printers Specialized printers} *) + + (** Some nodes in the AST are ambiguous as they encode multiple + language constructs: the `App` constructor of `expr` for + instance encodes (1) function applications, (2) fields + projectors, (3) constants... This is the same for `Construct`, + `TApp`, and some other. + + This section defines specialized methods for those language + constructs. When the variant `` of a type `` in + the AST is encoding various language constructs, we defined + various methods named `__`. *) + + (** {2:specialize-expr Specialized printers for [expr]} *) + + method virtual expr_App_constant : + full:expr -> concrete_ident -> generic_value list fn + (** [expr_App_constant ~full e generics] prints the constant + [e] with generics [generics]. [full] is the unspecialized [expr]. *) + + method virtual expr_App_application : + full:expr -> expr -> expr list -> generic_value list fn + (** [expr_App_application ~full e args generics] prints the + function application [e<...generics>(...args)]. [full] is the unspecialized [expr]. *) + + method virtual expr_App_tuple_projection : + full:expr -> size:int -> nth:int -> expr fn + (** [expr_App_tuple_projection ~full ~size ~nth expr] prints + the projection of the [nth] component of the tuple [expr] of + size [size]. [full] is the unspecialized [expr]. *) + + method virtual expr_App_field_projection : + full:expr -> concrete_ident -> expr fn + (** [expr_App_field_projection ~full field expr] prints the + projection of the field [field] in the expression [expr]. [full] + is the unspecialized [expr]. *) + + method virtual expr_Construct_inductive : + full:expr -> + is_record:bool -> + is_struct:bool -> + constructor:concrete_ident -> + base:(expr * F.construct_base) option -> + (global_ident * expr) list fn + (** [expr_Construct_inductive ~full ~is_record ~is_struct + ~constructor ~base fields] prints the construction of an + inductive with base [base] and fields [fields]. [full] is the + unspecialized [expr]. TODO doc is_record is_struct *) + + method virtual expr_Construct_tuple : full:expr -> expr list fn + + (** {2:specialize-expr Specialized printers for [ty]} *) + + method virtual ty_TApp_tuple : full:ty -> ty list fn + (** [ty_TApp_tuple ~full types] prints a tuple type with + compounds types [types]. [full] is the unspecialized [ty]. *) + + method virtual ty_TApp_application : + full:ty -> concrete_ident -> generic_value list fn + (** [ty_TApp_application ~full typ generic_args] prints the type + [typ<...generic_args>]. [full] is the unspecialized [ty]. *) + + method items : item list fn + + (** {1 Misc methods} *) + + (** {1 Convenience methods} *) + + method attrs : attrs fn + + method assertion_failure : 'any. string -> 'any + (** Helper that throws and reports an [Types.AssertionFailure] error. *) + + method set_current_namespace : (string * string list) option -> unit + method get_current_namespace : unit -> (string * string list) option + + method virtual namespace_of_concrete_ident : + concrete_ident -> string * string list + + method virtual printer_name : string + method virtual par_state : ast_position -> par_state + + method unreachable : 'any. unit -> 'any + (** Mark an unreachable place in the printer. *) + end +end diff --git a/engine/lib/generic_printer/generic_printer_template.ml b/engine/lib/generic_printer/generic_printer_template.ml new file mode 100644 index 000000000..86582c455 --- /dev/null +++ b/engine/lib/generic_printer/generic_printer_template.ml @@ -0,0 +1,64 @@ +module Make (F : Features.T) = struct + module AST = Ast.Make (F) + open Ast.Make (F) + module P = Generic_printer_base.Make (F) + open PPrint + + let unimplemented s = string ("unimplemented: " ^ s) + + class print = + object + inherit P.base as _super + method ty_TApp_tuple ~full:_ _args = unimplemented "ty_TApp_tuple" + + method ty_TApp_application ~full:_ _f _args = + unimplemented "ty_TApp_application" + + method expr_App_constant ~full:_ _ident _generic_values = + unimplemented "expr_App_constant" + + method expr_App_application ~full:_ _f _args _generics = + unimplemented "expr_App_application" + + method expr_App_tuple_projection ~full:_ ~size:_ ~nth:_ _tuple = + unimplemented "expr_App_tuple_projection" + + method expr_App_field_projection ~full:_ _ident _data = + unimplemented "expr_App_field_projection" + + method expr_Construct_inductive ~full:_ ~is_record:_ ~is_struct:_ + ~constructor:_ ~base:_ _fields = + unimplemented "expr_Construct_inductive" + + method expr_Construct_tuple ~full:_ _components = + unimplemented "expr_Construct_tuple" + + method expr_ _ _ctx _expr = unimplemented "expr_" + method ty_ _ _ctx _typ = unimplemented "ty_" + method pat_ _ _ctx _pat = unimplemented "pat_" + method item_ _ _item = unimplemented "item_" + method arm_ _ _arm = unimplemented "arm_" + method generic_param_ _ _gp = unimplemented "generic_param_" + method param_ty_ _ _param_ty = unimplemented "param_ty_" + method impl_item_ _ _ii = unimplemented "impl_item_" + method trait_item_ _ _ti = unimplemented "trait_item_" + method attr_ _ _attr = unimplemented "attr_" + + method namespace_of_concrete_ident = + Concrete_ident.DefaultViewAPI.to_namespace + + method printer_name = "blank-template" + method par_state _ = AlreadyPar + + method concrete_ident_ _ ~under_current_ns:_ _ident = + unimplemented "concrete_ident_" + end + + open Generic_printer_api.Make (F) + + include Api (struct + type aux_info = unit + + let new_print _ = (new print :> print_object) + end) +end diff --git a/engine/lib/generic_printer/rust_printer.ml b/engine/lib/generic_printer/rust_printer.ml new file mode 100644 index 000000000..57d4503f4 --- /dev/null +++ b/engine/lib/generic_printer/rust_printer.ml @@ -0,0 +1,170 @@ +open Prelude + +module Make (F : Features.T) = struct + module AST = Ast.Make (F) + open Ast.Make (F) + open Generic_printer_base + module P = Generic_printer_base.Make (F) + open PPrint + + let unimplemented s = string ("unimplemented: " ^ s) + + module View = Concrete_ident.DefaultViewAPI + + let iblock f = group >> jump 2 0 >> terminate (break 0) >> f >> group + let call = ( !: ) + + class print = + object (print) + inherit P.base as _super + method ty_TApp_tuple ~full:_ _args = unimplemented "ty_TApp_tuple" + + method ty_TApp_application ~full:_ _f _args = + unimplemented "ty_TApp_application" + + method expr_App_constant ~full:_ _ident _generic_values = + unimplemented "expr_App_constant" + + method expr_App_application ~full:_ _f _args _generics = + unimplemented "expr_App_application" + + method expr_App_tuple_projection ~full:_ ~size:_ ~nth:_ _tuple = + unimplemented "expr_App_tuple_projection" + + method expr_App_field_projection ~full:_ _ident _data = + unimplemented "expr_App_field_projection" + + method expr_Construct_inductive ~full:_ ~is_record:_ ~is_struct:_ + ~constructor:_ ~base:_ _fields = + unimplemented "expr_Construct_inductive" + + method expr_Construct_tuple ~full:_ _components = + unimplemented "expr_Construct_tuple" + + method expr_ _ ctx expr = + let wrap_parens = + group + >> match ctx with AlreadyPar -> Fn.id | NeedsPar -> iblock braces + in + match expr.e with + | If { cond; then_; else_ } -> + let if_then = + (string "if" ^//^ nest 2 (print#expr_at Expr_If_cond cond)) + ^/^ string "then" + ^//^ (print#expr_at Expr_If_then then_ |> braces |> nest 1) + in + (match else_ with + | None -> if_then + | Some else_ -> + if_then ^^ break 1 ^^ string "else" ^^ space + ^^ (print#expr_at Expr_If_else else_ |> iblock braces)) + |> wrap_parens + | Match { scrutinee; arms } -> + let header = + string "match" ^^ space + ^^ (print#expr_at Expr_Match_scrutinee scrutinee + |> terminate space |> iblock Fn.id) + |> group + in + let arms = + separate_map hardline + (call print#arm >> group >> nest 2 + >> precede (bar ^^ space) + >> group) + arms + in + header ^^ iblock braces arms + | Let { monadic; lhs; rhs; body } -> + (Option.map ~f:(fun monad -> print#expr_monadic_let ~monad) monadic + |> Option.value ~default:print#expr_let) + ~lhs ~rhs body + |> wrap_parens + | Literal l -> print#literal l + | Block (e, _) -> call print#expr ctx e + | _ -> unimplemented "todo" + + + method expr_monadic_let + : monad:supported_monads * F.monadic_binding -> + lhs:pat -> + rhs:expr -> + expr fn = + fun ~monad:_ ~lhs ~rhs body -> print#expr_let ~lhs ~rhs body + + method expr_let : lhs:pat -> rhs:expr -> expr fn = + fun ~lhs ~rhs body -> + string "let" + ^/^ iblock Fn.id (print#pat_at Expr_Let_lhs lhs) + ^/^ equals + ^/^ iblock Fn.id (print#expr_at Expr_Let_rhs rhs) + ^^ semi + ^/^ (print#expr_at Expr_Let_body body |> group) + + + method literal = + function + | String s -> utf8string s |> dquotes + | Char c -> char c |> bquotes + | Int { value; negative; _ } -> + string value |> precede (if negative then minus else empty) + | Float { value; kind; negative } -> + string value + |> precede (if negative then minus else empty) + |> terminate + (string (match kind with F32 -> "f32" | F64 -> "f64")) + | Bool b -> OCaml.bool b + + method ty_ _ _ctx _typ = unimplemented "ty_" + method pat_ _ _ctx _pat = unimplemented "pat_" + + method item_ _ item = + match item.v with + | Fn { name; generics; body; params } -> + let params = + iblock parens (separate_map (comma ^^ break 1) print#param params) + in + let generics = + separate_map comma (call print#generic_param) generics.params + in + string "fn" ^^ space + ^^ call print#concrete_ident name + ^^ generics ^^ params + ^^ iblock braces (print#expr_at Item_Fn_body body) + | _ -> string "item not implemented" + + method param_ty_ _ _param_ty = unimplemented "param_ty_" + + method param (param : param) = + let { pat; typ = _; typ_span = _; attrs } = param in + print#attrs attrs ^^ print#pat_at Param_pat pat ^^ space ^^ colon + ^^ space ^^ !:(print#param_ty) param + + method arm_ _ _arm = unimplemented "arm_" + method generic_param_ _ _gp = unimplemented "generic_param_" + method impl_item_ _ _ii = unimplemented "impl_item_" + method trait_item_ _ _ti = unimplemented "trait_item_" + method attr_ _ _attr = unimplemented "attr_" + + method namespace_of_concrete_ident = + Concrete_ident.DefaultViewAPI.to_namespace + + method printer_name = "blank-template" + method par_state _ = AlreadyPar + + method concrete_ident_ _ ~under_current_ns id = + let id = View.to_view id in + let chunks = + if under_current_ns then [ id.definition ] + else id.crate :: (id.path @ [ id.definition ]) + in + separate_map (colon ^^ colon) utf8string chunks + end + + open Generic_printer_api.Make (F) + + include Api (struct + type aux_info = unit + + let new_print _ = (new print :> print_object) + end) +end diff --git a/engine/lib/generic_printer/rust_printer.mli b/engine/lib/generic_printer/rust_printer.mli new file mode 100644 index 000000000..6a277bb7f --- /dev/null +++ b/engine/lib/generic_printer/rust_printer.mli @@ -0,0 +1,4 @@ +module Make (F : Features.T) : sig + open Generic_printer_api.Make(F) + include API with type aux_info = unit +end diff --git a/engine/profile.dump b/engine/profile.dump new file mode 100644 index 000000000..e69de29bb diff --git a/flake.lock b/flake.lock index b5435ed81..768e5773c 100644 --- a/flake.lock +++ b/flake.lock @@ -101,11 +101,11 @@ }, "nixpkgs": { "locked": { - "lastModified": 1694343207, - "narHash": "sha256-jWi7OwFxU5Owi4k2JmiL1sa/OuBCQtpaAesuj5LXC8w=", + "lastModified": 1708847675, + "narHash": "sha256-RUZ7KEs/a4EzRELYDGnRB6i7M1Izii3JD/LyzH0c6Tg=", "owner": "NixOS", "repo": "nixpkgs", - "rev": "78058d810644f5ed276804ce7ea9e82d92bee293", + "rev": "2a34566b67bef34c551f204063faeecc444ae9da", "type": "github" }, "original": { @@ -113,6 +113,29 @@ "type": "indirect" } }, + "ocaml-sourcemaps": { + "inputs": { + "flake-utils": [ + "flake-utils" + ], + "nixpkgs": [ + "nixpkgs" + ] + }, + "locked": { + "lastModified": 1709059830, + "narHash": "sha256-K+g/h6xhE5uOBri1oCaOier3jeIwZrMGOSx79mz5FrU=", + "owner": "W95Psp", + "repo": "ocaml-sourcemaps", + "rev": "391ef51d2fad9884f7535e003b9c9f1a53536fbb", + "type": "github" + }, + "original": { + "owner": "W95Psp", + "repo": "ocaml-sourcemaps", + "type": "github" + } + }, "root": { "inputs": { "crane": "crane", @@ -120,10 +143,8 @@ "fstar": "fstar", "hacl-star": "hacl-star", "nixpkgs": "nixpkgs", - "rust-overlay": [ - "crane", - "rust-overlay" - ] + "ocaml-sourcemaps": "ocaml-sourcemaps", + "rust-overlay": "rust-overlay_2" } }, "rust-overlay": { @@ -151,6 +172,29 @@ "type": "github" } }, + "rust-overlay_2": { + "inputs": { + "flake-utils": [ + "flake-utils" + ], + "nixpkgs": [ + "nixpkgs" + ] + }, + "locked": { + "lastModified": 1708913568, + "narHash": "sha256-76PGANC2ADf0h7fe0w2nWpfdGN+bemFs2rvW2EdU/ZY=", + "owner": "oxalica", + "repo": "rust-overlay", + "rev": "cbdf3e5bb205ff2ca165fe661fbd6d885cbd0106", + "type": "github" + }, + "original": { + "owner": "oxalica", + "repo": "rust-overlay", + "type": "github" + } + }, "systems": { "locked": { "lastModified": 1681028828, diff --git a/flake.nix b/flake.nix index ea56f4ca6..7fa470aab 100644 --- a/flake.nix +++ b/flake.nix @@ -8,7 +8,13 @@ flake-utils.follows = "flake-utils"; }; }; - rust-overlay.follows = "crane/rust-overlay"; + rust-overlay = { + url = "github:oxalica/rust-overlay"; + inputs = { + nixpkgs.follows = "nixpkgs"; + flake-utils.follows = "flake-utils"; + }; + }; fstar = { url = "github:FStarLang/FStar/v2024.01.13"; inputs = { @@ -20,6 +26,14 @@ url = "github:hacl-star/hacl-star"; flake = false; }; + ocaml-sourcemaps = { + url = "github:W95Psp/ocaml-sourcemaps"; + flake = true; + inputs = { + nixpkgs.follows = "nixpkgs"; + flake-utils.follows = "flake-utils"; + }; + }; }; outputs = { @@ -41,13 +55,15 @@ ocamlformat = pkgs.ocamlformat_0_24_1; rustfmt = pkgs.rustfmt; fstar = inputs.fstar.packages.${system}.default; + ocaml-sourcemaps = inputs.ocaml-sourcemaps.packages.${system}.default; + ocamlPackages = pkgs.ocamlPackages; in rec { packages = { inherit rustc ocamlformat rustfmt fstar; hax-engine = pkgs.callPackage ./engine { hax-rust-frontend = packages.hax-rust-frontend.unwrapped; hax-engine-names-extract = packages.hax-rust-frontend.hax-engine-names-extract; - inherit rustc; + inherit rustc ocaml-sourcemaps ocamlPackages; }; hax-rust-frontend = pkgs.callPackage ./cli { inherit rustc craneLib; @@ -112,11 +128,11 @@ in let packages = [ ocamlformat - pkgs.ocamlPackages.ocaml-lsp - pkgs.ocamlPackages.ocamlformat-rpc-lib - pkgs.ocamlPackages.ocaml-print-intf - pkgs.ocamlPackages.odoc - pkgs.ocamlPackages.utop + ocamlPackages.ocaml-lsp + ocamlPackages.ocamlformat-rpc-lib + ocamlPackages.ocaml-print-intf + ocamlPackages.odoc + ocamlPackages.utop pkgs.cargo-expand pkgs.cargo-insta diff --git a/tests/attributes/src/lib.rs b/tests/attributes/src/lib.rs index c069aeaea..e02f181dc 100644 --- a/tests/attributes/src/lib.rs +++ b/tests/attributes/src/lib.rs @@ -1,41 +1,8 @@ -use hax_lib_macros as hax; - -// dummy max value -const u32_max: u32 = 90000; - -#[hax::requires(x > 10 && y > 10 && z > 10 && x + y + z < u32_max)] -#[hax::ensures(|result| hax_lib::implies(true, || result > 32))] -fn add3(x: u32, y: u32, z: u32) -> u32 { - x + y + z -} - -#[hax::lemma] -fn add3_lemma(x: u32) -> Proof<{ x <= 10 || x >= u32_max / 3 || add3(x, x, x) == x * 3 }> {} - -#[hax::exclude] -pub fn f<'a, T>(c: bool, x: &'a mut T, y: &'a mut T) -> &'a mut T { - if c { - x - } else { - y - } -} - -#[hax::attributes] -pub struct Foo { - pub x: u32, - #[refine(y > 3)] - pub y: u32, - #[refine(y + x + z > 3)] - pub z: u32, -} - -#[hax::exclude] -impl Foo { - fn g(&self) {} +trait Foo { + type X; + const FOO: Self::X; } -impl Foo { - #[hax::exclude] - fn h(&self) {} +fn f>(x: T) -> usize { + T::FOO + 3 }