From c9e9208ea29a34fe715310f47fa5ce786a4b3b8e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 22 Jan 2020 14:22:34 -0800 Subject: [PATCH] feat: cleanup bigop example --- tests/lean/run/bigop.lean | 71 +++++++++++++++++++++------------------ 1 file changed, 39 insertions(+), 32 deletions(-) diff --git a/tests/lean/run/bigop.lean b/tests/lean/run/bigop.lean index d599a122c9..58041acfaa 100644 --- a/tests/lean/run/bigop.lean +++ b/tests/lean/run/bigop.lean @@ -42,62 +42,70 @@ instance {n} : HasOfNat (Fin (Nat.succ n)) := new_frontend +-- Declare a new syntax category for "indexing" big operators declare_syntax_cat index - -syntax ident "|" term : index syntax term:50 "≤" ident "<" term : index syntax term:50 "≤" ident "<" term "|" term : index syntax ident "<-" term : index syntax ident "<-" term "|" term : index -syntax ident ":" term : index -syntax ident ":" term "|" term : index - +-- Primitive notation for big operators syntax "_big" "[" term "," term "]" "(" index ")" term : term +-- We define how to expand different `_bigop` with the different kinds of index macro_rules -| `(_big [ $op , $idx ] ( $i:ident <- $r | $p ) $F) => `(bigop $idx $r (fun $i:ident => ($i:ident, $op, $p, $F))) -| `(_big [ $op , $idx ] ( $i:ident <- $r ) $F) => `(bigop $idx $r (fun $i:ident => ($i:ident, $op, true, $F))) -| `(_big [ $op , $idx ] ( $lower ≤ $i:ident < $upper ) $F) => `(bigop $idx (index_iota $lower $upper) (fun $i:ident => ($i:ident, $op, true, $F))) -| `(_big [ $op , $idx ] ( $lower ≤ $i:ident < $upper | $p ) $F) => `(bigop $idx (index_iota $lower $upper) (fun $i:ident => ($i:ident, $op, $p, $F))) -| `(_big [ $op , $idx ] ( $i:ident : $type ) $F) => `(bigop $idx (Enumerable.elems $type) (fun $i:ident => ($i:ident, $op, true, $F))) -| `(_big [ $op , $idx ] ( $i:ident : $type | $p ) $F) => `(bigop $idx (Enumerable.elems $type) (fun $i:ident => ($i:ident, $op, $p, $F))) -| `(_big [ $op , $idx ] ( $i:ident | $p ) $F) => `(bigop $idx (Enumerable.elems _) (fun $i:ident => ($i:ident, $op, $p, $F))) +| `(_big [$op, $idx] ($i:ident <- $r | $p) $F) => `(bigop $idx $r (fun $i:ident => ($i:ident, $op, $p, $F))) +| `(_big [$op, $idx] ($i:ident <- $r) $F) => `(bigop $idx $r (fun $i:ident => ($i:ident, $op, true, $F))) +| `(_big [$op, $idx] ($lower ≤ $i:ident < $upper) $F) => `(bigop $idx (index_iota $lower $upper) (fun $i:ident => ($i:ident, $op, true, $F))) +| `(_big [$op, $idx] ($lower ≤ $i:ident < $upper | $p) $F) => `(bigop $idx (index_iota $lower $upper) (fun $i:ident => ($i:ident, $op, $p, $F))) +-- Define `Sum` syntax "Sum" "(" index ")" term : term - macro_rules | `(Sum ($idx:index) $F:term) => `(_big [HasAdd.add, 0] ($idx:index) $F:term) -syntax "Prod" "(" index ")" term : term - -macro_rules -| `(Prod ($idx:index) $F:term) => `(_big [HasMul.mul, 1] ($idx:index) $F:term) - -def myPred (x : Fin 10) : Bool := true - +-- We can already use `Sum` with the different kinds of index. #check Sum (i <- [0, 2, 4] | i != 2) i #check Sum (10 ≤ i < 20 | i != 5) i+1 #check Sum (10 ≤ i < 20) i+1 + +-- Define `Prod` +syntax "Prod" "(" index ")" term : term +macro_rules +| `(Prod ($idx:index) $F:term) => `(_big [HasMul.mul, 1] ($idx:index) $F:term) + +-- The examples above now also work for `Prod` +#check Prod (i <- [0, 2, 4] | i != 2) i +#check Prod (10 ≤ i < 20 | i != 5) i+1 +#check Prod (10 ≤ i < 20) i+1 + +-- We can extend our grammar for the syntax category `index`. +syntax ident "|" term : index +syntax ident ":" term : index +syntax ident ":" term "|" term : index +-- And new rules +macro_rules +| `(_big [$op, $idx] ($i:ident : $type) $F) => `(bigop $idx (Enumerable.elems $type) (fun $i:ident => ($i:ident, $op, true, $F))) +| `(_big [$op, $idx] ($i:ident : $type | $p) $F) => `(bigop $idx (Enumerable.elems $type) (fun $i:ident => ($i:ident, $op, $p, $F))) +| `(_big [$op, $idx] ($i:ident | $p) $F) => `(bigop $idx (Enumerable.elems _) (fun $i:ident => ($i:ident, $op, $p, $F))) + +-- The new syntax is immediately available for all big operators that we have defined +def myPred (x : Fin 10) : Bool := true #check Sum (i : Fin 10) i+1 #check Sum (i : Fin 10 | i != 2) i+1 #check Sum (i | myPred i) i+i - -#check Prod (i <- [0, 2, 4] | i != 2) i -#check Prod (10 ≤ i < 20 | i != 5) (i+1) -#check Prod (10 ≤ i < 20) (i+1) -#check Prod (10 ≤ i < 20) (i+1) +#check Prod (i : Fin 10) i+1 #check Prod (i : Fin 10 | i != 2) i+1 #check Prod (i | myPred i) i+i -syntax "Prod" index "=>" term : term - +-- We can easily create alternative syntax for any big operator. +syntax "Σ" index "=>" term : term macro_rules -| `(Prod $idx:index => $F:term) => `(Prod ($idx:index) $F) +| `(Σ $idx:index => $F:term) => `(Prod ($idx:index) $F) -#check Prod 10 ≤ i < 20 => i+1 +#check Σ 10 ≤ i < 20 => i+1 +-- Now, we create command for automating the generation of big operators. syntax "def_bigop" str term:max term:max : command - macro_rules | `(def_bigop $head:strLit $op $unit) => -- We have to use `$(mkAntiquotStx idx "index"):index` instead of `$idx:index` because it occurs inside of a nested quasiquotation. @@ -107,5 +115,4 @@ macro_rules `(macro $head:strLit "(" idx:index ")" F:term : term => `(_big [$op, $unit] ($(idx.termIdToAntiquot "index"):index) $(F.termIdToAntiquot "term"))))) def_bigop "SUM" Nat.add 0 - -#check SUM (i <- [0, 1, 2]) (i+1) +#check SUM (i <- [0, 1, 2]) i+1