diff --git a/Cargo.lock b/Cargo.lock index 69ae4476c9..a8e4b888b2 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -5287,6 +5287,7 @@ dependencies = [ name = "husky-figure-zone-protocol" version = "0.1.0" dependencies = [ + "enum-class", "serde", "shifted-unsigned-int", ] @@ -6788,6 +6789,7 @@ dependencies = [ "husky-standard-linket-impl", "husky-trace-protocol", "husky-visual-protocol", + "itertools 0.13.0", "rustc-hash 2.0.0", "serde", "ui", @@ -7467,6 +7469,7 @@ dependencies = [ "egui", "enum-class", "expect-test", + "husky-figure-zone-protocol", "husky-print-utils", "ordered-float 4.2.2", "serde", @@ -7735,6 +7738,7 @@ dependencies = [ "husky-check-utils", "husky-print-utils", "salsa", + "serde", ] [[package]] @@ -8228,6 +8232,7 @@ dependencies = [ "latex-vfs", "ptree", "salsa", + "serde", "smallvec", "time-capsule", ] @@ -8236,7 +8241,18 @@ dependencies = [ name = "latex-ast-hsy" version = "0.1.0" dependencies = [ + "husky-core", + "husky-linket-impl", + "husky-path-utils", + "husky-standard-linket-impl", + "husky-standard-value", + "idx-arena", "latex-ast", + "latex-prelude", + "latex-vfs", + "lazy_static 1.5.0", + "serde", + "vec-like", ] [[package]] diff --git a/crates/abstractions/idx-arena/Cargo.toml b/crates/abstractions/idx-arena/Cargo.toml index 8143d07d56..9f77350f95 100644 --- a/crates/abstractions/idx-arena/Cargo.toml +++ b/crates/abstractions/idx-arena/Cargo.toml @@ -9,6 +9,7 @@ edition = "2021" doctest = false [dependencies] +serde.workspace = true # abstractions salsa.workspace = true # utils diff --git a/crates/abstractions/idx-arena/src/arena_idx.rs b/crates/abstractions/idx-arena/src/arena_idx.rs index 727f00a857..01322d926a 100644 --- a/crates/abstractions/idx-arena/src/arena_idx.rs +++ b/crates/abstractions/idx-arena/src/arena_idx.rs @@ -1,4 +1,5 @@ use crate::*; +use serde::{Deserialize, Serialize}; use std::{num::NonZeroU32, ops::AddAssign}; pub struct ArenaIdx { @@ -6,6 +7,22 @@ pub struct ArenaIdx { phantom: PhantomData, } +impl Serialize for ArenaIdx { + fn serialize(&self, serializer: S) -> Result { + serializer.serialize_u32(self.raw.get()) + } +} + +impl<'de, T> Deserialize<'de> for ArenaIdx { + fn deserialize(deserializer: D) -> Result + where + D: serde::Deserializer<'de>, + { + let raw = u32::deserialize(deserializer)?; + Ok(Self::new(raw as usize)) + } +} + #[test] fn option_arena_idx_size_works() { assert_eq!( diff --git a/crates/abstractions/idx-arena/src/ordered_map.rs b/crates/abstractions/idx-arena/src/ordered_map.rs index b44e2e5316..8889ce8b51 100644 --- a/crates/abstractions/idx-arena/src/ordered_map.rs +++ b/crates/abstractions/idx-arena/src/ordered_map.rs @@ -42,6 +42,16 @@ impl ArenaOrderedMap { pub unsafe fn insert_next_unchecked(&mut self, v: V) { self.data.push(v) } + + pub fn insert_next_batch( + &mut self, + items: impl IntoIterator>, + comments: impl IntoIterator, + ) { + for (idx, comment) in items.into_iter().zip(comments) { + self.insert_next(idx, comment); + } + } } impl std::ops::Index> for ArenaOrderedMap { diff --git a/crates/devtime/husky-devtime/src/figure.rs b/crates/devtime/husky-devtime/src/figure.rs new file mode 100644 index 0000000000..c55667f1bb --- /dev/null +++ b/crates/devtime/husky-devtime/src/figure.rs @@ -0,0 +1,44 @@ +use crate::Devtime; +use husky_devsoul::devsoul::IsDevsoul; +use husky_entity_path::path::{major_item::MajorItemPath, ItemPath, ItemPathId}; +use husky_figure_zone_protocol::chunk_base::{text::FigureTextChunkBaseData, FigureChunkBase}; +use husky_item_path_interface::ItemPathIdInterface; +use husky_linket::linket::Linket; +use husky_linket_impl::ugly::__IsLinketImpl; +use husky_visual_protocol::synchrotron::VisualSynchrotron; + +impl Devtime { + pub fn figure_chunk_base( + &self, + static_var: ItemPathIdInterface, + chunk_idx: u32, + visual_synchrotron: &mut VisualSynchrotron, + ) -> FigureChunkBase { + self.figure_chunk_base_cache + .entry((static_var, chunk_idx)) + .or_insert_with(|| { + visual_synchrotron.alloc_figure_text_chunk_base( + self.calc_figure_chunk_base(static_var, chunk_idx), + ) + }) + .clone() + } + + fn calc_figure_chunk_base( + &self, + static_var: ItemPathIdInterface, + chunk_idx: u32, + ) -> FigureTextChunkBaseData { + let db = self.db(); + let item_path_id: ItemPathId = static_var.into(); + let item_path: ItemPath = item_path_id.item_path(db); + let ItemPath::MajorItem(MajorItemPath::Form(major_form_path)) = item_path else { + unreachable!() + }; + let linket = Linket::new_var(major_form_path, db); + let linket_impl = self.runtime.comptime().linket_impl(linket); + linket_impl + .static_var_svtable() + .figure_chunk_base(chunk_idx) + } +} diff --git a/crates/devtime/husky-devtime/src/lib.rs b/crates/devtime/husky-devtime/src/lib.rs index af7455eb65..27d953a8d5 100644 --- a/crates/devtime/husky-devtime/src/lib.rs +++ b/crates/devtime/husky-devtime/src/lib.rs @@ -2,6 +2,7 @@ #![feature(result_flattening)] #![feature(try_trait_v2)] pub mod eval; +mod figure; mod state; #[cfg(test)] mod tests; @@ -17,11 +18,11 @@ use husky_devsoul::{ devsoul::IsDevsoul, helpers::{ DevsoulCaryatid, DevsoulChart, DevsoulFigure, DevsoulKiControlFlow, DevsoulStaticVarResult, - DevsoulTraceStalk, DevsoulVmControlFlowFrozen, + DevsoulTraceStalk, DevsoulVarId, DevsoulVmControlFlowFrozen, }, }; use husky_entity_path::path::ItemPathId; -use husky_figure_zone_protocol::FigureZone; +use husky_figure_zone_protocol::{chunk_base::FigureChunkBase, FigureZone}; use husky_item_path_interface::ItemPathIdInterface; use husky_ki_repr::repr::KiRepr; use husky_ki_repr_interface::{KiDomainReprInterface, KiReprInterface}; @@ -66,6 +67,9 @@ pub struct Devtime { // when hot reload, reset this // TODO benchmark this eager_trace_cache: DashMap<(TracePath, Devsoul::Pedestal), Arc>>, + // cache figure chunk bases + // when hot reload, reset this + figure_chunk_base_cache: DashMap<(ItemPathIdInterface, u32), FigureChunkBase>, vmir_storage: DevVmirStorage, } @@ -77,6 +81,7 @@ impl Devtime { Ok(Self { runtime: DevRuntime::new(target_crate, runtime_config)?, eager_trace_cache: Default::default(), + figure_chunk_base_cache: Default::default(), vmir_storage: Default::default(), }) } @@ -187,26 +192,33 @@ impl IsTracetime for Devtime { let trace_plot_map = trace_visual_cache.calc_plots(figure_key.traces().collect()); match figure_key.figure_zone() { Some(zone) => match zone { - FigureZone::Gallery => match chart { + FigureZone::Parade => match chart { Some(chart) => match chart { Chart::Dim0(_) => todo!(), Chart::Dim1(chart) => { - IsFigure::new_gallery(chart, trace_plot_map, visual_synchrotron) + IsFigure::new_parading(chart, trace_plot_map, visual_synchrotron) } Chart::Dim2(chart) => todo!(), }, None => IsFigure::new_void(), // ad hoc }, - FigureZone::Text => match chart { - Some(chart) => match chart { - Chart::Dim0(_) => todo!(), - Chart::Dim1(chart) => { - IsFigure::new_text(Some(chart), trace_plot_map, visual_synchrotron) - } - Chart::Dim2(chart) => todo!(), - }, - None => IsFigure::new_text(None, trace_plot_map, visual_synchrotron), // ad hoc - }, + FigureZone::Roll => { + debug_assert_eq!(figure_key.generic_joint_static_vars().count(), 1); + let the_static_var = figure_key.generic_joint_static_vars().next().unwrap(); + let chart = match chart { + Some(Chart::Dim1(chart)) => Some(chart), + None => None, + _ => unreachable!(), + }; + IsFigure::new_rolling( + chart, + trace_plot_map, + visual_synchrotron, + |chunk_idx, visual_synchrotron| { + self.figure_chunk_base(the_static_var, chunk_idx, visual_synchrotron) + }, + ) + } }, None => match chart { Some(chart) => { diff --git a/crates/devtime/husky-trace/expect-files/registry/latex-ast-hsy-0.1.0/find_traces/src/lib.md b/crates/devtime/husky-trace/expect-files/registry/latex-ast-hsy-0.1.0/find_traces/src/lib.md index b545b60e79..ac867a127f 100644 --- a/crates/devtime/husky-trace/expect-files/registry/latex-ast-hsy-0.1.0/find_traces/src/lib.md +++ b/crates/devtime/husky-trace/expect-files/registry/latex-ast-hsy-0.1.0/find_traces/src/lib.md @@ -1,3 +1,32 @@ ```rust -[] +[ + ( + Trace { + path: TracePath { + data: TracePathData::StaticVarItem( + StaticVarTracePathData { + static_var_item_path: MajorFormPath(`latex_ast_hsy::AST`, `StaticVar`), + }, + ), + }, + data: StaticVar( + StaticVarTraceData { + path: TracePath( + Id { + value: 1, + }, + ), + static_var_item_path: MajorFormPath( + ItemPathId( + Id { + value: 2, + }, + ), + ), + }, + ), + }, + (), + ), +] ``` \ No newline at end of file diff --git a/crates/devtime/husky-trace/expect-files/registry/latex-ast-hsy-0.1.0/root_traces/src/lib.md b/crates/devtime/husky-trace/expect-files/registry/latex-ast-hsy-0.1.0/root_traces/src/lib.md index b545b60e79..d0a819e2fe 100644 --- a/crates/devtime/husky-trace/expect-files/registry/latex-ast-hsy-0.1.0/root_traces/src/lib.md +++ b/crates/devtime/husky-trace/expect-files/registry/latex-ast-hsy-0.1.0/root_traces/src/lib.md @@ -1,3 +1,29 @@ ```rust -[] +[ + Trace { + path: TracePath { + data: TracePathData::StaticVarItem( + StaticVarTracePathData { + static_var_item_path: MajorFormPath(`latex_ast_hsy::AST`, `StaticVar`), + }, + ), + }, + data: StaticVar( + StaticVarTraceData { + path: TracePath( + Id { + value: 1, + }, + ), + static_var_item_path: MajorFormPath( + ItemPathId( + Id { + value: 2, + }, + ), + ), + }, + ), + }, +] ``` \ No newline at end of file diff --git a/crates/devtime/husky-trace/expect-files/registry/latex-ast-hsy-0.1.0/trace_ki_repr/src/lib.md b/crates/devtime/husky-trace/expect-files/registry/latex-ast-hsy-0.1.0/trace_ki_repr/src/lib.md index b545b60e79..39a5c38c67 100644 --- a/crates/devtime/husky-trace/expect-files/registry/latex-ast-hsy-0.1.0/trace_ki_repr/src/lib.md +++ b/crates/devtime/husky-trace/expect-files/registry/latex-ast-hsy-0.1.0/trace_ki_repr/src/lib.md @@ -1,3 +1,56 @@ ```rust -[] +[ + ( + Trace { + path: TracePath { + data: TracePathData::StaticVarItem( + StaticVarTracePathData { + static_var_item_path: MajorFormPath(`latex_ast_hsy::AST`, `StaticVar`), + }, + ), + }, + data: StaticVar( + StaticVarTraceData { + path: TracePath( + Id { + value: 1, + }, + ), + static_var_item_path: MajorFormPath( + ItemPathId( + Id { + value: 2, + }, + ), + ), + }, + ), + }, + Some( + KiRepr { + ki_domain_repr: Omni, + opn: KiOpn::Linket( + Linket { + data: LinketData::MajorStaticVar { + path: MajorFormPath(`latex_ast_hsy::AST`, `StaticVar`), + instantiation: LinInstantiation { + path: ItemPath(`latex_ast_hsy::AST`), + context: LinTypeContext { + comptime_var_overrides: [], + }, + variable_resolutions: [], + separator: None, + }, + }, + }, + ), + arguments: [], + source: KiReprSource::Val( + MajorFormPath(`latex_ast_hsy::AST`, `StaticVar`), + ), + caching_class: Val, + }, + ), + ), +] ``` \ No newline at end of file diff --git a/crates/devtime/husky-trace/expect-files/registry/latex-ast-hsy-0.1.0/trace_var_deps/src/lib.md b/crates/devtime/husky-trace/expect-files/registry/latex-ast-hsy-0.1.0/trace_var_deps/src/lib.md index b545b60e79..c7f0dc810e 100644 --- a/crates/devtime/husky-trace/expect-files/registry/latex-ast-hsy-0.1.0/trace_var_deps/src/lib.md +++ b/crates/devtime/husky-trace/expect-files/registry/latex-ast-hsy-0.1.0/trace_var_deps/src/lib.md @@ -1,3 +1,34 @@ ```rust -[] +[ + ( + Trace { + path: TracePath { + data: TracePathData::StaticVarItem( + StaticVarTracePathData { + static_var_item_path: MajorFormPath(`latex_ast_hsy::AST`, `StaticVar`), + }, + ), + }, + data: StaticVar( + StaticVarTraceData { + path: TracePath( + Id { + value: 1, + }, + ), + static_var_item_path: MajorFormPath( + ItemPathId( + Id { + value: 2, + }, + ), + ), + }, + ), + }, + [ + ItemPath(`latex_ast_hsy::AST`), + ], + ), +] ``` \ No newline at end of file diff --git a/crates/devtime/husky-trace/expect-files/registry/latex-ast-hsy-0.1.0/trace_view_data/src/lib.md b/crates/devtime/husky-trace/expect-files/registry/latex-ast-hsy-0.1.0/trace_view_data/src/lib.md index b545b60e79..b4c985ef67 100644 --- a/crates/devtime/husky-trace/expect-files/registry/latex-ast-hsy-0.1.0/trace_view_data/src/lib.md +++ b/crates/devtime/husky-trace/expect-files/registry/latex-ast-hsy-0.1.0/trace_view_data/src/lib.md @@ -1,3 +1,63 @@ ```rust -[] +[ + ( + Trace( + Id { + value: 1, + }, + ), + TraceViewData { + trace_kind: StaticVar, + lines_data: [ + TraceViewLineData { + tokens_data: [ + TraceViewTokenData { + text: "pub", + token_class: OtherKeyword, + spaces_before: 0, + assoc_trace_id: None, + }, + TraceViewTokenData { + text: "static", + token_class: OtherKeyword, + spaces_before: 1, + assoc_trace_id: None, + }, + TraceViewTokenData { + text: "var", + token_class: OtherKeyword, + spaces_before: 1, + assoc_trace_id: None, + }, + TraceViewTokenData { + text: "AST", + token_class: StaticVarEntity, + spaces_before: 1, + assoc_trace_id: None, + }, + TraceViewTokenData { + text: ":", + token_class: Punctuation, + spaces_before: 0, + assoc_trace_id: None, + }, + TraceViewTokenData { + text: "LxAstId", + token_class: TypeEntity, + spaces_before: 1, + assoc_trace_id: None, + }, + TraceViewTokenData { + text: ";", + token_class: Punctuation, + spaces_before: 0, + assoc_trace_id: None, + }, + ], + }, + ], + have_subtraces: false, + }, + ), +] ``` \ No newline at end of file diff --git a/crates/hir/husky-hir-decl/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.module_hir_decls.md b/crates/hir/husky-hir-decl/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.module_hir_decls.md index 933a862065..1b99c4fd31 100644 --- a/crates/hir/husky-hir-decl/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.module_hir_decls.md +++ b/crates/hir/husky-hir-decl/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.module_hir_decls.md @@ -38,5 +38,47 @@ ), ), ), + HirDecl::MajorItem( + MajorItemHirDecl::Form( + MajorFormHirDecl::StaticVar( + MajorStaticVarHirDecl { + path: MajorFormPath(`latex_ast_hsy::AST`, `StaticVar`), + return_ty: HirType::PathLeading( + HirTypePathLeading { + ty_path: TypePath(`latex_ast_hsy::LxAstId`, `Extern`), + template_arguments: [], + always_copyable: false, + }, + ), + hir_eager_expr_region: HirEagerExprRegion { + region_path: RegionPath::ItemDecl( + ItemPath(`latex_ast_hsy::AST`), + ), + self_value_ty: None, + expr_arena: Arena { + data: [], + }, + stmt_arena: Arena { + data: [], + }, + pattern_arena: Arena { + data: [], + }, + comptime_variable_region_data: HirEagerComptimeVariableRegionData { + arena: Arena { + data: [], + }, + }, + runtime_variable_region_data: HirEagerRuntimeVariableRegionData { + arena: Arena { + data: [], + }, + self_value_variable: None, + }, + }, + }, + ), + ), + ), ] ``` \ No newline at end of file diff --git a/crates/hir/husky-hir-defn/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.module_hir_defn_deps.md b/crates/hir/husky-hir-defn/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.module_hir_defn_deps.md index e93675dcc4..0c13da06d6 100644 --- a/crates/hir/husky-hir-defn/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.module_hir_defn_deps.md +++ b/crates/hir/husky-hir-defn/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.module_hir_defn_deps.md @@ -5,5 +5,10 @@ value: 1, }, ), + HirDefnDeps( + Id { + value: 2, + }, + ), ] ``` \ No newline at end of file diff --git a/crates/hir/husky-hir-defn/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.module_hir_defn_version_stamps.md b/crates/hir/husky-hir-defn/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.module_hir_defn_version_stamps.md index 9c7e79fd80..e6f372e7b5 100644 --- a/crates/hir/husky-hir-defn/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.module_hir_defn_version_stamps.md +++ b/crates/hir/husky-hir-defn/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.module_hir_defn_version_stamps.md @@ -22,5 +22,27 @@ ), ), ), + ( + MajorItem( + Form( + MajorFormPath( + ItemPathId( + Id { + value: 2, + }, + ), + ), + ), + ), + Some( + Some( + HirDefnVersionStamp( + Id { + value: 2, + }, + ), + ), + ), + ), ] ``` \ No newline at end of file diff --git a/crates/hir/husky-hir-defn/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.module_hir_defns.md b/crates/hir/husky-hir-defn/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.module_hir_defns.md index 5daf9a4e32..5d6bd5d811 100644 --- a/crates/hir/husky-hir-defn/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.module_hir_defns.md +++ b/crates/hir/husky-hir-defn/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.module_hir_defns.md @@ -41,5 +41,51 @@ ), ), ), + HirDefn::MajorItem( + MajorItemHirDefn::Form( + MajorFormHirDefn::StaticVar( + MajorStaticVarHirDefn { + path: MajorFormPath(`latex_ast_hsy::AST`, `StaticVar`), + hir_decl: MajorStaticVarHirDecl { + path: MajorFormPath(`latex_ast_hsy::AST`, `StaticVar`), + return_ty: HirType::PathLeading( + HirTypePathLeading { + ty_path: TypePath(`latex_ast_hsy::LxAstId`, `Extern`), + template_arguments: [], + always_copyable: false, + }, + ), + hir_eager_expr_region: HirEagerExprRegion { + region_path: RegionPath::ItemDecl( + ItemPath(`latex_ast_hsy::AST`), + ), + self_value_ty: None, + expr_arena: Arena { + data: [], + }, + stmt_arena: Arena { + data: [], + }, + pattern_arena: Arena { + data: [], + }, + comptime_variable_region_data: HirEagerComptimeVariableRegionData { + arena: Arena { + data: [], + }, + }, + runtime_variable_region_data: HirEagerRuntimeVariableRegionData { + arena: Arena { + data: [], + }, + self_value_variable: None, + }, + }, + }, + hir_expr_body_and_region: None, + }, + ), + ), + ), ] ``` \ No newline at end of file diff --git a/crates/ide/husky-diagnostics/src/sheet/decl.rs b/crates/ide/husky-diagnostics/src/sheet/decl.rs index 4c212ba50a..6467252ce1 100644 --- a/crates/ide/husky-diagnostics/src/sheet/decl.rs +++ b/crates/ide/husky-diagnostics/src/sheet/decl.rs @@ -80,21 +80,47 @@ impl Diagnose for OriginalSynNodeDeclError { format!("Syntax Error: ExpectEqTokenForVariable",) } OriginalSynNodeDeclError::ExpectedLcurlOrLparOrSemicolonForStruct(_) => { - format!("Syntax Error: expected `{{` `(` or `;` for struct",) - } - OriginalSynNodeDeclError::ExpectedEqForAssocType(_) => todo!(), - OriginalSynNodeDeclError::ExpectedLeftDelimiterInDerive(_) => todo!(), - OriginalSynNodeDeclError::ExpectedRightDelimiterInDerive(_) => todo!(), - OriginalSynNodeDeclError::ExpectedColonBeforeValReturnType(_) => todo!(), - OriginalSynNodeDeclError::ExpectedEqTokenForBackpropArgument(_) => todo!(), - OriginalSynNodeDeclError::ExpectedExprForBackpropArgument(_) => todo!(), - OriginalSynNodeDeclError::ExpectedColonForTraitMemoizedField(_) => todo!(), - OriginalSynNodeDeclError::ExpectedColonBeforeStaticReturnType(_) => todo!(), - OriginalSynNodeDeclError::ExpectedStaticReturnType(_) => todo!(), - OriginalSynNodeDeclError::ExpectedCrateDeclNarrative(_) => todo!(), - OriginalSynNodeDeclError::ExpectedEqTokenForLibCrateDefaultConstExcludes(_) => todo!(), - OriginalSynNodeDeclError::ExpectedEqTokenForTypeAlias(_) => todo!(), - OriginalSynNodeDeclError::ExpectedEqTokenForStaticMut(_) => todo!(), + format!("Syntax Error: expect `{{`, `(`, or `;`") + } + OriginalSynNodeDeclError::ExpectedEqForAssocType(_) => { + format!("Syntax Error: expect `=` for associated type") + } + OriginalSynNodeDeclError::ExpectedLeftDelimiterInDerive(_) => { + format!("Syntax Error: expect `(` in derive") + } + OriginalSynNodeDeclError::ExpectedRightDelimiterInDerive(_) => { + format!("Syntax Error: expect `)` in derive") + } + OriginalSynNodeDeclError::ExpectedColonBeforeValReturnType(_) => { + format!("Syntax Error: expect `:` before return type") + } + OriginalSynNodeDeclError::ExpectedEqTokenForBackpropArgument(_) => { + format!("Syntax Error: expect `=` for backprop argument") + } + OriginalSynNodeDeclError::ExpectedExprForBackpropArgument(_) => { + format!("Syntax Error: expect expression for backprop argument") + } + OriginalSynNodeDeclError::ExpectedColonForTraitMemoizedField(_) => { + format!("Syntax Error: expect `:` for trait memoized field") + } + OriginalSynNodeDeclError::ExpectedColonBeforeStaticReturnType(_) => { + format!("Syntax Error: expect `:` before static return type") + } + OriginalSynNodeDeclError::ExpectedStaticReturnType(_) => { + format!("Syntax Error: expect static return type") + } + OriginalSynNodeDeclError::ExpectedCrateDeclNarrative(_) => { + format!("Syntax Error: expect crate declaration narrative") + } + OriginalSynNodeDeclError::ExpectedEqTokenForLibCrateDefaultConstExcludes(_) => { + format!("Syntax Error: expect `=` for lib crate default const excludes") + } + OriginalSynNodeDeclError::ExpectedEqTokenForTypeAlias(_) => { + format!("Syntax Error: expect `=` for type alias") + } + OriginalSynNodeDeclError::ExpectedEqTokenForStaticMut(_) => { + format!("Syntax Error: expect `=` for static mut") + } } } @@ -130,20 +156,38 @@ impl Diagnose for OriginalSynNodeDeclError { | OriginalSynNodeDeclError::ExpectedEqTokenForMemo(regional_token_stream_state) | OriginalSynNodeDeclError::ExpectedLcurlOrLparOrSemicolonForStruct( regional_token_stream_state, - ) => ctx.token_stream_state_text_range(*regional_token_stream_state), - OriginalSynNodeDeclError::ExpectedEqForAssocType(_) => todo!(), - OriginalSynNodeDeclError::ExpectedLeftDelimiterInDerive(_) => todo!(), - OriginalSynNodeDeclError::ExpectedRightDelimiterInDerive(_) => todo!(), - OriginalSynNodeDeclError::ExpectedColonBeforeValReturnType(_) => todo!(), - OriginalSynNodeDeclError::ExpectedEqTokenForBackpropArgument(_) => todo!(), - OriginalSynNodeDeclError::ExpectedExprForBackpropArgument(_) => todo!(), - OriginalSynNodeDeclError::ExpectedColonForTraitMemoizedField(_) => todo!(), - OriginalSynNodeDeclError::ExpectedColonBeforeStaticReturnType(_) => todo!(), - OriginalSynNodeDeclError::ExpectedStaticReturnType(_) => todo!(), - OriginalSynNodeDeclError::ExpectedCrateDeclNarrative(_) => todo!(), - OriginalSynNodeDeclError::ExpectedEqTokenForLibCrateDefaultConstExcludes(_) => todo!(), - OriginalSynNodeDeclError::ExpectedEqTokenForTypeAlias(_) => todo!(), - OriginalSynNodeDeclError::ExpectedEqTokenForStaticMut(_) => todo!(), + ) + | OriginalSynNodeDeclError::ExpectedEqForAssocType(regional_token_stream_state) + | OriginalSynNodeDeclError::ExpectedLeftDelimiterInDerive( + regional_token_stream_state, + ) + | OriginalSynNodeDeclError::ExpectedRightDelimiterInDerive( + regional_token_stream_state, + ) + | OriginalSynNodeDeclError::ExpectedColonBeforeValReturnType( + regional_token_stream_state, + ) + | OriginalSynNodeDeclError::ExpectedEqTokenForBackpropArgument( + regional_token_stream_state, + ) + | OriginalSynNodeDeclError::ExpectedExprForBackpropArgument( + regional_token_stream_state, + ) + | OriginalSynNodeDeclError::ExpectedColonForTraitMemoizedField( + regional_token_stream_state, + ) + | OriginalSynNodeDeclError::ExpectedColonBeforeStaticReturnType( + regional_token_stream_state, + ) + | OriginalSynNodeDeclError::ExpectedStaticReturnType(regional_token_stream_state) + | OriginalSynNodeDeclError::ExpectedCrateDeclNarrative(regional_token_stream_state) + | OriginalSynNodeDeclError::ExpectedEqTokenForLibCrateDefaultConstExcludes( + regional_token_stream_state, + ) + | OriginalSynNodeDeclError::ExpectedEqTokenForTypeAlias(regional_token_stream_state) + | OriginalSynNodeDeclError::ExpectedEqTokenForStaticMut(regional_token_stream_state) => { + ctx.token_stream_state_text_range(*regional_token_stream_state) + } } } } diff --git a/crates/ide/husky-hover/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.hover_result.md b/crates/ide/husky-hover/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.hover_result.md index caa12d7f1d..0381201ef1 100644 --- a/crates/ide/husky-hover/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.hover_result.md +++ b/crates/ide/husky-hover/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.hover_result.md @@ -570,5 +570,215 @@ }, ), ), + ( + TokenIdx( + 20, + ), + Some( + HoverResult { + hover: Hover { + contents: Markup( + MarkupContent { + kind: Markdown, + value: "Other keyword\n\n\nregional_token_indices = [];\n", + }, + ), + range: Some( + Range { + start: Position { + line: 3, + character: 0, + }, + end: Position { + line: 3, + character: 3, + }, + }, + ), + }, + actions: [], + }, + ), + ), + ( + TokenIdx( + 21, + ), + Some( + HoverResult { + hover: Hover { + contents: Markup( + MarkupContent { + kind: Markdown, + value: "This is a form keyword\n\n\nregional_token_indices = [];\n", + }, + ), + range: Some( + Range { + start: Position { + line: 3, + character: 4, + }, + end: Position { + line: 3, + character: 10, + }, + }, + ), + }, + actions: [], + }, + ), + ), + ( + TokenIdx( + 22, + ), + Some( + HoverResult { + hover: Hover { + contents: Markup( + MarkupContent { + kind: Markdown, + value: "Other keyword\n\n\nregional_token_indices = [];\n", + }, + ), + range: Some( + Range { + start: Position { + line: 3, + character: 11, + }, + end: Position { + line: 3, + character: 14, + }, + }, + ), + }, + actions: [], + }, + ), + ), + ( + TokenIdx( + 23, + ), + Some( + HoverResult { + hover: Hover { + contents: Markup( + MarkupContent { + kind: Markdown, + value: "\n\nentity node\n\nregional_token_indices = [];\n", + }, + ), + range: Some( + Range { + start: Position { + line: 3, + character: 15, + }, + end: Position { + line: 3, + character: 18, + }, + }, + ), + }, + actions: [], + }, + ), + ), + ( + TokenIdx( + 24, + ), + Some( + HoverResult { + hover: Hover { + contents: Markup( + MarkupContent { + kind: Markdown, + value: "\n\n\nregional_token_indices = [];\n", + }, + ), + range: Some( + Range { + start: Position { + line: 3, + character: 18, + }, + end: Position { + line: 3, + character: 19, + }, + }, + ), + }, + actions: [], + }, + ), + ), + ( + TokenIdx( + 25, + ), + Some( + HoverResult { + hover: Hover { + contents: Markup( + MarkupContent { + kind: Markdown, + value: "\n\nentity `latex_ast_hsy::LxAstId`\n\nregional_token_indices = [\n RegionalTokenIdx(\n 6,\n ),\n RegionalTokenIdx(\n 6,\n ),\n];\n\n\ncoercion = None\n\ntype = `Type`", + }, + ), + range: Some( + Range { + start: Position { + line: 3, + character: 20, + }, + end: Position { + line: 3, + character: 27, + }, + }, + ), + }, + actions: [], + }, + ), + ), + ( + TokenIdx( + 26, + ), + Some( + HoverResult { + hover: Hover { + contents: Markup( + MarkupContent { + kind: Markdown, + value: "\n\n\nregional_token_indices = [];\n", + }, + ), + range: Some( + Range { + start: Position { + line: 3, + character: 27, + }, + end: Position { + line: 3, + character: 28, + }, + }, + ), + }, + actions: [], + }, + ), + ), ] ``` \ No newline at end of file diff --git a/crates/ide/husky-semantic-token/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.semantic_tokens.md b/crates/ide/husky-semantic-token/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.semantic_tokens.md index 352030a636..c30ad313e7 100644 --- a/crates/ide/husky-semantic-token/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.semantic_tokens.md +++ b/crates/ide/husky-semantic-token/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.semantic_tokens.md @@ -134,6 +134,55 @@ Ok( token_type: 6, token_modifiers_bitset: 0, }, + SemanticToken { + delta_line: 2, + delta_start: 0, + length: 3, + token_type: 2, + token_modifiers_bitset: 0, + }, + SemanticToken { + delta_line: 0, + delta_start: 4, + length: 6, + token_type: 2, + token_modifiers_bitset: 0, + }, + SemanticToken { + delta_line: 0, + delta_start: 7, + length: 3, + token_type: 2, + token_modifiers_bitset: 0, + }, + SemanticToken { + delta_line: 0, + delta_start: 4, + length: 3, + token_type: 19, + token_modifiers_bitset: 0, + }, + SemanticToken { + delta_line: 0, + delta_start: 3, + length: 1, + token_type: 6, + token_modifiers_bitset: 0, + }, + SemanticToken { + delta_line: 0, + delta_start: 2, + length: 7, + token_type: 8, + token_modifiers_bitset: 0, + }, + SemanticToken { + delta_line: 0, + delta_start: 7, + length: 1, + token_type: 6, + token_modifiers_bitset: 0, + }, ], ) ``` \ No newline at end of file diff --git a/crates/ide/husky-token-info/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.token_infer_sheet.md b/crates/ide/husky-token-info/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.token_infer_sheet.md index ff468e61f6..1d2f540cd4 100644 --- a/crates/ide/husky-token-info/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.token_infer_sheet.md +++ b/crates/ide/husky-token-info/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.token_infer_sheet.md @@ -52,6 +52,76 @@ Ok( }, ], [], + [], + [], + [], + [ + TokenInfo { + regional_token_idx: None, + source: TokenInfoSource::AstIdentifiable, + data: TokenInfoData::EntityNode( + ItemSynNodePath::MajorItem( + MajorItemSynNodePath::Form( + MajorFormSynNodePath(`latex_ast_hsy::AST`, `StaticVar`, (0)), + ), + ), + EntityKind::MajorItem { + module_item_kind: MajorItemKind::Form( + MajorFormKind::StaticVar, + ), + connection: MajorItemConnectionKind::Connected, + }, + ), + }, + ], + [], + [ + TokenInfo { + regional_token_idx: Some( + RegionalTokenIdx( + 6, + ), + ), + source: TokenInfoSource::SemExpr( + RegionPath::ItemDecl( + ItemPath(`latex_ast_hsy::AST`), + ), + SemExprIdx( + 0, + ), + ), + data: TokenInfoData::Entity( + EntityPath::MajorItem( + MajorItemPath::Type( + TypePath(`latex_ast_hsy::LxAstId`, `Extern`), + ), + ), + ), + }, + TokenInfo { + regional_token_idx: Some( + RegionalTokenIdx( + 6, + ), + ), + source: TokenInfoSource::SynPrincipalEntityPathExpr( + 0, + PrincipalEntityPath::MajorItem( + MajorItemPath::Type( + TypePath(`latex_ast_hsy::LxAstId`, `Extern`), + ), + ), + ), + data: TokenInfoData::Entity( + EntityPath::MajorItem( + MajorItemPath::Type( + TypePath(`latex_ast_hsy::LxAstId`, `Extern`), + ), + ), + ), + }, + ], + [], ], }, ) diff --git a/crates/kernel/husky-dec-signature/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.module_dec_templates.md b/crates/kernel/husky-dec-signature/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.module_dec_templates.md index 296587a288..6574517611 100644 --- a/crates/kernel/husky-dec-signature/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.module_dec_templates.md +++ b/crates/kernel/husky-dec-signature/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.module_dec_templates.md @@ -16,5 +16,23 @@ ), ), ), + ( + ItemPath(`latex_ast_hsy::AST`), + Ok( + ItemDecTemplate::MajorItem( + MajorItemDecTemplate::Form( + MajorFormDecTemplate::StaticVar( + MajorStaticVarDecTemplate { + return_ty: DecTerm::ItemPath( + DecItemPath::Type( + TypePath(`latex_ast_hsy::LxAstId`, `Extern`), + ), + ), + }, + ), + ), + ), + ), + ), ] ``` \ No newline at end of file diff --git a/crates/kernel/husky-dec-signature/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.module_dec_var_projs.md b/crates/kernel/husky-dec-signature/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.module_dec_var_projs.md index b545b60e79..034fb894be 100644 --- a/crates/kernel/husky-dec-signature/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.module_dec_var_projs.md +++ b/crates/kernel/husky-dec-signature/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.module_dec_var_projs.md @@ -1,3 +1,12 @@ ```rust -[] +[ + ( + MajorFormPath(`latex_ast_hsy::AST`, `StaticVar`), + Ok( + [ + MajorFormPath(`latex_ast_hsy::AST`, `StaticVar`), + ], + ), + ), +] ``` \ No newline at end of file diff --git a/crates/kernel/husky-eth-signature/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.module_eth_templates.md b/crates/kernel/husky-eth-signature/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.module_eth_templates.md index 75f5d50f25..1677d35fb2 100644 --- a/crates/kernel/husky-eth-signature/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.module_eth_templates.md +++ b/crates/kernel/husky-eth-signature/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.module_eth_templates.md @@ -17,5 +17,21 @@ ), ), ), + ( + ItemPath(`latex_ast_hsy::AST`), + Ok( + ItemEthTemplate::MajorItem( + MajorItemEthTemplate::Form( + FormEthTemplate::StaticVar( + MajorStaticVarEthTemplate { + path: MajorFormPath(`latex_ast_hsy::AST`, `StaticVar`), + return_ty: EthTerm(`LxAstId`), + expr_ty: EthTerm(`Leash LxAstId`), + }, + ), + ), + ), + ), + ), ] ``` \ No newline at end of file diff --git a/crates/latex/latex-ast/Cargo.toml b/crates/latex/latex-ast/Cargo.toml index 2fd1cbaa63..8154acca41 100644 --- a/crates/latex/latex-ast/Cargo.toml +++ b/crates/latex/latex-ast/Cargo.toml @@ -13,6 +13,7 @@ keywords.workspace = true [dependencies] egui = { workspace = true, optional = true } +serde.workspace = true smallvec.workspace = true # abstractions coword.workspace = true diff --git a/crates/latex/latex-ast/src/ast.rs b/crates/latex/latex-ast/src/ast.rs index 0494763fe8..1da9eee70b 100644 --- a/crates/latex/latex-ast/src/ast.rs +++ b/crates/latex/latex-ast/src/ast.rs @@ -41,6 +41,7 @@ use latex_token::{ rose::LxRoseTokenData, }, }; +use serde::{Deserialize, Serialize}; #[enum_class::from_variants] #[derive(Debug, Clone, PartialEq, Eq)] @@ -65,6 +66,15 @@ impl LxAstArena { root: self.root.as_arena_ref(), } } + + pub fn all_asts(&self) -> impl Iterator { + self.math + .indices() + .map(LxAstIdx::Math) + .chain(self.rose.indices().map(LxAstIdx::Rose)) + .chain(self.lisp.indices().map(LxAstIdx::Lisp)) + .chain(self.root.indices().map(LxAstIdx::Root)) + } } #[derive(Debug, PartialEq, Eq, Clone, Copy)] @@ -129,7 +139,7 @@ impl LxAstArenaMap { } #[enum_class::from_variants] -#[derive(Debug, Clone, Copy, PartialEq, Eq)] +#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, Serialize, Deserialize)] pub enum LxAstIdx { Math(LxMathAstIdx), Rose(LxRoseAstIdx), diff --git a/crates/latex/latex-ast/src/ast/root/tests.rs b/crates/latex/latex-ast/src/ast/root/tests.rs index b66ae15d37..aee3212bb3 100644 --- a/crates/latex/latex-ast/src/ast/root/tests.rs +++ b/crates/latex/latex-ast/src/ast/root/tests.rs @@ -11,7 +11,7 @@ fn t(content: &str, expected: Expect) { let dev_paths = HuskyLangDevPaths::new(); let file_path = LxFilePath::new(PathBuf::from(file!())); let tracker = LxAstTracker::new(LxDocumentInput { - specs_dir: dev_paths.specs_dir(), + specs_dir: dev_paths.specs_dir().to_path_buf(), file_path, content, }); diff --git a/crates/latex/latex-ast/src/helpers/tracker.rs b/crates/latex/latex-ast/src/helpers/tracker.rs index 3648dc2f2f..0bae248fc0 100644 --- a/crates/latex/latex-ast/src/helpers/tracker.rs +++ b/crates/latex/latex-ast/src/helpers/tracker.rs @@ -5,7 +5,7 @@ use crate::{ parse_latex_input_into_asts, root::LxRootAstIdxRange, rose::LxRoseAstIdxRange, - LxAstArena, LxAstIdxRange, + LxAstArena, LxAstIdx, LxAstIdxRange, }, helpers::show::display_tree::LxAstDisplayTreeBuilder, parser::LxAstParser, diff --git a/crates/latex/latex-ast/src/range.rs b/crates/latex/latex-ast/src/range.rs index aa0d081bf2..7034689f0e 100644 --- a/crates/latex/latex-ast/src/range.rs +++ b/crates/latex/latex-ast/src/range.rs @@ -51,6 +51,19 @@ impl std::ops::Index for LxAstTokenIdxRangeMap { } } +impl std::ops::Index for LxAstTokenIdxRangeMap { + type Output = LxTokenIdxRange; + + fn index(&self, index: LxAstIdx) -> &Self::Output { + match index { + LxAstIdx::Math(index) => &self.math[index], + LxAstIdx::Rose(index) => &self.rose[index], + LxAstIdx::Lisp(index) => &self.lisp[index], + LxAstIdx::Root(index) => &self.root[index], + } + } +} + impl LxAstTokenIdxRangeMap { pub fn math_asts_token_idx_range(&self, asts: LxMathAstIdxRange) -> LxTokenIdxRange { todo!() diff --git a/crates/latex/latex-prelude/src/helper/tracker.rs b/crates/latex/latex-prelude/src/helper/tracker.rs index a4bcc91ecf..b213396b8a 100644 --- a/crates/latex/latex-prelude/src/helper/tracker.rs +++ b/crates/latex/latex-prelude/src/helper/tracker.rs @@ -2,37 +2,37 @@ use crate::mode::LxMode; use latex_vfs::path::LxFilePath; use std::path::{Path, PathBuf}; -pub trait IsLxInput<'a>: Copy { - fn specs_dir(self) -> &'a Path; - fn latex_complete_commands_path(self) -> PathBuf { +pub trait IsLxInput<'a> { + fn specs_dir(&self) -> &Path; + fn latex_complete_commands_path(&self) -> PathBuf { self.specs_dir().join("latex/complete-commands.lpcsv") } - fn content(self) -> &'a str; - fn root_mode(self) -> LxMode; - fn file_path(self) -> LxFilePath; + fn content(&self) -> &'a str; + fn root_mode(&self) -> LxMode; + fn file_path(&self) -> LxFilePath; } -#[derive(Debug, Clone, Copy, PartialEq, Eq)] +#[derive(Debug, Clone, PartialEq, Eq)] pub struct LxDocumentInput<'a> { - pub specs_dir: &'a Path, + pub specs_dir: PathBuf, pub file_path: LxFilePath, pub content: &'a str, } impl<'a> IsLxInput<'a> for LxDocumentInput<'a> { - fn specs_dir(self) -> &'a Path { - self.specs_dir + fn specs_dir(&self) -> &Path { + &self.specs_dir } - fn file_path(self) -> LxFilePath { + fn file_path(&self) -> LxFilePath { self.file_path } - fn content(self) -> &'a str { + fn content(&self) -> &'a str { self.content } - fn root_mode(self) -> LxMode { + fn root_mode(&self) -> LxMode { LxMode::Root } } @@ -45,19 +45,19 @@ pub struct LxDocumentBodyInput<'a> { } impl<'a> IsLxInput<'a> for LxDocumentBodyInput<'a> { - fn specs_dir(self) -> &'a Path { + fn specs_dir(&self) -> &Path { self.specs_dir } - fn file_path(self) -> LxFilePath { + fn file_path(&self) -> LxFilePath { self.file_path } - fn content(self) -> &'a str { + fn content(&self) -> &'a str { self.content } - fn root_mode(self) -> LxMode { + fn root_mode(&self) -> LxMode { LxMode::Rose } } @@ -70,19 +70,19 @@ pub struct LxPageInput<'a> { } impl<'a> IsLxInput<'a> for LxPageInput<'a> { - fn specs_dir(self) -> &'a Path { + fn specs_dir(&self) -> &Path { self.specs_dir } - fn file_path(self) -> LxFilePath { + fn file_path(&self) -> LxFilePath { self.file_path } - fn content(self) -> &'a str { + fn content(&self) -> &'a str { self.content } - fn root_mode(self) -> LxMode { + fn root_mode(&self) -> LxMode { LxMode::Rose } } @@ -95,19 +95,19 @@ pub struct LxFormulaInput<'a> { } impl<'a> IsLxInput<'a> for LxFormulaInput<'a> { - fn specs_dir(self) -> &'a Path { + fn specs_dir(&self) -> &Path { self.specs_dir } - fn file_path(self) -> LxFilePath { + fn file_path(&self) -> LxFilePath { self.file_path } - fn content(self) -> &'a str { + fn content(&self) -> &'a str { self.content } - fn root_mode(self) -> LxMode { + fn root_mode(&self) -> LxMode { LxMode::Math } } @@ -120,18 +120,19 @@ pub struct LxLispInput<'a> { } impl<'a> IsLxInput<'a> for LxLispInput<'a> { - fn specs_dir(self) -> &'a Path { + fn specs_dir(&self) -> &Path { self.specs_dir } - fn file_path(self) -> LxFilePath { + fn file_path(&self) -> LxFilePath { self.file_path } - fn content(self) -> &'a str { + fn content(&self) -> &'a str { self.content } - fn root_mode(self) -> LxMode { + + fn root_mode(&self) -> LxMode { LxMode::Lisp } } diff --git a/crates/latex/latex-token/src/storage.rs b/crates/latex/latex-token/src/storage.rs index 40d027fc92..95084ef6b8 100644 --- a/crates/latex/latex-token/src/storage.rs +++ b/crates/latex/latex-token/src/storage.rs @@ -127,6 +127,10 @@ impl LxTokenStorage { None => TextOffsetRange::new(0.into(), 0.into()), } } + + pub fn main_ranged_tokens(&self) -> &[LxTokenEntry] { + &self.main_ranged_tokens + } } /// # actions diff --git a/crates/lean/lean-mir-expr/src/builder.rs b/crates/lean/lean-mir-expr/src/constructor.rs similarity index 75% rename from crates/lean/lean-mir-expr/src/builder.rs rename to crates/lean/lean-mir-expr/src/constructor.rs index 0321de7d24..f8c2c841d4 100644 --- a/crates/lean/lean-mir-expr/src/builder.rs +++ b/crates/lean/lean-mir-expr/src/constructor.rs @@ -1,21 +1,25 @@ use crate::{ expr::{LnMirExprArena, LnMirExprData, LnMirExprIdx, LnMirExprIdxRange}, helpers::fmt::{LnMirExprFormatter, LnMirExprFormatterConfig}, - item_defn::{LnItemDefnArena, LnItemDefnData, LnItemDefnIdxRange}, + item_defn::{ + LnItemDefnArena, LnItemDefnComment, LnItemDefnCommentMap, LnItemDefnData, + LnItemDefnIdxRange, LnItemDefnOrderedMap, + }, stmt::{LnMirStmtArena, LnMirStmtData, LnMirStmtIdx, LnMirStmtIdxRange}, tactic::{LnMirTacticArena, LnMirTacticData, LnMirTacticIdx, LnMirTacticIdxRange}, }; use lean_entity_path::namespace::LnNamespace; -pub struct LnMirExprBuilder { +pub struct LnMirExprConstructor { expr_arena: LnMirExprArena, stmt_arena: LnMirStmtArena, tactic_arena: LnMirTacticArena, item_defn_arena: LnItemDefnArena, current_namespace: LnNamespace, + item_defn_comments: LnItemDefnOrderedMap, } -impl LnMirExprBuilder { +impl LnMirExprConstructor { pub fn new() -> Self { Self { expr_arena: Default::default(), @@ -23,23 +27,25 @@ impl LnMirExprBuilder { tactic_arena: Default::default(), item_defn_arena: Default::default(), current_namespace: LnNamespace::new_root(), + item_defn_comments: Default::default(), } } } -impl LnMirExprBuilder { +impl LnMirExprConstructor { pub fn formatter<'a>(&'a self, config: &'a LnMirExprFormatterConfig) -> LnMirExprFormatter<'a> { LnMirExprFormatter::new( self.expr_arena.as_arena_ref(), self.stmt_arena.as_arena_ref(), self.tactic_arena.as_arena_ref(), self.item_defn_arena.as_arena_ref(), + &self.item_defn_comments, config, ) } } -impl LnMirExprBuilder { +impl LnMirExprConstructor { pub fn alloc_expr(&mut self, data: LnMirExprData) -> LnMirExprIdx { self.expr_arena.alloc_one(data) } @@ -73,8 +79,15 @@ impl LnMirExprBuilder { self.tactic_arena.alloc_batch(data) } - pub fn alloc_item_defns(&mut self, item_defns: Vec) -> LnItemDefnIdxRange { - self.item_defn_arena.alloc_batch(item_defns) + pub fn alloc_item_defns( + &mut self, + item_defns: Vec, + comments: impl IntoIterator, + ) -> LnItemDefnIdxRange { + let item_defns = self.item_defn_arena.alloc_batch(item_defns); + self.item_defn_comments + .insert_next_batch(item_defns, comments); + item_defns } pub fn finish( @@ -84,18 +97,20 @@ impl LnMirExprBuilder { LnMirStmtArena, LnMirTacticArena, LnItemDefnArena, + LnItemDefnCommentMap, ) { ( self.expr_arena, self.stmt_arena, self.tactic_arena, self.item_defn_arena, + self.item_defn_comments, ) } } pub trait WithLnNamespace { - fn ln_mir_expr_builder_mut(&mut self) -> &mut LnMirExprBuilder; + fn ln_mir_expr_builder_mut(&mut self) -> &mut LnMirExprConstructor; fn with_ln_namespace( &mut self, diff --git a/crates/lean/lean-mir-expr/src/expr/application.rs b/crates/lean/lean-mir-expr/src/expr/application.rs index 6bc97c336a..23b7bb8a2d 100644 --- a/crates/lean/lean-mir-expr/src/expr/application.rs +++ b/crates/lean/lean-mir-expr/src/expr/application.rs @@ -1,5 +1,5 @@ use super::{LnMirExprData, LnMirExprIdx}; -use crate::builder::LnMirExprBuilder; +use crate::constructor::LnMirExprConstructor; use lazy_static::lazy_static; use lean_entity_path::{ menu::{ln_item_path_menu, LnItemPathMenu}, @@ -69,7 +69,7 @@ pub enum LnMirFuncKey { }, } -impl LnMirExprBuilder { +impl LnMirExprConstructor { pub fn build_func_from_key(&mut self, key: LnMirFuncKey) -> LnMirFunc { match key { LnMirFuncKey::ItemPath(item_path) => { diff --git a/crates/lean/lean-mir-expr/src/helpers/fmt.rs b/crates/lean/lean-mir-expr/src/helpers/fmt.rs index 4bf301cc86..524c8a0303 100644 --- a/crates/lean/lean-mir-expr/src/helpers/fmt.rs +++ b/crates/lean/lean-mir-expr/src/helpers/fmt.rs @@ -1,8 +1,8 @@ use crate::{ expr::{application::LnMirFunc, LnMirExprArenaRef, LnMirExprData, LnMirExprIdx}, item_defn::{ - def::LnMirDefBody, LnItemDefnArenaRef, LnItemDefnData, LnItemDefnIdx, LnItemDefnIdxRange, - LnMirItemDefnGroupMeta, + def::LnMirDefBody, LnItemDefnArenaRef, LnItemDefnComment, LnItemDefnData, LnItemDefnIdx, + LnItemDefnIdxRange, LnItemDefnOrderedMap, LnMirItemDefnGroupMeta, }, stmt::LnMirStmtArenaRef, tactic::{LnMirTacticArenaRef, LnMirTacticData, LnMirTacticIdx, LnMirTacticIdxRange}, @@ -16,6 +16,7 @@ pub struct LnMirExprFormatter<'a> { stmt_arena: LnMirStmtArenaRef<'a>, tactic_arena: LnMirTacticArenaRef<'a>, defn_arena: LnItemDefnArenaRef<'a>, + defn_comments: &'a LnItemDefnOrderedMap, config: &'a LnMirExprFormatterConfig, result: String, indent_level: usize, @@ -41,6 +42,7 @@ impl<'a> LnMirExprFormatter<'a> { stmt_arena: LnMirStmtArenaRef<'a>, tactic_arena: LnMirTacticArenaRef<'a>, defn_arena: LnItemDefnArenaRef<'a>, + defn_comments: &'a LnItemDefnOrderedMap, config: &'a LnMirExprFormatterConfig, ) -> Self { Self { @@ -48,6 +50,7 @@ impl<'a> LnMirExprFormatter<'a> { stmt_arena, tactic_arena, defn_arena, + defn_comments, config, result: Default::default(), indent_level: 0, @@ -205,6 +208,7 @@ impl<'a> LnMirExprFormatter<'a> { pub fn format_defn(&mut self, defn: LnItemDefnIdx) { self.make_sure_new_paragraph(); + self.format_defn_comment(defn); let defn_arena = self.defn_arena; match defn_arena[defn] { LnItemDefnData::Variable { ident: symbol, ty } => { @@ -239,6 +243,21 @@ impl<'a> LnMirExprFormatter<'a> { } } + pub fn format_defn_comment(&mut self, defn: LnItemDefnIdx) { + let comment = &self.defn_comments[defn]; + match *comment { + LnItemDefnComment::Void => {} + LnItemDefnComment::Lines(ref lines) => { + for line in lines { + self.make_sure_new_line(); + self.result += "-- "; + self.result += line; + } + self.make_sure_new_line(); + } + } + } + pub fn format_def_body(&mut self, body: LnMirDefBody) { match body { LnMirDefBody::Expr(expr) => self.format_expr_ext(expr), diff --git a/crates/lean/lean-mir-expr/src/item_defn.rs b/crates/lean/lean-mir-expr/src/item_defn.rs index f10cc9326a..2080667f3a 100644 --- a/crates/lean/lean-mir-expr/src/item_defn.rs +++ b/crates/lean/lean-mir-expr/src/item_defn.rs @@ -5,7 +5,9 @@ pub mod variable; use self::{def::*, variable::*}; use crate::*; use expr::LnMirExprIdx; -use idx_arena::{Arena, ArenaIdx, ArenaIdxRange, ArenaRef}; +use idx_arena::{ + map::ArenaMap, ordered_map::ArenaOrderedMap, Arena, ArenaIdx, ArenaIdxRange, ArenaRef, +}; use lean_coword::ident::LnIdent; use lean_entity_path::namespace::LnNamespace; @@ -53,6 +55,8 @@ pub enum LnMirItemDefnGroupMeta { } pub type LnItemDefnArena = Arena; +pub type LnItemDefnMap = ArenaMap; +pub type LnItemDefnOrderedMap = ArenaOrderedMap; pub type LnItemDefnArenaRef<'a> = ArenaRef<'a, LnItemDefnData>; pub type LnItemDefnIdx = ArenaIdx; pub type LnItemDefnIdxRange = ArenaIdxRange; @@ -67,3 +71,21 @@ impl std::fmt::Display for LnMirItemDefnGroupMeta { } } } + +pub enum LnItemDefnComment { + Void, + Lines(Vec), +} + +pub type LnItemDefnCommentMap = LnItemDefnOrderedMap; + +impl LnItemDefnComment { + pub fn from_latex_source(input: &str) -> Self { + let lines = input + .lines() + .into_iter() + .map(|line| line.to_string()) + .collect(); + Self::Lines(lines) + } +} diff --git a/crates/lean/lean-mir-expr/src/lib.rs b/crates/lean/lean-mir-expr/src/lib.rs index 6f40312b88..2056362ee7 100644 --- a/crates/lean/lean-mir-expr/src/lib.rs +++ b/crates/lean/lean-mir-expr/src/lib.rs @@ -1,5 +1,5 @@ #![feature(let_chains)] -pub mod builder; +pub mod constructor; pub mod expr; pub mod helpers; pub mod item_defn; diff --git a/crates/lex/husky-token/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.token_sheet.md b/crates/lex/husky-token/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.token_sheet.md index 16e00712e4..31de6f5a20 100644 --- a/crates/lex/husky-token/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.token_sheet.md +++ b/crates/lex/husky-token/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.token_sheet.md @@ -88,6 +88,33 @@ TokenSheetData { PunctuationMapped::Semicolon, ), ), + TokenData::Keyword( + Keyword::Pub, + ), + TokenData::Keyword( + Keyword::Form( + Static, + ), + ), + TokenData::Keyword( + Keyword::Var, + ), + TokenData::Ident( + `AST`, + ), + TokenData::Punctuation( + Punctuation( + PunctuationMapped::Colon, + ), + ), + TokenData::Ident( + `LxAstId`, + ), + TokenData::Punctuation( + Punctuation( + PunctuationMapped::Semicolon, + ), + ), ], token_verses: TokenVerses { main_sequence: MainTokenVerseSequence { @@ -108,6 +135,14 @@ TokenSheetData { ), indent: 0, }, + TokenVerseData { + start: TokenVerseStart( + TokenIdx( + 20, + ), + ), + indent: 0, + }, ], }, nested_sequences: [], diff --git a/crates/linket/husky-javelin/expect-files/registry/latex-ast-hsy-0.1.0/package_amazon_javelins.md b/crates/linket/husky-javelin/expect-files/registry/latex-ast-hsy-0.1.0/package_amazon_javelins.md index b545b60e79..ed6945ec71 100644 --- a/crates/linket/husky-javelin/expect-files/registry/latex-ast-hsy-0.1.0/package_amazon_javelins.md +++ b/crates/linket/husky-javelin/expect-files/registry/latex-ast-hsy-0.1.0/package_amazon_javelins.md @@ -1,3 +1,21 @@ ```rust -[] +[ + AmazonJavelin( + Javelin { + data: JavelinData::PathLeading { + path: JavPath::Form( + MajorFormPath(`latex_ast_hsy::AST`, `StaticVar`), + ), + instantiation: JavInstantiation { + path: ItemPath(`latex_ast_hsy::AST`), + context: JavTypeContext { + comptime_var_overrides: [], + }, + variable_resolutions: [], + separator: None, + }, + }, + }, + ), +] ``` \ No newline at end of file diff --git a/crates/linket/husky-javelin/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.item_valkyrie_rides.md b/crates/linket/husky-javelin/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.item_valkyrie_rides.md index c40168e0ee..b78403679c 100644 --- a/crates/linket/husky-javelin/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.item_valkyrie_rides.md +++ b/crates/linket/husky-javelin/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.item_valkyrie_rides.md @@ -13,5 +13,14 @@ }, ), ), + ( + ItemPath(`latex_ast_hsy::AST`), + Some( + ValkyrieRides { + hir_template_parameters: None, + rides: [], + }, + ), + ), ] ``` \ No newline at end of file diff --git a/crates/linket/husky-linket-impl/src/static_var.rs b/crates/linket/husky-linket-impl/src/static_var.rs index 03e6057dfa..a7cf39d5e6 100644 --- a/crates/linket/husky-linket-impl/src/static_var.rs +++ b/crates/linket/husky-linket-impl/src/static_var.rs @@ -1,6 +1,6 @@ use crate::*; use husky_figure_zone_protocol::{ - text::{FigureText, FigureTextKey}, + chunk_base::{text::FigureTextChunkBaseData, FigureChunkBase}, FigureZone, }; use husky_value::IsValue; @@ -76,18 +76,9 @@ pub trait IsStaticVar: 'static { fn zones() -> &'static [FigureZone]; - /// override if necessary - fn text_key(var_id: VarId) -> FigureTextKey { + fn figure_chunk_base(chunk_idx: u32) -> FigureTextChunkBaseData { unreachable!( - "IsStaticVar::text_key() not implemented for `{}`", - std::any::type_name::() - ) - } - - /// override if necessary - fn text(key: FigureTextKey) -> FigureText { - unreachable!( - "IsStaticVar::text() not implemented for `{}`", + "no implement of `figure_chunk_base` for type {}", std::any::type_name::() ) } @@ -113,6 +104,7 @@ pub struct StaticVarSvtable { ) -> StaticVarResult)>, get_value: fn() -> Value, zones: fn() -> &'static [FigureZone], // because rust doesn't support associated static items + figure_chunk_base: fn(chunk_idx: u32) -> FigureTextChunkBaseData, } impl StaticVarSvtable { @@ -136,6 +128,7 @@ impl StaticVarSvtable { default_page_start: V::default_page_start, get_value: V::get_value, zones: V::zones, + figure_chunk_base: V::figure_chunk_base, } } @@ -182,6 +175,10 @@ impl StaticVarSvtable { pub fn zones(&self) -> &'static [FigureZone] { (self.zones)() } + + pub fn figure_chunk_base(&self, chunk_idx: u32) -> FigureTextChunkBaseData { + (self.figure_chunk_base)(chunk_idx) + } } /// this is a mild error, sometimes intentionally triggered diff --git a/crates/linket/husky-linket-impl/src/ugly.rs b/crates/linket/husky-linket-impl/src/ugly.rs index 67adb1e216..774511a962 100644 --- a/crates/linket/husky-linket-impl/src/ugly.rs +++ b/crates/linket/husky-linket-impl/src/ugly.rs @@ -2,5 +2,11 @@ pub use crate::{ exception::ExceptionSource as __ExceptionSource, linket_impl::IsLinketImpl as __IsLinketImpl, pedestal::IsPedestal as __IsPedestal, static_var::IsStaticVar as __IsStaticVar, }; -pub use husky_figure_zone_protocol::FigureZone as __FigureZone; +pub use husky_figure_zone_protocol::{ + chunk_base::{ + text::FigureTextChunkBaseData as __FigureTextChunkBaseData, + FigureChunkBase as __FigureChunkBase, + }, + FigureZone as __FigureZone, +}; pub use smallvec::SmallVec as __SmallVec; diff --git a/crates/linket/husky-linket/expect-files/registry/latex-ast-hsy-0.1.0/package_linkets.md b/crates/linket/husky-linket/expect-files/registry/latex-ast-hsy-0.1.0/package_linkets.md index b545b60e79..76162a0dcb 100644 --- a/crates/linket/husky-linket/expect-files/registry/latex-ast-hsy-0.1.0/package_linkets.md +++ b/crates/linket/husky-linket/expect-files/registry/latex-ast-hsy-0.1.0/package_linkets.md @@ -1,3 +1,17 @@ ```rust -[] +[ + Linket { + data: LinketData::MajorStaticVar { + path: MajorFormPath(`latex_ast_hsy::AST`, `StaticVar`), + instantiation: LinInstantiation { + path: ItemPath(`latex_ast_hsy::AST`), + context: LinTypeContext { + comptime_var_overrides: [], + }, + variable_resolutions: [], + separator: None, + }, + }, + }, +] ``` \ No newline at end of file diff --git a/crates/linket/husky-standard-linket-impl/src/enum.rs b/crates/linket/husky-standard-linket-impl/src/enum.rs index e0368b0dbe..29ff2cba9f 100644 --- a/crates/linket/husky-standard-linket-impl/src/enum.rs +++ b/crates/linket/husky-standard-linket-impl/src/enum.rs @@ -121,7 +121,7 @@ macro_rules! enum_variant_discriminator_linket_impl { Value::Owned(owner) => { matches!(owner.downcast_into_owned::<$self_ty>(), $variant_path) } - Value::Leash(owner) => { + Value::LeashSized(owner) => { matches!( (owner as &'static dyn std::any::Any) .downcast_ref::<$self_ty>() @@ -145,7 +145,7 @@ macro_rules! enum_variant_discriminator_linket_impl { $variant_path { .. } ) } - Value::Leash(owner) => { + Value::LeashSized(owner) => { matches!( (owner as &'static dyn std::any::Any) .downcast_ref::<$self_ty>() @@ -166,7 +166,7 @@ macro_rules! enum_variant_discriminator_linket_impl { Value::Owned(owner) => { matches!(owner.downcast_into_owned::<$self_ty>(), $variant_path(..)) } - Value::Leash(owner) => { + Value::LeashSized(owner) => { matches!( (owner as &'static dyn std::any::Any) .downcast_ref::<$self_ty>() @@ -225,7 +225,7 @@ macro_rules! enum_variant_field_linket_impl { }; $field.into_value() } - Value::Leash(owner) => { + Value::LeashSized(owner) => { let $variant_path { $field, .. } = (owner as &'static dyn std::any::Any) .downcast_ref::<$self_ty>() .unwrap() @@ -250,7 +250,7 @@ macro_rules! enum_variant_field_linket_impl { }; v0.into_value() } - Value::Leash(owner) => { + Value::LeashSized(owner) => { let $variant_path(v0, ..) = (owner as &'static dyn std::any::Any) .downcast_ref::<$self_ty>() .unwrap() @@ -275,7 +275,7 @@ macro_rules! enum_variant_field_linket_impl { }; v1.into_value() } - Value::Leash(owner) => { + Value::LeashSized(owner) => { let $variant_path(_, v1, ..) = (owner as &'static dyn std::any::Any) .downcast_ref::<$self_ty>() .unwrap() @@ -301,7 +301,7 @@ macro_rules! enum_variant_field_linket_impl { }; v1.into_value() } - Value::Leash(owner) => { + Value::LeashSized(owner) => { let $variant_path(_, _, v2, ..) = (owner as &'static dyn std::any::Any) .downcast_ref::<$self_ty>() .unwrap() diff --git a/crates/linket/husky-standard-linket-impl/src/struct.rs b/crates/linket/husky-standard-linket-impl/src/struct.rs index 07afbb5879..d697b5623b 100644 --- a/crates/linket/husky-standard-linket-impl/src/struct.rs +++ b/crates/linket/husky-standard-linket-impl/src/struct.rs @@ -33,7 +33,7 @@ macro_rules! struct_field_linket_impl { fn struct_field_wrapper(owner: Value) -> Value { match owner { Value::Owned(owner) => owner.downcast_into_owned::<$self_ty>().$field.into_value(), - Value::Leash(owner) => class_specific_leashed_field_into_value!( + Value::LeashSized(owner) => class_specific_leashed_field_into_value!( $class & (owner as &'static dyn std::any::Any) .downcast_ref::<$self_ty>() diff --git a/crates/mayuri/mayuri-genetic-algorithms/src/basic/lab.rs b/crates/mayuri/mayuri-genetic-algorithms/src/basic/lab.rs index 2b7c5ed8bc..7c178cb876 100644 --- a/crates/mayuri/mayuri-genetic-algorithms/src/basic/lab.rs +++ b/crates/mayuri/mayuri-genetic-algorithms/src/basic/lab.rs @@ -46,11 +46,6 @@ impl Lab { self.population .sort_unstable_by(|a, b| b.fitness.cmp(&a.fitness)); - println!( - "Generation {}: Best fitness = {}, Genes = {:?}", - generation, self.population[0].fitness, self.population[0].genes - ); - let new_individuals: Vec = (0..self.population_size) .map(|_| { let parent1 = &self.population[self.rng.gen_range(0..self.population.len())]; diff --git a/crates/protocols/husky-figure-zone-protocol/Cargo.toml b/crates/protocols/husky-figure-zone-protocol/Cargo.toml index 7bd6275a97..26a4f055c2 100644 --- a/crates/protocols/husky-figure-zone-protocol/Cargo.toml +++ b/crates/protocols/husky-figure-zone-protocol/Cargo.toml @@ -14,6 +14,7 @@ keywords.workspace = true [dependencies] serde.workspace = true # abstractions +enum-class.workspace = true shifted-unsigned-int.workspace = true [lints] diff --git a/crates/protocols/husky-figure-zone-protocol/src/chunk_base.rs b/crates/protocols/husky-figure-zone-protocol/src/chunk_base.rs new file mode 100644 index 0000000000..bd69cefe73 --- /dev/null +++ b/crates/protocols/husky-figure-zone-protocol/src/chunk_base.rs @@ -0,0 +1,12 @@ +pub mod text; + +use serde::{Deserialize, Deserializer, Serialize, Serializer}; +use shifted_unsigned_int::ShiftedU32; +use text::FigureTextChunkBaseId; + +// TODO: maybe move this to other crates +#[enum_class::from_variants] +#[derive(Debug, PartialEq, Eq, Clone, Copy, Serialize, Deserialize)] +pub enum FigureChunkBase { + Text(FigureTextChunkBaseId), +} diff --git a/crates/protocols/husky-figure-zone-protocol/src/chunk_base/text.rs b/crates/protocols/husky-figure-zone-protocol/src/chunk_base/text.rs new file mode 100644 index 0000000000..02416f8003 --- /dev/null +++ b/crates/protocols/husky-figure-zone-protocol/src/chunk_base/text.rs @@ -0,0 +1,49 @@ +use super::*; + +#[derive(Debug, PartialEq, Eq, Clone, Serialize, Deserialize)] +pub struct FigureTextChunkBaseData { + pub text: String, +} + +#[derive(Debug, PartialEq, Eq, PartialOrd, Ord, Clone, Copy, Hash)] +pub struct FigureTextChunkBaseId(ShiftedU32); + +impl Serialize for FigureTextChunkBaseId { + fn serialize(&self, serializer: S) -> Result + where + S: Serializer, + { + serializer.serialize_u32(self.0.into()) + } +} + +impl<'de> Deserialize<'de> for FigureTextChunkBaseId { + fn deserialize(deserializer: D) -> Result + where + D: Deserializer<'de>, + { + let value = usize::deserialize(deserializer)?; + Ok(FigureTextChunkBaseId(ShiftedU32::new(value as u32))) + } +} + +#[derive(Default, Debug, Clone, PartialEq, Eq, Serialize, Deserialize)] +pub struct FigureTextChunkBaseArena { + data: Vec, +} + +impl FigureTextChunkBaseArena { + pub fn alloc(&mut self, text: FigureTextChunkBaseData) -> FigureTextChunkBaseId { + let id = FigureTextChunkBaseId(ShiftedU32::new(self.data.len() as u32)); + self.data.push(text); + id + } +} + +impl std::ops::Index for FigureTextChunkBaseArena { + type Output = FigureTextChunkBaseData; + + fn index(&self, index: FigureTextChunkBaseId) -> &Self::Output { + &self.data[index.0.index()] + } +} diff --git a/crates/protocols/husky-figure-zone-protocol/src/lib.rs b/crates/protocols/husky-figure-zone-protocol/src/lib.rs index 439ddd6810..bc6996d889 100644 --- a/crates/protocols/husky-figure-zone-protocol/src/lib.rs +++ b/crates/protocols/husky-figure-zone-protocol/src/lib.rs @@ -1,18 +1,18 @@ -pub mod text; +pub mod chunk_base; use serde::{Deserialize, Serialize}; #[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize, Hash)] pub enum FigureZone { - Gallery = 1, - Text, + Parade = 1, + Roll, } impl FigureZone { pub fn len(self) -> usize { match self { - FigureZone::Gallery => 1, - FigureZone::Text => 1, + FigureZone::Parade => 1, + FigureZone::Roll => 1, } } } diff --git a/crates/protocols/husky-figure-zone-protocol/src/text.rs b/crates/protocols/husky-figure-zone-protocol/src/text.rs deleted file mode 100644 index 1875ffef7f..0000000000 --- a/crates/protocols/husky-figure-zone-protocol/src/text.rs +++ /dev/null @@ -1,47 +0,0 @@ -use super::*; -use serde::{Deserialize, Deserializer, Serialize, Serializer}; -use shifted_unsigned_int::ShiftedU32; - -#[derive(Debug, PartialEq, Eq, Clone, Serialize, Deserialize)] -pub enum FigureTextKey { - Unit, - VarId(VarId), -} - -#[derive(Debug, PartialEq, Eq, Clone, Serialize, Deserialize)] -pub enum FigureText {} - -#[derive(Debug, PartialEq, Eq, PartialOrd, Ord, Clone, Copy, Hash)] -pub struct FigureTextId(ShiftedU32); - -impl Serialize for FigureTextId { - fn serialize(&self, serializer: S) -> Result - where - S: Serializer, - { - serializer.serialize_u32(self.0.into()) - } -} - -impl<'de> Deserialize<'de> for FigureTextId { - fn deserialize(deserializer: D) -> Result - where - D: Deserializer<'de>, - { - let value = usize::deserialize(deserializer)?; - Ok(FigureTextId(ShiftedU32::new(value as u32))) - } -} - -#[derive(Default)] -pub struct FigureTextArena { - data: Vec, -} - -impl FigureTextArena { - pub fn alloc(&mut self, text: FigureText) -> FigureTextId { - let id = FigureTextId(ShiftedU32::new(self.data.len() as u32)); - self.data.push(text); - id - } -} diff --git a/crates/protocols/husky-standard-trace-protocol/Cargo.toml b/crates/protocols/husky-standard-trace-protocol/Cargo.toml index d4d9684ad8..3156f6c530 100644 --- a/crates/protocols/husky-standard-trace-protocol/Cargo.toml +++ b/crates/protocols/husky-standard-trace-protocol/Cargo.toml @@ -13,6 +13,7 @@ keywords.workspace = true [dependencies] egui = { workspace = true, optional = true } +itertools.workspace = true rustc-hash.workspace = true serde.workspace = true # abstractions diff --git a/crates/protocols/husky-standard-trace-protocol/src/figure.rs b/crates/protocols/husky-standard-trace-protocol/src/figure.rs index 692f3a01ae..9bb613b278 100644 --- a/crates/protocols/husky-standard-trace-protocol/src/figure.rs +++ b/crates/protocols/husky-standard-trace-protocol/src/figure.rs @@ -1,13 +1,16 @@ pub mod dim2; -mod gallery; +mod parading; +pub mod rolling; mod specific; -pub mod text; -use self::{gallery::GalleryFigure, specific::SpecificFigure}; +use self::{parading::ParadingFigure, specific::SpecificFigure}; use crate::chart::{StandardChart, StandardChartDim0, StandardChartDim1}; #[cfg(feature = "egui")] use egui::{pos2, Color32, Rect, Ui, Vec2}; -use husky_figure_zone_protocol::FigureZone; +use husky_figure_zone_protocol::{ + chunk_base::{text::FigureTextChunkBaseId, FigureChunkBase}, + FigureZone, +}; use husky_ki_repr_interface::KiReprInterface; use husky_linket_impl::pedestal::{IsPedestal, IsPedestalFull, JointPedestal}; use husky_standard_linket_impl::pedestal::{StandardJointPedestal, StandardPedestal}; @@ -30,8 +33,8 @@ use husky_visual_protocol::{ Visual, }, }; +use rolling::RollingFigure; use serde::{Deserialize, Serialize}; -use text::TextFigure; use ui::visual::cache::VisualUiCache; #[enum_class::from_variants] @@ -39,8 +42,8 @@ use ui::visual::cache::VisualUiCache; pub enum StandardFigure { Void, Specific(SpecificFigure), - Dim1(GalleryFigure), - Text(TextFigure), + Marching(ParadingFigure), + Rolling(RollingFigure), } /// # impl IsFigure @@ -51,8 +54,8 @@ impl IsFigure for StandardFigure { match self { StandardFigure::Void => (), StandardFigure::Specific(slf) => slf.for_all_joint_pedestals(f), - StandardFigure::Dim1(slf) => slf.for_all_joint_pedestals(f), - StandardFigure::Text(slf) => slf.for_all_joint_pedestals(f), + StandardFigure::Marching(slf) => slf.for_all_joint_pedestals(f), + StandardFigure::Rolling(slf) => slf.for_all_joint_pedestals(f), } } @@ -68,20 +71,21 @@ impl IsFigure for StandardFigure { SpecificFigure::from_chart(chart, trace_plot_map, visual_synchrotron).into() } - fn new_gallery( + fn new_parading( chart: StandardChartDim1>, trace_plot_map: &TracePlotInfos, visual_synchrotron: &VisualSynchrotron, ) -> StandardFigure { - GalleryFigure::from_chart(chart, trace_plot_map, visual_synchrotron).into() + ParadingFigure::from_chart(chart, trace_plot_map, visual_synchrotron).into() } - fn new_text( + fn new_rolling( chart: Option>>, trace_plot_map: &TracePlotInfos, - visual_synchrotron: &VisualSynchrotron, + visual_synchrotron: &mut VisualSynchrotron, + f: impl Fn(u32, &mut VisualSynchrotron) -> FigureChunkBase, ) -> StandardFigure { - todo!() + RollingFigure::from_chart(chart, trace_plot_map, visual_synchrotron, f).into() } } @@ -96,8 +100,8 @@ impl FigureUi for StandardFigure { match self { StandardFigure::Void => (), StandardFigure::Specific(slf) => slf.figure_ui(visual_synchrotron, cache, ui), - StandardFigure::Dim1(slf) => slf.figure_ui(visual_synchrotron, cache, ui), - StandardFigure::Text(text_figure) => todo!(), + StandardFigure::Marching(slf) => slf.figure_ui(visual_synchrotron, cache, ui), + StandardFigure::Rolling(slf) => slf.figure_ui(visual_synchrotron, cache, ui), } } } diff --git a/crates/protocols/husky-standard-trace-protocol/src/figure/gallery.rs b/crates/protocols/husky-standard-trace-protocol/src/figure/parading.rs similarity index 94% rename from crates/protocols/husky-standard-trace-protocol/src/figure/gallery.rs rename to crates/protocols/husky-standard-trace-protocol/src/figure/parading.rs index ba96079383..f85a2d42df 100644 --- a/crates/protocols/husky-standard-trace-protocol/src/figure/gallery.rs +++ b/crates/protocols/husky-standard-trace-protocol/src/figure/parading.rs @@ -6,12 +6,12 @@ use husky_standard_linket_impl::pedestal::StandardJointPedestal; use ui::visual::cache::VisualUiCache; #[derive(Debug, PartialEq, Eq, Clone, Serialize, Deserialize)] -pub struct GalleryFigure { +pub struct ParadingFigure { specific_figures: Vec, } /// # constructor -impl GalleryFigure { +impl ParadingFigure { pub(super) fn from_chart( chart: StandardChartDim1>, trace_plot_map: &TracePlotInfos, @@ -19,8 +19,9 @@ impl GalleryFigure { ) -> Self { Self { specific_figures: chart + .points .into_iter() - .map(|chart_dim0| { + .map(|(var_id, chart_dim0)| { SpecificFigure::from_chart(chart_dim0, trace_plot_map, visual_synchrotron) }) .collect(), @@ -28,7 +29,7 @@ impl GalleryFigure { } } -impl GalleryFigure { +impl ParadingFigure { pub(super) fn for_all_joint_pedestals(&self, mut f: impl FnMut(&StandardJointPedestal)) { self.specific_figures .iter() @@ -38,7 +39,7 @@ impl GalleryFigure { /// # ui #[cfg(feature = "egui")] -impl GalleryFigure { +impl ParadingFigure { pub(super) fn figure_ui( &self, visual_synchrotron: &VisualSynchrotron, diff --git a/crates/protocols/husky-standard-trace-protocol/src/figure/rolling.rs b/crates/protocols/husky-standard-trace-protocol/src/figure/rolling.rs new file mode 100644 index 0000000000..5961ec141a --- /dev/null +++ b/crates/protocols/husky-standard-trace-protocol/src/figure/rolling.rs @@ -0,0 +1,95 @@ +use super::*; +use husky_figure_zone_protocol::chunk_base::{ + text::{FigureTextChunkBaseData, FigureTextChunkBaseId}, + FigureChunkBase, +}; + +#[derive(Debug, PartialEq, Eq, Clone, Serialize, Deserialize)] +pub struct RollingFigure { + chunks: Vec, +} + +#[derive(Debug, PartialEq, Eq, Clone, Serialize, Deserialize)] +pub struct RollingFigureChunk { + base: FigureChunkBase, + specific_figures: Vec, +} + +impl RollingFigure { + pub(super) fn from_chart( + chart: Option>>, + trace_plot_map: &TracePlotInfos, + visual_synchrotron: &mut VisualSynchrotron, + f: impl Fn(u32, &mut VisualSynchrotron) -> FigureChunkBase, + ) -> Self { + use itertools::Itertools; + + let Some(chart) = chart else { + return Self { chunks: vec![] }; + }; + let mut chunks = chart + .points + .into_iter() + .group_by(|(var_id, _)| { + let StandardVarId::Pair([chunk_id, _]) = *var_id else { + unreachable!() + }; + chunk_id + }) + .into_iter() + .map(|(chunk_id, group)| { + // TODO: other kinds of chunks + let base = f(chunk_id, visual_synchrotron); + RollingFigureChunk { + base, + specific_figures: group + .map(|(var_id, chart_dim0)| { + SpecificFigure::from_chart( + chart_dim0, + trace_plot_map, + visual_synchrotron, + ) + }) + .collect(), + } + }) + .collect(); + Self { chunks } + } +} + +impl RollingFigure { + pub(super) fn for_all_joint_pedestals(&self, mut f: impl FnMut(&StandardJointPedestal)) { + self.chunks + .iter() + .for_each(|chunk| chunk.for_all_joint_pedestals(&mut f)) + } +} + +impl RollingFigureChunk { + pub(super) fn for_all_joint_pedestals(&self, mut f: impl FnMut(&StandardJointPedestal)) { + self.specific_figures + .iter() + .for_each(|figure| figure.for_all_joint_pedestals(&mut f)) + } +} + +impl RollingFigure { + pub(crate) fn figure_ui( + &self, + visual_synchrotron: &VisualSynchrotron, + cache: &mut VisualUiCache, + ui: &mut Ui, + ) { + for chunk in self.chunks.iter() { + // TODO: wrap in a scrollable area or something + match chunk.base { + FigureChunkBase::Text(figure_text_chunk_base_id) => { + let data = &visual_synchrotron[figure_text_chunk_base_id]; + ui.label(&data.text); + } + _ => unreachable!(), + } + } + } +} diff --git a/crates/protocols/husky-standard-trace-protocol/src/figure/specific.rs b/crates/protocols/husky-standard-trace-protocol/src/figure/specific.rs index 474b9148dd..f88b0f959e 100644 --- a/crates/protocols/husky-standard-trace-protocol/src/figure/specific.rs +++ b/crates/protocols/husky-standard-trace-protocol/src/figure/specific.rs @@ -32,7 +32,10 @@ pub enum StandardPlot { /// # constructor impl SpecificFigure { pub(super) fn from_chart( - (joint_pedestal, composite_visual): StandardChartDim0>, + StandardChartDim0 { + joint_pedestal, + r: composite_visual, + }: StandardChartDim0>, trace_plot_map: &TracePlotInfos, visual_synchrotron: &VisualSynchrotron, ) -> Self { diff --git a/crates/protocols/husky-standard-trace-protocol/src/figure/text.rs b/crates/protocols/husky-standard-trace-protocol/src/figure/text.rs deleted file mode 100644 index db290787df..0000000000 --- a/crates/protocols/husky-standard-trace-protocol/src/figure/text.rs +++ /dev/null @@ -1,17 +0,0 @@ -use super::*; -use husky_figure_zone_protocol::text::{FigureText, FigureTextId}; - -#[derive(Debug, PartialEq, Eq, Clone, Serialize, Deserialize)] -pub struct TextFigure { - text: FigureTextId, - specific_figures: Vec, -} - -impl TextFigure { - pub(super) fn for_all_joint_pedestals(&self, mut f: impl FnMut(&StandardJointPedestal)) { - // TODO ad hoc - self.specific_figures - .iter() - .for_each(|figure| figure.for_all_joint_pedestals(&mut f)) - } -} diff --git a/crates/protocols/husky-trace-protocol/src/chart.rs b/crates/protocols/husky-trace-protocol/src/chart.rs index 01ae0348d6..aece976e11 100644 --- a/crates/protocols/husky-trace-protocol/src/chart.rs +++ b/crates/protocols/husky-trace-protocol/src/chart.rs @@ -11,6 +11,27 @@ pub enum Chart { Dim2(ChartDim2), } -pub type ChartDim0 = (JointPedestal, R); -pub type ChartDim1 = Vec<(JointPedestal, R)>; -pub type ChartDim2 = Vec, R)>>; +#[derive(Debug, PartialEq, Eq)] +pub struct ChartDim0 +where + VarId: IsVarId, +{ + pub joint_pedestal: JointPedestal, + pub r: R, +} + +#[derive(Debug, PartialEq, Eq)] +pub struct ChartDim1 +where + VarId: IsVarId, +{ + pub points: Vec<(VarId, ChartDim0)>, +} + +#[derive(Debug, PartialEq, Eq)] +pub struct ChartDim2 +where + VarId: IsVarId, +{ + pub rows: Vec<(VarId, ChartDim1)>, +} diff --git a/crates/protocols/husky-trace-protocol/src/figure.rs b/crates/protocols/husky-trace-protocol/src/figure.rs index b4a93228dc..2e21302a1e 100644 --- a/crates/protocols/husky-trace-protocol/src/figure.rs +++ b/crates/protocols/husky-trace-protocol/src/figure.rs @@ -7,7 +7,10 @@ use crate::{ windlass::Windlass, IsTraceProtocol, TraceId, TraceSynchrotron, }; -use husky_figure_zone_protocol::FigureZone; +use husky_figure_zone_protocol::{ + chunk_base::{text::FigureTextChunkBaseId, FigureChunkBase}, + FigureZone, +}; use husky_item_path_interface::ItemPathIdInterface; use husky_ki_repr_interface::KiReprInterface; use husky_linket_impl::{ @@ -43,15 +46,16 @@ pub trait IsFigure: trace_plot_map: &TracePlotInfos, visual_synchrotron: &VisualSynchrotron, ) -> Self; - fn new_gallery( + fn new_parading( chart: ChartDim1, CompositeVisual>, trace_plot_map: &TracePlotInfos, visual_synchrotron: &VisualSynchrotron, ) -> Self; - fn new_text( + fn new_rolling( chart: Option, CompositeVisual>>, trace_plot_map: &TracePlotInfos, - visual_synchrotron: &VisualSynchrotron, + visual_synchrotron: &mut VisualSynchrotron, + f: impl Fn(u32, &mut VisualSynchrotron) -> FigureChunkBase, ) -> Self; fn for_all_joint_pedestals( @@ -228,6 +232,13 @@ impl FigureKey { &self.joint_static_var_anchors } + pub fn generic_joint_static_vars(&self) -> impl Iterator + '_ { + self.joint_static_var_anchors + .iter() + .filter(|(_, anchor)| anchor.is_generic()) + .map(|(id, _)| *id) + } + pub fn figure_zone(&self) -> Option { self.figure_zone } diff --git a/crates/protocols/husky-visual-protocol/Cargo.toml b/crates/protocols/husky-visual-protocol/Cargo.toml index 78c4e9e507..ceef947d58 100644 --- a/crates/protocols/husky-visual-protocol/Cargo.toml +++ b/crates/protocols/husky-visual-protocol/Cargo.toml @@ -11,6 +11,8 @@ ordered-float.workspace = true # abstractions enum-class.workspace = true shifted-unsigned-int.workspace = true +# protocols +husky-figure-zone-protocol.workspace = true # utils husky-print-utils.workspace = true diff --git a/crates/protocols/husky-visual-protocol/src/synchrotron.rs b/crates/protocols/husky-visual-protocol/src/synchrotron.rs index 6327fe5767..b958ab349c 100644 --- a/crates/protocols/husky-visual-protocol/src/synchrotron.rs +++ b/crates/protocols/husky-visual-protocol/src/synchrotron.rs @@ -2,11 +2,16 @@ pub mod action; use self::action::{VisualSynchrotronAction, VisualSynchrotronActionOutcome}; use crate::visual::{VisualArena, VisualData, VisualId}; +use husky_figure_zone_protocol::chunk_base::{ + text::{FigureTextChunkBaseArena, FigureTextChunkBaseData, FigureTextChunkBaseId}, + FigureChunkBase, +}; use serde::{Deserialize, Serialize}; #[derive(Default, Debug, Clone, PartialEq, Eq, Serialize, Deserialize)] pub struct VisualSynchrotron { visual_arena: VisualArena, + figure_text_arena: FigureTextChunkBaseArena, actions: Vec, } @@ -15,10 +20,37 @@ impl VisualSynchrotron { &self.visual_arena } + pub fn figure_text_arena(&self) -> &FigureTextChunkBaseArena { + &self.figure_text_arena + } +} + +impl VisualSynchrotron { /// stores the data in the arena and returns a visual id pub(crate) fn alloc_visual(&mut self, data: impl Into) -> VisualId { match self.take_action(VisualSynchrotronAction::AllocVisual { data: data.into() }) { VisualSynchrotronActionOutcome::AllocVisual { visual_id } => visual_id, + _ => unreachable!(), } } + + pub fn alloc_figure_text_chunk_base( + &mut self, + text: impl Into, + ) -> FigureChunkBase { + match self.take_action(VisualSynchrotronAction::AllocFigureText { text: text.into() }) { + VisualSynchrotronActionOutcome::AllocFigureText { figure_text_id } => { + FigureChunkBase::Text(figure_text_id) + } + _ => unreachable!(), + } + } +} + +impl std::ops::Index for VisualSynchrotron { + type Output = FigureTextChunkBaseData; + + fn index(&self, index: FigureTextChunkBaseId) -> &Self::Output { + &self.figure_text_arena[index] + } } diff --git a/crates/protocols/husky-visual-protocol/src/synchrotron/action.rs b/crates/protocols/husky-visual-protocol/src/synchrotron/action.rs index 017af29683..0d09333cfc 100644 --- a/crates/protocols/husky-visual-protocol/src/synchrotron/action.rs +++ b/crates/protocols/husky-visual-protocol/src/synchrotron/action.rs @@ -3,10 +3,16 @@ use super::*; #[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)] pub enum VisualSynchrotronAction { AllocVisual { data: VisualData }, + AllocFigureText { text: FigureTextChunkBaseData }, } pub(super) enum VisualSynchrotronActionOutcome { - AllocVisual { visual_id: VisualId }, + AllocVisual { + visual_id: VisualId, + }, + AllocFigureText { + figure_text_id: FigureTextChunkBaseId, + }, } #[derive(Default, Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)] @@ -31,6 +37,11 @@ impl VisualSynchrotron { visual_id: self.visual_arena.alloc(data), } } + VisualSynchrotronAction::AllocFigureText { text } => { + VisualSynchrotronActionOutcome::AllocFigureText { + figure_text_id: self.figure_text_arena.alloc(text), + } + } } } diff --git a/crates/runtime/husky-dev-runtime/src/var.rs b/crates/runtime/husky-dev-runtime/src/var.rs index 0c3d93374e..857a1ced12 100644 --- a/crates/runtime/husky-dev-runtime/src/var.rs +++ b/crates/runtime/husky-dev-runtime/src/var.rs @@ -206,7 +206,7 @@ impl DevRuntime { let &[(path, anchor, ref locked), ref remaining_vars @ ..] = remaining_vars else { let joint_pedestal = JointPedestal::new(var_map); let r = f(&joint_pedestal)?; - return Some((joint_pedestal, r)); + return Some(ChartDim0 { joint_pedestal, r }); }; let db = self.db(); let ItemPath::MajorItem(MajorItemPath::Form(major_form_path)) = path else { @@ -270,16 +270,21 @@ impl DevRuntime { .filter_map(|var_id| { let mut var_map = var_map.clone(); var_map.insert(((*path).into(), var_id)); - linket_impl - .with_var_id(var_id, locked, || { - self.with_var_anchors0(var_map, remaining_vars, &mut f) - }) - .ok() - .flatten() + Some(( + var_id, + linket_impl + .with_var_id(var_id, locked, || { + self.with_var_anchors0(var_map, remaining_vars, &mut f) + }) + .ok() + .flatten()?, + )) }); - Some(match page_limit { - Some(page_limit) => iter.take(page_limit).collect(), - None => iter.collect(), + Some(ChartDim1 { + points: match page_limit { + Some(page_limit) => iter.take(page_limit).collect(), + None => iter.collect(), + }, }) } } diff --git a/crates/semantics/husky-sem-expr/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.decl_sem_expr_range_regions.md b/crates/semantics/husky-sem-expr/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.decl_sem_expr_range_regions.md index 396c759cb3..b133e64df1 100644 --- a/crates/semantics/husky-sem-expr/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.decl_sem_expr_range_regions.md +++ b/crates/semantics/husky-sem-expr/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.decl_sem_expr_range_regions.md @@ -10,5 +10,41 @@ ), }, }, + SemExprRangeRegion { + data: SemExprRangeRegionData { + principal_entity_path_expr_ranges: [ + RegionalTokenIdxRange { + start: RegionalTokenIdxRangeStart( + RegionalTokenIdx( + 6, + ), + ), + end: RegionalTokenIdxRangeEnd( + RegionalTokenIdx( + 7, + ), + ), + }, + ], + pattern_ranges: [], + expr_ranges: [ + RegionalTokenIdxRange { + start: RegionalTokenIdxRangeStart( + RegionalTokenIdx( + 6, + ), + ), + end: RegionalTokenIdxRangeEnd( + RegionalTokenIdx( + 7, + ), + ), + }, + ], + stmt_ranges: SemStmtMap( + [], + ), + }, + }, ] ``` \ No newline at end of file diff --git a/crates/semantics/husky-sem-expr/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.decl_sem_expr_regions.md b/crates/semantics/husky-sem-expr/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.decl_sem_expr_regions.md index 6dc2df2f91..8dc501a6fd 100644 --- a/crates/semantics/husky-sem-expr/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.decl_sem_expr_regions.md +++ b/crates/semantics/husky-sem-expr/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.decl_sem_expr_regions.md @@ -62,5 +62,155 @@ }, }, }, + SemExprRegion { + path: RegionPath::ItemDecl( + ItemPath(`latex_ast_hsy::AST`), + ), + data: SemExprRegionData { + path: RegionPath::ItemDecl( + ItemPath(`latex_ast_hsy::AST`), + ), + place_registry: PlaceRegistry { + infos: [], + }, + sem_expr_arena: SemExprArena( + Arena { + data: [ + SemExprEntry { + data_result: Ok( + SemExprData::PrincipalEntityPath { + path_expr_idx: 0, + path: PrincipalEntityPath::MajorItem( + MajorItemPath::Type( + TypePath(`latex_ast_hsy::LxAstId`, `Extern`), + ), + ), + ty_path_disambiguation: OntologyConstructor, + instantiation: None, + }, + ), + ty_result: Ok( + FlyTerm { + quary: None, + base: FlyTermBase::Eth( + EthTerm(`Type`), + ), + }, + ), + expectation_idx_and_ty: Some( + ( + 0, + FlyTerm { + quary: None, + base: FlyTermBase::Eth( + EthTerm(`Type`), + ), + }, + ), + ), + }, + ], + }, + ), + sem_stmt_arena: SemStmtArena( + Arena { + data: [], + }, + ), + sem_expr_roots: [ + ( + 0, + ( + SemExprIdx( + 0, + ), + SynExprRootKind::ReturnType, + ), + ), + ], + syn_pattern_ty_infos: [], + syn_pattern_variable_ty_infos: ArenaMap { + data: [], + }, + sem_expr_terms: [ + ( + SemExprIdx( + 0, + ), + Ok( + FlyTerm { + quary: None, + base: FlyTermBase::Eth( + EthTerm(`LxAstId`), + ), + }, + ), + ), + ], + symbol_tys: SymbolMap { + inherited_variable_map: [], + current_variable_map: [], + }, + symbol_terms: SymbolMap { + inherited_variable_map: [], + current_variable_map: [], + }, + fly_term_region: FlyTermRegion { + terms: FlyTerms { + sol_terms: SolTerms { + entries: [], + }, + hol_terms: HolTerms { + entries: [], + first_unresolved_term_idx: 0, + }, + }, + expectations: Expectations { + arena: Arena { + data: [ + FlyTermExpectationEntry { + expectation: Expectation::EqsSort( + ExpectSort { + smallest_universe: Universe( + 1, + ), + }, + ), + state: ExpectationState { + idx: 0, + src: ExpectationSource { + syn_expr_idx: 0, + kind: Expr, + }, + expectee: FlyTerm { + quary: None, + base: FlyTermBase::Eth( + EthTerm(`Type`), + ), + }, + resolve_progress: ExpectationProgress::Resolved( + Ok( + ExpectationOutcome::EqsSort( + Universe( + 1, + ), + ), + ), + ), + }, + }, + ], + }, + first_unresolved_expectation: 0, + }, + }, + return_ty: None, + self_ty: None, + self_value_ty: None, + context_itd: EthTermContextItd { + task_ty: None, + }, + }, + }, ] ``` \ No newline at end of file diff --git a/crates/semantics/husky-sem-expr/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.sem_expr_aggregator.md b/crates/semantics/husky-sem-expr/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.sem_expr_aggregator.md index e93cb4df14..2962788d01 100644 --- a/crates/semantics/husky-sem-expr/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.sem_expr_aggregator.md +++ b/crates/semantics/husky-sem-expr/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.sem_expr_aggregator.md @@ -9,3 +9,15 @@ None ```rust None ``` + +## `AST` decl + +```rust +None +``` + +## `AST` defn + +```rust +None +``` diff --git a/crates/semantics/husky-sem-expr/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.visit_sem_expr.md b/crates/semantics/husky-sem-expr/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.visit_sem_expr.md index c284a625cc..f97e81fc4d 100644 --- a/crates/semantics/husky-sem-expr/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.visit_sem_expr.md +++ b/crates/semantics/husky-sem-expr/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.visit_sem_expr.md @@ -11,3 +11,19 @@ Some( ```rust None ``` + +## `AST` decl + +```rust +Some( + [ + "LxAstId", + ], +) +``` + +## `AST` defn + +```rust +None +``` diff --git a/crates/semantics/husky-sem-item-path-deps/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.item_sem_item_path_cycle_group_itd.md b/crates/semantics/husky-sem-item-path-deps/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.item_sem_item_path_cycle_group_itd.md index c0a9d2177c..304b2858f8 100644 --- a/crates/semantics/husky-sem-item-path-deps/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.item_sem_item_path_cycle_group_itd.md +++ b/crates/semantics/husky-sem-item-path-deps/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.item_sem_item_path_cycle_group_itd.md @@ -9,3 +9,15 @@ SemItemPathDepsCyclceGroupItd { }, } ``` + +## `AST` + +```rust +SemItemPathDepsCyclceGroupItd { + cycle_group: CycleGroup { + nodes: [ + ItemPath(`latex_ast_hsy::AST`), + ], + }, +} +``` diff --git a/crates/semantics/husky-sem-item-path-deps/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.item_sem_item_path_deps.md b/crates/semantics/husky-sem-item-path-deps/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.item_sem_item_path_deps.md index dc14f627e3..fe7f2758d6 100644 --- a/crates/semantics/husky-sem-item-path-deps/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.item_sem_item_path_deps.md +++ b/crates/semantics/husky-sem-item-path-deps/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.item_sem_item_path_deps.md @@ -7,3 +7,15 @@ Some( ), ) ``` + +## `AST` + +```rust +Some( + Ok( + [ + ItemPath(`latex_ast_hsy::LxAstId`), + ], + ), +) +``` diff --git a/crates/semantics/husky-sem-item-path-deps/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.item_sem_item_path_deps_cropped.md b/crates/semantics/husky-sem-item-path-deps/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.item_sem_item_path_deps_cropped.md index dc14f627e3..fe7f2758d6 100644 --- a/crates/semantics/husky-sem-item-path-deps/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.item_sem_item_path_deps_cropped.md +++ b/crates/semantics/husky-sem-item-path-deps/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.item_sem_item_path_deps_cropped.md @@ -7,3 +7,15 @@ Some( ), ) ``` + +## `AST` + +```rust +Some( + Ok( + [ + ItemPath(`latex_ast_hsy::LxAstId`), + ], + ), +) +``` diff --git a/crates/semantics/husky-sem-item-path-deps/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.item_sem_item_path_full_deps_cropped.md b/crates/semantics/husky-sem-item-path-deps/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.item_sem_item_path_full_deps_cropped.md index 57b79073a2..3086f8c4e0 100644 --- a/crates/semantics/husky-sem-item-path-deps/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.item_sem_item_path_full_deps_cropped.md +++ b/crates/semantics/husky-sem-item-path-deps/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.item_sem_item_path_full_deps_cropped.md @@ -5,3 +5,12 @@ ItemPath(`latex_ast_hsy::LxAstId`), ] ``` + +## `AST` + +```rust +[ + ItemPath(`latex_ast_hsy::AST`), + ItemPath(`latex_ast_hsy::LxAstId`), +] +``` diff --git a/crates/semantics/husky-sem-place-contract/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.decl_sem_place_contract_regions.md b/crates/semantics/husky-sem-place-contract/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.decl_sem_place_contract_regions.md index d9fab3652b..f493f2e0e0 100644 --- a/crates/semantics/husky-sem-place-contract/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.decl_sem_place_contract_regions.md +++ b/crates/semantics/husky-sem-place-contract/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.decl_sem_place_contract_regions.md @@ -7,5 +7,14 @@ }, ), }, + SemPlaceContractRegion { + expr_sites: SemExprMap( + ArenaMap { + data: [ + None, + ], + }, + ), + }, ] ``` \ No newline at end of file diff --git a/crates/semantics/husky-sem-static-mut-deps/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.item_sem_static_mut_deps.md b/crates/semantics/husky-sem-static-mut-deps/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.item_sem_static_mut_deps.md index 19af7ab87d..dc8a2f4042 100644 --- a/crates/semantics/husky-sem-static-mut-deps/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.item_sem_static_mut_deps.md +++ b/crates/semantics/husky-sem-static-mut-deps/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.item_sem_static_mut_deps.md @@ -5,3 +5,11 @@ SemValueStaticMutDeps( [], ) ``` + +## `AST` + +```rust +SemValueStaticMutDeps( + [], +) +``` diff --git a/crates/semantics/husky-sem-var-deps/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.item_history_sem_var_deps.md b/crates/semantics/husky-sem-var-deps/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.item_history_sem_var_deps.md index 4a105c52d2..c73b89f9de 100644 --- a/crates/semantics/husky-sem-var-deps/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.item_history_sem_var_deps.md +++ b/crates/semantics/husky-sem-var-deps/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.item_history_sem_var_deps.md @@ -3,3 +3,9 @@ ```rust None ``` + +## `AST` + +```rust +None +``` diff --git a/crates/semantics/husky-sem-var-deps/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.item_sem_var_deps.md b/crates/semantics/husky-sem-var-deps/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.item_sem_var_deps.md index f149bd4072..e1cd114896 100644 --- a/crates/semantics/husky-sem-var-deps/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.item_sem_var_deps.md +++ b/crates/semantics/husky-sem-var-deps/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.item_sem_var_deps.md @@ -5,3 +5,15 @@ SemValueVarDeps( [], ) ``` + +## `AST` + +```rust +SemValueVarDeps( + [ + SemVarDep::Item( + ItemPath(`latex_ast_hsy::AST`), + ), + ], +) +``` diff --git a/crates/syntax/husky-ast/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.ast_range_sheet.md b/crates/syntax/husky-ast/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.ast_range_sheet.md index 2fdd4c996b..007bfcde6f 100644 --- a/crates/syntax/husky-ast/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.ast_range_sheet.md +++ b/crates/syntax/husky-ast/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.ast_range_sheet.md @@ -3,6 +3,7 @@ AstTokenIdxRangeSheet { ast_token_idx_ranges: [ 0..15, 15..19, + 19..26, ], } ``` \ No newline at end of file diff --git a/crates/syntax/husky-ast/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.ast_sheet.md b/crates/syntax/husky-ast/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.ast_sheet.md index c9e10177a7..6a46bd9ecb 100644 --- a/crates/syntax/husky-ast/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.ast_sheet.md +++ b/crates/syntax/husky-ast/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.ast_sheet.md @@ -47,15 +47,57 @@ AstSheet { variants: None, }, }, + AstData::Identifiable { + token_verse_idx: TokenVerseIdx { + lcurl: None, + raw: 2, + }, + visibility_expr: VisibilityExpr { + data: VisibilityExprData::Pub { + pub_token: PubToken { + token_idx: TokenIdx( + 20, + ), + }, + }, + visibility: Scope::Pub, + }, + item_kind: EntityKind::MajorItem { + module_item_kind: MajorItemKind::Form( + MajorFormKind::StaticVar, + ), + connection: MajorItemConnectionKind::Connected, + }, + ident_token: IdentToken { + ident: `AST`, + token_idx: TokenIdx( + 23, + ), + }, + is_generic: false, + saved_stream_state: TokenStreamState { + next_token_idx: TokenIdx( + 24, + ), + drained: false, + }, + block: DefnBlock::Form { + path: MajorFormPath(`latex_ast_hsy::AST`, `StaticVar`), + body: None, + }, + }, ], }, top_level_asts: ArenaIdxRange( - 0..2, + 0..3, ), nested_top_level_asts: [], siblings: [ ArenaIdxRange( - 0..2, + 0..0, + ), + ArenaIdxRange( + 0..3, ), ], } diff --git a/crates/syntax/husky-entity-tree/expect-files/registry/latex-ast-hsy-0.1.0/crate_item_paths/src/lib.md b/crates/syntax/husky-entity-tree/expect-files/registry/latex-ast-hsy-0.1.0/crate_item_paths/src/lib.md index d9e181b835..bafdb35b8c 100644 --- a/crates/syntax/husky-entity-tree/expect-files/registry/latex-ast-hsy-0.1.0/crate_item_paths/src/lib.md +++ b/crates/syntax/husky-entity-tree/expect-files/registry/latex-ast-hsy-0.1.0/crate_item_paths/src/lib.md @@ -1,5 +1,6 @@ ```rust [ ItemPath(`latex_ast_hsy::LxAstId`), + ItemPath(`latex_ast_hsy::AST`), ] ``` \ No newline at end of file diff --git a/crates/syntax/husky-entity-tree/expect-files/registry/latex-ast-hsy-0.1.0/item_tree_bundle/src/lib.md b/crates/syntax/husky-entity-tree/expect-files/registry/latex-ast-hsy-0.1.0/item_tree_bundle/src/lib.md index 5eda54e779..c0c41fdc08 100644 --- a/crates/syntax/husky-entity-tree/expect-files/registry/latex-ast-hsy-0.1.0/item_tree_bundle/src/lib.md +++ b/crates/syntax/husky-entity-tree/expect-files/registry/latex-ast-hsy-0.1.0/item_tree_bundle/src/lib.md @@ -59,6 +59,34 @@ EntityTreeCrateBundle { ident: `LxAstId`, visibility: Scope::Pub, }, + ItemNodeEntry { + node: ItemSynNode::MajorItem( + MajorItemSynNode { + syn_node_path: MajorItemSynNodePath::Form( + MajorFormSynNodePath(`latex_ast_hsy::AST`, `StaticVar`, (0)), + ), + visibility: Scope::Pub, + ast_idx: 2, + ident_token: IdentToken { + ident: `AST`, + token_idx: TokenIdx( + 23, + ), + }, + block: DefnBlock::Form { + path: MajorFormPath(`latex_ast_hsy::AST`, `StaticVar`), + body: None, + }, + }, + ), + syn_node_path: ItemSynNodePath::MajorItem( + MajorItemSynNodePath::Form( + MajorFormSynNodePath(`latex_ast_hsy::AST`, `StaticVar`, (0)), + ), + ), + ident: `AST`, + visibility: Scope::Pub, + }, ], }, item_symbol_table: EntitySymbolTable( @@ -72,6 +100,15 @@ EntityTreeCrateBundle { ), }, }, + EntitySymbolEntry { + ident: `AST`, + visible_scope: Scope::Pub, + symbol: EntitySymbol::MajorItem { + major_item_path: MajorItemPath::Form( + MajorFormPath(`latex_ast_hsy::AST`, `StaticVar`), + ), + }, + }, ], ), impl_block_syn_node_table: [], diff --git a/crates/syntax/husky-entity-tree/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.item_tree_presheet.md b/crates/syntax/husky-entity-tree/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.item_tree_presheet.md index be85209c12..0d43f9190c 100644 --- a/crates/syntax/husky-entity-tree/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.item_tree_presheet.md +++ b/crates/syntax/husky-entity-tree/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.item_tree_presheet.md @@ -57,6 +57,34 @@ EntityTreePresheet { ident: `LxAstId`, visibility: Scope::Pub, }, + ItemNodeEntry { + node: ItemSynNode::MajorItem( + MajorItemSynNode { + syn_node_path: MajorItemSynNodePath::Form( + MajorFormSynNodePath(`latex_ast_hsy::AST`, `StaticVar`, (0)), + ), + visibility: Scope::Pub, + ast_idx: 2, + ident_token: IdentToken { + ident: `AST`, + token_idx: TokenIdx( + 23, + ), + }, + block: DefnBlock::Form { + path: MajorFormPath(`latex_ast_hsy::AST`, `StaticVar`), + body: None, + }, + }, + ), + syn_node_path: ItemSynNodePath::MajorItem( + MajorItemSynNodePath::Form( + MajorFormSynNodePath(`latex_ast_hsy::AST`, `StaticVar`, (0)), + ), + ), + ident: `AST`, + visibility: Scope::Pub, + }, ], }, once_use_rules: OnceUseRules( diff --git a/crates/syntax/husky-entity-tree/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.item_tree_sheet.md b/crates/syntax/husky-entity-tree/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.item_tree_sheet.md index 8c520f0c0a..ab6022adb7 100644 --- a/crates/syntax/husky-entity-tree/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.item_tree_sheet.md +++ b/crates/syntax/husky-entity-tree/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.item_tree_sheet.md @@ -57,6 +57,34 @@ EntityTreeSheet { ident: `LxAstId`, visibility: Scope::Pub, }, + ItemNodeEntry { + node: ItemSynNode::MajorItem( + MajorItemSynNode { + syn_node_path: MajorItemSynNodePath::Form( + MajorFormSynNodePath(`latex_ast_hsy::AST`, `StaticVar`, (0)), + ), + visibility: Scope::Pub, + ast_idx: 2, + ident_token: IdentToken { + ident: `AST`, + token_idx: TokenIdx( + 23, + ), + }, + block: DefnBlock::Form { + path: MajorFormPath(`latex_ast_hsy::AST`, `StaticVar`), + body: None, + }, + }, + ), + syn_node_path: ItemSynNodePath::MajorItem( + MajorItemSynNodePath::Form( + MajorFormSynNodePath(`latex_ast_hsy::AST`, `StaticVar`, (0)), + ), + ), + ident: `AST`, + visibility: Scope::Pub, + }, ], }, item_symbol_table: EntitySymbolTable( @@ -70,6 +98,15 @@ EntityTreeSheet { ), }, }, + EntitySymbolEntry { + ident: `AST`, + visible_scope: Scope::Pub, + symbol: EntitySymbol::MajorItem { + major_item_path: MajorItemPath::Form( + MajorFormPath(`latex_ast_hsy::AST`, `StaticVar`), + ), + }, + }, ], ), impl_block_syn_node_table: [], diff --git a/crates/syntax/husky-entity-tree/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.module_item_paths.md b/crates/syntax/husky-entity-tree/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.module_item_paths.md index d9e181b835..bafdb35b8c 100644 --- a/crates/syntax/husky-entity-tree/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.module_item_paths.md +++ b/crates/syntax/husky-entity-tree/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.module_item_paths.md @@ -1,5 +1,6 @@ ```rust [ ItemPath(`latex_ast_hsy::LxAstId`), + ItemPath(`latex_ast_hsy::AST`), ] ``` \ No newline at end of file diff --git a/crates/syntax/husky-syn-decl/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.syn_decl_sheet.md b/crates/syntax/husky-syn-decl/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.syn_decl_sheet.md index 487ec44bc9..ee8ffe3811 100644 --- a/crates/syntax/husky-syn-decl/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.syn_decl_sheet.md +++ b/crates/syntax/husky-syn-decl/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.syn_decl_sheet.md @@ -77,6 +77,104 @@ SynDeclSheet { ), ), ), + ( + ItemPath(`latex_ast_hsy::AST`), + SynDecl::MajorItem( + MajorItemSynDecl::Form( + FormSynDecl::StaticVar( + MajorStaticVarSynDecl { + path: MajorFormPath(`latex_ast_hsy::AST`, `StaticVar`), + return_ty: ReturnTypeBeforeEqSyndicate { + expr: 0, + }, + expr: None, + syn_expr_region: SynExprRegion { + data: SynExprRegionData { + parent: None, + path: SynNodeRegionPath::ItemDecl( + ItemSynNodePath::MajorItem( + MajorItemSynNodePath::Form( + MajorFormSynNodePath(`latex_ast_hsy::AST`, `StaticVar`, (0)), + ), + ), + ), + expr_arena: Arena { + data: [ + SynExprData::PrincipalEntityPath { + path_expr_idx: 0, + opt_path: Some( + PrincipalEntityPath::MajorItem( + MajorItemPath::Type( + TypePath(`latex_ast_hsy::LxAstId`, `Extern`), + ), + ), + ), + }, + ], + }, + principal_item_path_expr_arena: Arena { + data: [ + SynPrincipalEntityPathExpr::Root { + path_name_token: PathNameRegionalToken::Ident( + IdentRegionalToken { + ident: `LxAstId`, + regional_token_idx: RegionalTokenIdx( + 6, + ), + }, + ), + principal_entity_path: PrincipalEntityPath::MajorItem( + MajorItemPath::Type( + TypePath(`latex_ast_hsy::LxAstId`, `Extern`), + ), + ), + }, + ], + }, + stmt_arena: Arena { + data: [], + }, + pattern_region: SynPatternRegion { + pattern_arena: Arena { + data: [], + }, + pattern_contracts: [], + pattern_variable_arena: Arena { + data: [], + }, + pattern_variable_maps: [], + pattern_variable_modifiers: ArenaMap { + data: [], + }, + }, + variable_region: VariableRegionData { + inherited_variable_arena: Arena { + data: [], + }, + current_variable_arena: Arena { + data: [], + }, + allow_self_type: False, + allow_self_value: False, + pattern_ty_constraints: [], + }, + pattern_roots: [], + expr_roots: [ + SynExprRoot { + kind: SynExprRootKind::ReturnType, + syn_expr_idx: 0, + }, + ], + has_self_lifetime: false, + has_self_place: false, + pattern_to_current_variable_map: [], + }, + }, + }, + ), + ), + ), + ), ], } ``` \ No newline at end of file diff --git a/crates/syntax/husky-syn-decl/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.syn_node_decl_sheet.md b/crates/syntax/husky-syn-decl/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.syn_node_decl_sheet.md index bbc0eb8bbf..68d0864394 100644 --- a/crates/syntax/husky-syn-decl/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.syn_node_decl_sheet.md +++ b/crates/syntax/husky-syn-decl/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.syn_node_decl_sheet.md @@ -109,6 +109,120 @@ SynNodeDeclSheet { ), ), ), + ( + ItemSynNodePath::MajorItem( + MajorItemSynNodePath::Form( + MajorFormSynNodePath(`latex_ast_hsy::AST`, `StaticVar`, (0)), + ), + ), + ItemSynNodeDecl::MajorItem( + MajorItemSynNodeDecl::Form( + FormSynNodeDecl::StaticVar( + MajorStaticVarSynNodeDecl { + syn_node_path: MajorFormSynNodePath(`latex_ast_hsy::AST`, `StaticVar`, (0)), + colon_token: Ok( + ColonRegionalToken( + RegionalTokenIdx( + 5, + ), + ), + ), + return_ty: Ok( + ReturnTypeBeforeEqSyndicate { + expr: 0, + }, + ), + opt_eq_token: Ok( + None, + ), + expr: None, + syn_expr_region: SynExprRegion { + data: SynExprRegionData { + parent: None, + path: SynNodeRegionPath::ItemDecl( + ItemSynNodePath::MajorItem( + MajorItemSynNodePath::Form( + MajorFormSynNodePath(`latex_ast_hsy::AST`, `StaticVar`, (0)), + ), + ), + ), + expr_arena: Arena { + data: [ + SynExprData::PrincipalEntityPath { + path_expr_idx: 0, + opt_path: Some( + PrincipalEntityPath::MajorItem( + MajorItemPath::Type( + TypePath(`latex_ast_hsy::LxAstId`, `Extern`), + ), + ), + ), + }, + ], + }, + principal_item_path_expr_arena: Arena { + data: [ + SynPrincipalEntityPathExpr::Root { + path_name_token: PathNameRegionalToken::Ident( + IdentRegionalToken { + ident: `LxAstId`, + regional_token_idx: RegionalTokenIdx( + 6, + ), + }, + ), + principal_entity_path: PrincipalEntityPath::MajorItem( + MajorItemPath::Type( + TypePath(`latex_ast_hsy::LxAstId`, `Extern`), + ), + ), + }, + ], + }, + stmt_arena: Arena { + data: [], + }, + pattern_region: SynPatternRegion { + pattern_arena: Arena { + data: [], + }, + pattern_contracts: [], + pattern_variable_arena: Arena { + data: [], + }, + pattern_variable_maps: [], + pattern_variable_modifiers: ArenaMap { + data: [], + }, + }, + variable_region: VariableRegionData { + inherited_variable_arena: Arena { + data: [], + }, + current_variable_arena: Arena { + data: [], + }, + allow_self_type: False, + allow_self_value: False, + pattern_ty_constraints: [], + }, + pattern_roots: [], + expr_roots: [ + SynExprRoot { + kind: SynExprRootKind::ReturnType, + syn_expr_idx: 0, + }, + ], + has_self_lifetime: false, + has_self_place: false, + pattern_to_current_variable_map: [], + }, + }, + }, + ), + ), + ), + ), ], } ``` \ No newline at end of file diff --git a/crates/syntax/husky-syn-decl/src/error.rs b/crates/syntax/husky-syn-decl/src/error.rs index 6f5f790497..338d5f3abe 100644 --- a/crates/syntax/husky-syn-decl/src/error.rs +++ b/crates/syntax/husky-syn-decl/src/error.rs @@ -118,9 +118,7 @@ pub enum SynDeclError { pub type SynDeclResult = Result; impl From<&SynNodeDeclError> for SynDeclError { - #[track_caller] - fn from(_value: &SynNodeDeclError) -> Self { - todo!(); + fn from(error: &SynNodeDeclError) -> Self { SynDeclError::NodeDecl } } diff --git a/crates/syntax/husky-syn-defn/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.module_item_syn_defns.md b/crates/syntax/husky-syn-defn/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.module_item_syn_defns.md index 48b31b8344..53e66d391f 100644 --- a/crates/syntax/husky-syn-defn/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.module_item_syn_defns.md +++ b/crates/syntax/husky-syn-defn/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.module_item_syn_defns.md @@ -4,5 +4,9 @@ ItemPath(`latex_ast_hsy::LxAstId`), None, ), + ( + ItemPath(`latex_ast_hsy::AST`), + None, + ), ] ``` \ No newline at end of file diff --git a/crates/syntax/husky-syn-defn/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.module_item_syn_node_defns.md b/crates/syntax/husky-syn-defn/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.module_item_syn_node_defns.md index 1496abe72f..7e7e612ac1 100644 --- a/crates/syntax/husky-syn-defn/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.module_item_syn_node_defns.md +++ b/crates/syntax/husky-syn-defn/expect-files/registry/latex-ast-hsy-0.1.0/src/lib.module_item_syn_node_defns.md @@ -21,5 +21,13 @@ ), None, ), + ( + ItemSynNodePath::MajorItem( + MajorItemSynNodePath::Form( + MajorFormSynNodePath(`latex_ast_hsy::AST`, `StaticVar`, (0)), + ), + ), + None, + ), ] ``` \ No newline at end of file diff --git a/crates/utils/husky-jar-utils/expect-files/husky_lang_packages.txt b/crates/utils/husky-jar-utils/expect-files/husky_lang_packages.txt index bb4e4f09d4..94eeae5436 100644 --- a/crates/utils/husky-jar-utils/expect-files/husky_lang_packages.txt +++ b/crates/utils/husky-jar-utils/expect-files/husky_lang_packages.txt @@ -4507,6 +4507,7 @@ "husky-tree-utils", "interned", "latex-prelude", + "latex-token", "lean-coword", "lean-entity-path", "lean-mir-expr", @@ -4520,6 +4521,7 @@ "visored-mir-expr", "visored-opr", "visored-prelude", + "visored-sem-expr", "visored-signature", "visored-term", "expect-test", @@ -4548,6 +4550,7 @@ "latex-environment", "latex-math-letter", "latex-prelude", + "latex-token", "latex-vfs", "lazy_static", "salsa", @@ -4679,7 +4682,16 @@ name: "latex-ast-hsy", relative_path: "registry/latex-ast-hsy-0.1.0", dependencies: [ + "husky-core", + "husky-linket-impl", + "husky-path-utils", + "husky-standard-linket-impl", + "idx-arena", "latex-ast", + "latex-prelude", + "latex-vfs", + "lazy_static", + "vec-like", ], }, PackageSummary { diff --git a/crates/value/husky-standard-value/src/thawed.rs b/crates/value/husky-standard-value/src/thawed.rs index 34b0e1b6e0..9dc538c64f 100644 --- a/crates/value/husky-standard-value/src/thawed.rs +++ b/crates/value/husky-standard-value/src/thawed.rs @@ -1212,10 +1212,11 @@ impl From for ThawedValue { Value::F64(f) => ThawedValue::F64(f.into()), Value::StringLiteral(id) => ThawedValue::StringLiteral(id), Value::Owned(owned_value) => todo!(), - Value::Leash(leashed_value) => ThawedValue::Leash(leashed_value), + Value::LeashSized(leashed_value) => ThawedValue::Leash(leashed_value), Value::OptionBox(immortal_dyn) => todo!(), Value::OptionLeash(_) => todo!(), Value::EnumUnit { index, presenter } => ThawedValue::EnumUnit { index, presenter }, + Value::Copyable(_, _) => todo!(), } } } diff --git a/crates/value/husky-standard-value/src/value.rs b/crates/value/husky-standard-value/src/value.rs index ea5939ea88..d01348cf85 100644 --- a/crates/value/husky-standard-value/src/value.rs +++ b/crates/value/husky-standard-value/src/value.rs @@ -1,3 +1,4 @@ +pub mod copyable; mod option; pub mod owned; mod primitive; @@ -13,6 +14,7 @@ use crate::{ thawed::{Thawed, ThawedDyn}, *, }; +use copyable::CopyableConverter; use frozen::{Frozen, FrozenDyn, FrozenValue}; use husky_decl_macro_utils::*; #[cfg(feature = "constant")] @@ -35,7 +37,6 @@ use thawed::{FromThawedValue, ThawedValue}; pub(crate) const REGULAR_VALUE_SIZE_OVER_I64: usize = 4; -/// we use this layout instead of struct to reduce size to `2 * std::mem::size_of::()` #[value_ty] #[derive(Debug)] #[repr(u8)] @@ -68,13 +69,33 @@ pub enum Value { Owned(OwnedValue), // ad hoc /// `~T` - Leash(&'static dyn ImmortalDyn), + LeashSized(&'static dyn ImmortalDyn), OptionBox(Option>), OptionLeash(Option<&'static dyn ImmortalDyn>), EnumUnit { index: usize, presenter: EnumUnitValuePresenter, }, + Copyable(CopyableConverter, u128), +} + +impl Value { + pub fn new_copyable(t: T) -> Self + where + T: Copy + Immortal + Into + Eq, + for<'a> &'a T: From<&'a u128>, + { + let (converter, v) = CopyableConverter::new(t); + Value::Copyable(converter, v) + } +} + +#[test] +fn value_size_works() { + assert_eq!( + std::mem::size_of::(), + 4 * std::mem::size_of::() + ) } impl Eq for Value {} @@ -194,7 +215,7 @@ impl Value { match self { Value::Owned(slf) => slf.downcast_into_owned(), // ad hoc - Value::Leash(slf) => slf.try_copy_dyn().unwrap().into_owned(), + Value::LeashSized(slf) => slf.try_copy_dyn().unwrap().into_owned(), // *(slf.try_copy_dyn() as Box) // .downcast() // .unwrap(), @@ -206,13 +227,13 @@ impl Value { where T: ImmortalDyn, { - Value::Leash(t) + Value::LeashSized(t) } pub fn into_leash(self) -> &'static T { match self { // ad hoc, we maybe encounter &'static Leash here, so can't always just unwrap it - Value::Leash(slf) => (slf as &dyn std::any::Any).downcast_ref().unwrap(), + Value::LeashSized(slf) => (slf as &dyn std::any::Any).downcast_ref().unwrap(), _ => unreachable!(), } } @@ -259,7 +280,7 @@ impl Value { .push(SlushValue::Box(slf.into_inner())); t } - Value::Leash(slf) => { + Value::LeashSized(slf) => { let slf: &T = ((slf as &dyn ImmortalDyn) as &dyn std::any::Any) .downcast_ref() .expect("type id is correct"); @@ -268,6 +289,7 @@ impl Value { Value::OptionBox(_) => todo!(), Value::OptionLeash(_) => todo!(), Value::EnumUnit { .. } => todo!(), + Value::Copyable(_, _) => todo!(), } } } @@ -329,11 +351,12 @@ impl IsValue for Value { Value::F32(slf) => Value::F32(slf), Value::F64(slf) => Value::F64(slf), Value::StringLiteral(slf) => Value::StringLiteral(slf), - Value::Owned(ref slf) => Value::Leash(slf.as_ref()), // Clone the boxed value - Value::Leash(slf) => Value::Leash(slf), + Value::Owned(ref slf) => Value::LeashSized(slf.as_ref()), // Clone the boxed value + Value::LeashSized(slf) => Value::LeashSized(slf), Value::OptionBox(ref slf) => Value::OptionLeash(slf.as_ref().map(|v| &**v)), // Clone the boxed option Value::OptionLeash(slf) => Value::OptionLeash(slf), Value::EnumUnit { index, presenter } => Value::EnumUnit { index, presenter }, + Value::Copyable(_, _) => todo!(), } } @@ -367,7 +390,7 @@ impl IsValue for Value { match self { Value::OptionBox(opt) => opt.is_none(), Value::OptionLeash(opt) => opt.is_none(), - Value::Leash(opt) => opt.is_none_dyn(), + Value::LeashSized(opt) => opt.is_none_dyn(), _ => { unreachable!() } @@ -378,7 +401,7 @@ impl IsValue for Value { match self { Value::OptionBox(opt) => opt.is_some(), Value::OptionLeash(opt) => opt.is_some(), - Value::Leash(opt) => opt.is_some_dyn(), + Value::LeashSized(opt) => opt.is_some_dyn(), _ => unreachable!(), } } @@ -435,10 +458,11 @@ impl IsValue for Value { Value::F64(_) => todo!(), Value::StringLiteral(_) => todo!(), Value::Owned(slf) => slf.index_owned_dyn(index), - Value::Leash(slf) => slf.index_leash_dyn(index), + Value::LeashSized(slf) => slf.index_leash_dyn(index), Value::OptionBox(_) => todo!(), Value::OptionLeash(_) => todo!(), Value::EnumUnit { .. } => todo!(), + Value::Copyable(_, _) => todo!(), } } @@ -473,12 +497,13 @@ impl IsValue for Value { Value::F64(f) => ValuePresentation::F64(f.into()), Value::StringLiteral(_) => todo!(), Value::Owned(ref value) => (**value).present_dyn(), - Value::Leash(value) => value.present_dyn(), + Value::LeashSized(value) => value.present_dyn(), Value::OptionBox(ref value) => todo!(), Value::OptionLeash(_) => todo!(), Value::EnumUnit { index, presenter } => { presenter(index, cache, value_presentation_synchrotron) } + Value::Copyable(_, _) => todo!(), } } @@ -510,10 +535,11 @@ impl IsValue for Value { Value::F64(_) => todo!(), Value::StringLiteral(_) => todo!(), Value::Owned(ref value) => (**value).visualize_or_void_dyn(visual_synchrotron), - Value::Leash(value) => value.visualize_or_void_dyn(visual_synchrotron), + Value::LeashSized(value) => value.visualize_or_void_dyn(visual_synchrotron), Value::OptionBox(_) => todo!(), Value::OptionLeash(_) => todo!(), Value::EnumUnit { .. } => Visual::Void, + Value::Copyable(_, _) => todo!(), } } @@ -548,10 +574,11 @@ impl IsValue for Value { Value::F64(_) => todo!(), Value::StringLiteral(_) => todo!(), Value::Owned(_) => todo!(), - Value::Leash(slf) => slf.unwrap_leash_dyn(), + Value::LeashSized(slf) => slf.unwrap_leash_dyn(), Value::OptionBox(_) => todo!(), Value::OptionLeash(_) => todo!(), Value::EnumUnit { index, presenter } => todo!(), + Value::Copyable(_, _) => todo!(), } } @@ -590,7 +617,7 @@ impl PartialEq for Value { (Self::F64(l0), Self::F64(r0)) => l0 == r0, (Self::StringLiteral(l0), Self::StringLiteral(r0)) => todo!(), (Self::Owned(l0), Self::Owned(r0)) => todo!(), - (Self::Leash(l0), Self::Leash(r0)) => todo!(), + (Self::LeashSized(l0), Self::LeashSized(r0)) => todo!(), (Self::OptionBox(l0), Self::OptionBox(r0)) => todo!(), (Self::OptionLeash(l0), Self::OptionLeash(r0)) => todo!(), (Self::EnumUnit { index: l0, .. }, Self::EnumUnit { index: r0, .. }) => l0 == r0, @@ -622,7 +649,7 @@ impl PartialOrd for Value { (F64(f1), F64(f2)) => f1.partial_cmp(f2), (StringLiteral(l0), StringLiteral(r0)) => todo!(), (Value::Owned(l0), Value::Owned(r0)) => todo!(), - (Leash(l0), Leash(r0)) => todo!(), + (LeashSized(l0), LeashSized(r0)) => todo!(), (OptionBox(l0), OptionBox(r0)) => todo!(), (OptionLeash(l0), OptionLeash(r0)) => todo!(), (EnumUnit { index: l0, .. }, EnumUnit { index: r0, .. }) => todo!(), @@ -821,10 +848,11 @@ impl std::ops::Neg for Value { Value::F64(f) => Value::F64(-f), Value::StringLiteral(_) => todo!(), Value::Owned(_) => todo!(), - Value::Leash(_) => todo!(), + Value::LeashSized(_) => todo!(), Value::OptionBox(_) => todo!(), Value::OptionLeash(_) => todo!(), Value::EnumUnit { index, presenter } => todo!(), + Value::Copyable(_, _) => todo!(), } } } diff --git a/crates/value/husky-standard-value/src/value/copyable.rs b/crates/value/husky-standard-value/src/value/copyable.rs new file mode 100644 index 0000000000..90c9546965 --- /dev/null +++ b/crates/value/husky-standard-value/src/value/copyable.rs @@ -0,0 +1,26 @@ +use super::*; + +#[derive(Debug)] +pub struct CopyableConverter(fn(&u128) -> &dyn ImmortalDyn); + +impl CopyableConverter { + pub fn new(t: T) -> (Self, u128) + where + T: Copy + Immortal + Into + Eq, + for<'a> &'a T: From<&'a u128>, + { + let v: u128 = t.into(); + #[cfg(debug_assertions)] + { + let s: &T = (&v).into(); + assert_eq!(*s, t); + } + ( + Self(|v| { + let t: &T = v.into(); + t + }), + v, + ) + } +} diff --git a/crates/visored/visored-lean-transpilation/Cargo.toml b/crates/visored/visored-lean-transpilation/Cargo.toml index 052fdadcd3..1c7b9d5c03 100644 --- a/crates/visored/visored-lean-transpilation/Cargo.toml +++ b/crates/visored/visored-lean-transpilation/Cargo.toml @@ -21,6 +21,7 @@ interned.workspace = true salsa = { workspace = true, optional = true } # latex latex-prelude.workspace = true +latex-token.workspace = true # lean lean-coword.workspace = true lean-mir-expr.workspace = true @@ -33,6 +34,7 @@ husky-tree-utils.workspace = true # visored visored-annotation.workspace = true visored-entity-path.workspace = true +visored-sem-expr.workspace = true visored-mir-expr.workspace = true visored-opr.workspace = true visored-prelude.workspace = true diff --git a/crates/visored/visored-lean-transpilation/src/builder.rs b/crates/visored/visored-lean-transpilation/src/builder.rs index 5b272501bf..77e8d1a7ed 100644 --- a/crates/visored/visored-lean-transpilation/src/builder.rs +++ b/crates/visored/visored-lean-transpilation/src/builder.rs @@ -1,8 +1,12 @@ +use latex_token::storage::LxTokenStorage; use lean_coword::ident::LnIdent; use lean_mir_expr::{ - builder::{LnMirExprBuilder, WithLnNamespace}, + constructor::{LnMirExprConstructor, WithLnNamespace}, expr::{LnMirExprArena, LnMirExprData}, - item_defn::{def::LnMirDefBody, LnItemDefnArena, LnItemDefnData, LnItemDefnIdxRange}, + item_defn::{ + def::LnMirDefBody, LnItemDefnArena, LnItemDefnComment, LnItemDefnCommentMap, + LnItemDefnData, LnItemDefnIdxRange, + }, stmt::LnMirStmtArena, tactic::LnMirTacticArena, }; @@ -11,9 +15,14 @@ use visored_entity_path::module::VdModulePath; use visored_mir_expr::{ expr::VdMirExprArenaRef, region::VdMirExprRegionData, + source_map::VdMirSourceMap, stmt::VdMirStmtArenaRef, symbol::local_defn::{storage::VdMirSymbolLocalDefnStorage, VdMirSymbolLocalDefnIdx}, }; +use visored_sem_expr::range::{ + VdSemClauseTokenIdxRangeMap, VdSemDivisionTokenIdxRangeMap, VdSemExprTokenIdxRangeMap, + VdSemPhraseTokenIdxRangeMap, VdSemSentenceTokenIdxRangeMap, VdSemStmtTokenIdxRangeMap, +}; use crate::{ dictionary::VdLeanDictionary, @@ -22,49 +31,94 @@ use crate::{ }; pub struct VdLeanTranspilationBuilder<'a> { - lean_hir_expr_builder: LnMirExprBuilder, + lean_hir_expr_builder: LnMirExprConstructor, expr_arena: VdMirExprArenaRef<'a>, stmt_arena: VdMirStmtArenaRef<'a>, dictionary: &'a VdLeanDictionary, mangler: VdLeanTranspilationMangler, current_module_path: VdModulePath, + source_map: &'a VdMirSourceMap, + sem_expr_range_map: &'a VdSemExprTokenIdxRangeMap, + sem_phrase_range_map: &'a VdSemPhraseTokenIdxRangeMap, + sem_clause_range_map: &'a VdSemClauseTokenIdxRangeMap, + sem_sentence_range_map: &'a VdSemSentenceTokenIdxRangeMap, + sem_stmt_range_map: &'a VdSemStmtTokenIdxRangeMap, + sem_division_range_map: &'a VdSemDivisionTokenIdxRangeMap, + token_storage: &'a LxTokenStorage, + input: &'a str, } impl<'a> WithLnNamespace for VdLeanTranspilationBuilder<'a> { - fn ln_mir_expr_builder_mut(&mut self) -> &mut LnMirExprBuilder { + fn ln_mir_expr_builder_mut(&mut self) -> &mut LnMirExprConstructor { &mut self.lean_hir_expr_builder } } impl<'a> VdLeanTranspilationBuilder<'a> { pub fn new0( + input: &'a str, vd_mir_expr_region_data: &'a VdMirExprRegionData, + source_map: &'a VdMirSourceMap, dictionary: &'a VdLeanDictionary, root_module_path: VdModulePath, + sem_expr_range_map: &'a VdSemExprTokenIdxRangeMap, + sem_phrase_range_map: &'a VdSemPhraseTokenIdxRangeMap, + sem_clause_range_map: &'a VdSemClauseTokenIdxRangeMap, + sem_sentence_range_map: &'a VdSemSentenceTokenIdxRangeMap, + sem_stmt_range_map: &'a VdSemStmtTokenIdxRangeMap, + sem_division_range_map: &'a VdSemDivisionTokenIdxRangeMap, + token_storage: &'a LxTokenStorage, ) -> Self { Self::new( + input, vd_mir_expr_region_data.expr_arena(), vd_mir_expr_region_data.stmt_arena(), vd_mir_expr_region_data.symbol_local_defn_storage(), + source_map, dictionary, root_module_path, + sem_expr_range_map, + sem_phrase_range_map, + sem_clause_range_map, + sem_sentence_range_map, + sem_stmt_range_map, + sem_division_range_map, + token_storage, ) } pub fn new( + input: &'a str, expr_arena: VdMirExprArenaRef<'a>, stmt_arena: VdMirStmtArenaRef<'a>, symbol_local_defn_storage: &'a VdMirSymbolLocalDefnStorage, + source_map: &'a VdMirSourceMap, dictionary: &'a VdLeanDictionary, root_module_path: VdModulePath, + sem_expr_range_map: &'a VdSemExprTokenIdxRangeMap, + sem_phrase_range_map: &'a VdSemPhraseTokenIdxRangeMap, + sem_clause_range_map: &'a VdSemClauseTokenIdxRangeMap, + sem_sentence_range_map: &'a VdSemSentenceTokenIdxRangeMap, + sem_stmt_range_map: &'a VdSemStmtTokenIdxRangeMap, + sem_division_range_map: &'a VdSemDivisionTokenIdxRangeMap, + token_storage: &'a LxTokenStorage, ) -> Self { Self { - lean_hir_expr_builder: LnMirExprBuilder::new(), + lean_hir_expr_builder: LnMirExprConstructor::new(), expr_arena, stmt_arena, + source_map, dictionary, mangler: VdLeanTranspilationMangler::new(symbol_local_defn_storage), current_module_path: root_module_path, + sem_expr_range_map, + sem_phrase_range_map, + sem_clause_range_map, + sem_sentence_range_map, + sem_stmt_range_map, + sem_division_range_map, + token_storage, + input, } } @@ -121,13 +175,49 @@ impl<'db> VdLeanTranspilationBuilder<'db> { self.stmt_arena } - pub fn dictionary(&self) -> &VdLeanDictionary { + pub fn source_map(&self) -> &'db VdMirSourceMap { + self.source_map + } + + pub fn dictionary(&self) -> &'db VdLeanDictionary { self.dictionary } + + pub fn input(&self) -> &'db str { + self.input + } + + pub fn token_storage(&self) -> &'db LxTokenStorage { + self.token_storage + } + + pub fn sem_expr_range_map(&self) -> &'db VdSemExprTokenIdxRangeMap { + self.sem_expr_range_map + } + + pub fn sem_phrase_range_map(&self) -> &'db VdSemPhraseTokenIdxRangeMap { + self.sem_phrase_range_map + } + + pub fn sem_clause_range_map(&self) -> &'db VdSemClauseTokenIdxRangeMap { + self.sem_clause_range_map + } + + pub fn sem_sentence_range_map(&self) -> &'db VdSemSentenceTokenIdxRangeMap { + self.sem_sentence_range_map + } + + pub fn sem_stmt_range_map(&self) -> &'db VdSemStmtTokenIdxRangeMap { + self.sem_stmt_range_map + } + + pub fn sem_division_range_map(&self) -> &'db VdSemDivisionTokenIdxRangeMap { + self.sem_division_range_map + } } impl<'db> Deref for VdLeanTranspilationBuilder<'db> { - type Target = LnMirExprBuilder; + type Target = LnMirExprConstructor; fn deref(&self) -> &Self::Target { &self.lean_hir_expr_builder @@ -148,6 +238,7 @@ impl<'db> VdLeanTranspilationBuilder<'db> { LnMirStmtArena, LnMirTacticArena, LnItemDefnArena, + LnItemDefnCommentMap, ) { self.lean_hir_expr_builder.finish() } diff --git a/crates/visored/visored-lean-transpilation/src/helpers/tracker.rs b/crates/visored/visored-lean-transpilation/src/helpers/tracker.rs index db24052c45..fd3cfcd463 100644 --- a/crates/visored/visored-lean-transpilation/src/helpers/tracker.rs +++ b/crates/visored/visored-lean-transpilation/src/helpers/tracker.rs @@ -13,7 +13,7 @@ use lean_mir_expr::{ fmt::{LnMirExprFormatter, LnMirExprFormatterConfig}, show::display_tree::LnMirExprDisplayTreeBuilder, }, - item_defn::{LnItemDefnArena, LnItemDefnIdxRange}, + item_defn::{LnItemDefnArena, LnItemDefnComment, LnItemDefnIdxRange, LnItemDefnOrderedMap}, stmt::{LnMirStmtArena, LnMirStmtIdxRange}, tactic::LnMirTacticArena, }; @@ -29,10 +29,11 @@ pub struct VdLeanTranspilationTracker<'a, Input: IsVdLeanTranspilationInput<'a>> stmt_arena: LnMirStmtArena, tactic_arena: LnMirTacticArena, defn_arena: LnItemDefnArena, + defn_comments: LnItemDefnOrderedMap, output: Input::VdLeanTranspilationOutput, } -pub trait IsVdLeanTranspilationInput<'a>: IsVdMirExprInput<'a> + Copy { +pub trait IsVdLeanTranspilationInput<'a>: IsVdMirExprInput<'a> { type VdLeanTranspilationOutput: IsVdLeanTranspilationOutput + FromVdTranspileToLean; } @@ -61,28 +62,47 @@ impl<'a, Input: IsVdLeanTranspilationInput<'a>> VdLeanTranspilationTracker<'a, I token_annotations: &[((&str, &str), VdTokenAnnotation)], space_annotations: &[((&str, &str), VdSpaceAnnotation)], ) -> Self { + let content = input.content(); let VdMirExprTracker { root_module_path, expr_arena: vd_mir_expr_arena, stmt_arena: vd_mir_stmt_arena, symbol_local_defn_storage: vd_mir_symbol_local_defn_storage, + source_map: vd_mir_source_map, + sem_expr_range_map, + sem_phrase_range_map, + sem_clause_range_map, + sem_sentence_range_map, + sem_stmt_range_map, + sem_division_range_map, + token_storage, output, } = VdMirExprTracker::new(input, &[], &[]); let dictionary = &VdLeanDictionary::new_standard(); let mut builder = VdLeanTranspilationBuilder::new( + content, vd_mir_expr_arena.as_arena_ref(), vd_mir_stmt_arena.as_arena_ref(), &vd_mir_symbol_local_defn_storage, + &vd_mir_source_map, dictionary, root_module_path, + &sem_expr_range_map, + &sem_phrase_range_map, + &sem_clause_range_map, + &sem_sentence_range_map, + &sem_stmt_range_map, + &sem_division_range_map, + &token_storage, ); let output = FromVdTranspileToLean::from_transpile_to_lean(output, &mut builder); - let (expr_arena, stmt_arena, tactic_arena, defn_arena) = builder.finish(); + let (expr_arena, stmt_arena, tactic_arena, defn_arena, defn_comments) = builder.finish(); Self { expr_arena, stmt_arena, tactic_arena, defn_arena, + defn_comments, output, } } @@ -110,6 +130,7 @@ impl<'a, Input: IsVdLeanTranspilationInput<'a>> VdLeanTranspilationTracker<'a, I self.stmt_arena.as_arena_ref(), self.tactic_arena.as_arena_ref(), self.defn_arena.as_arena_ref(), + &self.defn_comments, config, ) } diff --git a/crates/visored/visored-lean-transpilation/src/stmt.rs b/crates/visored/visored-lean-transpilation/src/stmt.rs index bdecde9cbc..c5dbfac1df 100644 --- a/crates/visored/visored-lean-transpilation/src/stmt.rs +++ b/crates/visored/visored-lean-transpilation/src/stmt.rs @@ -3,14 +3,16 @@ mod then; use crate::*; use lean_mir_expr::{ expr::LnMirExprData, - item_defn::{LnItemDefnData, LnItemDefnIdxRange, LnMirItemDefnGroupMeta}, + item_defn::{LnItemDefnComment, LnItemDefnData, LnItemDefnIdxRange, LnMirItemDefnGroupMeta}, }; use namespace::vd_module_path_to_ln_namespace; use ty::VdTypeLeanTranspilation; use visored_mir_expr::{ expr::{VdMirExprData, VdMirExprIdx}, pattern::VdMirPattern, - stmt::{block::VdMirBlockMeta, VdMirStmtData, VdMirStmtIdx, VdMirStmtIdxRange}, + stmt::{ + block::VdMirBlockMeta, VdMirStmtData, VdMirStmtIdx, VdMirStmtIdxRange, VdMirStmtSource, + }, }; use visored_term::ty::VdType; @@ -20,7 +22,28 @@ impl VdTranspileToLean for VdMirStmtIdxRange { .into_iter() .map(|stmt| builder.build_ln_item_defn_from_vd_stmt(stmt)) .collect(); - builder.alloc_item_defns(item_defns) + let source_map = builder.source_map(); + let input = builder.input(); + let token_storage = builder.token_storage(); + let sem_expr_range_map = builder.sem_expr_range_map(); + let sem_phrase_range_map = builder.sem_phrase_range_map(); + let sem_clause_range_map = builder.sem_clause_range_map(); + let sem_sentence_range_map = builder.sem_sentence_range_map(); + let sem_division_range_map = builder.sem_division_range_map(); + let sem_stmt_range_map = builder.sem_stmt_range_map(); + builder.alloc_item_defns( + item_defns, + self.into_iter().map(|stmt| { + let token_idx_range = match source_map[stmt] { + VdMirStmtSource::Stmt(_) + | VdMirStmtSource::Division(_) + | VdMirStmtSource::Sentence(_) => return LnItemDefnComment::Void, + VdMirStmtSource::Clause(clause) => sem_clause_range_map[clause], + }; + let offset_range = token_storage.token_idx_range_offset_range(token_idx_range); + LnItemDefnComment::from_latex_source(&input[offset_range]) + }), + ) } } diff --git a/crates/visored/visored-lean-transpilation/src/tests/body.rs b/crates/visored/visored-lean-transpilation/src/tests/body.rs index b9cf013978..3460a105fe 100644 --- a/crates/visored/visored-lean-transpilation/src/tests/body.rs +++ b/crates/visored/visored-lean-transpilation/src/tests/body.rs @@ -35,7 +35,9 @@ fn basic_body_to_lean_works() { └─ group: `sentence` └─ variable: `x` "#]], - &expect!["variable (x : ℕ)"], + &expect![[r#" + -- Let $x\in\mathbb{N}$ + variable (x : ℕ)"#]], ); t( r#"\begin{example}\end{example}"#, @@ -59,6 +61,7 @@ fn basic_body_to_lean_works() { "#]], &expect![[r#" namespace Example1 + -- Let $x\in\mathbb{R}$ variable (x : ℝ) end Example1 "#]], @@ -74,6 +77,7 @@ fn basic_body_to_lean_works() { "#]], &expect![[r#" namespace Section1 + -- Let $x\in\mathbb{R}$ variable (x : ℝ) end Section1 "#]], @@ -98,9 +102,11 @@ fn basic_body_to_lean_works() { "#]], &expect![[r#" namespace Section1 + -- Let $x\in\mathbb{R}$ variable (x : ℝ) namespace Subsection1 + -- Let $y\in\mathbb{R}$ variable (y : ℝ) end Subsection1 diff --git a/crates/visored/visored-lean-transpilation/src/tests/document.rs b/crates/visored/visored-lean-transpilation/src/tests/document.rs index 2b7ee0ea98..f04ad6955c 100644 --- a/crates/visored/visored-lean-transpilation/src/tests/document.rs +++ b/crates/visored/visored-lean-transpilation/src/tests/document.rs @@ -14,7 +14,7 @@ fn t(content: &str, expected_display_tree: &Expect, expected_fmt: &Expect) { let file_path = LxFilePath::new(PathBuf::from(file!())); let tracker = VdLeanTranspilationTracker::new( LxDocumentInput { - specs_dir: dev_paths.specs_dir(), + specs_dir: dev_paths.specs_dir().to_path_buf(), file_path, content, }, @@ -39,7 +39,9 @@ Let $x\in\mathbb{R}$. └─ group: `sentence` └─ variable: `x` "#]], - &expect!["variable (x : ℝ)"], + &expect![[r#" + -- Let $x\in\mathbb{R}$ + variable (x : ℝ)"#]], ); t( r#"\documentclass{article} @@ -57,6 +59,7 @@ Let $x\in\mathbb{R}$. "#]], &expect![[r#" namespace Section1 + -- Let $x\in\mathbb{R}$ variable (x : ℝ) end Section1 "#]], @@ -92,9 +95,11 @@ Let $y\in\mathbb{R}$. "#]], &expect![[r#" namespace Section1 + -- Let $x\in\mathbb{R}$ variable (x : ℝ) namespace Subsection1 + -- Let $y\in\mathbb{R}$ variable (y : ℝ) end Subsection1 @@ -133,7 +138,7 @@ fn latex_shorts_to_lean_works() { let file_path = LxFilePath::new(file_path.clone()); let tracker = VdLeanTranspilationTracker::new( LxDocumentInput { - specs_dir: dev_paths.specs_dir(), + specs_dir: dev_paths.specs_dir().to_path_buf(), file_path, content, }, diff --git a/crates/visored/visored-lean-transpilation/src/tests/page.rs b/crates/visored/visored-lean-transpilation/src/tests/page.rs index 572e20819b..89f600b86f 100644 --- a/crates/visored/visored-lean-transpilation/src/tests/page.rs +++ b/crates/visored/visored-lean-transpilation/src/tests/page.rs @@ -31,7 +31,9 @@ fn basic_visored_clause_to_lean_works() { └─ group: `sentence` └─ variable: `x` "#]], - &expect!["variable (x : ℕ)"], + &expect![[r#" + -- Let $x\in\mathbb{N}$ + variable (x : ℕ)"#]], ); t( "Let $x\\in\\mathbb{Z}$.", @@ -40,7 +42,9 @@ fn basic_visored_clause_to_lean_works() { └─ group: `sentence` └─ variable: `x` "#]], - &expect!["variable (x : ℤ)"], + &expect![[r#" + -- Let $x\in\mathbb{Z}$ + variable (x : ℤ)"#]], ); t( "Let $x\\in\\mathbb{Q}$.", @@ -49,7 +53,9 @@ fn basic_visored_clause_to_lean_works() { └─ group: `sentence` └─ variable: `x` "#]], - &expect!["variable (x : ℚ)"], + &expect![[r#" + -- Let $x\in\mathbb{Q}$ + variable (x : ℚ)"#]], ); t( "Let $x\\in\\mathbb{R}$.", @@ -58,7 +64,9 @@ fn basic_visored_clause_to_lean_works() { └─ group: `sentence` └─ variable: `x` "#]], - &expect!["variable (x : ℝ)"], + &expect![[r#" + -- Let $x\in\mathbb{R}$ + variable (x : ℝ)"#]], ); t( "Let $x\\in\\mathbb{C}$.", @@ -67,7 +75,9 @@ fn basic_visored_clause_to_lean_works() { └─ group: `sentence` └─ variable: `x` "#]], - &expect!["variable (x : ℂ)"], + &expect![[r#" + -- Let $x\in\mathbb{C}$ + variable (x : ℂ)"#]], ); t( "Let $x\\in\\mathbb{R}$. Then $x=x$.", @@ -83,8 +93,10 @@ fn basic_visored_clause_to_lean_works() { └─ sorry "#]], &expect![[r#" + -- Let $x\in\mathbb{R}$ variable (x : ℝ) + -- Then $x=x$ def h : x = x := sorry"#]], ); t( @@ -103,8 +115,10 @@ fn basic_visored_clause_to_lean_works() { └─ sorry "#]], &expect![[r#" + -- Let $x\in\mathbb{N}$ variable (x : ℕ) + -- Then $2x\ge x$ def h : 2 * x ≥ x := sorry"#]], ); t( @@ -151,12 +165,16 @@ fn basic_visored_clause_to_lean_works() { └─ sorry "#]], &expect![[r#" + -- Let $x\in\mathbb{R}$ variable (x : ℝ) + -- Then ${(x-1)}^2 \ge 0$ def h : (x - 1) ^ 2 ≥ 0 := sorry + -- Then $x^2-2x+1 \ge 0$ def h1 : x ^ 2 - 2 * x + 1 ≥ 0 := sorry + -- Then $x^2 + 1\ge 2x$ def h2 : x ^ 2 + 1 ≥ 2 * x := sorry"#]], ); } diff --git a/crates/visored/visored-mir-expr/Cargo.toml b/crates/visored/visored-mir-expr/Cargo.toml index e60098bc1b..09c0a158ac 100644 --- a/crates/visored/visored-mir-expr/Cargo.toml +++ b/crates/visored/visored-mir-expr/Cargo.toml @@ -22,6 +22,7 @@ salsa = { workspace = true, optional = true } latex-environment.workspace = true latex-math-letter.workspace = true latex-prelude.workspace = true +latex-token.workspace = true # utils husky-tree-utils.workspace = true # visored diff --git a/crates/visored/visored-mir-expr/src/builder.rs b/crates/visored/visored-mir-expr/src/builder.rs index 2a5f93d3e5..13683b34cb 100644 --- a/crates/visored/visored-mir-expr/src/builder.rs +++ b/crates/visored/visored-mir-expr/src/builder.rs @@ -1,7 +1,8 @@ use crate::{ expr::{VdMirExprArena, VdMirExprArenaRef, VdMirExprData, VdMirExprIdx, VdMirExprIdxRange}, region::VdMirExprRegionData, - stmt::{VdMirStmtArena, VdMirStmtArenaRef, VdMirStmtData, VdMirStmtIdxRange}, + source_map::VdMirSourceMap, + stmt::{VdMirStmtArena, VdMirStmtArenaRef, VdMirStmtData, VdMirStmtIdxRange, VdMirStmtSource}, symbol::local_defn::{storage::VdMirSymbolLocalDefnStorage, VdMirSymbolLocalDefnData}, }; use visored_sem_expr::{ @@ -20,6 +21,7 @@ pub struct VdMirExprBuilder<'db> { expr_arena: VdMirExprArena, stmt_arena: VdMirStmtArena, symbol_local_defn_storage: VdMirSymbolLocalDefnStorage, + source_map: VdMirSourceMap, } impl<'db> VdMirExprBuilder<'db> { @@ -54,6 +56,7 @@ impl<'db> VdMirExprBuilder<'db> { expr_arena: VdMirExprArena::default(), stmt_arena: VdMirStmtArena::default(), symbol_local_defn_storage: VdMirSymbolLocalDefnStorage::new_empty(), + source_map: Default::default(), }; slf.build_symbol_local_defns(sem_symbol_local_defn_storage); slf @@ -110,8 +113,11 @@ impl<'db> VdMirExprBuilder<'db> { pub(crate) fn alloc_stmts( &mut self, data: impl IntoIterator, + sources: impl IntoIterator, ) -> VdMirStmtIdxRange { - self.stmt_arena.alloc_batch(data) + let stmts = self.stmt_arena.alloc_batch(data); + self.source_map.set_stmts(stmts, sources); + stmts } pub(crate) fn alloc_symbol_local_defns(&mut self, data: Vec) { @@ -126,11 +132,19 @@ impl<'db> VdMirExprBuilder<'db> { ) } - pub fn finish(self) -> (VdMirExprArena, VdMirStmtArena, VdMirSymbolLocalDefnStorage) { + pub fn finish( + self, + ) -> ( + VdMirExprArena, + VdMirStmtArena, + VdMirSymbolLocalDefnStorage, + VdMirSourceMap, + ) { ( self.expr_arena, self.stmt_arena, self.symbol_local_defn_storage, + self.source_map, ) } } diff --git a/crates/visored/visored-mir-expr/src/expr.rs b/crates/visored/visored-mir-expr/src/expr.rs index 6d1e21bfee..1ad5106fbc 100644 --- a/crates/visored/visored-mir-expr/src/expr.rs +++ b/crates/visored/visored-mir-expr/src/expr.rs @@ -6,7 +6,9 @@ pub mod tests; use crate::*; use application::VdMirFunc; -use idx_arena::{Arena, ArenaIdx, ArenaIdxRange, ArenaRef}; +use idx_arena::{ + map::ArenaMap, ordered_map::ArenaOrderedMap, Arena, ArenaIdx, ArenaIdxRange, ArenaRef, +}; use smallvec::SmallVec; use symbol::local_defn::VdMirSymbolLocalDefnIdx; use visored_entity_path::path::VdItemPath; @@ -47,6 +49,8 @@ pub enum VdMirExprData { } pub type VdMirExprArena = Arena; +pub type VdMirExprMap = ArenaMap; +pub type VdMirExprOrderedMap = ArenaOrderedMap; pub type VdMirExprArenaRef<'a> = ArenaRef<'a, VdMirExprData>; pub type VdMirExprIdx = ArenaIdx; pub type VdMirExprIdxRange = ArenaIdxRange; diff --git a/crates/visored/visored-mir-expr/src/helpers/tracker.rs b/crates/visored/visored-mir-expr/src/helpers/tracker.rs index 1cc644f32b..9cad308fa9 100644 --- a/crates/visored/visored-mir-expr/src/helpers/tracker.rs +++ b/crates/visored/visored-mir-expr/src/helpers/tracker.rs @@ -12,16 +12,32 @@ use latex_prelude::{ helper::tracker::{LxDocumentBodyInput, LxDocumentInput, LxFormulaInput, LxPageInput}, mode::LxMode, }; +use latex_token::storage::LxTokenStorage; +use source_map::VdMirSourceMap; use symbol::local_defn::storage::VdMirSymbolLocalDefnStorage; use visored_annotation::annotation::{space::VdSpaceAnnotation, token::VdTokenAnnotation}; use visored_entity_path::module::VdModulePath; -use visored_sem_expr::helpers::tracker::{IsVdSemExprInput, VdSemExprTracker}; +use visored_sem_expr::{ + helpers::tracker::{IsVdSemExprInput, VdSemExprTracker}, + range::{ + VdSemClauseTokenIdxRangeMap, VdSemDivisionTokenIdxRangeMap, VdSemExprTokenIdxRangeMap, + VdSemPhraseTokenIdxRangeMap, VdSemSentenceTokenIdxRangeMap, VdSemStmtTokenIdxRangeMap, + }, +}; pub struct VdMirExprTracker<'a, Input: IsVdMirExprInput<'a>> { pub root_module_path: VdModulePath, pub expr_arena: VdMirExprArena, pub stmt_arena: VdMirStmtArena, pub symbol_local_defn_storage: VdMirSymbolLocalDefnStorage, + pub source_map: VdMirSourceMap, + pub sem_expr_range_map: VdSemExprTokenIdxRangeMap, + pub sem_phrase_range_map: VdSemPhraseTokenIdxRangeMap, + pub sem_clause_range_map: VdSemClauseTokenIdxRangeMap, + pub sem_sentence_range_map: VdSemSentenceTokenIdxRangeMap, + pub sem_stmt_range_map: VdSemStmtTokenIdxRangeMap, + pub sem_division_range_map: VdSemDivisionTokenIdxRangeMap, + pub token_storage: LxTokenStorage, pub output: Input::VdMirExprOutput, } @@ -85,12 +101,20 @@ impl<'a, Input: IsVdMirExprInput<'a>> VdMirExprTracker<'a, Input> { &sem_symbol_local_defn_storage, ); let result = FromToVdMir::from_to_vd_mir(output, &mut builder); - let (expr_arena, stmt_arena, symbol_local_defn_storage) = builder.finish(); + let (expr_arena, stmt_arena, symbol_local_defn_storage, source_map) = builder.finish(); Self { root_module_path, expr_arena, stmt_arena, symbol_local_defn_storage, + source_map, + sem_expr_range_map, + sem_phrase_range_map, + sem_clause_range_map, + sem_sentence_range_map, + sem_stmt_range_map, + sem_division_range_map, + token_storage, output: result, } } diff --git a/crates/visored/visored-mir-expr/src/lib.rs b/crates/visored/visored-mir-expr/src/lib.rs index 0bc7e5fa27..490bb736d5 100644 --- a/crates/visored/visored-mir-expr/src/lib.rs +++ b/crates/visored/visored-mir-expr/src/lib.rs @@ -3,6 +3,7 @@ pub mod expr; pub mod helpers; pub mod pattern; pub mod region; +pub mod source_map; pub mod stmt; pub mod symbol; #[cfg(test)] diff --git a/crates/visored/visored-mir-expr/src/source_map.rs b/crates/visored/visored-mir-expr/src/source_map.rs new file mode 100644 index 0000000000..99d5f5946b --- /dev/null +++ b/crates/visored/visored-mir-expr/src/source_map.rs @@ -0,0 +1,35 @@ +use crate::{ + expr::VdMirExprOrderedMap, + stmt::{VdMirStmtIdx, VdMirStmtIdxRange, VdMirStmtOrderedMap, VdMirStmtSource}, +}; +use visored_sem_expr::{ + clause::VdSemClauseIdx, division::VdSemDivisionIdx, expr::VdSemExprIdx, + sentence::VdSemSentenceIdx, stmt::VdSemStmtIdx, +}; + +#[derive(Default, Debug, PartialEq, Eq)] +pub struct VdMirSourceMap { + stmt_map: VdMirStmtOrderedMap, +} + +impl VdMirSourceMap { + pub(crate) fn set_stmts( + &mut self, + stmts: VdMirStmtIdxRange, + sources: impl IntoIterator, + ) { + let mut source_iter = sources.into_iter(); + for stmt in stmts { + self.stmt_map.insert_next(stmt, source_iter.next().unwrap()) + } + debug_assert!(source_iter.next().is_none()) + } +} + +impl std::ops::Index for VdMirSourceMap { + type Output = VdMirStmtSource; + + fn index(&self, index: VdMirStmtIdx) -> &Self::Output { + &self.stmt_map[index] + } +} diff --git a/crates/visored/visored-mir-expr/src/stmt.rs b/crates/visored/visored-mir-expr/src/stmt.rs index cd13db3983..3d96bdefa9 100644 --- a/crates/visored/visored-mir-expr/src/stmt.rs +++ b/crates/visored/visored-mir-expr/src/stmt.rs @@ -4,7 +4,9 @@ mod tests; use self::block::*; use crate::{expr::VdMirExprIdx, pattern::VdMirPattern, *}; -use idx_arena::{Arena, ArenaIdx, ArenaIdxRange, ArenaRef}; +use idx_arena::{ + map::ArenaMap, ordered_map::ArenaOrderedMap, Arena, ArenaIdx, ArenaIdxRange, ArenaRef, +}; use visored_entity_path::module::VdModulePath; use visored_prelude::division::VdDivisionLevel; use visored_sem_expr::{ @@ -38,17 +40,28 @@ pub enum VdMirStmtData { } pub type VdMirStmtArena = Arena; +pub type VdMirStmtOrderedMap = ArenaOrderedMap; +pub type VdMirStmtMap = ArenaMap; pub type VdMirStmtArenaRef<'a> = ArenaRef<'a, VdMirStmtData>; pub type VdMirStmtIdx = ArenaIdx; pub type VdMirStmtIdxRange = ArenaIdxRange; +#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, PartialOrd, Ord)] +pub enum VdMirStmtSource { + Stmt(VdSemStmtIdx), + Division(VdSemDivisionIdx), + Sentence(VdSemSentenceIdx), + Clause(VdSemClauseIdx), +} + impl ToVdMir for VdSemDivisionIdxRange { fn to_vd_mir(self, builder: &mut VdMirExprBuilder) -> VdMirStmtIdxRange { let data = self .into_iter() .map(|division| builder.build_stmt_from_sem_division(division)) .collect::>(); - builder.alloc_stmts(data) + let sources = self.into_iter().map(VdMirStmtSource::Division); + builder.alloc_stmts(data, sources) } } @@ -86,7 +99,8 @@ impl ToVdMir for VdSemStmtIdxRange { .into_iter() .map(|stmt| builder.build_stmt_from_sem_stmt(stmt)) .collect::>(); - builder.alloc_stmts(data) + let sources = self.into_iter().map(VdMirStmtSource::Stmt); + builder.alloc_stmts(data, sources) } } @@ -119,7 +133,8 @@ impl ToVdMir for VdSemSentenceIdxRange { .into_iter() .map(|sentence| builder.build_stmt_from_sem_sentence(sentence)) .collect::>(); - builder.alloc_stmts(data) + let sources = self.into_iter().map(VdMirStmtSource::Sentence); + builder.alloc_stmts(data, sources) } } @@ -140,7 +155,8 @@ impl ToVdMir for VdSemClauseIdxRange { .into_iter() .map(|clause| builder.build_stmt_from_sem_clause(clause)) .collect::>(); - builder.alloc_stmts(data) + let sources = self.into_iter().map(VdMirStmtSource::Clause); + builder.alloc_stmts(data, sources) } } diff --git a/crates/visored/visored-mir-expr/src/stmt/tests/document.rs b/crates/visored/visored-mir-expr/src/stmt/tests/document.rs index d333ec0069..28edf2d7aa 100644 --- a/crates/visored/visored-mir-expr/src/stmt/tests/document.rs +++ b/crates/visored/visored-mir-expr/src/stmt/tests/document.rs @@ -13,7 +13,7 @@ fn t(content: &str, expect: &Expect) { let file_path = LxFilePath::new(PathBuf::from(file!())); let tracker = VdMirExprTracker::new( LxDocumentInput { - specs_dir: dev_paths.specs_dir(), + specs_dir: dev_paths.specs_dir().to_path_buf(), file_path, content, }, diff --git a/crates/visored/visored-sem-expr/src/division/tests/document.rs b/crates/visored/visored-sem-expr/src/division/tests/document.rs index f913e16ec7..fa015715ca 100644 --- a/crates/visored/visored-sem-expr/src/division/tests/document.rs +++ b/crates/visored/visored-sem-expr/src/division/tests/document.rs @@ -9,7 +9,7 @@ fn t(content: &str, expected: &Expect) { let file_path = LxFilePath::new(PathBuf::from(file!())); let tracker = VdSemExprTracker::new( LxDocumentInput { - specs_dir: dev_paths.specs_dir(), + specs_dir: dev_paths.specs_dir().to_path_buf(), file_path, content, }, diff --git a/crates/visored/visored-syn-expr/src/division/tests/document.rs b/crates/visored/visored-syn-expr/src/division/tests/document.rs index 9f03120156..25a48020b9 100644 --- a/crates/visored/visored-syn-expr/src/division/tests/document.rs +++ b/crates/visored/visored-syn-expr/src/division/tests/document.rs @@ -9,7 +9,7 @@ fn t(content: &str, expected: &Expect) { let file_path = LxFilePath::new(PathBuf::from(file!())); let tracker = VdSynExprTracker::new( LxDocumentInput { - specs_dir: dev_paths.specs_dir(), + specs_dir: dev_paths.specs_dir().to_path_buf(), file_path, content, }, diff --git a/crates/vmir/husky-vmir/expect-files/registry/latex-ast-hsy-0.1.0/package_linket_linket_vmir_regions.md b/crates/vmir/husky-vmir/expect-files/registry/latex-ast-hsy-0.1.0/package_linket_linket_vmir_regions.md index b545b60e79..ecc5296c0c 100644 --- a/crates/vmir/husky-vmir/expect-files/registry/latex-ast-hsy-0.1.0/package_linket_linket_vmir_regions.md +++ b/crates/vmir/husky-vmir/expect-files/registry/latex-ast-hsy-0.1.0/package_linket_linket_vmir_regions.md @@ -1,3 +1,20 @@ ```rust -[] +[ + ( + Linket { + data: LinketData::MajorStaticVar { + path: MajorFormPath(`latex_ast_hsy::AST`, `StaticVar`), + instantiation: LinInstantiation { + path: ItemPath(`latex_ast_hsy::AST`), + context: LinTypeContext { + comptime_var_overrides: [], + }, + variable_resolutions: [], + separator: None, + }, + }, + }, + None, + ), +] ``` \ No newline at end of file diff --git a/crates/vmir/husky-vmir/src/expr.rs b/crates/vmir/husky-vmir/src/expr.rs index d138156c52..bf027713a5 100644 --- a/crates/vmir/husky-vmir/src/expr.rs +++ b/crates/vmir/husky-vmir/src/expr.rs @@ -207,12 +207,7 @@ impl<'comptime, Linktime: IsLinktime> VmirBuilder<'comptime, Linktime> { MajorItemPath::Type(ty_path) => todo!(), MajorItemPath::Trait(trai_path) => todo!(), MajorItemPath::Form(major_form_path) => match major_form_path.kind(db) { - MajorFormKind::Ritchie(ritchie_item_kind) => { - use husky_print_utils::p; - use salsa::DebugWithDb; - p!(path.debug(db)); - VmirExprData::RitchieItemPath - } + MajorFormKind::Ritchie(ritchie_item_kind) => VmirExprData::RitchieItemPath, MajorFormKind::TypeAlias => todo!(), MajorFormKind::TypeVar => todo!(), MajorFormKind::Val => { diff --git a/projects/ai-math-autoformalization/husky/latex2lean/Corgi.toml b/projects/ai-math-autoformalization/husky/latex2lean/Corgi.toml index bca1cc55b3..48c54770f3 100644 --- a/projects/ai-math-autoformalization/husky/latex2lean/Corgi.toml +++ b/projects/ai-math-autoformalization/husky/latex2lean/Corgi.toml @@ -1,2 +1,5 @@ [package] name = "latex2lean" + +[dependencies] +latex-ast-hsy = "0.1.0" diff --git a/projects/ai-math-autoformalization/husky/latex2lean/target-rs/Cargo.lock b/projects/ai-math-autoformalization/husky/latex2lean/target-rs/Cargo.lock index 78a1402709..3fcec44f82 100644 --- a/projects/ai-math-autoformalization/husky/latex2lean/target-rs/Cargo.lock +++ b/projects/ai-math-autoformalization/husky/latex2lean/target-rs/Cargo.lock @@ -26,23 +26,73 @@ dependencies = [ "zerocopy", ] +[[package]] +name = "allocator-api2" +version = "0.2.20" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "45862d1c77f2228b9e10bc609d5bc203d86ebc9b87ad8d5d5167a6c9abf739d9" + +[[package]] +name = "ansi_term" +version = "0.12.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d52a9bb7ec0cf484c551830a7ce27bd20d67eac647e1befb56b0be4ee39a55d2" +dependencies = [ + "winapi", +] + [[package]] name = "arc-swap" version = "1.7.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "69f7f8c3906b62b754cd5326047894316021dcfe5a194c8ea52bdd94934a3457" +[[package]] +name = "arraydeque" +version = "0.5.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "7d902e3d592a523def97af8f317b08ce16b7ab854c1985a0c671e6f15cebc236" + +[[package]] +name = "async-trait" +version = "0.1.83" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "721cae7de5c34fbb2acd27e21e6d2cf7b886dce0c27388d46c4e6c47ea4318dd" +dependencies = [ + "proc-macro2", + "quote", + "syn", +] + [[package]] name = "autocfg" version = "1.4.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "ace50bade8e6234aa140d9a2f552bbee1db4d353f69b8217bc503490fc1a9f26" +[[package]] +name = "base64" +version = "0.21.7" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9d297deb1925b89f2ccc13d7635fa0714f12c87adce1c75356b39ca9b7178567" + [[package]] name = "bitflags" version = "2.6.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "b048fb63fd8b5923fc5aa7b340d8e156aec7ec02f0c78fa8a6ddc2613f6f71de" +dependencies = [ + "serde", +] + +[[package]] +name = "block-buffer" +version = "0.10.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "3078c7629b62d3f0439517fa394996acacc5cbc91c5a20d8c658e77abd503a71" +dependencies = [ + "generic-array", +] [[package]] name = "cc" @@ -65,10 +115,53 @@ version = "2.1.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "cbf2150cce219b664a8a70df7a1f933836724b503f8a413af9365b4dcc4d90b8" dependencies = [ - "lazy_static", + "lazy_static 1.5.0", "windows-sys 0.48.0", ] +[[package]] +name = "composite-pattern" +version = "0.1.0" + +[[package]] +name = "config" +version = "0.14.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "68578f196d2a33ff61b27fae256c3164f65e36382648e30666dde05b8cc9dfdf" +dependencies = [ + "async-trait", + "convert_case", + "json5", + "nom", + "pathdiff", + "ron", + "rust-ini", + "serde", + "serde_json", + "toml", + "yaml-rust2", +] + +[[package]] +name = "const-random" +version = "0.1.18" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "87e00182fe74b066627d63b85fd550ac2998d4b0bd86bfed477a0ae4c7c71359" +dependencies = [ + "const-random-macro", +] + +[[package]] +name = "const-random-macro" +version = "0.1.16" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f9d839f2a20b0aee515dc581a6172f2321f96cab76c1a38a4c584a194955390e" +dependencies = [ + "getrandom", + "once_cell", + "tiny-keccak", +] + [[package]] name = "convert_case" version = "0.6.0" @@ -78,6 +171,23 @@ dependencies = [ "unicode-segmentation", ] +[[package]] +name = "coword" +version = "0.1.0" +dependencies = [ + "interned", + "lazy_static 1.5.0", +] + +[[package]] +name = "cpufeatures" +version = "0.2.16" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "16b80225097f2e5ae4e7179dd2266824648f3e2f49d9134d584b76389d31c4c3" +dependencies = [ + "libc", +] + [[package]] name = "crossbeam" version = "0.8.4" @@ -134,6 +244,22 @@ version = "0.8.20" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "22ec99545bb0ed0ea7bb9b8e1e9122ea386ff8a48c0922e43f36d45ab09e0e80" +[[package]] +name = "crunchy" +version = "0.2.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "7a81dae078cea95a014a339291cec439d2f232ebe854a9d672b796c6afafa9b7" + +[[package]] +name = "crypto-common" +version = "0.1.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "1bfb12502f3fc46cca1bb51ac28df9d618d813cdc3d2f25b9fe775a34af26bb3" +dependencies = [ + "generic-array", + "typenum", +] + [[package]] name = "dashmap" version = "6.1.0" @@ -148,18 +274,67 @@ dependencies = [ "parking_lot_core", ] +[[package]] +name = "digest" +version = "0.10.7" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9ed9a281f7bc9b7576e61468ba615a66a5c8cfdff42420a70aa82701a3b1e292" +dependencies = [ + "block-buffer", + "crypto-common", +] + +[[package]] +name = "directories" +version = "5.0.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9a49173b84e034382284f27f1af4dcbbd231ffa358c0fe316541a7337f376a35" +dependencies = [ + "dirs-sys", +] + +[[package]] +name = "dirs-sys" +version = "0.4.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "520f05a5cbd335fae5a99ff7a6ab8627577660ee5cfd6a94a6a929b52ff0321c" +dependencies = [ + "libc", + "option-ext", + "redox_users", + "windows-sys 0.48.0", +] + [[package]] name = "dissimilar" version = "1.0.9" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "59f8e79d1fbf76bdfbde321e902714bf6c49df88a7dda6fc682fc2979226962d" +[[package]] +name = "dlv-list" +version = "0.5.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "442039f5147480ba31067cb00ada1adae6892028e40e45fc5de7b7df6dcc1b5f" +dependencies = [ + "const-random", +] + [[package]] name = "either" version = "1.13.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "60b1af1c220855b6ceac025d3f6ecdd2b7c4894bfe9cd9bda4fbb4bc7c0d4cf0" +[[package]] +name = "encoding_rs" +version = "0.8.35" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "75030f3c4f45dafd7586dd6780965a8c7e8e285a5ecb86713e63a79c5b2766f3" +dependencies = [ + "cfg-if", +] + [[package]] name = "enum-class" version = "0.1.0" @@ -209,6 +384,33 @@ dependencies = [ "once_cell", ] +[[package]] +name = "fixedbitset" +version = "0.4.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0ce7134b9999ecaf8bcd65542e436736ef32ddca1b3e06094cb6ec5755203b80" + +[[package]] +name = "generic-array" +version = "0.14.7" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "85649ca51fd72272d7821adaf274ad91c288277713d9c18820d8499a7ff69e9a" +dependencies = [ + "typenum", + "version_check", +] + +[[package]] +name = "getrandom" +version = "0.2.15" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "c4567c8db10ae91089c99af84c68c38da3ec2f087c3f82960bcdbf3656b6f4d7" +dependencies = [ + "cfg-if", + "libc", + "wasi", +] + [[package]] name = "hashbrown" version = "0.14.5" @@ -216,6 +418,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "e5274423e17b7c9fc20b6e7e208532f9b19825d82dfd615708b70edd83df41f1" dependencies = [ "ahash", + "allocator-api2", ] [[package]] @@ -224,6 +427,15 @@ version = "0.15.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "3a9bfc1af68b1726ea47d3d5109de126281def866b33970e10fbab11b5dafab3" +[[package]] +name = "hashlink" +version = "0.8.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e8094feaf31ff591f651a2664fb9cfd92bba7a60ce3197265e9482ebe753c8f7" +dependencies = [ + "hashbrown 0.14.5", +] + [[package]] name = "hashlink" version = "0.9.1" @@ -264,7 +476,7 @@ dependencies = [ "husky-standard-linket-impl", "husky-standard-value", "husky-visual-protocol", - "ordered-float", + "ordered-float 4.5.0", ] [[package]] @@ -289,10 +501,21 @@ dependencies = [ name = "husky-figure-zone-protocol" version = "0.1.0" dependencies = [ + "enum-class", "serde", "shifted-unsigned-int", ] +[[package]] +name = "husky-io-utils" +version = "0.1.0" +dependencies = [ + "composite-pattern", + "husky-print-utils", + "relative-path", + "thiserror", +] + [[package]] name = "husky-item-path-interface" version = "0.1.0" @@ -331,7 +554,7 @@ name = "husky-literal-value" version = "0.1.0" dependencies = [ "husky-value", - "ordered-float", + "ordered-float 4.5.0", ] [[package]] @@ -339,6 +562,7 @@ name = "husky-minimal-toml-utils" version = "0.1.0" dependencies = [ "husky-coword", + "husky-io-utils", "husky-print-utils", "salsa", "thiserror", @@ -417,7 +641,7 @@ dependencies = [ "husky-value-protocol", "husky-visual-protocol", "husky-wild-utils", - "ordered-float", + "ordered-float 4.5.0", "paste", "serde", "serde-impl", @@ -436,6 +660,19 @@ dependencies = [ "syn", ] +[[package]] +name = "husky-text-protocol" +version = "0.1.0" +dependencies = [ + "rustc-hash", + "serde", + "shifted-unsigned-int", +] + +[[package]] +name = "husky-tree-utils" +version = "0.1.0" + [[package]] name = "husky-unicode-symbols" version = "0.1.0" @@ -463,7 +700,7 @@ dependencies = [ name = "husky-value-protocol" version = "0.1.0" dependencies = [ - "ordered-float", + "ordered-float 4.5.0", "serde", ] @@ -472,8 +709,9 @@ name = "husky-visual-protocol" version = "0.1.0" dependencies = [ "enum-class", + "husky-figure-zone-protocol", "husky-print-utils", - "ordered-float", + "ordered-float 4.5.0", "serde", "shifted-unsigned-int", "smallvec", @@ -483,6 +721,16 @@ dependencies = [ name = "husky-wild-utils" version = "0.1.0" +[[package]] +name = "idx-arena" +version = "0.0.0" +dependencies = [ + "husky-check-utils", + "husky-print-utils", + "salsa", + "serde", +] + [[package]] name = "indexmap" version = "2.6.0" @@ -493,18 +741,168 @@ dependencies = [ "hashbrown 0.15.1", ] +[[package]] +name = "interned" +version = "0.1.0" +dependencies = [ + "dashmap", + "interned-macros", + "lazy_static 1.5.0", +] + +[[package]] +name = "interned-macros" +version = "0.1.0" +dependencies = [ + "convert_case", + "proc-macro2", + "quote", + "syn", +] + [[package]] name = "itoa" version = "1.0.13" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "540654e97a3f4470a492cd30ff187bc95d89557a903a2bbf112e2fae98104ef2" +[[package]] +name = "json5" +version = "0.4.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "96b0db21af676c1ce64250b5f40f3ce2cf27e4e47cb91ed91eb6fe9350b430c1" +dependencies = [ + "pest", + "pest_derive", + "serde", +] + +[[package]] +name = "latex-ast" +version = "0.1.0" +dependencies = [ + "coword", + "enum-class", + "husky-coword", + "husky-print-utils", + "husky-tree-utils", + "idx-arena", + "latex-command", + "latex-environment", + "latex-math-letter", + "latex-math-punctuation", + "latex-prelude", + "latex-rose-punctuation", + "latex-token", + "ptree", + "serde", + "smallvec", + "time-capsule", +] + +[[package]] +name = "latex-ast-hsy" +version = "0.1.0" +dependencies = [ + "husky-core", + "husky-linket-impl", + "husky-path-utils", + "husky-standard-linket-impl", + "husky-standard-value", + "idx-arena", + "latex-ast", + "latex-prelude", + "latex-vfs", + "lazy_static 1.5.0", + "serde", + "vec-like", +] + +[[package]] +name = "latex-command" +version = "0.1.0" +dependencies = [ + "coword", + "husky-coword", + "latex-math-letter", + "latex-prelude", + "lazy_static 1.5.0", + "lisp-csv", + "rustc-hash", + "thiserror", +] + +[[package]] +name = "latex-environment" +version = "0.1.0" +dependencies = [ + "coword", + "husky-coword", + "latex-prelude", + "lazy_static 1.5.0", + "rustc-hash", + "thiserror", +] + +[[package]] +name = "latex-math-letter" +version = "0.1.0" +dependencies = [ + "thiserror", +] + +[[package]] +name = "latex-math-punctuation" +version = "0.1.0" +dependencies = [ + "enum-index", +] + +[[package]] +name = "latex-prelude" +version = "0.1.0" +dependencies = [ + "latex-vfs", + "salsa", +] + +[[package]] +name = "latex-rose-punctuation" +version = "0.1.0" + +[[package]] +name = "latex-token" +version = "0.1.0" +dependencies = [ + "coword", + "enum-class", + "husky-print-utils", + "husky-text-protocol", + "interned", + "latex-command", + "latex-math-letter", + "latex-math-punctuation", + "latex-prelude", + "latex-rose-punctuation", + "ordered-float 4.5.0", + "rustc-hash", + "shifted-unsigned-int", +] + +[[package]] +name = "latex-vfs" +version = "0.1.0" +dependencies = [ + "interned", +] + [[package]] name = "latex2lean" version = "0.1.0" dependencies = [ "ad-hoc-devsoul-dependency", "husky-core", + "latex-ast-hsy", ] [[package]] @@ -513,9 +911,16 @@ version = "0.1.0" dependencies = [ "ad-hoc-devsoul-dependency", "husky-core", + "latex-ast-hsy", "latex2lean", ] +[[package]] +name = "lazy_static" +version = "0.2.11" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "76f033c7ad61445c5b347c7382dd1237847eb1bce590fe50365dcb33d546be73" + [[package]] name = "lazy_static" version = "1.5.0" @@ -528,6 +933,28 @@ version = "0.2.164" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "433bfe06b8c75da9b2e3fbea6e5329ff87748f0b144ef75306e674c3f6f7c13f" +[[package]] +name = "libredox" +version = "0.1.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "c0ff37bd590ca25063e35af745c343cb7a0271906fb7b37e4813e8f79f00268d" +dependencies = [ + "bitflags", + "libc", +] + +[[package]] +name = "lisp-csv" +version = "0.1.0" +dependencies = [ + "either", + "husky-print-utils", + "husky-text-protocol", + "maybe-result", + "ordered-float 4.5.0", + "thiserror", +] + [[package]] name = "lock_api" version = "0.4.12" @@ -557,6 +984,22 @@ version = "2.7.4" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "78ca9ab1a0babb1e7d5695e3530886289c18cf2f87ec19a575a0abdce112e3a3" +[[package]] +name = "minimal-lexical" +version = "0.2.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "68354c5c6bd36d73ff3feceb05efa59b6acb7626617f4962be322a825e61f79a" + +[[package]] +name = "nom" +version = "7.1.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d273983c5a657a70a3e8f2a01329822f3b8c8172b73826411a55751e404a0a4a" +dependencies = [ + "memchr", + "minimal-lexical", +] + [[package]] name = "num-traits" version = "0.2.19" @@ -572,6 +1015,21 @@ version = "1.20.2" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "1261fe7e33c73b354eab43b1273a57c8f967d0391e80353e51f764ac02cf6775" +[[package]] +name = "option-ext" +version = "0.2.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "04744f49eae99ab78e0d5c0b603ab218f515ea8cfe5a456d7629ad883a3b6e7d" + +[[package]] +name = "ordered-float" +version = "2.10.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "68f19d67e5a2795c94e73e0bb1cc1a7edeb2e28efd39e2e1c9b7a40c1108b11c" +dependencies = [ + "num-traits", +] + [[package]] name = "ordered-float" version = "4.5.0" @@ -583,6 +1041,16 @@ dependencies = [ "serde", ] +[[package]] +name = "ordered-multimap" +version = "0.7.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "49203cdcae0030493bad186b28da2fa25645fa276a51b6fec8010d281e02ef79" +dependencies = [ + "dlv-list", + "hashbrown 0.14.5", +] + [[package]] name = "original-error" version = "0.1.0" @@ -622,6 +1090,61 @@ version = "0.2.2" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "d61c5ce1153ab5b689d0c074c4e7fc613e942dfb7dd9eea5ab202d2ad91fe361" +[[package]] +name = "pest" +version = "2.7.14" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "879952a81a83930934cbf1786752d6dedc3b1f29e8f8fb2ad1d0a36f377cf442" +dependencies = [ + "memchr", + "thiserror", + "ucd-trie", +] + +[[package]] +name = "pest_derive" +version = "2.7.14" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d214365f632b123a47fd913301e14c946c61d1c183ee245fa76eb752e59a02dd" +dependencies = [ + "pest", + "pest_generator", +] + +[[package]] +name = "pest_generator" +version = "2.7.14" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "eb55586734301717aea2ac313f50b2eb8f60d2fc3dc01d190eefa2e625f60c4e" +dependencies = [ + "pest", + "pest_meta", + "proc-macro2", + "quote", + "syn", +] + +[[package]] +name = "pest_meta" +version = "2.7.14" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b75da2a70cf4d9cb76833c990ac9cd3923c9a8905a8929789ce347c84564d03d" +dependencies = [ + "once_cell", + "pest", + "sha2", +] + +[[package]] +name = "petgraph" +version = "0.6.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b4c5cc86750666a3ed20bdaf5ca2a0344f9c67674cae0515bec2da16fbaa47db" +dependencies = [ + "fixedbitset", + "indexmap", +] + [[package]] name = "proc-macro2" version = "1.0.92" @@ -640,6 +1163,21 @@ dependencies = [ "cc", ] +[[package]] +name = "ptree" +version = "0.5.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e98cc9b19fef1b3e9d04e52df8a5b2a521e44d488cb3162bcd0bba3b5f0c35a4" +dependencies = [ + "ansi_term", + "config", + "directories", + "petgraph", + "serde", + "serde-value", + "tint", +] + [[package]] name = "quote" version = "1.0.37" @@ -677,12 +1215,45 @@ dependencies = [ "bitflags", ] +[[package]] +name = "redox_users" +version = "0.4.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ba009ff324d1fc1b900bd1fdb31564febe58a8ccc8a6fdbb93b543d33b13ca43" +dependencies = [ + "getrandom", + "libredox", + "thiserror", +] + [[package]] name = "relative-path" version = "1.9.3" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "ba39f3699c378cd8970968dcbff9c43159ea4cfbd88d43c00b22f2ef10a435d2" +[[package]] +name = "ron" +version = "0.8.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b91f7eff05f748767f183df4320a63d6936e9c6107d97c9e6bdd9784f4289c94" +dependencies = [ + "base64", + "bitflags", + "serde", + "serde_derive", +] + +[[package]] +name = "rust-ini" +version = "0.20.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "3e0698206bcb8882bf2a9ecb4c1e7785db57ff052297085a6efd4fe42302068a" +dependencies = [ + "cfg-if", + "ordered-multimap", +] + [[package]] name = "rustc-hash" version = "2.0.0" @@ -714,7 +1285,7 @@ dependencies = [ "dashmap", "either", "enum-index", - "hashlink", + "hashlink 0.9.1", "husky-salsa-log-utils", "indexmap", "log", @@ -771,6 +1342,16 @@ dependencies = [ "serde_json", ] +[[package]] +name = "serde-value" +version = "0.7.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f3a1a3341211875ef120e117ea7fd5228530ae7e7036a779fdc9117be6b3282c" +dependencies = [ + "ordered-float 2.10.1", + "serde", +] + [[package]] name = "serde_derive" version = "1.0.215" @@ -795,6 +1376,26 @@ dependencies = [ "serde", ] +[[package]] +name = "serde_spanned" +version = "0.6.8" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "87607cb1398ed59d48732e575a4c28a7a8ebf2454b964fe3f224f2afc07909e1" +dependencies = [ + "serde", +] + +[[package]] +name = "sha2" +version = "0.10.8" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "793db75ad2bcafc3ffa7c68b215fee268f537982cd901d132f89c6343f3a3dc8" +dependencies = [ + "cfg-if", + "cpufeatures", + "digest", +] + [[package]] name = "shifted-unsigned-int" version = "0.1.0" @@ -865,6 +1466,74 @@ dependencies = [ "syn", ] +[[package]] +name = "time-capsule" +version = "0.1.0" + +[[package]] +name = "tint" +version = "1.0.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "7af24570664a3074673dbbf69a65bdae0ae0b72f2949b1adfbacb736ee4d6896" +dependencies = [ + "lazy_static 0.2.11", +] + +[[package]] +name = "tiny-keccak" +version = "2.0.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "2c9d3793400a45f954c52e73d068316d76b6f4e36977e3fcebb13a2721e80237" +dependencies = [ + "crunchy", +] + +[[package]] +name = "toml" +version = "0.8.19" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "a1ed1f98e3fdc28d6d910e6737ae6ab1a93bf1985935a1193e68f93eeb68d24e" +dependencies = [ + "serde", + "serde_spanned", + "toml_datetime", + "toml_edit", +] + +[[package]] +name = "toml_datetime" +version = "0.6.8" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0dd7358ecb8fc2f8d014bf86f6f638ce72ba252a2c3a2572f2a795f1d23efb41" +dependencies = [ + "serde", +] + +[[package]] +name = "toml_edit" +version = "0.22.22" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "4ae48d6208a266e853d946088ed816055e556cc6028c5e8e2b84d9fa5dd7c7f5" +dependencies = [ + "indexmap", + "serde", + "serde_spanned", + "toml_datetime", + "winnow", +] + +[[package]] +name = "typenum" +version = "1.17.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "42ff0bf0c66b8238c6f3b578df37d0b7848e55df8577b3f74f92a69acceeb825" + +[[package]] +name = "ucd-trie" +version = "0.1.7" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "2896d95c02a80c6d6a5d6e953d479f5ddf2dfdb6a244441010e373ac0fb88971" + [[package]] name = "unicode-ident" version = "1.0.14" @@ -893,6 +1562,34 @@ version = "0.9.5" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "0b928f33d975fc6ad9f86c8f283853ad26bdd5b10b7f1542aa2fa15e2289105a" +[[package]] +name = "wasi" +version = "0.11.0+wasi-snapshot-preview1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9c8d87e72b64a3b4db28d11ce29237c246188f4f51057d65a7eab63b7987e423" + +[[package]] +name = "winapi" +version = "0.3.9" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "5c839a674fcd7a98952e593242ea400abe93992746761e38641405d28b00f419" +dependencies = [ + "winapi-i686-pc-windows-gnu", + "winapi-x86_64-pc-windows-gnu", +] + +[[package]] +name = "winapi-i686-pc-windows-gnu" +version = "0.4.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ac3b87c63620426dd9b991e5ce0329eff545bccbbb34f3be09ff6fb6ab51b7b6" + +[[package]] +name = "winapi-x86_64-pc-windows-gnu" +version = "0.4.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "712e227841d057c1ee1cd2fb22fa7e5a5461ae8e48fa2ca79ec42cfc1931183f" + [[package]] name = "windows-sys" version = "0.48.0" @@ -1032,6 +1729,26 @@ version = "0.52.6" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "589f6da84c646204747d1270a2a5661ea66ed1cced2631d546fdfb155959f9ec" +[[package]] +name = "winnow" +version = "0.6.20" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "36c1fec1a2bb5866f07c25f68c26e565c4c200aebb96d7e55710c19d3e8ac49b" +dependencies = [ + "memchr", +] + +[[package]] +name = "yaml-rust2" +version = "0.8.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8902160c4e6f2fb145dbe9d6760a75e3c9522d8bf796ed7047c85919ac7115f8" +dependencies = [ + "arraydeque", + "encoding_rs", + "hashlink 0.8.4", +] + [[package]] name = "zerocopy" version = "0.7.35" diff --git a/projects/ai-math-autoformalization/husky/latex2lean/target-rs/Cargo.toml b/projects/ai-math-autoformalization/husky/latex2lean/target-rs/Cargo.toml index 15324c8fce..130e54caf5 100644 --- a/projects/ai-math-autoformalization/husky/latex2lean/target-rs/Cargo.toml +++ b/projects/ai-math-autoformalization/husky/latex2lean/target-rs/Cargo.toml @@ -8,6 +8,9 @@ path = "../../../../../registry/ad-hoc-devsoul-dependency" [workspace.dependencies.husky-core] path = "../../../../../library/core" +[workspace.dependencies.latex-ast-hsy] +path = "../../../../../registry/latex-ast-hsy-0.1.0" + [workspace.dependencies.latex2lean] path = "latex2lean" diff --git a/projects/ai-math-autoformalization/husky/latex2lean/target-rs/latex2lean-linkets/Cargo.toml b/projects/ai-math-autoformalization/husky/latex2lean/target-rs/latex2lean-linkets/Cargo.toml index a0486ef50e..339c79367e 100644 --- a/projects/ai-math-autoformalization/husky/latex2lean/target-rs/latex2lean-linkets/Cargo.toml +++ b/projects/ai-math-autoformalization/husky/latex2lean/target-rs/latex2lean-linkets/Cargo.toml @@ -9,6 +9,9 @@ workspace = true [dependencies.husky-core] workspace = true +[dependencies.latex-ast-hsy] +workspace = true + [dependencies.latex2lean] workspace = true diff --git a/projects/ai-math-autoformalization/husky/latex2lean/target-rs/latex2lean-linkets/src/lib.rs b/projects/ai-math-autoformalization/husky/latex2lean/target-rs/latex2lean-linkets/src/lib.rs index 0b2320528d..f946ea40cf 100644 --- a/projects/ai-math-autoformalization/husky/latex2lean/target-rs/latex2lean-linkets/src/lib.rs +++ b/projects/ai-math-autoformalization/husky/latex2lean/target-rs/latex2lean-linkets/src/lib.rs @@ -44,4 +44,5 @@ linket_impls![ fn_linket_impl!(::span), fn_linket_impl!(::right_mass), static_var_linket_impl!(husky_core::task::TASK, husky_core::task::__TASK__ITEM_PATH_ID_INTERFACE), + static_var_linket_impl!(latex_ast_hsy::AST, latex_ast_hsy::__AST__ITEM_PATH_ID_INTERFACE), ]; \ No newline at end of file diff --git a/projects/ai-math-autoformalization/husky/latex2lean/target-rs/latex2lean/Cargo.toml b/projects/ai-math-autoformalization/husky/latex2lean/target-rs/latex2lean/Cargo.toml index 3eb047b9ad..dc7031687e 100644 --- a/projects/ai-math-autoformalization/husky/latex2lean/target-rs/latex2lean/Cargo.toml +++ b/projects/ai-math-autoformalization/husky/latex2lean/target-rs/latex2lean/Cargo.toml @@ -8,3 +8,6 @@ workspace = true [dependencies.husky-core] workspace = true + +[dependencies.latex-ast-hsy] +workspace = true diff --git a/projects/ai-math-autoformalization/husky/latex2lean/target-rs/latex2lean/src/lib.rs b/projects/ai-math-autoformalization/husky/latex2lean/target-rs/latex2lean/src/lib.rs index 1c3ace03e3..4b85a1d2d5 100644 --- a/projects/ai-math-autoformalization/husky/latex2lean/target-rs/latex2lean/src/lib.rs +++ b/projects/ai-math-autoformalization/husky/latex2lean/target-rs/latex2lean/src/lib.rs @@ -2,3 +2,4 @@ use husky_core::*; use ad_hoc_devsoul_dependency::{*, ugly::*}; +use latex_ast_hsy::*; \ No newline at end of file diff --git a/projects/ai-math-autoformalization/lean/central-46/Central46/Shorts/batch0.lean b/projects/ai-math-autoformalization/lean/central-46/Central46/Shorts/batch0.lean index 3cdf54b779..4a0fbd15cf 100644 --- a/projects/ai-math-autoformalization/lean/central-46/Central46/Shorts/batch0.lean +++ b/projects/ai-math-autoformalization/lean/central-46/Central46/Shorts/batch0.lean @@ -4,32 +4,40 @@ import Mathlib.Data.Real.Basic import Mathlib.Tactic.Explode namespace Example1 +-- Then $1+1=2$ def h : 1 + 1 = 2 := sorry end Example1 namespace Example2 +-- Let $x\in\mathbb{R}$ variable (x : ℝ) +-- Then $x^2\ge 0$ def h : x ^ 2 ≥ 0 := sorry end Example2 namespace Example3 +-- Let $x\in\mathbb{R}$ variable (x : ℝ) +-- Then $x^2 + 1\ge 2x$ def h : x ^ 2 + 1 ≥ 2 * x := sorry end Example3 namespace Example4 +-- Then $1=1=1$ def h : 1 = 1 := by calc 1 = 1 := sorry _ = 1 := sorry +-- Then $1=1<2$ def h1 : 1 < 2 := by calc 1 = 1 := sorry _ < 2 := sorry +-- Then $1.0 \le 1 \le 1$ def h2 : 1.0 ≤ 1 := by calc 1.0 ≤ 1 := sorry diff --git a/projects/ai-math-autoformalization/lean/central-46/Central46/Shorts/batch1.lean b/projects/ai-math-autoformalization/lean/central-46/Central46/Shorts/batch1.lean index 29b15cf552..0b166f153a 100644 --- a/projects/ai-math-autoformalization/lean/central-46/Central46/Shorts/batch1.lean +++ b/projects/ai-math-autoformalization/lean/central-46/Central46/Shorts/batch1.lean @@ -4,135 +4,191 @@ import Mathlib.Data.Real.Basic import Mathlib.Tactic.Explode namespace Example1 +-- Then $1+1=2$ def h : 1 + 1 = 2 := sorry end Example1 namespace Example2 +-- Let $x\in\mathbb{R}$ variable (x : ℝ) +-- Then $x^2\ge 0$ def h : x ^ 2 ≥ 0 := sorry end Example2 namespace Example3 +-- Let $a\in\mathbb{R}$ variable (a : ℝ) +-- Let $b\in\mathbb{R}$ variable (b : ℝ) +-- Then $a+b=b+a$ def h : a + b = b + a := sorry end Example3 namespace Example4 +-- Let $x\in\mathbb{R}$ variable (x : ℝ) +-- Then $x^2 \ge 0$ def h : x ^ 2 ≥ 0 := sorry end Example4 namespace Example5 +-- Let $x\in\mathbb{R}$ variable (x : ℝ) +-- Assume $x>0$ variable (h : x > 0) +-- Then $x + \frac{1}{x} - 2 = \frac{x^2 + 1 - 2x}{x}$ def h1 : x + 1 / x - 2 = (x ^ 2 + 1 - 2 * x) / x := sorry +-- Then $\frac{x^2 + 1 - 2x}{x} = \frac{{(x-1)}^2}{x}$ def h2 : (x ^ 2 + 1 - 2 * x) / x = (x - 1) ^ 2 / x := sorry +-- Then $x + \frac{1}{x} - 2 = \frac{{(x-1)}^2}{x}$ def h3 : x + 1 / x - 2 = (x - 1) ^ 2 / x := sorry +-- Then $\frac{{(x-1)}^2}{x} \ge 0$ def h4 : (x - 1) ^ 2 / x ≥ 0 := sorry +-- Then $x + \frac{1}{x} - 2 \ge 0$ def h5 : x + 1 / x - 2 ≥ 0 := sorry +-- Then $x + \frac{1}{x} \ge 2$ def h6 : x + 1 / x ≥ 2 := sorry end Example5 namespace Example6 +-- Let $x\in\mathbb{R}$ variable (x : ℝ) +-- Then $x + \frac{1}{x} - 2 = \frac{x^2 + 1 - 2x}{x}$ def h : x + 1 / x - 2 = (x ^ 2 + 1 - 2 * x) / x := sorry +-- Then $\frac{x^2 + 1 - 2x}{x} = \frac{{(x-1)}^2}{x}$ def h1 : (x ^ 2 + 1 - 2 * x) / x = (x - 1) ^ 2 / x := sorry +-- Then $x + \frac{1}{x} - 2 = \frac{{(x-1)}^2}{x}$ def h2 : x + 1 / x - 2 = (x - 1) ^ 2 / x := sorry +-- Then $\frac{{(x-1)}^2}{x} \ge 0$ def h3 : (x - 1) ^ 2 / x ≥ 0 := sorry +-- Then $x + \frac{1}{x} - 2 \ge 0$ def h4 : x + 1 / x - 2 ≥ 0 := sorry +-- Then $x + \frac{1}{x} \ge 2$ def h5 : x + 1 / x ≥ 2 := sorry end Example6 namespace Example7 +-- Let $x\in\mathbb{R}$ variable (x : ℝ) +-- Then $x^2 + 1 - 2x = {(x-1)}^2$ def h : x ^ 2 + 1 - 2 * x = (x - 1) ^ 2 := sorry +-- Then ${(x-1)}^2 \ge 0$ def h1 : (x - 1) ^ 2 ≥ 0 := sorry +-- Then $x^2 + 1 - 2x \ge 0$ def h2 : x ^ 2 + 1 - 2 * x ≥ 0 := sorry +-- Then $x^2 + 1 \ge 2x$ def h3 : x ^ 2 + 1 ≥ 2 * x := sorry end Example7 namespace Example8 +-- Let $x\in\mathbb{R}$ variable (x : ℝ) +-- Assume $x > 0$ variable (h : x > 0) +-- Then $x + 1 - 2\sqrt{x} = {(\sqrt{x}-1)}^2$ def h1 : x + 1 - 2 * (√ x) = ((√ x) - 1) ^ 2 := sorry +-- Then ${(\sqrt{x}-1)}^2 \ge 0$ def h2 : ((√ x) - 1) ^ 2 ≥ 0 := sorry +-- Then $x + 1 - 2\sqrt{x} \ge 0$ def h3 : x + 1 - 2 * (√ x) ≥ 0 := sorry +-- Then $x + 1 \ge 2\sqrt{x}$ def h4 : x + 1 ≥ 2 * (√ x) := sorry end Example8 namespace Example9 +-- Let $x\in\mathbb{R}$ variable (x : ℝ) +-- Let $y\in\mathbb{R}$ variable (y : ℝ) +-- Then $\frac{1}{x} + \frac{1}{y} - \frac{4}{x+y} = \frac{y(x+y) + x(x+y) - 4xy}{xy(x+y)}$ def h : 1 / x + 1 / y - 4 / (x + y) = (y * (x + y) + x * (x + y) - 4 * x * y) / (x * y * (x + y)) := sorry +-- Then $\frac{y(x+y) + x(x+y) - 4xy}{xy(x+y)} = \frac{yx + x^2 + x^2 + yx - 4xy}{xy(x+y)}$ def h1 : (y * (x + y) + x * (x + y) - 4 * x * y) / (x * y * (x + y)) = (y * x + x ^ 2 + x ^ 2 + y * x - 4 * x * y) / (x * y * (x + y)) := sorry +-- Then $\frac{yx + x^2 + x^2 + yx - 4xy}{xy(x+y)} = \frac{x^2 + x^2 -2xy}{xy(x+y)}$ def h2 : (y * x + x ^ 2 + x ^ 2 + y * x - 4 * x * y) / (x * y * (x + y)) = (x ^ 2 + x ^ 2 - 2 * x * y) / (x * y * (x + y)) := sorry +-- Then $\frac{x^2 + x^2 -2xy}{xy(x+y)} = \frac{{(x-y)}^2}{xy(x+y)}$ def h3 : (x ^ 2 + x ^ 2 - 2 * x * y) / (x * y * (x + y)) = (x - y) ^ 2 / (x * y * (x + y)) := sorry +-- Then $\frac{{(x-y)}^2}{xy(x+y)} \ge 0$ def h4 : (x - y) ^ 2 / (x * y * (x + y)) ≥ 0 := sorry +-- Then $\frac{1}{x} + \frac{1}{y} - \frac{4}{x+y} \ge 0$ def h5 : 1 / x + 1 / y - 4 / (x + y) ≥ 0 := sorry +-- Then $\frac{1}{x} + \frac{1}{y} \ge \frac{4}{x+y}$ def h6 : 1 / x + 1 / y ≥ 4 / (x + y) := sorry end Example9 namespace Example10 +-- Let $a\in\mathbb{R}$ variable (a : ℝ) +-- Let $b\in\mathbb{R}$ variable (b : ℝ) +-- Then $\frac{a}{b} + \frac{b}{a} - 2 = \frac{a^2 + b^2 - 2ab}{ab}$ def h : a / b + b / a - 2 = (a ^ 2 + b ^ 2 - 2 * a * b) / (a * b) := sorry +-- Then $\frac{a^2 + b^2 - 2ab}{ab} = \frac{{(a-b)}^2}{ab}$ def h1 : (a ^ 2 + b ^ 2 - 2 * a * b) / (a * b) = (a - b) ^ 2 / (a * b) := sorry +-- Then $\frac{{(a-b)}^2}{ab} \ge 0$ def h2 : (a - b) ^ 2 / (a * b) ≥ 0 := sorry +-- Then $\frac{a}{b} + \frac{b}{a} - 2 \ge 0$ def h3 : a / b + b / a - 2 ≥ 0 := sorry +-- Then $\frac{a}{b} + \frac{b}{a} \ge 2$ def h4 : a / b + b / a ≥ 2 := sorry end Example10 namespace Example11 +-- Let $x\in\mathbb{R}$ variable (x : ℝ) +-- Let $y\in\mathbb{R}$ variable (y : ℝ) +-- Then $x^2 + y^2 - 2xy = {(x-y)}^2$ def h : x ^ 2 + y ^ 2 - 2 * x * y = (x - y) ^ 2 := sorry +-- Then ${(x-y)}^2 \ge 0$ def h1 : (x - y) ^ 2 ≥ 0 := sorry +-- Then $x^2 + y^2 - 2xy \ge 0$ def h2 : x ^ 2 + y ^ 2 - 2 * x * y ≥ 0 := sorry +-- Then $x^2 + y^2 \ge 2xy$ def h3 : x ^ 2 + y ^ 2 ≥ 2 * x * y := sorry end Example11 diff --git a/registry/cybertron-mini-lean-tokens-0.1.0/src/lib.rs b/registry/cybertron-mini-lean-tokens-0.1.0/src/lib.rs index c077c6fd5a..e47c5a30da 100644 --- a/registry/cybertron-mini-lean-tokens-0.1.0/src/lib.rs +++ b/registry/cybertron-mini-lean-tokens-0.1.0/src/lib.rs @@ -95,6 +95,6 @@ impl __IsStaticVar<__VarId> for TOKEN_FILE_POSITION { } fn zones() -> &'static [__FigureZone] { - &[__FigureZone::Text] + &[__FigureZone::Roll] } } diff --git a/registry/latex-ast-hsy-0.1.0/Cargo.toml b/registry/latex-ast-hsy-0.1.0/Cargo.toml index c704a3d1e7..cf3d8fd4d8 100644 --- a/registry/latex-ast-hsy-0.1.0/Cargo.toml +++ b/registry/latex-ast-hsy-0.1.0/Cargo.toml @@ -12,8 +12,24 @@ categories.workspace = true keywords.workspace = true [dependencies] +lazy_static.workspace = true +serde.workspace = true +# abstractions +idx-arena.workspace = true +vec-like.workspace = true # latex latex-ast.workspace = true +latex-prelude.workspace = true +latex-vfs.workspace = true +# linket +husky-linket-impl.workspace = true +husky-standard-linket-impl.workspace = true +# utils +husky-path-utils.workspace = true +# value +husky-standard-value.workspace = true +# library +husky-core.workspace = true [lints] workspace = true diff --git a/registry/latex-ast-hsy-0.1.0/src/file.rs b/registry/latex-ast-hsy-0.1.0/src/file.rs new file mode 100644 index 0000000000..09d53e15f9 --- /dev/null +++ b/registry/latex-ast-hsy-0.1.0/src/file.rs @@ -0,0 +1,94 @@ +pub mod map; + +use crate::*; +use lazy_static::lazy_static; +use serde::{Deserialize, Serialize}; +use std::ops::Deref; + +#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, Serialize, Deserialize)] +pub struct LxFileIdx(u32); + +impl LxFileIdx { + pub fn index(self) -> usize { + self.0 as usize + } +} + +pub struct LxFileStorage { + files: Vec, +} + +lazy_static! { + pub static ref LX_FILE_STORAGE: LxFileStorage = LxFileStorage::new(); +} + +impl LxFileStorage { + pub fn new() -> Self { + Self { + files: vec![ + r#"\documentclass{article} +\begin{document} +Hello, world! +\end{document}"# + .to_string(), + r#"\documentclass{article} +\usepackage{amsmath} +\begin{document} +$E = mc^2$ +\end{document}"# + .to_string(), + ], + } + } + + pub fn get(&self, idx: LxFileIdx) -> Option<&str> { + self.files.get(idx.0 as usize).map(|s| s.as_str()) + } + + pub fn len(&self) -> usize { + self.files.len() + } + + pub fn is_empty(&self) -> bool { + self.files.is_empty() + } + + pub fn files(&self) -> &[String] { + &self.files + } +} + +impl From for LxFileIdx { + fn from(idx: u32) -> Self { + Self(idx) + } +} + +impl Into for LxFileIdx { + fn into(self) -> u32 { + self.0 + } +} + +impl std::ops::Index for LxFileStorage { + type Output = str; + + fn index(&self, idx: LxFileIdx) -> &Self::Output { + &self.files[idx.0 as usize] + } +} + +#[test] +fn conversion_between_u32_and_file_idx_works() { + let idx = LxFileIdx(0); + let u32_val: u32 = idx.into(); + let converted_back: LxFileIdx = u32_val.into(); + assert_eq!(converted_back, idx); +} + +#[test] +fn index_operator_works() { + let storage = LxFileStorage::new(); + let content = &storage[LxFileIdx(0)]; + assert!(content.contains("Hello, world!")); +} diff --git a/registry/latex-ast-hsy-0.1.0/src/file/map.rs b/registry/latex-ast-hsy-0.1.0/src/file/map.rs new file mode 100644 index 0000000000..3086511113 --- /dev/null +++ b/registry/latex-ast-hsy-0.1.0/src/file/map.rs @@ -0,0 +1,34 @@ +use super::*; + +pub struct LxFileMap { + values: Vec, +} + +impl std::ops::Index for LxFileMap { + type Output = V; + + fn index(&self, idx: LxFileIdx) -> &Self::Output { + &self.values[idx.index()] + } +} + +impl std::ops::Deref for LxFileMap { + type Target = Vec; + + fn deref(&self) -> &Self::Target { + &self.values + } +} + +impl LxFileStorage { + pub fn file_map<'a, V>(&'a self, f: impl Fn(usize, &'a str) -> V) -> LxFileMap { + LxFileMap { + values: self + .files + .iter() + .enumerate() + .map(|(i, s)| f(i, s)) + .collect(), + } + } +} diff --git a/registry/latex-ast-hsy-0.1.0/src/lib.hsy b/registry/latex-ast-hsy-0.1.0/src/lib.hsy index 777fdd1128..7b4dab855c 100644 --- a/registry/latex-ast-hsy-0.1.0/src/lib.hsy +++ b/registry/latex-ast-hsy-0.1.0/src/lib.hsy @@ -1,2 +1,4 @@ #[derive(Debug, Clone, Copy, PartialEq, Eq)] -pub extern LxAstId; \ No newline at end of file +pub extern LxAstId; + +pub static var AST: LxAstId; \ No newline at end of file diff --git a/registry/latex-ast-hsy-0.1.0/src/lib.rs b/registry/latex-ast-hsy-0.1.0/src/lib.rs index 358c00631d..11ff05455b 100644 --- a/registry/latex-ast-hsy-0.1.0/src/lib.rs +++ b/registry/latex-ast-hsy-0.1.0/src/lib.rs @@ -1,6 +1,230 @@ +mod file; +mod tracker; + +use self::{file::*, tracker::*}; +use husky_core::*; +use husky_standard_linket_impl::ugly::*; +use idx_arena::ArenaIdx; use latex_ast::ast::LxAstIdx; +// #[husky_standard_value::copyable_value_conversion] +#[husky_standard_value::value_conversion] +#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)] pub struct LxAstId { - // TODO: file id - pub idx: LxAstIdx, + pub file_idx: LxFileIdx, + pub ast_idx: LxAstIdx, +} + +impl From<&u128> for &LxAstId { + fn from(value: &u128) -> Self { + todo!() + } +} + +impl Into for LxAstId { + fn into(self) -> u128 { + todo!() + } +} + +impl From<__VarId> for LxAstId { + fn from(id: __VarId) -> Self { + let __VarId::Pair([fst, snd]) = id else { + todo!() + }; + Self { + file_idx: fst.into(), + ast_idx: unsafe { lx_ast_idx_from_u32(snd) }, + } + } +} + +impl Into<__VarId> for LxAstId { + fn into(self) -> __VarId { + [self.file_idx.into(), unsafe { + lx_ast_idx_to_u32(self.ast_idx) + }] + .into() + } +} + +unsafe fn lx_ast_idx_from_u32(idx: u32) -> LxAstIdx { + match idx >> 30 { + 0 => LxAstIdx::Math(ArenaIdx::new_ext(idx as usize & 0x3FFFFFFF)), + 1 => LxAstIdx::Rose(ArenaIdx::new_ext(idx as usize & 0x3FFFFFFF)), + 2 => LxAstIdx::Lisp(ArenaIdx::new_ext(idx as usize & 0x3FFFFFFF)), + 3 => LxAstIdx::Root(ArenaIdx::new_ext(idx as usize & 0x3FFFFFFF)), + _ => unreachable!(), + } +} + +fn lx_ast_idx_to_u32(idx: LxAstIdx) -> u32 { + match idx { + LxAstIdx::Math(idx) => { + assert!(idx.index() <= 0x3FFFFFFF); + (0b00 << 30) | idx.index() as u32 + } + LxAstIdx::Rose(idx) => { + assert!(idx.index() <= 0x3FFFFFFF); + (0b01 << 30) | idx.index() as u32 + } + LxAstIdx::Lisp(idx) => { + assert!(idx.index() <= 0x3FFFFFFF); + (0b10 << 30) | idx.index() as u32 + } + LxAstIdx::Root(idx) => { + assert!(idx.index() <= 0x3FFFFFFF); + (0b11 << 30) | idx.index() as u32 + } + } +} + +#[test] +fn conversion_between_u32_and_ast_idx_works() { + // Test Math variant (00) + let idx = LxAstIdx::Math(unsafe { ArenaIdx::new_ext(0) }); + assert_eq!( + unsafe { lx_ast_idx_to_u32(idx) }, + 0b0000_0000_0000_0000_0000_0000_0000_0000 + ); + assert_eq!( + unsafe { lx_ast_idx_from_u32(unsafe { lx_ast_idx_to_u32(idx) }) }, + idx + ); + + // Test Rose variant (01) + let idx = LxAstIdx::Rose(unsafe { ArenaIdx::new_ext(42) }); + assert_eq!( + unsafe { lx_ast_idx_to_u32(idx) }, + 0b0100_0000_0000_0000_0000_0000_0010_1010 + ); + assert_eq!( + unsafe { lx_ast_idx_from_u32(unsafe { lx_ast_idx_to_u32(idx) }) }, + idx + ); + + // Test Lisp variant (10) + let idx = LxAstIdx::Lisp(unsafe { ArenaIdx::new_ext(0x3FFFFFFE) }); + assert_eq!( + unsafe { lx_ast_idx_to_u32(idx) }, + 0b1011_1111_1111_1111_1111_1111_1111_1110 + ); + assert_eq!( + unsafe { lx_ast_idx_from_u32(unsafe { lx_ast_idx_to_u32(idx) }) }, + idx + ); + + // Test Root variant (11) + let idx = LxAstIdx::Root(unsafe { ArenaIdx::new_ext(0x3FFFFFFF) }); + assert_eq!( + unsafe { lx_ast_idx_to_u32(idx) }, + 0b1111_1111_1111_1111_1111_1111_1111_1111 + ); + assert_eq!( + unsafe { lx_ast_idx_from_u32(unsafe { lx_ast_idx_to_u32(idx) }) }, + idx + ); +} + +#[test] +#[should_panic(expected = "assertion failed")] +fn test_idx_overflow() { + let idx = LxAstIdx::Math(unsafe { ArenaIdx::new_ext(0x40000000) }); + unsafe { lx_ast_idx_to_u32(idx) }; // Should panic due to index being too large +} + +#[allow(non_upper_case_globals)] +pub static mut __AST__ITEM_PATH_ID_INTERFACE: Option<__ItemPathIdInterface> = None; + +#[allow(non_snake_case)] +pub fn AST() -> LxAstId { + ast_id() +} + +thread_local! { + static __AST_ID: std::cell::Cell> = Default::default(); +} + +pub(crate) fn file_idx() -> LxFileIdx { + // TODO: use a dedicated static for this? + ast_id().file_idx +} + +pub(crate) fn ast_id() -> LxAstId { + __AST_ID.get().unwrap() +} + +pub(crate) fn with_ast_id(ast_id: LxAstId, f: impl Fn() -> R) -> R { + let old = __AST_ID.replace(Some(ast_id)); + let r = f(); + __AST_ID.set(old); + r +} + +pub(crate) fn replace_ast_id(ast_id: LxAstId) -> Option { + __AST_ID.replace(Some(ast_id)) +} + +pub(crate) fn set_ast_id(ast_id: Option) { + __AST_ID.set(ast_id) +} + +pub struct AST {} + +impl __IsStaticVar<__VarId> for AST { + fn item_path_id_interface() -> __ItemPathIdInterface { + unsafe { __AST__ITEM_PATH_ID_INTERFACE.unwrap() } + } + + fn page_var_ids_aux(locked: &[__ItemPathIdInterface]) -> impl Iterator { + all_asts_within_file(0.into()).map(Into::into) + } + + fn default_page_start( + figure_zone: __FigureZone, + locked: &[__ItemPathIdInterface], + ) -> __StaticVarResult<__VarId> { + let file_idx: LxFileIdx = 0.into(); + let ast_idx = first_ast(file_idx); + Ok(LxAstId { file_idx, ast_idx }.into()) + } + + fn get_id() -> __VarId { + AST().into() + } + + fn try_set_var_id_aux( + new: __VarId, + locked: &[__ItemPathIdInterface], + ) -> __StaticVarResult { + let old = replace_ast_id(new.into()); + Ok(move || { + set_ast_id(old); + }) + } + + fn try_set_default_var_id( + locked: &[__ItemPathIdInterface], + ) -> __StaticVarResult<(__VarId, impl FnOnce() + 'static)> { + let file_idx: LxFileIdx = 0.into(); + let ast_idx = first_ast(file_idx); + let default = LxAstId { file_idx, ast_idx }.into(); + Ok((default, Self::try_set_var_id(default, locked)?)) + } + + type Value = __Value; + + fn get_value() -> Self::Value { + AST().into_value() + } + + fn zones() -> &'static [__FigureZone] { + &[__FigureZone::Roll] + } + + fn figure_chunk_base(chunk_idx: u32) -> __FigureTextChunkBaseData { + __FigureTextChunkBaseData { + text: LX_FILE_STORAGE[chunk_idx.into()].to_string(), + } + } } diff --git a/registry/latex-ast-hsy-0.1.0/src/tracker.rs b/registry/latex-ast-hsy-0.1.0/src/tracker.rs new file mode 100644 index 0000000000..7f03d54129 --- /dev/null +++ b/registry/latex-ast-hsy-0.1.0/src/tracker.rs @@ -0,0 +1,87 @@ +use crate::{file::map::LxFileMap, LxAstId, LxFileIdx, LX_FILE_STORAGE}; +use husky_path_utils::HuskyLangDevPaths; +use latex_ast::ast::LxAstIdx; +use latex_ast::helpers::tracker::LxAstTracker; +use latex_prelude::helper::tracker::LxDocumentInput; +use latex_vfs::path::LxFilePath; +use lazy_static::lazy_static; +use std::path::PathBuf; +use vec_like::SmallVecSet; + +lazy_static! { + pub static ref TRACKERS: LxFileMap = trackers(); +} + +pub struct LxAstTrackerExtended { + pub tracker: LxAstTracker<'static, LxDocumentInput<'static>>, + pub asts_over_tokens: Vec>, +} + +impl std::ops::Deref for LxAstTrackerExtended { + type Target = LxAstTracker<'static, LxDocumentInput<'static>>; + + fn deref(&self) -> &Self::Target { + &self.tracker + } +} + +// TODO: maybe use memo-like abstraction for this? +fn trackers() -> LxFileMap { + let dev_paths = HuskyLangDevPaths::new(); + let specs_dir = dev_paths.specs_dir(); + LX_FILE_STORAGE.file_map(|i, content| { + let file_path = LxFilePath::new(PathBuf::from(format!("lx-file-{i}",))); + let tracker = LxAstTracker::new(LxDocumentInput { + specs_dir: specs_dir.to_path_buf(), + file_path, + content, + }); + let asts_over_tokens = calc_asts_over_tokens(&tracker); + LxAstTrackerExtended { + tracker, + asts_over_tokens, + } + }) +} + +fn calc_asts_over_tokens( + tracker: &LxAstTracker<'static, LxDocumentInput<'static>>, +) -> Vec> { + // TODO: other lanes, and a data structure for token map + let mut asts_over_tokens: Vec> = + (0..tracker.token_storage.main_ranged_tokens().len()) + .into_iter() + .map(|_| Default::default()) + .collect(); + let LxAstTracker { + ast_arena, + ast_token_idx_range_map, + .. + } = tracker; + for ast_idx in ast_arena.all_asts() { + let token_idx_range = ast_token_idx_range_map[ast_idx]; + for token_idx in token_idx_range { + asts_over_tokens[token_idx.index()].insert(ast_idx); + } + } + asts_over_tokens +} + +#[test] +fn trackers_works() { + let trackers = trackers(); + assert_eq!(trackers.len(), LX_FILE_STORAGE.files().len()); +} + +pub(crate) fn all_asts_within_file(file_idx: LxFileIdx) -> impl Iterator { + let tracker = &TRACKERS[file_idx]; + tracker + .ast_arena + .all_asts() + .map(move |ast_idx| LxAstId { file_idx, ast_idx }) +} + +pub(crate) fn first_ast(file_idx: LxFileIdx) -> LxAstIdx { + let tracker = &TRACKERS[file_idx]; + tracker.asts_over_tokens[0][0] +} diff --git a/registry/latex-ast-hsy-0.1.0/target-rs/Cargo.lock b/registry/latex-ast-hsy-0.1.0/target-rs/Cargo.lock index 6bb12bbd95..d5eaf8ad4d 100644 --- a/registry/latex-ast-hsy-0.1.0/target-rs/Cargo.lock +++ b/registry/latex-ast-hsy-0.1.0/target-rs/Cargo.lock @@ -800,7 +800,16 @@ dependencies = [ name = "latex-ast-hsy" version = "0.1.0" dependencies = [ + "husky-core", + "husky-linket-impl", + "husky-path-utils", + "husky-standard-linket-impl", + "idx-arena", "latex-ast", + "latex-prelude", + "latex-vfs", + "lazy_static 1.5.0", + "vec-like", ] [[package]] diff --git a/registry/latex-ast-hsy-0.1.0/target-rs/latex-ast-hsy-linkets/src/lib.rs b/registry/latex-ast-hsy-0.1.0/target-rs/latex-ast-hsy-linkets/src/lib.rs index 0b2320528d..4867202ef3 100644 --- a/registry/latex-ast-hsy-0.1.0/target-rs/latex-ast-hsy-linkets/src/lib.rs +++ b/registry/latex-ast-hsy-0.1.0/target-rs/latex-ast-hsy-linkets/src/lib.rs @@ -4,6 +4,7 @@ use ad_hoc_devsoul_dependency::{*, ugly::*}; #[rustfmt::skip] linket_impls![ + static_var_linket_impl!(latex_ast_hsy::AST, latex_ast_hsy::__AST__ITEM_PATH_ID_INTERFACE), fn_linket_impl!(::abs), fn_linket_impl!(::max), fn_linket_impl!(>::add), diff --git a/registry/mnist-0.1.0/src/lib.rs b/registry/mnist-0.1.0/src/lib.rs index d4756839a4..b0036a72ef 100644 --- a/registry/mnist-0.1.0/src/lib.rs +++ b/registry/mnist-0.1.0/src/lib.rs @@ -165,7 +165,7 @@ impl __IsStaticVar<__VarId> for INPUT { } fn zones() -> &'static [__FigureZone] { - &[__FigureZone::Gallery] + &[__FigureZone::Parade] } } diff --git a/rustc-ice-2024-11-30T03_11_35-20356.txt b/rustc-ice-2024-11-30T03_11_35-20356.txt new file mode 100644 index 0000000000..fa63a70677 --- /dev/null +++ b/rustc-ice-2024-11-30T03_11_35-20356.txt @@ -0,0 +1,45 @@ +thread 'rustc' panicked at compiler/rustc_metadata/src/rmeta/def_path_hash_map.rs:23:54: +called `Option::unwrap()` on a `None` value +stack backtrace: + 0: 0x7a75824966e5 - std::backtrace::Backtrace::create::h0e78ea677463d3fd + 1: 0x7a7580bddd35 - std::backtrace::Backtrace::force_capture::hdaf715b2c6978242 + 2: 0x7a757fd5435e - std[4821b876adeec04f]::panicking::update_hook::>::{closure#0} + 3: 0x7a7580bf5ba7 - std::panicking::rust_panic_with_hook::hdf548254c8466072 + 4: 0x7a7580bf5833 - std::panicking::begin_panic_handler::{{closure}}::h3816939d6279b662 + 5: 0x7a7580bf3069 - std::sys::backtrace::__rust_end_short_backtrace::he8fc83e4c72749c8 + 6: 0x7a7580bf5534 - rust_begin_unwind + 7: 0x7a757da97b43 - core::panicking::panic_fmt::h7a006cece2943dea + 8: 0x7a757dc725cc - core::panicking::panic::hb3c7ea25df633151 + 9: 0x7a757e054db9 - core::option::unwrap_failed::hf05a1feec3e91ee0 + 10: 0x7a75815aa3b1 - ::extract_def_id + 11: 0x7a75821eb360 - rustc_query_impl[b7cf2626c3b456b5]::plumbing::force_from_dep_node::>, false, false, false>> + 12: 0x7a75821eb22d - ::{closure#0} as core[3a188adb88b8af3f]::ops::function::FnOnce<(rustc_middle[177a089697687a0f]::ty::context::TyCtxt, rustc_query_system[8ccef4992b07fb90]::dep_graph::dep_node::DepNode)>>::call_once + 13: 0x7a75815e9d1f - >::try_mark_previous_green:: + 14: 0x7a75815e9c8f - >::try_mark_previous_green:: + 15: 0x7a75815e9c8f - >::try_mark_previous_green:: + 16: 0x7a75815e9c8f - >::try_mark_previous_green:: + 17: 0x7a75815e9c8f - >::try_mark_previous_green:: + 18: 0x7a7581623957 - rustc_query_system[8ccef4992b07fb90]::query::plumbing::try_execute_query::)>, rustc_middle[177a089697687a0f]::query::erase::Erased<[u8; 16usize]>>, false, false, false>, rustc_query_impl[b7cf2626c3b456b5]::plumbing::QueryCtxt, true> + 19: 0x7a7581622373 - rustc_query_impl[b7cf2626c3b456b5]::query_impl::fn_abi_of_instance::get_query_incr::__rust_end_short_backtrace + 20: 0x7a757e2aa260 - ::predefine_fn + 21: 0x7a75823068ff - rustc_codegen_llvm[f7f993617aa7612f]::base::compile_codegen_unit::module_codegen + 22: 0x7a75823e060d - ::compile_codegen_unit + 23: 0x7a75823dcc84 - ::codegen_crate + 24: 0x7a75823e5bf0 - ::codegen_and_build_linker + 25: 0x7a75821dc199 - rustc_interface[4e8b14457d10516f]::interface::run_compiler::, rustc_driver_impl[699cd2d3c3a41798]::run_compiler::{closure#0}>::{closure#1} + 26: 0x7a75822a9604 - std[4821b876adeec04f]::sys::backtrace::__rust_begin_short_backtrace::, rustc_driver_impl[699cd2d3c3a41798]::run_compiler::{closure#0}>::{closure#1}, core[3a188adb88b8af3f]::result::Result<(), rustc_span[617b2c4e116b8252]::ErrorGuaranteed>>::{closure#0}, core[3a188adb88b8af3f]::result::Result<(), rustc_span[617b2c4e116b8252]::ErrorGuaranteed>>::{closure#0}::{closure#0}, core[3a188adb88b8af3f]::result::Result<(), rustc_span[617b2c4e116b8252]::ErrorGuaranteed>> + 27: 0x7a75822a9c70 - <::spawn_unchecked_, rustc_driver_impl[699cd2d3c3a41798]::run_compiler::{closure#0}>::{closure#1}, core[3a188adb88b8af3f]::result::Result<(), rustc_span[617b2c4e116b8252]::ErrorGuaranteed>>::{closure#0}, core[3a188adb88b8af3f]::result::Result<(), rustc_span[617b2c4e116b8252]::ErrorGuaranteed>>::{closure#0}::{closure#0}, core[3a188adb88b8af3f]::result::Result<(), rustc_span[617b2c4e116b8252]::ErrorGuaranteed>>::{closure#1} as core[3a188adb88b8af3f]::ops::function::FnOnce<()>>::call_once::{shim:vtable#0} + 28: 0x7a75822a9feb - std::sys::pal::unix::thread::Thread::new::thread_start::h7ef170129820a8c9 + 29: 0x7a757c49ca94 - start_thread + at ./nptl/pthread_create.c:447:8 + 30: 0x7a757c529c3c - clone3 + at ./misc/../sysdeps/unix/sysv/linux/x86_64/clone3.S:78 + 31: 0x0 - + + +rustc version: 1.82.0-nightly (100fde524 2024-08-28) +platform: x86_64-unknown-linux-gnu + +query stack during panic: +#0 [fn_abi_of_instance] computing call ABI of `core::ptr::drop_in_place::> - shim(Some(husky_trace_protocol::synchrotron::action::TraceSynchrotronAction))` +end of query stack