# HG changeset patch # User blanchet # Date 1304267844 -7200 # Node ID a462dbaa584f903c0b1300850a48046042665d0a # Parent f64c546efe8c70b1cb4b92b53b9add721c574976 added more rudimentary type support to Sledgehammer's ATP encoding diff -r f64c546efe8c -r a462dbaa584f src/HOL/Tools/ATP/atp_problem.ML --- a/src/HOL/Tools/ATP/atp_problem.ML Sun May 01 18:37:24 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_problem.ML Sun May 01 18:37:24 2011 +0200 @@ -10,16 +10,15 @@ datatype 'a fo_term = ATerm of 'a * 'a fo_term list datatype quantifier = AForall | AExists datatype connective = ANot | AAnd | AOr | AImplies | AIf | AIff | ANotIff - datatype ('a, 'b) formula = - AQuant of quantifier * ('a * 'b option) list * ('a, 'b) formula | - AConn of connective * ('a, 'b) formula list | - AAtom of 'b - type 'a uniform_formula = ('a, 'a fo_term) formula + datatype ('a, 'b, 'c) formula = + AQuant of quantifier * ('a * 'b option) list * ('a, 'b, 'c) formula | + AConn of connective * ('a, 'b, 'c) formula list | + AAtom of 'c datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture datatype 'a problem_line = Type_Decl of string * 'a * 'a list * 'a | - Formula of string * formula_kind * ('a, 'a fo_term) formula + Formula of string * formula_kind * ('a, 'a, 'a fo_term) formula * string fo_term option * string fo_term option type 'a problem = (string * 'a problem_line list) list @@ -41,16 +40,15 @@ datatype 'a fo_term = ATerm of 'a * 'a fo_term list datatype quantifier = AForall | AExists datatype connective = ANot | AAnd | AOr | AImplies | AIf | AIff | ANotIff -datatype ('a, 'b) formula = - AQuant of quantifier * ('a * 'b option) list * ('a, 'b) formula | - AConn of connective * ('a, 'b) formula list | - AAtom of 'b -type 'a uniform_formula = ('a, 'a fo_term) formula +datatype ('a, 'b, 'c) formula = + AQuant of quantifier * ('a * 'b option) list * ('a, 'b, 'c) formula | + AConn of connective * ('a, 'b, 'c) formula list | + AAtom of 'c datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture datatype 'a problem_line = Type_Decl of string * 'a * 'a list * 'a | - Formula of string * formula_kind * ('a, 'a fo_term) formula + Formula of string * formula_kind * ('a, 'a, 'a fo_term) formula * string fo_term option * string fo_term option type 'a problem = (string * 'a problem_line list) list @@ -80,7 +78,7 @@ | string_for_connective AIff = "<=>" | string_for_connective ANotIff = "<~>" fun string_for_bound_var (s, NONE) = s - | string_for_bound_var (s, SOME ty) = s ^ " : " ^ string_for_term ty + | string_for_bound_var (s, SOME ty) = s ^ " : " ^ ty fun string_for_formula (AQuant (q, xs, phi)) = "(" ^ string_for_quantifier q ^ "[" ^ commas (map string_for_bound_var xs) ^ "] : " ^ @@ -201,7 +199,7 @@ fun nice_formula (AQuant (q, xs, phi)) = pool_map nice_name (map fst xs) ##>> pool_map (fn NONE => pair NONE - | SOME ty => nice_term ty #>> SOME) (map snd xs) + | SOME ty => nice_name ty #>> SOME) (map snd xs) ##>> nice_formula phi #>> (fn ((ss, ts), phi) => AQuant (q, ss ~~ ts, phi)) | nice_formula (AConn (c, phis)) = diff -r f64c546efe8c -r a462dbaa584f src/HOL/Tools/ATP/atp_proof.ML --- a/src/HOL/Tools/ATP/atp_proof.ML Sun May 01 18:37:24 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_proof.ML Sun May 01 18:37:24 2011 +0200 @@ -9,7 +9,7 @@ signature ATP_PROOF = sig type 'a fo_term = 'a ATP_Problem.fo_term - type 'a uniform_formula = 'a ATP_Problem.uniform_formula + type ('a, 'b, 'c) formula = ('a, 'b, 'c) ATP_Problem.formula datatype failure = Unprovable | IncompleteUnprovable | ProofMissing | UnsoundProof | @@ -23,7 +23,7 @@ Definition of step_name * 'a * 'a | Inference of step_name * 'a * step_name list - type 'a proof = 'a uniform_formula step list + type 'a proof = ('a, 'a, 'a fo_term) formula step list val strip_spaces : (char -> bool) -> string -> string val short_output : bool -> string -> string @@ -203,7 +203,7 @@ Definition of step_name * 'a * 'a | Inference of step_name * 'a * step_name list -type 'a proof = 'a uniform_formula step list +type 'a proof = ('a, 'a, 'a fo_term) formula step list fun step_name (Definition (name, _, _)) = name | step_name (Inference (name, _, _)) = name diff -r f64c546efe8c -r a462dbaa584f src/HOL/Tools/Metis/metis_translate.ML --- a/src/HOL/Tools/Metis/metis_translate.ML Sun May 01 18:37:24 2011 +0200 +++ b/src/HOL/Tools/Metis/metis_translate.ML Sun May 01 18:37:24 2011 +0200 @@ -68,6 +68,7 @@ theory -> string list -> class list -> class list * arity_clause list val combtyp_of : combterm -> combtyp val strip_combterm_comb : combterm -> combterm * combterm list + val combtyp_from_typ : typ -> combtyp val combterm_from_term : theory -> (string * typ) list -> term -> combterm * typ list val reveal_old_skolem_terms : (string * term) list -> term -> term @@ -393,23 +394,24 @@ | stripc x = x in stripc(u,[]) end -fun combtype_of (Type (a, Ts)) = - let val (folTypes, ts) = combtypes_of Ts in - (CombType (`make_fixed_type_const a, folTypes), ts) +fun combtyp_and_sorts_from_type (Type (a, Ts)) = + let val (tys, ts) = combtyps_and_sorts_from_types Ts in + (CombType (`make_fixed_type_const a, tys), ts) end - | combtype_of (tp as TFree (a, _)) = (CombTFree (`make_fixed_type_var a), [tp]) - | combtype_of (tp as TVar (x, _)) = + | combtyp_and_sorts_from_type (tp as TFree (a, _)) = + (CombTFree (`make_fixed_type_var a), [tp]) + | combtyp_and_sorts_from_type (tp as TVar (x, _)) = (CombTVar (make_schematic_type_var x, string_of_indexname x), [tp]) -and combtypes_of Ts = - let val (folTyps, ts) = ListPair.unzip (map combtype_of Ts) in - (folTyps, union_all ts) +and combtyps_and_sorts_from_types Ts = + let val (tys, ts) = ListPair.unzip (map combtyp_and_sorts_from_type Ts) in + (tys, union_all ts) end (* same as above, but no gathering of sort information *) -fun simple_combtype_of (Type (a, Ts)) = - CombType (`make_fixed_type_const a, map simple_combtype_of Ts) - | simple_combtype_of (TFree (a, _)) = CombTFree (`make_fixed_type_var a) - | simple_combtype_of (TVar (x, _)) = +fun combtyp_from_typ (Type (a, Ts)) = + CombType (`make_fixed_type_const a, map combtyp_from_typ Ts) + | combtyp_from_typ (TFree (a, _)) = CombTFree (`make_fixed_type_var a) + | combtyp_from_typ (TVar (x, _)) = CombTVar (make_schematic_type_var x, string_of_indexname x) fun new_skolem_const_name s num_T_args = @@ -425,37 +427,35 @@ in (CombApp (P', Q'), union (op =) tsP tsQ) end | combterm_from_term thy _ (Const (c, T)) = let - val (tp, ts) = combtype_of T + val (tp, ts) = combtyp_and_sorts_from_type T val tvar_list = (if String.isPrefix old_skolem_const_prefix c then [] |> Term.add_tvarsT T |> map TVar else (c, T) |> Sign.const_typargs thy) - |> map simple_combtype_of + |> map combtyp_from_typ val c' = CombConst (`make_fixed_const c, tp, tvar_list) in (c',ts) end | combterm_from_term _ _ (Free (v, T)) = - let val (tp, ts) = combtype_of T + let val (tp, ts) = combtyp_and_sorts_from_type T val v' = CombConst (`make_fixed_var v, tp, []) in (v',ts) end | combterm_from_term _ _ (Var (v as (s, _), T)) = let - val (tp, ts) = combtype_of T + val (tp, ts) = combtyp_and_sorts_from_type T val v' = if String.isPrefix Meson_Clausify.new_skolem_var_prefix s then let val tys = T |> strip_type |> swap |> op :: val s' = new_skolem_const_name s (length tys) - in - CombConst (`make_fixed_const s', tp, map simple_combtype_of tys) - end + in CombConst (`make_fixed_const s', tp, map combtyp_from_typ tys) end else CombVar ((make_schematic_var v, string_of_indexname v), tp) in (v', ts) end | combterm_from_term _ bs (Bound j) = let val (s, T) = nth bs j - val (tp, ts) = combtype_of T + val (tp, ts) = combtyp_and_sorts_from_type T val v' = CombConst (`make_bound_var s, tp, []) in (v', ts) end | combterm_from_term _ _ (Abs _) = raise Fail "HOL clause: Abs" diff -r f64c546efe8c -r a462dbaa584f src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Sun May 01 18:37:24 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Sun May 01 18:37:24 2011 +0200 @@ -272,7 +272,7 @@ (**** INTERPRETATION OF TSTP SYNTAX TREES ****) exception FO_TERM of string fo_term list -exception FORMULA of (string, string fo_term) formula list +exception FORMULA of (string, string, string fo_term) formula list exception SAME of unit (* Type variables are given the basic sort "HOL.type". Some will later be diff -r f64c546efe8c -r a462dbaa584f src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Sun May 01 18:37:24 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Sun May 01 18:37:24 2011 +0200 @@ -49,13 +49,18 @@ val arity_clause_prefix = "arity_" val tfree_prefix = "tfree_" +val is_base = "is" +val type_prefix = "ty_" + +fun make_type ty = type_prefix ^ ascii_of ty + (* Freshness almost guaranteed! *) val sledgehammer_weak_prefix = "Sledgehammer:" type translated_formula = {name: string, kind: formula_kind, - combformula: (name, combterm) formula, + combformula: (name, combtyp, combterm) formula, ctypes_sorts: typ list} datatype type_system = @@ -75,13 +80,14 @@ | type_system_types_dangerous_types type_sys = is_type_system_sound type_sys fun dont_need_type_args type_sys s = - member (op =) [@{const_name HOL.eq}, @{const_name Metis.fequal}] s orelse - case type_sys of - Many_Typed => true - | Tags full_types => full_types - | Args full_types => full_types - | Mangled full_types => full_types - | No_Types => true + s <> is_base andalso + (member (op =) [@{const_name HOL.eq}, @{const_name Metis.fequal}] s orelse + case type_sys of + Many_Typed => true + | Tags full_types => full_types + | Args full_types => full_types + | Mangled full_types => full_types + | No_Types => true) datatype type_arg_policy = No_Type_Args | Explicit_Type_Args | Mangled_Types @@ -90,8 +96,10 @@ else case type_sys of Mangled _ => Mangled_Types | _ => Explicit_Type_Args fun num_atp_type_args thy type_sys s = - if type_arg_policy type_sys s = Explicit_Type_Args then num_type_args thy s - else 0 + if type_arg_policy type_sys s = Explicit_Type_Args then + if s = is_base then 1 else num_type_args thy s + else + 0 fun atp_type_literals_for_types type_sys kind Ts = if type_sys = No_Types then @@ -121,14 +129,13 @@ |> filter_out (member (op =) bounds o fst)) in mk_aquant AForall (formula_vars [] phi []) phi end -fun combterm_vars (CombApp (ct, cu)) = fold combterm_vars [ct, cu] +fun combterm_vars (CombApp (tm1, tm2)) = fold combterm_vars [tm1, tm2] | combterm_vars (CombConst _) = I - | combterm_vars (CombVar (name, _)) = - insert (op =) (name, NONE) (* FIXME: TFF *) + | combterm_vars (CombVar (name, ty)) = insert (op =) (name, SOME ty) val close_combformula_universally = close_universally combterm_vars fun term_vars (ATerm (name as (s, _), tms)) = - is_atp_variable s ? insert (op =) (name, NONE) (* FIXME: TFF *) + is_atp_variable s ? insert (op =) (name, NONE) #> fold term_vars tms val close_formula_universally = close_universally term_vars @@ -140,16 +147,14 @@ fun do_quant bs q s T t' = let val s = Name.variant (map fst bs) s in do_formula ((s, T) :: bs) t' - (* FIXME: TFF *) - #>> (fn phi => AQuant (q, [(`make_bound_var s, NONE)], phi)) + #>> mk_aquant q [(`make_bound_var s, SOME (combtyp_from_typ T))] end and do_conn bs c t1 t2 = do_formula bs t1 ##>> do_formula bs t2 - #>> (fn (phi1, phi2) => AConn (c, [phi1, phi2])) + #>> uncurry (mk_aconn c) and do_formula bs t = case t of - @{const Not} $ t1 => - do_formula bs t1 #>> (fn phi => AConn (ANot, [phi])) + @{const Not} $ t1 => do_formula bs t1 #>> mk_anot | Const (@{const_name All}, _) $ Abs (s, T, t') => do_quant bs AForall s T t' | Const (@{const_name Ex}, _) $ Abs (s, T, t') => @@ -414,16 +419,20 @@ (* We are crossing our fingers that it doesn't clash with anything else. *) val mangled_type_sep = "\000" -fun mangled_combtyp f (CombTFree name) = f name - | mangled_combtyp f (CombTVar name) = +fun mangled_combtyp_component f (CombTFree name) = f name + | mangled_combtyp_component f (CombTVar name) = f name (* FIXME: shouldn't happen *) (* raise Fail "impossible schematic type variable" *) - | mangled_combtyp f (CombType (name, tys)) = - "(" ^ commas (map (mangled_combtyp f) tys) ^ ")" ^ f name + | mangled_combtyp_component f (CombType (name, tys)) = + "(" ^ commas (map (mangled_combtyp_component f) tys) ^ ")" ^ f name + +fun mangled_combtyp ty = + (make_type (mangled_combtyp_component fst ty), + mangled_combtyp_component snd ty) fun mangled_type_suffix f g tys = - fold_rev (curry (op ^) o g o prefix mangled_type_sep o mangled_combtyp f) - tys "" + fold_rev (curry (op ^) o g o prefix mangled_type_sep + o mangled_combtyp_component f) tys "" val parse_mangled_ident = Scan.many1 (not o member (op =) ["(", ")", ","]) >> implode @@ -447,6 +456,11 @@ (hd ss, map unmangled_type (tl ss)) end +fun pred_combtyp ty = + case combtyp_from_typ @{typ "unit => bool"} of + CombType (name, [_, bool_ty]) => CombType (name, [ty, bool_ty]) + | _ => raise Fail "expected two-argument type constructor" + fun formula_for_combformula ctxt type_sys = let fun do_term top_level u = @@ -487,8 +501,25 @@ else I) end + val do_bound_type = + if type_sys = Many_Typed then SOME o mangled_combtyp else K NONE + val do_out_of_bound_type = + if member (op =) [Args true, Mangled true] type_sys then + (fn (s, ty) => + CombApp (CombConst ((const_prefix ^ is_base, is_base), + pred_combtyp ty, [ty]), + CombVar (s, ty)) + |> AAtom |> formula_for_combformula ctxt type_sys |> SOME) + else + K NONE fun do_formula (AQuant (q, xs, phi)) = - AQuant (q, map (apsnd (Option.map (do_term true))) xs, do_formula phi) + AQuant (q, xs |> map (apsnd (fn NONE => NONE + | SOME ty => do_bound_type ty)), + (if q = AForall then mk_ahorn else fold (mk_aconn AAnd)) + (map_filter + (fn (_, NONE) => NONE + | (s, SOME ty) => do_out_of_bound_type (s, ty)) xs) + (do_formula phi)) | do_formula (AConn (c, phis)) = AConn (c, map do_formula phis) | do_formula (AAtom tm) = AAtom (do_term true tm) in do_formula end