feat: arithmetic generics by michaeljklein · Pull Request #5060 · noir-lang/noir

michaeljklein · 2024-05-21T14:58:22Z

Description

Problem*

Supersedes #4958

Summary*

keeping variables up to date in the other approach was too heavy
this approach interns the arithmetic part so that a generic arithmetic expression can be represented as:

(id_to_expr_with_holes, Vec<variable_in_expr>)

Additional Context

Remaining issues:

Documentation*

Check one:

No documentation needed.
Documentation included in this PR.
[For Experimental Features] Documentation to be submitted in a separate PR. (Document generic arithmetic types once supported without --use-elaborator #5151)

PR Checklist*

I have tested the changes locally.
I have formatted the changes with Prettier and/or cargo fmt on default settings.

…d register in node interner, add generic arith ~tuple-like to hir, add key cases in monomorphizer, resolver, etc (wip)

…ssions for convert_expression_type, add conversion from BinaryTypeOperator for ArithOpKind, add node_interner api for arithmetic_expressions

jfecher

Initial approach looks good, nothing really jumped out at me

compiler/noirc_frontend/src/node_interner.rs

…ation to interner map for errors, add constraint validator to monomorphizer, add ArithConstraintError w/ conversion to MonomorphizerError, add monomorphizer evaluator, add evaluator and validator for arith expressions

… the node interner instead of a mutable parameter

…r locations in the call stack for emitting, evaluate generic args to u64, add error for distinct expressions

…rith's, intern constants as generic arith expressions, block unsupported impl's, add function to check for any GenericArith's in a Type, unify with constant case, wip following bindings and unifying against GenericArith, wip patching TypeVariable's, convert ArithId to a hash of the expression and do normalization, wip testing and added tests for blocked impl's

…ypeVariableId's, get_outer_type_variable, map_variables, converting 'stale' TypeVariables to the 'fresh' ones in the arguments

…Index in ArithExpr::Variable

…n variables as generic arith during resolution, add missing integer-like test for generic arith, add cases where a generic arith constraint was missing during try_unify, wip testing

…ry_evaluate_to_u64, propagate interner arg, found case that's causing current error in evaluate_generics_to_u64

…d', add NeedsInterning, filter out dummy locations for monomorphizer errors, add recursive follow_bindings case, fix sorting ArithOpKind::Sub expressions, calculate the maximum generic index for offsets, add errors for underflow and unexpected cases, added test cases

…h Vec, rename GenericIndex -> ArithGenericId, factor out impute_variables function, reduce clones where possible, add test result for turbofish

…on to convert_type_to_arith_expr, skip linting false positive

…ce hack of hash to order ArithExpr with proper ordering, fix broken impute, key test passing with elaborator

…better errors for partial evaluation

…ric_arith_in_self_type and prevent_generic_arith_in_trait_generics as separate functions, add issues for TODO's, add message to --use-elaborator, nargo fmt

vezenovm · 2024-05-31T14:39:03Z

test_programs/execution_success/generic_arith/src/main.nr

+
+    // it also fails when using turbofish 
+    //
+    // assert(tail::<Field, 3>([1,2,3]) == [2, 3]);


Does this line and the other commented out assertions also pass in the elaborator?

Great question: it and the other commented assertions pass nargo check with the elaborator, but not nargo test (with a test that just calls main). The unification assertion in node_interner/generic_arith.rs doesn't pass in either case: #5150

jfecher

I'm hesitant on the approach here and want to hold off on merging for now.

The use of interning bloats the code a bit and it's unclear to me why we need to intern every constant used in a type position for example. I would have thought we'd only need to remember arith expressions that are unified against each other.

I also think delaying these type checks until monomorphization will probably introduce bugs that are difficult/impossible to fix without changing the approach.

I'm thinking now maybe we should just admit we're adding dependent types to Noir and try to add unification / checking for those directly. We may need to switch to a bidirectional type checker but I think it'd end up being the cleaner approach in the end and could let us eventually handle traits as well.

michaeljklein · 2024-05-31T17:05:26Z

compiler/noirc_frontend/src/hir_def/types.rs

                let typevars = vecmap(typevars, |var| var.id().to_string());
                write!(f, "forall {}. {}", typevars.join(" "), typ)
            }
+            Type::GenericArith(arith_id, generics) => {


Need a TODO: this prints the arith ID

TomAFrench · 2024-06-14T15:23:06Z

Closing after discussing with Michael

michaeljklein added 2 commits May 20, 2024 14:40

feat: add generic arithmetics (2nd version), add arith expr struct an…

db3343e

…d register in node interner, add generic arith ~tuple-like to hir, add key cases in monomorphizer, resolver, etc (wip)

add error from other branch, pre-process generic arith relevant expre…

8e1ace9

…ssions for convert_expression_type, add conversion from BinaryTypeOperator for ArithOpKind, add node_interner api for arithmetic_expressions

jfecher reviewed May 21, 2024

View reviewed changes

compiler/noirc_frontend/src/node_interner.rs Outdated Show resolved Hide resolved

michaeljklein and others added 22 commits May 22, 2024 14:44

wip

7a51a52

add expected failure, update expected success test, use a ref cell in…

39433d2

… the node interner instead of a mutable parameter

wip, add other_locations method for arith constraint errors, put othe…

75f2673

…r locations in the call stack for emitting, evaluate generic args to u64, add error for distinct expressions

wip TypeVariableId's don't appear to be consistent w/ named generic T…

af0afbe

…ypeVariableId's, get_outer_type_variable, map_variables, converting 'stale' TypeVariables to the 'fresh' ones in the arguments

got key test case working, using GenericIndex + offsets, keep Generic…

7ac0c42

…Index in ArithExpr::Variable

wip debugging new error, "Type annotations needed" on function, inter…

8b43b96

…n variables as generic arith during resolution, add missing integer-like test for generic arith, add cases where a generic arith constraint was missing during try_unify, wip testing

wip debugging 'Type annotations needed', added GenericArith case to t…

a5ba238

…ry_evaluate_to_u64, propagate interner arg, found case that's causing current error in evaluate_generics_to_u64

uncomment unit tests

ddefa27

Merge branch 'master' into michaeljklein/interned-arith-generics

3392d5a

cargo fmt/clippy, cleanup pass

eb24682

todo/cleanup pass

e6f039c

clippy pass

d5805ca

clippy pass, refactor copy/pasted code, replace redundant HashMap wit…

ac983c4

…h Vec, rename GenericIndex -> ArithGenericId, factor out impute_variables function, reduce clones where possible, add test result for turbofish

cargo fmt

36918cd

Merge branch 'master' into michaeljklein/interned-arith-generics

506442e

Merge branch 'master' into michaeljklein/interned-arith-generics

c859821

wip moving changes over to elaborator, renamed prepare_arith_expressi…

f360857

…on to convert_type_to_arith_expr, skip linting false positive

cleanup copy/pasted block, properly recurse in follow_bindings, repla…

a762e9c

…ce hack of hash to order ArithExpr with proper ordering, fix broken impute, key test passing with elaborator

cargo clippy/fmt, move generic arith to own module, TODO's including …

a1f4aef

…better errors for partial evaluation

michaeljklein mentioned this pull request May 31, 2024

Document generic arithmetic types once supported without --use-elaborator #5151

Closed

clippy/fmt, ignore debugger generic arithmetic test, add prevent_gene…

4d9ccef

…ric_arith_in_self_type and prevent_generic_arith_in_trait_generics as separate functions, add issues for TODO's, add message to --use-elaborator, nargo fmt

michaeljklein marked this pull request as ready for review May 31, 2024 01:31

michaeljklein requested review from TomAFrench and vezenovm May 31, 2024 01:31

vezenovm reviewed May 31, 2024

View reviewed changes

michaeljklein and others added 2 commits May 31, 2024 11:28

partially revert commented out assertion to answer questions for PR

614c84b

Merge branch 'master' into michaeljklein/interned-arith-generics

7ab7503

TomAFrench mentioned this pull request May 31, 2024

feat: implement arithmetic on numeric generics #4958

Closed

5 tasks

michaeljklein and others added 2 commits May 31, 2024 12:04

cargo fmt

33f2204

Merge branch 'master' into michaeljklein/interned-arith-generics

c44a7e6

jfecher requested changes May 31, 2024

View reviewed changes

michaeljklein commented May 31, 2024

View reviewed changes

add backwards_tail and cons tests

03565dc

RajeshRk18 mentioned this pull request Jun 11, 2024

Const generics RajeshRk18/Hmac_Sha256-verifier-noir#1

Open

TomAFrench closed this Jun 14, 2024

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat: arithmetic generics #5060

feat: arithmetic generics #5060
michaeljklein wants to merge 30 commits intomasterfrom
michaeljklein/interned-arith-generics

michaeljklein commented May 21, 2024 •

edited

Loading

Uh oh!

jfecher left a comment

Uh oh!

Uh oh!

vezenovm May 31, 2024

Uh oh!

michaeljklein May 31, 2024

Uh oh!

jfecher left a comment

Uh oh!

michaeljklein May 31, 2024

Uh oh!

TomAFrench commented Jun 14, 2024

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

Conversation

michaeljklein commented May 21, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Description

Problem*

Summary*

Additional Context

Documentation*

PR Checklist*

Uh oh!

jfecher left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

vezenovm May 31, 2024

Choose a reason for hiding this comment

Uh oh!

michaeljklein May 31, 2024

Choose a reason for hiding this comment

Uh oh!

jfecher left a comment

Choose a reason for hiding this comment

Uh oh!

michaeljklein May 31, 2024

Choose a reason for hiding this comment

Uh oh!

TomAFrench commented Jun 14, 2024

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

michaeljklein commented May 21, 2024 •

edited

Loading