diff --git a/ast_spec.md b/ast_spec.md new file mode 100644 index 000000000..988aac373 --- /dev/null +++ b/ast_spec.md @@ -0,0 +1,79 @@ +# Hax CFG + +```ebnf +literal ::= +| """ string """ +| "'" char "'" +| int +| float +| ("true" | "false") +``` + +```ebnf +ty ::= +| "bool" +| "char" +| ("u8" | "u16" | "u32" | "u64" | "u128" | "usize") +| ("f16" | "f32" | "f64") +| "str" +| (ty ",")* +| "[" ty ";" int "]" +| /* features: slice */ "[" ty "]" +| (/* features: raw_pointer */ "*const" ty | /* features: raw_pointer */ "*mut" ty) +| (/* features: reference */ "*" expr | /* features: reference , mutable_reference */ "*mut" expr) +| ident +| (ty "->")* ty +| impl "::" item +| "impl" ty +| /* features: dyn */ (goal)* +``` + +```ebnf +pat ::= +| "_" +| pat ":" +| constructor pat +| ("pat" "|")* "pat" +| ("[" (expr ",")* "]" | "[" expr ";" int "]") +| /* features: reference */ "&" pat +| literal +| /*TODO: please implement the method `pat'_PBinding`*/ +``` + +```ebnf +expr ::= +| "if" expr "{" expr "}" ("else" "{" expr "}")? +| expr "(" (expr ",")* ")" +| literal +| ("[" (expr ",")* "]" | "[" expr ";" int "]") +| (ident"(" (expr ",")* ")" | ident"{" (ident ":"expr ";")* "}" | /* features: construct_base */ ident"{" (ident ":"expr ";")* ".." base "}") +| "match" expr "{" (("|" pat)* "=>" (expr "," | "{" expr "}"))* "}" +| ("let" pat (":" ty)? ":=" expr ";" expr | /* features: monadic_binding */ monadic_binding "<" monad ">" "(" "|" pat "|" expr","expr ")") +| /* features: block */ modifiers "{" expr "}" +| local_var +| /*TODO: please implement the method `expr'_GlobalVar_concrete`*/ +| expr "as" ty +| macro_name "!" "(" macro_args ")" +| lhs "=" expr +| (/* features: loop */ "loop" "{" expr "}" | /* features: loop , while_loop */ "while" "(" expr ")" "{" expr "}" | /* features: loop , for_loop */ "for" "(" pat "in" expr ")" "{" expr "}" | /* features: loop , for_index_loop */ "for" "(" "let" ident "in" expr ".." expr ")" "{" expr "}") +| /* features: break , loop */ "break" expr +| /* features: early_exit */ "return" expr +| /* features: question_mark */ expr "?" +| /* features: continue , loop */ "continue" +| /* features: reference */ "&" ("mut")? expr +| ("&" expr "as" "&const _" | /* features: mutable_pointer */ "&mut" expr"as" "&mut _") +| "|" param "|" expr +``` + +```ebnf +item ::= +| modifiers "fn" ident "(" (pat ":"ty ",")* ")" (":"ty)? "{" expr "}" +| "type" ident "=" ty +| "enum" ident "=" "{" (ident ("(" (ty)* ")")? ",")* "}" +| "struct" ident "=" "{" (ident ":" ty ",")* "}" +| /* features: macro */ (public_nat_mod | bytes | public_bytes | array | unsigned_public_integer) +| "trait" ident "{" (trait_item)* "}" +| "impl" ("<" (generics ",")* ">")? ident "for" ty "{" (impl_item)* "}" +| /*TODO: please implement the method `item'_Alias`*/ +| "use" path ";" +``` \ No newline at end of file diff --git a/cli/subcommands/src/cargo_hax.rs b/cli/subcommands/src/cargo_hax.rs index a2bf5e666..4c5e1ce86 100644 --- a/cli/subcommands/src/cargo_hax.rs +++ b/cli/subcommands/src/cargo_hax.rs @@ -124,6 +124,58 @@ fn find_hax_engine(message_format: MessageFormat) -> process::Command { }) } +const AST_PRINTER_BINARY_NAME: &str = "hax-ast-printer"; +const AST_PRINTER_BINARY_NOT_FOUND: &str = + "The binary [hax-ast-printer] was not found in your [PATH]."; + +/// Dynamically looks for binary [AST_PRINTER_BINARY_NAME]. First, we +/// check whether [HAX_AST_PRINTER_BINARY] is set, and use that if it +/// is. Then, we try to find [AST_PRINTER_BINARY_NAME] in PATH. If not +/// found, detect whether nodejs is available, download the JS-compiled +/// ast_printer and use it. +#[allow(unused_variables, unreachable_code)] +fn find_hax_ast_printer(message_format: MessageFormat) -> process::Command { + use which::which; + + std::env::var("HAX_AST_PRINTER_BINARY") + .ok() + .map(process::Command::new) + .or_else(|| { + which(AST_PRINTER_BINARY_NAME) + .ok() + .map(process::Command::new) + }) + .or_else(|| { + which("node").ok().and_then(|_| { + if let Ok(true) = inquire::Confirm::new(&format!( + "{} Should I try to download it from GitHub?", + AST_PRINTER_BINARY_NOT_FOUND, + )) + .with_default(true) + .prompt() + { + let cmd = process::Command::new("node"); + let ast_printer_js_path: String = + panic!("TODO: Downloading from GitHub is not supported yet."); + cmd.arg(ast_printer_js_path); + Some(cmd) + } else { + None + } + }) + }) + .unwrap_or_else(|| { + fn is_opam_setup_correctly() -> bool { + std::env::var("OPAM_SWITCH_PREFIX").is_ok() + } + HaxMessage::AstPrinterNotFound { + is_opam_setup_correctly: is_opam_setup_correctly(), + } + .report(message_format, None); + std::process::exit(2); + }) +} + use hax_types::diagnostics::message::HaxMessage; use hax_types::diagnostics::report::ReportCtx; @@ -194,6 +246,19 @@ impl HaxMessage { ); eprintln!("{}", renderer.render(Level::Warning.title(&title))); } + Self::AstPrinterNotFound { + is_opam_setup_correctly, + } => { + use colored::Colorize; + let message = format!("hax: {}\n{}\n\n{} {}\n", + &AST_PRINTER_BINARY_NOT_FOUND, + "Please make sure the ast_printer is installed and is in PATH!", + "Hint: With OPAM, `eval $(opam env)` is necessary for OPAM binaries to be in PATH: make sure to run `eval $(opam env)` before running `cargo hax`.".bright_black(), + format!("(diagnostics: {})", if is_opam_setup_correctly { "opam seems okay ✓" } else {"opam seems not okay ❌"}).bright_black() + ); + let message = Level::Error.title(&message); + eprintln!("{}", renderer.render(message)) + } } } } @@ -541,6 +606,27 @@ fn run_command(options: &Options, haxmeta_files: Vec) -> boo } error } + Command::GenerateAST => { + let mut generate_ast_subprocess = find_hax_ast_printer(options.message_format) + .stdin(std::process::Stdio::piped()) + .stdout(std::process::Stdio::piped()) + .spawn() + .inspect_err(|e| { + if let std::io::ErrorKind::NotFound = e.kind() { + panic!( + "The binary [{}] was not found in your [PATH].", + ENGINE_BINARY_NAME + ) + } + }) + .unwrap(); + + let stdout = std::io::BufReader::new(generate_ast_subprocess.stdout.take().unwrap()); + for msg in stdout.lines() { + println!("{}", msg.unwrap()); + } + true + } } } diff --git a/engine/bin/ast_printer.ml b/engine/bin/ast_printer.ml new file mode 100644 index 000000000..2555171b9 --- /dev/null +++ b/engine/bin/ast_printer.ml @@ -0,0 +1,687 @@ +open Hax_engine +open Utils +open Base +open Ast + +module Make + (F : Features.T) (Default : sig + val default : string -> string + end) = +struct + module AST = Ast.Make (F) + open Ast.Make (F) + module Base = Generic_printer.Make (F) + open PPrint + + let default_string_for s = + "/*" ^ "TODO: please implement the method `" ^ s ^ "`" ^ "*/" + + let default_document_for = default_string_for >> string + let any_number_of x = parens x ^^ string "*" + let option_of x = parens x ^^ string "?" + let either_of x = parens (separate (space ^^ string "|" ^^ space) x) + let symbol_of x = string "\"" ^^ x ^^ string "\"" + let symbol_str x = string "\"" ^^ string x ^^ string "\"" + let symbol_colon = symbol_of colon + let symbol_semi = symbol_of semi + let symbol_comma = symbol_of comma + + let symbol_parens x = + string "\"" + ^^ parens (string "\"" ^^ space ^^ x ^^ space ^^ string "\"") + ^^ string "\"" + + let symbol_brackets x = + string "\"" + ^^ brackets (string "\"" ^^ space ^^ x ^^ space ^^ string "\"") + ^^ string "\"" + + let symbol_braces x = + string "\"" + ^^ braces (string "\"" ^^ space ^^ x ^^ space ^^ string "\"") + ^^ string "\"" + + let features l = + string "/*" ^^ space ^^ string "features:" ^^ space + ^^ separate_map (space ^^ comma ^^ space) (fun x -> string x) l + ^^ space ^^ string "*/" ^^ space + + (* let code_parens x = string "1;31m" ^ parens ( x ^^ string "\x1b[1;31m" ) ^^ string "\x1b[0m" *) + + class printer = + object + inherit Base.base + + (* BEGIN GENERATED *) + method arm ~arm:_ ~span:_ = default_document_for "arm" + + method arm' ~super:_ ~arm_pat:_ ~body:_ ~guard:_ = + default_document_for "arm'" + + method attrs _x1 = default_document_for "attrs" + + method binding_mode_ByRef _x1 _x2 = + default_document_for "binding_mode_ByRef" + + method binding_mode_ByValue = default_document_for "binding_mode_ByValue" + method borrow_kind_Mut _x1 = default_document_for "borrow_kind_Mut" + method borrow_kind_Shared = default_document_for "borrow_kind_Shared" + method borrow_kind_Unique = default_document_for "borrow_kind_Unique" + + method common_array x1 = + either_of + [ + symbol_brackets + (any_number_of (string "expr" ^^ space ^^ symbol_comma)); + symbol_brackets + (string "expr" ^^ space ^^ symbol_str ";" ^^ space ^^ string "int"); + ] + + method dyn_trait_goal ~trait:_ ~non_self_args:_ = + default_document_for "dyn_trait_goal" + + method error_expr _x1 = default_document_for "error_expr" + method error_item _x1 = default_document_for "error_item" + method error_pat _x1 = default_document_for "error_pat" + method expr ~e ~span:_ ~typ:_ = e#p + + method expr'_AddressOf ~super:_ ~mut ~e:_ ~witness:_ = + either_of + [ + symbol_str "&" ^^ space ^^ string "expr" ^^ space ^^ symbol_str "as" + ^^ space ^^ symbol_str "&const _"; + features [ "mutable_pointer" ] + ^^ symbol_str "&mut" ^^ space ^^ string "expr" ^^ symbol_str "as" + ^^ space ^^ symbol_str "&mut _"; + ] + + method _do_not_override_expr'_App ~super ~f ~args ~generic_args + ~bounds_impls ~trait = + string "expr" ^^ space + ^^ symbol_parens + (any_number_of (string "expr" ^^ space ^^ symbol_comma)) + + method expr'_App_application ~super:_ ~f:_ ~args:_ ~generics:_ = + default_document_for "expr'_App_application" + + method expr'_App_constant ~super:_ ~constant:_ ~generics:_ = + default_document_for "expr'_App_constant" + + method expr'_App_field_projection ~super:_ ~field:_ ~e:_ = + default_document_for "expr'_App_field_projection" + + method expr'_App_tuple_projection ~super:_ ~size:_ ~nth:_ ~e:_ = + default_document_for "expr'_App_tuple_projection" + + method expr'_Ascription ~super:_ ~e:_ ~typ:_ = + string "expr" ^^ space ^^ symbol_str "as" ^^ space ^^ string "ty" + + method expr'_Assign ~super:_ ~lhs:_ ~e:_ ~witness:_ = + string "lhs" ^^ space ^^ symbol_str "=" ^^ space ^^ string "expr" + + method expr'_Block ~super:_ ~e:_ ~safety_mode:_ ~witness:_ = + features [ "block" ] ^^ string "modifiers" ^^ space + ^^ symbol_braces (string "expr") + + method expr'_Borrow ~super:_ ~kind:_ ~e:_ ~witness:_ = + features [ "reference" ] ^^ symbol_str "&" ^^ space + ^^ option_of (symbol_str "mut") + ^^ space ^^ string "expr" + + method expr'_Break ~super:_ ~e:_ ~acc:_ ~label:_ ~witness:_ = + features [ "break"; "loop" ] + ^^ symbol_str "break" ^^ space ^^ string "expr" + + method expr'_Closure ~super:_ ~params:_ ~body:_ ~captures:_ = + symbol_str "|" ^^ space ^^ string "param" ^^ space ^^ symbol_str "|" + ^^ space ^^ string "expr" + + method expr'_Construct_inductive ~super:_ ~constructor:_ ~is_record:_ + ~is_struct:_ ~fields:_ ~base:_ = + either_of + [ + string "ident" + ^^ symbol_parens + (any_number_of (string "expr" ^^ space ^^ symbol_comma)); + string "ident" + ^^ symbol_braces + (any_number_of + (string "ident" ^^ space ^^ symbol_colon ^^ string "expr" + ^^ space ^^ symbol_semi)); + features [ "construct_base" ] + ^^ string "ident" + ^^ symbol_braces + (any_number_of + (string "ident" ^^ space ^^ symbol_colon ^^ string "expr" + ^^ space ^^ symbol_semi) + ^^ space ^^ symbol_str ".." ^^ space ^^ string "base"); + ] + (* string "constructor" ^^ space ^^ any_number_of (string "expr") *) + + method expr'_Construct_tuple ~super:_ ~components:_ = + default_document_for "expr'_Construct_tuple" + + method expr'_Continue ~super:_ ~acc:_ ~label:_ ~witness:_ = + features [ "continue"; "loop" ] ^^ symbol_str "continue" + + method expr'_EffectAction ~super:_ ~action:_ ~argument:_ = + features [ "monadic_action" ] + ^^ default_document_for "expr'_EffectAction" + + method expr'_GlobalVar_concrete ~super:_ _x2 = + default_document_for "expr'_GlobalVar_concrete" + + method expr'_GlobalVar_primitive ~super:_ _x2 = + default_document_for "expr'_GlobalVar_primitive" + + method expr'_If ~super:_ ~cond:_ ~then_:_ ~else_:_ = + symbol_str "if" ^^ space ^^ string "expr" ^^ space + ^^ symbol_braces (string "expr") + ^^ space + ^^ option_of + (symbol_str "else" ^^ space ^^ symbol_braces (string "expr")) + + method expr'_Let ~super:_ ~monadic:_ ~lhs:_ ~rhs:_ ~body:_ = + either_of + [ + symbol_str "let" ^^ space ^^ string "pat" ^^ space + ^^ option_of (symbol_colon ^^ space ^^ string "ty") + ^^ space ^^ symbol_str ":=" ^^ space ^^ string "expr" ^^ space + ^^ symbol_semi ^^ space ^^ string "expr"; + features [ "monadic_binding" ] + ^^ string "monadic_binding" ^^ space ^^ symbol_str "<" ^^ space + ^^ string "monad" ^^ space ^^ symbol_str ">" ^^ space + ^^ symbol_parens + (symbol_str "|" ^^ space ^^ string "pat" ^^ space + ^^ symbol_str "|" ^^ space ^^ string "expr" ^^ symbol_comma + ^^ string "expr"); + ] + + method expr'_Literal ~super:_ _x2 = string "literal" + method expr'_LocalVar ~super:_ _x2 = string "local_var" + + method expr'_Loop ~super:_ ~body:_ ~kind:_ ~state:_ ~control_flow:_ + ~label:_ ~witness:_ = + (* Type of loop *) + either_of + [ + features [ "loop" ] ^^ symbol_str "loop" ^^ space + ^^ symbol_braces (string "expr"); + features [ "loop"; "while_loop" ] + ^^ symbol_str "while" ^^ space + ^^ symbol_parens (string "expr") + ^^ space + ^^ symbol_braces (string "expr"); + features [ "loop"; "for_loop" ] + ^^ symbol_str "for" ^^ space + ^^ symbol_parens + (string "pat" ^^ space ^^ symbol_str "in" ^^ space + ^^ string "expr") + ^^ space + ^^ symbol_braces (string "expr"); + features [ "loop"; "for_index_loop" ] + ^^ symbol_str "for" ^^ space + ^^ symbol_parens + (symbol_str "let" ^^ space ^^ string "ident" ^^ space + ^^ symbol_str "in" ^^ space ^^ string "expr" ^^ space + ^^ symbol_str ".." ^^ space ^^ string "expr") + ^^ space + ^^ symbol_braces (string "expr"); + ] + + method expr'_MacroInvokation ~super:_ ~macro:_ ~args:_ ~witness:_ = + string "macro_name" ^^ space ^^ symbol_str "!" ^^ space + ^^ symbol_parens (string "macro_args") + + method expr'_Match ~super:_ ~scrutinee:_ ~arms:_ = + symbol_str "match" ^^ space ^^ string "expr" ^^ space + ^^ symbol_braces + (any_number_of + (any_number_of (symbol_str "|" ^^ space ^^ string "pat") + ^^ space ^^ symbol_str "=>" ^^ space + ^^ either_of + [ + string "expr" ^^ space ^^ symbol_comma; + symbol_braces (string "expr"); + ])) + + method expr'_QuestionMark ~super:_ ~e:_ ~return_typ:_ ~witness:_ = + features [ "question_mark" ] ^^ string "expr" ^^ space ^^ symbol_str "?" + + method expr'_Quote ~super:_ _x2 = default_document_for "expr'_Quote" + + method expr'_Return ~super:_ ~e:_ ~witness:_ = + features [ "early_exit" ] ^^ symbol_str "return" ^^ space + ^^ string "expr" + + method cf_kind_BreakOrReturn = + default_document_for "cf_kind_BreakOrReturn" + + method cf_kind_BreakOnly = default_document_for "cf_kind_BreakOnly" + method field_pat ~field:_ ~pat:_ = default_document_for "field_pat" + + method generic_constraint_GCLifetime _x1 _x2 = + default_document_for "generic_constraint_GCLifetime" + + method generic_constraint_GCProjection _x1 = + default_document_for "generic_constraint_GCProjection" + + method generic_constraint_GCType _x1 = + default_document_for "generic_constraint_GCType" + + method generic_param ~ident:_ ~span:_ ~attrs:_ ~kind:_ = + default_document_for "generic_param" + + method generic_param_kind_GPConst ~typ:_ = + default_document_for "generic_param_kind_GPConst" + + method generic_param_kind_GPLifetime ~witness:_ = + default_document_for "generic_param_kind_GPLifetime" + + method generic_param_kind_GPType = + default_document_for "generic_param_kind_GPType" + + method generic_value_GConst _x1 = + default_document_for "generic_value_GConst" + + method generic_value_GLifetime ~lt:_ ~witness:_ = + default_document_for "generic_value_GLifetime" + + method generic_value_GType _x1 = + default_document_for "generic_value_GType" + + method generics ~params:_ ~constraints:_ = default_document_for "generics" + method guard ~guard:_ ~span:_ = default_document_for "guard" + + method guard'_IfLet ~super:_ ~lhs:_ ~rhs:_ ~witness:_ = + default_document_for "guard'_IfLet" + + method impl_expr ~kind:_ ~goal:_ = default_document_for "impl_expr" + + method impl_expr_kind_Builtin _x1 = + default_document_for "impl_expr_kind_Builtin" + + method impl_expr_kind_Concrete _x1 = + default_document_for "impl_expr_kind_Concrete" + + method impl_expr_kind_Dyn = default_document_for "impl_expr_kind_Dyn" + + method impl_expr_kind_ImplApp ~impl:_ ~args:_ = + default_document_for "impl_expr_kind_ImplApp" + + method impl_expr_kind_LocalBound ~id:_ = + default_document_for "impl_expr_kind_LocalBound" + + method impl_expr_kind_Parent ~impl:_ ~ident:_ = + default_document_for "impl_expr_kind_Parent" + + method impl_expr_kind_Projection ~impl:_ ~item:_ ~ident:_ = + default_document_for "impl_expr_kind_Projection" + + method impl_expr_kind_Self = default_document_for "impl_expr_kind_Self" + method impl_ident ~goal:_ ~name:_ = default_document_for "impl_ident" + + method impl_item ~ii_span:_ ~ii_generics:_ ~ii_v:_ ~ii_ident:_ ~ii_attrs:_ + = + default_document_for "impl_item" + + method impl_item'_IIFn ~body:_ ~params:_ = + default_document_for "impl_item'_IIFn" + + method impl_item'_IIType ~typ:_ ~parent_bounds:_ = + default_document_for "impl_item'_IIType" + + method item ~v ~span:_ ~ident:_ ~attrs:_ = + v#p (* default_document_for "item" *) + + method item'_Alias ~super:_ ~name:_ ~item:_ = + default_document_for "item'_Alias" + + method item'_Fn ~super:_ ~name:_ ~generics:_ ~body:_ ~params:_ ~safety:_ = + (* TODOD: safe, pub, const, pub(crate) *) + string "modifiers" ^^ space ^^ symbol_str "fn" ^^ space + ^^ string "ident" ^^ space + ^^ symbol_parens + (any_number_of + (string "pat" ^^ space ^^ symbol_colon ^^ string "ty" ^^ space + ^^ symbol_comma)) + ^^ space + ^^ option_of (symbol_colon ^^ string "ty") + ^^ space + ^^ symbol_braces (string "expr") + + method item'_HaxError ~super:_ _x2 = default_document_for "item'_HaxError" + + method item'_IMacroInvokation ~super:_ ~macro:_ ~argument:_ ~span:_ + ~witness:_ = + features [ "macro" ] + ^^ either_of + [ + string "public_nat_mod"; + string "bytes"; + string "public_bytes"; + string "array"; + string "unsigned_public_integer"; + ] + + method item'_Impl ~super:_ ~generics:_ ~self_ty:_ ~of_trait:_ ~items:_ + ~parent_bounds:_ ~safety:_ = + symbol_str "impl" ^^ space + ^^ option_of + (symbol_str "<" ^^ space + ^^ any_number_of (string "generics" ^^ space ^^ symbol_comma) + ^^ space ^^ symbol_str ">") + ^^ space ^^ string "ident" ^^ space ^^ symbol_str "for" ^^ space + ^^ string "ty" ^^ space + ^^ symbol_braces (any_number_of (string "impl_item")) + + method item'_NotImplementedYet = + default_document_for "item'_NotImplementedYet" + + method item'_Quote ~super:_ ~quote:_ ~origin:_ = + features [ "quote" ] ^^ default_document_for "item'_Quote" + + method item'_Trait ~super:_ ~name:_ ~generics:_ ~items:_ ~safety:_ = + symbol_str "trait" ^^ space ^^ string "ident" ^^ space + ^^ symbol_braces (any_number_of (string "trait_item")) + + method item'_TyAlias ~super:_ ~name:_ ~generics:_ ~ty:_ = + symbol_str "type" ^^ space ^^ string "ident" ^^ space ^^ symbol_str "=" + ^^ space ^^ string "ty" + + method item'_Type ~super:_ ~name:_ ~generics:_ ~variants:_ ~is_struct = + (* TODO globality *) + if is_struct then + symbol_str "struct" ^^ space ^^ string "ident" ^^ space + ^^ symbol_str "=" ^^ space + ^^ symbol_braces + (any_number_of + (string "ident" ^^ space ^^ symbol_colon ^^ space + ^^ string "ty" ^^ space ^^ symbol_comma)) + else + symbol_str "enum" ^^ space ^^ string "ident" ^^ space + ^^ symbol_str "=" ^^ space + ^^ symbol_braces + (any_number_of + (string "ident" ^^ space + ^^ option_of (symbol_parens (any_number_of (string "ty"))) + ^^ space ^^ symbol_comma)) + + method item'_Use ~super:_ ~path:_ ~is_external:_ ~rename:_ = + symbol_str "use" ^^ space ^^ string "path" ^^ space ^^ symbol_semi + + method lhs_LhsArbitraryExpr ~e:_ ~witness:_ = + default_document_for "lhs_LhsArbitraryExpr" + + method lhs_LhsArrayAccessor ~e:_ ~typ:_ ~index:_ ~witness:_ = + default_document_for "lhs_LhsArrayAccessor" + + method lhs_LhsFieldAccessor_field ~e:_ ~typ:_ ~field:_ ~witness:_ = + default_document_for "lhs_LhsFieldAccessor_field" + + method lhs_LhsFieldAccessor_tuple ~e:_ ~typ:_ ~nth:_ ~size:_ ~witness:_ = + default_document_for "lhs_LhsFieldAccessor_tuple" + + method lhs_LhsLocalVar ~var:_ ~typ:_ = + default_document_for "lhs_LhsLocalVar" + + method literal_Bool _x1 = + either_of [ symbol_str "true"; symbol_str "false" ] + + method literal_Char _x1 = + symbol_str "'" ^^ space ^^ string "char" ^^ space ^^ symbol_str "'" + + method literal_Float ~value:_ ~negative:_ ~kind:_ = string "float" + method literal_Int ~value:_ ~negative:_ ~kind:_ = string "int" + + method literal_String _x1 = + symbol_str "\"" ^^ space ^^ string "string" ^^ space ^^ symbol_str "\"" + + method loop_kind_ForIndexLoop ~start:_ ~end_:_ ~var:_ ~var_typ:_ + ~witness:_ = + default_document_for "loop_kind_ForIndexLoop" + + method loop_kind_ForLoop ~pat:_ ~it:_ ~witness:_ = + default_document_for "loop_kind_ForLoop" + + method loop_kind_UnconditionalLoop = + default_document_for "loop_kind_UnconditionalLoop" + + method loop_kind_WhileLoop ~condition:_ ~witness:_ = + default_document_for "loop_kind_WhileLoop" + + method loop_state ~init:_ ~bpat:_ ~witness:_ = + default_document_for "loop_state" + + method modul _x1 = default_document_for "modul" + + method param ~pat:_ ~typ:_ ~typ_span:_ ~attrs:_ = + default_document_for "param" + + method pat ~p ~span:_ ~typ:_ = p#p + + method pat'_PAscription ~super:_ ~typ:_ ~typ_span:_ ~pat:_ = + string "pat" ^^ space ^^ symbol_colon + + method pat'_PBinding ~super:_ ~mut:_ ~mode:_ ~var:_ ~typ:_ ~subpat:_ = + default_document_for "pat'_PBinding" + + method pat'_PConstant ~super:_ ~lit:_ = string "literal" + + method pat'_PConstruct_inductive ~super:_ ~constructor:_ ~is_record:_ + ~is_struct:_ ~fields:_ = + string "constructor" ^^ space ^^ string "pat" + + method pat'_PConstruct_tuple ~super:_ ~components:_ = + default_document_for "pat'_PConstruct_tuple" + + method pat'_PDeref ~super:_ ~subpat:_ ~witness:_ = + features [ "reference" ] ^^ symbol_str "&" ^^ space ^^ string "pat" + + method pat'_PWild = symbol_str "_" + + method pat'_POr ~super:_ ~subpats:_ = + any_number_of (symbol_str "pat" ^^ space ^^ symbol_str "|") + ^^ space ^^ symbol_str "pat" + + method printer_name = default_string_for "printer_name" + + method projection_predicate ~impl:_ ~assoc_item:_ ~typ:_ = + default_document_for "projection_predicate" + + method safety_kind_Safe = default_document_for "safety_kind_Safe" + method safety_kind_Unsafe _x1 = default_document_for "safety_kind_Unsafe" + + method supported_monads_MException _x1 = + default_document_for "supported_monads_MException" + + method supported_monads_MOption = + default_document_for "supported_monads_MOption" + + method supported_monads_MResult _x1 = + default_document_for "supported_monads_MResult" + + method trait_goal ~trait:_ ~args:_ = default_document_for "trait_goal" + + method trait_item ~ti_span:_ ~ti_generics:_ ~ti_v:_ ~ti_ident:_ + ~ti_attrs:_ = + default_document_for "trait_item" + + method trait_item'_TIDefault ~params:_ ~body:_ ~witness:_ = + default_document_for "trait_item'_TIDefault" + + method trait_item'_TIFn _x1 = default_document_for "trait_item'_TIFn" + method trait_item'_TIType _x1 = default_document_for "trait_item'_TIType" + + method ty_TApp_application ~typ:_ ~generics:_ = + any_number_of (string "ty" ^^ space ^^ symbol_comma) + (* TODO uses top level implementation ? *) + + method ty_TApp_tuple ~types:_ = default_document_for "ty_TApp_tuple" + + method ty_TArray ~typ:_ ~length:_ = + symbol_brackets + (string "ty" ^^ space ^^ symbol_semi ^^ space ^^ string "int") + + method ty_TArrow _x1 _x2 = + any_number_of (string "ty" ^^ space ^^ symbol_str "->") + ^^ space ^^ string "ty" + + method ty_TAssociatedType ~impl:_ ~item:_ = + string "impl" ^^ space ^^ symbol_str "::" ^^ space ^^ string "item" + + method ty_TBool = symbol_str "bool" + method ty_TChar = symbol_str "char" + + method ty_TDyn ~witness:_ ~goals:_ = + features [ "dyn" ] ^^ any_number_of (string "goal") + + method ty_TFloat _x1 = + either_of [ symbol_str "f16"; symbol_str "f32"; symbol_str "f64" ] + + method ty_TInt _x1 = + either_of + [ + symbol_str "u8"; + symbol_str "u16"; + symbol_str "u32"; + symbol_str "u64"; + symbol_str "u128"; + symbol_str "usize"; + ] + + method ty_TOpaque _x1 = symbol_str "impl" ^^ space ^^ string "ty" + method ty_TParam _x1 = string "ident" + + method ty_TRawPointer ~witness:_ = + either_of + [ + features [ "raw_pointer" ] ^^ symbol_str "*const" ^^ space + ^^ string "ty"; + features [ "raw_pointer" ] ^^ symbol_str "*mut" ^^ space + ^^ string "ty"; + ] + + method ty_TRef ~witness:_ ~region:_ ~typ:_ ~mut:_ = + either_of + [ + features [ "reference" ] ^^ symbol_str "*" ^^ space ^^ string "expr"; + features [ "reference"; "mutable_reference" ] + ^^ symbol_str "*mut" ^^ space ^^ string "expr"; + ] + + method ty_TSlice ~witness:_ ~ty:_ = + features [ "slice" ] ^^ symbol_brackets (string "ty") + + method ty_TStr = symbol_str "str" + + method item'_Enum_Variant ~name:_ ~arguments:_ ~is_record:_ ~attrs:_ = + default_document_for "item'_Enum_Variant" + + method item'_Type_enum ~super:_ ~name:_ ~generics:_ ~variants:_ = + default_document_for "item'_Type_enum" + + method item'_Type_struct ~super:_ ~name:_ ~generics:_ ~tuple_struct:_ + ~arguments:_ = + default_document_for "item'_Type_struct" + + (* END GENERATED *) + end +end + +module HaxCFG = struct + module MyPrinter = + Make + (Features.Full) + (struct + let default x = x + end) + + module MyAstGenerator = Ast_utils.ASTGenerator (Features.Full) + module AST = Ast.Make (Features.Full) + open AST + + let print_ast (_ : unit) = + let my_printer = new MyPrinter.printer in + + let (my_literals, my_tys, my_pats, my_exprs, my_items) + : literal list * ty list * pat list * expr list * item list = + MyAstGenerator.generate_full_ast () + in + + let literal_string = + "\n\n```ebnf\nliteral ::=\n" + ^ String.concat ~sep:"\n" + (List.map + ~f:(fun literal -> + let buf = Buffer.create 0 in + PPrint.ToBuffer.pretty 1.0 80 buf + (my_printer#entrypoint_literal literal); + "| " ^ Buffer.contents buf) + my_literals) + ^ "\n```" + in + let ty_string = + "\n\n```ebnf\nty ::=\n" + ^ String.concat ~sep:"\n" + (List.map + ~f:(fun ty -> + let buf = Buffer.create 0 in + PPrint.ToBuffer.pretty 1.0 80 buf (my_printer#entrypoint_ty ty); + "| " ^ Buffer.contents buf) + my_tys) + ^ "\n```" + in + let pat_string = + "\n\n```ebnf\npat ::=\n" + ^ String.concat ~sep:"\n" + (List.map + ~f:(fun pat -> + let buf = Buffer.create 0 in + PPrint.ToBuffer.pretty 1.0 80 buf (my_printer#entrypoint_pat pat); + "| " ^ Buffer.contents buf) + my_pats) + ^ "\n```" + in + let expr_string = + "\n\n```ebnf\nexpr ::=\n" + ^ String.concat ~sep:"\n" + (List.map + ~f:(fun expr -> + let buf = Buffer.create 0 in + PPrint.ToBuffer.pretty 1.0 80 buf + (my_printer#entrypoint_expr expr); + "| " ^ Buffer.contents buf) + my_exprs) + ^ "\n```" + in + let item_string = + "\n\n```ebnf\nitem ::=\n" + ^ String.concat ~sep:"\n" + (List.map + ~f:(fun item -> + let buf = Buffer.create 0 in + PPrint.ToBuffer.pretty 1.0 80 buf + (my_printer#entrypoint_item item); + "| " ^ Buffer.contents buf) + my_items) + ^ "\n```" + in + + "# Hax CFG" ^ literal_string ^ ty_string ^ pat_string ^ expr_string + ^ item_string +end + +let main = + (* let options = *) + (* let table, json = *) + (* Hax_io.read_json () |> Option.value_exn |> parse_id_table_node *) + (* in *) + (* table *) + (* |> List.iter ~f:(fun (id, json) -> *) + (* Hashtbl.add_exn Types.cache_map ~key:id ~data:(`JSON json)); *) + (* Types.parse_engine_options json *) + (* in *) + Concrete_ident.ImplInfoStore.init + Concrete_ident_generated.impl_infos (* @ options.impl_infos *); + print_endline (HaxCFG.print_ast ()) diff --git a/engine/bin/dune b/engine/bin/dune index da07f5d3e..7ff175d06 100644 --- a/engine/bin/dune +++ b/engine/bin/dune @@ -25,6 +25,12 @@ (modules native_driver) (libraries lib)) +(executable + (public_name hax-ast-printer) + (name ast_printer) + (modules ast_printer) + (libraries lib)) + ; The following line is commented: by default, we don't want to ; generate javascript. diff --git a/engine/lib/ast_utils.ml b/engine/lib/ast_utils.ml index 26e826bbf..a0833282a 100644 --- a/engine/lib/ast_utils.ml +++ b/engine/lib/ast_utils.ml @@ -1273,3 +1273,882 @@ struct (module StringList) ~iteri:(Hashtbl.map h ~f:( ! ) |> Hashtbl.iteri) end + +module ASTGenerator (F : Features.T) = struct + module AST = Ast.Make (F) + open AST + + type ast_type = + | CONCRETE_IDENT + | LITERAL + | TY + | EXPR + | GENERICS + | GLOBAL_IDENT + | PAT + | LOCAL_IDENT + | IMPL_EXPR + | ITEM + + let rec generate_helper (t : ast_type) (indexes : int list) : + Yojson.Safe.t * int list = + let i, indexes = + (List.hd_exn indexes, Option.value ~default:[] (List.tl indexes)) + in + let cases : (unit -> Yojson.Safe.t * int list) list = + match t with + | CONCRETE_IDENT -> + [ + (fun () -> + ( [%yojson_of: concrete_ident] + (Concrete_ident.of_name Value Hax_lib__RefineAs__into_checked), + indexes )); + ] + | LITERAL -> + [ + (fun () -> ([%yojson_of: literal] (String "dummy"), indexes)); + (fun () -> ([%yojson_of: literal] (Char 'a'), indexes)); + (fun () -> + ( [%yojson_of: literal] + (Int + { + value = "42"; + negative = false; + kind = { size = S8; signedness = Unsigned }; + }), + indexes )); + (fun () -> + ( [%yojson_of: literal] + (Float { value = "6.9"; negative = false; kind = F16 }), + indexes )); + (fun () -> ([%yojson_of: literal] (Bool false), indexes)); + ] + | TY -> + [ + (fun () -> ([%yojson_of: ty] TBool, indexes)); + (fun () -> ([%yojson_of: ty] TChar, indexes)); + (fun () -> + ( [%yojson_of: ty] (TInt { size = S8; signedness = Unsigned }), + indexes )); + (fun () -> ([%yojson_of: ty] (TFloat F16), indexes)); + (fun () -> ([%yojson_of: ty] TStr, indexes)); + (fun () -> + let g_ident, indexes = generate_helper GLOBAL_IDENT indexes in + let g_ident = [%of_yojson: global_ident] g_ident in + + let typ, indexes = generate_helper TY indexes in + let typ = [%of_yojson: ty] typ in + + ( [%yojson_of: ty] + (TApp + { + ident = g_ident; + args = [ GType typ (* must have 1+ items *) ]; + }), + indexes )); + (fun () -> + let typ, indexes = generate_helper TY indexes in + let typ = [%of_yojson: ty] typ in + let length, indexes = generate_helper EXPR indexes in + (* Should be const expr ! *) + let length = [%of_yojson: expr] length in + ([%yojson_of: ty] (TArray { typ; length }), indexes)); + (fun () -> + let typ, indexes = generate_helper TY indexes in + let typ = [%of_yojson: ty] typ in + + let wit = [%of_yojson: F.slice] (`String "Slice") in + + ( [%yojson_of: ty] + (TSlice { witness = wit (* Features.On.slice *); ty = typ }), + indexes )); + (fun () -> + let wit = [%of_yojson: F.raw_pointer] (`String "Raw_pointer") in + ([%yojson_of: ty] (TRawPointer { witness = wit }), indexes)); + (fun () -> + let typ, indexes = generate_helper TY indexes in + let typ = [%of_yojson: ty] typ in + + let wit = [%of_yojson: F.reference] (`String "Reference") in + + ( [%yojson_of: ty] + (TRef { witness = wit; region = "todo"; typ; mut = Immutable }), + indexes )); + (fun () -> + let l_ident, indexes = generate_helper LOCAL_IDENT indexes in + let l_ident = [%of_yojson: local_ident] l_ident in + ([%yojson_of: ty] (TParam l_ident), indexes)); + (fun () -> + let typ, indexes = generate_helper TY indexes in + let typ = [%of_yojson: ty] typ in + ([%yojson_of: ty] (TArrow ([], typ)), indexes)); + (fun () -> + let impl_expr, indexes = generate_helper IMPL_EXPR indexes in + let impl_expr = [%of_yojson: impl_expr] impl_expr in + + let c_ident, indexes = generate_helper CONCRETE_IDENT indexes in + let c_ident = [%of_yojson: concrete_ident] c_ident in + ( [%yojson_of: ty] + (TAssociatedType { impl = impl_expr; item = c_ident }), + indexes )); + (fun () -> + let c_ident, indexes = generate_helper CONCRETE_IDENT indexes in + let c_ident = [%of_yojson: concrete_ident] c_ident in + ([%yojson_of: ty] (TOpaque c_ident), indexes)); + (fun () -> + let wit = [%of_yojson: F.dyn] (`String "Dyn") in + ([%yojson_of: ty] (TDyn { witness = wit; goals = [] }), indexes)); + ] + | EXPR -> + let expr_shell e indexes = + let typ, indexes = generate_helper TY indexes in + ( `Assoc + [ + ("e", e); + ("span", `Assoc [ ("id", `Int 79902); ("data", `List []) ]); + ("typ", typ); + ], + indexes ) + in + List.map + ~f:(fun expr_f () -> + let expr', indexes = expr_f () in + expr_shell expr' indexes) + [ + (fun () -> + let cond, indexes = generate_helper EXPR indexes in + let cond = [%of_yojson: expr] cond in + + let then_, indexes = generate_helper EXPR indexes in + let then_ = [%of_yojson: expr] then_ in + + ([%yojson_of: expr'] (If { cond; then_; else_ = None }), indexes)); + (fun () -> + let f, indexes = generate_helper EXPR indexes in + let f = [%of_yojson: expr] f in + + let args, indexes = generate_helper EXPR indexes in + let args = [%of_yojson: expr] args in + + ( [%yojson_of: expr'] + (App + { + f; + args = [ args (* must have 1+ items *) ]; + generic_args = []; + bounds_impls = []; + trait = None; + }), + indexes )); + (fun () -> + let lit, indexes = generate_helper LITERAL indexes in + let lit = [%of_yojson: literal] lit in + ([%yojson_of: expr'] (Literal lit), indexes)); + (fun () -> ([%yojson_of: expr'] (Array []), indexes)); + (fun () -> + let g_ident, indexes = generate_helper GLOBAL_IDENT indexes in + let g_ident = [%of_yojson: global_ident] g_ident in + + ( [%yojson_of: expr'] + (Construct + { + constructor = g_ident; + is_record = false; + is_struct = false; + fields = []; + base = None; + }), + indexes )); + (fun () -> + let expr, indexes = generate_helper EXPR indexes in + let expr = [%of_yojson: expr] expr in + + ( [%yojson_of: expr'] (Match { scrutinee = expr; arms = [] }), + indexes )); + (fun () -> + let lhs, indexes = generate_helper PAT indexes in + let lhs = [%of_yojson: pat] lhs in + + let rhs, indexes = generate_helper EXPR indexes in + let rhs = [%of_yojson: expr] rhs in + + let body, indexes = generate_helper EXPR indexes in + let body = [%of_yojson: expr] body in + + ( [%yojson_of: expr'] (Let { monadic = None; lhs; rhs; body }), + indexes )); + (fun () -> + let expr, indexes = generate_helper EXPR indexes in + let expr = [%of_yojson: expr] expr in + + let wit = [%of_yojson: F.block] (`String "Block") in + + ( [%yojson_of: expr'] + (Block { e = expr; safety_mode = Safe; witness = wit }), + indexes )); + (fun () -> + let l_ident, indexes = generate_helper LOCAL_IDENT indexes in + let l_ident = [%of_yojson: local_ident] l_ident in + ([%yojson_of: expr'] (LocalVar l_ident), indexes)); + (fun () -> + let g_ident, indexes = generate_helper GLOBAL_IDENT indexes in + let g_ident = [%of_yojson: global_ident] g_ident in + ([%yojson_of: expr'] (GlobalVar g_ident), indexes)); + (fun () -> + let expr, indexes = generate_helper EXPR indexes in + let expr = [%of_yojson: expr] expr in + + let typ, indexes = generate_helper TY indexes in + let typ = [%of_yojson: ty] typ in + ([%yojson_of: expr'] (Ascription { e = expr; typ }), indexes)); + (fun () -> + let g_ident, indexes = generate_helper GLOBAL_IDENT indexes in + let g_ident = [%of_yojson: global_ident] g_ident in + + let wit = [%of_yojson: F.macro] (`String "Macro") in + + ( [%yojson_of: expr'] + (MacroInvokation + { macro = g_ident; args = "dummy"; witness = wit }), + indexes )); + (fun () -> + let l_ident, indexes = generate_helper LOCAL_IDENT indexes in + let l_ident = [%of_yojson: local_ident] l_ident in + + let expr, indexes = generate_helper EXPR indexes in + let expr = [%of_yojson: expr] expr in + + let typ, indexes = generate_helper TY indexes in + let typ = [%of_yojson: ty] typ in + + let wit = + [%of_yojson: F.mutable_variable] (`String "mutable_variable") + in + + ( [%yojson_of: expr'] + (Assign + { + lhs = LhsLocalVar { var = l_ident; typ }; + e = expr; + witness = wit; + }), + indexes )); + (fun () -> + let body, indexes = generate_helper EXPR indexes in + let body = [%of_yojson: expr] body in + + let wit = [%of_yojson: F.loop] (`String "Loop") in + + ( [%yojson_of: expr'] + (Loop + { + body; + kind = UnconditionalLoop; + state = None; + control_flow = None; + label = None; + witness = wit; + }), + indexes )); + (fun () -> + let expr, indexes = generate_helper EXPR indexes in + let expr = [%of_yojson: expr] expr in + + let wit = [%of_yojson: F.break] (`String "Break") in + let wit2 = [%of_yojson: F.loop] (`String "Loop") in + + ( [%yojson_of: expr'] + (Break + { + e = expr; + acc = None; + label = None; + witness = (wit, wit2); + }), + indexes )); + (fun () -> + let expr, indexes = generate_helper EXPR indexes in + let expr = [%of_yojson: expr] expr in + + let wit = [%of_yojson: F.early_exit] (`String "Early_exit") in + + ( [%yojson_of: expr'] (Return { e = expr; witness = wit }), + indexes )); + (fun () -> + let expr, indexes = generate_helper EXPR indexes in + let expr = [%of_yojson: expr] expr in + + let typ, indexes = generate_helper TY indexes in + let typ = [%of_yojson: ty] typ in + + let wit = + [%of_yojson: F.question_mark] (`String "Question_mark") + in + + ( [%yojson_of: expr'] + (QuestionMark { e = expr; return_typ = typ; witness = wit }), + indexes )); + (fun () -> + let wit = [%of_yojson: F.continue] (`String "Continue") in + let wit2 = [%of_yojson: F.loop] (`String "Loop") in + ( [%yojson_of: expr'] + (Continue + { acc = None; label = None; witness = (wit, wit2) }), + indexes )); + (fun () -> + let expr, indexes = generate_helper EXPR indexes in + let expr = [%of_yojson: expr] expr in + + let wit = [%of_yojson: F.reference] (`String "Reference") in + + ( [%yojson_of: expr'] + (Borrow { kind = Shared; e = expr; witness = wit }), + indexes )); + (fun () -> + let expr, indexes = generate_helper EXPR indexes in + let expr = [%of_yojson: expr] expr in + + let wit = [%of_yojson: F.raw_pointer] (`String "Raw_pointer") in + + ( [%yojson_of: expr'] + (AddressOf { mut = Immutable; e = expr; witness = wit }), + indexes )); + (fun () -> + let body, indexes = generate_helper EXPR indexes in + let body = [%of_yojson: expr] body in + ( [%yojson_of: expr'] + (Closure { params = []; body; captures = [] }), + indexes )); + (* TODO: The two remaing ast elements! *) + (* EffectAction *) + (* { action = Features.On.monadic_action; argument = dummy_expr }; *) + (* Quote { contents = []; witness = Features.On.quote }; *) + ] + | GENERICS -> + [ + (fun () -> + ([%yojson_of: generics] { params = []; constraints = [] }, indexes)); + ] + | GLOBAL_IDENT -> + [ + (fun () -> + let c_ident, indexes = generate_helper CONCRETE_IDENT indexes in + (`List [ `String "Concrete"; c_ident ], indexes)); + ] + | PAT -> + let pat_shell v indexes = + let typ, indexes = generate_helper TY indexes in + ( `Assoc + [ + ("p", v); + ("span", `Assoc [ ("id", `Int 79902); ("data", `List []) ]); + ("typ", typ); + ], + indexes ) + in + List.map + ~f:(fun pat_f () -> + let pat', indexes = pat_f () in + pat_shell pat' indexes) + [ + (fun () -> ([%yojson_of: pat'] PWild, indexes)); + (fun () -> + let typ, indexes = generate_helper TY indexes in + let typ = [%of_yojson: ty] typ in + + let pat, indexes = generate_helper PAT indexes in + let pat = [%of_yojson: pat] pat in + ( [%yojson_of: pat'] + (PAscription { typ; typ_span = Span.dummy (); pat }), + indexes )); + (fun () -> + let g_ident, indexes = generate_helper GLOBAL_IDENT indexes in + let g_ident = [%of_yojson: global_ident] g_ident in + ( [%yojson_of: pat'] + (PConstruct + { + constructor = g_ident; + is_record = false; + is_struct = false; + fields = []; + }), + indexes )); + (fun () -> + let lhs_pat, indexes = generate_helper PAT indexes in + let lhs_pat = [%of_yojson: pat] lhs_pat in + + let rhs_pat, indexes = generate_helper PAT indexes in + let rhs_pat = [%of_yojson: pat] rhs_pat in + ( [%yojson_of: pat'] (POr { subpats = [ lhs_pat; rhs_pat ] }), + indexes )); + (fun () -> ([%yojson_of: pat'] (PArray { args = [] }), indexes)); + (fun () -> + let pat, indexes = generate_helper PAT indexes in + let pat = [%of_yojson: pat] pat in + + let wit = [%of_yojson: F.reference] (`String "Reference") in + + ( [%yojson_of: pat'] (PDeref { subpat = pat; witness = wit }), + indexes )); + (fun () -> + let lit, indexes = generate_helper LITERAL indexes in + let lit = [%of_yojson: literal] lit in + ([%yojson_of: pat'] (PConstant { lit }), indexes)); + (fun () -> + let l_ident, indexes = generate_helper LOCAL_IDENT indexes in + let l_ident = [%of_yojson: local_ident] l_ident in + + let typ, indexes = generate_helper TY indexes in + let typ = [%of_yojson: ty] typ in + + let wit = + [%of_yojson: F.mutable_variable] (`String "mutable_variable") + in + ( [%yojson_of: pat'] + (PBinding + { + mut = Mutable wit; + mode = ByValue; + var = l_ident; + typ; + subpat = None; + }), + indexes )); + ] + | LOCAL_IDENT -> + [ + (fun () -> + ( `Assoc + [ + ("name", `String "dummy"); + ("id", `List [ `List [ `String "Typ" ]; `Int 0 ]); + ], + indexes )); + ] + | IMPL_EXPR -> + [ + (fun () -> + let c_ident, indexes = generate_helper CONCRETE_IDENT indexes in + ( `Assoc + [ + ("kind", `List [ `String "Self" ]); + ("goal", `Assoc [ ("trait", c_ident); ("args", `List []) ]); + ], + indexes )); + ] + | ITEM -> + let item_shell v indexes = + let ident, indexes = generate_helper CONCRETE_IDENT indexes in + ( `Assoc + [ + ("v", v); + ("span", `Assoc [ ("id", `Int 79902); ("data", `List []) ]); + ("ident", ident); + ("attrs", `List []); + ], + indexes ) + in + List.map + ~f:(fun item_f () -> + let item', indexes = item_f () in + item_shell item' indexes) + [ + (fun () -> + let name, indexes = generate_helper CONCRETE_IDENT indexes in + let name = [%of_yojson: concrete_ident] name in + + let generics, indexes = generate_helper GENERICS indexes in + let generics = [%of_yojson: generics] generics in + + let body, indexes = generate_helper EXPR indexes in + let body = [%of_yojson: expr] body in + ( [%yojson_of: item'] + (Fn { name; generics; body; params = []; safety = Safe }), + indexes )); + (fun () -> + let name, indexes = generate_helper CONCRETE_IDENT indexes in + let name = [%of_yojson: concrete_ident] name in + + let generics, indexes = generate_helper GENERICS indexes in + let generics = [%of_yojson: generics] generics in + + let typ, indexes = generate_helper TY indexes in + let typ = [%of_yojson: ty] typ in + ( [%yojson_of: item'] (TyAlias { name; generics; ty = typ }), + indexes )); + (* enum *) + (fun () -> + let name, indexes = generate_helper CONCRETE_IDENT indexes in + let name = [%of_yojson: concrete_ident] name in + + let generics, indexes = generate_helper GENERICS indexes in + let generics = [%of_yojson: generics] generics in + ( [%yojson_of: item'] + (Type { name; generics; variants = []; is_struct = false }), + indexes )); + (* struct *) + (fun () -> + let name, indexes = generate_helper CONCRETE_IDENT indexes in + let name = [%of_yojson: concrete_ident] name in + + let generics, indexes = generate_helper GENERICS indexes in + let generics = [%of_yojson: generics] generics in + ( [%yojson_of: item'] + (Type { name; generics; variants = []; is_struct = true }), + indexes )); + (fun () -> + let macro, indexes = generate_helper CONCRETE_IDENT indexes in + let macro = [%of_yojson: concrete_ident] macro in + + let wit = [%of_yojson: F.macro] (`String "Macro") in + + ( [%yojson_of: item'] + (IMacroInvokation + { + macro; + argument = "TODO"; + span = Span.dummy (); + witness = wit; + }), + indexes )); + (fun () -> + let name, indexes = generate_helper CONCRETE_IDENT indexes in + let name = [%of_yojson: concrete_ident] name in + + let generics, indexes = generate_helper GENERICS indexes in + let generics = [%of_yojson: generics] generics in + ( [%yojson_of: item'] + (Trait { name; generics; items = []; safety = Safe }), + indexes )); + (fun () -> + let generics, indexes = generate_helper GENERICS indexes in + let generics = [%of_yojson: generics] generics in + + let ty, indexes = generate_helper TY indexes in + let ty = [%of_yojson: ty] ty in + + let c_ident, indexes = generate_helper CONCRETE_IDENT indexes in + let c_ident = [%of_yojson: concrete_ident] c_ident in + ( [%yojson_of: item'] + (Impl + { + generics; + self_ty = ty; + of_trait = (c_ident, []); + items = []; + parent_bounds = []; + safety = Safe; + }), + indexes )); + (fun () -> + let name, indexes = generate_helper CONCRETE_IDENT indexes in + let name = [%of_yojson: concrete_ident] name in + + let item, indexes = generate_helper CONCRETE_IDENT indexes in + let item = [%of_yojson: concrete_ident] item in + ([%yojson_of: item'] (Alias { name; item }), indexes)); + (fun () -> + ( [%yojson_of: item'] + (Use { path = []; is_external = false; rename = None }), + indexes )); + (* Quote { contents = []; witness = Features.On.quote }; *) + (* HaxError "dummy"; *) + (* NotImplementedYet; *) + ] + in + List.nth_exn cases i () + + let generate (t : ast_type) (indexes : int list) : Yojson.Safe.t = + fst (generate_helper t indexes) + + (* AST depth: + 0 is constants (no recursion), + 1 is the flat AST with each AST elements present, + inf is all possible expressions *) + let rec generate_depth depth (pre : int list) (t : ast_type) : int list list = + List.map + ~f:(fun l -> pre @ l) + (match t with + (* TODO: Base dummy values *) + | CONCRETE_IDENT -> [ [ 0 ] ] + | GLOBAL_IDENT -> + generate_depth_list_helper depth [ 0 ] [ CONCRETE_IDENT ] + | LOCAL_IDENT -> [ [ 0 ] ] + | IMPL_EXPR -> [ [ 0; 0 ] ] + | GENERICS -> [ [ 0 ] ] + (* Fully defined AST elements *) + | LITERAL -> + [ + (* String *) + [ 0 ]; + (* Char *) + [ 1 ]; + (* Int *) + [ 2 ]; + (* Float *) + [ 3 ]; + (* Bool *) + [ 4 ]; + ] + | TY -> ( + [ + (* TBool *) + [ 0 ]; + (* TChar *) + [ 1 ]; + (* TInt *) + [ 2 ]; + (* TFloat *) + [ 3 ]; + (* TStr *) + [ 4 ]; + ] + (* TApp *) + @ generate_depth_list_helper (depth - 1) [ 5 ] [ GLOBAL_IDENT; TY ] + (* TODO: Any number of extra ty args? *) + (* TArray *) + @ generate_depth_list_helper (depth - 1) [ 6 ] [ TY; EXPR ] + (* TSlice *) + @ (try + let _ = [%of_yojson: F.slice] (`String "Slice") in + generate_depth_list_helper (depth - 1) [ 7 ] [ TY ] + with _ -> []) + @ (try + let _ = [%of_yojson: F.raw_pointer] (`String "Raw_pointer") in + [ (* TRawPointer *) [ 8 ] ] + with _ -> []) + (* TRef *) + @ (try + let _ = [%of_yojson: F.reference] (`String "Reference") in + generate_depth_list_helper (depth - 1) [ 9 ] [ TY ] + with _ -> []) + (* TODO: mutable? *) + (* TParam *) + @ generate_depth_list_helper depth [ 10 ] [ LOCAL_IDENT ] + (* TArrow *) + @ generate_depth_list_helper (depth - 1) [ 11 ] [ TY ] + (* TAssociatedType *) + @ generate_depth_list_helper (depth - 1) [ 12 ] + [ IMPL_EXPR; CONCRETE_IDENT ] + (* TOpaque *) + @ generate_depth_list_helper (depth - 1) [ 13 ] [ CONCRETE_IDENT ] + @ + try + let _ = [%of_yojson: F.dyn] (`String "Dyn") in + [ (* TDyn *) [ 14 ] ] + with _ -> []) + | PAT -> + List.map + ~f:(fun x -> + x @ [ 0 ] + (* TODO: Append correct type, instead of dummy / guessing *)) + ([ (* PWild *) [ 0 ] ] + (* PAscription *) + @ generate_depth_list_helper (depth - 1) [ 1 ] [ TY; PAT ] + (* PConstruct *) + @ generate_depth_list_helper depth [ 2 ] [ GLOBAL_IDENT ] + (* POr *) + @ generate_depth_list_helper (depth - 1) [ 3 ] [ PAT; PAT ] + @ [ (* PArray *) [ 4 ] ] + (* PDeref *) + @ (try + let _ = [%of_yojson: F.reference] (`String "Reference") in + generate_depth_list_helper (depth - 1) [ 5 ] [ PAT ] + with _ -> []) + (* PConstant *) + @ generate_depth_list_helper depth [ 6 ] [ LITERAL ] + @ + (* PBinding *) + try + let _ = + [%of_yojson: F.mutable_variable] (`String "Mutable_variable") + in + generate_depth_list_helper (depth - 1) [ 7 ] [ LOCAL_IDENT; TY ] + with _ -> []) + | EXPR -> + List.map + ~f:(fun x -> + x @ [ 0 ] + (* TODO: Append correct type, instead of dummy / guessing *)) + ((* If *) + generate_depth_list_helper (depth - 1) [ 0 ] [ EXPR; EXPR ] + (*; expr3 *) + (* App *) + @ generate_depth_list_helper (depth - 1) [ 1 ] [ EXPR; EXPR ] + (* Literal *) + @ generate_depth_list_helper depth [ 2 ] [ LITERAL ] + @ [ (* Array *) [ 3 ] ] + (* Construct *) + @ generate_depth_list_helper (depth - 1) [ 4 ] [ GLOBAL_IDENT ] + (* Match *) + @ generate_depth_list_helper (depth - 1) [ 5 ] [ EXPR ] + (* Let *) + @ generate_depth_list_helper (depth - 1) [ 6 ] [ PAT; EXPR; EXPR ] + (* Block *) + @ (try + let _ = [%of_yojson: F.block] (`String "Block") in + generate_depth_list_helper (depth - 1) [ 7 ] [ EXPR ] + with _ -> []) + (* LocalVar *) + @ generate_depth_list_helper (depth - 1) [ 8 ] [ LOCAL_IDENT ] + (* GlobalVar *) + @ generate_depth_list_helper (depth - 1) [ 9 ] [ GLOBAL_IDENT ] + (* Ascription *) + @ generate_depth_list_helper (depth - 1) [ 10 ] [ EXPR; TY ] + (* MacroInvokation *) + @ (try + let _ = [%of_yojson: F.macro] (`String "Macro") in + generate_depth_list_helper (depth - 1) [ 11 ] [ GLOBAL_IDENT ] + with _ -> []) + (* Assign *) + @ (try + let _ = + [%of_yojson: F.mutable_variable] (`String "Mutable_variable") + in + generate_depth_list_helper (depth - 1) [ 12 ] + [ LOCAL_IDENT; EXPR; TY ] + with _ -> []) + (* Loop *) + @ (try + let _ = [%of_yojson: F.loop] (`String "Loop") in + generate_depth_list_helper (depth - 1) [ 13 ] [ EXPR ] + with _ -> []) + (* Break *) + @ (try + let _ = [%of_yojson: F.loop] (`String "Loop") in + let _ = [%of_yojson: F.break] (`String "Break") in + generate_depth_list_helper (depth - 1) [ 14 ] [ EXPR ] + with _ -> []) + (* Return *) + @ (try + let _ = [%of_yojson: F.early_exit] (`String "Early_exit") in + generate_depth_list_helper (depth - 1) [ 15 ] [ EXPR ] + with _ -> []) + (* QuestionMark *) + @ (try + let _ = + [%of_yojson: F.question_mark] (`String "Question_mark") + in + generate_depth_list_helper (depth - 1) [ 16 ] [ EXPR; TY ] + with _ -> []) + @ (try + let _ = [%of_yojson: F.loop] (`String "Loop") in + let _ = [%of_yojson: F.continue] (`String "Continue") in + [ (* Continue *) [ 17 ] ] + with _ -> []) + (* Borrow *) + @ (try + let _ = [%of_yojson: F.reference] (`String "Reference") in + generate_depth_list_helper (depth - 1) [ 18 ] [ EXPR ] + with _ -> []) + (* AddressOf *) + @ (try + let _ = [%of_yojson: F.raw_pointer] (`String "Raw_pointer") in + generate_depth_list_helper (depth - 1) [ 19 ] [ EXPR ] + with _ -> []) + @ (* Closure *) + generate_depth_list_helper (depth - 1) [ 20 ] [ EXPR ]) + | ITEM -> + List.concat_map + ~f:(fun x -> generate_depth_list_helper depth x [ CONCRETE_IDENT ]) + ((* Fn *) + generate_depth_list_helper (depth - 1) [ 0 ] + [ CONCRETE_IDENT; GENERICS; EXPR ] + (* TYAlias *) + @ generate_depth_list_helper (depth - 1) [ 1 ] + [ CONCRETE_IDENT; GENERICS; TY ] + (* TYpe *) + @ generate_depth_list_helper (depth - 1) [ 2 ] + [ CONCRETE_IDENT; GENERICS ] + (* TYpe *) + @ generate_depth_list_helper (depth - 1) [ 3 ] + [ CONCRETE_IDENT; GENERICS ] + (* IMacroInvokation *) + @ (try + let _ = [%of_yojson: F.macro] (`String "Macro") in + generate_depth_list_helper depth [ 4 ] [ CONCRETE_IDENT ] + with _ -> []) + (* Trait *) + @ generate_depth_list_helper (depth - 1) [ 5 ] + [ CONCRETE_IDENT; GENERICS ] + (* Impl *) + @ generate_depth_list_helper (depth - 1) [ 6 ] + [ GENERICS; TY; CONCRETE_IDENT ] + (* Alias *) + @ generate_depth_list_helper (depth - 1) [ 7 ] + [ CONCRETE_IDENT; CONCRETE_IDENT ] + @ [ (* Use *) [ 8 ] ])) + + and generate_depth_list depth (pre : int list) (t : ast_type list) : + int list list = + match t with + | [] -> [] + | [ x ] -> generate_depth depth pre x + | x :: xs -> + List.concat_map + ~f:(fun pre -> generate_depth_list depth pre xs) + (generate_depth depth pre x) + + and generate_depth_list_helper depth (pre : int list) (t : ast_type list) : + int list list = + if depth >= 0 then generate_depth_list depth pre t else [] + + let generate_literals () = + let literal_args = generate_depth 0 [] LITERAL in + List.map + ~f:(fun x -> [%of_yojson: literal] (generate LITERAL x)) + literal_args + + let generate_tys depth : ty list = + let ty_args = generate_depth depth [] TY in + List.map ~f:(fun x -> [%of_yojson: ty] (generate TY x)) ty_args + + let generate_pats depth = + let pat_args = generate_depth depth [] PAT in + List.map ~f:(fun x -> [%of_yojson: pat] (generate PAT x)) pat_args + + let generate_exprs depth = + let expr_args = generate_depth depth [] EXPR in + List.map ~f:(fun x -> [%of_yojson: expr] (generate EXPR x)) expr_args + + let generate_items depth = + let item_args = generate_depth depth [] ITEM in + List.map ~f:(fun x -> [%of_yojson: item] (generate ITEM x)) item_args + + let rec flatten (l : int list list) : int list list = + match l with + | (x :: xs) :: (y :: ys) :: ls -> + (if phys_equal x y then [] else [ x :: xs ]) @ flatten ((y :: ys) :: ls) + | _ -> l + + let generate_flat_literals () = + let literal_args = flatten (generate_depth 0 [] LITERAL) in + List.map + ~f:(fun x -> [%of_yojson: literal] (generate LITERAL x)) + literal_args + + let generate_flat_tys () : ty list = + let ty_args = flatten (generate_depth 1 [] TY) in + List.map ~f:(fun x -> [%of_yojson: ty] (generate TY x)) ty_args + + let generate_flat_pats () = + let pat_args = flatten (generate_depth 1 [] PAT) in + List.map ~f:(fun x -> [%of_yojson: pat] (generate PAT x)) pat_args + + let generate_flat_exprs () = + let expr_args = flatten (generate_depth 1 [] EXPR) in + List.map ~f:(fun x -> [%of_yojson: expr] (generate EXPR x)) expr_args + + let generate_flat_items () = + let item_args = flatten (generate_depth 1 [] ITEM) in + List.map ~f:(fun x -> [%of_yojson: item] (generate ITEM x)) item_args + + let generate_full_ast () : + literal list * ty list * pat list * expr list * item list = + let my_literals = generate_flat_literals () in + let my_tys = generate_flat_tys () in + let my_pats = generate_flat_pats () in + let my_exprs = generate_flat_exprs () in + let my_items = generate_flat_items () in + (my_literals, my_tys, my_pats, my_exprs, my_items) +end diff --git a/engine/lib/backend.ml b/engine/lib/backend.ml index 0dfb6ea26..f29d8c626 100644 --- a/engine/lib/backend.ml +++ b/engine/lib/backend.ml @@ -78,7 +78,7 @@ module Make (InputLanguage : Features.T) (M : BackendMetadata) = struct ("[TODO: this error uses failwith, and thus leads to bad error \ messages, please update it using [Diagnostics.*] helpers] " ^ msg) span - [@@ocaml.deprecated - "Use more precise errors: Error.unimplemented, Error.assertion_failure \ - or a raw Error.t (with Error.raise)"] + (* [@@ocaml.deprecated *) + (* "Use more precise errors: Error.unimplemented, Error.assertion_failure \ *) + (* or a raw Error.t (with Error.raise)"] *) end diff --git a/engine/utils/sourcemaps/source_maps.ml b/engine/utils/sourcemaps/source_maps.ml index 6da383baa..64f2aa3fb 100644 --- a/engine/utils/sourcemaps/source_maps.ml +++ b/engine/utils/sourcemaps/source_maps.ml @@ -1,4 +1,5 @@ open Prelude +open Ppx_yojson_conv_lib.Yojson_conv.Primitives module Location = Location include Mappings diff --git a/hax-lib-macros/src/lib.rs b/hax-lib-macros/src/lib.rs index a69da2fce..ddabc5d59 100644 --- a/hax-lib-macros/src/lib.rs +++ b/hax-lib-macros/src/lib.rs @@ -381,6 +381,28 @@ pub fn ensures(attr: pm::TokenStream, item: pm::TokenStream) -> pm::TokenStream .into() } +/// Exclude this item from the Hax translation. +#[proc_macro_error] +#[proc_macro_attribute] +pub fn interface(attr: pm::TokenStream, item: pm::TokenStream) -> pm::TokenStream { + let item: ItemFn = parse_macro_input!(item); + let ItemFn { + // The function signature + sig, + // The visibility specifier of this function + vis, + // The function block or body + block, + // Other attributes applied to this function + attrs, + } = item.clone(); + + quote! { + #(#attrs)* #vis #sig { todo!() } + } + .into() +} + mod kw { syn::custom_keyword!(hax_lib); syn::custom_keyword!(decreases); diff --git a/hax-lib/src/proc_macros.rs b/hax-lib/src/proc_macros.rs index 866c7cfda..b54ba3d5c 100644 --- a/hax-lib/src/proc_macros.rs +++ b/hax-lib/src/proc_macros.rs @@ -2,8 +2,8 @@ //! proc-macro crate cannot export anything but procedural macros. pub use hax_lib_macros::{ - attributes, ensures, exclude, impl_fn_decoration, include, lemma, loop_invariant, opaque_type, - refinement_type, requires, trait_fn_decoration, + attributes, ensures, exclude, impl_fn_decoration, include, interface, lemma, loop_invariant, + opaque_type, refinement_type, requires, trait_fn_decoration, }; pub use hax_lib_macros::{ diff --git a/hax-types/src/cli_options/mod.rs b/hax-types/src/cli_options/mod.rs index 4f275606a..98348dadf 100644 --- a/hax-types/src/cli_options/mod.rs +++ b/hax-types/src/cli_options/mod.rs @@ -356,6 +356,10 @@ pub enum Command { #[clap(name = "into")] Backend(BackendOptions), + /// Generate AST and print it as an EBNF formula + #[clap(name = "generate-ast")] + GenerateAST, + /// Export directly as a JSON file JSON { /// Path to the output JSON file, "-" denotes stdout. diff --git a/hax-types/src/diagnostics/message.rs b/hax-types/src/diagnostics/message.rs index 2a94c0b56..651722d34 100644 --- a/hax-types/src/diagnostics/message.rs +++ b/hax-types/src/diagnostics/message.rs @@ -23,6 +23,9 @@ pub enum HaxMessage { WarnExperimentalBackend { backend: Backend<()>, } = 4, + AstPrinterNotFound { + is_opam_setup_correctly: bool, + } = 5, } impl HaxMessage {