chore: update stage0
This commit is contained in:
Leonardo de Moura
parent
263d22576b
commit
8094d35366
10 changed files with 7472 additions and 5303 deletions
|
|
@ -271,7 +271,8 @@ private def elabAppArgs (ref : Syntax) (f : Expr) (namedArgs : Array NamedArg) (
|
|||
fType ← inferType ref f;
|
||||
fType ← instantiateMVars ref fType;
|
||||
trace `Elab.app.args ref $ fun _ => "explicit: " ++ toString explicit ++ ", " ++ f ++ " : " ++ fType;
|
||||
tryPostponeIfMVar fType;
|
||||
unless (namedArgs.isEmpty && args.isEmpty) $
|
||||
tryPostponeIfMVar fType;
|
||||
elabAppArgsAux {ref := ref, args := args, expectedType? := expectedType?, explicit := explicit, namedArgs := namedArgs } f fType
|
||||
|
||||
/-- Auxiliary inductive datatype that represents the resolution of an `LVal`. -/
|
||||
|
|
@ -493,17 +494,8 @@ private partial def elabAppFn (ref : Syntax) : Syntax → List LVal → Array Na
|
|||
-- Remark: `id.<namedPattern>` should already have been expanded
|
||||
us ← if us.isEmpty then pure [] else elabExplicitUniv (us.get! 0);
|
||||
elabAppFnId ref id us lvals namedArgs args expectedType? explicit acc
|
||||
| `(@($f:fun)) => do
|
||||
s ← observing $ do {
|
||||
if lvals.isEmpty && namedArgs.isEmpty && args.isEmpty then
|
||||
elabFunCore f expectedType? true
|
||||
else do
|
||||
f ← elabFunCore f none true;
|
||||
elabAppLVals ref f lvals namedArgs args expectedType? true
|
||||
};
|
||||
pure $ acc.push s
|
||||
| `(@$f) =>
|
||||
elabAppFn f lvals namedArgs args expectedType? true acc
|
||||
| `(@$id:id) =>
|
||||
elabAppFn id lvals namedArgs args expectedType? true acc
|
||||
| _ => do
|
||||
s ← observing $ do {
|
||||
f ← elabTerm f none;
|
||||
|
|
@ -579,7 +571,18 @@ def elabAtom : TermElab :=
|
|||
fun stx expectedType? => elabAppAux stx stx #[] #[] expectedType?
|
||||
|
||||
@[builtinTermElab «id»] def elabId : TermElab := elabAtom
|
||||
@[builtinTermElab explicit] def elabExplicit : TermElab := elabAtom
|
||||
|
||||
@[builtinTermElab explicit] def elabExplicit : TermElab :=
|
||||
fun stx expectedType? => match_syntax stx with
|
||||
| `(@$f:fun) => elabFunCore f expectedType? true
|
||||
| `(@($f:fun)) => elabFunCore f expectedType? true
|
||||
| `(@($f:fun : $type)) => do
|
||||
type ← elabType type;
|
||||
f ← elabFunCore f type true;
|
||||
ensureHasType stx type f
|
||||
| `(@$id:id) => elabAtom stx expectedType?
|
||||
| _ => throwUnsupportedSyntax
|
||||
|
||||
@[builtinTermElab choice] def elabChoice : TermElab := elabAtom
|
||||
@[builtinTermElab proj] def elabProj : TermElab := elabAtom
|
||||
@[builtinTermElab arrayRef] def elabArrayRef : TermElab := elabAtom
|
||||
|
|
@ -587,11 +590,6 @@ fun stx expectedType? => elabAppAux stx stx #[] #[] expectedType?
|
|||
but it is nice to have a handler for them because it allows `macros` to insert them into terms. -/
|
||||
@[builtinTermElab ident] def elabRawIdent : TermElab := elabAtom
|
||||
|
||||
@[builtinTermElab «fun»] def elabFun : TermElab :=
|
||||
fun stx expectedType? => do
|
||||
f ← elabFunCore stx expectedType? false;
|
||||
elabAppArgs stx f #[] #[] none false
|
||||
|
||||
@[builtinTermElab sortApp] def elabSortApp : TermElab :=
|
||||
fun stx _ => do
|
||||
u ← elabLevel (stx.getArg 1);
|
||||
|
|
|
|||
|
|
@ -243,7 +243,6 @@ expandFunBindersAux binders body 0 #[]
|
|||
namespace FunBinders
|
||||
|
||||
structure State :=
|
||||
(implicitArgs : Array Expr := #[])
|
||||
(fvars : Array Expr := #[])
|
||||
(lctx : LocalContext)
|
||||
(localInsts : LocalInstances)
|
||||
|
|
@ -267,20 +266,29 @@ private partial def elabFunBinderViews (binderViews : Array BinderView) : Nat
|
|||
if h : i < binderViews.size then
|
||||
let binderView := binderViews.get ⟨i, h⟩;
|
||||
withLCtx s.lctx s.localInsts $ do
|
||||
let s := if binderView.bi.isExplicit then { explicit := true, .. s } else s;
|
||||
type ← elabType binderView.type;
|
||||
fvarId ← mkFreshFVarId;
|
||||
fvarId ← mkFreshFVarId;
|
||||
let fvar := mkFVar fvarId;
|
||||
let fvars := s.fvars.push fvar;
|
||||
-- dbgTrace (toString binderView.id.getId ++ " : " ++ toString type);
|
||||
let lctx := s.lctx.mkLocalDecl fvarId binderView.id.getId type binderView.bi;
|
||||
s ← propagateExpectedType binderView.id fvar type s;
|
||||
className? ← isClass binderView.type type;
|
||||
match className? with
|
||||
| none => elabFunBinderViews (i+1) { fvars := fvars, lctx := lctx, .. s }
|
||||
| some className => do
|
||||
resetSynthInstanceCache;
|
||||
let localInsts := s.localInsts.push { className := className, fvar := mkFVar fvarId };
|
||||
elabFunBinderViews (i+1) { fvars := fvars, lctx := lctx, localInsts := localInsts, .. s }
|
||||
let s := { fvars := s.fvars.push fvar, .. s };
|
||||
let continue (s : State) : TermElabM State := do {
|
||||
className? ← isClass binderView.type type;
|
||||
match className? with
|
||||
| none => elabFunBinderViews (i+1) s
|
||||
| some className => do
|
||||
resetSynthInstanceCache;
|
||||
let localInsts := s.localInsts.push { className := className, fvar := mkFVar fvarId };
|
||||
elabFunBinderViews (i+1) { localInsts := localInsts, .. s }
|
||||
};
|
||||
if s.explicit then do
|
||||
-- dbgTrace (toString binderView.id.getId ++ " : " ++ toString type);
|
||||
let lctx := s.lctx.mkLocalDecl fvarId binderView.id.getId type binderView.bi;
|
||||
s ← propagateExpectedType binderView.id fvar type s;
|
||||
continue { lctx := lctx, .. s }
|
||||
else do
|
||||
mvar ← mkFreshExprMVar binderView.id type;
|
||||
let lctx := s.lctx.mkLetDecl fvarId binderView.id.getId type mvar;
|
||||
continue { lctx := lctx, .. s }
|
||||
else
|
||||
pure s
|
||||
|
||||
|
|
@ -314,6 +322,9 @@ elabFunBinders binders expectedType? explicit $ fun xs expectedType? => do {
|
|||
mkLambda stx xs e
|
||||
}
|
||||
|
||||
@[builtinTermElab «fun»] def elabFun : TermElab :=
|
||||
fun stx expectedType? => elabFunCore stx expectedType? false
|
||||
|
||||
/-
|
||||
Recall that
|
||||
```
|
||||
|
|
|
|||
|
|
@ -522,6 +522,33 @@ fun stx => do
|
|||
logInfo stx (e ++ " : " ++ type);
|
||||
pure ()
|
||||
|
||||
def hasNoErrorMessages : CommandElabM Bool := do
|
||||
s ← get; pure $ !s.messages.hasErrors
|
||||
|
||||
def failIfSucceeds {α} (ref : Syntax) (x : CommandElabM α) : CommandElabM Unit := do
|
||||
let resetMessages : CommandElabM MessageLog := do {
|
||||
s ← get;
|
||||
let messages := s.messages;
|
||||
modify $ fun s => { messages := {}, .. s };
|
||||
pure messages
|
||||
};
|
||||
let restoreMessages (prevMessages : MessageLog) : CommandElabM Unit := do {
|
||||
modify $ fun s => { messages := prevMessages ++ s.messages.errorsToWarnings, .. s }
|
||||
};
|
||||
prevMessages ← resetMessages;
|
||||
succeeded ← finally
|
||||
(catch
|
||||
(do x; hasNoErrorMessages)
|
||||
(fun ex => match ex with
|
||||
| Exception.error msg => do modify (fun s => { messages := s.messages.add msg, .. s }); pure false
|
||||
| Exception.unsupportedSyntax => do logError ref "unsupported syntax"; pure false))
|
||||
(restoreMessages prevMessages);
|
||||
when succeeded $
|
||||
throwError ref "unexpected success"
|
||||
|
||||
@[builtinCommandElab «check_failure»] def elabCheckFailure : CommandElab :=
|
||||
fun stx => failIfSucceeds stx $ elabCheck stx
|
||||
|
||||
@[builtinCommandElab «synth»] def elabSynth : CommandElab :=
|
||||
fun stx => do
|
||||
let ref := stx;
|
||||
|
|
|
|||
|
|
@ -166,6 +166,9 @@ log.msgs.any $ fun m => match m.severity with
|
|||
| MessageSeverity.error => true
|
||||
| _ => false
|
||||
|
||||
def errorsToWarnings (log : MessageLog) : MessageLog :=
|
||||
{ msgs := log.msgs.map (fun m => match m.severity with | MessageSeverity.error => { severity := MessageSeverity.warning, .. m} | _ => m) }
|
||||
|
||||
def forM {m : Type → Type} [Monad m] (log : MessageLog) (f : Message → m Unit) : m Unit :=
|
||||
log.msgs.forM f
|
||||
|
||||
|
|
|
|||
|
|
@ -611,7 +611,7 @@ private partial def processAssignmentAux (mvar : Expr) (mvarDecl : MetavarDecl)
|
|||
arg ← simpAssignmentArg arg;
|
||||
let args := args.set ⟨i, h⟩ arg;
|
||||
let useConstApprox : Unit → MetaM Bool := fun _ =>
|
||||
if cfg.constApprox then
|
||||
if cfg.constApprox || (not args.isEmpty && not v.isApp) then
|
||||
processConstApprox mvar args.size v
|
||||
else
|
||||
pure false;
|
||||
|
|
|
|||
File diff suppressed because it is too large
Load diff
File diff suppressed because it is too large
Load diff
File diff suppressed because it is too large
Load diff
|
|
@ -16,10 +16,13 @@ extern "C" {
|
|||
lean_object* l_List_reverse___rarg(lean_object*);
|
||||
lean_object* l_PersistentArray_forM___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
extern lean_object* l_Lean_Name_toString___closed__1;
|
||||
lean_object* l_PersistentArray_mapM___at_Lean_MessageLog_errorsToWarnings___spec__1(lean_object*);
|
||||
lean_object* l_Array_iterateMAux___main___at_Lean_MessageLog_toList___spec__5(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
extern lean_object* l_addParenHeuristic___closed__2;
|
||||
lean_object* l_Array_umapMAux___main___at_Lean_MessageLog_errorsToWarnings___spec__3(lean_object*, lean_object*);
|
||||
lean_object* l_PersistentArray_foldlM___at_Lean_MessageLog_toList___spec__1___boxed(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_MessageData_ofList___closed__3;
|
||||
lean_object* l_Array_umapMAux___main___at_Lean_MessageLog_errorsToWarnings___spec__4(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_MessageData_ofArray___boxed(lean_object*);
|
||||
lean_object* l_Lean_Message_toString___closed__3;
|
||||
lean_object* l_Lean_MessageLog_Inhabited;
|
||||
|
|
@ -33,6 +36,7 @@ lean_object* l_Lean_MessageData_coeOfSyntax(lean_object*);
|
|||
extern lean_object* l_Lean_List_format___rarg___closed__1;
|
||||
extern lean_object* l_Prod_HasRepr___rarg___closed__1;
|
||||
lean_object* l_Lean_mkMVar(lean_object*);
|
||||
extern lean_object* l_Array_empty___closed__1;
|
||||
extern lean_object* l_Lean_Format_flatten___main___closed__1;
|
||||
lean_object* l_Lean_MessageData_coeOfLevel(lean_object*);
|
||||
uint8_t l_PersistentArray_anyMAux___main___at_Lean_MessageLog_hasErrors___spec__2(lean_object*);
|
||||
|
|
@ -73,6 +77,8 @@ lean_object* l_Array_iterateMAux___main___at_Lean_MessageData_formatAux___main__
|
|||
lean_object* l_Lean_MessageData_Inhabited;
|
||||
lean_object* l_Lean_fmt___at_Lean_MessageData_formatAux___main___spec__1(lean_object*);
|
||||
lean_object* l_Lean_MessageData_stxMaxDepthOption___closed__1;
|
||||
lean_object* lean_array_fset(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_MessageLog_errorsToWarnings(lean_object*);
|
||||
lean_object* l_PersistentArray_foldlM___at_Lean_MessageLog_toList___spec__1(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Message_Inhabited;
|
||||
lean_object* l_Lean_Message_HasToString;
|
||||
|
|
@ -103,6 +109,7 @@ lean_object* l_Lean_MessageData_arrayExpr_toMessageData(lean_object*, lean_objec
|
|||
lean_object* l_Lean_MessageData_joinSep___main(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_KVMap_getNat(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_MessageLog_toList___boxed(lean_object*);
|
||||
lean_object* l_PersistentArray_mapMAux___main___at_Lean_MessageLog_errorsToWarnings___spec__2(lean_object*);
|
||||
lean_object* l_Array_iterateMAux___main___at_Lean_MessageLog_toList___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
uint8_t lean_message_severity(lean_object*);
|
||||
lean_object* l_Lean_MessageLog_HasAppend___closed__1;
|
||||
|
|
@ -143,6 +150,7 @@ lean_object* l_Lean_MessageData_coeOfOptExpr___closed__1;
|
|||
lean_object* l_PersistentArray_foldlMAux___main___at_Lean_MessageLog_toList___spec__2___boxed(lean_object*, lean_object*);
|
||||
uint8_t l_PersistentArray_anyM___at_Lean_MessageLog_hasErrors___spec__1(lean_object*);
|
||||
lean_object* l_Lean_Syntax_formatStxAux___main(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_unsafeCast(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_iterateMAux___main___at_Lean_MessageData_formatAux___main___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Name_toStringWithSep___main(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Message_toString___closed__5;
|
||||
|
|
@ -1881,6 +1889,226 @@ x_3 = lean_box(x_2);
|
|||
return x_3;
|
||||
}
|
||||
}
|
||||
lean_object* l_Array_umapMAux___main___at_Lean_MessageLog_errorsToWarnings___spec__3(lean_object* x_1, lean_object* x_2) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_3; uint8_t x_4;
|
||||
x_3 = lean_array_get_size(x_2);
|
||||
x_4 = lean_nat_dec_lt(x_1, x_3);
|
||||
lean_dec(x_3);
|
||||
if (x_4 == 0)
|
||||
{
|
||||
lean_object* x_5; lean_object* x_6;
|
||||
lean_dec(x_1);
|
||||
x_5 = l_Array_empty___closed__1;
|
||||
x_6 = x_2;
|
||||
return x_6;
|
||||
}
|
||||
else
|
||||
{
|
||||
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; lean_object* x_15;
|
||||
x_7 = lean_array_fget(x_2, x_1);
|
||||
x_8 = lean_box(0);
|
||||
x_9 = x_8;
|
||||
x_10 = lean_array_fset(x_2, x_1, x_9);
|
||||
lean_inc(x_7);
|
||||
x_11 = l_PersistentArray_mapMAux___main___at_Lean_MessageLog_errorsToWarnings___spec__2(x_7);
|
||||
x_12 = lean_unsigned_to_nat(1u);
|
||||
x_13 = lean_nat_add(x_1, x_12);
|
||||
x_14 = x_11;
|
||||
lean_dec(x_7);
|
||||
x_15 = lean_array_fset(x_10, x_1, x_14);
|
||||
lean_dec(x_1);
|
||||
x_1 = x_13;
|
||||
x_2 = x_15;
|
||||
goto _start;
|
||||
}
|
||||
}
|
||||
}
|
||||
lean_object* l_Array_umapMAux___main___at_Lean_MessageLog_errorsToWarnings___spec__4(lean_object* x_1, lean_object* x_2) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_3; uint8_t x_4;
|
||||
x_3 = lean_array_get_size(x_2);
|
||||
x_4 = lean_nat_dec_lt(x_1, x_3);
|
||||
lean_dec(x_3);
|
||||
if (x_4 == 0)
|
||||
{
|
||||
lean_object* x_5; lean_object* x_6;
|
||||
lean_dec(x_1);
|
||||
x_5 = l_Array_empty___closed__1;
|
||||
x_6 = x_2;
|
||||
return x_6;
|
||||
}
|
||||
else
|
||||
{
|
||||
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; uint8_t x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19;
|
||||
x_7 = lean_array_fget(x_2, x_1);
|
||||
x_8 = lean_box(0);
|
||||
x_9 = x_8;
|
||||
x_10 = lean_array_fset(x_2, x_1, x_9);
|
||||
x_11 = lean_ctor_get(x_7, 0);
|
||||
lean_inc(x_11);
|
||||
x_12 = lean_ctor_get(x_7, 1);
|
||||
lean_inc(x_12);
|
||||
x_13 = lean_ctor_get(x_7, 2);
|
||||
lean_inc(x_13);
|
||||
x_14 = lean_ctor_get_uint8(x_7, sizeof(void*)*5);
|
||||
x_15 = lean_ctor_get(x_7, 3);
|
||||
lean_inc(x_15);
|
||||
x_16 = lean_ctor_get(x_7, 4);
|
||||
lean_inc(x_16);
|
||||
x_17 = lean_unsigned_to_nat(1u);
|
||||
x_18 = lean_nat_add(x_1, x_17);
|
||||
x_19 = lean_box(x_14);
|
||||
if (lean_obj_tag(x_19) == 2)
|
||||
{
|
||||
uint8_t x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23;
|
||||
x_20 = 1;
|
||||
x_21 = lean_alloc_ctor(0, 5, 1);
|
||||
lean_ctor_set(x_21, 0, x_11);
|
||||
lean_ctor_set(x_21, 1, x_12);
|
||||
lean_ctor_set(x_21, 2, x_13);
|
||||
lean_ctor_set(x_21, 3, x_15);
|
||||
lean_ctor_set(x_21, 4, x_16);
|
||||
lean_ctor_set_uint8(x_21, sizeof(void*)*5, x_20);
|
||||
x_22 = x_21;
|
||||
lean_dec(x_7);
|
||||
x_23 = lean_array_fset(x_10, x_1, x_22);
|
||||
lean_dec(x_1);
|
||||
x_1 = x_18;
|
||||
x_2 = x_23;
|
||||
goto _start;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_25; lean_object* x_26;
|
||||
lean_dec(x_19);
|
||||
lean_dec(x_16);
|
||||
lean_dec(x_15);
|
||||
lean_dec(x_13);
|
||||
lean_dec(x_12);
|
||||
lean_dec(x_11);
|
||||
lean_inc(x_7);
|
||||
x_25 = x_7;
|
||||
lean_dec(x_7);
|
||||
x_26 = lean_array_fset(x_10, x_1, x_25);
|
||||
lean_dec(x_1);
|
||||
x_1 = x_18;
|
||||
x_2 = x_26;
|
||||
goto _start;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
lean_object* l_PersistentArray_mapMAux___main___at_Lean_MessageLog_errorsToWarnings___spec__2(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
if (lean_obj_tag(x_1) == 0)
|
||||
{
|
||||
uint8_t x_2;
|
||||
x_2 = !lean_is_exclusive(x_1);
|
||||
if (x_2 == 0)
|
||||
{
|
||||
lean_object* x_3; lean_object* x_4; lean_object* x_5;
|
||||
x_3 = lean_ctor_get(x_1, 0);
|
||||
x_4 = lean_unsigned_to_nat(0u);
|
||||
x_5 = l_Array_umapMAux___main___at_Lean_MessageLog_errorsToWarnings___spec__3(x_4, x_3);
|
||||
lean_ctor_set(x_1, 0, x_5);
|
||||
return x_1;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9;
|
||||
x_6 = lean_ctor_get(x_1, 0);
|
||||
lean_inc(x_6);
|
||||
lean_dec(x_1);
|
||||
x_7 = lean_unsigned_to_nat(0u);
|
||||
x_8 = l_Array_umapMAux___main___at_Lean_MessageLog_errorsToWarnings___spec__3(x_7, x_6);
|
||||
x_9 = lean_alloc_ctor(0, 1, 0);
|
||||
lean_ctor_set(x_9, 0, x_8);
|
||||
return x_9;
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
uint8_t x_10;
|
||||
x_10 = !lean_is_exclusive(x_1);
|
||||
if (x_10 == 0)
|
||||
{
|
||||
lean_object* x_11; lean_object* x_12; lean_object* x_13;
|
||||
x_11 = lean_ctor_get(x_1, 0);
|
||||
x_12 = lean_unsigned_to_nat(0u);
|
||||
x_13 = l_Array_umapMAux___main___at_Lean_MessageLog_errorsToWarnings___spec__4(x_12, x_11);
|
||||
lean_ctor_set(x_1, 0, x_13);
|
||||
return x_1;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17;
|
||||
x_14 = lean_ctor_get(x_1, 0);
|
||||
lean_inc(x_14);
|
||||
lean_dec(x_1);
|
||||
x_15 = lean_unsigned_to_nat(0u);
|
||||
x_16 = l_Array_umapMAux___main___at_Lean_MessageLog_errorsToWarnings___spec__4(x_15, x_14);
|
||||
x_17 = lean_alloc_ctor(1, 1, 0);
|
||||
lean_ctor_set(x_17, 0, x_16);
|
||||
return x_17;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
lean_object* l_PersistentArray_mapM___at_Lean_MessageLog_errorsToWarnings___spec__1(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
uint8_t x_2;
|
||||
x_2 = !lean_is_exclusive(x_1);
|
||||
if (x_2 == 0)
|
||||
{
|
||||
lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7;
|
||||
x_3 = lean_ctor_get(x_1, 0);
|
||||
x_4 = lean_ctor_get(x_1, 1);
|
||||
x_5 = l_PersistentArray_mapMAux___main___at_Lean_MessageLog_errorsToWarnings___spec__2(x_3);
|
||||
x_6 = lean_unsigned_to_nat(0u);
|
||||
x_7 = l_Array_umapMAux___main___at_Lean_MessageLog_errorsToWarnings___spec__4(x_6, x_4);
|
||||
lean_ctor_set(x_1, 1, x_7);
|
||||
lean_ctor_set(x_1, 0, x_5);
|
||||
return x_1;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_8; lean_object* x_9; lean_object* x_10; size_t x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16;
|
||||
x_8 = lean_ctor_get(x_1, 0);
|
||||
x_9 = lean_ctor_get(x_1, 1);
|
||||
x_10 = lean_ctor_get(x_1, 2);
|
||||
x_11 = lean_ctor_get_usize(x_1, 4);
|
||||
x_12 = lean_ctor_get(x_1, 3);
|
||||
lean_inc(x_12);
|
||||
lean_inc(x_10);
|
||||
lean_inc(x_9);
|
||||
lean_inc(x_8);
|
||||
lean_dec(x_1);
|
||||
x_13 = l_PersistentArray_mapMAux___main___at_Lean_MessageLog_errorsToWarnings___spec__2(x_8);
|
||||
x_14 = lean_unsigned_to_nat(0u);
|
||||
x_15 = l_Array_umapMAux___main___at_Lean_MessageLog_errorsToWarnings___spec__4(x_14, x_9);
|
||||
x_16 = lean_alloc_ctor(0, 4, sizeof(size_t)*1);
|
||||
lean_ctor_set(x_16, 0, x_13);
|
||||
lean_ctor_set(x_16, 1, x_15);
|
||||
lean_ctor_set(x_16, 2, x_10);
|
||||
lean_ctor_set(x_16, 3, x_12);
|
||||
lean_ctor_set_usize(x_16, 4, x_11);
|
||||
return x_16;
|
||||
}
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_MessageLog_errorsToWarnings(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_2;
|
||||
x_2 = l_PersistentArray_mapM___at_Lean_MessageLog_errorsToWarnings___spec__1(x_1);
|
||||
return x_2;
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_MessageLog_forM___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
|
||||
_start:
|
||||
{
|
||||
|
|
|
|||
|
|
@ -38497,61 +38497,61 @@ lean_inc(x_5);
|
|||
x_161 = lean_array_fset(x_5, x_4, x_158);
|
||||
if (lean_obj_tag(x_158) == 1)
|
||||
{
|
||||
lean_object* x_201; lean_object* x_202; uint8_t x_203;
|
||||
x_201 = lean_ctor_get(x_158, 0);
|
||||
lean_inc(x_201);
|
||||
x_202 = lean_array_get_size(x_161);
|
||||
x_203 = lean_nat_dec_le(x_4, x_202);
|
||||
if (x_203 == 0)
|
||||
lean_object* x_211; lean_object* x_212; uint8_t x_213;
|
||||
x_211 = lean_ctor_get(x_158, 0);
|
||||
lean_inc(x_211);
|
||||
x_212 = lean_array_get_size(x_161);
|
||||
x_213 = lean_nat_dec_le(x_4, x_212);
|
||||
if (x_213 == 0)
|
||||
{
|
||||
lean_object* x_204; uint8_t x_205;
|
||||
x_204 = lean_unsigned_to_nat(0u);
|
||||
x_205 = l_Array_anyRangeMAux___main___at___private_Init_Lean_Meta_ExprDefEq_18__processAssignmentAux___main___spec__2(x_4, x_5, lean_box(0), x_158, x_161, x_202, x_204);
|
||||
lean_dec(x_202);
|
||||
lean_object* x_214; uint8_t x_215;
|
||||
x_214 = lean_unsigned_to_nat(0u);
|
||||
x_215 = l_Array_anyRangeMAux___main___at___private_Init_Lean_Meta_ExprDefEq_18__processAssignmentAux___main___spec__2(x_4, x_5, lean_box(0), x_158, x_161, x_212, x_214);
|
||||
lean_dec(x_212);
|
||||
lean_dec(x_158);
|
||||
lean_dec(x_5);
|
||||
if (x_205 == 0)
|
||||
if (x_215 == 0)
|
||||
{
|
||||
lean_object* x_206; uint8_t x_207;
|
||||
x_206 = lean_ctor_get(x_2, 1);
|
||||
lean_inc(x_206);
|
||||
x_207 = l_Lean_LocalContext_contains(x_206, x_201);
|
||||
lean_dec(x_201);
|
||||
if (x_207 == 0)
|
||||
lean_object* x_216; uint8_t x_217;
|
||||
x_216 = lean_ctor_get(x_2, 1);
|
||||
lean_inc(x_216);
|
||||
x_217 = l_Lean_LocalContext_contains(x_216, x_211);
|
||||
lean_dec(x_211);
|
||||
if (x_217 == 0)
|
||||
{
|
||||
lean_object* x_208; lean_object* x_209;
|
||||
lean_object* x_218; lean_object* x_219;
|
||||
lean_dec(x_160);
|
||||
lean_dec(x_155);
|
||||
x_208 = lean_unsigned_to_nat(1u);
|
||||
x_209 = lean_nat_add(x_4, x_208);
|
||||
x_218 = lean_unsigned_to_nat(1u);
|
||||
x_219 = lean_nat_add(x_4, x_218);
|
||||
lean_dec(x_4);
|
||||
x_4 = x_209;
|
||||
x_4 = x_219;
|
||||
x_5 = x_161;
|
||||
x_7 = x_159;
|
||||
goto _start;
|
||||
}
|
||||
else
|
||||
{
|
||||
uint8_t x_211;
|
||||
x_211 = lean_ctor_get_uint8(x_155, sizeof(void*)*1 + 2);
|
||||
if (x_211 == 0)
|
||||
uint8_t x_221;
|
||||
x_221 = lean_ctor_get_uint8(x_155, sizeof(void*)*1 + 2);
|
||||
if (x_221 == 0)
|
||||
{
|
||||
lean_object* x_212;
|
||||
lean_object* x_222;
|
||||
lean_dec(x_4);
|
||||
lean_dec(x_2);
|
||||
x_212 = lean_box(0);
|
||||
x_162 = x_212;
|
||||
goto block_200;
|
||||
x_222 = lean_box(0);
|
||||
x_162 = x_222;
|
||||
goto block_210;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_213; lean_object* x_214;
|
||||
lean_object* x_223; lean_object* x_224;
|
||||
lean_dec(x_160);
|
||||
lean_dec(x_155);
|
||||
x_213 = lean_unsigned_to_nat(1u);
|
||||
x_214 = lean_nat_add(x_4, x_213);
|
||||
x_223 = lean_unsigned_to_nat(1u);
|
||||
x_224 = lean_nat_add(x_4, x_223);
|
||||
lean_dec(x_4);
|
||||
x_4 = x_214;
|
||||
x_4 = x_224;
|
||||
x_5 = x_161;
|
||||
x_7 = x_159;
|
||||
goto _start;
|
||||
|
|
@ -38560,275 +38560,320 @@ goto _start;
|
|||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_216;
|
||||
lean_dec(x_201);
|
||||
lean_object* x_226;
|
||||
lean_dec(x_211);
|
||||
lean_dec(x_4);
|
||||
lean_dec(x_2);
|
||||
x_216 = lean_box(0);
|
||||
x_162 = x_216;
|
||||
goto block_200;
|
||||
x_226 = lean_box(0);
|
||||
x_162 = x_226;
|
||||
goto block_210;
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_217; uint8_t x_218;
|
||||
lean_dec(x_202);
|
||||
x_217 = lean_unsigned_to_nat(0u);
|
||||
x_218 = l_Array_anyRangeMAux___main___at___private_Init_Lean_Meta_ExprDefEq_18__processAssignmentAux___main___spec__3(x_4, x_5, lean_box(0), x_158, lean_box(0), x_161, x_4, x_217);
|
||||
lean_object* x_227; uint8_t x_228;
|
||||
lean_dec(x_212);
|
||||
x_227 = lean_unsigned_to_nat(0u);
|
||||
x_228 = l_Array_anyRangeMAux___main___at___private_Init_Lean_Meta_ExprDefEq_18__processAssignmentAux___main___spec__3(x_4, x_5, lean_box(0), x_158, lean_box(0), x_161, x_4, x_227);
|
||||
lean_dec(x_158);
|
||||
lean_dec(x_5);
|
||||
if (x_218 == 0)
|
||||
if (x_228 == 0)
|
||||
{
|
||||
lean_object* x_219; uint8_t x_220;
|
||||
x_219 = lean_ctor_get(x_2, 1);
|
||||
lean_inc(x_219);
|
||||
x_220 = l_Lean_LocalContext_contains(x_219, x_201);
|
||||
lean_dec(x_201);
|
||||
if (x_220 == 0)
|
||||
{
|
||||
lean_object* x_221; lean_object* x_222;
|
||||
lean_dec(x_160);
|
||||
lean_dec(x_155);
|
||||
x_221 = lean_unsigned_to_nat(1u);
|
||||
x_222 = lean_nat_add(x_4, x_221);
|
||||
lean_dec(x_4);
|
||||
x_4 = x_222;
|
||||
x_5 = x_161;
|
||||
x_7 = x_159;
|
||||
goto _start;
|
||||
}
|
||||
else
|
||||
{
|
||||
uint8_t x_224;
|
||||
x_224 = lean_ctor_get_uint8(x_155, sizeof(void*)*1 + 2);
|
||||
if (x_224 == 0)
|
||||
{
|
||||
lean_object* x_225;
|
||||
lean_dec(x_4);
|
||||
lean_dec(x_2);
|
||||
x_225 = lean_box(0);
|
||||
x_162 = x_225;
|
||||
goto block_200;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_226; lean_object* x_227;
|
||||
lean_dec(x_160);
|
||||
lean_dec(x_155);
|
||||
x_226 = lean_unsigned_to_nat(1u);
|
||||
x_227 = lean_nat_add(x_4, x_226);
|
||||
lean_dec(x_4);
|
||||
x_4 = x_227;
|
||||
x_5 = x_161;
|
||||
x_7 = x_159;
|
||||
goto _start;
|
||||
}
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_229;
|
||||
lean_dec(x_201);
|
||||
lean_dec(x_4);
|
||||
lean_dec(x_2);
|
||||
x_229 = lean_box(0);
|
||||
x_162 = x_229;
|
||||
goto block_200;
|
||||
}
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
uint8_t x_230;
|
||||
lean_dec(x_160);
|
||||
lean_dec(x_158);
|
||||
lean_dec(x_5);
|
||||
lean_dec(x_4);
|
||||
lean_dec(x_2);
|
||||
x_230 = lean_ctor_get_uint8(x_155, sizeof(void*)*1);
|
||||
lean_object* x_229; uint8_t x_230;
|
||||
x_229 = lean_ctor_get(x_2, 1);
|
||||
lean_inc(x_229);
|
||||
x_230 = l_Lean_LocalContext_contains(x_229, x_211);
|
||||
lean_dec(x_211);
|
||||
if (x_230 == 0)
|
||||
{
|
||||
uint8_t x_231;
|
||||
x_231 = lean_ctor_get_uint8(x_155, sizeof(void*)*1 + 3);
|
||||
lean_object* x_231; lean_object* x_232;
|
||||
lean_dec(x_160);
|
||||
lean_dec(x_155);
|
||||
if (x_231 == 0)
|
||||
x_231 = lean_unsigned_to_nat(1u);
|
||||
x_232 = lean_nat_add(x_4, x_231);
|
||||
lean_dec(x_4);
|
||||
x_4 = x_232;
|
||||
x_5 = x_161;
|
||||
x_7 = x_159;
|
||||
goto _start;
|
||||
}
|
||||
else
|
||||
{
|
||||
uint8_t x_232; lean_object* x_233; lean_object* x_234;
|
||||
uint8_t x_234;
|
||||
x_234 = lean_ctor_get_uint8(x_155, sizeof(void*)*1 + 2);
|
||||
if (x_234 == 0)
|
||||
{
|
||||
lean_object* x_235;
|
||||
lean_dec(x_4);
|
||||
lean_dec(x_2);
|
||||
x_235 = lean_box(0);
|
||||
x_162 = x_235;
|
||||
goto block_210;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_236; lean_object* x_237;
|
||||
lean_dec(x_160);
|
||||
lean_dec(x_155);
|
||||
x_236 = lean_unsigned_to_nat(1u);
|
||||
x_237 = lean_nat_add(x_4, x_236);
|
||||
lean_dec(x_4);
|
||||
x_4 = x_237;
|
||||
x_5 = x_161;
|
||||
x_7 = x_159;
|
||||
goto _start;
|
||||
}
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_239;
|
||||
lean_dec(x_211);
|
||||
lean_dec(x_4);
|
||||
lean_dec(x_2);
|
||||
x_239 = lean_box(0);
|
||||
x_162 = x_239;
|
||||
goto block_210;
|
||||
}
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
uint8_t x_240;
|
||||
lean_dec(x_160);
|
||||
lean_dec(x_158);
|
||||
lean_dec(x_5);
|
||||
lean_dec(x_4);
|
||||
lean_dec(x_2);
|
||||
x_240 = lean_ctor_get_uint8(x_155, sizeof(void*)*1);
|
||||
if (x_240 == 0)
|
||||
{
|
||||
uint8_t x_241;
|
||||
x_241 = lean_ctor_get_uint8(x_155, sizeof(void*)*1 + 3);
|
||||
lean_dec(x_155);
|
||||
if (x_241 == 0)
|
||||
{
|
||||
uint8_t x_242;
|
||||
x_242 = l_Array_isEmpty___rarg(x_161);
|
||||
if (x_242 == 0)
|
||||
{
|
||||
uint8_t x_243;
|
||||
x_243 = l_Lean_Expr_isApp(x_3);
|
||||
if (x_243 == 0)
|
||||
{
|
||||
lean_object* x_244; lean_object* x_245;
|
||||
x_244 = lean_array_get_size(x_161);
|
||||
lean_dec(x_161);
|
||||
x_245 = l___private_Init_Lean_Meta_ExprDefEq_17__processConstApprox(x_1, x_244, x_3, x_6, x_159);
|
||||
return x_245;
|
||||
}
|
||||
else
|
||||
{
|
||||
uint8_t x_246; lean_object* x_247; lean_object* x_248;
|
||||
lean_dec(x_161);
|
||||
lean_dec(x_6);
|
||||
lean_dec(x_3);
|
||||
lean_dec(x_1);
|
||||
x_232 = 0;
|
||||
x_233 = lean_box(x_232);
|
||||
x_234 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_234, 0, x_233);
|
||||
lean_ctor_set(x_234, 1, x_159);
|
||||
return x_234;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_235; lean_object* x_236;
|
||||
x_235 = lean_array_get_size(x_161);
|
||||
lean_dec(x_161);
|
||||
x_236 = l___private_Init_Lean_Meta_ExprDefEq_17__processConstApprox(x_1, x_235, x_3, x_6, x_159);
|
||||
return x_236;
|
||||
x_246 = 0;
|
||||
x_247 = lean_box(x_246);
|
||||
x_248 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_248, 0, x_247);
|
||||
lean_ctor_set(x_248, 1, x_159);
|
||||
return x_248;
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
uint8_t x_237;
|
||||
x_237 = l_Lean_Expr_isApp(x_3);
|
||||
if (x_237 == 0)
|
||||
{
|
||||
uint8_t x_238;
|
||||
x_238 = lean_ctor_get_uint8(x_155, sizeof(void*)*1 + 3);
|
||||
lean_dec(x_155);
|
||||
if (x_238 == 0)
|
||||
{
|
||||
uint8_t x_239; lean_object* x_240; lean_object* x_241;
|
||||
uint8_t x_249; lean_object* x_250; lean_object* x_251;
|
||||
lean_dec(x_161);
|
||||
lean_dec(x_6);
|
||||
lean_dec(x_3);
|
||||
lean_dec(x_1);
|
||||
x_239 = 0;
|
||||
x_240 = lean_box(x_239);
|
||||
x_241 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_241, 0, x_240);
|
||||
lean_ctor_set(x_241, 1, x_159);
|
||||
return x_241;
|
||||
x_249 = 0;
|
||||
x_250 = lean_box(x_249);
|
||||
x_251 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_251, 0, x_250);
|
||||
lean_ctor_set(x_251, 1, x_159);
|
||||
return x_251;
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_242; lean_object* x_243;
|
||||
x_242 = lean_array_get_size(x_161);
|
||||
lean_object* x_252; lean_object* x_253;
|
||||
x_252 = lean_array_get_size(x_161);
|
||||
lean_dec(x_161);
|
||||
x_243 = l___private_Init_Lean_Meta_ExprDefEq_17__processConstApprox(x_1, x_242, x_3, x_6, x_159);
|
||||
return x_243;
|
||||
x_253 = l___private_Init_Lean_Meta_ExprDefEq_17__processConstApprox(x_1, x_252, x_3, x_6, x_159);
|
||||
return x_253;
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_244;
|
||||
uint8_t x_254;
|
||||
x_254 = l_Lean_Expr_isApp(x_3);
|
||||
if (x_254 == 0)
|
||||
{
|
||||
uint8_t x_255;
|
||||
x_255 = lean_ctor_get_uint8(x_155, sizeof(void*)*1 + 3);
|
||||
lean_dec(x_155);
|
||||
if (x_255 == 0)
|
||||
{
|
||||
uint8_t x_256;
|
||||
x_256 = l_Array_isEmpty___rarg(x_161);
|
||||
if (x_256 == 0)
|
||||
{
|
||||
lean_object* x_257; lean_object* x_258;
|
||||
x_257 = lean_array_get_size(x_161);
|
||||
lean_dec(x_161);
|
||||
x_258 = l___private_Init_Lean_Meta_ExprDefEq_17__processConstApprox(x_1, x_257, x_3, x_6, x_159);
|
||||
return x_258;
|
||||
}
|
||||
else
|
||||
{
|
||||
uint8_t x_259; lean_object* x_260; lean_object* x_261;
|
||||
lean_dec(x_161);
|
||||
lean_dec(x_6);
|
||||
lean_dec(x_3);
|
||||
lean_dec(x_1);
|
||||
x_259 = 0;
|
||||
x_260 = lean_box(x_259);
|
||||
x_261 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_261, 0, x_260);
|
||||
lean_ctor_set(x_261, 1, x_159);
|
||||
return x_261;
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_262; lean_object* x_263;
|
||||
x_262 = lean_array_get_size(x_161);
|
||||
lean_dec(x_161);
|
||||
x_263 = l___private_Init_Lean_Meta_ExprDefEq_17__processConstApprox(x_1, x_262, x_3, x_6, x_159);
|
||||
return x_263;
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_264;
|
||||
lean_inc(x_6);
|
||||
lean_inc(x_3);
|
||||
lean_inc(x_1);
|
||||
x_244 = l___private_Init_Lean_Meta_ExprDefEq_14__processAssignmentFOApprox___main(x_1, x_161, x_3, x_6, x_159);
|
||||
if (lean_obj_tag(x_244) == 0)
|
||||
x_264 = l___private_Init_Lean_Meta_ExprDefEq_14__processAssignmentFOApprox___main(x_1, x_161, x_3, x_6, x_159);
|
||||
if (lean_obj_tag(x_264) == 0)
|
||||
{
|
||||
lean_object* x_245; uint8_t x_246;
|
||||
x_245 = lean_ctor_get(x_244, 0);
|
||||
lean_inc(x_245);
|
||||
x_246 = lean_unbox(x_245);
|
||||
if (x_246 == 0)
|
||||
{
|
||||
uint8_t x_247;
|
||||
lean_dec(x_245);
|
||||
x_247 = lean_ctor_get_uint8(x_155, sizeof(void*)*1 + 3);
|
||||
lean_dec(x_155);
|
||||
if (x_247 == 0)
|
||||
{
|
||||
uint8_t x_248;
|
||||
lean_dec(x_161);
|
||||
lean_dec(x_6);
|
||||
lean_dec(x_3);
|
||||
lean_dec(x_1);
|
||||
x_248 = !lean_is_exclusive(x_244);
|
||||
if (x_248 == 0)
|
||||
{
|
||||
lean_object* x_249; uint8_t x_250; lean_object* x_251;
|
||||
x_249 = lean_ctor_get(x_244, 0);
|
||||
lean_dec(x_249);
|
||||
x_250 = 0;
|
||||
x_251 = lean_box(x_250);
|
||||
lean_ctor_set(x_244, 0, x_251);
|
||||
return x_244;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_252; uint8_t x_253; lean_object* x_254; lean_object* x_255;
|
||||
x_252 = lean_ctor_get(x_244, 1);
|
||||
lean_inc(x_252);
|
||||
lean_dec(x_244);
|
||||
x_253 = 0;
|
||||
x_254 = lean_box(x_253);
|
||||
x_255 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_255, 0, x_254);
|
||||
lean_ctor_set(x_255, 1, x_252);
|
||||
return x_255;
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_256; lean_object* x_257; lean_object* x_258;
|
||||
x_256 = lean_ctor_get(x_244, 1);
|
||||
lean_inc(x_256);
|
||||
lean_dec(x_244);
|
||||
x_257 = lean_array_get_size(x_161);
|
||||
lean_dec(x_161);
|
||||
x_258 = l___private_Init_Lean_Meta_ExprDefEq_17__processConstApprox(x_1, x_257, x_3, x_6, x_256);
|
||||
return x_258;
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
uint8_t x_259;
|
||||
lean_dec(x_161);
|
||||
lean_dec(x_155);
|
||||
lean_dec(x_6);
|
||||
lean_dec(x_3);
|
||||
lean_dec(x_1);
|
||||
x_259 = !lean_is_exclusive(x_244);
|
||||
if (x_259 == 0)
|
||||
{
|
||||
lean_object* x_260;
|
||||
x_260 = lean_ctor_get(x_244, 0);
|
||||
lean_dec(x_260);
|
||||
return x_244;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_261; lean_object* x_262;
|
||||
x_261 = lean_ctor_get(x_244, 1);
|
||||
lean_inc(x_261);
|
||||
lean_dec(x_244);
|
||||
x_262 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_262, 0, x_245);
|
||||
lean_ctor_set(x_262, 1, x_261);
|
||||
return x_262;
|
||||
}
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
uint8_t x_263;
|
||||
lean_dec(x_161);
|
||||
lean_dec(x_155);
|
||||
lean_dec(x_6);
|
||||
lean_dec(x_3);
|
||||
lean_dec(x_1);
|
||||
x_263 = !lean_is_exclusive(x_244);
|
||||
if (x_263 == 0)
|
||||
{
|
||||
return x_244;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_264; lean_object* x_265; lean_object* x_266;
|
||||
x_264 = lean_ctor_get(x_244, 0);
|
||||
x_265 = lean_ctor_get(x_244, 1);
|
||||
lean_object* x_265; uint8_t x_266;
|
||||
x_265 = lean_ctor_get(x_264, 0);
|
||||
lean_inc(x_265);
|
||||
lean_inc(x_264);
|
||||
lean_dec(x_244);
|
||||
x_266 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_266, 0, x_264);
|
||||
lean_ctor_set(x_266, 1, x_265);
|
||||
return x_266;
|
||||
x_266 = lean_unbox(x_265);
|
||||
if (x_266 == 0)
|
||||
{
|
||||
uint8_t x_267;
|
||||
lean_dec(x_265);
|
||||
x_267 = lean_ctor_get_uint8(x_155, sizeof(void*)*1 + 3);
|
||||
lean_dec(x_155);
|
||||
if (x_267 == 0)
|
||||
{
|
||||
uint8_t x_268;
|
||||
lean_dec(x_161);
|
||||
lean_dec(x_6);
|
||||
lean_dec(x_3);
|
||||
lean_dec(x_1);
|
||||
x_268 = !lean_is_exclusive(x_264);
|
||||
if (x_268 == 0)
|
||||
{
|
||||
lean_object* x_269; uint8_t x_270; lean_object* x_271;
|
||||
x_269 = lean_ctor_get(x_264, 0);
|
||||
lean_dec(x_269);
|
||||
x_270 = 0;
|
||||
x_271 = lean_box(x_270);
|
||||
lean_ctor_set(x_264, 0, x_271);
|
||||
return x_264;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_272; uint8_t x_273; lean_object* x_274; lean_object* x_275;
|
||||
x_272 = lean_ctor_get(x_264, 1);
|
||||
lean_inc(x_272);
|
||||
lean_dec(x_264);
|
||||
x_273 = 0;
|
||||
x_274 = lean_box(x_273);
|
||||
x_275 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_275, 0, x_274);
|
||||
lean_ctor_set(x_275, 1, x_272);
|
||||
return x_275;
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_276; lean_object* x_277; lean_object* x_278;
|
||||
x_276 = lean_ctor_get(x_264, 1);
|
||||
lean_inc(x_276);
|
||||
lean_dec(x_264);
|
||||
x_277 = lean_array_get_size(x_161);
|
||||
lean_dec(x_161);
|
||||
x_278 = l___private_Init_Lean_Meta_ExprDefEq_17__processConstApprox(x_1, x_277, x_3, x_6, x_276);
|
||||
return x_278;
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
uint8_t x_279;
|
||||
lean_dec(x_161);
|
||||
lean_dec(x_155);
|
||||
lean_dec(x_6);
|
||||
lean_dec(x_3);
|
||||
lean_dec(x_1);
|
||||
x_279 = !lean_is_exclusive(x_264);
|
||||
if (x_279 == 0)
|
||||
{
|
||||
lean_object* x_280;
|
||||
x_280 = lean_ctor_get(x_264, 0);
|
||||
lean_dec(x_280);
|
||||
return x_264;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_281; lean_object* x_282;
|
||||
x_281 = lean_ctor_get(x_264, 1);
|
||||
lean_inc(x_281);
|
||||
lean_dec(x_264);
|
||||
x_282 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_282, 0, x_265);
|
||||
lean_ctor_set(x_282, 1, x_281);
|
||||
return x_282;
|
||||
}
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
uint8_t x_283;
|
||||
lean_dec(x_161);
|
||||
lean_dec(x_155);
|
||||
lean_dec(x_6);
|
||||
lean_dec(x_3);
|
||||
lean_dec(x_1);
|
||||
x_283 = !lean_is_exclusive(x_264);
|
||||
if (x_283 == 0)
|
||||
{
|
||||
return x_264;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_284; lean_object* x_285; lean_object* x_286;
|
||||
x_284 = lean_ctor_get(x_264, 0);
|
||||
x_285 = lean_ctor_get(x_264, 1);
|
||||
lean_inc(x_285);
|
||||
lean_inc(x_284);
|
||||
lean_dec(x_264);
|
||||
x_286 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_286, 0, x_284);
|
||||
lean_ctor_set(x_286, 1, x_285);
|
||||
return x_286;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
block_200:
|
||||
block_210:
|
||||
{
|
||||
uint8_t x_163;
|
||||
lean_dec(x_162);
|
||||
|
|
@ -38840,43 +38885,42 @@ x_164 = lean_ctor_get_uint8(x_155, sizeof(void*)*1 + 3);
|
|||
lean_dec(x_155);
|
||||
if (x_164 == 0)
|
||||
{
|
||||
uint8_t x_165; lean_object* x_166; lean_object* x_167;
|
||||
uint8_t x_165;
|
||||
x_165 = l_Array_isEmpty___rarg(x_161);
|
||||
if (x_165 == 0)
|
||||
{
|
||||
uint8_t x_166;
|
||||
x_166 = l_Lean_Expr_isApp(x_3);
|
||||
if (x_166 == 0)
|
||||
{
|
||||
lean_object* x_167; lean_object* x_168;
|
||||
lean_dec(x_160);
|
||||
x_167 = lean_array_get_size(x_161);
|
||||
lean_dec(x_161);
|
||||
x_168 = l___private_Init_Lean_Meta_ExprDefEq_17__processConstApprox(x_1, x_167, x_3, x_6, x_159);
|
||||
return x_168;
|
||||
}
|
||||
else
|
||||
{
|
||||
uint8_t x_169; lean_object* x_170; lean_object* x_171;
|
||||
lean_dec(x_161);
|
||||
lean_dec(x_6);
|
||||
lean_dec(x_3);
|
||||
lean_dec(x_1);
|
||||
x_165 = 0;
|
||||
x_166 = lean_box(x_165);
|
||||
x_169 = 0;
|
||||
x_170 = lean_box(x_169);
|
||||
if (lean_is_scalar(x_160)) {
|
||||
x_167 = lean_alloc_ctor(0, 2, 0);
|
||||
x_171 = lean_alloc_ctor(0, 2, 0);
|
||||
} else {
|
||||
x_167 = x_160;
|
||||
x_171 = x_160;
|
||||
}
|
||||
lean_ctor_set(x_167, 0, x_166);
|
||||
lean_ctor_set(x_167, 1, x_159);
|
||||
return x_167;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_168; lean_object* x_169;
|
||||
lean_dec(x_160);
|
||||
x_168 = lean_array_get_size(x_161);
|
||||
lean_dec(x_161);
|
||||
x_169 = l___private_Init_Lean_Meta_ExprDefEq_17__processConstApprox(x_1, x_168, x_3, x_6, x_159);
|
||||
return x_169;
|
||||
lean_ctor_set(x_171, 0, x_170);
|
||||
lean_ctor_set(x_171, 1, x_159);
|
||||
return x_171;
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
uint8_t x_170;
|
||||
x_170 = l_Lean_Expr_isApp(x_3);
|
||||
if (x_170 == 0)
|
||||
{
|
||||
uint8_t x_171;
|
||||
x_171 = lean_ctor_get_uint8(x_155, sizeof(void*)*1 + 3);
|
||||
lean_dec(x_155);
|
||||
if (x_171 == 0)
|
||||
{
|
||||
uint8_t x_172; lean_object* x_173; lean_object* x_174;
|
||||
lean_dec(x_161);
|
||||
lean_dec(x_6);
|
||||
|
|
@ -38893,6 +38937,7 @@ lean_ctor_set(x_174, 0, x_173);
|
|||
lean_ctor_set(x_174, 1, x_159);
|
||||
return x_174;
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_175; lean_object* x_176;
|
||||
|
|
@ -38905,122 +38950,173 @@ return x_176;
|
|||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_177;
|
||||
uint8_t x_177;
|
||||
x_177 = l_Lean_Expr_isApp(x_3);
|
||||
if (x_177 == 0)
|
||||
{
|
||||
uint8_t x_178;
|
||||
x_178 = lean_ctor_get_uint8(x_155, sizeof(void*)*1 + 3);
|
||||
lean_dec(x_155);
|
||||
if (x_178 == 0)
|
||||
{
|
||||
uint8_t x_179;
|
||||
x_179 = l_Array_isEmpty___rarg(x_161);
|
||||
if (x_179 == 0)
|
||||
{
|
||||
lean_object* x_180; lean_object* x_181;
|
||||
lean_dec(x_160);
|
||||
x_180 = lean_array_get_size(x_161);
|
||||
lean_dec(x_161);
|
||||
x_181 = l___private_Init_Lean_Meta_ExprDefEq_17__processConstApprox(x_1, x_180, x_3, x_6, x_159);
|
||||
return x_181;
|
||||
}
|
||||
else
|
||||
{
|
||||
uint8_t x_182; lean_object* x_183; lean_object* x_184;
|
||||
lean_dec(x_161);
|
||||
lean_dec(x_6);
|
||||
lean_dec(x_3);
|
||||
lean_dec(x_1);
|
||||
x_182 = 0;
|
||||
x_183 = lean_box(x_182);
|
||||
if (lean_is_scalar(x_160)) {
|
||||
x_184 = lean_alloc_ctor(0, 2, 0);
|
||||
} else {
|
||||
x_184 = x_160;
|
||||
}
|
||||
lean_ctor_set(x_184, 0, x_183);
|
||||
lean_ctor_set(x_184, 1, x_159);
|
||||
return x_184;
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_185; lean_object* x_186;
|
||||
lean_dec(x_160);
|
||||
x_185 = lean_array_get_size(x_161);
|
||||
lean_dec(x_161);
|
||||
x_186 = l___private_Init_Lean_Meta_ExprDefEq_17__processConstApprox(x_1, x_185, x_3, x_6, x_159);
|
||||
return x_186;
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_187;
|
||||
lean_dec(x_160);
|
||||
lean_inc(x_6);
|
||||
lean_inc(x_3);
|
||||
lean_inc(x_1);
|
||||
x_177 = l___private_Init_Lean_Meta_ExprDefEq_14__processAssignmentFOApprox___main(x_1, x_161, x_3, x_6, x_159);
|
||||
if (lean_obj_tag(x_177) == 0)
|
||||
x_187 = l___private_Init_Lean_Meta_ExprDefEq_14__processAssignmentFOApprox___main(x_1, x_161, x_3, x_6, x_159);
|
||||
if (lean_obj_tag(x_187) == 0)
|
||||
{
|
||||
lean_object* x_178; uint8_t x_179;
|
||||
x_178 = lean_ctor_get(x_177, 0);
|
||||
lean_inc(x_178);
|
||||
x_179 = lean_unbox(x_178);
|
||||
if (x_179 == 0)
|
||||
lean_object* x_188; uint8_t x_189;
|
||||
x_188 = lean_ctor_get(x_187, 0);
|
||||
lean_inc(x_188);
|
||||
x_189 = lean_unbox(x_188);
|
||||
if (x_189 == 0)
|
||||
{
|
||||
uint8_t x_180;
|
||||
lean_dec(x_178);
|
||||
x_180 = lean_ctor_get_uint8(x_155, sizeof(void*)*1 + 3);
|
||||
uint8_t x_190;
|
||||
lean_dec(x_188);
|
||||
x_190 = lean_ctor_get_uint8(x_155, sizeof(void*)*1 + 3);
|
||||
lean_dec(x_155);
|
||||
if (x_180 == 0)
|
||||
if (x_190 == 0)
|
||||
{
|
||||
uint8_t x_181;
|
||||
uint8_t x_191;
|
||||
lean_dec(x_161);
|
||||
lean_dec(x_6);
|
||||
lean_dec(x_3);
|
||||
lean_dec(x_1);
|
||||
x_181 = !lean_is_exclusive(x_177);
|
||||
if (x_181 == 0)
|
||||
x_191 = !lean_is_exclusive(x_187);
|
||||
if (x_191 == 0)
|
||||
{
|
||||
lean_object* x_182; uint8_t x_183; lean_object* x_184;
|
||||
x_182 = lean_ctor_get(x_177, 0);
|
||||
lean_dec(x_182);
|
||||
x_183 = 0;
|
||||
x_184 = lean_box(x_183);
|
||||
lean_ctor_set(x_177, 0, x_184);
|
||||
return x_177;
|
||||
lean_object* x_192; uint8_t x_193; lean_object* x_194;
|
||||
x_192 = lean_ctor_get(x_187, 0);
|
||||
lean_dec(x_192);
|
||||
x_193 = 0;
|
||||
x_194 = lean_box(x_193);
|
||||
lean_ctor_set(x_187, 0, x_194);
|
||||
return x_187;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_185; uint8_t x_186; lean_object* x_187; lean_object* x_188;
|
||||
x_185 = lean_ctor_get(x_177, 1);
|
||||
lean_inc(x_185);
|
||||
lean_dec(x_177);
|
||||
x_186 = 0;
|
||||
x_187 = lean_box(x_186);
|
||||
x_188 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_188, 0, x_187);
|
||||
lean_ctor_set(x_188, 1, x_185);
|
||||
return x_188;
|
||||
lean_object* x_195; uint8_t x_196; lean_object* x_197; lean_object* x_198;
|
||||
x_195 = lean_ctor_get(x_187, 1);
|
||||
lean_inc(x_195);
|
||||
lean_dec(x_187);
|
||||
x_196 = 0;
|
||||
x_197 = lean_box(x_196);
|
||||
x_198 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_198, 0, x_197);
|
||||
lean_ctor_set(x_198, 1, x_195);
|
||||
return x_198;
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_189; lean_object* x_190; lean_object* x_191;
|
||||
x_189 = lean_ctor_get(x_177, 1);
|
||||
lean_inc(x_189);
|
||||
lean_dec(x_177);
|
||||
x_190 = lean_array_get_size(x_161);
|
||||
lean_object* x_199; lean_object* x_200; lean_object* x_201;
|
||||
x_199 = lean_ctor_get(x_187, 1);
|
||||
lean_inc(x_199);
|
||||
lean_dec(x_187);
|
||||
x_200 = lean_array_get_size(x_161);
|
||||
lean_dec(x_161);
|
||||
x_191 = l___private_Init_Lean_Meta_ExprDefEq_17__processConstApprox(x_1, x_190, x_3, x_6, x_189);
|
||||
return x_191;
|
||||
x_201 = l___private_Init_Lean_Meta_ExprDefEq_17__processConstApprox(x_1, x_200, x_3, x_6, x_199);
|
||||
return x_201;
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
uint8_t x_192;
|
||||
uint8_t x_202;
|
||||
lean_dec(x_161);
|
||||
lean_dec(x_155);
|
||||
lean_dec(x_6);
|
||||
lean_dec(x_3);
|
||||
lean_dec(x_1);
|
||||
x_192 = !lean_is_exclusive(x_177);
|
||||
if (x_192 == 0)
|
||||
x_202 = !lean_is_exclusive(x_187);
|
||||
if (x_202 == 0)
|
||||
{
|
||||
lean_object* x_193;
|
||||
x_193 = lean_ctor_get(x_177, 0);
|
||||
lean_dec(x_193);
|
||||
return x_177;
|
||||
lean_object* x_203;
|
||||
x_203 = lean_ctor_get(x_187, 0);
|
||||
lean_dec(x_203);
|
||||
return x_187;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_194; lean_object* x_195;
|
||||
x_194 = lean_ctor_get(x_177, 1);
|
||||
lean_inc(x_194);
|
||||
lean_dec(x_177);
|
||||
x_195 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_195, 0, x_178);
|
||||
lean_ctor_set(x_195, 1, x_194);
|
||||
return x_195;
|
||||
lean_object* x_204; lean_object* x_205;
|
||||
x_204 = lean_ctor_get(x_187, 1);
|
||||
lean_inc(x_204);
|
||||
lean_dec(x_187);
|
||||
x_205 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_205, 0, x_188);
|
||||
lean_ctor_set(x_205, 1, x_204);
|
||||
return x_205;
|
||||
}
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
uint8_t x_196;
|
||||
uint8_t x_206;
|
||||
lean_dec(x_161);
|
||||
lean_dec(x_155);
|
||||
lean_dec(x_6);
|
||||
lean_dec(x_3);
|
||||
lean_dec(x_1);
|
||||
x_196 = !lean_is_exclusive(x_177);
|
||||
if (x_196 == 0)
|
||||
x_206 = !lean_is_exclusive(x_187);
|
||||
if (x_206 == 0)
|
||||
{
|
||||
return x_177;
|
||||
return x_187;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_197; lean_object* x_198; lean_object* x_199;
|
||||
x_197 = lean_ctor_get(x_177, 0);
|
||||
x_198 = lean_ctor_get(x_177, 1);
|
||||
lean_inc(x_198);
|
||||
lean_inc(x_197);
|
||||
lean_dec(x_177);
|
||||
x_199 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_199, 0, x_197);
|
||||
lean_ctor_set(x_199, 1, x_198);
|
||||
return x_199;
|
||||
lean_object* x_207; lean_object* x_208; lean_object* x_209;
|
||||
x_207 = lean_ctor_get(x_187, 0);
|
||||
x_208 = lean_ctor_get(x_187, 1);
|
||||
lean_inc(x_208);
|
||||
lean_inc(x_207);
|
||||
lean_dec(x_187);
|
||||
x_209 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_209, 0, x_207);
|
||||
lean_ctor_set(x_209, 1, x_208);
|
||||
return x_209;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
@ -39029,7 +39125,7 @@ return x_199;
|
|||
}
|
||||
else
|
||||
{
|
||||
uint8_t x_267;
|
||||
uint8_t x_287;
|
||||
lean_dec(x_155);
|
||||
lean_dec(x_6);
|
||||
lean_dec(x_5);
|
||||
|
|
@ -39037,23 +39133,23 @@ lean_dec(x_4);
|
|||
lean_dec(x_3);
|
||||
lean_dec(x_2);
|
||||
lean_dec(x_1);
|
||||
x_267 = !lean_is_exclusive(x_157);
|
||||
if (x_267 == 0)
|
||||
x_287 = !lean_is_exclusive(x_157);
|
||||
if (x_287 == 0)
|
||||
{
|
||||
return x_157;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_268; lean_object* x_269; lean_object* x_270;
|
||||
x_268 = lean_ctor_get(x_157, 0);
|
||||
x_269 = lean_ctor_get(x_157, 1);
|
||||
lean_inc(x_269);
|
||||
lean_inc(x_268);
|
||||
lean_object* x_288; lean_object* x_289; lean_object* x_290;
|
||||
x_288 = lean_ctor_get(x_157, 0);
|
||||
x_289 = lean_ctor_get(x_157, 1);
|
||||
lean_inc(x_289);
|
||||
lean_inc(x_288);
|
||||
lean_dec(x_157);
|
||||
x_270 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_270, 0, x_268);
|
||||
lean_ctor_set(x_270, 1, x_269);
|
||||
return x_270;
|
||||
x_290 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_290, 0, x_288);
|
||||
lean_ctor_set(x_290, 1, x_289);
|
||||
return x_290;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue