From efb859013e237f498abf5758e37a55a67d152acc Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 13 Apr 2022 09:37:35 -0700 Subject: [PATCH] chore: ignore `{}` annotations at `mk_projections` --- src/Lean/Elab/Structure.lean | 14 +++------ src/library/constructions/projection.cpp | 14 ++++----- src/library/constructions/projection.h | 6 +--- tests/lean/run/bigop.lean | 38 ++++++++++++------------ 4 files changed, 29 insertions(+), 43 deletions(-) diff --git a/src/Lean/Elab/Structure.lean b/src/Lean/Elab/Structure.lean index f7b5fa1c81..81d4796742 100644 --- a/src/Lean/Elab/Structure.lean +++ b/src/Lean/Elab/Structure.lean @@ -82,11 +82,6 @@ def StructFieldInfo.isSubobject (info : StructFieldInfo) : Bool := | StructFieldKind.subobject => true | _ => false -/- Auxiliary declaration for `mkProjections` -/ -structure ProjectionInfo where - declName : Name - inferMod : Bool - structure ElabStructResult where decl : Declaration projInfos : List ProjectionInfo @@ -687,9 +682,9 @@ private def mkCtor (view : StructView) (levelParams : List Name) (params : Array pure { name := view.ctor.declName, type } @[extern "lean_mk_projections"] -private constant mkProjections (env : Environment) (structName : Name) (projs : List ProjectionInfo) (isClass : Bool) : Except KernelException Environment +private constant mkProjections (env : Environment) (structName : Name) (projs : List Name) (isClass : Bool) : Except KernelException Environment -private def addProjections (structName : Name) (projs : List ProjectionInfo) (isClass : Bool) : TermElabM Unit := do +private def addProjections (structName : Name) (projs : List Name) (isClass : Bool) : TermElabM Unit := do let env ← getEnv match mkProjections env structName projs isClass with | Except.ok env => setEnv env @@ -817,9 +812,8 @@ private def elabStructureView (view : StructView) : TermElabM Unit := do let decl := Declaration.inductDecl levelParams params.size [indType] view.modifiers.isUnsafe Term.ensureNoUnassignedMVars decl addDecl decl - let projInfos := (fieldInfos.filter fun (info : StructFieldInfo) => !info.isFromParent).toList.map fun (info : StructFieldInfo) => - { declName := info.declName, inferMod := info.inferMod : ProjectionInfo } - addProjections view.declName projInfos view.isClass + let projNames := (fieldInfos.filter fun (info : StructFieldInfo) => !info.isFromParent).toList.map fun (info : StructFieldInfo) => info.declName + addProjections view.declName projNames view.isClass registerStructure view.declName fieldInfos mkAuxConstructions view.declName let instParents ← fieldInfos.filterM fun info => do diff --git a/src/library/constructions/projection.cpp b/src/library/constructions/projection.cpp index 2add547836..b3ac5414af 100644 --- a/src/library/constructions/projection.cpp +++ b/src/library/constructions/projection.cpp @@ -30,8 +30,7 @@ static bool is_prop(expr type) { return is_sort(type) && is_zero(sort_level(type)); } -environment mk_projections(environment const & env, name const & n, buffer const & proj_names, - buffer const & infer_kinds, bool inst_implicit) { +environment mk_projections(environment const & env, name const & n, buffer const & proj_names, bool inst_implicit) { lean_assert(proj_names.size() == infer_kinds.size()); local_ctx lctx; name_generator ngen = mk_constructions_name_generator(); @@ -94,7 +93,7 @@ environment mk_projections(environment const & env, name const & n, buffer proj_args.append(params); proj_args.push_back(c); expr proj_type = lctx.mk_pi(proj_args, result_type); - proj_type = infer_implicit_params(proj_type, nparams, infer_kinds[i]); + proj_type = infer_implicit_params(proj_type, nparams, implicit_infer_kind::RelaxedImplicit); expr proj_val = mk_proj(n, i, c); proj_val = lctx.mk_lambda(proj_args, proj_val); declaration new_d = mk_definition_inferring_unsafe(env, proj_name, lvl_params, proj_type, proj_val, @@ -114,15 +113,12 @@ environment mk_projections(environment const & env, name const & n, buffer extern "C" LEAN_EXPORT object * lean_mk_projections(object * env, object * struct_name, object * proj_infos, uint8 inst_implicit) { environment new_env(env); name n(struct_name); - list_ref ps(proj_infos); + list_ref ps(proj_infos); buffer proj_names; - buffer infer_kinds; for (auto p : ps) { - proj_names.push_back(cnstr_get_ref_t(p, 0)); - bool infer_mod = cnstr_get_uint8(p.raw(), sizeof(object*)); - infer_kinds.push_back(infer_mod ? implicit_infer_kind::Implicit : implicit_infer_kind::RelaxedImplicit); + proj_names.push_back(p); } - return catch_kernel_exceptions([&]() { return mk_projections(new_env, n, proj_names, infer_kinds, inst_implicit != 0); }); + return catch_kernel_exceptions([&]() { return mk_projections(new_env, n, proj_names, inst_implicit != 0); }); } void initialize_def_projection() { diff --git a/src/library/constructions/projection.h b/src/library/constructions/projection.h index 1f88a6e3fc..95abd81b3d 100644 --- a/src/library/constructions/projection.h +++ b/src/library/constructions/projection.h @@ -12,15 +12,11 @@ namespace lean { /** \brief Create projections operators for the structure named \c n. The procedure assumes \c n is a structure. - The argument \c infer_kinds specifies the implicit argument inference strategies used for the - structure parameters. - If \c inst_implicit == true, then the structure argument of the projection is decorated as "instance implicit" [s : n] */ -environment mk_projections(environment const & env, name const & n, buffer const & proj_names, - buffer const & infer_kinds, bool inst_implicit = false); +environment mk_projections(environment const & env, name const & n, buffer const & proj_names, bool inst_implicit = false); void initialize_def_projection(); void finalize_def_projection(); diff --git a/tests/lean/run/bigop.lean b/tests/lean/run/bigop.lean index 4d727e53cb..0ee92ab6f5 100644 --- a/tests/lean/run/bigop.lean +++ b/tests/lean/run/bigop.lean @@ -3,42 +3,42 @@ def Sequence (α : Type) := List α def BigBody (β α) := α × (β → β → β) × Bool × β def applyBig {α β : Type} (body : BigBody β α) (x : β) : β := -let (_, op, b, v) := body; -if b then op v x else x + let (_, op, b, v) := body; + if b then op v x else x def reducebig {α β : Type} (idx : β) (r : Sequence α) (body : α → BigBody β α) : β := -r.foldr (applyBig ∘ body) idx + r.foldr (applyBig ∘ body) idx def bigop := @reducebig partial def iota : Nat → Nat → List Nat -| m, 0 => [] -| m, n+1 => m :: iota (m+1) n + | m, 0 => [] + | m, n+1 => m :: iota (m+1) n def index_iota (m n : Nat) := iota m (n - m) -class Enumerable (α : Type) := -(elems {} : List α) +class Enumerable (α : Type) where + elems : List α -instance : Enumerable Bool := -{ elems := [false, true] } +instance : Enumerable Bool where + elems := [false, true] -- instance {α β} [Enumerable α] [Enumerable β]: Enumerable (α × β) := -- { elems := do let a ← Enumerable.elems α; let b ← Enumerable.elems β; pure (a, b) } partial def finElemsAux (n : Nat) : (i : Nat) → i < n → List (Fin n) -| 0, h => [⟨0, h⟩] -| i+1, h => ⟨i+1, h⟩ :: finElemsAux n i (Nat.lt_of_succ_lt h) + | 0, h => [⟨0, h⟩] + | i+1, h => ⟨i+1, h⟩ :: finElemsAux n i (Nat.lt_of_succ_lt h) partial def finElems : (n : Nat) → List (Fin n) -| 0 => [] -| (n+1) => finElemsAux (n+1) n (Nat.lt_succ_self n) + | 0 => [] + | (n+1) => finElemsAux (n+1) n (Nat.lt_succ_self n) -instance {n} : Enumerable (Fin n) := -{ elems := (finElems n).reverse } +instance {n} : Enumerable (Fin n) where + elems := (finElems n).reverse instance : OfNat (Fin (Nat.succ n)) m := -⟨Fin.ofNat m⟩ + ⟨Fin.ofNat m⟩ -- Declare a new syntax category for "indexing" big operators declare_syntax_cat index @@ -80,9 +80,9 @@ syntax ident ":" term : index syntax ident ":" term "|" term : index -- And new rules macro_rules -| `(_big [$op, $idx] ($i:ident : $type) $F) => `(bigop $idx (Enumerable.elems $type) (fun $i:ident => ($i:ident, $op, true, $F))) -| `(_big [$op, $idx] ($i:ident : $type | $p) $F) => `(bigop $idx (Enumerable.elems $type) (fun $i:ident => ($i:ident, $op, $p, $F))) -| `(_big [$op, $idx] ($i:ident | $p) $F) => `(bigop $idx (Enumerable.elems _) (fun $i:ident => ($i:ident, $op, $p, $F))) +| `(_big [$op, $idx] ($i:ident : $type) $F) => `(bigop $idx (Enumerable.elems (α := $type)) (fun $i:ident => ($i:ident, $op, true, $F))) +| `(_big [$op, $idx] ($i:ident : $type | $p) $F) => `(bigop $idx (Enumerable.elems (α := $type)) (fun $i:ident => ($i:ident, $op, $p, $F))) +| `(_big [$op, $idx] ($i:ident | $p) $F) => `(bigop $idx (Enumerable.elems) (fun $i:ident => ($i:ident, $op, $p, $F))) -- The new syntax is immediately available for all big operators that we have defined def myPred (x : Fin 10) : Bool := true