Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Type inference #1010

Merged
merged 1 commit into from
Mar 1, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 7 additions & 1 deletion ast/src/analyzed/display.rs
Original file line number Diff line number Diff line change
Expand Up @@ -304,7 +304,13 @@ impl Display for AlgebraicReference {

impl Display for PolynomialReference {
fn fmt(&self, f: &mut Formatter<'_>) -> Result {
write!(f, "{}", self.name,)
write!(f, "{}", self.name)?;
if let Some(generic_args) = &self.generic_args {
if !generic_args.is_empty() {
write!(f, "::<{}>", generic_args.iter().join(", "))?;
}
}
Ok(())
}
}

Expand Down
50 changes: 49 additions & 1 deletion ast/src/analyzed/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -11,14 +11,15 @@ use powdr_number::{DegreeType, FieldElement};
use schemars::JsonSchema;
use serde::{Deserialize, Serialize};

use crate::analyzed::types::ArrayType;
use crate::parsed::utils::expr_any;
use crate::parsed::visitor::ExpressionVisitable;
pub use crate::parsed::BinaryOperator;
pub use crate::parsed::UnaryOperator;
use crate::parsed::{self, SelectedExpressions};
use crate::SourceRef;

use self::types::TypedExpression;
use self::types::{Type, TypeScheme, TypedExpression};

#[derive(Debug, Clone, Serialize, Deserialize, JsonSchema)]
pub enum StatementIdentifier {
Expand Down Expand Up @@ -143,6 +144,12 @@ impl<T> Analyzed<T> {
.sum()
}

/// Returns the type (scheme) of a symbol with the given name.
pub fn type_of_symbol(&self, name: &str) -> TypeScheme {
let (sym, value) = &self.definitions[name];
type_from_definition(sym, value).unwrap()
}

/// Removes the specified polynomials and updates the IDs of the other polynomials
/// so that they are contiguous again.
/// There must not be any reference to the removed polynomials left.
Expand Down Expand Up @@ -419,6 +426,39 @@ fn inlined_expression_from_intermediate_poly_id<T: Copy + Display>(
expr
}

/// Extracts the declared (or implicit) type from a definition.
pub fn type_from_definition<T>(
symbol: &Symbol,
value: &Option<FunctionValueDefinition<T>>,
) -> Option<TypeScheme> {
if let Some(value) = value {
match value {
FunctionValueDefinition::Array(_) | FunctionValueDefinition::Query(_) => {
Some(Type::Col.into())
}
FunctionValueDefinition::Expression(TypedExpression { e: _, type_scheme }) => {
type_scheme.clone()
}
}
} else {
assert!(
symbol.kind == SymbolKind::Poly(PolynomialType::Committed)
|| symbol.kind == SymbolKind::Poly(PolynomialType::Constant)
);
if symbol.length.is_some() {
Some(
Type::Array(ArrayType {
base: Box::new(Type::Col),
length: None,
})
.into(),
)
} else {
Some(Type::Col.into())
}
}
}

#[derive(Debug, Clone, Serialize, Deserialize, JsonSchema)]
pub struct Symbol {
pub id: u64,
Expand Down Expand Up @@ -526,6 +566,11 @@ impl<T> RepeatedArray<T> {
&self.pattern
}

/// Returns the pattern to be repeated
pub fn pattern_mut(&mut self) -> &mut [Expression<T>] {
&mut self.pattern
}

/// Returns true iff this array is empty.
pub fn is_empty(&self) -> bool {
self.size == 0
Expand Down Expand Up @@ -828,6 +873,9 @@ pub struct PolynomialReference {
/// Optional because it is filled in in a second stage of analysis.
/// TODO make this non-optional
pub poly_id: Option<PolyID>,
/// The type arguments if the symbol is generic.
/// Guarenteed to be Some(_) after type checking is completed.
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

If it's guaranteed maybe it should be a GuaranteedGenericArgs type :D

pub generic_args: Option<Vec<Type>>,
}

#[derive(
Expand Down
7 changes: 6 additions & 1 deletion ast/src/analyzed/types.rs
Original file line number Diff line number Diff line change
Expand Up @@ -112,6 +112,11 @@ impl Type {
}
}

pub fn substitute_type_vars_to(mut self, substitutions: &HashMap<String, Type>) -> Self {
self.substitute_type_vars(substitutions);
self
}

fn contained_type_vars_with_repetitions(&self) -> Box<dyn Iterator<Item = &String> + '_> {
match self {
Type::TypeVar(n) => Box::new(std::iter::once(n)),
Expand Down Expand Up @@ -211,7 +216,7 @@ impl<T: FieldElement, Ref: Display> From<FunctionTypeName<Expression<T, Ref>>> f
pub struct TypeScheme {
/// Type variables and their trait bounds
pub vars: TypeBounds,
/// The actual type (using the type variables from `vars`)
/// The actual type (using the type variables from `vars` but potentially also other type variables)
pub ty: Type,
}

Expand Down
22 changes: 20 additions & 2 deletions ast/src/analyzed/visitor.rs
Original file line number Diff line number Diff line change
Expand Up @@ -92,7 +92,6 @@ impl<T> ExpressionVisitable<Expression<T>> for FunctionValueDefinition<T> {
}
FunctionValueDefinition::Array(array) => array
.iter_mut()
.flat_map(|a| a.pattern.iter_mut())
.try_for_each(move |item| item.visit_expressions_mut(f, o)),
}
}
Expand All @@ -108,8 +107,27 @@ impl<T> ExpressionVisitable<Expression<T>> for FunctionValueDefinition<T> {
}
FunctionValueDefinition::Array(array) => array
.iter()
.flat_map(|a| a.pattern().iter())
.try_for_each(move |item| item.visit_expressions(f, o)),
}
}
}

impl<T> ExpressionVisitable<Expression<T>> for RepeatedArray<T> {
fn visit_expressions_mut<F, B>(&mut self, f: &mut F, o: VisitOrder) -> ControlFlow<B>
where
F: FnMut(&mut Expression<T>) -> ControlFlow<B>,
{
self.pattern
.iter_mut()
.try_for_each(move |item| item.visit_expressions_mut(f, o))
}

fn visit_expressions<F, B>(&self, f: &mut F, o: VisitOrder) -> ControlFlow<B>
where
F: FnMut(&Expression<T>) -> ControlFlow<B>,
{
self.pattern
.iter()
.try_for_each(move |item| item.visit_expressions(f, o))
}
}
4 changes: 2 additions & 2 deletions ast/src/parsed/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -311,7 +311,7 @@ pub struct ArrayLiteral<T, Ref = NamespacedPolynomialReference> {
}

#[derive(
Debug, PartialEq, Eq, PartialOrd, Ord, Clone, Copy, Serialize, Deserialize, JsonSchema,
Debug, PartialEq, Eq, PartialOrd, Ord, Clone, Copy, Hash, Serialize, Deserialize, JsonSchema,
)]
pub enum UnaryOperator {
Minus,
Expand All @@ -330,7 +330,7 @@ impl UnaryOperator {
}

#[derive(
Debug, PartialEq, Eq, PartialOrd, Ord, Clone, Copy, Serialize, Deserialize, JsonSchema,
Debug, PartialEq, Eq, PartialOrd, Ord, Clone, Copy, Hash, Serialize, Deserialize, JsonSchema,
)]
pub enum BinaryOperator {
Add,
Expand Down
5 changes: 3 additions & 2 deletions book/src/asm/declarations.md
Original file line number Diff line number Diff line change
@@ -1,7 +1,8 @@
# Declarations

Symbols can be defined via ``let <name> = <value>;``. The value is a generic [PIL-expression](../pil/expressions.md)
and its type is unconstrained (it can be a value, a function or even a higher-order function).
Symbols can be defined via ``let <name> = <value>;``, or via ``let <name>: <type> = <value>;`` if you want to
specify the type explicitly. The value is an arbitrary [PIL-expression](../pil/expressions.md).
For details, see the [Declarations](../pil/declarations.md) section in the PIL part.

Other symbols available in the current module can be accessed by name, but it is also possible to specify
full relative paths in the form of e.g. ``super::super::module_name::symbol``.
Expand Down
77 changes: 65 additions & 12 deletions book/src/pil/builtins.md
Original file line number Diff line number Diff line change
@@ -1,11 +1,15 @@
# Built-in Functions
# Built-ins

## Functions

The following functions are built into the compiler.
They need to be defined to be accessible, but their assigned value is ignored and the compiler replaces it with the following.

### Array length

`std::array::len: _[] -> int`
```rust
let<T> std::array::len: T[] -> int
```

Returns the length of an array as an integer.

Expand All @@ -17,7 +21,9 @@ let l = std::array::len(x); // returns 3

### Panic

`std::check::panic: string -> !`
```rust
let std::check::panic: string -> !
```

Aborts evaluation and prints its argument as error message as a
side-effect of its evaluation.
Expand All @@ -39,37 +45,47 @@ let secp256k1_inverse = |x|

### Conversions

`std::convert::fe: int -> fe`
```rust
let<T: FromLiteral> std::convert::fe: T -> fe
```

This function is meant to be used on `int`, but also works on `fe` for convenience.

Converts a non-negative integer less than the field modulus to a field element.
It converts a non-negative integer less than the field modulus to a field element.
Causes a type error in all other cases.

If the argument is already a field element, it is returned without modification.

`std::convert::int: fe -> int`
```rust
let<T: FromLiteral> std::convert::int: T -> int
```

This function is meant to be used on `fe`, but also works on `int` for convenience.

Converts a field element to an integer.
It converts a field element to an integer.

If the argument is already an integer, it is returned without modification.

### Printing

`std::debug::print: string -> []`
```rust
let std::debug::print: string -> constr[]
```

This function takes a string and prints it on the standard output during evaluation, as a side-effect of its evaluation.

This function should only be used for debugging purposes.

Any non-string argument is converted to a string first and then printed.

Note that the function does not append a newline at the end.

It returns an empty array so that it can be used at statement level where
It returns an empty `constr` array so that it can be used at statement level where
constraints are expected.

### Modulus

`std::field::modulus: -> int`
```rust
let std::field::modulus: -> int
```

Returns the current field's modulus as an integer.

Expand All @@ -82,3 +98,40 @@ if std::field::modulus() != 2**64 - 2**32 + 1 {
[]
};
```

## Operators

The following operators are supported by powdr-pil with their respective signatures.

```
let<T: Add> +: T, T -> T
let<T: Sub> -: T, T -> T
let<T: Neg> -: T -> T

let<T: Mul> *: T, T -> T
let /: int, int -> int
let %: int, int -> int
let<T: Pow> **: T, int -> T

let <<: int, int -> int
let >>: int, int -> int
let &: int, int -> int
let |: int, int -> int
let ^: int, int -> int

let<T: Ord> <: T, T -> bool
let<T: Ord> <=: T, T -> bool
let<T: Ord> >: T, T -> bool
let<T: Ord> >=: T, T -> bool
let<T: Ord> <: T, T -> bool

let<T: Eq> ==: T, T -> bool
let<T: Eq> !=: T, T -> bool

let =: expr, expr -> constr
let ': expr -> expr

let ||: bool, bool -> bool
let &&: bool, bool -> bool
let !: bool -> bool
```
13 changes: 6 additions & 7 deletions book/src/pil/declarations.md
Original file line number Diff line number Diff line change
Expand Up @@ -7,18 +7,17 @@ from the type of the symbol and the way the symbol is used.
Symbols can be declared using ``let <name>;`` and they can be declared and defined
using ``let <name> = <value>;``, where ``<value>`` is an expression. The [type](./types.md) of the symbol
can be explicitly specified using ``let <name>: <type>;`` and ``let <name>: <type> = <value>;``.
Symbols with a generic type can be defined using ``let<TV1, TV1, ..> <name>: <type> = <value>;``,
where the `TV` are newly created type variables that can be used in the type.

This syntax can be used for constants, fixed columns, witness columns and even (higher-order)
functions that can transform expressions. The kind of symbol is deduced by its type and the
way the symbol is used:

- Symbols without a value are witness columns or arrays of witness columns. Their type can be omitted. If it is given, it must be ``col`` or ``col[]``.
- Symbols evaluating to a number or with type ``fe`` are constants.
- Symbols without type but with a value that is a function with a single parameter are fixed columns.
- Symbols defined with a value and type ``col`` (or ``col[]``) are fixed columns (or arrays of fixed columns).
- Everything else is a "generic symbol" that is not a column or constant.

> Note that the type ``col`` is the same as ``int -> fe``, so ``let w: int -> fe`` also declares a witness column.
- Symbols without a value are witness columns or arrays of witness columns. Their type can be omitted. If it is given, it must be ``col`` or ``col[k]``.
- Symbols defined with a value and type ``col`` (or ``col[k]``) are fixed columns (or arrays of fixed columns).
- Symbols defined with a value and type ``expr`` (or ``expr[k]``) are intermediate columns (or arrays of intermediate columns).
- Everything else is a "generic symbol" that is not a column.

Examples:

Expand Down
8 changes: 4 additions & 4 deletions book/src/pil/expressions.md
Original file line number Diff line number Diff line change
Expand Up @@ -50,7 +50,7 @@ The "default" arm with the pattern `_` matches all values.

Example:

```
```rust
let fib = |i| match i {
0 => 1,
1 => 1,
Expand All @@ -62,12 +62,12 @@ let fib = |i| match i {

If expressions take the form ``if <condition> { <true value> } else { <false value> }``, where the "else" part is not optional.

If the condition evaluates to a non-zero number, `<true value>` is evaluated, otherwise `<false value>` is.
If the condition evaluates to ``true``, then `<true value>` is evaluated, otherwise `<false value>` is.


Example:

```
```rust
let is_seven = |i| if i == 7 { 1 } else { 0 };
```

Expand All @@ -88,6 +88,6 @@ Arbitrary parentheses are allowed.

The following example illustrates how you can still use the generic language:

```
```rust
{{#include ../../../test_data/pil/book/generic_to_algebraic.pil}}
```
2 changes: 0 additions & 2 deletions book/src/pil/fixed_columns.md
Original file line number Diff line number Diff line change
Expand Up @@ -30,5 +30,3 @@ A column can be seen as a mapping from integers to field elements. In this conte
```
{{#include ../../../test_data/pil/fixed_columns.pil:mapping}}
```

> Note that conversion from integer to field element is currently implicit, as seen in the first example above.
Loading
Loading