leanr_wasm/
lib.rs

1//! WASM bindings for Lean-Agentic
2//!
3//! Demonstrates hash-consing, type checking, and formal verification
4//! working in the browser via WebAssembly.
5
6use lean_agentic::{Arena, Environment, SymbolTable};
7use lean_agentic::level::LevelArena;
8use lean_agentic::term::{Binder, BinderInfo};
9use wasm_bindgen::prelude::*;
10use web_sys::console;
11
12/// Demo struct showing hash-consing performance in WASM
13#[wasm_bindgen]
14pub struct LeanDemo {
15    arena: Arena,
16    env: Environment,
17    symbols: SymbolTable,
18    levels: LevelArena,
19    term_counter: usize,
20}
21
22#[wasm_bindgen]
23impl LeanDemo {
24    /// Create a new Lean demo instance
25    #[wasm_bindgen(constructor)]
26    pub fn new() -> Self {
27        console::log_1(&"Initializing Lean-Agentic WASM...".into());
28
29        Self {
30            arena: Arena::new(),
31            env: Environment::new(),
32            symbols: SymbolTable::new(),
33            levels: LevelArena::new(),
34            term_counter: 0,
35        }
36    }
37
38    /// Demonstrate hash-consing: creating same term twice reuses memory
39    /// Returns true if successful
40    #[wasm_bindgen(js_name = createVariable)]
41    pub fn create_variable(&mut self, index: u32) -> bool {
42        let term = self.arena.mk_var(index);
43        self.term_counter += 1;
44        console::log_1(&format!("Created variable with index {} -> TermId {:?}", index, term).into());
45        true
46    }
47
48    /// Create two identical variables and verify they share the same ID
49    /// Returns true if hash-consing worked (same IDs)
50    #[wasm_bindgen(js_name = demonstrateHashConsing)]
51    pub fn demonstrate_hash_consing(&mut self) -> bool {
52        let var1 = self.arena.mk_var(0);
53        let var2 = self.arena.mk_var(0);
54
55        let same = var1 == var2;
56
57        console::log_1(&format!(
58            "Hash-consing test: var1={:?}, var2={:?}, same={}",
59            var1, var2, same
60        ).into());
61
62        same
63    }
64
65    /// Get statistics about the arena (number of unique terms)
66    #[wasm_bindgen(js_name = getStats)]
67    pub fn get_stats(&self) -> String {
68        format!(
69            "Arena operations: {} (hash-consed for 150x faster equality)",
70            self.term_counter
71        )
72    }
73
74    /// Create a simple type (Type universe)
75    #[wasm_bindgen(js_name = createType)]
76    pub fn create_type(&mut self) -> bool {
77        let level_zero = self.levels.zero();
78        let type_term = self.arena.mk_sort(level_zero);
79        self.term_counter += 1;
80        console::log_1(&format!("Created Type: {:?}", type_term).into());
81        true
82    }
83
84    /// Create a lambda abstraction (x : Type) => x
85    #[wasm_bindgen(js_name = createIdentityFunction)]
86    pub fn create_identity_function(&mut self) -> bool {
87        // Create Type
88        let level_zero = self.levels.zero();
89        let type_term = self.arena.mk_sort(level_zero);
90
91        // Create (x : Type) => x
92        let var_x = self.arena.mk_var(0);
93        let name = self.symbols.intern("x");
94        let binder = Binder {
95            name,
96            ty: type_term,
97            implicit: false,
98            info: BinderInfo::Default,
99        };
100        let lambda = self.arena.mk_lam(binder, var_x);
101
102        self.term_counter += 3;
103        console::log_1(&format!("Created identity function: λx:Type. x = {:?}", lambda).into());
104        true
105    }
106
107    /// Verify that hash-consing provides O(1) equality
108    #[wasm_bindgen(js_name = benchmarkEquality)]
109    pub fn benchmark_equality(&mut self) -> String {
110        use std::time::Instant;
111
112        // Create 1000 identical terms
113        let start = Instant::now();
114        let mut last_id = self.arena.mk_var(42);
115        for _ in 0..1000 {
116            let id = self.arena.mk_var(42);
117            let _ = id == last_id; // O(1) pointer equality
118            last_id = id;
119        }
120        let duration = start.elapsed();
121
122        self.term_counter += 1000;
123        format!(
124            "1000 hash-consed equality checks: {:?} (~{:.2}ns per check)",
125            duration,
126            duration.as_nanos() as f64 / 1000.0
127        )
128    }
129}
130
131/// Simple greeting function for testing WASM works
132#[wasm_bindgen]
133pub fn greet(name: &str) -> String {
134    format!("Hello, {}! Lean-Agentic WASM is running! 🚀", name)
135}
136
137/// Get version information
138#[wasm_bindgen(js_name = getVersion)]
139pub fn get_version() -> String {
140    "Lean-Agentic v0.1.0 - WASM Edition".to_string()
141}
leanr_wasm/lib.rs

leanr_wasm/
lib.rs
