49 datatype 'a problem_line = |
49 datatype 'a 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 ho_type | |
52 Sym_Decl of string * 'a * 'a ho_type | |
53 Datatype_Decl of string * ('a * 'a list) list * 'a ho_type |
53 Datatype_Decl of string * ('a * 'a list) list * 'a ho_type |
54 * ('a, 'a ho_type) ho_term list | |
54 * ('a, 'a ho_type) ho_term list * bool | |
55 Class_Memb of string * ('a * 'a list) list * 'a ho_type * 'a | |
55 Class_Memb of string * ('a * 'a list) list * 'a ho_type * 'a | |
56 Formula of (string * string) * formula_role |
56 Formula of (string * string) * formula_role |
57 * ('a, 'a ho_type, ('a, 'a ho_type) ho_term, 'a) formula |
57 * ('a, 'a ho_type, ('a, 'a ho_type) ho_term, 'a) formula |
58 * (string, string ho_type) ho_term option |
58 * (string, string ho_type) ho_term option |
59 * (string, string ho_type) ho_term list |
59 * (string, string ho_type) ho_term list |
192 datatype 'a problem_line = |
192 datatype 'a problem_line = |
193 Class_Decl of string * 'a * 'a list | |
193 Class_Decl of string * 'a * 'a list | |
194 Type_Decl of string * 'a * int | |
194 Type_Decl of string * 'a * int | |
195 Sym_Decl of string * 'a * 'a ho_type | |
195 Sym_Decl of string * 'a * 'a ho_type | |
196 Datatype_Decl of string * ('a * 'a list) list * 'a ho_type |
196 Datatype_Decl of string * ('a * 'a list) list * 'a ho_type |
197 * ('a, 'a ho_type) ho_term list | |
197 * ('a, 'a ho_type) ho_term list * bool | |
198 Class_Memb of string * ('a * 'a list) list * 'a ho_type * 'a | |
198 Class_Memb of string * ('a * 'a list) list * 'a ho_type * 'a | |
199 Formula of (string * string) * formula_role |
199 Formula of (string * string) * formula_role |
200 * ('a, 'a ho_type, ('a, 'a ho_type) ho_term, 'a) formula |
200 * ('a, 'a ho_type, ('a, 'a ho_type) ho_term, 'a) formula |
201 * (string, string ho_type) ho_term option |
201 * (string, string ho_type) ho_term option |
202 * (string, string ho_type) ho_term list |
202 * (string, string ho_type) ho_term list |
599 | bound_tvar (ty, cls) = ty ^ " : " ^ dfg_class_inter cls |
599 | bound_tvar (ty, cls) = ty ^ " : " ^ dfg_class_inter cls |
600 fun binder_typ xs ty = |
600 fun binder_typ xs ty = |
601 (if null xs then "" else "[" ^ commas (map bound_tvar xs) ^ "], ") ^ |
601 (if null xs then "" else "[" ^ commas (map bound_tvar xs) ^ "], ") ^ |
602 typ ty |
602 typ ty |
603 fun sort_decl xs ty cl = "sort(" ^ binder_typ xs ty ^ ", " ^ cl ^ ")." |
603 fun sort_decl xs ty cl = "sort(" ^ binder_typ xs ty ^ ", " ^ cl ^ ")." |
604 fun datatype_decl xs ty tms = |
604 fun datatype_decl xs ty tms exhaust = |
605 "datatype(" ^ commas (binder_typ xs ty :: map term tms) ^ ")." |
605 "datatype(" ^ commas (binder_typ xs ty :: map term tms @ |
|
606 (if exhaust then [] else ["..."])) ^ ")." |
606 fun subclass_of sub super = "subclass(" ^ sub ^ ", " ^ super ^ ")." |
607 fun subclass_of sub super = "subclass(" ^ sub ^ ", " ^ super ^ ")." |
607 fun formula pred (Formula ((ident, alt), kind, phi, _, info)) = |
608 fun formula pred (Formula ((ident, alt), kind, phi, _, info)) = |
608 if pred kind then |
609 if pred kind then |
609 let val rank = extract_isabelle_rank info in |
610 let val rank = extract_isabelle_rank info in |
610 "formula(" ^ dfg_string_of_formula poly gen_simp info phi ^ |
611 "formula(" ^ dfg_string_of_formula poly gen_simp info phi ^ |
648 filt (fn Sym_Decl (_, sym, ty) => |
649 filt (fn Sym_Decl (_, sym, ty) => |
649 if is_nontrivial_predicate_atype ty then SOME (pred_typ sym ty) |
650 if is_nontrivial_predicate_atype ty then SOME (pred_typ sym ty) |
650 else NONE |
651 else NONE |
651 | _ => NONE) |> flat |
652 | _ => NONE) |> flat |
652 val datatype_decls = |
653 val datatype_decls = |
653 filt (try (fn Datatype_Decl (_, xs, ty, tms) => datatype_decl xs ty tms)) |
654 filt (try (fn Datatype_Decl (_, xs, ty, tms, exhaust) => |
654 |> flat |
655 datatype_decl xs ty tms exhaust)) |> flat |
655 val sort_decls = |
656 val sort_decls = |
656 filt (try (fn Class_Memb (_, xs, ty, cl) => sort_decl xs ty cl)) |> flat |
657 filt (try (fn Class_Memb (_, xs, ty, cl) => sort_decl xs ty cl)) |> flat |
657 val subclass_decls = |
658 val subclass_decls = |
658 filt (try (fn Class_Decl (_, sub, supers) => |
659 filt (try (fn Class_Decl (_, sub, supers) => |
659 map (subclass_of sub) supers)) |
660 map (subclass_of sub) supers)) |
927 | nice_line (Type_Decl (ident, ty, ary)) = |
928 | nice_line (Type_Decl (ident, ty, ary)) = |
928 nice_name ty #>> (fn ty => Type_Decl (ident, ty, ary)) |
929 nice_name ty #>> (fn ty => Type_Decl (ident, ty, ary)) |
929 | nice_line (Sym_Decl (ident, sym, ty)) = |
930 | nice_line (Sym_Decl (ident, sym, ty)) = |
930 nice_name sym ##>> nice_type ty |
931 nice_name sym ##>> nice_type ty |
931 #>> (fn (sym, ty) => Sym_Decl (ident, sym, ty)) |
932 #>> (fn (sym, ty) => Sym_Decl (ident, sym, ty)) |
932 | nice_line (Datatype_Decl (ident, xs, ty, tms)) = |
933 | nice_line (Datatype_Decl (ident, xs, ty, tms, exhaust)) = |
933 nice_bound_tvars xs ##>> nice_type ty ##>> fold_map nice_term tms |
934 nice_bound_tvars xs ##>> nice_type ty ##>> fold_map nice_term tms |
934 #>> (fn ((xs, ty), tms) => Datatype_Decl (ident, xs, ty, tms)) |
935 #>> (fn ((xs, ty), tms) => Datatype_Decl (ident, xs, ty, tms, exhaust)) |
935 | nice_line (Class_Memb (ident, xs, ty, cl)) = |
936 | nice_line (Class_Memb (ident, xs, ty, cl)) = |
936 nice_bound_tvars xs ##>> nice_type ty ##>> nice_name cl |
937 nice_bound_tvars xs ##>> nice_type ty ##>> nice_name cl |
937 #>> (fn ((xs, ty), cl) => Class_Memb (ident, xs, ty, cl)) |
938 #>> (fn ((xs, ty), cl) => Class_Memb (ident, xs, ty, cl)) |
938 | nice_line (Formula (ident, kind, phi, source, info)) = |
939 | nice_line (Formula (ident, kind, phi, source, info)) = |
939 nice_formula phi |
940 nice_formula phi |