# HG changeset patch # User wenzelm # Date 1085835839 -7200 # Node ID 15d12761ba54653bac81c90b6306e338224ee879 # Parent d973e7f820cb4271802d133c7f7cf57a9599c3b8 improved output; refer to Pretty.pp; diff -r d973e7f820cb -r 15d12761ba54 src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Sat May 29 15:02:35 2004 +0200 +++ b/src/Pure/Isar/proof_context.ML Sat May 29 15:03:59 2004 +0200 @@ -15,13 +15,20 @@ exception CONTEXT of string * context val theory_of: context -> theory val sign_of: context -> Sign.sg - val syntax_of: context -> Syntax.syntax * string list * string list + val is_fixed: context -> string -> bool val fixed_names_of: context -> string list val assumptions_of: context -> (cterm list * exporter) list val prems_of: context -> thm list val print_proof_data: theory -> unit val init: theory -> context - val is_fixed: context -> string -> bool + val pretty_term: context -> term -> Pretty.T + val pretty_typ: context -> typ -> Pretty.T + val pretty_sort: context -> sort -> Pretty.T + val pp: context -> Pretty.pp + val pretty_thm: context -> thm -> Pretty.T + val pretty_thms: context -> thm list -> Pretty.T + val pretty_fact: context -> string * thm list -> Pretty.T + val string_of_term: context -> term -> string val default_type: context -> string -> typ option val used_types: context -> string list val read_typ: context -> string -> typ @@ -123,13 +130,6 @@ val add_cases: (string * RuleCases.T) list -> context -> context val apply_case: RuleCases.T -> context -> context * ((indexname * term option) list * (string * term list) list) - val pretty_term: context -> term -> Pretty.T - val pretty_typ: context -> typ -> Pretty.T - val pretty_sort: context -> sort -> Pretty.T - val pretty_thm: context -> thm -> Pretty.T - val pretty_thms: context -> thm list -> Pretty.T - val pretty_fact: context -> string * thm list -> Pretty.T - val string_of_term: context -> term -> string val verbose: bool ref val setmp_verbose: ('a -> 'b) -> 'a -> 'b val print_syntax: context -> unit @@ -379,6 +379,33 @@ +(** pretty printing **) + +fun pretty_term ctxt = Sign.pretty_term' (syn_of ctxt) (sign_of ctxt) o context_tr' ctxt; +val pretty_typ = Sign.pretty_typ o sign_of; +val pretty_sort = Sign.pretty_sort o sign_of; + +fun pp ctxt = Pretty.pp (pretty_term ctxt) (pretty_typ ctxt) (pretty_sort ctxt) + (Sign.pretty_classrel (sign_of ctxt)) (Sign.pretty_arity (sign_of ctxt)); + +val string_of_term = Pretty.string_of oo pretty_term; + +fun pretty_thm ctxt thm = + if ! Display.show_hyps then + Display.pretty_thm_aux (pretty_sort ctxt, pretty_term ctxt) false thm + else pretty_term ctxt (Thm.prop_of thm); + +fun pretty_thms ctxt [th] = pretty_thm ctxt th + | pretty_thms ctxt ths = Pretty.blk (0, Pretty.fbreaks (map (pretty_thm ctxt) ths)); + +fun pretty_fact ctxt ("", ths) = pretty_thms ctxt ths + | pretty_fact ctxt (a, [th]) = + Pretty.block [Pretty.str (a ^ ":"), Pretty.brk 1, pretty_thm ctxt th] + | pretty_fact ctxt (a, ths) = + Pretty.block (Pretty.fbreaks (Pretty.str (a ^ ":") :: map (pretty_thm ctxt) ths)); + + + (** default sorts and types **) fun def_sort (Context {defs = (_, sorts, _, _), ...}) xi = Vartab.lookup (sorts, xi); @@ -474,28 +501,29 @@ (* read / certify wrt. signature *) (*exception ERROR*) (*exception TERM*) -fun read_def_termTs freeze syn sg (types, sorts, used) sTs = - Sign.read_def_terms' syn (sg, types, sorts) used freeze sTs; +fun read_def_termTs freeze pp syn sg (types, sorts, used) sTs = + Sign.read_def_terms' pp syn (sg, types, sorts) used freeze sTs; -fun read_def_termT freeze syn sg defs sT = apfst hd (read_def_termTs freeze syn sg defs [sT]); +fun read_def_termT freeze pp syn sg defs sT = + apfst hd (read_def_termTs freeze pp syn sg defs [sT]); + +fun read_term_sg freeze pp syn sg defs s = + #1 (read_def_termT freeze pp syn sg defs (s, TypeInfer.logicT)); -fun read_term_sg freeze syn sg defs s = - #1 (read_def_termT freeze syn sg defs (s, TypeInfer.logicT)); - -fun read_prop_sg freeze syn sg defs s = #1 (read_def_termT freeze syn sg defs (s, propT)); +fun read_prop_sg freeze pp syn sg defs s = + #1 (read_def_termT freeze pp syn sg defs (s, propT)); -fun read_terms_sg freeze syn sg defs = - #1 o read_def_termTs freeze syn sg defs o map (rpair TypeInfer.logicT); +fun read_terms_sg freeze pp syn sg defs = + #1 o read_def_termTs freeze pp syn sg defs o map (rpair TypeInfer.logicT); -fun read_props_sg freeze syn sg defs = #1 o read_def_termTs freeze syn sg defs o map (rpair propT); +fun read_props_sg freeze pp syn sg defs = + #1 o read_def_termTs freeze pp syn sg defs o map (rpair propT); -fun cert_term_sg sg t = Thm.term_of (Thm.cterm_of sg t); +fun cert_term_sg pp sg t = #1 (Sign.certify_term pp sg t); -fun cert_prop_sg sg tm = - let - val ctm = Thm.cterm_of sg tm; - val {t, T, ...} = Thm.rep_cterm ctm; +fun cert_prop_sg pp sg tm = + let val (t, T, _) = Sign.certify_term pp sg tm in if T = propT then t else raise TERM ("Term not of type prop", [t]) end; @@ -556,7 +584,7 @@ val sorts = append_env (def_sort ctxt) more_sorts; val used = used_types ctxt @ more_used; in - (transform_error (read (syn_of ctxt) (sign_of ctxt) (types, sorts, used)) s + (transform_error (read (pp ctxt) (syn_of ctxt) (sign_of ctxt) (types, sorts, used)) s handle TERM (msg, _) => raise CONTEXT (msg, ctxt) | ERROR_MESSAGE msg => raise CONTEXT (msg, ctxt)) |> app (intern_skolem ctxt internal) @@ -595,7 +623,8 @@ fun gen_cert cert pattern schematic ctxt t = t |> (if pattern then I else norm_term ctxt schematic) - |> (fn t' => cert (sign_of ctxt) t' handle TERM (msg, _) => raise CONTEXT (msg, ctxt)); + |> (fn t' => cert (pp ctxt) (sign_of ctxt) t' + handle TERM (msg, _) => raise CONTEXT (msg, ctxt)); in @@ -661,30 +690,6 @@ -(** pretty printing **) - -fun pretty_term ctxt = Sign.pretty_term' (syn_of ctxt) (sign_of ctxt) o context_tr' ctxt; -val pretty_typ = Sign.pretty_typ o sign_of; -val pretty_sort = Sign.pretty_sort o sign_of; - -val string_of_term = Pretty.string_of oo pretty_term; - -fun pretty_thm ctxt thm = - if ! Display.show_hyps then - Display.pretty_thm_aux (pretty_sort ctxt, pretty_term ctxt) false thm - else pretty_term ctxt (Thm.prop_of thm); - -fun pretty_thms ctxt [th] = pretty_thm ctxt th - | pretty_thms ctxt ths = Pretty.blk (0, Pretty.fbreaks (map (pretty_thm ctxt) ths)); - -fun pretty_fact ctxt ("", ths) = pretty_thms ctxt ths - | pretty_fact ctxt (a, [th]) = - Pretty.block [Pretty.str (a ^ ":"), Pretty.brk 1, pretty_thm ctxt th] - | pretty_fact ctxt (a, ths) = - Pretty.block (Pretty.fbreaks (Pretty.str (a ^ ":") :: map (pretty_thm ctxt) ths)); - - - (** Hindley-Milner polymorphism **) (* warn_extra_tfrees *) diff -r d973e7f820cb -r 15d12761ba54 src/Pure/sign.ML --- a/src/Pure/sign.ML Sat May 29 15:02:35 2004 +0200 +++ b/src/Pure/sign.ML Sat May 29 15:03:59 2004 +0200 @@ -78,36 +78,38 @@ val pretty_term': Syntax.syntax -> sg -> term -> Pretty.T val pretty_typ: sg -> typ -> Pretty.T val pretty_sort: sg -> sort -> Pretty.T - val pretty_classrel: sg -> class * class -> Pretty.T - val pretty_arity: sg -> string * sort list * sort -> Pretty.T + val pretty_classrel: sg -> class list -> Pretty.T + val pretty_arity: sg -> arity -> Pretty.T val string_of_term: sg -> term -> string val string_of_typ: sg -> typ -> string val string_of_sort: sg -> sort -> string - val str_of_sort: sg -> sort -> string - val str_of_classrel: sg -> class * class -> string - val str_of_arity: sg -> string * sort list * sort -> string + val string_of_classrel: sg -> class list -> string + val string_of_arity: sg -> arity -> string val pprint_term: sg -> term -> pprint_args -> unit val pprint_typ: sg -> typ -> pprint_args -> unit + val pp: sg -> Pretty.pp val certify_class: sg -> class -> class val certify_sort: sg -> sort -> sort val certify_typ: sg -> typ -> typ val certify_typ_raw: sg -> typ -> typ val certify_tyname: sg -> string -> string val certify_const: sg -> string -> string - val certify_term: sg -> term -> term * typ * int + val certify_term: Pretty.pp -> sg -> term -> term * typ * int val read_sort: sg -> string -> sort val read_raw_typ: sg * (indexname -> sort option) -> string -> typ val read_typ: sg * (indexname -> sort option) -> string -> typ val read_typ': Syntax.syntax -> sg * (indexname -> sort option) -> string -> typ val read_typ_raw': Syntax.syntax -> sg * (indexname -> sort option) -> string -> typ - val infer_types: sg -> (indexname -> typ option) -> + val inst_typ_tvars: sg -> (indexname * typ) list -> typ -> typ + val inst_term_tvars: sg -> (indexname * typ) list -> term -> term + val infer_types: Pretty.pp -> sg -> (indexname -> typ option) -> (indexname -> sort option) -> string list -> bool -> xterm list * typ -> term * (indexname * typ) list - val infer_types_simult: sg -> (indexname -> typ option) -> + val infer_types_simult: Pretty.pp -> sg -> (indexname -> typ option) -> (indexname -> sort option) -> string list -> bool -> (xterm list * typ) list -> term list * (indexname * typ) list - val read_def_terms': - Syntax.syntax -> sg * (indexname -> typ option) * (indexname -> sort option) -> + val read_def_terms': Pretty.pp -> Syntax.syntax -> + sg * (indexname -> typ option) * (indexname -> sort option) -> string list -> bool -> (string * typ) list -> term list * (indexname * typ) list val read_def_terms: sg * (indexname -> typ option) * (indexname -> sort option) -> @@ -337,6 +339,7 @@ val typ_instance = Type.typ_instance o tsig_of; + (** signature data **) (* errors *) @@ -603,8 +606,8 @@ Syntax.pretty_sort (syn_of sg) (if ! NameSpace.long_names then S else extrn_sort spaces S); -fun pretty_classrel sg (c1, c2) = Pretty.block - [pretty_sort sg [c1], Pretty.str " <", Pretty.brk 1, pretty_sort sg [c2]]; +fun pretty_classrel sg cs = Pretty.block (flat + (separate [Pretty.str " <", Pretty.brk 1] (map (single o pretty_sort sg o single) cs))); fun pretty_arity sg (t, Ss, S) = let @@ -617,17 +620,18 @@ ([Pretty.str (t' ^ " ::"), Pretty.brk 1] @ dom @ [pretty_sort sg S]) end; -fun string_of_term sg t = Pretty.string_of (pretty_term sg t); -fun string_of_typ sg T = Pretty.string_of (pretty_typ sg T); -fun string_of_sort sg S = Pretty.string_of (pretty_sort sg S); - -fun str_of_sort sg S = Pretty.str_of (pretty_sort sg S); -fun str_of_classrel sg c1_c2 = Pretty.str_of (pretty_classrel sg c1_c2); -fun str_of_arity sg ar = Pretty.str_of (pretty_arity sg ar); +val string_of_term = Pretty.string_of oo pretty_term; +val string_of_typ = Pretty.string_of oo pretty_typ; +val string_of_sort = Pretty.string_of oo pretty_sort; +val string_of_classrel = Pretty.string_of oo pretty_classrel; +val string_of_arity = Pretty.string_of oo pretty_arity; fun pprint_term sg = Pretty.pprint o Pretty.quote o (pretty_term sg); fun pprint_typ sg = Pretty.pprint o Pretty.quote o (pretty_typ sg); +fun pp sg = Pretty.pp (pretty_term sg) (pretty_typ sg) (pretty_sort sg) + (pretty_classrel sg) (pretty_arity sg); + (** read sorts **) (*exception ERROR*) @@ -741,17 +745,15 @@ in nodups (([], []), ([], [])) tm; tm end; (*compute and check type of the term*) -fun type_check sg tm = +fun type_check pp sg tm = let - val prt = setmp Syntax.show_brackets true (pretty_term sg); - val prT = pretty_typ sg; - fun err_appl why bs t T u U = let val xs = map Free bs; (*we do not rename here*) val t' = subst_bounds (xs, t); val u' = subst_bounds (xs, u); - val text = cat_lines (TypeInfer.appl_error prt prT why t' T u' U); + val text = cat_lines + (TypeInfer.appl_error (Syntax.pp_show_brackets pp) why t' T u' U); in raise TYPE (text, [T, U], [t', u']) end; fun typ_of (_, Const (_, T)) = T @@ -764,13 +766,13 @@ let val T = typ_of (bs, t) and U = typ_of (bs, u) in (case T of Type ("fun", [T1, T2]) => - if T1 = U then T2 else err_appl "Incompatible operand type." bs t T u U - | _ => err_appl "Operator not of function type." bs t T u U) + if T1 = U then T2 else err_appl "Incompatible operand type" bs t T u U + | _ => err_appl "Operator not of function type" bs t T u U) end; in typ_of ([], tm) end; -fun certify_term sg tm = +fun certify_term pp sg tm = let val _ = check_stale sg; @@ -779,7 +781,7 @@ fun err msg = raise TYPE (msg, [], [tm']); - fun show_const a T = quote a ^ " :: " ^ quote (string_of_typ sg T); + fun show_const a T = quote a ^ " :: " ^ Pretty.string_of_typ pp T; fun check_atoms (t $ u) = (check_atoms t; check_atoms u) | check_atoms (Abs (_, _, t)) = check_atoms t @@ -795,11 +797,18 @@ in check_atoms tm'; nodup_vars tm'; - (tm', type_check sg tm', maxidx_of_term tm') + (tm', type_check pp sg tm', maxidx_of_term tm') end; +(** instantiation **) + +fun inst_typ_tvars sg = Type.inst_typ_tvars (pp sg) (tsig_of sg); +fun inst_term_tvars sg = Type.inst_term_tvars (pp sg) (tsig_of sg); + + + (** infer_types **) (*exception ERROR*) (* @@ -812,19 +821,17 @@ typs: expected types *) -fun infer_types_simult sg def_type def_sort used freeze args = +fun infer_types_simult pp sg def_type def_sort used freeze args = let val tsig = tsig_of sg; - val prt = setmp Syntax.show_brackets true (pretty_term sg); - val prT = pretty_typ sg; val termss = foldr multiply (map fst args, [[]]); val typs = map (fn (_, T) => certify_typ sg T handle TYPE (msg, _, _) => error msg) args; - fun infer ts = OK - (TypeInfer.infer_types prt prT tsig (const_type sg) def_type def_sort - (intern_const sg) (intern_tycons sg) (intern_sort sg) used freeze typs ts) + fun infer ts = OK (TypeInfer.infer_types (Syntax.pp_show_brackets pp) tsig + (const_type sg) def_type def_sort (intern_const sg) (intern_tycons sg) + (intern_sort sg) used freeze typs ts) handle TYPE (msg, _, _) => Error msg; val err_results = map infer termss; @@ -847,27 +854,27 @@ \You may still want to disambiguate your grammar or your input." else (); hd results) else (ambig_msg (); error ("More than one term is type correct:\n" ^ - (cat_lines (map (Pretty.string_of o prt) (flat (map fst results)))))) + cat_lines (map (Pretty.string_of_term pp) (flat (map fst results))))) end; -fun infer_types sg def_type def_sort used freeze tsT = - apfst hd (infer_types_simult sg def_type def_sort used freeze [tsT]); +fun infer_types pp sg def_type def_sort used freeze tsT = + apfst hd (infer_types_simult pp sg def_type def_sort used freeze [tsT]); (** read_def_terms **) (*read terms, infer types*) -fun read_def_terms' syn (sign, types, sorts) used freeze sTs = +fun read_def_terms' pp syn (sign, types, sorts) used freeze sTs = let fun read (s, T) = let val T' = certify_typ sign T handle TYPE (msg, _, _) => error msg in (Syntax.read syn T' s, T') end; val tsTs = map read sTs; - in infer_types_simult sign types sorts used freeze tsTs end; + in infer_types_simult pp sign types sorts used freeze tsTs end; fun read_def_terms (sign, types, sorts) = - read_def_terms' (syn_of sign) (sign, types, sorts); + read_def_terms' (pp sign) (syn_of sign) (sign, types, sorts); fun simple_read_term sign T s = (read_def_terms (sign, K None, K None) [] true [(s, T)] @@ -946,7 +953,7 @@ val prepS = prep_sort sg syn tsig spaces; fun prep_arity (c, Ss, S) = (if int then intrn spaces typeK c else c, map prepS Ss, prepS S); - val tsig' = Type.add_arities (map prep_arity arities) tsig; + val tsig' = Type.add_arities (pp sg) (map prep_arity arities) tsig; val log_types = Type.logical_types tsig'; in (map_syntax (Syntax.extend_log_types log_types) syn, @@ -1027,16 +1034,16 @@ in ext_consts_i sg (map_syntax (Syntax.extend_consts names) syn, - Type.add_classes classes' tsig, ctab, (path, spaces'), data) + Type.add_classes (pp sg) classes' tsig, ctab, (path, spaces'), data) consts end; (* add to classrel *) -fun ext_classrel int _ (syn, tsig, ctab, (path, spaces), data) pairs = +fun ext_classrel int sg (syn, tsig, ctab, (path, spaces), data) pairs = let val intrn = if int then map (pairself (intrn_class spaces)) else I in - (syn, Type.add_classrel (intrn pairs) tsig, ctab, (path, spaces), data) + (syn, Type.add_classrel (pp sg) (intrn pairs) tsig, ctab, (path, spaces), data) end; @@ -1213,7 +1220,7 @@ val stamps = merge_stamps stamps1 stamps2; val syntax = Syntax.merge_syntaxes syntax1 syntax2; val trfuns = merge_trfuns trfuns1 trfuns2; - val tsig = Type.merge_tsigs (tsig1, tsig2); + val tsig = Type.merge_tsigs (pp sg1) (tsig1, tsig2); (* FIXME improve pp *) val consts = Symtab.merge eq_snd (consts1, consts2) handle Symtab.DUPS cs => err_dup_consts cs; diff -r d973e7f820cb -r 15d12761ba54 src/Pure/sorts.ML --- a/src/Pure/sorts.ML Sat May 29 15:02:35 2004 +0200 +++ b/src/Pure/sorts.ML Sat May 29 15:03:59 2004 +0200 @@ -7,8 +7,6 @@ signature SORTS = sig - val str_of_sort: sort -> string - val str_of_arity: string * sort list * sort -> string val eq_sort: sort * sort -> bool val mem_sort: sort * sort list -> bool val subset_sort: sort list * sort list -> bool @@ -31,8 +29,8 @@ val of_sort: classes * arities -> typ * sort -> bool exception DOMAIN of string * class val mg_domain: classes * arities -> string -> sort -> sort list (*exception DOMAIN*) - val witness_sorts: classes * arities -> string list - -> sort list -> sort list -> (typ * sort) list + val witness_sorts: classes * arities -> string list -> + sort list -> sort list -> (typ * sort) list end; structure Sorts: SORTS = @@ -53,16 +51,6 @@ *) -(* simple printing -- lacks pretty printing, translations etc. *) - -fun str_of_sort [c] = c - | str_of_sort cs = Library.enclose "{" "}" (Library.commas cs); - -fun str_of_arity (t, [], S) = t ^ " :: " ^ str_of_sort S - | str_of_arity (t, Ss, S) = t ^ " :: " ^ - Library.enclose "(" ")" (Library.commas (map str_of_sort Ss)) ^ " " ^ str_of_sort S; - - (* equality, membership and insertion of sorts *) fun eq_sort ([]: sort, []) = true @@ -190,7 +178,9 @@ (** witness_sorts **) -fun witness_sorts_aux (classes, arities) log_types hyps sorts = +local + +fun witness_aux (classes, arities) log_types hyps sorts = let val top_witn = (propT, []); fun le S1 S2 = sort_le classes (S1, S2); @@ -229,6 +219,10 @@ in witn_sorts [] (([], []), sorts) end; +fun str_of_sort [c] = c + | str_of_sort cs = enclose "{" "}" (commas cs); + +in fun witness_sorts (classes, arities) log_types hyps sorts = let @@ -237,7 +231,8 @@ | check_result (Some (T, S)) = if of_sort (classes, arities) (T, S) then Some (T, S) else sys_error ("Sorts.witness_sorts: bad witness for sort " ^ str_of_sort S); - in mapfilter check_result (#2 (witness_sorts_aux (classes, arities) log_types hyps sorts)) end; - + in mapfilter check_result (#2 (witness_aux (classes, arities) log_types hyps sorts)) end; end; + +end; diff -r d973e7f820cb -r 15d12761ba54 src/Pure/theory.ML --- a/src/Pure/theory.ML Sat May 29 15:02:35 2004 +0200 +++ b/src/Pure/theory.ML Sat May 29 15:03:59 2004 +0200 @@ -260,7 +260,7 @@ fun cert_axm sg (name, raw_tm) = let - val (t, T, _) = Sign.certify_term sg raw_tm + val (t, T, _) = Sign.certify_term (Sign.pp sg) sg raw_tm handle TYPE (msg, _, _) => error msg | TERM (msg, _) => error msg; in @@ -273,15 +273,15 @@ fun read_def_axm (sg, types, sorts) used (name, str) = let val ts = Syntax.read (Sign.syn_of sg) propT str; - val (t, _) = Sign.infer_types sg types sorts used true (ts, propT); + val (t, _) = Sign.infer_types (Sign.pp sg) sg types sorts used true (ts, propT); in cert_axm sg (name, t) end handle ERROR => err_in_axm name; fun read_axm sg name_str = read_def_axm (sg, K None, K None) [] name_str; fun inferT_axm sg (name, pre_tm) = - let - val (t, _) = Sign.infer_types sg (K None) (K None) [] true ([pre_tm], propT); + let val (t, _) = Sign.infer_types (Sign.pp sg) sg + (K None) (K None) [] true ([pre_tm], propT); in (name, no_vars sg t) end handle ERROR => err_in_axm name; @@ -510,7 +510,7 @@ local fun read_term sg = Sign.simple_read_term sg TypeInfer.logicT; - val cert_term = #1 oo Sign.certify_term; + fun cert_term sg = #1 o Sign.certify_term (Sign.pp sg) sg; in val add_finals = ext_finals read_term; val add_finals_i = ext_finals cert_term; diff -r d973e7f820cb -r 15d12761ba54 src/Pure/thm.ML --- a/src/Pure/thm.ML Sat May 29 15:02:35 2004 +0200 +++ b/src/Pure/thm.ML Sat May 29 15:03:59 2004 +0200 @@ -176,7 +176,7 @@ (*create a cterm by checking a "raw" term with respect to a signature*) fun cterm_of sign tm = - let val (t, T, maxidx) = Sign.certify_term sign tm + let val (t, T, maxidx) = Sign.certify_term (Sign.pp sign) sign tm in Cterm {sign_ref = Sign.self_ref sign, t = t, T = T, maxidx = maxidx} end; @@ -972,8 +972,8 @@ | instantiate (vcTs,ctpairs) (th as Thm{sign_ref,der,maxidx,hyps,shyps,tpairs=dpairs,prop}) = let val (newsign_ref,tpairs) = foldr add_ctpair (ctpairs, (sign_ref,[])); val (newsign_ref,vTs) = foldr add_ctyp (vcTs, (newsign_ref,[])); - val tsig = Sign.tsig_of (Sign.deref newsign_ref); - fun subst t = subst_atomic tpairs (Type.inst_term_tvars tsig vTs t); + fun subst t = + subst_atomic tpairs (Sign.inst_term_tvars (Sign.deref newsign_ref) vTs t); val newprop = subst prop; val newdpairs = map (pairself subst) dpairs; val newth = @@ -1460,7 +1460,8 @@ let val sign_ref' = Sign.merge_refs (Sign.self_ref sg, Sign.self_ref sign); val sign' = Sign.deref sign_ref'; - val (prop, T, maxidx) = Sign.certify_term sign' (oracle (sign', exn)); + val (prop, T, maxidx) = + Sign.certify_term (Sign.pp sign') sign' (oracle (sign', exn)); in if T <> propT then raise THM ("Oracle's result must have type prop: " ^ name, 0, []) diff -r d973e7f820cb -r 15d12761ba54 src/Pure/type_infer.ML --- a/src/Pure/type_infer.ML Sat May 29 15:02:35 2004 +0200 +++ b/src/Pure/type_infer.ML Sat May 29 15:03:59 2004 +0200 @@ -10,14 +10,13 @@ val anyT: sort -> typ val logicT: typ val polymorphicT: typ -> typ - val appl_error: (term -> Pretty.T) -> (typ -> Pretty.T) - -> string -> term -> typ -> term -> typ -> string list + val appl_error: Pretty.pp -> string -> term -> typ -> term -> typ -> string list val constrain: term -> typ -> term val param: int -> string * sort -> typ val paramify_dummies: int * typ -> int * typ val get_sort: Type.tsig -> (indexname -> sort option) -> (sort -> sort) -> (indexname * sort) list -> indexname -> sort - val infer_types: (term -> Pretty.T) -> (typ -> Pretty.T) + val infer_types: Pretty.pp -> Type.tsig -> (string -> typ option) -> (indexname -> typ option) -> (indexname -> sort option) -> (string -> string) -> (typ -> typ) -> (sort -> sort) -> string list -> bool -> typ list -> term list @@ -253,16 +252,16 @@ exception NO_UNIFIER of string; -fun unify classes arities = +fun unify pp classes arities = let (* adjust sorts of parameters *) fun not_in_sort x S' S = - "Variable " ^ x ^ "::" ^ Sorts.str_of_sort S' ^ " not of sort " ^ - Sorts.str_of_sort S ^ "."; + "Variable " ^ x ^ "::" ^ Pretty.string_of_sort pp S' ^ " not of sort " ^ + Pretty.string_of_sort pp S; - fun no_domain (a, c) = "No way to get " ^ a ^ "::" ^ c ^ "."; + fun no_domain (a, c) = "No way to get " ^ Pretty.string_of_arity pp (a, [], [c]); fun meet (_, []) = () | meet (Link (r as (ref (Param S'))), S) = @@ -304,7 +303,7 @@ | unif (T, Link (ref U)) = unif (T, U) | unif (PType (a, Ts), PType (b, Us)) = if a <> b then - raise NO_UNIFIER ("Clash of types " ^ quote a ^ " and " ^ quote b ^ ".") + raise NO_UNIFIER ("Clash of types " ^ quote a ^ " and " ^ quote b) else seq2 unif (Ts, Us) | unif (T, U) = if T = U then () else raise NO_UNIFIER ""; @@ -314,24 +313,26 @@ (** type inference **) -fun appl_error prt prT why t T u U = +fun appl_error pp why t T u U = ["Type error in application: " ^ why, "", Pretty.string_of (Pretty.block - [Pretty.str "Operator:", Pretty.brk 2, prt t, Pretty.str " ::", Pretty.brk 1, prT T]), + [Pretty.str "Operator:", Pretty.brk 2, Pretty.term pp t, + Pretty.str " ::", Pretty.brk 1, Pretty.typ pp T]), Pretty.string_of (Pretty.block - [Pretty.str "Operand:", Pretty.brk 3, prt u, Pretty.str " ::", Pretty.brk 1, prT U]), + [Pretty.str "Operand:", Pretty.brk 3, Pretty.term pp u, + Pretty.str " ::", Pretty.brk 1, Pretty.typ pp U]), ""]; (* infer *) (*DESTRUCTIVE*) -fun infer prt prT classes arities = +fun infer pp classes arities = let (* errors *) fun unif_failed msg = - "Type unification failed" ^ (if msg = "" then "." else ": " ^ msg) ^ "\n"; + "Type unification failed" ^ (if msg = "" then "" else ": " ^ msg) ^ "\n"; fun prep_output bs ts Ts = let @@ -349,10 +350,9 @@ val ([t', u'], [T', U']) = prep_output bs [t, u] [T, U]; val why = (case T' of - Type ("fun", _) => "Incompatible operand type." - | _ => "Operator not of function type."); - val text = unif_failed msg ^ - cat_lines (appl_error prt prT why t' T' u' U'); + Type ("fun", _) => "Incompatible operand type" + | _ => "Operator not of function type"); + val text = unif_failed msg ^ cat_lines (appl_error pp why t' T' u' U'); in raise TYPE (text, [T', U'], [t', u']) end; fun err_constraint msg bs t T U = @@ -361,17 +361,17 @@ val text = cat_lines [unif_failed msg, "Cannot meet type constraint:", "", - Pretty.string_of - (Pretty.block [Pretty.str "Term:", Pretty.brk 2, prt t', - Pretty.str " ::", Pretty.brk 1, prT T']), - Pretty.string_of - (Pretty.block [Pretty.str "Type:", Pretty.brk 2, prT U']), ""]; + Pretty.string_of (Pretty.block + [Pretty.str "Term:", Pretty.brk 2, Pretty.term pp t', + Pretty.str " ::", Pretty.brk 1, Pretty.typ pp T']), + Pretty.string_of (Pretty.block + [Pretty.str "Type:", Pretty.brk 2, Pretty.typ pp U']), ""]; in raise TYPE (text, [T', U'], [t']) end; (* main *) - val unif = unify classes arities; + val unif = unify pp classes arities; fun inf _ (PConst (_, T)) = T | inf _ (PFree (_, T)) = T @@ -397,7 +397,7 @@ (* basic_infer_types *) -fun basic_infer_types prt prT const_type classes arities used freeze is_param ts Ts = +fun basic_infer_types pp const_type classes arities used freeze is_param ts Ts = let (*convert to preterms/typs*) val (Tps, Ts') = pretyps_of (K true) ([], Ts); @@ -405,7 +405,7 @@ (*run type inference*) val tTs' = ListPair.map Constraint (ts', Ts'); - val _ = seq (fn t => (infer prt prT classes arities t; ())) tTs'; + val _ = seq (fn t => (infer pp classes arities t; ())) tTs'; (*collect result unifier*) fun ch_var (xi, Link (r as ref (Param S))) = (r := PTVar (xi, S); None) @@ -452,11 +452,9 @@ xi = xi' andalso Type.eq_sort tsig (S, S'); val env = gen_distinct eq (map (apsnd map_sort) raw_env); - val _ = - (case gen_duplicates eq_fst env of - [] => () - | dups => error ("Inconsistent sort constraints for type variable(s) " ^ - commas (map (quote o Syntax.string_of_vname' o fst) dups))); + val _ = (case gen_duplicates eq_fst env of [] => () + | dups => error ("Inconsistent sort constraints for type variable(s) " + ^ commas_quote (map (Syntax.string_of_vname' o fst) dups))); fun get xi = (case (assoc (env, xi), def_sort xi) of @@ -516,7 +514,7 @@ used: list of already used type variables freeze: if true then generated parameters are turned into TFrees, else TVars*) -fun infer_types prt prT tsig const_type def_type def_sort +fun infer_types pp tsig const_type def_type def_sort map_const map_type map_sort used freeze pat_Ts raw_ts = let val {classes, arities, ...} = Type.rep_tsig tsig; @@ -524,7 +522,7 @@ val is_const = is_some o const_type; val raw_ts' = map (decode_types tsig is_const def_type def_sort map_const map_type map_sort) raw_ts; - val (ts, Ts, unifier) = basic_infer_types prt prT const_type + val (ts, Ts, unifier) = basic_infer_types pp const_type classes arities used freeze is_param raw_ts' pat_Ts'; in (ts, unifier) end;