src/Pure/context.ML
changeset 18632 3149c6abe876
parent 17756 d4a35f82fbb4
child 18665 5198a2c4c00e
     1.1 --- a/src/Pure/context.ML	Tue Jan 10 19:33:30 2006 +0100
     1.2 +++ b/src/Pure/context.ML	Tue Jan 10 19:33:31 2006 +0100
     1.3 @@ -72,9 +72,12 @@
     1.4    val init_proof: theory -> proof
     1.5    val proof_data_of: theory -> string list
     1.6    (*generic context*)
     1.7 -  datatype context = Theory of theory | Proof of proof
     1.8 -  val theory_of: context -> theory
     1.9 -  val proof_of: context -> proof
    1.10 +  datatype generic = Theory of theory | Proof of proof
    1.11 +  val cases: (theory -> 'a) -> (proof -> 'a) -> generic -> 'a
    1.12 +  val the_theory: generic -> theory
    1.13 +  val the_proof: generic -> proof
    1.14 +  val theory_of: generic -> theory
    1.15 +  val proof_of: generic -> proof
    1.16  end;
    1.17  
    1.18  signature PRIVATE_CONTEXT =
    1.19 @@ -565,15 +568,19 @@
    1.20  end;
    1.21  
    1.22  
    1.23 +
    1.24  (*** generic context ***)
    1.25  
    1.26 -datatype context = Theory of theory | Proof of proof;
    1.27 +datatype generic = Theory of theory | Proof of proof;
    1.28 +
    1.29 +fun cases f _ (Theory thy) = f thy
    1.30 +  | cases _ g (Proof prf) = g prf;
    1.31  
    1.32 -fun theory_of (Theory thy) = thy
    1.33 -  | theory_of (Proof prf) = theory_of_proof prf;
    1.34 +val the_theory = cases I (fn _ => raise Fail "Bad generic context: theory expected");
    1.35 +val the_proof = cases (fn _ => raise Fail "Bad generic context: proof context expected") I;
    1.36  
    1.37 -fun proof_of (Theory thy) = init_proof thy
    1.38 -  | proof_of (Proof prf) = prf;
    1.39 +val theory_of = cases I theory_of_proof;
    1.40 +val proof_of = cases init_proof I;
    1.41  
    1.42  end;
    1.43  
    1.44 @@ -671,5 +678,52 @@
    1.45  
    1.46  end;
    1.47  
    1.48 +
    1.49 +
    1.50 +(** generic data **)
    1.51 +
    1.52 +signature GENERIC_DATA_ARGS =
    1.53 +sig
    1.54 +  val name: string
    1.55 +  type T
    1.56 +  val empty: T
    1.57 +  val extend: T -> T
    1.58 +  val merge: Pretty.pp -> T * T -> T
    1.59 +  val print: Context.generic -> T -> unit
    1.60 +end;
    1.61 +
    1.62 +signature GENERIC_DATA =
    1.63 +sig
    1.64 +  type T
    1.65 +  val init: theory -> theory
    1.66 +  val get: Context.generic -> T
    1.67 +  val put: T -> Context.generic -> Context.generic
    1.68 +  val map: (T -> T) -> Context.generic -> Context.generic
    1.69 +  val print: Context.generic -> unit
    1.70 +end;
    1.71 +
    1.72 +functor GenericDataFun(Data: GENERIC_DATA_ARGS): GENERIC_DATA =
    1.73 +struct
    1.74 +
    1.75 +structure ThyData = TheoryDataFun(open Data val copy = I fun print _ _ = ());
    1.76 +structure PrfData =
    1.77 +  ProofDataFun(val name = Data.name type T = Data.T val init = ThyData.get fun print _ _ = ());
    1.78 +
    1.79 +type T = Data.T;
    1.80 +val init = ThyData.init #> PrfData.init;
    1.81 +
    1.82 +fun get (Context.Theory thy) = ThyData.get thy
    1.83 +  | get (Context.Proof prf) = PrfData.get prf;
    1.84 +
    1.85 +fun put x (Context.Theory thy) = Context.Theory (ThyData.put x thy)
    1.86 +  | put x (Context.Proof prf) = Context.Proof (PrfData.put x prf);
    1.87 +
    1.88 +fun map f ctxt = put (f (get ctxt)) ctxt;
    1.89 +
    1.90 +fun print ctxt = Data.print ctxt (get ctxt);
    1.91 +
    1.92 +end;
    1.93 +
    1.94 +
    1.95  (*hide private interface*)
    1.96  structure Context: CONTEXT = Context;