diff --git a/.gitignore b/.gitignore index 67f1b67..1e08d15 100644 --- a/.gitignore +++ b/.gitignore @@ -21,3 +21,8 @@ result-* # Agda compiled interface files (generated by typecheck runs) *.agdai + +# Idris2 compiled output (generated by `idris2 --check` runs) +build/ +*.ttc +*.ttm diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml index 3725dc8..7d4d376 100644 --- a/.machine_readable/6a2/STATE.a2ml +++ b/.machine_readable/6a2/STATE.a2ml @@ -44,7 +44,7 @@ milestones = [ { name = "M1: Backend trait (Assistant|Solver kinds; Outcome/Verdict); agda.rs -> prover/agda.rs; graph/dag take &dyn Backend (pure refactor, 50 tests stay green)", completion = 100 }, { name = "M2: Cubical-Agda variant (Agda::cubical(), --cubical --safe island)", completion = 0 }, { name = "M3: Flying-Logic reasoning graph (src/reason: And|Or juncts, demote-only cycle-safe Verdict propagation, additive studio JSON)", completion = 100 }, - { name = "M4: Idris2 adapter (core/ABI language: .ipkg/--check/totality; escape-hatches)", completion = 0 }, + { name = "M4: Idris2 adapter (core/ABI language: .ipkg/--check/totality; escape-hatches)", completion = 90 }, { name = "M5: SMT solver backends (Z3, CVC5): SMT-LIB2 -> sat/unsat/unknown -> Verdict", completion = 0 }, { name = "M6: Lean4 adapter (lake build + #print axioms audit)", completion = 0 }, { name = "M7: Echidna dispatch seam (optional route to orchestrator :8090, same Outcome)", completion = 0 }, @@ -60,6 +60,22 @@ milestones = [ # Remaining M0: `arghda doctor` Rust subcommand (interim: `just doctor` shells # the script's --verify-only table). # +# M4 landed 2026-07-01 (90%): the Idris2 backend — arghda is now genuinely +# multi-backend. src/prover/idris2.rs: `idris2 --check --source-dir +# ` (ground-truthed vs Idris2 0.7.0), exit-code-only verdict; dotted +# module names reuse graph::module_name_of; .idr module_to_path; Idris2 import +# parser (`import [public] Mod [as Alias]`, top-level — no `open`); Main.idr +# root discovery. src/lint/idris2.rs: Idris2EscapeHatch (believe_me/assert_total +# /assert_smaller/idris_crash + `%default partial`), named "escape-hatch" so it +# reuses the reason-graph amber cap. WIRED via a new `--backend agda|idris2` CLI +# selector on scan/check/dag/reason (backend_for()); unknown backend errors +# cleanly. 93 tests (70 lib + 23 integration; +9 Idris2 unit +3 Idris2 +# integration; the graph/dag/reason tests are hermetic — text parsing, no binary +# needed). Dogfooded with REAL idris2 on PATH: `check --backend idris2` → +# proven-eligible; `reason --backend idris2 --check` → live typechecks, Main cone +# proven+wired, Orphan proven-but-unwired. Follow-ons (the missing 10%): +# .ipkg-declared roots, totality-hole (`?name`) + per-def `partial` lint. +# # M3 landed 2026-07-01: the Flying-Logic reasoning graph (src/reason/) — the # headline capability. Wraps DagDocument verbatim (ReasonDocument.dag) + adds a # per-node Verdict, And|Or edge juncts, and a memoised, cycle-safe, DEMOTE-ONLY @@ -104,10 +120,10 @@ milestones = [ [critical-next-actions] actions = [ - "M1 (Backend trait) + M3 (reasoning graph) DONE. Next, all unblocked by the stable trait — pick per priority:", - "Flying-Logic epic M4: Idris2 adapter (core/ABI language: .ipkg/--check/totality; believe_me/assert_total/%partial escape-hatches) — Idris2 v0.7.0 is provisioned.", - "Flying-Logic epic M5: SMT solver backends (Z3, CVC5) — the Solver kind; SMT-LIB2 -> sat(Refuted)/unsat(Proven)/unknown(Unknown). Both binaries are provisioned.", + "M1 (Backend trait) + M3 (reasoning graph) + M4 (Idris2) DONE. Next, all unblocked by the stable trait + --backend selector:", + "Flying-Logic epic M5: SMT solver backends (Z3, CVC5) — the FIRST Solver-kind backend; SMT-LIB2 -> unsat(Proven)/sat(Refuted)/unknown(Unknown). Both binaries provisioned. Exercises the Solver half of the taxonomy (no imports; isolated nodes).", "Flying-Logic epic M2: Cubical-Agda variant (Agda::cubical(), --cubical --safe island; cross-flag import edges forbidden).", + "M4 follow-on (the missing 10%): .ipkg-declared roots; totality-hole (?name) + per-def `partial` lint.", "M3 follow-on: feed real verdicts into `reason` from a workspace `proven/` state + wire staleness from the content-hash closure (proven.rs) so `arghda reason ` lights the cone without --check.", "Finish M0: add the `arghda doctor` Rust subcommand and repoint `just doctor` at it (interim shells provision-provers.sh --verify-only).", "Serve /.well-known/groove for PanLL discovery (Groove protocol) — folds into M11.", @@ -119,10 +135,11 @@ last-result = "pass" # unknown | pass | warn | fail open-warnings = 0 open-failures = 0 # `just check` (fmt-check + clippy -D warnings + build + test + SPDX) green -# post-M3: 61 lib + 20 integration = 81 tests pass. Dogfooded via real CLI -# runs: `dag` JSON byte-compatible; `check` + `reason --check` ran real agda -# typechecks (proven-eligible / all-Proven+wired cone). Dogfooded historically -# against echo-types + agda-unused. +# post-M4: 70 lib + 23 integration = 93 tests pass. Dogfooded via real CLI +# runs on BOTH backends: agda (`check`/`reason --check`) and idris2 (`check +# --backend idris2` → proven-eligible; `reason --backend idris2 --check` → +# live-typechecked cone). Dogfooded historically against echo-types + +# agda-unused. [ecosystem] part-of = ["arghda"] diff --git a/src/lib.rs b/src/lib.rs index 10b8905..f1d00a0 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -30,6 +30,6 @@ pub use diagnostic::{Diagnostic, LintReport, Severity}; pub use event::{Event, EventKind}; pub use graph::{build as build_graph, ImportGraph}; pub use lint::{default_rules, rules_with_config, run_lints, LintRule, RuleConfig}; -pub use prover::{default_backend, Agda, Backend, BackendKind, Outcome, Verdict}; +pub use prover::{default_backend, Agda, Backend, BackendKind, Idris2, Outcome, Verdict}; pub use reason::{build as build_reason, Junct, ReasonDocument, ReasonEdge, ReasonNode}; pub use workspace::{StaleEntry, State, Workspace}; diff --git a/src/lint/idris2.rs b/src/lint/idris2.rs new file mode 100644 index 0000000..36fb28c --- /dev/null +++ b/src/lint/idris2.rs @@ -0,0 +1,140 @@ +// SPDX-License-Identifier: MPL-2.0 +// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) + +//! Idris2 `escape-hatch` (warn) — surface soundness escape hatches. +//! +//! The Idris2 analogue of the Agda [`super::escape_hatch::EscapeHatch`]. It +//! shares the rule *name* `escape-hatch` deliberately: the reasoning graph +//! (`crate::reason`) caps any `escape-hatch` node at amber, so a `believe_me` +//! in Idris2 and a `believe_me` in Agda get the same honest treatment. +//! +//! Flags the Idris2 trust/escape primitives `believe_me`, `assert_total`, +//! `assert_smaller`, `idris_crash`, and the `%default partial` directive. +//! Idris2 `--check` exits 0 even when these are present, so without this rule +//! they would silently ride along in an otherwise-green verdict — exactly the +//! silent-failure class arghda exists to surface. Totality holes (`?name`) +//! and per-def `partial` modifiers are a documented follow-on. + +use super::{LintContext, LintRule}; +use crate::diagnostic::{Diagnostic, LintReport, Severity}; +use anyhow::{Context, Result}; +use std::fs; +use std::path::Path; + +pub struct Idris2EscapeHatch; + +const ESCAPE_TOKENS: &[&str] = &[ + "believe_me", + "assert_total", + "assert_smaller", + "idris_crash", +]; + +impl LintRule for Idris2EscapeHatch { + fn name(&self) -> &'static str { + // Shared with the Agda rule on purpose — the reasoning graph's + // lint→verdict cap keys on this name. + "escape-hatch" + } + + fn run(&self, file: &Path, _ctx: &LintContext<'_>, report: &mut LintReport) -> Result<()> { + let contents = + fs::read_to_string(file).with_context(|| format!("reading {}", file.display()))?; + for (i, line) in contents.lines().enumerate() { + let trimmed = line.trim_start(); + if trimmed.starts_with("--") { + continue; // whole-line comment + } + // The `%default partial` directive turns off totality checking. + if trimmed.starts_with("%default") && trimmed.contains("partial") { + report.push(warn( + self.name(), + file, + i + 1, + "totality escape directive `%default partial`".to_string(), + )); + } + // Trust/escape primitives, ignoring any trailing line comment. + let code = line.split(" --").next().unwrap_or(line); + for tok in ESCAPE_TOKENS { + if has_token(code, tok) { + report.push(warn( + self.name(), + file, + i + 1, + format!("escape primitive `{tok}`"), + )); + } + } + } + Ok(()) + } +} + +fn warn(rule: &str, file: &Path, line: usize, message: String) -> Diagnostic { + Diagnostic { + rule: rule.to_string(), + severity: Severity::Warn, + file: file.to_path_buf(), + message, + line: Some(line), + } +} + +/// `tok` appears in `s` as a delimited token (so `assert_totally` or +/// `believe_me_helper` do not match). +fn has_token(s: &str, tok: &str) -> bool { + s.split(|c: char| c.is_whitespace() || "(){};,".contains(c)) + .any(|w| w == tok) +} + +#[cfg(test)] +mod tests { + use super::*; + use crate::lint::run_lints; + use std::path::PathBuf; + + fn lint_str(body: &str) -> LintReport { + let tmp = tempfile::NamedTempFile::new().unwrap(); + std::fs::write(tmp.path(), body).unwrap(); + let roots: [PathBuf; 0] = []; + let ctx = LintContext { + include_root: tmp.path().parent().unwrap(), + entry_modules: &roots, + }; + let rules: Vec> = vec![Box::new(Idris2EscapeHatch)]; + run_lints(tmp.path(), &ctx, &rules).unwrap() + } + + #[test] + fn believe_me_is_warned_under_the_escape_hatch_name() { + let r = lint_str("module M\n\nx : Nat\nx = believe_me 0\n"); + assert_eq!(r.warns().count(), 1); + assert_eq!(r.diagnostics[0].rule, "escape-hatch"); + assert!(r.diagnostics[0].message.contains("believe_me")); + } + + #[test] + fn assert_total_and_default_partial_are_warned() { + let r = lint_str("%default partial\n\nf : Nat -> Nat\nf x = assert_total (f x)\n"); + assert_eq!(r.warns().count(), 2); + } + + #[test] + fn escape_token_in_comment_is_ignored() { + let r = lint_str("module M\n\nx : Nat\nx = 0 -- avoid believe_me here\n"); + assert!(r.diagnostics.is_empty()); + } + + #[test] + fn longer_identifier_does_not_match() { + let r = lint_str("module M\n\nbelieve_me_helper : Nat\nbelieve_me_helper = 0\n"); + assert!(r.diagnostics.is_empty()); + } + + #[test] + fn clean_idris_file_is_silent() { + let r = lint_str("module M\n\ngreeting : String\ngreeting = \"hi\"\n"); + assert!(r.diagnostics.is_empty()); + } +} diff --git a/src/lint/mod.rs b/src/lint/mod.rs index 63f2e67..47f9471 100644 --- a/src/lint/mod.rs +++ b/src/lint/mod.rs @@ -6,6 +6,7 @@ use anyhow::Result; use std::path::{Path, PathBuf}; pub mod escape_hatch; +pub mod idris2; pub mod orphan_module; pub mod postulate; pub mod safe_pragma; diff --git a/src/main.rs b/src/main.rs index b202a79..c8aef49 100644 --- a/src/main.rs +++ b/src/main.rs @@ -4,7 +4,7 @@ use anyhow::{Context, Result}; use arghda_core::lint::LintContext; use arghda_core::{ - build_dag, build_reason, event, run_lints, unused, watcher, Agda, Backend, LintRule, + build_dag, build_reason, event, run_lints, unused, watcher, Agda, Backend, Idris2, LintRule, RuleConfig, State, Workspace, }; use clap::{Parser, Subcommand}; @@ -15,11 +15,21 @@ use walkdir::WalkDir; /// A lint pack (boxed trait objects). type RuleSet = Vec>; +/// Resolve a `--backend` name to a backend instance. Agda is the default and +/// v0.1 reference; Idris2 is the estate ABI language. +fn backend_for(name: &str) -> Result> { + match name { + "agda" => Ok(Box::new(Agda)), + "idris2" => Ok(Box::new(Idris2)), + other => anyhow::bail!("unknown backend `{other}` (known: agda, idris2)"), + } +} + #[derive(Parser)] #[command( name = "arghda", version, - about = "Proof-workspace manager (Agda, v0.1)" + about = "Proof-workspace manager for provers/solvers (Agda, Idris2)" )] struct Cli { #[command(subcommand)] @@ -46,6 +56,9 @@ enum Cmd { /// `/.arghda/config.toml` if present. #[arg(long)] config: Option, + /// Prover/solver backend to use: `agda` (default) or `idris2`. + #[arg(long, default_value = "agda")] + backend: String, /// Also run the external `agda-unused` analyser and re-emit its /// findings as `unused-import` warnings (requires `agda-unused` on /// PATH; skipped with a note if absent). @@ -55,13 +68,16 @@ enum Cmd { #[arg(long)] json: bool, }, - /// Typecheck one file with Agda and lint it; report the verdict. + /// Typecheck one file with the backend and lint it; report the verdict. Check { - /// The `.agda` file to check. + /// The source file to check. file: PathBuf, - /// Agda include root. Defaults to the file's directory. + /// Include root (search path). Defaults to the file's directory. #[arg(long)] include_root: Option, + /// Prover/solver backend to use: `agda` (default) or `idris2`. + #[arg(long, default_value = "agda")] + backend: String, /// Emit the report as JSON. #[arg(long)] json: bool, @@ -82,6 +98,9 @@ enum Cmd { /// `/.arghda/config.toml` if present. #[arg(long)] config: Option, + /// Prover/solver backend to use: `agda` (default) or `idris2`. + #[arg(long, default_value = "agda")] + backend: String, }, /// Emit the Flying-Logic reasoning graph (JSON) for the tree at PATH: /// the DAG plus a demote-only verdict propagation. Without `--check`, @@ -102,6 +121,9 @@ enum Cmd { /// `/.arghda/config.toml` if present. #[arg(long)] config: Option, + /// Prover/solver backend to use: `agda` (default) or `idris2`. + #[arg(long, default_value = "agda")] + backend: String, /// Run the backend on every node to populate REAL prover verdicts /// (honest exit codes). Slower — typechecks each module. Off by /// default, in which case clean nodes are `unknown`. @@ -143,6 +165,7 @@ fn main() -> Result<()> { entry, headline_pattern, config, + backend, unused, json, } => scan( @@ -150,36 +173,42 @@ fn main() -> Result<()> { &entry, headline_pattern.as_deref(), config.as_deref(), + &backend, unused, json, )?, Cmd::Check { file, include_root, + backend, json, - } => check(&file, include_root.as_deref(), json)?, + } => check(&file, include_root.as_deref(), &backend, json)?, Cmd::Dag { path, entry, headline_pattern, config, + backend, } => dag( &path, &entry, headline_pattern.as_deref(), config.as_deref(), + &backend, )?, Cmd::Reason { path, entry, headline_pattern, config, + backend, check, } => reason( &path, &entry, headline_pattern.as_deref(), config.as_deref(), + &backend, check, )?, Cmd::Claim { workspace, file } => { @@ -212,12 +241,18 @@ fn scan( entry: &[PathBuf], headline_pattern: Option<&str>, config: Option<&Path>, + backend_name: &str, unused: bool, json: bool, ) -> Result<()> { - let backend = Agda; - let (roots, rules, _cfg) = - resolve_roots_and_rules(include_root, entry, headline_pattern, config, &backend)?; + let backend = backend_for(backend_name)?; + let (roots, rules, _cfg) = resolve_roots_and_rules( + include_root, + entry, + headline_pattern, + config, + backend.as_ref(), + )?; let ctx = LintContext { include_root, entry_modules: &roots, @@ -303,7 +338,7 @@ fn scan( Ok(()) } -fn check(file: &Path, include_root: Option<&Path>, json: bool) -> Result<()> { +fn check(file: &Path, include_root: Option<&Path>, backend_name: &str, json: bool) -> Result<()> { if !file.is_file() { anyhow::bail!("file not found: {}", file.display()); } @@ -318,7 +353,7 @@ fn check(file: &Path, include_root: Option<&Path>, json: bool) -> Result<()> { // The orphan rule self-skips when the file is its own root, which is // exactly what a single-file check wants. - let backend = Agda; + let backend = backend_for(backend_name)?; let rules = backend.lint_rules(&RuleConfig::default())?; let roots = [file.to_path_buf()]; let ctx = LintContext { @@ -377,16 +412,22 @@ fn dag( entry: &[PathBuf], headline_pattern: Option<&str>, config: Option<&Path>, + backend_name: &str, ) -> Result<()> { - let backend = Agda; - let (roots, rules, cfg) = - resolve_roots_and_rules(include_root, entry, headline_pattern, config, &backend)?; + let backend = backend_for(backend_name)?; + let (roots, rules, cfg) = resolve_roots_and_rules( + include_root, + entry, + headline_pattern, + config, + backend.as_ref(), + )?; let doc = build_dag( include_root, &roots, &rules, &cfg.headline_pattern, - &backend, + backend.as_ref(), )?; println!("{}", serde_json::to_string_pretty(&doc)?); Ok(()) @@ -397,17 +438,23 @@ fn reason( entry: &[PathBuf], headline_pattern: Option<&str>, config: Option<&Path>, + backend_name: &str, do_check: bool, ) -> Result<()> { - let backend = Agda; - let (roots, rules, cfg) = - resolve_roots_and_rules(include_root, entry, headline_pattern, config, &backend)?; + let backend = backend_for(backend_name)?; + let (roots, rules, cfg) = resolve_roots_and_rules( + include_root, + entry, + headline_pattern, + config, + backend.as_ref(), + )?; let dag_doc = build_dag( include_root, &roots, &rules, &cfg.headline_pattern, - &backend, + backend.as_ref(), )?; // Real prover verdicts by module id. Empty unless `--check`, in which @@ -426,7 +473,7 @@ fn reason( } } - let doc = build_reason(dag_doc, &backend, &verdicts, &stale); + let doc = build_reason(dag_doc, backend.as_ref(), &verdicts, &stale); println!("{}", serde_json::to_string_pretty(&doc)?); Ok(()) } diff --git a/src/prover/idris2.rs b/src/prover/idris2.rs new file mode 100644 index 0000000..9b50100 --- /dev/null +++ b/src/prover/idris2.rs @@ -0,0 +1,216 @@ +// SPDX-License-Identifier: MPL-2.0 +// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) + +//! The Idris2 backend. +//! +//! Idris2 is a core estate language — it owns ABIs (the Idris2-ABI / Zig-FFI +//! pattern), so it is a first-class backend, not merely a prover. This +//! adapter shells out to `idris2 --check --source-dir ` (the +//! `-i`-style include-root analog, ground-truthed against Idris2 0.7.0). +//! +//! Assistant model, exit-code-only: exit 0 → [`Verdict::Proven`], a run that +//! errors → [`Verdict::Error`], an absent binary → [`Verdict::Unavailable`]. +//! arghda never claims a result Idris2 did not return. +//! +//! Idris2 modules are dotted and map to paths exactly like Agda +//! (`Data.Vect` ↔ `Data/Vect.idr`), so [`crate::graph::module_name_of`] is +//! reused; only the file extension (`.idr`) and the import syntax +//! (`import [public] Mod [as Alias]`, top-level — no `open`) differ. + +use super::{Backend, BackendKind, Outcome, Verdict}; +use crate::graph; +use crate::lint::{idris2::Idris2EscapeHatch, LintRule, RuleConfig}; +use anyhow::{Context, Result}; +use std::fs; +use std::path::{Path, PathBuf}; +use std::process::Command; +use walkdir::WalkDir; + +const TAIL_LINES: usize = 40; + +/// The Idris2 proof assistant / dependently-typed language. +#[derive(Clone, Copy, Debug, Default)] +pub struct Idris2; + +impl Backend for Idris2 { + fn name(&self) -> &'static str { + "idris2" + } + + fn kind(&self) -> BackendKind { + BackendKind::Assistant + } + + fn extensions(&self) -> &'static [&'static str] { + &["idr"] + } + + fn safe_mode(&self) -> Option<&'static str> { + // Idris2 has no global `--safe`; totality is per-definition, opted in + // file-wide with this directive. + Some("%default total") + } + + fn check_file(&self, file: &Path, include_root: &Path) -> Result { + let output = Command::new("idris2") + .arg("--check") + .arg("--source-dir") + .arg(include_root) + .arg(file) + .output(); + + match output { + Ok(out) => { + let mut combined = String::from_utf8_lossy(&out.stdout).into_owned(); + combined.push_str(&String::from_utf8_lossy(&out.stderr)); + let ok = out.status.success(); + Ok(Outcome { + available: true, + exit_code: out.status.code(), + ok, + output_tail: tail(&combined, TAIL_LINES), + kind: BackendKind::Assistant, + verdict: if ok { Verdict::Proven } else { Verdict::Error }, + }) + } + Err(e) if e.kind() == std::io::ErrorKind::NotFound => { + Ok(Outcome::unavailable(BackendKind::Assistant)) + } + Err(e) => Err(e.into()), + } + } + + fn module_name_of(&self, file: &Path, include_root: &Path) -> Option { + // Extension-agnostic; identical dotted convention to Agda. + graph::module_name_of(file, include_root) + } + + fn module_to_path(&self, module: &str, include_root: &Path) -> PathBuf { + let mut p = include_root.to_path_buf(); + for part in module.split('.') { + p.push(part); + } + p.set_extension("idr"); + p + } + + fn direct_imports(&self, file: &Path) -> Result> { + let contents = + fs::read_to_string(file).with_context(|| format!("reading {}", file.display()))?; + let mut out = Vec::new(); + for line in contents.lines() { + let trimmed = line.trim_start(); + if trimmed.starts_with("--") { + continue; + } + // Strip a trailing line comment, then tokenise. + let code = trimmed.split(" --").next().unwrap_or(trimmed); + let tokens: Vec<&str> = code.split_whitespace().collect(); + // Idris2 imports are top-level: `import [public] Mod [as Alias]`. + if tokens.first() != Some(&"import") { + continue; + } + let mut idx = 1; + if tokens.get(idx) == Some(&"public") { + idx += 1; + } + if let Some(module) = tokens.get(idx) { + let cleaned = + module.trim_end_matches(|c: char| !c.is_alphanumeric() && c != '.' && c != '_'); + if !cleaned.is_empty() { + out.push(cleaned.to_string()); + } + } + } + Ok(out) + } + + fn discover_roots(&self, include_root: &Path) -> Vec { + // Idris2 has no `All.agda`-style convention; the executable entry is + // `Main.idr`. (`.ipkg`-declared `main`/`modules` roots are a + // documented follow-on.) + let mut roots = Vec::new(); + for entry in WalkDir::new(include_root) + .into_iter() + .filter_map(|e| e.ok()) + { + let path = entry.path(); + if path.extension().and_then(|s| s.to_str()) != Some("idr") { + continue; + } + if path.file_name().and_then(|s| s.to_str()) == Some("Main.idr") { + roots.push(path.to_path_buf()); + } + } + roots.sort(); + roots + } + + fn lint_rules(&self, _cfg: &RuleConfig) -> Result>> { + Ok(vec![Box::new(Idris2EscapeHatch)]) + } +} + +fn tail(s: &str, n: usize) -> String { + let lines: Vec<&str> = s.lines().collect(); + let start = lines.len().saturating_sub(n); + lines[start..].join("\n") +} + +#[cfg(test)] +mod tests { + use super::*; + + #[test] + fn idris2_backend_identity() { + assert_eq!(Idris2.name(), "idris2"); + assert_eq!(Idris2.kind(), BackendKind::Assistant); + assert_eq!(Idris2.extensions(), &["idr"]); + } + + #[test] + fn module_to_path_uses_idr_extension() { + let root = Path::new("/r"); + assert_eq!( + Idris2.module_to_path("Data.Vect", root), + PathBuf::from("/r/Data/Vect.idr") + ); + } + + #[test] + fn parses_idris_imports_including_public_and_alias() { + let tmp = tempfile::NamedTempFile::new().unwrap(); + std::fs::write( + tmp.path(), + "module Main\n\ + import Data.Vect\n\ + import public Data.List\n\ + import Util as U\n\ + -- import Ignored.Comment\n\ + x = 0 -- import AlsoIgnored\n", + ) + .unwrap(); + let imports = Idris2.direct_imports(tmp.path()).unwrap(); + assert!(imports.contains(&"Data.Vect".to_string())); + assert!(imports.contains(&"Data.List".to_string()), "public import"); + assert!(imports.contains(&"Util".to_string()), "aliased import"); + assert!(!imports.iter().any(|i| i.contains("Ignored"))); + assert!(!imports.iter().any(|i| i.contains("Also"))); + } + + #[test] + fn check_file_is_honest_about_availability() { + let tmp = tempfile::tempdir().unwrap(); + let f = tmp.path().join("Main.idr"); + std::fs::write(&f, "module Main\n\nmain : IO ()\nmain = pure ()\n").unwrap(); + let out = Idris2.check_file(&f, tmp.path()).unwrap(); + if out.available { + assert!(matches!(out.verdict, Verdict::Proven | Verdict::Error)); + assert_eq!(out.ok, out.verdict == Verdict::Proven); + } else { + assert_eq!(out.verdict, Verdict::Unavailable); + assert!(!out.ok); + assert!(out.exit_code.is_none()); + } + } +} diff --git a/src/prover/mod.rs b/src/prover/mod.rs index 13cb0ac..cbe4394 100644 --- a/src/prover/mod.rs +++ b/src/prover/mod.rs @@ -27,8 +27,10 @@ use serde::Serialize; use std::path::{Path, PathBuf}; pub mod agda; +pub mod idris2; pub use agda::Agda; +pub use idris2::Idris2; /// The two backend interaction models. #[derive(Clone, Copy, Debug, PartialEq, Eq, Serialize)] diff --git a/tests/fixtures/idris2/Data/Helper.idr b/tests/fixtures/idris2/Data/Helper.idr new file mode 100644 index 0000000..bdd9614 --- /dev/null +++ b/tests/fixtures/idris2/Data/Helper.idr @@ -0,0 +1,5 @@ +module Data.Helper + +export +answer : Nat +answer = 42 diff --git a/tests/fixtures/idris2/Main.idr b/tests/fixtures/idris2/Main.idr new file mode 100644 index 0000000..d22a08b --- /dev/null +++ b/tests/fixtures/idris2/Main.idr @@ -0,0 +1,7 @@ +module Main + +import Util +import public Data.Helper + +main : IO () +main = putStrLn greeting diff --git a/tests/fixtures/idris2/Orphan.idr b/tests/fixtures/idris2/Orphan.idr new file mode 100644 index 0000000..2f4a8c5 --- /dev/null +++ b/tests/fixtures/idris2/Orphan.idr @@ -0,0 +1,6 @@ +module Orphan + +-- Imported by nothing reachable from Main: the reason graph marks it unwired. +export +stray : Nat +stray = 0 diff --git a/tests/fixtures/idris2/Util.idr b/tests/fixtures/idris2/Util.idr new file mode 100644 index 0000000..49ab189 --- /dev/null +++ b/tests/fixtures/idris2/Util.idr @@ -0,0 +1,5 @@ +module Util + +export +greeting : String +greeting = "hi" diff --git a/tests/idris2.rs b/tests/idris2.rs new file mode 100644 index 0000000..85e725a --- /dev/null +++ b/tests/idris2.rs @@ -0,0 +1,91 @@ +// SPDX-License-Identifier: MPL-2.0 +// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) + +//! Idris2 backend, exercised through the backend-parametric graph/dag/reason +//! path. These tests are hermetic — they only parse `.idr` text (module +//! names + imports), so they run with or without the `idris2` binary present. +//! The real typecheck (`check_file`) is covered by the unit test in +//! `src/prover/idris2.rs` (honest either way) and by manual dogfooding. + +use arghda_core::lint::unpinned_headline::DEFAULT_HEADLINE_PATTERN; +use arghda_core::{build_dag, build_reason, Backend, Idris2, LintRule}; +use std::collections::{BTreeMap, BTreeSet}; +use std::path::PathBuf; + +fn idris2_fixture() -> PathBuf { + let mut p = PathBuf::from(env!("CARGO_MANIFEST_DIR")); + p.push("tests"); + p.push("fixtures"); + p.push("idris2"); + p +} + +/// The graph path needs no lint rules; a typed empty pack. +fn no_rules() -> Vec> { + Vec::new() +} + +#[test] +fn idris2_import_graph_over_the_fixture() { + let root = idris2_fixture(); + // No lint rules needed to exercise the graph; the Idris2 backend drives + // extension filtering (.idr), module naming, and import parsing. + let roots = Idris2.discover_roots(&root); + let dag = build_dag( + &root, + &roots, + &no_rules(), + DEFAULT_HEADLINE_PATTERN, + &Idris2, + ) + .unwrap(); + + let ids: Vec<&str> = dag.nodes.iter().map(|n| n.id.as_str()).collect(); + // Dotted Idris2 module names, sorted. + assert_eq!(ids, vec!["Data.Helper", "Main", "Orphan", "Util"]); + + // `import Util` and `import public Data.Helper` both become edges. + assert!(dag + .edges + .iter() + .any(|e| e.from == "Main" && e.to == "Util" && e.kind == "imports")); + assert!(dag + .edges + .iter() + .any(|e| e.from == "Main" && e.to == "Data.Helper")); + // Nothing imports Orphan. + assert!(!dag.edges.iter().any(|e| e.to == "Orphan")); +} + +#[test] +fn idris2_discover_roots_finds_main() { + let root = idris2_fixture(); + let roots = Idris2.discover_roots(&root); + let names: Vec = roots + .iter() + .map(|p| p.file_name().unwrap().to_str().unwrap().to_string()) + .collect(); + assert_eq!(names, vec!["Main.idr".to_string()]); +} + +#[test] +fn idris2_reason_graph_wires_the_main_cone() { + let root = idris2_fixture(); + let roots = Idris2.discover_roots(&root); + let dag = build_dag( + &root, + &roots, + &no_rules(), + DEFAULT_HEADLINE_PATTERN, + &Idris2, + ) + .unwrap(); + let doc = build_reason(dag, &Idris2, &BTreeMap::new(), &BTreeSet::new()); + + assert_eq!(doc.crt_roots, vec!["Main".to_string()]); + let wired = |id: &str| doc.nodes.iter().find(|n| n.id == id).unwrap().wired; + assert!(wired("Main")); + assert!(wired("Util")); + assert!(wired("Data.Helper")); + assert!(!wired("Orphan"), "Orphan must be unwired"); +}