weft_lang/
project.rs

1//! **Projection** — the human-readable rendering of a Weft module.
2//!
3//! Weft has no source text: the graph is the ground truth. But *audit is a
4//! right* (spec §1.1) — commerce and Passports demand that a person can always
5//! read what a behavior does. A projection is a faithful, derived view:
6//! generated from the verified artifact on demand, never stored, never
7//! written. Local binders get generated names (`a`, `b`, `c`… by depth) since
8//! the code carries none — alpha-equivalence made visible.
9//!
10//! The projection is **deterministic**: same module, same text, always — so a
11//! rendering can be cached, diffed, and cited by the module's hash.
12
13use std::fmt::Write;
14
15use crate::{Def, EffectKind, Module, PrimOp, Term, Ty};
16
17/// Render a whole module: entry first, then every other definition, each
18/// headed by its full hash.
19pub fn module(m: &Module) -> String {
20    let mut out = String::new();
21    let _ = writeln!(out, "weft module · entry {}", m.entry);
22    let mut order: Vec<_> = m.defs.keys().collect();
23    order.sort_by_key(|h| **h != m.entry); // entry first, then hash order
24    for h in order {
25        let _ = writeln!(out, "\n{}", def(&m.defs[h]));
26        let _ = writeln!(out, "  = {}", h);
27    }
28    out
29}
30
31/// Render one definition: signature, effect row, contracts, body.
32pub fn def(d: &Def) -> String {
33    let mut out = String::new();
34    let params: Vec<String> = d
35        .params
36        .iter()
37        .enumerate()
38        .map(|(i, t)| format!("{}: {}", name(i), ty(t)))
39        .collect();
40    let _ = write!(out, "def ({}) -> {}", params.join(", "), ty(&d.ret));
41    if !d.effects.is_empty() {
42        let effs: Vec<&str> = d.effects.iter().map(|e| effect_name(*e)).collect();
43        let _ = write!(out, "\n  effects: {}", effs.join(", "));
44    }
45    let depth = d.params.len();
46    if let Some(pre) = &d.pre {
47        let _ = write!(out, "\n  requires {}", term(pre, depth));
48    }
49    if let Some(post) = &d.post {
50        let _ = write!(out, "\n  ensures {}", term(post, depth + 1));
51    }
52    let _ = write!(out, "\n  {}", term(&d.body, depth));
53    out
54}
55
56/// Binder names by depth: `a b c … z aa ab …` — stable and readable.
57fn name(depth: usize) -> String {
58    let mut n = depth;
59    let mut s = String::new();
60    loop {
61        s.insert(0, (b'a' + (n % 26) as u8) as char);
62        if n < 26 {
63            break;
64        }
65        n = n / 26 - 1;
66    }
67    s
68}
69
70fn weft_fix_scale() -> i64 {
71    crate::FIX_SCALE
72}
73
74fn ty(t: &Ty) -> String {
75    match t {
76        Ty::Int => "Int".into(),
77        Ty::Fix => "Fix".into(),
78        Ty::Bool => "Bool".into(),
79        Ty::Text => "Text".into(),
80        Ty::Action => "Action".into(),
81        Ty::List(e) => format!("List {}", ty(e)),
82        Ty::Record(fs) => {
83            let fields: Vec<String> = fs.iter().map(|(k, v)| format!("{k}: {}", ty(v))).collect();
84            format!("{{{}}}", fields.join(", "))
85        }
86    }
87}
88
89fn effect_name(e: EffectKind) -> &'static str {
90    match e {
91        EffectKind::Notify => "notify",
92        EffectKind::Navigate => "navigate",
93        EffectKind::CodexOpen => "codex.open",
94        EffectKind::CommerceBuy => "commerce.buy",
95        EffectKind::PresenceEmit => "presence.emit",
96        EffectKind::SetState => "set_state",
97        EffectKind::GiveItem => "give_item",
98        EffectKind::Despawn => "despawn",
99        EffectKind::Spawn => "spawn",
100    }
101}
102
103fn prim_name(p: PrimOp) -> &'static str {
104    match p {
105        PrimOp::Add => "+",
106        PrimOp::Sub => "-",
107        PrimOp::Mul => "*",
108        PrimOp::Div => "/",
109        PrimOp::Lt => "<",
110        PrimOp::Le => "<=",
111        PrimOp::EqInt | PrimOp::EqText => "==",
112        PrimOp::And => "and",
113        PrimOp::Or => "or",
114        PrimOp::Not => "not",
115        PrimOp::Concat => "++",
116        PrimOp::ToText => "text",
117        PrimOp::FAdd => "+.",
118        PrimOp::FSub => "-.",
119        PrimOp::FMul => "*.",
120        PrimOp::FDiv => "/.",
121        PrimOp::FLt => "<.",
122        PrimOp::FLe => "<=.",
123        PrimOp::EqFix => "==.",
124        PrimOp::FixOfInt => "fix",
125        PrimOp::IntOfFix => "trunc",
126        PrimOp::FixToText => "text",
127        PrimOp::Len => "len",
128        PrimOp::FSin => "sin",
129        PrimOp::FCos => "cos",
130        PrimOp::ListCat => "++list",
131    }
132}
133
134/// Render a term with `depth` binders in scope (params + enclosing lets).
135fn term(t: &Term, depth: usize) -> String {
136    match t {
137        Term::Int(v) => v.to_string(),
138        Term::Fix(v) => {
139            let s = weft_fix_scale();
140            let sign = if *v < 0 { "-" } else { "" };
141            let (w, f) = ((v / s).abs(), (v % s).abs());
142            if f == 0 {
143                format!("{sign}{w}.0")
144            } else {
145                format!("{sign}{w}.{}", format!("{f:06}").trim_end_matches('0'))
146            }
147        }
148        Term::Bool(b) => b.to_string(),
149        Term::Text(s) => format!("{s:?}"),
150        // de Bruijn index i → the binder `depth - 1 - i` deep.
151        Term::Var(i) => match (depth as u32).checked_sub(1 + i) {
152            Some(k) => name(k as usize),
153            None => format!("?var{i}"),
154        },
155        Term::Let(v, b) => {
156            format!(
157                "let {} = {} in\n  {}",
158                name(depth),
159                term(v, depth),
160                term(b, depth + 1)
161            )
162        }
163        Term::Map { cap, list, body } => format!(
164            "map[{cap}] {} ({} -> {})",
165            term(list, depth),
166            name(depth),
167            term(body, depth + 1)
168        ),
169        Term::Iota { cap, count } => format!("iota[{cap}] {}", term(count, depth)),
170        Term::Fold {
171            cap,
172            list,
173            init,
174            body,
175        } => format!(
176            "fold[{cap}] {} from {} ({} {} -> {})",
177            term(list, depth),
178            term(init, depth),
179            name(depth),
180            name(depth + 1),
181            term(body, depth + 2)
182        ),
183        Term::If(c, a, b) => format!(
184            "if {} then {} else {}",
185            term(c, depth),
186            term(a, depth),
187            term(b, depth)
188        ),
189        Term::Prim(PrimOp::Not, args) => format!("not {}", term(&args[0], depth)),
190        Term::Prim(PrimOp::ToText, args) => format!("text({})", term(&args[0], depth)),
191        Term::Prim(op, args) if args.len() == 2 => format!(
192            "({} {} {})",
193            term(&args[0], depth),
194            prim_name(*op),
195            term(&args[1], depth)
196        ),
197        Term::Prim(op, args) => {
198            let xs: Vec<String> = args.iter().map(|a| term(a, depth)).collect();
199            format!("{}({})", prim_name(*op), xs.join(", "))
200        }
201        Term::Rec(fields) => {
202            let fs: Vec<String> = fields
203                .iter()
204                .map(|(k, v)| format!("{k}: {}", term(v, depth)))
205                .collect();
206            format!("{{{}}}", fs.join(", "))
207        }
208        Term::Get(r, k) => format!("{}.{k}", term(r, depth)),
209        Term::ListNew(items) => {
210            let xs: Vec<String> = items.iter().map(|i| term(i, depth)).collect();
211            format!("[{}]", xs.join(", "))
212        }
213        Term::Call(h, args) => {
214            let xs: Vec<String> = args.iter().map(|a| term(a, depth)).collect();
215            format!("{:?}({})", h, xs.join(", "))
216        }
217        Term::Effect(kind, fields) => {
218            let fs: Vec<String> = fields
219                .iter()
220                .map(|(k, v)| format!("{k}: {}", term(v, depth)))
221                .collect();
222            format!("{}{{{}}}", effect_name(*kind), fs.join(", "))
223        }
224    }
225}
226
227#[cfg(test)]
228mod tests {
229    use super::*;
230    use crate::{hash_def, PrimOp, Term};
231    use std::collections::BTreeSet;
232
233    #[test]
234    fn a_projection_is_readable_and_deterministic() {
235        // inc(x) = x + 1 with a contract — the audit view a person would read.
236        let inc = Def {
237            params: vec![Ty::Int],
238            ret: Ty::Int,
239            effects: BTreeSet::new(),
240            body: Term::Prim(PrimOp::Add, vec![Term::Var(0), Term::Int(1)]),
241            pre: Some(Term::Prim(PrimOp::Le, vec![Term::Int(0), Term::Var(0)])),
242            post: Some(Term::Prim(PrimOp::Lt, vec![Term::Var(1), Term::Var(0)])),
243        };
244        let h = hash_def(&inc);
245        let m = Module::build(vec![inc], 0).unwrap();
246        let text = module(&m);
247        assert!(text.contains("def (a: Int) -> Int"), "{text}");
248        assert!(text.contains("requires (0 <= a)"), "{text}");
249        // post binds params + result: result is the innermost binder `b`.
250        assert!(text.contains("ensures (a < b)"), "{text}");
251        assert!(text.contains("(a + 1)"), "{text}");
252        assert!(text.contains(&h.to_string()), "cited by hash");
253        assert_eq!(text, module(&m), "same module, same projection, always");
254    }
255
256    #[test]
257    fn effects_and_lets_render_with_generated_names() {
258        let d = Def {
259            params: vec![Ty::Int],
260            ret: Ty::Action,
261            effects: BTreeSet::from([crate::EffectKind::Notify]),
262            body: Term::Let(
263                Box::new(Term::Prim(PrimOp::ToText, vec![Term::Var(0)])),
264                Box::new(Term::Effect(
265                    crate::EffectKind::Notify,
266                    [("text".to_string(), Term::Var(0))].into(),
267                )),
268            ),
269            pre: None,
270            post: None,
271        };
272        let text = def(&d);
273        assert!(text.contains("effects: notify"), "{text}");
274        assert!(text.contains("let b = text(a) in"), "{text}");
275        assert!(text.contains("notify{text: b}"), "{text}");
276    }
277}
weft_lang/project.rs

weft_lang/
project.rs
