diff --git a/kmir/src/kmir/kdist/mir-semantics/kmir.md b/kmir/src/kmir/kdist/mir-semantics/kmir.md index 5a2b48c65..b85ee0002 100644 --- a/kmir/src/kmir/kdist/mir-semantics/kmir.md +++ b/kmir/src/kmir/kdist/mir-semantics/kmir.md @@ -606,6 +606,11 @@ Therefore a heuristics is used here: // unpack tuple and set arguments individually rule #setTupleArgs(IDX, Aggregate(variantIdx(0), ARGS)) => #setTupleArgs(IDX, ARGS) ... + rule #setTupleArgs(IDX, VAL:Value) + => #setTupleArgs(IDX, ListItem(VAL)) + ... + [owise] + rule #setTupleArgs(_, .List ) => .K ... rule #setTupleArgs(IDX, ListItem(VAL) REST:List) diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/data.md b/kmir/src/kmir/kdist/mir-semantics/rt/data.md index 840ae6095..bcce7438b 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/data.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/data.md @@ -1051,6 +1051,12 @@ Literal arrays are also built using this RValue. ... + rule ARGS:List ~> #mkAggregate(aggregateKindClosure(_DEF, _TY_ARGS)) + => + Aggregate(variantIdx(0), ARGS) + ... + + // #readOperands accumulates a list of `TypedLocal` values from operands syntax KItem ::= #readOperands ( Operands ) diff --git a/kmir/src/tests/integration/data/prove-rs/closure-staged.rs b/kmir/src/tests/integration/data/prove-rs/closure-staged.rs new file mode 100644 index 000000000..98e256256 --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/closure-staged.rs @@ -0,0 +1,11 @@ +fn apply u8>(f: F, v: u8) -> u8 { + f(v) +} + +fn main() { + let delta: u8 = 1u8; + let _captured = |x: u8| x + delta; + + let f = |x: u8| x + 1u8; + assert_eq!(apply(f, 41u8), 42u8); +}