Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
96 changes: 96 additions & 0 deletions crates/jtv-core/src/echo.rs
Original file line number Diff line number Diff line change
Expand Up @@ -172,10 +172,106 @@ fn classify_control_stmts(stmts: &[ControlStmt]) -> Echo {
.fold(Echo::Safe, Echo::join)
}

// ============================================================================
// SECTION 4: ECHO AS A FUNCTION EFFECT (ADR-0009 D1, slice 1)
// ============================================================================

/// The Echo grade a *function body* induces (ADR-0009 D1) — the inference half
/// of Echo-as-a-first-class-function-effect. It is the join of the echoes of the
/// body's statements: addition-only data assignments are `Safe` (no loss);
/// `reverse` / `reversible` blocks contribute their block echo
/// (`classify_stmts`); control flow joins its sub-bodies. Lifts the block-level
/// `classify_stmts` to a whole function body.
///
/// Slice 1 computes a function's *own* body grade; resolving the grade of
/// `FunctionCall`s (joining the callee's grade into the caller's) is a later
/// slice that needs a function-echo environment.
pub fn function_echo(body: &[ControlStmt]) -> Echo {
body.iter()
.map(control_stmt_echo)
.fold(Echo::Safe, Echo::join)
}

fn control_stmt_echo(s: &ControlStmt) -> Echo {
match s {
// Addition-only data assignment: no loss.
ControlStmt::Assignment(_) => Echo::Safe,
ControlStmt::If(i) => {
let then_echo = function_echo(&i.then_branch);
match &i.else_branch {
Some(b) => then_echo.join(function_echo(b)),
None => then_echo,
}
}
ControlStmt::While(w) => function_echo(&w.body),
ControlStmt::For(f) => function_echo(&f.body),
// Reverse / reversible blocks carry their own block echo.
ControlStmt::ReverseBlock(b) => classify_stmts(&b.body),
ControlStmt::ReversibleBlock(b) => classify_stmts(&b.body),
ControlStmt::Block(ss) => function_echo(ss),
// Reading, printing, and token consumption induce no data loss here.
ControlStmt::Return(_)
| ControlStmt::Print(_)
| ControlStmt::ReverseToken(_)
| ControlStmt::AbandonToken(_) => Echo::Safe,
}
}

#[cfg(test)]
mod tests {
use super::*;

#[test]
fn empty_function_is_safe() {
assert_eq!(function_echo(&[]), Echo::Safe);
}

#[test]
fn function_echo_addition_only_is_safe() {
// body: x = a + b
let body = vec![ControlStmt::Assignment(Assignment {
target: "x".to_string(),
value: Expr::Data(DataExpr::add(
DataExpr::identifier("a"),
DataExpr::identifier("b"),
)),
})];
assert_eq!(function_echo(&body), Echo::Safe);
}

#[test]
fn function_echo_self_reference_reverse_is_neutral() {
// body: reverse { x += x } — the block is Neutral, so the function is.
let body = vec![ControlStmt::ReverseBlock(ReverseBlock {
body: vec![ReversibleStmt::AddAssign(
"x".to_string(),
DataExpr::Identifier("x".to_string()),
)],
})];
assert_eq!(function_echo(&body), Echo::Neutral);
}

#[test]
fn function_echo_joins_branches() {
// if cond { reverse { x += x } } else { y = 1 } -> Neutral join Safe = Neutral
let then_branch = vec![ControlStmt::ReverseBlock(ReverseBlock {
body: vec![ReversibleStmt::AddAssign(
"x".to_string(),
DataExpr::Identifier("x".to_string()),
)],
})];
let else_branch = vec![ControlStmt::Assignment(Assignment {
target: "y".to_string(),
value: Expr::Data(DataExpr::Number(Number::Int(1))),
})];
let body = vec![ControlStmt::If(IfStmt {
condition: ControlExpr::Data(DataExpr::Identifier("cond".to_string())),
then_branch,
else_branch: Some(else_branch),
})];
assert_eq!(function_echo(&body), Echo::Neutral);
}

#[test]
fn join_is_lattice() {
use Echo::*;
Expand Down
206 changes: 206 additions & 0 deletions crates/jtv-core/src/epistemic.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,206 @@
// SPDX-License-Identifier: MPL-2.0
// Copyright (c) 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
//
// ADR-0009 D2: the Epistemic effect — what a function reveals about its inputs
// (knowledge / observability). Lattice:
//
// Opaque (reveals nothing) ⊑ Partial (reveals a bounded function of inputs)
// ⊑ Transparent (reveals the inputs fully)
//
// Dual to Echo (loss vs revelation) with the same join law. The v1 inference
// here is output-based and deliberately conservative: a function is graded by
// the worst-case revelation across its OUTPUT expressions (each `return e` /
// `print e`). Refine on use, per ADR-0009.

use crate::ast::*;
use std::collections::HashSet;

/// The epistemic grade (ADR-0009 D2): how much a function reveals about inputs.
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub enum Epistemic {
/// Reveals nothing about the inputs.
Opaque,
/// Reveals a bounded function of the inputs.
Partial,
/// Reveals the inputs fully (the output determines the input).
Transparent,
}

impl Epistemic {
fn rank(self) -> u8 {
match self {
Epistemic::Opaque => 0,
Epistemic::Partial => 1,
Epistemic::Transparent => 2,
}
}

/// Least upper bound: the worst-case revelation (the higher of the two).
pub fn join(self, other: Epistemic) -> Epistemic {
if self.rank() >= other.rank() {
self
} else {
other
}
}

/// Lattice order `a ⊑ b`.
pub fn leq(self, other: Epistemic) -> bool {
self.rank() <= other.rank()
}
}

/// The epistemic grade a function induces (ADR-0009 D2) — the worst-case
/// revelation across its output expressions (each `return e` and `print e`). An
/// output that *is* an input parameter is `Transparent`; one that merely
/// references an input is `Partial`; one independent of the inputs is `Opaque`.
/// A function with no outputs is `Opaque`. (Conservative v1; refine on use.)
pub fn function_epistemic(func: &FunctionDecl) -> Epistemic {
let params: HashSet<&str> = func.params.iter().map(|p| p.name.as_str()).collect();
let mut outputs: Vec<&DataExpr> = Vec::new();
collect_outputs(&func.body, &mut outputs);
outputs
.iter()
.map(|&e| output_epistemic(e, &params))
.fold(Epistemic::Opaque, Epistemic::join)
}

fn output_epistemic(e: &DataExpr, params: &HashSet<&str>) -> Epistemic {
if is_param(e, params) {
Epistemic::Transparent
} else if refs_param(e, params) {
Epistemic::Partial
} else {
Epistemic::Opaque
}
}

/// `e` is exactly an input parameter.
fn is_param(e: &DataExpr, params: &HashSet<&str>) -> bool {
matches!(e, DataExpr::Identifier(name) if params.contains(name.as_str()))
}

/// `e` references any input parameter (transitively).
fn refs_param(e: &DataExpr, params: &HashSet<&str>) -> bool {
match e {
DataExpr::Identifier(name) => params.contains(name.as_str()),
DataExpr::Add(l, r) => refs_param(l, params) || refs_param(r, params),
DataExpr::Negate(inner) => refs_param(inner, params),
DataExpr::FunctionCall(c) => c.args.iter().any(|a| refs_param(a, params)),
DataExpr::List(es) | DataExpr::Tuple(es) => es.iter().any(|x| refs_param(x, params)),
DataExpr::Number(_) | DataExpr::StringLit(_) => false,
}
}

/// Collect every output expression (`return e` value, `print` args) in a body.
fn collect_outputs<'a>(body: &'a [ControlStmt], out: &mut Vec<&'a DataExpr>) {
for s in body {
match s {
ControlStmt::Return(Some(e)) => out.push(e),
ControlStmt::Print(es) => out.extend(es.iter()),
ControlStmt::If(i) => {
collect_outputs(&i.then_branch, out);
if let Some(b) = &i.else_branch {
collect_outputs(b, out);
}
}
ControlStmt::While(w) => collect_outputs(&w.body, out),
ControlStmt::For(f) => collect_outputs(&f.body, out),
ControlStmt::Block(ss) => collect_outputs(ss, out),
ControlStmt::Return(None)
| ControlStmt::Assignment(_)
| ControlStmt::ReverseBlock(_)
| ControlStmt::ReversibleBlock(_)
| ControlStmt::ReverseToken(_)
| ControlStmt::AbandonToken(_) => {}
}
}
}

#[cfg(test)]
mod tests {
use super::*;

fn func(params: Vec<&str>, body: Vec<ControlStmt>) -> FunctionDecl {
FunctionDecl {
name: "f".to_string(),
params: params
.into_iter()
.map(|n| Param {
name: n.to_string(),
type_annotation: None,
})
.collect(),
return_type: None,
purity: Purity::Pure,
body,
}
}

#[test]
fn lattice_join_is_max() {
use Epistemic::*;
assert_eq!(Opaque.join(Partial), Partial);
assert_eq!(Partial.join(Transparent), Transparent);
assert_eq!(Transparent.join(Opaque), Transparent);
assert_eq!(Opaque.join(Opaque), Opaque);
assert!(Opaque.leq(Transparent));
assert!(!Transparent.leq(Opaque));
}

#[test]
fn returning_a_param_is_transparent() {
// f(x) { return x }
let f = func(
vec!["x"],
vec![ControlStmt::Return(Some(DataExpr::identifier("x")))],
);
assert_eq!(function_epistemic(&f), Epistemic::Transparent);
}

#[test]
fn returning_a_constant_is_opaque() {
// f(x) { return 1 }
let f = func(
vec!["x"],
vec![ControlStmt::Return(Some(DataExpr::Number(Number::Int(1))))],
);
assert_eq!(function_epistemic(&f), Epistemic::Opaque);
}

#[test]
fn returning_a_function_of_input_is_partial() {
// f(x) { return x + 1 }
let f = func(
vec!["x"],
vec![ControlStmt::Return(Some(DataExpr::add(
DataExpr::identifier("x"),
DataExpr::Number(Number::Int(1)),
)))],
);
assert_eq!(function_epistemic(&f), Epistemic::Partial);
}

#[test]
fn no_output_is_opaque() {
// f(x) { y = 1 }
let f = func(
vec!["x"],
vec![ControlStmt::Assignment(Assignment {
target: "y".to_string(),
value: Expr::Data(DataExpr::Number(Number::Int(1))),
})],
);
assert_eq!(function_epistemic(&f), Epistemic::Opaque);
}

#[test]
fn printing_an_input_is_transparent() {
// f(x) { print x }
let f = func(
vec!["x"],
vec![ControlStmt::Print(vec![DataExpr::identifier("x")])],
);
assert_eq!(function_epistemic(&f), Epistemic::Transparent);
}
}
1 change: 1 addition & 0 deletions crates/jtv-core/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,7 @@ pub mod coproc;
pub mod coproc_lower;
pub mod dialect;
pub mod echo;
pub mod epistemic;
pub mod error;
pub mod formatter;
pub mod interpreter;
Expand Down
Loading