Skip to content

Commit 4c2aa88

Browse files
tiiftiif
committed
Support constant in ValueExpression and Terminator::Switch
1 parent 55388d3 commit 4c2aa88

File tree

10 files changed

+524
-39
lines changed

10 files changed

+524
-39
lines changed

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -25,7 +25,7 @@ impl Check<'_> {
2525
in_env: &Env,
2626
in_assumptions: impl ToWcs,
2727
f: &Fn,
28-
crate_id: &CrateId
28+
crate_id: &CrateId,
2929
) -> Fallible<()> {
3030
let in_assumptions = in_assumptions.to_wcs();
3131

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -21,7 +21,7 @@ impl super::Check<'_> {
2121
pub(super) fn check_trait_impl(
2222
&self,
2323
trait_impl: &TraitImpl,
24-
crate_id: &CrateId
24+
crate_id: &CrateId,
2525
) -> Fallible<()> {
2626
let TraitImpl { binder, safety: _ } = trait_impl;
2727

@@ -126,7 +126,7 @@ impl super::Check<'_> {
126126
impl_assumptions: impl ToWcs,
127127
trait_items: &[TraitItem],
128128
ii_fn: &Fn,
129-
crate_id: &CrateId
129+
crate_id: &CrateId,
130130
) -> Fallible<()> {
131131
let impl_assumptions: Wcs = impl_assumptions.to_wcs();
132132
assert!(

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

Lines changed: 53 additions & 26 deletions
Original file line numberDiff line numberDiff line change
@@ -4,11 +4,12 @@ use formality_core::{Fallible, Map, Upcast};
44
use formality_prove::Env;
55
use formality_rust::grammar::minirust::ArgumentExpression::{ByValue, InPlace};
66
use formality_rust::grammar::minirust::PlaceExpression::Local;
7-
use formality_rust::grammar::minirust::ValueExpression::{Fn, Load};
7+
use formality_rust::grammar::minirust::ValueExpression::{Constant, Fn, Load};
88
use formality_rust::grammar::minirust::{
9-
self, ArgumentExpression, BasicBlock, BbId, LocalId, PlaceExpression, ValueExpression,
9+
self, ty_is_int, ArgumentExpression, BasicBlock, BbId, LocalId, PlaceExpression,
10+
ValueExpression,
1011
};
11-
use formality_rust::grammar::{FnBoundData};
12+
use formality_rust::grammar::FnBoundData;
1213
use formality_types::grammar::{CrateId, FnId};
1314
use formality_types::grammar::{Relation, Ty, Wcs};
1415

@@ -23,7 +24,7 @@ impl Check<'_> {
2324
fn_assumptions: &Wcs,
2425
body: minirust::Body,
2526
declared_input_tys: Vec<Ty>,
26-
crate_id: &CrateId
27+
crate_id: &CrateId,
2728
) -> Fallible<()> {
2829
// Type-check:
2930
//
@@ -219,6 +220,25 @@ impl Check<'_> {
219220
bail!("The return local variable has not been initialized.")
220221
}
221222
}
223+
224+
minirust::Terminator::Switch {
225+
switch_value,
226+
switch_targets,
227+
fallback,
228+
} => {
229+
// Check if the value is well-formed.
230+
let value_ty = self.check_value(typeck_env, switch_value).unwrap();
231+
232+
if !ty_is_int(value_ty) {
233+
bail!("The value used for switch must be an int.");
234+
}
235+
236+
// Ensure all bbid are valid.
237+
for switch_target in switch_targets {
238+
self.check_block_exists(typeck_env, &switch_target.target)?;
239+
}
240+
self.check_block_exists(typeck_env, fallback)?;
241+
}
222242
}
223243
Ok(())
224244
}
@@ -256,30 +276,32 @@ impl Check<'_> {
256276
Fn(fn_id) => {
257277
// Check if the function called is in declared in current crate.
258278

259-
// Find the crate that is currently being typeck.
260-
let curr_crate = self.program.crates.iter().find(|c| c.id == typeck_env.crate_id ).unwrap();
261-
262-
// Find the callee from current crate.
263-
let callee = curr_crate
264-
.items
279+
// Find the crate that is currently being typeck.
280+
let curr_crate = self
281+
.program
282+
.crates
265283
.iter()
266-
.find(|item| {
267-
match item {
268-
CrateItem::Fn(fn_declared) => {
269-
if fn_declared.id == *fn_id {
270-
let fn_bound_data =
271-
typeck_env.env.instantiate_universally(&fn_declared.binder);
272-
// Store the callee information in typeck_env, we will need this when type checking Terminator::Call.
273-
typeck_env
274-
.callee_input_tys
275-
.insert(fn_declared.id.clone(), fn_bound_data);
276-
return true;
277-
}
278-
false
284+
.find(|c| c.id == typeck_env.crate_id)
285+
.unwrap();
286+
287+
// Find the callee from current crate.
288+
let callee = curr_crate.items.iter().find(|item| {
289+
match item {
290+
CrateItem::Fn(fn_declared) => {
291+
if fn_declared.id == *fn_id {
292+
let fn_bound_data =
293+
typeck_env.env.instantiate_universally(&fn_declared.binder);
294+
// Store the callee information in typeck_env, we will need this when type checking Terminator::Call.
295+
typeck_env
296+
.callee_input_tys
297+
.insert(fn_declared.id.clone(), fn_bound_data);
298+
return true;
279299
}
280-
_ => false,
300+
false
281301
}
282-
});
302+
_ => false,
303+
}
304+
});
283305

284306
// If the callee is not found, return error.
285307
if callee.is_none() {
@@ -288,6 +310,11 @@ impl Check<'_> {
288310
value_ty = typeck_env.output_ty.clone();
289311
Ok(value_ty)
290312
}
313+
Constant(constant) => {
314+
// If the actual value overflows / does not match the type of the constant,
315+
// it will be rejected by the parser.
316+
Ok(constant.get_ty())
317+
}
291318
}
292319
}
293320

@@ -343,7 +370,7 @@ struct TypeckEnv {
343370
callee_input_tys: Map<FnId, FnBoundData>,
344371

345372
/// The id of the crate where this function resides.
346-
/// We need this to access information about other functions
373+
/// We need this to access information about other functions
347374
/// declared in the current crate.
348375
crate_id: CrateId,
349376
}

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -75,7 +75,7 @@ impl super::Check<'_> {
7575
env: &Env,
7676
where_clauses: &[WhereClause],
7777
f: &Fn,
78-
crate_id: &CrateId
78+
crate_id: &CrateId,
7979
) -> Fallible<()> {
8080
self.check_fn(env, where_clauses, f, crate_id)
8181
}

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

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -355,8 +355,15 @@ macro_rules! cast_impl {
355355
}
356356

357357
cast_impl!(usize);
358+
cast_impl!(u8);
359+
cast_impl!(u16);
358360
cast_impl!(u32);
359361
cast_impl!(u64);
362+
cast_impl!(i8);
363+
cast_impl!(i16);
364+
cast_impl!(i32);
365+
cast_impl!(i64);
366+
cast_impl!(isize);
360367
cast_impl!(String);
361368

362369
impl UpcastFrom<&str> for String {

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

Lines changed: 48 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -70,12 +70,60 @@ impl<L: Language> CoreFold<L> for usize {
7070
}
7171
}
7272

73+
impl<L: Language> CoreFold<L> for u8 {
74+
fn substitute(&self, _substitution_fn: SubstitutionFn<'_, L>) -> Self {
75+
*self
76+
}
77+
}
78+
79+
impl<L: Language> CoreFold<L> for u16 {
80+
fn substitute(&self, _substitution_fn: SubstitutionFn<'_, L>) -> Self {
81+
*self
82+
}
83+
}
84+
7385
impl<L: Language> CoreFold<L> for u32 {
7486
fn substitute(&self, _substitution_fn: SubstitutionFn<'_, L>) -> Self {
7587
*self
7688
}
7789
}
7890

91+
impl<L: Language> CoreFold<L> for u64 {
92+
fn substitute(&self, _substitution_fn: SubstitutionFn<'_, L>) -> Self {
93+
*self
94+
}
95+
}
96+
97+
impl<L: Language> CoreFold<L> for i8 {
98+
fn substitute(&self, _substitution_fn: SubstitutionFn<'_, L>) -> Self {
99+
*self
100+
}
101+
}
102+
103+
impl<L: Language> CoreFold<L> for i16 {
104+
fn substitute(&self, _substitution_fn: SubstitutionFn<'_, L>) -> Self {
105+
*self
106+
}
107+
}
108+
109+
impl<L: Language> CoreFold<L> for i32 {
110+
fn substitute(&self, _substitution_fn: SubstitutionFn<'_, L>) -> Self {
111+
*self
112+
}
113+
}
114+
115+
impl<L: Language> CoreFold<L> for i64 {
116+
fn substitute(&self, _substitution_fn: SubstitutionFn<'_, L>) -> Self {
117+
*self
118+
}
119+
}
120+
121+
impl<L: Language> CoreFold<L> for isize {
122+
fn substitute(&self, _substitution_fn: SubstitutionFn<'_, L>) -> Self {
123+
*self
124+
}
125+
}
126+
79127
impl<L: Language> CoreFold<L> for () {
80128
fn substitute(&self, _substitution_fn: SubstitutionFn<'_, L>) -> Self {}
81129
}

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

Lines changed: 63 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -361,6 +361,24 @@ where
361361
}
362362
}
363363

364+
impl<L> CoreParse<L> for u8
365+
where
366+
L: Language,
367+
{
368+
fn parse<'t>(scope: &Scope<L>, text: &'t str) -> ParseResult<'t, Self> {
369+
Parser::single_variant(scope, text, "u8", |p| p.number())
370+
}
371+
}
372+
373+
impl<L> CoreParse<L> for u16
374+
where
375+
L: Language,
376+
{
377+
fn parse<'t>(scope: &Scope<L>, text: &'t str) -> ParseResult<'t, Self> {
378+
Parser::single_variant(scope, text, "u16", |p| p.number())
379+
}
380+
}
381+
364382
impl<L> CoreParse<L> for u32
365383
where
366384
L: Language,
@@ -379,6 +397,51 @@ where
379397
}
380398
}
381399

400+
impl<L> CoreParse<L> for i8
401+
where
402+
L: Language,
403+
{
404+
fn parse<'t>(scope: &Scope<L>, text: &'t str) -> ParseResult<'t, Self> {
405+
Parser::single_variant(scope, text, "u16", |p| p.number())
406+
}
407+
}
408+
409+
impl<L> CoreParse<L> for i16
410+
where
411+
L: Language,
412+
{
413+
fn parse<'t>(scope: &Scope<L>, text: &'t str) -> ParseResult<'t, Self> {
414+
Parser::single_variant(scope, text, "u16", |p| p.number())
415+
}
416+
}
417+
418+
impl<L> CoreParse<L> for i32
419+
where
420+
L: Language,
421+
{
422+
fn parse<'t>(scope: &Scope<L>, text: &'t str) -> ParseResult<'t, Self> {
423+
Parser::single_variant(scope, text, "u16", |p| p.number())
424+
}
425+
}
426+
427+
impl<L> CoreParse<L> for i64
428+
where
429+
L: Language,
430+
{
431+
fn parse<'t>(scope: &Scope<L>, text: &'t str) -> ParseResult<'t, Self> {
432+
Parser::single_variant(scope, text, "u16", |p| p.number())
433+
}
434+
}
435+
436+
impl<L> CoreParse<L> for isize
437+
where
438+
L: Language,
439+
{
440+
fn parse<'t>(scope: &Scope<L>, text: &'t str) -> ParseResult<'t, Self> {
441+
Parser::single_variant(scope, text, "u16", |p| p.number())
442+
}
443+
}
444+
382445
impl<L: Language> CoreParse<L> for () {
383446
fn parse<'t>(scope: &Scope<L>, text: &'t str) -> ParseResult<'t, Self> {
384447
Parser::single_variant(scope, text, "`()`", |p| {

0 commit comments

Comments
 (0)