diff --git a/rust-engine/src/backends/lean.rs b/rust-engine/src/backends/lean.rs index 701f64e5a..2b0f675be 100644 --- a/rust-engine/src/backends/lean.rs +++ b/rust-engine/src/backends/lean.rs @@ -1,8 +1,7 @@ //! The Lean backend //! //! This module defines the trait implementations to export the rust ast to -//! Pretty::Doc type, which can in turn be exported to string (or, eventually, -//! source maps). +//! Pretty::Doc type, which can in turn be exported to string and source maps. use std::collections::HashSet; use std::sync::OnceLock; @@ -224,18 +223,31 @@ impl Backend for LeanBackend { return vec![]; } let path = self.module_path(modules.first().unwrap()).to_string(); - let contents = modules - .into_iter() - .map(|module: Module| { - let (c, _) = printer.print(module); - c - }) - .collect::>() - .join("\n"); + + // The HEADER is prepended to the generated content, so all generated + // line numbers must be shifted by the number of lines in HEADER. + let header_line_count = HEADER.chars().filter(|&c| c == '\n').count() as u32; + + let mut all_raw: Vec<(u32, u32, String, u32, u32)> = vec![]; + let mut parts: Vec = vec![]; + let mut line_offset: u32 = header_line_count; + + for module in modules { + let (content, sm) = printer.print(module); + for (gl, gc, src, sl, sc) in sm.raw { + all_raw.push((gl + line_offset, gc, src, sl, sc)); + } + line_offset += + content.chars().filter(|&c| c == '\n').count() as u32 + 1 /* "\n" join */; + parts.push(content); + } + + let contents = format!("{}{}", HEADER, parts.join("\n")); + let sourcemap = SourceMap { raw: all_raw }.to_engine_sourcemap(&path); vec![File { path, - contents: format!("{}{}", HEADER, contents), - sourcemap: None, + contents, + sourcemap, }] } } @@ -316,7 +328,7 @@ impl LeanPrinter { } /// Render parameters, adding a line after each parameter -impl ToDocument for Vec { +impl> ToDocument for Vec { fn to_document(&self, printer: &LeanPrinter) -> DocBuilder { printer.params(self) } @@ -358,7 +370,7 @@ const _: () = { impl LeanPrinter { /// Prints arguments a variant or constructor of struct, using named or unamed arguments based /// on the `is_record` flag. Used for both expressions and patterns - pub fn arguments( + pub fn arguments, D>( &self, fields: &[(GlobalId, D)], is_record: &bool, @@ -374,7 +386,7 @@ const _: () = { } /// Prints fields of structures (when in braced notation) - fn struct_fields(&self, fields: &[(GlobalId, D)]) -> DocBuilder + fn struct_fields, D>(&self, fields: &[(GlobalId, D)]) -> DocBuilder where D: ToDocument, { @@ -387,7 +399,7 @@ const _: () = { .group() } /// Prints named arguments (record) of a variant or constructor of struct - fn named_arguments(&self, fields: &[(GlobalId, D)]) -> DocBuilder + fn named_arguments, D>(&self, fields: &[(GlobalId, D)]) -> DocBuilder where D: ToDocument, { @@ -403,7 +415,7 @@ const _: () = { } /// Prints positional arguments (tuple) of a variant or constructor of struct - fn positional_arguments( + fn positional_arguments, D>( &self, fields: &[(GlobalId, D)], ) -> DocBuilder @@ -414,12 +426,12 @@ const _: () = { } /// Prints parameters of functions (items, trait items, impl items) - fn params(&self, params: &Vec) -> DocBuilder { + fn params>(&self, params: &Vec) -> DocBuilder { zip_left!(line!(), params) } /// Print parameters as function arguments - fn params_as_args(&self, params: &[Param]) -> DocBuilder { + fn params_as_args>(&self, params: &[Param]) -> DocBuilder { zip_left!( line!(), params.iter().map(|param| { @@ -439,7 +451,7 @@ const _: () = { /// Renders expressions with an explicit ascription `(e : RustM ty)`. Used for the body of closure, for /// numeric literals, etc. - fn expr_typed_result(&self, expr: &Expr) -> DocBuilder { + fn expr_typed_result>(&self, expr: &Expr) -> DocBuilder { docs![ expr, softline!(), @@ -450,11 +462,11 @@ const _: () = { .group() } - fn pat_typed(&self, pat: &Pat) -> DocBuilder { + fn pat_typed>(&self, pat: &Pat) -> DocBuilder { docs![pat, reflow!(" :"), line!(), &pat.ty].parens().group() } - fn do_block>(&self, body: D) -> DocBuilder { + fn do_block, D: ToDocument>(&self, body: D) -> DocBuilder { docs!["do", line!(), body].group() } @@ -467,7 +479,7 @@ const _: () = { /// Renders a named argument for associated types with equality constraints /// (aka projections). If there are no equality constraints, returns None. - fn associated_type_projections( + fn associated_type_projections>( &self, impl_ident: &ImplIdent, projections: Vec>, @@ -504,7 +516,7 @@ const _: () = { /// Turns an expression of type `RustM T` into one of type `T` (out of the monad), providing /// reflexivity as a proof witness. - fn monad_extract(&self, expr: &Expr) -> DocBuilder { + fn monad_extract>(&self, expr: &Expr) -> DocBuilder { if let ExprKind::Literal(_) | ExprKind::GlobalId(_) | ExprKind::LocalId(_) = expr.kind() { // Pure values are displayed directly. Note that constructors, while pure, may @@ -525,7 +537,7 @@ const _: () = { } /// When possible, unwraps the `pure` surrounding an expression to simplify it - fn monad_extract_simplify(&self, expr: &Expr) -> DocBuilder { + fn monad_extract_simplify>(&self, expr: &Expr) -> DocBuilder { if let ExprKind::App { head, args, .. } = expr.kind() && let ExprKind::GlobalId(PURE) = head.kind() && let [pure_expr] = &args[..] @@ -537,7 +549,7 @@ const _: () = { } /// Print trait items, adding trait-level params as extra arguments - fn trait_item_with_trait_params( + fn trait_item_with_trait_params>( &self, trait_generics: &[GenericParam], TraitItem { @@ -608,7 +620,7 @@ const _: () = { } // Print generics, using `name` as a prefix for constraint names - fn generics( + fn generics>( &self, generics: &Generics, name: &String, @@ -667,7 +679,7 @@ const _: () = { } /// Print spec of an item - fn spec( + fn spec>( &self, item: &Item, name: &GlobalId, @@ -794,13 +806,13 @@ const _: () = { } } - impl ToDocument for (Vec, &TraitItem) { + impl> ToDocument for (Vec, &TraitItem) { fn to_document(&self, printer: &LeanPrinter) -> DocBuilder { printer.trait_item_with_trait_params(&self.0, self.1) } } - impl PrettyAst for LeanPrinter { + impl> PrettyAst for LeanPrinter { const NAME: &'static str = "Lean"; /// Produce a non-panicking placeholder document. In general, prefer the use of the helper macro [`todo_document!`]. diff --git a/rust-engine/src/backends/rust.rs b/rust-engine/src/backends/rust.rs index 5e93ea5eb..601444c97 100644 --- a/rust-engine/src/backends/rust.rs +++ b/rust-engine/src/backends/rust.rs @@ -1,7 +1,7 @@ //! A Rust backend (and printer) for hax. use super::prelude::*; -use crate::ast::identifiers::global_id::view::{PathSegment, View}; +use crate::ast::{identifiers::global_id::view::{PathSegment, View}, span::Span}; use std::cell::RefCell; mod renamings; @@ -133,14 +133,14 @@ const _: () = { } impl<'a, 'b> RustPrinter { - fn generic_params(&'a self, generic_params: &'b [GenericParam]) -> DocBuilder { + fn generic_params>(&'a self, generic_params: &'b [GenericParam]) -> DocBuilder { let generic_params = generic_params .iter() .filter(|p| !matches!(&p.kind, GenericParamKind::Lifetime if p.ident.0.to_string() == "_")) .collect::>(); sep_opt!("<", generic_params, ">") } - fn where_clause(&'a self, constraints: &'b [GenericConstraint]) -> DocBuilder { + fn where_clause>(&'a self, constraints: &'b [GenericConstraint]) -> DocBuilder { if constraints.is_empty() { return nil!(); } @@ -156,7 +156,7 @@ const _: () = { .nest(INDENT) .group() } - fn attributes(&'a self, attrs: &'b [Attribute]) -> DocBuilder { + fn attributes>(&'a self, attrs: &'b [Attribute]) -> DocBuilder { concat!( attrs .iter() @@ -168,7 +168,7 @@ const _: () = { ) } - fn id_name(&'a self, id: GlobalId) -> DocBuilder { + fn id_name>(&'a self, id: GlobalId) -> DocBuilder { let view = id.view(); let path = ::render_strings(self, &view); let name = path.last().unwrap().clone(); @@ -180,7 +180,7 @@ const _: () = { } } - impl PrettyAst for RustPrinter { + impl> PrettyAst for RustPrinter { const NAME: &'static str = "Rust"; fn module(&self, module: &Module) -> DocBuilder { diff --git a/rust-engine/src/printer.rs b/rust-engine/src/printer.rs index 015eaedb1..9dcb21905 100644 --- a/rust-engine/src/printer.rs +++ b/rust-engine/src/printer.rs @@ -9,7 +9,7 @@ //! - The resugaring pipeline: a sequence of local AST rewrites that make //! emitted code idiomatic for the target language before pretty-printing. -use std::ops::Deref; +use std::{fmt, ops::Deref}; use crate::{ ast::{self, span::Span}, @@ -17,6 +17,7 @@ use crate::{ printer::pretty_ast::ToDocument, }; use ast::visitors::dyn_compatible; +use pretty::RenderAnnotated; pub mod pretty_ast; pub use pretty_ast::PrettyAst; @@ -54,9 +55,194 @@ pub trait HasLinkedItemGraph { fn with_linked_item_graph(self, graph: std::rc::Rc) -> Self; } -#[derive(Clone, Debug, serde::Serialize, serde::Deserialize)] -/// Placeholder type for sourcemaps. -pub struct SourceMap; +/// Raw source map data collected during rendering. +/// +/// Each entry is `(gen_line, gen_col, source_path, src_line, src_col)` where +/// all values are 0-indexed. +#[derive(Clone, Debug, Default, serde::Serialize, serde::Deserialize)] +pub struct SourceMap { + /// Mappings as `(gen_line, gen_col, source_path, src_line, src_col)`, all 0-indexed. + pub raw: Vec<(u32, u32, String, u32, u32)>, +} + +impl SourceMap { + /// Encode the collected mappings into a source map v3 + /// [`hax_types::engine_api::SourceMap`]. + /// + /// Returns `None` when there are no mappings (e.g. for backends that do + /// not override [`PrettyAst::annotate_with_span`]). + pub fn to_engine_sourcemap( + &self, + file: &str, + ) -> Option { + if self.raw.is_empty() { + return None; + } + + // Collect unique source paths while preserving insertion order. + let mut sources: Vec = vec![]; + for (_, _, src, _, _) in &self.raw { + if !sources.contains(src) { + sources.push(src.clone()); + } + } + + // Sort mappings by generated position. + let mut mappings = self.raw.clone(); + mappings.sort_by_key(|&(gl, gc, _, _, _)| (gl, gc)); + + // Encode as source map v3 VLQ. + let encoded = encode_mappings(&mappings, &sources); + + Some(hax_types::engine_api::SourceMap { + version: 3, + file: file.to_string(), + sourceRoot: String::new(), + sourcesContent: sources.iter().map(|_| None).collect(), + sources, + names: vec![], + mappings: encoded, + }) + } +} + +// --------------------------------------------------------------------------- +// VLQ / source-map v3 encoding +// --------------------------------------------------------------------------- + +const BASE64_CHARS: &[u8] = b"ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz0123456789+/"; + +/// Encode a single signed integer as VLQ base64. +fn vlq_encode(value: i64, out: &mut String) { + // The first group encodes the sign in its lowest bit. + let mut encoded = if value < 0 { + ((-value) << 1) | 1 + } else { + value << 1 + }; + loop { + let mut digit = encoded & 0x1F; // 5 bits + encoded >>= 5; + if encoded > 0 { + digit |= 0x20; // set continuation bit + } + out.push(BASE64_CHARS[digit as usize] as char); + if encoded == 0 { + break; + } + } +} + +/// Encode all mappings into the source map v3 `mappings` string. +fn encode_mappings( + mappings: &[(u32, u32, String, u32, u32)], + sources: &[String], +) -> String { + let mut result = String::new(); + let mut prev_gen_line: u32 = 0; + let mut prev_gen_col: i64 = 0; + let mut prev_src_idx: i64 = 0; + let mut prev_src_line: i64 = 0; + let mut prev_src_col: i64 = 0; + let mut first_on_line = true; + + for &(gen_line, gen_col, ref source, src_line, src_col) in mappings { + // Advance to the correct line with semicolons. + while prev_gen_line < gen_line { + result.push(';'); + prev_gen_line += 1; + prev_gen_col = 0; + first_on_line = true; + } + + if !first_on_line { + result.push(','); + } + first_on_line = false; + + let src_idx = sources.iter().position(|s| s == source).unwrap_or(0) as i64; + + // generated column (relative) + vlq_encode(gen_col as i64 - prev_gen_col, &mut result); + // source file index (relative) + vlq_encode(src_idx - prev_src_idx, &mut result); + // original line (relative) + vlq_encode(src_line as i64 - prev_src_line, &mut result); + // original column (relative) + vlq_encode(src_col as i64 - prev_src_col, &mut result); + + prev_gen_col = gen_col as i64; + prev_src_idx = src_idx; + prev_src_line = src_line as i64; + prev_src_col = src_col as i64; + } + + result +} + +// --------------------------------------------------------------------------- +// SourceMapWriter: a writer that collects span annotations while rendering +// --------------------------------------------------------------------------- + +/// A writer implementing [`pretty::RenderAnnotated`] that both accumulates +/// rendered text and records source-map mappings whenever a [`Span`] annotation +/// is pushed. +#[derive(Default)] +pub struct SourceMapWriter { + /// The fully rendered output string. + pub output: String, + /// 0-indexed current line in the output. + current_line: u32, + /// 0-indexed current column in the output. + current_col: u32, + /// Collected raw mappings (see [`SourceMap::raw`]). + pub raw_mappings: Vec<(u32, u32, String, u32, u32)>, +} + +impl pretty::Render for SourceMapWriter { + type Error = fmt::Error; + + fn write_str(&mut self, s: &str) -> Result { + for ch in s.chars() { + if ch == '\n' { + self.current_line += 1; + self.current_col = 0; + } else { + self.current_col += 1; + } + } + self.output.push_str(s); + Ok(s.len()) + } + + fn fail_doc(&self) -> fmt::Error { + fmt::Error + } +} + +impl<'a> RenderAnnotated<'a, Span> for SourceMapWriter { + fn push_annotation(&mut self, span: &'a Span) -> Result<(), fmt::Error> { + if let Some(fe_span) = span.as_frontend_spans().first() { + // Only record mappings for real source files. + if fe_span.filename.to_path().is_some() { + let source = fe_span.filename.to_string(); + self.raw_mappings.push(( + self.current_line, + self.current_col, + source, + // frontend spans are 1-indexed; source map v3 is 0-indexed + fe_span.lo.line.saturating_sub(1) as u32, + fe_span.lo.col as u32, + )); + } + } + Ok(()) + } + + fn pop_annotation(&mut self) -> Result<(), fmt::Error> { + Ok(()) + } +} /// Helper trait to print AST fragments. pub trait Print @@ -83,11 +269,10 @@ where T: ToDocument, { let doc_builder = fragment.to_document(self).into_doc(); - ( - doc_builder.deref().pretty(80).to_string(), - SourceMap, - fragment, - ) + let mut writer = SourceMapWriter::default(); + doc_builder.deref().render_raw(80, &mut writer).ok(); + let source_map = SourceMap { raw: writer.raw_mappings }; + (writer.output, source_map, fragment) } fn print(&mut self, fragment: T) -> (String, SourceMap) diff --git a/rust-engine/src/printer/pretty_ast.rs b/rust-engine/src/printer/pretty_ast.rs index b816cef15..f8fedfec1 100644 --- a/rust-engine/src/printer/pretty_ast.rs +++ b/rust-engine/src/printer/pretty_ast.rs @@ -287,7 +287,7 @@ pub trait PrettyAstExt: Sized { } } -impl> PrettyAstExt for P {} +impl, P: PrettyAst> PrettyAstExt for P {} /// Generate a dispatcher macro that forwards a token to specialised macros. macro_rules! make_cases_macro { @@ -364,7 +364,7 @@ macro_rules! mk { /// Note that using `install_pretty_helpers!` will produce macro /// that implicitely use `self` as allocator. Take a look at a /// printer in the [`backends`] module for an example. - pub trait PrettyAst: Sized + HasContextualSpan { + pub trait PrettyAst>: Sized + HasContextualSpan { /// A name for this instance of `PrettyAst`. /// Useful for diagnostics and debugging. const NAME: &'static str; @@ -420,7 +420,7 @@ macro_rules! mk { $( method_deny_list!($ty{ - impl> ToDocument for $ty { + impl, P: PrettyAst> ToDocument for $ty { fn to_document(&self, printer: &P) -> DocBuilder { span_handling!($ty{ let printer = &(printer.with_span(self.span())); @@ -430,7 +430,11 @@ macro_rules! mk { // Here is the place we (will) take care of spans, etc. #[allow(deprecated)] let print =

>::[<$ty:snake>]; - print(printer, self) + let doc = print(printer, self); + span_handling!($ty{ + let doc = doc.annotate(A::from(self.span())); + }); + doc } } }); diff --git a/tools/vscode-hax-sourcemap/.vscodeignore b/tools/vscode-hax-sourcemap/.vscodeignore new file mode 100644 index 000000000..f8f5bb1bb --- /dev/null +++ b/tools/vscode-hax-sourcemap/.vscodeignore @@ -0,0 +1,5 @@ +.vscode/** +.vscode-test/** +src/** +.gitignore +tsconfig.json diff --git a/tools/vscode-hax-sourcemap/out/extension.js b/tools/vscode-hax-sourcemap/out/extension.js new file mode 100644 index 000000000..2c4db1432 --- /dev/null +++ b/tools/vscode-hax-sourcemap/out/extension.js @@ -0,0 +1,655 @@ +"use strict"; +Object.defineProperty(exports, "__esModule", { value: true }); +exports.activate = activate; +exports.deactivate = deactivate; +const vscode = require("vscode"); +const path = require("path"); +const fs = require("fs"); +// ───────────────────────────────────────────────────────────────────────────── +// VLQ / Source Map v3 decoder +// ───────────────────────────────────────────────────────────────────────────── +const BASE64 = 'ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz0123456789+/'; +const B64 = {}; +for (let i = 0; i < BASE64.length; i++) + B64[BASE64[i]] = i; +function decodeVlq(s, pos) { + let result = 0, shift = 0; + for (;;) { + const digit = B64[s[pos++]]; + result |= (digit & 31) << shift; + shift += 5; + if (!(digit & 32)) { + break; + } + } + return [(result & 1) ? -(result >>> 1) : (result >>> 1), pos]; +} +// ───────────────────────────────────────────────────────────────────────────── +// Source map parsing +// ───────────────────────────────────────────────────────────────────────────── +function decodeSourceMap(mapFilePath) { + let raw; + try { + raw = JSON.parse(fs.readFileSync(mapFilePath, 'utf8')); + } + catch { + return null; + } + const sources = raw.sources ?? []; + const sourcesContent = raw.sourcesContent ?? sources.map(() => null); + const encoded = raw.mappings ?? ''; + const mappings = []; + let genLine = 0; + let pGC = 0, pSI = 0, pSL = 0, pSC = 0; + for (let i = 0; i < encoded.length;) { + const ch = encoded[i]; + if (ch === ';') { + genLine++; + pGC = 0; + i++; + continue; + } + if (ch === ',') { + i++; + continue; + } + let dGC; + [dGC, i] = decodeVlq(encoded, i); + const genCol = pGC + dGC; + pGC = genCol; + if (i >= encoded.length || encoded[i] === ';' || encoded[i] === ',') { + continue; + } + let dSI, dSL, dSC; + [dSI, i] = decodeVlq(encoded, i); + [dSL, i] = decodeVlq(encoded, i); + [dSC, i] = decodeVlq(encoded, i); + // optional name index + if (i < encoded.length && encoded[i] !== ';' && encoded[i] !== ',') { + [, i] = decodeVlq(encoded, i); + } + pSI += dSI; + pSL += dSL; + pSC += dSC; + mappings.push({ genLine, genCol, srcIdx: pSI, srcLine: pSL, srcCol: pSC }); + } + const resolvedPaths = resolveSources(sources, mapFilePath); + return { mappings, sources, sourcesContent, resolvedPaths }; +} +function normPath(p) { + try { + return fs.realpathSync(p); + } + catch { + return path.resolve(p); + } +} +function resolveSources(sources, mapFilePath) { + const resolved = new Map(); + const mapDir = path.dirname(mapFilePath); + for (let idx = 0; idx < sources.length; idx++) { + const src = sources[idx]; + if (!src) { + continue; + } + const tryAdd = (p) => { + if (fs.existsSync(p)) { + resolved.set(idx, normPath(p)); + return true; + } + return false; + }; + if (path.isAbsolute(src)) { + tryAdd(src); + continue; + } + // Workspace roots + let found = false; + for (const folder of vscode.workspace.workspaceFolders ?? []) { + if (tryAdd(path.join(folder.uri.fsPath, src))) { + found = true; + break; + } + } + if (found) { + continue; + } + // Walk up from map file + let dir = mapDir; + for (let depth = 0; depth < 12; depth++) { + if (tryAdd(path.join(dir, src))) { + break; + } + const parent = path.dirname(dir); + if (parent === dir) { + break; + } + dir = parent; + } + } + return resolved; +} +// ───────────────────────────────────────────────────────────────────────────── +// Colour palette +// ───────────────────────────────────────────────────────────────────────────── +// 8-colour palette, legible on dark and light themes. +const PALETTE = [ + { r: 224, g: 108, b: 117 }, // red + { r: 229, g: 192, b: 123 }, // amber + { r: 152, g: 195, b: 121 }, // green + { r: 86, g: 182, b: 194 }, // cyan + { r: 97, g: 175, b: 239 }, // blue + { r: 198, g: 120, b: 221 }, // purple + { r: 209, g: 154, b: 102 }, // orange + { r: 171, g: 178, b: 191 }, // slate +]; +const N = PALETTE.length; +function rgba(c, a) { + return `rgba(${c.r},${c.g},${c.b},${a})`; +} +function makeDecTypes(bgAlpha) { + const bg = []; + const active = []; + for (const c of PALETTE) { + bg.push(vscode.window.createTextEditorDecorationType({ + backgroundColor: rgba(c, bgAlpha), + isWholeLine: true, + overviewRulerColor: rgba(c, 0.6), + overviewRulerLane: vscode.OverviewRulerLane.Left, + })); + active.push(vscode.window.createTextEditorDecorationType({ + backgroundColor: rgba(c, Math.min(1, bgAlpha * 2.8)), + isWholeLine: true, + border: `0 0 0 3px solid ${rgba(c, 0.9)}`, + overviewRulerColor: rgba(c, 1.0), + overviewRulerLane: vscode.OverviewRulerLane.Full, + })); + } + return { bg, active }; +} +// ───────────────────────────────────────────────────────────────────────────── +// Manager +// ───────────────────────────────────────────────────────────────────────────── +class HaxManager { + constructor(ctx) { + this.ctx = ctx; + this.smCache = new Map(); + this.colorMapCache = new Map(); + /** rust absolute path → lean absolute paths that reference it */ + this.rustToLean = new Map(); + const cfg = vscode.workspace.getConfiguration('hax.sourcemap'); + this.rainbowEnabled = cfg.get('rainbowOnOpen', true); + this.decTypes = makeDecTypes(cfg.get('rainbowOpacity', 0.07)); + this.statusBar = vscode.window.createStatusBarItem(vscode.StatusBarAlignment.Right, 100); + this.statusBar.command = 'hax.jumpToSource'; + ctx.subscriptions.push(this.statusBar); + ctx.subscriptions.push(vscode.workspace.onDidChangeConfiguration(e => { + if (!e.affectsConfiguration('hax.sourcemap')) { + return; + } + const newCfg = vscode.workspace.getConfiguration('hax.sourcemap'); + this.rainbowEnabled = newCfg.get('rainbowOnOpen', true); + // Dispose old decoration types and recreate with new opacity. + for (const d of [...this.decTypes.bg, ...this.decTypes.active]) { + d.dispose(); + } + this.decTypes = makeDecTypes(newCfg.get('rainbowOpacity', 0.07)); + for (const editor of vscode.window.visibleTextEditors) { + this.update(editor); + } + })); + } + // ── Source map access ──────────────────────────────────────────────────── + loadSourceMap(leanPath) { + if (this.smCache.has(leanPath)) { + return this.smCache.get(leanPath); + } + const mapPath = leanPath + '.map'; + const sm = fs.existsSync(mapPath) ? decodeSourceMap(mapPath) : null; + this.smCache.set(leanPath, sm); + if (sm) { + this.colorMapCache.set(leanPath, buildColorMap(sm)); + for (const [, resolved] of sm.resolvedPaths) { + if (!this.rustToLean.has(resolved)) { + this.rustToLean.set(resolved, new Set()); + } + this.rustToLean.get(resolved).add(leanPath); + } + // Update context key for rust files + vscode.commands.executeCommand('setContext', 'hax.hasReverseMap', this.rustToLean.size > 0); + } + return sm; + } + getColorMap(leanPath) { + if (this.colorMapCache.has(leanPath)) { + return this.colorMapCache.get(leanPath); + } + const sm = this.loadSourceMap(leanPath); + if (!sm) { + return new Map(); + } + const cm = buildColorMap(sm); + this.colorMapCache.set(leanPath, cm); + return cm; + } + // ── Main update entry ──────────────────────────────────────────────────── + update(editor) { + const p = editor.document.uri.fsPath; + if (p.endsWith('.lean')) { + this.updateLean(editor); + } + else if (p.endsWith('.rs')) { + this.updateRust(editor); + } + } + // ── Lean file update ───────────────────────────────────────────────────── + updateLean(editor) { + const leanPath = editor.document.uri.fsPath; + const sm = this.loadSourceMap(leanPath); + if (!sm) { + this.clearAll(editor); + this.statusBar.hide(); + vscode.commands.executeCommand('setContext', 'hax.hasSourceMap', false); + return; + } + vscode.commands.executeCommand('setContext', 'hax.hasSourceMap', true); + const colorMap = this.getColorMap(leanPath); + const cursor = editor.selection.active; + // Rainbow background + if (this.rainbowEnabled) { + const buckets = Array.from({ length: N }, () => []); + for (const [line, ci] of colorMap) { + buckets[ci].push(new vscode.Range(line, 0, line, 0)); + } + for (let i = 0; i < N; i++) { + editor.setDecorations(this.decTypes.bg[i], buckets[i]); + } + } + else { + for (let i = 0; i < N; i++) { + editor.setDecorations(this.decTypes.bg[i], []); + } + } + // Active cursor highlight + const activeMappings = findActiveSegment(sm, colorMap, cursor.line, cursor.character); + for (let i = 0; i < N; i++) { + editor.setDecorations(this.decTypes.active[i], []); + } + if (activeMappings.length > 0) { + const ci = colorMap.get(activeMappings[0].genLine) ?? 0; + editor.setDecorations(this.decTypes.active[ci], activeMappings.map(m => new vscode.Range(m.genLine, 0, m.genLine, 0))); + const rep = activeMappings[0]; + const srcPath = sm.resolvedPaths.get(rep.srcIdx) ?? sm.sources[rep.srcIdx] ?? '?'; + this.statusBar.text = `$(link) ${path.basename(srcPath)}:${rep.srcLine + 1}`; + this.statusBar.tooltip = `Rust source: ${srcPath}:${rep.srcLine + 1}:${rep.srcCol + 1}\nClick to jump`; + this.statusBar.show(); + // Highlight paired rust editors + for (const ve of vscode.window.visibleTextEditors) { + if (ve.document.uri.fsPath.endsWith('.rs')) { + this.applyRainbowToRust(ve, sm, colorMap, leanPath, rep, ci); + } + } + } + else { + this.statusBar.hide(); + // Still paint rainbow on rust if visible + for (const ve of vscode.window.visibleTextEditors) { + if (ve.document.uri.fsPath.endsWith('.rs')) { + this.applyRainbowToRust(ve, sm, colorMap, leanPath, null, -1); + } + } + } + } + // ── Rust file update ───────────────────────────────────────────────────── + updateRust(editor) { + const rustPath = normPath(editor.document.uri.fsPath); + // Ensure lean source maps are loaded for any open lean editors + for (const ve of vscode.window.visibleTextEditors) { + if (ve.document.fileName.endsWith('.lean')) { + this.loadSourceMap(ve.document.uri.fsPath); + } + } + const leanPaths = this.rustToLean.get(rustPath); + if (!leanPaths || leanPaths.size === 0) { + this.clearAll(editor); + return; + } + vscode.commands.executeCommand('setContext', 'hax.hasReverseMap', true); + const cursor = editor.selection.active; + for (const leanPath of leanPaths) { + const sm = this.loadSourceMap(leanPath); + if (!sm) { + continue; + } + const colorMap = this.getColorMap(leanPath); + const srcIdx = [...sm.resolvedPaths.entries()].find(([, p]) => p === rustPath)?.[0]; + if (srcIdx === undefined) { + continue; + } + this.applyRainbowToRust(editor, sm, colorMap, leanPath, null, -1); + // Active: highlight current rust line + const rustLineMappings = sm.mappings.filter(m => m.srcIdx === srcIdx && m.srcLine === cursor.line); + if (rustLineMappings.length > 0) { + const ci = colorMap.get(rustLineMappings[0].genLine) ?? 0; + for (let i = 0; i < N; i++) { + editor.setDecorations(this.decTypes.active[i], []); + } + editor.setDecorations(this.decTypes.active[ci], [new vscode.Range(cursor.line, 0, cursor.line, 0)]); + } + // Highlight lean editor if visible + for (const ve of vscode.window.visibleTextEditors) { + if (ve.document.uri.fsPath !== leanPath) { + continue; + } + const leanMappings = sm.mappings.filter(m => m.srcIdx === srcIdx && m.srcLine === cursor.line); + for (let i = 0; i < N; i++) { + ve.setDecorations(this.decTypes.active[i], []); + } + if (leanMappings.length > 0) { + const ci = colorMap.get(leanMappings[0].genLine) ?? 0; + ve.setDecorations(this.decTypes.active[ci], leanMappings.map(m => new vscode.Range(m.genLine, 0, m.genLine, 0))); + } + } + } + } + applyRainbowToRust(editor, sm, colorMap, _leanPath, activeMapping, activeCi) { + const rustPath = normPath(editor.document.uri.fsPath); + const srcIdx = [...sm.resolvedPaths.entries()].find(([, p]) => p === rustPath)?.[0]; + if (srcIdx === undefined) { + return; + } + if (this.rainbowEnabled) { + // Build rust-line → colorIdx (one representative per source line). + const rustLineColor = new Map(); + for (const m of sm.mappings) { + if (m.srcIdx !== srcIdx) { + continue; + } + if (rustLineColor.has(m.srcLine)) { + continue; + } + const ci = colorMap.get(m.genLine); + if (ci !== undefined) { + rustLineColor.set(m.srcLine, ci); + } + } + // Sort and build contiguous ranges so gaps between mapped lines are filled. + const sorted = [...rustLineColor.entries()].sort((a, b) => a[0] - b[0]); + const buckets = Array.from({ length: N }, () => []); + for (let i = 0; i < sorted.length; i++) { + const [startLine, ci] = sorted[i]; + const endLine = i + 1 < sorted.length ? sorted[i + 1][0] - 1 : startLine; + buckets[ci].push(new vscode.Range(startLine, 0, endLine, 0)); + } + for (let i = 0; i < N; i++) { + editor.setDecorations(this.decTypes.bg[i], buckets[i]); + } + } + if (activeMapping !== null && activeMapping.srcIdx === srcIdx) { + for (let i = 0; i < N; i++) { + editor.setDecorations(this.decTypes.active[i], []); + } + editor.setDecorations(this.decTypes.active[activeCi], [new vscode.Range(activeMapping.srcLine, 0, activeMapping.srcLine, 0)]); + } + } + clearAll(editor) { + for (let i = 0; i < N; i++) { + editor.setDecorations(this.decTypes.bg[i], []); + editor.setDecorations(this.decTypes.active[i], []); + } + } + // ── Commands ───────────────────────────────────────────────────────────── + async jumpToSource() { + const editor = vscode.window.activeTextEditor; + if (!editor || !editor.document.fileName.endsWith('.lean')) { + return; + } + const sm = this.loadSourceMap(editor.document.uri.fsPath); + if (!sm) { + vscode.window.showWarningMessage('Hax: no source map found for this file.'); + return; + } + const cursor = editor.selection.active; + const m = closestMapping(sm.mappings, cursor.line, cursor.character); + if (!m) { + vscode.window.showWarningMessage('Hax: no mapping at cursor position.'); + return; + } + const resolved = sm.resolvedPaths.get(m.srcIdx); + if (!resolved) { + const content = sm.sourcesContent[m.srcIdx]; + if (content) { + const doc = await vscode.workspace.openTextDocument({ + language: 'rust', + content: `// Source: ${sm.sources[m.srcIdx]}\n// (file not found on disk)\n\n${content}`, + }); + const te = await vscode.window.showTextDocument(doc, vscode.ViewColumn.Beside); + const pos = new vscode.Position(m.srcLine + 3 /* header offset */, m.srcCol); + te.selection = new vscode.Selection(pos, pos); + te.revealRange(new vscode.Range(pos, pos), vscode.TextEditorRevealType.InCenter); + } + else { + vscode.window.showWarningMessage(`Hax: source file not found: ${sm.sources[m.srcIdx]}`); + } + return; + } + const doc = await vscode.workspace.openTextDocument(vscode.Uri.file(resolved)); + const te = await vscode.window.showTextDocument(doc, vscode.ViewColumn.Beside); + const pos = new vscode.Position(m.srcLine, m.srcCol); + te.selection = new vscode.Selection(pos, pos); + te.revealRange(new vscode.Range(pos, pos), vscode.TextEditorRevealType.InCenter); + } + async jumpToLean() { + const editor = vscode.window.activeTextEditor; + if (!editor) { + return; + } + const rustPath = editor.document.uri.fsPath; + // Eagerly load source maps for open lean editors + for (const ve of vscode.window.visibleTextEditors) { + if (ve.document.fileName.endsWith('.lean')) { + this.loadSourceMap(ve.document.uri.fsPath); + } + } + let leanPaths = this.rustToLean.get(rustPath); + // If still empty, search workspace for .lean.map files + if (!leanPaths || leanPaths.size === 0) { + const maps = await vscode.workspace.findFiles('**/*.lean.map', '**/node_modules/**', 20); + for (const mapUri of maps) { + const leanPath = mapUri.fsPath.replace(/\.map$/, ''); + this.loadSourceMap(leanPath); + } + leanPaths = this.rustToLean.get(rustPath); + } + if (!leanPaths || leanPaths.size === 0) { + vscode.window.showWarningMessage('Hax: no Lean extraction found for this Rust file.'); + return; + } + const cursorLine = editor.selection.active.line; + for (const leanPath of leanPaths) { + const sm = this.loadSourceMap(leanPath); + if (!sm) { + continue; + } + const srcIdx = [...sm.resolvedPaths.entries()].find(([, p]) => p === rustPath)?.[0]; + if (srcIdx === undefined) { + continue; + } + const candidates = sm.mappings + .filter(m => m.srcIdx === srcIdx && m.srcLine <= cursorLine + 5) + .sort((a, b) => Math.abs(a.srcLine - cursorLine) - Math.abs(b.srcLine - cursorLine)); + if (candidates.length === 0) { + continue; + } + const best = candidates[0]; + const doc = await vscode.workspace.openTextDocument(vscode.Uri.file(leanPath)); + const te = await vscode.window.showTextDocument(doc, vscode.ViewColumn.Beside); + const pos = new vscode.Position(best.genLine, best.genCol); + te.selection = new vscode.Selection(pos, pos); + te.revealRange(new vscode.Range(pos, pos), vscode.TextEditorRevealType.InCenter); + return; + } + vscode.window.showWarningMessage('Hax: no mapping found near cursor position.'); + } + toggleRainbow() { + this.rainbowEnabled = !this.rainbowEnabled; + vscode.window.showInformationMessage(`Hax rainbow colours ${this.rainbowEnabled ? 'enabled' : 'disabled'}`); + for (const editor of vscode.window.visibleTextEditors) { + this.update(editor); + } + } + invalidateCache() { + this.smCache.clear(); + this.colorMapCache.clear(); + this.rustToLean.clear(); + } +} +// ───────────────────────────────────────────────────────────────────────────── +// Pure helpers +// ───────────────────────────────────────────────────────────────────────────── +/** Assign a stable colour index to each (srcIdx:srcLine) key. */ +function buildColorMap(sm) { + const colorMap = new Map(); + const keyToColor = new Map(); + // Representative mapping per lean line (first one) + const lineRep = new Map(); + for (const m of sm.mappings) { + if (!lineRep.has(m.genLine)) { + lineRep.set(m.genLine, m); + } + } + let next = 0; + // Sort by lean line so colours flow top-to-bottom + for (const [genLine, m] of [...lineRep.entries()].sort((a, b) => a[0] - b[0])) { + const key = `${m.srcIdx}:${m.srcLine}`; + if (!keyToColor.has(key)) { + keyToColor.set(key, next++ % N); + } + colorMap.set(genLine, keyToColor.get(key)); + } + return colorMap; +} +/** Find the mapping entry at or just before (line, col). */ +function closestMapping(mappings, line, col) { + let best = null; + for (const m of mappings) { + if (m.genLine > line) { + break; + } + if (m.genLine < line || m.genCol <= col) { + best = m; + } + } + return best; +} +/** + * Given a cursor position in the lean file, return all lean mappings that + * belong to the same "active segment" (same srcIdx + srcLine as the cursor mapping). + */ +function findActiveSegment(sm, colorMap, cursorLine, cursorCol) { + const rep = closestMapping(sm.mappings, cursorLine, cursorCol); + if (!rep) { + return []; + } + // All lean lines that map to the same (srcIdx, srcLine) + const seen = new Set(); + return sm.mappings.filter(m => { + if (m.srcIdx !== rep.srcIdx || m.srcLine !== rep.srcLine) { + return false; + } + if (seen.has(m.genLine)) { + return false; + } + seen.add(m.genLine); + return true; + }); +} +// ───────────────────────────────────────────────────────────────────────────── +// Hover provider +// ───────────────────────────────────────────────────────────────────────────── +class HaxHoverProvider { + constructor(mgr) { + this.mgr = mgr; + } + provideHover(document, position) { + const leanPath = document.uri.fsPath; + // Access the manager's source map via the public helper + const mapPath = leanPath + '.map'; + if (!fs.existsSync(mapPath)) { + return null; + } + // Decode inline (cached by mgr internally via update, but we need sm here) + let raw; + try { + raw = JSON.parse(fs.readFileSync(mapPath, 'utf8')); + } + catch { + return null; + } + const sources = raw.sources ?? []; + const sourcesContent = raw.sourcesContent ?? []; + const sm = decodeSourceMap(mapPath); + if (!sm) { + return null; + } + const m = closestMapping(sm.mappings, position.line, position.character); + if (!m) { + return null; + } + const srcPath = sm.resolvedPaths.get(m.srcIdx) ?? sources[m.srcIdx]; + if (!srcPath) { + return null; + } + // Get a few lines of context + let snippet; + const content = sourcesContent[m.srcIdx]; + if (content) { + const lines = content.split('\n'); + const start = Math.max(0, m.srcLine - 1); + const end = Math.min(lines.length, m.srcLine + 3); + snippet = lines.slice(start, end).join('\n'); + } + else { + try { + const lines = fs.readFileSync(srcPath, 'utf8').split('\n'); + const start = Math.max(0, m.srcLine - 1); + const end = Math.min(lines.length, m.srcLine + 3); + snippet = lines.slice(start, end).join('\n'); + } + catch { + snippet = ''; + } + } + const label = `**Rust source** — \`${path.basename(srcPath)}\` line ${m.srcLine + 1}`; + const md = new vscode.MarkdownString(`${label}\n\`\`\`rust\n${snippet}\n\`\`\``); + return new vscode.Hover(md); + } +} +// ───────────────────────────────────────────────────────────────────────────── +// Extension entry point +// ───────────────────────────────────────────────────────────────────────────── +function activate(ctx) { + const mgr = new HaxManager(ctx); + // Initial decoration pass + for (const editor of vscode.window.visibleTextEditors) { + mgr.update(editor); + } + ctx.subscriptions.push(vscode.window.onDidChangeActiveTextEditor(e => { if (e) { + mgr.update(e); + } }), vscode.window.onDidChangeTextEditorSelection(e => { mgr.update(e.textEditor); }), vscode.window.onDidChangeVisibleTextEditors(editors => { + for (const e of editors) { + mgr.update(e); + } + }), + // Invalidate cache when .lean.map files change on disk + vscode.workspace.onDidSaveTextDocument(doc => { + if (doc.fileName.endsWith('.lean.map') || doc.fileName.endsWith('.lean')) { + mgr.invalidateCache(); + for (const e of vscode.window.visibleTextEditors) { + mgr.update(e); + } + } + }), vscode.commands.registerCommand('hax.jumpToSource', () => mgr.jumpToSource()), vscode.commands.registerCommand('hax.jumpToLean', () => mgr.jumpToLean()), vscode.commands.registerCommand('hax.toggleRainbow', () => mgr.toggleRainbow()), vscode.languages.registerHoverProvider([{ language: 'lean4' }, { language: 'lean' }, { pattern: '**/*.lean' }], new HaxHoverProvider(mgr))); +} +function deactivate() { } +//# sourceMappingURL=extension.js.map \ No newline at end of file diff --git a/tools/vscode-hax-sourcemap/out/extension.js.map b/tools/vscode-hax-sourcemap/out/extension.js.map new file mode 100644 index 000000000..795f4acbc --- /dev/null +++ b/tools/vscode-hax-sourcemap/out/extension.js.map @@ -0,0 +1 @@ +{"version":3,"file":"extension.js","sourceRoot":"","sources":["../src/extension.ts"],"names":[],"mappings":";;AA+nBA,4BA2BC;AAED,gCAA+B;AA5pB/B,iCAAiC;AACjC,6BAA6B;AAC7B,yBAAyB;AAEzB,gFAAgF;AAChF,8BAA8B;AAC9B,gFAAgF;AAEhF,MAAM,MAAM,GAAG,kEAAkE,CAAC;AAClF,MAAM,GAAG,GAA2B,EAAE,CAAC;AACvC,KAAK,IAAI,CAAC,GAAG,CAAC,EAAE,CAAC,GAAG,MAAM,CAAC,MAAM,EAAE,CAAC,EAAE;IAAE,GAAG,CAAC,MAAM,CAAC,CAAC,CAAC,CAAC,GAAG,CAAC,CAAC;AAE3D,SAAS,SAAS,CAAC,CAAS,EAAE,GAAW;IACrC,IAAI,MAAM,GAAG,CAAC,EAAE,KAAK,GAAG,CAAC,CAAC;IAC1B,SAAS,CAAC;QACN,MAAM,KAAK,GAAG,GAAG,CAAC,CAAC,CAAC,GAAG,EAAE,CAAC,CAAC,CAAC;QAC5B,MAAM,IAAI,CAAC,KAAK,GAAG,EAAE,CAAC,IAAI,KAAK,CAAC;QAChC,KAAK,IAAI,CAAC,CAAC;QACX,IAAI,CAAC,CAAC,KAAK,GAAG,EAAE,CAAC,EAAE,CAAC;YAAC,MAAM;QAAC,CAAC;IACjC,CAAC;IACD,OAAO,CAAC,CAAC,MAAM,GAAG,CAAC,CAAC,CAAC,CAAC,CAAC,CAAC,CAAC,MAAM,KAAK,CAAC,CAAC,CAAC,CAAC,CAAC,CAAC,MAAM,KAAK,CAAC,CAAC,EAAE,GAAG,CAAC,CAAC;AAClE,CAAC;AAsBD,gFAAgF;AAChF,qBAAqB;AACrB,gFAAgF;AAEhF,SAAS,eAAe,CAAC,WAAmB;IACxC,IAAI,GAAgF,CAAC;IACrF,IAAI,CAAC;QAAC,GAAG,GAAG,IAAI,CAAC,KAAK,CAAC,EAAE,CAAC,YAAY,CAAC,WAAW,EAAE,MAAM,CAAC,CAAC,CAAC;IAAC,CAAC;IAC/D,MAAM,CAAC;QAAC,OAAO,IAAI,CAAC;IAAC,CAAC;IAEtB,MAAM,OAAO,GAAa,GAAG,CAAC,OAAO,IAAI,EAAE,CAAC;IAC5C,MAAM,cAAc,GAAsB,GAAG,CAAC,cAAc,IAAI,OAAO,CAAC,GAAG,CAAC,GAAG,EAAE,CAAC,IAAI,CAAC,CAAC;IACxF,MAAM,OAAO,GAAW,GAAG,CAAC,QAAQ,IAAI,EAAE,CAAC;IAC3C,MAAM,QAAQ,GAAc,EAAE,CAAC;IAE/B,IAAI,OAAO,GAAG,CAAC,CAAC;IAChB,IAAI,GAAG,GAAG,CAAC,EAAE,GAAG,GAAG,CAAC,EAAE,GAAG,GAAG,CAAC,EAAE,GAAG,GAAG,CAAC,CAAC;IAEvC,KAAK,IAAI,CAAC,GAAG,CAAC,EAAE,CAAC,GAAG,OAAO,CAAC,MAAM,GAAG,CAAC;QAClC,MAAM,EAAE,GAAG,OAAO,CAAC,CAAC,CAAC,CAAC;QACtB,IAAI,EAAE,KAAK,GAAG,EAAE,CAAC;YAAC,OAAO,EAAE,CAAC;YAAC,GAAG,GAAG,CAAC,CAAC;YAAC,CAAC,EAAE,CAAC;YAAC,SAAS;QAAC,CAAC;QACtD,IAAI,EAAE,KAAK,GAAG,EAAE,CAAC;YAAC,CAAC,EAAE,CAAC;YAAC,SAAS;QAAC,CAAC;QAElC,IAAI,GAAW,CAAC;QAChB,CAAC,GAAG,EAAE,CAAC,CAAC,GAAG,SAAS,CAAC,OAAO,EAAE,CAAC,CAAC,CAAC;QACjC,MAAM,MAAM,GAAG,GAAG,GAAG,GAAG,CAAC;QACzB,GAAG,GAAG,MAAM,CAAC;QAEb,IAAI,CAAC,IAAI,OAAO,CAAC,MAAM,IAAI,OAAO,CAAC,CAAC,CAAC,KAAK,GAAG,IAAI,OAAO,CAAC,CAAC,CAAC,KAAK,GAAG,EAAE,CAAC;YAAC,SAAS;QAAC,CAAC;QAElF,IAAI,GAAW,EAAE,GAAW,EAAE,GAAW,CAAC;QAC1C,CAAC,GAAG,EAAE,CAAC,CAAC,GAAG,SAAS,CAAC,OAAO,EAAE,CAAC,CAAC,CAAC;QACjC,CAAC,GAAG,EAAE,CAAC,CAAC,GAAG,SAAS,CAAC,OAAO,EAAE,CAAC,CAAC,CAAC;QACjC,CAAC,GAAG,EAAE,CAAC,CAAC,GAAG,SAAS,CAAC,OAAO,EAAE,CAAC,CAAC,CAAC;QAEjC,sBAAsB;QACtB,IAAI,CAAC,GAAG,OAAO,CAAC,MAAM,IAAI,OAAO,CAAC,CAAC,CAAC,KAAK,GAAG,IAAI,OAAO,CAAC,CAAC,CAAC,KAAK,GAAG,EAAE,CAAC;YACjE,CAAC,EAAE,CAAC,CAAC,GAAG,SAAS,CAAC,OAAO,EAAE,CAAC,CAAC,CAAC;QAClC,CAAC;QAED,GAAG,IAAI,GAAG,CAAC;QAAC,GAAG,IAAI,GAAG,CAAC;QAAC,GAAG,IAAI,GAAG,CAAC;QACnC,QAAQ,CAAC,IAAI,CAAC,EAAE,OAAO,EAAE,MAAM,EAAE,MAAM,EAAE,GAAG,EAAE,OAAO,EAAE,GAAG,EAAE,MAAM,EAAE,GAAG,EAAE,CAAC,CAAC;IAC/E,CAAC;IAED,MAAM,aAAa,GAAG,cAAc,CAAC,OAAO,EAAE,WAAW,CAAC,CAAC;IAC3D,OAAO,EAAE,QAAQ,EAAE,OAAO,EAAE,cAAc,EAAE,aAAa,EAAE,CAAC;AAChE,CAAC;AAED,SAAS,QAAQ,CAAC,CAAS;IACvB,IAAI,CAAC;QAAC,OAAO,EAAE,CAAC,YAAY,CAAC,CAAC,CAAC,CAAC;IAAC,CAAC;IAAC,MAAM,CAAC;QAAC,OAAO,IAAI,CAAC,OAAO,CAAC,CAAC,CAAC,CAAC;IAAC,CAAC;AACxE,CAAC;AAED,SAAS,cAAc,CAAC,OAAiB,EAAE,WAAmB;IAC1D,MAAM,QAAQ,GAAG,IAAI,GAAG,EAAkB,CAAC;IAC3C,MAAM,MAAM,GAAG,IAAI,CAAC,OAAO,CAAC,WAAW,CAAC,CAAC;IAEzC,KAAK,IAAI,GAAG,GAAG,CAAC,EAAE,GAAG,GAAG,OAAO,CAAC,MAAM,EAAE,GAAG,EAAE,EAAE,CAAC;QAC5C,MAAM,GAAG,GAAG,OAAO,CAAC,GAAG,CAAC,CAAC;QACzB,IAAI,CAAC,GAAG,EAAE,CAAC;YAAC,SAAS;QAAC,CAAC;QAEvB,MAAM,MAAM,GAAG,CAAC,CAAS,EAAE,EAAE;YACzB,IAAI,EAAE,CAAC,UAAU,CAAC,CAAC,CAAC,EAAE,CAAC;gBAAC,QAAQ,CAAC,GAAG,CAAC,GAAG,EAAE,QAAQ,CAAC,CAAC,CAAC,CAAC,CAAC;gBAAC,OAAO,IAAI,CAAC;YAAC,CAAC;YACtE,OAAO,KAAK,CAAC;QACjB,CAAC,CAAC;QAEF,IAAI,IAAI,CAAC,UAAU,CAAC,GAAG,CAAC,EAAE,CAAC;YAAC,MAAM,CAAC,GAAG,CAAC,CAAC;YAAC,SAAS;QAAC,CAAC;QAEpD,kBAAkB;QAClB,IAAI,KAAK,GAAG,KAAK,CAAC;QAClB,KAAK,MAAM,MAAM,IAAI,MAAM,CAAC,SAAS,CAAC,gBAAgB,IAAI,EAAE,EAAE,CAAC;YAC3D,IAAI,MAAM,CAAC,IAAI,CAAC,IAAI,CAAC,MAAM,CAAC,GAAG,CAAC,MAAM,EAAE,GAAG,CAAC,CAAC,EAAE,CAAC;gBAAC,KAAK,GAAG,IAAI,CAAC;gBAAC,MAAM;YAAC,CAAC;QAC3E,CAAC;QACD,IAAI,KAAK,EAAE,CAAC;YAAC,SAAS;QAAC,CAAC;QAExB,wBAAwB;QACxB,IAAI,GAAG,GAAG,MAAM,CAAC;QACjB,KAAK,IAAI,KAAK,GAAG,CAAC,EAAE,KAAK,GAAG,EAAE,EAAE,KAAK,EAAE,EAAE,CAAC;YACtC,IAAI,MAAM,CAAC,IAAI,CAAC,IAAI,CAAC,GAAG,EAAE,GAAG,CAAC,CAAC,EAAE,CAAC;gBAAC,MAAM;YAAC,CAAC;YAC3C,MAAM,MAAM,GAAG,IAAI,CAAC,OAAO,CAAC,GAAG,CAAC,CAAC;YACjC,IAAI,MAAM,KAAK,GAAG,EAAE,CAAC;gBAAC,MAAM;YAAC,CAAC;YAC9B,GAAG,GAAG,MAAM,CAAC;QACjB,CAAC;IACL,CAAC;IACD,OAAO,QAAQ,CAAC;AACpB,CAAC;AAED,gFAAgF;AAChF,iBAAiB;AACjB,gFAAgF;AAEhF,sDAAsD;AACtD,MAAM,OAAO,GAA+C;IACxD,EAAE,CAAC,EAAE,GAAG,EAAE,CAAC,EAAE,GAAG,EAAE,CAAC,EAAE,GAAG,EAAE,EAAE,MAAM;IAClC,EAAE,CAAC,EAAE,GAAG,EAAE,CAAC,EAAE,GAAG,EAAE,CAAC,EAAE,GAAG,EAAE,EAAE,QAAQ;IACpC,EAAE,CAAC,EAAE,GAAG,EAAE,CAAC,EAAE,GAAG,EAAE,CAAC,EAAE,GAAG,EAAE,EAAE,QAAQ;IACpC,EAAE,CAAC,EAAG,EAAE,EAAE,CAAC,EAAE,GAAG,EAAE,CAAC,EAAE,GAAG,EAAE,EAAE,OAAO;IACnC,EAAE,CAAC,EAAG,EAAE,EAAE,CAAC,EAAE,GAAG,EAAE,CAAC,EAAE,GAAG,EAAE,EAAE,OAAO;IACnC,EAAE,CAAC,EAAE,GAAG,EAAE,CAAC,EAAE,GAAG,EAAE,CAAC,EAAE,GAAG,EAAE,EAAE,SAAS;IACrC,EAAE,CAAC,EAAE,GAAG,EAAE,CAAC,EAAE,GAAG,EAAE,CAAC,EAAE,GAAG,EAAE,EAAE,SAAS;IACrC,EAAE,CAAC,EAAE,GAAG,EAAE,CAAC,EAAE,GAAG,EAAE,CAAC,EAAE,GAAG,EAAE,EAAE,QAAQ;CACvC,CAAC;AACF,MAAM,CAAC,GAAG,OAAO,CAAC,MAAM,CAAC;AAEzB,SAAS,IAAI,CAAC,CAAsC,EAAE,CAAS;IAC3D,OAAO,QAAQ,CAAC,CAAC,CAAC,IAAI,CAAC,CAAC,CAAC,IAAI,CAAC,CAAC,CAAC,IAAI,CAAC,GAAG,CAAC;AAC7C,CAAC;AAED,SAAS,YAAY,CAAC,OAAe;IAIjC,MAAM,EAAE,GAAsC,EAAE,CAAC;IACjD,MAAM,MAAM,GAAsC,EAAE,CAAC;IACrD,KAAK,MAAM,CAAC,IAAI,OAAO,EAAE,CAAC;QACtB,EAAE,CAAC,IAAI,CAAC,MAAM,CAAC,MAAM,CAAC,8BAA8B,CAAC;YACjD,eAAe,EAAE,IAAI,CAAC,CAAC,EAAE,OAAO,CAAC;YACjC,WAAW,EAAE,IAAI;YACjB,kBAAkB,EAAE,IAAI,CAAC,CAAC,EAAE,GAAG,CAAC;YAChC,iBAAiB,EAAE,MAAM,CAAC,iBAAiB,CAAC,IAAI;SACnD,CAAC,CAAC,CAAC;QACJ,MAAM,CAAC,IAAI,CAAC,MAAM,CAAC,MAAM,CAAC,8BAA8B,CAAC;YACrD,eAAe,EAAE,IAAI,CAAC,CAAC,EAAE,IAAI,CAAC,GAAG,CAAC,CAAC,EAAE,OAAO,GAAG,GAAG,CAAC,CAAC;YACpD,WAAW,EAAE,IAAI;YACjB,MAAM,EAAE,mBAAmB,IAAI,CAAC,CAAC,EAAE,GAAG,CAAC,EAAE;YACzC,kBAAkB,EAAE,IAAI,CAAC,CAAC,EAAE,GAAG,CAAC;YAChC,iBAAiB,EAAE,MAAM,CAAC,iBAAiB,CAAC,IAAI;SACnD,CAAC,CAAC,CAAC;IACR,CAAC;IACD,OAAO,EAAE,EAAE,EAAE,MAAM,EAAE,CAAC;AAC1B,CAAC;AAED,gFAAgF;AAChF,UAAU;AACV,gFAAgF;AAEhF,MAAM,UAAU;IASZ,YAA6B,GAA4B;QAA5B,QAAG,GAAH,GAAG,CAAyB;QARjD,YAAO,GAAG,IAAI,GAAG,EAAgC,CAAC;QAClD,kBAAa,GAAG,IAAI,GAAG,EAA+B,CAAC;QAC/D,iEAAiE;QACzD,eAAU,GAAG,IAAI,GAAG,EAAuB,CAAC;QAMhD,MAAM,GAAG,GAAG,MAAM,CAAC,SAAS,CAAC,gBAAgB,CAAC,eAAe,CAAC,CAAC;QAC/D,IAAI,CAAC,cAAc,GAAG,GAAG,CAAC,GAAG,CAAU,eAAe,EAAE,IAAI,CAAC,CAAC;QAC9D,IAAI,CAAC,QAAQ,GAAG,YAAY,CAAC,GAAG,CAAC,GAAG,CAAS,gBAAgB,EAAE,IAAI,CAAC,CAAC,CAAC;QAEtE,IAAI,CAAC,SAAS,GAAG,MAAM,CAAC,MAAM,CAAC,mBAAmB,CAAC,MAAM,CAAC,kBAAkB,CAAC,KAAK,EAAE,GAAG,CAAC,CAAC;QACzF,IAAI,CAAC,SAAS,CAAC,OAAO,GAAG,kBAAkB,CAAC;QAC5C,GAAG,CAAC,aAAa,CAAC,IAAI,CAAC,IAAI,CAAC,SAAS,CAAC,CAAC;QAEvC,GAAG,CAAC,aAAa,CAAC,IAAI,CAAC,MAAM,CAAC,SAAS,CAAC,wBAAwB,CAAC,CAAC,CAAC,EAAE;YACjE,IAAI,CAAC,CAAC,CAAC,oBAAoB,CAAC,eAAe,CAAC,EAAE,CAAC;gBAAC,OAAO;YAAC,CAAC;YACzD,MAAM,MAAM,GAAG,MAAM,CAAC,SAAS,CAAC,gBAAgB,CAAC,eAAe,CAAC,CAAC;YAClE,IAAI,CAAC,cAAc,GAAG,MAAM,CAAC,GAAG,CAAU,eAAe,EAAE,IAAI,CAAC,CAAC;YACjE,8DAA8D;YAC9D,KAAK,MAAM,CAAC,IAAI,CAAC,GAAG,IAAI,CAAC,QAAQ,CAAC,EAAE,EAAE,GAAG,IAAI,CAAC,QAAQ,CAAC,MAAM,CAAC,EAAE,CAAC;gBAAC,CAAC,CAAC,OAAO,EAAE,CAAC;YAAC,CAAC;YAChF,IAAI,CAAC,QAAQ,GAAG,YAAY,CAAC,MAAM,CAAC,GAAG,CAAS,gBAAgB,EAAE,IAAI,CAAC,CAAC,CAAC;YACzE,KAAK,MAAM,MAAM,IAAI,MAAM,CAAC,MAAM,CAAC,kBAAkB,EAAE,CAAC;gBAAC,IAAI,CAAC,MAAM,CAAC,MAAM,CAAC,CAAC;YAAC,CAAC;QACnF,CAAC,CAAC,CAAC,CAAC;IACR,CAAC;IAED,4EAA4E;IAEpE,aAAa,CAAC,QAAgB;QAClC,IAAI,IAAI,CAAC,OAAO,CAAC,GAAG,CAAC,QAAQ,CAAC,EAAE,CAAC;YAAC,OAAO,IAAI,CAAC,OAAO,CAAC,GAAG,CAAC,QAAQ,CAAE,CAAC;QAAC,CAAC;QACvE,MAAM,OAAO,GAAG,QAAQ,GAAG,MAAM,CAAC;QAClC,MAAM,EAAE,GAAG,EAAE,CAAC,UAAU,CAAC,OAAO,CAAC,CAAC,CAAC,CAAC,eAAe,CAAC,OAAO,CAAC,CAAC,CAAC,CAAC,IAAI,CAAC;QACpE,IAAI,CAAC,OAAO,CAAC,GAAG,CAAC,QAAQ,EAAE,EAAE,CAAC,CAAC;QAC/B,IAAI,EAAE,EAAE,CAAC;YACL,IAAI,CAAC,aAAa,CAAC,GAAG,CAAC,QAAQ,EAAE,aAAa,CAAC,EAAE,CAAC,CAAC,CAAC;YACpD,KAAK,MAAM,CAAC,EAAE,QAAQ,CAAC,IAAI,EAAE,CAAC,aAAa,EAAE,CAAC;gBAC1C,IAAI,CAAC,IAAI,CAAC,UAAU,CAAC,GAAG,CAAC,QAAQ,CAAC,EAAE,CAAC;oBAAC,IAAI,CAAC,UAAU,CAAC,GAAG,CAAC,QAAQ,EAAE,IAAI,GAAG,EAAE,CAAC,CAAC;gBAAC,CAAC;gBACjF,IAAI,CAAC,UAAU,CAAC,GAAG,CAAC,QAAQ,CAAE,CAAC,GAAG,CAAC,QAAQ,CAAC,CAAC;YACjD,CAAC;YACD,oCAAoC;YACpC,MAAM,CAAC,QAAQ,CAAC,cAAc,CAAC,YAAY,EAAE,mBAAmB,EAC5D,IAAI,CAAC,UAAU,CAAC,IAAI,GAAG,CAAC,CAAC,CAAC;QAClC,CAAC;QACD,OAAO,EAAE,CAAC;IACd,CAAC;IAEO,WAAW,CAAC,QAAgB;QAChC,IAAI,IAAI,CAAC,aAAa,CAAC,GAAG,CAAC,QAAQ,CAAC,EAAE,CAAC;YAAC,OAAO,IAAI,CAAC,aAAa,CAAC,GAAG,CAAC,QAAQ,CAAE,CAAC;QAAC,CAAC;QACnF,MAAM,EAAE,GAAG,IAAI,CAAC,aAAa,CAAC,QAAQ,CAAC,CAAC;QACxC,IAAI,CAAC,EAAE,EAAE,CAAC;YAAC,OAAO,IAAI,GAAG,EAAE,CAAC;QAAC,CAAC;QAC9B,MAAM,EAAE,GAAG,aAAa,CAAC,EAAE,CAAC,CAAC;QAC7B,IAAI,CAAC,aAAa,CAAC,GAAG,CAAC,QAAQ,EAAE,EAAE,CAAC,CAAC;QACrC,OAAO,EAAE,CAAC;IACd,CAAC;IAED,4EAA4E;IAE5E,MAAM,CAAC,MAAyB;QAC5B,MAAM,CAAC,GAAG,MAAM,CAAC,QAAQ,CAAC,GAAG,CAAC,MAAM,CAAC;QACrC,IAAI,CAAC,CAAC,QAAQ,CAAC,OAAO,CAAC,EAAE,CAAC;YAAC,IAAI,CAAC,UAAU,CAAC,MAAM,CAAC,CAAC;QAAC,CAAC;aAChD,IAAI,CAAC,CAAC,QAAQ,CAAC,KAAK,CAAC,EAAE,CAAC;YAAC,IAAI,CAAC,UAAU,CAAC,MAAM,CAAC,CAAC;QAAC,CAAC;IAC5D,CAAC;IAED,4EAA4E;IAEpE,UAAU,CAAC,MAAyB;QACxC,MAAM,QAAQ,GAAG,MAAM,CAAC,QAAQ,CAAC,GAAG,CAAC,MAAM,CAAC;QAC5C,MAAM,EAAE,GAAG,IAAI,CAAC,aAAa,CAAC,QAAQ,CAAC,CAAC;QAExC,IAAI,CAAC,EAAE,EAAE,CAAC;YACN,IAAI,CAAC,QAAQ,CAAC,MAAM,CAAC,CAAC;YACtB,IAAI,CAAC,SAAS,CAAC,IAAI,EAAE,CAAC;YACtB,MAAM,CAAC,QAAQ,CAAC,cAAc,CAAC,YAAY,EAAE,kBAAkB,EAAE,KAAK,CAAC,CAAC;YACxE,OAAO;QACX,CAAC;QAED,MAAM,CAAC,QAAQ,CAAC,cAAc,CAAC,YAAY,EAAE,kBAAkB,EAAE,IAAI,CAAC,CAAC;QACvE,MAAM,QAAQ,GAAG,IAAI,CAAC,WAAW,CAAC,QAAQ,CAAC,CAAC;QAC5C,MAAM,MAAM,GAAG,MAAM,CAAC,SAAS,CAAC,MAAM,CAAC;QAEvC,qBAAqB;QACrB,IAAI,IAAI,CAAC,cAAc,EAAE,CAAC;YACtB,MAAM,OAAO,GAAqB,KAAK,CAAC,IAAI,CAAC,EAAE,MAAM,EAAE,CAAC,EAAE,EAAE,GAAG,EAAE,CAAC,EAAE,CAAC,CAAC;YACtE,KAAK,MAAM,CAAC,IAAI,EAAE,EAAE,CAAC,IAAI,QAAQ,EAAE,CAAC;gBAChC,OAAO,CAAC,EAAE,CAAC,CAAC,IAAI,CAAC,IAAI,MAAM,CAAC,KAAK,CAAC,IAAI,EAAE,CAAC,EAAE,IAAI,EAAE,CAAC,CAAC,CAAC,CAAC;YACzD,CAAC;YACD,KAAK,IAAI,CAAC,GAAG,CAAC,EAAE,CAAC,GAAG,CAAC,EAAE,CAAC,EAAE,EAAE,CAAC;gBAAC,MAAM,CAAC,cAAc,CAAC,IAAI,CAAC,QAAQ,CAAC,EAAE,CAAC,CAAC,CAAC,EAAE,OAAO,CAAC,CAAC,CAAC,CAAC,CAAC;YAAC,CAAC;QAC3F,CAAC;aAAM,CAAC;YACJ,KAAK,IAAI,CAAC,GAAG,CAAC,EAAE,CAAC,GAAG,CAAC,EAAE,CAAC,EAAE,EAAE,CAAC;gBAAC,MAAM,CAAC,cAAc,CAAC,IAAI,CAAC,QAAQ,CAAC,EAAE,CAAC,CAAC,CAAC,EAAE,EAAE,CAAC,CAAC;YAAC,CAAC;QACnF,CAAC;QAED,0BAA0B;QAC1B,MAAM,cAAc,GAAG,iBAAiB,CAAC,EAAE,EAAE,QAAQ,EAAE,MAAM,CAAC,IAAI,EAAE,MAAM,CAAC,SAAS,CAAC,CAAC;QACtF,KAAK,IAAI,CAAC,GAAG,CAAC,EAAE,CAAC,GAAG,CAAC,EAAE,CAAC,EAAE,EAAE,CAAC;YAAC,MAAM,CAAC,cAAc,CAAC,IAAI,CAAC,QAAQ,CAAC,MAAM,CAAC,CAAC,CAAC,EAAE,EAAE,CAAC,CAAC;QAAC,CAAC;QAEnF,IAAI,cAAc,CAAC,MAAM,GAAG,CAAC,EAAE,CAAC;YAC5B,MAAM,EAAE,GAAG,QAAQ,CAAC,GAAG,CAAC,cAAc,CAAC,CAAC,CAAC,CAAC,OAAO,CAAC,IAAI,CAAC,CAAC;YACxD,MAAM,CAAC,cAAc,CAAC,IAAI,CAAC,QAAQ,CAAC,MAAM,CAAC,EAAE,CAAC,EAC1C,cAAc,CAAC,GAAG,CAAC,CAAC,CAAC,EAAE,CAAC,IAAI,MAAM,CAAC,KAAK,CAAC,CAAC,CAAC,OAAO,EAAE,CAAC,EAAE,CAAC,CAAC,OAAO,EAAE,CAAC,CAAC,CAAC,CAAC,CAAC;YAE3E,MAAM,GAAG,GAAG,cAAc,CAAC,CAAC,CAAC,CAAC;YAC9B,MAAM,OAAO,GAAG,EAAE,CAAC,aAAa,CAAC,GAAG,CAAC,GAAG,CAAC,MAAM,CAAC,IAAI,EAAE,CAAC,OAAO,CAAC,GAAG,CAAC,MAAM,CAAC,IAAI,GAAG,CAAC;YAClF,IAAI,CAAC,SAAS,CAAC,IAAI,GAAG,WAAW,IAAI,CAAC,QAAQ,CAAC,OAAO,CAAC,IAAI,GAAG,CAAC,OAAO,GAAG,CAAC,EAAE,CAAC;YAC7E,IAAI,CAAC,SAAS,CAAC,OAAO,GAAG,gBAAgB,OAAO,IAAI,GAAG,CAAC,OAAO,GAAG,CAAC,IAAI,GAAG,CAAC,MAAM,GAAG,CAAC,iBAAiB,CAAC;YACvG,IAAI,CAAC,SAAS,CAAC,IAAI,EAAE,CAAC;YAEtB,gCAAgC;YAChC,KAAK,MAAM,EAAE,IAAI,MAAM,CAAC,MAAM,CAAC,kBAAkB,EAAE,CAAC;gBAChD,IAAI,EAAE,CAAC,QAAQ,CAAC,GAAG,CAAC,MAAM,CAAC,QAAQ,CAAC,KAAK,CAAC,EAAE,CAAC;oBACzC,IAAI,CAAC,kBAAkB,CAAC,EAAE,EAAE,EAAE,EAAE,QAAQ,EAAE,QAAQ,EAAE,GAAG,EAAE,EAAE,CAAC,CAAC;gBACjE,CAAC;YACL,CAAC;QACL,CAAC;aAAM,CAAC;YACJ,IAAI,CAAC,SAAS,CAAC,IAAI,EAAE,CAAC;YACtB,yCAAyC;YACzC,KAAK,MAAM,EAAE,IAAI,MAAM,CAAC,MAAM,CAAC,kBAAkB,EAAE,CAAC;gBAChD,IAAI,EAAE,CAAC,QAAQ,CAAC,GAAG,CAAC,MAAM,CAAC,QAAQ,CAAC,KAAK,CAAC,EAAE,CAAC;oBACzC,IAAI,CAAC,kBAAkB,CAAC,EAAE,EAAE,EAAE,EAAE,QAAQ,EAAE,QAAQ,EAAE,IAAI,EAAE,CAAC,CAAC,CAAC,CAAC;gBAClE,CAAC;YACL,CAAC;QACL,CAAC;IACL,CAAC;IAED,4EAA4E;IAEpE,UAAU,CAAC,MAAyB;QACxC,MAAM,QAAQ,GAAG,QAAQ,CAAC,MAAM,CAAC,QAAQ,CAAC,GAAG,CAAC,MAAM,CAAC,CAAC;QAEtD,+DAA+D;QAC/D,KAAK,MAAM,EAAE,IAAI,MAAM,CAAC,MAAM,CAAC,kBAAkB,EAAE,CAAC;YAChD,IAAI,EAAE,CAAC,QAAQ,CAAC,QAAQ,CAAC,QAAQ,CAAC,OAAO,CAAC,EAAE,CAAC;gBACzC,IAAI,CAAC,aAAa,CAAC,EAAE,CAAC,QAAQ,CAAC,GAAG,CAAC,MAAM,CAAC,CAAC;YAC/C,CAAC;QACL,CAAC;QAED,MAAM,SAAS,GAAG,IAAI,CAAC,UAAU,CAAC,GAAG,CAAC,QAAQ,CAAC,CAAC;QAChD,IAAI,CAAC,SAAS,IAAI,SAAS,CAAC,IAAI,KAAK,CAAC,EAAE,CAAC;YACrC,IAAI,CAAC,QAAQ,CAAC,MAAM,CAAC,CAAC;YACtB,OAAO;QACX,CAAC;QACD,MAAM,CAAC,QAAQ,CAAC,cAAc,CAAC,YAAY,EAAE,mBAAmB,EAAE,IAAI,CAAC,CAAC;QAExE,MAAM,MAAM,GAAG,MAAM,CAAC,SAAS,CAAC,MAAM,CAAC;QAEvC,KAAK,MAAM,QAAQ,IAAI,SAAS,EAAE,CAAC;YAC/B,MAAM,EAAE,GAAG,IAAI,CAAC,aAAa,CAAC,QAAQ,CAAC,CAAC;YACxC,IAAI,CAAC,EAAE,EAAE,CAAC;gBAAC,SAAS;YAAC,CAAC;YACtB,MAAM,QAAQ,GAAG,IAAI,CAAC,WAAW,CAAC,QAAQ,CAAC,CAAC;YAC5C,MAAM,MAAM,GAAG,CAAC,GAAG,EAAE,CAAC,aAAa,CAAC,OAAO,EAAE,CAAC,CAAC,IAAI,CAAC,CAAC,CAAC,EAAE,CAAC,CAAC,EAAE,EAAE,CAAC,CAAC,KAAK,QAAQ,CAAC,EAAE,CAAC,CAAC,CAAC,CAAC;YACpF,IAAI,MAAM,KAAK,SAAS,EAAE,CAAC;gBAAC,SAAS;YAAC,CAAC;YAEvC,IAAI,CAAC,kBAAkB,CAAC,MAAM,EAAE,EAAE,EAAE,QAAQ,EAAE,QAAQ,EAAE,IAAI,EAAE,CAAC,CAAC,CAAC,CAAC;YAElE,sCAAsC;YACtC,MAAM,gBAAgB,GAAG,EAAE,CAAC,QAAQ,CAAC,MAAM,CACvC,CAAC,CAAC,EAAE,CAAC,CAAC,CAAC,MAAM,KAAK,MAAM,IAAI,CAAC,CAAC,OAAO,KAAK,MAAM,CAAC,IAAI,CAAC,CAAC;YAC3D,IAAI,gBAAgB,CAAC,MAAM,GAAG,CAAC,EAAE,CAAC;gBAC9B,MAAM,EAAE,GAAG,QAAQ,CAAC,GAAG,CAAC,gBAAgB,CAAC,CAAC,CAAC,CAAC,OAAO,CAAC,IAAI,CAAC,CAAC;gBAC1D,KAAK,IAAI,CAAC,GAAG,CAAC,EAAE,CAAC,GAAG,CAAC,EAAE,CAAC,EAAE,EAAE,CAAC;oBAAC,MAAM,CAAC,cAAc,CAAC,IAAI,CAAC,QAAQ,CAAC,MAAM,CAAC,CAAC,CAAC,EAAE,EAAE,CAAC,CAAC;gBAAC,CAAC;gBACnF,MAAM,CAAC,cAAc,CAAC,IAAI,CAAC,QAAQ,CAAC,MAAM,CAAC,EAAE,CAAC,EAC1C,CAAC,IAAI,MAAM,CAAC,KAAK,CAAC,MAAM,CAAC,IAAI,EAAE,CAAC,EAAE,MAAM,CAAC,IAAI,EAAE,CAAC,CAAC,CAAC,CAAC,CAAC;YAC5D,CAAC;YAED,mCAAmC;YACnC,KAAK,MAAM,EAAE,IAAI,MAAM,CAAC,MAAM,CAAC,kBAAkB,EAAE,CAAC;gBAChD,IAAI,EAAE,CAAC,QAAQ,CAAC,GAAG,CAAC,MAAM,KAAK,QAAQ,EAAE,CAAC;oBAAC,SAAS;gBAAC,CAAC;gBACtD,MAAM,YAAY,GAAG,EAAE,CAAC,QAAQ,CAAC,MAAM,CACnC,CAAC,CAAC,EAAE,CAAC,CAAC,CAAC,MAAM,KAAK,MAAM,IAAI,CAAC,CAAC,OAAO,KAAK,MAAM,CAAC,IAAI,CAAC,CAAC;gBAC3D,KAAK,IAAI,CAAC,GAAG,CAAC,EAAE,CAAC,GAAG,CAAC,EAAE,CAAC,EAAE,EAAE,CAAC;oBAAC,EAAE,CAAC,cAAc,CAAC,IAAI,CAAC,QAAQ,CAAC,MAAM,CAAC,CAAC,CAAC,EAAE,EAAE,CAAC,CAAC;gBAAC,CAAC;gBAC/E,IAAI,YAAY,CAAC,MAAM,GAAG,CAAC,EAAE,CAAC;oBAC1B,MAAM,EAAE,GAAG,QAAQ,CAAC,GAAG,CAAC,YAAY,CAAC,CAAC,CAAC,CAAC,OAAO,CAAC,IAAI,CAAC,CAAC;oBACtD,EAAE,CAAC,cAAc,CAAC,IAAI,CAAC,QAAQ,CAAC,MAAM,CAAC,EAAE,CAAC,EACtC,YAAY,CAAC,GAAG,CAAC,CAAC,CAAC,EAAE,CAAC,IAAI,MAAM,CAAC,KAAK,CAAC,CAAC,CAAC,OAAO,EAAE,CAAC,EAAE,CAAC,CAAC,OAAO,EAAE,CAAC,CAAC,CAAC,CAAC,CAAC;gBAC7E,CAAC;YACL,CAAC;QACL,CAAC;IACL,CAAC;IAEO,kBAAkB,CACtB,MAAyB,EACzB,EAAiB,EACjB,QAA6B,EAC7B,SAAiB,EACjB,aAA6B,EAC7B,QAAgB;QAEhB,MAAM,QAAQ,GAAG,QAAQ,CAAC,MAAM,CAAC,QAAQ,CAAC,GAAG,CAAC,MAAM,CAAC,CAAC;QACtD,MAAM,MAAM,GAAG,CAAC,GAAG,EAAE,CAAC,aAAa,CAAC,OAAO,EAAE,CAAC,CAAC,IAAI,CAAC,CAAC,CAAC,EAAE,CAAC,CAAC,EAAE,EAAE,CAAC,CAAC,KAAK,QAAQ,CAAC,EAAE,CAAC,CAAC,CAAC,CAAC;QACpF,IAAI,MAAM,KAAK,SAAS,EAAE,CAAC;YAAC,OAAO;QAAC,CAAC;QAErC,IAAI,IAAI,CAAC,cAAc,EAAE,CAAC;YACtB,mEAAmE;YACnE,MAAM,aAAa,GAAG,IAAI,GAAG,EAAkB,CAAC;YAChD,KAAK,MAAM,CAAC,IAAI,EAAE,CAAC,QAAQ,EAAE,CAAC;gBAC1B,IAAI,CAAC,CAAC,MAAM,KAAK,MAAM,EAAE,CAAC;oBAAC,SAAS;gBAAC,CAAC;gBACtC,IAAI,aAAa,CAAC,GAAG,CAAC,CAAC,CAAC,OAAO,CAAC,EAAE,CAAC;oBAAC,SAAS;gBAAC,CAAC;gBAC/C,MAAM,EAAE,GAAG,QAAQ,CAAC,GAAG,CAAC,CAAC,CAAC,OAAO,CAAC,CAAC;gBACnC,IAAI,EAAE,KAAK,SAAS,EAAE,CAAC;oBAAC,aAAa,CAAC,GAAG,CAAC,CAAC,CAAC,OAAO,EAAE,EAAE,CAAC,CAAC;gBAAC,CAAC;YAC/D,CAAC;YAED,4EAA4E;YAC5E,MAAM,MAAM,GAAG,CAAC,GAAG,aAAa,CAAC,OAAO,EAAE,CAAC,CAAC,IAAI,CAAC,CAAC,CAAC,EAAE,CAAC,EAAE,EAAE,CAAC,CAAC,CAAC,CAAC,CAAC,GAAG,CAAC,CAAC,CAAC,CAAC,CAAC,CAAC;YACxE,MAAM,OAAO,GAAqB,KAAK,CAAC,IAAI,CAAC,EAAE,MAAM,EAAE,CAAC,EAAE,EAAE,GAAG,EAAE,CAAC,EAAE,CAAC,CAAC;YACtE,KAAK,IAAI,CAAC,GAAG,CAAC,EAAE,CAAC,GAAG,MAAM,CAAC,MAAM,EAAE,CAAC,EAAE,EAAE,CAAC;gBACrC,MAAM,CAAC,SAAS,EAAE,EAAE,CAAC,GAAG,MAAM,CAAC,CAAC,CAAC,CAAC;gBAClC,MAAM,OAAO,GAAG,CAAC,GAAG,CAAC,GAAG,MAAM,CAAC,MAAM,CAAC,CAAC,CAAC,MAAM,CAAC,CAAC,GAAG,CAAC,CAAC,CAAC,CAAC,CAAC,GAAG,CAAC,CAAC,CAAC,CAAC,SAAS,CAAC;gBACzE,OAAO,CAAC,EAAE,CAAC,CAAC,IAAI,CAAC,IAAI,MAAM,CAAC,KAAK,CAAC,SAAS,EAAE,CAAC,EAAE,OAAO,EAAE,CAAC,CAAC,CAAC,CAAC;YACjE,CAAC;YACD,KAAK,IAAI,CAAC,GAAG,CAAC,EAAE,CAAC,GAAG,CAAC,EAAE,CAAC,EAAE,EAAE,CAAC;gBAAC,MAAM,CAAC,cAAc,CAAC,IAAI,CAAC,QAAQ,CAAC,EAAE,CAAC,CAAC,CAAC,EAAE,OAAO,CAAC,CAAC,CAAC,CAAC,CAAC;YAAC,CAAC;QAC3F,CAAC;QAED,IAAI,aAAa,KAAK,IAAI,IAAI,aAAa,CAAC,MAAM,KAAK,MAAM,EAAE,CAAC;YAC5D,KAAK,IAAI,CAAC,GAAG,CAAC,EAAE,CAAC,GAAG,CAAC,EAAE,CAAC,EAAE,EAAE,CAAC;gBAAC,MAAM,CAAC,cAAc,CAAC,IAAI,CAAC,QAAQ,CAAC,MAAM,CAAC,CAAC,CAAC,EAAE,EAAE,CAAC,CAAC;YAAC,CAAC;YACnF,MAAM,CAAC,cAAc,CAAC,IAAI,CAAC,QAAQ,CAAC,MAAM,CAAC,QAAQ,CAAC,EAChD,CAAC,IAAI,MAAM,CAAC,KAAK,CAAC,aAAa,CAAC,OAAO,EAAE,CAAC,EAAE,aAAa,CAAC,OAAO,EAAE,CAAC,CAAC,CAAC,CAAC,CAAC;QAChF,CAAC;IACL,CAAC;IAEO,QAAQ,CAAC,MAAyB;QACtC,KAAK,IAAI,CAAC,GAAG,CAAC,EAAE,CAAC,GAAG,CAAC,EAAE,CAAC,EAAE,EAAE,CAAC;YACzB,MAAM,CAAC,cAAc,CAAC,IAAI,CAAC,QAAQ,CAAC,EAAE,CAAC,CAAC,CAAC,EAAE,EAAE,CAAC,CAAC;YAC/C,MAAM,CAAC,cAAc,CAAC,IAAI,CAAC,QAAQ,CAAC,MAAM,CAAC,CAAC,CAAC,EAAE,EAAE,CAAC,CAAC;QACvD,CAAC;IACL,CAAC;IAED,4EAA4E;IAE5E,KAAK,CAAC,YAAY;QACd,MAAM,MAAM,GAAG,MAAM,CAAC,MAAM,CAAC,gBAAgB,CAAC;QAC9C,IAAI,CAAC,MAAM,IAAI,CAAC,MAAM,CAAC,QAAQ,CAAC,QAAQ,CAAC,QAAQ,CAAC,OAAO,CAAC,EAAE,CAAC;YAAC,OAAO;QAAC,CAAC;QAEvE,MAAM,EAAE,GAAG,IAAI,CAAC,aAAa,CAAC,MAAM,CAAC,QAAQ,CAAC,GAAG,CAAC,MAAM,CAAC,CAAC;QAC1D,IAAI,CAAC,EAAE,EAAE,CAAC;YACN,MAAM,CAAC,MAAM,CAAC,kBAAkB,CAAC,yCAAyC,CAAC,CAAC;YAC5E,OAAO;QACX,CAAC;QAED,MAAM,MAAM,GAAG,MAAM,CAAC,SAAS,CAAC,MAAM,CAAC;QACvC,MAAM,CAAC,GAAG,cAAc,CAAC,EAAE,CAAC,QAAQ,EAAE,MAAM,CAAC,IAAI,EAAE,MAAM,CAAC,SAAS,CAAC,CAAC;QACrE,IAAI,CAAC,CAAC,EAAE,CAAC;YACL,MAAM,CAAC,MAAM,CAAC,kBAAkB,CAAC,qCAAqC,CAAC,CAAC;YACxE,OAAO;QACX,CAAC;QAED,MAAM,QAAQ,GAAG,EAAE,CAAC,aAAa,CAAC,GAAG,CAAC,CAAC,CAAC,MAAM,CAAC,CAAC;QAChD,IAAI,CAAC,QAAQ,EAAE,CAAC;YACZ,MAAM,OAAO,GAAG,EAAE,CAAC,cAAc,CAAC,CAAC,CAAC,MAAM,CAAC,CAAC;YAC5C,IAAI,OAAO,EAAE,CAAC;gBACV,MAAM,GAAG,GAAG,MAAM,MAAM,CAAC,SAAS,CAAC,gBAAgB,CAAC;oBAChD,QAAQ,EAAE,MAAM;oBAChB,OAAO,EAAE,cAAc,EAAE,CAAC,OAAO,CAAC,CAAC,CAAC,MAAM,CAAC,oCAAoC,OAAO,EAAE;iBAC3F,CAAC,CAAC;gBACH,MAAM,EAAE,GAAG,MAAM,MAAM,CAAC,MAAM,CAAC,gBAAgB,CAAC,GAAG,EAAE,MAAM,CAAC,UAAU,CAAC,MAAM,CAAC,CAAC;gBAC/E,MAAM,GAAG,GAAG,IAAI,MAAM,CAAC,QAAQ,CAAC,CAAC,CAAC,OAAO,GAAG,CAAC,CAAC,mBAAmB,EAAE,CAAC,CAAC,MAAM,CAAC,CAAC;gBAC7E,EAAE,CAAC,SAAS,GAAG,IAAI,MAAM,CAAC,SAAS,CAAC,GAAG,EAAE,GAAG,CAAC,CAAC;gBAC9C,EAAE,CAAC,WAAW,CAAC,IAAI,MAAM,CAAC,KAAK,CAAC,GAAG,EAAE,GAAG,CAAC,EAAE,MAAM,CAAC,oBAAoB,CAAC,QAAQ,CAAC,CAAC;YACrF,CAAC;iBAAM,CAAC;gBACJ,MAAM,CAAC,MAAM,CAAC,kBAAkB,CAAC,+BAA+B,EAAE,CAAC,OAAO,CAAC,CAAC,CAAC,MAAM,CAAC,EAAE,CAAC,CAAC;YAC5F,CAAC;YACD,OAAO;QACX,CAAC;QAED,MAAM,GAAG,GAAG,MAAM,MAAM,CAAC,SAAS,CAAC,gBAAgB,CAAC,MAAM,CAAC,GAAG,CAAC,IAAI,CAAC,QAAQ,CAAC,CAAC,CAAC;QAC/E,MAAM,EAAE,GAAG,MAAM,MAAM,CAAC,MAAM,CAAC,gBAAgB,CAAC,GAAG,EAAE,MAAM,CAAC,UAAU,CAAC,MAAM,CAAC,CAAC;QAC/E,MAAM,GAAG,GAAG,IAAI,MAAM,CAAC,QAAQ,CAAC,CAAC,CAAC,OAAO,EAAE,CAAC,CAAC,MAAM,CAAC,CAAC;QACrD,EAAE,CAAC,SAAS,GAAG,IAAI,MAAM,CAAC,SAAS,CAAC,GAAG,EAAE,GAAG,CAAC,CAAC;QAC9C,EAAE,CAAC,WAAW,CAAC,IAAI,MAAM,CAAC,KAAK,CAAC,GAAG,EAAE,GAAG,CAAC,EAAE,MAAM,CAAC,oBAAoB,CAAC,QAAQ,CAAC,CAAC;IACrF,CAAC;IAED,KAAK,CAAC,UAAU;QACZ,MAAM,MAAM,GAAG,MAAM,CAAC,MAAM,CAAC,gBAAgB,CAAC;QAC9C,IAAI,CAAC,MAAM,EAAE,CAAC;YAAC,OAAO;QAAC,CAAC;QAExB,MAAM,QAAQ,GAAG,MAAM,CAAC,QAAQ,CAAC,GAAG,CAAC,MAAM,CAAC;QAE5C,iDAAiD;QACjD,KAAK,MAAM,EAAE,IAAI,MAAM,CAAC,MAAM,CAAC,kBAAkB,EAAE,CAAC;YAChD,IAAI,EAAE,CAAC,QAAQ,CAAC,QAAQ,CAAC,QAAQ,CAAC,OAAO,CAAC,EAAE,CAAC;gBACzC,IAAI,CAAC,aAAa,CAAC,EAAE,CAAC,QAAQ,CAAC,GAAG,CAAC,MAAM,CAAC,CAAC;YAC/C,CAAC;QACL,CAAC;QAED,IAAI,SAAS,GAAG,IAAI,CAAC,UAAU,CAAC,GAAG,CAAC,QAAQ,CAAC,CAAC;QAE9C,uDAAuD;QACvD,IAAI,CAAC,SAAS,IAAI,SAAS,CAAC,IAAI,KAAK,CAAC,EAAE,CAAC;YACrC,MAAM,IAAI,GAAG,MAAM,MAAM,CAAC,SAAS,CAAC,SAAS,CAAC,eAAe,EAAE,oBAAoB,EAAE,EAAE,CAAC,CAAC;YACzF,KAAK,MAAM,MAAM,IAAI,IAAI,EAAE,CAAC;gBACxB,MAAM,QAAQ,GAAG,MAAM,CAAC,MAAM,CAAC,OAAO,CAAC,QAAQ,EAAE,EAAE,CAAC,CAAC;gBACrD,IAAI,CAAC,aAAa,CAAC,QAAQ,CAAC,CAAC;YACjC,CAAC;YACD,SAAS,GAAG,IAAI,CAAC,UAAU,CAAC,GAAG,CAAC,QAAQ,CAAC,CAAC;QAC9C,CAAC;QAED,IAAI,CAAC,SAAS,IAAI,SAAS,CAAC,IAAI,KAAK,CAAC,EAAE,CAAC;YACrC,MAAM,CAAC,MAAM,CAAC,kBAAkB,CAAC,mDAAmD,CAAC,CAAC;YACtF,OAAO;QACX,CAAC;QAED,MAAM,UAAU,GAAG,MAAM,CAAC,SAAS,CAAC,MAAM,CAAC,IAAI,CAAC;QAEhD,KAAK,MAAM,QAAQ,IAAI,SAAS,EAAE,CAAC;YAC/B,MAAM,EAAE,GAAG,IAAI,CAAC,aAAa,CAAC,QAAQ,CAAC,CAAC;YACxC,IAAI,CAAC,EAAE,EAAE,CAAC;gBAAC,SAAS;YAAC,CAAC;YACtB,MAAM,MAAM,GAAG,CAAC,GAAG,EAAE,CAAC,aAAa,CAAC,OAAO,EAAE,CAAC,CAAC,IAAI,CAAC,CAAC,CAAC,EAAE,CAAC,CAAC,EAAE,EAAE,CAAC,CAAC,KAAK,QAAQ,CAAC,EAAE,CAAC,CAAC,CAAC,CAAC;YACpF,IAAI,MAAM,KAAK,SAAS,EAAE,CAAC;gBAAC,SAAS;YAAC,CAAC;YAEvC,MAAM,UAAU,GAAG,EAAE,CAAC,QAAQ;iBACzB,MAAM,CAAC,CAAC,CAAC,EAAE,CAAC,CAAC,CAAC,MAAM,KAAK,MAAM,IAAI,CAAC,CAAC,OAAO,IAAI,UAAU,GAAG,CAAC,CAAC;iBAC/D,IAAI,CAAC,CAAC,CAAC,EAAE,CAAC,EAAE,EAAE,CAAC,IAAI,CAAC,GAAG,CAAC,CAAC,CAAC,OAAO,GAAG,UAAU,CAAC,GAAG,IAAI,CAAC,GAAG,CAAC,CAAC,CAAC,OAAO,GAAG,UAAU,CAAC,CAAC,CAAC;YAEzF,IAAI,UAAU,CAAC,MAAM,KAAK,CAAC,EAAE,CAAC;gBAAC,SAAS;YAAC,CAAC;YAE1C,MAAM,IAAI,GAAG,UAAU,CAAC,CAAC,CAAC,CAAC;YAC3B,MAAM,GAAG,GAAG,MAAM,MAAM,CAAC,SAAS,CAAC,gBAAgB,CAAC,MAAM,CAAC,GAAG,CAAC,IAAI,CAAC,QAAQ,CAAC,CAAC,CAAC;YAC/E,MAAM,EAAE,GAAG,MAAM,MAAM,CAAC,MAAM,CAAC,gBAAgB,CAAC,GAAG,EAAE,MAAM,CAAC,UAAU,CAAC,MAAM,CAAC,CAAC;YAC/E,MAAM,GAAG,GAAG,IAAI,MAAM,CAAC,QAAQ,CAAC,IAAI,CAAC,OAAO,EAAE,IAAI,CAAC,MAAM,CAAC,CAAC;YAC3D,EAAE,CAAC,SAAS,GAAG,IAAI,MAAM,CAAC,SAAS,CAAC,GAAG,EAAE,GAAG,CAAC,CAAC;YAC9C,EAAE,CAAC,WAAW,CAAC,IAAI,MAAM,CAAC,KAAK,CAAC,GAAG,EAAE,GAAG,CAAC,EAAE,MAAM,CAAC,oBAAoB,CAAC,QAAQ,CAAC,CAAC;YACjF,OAAO;QACX,CAAC;QAED,MAAM,CAAC,MAAM,CAAC,kBAAkB,CAAC,6CAA6C,CAAC,CAAC;IACpF,CAAC;IAED,aAAa;QACT,IAAI,CAAC,cAAc,GAAG,CAAC,IAAI,CAAC,cAAc,CAAC;QAC3C,MAAM,CAAC,MAAM,CAAC,sBAAsB,CAChC,uBAAuB,IAAI,CAAC,cAAc,CAAC,CAAC,CAAC,SAAS,CAAC,CAAC,CAAC,UAAU,EAAE,CAAC,CAAC;QAC3E,KAAK,MAAM,MAAM,IAAI,MAAM,CAAC,MAAM,CAAC,kBAAkB,EAAE,CAAC;YAAC,IAAI,CAAC,MAAM,CAAC,MAAM,CAAC,CAAC;QAAC,CAAC;IACnF,CAAC;IAED,eAAe;QACX,IAAI,CAAC,OAAO,CAAC,KAAK,EAAE,CAAC;QACrB,IAAI,CAAC,aAAa,CAAC,KAAK,EAAE,CAAC;QAC3B,IAAI,CAAC,UAAU,CAAC,KAAK,EAAE,CAAC;IAC5B,CAAC;CACJ;AAED,gFAAgF;AAChF,eAAe;AACf,gFAAgF;AAEhF,iEAAiE;AACjE,SAAS,aAAa,CAAC,EAAiB;IACpC,MAAM,QAAQ,GAAG,IAAI,GAAG,EAAkB,CAAC;IAC3C,MAAM,UAAU,GAAG,IAAI,GAAG,EAAkB,CAAC;IAE7C,mDAAmD;IACnD,MAAM,OAAO,GAAG,IAAI,GAAG,EAAmB,CAAC;IAC3C,KAAK,MAAM,CAAC,IAAI,EAAE,CAAC,QAAQ,EAAE,CAAC;QAC1B,IAAI,CAAC,OAAO,CAAC,GAAG,CAAC,CAAC,CAAC,OAAO,CAAC,EAAE,CAAC;YAAC,OAAO,CAAC,GAAG,CAAC,CAAC,CAAC,OAAO,EAAE,CAAC,CAAC,CAAC;QAAC,CAAC;IAC/D,CAAC;IAED,IAAI,IAAI,GAAG,CAAC,CAAC;IACb,kDAAkD;IAClD,KAAK,MAAM,CAAC,OAAO,EAAE,CAAC,CAAC,IAAI,CAAC,GAAG,OAAO,CAAC,OAAO,EAAE,CAAC,CAAC,IAAI,CAAC,CAAC,CAAC,EAAE,CAAC,EAAE,EAAE,CAAC,CAAC,CAAC,CAAC,CAAC,GAAG,CAAC,CAAC,CAAC,CAAC,CAAC,EAAE,CAAC;QAC5E,MAAM,GAAG,GAAG,GAAG,CAAC,CAAC,MAAM,IAAI,CAAC,CAAC,OAAO,EAAE,CAAC;QACvC,IAAI,CAAC,UAAU,CAAC,GAAG,CAAC,GAAG,CAAC,EAAE,CAAC;YAAC,UAAU,CAAC,GAAG,CAAC,GAAG,EAAE,IAAI,EAAE,GAAG,CAAC,CAAC,CAAC;QAAC,CAAC;QAC9D,QAAQ,CAAC,GAAG,CAAC,OAAO,EAAE,UAAU,CAAC,GAAG,CAAC,GAAG,CAAE,CAAC,CAAC;IAChD,CAAC;IACD,OAAO,QAAQ,CAAC;AACpB,CAAC;AAED,4DAA4D;AAC5D,SAAS,cAAc,CAAC,QAAmB,EAAE,IAAY,EAAE,GAAW;IAClE,IAAI,IAAI,GAAmB,IAAI,CAAC;IAChC,KAAK,MAAM,CAAC,IAAI,QAAQ,EAAE,CAAC;QACvB,IAAI,CAAC,CAAC,OAAO,GAAG,IAAI,EAAE,CAAC;YAAC,MAAM;QAAC,CAAC;QAChC,IAAI,CAAC,CAAC,OAAO,GAAG,IAAI,IAAI,CAAC,CAAC,MAAM,IAAI,GAAG,EAAE,CAAC;YAAC,IAAI,GAAG,CAAC,CAAC;QAAC,CAAC;IAC1D,CAAC;IACD,OAAO,IAAI,CAAC;AAChB,CAAC;AAED;;;GAGG;AACH,SAAS,iBAAiB,CACtB,EAAiB,EACjB,QAA6B,EAC7B,UAAkB,EAClB,SAAiB;IAEjB,MAAM,GAAG,GAAG,cAAc,CAAC,EAAE,CAAC,QAAQ,EAAE,UAAU,EAAE,SAAS,CAAC,CAAC;IAC/D,IAAI,CAAC,GAAG,EAAE,CAAC;QAAC,OAAO,EAAE,CAAC;IAAC,CAAC;IAExB,wDAAwD;IACxD,MAAM,IAAI,GAAG,IAAI,GAAG,EAAU,CAAC;IAC/B,OAAO,EAAE,CAAC,QAAQ,CAAC,MAAM,CAAC,CAAC,CAAC,EAAE;QAC1B,IAAI,CAAC,CAAC,MAAM,KAAK,GAAG,CAAC,MAAM,IAAI,CAAC,CAAC,OAAO,KAAK,GAAG,CAAC,OAAO,EAAE,CAAC;YAAC,OAAO,KAAK,CAAC;QAAC,CAAC;QAC3E,IAAI,IAAI,CAAC,GAAG,CAAC,CAAC,CAAC,OAAO,CAAC,EAAE,CAAC;YAAC,OAAO,KAAK,CAAC;QAAC,CAAC;QAC1C,IAAI,CAAC,GAAG,CAAC,CAAC,CAAC,OAAO,CAAC,CAAC;QACpB,OAAO,IAAI,CAAC;IAChB,CAAC,CAAC,CAAC;AACP,CAAC;AAED,gFAAgF;AAChF,iBAAiB;AACjB,gFAAgF;AAEhF,MAAM,gBAAgB;IAClB,YAA6B,GAAe;QAAf,QAAG,GAAH,GAAG,CAAY;IAAG,CAAC;IAEhD,YAAY,CACR,QAA6B,EAC7B,QAAyB;QAEzB,MAAM,QAAQ,GAAG,QAAQ,CAAC,GAAG,CAAC,MAAM,CAAC;QACrC,wDAAwD;QACxD,MAAM,OAAO,GAAG,QAAQ,GAAG,MAAM,CAAC;QAClC,IAAI,CAAC,EAAE,CAAC,UAAU,CAAC,OAAO,CAAC,EAAE,CAAC;YAAC,OAAO,IAAI,CAAC;QAAC,CAAC;QAC7C,2EAA2E;QAC3E,IAAI,GAAgF,CAAC;QACrF,IAAI,CAAC;YAAC,GAAG,GAAG,IAAI,CAAC,KAAK,CAAC,EAAE,CAAC,YAAY,CAAC,OAAO,EAAE,MAAM,CAAC,CAAC,CAAC;QAAC,CAAC;QAC3D,MAAM,CAAC;YAAC,OAAO,IAAI,CAAC;QAAC,CAAC;QAEtB,MAAM,OAAO,GAAa,GAAG,CAAC,OAAO,IAAI,EAAE,CAAC;QAC5C,MAAM,cAAc,GAAsB,GAAG,CAAC,cAAc,IAAI,EAAE,CAAC;QACnE,MAAM,EAAE,GAAG,eAAe,CAAC,OAAO,CAAC,CAAC;QACpC,IAAI,CAAC,EAAE,EAAE,CAAC;YAAC,OAAO,IAAI,CAAC;QAAC,CAAC;QAEzB,MAAM,CAAC,GAAG,cAAc,CAAC,EAAE,CAAC,QAAQ,EAAE,QAAQ,CAAC,IAAI,EAAE,QAAQ,CAAC,SAAS,CAAC,CAAC;QACzE,IAAI,CAAC,CAAC,EAAE,CAAC;YAAC,OAAO,IAAI,CAAC;QAAC,CAAC;QAExB,MAAM,OAAO,GAAG,EAAE,CAAC,aAAa,CAAC,GAAG,CAAC,CAAC,CAAC,MAAM,CAAC,IAAI,OAAO,CAAC,CAAC,CAAC,MAAM,CAAC,CAAC;QACpE,IAAI,CAAC,OAAO,EAAE,CAAC;YAAC,OAAO,IAAI,CAAC;QAAC,CAAC;QAE9B,6BAA6B;QAC7B,IAAI,OAAe,CAAC;QACpB,MAAM,OAAO,GAAG,cAAc,CAAC,CAAC,CAAC,MAAM,CAAC,CAAC;QACzC,IAAI,OAAO,EAAE,CAAC;YACV,MAAM,KAAK,GAAG,OAAO,CAAC,KAAK,CAAC,IAAI,CAAC,CAAC;YAClC,MAAM,KAAK,GAAG,IAAI,CAAC,GAAG,CAAC,CAAC,EAAE,CAAC,CAAC,OAAO,GAAG,CAAC,CAAC,CAAC;YACzC,MAAM,GAAG,GAAG,IAAI,CAAC,GAAG,CAAC,KAAK,CAAC,MAAM,EAAE,CAAC,CAAC,OAAO,GAAG,CAAC,CAAC,CAAC;YAClD,OAAO,GAAG,KAAK,CAAC,KAAK,CAAC,KAAK,EAAE,GAAG,CAAC,CAAC,IAAI,CAAC,IAAI,CAAC,CAAC;QACjD,CAAC;aAAM,CAAC;YACJ,IAAI,CAAC;gBACD,MAAM,KAAK,GAAG,EAAE,CAAC,YAAY,CAAC,OAAO,EAAE,MAAM,CAAC,CAAC,KAAK,CAAC,IAAI,CAAC,CAAC;gBAC3D,MAAM,KAAK,GAAG,IAAI,CAAC,GAAG,CAAC,CAAC,EAAE,CAAC,CAAC,OAAO,GAAG,CAAC,CAAC,CAAC;gBACzC,MAAM,GAAG,GAAG,IAAI,CAAC,GAAG,CAAC,KAAK,CAAC,MAAM,EAAE,CAAC,CAAC,OAAO,GAAG,CAAC,CAAC,CAAC;gBAClD,OAAO,GAAG,KAAK,CAAC,KAAK,CAAC,KAAK,EAAE,GAAG,CAAC,CAAC,IAAI,CAAC,IAAI,CAAC,CAAC;YACjD,CAAC;YAAC,MAAM,CAAC;gBACL,OAAO,GAAG,EAAE,CAAC;YACjB,CAAC;QACL,CAAC;QAED,MAAM,KAAK,GAAG,uBAAuB,IAAI,CAAC,QAAQ,CAAC,OAAO,CAAC,WAAW,CAAC,CAAC,OAAO,GAAG,CAAC,EAAE,CAAC;QACtF,MAAM,EAAE,GAAG,IAAI,MAAM,CAAC,cAAc,CAChC,GAAG,KAAK,iBAAiB,OAAO,UAAU,CAC7C,CAAC;QACF,OAAO,IAAI,MAAM,CAAC,KAAK,CAAC,EAAE,CAAC,CAAC;IAChC,CAAC;CACJ;AAED,gFAAgF;AAChF,wBAAwB;AACxB,gFAAgF;AAEhF,SAAgB,QAAQ,CAAC,GAA4B;IACjD,MAAM,GAAG,GAAG,IAAI,UAAU,CAAC,GAAG,CAAC,CAAC;IAEhC,0BAA0B;IAC1B,KAAK,MAAM,MAAM,IAAI,MAAM,CAAC,MAAM,CAAC,kBAAkB,EAAE,CAAC;QAAC,GAAG,CAAC,MAAM,CAAC,MAAM,CAAC,CAAC;IAAC,CAAC;IAE9E,GAAG,CAAC,aAAa,CAAC,IAAI,CAClB,MAAM,CAAC,MAAM,CAAC,2BAA2B,CAAC,CAAC,CAAC,EAAE,GAAG,IAAI,CAAC,EAAE,CAAC;QAAC,GAAG,CAAC,MAAM,CAAC,CAAC,CAAC,CAAC;IAAC,CAAC,CAAC,CAAC,CAAC,EAC7E,MAAM,CAAC,MAAM,CAAC,8BAA8B,CAAC,CAAC,CAAC,EAAE,GAAG,GAAG,CAAC,MAAM,CAAC,CAAC,CAAC,UAAU,CAAC,CAAC,CAAC,CAAC,CAAC,EAChF,MAAM,CAAC,MAAM,CAAC,6BAA6B,CAAC,OAAO,CAAC,EAAE;QAClD,KAAK,MAAM,CAAC,IAAI,OAAO,EAAE,CAAC;YAAC,GAAG,CAAC,MAAM,CAAC,CAAC,CAAC,CAAC;QAAC,CAAC;IAC/C,CAAC,CAAC;IACF,uDAAuD;IACvD,MAAM,CAAC,SAAS,CAAC,qBAAqB,CAAC,GAAG,CAAC,EAAE;QACzC,IAAI,GAAG,CAAC,QAAQ,CAAC,QAAQ,CAAC,WAAW,CAAC,IAAI,GAAG,CAAC,QAAQ,CAAC,QAAQ,CAAC,OAAO,CAAC,EAAE,CAAC;YACvE,GAAG,CAAC,eAAe,EAAE,CAAC;YACtB,KAAK,MAAM,CAAC,IAAI,MAAM,CAAC,MAAM,CAAC,kBAAkB,EAAE,CAAC;gBAAC,GAAG,CAAC,MAAM,CAAC,CAAC,CAAC,CAAC;YAAC,CAAC;QACxE,CAAC;IACL,CAAC,CAAC,EACF,MAAM,CAAC,QAAQ,CAAC,eAAe,CAAC,kBAAkB,EAAE,GAAG,EAAE,CAAC,GAAG,CAAC,YAAY,EAAE,CAAC,EAC7E,MAAM,CAAC,QAAQ,CAAC,eAAe,CAAC,gBAAgB,EAAE,GAAG,EAAE,CAAC,GAAG,CAAC,UAAU,EAAE,CAAC,EACzE,MAAM,CAAC,QAAQ,CAAC,eAAe,CAAC,mBAAmB,EAAE,GAAG,EAAE,CAAC,GAAG,CAAC,aAAa,EAAE,CAAC,EAC/E,MAAM,CAAC,SAAS,CAAC,qBAAqB,CAClC,CAAC,EAAE,QAAQ,EAAE,OAAO,EAAE,EAAE,EAAE,QAAQ,EAAE,MAAM,EAAE,EAAE,EAAE,OAAO,EAAE,WAAW,EAAE,CAAC,EACvE,IAAI,gBAAgB,CAAC,GAAG,CAAC,CAC5B,CACJ,CAAC;AACN,CAAC;AAED,SAAgB,UAAU,KAAI,CAAC"} \ No newline at end of file diff --git a/tools/vscode-hax-sourcemap/package-lock.json b/tools/vscode-hax-sourcemap/package-lock.json new file mode 100644 index 000000000..953c715e0 --- /dev/null +++ b/tools/vscode-hax-sourcemap/package-lock.json @@ -0,0 +1,58 @@ +{ + "name": "vscode-hax-sourcemap", + "version": "0.1.0", + "lockfileVersion": 3, + "requires": true, + "packages": { + "": { + "name": "vscode-hax-sourcemap", + "version": "0.1.0", + "devDependencies": { + "@types/node": "^20.0.0", + "@types/vscode": "^1.85.0", + "typescript": "^5.3.0" + }, + "engines": { + "vscode": "^1.85.0" + } + }, + "node_modules/@types/node": { + "version": "20.19.37", + "resolved": "https://registry.npmjs.org/@types/node/-/node-20.19.37.tgz", + "integrity": "sha512-8kzdPJ3FsNsVIurqBs7oodNnCEVbni9yUEkaHbgptDACOPW04jimGagZ51E6+lXUwJjgnBw+hyko/lkFWCldqw==", + "dev": true, + "license": "MIT", + "dependencies": { + "undici-types": "~6.21.0" + } + }, + "node_modules/@types/vscode": { + "version": "1.110.0", + "resolved": "https://registry.npmjs.org/@types/vscode/-/vscode-1.110.0.tgz", + "integrity": "sha512-AGuxUEpU4F4mfuQjxPPaQVyuOMhs+VT/xRok1jiHVBubHK7lBRvCuOMZG0LKUwxncrPorJ5qq/uil3IdZBd5lA==", + "dev": true, + "license": "MIT" + }, + "node_modules/typescript": { + "version": "5.9.3", + "resolved": "https://registry.npmjs.org/typescript/-/typescript-5.9.3.tgz", + "integrity": "sha512-jl1vZzPDinLr9eUt3J/t7V6FgNEw9QjvBPdysz9KfQDD41fQrC2Y4vKQdiaUpFT4bXlb1RHhLpp8wtm6M5TgSw==", + "dev": true, + "license": "Apache-2.0", + "bin": { + "tsc": "bin/tsc", + "tsserver": "bin/tsserver" + }, + "engines": { + "node": ">=14.17" + } + }, + "node_modules/undici-types": { + "version": "6.21.0", + "resolved": "https://registry.npmjs.org/undici-types/-/undici-types-6.21.0.tgz", + "integrity": "sha512-iwDZqg0QAGrg9Rav5H4n0M64c3mkR59cJ6wQp+7C4nI0gsmExaedaYLNO44eT4AtBBwjbTiGPMlt2Md0T9H9JQ==", + "dev": true, + "license": "MIT" + } + } +} diff --git a/tools/vscode-hax-sourcemap/package.json b/tools/vscode-hax-sourcemap/package.json new file mode 100644 index 000000000..283332321 --- /dev/null +++ b/tools/vscode-hax-sourcemap/package.json @@ -0,0 +1,87 @@ +{ + "name": "vscode-hax-sourcemap", + "displayName": "Hax Source Map", + "description": "Navigate between Lean extractions and Rust sources with colour-matched highlighting", + "version": "0.1.0", + "publisher": "hax", + "engines": { "vscode": "^1.85.0" }, + "categories": ["Other"], + "activationEvents": [ + "workspaceContains:**/*.lean.map", + "onLanguage:lean4", + "onLanguage:lean", + "onLanguage:rust" + ], + "main": "./out/extension.js", + "contributes": { + "commands": [ + { + "command": "hax.jumpToSource", + "title": "Hax: Jump to Rust Source", + "icon": "$(link-external)" + }, + { + "command": "hax.jumpToLean", + "title": "Hax: Jump to Lean Extraction", + "icon": "$(link-external)" + }, + { + "command": "hax.toggleRainbow", + "title": "Hax: Toggle Rainbow Colours" + } + ], + "keybindings": [ + { + "command": "hax.jumpToSource", + "key": "f12", + "when": "editorTextFocus && resourceExtname == .lean && hax.hasSourceMap" + }, + { + "command": "hax.jumpToLean", + "key": "alt+f12", + "when": "editorTextFocus && resourceExtname == .rs && hax.hasReverseMap" + } + ], + "menus": { + "editor/context": [ + { + "command": "hax.jumpToSource", + "when": "resourceExtname == .lean && hax.hasSourceMap", + "group": "navigation" + }, + { + "command": "hax.jumpToLean", + "when": "resourceExtname == .rs && hax.hasReverseMap", + "group": "navigation" + } + ] + }, + "configuration": { + "title": "Hax Source Map", + "properties": { + "hax.sourcemap.rainbowOnOpen": { + "type": "boolean", + "default": true, + "description": "Apply rainbow highlighting when a mapped Lean file is opened." + }, + "hax.sourcemap.rainbowOpacity": { + "type": "number", + "default": 0.07, + "minimum": 0.0, + "maximum": 1.0, + "description": "Background opacity for rainbow mode (0–1)." + } + } + } + }, + "scripts": { + "vscode:prepublish": "npm run compile", + "compile": "tsc -p .", + "watch": "tsc -watch -p ." + }, + "devDependencies": { + "@types/vscode": "^1.85.0", + "@types/node": "^20.0.0", + "typescript": "^5.3.0" + } +} diff --git a/tools/vscode-hax-sourcemap/src/extension.ts b/tools/vscode-hax-sourcemap/src/extension.ts new file mode 100644 index 000000000..27f9aca3d --- /dev/null +++ b/tools/vscode-hax-sourcemap/src/extension.ts @@ -0,0 +1,669 @@ +import * as vscode from 'vscode'; +import * as path from 'path'; +import * as fs from 'fs'; + +// ───────────────────────────────────────────────────────────────────────────── +// VLQ / Source Map v3 decoder +// ───────────────────────────────────────────────────────────────────────────── + +const BASE64 = 'ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz0123456789+/'; +const B64: Record = {}; +for (let i = 0; i < BASE64.length; i++) B64[BASE64[i]] = i; + +function decodeVlq(s: string, pos: number): [number, number] { + let result = 0, shift = 0; + for (;;) { + const digit = B64[s[pos++]]; + result |= (digit & 31) << shift; + shift += 5; + if (!(digit & 32)) { break; } + } + return [(result & 1) ? -(result >>> 1) : (result >>> 1), pos]; +} + +// ───────────────────────────────────────────────────────────────────────────── +// Types +// ───────────────────────────────────────────────────────────────────────────── + +interface Mapping { + genLine: number; + genCol: number; + srcIdx: number; + srcLine: number; + srcCol: number; +} + +interface SourceMapData { + mappings: Mapping[]; + sources: string[]; + sourcesContent: (string | null)[]; + /** srcIdx → resolved absolute filesystem path */ + resolvedPaths: Map; +} + +// ───────────────────────────────────────────────────────────────────────────── +// Source map parsing +// ───────────────────────────────────────────────────────────────────────────── + +function decodeSourceMap(mapFilePath: string): SourceMapData | null { + let raw: { sources?: string[]; sourcesContent?: (string|null)[]; mappings?: string }; + try { raw = JSON.parse(fs.readFileSync(mapFilePath, 'utf8')); } + catch { return null; } + + const sources: string[] = raw.sources ?? []; + const sourcesContent: (string | null)[] = raw.sourcesContent ?? sources.map(() => null); + const encoded: string = raw.mappings ?? ''; + const mappings: Mapping[] = []; + + let genLine = 0; + let pGC = 0, pSI = 0, pSL = 0, pSC = 0; + + for (let i = 0; i < encoded.length;) { + const ch = encoded[i]; + if (ch === ';') { genLine++; pGC = 0; i++; continue; } + if (ch === ',') { i++; continue; } + + let dGC: number; + [dGC, i] = decodeVlq(encoded, i); + const genCol = pGC + dGC; + pGC = genCol; + + if (i >= encoded.length || encoded[i] === ';' || encoded[i] === ',') { continue; } + + let dSI: number, dSL: number, dSC: number; + [dSI, i] = decodeVlq(encoded, i); + [dSL, i] = decodeVlq(encoded, i); + [dSC, i] = decodeVlq(encoded, i); + + // optional name index + if (i < encoded.length && encoded[i] !== ';' && encoded[i] !== ',') { + [, i] = decodeVlq(encoded, i); + } + + pSI += dSI; pSL += dSL; pSC += dSC; + mappings.push({ genLine, genCol, srcIdx: pSI, srcLine: pSL, srcCol: pSC }); + } + + const resolvedPaths = resolveSources(sources, mapFilePath); + return { mappings, sources, sourcesContent, resolvedPaths }; +} + +function normPath(p: string): string { + try { return fs.realpathSync(p); } catch { return path.resolve(p); } +} + +function resolveSources(sources: string[], mapFilePath: string): Map { + const resolved = new Map(); + const mapDir = path.dirname(mapFilePath); + + for (let idx = 0; idx < sources.length; idx++) { + const src = sources[idx]; + if (!src) { continue; } + + const tryAdd = (p: string) => { + if (fs.existsSync(p)) { resolved.set(idx, normPath(p)); return true; } + return false; + }; + + if (path.isAbsolute(src)) { tryAdd(src); continue; } + + // Workspace roots + let found = false; + for (const folder of vscode.workspace.workspaceFolders ?? []) { + if (tryAdd(path.join(folder.uri.fsPath, src))) { found = true; break; } + } + if (found) { continue; } + + // Walk up from map file + let dir = mapDir; + for (let depth = 0; depth < 12; depth++) { + if (tryAdd(path.join(dir, src))) { break; } + const parent = path.dirname(dir); + if (parent === dir) { break; } + dir = parent; + } + } + return resolved; +} + +// ───────────────────────────────────────────────────────────────────────────── +// Colour palette +// ───────────────────────────────────────────────────────────────────────────── + +// 8-colour palette, legible on dark and light themes. +const PALETTE: Array<{ r: number; g: number; b: number }> = [ + { r: 224, g: 108, b: 117 }, // red + { r: 229, g: 192, b: 123 }, // amber + { r: 152, g: 195, b: 121 }, // green + { r: 86, g: 182, b: 194 }, // cyan + { r: 97, g: 175, b: 239 }, // blue + { r: 198, g: 120, b: 221 }, // purple + { r: 209, g: 154, b: 102 }, // orange + { r: 171, g: 178, b: 191 }, // slate +]; +const N = PALETTE.length; + +function rgba(c: { r: number; g: number; b: number }, a: number): string { + return `rgba(${c.r},${c.g},${c.b},${a})`; +} + +function makeDecTypes(bgAlpha: number): { + bg: vscode.TextEditorDecorationType[]; + active: vscode.TextEditorDecorationType[]; +} { + const bg: vscode.TextEditorDecorationType[] = []; + const active: vscode.TextEditorDecorationType[] = []; + for (const c of PALETTE) { + bg.push(vscode.window.createTextEditorDecorationType({ + backgroundColor: rgba(c, bgAlpha), + isWholeLine: true, + overviewRulerColor: rgba(c, 0.6), + overviewRulerLane: vscode.OverviewRulerLane.Left, + })); + active.push(vscode.window.createTextEditorDecorationType({ + backgroundColor: rgba(c, Math.min(1, bgAlpha * 2.8)), + isWholeLine: true, + border: `0 0 0 3px solid ${rgba(c, 0.9)}`, + overviewRulerColor: rgba(c, 1.0), + overviewRulerLane: vscode.OverviewRulerLane.Full, + })); + } + return { bg, active }; +} + +// ───────────────────────────────────────────────────────────────────────────── +// Manager +// ───────────────────────────────────────────────────────────────────────────── + +class HaxManager { + private smCache = new Map(); + private colorMapCache = new Map>(); + /** rust absolute path → lean absolute paths that reference it */ + private rustToLean = new Map>(); + private decTypes: ReturnType; + private readonly statusBar: vscode.StatusBarItem; + private rainbowEnabled: boolean; + + constructor(private readonly ctx: vscode.ExtensionContext) { + const cfg = vscode.workspace.getConfiguration('hax.sourcemap'); + this.rainbowEnabled = cfg.get('rainbowOnOpen', true); + this.decTypes = makeDecTypes(cfg.get('rainbowOpacity', 0.07)); + + this.statusBar = vscode.window.createStatusBarItem(vscode.StatusBarAlignment.Right, 100); + this.statusBar.command = 'hax.jumpToSource'; + ctx.subscriptions.push(this.statusBar); + + ctx.subscriptions.push(vscode.workspace.onDidChangeConfiguration(e => { + if (!e.affectsConfiguration('hax.sourcemap')) { return; } + const newCfg = vscode.workspace.getConfiguration('hax.sourcemap'); + this.rainbowEnabled = newCfg.get('rainbowOnOpen', true); + // Dispose old decoration types and recreate with new opacity. + for (const d of [...this.decTypes.bg, ...this.decTypes.active]) { d.dispose(); } + this.decTypes = makeDecTypes(newCfg.get('rainbowOpacity', 0.07)); + for (const editor of vscode.window.visibleTextEditors) { this.update(editor); } + })); + } + + // ── Source map access ──────────────────────────────────────────────────── + + private loadSourceMap(leanPath: string): SourceMapData | null { + if (this.smCache.has(leanPath)) { return this.smCache.get(leanPath)!; } + const mapPath = leanPath + '.map'; + const sm = fs.existsSync(mapPath) ? decodeSourceMap(mapPath) : null; + this.smCache.set(leanPath, sm); + if (sm) { + this.colorMapCache.set(leanPath, buildColorMap(sm)); + for (const [, resolved] of sm.resolvedPaths) { + if (!this.rustToLean.has(resolved)) { this.rustToLean.set(resolved, new Set()); } + this.rustToLean.get(resolved)!.add(leanPath); + } + // Update context key for rust files + vscode.commands.executeCommand('setContext', 'hax.hasReverseMap', + this.rustToLean.size > 0); + } + return sm; + } + + private getColorMap(leanPath: string): Map { + if (this.colorMapCache.has(leanPath)) { return this.colorMapCache.get(leanPath)!; } + const sm = this.loadSourceMap(leanPath); + if (!sm) { return new Map(); } + const cm = buildColorMap(sm); + this.colorMapCache.set(leanPath, cm); + return cm; + } + + // ── Main update entry ──────────────────────────────────────────────────── + + update(editor: vscode.TextEditor) { + const p = editor.document.uri.fsPath; + if (p.endsWith('.lean')) { this.updateLean(editor); } + else if (p.endsWith('.rs')) { this.updateRust(editor); } + } + + // ── Lean file update ───────────────────────────────────────────────────── + + private updateLean(editor: vscode.TextEditor) { + const leanPath = editor.document.uri.fsPath; + const sm = this.loadSourceMap(leanPath); + + if (!sm) { + this.clearAll(editor); + this.statusBar.hide(); + vscode.commands.executeCommand('setContext', 'hax.hasSourceMap', false); + return; + } + + vscode.commands.executeCommand('setContext', 'hax.hasSourceMap', true); + const colorMap = this.getColorMap(leanPath); + const cursor = editor.selection.active; + + // Rainbow background + if (this.rainbowEnabled) { + const buckets: vscode.Range[][] = Array.from({ length: N }, () => []); + for (const [line, ci] of colorMap) { + buckets[ci].push(new vscode.Range(line, 0, line, 0)); + } + for (let i = 0; i < N; i++) { editor.setDecorations(this.decTypes.bg[i], buckets[i]); } + } else { + for (let i = 0; i < N; i++) { editor.setDecorations(this.decTypes.bg[i], []); } + } + + // Active cursor highlight + const activeMappings = findActiveSegment(sm, colorMap, cursor.line, cursor.character); + for (let i = 0; i < N; i++) { editor.setDecorations(this.decTypes.active[i], []); } + + if (activeMappings.length > 0) { + const ci = colorMap.get(activeMappings[0].genLine) ?? 0; + editor.setDecorations(this.decTypes.active[ci], + activeMappings.map(m => new vscode.Range(m.genLine, 0, m.genLine, 0))); + + const rep = activeMappings[0]; + const srcPath = sm.resolvedPaths.get(rep.srcIdx) ?? sm.sources[rep.srcIdx] ?? '?'; + this.statusBar.text = `$(link) ${path.basename(srcPath)}:${rep.srcLine + 1}`; + this.statusBar.tooltip = `Rust source: ${srcPath}:${rep.srcLine + 1}:${rep.srcCol + 1}\nClick to jump`; + this.statusBar.show(); + + // Highlight paired rust editors + for (const ve of vscode.window.visibleTextEditors) { + if (ve.document.uri.fsPath.endsWith('.rs')) { + this.applyRainbowToRust(ve, sm, colorMap, leanPath, rep, ci); + } + } + } else { + this.statusBar.hide(); + // Still paint rainbow on rust if visible + for (const ve of vscode.window.visibleTextEditors) { + if (ve.document.uri.fsPath.endsWith('.rs')) { + this.applyRainbowToRust(ve, sm, colorMap, leanPath, null, -1); + } + } + } + } + + // ── Rust file update ───────────────────────────────────────────────────── + + private updateRust(editor: vscode.TextEditor) { + const rustPath = normPath(editor.document.uri.fsPath); + + // Ensure lean source maps are loaded for any open lean editors + for (const ve of vscode.window.visibleTextEditors) { + if (ve.document.fileName.endsWith('.lean')) { + this.loadSourceMap(ve.document.uri.fsPath); + } + } + + const leanPaths = this.rustToLean.get(rustPath); + if (!leanPaths || leanPaths.size === 0) { + this.clearAll(editor); + return; + } + vscode.commands.executeCommand('setContext', 'hax.hasReverseMap', true); + + const cursor = editor.selection.active; + + for (const leanPath of leanPaths) { + const sm = this.loadSourceMap(leanPath); + if (!sm) { continue; } + const colorMap = this.getColorMap(leanPath); + const srcIdx = [...sm.resolvedPaths.entries()].find(([, p]) => p === rustPath)?.[0]; + if (srcIdx === undefined) { continue; } + + this.applyRainbowToRust(editor, sm, colorMap, leanPath, null, -1); + + // Active: highlight current rust line + const rustLineMappings = sm.mappings.filter( + m => m.srcIdx === srcIdx && m.srcLine === cursor.line); + if (rustLineMappings.length > 0) { + const ci = colorMap.get(rustLineMappings[0].genLine) ?? 0; + for (let i = 0; i < N; i++) { editor.setDecorations(this.decTypes.active[i], []); } + editor.setDecorations(this.decTypes.active[ci], + [new vscode.Range(cursor.line, 0, cursor.line, 0)]); + } + + // Highlight lean editor if visible + for (const ve of vscode.window.visibleTextEditors) { + if (ve.document.uri.fsPath !== leanPath) { continue; } + const leanMappings = sm.mappings.filter( + m => m.srcIdx === srcIdx && m.srcLine === cursor.line); + for (let i = 0; i < N; i++) { ve.setDecorations(this.decTypes.active[i], []); } + if (leanMappings.length > 0) { + const ci = colorMap.get(leanMappings[0].genLine) ?? 0; + ve.setDecorations(this.decTypes.active[ci], + leanMappings.map(m => new vscode.Range(m.genLine, 0, m.genLine, 0))); + } + } + } + } + + private applyRainbowToRust( + editor: vscode.TextEditor, + sm: SourceMapData, + colorMap: Map, + _leanPath: string, + activeMapping: Mapping | null, + activeCi: number, + ) { + const rustPath = normPath(editor.document.uri.fsPath); + const srcIdx = [...sm.resolvedPaths.entries()].find(([, p]) => p === rustPath)?.[0]; + if (srcIdx === undefined) { return; } + + if (this.rainbowEnabled) { + // Build rust-line → colorIdx (one representative per source line). + const rustLineColor = new Map(); + for (const m of sm.mappings) { + if (m.srcIdx !== srcIdx) { continue; } + if (rustLineColor.has(m.srcLine)) { continue; } + const ci = colorMap.get(m.genLine); + if (ci !== undefined) { rustLineColor.set(m.srcLine, ci); } + } + + // Sort and build contiguous ranges so gaps between mapped lines are filled. + const sorted = [...rustLineColor.entries()].sort((a, b) => a[0] - b[0]); + const buckets: vscode.Range[][] = Array.from({ length: N }, () => []); + for (let i = 0; i < sorted.length; i++) { + const [startLine, ci] = sorted[i]; + const endLine = i + 1 < sorted.length ? sorted[i + 1][0] - 1 : startLine; + buckets[ci].push(new vscode.Range(startLine, 0, endLine, 0)); + } + for (let i = 0; i < N; i++) { editor.setDecorations(this.decTypes.bg[i], buckets[i]); } + } + + if (activeMapping !== null && activeMapping.srcIdx === srcIdx) { + for (let i = 0; i < N; i++) { editor.setDecorations(this.decTypes.active[i], []); } + editor.setDecorations(this.decTypes.active[activeCi], + [new vscode.Range(activeMapping.srcLine, 0, activeMapping.srcLine, 0)]); + } + } + + private clearAll(editor: vscode.TextEditor) { + for (let i = 0; i < N; i++) { + editor.setDecorations(this.decTypes.bg[i], []); + editor.setDecorations(this.decTypes.active[i], []); + } + } + + // ── Commands ───────────────────────────────────────────────────────────── + + async jumpToSource() { + const editor = vscode.window.activeTextEditor; + if (!editor || !editor.document.fileName.endsWith('.lean')) { return; } + + const sm = this.loadSourceMap(editor.document.uri.fsPath); + if (!sm) { + vscode.window.showWarningMessage('Hax: no source map found for this file.'); + return; + } + + const cursor = editor.selection.active; + const m = closestMapping(sm.mappings, cursor.line, cursor.character); + if (!m) { + vscode.window.showWarningMessage('Hax: no mapping at cursor position.'); + return; + } + + const resolved = sm.resolvedPaths.get(m.srcIdx); + if (!resolved) { + const content = sm.sourcesContent[m.srcIdx]; + if (content) { + const doc = await vscode.workspace.openTextDocument({ + language: 'rust', + content: `// Source: ${sm.sources[m.srcIdx]}\n// (file not found on disk)\n\n${content}`, + }); + const te = await vscode.window.showTextDocument(doc, vscode.ViewColumn.Beside); + const pos = new vscode.Position(m.srcLine + 3 /* header offset */, m.srcCol); + te.selection = new vscode.Selection(pos, pos); + te.revealRange(new vscode.Range(pos, pos), vscode.TextEditorRevealType.InCenter); + } else { + vscode.window.showWarningMessage(`Hax: source file not found: ${sm.sources[m.srcIdx]}`); + } + return; + } + + const doc = await vscode.workspace.openTextDocument(vscode.Uri.file(resolved)); + const te = await vscode.window.showTextDocument(doc, vscode.ViewColumn.Beside); + const pos = new vscode.Position(m.srcLine, m.srcCol); + te.selection = new vscode.Selection(pos, pos); + te.revealRange(new vscode.Range(pos, pos), vscode.TextEditorRevealType.InCenter); + } + + async jumpToLean() { + const editor = vscode.window.activeTextEditor; + if (!editor) { return; } + + const rustPath = editor.document.uri.fsPath; + + // Eagerly load source maps for open lean editors + for (const ve of vscode.window.visibleTextEditors) { + if (ve.document.fileName.endsWith('.lean')) { + this.loadSourceMap(ve.document.uri.fsPath); + } + } + + let leanPaths = this.rustToLean.get(rustPath); + + // If still empty, search workspace for .lean.map files + if (!leanPaths || leanPaths.size === 0) { + const maps = await vscode.workspace.findFiles('**/*.lean.map', '**/node_modules/**', 20); + for (const mapUri of maps) { + const leanPath = mapUri.fsPath.replace(/\.map$/, ''); + this.loadSourceMap(leanPath); + } + leanPaths = this.rustToLean.get(rustPath); + } + + if (!leanPaths || leanPaths.size === 0) { + vscode.window.showWarningMessage('Hax: no Lean extraction found for this Rust file.'); + return; + } + + const cursorLine = editor.selection.active.line; + + for (const leanPath of leanPaths) { + const sm = this.loadSourceMap(leanPath); + if (!sm) { continue; } + const srcIdx = [...sm.resolvedPaths.entries()].find(([, p]) => p === rustPath)?.[0]; + if (srcIdx === undefined) { continue; } + + const candidates = sm.mappings + .filter(m => m.srcIdx === srcIdx && m.srcLine <= cursorLine + 5) + .sort((a, b) => Math.abs(a.srcLine - cursorLine) - Math.abs(b.srcLine - cursorLine)); + + if (candidates.length === 0) { continue; } + + const best = candidates[0]; + const doc = await vscode.workspace.openTextDocument(vscode.Uri.file(leanPath)); + const te = await vscode.window.showTextDocument(doc, vscode.ViewColumn.Beside); + const pos = new vscode.Position(best.genLine, best.genCol); + te.selection = new vscode.Selection(pos, pos); + te.revealRange(new vscode.Range(pos, pos), vscode.TextEditorRevealType.InCenter); + return; + } + + vscode.window.showWarningMessage('Hax: no mapping found near cursor position.'); + } + + toggleRainbow() { + this.rainbowEnabled = !this.rainbowEnabled; + vscode.window.showInformationMessage( + `Hax rainbow colours ${this.rainbowEnabled ? 'enabled' : 'disabled'}`); + for (const editor of vscode.window.visibleTextEditors) { this.update(editor); } + } + + invalidateCache() { + this.smCache.clear(); + this.colorMapCache.clear(); + this.rustToLean.clear(); + } +} + +// ───────────────────────────────────────────────────────────────────────────── +// Pure helpers +// ───────────────────────────────────────────────────────────────────────────── + +/** Assign a stable colour index to each (srcIdx:srcLine) key. */ +function buildColorMap(sm: SourceMapData): Map { + const colorMap = new Map(); + const keyToColor = new Map(); + + // Representative mapping per lean line (first one) + const lineRep = new Map(); + for (const m of sm.mappings) { + if (!lineRep.has(m.genLine)) { lineRep.set(m.genLine, m); } + } + + let next = 0; + // Sort by lean line so colours flow top-to-bottom + for (const [genLine, m] of [...lineRep.entries()].sort((a, b) => a[0] - b[0])) { + const key = `${m.srcIdx}:${m.srcLine}`; + if (!keyToColor.has(key)) { keyToColor.set(key, next++ % N); } + colorMap.set(genLine, keyToColor.get(key)!); + } + return colorMap; +} + +/** Find the mapping entry at or just before (line, col). */ +function closestMapping(mappings: Mapping[], line: number, col: number): Mapping | null { + let best: Mapping | null = null; + for (const m of mappings) { + if (m.genLine > line) { break; } + if (m.genLine < line || m.genCol <= col) { best = m; } + } + return best; +} + +/** + * Given a cursor position in the lean file, return all lean mappings that + * belong to the same "active segment" (same srcIdx + srcLine as the cursor mapping). + */ +function findActiveSegment( + sm: SourceMapData, + colorMap: Map, + cursorLine: number, + cursorCol: number, +): Mapping[] { + const rep = closestMapping(sm.mappings, cursorLine, cursorCol); + if (!rep) { return []; } + + // All lean lines that map to the same (srcIdx, srcLine) + const seen = new Set(); + return sm.mappings.filter(m => { + if (m.srcIdx !== rep.srcIdx || m.srcLine !== rep.srcLine) { return false; } + if (seen.has(m.genLine)) { return false; } + seen.add(m.genLine); + return true; + }); +} + +// ───────────────────────────────────────────────────────────────────────────── +// Hover provider +// ───────────────────────────────────────────────────────────────────────────── + +class HaxHoverProvider implements vscode.HoverProvider { + constructor(private readonly mgr: HaxManager) {} + + provideHover( + document: vscode.TextDocument, + position: vscode.Position, + ): vscode.Hover | null { + const leanPath = document.uri.fsPath; + // Access the manager's source map via the public helper + const mapPath = leanPath + '.map'; + if (!fs.existsSync(mapPath)) { return null; } + // Decode inline (cached by mgr internally via update, but we need sm here) + let raw: { sources?: string[]; sourcesContent?: (string|null)[]; mappings?: string }; + try { raw = JSON.parse(fs.readFileSync(mapPath, 'utf8')); } + catch { return null; } + + const sources: string[] = raw.sources ?? []; + const sourcesContent: (string | null)[] = raw.sourcesContent ?? []; + const sm = decodeSourceMap(mapPath); + if (!sm) { return null; } + + const m = closestMapping(sm.mappings, position.line, position.character); + if (!m) { return null; } + + const srcPath = sm.resolvedPaths.get(m.srcIdx) ?? sources[m.srcIdx]; + if (!srcPath) { return null; } + + // Get a few lines of context + let snippet: string; + const content = sourcesContent[m.srcIdx]; + if (content) { + const lines = content.split('\n'); + const start = Math.max(0, m.srcLine - 1); + const end = Math.min(lines.length, m.srcLine + 3); + snippet = lines.slice(start, end).join('\n'); + } else { + try { + const lines = fs.readFileSync(srcPath, 'utf8').split('\n'); + const start = Math.max(0, m.srcLine - 1); + const end = Math.min(lines.length, m.srcLine + 3); + snippet = lines.slice(start, end).join('\n'); + } catch { + snippet = ''; + } + } + + const label = `**Rust source** — \`${path.basename(srcPath)}\` line ${m.srcLine + 1}`; + const md = new vscode.MarkdownString( + `${label}\n\`\`\`rust\n${snippet}\n\`\`\`` + ); + return new vscode.Hover(md); + } +} + +// ───────────────────────────────────────────────────────────────────────────── +// Extension entry point +// ───────────────────────────────────────────────────────────────────────────── + +export function activate(ctx: vscode.ExtensionContext) { + const mgr = new HaxManager(ctx); + + // Initial decoration pass + for (const editor of vscode.window.visibleTextEditors) { mgr.update(editor); } + + ctx.subscriptions.push( + vscode.window.onDidChangeActiveTextEditor(e => { if (e) { mgr.update(e); } }), + vscode.window.onDidChangeTextEditorSelection(e => { mgr.update(e.textEditor); }), + vscode.window.onDidChangeVisibleTextEditors(editors => { + for (const e of editors) { mgr.update(e); } + }), + // Invalidate cache when .lean.map files change on disk + vscode.workspace.onDidSaveTextDocument(doc => { + if (doc.fileName.endsWith('.lean.map') || doc.fileName.endsWith('.lean')) { + mgr.invalidateCache(); + for (const e of vscode.window.visibleTextEditors) { mgr.update(e); } + } + }), + vscode.commands.registerCommand('hax.jumpToSource', () => mgr.jumpToSource()), + vscode.commands.registerCommand('hax.jumpToLean', () => mgr.jumpToLean()), + vscode.commands.registerCommand('hax.toggleRainbow', () => mgr.toggleRainbow()), + vscode.languages.registerHoverProvider( + [{ language: 'lean4' }, { language: 'lean' }, { pattern: '**/*.lean' }], + new HaxHoverProvider(mgr), + ), + ); +} + +export function deactivate() {} diff --git a/tools/vscode-hax-sourcemap/tsconfig.json b/tools/vscode-hax-sourcemap/tsconfig.json new file mode 100644 index 000000000..6c9a9b5d4 --- /dev/null +++ b/tools/vscode-hax-sourcemap/tsconfig.json @@ -0,0 +1,12 @@ +{ + "compilerOptions": { + "module": "commonjs", + "target": "ES2020", + "outDir": "out", + "lib": ["ES2020"], + "sourceMap": true, + "rootDir": "src", + "strict": true + }, + "exclude": ["node_modules", ".vscode-test"] +}