chore: update stage0
This commit is contained in:
Leonardo de Moura
parent
5d3db23d4b
commit
21249b29a9
35 changed files with 32066 additions and 25642 deletions
|
|
@ -12,12 +12,9 @@ universes u v w w'
|
|||
class Coe (α : Sort u) (β : Sort v) :=
|
||||
(coe : α → β)
|
||||
|
||||
class CoeDep (α : Sort u) (a : α) (β : Sort v) :=
|
||||
(coe : β)
|
||||
|
||||
/-- Auxiliary class that contains the transitive closure of `Coe` and `CoeDep`. -/
|
||||
class CoeTC (α : Sort u) (a : α) (β : Sort v) :=
|
||||
(coe : β)
|
||||
/-- Auxiliary class that contains the transitive closure of `Coe`. -/
|
||||
class CoeTC (α : Sort u) (β : Sort v) :=
|
||||
(coe : α → β)
|
||||
|
||||
/- Expensive coercion that can only appear at the beggining of a sequence of coercions. -/
|
||||
class CoeHead (α : Sort u) (β : Sort v) :=
|
||||
|
|
@ -27,61 +24,57 @@ class CoeHead (α : Sort u) (β : Sort v) :=
|
|||
class CoeTail (α : Sort u) (β : Sort v) :=
|
||||
(coe : α → β)
|
||||
|
||||
/- CoeHead + CoeTC + CoeTail -/
|
||||
class CoeDep (α : Sort u) (a : α) (β : Sort v) :=
|
||||
(coe : β)
|
||||
|
||||
/- Combines CoeHead, CoeTC, CoeTail, CoeDep -/
|
||||
class CoeT (α : Sort u) (a : α) (β : Sort v) :=
|
||||
(coe : β)
|
||||
|
||||
class CoeFun (α : Sort u) (a : α) (γ : outParam (Sort v)) :=
|
||||
(coe : γ)
|
||||
class CoeFun (α : Sort u) (γ : outParam (α → outParam (Sort v))) :=
|
||||
(coe : forall (a : α), γ a)
|
||||
|
||||
class CoeSort (α : Sort u) (a : α) (β : outParam (Sort v)) :=
|
||||
(coe : β)
|
||||
class CoeSort (α : Sort u) (β : outParam (Sort v)) :=
|
||||
(coe : α → β)
|
||||
|
||||
abbrev coeB {α : Sort u} {β : Sort v} (a : α) [Coe α β] : β :=
|
||||
abbrev coeB {α : Sort u} {β : Sort v} [Coe α β] (a : α) : β :=
|
||||
@Coe.coe α β _ a
|
||||
|
||||
abbrev coeHead {α : Sort u} {β : Sort v} (a : α) [CoeHead α β] : β :=
|
||||
abbrev coeHead {α : Sort u} {β : Sort v} [CoeHead α β] (a : α) : β :=
|
||||
@CoeHead.coe α β _ a
|
||||
|
||||
abbrev coeTail {α : Sort u} {β : Sort v} (a : α) [CoeTail α β] : β :=
|
||||
abbrev coeTail {α : Sort u} {β : Sort v} [CoeTail α β] (a : α) : β :=
|
||||
@CoeTail.coe α β _ a
|
||||
|
||||
abbrev coeD {α : Sort u} {β : Sort v} (a : α) [CoeDep α a β] : β :=
|
||||
@CoeDep.coe α a β _
|
||||
|
||||
abbrev coeTC {α : Sort u} {β : Sort v} (a : α) [CoeTC α a β] : β :=
|
||||
@CoeTC.coe α a β _
|
||||
abbrev coeTC {α : Sort u} {β : Sort v} [CoeTC α β] (a : α) : β :=
|
||||
@CoeTC.coe α β _ a
|
||||
|
||||
/-- Apply coercion manually. -/
|
||||
abbrev coe {α : Sort u} {β : Sort v} (a : α) [CoeT α a β] : β :=
|
||||
@CoeT.coe α a β _
|
||||
|
||||
abbrev coeFun {α : Sort u} {γ : Sort v} (a : α) [CoeFun α a γ] : γ :=
|
||||
@CoeFun.coe α a γ _
|
||||
abbrev coeFun {α : Sort u} {γ : α → Sort v} (a : α) [CoeFun α γ] : γ a :=
|
||||
@CoeFun.coe α γ _ a
|
||||
|
||||
abbrev coeSort {α : Sort u} {γ : Sort v} (a : α) [CoeSort α a γ] : γ :=
|
||||
@CoeSort.coe α a γ _
|
||||
abbrev coeSort {α : Sort u} {β : Sort v} (a : α) [CoeSort α β] : β :=
|
||||
@CoeSort.coe α β _ a
|
||||
|
||||
instance coeDepTrans {α : Sort u} {β : Sort v} {δ : Sort w} (a : α) [CoeTC α a β] [CoeDep β (coeTC a) δ] : CoeTC α a δ :=
|
||||
{ coe := coeD (coeTC a : β) }
|
||||
instance coeTrans {α : Sort u} {β : Sort v} {δ : Sort w} [CoeTC α β] [Coe β δ] : CoeTC α δ :=
|
||||
{ coe := fun a => coeB (coeTC a : β) }
|
||||
|
||||
instance coeTrans {α : Sort u} {β : Sort v} {δ : Sort w} (a : α) [CoeTC α a β] [Coe β δ] : CoeTC α a δ :=
|
||||
{ coe := coeB (coeTC a : β) }
|
||||
instance coeBase {α : Sort u} {β : Sort v} [Coe α β] : CoeTC α β :=
|
||||
{ coe := fun a => coeB a }
|
||||
|
||||
instance coeBase {α : Sort u} {β : Sort v} (a : α) [Coe α β] : CoeTC α a β :=
|
||||
{ coe := coeB a }
|
||||
|
||||
instance coeDepBase {α : Sort u} {β : Sort v} (a : α) [CoeDep α a β] : CoeTC α a β :=
|
||||
{ coe := coeD a }
|
||||
|
||||
instance coeOfHeafOfTCOfTail {α : Sort u} {β : Sort v} {δ : Sort w} {γ : Sort w'} (a : α) [CoeHead α β] [CoeTC β (coeHead a) δ] [CoeTail δ γ] : CoeT α a γ :=
|
||||
instance coeOfHeafOfTCOfTail {α : Sort u} {β : Sort v} {δ : Sort w} {γ : Sort w'} (a : α) [CoeTC β δ] [CoeTail δ γ] [CoeHead α β] : CoeT α a γ :=
|
||||
{ coe := coeTail (coeTC (coeHead a : β) : δ) }
|
||||
|
||||
@[inferTCGoalsLR]
|
||||
instance coeOfHeadOfTC {α : Sort u} {β : Sort v} {δ : Sort w} (a : α) [CoeHead α β] [CoeTC β (coeHead a) δ] : CoeT α a δ :=
|
||||
instance coeOfHeadOfTC {α : Sort u} {β : Sort v} {δ : Sort w} (a : α) [CoeTC β δ] [CoeHead α β] : CoeT α a δ :=
|
||||
{ coe := coeTC (coeHead a : β) }
|
||||
|
||||
instance coeOfTCOfTail {α : Sort u} {β : Sort v} {δ : Sort w} (a : α) [CoeTC α a β] [CoeTail β δ] : CoeT α a δ :=
|
||||
instance coeOfTCOfTail {α : Sort u} {β : Sort v} {δ : Sort w} (a : α) [CoeTC α β] [CoeTail β δ] : CoeT α a δ :=
|
||||
{ coe := coeTail (coeTC a : β) }
|
||||
|
||||
instance coeOfHead {α : Sort u} {β : Sort v} (a : α) [CoeHead α β] : CoeT α a β :=
|
||||
|
|
@ -90,24 +83,17 @@ instance coeOfHead {α : Sort u} {β : Sort v} (a : α) [CoeHead α β] : CoeT
|
|||
instance coeOfTail {α : Sort u} {β : Sort v} (a : α) [CoeTail α β] : CoeT α a β :=
|
||||
{ coe := coeTail a }
|
||||
|
||||
instance coeOfTC {α : Sort u} {β : Sort v} (a : α) [CoeTC α a β] : CoeT α a β :=
|
||||
instance coeOfTC {α : Sort u} {β : Sort v} (a : α) [CoeTC α β] : CoeT α a β :=
|
||||
{ coe := coeTC a }
|
||||
|
||||
@[inferTCGoalsLR]
|
||||
instance coeFunDepTrans {α : Sort u} {β : Sort v} {γ : Sort w} (a : α) [CoeDep α a β] [CoeFun β (coe a) γ] : CoeFun α a γ :=
|
||||
{ coe := coeFun (coeD a : β) }
|
||||
instance coeOfDep {α : Sort u} {β : Sort v} (a : α) [CoeDep α a β] : CoeT α a β :=
|
||||
{ coe := coeD a }
|
||||
|
||||
@[inferTCGoalsLR]
|
||||
instance coeSortDepTrans {α : Sort u} {β : Sort v} {δ : Sort w} (a : α) [CoeDep α a β] [CoeSort β (coe a) δ] : CoeSort α a δ :=
|
||||
{ coe := coeSort (coeD a : β) }
|
||||
instance coeFunTrans {α : Sort u} {β : Sort v} {γ : β → Sort w} [CoeFun β γ] [Coe α β] : CoeFun α (fun a => γ (coe a)) :=
|
||||
{ coe := fun a => coeFun (coeB a : β) }
|
||||
|
||||
@[inferTCGoalsLR]
|
||||
instance coeFunTrans {α : Sort u} {β : Sort v} {γ : Sort w} (a : α) [Coe α β] [CoeFun β (coe a) γ] : CoeFun α a γ :=
|
||||
{ coe := coeFun (coeB a : β) }
|
||||
|
||||
@[inferTCGoalsLR]
|
||||
instance coeSortTrans {α : Sort u} {β : Sort v} {δ : Sort w} (a : α) [Coe α β] [CoeSort β (coe a) δ] : CoeSort α a δ :=
|
||||
{ coe := coeSort (coeB a : β) }
|
||||
instance coeSortTrans {α : Sort u} {β : Sort v} {δ : Sort w} [CoeSort β δ] [Coe α β] : CoeSort α δ :=
|
||||
{ coe := fun a => coeSort (coeB a : β) }
|
||||
|
||||
/- Basic instances -/
|
||||
|
||||
|
|
@ -131,7 +117,6 @@ instance subtypeCoe {α : Sort u} {p : α → Prop} : CoeHead { x // p x } α :=
|
|||
/-
|
||||
Remark: one may question why we use `HasOfNat α` instead of `Coe Nat α`.
|
||||
Reason: `HasOfNat` is for implementing polymorphic numeric literals, and we may
|
||||
want to have numberic literals for a type α and **no** coercion from `Nat` to `α`.
|
||||
-/
|
||||
instance hasOfNatOfCoe {α : Type u} {β : Type v} [HasOfNat α] [∀ a, CoeTC α a β] : HasOfNat β :=
|
||||
want to have numberic literals for a type α and **no** coercion from `Nat` to `α`. -/
|
||||
instance hasOfNatOfCoe {α : Type u} {β : Type v} [HasOfNat α] [Coe α β] : HasOfNat β :=
|
||||
{ ofNat := fun (n : Nat) => coe (HasOfNat.ofNat α n) }
|
||||
|
|
|
|||
|
|
@ -30,7 +30,7 @@ export HasMonadLiftT (monadLift)
|
|||
|
||||
abbrev liftM := @monadLift
|
||||
|
||||
instance hasMonadLiftTTrans (m n o) [HasMonadLift n o] [HasMonadLiftT m n] : HasMonadLiftT m o :=
|
||||
instance hasMonadLiftTTrans (m n o) [HasMonadLiftT m n] [HasMonadLift n o] : HasMonadLiftT m o :=
|
||||
⟨fun α ma => HasMonadLift.monadLift (monadLift ma : n α)⟩
|
||||
|
||||
instance hasMonadLiftTRefl (m) : HasMonadLiftT m m :=
|
||||
|
|
|
|||
|
|
@ -17,3 +17,4 @@ import Init.Lean.Elab.BuiltinNotation
|
|||
import Init.Lean.Elab.Declaration
|
||||
import Init.Lean.Elab.Tactic
|
||||
import Init.Lean.Elab.Syntax
|
||||
import Init.Lean.Elab.Match
|
||||
|
|
|
|||
|
|
@ -83,7 +83,7 @@ withUsedWhen ref vars xs e dummyExpr cond k
|
|||
def mkDef (view : DefView) (declName : Name) (explictLevelNames : List Name) (vars : Array Expr) (xs : Array Expr) (type : Expr) (val : Expr)
|
||||
: TermElabM (Option Declaration) := do
|
||||
let ref := view.ref;
|
||||
val ← Term.ensureHasType ref type val;
|
||||
val ← Term.ensureHasType view.val type val;
|
||||
Term.synthesizeSyntheticMVars false;
|
||||
type ← Term.instantiateMVars ref type;
|
||||
val ← Term.instantiateMVars view.val val;
|
||||
|
|
|
|||
32
stage0/src/Init/Lean/Elab/Match.lean
Normal file
32
stage0/src/Init/Lean/Elab/Match.lean
Normal file
|
|
@ -0,0 +1,32 @@
|
|||
/-
|
||||
Copyright (c) 2020 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Leonardo de Moura
|
||||
-/
|
||||
prelude
|
||||
import Init.Lean.Elab.Term
|
||||
|
||||
namespace Lean
|
||||
namespace Elab
|
||||
namespace Term
|
||||
|
||||
private def expandSimpleMatch (stx discr lhsVar rhs : Syntax) (expectedType? : Option Expr) : TermElabM Expr := do
|
||||
newStx ← `(let $lhsVar := $discr; $rhs);
|
||||
withMacroExpansion stx newStx $ elabTerm newStx expectedType?
|
||||
|
||||
private def expandSimpleMatchWithType (stx discr lhsVar type rhs : Syntax) (expectedType? : Option Expr) : TermElabM Expr := do
|
||||
newStx ← `(let $lhsVar : $type := $discr; $rhs);
|
||||
withMacroExpansion stx newStx $ elabTerm newStx expectedType?
|
||||
|
||||
-- parser! "match " >> sepBy1 termParser ", " >> optType >> " with " >> matchAlts
|
||||
@[builtinTermElab «match»] def elabMatch : TermElab :=
|
||||
fun stx expectedType? => match_syntax stx with
|
||||
| `(match $discr:term with $y:ident => $rhs:term) => expandSimpleMatch stx discr y rhs expectedType?
|
||||
| `(match $discr:term with | $y:ident => $rhs:term) => expandSimpleMatch stx discr y rhs expectedType?
|
||||
| `(match $discr:term : $type with $y:ident => $rhs:term) => expandSimpleMatchWithType stx discr y type rhs expectedType?
|
||||
| `(match $discr:term : $type with | $y:ident => $rhs:term) => expandSimpleMatchWithType stx discr y type rhs expectedType?
|
||||
| _ => throwUnsupportedSyntax
|
||||
|
||||
end Term
|
||||
end Elab
|
||||
end Lean
|
||||
|
|
@ -99,9 +99,6 @@ partial def toParserDescrAux : Syntax → ToParserDescrM Syntax
|
|||
else if kind == `Lean.Parser.Syntax.lookahead then do
|
||||
d ← withNoPushLeading $ toParserDescrAux (stx.getArg 1);
|
||||
`(ParserDescr.lookahead $d)
|
||||
else if kind == `Lean.Parser.Syntax.optional then do
|
||||
d ← withNoPushLeading $ toParserDescrAux (stx.getArg 1);
|
||||
`(ParserDescr.optional $d)
|
||||
else if kind == `Lean.Parser.Syntax.sepBy then do
|
||||
d₁ ← withNoPushLeading $ toParserDescrAux (stx.getArg 1);
|
||||
d₂ ← withNoPushLeading $ toParserDescrAux (stx.getArg 2);
|
||||
|
|
@ -116,12 +113,15 @@ partial def toParserDescrAux : Syntax → ToParserDescrM Syntax
|
|||
else if kind == `Lean.Parser.Syntax.many1 then do
|
||||
d ← withNoPushLeading $ toParserDescrAux (stx.getArg 0);
|
||||
`(ParserDescr.many1 $d)
|
||||
else if kind == `Lean.Parser.Syntax.optional then do
|
||||
d ← withNoPushLeading $ toParserDescrAux (stx.getArg 0);
|
||||
`(ParserDescr.optional $d)
|
||||
else if kind == `Lean.Parser.Syntax.orelse then do
|
||||
d₁ ← withNoPushLeading $ toParserDescrAux (stx.getArg 0);
|
||||
d₂ ← withNoPushLeading $ toParserDescrAux (stx.getArg 2);
|
||||
`(ParserDescr.orelse $d₁ $d₂)
|
||||
else
|
||||
liftM $ throwUnsupportedSyntax
|
||||
liftM $ throwError stx $ "unexpected syntax kind of category `syntax`: " ++ kind
|
||||
|
||||
/--
|
||||
Given a `stx` of category `syntax`, return a pair `(newStx, trailingParser)`,
|
||||
|
|
|
|||
|
|
@ -49,6 +49,9 @@ withMVarContext mvarId $ do
|
|||
mvarDecl ← getMVarDecl mvarId;
|
||||
expectedType ← instantiateMVars stx mvarDecl.type;
|
||||
result ← resumeElabTerm stx expectedType (!postponeOnError);
|
||||
/- We must ensure `result` has the expected type because it is the one expected by the method that postponed stx.
|
||||
That is, the method does not have an opportunity to check whether `result` has the expected type or not. -/
|
||||
result ← ensureHasType stx expectedType result;
|
||||
assignExprMVar mvarId result;
|
||||
pure true)
|
||||
(fun ex => match ex with
|
||||
|
|
|
|||
|
|
@ -33,6 +33,8 @@ structure Context extends Meta.Context :=
|
|||
the list of pending synthetic metavariables, and returns `?m`. -/
|
||||
(mayPostpone : Bool := true)
|
||||
(errToSorry : Bool := true)
|
||||
/- If `macroStackAtErr == true`, we include it in error messages. -/
|
||||
(macroStackAtErr : Bool := true)
|
||||
|
||||
/-- We use synthetic metavariables as placeholders for pending elaboration steps. -/
|
||||
inductive SyntheticMVarKind
|
||||
|
|
@ -130,7 +132,7 @@ instance monadLog : MonadLog TermElabM :=
|
|||
def throwError {α} (ref : Syntax) (msgData : MessageData) : TermElabM α := do
|
||||
ctx ← read;
|
||||
let ref := getBetterRef ref ctx.macroStack;
|
||||
let msgData := addMacroStack msgData ctx.macroStack;
|
||||
let msgData := if ctx.macroStackAtErr then addMacroStack msgData ctx.macroStack else msgData;
|
||||
msg ← mkMessage msgData MessageSeverity.error ref;
|
||||
throw (Exception.ex (Elab.Exception.error msg))
|
||||
|
||||
|
|
@ -261,6 +263,7 @@ fun ctx s =>
|
|||
| EStateM.Result.error ex newS => EStateM.Result.error (fromMetaException ctx ref ex) (fromMetaState ref ctx s newS oldTraceState)
|
||||
|
||||
def ppGoal (ref : Syntax) (mvarId : MVarId) : TermElabM Format := liftMetaM ref $ Meta.ppGoal mvarId
|
||||
def isType (ref : Syntax) (e : Expr) : TermElabM Bool := liftMetaM ref $ Meta.isType e
|
||||
def isDefEq (ref : Syntax) (t s : Expr) : TermElabM Bool := liftMetaM ref $ Meta.approxDefEq $ Meta.isDefEq t s
|
||||
def inferType (ref : Syntax) (e : Expr) : TermElabM Expr := liftMetaM ref $ Meta.inferType e
|
||||
def whnf (ref : Syntax) (e : Expr) : TermElabM Expr := liftMetaM ref $ Meta.whnf e
|
||||
|
|
@ -507,27 +510,6 @@ fun stx expectedType? => do
|
|||
stx' ← exp stx;
|
||||
withMacroExpansion stx stx' $ elabTerm stx' expectedType?
|
||||
|
||||
/--
|
||||
Make sure `e` is a type by inferring its type and making sure it is a `Expr.sort`
|
||||
or is unifiable with `Expr.sort`, or can be coerced into one. -/
|
||||
def ensureType (ref : Syntax) (e : Expr) : TermElabM Expr := do
|
||||
eType ← inferType ref e;
|
||||
eType ← whnf ref eType;
|
||||
if eType.isSort then
|
||||
pure e
|
||||
else do
|
||||
u ← mkFreshLevelMVar ref;
|
||||
condM (isDefEq ref eType (mkSort u))
|
||||
(pure e)
|
||||
(do -- TODO try coercion to sort
|
||||
throwError ref "type expected")
|
||||
|
||||
/-- Elaborate `stx` and ensure result is a type. -/
|
||||
def elabType (stx : Syntax) : TermElabM Expr := do
|
||||
u ← mkFreshLevelMVar stx;
|
||||
type ← elabTerm stx (mkSort u);
|
||||
ensureType stx type
|
||||
|
||||
@[inline] def withLCtx {α} (lctx : LocalContext) (localInsts : LocalInstances) (x : TermElabM α) : TermElabM α :=
|
||||
adaptReader (fun (ctx : Context) => { lctx := lctx, localInstances := localInsts, .. ctx }) x
|
||||
|
||||
|
|
@ -602,6 +584,9 @@ match f? with
|
|||
env ← getEnv; mctx ← getMCtx; lctx ← getLCtx; opts ← getOptions;
|
||||
throwError ref $ Meta.Exception.mkAppTypeMismatchMessage f e { env := env, mctx := mctx, lctx := lctx, opts := opts } ++ extraMsg
|
||||
|
||||
@[inline] def withoutMacroStackAtErr {α} (x : TermElabM α) : TermElabM α :=
|
||||
adaptReader (fun (ctx : Context) => { macroStackAtErr := false, .. ctx }) x
|
||||
|
||||
/--
|
||||
Try to apply coercion to make sure `e` has type `expectedType`.
|
||||
Relevant definitions:
|
||||
|
|
@ -617,7 +602,7 @@ mvar ← mkFreshExprMVar ref coeTInstType MetavarKind.synthetic;
|
|||
let eNew := mkAppN (mkConst `coe [u, v]) #[eType, expectedType, e, mvar];
|
||||
let mvarId := mvar.mvarId!;
|
||||
catch
|
||||
(do
|
||||
(withoutMacroStackAtErr $ do
|
||||
unlessM (synthesizeInstMVarCore ref mvarId) $
|
||||
registerSyntheticMVar ref mvarId (SyntheticMVarKind.coe expectedType eType e f?);
|
||||
pure eNew)
|
||||
|
|
@ -647,6 +632,47 @@ match expectedType? with
|
|||
| none => pure e
|
||||
| _ => do eType ← inferType ref e; ensureHasTypeAux ref expectedType? eType e
|
||||
|
||||
/-
|
||||
Relevant definitions:
|
||||
```
|
||||
class CoeSort (α : Sort u) (β : outParam (Sort v))
|
||||
abbrev coeSort {α : Sort u} {β : Sort v} (a : α) [CoeSort α β] : β
|
||||
``` -/
|
||||
private def tryCoeSort (ref : Syntax) (α : Expr) (a : Expr) : TermElabM Expr := do
|
||||
β ← mkFreshTypeMVar ref;
|
||||
u ← getLevel ref α;
|
||||
v ← getLevel ref β;
|
||||
let coeSortInstType := mkAppN (Lean.mkConst `CoeSort [u, v]) #[α, β];
|
||||
mvar ← mkFreshExprMVar ref coeSortInstType MetavarKind.synthetic;
|
||||
let mvarId := mvar.mvarId!;
|
||||
catch
|
||||
(withoutMacroStackAtErr $ condM (synthesizeInstMVarCore ref mvarId)
|
||||
(pure $ mkAppN (Lean.mkConst `coeSort [u, v]) #[α, β, a, mvar])
|
||||
(throwError ref "type expected"))
|
||||
(fun ex =>
|
||||
match ex with
|
||||
| Exception.ex (Elab.Exception.error errMsg) => throwError ref ("type expected" ++ Format.line ++ errMsg.data)
|
||||
| _ => throwError ref "type expected")
|
||||
|
||||
/--
|
||||
Make sure `e` is a type by inferring its type and making sure it is a `Expr.sort`
|
||||
or is unifiable with `Expr.sort`, or can be coerced into one. -/
|
||||
def ensureType (ref : Syntax) (e : Expr) : TermElabM Expr :=
|
||||
condM (isType ref e)
|
||||
(pure e)
|
||||
(do
|
||||
eType ← inferType ref e;
|
||||
u ← mkFreshLevelMVar ref;
|
||||
condM (isDefEq ref eType (mkSort u))
|
||||
(pure e)
|
||||
(tryCoeSort ref eType e))
|
||||
|
||||
/-- Elaborate `stx` and ensure result is a type. -/
|
||||
def elabType (stx : Syntax) : TermElabM Expr := do
|
||||
u ← mkFreshLevelMVar stx;
|
||||
type ← elabTerm stx (mkSort u);
|
||||
ensureType stx type
|
||||
|
||||
/- =======================================
|
||||
Builtin elaboration functions
|
||||
======================================= -/
|
||||
|
|
@ -732,7 +758,7 @@ fun stx expectedType? => do
|
|||
let consId := mkTermIdFrom openBkt `List.cons;
|
||||
let nilId := mkTermIdFrom closeBkt `List.nil;
|
||||
let newStx := args.foldSepRevArgs (fun arg r => mkAppStx consId #[arg, r]) nilId;
|
||||
elabTerm newStx expectedType?
|
||||
withMacroExpansion stx newStx $ elabTerm newStx expectedType?
|
||||
|
||||
@[builtinTermElab «arrayLit»] def elabArrayLit : TermElab :=
|
||||
fun stx expectedType? => do
|
||||
|
|
|
|||
|
|
@ -56,87 +56,202 @@ match arg with
|
|||
val ← elabTerm val expectedType;
|
||||
ensureArgType ref f val expectedType
|
||||
|
||||
private def mkArrow (d b : Expr) : TermElabM Expr := do
|
||||
n ← mkFreshAnonymousName;
|
||||
pure $ Lean.mkForall n BinderInfo.default d b
|
||||
|
||||
/-
|
||||
Relevant definitions:
|
||||
```
|
||||
class CoeFun (α : Sort u) (a : α) (γ : outParam (Sort v))
|
||||
abbrev coeFun {α : Sort u} {γ : Sort v} (a : α) [CoeFun α a γ]
|
||||
class CoeFun (α : Sort u) (γ : α → outParam (Sort v))
|
||||
abbrev coeFun {α : Sort u} {γ : α → Sort v} (a : α) [CoeFun α γ] : γ a
|
||||
``` -/
|
||||
private def tryCoeFun (ref : Syntax) (α : Expr) (a : Expr) : TermElabM Expr := do
|
||||
γ ← mkFreshTypeMVar ref;
|
||||
v ← mkFreshLevelMVar ref;
|
||||
type ← mkArrow α (mkSort v);
|
||||
γ ← mkFreshExprMVar ref type;
|
||||
u ← getLevel ref α;
|
||||
v ← getLevel ref γ;
|
||||
let coeFunInstType := mkAppN (Lean.mkConst `CoeFun [u, v]) #[α, a, γ];
|
||||
let coeFunInstType := mkAppN (Lean.mkConst `CoeFun [u, v]) #[α, γ];
|
||||
mvar ← mkFreshExprMVar ref coeFunInstType MetavarKind.synthetic;
|
||||
let mvarId := mvar.mvarId!;
|
||||
catch
|
||||
(condM (synthesizeInstMVarCore ref mvarId)
|
||||
(pure $ mkAppN (Lean.mkConst `coeFun [u, v]) #[α, γ, a, mvar])
|
||||
(throwError ref "function expected"))
|
||||
synthesized ←
|
||||
catch (withoutMacroStackAtErr $ synthesizeInstMVarCore ref mvarId)
|
||||
(fun ex =>
|
||||
match ex with
|
||||
| Exception.ex (Elab.Exception.error errMsg) => throwError ref ("function expected" ++ Format.line ++ errMsg.data)
|
||||
| _ => throwError ref "function expected")
|
||||
| _ => throwError ref "function expected");
|
||||
if synthesized then
|
||||
pure $ mkAppN (Lean.mkConst `coeFun [u, v]) #[α, γ, a, mvar]
|
||||
else
|
||||
throwError ref "function expected"
|
||||
|
||||
private partial def elabAppArgsAux (ref : Syntax) (args : Array Arg) (expectedType? : Option Expr) (explicit : Bool)
|
||||
: Nat → Array NamedArg → Array MVarId → Expr → Expr → TermElabM Expr
|
||||
| argIdx, namedArgs, instMVars, eType, e => do
|
||||
/-- Auxiliary structure used to elaborate function application arguments. -/
|
||||
structure ElabAppArgsCtx :=
|
||||
(ref : Syntax)
|
||||
(args : Array Arg)
|
||||
(expectedType? : Option Expr)
|
||||
(explicit : Bool) -- if true, all arguments are treated as explicit
|
||||
(argIdx : Nat := 0) -- position of next explicit argument to be processed
|
||||
(namedArgs : Array NamedArg) -- remaining named arguments to be processed
|
||||
(instMVars : Array MVarId := #[]) -- metavariables for the instance implicit arguments that have already been processed
|
||||
(typeMVars : Array MVarId := #[]) -- metavariables for implicit arguments of the form `{α : Sort u}` that have already been processed
|
||||
(foundExplicit : Bool := false) -- true if an explicit argument has already been processed
|
||||
|
||||
private def isAutoOrOptParam (type : Expr) : Bool :=
|
||||
-- TODO: add auto param
|
||||
type.getOptParamDefault?.isSome
|
||||
|
||||
/- Auxiliary function for retrieving the resulting type of a function application.
|
||||
See `propagateExpectedType`. -/
|
||||
private partial def getForallBody : Nat → Array NamedArg → Expr → Option Expr
|
||||
| i, namedArgs, type@(Expr.forallE n d b c) =>
|
||||
match namedArgs.findIdx? (fun namedArg => namedArg.name == n) with
|
||||
| some idx => getForallBody i (namedArgs.eraseIdx idx) b
|
||||
| none =>
|
||||
if !c.binderInfo.isExplicit then
|
||||
getForallBody i namedArgs b
|
||||
else if i > 0 then
|
||||
getForallBody (i-1) namedArgs b
|
||||
else if isAutoOrOptParam d then
|
||||
getForallBody i namedArgs b
|
||||
else
|
||||
some type
|
||||
| i, namedArgs, type => if i == 0 && namedArgs.isEmpty then some type else none
|
||||
|
||||
private def hasTypeMVar (ctx : ElabAppArgsCtx) (type : Expr) : Bool :=
|
||||
(type.findMVar? (fun mvarId => ctx.typeMVars.contains mvarId)).isSome
|
||||
|
||||
private def hasOnlyTypeMVar (ctx : ElabAppArgsCtx) (type : Expr) : Bool :=
|
||||
(type.findMVar? (fun mvarId => !ctx.typeMVars.contains mvarId)).isNone
|
||||
|
||||
/-
|
||||
Auxiliary method for propagating the expected type. We call it as soon as we find the first explict
|
||||
argument. The goal is to propagate the expected type in applications of functions such as
|
||||
```lean
|
||||
HasAdd.add {α : Type u} : α → α → α
|
||||
List.cons {α : Type u} : α → List α → List α
|
||||
```
|
||||
This is particularly useful when there applicable coercions. For example,
|
||||
assume we have a coercion from `Nat` to `Int`, and we have
|
||||
`(x : Nat)` and the expected type is `List Int`. Then, if we don't use this function,
|
||||
the elaborator will fail to elaborate
|
||||
```
|
||||
List.cons x []
|
||||
```
|
||||
First, the elaborator creates a new metavariable `?α` for the implicit argument `{α : Type u}`.
|
||||
Then, when it processes `x`, it assigns `?α := Nat`, and then obtain the
|
||||
resultant type `List Nat` which is **not** definitionally equal to `List Int`.
|
||||
We solve the problem by executing this method before we elaborate the first explicit argument (`x` in this example).
|
||||
This method infers that the resultant type is `List ?α` and unifies it with `List Int`.
|
||||
Then, when we elaborate `x`, the elaborate realizes the coercion from `Nat` to `Int` must be used, and the
|
||||
term
|
||||
```
|
||||
@List.cons Int (coe x) (@List.nil Int)
|
||||
```
|
||||
is produced.
|
||||
|
||||
The method will do nothing if
|
||||
1- The resultant type depends on the remaining arguments (i.e., `!eTypeBody.hasLooseBVars`)
|
||||
2- The resultant type does not contain any type metavariable.
|
||||
3- The resultant type contains a nontype metavariable.
|
||||
|
||||
We added conditions 2&3 to be able to restrict this method to simple functions that are "morally" in
|
||||
the Hindley&Milner fragment.
|
||||
For example, consider the following definitions
|
||||
```
|
||||
def foo {n m : Nat} (a : bv n) (b : bv m) : bv (n - m)
|
||||
```
|
||||
Now, consider
|
||||
```
|
||||
def test (x1 : bv 32) (x2 : bv 31) (y1 : bv 64) (y2 : bv 63) : bv 1 :=
|
||||
foo x1 x2 = foo y1 y2
|
||||
```
|
||||
When the elaborator reaches the term `foo y1 y2`, the expected type is `bv (32-31)`.
|
||||
If we apply this method, we would solve the unification problem `bv (?n - ?m) =?= bv (32 - 31)`,
|
||||
by assigning `?n := 32` and `?m := 31`. Then, the elaborator fails elaborating `y1` since
|
||||
`bv 64` is **not** definitionally equal to `bv 32`.
|
||||
-/
|
||||
private def propagateExpectedType (ctx : ElabAppArgsCtx) (eType : Expr) : TermElabM Unit :=
|
||||
unless (ctx.explicit || ctx.foundExplicit || ctx.typeMVars.isEmpty) $ do
|
||||
match ctx.expectedType? with
|
||||
| none => pure ()
|
||||
| some expectedType =>
|
||||
let numRemainingArgs := ctx.args.size - ctx.argIdx;
|
||||
match getForallBody numRemainingArgs ctx.namedArgs eType with
|
||||
| none => pure ()
|
||||
| some eTypeBody =>
|
||||
unless eTypeBody.hasLooseBVars $
|
||||
when (hasTypeMVar ctx eTypeBody && hasOnlyTypeMVar ctx eTypeBody) $ do
|
||||
isDefEq ctx.ref expectedType eTypeBody;
|
||||
pure ()
|
||||
|
||||
/- Elaborate function application arguments. -/
|
||||
private partial def elabAppArgsAux : ElabAppArgsCtx → Expr → Expr → TermElabM Expr
|
||||
| ctx, e, eType => do
|
||||
let finalize : Unit → TermElabM Expr := fun _ => do {
|
||||
-- all user explicit arguments have been consumed
|
||||
e ← ensureHasTypeAux ref expectedType? eType e;
|
||||
synthesizeAppInstMVars ref instMVars;
|
||||
match ctx.expectedType? with
|
||||
| none => pure ()
|
||||
| some expectedType => do {
|
||||
-- Try to propagate expected type. Ignore if types are not definitionally equal, caller must handle it.
|
||||
isDefEq ctx.ref expectedType eType;
|
||||
pure ()
|
||||
};
|
||||
synthesizeAppInstMVars ctx.ref ctx.instMVars;
|
||||
pure e
|
||||
};
|
||||
eType ← whnfForall ref eType;
|
||||
eType ← whnfForall ctx.ref eType;
|
||||
match eType with
|
||||
| Expr.forallE n d b c =>
|
||||
match namedArgs.findIdx? (fun namedArg => namedArg.name == n) with
|
||||
match ctx.namedArgs.findIdx? (fun namedArg => namedArg.name == n) with
|
||||
| some idx => do
|
||||
let arg := namedArgs.get! idx;
|
||||
let namedArgs := namedArgs.eraseIdx idx;
|
||||
argElab ← elabArg ref e arg.val d;
|
||||
elabAppArgsAux argIdx namedArgs instMVars (b.instantiate1 argElab) (mkApp e argElab)
|
||||
let arg := ctx.namedArgs.get! idx;
|
||||
let namedArgs := ctx.namedArgs.eraseIdx idx;
|
||||
argElab ← elabArg ctx.ref e arg.val d;
|
||||
propagateExpectedType ctx eType;
|
||||
elabAppArgsAux { foundExplicit := true, namedArgs := namedArgs, .. ctx } (mkApp e argElab) (b.instantiate1 argElab)
|
||||
| none =>
|
||||
let processExplictArg : Unit → TermElabM Expr := fun _ => do {
|
||||
if h : argIdx < args.size then do
|
||||
argElab ← elabArg ref e (args.get ⟨argIdx, h⟩) d;
|
||||
elabAppArgsAux (argIdx + 1) namedArgs instMVars (b.instantiate1 argElab) (mkApp e argElab)
|
||||
propagateExpectedType ctx eType;
|
||||
let ctx := { foundExplicit := true, .. ctx };
|
||||
if h : ctx.argIdx < ctx.args.size then do
|
||||
argElab ← elabArg ctx.ref e (ctx.args.get ⟨ctx.argIdx, h⟩) d;
|
||||
elabAppArgsAux { argIdx := ctx.argIdx + 1, .. ctx } (mkApp e argElab) (b.instantiate1 argElab)
|
||||
else match d.getOptParamDefault? with
|
||||
| some defVal => elabAppArgsAux argIdx namedArgs instMVars (b.instantiate1 defVal) (mkApp e defVal)
|
||||
| some defVal => elabAppArgsAux ctx (mkApp e defVal) (b.instantiate1 defVal)
|
||||
| none =>
|
||||
-- TODO: tactic auto param
|
||||
if namedArgs.isEmpty then
|
||||
if ctx.namedArgs.isEmpty then
|
||||
finalize ()
|
||||
else
|
||||
throwError ref ("explicit parameter '" ++ n ++ "' is missing, unused named arguments " ++ toString (namedArgs.map $ fun narg => narg.name))
|
||||
throwError ctx.ref ("explicit parameter '" ++ n ++ "' is missing, unused named arguments " ++ toString (ctx.namedArgs.map $ fun narg => narg.name))
|
||||
};
|
||||
if explicit then
|
||||
if ctx.explicit then
|
||||
processExplictArg ()
|
||||
else match c.binderInfo with
|
||||
| BinderInfo.implicit => do
|
||||
a ← mkFreshExprMVar ref d;
|
||||
elabAppArgsAux argIdx namedArgs instMVars (b.instantiate1 a) (mkApp e a)
|
||||
a ← mkFreshExprMVar ctx.ref d;
|
||||
typeMVars ← condM (isType ctx.ref a) (pure $ ctx.typeMVars.push a.mvarId!) (pure ctx.typeMVars);
|
||||
elabAppArgsAux { typeMVars := typeMVars, .. ctx } (mkApp e a) (b.instantiate1 a)
|
||||
| BinderInfo.instImplicit => do
|
||||
a ← mkFreshExprMVar ref d MetavarKind.synthetic;
|
||||
elabAppArgsAux argIdx namedArgs (instMVars.push a.mvarId!) (b.instantiate1 a) (mkApp e a)
|
||||
a ← mkFreshExprMVar ctx.ref d MetavarKind.synthetic;
|
||||
elabAppArgsAux { instMVars := ctx.instMVars.push a.mvarId!, .. ctx } (mkApp e a) (b.instantiate1 a)
|
||||
| _ =>
|
||||
processExplictArg ()
|
||||
| _ =>
|
||||
if namedArgs.isEmpty && argIdx == args.size then
|
||||
if ctx.namedArgs.isEmpty && ctx.argIdx == ctx.args.size then
|
||||
finalize ()
|
||||
else do
|
||||
e ← tryCoeFun ref eType e;
|
||||
eType ← inferType ref e;
|
||||
elabAppArgsAux argIdx namedArgs instMVars eType e
|
||||
e ← tryCoeFun ctx.ref eType e;
|
||||
eType ← inferType ctx.ref e;
|
||||
elabAppArgsAux ctx e eType
|
||||
|
||||
private def elabAppArgs (ref : Syntax) (f : Expr) (namedArgs : Array NamedArg) (args : Array Arg)
|
||||
(expectedType? : Option Expr) (explicit : Bool) : TermElabM Expr := do
|
||||
fType ← inferType ref f;
|
||||
fType ← instantiateMVars ref fType;
|
||||
tryPostponeIfMVar fType;
|
||||
let argIdx := 0;
|
||||
let instMVars := #[];
|
||||
elabAppArgsAux ref args expectedType? explicit argIdx namedArgs instMVars fType f
|
||||
elabAppArgsAux {ref := ref, args := args, expectedType? := expectedType?, explicit := explicit, namedArgs := namedArgs } f fType
|
||||
|
||||
/-- Auxiliary inductive datatype that represents the resolution of an `LVal`. -/
|
||||
inductive LValResolution
|
||||
|
|
|
|||
|
|
@ -276,11 +276,12 @@ if optType.isNone then
|
|||
else
|
||||
(optType.getArg 0).getArg 1
|
||||
|
||||
def elabLetDeclAux (ref : Syntax) (n : Name) (binders : Array Syntax) (type : Syntax) (val : Syntax) (body : Syntax)
|
||||
def elabLetDeclAux (ref : Syntax) (n : Name) (binders : Array Syntax) (typeStx : Syntax) (valStx : Syntax) (body : Syntax)
|
||||
(expectedType? : Option Expr) : TermElabM Expr := do
|
||||
(type, val) ← elabBinders binders $ fun xs => do {
|
||||
type ← elabType type;
|
||||
val ← elabTerm val type;
|
||||
type ← elabType typeStx;
|
||||
val ← elabTerm valStx type;
|
||||
val ← ensureHasType valStx type val;
|
||||
type ← mkForall ref xs type;
|
||||
val ← mkLambda ref xs val;
|
||||
pure (type, val)
|
||||
|
|
@ -305,11 +306,12 @@ fun stx expectedType? => match_syntax stx with
|
|||
elabLetDeclAux stx id.getId args (mkHole stx) val body expectedType?
|
||||
| `(let $id:ident $args* : $type := $val; $body) =>
|
||||
elabLetDeclAux stx id.getId args type val body expectedType?
|
||||
| `(let $id:id := $val; $body) => do
|
||||
-- HACK: support single Term.id pattern let (as produced by quotations) by translation to ident let for now
|
||||
let id := id.getArg 0;
|
||||
stx ← `(let $id := $val; $body);
|
||||
elabTerm stx expectedType?
|
||||
| `(let $pat:term := $val; $body) => do
|
||||
stxNew ← `(let x := $val; match x with $pat => $body);
|
||||
withMacroExpansion stx stxNew $ elabTerm stxNew expectedType?
|
||||
| `(let $pat:term : $type := $val; $body) => do
|
||||
stxNew ← `(let x : $type := $val; match x with $pat => $body);
|
||||
withMacroExpansion stx stxNew $ elabTerm stxNew expectedType?
|
||||
| _ => throwUnsupportedSyntax
|
||||
|
||||
@[init] private def regTraceClasses : IO Unit := do
|
||||
|
|
|
|||
|
|
@ -288,6 +288,39 @@ private partial def mkMaxAux (lvls : Array Level) (extraK : Nat) : Nat → Level
|
|||
else
|
||||
accMax result prev (extraK + prevK)
|
||||
|
||||
/-
|
||||
Auxiliary function for `normalize`. It assumes `lvls` has been sorted using `normLt`.
|
||||
It finds the first position that is not an explicit universe. -/
|
||||
private partial def skipExplicit (lvls : Array Level) : Nat → Nat
|
||||
| i =>
|
||||
if h : i < lvls.size then
|
||||
let lvl := lvls.get ⟨i, h⟩;
|
||||
if lvl.getLevelOffset.isZero then skipExplicit (i+1) else i
|
||||
else
|
||||
i
|
||||
|
||||
/-
|
||||
Auxiliary function for `normalize`.
|
||||
`maxExplicit` is the maximum explicit universe level at `lvls`.
|
||||
Return true if it finds a level with offset ≥ maxExplicit.
|
||||
`i` starts at the first non explict level.
|
||||
It assumes `lvls` has been sorted using `normLt`. -/
|
||||
private partial def isExplicitSubsumedAux (lvls : Array Level) (maxExplicit : Nat) : Nat → Bool
|
||||
| i =>
|
||||
if h : i < lvls.size then
|
||||
let lvl := lvls.get ⟨i, h⟩;
|
||||
if lvl.getOffset ≥ maxExplicit then true
|
||||
else isExplicitSubsumedAux (i+1)
|
||||
else
|
||||
false
|
||||
|
||||
/- Auxiliary function for `normalize`. See `isExplicitSubsumedAux` -/
|
||||
private def isExplicitSubsumed (lvls : Array Level) (firstNonExplicit : Nat) : Bool :=
|
||||
if firstNonExplicit == 0 then false
|
||||
else
|
||||
let max := (lvls.get! (firstNonExplicit - 1)).getOffset;
|
||||
isExplicitSubsumedAux lvls max firstNonExplicit
|
||||
|
||||
partial def normalize : Level → Level
|
||||
| l =>
|
||||
if isAlreadyNormalizedCheap l then l
|
||||
|
|
@ -299,10 +332,12 @@ partial def normalize : Level → Level
|
|||
let lvls := getMaxArgsAux normalize l₁ false #[];
|
||||
let lvls := getMaxArgsAux normalize l₂ false lvls;
|
||||
let lvls := lvls.qsort normLt;
|
||||
let lvl₁ := lvls.get! 0;
|
||||
let firstNonExplicit := skipExplicit lvls 0;
|
||||
let i := if isExplicitSubsumed lvls firstNonExplicit then firstNonExplicit else firstNonExplicit - 1;
|
||||
let lvl₁ := lvls.get! i;
|
||||
let prev := lvl₁.getLevelOffset;
|
||||
let prevK := lvl₁.getOffset;
|
||||
mkMaxAux lvls k 1 prev prevK levelZero
|
||||
mkMaxAux lvls k (i+1) prev prevK levelZero
|
||||
| imax l₁ l₂ _ =>
|
||||
if l₂.isNeverZero then addOffset (normalize (mkLevelMax l₁ l₂)) k
|
||||
else
|
||||
|
|
@ -311,7 +346,6 @@ partial def normalize : Level → Level
|
|||
addOffset (mkIMaxAux l₁ l₂) k
|
||||
| _ => unreachable!
|
||||
|
||||
|
||||
/- Return true if `u` and `v` denote the same level.
|
||||
Check is currently incomplete. -/
|
||||
def isEquiv (u v : Level) : Bool :=
|
||||
|
|
|
|||
|
|
@ -1460,6 +1460,14 @@ private def noImmediateColon {k : ParserKind} : Parser k :=
|
|||
else s
|
||||
}
|
||||
|
||||
def setExpectedFn {k : ParserKind} (expected : List String) (p : ParserFn k) : ParserFn k :=
|
||||
fun a c s => match p a c s with
|
||||
| s'@{ errorMsg := some msg } => { s' with errorMsg := some { msg with expected := [] } }
|
||||
| s' => s'
|
||||
|
||||
def setExpected {k : ParserKind} (expected : List String) (p : Parser k) : Parser k :=
|
||||
{ fn := setExpectedFn expected p.fn, info := p.info }
|
||||
|
||||
def pushNone {k : ParserKind} : Parser k :=
|
||||
{ fn := fun a c s => s.pushSyntax mkNullNode }
|
||||
|
||||
|
|
@ -1484,7 +1492,8 @@ let nameP := checkNoWsBefore ("no space before ':" ++ name ++ "'") >> symbolAux
|
|||
-- if parsing the kind fails and `anonymous` is true, check that we're not ignoring a different
|
||||
-- antiquotation kind via `noImmediateColon`
|
||||
let nameP := if anonymous then nameP <|> noImmediateColon >> pushNone >> pushNone else nameP;
|
||||
node kind $ try $ dollarSymbol >> checkNoWsBefore "no space before" >> antiquotExpr >> nameP >> optional (checkNoWsBefore "" >> "*")
|
||||
-- antiquotations are not part of the "standard" syntax, so hide "expected '$'" on error
|
||||
node kind $ try $ setExpected [] dollarSymbol >> checkNoWsBefore "no space before" >> antiquotExpr >> nameP >> optional (checkNoWsBefore "" >> "*")
|
||||
|
||||
/- ===================== -/
|
||||
/- End of Antiquotations -/
|
||||
|
|
|
|||
|
|
@ -30,12 +30,12 @@ namespace Syntax
|
|||
@[builtinSyntaxParser] def str := parser! nonReservedSymbol "str"
|
||||
@[builtinSyntaxParser] def char := parser! nonReservedSymbol "char"
|
||||
@[builtinSyntaxParser] def ident := parser! nonReservedSymbol "ident"
|
||||
@[builtinSyntaxParser] def try := parser! nonReservedSymbol "try " >> syntaxParser
|
||||
@[builtinSyntaxParser] def lookahead := parser! nonReservedSymbol "lookahead " >> syntaxParser
|
||||
@[builtinSyntaxParser] def optional := parser! nonReservedSymbol "optional " >> syntaxParser
|
||||
@[builtinSyntaxParser] def sepBy := parser! nonReservedSymbol "sepBy " >> syntaxParser >> syntaxParser
|
||||
@[builtinSyntaxParser] def sepBy1 := parser! nonReservedSymbol "sepBy1 " >> syntaxParser >> syntaxParser
|
||||
@[builtinSyntaxParser] def try := parser! nonReservedSymbol "try " >> syntaxParser appPrec
|
||||
@[builtinSyntaxParser] def lookahead := parser! nonReservedSymbol "lookahead " >> syntaxParser appPrec
|
||||
@[builtinSyntaxParser] def sepBy := parser! nonReservedSymbol "sepBy " >> syntaxParser appPrec >> syntaxParser appPrec
|
||||
@[builtinSyntaxParser] def sepBy1 := parser! nonReservedSymbol "sepBy1 " >> syntaxParser appPrec >> syntaxParser appPrec
|
||||
|
||||
@[builtinSyntaxParser] def optional := tparser! pushLeading >> symbolAux "?" none
|
||||
@[builtinSyntaxParser] def many := tparser! pushLeading >> symbolAux "*" none
|
||||
@[builtinSyntaxParser] def many1 := tparser! pushLeading >> symbolAux "+" none
|
||||
@[builtinSyntaxParser] def orelse := tparser! pushLeading >> " <|> " >> syntaxParser 1
|
||||
|
|
@ -59,8 +59,8 @@ def mixfixSymbol := quotedSymbolPrec <|> unquotedSymbol
|
|||
def strLitPrec := parser! strLit >> optPrecedence
|
||||
def identPrec := parser! ident >> optPrecedence
|
||||
|
||||
-- TODO: remove " := " after old frontend is gone
|
||||
def optKind : Parser := optional ("[" >> ident >> "]")
|
||||
-- TODO: remove " := " after old frontend is gone
|
||||
@[builtinCommandParser] def «notation» := parser! "notation" >> many (strLitPrec <|> quotedSymbolPrec <|> identPrec) >> (" := " <|> darrow) >> termParser
|
||||
@[builtinCommandParser] def «macro_rules» := parser! "macro_rules" >> optKind >> Term.matchAlts
|
||||
@[builtinCommandParser] def «syntax» := parser! "syntax " >> optKind >> many1 syntaxParser >> " : " >> ident
|
||||
|
|
|
|||
|
|
@ -37,3 +37,10 @@ panic (mkPanicMessage modName line col msg)
|
|||
-- TODO: should be a macro
|
||||
@[neverExtract, noinline, nospecialize] def unreachable! {α : Type u} [Inhabited α] : α :=
|
||||
panic! "unreachable"
|
||||
|
||||
|
||||
@[noinline, nospecialize, neverExtract] def withPtrEq {α : Type u} (r : α → α → Bool) (h : ∀ a, r a a = true) : α → α → Bool :=
|
||||
r
|
||||
|
||||
@[noinline, nospecialize, neverExtract] def withPtrAddr {α : Type u} {β : Type v} (a : α) (k : Nat → β) (h : ∀ u₁ u₂, k u₁ = k u₂) : β :=
|
||||
k 0
|
||||
|
|
|
|||
File diff suppressed because one or more lines are too long
|
|
@ -13,98 +13,71 @@
|
|||
#ifdef __cplusplus
|
||||
extern "C" {
|
||||
#endif
|
||||
lean_object* l_coeTC(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_coeTC(lean_object*, lean_object*);
|
||||
lean_object* l_coeBase___rarg(lean_object*, lean_object*);
|
||||
lean_object* l_coeOfHead___rarg(lean_object*, lean_object*);
|
||||
lean_object* l_coeTail___rarg(lean_object*, lean_object*);
|
||||
lean_object* l_coeSort___rarg___boxed(lean_object*);
|
||||
lean_object* l_coeOfDep___rarg___boxed(lean_object*);
|
||||
lean_object* l_coeOfDep(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_coeD___rarg(lean_object*);
|
||||
lean_object* l_coeOfTCOfTail(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_coeOfHeadOfTC___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_coeSortTrans___rarg___boxed(lean_object*);
|
||||
lean_object* l_coeTC___rarg(lean_object*);
|
||||
lean_object* l_coeOfTCOfTail(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_coeTC___rarg(lean_object*, lean_object*);
|
||||
lean_object* l_coeTail(lean_object*, lean_object*);
|
||||
lean_object* l_coeOfTC___rarg(lean_object*);
|
||||
lean_object* l_coeFun(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_coeOfTC___rarg(lean_object*, lean_object*);
|
||||
lean_object* l_coeFun(lean_object*, lean_object*);
|
||||
uint8_t l_decPropToBool___rarg(uint8_t);
|
||||
lean_object* l_coeBase(lean_object*, lean_object*);
|
||||
lean_object* l_coeDepTrans___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_coeTrans(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_coeSort___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_coeTrans(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_coeB___rarg(lean_object*, lean_object*);
|
||||
lean_object* l_coeOfTail(lean_object*, lean_object*);
|
||||
lean_object* l_coeSortTrans(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_coeOfHeadOfTC___rarg(lean_object*);
|
||||
lean_object* l_coeOfTC___rarg___boxed(lean_object*);
|
||||
lean_object* l_coeSortTrans(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_coeOfHeadOfTC___rarg(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_decPropToBool___rarg___boxed(lean_object*);
|
||||
lean_object* l_coeSort___rarg(lean_object*);
|
||||
lean_object* l_coeFun___rarg___boxed(lean_object*);
|
||||
lean_object* l_coeSort___rarg(lean_object*, lean_object*);
|
||||
lean_object* l_hasOfNatOfCoe___rarg(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_coeFunTrans___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_coeFunDepTrans(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_coeFunTrans___rarg(lean_object*);
|
||||
lean_object* l_coeOfHeafOfTCOfTail___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_coeSortDepTrans___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_coeDepTrans(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_coeFunDepTrans___rarg___boxed(lean_object*);
|
||||
lean_object* l_coeOfHeadOfTC(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_coeOfTCOfTail___rarg(lean_object*, lean_object*);
|
||||
lean_object* l_coeDepBase___rarg___boxed(lean_object*);
|
||||
lean_object* l_coeSortDepTrans___rarg(lean_object*);
|
||||
lean_object* l_coeFunTrans___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_coeFunTrans___rarg(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_coeOfHeadOfTC(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_coeOfTCOfTail___rarg(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_coe___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_coeFunDepTrans___rarg(lean_object*);
|
||||
lean_object* l_subtypeCoe___rarg___boxed(lean_object*);
|
||||
lean_object* l_coeOfTCOfTail___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_coeSortDepTrans___rarg___boxed(lean_object*);
|
||||
lean_object* l_coeOfHead(lean_object*, lean_object*);
|
||||
lean_object* l_optionCoe___rarg(lean_object*);
|
||||
lean_object* l_coeFun___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_coeSortTrans___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_coeFun___boxed(lean_object*, lean_object*);
|
||||
lean_object* l_hasOfNatOfCoe(lean_object*, lean_object*);
|
||||
lean_object* l_coeFunTrans(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_coeOfTC(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_coeFunTrans(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_coeOfDep___rarg(lean_object*);
|
||||
lean_object* l_coeOfTC(lean_object*, lean_object*);
|
||||
uint8_t l_coeDecidableEq(uint8_t);
|
||||
lean_object* l_coeD___rarg___boxed(lean_object*);
|
||||
lean_object* l_coeDepBase(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_coeOfTail___rarg(lean_object*, lean_object*);
|
||||
lean_object* l_coe___rarg(lean_object*);
|
||||
lean_object* l_coeDepTrans___rarg___boxed(lean_object*);
|
||||
lean_object* l_coeOfHeadOfTC___rarg___boxed(lean_object*);
|
||||
lean_object* l_coeSortDepTrans(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_coe(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_coeSortTrans___rarg(lean_object*);
|
||||
lean_object* l_coeSortTrans___rarg(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_coeDecidableEq___boxed(lean_object*);
|
||||
lean_object* l_coeTrans___rarg(lean_object*, lean_object*);
|
||||
lean_object* l_coeOfDep___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_coeTrans___rarg(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_optionCoe(lean_object*);
|
||||
lean_object* l_coeOfTC___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_coeDepTrans___rarg(lean_object*);
|
||||
lean_object* l_subtypeCoe___rarg(lean_object*);
|
||||
lean_object* l_coeFun___rarg(lean_object*);
|
||||
lean_object* l_coeFunDepTrans___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_coeFun___rarg(lean_object*, lean_object*);
|
||||
lean_object* l_coeB(lean_object*, lean_object*);
|
||||
lean_object* l_subtypeCoe(lean_object*, lean_object*);
|
||||
lean_object* l_coeSort(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_coeOfHeafOfTCOfTail___rarg(lean_object*, lean_object*);
|
||||
lean_object* l_coeSort(lean_object*, lean_object*);
|
||||
lean_object* l_coeOfHeafOfTCOfTail___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_coe___rarg___boxed(lean_object*);
|
||||
lean_object* l_boolToProp;
|
||||
lean_object* l_coeDepBase___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_coeHead___rarg(lean_object*, lean_object*);
|
||||
lean_object* l_subtypeCoe___boxed(lean_object*, lean_object*);
|
||||
lean_object* l_coeFunTrans___rarg___boxed(lean_object*);
|
||||
lean_object* l_coeTC___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_coeD___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_coeTC___rarg___boxed(lean_object*);
|
||||
lean_object* l_coeTrans___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_decPropToBool(lean_object*);
|
||||
lean_object* l_coeOfHeafOfTCOfTail(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_coeOfHeafOfTCOfTail(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_coeHead(lean_object*, lean_object*);
|
||||
lean_object* l_coeDepBase___rarg(lean_object*);
|
||||
lean_object* l_coeD(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_coeB___rarg(lean_object* x_1, lean_object* x_2) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_3;
|
||||
x_3 = lean_apply_1(x_2, x_1);
|
||||
x_3 = lean_apply_1(x_1, x_2);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
|
|
@ -120,7 +93,7 @@ lean_object* l_coeHead___rarg(lean_object* x_1, lean_object* x_2) {
|
|||
_start:
|
||||
{
|
||||
lean_object* x_3;
|
||||
x_3 = lean_apply_1(x_2, x_1);
|
||||
x_3 = lean_apply_1(x_1, x_2);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
|
|
@ -136,7 +109,7 @@ lean_object* l_coeTail___rarg(lean_object* x_1, lean_object* x_2) {
|
|||
_start:
|
||||
{
|
||||
lean_object* x_3;
|
||||
x_3 = lean_apply_1(x_2, x_1);
|
||||
x_3 = lean_apply_1(x_1, x_2);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
|
|
@ -181,37 +154,20 @@ lean_dec(x_3);
|
|||
return x_4;
|
||||
}
|
||||
}
|
||||
lean_object* l_coeTC___rarg(lean_object* x_1) {
|
||||
lean_object* l_coeTC___rarg(lean_object* x_1, lean_object* x_2) {
|
||||
_start:
|
||||
{
|
||||
lean_inc(x_1);
|
||||
return x_1;
|
||||
lean_object* x_3;
|
||||
x_3 = lean_apply_1(x_1, x_2);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
lean_object* l_coeTC(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
|
||||
lean_object* l_coeTC(lean_object* x_1, lean_object* x_2) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_4;
|
||||
x_4 = lean_alloc_closure((void*)(l_coeTC___rarg___boxed), 1, 0);
|
||||
return x_4;
|
||||
}
|
||||
}
|
||||
lean_object* l_coeTC___rarg___boxed(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_2;
|
||||
x_2 = l_coeTC___rarg(x_1);
|
||||
lean_dec(x_1);
|
||||
return x_2;
|
||||
}
|
||||
}
|
||||
lean_object* l_coeTC___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_4;
|
||||
x_4 = l_coeTC(x_1, x_2, x_3);
|
||||
lean_dec(x_3);
|
||||
return x_4;
|
||||
lean_object* x_3;
|
||||
x_3 = lean_alloc_closure((void*)(l_coeTC___rarg), 2, 0);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
lean_object* l_coe___rarg(lean_object* x_1) {
|
||||
|
|
@ -247,107 +203,7 @@ lean_dec(x_3);
|
|||
return x_4;
|
||||
}
|
||||
}
|
||||
lean_object* l_coeFun___rarg(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
lean_inc(x_1);
|
||||
return x_1;
|
||||
}
|
||||
}
|
||||
lean_object* l_coeFun(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_4;
|
||||
x_4 = lean_alloc_closure((void*)(l_coeFun___rarg___boxed), 1, 0);
|
||||
return x_4;
|
||||
}
|
||||
}
|
||||
lean_object* l_coeFun___rarg___boxed(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_2;
|
||||
x_2 = l_coeFun___rarg(x_1);
|
||||
lean_dec(x_1);
|
||||
return x_2;
|
||||
}
|
||||
}
|
||||
lean_object* l_coeFun___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_4;
|
||||
x_4 = l_coeFun(x_1, x_2, x_3);
|
||||
lean_dec(x_3);
|
||||
return x_4;
|
||||
}
|
||||
}
|
||||
lean_object* l_coeSort___rarg(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
lean_inc(x_1);
|
||||
return x_1;
|
||||
}
|
||||
}
|
||||
lean_object* l_coeSort(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_4;
|
||||
x_4 = lean_alloc_closure((void*)(l_coeSort___rarg___boxed), 1, 0);
|
||||
return x_4;
|
||||
}
|
||||
}
|
||||
lean_object* l_coeSort___rarg___boxed(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_2;
|
||||
x_2 = l_coeSort___rarg(x_1);
|
||||
lean_dec(x_1);
|
||||
return x_2;
|
||||
}
|
||||
}
|
||||
lean_object* l_coeSort___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_4;
|
||||
x_4 = l_coeSort(x_1, x_2, x_3);
|
||||
lean_dec(x_3);
|
||||
return x_4;
|
||||
}
|
||||
}
|
||||
lean_object* l_coeDepTrans___rarg(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
lean_inc(x_1);
|
||||
return x_1;
|
||||
}
|
||||
}
|
||||
lean_object* l_coeDepTrans(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_6;
|
||||
x_6 = lean_alloc_closure((void*)(l_coeDepTrans___rarg___boxed), 1, 0);
|
||||
return x_6;
|
||||
}
|
||||
}
|
||||
lean_object* l_coeDepTrans___rarg___boxed(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_2;
|
||||
x_2 = l_coeDepTrans___rarg(x_1);
|
||||
lean_dec(x_1);
|
||||
return x_2;
|
||||
}
|
||||
}
|
||||
lean_object* l_coeDepTrans___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_6;
|
||||
x_6 = l_coeDepTrans(x_1, x_2, x_3, x_4, x_5);
|
||||
lean_dec(x_5);
|
||||
lean_dec(x_4);
|
||||
return x_6;
|
||||
}
|
||||
}
|
||||
lean_object* l_coeTrans___rarg(lean_object* x_1, lean_object* x_2) {
|
||||
lean_object* l_coeFun___rarg(lean_object* x_1, lean_object* x_2) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_3;
|
||||
|
|
@ -355,28 +211,61 @@ x_3 = lean_apply_1(x_2, x_1);
|
|||
return x_3;
|
||||
}
|
||||
}
|
||||
lean_object* l_coeTrans(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
|
||||
lean_object* l_coeFun(lean_object* x_1, lean_object* x_2) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_5;
|
||||
x_5 = lean_alloc_closure((void*)(l_coeTrans___rarg), 2, 0);
|
||||
lean_object* x_3;
|
||||
x_3 = lean_alloc_closure((void*)(l_coeFun___rarg), 2, 0);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
lean_object* l_coeFun___boxed(lean_object* x_1, lean_object* x_2) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_3;
|
||||
x_3 = l_coeFun(x_1, x_2);
|
||||
lean_dec(x_2);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
lean_object* l_coeSort___rarg(lean_object* x_1, lean_object* x_2) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_3;
|
||||
x_3 = lean_apply_1(x_2, x_1);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
lean_object* l_coeSort(lean_object* x_1, lean_object* x_2) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_3;
|
||||
x_3 = lean_alloc_closure((void*)(l_coeSort___rarg), 2, 0);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
lean_object* l_coeTrans___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_4; lean_object* x_5;
|
||||
x_4 = lean_apply_1(x_1, x_3);
|
||||
x_5 = lean_apply_1(x_2, x_4);
|
||||
return x_5;
|
||||
}
|
||||
}
|
||||
lean_object* l_coeTrans___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
|
||||
lean_object* l_coeTrans(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_5;
|
||||
x_5 = l_coeTrans(x_1, x_2, x_3, x_4);
|
||||
lean_dec(x_4);
|
||||
return x_5;
|
||||
lean_object* x_4;
|
||||
x_4 = lean_alloc_closure((void*)(l_coeTrans___rarg), 3, 0);
|
||||
return x_4;
|
||||
}
|
||||
}
|
||||
lean_object* l_coeBase___rarg(lean_object* x_1, lean_object* x_2) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_3;
|
||||
x_3 = lean_apply_1(x_2, x_1);
|
||||
x_3 = lean_apply_1(x_1, x_2);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
|
|
@ -388,124 +277,58 @@ x_3 = lean_alloc_closure((void*)(l_coeBase___rarg), 2, 0);
|
|||
return x_3;
|
||||
}
|
||||
}
|
||||
lean_object* l_coeDepBase___rarg(lean_object* x_1) {
|
||||
lean_object* l_coeOfHeafOfTCOfTail___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
|
||||
_start:
|
||||
{
|
||||
lean_inc(x_1);
|
||||
return x_1;
|
||||
}
|
||||
}
|
||||
lean_object* l_coeDepBase(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_4;
|
||||
x_4 = lean_alloc_closure((void*)(l_coeDepBase___rarg___boxed), 1, 0);
|
||||
return x_4;
|
||||
}
|
||||
}
|
||||
lean_object* l_coeDepBase___rarg___boxed(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_2;
|
||||
x_2 = l_coeDepBase___rarg(x_1);
|
||||
lean_dec(x_1);
|
||||
return x_2;
|
||||
}
|
||||
}
|
||||
lean_object* l_coeDepBase___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_4;
|
||||
x_4 = l_coeDepBase(x_1, x_2, x_3);
|
||||
lean_dec(x_3);
|
||||
return x_4;
|
||||
}
|
||||
}
|
||||
lean_object* l_coeOfHeafOfTCOfTail___rarg(lean_object* x_1, lean_object* x_2) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_3;
|
||||
x_3 = lean_apply_1(x_2, x_1);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
lean_object* l_coeOfHeafOfTCOfTail(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:
|
||||
{
|
||||
lean_object* x_7;
|
||||
x_7 = lean_alloc_closure((void*)(l_coeOfHeafOfTCOfTail___rarg), 2, 0);
|
||||
lean_object* x_5; lean_object* x_6; lean_object* x_7;
|
||||
x_5 = lean_apply_1(x_4, x_1);
|
||||
x_6 = lean_apply_1(x_2, x_5);
|
||||
x_7 = lean_apply_1(x_3, x_6);
|
||||
return x_7;
|
||||
}
|
||||
}
|
||||
lean_object* l_coeOfHeafOfTCOfTail___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) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_7;
|
||||
x_7 = l_coeOfHeafOfTCOfTail(x_1, x_2, x_3, x_4, x_5, x_6);
|
||||
lean_dec(x_6);
|
||||
lean_dec(x_5);
|
||||
return x_7;
|
||||
}
|
||||
}
|
||||
lean_object* l_coeOfHeadOfTC___rarg(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
lean_inc(x_1);
|
||||
return x_1;
|
||||
}
|
||||
}
|
||||
lean_object* l_coeOfHeadOfTC(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_6;
|
||||
x_6 = lean_alloc_closure((void*)(l_coeOfHeadOfTC___rarg___boxed), 1, 0);
|
||||
return x_6;
|
||||
}
|
||||
}
|
||||
lean_object* l_coeOfHeadOfTC___rarg___boxed(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_2;
|
||||
x_2 = l_coeOfHeadOfTC___rarg(x_1);
|
||||
lean_dec(x_1);
|
||||
return x_2;
|
||||
}
|
||||
}
|
||||
lean_object* l_coeOfHeadOfTC___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_6;
|
||||
x_6 = l_coeOfHeadOfTC(x_1, x_2, x_3, x_4, x_5);
|
||||
lean_dec(x_5);
|
||||
lean_dec(x_4);
|
||||
return x_6;
|
||||
}
|
||||
}
|
||||
lean_object* l_coeOfTCOfTail___rarg(lean_object* x_1, lean_object* x_2) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_3;
|
||||
x_3 = lean_apply_1(x_2, x_1);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
lean_object* l_coeOfTCOfTail(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
|
||||
lean_object* l_coeOfHeafOfTCOfTail(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_5;
|
||||
x_5 = lean_alloc_closure((void*)(l_coeOfTCOfTail___rarg), 2, 0);
|
||||
x_5 = lean_alloc_closure((void*)(l_coeOfHeafOfTCOfTail___rarg), 4, 0);
|
||||
return x_5;
|
||||
}
|
||||
}
|
||||
lean_object* l_coeOfTCOfTail___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
|
||||
lean_object* l_coeOfHeadOfTC___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_5;
|
||||
x_5 = l_coeOfTCOfTail(x_1, x_2, x_3, x_4);
|
||||
lean_dec(x_4);
|
||||
lean_object* x_4; lean_object* x_5;
|
||||
x_4 = lean_apply_1(x_3, x_1);
|
||||
x_5 = lean_apply_1(x_2, x_4);
|
||||
return x_5;
|
||||
}
|
||||
}
|
||||
lean_object* l_coeOfHeadOfTC(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_4;
|
||||
x_4 = lean_alloc_closure((void*)(l_coeOfHeadOfTC___rarg), 3, 0);
|
||||
return x_4;
|
||||
}
|
||||
}
|
||||
lean_object* l_coeOfTCOfTail___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_4; lean_object* x_5;
|
||||
x_4 = lean_apply_1(x_2, x_1);
|
||||
x_5 = lean_apply_1(x_3, x_4);
|
||||
return x_5;
|
||||
}
|
||||
}
|
||||
lean_object* l_coeOfTCOfTail(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_4;
|
||||
x_4 = lean_alloc_closure((void*)(l_coeOfTCOfTail___rarg), 3, 0);
|
||||
return x_4;
|
||||
}
|
||||
}
|
||||
lean_object* l_coeOfHead___rarg(lean_object* x_1, lean_object* x_2) {
|
||||
_start:
|
||||
{
|
||||
|
|
@ -538,173 +361,96 @@ x_3 = lean_alloc_closure((void*)(l_coeOfTail___rarg), 2, 0);
|
|||
return x_3;
|
||||
}
|
||||
}
|
||||
lean_object* l_coeOfTC___rarg(lean_object* x_1) {
|
||||
lean_object* l_coeOfTC___rarg(lean_object* x_1, lean_object* x_2) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_3;
|
||||
x_3 = lean_apply_1(x_2, x_1);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
lean_object* l_coeOfTC(lean_object* x_1, lean_object* x_2) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_3;
|
||||
x_3 = lean_alloc_closure((void*)(l_coeOfTC___rarg), 2, 0);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
lean_object* l_coeOfDep___rarg(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
lean_inc(x_1);
|
||||
return x_1;
|
||||
}
|
||||
}
|
||||
lean_object* l_coeOfTC(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
|
||||
lean_object* l_coeOfDep(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_4;
|
||||
x_4 = lean_alloc_closure((void*)(l_coeOfTC___rarg___boxed), 1, 0);
|
||||
x_4 = lean_alloc_closure((void*)(l_coeOfDep___rarg___boxed), 1, 0);
|
||||
return x_4;
|
||||
}
|
||||
}
|
||||
lean_object* l_coeOfTC___rarg___boxed(lean_object* x_1) {
|
||||
lean_object* l_coeOfDep___rarg___boxed(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_2;
|
||||
x_2 = l_coeOfTC___rarg(x_1);
|
||||
x_2 = l_coeOfDep___rarg(x_1);
|
||||
lean_dec(x_1);
|
||||
return x_2;
|
||||
}
|
||||
}
|
||||
lean_object* l_coeOfTC___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
|
||||
lean_object* l_coeOfDep___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_4;
|
||||
x_4 = l_coeOfTC(x_1, x_2, x_3);
|
||||
x_4 = l_coeOfDep(x_1, x_2, x_3);
|
||||
lean_dec(x_3);
|
||||
return x_4;
|
||||
}
|
||||
}
|
||||
lean_object* l_coeFunDepTrans___rarg(lean_object* x_1) {
|
||||
lean_object* l_coeFunTrans___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
|
||||
_start:
|
||||
{
|
||||
lean_inc(x_1);
|
||||
return x_1;
|
||||
lean_object* x_4; lean_object* x_5;
|
||||
x_4 = lean_apply_1(x_2, x_3);
|
||||
x_5 = lean_apply_1(x_1, x_4);
|
||||
return x_5;
|
||||
}
|
||||
}
|
||||
lean_object* l_coeFunDepTrans(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
|
||||
lean_object* l_coeFunTrans(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_6;
|
||||
x_6 = lean_alloc_closure((void*)(l_coeFunDepTrans___rarg___boxed), 1, 0);
|
||||
return x_6;
|
||||
lean_object* x_4;
|
||||
x_4 = lean_alloc_closure((void*)(l_coeFunTrans___rarg), 3, 0);
|
||||
return x_4;
|
||||
}
|
||||
}
|
||||
lean_object* l_coeFunDepTrans___rarg___boxed(lean_object* x_1) {
|
||||
lean_object* l_coeFunTrans___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_2;
|
||||
x_2 = l_coeFunDepTrans___rarg(x_1);
|
||||
lean_dec(x_1);
|
||||
return x_2;
|
||||
lean_object* x_4;
|
||||
x_4 = l_coeFunTrans(x_1, x_2, x_3);
|
||||
lean_dec(x_3);
|
||||
return x_4;
|
||||
}
|
||||
}
|
||||
lean_object* l_coeFunDepTrans___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
|
||||
lean_object* l_coeSortTrans___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_6;
|
||||
x_6 = l_coeFunDepTrans(x_1, x_2, x_3, x_4, x_5);
|
||||
lean_dec(x_5);
|
||||
lean_dec(x_4);
|
||||
return x_6;
|
||||
lean_object* x_4; lean_object* x_5;
|
||||
x_4 = lean_apply_1(x_2, x_3);
|
||||
x_5 = lean_apply_1(x_1, x_4);
|
||||
return x_5;
|
||||
}
|
||||
}
|
||||
lean_object* l_coeSortDepTrans___rarg(lean_object* x_1) {
|
||||
lean_object* l_coeSortTrans(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
|
||||
_start:
|
||||
{
|
||||
lean_inc(x_1);
|
||||
return x_1;
|
||||
}
|
||||
}
|
||||
lean_object* l_coeSortDepTrans(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_6;
|
||||
x_6 = lean_alloc_closure((void*)(l_coeSortDepTrans___rarg___boxed), 1, 0);
|
||||
return x_6;
|
||||
}
|
||||
}
|
||||
lean_object* l_coeSortDepTrans___rarg___boxed(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_2;
|
||||
x_2 = l_coeSortDepTrans___rarg(x_1);
|
||||
lean_dec(x_1);
|
||||
return x_2;
|
||||
}
|
||||
}
|
||||
lean_object* l_coeSortDepTrans___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_6;
|
||||
x_6 = l_coeSortDepTrans(x_1, x_2, x_3, x_4, x_5);
|
||||
lean_dec(x_5);
|
||||
lean_dec(x_4);
|
||||
return x_6;
|
||||
}
|
||||
}
|
||||
lean_object* l_coeFunTrans___rarg(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
lean_inc(x_1);
|
||||
return x_1;
|
||||
}
|
||||
}
|
||||
lean_object* l_coeFunTrans(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_6;
|
||||
x_6 = lean_alloc_closure((void*)(l_coeFunTrans___rarg___boxed), 1, 0);
|
||||
return x_6;
|
||||
}
|
||||
}
|
||||
lean_object* l_coeFunTrans___rarg___boxed(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_2;
|
||||
x_2 = l_coeFunTrans___rarg(x_1);
|
||||
lean_dec(x_1);
|
||||
return x_2;
|
||||
}
|
||||
}
|
||||
lean_object* l_coeFunTrans___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_6;
|
||||
x_6 = l_coeFunTrans(x_1, x_2, x_3, x_4, x_5);
|
||||
lean_dec(x_5);
|
||||
lean_dec(x_4);
|
||||
return x_6;
|
||||
}
|
||||
}
|
||||
lean_object* l_coeSortTrans___rarg(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
lean_inc(x_1);
|
||||
return x_1;
|
||||
}
|
||||
}
|
||||
lean_object* l_coeSortTrans(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_6;
|
||||
x_6 = lean_alloc_closure((void*)(l_coeSortTrans___rarg___boxed), 1, 0);
|
||||
return x_6;
|
||||
}
|
||||
}
|
||||
lean_object* l_coeSortTrans___rarg___boxed(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_2;
|
||||
x_2 = l_coeSortTrans___rarg(x_1);
|
||||
lean_dec(x_1);
|
||||
return x_2;
|
||||
}
|
||||
}
|
||||
lean_object* l_coeSortTrans___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_6;
|
||||
x_6 = l_coeSortTrans(x_1, x_2, x_3, x_4, x_5);
|
||||
lean_dec(x_5);
|
||||
lean_dec(x_4);
|
||||
return x_6;
|
||||
lean_object* x_4;
|
||||
x_4 = lean_alloc_closure((void*)(l_coeSortTrans___rarg), 3, 0);
|
||||
return x_4;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_boolToProp() {
|
||||
|
|
|
|||
|
|
@ -60,8 +60,8 @@ lean_object* l_hasMonadLiftTTrans___rarg(lean_object* x_1, lean_object* x_2, lea
|
|||
_start:
|
||||
{
|
||||
lean_object* x_5; lean_object* x_6;
|
||||
x_5 = lean_apply_2(x_2, lean_box(0), x_4);
|
||||
x_6 = lean_apply_2(x_1, lean_box(0), x_5);
|
||||
x_5 = lean_apply_2(x_1, lean_box(0), x_4);
|
||||
x_6 = lean_apply_2(x_2, lean_box(0), x_5);
|
||||
return x_6;
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
// Lean compiler output
|
||||
// Module: Init.Lean.Elab
|
||||
// Imports: Init.Lean.Elab.Import Init.Lean.Elab.Exception Init.Lean.Elab.ElabStrategyAttrs Init.Lean.Elab.Command Init.Lean.Elab.Term Init.Lean.Elab.TermApp Init.Lean.Elab.TermBinders Init.Lean.Elab.Quotation Init.Lean.Elab.Frontend Init.Lean.Elab.BuiltinNotation Init.Lean.Elab.Declaration Init.Lean.Elab.Tactic Init.Lean.Elab.Syntax
|
||||
// Imports: Init.Lean.Elab.Import Init.Lean.Elab.Exception Init.Lean.Elab.ElabStrategyAttrs Init.Lean.Elab.Command Init.Lean.Elab.Term Init.Lean.Elab.TermApp Init.Lean.Elab.TermBinders Init.Lean.Elab.Quotation Init.Lean.Elab.Frontend Init.Lean.Elab.BuiltinNotation Init.Lean.Elab.Declaration Init.Lean.Elab.Tactic Init.Lean.Elab.Syntax Init.Lean.Elab.Match
|
||||
#include "runtime/lean.h"
|
||||
#if defined(__clang__)
|
||||
#pragma clang diagnostic ignored "-Wunused-parameter"
|
||||
|
|
@ -26,6 +26,7 @@ lean_object* initialize_Init_Lean_Elab_BuiltinNotation(lean_object*);
|
|||
lean_object* initialize_Init_Lean_Elab_Declaration(lean_object*);
|
||||
lean_object* initialize_Init_Lean_Elab_Tactic(lean_object*);
|
||||
lean_object* initialize_Init_Lean_Elab_Syntax(lean_object*);
|
||||
lean_object* initialize_Init_Lean_Elab_Match(lean_object*);
|
||||
static bool _G_initialized = false;
|
||||
lean_object* initialize_Init_Lean_Elab(lean_object* w) {
|
||||
lean_object * res;
|
||||
|
|
@ -70,6 +71,9 @@ lean_dec_ref(res);
|
|||
res = initialize_Init_Lean_Elab_Syntax(lean_io_mk_world());
|
||||
if (lean_io_result_is_error(res)) return res;
|
||||
lean_dec_ref(res);
|
||||
res = initialize_Init_Lean_Elab_Match(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
|
||||
|
|
|
|||
|
|
@ -368,6 +368,7 @@ lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabAppend___closed__2;
|
|||
lean_object* l_Lean_Elab_Term_elabWhere___lambda__1___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_elabPow___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabMapConst___closed__3;
|
||||
extern lean_object* l___private_Init_Lean_Elab_Term_10__mkPairsAux___main___closed__5;
|
||||
lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabModN___closed__3;
|
||||
lean_object* l_Lean_Elab_Term_elabGE(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_iterateMAux___main___at_Array_append___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -613,7 +614,6 @@ lean_object* l_Lean_Elab_Term_elabNe___closed__2;
|
|||
extern lean_object* l_Lean_Parser_Term_and___elambda__1___closed__1;
|
||||
lean_object* l_Lean_Elab_Term_elabParserMacro___lambda__1___closed__7;
|
||||
lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabOrM(lean_object*);
|
||||
extern lean_object* l___private_Init_Lean_Elab_Term_9__mkPairsAux___main___closed__5;
|
||||
lean_object* l_Lean_Elab_Term_elabNe(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
extern lean_object* l_Lean_Parser_Term_orelse___elambda__1___closed__1;
|
||||
lean_object* l_Lean_Elab_Term_ElabFComp___closed__2;
|
||||
|
|
@ -3027,30 +3027,30 @@ return x_2;
|
|||
lean_object* l_Lean_Elab_Term_elabAnonymousCtor(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
|
||||
_start:
|
||||
{
|
||||
uint8_t x_5; lean_object* x_139; uint8_t x_140;
|
||||
x_139 = l_Lean_Parser_Term_anonymousCtor___elambda__1___closed__2;
|
||||
uint8_t x_5; lean_object* x_141; uint8_t x_142;
|
||||
x_141 = l_Lean_Parser_Term_anonymousCtor___elambda__1___closed__2;
|
||||
lean_inc(x_1);
|
||||
x_140 = l_Lean_Syntax_isOfKind(x_1, x_139);
|
||||
if (x_140 == 0)
|
||||
x_142 = l_Lean_Syntax_isOfKind(x_1, x_141);
|
||||
if (x_142 == 0)
|
||||
{
|
||||
uint8_t x_141;
|
||||
x_141 = 0;
|
||||
x_5 = x_141;
|
||||
goto block_138;
|
||||
uint8_t x_143;
|
||||
x_143 = 0;
|
||||
x_5 = x_143;
|
||||
goto block_140;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_142; lean_object* x_143; lean_object* x_144; uint8_t x_145;
|
||||
x_142 = l_Lean_Syntax_getArgs(x_1);
|
||||
x_143 = lean_array_get_size(x_142);
|
||||
lean_dec(x_142);
|
||||
x_144 = lean_unsigned_to_nat(3u);
|
||||
x_145 = lean_nat_dec_eq(x_143, x_144);
|
||||
lean_dec(x_143);
|
||||
x_5 = x_145;
|
||||
goto block_138;
|
||||
lean_object* x_144; lean_object* x_145; lean_object* x_146; uint8_t x_147;
|
||||
x_144 = l_Lean_Syntax_getArgs(x_1);
|
||||
x_145 = lean_array_get_size(x_144);
|
||||
lean_dec(x_144);
|
||||
x_146 = lean_unsigned_to_nat(3u);
|
||||
x_147 = lean_nat_dec_eq(x_145, x_146);
|
||||
lean_dec(x_145);
|
||||
x_5 = x_147;
|
||||
goto block_140;
|
||||
}
|
||||
block_138:
|
||||
block_140:
|
||||
{
|
||||
uint8_t x_6;
|
||||
x_6 = l_coeDecidableEq(x_5);
|
||||
|
|
@ -3211,7 +3211,7 @@ return x_79;
|
|||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_80; lean_object* x_81; lean_object* x_82; lean_object* x_83; lean_object* x_84; lean_object* x_85; lean_object* x_86; lean_object* x_87; lean_object* x_88; lean_object* x_89; uint8_t x_90; uint8_t x_91; lean_object* x_92; lean_object* x_93; uint8_t x_94; lean_object* x_95;
|
||||
lean_object* x_80; lean_object* x_81; lean_object* x_82; lean_object* x_83; lean_object* x_84; lean_object* x_85; lean_object* x_86; lean_object* x_87; lean_object* x_88; lean_object* x_89; uint8_t x_90; uint8_t x_91; uint8_t x_92; lean_object* x_93; lean_object* x_94; uint8_t x_95; lean_object* x_96;
|
||||
x_80 = lean_ctor_get(x_3, 0);
|
||||
x_81 = lean_ctor_get(x_3, 1);
|
||||
x_82 = lean_ctor_get(x_3, 2);
|
||||
|
|
@ -3224,6 +3224,7 @@ x_88 = lean_ctor_get(x_3, 8);
|
|||
x_89 = lean_ctor_get(x_3, 9);
|
||||
x_90 = lean_ctor_get_uint8(x_3, sizeof(void*)*10);
|
||||
x_91 = lean_ctor_get_uint8(x_3, sizeof(void*)*10 + 1);
|
||||
x_92 = lean_ctor_get_uint8(x_3, sizeof(void*)*10 + 2);
|
||||
lean_inc(x_89);
|
||||
lean_inc(x_88);
|
||||
lean_inc(x_87);
|
||||
|
|
@ -3236,83 +3237,85 @@ lean_inc(x_81);
|
|||
lean_inc(x_80);
|
||||
lean_dec(x_3);
|
||||
lean_inc(x_74);
|
||||
x_92 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_92, 0, x_1);
|
||||
lean_ctor_set(x_92, 1, x_74);
|
||||
x_93 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_93, 0, x_1);
|
||||
lean_ctor_set(x_93, 1, x_74);
|
||||
lean_ctor_set(x_53, 1, x_88);
|
||||
lean_ctor_set(x_53, 0, x_92);
|
||||
x_93 = lean_alloc_ctor(0, 10, 2);
|
||||
lean_ctor_set(x_93, 0, x_80);
|
||||
lean_ctor_set(x_93, 1, x_81);
|
||||
lean_ctor_set(x_93, 2, x_82);
|
||||
lean_ctor_set(x_93, 3, x_83);
|
||||
lean_ctor_set(x_93, 4, x_84);
|
||||
lean_ctor_set(x_93, 5, x_85);
|
||||
lean_ctor_set(x_93, 6, x_86);
|
||||
lean_ctor_set(x_93, 7, x_87);
|
||||
lean_ctor_set(x_93, 8, x_53);
|
||||
lean_ctor_set(x_93, 9, x_89);
|
||||
lean_ctor_set_uint8(x_93, sizeof(void*)*10, x_90);
|
||||
lean_ctor_set_uint8(x_93, sizeof(void*)*10 + 1, x_91);
|
||||
x_94 = 1;
|
||||
x_95 = l_Lean_Elab_Term_elabTermAux___main(x_2, x_94, x_74, x_93, x_62);
|
||||
return x_95;
|
||||
lean_ctor_set(x_53, 0, x_93);
|
||||
x_94 = lean_alloc_ctor(0, 10, 3);
|
||||
lean_ctor_set(x_94, 0, x_80);
|
||||
lean_ctor_set(x_94, 1, x_81);
|
||||
lean_ctor_set(x_94, 2, x_82);
|
||||
lean_ctor_set(x_94, 3, x_83);
|
||||
lean_ctor_set(x_94, 4, x_84);
|
||||
lean_ctor_set(x_94, 5, x_85);
|
||||
lean_ctor_set(x_94, 6, x_86);
|
||||
lean_ctor_set(x_94, 7, x_87);
|
||||
lean_ctor_set(x_94, 8, x_53);
|
||||
lean_ctor_set(x_94, 9, x_89);
|
||||
lean_ctor_set_uint8(x_94, sizeof(void*)*10, x_90);
|
||||
lean_ctor_set_uint8(x_94, sizeof(void*)*10 + 1, x_91);
|
||||
lean_ctor_set_uint8(x_94, sizeof(void*)*10 + 2, x_92);
|
||||
x_95 = 1;
|
||||
x_96 = l_Lean_Elab_Term_elabTermAux___main(x_2, x_95, x_74, x_94, x_62);
|
||||
return x_96;
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_96; lean_object* x_97; lean_object* x_98; lean_object* x_99; lean_object* x_100; lean_object* x_101; lean_object* x_102; lean_object* x_103; lean_object* x_104; lean_object* x_105; lean_object* x_106; lean_object* x_107; lean_object* x_108; lean_object* x_109; lean_object* x_110; lean_object* x_111; lean_object* x_112; lean_object* x_113; lean_object* x_114; lean_object* x_115; lean_object* x_116; lean_object* x_117; lean_object* x_118; lean_object* x_119; lean_object* x_120; lean_object* x_121; lean_object* x_122; uint8_t x_123; uint8_t x_124; lean_object* x_125; lean_object* x_126; lean_object* x_127; lean_object* x_128; uint8_t x_129; lean_object* x_130;
|
||||
x_96 = lean_ctor_get(x_53, 0);
|
||||
lean_inc(x_96);
|
||||
lean_object* x_97; lean_object* x_98; lean_object* x_99; lean_object* x_100; lean_object* x_101; lean_object* x_102; lean_object* x_103; lean_object* x_104; lean_object* x_105; lean_object* x_106; lean_object* x_107; lean_object* x_108; lean_object* x_109; lean_object* x_110; lean_object* x_111; lean_object* x_112; lean_object* x_113; lean_object* x_114; lean_object* x_115; lean_object* x_116; lean_object* x_117; lean_object* x_118; lean_object* x_119; lean_object* x_120; lean_object* x_121; lean_object* x_122; lean_object* x_123; uint8_t x_124; uint8_t x_125; uint8_t x_126; lean_object* x_127; lean_object* x_128; lean_object* x_129; lean_object* x_130; uint8_t x_131; lean_object* x_132;
|
||||
x_97 = lean_ctor_get(x_53, 0);
|
||||
lean_inc(x_97);
|
||||
lean_dec(x_53);
|
||||
x_97 = l_Lean_Elab_Term_getCurrMacroScope(x_3, x_32);
|
||||
x_98 = lean_ctor_get(x_97, 1);
|
||||
lean_inc(x_98);
|
||||
lean_dec(x_97);
|
||||
x_99 = l_Lean_Elab_Term_getMainModule___rarg(x_98);
|
||||
x_100 = lean_ctor_get(x_99, 1);
|
||||
lean_inc(x_100);
|
||||
lean_dec(x_99);
|
||||
x_101 = l_Lean_mkCTermIdFrom(x_1, x_96);
|
||||
x_102 = l_Array_empty___closed__1;
|
||||
x_103 = lean_array_push(x_102, x_101);
|
||||
x_104 = lean_unsigned_to_nat(2u);
|
||||
x_105 = lean_unsigned_to_nat(0u);
|
||||
x_106 = l_Array_foldlStepMAux___main___at_Lean_Elab_Term_elabParen___spec__1(x_104, x_10, x_105, x_102);
|
||||
x_98 = l_Lean_Elab_Term_getCurrMacroScope(x_3, x_32);
|
||||
x_99 = lean_ctor_get(x_98, 1);
|
||||
lean_inc(x_99);
|
||||
lean_dec(x_98);
|
||||
x_100 = l_Lean_Elab_Term_getMainModule___rarg(x_99);
|
||||
x_101 = lean_ctor_get(x_100, 1);
|
||||
lean_inc(x_101);
|
||||
lean_dec(x_100);
|
||||
x_102 = l_Lean_mkCTermIdFrom(x_1, x_97);
|
||||
x_103 = l_Array_empty___closed__1;
|
||||
x_104 = lean_array_push(x_103, x_102);
|
||||
x_105 = lean_unsigned_to_nat(2u);
|
||||
x_106 = lean_unsigned_to_nat(0u);
|
||||
x_107 = l_Array_foldlStepMAux___main___at_Lean_Elab_Term_elabParen___spec__1(x_105, x_10, x_106, x_103);
|
||||
lean_dec(x_10);
|
||||
x_107 = l_Array_iterateMAux___main___at_Array_append___spec__1___rarg(x_106, x_106, x_105, x_102);
|
||||
lean_dec(x_106);
|
||||
x_108 = l_Lean_nullKind___closed__2;
|
||||
x_109 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_109, 0, x_108);
|
||||
lean_ctor_set(x_109, 1, x_107);
|
||||
x_110 = lean_array_push(x_103, x_109);
|
||||
x_111 = l_Lean_mkAppStx___closed__8;
|
||||
x_112 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_112, 0, x_111);
|
||||
lean_ctor_set(x_112, 1, x_110);
|
||||
x_113 = lean_ctor_get(x_3, 0);
|
||||
lean_inc(x_113);
|
||||
x_114 = lean_ctor_get(x_3, 1);
|
||||
x_108 = l_Array_iterateMAux___main___at_Array_append___spec__1___rarg(x_107, x_107, x_106, x_103);
|
||||
lean_dec(x_107);
|
||||
x_109 = l_Lean_nullKind___closed__2;
|
||||
x_110 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_110, 0, x_109);
|
||||
lean_ctor_set(x_110, 1, x_108);
|
||||
x_111 = lean_array_push(x_104, x_110);
|
||||
x_112 = l_Lean_mkAppStx___closed__8;
|
||||
x_113 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_113, 0, x_112);
|
||||
lean_ctor_set(x_113, 1, x_111);
|
||||
x_114 = lean_ctor_get(x_3, 0);
|
||||
lean_inc(x_114);
|
||||
x_115 = lean_ctor_get(x_3, 2);
|
||||
x_115 = lean_ctor_get(x_3, 1);
|
||||
lean_inc(x_115);
|
||||
x_116 = lean_ctor_get(x_3, 3);
|
||||
x_116 = lean_ctor_get(x_3, 2);
|
||||
lean_inc(x_116);
|
||||
x_117 = lean_ctor_get(x_3, 4);
|
||||
x_117 = lean_ctor_get(x_3, 3);
|
||||
lean_inc(x_117);
|
||||
x_118 = lean_ctor_get(x_3, 5);
|
||||
x_118 = lean_ctor_get(x_3, 4);
|
||||
lean_inc(x_118);
|
||||
x_119 = lean_ctor_get(x_3, 6);
|
||||
x_119 = lean_ctor_get(x_3, 5);
|
||||
lean_inc(x_119);
|
||||
x_120 = lean_ctor_get(x_3, 7);
|
||||
x_120 = lean_ctor_get(x_3, 6);
|
||||
lean_inc(x_120);
|
||||
x_121 = lean_ctor_get(x_3, 8);
|
||||
x_121 = lean_ctor_get(x_3, 7);
|
||||
lean_inc(x_121);
|
||||
x_122 = lean_ctor_get(x_3, 9);
|
||||
x_122 = lean_ctor_get(x_3, 8);
|
||||
lean_inc(x_122);
|
||||
x_123 = lean_ctor_get_uint8(x_3, sizeof(void*)*10);
|
||||
x_124 = lean_ctor_get_uint8(x_3, sizeof(void*)*10 + 1);
|
||||
x_123 = lean_ctor_get(x_3, 9);
|
||||
lean_inc(x_123);
|
||||
x_124 = lean_ctor_get_uint8(x_3, sizeof(void*)*10);
|
||||
x_125 = lean_ctor_get_uint8(x_3, sizeof(void*)*10 + 1);
|
||||
x_126 = lean_ctor_get_uint8(x_3, sizeof(void*)*10 + 2);
|
||||
if (lean_is_exclusive(x_3)) {
|
||||
lean_ctor_release(x_3, 0);
|
||||
lean_ctor_release(x_3, 1);
|
||||
|
|
@ -3324,61 +3327,62 @@ if (lean_is_exclusive(x_3)) {
|
|||
lean_ctor_release(x_3, 7);
|
||||
lean_ctor_release(x_3, 8);
|
||||
lean_ctor_release(x_3, 9);
|
||||
x_125 = x_3;
|
||||
x_127 = x_3;
|
||||
} else {
|
||||
lean_dec_ref(x_3);
|
||||
x_125 = lean_box(0);
|
||||
x_127 = lean_box(0);
|
||||
}
|
||||
lean_inc(x_112);
|
||||
x_126 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_126, 0, x_1);
|
||||
lean_ctor_set(x_126, 1, x_112);
|
||||
x_127 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_127, 0, x_126);
|
||||
lean_ctor_set(x_127, 1, x_121);
|
||||
if (lean_is_scalar(x_125)) {
|
||||
x_128 = lean_alloc_ctor(0, 10, 2);
|
||||
lean_inc(x_113);
|
||||
x_128 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_128, 0, x_1);
|
||||
lean_ctor_set(x_128, 1, x_113);
|
||||
x_129 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_129, 0, x_128);
|
||||
lean_ctor_set(x_129, 1, x_122);
|
||||
if (lean_is_scalar(x_127)) {
|
||||
x_130 = lean_alloc_ctor(0, 10, 3);
|
||||
} else {
|
||||
x_128 = x_125;
|
||||
x_130 = x_127;
|
||||
}
|
||||
lean_ctor_set(x_128, 0, x_113);
|
||||
lean_ctor_set(x_128, 1, x_114);
|
||||
lean_ctor_set(x_128, 2, x_115);
|
||||
lean_ctor_set(x_128, 3, x_116);
|
||||
lean_ctor_set(x_128, 4, x_117);
|
||||
lean_ctor_set(x_128, 5, x_118);
|
||||
lean_ctor_set(x_128, 6, x_119);
|
||||
lean_ctor_set(x_128, 7, x_120);
|
||||
lean_ctor_set(x_128, 8, x_127);
|
||||
lean_ctor_set(x_128, 9, x_122);
|
||||
lean_ctor_set_uint8(x_128, sizeof(void*)*10, x_123);
|
||||
lean_ctor_set_uint8(x_128, sizeof(void*)*10 + 1, x_124);
|
||||
x_129 = 1;
|
||||
x_130 = l_Lean_Elab_Term_elabTermAux___main(x_2, x_129, x_112, x_128, x_100);
|
||||
return x_130;
|
||||
lean_ctor_set(x_130, 0, x_114);
|
||||
lean_ctor_set(x_130, 1, x_115);
|
||||
lean_ctor_set(x_130, 2, x_116);
|
||||
lean_ctor_set(x_130, 3, x_117);
|
||||
lean_ctor_set(x_130, 4, x_118);
|
||||
lean_ctor_set(x_130, 5, x_119);
|
||||
lean_ctor_set(x_130, 6, x_120);
|
||||
lean_ctor_set(x_130, 7, x_121);
|
||||
lean_ctor_set(x_130, 8, x_129);
|
||||
lean_ctor_set(x_130, 9, x_123);
|
||||
lean_ctor_set_uint8(x_130, sizeof(void*)*10, x_124);
|
||||
lean_ctor_set_uint8(x_130, sizeof(void*)*10 + 1, x_125);
|
||||
lean_ctor_set_uint8(x_130, sizeof(void*)*10 + 2, x_126);
|
||||
x_131 = 1;
|
||||
x_132 = l_Lean_Elab_Term_elabTermAux___main(x_2, x_131, x_113, x_130, x_101);
|
||||
return x_132;
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_131;
|
||||
lean_object* x_133;
|
||||
lean_dec(x_55);
|
||||
lean_dec(x_53);
|
||||
lean_dec(x_10);
|
||||
lean_dec(x_2);
|
||||
x_131 = lean_box(0);
|
||||
x_41 = x_131;
|
||||
x_133 = lean_box(0);
|
||||
x_41 = x_133;
|
||||
goto block_48;
|
||||
}
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_132;
|
||||
lean_object* x_134;
|
||||
lean_dec(x_51);
|
||||
lean_dec(x_10);
|
||||
lean_dec(x_2);
|
||||
x_132 = lean_box(0);
|
||||
x_33 = x_132;
|
||||
x_134 = lean_box(0);
|
||||
x_33 = x_134;
|
||||
goto block_40;
|
||||
}
|
||||
}
|
||||
|
|
@ -3421,12 +3425,12 @@ return x_47;
|
|||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_133;
|
||||
lean_object* x_135;
|
||||
lean_dec(x_28);
|
||||
lean_dec(x_10);
|
||||
lean_dec(x_2);
|
||||
x_133 = lean_box(0);
|
||||
x_21 = x_133;
|
||||
x_135 = lean_box(0);
|
||||
x_21 = x_135;
|
||||
goto block_27;
|
||||
}
|
||||
block_27:
|
||||
|
|
@ -3448,28 +3452,28 @@ return x_26;
|
|||
}
|
||||
else
|
||||
{
|
||||
uint8_t x_134;
|
||||
uint8_t x_136;
|
||||
lean_dec(x_10);
|
||||
lean_dec(x_3);
|
||||
lean_dec(x_2);
|
||||
lean_dec(x_1);
|
||||
x_134 = !lean_is_exclusive(x_11);
|
||||
if (x_134 == 0)
|
||||
x_136 = !lean_is_exclusive(x_11);
|
||||
if (x_136 == 0)
|
||||
{
|
||||
return x_11;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_135; lean_object* x_136; lean_object* x_137;
|
||||
x_135 = lean_ctor_get(x_11, 0);
|
||||
x_136 = lean_ctor_get(x_11, 1);
|
||||
lean_inc(x_136);
|
||||
lean_inc(x_135);
|
||||
lean_object* x_137; lean_object* x_138; lean_object* x_139;
|
||||
x_137 = lean_ctor_get(x_11, 0);
|
||||
x_138 = lean_ctor_get(x_11, 1);
|
||||
lean_inc(x_138);
|
||||
lean_inc(x_137);
|
||||
lean_dec(x_11);
|
||||
x_137 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_137, 0, x_135);
|
||||
lean_ctor_set(x_137, 1, x_136);
|
||||
return x_137;
|
||||
x_139 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_139, 0, x_137);
|
||||
lean_ctor_set(x_139, 1, x_138);
|
||||
return x_139;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
@ -6369,7 +6373,7 @@ lean_object* l_Lean_Elab_Term_elabProd(lean_object* x_1, lean_object* x_2, lean_
|
|||
_start:
|
||||
{
|
||||
lean_object* x_5; lean_object* x_6;
|
||||
x_5 = l___private_Init_Lean_Elab_Term_9__mkPairsAux___main___closed__5;
|
||||
x_5 = l___private_Init_Lean_Elab_Term_10__mkPairsAux___main___closed__5;
|
||||
x_6 = l_Lean_Elab_Term_elabInfixOp(x_5, x_1, x_2, x_3, x_4);
|
||||
return x_6;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -7038,7 +7038,7 @@ lean_inc(x_16);
|
|||
lean_inc(x_15);
|
||||
lean_inc(x_13);
|
||||
lean_inc(x_12);
|
||||
x_24 = lean_alloc_ctor(0, 10, 2);
|
||||
x_24 = lean_alloc_ctor(0, 10, 3);
|
||||
lean_ctor_set(x_24, 0, x_20);
|
||||
lean_ctor_set(x_24, 1, x_12);
|
||||
lean_ctor_set(x_24, 2, x_13);
|
||||
|
|
@ -7051,6 +7051,7 @@ lean_ctor_set(x_24, 8, x_16);
|
|||
lean_ctor_set(x_24, 9, x_17);
|
||||
lean_ctor_set_uint8(x_24, sizeof(void*)*10, x_8);
|
||||
lean_ctor_set_uint8(x_24, sizeof(void*)*10 + 1, x_8);
|
||||
lean_ctor_set_uint8(x_24, sizeof(void*)*10 + 2, x_8);
|
||||
return x_24;
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -70,7 +70,6 @@ lean_object* l_Lean_Elab_Command_elabConstant___closed__11;
|
|||
extern lean_object* l_Lean_Parser_Command_def___elambda__1___closed__2;
|
||||
extern lean_object* l_Lean_Parser_Command_declValSimple___elambda__1___closed__2;
|
||||
extern lean_object* l_Lean_Meta_registerInstanceAttr___closed__1;
|
||||
extern lean_object* l_Lean_Elab_Term_elabLetDecl___closed__4;
|
||||
lean_object* l_Lean_Elab_Command_elabConstant(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Command_elabAxiom___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Command_expandOptDeclSig(lean_object*);
|
||||
|
|
@ -108,6 +107,7 @@ lean_object* l_Lean_Elab_Command_elabInstance(lean_object*, lean_object*, lean_o
|
|||
extern lean_object* l_Lean_Parser_Command_axiom___elambda__1___closed__2;
|
||||
lean_object* l_Lean_Elab_Command_getCurrMacroScope(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Command_getMainModule(lean_object*, lean_object*);
|
||||
extern lean_object* l_Lean_Elab_Term_elabLetDecl___closed__6;
|
||||
lean_object* l_Lean_Syntax_getArgs(lean_object*);
|
||||
lean_object* l_Lean_Syntax_getKind(lean_object*);
|
||||
lean_object* l_Lean_MacroScopesView_review(lean_object*);
|
||||
|
|
@ -545,7 +545,7 @@ x_34 = l_Lean_mkAppStx___closed__8;
|
|||
x_35 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_35, 0, x_34);
|
||||
lean_ctor_set(x_35, 1, x_33);
|
||||
x_36 = l_Lean_Elab_Term_elabLetDecl___closed__4;
|
||||
x_36 = l_Lean_Elab_Term_elabLetDecl___closed__6;
|
||||
x_37 = l_Lean_mkAtomFrom(x_2, x_36);
|
||||
x_38 = l_Lean_mkAppStx___closed__9;
|
||||
x_39 = lean_array_push(x_38, x_37);
|
||||
|
|
|
|||
|
|
@ -1193,7 +1193,7 @@ return x_29;
|
|||
}
|
||||
else
|
||||
{
|
||||
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; lean_object* x_37; lean_object* x_38; uint8_t x_39; uint8_t x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43; lean_object* x_44; lean_object* x_45; lean_object* x_46; lean_object* x_47;
|
||||
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; lean_object* x_37; lean_object* x_38; uint8_t x_39; uint8_t x_40; uint8_t x_41; lean_object* x_42; lean_object* x_43; lean_object* x_44; lean_object* x_45; lean_object* x_46; lean_object* x_47; lean_object* x_48;
|
||||
x_30 = lean_ctor_get(x_8, 1);
|
||||
x_31 = lean_ctor_get(x_8, 2);
|
||||
x_32 = lean_ctor_get(x_8, 3);
|
||||
|
|
@ -1205,6 +1205,7 @@ x_37 = lean_ctor_get(x_8, 8);
|
|||
x_38 = lean_ctor_get(x_8, 9);
|
||||
x_39 = lean_ctor_get_uint8(x_8, sizeof(void*)*10);
|
||||
x_40 = lean_ctor_get_uint8(x_8, sizeof(void*)*10 + 1);
|
||||
x_41 = lean_ctor_get_uint8(x_8, sizeof(void*)*10 + 2);
|
||||
lean_inc(x_38);
|
||||
lean_inc(x_37);
|
||||
lean_inc(x_36);
|
||||
|
|
@ -1215,72 +1216,73 @@ lean_inc(x_32);
|
|||
lean_inc(x_31);
|
||||
lean_inc(x_30);
|
||||
lean_dec(x_8);
|
||||
x_41 = lean_ctor_get(x_14, 0);
|
||||
lean_inc(x_41);
|
||||
x_42 = lean_ctor_get(x_14, 3);
|
||||
x_42 = lean_ctor_get(x_14, 0);
|
||||
lean_inc(x_42);
|
||||
x_43 = lean_ctor_get(x_14, 4);
|
||||
x_43 = lean_ctor_get(x_14, 3);
|
||||
lean_inc(x_43);
|
||||
x_44 = lean_ctor_get(x_14, 4);
|
||||
lean_inc(x_44);
|
||||
if (lean_is_exclusive(x_14)) {
|
||||
lean_ctor_release(x_14, 0);
|
||||
lean_ctor_release(x_14, 1);
|
||||
lean_ctor_release(x_14, 2);
|
||||
lean_ctor_release(x_14, 3);
|
||||
lean_ctor_release(x_14, 4);
|
||||
x_44 = x_14;
|
||||
x_45 = x_14;
|
||||
} else {
|
||||
lean_dec_ref(x_14);
|
||||
x_44 = lean_box(0);
|
||||
x_45 = lean_box(0);
|
||||
}
|
||||
if (lean_is_scalar(x_44)) {
|
||||
x_45 = lean_alloc_ctor(0, 5, 0);
|
||||
if (lean_is_scalar(x_45)) {
|
||||
x_46 = lean_alloc_ctor(0, 5, 0);
|
||||
} else {
|
||||
x_45 = x_44;
|
||||
x_46 = x_45;
|
||||
}
|
||||
lean_ctor_set(x_45, 0, x_41);
|
||||
lean_ctor_set(x_45, 1, x_16);
|
||||
lean_ctor_set(x_45, 2, x_17);
|
||||
lean_ctor_set(x_45, 3, x_42);
|
||||
lean_ctor_set(x_45, 4, x_43);
|
||||
x_46 = lean_alloc_ctor(0, 10, 2);
|
||||
lean_ctor_set(x_46, 0, x_45);
|
||||
lean_ctor_set(x_46, 1, x_30);
|
||||
lean_ctor_set(x_46, 2, x_31);
|
||||
lean_ctor_set(x_46, 3, x_32);
|
||||
lean_ctor_set(x_46, 4, x_33);
|
||||
lean_ctor_set(x_46, 5, x_34);
|
||||
lean_ctor_set(x_46, 6, x_35);
|
||||
lean_ctor_set(x_46, 7, x_36);
|
||||
lean_ctor_set(x_46, 8, x_37);
|
||||
lean_ctor_set(x_46, 9, x_38);
|
||||
lean_ctor_set_uint8(x_46, sizeof(void*)*10, x_39);
|
||||
lean_ctor_set_uint8(x_46, sizeof(void*)*10 + 1, x_40);
|
||||
x_47 = lean_apply_3(x_7, x_18, x_46, x_15);
|
||||
return x_47;
|
||||
lean_ctor_set(x_46, 0, x_42);
|
||||
lean_ctor_set(x_46, 1, x_16);
|
||||
lean_ctor_set(x_46, 2, x_17);
|
||||
lean_ctor_set(x_46, 3, x_43);
|
||||
lean_ctor_set(x_46, 4, x_44);
|
||||
x_47 = lean_alloc_ctor(0, 10, 3);
|
||||
lean_ctor_set(x_47, 0, x_46);
|
||||
lean_ctor_set(x_47, 1, x_30);
|
||||
lean_ctor_set(x_47, 2, x_31);
|
||||
lean_ctor_set(x_47, 3, x_32);
|
||||
lean_ctor_set(x_47, 4, x_33);
|
||||
lean_ctor_set(x_47, 5, x_34);
|
||||
lean_ctor_set(x_47, 6, x_35);
|
||||
lean_ctor_set(x_47, 7, x_36);
|
||||
lean_ctor_set(x_47, 8, x_37);
|
||||
lean_ctor_set(x_47, 9, x_38);
|
||||
lean_ctor_set_uint8(x_47, sizeof(void*)*10, x_39);
|
||||
lean_ctor_set_uint8(x_47, sizeof(void*)*10 + 1, x_40);
|
||||
lean_ctor_set_uint8(x_47, sizeof(void*)*10 + 2, x_41);
|
||||
x_48 = lean_apply_3(x_7, x_18, x_47, x_15);
|
||||
return x_48;
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
uint8_t x_48;
|
||||
uint8_t x_49;
|
||||
lean_dec(x_8);
|
||||
lean_dec(x_7);
|
||||
x_48 = !lean_is_exclusive(x_11);
|
||||
if (x_48 == 0)
|
||||
x_49 = !lean_is_exclusive(x_11);
|
||||
if (x_49 == 0)
|
||||
{
|
||||
return x_11;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_49; lean_object* x_50; lean_object* x_51;
|
||||
x_49 = lean_ctor_get(x_11, 0);
|
||||
x_50 = lean_ctor_get(x_11, 1);
|
||||
lean_object* x_50; lean_object* x_51; lean_object* x_52;
|
||||
x_50 = lean_ctor_get(x_11, 0);
|
||||
x_51 = lean_ctor_get(x_11, 1);
|
||||
lean_inc(x_51);
|
||||
lean_inc(x_50);
|
||||
lean_inc(x_49);
|
||||
lean_dec(x_11);
|
||||
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;
|
||||
x_52 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_52, 0, x_50);
|
||||
lean_ctor_set(x_52, 1, x_51);
|
||||
return x_52;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
@ -1729,44 +1731,44 @@ return x_92;
|
|||
lean_object* l_Lean_Elab_Command_mkDef(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) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_10; lean_object* x_11; lean_object* x_12;
|
||||
lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13;
|
||||
x_10 = lean_ctor_get(x_1, 0);
|
||||
lean_inc(x_10);
|
||||
x_11 = lean_ctor_get(x_1, 5);
|
||||
lean_inc(x_11);
|
||||
lean_inc(x_6);
|
||||
x_11 = lean_alloc_ctor(1, 1, 0);
|
||||
lean_ctor_set(x_11, 0, x_6);
|
||||
x_12 = lean_alloc_ctor(1, 1, 0);
|
||||
lean_ctor_set(x_12, 0, x_6);
|
||||
lean_inc(x_8);
|
||||
lean_inc(x_10);
|
||||
x_12 = l_Lean_Elab_Term_ensureHasType(x_10, x_11, x_7, x_8, x_9);
|
||||
if (lean_obj_tag(x_12) == 0)
|
||||
lean_inc(x_11);
|
||||
x_13 = l_Lean_Elab_Term_ensureHasType(x_11, x_12, x_7, x_8, x_9);
|
||||
if (lean_obj_tag(x_13) == 0)
|
||||
{
|
||||
lean_object* x_13; lean_object* x_14; uint8_t x_15; lean_object* x_16; lean_object* x_17;
|
||||
x_13 = lean_ctor_get(x_12, 0);
|
||||
lean_inc(x_13);
|
||||
x_14 = lean_ctor_get(x_12, 1);
|
||||
lean_object* x_14; lean_object* x_15; uint8_t x_16; lean_object* x_17; lean_object* x_18;
|
||||
x_14 = lean_ctor_get(x_13, 0);
|
||||
lean_inc(x_14);
|
||||
lean_dec(x_12);
|
||||
x_15 = 0;
|
||||
x_16 = lean_box(0);
|
||||
x_15 = lean_ctor_get(x_13, 1);
|
||||
lean_inc(x_15);
|
||||
lean_dec(x_13);
|
||||
x_16 = 0;
|
||||
x_17 = lean_box(0);
|
||||
lean_inc(x_8);
|
||||
x_17 = l___private_Init_Lean_Elab_SynthesizeSyntheticMVars_11__synthesizeSyntheticMVarsAux___main(x_15, x_16, x_8, x_14);
|
||||
if (lean_obj_tag(x_17) == 0)
|
||||
x_18 = l___private_Init_Lean_Elab_SynthesizeSyntheticMVars_11__synthesizeSyntheticMVarsAux___main(x_16, x_17, x_8, x_15);
|
||||
if (lean_obj_tag(x_18) == 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; uint8_t x_24;
|
||||
x_18 = lean_ctor_get(x_17, 1);
|
||||
lean_inc(x_18);
|
||||
lean_dec(x_17);
|
||||
lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; uint8_t x_24;
|
||||
x_19 = lean_ctor_get(x_18, 1);
|
||||
lean_inc(x_19);
|
||||
lean_dec(x_18);
|
||||
lean_inc(x_8);
|
||||
x_19 = l_Lean_Elab_Term_instantiateMVars(x_10, x_6, x_8, x_18);
|
||||
x_20 = lean_ctor_get(x_19, 0);
|
||||
lean_inc(x_20);
|
||||
x_21 = lean_ctor_get(x_19, 1);
|
||||
x_20 = l_Lean_Elab_Term_instantiateMVars(x_10, x_6, x_8, x_19);
|
||||
x_21 = lean_ctor_get(x_20, 0);
|
||||
lean_inc(x_21);
|
||||
lean_dec(x_19);
|
||||
x_22 = lean_ctor_get(x_1, 5);
|
||||
x_22 = lean_ctor_get(x_20, 1);
|
||||
lean_inc(x_22);
|
||||
lean_dec(x_20);
|
||||
lean_inc(x_8);
|
||||
x_23 = l_Lean_Elab_Term_instantiateMVars(x_22, x_13, x_8, x_21);
|
||||
x_23 = l_Lean_Elab_Term_instantiateMVars(x_11, x_14, x_8, x_22);
|
||||
x_24 = !lean_is_exclusive(x_23);
|
||||
if (x_24 == 0)
|
||||
{
|
||||
|
|
@ -1782,20 +1784,20 @@ lean_free_object(x_23);
|
|||
x_29 = l_Lean_Elab_Command_DefKind_isDefOrOpaque(x_27);
|
||||
x_30 = lean_box(x_27);
|
||||
lean_inc(x_25);
|
||||
lean_inc(x_20);
|
||||
lean_inc(x_21);
|
||||
lean_inc(x_5);
|
||||
lean_inc(x_10);
|
||||
x_31 = lean_alloc_closure((void*)(l_Lean_Elab_Command_mkDef___lambda__1___boxed), 12, 9);
|
||||
lean_closure_set(x_31, 0, x_10);
|
||||
lean_closure_set(x_31, 1, x_5);
|
||||
lean_closure_set(x_31, 2, x_20);
|
||||
lean_closure_set(x_31, 2, x_21);
|
||||
lean_closure_set(x_31, 3, x_25);
|
||||
lean_closure_set(x_31, 4, x_22);
|
||||
lean_closure_set(x_31, 4, x_11);
|
||||
lean_closure_set(x_31, 5, x_3);
|
||||
lean_closure_set(x_31, 6, x_30);
|
||||
lean_closure_set(x_31, 7, x_2);
|
||||
lean_closure_set(x_31, 8, x_1);
|
||||
x_32 = l_Lean_Elab_Command_withUsedWhen___rarg(x_10, x_4, x_5, x_25, x_20, x_29, x_31, x_8, x_26);
|
||||
x_32 = l_Lean_Elab_Command_withUsedWhen___rarg(x_10, x_4, x_5, x_25, x_21, x_29, x_31, x_8, x_26);
|
||||
lean_dec(x_5);
|
||||
lean_dec(x_10);
|
||||
return x_32;
|
||||
|
|
@ -1804,8 +1806,8 @@ else
|
|||
{
|
||||
lean_object* x_33;
|
||||
lean_dec(x_25);
|
||||
lean_dec(x_22);
|
||||
lean_dec(x_20);
|
||||
lean_dec(x_21);
|
||||
lean_dec(x_11);
|
||||
lean_dec(x_10);
|
||||
lean_dec(x_8);
|
||||
lean_dec(x_5);
|
||||
|
|
@ -1834,20 +1836,20 @@ uint8_t x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41;
|
|||
x_38 = l_Lean_Elab_Command_DefKind_isDefOrOpaque(x_36);
|
||||
x_39 = lean_box(x_36);
|
||||
lean_inc(x_34);
|
||||
lean_inc(x_20);
|
||||
lean_inc(x_21);
|
||||
lean_inc(x_5);
|
||||
lean_inc(x_10);
|
||||
x_40 = lean_alloc_closure((void*)(l_Lean_Elab_Command_mkDef___lambda__1___boxed), 12, 9);
|
||||
lean_closure_set(x_40, 0, x_10);
|
||||
lean_closure_set(x_40, 1, x_5);
|
||||
lean_closure_set(x_40, 2, x_20);
|
||||
lean_closure_set(x_40, 2, x_21);
|
||||
lean_closure_set(x_40, 3, x_34);
|
||||
lean_closure_set(x_40, 4, x_22);
|
||||
lean_closure_set(x_40, 4, x_11);
|
||||
lean_closure_set(x_40, 5, x_3);
|
||||
lean_closure_set(x_40, 6, x_39);
|
||||
lean_closure_set(x_40, 7, x_2);
|
||||
lean_closure_set(x_40, 8, x_1);
|
||||
x_41 = l_Lean_Elab_Command_withUsedWhen___rarg(x_10, x_4, x_5, x_34, x_20, x_38, x_40, x_8, x_35);
|
||||
x_41 = l_Lean_Elab_Command_withUsedWhen___rarg(x_10, x_4, x_5, x_34, x_21, x_38, x_40, x_8, x_35);
|
||||
lean_dec(x_5);
|
||||
lean_dec(x_10);
|
||||
return x_41;
|
||||
|
|
@ -1856,8 +1858,8 @@ else
|
|||
{
|
||||
lean_object* x_42; lean_object* x_43;
|
||||
lean_dec(x_34);
|
||||
lean_dec(x_22);
|
||||
lean_dec(x_20);
|
||||
lean_dec(x_21);
|
||||
lean_dec(x_11);
|
||||
lean_dec(x_10);
|
||||
lean_dec(x_8);
|
||||
lean_dec(x_5);
|
||||
|
|
@ -1876,7 +1878,8 @@ return x_43;
|
|||
else
|
||||
{
|
||||
uint8_t x_44;
|
||||
lean_dec(x_13);
|
||||
lean_dec(x_14);
|
||||
lean_dec(x_11);
|
||||
lean_dec(x_10);
|
||||
lean_dec(x_8);
|
||||
lean_dec(x_6);
|
||||
|
|
@ -1885,19 +1888,19 @@ lean_dec(x_4);
|
|||
lean_dec(x_3);
|
||||
lean_dec(x_2);
|
||||
lean_dec(x_1);
|
||||
x_44 = !lean_is_exclusive(x_17);
|
||||
x_44 = !lean_is_exclusive(x_18);
|
||||
if (x_44 == 0)
|
||||
{
|
||||
return x_17;
|
||||
return x_18;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_45; lean_object* x_46; lean_object* x_47;
|
||||
x_45 = lean_ctor_get(x_17, 0);
|
||||
x_46 = lean_ctor_get(x_17, 1);
|
||||
x_45 = lean_ctor_get(x_18, 0);
|
||||
x_46 = lean_ctor_get(x_18, 1);
|
||||
lean_inc(x_46);
|
||||
lean_inc(x_45);
|
||||
lean_dec(x_17);
|
||||
lean_dec(x_18);
|
||||
x_47 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_47, 0, x_45);
|
||||
lean_ctor_set(x_47, 1, x_46);
|
||||
|
|
@ -1908,6 +1911,7 @@ return x_47;
|
|||
else
|
||||
{
|
||||
uint8_t x_48;
|
||||
lean_dec(x_11);
|
||||
lean_dec(x_10);
|
||||
lean_dec(x_8);
|
||||
lean_dec(x_6);
|
||||
|
|
@ -1916,19 +1920,19 @@ lean_dec(x_4);
|
|||
lean_dec(x_3);
|
||||
lean_dec(x_2);
|
||||
lean_dec(x_1);
|
||||
x_48 = !lean_is_exclusive(x_12);
|
||||
x_48 = !lean_is_exclusive(x_13);
|
||||
if (x_48 == 0)
|
||||
{
|
||||
return x_12;
|
||||
return x_13;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_49; lean_object* x_50; lean_object* x_51;
|
||||
x_49 = lean_ctor_get(x_12, 0);
|
||||
x_50 = lean_ctor_get(x_12, 1);
|
||||
x_49 = lean_ctor_get(x_13, 0);
|
||||
x_50 = lean_ctor_get(x_13, 1);
|
||||
lean_inc(x_50);
|
||||
lean_inc(x_49);
|
||||
lean_dec(x_12);
|
||||
lean_dec(x_13);
|
||||
x_51 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_51, 0, x_49);
|
||||
lean_ctor_set(x_51, 1, x_50);
|
||||
|
|
|
|||
1833
stage0/stdlib/Init/Lean/Elab/Match.c
Normal file
1833
stage0/stdlib/Init/Lean/Elab/Match.c
Normal file
File diff suppressed because it is too large
Load diff
File diff suppressed because it is too large
Load diff
File diff suppressed because it is too large
Load diff
File diff suppressed because it is too large
Load diff
File diff suppressed because it is too large
Load diff
|
|
@ -159,7 +159,7 @@ return x_23;
|
|||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; uint8_t x_34; uint8_t x_35; lean_object* x_36; uint8_t x_37; lean_object* x_38;
|
||||
lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; uint8_t x_34; uint8_t x_35; uint8_t x_36; lean_object* x_37; uint8_t x_38; lean_object* x_39;
|
||||
x_24 = lean_ctor_get(x_4, 0);
|
||||
x_25 = lean_ctor_get(x_4, 1);
|
||||
x_26 = lean_ctor_get(x_4, 2);
|
||||
|
|
@ -171,6 +171,7 @@ x_31 = lean_ctor_get(x_4, 7);
|
|||
x_32 = lean_ctor_get(x_4, 8);
|
||||
x_33 = lean_ctor_get(x_4, 9);
|
||||
x_34 = lean_ctor_get_uint8(x_4, sizeof(void*)*10);
|
||||
x_35 = lean_ctor_get_uint8(x_4, sizeof(void*)*10 + 2);
|
||||
lean_inc(x_33);
|
||||
lean_inc(x_32);
|
||||
lean_inc(x_31);
|
||||
|
|
@ -182,98 +183,99 @@ lean_inc(x_26);
|
|||
lean_inc(x_25);
|
||||
lean_inc(x_24);
|
||||
lean_dec(x_4);
|
||||
x_35 = 0;
|
||||
x_36 = lean_alloc_ctor(0, 10, 2);
|
||||
lean_ctor_set(x_36, 0, x_24);
|
||||
lean_ctor_set(x_36, 1, x_25);
|
||||
lean_ctor_set(x_36, 2, x_26);
|
||||
lean_ctor_set(x_36, 3, x_27);
|
||||
lean_ctor_set(x_36, 4, x_28);
|
||||
lean_ctor_set(x_36, 5, x_29);
|
||||
lean_ctor_set(x_36, 6, x_30);
|
||||
lean_ctor_set(x_36, 7, x_31);
|
||||
lean_ctor_set(x_36, 8, x_32);
|
||||
lean_ctor_set(x_36, 9, x_33);
|
||||
lean_ctor_set_uint8(x_36, sizeof(void*)*10, x_34);
|
||||
lean_ctor_set_uint8(x_36, sizeof(void*)*10 + 1, x_35);
|
||||
x_37 = 1;
|
||||
lean_inc(x_36);
|
||||
x_36 = 0;
|
||||
x_37 = lean_alloc_ctor(0, 10, 3);
|
||||
lean_ctor_set(x_37, 0, x_24);
|
||||
lean_ctor_set(x_37, 1, x_25);
|
||||
lean_ctor_set(x_37, 2, x_26);
|
||||
lean_ctor_set(x_37, 3, x_27);
|
||||
lean_ctor_set(x_37, 4, x_28);
|
||||
lean_ctor_set(x_37, 5, x_29);
|
||||
lean_ctor_set(x_37, 6, x_30);
|
||||
lean_ctor_set(x_37, 7, x_31);
|
||||
lean_ctor_set(x_37, 8, x_32);
|
||||
lean_ctor_set(x_37, 9, x_33);
|
||||
lean_ctor_set_uint8(x_37, sizeof(void*)*10, x_34);
|
||||
lean_ctor_set_uint8(x_37, sizeof(void*)*10 + 1, x_36);
|
||||
lean_ctor_set_uint8(x_37, sizeof(void*)*10 + 2, x_35);
|
||||
x_38 = 1;
|
||||
lean_inc(x_37);
|
||||
lean_inc(x_2);
|
||||
x_38 = l_Lean_Elab_Term_elabTermAux___main(x_1, x_37, x_2, x_36, x_5);
|
||||
if (lean_obj_tag(x_38) == 0)
|
||||
x_39 = l_Lean_Elab_Term_elabTermAux___main(x_1, x_38, x_2, x_37, x_5);
|
||||
if (lean_obj_tag(x_39) == 0)
|
||||
{
|
||||
lean_object* x_39; lean_object* x_40; lean_object* x_41; lean_object* x_42;
|
||||
x_39 = lean_ctor_get(x_38, 0);
|
||||
lean_inc(x_39);
|
||||
x_40 = lean_ctor_get(x_38, 1);
|
||||
lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43;
|
||||
x_40 = lean_ctor_get(x_39, 0);
|
||||
lean_inc(x_40);
|
||||
lean_dec(x_38);
|
||||
x_41 = lean_box(0);
|
||||
lean_inc(x_36);
|
||||
x_42 = l___private_Init_Lean_Elab_SynthesizeSyntheticMVars_11__synthesizeSyntheticMVarsAux___main(x_3, x_41, x_36, x_40);
|
||||
if (lean_obj_tag(x_42) == 0)
|
||||
{
|
||||
lean_object* x_43; lean_object* x_44;
|
||||
x_43 = lean_ctor_get(x_42, 1);
|
||||
lean_inc(x_43);
|
||||
lean_dec(x_42);
|
||||
x_44 = l_Lean_Elab_Term_instantiateMVars(x_2, x_39, x_36, x_43);
|
||||
lean_dec(x_2);
|
||||
return x_44;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_45; lean_object* x_46; lean_object* x_47; lean_object* x_48;
|
||||
x_41 = lean_ctor_get(x_39, 1);
|
||||
lean_inc(x_41);
|
||||
lean_dec(x_39);
|
||||
lean_dec(x_36);
|
||||
x_42 = lean_box(0);
|
||||
lean_inc(x_37);
|
||||
x_43 = l___private_Init_Lean_Elab_SynthesizeSyntheticMVars_11__synthesizeSyntheticMVarsAux___main(x_3, x_42, x_37, x_41);
|
||||
if (lean_obj_tag(x_43) == 0)
|
||||
{
|
||||
lean_object* x_44; lean_object* x_45;
|
||||
x_44 = lean_ctor_get(x_43, 1);
|
||||
lean_inc(x_44);
|
||||
lean_dec(x_43);
|
||||
x_45 = l_Lean_Elab_Term_instantiateMVars(x_2, x_40, x_37, x_44);
|
||||
lean_dec(x_2);
|
||||
x_45 = lean_ctor_get(x_42, 0);
|
||||
lean_inc(x_45);
|
||||
x_46 = lean_ctor_get(x_42, 1);
|
||||
return x_45;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_46; lean_object* x_47; lean_object* x_48; lean_object* x_49;
|
||||
lean_dec(x_40);
|
||||
lean_dec(x_37);
|
||||
lean_dec(x_2);
|
||||
x_46 = lean_ctor_get(x_43, 0);
|
||||
lean_inc(x_46);
|
||||
if (lean_is_exclusive(x_42)) {
|
||||
lean_ctor_release(x_42, 0);
|
||||
lean_ctor_release(x_42, 1);
|
||||
x_47 = x_42;
|
||||
x_47 = lean_ctor_get(x_43, 1);
|
||||
lean_inc(x_47);
|
||||
if (lean_is_exclusive(x_43)) {
|
||||
lean_ctor_release(x_43, 0);
|
||||
lean_ctor_release(x_43, 1);
|
||||
x_48 = x_43;
|
||||
} else {
|
||||
lean_dec_ref(x_42);
|
||||
x_47 = lean_box(0);
|
||||
lean_dec_ref(x_43);
|
||||
x_48 = lean_box(0);
|
||||
}
|
||||
if (lean_is_scalar(x_47)) {
|
||||
x_48 = lean_alloc_ctor(1, 2, 0);
|
||||
if (lean_is_scalar(x_48)) {
|
||||
x_49 = lean_alloc_ctor(1, 2, 0);
|
||||
} else {
|
||||
x_48 = x_47;
|
||||
x_49 = x_48;
|
||||
}
|
||||
lean_ctor_set(x_48, 0, x_45);
|
||||
lean_ctor_set(x_48, 1, x_46);
|
||||
return x_48;
|
||||
lean_ctor_set(x_49, 0, x_46);
|
||||
lean_ctor_set(x_49, 1, x_47);
|
||||
return x_49;
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_49; lean_object* x_50; lean_object* x_51; lean_object* x_52;
|
||||
lean_dec(x_36);
|
||||
lean_object* x_50; lean_object* x_51; lean_object* x_52; lean_object* x_53;
|
||||
lean_dec(x_37);
|
||||
lean_dec(x_2);
|
||||
x_49 = lean_ctor_get(x_38, 0);
|
||||
lean_inc(x_49);
|
||||
x_50 = lean_ctor_get(x_38, 1);
|
||||
x_50 = lean_ctor_get(x_39, 0);
|
||||
lean_inc(x_50);
|
||||
if (lean_is_exclusive(x_38)) {
|
||||
lean_ctor_release(x_38, 0);
|
||||
lean_ctor_release(x_38, 1);
|
||||
x_51 = x_38;
|
||||
x_51 = lean_ctor_get(x_39, 1);
|
||||
lean_inc(x_51);
|
||||
if (lean_is_exclusive(x_39)) {
|
||||
lean_ctor_release(x_39, 0);
|
||||
lean_ctor_release(x_39, 1);
|
||||
x_52 = x_39;
|
||||
} else {
|
||||
lean_dec_ref(x_38);
|
||||
x_51 = lean_box(0);
|
||||
lean_dec_ref(x_39);
|
||||
x_52 = lean_box(0);
|
||||
}
|
||||
if (lean_is_scalar(x_51)) {
|
||||
x_52 = lean_alloc_ctor(1, 2, 0);
|
||||
if (lean_is_scalar(x_52)) {
|
||||
x_53 = lean_alloc_ctor(1, 2, 0);
|
||||
} else {
|
||||
x_52 = x_51;
|
||||
x_53 = x_52;
|
||||
}
|
||||
lean_ctor_set(x_52, 0, x_49);
|
||||
lean_ctor_set(x_52, 1, x_50);
|
||||
return x_52;
|
||||
lean_ctor_set(x_53, 0, x_50);
|
||||
lean_ctor_set(x_53, 1, x_51);
|
||||
return x_53;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
|
|||
File diff suppressed because it is too large
Load diff
File diff suppressed because it is too large
Load diff
File diff suppressed because it is too large
Load diff
|
|
@ -46,6 +46,7 @@ lean_object* lean_level_mk_max(lean_object*, lean_object*);
|
|||
lean_object* l_Lean_Level_LevelToFormat_Result_format___main___closed__1;
|
||||
extern lean_object* l_Array_empty___closed__1;
|
||||
lean_object* l_Lean_Level_mkData___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___private_Init_Lean_Level_6__skipExplicit___main(lean_object*, lean_object*);
|
||||
lean_object* l___private_Init_Util_1__mkPanicMessage(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___private_Init_Lean_Level_3__getMaxArgsAux___main___at_Lean_Level_normalize___main___spec__1(lean_object*, uint8_t, lean_object*);
|
||||
lean_object* l_Lean_Level_mkData___closed__1;
|
||||
|
|
@ -54,8 +55,10 @@ lean_object* lean_level_mk_succ(lean_object*);
|
|||
uint8_t l_Lean_Level_hasMVar(lean_object*);
|
||||
lean_object* l_Lean_Level_hasMVarEx___boxed(lean_object*);
|
||||
lean_object* l_Lean_Level_mkData___closed__2;
|
||||
uint8_t l___private_Init_Lean_Level_8__isExplicitSubsumed(lean_object*, lean_object*);
|
||||
uint8_t l_Lean_Level_isEquiv(lean_object*, lean_object*);
|
||||
lean_object* l___private_Init_Lean_Level_3__getMaxArgsAux___main___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___private_Init_Lean_Level_6__skipExplicit(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Level_HasBeq___closed__1;
|
||||
lean_object* l_Lean_Level_dec___main(lean_object*);
|
||||
uint8_t lean_level_has_param(lean_object*);
|
||||
|
|
@ -68,11 +71,11 @@ lean_object* lean_array_push(lean_object*, lean_object*);
|
|||
lean_object* l_Lean_Level_hasParamEx___boxed(lean_object*);
|
||||
lean_object* l_Lean_Level_LevelToFormat_Result_format___main___boxed(lean_object*, lean_object*);
|
||||
lean_object* lean_array_get_size(lean_object*);
|
||||
lean_object* l___private_Init_Lean_Level_6__formatLst___main(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Level_mkData___closed__4;
|
||||
lean_object* l_Nat_max(lean_object*, lean_object*);
|
||||
extern lean_object* l_Lean_Name_inhabited;
|
||||
lean_object* l_Lean_Level_HasToString;
|
||||
lean_object* l___private_Init_Lean_Level_7__isExplicitSubsumedAux___main___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Level_Inhabited;
|
||||
lean_object* l_Lean_Level_getOffsetAux(lean_object*, lean_object*);
|
||||
uint8_t l_Lean_Level_hasParam(lean_object*);
|
||||
|
|
@ -95,7 +98,6 @@ lean_object* l_Lean_Level_ofNat___main___boxed(lean_object*);
|
|||
uint8_t l_Lean_Level_normLtAux___main(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Level_Data_hasMVar___boxed(lean_object*);
|
||||
lean_object* l_Lean_Level_LevelToFormat_toResult(lean_object*);
|
||||
lean_object* l___private_Init_Lean_Level_6__formatLst___main___at_Lean_Level_LevelToFormat_Result_format___main___spec__2(lean_object*);
|
||||
lean_object* l_Lean_Level_occurs___main___boxed(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Level_updateIMax_x21(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_mkLevelIMax(lean_object*, lean_object*);
|
||||
|
|
@ -133,6 +135,7 @@ lean_object* l_Nat_repr(lean_object*);
|
|||
lean_object* l_Lean_Level_addOffsetAux___main(lean_object*, lean_object*);
|
||||
lean_object* l___private_Init_Lean_Level_2__mkIMaxAux(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Level_LevelToFormat_Result_format___main___closed__5;
|
||||
lean_object* l___private_Init_Lean_Level_6__skipExplicit___main___boxed(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Level_toNat___boxed(lean_object*);
|
||||
extern uint64_t l_UInt64_Inhabited;
|
||||
lean_object* l_Lean_Level_addOffset(lean_object*, lean_object*);
|
||||
|
|
@ -144,6 +147,7 @@ lean_object* l_Lean_fmt___at_Lean_Level_LevelToFormat_Result_format___main___spe
|
|||
lean_object* l_Lean_Level_isZero___boxed(lean_object*);
|
||||
lean_object* l_Lean_Level_ctorToNat(lean_object*);
|
||||
lean_object* l_Function_comp___rarg(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___private_Init_Lean_Level_8__isExplicitSubsumed___boxed(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Level_getOffsetAux___main(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Level_ofNat___boxed(lean_object*);
|
||||
lean_object* l_Lean_Level_updateSucc___boxed(lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -162,6 +166,8 @@ lean_object* l_Lean_Level_instantiateParams___main(lean_object*, lean_object*);
|
|||
lean_object* l_Lean_Level_getOffset___boxed(lean_object*);
|
||||
lean_object* l___private_Init_Lean_Level_4__accMax(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_mkLevelMVar(lean_object*);
|
||||
uint8_t l___private_Init_Lean_Level_7__isExplicitSubsumedAux(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___private_Init_Lean_Level_6__skipExplicit___boxed(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Level_normalize___boxed(lean_object*);
|
||||
lean_object* l_Nat_toLevel(lean_object*);
|
||||
uint8_t l_Lean_Level_normLt(lean_object*, lean_object*);
|
||||
|
|
@ -201,19 +207,21 @@ lean_object* lean_level_mk_imax(lean_object*, lean_object*);
|
|||
lean_object* l___private_Init_Lean_Level_5__mkMaxAux(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Nat_imax(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Level_isNeverZero___main___boxed(lean_object*);
|
||||
lean_object* l___private_Init_Lean_Level_7__isExplicitSubsumedAux___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Level_depthEx___boxed(lean_object*);
|
||||
lean_object* lean_level_update_succ(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Level_getLevelOffset(lean_object*);
|
||||
lean_object* l_Lean_Level_LevelToFormat_Result_format___main___closed__3;
|
||||
lean_object* l_Lean_Level_dec___boxed(lean_object*);
|
||||
uint8_t l_Lean_Level_isExplicit___main(lean_object*);
|
||||
lean_object* l___private_Init_Lean_Level_6__formatLst(lean_object*, lean_object*);
|
||||
lean_object* l___private_Init_Lean_Level_9__formatLst(lean_object*, lean_object*);
|
||||
lean_object* l_Array_qsortAux___main___at_Lean_Level_normalize___main___spec__2(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Level_isEquiv___boxed(lean_object*, lean_object*);
|
||||
size_t lean_usize_mix_hash(size_t, size_t);
|
||||
lean_object* lean_level_mk_zero(lean_object*);
|
||||
lean_object* l___private_Init_Lean_Level_3__getMaxArgsAux___main___at_Lean_Level_normalize___main___spec__1___boxed(lean_object*, lean_object*, lean_object*);
|
||||
uint8_t l_Lean_Level_isZero(lean_object*);
|
||||
lean_object* l___private_Init_Lean_Level_9__formatLst___main(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Level_hasParam___boxed(lean_object*);
|
||||
uint8_t l_Lean_Level_occurs(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Level_hashEx___boxed(lean_object*);
|
||||
|
|
@ -224,6 +232,7 @@ uint8_t l_Lean_Level_isMaxIMax(lean_object*);
|
|||
extern lean_object* l_Lean_Format_paren___closed__3;
|
||||
lean_object* l_Lean_Level_hash___boxed(lean_object*);
|
||||
lean_object* l_Lean_Level_instantiateParams(lean_object*, lean_object*);
|
||||
uint8_t l___private_Init_Lean_Level_7__isExplicitSubsumedAux___main(lean_object*, lean_object*, lean_object*);
|
||||
uint8_t l_Lean_Level_isSucc(lean_object*);
|
||||
uint8_t l_Lean_Level_isExplicit(lean_object*);
|
||||
extern lean_object* l_System_FilePath_dirName___closed__1;
|
||||
|
|
@ -239,6 +248,7 @@ lean_object* l_Lean_Level_HasToString___closed__1;
|
|||
lean_object* l_Lean_Level_beq___boxed(lean_object*, lean_object*);
|
||||
lean_object* lean_level_mk_mvar(lean_object*);
|
||||
lean_object* l_Lean_Level_format(lean_object*);
|
||||
lean_object* l___private_Init_Lean_Level_9__formatLst___main___at_Lean_Level_LevelToFormat_Result_format___main___spec__2(lean_object*);
|
||||
uint8_t l_Lean_Level_isNeverZero___main(lean_object*);
|
||||
lean_object* lean_uint32_to_nat(uint32_t);
|
||||
lean_object* l_Lean_Level_HasBeq;
|
||||
|
|
@ -2591,6 +2601,178 @@ lean_dec(x_1);
|
|||
return x_7;
|
||||
}
|
||||
}
|
||||
lean_object* l___private_Init_Lean_Level_6__skipExplicit___main(lean_object* x_1, lean_object* x_2) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_3; uint8_t x_4;
|
||||
x_3 = lean_array_get_size(x_1);
|
||||
x_4 = lean_nat_dec_lt(x_2, x_3);
|
||||
lean_dec(x_3);
|
||||
if (x_4 == 0)
|
||||
{
|
||||
return x_2;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_5; lean_object* x_6; uint8_t x_7;
|
||||
x_5 = lean_array_fget(x_1, x_2);
|
||||
x_6 = l_Lean_Level_getLevelOffset___main(x_5);
|
||||
lean_dec(x_5);
|
||||
x_7 = l_Lean_Level_isZero(x_6);
|
||||
lean_dec(x_6);
|
||||
if (x_7 == 0)
|
||||
{
|
||||
return x_2;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_8; lean_object* x_9;
|
||||
x_8 = lean_unsigned_to_nat(1u);
|
||||
x_9 = lean_nat_add(x_2, x_8);
|
||||
lean_dec(x_2);
|
||||
x_2 = x_9;
|
||||
goto _start;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
lean_object* l___private_Init_Lean_Level_6__skipExplicit___main___boxed(lean_object* x_1, lean_object* x_2) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_3;
|
||||
x_3 = l___private_Init_Lean_Level_6__skipExplicit___main(x_1, x_2);
|
||||
lean_dec(x_1);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
lean_object* l___private_Init_Lean_Level_6__skipExplicit(lean_object* x_1, lean_object* x_2) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_3;
|
||||
x_3 = l___private_Init_Lean_Level_6__skipExplicit___main(x_1, x_2);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
lean_object* l___private_Init_Lean_Level_6__skipExplicit___boxed(lean_object* x_1, lean_object* x_2) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_3;
|
||||
x_3 = l___private_Init_Lean_Level_6__skipExplicit(x_1, x_2);
|
||||
lean_dec(x_1);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
uint8_t l___private_Init_Lean_Level_7__isExplicitSubsumedAux___main(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_4; uint8_t x_5;
|
||||
x_4 = lean_array_get_size(x_1);
|
||||
x_5 = lean_nat_dec_lt(x_3, x_4);
|
||||
lean_dec(x_4);
|
||||
if (x_5 == 0)
|
||||
{
|
||||
uint8_t x_6;
|
||||
lean_dec(x_3);
|
||||
x_6 = 0;
|
||||
return x_6;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_7; lean_object* x_8; lean_object* x_9; uint8_t x_10;
|
||||
x_7 = lean_array_fget(x_1, x_3);
|
||||
x_8 = lean_unsigned_to_nat(0u);
|
||||
x_9 = l_Lean_Level_getOffsetAux___main(x_7, x_8);
|
||||
lean_dec(x_7);
|
||||
x_10 = lean_nat_dec_le(x_2, x_9);
|
||||
lean_dec(x_9);
|
||||
if (x_10 == 0)
|
||||
{
|
||||
lean_object* x_11; lean_object* x_12;
|
||||
x_11 = lean_unsigned_to_nat(1u);
|
||||
x_12 = lean_nat_add(x_3, x_11);
|
||||
lean_dec(x_3);
|
||||
x_3 = x_12;
|
||||
goto _start;
|
||||
}
|
||||
else
|
||||
{
|
||||
uint8_t x_14;
|
||||
lean_dec(x_3);
|
||||
x_14 = 1;
|
||||
return x_14;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
lean_object* l___private_Init_Lean_Level_7__isExplicitSubsumedAux___main___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
|
||||
_start:
|
||||
{
|
||||
uint8_t x_4; lean_object* x_5;
|
||||
x_4 = l___private_Init_Lean_Level_7__isExplicitSubsumedAux___main(x_1, x_2, x_3);
|
||||
lean_dec(x_2);
|
||||
lean_dec(x_1);
|
||||
x_5 = lean_box(x_4);
|
||||
return x_5;
|
||||
}
|
||||
}
|
||||
uint8_t l___private_Init_Lean_Level_7__isExplicitSubsumedAux(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
|
||||
_start:
|
||||
{
|
||||
uint8_t x_4;
|
||||
x_4 = l___private_Init_Lean_Level_7__isExplicitSubsumedAux___main(x_1, x_2, x_3);
|
||||
return x_4;
|
||||
}
|
||||
}
|
||||
lean_object* l___private_Init_Lean_Level_7__isExplicitSubsumedAux___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
|
||||
_start:
|
||||
{
|
||||
uint8_t x_4; lean_object* x_5;
|
||||
x_4 = l___private_Init_Lean_Level_7__isExplicitSubsumedAux(x_1, x_2, x_3);
|
||||
lean_dec(x_2);
|
||||
lean_dec(x_1);
|
||||
x_5 = lean_box(x_4);
|
||||
return x_5;
|
||||
}
|
||||
}
|
||||
uint8_t l___private_Init_Lean_Level_8__isExplicitSubsumed(lean_object* x_1, lean_object* x_2) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_3; uint8_t x_4;
|
||||
x_3 = lean_unsigned_to_nat(0u);
|
||||
x_4 = lean_nat_dec_eq(x_2, x_3);
|
||||
if (x_4 == 0)
|
||||
{
|
||||
lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; uint8_t x_10;
|
||||
x_5 = lean_unsigned_to_nat(1u);
|
||||
x_6 = lean_nat_sub(x_2, x_5);
|
||||
x_7 = l_Lean_Level_Inhabited;
|
||||
x_8 = lean_array_get(x_7, x_1, x_6);
|
||||
lean_dec(x_6);
|
||||
x_9 = l_Lean_Level_getOffsetAux___main(x_8, x_3);
|
||||
lean_dec(x_8);
|
||||
x_10 = l___private_Init_Lean_Level_7__isExplicitSubsumedAux___main(x_1, x_9, x_2);
|
||||
lean_dec(x_9);
|
||||
return x_10;
|
||||
}
|
||||
else
|
||||
{
|
||||
uint8_t x_11;
|
||||
lean_dec(x_2);
|
||||
x_11 = 0;
|
||||
return x_11;
|
||||
}
|
||||
}
|
||||
}
|
||||
lean_object* l___private_Init_Lean_Level_8__isExplicitSubsumed___boxed(lean_object* x_1, lean_object* x_2) {
|
||||
_start:
|
||||
{
|
||||
uint8_t x_3; lean_object* x_4;
|
||||
x_3 = l___private_Init_Lean_Level_8__isExplicitSubsumed(x_1, x_2);
|
||||
lean_dec(x_1);
|
||||
x_4 = lean_box(x_3);
|
||||
return x_4;
|
||||
}
|
||||
}
|
||||
lean_object* l___private_Init_Lean_Level_3__getMaxArgsAux___main___at_Lean_Level_normalize___main___spec__1(lean_object* x_1, uint8_t x_2, lean_object* x_3) {
|
||||
_start:
|
||||
{
|
||||
|
|
@ -2830,7 +3012,7 @@ x_5 = l_Lean_Level_getLevelOffset___main(x_1);
|
|||
switch (lean_obj_tag(x_5)) {
|
||||
case 2:
|
||||
{
|
||||
lean_object* x_6; lean_object* x_7; uint8_t x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21;
|
||||
lean_object* x_6; lean_object* x_7; uint8_t x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; uint8_t x_17;
|
||||
x_6 = lean_ctor_get(x_5, 0);
|
||||
lean_inc(x_6);
|
||||
x_7 = lean_ctor_get(x_5, 1);
|
||||
|
|
@ -2846,55 +3028,82 @@ x_14 = lean_nat_sub(x_12, x_13);
|
|||
lean_dec(x_12);
|
||||
x_15 = l_Array_qsortAux___main___at_Lean_Level_normalize___main___spec__2(x_11, x_3, x_14);
|
||||
lean_dec(x_14);
|
||||
x_16 = l_Lean_Level_Inhabited;
|
||||
x_17 = lean_array_get(x_16, x_15, x_3);
|
||||
x_18 = l_Lean_Level_getLevelOffset___main(x_17);
|
||||
x_19 = l_Lean_Level_getOffsetAux___main(x_17, x_3);
|
||||
lean_dec(x_17);
|
||||
x_20 = l_Lean_levelZero;
|
||||
x_21 = l___private_Init_Lean_Level_5__mkMaxAux___main(x_15, x_4, x_13, x_18, x_19, x_20);
|
||||
x_16 = l___private_Init_Lean_Level_6__skipExplicit___main(x_15, x_3);
|
||||
lean_inc(x_16);
|
||||
x_17 = l___private_Init_Lean_Level_8__isExplicitSubsumed(x_15, x_16);
|
||||
if (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; lean_object* x_24; lean_object* x_25;
|
||||
x_18 = lean_nat_sub(x_16, x_13);
|
||||
lean_dec(x_16);
|
||||
x_19 = l_Lean_Level_Inhabited;
|
||||
x_20 = lean_array_get(x_19, x_15, x_18);
|
||||
x_21 = l_Lean_Level_getLevelOffset___main(x_20);
|
||||
x_22 = l_Lean_Level_getOffsetAux___main(x_20, x_3);
|
||||
lean_dec(x_20);
|
||||
x_23 = lean_nat_add(x_18, x_13);
|
||||
lean_dec(x_18);
|
||||
x_24 = l_Lean_levelZero;
|
||||
x_25 = l___private_Init_Lean_Level_5__mkMaxAux___main(x_15, x_4, x_23, x_21, x_22, x_24);
|
||||
lean_dec(x_4);
|
||||
lean_dec(x_15);
|
||||
return x_21;
|
||||
}
|
||||
case 3:
|
||||
{
|
||||
lean_object* x_22; lean_object* x_23; uint8_t x_24;
|
||||
x_22 = lean_ctor_get(x_5, 0);
|
||||
lean_inc(x_22);
|
||||
x_23 = lean_ctor_get(x_5, 1);
|
||||
lean_inc(x_23);
|
||||
lean_dec(x_5);
|
||||
x_24 = l_Lean_Level_isNeverZero___main(x_23);
|
||||
if (x_24 == 0)
|
||||
{
|
||||
lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28;
|
||||
x_25 = l_Lean_Level_normalize___main(x_22);
|
||||
lean_dec(x_22);
|
||||
x_26 = l_Lean_Level_normalize___main(x_23);
|
||||
lean_dec(x_23);
|
||||
x_27 = l___private_Init_Lean_Level_2__mkIMaxAux(x_25, x_26);
|
||||
x_28 = l_Lean_Level_addOffsetAux___main(x_4, x_27);
|
||||
return x_28;
|
||||
return x_25;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_29; lean_object* x_30; lean_object* x_31;
|
||||
x_29 = l_Lean_mkLevelMax(x_22, x_23);
|
||||
x_30 = l_Lean_Level_normalize___main(x_29);
|
||||
lean_dec(x_29);
|
||||
x_31 = l_Lean_Level_addOffsetAux___main(x_4, x_30);
|
||||
return x_31;
|
||||
lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32;
|
||||
x_26 = l_Lean_Level_Inhabited;
|
||||
x_27 = lean_array_get(x_26, x_15, x_16);
|
||||
x_28 = l_Lean_Level_getLevelOffset___main(x_27);
|
||||
x_29 = l_Lean_Level_getOffsetAux___main(x_27, x_3);
|
||||
lean_dec(x_27);
|
||||
x_30 = lean_nat_add(x_16, x_13);
|
||||
lean_dec(x_16);
|
||||
x_31 = l_Lean_levelZero;
|
||||
x_32 = l___private_Init_Lean_Level_5__mkMaxAux___main(x_15, x_4, x_30, x_28, x_29, x_31);
|
||||
lean_dec(x_4);
|
||||
lean_dec(x_15);
|
||||
return x_32;
|
||||
}
|
||||
}
|
||||
case 3:
|
||||
{
|
||||
lean_object* x_33; lean_object* x_34; uint8_t x_35;
|
||||
x_33 = lean_ctor_get(x_5, 0);
|
||||
lean_inc(x_33);
|
||||
x_34 = lean_ctor_get(x_5, 1);
|
||||
lean_inc(x_34);
|
||||
lean_dec(x_5);
|
||||
x_35 = l_Lean_Level_isNeverZero___main(x_34);
|
||||
if (x_35 == 0)
|
||||
{
|
||||
lean_object* x_36; lean_object* x_37; lean_object* x_38; lean_object* x_39;
|
||||
x_36 = l_Lean_Level_normalize___main(x_33);
|
||||
lean_dec(x_33);
|
||||
x_37 = l_Lean_Level_normalize___main(x_34);
|
||||
lean_dec(x_34);
|
||||
x_38 = l___private_Init_Lean_Level_2__mkIMaxAux(x_36, x_37);
|
||||
x_39 = l_Lean_Level_addOffsetAux___main(x_4, x_38);
|
||||
return x_39;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_40; lean_object* x_41; lean_object* x_42;
|
||||
x_40 = l_Lean_mkLevelMax(x_33, x_34);
|
||||
x_41 = l_Lean_Level_normalize___main(x_40);
|
||||
lean_dec(x_40);
|
||||
x_42 = l_Lean_Level_addOffsetAux___main(x_4, x_41);
|
||||
return x_42;
|
||||
}
|
||||
}
|
||||
default:
|
||||
{
|
||||
lean_object* x_32; lean_object* x_33;
|
||||
lean_object* x_43; lean_object* x_44;
|
||||
lean_dec(x_5);
|
||||
lean_dec(x_4);
|
||||
x_32 = l_Lean_Level_Inhabited;
|
||||
x_33 = l_unreachable_x21___rarg(x_32);
|
||||
return x_33;
|
||||
x_43 = l_Lean_Level_Inhabited;
|
||||
x_44 = l_unreachable_x21___rarg(x_43);
|
||||
return x_44;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
@ -3373,7 +3582,7 @@ x_4 = l_Lean_Level_LevelToFormat_parenIfFalse(x_1, x_3);
|
|||
return x_4;
|
||||
}
|
||||
}
|
||||
lean_object* l___private_Init_Lean_Level_6__formatLst___main(lean_object* x_1, lean_object* x_2) {
|
||||
lean_object* l___private_Init_Lean_Level_9__formatLst___main(lean_object* x_1, lean_object* x_2) {
|
||||
_start:
|
||||
{
|
||||
if (lean_obj_tag(x_2) == 0)
|
||||
|
|
@ -3399,7 +3608,7 @@ x_9 = lean_alloc_ctor(4, 2, 1);
|
|||
lean_ctor_set(x_9, 0, x_8);
|
||||
lean_ctor_set(x_9, 1, x_6);
|
||||
lean_ctor_set_uint8(x_9, sizeof(void*)*2, x_7);
|
||||
x_10 = l___private_Init_Lean_Level_6__formatLst___main(x_1, x_5);
|
||||
x_10 = l___private_Init_Lean_Level_9__formatLst___main(x_1, x_5);
|
||||
x_11 = lean_alloc_ctor(4, 2, 1);
|
||||
lean_ctor_set(x_11, 0, x_9);
|
||||
lean_ctor_set(x_11, 1, x_10);
|
||||
|
|
@ -3408,11 +3617,11 @@ return x_11;
|
|||
}
|
||||
}
|
||||
}
|
||||
lean_object* l___private_Init_Lean_Level_6__formatLst(lean_object* x_1, lean_object* x_2) {
|
||||
lean_object* l___private_Init_Lean_Level_9__formatLst(lean_object* x_1, lean_object* x_2) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_3;
|
||||
x_3 = l___private_Init_Lean_Level_6__formatLst___main(x_1, x_2);
|
||||
x_3 = l___private_Init_Lean_Level_9__formatLst___main(x_1, x_2);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
|
|
@ -3426,7 +3635,7 @@ lean_ctor_set(x_3, 0, x_2);
|
|||
return x_3;
|
||||
}
|
||||
}
|
||||
lean_object* l___private_Init_Lean_Level_6__formatLst___main___at_Lean_Level_LevelToFormat_Result_format___main___spec__2(lean_object* x_1) {
|
||||
lean_object* l___private_Init_Lean_Level_9__formatLst___main___at_Lean_Level_LevelToFormat_Result_format___main___spec__2(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
if (lean_obj_tag(x_1) == 0)
|
||||
|
|
@ -3450,7 +3659,7 @@ x_8 = lean_alloc_ctor(4, 2, 1);
|
|||
lean_ctor_set(x_8, 0, x_7);
|
||||
lean_ctor_set(x_8, 1, x_6);
|
||||
lean_ctor_set_uint8(x_8, sizeof(void*)*2, x_5);
|
||||
x_9 = l___private_Init_Lean_Level_6__formatLst___main___at_Lean_Level_LevelToFormat_Result_format___main___spec__2(x_4);
|
||||
x_9 = l___private_Init_Lean_Level_9__formatLst___main___at_Lean_Level_LevelToFormat_Result_format___main___spec__2(x_4);
|
||||
x_10 = lean_alloc_ctor(4, 2, 1);
|
||||
lean_ctor_set(x_10, 0, x_8);
|
||||
lean_ctor_set(x_10, 1, x_9);
|
||||
|
|
@ -3582,7 +3791,7 @@ lean_object* x_22; lean_object* x_23; uint8_t x_24; lean_object* x_25; lean_obje
|
|||
x_22 = lean_ctor_get(x_1, 0);
|
||||
lean_inc(x_22);
|
||||
lean_dec(x_1);
|
||||
x_23 = l___private_Init_Lean_Level_6__formatLst___main___at_Lean_Level_LevelToFormat_Result_format___main___spec__2(x_22);
|
||||
x_23 = l___private_Init_Lean_Level_9__formatLst___main___at_Lean_Level_LevelToFormat_Result_format___main___spec__2(x_22);
|
||||
x_24 = 0;
|
||||
x_25 = l_Lean_Level_LevelToFormat_Result_format___main___closed__4;
|
||||
x_26 = lean_alloc_ctor(4, 2, 1);
|
||||
|
|
@ -3599,7 +3808,7 @@ lean_object* x_29; lean_object* x_30; uint8_t x_31; lean_object* x_32; lean_obje
|
|||
x_29 = lean_ctor_get(x_1, 0);
|
||||
lean_inc(x_29);
|
||||
lean_dec(x_1);
|
||||
x_30 = l___private_Init_Lean_Level_6__formatLst___main___at_Lean_Level_LevelToFormat_Result_format___main___spec__2(x_29);
|
||||
x_30 = l___private_Init_Lean_Level_9__formatLst___main___at_Lean_Level_LevelToFormat_Result_format___main___spec__2(x_29);
|
||||
x_31 = 0;
|
||||
x_32 = l_Lean_Level_LevelToFormat_Result_format___main___closed__6;
|
||||
x_33 = lean_alloc_ctor(4, 2, 1);
|
||||
|
|
@ -3798,7 +4007,7 @@ _start:
|
|||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
|
||||
x_1 = l_Lean_Level_mkData___closed__2;
|
||||
x_2 = lean_unsigned_to_nat(403u);
|
||||
x_2 = lean_unsigned_to_nat(437u);
|
||||
x_3 = lean_unsigned_to_nat(16u);
|
||||
x_4 = l_Lean_Level_updateSucc_x21___closed__1;
|
||||
x_5 = l___private_Init_Util_1__mkPanicMessage(x_1, x_2, x_3, x_4);
|
||||
|
|
@ -3847,7 +4056,7 @@ _start:
|
|||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
|
||||
x_1 = l_Lean_Level_mkData___closed__2;
|
||||
x_2 = lean_unsigned_to_nat(412u);
|
||||
x_2 = lean_unsigned_to_nat(446u);
|
||||
x_3 = lean_unsigned_to_nat(19u);
|
||||
x_4 = l_Lean_Level_updateMax_x21___closed__1;
|
||||
x_5 = l___private_Init_Util_1__mkPanicMessage(x_1, x_2, x_3, x_4);
|
||||
|
|
@ -3897,7 +4106,7 @@ _start:
|
|||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
|
||||
x_1 = l_Lean_Level_mkData___closed__2;
|
||||
x_2 = lean_unsigned_to_nat(421u);
|
||||
x_2 = lean_unsigned_to_nat(455u);
|
||||
x_3 = lean_unsigned_to_nat(20u);
|
||||
x_4 = l_Lean_Level_updateIMax_x21___closed__1;
|
||||
x_5 = l___private_Init_Util_1__mkPanicMessage(x_1, x_2, x_3, x_4);
|
||||
|
|
|
|||
|
|
@ -156,6 +156,7 @@ lean_object* l_Array_iterateMAux___main___at_Lean_Parser_SyntaxNodeKindSet_inser
|
|||
lean_object* l_Lean_Parser_ParserState_next(lean_object*, lean_object*, lean_object*);
|
||||
extern lean_object* l_Prod_HasRepr___rarg___closed__1;
|
||||
lean_object* l_Array_extract___rarg(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_setExpected___elambda__1___boxed(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_addParser(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_PrattParsingTables_inhabited;
|
||||
lean_object* l_Lean_Parser_categoryParserFnRef;
|
||||
|
|
@ -299,6 +300,7 @@ lean_object* l_Lean_Parser_declareBuiltinParser___closed__4;
|
|||
lean_object* l_Lean_Parser_nameLitFn(uint8_t, lean_object*);
|
||||
lean_object* l_Lean_Parser_quotedSymbolFn(uint8_t);
|
||||
lean_object* l_Lean_Parser_quotedSymbolFn___rarg___closed__4;
|
||||
lean_object* l_Lean_Parser_setExpected___elambda__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
extern lean_object* l_Nat_HasOfNat___closed__1;
|
||||
lean_object* l_Lean_Parser_categoryParserFnExtension___elambda__1___rarg(lean_object*);
|
||||
lean_object* l_Lean_Parser_takeUntilFn___main(lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -362,6 +364,7 @@ lean_object* l_Lean_Parser_rawIdentFn(lean_object*, lean_object*);
|
|||
lean_object* l_Lean_Parser_takeUntilFn___main___boxed(lean_object*, lean_object*, lean_object*);
|
||||
uint8_t l_Lean_Parser_leadingIdentAsSymbol(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_indexed(lean_object*);
|
||||
lean_object* l_Lean_Parser_setExpectedFn___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_strLit___elambda__1(uint8_t);
|
||||
extern lean_object* l_Lean_mkTermIdFromIdent___closed__2;
|
||||
lean_object* l_Array_foldlStepMAux___main___at_Lean_Syntax_foldSepArgs___spec__1(lean_object*);
|
||||
|
|
@ -406,6 +409,7 @@ extern lean_object* l_Lean_Parser_Trie_HasEmptyc___closed__1;
|
|||
lean_object* l_Lean_Parser_mkIdResult___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_fieldIdx___closed__1;
|
||||
lean_object* l_Lean_Parser_TokenMap_insert(lean_object*);
|
||||
lean_object* l_Lean_Parser_setExpected___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_unicodeSymbol(uint8_t, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_longestMatchFn___closed__1;
|
||||
lean_object* l_Lean_Parser_termParser___boxed(lean_object*, lean_object*);
|
||||
|
|
@ -468,6 +472,7 @@ lean_object* l_Lean_Parser_quotedSymbolFn___rarg___closed__3;
|
|||
lean_object* l_Lean_Parser_quotedSymbol(uint8_t);
|
||||
lean_object* l_Lean_Parser_numLitNoAntiquot___closed__1;
|
||||
lean_object* lean_nat_sub(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_setExpected(uint8_t, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_ParserState_keepLatest(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_checkLeadingFn___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_declareBuiltinParser(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -560,6 +565,7 @@ lean_object* l_Lean_Parser_andthenFn___rarg(lean_object*, lean_object*, lean_obj
|
|||
lean_object* l_Lean_Parser_longestMatchStep(uint8_t);
|
||||
lean_object* l_Lean_Parser_addLeadingParser___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_charLitNoAntiquot___boxed(lean_object*);
|
||||
lean_object* l_Lean_Parser_setExpectedFn(uint8_t, lean_object*);
|
||||
lean_object* l_Lean_Parser_strLitFn(uint8_t, lean_object*);
|
||||
lean_object* l_Lean_Parser_mkParserExtension___lambda__2___boxed(lean_object*);
|
||||
lean_object* l_Lean_Parser_nodeFn___boxed(lean_object*);
|
||||
|
|
@ -896,6 +902,7 @@ lean_object* l_Lean_Parser_FirstTokens_toStr___closed__1;
|
|||
lean_object* l_Lean_Parser_runParserCategory(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_iterateMAux___main___at_Lean_Parser_getSyntaxNodeKinds___spec__4(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_addLeadingParser(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_setExpectedFn___boxed(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_quotedSymbolFn___boxed(lean_object*);
|
||||
uint8_t l_PersistentHashMap_containsAtAux___main___at_Lean_Parser_isValidSyntaxNodeKind___spec__3(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___private_Init_Lean_Parser_Parser_13__antiquotNestedExpr___closed__5;
|
||||
|
|
@ -1145,6 +1152,7 @@ uint8_t l___private_Init_Lean_Parser_Parser_5__isIdFirstOrBeginEscape(uint32_t);
|
|||
lean_object* l_Lean_Parser_mkParserOfConstantUnsafe___closed__3;
|
||||
lean_object* l_RBNode_ins___main___at_Lean_Parser_TokenMap_insert___spec__4(lean_object*);
|
||||
lean_object* l_List_toStringAux___main___at_Lean_Parser_FirstTokens_toStr___spec__2___boxed(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_setExpected___elambda__1(uint8_t, lean_object*);
|
||||
lean_object* l_RBNode_insert___at_Lean_Parser_TokenMap_insert___spec__5___rarg(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_unicodeSymbolInfo___closed__1;
|
||||
lean_object* l_Lean_Parser_checkColGe___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -26271,6 +26279,237 @@ x_3 = l___private_Init_Lean_Parser_Parser_11__noImmediateColon(x_2);
|
|||
return x_3;
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_Parser_setExpectedFn___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_5; lean_object* x_6;
|
||||
x_5 = lean_apply_3(x_1, x_2, x_3, x_4);
|
||||
x_6 = lean_ctor_get(x_5, 3);
|
||||
lean_inc(x_6);
|
||||
if (lean_obj_tag(x_6) == 0)
|
||||
{
|
||||
return x_5;
|
||||
}
|
||||
else
|
||||
{
|
||||
uint8_t x_7;
|
||||
x_7 = !lean_is_exclusive(x_6);
|
||||
if (x_7 == 0)
|
||||
{
|
||||
uint8_t x_8;
|
||||
x_8 = !lean_is_exclusive(x_5);
|
||||
if (x_8 == 0)
|
||||
{
|
||||
lean_object* x_9; lean_object* x_10; uint8_t x_11;
|
||||
x_9 = lean_ctor_get(x_6, 0);
|
||||
x_10 = lean_ctor_get(x_5, 3);
|
||||
lean_dec(x_10);
|
||||
x_11 = !lean_is_exclusive(x_9);
|
||||
if (x_11 == 0)
|
||||
{
|
||||
lean_object* x_12; lean_object* x_13;
|
||||
x_12 = lean_ctor_get(x_9, 1);
|
||||
lean_dec(x_12);
|
||||
x_13 = lean_box(0);
|
||||
lean_ctor_set(x_9, 1, x_13);
|
||||
return x_5;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_14; lean_object* x_15; lean_object* x_16;
|
||||
x_14 = lean_ctor_get(x_9, 0);
|
||||
lean_inc(x_14);
|
||||
lean_dec(x_9);
|
||||
x_15 = lean_box(0);
|
||||
x_16 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_16, 0, x_14);
|
||||
lean_ctor_set(x_16, 1, x_15);
|
||||
lean_ctor_set(x_6, 0, x_16);
|
||||
return x_5;
|
||||
}
|
||||
}
|
||||
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; lean_object* x_24; lean_object* x_25;
|
||||
x_17 = lean_ctor_get(x_6, 0);
|
||||
x_18 = lean_ctor_get(x_5, 0);
|
||||
x_19 = lean_ctor_get(x_5, 1);
|
||||
x_20 = lean_ctor_get(x_5, 2);
|
||||
lean_inc(x_20);
|
||||
lean_inc(x_19);
|
||||
lean_inc(x_18);
|
||||
lean_dec(x_5);
|
||||
x_21 = lean_ctor_get(x_17, 0);
|
||||
lean_inc(x_21);
|
||||
if (lean_is_exclusive(x_17)) {
|
||||
lean_ctor_release(x_17, 0);
|
||||
lean_ctor_release(x_17, 1);
|
||||
x_22 = x_17;
|
||||
} else {
|
||||
lean_dec_ref(x_17);
|
||||
x_22 = lean_box(0);
|
||||
}
|
||||
x_23 = lean_box(0);
|
||||
if (lean_is_scalar(x_22)) {
|
||||
x_24 = lean_alloc_ctor(0, 2, 0);
|
||||
} else {
|
||||
x_24 = x_22;
|
||||
}
|
||||
lean_ctor_set(x_24, 0, x_21);
|
||||
lean_ctor_set(x_24, 1, x_23);
|
||||
lean_ctor_set(x_6, 0, x_24);
|
||||
x_25 = lean_alloc_ctor(0, 4, 0);
|
||||
lean_ctor_set(x_25, 0, x_18);
|
||||
lean_ctor_set(x_25, 1, x_19);
|
||||
lean_ctor_set(x_25, 2, x_20);
|
||||
lean_ctor_set(x_25, 3, x_6);
|
||||
return x_25;
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_26; lean_object* x_27; 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; lean_object* x_36;
|
||||
x_26 = lean_ctor_get(x_6, 0);
|
||||
lean_inc(x_26);
|
||||
lean_dec(x_6);
|
||||
x_27 = lean_ctor_get(x_5, 0);
|
||||
lean_inc(x_27);
|
||||
x_28 = lean_ctor_get(x_5, 1);
|
||||
lean_inc(x_28);
|
||||
x_29 = lean_ctor_get(x_5, 2);
|
||||
lean_inc(x_29);
|
||||
if (lean_is_exclusive(x_5)) {
|
||||
lean_ctor_release(x_5, 0);
|
||||
lean_ctor_release(x_5, 1);
|
||||
lean_ctor_release(x_5, 2);
|
||||
lean_ctor_release(x_5, 3);
|
||||
x_30 = x_5;
|
||||
} else {
|
||||
lean_dec_ref(x_5);
|
||||
x_30 = lean_box(0);
|
||||
}
|
||||
x_31 = lean_ctor_get(x_26, 0);
|
||||
lean_inc(x_31);
|
||||
if (lean_is_exclusive(x_26)) {
|
||||
lean_ctor_release(x_26, 0);
|
||||
lean_ctor_release(x_26, 1);
|
||||
x_32 = x_26;
|
||||
} else {
|
||||
lean_dec_ref(x_26);
|
||||
x_32 = lean_box(0);
|
||||
}
|
||||
x_33 = lean_box(0);
|
||||
if (lean_is_scalar(x_32)) {
|
||||
x_34 = lean_alloc_ctor(0, 2, 0);
|
||||
} else {
|
||||
x_34 = x_32;
|
||||
}
|
||||
lean_ctor_set(x_34, 0, x_31);
|
||||
lean_ctor_set(x_34, 1, x_33);
|
||||
x_35 = lean_alloc_ctor(1, 1, 0);
|
||||
lean_ctor_set(x_35, 0, x_34);
|
||||
if (lean_is_scalar(x_30)) {
|
||||
x_36 = lean_alloc_ctor(0, 4, 0);
|
||||
} else {
|
||||
x_36 = x_30;
|
||||
}
|
||||
lean_ctor_set(x_36, 0, x_27);
|
||||
lean_ctor_set(x_36, 1, x_28);
|
||||
lean_ctor_set(x_36, 2, x_29);
|
||||
lean_ctor_set(x_36, 3, x_35);
|
||||
return x_36;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_Parser_setExpectedFn(uint8_t x_1, lean_object* x_2) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_3;
|
||||
x_3 = lean_alloc_closure((void*)(l_Lean_Parser_setExpectedFn___rarg), 4, 0);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_Parser_setExpectedFn___boxed(lean_object* x_1, lean_object* x_2) {
|
||||
_start:
|
||||
{
|
||||
uint8_t x_3; lean_object* x_4;
|
||||
x_3 = lean_unbox(x_1);
|
||||
lean_dec(x_1);
|
||||
x_4 = l_Lean_Parser_setExpectedFn(x_3, x_2);
|
||||
lean_dec(x_2);
|
||||
return x_4;
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_Parser_setExpected___elambda__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_5;
|
||||
x_5 = l_Lean_Parser_setExpectedFn___rarg(x_1, x_2, x_3, x_4);
|
||||
return x_5;
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_Parser_setExpected___elambda__1(uint8_t x_1, lean_object* x_2) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_3;
|
||||
x_3 = lean_alloc_closure((void*)(l_Lean_Parser_setExpected___elambda__1___rarg), 4, 0);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_Parser_setExpected(uint8_t x_1, lean_object* x_2, lean_object* x_3) {
|
||||
_start:
|
||||
{
|
||||
uint8_t x_4;
|
||||
x_4 = !lean_is_exclusive(x_3);
|
||||
if (x_4 == 0)
|
||||
{
|
||||
lean_object* x_5; lean_object* x_6;
|
||||
x_5 = lean_ctor_get(x_3, 1);
|
||||
x_6 = lean_alloc_closure((void*)(l_Lean_Parser_setExpected___elambda__1___rarg), 4, 1);
|
||||
lean_closure_set(x_6, 0, x_5);
|
||||
lean_ctor_set(x_3, 1, x_6);
|
||||
return x_3;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10;
|
||||
x_7 = lean_ctor_get(x_3, 0);
|
||||
x_8 = lean_ctor_get(x_3, 1);
|
||||
lean_inc(x_8);
|
||||
lean_inc(x_7);
|
||||
lean_dec(x_3);
|
||||
x_9 = lean_alloc_closure((void*)(l_Lean_Parser_setExpected___elambda__1___rarg), 4, 1);
|
||||
lean_closure_set(x_9, 0, x_8);
|
||||
x_10 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_10, 0, x_7);
|
||||
lean_ctor_set(x_10, 1, x_9);
|
||||
return x_10;
|
||||
}
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_Parser_setExpected___elambda__1___boxed(lean_object* x_1, lean_object* x_2) {
|
||||
_start:
|
||||
{
|
||||
uint8_t x_3; lean_object* x_4;
|
||||
x_3 = lean_unbox(x_1);
|
||||
lean_dec(x_1);
|
||||
x_4 = l_Lean_Parser_setExpected___elambda__1(x_3, x_2);
|
||||
lean_dec(x_2);
|
||||
return x_4;
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_Parser_setExpected___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
|
||||
_start:
|
||||
{
|
||||
uint8_t x_4; lean_object* x_5;
|
||||
x_4 = lean_unbox(x_1);
|
||||
lean_dec(x_1);
|
||||
x_5 = l_Lean_Parser_setExpected(x_4, x_2, x_3);
|
||||
lean_dec(x_2);
|
||||
return x_5;
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_Parser_pushNone___elambda__1___rarg(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
|
|
@ -26884,7 +27123,7 @@ return x_2;
|
|||
lean_object* l_Lean_Parser_mkAntiquot(uint8_t x_1, lean_object* x_2, lean_object* x_3, uint8_t x_4) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; uint8_t x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; 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; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28;
|
||||
lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; uint8_t x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; 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; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29;
|
||||
x_5 = l_Lean_Parser_mkAntiquot___closed__2;
|
||||
x_6 = lean_string_append(x_5, x_2);
|
||||
x_7 = l_Char_HasRepr___closed__1;
|
||||
|
|
@ -26908,136 +27147,139 @@ lean_closure_set(x_19, 0, x_8);
|
|||
x_20 = lean_alloc_closure((void*)(l_Lean_Parser_andthenFn___rarg), 5, 2);
|
||||
lean_closure_set(x_20, 0, x_19);
|
||||
lean_closure_set(x_20, 1, x_16);
|
||||
x_21 = l_Lean_Parser_dollarSymbol(x_1);
|
||||
x_22 = l___private_Init_Lean_Parser_Parser_14__antiquotExpr(x_1);
|
||||
x_23 = lean_ctor_get(x_22, 0);
|
||||
lean_inc(x_23);
|
||||
x_24 = lean_ctor_get(x_22, 1);
|
||||
lean_inc(x_24);
|
||||
lean_dec(x_22);
|
||||
x_25 = lean_ctor_get(x_21, 0);
|
||||
x_21 = lean_box(0);
|
||||
x_22 = l_Lean_Parser_dollarSymbol(x_1);
|
||||
lean_inc(x_22);
|
||||
x_23 = l_Lean_Parser_setExpected(x_1, x_21, x_22);
|
||||
x_24 = l___private_Init_Lean_Parser_Parser_14__antiquotExpr(x_1);
|
||||
x_25 = lean_ctor_get(x_24, 0);
|
||||
lean_inc(x_25);
|
||||
lean_dec(x_21);
|
||||
x_26 = lean_box(x_1);
|
||||
x_27 = lean_alloc_closure((void*)(l_Lean_Parser_dollarSymbol___elambda__1___boxed), 2, 1);
|
||||
lean_closure_set(x_27, 0, x_26);
|
||||
x_26 = lean_ctor_get(x_24, 1);
|
||||
lean_inc(x_26);
|
||||
lean_dec(x_24);
|
||||
x_27 = lean_ctor_get(x_22, 0);
|
||||
lean_inc(x_27);
|
||||
lean_dec(x_22);
|
||||
x_28 = lean_ctor_get(x_23, 1);
|
||||
lean_inc(x_28);
|
||||
lean_dec(x_23);
|
||||
if (lean_obj_tag(x_3) == 0)
|
||||
{
|
||||
lean_object* x_76;
|
||||
x_76 = lean_box(0);
|
||||
x_28 = x_76;
|
||||
goto block_75;
|
||||
lean_object* x_77;
|
||||
x_77 = lean_box(0);
|
||||
x_29 = x_77;
|
||||
goto block_76;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_77;
|
||||
x_77 = lean_ctor_get(x_3, 0);
|
||||
lean_inc(x_77);
|
||||
lean_object* x_78;
|
||||
x_78 = lean_ctor_get(x_3, 0);
|
||||
lean_inc(x_78);
|
||||
lean_dec(x_3);
|
||||
x_28 = x_77;
|
||||
goto block_75;
|
||||
x_29 = x_78;
|
||||
goto block_76;
|
||||
}
|
||||
block_75:
|
||||
block_76:
|
||||
{
|
||||
lean_object* x_29; lean_object* x_30;
|
||||
x_29 = l_Lean_Parser_mkAntiquot___closed__1;
|
||||
x_30 = l_Lean_Name_append___main(x_28, x_29);
|
||||
lean_dec(x_28);
|
||||
lean_object* x_30; lean_object* x_31;
|
||||
x_30 = l_Lean_Parser_mkAntiquot___closed__1;
|
||||
x_31 = l_Lean_Name_append___main(x_29, x_30);
|
||||
lean_dec(x_29);
|
||||
if (x_4 == 0)
|
||||
{
|
||||
lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36; lean_object* x_37; lean_object* x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43; lean_object* x_44; lean_object* x_45;
|
||||
x_31 = l_Lean_Parser_mkAntiquot___closed__13;
|
||||
x_32 = l_Lean_Parser_andthenInfo(x_18, x_31);
|
||||
x_33 = l_Lean_Parser_mkAntiquot___closed__14;
|
||||
x_34 = lean_alloc_closure((void*)(l_Lean_Parser_andthenFn___rarg), 5, 2);
|
||||
lean_closure_set(x_34, 0, x_20);
|
||||
lean_closure_set(x_34, 1, x_33);
|
||||
x_35 = l_Lean_Parser_andthenInfo(x_23, x_32);
|
||||
x_36 = lean_alloc_closure((void*)(l_Lean_Parser_andthenFn___rarg), 5, 2);
|
||||
lean_closure_set(x_36, 0, x_24);
|
||||
lean_closure_set(x_36, 1, x_34);
|
||||
x_37 = l_Lean_Parser_andthenInfo(x_17, x_35);
|
||||
x_38 = l_Lean_Parser_mkAntiquot___closed__16;
|
||||
x_39 = lean_alloc_closure((void*)(l_Lean_Parser_andthenFn___rarg), 5, 2);
|
||||
lean_closure_set(x_39, 0, x_38);
|
||||
lean_closure_set(x_39, 1, x_36);
|
||||
x_40 = l_Lean_Parser_andthenInfo(x_25, x_37);
|
||||
x_41 = lean_alloc_closure((void*)(l_Lean_Parser_andthenFn___rarg), 5, 2);
|
||||
lean_closure_set(x_41, 0, x_27);
|
||||
lean_closure_set(x_41, 1, x_39);
|
||||
x_42 = lean_alloc_closure((void*)(l_Lean_Parser_tryFn___rarg), 4, 1);
|
||||
lean_closure_set(x_42, 0, x_41);
|
||||
lean_inc(x_30);
|
||||
x_43 = l_Lean_Parser_nodeInfo(x_30, x_40);
|
||||
x_44 = lean_alloc_closure((void*)(l_Lean_Parser_mkAntiquot___elambda__1___rarg), 5, 2);
|
||||
lean_closure_set(x_44, 0, x_30);
|
||||
lean_closure_set(x_44, 1, x_42);
|
||||
x_45 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_45, 0, x_43);
|
||||
lean_ctor_set(x_45, 1, x_44);
|
||||
return x_45;
|
||||
lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36; lean_object* x_37; lean_object* x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43; lean_object* x_44; lean_object* x_45; lean_object* x_46;
|
||||
x_32 = l_Lean_Parser_mkAntiquot___closed__13;
|
||||
x_33 = l_Lean_Parser_andthenInfo(x_18, x_32);
|
||||
x_34 = l_Lean_Parser_mkAntiquot___closed__14;
|
||||
x_35 = lean_alloc_closure((void*)(l_Lean_Parser_andthenFn___rarg), 5, 2);
|
||||
lean_closure_set(x_35, 0, x_20);
|
||||
lean_closure_set(x_35, 1, x_34);
|
||||
x_36 = l_Lean_Parser_andthenInfo(x_25, x_33);
|
||||
x_37 = lean_alloc_closure((void*)(l_Lean_Parser_andthenFn___rarg), 5, 2);
|
||||
lean_closure_set(x_37, 0, x_26);
|
||||
lean_closure_set(x_37, 1, x_35);
|
||||
x_38 = l_Lean_Parser_andthenInfo(x_17, x_36);
|
||||
x_39 = l_Lean_Parser_mkAntiquot___closed__16;
|
||||
x_40 = lean_alloc_closure((void*)(l_Lean_Parser_andthenFn___rarg), 5, 2);
|
||||
lean_closure_set(x_40, 0, x_39);
|
||||
lean_closure_set(x_40, 1, x_37);
|
||||
x_41 = l_Lean_Parser_andthenInfo(x_27, x_38);
|
||||
x_42 = lean_alloc_closure((void*)(l_Lean_Parser_andthenFn___rarg), 5, 2);
|
||||
lean_closure_set(x_42, 0, x_28);
|
||||
lean_closure_set(x_42, 1, x_40);
|
||||
x_43 = lean_alloc_closure((void*)(l_Lean_Parser_tryFn___rarg), 4, 1);
|
||||
lean_closure_set(x_43, 0, x_42);
|
||||
lean_inc(x_31);
|
||||
x_44 = l_Lean_Parser_nodeInfo(x_31, x_41);
|
||||
x_45 = lean_alloc_closure((void*)(l_Lean_Parser_mkAntiquot___elambda__1___rarg), 5, 2);
|
||||
lean_closure_set(x_45, 0, x_31);
|
||||
lean_closure_set(x_45, 1, x_43);
|
||||
x_46 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_46, 0, x_44);
|
||||
lean_ctor_set(x_46, 1, x_45);
|
||||
return x_46;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_46; lean_object* x_47; lean_object* x_48; lean_object* x_49; lean_object* x_50; lean_object* x_51; lean_object* x_52; lean_object* x_53; lean_object* x_54; lean_object* x_55; lean_object* x_56; lean_object* x_57; lean_object* x_58; lean_object* x_59; lean_object* x_60; lean_object* x_61; lean_object* x_62; lean_object* x_63; lean_object* x_64; lean_object* x_65; lean_object* x_66; lean_object* x_67; lean_object* x_68; lean_object* x_69; lean_object* x_70; lean_object* x_71; lean_object* x_72; lean_object* x_73; lean_object* x_74;
|
||||
x_46 = l___private_Init_Lean_Parser_Parser_11__noImmediateColon(x_1);
|
||||
x_47 = l_Lean_Parser_pushNone(x_1);
|
||||
x_48 = lean_ctor_get(x_47, 0);
|
||||
lean_inc(x_48);
|
||||
lean_dec(x_47);
|
||||
lean_inc(x_48);
|
||||
x_49 = l_Lean_Parser_andthenInfo(x_48, x_48);
|
||||
x_50 = lean_box(x_1);
|
||||
x_51 = lean_alloc_closure((void*)(l_Lean_Parser_pushNone___elambda__1___boxed), 3, 1);
|
||||
lean_closure_set(x_51, 0, x_50);
|
||||
lean_inc(x_51);
|
||||
x_52 = lean_alloc_closure((void*)(l_Lean_Parser_andthenFn___rarg), 5, 2);
|
||||
lean_object* x_47; lean_object* x_48; lean_object* x_49; lean_object* x_50; lean_object* x_51; lean_object* x_52; lean_object* x_53; lean_object* x_54; lean_object* x_55; lean_object* x_56; lean_object* x_57; lean_object* x_58; lean_object* x_59; lean_object* x_60; lean_object* x_61; lean_object* x_62; lean_object* x_63; lean_object* x_64; lean_object* x_65; lean_object* x_66; lean_object* x_67; lean_object* x_68; lean_object* x_69; lean_object* x_70; lean_object* x_71; lean_object* x_72; lean_object* x_73; lean_object* x_74; lean_object* x_75;
|
||||
x_47 = l___private_Init_Lean_Parser_Parser_11__noImmediateColon(x_1);
|
||||
x_48 = l_Lean_Parser_pushNone(x_1);
|
||||
x_49 = lean_ctor_get(x_48, 0);
|
||||
lean_inc(x_49);
|
||||
lean_dec(x_48);
|
||||
lean_inc(x_49);
|
||||
x_50 = l_Lean_Parser_andthenInfo(x_49, x_49);
|
||||
x_51 = lean_box(x_1);
|
||||
x_52 = lean_alloc_closure((void*)(l_Lean_Parser_pushNone___elambda__1___boxed), 3, 1);
|
||||
lean_closure_set(x_52, 0, x_51);
|
||||
lean_closure_set(x_52, 1, x_51);
|
||||
x_53 = lean_ctor_get(x_46, 0);
|
||||
lean_inc(x_53);
|
||||
lean_dec(x_46);
|
||||
x_54 = l_Lean_Parser_andthenInfo(x_53, x_49);
|
||||
x_55 = lean_box(x_1);
|
||||
x_56 = lean_alloc_closure((void*)(l___private_Init_Lean_Parser_Parser_11__noImmediateColon___elambda__1___boxed), 2, 1);
|
||||
lean_closure_set(x_56, 0, x_55);
|
||||
x_57 = lean_alloc_closure((void*)(l_Lean_Parser_andthenFn___rarg), 5, 2);
|
||||
lean_inc(x_52);
|
||||
x_53 = lean_alloc_closure((void*)(l_Lean_Parser_andthenFn___rarg), 5, 2);
|
||||
lean_closure_set(x_53, 0, x_52);
|
||||
lean_closure_set(x_53, 1, x_52);
|
||||
x_54 = lean_ctor_get(x_47, 0);
|
||||
lean_inc(x_54);
|
||||
lean_dec(x_47);
|
||||
x_55 = l_Lean_Parser_andthenInfo(x_54, x_50);
|
||||
x_56 = lean_box(x_1);
|
||||
x_57 = lean_alloc_closure((void*)(l___private_Init_Lean_Parser_Parser_11__noImmediateColon___elambda__1___boxed), 2, 1);
|
||||
lean_closure_set(x_57, 0, x_56);
|
||||
lean_closure_set(x_57, 1, x_52);
|
||||
x_58 = l_Lean_Parser_orelseInfo(x_18, x_54);
|
||||
x_59 = lean_alloc_closure((void*)(l_Lean_Parser_orelseFn___rarg), 5, 2);
|
||||
lean_closure_set(x_59, 0, x_20);
|
||||
lean_closure_set(x_59, 1, x_57);
|
||||
x_60 = l_Lean_Parser_mkAntiquot___closed__13;
|
||||
x_61 = l_Lean_Parser_andthenInfo(x_58, x_60);
|
||||
x_62 = l_Lean_Parser_mkAntiquot___closed__14;
|
||||
x_63 = lean_alloc_closure((void*)(l_Lean_Parser_andthenFn___rarg), 5, 2);
|
||||
lean_closure_set(x_63, 0, x_59);
|
||||
lean_closure_set(x_63, 1, x_62);
|
||||
x_64 = l_Lean_Parser_andthenInfo(x_23, x_61);
|
||||
x_65 = lean_alloc_closure((void*)(l_Lean_Parser_andthenFn___rarg), 5, 2);
|
||||
lean_closure_set(x_65, 0, x_24);
|
||||
lean_closure_set(x_65, 1, x_63);
|
||||
x_66 = l_Lean_Parser_andthenInfo(x_17, x_64);
|
||||
x_67 = l_Lean_Parser_mkAntiquot___closed__16;
|
||||
x_68 = lean_alloc_closure((void*)(l_Lean_Parser_andthenFn___rarg), 5, 2);
|
||||
lean_closure_set(x_68, 0, x_67);
|
||||
lean_closure_set(x_68, 1, x_65);
|
||||
x_69 = l_Lean_Parser_andthenInfo(x_25, x_66);
|
||||
x_70 = lean_alloc_closure((void*)(l_Lean_Parser_andthenFn___rarg), 5, 2);
|
||||
lean_closure_set(x_70, 0, x_27);
|
||||
lean_closure_set(x_70, 1, x_68);
|
||||
x_71 = lean_alloc_closure((void*)(l_Lean_Parser_tryFn___rarg), 4, 1);
|
||||
lean_closure_set(x_71, 0, x_70);
|
||||
lean_inc(x_30);
|
||||
x_72 = l_Lean_Parser_nodeInfo(x_30, x_69);
|
||||
x_73 = lean_alloc_closure((void*)(l_Lean_Parser_mkAntiquot___elambda__2___rarg), 5, 2);
|
||||
lean_closure_set(x_73, 0, x_30);
|
||||
lean_closure_set(x_73, 1, x_71);
|
||||
x_74 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_74, 0, x_72);
|
||||
lean_ctor_set(x_74, 1, x_73);
|
||||
return x_74;
|
||||
x_58 = lean_alloc_closure((void*)(l_Lean_Parser_andthenFn___rarg), 5, 2);
|
||||
lean_closure_set(x_58, 0, x_57);
|
||||
lean_closure_set(x_58, 1, x_53);
|
||||
x_59 = l_Lean_Parser_orelseInfo(x_18, x_55);
|
||||
x_60 = lean_alloc_closure((void*)(l_Lean_Parser_orelseFn___rarg), 5, 2);
|
||||
lean_closure_set(x_60, 0, x_20);
|
||||
lean_closure_set(x_60, 1, x_58);
|
||||
x_61 = l_Lean_Parser_mkAntiquot___closed__13;
|
||||
x_62 = l_Lean_Parser_andthenInfo(x_59, x_61);
|
||||
x_63 = l_Lean_Parser_mkAntiquot___closed__14;
|
||||
x_64 = lean_alloc_closure((void*)(l_Lean_Parser_andthenFn___rarg), 5, 2);
|
||||
lean_closure_set(x_64, 0, x_60);
|
||||
lean_closure_set(x_64, 1, x_63);
|
||||
x_65 = l_Lean_Parser_andthenInfo(x_25, x_62);
|
||||
x_66 = lean_alloc_closure((void*)(l_Lean_Parser_andthenFn___rarg), 5, 2);
|
||||
lean_closure_set(x_66, 0, x_26);
|
||||
lean_closure_set(x_66, 1, x_64);
|
||||
x_67 = l_Lean_Parser_andthenInfo(x_17, x_65);
|
||||
x_68 = l_Lean_Parser_mkAntiquot___closed__16;
|
||||
x_69 = lean_alloc_closure((void*)(l_Lean_Parser_andthenFn___rarg), 5, 2);
|
||||
lean_closure_set(x_69, 0, x_68);
|
||||
lean_closure_set(x_69, 1, x_66);
|
||||
x_70 = l_Lean_Parser_andthenInfo(x_27, x_67);
|
||||
x_71 = lean_alloc_closure((void*)(l_Lean_Parser_andthenFn___rarg), 5, 2);
|
||||
lean_closure_set(x_71, 0, x_28);
|
||||
lean_closure_set(x_71, 1, x_69);
|
||||
x_72 = lean_alloc_closure((void*)(l_Lean_Parser_tryFn___rarg), 4, 1);
|
||||
lean_closure_set(x_72, 0, x_71);
|
||||
lean_inc(x_31);
|
||||
x_73 = l_Lean_Parser_nodeInfo(x_31, x_70);
|
||||
x_74 = lean_alloc_closure((void*)(l_Lean_Parser_mkAntiquot___elambda__2___rarg), 5, 2);
|
||||
lean_closure_set(x_74, 0, x_31);
|
||||
lean_closure_set(x_74, 1, x_72);
|
||||
x_75 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_75, 0, x_73);
|
||||
lean_ctor_set(x_75, 1, x_74);
|
||||
return x_75;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -70,7 +70,6 @@ extern lean_object* l_Lean_Parser_regBuiltinCommandParserAttr___closed__4;
|
|||
lean_object* l_Lean_Parser_Syntax_paren___elambda__1___closed__5;
|
||||
lean_object* l_Lean_Parser_Command_quotedSymbolPrec___closed__5;
|
||||
lean_object* l_Lean_Parser_Command_macroHead;
|
||||
lean_object* l_Lean_Parser_Syntax_optional___closed__6;
|
||||
lean_object* l_Lean_Parser_Syntax_paren___closed__4;
|
||||
lean_object* l_Lean_Parser_Syntax_many1___elambda__1___closed__2;
|
||||
lean_object* l_Lean_Parser_Syntax_cat___closed__4;
|
||||
|
|
@ -86,7 +85,6 @@ lean_object* l_Lean_Parser_Command_macro__rules___elambda__1___closed__8;
|
|||
lean_object* l_Lean_Parser_Command_macroArgSimple___closed__5;
|
||||
lean_object* l_Lean_Parser_regBuiltinSyntaxParserAttr___closed__4;
|
||||
lean_object* l_Lean_Parser_Syntax_many___closed__1;
|
||||
lean_object* l_Lean_Parser_Syntax_optional___elambda__1___closed__7;
|
||||
lean_object* l_Lean_Parser_Syntax_many___closed__2;
|
||||
lean_object* l_Lean_Parser_Command_prefix___elambda__1___closed__6;
|
||||
lean_object* l_Lean_Parser_Syntax_many___elambda__1___closed__5;
|
||||
|
|
@ -123,6 +121,7 @@ extern lean_object* l_Lean_Parser_Level_num___elambda__1___closed__1;
|
|||
lean_object* l_Lean_Parser_Command_strLitPrec___elambda__1___closed__3;
|
||||
lean_object* l_Lean_Parser_Command_syntaxCat___elambda__1___closed__7;
|
||||
lean_object* l_Lean_Parser_Command_macroArgSimple___closed__1;
|
||||
lean_object* l_Lean_Parser_Syntax_try___closed__7;
|
||||
lean_object* l_Lean_Parser_precedenceLit___closed__2;
|
||||
lean_object* l_Lean_Parser_unquotedSymbolFn___rarg(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_Command_mixfix___elambda__1(lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -295,11 +294,11 @@ lean_object* l_Lean_Parser_Syntax_str___closed__1;
|
|||
lean_object* l_Lean_Parser_optionaInfo(lean_object*);
|
||||
lean_object* l_Lean_Parser_Command_syntaxCat___elambda__1(lean_object*, lean_object*, lean_object*);
|
||||
extern lean_object* l_Lean_Parser_Term_tacticStxQuot___closed__2;
|
||||
extern lean_object* l_Lean_Parser_Term_namedHole___elambda__1___closed__8;
|
||||
lean_object* l_Lean_Parser_Syntax_paren___closed__5;
|
||||
lean_object* l_Lean_Parser_Command_prefix___elambda__1___closed__3;
|
||||
lean_object* l_Lean_Parser_Syntax_optional___elambda__1___closed__1;
|
||||
lean_object* l_Lean_Parser_Syntax_paren___elambda__1___closed__4;
|
||||
lean_object* l_Lean_Parser_Syntax_optional___elambda__1___closed__8;
|
||||
lean_object* l_Lean_Parser_Command_reserve___elambda__1___closed__9;
|
||||
lean_object* l_Lean_Parser_precedence___elambda__1___closed__5;
|
||||
lean_object* l_Lean_Parser_Command_reserve___elambda__1___closed__4;
|
||||
|
|
@ -321,7 +320,6 @@ lean_object* l_Lean_Parser_Command_infixl___elambda__1___closed__6;
|
|||
lean_object* l_Lean_Parser_checkNoWsBeforeFn(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_Syntax_cat;
|
||||
extern lean_object* l_Lean_Parser_mkAntiquot___closed__10;
|
||||
lean_object* l_Lean_Parser_Syntax_optional___elambda__1___closed__4;
|
||||
lean_object* l_Lean_Parser_orelseInfo(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_Syntax_char___closed__4;
|
||||
lean_object* l_Lean_Parser_Command_syntax___elambda__1___closed__3;
|
||||
|
|
@ -366,6 +364,7 @@ lean_object* l_Lean_Parser_Syntax_char___elambda__1___closed__1;
|
|||
lean_object* l_Lean_Parser_Syntax_sepBy1___elambda__1___closed__8;
|
||||
extern lean_object* l_Lean_Parser_Term_typeAscription___elambda__1___closed__8;
|
||||
lean_object* l_Lean_Parser_Command_identPrec___elambda__1___closed__2;
|
||||
extern lean_object* l_Lean_Parser_Term_namedHole___elambda__1___closed__5;
|
||||
lean_object* l_Lean_Parser_Syntax_cat___elambda__1___closed__2;
|
||||
lean_object* l_Lean_Parser_Command_prefix___closed__2;
|
||||
lean_object* l_Lean_Parser_Syntax_num___elambda__1(lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -427,6 +426,7 @@ lean_object* l_Lean_Parser_Syntax_atom___closed__1;
|
|||
lean_object* l_Lean_Parser_Command_macroTailTactic___closed__4;
|
||||
lean_object* l_Lean_Parser_Syntax_sepBy___elambda__1___closed__4;
|
||||
lean_object* l_Lean_Parser_Command_mixfix___closed__2;
|
||||
extern lean_object* l_Lean_Parser_appPrec;
|
||||
lean_object* l_Lean_Parser_Command_syntaxCat___closed__6;
|
||||
lean_object* l_Lean_Parser_Command_infix___elambda__1___closed__6;
|
||||
lean_object* l_Lean_Parser_manyAux___main___at_Lean_Parser_Syntax_paren___elambda__1___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -544,7 +544,6 @@ extern lean_object* l_Lean_Level_LevelToFormat_Result_format___main___closed__3;
|
|||
lean_object* l_Lean_Parser_Syntax_orelse___closed__2;
|
||||
lean_object* l_Lean_Parser_Command_syntax___elambda__1___closed__4;
|
||||
lean_object* l_Lean_Parser_Syntax_char___closed__3;
|
||||
lean_object* l_Lean_Parser_Syntax_optional___elambda__1___closed__3;
|
||||
lean_object* l_Lean_Parser_Command_notation___elambda__1___closed__7;
|
||||
lean_object* l_String_trim(lean_object*);
|
||||
lean_object* l_Lean_Parser_Command_strLitPrec___elambda__1(lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -570,7 +569,6 @@ lean_object* l_Lean_Parser_Command_macro___closed__8;
|
|||
lean_object* l_Lean_Parser_Command_mixfixKind___closed__4;
|
||||
lean_object* l_Lean_Parser_Command_macroArgSimple___closed__2;
|
||||
lean_object* l_Lean_Parser_Command_reserve___closed__7;
|
||||
lean_object* l_Lean_Parser_Syntax_optional___elambda__1___closed__5;
|
||||
lean_object* l_Lean_Parser_Syntax_many;
|
||||
lean_object* l_Lean_Parser_Syntax_try___closed__1;
|
||||
lean_object* l_Lean_Parser_Command_identPrec___elambda__1___closed__3;
|
||||
|
|
@ -589,7 +587,6 @@ lean_object* l_Lean_Parser_Command_macro__rules;
|
|||
lean_object* l_Lean_Parser_Command_syntaxCat___elambda__1___closed__2;
|
||||
lean_object* l_Lean_Parser_Command_infix___elambda__1___closed__7;
|
||||
lean_object* l_Lean_Parser_Command_prefix___closed__3;
|
||||
lean_object* l_Lean_Parser_Syntax_optional___elambda__1___closed__6;
|
||||
lean_object* l_Lean_Parser_maxPrec___elambda__1___closed__5;
|
||||
lean_object* l_Lean_Parser_Syntax_try___closed__2;
|
||||
lean_object* l_Lean_Parser_Command_quotedSymbolPrec___elambda__1___closed__2;
|
||||
|
|
@ -3283,7 +3280,7 @@ if (lean_obj_tag(x_20) == 0)
|
|||
{
|
||||
lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26;
|
||||
x_21 = l_Lean_Parser_regBuiltinSyntaxParserAttr___closed__4;
|
||||
x_22 = lean_unsigned_to_nat(0u);
|
||||
x_22 = l_Lean_Parser_appPrec;
|
||||
x_23 = l_Lean_Parser_categoryParserFn(x_21, x_22, x_2, x_19);
|
||||
x_24 = l_Lean_Parser_Syntax_try___elambda__1___closed__2;
|
||||
x_25 = l_Lean_Parser_ParserState_mkNode(x_23, x_24, x_16);
|
||||
|
|
@ -3319,8 +3316,19 @@ return x_3;
|
|||
lean_object* _init_l_Lean_Parser_Syntax_try___closed__2() {
|
||||
_start:
|
||||
{
|
||||
uint8_t x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
|
||||
x_1 = 0;
|
||||
x_2 = l_Lean_Parser_regBuiltinSyntaxParserAttr___closed__4;
|
||||
x_3 = l_Lean_Parser_appPrec;
|
||||
x_4 = l_Lean_Parser_categoryParser(x_1, x_2, x_3);
|
||||
return x_4;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Parser_Syntax_try___closed__3() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
|
||||
x_1 = l_Lean_Parser_Syntax_paren___closed__1;
|
||||
x_1 = l_Lean_Parser_Syntax_try___closed__2;
|
||||
x_2 = lean_ctor_get(x_1, 0);
|
||||
lean_inc(x_2);
|
||||
x_3 = l_Lean_Parser_Syntax_try___closed__1;
|
||||
|
|
@ -3328,29 +3336,29 @@ x_4 = l_Lean_Parser_andthenInfo(x_3, x_2);
|
|||
return x_4;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Parser_Syntax_try___closed__3() {
|
||||
lean_object* _init_l_Lean_Parser_Syntax_try___closed__4() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = l_Lean_Parser_Syntax_try___elambda__1___closed__2;
|
||||
x_2 = l_Lean_Parser_Syntax_try___closed__2;
|
||||
x_2 = l_Lean_Parser_Syntax_try___closed__3;
|
||||
x_3 = l_Lean_Parser_nodeInfo(x_1, x_2);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Parser_Syntax_try___closed__4() {
|
||||
lean_object* _init_l_Lean_Parser_Syntax_try___closed__5() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
|
||||
x_1 = l_Lean_Parser_Syntax_try___elambda__1___closed__4;
|
||||
x_2 = lean_ctor_get(x_1, 0);
|
||||
lean_inc(x_2);
|
||||
x_3 = l_Lean_Parser_Syntax_try___closed__3;
|
||||
x_3 = l_Lean_Parser_Syntax_try___closed__4;
|
||||
x_4 = l_Lean_Parser_orelseInfo(x_2, x_3);
|
||||
return x_4;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Parser_Syntax_try___closed__5() {
|
||||
lean_object* _init_l_Lean_Parser_Syntax_try___closed__6() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
|
|
@ -3358,12 +3366,12 @@ x_1 = lean_alloc_closure((void*)(l_Lean_Parser_Syntax_try___elambda__1), 3, 0);
|
|||
return x_1;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Parser_Syntax_try___closed__6() {
|
||||
lean_object* _init_l_Lean_Parser_Syntax_try___closed__7() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = l_Lean_Parser_Syntax_try___closed__4;
|
||||
x_2 = l_Lean_Parser_Syntax_try___closed__5;
|
||||
x_1 = l_Lean_Parser_Syntax_try___closed__5;
|
||||
x_2 = l_Lean_Parser_Syntax_try___closed__6;
|
||||
x_3 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_3, 0, x_1);
|
||||
lean_ctor_set(x_3, 1, x_2);
|
||||
|
|
@ -3374,7 +3382,7 @@ lean_object* _init_l_Lean_Parser_Syntax_try() {
|
|||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
x_1 = l_Lean_Parser_Syntax_try___closed__6;
|
||||
x_1 = l_Lean_Parser_Syntax_try___closed__7;
|
||||
return x_1;
|
||||
}
|
||||
}
|
||||
|
|
@ -3529,7 +3537,7 @@ if (lean_obj_tag(x_20) == 0)
|
|||
{
|
||||
lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26;
|
||||
x_21 = l_Lean_Parser_regBuiltinSyntaxParserAttr___closed__4;
|
||||
x_22 = lean_unsigned_to_nat(0u);
|
||||
x_22 = l_Lean_Parser_appPrec;
|
||||
x_23 = l_Lean_Parser_categoryParserFn(x_21, x_22, x_2, x_19);
|
||||
x_24 = l_Lean_Parser_Syntax_lookahead___elambda__1___closed__2;
|
||||
x_25 = l_Lean_Parser_ParserState_mkNode(x_23, x_24, x_16);
|
||||
|
|
@ -3566,7 +3574,7 @@ lean_object* _init_l_Lean_Parser_Syntax_lookahead___closed__2() {
|
|||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
|
||||
x_1 = l_Lean_Parser_Syntax_paren___closed__1;
|
||||
x_1 = l_Lean_Parser_Syntax_try___closed__2;
|
||||
x_2 = lean_ctor_get(x_1, 0);
|
||||
lean_inc(x_2);
|
||||
x_3 = l_Lean_Parser_Syntax_lookahead___closed__1;
|
||||
|
|
@ -3636,252 +3644,6 @@ x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
|
|||
return x_6;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Parser_Syntax_optional___elambda__1___closed__1() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
x_1 = lean_mk_string("optional");
|
||||
return x_1;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Parser_Syntax_optional___elambda__1___closed__2() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = l_Lean_Parser_Syntax_paren___elambda__1___closed__2;
|
||||
x_2 = l_Lean_Parser_Syntax_optional___elambda__1___closed__1;
|
||||
x_3 = lean_name_mk_string(x_1, x_2);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Parser_Syntax_optional___elambda__1___closed__3() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2;
|
||||
x_1 = l_Lean_Parser_Syntax_optional___elambda__1___closed__2;
|
||||
x_2 = lean_alloc_ctor(1, 1, 0);
|
||||
lean_ctor_set(x_2, 0, x_1);
|
||||
return x_2;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Parser_Syntax_optional___elambda__1___closed__4() {
|
||||
_start:
|
||||
{
|
||||
uint8_t x_1; lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5;
|
||||
x_1 = 0;
|
||||
x_2 = l_Lean_Parser_Syntax_optional___elambda__1___closed__1;
|
||||
x_3 = l_Lean_Parser_Syntax_optional___elambda__1___closed__3;
|
||||
x_4 = 1;
|
||||
x_5 = l_Lean_Parser_mkAntiquot(x_1, x_2, x_3, x_4);
|
||||
return x_5;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Parser_Syntax_optional___elambda__1___closed__5() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
x_1 = lean_mk_string("optional ");
|
||||
return x_1;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Parser_Syntax_optional___elambda__1___closed__6() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2;
|
||||
x_1 = l_Lean_Parser_Syntax_optional___elambda__1___closed__5;
|
||||
x_2 = l_String_trim(x_1);
|
||||
return x_2;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Parser_Syntax_optional___elambda__1___closed__7() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = l_Char_HasRepr___closed__1;
|
||||
x_2 = l_Lean_Parser_Syntax_optional___elambda__1___closed__6;
|
||||
x_3 = lean_string_append(x_1, x_2);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Parser_Syntax_optional___elambda__1___closed__8() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = l_Lean_Parser_Syntax_optional___elambda__1___closed__7;
|
||||
x_2 = l_Char_HasRepr___closed__1;
|
||||
x_3 = lean_string_append(x_1, x_2);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_Parser_Syntax_optional___elambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10;
|
||||
x_4 = l_Lean_Parser_Syntax_optional___elambda__1___closed__4;
|
||||
x_5 = lean_ctor_get(x_4, 1);
|
||||
lean_inc(x_5);
|
||||
x_6 = lean_ctor_get(x_3, 0);
|
||||
lean_inc(x_6);
|
||||
x_7 = lean_array_get_size(x_6);
|
||||
lean_dec(x_6);
|
||||
x_8 = lean_ctor_get(x_3, 1);
|
||||
lean_inc(x_8);
|
||||
lean_inc(x_2);
|
||||
x_9 = lean_apply_3(x_5, x_1, x_2, x_3);
|
||||
x_10 = lean_ctor_get(x_9, 3);
|
||||
lean_inc(x_10);
|
||||
if (lean_obj_tag(x_10) == 0)
|
||||
{
|
||||
lean_dec(x_8);
|
||||
lean_dec(x_7);
|
||||
lean_dec(x_2);
|
||||
return x_9;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_11; lean_object* x_12; uint8_t x_13;
|
||||
x_11 = lean_ctor_get(x_10, 0);
|
||||
lean_inc(x_11);
|
||||
lean_dec(x_10);
|
||||
x_12 = lean_ctor_get(x_9, 1);
|
||||
lean_inc(x_12);
|
||||
x_13 = lean_nat_dec_eq(x_12, x_8);
|
||||
lean_dec(x_12);
|
||||
if (x_13 == 0)
|
||||
{
|
||||
lean_dec(x_11);
|
||||
lean_dec(x_8);
|
||||
lean_dec(x_7);
|
||||
lean_dec(x_2);
|
||||
return x_9;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20;
|
||||
lean_inc(x_8);
|
||||
x_14 = l_Lean_Parser_ParserState_restore(x_9, x_7, x_8);
|
||||
lean_dec(x_7);
|
||||
x_15 = lean_ctor_get(x_14, 0);
|
||||
lean_inc(x_15);
|
||||
x_16 = lean_array_get_size(x_15);
|
||||
lean_dec(x_15);
|
||||
x_17 = l_Lean_Parser_Syntax_optional___elambda__1___closed__6;
|
||||
x_18 = l_Lean_Parser_Syntax_optional___elambda__1___closed__8;
|
||||
lean_inc(x_2);
|
||||
x_19 = l_Lean_Parser_nonReservedSymbolFnAux(x_17, x_18, x_2, x_14);
|
||||
x_20 = lean_ctor_get(x_19, 3);
|
||||
lean_inc(x_20);
|
||||
if (lean_obj_tag(x_20) == 0)
|
||||
{
|
||||
lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26;
|
||||
x_21 = l_Lean_Parser_regBuiltinSyntaxParserAttr___closed__4;
|
||||
x_22 = lean_unsigned_to_nat(0u);
|
||||
x_23 = l_Lean_Parser_categoryParserFn(x_21, x_22, x_2, x_19);
|
||||
x_24 = l_Lean_Parser_Syntax_optional___elambda__1___closed__2;
|
||||
x_25 = l_Lean_Parser_ParserState_mkNode(x_23, x_24, x_16);
|
||||
x_26 = l_Lean_Parser_mergeOrElseErrors(x_25, x_11, x_8);
|
||||
lean_dec(x_8);
|
||||
return x_26;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_27; lean_object* x_28; lean_object* x_29;
|
||||
lean_dec(x_20);
|
||||
lean_dec(x_2);
|
||||
x_27 = l_Lean_Parser_Syntax_optional___elambda__1___closed__2;
|
||||
x_28 = l_Lean_Parser_ParserState_mkNode(x_19, x_27, x_16);
|
||||
x_29 = l_Lean_Parser_mergeOrElseErrors(x_28, x_11, x_8);
|
||||
lean_dec(x_8);
|
||||
return x_29;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Parser_Syntax_optional___closed__1() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; uint8_t x_2; lean_object* x_3;
|
||||
x_1 = l_Lean_Parser_Syntax_optional___elambda__1___closed__6;
|
||||
x_2 = 0;
|
||||
x_3 = l_Lean_Parser_nonReservedSymbolInfo(x_1, x_2);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Parser_Syntax_optional___closed__2() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
|
||||
x_1 = l_Lean_Parser_Syntax_paren___closed__1;
|
||||
x_2 = lean_ctor_get(x_1, 0);
|
||||
lean_inc(x_2);
|
||||
x_3 = l_Lean_Parser_Syntax_optional___closed__1;
|
||||
x_4 = l_Lean_Parser_andthenInfo(x_3, x_2);
|
||||
return x_4;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Parser_Syntax_optional___closed__3() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = l_Lean_Parser_Syntax_optional___elambda__1___closed__2;
|
||||
x_2 = l_Lean_Parser_Syntax_optional___closed__2;
|
||||
x_3 = l_Lean_Parser_nodeInfo(x_1, x_2);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Parser_Syntax_optional___closed__4() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
|
||||
x_1 = l_Lean_Parser_Syntax_optional___elambda__1___closed__4;
|
||||
x_2 = lean_ctor_get(x_1, 0);
|
||||
lean_inc(x_2);
|
||||
x_3 = l_Lean_Parser_Syntax_optional___closed__3;
|
||||
x_4 = l_Lean_Parser_orelseInfo(x_2, x_3);
|
||||
return x_4;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Parser_Syntax_optional___closed__5() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
x_1 = lean_alloc_closure((void*)(l_Lean_Parser_Syntax_optional___elambda__1), 3, 0);
|
||||
return x_1;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Parser_Syntax_optional___closed__6() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = l_Lean_Parser_Syntax_optional___closed__4;
|
||||
x_2 = l_Lean_Parser_Syntax_optional___closed__5;
|
||||
x_3 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_3, 0, x_1);
|
||||
lean_ctor_set(x_3, 1, x_2);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Parser_Syntax_optional() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
x_1 = l_Lean_Parser_Syntax_optional___closed__6;
|
||||
return x_1;
|
||||
}
|
||||
}
|
||||
lean_object* l___regBuiltinParser_Lean_Parser_Syntax_optional(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
uint8_t x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
|
||||
x_2 = 0;
|
||||
x_3 = l_Lean_Parser_regBuiltinSyntaxParserAttr___closed__4;
|
||||
x_4 = l_Lean_Parser_Syntax_optional___elambda__1___closed__2;
|
||||
x_5 = l_Lean_Parser_Syntax_optional;
|
||||
x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
|
||||
return x_6;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Parser_Syntax_sepBy___elambda__1___closed__1() {
|
||||
_start:
|
||||
{
|
||||
|
|
@ -4021,7 +3783,7 @@ if (lean_obj_tag(x_20) == 0)
|
|||
{
|
||||
lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24;
|
||||
x_21 = l_Lean_Parser_regBuiltinSyntaxParserAttr___closed__4;
|
||||
x_22 = lean_unsigned_to_nat(0u);
|
||||
x_22 = l_Lean_Parser_appPrec;
|
||||
lean_inc(x_2);
|
||||
x_23 = l_Lean_Parser_categoryParserFn(x_21, x_22, x_2, x_19);
|
||||
x_24 = lean_ctor_get(x_23, 3);
|
||||
|
|
@ -4077,7 +3839,7 @@ lean_object* _init_l_Lean_Parser_Syntax_sepBy___closed__2() {
|
|||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = l_Lean_Parser_Syntax_paren___closed__1;
|
||||
x_1 = l_Lean_Parser_Syntax_try___closed__2;
|
||||
x_2 = lean_ctor_get(x_1, 0);
|
||||
lean_inc(x_2);
|
||||
lean_inc(x_2);
|
||||
|
|
@ -4296,7 +4058,7 @@ if (lean_obj_tag(x_20) == 0)
|
|||
{
|
||||
lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24;
|
||||
x_21 = l_Lean_Parser_regBuiltinSyntaxParserAttr___closed__4;
|
||||
x_22 = lean_unsigned_to_nat(0u);
|
||||
x_22 = l_Lean_Parser_appPrec;
|
||||
lean_inc(x_2);
|
||||
x_23 = l_Lean_Parser_categoryParserFn(x_21, x_22, x_2, x_19);
|
||||
x_24 = lean_ctor_get(x_23, 3);
|
||||
|
|
@ -4420,6 +4182,183 @@ x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
|
|||
return x_6;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Parser_Syntax_optional___elambda__1___closed__1() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
x_1 = lean_mk_string("optional");
|
||||
return x_1;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Parser_Syntax_optional___elambda__1___closed__2() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = l_Lean_Parser_Syntax_paren___elambda__1___closed__2;
|
||||
x_2 = l_Lean_Parser_Syntax_optional___elambda__1___closed__1;
|
||||
x_3 = lean_name_mk_string(x_1, x_2);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_Parser_Syntax_optional___elambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7;
|
||||
x_4 = lean_ctor_get(x_3, 0);
|
||||
lean_inc(x_4);
|
||||
x_5 = lean_array_get_size(x_4);
|
||||
lean_dec(x_4);
|
||||
lean_inc(x_3);
|
||||
x_6 = l_Lean_Parser_ParserState_pushSyntax(x_3, x_1);
|
||||
x_7 = lean_ctor_get(x_3, 3);
|
||||
lean_inc(x_7);
|
||||
if (lean_obj_tag(x_7) == 0)
|
||||
{
|
||||
lean_object* x_8; lean_object* x_9; lean_object* x_10;
|
||||
x_8 = lean_ctor_get(x_3, 1);
|
||||
lean_inc(x_8);
|
||||
lean_dec(x_3);
|
||||
x_9 = l_Lean_Parser_tokenFn(x_2, x_6);
|
||||
x_10 = lean_ctor_get(x_9, 3);
|
||||
lean_inc(x_10);
|
||||
if (lean_obj_tag(x_10) == 0)
|
||||
{
|
||||
lean_object* x_11; lean_object* x_12;
|
||||
x_11 = lean_ctor_get(x_9, 0);
|
||||
lean_inc(x_11);
|
||||
x_12 = l_Array_back___at___private_Init_Lean_Parser_Parser_6__nameLitAux___spec__1(x_11);
|
||||
lean_dec(x_11);
|
||||
if (lean_obj_tag(x_12) == 2)
|
||||
{
|
||||
lean_object* x_13; lean_object* x_14; uint8_t x_15;
|
||||
x_13 = lean_ctor_get(x_12, 1);
|
||||
lean_inc(x_13);
|
||||
lean_dec(x_12);
|
||||
x_14 = l_Lean_Parser_Term_namedHole___elambda__1___closed__5;
|
||||
x_15 = lean_string_dec_eq(x_13, x_14);
|
||||
lean_dec(x_13);
|
||||
if (x_15 == 0)
|
||||
{
|
||||
lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19;
|
||||
x_16 = l_Lean_Parser_Term_namedHole___elambda__1___closed__8;
|
||||
x_17 = l_Lean_Parser_ParserState_mkErrorsAt(x_9, x_16, x_8);
|
||||
x_18 = l_Lean_Parser_Syntax_optional___elambda__1___closed__2;
|
||||
x_19 = l_Lean_Parser_ParserState_mkNode(x_17, x_18, x_5);
|
||||
return x_19;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_20; lean_object* x_21;
|
||||
lean_dec(x_8);
|
||||
x_20 = l_Lean_Parser_Syntax_optional___elambda__1___closed__2;
|
||||
x_21 = l_Lean_Parser_ParserState_mkNode(x_9, x_20, x_5);
|
||||
return x_21;
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25;
|
||||
lean_dec(x_12);
|
||||
x_22 = l_Lean_Parser_Term_namedHole___elambda__1___closed__8;
|
||||
x_23 = l_Lean_Parser_ParserState_mkErrorsAt(x_9, x_22, x_8);
|
||||
x_24 = l_Lean_Parser_Syntax_optional___elambda__1___closed__2;
|
||||
x_25 = l_Lean_Parser_ParserState_mkNode(x_23, x_24, x_5);
|
||||
return x_25;
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29;
|
||||
lean_dec(x_10);
|
||||
x_26 = l_Lean_Parser_Term_namedHole___elambda__1___closed__8;
|
||||
x_27 = l_Lean_Parser_ParserState_mkErrorsAt(x_9, x_26, x_8);
|
||||
x_28 = l_Lean_Parser_Syntax_optional___elambda__1___closed__2;
|
||||
x_29 = l_Lean_Parser_ParserState_mkNode(x_27, x_28, x_5);
|
||||
return x_29;
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_30; lean_object* x_31;
|
||||
lean_dec(x_7);
|
||||
lean_dec(x_3);
|
||||
lean_dec(x_2);
|
||||
x_30 = l_Lean_Parser_Syntax_optional___elambda__1___closed__2;
|
||||
x_31 = l_Lean_Parser_ParserState_mkNode(x_6, x_30, x_5);
|
||||
return x_31;
|
||||
}
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Parser_Syntax_optional___closed__1() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = lean_box(0);
|
||||
x_2 = l_Lean_Parser_Term_namedHole___elambda__1___closed__5;
|
||||
x_3 = l_Lean_Parser_symbolInfo(x_2, x_1);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Parser_Syntax_optional___closed__2() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = l_Lean_Parser_epsilonInfo;
|
||||
x_2 = l_Lean_Parser_Syntax_optional___closed__1;
|
||||
x_3 = l_Lean_Parser_andthenInfo(x_1, x_2);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Parser_Syntax_optional___closed__3() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = l_Lean_Parser_Syntax_optional___elambda__1___closed__2;
|
||||
x_2 = l_Lean_Parser_Syntax_optional___closed__2;
|
||||
x_3 = l_Lean_Parser_nodeInfo(x_1, x_2);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Parser_Syntax_optional___closed__4() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
x_1 = lean_alloc_closure((void*)(l_Lean_Parser_Syntax_optional___elambda__1), 3, 0);
|
||||
return x_1;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Parser_Syntax_optional___closed__5() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = l_Lean_Parser_Syntax_optional___closed__3;
|
||||
x_2 = l_Lean_Parser_Syntax_optional___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* _init_l_Lean_Parser_Syntax_optional() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
x_1 = l_Lean_Parser_Syntax_optional___closed__5;
|
||||
return x_1;
|
||||
}
|
||||
}
|
||||
lean_object* l___regBuiltinParser_Lean_Parser_Syntax_optional(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
uint8_t x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
|
||||
x_2 = 1;
|
||||
x_3 = l_Lean_Parser_regBuiltinSyntaxParserAttr___closed__4;
|
||||
x_4 = l_Lean_Parser_Syntax_optional___elambda__1___closed__2;
|
||||
x_5 = l_Lean_Parser_Syntax_optional;
|
||||
x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
|
||||
return x_6;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Parser_Syntax_many___elambda__1___closed__1() {
|
||||
_start:
|
||||
{
|
||||
|
|
@ -13482,6 +13421,8 @@ l_Lean_Parser_Syntax_try___closed__5 = _init_l_Lean_Parser_Syntax_try___closed__
|
|||
lean_mark_persistent(l_Lean_Parser_Syntax_try___closed__5);
|
||||
l_Lean_Parser_Syntax_try___closed__6 = _init_l_Lean_Parser_Syntax_try___closed__6();
|
||||
lean_mark_persistent(l_Lean_Parser_Syntax_try___closed__6);
|
||||
l_Lean_Parser_Syntax_try___closed__7 = _init_l_Lean_Parser_Syntax_try___closed__7();
|
||||
lean_mark_persistent(l_Lean_Parser_Syntax_try___closed__7);
|
||||
l_Lean_Parser_Syntax_try = _init_l_Lean_Parser_Syntax_try();
|
||||
lean_mark_persistent(l_Lean_Parser_Syntax_try);
|
||||
res = l___regBuiltinParser_Lean_Parser_Syntax_try(lean_io_mk_world());
|
||||
|
|
@ -13520,39 +13461,6 @@ lean_mark_persistent(l_Lean_Parser_Syntax_lookahead);
|
|||
res = l___regBuiltinParser_Lean_Parser_Syntax_lookahead(lean_io_mk_world());
|
||||
if (lean_io_result_is_error(res)) return res;
|
||||
lean_dec_ref(res);
|
||||
l_Lean_Parser_Syntax_optional___elambda__1___closed__1 = _init_l_Lean_Parser_Syntax_optional___elambda__1___closed__1();
|
||||
lean_mark_persistent(l_Lean_Parser_Syntax_optional___elambda__1___closed__1);
|
||||
l_Lean_Parser_Syntax_optional___elambda__1___closed__2 = _init_l_Lean_Parser_Syntax_optional___elambda__1___closed__2();
|
||||
lean_mark_persistent(l_Lean_Parser_Syntax_optional___elambda__1___closed__2);
|
||||
l_Lean_Parser_Syntax_optional___elambda__1___closed__3 = _init_l_Lean_Parser_Syntax_optional___elambda__1___closed__3();
|
||||
lean_mark_persistent(l_Lean_Parser_Syntax_optional___elambda__1___closed__3);
|
||||
l_Lean_Parser_Syntax_optional___elambda__1___closed__4 = _init_l_Lean_Parser_Syntax_optional___elambda__1___closed__4();
|
||||
lean_mark_persistent(l_Lean_Parser_Syntax_optional___elambda__1___closed__4);
|
||||
l_Lean_Parser_Syntax_optional___elambda__1___closed__5 = _init_l_Lean_Parser_Syntax_optional___elambda__1___closed__5();
|
||||
lean_mark_persistent(l_Lean_Parser_Syntax_optional___elambda__1___closed__5);
|
||||
l_Lean_Parser_Syntax_optional___elambda__1___closed__6 = _init_l_Lean_Parser_Syntax_optional___elambda__1___closed__6();
|
||||
lean_mark_persistent(l_Lean_Parser_Syntax_optional___elambda__1___closed__6);
|
||||
l_Lean_Parser_Syntax_optional___elambda__1___closed__7 = _init_l_Lean_Parser_Syntax_optional___elambda__1___closed__7();
|
||||
lean_mark_persistent(l_Lean_Parser_Syntax_optional___elambda__1___closed__7);
|
||||
l_Lean_Parser_Syntax_optional___elambda__1___closed__8 = _init_l_Lean_Parser_Syntax_optional___elambda__1___closed__8();
|
||||
lean_mark_persistent(l_Lean_Parser_Syntax_optional___elambda__1___closed__8);
|
||||
l_Lean_Parser_Syntax_optional___closed__1 = _init_l_Lean_Parser_Syntax_optional___closed__1();
|
||||
lean_mark_persistent(l_Lean_Parser_Syntax_optional___closed__1);
|
||||
l_Lean_Parser_Syntax_optional___closed__2 = _init_l_Lean_Parser_Syntax_optional___closed__2();
|
||||
lean_mark_persistent(l_Lean_Parser_Syntax_optional___closed__2);
|
||||
l_Lean_Parser_Syntax_optional___closed__3 = _init_l_Lean_Parser_Syntax_optional___closed__3();
|
||||
lean_mark_persistent(l_Lean_Parser_Syntax_optional___closed__3);
|
||||
l_Lean_Parser_Syntax_optional___closed__4 = _init_l_Lean_Parser_Syntax_optional___closed__4();
|
||||
lean_mark_persistent(l_Lean_Parser_Syntax_optional___closed__4);
|
||||
l_Lean_Parser_Syntax_optional___closed__5 = _init_l_Lean_Parser_Syntax_optional___closed__5();
|
||||
lean_mark_persistent(l_Lean_Parser_Syntax_optional___closed__5);
|
||||
l_Lean_Parser_Syntax_optional___closed__6 = _init_l_Lean_Parser_Syntax_optional___closed__6();
|
||||
lean_mark_persistent(l_Lean_Parser_Syntax_optional___closed__6);
|
||||
l_Lean_Parser_Syntax_optional = _init_l_Lean_Parser_Syntax_optional();
|
||||
lean_mark_persistent(l_Lean_Parser_Syntax_optional);
|
||||
res = l___regBuiltinParser_Lean_Parser_Syntax_optional(lean_io_mk_world());
|
||||
if (lean_io_result_is_error(res)) return res;
|
||||
lean_dec_ref(res);
|
||||
l_Lean_Parser_Syntax_sepBy___elambda__1___closed__1 = _init_l_Lean_Parser_Syntax_sepBy___elambda__1___closed__1();
|
||||
lean_mark_persistent(l_Lean_Parser_Syntax_sepBy___elambda__1___closed__1);
|
||||
l_Lean_Parser_Syntax_sepBy___elambda__1___closed__2 = _init_l_Lean_Parser_Syntax_sepBy___elambda__1___closed__2();
|
||||
|
|
@ -13621,6 +13529,25 @@ lean_mark_persistent(l_Lean_Parser_Syntax_sepBy1);
|
|||
res = l___regBuiltinParser_Lean_Parser_Syntax_sepBy1(lean_io_mk_world());
|
||||
if (lean_io_result_is_error(res)) return res;
|
||||
lean_dec_ref(res);
|
||||
l_Lean_Parser_Syntax_optional___elambda__1___closed__1 = _init_l_Lean_Parser_Syntax_optional___elambda__1___closed__1();
|
||||
lean_mark_persistent(l_Lean_Parser_Syntax_optional___elambda__1___closed__1);
|
||||
l_Lean_Parser_Syntax_optional___elambda__1___closed__2 = _init_l_Lean_Parser_Syntax_optional___elambda__1___closed__2();
|
||||
lean_mark_persistent(l_Lean_Parser_Syntax_optional___elambda__1___closed__2);
|
||||
l_Lean_Parser_Syntax_optional___closed__1 = _init_l_Lean_Parser_Syntax_optional___closed__1();
|
||||
lean_mark_persistent(l_Lean_Parser_Syntax_optional___closed__1);
|
||||
l_Lean_Parser_Syntax_optional___closed__2 = _init_l_Lean_Parser_Syntax_optional___closed__2();
|
||||
lean_mark_persistent(l_Lean_Parser_Syntax_optional___closed__2);
|
||||
l_Lean_Parser_Syntax_optional___closed__3 = _init_l_Lean_Parser_Syntax_optional___closed__3();
|
||||
lean_mark_persistent(l_Lean_Parser_Syntax_optional___closed__3);
|
||||
l_Lean_Parser_Syntax_optional___closed__4 = _init_l_Lean_Parser_Syntax_optional___closed__4();
|
||||
lean_mark_persistent(l_Lean_Parser_Syntax_optional___closed__4);
|
||||
l_Lean_Parser_Syntax_optional___closed__5 = _init_l_Lean_Parser_Syntax_optional___closed__5();
|
||||
lean_mark_persistent(l_Lean_Parser_Syntax_optional___closed__5);
|
||||
l_Lean_Parser_Syntax_optional = _init_l_Lean_Parser_Syntax_optional();
|
||||
lean_mark_persistent(l_Lean_Parser_Syntax_optional);
|
||||
res = l___regBuiltinParser_Lean_Parser_Syntax_optional(lean_io_mk_world());
|
||||
if (lean_io_result_is_error(res)) return res;
|
||||
lean_dec_ref(res);
|
||||
l_Lean_Parser_Syntax_many___elambda__1___closed__1 = _init_l_Lean_Parser_Syntax_many___elambda__1___closed__1();
|
||||
lean_mark_persistent(l_Lean_Parser_Syntax_many___elambda__1___closed__1);
|
||||
l_Lean_Parser_Syntax_many___elambda__1___closed__2 = _init_l_Lean_Parser_Syntax_many___elambda__1___closed__2();
|
||||
|
|
|
|||
|
|
@ -17,7 +17,9 @@ lean_object* l_panicWithPos___rarg(lean_object*, lean_object*, lean_object*, lea
|
|||
lean_object* l_dbgTrace___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_unreachable_x21___rarg(lean_object*);
|
||||
lean_object* l_dbgTraceIfShared___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_withPtrAddr(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_panic___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_withPtrEq___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___private_Init_Util_1__mkPanicMessage(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* lean_dbg_trace(lean_object*, lean_object*);
|
||||
lean_object* lean_string_append(lean_object*, lean_object*);
|
||||
|
|
@ -25,6 +27,8 @@ lean_object* l_unreachable_x21___rarg___closed__2;
|
|||
lean_object* l_panicWithPos___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* lean_dbg_sleep(uint32_t, lean_object*);
|
||||
lean_object* l_Nat_repr(lean_object*);
|
||||
lean_object* l_withPtrAddr___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_withPtrEq(lean_object*);
|
||||
lean_object* lean_dbg_trace_if_shared(lean_object*, lean_object*);
|
||||
lean_object* l_unreachable_x21(lean_object*);
|
||||
lean_object* l_unreachable_x21___rarg___closed__3;
|
||||
|
|
@ -34,6 +38,7 @@ lean_object* l___private_Init_Util_1__mkPanicMessage___closed__1;
|
|||
lean_object* lean_panic_fn(lean_object*, lean_object*);
|
||||
lean_object* l___private_Init_Util_1__mkPanicMessage___closed__2;
|
||||
lean_object* l_unreachable_x21___rarg___closed__1;
|
||||
lean_object* l_withPtrAddr___rarg(lean_object*, lean_object*);
|
||||
lean_object* l_unsafeCast(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___private_Init_Util_1__mkPanicMessage___closed__3;
|
||||
lean_object* l_dbgSleep___boxed(lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -208,6 +213,48 @@ x_2 = lean_alloc_closure((void*)(l_unreachable_x21___rarg), 1, 0);
|
|||
return x_2;
|
||||
}
|
||||
}
|
||||
lean_object* l_withPtrEq___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_5;
|
||||
x_5 = lean_apply_2(x_1, x_3, x_4);
|
||||
return x_5;
|
||||
}
|
||||
}
|
||||
lean_object* l_withPtrEq(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_2;
|
||||
x_2 = lean_alloc_closure((void*)(l_withPtrEq___rarg), 4, 0);
|
||||
return x_2;
|
||||
}
|
||||
}
|
||||
lean_object* l_withPtrAddr___rarg(lean_object* x_1, lean_object* x_2) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_3; lean_object* x_4;
|
||||
x_3 = lean_unsigned_to_nat(0u);
|
||||
x_4 = lean_apply_1(x_1, x_3);
|
||||
return x_4;
|
||||
}
|
||||
}
|
||||
lean_object* l_withPtrAddr(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_4;
|
||||
x_4 = lean_alloc_closure((void*)(l_withPtrAddr___rarg), 2, 0);
|
||||
return x_4;
|
||||
}
|
||||
}
|
||||
lean_object* l_withPtrAddr___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_4;
|
||||
x_4 = l_withPtrAddr(x_1, x_2, x_3);
|
||||
lean_dec(x_3);
|
||||
return x_4;
|
||||
}
|
||||
}
|
||||
lean_object* initialize_Init_Data_String_Basic(lean_object*);
|
||||
lean_object* initialize_Init_Data_ToString(lean_object*);
|
||||
static bool _G_initialized = false;
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue