Skip to content

Commit

Permalink
Support typed literals. (#1915)
Browse files Browse the repository at this point in the history
  • Loading branch information
@chriseth
chriseth authored Oct 21, 2024
1 parent 51dd71f commit b50a586
Show file tree
Hide file tree
Showing 7 changed files with 188 additions and 112 deletions.
14 changes: 13 additions & 1 deletion ast/src/parsed/display.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -709,7 +709,7 @@ impl<Ref: Display> Display for Expression<Ref> {
match self {
Expression::Reference(_, reference) => write!(f, "{reference}"),
Expression::PublicReference(_, name) => write!(f, ":{name}"),
Expression::Number(_, Number { value, .. }) => write!(f, "{value}"),
Expression::Number(_, n) => write!(f, "{n}"),
Expression::String(_, value) => write!(f, "{}", quote(value)),
Expression::Tuple(_, items) => write!(f, "({})", format_list(items)),
Expression::LambdaExpression(_, lambda) => write!(f, "{lambda}"),
Expand Down Expand Up @@ -759,6 +759,18 @@ impl Display for NamespacedPolynomialReference {
}
}

impl Display for Number {
fn fmt(&self, f: &mut Formatter<'_>) -> Result {
let Number { value, type_ } = self;
write!(f, "{value}")?;
match type_ {
Some(ty @ (Type::Int | Type::Fe | Type::Expr)) => write!(f, "_{ty}"),
Some(Type::TypeVar(_)) | None => Ok(()),
Some(_) => unreachable!(),
}
}
}

impl<E> Display for LambdaExpression<E>
where
E: Display + Precedence,
Expand Down
20 changes: 19 additions & 1 deletion parser/src/powdr.lalrpop
View file
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,8 @@ use crate::{ParserContext, unescape_string};
use powdr_parser_util::Error;
use std::sync::Arc;

use lalrpop_util::ParseError;

grammar(ctx: &ParserContext);

extern {
Expand Down Expand Up @@ -594,6 +596,7 @@ TermCommon<StructOption>: Box<Expression> = {
<start:@L> <g:GenericReference> <end:@R> => ctx.to_expr_with_source_ref(g, start, end),
<start:@L> <p:PublicIdentifier> <end:@R> => Box::new(Expression::PublicReference(ctx.source_ref(start, end), p)),
<start:@L> <value:Number> <end:@R> => ctx.to_expr_with_source_ref(Number {value: value.into(), type_: None}, start, end),
<start:@L> <number:TypedNumber> <end:@R> => { let (value, ty) = number; ctx.to_expr_with_source_ref(Number {value, type_: Some(ty)}, start, end) },
<start:@L> <s:StringLiteral> <end:@R> => Box::new(Expression::String(ctx.source_ref(start, end), s)),
MatchExpression,
IfExpression,
Expand Down Expand Up @@ -892,7 +895,22 @@ PublicIdentifier: String = {

Number: BigUint = {
r"[0-9][0-9_]*" => BigUint::from_str(&<>.replace('_', "")).unwrap().into(),
r"0x[0-9A-Fa-f][0-9A-Fa-f_]*" => BigUint::from_str_radix(&<>[2..].replace('_', ""), 16).unwrap().into(),
<start:@L> <v:r"0x[0-9A-Fa-f][0-9A-Fa-f_]*"> <end:@R> =>?
if v.ends_with("_fe") {
// It would be too easy to confuse e.g. 0x12_fe with the field element 0x12.
Err(ParseError::User{ error: ctx.source_ref(start, end).with_error("Hex literals cannot end in '_fe'.".to_string()) })
} else {
Ok(BigUint::from_str_radix(&v[2..].replace('_', ""), 16).unwrap().into())
},
}

TypedNumber: (BigUint, Type) = {
r"[0-9][0-9_]*_fe" => (BigUint::from_str(&<>.strip_suffix("_fe").unwrap().replace('_', "")).unwrap().into(), Type::Fe),
// No hex with _fe suffix for now, because 'fe' is valid hex.
r"[0-9][0-9_]*_int" => (BigUint::from_str(&<>.strip_suffix("_int").unwrap().replace('_', "")).unwrap().into(), Type::Int),
r"0x[0-9A-Fa-f][0-9A-Fa-f_]*_int" => (BigUint::from_str_radix(&<>[2..].strip_suffix("_int").unwrap().replace('_', ""), 16).unwrap().into(), Type::Int),
r"[0-9][0-9_]*_expr" => (BigUint::from_str(&<>.strip_suffix("_expr").unwrap().replace('_', "")).unwrap().into(), Type::Expr),
r"0x[0-9A-Fa-f][0-9A-Fa-f_]*_expr" => (BigUint::from_str_radix(&<>[2..].strip_suffix("_expr").unwrap().replace('_', ""), 16).unwrap().into(), Type::Expr),
}

UnsignedInteger: BigUint = {
Expand Down
6 changes: 1 addition & 5 deletions pil-analyzer/src/pil_analyzer.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -44,11 +44,7 @@ pub fn analyze_ast<T: FieldElement>(pil_file: PILFile) -> Result<Analyzed<T>, Ve
}

pub fn analyze_string<T: FieldElement>(contents: &str) -> Result<Analyzed<T>, Vec<Error>> {
let pil_file = powdr_parser::parse(Some("input"), contents).unwrap_or_else(|err| {
eprintln!("Error parsing .pil file:");
err.output_to_stderr();
panic!();
});
let pil_file = powdr_parser::parse(Some("input"), contents).map_err(|e| vec![e])?;
analyze(vec![pil_file])
}

Expand Down
84 changes: 42 additions & 42 deletions pil-analyzer/tests/condenser.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -37,7 +37,7 @@ fn new_witness_column() {
t[0] = t[1];
"#;
let expected = r#"namespace N(16);
col fixed even(i) { i * 2 };
col fixed even(i) { i * 2_int };
let new_wit: -> expr = constr || {
let x: col;
x
Expand Down Expand Up @@ -99,7 +99,7 @@ fn create_constraints() {
y = x_is_zero + 2;
"#;
let expected = r#"namespace N(16);
let force_bool: expr -> std::prelude::Constr = |c| c * (1 - c) = 0;
let force_bool: expr -> std::prelude::Constr = |c| c * (1_expr - c) = 0_expr;
let new_bool: -> expr = constr || {
let x: col;
N::force_bool(x);
Expand All @@ -109,8 +109,8 @@ fn create_constraints() {
let x_is_zero: col;
N::force_bool(x_is_zero);
let x_inv: col;
x_is_zero = 1 - x * x_inv;
x_is_zero * x = 0;
x_is_zero = 1_expr - x * x_inv;
x_is_zero * x = 0_expr;
x_is_zero
};
col witness x;
Expand Down Expand Up @@ -250,12 +250,12 @@ fn new_fixed_column() {
let formatted = analyze_string(input).to_string();
let expected = r#"namespace N(16);
let f: -> expr = constr || {
let even: col = |i| i * 2;
let even: col = |i| i * 2_int;
even
};
let ev: expr = N::f();
col witness x;
col fixed even(i) { i * 2 };
col fixed even(i) { i * 2_int };
N::x = N::even;
"#;
assert_eq!(formatted, expected);
Expand All @@ -275,14 +275,14 @@ fn new_fixed_column_as_closure() {
let formatted = analyze_string(input).to_string();
let expected = r#"namespace N(16);
let f: int -> expr = constr |j| {
let fi: col = |i| (i + j) * 2;
let fi: col = |i| (i + j) * 2_int;
fi
};
let ev: expr = N::f(2);
let ev: expr = N::f(2_int);
col witness x;
let fi = {
let j = 2;
|i| (i + j) * 2
let j = 2_int;
|i| (i + j) * 2_int
};
N::x = N::fi;
"#;
Expand Down Expand Up @@ -315,7 +315,7 @@ namespace N(16);
col witness y;
std::prelude::set_hint(N::y, query |i| std::prelude::Query::Hint(std::prover::eval(N::x)));
col witness z;
std::prelude::set_hint(N::z, query |_| std::prelude::Query::Hint(1));
std::prelude::set_hint(N::z, query |_| std::prelude::Query::Hint(1_fe));
"#;
let formatted = analyze_string(input).to_string();
assert_eq!(formatted, expected);
Expand Down Expand Up @@ -429,19 +429,19 @@ fn set_hint_outside() {
}
namespace N(16);
col witness x;
std::prelude::set_hint(N::x, query |_| std::prelude::Query::Hint(8));
std::prelude::set_hint(N::x, query |_| std::prelude::Query::Hint(8_fe));
col witness y;
std::prelude::set_hint(N::y, query |_| std::prelude::Query::Hint(8));
std::prelude::set_hint(N::y, query |_| std::prelude::Query::Hint(8_fe));
let create_wit: -> expr = constr || {
let w: col;
w
};
let z: expr = N::create_wit();
let set_hint: expr -> () = constr |c| {
std::prelude::set_hint(c, query |_| std::prelude::Query::Hint(8));
std::prelude::set_hint(c, query |_| std::prelude::Query::Hint(8_fe));
};
col witness w;
std::prelude::set_hint(N::w, query |_| std::prelude::Query::Hint(8));
std::prelude::set_hint(N::w, query |_| std::prelude::Query::Hint(8_fe));
"#;
let formatted = analyze_string(input).to_string();
assert_eq!(formatted, expected);
Expand Down Expand Up @@ -535,8 +535,8 @@ fn closure() {
namespace N(16);
col witness x;
std::prelude::set_hint(N::x, {
let r = 9;
|i| N::y(1, i, || 9 + r)
let r = 9_fe;
|i| N::y(1_fe, i, || 9_fe + r)
});
let y: fe, int, (-> fe) -> std::prelude::Query = |a, b, c| std::prelude::Query::Hint(a + c());
"#;
Expand Down Expand Up @@ -572,14 +572,14 @@ namespace std::convert;
namespace N(16);
col witness x;
std::prelude::set_hint(N::x, {
let r = 9;
let k = [-2];
let r = 9_fe;
let k = [-2_int];
let q = std::prelude::false;
let b = {
let s = "";
|| "" == s
};
|i| { N::y(1, i, || if b() && q { 9 + r } else { std::convert::fe::<int>(k[0]) }) }
|i| { N::y(1_fe, i, || if b() && q { 9_fe + r } else { std::convert::fe::<int>(k[0_int]) }) }
});
let y: fe, int, (-> fe) -> std::prelude::Query = |a, b, c| std::prelude::Query::Hint(a + c());
"#;
Expand Down Expand Up @@ -681,8 +681,8 @@ namespace N(16);
col witness y;
N::x = N::y;
query |i| {
std::prover::provide_value(N::x, i, std::convert::fe::<int>(i % 2));
std::prover::provide_value(N::y, i, std::convert::fe::<int>(i % 2));
std::prover::provide_value(N::x, i, std::convert::fe::<int>(i % 2_int));
std::prover::provide_value(N::y, i, std::convert::fe::<int>(i % 2_int));
};
"#;
assert_eq!(analyzed.to_string(), expected);
Expand Down Expand Up @@ -718,8 +718,8 @@ namespace N(16);
let y: col;
x = y;
query |i| {
std::prover::provide_value(x, i, std::convert::fe::<int>(i % 2));
std::prover::provide_value(y, i, std::convert::fe::<int>(i % 2));
std::prover::provide_value(x, i, std::convert::fe::<int>(i % 2_int));
std::prover::provide_value(y, i, std::convert::fe::<int>(i % 2_int));
};
};
col witness x;
Expand All @@ -729,8 +729,8 @@ namespace N(16);
let x = N::x;
let y = N::y;
query |i| {
std::prover::provide_value(x, i, std::convert::fe::<int>(i % 2));
std::prover::provide_value(y, i, std::convert::fe::<int>(i % 2));
std::prover::provide_value(x, i, std::convert::fe::<int>(i % 2_int));
std::prover::provide_value(y, i, std::convert::fe::<int>(i % 2_int));
}
};
"#;
Expand All @@ -757,12 +757,12 @@ fn new_cols_at_stage() {
let new_witness_col_at_stage: string, int -> expr = [];
namespace N(16);
col witness x;
let r: expr = std::prover::new_witness_col_at_stage("x", 0);
let s: expr = std::prover::new_witness_col_at_stage("x", 1);
let t: expr = std::prover::new_witness_col_at_stage("x", 2);
let u: expr = std::prover::new_witness_col_at_stage("y", 1);
let v: expr = std::prover::new_witness_col_at_stage("y", 2);
let unused: expr = std::prover::new_witness_col_at_stage("z", 10);
let r: expr = std::prover::new_witness_col_at_stage("x", 0_int);
let s: expr = std::prover::new_witness_col_at_stage("x", 1_int);
let t: expr = std::prover::new_witness_col_at_stage("x", 2_int);
let u: expr = std::prover::new_witness_col_at_stage("y", 1_int);
let v: expr = std::prover::new_witness_col_at_stage("y", 2_int);
let unused: expr = std::prover::new_witness_col_at_stage("z", 10_int);
col witness y;
col witness x_1;
col witness stage(1) x_2;
Expand Down Expand Up @@ -801,7 +801,7 @@ fn capture_enums() {
{
let x = N::E::A("abc");
let y = N::E::B;
let z = N::E::C([1, 2], 9);
let z = N::E::C([1_int, 2_int], 9_int);
let w = N::E::D();
query |_| {
let t: (N::E<string>, N::E<int[][]>, N::E<int[]>, N::E<fe>) = (x, y, z, w);
Expand Down Expand Up @@ -842,7 +842,7 @@ namespace std::prover;
{
let x = std::prelude::challenge(0, 4);
let y = std::prover::y;
let t = 2;
let t = 2_fe;
query |i| {
std::prover::provide_value(y, i, std::prover::eval(x) + t);
}
Expand Down Expand Up @@ -942,8 +942,8 @@ pub fn capture_constraints_new_col_and_constr() {
namespace Main;
let gen: -> () = constr || {
let x: col;
[x = 1, x = 2];
x = 3;
[x = 1_expr, x = 2_expr];
x = 3_expr;
};
col witness a;
col witness b;
Expand Down Expand Up @@ -989,13 +989,13 @@ namespace Main;
[Main::a] in [Main::b];
let constrs: std::prelude::Constr[] = std::prover::capture_constraints(constr || {
let x: col;
[x = 1, x = 2];
[x = 1_expr, x = 2_expr];
std::prover::capture_constraints(constr || {
let y: col;
[y = 1, [y] in [x]];
y = 3;
})[1];
x = 3;
[y = 1_expr, [y] in [x]];
y = 3_expr;
})[1_int];
x = 3_expr;
});
col witness x;
col witness y;
Expand Down Expand Up @@ -1068,7 +1068,7 @@ namespace Main;
col witness a;
col b = Main::a * Main::a;
col witness stage(1) c;
col fixed first(i) { if i == 0 { 1 } else { 0 } };
col fixed first(i) { if i == 0_int { 1_fe } else { 0_fe } };
col d = Main::a + Main::c;
Main::c' = Main::first;
col witness x;
Expand Down
Loading

0 comments on commit b50a586

Please sign in to comment.