1.1 --- a/src/HOL/Tools/ATP/atp_problem.ML Sun May 01 18:37:24 2011 +0200
1.2 +++ b/src/HOL/Tools/ATP/atp_problem.ML Sun May 01 18:37:24 2011 +0200
1.3 @@ -10,16 +10,15 @@
1.4 datatype 'a fo_term = ATerm of 'a * 'a fo_term list
1.5 datatype quantifier = AForall | AExists
1.6 datatype connective = ANot | AAnd | AOr | AImplies | AIf | AIff | ANotIff
1.7 - datatype ('a, 'b) formula =
1.8 - AQuant of quantifier * ('a * 'b option) list * ('a, 'b) formula |
1.9 - AConn of connective * ('a, 'b) formula list |
1.10 - AAtom of 'b
1.11 - type 'a uniform_formula = ('a, 'a fo_term) formula
1.12 + datatype ('a, 'b, 'c) formula =
1.13 + AQuant of quantifier * ('a * 'b option) list * ('a, 'b, 'c) formula |
1.14 + AConn of connective * ('a, 'b, 'c) formula list |
1.15 + AAtom of 'c
1.16
1.17 datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture
1.18 datatype 'a problem_line =
1.19 Type_Decl of string * 'a * 'a list * 'a |
1.20 - Formula of string * formula_kind * ('a, 'a fo_term) formula
1.21 + Formula of string * formula_kind * ('a, 'a, 'a fo_term) formula
1.22 * string fo_term option * string fo_term option
1.23 type 'a problem = (string * 'a problem_line list) list
1.24
1.25 @@ -41,16 +40,15 @@
1.26 datatype 'a fo_term = ATerm of 'a * 'a fo_term list
1.27 datatype quantifier = AForall | AExists
1.28 datatype connective = ANot | AAnd | AOr | AImplies | AIf | AIff | ANotIff
1.29 -datatype ('a, 'b) formula =
1.30 - AQuant of quantifier * ('a * 'b option) list * ('a, 'b) formula |
1.31 - AConn of connective * ('a, 'b) formula list |
1.32 - AAtom of 'b
1.33 -type 'a uniform_formula = ('a, 'a fo_term) formula
1.34 +datatype ('a, 'b, 'c) formula =
1.35 + AQuant of quantifier * ('a * 'b option) list * ('a, 'b, 'c) formula |
1.36 + AConn of connective * ('a, 'b, 'c) formula list |
1.37 + AAtom of 'c
1.38
1.39 datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture
1.40 datatype 'a problem_line =
1.41 Type_Decl of string * 'a * 'a list * 'a |
1.42 - Formula of string * formula_kind * ('a, 'a fo_term) formula
1.43 + Formula of string * formula_kind * ('a, 'a, 'a fo_term) formula
1.44 * string fo_term option * string fo_term option
1.45 type 'a problem = (string * 'a problem_line list) list
1.46
1.47 @@ -80,7 +78,7 @@
1.48 | string_for_connective AIff = "<=>"
1.49 | string_for_connective ANotIff = "<~>"
1.50 fun string_for_bound_var (s, NONE) = s
1.51 - | string_for_bound_var (s, SOME ty) = s ^ " : " ^ string_for_term ty
1.52 + | string_for_bound_var (s, SOME ty) = s ^ " : " ^ ty
1.53 fun string_for_formula (AQuant (q, xs, phi)) =
1.54 "(" ^ string_for_quantifier q ^
1.55 "[" ^ commas (map string_for_bound_var xs) ^ "] : " ^
1.56 @@ -201,7 +199,7 @@
1.57 fun nice_formula (AQuant (q, xs, phi)) =
1.58 pool_map nice_name (map fst xs)
1.59 ##>> pool_map (fn NONE => pair NONE
1.60 - | SOME ty => nice_term ty #>> SOME) (map snd xs)
1.61 + | SOME ty => nice_name ty #>> SOME) (map snd xs)
1.62 ##>> nice_formula phi
1.63 #>> (fn ((ss, ts), phi) => AQuant (q, ss ~~ ts, phi))
1.64 | nice_formula (AConn (c, phis)) =
2.1 --- a/src/HOL/Tools/ATP/atp_proof.ML Sun May 01 18:37:24 2011 +0200
2.2 +++ b/src/HOL/Tools/ATP/atp_proof.ML Sun May 01 18:37:24 2011 +0200
2.3 @@ -9,7 +9,7 @@
2.4 signature ATP_PROOF =
2.5 sig
2.6 type 'a fo_term = 'a ATP_Problem.fo_term
2.7 - type 'a uniform_formula = 'a ATP_Problem.uniform_formula
2.8 + type ('a, 'b, 'c) formula = ('a, 'b, 'c) ATP_Problem.formula
2.9
2.10 datatype failure =
2.11 Unprovable | IncompleteUnprovable | ProofMissing | UnsoundProof |
2.12 @@ -23,7 +23,7 @@
2.13 Definition of step_name * 'a * 'a |
2.14 Inference of step_name * 'a * step_name list
2.15
2.16 - type 'a proof = 'a uniform_formula step list
2.17 + type 'a proof = ('a, 'a, 'a fo_term) formula step list
2.18
2.19 val strip_spaces : (char -> bool) -> string -> string
2.20 val short_output : bool -> string -> string
2.21 @@ -203,7 +203,7 @@
2.22 Definition of step_name * 'a * 'a |
2.23 Inference of step_name * 'a * step_name list
2.24
2.25 -type 'a proof = 'a uniform_formula step list
2.26 +type 'a proof = ('a, 'a, 'a fo_term) formula step list
2.27
2.28 fun step_name (Definition (name, _, _)) = name
2.29 | step_name (Inference (name, _, _)) = name
3.1 --- a/src/HOL/Tools/Metis/metis_translate.ML Sun May 01 18:37:24 2011 +0200
3.2 +++ b/src/HOL/Tools/Metis/metis_translate.ML Sun May 01 18:37:24 2011 +0200
3.3 @@ -68,6 +68,7 @@
3.4 theory -> string list -> class list -> class list * arity_clause list
3.5 val combtyp_of : combterm -> combtyp
3.6 val strip_combterm_comb : combterm -> combterm * combterm list
3.7 + val combtyp_from_typ : typ -> combtyp
3.8 val combterm_from_term :
3.9 theory -> (string * typ) list -> term -> combterm * typ list
3.10 val reveal_old_skolem_terms : (string * term) list -> term -> term
3.11 @@ -393,23 +394,24 @@
3.12 | stripc x = x
3.13 in stripc(u,[]) end
3.14
3.15 -fun combtype_of (Type (a, Ts)) =
3.16 - let val (folTypes, ts) = combtypes_of Ts in
3.17 - (CombType (`make_fixed_type_const a, folTypes), ts)
3.18 +fun combtyp_and_sorts_from_type (Type (a, Ts)) =
3.19 + let val (tys, ts) = combtyps_and_sorts_from_types Ts in
3.20 + (CombType (`make_fixed_type_const a, tys), ts)
3.21 end
3.22 - | combtype_of (tp as TFree (a, _)) = (CombTFree (`make_fixed_type_var a), [tp])
3.23 - | combtype_of (tp as TVar (x, _)) =
3.24 + | combtyp_and_sorts_from_type (tp as TFree (a, _)) =
3.25 + (CombTFree (`make_fixed_type_var a), [tp])
3.26 + | combtyp_and_sorts_from_type (tp as TVar (x, _)) =
3.27 (CombTVar (make_schematic_type_var x, string_of_indexname x), [tp])
3.28 -and combtypes_of Ts =
3.29 - let val (folTyps, ts) = ListPair.unzip (map combtype_of Ts) in
3.30 - (folTyps, union_all ts)
3.31 +and combtyps_and_sorts_from_types Ts =
3.32 + let val (tys, ts) = ListPair.unzip (map combtyp_and_sorts_from_type Ts) in
3.33 + (tys, union_all ts)
3.34 end
3.35
3.36 (* same as above, but no gathering of sort information *)
3.37 -fun simple_combtype_of (Type (a, Ts)) =
3.38 - CombType (`make_fixed_type_const a, map simple_combtype_of Ts)
3.39 - | simple_combtype_of (TFree (a, _)) = CombTFree (`make_fixed_type_var a)
3.40 - | simple_combtype_of (TVar (x, _)) =
3.41 +fun combtyp_from_typ (Type (a, Ts)) =
3.42 + CombType (`make_fixed_type_const a, map combtyp_from_typ Ts)
3.43 + | combtyp_from_typ (TFree (a, _)) = CombTFree (`make_fixed_type_var a)
3.44 + | combtyp_from_typ (TVar (x, _)) =
3.45 CombTVar (make_schematic_type_var x, string_of_indexname x)
3.46
3.47 fun new_skolem_const_name s num_T_args =
3.48 @@ -425,37 +427,35 @@
3.49 in (CombApp (P', Q'), union (op =) tsP tsQ) end
3.50 | combterm_from_term thy _ (Const (c, T)) =
3.51 let
3.52 - val (tp, ts) = combtype_of T
3.53 + val (tp, ts) = combtyp_and_sorts_from_type T
3.54 val tvar_list =
3.55 (if String.isPrefix old_skolem_const_prefix c then
3.56 [] |> Term.add_tvarsT T |> map TVar
3.57 else
3.58 (c, T) |> Sign.const_typargs thy)
3.59 - |> map simple_combtype_of
3.60 + |> map combtyp_from_typ
3.61 val c' = CombConst (`make_fixed_const c, tp, tvar_list)
3.62 in (c',ts) end
3.63 | combterm_from_term _ _ (Free (v, T)) =
3.64 - let val (tp, ts) = combtype_of T
3.65 + let val (tp, ts) = combtyp_and_sorts_from_type T
3.66 val v' = CombConst (`make_fixed_var v, tp, [])
3.67 in (v',ts) end
3.68 | combterm_from_term _ _ (Var (v as (s, _), T)) =
3.69 let
3.70 - val (tp, ts) = combtype_of T
3.71 + val (tp, ts) = combtyp_and_sorts_from_type T
3.72 val v' =
3.73 if String.isPrefix Meson_Clausify.new_skolem_var_prefix s then
3.74 let
3.75 val tys = T |> strip_type |> swap |> op ::
3.76 val s' = new_skolem_const_name s (length tys)
3.77 - in
3.78 - CombConst (`make_fixed_const s', tp, map simple_combtype_of tys)
3.79 - end
3.80 + in CombConst (`make_fixed_const s', tp, map combtyp_from_typ tys) end
3.81 else
3.82 CombVar ((make_schematic_var v, string_of_indexname v), tp)
3.83 in (v', ts) end
3.84 | combterm_from_term _ bs (Bound j) =
3.85 let
3.86 val (s, T) = nth bs j
3.87 - val (tp, ts) = combtype_of T
3.88 + val (tp, ts) = combtyp_and_sorts_from_type T
3.89 val v' = CombConst (`make_bound_var s, tp, [])
3.90 in (v', ts) end
3.91 | combterm_from_term _ _ (Abs _) = raise Fail "HOL clause: Abs"
4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Sun May 01 18:37:24 2011 +0200
4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Sun May 01 18:37:24 2011 +0200
4.3 @@ -272,7 +272,7 @@
4.4 (**** INTERPRETATION OF TSTP SYNTAX TREES ****)
4.5
4.6 exception FO_TERM of string fo_term list
4.7 -exception FORMULA of (string, string fo_term) formula list
4.8 +exception FORMULA of (string, string, string fo_term) formula list
4.9 exception SAME of unit
4.10
4.11 (* Type variables are given the basic sort "HOL.type". Some will later be
5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Sun May 01 18:37:24 2011 +0200
5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Sun May 01 18:37:24 2011 +0200
5.3 @@ -49,13 +49,18 @@
5.4 val arity_clause_prefix = "arity_"
5.5 val tfree_prefix = "tfree_"
5.6
5.7 +val is_base = "is"
5.8 +val type_prefix = "ty_"
5.9 +
5.10 +fun make_type ty = type_prefix ^ ascii_of ty
5.11 +
5.12 (* Freshness almost guaranteed! *)
5.13 val sledgehammer_weak_prefix = "Sledgehammer:"
5.14
5.15 type translated_formula =
5.16 {name: string,
5.17 kind: formula_kind,
5.18 - combformula: (name, combterm) formula,
5.19 + combformula: (name, combtyp, combterm) formula,
5.20 ctypes_sorts: typ list}
5.21
5.22 datatype type_system =
5.23 @@ -75,13 +80,14 @@
5.24 | type_system_types_dangerous_types type_sys = is_type_system_sound type_sys
5.25
5.26 fun dont_need_type_args type_sys s =
5.27 - member (op =) [@{const_name HOL.eq}, @{const_name Metis.fequal}] s orelse
5.28 - case type_sys of
5.29 - Many_Typed => true
5.30 - | Tags full_types => full_types
5.31 - | Args full_types => full_types
5.32 - | Mangled full_types => full_types
5.33 - | No_Types => true
5.34 + s <> is_base andalso
5.35 + (member (op =) [@{const_name HOL.eq}, @{const_name Metis.fequal}] s orelse
5.36 + case type_sys of
5.37 + Many_Typed => true
5.38 + | Tags full_types => full_types
5.39 + | Args full_types => full_types
5.40 + | Mangled full_types => full_types
5.41 + | No_Types => true)
5.42
5.43 datatype type_arg_policy = No_Type_Args | Explicit_Type_Args | Mangled_Types
5.44
5.45 @@ -90,8 +96,10 @@
5.46 else case type_sys of Mangled _ => Mangled_Types | _ => Explicit_Type_Args
5.47
5.48 fun num_atp_type_args thy type_sys s =
5.49 - if type_arg_policy type_sys s = Explicit_Type_Args then num_type_args thy s
5.50 - else 0
5.51 + if type_arg_policy type_sys s = Explicit_Type_Args then
5.52 + if s = is_base then 1 else num_type_args thy s
5.53 + else
5.54 + 0
5.55
5.56 fun atp_type_literals_for_types type_sys kind Ts =
5.57 if type_sys = No_Types then
5.58 @@ -121,14 +129,13 @@
5.59 |> filter_out (member (op =) bounds o fst))
5.60 in mk_aquant AForall (formula_vars [] phi []) phi end
5.61
5.62 -fun combterm_vars (CombApp (ct, cu)) = fold combterm_vars [ct, cu]
5.63 +fun combterm_vars (CombApp (tm1, tm2)) = fold combterm_vars [tm1, tm2]
5.64 | combterm_vars (CombConst _) = I
5.65 - | combterm_vars (CombVar (name, _)) =
5.66 - insert (op =) (name, NONE) (* FIXME: TFF *)
5.67 + | combterm_vars (CombVar (name, ty)) = insert (op =) (name, SOME ty)
5.68 val close_combformula_universally = close_universally combterm_vars
5.69
5.70 fun term_vars (ATerm (name as (s, _), tms)) =
5.71 - is_atp_variable s ? insert (op =) (name, NONE) (* FIXME: TFF *)
5.72 + is_atp_variable s ? insert (op =) (name, NONE)
5.73 #> fold term_vars tms
5.74 val close_formula_universally = close_universally term_vars
5.75
5.76 @@ -140,16 +147,14 @@
5.77 fun do_quant bs q s T t' =
5.78 let val s = Name.variant (map fst bs) s in
5.79 do_formula ((s, T) :: bs) t'
5.80 - (* FIXME: TFF *)
5.81 - #>> (fn phi => AQuant (q, [(`make_bound_var s, NONE)], phi))
5.82 + #>> mk_aquant q [(`make_bound_var s, SOME (combtyp_from_typ T))]
5.83 end
5.84 and do_conn bs c t1 t2 =
5.85 do_formula bs t1 ##>> do_formula bs t2
5.86 - #>> (fn (phi1, phi2) => AConn (c, [phi1, phi2]))
5.87 + #>> uncurry (mk_aconn c)
5.88 and do_formula bs t =
5.89 case t of
5.90 - @{const Not} $ t1 =>
5.91 - do_formula bs t1 #>> (fn phi => AConn (ANot, [phi]))
5.92 + @{const Not} $ t1 => do_formula bs t1 #>> mk_anot
5.93 | Const (@{const_name All}, _) $ Abs (s, T, t') =>
5.94 do_quant bs AForall s T t'
5.95 | Const (@{const_name Ex}, _) $ Abs (s, T, t') =>
5.96 @@ -414,16 +419,20 @@
5.97 (* We are crossing our fingers that it doesn't clash with anything else. *)
5.98 val mangled_type_sep = "\000"
5.99
5.100 -fun mangled_combtyp f (CombTFree name) = f name
5.101 - | mangled_combtyp f (CombTVar name) =
5.102 +fun mangled_combtyp_component f (CombTFree name) = f name
5.103 + | mangled_combtyp_component f (CombTVar name) =
5.104 f name (* FIXME: shouldn't happen *)
5.105 (* raise Fail "impossible schematic type variable" *)
5.106 - | mangled_combtyp f (CombType (name, tys)) =
5.107 - "(" ^ commas (map (mangled_combtyp f) tys) ^ ")" ^ f name
5.108 + | mangled_combtyp_component f (CombType (name, tys)) =
5.109 + "(" ^ commas (map (mangled_combtyp_component f) tys) ^ ")" ^ f name
5.110 +
5.111 +fun mangled_combtyp ty =
5.112 + (make_type (mangled_combtyp_component fst ty),
5.113 + mangled_combtyp_component snd ty)
5.114
5.115 fun mangled_type_suffix f g tys =
5.116 - fold_rev (curry (op ^) o g o prefix mangled_type_sep o mangled_combtyp f)
5.117 - tys ""
5.118 + fold_rev (curry (op ^) o g o prefix mangled_type_sep
5.119 + o mangled_combtyp_component f) tys ""
5.120
5.121 val parse_mangled_ident =
5.122 Scan.many1 (not o member (op =) ["(", ")", ","]) >> implode
5.123 @@ -447,6 +456,11 @@
5.124 (hd ss, map unmangled_type (tl ss))
5.125 end
5.126
5.127 +fun pred_combtyp ty =
5.128 + case combtyp_from_typ @{typ "unit => bool"} of
5.129 + CombType (name, [_, bool_ty]) => CombType (name, [ty, bool_ty])
5.130 + | _ => raise Fail "expected two-argument type constructor"
5.131 +
5.132 fun formula_for_combformula ctxt type_sys =
5.133 let
5.134 fun do_term top_level u =
5.135 @@ -487,8 +501,25 @@
5.136 else
5.137 I)
5.138 end
5.139 + val do_bound_type =
5.140 + if type_sys = Many_Typed then SOME o mangled_combtyp else K NONE
5.141 + val do_out_of_bound_type =
5.142 + if member (op =) [Args true, Mangled true] type_sys then
5.143 + (fn (s, ty) =>
5.144 + CombApp (CombConst ((const_prefix ^ is_base, is_base),
5.145 + pred_combtyp ty, [ty]),
5.146 + CombVar (s, ty))
5.147 + |> AAtom |> formula_for_combformula ctxt type_sys |> SOME)
5.148 + else
5.149 + K NONE
5.150 fun do_formula (AQuant (q, xs, phi)) =
5.151 - AQuant (q, map (apsnd (Option.map (do_term true))) xs, do_formula phi)
5.152 + AQuant (q, xs |> map (apsnd (fn NONE => NONE
5.153 + | SOME ty => do_bound_type ty)),
5.154 + (if q = AForall then mk_ahorn else fold (mk_aconn AAnd))
5.155 + (map_filter
5.156 + (fn (_, NONE) => NONE
5.157 + | (s, SOME ty) => do_out_of_bound_type (s, ty)) xs)
5.158 + (do_formula phi))
5.159 | do_formula (AConn (c, phis)) = AConn (c, map do_formula phis)
5.160 | do_formula (AAtom tm) = AAtom (do_term true tm)
5.161 in do_formula end