# HG changeset patch # User wenzelm # Date 1303125999 -7200 # Node ID b1965c8992c84c80eb2efbb269046352842ae78c # Parent 50ea65e84d98fe4737455c96872b4515bcb7b06e pass plain Proof.context for pretty printing; diff -r 50ea65e84d98 -r b1965c8992c8 src/Pure/Isar/class.ML --- a/src/Pure/Isar/class.ML Mon Apr 18 12:11:58 2011 +0200 +++ b/src/Pure/Isar/class.ML Mon Apr 18 13:26:39 2011 +0200 @@ -530,7 +530,7 @@ 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 (Context.pretty_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 =) diff -r 50ea65e84d98 -r b1965c8992c8 src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Mon Apr 18 12:11:58 2011 +0200 +++ b/src/Pure/Isar/proof_context.ML Mon Apr 18 13:26:39 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 (Context.pretty 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 (Context.pretty ctxt) arity (tsig_of ctxt); arity end; + in Type.add_arity ctxt arity (tsig_of ctxt); arity end; in diff -r 50ea65e84d98 -r b1965c8992c8 src/Pure/sign.ML --- a/src/Pure/sign.ML Mon Apr 18 12:11:58 2011 +0200 +++ b/src/Pure/sign.ML Mon Apr 18 13:26:39 2011 +0200 @@ -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; ); @@ -455,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 (Context.pretty 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 (Context.pretty_global thy) arg); -fun primitive_arity arg thy = thy |> map_tsig (Type.add_arity (Context.pretty_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 *) diff -r 50ea65e84d98 -r b1965c8992c8 src/Pure/sorts.ML --- a/src/Pure/sorts.ML Mon Apr 18 12:11:58 2011 +0200 +++ b/src/Pure/sorts.ML Mon Apr 18 13:26:39 2011 +0200 @@ -40,12 +40,12 @@ 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: Context.pretty -> class * class list -> algebra -> algebra - val add_classrel: Context.pretty -> class * class -> algebra -> algebra - val add_arities: Context.pretty -> 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: Context.pretty -> algebra * algebra -> algebra - val subalgebra: Context.pretty -> (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: Proof.context -> class_error -> string @@ -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: " ^ Syntax.string_of_classrel (Syntax.init_pretty 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 " ^ Syntax.string_of_classrel (Syntax.init_pretty 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 " ^ - Syntax.string_of_arity (Syntax.init_pretty pp) (t, Ss, [c]) ^ " and\n " ^ - Syntax.string_of_arity (Syntax.init_pretty 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; diff -r 50ea65e84d98 -r b1965c8992c8 src/Pure/type.ML --- a/src/Pure/type.ML Mon Apr 18 12:11:58 2011 +0200 +++ b/src/Pure/type.ML Mon Apr 18 13:26:39 2011 +0200 @@ -86,17 +86,16 @@ val eq_type: tyenv -> typ * typ -> bool (*extend and merge type signatures*) - val add_class: Proof.context -> Context.pretty -> 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: Context.pretty -> arity -> tsig -> tsig - val add_classrel: Context.pretty -> class * class -> tsig -> tsig - val merge_tsig: Context.pretty -> 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 = @@ -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; diff -r 50ea65e84d98 -r b1965c8992c8 src/Tools/Code/code_preproc.ML --- a/src/Tools/Code/code_preproc.ML Mon Apr 18 12:11:58 2011 +0200 +++ b/src/Tools/Code/code_preproc.ML Mon Apr 18 13:26:39 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 = Context.pretty_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)