src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML
author blanchet
Fri Jun 25 15:01:35 2010 +0200 (2010-06-25 ago)
changeset 37566 9ca40dff25bd
parent 37515 ef3742657bc6
child 37570 de5feddaa95c
permissions -rw-r--r--
move "prepare_clauses" from "sledgehammer_fact_filter.ML" to "sledgehammer_hol_clause.ML";
since it has nothing to do with filtering
blanchet@36375
     1
(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML
wenzelm@33311
     2
    Author:     Jia Meng, NICTA
blanchet@36375
     3
    Author:     Jasmin Blanchette, TU Muenchen
mengj@17998
     4
blanchet@37509
     5
FOL clauses translated from HOL formulas.
mengj@17998
     6
*)
mengj@17998
     7
blanchet@35826
     8
signature SLEDGEHAMMER_HOL_CLAUSE =
wenzelm@24311
     9
sig
blanchet@37500
    10
  type cnf_thm = Sledgehammer_Fact_Preprocessor.cnf_thm
blanchet@36170
    11
  type name = Sledgehammer_FOL_Clause.name
blanchet@36393
    12
  type name_pool = Sledgehammer_FOL_Clause.name_pool
blanchet@35865
    13
  type kind = Sledgehammer_FOL_Clause.kind
blanchet@35865
    14
  type classrel_clause = Sledgehammer_FOL_Clause.classrel_clause
blanchet@35865
    15
  type arity_clause = Sledgehammer_FOL_Clause.arity_clause
wenzelm@24311
    16
  type polarity = bool
blanchet@35865
    17
blanchet@37509
    18
  datatype combtyp =
blanchet@37509
    19
    TyVar of name |
blanchet@37509
    20
    TyFree of name |
blanchet@37509
    21
    TyConstr of name * combtyp list
wenzelm@24311
    22
  datatype combterm =
blanchet@37509
    23
    CombConst of name * combtyp * combtyp list (* Const and Free *) |
blanchet@37509
    24
    CombVar of name * combtyp |
blanchet@35865
    25
    CombApp of combterm * combterm
wenzelm@24311
    26
  datatype literal = Literal of polarity * combterm
blanchet@35865
    27
  datatype hol_clause =
blanchet@37500
    28
    HOLClause of {clause_id: int, axiom_name: string, th: thm, kind: kind,
blanchet@37500
    29
                  literals: literal list, ctypes_sorts: typ list}
blanchet@37566
    30
  exception TRIVIAL of unit
blanchet@35865
    31
blanchet@37509
    32
  val type_of_combterm : combterm -> combtyp
blanchet@35865
    33
  val strip_combterm_comb : combterm -> combterm * combterm list
blanchet@35865
    34
  val literals_of_term : theory -> term -> literal list * typ list
blanchet@37410
    35
  val conceal_skolem_somes :
blanchet@37410
    36
    int -> (string * term) list -> term -> (string * term) list * term
blanchet@37566
    37
  val is_quasi_fol_theorem : theory -> thm -> bool
blanchet@37566
    38
  val make_clause_table : (thm * 'a) list -> (thm * 'a) Termtab.table
blanchet@37566
    39
  val tfree_classes_of_terms : term list -> string list
blanchet@37566
    40
  val tvar_classes_of_terms : term list -> string list
blanchet@37566
    41
  val type_consts_of_terms : theory -> term list -> string list
blanchet@37566
    42
  val prepare_clauses :
blanchet@37566
    43
    bool -> thm list -> cnf_thm list -> cnf_thm list -> theory
blanchet@37566
    44
    -> string vector
blanchet@37566
    45
       * (hol_clause list * hol_clause list * hol_clause list * hol_clause list
blanchet@37566
    46
          * classrel_clause list * arity_clause list)
wenzelm@24311
    47
end
mengj@17998
    48
blanchet@35826
    49
structure Sledgehammer_HOL_Clause : SLEDGEHAMMER_HOL_CLAUSE =
mengj@17998
    50
struct
mengj@17998
    51
blanchet@36167
    52
open Sledgehammer_Util
blanchet@35865
    53
open Sledgehammer_FOL_Clause
blanchet@35865
    54
open Sledgehammer_Fact_Preprocessor
paulson@22825
    55
mengj@17998
    56
(******************************************************)
mengj@17998
    57
(* data types for typed combinator expressions        *)
mengj@17998
    58
(******************************************************)
mengj@17998
    59
blanchet@37500
    60
type polarity = bool
mengj@17998
    61
blanchet@37509
    62
datatype combtyp =
blanchet@37509
    63
  TyVar of name |
blanchet@37509
    64
  TyFree of name |
blanchet@37509
    65
  TyConstr of name * combtyp list
blanchet@37509
    66
blanchet@35865
    67
datatype combterm =
blanchet@37509
    68
  CombConst of name * combtyp * combtyp list (* Const and Free *) |
blanchet@37509
    69
  CombVar of name * combtyp |
blanchet@35865
    70
  CombApp of combterm * combterm
wenzelm@24311
    71
mengj@17998
    72
datatype literal = Literal of polarity * combterm;
mengj@17998
    73
blanchet@35865
    74
datatype hol_clause =
blanchet@37500
    75
  HOLClause of {clause_id: int, axiom_name: string, th: thm, kind: kind,
blanchet@37500
    76
                literals: literal list, ctypes_sorts: typ list}
mengj@17998
    77
mengj@17998
    78
(*********************************************************************)
mengj@17998
    79
(* convert a clause with type Term.term to a clause with type clause *)
mengj@17998
    80
(*********************************************************************)
mengj@17998
    81
blanchet@37509
    82
(*Result of a function type; no need to check that the argument type matches.*)
blanchet@37509
    83
fun result_type (TyConstr (_, [_, tp2])) = tp2
blanchet@37509
    84
  | result_type _ = raise Fail "non-function type"
blanchet@37509
    85
blanchet@37509
    86
fun type_of_combterm (CombConst (_, tp, _)) = tp
blanchet@37509
    87
  | type_of_combterm (CombVar (_, tp)) = tp
blanchet@37509
    88
  | type_of_combterm (CombApp (t1, _)) = result_type (type_of_combterm t1)
blanchet@37509
    89
blanchet@37509
    90
(*gets the head of a combinator application, along with the list of arguments*)
blanchet@37509
    91
fun strip_combterm_comb u =
blanchet@37509
    92
    let fun stripc (CombApp(t,u), ts) = stripc (t, u::ts)
blanchet@37509
    93
        |   stripc  x =  x
blanchet@37509
    94
    in stripc(u,[]) end
blanchet@37509
    95
blanchet@36170
    96
fun isFalse (Literal (pol, CombConst ((c, _), _, _))) =
blanchet@35865
    97
      (pol andalso c = "c_False") orelse (not pol andalso c = "c_True")
mengj@17998
    98
  | isFalse _ = false;
mengj@17998
    99
blanchet@36170
   100
fun isTrue (Literal (pol, CombConst ((c, _), _, _))) =
mengj@17998
   101
      (pol andalso c = "c_True") orelse
mengj@17998
   102
      (not pol andalso c = "c_False")
mengj@17998
   103
  | isTrue _ = false;
wenzelm@24311
   104
blanchet@35865
   105
fun isTaut (HOLClause {literals,...}) = exists isTrue literals;
mengj@17998
   106
blanchet@37498
   107
fun type_of (Type (a, Ts)) =
blanchet@37498
   108
    let val (folTypes,ts) = types_of Ts in
blanchet@37498
   109
      (TyConstr (`make_fixed_type_const a, folTypes), ts)
blanchet@36169
   110
    end
blanchet@37498
   111
  | type_of (tp as TFree (a, _)) = (TyFree (`make_fixed_type_var a), [tp])
blanchet@37498
   112
  | type_of (tp as TVar (x, _)) =
blanchet@36169
   113
    (TyVar (make_schematic_type_var x, string_of_indexname x), [tp])
blanchet@37498
   114
and types_of Ts =
blanchet@37498
   115
    let val (folTyps, ts) = ListPair.unzip (map type_of Ts) in
blanchet@37498
   116
      (folTyps, union_all ts)
blanchet@37498
   117
    end
mengj@17998
   118
mengj@17998
   119
(* same as above, but no gathering of sort information *)
blanchet@37498
   120
fun simp_type_of (Type (a, Ts)) =
blanchet@37498
   121
      TyConstr (`make_fixed_type_const a, map simp_type_of Ts)
blanchet@37498
   122
  | simp_type_of (TFree (a, _)) = TyFree (`make_fixed_type_var a)
blanchet@37498
   123
  | simp_type_of (TVar (x, _)) =
blanchet@37498
   124
    TyVar (make_schematic_type_var x, string_of_indexname x)
mengj@18440
   125
mengj@17998
   126
(* convert a Term.term (with combinators) into a combterm, also accummulate sort info *)
blanchet@37498
   127
fun combterm_of thy (Const (c, T)) =
blanchet@37399
   128
      let
blanchet@37498
   129
        val (tp, ts) = type_of T
blanchet@37399
   130
        val tvar_list =
blanchet@37410
   131
          (if String.isPrefix skolem_theory_name c then
blanchet@37399
   132
             [] |> Term.add_tvarsT T |> map TVar
blanchet@37399
   133
           else
blanchet@37399
   134
             (c, T) |> Sign.const_typargs thy)
blanchet@37498
   135
          |> map simp_type_of
blanchet@37498
   136
        val c' = CombConst (`make_fixed_const c, tp, tvar_list)
paulson@22078
   137
      in  (c',ts)  end
blanchet@37498
   138
  | combterm_of _ (Free(v, T)) =
blanchet@37498
   139
      let val (tp,ts) = type_of T
blanchet@36170
   140
          val v' = CombConst (`make_fixed_var v, tp, [])
paulson@22078
   141
      in  (v',ts)  end
blanchet@37498
   142
  | combterm_of _ (Var(v, T)) =
blanchet@37498
   143
      let val (tp,ts) = type_of T
blanchet@36170
   144
          val v' = CombVar ((make_schematic_var v, string_of_indexname v), tp)
paulson@22078
   145
      in  (v',ts)  end
blanchet@37498
   146
  | combterm_of thy (P $ Q) =
blanchet@37498
   147
      let val (P', tsP) = combterm_of thy P
blanchet@37498
   148
          val (Q', tsQ) = combterm_of thy Q
blanchet@37498
   149
      in  (CombApp (P', Q'), union (op =) tsP tsQ)  end
blanchet@37498
   150
  | combterm_of _ (t as Abs _) = raise CLAUSE ("HOL clause", t)
mengj@17998
   151
blanchet@37498
   152
fun predicate_of thy ((@{const Not} $ P), polarity) =
blanchet@37498
   153
    predicate_of thy (P, not polarity)
blanchet@37498
   154
  | predicate_of thy (t, polarity) =
blanchet@37498
   155
    (combterm_of thy (Envir.eta_contract t), polarity)
mengj@17998
   156
blanchet@37498
   157
fun literals_of_term1 args thy (@{const Trueprop} $ P) =
blanchet@37498
   158
    literals_of_term1 args thy P
blanchet@37498
   159
  | literals_of_term1 args thy (@{const "op |"} $ P $ Q) =
blanchet@37498
   160
    literals_of_term1 (literals_of_term1 args thy P) thy Q
blanchet@37498
   161
  | literals_of_term1 (lits, ts) thy P =
blanchet@37498
   162
    let val ((pred, ts'), pol) = predicate_of thy (P, true) in
blanchet@37498
   163
      (Literal (pol, pred) :: lits, union (op =) ts ts')
blanchet@37498
   164
    end
blanchet@37498
   165
val literals_of_term = literals_of_term1 ([], [])
mengj@17998
   166
blanchet@37399
   167
fun skolem_name i j num_T_args =
blanchet@37399
   168
  skolem_prefix ^ (space_implode "_" (map Int.toString [i, j, num_T_args])) ^
blanchet@37399
   169
  skolem_infix ^ "g"
blanchet@37399
   170
blanchet@37410
   171
fun conceal_skolem_somes i skolem_somes t =
blanchet@37410
   172
  if exists_Const (curry (op =) @{const_name skolem_id} o fst) t then
blanchet@37399
   173
    let
blanchet@37399
   174
      fun aux skolem_somes
blanchet@37410
   175
              (t as (Const (@{const_name skolem_id}, Type (_, [_, T])) $ _)) =
blanchet@37399
   176
          let
blanchet@37399
   177
            val (skolem_somes, s) =
blanchet@37399
   178
              if i = ~1 then
blanchet@37399
   179
                (skolem_somes, @{const_name undefined})
blanchet@37410
   180
              else case AList.find (op aconv) skolem_somes t of
blanchet@37399
   181
                s :: _ => (skolem_somes, s)
blanchet@37436
   182
              | [] =>
blanchet@37399
   183
                let
blanchet@37410
   184
                  val s = skolem_theory_name ^ "." ^
blanchet@37399
   185
                          skolem_name i (length skolem_somes)
blanchet@37399
   186
                                        (length (Term.add_tvarsT T []))
blanchet@37410
   187
                in ((s, t) :: skolem_somes, s) end
blanchet@37410
   188
          in (skolem_somes, Const (s, T)) end
blanchet@37399
   189
        | aux skolem_somes (t1 $ t2) =
blanchet@37399
   190
          let
blanchet@37399
   191
            val (skolem_somes, t1) = aux skolem_somes t1
blanchet@37399
   192
            val (skolem_somes, t2) = aux skolem_somes t2
blanchet@37399
   193
          in (skolem_somes, t1 $ t2) end
blanchet@37399
   194
        | aux skolem_somes (Abs (s, T, t')) =
blanchet@37399
   195
          let val (skolem_somes, t') = aux skolem_somes t' in
blanchet@37399
   196
            (skolem_somes, Abs (s, T, t'))
blanchet@37399
   197
          end
blanchet@37399
   198
        | aux skolem_somes t = (skolem_somes, t)
blanchet@37399
   199
    in aux skolem_somes t end
blanchet@37399
   200
  else
blanchet@37399
   201
    (skolem_somes, t)
blanchet@37399
   202
blanchet@37566
   203
fun is_quasi_fol_theorem thy =
blanchet@37566
   204
  Meson.is_fol_term thy o snd o conceal_skolem_somes ~1 [] o prop_of
blanchet@37566
   205
blanchet@35865
   206
(* Trivial problem, which resolution cannot handle (empty clause) *)
blanchet@37506
   207
exception TRIVIAL of unit
wenzelm@28835
   208
mengj@17998
   209
(* making axiom and conjecture clauses *)
blanchet@37498
   210
fun make_clause thy (clause_id, axiom_name, kind, th) skolem_somes =
blanchet@37399
   211
  let
blanchet@37399
   212
    val (skolem_somes, t) =
blanchet@37410
   213
      th |> prop_of |> conceal_skolem_somes clause_id skolem_somes
blanchet@37498
   214
    val (lits, ctypes_sorts) = literals_of_term thy t
blanchet@37399
   215
  in
blanchet@37399
   216
    if forall isFalse lits then
blanchet@37506
   217
      raise TRIVIAL ()
blanchet@37399
   218
    else
blanchet@37399
   219
      (skolem_somes,
blanchet@37399
   220
       HOLClause {clause_id = clause_id, axiom_name = axiom_name, th = th,
blanchet@37399
   221
                  kind = kind, literals = lits, ctypes_sorts = ctypes_sorts})
blanchet@36218
   222
  end
mengj@19354
   223
blanchet@37500
   224
fun add_axiom_clause thy (th, ((name, id), _ : thm)) (skolem_somes, clss) =
blanchet@37399
   225
  let
blanchet@37498
   226
    val (skolem_somes, cls) = make_clause thy (id, name, Axiom, th) skolem_somes
blanchet@37399
   227
  in (skolem_somes, clss |> not (isTaut cls) ? cons (name, cls)) end
blanchet@37399
   228
blanchet@37498
   229
fun make_axiom_clauses thy clauses =
blanchet@37515
   230
  ([], []) |> fold_rev (add_axiom_clause thy) clauses |> snd
mengj@19354
   231
blanchet@37498
   232
fun make_conjecture_clauses thy =
blanchet@37399
   233
  let
blanchet@37399
   234
    fun aux _ _ [] = []
blanchet@37399
   235
      | aux n skolem_somes (th :: ths) =
blanchet@37399
   236
        let
blanchet@37399
   237
          val (skolem_somes, cls) =
blanchet@37498
   238
            make_clause thy (n, "conjecture", Conjecture, th) skolem_somes
blanchet@37399
   239
        in cls :: aux (n + 1) skolem_somes ths end
blanchet@37399
   240
  in aux 0 [] end
mengj@17998
   241
blanchet@37566
   242
(** Helper clauses **)
blanchet@37566
   243
blanchet@37566
   244
fun count_combterm (CombConst ((c, _), _, _)) =
blanchet@37566
   245
    Symtab.map_entry c (Integer.add 1)
blanchet@37566
   246
  | count_combterm (CombVar _) = I
blanchet@37566
   247
  | count_combterm (CombApp (t1, t2)) = count_combterm t1 #> count_combterm t2
blanchet@37566
   248
fun count_literal (Literal (_, t)) = count_combterm t
blanchet@37566
   249
fun count_clause (HOLClause {literals, ...}) = fold count_literal literals
blanchet@37566
   250
blanchet@37566
   251
fun raw_cnf_rules_pairs ps = map (fn (name, thm) => (thm, ((name, 0), thm))) ps
blanchet@37566
   252
fun cnf_helper_thms thy raw =
blanchet@37566
   253
  map (`Thm.get_name_hint)
blanchet@37566
   254
  #> (if raw then raw_cnf_rules_pairs else cnf_rules_pairs thy)
blanchet@37566
   255
blanchet@37566
   256
val optional_helpers =
blanchet@37566
   257
  [(["c_COMBI", "c_COMBK"], (false, @{thms COMBI_def COMBK_def})),
blanchet@37566
   258
   (["c_COMBB", "c_COMBC"], (false, @{thms COMBB_def COMBC_def})),
blanchet@37566
   259
   (["c_COMBS"], (false, @{thms COMBS_def}))]
blanchet@37566
   260
val optional_typed_helpers =
blanchet@37566
   261
  [(["c_True", "c_False"], (true, @{thms True_or_False})),
blanchet@37566
   262
   (["c_If"], (true, @{thms if_True if_False True_or_False}))]
blanchet@37566
   263
val mandatory_helpers = @{thms fequal_imp_equal equal_imp_fequal}
blanchet@37566
   264
blanchet@37566
   265
val init_counters =
blanchet@37566
   266
  Symtab.make (maps (maps (map (rpair 0) o fst))
blanchet@37566
   267
                    [optional_helpers, optional_typed_helpers])
blanchet@37566
   268
blanchet@37566
   269
fun get_helper_clauses thy is_FO full_types conjectures axcls =
blanchet@37566
   270
  let
blanchet@37566
   271
    val axclauses = map snd (make_axiom_clauses thy axcls)
blanchet@37566
   272
    val ct = fold (fold count_clause) [conjectures, axclauses] init_counters
blanchet@37566
   273
    fun is_needed c = the (Symtab.lookup ct c) > 0
blanchet@37566
   274
    val cnfs =
blanchet@37566
   275
      (optional_helpers
blanchet@37566
   276
       |> full_types ? append optional_typed_helpers
blanchet@37566
   277
       |> maps (fn (ss, (raw, ths)) =>
blanchet@37566
   278
                   if exists is_needed ss then cnf_helper_thms thy raw ths
blanchet@37566
   279
                   else []))
blanchet@37566
   280
      @ (if is_FO then [] else cnf_helper_thms thy false mandatory_helpers)
blanchet@37566
   281
  in map snd (make_axiom_clauses thy cnfs) end
blanchet@37566
   282
blanchet@37566
   283
fun make_clause_table xs =
blanchet@37566
   284
  fold (Termtab.update o `(prop_of o fst)) xs Termtab.empty
blanchet@37566
   285
blanchet@37566
   286
blanchet@37566
   287
(***************************************************************)
blanchet@37566
   288
(* Type Classes Present in the Axiom or Conjecture Clauses     *)
blanchet@37566
   289
(***************************************************************)
blanchet@37566
   290
blanchet@37566
   291
fun set_insert (x, s) = Symtab.update (x, ()) s
blanchet@37566
   292
blanchet@37566
   293
fun add_classes (sorts, cset) = List.foldl set_insert cset (flat sorts)
blanchet@37566
   294
blanchet@37566
   295
(*Remove this trivial type class*)
blanchet@37566
   296
fun delete_type cset = Symtab.delete_safe (the_single @{sort HOL.type}) cset;
blanchet@37566
   297
blanchet@37566
   298
fun tfree_classes_of_terms ts =
blanchet@37566
   299
  let val sorts_list = map (map #2 o OldTerm.term_tfrees) ts
blanchet@37566
   300
  in  Symtab.keys (delete_type (List.foldl add_classes Symtab.empty sorts_list))  end;
blanchet@37566
   301
blanchet@37566
   302
fun tvar_classes_of_terms ts =
blanchet@37566
   303
  let val sorts_list = map (map #2 o OldTerm.term_tvars) ts
blanchet@37566
   304
  in  Symtab.keys (delete_type (List.foldl add_classes Symtab.empty sorts_list))  end;
blanchet@37566
   305
blanchet@37566
   306
(*fold type constructors*)
blanchet@37566
   307
fun fold_type_consts f (Type (a, Ts)) x = fold (fold_type_consts f) Ts (f (a,x))
blanchet@37566
   308
  | fold_type_consts _ _ x = x;
blanchet@37566
   309
blanchet@37566
   310
(*Type constructors used to instantiate overloaded constants are the only ones needed.*)
blanchet@37566
   311
fun add_type_consts_in_term thy =
blanchet@37566
   312
  let
blanchet@37566
   313
    val const_typargs = Sign.const_typargs thy
blanchet@37566
   314
    fun aux (Const x) = fold (fold_type_consts set_insert) (const_typargs x)
blanchet@37566
   315
      | aux (Abs (_, _, u)) = aux u
blanchet@37566
   316
      | aux (Const (@{const_name skolem_id}, _) $ _) = I
blanchet@37566
   317
      | aux (t $ u) = aux t #> aux u
blanchet@37566
   318
      | aux _ = I
blanchet@37566
   319
  in aux end
blanchet@37566
   320
blanchet@37566
   321
fun type_consts_of_terms thy ts =
blanchet@37566
   322
  Symtab.keys (fold (add_type_consts_in_term thy) ts Symtab.empty);
blanchet@37566
   323
blanchet@37566
   324
(* Remove existing axiom clauses from the conjecture clauses, as this can
blanchet@37566
   325
   dramatically boost an ATP's performance (for some reason). *)
blanchet@37566
   326
fun subtract_cls ax_clauses =
blanchet@37566
   327
  filter_out (Termtab.defined (make_clause_table ax_clauses) o prop_of)
blanchet@37566
   328
blanchet@37566
   329
(* prepare for passing to writer,
blanchet@37566
   330
   create additional clauses based on the information from extra_cls *)
blanchet@37566
   331
fun prepare_clauses full_types goal_cls axcls extra_cls thy =
blanchet@37566
   332
  let
blanchet@37566
   333
    val is_FO = forall (Meson.is_fol_term thy o prop_of) goal_cls
blanchet@37566
   334
    val ccls = subtract_cls extra_cls goal_cls
blanchet@37566
   335
    val _ = app (fn th => trace_msg (fn _ => Display.string_of_thm_global thy th)) ccls
blanchet@37566
   336
    val ccltms = map prop_of ccls
blanchet@37566
   337
    and axtms = map (prop_of o #1) extra_cls
blanchet@37566
   338
    val subs = tfree_classes_of_terms ccltms
blanchet@37566
   339
    and supers = tvar_classes_of_terms axtms
blanchet@37566
   340
    and tycons = type_consts_of_terms thy (ccltms @ axtms)
blanchet@37566
   341
    (*TFrees in conjecture clauses; TVars in axiom clauses*)
blanchet@37566
   342
    val conjectures = make_conjecture_clauses thy ccls
blanchet@37566
   343
    val (_, extra_clauses) = ListPair.unzip (make_axiom_clauses thy extra_cls)
blanchet@37566
   344
    val (clnames, axiom_clauses) = ListPair.unzip (make_axiom_clauses thy axcls)
blanchet@37566
   345
    val helper_clauses =
blanchet@37566
   346
      get_helper_clauses thy is_FO full_types conjectures extra_cls
blanchet@37566
   347
    val (supers', arity_clauses) = make_arity_clauses thy tycons supers
blanchet@37566
   348
    val classrel_clauses = make_classrel_clauses thy subs supers'
blanchet@37566
   349
  in
blanchet@37566
   350
    (Vector.fromList clnames,
blanchet@37566
   351
      (conjectures, axiom_clauses, extra_clauses, helper_clauses, classrel_clauses, arity_clauses))
blanchet@37566
   352
  end
blanchet@37566
   353
wenzelm@33311
   354
end;