chore(tests/lean): remove/fix tests
This commit is contained in:
Leonardo de Moura
parent
3afa4f7ab0
commit
aadb07d5e4
8 changed files with 0 additions and 361 deletions
|
|
@ -1,29 +0,0 @@
|
|||
import init.lean.expander init.io
|
||||
open Lean.Expander -- for coercions
|
||||
open Lean.Parser
|
||||
open Lean.Parser.Term
|
||||
|
||||
local attribute [reducible] MacroScope
|
||||
|
||||
#exit -- Disabled until we implement new VM
|
||||
|
||||
-- TODO(Sebastian): `Syntax.toFormat` should probably propagate scopes by itself in the end
|
||||
|
||||
#eval (do {
|
||||
let stx := review pi {op := Syntax.atom {val := "Π"}, binders := ["a"], range := review sort sort.View.Type},
|
||||
-- tag root with {1}
|
||||
let stx := stx.flipScopes [1],
|
||||
IO.println stx,
|
||||
-- tag root with {2} and propagate once
|
||||
let stx := stx.flipScopes [2],
|
||||
some n ← pure stx.asNode,
|
||||
let stx := Syntax.mkNode n.kind n.args,
|
||||
IO.println stx,
|
||||
-- flip {2}
|
||||
let stx := stx.flipScopes [2],
|
||||
IO.println stx,
|
||||
-- propagate once, only {1} remains
|
||||
some n ← pure stx.asNode,
|
||||
let stx := Syntax.mkNode n.kind n.args,
|
||||
IO.println stx
|
||||
} : ExceptT String IO Unit)
|
||||
|
|
@ -1 +0,0 @@
|
|||
macro_scopes.lean:8:0: warning: using 'exit' to interrupt Lean
|
||||
|
|
@ -1,194 +0,0 @@
|
|||
import init.lean.parser.identifier
|
||||
open Lean.Parser
|
||||
open Lean.Parser.MonadParsec
|
||||
|
||||
def test {α} [DecidableEq α] (p : Parsec' α) (s : String) (e : α) : IO Unit :=
|
||||
match Parsec.parse p s with
|
||||
| Except.ok a := if a = e then pure () else IO.println "unexpected Result"
|
||||
| Except.error e := IO.println e
|
||||
|
||||
def testFailure {α} (p : Parsec' α) (s : String) : IO Unit :=
|
||||
match Parsec.parse p s with
|
||||
| Except.ok a := IO.println "unexpected success"
|
||||
| Except.error e := pure ()
|
||||
|
||||
def showResult {α} [HasToString α] (p : Parsec' α) (s : String) : IO Unit :=
|
||||
match Parsec.parse p s with
|
||||
| Except.ok a := IO.println "Result: " *> IO.println (repr $ toString a)
|
||||
| Except.error e := IO.println e
|
||||
|
||||
#exit -- Disabled until we implement new VM
|
||||
|
||||
#eval test (ch 'a') "a" 'a'
|
||||
#eval test any "a" 'a'
|
||||
#eval test any "b" 'b'
|
||||
#eval test (str "foo" <|> str "bla" <|> str "boo") "bla" "bla"
|
||||
#eval test ((str "foo" *> str "foo") <|> str "bla" <|> str "boo") "bla" "bla"
|
||||
#eval testFailure ((str "foo" *> str "foo") <|> str "foo2" <|> str "boo") "foo2"
|
||||
#eval test (try (str "foo" *> str "foo") <|> str "foo2" <|> str "boo") "foo2" "foo2"
|
||||
#eval test num "1000" 1000
|
||||
#eval test (do n ← num, whitespace, m ← num, pure (n, m)) "1000 200" (1000, 200)
|
||||
#eval test (do n ← num, whitespace, m ← num, pure (n, m)) "1000 200" (1000, 200)
|
||||
#eval test (do n ← lexeme num, m ← num, pure (n, m)) "1000 200" (1000, 200)
|
||||
#eval test (whitespace *> Prod.mk <$> (lexeme num) <*> (lexeme num)) " 1000 200 " (1000, 200)
|
||||
#eval test (whitespace *> Prod.mk <$> (lexeme num) <*> (lexeme num) <* eoi) " 1000 200 " (1000, 200)
|
||||
#eval testFailure (whitespace *> Prod.mk <$> (lexeme num) <*> num <* eoi) " 1000 200 "
|
||||
|
||||
#eval testFailure ((ch 'a' *> ch 'b') <|> (ch 'a' *> ch 'c')) "ac"
|
||||
#eval test ((lookahead (str "ab") *> ch 'a' *> ch 'b') <|> (ch 'a' *> ch 'c')) "ac" 'c'
|
||||
#eval test (str "ab" *> pure () <|> (ch 'a' *> ch 'c' *> pure ())) "ac" ()
|
||||
#eval test (try (ch 'a' *> ch 'b') <|> (ch 'a' *> ch 'c')) "ac" 'c'
|
||||
#eval test (lookahead (ch 'a')) "abc" 'a'
|
||||
#eval testFailure (notFollowedBy (lookahead (ch 'a'))) "abc"
|
||||
|
||||
def symbol (c : Char) : Parsec' Char :=
|
||||
lexeme (ch c) <?> repr c
|
||||
|
||||
def paren {α} (p : Parsec' α) : Parsec' α :=
|
||||
symbol '(' *> lexeme p <* symbol ')'
|
||||
|
||||
#eval test (paren num) "( 10 )" 10
|
||||
#eval test (paren num) "(12)" 12
|
||||
#eval test (paren num) "(0)" 0
|
||||
#eval test (paren num) "(0 )" 0
|
||||
|
||||
def var : Parsec' String :=
|
||||
do c ← satisfy (λ a, a.isAlpha || a = '_'),
|
||||
r ← lexeme $ takeWhile (λ a, a.isDigit || a.isAlpha || a = '_'),
|
||||
pure (c.toString ++ r)
|
||||
|
||||
#eval test var "abc" "abc"
|
||||
#eval test var "_a1Bc" "_a1Bc"
|
||||
#eval test (paren var) "(_a1Bc )" "_a1Bc"
|
||||
#eval testFailure var "1A1Bc"
|
||||
#eval testFailure var "*_a1Bc"
|
||||
#eval test var "abc$" "abc"
|
||||
|
||||
open Lean
|
||||
|
||||
#eval test identifier "«!!aaa».b1'" (mkStrName (mkSimpleName "!!aaa") "b1'")
|
||||
#eval test identifier "a" (mkSimpleName "a")
|
||||
#eval test identifier "a'" (mkSimpleName "a'")
|
||||
#eval test identifier "_" (mkSimpleName "_")
|
||||
#eval test identifier "_a1" (mkSimpleName "_a1")
|
||||
#eval test identifier "aaa.bbb._αc" (mkStrName (mkStrName (mkSimpleName "aaa") "bbb") "_αc")
|
||||
#eval test identifier "«!a!aa».b12.ccc" (mkStrName (mkStrName (mkSimpleName "!a!aa") "b12") "ccc")
|
||||
#eval testFailure identifier "1A1Bc"
|
||||
#eval testFailure identifier "!"
|
||||
#eval testFailure identifier "1"
|
||||
#eval testFailure identifier "'a"
|
||||
#eval testFailure identifier ""
|
||||
#eval testFailure identifier " "
|
||||
|
||||
#eval test parseStringLiteral "\"abc\"" "abc"
|
||||
#eval test parseStringLiteral "\"\\\\abc\"" "\\abc"
|
||||
#eval test parseStringLiteral "\"\"" ""
|
||||
#eval test parseStringLiteral "\"\\\"\"" "\""
|
||||
#eval test parseStringLiteral "\"\\\'\"" "\'"
|
||||
#eval test parseStringLiteral "\"\\n\"" "\n"
|
||||
#eval test parseStringLiteral "\"\\t\"" "\t"
|
||||
#eval test parseStringLiteral "\"\\x4e\"" "N"
|
||||
#eval test parseStringLiteral "\"\\x4E\"" "N"
|
||||
#eval test parseStringLiteral "\"\\x7D\"" "}"
|
||||
#eval test parseStringLiteral "\"\\u03b1\\u03b1\"" "αα"
|
||||
#eval testFailure parseStringLiteral "\"abc"
|
||||
#eval testFailure parseStringLiteral "\"\\abc\""
|
||||
#eval testFailure parseStringLiteral "\"\\x4z\""
|
||||
#eval testFailure parseStringLiteral "\"\\x4\""
|
||||
#eval testFailure parseStringLiteral "\"\\u03b\\u03b1\""
|
||||
#eval testFailure parseStringLiteral "\"\\u03bz\\u03b1\""
|
||||
|
||||
def parseInstrPp : Parsec' String :=
|
||||
do cmd ← Lean.Ir.parseInstr,
|
||||
pure $ toString cmd
|
||||
|
||||
#eval test parseInstrPp "x : UInt32 := 10" "x : UInt32 := 10"
|
||||
#eval test parseInstrPp "x : Bool:=not y" "x : Bool := not y"
|
||||
#eval test parseInstrPp "x : Bool := and z y" "x : Bool := and z y"
|
||||
#eval test parseInstrPp "x := call f z w" "x := call f z w"
|
||||
#eval test parseInstrPp "x := call f z w" "x := call f z w"
|
||||
#eval test parseInstrPp "o := cnstr 0 3 0" "o := cnstr 0 3 0"
|
||||
#eval test parseInstrPp "set o 0 x" "set o 0 x"
|
||||
#eval test parseInstrPp "x := get o 0" "x := get o 0"
|
||||
#eval test parseInstrPp "sset o 8 x" "sset o 8 x"
|
||||
#eval test parseInstrPp "x : Bool := sget o 24" "x : Bool := sget o 24"
|
||||
#eval test parseInstrPp "x := closure f a" "x := closure f a"
|
||||
#eval test parseInstrPp "x := closure f a b" "x := closure f a b"
|
||||
#eval test parseInstrPp "x := apply f a" "x := apply f a"
|
||||
#eval test parseInstrPp "x := Array sz c" "x := Array sz c"
|
||||
#eval test parseInstrPp "arrayWrite a i v" "arrayWrite a i v"
|
||||
#eval test parseInstrPp "x : object := arrayRead a i" "x : object := arrayRead a i"
|
||||
#eval test parseInstrPp "x := sarray UInt32 sz c" "x := sarray UInt32 sz c"
|
||||
#eval test parseInstrPp "arrayWrite a i v" "arrayWrite a i v"
|
||||
#eval test parseInstrPp "x : UInt64 := arrayRead a i" "x : UInt64 := arrayRead a i"
|
||||
#eval test parseInstrPp "inc x" "inc x"
|
||||
#eval test parseInstrPp "dec x" "dec x"
|
||||
#eval test parseInstrPp "decSref x" "decSref x"
|
||||
#eval test parseInstrPp "free x" "free x"
|
||||
#eval test parseInstrPp "x := call f" "x := call f"
|
||||
#eval test parseInstrPp "x:UInt32:= arrayRead y z" "x : UInt32 := arrayRead y z"
|
||||
|
||||
inductive Expr
|
||||
| Add : Expr → Expr → Expr
|
||||
| Num : Nat → Expr
|
||||
| Var : String → Expr
|
||||
|
||||
open Expr
|
||||
|
||||
def eqExpr : Π a b : Expr, Decidable (a = b)
|
||||
| (Var x) (Var y) := if h : x = y then isTrue (h ▸ rfl)
|
||||
else isFalse (λ h', Expr.noConfusion h' (λ h', absurd h' h))
|
||||
| (Var x) (Num n) := isFalse (λ h, Expr.noConfusion h)
|
||||
| (Var x) (Add e₁ e₂) := isFalse (λ h, Expr.noConfusion h)
|
||||
| (Num n) (Num m) := if h : n = m then isTrue (h ▸ rfl)
|
||||
else isFalse (λ h', Expr.noConfusion h' (λ h', absurd h' h))
|
||||
| (Num n) (Var y) := isFalse (λ h, Expr.noConfusion h)
|
||||
| (Num n) (Add e₁ e₂) := isFalse (λ h, Expr.noConfusion h)
|
||||
| (Add e₁ e₂) (Num n) := isFalse (λ h, Expr.noConfusion h)
|
||||
| (Add e₁ e₂) (Var y) := isFalse (λ h, Expr.noConfusion h)
|
||||
| (Add e₁ e₂) (Add e₃ e₄) :=
|
||||
match eqExpr e₁ e₃ with
|
||||
| isTrue h := (match eqExpr e₂ e₄ with
|
||||
| isTrue h' := isTrue (h ▸ h' ▸ rfl)
|
||||
| isFalse h' := isFalse (λ he, Expr.noConfusion he (λ h₁ h₂, absurd h₂ h')))
|
||||
| isFalse h := isFalse (λ he, Expr.noConfusion he (λ h₁ h₂, absurd h₁ h))
|
||||
|
||||
instance : DecidableEq Expr :=
|
||||
{decEq := eqExpr}
|
||||
|
||||
def parseAtom (p : Parsec' Expr) : Parsec' Expr :=
|
||||
(Var <$> lexeme var <?> "variable")
|
||||
<|>
|
||||
(Num <$> lexeme num <?> "numeral")
|
||||
<|>
|
||||
(paren p)
|
||||
|
||||
def parseAdd (p : Parsec' Expr) : Parsec' Expr :=
|
||||
do l ← parseAtom p,
|
||||
(do symbol '+', r ← p, pure $ Add l r) <|> pure l
|
||||
|
||||
def parseExpr : Parsec' Expr :=
|
||||
whitespace *> fix (λ F, parseAdd F) <* eoi
|
||||
|
||||
#eval test parseExpr "10" (Num 10)
|
||||
#eval test parseExpr "(20)" (Num 20)
|
||||
#eval test parseExpr "a" (Var "a")
|
||||
#eval test parseExpr "(20 + a)" (Add (Num 20) (Var "a"))
|
||||
#eval test parseExpr " (20 + (a) + 2 ) " (Add (Num 20) (Add (Var "a") (Num 2)))
|
||||
|
||||
/- Failures -/
|
||||
#print "Failure 1"
|
||||
#eval test parseExpr "(20 +" (Num 0)
|
||||
#print "---------"
|
||||
#print "Failure 2"
|
||||
#eval test parseExpr "" (Num 0)
|
||||
#print "---------"
|
||||
|
||||
namespace paperEx
|
||||
#print "Failure 3"
|
||||
def digit : Parsec' Char := MonadParsec.digit <?> "digit"
|
||||
def letter : Parsec' Char := MonadParsec.alpha <?> "letter"
|
||||
def tst : Parsec' Char := (digit <|> pure '0') *> letter
|
||||
#eval test tst "*" 'a'
|
||||
#print "---------"
|
||||
end paperEx
|
||||
|
|
@ -1 +0,0 @@
|
|||
parsec1.lean:20:0: warning: using 'exit' to interrupt Lean
|
||||
|
|
@ -1,112 +0,0 @@
|
|||
import init.lean.frontend init.io
|
||||
open Lean
|
||||
open Lean.Parser
|
||||
open Lean.Expander
|
||||
open Lean.Elaborator
|
||||
|
||||
#exit -- Test contain many type errors, `#eval` is not working
|
||||
|
||||
def checkReprint (p : List ModuleParserOutput) (s : String) : ExceptT String IO Unit :=
|
||||
do let stx := Syntax.List $ p.map (λ o, o.cmd),
|
||||
let stx := stx.updateLeading s,
|
||||
some s' ← pure $ stx.reprint | IO.println "reprint fail: choice Node",
|
||||
when (s ≠ s') (
|
||||
IO.println "reprint fail:" *>
|
||||
IO.println s'
|
||||
)
|
||||
|
||||
def showResult (p : List moduleParserOutput) (s : String) : ExceptT String IO Unit :=
|
||||
let stx := Syntax.List $ p.map (λ r, r.cmd) in
|
||||
let stx := stx.updateLeading s in
|
||||
let msgs := (do r ← p, r.messages.toList) in
|
||||
match msgs with
|
||||
| [] := do
|
||||
IO.println "Result:",
|
||||
IO.println (toString stx)
|
||||
| msgs := do
|
||||
msgs.mfor $ λ e, IO.println e.toString,
|
||||
IO.println "partial Syntax tree:",
|
||||
IO.println (toString stx)
|
||||
|
||||
def parseModule (s : String) : Except String (List moduleParserOutput) :=
|
||||
do cfg ← mkConfig,
|
||||
(outputs, Sum.inl (), ⟨[]⟩) ← pure $ coroutine.finish (λ_, cfg)
|
||||
(Parser.run cfg s (λ st _, Module.Parser.run st)) cfg
|
||||
| Except.error "final Parser output should be Empty!",
|
||||
pure outputs
|
||||
|
||||
def showParse (s : String) : ExceptT String IO Unit :=
|
||||
do r ← MonadExcept.liftExcept $ parseModule s,
|
||||
checkReprint r s,
|
||||
showResult r s
|
||||
|
||||
#eval showParse "prelude"
|
||||
#eval showParse "import me"
|
||||
#eval showParse "importme"
|
||||
#eval showParse "import"
|
||||
|
||||
#eval showParse "prelude
|
||||
import ..a b
|
||||
import c"
|
||||
|
||||
#eval showParse "open me you"
|
||||
#eval showParse "open me as you (a b c) (renaming a->b c->d) (hiding a b)"
|
||||
#eval showParse "open me you."
|
||||
#eval showParse "open open"
|
||||
#eval showParse "open me import open you"
|
||||
|
||||
#eval showParse "open a
|
||||
section b
|
||||
open c
|
||||
section d
|
||||
open e
|
||||
end d
|
||||
end b"
|
||||
|
||||
-- should not be a Parser error
|
||||
#eval showParse "section a end"
|
||||
|
||||
universes u v
|
||||
#check Type max u v -- eh
|
||||
-- parsed as `Type (max) (u) (v)`, will fail on elaboration ("max: must have at least two arguments", "Function expected at 'Type'", "unknown identifier 'u'/'v'")
|
||||
#eval showParse "#check Type max u v"
|
||||
|
||||
#eval do
|
||||
[header, nota, eoi] ← parseModule "infixl `+`:65 := Nat.add" | throw "huh",
|
||||
Except.ok cmd' ← pure $ (expand nota.cmd).run {filename := "foo", input := "", transformers := builtinTransformers} | throw "heh",
|
||||
pure cmd'.reprint
|
||||
|
||||
-- test overloading
|
||||
#eval do
|
||||
let s := "
|
||||
prelude
|
||||
constant α : Type
|
||||
constant a : α
|
||||
namespace foo
|
||||
constant α : Type
|
||||
end foo
|
||||
constant b : α
|
||||
open foo
|
||||
constant c : α",
|
||||
runFrontend s (IO.println ∘ Message.toString),
|
||||
pure ()
|
||||
|
||||
-- "sticky" `open`
|
||||
#eval do
|
||||
let s := "
|
||||
prelude
|
||||
open foo
|
||||
constant foo.α : Type
|
||||
constant b : α",
|
||||
runFrontend s (IO.println ∘ Message.toString),
|
||||
pure ()
|
||||
|
||||
#exit
|
||||
|
||||
-- slowly progressing...
|
||||
setOption profiler True
|
||||
#eval do
|
||||
s ← IO.Fs.readFile "../../library/init/core.Lean",
|
||||
--let s := (s.mkIterator.nextn 10000).prevToString,
|
||||
runFrontend "core.Lean" s (IO.println ∘ Message.toString),
|
||||
pure ()
|
||||
|
|
@ -1 +0,0 @@
|
|||
parser1.lean:7:0: warning: using 'exit' to interrupt Lean
|
||||
|
|
@ -1,22 +0,0 @@
|
|||
import init.lean.parser.identifier
|
||||
open Lean Lean.Parser
|
||||
|
||||
#exit
|
||||
|
||||
open tactic
|
||||
|
||||
meta def check (s : String) : tactic Unit :=
|
||||
match id.run $ Parsec.parse (identifier : Parsec' _) s with
|
||||
| Except.ok n :=
|
||||
Trace (Name.mangle n) >>
|
||||
if Name.demangle (Name.mangle n) = some n then exact `(True)
|
||||
else Trace ("mangling failed at " ++ s) >> exact `(False)
|
||||
| Except.error ex := Trace ex >> exact `(False)
|
||||
|
||||
example : by check "_αβ" := trivial
|
||||
example : by check "αβ" := trivial
|
||||
example : by check "Nat.add" := trivial
|
||||
example : by check "test.bla.foo" := trivial
|
||||
example : by check "t21'αβ._₁._12" := trivial
|
||||
example : by check "Nat" := trivial
|
||||
example : by check "Nat.equations._eqn1" := trivial
|
||||
|
|
@ -1,4 +1,3 @@
|
|||
import init.lean.parser.parsec
|
||||
universes u v w r s
|
||||
|
||||
set_option trace.compiler.stage1 true
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue