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

chore: ignore {} annotations at mk_projections

Browse source
This commit is contained in:
Leonardo de Moura 2022-04-13 09:37:35 -07:00
parent e00550c57e
commit efb859013e
4 changed files with 29 additions and 43 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
src/Lean/Elab/Structure.lean
View file

@ -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

14
src/library/constructions/projection.cpp
View file

@ -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<name> const & proj_names,
buffer<implicit_infer_kind> const & infer_kinds, bool inst_implicit) {
environment mk_projections(environment const & env, name const & n, buffer<name> 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<name>
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<name>
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<object_ref> ps(proj_infos);
list_ref<name> ps(proj_infos);
buffer<name> proj_names;
buffer<implicit_infer_kind> infer_kinds;
for (auto p : ps) {
proj_names.push_back(cnstr_get_ref_t<name>(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<environment>([&]() { return mk_projections(new_env, n, proj_names, infer_kinds, inst_implicit != 0); });
return catch_kernel_exceptions<environment>([&]() { return mk_projections(new_env, n, proj_names, inst_implicit != 0); });
}
void initialize_def_projection() {

6
src/library/constructions/projection.h
View file

@ -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 <name> const & proj_names,
buffer<implicit_infer_kind> const & infer_kinds, bool inst_implicit = false);
environment mk_projections(environment const & env, name const & n, buffer <name> const & proj_names, bool inst_implicit = false);
void initialize_def_projection();
void finalize_def_projection();

38
tests/lean/run/bigop.lean
View file

@ -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