--- a/src/HOL/Nominal/nominal_datatype.ML Mon Apr 18 12:12:42 2011 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML Mon Apr 18 15:02:50 2011 +0200
@@ -211,7 +211,7 @@
val tyvars = map (map (fn s =>
(s, the (AList.lookup (op =) sorts s))) o #1) dts';
- fun inter_sort thy S S' = Type.inter_sort (Sign.tsig_of thy) (S, S');
+ fun inter_sort thy S S' = Sign.inter_sort thy (S, S');
fun augment_sort_typ thy S =
let val S = Sign.minimize_sort thy (Sign.certify_sort thy S)
in map_type_tfree (fn (s, S') => TFree (s,
--- a/src/HOL/Tools/Function/partial_function.ML Mon Apr 18 12:12:42 2011 +0200
+++ b/src/HOL/Tools/Function/partial_function.ML Mon Apr 18 15:02:50 2011 +0200
@@ -125,7 +125,7 @@
val thy = Proof_Context.theory_of ctxt;
val T = domain_type (fastype_of t);
val T' = fastype_of u;
- val subst = Type.typ_match (Sign.tsig_of thy) (T, T') Vartab.empty
+ val subst = Sign.typ_match thy (T, T') Vartab.empty
handle Type.TYPE_MATCH => raise TYPE ("apply_inst", [T, T'], [t, u])
in
map_types (Envir.norm_type subst) t $ u
--- a/src/HOL/Tools/enriched_type.ML Mon Apr 18 12:12:42 2011 +0200
+++ b/src/HOL/Tools/enriched_type.ML Mon Apr 18 15:02:50 2011 +0200
@@ -218,10 +218,11 @@
val qualify = Binding.qualify true prfx o Binding.name;
fun mapper_declaration comp_thm id_thm phi context =
let
- val typ_instance = Type.typ_instance (Proof_Context.tsig_of (Context.proof_of context));
+ val typ_instance = Sign.typ_instance (Context.theory_of context);
val mapper' = Morphism.term phi mapper;
val T_T' = pairself fastype_of (mapper, mapper');
- in if typ_instance T_T' andalso typ_instance (swap T_T')
+ in
+ if typ_instance T_T' andalso typ_instance (swap T_T')
then (Data.map o Symtab.cons_list) (tyco,
{ mapper = mapper', variances = variances,
comp = Morphism.thm phi comp_thm, id = Morphism.thm phi id_thm }) context
--- a/src/Pure/General/pretty.ML Mon Apr 18 12:12:42 2011 +0200
+++ b/src/Pure/General/pretty.ML Mon Apr 18 15:02:50 2011 +0200
@@ -64,18 +64,6 @@
val writeln: T -> unit
val to_ML: T -> ML_Pretty.pretty
val from_ML: ML_Pretty.pretty -> T
- type pp
- val pp: (term -> T) * (typ -> T) * (sort -> T) * (class list -> T) * (arity -> T) -> pp
- val term: pp -> term -> T
- val typ: pp -> typ -> T
- val sort: pp -> sort -> T
- val classrel: pp -> class list -> T
- val arity: pp -> arity -> T
- val string_of_term: pp -> term -> string
- val string_of_typ: pp -> typ -> string
- val string_of_sort: pp -> sort -> string
- val string_of_classrel: pp -> class list -> string
- val string_of_arity: pp -> arity -> string
end;
structure Pretty: PRETTY =
@@ -332,27 +320,4 @@
end;
-
-
-(** abstract pretty printing context **)
-
-datatype pp =
- PP of (term -> T) * (typ -> T) * (sort -> T) * (class list -> T) * (arity -> T);
-
-val pp = PP;
-
-fun pp_fun f (PP x) = f x;
-
-val term = pp_fun #1;
-val typ = pp_fun #2;
-val sort = pp_fun #3;
-val classrel = pp_fun #4;
-val arity = pp_fun #5;
-
-val string_of_term = string_of oo term;
-val string_of_typ = string_of oo typ;
-val string_of_sort = string_of oo sort;
-val string_of_classrel = string_of oo classrel;
-val string_of_arity = string_of oo arity;
-
end;
--- a/src/Pure/Isar/class.ML Mon Apr 18 12:12:42 2011 +0200
+++ b/src/Pure/Isar/class.ML Mon Apr 18 15:02:50 2011 +0200
@@ -450,15 +450,16 @@
(((primary_constraints, []), (((improve, subst), false), unchecks)), false))
end;
-fun resort_terms pp algebra consts constraints ts =
+fun resort_terms ctxt algebra consts constraints ts =
let
- fun matchings (Const (c_ty as (c, _))) = (case constraints c
- of NONE => I
- | SOME sorts => fold2 (curry (Sorts.meet_sort algebra))
- (Consts.typargs consts c_ty) sorts)
- | matchings _ = I
+ fun matchings (Const (c_ty as (c, _))) =
+ (case constraints c of
+ NONE => I
+ | SOME sorts =>
+ fold2 (curry (Sorts.meet_sort algebra)) (Consts.typargs consts c_ty) sorts)
+ | matchings _ = I;
val tvartab = (fold o fold_aterms) matchings ts Vartab.empty
- handle Sorts.CLASS_ERROR e => error (Sorts.class_error pp e);
+ handle Sorts.CLASS_ERROR e => error (Sorts.class_error ctxt e);
val inst = map_type_tvar
(fn (vi, sort) => TVar (vi, the_default sort (Vartab.lookup tvartab vi)));
in if Vartab.is_empty tvartab then NONE else SOME ((map o map_types) inst ts) end;
@@ -529,19 +530,20 @@
val primary_constraints = map (apsnd
(map_atyps (K (TVar ((Name.aT, 0), [])))) o snd o snd) class_params;
val algebra = Sign.classes_of thy
- |> fold (fn tyco => Sorts.add_arities (Syntax.pp_global thy)
+ |> fold (fn tyco => Sorts.add_arities (Proof_Context.init_global thy)
(tyco, map (fn class => (class, map snd vs)) sort)) tycos;
val consts = Sign.consts_of thy;
val improve_constraints = AList.lookup (op =)
(map (fn (_, (class, (c, _))) => (c, [[class]])) class_params);
- fun resort_check ts ctxt = case resort_terms (Syntax.pp ctxt) algebra consts improve_constraints ts
- of NONE => NONE
- | SOME ts' => SOME (ts', ctxt);
+ fun resort_check ts ctxt =
+ (case resort_terms ctxt algebra consts improve_constraints ts of
+ NONE => NONE
+ | SOME ts' => SOME (ts', ctxt));
val lookup_inst_param = AxClass.lookup_inst_param consts params;
- val typ_instance = Type.typ_instance (Sign.tsig_of thy);
- fun improve (c, ty) = case lookup_inst_param (c, ty)
- of SOME (_, ty') => if typ_instance (ty', ty) then SOME (ty, ty') else NONE
- | NONE => NONE;
+ fun improve (c, ty) =
+ (case lookup_inst_param (c, ty) of
+ SOME (_, ty') => if Sign.typ_instance thy (ty', ty) then SOME (ty, ty') else NONE
+ | NONE => NONE);
in
thy
|> Theory.checkpoint
@@ -559,7 +561,8 @@
notes = Generic_Target.notes
(fn kind => fn global_facts => fn _ => Generic_Target.theory_notes kind global_facts),
abbrev = Generic_Target.abbrev
- (fn prmode => fn (b, mx) => fn (t, _) => fn _ => Generic_Target.theory_abbrev prmode ((b, mx), t)),
+ (fn prmode => fn (b, mx) => fn (t, _) => fn _ =>
+ Generic_Target.theory_abbrev prmode ((b, mx), t)),
declaration = K Generic_Target.theory_declaration,
syntax_declaration = K Generic_Target.theory_declaration,
pretty = pretty,
--- a/src/Pure/Isar/overloading.ML Mon Apr 18 12:12:42 2011 +0200
+++ b/src/Pure/Isar/overloading.ML Mon Apr 18 15:02:50 2011 +0200
@@ -63,20 +63,25 @@
fun improve_term_check ts ctxt =
let
+ val thy = Proof_Context.theory_of ctxt;
+
val { secondary_constraints, improve, subst, consider_abbrevs, passed, ... } =
ImprovableSyntax.get ctxt;
- val tsig = (Sign.tsig_of o Proof_Context.theory_of) ctxt;
val is_abbrev = consider_abbrevs andalso Proof_Context.abbrev_mode ctxt;
val passed_or_abbrev = passed orelse is_abbrev;
- fun accumulate_improvements (Const (c, ty)) = (case improve (c, ty)
- of SOME ty_ty' => Type.typ_match tsig ty_ty'
+ fun accumulate_improvements (Const (c, ty)) =
+ (case improve (c, ty) of
+ SOME ty_ty' => Sign.typ_match thy ty_ty'
| _ => I)
| accumulate_improvements _ = I;
val improvements = (fold o fold_aterms) accumulate_improvements ts Vartab.empty;
val ts' = (map o map_types) (Envir.subst_type improvements) ts;
- fun apply_subst t = Envir.expand_term (fn Const (c, ty) => (case subst (c, ty)
- of SOME (ty', t') =>
- if Type.typ_instance tsig (ty, ty')
+ fun apply_subst t =
+ Envir.expand_term
+ (fn Const (c, ty) =>
+ (case subst (c, ty) of
+ SOME (ty', t') =>
+ if Sign.typ_instance thy (ty, ty')
then SOME (ty', apply_subst t') else NONE
| NONE => NONE)
| _ => NONE) t;
--- a/src/Pure/Isar/proof_context.ML Mon Apr 18 12:12:42 2011 +0200
+++ b/src/Pure/Isar/proof_context.ML Mon Apr 18 15:02:50 2011 +0200
@@ -302,7 +302,7 @@
map_tsig (fn tsig as (local_tsig, global_tsig) =>
let val thy_tsig = Sign.tsig_of thy in
if Type.eq_tsig (thy_tsig, global_tsig) then tsig
- else (Type.merge_tsig (Syntax.pp ctxt) (local_tsig, thy_tsig), thy_tsig)
+ else (Type.merge_tsig ctxt (local_tsig, thy_tsig), thy_tsig)
end) |>
map_consts (fn consts as (local_consts, global_consts) =>
let val thy_consts = Sign.consts_of thy in
@@ -376,7 +376,7 @@
fun prep_arity prep_tycon prep_sort ctxt (t, Ss, S) =
let val arity = (prep_tycon ctxt t, map (prep_sort ctxt) Ss, prep_sort ctxt S)
- in Type.add_arity (Syntax.pp ctxt) arity (tsig_of ctxt); arity end;
+ in Type.add_arity ctxt arity (tsig_of ctxt); arity end;
in
@@ -546,7 +546,7 @@
local
-fun certify_consts ctxt = Consts.certify (Syntax.pp ctxt) (tsig_of ctxt)
+fun certify_consts ctxt = Consts.certify (Context.pretty ctxt) (tsig_of ctxt)
(not (abbrev_mode ctxt)) (consts_of ctxt);
fun expand_binds ctxt =
@@ -666,9 +666,9 @@
fun gen_cert prop ctxt t =
t
|> expand_abbrevs ctxt
- |> (fn t' => #1 (Sign.certify' prop (Syntax.pp ctxt) false (consts_of ctxt) (theory_of ctxt) t')
- handle TYPE (msg, _, _) => error msg
- | TERM (msg, _) => error msg);
+ |> (fn t' =>
+ #1 (Sign.certify' prop (Context.pretty ctxt) false (consts_of ctxt) (theory_of ctxt) t')
+ handle TYPE (msg, _, _) => error msg | TERM (msg, _) => error msg);
in
--- a/src/Pure/ROOT.ML Mon Apr 18 12:12:42 2011 +0200
+++ b/src/Pure/ROOT.ML Mon Apr 18 15:02:50 2011 +0200
@@ -53,6 +53,7 @@
use "General/xml.ML";
use "General/xml_data.ML";
use "General/yxml.ML";
+use "General/pretty.ML";
use "General/sha1.ML";
if String.isPrefix "polyml" ml_system
@@ -103,24 +104,15 @@
use "name.ML";
use "term.ML";
-use "term_ord.ML";
-use "term_subst.ML";
-use "old_term.ML";
-use "General/pretty.ML";
use "context.ML";
use "config.ML";
use "context_position.ML";
-use "General/name_space.ML";
-use "sorts.ML";
-use "type.ML";
-use "logic.ML";
(* inner syntax *)
use "Syntax/term_position.ML";
use "Syntax/lexicon.ML";
-use "Syntax/simple_syntax.ML";
use "Syntax/ast.ML";
use "Syntax/syntax_ext.ML";
use "Syntax/parser.ML";
@@ -132,6 +124,14 @@
(* core of tactical proof system *)
+use "term_ord.ML";
+use "term_subst.ML";
+use "old_term.ML";
+use "General/name_space.ML";
+use "sorts.ML";
+use "type.ML";
+use "logic.ML";
+use "Syntax/simple_syntax.ML";
use "net.ML";
use "item_net.ML";
use "envir.ML";
--- a/src/Pure/Syntax/printer.ML Mon Apr 18 12:12:42 2011 +0200
+++ b/src/Pure/Syntax/printer.ML Mon Apr 18 15:02:50 2011 +0200
@@ -36,12 +36,12 @@
val pretty_term_ast: bool -> Proof.context -> prtabs ->
(string -> Proof.context -> Ast.ast list -> Ast.ast) ->
(string -> string -> Pretty.T option) ->
- (string -> Markup.T list * xstring) ->
+ (string -> Markup.T list * string) ->
Ast.ast -> Pretty.T list
val pretty_typ_ast: Proof.context -> prtabs ->
(string -> Proof.context -> Ast.ast list -> Ast.ast) ->
(string -> string -> Pretty.T option) ->
- (string -> Markup.T list * xstring) -> Ast.ast -> Pretty.T list
+ (string -> Markup.T list * string) -> Ast.ast -> Pretty.T list
end;
structure Printer: PRINTER =
--- a/src/Pure/Syntax/syntax.ML Mon Apr 18 12:12:42 2011 +0200
+++ b/src/Pure/Syntax/syntax.ML Mon Apr 18 15:02:50 2011 +0200
@@ -10,6 +10,8 @@
val const: string -> term
val free: string -> term
val var: indexname -> term
+ type operations
+ val install_operations: operations -> unit
val root: string Config.T
val positions_raw: Config.raw
val positions: bool Config.T
@@ -28,14 +30,6 @@
val unparse_arity: Proof.context -> arity -> Pretty.T
val unparse_typ: Proof.context -> typ -> Pretty.T
val unparse_term: Proof.context -> term -> Pretty.T
- val install_operations:
- {parse_sort: Proof.context -> string -> sort,
- parse_typ: Proof.context -> string -> typ,
- parse_term: Proof.context -> string -> term,
- parse_prop: Proof.context -> string -> term,
- unparse_sort: Proof.context -> sort -> Pretty.T,
- unparse_typ: Proof.context -> typ -> Pretty.T,
- unparse_term: Proof.context -> term -> Pretty.T} -> unit
val print_checks: Proof.context -> unit
val add_typ_check: int -> string ->
(typ list -> Proof.context -> (typ list * Proof.context) option) ->
@@ -49,6 +43,10 @@
val add_term_uncheck: int -> string ->
(term list -> Proof.context -> (term list * Proof.context) option) ->
Context.generic -> Context.generic
+ val typ_check: Proof.context -> typ list -> typ list
+ val term_check: Proof.context -> term list -> term list
+ val typ_uncheck: Proof.context -> typ list -> typ list
+ val term_uncheck: Proof.context -> term list -> term list
val check_sort: Proof.context -> sort -> sort
val check_typ: Proof.context -> typ -> typ
val check_term: Proof.context -> term -> term
@@ -84,14 +82,13 @@
val is_pretty_global: Proof.context -> bool
val set_pretty_global: bool -> Proof.context -> Proof.context
val init_pretty_global: theory -> Proof.context
+ val init_pretty: Context.pretty -> Proof.context
val pretty_term_global: theory -> term -> Pretty.T
val pretty_typ_global: theory -> typ -> Pretty.T
val pretty_sort_global: theory -> sort -> Pretty.T
val string_of_term_global: theory -> term -> string
val string_of_typ_global: theory -> typ -> string
val string_of_sort_global: theory -> sort -> string
- val pp: Proof.context -> Pretty.pp
- val pp_global: theory -> Pretty.pp
type syntax
val eq_syntax: syntax * syntax -> bool
val lookup_const: syntax -> string -> string option
@@ -151,6 +148,31 @@
(** inner syntax operations **)
+(* back-patched operations *)
+
+type operations =
+ {parse_sort: Proof.context -> string -> sort,
+ parse_typ: Proof.context -> string -> typ,
+ parse_term: Proof.context -> string -> term,
+ parse_prop: Proof.context -> string -> term,
+ unparse_sort: Proof.context -> sort -> Pretty.T,
+ unparse_typ: Proof.context -> typ -> Pretty.T,
+ unparse_term: Proof.context -> term -> Pretty.T,
+ check_typs: Proof.context -> typ list -> typ list,
+ check_terms: Proof.context -> term list -> term list,
+ check_props: Proof.context -> term list -> term list,
+ uncheck_typs: Proof.context -> typ list -> typ list,
+ uncheck_terms: Proof.context -> term list -> term list};
+
+val operations: operations Single_Assignment.var = Single_Assignment.var "Syntax.operations";
+fun install_operations ops = Single_Assignment.assign operations ops;
+
+fun operation which ctxt x =
+ (case Single_Assignment.peek operations of
+ NONE => raise Fail "Inner syntax operations not installed"
+ | SOME ops => which ops ctxt x);
+
+
(* configuration options *)
val root = Config.string (Config.declare "syntax_root" (K (Config.String "any")));
@@ -191,26 +213,6 @@
val _ = Context_Position.report ctxt pos markup;
in (syms, pos) end;
-local
-
-type operations =
- {parse_sort: Proof.context -> string -> sort,
- parse_typ: Proof.context -> string -> typ,
- parse_term: Proof.context -> string -> term,
- parse_prop: Proof.context -> string -> term,
- unparse_sort: Proof.context -> sort -> Pretty.T,
- unparse_typ: Proof.context -> typ -> Pretty.T,
- unparse_term: Proof.context -> term -> Pretty.T};
-
-val operations: operations Single_Assignment.var = Single_Assignment.var "Syntax.operations";
-
-fun operation which ctxt x =
- (case Single_Assignment.peek operations of
- NONE => raise Fail "Inner syntax operations not installed"
- | SOME ops => which ops ctxt x);
-
-in
-
val parse_sort = operation #parse_sort;
val parse_typ = operation #parse_typ;
val parse_term = operation #parse_term;
@@ -219,10 +221,6 @@
val unparse_typ = operation #unparse_typ;
val unparse_term = operation #unparse_term;
-fun install_operations ops = Single_Assignment.assign operations ops;
-
-end;
-
(* context-sensitive (un)checking *)
@@ -290,17 +288,22 @@
fun add_typ_uncheck stage = gen_add apfst (stage, true);
fun add_term_uncheck stage = gen_add apsnd (stage, true);
-val check_typs = gen_check fst false;
-val check_terms = gen_check snd false;
-fun check_props ctxt = map (Type.constraint propT) #> check_terms ctxt;
+val typ_check = gen_check fst false;
+val term_check = gen_check snd false;
+val typ_uncheck = gen_check fst true;
+val term_uncheck = gen_check snd true;
+
+val check_typs = operation #check_typs;
+val check_terms = operation #check_terms;
+val check_props = operation #check_props;
val check_typ = singleton o check_typs;
val check_term = singleton o check_terms;
val check_prop = singleton o check_props;
val check_sort = map_sort o check_typ;
-val uncheck_typs = gen_check fst true;
-val uncheck_terms = gen_check snd true;
+val uncheck_typs = operation #uncheck_typs;
+val uncheck_terms = operation #uncheck_terms;
val uncheck_sort = map_sort o singleton o uncheck_typs;
end;
@@ -371,6 +374,7 @@
fun is_pretty_global ctxt = Config.get ctxt pretty_global;
val set_pretty_global = Config.put pretty_global;
val init_pretty_global = set_pretty_global true o Proof_Context.init_global;
+val init_pretty = Context.pretty_context init_pretty_global;
val pretty_term_global = pretty_term o init_pretty_global;
val pretty_typ_global = pretty_typ o init_pretty_global;
@@ -381,23 +385,6 @@
val string_of_sort_global = string_of_sort o init_pretty_global;
-(* pp operations -- deferred evaluation *)
-
-fun pp ctxt = Pretty.pp
- (fn x => pretty_term ctxt x,
- fn x => pretty_typ ctxt x,
- fn x => pretty_sort ctxt x,
- fn x => pretty_classrel ctxt x,
- fn x => pretty_arity ctxt x);
-
-fun pp_global thy = Pretty.pp
- (fn x => pretty_term_global thy x,
- fn x => pretty_typ_global thy x,
- fn x => pretty_sort_global thy x,
- fn x => pretty_classrel (init_pretty_global thy) x,
- fn x => pretty_arity (init_pretty_global thy) x);
-
-
(** tables of translation functions **)
--- a/src/Pure/Syntax/syntax_phases.ML Mon Apr 18 12:12:42 2011 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML Mon Apr 18 15:02:50 2011 +0200
@@ -702,6 +702,17 @@
+(** check/uncheck **)
+
+val check_typs = Syntax.typ_check;
+val check_terms = Syntax.term_check;
+fun check_props ctxt = map (Type.constraint propT) #> check_terms ctxt;
+
+val uncheck_typs = Syntax.typ_uncheck;
+val uncheck_terms = Syntax.term_uncheck;
+
+
+
(** install operations **)
val _ = Syntax.install_operations
@@ -711,6 +722,11 @@
parse_prop = parse_term true,
unparse_sort = unparse_sort,
unparse_typ = unparse_typ,
- unparse_term = unparse_term};
+ unparse_term = unparse_term,
+ check_typs = check_typs,
+ check_terms = check_terms,
+ check_props = check_props,
+ uncheck_typs = uncheck_typs,
+ uncheck_terms = uncheck_terms};
end;
--- a/src/Pure/axclass.ML Mon Apr 18 12:12:42 2011 +0200
+++ b/src/Pure/axclass.ML Mon Apr 18 15:02:50 2011 +0200
@@ -59,12 +59,12 @@
type param = string * class;
-fun add_param pp ((x, c): param) params =
+fun add_param ctxt ((x, c): param) params =
(case AList.lookup (op =) params x of
NONE => (x, c) :: params
- | SOME c' => error ("Duplicate class parameter " ^ quote x ^
- " for " ^ Pretty.string_of_sort pp [c] ^
- (if c = c' then "" else " and " ^ Pretty.string_of_sort pp [c'])));
+ | SOME c' =>
+ error ("Duplicate class parameter " ^ quote x ^ " for " ^ Syntax.string_of_sort ctxt [c] ^
+ (if c = c' then "" else " and " ^ Syntax.string_of_sort ctxt [c'])));
(* setup data *)
@@ -104,10 +104,14 @@
proven_arities = proven_arities2, inst_params = inst_params2,
diff_classrels = diff_classrels2}) =
let
+ val ctxt = Syntax.init_pretty pp;
+
val axclasses' = Symtab.merge (K true) (axclasses1, axclasses2);
val params' =
if null params1 then params2
- else fold_rev (fn p => if member (op =) params1 p then I else add_param pp p) params2 params1;
+ else
+ fold_rev (fn p => if member (op =) params1 p then I else add_param ctxt p)
+ params2 params1;
(*transitive closure of classrels and arity completion is done in Theory.at_begin hook*)
val proven_classrels' = Symreltab.join (K #1) (proven_classrels1, proven_classrels2);
@@ -590,7 +594,7 @@
|> #2
|> Sign.restore_naming facts_thy
|> map_axclasses (Symtab.update (class, axclass))
- |> map_params (fold (fn (x, _) => add_param (Syntax.pp ctxt) (x, class)) params);
+ |> map_params (fold (fn (x, _) => add_param ctxt (x, class)) params);
in (class, result_thy) end;
--- a/src/Pure/consts.ML Mon Apr 18 12:12:42 2011 +0200
+++ b/src/Pure/consts.ML Mon Apr 18 15:02:50 2011 +0200
@@ -26,7 +26,7 @@
val intern_syntax: T -> xstring -> string
val extern_syntax: Proof.context -> T -> string -> xstring
val read_const: T -> string -> term
- val certify: Pretty.pp -> Type.tsig -> bool -> T -> term -> term (*exception TYPE*)
+ val certify: Context.pretty -> Type.tsig -> bool -> T -> term -> term (*exception TYPE*)
val typargs: T -> string * typ -> typ list
val instance: T -> string * typ list -> typ
val declare: Proof.context -> Name_Space.naming -> binding * typ -> T -> T
@@ -156,7 +156,8 @@
fun certify pp tsig do_expand consts =
let
fun err msg (c, T) =
- raise TYPE (msg ^ " " ^ quote c ^ " :: " ^ Pretty.string_of_typ pp T, [], []);
+ raise TYPE (msg ^ " " ^ quote c ^ " :: " ^
+ Syntax.string_of_typ (Syntax.init_pretty pp) T, [], []);
val certT = Type.cert_typ tsig;
fun cert tm =
let
@@ -269,7 +270,7 @@
fun abbreviate ctxt tsig naming mode (b, raw_rhs) consts =
let
- val pp = Syntax.pp ctxt;
+ val pp = Context.pretty ctxt;
val cert_term = certify pp tsig false consts;
val expand_term = certify pp tsig true consts;
val force_expand = mode = Print_Mode.internal;
--- a/src/Pure/context.ML Mon Apr 18 12:12:42 2011 +0200
+++ b/src/Pure/context.ML Mon Apr 18 15:02:50 2011 +0200
@@ -28,6 +28,7 @@
sig
include BASIC_CONTEXT
(*theory context*)
+ type pretty
val parents_of: theory -> theory list
val ancestors_of: theory -> theory list
val theory_name: theory -> string
@@ -52,7 +53,7 @@
val copy_thy: theory -> theory
val checkpoint_thy: theory -> theory
val finish_thy: theory -> theory
- val begin_thy: (theory -> Pretty.pp) -> string -> theory list -> theory
+ val begin_thy: (theory -> pretty) -> string -> theory list -> theory
(*proof context*)
val raw_transfer: theory -> Proof.context -> Proof.context
(*generic context*)
@@ -71,6 +72,10 @@
val proof_map: (generic -> generic) -> Proof.context -> Proof.context
val theory_of: generic -> theory (*total*)
val proof_of: generic -> Proof.context (*total*)
+ (*pretty printing context*)
+ val pretty: Proof.context -> pretty
+ val pretty_global: theory -> pretty
+ val pretty_context: (theory -> Proof.context) -> pretty -> Proof.context
(*thread data*)
val thread_data: unit -> generic option
val the_thread_data: unit -> generic
@@ -86,7 +91,7 @@
structure Theory_Data:
sig
val declare: Object.T -> (Object.T -> Object.T) ->
- (Pretty.pp -> Object.T * Object.T -> Object.T) -> serial
+ (pretty -> Object.T * Object.T -> Object.T) -> serial
val get: serial -> (Object.T -> 'a) -> theory -> 'a
val put: serial -> ('a -> Object.T) -> 'a -> theory -> theory
end
@@ -110,12 +115,14 @@
(*private copy avoids potential conflict of table exceptions*)
structure Datatab = Table(type key = int val ord = int_ord);
+datatype pretty = Pretty of Object.T;
+
local
type kind =
{empty: Object.T,
extend: Object.T -> Object.T,
- merge: Pretty.pp -> Object.T * Object.T -> Object.T};
+ merge: pretty -> Object.T * Object.T -> Object.T};
val kinds = Unsynchronized.ref (Datatab.empty: kind Datatab.table);
@@ -546,6 +553,16 @@
val proof_of = cases Proof_Context.init_global I;
+(* pretty printing context *)
+
+exception PRETTY of generic;
+
+val pretty = Pretty o PRETTY o Proof;
+val pretty_global = Pretty o PRETTY o Theory;
+
+fun pretty_context init (Pretty (PRETTY context)) = cases init I context;
+
+
(** thread data **)
@@ -593,7 +610,7 @@
type T
val empty: T
val extend: T -> T
- val merge: Pretty.pp -> T * T -> T
+ val merge: Context.pretty -> T * T -> T
end;
signature THEORY_DATA_ARGS =
--- a/src/Pure/defs.ML Mon Apr 18 12:12:42 2011 +0200
+++ b/src/Pure/defs.ML Mon Apr 18 15:02:50 2011 +0200
@@ -7,7 +7,7 @@
signature DEFS =
sig
- val pretty_const: Pretty.pp -> string * typ list -> Pretty.T
+ val pretty_const: Proof.context -> string * typ list -> Pretty.T
val plain_args: typ list -> bool
type T
type spec =
@@ -18,8 +18,8 @@
{restricts: ((string * typ list) * string) list,
reducts: ((string * typ list) * (string * typ list) list) list}
val empty: T
- val merge: Pretty.pp -> T * T -> T
- val define: Pretty.pp -> bool -> string option -> string ->
+ val merge: Proof.context -> T * T -> T
+ val define: Proof.context -> bool -> string option -> string ->
string * typ list -> (string * typ list) list -> T -> T
end
@@ -30,11 +30,11 @@
type args = typ list;
-fun pretty_const pp (c, args) =
+fun pretty_const ctxt (c, args) =
let
val prt_args =
if null args then []
- else [Pretty.list "(" ")" (map (Pretty.typ pp o Logic.unvarifyT_global) args)];
+ else [Pretty.list "(" ")" (map (Syntax.pretty_typ ctxt o Logic.unvarifyT_global) args)];
in Pretty.block (Pretty.str c :: prt_args) end;
fun plain_args args =
@@ -118,27 +118,27 @@
local
val prt = Pretty.string_of oo pretty_const;
-fun err pp (c, args) (d, Us) s1 s2 =
- error (s1 ^ " dependency of constant " ^ prt pp (c, args) ^ " -> " ^ prt pp (d, Us) ^ s2);
+fun err ctxt (c, args) (d, Us) s1 s2 =
+ error (s1 ^ " dependency of constant " ^ prt ctxt (c, args) ^ " -> " ^ prt ctxt (d, Us) ^ s2);
fun contained (U as TVar _) (Type (_, Ts)) = exists (fn T => T = U orelse contained U T) Ts
| contained _ _ = false;
-fun acyclic pp (c, args) (d, Us) =
+fun acyclic ctxt (c, args) (d, Us) =
c <> d orelse
exists (fn U => exists (contained U) args) Us orelse
is_none (match_args (args, Us)) orelse
- err pp (c, args) (d, Us) "Circular" "";
+ err ctxt (c, args) (d, Us) "Circular" "";
-fun wellformed pp defs (c, args) (d, Us) =
+fun wellformed ctxt defs (c, args) (d, Us) =
forall is_TVar Us orelse
(case find_first (fn (Ts, _) => not (disjoint_args (Ts, Us))) (restricts_of defs d) of
SOME (Ts, description) =>
- err pp (c, args) (d, Us) "Malformed"
- ("\n(restriction " ^ prt pp (d, Ts) ^ " from " ^ quote description ^ ")")
+ err ctxt (c, args) (d, Us) "Malformed"
+ ("\n(restriction " ^ prt ctxt (d, Ts) ^ " from " ^ quote description ^ ")")
| NONE => true);
-fun reduction pp defs const deps =
+fun reduction ctxt defs const deps =
let
fun reduct Us (Ts, rhs) =
(case match_args (Ts, Us) of
@@ -151,17 +151,17 @@
if forall (is_none o #1) reds then NONE
else SOME (fold_rev
(fn (NONE, dp) => insert (op =) dp | (SOME dps, _) => fold (insert (op =)) dps) reds []);
- val _ = forall (acyclic pp const) (the_default deps deps');
+ val _ = forall (acyclic ctxt const) (the_default deps deps');
in deps' end;
in
-fun normalize pp =
+fun normalize ctxt =
let
fun norm_update (c, {reducts, ...}: def) (changed, defs) =
let
val reducts' = reducts |> map (fn (args, deps) =>
- (args, perhaps (reduction pp defs (c, args)) deps));
+ (args, perhaps (reduction ctxt defs (c, args)) deps));
in
if reducts = reducts' then (changed, defs)
else (true, defs |> map_def c (fn (specs, restricts, _) => (specs, restricts, reducts')))
@@ -171,38 +171,38 @@
(true, defs') => norm_all defs'
| (false, _) => defs);
fun check defs (c, {reducts, ...}: def) =
- reducts |> forall (fn (args, deps) => forall (wellformed pp defs (c, args)) deps);
+ reducts |> forall (fn (args, deps) => forall (wellformed ctxt defs (c, args)) deps);
in norm_all #> (fn defs => tap (Symtab.forall (check defs)) defs) end;
-fun dependencies pp (c, args) restr deps =
+fun dependencies ctxt (c, args) restr deps =
map_def c (fn (specs, restricts, reducts) =>
let
val restricts' = Library.merge (op =) (restricts, restr);
val reducts' = insert (op =) (args, deps) reducts;
in (specs, restricts', reducts') end)
- #> normalize pp;
+ #> normalize ctxt;
end;
(* merge *)
-fun merge pp (Defs defs1, Defs defs2) =
+fun merge ctxt (Defs defs1, Defs defs2) =
let
fun add_deps (c, args) restr deps defs =
if AList.defined (op =) (reducts_of defs c) args then defs
- else dependencies pp (c, args) restr deps defs;
+ else dependencies ctxt (c, args) restr deps defs;
fun add_def (c, {restricts, reducts, ...}: def) =
fold (fn (args, deps) => add_deps (c, args) restricts deps) reducts;
in
Defs (Symtab.join join_specs (defs1, defs2)
- |> normalize pp |> Symtab.fold add_def defs2)
+ |> normalize ctxt |> Symtab.fold add_def defs2)
end;
(* define *)
-fun define pp unchecked def description (c, args) deps (Defs defs) =
+fun define ctxt unchecked def description (c, args) deps (Defs defs) =
let
val restr =
if plain_args args orelse
@@ -211,6 +211,6 @@
val spec =
(serial (), {def = def, description = description, lhs = args, rhs = deps});
val defs' = defs |> update_specs c spec;
- in Defs (defs' |> (if unchecked then I else dependencies pp (c, args) restr deps)) end;
+ in Defs (defs' |> (if unchecked then I else dependencies ctxt (c, args) restr deps)) end;
end;
--- a/src/Pure/display.ML Mon Apr 18 12:12:42 2011 +0200
+++ b/src/Pure/display.ML Mon Apr 18 15:02:50 2011 +0200
@@ -143,7 +143,7 @@
fun prt_term t = Pretty.quote (Syntax.pretty_term ctxt t);
val prt_term_no_vars = prt_term o Logic.unvarify_global;
fun prt_const (c, ty) = [Pretty.str c, Pretty.str " ::", Pretty.brk 1, prt_typ_no_tvars ty];
- val prt_const' = Defs.pretty_const (Syntax.pp ctxt);
+ val prt_const' = Defs.pretty_const ctxt;
fun pretty_classrel (c, []) = prt_cls c
| pretty_classrel (c, cs) = Pretty.block
--- a/src/Pure/sign.ML Mon Apr 18 12:12:42 2011 +0200
+++ b/src/Pure/sign.ML Mon Apr 18 15:02:50 2011 +0200
@@ -61,7 +61,7 @@
val certify_sort: theory -> sort -> sort
val certify_typ: theory -> typ -> typ
val certify_typ_mode: Type.mode -> theory -> typ -> typ
- val certify': bool -> Pretty.pp -> bool -> Consts.T -> theory -> term -> term * typ * int
+ val certify': bool -> Context.pretty -> bool -> Consts.T -> theory -> term -> term * typ * int
val certify_term: theory -> term -> term * typ * int
val cert_term: theory -> term -> term
val cert_prop: theory -> term -> term
@@ -144,12 +144,13 @@
fun merge pp (sign1, sign2) =
let
+ val ctxt = Syntax.init_pretty pp;
val Sign {naming = _, syn = syn1, tsig = tsig1, consts = consts1} = sign1;
val Sign {naming = _, syn = syn2, tsig = tsig2, consts = consts2} = sign2;
val naming = Name_Space.default_naming;
val syn = Syntax.merge_syntaxes syn1 syn2;
- val tsig = Type.merge_tsig pp (tsig1, tsig2);
+ val tsig = Type.merge_tsig ctxt (tsig1, tsig2);
val consts = Consts.merge (consts1, consts2);
in make_sign (naming, syn, tsig, consts) end;
);
@@ -243,11 +244,11 @@
(* certify wrt. type signature *)
val arity_number = Type.arity_number o tsig_of;
-fun arity_sorts thy = Type.arity_sorts (Syntax.pp_global thy) (tsig_of thy);
+fun arity_sorts thy = Type.arity_sorts (Context.pretty_global thy) (tsig_of thy);
-val certify_class = Type.cert_class o tsig_of;
-val certify_sort = Type.cert_sort o tsig_of;
-val certify_typ = Type.cert_typ o tsig_of;
+val certify_class = Type.cert_class o tsig_of;
+val certify_sort = Type.cert_sort o tsig_of;
+val certify_typ = Type.cert_typ o tsig_of;
fun certify_typ_mode mode = Type.cert_typ_mode mode o tsig_of;
@@ -262,7 +263,7 @@
val xs = map Free bs; (*we do not rename here*)
val t' = subst_bounds (xs, t);
val u' = subst_bounds (xs, u);
- val msg = Type.appl_error pp t' T u' U;
+ val msg = Type.appl_error (Syntax.init_pretty pp) t' T u' U;
in raise TYPE (msg, [T, U], [t', u']) end;
fun typ_of (_, Const (_, T)) = T
@@ -301,10 +302,11 @@
val tm'' = Consts.certify pp (tsig_of thy) do_expand consts tm';
in (if tm = tm'' then tm else tm'', T, Term.maxidx_of_term tm'') end;
-fun certify_term thy = certify' false (Syntax.pp_global thy) true (consts_of thy) thy;
-fun cert_term_abbrev thy = #1 o certify' false (Syntax.pp_global thy) false (consts_of thy) thy;
+fun certify_term thy = certify' false (Context.pretty_global thy) true (consts_of thy) thy;
+fun cert_term_abbrev thy =
+ #1 o certify' false (Context.pretty_global thy) false (consts_of thy) thy;
val cert_term = #1 oo certify_term;
-fun cert_prop thy = #1 o certify' true (Syntax.pp_global thy) true (consts_of thy) thy;
+fun cert_prop thy = #1 o certify' true (Context.pretty_global thy) true (consts_of thy) thy;
end;
@@ -454,15 +456,19 @@
(* primitive classes and arities *)
fun primitive_class (bclass, classes) thy =
- thy |> map_sign (fn (naming, syn, tsig, consts) =>
+ thy
+ |> map_sign (fn (naming, syn, tsig, consts) =>
let
val ctxt = Syntax.init_pretty_global thy;
- val tsig' = Type.add_class ctxt (Syntax.pp ctxt) naming (bclass, classes) tsig;
+ val tsig' = Type.add_class ctxt naming (bclass, classes) tsig;
in (naming, syn, tsig', consts) end)
|> add_consts_i [(Binding.map_name Logic.const_of_class bclass, Term.a_itselfT --> propT, NoSyn)];
-fun primitive_classrel arg thy = thy |> map_tsig (Type.add_classrel (Syntax.pp_global thy) arg);
-fun primitive_arity arg thy = thy |> map_tsig (Type.add_arity (Syntax.pp_global thy) arg);
+fun primitive_classrel arg thy =
+ thy |> map_tsig (Type.add_classrel (Syntax.init_pretty_global thy) arg);
+
+fun primitive_arity arg thy =
+ thy |> map_tsig (Type.add_arity (Syntax.init_pretty_global thy) arg);
(* add translation functions *)
--- a/src/Pure/sorts.ML Mon Apr 18 12:12:42 2011 +0200
+++ b/src/Pure/sorts.ML Mon Apr 18 15:02:50 2011 +0200
@@ -40,15 +40,15 @@
val minimal_sorts: algebra -> sort list -> sort Ord_List.T
val certify_class: algebra -> class -> class (*exception TYPE*)
val certify_sort: algebra -> sort -> sort (*exception TYPE*)
- val add_class: Pretty.pp -> class * class list -> algebra -> algebra
- val add_classrel: Pretty.pp -> class * class -> algebra -> algebra
- val add_arities: Pretty.pp -> string * (class * sort list) list -> algebra -> algebra
+ val add_class: Proof.context -> class * class list -> algebra -> algebra
+ val add_classrel: Proof.context -> class * class -> algebra -> algebra
+ val add_arities: Proof.context -> string * (class * sort list) list -> algebra -> algebra
val empty_algebra: algebra
- val merge_algebra: Pretty.pp -> algebra * algebra -> algebra
- val subalgebra: Pretty.pp -> (class -> bool) -> (class * string -> sort list option)
+ val merge_algebra: Proof.context -> algebra * algebra -> algebra
+ val subalgebra: Proof.context -> (class -> bool) -> (class * string -> sort list option)
-> algebra -> (sort -> sort) * algebra
type class_error
- val class_error: Pretty.pp -> class_error -> string
+ val class_error: Proof.context -> class_error -> string
exception CLASS_ERROR of class_error
val mg_domain: algebra -> string -> sort -> sort list (*exception CLASS_ERROR*)
val meet_sort: algebra -> typ * sort
@@ -198,16 +198,16 @@
fun err_dup_class c = error ("Duplicate declaration of class: " ^ quote c);
-fun err_cyclic_classes pp css =
+fun err_cyclic_classes ctxt css =
error (cat_lines (map (fn cs =>
- "Cycle in class relation: " ^ Pretty.string_of_classrel pp cs) css));
+ "Cycle in class relation: " ^ Syntax.string_of_classrel ctxt cs) css));
-fun add_class pp (c, cs) = map_classes (fn classes =>
+fun add_class ctxt (c, cs) = map_classes (fn classes =>
let
val classes' = classes |> Graph.new_node (c, serial ())
handle Graph.DUP dup => err_dup_class dup;
val classes'' = classes' |> fold Graph.add_edge_trans_acyclic (map (pair c) cs)
- handle Graph.CYCLES css => err_cyclic_classes pp css;
+ handle Graph.CYCLES css => err_cyclic_classes ctxt css;
in classes'' end);
@@ -216,15 +216,14 @@
local
fun for_classes _ NONE = ""
- | for_classes pp (SOME (c1, c2)) =
- " for classes " ^ Pretty.string_of_classrel pp [c1, c2];
+ | for_classes ctxt (SOME (c1, c2)) = " for classes " ^ Syntax.string_of_classrel ctxt [c1, c2];
-fun err_conflict pp t cc (c, Ss) (c', Ss') =
- error ("Conflict of type arities" ^ for_classes pp cc ^ ":\n " ^
- Pretty.string_of_arity pp (t, Ss, [c]) ^ " and\n " ^
- Pretty.string_of_arity pp (t, Ss', [c']));
+fun err_conflict ctxt t cc (c, Ss) (c', Ss') =
+ error ("Conflict of type arities" ^ for_classes ctxt cc ^ ":\n " ^
+ Syntax.string_of_arity ctxt (t, Ss, [c]) ^ " and\n " ^
+ Syntax.string_of_arity ctxt (t, Ss', [c']));
-fun coregular pp algebra t (c, Ss) ars =
+fun coregular ctxt algebra t (c, Ss) ars =
let
fun conflict (c', Ss') =
if class_le algebra (c, c') andalso not (sorts_le algebra (Ss, Ss')) then
@@ -234,62 +233,62 @@
else NONE;
in
(case get_first conflict ars of
- SOME ((c1, c2), (c', Ss')) => err_conflict pp t (SOME (c1, c2)) (c, Ss) (c', Ss')
+ SOME ((c1, c2), (c', Ss')) => err_conflict ctxt t (SOME (c1, c2)) (c, Ss) (c', Ss')
| NONE => (c, Ss) :: ars)
end;
fun complete algebra (c, Ss) = map (rpair Ss) (c :: super_classes algebra c);
-fun insert pp algebra t (c, Ss) ars =
+fun insert ctxt algebra t (c, Ss) ars =
(case AList.lookup (op =) ars c of
- NONE => coregular pp algebra t (c, Ss) ars
+ NONE => coregular ctxt algebra t (c, Ss) ars
| SOME Ss' =>
if sorts_le algebra (Ss, Ss') then ars
else if sorts_le algebra (Ss', Ss)
- then coregular pp algebra t (c, Ss) (remove (op =) (c, Ss') ars)
- else err_conflict pp t NONE (c, Ss) (c, Ss'));
+ then coregular ctxt algebra t (c, Ss) (remove (op =) (c, Ss') ars)
+ else err_conflict ctxt t NONE (c, Ss) (c, Ss'));
in
-fun insert_ars pp algebra t = fold_rev (insert pp algebra t);
+fun insert_ars ctxt algebra t = fold_rev (insert ctxt algebra t);
-fun insert_complete_ars pp algebra (t, ars) arities =
+fun insert_complete_ars ctxt algebra (t, ars) arities =
let val ars' =
Symtab.lookup_list arities t
- |> fold_rev (insert_ars pp algebra t) (map (complete algebra) ars);
+ |> fold_rev (insert_ars ctxt algebra t) (map (complete algebra) ars);
in Symtab.update (t, ars') arities end;
-fun add_arities pp arg algebra =
- algebra |> map_arities (insert_complete_ars pp algebra arg);
+fun add_arities ctxt arg algebra =
+ algebra |> map_arities (insert_complete_ars ctxt algebra arg);
-fun add_arities_table pp algebra =
- Symtab.fold (fn (t, ars) => insert_complete_ars pp algebra (t, ars));
+fun add_arities_table ctxt algebra =
+ Symtab.fold (fn (t, ars) => insert_complete_ars ctxt algebra (t, ars));
end;
(* classrel *)
-fun rebuild_arities pp algebra = algebra |> map_arities (fn arities =>
+fun rebuild_arities ctxt algebra = algebra |> map_arities (fn arities =>
Symtab.empty
- |> add_arities_table pp algebra arities);
+ |> add_arities_table ctxt algebra arities);
-fun add_classrel pp rel = rebuild_arities pp o map_classes (fn classes =>
+fun add_classrel ctxt rel = rebuild_arities ctxt o map_classes (fn classes =>
classes |> Graph.add_edge_trans_acyclic rel
- handle Graph.CYCLES css => err_cyclic_classes pp css);
+ handle Graph.CYCLES css => err_cyclic_classes ctxt css);
(* empty and merge *)
val empty_algebra = make_algebra (Graph.empty, Symtab.empty);
-fun merge_algebra pp
+fun merge_algebra ctxt
(Algebra {classes = classes1, arities = arities1},
Algebra {classes = classes2, arities = arities2}) =
let
val classes' = Graph.merge_trans_acyclic (op =) (classes1, classes2)
handle Graph.DUP c => err_dup_class c
- | Graph.CYCLES css => err_cyclic_classes pp css;
+ | Graph.CYCLES css => err_cyclic_classes ctxt css;
val algebra0 = make_algebra (classes', Symtab.empty);
val arities' =
(case (pointer_eq (classes1, classes2), pointer_eq (arities1, arities2)) of
@@ -297,20 +296,20 @@
| (true, false) => (*no completion*)
(arities1, arities2) |> Symtab.join (fn t => fn (ars1, ars2) =>
if pointer_eq (ars1, ars2) then raise Symtab.SAME
- else insert_ars pp algebra0 t ars2 ars1)
+ else insert_ars ctxt algebra0 t ars2 ars1)
| (false, true) => (*unary completion*)
Symtab.empty
- |> add_arities_table pp algebra0 arities1
+ |> add_arities_table ctxt algebra0 arities1
| (false, false) => (*binary completion*)
Symtab.empty
- |> add_arities_table pp algebra0 arities1
- |> add_arities_table pp algebra0 arities2);
+ |> add_arities_table ctxt algebra0 arities1
+ |> add_arities_table ctxt algebra0 arities2);
in make_algebra (classes', arities') end;
(* algebra projections *) (* FIXME potentially violates abstract type integrity *)
-fun subalgebra pp P sargs (algebra as Algebra {classes, arities}) =
+fun subalgebra ctxt P sargs (algebra as Algebra {classes, arities}) =
let
val restrict_sort = minimize_sort algebra o filter P o Graph.all_succs classes;
fun restrict_arity t (c, Ss) =
@@ -322,7 +321,7 @@
else NONE;
val classes' = classes |> Graph.subgraph P;
val arities' = arities |> Symtab.map (map_filter o restrict_arity);
- in (restrict_sort, rebuild_arities pp (make_algebra (classes', arities'))) end;
+ in (restrict_sort, rebuild_arities ctxt (make_algebra (classes', arities'))) end;
@@ -335,13 +334,13 @@
No_Arity of string * class |
No_Subsort of sort * sort;
-fun class_error pp (No_Classrel (c1, c2)) =
- "No class relation " ^ Pretty.string_of_classrel pp [c1, c2]
- | class_error pp (No_Arity (a, c)) =
- "No type arity " ^ Pretty.string_of_arity pp (a, [], [c])
- | class_error pp (No_Subsort (S1, S2)) =
- "Cannot derive subsort relation " ^ Pretty.string_of_sort pp S1
- ^ " < " ^ Pretty.string_of_sort pp S2;
+fun class_error ctxt (No_Classrel (c1, c2)) =
+ "No class relation " ^ Syntax.string_of_classrel ctxt [c1, c2]
+ | class_error ctxt (No_Arity (a, c)) =
+ "No type arity " ^ Syntax.string_of_arity ctxt (a, [], [c])
+ | class_error ctxt (No_Subsort (S1, S2)) =
+ "Cannot derive subsort relation " ^
+ Syntax.string_of_sort ctxt S1 ^ " < " ^ Syntax.string_of_sort ctxt S2;
exception CLASS_ERROR of class_error;
--- a/src/Pure/theory.ML Mon Apr 18 12:12:42 2011 +0200
+++ b/src/Pure/theory.ML Mon Apr 18 15:02:50 2011 +0200
@@ -95,11 +95,12 @@
fun merge pp (thy1, thy2) =
let
+ val ctxt = Syntax.init_pretty pp;
val Thy {axioms = _, defs = defs1, wrappers = (bgs1, ens1)} = thy1;
val Thy {axioms = _, defs = defs2, wrappers = (bgs2, ens2)} = thy2;
val axioms' = empty_axioms;
- val defs' = Defs.merge pp (defs1, defs2);
+ val defs' = Defs.merge ctxt (defs1, defs2);
val bgs' = Library.merge (eq_snd op =) (bgs1, bgs2);
val ens' = Library.merge (eq_snd op =) (ens1, ens2);
in make_thy (axioms', defs', (bgs', ens')) end;
@@ -137,7 +138,7 @@
fun begin_theory name imports =
let
- val thy = Context.begin_thy Syntax.pp_global name imports;
+ val thy = Context.begin_thy Context.pretty_global name imports;
val wrappers = begin_wrappers thy;
in
thy
@@ -196,7 +197,7 @@
else error ("Specification depends on extra type variables: " ^
commas_quote (map (Syntax.string_of_typ ctxt o TFree) rhs_extras) ^
"\nThe error(s) above occurred in " ^ quote description);
- in Defs.define (Syntax.pp ctxt) unchecked def description (prep lhs) (map prep rhs) end;
+ in Defs.define ctxt unchecked def description (prep lhs) (map prep rhs) end;
fun add_deps ctxt a raw_lhs raw_rhs thy =
let
@@ -239,9 +240,8 @@
local
-fun check_def ctxt unchecked overloaded (b, tm) defs =
+fun check_def ctxt thy unchecked overloaded (b, tm) defs =
let
- val thy = Proof_Context.theory_of ctxt;
val name = Sign.full_name thy b;
val ((lhs, rhs), _) = Primitive_Defs.dest_def ctxt Term.is_Const (K false) (K false) tm
handle TERM (msg, _) => error msg;
@@ -258,7 +258,7 @@
fun add_def ctxt unchecked overloaded raw_axm thy =
let val axm = cert_axm ctxt raw_axm in
thy
- |> map_defs (check_def ctxt unchecked overloaded axm)
+ |> map_defs (check_def ctxt thy unchecked overloaded axm)
|> add_axiom ctxt axm
end;
--- a/src/Pure/type.ML Mon Apr 18 12:12:42 2011 +0200
+++ b/src/Pure/type.ML Mon Apr 18 15:02:50 2011 +0200
@@ -11,7 +11,7 @@
val mark_polymorphic: typ -> typ
val constraint: typ -> term -> term
val strip_constraints: term -> term
- val appl_error: Pretty.pp -> term -> typ -> term -> typ -> string
+ val appl_error: Proof.context -> term -> typ -> term -> typ -> string
(*type signatures and certified types*)
datatype decl =
LogicalType of int |
@@ -55,7 +55,7 @@
val cert_typ_mode: mode -> tsig -> typ -> typ
val cert_typ: tsig -> typ -> typ
val arity_number: tsig -> string -> int
- val arity_sorts: Pretty.pp -> tsig -> string -> sort -> sort list
+ val arity_sorts: Context.pretty -> tsig -> string -> sort -> sort list
(*special treatment of type vars*)
val sort_of_atyp: typ -> sort
@@ -86,17 +86,16 @@
val eq_type: tyenv -> typ * typ -> bool
(*extend and merge type signatures*)
- val add_class: Proof.context -> Pretty.pp -> Name_Space.naming ->
- binding * class list -> tsig -> tsig
+ val add_class: Proof.context -> Name_Space.naming -> binding * class list -> tsig -> tsig
val hide_class: bool -> string -> tsig -> tsig
val set_defsort: sort -> tsig -> tsig
val add_type: Proof.context -> Name_Space.naming -> binding * int -> tsig -> tsig
val add_abbrev: Proof.context -> Name_Space.naming -> binding * string list * typ -> tsig -> tsig
val add_nonterminal: Proof.context -> Name_Space.naming -> binding -> tsig -> tsig
val hide_type: bool -> string -> tsig -> tsig
- val add_arity: Pretty.pp -> arity -> tsig -> tsig
- val add_classrel: Pretty.pp -> class * class -> tsig -> tsig
- val merge_tsig: Pretty.pp -> tsig * tsig -> tsig
+ val add_arity: Proof.context -> arity -> tsig -> tsig
+ val add_classrel: Proof.context -> class * class -> tsig -> tsig
+ val merge_tsig: Proof.context -> tsig * tsig -> tsig
end;
structure Type: TYPE =
@@ -116,15 +115,15 @@
| strip_constraints (Abs (x, T, t)) = Abs (x, T, strip_constraints t)
| strip_constraints a = a;
-fun appl_error pp (Const ("_type_constraint_", Type ("fun", [T, _]))) _ u U =
+fun appl_error ctxt (Const ("_type_constraint_", Type ("fun", [T, _]))) _ u U =
cat_lines
["Failed to meet type constraint:", "",
Pretty.string_of (Pretty.block
- [Pretty.str "Term:", Pretty.brk 2, Pretty.term pp u,
- Pretty.str " ::", Pretty.brk 1, Pretty.typ pp U]),
+ [Pretty.str "Term:", Pretty.brk 2, Syntax.pretty_term ctxt u,
+ Pretty.str " ::", Pretty.brk 1, Syntax.pretty_typ ctxt U]),
Pretty.string_of (Pretty.block
- [Pretty.str "Type:", Pretty.brk 2, Pretty.typ pp T])]
- | appl_error pp t T u U =
+ [Pretty.str "Type:", Pretty.brk 2, Syntax.pretty_typ ctxt T])]
+ | appl_error ctxt t T u U =
cat_lines
["Type error in application: " ^
(case T of
@@ -132,11 +131,11 @@
| _ => "operator not of function type"),
"",
Pretty.string_of (Pretty.block
- [Pretty.str "Operator:", Pretty.brk 2, Pretty.term pp t,
- Pretty.str " ::", Pretty.brk 1, Pretty.typ pp T]),
+ [Pretty.str "Operator:", Pretty.brk 2, Syntax.pretty_term ctxt t,
+ Pretty.str " ::", Pretty.brk 1, Syntax.pretty_typ ctxt T]),
Pretty.string_of (Pretty.block
- [Pretty.str "Operand:", Pretty.brk 3, Pretty.term pp u,
- Pretty.str " ::", Pretty.brk 1, Pretty.typ pp U])];
+ [Pretty.str "Operand:", Pretty.brk 3, Syntax.pretty_term ctxt u,
+ Pretty.str " ::", Pretty.brk 1, Syntax.pretty_typ ctxt U])];
@@ -310,7 +309,7 @@
fun arity_sorts _ tsig a [] = replicate (arity_number tsig a) []
| arity_sorts pp (TSig {classes, ...}) a S = Sorts.mg_domain (#2 classes) a S
- handle Sorts.CLASS_ERROR err => error (Sorts.class_error pp err);
+ handle Sorts.CLASS_ERROR err => error (Sorts.class_error (Syntax.init_pretty pp) err);
@@ -577,14 +576,14 @@
(* classes *)
-fun add_class ctxt pp naming (c, cs) tsig =
+fun add_class ctxt naming (c, cs) tsig =
tsig |> map_tsig (fn ((space, classes), default, types) =>
let
val cs' = map (cert_class tsig) cs
handle TYPE (msg, _, _) => error msg;
val _ = Binding.check c;
val (c', space') = space |> Name_Space.declare ctxt true naming c;
- val classes' = classes |> Sorts.add_class pp (c', cs');
+ val classes' = classes |> Sorts.add_class ctxt (c', cs');
in ((space', classes'), default, types) end);
fun hide_class fully c = map_tsig (fn ((space, classes), default, types) =>
@@ -593,7 +592,7 @@
(* arities *)
-fun add_arity pp (t, Ss, S) tsig = tsig |> map_tsig (fn ((space, classes), default, types) =>
+fun add_arity ctxt (t, Ss, S) tsig = tsig |> map_tsig (fn ((space, classes), default, types) =>
let
val _ =
(case lookup_type tsig t of
@@ -602,18 +601,18 @@
| NONE => error (undecl_type t));
val (Ss', S') = (map (cert_sort tsig) Ss, cert_sort tsig S)
handle TYPE (msg, _, _) => error msg;
- val classes' = classes |> Sorts.add_arities pp ((t, map (fn c' => (c', Ss')) S'));
+ val classes' = classes |> Sorts.add_arities ctxt ((t, map (fn c' => (c', Ss')) S'));
in ((space, classes'), default, types) end);
(* classrel *)
-fun add_classrel pp rel tsig =
+fun add_classrel ctxt rel tsig =
tsig |> map_tsig (fn ((space, classes), default, types) =>
let
val rel' = pairself (cert_class tsig) rel
handle TYPE (msg, _, _) => error msg;
- val classes' = classes |> Sorts.add_classrel pp rel';
+ val classes' = classes |> Sorts.add_classrel ctxt rel';
in ((space, classes'), default, types) end);
@@ -674,7 +673,7 @@
(* merge type signatures *)
-fun merge_tsig pp (tsig1, tsig2) =
+fun merge_tsig ctxt (tsig1, tsig2) =
let
val (TSig {classes = (space1, classes1), default = default1, types = types1,
log_types = _}) = tsig1;
@@ -682,7 +681,7 @@
log_types = _}) = tsig2;
val space' = Name_Space.merge (space1, space2);
- val classes' = Sorts.merge_algebra pp (classes1, classes2);
+ val classes' = Sorts.merge_algebra ctxt (classes1, classes2);
val default' = Sorts.inter_sort classes' (default1, default2);
val types' = Name_Space.merge_tables (types1, types2);
in build_tsig ((space', classes'), default', types') end;
--- a/src/Pure/type_infer.ML Mon Apr 18 12:12:42 2011 +0200
+++ b/src/Pure/type_infer.ML Mon Apr 18 15:02:50 2011 +0200
@@ -217,10 +217,10 @@
exception NO_UNIFIER of string * typ Vartab.table;
-fun unify ctxt pp =
+fun unify ctxt =
let
val thy = Proof_Context.theory_of ctxt;
- val arity_sorts = Type.arity_sorts pp (Sign.tsig_of thy);
+ val arity_sorts = Type.arity_sorts (Context.pretty ctxt) (Sign.tsig_of thy);
(* adjust sorts of parameters *)
@@ -289,9 +289,6 @@
fun infer ctxt =
let
- val pp = Syntax.pp ctxt;
-
-
(* errors *)
fun prep_output tye bs ts Ts =
@@ -310,7 +307,7 @@
fun err_appl msg tye bs t T u U =
let val ([t', u'], [T', U']) = prep_output tye bs [t, u] [T, U]
- in error (unif_failed msg ^ Type.appl_error pp t' T' u' U' ^ "\n") end;
+ in error (unif_failed msg ^ Type.appl_error ctxt t' T' u' U' ^ "\n") end;
(* main *)
@@ -328,7 +325,7 @@
val (T, tye_idx') = inf bs t tye_idx;
val (U, (tye, idx)) = inf bs u tye_idx';
val V = mk_param idx [];
- val tye_idx'' = unify ctxt pp (U --> V, T) (tye, idx + 1)
+ val tye_idx'' = unify ctxt (U --> V, T) (tye, idx + 1)
handle NO_UNIFIER (msg, tye') => err_appl msg tye' bs t T u U;
in (V, tye_idx'') end;
--- a/src/Tools/Code/code_preproc.ML Mon Apr 18 12:12:42 2011 +0200
+++ b/src/Tools/Code/code_preproc.ML Mon Apr 18 15:02:50 2011 +0200
@@ -431,8 +431,7 @@
|> fold (ensure_fun thy arities eqngr) cs
|> fold (ensure_rhs thy arities eqngr) cs_rhss;
val arities' = fold (add_arity thy vardeps) insts arities;
- val pp = Syntax.pp_global thy;
- val algebra = Sorts.subalgebra pp (is_proper_class thy)
+ val algebra = Sorts.subalgebra (Syntax.init_pretty_global thy) (is_proper_class thy)
(AList.lookup (op =) arities') (Sign.classes_of thy);
val (rhss, eqngr') = Symtab.fold (add_cert thy vardeps) eqntab ([], eqngr);
fun deps_of (c, rhs) = c :: maps (dicts_of thy algebra)
--- a/src/Tools/Code/code_thingol.ML Mon Apr 18 12:12:42 2011 +0200
+++ b/src/Tools/Code/code_thingol.ML Mon Apr 18 15:02:50 2011 +0200
@@ -574,18 +574,25 @@
fun translation_error thy permissive some_thm msg sub_msg =
if permissive
then raise PERMISSIVE ()
- else let
- val err_thm = case some_thm
- of SOME thm => "\n(in code equation " ^ Display.string_of_thm_global thy thm ^ ")"
- | NONE => "";
- in error (msg ^ err_thm ^ ":\n" ^ sub_msg) end;
+ else
+ let
+ val err_thm =
+ (case some_thm of
+ SOME thm => "\n(in code equation " ^ Display.string_of_thm_global thy thm ^ ")"
+ | NONE => "");
+ in error (msg ^ err_thm ^ ":\n" ^ sub_msg) end;
fun not_wellsorted thy permissive some_thm ty sort e =
let
- val err_class = Sorts.class_error (Syntax.pp_global thy) e;
- val err_typ = "Type " ^ Syntax.string_of_typ_global thy ty ^ " not of sort "
- ^ Syntax.string_of_sort_global thy sort;
- in translation_error thy permissive some_thm "Wellsortedness error" (err_typ ^ "\n" ^ err_class) end;
+ val ctxt = Syntax.init_pretty_global thy;
+ val err_class = Sorts.class_error ctxt e;
+ val err_typ =
+ "Type " ^ Syntax.string_of_typ ctxt ty ^ " not of sort " ^
+ Syntax.string_of_sort_global thy sort;
+ in
+ translation_error thy permissive some_thm "Wellsortedness error"
+ (err_typ ^ "\n" ^ err_class)
+ end;
(* translation *)
--- a/src/Tools/subtyping.ML Mon Apr 18 12:12:42 2011 +0200
+++ b/src/Tools/subtyping.ML Mon Apr 18 15:02:50 2011 +0200
@@ -98,8 +98,7 @@
fun unify weak ctxt =
let
val thy = Proof_Context.theory_of ctxt;
- val pp = Syntax.pp ctxt;
- val arity_sorts = Type.arity_sorts pp (Sign.tsig_of thy);
+ val arity_sorts = Type.arity_sorts (Context.pretty ctxt) (Sign.tsig_of thy);
(* adjust sorts of parameters *)
@@ -190,8 +189,8 @@
(** error messages **)
-fun gen_msg err msg =
- err () ^ "\nNow trying to infer coercions:\n\nCoercion inference failed" ^
+fun gen_msg err msg =
+ err () ^ "\nNow trying to infer coercions:\n\nCoercion inference failed" ^
(if msg = "" then "" else ": " ^ msg) ^ "\n";
fun prep_output ctxt tye bs ts Ts =
@@ -204,27 +203,26 @@
in (map prep ts', Ts') end;
fun err_loose i = error ("Loose bound variable: B." ^ string_of_int i);
-
+
fun unif_failed msg =
"Type unification failed" ^ (if msg = "" then "" else ": " ^ msg) ^ "\n\n";
-
+
fun err_appl_msg ctxt msg tye bs t T u U () =
let val ([t', u'], [T', U']) = prep_output ctxt tye bs [t, u] [T, U]
- in unif_failed msg ^ Type.appl_error (Syntax.pp ctxt) t' T' u' U' ^ "\n" end;
+ in unif_failed msg ^ Type.appl_error ctxt t' T' u' U' ^ "\n" end;
fun err_list ctxt msg tye Ts =
let
val (_, Ts') = prep_output ctxt tye [] [] Ts;
- val text = cat_lines ([msg,
- "Cannot unify a list of types that should be the same:",
- (Pretty.string_of (Pretty.list "[" "]" (map (Pretty.typ (Syntax.pp ctxt)) Ts')))]);
+ val text =
+ msg ^ "\n" ^ "Cannot unify a list of types that should be the same:" ^ "\n" ^
+ Pretty.string_of (Pretty.list "[" "]" (map (Syntax.pretty_typ ctxt) Ts'));
in
error text
end;
fun err_bound ctxt msg tye packs =
let
- val pp = Syntax.pp ctxt;
val (ts, Ts) = fold
(fn (bs, t $ u, U, _, U') => fn (ts, Ts) =>
let val (t', T') = prep_output ctxt tye bs [t, u] [U', U]
@@ -233,9 +231,10 @@
val text = cat_lines ([msg, "Cannot fulfil subtype constraints:"] @
(map2 (fn [t, u] => fn [T, U] => Pretty.string_of (
Pretty.block [
- Pretty.typ pp T, Pretty.brk 2, Pretty.str "<:", Pretty.brk 2, Pretty.typ pp U,
- Pretty.brk 3, Pretty.str "from function application", Pretty.brk 2,
- Pretty.block [Pretty.term pp (t $ u)]]))
+ Syntax.pretty_typ ctxt T, Pretty.brk 2, Pretty.str "<:", Pretty.brk 2,
+ Syntax.pretty_typ ctxt U, Pretty.brk 3,
+ Pretty.str "from function application", Pretty.brk 2,
+ Pretty.block [Syntax.pretty_term ctxt (t $ u)]]))
ts Ts))
in
error text
@@ -277,21 +276,20 @@
fun process_constraints ctxt err cs tye_idx =
let
+ val thy = Proof_Context.theory_of ctxt;
+
val coes_graph = coes_graph_of ctxt;
val tmaps = tmaps_of ctxt;
- val tsig = Sign.tsig_of (Proof_Context.theory_of ctxt);
- val pp = Syntax.pp ctxt;
- val arity_sorts = Type.arity_sorts pp tsig;
- val subsort = Type.subsort tsig;
+ val arity_sorts = Type.arity_sorts (Context.pretty ctxt) (Sign.tsig_of thy);
fun split_cs _ [] = ([], [])
| split_cs f (c :: cs) =
(case pairself f (fst c) of
(false, false) => apsnd (cons c) (split_cs f cs)
| _ => apfst (cons c) (split_cs f cs));
-
+
fun unify_list (T :: Ts) tye_idx =
- fold (fn U => fn tye_idx' => strong_unify ctxt (T, U) tye_idx') Ts tye_idx;
+ fold (fn U => fn tye_idx' => strong_unify ctxt (T, U) tye_idx') Ts tye_idx;
(* check whether constraint simplification will terminate using weak unification *)
@@ -317,12 +315,12 @@
COVARIANT => (constraint :: cs, tye_idx)
| CONTRAVARIANT => (swap constraint :: cs, tye_idx)
| INVARIANT_TO T => (cs, unify_list [T, fst constraint, snd constraint] tye_idx
- handle NO_UNIFIER (msg, _) =>
- err_list ctxt (gen_msg err
- "failed to unify invariant arguments w.r.t. to the known map function")
+ handle NO_UNIFIER (msg, _) =>
+ err_list ctxt (gen_msg err
+ "failed to unify invariant arguments w.r.t. to the known map function")
(fst tye_idx) Ts)
| INVARIANT => (cs, strong_unify ctxt constraint tye_idx
- handle NO_UNIFIER (msg, _) =>
+ handle NO_UNIFIER (msg, _) =>
error (gen_msg err ("failed to unify invariant arguments" ^ msg))));
val (new, (tye', idx')) = apfst (fn cs => (cs ~~ replicate (length cs) error_pack))
(fold new_constraints (arg_var ~~ (Ts ~~ Us)) ([], (tye, idx)));
@@ -359,7 +357,7 @@
val (ch, done') = split_cs (test_update o Type_Infer.deref tye') done;
val todo' = ch @ todo;
in
- if subsort (S', S) (*TODO check this*)
+ if Sign.subsort thy (S', S) (*TODO check this*)
then simplify done' todo' (tye', idx)
else error (gen_msg err "sort mismatch")
end
@@ -394,11 +392,11 @@
(* do simplification *)
val (cs', tye_idx') = simplify_constraints cs tye_idx;
-
- fun find_error_pack lower T' = map_filter
+
+ fun find_error_pack lower T' = map_filter
(fn ((T, U), pack) => if if lower then T' = U else T' = T then SOME pack else NONE) cs';
-
- fun find_cycle_packs nodes =
+
+ fun find_cycle_packs nodes =
let
val (but_last, last) = split_last nodes
val pairs = (last, hd nodes) :: (but_last ~~ tl nodes);
@@ -431,7 +429,7 @@
fun adjust T U = if super then (T, U) else (U, T);
fun styp_test U Ts = forall
(fn T => T = U orelse Graph.is_edge coes_graph (adjust U T)) Ts;
- fun fitting Ts S U = Type.of_sort tsig (t_of U, S) andalso styp_test U Ts
+ fun fitting Ts S U = Sign.of_sort thy (t_of U, S) andalso styp_test U Ts
in
forall (fn (Ts, S) => exists (fitting Ts S) (T :: styps super T)) styps_and_sorts
end;
@@ -448,7 +446,7 @@
*)
fun tightest sup S styps_and_sorts (T :: Ts) =
let
- fun restriction T = Type.of_sort tsig (t_of T, S)
+ fun restriction T = Sign.of_sort thy (t_of T, S)
andalso ex_styp_of_sort (not sup) T styps_and_sorts;
fun candidates T = inter (op =) (filter restriction (T :: styps sup T));
in
@@ -467,11 +465,11 @@
val (G'', tye_idx') = (add_edge (T, U) G', tye_idx)
handle Typ_Graph.CYCLES cycles =>
let
- val (tye, idx) =
- fold
+ val (tye, idx) =
+ fold
(fn cycle => fn tye_idx' => (unify_list cycle tye_idx'
- handle NO_UNIFIER (msg, _) =>
- err_bound ctxt
+ handle NO_UNIFIER (msg, _) =>
+ err_bound ctxt
(gen_msg err ("constraint cycle not unifiable" ^ msg)) (fst tye_idx)
(find_cycle_packs cycle)))
cycles tye_idx
@@ -495,13 +493,13 @@
in
if not (is_typeT T) orelse not (is_typeT U) orelse T = U
then if super then (hd nodes, T') else (T', hd nodes)
- else
- if super andalso
+ else
+ if super andalso
Graph.is_edge coes_graph (nameT T, nameT U) then (hd nodes, T')
- else if not super andalso
+ else if not super andalso
Graph.is_edge coes_graph (nameT U, nameT T) then (T', hd nodes)
else err_bound ctxt (gen_msg err "cycle elimination produces inconsistent graph")
- (fst tye_idx)
+ (fst tye_idx)
(maps find_cycle_packs cycles @ find_error_pack super T')
end;
in
@@ -528,7 +526,7 @@
val assignment =
if null bound orelse null not_params then NONE
else SOME (tightest lower S styps_and_sorts (map nameT not_params)
- handle BOUND_ERROR msg =>
+ handle BOUND_ERROR msg =>
err_bound ctxt (gen_msg err msg) tye (find_error_pack lower key))
in
(case assignment of
@@ -560,7 +558,7 @@
val (tye_idx' as (tye, _)) = fold (assign_lb G) ts tye_idx
|> fold (assign_ub G) ts;
in
- assign_alternating ts
+ assign_alternating ts
(filter (Type_Infer.is_paramT o Type_Infer.deref tye) ts) G tye_idx'
end;
@@ -573,7 +571,7 @@
filter (Type_Infer.is_paramT o Type_Infer.deref tye) (Typ_Graph.maximals G);
val to_unify = map (fn T => T :: get_preds G T) max_params;
in
- fold
+ fold
(fn Ts => fn tye_idx' => unify_list Ts tye_idx'
handle NO_UNIFIER (msg, _) => err_list ctxt (gen_msg err msg) (fst tye_idx) Ts)
to_unify tye_idx
@@ -686,24 +684,24 @@
val (u', U, (tye, idx)) = inf bs u tye_idx';
val V = Type_Infer.mk_param idx [];
val (tu, tye_idx'') = (t' $ u', strong_unify ctxt (U --> V, T) (tye, idx + 1))
- handle NO_UNIFIER (msg, tye') =>
+ handle NO_UNIFIER (msg, tye') =>
raise TYPE_INFERENCE_ERROR (err_appl_msg ctxt msg tye' bs t T u U);
in (tu, V, tye_idx'') end;
- fun infer_single t tye_idx =
+ fun infer_single t tye_idx =
let val (t, _, tye_idx') = inf [] t tye_idx;
in (t, tye_idx') end;
-
+
val (ts', (tye, _)) = (fold_map infer_single ts (Vartab.empty, idx)
- handle TYPE_INFERENCE_ERROR err =>
+ handle TYPE_INFERENCE_ERROR err =>
let
fun gen_single t (tye_idx, constraints) =
let val (_, tye_idx', constraints') = generate_constraints ctxt err t tye_idx
in (tye_idx', constraints' @ constraints) end;
-
+
val (tye_idx, constraints) = fold gen_single ts ((Vartab.empty, idx), []);
val (tye, idx) = process_constraints ctxt err constraints tye_idx;
- in
+ in
(insert_coercions ctxt tye ts, (tye, idx))
end);
@@ -739,15 +737,15 @@
val ctxt = Context.proof_of context;
val t = singleton (Variable.polymorphic ctxt) raw_t;
- fun err_str t = "\n\nThe provided function has the type\n" ^
- Syntax.string_of_typ ctxt (fastype_of t) ^
+ fun err_str t = "\n\nThe provided function has the type\n" ^
+ Syntax.string_of_typ ctxt (fastype_of t) ^
"\n\nThe general type signature of a map function is" ^
"\nf1 => f2 => ... => fn => C [x1, ..., xn] => C [y1, ..., yn]" ^
"\nwhere C is a constructor and fi is of type (xi => yi) or (yi => xi)";
-
+
val ((fis, T1), T2) = apfst split_last (strip_type (fastype_of t))
handle Empty => error ("Not a proper map function:" ^ err_str t);
-
+
fun gen_arg_var ([], []) = []
| gen_arg_var ((T, T') :: Ts, (U, U') :: Us) =
if U = U' then
@@ -756,8 +754,8 @@
else if T = U andalso T' = U' then COVARIANT :: gen_arg_var (Ts, Us)
else if T = U' andalso T' = U then CONTRAVARIANT :: gen_arg_var (Ts, Us)
else error ("Functions do not apply to arguments correctly:" ^ err_str t)
- | gen_arg_var (_, Ts) =
- if forall (op = andf is_stypeT o fst) Ts
+ | gen_arg_var (_, Ts) =
+ if forall (op = andf is_stypeT o fst) Ts
then map (INVARIANT_TO o fst) Ts
else error ("Different numbers of functions and variant arguments\n" ^ err_str t);