48 |
48 |
49 datatype 'a atp_problem_line = |
49 datatype 'a atp_problem_line = |
50 Class_Decl of string * 'a * 'a list | |
50 Class_Decl of string * 'a * 'a list | |
51 Type_Decl of string * 'a * int | |
51 Type_Decl of string * 'a * int | |
52 Sym_Decl of string * 'a * 'a atp_type | |
52 Sym_Decl of string * 'a * 'a atp_type | |
53 Datatype_Decl of string * ('a * 'a list) list * 'a atp_type |
53 Datatype_Decl of string * ('a * 'a list) list * 'a atp_type * ('a, 'a atp_type) atp_term list | |
54 * ('a, 'a atp_type) atp_term list * bool | |
|
55 Class_Memb of string * ('a * 'a list) list * 'a atp_type * 'a | |
54 Class_Memb of string * ('a * 'a list) list * 'a atp_type * 'a | |
56 Formula of (string * string) * atp_formula_role |
55 Formula of (string * string) * atp_formula_role |
57 * ('a, 'a atp_type, ('a, 'a atp_type) atp_term, 'a) atp_formula |
56 * ('a, 'a atp_type, ('a, 'a atp_type) atp_term, 'a) atp_formula |
58 * (string, string atp_type) atp_term option |
57 * (string, string atp_type) atp_term option |
59 * (string, string atp_type) atp_term list |
58 * (string, string atp_type) atp_term list |
193 |
192 |
194 datatype 'a atp_problem_line = |
193 datatype 'a atp_problem_line = |
195 Class_Decl of string * 'a * 'a list | |
194 Class_Decl of string * 'a * 'a list | |
196 Type_Decl of string * 'a * int | |
195 Type_Decl of string * 'a * int | |
197 Sym_Decl of string * 'a * 'a atp_type | |
196 Sym_Decl of string * 'a * 'a atp_type | |
198 Datatype_Decl of string * ('a * 'a list) list * 'a atp_type |
197 Datatype_Decl of string * ('a * 'a list) list * 'a atp_type * ('a, 'a atp_type) atp_term list | |
199 * ('a, 'a atp_type) atp_term list * bool | |
|
200 Class_Memb of string * ('a * 'a list) list * 'a atp_type * 'a | |
198 Class_Memb of string * ('a * 'a list) list * 'a atp_type * 'a | |
201 Formula of (string * string) * atp_formula_role |
199 Formula of (string * string) * atp_formula_role |
202 * ('a, 'a atp_type, ('a, 'a atp_type) atp_term, 'a) atp_formula |
200 * ('a, 'a atp_type, ('a, 'a atp_type) atp_term, 'a) atp_formula |
203 * (string, string atp_type) atp_term option |
201 * (string, string atp_type) atp_term option |
204 * (string, string atp_type) atp_term list |
202 * (string, string atp_type) atp_term list |
622 | bound_tvar (ty, cls) = ty ^ " : " ^ dfg_class_inter cls |
620 | bound_tvar (ty, cls) = ty ^ " : " ^ dfg_class_inter cls |
623 fun binder_typ xs ty = |
621 fun binder_typ xs ty = |
624 (if null xs then "" else "[" ^ commas (map bound_tvar xs) ^ "], ") ^ |
622 (if null xs then "" else "[" ^ commas (map bound_tvar xs) ^ "], ") ^ |
625 typ ty |
623 typ ty |
626 fun sort_decl xs ty cl = "sort(" ^ binder_typ xs ty ^ ", " ^ cl ^ ")." |
624 fun sort_decl xs ty cl = "sort(" ^ binder_typ xs ty ^ ", " ^ cl ^ ")." |
627 fun datatype_decl xs ty tms exhaust = |
625 fun datatype_decl xs ty tms = "datatype(" ^ commas (binder_typ xs ty :: map term tms) ^ ")." |
628 "datatype(" ^ commas (binder_typ xs ty :: map term tms @ |
|
629 (if exhaust then [] else ["..."])) ^ ")." |
|
630 fun subclass_of sub super = "subclass(" ^ sub ^ ", " ^ super ^ ")." |
626 fun subclass_of sub super = "subclass(" ^ sub ^ ", " ^ super ^ ")." |
631 fun formula pred (Formula ((ident, alt), kind, phi, _, info)) = |
627 fun formula pred (Formula ((ident, alt), kind, phi, _, info)) = |
632 if pred kind then |
628 if pred kind then |
633 let val rank = extract_isabelle_rank info in |
629 let val rank = extract_isabelle_rank info in |
634 "formula(" ^ dfg_string_of_formula poly gen_simp info phi ^ |
630 "formula(" ^ dfg_string_of_formula poly gen_simp info phi ^ |
672 filt (fn Sym_Decl (_, sym, ty) => |
668 filt (fn Sym_Decl (_, sym, ty) => |
673 if is_nontrivial_predicate_atype ty then SOME (pred_typ sym ty) |
669 if is_nontrivial_predicate_atype ty then SOME (pred_typ sym ty) |
674 else NONE |
670 else NONE |
675 | _ => NONE) |> flat |
671 | _ => NONE) |> flat |
676 val datatype_decls = |
672 val datatype_decls = |
677 filt (try (fn Datatype_Decl (_, xs, ty, tms, exhaust) => |
673 filt (try (fn Datatype_Decl (_, xs, ty, tms) => datatype_decl xs ty tms)) |> flat |
678 datatype_decl xs ty tms exhaust)) |> flat |
|
679 val sort_decls = |
674 val sort_decls = |
680 filt (try (fn Class_Memb (_, xs, ty, cl) => sort_decl xs ty cl)) |> flat |
675 filt (try (fn Class_Memb (_, xs, ty, cl) => sort_decl xs ty cl)) |> flat |
681 val subclass_decls = |
676 val subclass_decls = |
682 filt (try (fn Class_Decl (_, sub, supers) => |
677 filt (try (fn Class_Decl (_, sub, supers) => |
683 map (subclass_of sub) supers)) |
678 map (subclass_of sub) supers)) |
950 | nice_line (Type_Decl (ident, ty, ary)) = |
945 | nice_line (Type_Decl (ident, ty, ary)) = |
951 nice_name ty #>> (fn ty => Type_Decl (ident, ty, ary)) |
946 nice_name ty #>> (fn ty => Type_Decl (ident, ty, ary)) |
952 | nice_line (Sym_Decl (ident, sym, ty)) = |
947 | nice_line (Sym_Decl (ident, sym, ty)) = |
953 nice_name sym ##>> nice_type ty |
948 nice_name sym ##>> nice_type ty |
954 #>> (fn (sym, ty) => Sym_Decl (ident, sym, ty)) |
949 #>> (fn (sym, ty) => Sym_Decl (ident, sym, ty)) |
955 | nice_line (Datatype_Decl (ident, xs, ty, tms, exhaust)) = |
950 | nice_line (Datatype_Decl (ident, xs, ty, tms)) = |
956 nice_bound_tvars xs ##>> nice_type ty ##>> fold_map nice_term tms |
951 nice_bound_tvars xs ##>> nice_type ty ##>> fold_map nice_term tms |
957 #>> (fn ((xs, ty), tms) => Datatype_Decl (ident, xs, ty, tms, exhaust)) |
952 #>> (fn ((xs, ty), tms) => Datatype_Decl (ident, xs, ty, tms)) |
958 | nice_line (Class_Memb (ident, xs, ty, cl)) = |
953 | nice_line (Class_Memb (ident, xs, ty, cl)) = |
959 nice_bound_tvars xs ##>> nice_type ty ##>> nice_name cl |
954 nice_bound_tvars xs ##>> nice_type ty ##>> nice_name cl |
960 #>> (fn ((xs, ty), cl) => Class_Memb (ident, xs, ty, cl)) |
955 #>> (fn ((xs, ty), cl) => Class_Memb (ident, xs, ty, cl)) |
961 | nice_line (Formula (ident, kind, phi, source, info)) = |
956 | nice_line (Formula (ident, kind, phi, source, info)) = |
962 nice_formula phi |
957 nice_formula phi |