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

chore: remove Fix.lean

Browse source 
see #1208
This commit is contained in:
Leonardo de Moura 2022-06-16 15:30:47 -07:00
parent 9e7a6fa085
commit 8d9428261e
4 changed files with 0 additions and 233 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/Init.lean
View file

@ -15,7 +15,6 @@ import Init.WFTactics
import Init.Data
import Init.System
import Init.Util
import Init.Fix
import Init.Meta
import Init.NotationExtra
import Init.SimpLemmas

80
src/Init/Fix.lean
View file

@ -1,80 +0,0 @@
/-
Copyright (c) 2019 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
prelude
import Init.Data.UInt
universe u
def bfix1 {α β : Type u} (base : α → β) (rec : (α → β) → α → β) : Nat → α → β
| 0, a => base a
| n+1, a => rec (bfix1 base rec n) a
@[extern c inline "lean_fixpoint(#4, #5)"]
def fixCore1 {α β : Type u} (base : @& (α → β)) (rec : (α → β) → α → β) : α → β :=
bfix1 base rec USize.size
@[inline] def fixCore {α β : Type u} (base : @& (α → β)) (rec : (α → β) → α → β) : α → β :=
fixCore1 base rec
@[inline] def fix1 {α β : Type u} [Inhabited β] (rec : (α → β) → α → β) : α → β :=
fixCore1 (fun _ => default) rec
@[inline] def fix {α β : Type u} [Inhabited β] (rec : (α → β) → α → β) : α → β :=
fixCore1 (fun _ => default) rec
def bfix2 {α₁ α₂ β : Type u} (base : α₁ → α₂ → β) (rec : (α₁ → α₂ → β) → α₁ → α₂ → β) : Nat → α₁ → α₂ → β
| 0, a₁, a₂ => base a₁ a₂
| n+1, a₁, a₂ => rec (bfix2 base rec n) a₁ a₂
@[extern c inline "lean_fixpoint2(#5, #6, #7)"]
def fixCore2 {α₁ α₂ β : Type u} (base : α₁ → α₂ → β) (rec : (α₁ → α₂ → β) → α₁ → α₂ → β) : α₁ → α₂ → β :=
bfix2 base rec USize.size
@[inline] def fix2 {α₁ α₂ β : Type u} [Inhabited β] (rec : (α₁ → α₂ → β) → α₁ → α₂ → β) : α₁ → α₂ → β :=
fixCore2 (fun _ _ => default) rec
def bfix3 {α₁ α₂ α₃ β : Type u} (base : α₁ → α₂ → α₃ → β) (rec : (α₁ → α₂ → α₃ → β) → α₁ → α₂ → α₃ → β) : Nat → α₁ → α₂ → α₃ → β
| 0, a₁, a₂, a₃ => base a₁ a₂ a₃
| n+1, a₁, a₂, a₃ => rec (bfix3 base rec n) a₁ a₂ a₃
@[extern c inline "lean_fixpoint3(#6, #7, #8, #9)"]
def fixCore3 {α₁ α₂ α₃ β : Type u} (base : α₁ → α₂ → α₃ → β) (rec : (α₁ → α₂ → α₃ → β) → α₁ → α₂ → α₃ → β) : α₁ → α₂ → α₃ → β :=
bfix3 base rec USize.size
@[inline] def fix3 {α₁ α₂ α₃ β : Type u} [Inhabited β] (rec : (α₁ → α₂ → α₃ → β) → α₁ → α₂ → α₃ → β) : α₁ → α₂ → α₃ → β :=
fixCore3 (fun _ _ _ => default) rec
def bfix4 {α₁ α₂ α₃ α₄ β : Type u} (base : α₁ → α₂ → α₃ → α₄ → β) (rec : (α₁ → α₂ → α₃ → α₄ → β) → α₁ → α₂ → α₃ → α₄ → β) : Nat → α₁ → α₂ → α₃ → α₄ → β
| 0, a₁, a₂, a₃, a₄ => base a₁ a₂ a₃ a₄
| n+1, a₁, a₂, a₃, a₄ => rec (bfix4 base rec n) a₁ a₂ a₃ a₄
@[extern c inline "lean_fixpoint4(#7, #8, #9, #10, #11)"]
def fixCore4 {α₁ α₂ α₃ α₄ β : Type u} (base : α₁ → α₂ → α₃ → α₄ → β) (rec : (α₁ → α₂ → α₃ → α₄ → β) → α₁ → α₂ → α₃ → α₄ → β) : α₁ → α₂ → α₃ → α₄ → β :=
bfix4 base rec USize.size
@[inline] def fix4 {α₁ α₂ α₃ α₄ β : Type u} [Inhabited β] (rec : (α₁ → α₂ → α₃ → α₄ → β) → α₁ → α₂ → α₃ → α₄ → β) : α₁ → α₂ → α₃ → α₄ → β :=
fixCore4 (fun _ _ _ _ => default) rec
def bfix5 {α₁ α₂ α₃ α₄ α₅ β : Type u} (base : α₁ → α₂ → α₃ → α₄ → α₅ → β) (rec : (α₁ → α₂ → α₃ → α₄ → α₅ → β) → α₁ → α₂ → α₃ → α₄ → α₅ → β) : Nat → α₁ → α₂ → α₃ → α₄ → α₅ → β
| 0, a₁, a₂, a₃, a₄, a₅ => base a₁ a₂ a₃ a₄ a₅
| n+1, a₁, a₂, a₃, a₄, a₅ => rec (bfix5 base rec n) a₁ a₂ a₃ a₄ a₅
@[extern c inline "lean_fixpoint5(#8, #9, #10, #11, #12, #13)"]
def fixCore5 {α₁ α₂ α₃ α₄ α₅ β : Type u} (base : α₁ → α₂ → α₃ → α₄ → α₅ → β) (rec : (α₁ → α₂ → α₃ → α₄ → α₅ → β) → α₁ → α₂ → α₃ → α₄ → α₅ → β) : α₁ → α₂ → α₃ → α₄ → α₅ → β :=
bfix5 base rec USize.size
@[inline] def fix5 {α₁ α₂ α₃ α₄ α₅ β : Type u} [Inhabited β] (rec : (α₁ → α₂ → α₃ → α₄ → α₅ → β) → α₁ → α₂ → α₃ → α₄ → α₅ → β) : α₁ → α₂ → α₃ → α₄ → α₅ → β :=
fixCore5 (fun _ _ _ _ _ => default) rec
def bfix6 {α₁ α₂ α₃ α₄ α₅ α₆ β : Type u} (base : α₁ → α₂ → α₃ → α₄ → α₅ → α₆ → β) (rec : (α₁ → α₂ → α₃ → α₄ → α₅ → α₆ → β) → α₁ → α₂ → α₃ → α₄ → α₅ → α₆ → β) : Nat → α₁ → α₂ → α₃ → α₄ → α₅ → α₆ → β
| 0, a₁, a₂, a₃, a₄, a₅, a₆ => base a₁ a₂ a₃ a₄ a₅ a₆
| n+1, a₁, a₂, a₃, a₄, a₅, a₆ => rec (bfix6 base rec n) a₁ a₂ a₃ a₄ a₅ a₆
@[extern c inline "lean_fixpoint6(#9, #10, #11, #12, #13, #14, #15)"]
def fixCore6 {α₁ α₂ α₃ α₄ α₅ α₆ β : Type u} (base : α₁ → α₂ → α₃ → α₄ → α₅ → α₆ → β) (rec : (α₁ → α₂ → α₃ → α₄ → α₅ → α₆ → β) → α₁ → α₂ → α₃ → α₄ → α₅ → α₆ → β) : α₁ → α₂ → α₃ → α₄ → α₅ → α₆ → β :=
bfix6 base rec USize.size
@[inline] def fix6 {α₁ α₂ α₃ α₄ α₅ α₆ β : Type u} [Inhabited β] (rec : (α₁ → α₂ → α₃ → α₄ → α₅ → α₆ → β) → α₁ → α₂ → α₃ → α₄ → α₅ → α₆ → β) : α₁ → α₂ → α₃ → α₄ → α₅ → α₆ → β :=
fixCore6 (fun _ _ _ _ _ _ => default) rec

101
src/runtime/object.cpp
View file

@ -351,107 +351,6 @@ extern "C" LEAN_EXPORT b_obj_res lean_thunk_get_core(b_obj_arg t) {
}
}
// =======================================
// Fixpoint
static inline object * ptr_to_weak_ptr(object * p) {
return reinterpret_cast<object*>(reinterpret_cast<uintptr_t>(p) | 1);
}
static inline object * weak_ptr_to_ptr(object * w) {
return reinterpret_cast<object*>((reinterpret_cast<uintptr_t>(w) >> 1) << 1);
}
obj_res fixpoint_aux(obj_arg rec, obj_arg weak_k, obj_arg a) {
object * k = weak_ptr_to_ptr(weak_k);
lean_inc(k);
return lean_apply_2(rec, k, a);
}
extern "C" LEAN_EXPORT obj_res lean_fixpoint(obj_arg rec, obj_arg a) {
object * k = lean_alloc_closure((void*)fixpoint_aux, 3, 2);
lean_inc(rec);
lean_closure_set(k, 0, rec);
lean_closure_set(k, 1, ptr_to_weak_ptr(k));
object * r = lean_apply_2(rec, k, a);
return r;
}
obj_res fixpoint_aux2(obj_arg rec, obj_arg weak_k, obj_arg a1, obj_arg a2) {
object * k = weak_ptr_to_ptr(weak_k);
lean_inc(k);
return lean_apply_3(rec, k, a1, a2);
}
extern "C" LEAN_EXPORT obj_res lean_fixpoint2(obj_arg rec, obj_arg a1, obj_arg a2) {
object * k = lean_alloc_closure((void*)fixpoint_aux2, 4, 2);
lean_inc(rec);
lean_closure_set(k, 0, rec);
lean_closure_set(k, 1, ptr_to_weak_ptr(k));
object * r = lean_apply_3(rec, k, a1, a2);
return r;
}
obj_res fixpoint_aux3(obj_arg rec, obj_arg weak_k, obj_arg a1, obj_arg a2, obj_arg a3) {
object * k = weak_ptr_to_ptr(weak_k);
lean_inc(k);
return lean_apply_4(rec, k, a1, a2, a3);
}
extern "C" LEAN_EXPORT obj_res lean_fixpoint3(obj_arg rec, obj_arg a1, obj_arg a2, obj_arg a3) {
object * k = lean_alloc_closure((void*)fixpoint_aux3, 5, 2);
lean_inc(rec);
lean_closure_set(k, 0, rec);
lean_closure_set(k, 1, ptr_to_weak_ptr(k));
object * r = lean_apply_4(rec, k, a1, a2, a3);
return r;
}
obj_res fixpoint_aux4(obj_arg rec, obj_arg weak_k, obj_arg a1, obj_arg a2, obj_arg a3, obj_arg a4) {
object * k = weak_ptr_to_ptr(weak_k);
lean_inc(k);
return lean_apply_5(rec, k, a1, a2, a3, a4);
}
extern "C" LEAN_EXPORT obj_res lean_fixpoint4(obj_arg rec, obj_arg a1, obj_arg a2, obj_arg a3, obj_arg a4) {
object * k = lean_alloc_closure((void*)fixpoint_aux4, 6, 2);
lean_inc(rec);
lean_closure_set(k, 0, rec);
lean_closure_set(k, 1, ptr_to_weak_ptr(k));
object * r = lean_apply_5(rec, k, a1, a2, a3, a4);
return r;
}
obj_res fixpoint_aux5(obj_arg rec, obj_arg weak_k, obj_arg a1, obj_arg a2, obj_arg a3, obj_arg a4, obj_arg a5) {
object * k = weak_ptr_to_ptr(weak_k);
lean_inc(k);
return lean_apply_6(rec, k, a1, a2, a3, a4, a5);
}
extern "C" LEAN_EXPORT obj_res lean_fixpoint5(obj_arg rec, obj_arg a1, obj_arg a2, obj_arg a3, obj_arg a4, obj_arg a5) {
object * k = lean_alloc_closure((void*)fixpoint_aux5, 7, 2);
lean_inc(rec);
lean_closure_set(k, 0, rec);
lean_closure_set(k, 1, ptr_to_weak_ptr(k));
object * r = lean_apply_6(rec, k, a1, a2, a3, a4, a5);
return r;
}
obj_res fixpoint_aux6(obj_arg rec, obj_arg weak_k, obj_arg a1, obj_arg a2, obj_arg a3, obj_arg a4, obj_arg a5, obj_arg a6) {
object * k = weak_ptr_to_ptr(weak_k);
lean_inc(k);
return lean_apply_7(rec, k, a1, a2, a3, a4, a5, a6);
}
extern "C" LEAN_EXPORT obj_res lean_fixpoint6(obj_arg rec, obj_arg a1, obj_arg a2, obj_arg a3, obj_arg a4, obj_arg a5, obj_arg a6) {
object * k = lean_alloc_closure((void*)fixpoint_aux6, 8, 2);
lean_inc(rec);
lean_closure_set(k, 0, rec);
lean_closure_set(k, 1, ptr_to_weak_ptr(k));
object * r = lean_apply_7(rec, k, a1, a2, a3, a4, a5, a6);
return r;
}
// =======================================
// Mark Persistent

51
tests/lean/interactive/533.lean.expected.out
View file

@ -24,57 +24,6 @@
{"label": "Functor",
"kind": 7,
"detail": "(Type u → Type v) → Type (max (u + 1) v)"},
{"label": "fix",
"kind": 3,
"detail": "[inst : Inhabited β] → ((α → β) → α → β) → α → β"},
{"label": "fix1",
"kind": 3,
"detail": "[inst : Inhabited β] → ((α → β) → α → β) → α → β"},
{"label": "fix2",
"kind": 3,
"detail":
"[inst : Inhabited β] → ((α₁ → α₂ → β) → α₁ → α₂ → β) → α₁ → α₂ → β"},
{"label": "fix3",
"kind": 3,
"detail":
"[inst : Inhabited β] → ((α₁ → α₂ → α₃ → β) → α₁ → α₂ → α₃ → β) → α₁ → α₂ → α₃ → β"},
{"label": "fix4",
"kind": 3,
"detail":
"[inst : Inhabited β] → ((α₁ → α₂ → α₃ → α₄ → β) → α₁ → α₂ → α₃ → α₄ → β) → α₁ → α₂ → α₃ → α₄ → β"},
{"label": "fix5",
"kind": 3,
"detail":
"[inst : Inhabited β] → ((α₁ → α₂ → α₃ → α₄ → α₅ → β) → α₁ → α₂ → α₃ → α₄ → α₅ → β) → α₁ → α₂ → α₃ → α₄ → α₅ → β"},
{"label": "fix6",
"kind": 3,
"detail":
"[inst : Inhabited β] →\n ((α₁ → α₂ → α₃ → α₄ → α₅ → α₆ → β) → α₁ → α₂ → α₃ → α₄ → α₅ → α₆ → β) → α₁ → α₂ → α₃ → α₄ → α₅ → α₆ → β"},
{"label": "fixCore",
"kind": 3,
"detail": "(α → β) → ((α → β) → α → β) → α → β"},
{"label": "fixCore1",
"kind": 3,
"detail": "(α → β) → ((α → β) → α → β) → α → β"},
{"label": "fixCore2",
"kind": 3,
"detail": "(α₁ → α₂ → β) → ((α₁ → α₂ → β) → α₁ → α₂ → β) → α₁ → α₂ → β"},
{"label": "fixCore3",
"kind": 3,
"detail":
"(α₁ → α₂ → α₃ → β) → ((α₁ → α₂ → α₃ → β) → α₁ → α₂ → α₃ → β) → α₁ → α₂ → α₃ → β"},
{"label": "fixCore4",
"kind": 3,
"detail":
"(α₁ → α₂ → α₃ → α₄ → β) → ((α₁ → α₂ → α₃ → α₄ → β) → α₁ → α₂ → α₃ → α₄ → β) → α₁ → α₂ → α₃ → α₄ → β"},
{"label": "fixCore5",
"kind": 3,
"detail":
"(α₁ → α₂ → α₃ → α₄ → α₅ → β) → ((α₁ → α₂ → α₃ → α₄ → α₅ → β) → α₁ → α₂ → α₃ → α₄ → α₅ → β) → α₁ → α₂ → α₃ → α₄ → α₅ → β"},
{"label": "fixCore6",
"kind": 3,
"detail":
"(α₁ → α₂ → α₃ → α₄ → α₅ → α₆ → β) →\n ((α₁ → α₂ → α₃ → α₄ → α₅ → α₆ → β) → α₁ → α₂ → α₃ → α₄ → α₅ → α₆ → β) → α₁ → α₂ → α₃ → α₄ → α₅ → α₆ → β"},
{"label": "failure",
"kind": 5,
"detail": "[self : Alternative f] → {α : Type u} → f α"},