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 =