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

fix: tests and elabDo

Browse source
This commit is contained in:
Leonardo de Moura 2020-09-26 19:12:01 -07:00
parent 65be990bdf
commit a0a724ddbd
71 changed files with 535 additions and 532 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
src/Lean/Elab/Do.lean
View file

@ -66,7 +66,7 @@ private partial def expandLiftMethodAux : Syntax → StateT (Array Syntax) Macro
else if k == `Lean.Parser.Term.liftMethod then withFreshMacroScope $ do
let term := args.get! 1;
term ← expandLiftMethodAux term;
auxDo ← `(do a ← $term; $(Syntax.missing));
auxDo ← `(do let a ← $term; $(Syntax.missing));
let auxDoElems := (getDoElems auxDo).pop;
modify $ fun s => s ++ auxDoElems;
`(a)
@ -117,7 +117,9 @@ private partial def expandDoElems : Bool → Array Syntax → Nat → MacroM Syn
rest ← mkRest ();
newBody ← `(let $letDecl:letDecl; $rest);
addPrefix newBody
else if doElem.getKind == `Lean.Parser.Term.doPat then withFreshMacroScope $ do
-- cleanup the following code
else if doElem.getKind == `Lean.Parser.Term.doLetArrow && (doElem.getArg 1).getKind == `Lean.Parser.Term.doPat then withFreshMacroScope $ do
let doElem := doElem.getArg 1;
-- (termParser >> leftArrow) >> termParser >> optional (" | " >> termParser)
let pat := doElem.getArg 0;
let discr := doElem.getArg 2;
@ -125,15 +127,15 @@ private partial def expandDoElems : Bool → Array Syntax → Nat → MacroM Syn
rest ← mkRest ();
newBody ←
if optElse.isNone then do
`(do x ← $discr; match x with | $pat => $rest)
`(do let x ← $discr; match x with | $pat => $rest)
else
let elseBody := optElse.getArg 1;
`(do x ← $discr; match x with | $pat => $rest | _ => $elseBody);
`(do let x ← $discr; match x with | $pat => $rest | _ => $elseBody);
addPrefix newBody
else if i < doElems.size - 1 && doElem.getKind == `Lean.Parser.Term.doExpr then do
-- def doExpr := parser! termParser
let term := doElem.getArg 0;
auxDo ← `(do x ← $term; $(Syntax.missing));
auxDo ← `(do let x ← $term; $(Syntax.missing));
let doElemNew := (getDoElems auxDo).get! 0;
let doElems := doElems.set! i doElemNew;
expandDoElems true doElems (i+2)
@ -193,9 +195,10 @@ private partial def processDoElemsAux (doElems : Array Syntax) (m bindInstVal :
let doElem := doElems.get! i;
let k := doElem.getKind;
withRef doElem $
if k == `Lean.Parser.Term.doId then do
if k == `Lean.Parser.Term.doLetArrow then do
when (i == doElems.size - 1) $
throwError "the last statement in a 'do' block must be an expression";
let doElem := doElem.getArg 1;
-- try (ident >> optType >> leftArrow) >> termParser
let id := doElem.getIdAt 0;
let typeStx := expandOptType doElem (doElem.getArg 1);

8
tests/compiler/termparsertest1.lean
View file

@ -104,14 +104,14 @@ match x with
"¬ a ∧ b",
"
do
x ← f a;
x : Nat ← f a;
let x ← f a;
let x : Nat ← f a;
g x;
let y := g x;
(a, b) <- h x y;
let (a, b) <- h x y;
let (a, b) := (b, a);
pure (a + b)",
"do { x ← f a; pure $ a + a }",
"do { let x ← f a; pure $ a + a }",
"let f : Nat → Nat → Nat
| 0, a => a + 10
| n+1, b => n * b;

18
tests/compiler/termparsertest1.lean.expected.out
View file

@ -265,24 +265,24 @@ let x[i] := f 20; x
(Term.and (Term.not "¬" `a) "∧" `b)
do
x ← f a;
x : Nat ← f a;
let x ← f a;
let x : Nat ← f a;
g x;
let y := g x;
(a, b) <- h x y;
let (a, b) <- h x y;
let (a, b) := (b, a);
pure (a + b)
(Term.do
"do"
[(Term.doId `x [] "←" (Term.app `f [`a]))
[(Term.doLetArrow "let" (Term.doId `x [] "←" (Term.app `f [`a])))
";"
(Term.doId `x [(Term.typeSpec ":" `Nat)] "←" (Term.app `f [`a]))
(Term.doLetArrow "let" (Term.doId `x [(Term.typeSpec ":" `Nat)] "←" (Term.app `f [`a])))
";"
(Term.doExpr (Term.app `g [`x]))
";"
(Term.doLet "let" (Term.letDecl (Term.letIdDecl `y [] [] ":=" (Term.app `g [`x]))))
";"
(Term.doPat (Term.paren "(" [`a [(Term.tupleTail "," [`b])]] ")") "<-" (Term.app `h [`x `y]) [])
(Term.doLetArrow "let" (Term.doPat (Term.paren "(" [`a [(Term.tupleTail "," [`b])]] ")") "<-" (Term.app `h [`x `y]) []))
";"
(Term.doLet
"let"
@ -296,12 +296,14 @@ do
";"
(Term.doExpr (Term.app `pure [(Term.paren "(" [(Term.add `a "+" `b) []] ")")]))]
[])
do { x ← f a; pure $ a + a }
do { let x ← f a; pure $ a + a }
(Term.do
"do"
(Term.doSeqBracketed
"{"
[(Term.doId `x [] "←" (Term.app `f [`a])) ";" (Term.doExpr (Term.dollar `pure "$" (Term.add `a "+" `a)))]
[(Term.doLetArrow "let" (Term.doId `x [] "←" (Term.app `f [`a])))
";"
(Term.doExpr (Term.dollar `pure "$" (Term.add `a "+" `a)))]
"}"))
let f : Nat → Nat → Nat
| 0, a => a + 10

6
tests/lean/IRbug.lean
View file

@ -14,10 +14,10 @@ instance : Monad FooM := {}
def unexpectedBehavior : FooM String := do
let b : Bool := (#[] : Array Nat).isEmpty;
trueBranch ← pure "trueBranch";
falseBranch ← pure "falseBranch";
let trueBranch ← pure "trueBranch";
let falseBranch ← pure "falseBranch";
(1 : Nat).foldM (λ _ (s : String) => do
s ← pure $ if b then trueBranch else falseBranch; pure s) ""
let s ← pure $ if b then trueBranch else falseBranch; pure s) ""
#eval unexpectedBehavior ()

16
tests/lean/PPRoundtrip.lean
View file

@ -9,18 +9,18 @@ open Lean.Format
open Lean.Meta
def check (stx : TermElabM Syntax) (optionsPerPos : OptionsPerPos := {}) : TermElabM Unit := do
opts ← getOptions;
stx ← stx;
e ← elabTermAndSynthesize stx none <* throwErrorIfErrors;
stx' ← liftMetaM $ delab Name.anonymous [] e optionsPerPos;
stx' ← liftCoreM $ PrettyPrinter.parenthesizeTerm stx';
f' ← liftCoreM $ PrettyPrinter.formatTerm stx';
let opts ← getOptions;
let stx ← stx;
let e ← elabTermAndSynthesize stx none <* throwErrorIfErrors;
let stx' ← liftMetaM $ delab Name.anonymous [] e optionsPerPos;
let stx' ← liftCoreM $ PrettyPrinter.parenthesizeTerm stx';
let f' ← liftCoreM $ PrettyPrinter.formatTerm stx';
IO.println $ f'.pretty opts;
env ← getEnv;
let env ← getEnv;
match Parser.runParserCategory env `term (toString f') "<input>" with
| Except.error e => throwErrorAt stx e
| Except.ok stx'' => do
e' ← elabTermAndSynthesize stx'' none <* throwErrorIfErrors;
let e' ← elabTermAndSynthesize stx'' none <* throwErrorIfErrors;
unlessM (isDefEq e e') $
throwErrorAt stx (fmt "failed to round-trip" ++ line ++ fmt e ++ line ++ fmt e')

10
tests/lean/Process.lean
View file

@ -4,27 +4,27 @@ open IO.Process
def usingIO {α} (x : IO α) : IO α := x
#eval usingIO do
child ← spawn { cmd := "sh", args := #["-c", "exit 1"] };
let child ← spawn { cmd := "sh", args := #["-c", "exit 1"] };
child.wait
#eval usingIO do
child ← spawn { cmd := "sh", args := #["-c", "echo hi!"] };
let child ← spawn { cmd := "sh", args := #["-c", "echo hi!"] };
child.wait
#eval usingIO do
child ← spawn { cmd := "sh", args := #["-c", "echo ho!"], stdout := Stdio.piped };
let child ← spawn { cmd := "sh", args := #["-c", "echo ho!"], stdout := Stdio.piped };
child.wait;
child.stdout.readToEnd
#eval usingIO do
child ← spawn { cmd := "head", args := #["-n1"], stdin := Stdio.piped, stdout := Stdio.piped };
let child ← spawn { cmd := "head", args := #["-n1"], stdin := Stdio.piped, stdout := Stdio.piped };
child.stdin.putStrLn "hu!";
child.stdin.flush;
child.wait;
child.stdout.readToEnd
#eval usingIO do
child ← spawn { cmd := "true", stdin := Stdio.piped };
let child ← spawn { cmd := "true", stdin := Stdio.piped };
child.wait;
child.stdin.putStrLn "ha!";
child.stdin.flush <|> IO.println "flush of broken pipe failed"

36
tests/lean/StxQuot.lean
View file

@ -17,25 +17,25 @@ end Syntax
#eval run $ `(fun a => a) >>= pure
#eval run $ `(def foo := 1)
#eval run $ `(def foo := 1 def bar := 2)
#eval run $ do a ← `(Nat.one); `($a)
#eval run $ do a ← `(Nat.one); `(f $a $a)
#eval run $ do a ← `(Nat.one); `(f $ f $a 1)
#eval run $ do a ← `(Nat.one); `(f $(id a))
#eval run $ do a ← `(Nat.one); `($(a).b)
#eval run $ do a ← `(1 + 2); match_syntax a with `($a + $b) => `($b + $a) | _ => pure Syntax.missing
#eval run $ do a ← `(def foo := 1); match_syntax a with `($f:command) => pure f | _ => pure Syntax.missing
#eval run $ do a ← `(def foo := 1 def bar := 2); match_syntax a with `($f:command $g:command) => `($g:command $f:command) | _ => pure Syntax.missing
#eval run $ do let a ← `(Nat.one); `($a)
#eval run $ do let a ← `(Nat.one); `(f $a $a)
#eval run $ do let a ← `(Nat.one); `(f $ f $a 1)
#eval run $ do let a ← `(Nat.one); `(f $(id a))
#eval run $ do let a ← `(Nat.one); `($(a).b)
#eval run $ do let a ← `(1 + 2); match_syntax a with `($a + $b) => `($b + $a) | _ => pure Syntax.missing
#eval run $ do let a ← `(def foo := 1); match_syntax a with `($f:command) => pure f | _ => pure Syntax.missing
#eval run $ do let a ← `(def foo := 1 def bar := 2); match_syntax a with `($f:command $g:command) => `($g:command $f:command) | _ => pure Syntax.missing
#eval run $ do a ← `(aa); match_syntax a with `($id:ident) => pure 0 | `($e) => pure 1 | _ => pure 2
#eval run $ do a ← `(1 + 2); match_syntax a with `($id:ident) => pure 0 | `($e) => pure 1 | _ => pure 2
#eval run $ do params ← #[`(a), `((b : Nat))].mapM id; `(fun $params* => 1)
#eval run $ do a ← `(fun (a : Nat) b => c); match_syntax a with `(fun $aa* => $e) => pure aa | _ => pure #[]
#eval run $ do a ← `(∀ a, c); match_syntax a with `(∀ $id:ident, $e) => pure id | _ => pure a
#eval run $ do a ← `(∀ _, c); match_syntax a with `(∀ $id:ident, $e) => pure id | _ => pure a
#eval run $ do let a ← `(aa); match_syntax a with `($id:ident) => pure 0 | `($e) => pure 1 | _ => pure 2
#eval run $ do let a ← `(1 + 2); match_syntax a with `($id:ident) => pure 0 | `($e) => pure 1 | _ => pure 2
#eval run $ do let params ← #[`(a), `((b : Nat))].mapM id; `(fun $params* => 1)
#eval run $ do let a ← `(fun (a : Nat) b => c); match_syntax a with `(fun $aa* => $e) => pure aa | _ => pure #[]
#eval run $ do let a ← `(∀ a, c); match_syntax a with `(∀ $id:ident, $e) => pure id | _ => pure a
#eval run $ do let a ← `(∀ _, c); match_syntax a with `(∀ $id:ident, $e) => pure id | _ => pure a
-- this one should NOT check the kind of the matched node
#eval run $ do a ← `(∀ _, c); match_syntax a with `(∀ $a, $e) => pure a | _ => pure a
#eval run $ do a ← `(a); match_syntax a with `($id:ident) => pure id | _ => pure a
#eval run $ do a ← `(a.{0}); match_syntax a with `($id:ident) => pure id | _ => pure a
#eval run $ do a ← `(match a with | a => 1 | _ => 2); match_syntax a with `(match $e with $eqns:matchAlt*) => pure eqns | _ => pure #[]
#eval run $ do let a ← `(∀ _, c); match_syntax a with `(∀ $a, $e) => pure a | _ => pure a
#eval run $ do let a ← `(a); match_syntax a with `($id:ident) => pure id | _ => pure a
#eval run $ do let a ← `(a.{0}); match_syntax a with `($id:ident) => pure id | _ => pure a
#eval run $ do let a ← `(match a with | a => 1 | _ => 2); match_syntax a with `(match $e with $eqns:matchAlt*) => pure eqns | _ => pure #[]
end Lean

6
tests/lean/ctor_layout.lean
View file

@ -5,13 +5,13 @@ open Lean.IR
unsafe def main : IO Unit :=
withImportModules [{module := `Lean.Compiler.IR.Basic}] 0 fun env => do
ctorLayout ← IO.ofExcept $ getCtorLayout env `Lean.IR.Expr.reuse;
let ctorLayout ← IO.ofExcept $ getCtorLayout env `Lean.IR.Expr.reuse;
ctorLayout.fieldInfo.forM $ fun finfo => IO.println (format finfo);
IO.println "---";
ctorLayout ← IO.ofExcept $ getCtorLayout env `Lean.EnvironmentHeader.mk;
let ctorLayout ← IO.ofExcept $ getCtorLayout env `Lean.EnvironmentHeader.mk;
ctorLayout.fieldInfo.forM $ fun finfo => IO.println (format finfo);
IO.println "---";
ctorLayout ← IO.ofExcept $ getCtorLayout env `Subtype.mk;
let ctorLayout ← IO.ofExcept $ getCtorLayout env `Subtype.mk;
ctorLayout.fieldInfo.forM $ fun finfo => IO.println (format finfo);
pure ()

2
tests/lean/file_not_found.lean
View file

@ -12,7 +12,7 @@ def usingIO {α} (x : IO α) := x
pure ()
#eval (discard $ IO.FS.Handle.mk "readonly.txt" Mode.write : IO Unit)
#eval usingIO do
h ← IO.FS.Handle.mk "readonly.txt" Mode.read;
let h ← IO.FS.Handle.mk "readonly.txt" Mode.read;
h.putStr "foo";
IO.println "foo";
pure ()

30
tests/lean/ref1.lean
View file

@ -1,24 +1,24 @@
new_frontend
def inc (r : IO.Ref Nat) : IO Unit :=
do v ← r.get;
r.set (v+1);
IO.println (">> " ++ toString v)
def inc (r : IO.Ref Nat) : IO Unit := do
let v ← r.get;
r.set (v+1);
IO.println (">> " ++ toString v)
def initArray (r : IO.Ref (Array Nat)) (n : Nat) : IO Unit :=
n.forM $ fun i => do
r.modify $ fun a => a.push (2*i)
def showArrayRef (r : IO.Ref (Array Nat)) : IO Unit :=
do a ← r.swap ∅;
a.size.forM (fun i => IO.println ("[" ++ toString i ++ "]: " ++ toString (a.get! i)));
_ ← r.swap a;
pure ()
def showArrayRef (r : IO.Ref (Array Nat)) : IO Unit := do
let a ← r.swap ∅;
a.size.forM (fun i => IO.println ("[" ++ toString i ++ "]: " ++ toString (a.get! i)));
r.swap a;
pure ()
def tst (n : Nat) : IO Unit :=
do r₁ ← IO.mkRef 0;
n.forM $ λ _ => inc r₁;
r₂ ← IO.mkRef (∅ : Array Nat);
initArray r₂ n;
showArrayRef r₂
def tst (n : Nat) : IO Unit := do
let r₁ ← IO.mkRef 0;
n.forM fun _ => inc r₁;
let r₂ ← IO.mkRef (∅ : Array Nat);
initArray r₂ n;
showArrayRef r₂
#eval tst 10

2
tests/lean/repr_issue.lean
View file

@ -2,7 +2,7 @@ new_frontend
def foo {m} [Monad m] [MonadExcept String m] [MonadState (Array Nat) m] : m Nat :=
catch (do modify $ fun (a : Array Nat) => a.set! 0 33;
throw "error")
(fun _ => do a ← get; pure $ a.get! 0)
(fun _ => do let a ← get; pure $ a.get! 0)
def ex₁ : StateT (Array Nat) (ExceptT String Id) Nat :=
foo

2
tests/lean/resolveGlobalName.lean
View file

@ -18,7 +18,7 @@ syntax[resolveKind] "#resolve " ident : command
@[commandElab resolveKind] def elabResolve : CommandElab :=
fun stx => liftTermElabM none do
cs ← resolveGlobalName $ stx.getIdAt 1;
let cs ← resolveGlobalName $ stx.getIdAt 1;
Lean.Elab.logInfo $ toString cs;
pure ()

4
tests/lean/run/28.lean
View file

@ -37,8 +37,8 @@ def evalInstr : instr → sim (Option val)
| _, _ => throw (IO.userError "expected pointer value in load" )
| instr.store _ _ _ =>
do pv <- f;
_ <- g;
do let pv <- f;
g;
match pv with
| val.bv 27 _ => throw (IO.userError "asdf")
| _ => throw (IO.userError "expected pointer value in store" )

8
tests/lean/run/DefEqAssignBug.lean
View file

@ -12,16 +12,16 @@ unlessM x $ throwError "check failed"
def tst1 : MetaM Unit := do
let nat := mkConst `Nat;
m1 ← mkFreshExprMVar nat;
m2 ← mkFreshExprMVar (mkArrow nat nat);
let m1 ← mkFreshExprMVar nat;
let m2 ← mkFreshExprMVar (mkArrow nat nat);
withLocalDeclD `x nat $ fun x => do
let t := mkApp m2 x;
check $ isDefEq t m1
def tst2 : MetaM Unit := do
let nat := mkConst `Nat;
m1 ← mkFreshExprMVar nat;
m2 ← mkFreshExprMVar (mkArrow nat nat);
let m1 ← mkFreshExprMVar nat;
let m2 ← mkFreshExprMVar (mkArrow nat nat);
withLocalDeclD `x nat $ fun x => do
let t := mkApp m2 x;
check $ isDefEq m1 t

28
tests/lean/run/IO_test.lean
View file

@ -21,22 +21,22 @@ withFile fn Mode.write fun h => do
h.write xs;
h.write xs;
pure ();
ys ← withFile "foo.txt" Mode.read $ fun h => h.read 10;
let ys ← withFile "foo.txt" Mode.read $ fun h => h.read 10;
check_eq "1" (xs.toList ++ xs.toList) ys.toList;
withFile fn Mode.append fun h => do
h.write ⟨#[5,6,7,8]⟩;
pure ();
withFile "foo.txt" Mode.read fun h => do
ys ← h.read 10;
let ys ← h.read 10;
check_eq "2" [1,2,3,4,1,2,3,4,5,6] ys.toList;
ys ← h.read 2;
let ys ← h.read 2;
check_eq "3" [7,8] ys.toList;
b ← h.isEof;
let b ← h.isEof;
unless (!b)
(throw $ IO.userError $ "wrong (4): ");
ys ← h.read 2;
let ys ← h.read 2;
check_eq "5" [] ys.toList;
b ← h.isEof;
let b ← h.isEof;
unless b
(throw $ IO.userError $ "wrong (6): ");
pure ()
@ -60,26 +60,26 @@ withFile fn2 Mode.write $ fun h => do
h.putStrLn xs₂;
h.putStrLn xs₁;
pure () };
ys ← withFile fn2 Mode.read $ fun h => h.getLine;
let ys ← withFile fn2 Mode.read $ fun h => h.getLine;
IO.println ys;
check_eq "1" (xs₀ ++ xs₀ ++ "\n") ys;
IO.println ys;
withFile fn2 Mode.append $ fun h => do
{ h.putStrLn xs₁;
pure () };
ys ← withFile fn2 Mode.read $ fun h => do
{ ys ← (List.iota 4).mapM $ fun i => do
{ ln ← h.getLine;
let ys ← withFile fn2 Mode.read $ fun h => do
{ let ys ← (List.iota 4).mapM $ fun i => do
{ let ln ← h.getLine;
IO.println i;
IO.println ∘ repr $ ln;
b ← h.isEof;
let b ← h.isEof;
unless (i == 1 || !b) (throw $ IO.userError "isEof");
pure ln };
pure ys };
IO.println ys;
let rs := [xs₀ ++ xs₀ ++ "\n", xs₂ ++ "\n", xs₁ ++ "\n", xs₁ ++ "\n"];
check_eq "2" rs ys;
ys ← readFile fn2;
let ys ← readFile fn2;
check_eq "3" (String.join rs) ys;
pure ()
@ -94,7 +94,7 @@ let xs₃ := "world";
withFile fn3 Mode.write $ fun h => do {
pure ()
};
ys ← lines fn3;
let ys ← lines fn3;
IO.println $ repr ys;
check_eq "1" ys #[];
withFile fn3 Mode.write $ fun h => do
@ -102,7 +102,7 @@ withFile fn3 Mode.write $ fun h => do
h.putStrLn xs₁;
h.putStrLn xs₂;
h.putStrLn xs₃ };
ys ← lines fn3;
let ys ← lines fn3;
IO.println $ repr ys;
check_eq "2" ys #[xs₀, xs₁, xs₂, xs₃];
pure ()

4
tests/lean/run/LiftMethodIssue.lean
View file

@ -1,11 +1,11 @@
new_frontend
def tst : IO (Option Nat) := do
x? : Option Nat ← pure none;
let x? : Option Nat ← pure none;
pure x?
def tst2 (x : Nat) : IO (Option Nat) := do
x? : Option Nat ← pure x;
let x? : Option Nat ← pure x;
(if x?.isNone then
/-
We need the `some` because we propagate the expected type at `pure` applications.

6
tests/lean/run/Reformat.lean
View file

@ -11,9 +11,9 @@ let (debug, f) : Bool × String := match args with
| [f, "-d"] => (true, f)
| [f] => (false, f)
| _ => panic! "usage: file [-d]";
env ← mkEmptyEnvironment;
stx ← Lean.Parser.parseFile env args.head!;
(f, _) ← (finally (PrettyPrinter.ppModule stx) printTraces).toIO { options := Options.empty.setBool `trace.PrettyPrinter.parenthesize debug } { env := env };
let env ← mkEmptyEnvironment;
let stx ← Lean.Parser.parseFile env args.head!;
let (f, _) ← (finally (PrettyPrinter.ppModule stx) printTraces).toIO { options := Options.empty.setBool `trace.PrettyPrinter.parenthesize debug } { env := env };
IO.print f;
--stx' ← Lean.Parser.parseModule env args.head! (toString f);
pure ()

14
tests/lean/run/Reparen.lean
View file

@ -22,24 +22,24 @@ let (debug, f) : Bool × String := match args with
| [f, "-d"] => (true, f)
| [f] => (false, f)
| _ => panic! "usage: file [-d]";
env ← mkEmptyEnvironment;
stx ← Lean.Parser.parseFile env args.head!;
let env ← mkEmptyEnvironment;
let stx ← Lean.Parser.parseFile env args.head!;
let header := stx.getArg 0;
some s ← pure header.reprint | throw $ IO.userError "header reprint failed";
let some s ← pure header.reprint | throw $ IO.userError "header reprint failed";
IO.print s;
let cmds := (stx.getArg 1).getArgs;
cmds.forM $ fun cmd => do
let cmd := unparen cmd;
(cmd, _) ← (finally (PrettyPrinter.parenthesizeCommand cmd) printTraces).toIO { options := Options.empty.setBool `trace.PrettyPrinter.parenthesize debug } { env := env };
some s ← pure cmd.reprint | throw $ IO.userError "cmd reprint failed";
let (cmd, _) ← (finally (PrettyPrinter.parenthesizeCommand cmd) printTraces).toIO { options := Options.empty.setBool `trace.PrettyPrinter.parenthesize debug } { env := env };
let some s ← pure cmd.reprint | throw $ IO.userError "cmd reprint failed";
IO.print s
#eval main ["../../../src/Init/Core.lean"]
def check (stx : Syntax) : CoreM Unit := do
let stx' := unparen stx;
stx' ← PrettyPrinter.parenthesizeTerm stx';
f ← PrettyPrinter.formatTerm stx';
let stx' ← PrettyPrinter.parenthesizeTerm stx';
let f ← PrettyPrinter.formatTerm stx';
IO.println f;
when (stx != stx') $
throwError "reparenthesization failed"

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

@ -26,7 +26,7 @@ instance : Enumerable Bool :=
{ elems := [false, true] }
instance {α β} [Enumerable α] [Enumerable β]: Enumerable (α × β) :=
{ elems := do a ← Enumerable.elems α; b ← Enumerable.elems β; pure (a, b) }
{ elems := do let a ← Enumerable.elems α; let b ← Enumerable.elems β; pure (a, b) }
partial def finElemsAux (n : Nat) : (i : Nat) → i < n → List (Fin n)
| 0, h => [⟨0, h⟩]

2
tests/lean/run/catchThe.lean
View file

@ -8,7 +8,7 @@ universes u v w
abbrev M := ExceptT String $ MetaM
def testM {α} [HasBeq α] [HasToString α] (x : M α) (expected : α) : MetaM Unit := do
r ← x;
let r ← x;
match r with
| Except.ok a => unless (a == expected) $ throwError ("unexpected result " ++ toString a)
| Except.error e => throwError ("FAILED: " ++ e)

2
tests/lean/run/choiceExpectedTypeBug.lean
View file

@ -22,7 +22,7 @@ open Lean.Elab.Term
@[termElab emptyS] def elabEmptyS : TermElab :=
fun stx expectedType? => do
tryPostponeIfNoneOrMVar expectedType?;
stxNew ← `(Nat.zero);
let stxNew ← `(Nat.zero);
withMacroExpansion stx stxNew $ elabTerm stxNew expectedType?
def foo (x : Unit) := x

14
tests/lean/run/closure1.lean
View file

@ -14,21 +14,21 @@ set_option trace.Meta.debug true
def mkArrow (d b : Expr) : Expr := mkForall `_ BinderInfo.default d b
def printDef (declName : Name) : MetaM Unit := do
cinfo ← getConstInfo declName;
let cinfo ← getConstInfo declName;
trace! `Meta.debug cinfo.value!
def tst1 : MetaM Unit := do
let u := mkLevelParam `u;
let v := mkLevelMVar `v;
m1 ← mkFreshExprMVar (mkSort levelOne);
let m1 ← mkFreshExprMVar (mkSort levelOne);
withLocalDeclD `α (mkSort u) $ fun α => do
withLocalDeclD `β (mkSort v) $ fun β => do
m2 ← mkFreshExprMVar (mkArrow α m1);
let m2 ← mkFreshExprMVar (mkArrow α m1);
withLocalDeclD `a α $ fun a => do
withLocalDeclD `f (mkArrow α α) $ fun f => do
withLetDecl `b α (mkApp f a) $ fun b => do
let t := mkApp m2 (mkApp f b);
e ← mkAuxDefinitionFor `foo1 t;
let e ← mkAuxDefinitionFor `foo1 t;
trace! `Meta.debug e;
printDef `foo1;
pure ()
@ -41,11 +41,11 @@ withLocalDeclD `α (mkSort (mkLevelSucc u)) $ fun α => do
withLocalDeclD `v1 (mkApp2 (mkConst `Vec [u]) α (mkNatLit 10)) $ fun v1 =>
withLetDecl `n (mkConst `Nat) (mkNatLit 10) $ fun n =>
withLocalDeclD `v2 (mkApp2 (mkConst `Vec [u]) α n) $ fun v2 => do
m ← mkFreshExprMVar (mkArrow (mkApp2 (mkConst `Vec [u]) α (mkNatLit 10)) (mkSort levelZero));
let m ← mkFreshExprMVar (mkArrow (mkApp2 (mkConst `Vec [u]) α (mkNatLit 10)) (mkSort levelZero));
withLocalDeclD `p (mkSort levelZero) $ fun p => do
t ← mkEq v1 v2;
let t ← mkEq v1 v2;
let t := mkApp2 (mkConst `And) t (mkApp2 (mkConst `Or) (mkApp m v2) p);
e ← mkAuxDefinitionFor `foo2 t;
let e ← mkAuxDefinitionFor `foo2 t;
trace! `Meta.debug e;
printDef `foo2;
pure ()

5
tests/lean/run/coeIssues4.lean
View file

@ -2,9 +2,8 @@ new_frontend
def f : List Int → Bool := fun _ => true
def ex3 : IO Bool :=
do
xs ← pure [1, 2, 3];
def ex3 : IO Bool := do
let xs ← pure [1, 2, 3];
pure $ f xs -- Works
inductive Expr

15
tests/lean/run/core.lean
View file

@ -3,14 +3,13 @@ new_frontend
open Lean
open Lean.Core
def f : CoreM Nat := do {
env ← getEnv;
cinfo ← getConstInfo `Nat.add;
trace! `Elab "trace message";
liftIO $ IO.println $ toString cinfo.type;
liftIO $ IO.println "testing...";
pure 10
}
def f : CoreM Nat := do
let env ← getEnv;
let cinfo ← getConstInfo `Nat.add;
trace! `Elab "trace message";
IO.println $ toString cinfo.type;
IO.println "testing...";
pure 10;
#eval f

58
tests/lean/run/depElim1.lean
View file

@ -25,13 +25,13 @@ inductive ArrayLit3 {α : Sort u} (a b c : α) : Type u | mk : ArrayLit3 a b c
inductive ArrayLit4 {α : Sort u} (a b c d : α) : Type u | mk : ArrayLit4 a b c d
private def getConstructorVal (ctorName : Name) (fn : Expr) (args : Array Expr) : MetaM (Option (ConstructorVal × Expr × Array Expr)) := do
env ← getEnv;
let env ← getEnv;
match env.find? ctorName with
| some (ConstantInfo.ctorInfo v) => if args.size == v.nparams + v.nfields then pure $ some (v, fn, args) else pure none
| _ => pure none
private def constructorApp? (e : Expr) : MetaM (Option (ConstructorVal × Expr × Array Expr)) := do
env ← getEnv;
let env ← getEnv;
match e with
| Expr.lit (Literal.natVal n) _ =>
if n == 0 then getConstructorVal `Nat.zero (mkConst `Nat.zero) #[] else getConstructorVal `Nat.succ (mkConst `Nat.succ) #[mkNatLit (n-1)]
@ -53,7 +53,7 @@ partial def mkPattern : Expr → MetaM Pattern
else if e.isAppOfArity `As 3 && (e.getArg! 1).isFVar then do
let v := e.getArg! 1;
let p := e.getArg! 2;
p ← mkPattern p;
let p ← mkPattern p;
pure $ Pattern.as v.fvarId! p
else if e.isAppOfArity `ArrayLit0 1 ||
e.isAppOfArity `ArrayLit1 2 ||
@ -63,64 +63,64 @@ partial def mkPattern : Expr → MetaM Pattern
let args := e.getAppArgs;
let type := args.get! 0;
let ps := args.extract 1 args.size;
ps ← ps.toList.mapM mkPattern;
let ps ← ps.toList.mapM mkPattern;
pure $ Pattern.arrayLit type ps
else match e.arrayLit? with
| some (_, es) => do
pats ← es.mapM mkPattern;
type ← inferType e;
type ← whnfD type;
let pats ← es.mapM mkPattern;
let type ← inferType e;
let type ← whnfD type;
let elemType := type.appArg!;
pure $ Pattern.arrayLit elemType pats
| none => do
e ← whnfD e;
r? ← constructorApp? e;
let e ← whnfD e;
let r? ← constructorApp? e;
match r? with
| none => throwError "unexpected pattern"
| some (cval, fn, args) => do
let params := args.extract 0 cval.nparams;
let fields := args.extract cval.nparams args.size;
pats ← fields.toList.mapM mkPattern;
let pats ← fields.toList.mapM mkPattern;
pure $ Pattern.ctor cval.name fn.constLevels! params.toList pats
partial def decodePats : Expr → MetaM (List Pattern)
| e =>
match e.app2? `Pat with
| some (_, pat) => do pat ← mkPattern pat; pure [pat]
| some (_, pat) => do let pat ← mkPattern pat; pure [pat]
| none =>
match e.prod? with
| none => throwError "unexpected pattern"
| some (pat, pats) => do
pat ← decodePats pat;
pats ← decodePats pats;
let pat ← decodePats pat;
let pats ← decodePats pats;
pure (pat ++ pats)
partial def decodeAltLHS (e : Expr) : MetaM AltLHS :=
forallTelescopeReducing e fun args body => do
decls ← args.toList.mapM (fun arg => getLocalDecl arg.fvarId!);
pats ← decodePats body;
let decls ← args.toList.mapM (fun arg => getLocalDecl arg.fvarId!);
let pats ← decodePats body;
pure { ref := Syntax.missing, fvarDecls := decls, patterns := pats }
partial def decodeAltLHSs : Expr → MetaM (List AltLHS)
| e =>
match e.app2? `LHS with
| some (_, lhs) => do lhs ← decodeAltLHS lhs; pure [lhs]
| some (_, lhs) => do let lhs ← decodeAltLHS lhs; pure [lhs]
| none =>
match e.prod? with
| none => throwError "unexpected LHS"
| some (lhs, lhss) => do
lhs ← decodeAltLHSs lhs;
lhss ← decodeAltLHSs lhss;
let lhs ← decodeAltLHSs lhs;
let lhss ← decodeAltLHSs lhss;
pure (lhs ++ lhss)
def withDepElimFrom {α} (declName : Name) (numPats : Nat) (k : List FVarId → List AltLHS → MetaM α) : MetaM α := do
cinfo ← getConstInfo declName;
let cinfo ← getConstInfo declName;
forallTelescopeReducing cinfo.type fun args body =>
if args.size < numPats then
throwError "insufficient number of parameters"
else do
let xs := (args.extract (args.size - numPats) args.size).toList.map $ Expr.fvarId!;
alts ← decodeAltLHSs body;
let alts ← decodeAltLHSs body;
k xs alts
inductive LHS {α : Sort u} (a : α) : Type u
@ -140,11 +140,11 @@ registerTraceClass `Meta.mkElim
private def getUnusedLevelParam (majors : List Expr) (lhss : List AltLHS) : MetaM Level := do
let s : CollectLevelParams.State := {};
s ← majors.foldlM
let s ← majors.foldlM
(fun s major => do
major ← instantiateMVars major;
majorType ← inferType major;
majorType ← instantiateMVars majorType;
let major ← instantiateMVars major;
let majorType ← inferType major;
let majorType ← instantiateMVars majorType;
let s := collectLevelParams s major;
pure $ collectLevelParams s majorType)
s;
@ -155,30 +155,30 @@ private def mkElimSort (majors : List Expr) (lhss : List AltLHS) (inProp : Bool)
if inProp then
pure $ mkSort $ levelZero
else do
v ← getUnusedLevelParam majors lhss;
let v ← getUnusedLevelParam majors lhss;
pure $ mkSort $ v
def mkTester (elimName : Name) (majors : List Expr) (lhss : List AltLHS) (inProp : Bool := false) : MetaM MatcherResult := do
generalizeTelescope majors.toArray `_d fun majors => do
let resultType := if inProp then mkConst `True /- some proposition -/ else mkConst `Nat;
matchType ← mkForallFVars majors resultType;
let matchType ← mkForallFVars majors resultType;
Match.mkMatcher elimName matchType majors.size lhss
def test (ex : Name) (numPats : Nat) (elimName : Name) (inProp : Bool := false) : MetaM Unit :=
withDepElimFrom ex numPats fun majors alts => do
let majors := majors.map mkFVar;
trace! `Meta.debug ("majors: " ++ majors.toArray);
r ← mkTester elimName majors alts inProp;
let r ← mkTester elimName majors alts inProp;
unless r.counterExamples.isEmpty $
throwError ("missing cases:" ++ Format.line ++ counterExamplesToMessageData r.counterExamples);
unless r.unusedAltIdxs.isEmpty $
throwError ("unused alternatives: " ++ toString (r.unusedAltIdxs.map fun idx => "#" ++ toString (idx+1)));
cinfo ← getConstInfo elimName;
let cinfo ← getConstInfo elimName;
IO.println (toString cinfo.name ++ " : " ++ toString cinfo.type);
pure ()
def testFailure (ex : Name) (numPats : Nat) (elimName : Name) (inProp : Bool := false) : MetaM Unit := do
worked ← catch (do test ex numPats elimName inProp; pure true) (fun ex => pure false);
let worked ← catch (do test ex numPats elimName inProp; pure true) (fun ex => pure false);
when worked $ throwError "unexpected success"
def ex0 (x : Nat) : LHS (forall (y : Nat), Pat y)

2
tests/lean/run/deriv.lean
View file

@ -93,5 +93,5 @@ do
unsafe def main : IO Unit :=
do let x := Var "x";
let f := pow x x;
_ ← nest deriv 9 f;
nest deriv 9 f;
pure ()

26
tests/lean/run/doNotation1.lean
View file

@ -16,9 +16,9 @@ p.1
set_option trace.Elab.definition true
def h (x : Nat) : StateT Nat IO Nat := do
s ← get;
a ← f; -- liftM inserted here
b ← g1 1; -- liftM inserted here
let s ← get;
let a ← f; -- liftM inserted here
let b ← g1 1; -- liftM inserted here
let x := g2 b;
IO.println b;
pure (s+a);
@ -27,9 +27,9 @@ def myPrint {α} [HasToString α] (a : α) : IO Unit :=
IO.println (">> " ++ toString a)
def h₂ (x : Nat) : StateT Nat IO Nat := do
a ← h 1; -- liftM inserted here
let a ← h 1; -- liftM inserted here
IO.println x;
b ← g1 a; -- liftM inserted here
let b ← g1 a; -- liftM inserted here
when (a > 100) $ throw $ IO.userError "Error";
myPrint b.1; -- liftM inserted here
pure (a + 1)
@ -43,9 +43,9 @@ let m2 (y : Nat) := do { -- Type inferred from application below
h (x+y); -- liftM inserted here
myPrint y -- liftM inserted here
};
a ← h 1; -- liftM inserted here
let a ← h 1; -- liftM inserted here
IO.println x;
b ← g1 a; -- liftM inserted here
let b ← g1 a; -- liftM inserted here
when (a > 100) $ throw $ IO.userError "Error";
myPrint b.1; -- liftM inserted here
m1;
@ -53,14 +53,14 @@ m2 a;
pure 1
def tst0 : IO Unit := do {
a ← f;
let a ← f;
let x := a + 1;
IO.println "hello";
IO.println x;
}
def tst1 : IO Unit := do
a ← f;
let a ← f;
let x := a + 1;
IO.println "hello";
IO.println x;
@ -74,8 +74,8 @@ def tst3 : IO Unit := do
(if (← g 1) > 0 then
IO.println "gt"
else do
x ← f;
y ← g x;
let x ← f;
let y ← g x;
IO.println y)
def pred (x : Nat) : IO Bool := do
@ -102,13 +102,13 @@ partial def expandHash : Syntax → StateT Bool MacroM Syntax
| Syntax.node k args =>
if k == `doHash then do set true; `(←MonadState.get)
else do
args ← args.mapM expandHash;
let args ← args.mapM expandHash;
pure $ Syntax.node k args;
| stx => pure stx
@[macro Lean.Parser.Term.do] def expandDo : Macro :=
fun stx => do
(stx, expanded) ← expandHash stx false;
let (stx, expanded) ← expandHash stx false;
(if expanded then pure stx
else Macro.throwUnsupported)

6
tests/lean/run/elabCmd.lean
View file

@ -6,7 +6,7 @@ open Lean.Elab
open Lean.Elab.Term
def getCtors (c : Name) : TermElabM (List Name) := do
env ← getEnv;
let env ← getEnv;
match env.find? c with
| some (ConstantInfo.inductInfo val) =>
pure val.ctors
@ -15,10 +15,10 @@ match env.find? c with
def elabAnonCtor (args : Syntax) (τ : Expr) : TermElabM Expr := do
match τ.getAppFn with
| Expr.const C _ _ => do
ctors ← getCtors C;
let ctors ← getCtors C;
match ctors with
| [c] => do
stx ← `($(Lean.mkIdent c) $(Array.getSepElems args.getArgs)*);
let stx ← `($(Lean.mkIdent c) $(Array.getSepElems args.getArgs)*);
elabTerm stx τ
-- error handling
| _ => unreachable!

6
tests/lean/run/elab_cmd.lean
View file

@ -6,11 +6,11 @@ open Lean.Elab.Term
open Lean.Elab.Command
elab "∃" b:term "," P:term : term => do
ex ← `(Exists (fun $b => $P));
let ex ← `(Exists (fun $b => $P));
elabTerm ex none
elab "#check2" b:term : command => do
cmd ← `(#check $b #check $b);
let cmd ← `(#check $b #check $b);
elabCommand cmd
#check ∃ x, x > 0
@ -20,7 +20,7 @@ elab "#check2" b:term : command => do
#check2 10
elab "try" t:tactic : tactic => do
t' ← `(tactic| $t <|> skip);
let t' ← `(tactic| $t <|> skip);
Lean.Elab.Tactic.evalTactic t'
theorem tst (x y z : Nat) : y = z → x = x → x = y → x = z :=

4
tests/lean/run/eval_unboxed_const.lean
View file

@ -6,7 +6,7 @@ open Lean
def c1 : Bool := true
unsafe def tst1 : CoreM Unit := do
env ← getEnv;
let env ← getEnv;
let v := env.evalConst Bool `c1;
IO.println v
@ -15,7 +15,7 @@ IO.println v
def c2 : Bool := false
unsafe def tst2 : CoreM Unit := do
env ← getEnv;
let env ← getEnv;
let v := env.evalConst Bool `c2;
IO.println v

6
tests/lean/run/evalconst.lean
View file

@ -5,7 +5,7 @@ open Lean
def x := 10
unsafe def tst : CoreM Unit := do
env ← getEnv;
let env ← getEnv;
IO.println $ env.evalConst Nat `x;
pure ()
@ -14,8 +14,8 @@ pure ()
def f (x : Nat) := x + 1
unsafe def tst2 : CoreM Unit := do
env ← getEnv;
f ← liftIO $ IO.ofExcept $ env.evalConst (Nat → Nat) `f;
let env ← getEnv;
let f ← liftIO $ IO.ofExcept $ env.evalConst (Nat → Nat) `f;
IO.println $ (f 10);
pure ()

10
tests/lean/run/finally.lean
View file

@ -17,7 +17,7 @@ catch
(fun _ => get)
def checkE {α ε : Type} [HasBeq α] (x : IO (Except ε α)) (expected : α) : IO Unit := do
r ← x;
let r ← x;
match r with
| Except.ok a => unless (a == expected) $ throw $ IO.userError "unexpected result"
| Except.error _ => throw $ IO.userError "unexpected error"
@ -47,10 +47,10 @@ catchThe IO.Error
#eval checkE ((tst3.run).run' 0) 101
def tst4 : M Nat := do
a ← finally
let a ← finally
(finally (pure 42) (do set 100; IO.println "inner finisher executed"; pure ()))
(do modify Nat.succ; IO.println "outer finisher executed");
s ← get;
let s ← get;
pure (a + s)
#eval (tst4.run).run' 0
@ -58,13 +58,13 @@ pure (a + s)
#eval checkE ((tst4.run).run' 0) 143
def tst5 : M Nat := do
(a, _) ← finally' (pure 42) (fun a? => do IO.println ("finalizer received: " ++ toString a?));
let (a, _) ← finally' (pure 42) (fun a? => do IO.println ("finalizer received: " ++ toString a?));
pure a
#eval (tst5.run).run' 0
def tst6 : M Nat := do
(a, _) ← finally' f2 (fun a? => do IO.println ("finalizer received: " ++ toString a?));
let (a, _) ← finally' f2 (fun a? => do IO.println ("finalizer received: " ++ toString a?));
pure a
def tst7 : IO Unit :=

16
tests/lean/run/frontend1.lean
View file

@ -3,14 +3,14 @@ new_frontend
open Lean
open Lean.Elab
def run (input : String) (failIff : Bool := true) : CoreM Unit :=
do env ← getEnv;
opts ← getOptions;
(env, messages) ← liftIO $ process input env opts;
messages.forM $ fun msg => (liftIO msg.toString) >>= IO.println;
when (failIff && messages.hasErrors) $ throwError "errors have been found";
when (!failIff && !messages.hasErrors) $ throwError "there are no errors";
pure ()
def run (input : String) (failIff : Bool := true) : CoreM Unit := do
let env ← getEnv;
let opts ← getOptions;
let (env, messages) ← liftIO $ process input env opts;
messages.forM $ fun msg => (liftIO msg.toString) >>= IO.println;
when (failIff && messages.hasErrors) $ throwError "errors have been found";
when (!failIff && !messages.hasErrors) $ throwError "there are no errors";
pure ()
def fail (input : String) : CoreM Unit :=
run input false

10
tests/lean/run/generalizeTelescope.lean
View file

@ -18,7 +18,7 @@ let n1 := mkApp succ n;
let vecN1 := mkApp2 (mkConst `Vec) nat n1;
withLocalDeclD `xs vecN1 $ fun xs => do
generalizeTelescope #[n1, xs] `aux $ fun ys => do
t ← mkLambdaFVars ys ys.back;
let t ← mkLambdaFVars ys ys.back;
trace! `Meta.debug t;
pure ()
@ -31,9 +31,9 @@ withLocalDeclD `n nat $ fun n => do
let n1 := mkApp succ n;
let vecN1 := mkApp2 (mkConst `Vec) nat n1;
withLocalDeclD `xs vecN1 $ fun xs => do
e ← mkEqRefl xs;
let e ← mkEqRefl xs;
generalizeTelescope #[n1, xs, e] `aux $ fun ys => do
t ← mkLambdaFVars ys ys.back;
let t ← mkLambdaFVars ys ys.back;
trace! `Meta.debug t;
pure ()
@ -48,10 +48,10 @@ withLocalDeclD `n nat $ fun n => do
let n1 := mkApp succ n;
let vecN1 := mkApp2 (mkConst `Vec) nat n1;
withLocalDeclD `xs vecN1 $ fun xs => do
e ← mkEqRefl xs;
let e ← mkEqRefl xs;
failIfSuccess $ do {
generalizeTelescope #[n1, e] `aux $ fun ys => do
t ← mkLambdaFVars ys ys.back;
let t ← mkLambdaFVars ys ys.back;
trace! `Meta.debug t;
pure ()
};

10
tests/lean/run/genindices.lean
View file

@ -11,14 +11,14 @@ open Lean
open Lean.Meta
def tst1 : MetaM Unit := do
cinfo ← getConstInfo `goal;
let cinfo ← getConstInfo `goal;
let type := cinfo.type;
mvar ← mkFreshExprMVar type;
let mvar ← mkFreshExprMVar type;
trace! `Elab (MessageData.ofGoal mvar.mvarId!);
(_, mvarId) ← introN mvar.mvarId! 2;
(fvarId, mvarId) ← intro1 mvarId;
let (_, mvarId) ← introN mvar.mvarId! 2;
let (fvarId, mvarId) ← intro1 mvarId;
trace! `Elab (MessageData.ofGoal mvarId);
s ← generalizeIndices mvarId fvarId;
let s ← generalizeIndices mvarId fvarId;
trace! `Elab (MessageData.ofGoal s.mvarId);
pure ()

6
tests/lean/run/getline_crash.lean
View file

@ -5,7 +5,7 @@ let path := "tmp_file";
IO.FS.withFile path IO.FS.Mode.write $ λ (h : IO.FS.Handle) =>
h.putStrLn str;
IO.FS.withFile path IO.FS.Mode.read $ λ (h : IO.FS.Handle) => do
str' ← h.getLine;
let str' ← h.getLine;
IO.println str.length;
IO.println str'.length;
IO.print str';
@ -20,8 +20,8 @@ IO.FS.withFile path IO.FS.Mode.write $ λ (h : IO.FS.Handle) => do {
h.putStrLn str1; h.putStr str2
};
IO.FS.withFile path IO.FS.Mode.read $ λ (h : IO.FS.Handle) => do
str1' ← h.getLine;
str2' ← h.getLine;
let str1' ← h.getLine;
let str2' ← h.getLine;
unless (str1'.length == str1.length + 1) $
throw (IO.userError ("unexpected length: " ++ toString str1'.trim.length));
unless (str1'.trim == str1) $

10
tests/lean/run/irCompilerBug.lean
View file

@ -17,17 +17,17 @@ inductive T
@[noinline] def foo (p : Payload) : Option T :=
(do
i ← get? p 1;
let i ← get? p 1;
pure (T.a i))
<|> (do
i ← get? p 2;
let i ← get? p 2;
pure (T.b i))
<|> (do
i ← get? p 3;
let i ← get? p 3;
pure (T.c i))
<|> (do
i ← get? p 4;
i ← get? p 5;
let i ← get? p 4;
let i ← get? p 5;
pure (T.d i))
def wrongOutput : String :=

2
tests/lean/run/kernel1.lean
View file

@ -3,7 +3,7 @@ new_frontend
open Lean
def checkDefEq (a b : Name) : CoreM Unit := do
env ← getEnv;
let env ← getEnv;
let a := mkConst a;
let b := mkConst b;
let r := Kernel.isDefEq env {} a b;

4
tests/lean/run/kernel2.lean
View file

@ -3,14 +3,14 @@ new_frontend
open Lean
def checkDefEq (a b : Name) : CoreM Unit := do
env ← getEnv;
let env ← getEnv;
let a := mkConst a;
let b := mkConst b;
let r := Kernel.isDefEq env {} a b;
IO.println (toString a ++ " =?= " ++ toString b ++ " := " ++ toString r)
def whnf (a : Name) : CoreM Unit := do
env ← getEnv;
let env ← getEnv;
let a := mkConst a;
let r := Kernel.whnf env {} a;
IO.println (toString a ++ " ==> " ++ toString r)

2
tests/lean/run/matchNoPostponing.lean
View file

@ -6,5 +6,5 @@ new_frontend
`mkMatcher` assumes `matchType` does not contain metavariables.
We accomplish that by invoking `synthesizeSyntheticMVarsNoPostponing` at `elabMatch`. -/
def foo : IO Unit := do
(x, y) ← pure (0, 0);
let (x, y) ← pure (0, 0);
IO.println x

6
tests/lean/run/meta1.lean
View file

@ -5,17 +5,17 @@ open Lean.Meta
unsafe def tstInferType (mods : List Name) (e : Expr) : IO Unit :=
withImportModules (mods.map $ fun m => {module := m}) 0 fun env => do
(type, _, _) ← (inferType e : MetaM _).toIO {} { env := env } {} {};
let (type, _, _) ← (inferType e : MetaM _).toIO {} { env := env } {} {};
IO.println (toString e ++ " : " ++ toString type)
unsafe def tstWHNF (mods : List Name) (e : Expr) (t := TransparencyMode.default) : IO Unit :=
withImportModules (mods.map $ fun m => {module := m}) 0 fun env => do
(s, _, _) ← (whnf e : MetaM _).toIO {} { env := env };
let (s, _, _) ← (whnf e : MetaM _).toIO {} { env := env };
IO.println (toString e ++ " ==> " ++ toString s)
unsafe def tstIsProp (mods : List Name) (e : Expr) : IO Unit :=
withImportModules (mods.map $ fun m => {module := m}) 0 fun env => do
(b, _, _) ← (isProp e : MetaM _).toIO {} { env := env };
let (b, _, _) ← (isProp e : MetaM _).toIO {} { env := env };
IO.println (toString e ++ ", isProp: " ++ toString b)
def t1 : Expr :=

290
tests/lean/run/meta2.lean
View file

@ -15,7 +15,7 @@ def check (x : MetaM Bool) : MetaM Unit :=
unlessM x $ throwError "check failed"
def getAssignment (m : Expr) : MetaM Expr :=
do v? ← getExprMVarAssignment? m.mvarId!;
do let v? ← getExprMVarAssignment? m.mvarId!;
match v? with
| some v => pure v
| none => throwError "metavariable is not assigned"
@ -32,7 +32,7 @@ def boolTrue := mkConst `Bool.true
def tst1 : MetaM Unit :=
do print "----- tst1 -----";
mvar ← mkFreshExprMVar nat;
let mvar <- mkFreshExprMVar nat;
check $ isExprDefEq mvar (mkNatLit 10);
check $ isExprDefEq mvar (mkNatLit 10);
pure ()
@ -41,7 +41,7 @@ do print "----- tst1 -----";
def tst2 : MetaM Unit :=
do print "----- tst2 -----";
mvar ← mkFreshExprMVar nat;
let mvar <- mkFreshExprMVar nat;
check $ isExprDefEq (mkApp succ mvar) (mkApp succ (mkNatLit 10));
check $ isExprDefEq mvar (mkNatLit 10);
pure ()
@ -51,12 +51,12 @@ do print "----- tst2 -----";
def tst3 : MetaM Unit :=
do print "----- tst3 -----";
let t := mkLambda `x BinderInfo.default nat $ mkBVar 0;
mvar ← mkFreshExprMVar (mkForall `x BinderInfo.default nat nat);
let mvar <- mkFreshExprMVar (mkForall `x BinderInfo.default nat nat);
lambdaTelescope t fun xs _ => do
let x := xs.get! 0;
check $ isExprDefEq (mkApp mvar x) (mkAppN add #[x, mkAppN add #[mkNatLit 10, x]]);
pure ();
v ← getAssignment mvar;
let v <- getAssignment mvar;
print v;
pure ()
@ -67,11 +67,11 @@ do print "----- tst4 -----";
let t := mkLambda `x BinderInfo.default nat $ mkBVar 0;
lambdaTelescope t fun xs _ => do
let x := xs.get! 0;
mvar ← mkFreshExprMVar (mkForall `x BinderInfo.default nat nat);
let mvar <- mkFreshExprMVar (mkForall `x BinderInfo.default nat nat);
-- the following `isExprDefEq` fails because `x` is also in the context of `mvar`
check $ not <$> isExprDefEq (mkApp mvar x) (mkAppN add #[x, mkAppN add #[mkNatLit 10, x]]);
check $ approxDefEq $ isExprDefEq (mkApp mvar x) (mkAppN add #[x, mkAppN add #[mkNatLit 10, x]]);
v ← getAssignment mvar;
let v <- getAssignment mvar;
print v;
pure ();
pure ()
@ -79,7 +79,7 @@ do print "----- tst4 -----";
#eval tst4
def mkAppC (c : Name) (xs : Array Expr) : MetaM Expr :=
do r ← mkAppM c xs;
do let r <- mkAppM c xs;
check r;
pure r
@ -90,23 +90,23 @@ def mkSnd (s : Expr) : MetaM Expr := mkAppC `Prod.snd #[s]
def tst5 : MetaM Unit :=
do print "----- tst5 -----";
p₁ ← mkPair (mkNatLit 1) (mkNatLit 2);
x ← mkFst p₁;
let p₁ <- mkPair (mkNatLit 1) (mkNatLit 2);
let x <- mkFst p₁;
print x;
v ← whnf x;
let v <- whnf x;
print v;
v ← withTransparency TransparencyMode.reducible $ whnf x;
let v <- withTransparency TransparencyMode.reducible $ whnf x;
print v;
x ← mkId x;
let x <- mkId x;
print x;
prod ← mkProd nat nat;
m ← mkFreshExprMVar prod;
y ← mkFst m;
let prod <- mkProd nat nat;
let m <- mkFreshExprMVar prod;
let y <- mkFst m;
check $ isExprDefEq y x;
print y;
x ← mkProjection p₁ `fst;
let x <- mkProjection p₁ `fst;
print x;
y ← mkProjection p₁ `snd;
let y <- mkProjection p₁ `snd;
print y
#eval tst5
@ -114,22 +114,22 @@ do print "----- tst5 -----";
def tst6 : MetaM Unit :=
do print "----- tst6 -----";
withLocalDeclD `x nat $ fun x => do
m ← mkFreshExprMVar nat;
let m <- mkFreshExprMVar nat;
let t := mkAppN add #[m, mkNatLit 4];
let s := mkAppN add #[x, mkNatLit 3];
check $ not <$> isExprDefEq t s;
let s := mkAppN add #[x, mkNatLit 6];
check $ isExprDefEq t s;
v ← getAssignment m;
let v <- getAssignment m;
check $ pure $ v == mkAppN add #[x, mkNatLit 2];
print v;
m ← mkFreshExprMVar nat;
let m <- mkFreshExprMVar nat;
let t := mkAppN add #[m, mkNatLit 4];
let s := mkNatLit 3;
check $ not <$> isExprDefEq t s;
let s := mkNatLit 10;
check $ isExprDefEq t s;
v ← getAssignment m;
let v <- getAssignment m;
check $ pure $ v == mkNatLit 6;
print v;
pure ()
@ -141,15 +141,15 @@ def mkArrow (d b : Expr) : Expr := mkForall `_ BinderInfo.default d b
def tst7 : MetaM Unit :=
do print "----- tst7 -----";
withLocalDeclD `x type $ fun x => do
m1 ← mkFreshExprMVar (mkArrow type type);
m2 ← mkFreshExprMVar type;
let m1 <- mkFreshExprMVar (mkArrow type type);
let m2 <- mkFreshExprMVar type;
let t := mkApp io x;
-- we need to use foApprox to solve `?m1 ?m2 =?= IO x`
check $ not <$> isDefEq (mkApp m1 m2) t;
check $ approxDefEq $ isDefEq (mkApp m1 m2) t;
v ← getAssignment m1;
let v <- getAssignment m1;
check $ pure $ v == io;
v ← getAssignment m2;
let v <- getAssignment m2;
check $ pure $ v == x;
pure ()
@ -159,11 +159,11 @@ def tst8 : MetaM Unit :=
do print "----- tst8 -----";
let add := mkAppN (mkConst `HasAdd.add [levelOne]) #[nat, mkConst `Nat.HasAdd];
let t := mkAppN add #[mkNatLit 2, mkNatLit 3];
t ← withTransparency TransparencyMode.reducible $ whnf t;
let t <- withTransparency TransparencyMode.reducible $ whnf t;
print t;
t ← whnf t;
let t <- whnf t;
print t;
t ← reduce t;
let t <- reduce t;
print t;
pure ()
@ -171,7 +171,7 @@ do print "----- tst8 -----";
def tst9 : MetaM Unit :=
do print "----- tst9 -----";
env ← getEnv;
let env <- getEnv;
print (toString $ Lean.isReducible env `Prod.fst);
print (toString $ Lean.isReducible env `HasAdd.add);
pure ()
@ -180,12 +180,12 @@ do print "----- tst9 -----";
def tst10 : MetaM Unit :=
do print "----- tst10 -----";
t ← withLocalDeclD `x nat $ fun x => do {
let t <- withLocalDeclD `x nat $ fun x => do {
let b := mkAppN add #[x, mkAppN add #[mkNatLit 2, mkNatLit 3]];
mkLambdaFVars #[x] b
};
print t;
t ← reduce t;
let t <- reduce t;
print t;
pure ()
@ -201,8 +201,8 @@ do print "----- tst11 -----";
check $ not <$> isType x;
check $ not <$> (mkLambdaFVars #[x] x >>= isType);
check $ not <$> (mkLambdaFVars #[x] nat >>= isType);
t ← mkEq x (mkNatLit 0);
(t, _) ← mkForallUsedOnly #[x] t;
let t <- mkEq x (mkNatLit 0);
let (t, _) <- mkForallUsedOnly #[x] t;
print t;
check $ isType t;
pure ();
@ -213,9 +213,9 @@ do print "----- tst11 -----";
def tst12 : MetaM Unit :=
do print "----- tst12 -----";
withLocalDeclD `x nat $ fun x => do
t ← mkEqRefl x >>= mkLambdaFVars #[x];
let t <- mkEqRefl x >>= mkLambdaFVars #[x];
print t;
type ← inferType t;
let type <- inferType t;
print type;
isProofQuick t >>= fun b => print (toString b);
isProofQuick nat >>= fun b => print (toString b);
@ -227,13 +227,13 @@ do print "----- tst12 -----";
def tst13 : MetaM Unit :=
do print "----- tst13 -----";
m₁ ← mkFreshExprMVar (mkArrow type type);
m₂ ← mkFreshExprMVar (mkApp m₁ nat);
t ← mkId m₂;
let m₁ <- mkFreshExprMVar (mkArrow type type);
let m₂ <- mkFreshExprMVar (mkApp m₁ nat);
let t <- mkId m₂;
print t;
r ← abstractMVars t;
let r <- abstractMVars t;
print r.expr;
(_, _, e) ← openAbstractMVarsResult r;
let (_, _, e) <- openAbstractMVarsResult r;
print e;
pure ()
@ -246,11 +246,11 @@ def mkHasToString (a : Expr) : MetaM Expr := mkAppC `HasToString #[a]
def tst14 : MetaM Unit :=
do print "----- tst14 -----";
stateM ← mkStateM nat;
let stateM <- mkStateM nat;
print stateM;
monad ← mkMonad stateM;
globalInsts ← getGlobalInstances;
insts ← globalInsts.getUnify monad;
let monad <- mkMonad stateM;
let globalInsts <- getGlobalInstances;
let insts <- globalInsts.getUnify monad;
print insts;
pure ()
@ -258,8 +258,8 @@ do print "----- tst14 -----";
def tst15 : MetaM Unit :=
do print "----- tst15 -----";
inst ← mkHasAdd nat;
r ← synthInstance inst;
let inst <- mkHasAdd nat;
let r <- synthInstance inst;
print r;
pure ()
@ -267,10 +267,10 @@ do print "----- tst15 -----";
def tst16 : MetaM Unit :=
do print "----- tst16 -----";
prod ← mkProd nat nat;
inst ← mkHasToString prod;
let prod <- mkProd nat nat;
let inst <- mkHasToString prod;
print inst;
r ← synthInstance inst;
let r <- synthInstance inst;
print r;
pure ()
@ -278,11 +278,11 @@ do print "----- tst16 -----";
def tst17 : MetaM Unit :=
do print "----- tst17 -----";
prod ← mkProd nat nat;
prod ← mkProd boolE prod;
inst ← mkHasToString prod;
let prod <- mkProd nat nat;
let prod <- mkProd boolE prod;
let inst <- mkHasToString prod;
print inst;
r ← synthInstance inst;
let r <- synthInstance inst;
print r;
pure ()
@ -290,8 +290,8 @@ do print "----- tst17 -----";
def tst18 : MetaM Unit :=
do print "----- tst18 -----";
decEqNat ← mkDecEq nat;
r ← synthInstance decEqNat;
let decEqNat <- mkDecEq nat;
let r <- synthInstance decEqNat;
print r;
pure ()
@ -299,11 +299,11 @@ do print "----- tst18 -----";
def tst19 : MetaM Unit :=
do print "----- tst19 -----";
stateM ← mkStateM nat;
let stateM <- mkStateM nat;
print stateM;
monad ← mkMonad stateM;
let monad <- mkMonad stateM;
print monad;
r ← synthInstance monad;
let r <- synthInstance monad;
print r;
pure ()
@ -311,11 +311,11 @@ do print "----- tst19 -----";
def tst20 : MetaM Unit :=
do print "----- tst20 -----";
stateM ← mkStateM nat;
let stateM <- mkStateM nat;
print stateM;
monadState ← mkMonadState nat stateM;
let monadState <- mkMonadState nat stateM;
print monadState;
r ← synthInstance monadState;
let r <- synthInstance monadState;
print r;
pure ()
@ -326,21 +326,21 @@ do print "----- tst21 -----";
withLocalDeclD `x nat $ fun x => do
withLocalDeclD `y nat $ fun y => do
withLocalDeclD `z nat $ fun z => do
eq₁ ← mkEq x y;
eq₂ ← mkEq y z;
let eq₁ <- mkEq x y;
let eq₂ <- mkEq y z;
withLocalDeclD `h₁ eq₁ $ fun h₁ => do
withLocalDeclD `h₂ eq₂ $ fun h₂ => do
h ← mkEqTrans h₁ h₂;
h ← mkEqSymm h;
h ← mkCongrArg succ h;
h₂ ← mkEqRefl succ;
h ← mkCongr h₂ h;
t ← inferType h;
let h <- mkEqTrans h₁ h₂;
let h <- mkEqSymm h;
let h <- mkCongrArg succ h;
let h₂ <- mkEqRefl succ;
let h <- mkCongr h₂ h;
let t <- inferType h;
check h;
print h;
print t;
h ← mkCongrFun h₂ x;
t ← inferType h;
let h <- mkCongrFun h₂ x;
let t <- inferType h;
check h;
print t;
pure ()
@ -351,11 +351,11 @@ def tst22 : MetaM Unit :=
do print "----- tst22 -----";
withLocalDeclD `x nat $ fun x => do
withLocalDeclD `y nat $ fun y => do
t ← mkAppC `HasAdd.add #[x, y];
let t <- mkAppC `HasAdd.add #[x, y];
print t;
t ← mkAppC `HasAdd.add #[y, x];
let t <- mkAppC `HasAdd.add #[y, x];
print t;
t ← mkAppC `HasToString.toString #[x];
let t <- mkAppC `HasToString.toString #[x];
print t;
pure ()
@ -365,7 +365,7 @@ def test1 : Nat := (fun x y => x + y) 0 1
def tst23 : MetaM Unit :=
do print "----- tst23 -----";
cinfo ← getConstInfo `test1;
let cinfo <- getConstInfo `test1;
let v := cinfo.value?.get!;
print v;
print v.headBeta
@ -374,10 +374,10 @@ do print "----- tst23 -----";
def tst24 : MetaM Unit :=
do print "----- tst24 -----";
m1 ← mkFreshExprMVar (mkArrow nat (mkArrow type type));
m2 ← mkFreshExprMVar type;
zero ← mkAppM `HasZero.zero #[nat];
idNat ← mkAppM `Id #[nat];
let m1 <- mkFreshExprMVar (mkArrow nat (mkArrow type type));
let m2 <- mkFreshExprMVar type;
let zero <- mkAppM `HasZero.zero #[nat];
let idNat <- mkAppM `Id #[nat];
let lhs := mkAppB m1 zero m2;
print zero;
print idNat;
@ -392,19 +392,19 @@ do print "----- tst25 -----";
withLocalDeclD `α type $ fun α =>
withLocalDeclD `β type $ fun β =>
withLocalDeclD `σ type $ fun σ => do {
(t1, n) ← mkForallUsedOnly #[α, β, σ] $ mkArrow α β;
let (t1, n) <- mkForallUsedOnly #[α, β, σ] $ mkArrow α β;
print t1;
check $ pure $ n == 2;
(t2, n) ← mkForallUsedOnly #[α, β, σ] $ mkArrow α (mkArrow β σ);
let (t2, n) <- mkForallUsedOnly #[α, β, σ] $ mkArrow α (mkArrow β σ);
check $ pure $ n == 3;
print t2;
(t3, n) ← mkForallUsedOnly #[α, β, σ] $ α;
let (t3, n) <- mkForallUsedOnly #[α, β, σ] $ α;
check $ pure $ n == 1;
print t3;
(t4, n) ← mkForallUsedOnly #[α, β, σ] $ σ;
let (t4, n) <- mkForallUsedOnly #[α, β, σ] $ σ;
check $ pure $ n == 1;
print t4;
(t5, n) ← mkForallUsedOnly #[α, β, σ] $ nat;
let (t5, n) <- mkForallUsedOnly #[α, β, σ] $ nat;
check $ pure $ n == 0;
print t5;
pure ()
@ -415,11 +415,11 @@ do print "----- tst25 -----";
def tst26 : MetaM Unit := do
print "----- tst26 -----";
m1 ← mkFreshExprMVar (mkArrow nat nat);
m2 ← mkFreshExprMVar nat;
m3 ← mkFreshExprMVar nat;
let m1 <- mkFreshExprMVar (mkArrow nat nat);
let m2 <- mkFreshExprMVar nat;
let m3 <- mkFreshExprMVar nat;
check $ approxDefEq $ isDefEq (mkApp m1 m2) m3;
check $ do { b ← isExprMVarAssigned $ m1.mvarId!; pure (!b) };
check $ do { let b <- isExprMVarAssigned $ m1.mvarId!; pure (!b) };
check $ isExprMVarAssigned $ m3.mvarId!;
pure ()
@ -435,7 +435,7 @@ set_option trace.Meta.isDefEq.assign true
def tst27 : MetaM Unit := do
print "----- tst27 -----";
m ← mkFreshExprMVar nat;
let m <- mkFreshExprMVar nat;
check $ isDefEq (mkNatLit 1) (mkApp (mkConst `Nat.succ) m);
pure ()
@ -447,19 +447,19 @@ print "----- tst28 -----";
withLocalDeclD `x nat $ fun x =>
withLocalDeclD `y nat $ fun y =>
withLocalDeclD `z nat $ fun z => do
t1 ← mkAppM `HasAdd.add #[x, y];
t1 ← mkAppM `HasAdd.add #[x, t1];
t1 ← mkAppM `HasAdd.add #[t1, t1];
t2 ← mkAppM `HasAdd.add #[z, y];
t3 ← mkAppM `Eq #[t2, t1];
t3 ← mkForallFVars #[z] t3;
m ← mkFreshExprMVar nat;
p ← mkAppM `HasAdd.add #[x, m];
let t1 <- mkAppM `HasAdd.add #[x, y];
let t1 <- mkAppM `HasAdd.add #[x, t1];
let t1 <- mkAppM `HasAdd.add #[t1, t1];
let t2 <- mkAppM `HasAdd.add #[z, y];
let t3 <- mkAppM `Eq #[t2, t1];
let t3 <- mkForallFVars #[z] t3;
let m <- mkFreshExprMVar nat;
let p <- mkAppM `HasAdd.add #[x, m];
print t3;
r ← kabstract t3 p;
let r <- kabstract t3 p;
print r;
p ← mkAppM `HasAdd.add #[x, y];
r ← kabstract t3 p;
let p <- mkAppM `HasAdd.add #[x, y];
let r <- kabstract t3 p;
print r;
pure ()
@ -495,15 +495,15 @@ pure ()
def tst30 : MetaM Unit := do
print "----- tst30 -----";
m1 ← mkFreshExprMVar nat;
m2 ← mkFreshExprMVar (mkArrow nat nat);
let m1 <- mkFreshExprMVar nat;
let m2 <- mkFreshExprMVar (mkArrow nat nat);
withLocalDeclD `x nat $ fun x => do
let t := mkApp succ $ mkApp m2 x;
print t;
check $ approxDefEq $ isDefEq m1 t;
r ← instantiateMVars m1;
let r <- instantiateMVars m1;
print r;
r ← instantiateMVars m2;
let r <- instantiateMVars m2;
print r;
pure ()
@ -511,7 +511,7 @@ withLocalDeclD `x nat $ fun x => do
def tst31 : MetaM Unit := do
print "----- tst31 -----";
m ← mkFreshExprMVar nat;
let m <- mkFreshExprMVar nat;
let t := mkLet `x nat zero m;
print t;
check $ isDefEq t m;
@ -521,15 +521,15 @@ def tst32 : MetaM Unit := do
print "----- tst32 -----";
withLocalDeclD `a nat $ fun a => do
withLocalDeclD `b nat $ fun b => do
aeqb ← mkEq a b;
let aeqb <- mkEq a b;
withLocalDeclD `h2 aeqb $ fun h2 => do
t ← mkEq (mkApp2 add a a) a;
let t <- mkEq (mkApp2 add a a) a;
print t;
let motive := mkLambda `x BinderInfo.default nat (mkApp3 (mkConst `Eq [levelOne]) nat (mkApp2 add a (mkBVar 0)) a);
withLocalDeclD `h1 t $ fun h1 => do
r ← mkEqNDRec motive h1 h2;
let r <- mkEqNDRec motive h1 h2;
print r;
rType ← inferType r >>= whnf;
let rType <- inferType r >>= whnf;
print rType;
check r;
pure ()
@ -540,17 +540,17 @@ def tst33 : MetaM Unit := do
print "----- tst33 -----";
withLocalDeclD `a nat $ fun a => do
withLocalDeclD `b nat $ fun b => do
aeqb ← mkEq a b;
let aeqb <- mkEq a b;
withLocalDeclD `h2 aeqb $ fun h2 => do
t ← mkEq (mkApp2 add a a) a;
let t <- mkEq (mkApp2 add a a) a;
let motive :=
mkLambda `x BinderInfo.default nat $
mkLambda `h BinderInfo.default (mkApp3 (mkConst `Eq [levelOne]) nat a (mkBVar 0)) $
(mkApp3 (mkConst `Eq [levelOne]) nat (mkApp2 add a (mkBVar 1)) a);
withLocalDeclD `h1 t $ fun h1 => do
r ← mkEqRec motive h1 h2;
let r <- mkEqRec motive h1 h2;
print r;
rType ← inferType r >>= whnf;
let rType <- inferType r >>= whnf;
print rType;
check r;
pure ()
@ -561,8 +561,8 @@ def tst34 : MetaM Unit := do
print "----- tst34 -----";
let type := mkSort levelOne;
withLocalDeclD `α type $ fun α => do
m ← mkFreshExprMVar type;
t ← mkLambdaFVars #[α] (mkArrow m m);
let m <- mkFreshExprMVar type;
let t <- mkLambdaFVars #[α] (mkArrow m m);
print t;
pure ()
@ -573,15 +573,15 @@ def tst35 : MetaM Unit := do
print "----- tst35 -----";
let type := mkSort levelOne;
withLocalDeclD `α type $ fun α => do
m1 ← mkFreshExprMVar type;
m2 ← mkFreshExprMVar (mkArrow nat type);
let m1 <- mkFreshExprMVar type;
let m2 <- mkFreshExprMVar (mkArrow nat type);
let v := mkLambda `x BinderInfo.default nat m1;
assignExprMVar m2.mvarId! v;
let w := mkApp m2 zero;
t1 ← mkLambdaFVars #[α] (mkArrow w w);
let t1 <- mkLambdaFVars #[α] (mkArrow w w);
print t1;
m3 ← mkFreshExprMVar type;
t2 ← mkLambdaFVars #[α] (mkArrow (mkBVar 0) (mkBVar 1));
let m3 <- mkFreshExprMVar type;
let t2 <- mkLambdaFVars #[α] (mkArrow (mkBVar 0) (mkBVar 1));
print t2;
check $ isDefEq t1 t2;
pure ()
@ -592,10 +592,10 @@ withLocalDeclD `α type $ fun α => do
def tst36 : MetaM Unit := do
print "----- tst36 -----";
let type := mkSort levelOne;
m1 ← mkFreshExprMVar (mkArrow type type);
let m1 <- mkFreshExprMVar (mkArrow type type);
withLocalDeclD `α type $ fun α => do
m2 ← mkFreshExprMVar type;
t ← mkAppM `Id #[m2];
let m2 <- mkFreshExprMVar type;
let t <- mkAppM `Id #[m2];
check $ approxDefEq $ isDefEq (mkApp m1 α) t;
check $ approxDefEq $ isDefEq m1 (mkConst `Id [levelZero]);
pure ()
@ -604,11 +604,11 @@ withLocalDeclD `α type $ fun α => do
def tst37 : MetaM Unit := do
print "----- tst37 -----";
m1 ← mkFreshExprMVar (mkArrow nat (mkArrow type type));
m2 ← mkFreshExprMVar (mkArrow nat type);
let m1 <- mkFreshExprMVar (mkArrow nat (mkArrow type type));
let m2 <- mkFreshExprMVar (mkArrow nat type);
withLocalDeclD `v nat $ fun v => do
let lhs := mkApp2 m1 v (mkApp m2 v);
rhs ← mkAppM `StateM #[nat, nat];
let rhs <- mkAppM `StateM #[nat, nat];
print lhs;
print rhs;
check $ approxDefEq $ isDefEq lhs rhs;
@ -618,11 +618,11 @@ withLocalDeclD `v nat $ fun v => do
def tst38 : MetaM Unit := do
print "----- tst38 -----";
m1 ← mkFreshExprMVar nat;
let m1 <- mkFreshExprMVar nat;
withLocalDeclD `x nat $ fun x => do
m2 ← mkFreshExprMVar type;
let m2 <- mkFreshExprMVar type;
withLocalDeclD `y m2 $ fun y => do
m3 ← mkFreshExprMVar (mkArrow m2 nat);
let m3 <- mkFreshExprMVar (mkArrow m2 nat);
let rhs := mkApp m3 y;
check $ approxDefEq $ isDefEq m2 nat;
print m2;
@ -643,10 +643,10 @@ def tst39 : MetaM Unit := do
print "----- tst39 -----";
withLocalDeclD `α type $ fun α =>
withLocalDeclD `β type $ fun β => do
p ← mkProd α β;
t ← mkForallFVars #[α, β] p;
let p <- mkProd α β;
let t <- mkForallFVars #[α, β] p;
print t;
e ← instantiateForall t #[nat, boolE];
let e <- instantiateForall t #[nat, boolE];
print e;
pure ()
@ -660,9 +660,9 @@ withLocalDeclD `β type $ fun β =>
withLocalDeclD `a α $ fun a =>
withLocalDeclD `b β $ fun b =>
do
p ← mkProd α β;
t1 ← mkForallFVars #[α, β] p;
t2 ← mkForallFVars #[α, β, a, b] p;
let p <- mkProd α β;
let t1 <- mkForallFVars #[α, β] p;
let t2 <- mkForallFVars #[α, β, a, b] p;
print t1;
print $ toString $ t1.bindingBody!.hasLooseBVarInExplicitDomain 0 false;
print $ toString $ t1.bindingBody!.hasLooseBVarInExplicitDomain 0 true;
@ -697,24 +697,24 @@ structure C (α : Type u) extends A α, B α :=
def mkA (x y : Expr) : MetaM Expr := mkAppC `A.mk #[x, y]
def mkB (z : Expr) : MetaM Expr := mkAppC `B.mk #[z]
def mkC (x y z w : Expr) : MetaM Expr := do
a ← mkA x y;
b ← mkB z;
let a <- mkA x y;
let b <- mkB z;
mkAppC `C.mk #[a, b, w]
def tst41 : MetaM Unit := do
print "----- tst41 -----";
c ← mkC (mkNatLit 1) (mkNatLit 2) (mkNatLit 3) boolTrue;
let c <- mkC (mkNatLit 1) (mkNatLit 2) (mkNatLit 3) boolTrue;
print c;
x ← mkProjection c `x;
let x <- mkProjection c `x;
check x;
print x;
y ← mkProjection c `y;
let y <- mkProjection c `y;
check y;
print y;
z ← mkProjection c `z;
let z <- mkProjection c `z;
check z;
print z;
w ← mkProjection c `w;
let w <- mkProjection c `w;
check w;
print w;
pure ()
@ -728,10 +728,10 @@ set_option pp.all false
def tst42 : MetaM Unit := do
print "----- tst42 -----";
t ← mkListLit nat [mkNatLit 1, mkNatLit 2];
let t <- mkListLit nat [mkNatLit 1, mkNatLit 2];
print t;
check t;
t ← mkArrayLit nat [mkNatLit 1, mkNatLit 2];
let t <- mkArrayLit nat [mkNatLit 1, mkNatLit 2];
print t;
check t;
match t.arrayLit? with

28
tests/lean/run/meta3.lean
View file

@ -16,7 +16,7 @@ def check (x : MetaM Bool) : MetaM Unit :=
unlessM x $ throwError "check failed"
def getAssignment (m : Expr) : MetaM Expr :=
do v? ← getExprMVarAssignment? m.mvarId!;
do let v? ← getExprMVarAssignment? m.mvarId!;
match v? with
| some v => pure v
| none => throwError "metavariable is not assigned"
@ -24,7 +24,7 @@ do v? ← getExprMVarAssignment? m.mvarId!;
unsafe def run (mods : List Name) (x : MetaM Unit) (opts : Options := dbgOpt) : IO Unit :=
withImportModules (mods.map $ fun m => {module := m}) 0 fun env => do
let x : MetaM Unit := do { x; printTraces };
_ ← x.toIO { options := opts } { env := env };
x.toIO { options := opts } { env := env };
pure ()
def nat := mkConst `Nat
@ -33,26 +33,26 @@ def add := mkAppN (mkConst `HasAdd.add [levelZero]) #[nat, mkConst `Nat.HasAdd]
def tst1 : MetaM Unit :=
do let d : DiscrTree Nat := {};
mvar ← mkFreshExprMVar nat;
d ← d.insert (mkAppN add #[mvar, mkNatLit 10]) 1;
d ← d.insert (mkAppN add #[mkNatLit 0, mkNatLit 10]) 2;
d ← d.insert (mkAppN (mkConst `Nat.add) #[mkNatLit 0, mkNatLit 20]) 3;
d ← d.insert (mkAppN add #[mvar, mkNatLit 20]) 4;
d ← d.insert mvar 5;
let mvar ← mkFreshExprMVar nat;
let d ← d.insert (mkAppN add #[mvar, mkNatLit 10]) 1;
let d ← d.insert (mkAppN add #[mkNatLit 0, mkNatLit 10]) 2;
let d ← d.insert (mkAppN (mkConst `Nat.add) #[mkNatLit 0, mkNatLit 20]) 3;
let d ← d.insert (mkAppN add #[mvar, mkNatLit 20]) 4;
let d ← d.insert mvar 5;
print (format d);
vs ← d.getMatch (mkAppN add #[mkNatLit 1, mkNatLit 10]);
let vs ← d.getMatch (mkAppN add #[mkNatLit 1, mkNatLit 10]);
print (format vs);
let t := mkAppN add #[mvar, mvar];
print t;
vs ← d.getMatch t;
let vs ← d.getMatch t;
print (format vs);
vs ← d.getUnify t;
let vs ← d.getUnify t;
print (format vs);
vs ← d.getUnify mvar;
let vs ← d.getUnify mvar;
print (format vs);
vs ← d.getUnify $ mkAppN add #[mkNatLit 0, mvar];
let vs ← d.getUnify $ mkAppN add #[mkNatLit 0, mvar];
print (format vs);
vs ← d.getUnify $ mkAppN add #[mvar, mkNatLit 20];
let vs ← d.getUnify $ mkAppN add #[mvar, mkNatLit 20];
print (format vs);
pure ()

12
tests/lean/run/meta4.lean
View file

@ -14,23 +14,23 @@ axiom Ax : forall (α β : Type), α → β → DecidableEq β
set_option trace.Meta.debug true
def tst1 : MetaM Unit := do
cinfo ← getConstInfo `Ax;
(_, _, e) ← forallMetaTelescopeReducing cinfo.type (some 0);
let cinfo ← getConstInfo `Ax;
let (_, _, e) ← forallMetaTelescopeReducing cinfo.type (some 0);
check (pure (!e.hasMVar));
print e;
(_, _, e) ← forallMetaTelescopeReducing cinfo.type (some 1);
let (_, _, e) ← forallMetaTelescopeReducing cinfo.type (some 1);
check (pure e.hasMVar);
check (pure e.isForall);
print e;
(_, _, e) ← forallMetaTelescopeReducing cinfo.type (some 5);
let (_, _, e) ← forallMetaTelescopeReducing cinfo.type (some 5);
check (pure e.hasMVar);
check (pure e.isForall);
print e;
(_, _, e) ← forallMetaTelescopeReducing cinfo.type (some 6);
let (_, _, e) ← forallMetaTelescopeReducing cinfo.type (some 6);
check (pure e.hasMVar);
check (pure (!e.isForall));
print e;
(_, _, e') ← forallMetaTelescopeReducing cinfo.type;
let (_, _, e') ← forallMetaTelescopeReducing cinfo.type;
print e';
check (isDefEq e e');
forallBoundedTelescope cinfo.type (some 0) $ fun xs body => check (pure (xs.size == 0));

6
tests/lean/run/meta5.lean
View file

@ -6,15 +6,15 @@ open Lean.Meta
def tst1 : MetaM Unit :=
withLocalDeclD `y (mkConst `Nat) $ fun y => do
withLetDecl `x (mkConst `Nat) (mkNatLit 0) $ fun x => do {
mvar ← mkFreshExprMVar (mkConst `Nat) MetavarKind.syntheticOpaque;
let mvar ← mkFreshExprMVar (mkConst `Nat) MetavarKind.syntheticOpaque;
trace! `Meta mvar;
r ← mkLambdaFVars #[y, x] mvar;
let r ← mkLambdaFVars #[y, x] mvar;
trace! `Meta r;
let v := mkApp2 (mkConst `Nat.add) x y;
assignExprMVar mvar.mvarId! v;
trace! `Meta mvar;
trace! `Meta r;
mctx ← getMCtx;
let mctx ← getMCtx;
mctx.decls.forM $ fun mvarId mvarDecl => do {
trace! `Meta ("?" ++ mvarId ++ " : " ++ mvarDecl.type);
pure ()

36
tests/lean/run/meta6.lean
View file

@ -20,7 +20,7 @@ def mkArrow (d b : Expr) : Expr := mkForall `_ BinderInfo.default d b
def tst1 : MetaM Unit := do
print "----- tst1 -----";
m1 ← mkFreshExprMVar (mkArrow nat nat);
let m1 ← mkFreshExprMVar (mkArrow nat nat);
let lhs := mkApp m1 zero;
let rhs := zero;
check $ fullApproxDefEq $ isDefEq lhs rhs;
@ -34,9 +34,9 @@ set_option trace.Meta.debug true
def tst2 : MetaM Unit := do
print "----- tst2 -----";
ps ← getParamNames `Or.elim; print (toString ps);
ps ← getParamNames `Iff.elim; print (toString ps);
ps ← getParamNames `check; print (toString ps);
let ps ← getParamNames `Or.elim; print (toString ps);
let ps ← getParamNames `Iff.elim; print (toString ps);
let ps ← getParamNames `check; print (toString ps);
pure ()
#eval tst2
@ -45,17 +45,17 @@ axiom t1 : [Unit] = []
axiom t2 : 0 > 5
def tst3 : MetaM Unit := do
env ← getEnv;
t2 ← getConstInfo `t2;
c ← mkNoConfusion t2.type (mkConst `t1);
let env ← getEnv;
let t2 ← getConstInfo `t2;
let c ← mkNoConfusion t2.type (mkConst `t1);
print c;
Meta.check c;
cType ← inferType c;
let cType ← inferType c;
print cType;
lt ← mkLt (mkNatLit 10000000) (mkNatLit 20000000000);
ltPrf ← mkDecideProof lt;
let lt ← mkLt (mkNatLit 10000000) (mkNatLit 20000000000);
let ltPrf ← mkDecideProof lt;
Meta.check ltPrf;
t ← inferType ltPrf;
let t ← inferType ltPrf;
print t;
pure ()
@ -68,15 +68,15 @@ inductive Vec.{u} (α : Type u) : Nat → Type u
def tst4 : MetaM Unit :=
withLocalDeclD `x nat fun x =>
withLocalDeclD `y nat fun y => do
vType ← mkAppM `Vec #[nat, x];
let vType ← mkAppM `Vec #[nat, x];
withLocalDeclD `v vType fun v => do
m ← mkFreshExprSyntheticOpaqueMVar vType;
subgoals ← caseValues m.mvarId! x.fvarId! #[mkNatLit 2, mkNatLit 3, mkNatLit 5];
let m ← mkFreshExprSyntheticOpaqueMVar vType;
let subgoals ← caseValues m.mvarId! x.fvarId! #[mkNatLit 2, mkNatLit 3, mkNatLit 5];
subgoals.forM fun s => do {
print (MessageData.ofGoal s.mvarId);
assumption s.mvarId
};
t ← instantiateMVars m;
let t ← instantiateMVars m;
print t;
Meta.check t;
pure ()
@ -84,14 +84,14 @@ pure ()
#eval tst4
def tst5 : MetaM Unit := do
arrayNat ← mkAppM `Array #[nat];
let arrayNat ← mkAppM `Array #[nat];
withLocalDeclD `a arrayNat fun a => do
withLocalDeclD `b arrayNat fun b => do
let motiveType := _root_.mkArrow arrayNat (mkSort levelZero);
withLocalDeclD `motive motiveType fun motive => do
let mvarType := mkApp motive a;
mvar ← mkFreshExprSyntheticOpaqueMVar mvarType;
subgoals ← caseArraySizes mvar.mvarId! a.fvarId! #[1, 0, 4, 5];
let mvar ← mkFreshExprSyntheticOpaqueMVar mvarType;
let subgoals ← caseArraySizes mvar.mvarId! a.fvarId! #[1, 0, 4, 5];
subgoals.forM fun s => do {
print (MessageData.ofGoal s.mvarId);
pure ()

32
tests/lean/run/meta7.lean
View file

@ -26,15 +26,15 @@ let z := f 10;
def tst1 : MetaM Unit := do
print "----- tst1 -----";
c ← getConstInfo `ex;
let c ← getConstInfo `ex;
lambdaTelescope c.value?.get! fun xs body =>
withTrackingZeta do
Meta.check body;
ys ← getZetaFVarIds;
let ys ← getZetaFVarIds;
let ys := ys.toList.map mkFVar;
print ys;
check $ pure $ ys.length == 2;
c ← mkAuxDefinitionFor `foo body;
let c ← mkAuxDefinitionFor `foo body;
print c;
Meta.check c;
pure ()
@ -79,10 +79,10 @@ print "----- tst4 -----";
let nat := mkConst `Nat;
withLocalDeclD `x nat fun x =>
withLocalDeclD `y nat fun y => do
m ← mkFreshExprMVar nat;
let m ← mkFreshExprMVar nat;
print (← ppGoal m.mvarId!);
val ← mkAppM `HasAdd.add #[mkNatLit 10, y];
⟨zId, nId, subst⟩ ← assertAfter m.mvarId! x.fvarId! `z nat val;
let val ← mkAppM `HasAdd.add #[mkNatLit 10, y];
let ⟨zId, nId, subst⟩ ← assertAfter m.mvarId! x.fvarId! `z nat val;
print m;
print (← ppGoal nId);
withMVarContext nId do {
@ -91,7 +91,7 @@ withMVarContext nId do {
print (mkMVar nId)
};
print m;
expected ← mkAppM `HasAdd.add #[x, val];
let expected ← mkAppM `HasAdd.add #[x, val];
check (isDefEq m expected);
pure ()
@ -103,10 +103,10 @@ let prop := mkSort levelZero;
withLocalDeclD `p prop fun p =>
withLocalDeclD `q prop fun q => do
withLocalDeclD `h₁ p fun h₁ => do
eq ← mkEq p q;
let eq ← mkEq p q;
withLocalDeclD `h₂ eq fun h₂ => do
m ← mkFreshExprMVar q;
r ← replaceLocalDecl m.mvarId! h₁.fvarId! q h₂;
let m ← mkFreshExprMVar q;
let r ← replaceLocalDecl m.mvarId! h₁.fvarId! q h₂;
print (← ppGoal r.mvarId);
assignExprMVar r.mvarId (mkFVar r.fvarId);
print m;
@ -120,10 +120,10 @@ print "----- tst6 -----";
let nat := mkConst `Nat;
withLocalDeclD `x nat fun x =>
withLocalDeclD `y nat fun y => do
m ← mkFreshExprMVar nat;
let m ← mkFreshExprMVar nat;
print (← ppGoal m.mvarId!);
val ← mkAppM `HasAdd.add #[mkNatLit 10, y];
⟨zId, nId, subst⟩ ← assertAfter m.mvarId! y.fvarId! `z nat val;
let val ← mkAppM `HasAdd.add #[mkNatLit 10, y];
let ⟨zId, nId, subst⟩ ← assertAfter m.mvarId! y.fvarId! `z nat val;
print m;
print (← ppGoal nId);
withMVarContext nId do {
@ -132,7 +132,7 @@ withMVarContext nId do {
print (mkMVar nId)
};
print m;
expected ← mkAppM `HasAdd.add #[x, val];
let expected ← mkAppM `HasAdd.add #[x, val];
check (isDefEq m expected);
pure ()
@ -143,11 +143,11 @@ print "----- tst7 -----";
let nat := mkConst `Nat;
withLocalDeclD `x nat fun x =>
withLocalDeclD `y nat fun y => do
val ← mkAppM `HasAdd.add #[x, y];
let val ← mkAppM `HasAdd.add #[x, y];
print val;
let val := val.replaceFVars #[x, y] #[mkNatLit 0, mkNatLit 1];
print val;
expected ← mkAppM `HasAdd.add #[mkNatLit 0, mkNatLit 1];
let expected ← mkAppM `HasAdd.add #[mkNatLit 0, mkNatLit 1];
print expected;
check (pure $ val == expected);
pure ()

6
tests/lean/run/monadCache.lean
View file

@ -11,7 +11,7 @@ partial def depth : Expr → MonadCacheT Expr Nat CoreM Nat
checkCache e fun e =>
match e with
| Expr.const c [] _ => pure 1
| Expr.app f a _ => do d₁ ← depth f; d₂ ← depth a; pure $ Nat.max d₁ d₂ + 1
| Expr.app f a _ => do pure $ Nat.max (← depth f) (← depth a) + 1
| _ => pure 0
#eval (depth (mkTower 100)).run
@ -27,7 +27,7 @@ partial def visit : Expr → MonadCacheT Expr Expr CoreM Expr
#eval (visit (mkTower 4)).run
def tst : CoreM Nat := do
e ← (visit (mkTower 100)).run; (depth e).run
let e ← (visit (mkTower 100)).run; (depth e).run
#eval tst
@ -47,6 +47,6 @@ e.forEach fun e => match e with
| _ => pure ()
def tst2 : CoreM Unit := do
e ← (visit (mkTower 100)).run; displayConsts e
let e ← (visit (mkTower 100)).run; displayConsts e
#eval tst2

8
tests/lean/run/monadControl.lean
View file

@ -3,7 +3,7 @@ new_frontend
@[inline] def f {α} (s : String) (x : IO α) : IO α := do
IO.println "started";
IO.println s;
a ← x;
let a ← x;
IO.println ("ended");
pure a
@ -13,7 +13,7 @@ controlAt IO fun runInBase => f msg (runInBase x)
abbrev M := StateT Bool $ ExceptT String $ StateT String $ ReaderT Nat $ StateT Nat IO
def tst : M Nat := do
a ← f'' "hello" do { s ← getThe Nat; ctx ← read; modifyThe Nat fun s => s + ctx; when (s > 10) $ throw "ERROR"; getThe Nat };
let a ← f'' "hello" do { let s ← getThe Nat; let ctx ← read; modifyThe Nat fun s => s + ctx; when (s > 10) $ throw "ERROR"; getThe Nat };
modifyThe Nat Nat.succ;
pure a
@ -22,7 +22,7 @@ pure a
@[inline] def g {α} (s : String) (x : Nat → IO α) : IO α := do
IO.println "started";
IO.println s;
a ← x s.length;
let a ← x s.length;
IO.println ("ended");
pure a
@ -30,7 +30,7 @@ pure a
controlAt IO fun runInBase => g msg (fun n => runInBase (x n))
def tst2 : M Nat := do
a ← g' "hello" fun x => do { s ← getThe Nat; ctx ← read; modifyThe Nat fun s => s + ctx + x; when (s > 10) $ throw "ERROR"; getThe Nat };
let a ← g' "hello" fun x => do { let s ← getThe Nat; let ctx ← read; modifyThe Nat fun s => s + ctx + x; when (s > 10) $ throw "ERROR"; getThe Nat };
modifyThe Nat Nat.succ;
pure a

4
tests/lean/run/nicerNestedDos.lean
View file

@ -12,7 +12,7 @@ pure (x + 1)
def g (x : Nat) : StateT Nat Id Unit := do
when (x > 10) do
s ← get;
let s ← get;
set (s + x);
pure ()
@ -24,7 +24,7 @@ rfl
def h (x : Nat) : StateT Nat Id Unit := do
when (x > 10) do {
s ← get;
let s ← get;
set (s + x) -- we don't need to respect indentation when `{` `}` are used
};
pure ()

4
tests/lean/run/parseCore.lean
View file

@ -4,8 +4,8 @@ def test : IO Unit :=
if System.Platform.isWindows then
pure () -- TODO investigate why the following doesn't work on Windows
else do
env ← Lean.mkEmptyEnvironment;
_ ← Lean.Parser.parseFile env (System.mkFilePath ["..", "..", "..", "src", "Init", "Core.lean"]);
let env ← Lean.mkEmptyEnvironment;
Lean.Parser.parseFile env (System.mkFilePath ["..", "..", "..", "src", "Init", "Core.lean"]);
IO.println "done"
#eval test

6
tests/lean/run/quasi_pattern_unification_approx_issue.lean
View file

@ -8,6 +8,6 @@ getThe σ
def foo1 : StateT δ (StateT σ Id) σ :=
monadLift (get : StateT σ Id σ)
def foo2 : StateT δ (StateT σ Id) σ :=
do s : σ ← monadLift (get : StateT σ Id σ);
pure s
def foo2 : StateT δ (StateT σ Id) σ := do
let s : σ ← monadLift (get : StateT σ Id σ);
pure s

6
tests/lean/run/readerThe.lean
View file

@ -4,11 +4,11 @@ abbrev M := ReaderT String $ StateT Nat $ ReaderT Bool $ IO
def f : M Nat := do
s ← read;
let s ← read;
IO.println s;
b ← readThe Bool;
let b ← readThe Bool;
IO.println b;
s ← get;
let s ← get;
pure s
#eval (f "hello").run' 10 true

2
tests/lean/run/recInfo1.lean
View file

@ -7,7 +7,7 @@ def print (msg : MessageData) : MetaM Unit :=
trace! `Meta.debug msg
def showRecInfo (declName : Name) (majorPos? : Option Nat := none) : MetaM Unit := do
info ← mkRecursorInfo declName majorPos?;
let info ← mkRecursorInfo declName majorPos?;
print (toString info)
set_option trace.Meta true

42
tests/lean/run/sharecommon.lean
View file

@ -8,11 +8,11 @@ unsafe def tst1 : ShareCommonT IO Unit := do
let x := [1];
let y := [0].map (fun x => x + 1);
check $ ptrAddrUnsafe x != ptrAddrUnsafe y;
x ← shareCommonM x;
y ← shareCommonM y;
let x ← shareCommonM x;
let y ← shareCommonM y;
check $ ptrAddrUnsafe x == ptrAddrUnsafe y;
z ← shareCommonM [2];
x ← shareCommonM x;
let z ← shareCommonM [2];
let x ← shareCommonM x;
check $ ptrAddrUnsafe x == ptrAddrUnsafe y;
check $ ptrAddrUnsafe x != ptrAddrUnsafe z;
IO.println x;
@ -25,11 +25,11 @@ unsafe def tst2 : ShareCommonT IO Unit := do
let x := [1, 2];
let y := [0, 1].map (fun x => x + 1);
check $ ptrAddrUnsafe x != ptrAddrUnsafe y;
x ← shareCommonM x;
y ← shareCommonM y;
let x ← shareCommonM x;
let y ← shareCommonM y;
check $ ptrAddrUnsafe x == ptrAddrUnsafe y;
z ← shareCommonM [2];
x ← shareCommonM x;
let z ← shareCommonM [2];
let x ← shareCommonM x;
check $ ptrAddrUnsafe x == ptrAddrUnsafe y;
check $ ptrAddrUnsafe x != ptrAddrUnsafe z;
IO.println x;
@ -52,9 +52,9 @@ let o2 := mkFoo2 10 true;
let o3 := mkFoo2 10 false;
check $ ptrAddrUnsafe o1 != ptrAddrUnsafe o2;
check $ ptrAddrUnsafe o1 != ptrAddrUnsafe o3;
o1 ← shareCommonM o1;
o2 ← shareCommonM o2;
o3 ← shareCommonM o3;
let o1 ← shareCommonM o1;
let o2 ← shareCommonM o2;
let o3 ← shareCommonM o3;
check $
o1.x == 10 && o1.y == true &&
o1.z == true && o3.z == false &&
@ -69,11 +69,11 @@ unsafe def tst4 : ShareCommonT IO Unit := do
let x := ["hello"];
let y := ["ello"].map (fun x => "h" ++ x);
check $ ptrAddrUnsafe x != ptrAddrUnsafe y;
x ← shareCommonM x;
y ← shareCommonM y;
let x ← shareCommonM x;
let y ← shareCommonM y;
check $ ptrAddrUnsafe x == ptrAddrUnsafe y;
z ← shareCommonM ["world"];
x ← shareCommonM x;
let z ← shareCommonM ["world"];
let x ← shareCommonM x;
check $
ptrAddrUnsafe x == ptrAddrUnsafe y &&
ptrAddrUnsafe x != ptrAddrUnsafe z;
@ -104,9 +104,9 @@ check $
ptrAddrUnsafe (a.get! 0) != ptrAddrUnsafe (a.get! 2) &&
ptrAddrUnsafe (b.get! 0) != ptrAddrUnsafe (b.get! 1) &&
ptrAddrUnsafe (c.get! 0) != ptrAddrUnsafe (c.get! 1);
a ← shareCommonM a;
b ← shareCommonM b;
c ← shareCommonM c;
let a ← shareCommonM a;
let b ← shareCommonM b;
let c ← shareCommonM c;
check $
ptrAddrUnsafe a == ptrAddrUnsafe b &&
ptrAddrUnsafe a != ptrAddrUnsafe c &&
@ -137,9 +137,9 @@ IO.println b;
IO.println c;
check $ ptrAddrUnsafe a != ptrAddrUnsafe b;
check $ ptrAddrUnsafe a != ptrAddrUnsafe c;
a ← shareCommonM a;
b ← shareCommonM b;
c ← shareCommonM c;
let a ← shareCommonM a;
let b ← shareCommonM b;
let c ← shareCommonM c;
check $ ptrAddrUnsafe a == ptrAddrUnsafe b;
check $ ptrAddrUnsafe a != ptrAddrUnsafe c;
pure ()

2
tests/lean/run/spec_issue.lean
View file

@ -3,5 +3,5 @@ set_option trace.compiler.ir.result true
def g (ys : List Nat) : IO Nat := do
let x := 0;
(_, x) ← StateT.run (ys.forM fun y => IO.println y) x;
let (_, x) ← StateT.run (ys.forM fun y => IO.println y) x;
pure x

18
tests/lean/run/stateRef.lean
View file

@ -13,7 +13,7 @@ def g : IO Nat :=
#eval (do set 100; f 5 : StateRefT Nat IO Nat).run' 0
def f2 : ReaderT Nat (StateRefT Nat IO) Nat := do
v ← read;
let v ← read;
IO.println $ "context " ++ toString v;
modify fun s => s + v;
get
@ -21,10 +21,10 @@ get
#eval (f2.run 10).run' 20
def f3 : StateT String (StateRefT Nat IO) Nat := do
s ← get;
n ← getThe Nat;
let s ← get;
let n ← getThe Nat;
set (s ++ ", " ++ toString n);
s ← get;
let s ← get;
IO.println s;
set (n+1);
getThe Nat
@ -38,16 +38,16 @@ class HasGetAt {β : Type} (v : β) (α : outParam Type) (m : Type → Type) :=
(getAt : m α)
instance monadState.hasGetAt (β : Type) (v : β) (α : Type) (m : Type → Type) [Monad m] [MonadStateOf (Label v α) m] : HasGetAt v α m :=
{ getAt := do a ← getThe (Label v α); pure a.val }
{ getAt := do let a ← getThe (Label v α); pure a.val }
export HasGetAt (getAt)
abbrev M := StateRefT (Label 0 Nat) $ StateRefT (Label 1 Nat) $ StateRefT (Label 2 Nat) IO
def f4 : M Nat := do
a0 : Nat ← getAt 0;
a1 ← getAt 1;
a2 ← getAt 2;
let a0 : Nat ← getAt 0;
let a1 ← getAt 1;
let a2 ← getAt 2;
IO.println $ "state0 " ++ toString a0;
IO.println $ "state1 " ++ toString a1;
IO.println $ "state1 " ++ toString a2;
@ -58,7 +58,7 @@ pure (a0 + a1 + a2)
abbrev S (ω : Type) := StateRefT Nat $ StateRefT String $ ST ω
def f5 {ω} : S ω Unit := do
s ← getThe String;
let s ← getThe String;
modify fun n => n + s.length;
pure ()

4
tests/lean/run/strInterpolation.lean
View file

@ -87,7 +87,7 @@ let rec loop (i : String.Pos) (acc : String) :=
else if s.atEnd i then
none
else if c == '\\' then do
(c, i) ← decodeStrInterpolantQuotedChar s i;
let (c, i) ← decodeStrInterpolantQuotedChar s i;
loop i (acc.push c)
else
loop i (acc.push c);
@ -100,7 +100,7 @@ match isLit? Parser.strInterpolantStrLitKind stx with
def expandStrInterpolantChunks (chunks : Array Syntax) (mkAppend : Syntax → Syntax → MacroM Syntax) (mkElem : Syntax → MacroM Syntax) : MacroM Syntax :=
chunks.iterateM Syntax.missing fun i elem result => do
elem ← match elem.isStrInterpolantStrLit? with
let elem ← match elem.isStrInterpolantStrLit? with
| none => mkElem elem
| some str => mkElem (mkStxStrLit str);
-- TODO: remove `(` after we write new elabDo

4
tests/lean/run/structInst2.lean
View file

@ -11,7 +11,7 @@ variables {m : Type u → Type v} [Monad m] {α β : Type u}
@[inline] protected def bind (ma : OptionT2 m α) (f : α → OptionT2 m β) : OptionT2 m β :=
(do {
a? ← ma;
let a? ← ma;
match a? with
| some a => f a
| none => pure none
@ -21,7 +21,7 @@ variables {m : Type u → Type v} [Monad m] {α β : Type u}
(HasPure.pure (some a) : m (Option α))
@[inline] protected def orelse (ma : OptionT2 m α) (mb : OptionT2 m α) : OptionT2 m α :=
(do { a? ← ma;
(do { let a? ← ma;
match a? with
| some a => pure (some a)
| _ => mb } : m (Option α))

2
tests/lean/run/structure.lean
View file

@ -24,7 +24,7 @@ inductive D
| mk (x y z : Nat) : D
def tst : CoreM Unit :=
do env ← getEnv;
do let env ← getEnv;
IO.println (getStructureFields env `Lean.Environment);
check $ getStructureFields env `S4 == #[`toS2, `toS3, `s];
check $ getStructureFields env `S1 == #[`x, `y];

2
tests/lean/run/stxMacro.lean
View file

@ -7,7 +7,7 @@ syntax "sum! " (many term:max) : term
macro_rules
| `(sum! $x*) => do
r ← `(0);
let r ← `(0);
x.foldlM (fun r elem => `($r + $elem)) r
#check sum! 1 2 3

36
tests/lean/run/synth1.lean
View file

@ -28,34 +28,34 @@ def print {α} [HasToString α] (a : α) : MetaM Unit :=
trace! `Meta.synthInstance (toString a)
def tst1 : MetaM Unit :=
do inst ← mkAppM `HasCoerce #[mkConst `Nat, mkSort levelZero];
r ← synthInstance inst;
print r
def tst1 : MetaM Unit := do
let inst ← mkAppM `HasCoerce #[mkConst `Nat, mkSort levelZero];
let r ← synthInstance inst;
print r
set_option trace.Meta.synthInstance true in
set_option trace.Meta.synthInstance.tryResolve false in
#eval tst1
def tst2 : MetaM Unit :=
do inst ← mkAppM `HasBind #[mkConst `IO];
-- globalInstances ← getGlobalInstances;
-- print (format globalInstances);
-- result ← globalInstances.getUnify inst;
-- print result;
r ← synthInstance inst;
print r;
pure ()
def tst2 : MetaM Unit := do
let inst ← mkAppM `HasBind #[mkConst `IO];
-- globalInstances ← getGlobalInstances;
-- print (format globalInstances);
-- result ← globalInstances.getUnify inst;
-- print result;
let r ← synthInstance inst;
print r;
pure ()
set_option trace.Meta.synthInstance true in
set_option trace.Meta.synthInstance.tryResolve false in
#eval tst2
def tst3 : MetaM Unit :=
do inst ← mkAppM `HasBeq #[mkConst `Nat];
r ← synthInstance inst;
print r;
pure ()
def tst3 : MetaM Unit := do
let inst ← mkAppM `HasBeq #[mkConst `Nat];
let r ← synthInstance inst;
print r;
pure ()
set_option trace.Meta.synthInstance true in
set_option trace.Meta.synthInstance.tryResolve false in

16
tests/lean/run/tactic.lean
View file

@ -9,14 +9,14 @@ axiom simple : forall {p q : Prop}, p → q → p
def print (msg : MessageData) : MetaM Unit :=
trace! `Meta.Tactic msg
def tst1 : MetaM Unit :=
do cinfo ← getConstInfo `simple;
mvar ← mkFreshExprSyntheticOpaqueMVar cinfo.type;
let mvarId := mvar.mvarId!;
(_, mvarId) ← introN mvarId 4;
assumption mvarId;
result ← instantiateMVars mvar;
print result
def tst1 : MetaM Unit := do
let cinfo ← getConstInfo `simple;
let mvar ← mkFreshExprSyntheticOpaqueMVar cinfo.type;
let mvarId := mvar.mvarId!;
let (_, mvarId) ← introN mvarId 4;
assumption mvarId;
let result ← instantiateMVars mvar;
print result
set_option trace.Meta.Tactic true

12
tests/lean/run/termElab.lean
View file

@ -6,21 +6,21 @@ open Lean.Elab
open Lean.Elab.Term
def tst1 : TermElabM Unit := do
opt ← getOptions;
stx ← `(forall (a b : Nat), Nat);
let opt ← getOptions;
let stx ← `(forall (a b : Nat), Nat);
IO.println "message 1"; -- This message goes direct to stdio. It will be displayed before trace messages.
e ← elabTermAndSynthesize stx none;
let e ← elabTermAndSynthesize stx none;
logDbgTrace (">>> " ++ e); -- display message when `trace.Elab.debug` is true
IO.println "message 2"
#eval tst1
def tst2 : TermElabM Unit := do
opt ← getOptions;
let opt ← getOptions;
let a := mkIdent `a;
let b := mkIdent `b;
stx ← `((fun ($a : Type) (x : $a) => @id $a x) _ 1);
e ← elabTermAndSynthesize stx none;
let stx ← `((fun ($a : Type) (x : $a) => @id $a x) _ 1);
let e ← elabTermAndSynthesize stx none;
logDbgTrace (">>> " ++ e);
throwErrorIfErrors

16
tests/lean/run/termParserAttr.lean
View file

@ -3,14 +3,14 @@ new_frontend
open Lean
open Lean.Elab
def run (input : String) (failIff : Bool := true) : CoreM Unit :=
do env ← getEnv;
opts ← getOptions;
(env, messages) ← liftIO $ process input env opts;
messages.toList.forM $ fun msg => liftIO (msg.toString >>= IO.println);
when (failIff && messages.hasErrors) $ throwError "errors have been found";
when (!failIff && !messages.hasErrors) $ throwError "there are no errors";
pure ()
def run (input : String) (failIff : Bool := true) : CoreM Unit := do
let env ← getEnv;
let opts ← getOptions;
let (env, messages) ← liftIO $ process input env opts;
messages.toList.forM $ fun msg => liftIO (msg.toString >>= IO.println);
when (failIff && messages.hasErrors) $ throwError "errors have been found";
when (!failIff && !messages.hasErrors) $ throwError "there are no errors";
pure ()
open Lean.Parser

14
tests/lean/run/termparsertest1.lean
View file

@ -5,8 +5,8 @@ open Lean.Parser
def testParser (input : String) : IO Unit :=
do
env ← mkEmptyEnvironment;
stx ← IO.ofExcept $ runParserCategory env `term input "<input>";
let env ← mkEmptyEnvironment;
let stx ← IO.ofExcept $ runParserCategory env `term input "<input>";
IO.println stx
def test (is : List String) : IO Unit :=
@ -16,7 +16,7 @@ is.forM $ fun input => do
def testParserFailure (input : String) : IO Unit :=
do
env ← mkEmptyEnvironment;
let env ← mkEmptyEnvironment;
match runParserCategory env `term input "<input>" with
| Except.ok stx => throw (IO.userError ("unexpected success\n" ++ toString stx))
| Except.error msg => IO.println ("failed as expected, error: " ++ msg)
@ -107,14 +107,14 @@ match x with
"¬ a ∧ b",
"
do
x ← f a;
x : Nat ← f a;
let x ← f a;
let x : Nat ← f a;
g x;
let y := g x;
(a, b) <- h x y;
let (a, b) <- h x y;
let (a, b) := (b, a);
pure (a + b)",
"do { x ← f a; pure $ a + a }",
"do { let x ← f a; pure $ a + a }",
"let f : Nat → Nat → Nat
| 0, a => a + 10
| n+1, b => n * b;

2
tests/lean/run/toExpr.lean
View file

@ -3,7 +3,7 @@ new_frontend
open Lean
unsafe def test {α : Type} [HasToString α] [ToExpr α] [HasBeq α] (a : α) : CoreM Unit := do
env ← getEnv;
let env ← getEnv;
let auxName := `_toExpr._test;
let decl := Declaration.defnDecl {
name := auxName,

2
tests/lean/run/typeclass_loop.lean
View file

@ -1,5 +1,5 @@
new_frontend
example (M : Type → Type) [Monad M] : ExceptT Unit (ReaderT Unit (StateT Unit M)) Unit := do
ctx ← read;
let ctx ← read;
pure ()

6
tests/lean/run/unexpected_result_with_bind.lean
View file

@ -13,10 +13,10 @@ instance : Monad FooM := {}
def unexpectedBehavior : FooM String := do
let b : Bool := (#[] : Array Nat).isEmpty;
trueBranch ← pure "trueBranch";
falseBranch ← pure "falseBranch";
let trueBranch ← pure "trueBranch";
let falseBranch ← pure "falseBranch";
(1 : Nat).foldM (λ _ (s : String) => do
s ← pure $ if b then trueBranch else falseBranch; pure s) ""
let s ← pure $ if b then trueBranch else falseBranch; pure s) ""
#eval unexpectedBehavior ()

4
tests/lean/run/unif_issue.lean
View file

@ -4,7 +4,7 @@ open Lean
#eval toString $
Unhygienic.run do
a ← `(Nat.one);
let a ← `(Nat.one);
let rhs_0 : _ := fun (a : Lean.Syntax) (b : Lean.Syntax) => pure Syntax.missing;
let rhs_1 : _ := fun (_a : _) => pure Lean.Syntax.missing;
let discr_2 : _ := a;
@ -23,7 +23,7 @@ open Lean
#check toString $
Unhygienic.run do
a ← `(Nat.one);
let a ← `(Nat.one);
let rhs_0 : _ := fun (a : Lean.Syntax) (b : Lean.Syntax) => pure Syntax.missing;
let rhs_1 : _ := fun (_a : _) => pure Lean.Syntax.missing;
let discr_2 : _ := a;

6
tests/lean/stdio.lean
View file

@ -2,18 +2,18 @@ new_frontend
open IO.FS
def usingIO {α} (x : IO α) := x
#eval usingIO do
out ← IO.getStdout;
let out ← IO.getStdout;
(out.putStrLn "print stdout" : IO Unit)
#eval usingIO do
err ← IO.getStderr;
let err ← IO.getStderr;
(err.putStr "print stderr" : IO Unit)
open usingIO IO
def test : IO Unit := do
FS.withFile "stdout1.txt" IO.FS.Mode.write $ fun h₁ => do
{ h₂ ← FS.Handle.mk "stdout2.txt" IO.FS.Mode.write;
{ let h₂ ← FS.Handle.mk "stdout2.txt" IO.FS.Mode.write;
withStdout (Stream.ofHandle h₁) $ do
println "line 1";
catch