diff --git a/stage0/src/Init/Lean/Elab/Binders.lean b/stage0/src/Init/Lean/Elab/Binders.lean index f671e5e86c..219a605723 100644 --- a/stage0/src/Init/Lean/Elab/Binders.lean +++ b/stage0/src/Init/Lean/Elab/Binders.lean @@ -163,7 +163,7 @@ else do x fvars @[inline] def elabBinder {α} (binder : Syntax) (x : Expr → TermElabM α) : TermElabM α := -elabBinders #[binder] (fun fvars => x (fvars.get! 1)) +elabBinders #[binder] (fun fvars => x (fvars.get! 0)) @[builtinTermElab «forall»] def elabForall : TermElab := fun stx _ => match_syntax stx with diff --git a/stage0/src/Init/Lean/Elab/SyntheticMVars.lean b/stage0/src/Init/Lean/Elab/SyntheticMVars.lean index c07fafab77..688baf4901 100644 --- a/stage0/src/Init/Lean/Elab/SyntheticMVars.lean +++ b/stage0/src/Init/Lean/Elab/SyntheticMVars.lean @@ -22,7 +22,7 @@ withMVarContext mvarId $ fun ctx s => def ensureAssignmentHasNoMVars (ref : Syntax) (mvarId : MVarId) : TermElabM Unit := do val ← instantiateMVars ref (mkMVar mvarId); -when val.hasMVar $ throwError ref ("tactic failed, result still contain metavariables" ++ indentExpr val) +when val.hasExprMVar $ throwError ref ("tactic failed, result still contain metavariables" ++ indentExpr val) def runTactic (ref : Syntax) (mvarId : MVarId) (tacticCode : Syntax) : TermElabM Unit := do modify $ fun s => { mctx := s.mctx.instantiateMVarDeclMVars mvarId, .. s }; diff --git a/stage0/src/Init/Lean/Elab/Tactic.lean b/stage0/src/Init/Lean/Elab/Tactic.lean index 0261d106b1..6cbb6b016e 100644 --- a/stage0/src/Init/Lean/Elab/Tactic.lean +++ b/stage0/src/Init/Lean/Elab/Tactic.lean @@ -9,3 +9,4 @@ import Init.Lean.Elab.Tactic.Basic import Init.Lean.Elab.Tactic.ElabTerm import Init.Lean.Elab.Tactic.Induction import Init.Lean.Elab.Tactic.Generalize +import Init.Lean.Elab.Tactic.Injection diff --git a/stage0/src/Init/Lean/Elab/Tactic/ElabTerm.lean b/stage0/src/Init/Lean/Elab/Tactic/ElabTerm.lean index 9f9856db08..d6bf27ac27 100644 --- a/stage0/src/Init/Lean/Elab/Tactic/ElabTerm.lean +++ b/stage0/src/Init/Lean/Elab/Tactic/ElabTerm.lean @@ -5,6 +5,7 @@ Authors: Leonardo de Moura -/ prelude import Init.Lean.Meta.Tactic.Apply +import Init.Lean.Meta.Tactic.Assert import Init.Lean.Elab.Tactic.Basic import Init.Lean.Elab.SyntheticMVars @@ -68,6 +69,29 @@ fun stx => match_syntax stx with setGoals (gs' ++ gs) | _ => throwUnsupportedSyntax +/-- + Elaborate `stx`. If it a free variable, return it. Otherwise, assert it, and return the free variable. + Note that, the main goal is updated when `Meta.assert` is used in the second case. -/ +def elabAsFVar (stx : Syntax) (userName? : Option Name := none) : TacticM FVarId := do +(mvarId, others) ← getMainGoal stx; +withMVarContext mvarId $ do + e ← elabTerm stx none; + match e with + | Expr.fvar fvarId _ => pure fvarId + | _ => do + type ← inferType stx e; + let intro (userName : Name) (useUnusedNames : Bool) : TacticM FVarId := do { + (fvarId, mvarId) ← liftMetaM stx $ do { + mvarId ← Meta.assert mvarId userName type e; + Meta.intro1 mvarId useUnusedNames + }; + setGoals $ mvarId::others; + pure fvarId + }; + match userName? with + | none => intro `h true + | some userName => intro userName false + end Tactic end Elab end Lean diff --git a/stage0/src/Init/Lean/Elab/Tactic/Injection.lean b/stage0/src/Init/Lean/Elab/Tactic/Injection.lean new file mode 100644 index 0000000000..0ce5dc6419 --- /dev/null +++ b/stage0/src/Init/Lean/Elab/Tactic/Injection.lean @@ -0,0 +1,32 @@ +/- +Copyright (c) 2020 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Leonardo de Moura +-/ +prelude +import Init.Lean.Meta.Tactic.Injection +import Init.Lean.Elab.Tactic.ElabTerm + +namespace Lean +namespace Elab +namespace Tactic + +-- optional (" with " >> many1 ident') +private def getInjectionNewIds (stx : Syntax) : List Name := +if stx.isNone then [] +else (stx.getArg 1).getArgs.toList.map Syntax.getId + +@[builtinTactic «injection»] def evalInjection : Tactic := +fun stx => do + -- parser! nonReservedSymbol "injection " >> termParser >> withIds + fvarId ← elabAsFVar (stx.getArg 1); + let ids := getInjectionNewIds (stx.getArg 2); + liftMetaTactic stx $ fun mvarId => do + r ← Meta.injection mvarId fvarId ids (!ids.isEmpty); + match r with + | Meta.InjectionResult.solved => pure [] + | Meta.InjectionResult.subgoal mvarId _ _ => pure [mvarId] + +end Tactic +end Elab +end Lean diff --git a/stage0/src/Init/Lean/Meta/Tactic/Injection.lean b/stage0/src/Init/Lean/Meta/Tactic/Injection.lean index 8872bbfbb9..a76db94c8f 100644 --- a/stage0/src/Init/Lean/Meta/Tactic/Injection.lean +++ b/stage0/src/Init/Lean/Meta/Tactic/Injection.lean @@ -54,7 +54,7 @@ withMVarContext mvarId $ do newMVar ← mkFreshExprSyntheticOpaqueMVar newTarget tag; assignExprMVar mvarId (mkApp val newMVar); mvarId ← tryClear newMVar.mvarId! fvarId; - pure $ InjectionResultCore.subgoal newMVar.mvarId! aCtor.nfields + pure $ InjectionResultCore.subgoal mvarId aCtor.nfields | _ => throwTacticEx `injection mvarId "ill-formed noConfusion auxiliary construction" | _, _ => throwTacticEx `injection mvarId "equality of constructor applications expected" diff --git a/stage0/src/Init/Lean/Parser/Term.lean b/stage0/src/Init/Lean/Parser/Term.lean index 5a5e495433..1c2cf0f467 100644 --- a/stage0/src/Init/Lean/Parser/Term.lean +++ b/stage0/src/Init/Lean/Parser/Term.lean @@ -124,6 +124,7 @@ def letPatDecl : Parser := node `Lean.Parser.Term.letDecl $ try (termParser >> def letEqnsDecl : Parser := node `Lean.Parser.Term.letDecl $ letIdLhs >> matchAlts false def letDecl := letIdDecl <|> letPatDecl <|> letEqnsDecl @[builtinTermParser] def «let» := parser! symbol "let " leadPrec >> letDecl >> "; " >> termParser +@[builtinTermParser] def «let!» := parser! symbol "let! " leadPrec >> letDecl >> "; " >> termParser def leftArrow : Parser := unicodeSymbol " ← " " <- " def doLet := parser! "let " >> letDecl diff --git a/stage0/stdlib/CMakeLists.txt b/stage0/stdlib/CMakeLists.txt index 6740397f6c..87e6cd375a 100644 --- a/stage0/stdlib/CMakeLists.txt +++ b/stage0/stdlib/CMakeLists.txt @@ -1 +1 @@ -add_library (stage0 OBJECT Init/./Coe.c Init/./Control.c Init/./Control/Alternative.c Init/./Control/Applicative.c Init/./Control/Conditional.c Init/./Control/EState.c Init/./Control/Except.c Init/./Control/Functor.c Init/./Control/Id.c Init/./Control/Lift.c Init/./Control/Monad.c Init/./Control/Option.c Init/./Control/Reader.c Init/./Control/State.c Init/./Core.c Init/./Data.c Init/./Data/Array.c Init/./Data/Array/Basic.c Init/./Data/Array/BinSearch.c Init/./Data/Array/QSort.c Init/./Data/AssocList.c Init/./Data/Basic.c Init/./Data/BinomialHeap.c Init/./Data/BinomialHeap/Basic.c Init/./Data/ByteArray.c Init/./Data/ByteArray/Basic.c Init/./Data/Char.c Init/./Data/Char/Basic.c Init/./Data/DList.c Init/./Data/Fin.c Init/./Data/Fin/Basic.c Init/./Data/HashMap.c Init/./Data/HashMap/Basic.c Init/./Data/HashSet.c Init/./Data/Hashable.c Init/./Data/Int.c Init/./Data/Int/Basic.c Init/./Data/List.c Init/./Data/List/Basic.c Init/./Data/List/BasicAux.c Init/./Data/List/Control.c Init/./Data/List/Instances.c Init/./Data/Nat.c Init/./Data/Nat/Basic.c Init/./Data/Nat/Bitwise.c Init/./Data/Nat/Control.c Init/./Data/Nat/Div.c Init/./Data/Option.c Init/./Data/Option/Basic.c Init/./Data/Option/BasicAux.c Init/./Data/Option/Instances.c Init/./Data/PersistentArray.c Init/./Data/PersistentArray/Basic.c Init/./Data/PersistentHashMap.c Init/./Data/PersistentHashMap/Basic.c Init/./Data/PersistentHashSet.c Init/./Data/Queue.c Init/./Data/Queue/Basic.c Init/./Data/RBMap.c Init/./Data/RBMap/Basic.c Init/./Data/RBMap/BasicAux.c Init/./Data/RBTree.c Init/./Data/RBTree/Basic.c Init/./Data/Random.c Init/./Data/Repr.c Init/./Data/Stack.c Init/./Data/Stack/Basic.c Init/./Data/String.c Init/./Data/String/Basic.c Init/./Data/ToString.c Init/./Data/UInt.c Init/./Default.c Init/./Fix.c Init/./HasCoe.c Init/./Lean.c Init/./Lean/Attributes.c Init/./Lean/AuxRecursor.c Init/./Lean/Class.c Init/./Lean/Compiler.c Init/./Lean/Compiler/ClosedTermCache.c Init/./Lean/Compiler/ConstFolding.c Init/./Lean/Compiler/ExportAttr.c Init/./Lean/Compiler/ExternAttr.c Init/./Lean/Compiler/IR.c Init/./Lean/Compiler/IR/Basic.c Init/./Lean/Compiler/IR/Borrow.c Init/./Lean/Compiler/IR/Boxing.c Init/./Lean/Compiler/IR/Checker.c Init/./Lean/Compiler/IR/CompilerM.c Init/./Lean/Compiler/IR/CtorLayout.c Init/./Lean/Compiler/IR/ElimDeadBranches.c Init/./Lean/Compiler/IR/ElimDeadVars.c Init/./Lean/Compiler/IR/EmitC.c Init/./Lean/Compiler/IR/EmitUtil.c Init/./Lean/Compiler/IR/ExpandResetReuse.c Init/./Lean/Compiler/IR/Format.c Init/./Lean/Compiler/IR/FreeVars.c Init/./Lean/Compiler/IR/LiveVars.c Init/./Lean/Compiler/IR/NormIds.c Init/./Lean/Compiler/IR/PushProj.c Init/./Lean/Compiler/IR/RC.c Init/./Lean/Compiler/IR/ResetReuse.c Init/./Lean/Compiler/IR/SimpCase.c Init/./Lean/Compiler/IR/UnboxResult.c Init/./Lean/Compiler/ImplementedByAttr.c Init/./Lean/Compiler/InitAttr.c Init/./Lean/Compiler/InlineAttrs.c Init/./Lean/Compiler/NameMangling.c Init/./Lean/Compiler/NeverExtractAttr.c Init/./Lean/Compiler/Specialize.c Init/./Lean/Compiler/Util.c Init/./Lean/Data/Format.c Init/./Lean/Data/KVMap.c Init/./Lean/Data/LBool.c Init/./Lean/Data/LOption.c Init/./Lean/Data/Name.c Init/./Lean/Data/Occurrences.c Init/./Lean/Data/Options.c Init/./Lean/Data/Position.c Init/./Lean/Data/SMap.c Init/./Lean/Data/Trie.c Init/./Lean/Declaration.c Init/./Lean/Elab.c Init/./Lean/Elab/Alias.c Init/./Lean/Elab/App.c Init/./Lean/Elab/Binders.c Init/./Lean/Elab/BuiltinNotation.c Init/./Lean/Elab/Command.c Init/./Lean/Elab/DeclModifiers.c Init/./Lean/Elab/Declaration.c Init/./Lean/Elab/Definition.c Init/./Lean/Elab/DoNotation.c Init/./Lean/Elab/Exception.c Init/./Lean/Elab/Frontend.c Init/./Lean/Elab/Import.c Init/./Lean/Elab/Level.c Init/./Lean/Elab/Log.c Init/./Lean/Elab/Match.c Init/./Lean/Elab/Quotation.c Init/./Lean/Elab/ResolveName.c Init/./Lean/Elab/StrategyAttrs.c Init/./Lean/Elab/StructInst.c Init/./Lean/Elab/Syntax.c Init/./Lean/Elab/SyntheticMVars.c Init/./Lean/Elab/Tactic.c Init/./Lean/Elab/Tactic/Basic.c Init/./Lean/Elab/Tactic/ElabTerm.c Init/./Lean/Elab/Tactic/Generalize.c Init/./Lean/Elab/Tactic/Induction.c Init/./Lean/Elab/Term.c Init/./Lean/Elab/Util.c Init/./Lean/Environment.c Init/./Lean/EqnCompiler.c Init/./Lean/EqnCompiler/MatchPattern.c Init/./Lean/Eval.c Init/./Lean/Expr.c Init/./Lean/HeadIndex.c Init/./Lean/Hygiene.c Init/./Lean/Level.c Init/./Lean/Linter.c Init/./Lean/LocalContext.c Init/./Lean/Message.c Init/./Lean/Meta.c Init/./Lean/Meta/AbstractMVars.c Init/./Lean/Meta/AppBuilder.c Init/./Lean/Meta/Basic.c Init/./Lean/Meta/Check.c Init/./Lean/Meta/DiscrTree.c Init/./Lean/Meta/DiscrTreeTypes.c Init/./Lean/Meta/Exception.c Init/./Lean/Meta/ExprDefEq.c Init/./Lean/Meta/FunInfo.c Init/./Lean/Meta/InferType.c Init/./Lean/Meta/Instances.c Init/./Lean/Meta/KAbstract.c Init/./Lean/Meta/LevelDefEq.c Init/./Lean/Meta/Message.c Init/./Lean/Meta/Offset.c Init/./Lean/Meta/RecursorInfo.c Init/./Lean/Meta/Reduce.c Init/./Lean/Meta/SynthInstance.c Init/./Lean/Meta/Tactic.c Init/./Lean/Meta/Tactic/Apply.c Init/./Lean/Meta/Tactic/Assert.c Init/./Lean/Meta/Tactic/Assumption.c Init/./Lean/Meta/Tactic/Cases.c Init/./Lean/Meta/Tactic/Clear.c Init/./Lean/Meta/Tactic/FVarSubst.c Init/./Lean/Meta/Tactic/Generalize.c Init/./Lean/Meta/Tactic/Induction.c Init/./Lean/Meta/Tactic/Injection.c Init/./Lean/Meta/Tactic/Intro.c Init/./Lean/Meta/Tactic/LocalDecl.c Init/./Lean/Meta/Tactic/Revert.c Init/./Lean/Meta/Tactic/Rewrite.c Init/./Lean/Meta/Tactic/Subst.c Init/./Lean/Meta/Tactic/Target.c Init/./Lean/Meta/Tactic/Util.c Init/./Lean/Meta/WHNF.c Init/./Lean/MetavarContext.c Init/./Lean/Modifiers.c Init/./Lean/Parser.c Init/./Lean/Parser/Command.c Init/./Lean/Parser/Level.c Init/./Lean/Parser/Module.c Init/./Lean/Parser/Parser.c Init/./Lean/Parser/Syntax.c Init/./Lean/Parser/Tactic.c Init/./Lean/Parser/Term.c Init/./Lean/Parser/Transform.c Init/./Lean/ProjFns.c Init/./Lean/ReducibilityAttrs.c Init/./Lean/Runtime.c Init/./Lean/Scopes.c Init/./Lean/Structure.c Init/./Lean/Syntax.c Init/./Lean/ToExpr.c Init/./Lean/Util.c Init/./Lean/Util/CollectFVars.c Init/./Lean/Util/CollectLevelParams.c Init/./Lean/Util/CollectMVars.c Init/./Lean/Util/FindExpr.c Init/./Lean/Util/FindMVar.c Init/./Lean/Util/MonadCache.c Init/./Lean/Util/PPExt.c Init/./Lean/Util/PPGoal.c Init/./Lean/Util/Path.c Init/./Lean/Util/Profile.c Init/./Lean/Util/RecDepth.c Init/./Lean/Util/ReplaceExpr.c Init/./Lean/Util/Sorry.c Init/./Lean/Util/Trace.c Init/./Lean/Util/WHNF.c Init/./LeanInit.c Init/./ShareCommon.c Init/./System.c Init/./System/FilePath.c Init/./System/IO.c Init/./System/IOError.c Init/./System/Platform.c Init/./Util.c Init/./WF.c) +add_library (stage0 OBJECT Init/./Coe.c Init/./Control.c Init/./Control/Alternative.c Init/./Control/Applicative.c Init/./Control/Conditional.c Init/./Control/EState.c Init/./Control/Except.c Init/./Control/Functor.c Init/./Control/Id.c Init/./Control/Lift.c Init/./Control/Monad.c Init/./Control/Option.c Init/./Control/Reader.c Init/./Control/State.c Init/./Core.c Init/./Data.c Init/./Data/Array.c Init/./Data/Array/Basic.c Init/./Data/Array/BinSearch.c Init/./Data/Array/QSort.c Init/./Data/AssocList.c Init/./Data/Basic.c Init/./Data/BinomialHeap.c Init/./Data/BinomialHeap/Basic.c Init/./Data/ByteArray.c Init/./Data/ByteArray/Basic.c Init/./Data/Char.c Init/./Data/Char/Basic.c Init/./Data/DList.c Init/./Data/Fin.c Init/./Data/Fin/Basic.c Init/./Data/HashMap.c Init/./Data/HashMap/Basic.c Init/./Data/HashSet.c Init/./Data/Hashable.c Init/./Data/Int.c Init/./Data/Int/Basic.c Init/./Data/List.c Init/./Data/List/Basic.c Init/./Data/List/BasicAux.c Init/./Data/List/Control.c Init/./Data/List/Instances.c Init/./Data/Nat.c Init/./Data/Nat/Basic.c Init/./Data/Nat/Bitwise.c Init/./Data/Nat/Control.c Init/./Data/Nat/Div.c Init/./Data/Option.c Init/./Data/Option/Basic.c Init/./Data/Option/BasicAux.c Init/./Data/Option/Instances.c Init/./Data/PersistentArray.c Init/./Data/PersistentArray/Basic.c Init/./Data/PersistentHashMap.c Init/./Data/PersistentHashMap/Basic.c Init/./Data/PersistentHashSet.c Init/./Data/Queue.c Init/./Data/Queue/Basic.c Init/./Data/RBMap.c Init/./Data/RBMap/Basic.c Init/./Data/RBMap/BasicAux.c Init/./Data/RBTree.c Init/./Data/RBTree/Basic.c Init/./Data/Random.c Init/./Data/Repr.c Init/./Data/Stack.c Init/./Data/Stack/Basic.c Init/./Data/String.c Init/./Data/String/Basic.c Init/./Data/ToString.c Init/./Data/UInt.c Init/./Default.c Init/./Fix.c Init/./HasCoe.c Init/./Lean.c Init/./Lean/Attributes.c Init/./Lean/AuxRecursor.c Init/./Lean/Class.c Init/./Lean/Compiler.c Init/./Lean/Compiler/ClosedTermCache.c Init/./Lean/Compiler/ConstFolding.c Init/./Lean/Compiler/ExportAttr.c Init/./Lean/Compiler/ExternAttr.c Init/./Lean/Compiler/IR.c Init/./Lean/Compiler/IR/Basic.c Init/./Lean/Compiler/IR/Borrow.c Init/./Lean/Compiler/IR/Boxing.c Init/./Lean/Compiler/IR/Checker.c Init/./Lean/Compiler/IR/CompilerM.c Init/./Lean/Compiler/IR/CtorLayout.c Init/./Lean/Compiler/IR/ElimDeadBranches.c Init/./Lean/Compiler/IR/ElimDeadVars.c Init/./Lean/Compiler/IR/EmitC.c Init/./Lean/Compiler/IR/EmitUtil.c Init/./Lean/Compiler/IR/ExpandResetReuse.c Init/./Lean/Compiler/IR/Format.c Init/./Lean/Compiler/IR/FreeVars.c Init/./Lean/Compiler/IR/LiveVars.c Init/./Lean/Compiler/IR/NormIds.c Init/./Lean/Compiler/IR/PushProj.c Init/./Lean/Compiler/IR/RC.c Init/./Lean/Compiler/IR/ResetReuse.c Init/./Lean/Compiler/IR/SimpCase.c Init/./Lean/Compiler/IR/UnboxResult.c Init/./Lean/Compiler/ImplementedByAttr.c Init/./Lean/Compiler/InitAttr.c Init/./Lean/Compiler/InlineAttrs.c Init/./Lean/Compiler/NameMangling.c Init/./Lean/Compiler/NeverExtractAttr.c Init/./Lean/Compiler/Specialize.c Init/./Lean/Compiler/Util.c Init/./Lean/Data/Format.c Init/./Lean/Data/KVMap.c Init/./Lean/Data/LBool.c Init/./Lean/Data/LOption.c Init/./Lean/Data/Name.c Init/./Lean/Data/Occurrences.c Init/./Lean/Data/Options.c Init/./Lean/Data/Position.c Init/./Lean/Data/SMap.c Init/./Lean/Data/Trie.c Init/./Lean/Declaration.c Init/./Lean/Elab.c Init/./Lean/Elab/Alias.c Init/./Lean/Elab/App.c Init/./Lean/Elab/Binders.c Init/./Lean/Elab/BuiltinNotation.c Init/./Lean/Elab/Command.c Init/./Lean/Elab/DeclModifiers.c Init/./Lean/Elab/Declaration.c Init/./Lean/Elab/Definition.c Init/./Lean/Elab/DoNotation.c Init/./Lean/Elab/Exception.c Init/./Lean/Elab/Frontend.c Init/./Lean/Elab/Import.c Init/./Lean/Elab/Level.c Init/./Lean/Elab/Log.c Init/./Lean/Elab/Match.c Init/./Lean/Elab/Quotation.c Init/./Lean/Elab/ResolveName.c Init/./Lean/Elab/StrategyAttrs.c Init/./Lean/Elab/StructInst.c Init/./Lean/Elab/Syntax.c Init/./Lean/Elab/SyntheticMVars.c Init/./Lean/Elab/Tactic.c Init/./Lean/Elab/Tactic/Basic.c Init/./Lean/Elab/Tactic/ElabTerm.c Init/./Lean/Elab/Tactic/Generalize.c Init/./Lean/Elab/Tactic/Induction.c Init/./Lean/Elab/Tactic/Injection.c Init/./Lean/Elab/Term.c Init/./Lean/Elab/Util.c Init/./Lean/Environment.c Init/./Lean/EqnCompiler.c Init/./Lean/EqnCompiler/MatchPattern.c Init/./Lean/Eval.c Init/./Lean/Expr.c Init/./Lean/HeadIndex.c Init/./Lean/Hygiene.c Init/./Lean/Level.c Init/./Lean/Linter.c Init/./Lean/LocalContext.c Init/./Lean/Message.c Init/./Lean/Meta.c Init/./Lean/Meta/AbstractMVars.c Init/./Lean/Meta/AppBuilder.c Init/./Lean/Meta/Basic.c Init/./Lean/Meta/Check.c Init/./Lean/Meta/DiscrTree.c Init/./Lean/Meta/DiscrTreeTypes.c Init/./Lean/Meta/Exception.c Init/./Lean/Meta/ExprDefEq.c Init/./Lean/Meta/FunInfo.c Init/./Lean/Meta/InferType.c Init/./Lean/Meta/Instances.c Init/./Lean/Meta/KAbstract.c Init/./Lean/Meta/LevelDefEq.c Init/./Lean/Meta/Message.c Init/./Lean/Meta/Offset.c Init/./Lean/Meta/RecursorInfo.c Init/./Lean/Meta/Reduce.c Init/./Lean/Meta/SynthInstance.c Init/./Lean/Meta/Tactic.c Init/./Lean/Meta/Tactic/Apply.c Init/./Lean/Meta/Tactic/Assert.c Init/./Lean/Meta/Tactic/Assumption.c Init/./Lean/Meta/Tactic/Cases.c Init/./Lean/Meta/Tactic/Clear.c Init/./Lean/Meta/Tactic/FVarSubst.c Init/./Lean/Meta/Tactic/Generalize.c Init/./Lean/Meta/Tactic/Induction.c Init/./Lean/Meta/Tactic/Injection.c Init/./Lean/Meta/Tactic/Intro.c Init/./Lean/Meta/Tactic/LocalDecl.c Init/./Lean/Meta/Tactic/Revert.c Init/./Lean/Meta/Tactic/Rewrite.c Init/./Lean/Meta/Tactic/Subst.c Init/./Lean/Meta/Tactic/Target.c Init/./Lean/Meta/Tactic/Util.c Init/./Lean/Meta/WHNF.c Init/./Lean/MetavarContext.c Init/./Lean/Modifiers.c Init/./Lean/Parser.c Init/./Lean/Parser/Command.c Init/./Lean/Parser/Level.c Init/./Lean/Parser/Module.c Init/./Lean/Parser/Parser.c Init/./Lean/Parser/Syntax.c Init/./Lean/Parser/Tactic.c Init/./Lean/Parser/Term.c Init/./Lean/Parser/Transform.c Init/./Lean/ProjFns.c Init/./Lean/ReducibilityAttrs.c Init/./Lean/Runtime.c Init/./Lean/Scopes.c Init/./Lean/Structure.c Init/./Lean/Syntax.c Init/./Lean/ToExpr.c Init/./Lean/Util.c Init/./Lean/Util/CollectFVars.c Init/./Lean/Util/CollectLevelParams.c Init/./Lean/Util/CollectMVars.c Init/./Lean/Util/FindExpr.c Init/./Lean/Util/FindMVar.c Init/./Lean/Util/MonadCache.c Init/./Lean/Util/PPExt.c Init/./Lean/Util/PPGoal.c Init/./Lean/Util/Path.c Init/./Lean/Util/Profile.c Init/./Lean/Util/RecDepth.c Init/./Lean/Util/ReplaceExpr.c Init/./Lean/Util/Sorry.c Init/./Lean/Util/Trace.c Init/./Lean/Util/WHNF.c Init/./LeanInit.c Init/./ShareCommon.c Init/./System.c Init/./System/FilePath.c Init/./System/IO.c Init/./System/IOError.c Init/./System/Platform.c Init/./Util.c Init/./WF.c) diff --git a/stage0/stdlib/Init/Lean/Elab/Binders.c b/stage0/stdlib/Init/Lean/Elab/Binders.c index 5d18446f3b..37d5f8db0f 100644 --- a/stage0/stdlib/Init/Lean/Elab/Binders.c +++ b/stage0/stdlib/Init/Lean/Elab/Binders.c @@ -5051,7 +5051,7 @@ _start: { lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; x_5 = l_Lean_Expr_Inhabited; -x_6 = lean_unsigned_to_nat(1u); +x_6 = lean_unsigned_to_nat(0u); x_7 = lean_array_get(x_5, x_2, x_6); x_8 = lean_apply_3(x_1, x_7, x_3, x_4); return x_8; diff --git a/stage0/stdlib/Init/Lean/Elab/SyntheticMVars.c b/stage0/stdlib/Init/Lean/Elab/SyntheticMVars.c index d63080b342..6e516f0865 100644 --- a/stage0/stdlib/Init/Lean/Elab/SyntheticMVars.c +++ b/stage0/stdlib/Init/Lean/Elab/SyntheticMVars.c @@ -60,6 +60,7 @@ lean_object* l___private_Init_Lean_Elab_SyntheticMVars_7__synthesizeSyntheticMVa lean_object* l_Lean_Elab_Term_elabTerm(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*); lean_object* l_List_forM___main___at___private_Init_Lean_Elab_SyntheticMVars_9__reportStuckSyntheticMVars___spec__1___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l___private_Init_Lean_Elab_SyntheticMVars_7__synthesizeSyntheticMVarsStep___closed__4; +uint8_t l_Lean_Expr_hasExprMVar(lean_object*); lean_object* l___private_Init_Lean_Elab_SyntheticMVars_6__synthesizeSyntheticMVar___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_ReaderT_lift___at_Lean_Elab_Term_Lean_Elab_MonadMacroAdapter___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_getMVarDecl___boxed(lean_object*, lean_object*, lean_object*); @@ -110,7 +111,6 @@ lean_object* l_List_filterAuxM___main___at___private_Init_Lean_Elab_SyntheticMVa uint8_t l_Lean_Expr_isMVar(lean_object*); lean_object* l___private_Init_Lean_Elab_SyntheticMVars_7__synthesizeSyntheticMVarsStep___closed__7; lean_object* l_List_filterAuxM___main___at___private_Init_Lean_Elab_SyntheticMVars_7__synthesizeSyntheticMVarsStep___spec__2___closed__9; -uint8_t l_Lean_Expr_hasMVar(lean_object*); lean_object* l_Lean_Elab_Term_synthesizeInstMVarCore(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l___private_Init_Lean_Elab_SyntheticMVars_4__synthesizePendingCoeInstMVar___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_log___at_Lean_Elab_Term_logTrace___spec__1(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*); @@ -830,7 +830,7 @@ if (x_7 == 0) lean_object* x_8; lean_object* x_9; uint8_t x_10; x_8 = lean_ctor_get(x_6, 0); x_9 = lean_ctor_get(x_6, 1); -x_10 = l_Lean_Expr_hasMVar(x_8); +x_10 = l_Lean_Expr_hasExprMVar(x_8); if (x_10 == 0) { lean_object* x_11; @@ -863,7 +863,7 @@ x_18 = lean_ctor_get(x_6, 1); lean_inc(x_18); lean_inc(x_17); lean_dec(x_6); -x_19 = l_Lean_Expr_hasMVar(x_17); +x_19 = l_Lean_Expr_hasExprMVar(x_17); if (x_19 == 0) { lean_object* x_20; lean_object* x_21; diff --git a/stage0/stdlib/Init/Lean/Elab/Tactic.c b/stage0/stdlib/Init/Lean/Elab/Tactic.c index 9228c20b55..85f1f3a413 100644 --- a/stage0/stdlib/Init/Lean/Elab/Tactic.c +++ b/stage0/stdlib/Init/Lean/Elab/Tactic.c @@ -1,6 +1,6 @@ // Lean compiler output // Module: Init.Lean.Elab.Tactic -// Imports: Init.Lean.Elab.Term Init.Lean.Elab.Tactic.Basic Init.Lean.Elab.Tactic.ElabTerm Init.Lean.Elab.Tactic.Induction Init.Lean.Elab.Tactic.Generalize +// Imports: Init.Lean.Elab.Term Init.Lean.Elab.Tactic.Basic Init.Lean.Elab.Tactic.ElabTerm Init.Lean.Elab.Tactic.Induction Init.Lean.Elab.Tactic.Generalize Init.Lean.Elab.Tactic.Injection #include "runtime/lean.h" #if defined(__clang__) #pragma clang diagnostic ignored "-Wunused-parameter" @@ -18,6 +18,7 @@ lean_object* initialize_Init_Lean_Elab_Tactic_Basic(lean_object*); lean_object* initialize_Init_Lean_Elab_Tactic_ElabTerm(lean_object*); lean_object* initialize_Init_Lean_Elab_Tactic_Induction(lean_object*); lean_object* initialize_Init_Lean_Elab_Tactic_Generalize(lean_object*); +lean_object* initialize_Init_Lean_Elab_Tactic_Injection(lean_object*); static bool _G_initialized = false; lean_object* initialize_Init_Lean_Elab_Tactic(lean_object* w) { lean_object * res; @@ -38,6 +39,9 @@ lean_dec_ref(res); res = initialize_Init_Lean_Elab_Tactic_Generalize(lean_io_mk_world()); if (lean_io_result_is_error(res)) return res; lean_dec_ref(res); +res = initialize_Init_Lean_Elab_Tactic_Injection(lean_io_mk_world()); +if (lean_io_result_is_error(res)) return res; +lean_dec_ref(res); return lean_mk_io_result(lean_box(0)); } #ifdef __cplusplus diff --git a/stage0/stdlib/Init/Lean/Elab/Tactic/ElabTerm.c b/stage0/stdlib/Init/Lean/Elab/Tactic/ElabTerm.c index fe092fa050..a34579f4a5 100644 --- a/stage0/stdlib/Init/Lean/Elab/Tactic/ElabTerm.c +++ b/stage0/stdlib/Init/Lean/Elab/Tactic/ElabTerm.c @@ -1,6 +1,6 @@ // Lean compiler output // Module: Init.Lean.Elab.Tactic.ElabTerm -// Imports: Init.Lean.Meta.Tactic.Apply Init.Lean.Elab.Tactic.Basic Init.Lean.Elab.SyntheticMVars +// Imports: Init.Lean.Meta.Tactic.Apply Init.Lean.Meta.Tactic.Assert Init.Lean.Elab.Tactic.Basic Init.Lean.Elab.SyntheticMVars #include "runtime/lean.h" #if defined(__clang__) #pragma clang diagnostic ignored "-Wunused-parameter" @@ -13,15 +13,20 @@ #ifdef __cplusplus extern "C" { #endif +lean_object* l_Lean_Elab_Tactic_elabAsFVar___lambda__1___boxed(lean_object*, lean_object*, lean_object*); lean_object* l___regBuiltinTactic_Lean_Elab_Tactic_evalApply___closed__1; lean_object* l_Lean_Elab_Tactic_withMVarContext___rarg(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_instantiateMVars(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l___regBuiltinTactic_Lean_Elab_Tactic_evalApply___closed__2; +lean_object* l_Lean_Meta_assert___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l___regBuiltinTactic_Lean_Elab_Tactic_evalRefine___closed__1; lean_object* l_Lean_Elab_Tactic_liftMetaM___rarg(lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_ReaderT_bind___at_Lean_Meta_isClassExpensive___main___spec__4___rarg(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_List_append___rarg(lean_object*, lean_object*); lean_object* lean_array_get_size(lean_object*); +lean_object* l_Lean_Elab_Tactic_elabAsFVar___lambda__1(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Tactic_evalApply(lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Elab_Tactic_inferType(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Tactic_evalRefine(lean_object*, lean_object*, lean_object*); lean_object* l___regBuiltinTactic_Lean_Elab_Tactic_evalExact(lean_object*); lean_object* l___private_Init_Lean_Elab_SyntheticMVars_11__synthesizeSyntheticMVarsAux___main(uint8_t, lean_object*, lean_object*, lean_object*); @@ -33,18 +38,23 @@ extern lean_object* l_Lean_Elab_Tactic_declareBuiltinTactic___closed__3; lean_object* l_Lean_Elab_Term_elabTerm(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*); lean_object* l_Lean_Meta_apply___boxed(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Tactic_evalApply___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Elab_Tactic_elabAsFVar___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l___regBuiltinTactic_Lean_Elab_Tactic_evalRefine(lean_object*); lean_object* l_Lean_Elab_Tactic_getMVarDecl___boxed(lean_object*, lean_object*, lean_object*); lean_object* l___regBuiltinTactic_Lean_Elab_Tactic_evalApply(lean_object*); lean_object* lean_name_mk_string(lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_synthesizeSyntheticMVars___boxed(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Tactic_getMainGoal(lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Elab_Tactic_elabAsFVar___lambda__2(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Tactic_evalApply___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Tactic_evalExact___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Tactic_evalExact___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Tactic_evalRefine___lambda__1___closed__1; lean_object* l_Lean_Elab_Tactic_elabTerm___lambda__1(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*); +lean_object* l_Lean_Elab_Tactic_elabAsFVar___lambda__3___closed__1; lean_object* l___regBuiltinTactic_Lean_Elab_Tactic_evalExact___closed__1; +lean_object* l_Lean_Elab_Tactic_elabAsFVar___lambda__2___boxed(lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Elab_Tactic_elabAsFVar___lambda__3___closed__2; lean_object* l___regBuiltinTactic_Lean_Elab_Tactic_evalExact___closed__2; lean_object* l_Lean_Elab_Tactic_evalApply___lambda__1___closed__1; lean_object* l_Lean_Syntax_getArgs(lean_object*); @@ -52,15 +62,19 @@ lean_object* l_Lean_Elab_Tactic_evalRefine___lambda__1(lean_object*, lean_object lean_object* l_Lean_Elab_Tactic_setGoals(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Tactic_addBuiltinTactic(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Tactic_tagUntaggedGoals(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Elab_Tactic_elabAsFVar(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Tactic_assignExprMVar(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Tactic_ensureHasNoMVars(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Tactic_elabTerm(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*); +lean_object* l_Lean_Elab_Tactic_elabAsFVar___lambda__3___closed__3; lean_object* l_Lean_Elab_Tactic_liftTermElabM___rarg(lean_object*, lean_object*, lean_object*); extern lean_object* l_Lean_Parser_Tactic_exact___elambda__1___closed__2; +lean_object* l_Lean_Meta_intro1(lean_object*, uint8_t, lean_object*, lean_object*); lean_object* l_Lean_Elab_Tactic_ensureHasType(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); uint8_t l_Lean_Syntax_isOfKind(lean_object*, lean_object*); extern lean_object* l_Lean_Parser_Tactic_apply___elambda__1___closed__2; lean_object* l_Lean_Elab_Tactic_throwUnsupportedSyntax___rarg(lean_object*, lean_object*); +lean_object* l_Lean_Elab_Tactic_elabAsFVar___lambda__3___closed__4; lean_object* l_Lean_Syntax_getArg(lean_object*, lean_object*); lean_object* l_Lean_Elab_Tactic_collectMVars(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l___regBuiltinTactic_Lean_Elab_Tactic_evalApply___closed__3; @@ -1309,7 +1323,385 @@ x_5 = l_Lean_Elab_Tactic_addBuiltinTactic(x_2, x_3, x_4, x_1); return x_5; } } +lean_object* l_Lean_Elab_Tactic_elabAsFVar___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +_start: +{ +uint8_t x_4; lean_object* x_5; +x_4 = 1; +x_5 = l_Lean_Meta_intro1(x_1, x_4, x_2, x_3); +return x_5; +} +} +lean_object* l_Lean_Elab_Tactic_elabAsFVar___lambda__2(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +_start: +{ +uint8_t x_4; lean_object* x_5; +x_4 = 0; +x_5 = l_Lean_Meta_intro1(x_1, x_4, x_2, x_3); +return x_5; +} +} +lean_object* _init_l_Lean_Elab_Tactic_elabAsFVar___lambda__3___closed__1() { +_start: +{ +lean_object* x_1; +x_1 = lean_mk_string("h"); +return x_1; +} +} +lean_object* _init_l_Lean_Elab_Tactic_elabAsFVar___lambda__3___closed__2() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = lean_box(0); +x_2 = l_Lean_Elab_Tactic_elabAsFVar___lambda__3___closed__1; +x_3 = lean_name_mk_string(x_1, x_2); +return x_3; +} +} +lean_object* _init_l_Lean_Elab_Tactic_elabAsFVar___lambda__3___closed__3() { +_start: +{ +lean_object* x_1; +x_1 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_elabAsFVar___lambda__1___boxed), 3, 0); +return x_1; +} +} +lean_object* _init_l_Lean_Elab_Tactic_elabAsFVar___lambda__3___closed__4() { +_start: +{ +lean_object* x_1; +x_1 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_elabAsFVar___lambda__2___boxed), 3, 0); +return x_1; +} +} +lean_object* l_Lean_Elab_Tactic_elabAsFVar___lambda__3(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) { +_start: +{ +lean_object* x_8; +if (lean_obj_tag(x_5) == 1) +{ +lean_object* x_57; lean_object* x_58; +lean_dec(x_6); +lean_dec(x_4); +lean_dec(x_3); +lean_dec(x_2); +lean_dec(x_1); +x_57 = lean_ctor_get(x_5, 0); +lean_inc(x_57); +lean_dec(x_5); +x_58 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_58, 0, x_57); +lean_ctor_set(x_58, 1, x_7); +return x_58; +} +else +{ +lean_object* x_59; +x_59 = lean_box(0); +x_8 = x_59; +goto block_56; +} +block_56: +{ +lean_object* x_9; +lean_dec(x_8); +lean_inc(x_6); +lean_inc(x_5); +lean_inc(x_1); +x_9 = l_Lean_Elab_Tactic_inferType(x_1, x_5, x_6, x_7); +if (lean_obj_tag(x_9) == 0) +{ +if (lean_obj_tag(x_2) == 0) +{ +lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; +x_10 = lean_ctor_get(x_9, 0); +lean_inc(x_10); +x_11 = lean_ctor_get(x_9, 1); +lean_inc(x_11); +lean_dec(x_9); +x_12 = l_Lean_Elab_Tactic_elabAsFVar___lambda__3___closed__2; +x_13 = lean_alloc_closure((void*)(l_Lean_Meta_assert___boxed), 6, 4); +lean_closure_set(x_13, 0, x_3); +lean_closure_set(x_13, 1, x_12); +lean_closure_set(x_13, 2, x_10); +lean_closure_set(x_13, 3, x_5); +x_14 = l_Lean_Elab_Tactic_elabAsFVar___lambda__3___closed__3; +x_15 = lean_alloc_closure((void*)(l_ReaderT_bind___at_Lean_Meta_isClassExpensive___main___spec__4___rarg), 4, 2); +lean_closure_set(x_15, 0, x_13); +lean_closure_set(x_15, 1, x_14); +lean_inc(x_6); +x_16 = l_Lean_Elab_Tactic_liftMetaM___rarg(x_1, x_15, x_6, x_11); +if (lean_obj_tag(x_16) == 0) +{ +lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; uint8_t x_23; +x_17 = lean_ctor_get(x_16, 0); +lean_inc(x_17); +x_18 = lean_ctor_get(x_16, 1); +lean_inc(x_18); +lean_dec(x_16); +x_19 = lean_ctor_get(x_17, 0); +lean_inc(x_19); +x_20 = lean_ctor_get(x_17, 1); +lean_inc(x_20); +lean_dec(x_17); +x_21 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_21, 0, x_20); +lean_ctor_set(x_21, 1, x_4); +x_22 = l_Lean_Elab_Tactic_setGoals(x_21, x_6, x_18); +lean_dec(x_6); +x_23 = !lean_is_exclusive(x_22); +if (x_23 == 0) +{ +lean_object* x_24; +x_24 = lean_ctor_get(x_22, 0); +lean_dec(x_24); +lean_ctor_set(x_22, 0, x_19); +return x_22; +} +else +{ +lean_object* x_25; lean_object* x_26; +x_25 = lean_ctor_get(x_22, 1); +lean_inc(x_25); +lean_dec(x_22); +x_26 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_26, 0, x_19); +lean_ctor_set(x_26, 1, x_25); +return x_26; +} +} +else +{ +uint8_t x_27; +lean_dec(x_6); +lean_dec(x_4); +x_27 = !lean_is_exclusive(x_16); +if (x_27 == 0) +{ +return x_16; +} +else +{ +lean_object* x_28; lean_object* x_29; lean_object* x_30; +x_28 = lean_ctor_get(x_16, 0); +x_29 = lean_ctor_get(x_16, 1); +lean_inc(x_29); +lean_inc(x_28); +lean_dec(x_16); +x_30 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_30, 0, x_28); +lean_ctor_set(x_30, 1, x_29); +return x_30; +} +} +} +else +{ +lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36; lean_object* x_37; +x_31 = lean_ctor_get(x_9, 0); +lean_inc(x_31); +x_32 = lean_ctor_get(x_9, 1); +lean_inc(x_32); +lean_dec(x_9); +x_33 = lean_ctor_get(x_2, 0); +lean_inc(x_33); +lean_dec(x_2); +x_34 = lean_alloc_closure((void*)(l_Lean_Meta_assert___boxed), 6, 4); +lean_closure_set(x_34, 0, x_3); +lean_closure_set(x_34, 1, x_33); +lean_closure_set(x_34, 2, x_31); +lean_closure_set(x_34, 3, x_5); +x_35 = l_Lean_Elab_Tactic_elabAsFVar___lambda__3___closed__4; +x_36 = lean_alloc_closure((void*)(l_ReaderT_bind___at_Lean_Meta_isClassExpensive___main___spec__4___rarg), 4, 2); +lean_closure_set(x_36, 0, x_34); +lean_closure_set(x_36, 1, x_35); +lean_inc(x_6); +x_37 = l_Lean_Elab_Tactic_liftMetaM___rarg(x_1, x_36, x_6, x_32); +if (lean_obj_tag(x_37) == 0) +{ +lean_object* x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43; uint8_t x_44; +x_38 = lean_ctor_get(x_37, 0); +lean_inc(x_38); +x_39 = lean_ctor_get(x_37, 1); +lean_inc(x_39); +lean_dec(x_37); +x_40 = lean_ctor_get(x_38, 0); +lean_inc(x_40); +x_41 = lean_ctor_get(x_38, 1); +lean_inc(x_41); +lean_dec(x_38); +x_42 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_42, 0, x_41); +lean_ctor_set(x_42, 1, x_4); +x_43 = l_Lean_Elab_Tactic_setGoals(x_42, x_6, x_39); +lean_dec(x_6); +x_44 = !lean_is_exclusive(x_43); +if (x_44 == 0) +{ +lean_object* x_45; +x_45 = lean_ctor_get(x_43, 0); +lean_dec(x_45); +lean_ctor_set(x_43, 0, x_40); +return x_43; +} +else +{ +lean_object* x_46; lean_object* x_47; +x_46 = lean_ctor_get(x_43, 1); +lean_inc(x_46); +lean_dec(x_43); +x_47 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_47, 0, x_40); +lean_ctor_set(x_47, 1, x_46); +return x_47; +} +} +else +{ +uint8_t x_48; +lean_dec(x_6); +lean_dec(x_4); +x_48 = !lean_is_exclusive(x_37); +if (x_48 == 0) +{ +return x_37; +} +else +{ +lean_object* x_49; lean_object* x_50; lean_object* x_51; +x_49 = lean_ctor_get(x_37, 0); +x_50 = lean_ctor_get(x_37, 1); +lean_inc(x_50); +lean_inc(x_49); +lean_dec(x_37); +x_51 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_51, 0, x_49); +lean_ctor_set(x_51, 1, x_50); +return x_51; +} +} +} +} +else +{ +uint8_t x_52; +lean_dec(x_6); +lean_dec(x_5); +lean_dec(x_4); +lean_dec(x_3); +lean_dec(x_2); +lean_dec(x_1); +x_52 = !lean_is_exclusive(x_9); +if (x_52 == 0) +{ +return x_9; +} +else +{ +lean_object* x_53; lean_object* x_54; lean_object* x_55; +x_53 = lean_ctor_get(x_9, 0); +x_54 = lean_ctor_get(x_9, 1); +lean_inc(x_54); +lean_inc(x_53); +lean_dec(x_9); +x_55 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_55, 0, x_53); +lean_ctor_set(x_55, 1, x_54); +return x_55; +} +} +} +} +} +lean_object* l_Lean_Elab_Tactic_elabAsFVar(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) { +_start: +{ +lean_object* x_5; +lean_inc(x_3); +lean_inc(x_1); +x_5 = l_Lean_Elab_Tactic_getMainGoal(x_1, x_3, x_4); +if (lean_obj_tag(x_5) == 0) +{ +lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; uint8_t x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; +x_6 = lean_ctor_get(x_5, 0); +lean_inc(x_6); +x_7 = lean_ctor_get(x_5, 1); +lean_inc(x_7); +lean_dec(x_5); +x_8 = lean_ctor_get(x_6, 0); +lean_inc(x_8); +x_9 = lean_ctor_get(x_6, 1); +lean_inc(x_9); +lean_dec(x_6); +x_10 = lean_box(0); +x_11 = 0; +x_12 = lean_box(x_11); +lean_inc(x_1); +x_13 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_elabTerm___boxed), 5, 3); +lean_closure_set(x_13, 0, x_1); +lean_closure_set(x_13, 1, x_10); +lean_closure_set(x_13, 2, x_12); +lean_inc(x_8); +x_14 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_elabAsFVar___lambda__3), 7, 4); +lean_closure_set(x_14, 0, x_1); +lean_closure_set(x_14, 1, x_2); +lean_closure_set(x_14, 2, x_8); +lean_closure_set(x_14, 3, x_9); +x_15 = lean_alloc_closure((void*)(l_ReaderT_bind___at_Lean_Elab_Tactic_monadLog___spec__2___rarg), 4, 2); +lean_closure_set(x_15, 0, x_13); +lean_closure_set(x_15, 1, x_14); +x_16 = l_Lean_Elab_Tactic_withMVarContext___rarg(x_8, x_15, x_3, x_7); +lean_dec(x_8); +return x_16; +} +else +{ +uint8_t x_17; +lean_dec(x_3); +lean_dec(x_2); +lean_dec(x_1); +x_17 = !lean_is_exclusive(x_5); +if (x_17 == 0) +{ +return x_5; +} +else +{ +lean_object* x_18; lean_object* x_19; lean_object* x_20; +x_18 = lean_ctor_get(x_5, 0); +x_19 = lean_ctor_get(x_5, 1); +lean_inc(x_19); +lean_inc(x_18); +lean_dec(x_5); +x_20 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_20, 0, x_18); +lean_ctor_set(x_20, 1, x_19); +return x_20; +} +} +} +} +lean_object* l_Lean_Elab_Tactic_elabAsFVar___lambda__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +_start: +{ +lean_object* x_4; +x_4 = l_Lean_Elab_Tactic_elabAsFVar___lambda__1(x_1, x_2, x_3); +lean_dec(x_2); +return x_4; +} +} +lean_object* l_Lean_Elab_Tactic_elabAsFVar___lambda__2___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +_start: +{ +lean_object* x_4; +x_4 = l_Lean_Elab_Tactic_elabAsFVar___lambda__2(x_1, x_2, x_3); +lean_dec(x_2); +return x_4; +} +} lean_object* initialize_Init_Lean_Meta_Tactic_Apply(lean_object*); +lean_object* initialize_Init_Lean_Meta_Tactic_Assert(lean_object*); lean_object* initialize_Init_Lean_Elab_Tactic_Basic(lean_object*); lean_object* initialize_Init_Lean_Elab_SyntheticMVars(lean_object*); static bool _G_initialized = false; @@ -1320,6 +1712,9 @@ _G_initialized = true; res = initialize_Init_Lean_Meta_Tactic_Apply(lean_io_mk_world()); if (lean_io_result_is_error(res)) return res; lean_dec_ref(res); +res = initialize_Init_Lean_Meta_Tactic_Assert(lean_io_mk_world()); +if (lean_io_result_is_error(res)) return res; +lean_dec_ref(res); res = initialize_Init_Lean_Elab_Tactic_Basic(lean_io_mk_world()); if (lean_io_result_is_error(res)) return res; lean_dec_ref(res); @@ -1357,6 +1752,14 @@ lean_mark_persistent(l___regBuiltinTactic_Lean_Elab_Tactic_evalApply___closed__3 res = l___regBuiltinTactic_Lean_Elab_Tactic_evalApply(lean_io_mk_world()); if (lean_io_result_is_error(res)) return res; lean_dec_ref(res); +l_Lean_Elab_Tactic_elabAsFVar___lambda__3___closed__1 = _init_l_Lean_Elab_Tactic_elabAsFVar___lambda__3___closed__1(); +lean_mark_persistent(l_Lean_Elab_Tactic_elabAsFVar___lambda__3___closed__1); +l_Lean_Elab_Tactic_elabAsFVar___lambda__3___closed__2 = _init_l_Lean_Elab_Tactic_elabAsFVar___lambda__3___closed__2(); +lean_mark_persistent(l_Lean_Elab_Tactic_elabAsFVar___lambda__3___closed__2); +l_Lean_Elab_Tactic_elabAsFVar___lambda__3___closed__3 = _init_l_Lean_Elab_Tactic_elabAsFVar___lambda__3___closed__3(); +lean_mark_persistent(l_Lean_Elab_Tactic_elabAsFVar___lambda__3___closed__3); +l_Lean_Elab_Tactic_elabAsFVar___lambda__3___closed__4 = _init_l_Lean_Elab_Tactic_elabAsFVar___lambda__3___closed__4(); +lean_mark_persistent(l_Lean_Elab_Tactic_elabAsFVar___lambda__3___closed__4); return lean_mk_io_result(lean_box(0)); } #ifdef __cplusplus diff --git a/stage0/stdlib/Init/Lean/Elab/Tactic/Injection.c b/stage0/stdlib/Init/Lean/Elab/Tactic/Injection.c new file mode 100644 index 0000000000..6482c2ce8e --- /dev/null +++ b/stage0/stdlib/Init/Lean/Elab/Tactic/Injection.c @@ -0,0 +1,387 @@ +// Lean compiler output +// Module: Init.Lean.Elab.Tactic.Injection +// Imports: Init.Lean.Meta.Tactic.Injection Init.Lean.Elab.Tactic.ElabTerm +#include "runtime/lean.h" +#if defined(__clang__) +#pragma clang diagnostic ignored "-Wunused-parameter" +#pragma clang diagnostic ignored "-Wunused-label" +#elif defined(__GNUC__) && !defined(__CLANG__) +#pragma GCC diagnostic ignored "-Wunused-parameter" +#pragma GCC diagnostic ignored "-Wunused-label" +#pragma GCC diagnostic ignored "-Wunused-but-set-variable" +#endif +#ifdef __cplusplus +extern "C" { +#endif +lean_object* l_Lean_Elab_Tactic_withMVarContext___rarg(lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Elab_Tactic_liftMetaM___rarg(lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_ReaderT_bind___at_Lean_Meta_isClassExpensive___main___spec__4___rarg(lean_object*, lean_object*, lean_object*, lean_object*); +extern lean_object* l_Lean_Elab_Tactic_liftMetaTactic___closed__1; +lean_object* l_ReaderT_bind___at_Lean_Elab_Tactic_monadLog___spec__2___rarg(lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l___regBuiltinTactic_Lean_Elab_Tactic_evalInjection___closed__1; +extern lean_object* l_Lean_Elab_Tactic_declareBuiltinTactic___closed__3; +lean_object* l_Lean_Syntax_getId(lean_object*); +lean_object* lean_name_mk_string(lean_object*, lean_object*); +lean_object* l_Lean_Elab_Tactic_getMainGoal(lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Elab_Tactic_evalInjection___closed__1; +lean_object* l___private_Init_Lean_Elab_Tactic_Injection_1__getInjectionNewIds(lean_object*); +lean_object* l_List_map___main___at___private_Init_Lean_Elab_Tactic_Injection_1__getInjectionNewIds___spec__1(lean_object*); +lean_object* l___regBuiltinTactic_Lean_Elab_Tactic_evalInjection(lean_object*); +lean_object* l___regBuiltinTactic_Lean_Elab_Tactic_evalInjection___closed__2; +lean_object* l_Lean_Meta_injection___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Elab_Tactic_evalInjection(lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Syntax_getArgs(lean_object*); +lean_object* l_Lean_Elab_Tactic_addBuiltinTactic(lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Elab_Tactic_evalInjection___lambda__1___boxed(lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Elab_Tactic_elabAsFVar(lean_object*, lean_object*, lean_object*, lean_object*); +uint8_t l_Lean_Syntax_isNone(lean_object*); +lean_object* l_Array_toList___rarg(lean_object*); +lean_object* l_Lean_Elab_Tactic_evalInjection___lambda__1(lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Syntax_getArg(lean_object*, lean_object*); +uint8_t l_List_isEmpty___rarg(lean_object*); +lean_object* l___private_Init_Lean_Elab_Tactic_Injection_1__getInjectionNewIds___boxed(lean_object*); +extern lean_object* l_Lean_Parser_Tactic_injection___elambda__1___closed__2; +lean_object* l___regBuiltinTactic_Lean_Elab_Tactic_evalInjection___closed__3; +lean_object* l_Lean_Elab_Tactic_liftMetaTacticAux___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_List_map___main___at___private_Init_Lean_Elab_Tactic_Injection_1__getInjectionNewIds___spec__1(lean_object* x_1) { +_start: +{ +if (lean_obj_tag(x_1) == 0) +{ +lean_object* x_2; +x_2 = lean_box(0); +return x_2; +} +else +{ +uint8_t x_3; +x_3 = !lean_is_exclusive(x_1); +if (x_3 == 0) +{ +lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; +x_4 = lean_ctor_get(x_1, 0); +x_5 = lean_ctor_get(x_1, 1); +x_6 = l_Lean_Syntax_getId(x_4); +lean_dec(x_4); +x_7 = l_List_map___main___at___private_Init_Lean_Elab_Tactic_Injection_1__getInjectionNewIds___spec__1(x_5); +lean_ctor_set(x_1, 1, x_7); +lean_ctor_set(x_1, 0, x_6); +return x_1; +} +else +{ +lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; +x_8 = lean_ctor_get(x_1, 0); +x_9 = lean_ctor_get(x_1, 1); +lean_inc(x_9); +lean_inc(x_8); +lean_dec(x_1); +x_10 = l_Lean_Syntax_getId(x_8); +lean_dec(x_8); +x_11 = l_List_map___main___at___private_Init_Lean_Elab_Tactic_Injection_1__getInjectionNewIds___spec__1(x_9); +x_12 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_12, 0, x_10); +lean_ctor_set(x_12, 1, x_11); +return x_12; +} +} +} +} +lean_object* l___private_Init_Lean_Elab_Tactic_Injection_1__getInjectionNewIds(lean_object* x_1) { +_start: +{ +uint8_t x_2; +x_2 = l_Lean_Syntax_isNone(x_1); +if (x_2 == 0) +{ +lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; +x_3 = lean_unsigned_to_nat(1u); +x_4 = l_Lean_Syntax_getArg(x_1, x_3); +x_5 = l_Lean_Syntax_getArgs(x_4); +lean_dec(x_4); +x_6 = l_Array_toList___rarg(x_5); +lean_dec(x_5); +x_7 = l_List_map___main___at___private_Init_Lean_Elab_Tactic_Injection_1__getInjectionNewIds___spec__1(x_6); +return x_7; +} +else +{ +lean_object* x_8; +x_8 = lean_box(0); +return x_8; +} +} +} +lean_object* l___private_Init_Lean_Elab_Tactic_Injection_1__getInjectionNewIds___boxed(lean_object* x_1) { +_start: +{ +lean_object* x_2; +x_2 = l___private_Init_Lean_Elab_Tactic_Injection_1__getInjectionNewIds(x_1); +lean_dec(x_1); +return x_2; +} +} +lean_object* l_Lean_Elab_Tactic_evalInjection___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +_start: +{ +if (lean_obj_tag(x_1) == 0) +{ +lean_object* x_4; lean_object* x_5; +x_4 = lean_box(0); +x_5 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_5, 0, x_4); +lean_ctor_set(x_5, 1, x_3); +return x_5; +} +else +{ +lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; +x_6 = lean_ctor_get(x_1, 0); +x_7 = lean_box(0); +lean_inc(x_6); +x_8 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_8, 0, x_6); +lean_ctor_set(x_8, 1, x_7); +x_9 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_9, 0, x_8); +lean_ctor_set(x_9, 1, x_3); +return x_9; +} +} +} +lean_object* _init_l_Lean_Elab_Tactic_evalInjection___closed__1() { +_start: +{ +lean_object* x_1; +x_1 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_evalInjection___lambda__1___boxed), 3, 0); +return x_1; +} +} +lean_object* l_Lean_Elab_Tactic_evalInjection(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +_start: +{ +lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; +x_4 = lean_unsigned_to_nat(1u); +x_5 = l_Lean_Syntax_getArg(x_1, x_4); +x_6 = lean_box(0); +lean_inc(x_2); +x_7 = l_Lean_Elab_Tactic_elabAsFVar(x_5, x_6, x_2, x_3); +if (lean_obj_tag(x_7) == 0) +{ +lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; +x_8 = lean_ctor_get(x_7, 0); +lean_inc(x_8); +x_9 = lean_ctor_get(x_7, 1); +lean_inc(x_9); +lean_dec(x_7); +x_10 = lean_unsigned_to_nat(2u); +x_11 = l_Lean_Syntax_getArg(x_1, x_10); +x_12 = l___private_Init_Lean_Elab_Tactic_Injection_1__getInjectionNewIds(x_11); +lean_dec(x_11); +lean_inc(x_2); +lean_inc(x_1); +x_13 = l_Lean_Elab_Tactic_getMainGoal(x_1, x_2, x_9); +if (lean_obj_tag(x_13) == 0) +{ +lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; uint8_t x_18; lean_object* x_19; +x_14 = lean_ctor_get(x_13, 0); +lean_inc(x_14); +x_15 = lean_ctor_get(x_13, 1); +lean_inc(x_15); +lean_dec(x_13); +x_16 = lean_ctor_get(x_14, 0); +lean_inc(x_16); +x_17 = lean_ctor_get(x_14, 1); +lean_inc(x_17); +lean_dec(x_14); +x_18 = l_List_isEmpty___rarg(x_12); +x_19 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_liftMetaTacticAux___rarg___lambda__1___boxed), 4, 1); +lean_closure_set(x_19, 0, x_17); +if (x_18 == 0) +{ +uint8_t x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; +x_20 = 1; +x_21 = lean_box(x_20); +lean_inc(x_16); +x_22 = lean_alloc_closure((void*)(l_Lean_Meta_injection___boxed), 6, 4); +lean_closure_set(x_22, 0, x_16); +lean_closure_set(x_22, 1, x_8); +lean_closure_set(x_22, 2, x_12); +lean_closure_set(x_22, 3, x_21); +x_23 = l_Lean_Elab_Tactic_evalInjection___closed__1; +x_24 = lean_alloc_closure((void*)(l_ReaderT_bind___at_Lean_Meta_isClassExpensive___main___spec__4___rarg), 4, 2); +lean_closure_set(x_24, 0, x_22); +lean_closure_set(x_24, 1, x_23); +x_25 = l_Lean_Elab_Tactic_liftMetaTactic___closed__1; +x_26 = lean_alloc_closure((void*)(l_ReaderT_bind___at_Lean_Meta_isClassExpensive___main___spec__4___rarg), 4, 2); +lean_closure_set(x_26, 0, x_24); +lean_closure_set(x_26, 1, x_25); +x_27 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_liftMetaM___rarg), 4, 2); +lean_closure_set(x_27, 0, x_1); +lean_closure_set(x_27, 1, x_26); +x_28 = lean_alloc_closure((void*)(l_ReaderT_bind___at_Lean_Elab_Tactic_monadLog___spec__2___rarg), 4, 2); +lean_closure_set(x_28, 0, x_27); +lean_closure_set(x_28, 1, x_19); +x_29 = l_Lean_Elab_Tactic_withMVarContext___rarg(x_16, x_28, x_2, x_15); +lean_dec(x_16); +return x_29; +} +else +{ +uint8_t x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36; lean_object* x_37; lean_object* x_38; lean_object* x_39; +x_30 = 0; +x_31 = lean_box(x_30); +lean_inc(x_16); +x_32 = lean_alloc_closure((void*)(l_Lean_Meta_injection___boxed), 6, 4); +lean_closure_set(x_32, 0, x_16); +lean_closure_set(x_32, 1, x_8); +lean_closure_set(x_32, 2, x_12); +lean_closure_set(x_32, 3, x_31); +x_33 = l_Lean_Elab_Tactic_evalInjection___closed__1; +x_34 = lean_alloc_closure((void*)(l_ReaderT_bind___at_Lean_Meta_isClassExpensive___main___spec__4___rarg), 4, 2); +lean_closure_set(x_34, 0, x_32); +lean_closure_set(x_34, 1, x_33); +x_35 = l_Lean_Elab_Tactic_liftMetaTactic___closed__1; +x_36 = lean_alloc_closure((void*)(l_ReaderT_bind___at_Lean_Meta_isClassExpensive___main___spec__4___rarg), 4, 2); +lean_closure_set(x_36, 0, x_34); +lean_closure_set(x_36, 1, x_35); +x_37 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_liftMetaM___rarg), 4, 2); +lean_closure_set(x_37, 0, x_1); +lean_closure_set(x_37, 1, x_36); +x_38 = lean_alloc_closure((void*)(l_ReaderT_bind___at_Lean_Elab_Tactic_monadLog___spec__2___rarg), 4, 2); +lean_closure_set(x_38, 0, x_37); +lean_closure_set(x_38, 1, x_19); +x_39 = l_Lean_Elab_Tactic_withMVarContext___rarg(x_16, x_38, x_2, x_15); +lean_dec(x_16); +return x_39; +} +} +else +{ +uint8_t x_40; +lean_dec(x_12); +lean_dec(x_8); +lean_dec(x_2); +lean_dec(x_1); +x_40 = !lean_is_exclusive(x_13); +if (x_40 == 0) +{ +return x_13; +} +else +{ +lean_object* x_41; lean_object* x_42; lean_object* x_43; +x_41 = lean_ctor_get(x_13, 0); +x_42 = lean_ctor_get(x_13, 1); +lean_inc(x_42); +lean_inc(x_41); +lean_dec(x_13); +x_43 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_43, 0, x_41); +lean_ctor_set(x_43, 1, x_42); +return x_43; +} +} +} +else +{ +uint8_t x_44; +lean_dec(x_2); +lean_dec(x_1); +x_44 = !lean_is_exclusive(x_7); +if (x_44 == 0) +{ +return x_7; +} +else +{ +lean_object* x_45; lean_object* x_46; lean_object* x_47; +x_45 = lean_ctor_get(x_7, 0); +x_46 = lean_ctor_get(x_7, 1); +lean_inc(x_46); +lean_inc(x_45); +lean_dec(x_7); +x_47 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_47, 0, x_45); +lean_ctor_set(x_47, 1, x_46); +return x_47; +} +} +} +} +lean_object* l_Lean_Elab_Tactic_evalInjection___lambda__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +_start: +{ +lean_object* x_4; +x_4 = l_Lean_Elab_Tactic_evalInjection___lambda__1(x_1, x_2, x_3); +lean_dec(x_2); +lean_dec(x_1); +return x_4; +} +} +lean_object* _init_l___regBuiltinTactic_Lean_Elab_Tactic_evalInjection___closed__1() { +_start: +{ +lean_object* x_1; +x_1 = lean_mk_string("evalInjection"); +return x_1; +} +} +lean_object* _init_l___regBuiltinTactic_Lean_Elab_Tactic_evalInjection___closed__2() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Elab_Tactic_declareBuiltinTactic___closed__3; +x_2 = l___regBuiltinTactic_Lean_Elab_Tactic_evalInjection___closed__1; +x_3 = lean_name_mk_string(x_1, x_2); +return x_3; +} +} +lean_object* _init_l___regBuiltinTactic_Lean_Elab_Tactic_evalInjection___closed__3() { +_start: +{ +lean_object* x_1; +x_1 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_evalInjection), 3, 0); +return x_1; +} +} +lean_object* l___regBuiltinTactic_Lean_Elab_Tactic_evalInjection(lean_object* x_1) { +_start: +{ +lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; +x_2 = l_Lean_Parser_Tactic_injection___elambda__1___closed__2; +x_3 = l___regBuiltinTactic_Lean_Elab_Tactic_evalInjection___closed__2; +x_4 = l___regBuiltinTactic_Lean_Elab_Tactic_evalInjection___closed__3; +x_5 = l_Lean_Elab_Tactic_addBuiltinTactic(x_2, x_3, x_4, x_1); +return x_5; +} +} +lean_object* initialize_Init_Lean_Meta_Tactic_Injection(lean_object*); +lean_object* initialize_Init_Lean_Elab_Tactic_ElabTerm(lean_object*); +static bool _G_initialized = false; +lean_object* initialize_Init_Lean_Elab_Tactic_Injection(lean_object* w) { +lean_object * res; +if (_G_initialized) return lean_mk_io_result(lean_box(0)); +_G_initialized = true; +res = initialize_Init_Lean_Meta_Tactic_Injection(lean_io_mk_world()); +if (lean_io_result_is_error(res)) return res; +lean_dec_ref(res); +res = initialize_Init_Lean_Elab_Tactic_ElabTerm(lean_io_mk_world()); +if (lean_io_result_is_error(res)) return res; +lean_dec_ref(res); +l_Lean_Elab_Tactic_evalInjection___closed__1 = _init_l_Lean_Elab_Tactic_evalInjection___closed__1(); +lean_mark_persistent(l_Lean_Elab_Tactic_evalInjection___closed__1); +l___regBuiltinTactic_Lean_Elab_Tactic_evalInjection___closed__1 = _init_l___regBuiltinTactic_Lean_Elab_Tactic_evalInjection___closed__1(); +lean_mark_persistent(l___regBuiltinTactic_Lean_Elab_Tactic_evalInjection___closed__1); +l___regBuiltinTactic_Lean_Elab_Tactic_evalInjection___closed__2 = _init_l___regBuiltinTactic_Lean_Elab_Tactic_evalInjection___closed__2(); +lean_mark_persistent(l___regBuiltinTactic_Lean_Elab_Tactic_evalInjection___closed__2); +l___regBuiltinTactic_Lean_Elab_Tactic_evalInjection___closed__3 = _init_l___regBuiltinTactic_Lean_Elab_Tactic_evalInjection___closed__3(); +lean_mark_persistent(l___regBuiltinTactic_Lean_Elab_Tactic_evalInjection___closed__3); +res = l___regBuiltinTactic_Lean_Elab_Tactic_evalInjection(lean_io_mk_world()); +if (lean_io_result_is_error(res)) return res; +lean_dec_ref(res); +return lean_mk_io_result(lean_box(0)); +} +#ifdef __cplusplus +} +#endif diff --git a/stage0/stdlib/Init/Lean/Meta/Tactic/Injection.c b/stage0/stdlib/Init/Lean/Meta/Tactic/Injection.c index a63a61023f..eea1f31ac2 100644 --- a/stage0/stdlib/Init/Lean/Meta/Tactic/Injection.c +++ b/stage0/stdlib/Init/Lean/Meta/Tactic/Injection.c @@ -587,7 +587,6 @@ lean_inc(x_89); lean_dec(x_88); x_90 = l_Lean_Expr_mvarId_x21(x_85); lean_dec(x_85); -lean_inc(x_90); x_91 = l_Lean_Meta_tryClear(x_90, x_1, x_5, x_89); lean_dec(x_5); if (lean_obj_tag(x_91) == 0) @@ -598,216 +597,216 @@ if (x_92 == 0) { lean_object* x_93; lean_object* x_94; lean_object* x_95; x_93 = lean_ctor_get(x_91, 0); -lean_dec(x_93); x_94 = lean_ctor_get(x_50, 4); lean_inc(x_94); lean_dec(x_50); x_95 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_95, 0, x_90); +lean_ctor_set(x_95, 0, x_93); lean_ctor_set(x_95, 1, x_94); lean_ctor_set(x_91, 0, x_95); return x_91; } else { -lean_object* x_96; lean_object* x_97; lean_object* x_98; lean_object* x_99; -x_96 = lean_ctor_get(x_91, 1); +lean_object* x_96; lean_object* x_97; lean_object* x_98; lean_object* x_99; lean_object* x_100; +x_96 = lean_ctor_get(x_91, 0); +x_97 = lean_ctor_get(x_91, 1); +lean_inc(x_97); lean_inc(x_96); lean_dec(x_91); -x_97 = lean_ctor_get(x_50, 4); -lean_inc(x_97); +x_98 = lean_ctor_get(x_50, 4); +lean_inc(x_98); lean_dec(x_50); -x_98 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_98, 0, x_90); -lean_ctor_set(x_98, 1, x_97); -x_99 = lean_alloc_ctor(0, 2, 0); -lean_ctor_set(x_99, 0, x_98); -lean_ctor_set(x_99, 1, x_96); -return x_99; +x_99 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_99, 0, x_96); +lean_ctor_set(x_99, 1, x_98); +x_100 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_100, 0, x_99); +lean_ctor_set(x_100, 1, x_97); +return x_100; } } else { -uint8_t x_100; -lean_dec(x_90); +uint8_t x_101; lean_dec(x_50); -x_100 = !lean_is_exclusive(x_91); -if (x_100 == 0) +x_101 = !lean_is_exclusive(x_91); +if (x_101 == 0) { return x_91; } else { -lean_object* x_101; lean_object* x_102; lean_object* x_103; -x_101 = lean_ctor_get(x_91, 0); -x_102 = lean_ctor_get(x_91, 1); +lean_object* x_102; lean_object* x_103; lean_object* x_104; +x_102 = lean_ctor_get(x_91, 0); +x_103 = lean_ctor_get(x_91, 1); +lean_inc(x_103); lean_inc(x_102); -lean_inc(x_101); lean_dec(x_91); -x_103 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_103, 0, x_101); -lean_ctor_set(x_103, 1, x_102); -return x_103; +x_104 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_104, 0, x_102); +lean_ctor_set(x_104, 1, x_103); +return x_104; } } } else { -uint8_t x_104; +uint8_t x_105; lean_dec(x_85); lean_dec(x_50); lean_dec(x_5); lean_dec(x_1); -x_104 = !lean_is_exclusive(x_88); -if (x_104 == 0) +x_105 = !lean_is_exclusive(x_88); +if (x_105 == 0) { return x_88; } else { -lean_object* x_105; lean_object* x_106; lean_object* x_107; -x_105 = lean_ctor_get(x_88, 0); -x_106 = lean_ctor_get(x_88, 1); +lean_object* x_106; lean_object* x_107; lean_object* x_108; +x_106 = lean_ctor_get(x_88, 0); +x_107 = lean_ctor_get(x_88, 1); +lean_inc(x_107); lean_inc(x_106); -lean_inc(x_105); lean_dec(x_88); -x_107 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_107, 0, x_105); -lean_ctor_set(x_107, 1, x_106); -return x_107; +x_108 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_108, 0, x_106); +lean_ctor_set(x_108, 1, x_107); +return x_108; } } } else { -uint8_t x_108; +uint8_t x_109; lean_dec(x_79); lean_dec(x_54); lean_dec(x_50); lean_dec(x_5); lean_dec(x_3); lean_dec(x_1); -x_108 = !lean_is_exclusive(x_80); -if (x_108 == 0) +x_109 = !lean_is_exclusive(x_80); +if (x_109 == 0) { return x_80; } else { -lean_object* x_109; lean_object* x_110; lean_object* x_111; -x_109 = lean_ctor_get(x_80, 0); -x_110 = lean_ctor_get(x_80, 1); +lean_object* x_110; lean_object* x_111; lean_object* x_112; +x_110 = lean_ctor_get(x_80, 0); +x_111 = lean_ctor_get(x_80, 1); +lean_inc(x_111); lean_inc(x_110); -lean_inc(x_109); lean_dec(x_80); -x_111 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_111, 0, x_109); -lean_ctor_set(x_111, 1, x_110); -return x_111; +x_112 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_112, 0, x_110); +lean_ctor_set(x_112, 1, x_111); +return x_112; } } } else { -lean_object* x_112; lean_object* x_113; lean_object* x_114; +lean_object* x_113; lean_object* x_114; lean_object* x_115; lean_dec(x_76); lean_dec(x_54); lean_dec(x_50); lean_dec(x_1); -x_112 = lean_ctor_get(x_75, 1); -lean_inc(x_112); +x_113 = lean_ctor_get(x_75, 1); +lean_inc(x_113); lean_dec(x_75); -x_113 = l_Lean_Meta_injectionCore___lambda__1___closed__8; -x_114 = l_Lean_Meta_throwTacticEx___rarg(x_2, x_3, x_113, x_5, x_112); +x_114 = l_Lean_Meta_injectionCore___lambda__1___closed__8; +x_115 = l_Lean_Meta_throwTacticEx___rarg(x_2, x_3, x_114, x_5, x_113); lean_dec(x_5); -return x_114; +return x_115; } } else { -uint8_t x_115; +uint8_t x_116; lean_dec(x_54); lean_dec(x_50); lean_dec(x_5); lean_dec(x_3); lean_dec(x_2); lean_dec(x_1); -x_115 = !lean_is_exclusive(x_75); -if (x_115 == 0) +x_116 = !lean_is_exclusive(x_75); +if (x_116 == 0) { return x_75; } else { -lean_object* x_116; lean_object* x_117; lean_object* x_118; -x_116 = lean_ctor_get(x_75, 0); -x_117 = lean_ctor_get(x_75, 1); +lean_object* x_117; lean_object* x_118; lean_object* x_119; +x_117 = lean_ctor_get(x_75, 0); +x_118 = lean_ctor_get(x_75, 1); +lean_inc(x_118); lean_inc(x_117); -lean_inc(x_116); lean_dec(x_75); -x_118 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_118, 0, x_116); -lean_ctor_set(x_118, 1, x_117); -return x_118; +x_119 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_119, 0, x_117); +lean_ctor_set(x_119, 1, x_118); +return x_119; } } } else { -uint8_t x_119; +uint8_t x_120; lean_dec(x_54); lean_dec(x_50); lean_dec(x_5); lean_dec(x_3); lean_dec(x_2); lean_dec(x_1); -x_119 = !lean_is_exclusive(x_72); -if (x_119 == 0) +x_120 = !lean_is_exclusive(x_72); +if (x_120 == 0) { return x_72; } else { -lean_object* x_120; lean_object* x_121; lean_object* x_122; -x_120 = lean_ctor_get(x_72, 0); -x_121 = lean_ctor_get(x_72, 1); +lean_object* x_121; lean_object* x_122; lean_object* x_123; +x_121 = lean_ctor_get(x_72, 0); +x_122 = lean_ctor_get(x_72, 1); +lean_inc(x_122); lean_inc(x_121); -lean_inc(x_120); lean_dec(x_72); -x_122 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_122, 0, x_120); -lean_ctor_set(x_122, 1, x_121); -return x_122; +x_123 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_123, 0, x_121); +lean_ctor_set(x_123, 1, x_122); +return x_123; } } } } else { -uint8_t x_123; +uint8_t x_124; lean_dec(x_51); lean_dec(x_50); lean_dec(x_5); lean_dec(x_3); lean_dec(x_2); lean_dec(x_1); -x_123 = !lean_is_exclusive(x_53); -if (x_123 == 0) +x_124 = !lean_is_exclusive(x_53); +if (x_124 == 0) { return x_53; } else { -lean_object* x_124; lean_object* x_125; lean_object* x_126; -x_124 = lean_ctor_get(x_53, 0); -x_125 = lean_ctor_get(x_53, 1); +lean_object* x_125; lean_object* x_126; lean_object* x_127; +x_125 = lean_ctor_get(x_53, 0); +x_126 = lean_ctor_get(x_53, 1); +lean_inc(x_126); lean_inc(x_125); -lean_inc(x_124); lean_dec(x_53); -x_126 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_126, 0, x_124); -lean_ctor_set(x_126, 1, x_125); -return x_126; +x_127 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_127, 0, x_125); +lean_ctor_set(x_127, 1, x_126); +return x_127; } } } @@ -815,141 +814,141 @@ return x_126; } else { -uint8_t x_127; +uint8_t x_128; lean_dec(x_33); lean_dec(x_30); lean_dec(x_5); lean_dec(x_3); lean_dec(x_2); lean_dec(x_1); -x_127 = !lean_is_exclusive(x_35); -if (x_127 == 0) +x_128 = !lean_is_exclusive(x_35); +if (x_128 == 0) { return x_35; } else { -lean_object* x_128; lean_object* x_129; lean_object* x_130; -x_128 = lean_ctor_get(x_35, 0); -x_129 = lean_ctor_get(x_35, 1); +lean_object* x_129; lean_object* x_130; lean_object* x_131; +x_129 = lean_ctor_get(x_35, 0); +x_130 = lean_ctor_get(x_35, 1); +lean_inc(x_130); lean_inc(x_129); -lean_inc(x_128); lean_dec(x_35); -x_130 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_130, 0, x_128); -lean_ctor_set(x_130, 1, x_129); -return x_130; +x_131 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_131, 0, x_129); +lean_ctor_set(x_131, 1, x_130); +return x_131; } } } else { -uint8_t x_131; +uint8_t x_132; lean_dec(x_30); lean_dec(x_5); lean_dec(x_3); lean_dec(x_2); lean_dec(x_1); -x_131 = !lean_is_exclusive(x_32); -if (x_131 == 0) +x_132 = !lean_is_exclusive(x_32); +if (x_132 == 0) { return x_32; } else { -lean_object* x_132; lean_object* x_133; lean_object* x_134; -x_132 = lean_ctor_get(x_32, 0); -x_133 = lean_ctor_get(x_32, 1); +lean_object* x_133; lean_object* x_134; lean_object* x_135; +x_133 = lean_ctor_get(x_32, 0); +x_134 = lean_ctor_get(x_32, 1); +lean_inc(x_134); lean_inc(x_133); -lean_inc(x_132); lean_dec(x_32); -x_134 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_134, 0, x_132); -lean_ctor_set(x_134, 1, x_133); -return x_134; +x_135 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_135, 0, x_133); +lean_ctor_set(x_135, 1, x_134); +return x_135; } } } else { -uint8_t x_135; +uint8_t x_136; lean_dec(x_28); lean_dec(x_5); lean_dec(x_3); lean_dec(x_2); lean_dec(x_1); -x_135 = !lean_is_exclusive(x_29); -if (x_135 == 0) +x_136 = !lean_is_exclusive(x_29); +if (x_136 == 0) { return x_29; } else { -lean_object* x_136; lean_object* x_137; lean_object* x_138; -x_136 = lean_ctor_get(x_29, 0); -x_137 = lean_ctor_get(x_29, 1); +lean_object* x_137; lean_object* x_138; lean_object* x_139; +x_137 = lean_ctor_get(x_29, 0); +x_138 = lean_ctor_get(x_29, 1); +lean_inc(x_138); lean_inc(x_137); -lean_inc(x_136); lean_dec(x_29); -x_138 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_138, 0, x_136); -lean_ctor_set(x_138, 1, x_137); -return x_138; +x_139 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_139, 0, x_137); +lean_ctor_set(x_139, 1, x_138); +return x_139; } } } } else { -uint8_t x_139; +uint8_t x_140; lean_dec(x_5); lean_dec(x_3); lean_dec(x_2); lean_dec(x_1); -x_139 = !lean_is_exclusive(x_11); -if (x_139 == 0) +x_140 = !lean_is_exclusive(x_11); +if (x_140 == 0) { return x_11; } else { -lean_object* x_140; lean_object* x_141; lean_object* x_142; -x_140 = lean_ctor_get(x_11, 0); -x_141 = lean_ctor_get(x_11, 1); +lean_object* x_141; lean_object* x_142; lean_object* x_143; +x_141 = lean_ctor_get(x_11, 0); +x_142 = lean_ctor_get(x_11, 1); +lean_inc(x_142); lean_inc(x_141); -lean_inc(x_140); lean_dec(x_11); -x_142 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_142, 0, x_140); -lean_ctor_set(x_142, 1, x_141); -return x_142; +x_143 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_143, 0, x_141); +lean_ctor_set(x_143, 1, x_142); +return x_143; } } } else { -uint8_t x_143; +uint8_t x_144; lean_dec(x_5); lean_dec(x_3); lean_dec(x_2); lean_dec(x_1); -x_143 = !lean_is_exclusive(x_7); -if (x_143 == 0) +x_144 = !lean_is_exclusive(x_7); +if (x_144 == 0) { return x_7; } else { -lean_object* x_144; lean_object* x_145; lean_object* x_146; -x_144 = lean_ctor_get(x_7, 0); -x_145 = lean_ctor_get(x_7, 1); +lean_object* x_145; lean_object* x_146; lean_object* x_147; +x_145 = lean_ctor_get(x_7, 0); +x_146 = lean_ctor_get(x_7, 1); +lean_inc(x_146); lean_inc(x_145); -lean_inc(x_144); lean_dec(x_7); -x_146 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_146, 0, x_144); -lean_ctor_set(x_146, 1, x_145); -return x_146; +x_147 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_147, 0, x_145); +lean_ctor_set(x_147, 1, x_146); +return x_147; } } } diff --git a/stage0/stdlib/Init/Lean/Parser/Term.c b/stage0/stdlib/Init/Lean/Parser/Term.c index de86167d90..fc8d290bf5 100644 --- a/stage0/stdlib/Init/Lean/Parser/Term.c +++ b/stage0/stdlib/Init/Lean/Parser/Term.c @@ -246,6 +246,7 @@ lean_object* l_Lean_Parser_Term_letPatDecl; lean_object* l_Lean_Parser_Term_sortApp___closed__4; lean_object* l_Lean_Parser_Term_bnot___closed__2; lean_object* l_Lean_Parser_Term_typeAscription___elambda__1(lean_object*, lean_object*); +lean_object* l_Lean_Parser_Term_let_x21___elambda__1___closed__4; lean_object* l_Lean_Parser_Term_band___elambda__1___closed__3; lean_object* l_Lean_Parser_Term_explicitBinder___elambda__1___closed__3; lean_object* l_Lean_Parser_Term_and___closed__3; @@ -378,6 +379,7 @@ lean_object* l_Lean_Parser_Term_if___elambda__1___closed__20; lean_object* l_Lean_Parser_Term_seqRight___elambda__1___closed__2; lean_object* l_Lean_Parser_Term_prop___elambda__1___closed__6; lean_object* l_Lean_Parser_Term_match___elambda__1___closed__11; +lean_object* l___regBuiltinParser_Lean_Parser_Term_let_x21(lean_object*); lean_object* l_Lean_Parser_Term_let___elambda__1___closed__7; lean_object* l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_matchAlts___elambda__1___spec__10___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_tacticBlock___elambda__1(lean_object*, lean_object*); @@ -410,6 +412,7 @@ lean_object* l_Lean_Parser_tokenFn(lean_object*, lean_object*); lean_object* l___regBuiltinParser_Lean_Parser_Term_let(lean_object*); lean_object* l_Lean_Parser_Term_doPat___closed__8; lean_object* l_Lean_Parser_Term_id___closed__4; +lean_object* l_Lean_Parser_Term_let_x21___elambda__1___closed__9; lean_object* l_Lean_Parser_Term_show___closed__6; lean_object* l_Lean_Parser_Term_nomatch___elambda__1___closed__9; lean_object* l_Lean_Parser_Term_listLit___closed__4; @@ -454,6 +457,7 @@ lean_object* l_Lean_Parser_Term_forall___elambda__1___closed__13; lean_object* l_Lean_Parser_Term_anonymousCtor___closed__9; lean_object* l_Lean_Parser_Term_sorry___closed__1; lean_object* l_Lean_Parser_Term_structInst___elambda__1___closed__3; +lean_object* l_Lean_Parser_Term_let_x21___closed__6; lean_object* l_Lean_Parser_Term_ge___elambda__1___closed__4; lean_object* l_Lean_Parser_Term_simpleBinder___closed__3; lean_object* l_Lean_Parser_Term_heq___elambda__1___closed__3; @@ -536,6 +540,7 @@ lean_object* l_Lean_Parser_Term_fun___elambda__1___closed__4; lean_object* l_Lean_Parser_Term_equiv___closed__3; lean_object* l_Lean_Parser_Term_sorry___elambda__1___closed__4; lean_object* l_Lean_Parser_Term_suffices___elambda__1___closed__2; +lean_object* l_Lean_Parser_Term_let_x21___closed__5; lean_object* l_Lean_Parser_Term_let___elambda__1___closed__5; lean_object* l_Lean_Parser_tacticParser(lean_object*); lean_object* l_Lean_Parser_Term_quotedName___elambda__1___closed__3; @@ -632,6 +637,7 @@ lean_object* l_Lean_Parser_Term_uminus___closed__3; lean_object* l_Lean_Parser_Term_let___closed__1; lean_object* l_Lean_Parser_Term_namedHole___elambda__1(lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_subtype___elambda__1___closed__4; +lean_object* l_Lean_Parser_Term_let_x21___closed__3; lean_object* l_Lean_Parser_Term_typeAscription; lean_object* l_Lean_Parser_Term_sortApp; lean_object* l_Lean_Parser_Term_simpleBinder___closed__4; @@ -1075,6 +1081,7 @@ lean_object* l_Lean_Parser_sepByFn___at_Lean_Parser_Term_listLit___elambda__1___ lean_object* l_Lean_Parser_Term_leftArrow___elambda__1___closed__4; lean_object* l_Lean_Parser_Term_char___elambda__1(lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_explicitBinder___closed__1; +lean_object* l_Lean_Parser_Term_let_x21___elambda__1___closed__3; lean_object* l_Lean_Parser_Term_dollarProj___closed__1; lean_object* l_Lean_Parser_Term_do; lean_object* l_Lean_Parser_Term_seqRight___closed__3; @@ -1083,6 +1090,7 @@ lean_object* l_Lean_Parser_sepBy1Fn___at_Lean_Parser_Tactic_nonEmptySeq___elambd lean_object* l_Lean_Parser_registerBuiltinParserAttribute(lean_object*, lean_object*, uint8_t, lean_object*); lean_object* l___regBuiltinParser_Lean_Parser_Term_bnot(lean_object*); lean_object* l_Lean_Parser_Term_binderTactic___closed__1; +lean_object* l_Lean_Parser_Term_let_x21; lean_object* l_Lean_Parser_Term_tacticBlock___elambda__1___closed__3; lean_object* l_Lean_Parser_Term_cdot___elambda__1___closed__3; lean_object* l_Lean_Parser_Term_bnot___elambda__1___closed__2; @@ -1105,6 +1113,7 @@ lean_object* l_Lean_Parser_Term_explicitUniv___closed__4; lean_object* l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_matchAlts___elambda__1___spec__12(lean_object*, lean_object*, uint8_t, lean_object*, uint8_t, uint8_t, lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_append___elambda__1___closed__1; lean_object* l_Lean_Parser_Term_proj___closed__2; +lean_object* l_Lean_Parser_Term_let_x21___elambda__1___closed__5; lean_object* l_Lean_FileMap_toPosition(lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_fun___closed__4; lean_object* l_Lean_Parser_Term_tacticStxQuot___elambda__1___closed__3; @@ -1391,6 +1400,7 @@ lean_object* l_Lean_Parser_Term_simpleBinder; lean_object* l_Lean_Parser_Term_bor___elambda__1___closed__3; lean_object* l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_explicitUniv___elambda__1___spec__2(uint8_t, lean_object*, uint8_t, uint8_t, lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_div___elambda__1___closed__3; +lean_object* l_Lean_Parser_Term_let_x21___elambda__1___closed__7; lean_object* l_Lean_Parser_Term_doExpr___elambda__1(lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_let___closed__5; lean_object* l_Lean_Parser_Term_structInstArrayRef___closed__8; @@ -1493,6 +1503,7 @@ lean_object* l_Lean_Parser_Term_hole___elambda__1___closed__2; lean_object* l_Lean_Parser_Term_match__syntax___elambda__1___closed__2; lean_object* l___regBuiltinParser_Lean_Parser_Term_mapConst(lean_object*); lean_object* l_Lean_Parser_Term_inaccessible___closed__5; +lean_object* l_Lean_Parser_Term_let_x21___elambda__1(lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_typeAscription___closed__4; lean_object* l_Lean_Parser_Term_doPat___elambda__1___closed__3; lean_object* l_Lean_Parser_Term_binderType___closed__2; @@ -1632,6 +1643,7 @@ lean_object* l_Lean_Parser_Term_borrowed___elambda__1___closed__1; lean_object* l_Lean_Parser_Term_if___closed__6; lean_object* l_Lean_Parser_Term_letIdDecl___closed__2; lean_object* l_Lean_Parser_Term_char; +lean_object* l_Lean_Parser_Term_let_x21___elambda__1___closed__1; lean_object* l_Lean_Parser_Term_structInstField___closed__5; lean_object* l_Lean_Parser_Term_matchAlts___closed__2; lean_object* l_Lean_Parser_Term_doPat___elambda__1___closed__6; @@ -1795,6 +1807,7 @@ lean_object* l_Lean_Parser_mkAntiquot(lean_object*, lean_object*, uint8_t); lean_object* l_Lean_Parser_Term_funBinder___closed__2; lean_object* l_Lean_Parser_Term_dollarProj___elambda__1___closed__6; lean_object* l_Lean_Parser_Term_tacticBlock___elambda__1___closed__9; +lean_object* l_Lean_Parser_Term_let_x21___elambda__1___closed__6; lean_object* l_Lean_Parser_Term_explicit; lean_object* l_Lean_Parser_Term_match__syntax___elambda__1___closed__7; lean_object* l___regBuiltinParser_Lean_Parser_Term_arrow(lean_object*); @@ -1852,6 +1865,7 @@ lean_object* l_Lean_Parser_Term_ne___elambda__1___closed__4; lean_object* l_Lean_Parser_Term_paren___elambda__1(lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_explicitUniv___closed__11; lean_object* l_Lean_Parser_Term_arrayLit___closed__1; +lean_object* l_Lean_Parser_Term_let_x21___closed__1; lean_object* l_Lean_Parser_Term_nomatch___closed__5; lean_object* l_Lean_Parser_Term_beq___closed__1; lean_object* l_Lean_Parser_Term_fun___closed__2; @@ -1916,6 +1930,7 @@ lean_object* l_Lean_Parser_Term_nomatch___closed__3; lean_object* l_Lean_Parser_Term_orM___elambda__1___closed__3; lean_object* l_Lean_Parser_Term_bindOp___elambda__1___closed__3; lean_object* l_Lean_Parser_Term_add___closed__3; +lean_object* l_Lean_Parser_Term_let_x21___elambda__1___closed__8; lean_object* l_Lean_Parser_Term_structInst; lean_object* l_Lean_Parser_Term_dollarProj___elambda__1___closed__1; lean_object* l_Lean_Parser_Tactic_nonEmptySeq___closed__1; @@ -1927,6 +1942,7 @@ lean_object* l_Lean_Parser_Term_char___elambda__1___closed__2; lean_object* l_Lean_Parser_Term_borrowed___elambda__1___closed__6; lean_object* l___regBuiltinParser_Lean_Parser_Term_borrowed(lean_object*); lean_object* l_Lean_Parser_Term_depArrow___elambda__1___closed__11; +lean_object* l_Lean_Parser_Term_let_x21___elambda__1___closed__2; lean_object* l_Lean_Parser_Term_structInst___elambda__1___closed__4; lean_object* l_Lean_Parser_Term_simpleBinder___elambda__1___closed__2; lean_object* l_Lean_Parser_Term_forall___elambda__1___closed__1; @@ -2031,6 +2047,7 @@ lean_object* l_Lean_Parser_Term_namedHole___closed__1; lean_object* l_Lean_Parser_Term_map; lean_object* l_Lean_Parser_Term_unicodeInfixR(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_tparser_x21___elambda__1___closed__9; +lean_object* l_Lean_Parser_Term_let_x21___closed__2; lean_object* l_Lean_Parser_Term_forall___closed__6; lean_object* l_Lean_Parser_Term_mod___elambda__1___closed__2; lean_object* l_Lean_Parser_Term_modN___closed__1; @@ -2065,6 +2082,7 @@ extern lean_object* l_Lean_Parser_Level_max___closed__2; lean_object* l_Lean_Parser_Term_binderTactic___closed__5; lean_object* l_Lean_Parser_Term_doId___elambda__1___closed__3; lean_object* l_Lean_Parser_sepBy1Fn___at_Lean_Parser_Term_matchAlts___elambda__1___spec__7(lean_object*, lean_object*, uint8_t, uint8_t, lean_object*, lean_object*); +lean_object* l_Lean_Parser_Term_let_x21___closed__4; lean_object* l_Lean_Parser_Term_proj___elambda__1___closed__3; lean_object* l_Lean_Parser_Term_letIdDecl___closed__6; lean_object* l_Lean_Parser_Term_app___closed__4; @@ -34868,6 +34886,578 @@ x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1); return x_6; } } +lean_object* _init_l_Lean_Parser_Term_let_x21___elambda__1___closed__1() { +_start: +{ +lean_object* x_1; +x_1 = lean_mk_string("let!"); +return x_1; +} +} +lean_object* _init_l_Lean_Parser_Term_let_x21___elambda__1___closed__2() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_mkAppStx___closed__6; +x_2 = l_Lean_Parser_Term_let_x21___elambda__1___closed__1; +x_3 = lean_name_mk_string(x_1, x_2); +return x_3; +} +} +lean_object* _init_l_Lean_Parser_Term_let_x21___elambda__1___closed__3() { +_start: +{ +lean_object* x_1; lean_object* x_2; +x_1 = l_Lean_Parser_Term_let_x21___elambda__1___closed__2; +x_2 = lean_alloc_ctor(1, 1, 0); +lean_ctor_set(x_2, 0, x_1); +return x_2; +} +} +lean_object* _init_l_Lean_Parser_Term_let_x21___elambda__1___closed__4() { +_start: +{ +lean_object* x_1; lean_object* x_2; uint8_t x_3; lean_object* x_4; +x_1 = l_Lean_Parser_Term_let_x21___elambda__1___closed__1; +x_2 = l_Lean_Parser_Term_let_x21___elambda__1___closed__3; +x_3 = 1; +x_4 = l_Lean_Parser_mkAntiquot(x_1, x_2, x_3); +return x_4; +} +} +lean_object* _init_l_Lean_Parser_Term_let_x21___elambda__1___closed__5() { +_start: +{ +lean_object* x_1; +x_1 = lean_mk_string("let! "); +return x_1; +} +} +lean_object* _init_l_Lean_Parser_Term_let_x21___elambda__1___closed__6() { +_start: +{ +lean_object* x_1; lean_object* x_2; +x_1 = l_Lean_Parser_Term_let_x21___elambda__1___closed__5; +x_2 = l_String_trim(x_1); +return x_2; +} +} +lean_object* _init_l_Lean_Parser_Term_let_x21___elambda__1___closed__7() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Char_HasRepr___closed__1; +x_2 = l_Lean_Parser_Term_let_x21___elambda__1___closed__6; +x_3 = lean_string_append(x_1, x_2); +return x_3; +} +} +lean_object* _init_l_Lean_Parser_Term_let_x21___elambda__1___closed__8() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Parser_Term_let_x21___elambda__1___closed__7; +x_2 = l_Char_HasRepr___closed__1; +x_3 = lean_string_append(x_1, x_2); +return x_3; +} +} +lean_object* _init_l_Lean_Parser_Term_let_x21___elambda__1___closed__9() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = lean_box(0); +x_2 = l_Lean_Parser_Term_let_x21___elambda__1___closed__8; +x_3 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_3, 0, x_2); +lean_ctor_set(x_3, 1, x_1); +return x_3; +} +} +lean_object* l_Lean_Parser_Term_let_x21___elambda__1(lean_object* x_1, lean_object* x_2) { +_start: +{ +lean_object* x_3; lean_object* x_4; uint8_t x_5; +x_3 = l_Lean_Parser_Term_let_x21___elambda__1___closed__4; +x_4 = lean_ctor_get(x_3, 1); +lean_inc(x_4); +lean_inc(x_2); +lean_inc(x_1); +x_5 = l_Lean_Parser_tryAnti(x_1, x_2); +if (x_5 == 0) +{ +lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_42; lean_object* x_43; lean_object* x_44; +lean_dec(x_4); +x_6 = lean_ctor_get(x_2, 0); +lean_inc(x_6); +x_7 = lean_array_get_size(x_6); +lean_dec(x_6); +x_42 = lean_ctor_get(x_2, 1); +lean_inc(x_42); +lean_inc(x_1); +x_43 = l_Lean_Parser_tokenFn(x_1, x_2); +x_44 = lean_ctor_get(x_43, 3); +lean_inc(x_44); +if (lean_obj_tag(x_44) == 0) +{ +lean_object* x_45; lean_object* x_46; +x_45 = lean_ctor_get(x_43, 0); +lean_inc(x_45); +x_46 = l_Array_back___at_Lean_Parser_checkStackTopFn___spec__1(x_45); +lean_dec(x_45); +if (lean_obj_tag(x_46) == 2) +{ +lean_object* x_47; lean_object* x_48; uint8_t x_49; +x_47 = lean_ctor_get(x_46, 1); +lean_inc(x_47); +lean_dec(x_46); +x_48 = l_Lean_Parser_Term_let_x21___elambda__1___closed__6; +x_49 = lean_string_dec_eq(x_47, x_48); +lean_dec(x_47); +if (x_49 == 0) +{ +lean_object* x_50; lean_object* x_51; +x_50 = l_Lean_Parser_Term_let_x21___elambda__1___closed__9; +x_51 = l_Lean_Parser_ParserState_mkErrorsAt(x_43, x_50, x_42); +x_8 = x_51; +goto block_41; +} +else +{ +lean_dec(x_42); +x_8 = x_43; +goto block_41; +} +} +else +{ +lean_object* x_52; lean_object* x_53; +lean_dec(x_46); +x_52 = l_Lean_Parser_Term_let_x21___elambda__1___closed__9; +x_53 = l_Lean_Parser_ParserState_mkErrorsAt(x_43, x_52, x_42); +x_8 = x_53; +goto block_41; +} +} +else +{ +lean_object* x_54; lean_object* x_55; +lean_dec(x_44); +x_54 = l_Lean_Parser_Term_let_x21___elambda__1___closed__9; +x_55 = l_Lean_Parser_ParserState_mkErrorsAt(x_43, x_54, x_42); +x_8 = x_55; +goto block_41; +} +block_41: +{ +lean_object* x_9; +x_9 = lean_ctor_get(x_8, 3); +lean_inc(x_9); +if (lean_obj_tag(x_9) == 0) +{ +lean_object* x_10; lean_object* x_11; +lean_inc(x_1); +x_10 = l_Lean_Parser_Term_letDecl___elambda__1(x_1, x_8); +x_11 = lean_ctor_get(x_10, 3); +lean_inc(x_11); +if (lean_obj_tag(x_11) == 0) +{ +lean_object* x_12; lean_object* x_13; lean_object* x_14; +x_12 = lean_ctor_get(x_10, 1); +lean_inc(x_12); +lean_inc(x_1); +x_13 = l_Lean_Parser_tokenFn(x_1, x_10); +x_14 = lean_ctor_get(x_13, 3); +lean_inc(x_14); +if (lean_obj_tag(x_14) == 0) +{ +lean_object* x_15; lean_object* x_16; +x_15 = lean_ctor_get(x_13, 0); +lean_inc(x_15); +x_16 = l_Array_back___at_Lean_Parser_checkStackTopFn___spec__1(x_15); +lean_dec(x_15); +if (lean_obj_tag(x_16) == 2) +{ +lean_object* x_17; lean_object* x_18; uint8_t x_19; +x_17 = lean_ctor_get(x_16, 1); +lean_inc(x_17); +lean_dec(x_16); +x_18 = l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Tactic_seq___elambda__1___spec__2___closed__1; +x_19 = lean_string_dec_eq(x_17, x_18); +lean_dec(x_17); +if (x_19 == 0) +{ +lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; +lean_dec(x_1); +x_20 = l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Tactic_seq___elambda__1___spec__2___closed__4; +x_21 = l_Lean_Parser_ParserState_mkErrorsAt(x_13, x_20, x_12); +x_22 = l_Lean_Parser_Term_let_x21___elambda__1___closed__2; +x_23 = l_Lean_Parser_ParserState_mkNode(x_21, x_22, x_7); +return x_23; +} +else +{ +lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; +lean_dec(x_12); +x_24 = l_Lean_Parser_termParser___closed__2; +x_25 = lean_unsigned_to_nat(0u); +x_26 = l_Lean_Parser_categoryParser___elambda__1(x_24, x_25, x_1, x_13); +x_27 = l_Lean_Parser_Term_let_x21___elambda__1___closed__2; +x_28 = l_Lean_Parser_ParserState_mkNode(x_26, x_27, x_7); +return x_28; +} +} +else +{ +lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; +lean_dec(x_16); +lean_dec(x_1); +x_29 = l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Tactic_seq___elambda__1___spec__2___closed__4; +x_30 = l_Lean_Parser_ParserState_mkErrorsAt(x_13, x_29, x_12); +x_31 = l_Lean_Parser_Term_let_x21___elambda__1___closed__2; +x_32 = l_Lean_Parser_ParserState_mkNode(x_30, x_31, x_7); +return x_32; +} +} +else +{ +lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36; +lean_dec(x_14); +lean_dec(x_1); +x_33 = l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Tactic_seq___elambda__1___spec__2___closed__4; +x_34 = l_Lean_Parser_ParserState_mkErrorsAt(x_13, x_33, x_12); +x_35 = l_Lean_Parser_Term_let_x21___elambda__1___closed__2; +x_36 = l_Lean_Parser_ParserState_mkNode(x_34, x_35, x_7); +return x_36; +} +} +else +{ +lean_object* x_37; lean_object* x_38; +lean_dec(x_11); +lean_dec(x_1); +x_37 = l_Lean_Parser_Term_let_x21___elambda__1___closed__2; +x_38 = l_Lean_Parser_ParserState_mkNode(x_10, x_37, x_7); +return x_38; +} +} +else +{ +lean_object* x_39; lean_object* x_40; +lean_dec(x_9); +lean_dec(x_1); +x_39 = l_Lean_Parser_Term_let_x21___elambda__1___closed__2; +x_40 = l_Lean_Parser_ParserState_mkNode(x_8, x_39, x_7); +return x_40; +} +} +} +else +{ +lean_object* x_56; lean_object* x_57; lean_object* x_58; lean_object* x_59; lean_object* x_60; +x_56 = lean_ctor_get(x_2, 0); +lean_inc(x_56); +x_57 = lean_array_get_size(x_56); +lean_dec(x_56); +x_58 = lean_ctor_get(x_2, 1); +lean_inc(x_58); +lean_inc(x_1); +x_59 = lean_apply_2(x_4, x_1, x_2); +x_60 = lean_ctor_get(x_59, 3); +lean_inc(x_60); +if (lean_obj_tag(x_60) == 0) +{ +lean_dec(x_58); +lean_dec(x_57); +lean_dec(x_1); +return x_59; +} +else +{ +lean_object* x_61; lean_object* x_62; uint8_t x_63; +x_61 = lean_ctor_get(x_60, 0); +lean_inc(x_61); +lean_dec(x_60); +x_62 = lean_ctor_get(x_59, 1); +lean_inc(x_62); +x_63 = lean_nat_dec_eq(x_62, x_58); +lean_dec(x_62); +if (x_63 == 0) +{ +lean_dec(x_61); +lean_dec(x_58); +lean_dec(x_57); +lean_dec(x_1); +return x_59; +} +else +{ +lean_object* x_64; lean_object* x_65; lean_object* x_66; lean_object* x_67; lean_object* x_107; lean_object* x_108; +lean_inc(x_58); +x_64 = l_Lean_Parser_ParserState_restore(x_59, x_57, x_58); +lean_dec(x_57); +x_65 = lean_ctor_get(x_64, 0); +lean_inc(x_65); +x_66 = lean_array_get_size(x_65); +lean_dec(x_65); +lean_inc(x_1); +x_107 = l_Lean_Parser_tokenFn(x_1, x_64); +x_108 = lean_ctor_get(x_107, 3); +lean_inc(x_108); +if (lean_obj_tag(x_108) == 0) +{ +lean_object* x_109; lean_object* x_110; +x_109 = lean_ctor_get(x_107, 0); +lean_inc(x_109); +x_110 = l_Array_back___at_Lean_Parser_checkStackTopFn___spec__1(x_109); +lean_dec(x_109); +if (lean_obj_tag(x_110) == 2) +{ +lean_object* x_111; lean_object* x_112; uint8_t x_113; +x_111 = lean_ctor_get(x_110, 1); +lean_inc(x_111); +lean_dec(x_110); +x_112 = l_Lean_Parser_Term_let_x21___elambda__1___closed__6; +x_113 = lean_string_dec_eq(x_111, x_112); +lean_dec(x_111); +if (x_113 == 0) +{ +lean_object* x_114; lean_object* x_115; +x_114 = l_Lean_Parser_Term_let_x21___elambda__1___closed__9; +lean_inc(x_58); +x_115 = l_Lean_Parser_ParserState_mkErrorsAt(x_107, x_114, x_58); +x_67 = x_115; +goto block_106; +} +else +{ +x_67 = x_107; +goto block_106; +} +} +else +{ +lean_object* x_116; lean_object* x_117; +lean_dec(x_110); +x_116 = l_Lean_Parser_Term_let_x21___elambda__1___closed__9; +lean_inc(x_58); +x_117 = l_Lean_Parser_ParserState_mkErrorsAt(x_107, x_116, x_58); +x_67 = x_117; +goto block_106; +} +} +else +{ +lean_object* x_118; lean_object* x_119; +lean_dec(x_108); +x_118 = l_Lean_Parser_Term_let_x21___elambda__1___closed__9; +lean_inc(x_58); +x_119 = l_Lean_Parser_ParserState_mkErrorsAt(x_107, x_118, x_58); +x_67 = x_119; +goto block_106; +} +block_106: +{ +lean_object* x_68; +x_68 = lean_ctor_get(x_67, 3); +lean_inc(x_68); +if (lean_obj_tag(x_68) == 0) +{ +lean_object* x_69; lean_object* x_70; +lean_inc(x_1); +x_69 = l_Lean_Parser_Term_letDecl___elambda__1(x_1, x_67); +x_70 = lean_ctor_get(x_69, 3); +lean_inc(x_70); +if (lean_obj_tag(x_70) == 0) +{ +lean_object* x_71; lean_object* x_72; lean_object* x_73; +x_71 = lean_ctor_get(x_69, 1); +lean_inc(x_71); +lean_inc(x_1); +x_72 = l_Lean_Parser_tokenFn(x_1, x_69); +x_73 = lean_ctor_get(x_72, 3); +lean_inc(x_73); +if (lean_obj_tag(x_73) == 0) +{ +lean_object* x_74; lean_object* x_75; +x_74 = lean_ctor_get(x_72, 0); +lean_inc(x_74); +x_75 = l_Array_back___at_Lean_Parser_checkStackTopFn___spec__1(x_74); +lean_dec(x_74); +if (lean_obj_tag(x_75) == 2) +{ +lean_object* x_76; lean_object* x_77; uint8_t x_78; +x_76 = lean_ctor_get(x_75, 1); +lean_inc(x_76); +lean_dec(x_75); +x_77 = l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Tactic_seq___elambda__1___spec__2___closed__1; +x_78 = lean_string_dec_eq(x_76, x_77); +lean_dec(x_76); +if (x_78 == 0) +{ +lean_object* x_79; lean_object* x_80; lean_object* x_81; lean_object* x_82; lean_object* x_83; +lean_dec(x_1); +x_79 = l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Tactic_seq___elambda__1___spec__2___closed__4; +x_80 = l_Lean_Parser_ParserState_mkErrorsAt(x_72, x_79, x_71); +x_81 = l_Lean_Parser_Term_let_x21___elambda__1___closed__2; +x_82 = l_Lean_Parser_ParserState_mkNode(x_80, x_81, x_66); +x_83 = l_Lean_Parser_mergeOrElseErrors(x_82, x_61, x_58); +lean_dec(x_58); +return x_83; +} +else +{ +lean_object* x_84; lean_object* x_85; lean_object* x_86; lean_object* x_87; lean_object* x_88; lean_object* x_89; +lean_dec(x_71); +x_84 = l_Lean_Parser_termParser___closed__2; +x_85 = lean_unsigned_to_nat(0u); +x_86 = l_Lean_Parser_categoryParser___elambda__1(x_84, x_85, x_1, x_72); +x_87 = l_Lean_Parser_Term_let_x21___elambda__1___closed__2; +x_88 = l_Lean_Parser_ParserState_mkNode(x_86, x_87, x_66); +x_89 = l_Lean_Parser_mergeOrElseErrors(x_88, x_61, x_58); +lean_dec(x_58); +return x_89; +} +} +else +{ +lean_object* x_90; lean_object* x_91; lean_object* x_92; lean_object* x_93; lean_object* x_94; +lean_dec(x_75); +lean_dec(x_1); +x_90 = l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Tactic_seq___elambda__1___spec__2___closed__4; +x_91 = l_Lean_Parser_ParserState_mkErrorsAt(x_72, x_90, x_71); +x_92 = l_Lean_Parser_Term_let_x21___elambda__1___closed__2; +x_93 = l_Lean_Parser_ParserState_mkNode(x_91, x_92, x_66); +x_94 = l_Lean_Parser_mergeOrElseErrors(x_93, x_61, x_58); +lean_dec(x_58); +return x_94; +} +} +else +{ +lean_object* x_95; lean_object* x_96; lean_object* x_97; lean_object* x_98; lean_object* x_99; +lean_dec(x_73); +lean_dec(x_1); +x_95 = l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Tactic_seq___elambda__1___spec__2___closed__4; +x_96 = l_Lean_Parser_ParserState_mkErrorsAt(x_72, x_95, x_71); +x_97 = l_Lean_Parser_Term_let_x21___elambda__1___closed__2; +x_98 = l_Lean_Parser_ParserState_mkNode(x_96, x_97, x_66); +x_99 = l_Lean_Parser_mergeOrElseErrors(x_98, x_61, x_58); +lean_dec(x_58); +return x_99; +} +} +else +{ +lean_object* x_100; lean_object* x_101; lean_object* x_102; +lean_dec(x_70); +lean_dec(x_1); +x_100 = l_Lean_Parser_Term_let_x21___elambda__1___closed__2; +x_101 = l_Lean_Parser_ParserState_mkNode(x_69, x_100, x_66); +x_102 = l_Lean_Parser_mergeOrElseErrors(x_101, x_61, x_58); +lean_dec(x_58); +return x_102; +} +} +else +{ +lean_object* x_103; lean_object* x_104; lean_object* x_105; +lean_dec(x_68); +lean_dec(x_1); +x_103 = l_Lean_Parser_Term_let_x21___elambda__1___closed__2; +x_104 = l_Lean_Parser_ParserState_mkNode(x_67, x_103, x_66); +x_105 = l_Lean_Parser_mergeOrElseErrors(x_104, x_61, x_58); +lean_dec(x_58); +return x_105; +} +} +} +} +} +} +} +lean_object* _init_l_Lean_Parser_Term_let_x21___closed__1() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Parser_Term_let_x21___elambda__1___closed__6; +x_2 = l_Lean_Parser_Term_if___closed__1; +x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); +return x_3; +} +} +lean_object* _init_l_Lean_Parser_Term_let_x21___closed__2() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Parser_Term_let_x21___closed__1; +x_2 = l_Lean_Parser_Term_let___closed__3; +x_3 = l_Lean_Parser_andthenInfo(x_1, x_2); +return x_3; +} +} +lean_object* _init_l_Lean_Parser_Term_let_x21___closed__3() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Parser_Term_let_x21___elambda__1___closed__2; +x_2 = l_Lean_Parser_Term_let_x21___closed__2; +x_3 = l_Lean_Parser_nodeInfo(x_1, x_2); +return x_3; +} +} +lean_object* _init_l_Lean_Parser_Term_let_x21___closed__4() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; +x_1 = l_Lean_Parser_Term_let_x21___elambda__1___closed__4; +x_2 = lean_ctor_get(x_1, 0); +lean_inc(x_2); +x_3 = l_Lean_Parser_Term_let_x21___closed__3; +x_4 = l_Lean_Parser_orelseInfo(x_2, x_3); +return x_4; +} +} +lean_object* _init_l_Lean_Parser_Term_let_x21___closed__5() { +_start: +{ +lean_object* x_1; +x_1 = lean_alloc_closure((void*)(l_Lean_Parser_Term_let_x21___elambda__1), 2, 0); +return x_1; +} +} +lean_object* _init_l_Lean_Parser_Term_let_x21___closed__6() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Parser_Term_let_x21___closed__4; +x_2 = l_Lean_Parser_Term_let_x21___closed__5; +x_3 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_3, 0, x_1); +lean_ctor_set(x_3, 1, x_2); +return x_3; +} +} +lean_object* _init_l_Lean_Parser_Term_let_x21() { +_start: +{ +lean_object* x_1; +x_1 = l_Lean_Parser_Term_let_x21___closed__6; +return x_1; +} +} +lean_object* l___regBuiltinParser_Lean_Parser_Term_let_x21(lean_object* x_1) { +_start: +{ +lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; +x_2 = l_Lean_Parser_termParser___closed__2; +x_3 = l_Lean_Parser_Term_let_x21___elambda__1___closed__2; +x_4 = 1; +x_5 = l_Lean_Parser_Term_let_x21; +x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1); +return x_6; +} +} lean_object* _init_l_Lean_Parser_Term_leftArrow___elambda__1___closed__1() { _start: { @@ -51088,6 +51678,41 @@ lean_mark_persistent(l_Lean_Parser_Term_let); res = l___regBuiltinParser_Lean_Parser_Term_let(lean_io_mk_world()); if (lean_io_result_is_error(res)) return res; lean_dec_ref(res); +l_Lean_Parser_Term_let_x21___elambda__1___closed__1 = _init_l_Lean_Parser_Term_let_x21___elambda__1___closed__1(); +lean_mark_persistent(l_Lean_Parser_Term_let_x21___elambda__1___closed__1); +l_Lean_Parser_Term_let_x21___elambda__1___closed__2 = _init_l_Lean_Parser_Term_let_x21___elambda__1___closed__2(); +lean_mark_persistent(l_Lean_Parser_Term_let_x21___elambda__1___closed__2); +l_Lean_Parser_Term_let_x21___elambda__1___closed__3 = _init_l_Lean_Parser_Term_let_x21___elambda__1___closed__3(); +lean_mark_persistent(l_Lean_Parser_Term_let_x21___elambda__1___closed__3); +l_Lean_Parser_Term_let_x21___elambda__1___closed__4 = _init_l_Lean_Parser_Term_let_x21___elambda__1___closed__4(); +lean_mark_persistent(l_Lean_Parser_Term_let_x21___elambda__1___closed__4); +l_Lean_Parser_Term_let_x21___elambda__1___closed__5 = _init_l_Lean_Parser_Term_let_x21___elambda__1___closed__5(); +lean_mark_persistent(l_Lean_Parser_Term_let_x21___elambda__1___closed__5); +l_Lean_Parser_Term_let_x21___elambda__1___closed__6 = _init_l_Lean_Parser_Term_let_x21___elambda__1___closed__6(); +lean_mark_persistent(l_Lean_Parser_Term_let_x21___elambda__1___closed__6); +l_Lean_Parser_Term_let_x21___elambda__1___closed__7 = _init_l_Lean_Parser_Term_let_x21___elambda__1___closed__7(); +lean_mark_persistent(l_Lean_Parser_Term_let_x21___elambda__1___closed__7); +l_Lean_Parser_Term_let_x21___elambda__1___closed__8 = _init_l_Lean_Parser_Term_let_x21___elambda__1___closed__8(); +lean_mark_persistent(l_Lean_Parser_Term_let_x21___elambda__1___closed__8); +l_Lean_Parser_Term_let_x21___elambda__1___closed__9 = _init_l_Lean_Parser_Term_let_x21___elambda__1___closed__9(); +lean_mark_persistent(l_Lean_Parser_Term_let_x21___elambda__1___closed__9); +l_Lean_Parser_Term_let_x21___closed__1 = _init_l_Lean_Parser_Term_let_x21___closed__1(); +lean_mark_persistent(l_Lean_Parser_Term_let_x21___closed__1); +l_Lean_Parser_Term_let_x21___closed__2 = _init_l_Lean_Parser_Term_let_x21___closed__2(); +lean_mark_persistent(l_Lean_Parser_Term_let_x21___closed__2); +l_Lean_Parser_Term_let_x21___closed__3 = _init_l_Lean_Parser_Term_let_x21___closed__3(); +lean_mark_persistent(l_Lean_Parser_Term_let_x21___closed__3); +l_Lean_Parser_Term_let_x21___closed__4 = _init_l_Lean_Parser_Term_let_x21___closed__4(); +lean_mark_persistent(l_Lean_Parser_Term_let_x21___closed__4); +l_Lean_Parser_Term_let_x21___closed__5 = _init_l_Lean_Parser_Term_let_x21___closed__5(); +lean_mark_persistent(l_Lean_Parser_Term_let_x21___closed__5); +l_Lean_Parser_Term_let_x21___closed__6 = _init_l_Lean_Parser_Term_let_x21___closed__6(); +lean_mark_persistent(l_Lean_Parser_Term_let_x21___closed__6); +l_Lean_Parser_Term_let_x21 = _init_l_Lean_Parser_Term_let_x21(); +lean_mark_persistent(l_Lean_Parser_Term_let_x21); +res = l___regBuiltinParser_Lean_Parser_Term_let_x21(lean_io_mk_world()); +if (lean_io_result_is_error(res)) return res; +lean_dec_ref(res); l_Lean_Parser_Term_leftArrow___elambda__1___closed__1 = _init_l_Lean_Parser_Term_leftArrow___elambda__1___closed__1(); lean_mark_persistent(l_Lean_Parser_Term_leftArrow___elambda__1___closed__1); l_Lean_Parser_Term_leftArrow___elambda__1___closed__2 = _init_l_Lean_Parser_Term_leftArrow___elambda__1___closed__2();