Skip to content

Commit bc1d38a

Browse files
hyperpolymathclaude
andcommitted
feat(jtv): Phase 2 — PataCL coproc integration (12/12 tests)
Grammar: extern_coproc_block + intrinsic_decl + insn_decl + encoding_clause. AST: ExternCoprocBlock, CoprocItem, CoprocResolution variants. coproc.rs: resolve_coproc_blocks — PataCL gate eval, block-inclusion pass, CoprocNamespace registration. Dead blocks silently dropped; live blocks annotated with (live, family). Interpreter: register_coproc_namespace + ExternCoprocNotYetLowered phase- boundary error at call sites (per ADR-0005). Formatter/pretty/typechecker exhaustiveness satisfied. All 41 existing tests still pass. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
1 parent 66e16fa commit bc1d38a

14 files changed

Lines changed: 810 additions & 3 deletions

File tree

Cargo.lock

Lines changed: 12 additions & 0 deletions
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

Cargo.toml

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -60,3 +60,6 @@ tower-lsp = "0.20"
6060

6161
# Internal crates
6262
jtv-core = { path = "crates/jtv-core" }
63+
64+
# PataCL — compile-time decision layer
65+
patacl-core = { path = "../patacl/crates/patacl-core" }

crates/jtv-core/Cargo.toml

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -22,6 +22,7 @@ thiserror.workspace = true
2222
serde.workspace = true
2323
serde_json.workspace = true
2424
wasm-bindgen.workspace = true
25+
patacl-core.workspace = true
2526

2627
[dev-dependencies]
2728
criterion.workspace = true

crates/jtv-core/src/ast.rs

Lines changed: 51 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -10,6 +10,7 @@ pub struct Program {
1010
pub enum TopLevel {
1111
Module(ModuleDecl),
1212
Import(ImportStmt),
13+
ExternCoproc(ExternCoprocBlock),
1314
Function(FunctionDecl),
1415
Control(ControlStmt),
1516
}
@@ -26,6 +27,56 @@ pub struct ImportStmt {
2627
pub alias: Option<String>,
2728
}
2829

30+
// ===== COPROCESSOR DECLARATIONS =====
31+
32+
/// A top-level `extern coproc <gate-name> { ... }` block.
33+
///
34+
/// `gate_name` is the name of a gate in a companion `.pata` file.
35+
/// PataCL evaluates the gate at compile time; if dead, this block is
36+
/// dropped entirely. If live, `items` are registered in the function
37+
/// namespace as `ExternCoproc` entries.
38+
///
39+
/// `resolved` is `None` until the PataCL resolution pass runs.
40+
#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]
41+
pub struct ExternCoprocBlock {
42+
pub gate_name: String,
43+
pub items: Vec<CoprocItem>,
44+
pub resolved: Option<CoprocResolution>,
45+
}
46+
47+
/// Outcome of PataCL gate evaluation for one `extern coproc` block.
48+
#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]
49+
pub struct CoprocResolution {
50+
pub live: bool,
51+
pub family: String,
52+
}
53+
54+
#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]
55+
pub enum CoprocItem {
56+
Intrinsic(CoprocIntrinsic),
57+
Insn(CoprocInsn),
58+
}
59+
60+
/// A coprocessor intrinsic — a named builtin with no encoding literal.
61+
#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]
62+
pub struct CoprocIntrinsic {
63+
pub name: String,
64+
pub params: Vec<Param>,
65+
pub return_type: TypeAnnotation,
66+
pub purity: Purity,
67+
}
68+
69+
/// A custom instruction with an optional opaque encoding string.
70+
/// The encoding is passed verbatim to the assembler backend.
71+
#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]
72+
pub struct CoprocInsn {
73+
pub name: String,
74+
pub params: Vec<Param>,
75+
pub return_type: TypeAnnotation,
76+
pub purity: Purity,
77+
pub encoding: Option<String>,
78+
}
79+
2980
// ===== CONTROL LANGUAGE (Turing-complete) =====
3081

3182
#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]

crates/jtv-core/src/coproc.rs

Lines changed: 225 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,225 @@
1+
// SPDX-License-Identifier: PMPL-1.0-or-later
2+
// (MPL-2.0 is automatic legal fallback until PMPL is formally recognised)
3+
// Copyright (c) 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
4+
5+
//! PataCL resolution pass for `extern coproc` blocks (Phase 2).
6+
//!
7+
//! Implements Steps 1–3 of the JtV/PataCL integration contract:
8+
//! 1. Name-resolution: for each `extern coproc <gate-name>` block,
9+
//! invoke PataCL with the gate-name and target fact environment.
10+
//! 2. Block-inclusion: drop blocks whose gate evaluated to dead.
11+
//! 3. Function-namespace registration: surviving decls are added to a
12+
//! `CoprocNamespace` for the interpreter and type-checker to consume.
13+
//!
14+
//! Call-site phase-boundary error (Step 4) lives in `interpreter.rs`;
15+
//! the namespace built here is what triggers it at evaluation time.
16+
//!
17+
//! # Usage
18+
//!
19+
//! ```rust,ignore
20+
//! let env = CoprocEnv::from_triple("riscv64gc-unknown-none-elf", &["v"]);
21+
//! let pata_src = std::fs::read_to_string("coproc/riscv.pata")?;
22+
//! let (program, ns) = resolve_coproc_blocks(program, &env, Some(&pata_src))?;
23+
//! ```
24+
25+
use std::collections::HashMap;
26+
27+
use patacl_core::{compile as patacl_compile, env_from_triple, eval::eval_gates, GateResult};
28+
29+
use crate::ast::{
30+
CoprocItem, CoprocResolution, ExternCoprocBlock, Program, TopLevel,
31+
};
32+
use crate::error::{JtvError, Result};
33+
34+
// ──────────────────────────────────────────────
35+
// Coproc environment
36+
// ──────────────────────────────────────────────
37+
38+
/// Build-time environment for PataCL gate evaluation.
39+
pub struct CoprocEnv {
40+
target_triple: String,
41+
features: Vec<String>,
42+
}
43+
44+
impl CoprocEnv {
45+
pub fn new(target_triple: impl Into<String>, features: impl IntoIterator<Item = impl Into<String>>) -> Self {
46+
CoprocEnv {
47+
target_triple: target_triple.into(),
48+
features: features.into_iter().map(|f| f.into()).collect(),
49+
}
50+
}
51+
52+
/// Convenience constructor — same argument shape as `patacl_core::env_from_triple`.
53+
pub fn from_triple(triple: &str, features: &[&str]) -> Self {
54+
CoprocEnv::new(triple, features.iter().copied())
55+
}
56+
57+
fn patacl_env(&self) -> patacl_core::FactEnv {
58+
let refs: Vec<&str> = self.features.iter().map(|s| s.as_str()).collect();
59+
env_from_triple(&self.target_triple, &refs)
60+
}
61+
}
62+
63+
// ──────────────────────────────────────────────
64+
// Function namespace entry
65+
// ──────────────────────────────────────────────
66+
67+
/// An extern coproc function registered in the function namespace.
68+
/// The interpreter uses this to return `ExternCoprocNotYetLowered` at
69+
/// call sites (per ADR-0005 call-site contract).
70+
#[derive(Debug, Clone)]
71+
pub struct CoprocEntry {
72+
/// Gate name this decl came from (for the phase-boundary error message).
73+
pub gate_name: String,
74+
/// ISA family string evaluated from the `.pata` file.
75+
pub family: String,
76+
pub kind: CoprocKind,
77+
pub param_count: usize,
78+
}
79+
80+
#[derive(Debug, Clone)]
81+
pub enum CoprocKind {
82+
Intrinsic,
83+
Insn { encoding: Option<String> },
84+
}
85+
86+
/// Namespace of surviving extern coproc function entries.
87+
/// Keyed by function name (unqualified); gate_name is in the value.
88+
#[derive(Debug, Clone, Default)]
89+
pub struct CoprocNamespace {
90+
pub entries: HashMap<String, CoprocEntry>,
91+
}
92+
93+
impl CoprocNamespace {
94+
pub fn get(&self, name: &str) -> Option<&CoprocEntry> {
95+
self.entries.get(name)
96+
}
97+
}
98+
99+
// ──────────────────────────────────────────────
100+
// Resolution pass
101+
// ──────────────────────────────────────────────
102+
103+
/// Run the PataCL resolution pass over a parsed JtV program.
104+
///
105+
/// For each `extern coproc <gate>` block:
106+
/// - If `pata_source` is `Some`, evaluate the gate via PataCL.
107+
/// - If the gate is dead → drop the block.
108+
/// - If the gate is live (or pata_source is None) → annotate the block
109+
/// with `CoprocResolution` and add its decls to the namespace.
110+
///
111+
/// Returns the modified program (dead blocks removed) and the namespace.
112+
pub fn resolve_coproc_blocks(
113+
program: Program,
114+
env: &CoprocEnv,
115+
pata_source: Option<&str>,
116+
) -> Result<(Program, CoprocNamespace)> {
117+
// Compile the pata file once, if provided, to get all gate results.
118+
let gate_results: HashMap<String, GateResult> = if let Some(src) = pata_source {
119+
let gates = patacl_compile(src)
120+
.map_err(|e| JtvError::CoprocResolutionFailed {
121+
gate: "<pata-file>".into(),
122+
detail: e.to_string(),
123+
})?;
124+
let patacl_env = env.patacl_env();
125+
eval_gates(&gates, &patacl_env)
126+
.map_err(|e| JtvError::CoprocResolutionFailed {
127+
gate: "<pata-file>".into(),
128+
detail: e.to_string(),
129+
})?
130+
.into_iter()
131+
.map(|r| (r.name.clone(), r))
132+
.collect()
133+
} else {
134+
HashMap::new()
135+
};
136+
137+
let mut namespace = CoprocNamespace::default();
138+
let mut filtered = Vec::with_capacity(program.statements.len());
139+
140+
for item in program.statements {
141+
match item {
142+
TopLevel::ExternCoproc(block) => {
143+
let (keep, resolved) = resolve_one_block(&block, pata_source, &gate_results)?;
144+
if keep {
145+
let family = resolved.as_ref().map(|r| r.family.clone()).unwrap_or_default();
146+
register_block_decls(&block, &family, &mut namespace);
147+
filtered.push(TopLevel::ExternCoproc(ExternCoprocBlock {
148+
resolved,
149+
..block
150+
}));
151+
}
152+
// Dead blocks are silently dropped.
153+
}
154+
other => filtered.push(other),
155+
}
156+
}
157+
158+
Ok((Program { statements: filtered }, namespace))
159+
}
160+
161+
/// Resolve a single block: returns (keep, Option<CoprocResolution>).
162+
fn resolve_one_block(
163+
block: &ExternCoprocBlock,
164+
pata_source: Option<&str>,
165+
gate_results: &HashMap<String, GateResult>,
166+
) -> Result<(bool, Option<CoprocResolution>)> {
167+
if pata_source.is_none() {
168+
// No pata source — treat all blocks as unconditionally live.
169+
// Useful during development before .pata files are written.
170+
return Ok((true, None));
171+
}
172+
173+
match gate_results.get(&block.gate_name) {
174+
Some(result) => {
175+
if result.live {
176+
Ok((true, Some(CoprocResolution {
177+
live: true,
178+
family: result.family.clone().unwrap_or_default(),
179+
})))
180+
} else {
181+
Ok((false, None))
182+
}
183+
}
184+
None => {
185+
// Gate name not found in pata file.
186+
// Per ADR-0004 strict semantics, this is a build error.
187+
Err(JtvError::CoprocResolutionFailed {
188+
gate: block.gate_name.clone(),
189+
detail: format!(
190+
"gate `{}` not found in .pata source; \
191+
declare it with `gate {} when <predicate>`",
192+
block.gate_name, block.gate_name
193+
),
194+
})
195+
}
196+
}
197+
}
198+
199+
/// Register all decls in a live block into the namespace.
200+
fn register_block_decls(
201+
block: &ExternCoprocBlock,
202+
family: &str,
203+
ns: &mut CoprocNamespace,
204+
) {
205+
for item in &block.items {
206+
match item {
207+
CoprocItem::Intrinsic(i) => {
208+
ns.entries.insert(i.name.clone(), CoprocEntry {
209+
gate_name: block.gate_name.clone(),
210+
family: family.to_string(),
211+
kind: CoprocKind::Intrinsic,
212+
param_count: i.params.len(),
213+
});
214+
}
215+
CoprocItem::Insn(i) => {
216+
ns.entries.insert(i.name.clone(), CoprocEntry {
217+
gate_name: block.gate_name.clone(),
218+
family: family.to_string(),
219+
kind: CoprocKind::Insn { encoding: i.encoding.clone() },
220+
param_count: i.params.len(),
221+
});
222+
}
223+
}
224+
}
225+
}

crates/jtv-core/src/error.rs

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -46,6 +46,21 @@ pub enum JtvError {
4646

4747
#[error("IO error: {0}")]
4848
IoError(String),
49+
50+
/// Phase-boundary error: the PataCL gate evaluated to live, the decl was
51+
/// registered, but native lowering (Zig FFI / Idris2 ABI / SPARK) is not
52+
/// yet implemented. Informational — marks the exact boundary between
53+
/// "pata done" and "emission pending" (per JtV ADR-0005).
54+
#[error(
55+
"extern coproc `{gate}` function `{name}` is live on this target \
56+
but native lowering is not yet implemented (Phase 2 boundary — \
57+
Zig FFI / Idris2 ABI / SPARK emission pending)"
58+
)]
59+
ExternCoprocNotYetLowered { gate: String, name: String },
60+
61+
/// PataCL gate resolution error surfaced during compile-time pass.
62+
#[error("PataCL gate resolution failed for `{gate}`: {detail}")]
63+
CoprocResolutionFailed { gate: String, detail: String },
4964
}
5065

5166
impl From<std::io::Error> for JtvError {

crates/jtv-core/src/formatter.rs

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -73,6 +73,14 @@ impl Formatter {
7373
self.format_control_stmt(stmt);
7474
self.output.push('\n');
7575
}
76+
TopLevel::ExternCoproc(block) => {
77+
self.write_indent();
78+
self.output.push_str(&format!(
79+
"extern coproc {} {{ /* {} item(s) */ }}\n",
80+
block.gate_name,
81+
block.items.len()
82+
));
83+
}
7684
}
7785
}
7886

0 commit comments

Comments
 (0)