Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 2 additions & 0 deletions lsp/tree-sitter-vine/grammar.js
Original file line number Diff line number Diff line change
Expand Up @@ -584,6 +584,7 @@ module.exports = grammar({
$.chain_deref,
$.chain_inverse,
$.chain_as,
$.chain_index,
),

chain_unwrap: $ => "!",
Expand All @@ -595,6 +596,7 @@ module.exports = grammar({
chain_deref: $ => seq(".", "*"),
chain_inverse: $ => seq(".", "~"),
chain_as: $ => seq(".", "as", "[", $._ty, "]"),
chain_index: $ => seq(".", "[", $._expr, "]"),

string: $ =>
seq(
Expand Down
14 changes: 13 additions & 1 deletion root/data/Array.vi
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@

use ops::{Cast, comparison::Eq};
use ops::{Cast, Index::{Index, IndexPlace, IndexSpace, IndexValue}, comparison::Eq};

/// A contiguous, indexed collection of `T`.
///
Expand Down Expand Up @@ -432,6 +432,18 @@ pub mod Array {
Show::Constructor("Array", self.&.as[&List].*.show())
}
}

pub impl [T]: Index[Array[T], N32, T] {}

pub impl [T]: IndexPlace[Array[T], N32, T] {
fn assume_at(&self: &Array[T], index: N32) -> &T {
self.at(index).assume()
}
}

pub impl [T?]: IndexSpace[Array[T], N32, T];

pub impl [T+]: IndexValue[Array[T], N32, T];
}

/// The internal tree structure of an array.
Expand Down
28 changes: 27 additions & 1 deletion root/data/Map.vi
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@

use data::Iterator::{Iterator, Collect};
use ops::{Cast, Concat, comparison::Ord};
use ops::{Cast, Concat, Index::{Index, IndexPlace, IndexSpace, IndexValue}, comparison::Ord};

pub struct* Map[K, V](Set[(K, V)]);

Expand Down Expand Up @@ -108,6 +108,32 @@ pub mod Map[K, V; Ord[K]] {
))
}

pub impl index[K, V]: Index[Map[K, V], K, V] {}

pub impl index_value[K?, V+; Ord[K]]: IndexValue[Map[K, V], K, V];

pub impl index_place[K?, V; Ord[K]]: IndexPlace[Map[K, V], K, V] {
fn assume_at(&self: &Map[K, V], key: K) -> &V {
self.at(&key).assume()
}
}

pub impl index_space[K?, V?; Ord[K]]: IndexSpace[Map[K, V], K, V] {
fn assume_set(&self: &Map[K, V], key: K, value: V) {
self.insert(key, value);
}
}

pub impl index_ref[K, V]: Index[Map[K, V], &K, V] {}

pub impl index_value_ref[K+, V+; Ord[K]]: IndexValue[Map[K, V], &K, V];

pub impl index_place_ref[K, V; Ord[K]]: IndexPlace[Map[K, V], &K, V] {
fn assume_at(&self: &Map[K, V], &key: &K) -> &V {
self.at(&key).assume()
}
}

pub impl iter_ref[...]: Cast[&Map[K, V], IterRef[K, V]] {
fn cast(&self: &Map[K, V]) -> IterRef[K, V] {
IterRef(self!.iter_ref())
Expand Down
36 changes: 36 additions & 0 deletions root/ops/Index.vi
Original file line number Diff line number Diff line change
@@ -0,0 +1,36 @@

#[builtin = "Index"]
pub trait Index[T, K, V] {}

#[builtin = "IndexValue"]
pub trait IndexValue[T, K, V] {
fn .assume_get(self: &T, key: K) -> V;
}

pub mod IndexValue {
#[basic]
pub impl by_place[T, K, V+; IndexPlace[T, K, V]]: IndexValue[T, K, V] {
fn assume_get(&self: &T, key: K) -> V {
*self.assume_at(key)
}
}
}

#[builtin = "IndexSpace"]
pub trait IndexSpace[T, K, V] {
fn .assume_set(self: &T, key: K, value: V);
}

pub mod IndexSpace {
#[basic]
pub impl by_place[T, K, V?; IndexPlace[T, K, V]]: IndexSpace[T, K, V] {
fn assume_set(&self: &T, key: K, value: V) {
*self.assume_at(key) = value;
}
}
}

#[builtin = "IndexPlace"]
pub trait IndexPlace[T, K, V] {
fn .assume_at(self: &T, key: K) -> &V;
}
1 change: 1 addition & 0 deletions root/ops/ops.vi
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,7 @@ pub mod bitwise;
pub mod comparison;
pub mod elementwise;
pub mod flex;
pub mod Index;
pub mod Range;

pub trait Concat[A, B, O] {
Expand Down
18 changes: 18 additions & 0 deletions tests/programs/repl/index.vi
Original file line number Diff line number Diff line change
@@ -0,0 +1,18 @@

use #root::data::{Array, Map};

let words = ["i", "have", "a", "dream"] as Array
words.[0]
words.[1]
words.[2]
words.[3]
words.[0] = "I"
words.[3] ++= "."
/clear words

let foods = Map::empty[String, String]
foods.["chicken"] = "tasty"
foods.["broccoli"] = "healthy"
foods.[&"broccoli"] ++= " and colorful"
foods.["chicken"]
foods.[&"chicken"]
75 changes: 75 additions & 0 deletions tests/snaps/vine/repl/index.repl.vi
Original file line number Diff line number Diff line change
@@ -0,0 +1,75 @@

let io: IO = <IO>;
>

let io: IO = <IO>;
> use #root::data::{Array, Map};

let io: IO = <IO>;
>

let io: IO = <IO>;
> let words = ["i", "have", "a", "dream"] as Array

let io: IO = <IO>;
let words: Array[String] = Array(["i", "have", "a", "dream"]);
> words.[0]
"i"

let io: IO = <IO>;
let words: Array[String] = Array(["i", "have", "a", "dream"]);
> words.[1]
"have"

let io: IO = <IO>;
let words: Array[String] = Array(["i", "have", "a", "dream"]);
> words.[2]
"a"

let io: IO = <IO>;
let words: Array[String] = Array(["i", "have", "a", "dream"]);
> words.[3]
"dream"

let io: IO = <IO>;
let words: Array[String] = Array(["i", "have", "a", "dream"]);
> words.[0] = "I"

let io: IO = <IO>;
let words: Array[String] = Array(["I", "have", "a", "dream"]);
> words.[3] ++= "."

let io: IO = <IO>;
let words: Array[String] = Array(["I", "have", "a", "dream."]);
> /clear words

let io: IO = <IO>;
>

let io: IO = <IO>;
> let foods = Map::empty[String, String]

let io: IO = <IO>;
let foods: Map[String, String] = Map({});
> foods.["chicken"] = "tasty"

let io: IO = <IO>;
let foods: Map[String, String] = Map({ "chicken": "tasty" });
> foods.["broccoli"] = "healthy"

let io: IO = <IO>;
let foods: Map[String, String] = Map({ "broccoli": "healthy", "chicken": "tasty" });
> foods.[&"broccoli"] ++= " and colorful"

let io: IO = <IO>;
let foods: Map[String, String] = Map({ "broccoli": "healthy and colorful", "chicken": "tasty" });
> foods.["chicken"]
"tasty"

let io: IO = <IO>;
let foods: Map[String, String] = Map({ "broccoli": "healthy and colorful", "chicken": "tasty" });
> foods.[&"chicken"]
"tasty"

let io: IO = <IO>;
let foods: Map[String, String] = Map({ "broccoli": "healthy and colorful", "chicken": "tasty" });
1 change: 1 addition & 0 deletions tests/tests.rs
Original file line number Diff line number Diff line change
Expand Up @@ -163,6 +163,7 @@ fn tests(t: &mut DynTester) {
test_vi_repl(t, "tests/programs/repl/F64.vi");
test_vi_repl(t, "tests/programs/repl/heap.vi");
test_vi_repl(t, "tests/programs/repl/i32_misc.vi");
test_vi_repl(t, "tests/programs/repl/index.vi");
test_vi_repl(t, "tests/programs/repl/misc.vi");
test_vi_repl(t, "tests/programs/repl/N64.vi");
test_vi_repl(t, "tests/programs/repl/Nat.vi");
Expand Down
31 changes: 28 additions & 3 deletions vine/src/components/distiller.rs
Original file line number Diff line number Diff line change
Expand Up @@ -6,15 +6,17 @@ use vine_util::{
};

use crate::{
components::finder::FinderCache,
components::finder::{Finder, FinderCache},
structures::{
ast::Span,
chart::{Chart, DefId, GenericsId},
diag::{Diag, Diags, ErrorGuaranteed},
resolutions::{Fragment, Rels},
signatures::Signatures,
tir::{ClosureId, Local, TargetId, TirExpr, TirExprKind, TirLocal, TirPat, TirPatKind},
types::{Type, Types},
tir::{
ClosureId, Local, TargetId, TirExpr, TirExprKind, TirImpl, TirLocal, TirPat, TirPatKind,
},
types::{ImplType, Type, Types},
vir::{
Header, Interface, InterfaceId, InterfaceKind, Layer, LayerId, Port, Stage, StageId, Step,
Transfer, Vir, VirLocal,
Expand Down Expand Up @@ -196,6 +198,19 @@ impl<'r> Distiller<'r> {
local
}

pub(crate) fn find_impl(&mut self, span: Span, ty: &ImplType, basic: bool) -> TirImpl {
let mut finder = Finder::new(
self.chart,
self.sigs,
self.diags,
self.finder_cache,
self.def,
self.generics,
span,
);
finder.find_impl(&mut self.types, ty, basic)
}

pub(crate) fn distill_vec<T>(
&mut self,
stage: &mut Stage,
Expand Down Expand Up @@ -297,6 +312,9 @@ impl<'r> Distiller<'r> {
TirExprKind::Call(rel, receiver, args) => {
self.distill_expr_value_call(stage, span, ty, *rel, receiver, args)
}
TirExprKind::Index(expr, index) => {
self.distill_expr_value_index(stage, span, expr, index, ty)
}
TirExprKind::String(init, rest) => {
self.distill_expr_value_string(stage, span, ty, init, rest)
}
Expand Down Expand Up @@ -328,6 +346,9 @@ impl<'r> Distiller<'r> {
TirExprKind::Composite(elements) => {
self.distill_expr_space_composite(stage, span, ty, elements)
}
TirExprKind::Index(expr, index) => {
self.distill_expr_space_index(stage, span, expr, index, ty)
}
}
}

Expand All @@ -350,6 +371,9 @@ impl<'r> Distiller<'r> {
TirExprKind::Composite(elements) => {
self.distill_expr_place_composite(stage, span, ty, elements)
}
TirExprKind::Index(expr, index) => {
self.distill_expr_place_index(stage, span, expr, index, ty)
}
}
}

Expand All @@ -373,6 +397,7 @@ impl<'r> Distiller<'r> {
TirExprKind::Field(inner, index, fields) => {
self.distill_expr_poly_field(stage, span, ty, inner, *index, fields)
}
TirExprKind::Index(expr, index) => self.distill_expr_poly_index(stage, span, expr, index, ty),
}
}

Expand Down
5 changes: 5 additions & 0 deletions vine/src/components/parser.rs
Original file line number Diff line number Diff line change
Expand Up @@ -370,6 +370,11 @@ impl<'src> Parser<'src> {
self.expect(Token::CloseBracket)?;
return Ok(Ok(ExprKind::Cast(lhs, ty, true)));
}
if self.eat(Token::OpenBracket)? {
let index = self.parse_expr()?;
self.expect(Token::CloseBracket)?;
return Ok(Ok(ExprKind::Index(lhs, index)));
}
let ident_span = self.span();
let ident = self.parse_ident()?;
if self.check(Token::OpenBracket) || self.check(Token::OpenParen) {
Expand Down
1 change: 1 addition & 0 deletions vine/src/components/resolver.rs
Original file line number Diff line number Diff line change
Expand Up @@ -517,6 +517,7 @@ impl<'a> Resolver<'a> {
}
ExprKind::ComparisonOp(init, cmps) => self.resolve_expr_comparison_op(span, init, cmps),
ExprKind::Cast(inner, to, _) => self.resolve_expr_cast(span, inner, to),
ExprKind::Index(expr, index) => self.resolve_expr_index(span, expr, index),
ExprKind::RangeExclusive(start, end) => {
self.resolve_expr_range(span, start.as_ref(), end.as_ref(), false)
}
Expand Down
1 change: 1 addition & 0 deletions vine/src/features.rs
Original file line number Diff line number Diff line change
Expand Up @@ -18,6 +18,7 @@ pub mod hole;
pub mod if_;
pub mod impl_;
pub mod import;
pub mod index;
pub mod inline_ivy;
pub mod inverse;
pub mod labels;
Expand Down
17 changes: 17 additions & 0 deletions vine/src/features/builtin.rs
Original file line number Diff line number Diff line change
Expand Up @@ -39,6 +39,10 @@ pub enum Builtin {
Drop,
Duplicate,
Erase,
Index,
IndexValue,
IndexSpace,
IndexPlace,
Range,
BoundUnbounded,
BoundInclusive,
Expand Down Expand Up @@ -104,6 +108,10 @@ impl Parser<'_> {
"Drop" => Builtin::Drop,
"duplicate" => Builtin::Duplicate,
"erase" => Builtin::Erase,
"Index" => Builtin::Index,
"IndexValue" => Builtin::IndexValue,
"IndexSpace" => Builtin::IndexSpace,
"IndexPlace" => Builtin::IndexPlace,
"Range" => Builtin::Range,
"BoundUnbounded" => Builtin::BoundUnbounded,
"BoundInclusive" => Builtin::BoundInclusive,
Expand Down Expand Up @@ -157,6 +165,11 @@ pub struct Builtins {
pub duplicate: Option<ImplId>,
pub erase: Option<ImplId>,

pub index: Option<TraitId>,
pub index_value: Option<TraitId>,
pub index_space: Option<TraitId>,
pub index_place: Option<TraitId>,

pub range: Option<StructId>,
pub bound_exclusive: Option<StructId>,
pub bound_inclusive: Option<StructId>,
Expand Down Expand Up @@ -241,6 +254,10 @@ impl Charter<'_> {
Builtin::BoolNot => set(&mut builtins.bool_not, impl_id),
Builtin::BinaryOp(op) => set(builtins.binary_ops.entry(op).or_default(), fn_id),
Builtin::ComparisonOp(op) => set(builtins.comparison_ops.entry(op).or_default(), fn_id),
Builtin::Index => set(&mut builtins.index, trait_id),
Builtin::IndexValue => set(&mut builtins.index_value, trait_id),
Builtin::IndexSpace => set(&mut builtins.index_space, trait_id),
Builtin::IndexPlace => set(&mut builtins.index_place, trait_id),
Builtin::Range => set(&mut builtins.range, struct_id),
Builtin::BoundUnbounded => set(&mut builtins.bound_unbounded, struct_id),
Builtin::BoundExclusive => set(&mut builtins.bound_exclusive, struct_id),
Expand Down
Loading