--- 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 *)
--- 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;
--- 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;
--- 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;
--- 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, [])
--- 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;