Skip to content

Commit ebef3ac

Browse files
authored
Refactor cil (#28)
1 parent a934935 commit ebef3ac

File tree

7 files changed

+293
-95
lines changed

7 files changed

+293
-95
lines changed

README.md

Lines changed: 47 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,50 @@
1+
[![Build](https://github.com/Inferara/inference/actions/workflows/build.yml/badge.svg?branch=main)](https://github.com/Inferara/inference/actions/workflows/build.yml)
2+
13
# Inference
24

35
🌀 Inference programming language [specification](https://github.com/Inferara/inference-language-spec)
6+
7+
## Inference Compiler CLI (`infc`)
8+
9+
`infc` drives the compilation pipeline for a single `.inf` source file. Phases are:
10+
11+
1. Parse (`--parse`) – build the typed AST.
12+
2. Analyze (`--analyze`) – perform semantic/type inference (WIP).
13+
3. Codegen (`--codegen`) – emit WebAssembly and optionally translate to V when `-o` is supplied.
14+
15+
You must specify at least one phase flag; requested phases run in canonical order.
16+
17+
### Basic usage
18+
19+
```bash
20+
cargo run -p inference-cli -- infc path/to/file.inf --parse
21+
```
22+
23+
After building you can call the binary directly:
24+
25+
```bash
26+
./target/debug/infc path/to/file.inf --parse --codegen -o
27+
```
28+
29+
### Show version
30+
31+
```bash
32+
infc --version
33+
```
34+
35+
### Output artifacts
36+
37+
Artifacts are written to an `out/` directory relative to the working directory. Rocq translation output is `out/out.v`.
38+
39+
### Exit codes
40+
41+
| Code | Meaning |
42+
|------|---------------------------------|
43+
| 0 | Success |
44+
| 1 | Usage / IO / Parse failure |
45+
46+
## Roadmap
47+
48+
* [Base type checker](https://github.com/Inferara/inference/issues/26)
49+
* Additional output formats.
50+
* [Linker](https://github.com/Inferara/inference/issues/9)

ast/src/builder.rs

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -33,6 +33,8 @@ impl BuilderInit for InitState {}
3333
pub struct CompleteState;
3434
impl BuilderComplete for CompleteState {}
3535

36+
pub type CompletedBuilder<'a> = Builder<'a, CompleteState>;
37+
3638
#[allow(dead_code)]
3739
pub struct Builder<'a, S> {
3840
arena: Arena,

cli/Cargo.toml

Lines changed: 10 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -7,8 +7,17 @@ homepage = { workspace = true }
77
repository = { workspace = true }
88

99
[dependencies]
10-
clap = { version = "4.5.50", features = ["derive"] }
10+
clap = { version = "4.5.51", features = ["derive"] }
1111
walkdir = "2.5.0"
1212
tempfile = "3.23.0"
1313
anyhow.workspace = true
1414
inference.workspace = true
15+
16+
[dev-dependencies]
17+
assert_cmd = "2.1.1"
18+
predicates = "3.1.3"
19+
assert_fs = "1.1.1"
20+
21+
[[bin]]
22+
name = "infc"
23+
path = "src/main.rs"

cli/src/main.rs

Lines changed: 93 additions & 87 deletions
Original file line numberDiff line numberDiff line change
@@ -1,122 +1,128 @@
11
#![warn(clippy::pedantic)]
22

3-
//! # Inference Compiler
3+
//! # Inference Compiler CLI
44
//!
5-
//! This is the entry point for the Inference compiler, which provides functionality to parse and
6-
//! translate `.inf` source files into Coq code (`.v` files).
5+
//! Command line interface for the Inference toolchain.
76
//!
8-
//! ## Modules
7+
//! 1. Parse (`--parse`) – build the typed AST.
8+
//! 2. Analyze (`--analyze`) – perform type / semantic inference and validation.
9+
//! 3. Codegen (`--codegen`) – emit WebAssembly, and optionally translate to V (`-o`).
910
//!
10-
//! - `ast`: Contains types and builders for constructing the AST from parsed source `.inf` files.
11-
//! - `cli`: Contains the command-line interface (CLI) parsing logic using the `clap` crate.
12-
//! - `wasm_to_coq_translator`: Handles the translation of WebAssembly (`.wasm`) files to Coq code (`.v` files).
11+
//! At least one of the phase flags must be supplied; the phases that are requested will be
12+
//! executed in the canonical order even if specified out of order on the command line.
1313
//!
14-
//! ## Main Functionality
14+
//! Output artifacts are written to an `out/` directory relative to the current working directory.
15+
//! When `-o` is passed together with `--codegen` the produced WASM module is further translated
16+
//! into V source and saved as `out/out.v`.
1517
//!
16-
//! The main function parses command-line arguments to determine the operation mode:
18+
//! ## Exit codes
19+
//! * 0 – success.
20+
//! * 1 – usage / IO / phase failure.
1721
//!
18-
//! - If the `--wasm` flag is provided, the program will translate the specified `.wasm` file into `.v` code.
19-
//! - Otherwise, the program will parse the specified `.inf` source file and generate an AST.
22+
//! ## Example
23+
//! ```bash
24+
//! infc examples/hello.inf --codegen -o
25+
//! ```
2026
//!
21-
//! ### Functions
22-
//!
23-
//! - `main`: The entry point of the program. Handles argument parsing and dispatches to the appropriate function
24-
//! based on the provided arguments. It handles parses specified in the first CLI argument
25-
//! and saves the request to the `out/` directory.
26-
//!
27-
//! ### Tests
28-
//!
29-
//! The `test` suite is located in the `main_tests` module and contains tests for the main functionality
27+
//! ## Tests
28+
//! Integration tests exercise flag validation and the happy path compilation pipeline.
3029
3130
mod parser;
3231
use clap::Parser;
33-
use inference::{compile_to_wat, wasm_to_v, wat_to_wasm};
32+
use inference::{analyze, codegen, parse, wasm_to_v};
3433
use parser::Cli;
3534
use std::{
3635
fs,
3736
path::PathBuf,
3837
process::{self},
3938
};
4039

41-
/// Inference compiler entry point
40+
/// Entry point for the CLI executable.
4241
///
43-
/// This function parses the command-line arguments to determine whether to parse an `.inf` source file
44-
/// or translate a `.wasm` file into Coq code. Depending on the `--wasm` flag, it either invokes the
45-
/// `wasm_to_coq` function or the `parse_file` function.
42+
/// Responsibilities:
43+
/// * Parse flags.
44+
/// * Validate that the input path exists and at least one phase is selected.
45+
/// * Run requested phases (parse -> analyze -> codegen).
46+
/// * Optionally translate emitted WASM into V source when `-o` is set.
47+
///
48+
/// On any failure a diagnostic is printed to stderr and the process exits with code `1`.
4649
fn main() {
4750
let args = Cli::parse();
4851
if !args.path.exists() {
4952
eprintln!("Error: path not found");
5053
process::exit(1);
5154
}
5255

53-
let output_path = match args.output {
54-
Some(path) => {
55-
if !path.exists() {
56-
fs::create_dir_all(&path).expect("Error creating output directory");
56+
let output_path = PathBuf::from("out");
57+
let need_parse = args.parse;
58+
let need_analyze = args.analyze;
59+
let need_codegen = args.codegen;
60+
61+
if !(need_parse || need_analyze || need_codegen) {
62+
eprintln!("Error: at least one of --parse, --analyze, or --codegen must be specified");
63+
process::exit(1);
64+
}
65+
66+
let source_code = fs::read_to_string(&args.path).expect("Error reading source file");
67+
let mut t_ast = None;
68+
if need_codegen || need_analyze || need_parse {
69+
match parse(source_code.as_str()) {
70+
Ok(ast) => {
71+
println!("Parsed: {}", args.path.display());
72+
t_ast = Some(ast);
73+
}
74+
Err(e) => {
75+
eprintln!("Parse error: {e}");
76+
process::exit(1);
5777
}
58-
path
5978
}
60-
None => PathBuf::from("out"),
61-
};
62-
let generate = match args.generate {
63-
Some(g) => match g.as_str().to_lowercase().as_str() {
64-
"wat" => "wat",
65-
"wasm" => "wasm",
66-
"f" | "full" => "f",
67-
_ => "v",
68-
},
69-
None => "v",
70-
};
71-
let source = match args.source {
72-
Some(s) => match s.as_str().to_lowercase().as_str() {
73-
"wat" => "wat",
74-
//"wasm" => "wasm",
75-
_ => "inf",
76-
},
77-
None => "inf",
78-
};
79-
let source_code = fs::read_to_string(&args.path).expect("Error reading source file");
80-
let wat = if source == "inf" {
81-
compile_to_wat(source_code.as_str()).unwrap()
82-
} else {
83-
source_code
84-
};
85-
if generate == "wat" {
86-
let wat_file_path = output_path.join("out.wat");
87-
fs::write(wat_file_path.clone(), wat).expect("Error writing WAT file");
88-
println!("WAT generated at: {}", wat_file_path.to_str().unwrap());
89-
process::exit(0);
9079
}
91-
let wasm = wat_to_wasm(wat.as_str()).unwrap();
92-
if generate == "wasm" {
93-
let wasm_file_path = output_path.join("out.wasm");
94-
fs::write(wasm_file_path.clone(), wasm).expect("Error writing WASM file");
95-
println!("WASM generated at: {}", wasm_file_path.to_str().unwrap());
96-
process::exit(0);
97-
}
98-
let mod_name = args.path.file_stem().unwrap().to_str().unwrap().to_string();
99-
let v = wasm_to_v(mod_name.as_str(), &wasm).unwrap();
100-
if generate == "v" {
101-
let v_file_path = output_path.join("out.v");
102-
fs::write(v_file_path.clone(), v).expect("Error writing V file");
103-
println!("V generated at: {}", v_file_path.to_str().unwrap());
104-
process::exit(0);
80+
81+
let Some(t_ast) = t_ast else {
82+
unreachable!("Phase validation guarantees parse ran when required");
83+
};
84+
85+
if need_codegen || need_analyze {
86+
if let Err(e) = analyze(&t_ast) {
87+
eprintln!("Analysis failed: {e}");
88+
process::exit(1);
89+
}
90+
println!("Analyzed: {}", args.path.display());
10591
}
106-
if generate == "f" {
107-
let v_file_path = output_path.join("out.v");
108-
fs::write(v_file_path.clone(), v).expect("Error writing V file");
109-
println!("V generated at: {}", v_file_path.to_str().unwrap());
110-
let wat_file_path = output_path.join("out.wat");
111-
fs::write(wat_file_path.clone(), wat).expect("Error writing WAT file");
112-
println!("WAT generated at: {}", wat_file_path.to_str().unwrap());
113-
let wasm_file_path = output_path.join("out.wasm");
114-
fs::write(wasm_file_path.clone(), wasm).expect("Error writing WASM file");
115-
println!("WASM generated at: {}", wasm_file_path.to_str().unwrap());
116-
process::exit(0);
92+
93+
if need_codegen {
94+
let wasm = match codegen(t_ast) {
95+
Ok(w) => w,
96+
Err(e) => {
97+
eprintln!("Codegen failed: {e}");
98+
process::exit(1);
99+
}
100+
};
101+
println!("WASM generated");
102+
if args.generate_v_output {
103+
let mod_name = args
104+
.path
105+
.file_stem()
106+
.unwrap_or_else(|| std::ffi::OsStr::new("module"))
107+
.to_str()
108+
.unwrap();
109+
match wasm_to_v(mod_name, &wasm) {
110+
Ok(v_output) => {
111+
let v_file_path = output_path.join("out.v");
112+
if let Err(e) = fs::write(&v_file_path, v_output) {
113+
eprintln!("Failed to write V file: {e}");
114+
process::exit(1);
115+
}
116+
println!("V generated at: {}", v_file_path.to_string_lossy());
117+
}
118+
Err(e) => {
119+
eprintln!("WASM->V translation failed: {e}");
120+
process::exit(1);
121+
}
122+
}
123+
}
117124
}
118-
eprintln!("Error: invalid generate option");
119-
process::exit(1);
125+
process::exit(0);
120126
}
121127

122128
#[cfg(test)]

cli/src/parser.rs

Lines changed: 21 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1,12 +1,27 @@
11
use clap::Parser;
22

33
#[derive(Parser)]
4+
#[command(
5+
author,
6+
version,
7+
about = "Inference compiler CLI (infc)",
8+
long_about = "The 'infc' command runs one or more compilation phases over a single .inf source file. \
9+
Parse builds the typed AST; analyze performs semantic/type inference; codegen emits WASM and can translate to V when -o is supplied."
10+
)]
11+
#[allow(clippy::struct_excessive_bools)] // CLI flag aggregation; bools are fine here.
412
pub(crate) struct Cli {
13+
// Path to the source file (later should support pointing to the project file infp)
514
pub(crate) path: std::path::PathBuf,
6-
#[clap(short = 'g', long = "generate", required = false)]
7-
pub(crate) generate: Option<String>,
8-
#[clap(short = 's', long = "source", required = false)]
9-
pub(crate) source: Option<String>,
10-
#[clap(short = 'o', long = "output", required = false)]
11-
pub(crate) output: Option<std::path::PathBuf>,
15+
// Runs source parsing and AST building, exit with 0 if successful
16+
#[clap(long = "parse", action = clap::ArgAction::SetTrue)]
17+
pub(crate) parse: bool,
18+
// Runs type checking, exit with 0 if successful
19+
#[clap(long = "analyze", action = clap::ArgAction::SetTrue)]
20+
pub(crate) analyze: bool,
21+
// Runs code generation, exit with 0 if successful
22+
#[clap(long = "codegen", action = clap::ArgAction::SetTrue)]
23+
pub(crate) codegen: bool,
24+
// Generates output .v files
25+
#[clap(short = 'o', action = clap::ArgAction::SetTrue)]
26+
pub(crate) generate_v_output: bool,
1227
}

0 commit comments

Comments
 (0)