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-08-17 06:29:24 -07:00
parent 5d945dba2d
commit ae2e00ae96
15 changed files with 23667 additions and 17536 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -44,7 +44,7 @@ pure $ namedArgs.push namedArg
def synthesizeAppInstMVars (instMVars : Array MVarId) : TermElabM Unit :=
instMVars.forM $ fun mvarId =>
unlessM (synthesizeInstMVarCore mvarId) $
registerSyntheticMVar mvarId SyntheticMVarKind.typeClass
registerSyntheticMVarWithCurrRef mvarId SyntheticMVarKind.typeClass
private def ensureArgType (f : Expr) (arg : Expr) (expectedType : Expr) : TermElabM Expr := do
argType ← inferType arg;

43
stage0/src/Lean/Elab/Binders.lean generated
View file

@ -218,21 +218,25 @@ private partial def getFunBinderIdsAux? : Bool → Syntax → Array Syntax → T
private def getFunBinderIds? (stx : Syntax) : TermElabM (Option (Array Syntax)) :=
getFunBinderIdsAux? false stx #[]
/-- Main loop for `expandFunBinders`. -/
private partial def expandFunBindersAux (binders : Array Syntax) : Syntax → Nat → Array Syntax → TermElabM (Array Syntax × Syntax)
/--
Main loop for `expandFunBinders`.
The resulting `Bool` is true if a pattern was found. We use it to "mark" a macro expansion. -/
private partial def expandFunBindersAux (binders : Array Syntax) : Syntax → Nat → Array Syntax → TermElabM (Array Syntax × Syntax × Bool)
| body, i, newBinders =>
if h : i < binders.size then
let binder := binders.get ⟨i, h⟩;
let processAsPattern : Unit → TermElabM (Array Syntax × Syntax) := fun _ => do {
let processAsPattern : Unit → TermElabM (Array Syntax × Syntax × Bool) := fun _ => do {
let pattern := binder;
major ← mkFreshAnonymousIdent binder;
(binders, newBody) ← expandFunBindersAux body (i+1) (newBinders.push $ mkExplicitBinder major (mkHole binder));
(binders, newBody, _) ← expandFunBindersAux body (i+1) (newBinders.push $ mkExplicitBinder major (mkHole binder));
newBody ← `(match $major:ident with | $pattern => $newBody);
pure (binders, newBody)
pure (binders, newBody, true)
};
match binder with
| Syntax.node `Lean.Parser.Term.implicitBinder _ => expandFunBindersAux body (i+1) (newBinders.push binder)
| Syntax.node `Lean.Parser.Term.instBinder _ => expandFunBindersAux body (i+1) (newBinders.push binder)
| Syntax.node `Lean.Parser.Term.explicitBinder _ => expandFunBindersAux body (i+1) (newBinders.push binder)
| Syntax.node `Lean.Parser.Term.hole _ => do
ident ← mkFreshAnonymousIdent binder;
let type := binder;
@ -262,7 +266,7 @@ private partial def expandFunBindersAux (binders : Array Syntax) : Syntax → Na
expandFunBindersAux body (i+1) (newBinders.push $ mkExplicitBinder ident type)
| none => processAsPattern ()
else
pure (newBinders, body)
pure (newBinders, body, false)
/--
Auxiliary function for expanding `fun` notation binders. Recall that `fun` parser is defined as
@ -278,8 +282,10 @@ private partial def expandFunBindersAux (binders : Array Syntax) : Syntax → Na
which can be elaborated using `elabBinders`, and `newBody` is the updated `body` syntax.
We update the `body` syntax when expanding the pattern notation.
Example: `fun (a, b) => a + b` expands into `fun _a_1 => match _a_1 with | (a, b) => a + b`.
See local function `processAsPattern` at `expandFunBindersAux`. -/
def expandFunBinders (binders : Array Syntax) (body : Syntax) : TermElabM (Array Syntax × Syntax) :=
See local function `processAsPattern` at `expandFunBindersAux`.
The resulting `Bool` is true if a pattern was found. We use it "mark" a macro expansion. -/
def expandFunBinders (binders : Array Syntax) (body : Syntax) : TermElabM (Array Syntax × Syntax × Bool) :=
expandFunBindersAux binders body 0 #[]
namespace FunBinders
@ -364,11 +370,14 @@ fun stx expectedType? => do
-- `fun` term+ `=>` term
let binders := (stx.getArg 1).getArgs;
let body := stx.getArg 3;
(binders, body) ← expandFunBinders binders body;
elabFunBinders binders expectedType? $ fun xs expectedType? => do {
e ← elabTerm body expectedType?;
mkLambda xs e
}
(binders, body, expandedPattern) ← expandFunBinders binders body;
if expandedPattern then do
newStx ← `(fun $binders* => $body);
withMacroExpansion stx newStx $ elabTerm newStx expectedType?
else
elabFunBinders binders expectedType? $ fun xs expectedType? => do
e ← elabTerm body expectedType?;
mkLambda xs e
/-
Recall that
@ -413,6 +422,10 @@ fun stx expectedType? => match_syntax stx with
elabLetDeclAux id.getId args (mkHole stx) val body expectedType? true
| `(let $id:ident $args* : $type := $val; $body) =>
elabLetDeclAux id.getId args type val body expectedType? true
| `(let $id:ident $args* | $alts:matchAlt*; $body) =>
throwError "invalid let-expression with pattern matching, type must be provided"
| `(let $id:ident $args* : $type | $alts:matchAlt*; $body) =>
throwError "WIP" -- TODO
| `(let $pat:term := $val; $body) => do
stxNew ← `(let x := $val; match x with $pat => $body);
withMacroExpansion stx stxNew $ elabTerm stxNew expectedType?
@ -427,6 +440,10 @@ fun stx expectedType? => match_syntax stx with
elabLetDeclAux id.getId args (mkHole stx) val body expectedType? false
| `(let! $id:ident $args* : $type := $val; $body) =>
elabLetDeclAux id.getId args type val body expectedType? false
| `(let! $id:ident $args* | $alts:matchAlt*; $body) =>
throwError "invalid let-expression with pattern matching, type must be provided"
| `(let! $id:ident $args* : $type | $alts:matchAlt*; $body) =>
throwError "WIP" -- TODO
| `(let! $pat:term := $val; $body) => do
stxNew ← `(let! x := $val; match x with $pat => $body);
withMacroExpansion stx stxNew $ elabTerm stxNew expectedType?

54
stage0/src/Lean/Elab/Match.lean generated
View file

@ -55,8 +55,9 @@ if optType.isNone then
else
pure $ (optType.getArg 0).getArg 1
private def elabMatchOptType (matchStx : Syntax) (numDiscrs : Nat) : TermElabM Expr := do
typeStx ← liftMacroM $ expandMatchOptType matchStx (matchStx.getArg 2) numDiscrs;
private def elabMatchOptType (matchOptType : Syntax) (numDiscrs : Nat) : TermElabM Expr := do
ref ← getRef;
typeStx ← liftMacroM $ expandMatchOptType ref matchOptType numDiscrs;
elabType typeStx
private partial def elabDiscrsAux (discrStxs : Array Syntax) (expectedType : Expr) : Nat → Expr → Array Expr → TermElabM (Array Expr)
@ -254,8 +255,8 @@ private partial def collect : Syntax → M Syntax
let fields := (args.get! 2).getArgs;
fields ← fields.mapSepElemsM fun field => do {
-- parser! structInstLVal >> " := " >> termParser
newVal ← collect (field.getArg 2);
pure $ field.setArg 2 newVal
newVal ← collect (field.getArg 3); -- `structInstLVal` has arity 2
pure $ field.setArg 3 newVal
};
pure $ Syntax.node k $ args.set! 2 $ mkNullNode fields
else if k == `Lean.Parser.Term.hole then do
@ -535,20 +536,10 @@ unless result.counterExamples.isEmpty $
unless result.unusedAltIdxs.isEmpty $
throwError ("unused alternatives: " ++ toString (result.unusedAltIdxs.map fun idx => "#" ++ toString (idx+1)))
/-
```
parser!:leadPrec "match " >> sepBy1 matchDiscr ", " >> optType >> " with " >> matchAlts
```
Remark the `optIdent` must be `none` at `matchDiscr`. They are expanded by `expandMatchDiscr?`.
-/
private def elabMatchCore (stx : Syntax) (expectedType? : Option Expr) : TermElabM Expr := do
tryPostponeIfNoneOrMVar expectedType?;
expectedType ← match expectedType? with
| some expectedType => pure expectedType
| none => mkFreshTypeMVar;
let discrStxs := (stx.getArg 1).getArgs.getSepElems.map fun d => d.getArg 1;
matchType ← elabMatchOptType stx discrStxs.size;
matchAlts ← expandMacrosInPatterns $ getMatchAlts stx;
private def elabMatchAux (discrStxs : Array Syntax) (altViews : Array MatchAltView) (matchOptType : Syntax) (expectedType : Expr)
: TermElabM Expr := do
matchType ← elabMatchOptType matchOptType discrStxs.size;
matchAlts ← expandMacrosInPatterns altViews;
discrs ← elabDiscrs discrStxs matchType expectedType;
trace `Elab.match fun _ => "matchType: " ++ matchType;
alts ← matchAlts.mapM $ fun alt => elabMatchAltView alt matchType;
@ -565,6 +556,25 @@ let r := mkAppN r rhss;
trace `Elab.match fun _ => "result: " ++ r;
pure r
private def waitExpectedType (expectedType? : Option Expr) : TermElabM Expr := do
tryPostponeIfNoneOrMVar expectedType?;
match expectedType? with
| some expectedType => pure expectedType
| none => mkFreshTypeMVar
/-
```
parser!:leadPrec "match " >> sepBy1 matchDiscr ", " >> optType >> " with " >> matchAlts
```
Remark the `optIdent` must be `none` at `matchDiscr`. They are expanded by `expandMatchDiscr?`.
-/
private def elabMatchCore (stx : Syntax) (expectedType? : Option Expr) : TermElabM Expr := do
expectedType ← waitExpectedType expectedType?;
let discrStxs := (stx.getArg 1).getArgs.getSepElems.map fun d => d.getArg 1;
let altViews := getMatchAlts stx;
let matchOptType := stx.getArg 2;
elabMatchAux discrStxs altViews matchOptType expectedType
/- Auxiliary method for `expandMatchDiscr?` -/
private partial def mkMatchType (discrs : Array Syntax) : Nat → MacroM Syntax
| i => withFreshMacroScope $
@ -673,6 +683,14 @@ fun stx expectedType? => match_syntax stx with
registerTraceClass `Elab.match;
pure ()
-- parser!:leadPrec "nomatch " >> termParser
@[builtinTermElab «nomatch»] def elabNoMatch : TermElab :=
fun stx expectedType? => match_syntax stx with
| `(nomatch $discr) => do
expectedType ← waitExpectedType expectedType?;
elabMatchAux #[discr] #[] mkNullNode expectedType
| _ => throwUnsupportedSyntax
end Term
end Elab
end Lean

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

@ -92,13 +92,13 @@ pure $ !val.getAppFn.isMVar
/-- Try to synthesize the given pending synthetic metavariable. -/
private def synthesizeSyntheticMVar (mvarSyntheticDecl : SyntheticMVarDecl) (postponeOnError : Bool) (runTactics : Bool) : TermElabM Bool :=
withRef mvarSyntheticDecl.ref $
withRef mvarSyntheticDecl.stx $
match mvarSyntheticDecl.kind with
| SyntheticMVarKind.typeClass => synthesizePendingInstMVar mvarSyntheticDecl.mvarId
| SyntheticMVarKind.coe expectedType eType e f? => synthesizePendingCoeInstMVar mvarSyntheticDecl.mvarId expectedType eType e f?
-- NOTE: actual processing at `synthesizeSyntheticMVarsAux`
| SyntheticMVarKind.withDefault _ => checkWithDefault mvarSyntheticDecl.mvarId
| SyntheticMVarKind.postponed macroStack => resumePostponed macroStack mvarSyntheticDecl.ref mvarSyntheticDecl.mvarId postponeOnError
| SyntheticMVarKind.postponed macroStack => resumePostponed macroStack mvarSyntheticDecl.stx mvarSyntheticDecl.mvarId postponeOnError
| SyntheticMVarKind.tactic tacticCode =>
if runTactics then do
runTactic mvarSyntheticDecl.mvarId tacticCode;
@ -136,7 +136,7 @@ private def synthesizeUsingDefault : TermElabM Bool := do
s ← get;
let len := s.syntheticMVars.length;
newSyntheticMVars ← s.syntheticMVars.filterM $ fun mvarDecl =>
withRef mvarDecl.ref $
withRef mvarDecl.stx $
match mvarDecl.kind with
| SyntheticMVarKind.withDefault defaultVal => withMVarContext mvarDecl.mvarId $ do
val ← instantiateMVars (mkMVar mvarDecl.mvarId);
@ -152,7 +152,7 @@ pure $ newSyntheticMVars.length != len
private def reportStuckSyntheticMVars : TermElabM Unit := do
s ← get;
s.syntheticMVars.forM $ fun mvarSyntheticDecl =>
withRef mvarSyntheticDecl.ref $
withRef mvarSyntheticDecl.stx $
match mvarSyntheticDecl.kind with
| SyntheticMVarKind.typeClass =>
withMVarContext mvarSyntheticDecl.mvarId $ do
@ -166,8 +166,8 @@ s.syntheticMVars.forM $ fun mvarSyntheticDecl =>
private def getSomeSynthethicMVarsRef : TermElabM Syntax := do
s ← get;
match s.syntheticMVars.find? $ fun (mvarDecl : SyntheticMVarDecl) => !mvarDecl.ref.getPos.isNone with
| some mvarDecl => pure mvarDecl.ref
match s.syntheticMVars.find? $ fun (mvarDecl : SyntheticMVarDecl) => !mvarDecl.stx.getPos.isNone with
| some mvarDecl => pure mvarDecl.stx
| none => pure Syntax.missing
/--

21
stage0/src/Lean/Elab/Term.lean generated
View file

@ -60,7 +60,7 @@ inductive SyntheticMVarKind
| withDefault (defaultVal : Expr)
structure SyntheticMVarDecl :=
(mvarId : MVarId) (ref : Syntax) (kind : SyntheticMVarKind)
(mvarId : MVarId) (stx : Syntax) (kind : SyntheticMVarKind)
structure State extends Meta.State :=
(syntheticMVars : List SyntheticMVarDecl := [])
@ -347,9 +347,12 @@ adaptReader (fun (ctx : Context) => { ctx with macroStack := { before := beforeS
/-
Add the given metavariable to the list of pending synthetic metavariables.
The method `synthesizeSyntheticMVars` is used to process the metavariables on this list. -/
def registerSyntheticMVar (mvarId : MVarId) (kind : SyntheticMVarKind) : TermElabM Unit := do
ref ← getRef;
modify $ fun s => { s with syntheticMVars := { mvarId := mvarId, ref := ref, kind := kind } :: s.syntheticMVars }
def registerSyntheticMVar (stx : Syntax) (mvarId : MVarId) (kind : SyntheticMVarKind) : TermElabM Unit := do
modify $ fun s => { s with syntheticMVars := { mvarId := mvarId, stx := stx, kind := kind } :: s.syntheticMVars }
def registerSyntheticMVarWithCurrRef (mvarId : MVarId) (kind : SyntheticMVarKind) : TermElabM Unit := do
ctx ← read;
registerSyntheticMVar ctx.ref mvarId kind
/-
Execute `x` without allowing it to postpone elaboration tasks.
@ -535,7 +538,7 @@ let mvarId := mvar.mvarId!;
catch
(withoutMacroStackAtErr $ do
unlessM (synthesizeInstMVarCore mvarId) $
registerSyntheticMVar mvarId (SyntheticMVarKind.coe expectedType eType e f?);
registerSyntheticMVarWithCurrRef mvarId (SyntheticMVarKind.coe expectedType eType e f?);
pure eNew)
(fun ex =>
match ex with
@ -765,7 +768,7 @@ private def postponeElabTerm (stx : Syntax) (expectedType? : Option Expr) : Term
trace `Elab.postpone $ fun _ => stx ++ " : " ++ expectedType?;
mvar ← mkFreshExprMVar expectedType? MetavarKind.syntheticOpaque;
ctx ← read;
withRef stx $ registerSyntheticMVar mvar.mvarId! (SyntheticMVarKind.postponed ctx.macroStack);
registerSyntheticMVar stx mvar.mvarId! (SyntheticMVarKind.postponed ctx.macroStack);
pure mvar
/-
@ -961,7 +964,7 @@ def mkInstMVar (type : Expr) : TermElabM Expr := do
mvar ← mkFreshExprMVar type MetavarKind.synthetic;
let mvarId := mvar.mvarId!;
unlessM (synthesizeInstMVarCore mvarId) $
registerSyntheticMVar mvarId SyntheticMVarKind.typeClass;
registerSyntheticMVarWithCurrRef mvarId SyntheticMVarKind.typeClass;
pure mvar
/-
@ -1079,7 +1082,7 @@ fun stx expectedType? =>
def mkTacticMVar (type : Expr) (tacticCode : Syntax) : TermElabM Expr := do
mvar ← mkFreshExprMVar type MetavarKind.syntheticOpaque `main;
let mvarId := mvar.mvarId!;
registerSyntheticMVar mvarId $ SyntheticMVarKind.tactic tacticCode;
registerSyntheticMVar tacticCode mvarId $ SyntheticMVarKind.tactic tacticCode;
pure mvar
@[builtinTermElab tacticBlock] def elabTacticBlock : TermElab :=
@ -1254,7 +1257,7 @@ fun stx expectedType? => do
| some val => pure (mkNatLit val)
| none => throwError "ill-formed syntax";
typeMVar ← mkFreshTypeMVar MetavarKind.synthetic;
registerSyntheticMVar typeMVar.mvarId! (SyntheticMVarKind.withDefault (Lean.mkConst `Nat));
registerSyntheticMVar stx typeMVar.mvarId! (SyntheticMVarKind.withDefault (Lean.mkConst `Nat));
match expectedType? with
| some expectedType => do _ ← isDefEq expectedType typeMVar; pure ()
| _ => pure ();

125
stage0/src/Lean/Meta/EqnCompiler/DepElim.lean generated
View file

@ -273,7 +273,7 @@ p.alts.all fun alt => match alt.patterns with
| _ => false
private def isConstructorTransition (p : Problem) : Bool :=
hasCtorPattern p
(hasCtorPattern p || p.alts.isEmpty)
&& p.alts.all fun alt => match alt.patterns with
| Pattern.ctor _ _ _ _ :: _ => true
| Pattern.var _ :: _ => true
@ -437,46 +437,80 @@ withExistingLocalDecls alt.fvarDecls do
| e => Pattern.inaccessible e;
pure $ some { alt with fvarDecls := newAltDecls, rhs := rhs, patterns := ctorFieldPatterns ++ patterns }
private def getInductiveVal? (x : Expr) : MetaM (Option InductiveVal) := do
xType ← inferType x;
xType ← whnfD xType;
match xType.getAppFn with
| Expr.const constName _ _ => do
cinfo ← getConstInfo constName;
match cinfo with
| ConstantInfo.inductInfo val => pure (some val)
| _ => pure none
| _ => pure none
private def hasRecursiveType (x : Expr) : MetaM Bool := do
val? ← getInductiveVal? x;
match val? with
| some val => pure val.isRec
| _ => pure false
private def processConstructor (p : Problem) : MetaM (Array Problem) := do
trace! `Meta.EqnCompiler.match ("constructor step");
env ← getEnv;
match p.vars with
| [] => unreachable!
| x :: xs => do
subgoals ← cases p.mvarId x.fvarId!;
subgoals.mapM fun subgoal => withMVarContext subgoal.mvarId do
let subst := subgoal.subst;
let fields := subgoal.fields.toList;
let newVars := fields ++ xs;
let newVars := newVars.map fun x => x.applyFVarSubst subst;
let subex := Example.ctor subgoal.ctorName $ fields.map fun field => match field with
| Expr.fvar fvarId _ => Example.var fvarId
| _ => Example.underscore; -- This case can happen due to dependent elimination
let examples := p.examples.map $ Example.replaceFVarId x.fvarId! subex;
let examples := examples.map $ Example.applyFVarSubst subst;
let newAlts := p.alts.filter fun alt => match alt.patterns with
| Pattern.ctor n _ _ _ :: _ => n == subgoal.ctorName
| Pattern.var _ :: _ => true
| Pattern.inaccessible _ :: _ => true
| _ => false;
let newAlts := newAlts.map fun alt => alt.applyFVarSubst subst;
newAlts ← newAlts.filterMapM fun alt => match alt.patterns with
| Pattern.ctor _ _ _ fields :: ps => pure $ some { alt with patterns := fields ++ ps }
| Pattern.var fvarId :: ps => expandVarIntoCtor? { alt with patterns := ps } fvarId subgoal.ctorName
| Pattern.inaccessible e :: ps => do
trace! `Meta.EqnCompiler.match ("inaccessible in ctor step " ++ e);
e ← whnfD e;
match e.constructorApp? env with
| some (ctorVal, ctorArgs) => do
if ctorVal.name == subgoal.ctorName then
let fields := ctorArgs.extract ctorVal.nparams ctorArgs.size;
let fields := fields.toList.map Pattern.inaccessible;
pure $ some { alt with patterns := fields ++ ps }
else
pure none
| _ => pure none
| _ => unreachable!;
pure { mvarId := subgoal.mvarId, vars := newVars, alts := newAlts, examples := examples }
subgoals? ← commitWhenSome? do {
subgoals ← cases p.mvarId x.fvarId!;
if subgoals.isEmpty then
/- Easy case: we have solved problem `p` since there are no subgoals -/
pure (some #[])
else if !p.alts.isEmpty then
pure (some subgoals)
else do
isRec ← withGoalOf p $ hasRecursiveType x;
/- If there are no alternatives and the type of the current variable is recursive, we do NOT consider
a constructor-transition to avoid nontermination.
TODO: implement a more general approach if this is not sufficient in practice -/
if isRec then pure none
else pure (some subgoals)
};
match subgoals? with
| none => pure #[{ p with vars := xs }]
| some subgoals =>
subgoals.mapM fun subgoal => withMVarContext subgoal.mvarId do
let subst := subgoal.subst;
let fields := subgoal.fields.toList;
let newVars := fields ++ xs;
let newVars := newVars.map fun x => x.applyFVarSubst subst;
let subex := Example.ctor subgoal.ctorName $ fields.map fun field => match field with
| Expr.fvar fvarId _ => Example.var fvarId
| _ => Example.underscore; -- This case can happen due to dependent elimination
let examples := p.examples.map $ Example.replaceFVarId x.fvarId! subex;
let examples := examples.map $ Example.applyFVarSubst subst;
let newAlts := p.alts.filter fun alt => match alt.patterns with
| Pattern.ctor n _ _ _ :: _ => n == subgoal.ctorName
| Pattern.var _ :: _ => true
| Pattern.inaccessible _ :: _ => true
| _ => false;
let newAlts := newAlts.map fun alt => alt.applyFVarSubst subst;
newAlts ← newAlts.filterMapM fun alt => match alt.patterns with
| Pattern.ctor _ _ _ fields :: ps => pure $ some { alt with patterns := fields ++ ps }
| Pattern.var fvarId :: ps => expandVarIntoCtor? { alt with patterns := ps } fvarId subgoal.ctorName
| Pattern.inaccessible e :: ps => do
trace! `Meta.EqnCompiler.match ("inaccessible in ctor step " ++ e);
e ← whnfD e;
match e.constructorApp? env with
| some (ctorVal, ctorArgs) => do
if ctorVal.name == subgoal.ctorName then
let fields := ctorArgs.extract ctorVal.nparams ctorArgs.size;
let fields := fields.toList.map Pattern.inaccessible;
pure $ some { alt with patterns := fields ++ ps }
else
pure none
| _ => pure none
| _ => unreachable!;
pure { mvarId := subgoal.mvarId, vars := newVars, alts := newAlts, examples := examples }
private def collectValues (p : Problem) : Array Expr :=
p.alts.foldl
@ -596,9 +630,22 @@ private def throwNonSupported (p : Problem) : MetaM Unit := do
msg ← p.toMessageData;
throwOther ("not implement yet " ++ msg)
@[inline] def withIncRecDepth {α} (x : StateT State MetaM α) : StateT State MetaM α := do
ctx ← read;
when (ctx.currRecDepth == ctx.maxRecDepth) $ liftM $ throwOther maxRecDepthErrorMessage;
adaptReader (fun (ctx : Context) => { ctx with currRecDepth := ctx.currRecDepth + 1 }) x
def isCurrVarInductive (p : Problem) : MetaM Bool := do
match p.vars with
| [] => pure false
| x::_ => withGoalOf p do
val? ← getInductiveVal? x;
pure val?.isSome
private partial def process : Problem → StateT State MetaM Unit
| p => do
| p => withIncRecDepth do
liftM $ traceState p;
isInductive ← liftM $ isCurrVarInductive p;
if isDone p then
processLeaf p
else if hasAsPattern p then do
@ -607,12 +654,12 @@ private partial def process : Problem → StateT State MetaM Unit
else if !isNextVar p then do
traceStep ("non variable");
process (processNonVariable p)
else if isInductive && isConstructorTransition p then do
ps ← liftM $ processConstructor p;
ps.forM process
else if isVariableTransition p then do
traceStep ("variable");
process (processVariable p)
else if isConstructorTransition p then do
ps ← liftM $ processConstructor p;
ps.forM process
else if isValueTransition p then do
ps ← liftM $ processValue p;
ps.forM process

26
stage0/src/Lean/Meta/LevelDefEq.lean generated
View file

@ -194,25 +194,35 @@ def restore (env : Environment) (mctx : MetavarContext) (postponed : PersistentA
modify $ fun s => { s with env := env, mctx := mctx, postponed := postponed }
/--
`commitWhen x` executes `x` and process all postponed universe level constraints produced by `x`.
We keep the modifications only if both return `true`.
`commitWhenSome? x` executes `x` and process all postponed universe level constraints produced by `x`.
We keep the modifications only if `processPostponed` return true and `x` returned `some a`.
Remark: postponed universe level constraints must be solved before returning. Otherwise,
we don't know whether `x` really succeeded. -/
@[specialize] def commitWhen (x : MetaM Bool) : MetaM Bool := do
@[specialize] def commitWhenSome? {α} (x? : MetaM (Option α)) : MetaM (Option α) := do
s ← get;
let env := s.env;
let mctx := s.mctx;
let postponed := s.postponed;
modify $ fun s => { s with postponed := {} };
catch
(condM x
(condM processPostponed
(pure true)
(do restore env mctx postponed; pure false))
(do restore env mctx postponed; pure false))
(do
a? ← x?;
match a? with
| some a =>
(condM processPostponed
(pure (some a))
(do restore env mctx postponed; pure none))
| none => do
restore env mctx postponed; pure none)
(fun ex => do restore env mctx postponed; throw ex)
@[specialize] def commitWhen (x : MetaM Bool) : MetaM Bool := do
r? ← commitWhenSome? (condM x (pure $ some ()) (pure none));
match r? with
| some _ => pure true
| none => pure false
/- Public interface -/
def isLevelDefEq (u v : Level) : MetaM Bool :=

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

@ -95,7 +95,6 @@ extern lean_object* l_Lean_Parser_Level_num___elambda__1___closed__1;
extern lean_object* l_Lean_Expr_ctorName___closed__2;
lean_object* l_ReaderT_failure___at_Lean_Delaborator_DelabM_inhabited___spec__1___rarg(lean_object*);
lean_object* l_Lean_Delaborator_mkDelabAttribute___closed__10;
lean_object* l_Lean_Delaborator_delabProjectionApp___lambda__1___closed__1;
lean_object* l_Lean_Delaborator_delabLam___lambda__1___closed__3;
extern lean_object* l_Lean_Expr_ctorName___closed__8;
lean_object* l_Std_PersistentHashMap_findAtAux___main___at_Lean_Delaborator_delabFor___main___spec__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -255,6 +254,7 @@ lean_object* l_Lean_Delaborator_delabForall___closed__1;
extern lean_object* l_Lean_Expr_isCharLit___closed__3;
lean_object* l___private_Init_Data_Array_Basic_3__iterateRevMAux___main___at_Lean_Delaborator_delabForall___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_numLitKind___closed__2;
extern lean_object* l_Lean_Meta_commitWhen___lambda__1___closed__1;
lean_object* l_Std_RBNode_find___main___at_Lean_Delaborator_getPPOption___spec__1___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Level_getOffsetAux___main(lean_object*, lean_object*);
extern lean_object* l_Lean_Meta_evalNat___main___closed__6;
@ -17541,16 +17541,6 @@ x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1);
return x_5;
}
}
lean_object* _init_l_Lean_Delaborator_delabProjectionApp___lambda__1___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = lean_box(0);
x_2 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
}
}
lean_object* l_Lean_Delaborator_delabProjectionApp___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
@ -17616,7 +17606,7 @@ goto block_172;
else
{
lean_object* x_177;
x_177 = l_Lean_Delaborator_delabProjectionApp___lambda__1___closed__1;
x_177 = l_Lean_Meta_commitWhen___lambda__1___closed__1;
x_18 = x_177;
x_19 = x_4;
goto block_172;
@ -18261,7 +18251,7 @@ goto block_60;
else
{
lean_object* x_66;
x_66 = l_Lean_Delaborator_delabProjectionApp___lambda__1___closed__1;
x_66 = l_Lean_Meta_commitWhen___lambda__1___closed__1;
x_5 = x_66;
x_6 = x_4;
goto block_60;
@ -19048,8 +19038,6 @@ lean_mark_persistent(l___regBuiltin_Lean_Delaborator_delabProj___closed__1);
res = l___regBuiltin_Lean_Delaborator_delabProj(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_Lean_Delaborator_delabProjectionApp___lambda__1___closed__1 = _init_l_Lean_Delaborator_delabProjectionApp___lambda__1___closed__1();
lean_mark_persistent(l_Lean_Delaborator_delabProjectionApp___lambda__1___closed__1);
l_Lean_Delaborator_delabProjectionApp___closed__1 = _init_l_Lean_Delaborator_delabProjectionApp___closed__1();
lean_mark_persistent(l_Lean_Delaborator_delabProjectionApp___closed__1);
l_Lean_Delaborator_delabProjectionApp___closed__2 = _init_l_Lean_Delaborator_delabProjectionApp___closed__2();

5
stage0/stdlib/Lean/Elab/App.c generated
View file

@ -292,7 +292,6 @@ lean_object* l___private_Lean_Elab_App_13__resolveLValAux___closed__24;
uint8_t l_Lean_Expr_hasMVar(lean_object*);
lean_object* l_Lean_Syntax_getArgs(lean_object*);
uint8_t l_Lean_BinderInfo_isExplicit(uint8_t);
lean_object* l_Lean_Elab_Term_registerSyntheticMVar(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_getKind(lean_object*);
lean_object* l___regBuiltin_Lean_Elab_Term_elabProj(lean_object*);
lean_object* l_Lean_Elab_Term_synthesizeInstMVarCore(lean_object*, lean_object*, lean_object*);
@ -343,6 +342,7 @@ lean_object* l___private_Lean_Elab_App_13__resolveLValAux___closed__11;
lean_object* l___private_Lean_Elab_App_10__elabAppArgsAux___main(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_App_19__elabAppLVals___closed__2;
lean_object* l___regBuiltin_Lean_Elab_Term_elabArrayRef___closed__1;
lean_object* l_Lean_Elab_Term_registerSyntheticMVarWithCurrRef(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_App_11__elabAppArgs___closed__4;
uint8_t l_Lean_Syntax_isOfKind(lean_object*, lean_object*);
uint8_t l_Lean_Expr_isOptParam(lean_object*);
@ -734,7 +734,8 @@ x_13 = lean_ctor_get(x_10, 1);
lean_inc(x_13);
lean_dec(x_10);
x_14 = lean_box(0);
x_15 = l_Lean_Elab_Term_registerSyntheticMVar(x_9, x_14, x_3, x_13);
lean_inc(x_3);
x_15 = l_Lean_Elab_Term_registerSyntheticMVarWithCurrRef(x_9, x_14, x_3, x_13);
x_16 = lean_ctor_get(x_15, 1);
lean_inc(x_16);
lean_dec(x_15);

26251
stage0/stdlib/Lean/Elab/Binders.c generated
View file

File diff suppressed because it is too large Load diff

2375
stage0/stdlib/Lean/Elab/Match.c generated
View file

File diff suppressed because it is too large Load diff

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

@ -80,6 +80,7 @@ lean_object* l_Lean_Format_pretty(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_getDeclName_x3f(lean_object*, lean_object*);
uint8_t lean_name_eq(lean_object*, lean_object*);
lean_object* l___regBuiltin_Lean_Elab_Term_elabTacticBlock(lean_object*);
extern lean_object* l_Lean_Meta_commitWhenSome_x3f___at___private_Lean_Meta_ExprDefEq_1__isDefEqEta___spec__2___closed__1;
lean_object* l_Lean_Elab_Term_mkFreshId(lean_object*, lean_object*);
lean_object* l_Lean_Meta_mkForall(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_mkAppM(lean_object*, lean_object*, lean_object*, lean_object*);
@ -177,7 +178,6 @@ lean_object* l_Lean_Elab_Level_elabLevel(lean_object*, lean_object*, lean_object
lean_object* l_Lean_Elab_Term_mkAuxName(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_WHNF_unfoldDefinitionAux___at_Lean_Meta_unfoldDefinition_x3f___spec__1(lean_object*, lean_object*, lean_object*);
lean_object* l___regBuiltin_Lean_Elab_Term_elabRawCharLit(lean_object*);
lean_object* l_Lean_Elab_Term_elabRawNumLit___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_List_repr___rarg___closed__3;
extern lean_object* l_Lean_unitToExpr___lambda__1___closed__3;
lean_object* l___private_Lean_Elab_Term_18__mkPairsAux___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -619,7 +619,7 @@ lean_object* l___regBuiltin_Lean_Elab_Term_elabHole___closed__1;
lean_object* l_Lean_Syntax_isTermId_x3f(lean_object*, uint8_t);
lean_object* l_Lean_Syntax_getArgs(lean_object*);
uint8_t l_Lean_BinderInfo_isExplicit(uint8_t);
lean_object* l_Lean_Elab_Term_registerSyntheticMVar(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_registerSyntheticMVar(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_getKind(lean_object*);
lean_object* l_Lean_Elab_Term_expandArrayLit(lean_object*, lean_object*, lean_object*);
lean_object* l___regBuiltin_Lean_Elab_Term_elabSort___closed__1;
@ -659,7 +659,6 @@ lean_object* l_Lean_Elab_Term_modifyEnv___boxed(lean_object*, lean_object*, lean
lean_object* l_Lean_Elab_logAt___at_Lean_Elab_Term_logTrace___spec__2(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*);
uint8_t l_Array_anyRangeMAux___main___at___private_Lean_Elab_Term_4__hasCDot___main___spec__1(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_resolveGlobalName___boxed(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Meta_commitWhen___at___private_Lean_Meta_ExprDefEq_1__isDefEqEta___spec__1___closed__1;
lean_object* l_Lean_Elab_Term_expandArrayLit___closed__6;
lean_object* l___regBuiltin_Lean_Elab_Term_elabProp___closed__1;
lean_object* l_Lean_Elab_Term_mkConst___closed__1;
@ -713,6 +712,7 @@ lean_object* l_Lean_Elab_Term_mkTacticMVar___closed__2;
lean_object* l_Lean_Meta_instantiateMVars(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Term_21__resolveLocalName(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_mkExplicitBinder___closed__1;
lean_object* l_Lean_Elab_Term_registerSyntheticMVarWithCurrRef(lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l___private_Lean_Elab_Term_13__isExplicitApp(lean_object*);
lean_object* l_Std_PersistentHashMap_find_x3f___at_Lean_Elab_Term_elabUsingElabFns___spec__2___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_elabImplicitLambda___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -828,7 +828,7 @@ lean_object* l_Lean_Elab_Term_resettingSynthInstanceCache(lean_object*);
lean_object* l_Lean_Elab_Term_MetaHasEval(lean_object*);
lean_object* l_Lean_mkConst(lean_object*, lean_object*);
extern lean_object* l_Lean_MessageData_Inhabited___closed__1;
lean_object* l_Lean_Elab_Term_registerSyntheticMVar___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_registerSyntheticMVar___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_withReducible___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_instantiateLevelMVars(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_ensureHasTypeAux(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -6516,7 +6516,6 @@ lean_inc(x_8);
x_9 = l_Lean_TraceState_Inhabited___closed__1;
lean_ctor_set(x_5, 4, x_9);
x_10 = l_Lean_Meta_isLevelDefEq(x_1, x_2, x_8, x_5);
lean_dec(x_8);
if (lean_obj_tag(x_10) == 0)
{
uint8_t x_11;
@ -6605,7 +6604,6 @@ lean_ctor_set(x_36, 3, x_31);
lean_ctor_set(x_36, 4, x_35);
lean_ctor_set(x_36, 5, x_33);
x_37 = l_Lean_Meta_isLevelDefEq(x_1, x_2, x_34, x_36);
lean_dec(x_34);
if (lean_obj_tag(x_37) == 0)
{
lean_object* x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41; lean_object* x_42;
@ -11426,78 +11424,85 @@ x_2 = lean_alloc_closure((void*)(l_Lean_Elab_Term_withMacroExpansion___rarg), 5,
return x_2;
}
}
lean_object* l_Lean_Elab_Term_registerSyntheticMVar(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
lean_object* l_Lean_Elab_Term_registerSyntheticMVar(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
_start:
{
uint8_t x_5;
x_5 = !lean_is_exclusive(x_4);
if (x_5 == 0)
uint8_t x_6;
x_6 = !lean_is_exclusive(x_5);
if (x_6 == 0)
{
lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11;
x_6 = lean_ctor_get(x_3, 9);
x_7 = lean_ctor_get(x_4, 1);
lean_inc(x_6);
lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11;
x_7 = lean_ctor_get(x_5, 1);
x_8 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_8, 0, x_1);
lean_ctor_set(x_8, 1, x_6);
lean_ctor_set(x_8, 2, x_2);
lean_ctor_set(x_8, 0, x_2);
lean_ctor_set(x_8, 1, x_1);
lean_ctor_set(x_8, 2, x_3);
x_9 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_9, 0, x_8);
lean_ctor_set(x_9, 1, x_7);
lean_ctor_set(x_4, 1, x_9);
lean_ctor_set(x_5, 1, x_9);
x_10 = lean_box(0);
x_11 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_11, 0, x_10);
lean_ctor_set(x_11, 1, x_4);
lean_ctor_set(x_11, 1, x_5);
return x_11;
}
else
{
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;
x_12 = lean_ctor_get(x_3, 9);
x_13 = lean_ctor_get(x_4, 0);
x_14 = lean_ctor_get(x_4, 1);
x_15 = lean_ctor_get(x_4, 2);
x_16 = lean_ctor_get(x_4, 3);
x_17 = lean_ctor_get(x_4, 4);
x_18 = lean_ctor_get(x_4, 5);
lean_inc(x_18);
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;
x_12 = lean_ctor_get(x_5, 0);
x_13 = lean_ctor_get(x_5, 1);
x_14 = lean_ctor_get(x_5, 2);
x_15 = lean_ctor_get(x_5, 3);
x_16 = lean_ctor_get(x_5, 4);
x_17 = lean_ctor_get(x_5, 5);
lean_inc(x_17);
lean_inc(x_16);
lean_inc(x_15);
lean_inc(x_14);
lean_inc(x_13);
lean_dec(x_4);
lean_inc(x_12);
x_19 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_19, 0, x_1);
lean_ctor_set(x_19, 1, x_12);
lean_ctor_set(x_19, 2, x_2);
x_20 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_20, 0, x_19);
lean_ctor_set(x_20, 1, x_14);
x_21 = lean_alloc_ctor(0, 6, 0);
lean_ctor_set(x_21, 0, x_13);
lean_ctor_set(x_21, 1, x_20);
lean_ctor_set(x_21, 2, x_15);
lean_ctor_set(x_21, 3, x_16);
lean_ctor_set(x_21, 4, x_17);
lean_ctor_set(x_21, 5, x_18);
x_22 = lean_box(0);
x_23 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_23, 0, x_22);
lean_ctor_set(x_23, 1, x_21);
return x_23;
lean_dec(x_5);
x_18 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_18, 0, x_2);
lean_ctor_set(x_18, 1, x_1);
lean_ctor_set(x_18, 2, x_3);
x_19 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_19, 0, x_18);
lean_ctor_set(x_19, 1, x_13);
x_20 = lean_alloc_ctor(0, 6, 0);
lean_ctor_set(x_20, 0, x_12);
lean_ctor_set(x_20, 1, x_19);
lean_ctor_set(x_20, 2, x_14);
lean_ctor_set(x_20, 3, x_15);
lean_ctor_set(x_20, 4, x_16);
lean_ctor_set(x_20, 5, x_17);
x_21 = lean_box(0);
x_22 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_22, 0, x_21);
lean_ctor_set(x_22, 1, x_20);
return x_22;
}
}
}
lean_object* l_Lean_Elab_Term_registerSyntheticMVar___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
lean_object* l_Lean_Elab_Term_registerSyntheticMVar___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_5;
x_5 = l_Lean_Elab_Term_registerSyntheticMVar(x_1, x_2, x_3, x_4);
lean_object* x_6;
x_6 = l_Lean_Elab_Term_registerSyntheticMVar(x_1, x_2, x_3, x_4, x_5);
lean_dec(x_4);
return x_6;
}
}
lean_object* l_Lean_Elab_Term_registerSyntheticMVarWithCurrRef(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_ctor_get(x_3, 9);
lean_inc(x_5);
x_6 = l_Lean_Elab_Term_registerSyntheticMVar(x_5, x_1, x_2, x_3, x_4);
lean_dec(x_3);
return x_5;
return x_6;
}
}
lean_object* l_Lean_Elab_Term_withoutPostponing___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
@ -14868,8 +14873,7 @@ lean_ctor_set(x_61, 0, x_1);
lean_ctor_set(x_61, 1, x_2);
lean_ctor_set(x_61, 2, x_3);
lean_ctor_set(x_61, 3, x_4);
x_62 = l_Lean_Elab_Term_registerSyntheticMVar(x_42, x_61, x_56, x_60);
lean_dec(x_56);
x_62 = l_Lean_Elab_Term_registerSyntheticMVarWithCurrRef(x_42, x_61, x_56, x_60);
x_63 = !lean_is_exclusive(x_62);
if (x_63 == 0)
{
@ -17156,7 +17160,7 @@ x_86 = l_Lean_mkConst(x_85, x_84);
x_87 = l_Lean_Parser_declareBuiltinParser___closed__3;
lean_inc(x_32);
x_88 = lean_array_push(x_87, x_32);
x_89 = l_Lean_Meta_commitWhen___at___private_Lean_Meta_ExprDefEq_1__isDefEqEta___spec__1___closed__1;
x_89 = l_Lean_Meta_commitWhenSome_x3f___at___private_Lean_Meta_ExprDefEq_1__isDefEqEta___spec__2___closed__1;
x_90 = lean_array_push(x_88, x_89);
lean_inc(x_20);
x_91 = lean_array_push(x_90, x_20);
@ -18173,66 +18177,66 @@ return x_3;
lean_object* l___private_Lean_Elab_Term_10__postponeElabTerm(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
lean_object* x_5; lean_object* x_43; lean_object* x_44; lean_object* x_45; lean_object* x_46; uint8_t x_47;
x_43 = l_Lean_Elab_Term_getOptions(x_3, x_4);
x_44 = lean_ctor_get(x_43, 0);
lean_inc(x_44);
x_45 = lean_ctor_get(x_43, 1);
lean_inc(x_45);
lean_dec(x_43);
x_46 = l___private_Lean_Elab_Term_10__postponeElabTerm___closed__2;
x_47 = l_Lean_checkTraceOption(x_44, x_46);
lean_dec(x_44);
if (x_47 == 0)
lean_object* x_5; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; uint8_t x_24;
x_20 = l_Lean_Elab_Term_getOptions(x_3, x_4);
x_21 = lean_ctor_get(x_20, 0);
lean_inc(x_21);
x_22 = lean_ctor_get(x_20, 1);
lean_inc(x_22);
lean_dec(x_20);
x_23 = l___private_Lean_Elab_Term_10__postponeElabTerm___closed__2;
x_24 = l_Lean_checkTraceOption(x_21, x_23);
lean_dec(x_21);
if (x_24 == 0)
{
x_5 = x_45;
goto block_42;
x_5 = x_22;
goto block_19;
}
else
{
lean_object* x_48; lean_object* x_49; lean_object* x_50;
lean_object* x_25; lean_object* x_26; lean_object* x_27;
lean_inc(x_1);
x_48 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_48, 0, x_1);
x_49 = l___private_Lean_Meta_ExprDefEq_8__checkTypesAndAssign___closed__7;
x_50 = lean_alloc_ctor(9, 2, 0);
lean_ctor_set(x_50, 0, x_48);
lean_ctor_set(x_50, 1, x_49);
x_25 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_25, 0, x_1);
x_26 = l___private_Lean_Meta_ExprDefEq_8__checkTypesAndAssign___closed__7;
x_27 = lean_alloc_ctor(9, 2, 0);
lean_ctor_set(x_27, 0, x_25);
lean_ctor_set(x_27, 1, x_26);
if (lean_obj_tag(x_2) == 0)
{
lean_object* x_51; lean_object* x_52; lean_object* x_53; lean_object* x_54;
x_51 = l_Lean_MessageData_coeOfOptExpr___closed__1;
x_52 = lean_alloc_ctor(9, 2, 0);
lean_ctor_set(x_52, 0, x_50);
lean_ctor_set(x_52, 1, x_51);
x_53 = l_Lean_Elab_Term_logTrace(x_46, x_52, x_3, x_45);
x_54 = lean_ctor_get(x_53, 1);
lean_inc(x_54);
lean_dec(x_53);
x_5 = x_54;
goto block_42;
lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31;
x_28 = l_Lean_MessageData_coeOfOptExpr___closed__1;
x_29 = lean_alloc_ctor(9, 2, 0);
lean_ctor_set(x_29, 0, x_27);
lean_ctor_set(x_29, 1, x_28);
x_30 = l_Lean_Elab_Term_logTrace(x_23, x_29, x_3, x_22);
x_31 = lean_ctor_get(x_30, 1);
lean_inc(x_31);
lean_dec(x_30);
x_5 = x_31;
goto block_19;
}
else
{
lean_object* x_55; lean_object* x_56; lean_object* x_57; lean_object* x_58; lean_object* x_59;
x_55 = lean_ctor_get(x_2, 0);
lean_inc(x_55);
x_56 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_56, 0, x_55);
x_57 = lean_alloc_ctor(9, 2, 0);
lean_ctor_set(x_57, 0, x_50);
lean_ctor_set(x_57, 1, x_56);
x_58 = l_Lean_Elab_Term_logTrace(x_46, x_57, x_3, x_45);
x_59 = lean_ctor_get(x_58, 1);
lean_inc(x_59);
lean_dec(x_58);
x_5 = x_59;
goto block_42;
lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36;
x_32 = lean_ctor_get(x_2, 0);
lean_inc(x_32);
x_33 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_33, 0, x_32);
x_34 = lean_alloc_ctor(9, 2, 0);
lean_ctor_set(x_34, 0, x_27);
lean_ctor_set(x_34, 1, x_33);
x_35 = l_Lean_Elab_Term_logTrace(x_23, x_34, x_3, x_22);
x_36 = lean_ctor_get(x_35, 1);
lean_inc(x_36);
lean_dec(x_35);
x_5 = x_36;
goto block_19;
}
}
block_42:
block_19:
{
uint8_t x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; uint8_t x_12;
uint8_t x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; uint8_t x_15;
x_6 = 2;
x_7 = lean_box(0);
lean_inc(x_3);
@ -18243,109 +18247,31 @@ x_10 = lean_ctor_get(x_8, 1);
lean_inc(x_10);
lean_dec(x_8);
x_11 = l_Lean_Expr_mvarId_x21(x_9);
x_12 = !lean_is_exclusive(x_3);
if (x_12 == 0)
x_12 = lean_ctor_get(x_3, 7);
lean_inc(x_12);
x_13 = lean_alloc_ctor(3, 1, 0);
lean_ctor_set(x_13, 0, x_12);
x_14 = l_Lean_Elab_Term_registerSyntheticMVar(x_1, x_11, x_13, x_3, x_10);
lean_dec(x_3);
x_15 = !lean_is_exclusive(x_14);
if (x_15 == 0)
{
lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; uint8_t x_18;
x_13 = lean_ctor_get(x_3, 7);
x_14 = lean_ctor_get(x_3, 9);
lean_inc(x_13);
x_15 = lean_alloc_ctor(3, 1, 0);
lean_ctor_set(x_15, 0, x_13);
x_16 = l_Lean_Elab_replaceRef(x_1, x_14);
lean_object* x_16;
x_16 = lean_ctor_get(x_14, 0);
lean_dec(x_16);
lean_ctor_set(x_14, 0, x_9);
return x_14;
}
else
{
lean_object* x_17; lean_object* x_18;
x_17 = lean_ctor_get(x_14, 1);
lean_inc(x_17);
lean_dec(x_14);
lean_dec(x_1);
lean_ctor_set(x_3, 9, x_16);
x_17 = l_Lean_Elab_Term_registerSyntheticMVar(x_11, x_15, x_3, x_10);
lean_dec(x_3);
x_18 = !lean_is_exclusive(x_17);
if (x_18 == 0)
{
lean_object* x_19;
x_19 = lean_ctor_get(x_17, 0);
lean_dec(x_19);
lean_ctor_set(x_17, 0, x_9);
return x_17;
}
else
{
lean_object* x_20; lean_object* x_21;
x_20 = lean_ctor_get(x_17, 1);
lean_inc(x_20);
lean_dec(x_17);
x_21 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_21, 0, x_9);
lean_ctor_set(x_21, 1, x_20);
return x_21;
}
}
else
{
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; lean_object* x_30; uint8_t x_31; uint8_t x_32; uint8_t 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;
x_22 = lean_ctor_get(x_3, 0);
x_23 = lean_ctor_get(x_3, 1);
x_24 = lean_ctor_get(x_3, 2);
x_25 = lean_ctor_get(x_3, 3);
x_26 = lean_ctor_get(x_3, 4);
x_27 = lean_ctor_get(x_3, 5);
x_28 = lean_ctor_get(x_3, 6);
x_29 = lean_ctor_get(x_3, 7);
x_30 = lean_ctor_get(x_3, 8);
x_31 = lean_ctor_get_uint8(x_3, sizeof(void*)*10);
x_32 = lean_ctor_get_uint8(x_3, sizeof(void*)*10 + 1);
x_33 = lean_ctor_get_uint8(x_3, sizeof(void*)*10 + 2);
x_34 = lean_ctor_get(x_3, 9);
lean_inc(x_34);
lean_inc(x_30);
lean_inc(x_29);
lean_inc(x_28);
lean_inc(x_27);
lean_inc(x_26);
lean_inc(x_25);
lean_inc(x_24);
lean_inc(x_23);
lean_inc(x_22);
lean_dec(x_3);
lean_inc(x_29);
x_35 = lean_alloc_ctor(3, 1, 0);
lean_ctor_set(x_35, 0, x_29);
x_36 = l_Lean_Elab_replaceRef(x_1, x_34);
lean_dec(x_34);
lean_dec(x_1);
x_37 = lean_alloc_ctor(0, 10, 3);
lean_ctor_set(x_37, 0, x_22);
lean_ctor_set(x_37, 1, x_23);
lean_ctor_set(x_37, 2, x_24);
lean_ctor_set(x_37, 3, x_25);
lean_ctor_set(x_37, 4, x_26);
lean_ctor_set(x_37, 5, x_27);
lean_ctor_set(x_37, 6, x_28);
lean_ctor_set(x_37, 7, x_29);
lean_ctor_set(x_37, 8, x_30);
lean_ctor_set(x_37, 9, x_36);
lean_ctor_set_uint8(x_37, sizeof(void*)*10, x_31);
lean_ctor_set_uint8(x_37, sizeof(void*)*10 + 1, x_32);
lean_ctor_set_uint8(x_37, sizeof(void*)*10 + 2, x_33);
x_38 = l_Lean_Elab_Term_registerSyntheticMVar(x_11, x_35, x_37, x_10);
lean_dec(x_37);
x_39 = lean_ctor_get(x_38, 1);
lean_inc(x_39);
if (lean_is_exclusive(x_38)) {
lean_ctor_release(x_38, 0);
lean_ctor_release(x_38, 1);
x_40 = x_38;
} else {
lean_dec_ref(x_38);
x_40 = lean_box(0);
}
if (lean_is_scalar(x_40)) {
x_41 = lean_alloc_ctor(0, 2, 0);
} else {
x_41 = x_40;
}
lean_ctor_set(x_41, 0, x_9);
lean_ctor_set(x_41, 1, x_39);
return x_41;
x_18 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_18, 0, x_9);
lean_ctor_set(x_18, 1, x_17);
return x_18;
}
}
}
@ -26441,8 +26367,7 @@ x_14 = lean_ctor_get(x_11, 1);
lean_inc(x_14);
lean_dec(x_11);
x_15 = lean_box(0);
x_16 = l_Lean_Elab_Term_registerSyntheticMVar(x_10, x_15, x_2, x_14);
lean_dec(x_2);
x_16 = l_Lean_Elab_Term_registerSyntheticMVarWithCurrRef(x_10, x_15, x_2, x_14);
x_17 = !lean_is_exclusive(x_16);
if (x_17 == 0)
{
@ -27876,9 +27801,10 @@ x_10 = lean_ctor_get(x_8, 1);
lean_inc(x_10);
lean_dec(x_8);
x_11 = l_Lean_Expr_mvarId_x21(x_9);
lean_inc(x_2);
x_12 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_12, 0, x_2);
x_13 = l_Lean_Elab_Term_registerSyntheticMVar(x_11, x_12, x_3, x_10);
x_13 = l_Lean_Elab_Term_registerSyntheticMVar(x_2, x_11, x_12, x_3, x_10);
lean_dec(x_3);
x_14 = !lean_is_exclusive(x_13);
if (x_14 == 0)
@ -30728,6 +30654,7 @@ if (lean_obj_tag(x_63) == 0)
{
lean_object* x_64; lean_object* x_65; uint8_t x_66;
lean_dec(x_2);
lean_dec(x_1);
x_64 = l_Lean_Elab_Term_elabRawStrLit___closed__3;
x_65 = l_Lean_Elab_Term_throwError___rarg(x_64, x_3, x_4);
x_66 = !lean_is_exclusive(x_65);
@ -30775,7 +30702,7 @@ lean_dec(x_9);
x_12 = l_Lean_Expr_mvarId_x21(x_10);
x_13 = lean_box(0);
x_50 = l_Lean_Elab_Term_elabRawNumLit___closed__1;
x_51 = l_Lean_Elab_Term_registerSyntheticMVar(x_12, x_50, x_3, x_11);
x_51 = l_Lean_Elab_Term_registerSyntheticMVar(x_1, x_12, x_50, x_3, x_11);
if (lean_obj_tag(x_2) == 0)
{
lean_object* x_52;
@ -30977,20 +30904,11 @@ return x_48;
}
}
}
lean_object* l_Lean_Elab_Term_elabRawNumLit___boxed(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_Elab_Term_elabRawNumLit(x_1, x_2, x_3, x_4);
lean_dec(x_1);
return x_5;
}
}
lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabRawNumLit___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Lean_Elab_Term_elabRawNumLit___boxed), 4, 0);
x_1 = lean_alloc_closure((void*)(l_Lean_Elab_Term_elabRawNumLit), 4, 0);
return x_1;
}
}
@ -31012,7 +30930,6 @@ lean_object* x_5; lean_object* x_6; lean_object* x_7;
x_5 = lean_unsigned_to_nat(0u);
x_6 = l_Lean_Syntax_getArg(x_1, x_5);
x_7 = l_Lean_Elab_Term_elabRawNumLit(x_6, x_2, x_3, x_4);
lean_dec(x_6);
return x_7;
}
}

3478
stage0/stdlib/Lean/Meta/EqnCompiler/DepElim.c generated
View file

File diff suppressed because it is too large Load diff

5025
stage0/stdlib/Lean/Meta/ExprDefEq.c generated
View file

File diff suppressed because it is too large Load diff

3415
stage0/stdlib/Lean/Meta/LevelDefEq.c generated
View file

File diff suppressed because it is too large Load diff