src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML
 changeset 38752 6628adcae4a7 parent 38748 69fea359d3f8 child 38786 e46e7a9cb622 child 38818 61cf050f8b2e
```     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML	Thu Aug 26 09:23:21 2010 +0200
1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML	Thu Aug 26 10:42:06 2010 +0200
1.3 @@ -18,8 +18,8 @@
1.4    val tfrees_name : string
1.5    val prepare_problem :
1.6      Proof.context -> bool -> bool -> bool -> bool -> term list -> term
1.7 -    -> ((string * bool) * thm) list
1.8 -    -> string problem * string Symtab.table * int * (string * bool) vector
1.9 +    -> ((string * 'a) * thm) list
1.10 +    -> string problem * string Symtab.table * int * (string * 'a) vector
1.11  end;
1.12
1.13  structure Sledgehammer_Translate : SLEDGEHAMMER_TRANSLATE =
1.14 @@ -39,11 +39,11 @@
1.15  (* Freshness almost guaranteed! *)
1.16  val sledgehammer_weak_prefix = "Sledgehammer:"
1.17
1.18 -datatype fol_formula =
1.19 -  FOLFormula of {name: string,
1.20 -                 kind: kind,
1.21 -                 combformula: (name, combterm) formula,
1.22 -                 ctypes_sorts: typ list}
1.23 +type fol_formula =
1.24 +  {name: string,
1.25 +   kind: kind,
1.26 +   combformula: (name, combterm) formula,
1.27 +   ctypes_sorts: typ list}
1.28
1.29  fun mk_anot phi = AConn (ANot, [phi])
1.30  fun mk_aconn c phi1 phi2 = AConn (c, [phi1, phi2])
1.31 @@ -190,15 +190,14 @@
1.32                |> kind <> Axiom ? freeze_term
1.33      val (combformula, ctypes_sorts) = combformula_for_prop thy t []
1.34    in
1.35 -    FOLFormula {name = name, combformula = combformula, kind = kind,
1.36 -                ctypes_sorts = ctypes_sorts}
1.37 +    {name = name, combformula = combformula, kind = kind,
1.38 +     ctypes_sorts = ctypes_sorts}
1.39    end
1.40
1.41 -fun make_axiom ctxt presimp ((name, chained), th) =
1.42 +fun make_axiom ctxt presimp ((name, loc), th) =
1.43    case make_formula ctxt presimp name Axiom (prop_of th) of
1.44 -    FOLFormula {combformula = AAtom (CombConst (("c_True", _), _, _)), ...} =>
1.45 -    NONE
1.46 -  | formula => SOME ((name, chained), formula)
1.47 +    {combformula = AAtom (CombConst (("c_True", _), _, _)), ...} => NONE
1.48 +  | formula => SOME ((name, loc), formula)
1.49  fun make_conjecture ctxt ts =
1.50    let val last = length ts - 1 in
1.51      map2 (fn j => make_formula ctxt true (Int.toString j)
1.52 @@ -215,7 +214,7 @@
1.53  fun count_combformula (AQuant (_, _, phi)) = count_combformula phi
1.54    | count_combformula (AConn (_, phis)) = fold count_combformula phis
1.55    | count_combformula (AAtom tm) = count_combterm tm
1.56 -fun count_fol_formula (FOLFormula {combformula, ...}) =
1.57 +fun count_fol_formula ({combformula, ...} : fol_formula) =
1.58    count_combformula combformula
1.59
1.60  val optional_helpers =
1.61 @@ -326,13 +325,13 @@
1.62        | aux (AAtom tm) = AAtom (fo_term_for_combterm full_types tm)
1.63    in aux end
1.64
1.65 -fun formula_for_axiom full_types (FOLFormula {combformula, ctypes_sorts, ...}) =
1.66 +fun formula_for_axiom full_types
1.67 +                      ({combformula, ctypes_sorts, ...} : fol_formula) =
1.68    mk_ahorn (map (formula_for_fo_literal o fo_literal_for_type_literal)
1.69                  (type_literals_for_types ctypes_sorts))
1.70             (formula_for_combformula full_types combformula)
1.71
1.72 -fun problem_line_for_fact prefix full_types
1.73 -                          (formula as FOLFormula {name, kind, ...}) =
1.74 +fun problem_line_for_fact prefix full_types (formula as {name, kind, ...}) =
1.75    Fof (prefix ^ ascii_of name, kind, formula_for_axiom full_types formula)
1.76
1.77  fun problem_line_for_class_rel_clause (ClassRelClause {name, subclass,
1.78 @@ -357,11 +356,11 @@
1.79                       (fo_literal_for_arity_literal conclLit)))
1.80
1.81  fun problem_line_for_conjecture full_types
1.82 -                                (FOLFormula {name, kind, combformula, ...}) =
1.83 +                                ({name, kind, combformula, ...} : fol_formula) =
1.84    Fof (conjecture_prefix ^ name, kind,
1.85         formula_for_combformula full_types combformula)
1.86
1.87 -fun free_type_literals_for_conjecture (FOLFormula {ctypes_sorts, ...}) =
1.88 +fun free_type_literals_for_conjecture ({ctypes_sorts, ...} : fol_formula) =
1.89    map fo_literal_for_type_literal (type_literals_for_types ctypes_sorts)
1.90
1.91  fun problem_line_for_free_type lit =
```