From 0241d7c197fa989e966deabc16192f78de5896fd Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 1 Apr 2022 11:34:50 -0700 Subject: [PATCH] chore: fix tests --- tests/lean/414.lean | 8 +++---- tests/lean/StxQuot.lean.expected.out | 34 ++++++++++++++-------------- tests/lean/run/bigop.lean | 4 ++-- tests/lean/run/constProp.lean | 2 +- tests/lean/run/macro_macro.lean | 2 +- tests/lean/run/toFromJson.lean | 4 ++-- 6 files changed, 27 insertions(+), 27 deletions(-) diff --git a/tests/lean/414.lean b/tests/lean/414.lean index 9770bcabf9..c9269557b9 100644 --- a/tests/lean/414.lean +++ b/tests/lean/414.lean @@ -1,14 +1,14 @@ -macro_rules (kind := numLit) - | `($n:numLit) => `("world") +macro_rules (kind := num) + | `($n:num) => `("world") #check 2 macro_rules - | `($n:numLit) => `("hello") + | `($n:num) => `("hello") #check 2 -macro_rules (kind := numLit) +macro_rules (kind := num) | n => `("boo") #check 2 diff --git a/tests/lean/StxQuot.lean.expected.out b/tests/lean/StxQuot.lean.expected.out index 85ea98dd3d..da6a5d841a 100644 --- a/tests/lean/StxQuot.lean.expected.out +++ b/tests/lean/StxQuot.lean.expected.out @@ -3,46 +3,46 @@ StxQuot.lean:8:12: error: expected command, identifier or term "" "" "" -"(«term_+_» \"+\" (numLit \"1\"))" -"(«term_+_» \"+\" (numLit \"1\"))" -"(«term_+_» (numLit \"1\") \"+\" (numLit \"1\"))" +"(«term_+_» \"+\" (num \"1\"))" +"(«term_+_» \"+\" (num \"1\"))" +"(«term_+_» (num \"1\") \"+\" (num \"1\"))" StxQuot.lean:18:15: error: expected term "(Term.fun \"fun\" (Term.basicFun [`a._@.UnhygienicMain._hyg.1] \"=>\" `a._@.UnhygienicMain._hyg.1))" -"(Command.declaration\n (Command.declModifiers [] [] [] [] [] [])\n (Command.def\n \"def\"\n (Command.declId `foo._@.UnhygienicMain._hyg.1 [])\n (Command.optDeclSig [] [])\n (Command.declValSimple \":=\" (numLit \"1\") [])\n []\n []\n []))" -"[(Command.declaration\n (Command.declModifiers [] [] [] [] [] [])\n (Command.def\n \"def\"\n (Command.declId `foo._@.UnhygienicMain._hyg.1 [])\n (Command.optDeclSig [] [])\n (Command.declValSimple \":=\" (numLit \"1\") [])\n []\n []\n []))\n (Command.declaration\n (Command.declModifiers [] [] [] [] [] [])\n (Command.def\n \"def\"\n (Command.declId `bar._@.UnhygienicMain._hyg.1 [])\n (Command.optDeclSig [] [])\n (Command.declValSimple \":=\" (numLit \"2\") [])\n []\n []\n []))]" +"(Command.declaration\n (Command.declModifiers [] [] [] [] [] [])\n (Command.def\n \"def\"\n (Command.declId `foo._@.UnhygienicMain._hyg.1 [])\n (Command.optDeclSig [] [])\n (Command.declValSimple \":=\" (num \"1\") [])\n []\n []\n []))" +"[(Command.declaration\n (Command.declModifiers [] [] [] [] [] [])\n (Command.def\n \"def\"\n (Command.declId `foo._@.UnhygienicMain._hyg.1 [])\n (Command.optDeclSig [] [])\n (Command.declValSimple \":=\" (num \"1\") [])\n []\n []\n []))\n (Command.declaration\n (Command.declModifiers [] [] [] [] [] [])\n (Command.def\n \"def\"\n (Command.declId `bar._@.UnhygienicMain._hyg.1 [])\n (Command.optDeclSig [] [])\n (Command.declValSimple \":=\" (num \"2\") [])\n []\n []\n []))]" "`Nat.one._@.UnhygienicMain._hyg.1" "`Nat.one._@.UnhygienicMain._hyg.1" "(Term.app `f._@.UnhygienicMain._hyg.1 [`Nat.one._@.UnhygienicMain._hyg.1 `Nat.one._@.UnhygienicMain._hyg.1])" -"(«term_$__»\n `f._@.UnhygienicMain._hyg.1\n \"$\"\n (Term.app `f._@.UnhygienicMain._hyg.1 [`Nat.one._@.UnhygienicMain._hyg.1 (numLit \"1\")]))" +"(«term_$__»\n `f._@.UnhygienicMain._hyg.1\n \"$\"\n (Term.app `f._@.UnhygienicMain._hyg.1 [`Nat.one._@.UnhygienicMain._hyg.1 (num \"1\")]))" "(Term.app `f._@.UnhygienicMain._hyg.1 [`Nat.one._@.UnhygienicMain._hyg.1])" "(Term.proj `Nat.one._@.UnhygienicMain._hyg.1 \".\" `b._@.UnhygienicMain._hyg.1)" -"(«term_+_» (numLit \"2\") \"+\" (numLit \"1\"))" -"(«term_+_» («term_+_» (numLit \"1\") \"+\" (numLit \"2\")) \"+\" (numLit \"1\"))" -"(Command.declaration\n (Command.declModifiers [] [] [] [] [] [])\n (Command.def\n \"def\"\n (Command.declId `foo._@.UnhygienicMain._hyg.1 [])\n (Command.optDeclSig [] [])\n (Command.declValSimple \":=\" (numLit \"1\") [])\n []\n []\n []))" -"[(Command.declaration\n (Command.declModifiers [] [] [] [] [] [])\n (Command.def\n \"def\"\n (Command.declId `bar._@.UnhygienicMain._hyg.1 [])\n (Command.optDeclSig [] [])\n (Command.declValSimple \":=\" (numLit \"2\") [])\n []\n []\n []))\n (Command.declaration\n (Command.declModifiers [] [] [] [] [] [])\n (Command.def\n \"def\"\n (Command.declId `foo._@.UnhygienicMain._hyg.1 [])\n (Command.optDeclSig [] [])\n (Command.declValSimple \":=\" (numLit \"1\") [])\n []\n []\n []))]" +"(«term_+_» (num \"2\") \"+\" (num \"1\"))" +"(«term_+_» («term_+_» (num \"1\") \"+\" (num \"2\")) \"+\" (num \"1\"))" +"(Command.declaration\n (Command.declModifiers [] [] [] [] [] [])\n (Command.def\n \"def\"\n (Command.declId `foo._@.UnhygienicMain._hyg.1 [])\n (Command.optDeclSig [] [])\n (Command.declValSimple \":=\" (num \"1\") [])\n []\n []\n []))" +"[(Command.declaration\n (Command.declModifiers [] [] [] [] [] [])\n (Command.def\n \"def\"\n (Command.declId `bar._@.UnhygienicMain._hyg.1 [])\n (Command.optDeclSig [] [])\n (Command.declValSimple \":=\" (num \"2\") [])\n []\n []\n []))\n (Command.declaration\n (Command.declModifiers [] [] [] [] [] [])\n (Command.def\n \"def\"\n (Command.declId `foo._@.UnhygienicMain._hyg.1 [])\n (Command.optDeclSig [] [])\n (Command.declValSimple \":=\" (num \"1\") [])\n []\n []\n []))]" "0" 0 1 "1" -"(Term.fun\n \"fun\"\n (Term.basicFun\n [`a._@.UnhygienicMain._hyg.1\n (Term.paren \"(\" [`b._@.UnhygienicMain._hyg.1 [(Term.typeAscription \":\" `Nat._@.UnhygienicMain._hyg.1)]] \")\")]\n \"=>\"\n (numLit \"1\")))" +"(Term.fun\n \"fun\"\n (Term.basicFun\n [`a._@.UnhygienicMain._hyg.1\n (Term.paren \"(\" [`b._@.UnhygienicMain._hyg.1 [(Term.typeAscription \":\" `Nat._@.UnhygienicMain._hyg.1)]] \")\")]\n \"=>\"\n (num \"1\")))" "#[(Term.paren \"(\" [`a._@.UnhygienicMain._hyg.1 [(Term.typeAscription \":\" `Nat._@.UnhygienicMain._hyg.1)]] \")\"), `b._@.UnhygienicMain._hyg.1]" "`a._@.UnhygienicMain._hyg.1" "(Term.forall \"∀\" [(Term.simpleBinder [(Term.hole \"_\")] [])] \",\" `c._@.UnhygienicMain._hyg.1)" "(Term.simpleBinder [(Term.hole \"_\")] [])" "`a._@.UnhygienicMain._hyg.1" -"(Term.explicitUniv `a._@.UnhygienicMain._hyg.1 \".{\" [(numLit \"0\")] \"}\")" -"#[(Term.matchAlt \"|\" [[`a._@.UnhygienicMain._hyg.1]] \"=>\" (numLit \"1\")), (Term.matchAlt \"|\" [[(Term.hole \"_\")]] \"=>\" (numLit \"2\"))]" +"(Term.explicitUniv `a._@.UnhygienicMain._hyg.1 \".{\" [(num \"0\")] \"}\")" +"#[(Term.matchAlt \"|\" [[`a._@.UnhygienicMain._hyg.1]] \"=>\" (num \"1\")), (Term.matchAlt \"|\" [[(Term.hole \"_\")]] \"=>\" (num \"2\"))]" "(Term.structInst\n \"{\"\n []\n [(group\n (Term.structInstField (Term.structInstLVal `a._@.UnhygienicMain._hyg.1 []) \":=\" `a._@.UnhygienicMain._hyg.1)\n [])]\n (Term.optEllipsis [])\n [\":\" `a._@.UnhygienicMain._hyg.1]\n \"}\")" "(Term.structInst\n \"{\"\n []\n [(group\n (Term.structInstField (Term.structInstLVal `a._@.UnhygienicMain._hyg.1 []) \":=\" `a._@.UnhygienicMain._hyg.1)\n [])]\n (Term.optEllipsis [])\n []\n \"}\")" "(Command.section \"section\" [])" "(Command.section \"section\" [`foo._@.UnhygienicMain._hyg.1])" -"(Term.match\n \"match\"\n []\n []\n [(Term.matchDiscr [] `a._@.UnhygienicMain._hyg.1)]\n \"with\"\n (Term.matchAlts\n [(Term.matchAlt \"|\" [[`a._@.UnhygienicMain._hyg.1]] \"=>\" `b._@.UnhygienicMain._hyg.1)\n (Term.matchAlt\n \"|\"\n [[(«term_+_» `a._@.UnhygienicMain._hyg.1 \"+\" (numLit \"1\"))]]\n \"=>\"\n («term_+_» `b._@.UnhygienicMain._hyg.1 \"+\" (numLit \"1\")))]))" -"(Term.match\n \"match\"\n []\n []\n [(Term.matchDiscr [] `a._@.UnhygienicMain._hyg.1)]\n \"with\"\n (Term.matchAlts\n [(Term.matchAlt \"|\" [[`a._@.UnhygienicMain._hyg.1]] \"=>\" `b._@.UnhygienicMain._hyg.1)\n (Term.matchAlt\n \"|\"\n [[(«term_+_» `a._@.UnhygienicMain._hyg.1 \"+\" (numLit \"1\"))]]\n \"=>\"\n («term_+_» `b._@.UnhygienicMain._hyg.1 \"+\" (numLit \"1\")))]))" +"(Term.match\n \"match\"\n []\n []\n [(Term.matchDiscr [] `a._@.UnhygienicMain._hyg.1)]\n \"with\"\n (Term.matchAlts\n [(Term.matchAlt \"|\" [[`a._@.UnhygienicMain._hyg.1]] \"=>\" `b._@.UnhygienicMain._hyg.1)\n (Term.matchAlt\n \"|\"\n [[(«term_+_» `a._@.UnhygienicMain._hyg.1 \"+\" (num \"1\"))]]\n \"=>\"\n («term_+_» `b._@.UnhygienicMain._hyg.1 \"+\" (num \"1\")))]))" +"(Term.match\n \"match\"\n []\n []\n [(Term.matchDiscr [] `a._@.UnhygienicMain._hyg.1)]\n \"with\"\n (Term.matchAlts\n [(Term.matchAlt \"|\" [[`a._@.UnhygienicMain._hyg.1]] \"=>\" `b._@.UnhygienicMain._hyg.1)\n (Term.matchAlt\n \"|\"\n [[(«term_+_» `a._@.UnhygienicMain._hyg.1 \"+\" (num \"1\"))]]\n \"=>\"\n («term_+_» `b._@.UnhygienicMain._hyg.1 \"+\" (num \"1\")))]))" "#[`a._@.UnhygienicMain._hyg.1, `b._@.UnhygienicMain._hyg.1]" "1" "(Term.sufficesDecl [] `x._@.UnhygienicMain._hyg.1 (Term.fromTerm \"from\" `x._@.UnhygienicMain._hyg.1))" -"#[(numLit \"1\"), [(numLit \"2\") (numLit \"3\")], (numLit \"4\")]" -"#[(numLit \"2\")]" +"#[(num \"1\"), [(num \"2\") (num \"3\")], (num \"4\")]" +"#[(num \"2\")]" StxQuot.lean:94:39-94:44: error: unexpected antiquotation splice fun a => sorryAx (?m a) : (a : ?m) → ?m a "#[(some 1), (some 2)]" diff --git a/tests/lean/run/bigop.lean b/tests/lean/run/bigop.lean index b7c2f2cc01..4d727e53cb 100644 --- a/tests/lean/run/bigop.lean +++ b/tests/lean/run/bigop.lean @@ -102,8 +102,8 @@ macro_rules | `(Σ $idx => $F) => `(Prod ($idx) $F) -- 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) => - `(macro $head:strLit "(" idx:index ")" F:term : term => `(_big [$op, $unit] ($$idx) $$F)) +| `(def_bigop $head:str $op $unit) => + `(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/tests/lean/run/constProp.lean b/tests/lean/run/constProp.lean index 84037594a0..bb2013493e 100644 --- a/tests/lean/run/constProp.lean +++ b/tests/lean/run/constProp.lean @@ -70,7 +70,7 @@ syntax "`[Expr|" term "]" : term macro_rules | `(`[Expr|true]) => `((true : Expr)) | `(`[Expr|false]) => `((false : Expr)) - | `(`[Expr|$n:numLit]) => `(($n : Expr)) + | `(`[Expr|$n:num]) => `(($n : Expr)) | `(`[Expr|$x:ident]) => `(($(Lean.quote x.getId.toString) : Expr)) | `(`[Expr|$x = $y]) => `(Expr.bin `[Expr|$x] BinOp.eq `[Expr|$y]) | `(`[Expr|$x && $y]) => `(Expr.bin `[Expr|$x] BinOp.and `[Expr|$y]) diff --git a/tests/lean/run/macro_macro.lean b/tests/lean/run/macro_macro.lean index 0d2758242c..05e3dbddeb 100644 --- a/tests/lean/run/macro_macro.lean +++ b/tests/lean/run/macro_macro.lean @@ -1,6 +1,6 @@ macro "mk_m " id:ident v:str n:num c:char : command => let tk : Lean.Syntax := Lean.Syntax.mkStrLit id.getId.toString - `(macro $tk:strLit : term => `(fun (x : String) => x ++ $v ++ toString $n ++ toString $c)) + `(macro $tk:str : term => `(fun (x : String) => x ++ $v ++ toString $n ++ toString $c)) #print " ---- " diff --git a/tests/lean/run/toFromJson.lean b/tests/lean/run/toFromJson.lean index a138a3f9f9..e87e9aa817 100644 --- a/tests/lean/run/toFromJson.lean +++ b/tests/lean/run/toFromJson.lean @@ -12,8 +12,8 @@ syntax "json " json : term /- declare a micro json parser, so we can write our tests in a more legible way. -/ open Json in macro_rules - | `(json $s:strLit) => pure s - | `(json $n:numLit) => pure n + | `(json $s:str) => pure s + | `(json $n:num) => pure n | `(json { $[$ns : $js],* }) => do let mut fields := #[] for n in ns, j in js do