Local theory operations, with optional target locale.
authorwenzelm
Sun Jan 22 18:46:01 2006 +0100 (2006-01-22 ago)
changeset 18744a9a5ee0e43e2
parent 18743 7ff2934480c9
child 18745 060400dc077c
Local theory operations, with optional target locale.
src/Pure/Isar/local_theory.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/Isar/local_theory.ML	Sun Jan 22 18:46:01 2006 +0100
     1.3 @@ -0,0 +1,83 @@
     1.4 +(*  Title:      Pure/Isar/local_theory.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Makarius
     1.7 +
     1.8 +Local theory operations, with optional target locale.
     1.9 +*)
    1.10 +
    1.11 +signature LOCAL_THEORY =
    1.12 +sig
    1.13 +  val map_theory: (theory -> theory) -> Proof.context -> Proof.context
    1.14 +  val map_theory_result: (theory -> 'a * theory) -> Proof.context -> 'a * Proof.context
    1.15 +  val init: string option -> theory -> Proof.context
    1.16 +  val exit: Proof.context -> theory
    1.17 +  val params_of: Proof.context -> (string * typ) list
    1.18 +  val consts: (string * typ * mixfix) list -> Proof.context ->
    1.19 +    ((string * typ) list * term list) * Proof.context
    1.20 +end;
    1.21 +
    1.22 +structure LocalTheory: LOCAL_THEORY =
    1.23 +struct
    1.24 +
    1.25 +(* local context data *)
    1.26 +
    1.27 +structure Data = ProofDataFun
    1.28 +(
    1.29 +  val name = "Isar/local_theory";
    1.30 +  type T =
    1.31 +   {locale: string option,
    1.32 +    params: (string * typ) list,
    1.33 +    hyps: term list,
    1.34 +    exit: theory -> theory};
    1.35 +  fun init _ = {locale = NONE, params = [], hyps = [], exit = I};
    1.36 +  fun print _ _ = ();
    1.37 +);
    1.38 +
    1.39 +val _ = Context.add_setup Data.init;
    1.40 +
    1.41 +
    1.42 +(* theory *)
    1.43 +
    1.44 +fun map_theory f ctxt =
    1.45 +  ProofContext.transfer (f (ProofContext.theory_of ctxt)) ctxt;
    1.46 +
    1.47 +fun map_theory_result f ctxt =
    1.48 +  let val (res, thy') = f (ProofContext.theory_of ctxt)
    1.49 +  in (res, ProofContext.transfer thy' ctxt) end;
    1.50 +
    1.51 +fun init NONE thy = ProofContext.init thy
    1.52 +  | init (SOME loc) thy =
    1.53 +      thy
    1.54 +      |> Locale.init loc
    1.55 +      |> (fn ctxt => Data.put
    1.56 +          {locale = SOME loc,
    1.57 +           params = Locale.the_params thy loc,
    1.58 +           hyps = ProofContext.assms_of ctxt,   (* FIXME query locale!! *)
    1.59 +           exit = Sign.restore_naming thy} ctxt)
    1.60 +      |> map_theory (Sign.add_path loc #> Sign.no_base_names);
    1.61 +
    1.62 +fun exit ctxt = #exit (Data.get ctxt) (ProofContext.theory_of ctxt);
    1.63 +
    1.64 +
    1.65 +(* local theory *)
    1.66 +
    1.67 +val params_of = #params o Data.get;
    1.68 +
    1.69 +fun consts decls ctxt =
    1.70 +  let
    1.71 +    val thy = ProofContext.theory_of ctxt;
    1.72 +    val params = params_of ctxt;
    1.73 +    val ps = map Free params;
    1.74 +    val Us = map snd params;
    1.75 +
    1.76 +    val xs = decls |> map (fn (c, _, mx) => Syntax.const_name c mx);
    1.77 +    val Ts = map #2 decls;
    1.78 +    fun const x T = Term.list_comb (Const (Sign.full_name thy x, Us ---> T), ps);
    1.79 +  in
    1.80 +    ctxt
    1.81 +    |> map_theory (Sign.add_consts_i (decls |> map (fn (c, T, mx) => (c, Us ---> T, mx))))
    1.82 +    |> ProofContext.add_fixes_i (decls |> map (fn (c, T, mx) => (c, SOME T, mx)))
    1.83 +    |-> (fn xs' => pair ((xs' ~~ Ts), map2 const xs Ts))
    1.84 +  end;
    1.85 +
    1.86 +end;