chore: fix tests
This commit is contained in:
Leonardo de Moura
parent
f45712ce74
commit
0241d7c197
6 changed files with 27 additions and 27 deletions
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -3,46 +3,46 @@ StxQuot.lean:8:12: error: expected command, identifier or term
|
|||
"<missing>"
|
||||
"<missing>"
|
||||
"<missing>"
|
||||
"(«term_+_» <missing> \"+\" (numLit \"1\"))"
|
||||
"(«term_+_» <missing> \"+\" (numLit \"1\"))"
|
||||
"(«term_+_» (numLit \"1\") \"+\" (numLit \"1\"))"
|
||||
"(«term_+_» <missing> \"+\" (num \"1\"))"
|
||||
"(«term_+_» <missing> \"+\" (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)]"
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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])
|
||||
|
|
|
|||
|
|
@ -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 " ---- "
|
||||
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue