src/Pure/Isar/local_theory.ML

Local theory operations, with optional target locale.

(*  Title:      Pure/Isar/local_theory.ML
    ID:         $Id$
    Author:     Makarius

Local theory operations, with optional target locale.
*)

signature LOCAL_THEORY =
sig
  val map_theory: (theory -> theory) -> Proof.context -> Proof.context
  val map_theory_result: (theory -> 'a * theory) -> Proof.context -> 'a * Proof.context
  val init: string option -> theory -> Proof.context
  val exit: Proof.context -> theory
  val params_of: Proof.context -> (string * typ) list
  val consts: (string * typ * mixfix) list -> Proof.context ->
    ((string * typ) list * term list) * Proof.context
end;

structure LocalTheory: LOCAL_THEORY =
struct

(* local context data *)

structure Data = ProofDataFun
(
  val name = "Isar/local_theory";
  type T =
   {locale: string option,
    params: (string * typ) list,
    hyps: term list,
    exit: theory -> theory};
  fun init _ = {locale = NONE, params = [], hyps = [], exit = I};
  fun print _ _ = ();
);

val _ = Context.add_setup Data.init;


(* theory *)

fun map_theory f ctxt =
  ProofContext.transfer (f (ProofContext.theory_of ctxt)) ctxt;

fun map_theory_result f ctxt =
  let val (res, thy') = f (ProofContext.theory_of ctxt)
  in (res, ProofContext.transfer thy' ctxt) end;

fun init NONE thy = ProofContext.init thy
  | init (SOME loc) thy =
      thy
      |> Locale.init loc
      |> (fn ctxt => Data.put
          {locale = SOME loc,
           params = Locale.the_params thy loc,
           hyps = ProofContext.assms_of ctxt,   (* FIXME query locale!! *)
           exit = Sign.restore_naming thy} ctxt)
      |> map_theory (Sign.add_path loc #> Sign.no_base_names);

fun exit ctxt = #exit (Data.get ctxt) (ProofContext.theory_of ctxt);


(* local theory *)

val params_of = #params o Data.get;

fun consts decls ctxt =
  let
    val thy = ProofContext.theory_of ctxt;
    val params = params_of ctxt;
    val ps = map Free params;
    val Us = map snd params;

    val xs = decls |> map (fn (c, _, mx) => Syntax.const_name c mx);
    val Ts = map #2 decls;
    fun const x T = Term.list_comb (Const (Sign.full_name thy x, Us ---> T), ps);
  in
    ctxt
    |> map_theory (Sign.add_consts_i (decls |> map (fn (c, T, mx) => (c, Us ---> T, mx))))
    |> ProofContext.add_fixes_i (decls |> map (fn (c, T, mx) => (c, SOME T, mx)))
    |-> (fn xs' => pair ((xs' ~~ Ts), map2 const xs Ts))
  end;

end;