From 0f85b5cd086de4bc11c769631c477671ad53f73c Mon Sep 17 00:00:00 2001 From: Josh Tilles Date: Wed, 20 Apr 2022 11:01:33 -0400 Subject: [PATCH] Use new names for node kinds See: Addresses errors: ```sh-session $ lean Bigop.lean bigop 0 [0, 2, 4] fun i => (i, Add.add, i != 2, i) : Nat bigop 0 (index_iota 10 20) fun i => (i, Add.add, i != 5, i + 1) : Nat bigop 0 (index_iota 10 20) fun i => (i, Add.add, true, i + 1) : Nat bigop 1 [0, 2, 4] fun i => (i, Mul.mul, i != 2, i) : Nat bigop 1 (index_iota 10 20) fun i => (i, Mul.mul, i != 5, i + 1) : Nat bigop 1 (index_iota 10 20) fun i => (i, Mul.mul, true, i + 1) : Nat bigop 0 Enumerable.elems fun i => (i, Add.add, true, i + 1) : Fin 10 bigop 0 Enumerable.elems fun i => (i, Add.add, i != 2, i + 1) : Fin 10 bigop 0 Enumerable.elems fun i => (i, Add.add, myPred i, i + i) : Fin 10 bigop 1 Enumerable.elems fun i => (i, Mul.mul, true, i + 1) : Fin 10 bigop 1 Enumerable.elems fun i => (i, Mul.mul, i != 2, i + 1) : Fin 10 bigop 1 Enumerable.elems fun i => (i, Mul.mul, myPred i, i + i) : Fin 10 bigop 0 (index_iota 10 20) fun i => (i, Add.add, true, i + 1) : Nat Bigop.lean:119:12: error: expected '&', '(', '[', 'atom', 'binary', 'cat', 'ident', 'macroArg', 'nonReserved', 'paren', 'sepBy', 'sepBy(', 'sepBy1', 'sepBy1(', 'str', 'stx', 'unary', identifier or string literal Bigop.lean:121:0: error: elaboration function for 'Bigop.commandDef_bigop___' has not been implemented Bigop.lean:122:14: error: expected ')' $ lean Expander.lean Expander.lean:127:6: error: expected '#check', '#check_failure', '#eval', '#exit', '#print', '#reduce', '#resolve_name', '#synth', '/-!', '`(tactic|', 'abbrev', 'attribute', 'axiom', 'builtin_initialize', 'check', 'check_failure', 'class', 'classInductive', 'classTk', 'command', 'constant', 'declaration', 'declare_syntax_cat', 'def', 'deriving', 'elab', 'elab_rules', 'end', 'eval', 'example', 'exit', 'export', 'genInjectiveTheorems', 'gen_injective_theorems%', 'inductive', 'infix', 'infixl', 'infixr', 'init_quot', 'initialize', 'instance', 'macro', 'macro_rules', 'mixfix', 'moduleDoc', 'mutual', 'namespace', 'noncomputable', 'noncomputableSection', 'notation', 'open', 'postfix', 'prefix', 'print', 'printAxioms', 'quot', 'reduce', 'resolve_name', 'section', 'set_option', 'structure', 'structureTk', 'syntax', 'syntaxAbbrev', 'syntaxCat', 'synth', 'term', 'theorem', 'unif_hint', 'universe', 'variable' or identifier Expander.lean:134:10: error: expected identifier Expander.lean:136:10: error: expected identifier Expander.lean:138:13: error: expected '&', '(', 'sepBy(', 'sepBy1(', identifier or string literal Expander.lean:138:89: error: expected '&', '(', 'sepBy(', 'sepBy1(', identifier or string literal Expander.lean:140:20: error: expected '`(tactic|' Expander.lean:143:20: error: expected '`(tactic|' Expander.lean:198:6: error: expected '#check', '#check_failure', '#eval', '#exit', '#print', '#reduce', '#resolve_name', '#synth', '/-!', '`(tactic|', 'abbrev', 'attribute', 'axiom', 'builtin_initialize', 'check', 'check_failure', 'class', 'classInductive', 'classTk', 'command', 'constant', 'declaration', 'declare_syntax_cat', 'def', 'deriving', 'elab', 'elab_rules', 'end', 'eval', 'example', 'exit', 'export', 'genInjectiveTheorems', 'gen_injective_theorems%', 'inductive', 'infix', 'infixl', 'infixr', 'init_quot', 'initialize', 'instance', 'macro', 'macro_rules', 'mixfix', 'moduleDoc', 'mutual', 'namespace', 'noncomputable', 'noncomputableSection', 'notation', 'open', 'postfix', 'prefix', 'print', 'printAxioms', 'quot', 'reduce', 'resolve_name', 'section', 'set_option', 'structure', 'structureTk', 'syntax', 'syntaxAbbrev', 'syntaxCat', 'synth', 'term', 'theorem', 'unif_hint', 'universe', 'variable' or identifier Expander.lean:201:10: error: expected identifier Expander.lean:202:13: error: expected '&', '(', 'sepBy(', 'sepBy1(', identifier or string literal Expander.lean:203:20: error: expected '`(tactic|' Expander.lean:301:0: error: cannot evaluate code because 'Lean.Expander.expand' uses 'sorry' and/or contains errors Expander.lean:308:0: error: cannot evaluate code because 'Lean.Expander.expand' uses 'sorry' and/or contains errors ``` --- Bigop.lean | 2 +- Expander.lean | 8 ++++---- lean-toolchain | 2 +- 3 files changed, 6 insertions(+), 6 deletions(-) diff --git a/Bigop.lean b/Bigop.lean index eb575a9..5adf4ec 100644 --- a/Bigop.lean +++ b/Bigop.lean @@ -116,7 +116,7 @@ syntax "def_bigop" str term:max term:max : command -- `F` is inserted only in the second expansion, the expansion of the new macro `$head`. macro_rules | `(def_bigop $head $op $unit) => - `(macro $head:strLit "(" idx:index ")" F:term : term => `(\big_ [$op, $unit] ($$idx) $$F)) + `(macro $head:str "(" idx:index ")" F:term : term => `(\big_ [$op, $unit] ($$idx) $$F)) def_bigop "SUM" Nat.add 0 #check SUM (i <- [0, 1, 2]) i+1 diff --git a/Expander.lean b/Expander.lean index 93c00bf..482e9c3 100644 --- a/Expander.lean +++ b/Expander.lean @@ -124,8 +124,8 @@ partial def expand : Syntax → ExpanderM Syntax | `(fun $id:ident => $e) => do let e ← withLocal (getIdentVal id) (expand e) `(fun $id:ident => $e) - | `($num:numLit) => `($num:numLit) - | `($str:strLit) => `($str:strLit) + | `($num:num) => `($num:num) + | `($str:str) => `($str:str) | `($n:quotedName) => `($n:quotedName) | `($fn $args*) => do let fn ← expand fn @@ -195,8 +195,8 @@ partial def pp : Syntax → Format | ps => ppIdent id.getId ++ bracket "{" (joinSep (ps.map (format ∘ Prod.fst)) ", ") "}" | `(fun ($id : $ty) => $e) => paren f!"fun {paren (pp id ++ " : " ++ pp ty)} => {pp e}" | `(fun $id => $e) => paren f!"fun {pp id} => {pp e}" - | `($num:numLit) => format (num.isNatLit?.getD 0) - | `($str:strLit) => repr (str.isStrLit?.getD "") + | `($num:num) => format (num.isNatLit?.getD 0) + | `($str:str) => repr (str.isStrLit?.getD "") | `($fn $args*) => paren <| pp fn ++ " " ++ joinSep (args.toList.map pp) line | `(def $id:ident := $e) => f!"def {ppIdent id.getId} := {pp e}" | `(syntax $[(name := $n)]? $[(priority := $prio)]? $[$args:stx]* : $kind) => "syntax ..." -- irrelevant for this example diff --git a/lean-toolchain b/lean-toolchain index a992958..3a406d1 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2022-02-05 +leanprover/lean4:nightly-2022-04-02