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

chore: update stage0

Browse source
This commit is contained in:
Leonardo de Moura 2020-10-18 09:11:58 -07:00
parent 679187ae0a
commit 4c0785493f
22 changed files with 12922 additions and 12099 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
stage0/src/Lean/Meta/Basic.lean generated
View file

@ -62,6 +62,9 @@ structure ParamInfo :=
instance ParamInfo.inhabited : Inhabited ParamInfo := ⟨{}⟩
def ParamInfo.isExplicit (p : ParamInfo) : Bool :=
!p.implicit && p.instImplicit
structure FunInfo :=
(paramInfo : Array ParamInfo := #[])
(resultDeps : Array Nat := #[])

74
stage0/src/Lean/Meta/Offset.lean generated
View file

@ -1,3 +1,4 @@
#lang lean4
/-
Copyright (c) 2019 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
@ -6,43 +7,43 @@ Authors: Leonardo de Moura
import Lean.Data.LBool
import Lean.Meta.InferType
namespace Lean
namespace Meta
namespace Lean.Meta
partial def evalNat : Expr → Option Nat
| Expr.lit (Literal.natVal n) _ => pure n
| Expr.mdata _ e _ => evalNat e
| Expr.const `Nat.zero _ _ => pure 0
| e@(Expr.app _ a _) =>
let fn := e.getAppFn;
| e@(Expr.app _ a _) => do
let fn := e.getAppFn
match fn with
| Expr.const c _ _ =>
let nargs := e.getAppNumArgs;
if c == `Nat.succ && nargs == 1 then do
v ← evalNat a; pure $ v+1
else if c == `Nat.add && nargs == 2 then do
v₁ ← evalNat (e.getArg! 0);
v₂ ← evalNat (e.getArg! 1);
let nargs := e.getAppNumArgs
if c == `Nat.succ && nargs == 1 then
let v ← evalNat a
pure $ v+1
else if c == `Nat.add && nargs == 2 then
let v₁ ← evalNat (e.getArg! 0)
let v₂ ← evalNat (e.getArg! 1)
pure $ v₁ + v₂
else if c == `Nat.sub && nargs == 2 then do
v₁ ← evalNat (e.getArg! 0);
v₂ ← evalNat (e.getArg! 1);
else if c == `Nat.sub && nargs == 2 then
let v₁ ← evalNat (e.getArg! 0)
let v₂ ← evalNat (e.getArg! 1)
pure $ v₁ - v₂
else if c == `Nat.mul && nargs == 2 then do
v₁ ← evalNat (e.getArg! 0);
v₂ ← evalNat (e.getArg! 1);
else if c == `Nat.mul && nargs == 2 then
let v₁ ← evalNat (e.getArg! 0)
let v₂ ← evalNat (e.getArg! 1)
pure $ v₁ * v₂
else if c == `HasAdd.add && nargs == 4 then do
v₁ ← evalNat (e.getArg! 2);
v₂ ← evalNat (e.getArg! 3);
else if c == `HasAdd.add && nargs == 4 then
let v₁ ← evalNat (e.getArg! 2)
let v₂ ← evalNat (e.getArg! 3)
pure $ v₁ + v₂
else if c == `HasAdd.sub && nargs == 4 then do
v₁ ← evalNat (e.getArg! 2);
v₂ ← evalNat (e.getArg! 3);
else if c == `HasAdd.sub && nargs == 4 then
let v₁ ← evalNat (e.getArg! 2)
let v₂ ← evalNat (e.getArg! 3)
pure $ v₁ - v₂
else if c == `HasAdd.mul && nargs == 4 then do
v₁ ← evalNat (e.getArg! 2);
v₂ ← evalNat (e.getArg! 3);
else if c == `HasAdd.mul && nargs == 4 then
let v₁ ← evalNat (e.getArg! 2)
let v₂ ← evalNat (e.getArg! 3)
pure $ v₁ * v₂
else if c == `HasOfNat.ofNat && nargs == 3 then
evalNat (e.getArg! 2)
@ -54,20 +55,20 @@ partial def evalNat : Expr → Option Nat
/- Quick function for converting `e` into `s + k` s.t. `e` is definitionally equal to `Nat.add s k`. -/
private partial def getOffsetAux : Expr → Bool → Option (Expr × Nat)
| e@(Expr.app _ a _), top =>
let fn := e.getAppFn;
let fn := e.getAppFn
match fn with
| Expr.const c _ _ =>
let nargs := e.getAppNumArgs;
let nargs := e.getAppNumArgs
if c == `Nat.succ && nargs == 1 then do
(s, k) ← getOffsetAux a false;
let (s, k) ← getOffsetAux a false
pure (s, k+1)
else if c == `Nat.add && nargs == 2 then do
v ← evalNat (e.getArg! 1);
(s, k) ← getOffsetAux (e.getArg! 0) false;
let v ← evalNat (e.getArg! 1)
let (s, k) ← getOffsetAux (e.getArg! 0) false
pure (s, k+v)
else if c == `HasAdd.add && nargs == 4 then do
v ← evalNat (e.getArg! 3);
(s, k) ← getOffsetAux (e.getArg! 2) false;
let v ← evalNat (e.getArg! 3)
let (s, k) ← getOffsetAux (e.getArg! 2) false
pure (s, k+v)
else if top then none else pure (e, 0)
| _ => if top then none else pure (e, 0)
@ -78,10 +79,10 @@ getOffsetAux e true
private partial def isOffset : Expr → Option (Expr × Nat)
| e@(Expr.app _ a _) =>
let fn := e.getAppFn;
let fn := e.getAppFn
match fn with
| Expr.const c _ _ =>
let nargs := e.getAppNumArgs;
let nargs := e.getAppNumArgs
if (c == `Nat.succ && nargs == 1) || (c == `Nat.add && nargs == 2) || (c == `HasAdd.add && nargs == 4) then
getOffset e
else none
@ -99,7 +100,7 @@ else if isNatZero e then mkNatLit offset
else mkAppB (mkConst `Nat.add) e (mkNatLit offset)
def isDefEqOffset (s t : Expr) : DefEqM LBool :=
let isDefEq (s t) : DefEqM LBool := toLBoolM $ Meta.isExprDefEqAux s t;
let isDefEq (s t) : DefEqM LBool := toLBoolM $ Meta.isExprDefEqAux s t
match isOffset s with
| some (s, k₁) => match isOffset t with
| some (t, k₂) => -- s+k₁ =?= t+k₂
@ -119,5 +120,4 @@ match isOffset s with
| none => pure LBool.undef
| none => pure LBool.undef
end Meta
end Lean
end Lean.Meta

234
stage0/src/Lean/Meta/RecursorInfo.lean generated
View file

@ -1,3 +1,4 @@
#lang lean4
/-
Copyright (c) 2020 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
@ -7,8 +8,7 @@ import Lean.AuxRecursor
import Lean.Util.FindExpr
import Lean.Meta.ExprDefEq
namespace Lean
namespace Meta
namespace Lean.Meta
def casesOnSuffix := "casesOn"
def recOnSuffix := "recOn"
@ -54,8 +54,8 @@ else if info.firstIndexPos ≤ pos && pos ≤ info.majorPos then false
else true
def numMinors (info : RecursorInfo) : Nat :=
let r := info.numArgs;
let r := r - info.motivePos - 1;
let r := info.numArgs
let r := r - info.motivePos - 1
r - (info.majorPos + 1 - info.firstIndexPos)
instance : HasToString RecursorInfo :=
@ -80,14 +80,14 @@ instance : HasToString RecursorInfo :=
end RecursorInfo
private def mkRecursorInfoForKernelRec (declName : Name) (val : RecursorVal) : MetaM RecursorInfo := do
ival ← getConstInfoInduct val.getInduct;
let numLParams := ival.lparams.length;
let univLevelPos := (List.range numLParams).map RecursorUnivLevelPos.majorType;
let univLevelPos := if val.lparams.length == numLParams then univLevelPos else RecursorUnivLevelPos.motive :: univLevelPos;
let produceMotive := List.replicate val.nminors true;
let paramsPos := (List.range val.nparams).map some;
let indicesPos := (List.range val.nindices).map (fun pos => val.nparams + pos);
let numArgs := val.nindices + val.nparams + val.nminors + val.nmotives + 1;
let ival ← getConstInfoInduct val.getInduct
let numLParams := ival.lparams.length
let univLevelPos := (List.range numLParams).map RecursorUnivLevelPos.majorType
let univLevelPos := if val.lparams.length == numLParams then univLevelPos else RecursorUnivLevelPos.motive :: univLevelPos
let produceMotive := List.replicate val.nminors true
let paramsPos := (List.range val.nparams).map some
let indicesPos := (List.range val.nindices).map fun pos => val.nparams + pos
let numArgs := val.nindices + val.nparams + val.nminors + val.nmotives + 1
pure {
recursorName := declName,
typeName := val.getInduct,
@ -105,30 +105,29 @@ pure {
private def getMajorPosIfAuxRecursor? (declName : Name) (majorPos? : Option Nat) : MetaM (Option Nat) :=
if majorPos?.isSome then pure majorPos?
else do
env ← getEnv;
let env ← getEnv
if !isAuxRecursor env declName then pure none
else match declName with
| Name.str p s _ =>
if s != recOnSuffix && s != casesOnSuffix && s != brecOnSuffix then
pure none
else do
val ← getConstInfoRec (mkRecFor p);
let val ← getConstInfoRec (mkRecFor p)
pure $ some (val.nparams + val.nindices + (if s == casesOnSuffix then 1 else val.nmotives))
| _ => pure none
private def checkMotive (declName : Name) (motive : Expr) (motiveArgs : Array Expr) : MetaM Unit :=
unless (motive.isFVar && motiveArgs.all Expr.isFVar) $ throwError
("invalid user defined recursor '" ++ toString declName ++ "', result type must be of the form (C t), " ++
"where C is a bound variable, and t is a (possibly empty) sequence of bound variables")
private def checkMotive (declName : Name) (motive : Expr) (motiveArgs : Array Expr) : MetaM Unit := do
unless motive.isFVar && motiveArgs.all Expr.isFVar do
throwError! "invalid user defined recursor '{declName}', result type must be of the form (C t), where C is a bound variable, and t is a (possibly empty) sequence of bound variables"
/- Compute number of parameters for (user-defined) recursor.
We assume a parameter is anything that occurs before the motive -/
private partial def getNumParams (xs : Array Expr) (motive : Expr) : Nat → Nat
| i =>
if h : i < xs.size then
let x := xs.get ⟨i, h⟩;
let x := xs.get ⟨i, h⟩
if motive == x then i
else getNumParams (i+1)
else getNumParams xs motive (i+1)
else
i
@ -137,121 +136,107 @@ private def getMajorPosDepElim (declName : Name) (majorPos? : Option Nat) (xs :
match majorPos? with
| some majorPos =>
if h : majorPos < xs.size then
let major := xs.get ⟨majorPos, h⟩;
let depElim := motiveArgs.contains major;
let major := xs.get ⟨majorPos, h⟩
let depElim := motiveArgs.contains major
pure (major, majorPos, depElim)
else throwError
("invalid major premise position for user defined recursor, recursor has only " ++ toString xs.size ++ " arguments")
else throwError! "invalid major premise position for user defined recursor, recursor has only {xs.size} arguments"
| none => do
when motiveArgs.isEmpty $ throwError
("invalid user defined recursor, '" ++ toString declName ++ "' does not support dependent elimination, " ++
"and position of the major premise was not specified " ++
"(solution: set attribute '[recursor <pos>]', where <pos> is the position of the major premise)");
let major := motiveArgs.back;
if motiveArgs.isEmpty then
throwError! "invalid user defined recursor, '{declName}' does not support dependent elimination, and position of the major premise was not specified (solution: set attribute '[recursor <pos>]', where <pos> is the position of the major premise)"
let major := motiveArgs.back
match xs.getIdx? major with
| some majorPos => pure (major, majorPos, true)
| none => throwError ("ill-formed recursor '" ++ toString declName ++ "'")
| none => throwError! "ill-formed recursor '{declName}'"
private def getParamsPos (declName : Name) (xs : Array Expr) (numParams : Nat) (Iargs : Array Expr) : MetaM (List (Option Nat)) := do
paramsPos ← numParams.foldM
(fun i (paramsPos : Array (Option Nat)) => do
let x := xs.get! i;
j? ← Iargs.findIdxM? $ fun Iarg => isDefEq Iarg x;
match j? with
| some j => pure $ paramsPos.push (some j)
| none => do
localDecl ← getLocalDecl x.fvarId!;
if localDecl.binderInfo.isInstImplicit then
pure $ paramsPos.push none
else
throwError
("invalid user defined recursor '" ++ toString declName ++ "' , type of the major premise does not contain the recursor parameter"))
#[];
let paramsPos := #[]
for i in [:numParams] do
let x := xs[i]
match (← Iargs.findIdxM? fun Iarg => isDefEq Iarg x) with
| some j => paramsPos := paramsPos.push (some j)
| none => do
let localDecl ← getLocalDecl x.fvarId!
if localDecl.binderInfo.isInstImplicit then
paramsPos := paramsPos.push none
else
throwError!"invalid user defined recursor '{declName}', type of the major premise does not contain the recursor parameter"
pure paramsPos.toList
private def getIndicesPos (declName : Name) (xs : Array Expr) (majorPos numIndices : Nat) (Iargs : Array Expr) : MetaM (List Nat) := do
indicesPos ← numIndices.foldM
(fun i (indicesPos : Array Nat) => do
let i := majorPos - numIndices + i;
let x := xs.get! i;
-- trace! `Meta ("getIndicesPos " ++ toString i ++ ": " ++ x);
j? ← Iargs.findIdxM? $ fun Iarg => isDefEq Iarg x;
match j? with
| some j => pure $ indicesPos.push j
| none => throwError
("invalid user defined recursor '" ++ toString declName ++ "' , type of the major premise does not contain the recursor index"))
#[];
let indicesPos := #[]
for i in [:numIndices] do
let i := majorPos - numIndices + i
let x := xs[i]
match (← Iargs.findIdxM? fun Iarg => isDefEq Iarg x) with
| some j => indicesPos := indicesPos.push j
| none => throwError! "invalid user defined recursor '{declName}', type of the major premise does not contain the recursor index"
pure indicesPos.toList
private def getMotiveLevel (declName : Name) (motiveResultType : Expr) : MetaM Level :=
match motiveResultType with
| Expr.sort u@(Level.zero _) _ => pure u
| Expr.sort u@(Level.param _ _) _ => pure u
| _ => throwError
("invalid user defined recursor '" ++ toString declName ++ "' , motive result sort must be Prop or (Sort u) where u is a universe level parameter")
| _ =>
throwError! "invalid user defined recursor '{declName}', motive result sort must be Prop or (Sort u) where u is a universe level parameter"
private def getUnivLevelPos (declName : Name) (lparams : List Name) (motiveLvl : Level) (Ilevels : List Level) : MetaM (List RecursorUnivLevelPos) := do
let Ilevels := Ilevels.toArray;
univLevelPos ← lparams.foldlM
(fun (univLevelPos : Array RecursorUnivLevelPos) p =>
if motiveLvl == mkLevelParam p then
pure $ univLevelPos.push RecursorUnivLevelPos.motive
else
match Ilevels.findIdx? $ fun u => u == mkLevelParam p with
| some i => pure $ univLevelPos.push $ RecursorUnivLevelPos.majorType i
| none => throwError
("invalid user defined recursor '" ++ toString declName ++ "' , major premise type does not contain universe level parameter '" ++ toString p ++ "'"))
#[];
let Ilevels := Ilevels.toArray
let univLevelPos := #[]
for p in lparams do
if motiveLvl == mkLevelParam p then
univLevelPos := univLevelPos.push RecursorUnivLevelPos.motive
else
match Ilevels.findIdx? fun u => u == mkLevelParam p with
| some i => univLevelPos := univLevelPos.push (RecursorUnivLevelPos.majorType i)
| none =>
throwError! "invalid user defined recursor '{declName}', major premise type does not contain universe level parameter '{p}'"
pure univLevelPos.toList
private def getProduceMotiveAndRecursive (xs : Array Expr) (numParams numIndices majorPos : Nat) (motive : Expr) : MetaM (List Bool × Bool) := do
(produceMotive, rec) ← xs.size.foldM
(fun i (p : Array Bool × Bool) =>
if i < numParams + 1 then pure p -- skip parameters and motive
else if majorPos - numIndices ≤ i && i ≤ majorPos then pure p -- skip indices and major premise
else do -- process minor premise
let (produceMotive, rec) := p;
let x := xs.get! i;
xType ← inferType x;
forallTelescopeReducing xType $ fun minorArgs minorResultType => minorResultType.withApp $ fun res _ => do
-- trace! `Meta ("xType: " ++ xType ++ ", motive: " ++ motive ++ ", " ++ minorArgs ++ ", " ++ res);
let produceMotive := produceMotive.push (res == motive);
rec ← if rec then pure rec else minorArgs.anyM $ fun minorArg => do {
minorArgType ← inferType minorArg;
pure $ (minorArgType.find? $ fun e => e == motive).isSome
};
pure (produceMotive, rec))
(#[], false);
pure (produceMotive.toList, rec)
let produceMotive := #[]
let recursor := false
for i in [:xs.size] do
if i < numParams + 1 then
continue --skip parameters and motive
if majorPos - numIndices ≤ i && i ≤ majorPos then
continue -- skip indices and major premise
-- process minor premise
let x := xs[i]
let xType ← inferType x
(produceMotive, recursor) ← forallTelescopeReducing xType fun minorArgs minorResultType => minorResultType.withApp fun res _ => do
let produceMotive := produceMotive.push (res == motive)
let recursor ← if recursor then pure recursor else minorArgs.anyM fun minorArg => do
let minorArgType ← inferType minorArg
pure (minorArgType.find? fun e => e == motive).isSome
pure (produceMotive, recursor)
pure (produceMotive.toList, recursor)
private def checkMotiveResultType (declName : Name) (motiveArgs : Array Expr) (motiveResultType : Expr) (motiveTypeParams : Array Expr) : MetaM Unit :=
when (!motiveResultType.isSort || motiveArgs.size != motiveTypeParams.size) $ throwError
("invalid user defined recursor '" ++ toString declName ++ "', motive must have a type of the form "
++ "(C : Pi (i : B A), I A i -> Type), where A is (possibly empty) sequence of variables (aka parameters), "
++ "(i : B A) is a (possibly empty) telescope (aka indices), and I is a constant")
private def checkMotiveResultType (declName : Name) (motiveArgs : Array Expr) (motiveResultType : Expr) (motiveTypeParams : Array Expr) : MetaM Unit := do
if !motiveResultType.isSort || motiveArgs.size != motiveTypeParams.size then
throwError! "invalid user defined recursor '{declName}', motive must have a type of the form (C : Pi (i : B A), I A i -> Type), where A is (possibly empty) sequence of variables (aka parameters), (i : B A) is a (possibly empty) telescope (aka indices), and I is a constant"
private def mkRecursorInfoAux (cinfo : ConstantInfo) (majorPos? : Option Nat) : MetaM RecursorInfo := do
let declName := cinfo.name;
majorPos? ← getMajorPosIfAuxRecursor? declName majorPos?;
forallTelescopeReducing cinfo.type $ fun xs type => type.withApp $ fun motive motiveArgs => do
checkMotive declName motive motiveArgs;
let numParams := getNumParams xs motive 0;
(major, majorPos, depElim) ← getMajorPosDepElim declName majorPos? xs motive motiveArgs;
let numIndices := if depElim then motiveArgs.size - 1 else motiveArgs.size;
when (majorPos < numIndices) $ throwError
("invalid user defined recursor '" ++ toString declName ++ "', indices must occur before major premise");
majorType ← inferType major;
majorType.withApp $ fun I Iargs =>
let declName := cinfo.name
let majorPos? ← getMajorPosIfAuxRecursor? declName majorPos?
forallTelescopeReducing cinfo.type fun xs type => type.withApp fun motive motiveArgs => do
checkMotive declName motive motiveArgs
let numParams := getNumParams xs motive 0
let (major, majorPos, depElim) ← getMajorPosDepElim declName majorPos? xs motive motiveArgs
let numIndices := if depElim then motiveArgs.size - 1 else motiveArgs.size
if majorPos < numIndices then
throwError! "invalid user defined recursor '{declName}', indices must occur before major premise"
let majorType ← inferType major
majorType.withApp fun I Iargs =>
match I with
| Expr.const Iname Ilevels _ => do
paramsPos ← getParamsPos declName xs numParams Iargs;
indicesPos ← getIndicesPos declName xs majorPos numIndices Iargs;
motiveType ← inferType motive;
forallTelescopeReducing motiveType $ fun motiveTypeParams motiveResultType => do
checkMotiveResultType declName motiveArgs motiveResultType motiveTypeParams;
motiveLvl ← getMotiveLevel declName motiveResultType;
univLevelPos ← getUnivLevelPos declName cinfo.lparams motiveLvl Ilevels;
(produceMotive, recursive) ← getProduceMotiveAndRecursive xs numParams numIndices majorPos motive;
let paramsPos ← getParamsPos declName xs numParams Iargs
let indicesPos ← getIndicesPos declName xs majorPos numIndices Iargs
let motiveType ← inferType motive
forallTelescopeReducing motiveType fun motiveTypeParams motiveResultType => do
checkMotiveResultType declName motiveArgs motiveResultType motiveTypeParams
let motiveLvl ← getMotiveLevel declName motiveResultType
let univLevelPos ← getUnivLevelPos declName cinfo.lparams motiveLvl Ilevels
let (produceMotive, recursive) ← getProduceMotiveAndRecursive xs numParams numIndices majorPos motive
pure {
recursorName := declName,
typeName := Iname,
@ -264,15 +249,13 @@ forallTelescopeReducing cinfo.type $ fun xs type => type.withApp $ fun motive mo
indicesPos := indicesPos,
numArgs := xs.size
}
| _ => throwError
("invalid user defined recursor '" ++ toString declName
++ "', type of the major premise must be of the form (I ...), where I is a constant")
| _ => throwError! "invalid user defined recursor '{declName}', type of the major premise must be of the form (I ...), where I is a constant"
private def syntaxToMajorPos (stx : Syntax) : Except String Nat :=
match stx with
| Syntax.node _ args =>
if args.size == 0 then Except.error "unexpected kind of argument"
else match (args.get! 0).isNatLit? with
else match args[0].isNatLit? with
| some idx =>
if idx == 0 then Except.error "major premise position must be greater than 0"
else pure (idx - 1)
@ -280,30 +263,27 @@ match stx with
| _ => Except.error "unexpected kind of argument"
private def mkRecursorInfoCore (declName : Name) (majorPos? : Option Nat := none) : MetaM RecursorInfo := do
cinfo ← getConstInfo declName;
let cinfo ← getConstInfo declName
match cinfo with
| ConstantInfo.recInfo val => mkRecursorInfoForKernelRec declName val
| _ => mkRecursorInfoAux cinfo majorPos?
def mkRecursorAttr : IO (ParametricAttribute Nat) :=
registerParametricAttribute `recursor "user defined recursor, numerical parameter specifies position of the major premise"
(fun _ stx => ofExcept $ syntaxToMajorPos stx)
(fun declName majorPos => do
liftM $ (mkRecursorInfoCore declName (some majorPos)).run';
pure ())
@[init mkRecursorAttr] constant recursorAttribute : ParametricAttribute Nat := arbitrary _
initialize recursorAttribute : ParametricAttribute Nat ←
registerParametricAttribute `recursor "user defined recursor, numerical parameter specifies position of the major premise"
(fun _ stx => ofExcept $ syntaxToMajorPos stx)
(fun declName majorPos => do
(mkRecursorInfoCore declName (some majorPos)).run'
pure ())
def getMajorPos? (env : Environment) (declName : Name) : Option Nat :=
recursorAttribute.getParam env declName
def mkRecursorInfo (declName : Name) (majorPos? : Option Nat := none) : MetaM RecursorInfo := do
cinfo ← getConstInfo declName;
let cinfo ← getConstInfo declName
match cinfo with
| ConstantInfo.recInfo val => mkRecursorInfoForKernelRec declName val
| _ => match majorPos? with
| none => do env ← getEnv; mkRecursorInfoAux cinfo (getMajorPos? env declName)
| none => do mkRecursorInfoAux cinfo (getMajorPos? (← getEnv) declName)
| _ => mkRecursorInfoAux cinfo majorPos?
end Meta
end Lean
end Lean.Meta

60
stage0/src/Lean/Meta/Reduce.lean generated
View file

@ -1,3 +1,4 @@
#lang lean4
/-
Copyright (c) 2019 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
@ -6,38 +7,33 @@ Authors: Leonardo de Moura
import Lean.Meta.Basic
import Lean.Meta.FunInfo
namespace Lean
namespace Meta
namespace Lean.Meta
partial def reduceAux (explicitOnly : Bool) (skipTypes : Bool) (skipProofs : Bool) : Expr → MetaM Expr
| e => do
condM (pure skipTypes <&&> isType e) (pure e) $
condM (pure skipProofs <&&> isProof e) (pure e) $ do
e ← whnf e;
partial def reduce (e : Expr) (explicitOnly skipTypes skipProofs := true) : MetaM Expr :=
let rec visit (e : Expr) := do
if (← (pure skipTypes <&&> isType e)) then
pure e
else if (← (pure skipProofs <&&> isProof e)) then
pure e
else
let e ← whnf e
match e with
| Expr.app _ _ _ => do
let f := e.getAppFn;
let nargs := e.getAppNumArgs;
finfo ← getFunInfoNArgs f nargs;
let args := e.getAppArgs;
args ← args.size.foldM
(fun i (args : Array Expr) =>
if h : i < finfo.paramInfo.size then
let info := finfo.paramInfo.get ⟨i, h⟩;
if explicitOnly && (info.implicit || info.instImplicit) then
pure args
else
args.modifyM i reduceAux
else
args.modifyM i reduceAux)
args;
pure $ mkAppN f args
| Expr.lam _ _ _ _ => lambdaTelescope e $ fun xs b => do b ← reduceAux b; mkLambdaFVars xs b
| Expr.forallE _ _ _ _ => forallTelescope e $ fun xs b => do b ← reduceAux b; mkForallFVars xs b
| _ => pure e
| Expr.app .. =>
let f := e.getAppFn
let nargs := e.getAppNumArgs
let finfo ← getFunInfoNArgs f nargs
let args := e.getAppArgs
for i in [:args.size] do
if i < finfo.paramInfo.size then
let info := finfo.paramInfo[i]
if !explicitOnly || info.isExplicit then
args ← args.modifyM i visit
else
args ← args.modifyM i visit
pure (mkAppN f args)
| Expr.lam .. => lambdaTelescope e fun xs b => do mkLambdaFVars xs (← visit b)
| Expr.forallE .. => forallTelescope e fun xs b => do mkForallFVars xs (← visit b)
| _ => pure e
visit e
def reduce (e : Expr) (explicitOnly skipTypes skipProofs := true) : MetaM Expr :=
reduceAux explicitOnly skipTypes skipProofs e
end Meta
end Lean
end Lean.Meta

65
stage0/src/Lean/Meta/ReduceEval.lean generated
View file

@ -1,3 +1,4 @@
#lang lean4
/-
Copyright (c) 2020 Sebastian Ullrich. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
@ -8,8 +9,7 @@ Authors: Sebastian Ullrich
import Lean.Meta.Offset
namespace Lean
namespace Meta
namespace Lean.Meta
class HasReduceEval (α : Type) :=
(reduceEval : Expr → MetaM α)
@ -18,44 +18,45 @@ def reduceEval {α : Type} [HasReduceEval α] (e : Expr) : MetaM α :=
withAtLeastTransparency TransparencyMode.default $
HasReduceEval.reduceEval e
instance Nat.hasReduceEval : HasReduceEval Nat := ⟨fun e => do
e ← whnf e;
some n ← pure $ evalNat e
| throwError $ "reduceEval: failed to evaluate argument: " ++ toString e;
pure n⟩
private def throwFailedToEval {α} (e : Expr) : MetaM α :=
throwError! "reduceEval: failed to evaluate argument{indentExpr e}"
instance Option.hasReduceEval {α : Type} [HasReduceEval α] : HasReduceEval (Option α) := ⟨fun e => do
e ← whnf e;
Expr.const c _ _ ← pure e.getAppFn
| throwError $ "reduceEval: failed to evaluate argument: " ++ toString e;
let nargs := e.getAppNumArgs;
if c == `Option.none && nargs == 0 then pure none
else if c == `Option.some && nargs == 1 then some <$> reduceEval e.appArg!
else throwError $ "reduceEval: failed to evaluate argument: " ++ toString e⟩
instance : HasReduceEval Nat :=
⟨fun e => do
let e ← whnf e
let some n ← pure $ evalNat e | throwFailedToEval e
pure n⟩
instance String.hasReduceEval : HasReduceEval String := ⟨fun e => do
Expr.lit (Literal.strVal s) _ ← whnf e
| throwError $ "reduceEval: failed to evaluate argument: " ++ toString e;
pure s⟩
instance {α : Type} [HasReduceEval α] : HasReduceEval (Option α) :=
⟨fun e => do
let e ← whnf e
let Expr.const c .. ← pure e.getAppFn | throwFailedToEval e
let nargs := e.getAppNumArgs
if c == `Option.none && nargs == 0 then pure none
else if c == `Option.some && nargs == 1 then some <$> reduceEval e.appArg!
else throwFailedToEval e⟩
private partial def evalName : Expr → MetaM Name | e => do
e ← whnf e;
Expr.const c _ _ ← pure e.getAppFn
| throwError $ "reduceEval: failed to evaluate argument: " ++ toString e;
let nargs := e.getAppNumArgs;
instance : HasReduceEval String :=
⟨fun e => do
let Expr.lit (Literal.strVal s) _ ← whnf e | throwFailedToEval e
pure s⟩
private partial def evalName (e : Expr) : MetaM Name := do
let e ← whnf e
let Expr.const c _ _ ← pure e.getAppFn | throwFailedToEval e
let nargs := e.getAppNumArgs
if c == `Lean.Name.anonymous && nargs == 0 then pure Name.anonymous
else if c == `Lean.Name.str && nargs == 3 then do
n ← evalName $ e.getArg! 0;
s ← reduceEval $ e.getArg! 1;
let n ← evalName $ e.getArg! 0
let s ← reduceEval $ e.getArg! 1
pure $ mkNameStr n s
else if c == `Lean.Name.num && nargs == 3 then do
n ← evalName $ e.getArg! 0;
u ← reduceEval $ e.getArg! 1;
let n ← evalName $ e.getArg! 0
let u ← reduceEval $ e.getArg! 1
pure $ mkNameNum n u
else
throwError $ "reduceEval: failed to evaluate argument: " ++ toString e
throwFailedToEval e
instance Name.hasReduceEval : HasReduceEval Name := ⟨evalName⟩
instance : HasReduceEval Name := ⟨evalName⟩
end Meta
end Lean
end Lean.Meta

1
stage0/src/Lean/Meta/Tactic.lean generated
View file

@ -1,3 +1,4 @@
#lang lean4
/-
Copyright (c) 2019 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.

7
stage0/src/Lean/Meta/TransparencyMode.lean generated
View file

@ -1,10 +1,10 @@
#lang lean4
/-
Copyright (c) 2020 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
namespace Lean
namespace Meta
namespace Lean.Meta
inductive TransparencyMode
| all | default | reducible
@ -35,5 +35,4 @@ def lt : TransparencyMode → TransparencyMode → Bool
end TransparencyMode
end Meta
end Lean
end Lean.Meta

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

@ -257,6 +257,7 @@ lean_object* l_Lean_Delaborator_delabseqLeft(lean_object*, lean_object*, lean_ob
uint8_t l_Lean_getPPStructureProjections(lean_object*);
extern lean_object* l_Array_myMacro____x40_Init_Data_Array_Macros___hyg_301____closed__4;
lean_object* l_Lean_Delaborator_delabAndThen___closed__1;
extern lean_object* l_Lean_Meta_evalNat___closed__8;
lean_object* l_Lean_Delaborator_liftMetaM___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Delaborator_DelabM_monadQuotation___closed__1;
lean_object* l_Std_AssocList_find_x3f___at_Lean_Delaborator_delabFor___main___spec__6___boxed(lean_object*, lean_object*);
@ -578,7 +579,6 @@ lean_object* l___regBuiltin_Lean_Delaborator_delabOrM___closed__2;
lean_object* l_Lean_Delaborator_delabEq___lambda__1___closed__2;
lean_object* l_Lean_Delaborator_delabIff___lambda__1___closed__2;
lean_object* l_Lean_Delaborator_delabModN___lambda__1___closed__4;
extern lean_object* l_Lean_Meta_evalNat___main___closed__6;
lean_object* l___private_Lean_Delaborator_5__getUnusedName___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_mkAppStx___closed__6;
lean_object* l_Lean_Delaborator_withBindingBody___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -694,6 +694,7 @@ lean_object* l___regBuiltin_Lean_Delaborator_delabAndThen___closed__3;
lean_object* l___regBuiltin_Lean_Delaborator_delabseq___closed__1;
extern lean_object* l_Lean_Expr_heq_x3f___closed__1;
lean_object* l___regBuiltin_Lean_Delaborator_delabSub___closed__1;
extern lean_object* l_Lean_Meta_evalNat___closed__6;
lean_object* l_Lean_Delaborator_delabHEq(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Delaborator_delabHEq___lambda__1___closed__5;
lean_object* l_Lean_Delaborator_delabIff___lambda__1___closed__4;
@ -744,7 +745,6 @@ lean_object* l_Lean_Delaborator_delabLetE(lean_object*, lean_object*, lean_objec
lean_object* l_Lean_Meta_getLocalDecl___at_Lean_Meta_getFVarLocalDecl___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Delaborator_delabEquiv___lambda__1___closed__3;
extern lean_object* l_Std_Range_myMacro____x40_Init_Data_Range___hyg_301____closed__29;
extern lean_object* l_Lean_Meta_evalNat___main___closed__4;
lean_object* l_Lean_Expr_bindingName_x21(lean_object*);
extern lean_object* l_Lean_Expr_ctorName___closed__10;
lean_object* l_Lean_Delaborator_delabBOr___lambda__1(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -795,7 +795,6 @@ lean_object* l_Lean_Level_quote___main___lambda__5(lean_object*, lean_object*, l
lean_object* l_Lean_SMap_find_x3f___at_Lean_Delaborator_delabFor___main___spec__1(lean_object*, lean_object*);
extern lean_object* l_Lean_setOptionFromString___closed__1;
lean_object* l_Lean_getPPUniverses___closed__2;
extern lean_object* l_Lean_Meta_evalNat___main___closed__9;
lean_object* l___private_Lean_Delaborator_2__unresolveUsingNamespace(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Level_quote___main___lambda__4___closed__2;
lean_object* l___regBuiltin_Lean_Delaborator_delabEquiv___closed__5;
@ -885,6 +884,7 @@ lean_object* l_Lean_Delaborator_delabSort___closed__9;
lean_object* l_Lean_Delaborator_delabInfixOp(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Delaborator_delabMul___closed__1;
lean_object* l_Lean_Name_getRoot___main(lean_object*);
extern lean_object* l_Lean_Meta_evalNat___closed__1;
lean_object* l_Lean_getPPNotation___closed__2;
lean_object* l_Std_RBNode_find___main___at_Lean_Delaborator_getPPOption___spec__1(lean_object*, lean_object*);
lean_object* l___regBuiltin_Lean_Delaborator_delabLit___closed__1;
@ -16934,7 +16934,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Delaborator_getExprKind___closed__5;
x_2 = l_Lean_Meta_evalNat___main___closed__6;
x_2 = l_Lean_Meta_evalNat___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
@ -20048,7 +20048,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_mkAppStx___closed__6;
x_2 = l_Lean_Meta_evalNat___main___closed__9;
x_2 = l_Lean_Meta_evalNat___closed__8;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
@ -20139,7 +20139,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___regBuiltin_Lean_Delaborator_delabSub___closed__2;
x_2 = l_Lean_Meta_evalNat___main___closed__9;
x_2 = l_Lean_Meta_evalNat___closed__8;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
@ -20168,7 +20168,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_mkAppStx___closed__6;
x_2 = l_Lean_Meta_evalNat___main___closed__4;
x_2 = l_Lean_Meta_evalNat___closed__6;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
@ -20259,7 +20259,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___regBuiltin_Lean_Delaborator_delabMul___closed__2;
x_2 = l_Lean_Meta_evalNat___main___closed__4;
x_2 = l_Lean_Meta_evalNat___closed__6;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}

12
stage0/stdlib/Lean/Elab/BuiltinNotation.c generated
View file

@ -165,6 +165,7 @@ lean_object* l_Lean_Expr_getAppFn___main(lean_object*);
lean_object* l_Lean_Elab_Term_expandDbgTrace___boxed(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Expr_getAppArgs___closed__1;
extern lean_object* l___private_Lean_Meta_DiscrTree_6__shouldAddAsStar___closed__9;
extern lean_object* l_Lean_Meta_evalNat___closed__8;
lean_object* l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabTParserMacroAux___closed__9;
lean_object* l___regBuiltin_Lean_Elab_Term_expandAndM___closed__1;
lean_object* l_Lean_Elab_Term_mkAuxName(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -486,6 +487,7 @@ lean_object* l_Lean_Elab_Term_elabAnonymousCtor_match__2(lean_object*);
extern lean_object* l_Lean_boolToExpr___lambda__1___closed__6;
extern lean_object* l_Lean_Elab_Term_termElabAttribute;
lean_object* l___regBuiltin_Lean_Elab_Term_expandMapRev(lean_object*);
extern lean_object* l_Lean_Meta_evalNat___closed__6;
lean_object* l___regBuiltin_Lean_Elab_Term_expandEquiv___closed__3;
lean_object* l_Lean_Elab_Term_ExpandFComp___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_mkAtomFrom(lean_object*, lean_object*);
@ -517,7 +519,6 @@ lean_object* l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabTParser
lean_object* l___regBuiltin_Lean_Elab_Term_expandShow(lean_object*);
lean_object* l___regBuiltin_Lean_Elab_Term_expandSubtype___closed__1;
extern lean_object* l_Lean_Elab_macroAttribute;
extern lean_object* l_Lean_Meta_evalNat___main___closed__4;
lean_object* l_Lean_Elab_Term_elabParserMacro(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_expandSubtype___closed__2;
lean_object* l_Lean_Elab_Term_expandHave___closed__7;
@ -551,7 +552,6 @@ lean_object* l_Lean_Elab_Term_expandOr___closed__2;
lean_object* l___regBuiltin_Lean_Elab_Term_expandAdd(lean_object*);
lean_object* l_Lean_Elab_getRefPos___at_Lean_Elab_Term_elabPanic___spec__2___rarg___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_expandEmptyC___closed__7;
extern lean_object* l_Lean_Meta_evalNat___main___closed__9;
lean_object* l___regBuiltin_Lean_Elab_Term_expandCons(lean_object*);
lean_object* l_Lean_Elab_Term_expandMap___closed__2;
lean_object* l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabTParserMacroAux_match__1___rarg(lean_object*, lean_object*, lean_object*);
@ -7824,7 +7824,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Elab_Term_expandSub___closed__2;
x_2 = l_Lean_Meta_evalNat___main___closed__9;
x_2 = l_Lean_Meta_evalNat___closed__8;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
@ -7853,7 +7853,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_mkAppStx___closed__6;
x_2 = l_Lean_Meta_evalNat___main___closed__9;
x_2 = l_Lean_Meta_evalNat___closed__8;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
@ -7900,7 +7900,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Elab_Term_expandMul___closed__2;
x_2 = l_Lean_Meta_evalNat___main___closed__4;
x_2 = l_Lean_Meta_evalNat___closed__6;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
@ -7929,7 +7929,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_mkAppStx___closed__6;
x_2 = l_Lean_Meta_evalNat___main___closed__4;
x_2 = l_Lean_Meta_evalNat___closed__6;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}

4
stage0/stdlib/Lean/Elab/Declaration.c generated
View file

@ -185,7 +185,6 @@ lean_object* l_Lean_Elab_Command_expandInitialize___closed__17;
lean_object* l_Lean_Elab_Command_expandInitialize___closed__1;
lean_object* l_Lean_throwErrorAt___at___private_Lean_Elab_Term_0__Lean_Elab_Term_elabTermAux___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_umapMAux___main___at___private_Lean_Elab_Declaration_0__Lean_Elab_Command_inductiveSyntaxToView___spec__1___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l___private_Lean_Meta_RecursorInfo_10__getProduceMotiveAndRecursive___closed__1;
lean_object* l_Lean_Elab_Command_expandInitialize___boxed(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Elab_Term_expandArrayLit___closed__11;
extern lean_object* l_Lean_Elab_Command_isDefLike___closed__9;
@ -348,6 +347,7 @@ lean_object* l_Lean_Elab_Command_expandMutualElement_match__2___rarg(lean_object
uint8_t l___private_Lean_Elab_Declaration_0__Lean_Elab_Command_isMutualInductive(lean_object*);
lean_object* l_Lean_Elab_Command_expandInitialize___closed__42;
lean_object* l_Lean_throwError___at_Lean_Elab_Term_throwErrorIfErrors___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Expr_withAppAux___main___at_Lean_Meta_induction___spec__12___closed__4;
lean_object* l_Lean_Elab_Command_expandMutualNamespace_match__3___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_checkValidInductiveModifier(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_mkConst(lean_object*, lean_object*);
@ -5273,7 +5273,7 @@ x_7 = lean_array_get_size(x_6);
x_8 = lean_usize_of_nat(x_7);
lean_dec(x_7);
x_9 = 0;
x_10 = l___private_Lean_Meta_RecursorInfo_10__getProduceMotiveAndRecursive___closed__1;
x_10 = l_Lean_Expr_withAppAux___main___at_Lean_Meta_induction___spec__12___closed__4;
x_11 = l_Array_forInUnsafe_loop___at_Lean_Elab_Command_expandMutualElement___spec__1(x_6, x_8, x_9, x_10, x_2, x_3);
lean_dec(x_6);
if (lean_obj_tag(x_11) == 0)

6
stage0/stdlib/Lean/Elab/MutualDef.c generated
View file

@ -349,7 +349,6 @@ lean_object* l_Lean_mkFVar(lean_object*);
uint8_t l_Lean_Expr_Data_binderInfo(uint64_t);
lean_object* l_Lean_Elab_mkDeclName___at___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabHeaders___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_checkModifiers___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Meta_forallTelescopeCompatibleAux___rarg___lambda__3___closed__3;
size_t lean_usize_of_nat(lean_object*);
lean_object* l_Nat_foldMAux___main___at_Lean_Elab_Term_MutualClosure_pushMain___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_MutualClosure_mkInitialUsedFVarsMap_match__1(lean_object*);
@ -554,6 +553,7 @@ lean_object* l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_check___lambda__3
uint8_t l_Array_anyRangeMAux___main___at___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_isTheorem___spec__1(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_umapMAux___main___at___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabFunValues___spec__1___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Elab_elabAttr___rarg___lambda__3___closed__2;
extern lean_object* l___private_Lean_Meta_RecursorInfo_0__Lean_Meta_getMajorPosDepElim___lambda__1___closed__3;
lean_object* l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_check___lambda__5(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_MutualClosure_mkInitialUsedFVarsMap___spec__2(lean_object*, lean_object*, size_t, size_t, lean_object*);
lean_object* l_Lean_Elab_mkDeclName___at___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabHeaders___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -2616,7 +2616,7 @@ if (lean_obj_tag(x_16) == 0)
lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; uint8_t x_23;
x_17 = lean_alloc_ctor(4, 1, 0);
lean_ctor_set(x_17, 0, x_1);
x_18 = l_Lean_Meta_forallTelescopeCompatibleAux___rarg___lambda__3___closed__3;
x_18 = l___private_Lean_Meta_RecursorInfo_0__Lean_Meta_getMajorPosDepElim___lambda__1___closed__3;
x_19 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_19, 0, x_18);
lean_ctor_set(x_19, 1, x_17);
@ -3040,7 +3040,7 @@ x_16 = l_Lean_Elab_mkDeclName___rarg___closed__2;
x_17 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_17, 0, x_16);
lean_ctor_set(x_17, 1, x_15);
x_18 = l_Lean_Meta_forallTelescopeCompatibleAux___rarg___lambda__3___closed__3;
x_18 = l___private_Lean_Meta_RecursorInfo_0__Lean_Meta_getMajorPosDepElim___lambda__1___closed__3;
x_19 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_19, 0, x_17);
lean_ctor_set(x_19, 1, x_18);

14
stage0/stdlib/Lean/Elab/PreDefinition/Structural.c generated
View file

@ -58,7 +58,6 @@ lean_object* l_Lean_Meta_MatcherApp_addArg(lean_object*, lean_object*, lean_obje
lean_object* l___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_mkBRecOn___closed__2;
lean_object* l_Lean_hasConst___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_findRecArg_loop___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Std_HashMap_inhabited___closed__1;
lean_object* l_Lean_Meta_forallTelescopeReducing___at_Lean_Meta_generalizeIndices___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_array_uset(lean_object*, size_t, lean_object*);
lean_object* l___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_ensureNoRecFn___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_toBelowAux___closed__16;
@ -71,6 +70,7 @@ lean_object* l___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_elimRec
lean_object* l_Array_filterAux___main___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_mkBRecOn___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Array_empty___closed__1;
lean_object* l_Lean_Expr_withAppAux___main___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_replaceRecApps_loop___spec__3___lambda__2___closed__1;
lean_object* l_Lean_Meta_forallTelescopeReducing___at___private_Lean_Meta_RecursorInfo_0__Lean_Meta_getProduceMotiveAndRecursive___spec__5___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_hasBadParamDep_x3f_match__1(lean_object*);
lean_object* lean_environment_find(lean_object*, lean_object*);
lean_object* l_Lean_addTrace___at_Lean_Meta_substCore___spec__12(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -7014,7 +7014,7 @@ x_25 = lean_alloc_closure((void*)(l___private_Lean_Elab_PreDefinition_Structural
lean_closure_set(x_25, 0, x_3);
lean_closure_set(x_25, 1, x_4);
lean_closure_set(x_25, 2, x_1);
x_26 = l_Lean_Meta_forallTelescopeReducing___at_Lean_Meta_generalizeIndices___spec__1___rarg(x_11, x_25, x_5, x_6, x_7, x_8, x_13);
x_26 = l_Lean_Meta_forallTelescopeReducing___at___private_Lean_Meta_RecursorInfo_0__Lean_Meta_getProduceMotiveAndRecursive___spec__5___rarg(x_11, x_25, x_5, x_6, x_7, x_8, x_13);
return x_26;
}
else
@ -7408,7 +7408,7 @@ x_113 = lean_alloc_closure((void*)(l___private_Lean_Elab_PreDefinition_Structura
lean_closure_set(x_113, 0, x_3);
lean_closure_set(x_113, 1, x_4);
lean_closure_set(x_113, 2, x_1);
x_114 = l_Lean_Meta_forallTelescopeReducing___at_Lean_Meta_generalizeIndices___spec__1___rarg(x_11, x_113, x_5, x_6, x_7, x_8, x_13);
x_114 = l_Lean_Meta_forallTelescopeReducing___at___private_Lean_Meta_RecursorInfo_0__Lean_Meta_getProduceMotiveAndRecursive___spec__5___rarg(x_11, x_113, x_5, x_6, x_7, x_8, x_13);
return x_114;
}
}
@ -7421,7 +7421,7 @@ x_115 = lean_alloc_closure((void*)(l___private_Lean_Elab_PreDefinition_Structura
lean_closure_set(x_115, 0, x_3);
lean_closure_set(x_115, 1, x_4);
lean_closure_set(x_115, 2, x_1);
x_116 = l_Lean_Meta_forallTelescopeReducing___at_Lean_Meta_generalizeIndices___spec__1___rarg(x_11, x_115, x_5, x_6, x_7, x_8, x_13);
x_116 = l_Lean_Meta_forallTelescopeReducing___at___private_Lean_Meta_RecursorInfo_0__Lean_Meta_getProduceMotiveAndRecursive___spec__5___rarg(x_11, x_115, x_5, x_6, x_7, x_8, x_13);
return x_116;
}
}
@ -7434,7 +7434,7 @@ x_117 = lean_alloc_closure((void*)(l___private_Lean_Elab_PreDefinition_Structura
lean_closure_set(x_117, 0, x_3);
lean_closure_set(x_117, 1, x_4);
lean_closure_set(x_117, 2, x_1);
x_118 = l_Lean_Meta_forallTelescopeReducing___at_Lean_Meta_generalizeIndices___spec__1___rarg(x_11, x_117, x_5, x_6, x_7, x_8, x_13);
x_118 = l_Lean_Meta_forallTelescopeReducing___at___private_Lean_Meta_RecursorInfo_0__Lean_Meta_getProduceMotiveAndRecursive___spec__5___rarg(x_11, x_117, x_5, x_6, x_7, x_8, x_13);
return x_118;
}
}
@ -7446,7 +7446,7 @@ x_119 = lean_alloc_closure((void*)(l___private_Lean_Elab_PreDefinition_Structura
lean_closure_set(x_119, 0, x_3);
lean_closure_set(x_119, 1, x_4);
lean_closure_set(x_119, 2, x_1);
x_120 = l_Lean_Meta_forallTelescopeReducing___at_Lean_Meta_generalizeIndices___spec__1___rarg(x_11, x_119, x_5, x_6, x_7, x_8, x_13);
x_120 = l_Lean_Meta_forallTelescopeReducing___at___private_Lean_Meta_RecursorInfo_0__Lean_Meta_getProduceMotiveAndRecursive___spec__5___rarg(x_11, x_119, x_5, x_6, x_7, x_8, x_13);
return x_120;
}
}
@ -7457,7 +7457,7 @@ x_121 = lean_alloc_closure((void*)(l___private_Lean_Elab_PreDefinition_Structura
lean_closure_set(x_121, 0, x_3);
lean_closure_set(x_121, 1, x_4);
lean_closure_set(x_121, 2, x_1);
x_122 = l_Lean_Meta_forallTelescopeReducing___at_Lean_Meta_generalizeIndices___spec__1___rarg(x_11, x_121, x_5, x_6, x_7, x_8, x_13);
x_122 = l_Lean_Meta_forallTelescopeReducing___at___private_Lean_Meta_RecursorInfo_0__Lean_Meta_getProduceMotiveAndRecursive___spec__5___rarg(x_11, x_121, x_5, x_6, x_7, x_8, x_13);
return x_122;
}
}

10
stage0/stdlib/Lean/Elab/Term.c generated
View file

@ -645,6 +645,7 @@ lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_tryLiftAndCoe___closed
lean_object* l_Lean_Meta_isExprDefEq___at_Lean_Elab_Term_synthesizeInstMVarCore___spec__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_resolveLocalName_loop_match__2___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_tryCoeSort___closed__9;
extern lean_object* l_Lean_Meta_evalNat___closed__3;
lean_object* l_Lean_Elab_Term_TermElabM_inhabited___closed__1;
lean_object* l___private_Lean_Meta_SynthInstance_9__trySynthInstanceImp(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
size_t l_USize_land(size_t, size_t);
@ -818,7 +819,6 @@ lean_object* l_Lean_Elab_Term_isExprMVarAssigned(lean_object*, lean_object*, lea
lean_object* l_Lean_Elab_Term_elabCharLit___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_elabHole___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_Context_macroStack___default;
extern lean_object* l_Lean_Meta_evalNat___main___closed__8;
lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_tryCoe_match__1(lean_object*);
lean_object* l_Lean_Elab_Term_mkExplicitBinder(lean_object*, lean_object*);
lean_object* l_Lean_Meta_throwAppTypeMismatch___at_Lean_Elab_Term_throwTypeMismatchError___spec__2___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -833,7 +833,6 @@ lean_object* l_Lean_MonadTracer_trace___at_Lean_Meta_isLevelDefEq___spec__2(lean
lean_object* l_Lean_Elab_Term_mkTypeMismatchError___closed__2;
lean_object* l_Lean_Elab_Term_adaptExpander(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_tryPostponeIfMVar(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Meta_evalNat___main___closed__7;
lean_object* l_Lean_Syntax_getPos(lean_object*);
lean_object* l_Lean_Elab_Term_getMessageLog___boxed(lean_object*);
lean_object* l_Lean_Elab_Term_Lean_Elab_Term___instance__6___rarg___closed__1;
@ -871,6 +870,7 @@ lean_object* l_Lean_Elab_Term_withFreshMacroScope___rarg(lean_object*, lean_obje
lean_object* l_Lean_Elab_Term_TermElabM_toIO_match__1(lean_object*, lean_object*);
lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Term_0__Lean_Elab_Term_applyAttributesCore___spec__1___closed__1;
uint8_t l_Lean_Syntax_isNone(lean_object*);
extern lean_object* l_Lean_Meta_evalNat___closed__2;
extern lean_object* l_Lean_TraceState_Inhabited___closed__1;
lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_mkFreshLevelMVars___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Meta_mkSorry___rarg___lambda__1___closed__2;
@ -31682,7 +31682,7 @@ lean_dec(x_15);
x_18 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_18, 0, x_16);
lean_ctor_set(x_18, 1, x_2);
x_19 = l_Lean_Meta_evalNat___main___closed__7;
x_19 = l_Lean_Meta_evalNat___closed__2;
lean_inc(x_18);
x_20 = l_Lean_mkConst(x_19, x_18);
lean_inc(x_1);
@ -31696,7 +31696,7 @@ if (x_23 == 0)
{
lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27;
x_24 = lean_ctor_get(x_22, 0);
x_25 = l_Lean_Meta_evalNat___main___closed__8;
x_25 = l_Lean_Meta_evalNat___closed__3;
x_26 = l_Lean_mkConst(x_25, x_18);
x_27 = l_Lean_mkApp3(x_26, x_1, x_24, x_3);
lean_ctor_set(x_22, 0, x_27);
@ -31710,7 +31710,7 @@ x_29 = lean_ctor_get(x_22, 1);
lean_inc(x_29);
lean_inc(x_28);
lean_dec(x_22);
x_30 = l_Lean_Meta_evalNat___main___closed__8;
x_30 = l_Lean_Meta_evalNat___closed__3;
x_31 = l_Lean_mkConst(x_30, x_18);
x_32 = l_Lean_mkApp3(x_31, x_1, x_28, x_3);
x_33 = lean_alloc_ctor(0, 2, 0);

31
stage0/stdlib/Lean/Meta/Basic.c generated
View file

@ -521,6 +521,7 @@ lean_object* l___private_Lean_Meta_Basic_12__withNewLocalInstancesImp___main___r
lean_object* l_Lean_Meta_getLocalDeclFromUserName___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_monadNameGeneratorLift___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Meta_inferType___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Meta_ParamInfo_isExplicit___boxed(lean_object*);
lean_object* l___private_Lean_Meta_Basic_12__withNewLocalInstancesImp___main___at___private_Lean_Meta_Basic_21__forallBoundedTelescopeImp___spec__22(lean_object*);
lean_object* l___private_Lean_Meta_Basic_24__forallMetaTelescopeReducingAux(uint8_t, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Meta_Basic_12__withNewLocalInstancesImp___main___at___private_Lean_Meta_Basic_20__forallTelescopeReducingImp___spec__23___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -782,6 +783,7 @@ lean_object* l___private_Lean_Meta_Basic_12__withNewLocalInstancesImp___main___a
lean_object* l_Lean_throwError___at_Lean_Meta_mkWHNFRef___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Meta_Basic_14__forallTelescopeReducingAuxAux___rarg(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_Lean_MonadMCtx___closed__1;
uint8_t l_Lean_Meta_ParamInfo_isExplicit(lean_object*);
lean_object* l___private_Lean_Meta_Basic_12__withNewLocalInstancesImp___main___at___private_Lean_Meta_Basic_21__forallBoundedTelescopeImp___spec__14(lean_object*);
lean_object* l___private_Lean_Meta_Basic_12__withNewLocalInstancesImp___main___at___private_Lean_Meta_Basic_20__forallTelescopeReducingImp___spec__4___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Meta_Basic_12__withNewLocalInstancesImp___main___rarg___closed__5;
@ -1334,6 +1336,35 @@ x_1 = l_Lean_Meta_ParamInfo_inhabited___closed__1;
return x_1;
}
}
uint8_t l_Lean_Meta_ParamInfo_isExplicit(lean_object* x_1) {
_start:
{
uint8_t x_2;
x_2 = lean_ctor_get_uint8(x_1, sizeof(void*)*1);
if (x_2 == 0)
{
uint8_t x_3;
x_3 = lean_ctor_get_uint8(x_1, sizeof(void*)*1 + 1);
return x_3;
}
else
{
uint8_t x_4;
x_4 = 0;
return x_4;
}
}
}
lean_object* l_Lean_Meta_ParamInfo_isExplicit___boxed(lean_object* x_1) {
_start:
{
uint8_t x_2; lean_object* x_3;
x_2 = l_Lean_Meta_ParamInfo_isExplicit(x_1);
lean_dec(x_1);
x_3 = lean_box(x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Meta_InfoCacheKey_Inhabited___closed__1() {
_start:
{

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

@ -118,7 +118,6 @@ lean_object* l_Lean_Meta_MatcherApp_addArg(lean_object*, lean_object*, lean_obje
lean_object* l_List_filterAux___main___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_processConstructor___spec__6(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_Match_Pattern_toExpr_match__1(lean_object*);
uint8_t l_List_foldr___main___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_hasNatValPattern___spec__1(uint8_t, lean_object*);
lean_object* l_Lean_Meta_forallTelescopeReducing___at_Lean_Meta_generalizeIndices___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_array_uset(lean_object*, size_t, lean_object*);
lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_hasNatValPattern_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_Match_Problem_Lean_Meta_Match_Match___instance__3___closed__1;
@ -141,7 +140,7 @@ lean_object* l_Lean_Meta_Match_processInaccessibleAsCtor_match__1(lean_object*);
size_t l_USize_sub(size_t, size_t);
extern lean_object* l_Array_empty___closed__1;
lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_expandVarIntoArrayLit(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_environment_find(lean_object*, lean_object*);
lean_object* l_Lean_Meta_forallTelescopeReducing___at___private_Lean_Meta_RecursorInfo_0__Lean_Meta_getProduceMotiveAndRecursive___spec__5___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_expandVarIntoCtor_x3f_match__3(lean_object*);
lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_collectArraySizes___boxed(lean_object*);
lean_object* l_Lean_Meta_isExprDefEqAux(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -389,6 +388,7 @@ lean_object* l_List_map___main___at_Lean_Meta_Match_Pattern_applyFVarSubst___spe
uint8_t l_Std_AssocList_contains___at_Lean_Meta_Match_Extension_State_addEntry___spec__7(lean_object*, lean_object*);
lean_object* l_Lean_Meta_getArrayArgType(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_getInductiveVal_x3f_match__2(lean_object*);
extern lean_object* l___private_Lean_Meta_RecursorInfo_0__Lean_Meta_getMajorPosDepElim___closed__8;
lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_expandVarIntoArrayLit___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_List_map___main___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_processSkipInaccessible___spec__1(lean_object*);
lean_object* l_Lean_Expr_toHeadIndex___main(lean_object*);
@ -413,6 +413,7 @@ lean_object* l_Lean_Meta_Match_Unify_unify___closed__2;
lean_object* l_List_map___main___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_expandVarIntoCtor_x3f___spec__3(lean_object*, lean_object*);
lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_processSkipInaccessible___closed__1;
lean_object* l_Lean_Meta_Match_Example_replaceFVarId_match__1(lean_object*);
extern lean_object* l_Lean_Meta_evalNat_match__2___rarg___closed__1;
lean_object* l_List_filterAux___main___at_Lean_Meta_Match_Alt_replaceFVarId___spec__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_replaceRef(lean_object*, lean_object*);
lean_object* lean_array_get(lean_object*, lean_object*, lean_object*);
@ -487,6 +488,7 @@ extern lean_object* l_List_reprAux___main___rarg___closed__1;
lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_getUElimPos_x3f___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Std_mkHashMap___at_Lean_Meta_Match_Extension_State_map___default___spec__1(lean_object*);
lean_object* l_Lean_Meta_Match_processInaccessibleAsCtor___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_getConstInfo___at___private_Lean_Meta_RecursorInfo_0__Lean_Meta_mkRecursorInfoForKernelRec___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_addMessageContextFull___at_Lean_Meta_Lean_AddMessageContext___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_MatcherApp_addArg___lambda__2___closed__3;
lean_object* l_Lean_Meta_Match_Pattern_toMessageData_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -494,7 +496,6 @@ extern size_t l_Std_PersistentHashMap_insertAux___main___rarg___closed__2;
lean_object* l_Lean_Meta_Match_processInaccessibleAsCtor___closed__6;
lean_object* l_Lean_Meta_Match_mkMatcher___lambda__1___closed__17;
lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_processAsPattern___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_getConstInfo___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_getInductiveVal_x3f___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_List_filterAux___main___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_processValue___spec__4(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_Match_Alt_checkAndReplaceFVarId___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_expandVarIntoArrayLit_loop_match__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
@ -502,7 +503,6 @@ lean_object* l___private_Lean_Meta_Basic_29__withExistingLocalDeclsImp___rarg(le
lean_object* l_Lean_Meta_Match_mkMatcher___lambda__1___closed__1;
lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_hasCtorPattern_match__1(lean_object*);
lean_object* l_Lean_Meta_mkFreshExprMVar___at_Lean_Meta_Match_mkMatcher___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_throwUnknownConstant___rarg___closed__5;
lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_getUElimPos_x3f___closed__2;
uint8_t l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_isFirstPatternVar(lean_object*);
lean_object* l_Lean_Meta_matchMatcherApp_x3f_match__2___rarg(lean_object*, lean_object*, lean_object*);
@ -543,13 +543,11 @@ lean_object* l_Lean_Meta_Match_Extension_extension___closed__4;
uint8_t l_Array_isEmpty___rarg(lean_object*);
lean_object* l_Lean_Meta_Match_Alt_toMessageData___closed__1;
lean_object* l_Lean_LocalDecl_toExpr(lean_object*);
lean_object* l_Lean_Meta_MatcherApp_addArg___lambda__4___closed__3;
lean_object* l_Lean_Meta_Match_Unify_unify___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_isExprDefEq___at_Lean_Meta_Match_Unify_unify___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_Match_Unify_unify___closed__1;
lean_object* l_Lean_Meta_instantiateLambda___at___private_Lean_Meta_Match_Match_0__Lean_Meta_updateAlts___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_Match_Extension_addMatcherInfo(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_throwUnknownConstant___rarg___closed__3;
size_t l_USize_mul(size_t, size_t);
lean_object* l_Array_iterateMAux___main___at_Lean_Meta_Match_Extension_State_addEntry___spec__5___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_List_redLength___main___rarg(lean_object*);
@ -561,7 +559,6 @@ lean_object* l_Lean_Meta_isLevelDefEqAux___boxed(lean_object*, lean_object*, lea
lean_object* l_Lean_Meta_Match_Problem_toMessageData___lambda__1___closed__5;
lean_object* l_List_mapM___main___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_processArrayLit___spec__8(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_Match_Unify_assign___closed__1;
lean_object* l_Lean_getConstInfo___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_getInductiveVal_x3f___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_formatEntry___closed__1;
lean_object* l_Array_iterateMAux___main___at_Array_append___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_List_map___main___at_Lean_Meta_Match_Example_applyFVarSubst___spec__1___boxed(lean_object*, lean_object*);
@ -587,6 +584,7 @@ lean_object* l_Lean_mkLevelMVar(lean_object*);
lean_object* l_Lean_Meta_Match_mkMatcher___lambda__1___closed__10;
lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_processArrayLit___closed__3;
lean_object* l_Lean_Expr_replaceFVarId(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Meta_evalNat___closed__15;
lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_expandVarIntoCtor_x3f___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_Match_Extension_mkExtension___lambda__1(lean_object*);
extern lean_object* l___private_Lean_Meta_ExprDefEq_8__checkTypesAndAssign___lambda__1___closed__1;
@ -744,7 +742,6 @@ lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_processSkipIna
lean_object* l_Lean_Meta_Match_Alt_checkAndReplaceFVarId___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_matchMatcherApp_x3f_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_Match_Extension_mkExtension(lean_object*);
extern lean_object* l_Lean_Meta_evalNat___main___closed__17;
lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_updateAlts___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Format_paren___closed__4;
lean_object* l_Std_HashMapImp_expand___at_Lean_Meta_Match_Extension_State_addEntry___spec__8(lean_object*, lean_object*);
@ -858,7 +855,6 @@ lean_object* l_Lean_Meta_Match_Alt_checkAndReplaceFVarId___closed__9;
lean_object* l_Lean_Meta_Match_State_used___default;
lean_object* l_Lean_Meta_forallBoundedTelescope___at___private_Lean_Meta_Match_Match_0__Lean_Meta_updateAlts___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_Match_Alt_checkAndReplaceFVarId___closed__8;
extern lean_object* l_Lean_Meta_evalNat___main___closed__1;
lean_object* l_Lean_Meta_instantiateMVars___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_unify_x3f___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_List_mapM___main___at_Lean_Meta_Match_Problem_toMessageData___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_expandVarIntoArrayLit_loop___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -877,7 +873,6 @@ lean_object* l_List_filterAux___main___at_Lean_Meta_Match_Alt_replaceFVarId___sp
lean_object* l_Lean_Meta_withExistingLocalDecls___at_Lean_Meta_Match_Alt_toMessageData___spec__2(lean_object*);
lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_isNextVar_match__1(lean_object*);
uint8_t l_Std_HashSetImp_contains___at_Lean_Meta_Match_mkMatcher___spec__5(lean_object*, lean_object*);
extern lean_object* l___private_Lean_Meta_RecursorInfo_5__getMajorPosDepElim___closed__19;
lean_object* l_List_mapM___main___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_expandVarIntoArrayLit_loop___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_Match_MatcherInfo_numAlts(lean_object*);
lean_object* l_List_map___main___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_processValue___spec__7(lean_object*, lean_object*);
@ -15133,7 +15128,7 @@ lean_closure_set(x_30, 0, x_26);
lean_closure_set(x_30, 1, x_1);
lean_closure_set(x_30, 2, x_3);
lean_closure_set(x_30, 3, x_17);
x_31 = l_Lean_Meta_forallTelescopeReducing___at_Lean_Meta_generalizeIndices___spec__1___rarg(x_28, x_30, x_5, x_6, x_7, x_8, x_29);
x_31 = l_Lean_Meta_forallTelescopeReducing___at___private_Lean_Meta_RecursorInfo_0__Lean_Meta_getProduceMotiveAndRecursive___spec__5___rarg(x_28, x_30, x_5, x_6, x_7, x_8, x_29);
return x_31;
}
else
@ -15428,94 +15423,6 @@ x_2 = lean_alloc_closure((void*)(l___private_Lean_Meta_Match_Match_0__Lean_Meta_
return x_2;
}
}
lean_object* l_Lean_getConstInfo___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_getInductiveVal_x3f___spec__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
_start:
{
lean_object* x_7; uint8_t x_8;
x_7 = lean_st_ref_get(x_5, x_6);
x_8 = !lean_is_exclusive(x_7);
if (x_8 == 0)
{
lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12;
x_9 = lean_ctor_get(x_7, 0);
x_10 = lean_ctor_get(x_7, 1);
x_11 = lean_ctor_get(x_9, 0);
lean_inc(x_11);
lean_dec(x_9);
lean_inc(x_1);
x_12 = lean_environment_find(x_11, x_1);
if (lean_obj_tag(x_12) == 0)
{
lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18;
lean_free_object(x_7);
x_13 = lean_alloc_ctor(4, 1, 0);
lean_ctor_set(x_13, 0, x_1);
x_14 = l_Lean_throwUnknownConstant___rarg___closed__3;
x_15 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_15, 0, x_14);
lean_ctor_set(x_15, 1, x_13);
x_16 = l_Lean_throwUnknownConstant___rarg___closed__5;
x_17 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_17, 0, x_15);
lean_ctor_set(x_17, 1, x_16);
x_18 = l_Lean_throwError___at_Lean_Meta_getArrayArgType___spec__3___rarg(x_17, x_2, x_3, x_4, x_5, x_10);
return x_18;
}
else
{
lean_object* x_19;
lean_dec(x_1);
x_19 = lean_ctor_get(x_12, 0);
lean_inc(x_19);
lean_dec(x_12);
lean_ctor_set(x_7, 0, x_19);
return x_7;
}
}
else
{
lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23;
x_20 = lean_ctor_get(x_7, 0);
x_21 = lean_ctor_get(x_7, 1);
lean_inc(x_21);
lean_inc(x_20);
lean_dec(x_7);
x_22 = lean_ctor_get(x_20, 0);
lean_inc(x_22);
lean_dec(x_20);
lean_inc(x_1);
x_23 = lean_environment_find(x_22, x_1);
if (lean_obj_tag(x_23) == 0)
{
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_24 = lean_alloc_ctor(4, 1, 0);
lean_ctor_set(x_24, 0, x_1);
x_25 = l_Lean_throwUnknownConstant___rarg___closed__3;
x_26 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_26, 0, x_25);
lean_ctor_set(x_26, 1, x_24);
x_27 = l_Lean_throwUnknownConstant___rarg___closed__5;
x_28 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_28, 0, x_26);
lean_ctor_set(x_28, 1, x_27);
x_29 = l_Lean_throwError___at_Lean_Meta_getArrayArgType___spec__3___rarg(x_28, x_2, x_3, x_4, x_5, x_21);
return x_29;
}
else
{
lean_object* x_30; lean_object* x_31;
lean_dec(x_1);
x_30 = lean_ctor_get(x_23, 0);
lean_inc(x_30);
lean_dec(x_23);
x_31 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_31, 0, x_30);
lean_ctor_set(x_31, 1, x_21);
return x_31;
}
}
}
}
lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_getInductiveVal_x3f(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:
{
@ -15556,7 +15463,7 @@ lean_free_object(x_10);
x_15 = lean_ctor_get(x_14, 0);
lean_inc(x_15);
lean_dec(x_14);
x_16 = l_Lean_getConstInfo___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_getInductiveVal_x3f___spec__1(x_15, x_2, x_3, x_4, x_5, x_13);
x_16 = l_Lean_getConstInfo___at___private_Lean_Meta_RecursorInfo_0__Lean_Meta_mkRecursorInfoForKernelRec___spec__2(x_15, x_2, x_3, x_4, x_5, x_13);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
@ -15680,7 +15587,7 @@ lean_object* x_40; lean_object* x_41;
x_40 = lean_ctor_get(x_39, 0);
lean_inc(x_40);
lean_dec(x_39);
x_41 = l_Lean_getConstInfo___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_getInductiveVal_x3f___spec__1(x_40, x_2, x_3, x_4, x_5, x_38);
x_41 = l_Lean_getConstInfo___at___private_Lean_Meta_RecursorInfo_0__Lean_Meta_mkRecursorInfoForKernelRec___spec__2(x_40, x_2, x_3, x_4, x_5, x_38);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
@ -15838,18 +15745,6 @@ return x_65;
}
}
}
lean_object* l_Lean_getConstInfo___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_getInductiveVal_x3f___spec__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
_start:
{
lean_object* x_7;
x_7 = l_Lean_getConstInfo___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_getInductiveVal_x3f___spec__1(x_1, x_2, x_3, x_4, x_5, x_6);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
return x_7;
}
}
lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_hasRecursiveType_match__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
@ -23227,7 +23122,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Literal_type___closed__2;
x_2 = l_Lean_Meta_evalNat___main___closed__1;
x_2 = l_Lean_Meta_evalNat_match__2___rarg___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
@ -23342,7 +23237,7 @@ x_30 = lean_box(0);
x_31 = l_Lean_mkNatLit(x_29);
lean_ctor_set(x_12, 0, x_31);
lean_ctor_set(x_10, 1, x_30);
x_32 = l_Lean_Meta_evalNat___main___closed__17;
x_32 = l_Lean_Meta_evalNat___closed__15;
x_33 = lean_alloc_ctor(2, 4, 0);
lean_ctor_set(x_33, 0, x_32);
lean_ctor_set(x_33, 1, x_30);
@ -23390,7 +23285,7 @@ lean_ctor_set(x_12, 0, x_43);
x_44 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_44, 0, x_12);
lean_ctor_set(x_44, 1, x_42);
x_45 = l_Lean_Meta_evalNat___main___closed__17;
x_45 = l_Lean_Meta_evalNat___closed__15;
x_46 = lean_alloc_ctor(2, 4, 0);
lean_ctor_set(x_46, 0, x_45);
lean_ctor_set(x_46, 1, x_42);
@ -23454,7 +23349,7 @@ if (lean_is_scalar(x_51)) {
}
lean_ctor_set(x_59, 0, x_12);
lean_ctor_set(x_59, 1, x_57);
x_60 = l_Lean_Meta_evalNat___main___closed__17;
x_60 = l_Lean_Meta_evalNat___closed__15;
x_61 = lean_alloc_ctor(2, 4, 0);
lean_ctor_set(x_61, 0, x_60);
lean_ctor_set(x_61, 1, x_57);
@ -23622,7 +23517,7 @@ if (lean_is_scalar(x_79)) {
}
lean_ctor_set(x_88, 0, x_87);
lean_ctor_set(x_88, 1, x_85);
x_89 = l_Lean_Meta_evalNat___main___closed__17;
x_89 = l_Lean_Meta_evalNat___closed__15;
x_90 = lean_alloc_ctor(2, 4, 0);
lean_ctor_set(x_90, 0, x_89);
lean_ctor_set(x_90, 1, x_85);
@ -23864,7 +23759,7 @@ if (lean_is_scalar(x_119)) {
}
lean_ctor_set(x_128, 0, x_127);
lean_ctor_set(x_128, 1, x_125);
x_129 = l_Lean_Meta_evalNat___main___closed__17;
x_129 = l_Lean_Meta_evalNat___closed__15;
x_130 = lean_alloc_ctor(2, 4, 0);
lean_ctor_set(x_130, 0, x_129);
lean_ctor_set(x_130, 1, x_125);
@ -32776,15 +32671,6 @@ x_2 = l_Lean_stringToMessageData(x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Meta_MatcherApp_addArg___lambda__4___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l___private_Lean_Meta_RecursorInfo_5__getMajorPosDepElim___closed__19;
x_2 = l_Lean_stringToMessageData(x_1);
return x_2;
}
}
lean_object* l_Lean_Meta_MatcherApp_addArg___lambda__4(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:
{
@ -32810,7 +32696,7 @@ x_16 = l_Lean_Meta_MatcherApp_addArg___lambda__4___closed__2;
x_17 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_17, 0, x_16);
lean_ctor_set(x_17, 1, x_15);
x_18 = l_Lean_Meta_MatcherApp_addArg___lambda__4___closed__3;
x_18 = l___private_Lean_Meta_RecursorInfo_0__Lean_Meta_getMajorPosDepElim___closed__8;
x_19 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_19, 0, x_17);
lean_ctor_set(x_19, 1, x_18);
@ -33397,8 +33283,6 @@ l_Lean_Meta_MatcherApp_addArg___lambda__4___closed__1 = _init_l_Lean_Meta_Matche
lean_mark_persistent(l_Lean_Meta_MatcherApp_addArg___lambda__4___closed__1);
l_Lean_Meta_MatcherApp_addArg___lambda__4___closed__2 = _init_l_Lean_Meta_MatcherApp_addArg___lambda__4___closed__2();
lean_mark_persistent(l_Lean_Meta_MatcherApp_addArg___lambda__4___closed__2);
l_Lean_Meta_MatcherApp_addArg___lambda__4___closed__3 = _init_l_Lean_Meta_MatcherApp_addArg___lambda__4___closed__3();
lean_mark_persistent(l_Lean_Meta_MatcherApp_addArg___lambda__4___closed__3);
res = l_Lean_Meta_initFn____x40_Lean_Meta_Match_Match___hyg_7756_(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);

3092
stage0/stdlib/Lean/Meta/Offset.c generated
View file

File diff suppressed because it is too large Load diff

12115
stage0/stdlib/Lean/Meta/RecursorInfo.c generated
View file

File diff suppressed because it is too large Load diff

1445
stage0/stdlib/Lean/Meta/Reduce.c generated
View file

File diff suppressed because it is too large Load diff

5424
stage0/stdlib/Lean/Meta/ReduceEval.c generated
View file

File diff suppressed because it is too large Load diff

1224
stage0/stdlib/Lean/Meta/Tactic/Cases.c generated
View file

File diff suppressed because it is too large Load diff

728
stage0/stdlib/Lean/Meta/Tactic/Induction.c generated
View file

File diff suppressed because it is too large Load diff

310
stage0/stdlib/Lean/Meta/TransparencyMode.c generated
View file

@ -14,17 +14,26 @@
extern "C" {
#endif
size_t l_Lean_Meta_TransparencyMode_hash(uint8_t);
lean_object* l_Lean_Meta_TransparencyMode_Hashable___closed__1;
lean_object* l_Lean_Meta_TransparencyMode_beq_match__1(lean_object*);
lean_object* l_Lean_Meta_TransparencyMode_beq_match__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_TransparencyMode_beq_match__1___rarg(uint8_t, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_TransparencyMode_hash_match__1(lean_object*);
lean_object* l_Lean_Meta_TransparencyMode_lt___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Meta_TransparencyMode_Hashable;
uint8_t l_Lean_Meta_TransparencyMode_Inhabited;
lean_object* l_Lean_Meta_TransparencyMode_HasBeq___closed__1;
lean_object* l_Lean_Meta_TransparencyMode_Lean_Meta_TransparencyMode___instance__2;
uint8_t l_Lean_Meta_TransparencyMode_beq(uint8_t, uint8_t);
lean_object* l_Lean_Meta_TransparencyMode_HasBeq;
lean_object* l_Lean_Meta_TransparencyMode_Lean_Meta_TransparencyMode___instance__2___closed__1;
lean_object* l_Lean_Meta_TransparencyMode_Lean_Meta_TransparencyMode___instance__3___closed__1;
lean_object* l_Lean_Meta_TransparencyMode_hash_match__1___rarg(uint8_t, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_TransparencyMode_beq___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Meta_TransparencyMode_lt_match__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_Meta_TransparencyMode_lt(uint8_t, uint8_t);
uint8_t l_Lean_Meta_TransparencyMode_Lean_Meta_TransparencyMode___instance__1;
lean_object* l_Lean_Meta_TransparencyMode_Lean_Meta_TransparencyMode___instance__3;
lean_object* l_Lean_Meta_TransparencyMode_hash_match__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_TransparencyMode_lt_match__1(lean_object*);
lean_object* l_Lean_Meta_TransparencyMode_hash___boxed(lean_object*);
static uint8_t _init_l_Lean_Meta_TransparencyMode_Inhabited() {
lean_object* l_Lean_Meta_TransparencyMode_lt_match__1___rarg(uint8_t, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*);
static uint8_t _init_l_Lean_Meta_TransparencyMode_Lean_Meta_TransparencyMode___instance__1() {
_start:
{
uint8_t x_1;
@ -32,6 +41,108 @@ x_1 = 1;
return x_1;
}
}
lean_object* l_Lean_Meta_TransparencyMode_beq_match__1___rarg(uint8_t x_1, uint8_t x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
_start:
{
switch (x_1) {
case 0:
{
lean_object* x_7;
lean_dec(x_5);
lean_dec(x_4);
x_7 = lean_box(x_2);
if (lean_obj_tag(x_7) == 0)
{
lean_object* x_8; lean_object* x_9;
lean_dec(x_6);
x_8 = lean_box(0);
x_9 = lean_apply_1(x_3, x_8);
return x_9;
}
else
{
lean_object* x_10; lean_object* x_11; lean_object* x_12;
lean_dec(x_7);
lean_dec(x_3);
x_10 = lean_box(x_1);
x_11 = lean_box(x_2);
x_12 = lean_apply_2(x_6, x_10, x_11);
return x_12;
}
}
case 1:
{
lean_object* x_13;
lean_dec(x_5);
lean_dec(x_3);
x_13 = lean_box(x_2);
if (lean_obj_tag(x_13) == 1)
{
lean_object* x_14; lean_object* x_15;
lean_dec(x_6);
x_14 = lean_box(0);
x_15 = lean_apply_1(x_4, x_14);
return x_15;
}
else
{
lean_object* x_16; lean_object* x_17; lean_object* x_18;
lean_dec(x_13);
lean_dec(x_4);
x_16 = lean_box(x_1);
x_17 = lean_box(x_2);
x_18 = lean_apply_2(x_6, x_16, x_17);
return x_18;
}
}
default:
{
lean_object* x_19;
lean_dec(x_4);
lean_dec(x_3);
x_19 = lean_box(x_2);
if (lean_obj_tag(x_19) == 2)
{
lean_object* x_20; lean_object* x_21;
lean_dec(x_6);
x_20 = lean_box(0);
x_21 = lean_apply_1(x_5, x_20);
return x_21;
}
else
{
lean_object* x_22; lean_object* x_23; lean_object* x_24;
lean_dec(x_19);
lean_dec(x_5);
x_22 = lean_box(x_1);
x_23 = lean_box(x_2);
x_24 = lean_apply_2(x_6, x_22, x_23);
return x_24;
}
}
}
}
}
lean_object* l_Lean_Meta_TransparencyMode_beq_match__1(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_Lean_Meta_TransparencyMode_beq_match__1___rarg___boxed), 6, 0);
return x_2;
}
}
lean_object* l_Lean_Meta_TransparencyMode_beq_match__1___rarg___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:
{
uint8_t x_7; uint8_t x_8; lean_object* x_9;
x_7 = lean_unbox(x_1);
lean_dec(x_1);
x_8 = lean_unbox(x_2);
lean_dec(x_2);
x_9 = l_Lean_Meta_TransparencyMode_beq_match__1___rarg(x_7, x_8, x_3, x_4, x_5, x_6);
return x_9;
}
}
uint8_t l_Lean_Meta_TransparencyMode_beq(uint8_t x_1, uint8_t x_2) {
_start:
{
@ -106,7 +217,7 @@ x_6 = lean_box(x_5);
return x_6;
}
}
static lean_object* _init_l_Lean_Meta_TransparencyMode_HasBeq___closed__1() {
static lean_object* _init_l_Lean_Meta_TransparencyMode_Lean_Meta_TransparencyMode___instance__2___closed__1() {
_start:
{
lean_object* x_1;
@ -114,14 +225,66 @@ x_1 = lean_alloc_closure((void*)(l_Lean_Meta_TransparencyMode_beq___boxed), 2, 0
return x_1;
}
}
static lean_object* _init_l_Lean_Meta_TransparencyMode_HasBeq() {
static lean_object* _init_l_Lean_Meta_TransparencyMode_Lean_Meta_TransparencyMode___instance__2() {
_start:
{
lean_object* x_1;
x_1 = l_Lean_Meta_TransparencyMode_HasBeq___closed__1;
x_1 = l_Lean_Meta_TransparencyMode_Lean_Meta_TransparencyMode___instance__2___closed__1;
return x_1;
}
}
lean_object* l_Lean_Meta_TransparencyMode_hash_match__1___rarg(uint8_t x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
switch (x_1) {
case 0:
{
lean_object* x_5; lean_object* x_6;
lean_dec(x_4);
lean_dec(x_3);
x_5 = lean_box(0);
x_6 = lean_apply_1(x_2, x_5);
return x_6;
}
case 1:
{
lean_object* x_7; lean_object* x_8;
lean_dec(x_4);
lean_dec(x_2);
x_7 = lean_box(0);
x_8 = lean_apply_1(x_3, x_7);
return x_8;
}
default:
{
lean_object* x_9; lean_object* x_10;
lean_dec(x_3);
lean_dec(x_2);
x_9 = lean_box(0);
x_10 = lean_apply_1(x_4, x_9);
return x_10;
}
}
}
}
lean_object* l_Lean_Meta_TransparencyMode_hash_match__1(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_Lean_Meta_TransparencyMode_hash_match__1___rarg___boxed), 4, 0);
return x_2;
}
}
lean_object* l_Lean_Meta_TransparencyMode_hash_match__1___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
uint8_t x_5; lean_object* x_6;
x_5 = lean_unbox(x_1);
lean_dec(x_1);
x_6 = l_Lean_Meta_TransparencyMode_hash_match__1___rarg(x_5, x_2, x_3, x_4);
return x_6;
}
}
size_t l_Lean_Meta_TransparencyMode_hash(uint8_t x_1) {
_start:
{
@ -158,7 +321,7 @@ x_4 = lean_box_usize(x_3);
return x_4;
}
}
static lean_object* _init_l_Lean_Meta_TransparencyMode_Hashable___closed__1() {
static lean_object* _init_l_Lean_Meta_TransparencyMode_Lean_Meta_TransparencyMode___instance__3___closed__1() {
_start:
{
lean_object* x_1;
@ -166,14 +329,119 @@ x_1 = lean_alloc_closure((void*)(l_Lean_Meta_TransparencyMode_hash___boxed), 1,
return x_1;
}
}
static lean_object* _init_l_Lean_Meta_TransparencyMode_Hashable() {
static lean_object* _init_l_Lean_Meta_TransparencyMode_Lean_Meta_TransparencyMode___instance__3() {
_start:
{
lean_object* x_1;
x_1 = l_Lean_Meta_TransparencyMode_Hashable___closed__1;
x_1 = l_Lean_Meta_TransparencyMode_Lean_Meta_TransparencyMode___instance__3___closed__1;
return x_1;
}
}
lean_object* l_Lean_Meta_TransparencyMode_lt_match__1___rarg(uint8_t x_1, uint8_t x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
_start:
{
switch (x_1) {
case 0:
{
lean_object* x_7; lean_object* x_8; lean_object* x_9;
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
x_7 = lean_box(x_1);
x_8 = lean_box(x_2);
x_9 = lean_apply_2(x_6, x_7, x_8);
return x_9;
}
case 1:
{
lean_dec(x_4);
lean_dec(x_3);
switch (x_2) {
case 0:
{
lean_object* x_10; lean_object* x_11;
lean_dec(x_6);
x_10 = lean_box(0);
x_11 = lean_apply_1(x_5, x_10);
return x_11;
}
case 1:
{
lean_object* x_12; lean_object* x_13; lean_object* x_14;
lean_dec(x_5);
x_12 = lean_box(x_2);
x_13 = lean_box(x_2);
x_14 = lean_apply_2(x_6, x_12, x_13);
return x_14;
}
default:
{
lean_object* x_15; lean_object* x_16; lean_object* x_17;
lean_dec(x_5);
x_15 = lean_box(x_1);
x_16 = lean_box(x_2);
x_17 = lean_apply_2(x_6, x_15, x_16);
return x_17;
}
}
}
default:
{
lean_dec(x_5);
switch (x_2) {
case 0:
{
lean_object* x_18; lean_object* x_19;
lean_dec(x_6);
lean_dec(x_3);
x_18 = lean_box(0);
x_19 = lean_apply_1(x_4, x_18);
return x_19;
}
case 1:
{
lean_object* x_20; lean_object* x_21;
lean_dec(x_6);
lean_dec(x_4);
x_20 = lean_box(0);
x_21 = lean_apply_1(x_3, x_20);
return x_21;
}
default:
{
lean_object* x_22; lean_object* x_23; lean_object* x_24;
lean_dec(x_4);
lean_dec(x_3);
x_22 = lean_box(x_2);
x_23 = lean_box(x_2);
x_24 = lean_apply_2(x_6, x_22, x_23);
return x_24;
}
}
}
}
}
}
lean_object* l_Lean_Meta_TransparencyMode_lt_match__1(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_Lean_Meta_TransparencyMode_lt_match__1___rarg___boxed), 6, 0);
return x_2;
}
}
lean_object* l_Lean_Meta_TransparencyMode_lt_match__1___rarg___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:
{
uint8_t x_7; uint8_t x_8; lean_object* x_9;
x_7 = lean_unbox(x_1);
lean_dec(x_1);
x_8 = lean_unbox(x_2);
lean_dec(x_2);
x_9 = l_Lean_Meta_TransparencyMode_lt_match__1___rarg(x_7, x_8, x_3, x_4, x_5, x_6);
return x_9;
}
}
uint8_t l_Lean_Meta_TransparencyMode_lt(uint8_t x_1, uint8_t x_2) {
_start:
{
@ -245,15 +513,15 @@ _G_initialized = true;
res = initialize_Init(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_Lean_Meta_TransparencyMode_Inhabited = _init_l_Lean_Meta_TransparencyMode_Inhabited();
l_Lean_Meta_TransparencyMode_HasBeq___closed__1 = _init_l_Lean_Meta_TransparencyMode_HasBeq___closed__1();
lean_mark_persistent(l_Lean_Meta_TransparencyMode_HasBeq___closed__1);
l_Lean_Meta_TransparencyMode_HasBeq = _init_l_Lean_Meta_TransparencyMode_HasBeq();
lean_mark_persistent(l_Lean_Meta_TransparencyMode_HasBeq);
l_Lean_Meta_TransparencyMode_Hashable___closed__1 = _init_l_Lean_Meta_TransparencyMode_Hashable___closed__1();
lean_mark_persistent(l_Lean_Meta_TransparencyMode_Hashable___closed__1);
l_Lean_Meta_TransparencyMode_Hashable = _init_l_Lean_Meta_TransparencyMode_Hashable();
lean_mark_persistent(l_Lean_Meta_TransparencyMode_Hashable);
l_Lean_Meta_TransparencyMode_Lean_Meta_TransparencyMode___instance__1 = _init_l_Lean_Meta_TransparencyMode_Lean_Meta_TransparencyMode___instance__1();
l_Lean_Meta_TransparencyMode_Lean_Meta_TransparencyMode___instance__2___closed__1 = _init_l_Lean_Meta_TransparencyMode_Lean_Meta_TransparencyMode___instance__2___closed__1();
lean_mark_persistent(l_Lean_Meta_TransparencyMode_Lean_Meta_TransparencyMode___instance__2___closed__1);
l_Lean_Meta_TransparencyMode_Lean_Meta_TransparencyMode___instance__2 = _init_l_Lean_Meta_TransparencyMode_Lean_Meta_TransparencyMode___instance__2();
lean_mark_persistent(l_Lean_Meta_TransparencyMode_Lean_Meta_TransparencyMode___instance__2);
l_Lean_Meta_TransparencyMode_Lean_Meta_TransparencyMode___instance__3___closed__1 = _init_l_Lean_Meta_TransparencyMode_Lean_Meta_TransparencyMode___instance__3___closed__1();
lean_mark_persistent(l_Lean_Meta_TransparencyMode_Lean_Meta_TransparencyMode___instance__3___closed__1);
l_Lean_Meta_TransparencyMode_Lean_Meta_TransparencyMode___instance__3 = _init_l_Lean_Meta_TransparencyMode_Lean_Meta_TransparencyMode___instance__3();
lean_mark_persistent(l_Lean_Meta_TransparencyMode_Lean_Meta_TransparencyMode___instance__3);
return lean_io_result_mk_ok(lean_box(0));
}
#ifdef __cplusplus