feat(frontends/lean): force 'classes' to be declared before instances are declared, closes #228

library/algebra/category.lean

@@ -61,11 +61,11 @@ namespace category
     i = id ∘ i : eq.symm id_left
     ... = id : H
 
-  inductive is_section {A B : ob} (f : mor A B) : Type :=
+  inductive is_section [class] {A B : ob} (f : mor A B) : Type :=
   mk : ∀{g}, g ∘ f = id → is_section f
-  inductive is_retraction {A B : ob} (f : mor A B) : Type :=
+  inductive is_retraction [class] {A B : ob} (f : mor A B) : Type :=
   mk : ∀{g}, f ∘ g = id → is_retraction f
-  inductive is_iso {A B : ob} (f : mor A B) : Type :=
+  inductive is_iso [class] {A B : ob} (f : mor A B) : Type :=
   mk : ∀{g}, g ∘ f = id → f ∘ g = id → is_iso f
 
   definition retraction_of {A B : ob} (f : mor A B) {H : is_section f} : mor B A :=

library/algebra/relation.lean

@@ -18,7 +18,7 @@ definition symmetric {T : Type} (R : T → T → Type) : Type := ∀⦃x y⦄, R
 definition transitive {T : Type} (R : T → T → Type) : Type := ∀⦃x y z⦄, R x y → R y z → R x z
 
 
-inductive is_reflexive {T : Type} (R : T → T → Type) : Prop :=
+inductive is_reflexive [class] {T : Type} (R : T → T → Type) : Prop :=
 mk : reflexive R → is_reflexive R
 
 namespace is_reflexive
@@ -32,7 +32,7 @@ namespace is_reflexive
 end is_reflexive
 
 
-inductive is_symmetric {T : Type} (R : T → T → Type) : Prop :=
+inductive is_symmetric [class] {T : Type} (R : T → T → Type) : Prop :=
 mk : symmetric R → is_symmetric R
 
 namespace is_symmetric
@@ -46,7 +46,7 @@ namespace is_symmetric
 end is_symmetric
 
 
-inductive is_transitive {T : Type} (R : T → T → Type) : Prop :=
+inductive is_transitive [class] {T : Type} (R : T → T → Type) : Prop :=
 mk : transitive R → is_transitive R
 
 namespace is_transitive
@@ -60,7 +60,7 @@ namespace is_transitive
 end is_transitive
 
 
-inductive is_equivalence {T : Type} (R : T → T → Type) : Prop :=
+inductive is_equivalence [class] {T : Type} (R : T → T → Type) : Prop :=
 mk : is_reflexive R → is_symmetric R → is_transitive R → is_equivalence R
 
 theorem is_equivalence.is_reflexive [instance]
@@ -90,12 +90,12 @@ theorem is_PER.is_transitive [instance]
 -- Congruence for unary and binary functions
 -- -----------------------------------------
 
-inductive congruence {T1 : Type} (R1 : T1 → T1 → Prop) {T2 : Type} (R2 : T2 → T2 → Prop)
+inductive congruence [class] {T1 : Type} (R1 : T1 → T1 → Prop) {T2 : Type} (R2 : T2 → T2 → Prop)
     (f : T1 → T2) : Prop :=
 mk : (∀x y, R1 x y → R2 (f x) (f y)) → congruence R1 R2 f
 
 -- for binary functions
-inductive congruence2 {T1 : Type}  (R1 : T1 → T1 → Prop) {T2 : Type} (R2 : T2 → T2 → Prop)
+inductive congruence2 [class] {T1 : Type}  (R1 : T1 → T1 → Prop) {T2 : Type} (R2 : T2 → T2 → Prop)
     {T3 : Type} (R3 : T3 → T3 → Prop) (f : T1 → T2 → T3) : Prop :=
 mk : (∀(x1 y1 : T1) (x2 y2 : T2), R1 x1 y1 → R2 x2 y2 → R3 (f x1 x2) (f y1 y2)) →
     congruence2 R1 R2 R3 f
@@ -161,7 +161,7 @@ congruence.mk (λx y H, H)
 -- Relations that can be coerced to functions / implications
 -- ---------------------------------------------------------
 
-inductive mp_like {R : Type → Type → Prop} {a b : Type} (H : R a b) : Type :=
+inductive mp_like [class] {R : Type → Type → Prop} {a b : Type} (H : R a b) : Type :=
 mk {} : (a → b) → @mp_like R a b H
 
 namespace mp_like

library/hott/fibrant.lean

@@ -7,7 +7,7 @@ import data.prod data.sum data.sigma
 
 open unit bool nat prod sum sigma
 
-inductive fibrant (T : Type) : Type :=
+inductive fibrant [class] (T : Type) : Type :=
 fibrant_mk : fibrant T
 
 namespace fibrant

library/logic/decidable.lean

@@ -4,7 +4,7 @@
 
 import logic.connectives
 
-inductive decidable (p : Prop) : Type :=
+inductive decidable [class] (p : Prop) : Type :=
 inl : p  → decidable p,
 inr : ¬p → decidable p
 

library/logic/inhabited.lean

@@ -4,7 +4,7 @@
 
 import logic.connectives
 
-inductive inhabited (A : Type) : Type :=
+inductive inhabited [class] (A : Type) : Type :=
 mk : A → inhabited A
 
 namespace inhabited

library/logic/nonempty.lean

@@ -4,7 +4,7 @@
 import .inhabited
 open inhabited
 
-inductive nonempty (A : Type) : Prop :=
+inductive nonempty [class] (A : Type) : Prop :=
 intro : A → nonempty A
 
 namespace nonempty

src/frontends/lean/class.cpp

@@ -123,11 +123,17 @@ static void check_class(environment const & env, name const & c_name) {
         throw exception(sstream() << "invalid class, '" << c_name << "' is a definition");
 }
 
+static void check_is_class(environment const & env, name const & c_name) {
+    class_state const & s = class_ext::get_state(env);
+    if (!s.m_instances.contains(c_name))
+        throw exception(sstream() << "'" << c_name << "' is not a class");
+}
+
 name get_class_name(environment const & env, expr const & e) {
     if (!is_constant(e))
         throw exception("class expected, expression is not a constant");
     name const & c_name = const_name(e);
-    check_class(env, c_name);
+    check_is_class(env, c_name);
     return c_name;
 }
 
@@ -156,7 +162,7 @@ environment add_instance(environment const & env, name const & n, unsigned prior
         type = instantiate(binding_body(type), mk_local(ngen.next(), binding_domain(type)));
     }
     name c = get_class_name(env, get_app_fn(type));
-    check_class(env, c);
+    check_is_class(env, c);
     return class_ext::add_entry(env, get_dummy_ios(), class_entry(c, n, priority), persistent);
 }
 

tests/lean/bad_class.lean

@@ -0,0 +1,7 @@
+import logic
+
+definition subsingleton (A : Type) := ∀⦃a b : A⦄, a = b
+class subsingleton
+
+protected definition prop.subsingleton [instance] (P : Prop) : subsingleton P :=
+λa b, !proof_irrel

tests/lean/bad_class.lean.expected.out

@@ -0,0 +1,2 @@
+bad_class.lean:4:0: error: invalid class, 'subsingleton' is a definition
+bad_class.lean:6:0: error: 'eq' is not a class

tests/lean/inst.lean

@@ -2,7 +2,7 @@ import logic data.prod priority
 open priority
 set_option pp.notation false
 
-inductive C (A : Type) :=
+inductive C [class] (A : Type) :=
 mk : A → C A
 
 definition val {A : Type} (c : C A) : A :=

tests/lean/run/algebra1.lean

@@ -15,10 +15,10 @@ context
 end
 
 namespace algebra
-  inductive mul_struct (A : Type) : Type :=
+  inductive mul_struct [class] (A : Type) : Type :=
   mk : (A → A → A) → mul_struct A
 
-  inductive add_struct (A : Type) : Type :=
+  inductive add_struct [class] (A : Type) : Type :=
   mk : (A → A → A) → add_struct A
 
   definition mul  {A : Type} {s : mul_struct A} (a b : A)
@@ -32,6 +32,7 @@ namespace algebra
   infixl `+`:65 := add
 end algebra
 
+open algebra
   inductive nat : Type :=
   zero : nat,
   succ : nat → nat
@@ -54,7 +55,7 @@ end nat
 
 namespace algebra
 namespace semigroup
-  inductive semigroup_struct (A : Type) : Type :=
+  inductive semigroup_struct [class] (A : Type) : Type :=
   mk : Π (mul : A → A → A), is_assoc mul → semigroup_struct A
 
   definition mul  {A : Type} (s : semigroup_struct A) (a b : A)
@@ -79,7 +80,7 @@ end semigroup
 namespace monoid
   check semigroup.mul
 
-  inductive monoid_struct (A : Type) : Type :=
+  inductive monoid_struct [class] (A : Type) : Type :=
   mk_monoid_struct : Π (mul : A → A → A) (id : A), is_assoc mul → is_id mul id → monoid_struct A
 
   definition mul  {A : Type} (s : monoid_struct A) (a b : A)

tests/lean/run/class4.lean

@@ -56,7 +56,7 @@ theorem not_zero_add (x y : nat) (H : ¬ is_zero y) : ¬ is_zero (x + y)
           not_is_zero_succ (x+w),
         subst (symm H1) H2)
 
-inductive not_zero (x : nat) : Prop :=
+inductive not_zero [class] (x : nat) : Prop :=
 intro : ¬ is_zero x → not_zero x
 
 theorem not_zero_not_is_zero {x : nat} (H : not_zero x) : ¬ is_zero x

tests/lean/run/class5.lean

@@ -1,7 +1,7 @@
 import logic
 
 namespace algebra
-  inductive mul_struct (A : Type) : Type :=
+  inductive mul_struct [class] (A : Type) : Type :=
   mk : (A → A → A) → mul_struct A
 
   definition mul {A : Type} {s : mul_struct A} (a b : A)
@@ -10,6 +10,7 @@ namespace algebra
   infixl `*`:75 := mul
 end algebra
 
+open algebra
 namespace nat
   inductive nat : Type :=
   zero : nat,

tests/lean/run/class7.lean

@@ -1,7 +1,7 @@
 import logic
 open tactic
 
-inductive inh (A : Type) : Type :=
+inductive inh [class] (A : Type) : Type :=
 intro : A -> inh A
 
 theorem inh_bool [instance] : inh Prop

tests/lean/run/class8.lean

@@ -1,7 +1,7 @@
 import logic data.prod
 open tactic prod
 
-inductive inh (A : Type) : Prop :=
+inductive inh [class] (A : Type) : Prop :=
 intro : A -> inh A
 
 instance inh.intro

tests/lean/run/class_coe.lean

@@ -6,7 +6,7 @@ constant nat_add  : nat → nat → nat
 constant int_add  : int → int → int
 constant real_add : real → real → real
 
-inductive add_struct (A : Type) :=
+inductive add_struct [class] (A : Type) :=
 mk : (A → A → A) → add_struct A
 
 definition add {A : Type} {S : add_struct A} (a b : A) : A :=

tests/lean/run/congr_imp_bug.lean

@@ -8,7 +8,7 @@ open function
 
 namespace congr
 
-inductive struc {T1 : Type} {T2 : Type} (R1 : T1 → T1 → Prop) (R2 : T2 → T2 → Prop)
+inductive struc [class] {T1 : Type} {T2 : Type} (R1 : T1 → T1 → Prop) (R2 : T2 → T2 → Prop)
     (f : T1 → T2) : Prop :=
 mk : (∀x y : T1, R1 x y → R2 (f x) (f y)) → struc R1 R2 f
 

tests/lean/run/elab_bug1.lean

@@ -16,7 +16,7 @@ definition reflexive {T : Type} (R : T → T → Prop) : Prop := ∀x, R x x
 -- Congruence classes for unary and binary functions
 -- -------------------------------------------------
 
-inductive congruence {T1 : Type} {T2 : Type} (R1 : T1 → T1 → Prop) (R2 : T2 → T2 → Prop)
+inductive congruence [class] {T1 : Type} {T2 : Type} (R1 : T1 → T1 → Prop) (R2 : T2 → T2 → Prop)
     (f : T1 → T2) : Prop :=
 mk : (∀x y : T1, R1 x y → R2 (f x) (f y)) → congruence R1 R2 f
 

tests/lean/run/group.lean

@@ -12,7 +12,7 @@ context
   definition is_inv   := ∀ a, a*a^-1 = one
 end
 
-inductive group_struct (A : Type) : Type :=
+inductive group_struct [class] (A : Type) : Type :=
 mk_group_struct : Π (mul : A → A → A) (one : A) (inv : A → A), is_assoc mul → is_id mul one → is_inv mul one inv → group_struct A
 
 inductive group : Type :=

tests/lean/run/group2.lean

@@ -12,7 +12,7 @@ context
   definition is_inv   := ∀ a, a*a^-1 = one
 end
 
-inductive group_struct (A : Type) : Type :=
+inductive group_struct [class] (A : Type) : Type :=
 mk : Π (mul : A → A → A) (one : A) (inv : A → A), is_assoc mul → is_id mul one → is_inv mul one inv → group_struct A
 
 inductive group : Type :=

tests/lean/run/group3.lean

@@ -56,7 +56,7 @@ section
   include s
   definition semigroup_has_mul [instance] : has_mul A := has_mul.mk semigroup.mul
 
-  theorem mul_assoc [instance] (a b c : A) : a * b * c = a * (b * c) :=
+  theorem mul_assoc (a b c : A) : a * b * c = a * (b * c) :=
     !semigroup.assoc
 end
 

tests/lean/run/univ_bug1.lean

@@ -12,7 +12,7 @@ namespace simp
 -- set_option pp.implicit true
 
 -- first define a class of homogeneous equality
-inductive simplifies_to {T : Type} (t1 t2 : T) : Prop :=
+inductive simplifies_to [class] {T : Type} (t1 t2 : T) : Prop :=
 mk : t1 = t2 → simplifies_to t1 t2
 
 theorem get_eq {T : Type} {t1 t2 : T} (C : simplifies_to t1 t2) : t1 = t2 :=

tests/lean/run/univ_bug2.lean

@@ -8,7 +8,7 @@ import logic data.nat
 open nat
 
 -- first define a class of homogeneous equality
-inductive simplifies_to {T : Type} (t1 t2 : T) : Prop :=
+inductive simplifies_to [class] {T : Type} (t1 t2 : T) : Prop :=
 mk : t1 = t2 → simplifies_to t1 t2
 
 namespace simplifies_to

tests/lean/slow/cat_sec_var_bug.lean

@@ -60,9 +60,9 @@ namespace category
     i = id ∘ i : eq.symm !id_left
     ... = id : H
 
-  inductive is_section    (f : hom a b) : Type := mk : ∀{g}, g ∘ f = id → is_section f
-  inductive is_retraction (f : hom a b) : Type := mk : ∀{g}, f ∘ g = id → is_retraction f
-  inductive is_iso        (f : hom a b) : Type := mk : ∀{g}, g ∘ f = id → f ∘ g = id → is_iso f
+  inductive is_section    [class] (f : hom a b) : Type := mk : ∀{g}, g ∘ f = id → is_section f
+  inductive is_retraction [class] (f : hom a b) : Type := mk : ∀{g}, f ∘ g = id → is_retraction f
+  inductive is_iso        [class] (f : hom a b) : Type := mk : ∀{g}, g ∘ f = id → f ∘ g = id → is_iso f
 
   definition retraction_of (f : hom a b) {H : is_section f} : hom b a :=
   is_section.rec (λg h, g) H