pass plain Proof.context for pretty printing;
authorwenzelm
Mon Apr 18 11:44:39 2011 +0200 (2011-04-18 ago)
changeset 423846b8e28b52ae3
parent 42383 0ae4ad40d7b5
child 42385 b46b47775cbe
pass plain Proof.context for pretty printing;
src/Pure/defs.ML
src/Pure/display.ML
src/Pure/theory.ML
     1.1 --- a/src/Pure/defs.ML	Mon Apr 18 11:13:29 2011 +0200
     1.2 +++ b/src/Pure/defs.ML	Mon Apr 18 11:44:39 2011 +0200
     1.3 @@ -7,7 +7,7 @@
     1.4  
     1.5  signature DEFS =
     1.6  sig
     1.7 -  val pretty_const: Context.pretty -> string * typ list -> Pretty.T
     1.8 +  val pretty_const: Proof.context -> string * typ list -> Pretty.T
     1.9    val plain_args: typ list -> bool
    1.10    type T
    1.11    type spec =
    1.12 @@ -19,7 +19,7 @@
    1.13      reducts: ((string * typ list) * (string * typ list) list) list}
    1.14    val empty: T
    1.15    val merge: Context.pretty -> T * T -> T
    1.16 -  val define: Context.pretty -> bool -> string option -> string ->
    1.17 +  val define: Proof.context -> bool -> string option -> string ->
    1.18      string * typ list -> (string * typ list) list -> T -> T
    1.19  end
    1.20  
    1.21 @@ -30,13 +30,11 @@
    1.22  
    1.23  type args = typ list;
    1.24  
    1.25 -fun pretty_const pp (c, args) =
    1.26 +fun pretty_const ctxt (c, args) =
    1.27    let
    1.28      val prt_args =
    1.29        if null args then []
    1.30 -      else
    1.31 -        [Pretty.list "(" ")"
    1.32 -          (map (Syntax.pretty_typ (Syntax.init_pretty pp) o Logic.unvarifyT_global) args)];
    1.33 +      else [Pretty.list "(" ")" (map (Syntax.pretty_typ ctxt o Logic.unvarifyT_global) args)];
    1.34    in Pretty.block (Pretty.str c :: prt_args) end;
    1.35  
    1.36  fun plain_args args =
    1.37 @@ -120,27 +118,27 @@
    1.38  local
    1.39  
    1.40  val prt = Pretty.string_of oo pretty_const;
    1.41 -fun err pp (c, args) (d, Us) s1 s2 =
    1.42 -  error (s1 ^ " dependency of constant " ^ prt pp (c, args) ^ " -> " ^ prt pp (d, Us) ^ s2);
    1.43 +fun err ctxt (c, args) (d, Us) s1 s2 =
    1.44 +  error (s1 ^ " dependency of constant " ^ prt ctxt (c, args) ^ " -> " ^ prt ctxt (d, Us) ^ s2);
    1.45  
    1.46  fun contained (U as TVar _) (Type (_, Ts)) = exists (fn T => T = U orelse contained U T) Ts
    1.47    | contained _ _ = false;
    1.48  
    1.49 -fun acyclic pp (c, args) (d, Us) =
    1.50 +fun acyclic ctxt (c, args) (d, Us) =
    1.51    c <> d orelse
    1.52    exists (fn U => exists (contained U) args) Us orelse
    1.53    is_none (match_args (args, Us)) orelse
    1.54 -  err pp (c, args) (d, Us) "Circular" "";
    1.55 +  err ctxt (c, args) (d, Us) "Circular" "";
    1.56  
    1.57 -fun wellformed pp defs (c, args) (d, Us) =
    1.58 +fun wellformed ctxt defs (c, args) (d, Us) =
    1.59    forall is_TVar Us orelse
    1.60    (case find_first (fn (Ts, _) => not (disjoint_args (Ts, Us))) (restricts_of defs d) of
    1.61      SOME (Ts, description) =>
    1.62 -      err pp (c, args) (d, Us) "Malformed"
    1.63 -        ("\n(restriction " ^ prt pp (d, Ts) ^ " from " ^ quote description ^ ")")
    1.64 +      err ctxt (c, args) (d, Us) "Malformed"
    1.65 +        ("\n(restriction " ^ prt ctxt (d, Ts) ^ " from " ^ quote description ^ ")")
    1.66    | NONE => true);
    1.67  
    1.68 -fun reduction pp defs const deps =
    1.69 +fun reduction ctxt defs const deps =
    1.70    let
    1.71      fun reduct Us (Ts, rhs) =
    1.72        (case match_args (Ts, Us) of
    1.73 @@ -153,17 +151,17 @@
    1.74        if forall (is_none o #1) reds then NONE
    1.75        else SOME (fold_rev
    1.76          (fn (NONE, dp) => insert (op =) dp | (SOME dps, _) => fold (insert (op =)) dps) reds []);
    1.77 -    val _ = forall (acyclic pp const) (the_default deps deps');
    1.78 +    val _ = forall (acyclic ctxt const) (the_default deps deps');
    1.79    in deps' end;
    1.80  
    1.81  in
    1.82  
    1.83 -fun normalize pp =
    1.84 +fun normalize ctxt =
    1.85    let
    1.86      fun norm_update (c, {reducts, ...}: def) (changed, defs) =
    1.87        let
    1.88          val reducts' = reducts |> map (fn (args, deps) =>
    1.89 -          (args, perhaps (reduction pp defs (c, args)) deps));
    1.90 +          (args, perhaps (reduction ctxt defs (c, args)) deps));
    1.91        in
    1.92          if reducts = reducts' then (changed, defs)
    1.93          else (true, defs |> map_def c (fn (specs, restricts, _) => (specs, restricts, reducts')))
    1.94 @@ -173,16 +171,16 @@
    1.95          (true, defs') => norm_all defs'
    1.96        | (false, _) => defs);
    1.97      fun check defs (c, {reducts, ...}: def) =
    1.98 -      reducts |> forall (fn (args, deps) => forall (wellformed pp defs (c, args)) deps);
    1.99 +      reducts |> forall (fn (args, deps) => forall (wellformed ctxt defs (c, args)) deps);
   1.100    in norm_all #> (fn defs => tap (Symtab.forall (check defs)) defs) end;
   1.101  
   1.102 -fun dependencies pp (c, args) restr deps =
   1.103 +fun dependencies ctxt (c, args) restr deps =
   1.104    map_def c (fn (specs, restricts, reducts) =>
   1.105      let
   1.106        val restricts' = Library.merge (op =) (restricts, restr);
   1.107        val reducts' = insert (op =) (args, deps) reducts;
   1.108      in (specs, restricts', reducts') end)
   1.109 -  #> normalize pp;
   1.110 +  #> normalize ctxt;
   1.111  
   1.112  end;
   1.113  
   1.114 @@ -191,20 +189,21 @@
   1.115  
   1.116  fun merge pp (Defs defs1, Defs defs2) =
   1.117    let
   1.118 +    val ctxt = Syntax.init_pretty pp;
   1.119      fun add_deps (c, args) restr deps defs =
   1.120        if AList.defined (op =) (reducts_of defs c) args then defs
   1.121 -      else dependencies pp (c, args) restr deps defs;
   1.122 +      else dependencies ctxt (c, args) restr deps defs;
   1.123      fun add_def (c, {restricts, reducts, ...}: def) =
   1.124        fold (fn (args, deps) => add_deps (c, args) restricts deps) reducts;
   1.125    in
   1.126      Defs (Symtab.join join_specs (defs1, defs2)
   1.127 -      |> normalize pp |> Symtab.fold add_def defs2)
   1.128 +      |> normalize ctxt |> Symtab.fold add_def defs2)
   1.129    end;
   1.130  
   1.131  
   1.132  (* define *)
   1.133  
   1.134 -fun define pp unchecked def description (c, args) deps (Defs defs) =
   1.135 +fun define ctxt unchecked def description (c, args) deps (Defs defs) =
   1.136    let
   1.137      val restr =
   1.138        if plain_args args orelse
   1.139 @@ -213,6 +212,6 @@
   1.140      val spec =
   1.141        (serial (), {def = def, description = description, lhs = args, rhs = deps});
   1.142      val defs' = defs |> update_specs c spec;
   1.143 -  in Defs (defs' |> (if unchecked then I else dependencies pp (c, args) restr deps)) end;
   1.144 +  in Defs (defs' |> (if unchecked then I else dependencies ctxt (c, args) restr deps)) end;
   1.145  
   1.146  end;
     2.1 --- a/src/Pure/display.ML	Mon Apr 18 11:13:29 2011 +0200
     2.2 +++ b/src/Pure/display.ML	Mon Apr 18 11:44:39 2011 +0200
     2.3 @@ -143,7 +143,7 @@
     2.4      fun prt_term t = Pretty.quote (Syntax.pretty_term ctxt t);
     2.5      val prt_term_no_vars = prt_term o Logic.unvarify_global;
     2.6      fun prt_const (c, ty) = [Pretty.str c, Pretty.str " ::", Pretty.brk 1, prt_typ_no_tvars ty];
     2.7 -    val prt_const' = Defs.pretty_const (Context.pretty ctxt);
     2.8 +    val prt_const' = Defs.pretty_const ctxt;
     2.9  
    2.10      fun pretty_classrel (c, []) = prt_cls c
    2.11        | pretty_classrel (c, cs) = Pretty.block
     3.1 --- a/src/Pure/theory.ML	Mon Apr 18 11:13:29 2011 +0200
     3.2 +++ b/src/Pure/theory.ML	Mon Apr 18 11:44:39 2011 +0200
     3.3 @@ -196,7 +196,7 @@
     3.4        else error ("Specification depends on extra type variables: " ^
     3.5          commas_quote (map (Syntax.string_of_typ ctxt o TFree) rhs_extras) ^
     3.6          "\nThe error(s) above occurred in " ^ quote description);
     3.7 -  in Defs.define (Context.pretty ctxt) unchecked def description (prep lhs) (map prep rhs) end;
     3.8 +  in Defs.define ctxt unchecked def description (prep lhs) (map prep rhs) end;
     3.9  
    3.10  fun add_deps ctxt a raw_lhs raw_rhs thy =
    3.11    let