# HG changeset patch # User blanchet # Date 1340702080 -7200 # Node ID cd4a4b9f1c76b44bd5bd94b336ad848f77be1a22 # Parent 6f524f2066e3003123422f4e80a152bb2715cee8 avoid detour through terms diff -r 6f524f2066e3 -r cd4a4b9f1c76 src/HOL/Tools/ATP/atp_problem_generate.ML --- a/src/HOL/Tools/ATP/atp_problem_generate.ML Tue Jun 26 11:14:40 2012 +0200 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Tue Jun 26 11:14:40 2012 +0200 @@ -878,24 +878,27 @@ val fused_infinite_type_name = "ATP.fused_inf" (* shouldn't clash *) val fused_infinite_type = Type (fused_infinite_type_name, []) -fun ho_term_from_typ type_enc = +fun raw_ho_type_from_typ type_enc = let fun term (Type (s, Ts)) = - ATerm ((case (is_type_enc_higher_order type_enc, s) of - (true, @{type_name bool}) => `I tptp_bool_type - | (true, @{type_name fun}) => `I tptp_fun_type - | _ => if s = fused_infinite_type_name andalso - is_type_enc_native type_enc then - `I tptp_individual_type - else - `make_fixed_type_const s, - []), map term Ts) - | term (TFree (s, _)) = ATerm ((`make_tfree s, []), []) - | term (TVar (x, _)) = ATerm ((tvar_name x, []), []) + AType (case (is_type_enc_higher_order type_enc, s) of + (true, @{type_name bool}) => `I tptp_bool_type + | (true, @{type_name fun}) => `I tptp_fun_type + | _ => if s = fused_infinite_type_name andalso + is_type_enc_native type_enc then + `I tptp_individual_type + else + `make_fixed_type_const s, + map term Ts) + | term (TFree (s, _)) = AType (`make_tfree s, []) + | term (TVar (x, _)) = AType (tvar_name x, []) in term end -fun ho_term_for_type_arg type_enc T = - if T = dummyT then NONE else SOME (ho_term_from_typ type_enc T) +fun ho_term_from_ho_type (AType (name, tys)) = ATerm ((name, []), map ho_term_from_ho_type tys) + | ho_term_from_ho_type _ = raise Fail "unexpected type" + +fun ho_type_for_type_arg type_enc T = + if T = dummyT then NONE else SOME (raw_ho_type_from_typ type_enc T) (* This shouldn't clash with anything else. *) val uncurried_alias_sep = "\000" @@ -903,15 +906,14 @@ val ascii_of_uncurried_alias_sep = ascii_of uncurried_alias_sep -(* ### FIXME: insane *) -fun generic_mangled_type_name f (ATerm ((name, _), [])) = f name - | generic_mangled_type_name f (ATerm ((name, _), tys)) = +fun generic_mangled_type_name f (AType (name, [])) = f name + | generic_mangled_type_name f (AType (name, tys)) = f name ^ "(" ^ space_implode "," (map (generic_mangled_type_name f) tys) ^ ")" - | generic_mangled_type_name _ _ = raise Fail "unexpected type abstraction" + | generic_mangled_type_name _ _ = raise Fail "unexpected type" fun mangled_type type_enc = - generic_mangled_type_name fst o ho_term_from_typ type_enc + generic_mangled_type_name fst o raw_ho_type_from_typ type_enc fun make_native_type s = if s = tptp_bool_type orelse s = tptp_fun_type orelse @@ -920,29 +922,29 @@ else native_type_prefix ^ ascii_of s -fun ho_type_from_ho_term type_enc pred_sym ary = +fun native_ho_type_from_raw_ho_type type_enc pred_sym ary = let fun to_mangled_atype ty = AType ((make_native_type (generic_mangled_type_name fst ty), generic_mangled_type_name snd ty), []) - fun to_poly_atype (ATerm ((name, []), tys)) = + fun to_poly_atype (AType (name, tys)) = AType (name, map to_poly_atype tys) - | to_poly_atype _ = raise Fail "unexpected type abstraction" + | to_poly_atype _ = raise Fail "unexpected type" val to_atype = if is_type_enc_polymorphic type_enc then to_poly_atype else to_mangled_atype fun to_afun f1 f2 tys = AFun (f1 (hd tys), f2 (nth tys 1)) fun to_fo 0 ty = if pred_sym then bool_atype else to_atype ty - | to_fo ary (ATerm (_, tys)) = to_afun to_atype (to_fo (ary - 1)) tys - | to_fo _ _ = raise Fail "unexpected type abstraction" - fun to_ho (ty as ATerm (((s, _), []), tys)) = + | to_fo ary (AType (_, tys)) = to_afun to_atype (to_fo (ary - 1)) tys + | to_fo _ _ = raise Fail "unexpected type" + fun to_ho (ty as AType ((s, _), tys)) = if s = tptp_fun_type then to_afun to_ho to_ho tys else to_atype ty - | to_ho _ = raise Fail "unexpected type abstraction" + | to_ho _ = raise Fail "unexpected type" in if is_type_enc_higher_order type_enc then to_ho else to_fo ary end -fun ho_type_from_typ type_enc pred_sym ary = - ho_type_from_ho_term type_enc pred_sym ary - o ho_term_from_typ type_enc +fun native_ho_type_from_typ type_enc pred_sym ary = + native_ho_type_from_raw_ho_type type_enc pred_sym ary + o raw_ho_type_from_typ type_enc (* Make atoms for sorted type variables. *) fun generic_add_sorts_on_type _ [] = I @@ -956,9 +958,10 @@ fun process_type_args type_enc T_args = if is_type_enc_native type_enc then - (map (ho_type_from_typ type_enc false 0) T_args, []) + (map (native_ho_type_from_typ type_enc false 0) T_args, []) else - ([], map_filter (ho_term_for_type_arg type_enc) T_args) + ([], map_filter (Option.map ho_term_from_ho_type + o ho_type_for_type_arg type_enc) T_args) fun type_class_atom type_enc (class, T) = let @@ -1040,7 +1043,7 @@ ty_args "" in (s ^ type_suffix fst ascii_of, s' ^ type_suffix snd I) end fun mangled_const_name type_enc = - map_filter (ho_term_for_type_arg type_enc) + map_filter (ho_type_for_type_arg type_enc) #> raw_mangled_const_name generic_mangled_type_name val parse_mangled_ident = @@ -2014,7 +2017,8 @@ fun do_bound_type ctxt mono type_enc = case type_enc of Native (_, _, level) => - fused_type ctxt mono level 0 #> ho_type_from_typ type_enc false 0 #> SOME + fused_type ctxt mono level 0 #> native_ho_type_from_typ type_enc false 0 + #> SOME | _ => K NONE fun tag_with_type ctxt mono type_enc pos T tm = @@ -2043,7 +2047,7 @@ map (term Elsewhere) args |> mk_aterm type_enc name [] | IAbs ((name, T), tm) => if is_type_enc_higher_order type_enc then - AAbs (((name, ho_type_from_typ type_enc true (* FIXME? why "true"? *) 0 T), + AAbs (((name, native_ho_type_from_typ type_enc true 0 T), (* FIXME? why "true"? *) term Elsewhere tm), map (term Elsewhere) args) else raise Fail "unexpected lambda-abstraction" @@ -2075,7 +2079,7 @@ else NONE fun do_formula pos (ATyQuant (q, xs, phi)) = - ATyQuant (q, map (apfst (ho_type_from_typ type_enc false 0)) xs, + ATyQuant (q, map (apfst (native_ho_type_from_typ type_enc false 0)) xs, do_formula pos phi) | do_formula pos (AQuant (q, xs, phi)) = let @@ -2358,7 +2362,7 @@ in Sym_Decl (sym_decl_prefix ^ s, (s, s'), T |> fused_type ctxt mono (level_of_type_enc type_enc) ary - |> ho_type_from_typ type_enc pred_sym ary + |> native_ho_type_from_typ type_enc pred_sym ary |> not (null T_args) ? curry APi (map (tvar_name o fst o dest_TVar) T_args)) end