From 8d9428261efa172376f9a8ba77360270fe6bbdaa Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 16 Jun 2022 15:30:47 -0700 Subject: [PATCH] chore: remove `Fix.lean` see #1208 --- src/Init.lean | 1 - src/Init/Fix.lean | 80 --------------- src/runtime/object.cpp | 101 ------------------- tests/lean/interactive/533.lean.expected.out | 51 ---------- 4 files changed, 233 deletions(-) delete mode 100644 src/Init/Fix.lean diff --git a/src/Init.lean b/src/Init.lean index 4c0ba1f795..d4b4636a62 100644 --- a/src/Init.lean +++ b/src/Init.lean @@ -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 diff --git a/src/Init/Fix.lean b/src/Init/Fix.lean deleted file mode 100644 index 4ce7d894af..0000000000 --- a/src/Init/Fix.lean +++ /dev/null @@ -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 diff --git a/src/runtime/object.cpp b/src/runtime/object.cpp index bdfb0fe3e2..77ff85853c 100644 --- a/src/runtime/object.cpp +++ b/src/runtime/object.cpp @@ -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(reinterpret_cast(p) | 1); -} - -static inline object * weak_ptr_to_ptr(object * w) { - return reinterpret_cast((reinterpret_cast(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 diff --git a/tests/lean/interactive/533.lean.expected.out b/tests/lean/interactive/533.lean.expected.out index 12af05069f..9df0a8c394 100644 --- a/tests/lean/interactive/533.lean.expected.out +++ b/tests/lean/interactive/533.lean.expected.out @@ -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 α"},