Skip to content

Commit e27651e

Browse files
committed
Add parsing for integer and boolean scalars
1 parent 3400b1a commit e27651e

File tree

3 files changed

+125
-0
lines changed

3 files changed

+125
-0
lines changed

chalk-integration/src/lowering.rs

+2
Original file line numberDiff line numberDiff line change
@@ -241,6 +241,7 @@ impl LowerProgram for Program {
241241
}
242242
Item::Impl(_) => continue,
243243
Item::Clause(_) => continue,
244+
Item::Scalar(_) => continue,
244245
};
245246
}
246247

@@ -357,6 +358,7 @@ impl LowerProgram for Program {
357358
Item::Clause(ref clause) => {
358359
custom_clauses.extend(clause.lower_clause(&empty_env)?);
359360
}
361+
Item::Scalar(_) => todo!("Implement this"),
360362
}
361363
}
362364

chalk-parse/src/ast.rs

+46
Original file line numberDiff line numberDiff line change
@@ -24,6 +24,8 @@ pub enum Item {
2424
TraitDefn(TraitDefn),
2525
Impl(Impl),
2626
Clause(Clause),
27+
Scalar(Scalar),
28+
// TODO: tuple
2729
}
2830

2931
#[derive(Clone, PartialEq, Eq, Debug)]
@@ -290,3 +292,47 @@ pub enum Goal {
290292
// Additional kinds of goals:
291293
Leaf(LeafGoal),
292294
}
295+
296+
#[derive(Clone, PartialEq, Eq, Debug)]
297+
/// This allows users to add arbitrary `A :- B` clauses into the
298+
/// logic; it has no equivalent in Rust, but it's useful for testing.
299+
pub struct Scalar {
300+
// Some scalars have names if we include variables...
301+
// TODO: review this
302+
pub name: Option<Identifier>,
303+
// Do we want to store the value too?
304+
// storing the value is simple if we're already parsing. TODO: is this useful?
305+
pub value: ScalarValue,
306+
}
307+
308+
#[derive(Clone, PartialEq, Eq, Debug)]
309+
/// The inner value and type of the scalar value.
310+
pub enum ScalarValue {
311+
Bool(bool),
312+
Char(char),
313+
Int(IntValue),
314+
Uint(UintValue),
315+
//Float(FloatValue),
316+
}
317+
318+
#[derive(Clone, PartialEq, Eq, Debug)]
319+
pub enum IntValue {
320+
// Is the size of an `isize` here tied to the `isize` of the host?
321+
Isize(isize),
322+
I8(i8),
323+
I16(i16),
324+
I32(i32),
325+
I64(i64),
326+
I128(i128),
327+
}
328+
329+
#[derive(Clone, PartialEq, Eq, Debug)]
330+
pub enum UintValue {
331+
// Is the size of an `usize` here tied to the `usize` of the host?
332+
Usize(usize),
333+
U8(u8),
334+
U16(u16),
335+
U32(u32),
336+
U64(u64),
337+
U128(u128),
338+
}

chalk-parse/src/parser.lalrpop

+77
Original file line numberDiff line numberDiff line change
@@ -17,6 +17,7 @@ Item: Option<Item> = {
1717
TraitDefn => Some(Item::TraitDefn(<>)),
1818
Impl => Some(Item::Impl(<>)),
1919
Clause => Some(Item::Clause(<>)),
20+
Scalar => Some(Item::Scalar(<>)),
2021
};
2122

2223
Comment: () = r"//.*";
@@ -217,6 +218,82 @@ Field: Field = {
217218
}
218219
};
219220

221+
Scalar: Scalar = {
222+
<s:ScalarValue> => Scalar { name: None, value: s },
223+
};
224+
225+
ScalarValue: ScalarValue = {
226+
<Boolean> => ScalarValue::Bool(<>),
227+
<Decimal> => <>,
228+
};
229+
230+
Boolean: bool = <"(true|false)"> => <> == "true";
231+
232+
Decimal: ScalarValue = <s:r"-?[0-9][0-9_]*((u|i)(8|16|32|64|128|size))?"> => {
233+
let mut negated = false;
234+
let mut digits = String::new();
235+
let mut end_type: Option<&str> = None;
236+
if s.chars().next().unwrap() == '-' {
237+
negated = true;
238+
digits.push('-');
239+
}
240+
for (i, c) in s.chars().enumerate().skip(negated as usize) {
241+
if c >= '0' && c <= '9' {
242+
digits.push(c);
243+
} else if c == 'i' || c == 'u' {
244+
end_type = Some(&s[i..]);
245+
break;
246+
}
247+
}
248+
if let Some(et) = end_type {
249+
// TODO: proper error handling here
250+
match et {
251+
"u8" => ScalarValue::Uint(UintValue::U8(
252+
digits.parse::<u8>().expect("failed to parse u8"),
253+
)),
254+
"u16" => ScalarValue::Uint(UintValue::U16(
255+
digits.parse::<u16>().expect("failed to parse u16"),
256+
)),
257+
"u32" => ScalarValue::Uint(UintValue::U32(
258+
digits.parse::<u32>().expect("failed to parse u32"),
259+
)),
260+
"u64" => ScalarValue::Uint(UintValue::U64(
261+
digits.parse::<u64>().expect("failed to parse u64"),
262+
)),
263+
"u128" => ScalarValue::Uint(UintValue::U128(
264+
digits.parse::<u128>().expect("failed to parse u128"),
265+
)),
266+
"usize" => ScalarValue::Uint(UintValue::Usize(
267+
digits.parse::<usize>().expect("failed to parse usize"),
268+
)),
269+
"i8" => ScalarValue::Int(IntValue::I8(
270+
digits.parse::<i8>().expect("failed to parse i8"),
271+
)),
272+
"i16" => ScalarValue::Int(IntValue::I16(
273+
digits.parse::<i16>().expect("failed to parse i16"),
274+
)),
275+
"i32" => ScalarValue::Int(IntValue::I32(
276+
digits.parse::<i32>().expect("failed to parse i32"),
277+
)),
278+
"i64" => ScalarValue::Int(IntValue::I64(
279+
digits.parse::<i64>().expect("failed to parse i64"),
280+
)),
281+
"i128" => ScalarValue::Int(IntValue::I128(
282+
digits.parse::<i128>().expect("failed to parse i128"),
283+
)),
284+
"isize" => ScalarValue::Int(IntValue::Isize(
285+
digits.parse::<isize>().expect("failed to parse isize"),
286+
)),
287+
otherwise => unreachable!("Unknown numeric type suffix found: `{}`", otherwise),
288+
}
289+
} else {
290+
// TODO: try various parsers/do whatever rustc does here
291+
ScalarValue::Uint(UintValue::U32(
292+
digits.parse::<u32>().expect("failed to parse u32"),
293+
))
294+
}
295+
};
296+
220297
Clause: Clause = {
221298
"forall" <pk:Angle<ParameterKind>> "{" <dg:DomainGoal> "if" <g:Comma<Goal1>> "}" => Clause {
222299
parameter_kinds: pk,

0 commit comments

Comments
 (0)