lex_types/
discharge.rs

1//! Static discharge of refinement-type predicates (#209 slice 2).
2//!
3//! Given a refined parameter type `Int{x | x > 0}` and a call-site
4//! argument `5`, this module evaluates the predicate with the binding
5//! bound to the argument's value and returns whether the call site
6//! satisfies, violates, or can't statically decide the constraint.
7//!
8//! Scope (deliberately small for v1):
9//!
10//! - **Argument shape**: only `CLit` literals (`Int`, `Float`, `Bool`,
11//!   `Str`). Anything else — variables, calls, arithmetic — defers
12//!   to slice 3's runtime residual check.
13//! - **Predicate shape**: literals, the bound variable, binary
14//!   arithmetic / comparison, boolean `and` / `or` with short-circuit,
15//!   `not`. Anything else defers.
16//! - **Free variables**: the predicate must reference *only* its
17//!   binding. Other identifiers (`balance`, `ceiling`, etc.) defer
18//!   — slice 2 doesn't try to evaluate them. Slice 3 will plumb
19//!   call-site context bindings.
20//!
21//! The deliberate fall-through to "deferred" is what makes this slice
22//! ship-able: anything we can't reason about cleanly stays a
23//! type-check pass and waits for slice 3's runtime check, rather
24//! than blocking type-check on cases we can't yet handle.
25
26use lex_ast::{CExpr, CLit};
27
28#[derive(Debug, Clone, PartialEq)]
29pub enum DischargeOutcome {
30    /// Predicate evaluated to `true` with the binding bound to the
31    /// argument value. Static check succeeds; no runtime work.
32    Proved,
33    /// Predicate evaluated to `false`. The call-site argument
34    /// definitely violates the refinement — surface as a type error.
35    Refuted { reason: String },
36    /// Couldn't decide statically. Slice 3 will emit a residual
37    /// runtime check at the call boundary; this slice just lets
38    /// type-check pass.
39    Deferred { reason: String },
40}
41
42/// Try to discharge `predicate` with `binding_name` bound to `arg`.
43/// `arg` is the CallExpr's argument expression — only literal forms
44/// (`CLit`) participate in static discharge; anything else defers.
45pub fn try_discharge(
46    predicate: &CExpr,
47    binding_name: &str,
48    arg: &CExpr,
49) -> DischargeOutcome {
50    let v = match arg_to_concrete(arg) {
51        Some(v) => v,
52        None => return DischargeOutcome::Deferred {
53            reason: "argument is not a literal; static discharge can't \
54                     evaluate it (slice 3 will add a runtime check)".into(),
55        },
56    };
57    match eval(predicate, binding_name, &v) {
58        Ok(Concrete::Bool(true)) => DischargeOutcome::Proved,
59        Ok(Concrete::Bool(false)) => DischargeOutcome::Refuted {
60            reason: format!(
61                "predicate failed for {} = {}",
62                binding_name, v.show()),
63        },
64        Ok(other) => DischargeOutcome::Deferred {
65            reason: format!("predicate didn't reduce to a Bool (got {})",
66                other.show()),
67        },
68        Err(e) => DischargeOutcome::Deferred { reason: e },
69    }
70}
71
72/// Reduce a call-site argument expression to a `Concrete` value if
73/// it's a literal or a sign-flipped literal. Lex parses `-5` as
74/// `UnaryOp { op: "-", expr: Literal { Int(5) } }` rather than a
75/// negative literal, so we fold that one shape inline. Anything
76/// more involved (arithmetic, var refs) defers — slice 3 territory.
77fn arg_to_concrete(e: &CExpr) -> Option<Concrete> {
78    match e {
79        CExpr::Literal { value } => Some(Concrete::from_lit(value)),
80        CExpr::UnaryOp { op, expr } if op == "-" => match expr.as_ref() {
81            CExpr::Literal { value: CLit::Int { value } } =>
82                Some(Concrete::Int(-value)),
83            CExpr::Literal { value: CLit::Float { value } } => {
84                value.parse::<f64>().ok().map(|f| Concrete::Float(-f))
85            }
86            _ => None,
87        },
88        _ => None,
89    }
90}
91
92#[derive(Debug, Clone, PartialEq)]
93enum Concrete {
94    Int(i64),
95    Float(f64),
96    Bool(bool),
97    Str(String),
98}
99
100impl Concrete {
101    fn from_lit(l: &CLit) -> Self {
102        match l {
103            CLit::Int { value } => Concrete::Int(*value),
104            CLit::Float { value } => Concrete::Float(value.parse().unwrap_or(0.0)),
105            CLit::Bool { value } => Concrete::Bool(*value),
106            CLit::Str { value } => Concrete::Str(value.clone()),
107            // Bytes / Unit are unusual in refinement contexts; surface
108            // as Unit so the predicate evaluator defers cleanly.
109            _ => Concrete::Bool(false),
110        }
111    }
112    fn show(&self) -> String {
113        match self {
114            Concrete::Int(n) => format!("{n}"),
115            Concrete::Float(f) => format!("{f}"),
116            Concrete::Bool(b) => format!("{b}"),
117            Concrete::Str(s) => format!("{s:?}"),
118        }
119    }
120}
121
122/// Tiny tree-walk evaluator for a predicate `CExpr` with a single
123/// in-scope binding. Returns `Err` for unsupported forms (caller
124/// folds these into `Deferred`).
125fn eval(e: &CExpr, name: &str, value: &Concrete) -> Result<Concrete, String> {
126    match e {
127        CExpr::Literal { value: lit } => Ok(Concrete::from_lit(lit)),
128        CExpr::Var { name: n } => {
129            if n == name { Ok(value.clone()) }
130            else { Err(format!("predicate references free var `{n}`; \
131                                slice 2 only supports the binding itself")) }
132        }
133        CExpr::UnaryOp { op, expr } => {
134            let v = eval(expr, name, value)?;
135            match (op.as_str(), v) {
136                ("not", Concrete::Bool(b)) => Ok(Concrete::Bool(!b)),
137                ("-",   Concrete::Int(n)) => Ok(Concrete::Int(-n)),
138                ("-",   Concrete::Float(n)) => Ok(Concrete::Float(-n)),
139                (o, v) => Err(format!("unsupported unary `{o}` on {}", v.show())),
140            }
141        }
142        CExpr::BinOp { op, lhs, rhs } => {
143            // Short-circuit `and` / `or` so the right side never
144            // gets evaluated when the left already decides.
145            if op == "and" || op == "or" {
146                let l = eval(lhs, name, value)?;
147                let lb = match l {
148                    Concrete::Bool(b) => b,
149                    other => return Err(format!("`{op}` on non-bool: {}", other.show())),
150                };
151                if op == "and" && !lb { return Ok(Concrete::Bool(false)); }
152                if op == "or"  &&  lb { return Ok(Concrete::Bool(true));  }
153                let r = eval(rhs, name, value)?;
154                return match r {
155                    Concrete::Bool(b) => Ok(Concrete::Bool(b)),
156                    other => Err(format!("`{op}` on non-bool: {}", other.show())),
157                };
158            }
159            let l = eval(lhs, name, value)?;
160            let r = eval(rhs, name, value)?;
161            apply_binop(op, &l, &r)
162        }
163        // Anything else (Call, Let, Match, FieldAccess, Lambda, Block,
164        // Constructors, Records, Tuples, Lists, Return) is out of
165        // slice-2 scope. Slice 3's runtime check handles these by
166        // falling back to actual evaluation under the host VM.
167        _ => Err(format!("unsupported predicate node: {e:?}")),
168    }
169}
170
171fn apply_binop(op: &str, l: &Concrete, r: &Concrete) -> Result<Concrete, String> {
172    use Concrete::*;
173    match (op, l, r) {
174        ("+", Int(a), Int(b)) => Ok(Int(a + b)),
175        ("-", Int(a), Int(b)) => Ok(Int(a - b)),
176        ("*", Int(a), Int(b)) => Ok(Int(a * b)),
177        ("/", Int(a), Int(b)) if *b != 0 => Ok(Int(a / b)),
178        ("%", Int(a), Int(b)) if *b != 0 => Ok(Int(a % b)),
179        ("+", Float(a), Float(b)) => Ok(Float(a + b)),
180        ("-", Float(a), Float(b)) => Ok(Float(a - b)),
181        ("*", Float(a), Float(b)) => Ok(Float(a * b)),
182        ("/", Float(a), Float(b)) => Ok(Float(a / b)),
183
184        ("==", a, b) => Ok(Bool(a == b)),
185        ("!=", a, b) => Ok(Bool(a != b)),
186
187        ("<",  Int(a), Int(b)) => Ok(Bool(a < b)),
188        ("<=", Int(a), Int(b)) => Ok(Bool(a <= b)),
189        (">",  Int(a), Int(b)) => Ok(Bool(a > b)),
190        (">=", Int(a), Int(b)) => Ok(Bool(a >= b)),
191
192        ("<",  Float(a), Float(b)) => Ok(Bool(a < b)),
193        ("<=", Float(a), Float(b)) => Ok(Bool(a <= b)),
194        (">",  Float(a), Float(b)) => Ok(Bool(a > b)),
195        (">=", Float(a), Float(b)) => Ok(Bool(a >= b)),
196
197        (op, a, b) => Err(format!(
198            "unsupported binop `{op}` on {} and {}", a.show(), b.show())),
199    }
200}
lex_types/discharge.rs

lex_types/
discharge.rs
