Skip to content

Commit 5e164d7

Browse files
nikomatsakisnikomatsakis
committed
change over to using formality-core
1 parent e5660f7 commit 5e164d7

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

75 files changed

+527
-2574
lines changed

‎Cargo.lock

Lines changed: 3 additions & 2 deletions
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

‎crates/formality-check/src/coherence.rs

Lines changed: 2 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,9 @@
11
use anyhow::bail;
22
use fn_error_context::context;
3+
use formality_core::Downcasted;
34
use formality_prove::Env;
45
use formality_rust::grammar::{Crate, NegTraitImpl, TraitImpl};
5-
use formality_types::{
6-
cast::Downcasted,
7-
grammar::{Fallible, Wc, Wcs},
8-
};
6+
use formality_types::grammar::{Fallible, Wc, Wcs};
97
use itertools::Itertools;
108

119
use crate::Check;

‎crates/formality-check/src/impls.rs

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,7 @@
11
use anyhow::bail;
22

33
use fn_error_context::context;
4+
use formality_core::Downcasted;
45
use formality_prove::Env;
56
use formality_rust::{
67
grammar::{
@@ -11,9 +12,8 @@ use formality_rust::{
1112
prove::ToWcs,
1213
};
1314
use formality_types::{
14-
cast::Downcasted,
1515
grammar::{Binder, Fallible, Relation, Substitution, Wcs},
16-
term::Term,
16+
rust::Term,
1717
};
1818

1919
impl super::Check<'_> {

‎crates/formality-check/src/where_clauses.rs

Lines changed: 2 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,13 +1,11 @@
11
use fn_error_context::context;
2+
use formality_core::Upcast;
23
use formality_prove::Env;
34
use formality_rust::{
45
grammar::{WhereClause, WhereClauseData},
56
prove::ToWcs,
67
};
7-
use formality_types::{
8-
cast::Upcast,
9-
grammar::{ConstData, Fallible, Parameter, Relation, TraitRef},
10-
};
8+
use formality_types::grammar::{ConstData, Fallible, Parameter, Relation, TraitRef};
119

1210
impl super::Check<'_> {
1311
pub(crate) fn prove_where_clauses_well_formed(

‎crates/formality-core/Cargo.toml

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -15,3 +15,6 @@ tracing-tree = { version = "0.2" }
1515
formality-macros = { path = "../formality-macros" }
1616
anyhow = "1.0.75"
1717
contracts = "0.6.3"
18+
19+
[dev-dependencies]
20+
expect-test = "1.4.1"

‎crates/formality-core/src/binder.rs

Lines changed: 15 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -40,7 +40,7 @@ impl<L: Language, T: CoreFold<L>> CoreBinder<L, T> {
4040
var_index: VarIndex { index },
4141
kind: *kind,
4242
};
43-
let new_bound_var = fresh_bound_var(*kind);
43+
let new_bound_var = CoreBoundVar::fresh(*kind);
4444
(new_bound_var, (old_bound_var, new_bound_var))
4545
})
4646
.unzip();
@@ -165,19 +165,21 @@ impl<L: Language, T: CoreFold<L>> CoreBinder<L, T> {
165165
}
166166
}
167167

168-
/// Creates a fresh bound var of the given kind that is not yet part of a binder.
169-
/// You can put this into a term and then use `Binder::new`.
170-
pub fn fresh_bound_var<L: Language>(kind: CoreKind<L>) -> CoreBoundVar<L> {
171-
lazy_static! {
172-
static ref COUNTER: AtomicUsize = AtomicUsize::new(0);
173-
}
168+
impl<L: Language> CoreBoundVar<L> {
169+
/// Creates a fresh bound var of the given kind that is not yet part of a binder.
170+
/// You can put this into a term and then use `Binder::new`.
171+
pub fn fresh(kind: CoreKind<L>) -> Self {
172+
lazy_static! {
173+
static ref COUNTER: AtomicUsize = AtomicUsize::new(0);
174+
}
174175

175-
let index = COUNTER.fetch_add(1, Ordering::SeqCst);
176-
let var_index = VarIndex { index };
177-
CoreBoundVar {
178-
debruijn: None,
179-
var_index,
180-
kind,
176+
let index = COUNTER.fetch_add(1, Ordering::SeqCst);
177+
let var_index = VarIndex { index };
178+
CoreBoundVar {
179+
debruijn: None,
180+
var_index,
181+
kind,
182+
}
181183
}
182184
}
183185

‎crates/formality-core/src/cast.rs

Lines changed: 14 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -295,13 +295,13 @@ where
295295
#[macro_export]
296296
macro_rules! cast_impl {
297297
($e:ident :: $v:ident ($u:ty)) => {
298-
impl $crate::cast::UpcastFrom<$u> for $e {
298+
impl $crate::UpcastFrom<$u> for $e {
299299
fn upcast_from(v: $u) -> $e {
300300
$e::$v(v)
301301
}
302302
}
303303

304-
impl $crate::cast::DowncastTo<$u> for $e {
304+
impl $crate::DowncastTo<$u> for $e {
305305
fn downcast_to(&self) -> Option<$u> {
306306
match self {
307307
$e::$v(u) => Some(Clone::clone(u)),
@@ -312,13 +312,13 @@ macro_rules! cast_impl {
312312
};
313313

314314
(impl($($p:tt)*) $e:ident ($($ep:tt)*) :: $v:ident ($u:ty)) => {
315-
impl<$($p)*> $crate::cast::UpcastFrom<$u> for $e<$($ep)*> {
315+
impl<$($p)*> $crate::UpcastFrom<$u> for $e<$($ep)*> {
316316
fn upcast_from(v: $u) -> $e<$($ep)*> {
317317
$e::$v(v)
318318
}
319319
}
320320

321-
impl<$($p)*> $crate::cast::DowncastTo<$u> for $e<$($ep)*> {
321+
impl<$($p)*> $crate::DowncastTo<$u> for $e<$($ep)*> {
322322
fn downcast_to(&self) -> Option<$u> {
323323
match self {
324324
$e::$v(u) => Some(Clone::clone(u)),
@@ -329,50 +329,50 @@ macro_rules! cast_impl {
329329
};
330330

331331
(impl($($p:tt)*) $t:ty) => {
332-
impl<$($p)*> $crate::cast::UpcastFrom<$t> for $t {
332+
impl<$($p)*> $crate::UpcastFrom<$t> for $t {
333333
fn upcast_from(v: $t) -> $t {
334334
v
335335
}
336336
}
337337

338-
impl<$($p)*> $crate::cast::DowncastTo<$t> for $t {
338+
impl<$($p)*> $crate::DowncastTo<$t> for $t {
339339
fn downcast_to(&self) -> Option<$t> {
340340
Some(Self::clone(self))
341341
}
342342
}
343343
};
344344

345345
($t:ty) => {
346-
impl $crate::cast::UpcastFrom<$t> for $t {
346+
impl $crate::UpcastFrom<$t> for $t {
347347
fn upcast_from(v: $t) -> $t {
348348
v
349349
}
350350
}
351351

352-
impl $crate::cast::DowncastTo<$t> for $t {
352+
impl $crate::DowncastTo<$t> for $t {
353353
fn downcast_to(&self) -> Option<$t> {
354354
Some(Self::clone(self))
355355
}
356356
}
357357
};
358358

359359
($(impl($($p:tt)*))? ($bot:ty) <: ($($mid:ty),*) <: ($top:ty)) => {
360-
impl$(<$($p)*>)? $crate::cast::UpcastFrom<$bot> for $top {
360+
impl$(<$($p)*>)? $crate::UpcastFrom<$bot> for $top {
361361
fn upcast_from(v: $bot) -> $top {
362362
$(
363-
let v: $mid = $crate::cast::Upcast::upcast(v);
363+
let v: $mid = $crate::Upcast::upcast(v);
364364
)*
365-
$crate::cast::Upcast::upcast(v)
365+
$crate::Upcast::upcast(v)
366366
}
367367
}
368368

369-
impl$(<$($p)*>)? $crate::cast::DowncastTo<$bot> for $top {
369+
impl$(<$($p)*>)? $crate::DowncastTo<$bot> for $top {
370370
fn downcast_to(&self) -> Option<$bot> {
371371
let v: &$top = self;
372372
$(
373-
let v: &$mid = &$crate::cast::DowncastFrom::downcast_from(v)?;
373+
let v: &$mid = &$crate::DowncastFrom::downcast_from(v)?;
374374
)*
375-
$crate::cast::DowncastFrom::downcast_from(v)
375+
$crate::DowncastFrom::downcast_from(v)
376376
}
377377
}
378378
};

‎crates/formality-core/src/collections.rs

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -11,11 +11,11 @@ pub type Set<E> = BTreeSet<E>;
1111
#[macro_export]
1212
macro_rules! set {
1313
() => {
14-
$crate::collections::Set::new()
14+
$crate::Set::new()
1515
};
1616

1717
($($t:tt)*) => {
18-
$crate::seq![$($t)*].into_iter().collect::<$crate::collections::Set<_>>()
18+
$crate::seq![$($t)*].into_iter().collect::<$crate::Set<_>>()
1919
};
2020
}
2121

‎crates/formality-types/src/judgment.rs renamed to ‎crates/formality-core/src/judgment.rs

Lines changed: 11 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
use std::{cell::RefCell, collections::BTreeSet, sync::Arc};
1+
use std::{cell::RefCell, collections::BTreeSet};
22

33
use crate::fixed_point::FixedPointStack;
44

@@ -7,13 +7,6 @@ mod test_reachable;
77

88
pub type JudgmentStack<J, O> = RefCell<FixedPointStack<J, BTreeSet<O>>>;
99

10-
type InferenceRuleClosure<I, O> = Arc<dyn Fn(&I) -> Vec<O> + Send>;
11-
12-
#[derive(Clone)]
13-
struct InferenceRule<I, O> {
14-
closure: InferenceRuleClosure<I, O>,
15-
}
16-
1710
#[macro_export]
1811
macro_rules! judgment_fn {
1912
(
@@ -26,7 +19,7 @@ macro_rules! judgment_fn {
2619
}
2720
) => {
2821
$(#[$attr])*
29-
$v fn $name($($input_name : impl $crate::cast::Upcast<$input_ty>),*) -> $crate::collections::Set<$output> {
22+
$v fn $name($($input_name : impl $crate::Upcast<$input_ty>),*) -> $crate::Set<$output> {
3023
#[derive(Ord, PartialOrd, Eq, PartialEq, Hash, Clone)]
3124
struct __JudgmentStruct($($input_ty),*);
3225

@@ -43,7 +36,7 @@ macro_rules! judgment_fn {
4336
}
4437
}
4538

46-
$(let $input_name: $input_ty = $crate::cast::Upcast::upcast($input_name);)*
39+
$(let $input_name: $input_ty = $crate::Upcast::upcast($input_name);)*
4740

4841
$(
4942
// Assertions are preconditions
@@ -60,7 +53,7 @@ macro_rules! judgment_fn {
6053

6154
$crate::fixed_point::fixed_point::<
6255
__JudgmentStruct,
63-
$crate::collections::Set<$output>,
56+
$crate::Set<$output>,
6457
>(
6558
// Tracing span:
6659
|input| {
@@ -87,7 +80,7 @@ macro_rules! judgment_fn {
8780

8881
// Next value:
8982
|input: __JudgmentStruct| {
90-
let mut output = $crate::collections::Set::new();
83+
let mut output = $crate::Set::new();
9184

9285
$crate::push_rules!(
9386
$name,
@@ -158,6 +151,7 @@ macro_rules! push_rules {
158151
// give the user a type error if the name they gave
159152
// in the conclusion is not the same as the name of the
160153
// function
154+
#[allow(dead_code)]
161155
struct WrongJudgmentNameInConclusion;
162156
const _: WrongJudgmentNameInConclusion = {
163157
let $judgment_name = WrongJudgmentNameInConclusion;
@@ -204,28 +198,28 @@ macro_rules! push_rules {
204198

205199
(@match inputs($in0:ident $($inputs:tt)*) patterns($pat0:ident : $ty0:ty, $($pats:tt)*) args $args:tt) => {
206200
{
207-
if let Some($pat0) = $crate::cast::Downcast::downcast::<$ty0>($in0) {
201+
if let Some($pat0) = $crate::Downcast::downcast::<$ty0>($in0) {
208202
$crate::push_rules!(@match inputs($($inputs)*) patterns($($pats)*) args $args);
209203
}
210204
}
211205
};
212206

213207
(@match inputs($in0:ident) patterns($pat0:ident : $ty0:ty) args $args:tt) => {
214208
{
215-
if let Some($pat0) = $crate::cast::Downcast::downcast::<$ty0>($in0) {
209+
if let Some($pat0) = $crate::Downcast::downcast::<$ty0>($in0) {
216210
$crate::push_rules!(@match inputs() patterns() args $args);
217211
}
218212
}
219213
};
220214

221215
(@match inputs($in0:ident $($inputs:tt)*) patterns($pat0:pat, $($pats:tt)*) args $args:tt) => {
222-
if let Some($pat0) = $crate::cast::Downcast::downcast(&$in0) {
216+
if let Some($pat0) = $crate::Downcast::downcast(&$in0) {
223217
$crate::push_rules!(@match inputs($($inputs)*) patterns($($pats)*) args $args);
224218
}
225219
};
226220

227221
(@match inputs($in0:ident) patterns($pat0:pat) args $args:tt) => {
228-
if let Some($pat0) = $crate::cast::Downcast::downcast(&$in0) {
222+
if let Some($pat0) = $crate::Downcast::downcast(&$in0) {
229223
$crate::push_rules!(@match inputs() patterns() args $args);
230224
}
231225
};
@@ -277,7 +271,7 @@ macro_rules! push_rules {
277271

278272
(@body ($judgment_name:ident, $rule_name:literal, $v:expr, $output:expr)) => {
279273
{
280-
let result = $crate::cast::Upcast::upcast($v);
274+
let result = $crate::Upcast::upcast($v);
281275
tracing::debug!("produced {:?} from rule {:?} in judgment {:?}", result, $rule_name, stringify!($judgment_name));
282276
$output.insert(result)
283277
}

‎crates/formality-types/src/judgment/test_filtered.rs renamed to ‎crates/formality-core/src/judgment/test_filtered.rs

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,16 +1,17 @@
11
#![cfg(test)]
22

33
use std::sync::Arc;
4-
5-
use formality_core::{term, test};
4+
use crate::cast_impl;
65

76
use crate::judgment_fn;
87

9-
#[term($edges)]
8+
#[derive(Ord, PartialOrd, Eq, PartialEq, Clone, Debug, Hash)]
109
struct Graph {
1110
edges: Vec<(u32, u32)>,
1211
}
1312

13+
cast_impl!(Graph);
14+
1415
impl Graph {
1516
fn successors(&self, n: u32) -> Vec<u32> {
1617
self.edges

0 commit comments

Comments
 (0)