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 2021-02-04 18:32:52 -08:00
parent 3d4bc9f991
commit ffaef4936c
4 changed files with 4896 additions and 4868 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
stage0/src/Init/Data/Stream.lean generated
View file

@ -61,16 +61,6 @@ protected partial def Stream.forIn [Stream ρ α] [Monad m] (s : ρ) (b : β) (f
instance (priority := low) [Stream ρ α] : ForIn m ρ α where
forIn := Stream.forIn
/- Helper class for using dot-notation with `Stream`s -/
structure StreamOf (ρ : Type u) where
s : ρ
abbrev streamOf (s : ρ) :=
StreamOf.mk s
@[inline] def StreamOf.forIn [Stream ρ α] [Monad m] [Inhabited (m β)] (s : StreamOf ρ) (b : β) (f : α → β → m (ForInStep β)) : m β := do
Stream.forIn s.s b f
instance : ToStream (List α) (List α) where
toStream c := c

4
stage0/src/Lean/Elab/Do.lean generated
View file

@ -1354,7 +1354,7 @@ mutual
let uvarsTuple ← liftMacroM do mkTuple (← uvars.mapM mkIdentFromRef)
if hasReturn forInBodyCodeBlock.code then
let forInBody ← liftMacroM <| destructTuple uvars (← `(r)) forInBody
let forInTerm ← `($(xs).forIn (MProd.mk none $uvarsTuple) fun $x r => let r := r.2; $forInBody)
let forInTerm ← `(forIn (m := $((← read).m)) $(xs) (MProd.mk none $uvarsTuple) fun $x r => let r := r.2; $forInBody)
let auxDo ← `(do let r ← $forInTerm:term;
$uvarsTuple:term := r.2;
match r.1 with
@ -1363,7 +1363,7 @@ mutual
doSeqToCode (getDoSeqElems (getDoSeq auxDo) ++ doElems)
else
let forInBody ← liftMacroM <| destructTuple uvars (← `(r)) forInBody
let forInTerm ← `($(xs).forIn $uvarsTuple fun $x r => $forInBody)
let forInTerm ← `(forIn (m := $((← read).m)) $(xs) $uvarsTuple fun $x r => $forInBody)
if doElems.isEmpty then
let auxDo ← `(do let r ← $forInTerm:term;
$uvarsTuple:term := r;

55
stage0/stdlib/Init/Data/Stream.c generated
View file

@ -14,7 +14,6 @@
extern "C" {
#endif
lean_object* l_instStreamList(lean_object*);
lean_object* l_StreamOf_forIn(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_instStreamProdProd_match__2___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_instToStreamArraySubarray(lean_object*);
lean_object* l_instToStreamRangeRange(lean_object*);
@ -27,7 +26,6 @@ lean_object* lean_nat_add(lean_object*, lean_object*);
lean_object* l_Stream_forIn_visit___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_string_utf8_next(lean_object*, lean_object*);
lean_object* l_instStreamList___rarg(lean_object*);
lean_object* l_streamOf(lean_object*);
lean_object* lean_array_fget(lean_object*, lean_object*);
lean_object* l_instStreamSubstringChar(lean_object*);
lean_object* l_instStreamSubarray(lean_object*);
@ -49,18 +47,14 @@ lean_object* l_Stream_forIn_visit_match__2(lean_object*, lean_object*, lean_obje
lean_object* l_instStreamList_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_instStreamProdProd_match__3(lean_object*, lean_object*, lean_object*);
lean_object* l_Stream_forIn_visit___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_streamOf___rarg(lean_object*);
lean_object* l_instForIn___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Stream_forIn_visit(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Stream_forIn_visit_match__1(lean_object*, lean_object*);
lean_object* l_Stream_forIn___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_instStreamProdProd___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_streamOf___rarg___boxed(lean_object*);
lean_object* l_instToStreamRangeRange___boxed(lean_object*);
lean_object* l_instStreamProdProd_match__1(lean_object*, lean_object*, lean_object*);
lean_object* l_StreamOf_forIn___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Stream_forIn_visit_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_StreamOf_forIn___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Stream_forIn_visit_match__2___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_instToStreamArraySubarray___rarg(lean_object*);
lean_object* l_instToStreamSubarraySubarray___rarg___boxed(lean_object*);
@ -252,55 +246,6 @@ x_4 = lean_alloc_closure((void*)(l_instForIn___rarg), 6, 0);
return x_4;
}
}
lean_object* l_streamOf___rarg(lean_object* x_1) {
_start:
{
lean_inc(x_1);
return x_1;
}
}
lean_object* l_streamOf(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_streamOf___rarg___boxed), 1, 0);
return x_2;
}
}
lean_object* l_streamOf___rarg___boxed(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = l_streamOf___rarg(x_1);
lean_dec(x_1);
return x_2;
}
}
lean_object* l_StreamOf_forIn___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
_start:
{
lean_object* x_7;
x_7 = l_Stream_forIn_visit___rarg(x_1, x_2, x_6, x_4, x_5);
return x_7;
}
}
lean_object* l_StreamOf_forIn(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
lean_object* x_5;
x_5 = lean_alloc_closure((void*)(l_StreamOf_forIn___rarg___boxed), 6, 0);
return x_5;
}
}
lean_object* l_StreamOf_forIn___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
_start:
{
lean_object* x_7;
x_7 = l_StreamOf_forIn___rarg(x_1, x_2, x_3, x_4, x_5, x_6);
lean_dec(x_3);
return x_7;
}
}
lean_object* l_instToStreamListList___rarg(lean_object* x_1) {
_start:
{

9695
stage0/stdlib/Lean/Elab/Do.c generated
View file

File diff suppressed because one or more lines are too long