src/HOL/TPTP/atp_theory_export.ML
author paulson <lp15@cam.ac.uk>
Tue Apr 25 16:39:54 2017 +0100 (2017-04-25)
changeset 65578 e4997c181cce
parent 62549 9498623b27f0
child 69597 ff784d5a5bfb
permissions -rw-r--r--
New material from PNT proof, as well as more default [simp] declarations. Also removed duplicate theorems about geometric series
blanchet@46321
     1
(*  Title:      HOL/TPTP/atp_theory_export.ML
blanchet@42602
     2
    Author:     Jasmin Blanchette, TU Muenchen
blanchet@42602
     3
    Copyright   2011
blanchet@42602
     4
blanchet@48234
     5
Export Isabelle theories as first-order TPTP inferences.
blanchet@42602
     6
*)
blanchet@42602
     7
blanchet@46321
     8
signature ATP_THEORY_EXPORT =
blanchet@42602
     9
sig
blanchet@45305
    10
  type atp_format = ATP_Problem.atp_format
blanchet@45305
    11
blanchet@51646
    12
  datatype inference_policy =
blanchet@51646
    13
    No_Inferences | Unchecked_Inferences | Checked_Inferences
blanchet@51646
    14
blanchet@61323
    15
  val generate_atp_inference_file_for_theory : Proof.context -> theory -> atp_format ->
blanchet@61323
    16
    inference_policy -> string -> string -> unit
blanchet@61323
    17
  val generate_casc_lbt_isa_files_for_theory : Proof.context -> theory -> atp_format ->
blanchet@61323
    18
    inference_policy -> string -> string -> unit
blanchet@42602
    19
end;
blanchet@42602
    20
blanchet@48234
    21
structure ATP_Theory_Export : ATP_THEORY_EXPORT =
blanchet@42602
    22
struct
blanchet@42602
    23
blanchet@43479
    24
open ATP_Problem
blanchet@43566
    25
open ATP_Proof
blanchet@46320
    26
open ATP_Problem_Generate
blanchet@43566
    27
open ATP_Systems
blanchet@42602
    28
blanchet@61323
    29
val max_dependencies = 100
blanchet@61323
    30
val max_facts = 512
blanchet@61323
    31
val atp_timeout = seconds 0.5
blanchet@61323
    32
blanchet@51646
    33
datatype inference_policy =
blanchet@51646
    34
  No_Inferences | Unchecked_Inferences | Checked_Inferences
blanchet@42602
    35
wenzelm@53980
    36
val prefix = Library.prefix
blanchet@51646
    37
val fact_name_of = prefix fact_prefix o ascii_of
blanchet@43479
    38
blanchet@54197
    39
fun atp_of_format (THF (Polymorphic, _)) = dummy_thfN
blanchet@54197
    40
  | atp_of_format (THF (Monomorphic, _)) = satallaxN
blanchet@59577
    41
  | atp_of_format (DFG Polymorphic) = pirateN
blanchet@51998
    42
  | atp_of_format (DFG Monomorphic) = spassN
blanchet@52995
    43
  | atp_of_format (TFF Polymorphic) = alt_ergoN
blanchet@52995
    44
  | atp_of_format (TFF Monomorphic) = vampireN
blanchet@51998
    45
  | atp_of_format FOF = eN
blanchet@51998
    46
  | atp_of_format CNF_UEQ = waldmeisterN
blanchet@51998
    47
  | atp_of_format CNF = eN
blanchet@48318
    48
blanchet@51646
    49
fun run_atp ctxt format problem =
blanchet@43566
    50
  let
blanchet@43566
    51
    val thy = Proof_Context.theory_of ctxt
blanchet@47055
    52
    val prob_file = File.tmp_path (Path.explode "prob")
blanchet@51998
    53
    val atp = atp_of_format format
blanchet@57676
    54
    val {exec, arguments, proof_delims, known_failures, ...} = get_atp thy atp ()
blanchet@47038
    55
    val ord = effective_term_order ctxt atp
blanchet@61323
    56
    val _ = problem
blanchet@61323
    57
      |> lines_of_atp_problem format ord (K [])
blanchet@61323
    58
      |> File.write_list prob_file
blanchet@57676
    59
    val exec = exec false
blanchet@48376
    60
    val path = getenv (List.last (fst exec)) ^ "/" ^ List.last (snd exec)
blanchet@43566
    61
    val command =
wenzelm@62549
    62
      File.bash_path (Path.explode path) ^ " " ^
wenzelm@62549
    63
      arguments ctxt false "" atp_timeout (File.bash_path prob_file)
blanchet@50927
    64
                (ord, K [], K [])
blanchet@51646
    65
    val outcome =
wenzelm@62519
    66
      Timeout.apply atp_timeout Isabelle_System.bash_output command
blanchet@51646
    67
      |> fst
blanchet@51646
    68
      |> extract_tstplike_proof_and_outcome false proof_delims known_failures
blanchet@51646
    69
      |> snd
wenzelm@62519
    70
      handle Timeout.TIMEOUT _ => SOME TimedOut
blanchet@51647
    71
    val _ =
blanchet@51647
    72
      tracing ("Ran ATP: " ^
blanchet@51649
    73
               (case outcome of
blanchet@51649
    74
                  NONE => "Success"
blanchet@53586
    75
                | SOME failure => string_of_atp_failure failure))
blanchet@51646
    76
  in outcome end
blanchet@43566
    77
blanchet@61860
    78
fun is_problem_line_reprovable ctxt format prelude axioms deps (Formula (ident', _, phi, _, _)) =
blanchet@51646
    79
    is_none (run_atp ctxt format
blanchet@61860
    80
      ((factsN,
blanchet@61860
    81
        Formula (ident', Conjecture, phi, NONE, []) :: map_filter (Symtab.lookup axioms) deps) ::
blanchet@61860
    82
       prelude))
blanchet@51646
    83
  | is_problem_line_reprovable _ _ _ _ _ _ = false
blanchet@51646
    84
blanchet@51646
    85
fun inference_term _ [] = NONE
blanchet@51646
    86
  | inference_term check_infs ss =
blanchet@51646
    87
    ATerm (("inference", []),
blanchet@51646
    88
        [ATerm (("checked_isabelle" |> not check_infs ? prefix "un", []), []),
blanchet@51646
    89
         ATerm ((tptp_empty_list, []), []),
blanchet@51646
    90
         ATerm ((tptp_empty_list, []),
blanchet@51646
    91
         map (fn s => ATerm ((s, []), [])) ss)])
blanchet@51646
    92
    |> SOME
blanchet@51646
    93
blanchet@51646
    94
fun add_inferences_to_problem_line ctxt format check_infs prelude axioms infers
blanchet@61860
    95
      (line as Formula ((ident, alt), Axiom, phi, NONE, info)) =
blanchet@51646
    96
    let
blanchet@51646
    97
      val deps =
blanchet@51646
    98
        case these (AList.lookup (op =) infers ident) of
blanchet@51646
    99
          [] => []
blanchet@51646
   100
        | deps =>
blanchet@51646
   101
          if check_infs andalso
blanchet@51646
   102
             not (is_problem_line_reprovable ctxt format prelude axioms deps
blanchet@51646
   103
                                             line) then
blanchet@51646
   104
            []
blanchet@51646
   105
          else
blanchet@51646
   106
            deps
blanchet@51646
   107
    in
blanchet@61860
   108
      Formula ((ident, alt), Lemma, phi, inference_term check_infs deps, info)
blanchet@51646
   109
    end
blanchet@51646
   110
  | add_inferences_to_problem_line _ _ _ _ _ _ line = line
blanchet@51646
   111
blanchet@51646
   112
fun add_inferences_to_problem ctxt format check_infs prelude infers problem =
blanchet@51646
   113
  let
blanchet@61323
   114
    fun add_if_axiom (axiom as Formula ((ident, _), Axiom, _, _, _)) = Symtab.default (ident, axiom)
blanchet@51646
   115
      | add_if_axiom _ = I
blanchet@61323
   116
blanchet@51646
   117
    val add_axioms_of_problem = fold (fold add_if_axiom o snd)
blanchet@51646
   118
    val axioms = Symtab.empty |> check_infs ? add_axioms_of_problem problem
blanchet@51646
   119
  in
blanchet@61323
   120
    map (apsnd (map (add_inferences_to_problem_line ctxt format check_infs prelude axioms infers)))
blanchet@61323
   121
      problem
blanchet@51646
   122
  end
blanchet@51646
   123
blanchet@51646
   124
fun ident_of_problem_line (Class_Decl (ident, _, _)) = ident
blanchet@51646
   125
  | ident_of_problem_line (Type_Decl (ident, _, _)) = ident
blanchet@51646
   126
  | ident_of_problem_line (Sym_Decl (ident, _, _)) = ident
blanchet@51646
   127
  | ident_of_problem_line (Class_Memb (ident, _, _, _)) = ident
blanchet@51646
   128
  | ident_of_problem_line (Formula ((ident, _), _, _, _, _)) = ident
blanchet@51646
   129
wenzelm@59058
   130
fun order_facts ord = sort (ord o apply2 ident_of_problem_line)
blanchet@51646
   131
blanchet@43499
   132
fun order_problem_facts _ [] = []
blanchet@43499
   133
  | order_problem_facts ord ((heading, lines) :: problem) =
blanchet@43499
   134
    if heading = factsN then (heading, order_facts ord lines) :: problem
blanchet@43499
   135
    else (heading, lines) :: order_problem_facts ord problem
blanchet@43499
   136
blanchet@45305
   137
(* A fairly random selection of types used for monomorphizing. *)
blanchet@45305
   138
val ground_types =
blanchet@45305
   139
  [@{typ nat}, HOLogic.intT, HOLogic.realT, @{typ "nat => bool"}, @{typ bool},
blanchet@45305
   140
   @{typ unit}]
blanchet@45305
   141
blanchet@61323
   142
fun ground_type_of_tvar _ [] tvar = raise TYPE ("ground_type_of_tvar", [TVar tvar], [])
blanchet@51998
   143
  | ground_type_of_tvar thy (T :: Ts) tvar =
blanchet@45305
   144
    if can (Sign.typ_match thy (TVar tvar, T)) Vartab.empty then T
blanchet@51998
   145
    else ground_type_of_tvar thy Ts tvar
blanchet@45305
   146
blanchet@45305
   147
fun monomorphize_term ctxt t =
blanchet@45305
   148
  let val thy = Proof_Context.theory_of ctxt in
blanchet@51998
   149
    t |> map_types (map_type_tvar (ground_type_of_tvar thy ground_types))
blanchet@45305
   150
    handle TYPE _ => @{prop True}
blanchet@45305
   151
  end
blanchet@45305
   152
blanchet@51633
   153
fun heading_sort_key heading =
blanchet@61323
   154
  if String.isPrefix factsN heading then "_" ^ heading else heading
blanchet@57306
   155
blanchet@51998
   156
fun problem_of_theory ctxt thy format infer_policy type_enc =
blanchet@42602
   157
  let
blanchet@48299
   158
    val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
blanchet@48315
   159
    val type_enc =
blanchet@52031
   160
      type_enc |> type_enc_of_string Non_Strict
blanchet@48315
   161
               |> adjust_type_enc format
blanchet@48131
   162
    val mono = not (is_type_enc_polymorphic type_enc)
blanchet@61323
   163
blanchet@48438
   164
    val facts =
blanchet@50442
   165
      Sledgehammer_Fact.all_facts (Proof_Context.init_global thy) true false
wenzelm@58922
   166
                                  Keyword.empty_keywords [] [] css_table
wenzelm@60641
   167
      |> sort (Sledgehammer_MaSh.crude_thm_ord ctxt o apply2 snd)
blanchet@51646
   168
    val problem =
blanchet@43576
   169
      facts
blanchet@45305
   170
      |> map (fn ((_, loc), th) =>
wenzelm@59582
   171
        ((Thm.get_name_hint th, loc), th |> Thm.prop_of |> mono ? monomorphize_term ctxt))
blanchet@61860
   172
      |> generate_atp_problem ctxt true format Axiom type_enc Exporter combsN false false true []
blanchet@57268
   173
        @{prop False}
wenzelm@60924
   174
      |> #1 |> sort_by (heading_sort_key o fst)
blanchet@51646
   175
    val prelude = fst (split_last problem)
blanchet@50735
   176
    val name_tabs = Sledgehammer_Fact.build_name_tables Thm.get_name_hint facts
blanchet@42602
   177
    val infers =
blanchet@51646
   178
      if infer_policy = No_Inferences then
blanchet@51646
   179
        []
blanchet@51646
   180
      else
blanchet@51646
   181
        facts
blanchet@51646
   182
        |> map (fn (_, th) =>
blanchet@51646
   183
                   (fact_name_of (Thm.get_name_hint th),
blanchet@57306
   184
                    th |> Sledgehammer_Util.thms_in_proof max_dependencies (SOME name_tabs)
blanchet@57306
   185
                       |> these |> map fact_name_of))
blanchet@51650
   186
    val all_problem_names =
blanchet@57307
   187
      problem |> maps (map ident_of_problem_line o snd) |> distinct (op =)
blanchet@51650
   188
    val all_problem_name_set = Symtab.make (map (rpair ()) all_problem_names)
blanchet@42602
   189
    val infers =
blanchet@51650
   190
      infers |> filter (Symtab.defined all_problem_name_set o fst)
blanchet@51650
   191
             |> map (apsnd (filter (Symtab.defined all_problem_name_set)))
blanchet@51650
   192
    val maybe_add_edge = perhaps o try o String_Graph.add_edge_acyclic
blanchet@43499
   193
    val ordered_names =
blanchet@43499
   194
      String_Graph.empty
blanchet@51646
   195
      |> fold (String_Graph.new_node o rpair ()) all_problem_names
blanchet@57307
   196
      |> fold (fn (to, froms) => fold (fn from => maybe_add_edge (from, to)) froms) infers
blanchet@51650
   197
      |> fold (fn (to, from) => maybe_add_edge (from, to))
blanchet@57307
   198
        (tl all_problem_names ~~ fst (split_last all_problem_names))
blanchet@43499
   199
      |> String_Graph.topological_order
blanchet@43499
   200
    val order_tab =
blanchet@43499
   201
      Symtab.empty
blanchet@57307
   202
      |> fold (Symtab.insert (op =)) (ordered_names ~~ (1 upto length ordered_names))
wenzelm@59058
   203
    val name_ord = int_ord o apply2 (the o Symtab.lookup order_tab)
blanchet@51646
   204
  in
blanchet@61323
   205
    (facts,
blanchet@61323
   206
     problem
blanchet@61323
   207
     |> (case format of
blanchet@51646
   208
          DFG _ => I
blanchet@61323
   209
        | _ => add_inferences_to_problem ctxt format (infer_policy = Checked_Inferences) prelude
blanchet@61323
   210
          infers)
blanchet@61323
   211
     |> order_problem_facts name_ord)
blanchet@51646
   212
  end
blanchet@51646
   213
blanchet@51998
   214
fun lines_of_problem ctxt format =
blanchet@51998
   215
  lines_of_atp_problem format (effective_term_order ctxt eN (* dummy *)) (K [])
blanchet@51646
   216
blanchet@51646
   217
fun write_lines path ss =
blanchet@51646
   218
  let
blanchet@51646
   219
    val _ = File.write path ""
blanchet@42602
   220
    val _ = app (File.append path) ss
blanchet@42602
   221
  in () end
blanchet@42602
   222
blanchet@51646
   223
fun generate_atp_inference_file_for_theory ctxt thy format infer_policy type_enc
blanchet@51646
   224
                                           file_name =
blanchet@51646
   225
  let
blanchet@61323
   226
    val (_, problem) = problem_of_theory ctxt thy format infer_policy type_enc
blanchet@51998
   227
    val ss = lines_of_problem ctxt format problem
blanchet@51646
   228
  in write_lines (Path.explode file_name) ss end
blanchet@51646
   229
blanchet@51646
   230
fun ap dir = Path.append dir o Path.explode
blanchet@51646
   231
blanchet@51646
   232
fun chop_maximal_groups eq xs =
blanchet@51646
   233
  let
blanchet@51646
   234
    val rev_xs = rev xs
blanchet@51646
   235
    fun chop_group _ [] = []
blanchet@51646
   236
      | chop_group n (xs as x :: _) =
blanchet@51646
   237
        let
blanchet@51646
   238
          val n' = find_index (curry eq x) rev_xs
blanchet@51646
   239
          val (ws', xs') = chop (n - n') xs
blanchet@51646
   240
        in ws' :: chop_group n' xs' end
blanchet@51646
   241
   in chop_group (length xs) xs end
blanchet@51646
   242
blanchet@51646
   243
fun theory_name_of_fact (Formula ((_, alt), _, _, _, _)) =
blanchet@51646
   244
    (case first_field Long_Name.separator alt of
blanchet@51646
   245
       NONE => alt
blanchet@51646
   246
     | SOME (thy, _) => thy)
blanchet@51646
   247
  | theory_name_of_fact _ = ""
blanchet@51646
   248
blanchet@51646
   249
val problem_suffix = ".p"
blanchet@61323
   250
val suggestion_suffix = ".sugg"
blanchet@51646
   251
val include_suffix = ".ax"
blanchet@51646
   252
blanchet@51646
   253
val file_order_name = "FilesInProcessingOrder"
blanchet@51646
   254
val problem_order_name = "ProblemsInProcessingOrder"
blanchet@51646
   255
val problem_name = "problems"
blanchet@61323
   256
val suggestion_name = "suggestions"
blanchet@51646
   257
val include_name = "incl"
blanchet@51646
   258
val prelude_base_name = "prelude"
blanchet@51646
   259
val prelude_name = prelude_base_name ^ include_suffix
blanchet@51646
   260
blanchet@51652
   261
val encode_meta = Sledgehammer_MaSh.encode_str
blanchet@51652
   262
wenzelm@53980
   263
fun include_base_name_of_fact x = encode_meta (theory_name_of_fact x)
blanchet@51646
   264
blanchet@51646
   265
fun include_line base_name =
blanchet@51646
   266
  "include('" ^ include_name ^ "/" ^ base_name ^ include_suffix ^ "').\n"
blanchet@51646
   267
blanchet@51652
   268
val hol_base_name = encode_meta "HOL"
blanchet@51652
   269
blanchet@51652
   270
fun should_generate_problem thy base_name (Formula ((_, alt), _, _, _, _)) =
blanchet@61860
   271
  (case try (Global_Theory.get_thm thy) alt of
blanchet@51652
   272
    SOME th =>
blanchet@61860
   273
    (* This is a crude hack to detect theorems stated and proved by the user (as opposed to those
blanchet@61860
   274
       derived by various packages). In addition, we leave out everything in "HOL" as too basic to
blanchet@61860
   275
       be interesting. *)
blanchet@51652
   276
    Thm.legacy_get_kind th <> "" andalso base_name <> hol_base_name
blanchet@61860
   277
  | NONE => false)
blanchet@51646
   278
blanchet@51646
   279
(* Convention: theoryname__goalname *)
blanchet@51652
   280
fun problem_name_of base_name n alt =
blanchet@51652
   281
  base_name ^ "__" ^ string_of_int n ^ "_" ^
blanchet@51652
   282
  perhaps (try (unprefix (base_name ^ "_"))) alt ^ problem_suffix
blanchet@51646
   283
blanchet@61323
   284
fun suggestion_name_of base_name n alt =
blanchet@61323
   285
  base_name ^ "__" ^ string_of_int n ^ "_" ^
blanchet@61323
   286
  perhaps (try (unprefix (base_name ^ "_"))) alt ^ suggestion_suffix
blanchet@61323
   287
blanchet@61323
   288
fun generate_casc_lbt_isa_files_for_theory ctxt thy format infer_policy type_enc dir_name =
blanchet@51646
   289
  let
blanchet@51646
   290
    val dir = Path.explode dir_name
blanchet@51646
   291
    val _ = Isabelle_System.mkdir dir
blanchet@51646
   292
    val file_order_path = ap dir file_order_name
blanchet@51646
   293
    val _ = File.write file_order_path ""
blanchet@51646
   294
    val problem_order_path = ap dir problem_order_name
blanchet@51646
   295
    val _ = File.write problem_order_path ""
blanchet@51646
   296
    val problem_dir = ap dir problem_name
blanchet@51646
   297
    val _ = Isabelle_System.mkdir problem_dir
blanchet@61323
   298
    val suggestion_dir = ap dir suggestion_name
blanchet@61323
   299
    val _ = Isabelle_System.mkdir suggestion_dir
blanchet@51646
   300
    val include_dir = ap problem_dir include_name
blanchet@51646
   301
    val _ = Isabelle_System.mkdir include_dir
blanchet@61323
   302
blanchet@61323
   303
    val (facts, (prelude, groups)) =
blanchet@51998
   304
      problem_of_theory ctxt thy format infer_policy type_enc
blanchet@61323
   305
      ||> split_last
blanchet@61323
   306
      ||> apsnd (snd
wenzelm@59058
   307
           #> chop_maximal_groups (op = o apply2 theory_name_of_fact)
blanchet@51646
   308
           #> map (`(include_base_name_of_fact o hd)))
blanchet@61323
   309
blanchet@61323
   310
    val fact_tab = Symtab.make (map (fn fact as (_, th) => (Thm.get_name_hint th, fact)) facts)
blanchet@61323
   311
blanchet@51646
   312
    fun write_prelude () =
blanchet@51998
   313
      let val ss = lines_of_problem ctxt format prelude in
blanchet@51646
   314
        File.append file_order_path (prelude_base_name ^ "\n");
blanchet@51646
   315
        write_lines (ap include_dir prelude_name) ss
blanchet@51646
   316
      end
blanchet@61323
   317
blanchet@61323
   318
    fun write_include_file (base_name, fact_lines) =
blanchet@51646
   319
      let
blanchet@51646
   320
        val name = base_name ^ include_suffix
blanchet@61323
   321
        val ss = lines_of_problem ctxt format [(factsN, fact_lines)]
blanchet@51646
   322
      in
blanchet@51646
   323
        File.append file_order_path (base_name ^ "\n");
blanchet@51646
   324
        write_lines (ap include_dir name) ss
blanchet@51646
   325
      end
blanchet@61323
   326
blanchet@61323
   327
    fun select_facts_for_fact facts fact =
blanchet@61323
   328
      let
blanchet@61323
   329
        val (hyp_ts, conj_t) = Logic.strip_horn (Thm.prop_of (snd fact))
blanchet@61323
   330
        val mepo = Sledgehammer_MePo.mepo_suggested_facts ctxt
blanchet@61323
   331
          (Sledgehammer_Commands.default_params thy []) max_facts NONE hyp_ts conj_t facts
blanchet@61323
   332
      in
blanchet@61323
   333
        map (suffix "\n" o fact_name_of o Thm.get_name_hint o snd) mepo
blanchet@61323
   334
      end
blanchet@61323
   335
blanchet@61323
   336
    fun write_problem_files _ _ _ _ [] = ()
blanchet@61323
   337
      | write_problem_files _ seen_facts includes [] groups =
blanchet@61323
   338
        write_problem_files 1 seen_facts includes includes groups
blanchet@61323
   339
      | write_problem_files n seen_facts includes _ ((base_name, []) :: groups) =
blanchet@61323
   340
        write_problem_files n seen_facts (includes @ [include_line base_name]) [] groups
blanchet@61323
   341
      | write_problem_files n seen_facts includes seen_ss
blanchet@61323
   342
          ((base_name, fact_line :: fact_lines) :: groups) =
blanchet@61323
   343
        let
blanchet@61860
   344
          val (alt, pname, sname, conj) =
blanchet@61323
   345
            (case fact_line of
blanchet@61323
   346
              Formula ((ident, alt), _, phi, _, _) =>
blanchet@61860
   347
              (alt, problem_name_of base_name n (encode_meta alt),
blanchet@61323
   348
               suggestion_name_of base_name n (encode_meta alt),
blanchet@61323
   349
               Formula ((ident, alt), Conjecture, phi, NONE, [])))
blanchet@61323
   350
          val fact = the (Symtab.lookup fact_tab alt)
blanchet@61323
   351
          val fact_s = tptp_string_of_line format fact_line
blanchet@61323
   352
        in
blanchet@61323
   353
          (if should_generate_problem thy base_name fact_line then
blanchet@51646
   354
             let
blanchet@51998
   355
               val conj_s = tptp_string_of_line format conj
blanchet@51646
   356
             in
blanchet@61323
   357
               File.append problem_order_path (pname ^ "\n");
blanchet@61323
   358
               write_lines (ap problem_dir pname) (seen_ss @ [conj_s]);
blanchet@61323
   359
               write_lines (ap suggestion_dir sname) (select_facts_for_fact facts fact)
blanchet@51646
   360
             end
blanchet@51646
   361
           else
blanchet@51646
   362
             ();
blanchet@61323
   363
           write_problem_files (n + 1) (fact :: seen_facts) includes (seen_ss @ [fact_s])
blanchet@61323
   364
             ((base_name, fact_lines) :: groups))
blanchet@51646
   365
        end
blanchet@61323
   366
blanchet@51646
   367
    val _ = write_prelude ()
blanchet@51646
   368
    val _ = app write_include_file groups
blanchet@61323
   369
    val _ = write_problem_files 1 [] [include_line prelude_base_name] [] groups
blanchet@51646
   370
  in () end
blanchet@51646
   371
blanchet@42602
   372
end;