From bd1873f6b18754f3860b789e7e949386dd222f5a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 7 Jul 2014 17:48:20 -0700 Subject: [PATCH] feat(frontends/lean): add coercion modifier Signed-off-by: Leonardo de Moura --- src/frontends/lean/decl_cmds.cpp | 9 +++ src/frontends/lean/token_table.cpp | 2 +- tests/lean/run/algebra1.lean | 110 +++++++++++++++++++++++++++++ 3 files changed, 120 insertions(+), 1 deletion(-) create mode 100644 tests/lean/run/algebra1.lean diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp index 8fa121712..42ca4e297 100644 --- a/src/frontends/lean/decl_cmds.cpp +++ b/src/frontends/lean/decl_cmds.cpp @@ -13,6 +13,7 @@ Author: Leonardo de Moura #include "library/placeholder.h" #include "library/locals.h" #include "library/explicit.h" +#include "library/coercion.h" #include "frontends/lean/parser.h" #include "frontends/lean/util.h" #include "frontends/lean/class.h" @@ -25,6 +26,7 @@ static name g_assign(":="); static name g_private("[private]"); static name g_inline("[inline]"); static name g_instance("[instance]"); +static name g_coercion("[coercion]"); environment universe_cmd(parser & p) { name n = p.check_id_next("invalid universe declaration, identifier expected"); @@ -167,10 +169,12 @@ struct decl_modifiers { bool m_is_private; bool m_is_opaque; bool m_is_instance; + bool m_is_coercion; decl_modifiers() { m_is_private = false; m_is_opaque = true; m_is_instance = false; + m_is_coercion = false; } void parse(parser & p) { @@ -184,6 +188,9 @@ struct decl_modifiers { } else if (p.curr_is_token(g_instance)) { m_is_instance = true; p.next(); + } else if (p.curr_is_token(g_coercion)) { + m_is_coercion = true; + p.next(); } else { break; } @@ -281,6 +288,8 @@ environment definition_cmd_core(parser & p, bool is_theorem, bool _is_opaque) { } if (modifiers.m_is_instance) env = add_instance(env, real_n); + if (modifiers.m_is_coercion) + env = add_coercion(env, real_n, p.ios()); return env; } environment definition_cmd(parser & p) { diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp index b9f5e347a..c6c504a84 100644 --- a/src/frontends/lean/token_table.cpp +++ b/src/frontends/lean/token_table.cpp @@ -73,7 +73,7 @@ token_table init_token_table() { {"+", g_plus_prec}, {g_cup, g_cup_prec}, {"->", g_arrow_prec}, {nullptr, 0}}; char const * commands[] = {"theorem", "axiom", "variable", "definition", "coercion", - "variables", "[private]", "[inline]", "[fact]", "[instance]", "[class]", "[module]", + "variables", "[private]", "[inline]", "[fact]", "[instance]", "[class]", "[module]", "[coercion]", "abbreviation", "opaque_hint", "evaluate", "check", "print", "end", "namespace", "section", "import", "abbreviation", "inductive", "record", "structure", "module", "universe", "precedence", "infixl", "infixr", "infix", "postfix", "prefix", "notation", diff --git a/tests/lean/run/algebra1.lean b/tests/lean/run/algebra1.lean new file mode 100644 index 000000000..23f8e8b22 --- /dev/null +++ b/tests/lean/run/algebra1.lean @@ -0,0 +1,110 @@ +import standard +using num + +abbreviation Type1 := Type.{1} + +section + parameter {A : Type} + parameter f : A → A → A + parameter one : A + parameter inv : A → A + infixl `*`:75 := f + postfix `^-1`:100 := inv + definition is_assoc := ∀ a b c, (a*b)*c = a*b*c + definition is_id := ∀ a, a*one = a + definition is_inv := ∀ a, a*a^-1 = one +end + +namespace algebra + inductive mul_struct (A : Type) : Type := + | mk_mul_struct : (A → A → A) → mul_struct A + + inductive add_struct (A : Type) : Type := + | mk_add_struct : (A → A → A) → add_struct A + + definition mul [inline] {A : Type} {s : mul_struct A} (a b : A) + := mul_struct_rec (fun f, f) s a b + + infixl `*`:75 := mul + + definition add [inline] {A : Type} {s : add_struct A} (a b : A) + := add_struct_rec (fun f, f) s a b + + infixl `+`:65 := add +end + +namespace nat + inductive nat : Type := + | zero : nat + | succ : nat → nat + + variable add : nat → nat → nat + variable mul : nat → nat → nat + + definition is_mul_struct [inline] [instance] : algebra.mul_struct nat + := algebra.mk_mul_struct mul + + definition is_add_struct [inline] [instance] : algebra.add_struct nat + := algebra.mk_add_struct add + + definition to_nat (n : num) : nat + := #algebra + num_rec zero (λ n, pos_num_rec (succ zero) (λ n r, r + r) (λ n r, r + r + succ zero) n) n +end + +namespace algebra +namespace semigroup + inductive semigroup_struct (A : Type) : Type := + | mk_semigroup_struct : Π (mul : A → A → A), is_assoc mul → semigroup_struct A + + definition mul [inline] {A : Type} (s : semigroup_struct A) (a b : A) + := semigroup_struct_rec (fun f h, f) s a b + + definition assoc [inline] {A : Type} (s : semigroup_struct A) : is_assoc (mul s) + := semigroup_struct_rec (fun f h, h) s + + definition is_mul_struct [inline] [instance] (A : Type) (s : semigroup_struct A) : mul_struct A + := mk_mul_struct (mul s) + + inductive semigroup : Type := + | mk_semigroup : Π (A : Type), semigroup_struct A → semigroup + + definition carrier [inline] [coercion] (g : semigroup) + := semigroup_rec (fun c s, c) g + + definition is_semigroup [inline] [instance] (g : semigroup) : semigroup_struct (carrier g) + := semigroup_rec (fun c s, s) g +end + +namespace monoid + inductive monoid_struct (A : Type) : Type := + | mk_monoid_struct : Π (mul : A → A → A) (id : A), is_assoc mul → is_id mul id → monoid_struct A + + definition mul [inline] {A : Type} (s : monoid_struct A) (a b : A) + := monoid_struct_rec (fun mul id a i, mul) s a b + + definition assoc [inline] {A : Type} (s : monoid_struct A) : is_assoc (mul s) + := monoid_struct_rec (fun mul id a i, a) s + + using algebra.semigroup -- Fix: allow user to write just semigroup + definition is_semigroup_struct [inline] [instance] (A : Type) (s : monoid_struct A) : semigroup_struct A + := mk_semigroup_struct (mul s) (assoc s) + + inductive monoid : Type := + | mk_monoid : Π (A : Type), monoid_struct A → monoid + + definition carrier [inline] [coercion] (m : monoid) + := monoid_rec (fun c s, c) m + + definition is_monoid [inline] [instance] (m : monoid) : monoid_struct (carrier m) + := monoid_rec (fun c s, s) m +end +end + +section + using algebra algebra.semigroup algebra.monoid + variable M : monoid + variables a b c : M + check a*b*c*a*b*c*a*b*a*b*c*a + check a*b +end