src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML
changeset 36169 27b1cc58715e
parent 36168 0a6ed065683d
child 36170 0cdb76723c88
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Thu Apr 15 13:57:17 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Fri Apr 16 14:48:34 2010 +0200
     1.3 @@ -33,11 +33,11 @@
     1.4    val get_helper_clauses : bool -> theory -> bool ->
     1.5         hol_clause list * (thm * (axiom_name * hol_clause_id)) list * string list ->
     1.6         hol_clause list
     1.7 -  val write_tptp_file : bool -> Path.T ->
     1.8 +  val write_tptp_file : bool -> bool -> Path.T ->
     1.9      hol_clause list * hol_clause list * hol_clause list * hol_clause list *
    1.10      classrel_clause list * arity_clause list ->
    1.11      int * int
    1.12 -  val write_dfg_file : bool -> Path.T ->
    1.13 +  val write_dfg_file : bool -> bool -> Path.T ->
    1.14      hol_clause list * hol_clause list * hol_clause list * hol_clause list *
    1.15      classrel_clause list * arity_clause list -> int * int
    1.16  end
    1.17 @@ -102,19 +102,22 @@
    1.18  fun isTaut (HOLClause {literals,...}) = exists isTrue literals;
    1.19  
    1.20  fun type_of dfg (Type (a, Ts)) =
    1.21 -      let val (folTypes,ts) = types_of dfg Ts
    1.22 -      in  (TyConstr (make_fixed_type_const dfg a, folTypes), ts)  end
    1.23 -  | type_of _ (tp as TFree (a, _)) = (TyFree (make_fixed_type_var a), [tp])
    1.24 -  | type_of _ (tp as TVar (v, _)) = (TyVar (make_schematic_type_var v), [tp])
    1.25 +    let val (folTypes,ts) = types_of dfg Ts in
    1.26 +      (TyConstr (`(make_fixed_type_const dfg) a, folTypes), ts)
    1.27 +    end
    1.28 +  | type_of _ (tp as TFree (a, _)) = (TyFree (`make_fixed_type_var a), [tp])
    1.29 +  | type_of _ (tp as TVar (x, _)) =
    1.30 +    (TyVar (make_schematic_type_var x, string_of_indexname x), [tp])
    1.31  and types_of dfg Ts =
    1.32        let val (folTyps,ts) = ListPair.unzip (map (type_of dfg) Ts)
    1.33        in  (folTyps, union_all ts)  end;
    1.34  
    1.35  (* same as above, but no gathering of sort information *)
    1.36  fun simp_type_of dfg (Type (a, Ts)) =
    1.37 -      TyConstr (make_fixed_type_const dfg a, map (simp_type_of dfg) Ts)
    1.38 -  | simp_type_of _ (TFree (a, _)) = TyFree (make_fixed_type_var a)
    1.39 -  | simp_type_of _ (TVar (v, _)) = TyVar (make_schematic_type_var v);
    1.40 +      TyConstr (`(make_fixed_type_const dfg) a, map (simp_type_of dfg) Ts)
    1.41 +  | simp_type_of _ (TFree (a, _)) = TyFree (`make_fixed_type_var a)
    1.42 +  | simp_type_of _ (TVar (x, _)) =
    1.43 +    TyVar (make_schematic_type_var x, string_of_indexname x);
    1.44  
    1.45  
    1.46  fun const_type_of dfg thy (c,t) =
    1.47 @@ -193,7 +196,7 @@
    1.48  (**********************************************************************)
    1.49  
    1.50  (*Result of a function type; no need to check that the argument type matches.*)
    1.51 -fun result_type (TyConstr ("tc_fun", [_, tp2])) = tp2
    1.52 +fun result_type (TyConstr (("tc_fun", _), [_, tp2])) = tp2
    1.53    | result_type _ = raise Fail "Non-function type"
    1.54  
    1.55  fun type_of_combterm (CombConst (_, tp, _)) = tp
    1.56 @@ -452,7 +455,7 @@
    1.57  
    1.58  (* TPTP format *)
    1.59  
    1.60 -fun write_tptp_file full_types file clauses =
    1.61 +fun write_tptp_file debug full_types file clauses =
    1.62    let
    1.63      fun section _ [] = []
    1.64        | section name ss = "\n% " ^ name ^ plural_s (length ss) ^ "\n" :: ss
    1.65 @@ -480,7 +483,7 @@
    1.66  
    1.67  (* DFG format *)
    1.68  
    1.69 -fun write_dfg_file full_types file clauses =
    1.70 +fun write_dfg_file debug full_types file clauses =
    1.71    let
    1.72      val (conjectures, axclauses, _, helper_clauses,
    1.73        classrel_clauses, arity_clauses) = clauses