max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: cleanup bigop example

Browse source
This commit is contained in:
Leonardo de Moura 2020-01-22 14:22:34 -08:00
parent c9474c1883
commit c9e9208ea2
1 changed files with 39 additions and 32 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

71
tests/lean/run/bigop.lean
View file

@ -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