Compare commits
2 commits
25ddc837c1
...
50c86e18dc
Author | SHA1 | Date | |
---|---|---|---|
|
50c86e18dc | ||
|
60734cc9d1 |
|
@ -12,10 +12,10 @@ jobs:
|
||||||
outputs:
|
outputs:
|
||||||
cache-primary-key: ${{ steps.restore-deps.outputs.cache-primary-key }}
|
cache-primary-key: ${{ steps.restore-deps.outputs.cache-primary-key }}
|
||||||
steps:
|
steps:
|
||||||
- uses: https://code.forgejo.org/actions/checkout@v3
|
- uses: https://git.libre-chip.org/mirrors/checkout@v3
|
||||||
with:
|
with:
|
||||||
fetch-depth: 0
|
fetch-depth: 0
|
||||||
- uses: https://code.forgejo.org/actions/cache/restore@v3
|
- uses: https://git.libre-chip.org/mirrors/cache/restore@v3
|
||||||
id: restore-deps
|
id: restore-deps
|
||||||
with:
|
with:
|
||||||
path: deps
|
path: deps
|
||||||
|
@ -58,19 +58,19 @@ jobs:
|
||||||
- name: Get SymbiYosys
|
- name: Get SymbiYosys
|
||||||
if: steps.restore-deps.outputs.cache-hit != 'true'
|
if: steps.restore-deps.outputs.cache-hit != 'true'
|
||||||
run: |
|
run: |
|
||||||
git clone --depth=1 --branch=yosys-0.45 https://github.com/YosysHQ/sby.git deps/sby
|
git clone --depth=1 --branch=yosys-0.45 https://git.libre-chip.org/mirrors/sby deps/sby
|
||||||
- name: Build Z3
|
- name: Build Z3
|
||||||
if: steps.restore-deps.outputs.cache-hit != 'true'
|
if: steps.restore-deps.outputs.cache-hit != 'true'
|
||||||
run: |
|
run: |
|
||||||
git clone --depth=1 --recursive --branch=z3-4.13.3 https://github.com/Z3Prover/z3.git deps/z3
|
git clone --depth=1 --recursive --branch=z3-4.13.3 https://git.libre-chip.org/mirrors/z3 deps/z3
|
||||||
(cd deps/z3; PYTHON=python3 ./configure --prefix=/usr/local)
|
(cd deps/z3; PYTHON=python3 ./configure --prefix=/usr/local)
|
||||||
make -C deps/z3/build -j"$(nproc)"
|
make -C deps/z3/build -j"$(nproc)"
|
||||||
- name: Build Yosys
|
- name: Build Yosys
|
||||||
if: steps.restore-deps.outputs.cache-hit != 'true'
|
if: steps.restore-deps.outputs.cache-hit != 'true'
|
||||||
run: |
|
run: |
|
||||||
git clone --depth=1 --recursive --branch=0.45 https://github.com/YosysHQ/yosys.git deps/yosys
|
git clone --depth=1 --recursive --branch=0.45 https://git.libre-chip.org/mirrors/yosys deps/yosys
|
||||||
make -C deps/yosys -j"$(nproc)"
|
make -C deps/yosys -j"$(nproc)"
|
||||||
- uses: https://code.forgejo.org/actions/cache/save@v3
|
- uses: https://git.libre-chip.org/mirrors/cache/save@v3
|
||||||
if: steps.restore-deps.outputs.cache-hit != 'true'
|
if: steps.restore-deps.outputs.cache-hit != 'true'
|
||||||
with:
|
with:
|
||||||
path: deps
|
path: deps
|
||||||
|
|
|
@ -9,7 +9,7 @@ jobs:
|
||||||
runs-on: debian-12
|
runs-on: debian-12
|
||||||
needs: deps
|
needs: deps
|
||||||
steps:
|
steps:
|
||||||
- uses: https://code.forgejo.org/actions/checkout@v3
|
- uses: https://git.libre-chip.org/mirrors/checkout@v3
|
||||||
with:
|
with:
|
||||||
fetch-depth: 0
|
fetch-depth: 0
|
||||||
- run: |
|
- run: |
|
||||||
|
@ -41,7 +41,7 @@ jobs:
|
||||||
curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh -s -- -y --default-toolchain 1.82.0
|
curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh -s -- -y --default-toolchain 1.82.0
|
||||||
source "$HOME/.cargo/env"
|
source "$HOME/.cargo/env"
|
||||||
echo "$PATH" >> "$GITHUB_PATH"
|
echo "$PATH" >> "$GITHUB_PATH"
|
||||||
- uses: https://code.forgejo.org/actions/cache/restore@v3
|
- uses: https://git.libre-chip.org/mirrors/cache/restore@v3
|
||||||
with:
|
with:
|
||||||
path: deps
|
path: deps
|
||||||
key: ${{ needs.deps.outputs.cache-primary-key }}
|
key: ${{ needs.deps.outputs.cache-primary-key }}
|
||||||
|
@ -52,7 +52,7 @@ jobs:
|
||||||
make -C deps/yosys install
|
make -C deps/yosys install
|
||||||
export PATH="$(realpath deps/firtool/bin):$PATH"
|
export PATH="$(realpath deps/firtool/bin):$PATH"
|
||||||
echo "$PATH" >> "$GITHUB_PATH"
|
echo "$PATH" >> "$GITHUB_PATH"
|
||||||
- uses: https://github.com/Swatinem/rust-cache@v2
|
- uses: https://git.libre-chip.org/mirrors/rust-cache@v2
|
||||||
with:
|
with:
|
||||||
save-if: ${{ github.ref == 'refs/heads/master' }}
|
save-if: ${{ github.ref == 'refs/heads/master' }}
|
||||||
- run: cargo test
|
- run: cargo test
|
||||||
|
|
|
@ -3,7 +3,7 @@
|
||||||
|
|
||||||
use crate::{
|
use crate::{
|
||||||
expr::{
|
expr::{
|
||||||
ops::{ArrayIndex, ArrayLiteral, ExprPartialEq},
|
ops::{ArrayLiteral, ExprFromIterator, ExprIntoIterator, ExprPartialEq},
|
||||||
CastToBits, Expr, HdlPartialEq, ReduceBits, ToExpr,
|
CastToBits, Expr, HdlPartialEq, ReduceBits, ToExpr,
|
||||||
},
|
},
|
||||||
int::{Bool, DynSize, KnownSize, Size, SizeType, DYN_SIZE},
|
int::{Bool, DynSize, KnownSize, Size, SizeType, DYN_SIZE},
|
||||||
|
@ -15,7 +15,7 @@ use crate::{
|
||||||
},
|
},
|
||||||
util::ConstUsize,
|
util::ConstUsize,
|
||||||
};
|
};
|
||||||
use std::ops::Index;
|
use std::{iter::FusedIterator, ops::Index};
|
||||||
|
|
||||||
#[derive(Copy, Clone, PartialEq, Eq, Hash)]
|
#[derive(Copy, Clone, PartialEq, Eq, Hash)]
|
||||||
pub struct ArrayType<T: Type = CanonicalType, Len: Size = DynSize> {
|
pub struct ArrayType<T: Type = CanonicalType, Len: Size = DynSize> {
|
||||||
|
@ -151,10 +151,8 @@ impl<T: Type, Len: Size> Type for ArrayType<T, Len> {
|
||||||
this: Expr<Self>,
|
this: Expr<Self>,
|
||||||
source_location: SourceLocation,
|
source_location: SourceLocation,
|
||||||
) -> Self::MatchVariantsIter {
|
) -> Self::MatchVariantsIter {
|
||||||
let base = Expr::as_dyn_array(this);
|
|
||||||
let base_ty = Expr::ty(base);
|
|
||||||
let _ = source_location;
|
let _ = source_location;
|
||||||
let retval = Vec::from_iter((0..base_ty.len()).map(|i| ArrayIndex::new(base, i).to_expr()));
|
let retval = Vec::from_iter(this);
|
||||||
std::iter::once(MatchVariantWithoutScope(
|
std::iter::once(MatchVariantWithoutScope(
|
||||||
Len::ArrayMatch::<T>::try_from(retval)
|
Len::ArrayMatch::<T>::try_from(retval)
|
||||||
.ok()
|
.ok()
|
||||||
|
@ -187,9 +185,7 @@ impl<T: Type, Len: Size> Type for ArrayType<T, Len> {
|
||||||
|
|
||||||
impl<T: Type, Len: Size> TypeWithDeref for ArrayType<T, Len> {
|
impl<T: Type, Len: Size> TypeWithDeref for ArrayType<T, Len> {
|
||||||
fn expr_deref(this: &Expr<Self>) -> &Self::MatchVariant {
|
fn expr_deref(this: &Expr<Self>) -> &Self::MatchVariant {
|
||||||
let base = Expr::as_dyn_array(*this);
|
let retval = Vec::from_iter(*this);
|
||||||
let base_ty = Expr::ty(base);
|
|
||||||
let retval = Vec::from_iter((0..base_ty.len()).map(|i| ArrayIndex::new(base, i).to_expr()));
|
|
||||||
Interned::into_inner(Intern::intern_sized(
|
Interned::into_inner(Intern::intern_sized(
|
||||||
Len::ArrayMatch::<T>::try_from(retval)
|
Len::ArrayMatch::<T>::try_from(retval)
|
||||||
.ok()
|
.ok()
|
||||||
|
@ -230,27 +226,122 @@ where
|
||||||
let lhs_ty = Expr::ty(lhs);
|
let lhs_ty = Expr::ty(lhs);
|
||||||
let rhs_ty = Expr::ty(rhs);
|
let rhs_ty = Expr::ty(rhs);
|
||||||
assert_eq!(lhs_ty.len(), rhs_ty.len());
|
assert_eq!(lhs_ty.len(), rhs_ty.len());
|
||||||
ArrayLiteral::<Bool, DynSize>::new(
|
lhs.into_iter()
|
||||||
Bool,
|
.zip(rhs)
|
||||||
(0..lhs_ty.len())
|
.map(|(l, r)| l.cmp_eq(r))
|
||||||
.map(|i| Expr::canonical(lhs[i].cmp_eq(rhs[i])))
|
.collect::<Expr<Array<Bool>>>()
|
||||||
.collect(),
|
.cast_to_bits()
|
||||||
)
|
.all_one_bits()
|
||||||
.cast_to_bits()
|
|
||||||
.all_one_bits()
|
|
||||||
}
|
}
|
||||||
|
|
||||||
fn cmp_ne(lhs: Expr<Self>, rhs: Expr<ArrayType<Rhs, Len>>) -> Expr<Bool> {
|
fn cmp_ne(lhs: Expr<Self>, rhs: Expr<ArrayType<Rhs, Len>>) -> Expr<Bool> {
|
||||||
let lhs_ty = Expr::ty(lhs);
|
let lhs_ty = Expr::ty(lhs);
|
||||||
let rhs_ty = Expr::ty(rhs);
|
let rhs_ty = Expr::ty(rhs);
|
||||||
assert_eq!(lhs_ty.len(), rhs_ty.len());
|
assert_eq!(lhs_ty.len(), rhs_ty.len());
|
||||||
ArrayLiteral::<Bool, DynSize>::new(
|
lhs.into_iter()
|
||||||
Bool,
|
.zip(rhs)
|
||||||
(0..lhs_ty.len())
|
.map(|(l, r)| l.cmp_ne(r))
|
||||||
.map(|i| Expr::canonical(lhs[i].cmp_ne(rhs[i])))
|
.collect::<Expr<Array<Bool>>>()
|
||||||
.collect(),
|
.cast_to_bits()
|
||||||
)
|
.any_one_bits()
|
||||||
.cast_to_bits()
|
}
|
||||||
.any_one_bits()
|
}
|
||||||
|
|
||||||
|
impl<T: Type, Len: Size> ExprIntoIterator for ArrayType<T, Len> {
|
||||||
|
type Item = T;
|
||||||
|
type ExprIntoIter = ExprArrayIter<T, Len>;
|
||||||
|
|
||||||
|
fn expr_into_iter(e: Expr<Self>) -> Self::ExprIntoIter {
|
||||||
|
ExprArrayIter {
|
||||||
|
base: e,
|
||||||
|
indexes: 0..Expr::ty(e).len(),
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
#[derive(Clone, Debug)]
|
||||||
|
pub struct ExprArrayIter<T: Type, Len: Size> {
|
||||||
|
base: Expr<ArrayType<T, Len>>,
|
||||||
|
indexes: std::ops::Range<usize>,
|
||||||
|
}
|
||||||
|
|
||||||
|
impl<T: Type, Len: Size> ExprArrayIter<T, Len> {
|
||||||
|
pub fn base(&self) -> Expr<ArrayType<T, Len>> {
|
||||||
|
self.base
|
||||||
|
}
|
||||||
|
pub fn indexes(&self) -> std::ops::Range<usize> {
|
||||||
|
self.indexes.clone()
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
impl<T: Type, Len: Size> Iterator for ExprArrayIter<T, Len> {
|
||||||
|
type Item = Expr<T>;
|
||||||
|
|
||||||
|
fn next(&mut self) -> Option<Self::Item> {
|
||||||
|
self.indexes.next().map(|i| self.base[i])
|
||||||
|
}
|
||||||
|
|
||||||
|
fn size_hint(&self) -> (usize, Option<usize>) {
|
||||||
|
self.indexes.size_hint()
|
||||||
|
}
|
||||||
|
|
||||||
|
fn count(self) -> usize {
|
||||||
|
self.indexes.count()
|
||||||
|
}
|
||||||
|
|
||||||
|
fn last(mut self) -> Option<Self::Item> {
|
||||||
|
self.next_back()
|
||||||
|
}
|
||||||
|
|
||||||
|
fn nth(&mut self, n: usize) -> Option<Self::Item> {
|
||||||
|
self.indexes.nth(n).map(|i| self.base[i])
|
||||||
|
}
|
||||||
|
|
||||||
|
fn fold<B, F>(self, init: B, mut f: F) -> B
|
||||||
|
where
|
||||||
|
F: FnMut(B, Self::Item) -> B,
|
||||||
|
{
|
||||||
|
self.indexes.fold(init, |b, i| f(b, self.base[i]))
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
impl<T: Type, Len: Size> DoubleEndedIterator for ExprArrayIter<T, Len> {
|
||||||
|
fn next_back(&mut self) -> Option<Self::Item> {
|
||||||
|
self.indexes.next_back().map(|i| self.base[i])
|
||||||
|
}
|
||||||
|
|
||||||
|
fn nth_back(&mut self, n: usize) -> Option<Self::Item> {
|
||||||
|
self.indexes.nth_back(n).map(|i| self.base[i])
|
||||||
|
}
|
||||||
|
|
||||||
|
fn rfold<B, F>(self, init: B, mut f: F) -> B
|
||||||
|
where
|
||||||
|
F: FnMut(B, Self::Item) -> B,
|
||||||
|
{
|
||||||
|
self.indexes.rfold(init, |b, i| f(b, self.base[i]))
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
impl<T: Type, Len: Size> ExactSizeIterator for ExprArrayIter<T, Len> {
|
||||||
|
fn len(&self) -> usize {
|
||||||
|
self.indexes.len()
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
impl<T: Type, Len: Size> FusedIterator for ExprArrayIter<T, Len> {}
|
||||||
|
|
||||||
|
impl<A: StaticType> ExprFromIterator<Expr<A>> for Array<A> {
|
||||||
|
fn expr_from_iter<T: IntoIterator<Item = Expr<A>>>(iter: T) -> Expr<Self> {
|
||||||
|
ArrayLiteral::new(
|
||||||
|
A::TYPE,
|
||||||
|
iter.into_iter().map(|v| Expr::canonical(v)).collect(),
|
||||||
|
)
|
||||||
|
.to_expr()
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
impl<'a, A: StaticType> ExprFromIterator<&'a Expr<A>> for Array<A> {
|
||||||
|
fn expr_from_iter<T: IntoIterator<Item = &'a Expr<A>>>(iter: T) -> Expr<Self> {
|
||||||
|
iter.into_iter().copied().collect()
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
|
@ -2708,3 +2708,47 @@ impl<T: Type> ToExpr for Uninit<T> {
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
pub trait ExprIntoIterator: Type {
|
||||||
|
type Item: Type;
|
||||||
|
type ExprIntoIter: Iterator<Item = Expr<Self::Item>>;
|
||||||
|
|
||||||
|
fn expr_into_iter(e: Expr<Self>) -> Self::ExprIntoIter;
|
||||||
|
}
|
||||||
|
|
||||||
|
impl<T: ExprIntoIterator> IntoIterator for Expr<T> {
|
||||||
|
type Item = Expr<T::Item>;
|
||||||
|
type IntoIter = T::ExprIntoIter;
|
||||||
|
|
||||||
|
fn into_iter(self) -> Self::IntoIter {
|
||||||
|
T::expr_into_iter(self)
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
impl<T: ExprIntoIterator> IntoIterator for &'_ Expr<T> {
|
||||||
|
type Item = Expr<T::Item>;
|
||||||
|
type IntoIter = T::ExprIntoIter;
|
||||||
|
|
||||||
|
fn into_iter(self) -> Self::IntoIter {
|
||||||
|
T::expr_into_iter(*self)
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
impl<T: ExprIntoIterator> IntoIterator for &'_ mut Expr<T> {
|
||||||
|
type Item = Expr<T::Item>;
|
||||||
|
type IntoIter = T::ExprIntoIter;
|
||||||
|
|
||||||
|
fn into_iter(self) -> Self::IntoIter {
|
||||||
|
T::expr_into_iter(*self)
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
pub trait ExprFromIterator<A>: Type {
|
||||||
|
fn expr_from_iter<T: IntoIterator<Item = A>>(iter: T) -> Expr<Self>;
|
||||||
|
}
|
||||||
|
|
||||||
|
impl<This: ExprFromIterator<A>, A> FromIterator<A> for Expr<This> {
|
||||||
|
fn from_iter<T: IntoIterator<Item = A>>(iter: T) -> Self {
|
||||||
|
This::expr_from_iter(iter)
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
Loading…
Reference in a new issue