From 11c3ada877c7e42c844602feebb99910ce9eb565 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Tue, 7 Apr 2020 17:26:14 +0200 Subject: [PATCH] feat: add [parenthesizer] attribute --- src/Init/Lean/PrettyPrinter.lean | 37 ++ stage0/stdlib/CMakeLists.txt | 2 +- stage0/stdlib/Init/Lean.c | 6 +- stage0/stdlib/Init/Lean/PrettyPrinter.c | 470 ++++++++++++++++++++++++ 4 files changed, 513 insertions(+), 2 deletions(-) create mode 100644 src/Init/Lean/PrettyPrinter.lean create mode 100644 stage0/stdlib/Init/Lean/PrettyPrinter.c diff --git a/src/Init/Lean/PrettyPrinter.lean b/src/Init/Lean/PrettyPrinter.lean new file mode 100644 index 0000000000..4a4a054403 --- /dev/null +++ b/src/Init/Lean/PrettyPrinter.lean @@ -0,0 +1,37 @@ +/- +Copyright (c) 2020 Sebastian Ullrich. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Sebastian Ullrich +-/ + +prelude +import Init.Lean.Parser +import Init.Lean.Elab.Command +import Init.Lean.Delaborator + +namespace Lean + +namespace PrettyPrinter + +constant Parenthesizer : Type := Unit -- TODO + +unsafe def mkParenthesizerAttribute : IO (KeyedDeclsAttribute Parenthesizer) := +KeyedDeclsAttribute.init { + builtinName := `builtinParenthesizer, + name := `parenthesizer, + descr := "Register a parenthesizer. + +[parenthesizer kind] registers a declaration of type `Lean.PrettyPrinter.Parenthesizer` for the `SyntaxNodeKind` +`kind`.", + valueTypeName := `Lean.PrettyPrinter.Parenthesizer, + evalKey := fun env args => match attrParamSyntaxToIdentifier args with + | some id => match env.find? id with + | some _ => pure id + | none => throw ("invalid [parenthesizer] argument, unknown identifier '" ++ toString id ++ "'") + | none => throw "invalid [parenthesizer] argument, expected identifier" +} `Lean.PrettyPrinter.parenthesizerAttribute +@[init mkParenthesizerAttribute] constant parenthesizerAttribute : KeyedDeclsAttribute Parenthesizer := arbitrary _ + +end PrettyPrinter + +end Lean diff --git a/stage0/stdlib/CMakeLists.txt b/stage0/stdlib/CMakeLists.txt index 2fe9718e2c..b47d1e53cd 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/Float.c Init/./Data/FloatArray.c Init/./Data/FloatArray/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/String/Extra.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/Delaborator.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/KeyedDeclsAttribute.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/GeneralizeTelescope.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/Closure.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/FoldConsts.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/Recognizers.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/Float.c Init/./Data/FloatArray.c Init/./Data/FloatArray/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/String/Extra.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/Delaborator.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/KeyedDeclsAttribute.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/GeneralizeTelescope.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/PrettyPrinter.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/Closure.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/FoldConsts.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/Recognizers.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.c b/stage0/stdlib/Init/Lean.c index 6beaa62d7d..1b0cf29be4 100644 --- a/stage0/stdlib/Init/Lean.c +++ b/stage0/stdlib/Init/Lean.c @@ -1,6 +1,6 @@ // Lean compiler output // Module: Init.Lean -// Imports: Init.Lean.Compiler Init.Lean.Environment Init.Lean.Modifiers Init.Lean.ProjFns Init.Lean.Runtime Init.Lean.Attributes Init.Lean.Parser Init.Lean.ReducibilityAttrs Init.Lean.Elab Init.Lean.EqnCompiler Init.Lean.Class Init.Lean.LocalContext Init.Lean.MetavarContext Init.Lean.AuxRecursor Init.Lean.Linter Init.Lean.Meta Init.Lean.Util Init.Lean.Eval Init.Lean.Structure Init.Lean.Delaborator +// Imports: Init.Lean.Compiler Init.Lean.Environment Init.Lean.Modifiers Init.Lean.ProjFns Init.Lean.Runtime Init.Lean.Attributes Init.Lean.Parser Init.Lean.ReducibilityAttrs Init.Lean.Elab Init.Lean.EqnCompiler Init.Lean.Class Init.Lean.LocalContext Init.Lean.MetavarContext Init.Lean.AuxRecursor Init.Lean.Linter Init.Lean.Meta Init.Lean.Util Init.Lean.Eval Init.Lean.Structure Init.Lean.Delaborator Init.Lean.PrettyPrinter #include "runtime/lean.h" #if defined(__clang__) #pragma clang diagnostic ignored "-Wunused-parameter" @@ -33,6 +33,7 @@ lean_object* initialize_Init_Lean_Util(lean_object*); lean_object* initialize_Init_Lean_Eval(lean_object*); lean_object* initialize_Init_Lean_Structure(lean_object*); lean_object* initialize_Init_Lean_Delaborator(lean_object*); +lean_object* initialize_Init_Lean_PrettyPrinter(lean_object*); static bool _G_initialized = false; lean_object* initialize_Init_Lean(lean_object* w) { lean_object * res; @@ -98,6 +99,9 @@ lean_dec_ref(res); res = initialize_Init_Lean_Delaborator(lean_io_mk_world()); if (lean_io_result_is_error(res)) return res; lean_dec_ref(res); +res = initialize_Init_Lean_PrettyPrinter(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/PrettyPrinter.c b/stage0/stdlib/Init/Lean/PrettyPrinter.c new file mode 100644 index 0000000000..1c6c6f477d --- /dev/null +++ b/stage0/stdlib/Init/Lean/PrettyPrinter.c @@ -0,0 +1,470 @@ +// Lean compiler output +// Module: Init.Lean.PrettyPrinter +// Imports: Init.Lean.Parser Init.Lean.Elab.Command Init.Lean.Delaborator +#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 +extern lean_object* l_Lean_Name_toString___closed__1; +extern lean_object* l_Lean_Meta_SynthInstance_inferTCGoalsLRAttr___closed__1; +lean_object* l_Lean_PrettyPrinter_parenthesizerAttribute___closed__1; +lean_object* l_Lean_PrettyPrinter_mkParenthesizerAttribute___closed__10; +extern lean_object* l_Array_empty___closed__1; +lean_object* lean_environment_find(lean_object*, lean_object*); +lean_object* l_Lean_PrettyPrinter_mkParenthesizerAttribute___closed__7; +lean_object* l_Lean_PrettyPrinter_parenthesizerAttribute___closed__4; +lean_object* l_Lean_SMap_empty___at_Lean_PrettyPrinter_parenthesizerAttribute___spec__1; +lean_object* lean_string_append(lean_object*, lean_object*); +extern lean_object* l_Lean_LocalContext_Inhabited___closed__1; +lean_object* l_Lean_PrettyPrinter_mkParenthesizerAttribute___closed__11; +lean_object* l_Lean_PrettyPrinter_mkParenthesizerAttribute___lambda__1___boxed(lean_object*, lean_object*); +lean_object* l_Lean_PrettyPrinter_mkParenthesizerAttribute___lambda__1___closed__1; +extern lean_object* l_Lean_PersistentEnvExtension_inhabited___rarg___closed__1; +lean_object* l_Lean_PrettyPrinter_parenthesizerAttribute; +lean_object* l_Lean_PrettyPrinter_parenthesizerAttribute___closed__3; +lean_object* l_Lean_PrettyPrinter_mkParenthesizerAttribute___lambda__1___closed__2; +extern lean_object* l_Lean_EnvExtension_Inhabited___rarg___closed__1; +lean_object* l_Lean_PrettyPrinter_parenthesizerAttribute___closed__2; +lean_object* l_Lean_PrettyPrinter_mkParenthesizerAttribute___closed__12; +extern lean_object* l_Char_HasRepr___closed__1; +lean_object* lean_name_mk_string(lean_object*, lean_object*); +lean_object* l_Lean_attrParamSyntaxToIdentifier(lean_object*); +lean_object* l_Lean_SMap_empty___at_Lean_PrettyPrinter_parenthesizerAttribute___spec__1___closed__2; +lean_object* l_Lean_PrettyPrinter_mkParenthesizerAttribute___closed__13; +lean_object* l_Lean_PrettyPrinter_mkParenthesizerAttribute___lambda__1___closed__3; +lean_object* l_mkHashMapImp___rarg(lean_object*); +lean_object* l_Lean_PrettyPrinter_mkParenthesizerAttribute___lambda__1(lean_object*, lean_object*); +lean_object* l_Lean_PrettyPrinter_parenthesizerAttribute___closed__5; +extern lean_object* l_Lean_PersistentEnvExtension_inhabited___rarg___closed__3; +lean_object* l_Lean_PrettyPrinter_mkParenthesizerAttribute___closed__2; +lean_object* l_Lean_PrettyPrinter_mkParenthesizerAttribute(lean_object*); +lean_object* l_Lean_PrettyPrinter_mkParenthesizerAttribute___closed__1; +lean_object* l_PersistentHashMap_empty___at_Lean_PrettyPrinter_parenthesizerAttribute___spec__3; +lean_object* l_Lean_PrettyPrinter_mkParenthesizerAttribute___closed__8; +lean_object* l_Lean_PrettyPrinter_mkParenthesizerAttribute___closed__4; +lean_object* l_Lean_SMap_empty___at_Lean_PrettyPrinter_parenthesizerAttribute___spec__1___closed__1; +lean_object* l_Lean_PrettyPrinter_mkParenthesizerAttribute___closed__9; +lean_object* l_mkHashMap___at_Lean_PrettyPrinter_parenthesizerAttribute___spec__2(lean_object*); +lean_object* l_Lean_PrettyPrinter_mkParenthesizerAttribute___closed__3; +lean_object* l_Lean_PrettyPrinter_mkParenthesizerAttribute___closed__5; +lean_object* l_Lean_Name_toStringWithSep___main(lean_object*, lean_object*); +lean_object* l_Lean_KeyedDeclsAttribute_init___rarg(lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_PrettyPrinter_mkParenthesizerAttribute___closed__6; +extern lean_object* l_Lean_mkAppStx___closed__2; +extern lean_object* l_Lean_PersistentEnvExtension_inhabited___rarg___closed__4; +lean_object* _init_l_Lean_PrettyPrinter_mkParenthesizerAttribute___lambda__1___closed__1() { +_start: +{ +lean_object* x_1; +x_1 = lean_mk_string("invalid [parenthesizer] argument, expected identifier"); +return x_1; +} +} +lean_object* _init_l_Lean_PrettyPrinter_mkParenthesizerAttribute___lambda__1___closed__2() { +_start: +{ +lean_object* x_1; lean_object* x_2; +x_1 = l_Lean_PrettyPrinter_mkParenthesizerAttribute___lambda__1___closed__1; +x_2 = lean_alloc_ctor(0, 1, 0); +lean_ctor_set(x_2, 0, x_1); +return x_2; +} +} +lean_object* _init_l_Lean_PrettyPrinter_mkParenthesizerAttribute___lambda__1___closed__3() { +_start: +{ +lean_object* x_1; +x_1 = lean_mk_string("invalid [parenthesizer] argument, unknown identifier '"); +return x_1; +} +} +lean_object* l_Lean_PrettyPrinter_mkParenthesizerAttribute___lambda__1(lean_object* x_1, lean_object* x_2) { +_start: +{ +lean_object* x_3; +x_3 = l_Lean_attrParamSyntaxToIdentifier(x_2); +if (lean_obj_tag(x_3) == 0) +{ +lean_object* x_4; +lean_dec(x_1); +x_4 = l_Lean_PrettyPrinter_mkParenthesizerAttribute___lambda__1___closed__2; +return x_4; +} +else +{ +lean_object* x_5; lean_object* x_6; +x_5 = lean_ctor_get(x_3, 0); +lean_inc(x_5); +lean_dec(x_3); +lean_inc(x_5); +x_6 = lean_environment_find(x_1, x_5); +if (lean_obj_tag(x_6) == 0) +{ +lean_object* x_7; 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_7 = l_Lean_Name_toString___closed__1; +x_8 = l_Lean_Name_toStringWithSep___main(x_7, x_5); +x_9 = l_Lean_PrettyPrinter_mkParenthesizerAttribute___lambda__1___closed__3; +x_10 = lean_string_append(x_9, x_8); +lean_dec(x_8); +x_11 = l_Char_HasRepr___closed__1; +x_12 = lean_string_append(x_10, x_11); +x_13 = lean_alloc_ctor(0, 1, 0); +lean_ctor_set(x_13, 0, x_12); +return x_13; +} +else +{ +lean_object* x_14; +lean_dec(x_6); +x_14 = lean_alloc_ctor(1, 1, 0); +lean_ctor_set(x_14, 0, x_5); +return x_14; +} +} +} +} +lean_object* _init_l_Lean_PrettyPrinter_mkParenthesizerAttribute___closed__1() { +_start: +{ +lean_object* x_1; +x_1 = lean_mk_string("builtinParenthesizer"); +return x_1; +} +} +lean_object* _init_l_Lean_PrettyPrinter_mkParenthesizerAttribute___closed__2() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = lean_box(0); +x_2 = l_Lean_PrettyPrinter_mkParenthesizerAttribute___closed__1; +x_3 = lean_name_mk_string(x_1, x_2); +return x_3; +} +} +lean_object* _init_l_Lean_PrettyPrinter_mkParenthesizerAttribute___closed__3() { +_start: +{ +lean_object* x_1; +x_1 = lean_mk_string("parenthesizer"); +return x_1; +} +} +lean_object* _init_l_Lean_PrettyPrinter_mkParenthesizerAttribute___closed__4() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = lean_box(0); +x_2 = l_Lean_PrettyPrinter_mkParenthesizerAttribute___closed__3; +x_3 = lean_name_mk_string(x_1, x_2); +return x_3; +} +} +lean_object* _init_l_Lean_PrettyPrinter_mkParenthesizerAttribute___closed__5() { +_start: +{ +lean_object* x_1; +x_1 = lean_mk_string("PrettyPrinter"); +return x_1; +} +} +lean_object* _init_l_Lean_PrettyPrinter_mkParenthesizerAttribute___closed__6() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_mkAppStx___closed__2; +x_2 = l_Lean_PrettyPrinter_mkParenthesizerAttribute___closed__5; +x_3 = lean_name_mk_string(x_1, x_2); +return x_3; +} +} +lean_object* _init_l_Lean_PrettyPrinter_mkParenthesizerAttribute___closed__7() { +_start: +{ +lean_object* x_1; +x_1 = lean_mk_string("Parenthesizer"); +return x_1; +} +} +lean_object* _init_l_Lean_PrettyPrinter_mkParenthesizerAttribute___closed__8() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_PrettyPrinter_mkParenthesizerAttribute___closed__6; +x_2 = l_Lean_PrettyPrinter_mkParenthesizerAttribute___closed__7; +x_3 = lean_name_mk_string(x_1, x_2); +return x_3; +} +} +lean_object* _init_l_Lean_PrettyPrinter_mkParenthesizerAttribute___closed__9() { +_start: +{ +lean_object* x_1; +x_1 = lean_mk_string("Register a parenthesizer.\n\n[parenthesizer kind] registers a declaration of type `Lean.PrettyPrinter.Parenthesizer` for the `SyntaxNodeKind`\n`kind`."); +return x_1; +} +} +lean_object* _init_l_Lean_PrettyPrinter_mkParenthesizerAttribute___closed__10() { +_start: +{ +lean_object* x_1; +x_1 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_mkParenthesizerAttribute___lambda__1___boxed), 2, 0); +return x_1; +} +} +lean_object* _init_l_Lean_PrettyPrinter_mkParenthesizerAttribute___closed__11() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; +x_1 = l_Lean_PrettyPrinter_mkParenthesizerAttribute___closed__2; +x_2 = l_Lean_PrettyPrinter_mkParenthesizerAttribute___closed__4; +x_3 = l_Lean_PrettyPrinter_mkParenthesizerAttribute___closed__9; +x_4 = l_Lean_PrettyPrinter_mkParenthesizerAttribute___closed__8; +x_5 = l_Lean_PrettyPrinter_mkParenthesizerAttribute___closed__10; +x_6 = lean_alloc_ctor(0, 5, 0); +lean_ctor_set(x_6, 0, x_1); +lean_ctor_set(x_6, 1, x_2); +lean_ctor_set(x_6, 2, x_3); +lean_ctor_set(x_6, 3, x_4); +lean_ctor_set(x_6, 4, x_5); +return x_6; +} +} +lean_object* _init_l_Lean_PrettyPrinter_mkParenthesizerAttribute___closed__12() { +_start: +{ +lean_object* x_1; +x_1 = lean_mk_string("parenthesizerAttribute"); +return x_1; +} +} +lean_object* _init_l_Lean_PrettyPrinter_mkParenthesizerAttribute___closed__13() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_PrettyPrinter_mkParenthesizerAttribute___closed__6; +x_2 = l_Lean_PrettyPrinter_mkParenthesizerAttribute___closed__12; +x_3 = lean_name_mk_string(x_1, x_2); +return x_3; +} +} +lean_object* l_Lean_PrettyPrinter_mkParenthesizerAttribute(lean_object* x_1) { +_start: +{ +lean_object* x_2; lean_object* x_3; lean_object* x_4; +x_2 = l_Lean_PrettyPrinter_mkParenthesizerAttribute___closed__11; +x_3 = l_Lean_PrettyPrinter_mkParenthesizerAttribute___closed__13; +x_4 = l_Lean_KeyedDeclsAttribute_init___rarg(x_2, x_3, x_1); +return x_4; +} +} +lean_object* l_Lean_PrettyPrinter_mkParenthesizerAttribute___lambda__1___boxed(lean_object* x_1, lean_object* x_2) { +_start: +{ +lean_object* x_3; +x_3 = l_Lean_PrettyPrinter_mkParenthesizerAttribute___lambda__1(x_1, x_2); +lean_dec(x_2); +return x_3; +} +} +lean_object* l_mkHashMap___at_Lean_PrettyPrinter_parenthesizerAttribute___spec__2(lean_object* x_1) { +_start: +{ +lean_object* x_2; +x_2 = l_mkHashMapImp___rarg(x_1); +return x_2; +} +} +lean_object* _init_l_PersistentHashMap_empty___at_Lean_PrettyPrinter_parenthesizerAttribute___spec__3() { +_start: +{ +lean_object* x_1; +x_1 = l_Lean_LocalContext_Inhabited___closed__1; +return x_1; +} +} +lean_object* _init_l_Lean_SMap_empty___at_Lean_PrettyPrinter_parenthesizerAttribute___spec__1___closed__1() { +_start: +{ +lean_object* x_1; lean_object* x_2; +x_1 = lean_unsigned_to_nat(8u); +x_2 = l_mkHashMapImp___rarg(x_1); +return x_2; +} +} +lean_object* _init_l_Lean_SMap_empty___at_Lean_PrettyPrinter_parenthesizerAttribute___spec__1___closed__2() { +_start: +{ +uint8_t x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; +x_1 = 1; +x_2 = l_Lean_SMap_empty___at_Lean_PrettyPrinter_parenthesizerAttribute___spec__1___closed__1; +x_3 = l_PersistentHashMap_empty___at_Lean_PrettyPrinter_parenthesizerAttribute___spec__3; +x_4 = lean_alloc_ctor(0, 2, 1); +lean_ctor_set(x_4, 0, x_2); +lean_ctor_set(x_4, 1, x_3); +lean_ctor_set_uint8(x_4, sizeof(void*)*2, x_1); +return x_4; +} +} +lean_object* _init_l_Lean_SMap_empty___at_Lean_PrettyPrinter_parenthesizerAttribute___spec__1() { +_start: +{ +lean_object* x_1; +x_1 = l_Lean_SMap_empty___at_Lean_PrettyPrinter_parenthesizerAttribute___spec__1___closed__2; +return x_1; +} +} +lean_object* _init_l_Lean_PrettyPrinter_parenthesizerAttribute___closed__1() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = lean_box(0); +x_2 = l_Lean_SMap_empty___at_Lean_PrettyPrinter_parenthesizerAttribute___spec__1; +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_PrettyPrinter_parenthesizerAttribute___closed__2() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Array_empty___closed__1; +x_2 = l_Lean_PrettyPrinter_parenthesizerAttribute___closed__1; +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_PrettyPrinter_parenthesizerAttribute___closed__3() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; +x_1 = lean_unsigned_to_nat(0u); +x_2 = l_Lean_EnvExtension_Inhabited___rarg___closed__1; +x_3 = l_Lean_PrettyPrinter_parenthesizerAttribute___closed__2; +x_4 = lean_alloc_ctor(0, 3, 0); +lean_ctor_set(x_4, 0, x_1); +lean_ctor_set(x_4, 1, x_2); +lean_ctor_set(x_4, 2, x_3); +return x_4; +} +} +lean_object* _init_l_Lean_PrettyPrinter_parenthesizerAttribute___closed__4() { +_start: +{ +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; +x_1 = l_Lean_PrettyPrinter_parenthesizerAttribute___closed__3; +x_2 = lean_box(0); +x_3 = l_Lean_PersistentEnvExtension_inhabited___rarg___closed__1; +x_4 = l_Lean_Meta_SynthInstance_inferTCGoalsLRAttr___closed__1; +x_5 = l_Lean_PersistentEnvExtension_inhabited___rarg___closed__3; +x_6 = l_Lean_PersistentEnvExtension_inhabited___rarg___closed__4; +x_7 = lean_alloc_ctor(0, 6, 0); +lean_ctor_set(x_7, 0, x_1); +lean_ctor_set(x_7, 1, x_2); +lean_ctor_set(x_7, 2, x_3); +lean_ctor_set(x_7, 3, x_4); +lean_ctor_set(x_7, 4, x_5); +lean_ctor_set(x_7, 5, x_6); +return x_7; +} +} +lean_object* _init_l_Lean_PrettyPrinter_parenthesizerAttribute___closed__5() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = lean_box(0); +x_2 = l_Lean_PrettyPrinter_parenthesizerAttribute___closed__4; +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* initialize_Init_Lean_Parser(lean_object*); +lean_object* initialize_Init_Lean_Elab_Command(lean_object*); +lean_object* initialize_Init_Lean_Delaborator(lean_object*); +static bool _G_initialized = false; +lean_object* initialize_Init_Lean_PrettyPrinter(lean_object* w) { +lean_object * res; +if (_G_initialized) return lean_mk_io_result(lean_box(0)); +_G_initialized = true; +res = initialize_Init_Lean_Parser(lean_io_mk_world()); +if (lean_io_result_is_error(res)) return res; +lean_dec_ref(res); +res = initialize_Init_Lean_Elab_Command(lean_io_mk_world()); +if (lean_io_result_is_error(res)) return res; +lean_dec_ref(res); +res = initialize_Init_Lean_Delaborator(lean_io_mk_world()); +if (lean_io_result_is_error(res)) return res; +lean_dec_ref(res); +l_Lean_PrettyPrinter_mkParenthesizerAttribute___lambda__1___closed__1 = _init_l_Lean_PrettyPrinter_mkParenthesizerAttribute___lambda__1___closed__1(); +lean_mark_persistent(l_Lean_PrettyPrinter_mkParenthesizerAttribute___lambda__1___closed__1); +l_Lean_PrettyPrinter_mkParenthesizerAttribute___lambda__1___closed__2 = _init_l_Lean_PrettyPrinter_mkParenthesizerAttribute___lambda__1___closed__2(); +lean_mark_persistent(l_Lean_PrettyPrinter_mkParenthesizerAttribute___lambda__1___closed__2); +l_Lean_PrettyPrinter_mkParenthesizerAttribute___lambda__1___closed__3 = _init_l_Lean_PrettyPrinter_mkParenthesizerAttribute___lambda__1___closed__3(); +lean_mark_persistent(l_Lean_PrettyPrinter_mkParenthesizerAttribute___lambda__1___closed__3); +l_Lean_PrettyPrinter_mkParenthesizerAttribute___closed__1 = _init_l_Lean_PrettyPrinter_mkParenthesizerAttribute___closed__1(); +lean_mark_persistent(l_Lean_PrettyPrinter_mkParenthesizerAttribute___closed__1); +l_Lean_PrettyPrinter_mkParenthesizerAttribute___closed__2 = _init_l_Lean_PrettyPrinter_mkParenthesizerAttribute___closed__2(); +lean_mark_persistent(l_Lean_PrettyPrinter_mkParenthesizerAttribute___closed__2); +l_Lean_PrettyPrinter_mkParenthesizerAttribute___closed__3 = _init_l_Lean_PrettyPrinter_mkParenthesizerAttribute___closed__3(); +lean_mark_persistent(l_Lean_PrettyPrinter_mkParenthesizerAttribute___closed__3); +l_Lean_PrettyPrinter_mkParenthesizerAttribute___closed__4 = _init_l_Lean_PrettyPrinter_mkParenthesizerAttribute___closed__4(); +lean_mark_persistent(l_Lean_PrettyPrinter_mkParenthesizerAttribute___closed__4); +l_Lean_PrettyPrinter_mkParenthesizerAttribute___closed__5 = _init_l_Lean_PrettyPrinter_mkParenthesizerAttribute___closed__5(); +lean_mark_persistent(l_Lean_PrettyPrinter_mkParenthesizerAttribute___closed__5); +l_Lean_PrettyPrinter_mkParenthesizerAttribute___closed__6 = _init_l_Lean_PrettyPrinter_mkParenthesizerAttribute___closed__6(); +lean_mark_persistent(l_Lean_PrettyPrinter_mkParenthesizerAttribute___closed__6); +l_Lean_PrettyPrinter_mkParenthesizerAttribute___closed__7 = _init_l_Lean_PrettyPrinter_mkParenthesizerAttribute___closed__7(); +lean_mark_persistent(l_Lean_PrettyPrinter_mkParenthesizerAttribute___closed__7); +l_Lean_PrettyPrinter_mkParenthesizerAttribute___closed__8 = _init_l_Lean_PrettyPrinter_mkParenthesizerAttribute___closed__8(); +lean_mark_persistent(l_Lean_PrettyPrinter_mkParenthesizerAttribute___closed__8); +l_Lean_PrettyPrinter_mkParenthesizerAttribute___closed__9 = _init_l_Lean_PrettyPrinter_mkParenthesizerAttribute___closed__9(); +lean_mark_persistent(l_Lean_PrettyPrinter_mkParenthesizerAttribute___closed__9); +l_Lean_PrettyPrinter_mkParenthesizerAttribute___closed__10 = _init_l_Lean_PrettyPrinter_mkParenthesizerAttribute___closed__10(); +lean_mark_persistent(l_Lean_PrettyPrinter_mkParenthesizerAttribute___closed__10); +l_Lean_PrettyPrinter_mkParenthesizerAttribute___closed__11 = _init_l_Lean_PrettyPrinter_mkParenthesizerAttribute___closed__11(); +lean_mark_persistent(l_Lean_PrettyPrinter_mkParenthesizerAttribute___closed__11); +l_Lean_PrettyPrinter_mkParenthesizerAttribute___closed__12 = _init_l_Lean_PrettyPrinter_mkParenthesizerAttribute___closed__12(); +lean_mark_persistent(l_Lean_PrettyPrinter_mkParenthesizerAttribute___closed__12); +l_Lean_PrettyPrinter_mkParenthesizerAttribute___closed__13 = _init_l_Lean_PrettyPrinter_mkParenthesizerAttribute___closed__13(); +lean_mark_persistent(l_Lean_PrettyPrinter_mkParenthesizerAttribute___closed__13); +l_PersistentHashMap_empty___at_Lean_PrettyPrinter_parenthesizerAttribute___spec__3 = _init_l_PersistentHashMap_empty___at_Lean_PrettyPrinter_parenthesizerAttribute___spec__3(); +lean_mark_persistent(l_PersistentHashMap_empty___at_Lean_PrettyPrinter_parenthesizerAttribute___spec__3); +l_Lean_SMap_empty___at_Lean_PrettyPrinter_parenthesizerAttribute___spec__1___closed__1 = _init_l_Lean_SMap_empty___at_Lean_PrettyPrinter_parenthesizerAttribute___spec__1___closed__1(); +lean_mark_persistent(l_Lean_SMap_empty___at_Lean_PrettyPrinter_parenthesizerAttribute___spec__1___closed__1); +l_Lean_SMap_empty___at_Lean_PrettyPrinter_parenthesizerAttribute___spec__1___closed__2 = _init_l_Lean_SMap_empty___at_Lean_PrettyPrinter_parenthesizerAttribute___spec__1___closed__2(); +lean_mark_persistent(l_Lean_SMap_empty___at_Lean_PrettyPrinter_parenthesizerAttribute___spec__1___closed__2); +l_Lean_SMap_empty___at_Lean_PrettyPrinter_parenthesizerAttribute___spec__1 = _init_l_Lean_SMap_empty___at_Lean_PrettyPrinter_parenthesizerAttribute___spec__1(); +lean_mark_persistent(l_Lean_SMap_empty___at_Lean_PrettyPrinter_parenthesizerAttribute___spec__1); +l_Lean_PrettyPrinter_parenthesizerAttribute___closed__1 = _init_l_Lean_PrettyPrinter_parenthesizerAttribute___closed__1(); +lean_mark_persistent(l_Lean_PrettyPrinter_parenthesizerAttribute___closed__1); +l_Lean_PrettyPrinter_parenthesizerAttribute___closed__2 = _init_l_Lean_PrettyPrinter_parenthesizerAttribute___closed__2(); +lean_mark_persistent(l_Lean_PrettyPrinter_parenthesizerAttribute___closed__2); +l_Lean_PrettyPrinter_parenthesizerAttribute___closed__3 = _init_l_Lean_PrettyPrinter_parenthesizerAttribute___closed__3(); +lean_mark_persistent(l_Lean_PrettyPrinter_parenthesizerAttribute___closed__3); +l_Lean_PrettyPrinter_parenthesizerAttribute___closed__4 = _init_l_Lean_PrettyPrinter_parenthesizerAttribute___closed__4(); +lean_mark_persistent(l_Lean_PrettyPrinter_parenthesizerAttribute___closed__4); +l_Lean_PrettyPrinter_parenthesizerAttribute___closed__5 = _init_l_Lean_PrettyPrinter_parenthesizerAttribute___closed__5(); +lean_mark_persistent(l_Lean_PrettyPrinter_parenthesizerAttribute___closed__5); +res = l_Lean_PrettyPrinter_mkParenthesizerAttribute(lean_io_mk_world()); +if (lean_io_result_is_error(res)) return res; +l_Lean_PrettyPrinter_parenthesizerAttribute = lean_io_result_get_value(res); +lean_mark_persistent(l_Lean_PrettyPrinter_parenthesizerAttribute); +lean_dec_ref(res); +return lean_mk_io_result(lean_box(0)); +} +#ifdef __cplusplus +} +#endif