Document valid CFG for Hax

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 ";"
+```

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<EmitHaxMetaMessage>) -> 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
+        }
     }
 }