Merge pull request #354 from xiyuzhai/main

progress on visored

Cargo.toml

@@ -119,7 +119,7 @@ ena = "0.14.2"
 env_logger = "0.10"
 env_proxy = "0.4"
 epaint = { git = "https://github.com/xiyuzhai-husky-lang/egui.git" }
-expect-test = "1.4.1"
+expect-test = "1.5.0"
 futures = "0.3.28"
 futures-util = { version = "0.3", default-features = false, features = [
     "sink",
@@ -152,6 +152,7 @@ parking_lot = "0.12.1"
 paste = "1.0.6"
 pathdiff = "0.2.1"
 proc-macro2 = "1.0.86"
+ptree = "0.5.0"
 pyo3 = "0.22.3"
 quote = "1.0.37"
 rand = "0.8.4"
@@ -315,14 +316,12 @@ husky-ki = { path = "crates/ki/husky-ki" }
 husky-ki-repr = { path = "crates/ki/husky-ki-repr" }
 husky-ki-repr-interface = { path = "crates/ki/husky-ki-repr-interface" }
 # latex
-latex-annotation = { path = "crates/latex/latex-annotation" }
 latex-ast = { path = "crates/latex/latex-ast" }
 latex-command = { path = "crates/latex/latex-command" }
 latex-math-letter = { path = "crates/latex/latex-math-letter" }
 latex-math-opr = { path = "crates/latex/latex-math-opr" }
 latex-prelude = { path = "crates/latex/latex-prelude" }
 latex-sem-expr = { path = "crates/latex/latex-sem-expr" }
-latex-syn-expr = { path = "crates/latex/latex-syn-expr" }
 latex-text = { path = "crates/latex/latex-text" }
 latex-token = { path = "crates/latex/latex-token" }
 # lean
@@ -415,6 +414,7 @@ husky-screen-utils = { path = "crates/utils/husky-screen-utils" }
 husky-sha-utils = { path = "crates/utils/husky-sha-utils" }
 husky-sync-utils = { path = "crates/utils/husky-sync-utils" }
 husky-toml-utils = { path = "crates/utils/husky-toml-utils" }
+husky-tree-utils = { path = "crates/utils/husky-tree-utils" }
 husky-rng-utils = { path = "crates/utils/husky-rng-utils" }
 husky-unicode-symbols = { path = "crates/utils/husky-unicode-symbols" }
 husky-wild-utils = { path = "crates/utils/husky-wild-utils" }
@@ -427,13 +427,15 @@ husky-standard-value = { path = "crates/value/husky-standard-value" }
 husky-standard-value-macros = { path = "crates/value/husky-standard-value-macros" }
 husky-virtual-value = { path = "crates/value/husky-virtual-value" }
 # visored
+visored-annotation = { path = "crates/visored/visored-annotation" }
 visored-coword = { path = "crates/visored/visored-coword" }
 visored-hir-expr = { path = "crates/visored/visored-hir-expr" }
 visored-isabelle-hol-transpilation = { path = "crates/visored/visored-isabelle-hol-transpilation" }
 visored-lean-transpilation = { path = "crates/visored/visored-lean-transpilation" }
 visored-sem-expr = { path = "crates/visored/visored-sem-expr" }
+visored-syn-expr = { path = "crates/visored/visored-syn-expr" }
 visored-opr = { path = "crates/visored/visored-opr" }
-visored-zfs-ty = { path = "crates/visored/visored-zfs-ty" }
+visored-zfc-ty = { path = "crates/visored/visored-zfc-ty" }
 # vm
 husky-vm = { path = "crates/vm/husky-vm" }
 # vmir

crates/abstractions/idx-arena/src/arena_idx.rs

@@ -1,5 +1,5 @@
 use crate::*;
-use std::num::NonZeroU32;
+use std::{num::NonZeroU32, ops::AddAssign};
 
 pub struct ArenaIdx<T> {
     raw: NonZeroU32,
@@ -83,6 +83,12 @@ impl<T> Add<usize> for ArenaIdx<T> {
     }
 }
 
+impl<T> AddAssign<usize> for ArenaIdx<T> {
+    fn add_assign(&mut self, rhs: usize) {
+        *self = *self + rhs;
+    }
+}
+
 impl<T> Sub<Self> for ArenaIdx<T> {
     type Output = usize;
 
@@ -94,6 +100,7 @@ impl<T> Sub<Self> for ArenaIdx<T> {
 impl<T> std::ops::Sub<usize> for ArenaIdx<T> {
     type Output = Self;
 
+    #[track_caller]
     fn sub(self, rhs: usize) -> Self::Output {
         Self::new(self.index() - rhs)
     }

crates/abstractions/idx-arena/src/lib.rs

@@ -106,7 +106,7 @@ impl<T> IntoIterator for ArenaIdxRange<T> {
     type IntoIter = impl Iterator<Item = Self::Item>;
 
     fn into_iter(self) -> Self::IntoIter {
-        self.to_range().into_iter()
+        self.to_range()
     }
 }
 
@@ -129,6 +129,10 @@ impl<T> ArenaIdxRange<T> {
         self.end.index() - self.start.index()
     }
 
+    pub fn is_empty(&self) -> bool {
+        self.start == self.end
+    }
+
     pub fn start(&self) -> ArenaIdx<T> {
         self.start
     }
@@ -142,7 +146,11 @@ impl<T> ArenaIdxRange<T> {
     }
 
     pub fn last(&self) -> Option<ArenaIdx<T>> {
-        (self.start < self.end).then_some(self.end - 1)
+        if self.start < self.end {
+            Some(self.end - 1)
+        } else {
+            None
+        }
     }
 
     pub fn new_single(idx: ArenaIdx<T>) -> Self {

crates/abstractions/idx-arena/src/map.rs

@@ -92,6 +92,7 @@ impl<T, V> ArenaMap<T, V> {
         self.data[idx.index()].is_some()
     }
 
+    #[track_caller]
     pub fn get(&self, idx: ArenaIdx<T>) -> Option<&V> {
         match self.data[idx.index()] {
             Some(ref v) => Some(v),

crates/abstractions/salsa-macros/src/lib.rs

@@ -53,7 +53,7 @@ pub fn jar(args: TokenStream, input: TokenStream) -> TokenStream {
     jar::jar(args, input)
 }
 
-#[deprecated(note = "try using derive(DebugWithDb) instead")]
+// TODO: try using derive(DebugWithDb) instead
 #[proc_macro_attribute]
 pub fn derive_debug_with_db(args: TokenStream, input: TokenStream) -> TokenStream {
     debug_with_db::debug_with_db(args, input)

crates/abstractions/salsa/src/jar.rs

@@ -193,8 +193,9 @@ pub enum JarIndex {
     LxAstJar,
     LxCommandJar,
     // visored
-    VdZfsTypeJar,
+    VdZfcTypeJar,
     VdOprJar,
+    VdSynExprJar,
     VdSemExprJar,
     VdHirExprJar,
     VdLeanTranspilationJar,

crates/abstractions/shifted-unsigned-int/src/lib.rs

@@ -1,7 +1,7 @@
 #![feature(nonzero_ops)]
 use std::{
     num::{NonZeroU16, NonZeroU32, NonZeroU64, NonZeroU8, NonZeroUsize},
-    ops::{Add, AddAssign, Sub},
+    ops::{Add, AddAssign, Sub, SubAssign},
 };
 
 #[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
@@ -88,6 +88,13 @@ impl ShiftedU32 {
     }
 }
 
+impl From<i32> for ShiftedU32 {
+    fn from(value: i32) -> Self {
+        let value: u32 = value.try_into().unwrap();
+        ShiftedU32::from(value)
+    }
+}
+
 impl From<u32> for ShiftedU32 {
     fn from(value: u32) -> Self {
         debug_assert!(value + 1 < u32::MAX as u32);
@@ -120,12 +127,6 @@ impl ShiftedU32 {
     }
 }
 
-impl AddAssign<u32> for ShiftedU32 {
-    fn add_assign(&mut self, rhs: u32) {
-        self.0 = unsafe { NonZeroU32::new_unchecked(self.0.get() + rhs) }
-    }
-}
-
 impl Add<u32> for ShiftedU32 {
     type Output = Self;
 
@@ -156,6 +157,46 @@ impl Sub<usize> for ShiftedU32 {
     }
 }
 
+impl Sub<u32> for ShiftedU32 {
+    type Output = Self;
+    fn sub(self, rhs: u32) -> Self::Output {
+        self.checked_sub(rhs).unwrap()
+    }
+}
+
+impl Sub<i32> for ShiftedU32 {
+    type Output = Self;
+    fn sub(self, rhs: i32) -> Self::Output {
+        self.checked_sub(rhs.try_into().unwrap()).unwrap()
+    }
+}
+
+impl AddAssign<u32> for ShiftedU32 {
+    fn add_assign(&mut self, rhs: u32) {
+        self.0 = unsafe { NonZeroU32::new_unchecked(self.0.get() + rhs) }
+    }
+}
+
+impl AddAssign<usize> for ShiftedU32 {
+    fn add_assign(&mut self, rhs: usize) {
+        let rhs: u32 = rhs.try_into().unwrap();
+        *self += rhs
+    }
+}
+
+impl SubAssign<u32> for ShiftedU32 {
+    fn sub_assign(&mut self, rhs: u32) {
+        *self = *self - rhs;
+    }
+}
+
+impl SubAssign<usize> for ShiftedU32 {
+    fn sub_assign(&mut self, rhs: usize) {
+        let rhs: u32 = rhs.try_into().unwrap();
+        *self -= rhs;
+    }
+}
+
 #[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
 #[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
 #[cfg_attr(feature = "serde", serde(from = "usize", into = "usize"))]

crates/cybertron/cybertron/src/seq/idx.rs

@@ -94,7 +94,7 @@ where
         )
     }
 
-    pub fn nearest_left2(self) -> Seq<(Option2<(Idx, T)>)> {
+    pub fn nearest_left2(self) -> Seq<Option2<(Idx, T)>> {
         let ts = self.data();
         Seq::new(
             (0..ts.len())
@@ -128,7 +128,7 @@ where
 {
     (1..=i)
         .into_iter()
-        .filter_map(|j| ts[(i - j)].map(|t| (idx!(i - j), t)))
+        .filter_map(|j| ts[i - j].map(|t| (idx!(i - j), t)))
         .next()
 }
 
@@ -138,7 +138,7 @@ where
 {
     (1..=i)
         .into_iter()
-        .filter_map(|j| ts[(i - j)].map(|t| (idx!(i - j), t)))
+        .filter_map(|j| ts[i - j].map(|t| (idx!(i - j), t)))
         .collect()
 }
 

crates/devtime/husky-trace/src/token.rs

@@ -92,13 +92,13 @@ where
         let spaces_before: u32 = if token_idx.index() > 0 {
             let prev_text_range = self.ranged_token_sheet.token_text_range(token_idx - 1);
             if prev_text_range.start.line == text_range.end.line {
-                text_range.start.col.0 - prev_text_range.end.col.0
+                text_range.start.col.index32() - prev_text_range.end.col.index32()
             } else {
                 self.new_line_if_tokens_data_is_empty();
-                text_range.start.col.0
+                text_range.start.col.index32()
             }
         } else {
-            text_range.start.col.0
+            text_range.start.col.index32()
         };
         self.tokens_data.push(TraceViewTokenData::new(
             text.to_string(),

crates/hir/husky-hir-eager-expr/Cargo.toml

@@ -32,6 +32,8 @@ husky-text.workspace = true
 husky-token-data.workspace = true
 husky-token.workspace = true
 husky-regional-token.workspace = true
+# protocols
+husky-text-protocol.workspace = true
 # semantics
 husky-sem-expr.workspace = true
 husky-sem-opr.workspace = true

crates/hir/husky-hir-eager-expr/src/helpers/codespan.rs

@@ -17,6 +17,7 @@ use husky_sem_expr::{
     SemExprIdx, SemExprRegionData,
 };
 use husky_text::{HasText, Text};
+use husky_text_protocol::offset::TextOffsetRange;
 use husky_token::{RangedTokenSheet, TokenDb};
 use husky_vfs::path::module_path::ModulePath;
 
@@ -145,7 +146,7 @@ impl<'a> HirEagerExprCodespanEmitter<'a> {
 
 /// # getters
 impl<'a> HirEagerExprCodespanEmitter<'a> {
-    fn expr_offset_range(&self, expr: HirEagerExprIdx) -> std::ops::Range<usize> {
+    fn expr_offset_range(&self, expr: HirEagerExprIdx) -> TextOffsetRange {
         let expr: SemExprIdx = self
             .hir_eager_expr_source_map_data
             .hir_eager_to_sem_expr_idx(expr);

crates/latex/README.md

@@ -1,4 +1,4 @@
-# HuskyTex
+# LaTeX (the Husky version)
 
 In the normal language, text -> token -> ast -> syn expr -> sema expr.
 
@@ -8,15 +8,15 @@ Further text <--> token <--> ast is totally handled automatically.
 
 Basically, the user modify directly the asts.
 
-HuskyTex asts is centered around displayability, what looks the same is processed the same way.
+LaTex asts is centered around displayability, what looks the same is processed the same way.
 
-HuskyTex differs from LaTex in that
+We differs from the standard implementation of LaTex in that
 - greek letters like `α`, `β`, ... and special symbols like `∀`, `∃` are allowed for better readability;
 - `{...}` in math mode can be interpreted directly as set notation if the content inside doesn't begin with `_` or `^`;
 - all `/` is interpreted as fraction, and thus no fraction command is needed for faster typing;
 - ...
 
-However, HuskyTex is designed to be as backward-compatible with LaTex as possible for easier data acquirement.
+Our LaTex is designed to be as a limited yet more structured subset of LaTex as possible for easier data acquirement. It should yield meaningful error messages for AI agents to fix. We'll gradually add more features to it as we see fit.
 
 Modes:
 - root.