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

chore: update stage0

Browse source
This commit is contained in:
Leonardo de Moura 2020-11-30 15:58:29 -08:00
parent b437cfd9a3
commit 8c712cd145
23 changed files with 43783 additions and 39043 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
stage0/src/Lean.lean generated
View file

@ -22,7 +22,6 @@ import Lean.Meta
import Lean.Util
import Lean.Eval
import Lean.Structure
import Lean.Delaborator
import Lean.PrettyPrinter
import Lean.CoreM
import Lean.InternalExceptionId

2
stage0/src/Lean/Elab/SyntheticMVars.lean generated
View file

@ -155,7 +155,7 @@ def tryToSynthesizeUsingDefaultInstances (mvarId : MVarId) : MetaM (Option (List
match (← getDefaultInstances className) with
| [] => return none
| defaultInstances =>
for defaultInstance in defaultInstances do
for (defaultInstance, prio) in defaultInstances do
match (← tryToSynthesizeUsingDefaultInstance mvarId defaultInstance) with
| some newMVarDecls => return some newMVarDecls
| none => continue

20
stage0/src/Lean/Meta/Instances.lean generated
View file

@ -76,17 +76,22 @@ def getGlobalInstancesIndex : MetaM (DiscrTree Expr) :=
structure DefaultInstanceEntry where
className : Name
instanceName : Name
priority : Nat
abbrev PrioritySet := Std.RBTree Nat (.<.)
structure DefaultInstances where
defaultInstances : NameMap (List Name) := {}
defaultInstances : NameMap (List (Name × Nat)) := {}
priorities : PrioritySet := {}
instance : Inhabited DefaultInstances where
default := {}
def addDefaultInstanceEntry (d : DefaultInstances) (e : DefaultInstanceEntry) : DefaultInstances :=
let d := { d with priorities := d.priorities.insert e.priority }
match d.defaultInstances.find? e.className with
| some insts => { defaultInstances := d.defaultInstances.insert e.className <| e.instanceName :: insts }
| none => { defaultInstances := d.defaultInstances.insert e.className [e.instanceName] }
| some insts => { d with defaultInstances := d.defaultInstances.insert e.className <| (e.instanceName, e.priority) :: insts }
| none => { d with defaultInstances := d.defaultInstances.insert e.className [(e.instanceName, e.priority)] }
builtin_initialize defaultInstanceExtension : SimplePersistentEnvExtension DefaultInstanceEntry DefaultInstances ←
registerSimplePersistentEnvExtension {
@ -95,7 +100,7 @@ builtin_initialize defaultInstanceExtension : SimplePersistentEnvExtension Defau
addImportedFn := fun es => (mkStateFromImportedEntries addDefaultInstanceEntry {} es)
}
def addDefaultInstance (declName : Name) : MetaM Unit := do
def addDefaultInstance (declName : Name) (prio : Nat := 0) : MetaM Unit := do
match (← getEnv).find? declName with
| none => throwError! "unknown constant '{declName}'"
| some info =>
@ -104,7 +109,7 @@ def addDefaultInstance (declName : Name) : MetaM Unit := do
| Expr.const className _ _ =>
unless isClass (← getEnv) className do
throwError! "invalid default instance '{declName}', it has type '({className} ...)', but {className}' is not a type class"
setEnv <| defaultInstanceExtension.addEntry (← getEnv) { className := className, instanceName := declName }
setEnv <| defaultInstanceExtension.addEntry (← getEnv) { className := className, instanceName := declName, priority := prio }
| _ => throwError! "invalid default instance '{declName}', type must be of the form '(C ...)' where 'C' is a type class"
builtin_initialize
@ -118,7 +123,10 @@ builtin_initialize
pure ()
}
def getDefaultInstances [Monad m] [MonadEnv m] (className : Name) : m (List Name) :=
def getDefaultInstancesPriorities [Monad m] [MonadEnv m] : m PrioritySet :=
return defaultInstanceExtension.getState (← getEnv) |>.priorities
def getDefaultInstances [Monad m] [MonadEnv m] (className : Name) : m (List (Name × Nat)) :=
return defaultInstanceExtension.getState (← getEnv) |>.defaultInstances.find? className |>.getD []
end Lean.Meta

57
stage0/src/Lean/Meta/Match/CaseArraySizes.lean generated
View file

@ -59,33 +59,34 @@ private partial def introArrayLit (mvarId : MVarId) (a : Expr) (n : Nat) (xNameP
n) `..., x_1 ... x_{sizes[n-1]} |- C #[x_1, ..., x_{sizes[n-1]}]`
n+1) `..., (h_1 : a.size != sizes[0]), ..., (h_n : a.size != sizes[n-1]) |- C a`
where `n = sizes.size` -/
def caseArraySizes (mvarId : MVarId) (fvarId : FVarId) (sizes : Array Nat) (xNamePrefix := `x) (hNamePrefix := `h) : MetaM (Array CaseArraySizesSubgoal) := do
let a := mkFVar fvarId
let α ← getArrayArgType a
let aSize ← mkAppM `Array.size #[a]
let mvarId ← assertExt mvarId `aSize (mkConst `Nat) aSize
let (aSizeFVarId, mvarId) ← intro1 mvarId
let (hEq, mvarId) ← intro1 mvarId
let subgoals ← caseValues mvarId aSizeFVarId (sizes.map mkNatLit) hNamePrefix
subgoals.mapIdxM fun i subgoal => do
let subst := subgoal.subst
let mvarId := subgoal.mvarId
let hEqSz := (subst.get hEq).fvarId!
if h : i.val < sizes.size then
let n := sizes.get ⟨i, h⟩
let mvarId ← clear mvarId subgoal.newHs[0]
let mvarId ← clear mvarId (subst.get aSizeFVarId).fvarId!
withMVarContext mvarId do
let hEqSzSymm ← mkEqSymm (mkFVar hEqSz)
let mvarId ← introArrayLit mvarId a n xNamePrefix hEqSzSymm
let (xs, mvarId) ← introN mvarId n
let (hEqLit, mvarId) ← intro1 mvarId
let mvarId ← clear mvarId hEqSz
let (subst, mvarId) ← substCore mvarId hEqLit false subst
pure { mvarId := mvarId, elems := xs, subst := subst }
else
let (subst, mvarId) ← substCore mvarId hEq false subst
let diseqs := subgoal.newHs.map fun fvarId => (subst.get fvarId).fvarId!
pure { mvarId := mvarId, diseqs := diseqs, subst := subst }
def caseArraySizes (mvarId : MVarId) (fvarId : FVarId) (sizes : Array Nat) (xNamePrefix := `x) (hNamePrefix := `h) : MetaM (Array CaseArraySizesSubgoal) :=
withMVarContext mvarId do
let a := mkFVar fvarId
let α ← getArrayArgType a
let aSize ← mkAppM `Array.size #[a]
let mvarId ← assertExt mvarId `aSize (mkConst `Nat) aSize
let (aSizeFVarId, mvarId) ← intro1 mvarId
let (hEq, mvarId) ← intro1 mvarId
let subgoals ← caseValues mvarId aSizeFVarId (sizes.map mkNatLit) hNamePrefix
subgoals.mapIdxM fun i subgoal => do
let subst := subgoal.subst
let mvarId := subgoal.mvarId
let hEqSz := (subst.get hEq).fvarId!
if h : i.val < sizes.size then
let n := sizes.get ⟨i, h⟩
let mvarId ← clear mvarId subgoal.newHs[0]
let mvarId ← clear mvarId (subst.get aSizeFVarId).fvarId!
withMVarContext mvarId do
let hEqSzSymm ← mkEqSymm (mkFVar hEqSz)
let mvarId ← introArrayLit mvarId a n xNamePrefix hEqSzSymm
let (xs, mvarId) ← introN mvarId n
let (hEqLit, mvarId) ← intro1 mvarId
let mvarId ← clear mvarId hEqSz
let (subst, mvarId) ← substCore mvarId hEqLit false subst
pure { mvarId := mvarId, elems := xs, subst := subst }
else
let (subst, mvarId) ← substCore mvarId hEq false subst
let diseqs := subgoal.newHs.map fun fvarId => (subst.get fvarId).fvarId!
pure { mvarId := mvarId, diseqs := diseqs, subst := subst }
end Lean.Meta

2
stage0/src/Lean/Meta/Match/CaseValues.lean generated
View file

@ -26,7 +26,7 @@ instance : Inhabited CaseValueSubgoal :=
Remark: `subst` field of the second subgoal is equal to the input `subst`. -/
def caseValueAux (mvarId : MVarId) (fvarId : FVarId) (value : Expr) (hName : Name := `h) (subst : FVarSubst := {})
: MetaM (CaseValueSubgoal × CaseValueSubgoal) :=
withMVarContext mvarId $ do
withMVarContext mvarId do
let tag ← getMVarTag mvarId
checkNotAssigned mvarId `caseValue
let target ← getMVarType mvarId

10
stage0/src/Lean/Meta/Match/Match.lean generated
View file

@ -453,9 +453,9 @@ private def processArrayLit (p : Problem) : MetaM (Array Problem) := do
let elems := subgoal.elems.toList
let newVars := elems.map mkFVar ++ xs
let newVars := newVars.map fun x => x.applyFVarSubst subst
let subex := Example.arrayLit $ elems.map Example.var
let examples := p.examples.map $ Example.replaceFVarId x.fvarId! subex
let examples := examples.map $ Example.applyFVarSubst subst
let subex := Example.arrayLit <| elems.map Example.var
let examples := p.examples.map <| Example.replaceFVarId x.fvarId! subex
let examples := examples.map <| Example.applyFVarSubst subst
let newAlts := p.alts.filter fun alt => match alt.patterns with
| Pattern.arrayLit _ ps :: _ => ps.length == size
| Pattern.var _ :: _ => true
@ -463,7 +463,9 @@ private def processArrayLit (p : Problem) : MetaM (Array Problem) := do
let newAlts := newAlts.map fun alt => alt.applyFVarSubst subst
let newAlts ← newAlts.mapM fun alt => match alt.patterns with
| Pattern.arrayLit _ pats :: ps => pure { alt with patterns := pats ++ ps }
| Pattern.var fvarId :: ps => do let α ← getArrayArgType x; expandVarIntoArrayLit { alt with patterns := ps } fvarId α size
| Pattern.var fvarId :: ps => do
let α ← getArrayArgType <| subst.apply x
expandVarIntoArrayLit { alt with patterns := ps } fvarId α size
| _ => unreachable!
pure { mvarId := subgoal.mvarId, vars := newVars, alts := newAlts, examples := examples }
else do

2
stage0/src/Lean/PrettyPrinter.lean generated
View file

@ -3,7 +3,7 @@ Copyright (c) 2020 Sebastian Ullrich. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Sebastian Ullrich
-/
import Lean.Delaborator
import Lean.PrettyPrinter.Delaborator
import Lean.PrettyPrinter.Parenthesizer
import Lean.PrettyPrinter.Formatter
import Lean.Parser.Module

7
stage0/src/Lean/PrettyPrinter/Delaborator.lean generated Normal file
View file

@ -0,0 +1,7 @@
/-
Copyright (c) 2020 Sebastian Ullrich. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Sebastian Ullrich
-/
import Lean.PrettyPrinter.Delaborator.Basic
import Lean.PrettyPrinter.Delaborator.Builtins

277
stage0/src/Lean/PrettyPrinter/Delaborator/Basic.lean generated Normal file
View file

@ -0,0 +1,277 @@
/-
Copyright (c) 2020 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Sebastian Ullrich
-/
/-!
The delaborator is the first stage of the pretty printer, and the inverse of the
elaborator: it turns fully elaborated `Expr` core terms back into surface-level
`Syntax`, omitting some implicit information again and using higher-level syntax
abstractions like notations where possible. The exact behavior can be customized
using pretty printer options; activating `pp.all` should guarantee that the
delaborator is injective and that re-elaborating the resulting `Syntax`
round-trips.
Pretty printer options can be given not only for the whole term, but also
specific subterms. This is used both when automatically refining pp options
until round-trip and when interactively selecting pp options for a subterm (both
TBD). The association of options to subterms is done by assigning a unique,
synthetic Nat position to each subterm derived from its position in the full
term. This position is added to the corresponding Syntax object so that
elaboration errors and interactions with the pretty printer output can be traced
back to the subterm.
The delaborator is extensible via the `[delab]` attribute.
-/
import Lean.KeyedDeclsAttribute
import Lean.ProjFns
import Lean.Syntax
import Lean.Meta.Match
import Lean.Elab.Term
namespace Lean
-- TODO: move, maybe
namespace Level
protected partial def quote : Level → Syntax
| zero _ => Unhygienic.run `(level|0)
| l@(succ _ _) => match l.toNat with
| some n => Unhygienic.run `(level|$(quote n):numLit)
| none => Unhygienic.run `(level|$(Level.quote l.getLevelOffset) + $(quote l.getOffset):numLit)
| max l1 l2 _ => match_syntax Level.quote l2 with
| `(level|max $ls*) => Unhygienic.run `(level|max $(Level.quote l1) $ls*)
| l2 => Unhygienic.run `(level|max $(Level.quote l1) $l2)
| imax l1 l2 _ => match_syntax Level.quote l2 with
| `(level|imax $ls*) => Unhygienic.run `(level|imax $(Level.quote l1) $ls*)
| l2 => Unhygienic.run `(level|imax $(Level.quote l1) $l2)
| param n _ => Unhygienic.run `(level|$(mkIdent n):ident)
-- HACK: approximation
| mvar n _ => Unhygienic.run `(level|_)
instance : Quote Level := ⟨Level.quote⟩
end Level
def getPPBinderTypes (o : Options) : Bool := o.get `pp.binder_types true
def getPPCoercions (o : Options) : Bool := o.get `pp.coercions true
def getPPExplicit (o : Options) : Bool := o.get `pp.explicit false
def getPPNotation (o : Options) : Bool := o.get `pp.notation true
def getPPStructureProjections (o : Options) : Bool := o.get `pp.structure_projections true
def getPPStructureInstances (o : Options) : Bool := o.get `pp.structure_instances true
def getPPStructureInstanceType (o : Options) : Bool := o.get `pp.structure_instance_type false
def getPPUniverses (o : Options) : Bool := o.get `pp.universes false
def getPPFullNames (o : Options) : Bool := o.get `pp.full_names false
def getPPPrivateNames (o : Options) : Bool := o.get `pp.private_names false
def getPPUnicode (o : Options) : Bool := o.get `pp.unicode true
def getPPAll (o : Options) : Bool := o.get `pp.all false
builtin_initialize
registerOption `pp.explicit { defValue := false, group := "pp", descr := "(pretty printer) display implicit arguments" }
registerOption `pp.structure_instance_type { defValue := false, group := "pp", descr := "(pretty printer) display type of structure instances" }
-- TODO: register other options when old pretty printer is removed
--registerOption `pp.universes { defValue := false, group := "pp", descr := "(pretty printer) display universes" }
/-- Associate pretty printer options to a specific subterm using a synthetic position. -/
abbrev OptionsPerPos := Std.RBMap Nat Options (fun a b => a < b)
namespace PrettyPrinter
namespace Delaborator
open Lean.Meta
structure Context where
-- In contrast to other systems like the elaborator, we do not pass the current term explicitly as a
-- parameter, but store it in the monad so that we can keep it in sync with `pos`.
expr : Expr
pos : Nat := 1
defaultOptions : Options
optionsPerPos : OptionsPerPos
currNamespace : Name
openDecls : List OpenDecl
-- Exceptions from delaborators are not expected. We use an internal exception to signal whether
-- the delaborator was able to produce a Syntax object.
builtin_initialize delabFailureId : InternalExceptionId ← registerInternalExceptionId `delabFailure
abbrev DelabM := ReaderT Context MetaM
abbrev Delab := DelabM Syntax
instance {α} : Inhabited (DelabM α) := ⟨throw arbitrary⟩
@[inline] protected def orElse {α} (d₁ d₂ : DelabM α) : DelabM α := do
catchInternalId delabFailureId d₁ (fun _ => d₂)
protected def failure {α} : DelabM α := throw $ Exception.internal delabFailureId
instance : Alternative DelabM := {
orElse := Delaborator.orElse,
failure := Delaborator.failure
}
-- HACK: necessary since it would otherwise prefer the instance from MonadExcept
instance {α} : OrElse (DelabM α) := ⟨Delaborator.orElse⟩
-- Macro scopes in the delaborator output are ultimately ignored by the pretty printer,
-- so give a trivial implementation.
instance : MonadQuotation DelabM := {
getCurrMacroScope := pure arbitrary,
getMainModule := pure arbitrary,
withFreshMacroScope := fun x => x
}
unsafe def mkDelabAttribute : IO (KeyedDeclsAttribute Delab) :=
KeyedDeclsAttribute.init {
builtinName := `builtinDelab,
name := `delab,
descr := "Register a delaborator.
[delab k] registers a declaration of type `Lean.PrettyPrinter.Delaborator.Delab` for the `Lean.Expr`
constructor `k`. Multiple delaborators for a single constructor are tried in turn until
the first success. If the term to be delaborated is an application of a constant `c`,
elaborators for `app.c` are tried first; this is also done for `Expr.const`s (\"nullary applications\")
to reduce special casing. If the term is an `Expr.mdata` with a single key `k`, `mdata.k`
is tried first.",
valueTypeName := `Lean.PrettyPrinter.Delaborator.Delab
} `Lean.PrettyPrinter.Delaborator.delabAttribute
@[builtinInit mkDelabAttribute] constant delabAttribute : KeyedDeclsAttribute Delab
def getExpr : DelabM Expr := do
let ctx ← read
pure ctx.expr
def getExprKind : DelabM Name := do
let e ← getExpr
pure $ match e with
| Expr.bvar _ _ => `bvar
| Expr.fvar _ _ => `fvar
| Expr.mvar _ _ => `mvar
| Expr.sort _ _ => `sort
| Expr.const c _ _ =>
-- we identify constants as "nullary applications" to reduce special casing
`app ++ c
| Expr.app fn _ _ => match fn.getAppFn with
| Expr.const c _ _ => `app ++ c
| _ => `app
| Expr.lam _ _ _ _ => `lam
| Expr.forallE _ _ _ _ => `forallE
| Expr.letE _ _ _ _ _ => `letE
| Expr.lit _ _ => `lit
| Expr.mdata m _ _ => match m.entries with
| [(key, _)] => `mdata ++ key
| _ => `mdata
| Expr.proj _ _ _ _ => `proj
/-- Evaluate option accessor, using subterm-specific options if set. Default to `true` if `pp.all` is set. -/
def getPPOption (opt : Options → Bool) : DelabM Bool := do
let ctx ← read
let opt := fun opts => opt opts || getPPAll opts
let val := opt ctx.defaultOptions
match ctx.optionsPerPos.find? ctx.pos with
| some opts => pure $ opt opts
| none => pure val
def whenPPOption (opt : Options → Bool) (d : Delab) : Delab := do
let b ← getPPOption opt
if b then d else failure
def whenNotPPOption (opt : Options → Bool) (d : Delab) : Delab := do
let b ← getPPOption opt
if b then failure else d
/--
Descend into `child`, the `childIdx`-th subterm of the current term, and update position.
Because `childIdx < 3` in the case of `Expr`, we can injectively map a path
`childIdxs` to a natural number by computing the value of the 3-ary representation
`1 :: childIdxs`, since n-ary representations without leading zeros are unique.
Note that `pos` is initialized to `1` (case `childIdxs == []`).
-/
def descend {α} (child : Expr) (childIdx : Nat) (d : DelabM α) : DelabM α :=
withReader (fun cfg => { cfg with expr := child, pos := cfg.pos * 3 + childIdx }) d
def withAppFn {α} (d : DelabM α) : DelabM α := do
let Expr.app fn _ _ ← getExpr | unreachable!
descend fn 0 d
def withAppArg {α} (d : DelabM α) : DelabM α := do
let Expr.app _ arg _ ← getExpr | unreachable!
descend arg 1 d
partial def withAppFnArgs {α} : DelabM α → (α → DelabM α) → DelabM α
| fnD, argD => do
let Expr.app fn arg _ ← getExpr | fnD
let a ← withAppFn (withAppFnArgs fnD argD)
withAppArg (argD a)
def withBindingDomain {α} (d : DelabM α) : DelabM α := do
let e ← getExpr
descend e.bindingDomain! 0 d
def withBindingBody {α} (n : Name) (d : DelabM α) : DelabM α := do
let e ← getExpr
withLocalDecl n e.binderInfo e.bindingDomain! fun fvar =>
let b := e.bindingBody!.instantiate1 fvar
descend b 1 d
def withProj {α} (d : DelabM α) : DelabM α := do
let Expr.proj _ _ e _ ← getExpr | unreachable!
descend e 0 d
def withMDataExpr {α} (d : DelabM α) : DelabM α := do
let Expr.mdata _ e _ ← getExpr | unreachable!
-- do not change position so that options on an mdata are automatically forwarded to the child
withReader ({ · with expr := e }) d
partial def annotatePos (pos : Nat) : Syntax → Syntax
| stx@(Syntax.ident _ _ _ _) => stx.setInfo { pos := pos }
-- app => annotate function
| stx@(Syntax.node `Lean.Parser.Term.app args) => stx.modifyArg 0 (annotatePos pos)
-- otherwise, annotate first direct child token if any
| stx => match stx.getArgs.findIdx? Syntax.isAtom with
| some idx => stx.modifyArg idx (Syntax.setInfo { pos := pos })
| none => stx
def annotateCurPos (stx : Syntax) : Delab := do
let ctx ← read
pure $ annotatePos ctx.pos stx
def getUnusedName (suggestion : Name) : DelabM Name := do
-- Use a nicer binder name than `[anonymous]`. We probably shouldn't do this in all LocalContext use cases, so do it here.
let suggestion := if suggestion.isAnonymous then `a else suggestion;
let lctx ← getLCtx
pure $ lctx.getUnusedName suggestion
def withBindingBodyUnusedName {α} (d : Syntax → DelabM α) : DelabM α := do
let n ← getUnusedName (← getExpr).bindingName!
let stxN ← annotateCurPos (mkIdent n)
withBindingBody n $ d stxN
@[inline] def liftMetaM {α} (x : MetaM α) : DelabM α :=
liftM x
partial def delabFor : Name → Delab
| Name.anonymous => failure
| k => do
let env ← getEnv
(match (delabAttribute.ext.getState env).table.find? k with
| some delabs => delabs.firstM id >>= annotateCurPos
| none => failure) <|>
-- have `app.Option.some` fall back to `app` etc.
delabFor k.getRoot
def delab : Delab := do
let k ← getExprKind
delabFor k <|> (liftM $ show MetaM Syntax from throwError $ "don't know how to delaborate '" ++ toString k ++ "'")
end Delaborator
/-- "Delaborate" the given term into surface-level syntax using the default and given subterm-specific options. -/
def delab (currNamespace : Name) (openDecls : List OpenDecl) (e : Expr) (optionsPerPos : OptionsPerPos := {}) : MetaM Syntax := do
trace[PrettyPrinter.delab.input]! "{fmt e}"
let opts ← MonadOptions.getOptions
catchInternalId Delaborator.delabFailureId
(Delaborator.delab.run { expr := e, defaultOptions := opts, optionsPerPos := optionsPerPos, currNamespace := currNamespace, openDecls := openDecls })
(fun _ => unreachable!)
builtin_initialize registerTraceClass `PrettyPrinter.delab
end PrettyPrinter
end Lean

270
stage0/src/Lean/Delaborator.lean → stage0/src/Lean/PrettyPrinter/Delaborator/Builtins.lean generated
View file

@ -1,264 +1,14 @@
/-
Copyright (c) 2020 Microsoft Corporation. All rights reserved.
Copyright (c) 2020 Sebastian Ullrich. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Sebastian Ullrich
-/
/-!
The delaborator is the first stage of the pretty printer, and the inverse of the
elaborator: it turns fully elaborated `Expr` core terms back into surface-level
`Syntax`, omitting some implicit information again and using higher-level syntax
abstractions like notations where possible. The exact behavior can be customized
using pretty printer options; activating `pp.all` should guarantee that the
delaborator is injective and that re-elaborating the resulting `Syntax`
round-trips.
import Lean.PrettyPrinter.Delaborator.Basic
Pretty printer options can be given not only for the whole term, but also
specific subterms. This is used both when automatically refining pp options
until round-trip and when interactively selecting pp options for a subterm (both
TBD). The association of options to subterms is done by assigning a unique,
synthetic Nat position to each subterm derived from its position in the full
term. This position is added to the corresponding Syntax object so that
elaboration errors and interactions with the pretty printer output can be traced
back to the subterm.
The delaborator is extensible via the `[delab]` attribute.
-/
import Lean.KeyedDeclsAttribute
import Lean.ProjFns
import Lean.Syntax
import Lean.Meta.Match
import Lean.Elab.Term
namespace Lean
-- TODO: move, maybe
namespace Level
protected partial def quote : Level → Syntax
| zero _ => Unhygienic.run `(level|0)
| l@(succ _ _) => match l.toNat with
| some n => Unhygienic.run `(level|$(quote n):numLit)
| none => Unhygienic.run `(level|$(Level.quote l.getLevelOffset) + $(quote l.getOffset):numLit)
| max l1 l2 _ => match_syntax Level.quote l2 with
| `(level|max $ls*) => Unhygienic.run `(level|max $(Level.quote l1) $ls*)
| l2 => Unhygienic.run `(level|max $(Level.quote l1) $l2)
| imax l1 l2 _ => match_syntax Level.quote l2 with
| `(level|imax $ls*) => Unhygienic.run `(level|imax $(Level.quote l1) $ls*)
| l2 => Unhygienic.run `(level|imax $(Level.quote l1) $l2)
| param n _ => Unhygienic.run `(level|$(mkIdent n):ident)
-- HACK: approximation
| mvar n _ => Unhygienic.run `(level|_)
instance : Quote Level := ⟨Level.quote⟩
end Level
def getPPBinderTypes (o : Options) : Bool := o.get `pp.binder_types true
def getPPCoercions (o : Options) : Bool := o.get `pp.coercions true
def getPPExplicit (o : Options) : Bool := o.get `pp.explicit false
def getPPNotation (o : Options) : Bool := o.get `pp.notation true
def getPPStructureProjections (o : Options) : Bool := o.get `pp.structure_projections true
def getPPStructureInstances (o : Options) : Bool := o.get `pp.structure_instances true
def getPPStructureInstanceType (o : Options) : Bool := o.get `pp.structure_instance_type false
def getPPUniverses (o : Options) : Bool := o.get `pp.universes false
def getPPFullNames (o : Options) : Bool := o.get `pp.full_names false
def getPPPrivateNames (o : Options) : Bool := o.get `pp.private_names false
def getPPUnicode (o : Options) : Bool := o.get `pp.unicode true
def getPPAll (o : Options) : Bool := o.get `pp.all false
builtin_initialize
registerOption `pp.explicit { defValue := false, group := "pp", descr := "(pretty printer) display implicit arguments" }
registerOption `pp.structure_instance_type { defValue := false, group := "pp", descr := "(pretty printer) display type of structure instances" }
-- TODO: register other options when old pretty printer is removed
--registerOption `pp.universes { defValue := false, group := "pp", descr := "(pretty printer) display universes" }
/-- Associate pretty printer options to a specific subterm using a synthetic position. -/
abbrev OptionsPerPos := Std.RBMap Nat Options (fun a b => a < b)
namespace Delaborator
namespace Lean.PrettyPrinter.Delaborator
open Lean.Meta
structure Context where
-- In contrast to other systems like the elaborator, we do not pass the current term explicitly as a
-- parameter, but store it in the monad so that we can keep it in sync with `pos`.
expr : Expr
pos : Nat := 1
defaultOptions : Options
optionsPerPos : OptionsPerPos
currNamespace : Name
openDecls : List OpenDecl
-- Exceptions from delaborators are not expected. We use an internal exception to signal whether
-- the delaborator was able to produce a Syntax object.
builtin_initialize delabFailureId : InternalExceptionId ← registerInternalExceptionId `delabFailure
abbrev DelabM := ReaderT Context MetaM
abbrev Delab := DelabM Syntax
instance {α} : Inhabited (DelabM α) := ⟨throw arbitrary⟩
@[inline] protected def orElse {α} (d₁ d₂ : DelabM α) : DelabM α := do
catchInternalId delabFailureId d₁ (fun _ => d₂)
protected def failure {α} : DelabM α := throw $ Exception.internal delabFailureId
instance : Alternative DelabM := {
orElse := Delaborator.orElse,
failure := Delaborator.failure
}
-- HACK: necessary since it would otherwise prefer the instance from MonadExcept
instance {α} : OrElse (DelabM α) := ⟨Delaborator.orElse⟩
-- Macro scopes in the delaborator output are ultimately ignored by the pretty printer,
-- so give a trivial implementation.
instance : MonadQuotation DelabM := {
getCurrMacroScope := pure arbitrary,
getMainModule := pure arbitrary,
withFreshMacroScope := fun x => x
}
unsafe def mkDelabAttribute : IO (KeyedDeclsAttribute Delab) :=
KeyedDeclsAttribute.init {
builtinName := `builtinDelab,
name := `delab,
descr := "Register a delaborator.
[delab k] registers a declaration of type `Lean.Delaborator.Delab` for the `Lean.Expr`
constructor `k`. Multiple delaborators for a single constructor are tried in turn until
the first success. If the term to be delaborated is an application of a constant `c`,
elaborators for `app.c` are tried first; this is also done for `Expr.const`s (\"nullary applications\")
to reduce special casing. If the term is an `Expr.mdata` with a single key `k`, `mdata.k`
is tried first.",
valueTypeName := `Lean.PrettyPrinter.Delaborator.Delab
} `Lean.PrettyPrinter.Delaborator.delabAttribute
@[builtinInit mkDelabAttribute] constant delabAttribute : KeyedDeclsAttribute Delab
def getExpr : DelabM Expr := do
let ctx ← read
pure ctx.expr
def getExprKind : DelabM Name := do
let e ← getExpr
pure $ match e with
| Expr.bvar _ _ => `bvar
| Expr.fvar _ _ => `fvar
| Expr.mvar _ _ => `mvar
| Expr.sort _ _ => `sort
| Expr.const c _ _ =>
-- we identify constants as "nullary applications" to reduce special casing
`app ++ c
| Expr.app fn _ _ => match fn.getAppFn with
| Expr.const c _ _ => `app ++ c
| _ => `app
| Expr.lam _ _ _ _ => `lam
| Expr.forallE _ _ _ _ => `forallE
| Expr.letE _ _ _ _ _ => `letE
| Expr.lit _ _ => `lit
| Expr.mdata m _ _ => match m.entries with
| [(key, _)] => `mdata ++ key
| _ => `mdata
| Expr.proj _ _ _ _ => `proj
/-- Evaluate option accessor, using subterm-specific options if set. Default to `true` if `pp.all` is set. -/
def getPPOption (opt : Options → Bool) : DelabM Bool := do
let ctx ← read
let opt := fun opts => opt opts || getPPAll opts
let val := opt ctx.defaultOptions
match ctx.optionsPerPos.find? ctx.pos with
| some opts => pure $ opt opts
| none => pure val
def whenPPOption (opt : Options → Bool) (d : Delab) : Delab := do
let b ← getPPOption opt
if b then d else failure
def whenNotPPOption (opt : Options → Bool) (d : Delab) : Delab := do
let b ← getPPOption opt
if b then failure else d
/--
Descend into `child`, the `childIdx`-th subterm of the current term, and update position.
Because `childIdx < 3` in the case of `Expr`, we can injectively map a path
`childIdxs` to a natural number by computing the value of the 3-ary representation
`1 :: childIdxs`, since n-ary representations without leading zeros are unique.
Note that `pos` is initialized to `1` (case `childIdxs == []`).
-/
def descend {α} (child : Expr) (childIdx : Nat) (d : DelabM α) : DelabM α :=
withReader (fun cfg => { cfg with expr := child, pos := cfg.pos * 3 + childIdx }) d
def withAppFn {α} (d : DelabM α) : DelabM α := do
let Expr.app fn _ _ ← getExpr | unreachable!
descend fn 0 d
def withAppArg {α} (d : DelabM α) : DelabM α := do
let Expr.app _ arg _ ← getExpr | unreachable!
descend arg 1 d
partial def withAppFnArgs {α} : DelabM α → (α → DelabM α) → DelabM α
| fnD, argD => do
let Expr.app fn arg _ ← getExpr | fnD
let a ← withAppFn (withAppFnArgs fnD argD)
withAppArg (argD a)
def withBindingDomain {α} (d : DelabM α) : DelabM α := do
let e ← getExpr
descend e.bindingDomain! 0 d
def withBindingBody {α} (n : Name) (d : DelabM α) : DelabM α := do
let e ← getExpr
withLocalDecl n e.binderInfo e.bindingDomain! fun fvar =>
let b := e.bindingBody!.instantiate1 fvar
descend b 1 d
def withProj {α} (d : DelabM α) : DelabM α := do
let Expr.proj _ _ e _ ← getExpr | unreachable!
descend e 0 d
def withMDataExpr {α} (d : DelabM α) : DelabM α := do
let Expr.mdata _ e _ ← getExpr | unreachable!
-- do not change position so that options on an mdata are automatically forwarded to the child
withReader ({ · with expr := e }) d
partial def annotatePos (pos : Nat) : Syntax → Syntax
| stx@(Syntax.ident _ _ _ _) => stx.setInfo { pos := pos }
-- app => annotate function
| stx@(Syntax.node `Lean.Parser.Term.app args) => stx.modifyArg 0 (annotatePos pos)
-- otherwise, annotate first direct child token if any
| stx => match stx.getArgs.findIdx? Syntax.isAtom with
| some idx => stx.modifyArg idx (Syntax.setInfo { pos := pos })
| none => stx
def annotateCurPos (stx : Syntax) : Delab := do
let ctx ← read
pure $ annotatePos ctx.pos stx
def getUnusedName (suggestion : Name) : DelabM Name := do
-- Use a nicer binder name than `[anonymous]`. We probably shouldn't do this in all LocalContext use cases, so do it here.
let suggestion := if suggestion.isAnonymous then `a else suggestion;
let lctx ← getLCtx
pure $ lctx.getUnusedName suggestion
def withBindingBodyUnusedName {α} (d : Syntax → DelabM α) : DelabM α := do
let n ← getUnusedName (← getExpr).bindingName!
let stxN ← annotateCurPos (mkIdent n)
withBindingBody n $ d stxN
@[inline] def liftMetaM {α} (x : MetaM α) : DelabM α :=
liftM x
partial def delabFor : Name → Delab
| Name.anonymous => failure
| k => do
let env ← getEnv
(match (delabAttribute.ext.getState env).table.find? k with
| some delabs => delabs.firstM id >>= annotateCurPos
| none => failure) <|>
-- have `app.Option.some` fall back to `app` etc.
delabFor k.getRoot
def delab : Delab := do
let k ← getExprKind
delabFor k <|> (liftM $ show MetaM Syntax from throwError $ "don't know how to delaborate '" ++ toString k ++ "'")
@[builtinDelab fvar]
def delabFVar : Delab := do
let Expr.fvar id _ ← getExpr | unreachable!
@ -852,16 +602,4 @@ def delabDo : Delab := whenPPOption getPPNotation do
let items := elems.toArray.map (mkNode `Lean.Parser.Term.doSeqItem #[·, mkNullNode])
`(do $items:doSeqItem*)
end Delaborator
/-- "Delaborate" the given term into surface-level syntax using the default and given subterm-specific options. -/
def delab (currNamespace : Name) (openDecls : List OpenDecl) (e : Expr) (optionsPerPos : OptionsPerPos := {}) : MetaM Syntax := do
trace[PrettyPrinter.delab.input]! "{fmt e}"
let opts ← MonadOptions.getOptions
catchInternalId Delaborator.delabFailureId
(Delaborator.delab.run { expr := e, defaultOptions := opts, optionsPerPos := optionsPerPos, currNamespace := currNamespace, openDecls := openDecls })
(fun _ => unreachable!)
builtin_initialize registerTraceClass `PrettyPrinter.delab
end Lean
end Lean.PrettyPrinter.Delaborator

2
stage0/stdlib/CMakeLists.txt generated
View file

File diff suppressed because one or more lines are too long

6
stage0/stdlib/Lean.c generated
View file

@ -1,6 +1,6 @@
// Lean compiler output
// Module: Lean
// Imports: Init Lean.Data Lean.Compiler Lean.Environment Lean.Modifiers Lean.ProjFns Lean.Runtime Lean.ResolveName Lean.Attributes Lean.Parser Lean.ReducibilityAttrs Lean.Elab Lean.Class Lean.LocalContext Lean.MetavarContext Lean.AuxRecursor Lean.Meta Lean.Util Lean.Eval Lean.Structure Lean.Delaborator Lean.PrettyPrinter Lean.CoreM Lean.InternalExceptionId Lean.Server
// Imports: Init Lean.Data Lean.Compiler Lean.Environment Lean.Modifiers Lean.ProjFns Lean.Runtime Lean.ResolveName Lean.Attributes Lean.Parser Lean.ReducibilityAttrs Lean.Elab Lean.Class Lean.LocalContext Lean.MetavarContext Lean.AuxRecursor Lean.Meta Lean.Util Lean.Eval Lean.Structure Lean.PrettyPrinter Lean.CoreM Lean.InternalExceptionId Lean.Server
#include <lean/lean.h>
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
@ -33,7 +33,6 @@ lean_object* initialize_Lean_Meta(lean_object*);
lean_object* initialize_Lean_Util(lean_object*);
lean_object* initialize_Lean_Eval(lean_object*);
lean_object* initialize_Lean_Structure(lean_object*);
lean_object* initialize_Lean_Delaborator(lean_object*);
lean_object* initialize_Lean_PrettyPrinter(lean_object*);
lean_object* initialize_Lean_CoreM(lean_object*);
lean_object* initialize_Lean_InternalExceptionId(lean_object*);
@ -103,9 +102,6 @@ lean_dec_ref(res);
res = initialize_Lean_Structure(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Lean_Delaborator(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Lean_PrettyPrinter(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);

37451
stage0/stdlib/Lean/Delaborator.c generated
View file

File diff suppressed because it is too large Load diff

334
stage0/stdlib/Lean/Elab/SyntheticMVars.c generated
View file

@ -86,6 +86,7 @@ lean_object* lean_nat_add(lean_object*, lean_object*);
lean_object* l_List_forIn_loop___at___private_Lean_Elab_SyntheticMVars_0__Lean_Elab_Term_reportStuckSyntheticMVars___spec__1___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_ensureHasType(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_isExprDefEqImp(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_tryToSynthesizeUsingDefaultInstances_match__6___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_SyntheticMVars_0__Lean_Elab_Term_synthesizeSyntheticMVarsStep___closed__3;
lean_object* l_Lean_mkAppN(lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_SyntheticMVars_0__Lean_Elab_Term_synthesizePendingCoeInstMVar_match__1(lean_object*);
@ -99,7 +100,6 @@ lean_object* l___private_Lean_Elab_SyntheticMVars_0__Lean_Elab_Term_synthesizeSy
lean_object* l_Lean_Elab_Term_tryToSynthesizeUsingDefaultInstances_match__1(lean_object*);
lean_object* l___private_Lean_Elab_SyntheticMVars_0__Lean_Elab_Term_synthesizeSyntheticMVar___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
lean_object* l_Std_RBNode_find___at_Lean_Meta_addDefaultInstanceEntry___spec__1(lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_SyntheticMVars_0__Lean_Elab_Term_getSomeSynthethicMVarsRef_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_forallMetaTelescopeReducingAux(lean_object*, uint8_t, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_st_ref_take(lean_object*, lean_object*);
@ -168,6 +168,7 @@ lean_object* l_Lean_ConstantInfo_lparams(lean_object*);
extern lean_object* l_Lean_Expr_instInhabitedExpr;
extern uint8_t l_Lean_instInhabitedBinderInfo;
lean_object* l___private_Lean_Elab_SyntheticMVars_0__Lean_Elab_Term_synthesizeSyntheticMVarsStep___closed__9;
lean_object* l_Lean_Elab_Term_tryToSynthesizeUsingDefaultInstances_match__6(lean_object*);
lean_object* l___private_Lean_Elab_SyntheticMVars_0__Lean_Elab_Term_synthesizeSyntheticMVarsStep___closed__4;
lean_object* l___private_Lean_Elab_SyntheticMVars_0__Lean_Elab_Term_resumePostponed___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Util_Trace_0__Lean_checkTraceOptionM___at___private_Lean_Elab_Term_0__Lean_Elab_Term_postponeElabTerm___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -180,7 +181,7 @@ lean_object* l_List_filterAuxM___at___private_Lean_Elab_SyntheticMVars_0__Lean_E
lean_object* l___private_Lean_Elab_SyntheticMVars_0__Lean_Elab_Term_reportStuckSyntheticMVars_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_839____closed__1;
uint8_t lean_nat_dec_le(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_tryToSynthesizeUsingDefaultInstances_match__3___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_tryToSynthesizeUsingDefaultInstances_match__3___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Meta_isClass_x3f___at___private_Lean_Meta_Basic_0__Lean_Meta_withNewFVar___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_ReaderT_bind___at_Lean_Elab_Tactic_liftMetaTacticAux___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_synthesizeInstMVarCore(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -236,6 +237,7 @@ lean_object* l_Lean_mkConst(lean_object*, lean_object*);
extern lean_object* l_Lean_Meta_defaultInstanceExtension;
lean_object* l_Lean_Elab_Term_synthesizeSyntheticMVars_loop___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_tryToSynthesizeUsingDefaultInstances___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Std_RBNode_find___at_Lean_Meta_addDefaultInstanceEntry___spec__3(lean_object*, lean_object*);
extern lean_object* l_Array_findSomeM_x3f___rarg___closed__1;
lean_object* l_Lean_Elab_Term_synthesizeUsingDefault_match__4(lean_object*);
lean_object* l_Lean_Elab_Term_liftTacticElabM___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -4711,7 +4713,28 @@ x_2 = lean_alloc_closure((void*)(l_Lean_Elab_Term_tryToSynthesizeUsingDefaultIns
return x_2;
}
}
lean_object* l_Lean_Elab_Term_tryToSynthesizeUsingDefaultInstances_match__3___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
lean_object* l_Lean_Elab_Term_tryToSynthesizeUsingDefaultInstances_match__3___rarg(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_3 = lean_ctor_get(x_1, 0);
lean_inc(x_3);
x_4 = lean_ctor_get(x_1, 1);
lean_inc(x_4);
lean_dec(x_1);
x_5 = lean_apply_2(x_2, x_3, x_4);
return x_5;
}
}
lean_object* l_Lean_Elab_Term_tryToSynthesizeUsingDefaultInstances_match__3(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_Lean_Elab_Term_tryToSynthesizeUsingDefaultInstances_match__3___rarg), 2, 0);
return x_2;
}
}
lean_object* l_Lean_Elab_Term_tryToSynthesizeUsingDefaultInstances_match__4___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
if (lean_obj_tag(x_1) == 0)
@ -4734,34 +4757,6 @@ return x_7;
}
}
}
lean_object* l_Lean_Elab_Term_tryToSynthesizeUsingDefaultInstances_match__3(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_Lean_Elab_Term_tryToSynthesizeUsingDefaultInstances_match__3___rarg), 3, 0);
return x_2;
}
}
lean_object* l_Lean_Elab_Term_tryToSynthesizeUsingDefaultInstances_match__4___rarg(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;
lean_dec(x_3);
x_4 = lean_box(0);
x_5 = lean_apply_1(x_2, x_4);
return x_5;
}
else
{
lean_object* x_6;
lean_dec(x_2);
x_6 = lean_apply_1(x_3, x_1);
return x_6;
}
}
}
lean_object* l_Lean_Elab_Term_tryToSynthesizeUsingDefaultInstances_match__4(lean_object* x_1) {
_start:
{
@ -4783,13 +4778,10 @@ return x_5;
}
else
{
lean_object* x_6; lean_object* x_7;
lean_object* x_6;
lean_dec(x_2);
x_6 = lean_ctor_get(x_1, 0);
lean_inc(x_6);
lean_dec(x_1);
x_7 = lean_apply_1(x_3, x_6);
return x_7;
x_6 = lean_apply_1(x_3, x_1);
return x_6;
}
}
}
@ -4801,6 +4793,37 @@ x_2 = lean_alloc_closure((void*)(l_Lean_Elab_Term_tryToSynthesizeUsingDefaultIns
return x_2;
}
}
lean_object* l_Lean_Elab_Term_tryToSynthesizeUsingDefaultInstances_match__6___rarg(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;
lean_dec(x_3);
x_4 = lean_box(0);
x_5 = lean_apply_1(x_2, x_4);
return x_5;
}
else
{
lean_object* x_6; lean_object* x_7;
lean_dec(x_2);
x_6 = lean_ctor_get(x_1, 0);
lean_inc(x_6);
lean_dec(x_1);
x_7 = lean_apply_1(x_3, x_6);
return x_7;
}
}
}
lean_object* l_Lean_Elab_Term_tryToSynthesizeUsingDefaultInstances_match__6(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_Lean_Elab_Term_tryToSynthesizeUsingDefaultInstances_match__6___rarg), 3, 0);
return x_2;
}
}
lean_object* l_Lean_Meta_getDefaultInstances___at_Lean_Elab_Term_tryToSynthesizeUsingDefaultInstances___spec__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
_start:
{
@ -4809,7 +4832,7 @@ x_7 = lean_st_ref_get(x_5, x_6);
x_8 = !lean_is_exclusive(x_7);
if (x_8 == 0)
{
lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13;
lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14;
x_9 = lean_ctor_get(x_7, 0);
x_10 = lean_ctor_get(x_9, 0);
lean_inc(x_10);
@ -4817,61 +4840,67 @@ lean_dec(x_9);
x_11 = l_Lean_Meta_defaultInstanceExtension;
x_12 = l_Lean_SimplePersistentEnvExtension_getState___rarg(x_11, x_10);
lean_dec(x_10);
x_13 = l_Std_RBNode_find___at_Lean_Meta_addDefaultInstanceEntry___spec__1(x_12, x_1);
x_13 = lean_ctor_get(x_12, 0);
lean_inc(x_13);
lean_dec(x_12);
if (lean_obj_tag(x_13) == 0)
{
lean_object* x_14;
x_14 = lean_box(0);
lean_ctor_set(x_7, 0, x_14);
return x_7;
}
else
x_14 = l_Std_RBNode_find___at_Lean_Meta_addDefaultInstanceEntry___spec__3(x_13, x_1);
lean_dec(x_13);
if (lean_obj_tag(x_14) == 0)
{
lean_object* x_15;
x_15 = lean_ctor_get(x_13, 0);
lean_inc(x_15);
lean_dec(x_13);
x_15 = lean_box(0);
lean_ctor_set(x_7, 0, x_15);
return x_7;
}
}
else
{
lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21;
x_16 = lean_ctor_get(x_7, 0);
x_17 = lean_ctor_get(x_7, 1);
lean_inc(x_17);
lean_object* x_16;
x_16 = lean_ctor_get(x_14, 0);
lean_inc(x_16);
lean_dec(x_7);
x_18 = lean_ctor_get(x_16, 0);
lean_inc(x_18);
lean_dec(x_16);
x_19 = l_Lean_Meta_defaultInstanceExtension;
x_20 = l_Lean_SimplePersistentEnvExtension_getState___rarg(x_19, x_18);
lean_dec(x_18);
x_21 = l_Std_RBNode_find___at_Lean_Meta_addDefaultInstanceEntry___spec__1(x_20, x_1);
lean_dec(x_20);
if (lean_obj_tag(x_21) == 0)
{
lean_object* x_22; lean_object* x_23;
x_22 = lean_box(0);
x_23 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_23, 0, x_22);
lean_ctor_set(x_23, 1, x_17);
return x_23;
lean_dec(x_14);
lean_ctor_set(x_7, 0, x_16);
return x_7;
}
}
else
{
lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23;
x_17 = lean_ctor_get(x_7, 0);
x_18 = lean_ctor_get(x_7, 1);
lean_inc(x_18);
lean_inc(x_17);
lean_dec(x_7);
x_19 = lean_ctor_get(x_17, 0);
lean_inc(x_19);
lean_dec(x_17);
x_20 = l_Lean_Meta_defaultInstanceExtension;
x_21 = l_Lean_SimplePersistentEnvExtension_getState___rarg(x_20, x_19);
lean_dec(x_19);
x_22 = lean_ctor_get(x_21, 0);
lean_inc(x_22);
lean_dec(x_21);
x_23 = l_Std_RBNode_find___at_Lean_Meta_addDefaultInstanceEntry___spec__3(x_22, x_1);
lean_dec(x_22);
if (lean_obj_tag(x_23) == 0)
{
lean_object* x_24; lean_object* x_25;
x_24 = lean_ctor_get(x_21, 0);
lean_inc(x_24);
lean_dec(x_21);
x_24 = lean_box(0);
x_25 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_25, 0, x_24);
lean_ctor_set(x_25, 1, x_17);
lean_ctor_set(x_25, 1, x_18);
return x_25;
}
else
{
lean_object* x_26; lean_object* x_27;
x_26 = lean_ctor_get(x_23, 0);
lean_inc(x_26);
lean_dec(x_23);
x_27 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_27, 0, x_26);
lean_ctor_set(x_27, 1, x_18);
return x_27;
}
}
}
}
@ -4894,35 +4923,38 @@ return x_10;
}
else
{
lean_object* x_11; lean_object* x_12; lean_object* x_13;
lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14;
lean_dec(x_4);
x_11 = lean_ctor_get(x_3, 0);
lean_inc(x_11);
x_12 = lean_ctor_get(x_3, 1);
lean_inc(x_12);
lean_dec(x_3);
x_13 = lean_ctor_get(x_11, 0);
lean_inc(x_13);
lean_dec(x_11);
lean_inc(x_8);
lean_inc(x_7);
lean_inc(x_6);
lean_inc(x_5);
lean_inc(x_1);
x_13 = l_Lean_Meta_commitWhenSome_x3f___at_Lean_Elab_Term_tryToSynthesizeUsingDefaultInstance___spec__3(x_1, x_11, x_5, x_6, x_7, x_8, x_9);
if (lean_obj_tag(x_13) == 0)
{
lean_object* x_14;
x_14 = lean_ctor_get(x_13, 0);
lean_inc(x_14);
x_14 = l_Lean_Meta_commitWhenSome_x3f___at_Lean_Elab_Term_tryToSynthesizeUsingDefaultInstance___spec__3(x_1, x_13, x_5, x_6, x_7, x_8, x_9);
if (lean_obj_tag(x_14) == 0)
{
lean_object* x_15;
x_15 = lean_ctor_get(x_13, 1);
x_15 = lean_ctor_get(x_14, 0);
lean_inc(x_15);
lean_dec(x_13);
if (lean_obj_tag(x_15) == 0)
{
lean_object* x_16;
x_16 = lean_ctor_get(x_14, 1);
lean_inc(x_16);
lean_dec(x_14);
lean_inc(x_2);
{
lean_object* _tmp_2 = x_12;
lean_object* _tmp_3 = x_2;
lean_object* _tmp_8 = x_15;
lean_object* _tmp_8 = x_16;
x_3 = _tmp_2;
x_4 = _tmp_3;
x_9 = _tmp_8;
@ -4931,7 +4963,7 @@ goto _start;
}
else
{
uint8_t x_17;
uint8_t x_18;
lean_dec(x_12);
lean_dec(x_8);
lean_dec(x_7);
@ -4939,80 +4971,80 @@ lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_2);
lean_dec(x_1);
x_17 = !lean_is_exclusive(x_13);
if (x_17 == 0)
x_18 = !lean_is_exclusive(x_14);
if (x_18 == 0)
{
lean_object* x_18; uint8_t x_19;
x_18 = lean_ctor_get(x_13, 0);
lean_dec(x_18);
x_19 = !lean_is_exclusive(x_14);
if (x_19 == 0)
lean_object* x_19; uint8_t x_20;
x_19 = lean_ctor_get(x_14, 0);
lean_dec(x_19);
x_20 = !lean_is_exclusive(x_15);
if (x_20 == 0)
{
lean_object* x_20; lean_object* x_21; lean_object* x_22;
x_20 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_20, 0, x_14);
x_21 = lean_box(0);
x_22 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_22, 0, x_20);
lean_ctor_set(x_22, 1, x_21);
lean_ctor_set(x_13, 0, x_22);
return x_13;
lean_object* x_21; lean_object* x_22; lean_object* x_23;
x_21 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_21, 0, x_15);
x_22 = lean_box(0);
x_23 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_23, 0, x_21);
lean_ctor_set(x_23, 1, x_22);
lean_ctor_set(x_14, 0, x_23);
return x_14;
}
else
{
lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27;
x_23 = lean_ctor_get(x_14, 0);
lean_inc(x_23);
lean_dec(x_14);
x_24 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_24, 0, x_23);
lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28;
x_24 = lean_ctor_get(x_15, 0);
lean_inc(x_24);
lean_dec(x_15);
x_25 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_25, 0, x_24);
x_26 = lean_box(0);
x_27 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_27, 0, x_25);
lean_ctor_set(x_27, 1, x_26);
lean_ctor_set(x_13, 0, x_27);
return x_13;
x_26 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_26, 0, x_25);
x_27 = lean_box(0);
x_28 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_28, 0, x_26);
lean_ctor_set(x_28, 1, x_27);
lean_ctor_set(x_14, 0, x_28);
return x_14;
}
}
else
{
lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35;
x_28 = lean_ctor_get(x_13, 1);
lean_inc(x_28);
lean_dec(x_13);
x_29 = lean_ctor_get(x_14, 0);
lean_object* x_29; lean_object* 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;
x_29 = lean_ctor_get(x_14, 1);
lean_inc(x_29);
if (lean_is_exclusive(x_14)) {
lean_ctor_release(x_14, 0);
x_30 = x_14;
lean_dec(x_14);
x_30 = lean_ctor_get(x_15, 0);
lean_inc(x_30);
if (lean_is_exclusive(x_15)) {
lean_ctor_release(x_15, 0);
x_31 = x_15;
} else {
lean_dec_ref(x_14);
x_30 = lean_box(0);
lean_dec_ref(x_15);
x_31 = lean_box(0);
}
if (lean_is_scalar(x_30)) {
x_31 = lean_alloc_ctor(1, 1, 0);
if (lean_is_scalar(x_31)) {
x_32 = lean_alloc_ctor(1, 1, 0);
} else {
x_31 = x_30;
x_32 = x_31;
}
lean_ctor_set(x_31, 0, x_29);
x_32 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_32, 0, x_31);
x_33 = lean_box(0);
x_34 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_34, 0, x_32);
lean_ctor_set(x_34, 1, x_33);
lean_ctor_set(x_32, 0, x_30);
x_33 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_33, 0, x_32);
x_34 = lean_box(0);
x_35 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_35, 0, x_34);
lean_ctor_set(x_35, 1, x_28);
return x_35;
lean_ctor_set(x_35, 0, x_33);
lean_ctor_set(x_35, 1, x_34);
x_36 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_36, 0, x_35);
lean_ctor_set(x_36, 1, x_29);
return x_36;
}
}
}
else
{
uint8_t x_36;
uint8_t x_37;
lean_dec(x_12);
lean_dec(x_8);
lean_dec(x_7);
@ -5020,23 +5052,23 @@ lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_2);
lean_dec(x_1);
x_36 = !lean_is_exclusive(x_13);
if (x_36 == 0)
x_37 = !lean_is_exclusive(x_14);
if (x_37 == 0)
{
return x_13;
return x_14;
}
else
{
lean_object* x_37; lean_object* x_38; lean_object* x_39;
x_37 = lean_ctor_get(x_13, 0);
x_38 = lean_ctor_get(x_13, 1);
lean_object* x_38; lean_object* x_39; lean_object* x_40;
x_38 = lean_ctor_get(x_14, 0);
x_39 = lean_ctor_get(x_14, 1);
lean_inc(x_39);
lean_inc(x_38);
lean_inc(x_37);
lean_dec(x_13);
x_39 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_39, 0, x_37);
lean_ctor_set(x_39, 1, x_38);
return x_39;
lean_dec(x_14);
x_40 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_40, 0, x_38);
lean_ctor_set(x_40, 1, x_39);
return x_40;
}
}
}

3357
stage0/stdlib/Lean/Meta/Instances.c generated
View file

File diff suppressed because it is too large Load diff

618
stage0/stdlib/Lean/Meta/Match/CaseArraySizes.c generated
View file

@ -17,11 +17,9 @@ lean_object* l_Lean_Meta_CaseArraySizesSubgoal_subst___default;
size_t l_USize_add(size_t, size_t);
lean_object* l_Lean_Expr_mvarId_x21(lean_object*);
lean_object* l_Lean_stringToMessageData(lean_object*);
lean_object* l_Lean_Meta_caseArraySizes___closed__2;
lean_object* l___private_Lean_Meta_AppBuilder_0__Lean_Meta_mkEqImp(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_mk_empty_array_with_capacity(lean_object*);
lean_object* l_Lean_Meta_mkForallFVarsImp(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_caseArraySizes___closed__3;
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* lean_array_uget(lean_object*, size_t);
lean_object* l___private_Lean_Meta_Match_CaseArraySizes_0__Lean_Meta_introArrayLit_loop___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -31,7 +29,9 @@ lean_object* l_Lean_Meta_inferType___at___private_Lean_Meta_InferType_0__Lean_Me
extern lean_object* l_Array_myMacro____x40_Init_Data_Array_Subarray___hyg_1011____closed__10;
lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_withLocalDeclImp___rarg(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Array_empty___closed__1;
lean_object* l_Lean_Meta_caseArraySizes___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_getMVarTag(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_caseArraySizes___lambda__1___closed__2;
lean_object* l_Lean_Meta_caseArraySizes_match__6___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Meta_CaseArraySizesSubgoal_elems___default;
extern lean_object* l_Lean_Literal_type___closed__3;
@ -40,6 +40,7 @@ lean_object* lean_array_get_size(lean_object*);
lean_object* l_ReaderT_bind___at_Lean_Meta_instMonadLCtxMetaM___spec__2___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_mapIdxM_map___at_Lean_Meta_caseArraySizes___spec__3___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Meta_Match_CaseArraySizes_0__Lean_Meta_mkArrayGetLit___closed__2;
lean_object* l_Lean_Meta_caseArraySizes___lambda__1___closed__1;
lean_object* l_Lean_throwError___at_Lean_Meta_initFn____x40_Lean_Meta_Basic___hyg_1019____spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_mkDecide___at_Lean_Meta_mkDecideProof___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Expr_appArg_x21(lean_object*);
@ -112,9 +113,10 @@ lean_object* l___private_Lean_Meta_AppBuilder_0__Lean_Meta_mkListLitImp(lean_obj
lean_object* l_Lean_Meta_caseArraySizes_match__3(lean_object*);
lean_object* l___private_Lean_Meta_Match_CaseArraySizes_0__Lean_Meta_introArrayLit(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_caseValues(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_caseArraySizes___closed__1;
extern lean_object* l_Lean_instInhabitedName;
lean_object* l___private_Lean_Meta_AppBuilder_0__Lean_Meta_mkExpectedTypeHintImp(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_caseArraySizes___lambda__1___closed__3;
lean_object* l_Lean_Meta_caseArraySizes___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_getArrayArgType___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_caseArraySizes_match__1(lean_object*);
lean_object* l_Array_mapMUnsafe_map___at_Lean_Meta_caseArraySizes___spec__1___boxed(lean_object*, lean_object*, lean_object*);
@ -2234,7 +2236,7 @@ return x_85;
}
}
}
static lean_object* _init_l_Lean_Meta_caseArraySizes___closed__1() {
static lean_object* _init_l_Lean_Meta_caseArraySizes___lambda__1___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
@ -2244,7 +2246,7 @@ x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Meta_caseArraySizes___closed__2() {
static lean_object* _init_l_Lean_Meta_caseArraySizes___lambda__1___closed__2() {
_start:
{
lean_object* x_1;
@ -2252,323 +2254,300 @@ x_1 = lean_mk_string("aSize");
return x_1;
}
}
static lean_object* _init_l_Lean_Meta_caseArraySizes___closed__3() {
static lean_object* _init_l_Lean_Meta_caseArraySizes___lambda__1___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_Meta_caseArraySizes___closed__2;
x_2 = l_Lean_Meta_caseArraySizes___lambda__1___closed__2;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
lean_object* l_Lean_Meta_caseArraySizes___lambda__1(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, lean_object* x_8, lean_object* x_9, lean_object* x_10, lean_object* x_11) {
_start:
{
lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15;
x_12 = l_Lean_mkOptionalNode___closed__2;
lean_inc(x_1);
x_13 = lean_array_push(x_12, x_1);
x_14 = l_Lean_Meta_caseArraySizes___lambda__1___closed__1;
lean_inc(x_10);
lean_inc(x_9);
lean_inc(x_8);
lean_inc(x_7);
x_15 = l_Lean_Meta_mkAppM___at_Lean_Meta_mkDecideProof___spec__6(x_14, x_13, x_7, x_8, x_9, x_10, x_11);
if (lean_obj_tag(x_15) == 0)
{
lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21;
x_16 = lean_ctor_get(x_15, 0);
lean_inc(x_16);
x_17 = lean_ctor_get(x_15, 1);
lean_inc(x_17);
lean_dec(x_15);
x_18 = l_Lean_Meta_caseArraySizes___lambda__1___closed__3;
x_19 = l_Lean_Literal_type___closed__3;
x_20 = l_Lean_Meta_caseValue___closed__2;
lean_inc(x_10);
lean_inc(x_9);
lean_inc(x_8);
lean_inc(x_7);
x_21 = l_Lean_Meta_assertExt(x_2, x_18, x_19, x_16, x_20, x_7, x_8, x_9, x_10, x_17);
if (lean_obj_tag(x_21) == 0)
{
lean_object* x_22; lean_object* x_23; uint8_t x_24; lean_object* x_25;
x_22 = lean_ctor_get(x_21, 0);
lean_inc(x_22);
x_23 = lean_ctor_get(x_21, 1);
lean_inc(x_23);
lean_dec(x_21);
x_24 = 0;
lean_inc(x_10);
lean_inc(x_9);
lean_inc(x_8);
lean_inc(x_7);
x_25 = l_Lean_Meta_intro1Core(x_22, x_24, x_7, x_8, x_9, x_10, x_23);
if (lean_obj_tag(x_25) == 0)
{
lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30;
x_26 = lean_ctor_get(x_25, 0);
lean_inc(x_26);
x_27 = lean_ctor_get(x_25, 1);
lean_inc(x_27);
lean_dec(x_25);
x_28 = lean_ctor_get(x_26, 0);
lean_inc(x_28);
x_29 = lean_ctor_get(x_26, 1);
lean_inc(x_29);
lean_dec(x_26);
lean_inc(x_10);
lean_inc(x_9);
lean_inc(x_8);
lean_inc(x_7);
x_30 = l_Lean_Meta_intro1Core(x_29, x_24, x_7, x_8, x_9, x_10, x_27);
if (lean_obj_tag(x_30) == 0)
{
lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35; size_t x_36; size_t x_37; lean_object* x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41;
x_31 = lean_ctor_get(x_30, 0);
lean_inc(x_31);
x_32 = lean_ctor_get(x_30, 1);
lean_inc(x_32);
lean_dec(x_30);
x_33 = lean_ctor_get(x_31, 0);
lean_inc(x_33);
x_34 = lean_ctor_get(x_31, 1);
lean_inc(x_34);
lean_dec(x_31);
x_35 = lean_array_get_size(x_3);
x_36 = lean_usize_of_nat(x_35);
x_37 = 0;
lean_inc(x_3);
x_38 = x_3;
x_39 = l_Array_mapMUnsafe_map___at_Lean_Meta_caseArraySizes___spec__1(x_36, x_37, x_38);
x_40 = x_39;
lean_inc(x_10);
lean_inc(x_9);
lean_inc(x_8);
lean_inc(x_7);
lean_inc(x_28);
x_41 = l_Lean_Meta_caseValues(x_34, x_28, x_40, x_4, x_7, x_8, x_9, x_10, x_32);
if (lean_obj_tag(x_41) == 0)
{
lean_object* x_42; lean_object* x_43; lean_object* x_44; lean_object* x_45; lean_object* x_46; lean_object* x_47;
x_42 = lean_ctor_get(x_41, 0);
lean_inc(x_42);
x_43 = lean_ctor_get(x_41, 1);
lean_inc(x_43);
lean_dec(x_41);
x_44 = lean_array_get_size(x_42);
x_45 = lean_mk_empty_array_with_capacity(x_44);
x_46 = lean_unsigned_to_nat(0u);
x_47 = l_Array_mapIdxM_map___at_Lean_Meta_caseArraySizes___spec__3(x_3, x_5, x_1, x_28, x_33, x_35, x_37, x_42, x_42, x_44, x_46, lean_box(0), x_45, x_7, x_8, x_9, x_10, x_43);
lean_dec(x_42);
lean_dec(x_35);
lean_dec(x_3);
return x_47;
}
else
{
uint8_t x_48;
lean_dec(x_35);
lean_dec(x_33);
lean_dec(x_28);
lean_dec(x_10);
lean_dec(x_9);
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_5);
lean_dec(x_3);
lean_dec(x_1);
x_48 = !lean_is_exclusive(x_41);
if (x_48 == 0)
{
return x_41;
}
else
{
lean_object* x_49; lean_object* x_50; lean_object* x_51;
x_49 = lean_ctor_get(x_41, 0);
x_50 = lean_ctor_get(x_41, 1);
lean_inc(x_50);
lean_inc(x_49);
lean_dec(x_41);
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_28);
lean_dec(x_10);
lean_dec(x_9);
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_1);
x_52 = !lean_is_exclusive(x_30);
if (x_52 == 0)
{
return x_30;
}
else
{
lean_object* x_53; lean_object* x_54; lean_object* x_55;
x_53 = lean_ctor_get(x_30, 0);
x_54 = lean_ctor_get(x_30, 1);
lean_inc(x_54);
lean_inc(x_53);
lean_dec(x_30);
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;
}
}
}
else
{
uint8_t x_56;
lean_dec(x_10);
lean_dec(x_9);
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_1);
x_56 = !lean_is_exclusive(x_25);
if (x_56 == 0)
{
return x_25;
}
else
{
lean_object* x_57; lean_object* x_58; lean_object* x_59;
x_57 = lean_ctor_get(x_25, 0);
x_58 = lean_ctor_get(x_25, 1);
lean_inc(x_58);
lean_inc(x_57);
lean_dec(x_25);
x_59 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_59, 0, x_57);
lean_ctor_set(x_59, 1, x_58);
return x_59;
}
}
}
else
{
uint8_t x_60;
lean_dec(x_10);
lean_dec(x_9);
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_1);
x_60 = !lean_is_exclusive(x_21);
if (x_60 == 0)
{
return x_21;
}
else
{
lean_object* x_61; lean_object* x_62; lean_object* x_63;
x_61 = lean_ctor_get(x_21, 0);
x_62 = lean_ctor_get(x_21, 1);
lean_inc(x_62);
lean_inc(x_61);
lean_dec(x_21);
x_63 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_63, 0, x_61);
lean_ctor_set(x_63, 1, x_62);
return x_63;
}
}
}
else
{
uint8_t x_64;
lean_dec(x_10);
lean_dec(x_9);
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
lean_dec(x_1);
x_64 = !lean_is_exclusive(x_15);
if (x_64 == 0)
{
return x_15;
}
else
{
lean_object* x_65; lean_object* x_66; lean_object* x_67;
x_65 = lean_ctor_get(x_15, 0);
x_66 = lean_ctor_get(x_15, 1);
lean_inc(x_66);
lean_inc(x_65);
lean_dec(x_15);
x_67 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_67, 0, x_65);
lean_ctor_set(x_67, 1, x_66);
return x_67;
}
}
}
}
lean_object* l_Lean_Meta_caseArraySizes(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, lean_object* x_8, lean_object* x_9, lean_object* x_10) {
_start:
{
lean_object* x_11; lean_object* x_12;
lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15;
x_11 = l_Lean_mkFVar(x_2);
lean_inc(x_9);
lean_inc(x_8);
lean_inc(x_7);
lean_inc(x_6);
lean_inc(x_11);
x_12 = l_Lean_Meta_getArrayArgType(x_11, x_6, x_7, x_8, x_9, x_10);
if (lean_obj_tag(x_12) == 0)
{
lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17;
x_13 = lean_ctor_get(x_12, 1);
lean_inc(x_13);
lean_dec(x_12);
x_14 = l_Lean_mkOptionalNode___closed__2;
lean_inc(x_11);
x_15 = lean_array_push(x_14, x_11);
x_16 = l_Lean_Meta_caseArraySizes___closed__1;
lean_inc(x_9);
lean_inc(x_8);
lean_inc(x_7);
lean_inc(x_6);
x_17 = l_Lean_Meta_mkAppM___at_Lean_Meta_mkDecideProof___spec__6(x_16, x_15, x_6, x_7, x_8, x_9, x_13);
if (lean_obj_tag(x_17) == 0)
{
lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23;
x_18 = lean_ctor_get(x_17, 0);
lean_inc(x_18);
x_19 = lean_ctor_get(x_17, 1);
lean_inc(x_19);
lean_dec(x_17);
x_20 = l_Lean_Meta_caseArraySizes___closed__3;
x_21 = l_Lean_Literal_type___closed__3;
x_22 = l_Lean_Meta_caseValue___closed__2;
lean_inc(x_9);
lean_inc(x_8);
lean_inc(x_7);
lean_inc(x_6);
x_23 = l_Lean_Meta_assertExt(x_1, x_20, x_21, x_18, x_22, x_6, x_7, x_8, x_9, x_19);
if (lean_obj_tag(x_23) == 0)
{
lean_object* x_24; lean_object* x_25; uint8_t x_26; lean_object* x_27;
x_24 = lean_ctor_get(x_23, 0);
lean_inc(x_24);
x_25 = lean_ctor_get(x_23, 1);
lean_inc(x_25);
lean_dec(x_23);
x_26 = 0;
lean_inc(x_9);
lean_inc(x_8);
lean_inc(x_7);
lean_inc(x_6);
x_27 = l_Lean_Meta_intro1Core(x_24, x_26, x_6, x_7, x_8, x_9, x_25);
if (lean_obj_tag(x_27) == 0)
{
lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32;
x_28 = lean_ctor_get(x_27, 0);
lean_inc(x_28);
x_29 = lean_ctor_get(x_27, 1);
lean_inc(x_29);
lean_dec(x_27);
x_30 = lean_ctor_get(x_28, 0);
lean_inc(x_30);
x_31 = lean_ctor_get(x_28, 1);
lean_inc(x_31);
lean_dec(x_28);
lean_inc(x_9);
lean_inc(x_8);
lean_inc(x_7);
lean_inc(x_6);
x_32 = l_Lean_Meta_intro1Core(x_31, x_26, x_6, x_7, x_8, x_9, x_29);
if (lean_obj_tag(x_32) == 0)
{
lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36; lean_object* x_37; size_t x_38; size_t x_39; lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43;
x_33 = lean_ctor_get(x_32, 0);
lean_inc(x_33);
x_34 = lean_ctor_get(x_32, 1);
lean_inc(x_34);
lean_dec(x_32);
x_35 = lean_ctor_get(x_33, 0);
lean_inc(x_35);
x_36 = lean_ctor_get(x_33, 1);
lean_inc(x_36);
lean_dec(x_33);
x_37 = lean_array_get_size(x_3);
x_38 = lean_usize_of_nat(x_37);
x_39 = 0;
lean_inc(x_3);
x_40 = x_3;
x_41 = l_Array_mapMUnsafe_map___at_Lean_Meta_caseArraySizes___spec__1(x_38, x_39, x_40);
x_42 = x_41;
lean_inc(x_9);
lean_inc(x_8);
lean_inc(x_7);
lean_inc(x_6);
lean_inc(x_30);
x_43 = l_Lean_Meta_caseValues(x_36, x_30, x_42, x_5, x_6, x_7, x_8, x_9, x_34);
if (lean_obj_tag(x_43) == 0)
{
lean_object* x_44; lean_object* x_45; lean_object* x_46; lean_object* x_47; lean_object* x_48; lean_object* x_49;
x_44 = lean_ctor_get(x_43, 0);
lean_inc(x_44);
x_45 = lean_ctor_get(x_43, 1);
lean_inc(x_45);
lean_dec(x_43);
x_46 = lean_array_get_size(x_44);
x_47 = lean_mk_empty_array_with_capacity(x_46);
x_48 = lean_unsigned_to_nat(0u);
x_49 = l_Array_mapIdxM_map___at_Lean_Meta_caseArraySizes___spec__3(x_3, x_4, x_11, x_30, x_35, x_37, x_39, x_44, x_44, x_46, x_48, lean_box(0), x_47, x_6, x_7, x_8, x_9, x_45);
lean_dec(x_44);
lean_dec(x_37);
lean_dec(x_3);
return x_49;
}
else
{
uint8_t x_50;
lean_dec(x_37);
lean_dec(x_35);
lean_dec(x_30);
lean_dec(x_11);
lean_dec(x_9);
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_4);
lean_dec(x_3);
x_50 = !lean_is_exclusive(x_43);
if (x_50 == 0)
{
return x_43;
}
else
{
lean_object* x_51; lean_object* x_52; lean_object* x_53;
x_51 = lean_ctor_get(x_43, 0);
x_52 = lean_ctor_get(x_43, 1);
lean_inc(x_52);
lean_inc(x_51);
lean_dec(x_43);
x_53 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_53, 0, x_51);
lean_ctor_set(x_53, 1, x_52);
return x_53;
}
}
}
else
{
uint8_t x_54;
lean_dec(x_30);
lean_dec(x_11);
lean_dec(x_9);
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
x_54 = !lean_is_exclusive(x_32);
if (x_54 == 0)
{
return x_32;
}
else
{
lean_object* x_55; lean_object* x_56; lean_object* x_57;
x_55 = lean_ctor_get(x_32, 0);
x_56 = lean_ctor_get(x_32, 1);
lean_inc(x_56);
lean_inc(x_55);
lean_dec(x_32);
x_57 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_57, 0, x_55);
lean_ctor_set(x_57, 1, x_56);
return x_57;
}
}
}
else
{
uint8_t x_58;
lean_dec(x_11);
lean_dec(x_9);
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
x_58 = !lean_is_exclusive(x_27);
if (x_58 == 0)
{
return x_27;
}
else
{
lean_object* x_59; lean_object* x_60; lean_object* x_61;
x_59 = lean_ctor_get(x_27, 0);
x_60 = lean_ctor_get(x_27, 1);
lean_inc(x_60);
lean_inc(x_59);
lean_dec(x_27);
x_61 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_61, 0, x_59);
lean_ctor_set(x_61, 1, x_60);
return x_61;
}
}
}
else
{
uint8_t x_62;
lean_dec(x_11);
lean_dec(x_9);
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
x_62 = !lean_is_exclusive(x_23);
if (x_62 == 0)
{
return x_23;
}
else
{
lean_object* x_63; lean_object* x_64; lean_object* x_65;
x_63 = lean_ctor_get(x_23, 0);
x_64 = lean_ctor_get(x_23, 1);
lean_inc(x_64);
lean_inc(x_63);
lean_dec(x_23);
x_65 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_65, 0, x_63);
lean_ctor_set(x_65, 1, x_64);
return x_65;
}
}
}
else
{
uint8_t x_66;
lean_dec(x_11);
lean_dec(x_9);
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_1);
x_66 = !lean_is_exclusive(x_17);
if (x_66 == 0)
{
return x_17;
}
else
{
lean_object* x_67; lean_object* x_68; lean_object* x_69;
x_67 = lean_ctor_get(x_17, 0);
x_68 = lean_ctor_get(x_17, 1);
lean_inc(x_68);
lean_inc(x_67);
lean_dec(x_17);
x_69 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_69, 0, x_67);
lean_ctor_set(x_69, 1, x_68);
return x_69;
}
}
}
else
{
uint8_t x_70;
lean_dec(x_11);
lean_dec(x_9);
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_1);
x_70 = !lean_is_exclusive(x_12);
if (x_70 == 0)
{
return x_12;
}
else
{
lean_object* x_71; lean_object* x_72; lean_object* x_73;
x_71 = lean_ctor_get(x_12, 0);
x_72 = lean_ctor_get(x_12, 1);
lean_inc(x_72);
lean_inc(x_71);
lean_dec(x_12);
x_73 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_73, 0, x_71);
lean_ctor_set(x_73, 1, x_72);
return x_73;
}
}
x_12 = lean_alloc_closure((void*)(l_Lean_Meta_getArrayArgType), 6, 1);
lean_closure_set(x_12, 0, x_11);
lean_inc(x_1);
x_13 = lean_alloc_closure((void*)(l_Lean_Meta_caseArraySizes___lambda__1___boxed), 11, 5);
lean_closure_set(x_13, 0, x_11);
lean_closure_set(x_13, 1, x_1);
lean_closure_set(x_13, 2, x_3);
lean_closure_set(x_13, 3, x_5);
lean_closure_set(x_13, 4, x_4);
x_14 = lean_alloc_closure((void*)(l_ReaderT_bind___at_Lean_Meta_instMonadLCtxMetaM___spec__2___rarg), 7, 2);
lean_closure_set(x_14, 0, x_12);
lean_closure_set(x_14, 1, x_13);
x_15 = l_Lean_Meta_withMVarContext___at_Lean_Meta_admit___spec__2___rarg(x_1, x_14, x_6, x_7, x_8, x_9, x_10);
return x_15;
}
}
lean_object* l_Array_mapMUnsafe_map___at_Lean_Meta_caseArraySizes___spec__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
@ -2628,6 +2607,15 @@ lean_dec(x_1);
return x_20;
}
}
lean_object* l_Lean_Meta_caseArraySizes___lambda__1___boxed(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, lean_object* x_8, lean_object* x_9, lean_object* x_10, lean_object* x_11) {
_start:
{
lean_object* x_12;
x_12 = l_Lean_Meta_caseArraySizes___lambda__1(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11);
lean_dec(x_6);
return x_12;
}
}
lean_object* initialize_Init(lean_object*);
lean_object* initialize_Lean_Meta_Tactic_Assert(lean_object*);
lean_object* initialize_Lean_Meta_Match_CaseValues(lean_object*);
@ -2673,12 +2661,12 @@ l___private_Lean_Meta_Match_CaseArraySizes_0__Lean_Meta_introArrayLit_loop___clo
lean_mark_persistent(l___private_Lean_Meta_Match_CaseArraySizes_0__Lean_Meta_introArrayLit_loop___closed__4);
l___private_Lean_Meta_Match_CaseArraySizes_0__Lean_Meta_introArrayLit_loop___closed__5 = _init_l___private_Lean_Meta_Match_CaseArraySizes_0__Lean_Meta_introArrayLit_loop___closed__5();
lean_mark_persistent(l___private_Lean_Meta_Match_CaseArraySizes_0__Lean_Meta_introArrayLit_loop___closed__5);
l_Lean_Meta_caseArraySizes___closed__1 = _init_l_Lean_Meta_caseArraySizes___closed__1();
lean_mark_persistent(l_Lean_Meta_caseArraySizes___closed__1);
l_Lean_Meta_caseArraySizes___closed__2 = _init_l_Lean_Meta_caseArraySizes___closed__2();
lean_mark_persistent(l_Lean_Meta_caseArraySizes___closed__2);
l_Lean_Meta_caseArraySizes___closed__3 = _init_l_Lean_Meta_caseArraySizes___closed__3();
lean_mark_persistent(l_Lean_Meta_caseArraySizes___closed__3);
l_Lean_Meta_caseArraySizes___lambda__1___closed__1 = _init_l_Lean_Meta_caseArraySizes___lambda__1___closed__1();
lean_mark_persistent(l_Lean_Meta_caseArraySizes___lambda__1___closed__1);
l_Lean_Meta_caseArraySizes___lambda__1___closed__2 = _init_l_Lean_Meta_caseArraySizes___lambda__1___closed__2();
lean_mark_persistent(l_Lean_Meta_caseArraySizes___lambda__1___closed__2);
l_Lean_Meta_caseArraySizes___lambda__1___closed__3 = _init_l_Lean_Meta_caseArraySizes___lambda__1___closed__3();
lean_mark_persistent(l_Lean_Meta_caseArraySizes___lambda__1___closed__3);
return lean_io_result_mk_ok(lean_box(0));
}
#ifdef __cplusplus

869
stage0/stdlib/Lean/Meta/Match/Match.c generated
View file

File diff suppressed because it is too large Load diff

1586
stage0/stdlib/Lean/Parser/Transform.c generated Normal file
View file

File diff suppressed because it is too large Load diff

10
stage0/stdlib/Lean/PrettyPrinter.c generated
View file

@ -1,6 +1,6 @@
// Lean compiler output
// Module: Lean.PrettyPrinter
// Imports: Init Lean.Delaborator Lean.PrettyPrinter.Parenthesizer Lean.PrettyPrinter.Formatter Lean.Parser.Module Lean.ParserCompiler
// Imports: Init Lean.PrettyPrinter.Delaborator Lean.PrettyPrinter.Parenthesizer Lean.PrettyPrinter.Formatter Lean.Parser.Module Lean.ParserCompiler
#include <lean/lean.h>
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
@ -79,7 +79,7 @@ extern lean_object* l_Lean_NameSet_empty;
lean_object* l_Lean_PPContext_runCoreM___rarg___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_PrettyPrinter_0__Lean_PrettyPrinter_withoutContext_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_PrettyPrinter_0__Lean_PrettyPrinter_withoutContext_match__1(lean_object*);
lean_object* l_Lean_delab(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_PrettyPrinter_delab(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_PrettyPrinter_formatCommand(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_PrettyPrinter_ppModule___closed__2;
lean_object* l_Lean_PPContext_runCoreM(lean_object*);
@ -437,7 +437,7 @@ x_13 = l_Lean_LocalContext_sanitizeNames(x_9, x_12);
x_14 = lean_ctor_get(x_13, 0);
lean_inc(x_14);
lean_dec(x_13);
x_15 = lean_alloc_closure((void*)(l_Lean_delab), 9, 4);
x_15 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_delab), 9, 4);
lean_closure_set(x_15, 0, x_1);
lean_closure_set(x_15, 1, x_2);
lean_closure_set(x_15, 2, x_3);
@ -1653,7 +1653,7 @@ return x_6;
}
}
lean_object* initialize_Init(lean_object*);
lean_object* initialize_Lean_Delaborator(lean_object*);
lean_object* initialize_Lean_PrettyPrinter_Delaborator(lean_object*);
lean_object* initialize_Lean_PrettyPrinter_Parenthesizer(lean_object*);
lean_object* initialize_Lean_PrettyPrinter_Formatter(lean_object*);
lean_object* initialize_Lean_Parser_Module(lean_object*);
@ -1666,7 +1666,7 @@ _G_initialized = true;
res = initialize_Init(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Lean_Delaborator(lean_io_mk_world());
res = initialize_Lean_PrettyPrinter_Delaborator(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Lean_PrettyPrinter_Parenthesizer(lean_io_mk_world());

37
stage0/stdlib/Lean/PrettyPrinter/Delaborator.c generated Normal file
View file

@ -0,0 +1,37 @@
// Lean compiler output
// Module: Lean.PrettyPrinter.Delaborator
// Imports: Init Lean.PrettyPrinter.Delaborator.Basic Lean.PrettyPrinter.Delaborator.Builtins
#include <lean/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* initialize_Init(lean_object*);
lean_object* initialize_Lean_PrettyPrinter_Delaborator_Basic(lean_object*);
lean_object* initialize_Lean_PrettyPrinter_Delaborator_Builtins(lean_object*);
static bool _G_initialized = false;
lean_object* initialize_Lean_PrettyPrinter_Delaborator(lean_object* w) {
lean_object * res;
if (_G_initialized) return lean_io_result_mk_ok(lean_box(0));
_G_initialized = true;
res = initialize_Init(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Lean_PrettyPrinter_Delaborator_Basic(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Lean_PrettyPrinter_Delaborator_Builtins(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
return lean_io_result_mk_ok(lean_box(0));
}
#ifdef __cplusplus
}
#endif

10647
stage0/stdlib/Lean/PrettyPrinter/Delaborator/Basic.c generated Normal file
View file

File diff suppressed because it is too large Load diff

26931
stage0/stdlib/Lean/PrettyPrinter/Delaborator/Builtins.c generated Normal file
View file

File diff suppressed because it is too large Load diff

330
stage0/stdlib/Lean/Server/ServerBin.c generated Normal file
View file

@ -0,0 +1,330 @@
// Lean compiler output
// Module: Lean.Server.ServerBin
// Imports: Init Init.System.IO Lean.Server
#include <lean/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* lean_get_stdin(lean_object*);
lean_object* lean_io_error_to_string(lean_object*);
lean_object* _lean_main(lean_object*, lean_object*);
lean_object* lean_get_stderr(lean_object*);
lean_object* l_main___boxed__const__1;
lean_object* l_IO_getStdin___at_main___spec__1(lean_object*);
lean_object* lean_init_search_path(lean_object*, lean_object*);
lean_object* lean_get_stdout(lean_object*);
lean_object* l_IO_FS_Stream_putStrLn___at_Lean_Server_Test_runWithInputFile___spec__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Server_initAndRunServer(lean_object*, lean_object*, lean_object*);
lean_object* l_IO_getStdin___at_main___spec__1(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_get_stdin(x_1);
return x_2;
}
}
static lean_object* _init_l_main___boxed__const__1() {
_start:
{
uint32_t x_1; lean_object* x_2;
x_1 = 0;
x_2 = lean_box_uint32(x_1);
return x_2;
}
}
lean_object* _lean_main(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
lean_dec(x_1);
x_3 = lean_get_stdin(x_2);
if (lean_obj_tag(x_3) == 0)
{
lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_4 = lean_ctor_get(x_3, 0);
lean_inc(x_4);
x_5 = lean_ctor_get(x_3, 1);
lean_inc(x_5);
lean_dec(x_3);
x_6 = lean_get_stdout(x_5);
if (lean_obj_tag(x_6) == 0)
{
lean_object* x_7; lean_object* x_8; lean_object* x_9;
x_7 = lean_ctor_get(x_6, 0);
lean_inc(x_7);
x_8 = lean_ctor_get(x_6, 1);
lean_inc(x_8);
lean_dec(x_6);
x_9 = lean_get_stderr(x_8);
if (lean_obj_tag(x_9) == 0)
{
lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13;
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 = lean_box(0);
x_13 = lean_init_search_path(x_12, x_11);
if (lean_obj_tag(x_13) == 0)
{
lean_object* x_14; lean_object* x_15;
x_14 = lean_ctor_get(x_13, 1);
lean_inc(x_14);
lean_dec(x_13);
x_15 = l_Lean_Server_initAndRunServer(x_4, x_7, x_14);
if (lean_obj_tag(x_15) == 0)
{
uint8_t x_16;
lean_dec(x_10);
x_16 = !lean_is_exclusive(x_15);
if (x_16 == 0)
{
lean_object* x_17; lean_object* x_18;
x_17 = lean_ctor_get(x_15, 0);
lean_dec(x_17);
x_18 = l_main___boxed__const__1;
lean_ctor_set(x_15, 0, x_18);
return x_15;
}
else
{
lean_object* x_19; lean_object* x_20; lean_object* x_21;
x_19 = lean_ctor_get(x_15, 1);
lean_inc(x_19);
lean_dec(x_15);
x_20 = l_main___boxed__const__1;
x_21 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_21, 0, x_20);
lean_ctor_set(x_21, 1, x_19);
return x_21;
}
}
else
{
lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25;
x_22 = lean_ctor_get(x_15, 0);
lean_inc(x_22);
x_23 = lean_ctor_get(x_15, 1);
lean_inc(x_23);
lean_dec(x_15);
x_24 = lean_io_error_to_string(x_22);
x_25 = l_IO_FS_Stream_putStrLn___at_Lean_Server_Test_runWithInputFile___spec__1(x_10, x_24, x_23);
if (lean_obj_tag(x_25) == 0)
{
uint8_t x_26;
x_26 = !lean_is_exclusive(x_25);
if (x_26 == 0)
{
lean_object* x_27; lean_object* x_28;
x_27 = lean_ctor_get(x_25, 0);
lean_dec(x_27);
x_28 = l_main___boxed__const__1;
lean_ctor_set(x_25, 0, x_28);
return x_25;
}
else
{
lean_object* x_29; lean_object* x_30; lean_object* x_31;
x_29 = lean_ctor_get(x_25, 1);
lean_inc(x_29);
lean_dec(x_25);
x_30 = l_main___boxed__const__1;
x_31 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_31, 0, x_30);
lean_ctor_set(x_31, 1, x_29);
return x_31;
}
}
else
{
uint8_t x_32;
x_32 = !lean_is_exclusive(x_25);
if (x_32 == 0)
{
return x_25;
}
else
{
lean_object* x_33; lean_object* x_34; lean_object* x_35;
x_33 = lean_ctor_get(x_25, 0);
x_34 = lean_ctor_get(x_25, 1);
lean_inc(x_34);
lean_inc(x_33);
lean_dec(x_25);
x_35 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_35, 0, x_33);
lean_ctor_set(x_35, 1, x_34);
return x_35;
}
}
}
}
else
{
uint8_t x_36;
lean_dec(x_10);
lean_dec(x_7);
lean_dec(x_4);
x_36 = !lean_is_exclusive(x_13);
if (x_36 == 0)
{
return x_13;
}
else
{
lean_object* x_37; lean_object* x_38; lean_object* x_39;
x_37 = lean_ctor_get(x_13, 0);
x_38 = lean_ctor_get(x_13, 1);
lean_inc(x_38);
lean_inc(x_37);
lean_dec(x_13);
x_39 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_39, 0, x_37);
lean_ctor_set(x_39, 1, x_38);
return x_39;
}
}
}
else
{
uint8_t x_40;
lean_dec(x_7);
lean_dec(x_4);
x_40 = !lean_is_exclusive(x_9);
if (x_40 == 0)
{
return x_9;
}
else
{
lean_object* x_41; lean_object* x_42; lean_object* x_43;
x_41 = lean_ctor_get(x_9, 0);
x_42 = lean_ctor_get(x_9, 1);
lean_inc(x_42);
lean_inc(x_41);
lean_dec(x_9);
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_4);
x_44 = !lean_is_exclusive(x_6);
if (x_44 == 0)
{
return x_6;
}
else
{
lean_object* x_45; lean_object* x_46; lean_object* x_47;
x_45 = lean_ctor_get(x_6, 0);
x_46 = lean_ctor_get(x_6, 1);
lean_inc(x_46);
lean_inc(x_45);
lean_dec(x_6);
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;
}
}
}
else
{
uint8_t x_48;
x_48 = !lean_is_exclusive(x_3);
if (x_48 == 0)
{
return x_3;
}
else
{
lean_object* x_49; lean_object* x_50; lean_object* x_51;
x_49 = lean_ctor_get(x_3, 0);
x_50 = lean_ctor_get(x_3, 1);
lean_inc(x_50);
lean_inc(x_49);
lean_dec(x_3);
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;
}
}
}
}
lean_object* initialize_Init(lean_object*);
lean_object* initialize_Init_System_IO(lean_object*);
lean_object* initialize_Lean_Server(lean_object*);
static bool _G_initialized = false;
lean_object* initialize_Lean_Server_ServerBin(lean_object* w) {
lean_object * res;
if (_G_initialized) return lean_io_result_mk_ok(lean_box(0));
_G_initialized = true;
res = initialize_Init(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_System_IO(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Lean_Server(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_main___boxed__const__1 = _init_l_main___boxed__const__1();
lean_mark_persistent(l_main___boxed__const__1);
return lean_io_result_mk_ok(lean_box(0));
}
void lean_initialize();
#if defined(WIN32) || defined(_WIN32)
#include <windows.h>
#endif
int main(int argc, char ** argv) {
#if defined(WIN32) || defined(_WIN32)
SetErrorMode(SEM_FAILCRITICALERRORS);
#endif
lean_object* in; lean_object* res;
lean_initialize();
res = initialize_Lean_Server_ServerBin(lean_io_mk_world());
lean_io_mark_end_initialization();
if (lean_io_result_is_ok(res)) {
lean_dec_ref(res);
lean_init_task_manager();
in = lean_box(0);
int i = argc;
while (i > 1) {
lean_object* n;
i--;
n = lean_alloc_ctor(1,2,0); lean_ctor_set(n, 0, lean_mk_string(argv[i])); lean_ctor_set(n, 1, in);
in = n;
}
res = _lean_main(in, lean_io_mk_world());
}
if (lean_io_result_is_ok(res)) {
int ret = lean_unbox(lean_io_result_get_value(res));
lean_dec_ref(res);
return ret;
} else {
lean_io_result_show_error(res);
lean_dec_ref(res);
return 1;
}
}
#ifdef __cplusplus
}
#endif