src/Pure/Isar/local_theory.ML
author wenzelm
Sun Jan 22 18:46:01 2006 +0100 (2006-01-22 ago)
changeset 18744 a9a5ee0e43e2
child 18767 2f064e6bea7e
permissions -rw-r--r--
Local theory operations, with optional target locale.
wenzelm@18744
     1
(*  Title:      Pure/Isar/local_theory.ML
wenzelm@18744
     2
    ID:         $Id$
wenzelm@18744
     3
    Author:     Makarius
wenzelm@18744
     4
wenzelm@18744
     5
Local theory operations, with optional target locale.
wenzelm@18744
     6
*)
wenzelm@18744
     7
wenzelm@18744
     8
signature LOCAL_THEORY =
wenzelm@18744
     9
sig
wenzelm@18744
    10
  val map_theory: (theory -> theory) -> Proof.context -> Proof.context
wenzelm@18744
    11
  val map_theory_result: (theory -> 'a * theory) -> Proof.context -> 'a * Proof.context
wenzelm@18744
    12
  val init: string option -> theory -> Proof.context
wenzelm@18744
    13
  val exit: Proof.context -> theory
wenzelm@18744
    14
  val params_of: Proof.context -> (string * typ) list
wenzelm@18744
    15
  val consts: (string * typ * mixfix) list -> Proof.context ->
wenzelm@18744
    16
    ((string * typ) list * term list) * Proof.context
wenzelm@18744
    17
end;
wenzelm@18744
    18
wenzelm@18744
    19
structure LocalTheory: LOCAL_THEORY =
wenzelm@18744
    20
struct
wenzelm@18744
    21
wenzelm@18744
    22
(* local context data *)
wenzelm@18744
    23
wenzelm@18744
    24
structure Data = ProofDataFun
wenzelm@18744
    25
(
wenzelm@18744
    26
  val name = "Isar/local_theory";
wenzelm@18744
    27
  type T =
wenzelm@18744
    28
   {locale: string option,
wenzelm@18744
    29
    params: (string * typ) list,
wenzelm@18744
    30
    hyps: term list,
wenzelm@18744
    31
    exit: theory -> theory};
wenzelm@18744
    32
  fun init _ = {locale = NONE, params = [], hyps = [], exit = I};
wenzelm@18744
    33
  fun print _ _ = ();
wenzelm@18744
    34
);
wenzelm@18744
    35
wenzelm@18744
    36
val _ = Context.add_setup Data.init;
wenzelm@18744
    37
wenzelm@18744
    38
wenzelm@18744
    39
(* theory *)
wenzelm@18744
    40
wenzelm@18744
    41
fun map_theory f ctxt =
wenzelm@18744
    42
  ProofContext.transfer (f (ProofContext.theory_of ctxt)) ctxt;
wenzelm@18744
    43
wenzelm@18744
    44
fun map_theory_result f ctxt =
wenzelm@18744
    45
  let val (res, thy') = f (ProofContext.theory_of ctxt)
wenzelm@18744
    46
  in (res, ProofContext.transfer thy' ctxt) end;
wenzelm@18744
    47
wenzelm@18744
    48
fun init NONE thy = ProofContext.init thy
wenzelm@18744
    49
  | init (SOME loc) thy =
wenzelm@18744
    50
      thy
wenzelm@18744
    51
      |> Locale.init loc
wenzelm@18744
    52
      |> (fn ctxt => Data.put
wenzelm@18744
    53
          {locale = SOME loc,
wenzelm@18744
    54
           params = Locale.the_params thy loc,
wenzelm@18744
    55
           hyps = ProofContext.assms_of ctxt,   (* FIXME query locale!! *)
wenzelm@18744
    56
           exit = Sign.restore_naming thy} ctxt)
wenzelm@18744
    57
      |> map_theory (Sign.add_path loc #> Sign.no_base_names);
wenzelm@18744
    58
wenzelm@18744
    59
fun exit ctxt = #exit (Data.get ctxt) (ProofContext.theory_of ctxt);
wenzelm@18744
    60
wenzelm@18744
    61
wenzelm@18744
    62
(* local theory *)
wenzelm@18744
    63
wenzelm@18744
    64
val params_of = #params o Data.get;
wenzelm@18744
    65
wenzelm@18744
    66
fun consts decls ctxt =
wenzelm@18744
    67
  let
wenzelm@18744
    68
    val thy = ProofContext.theory_of ctxt;
wenzelm@18744
    69
    val params = params_of ctxt;
wenzelm@18744
    70
    val ps = map Free params;
wenzelm@18744
    71
    val Us = map snd params;
wenzelm@18744
    72
wenzelm@18744
    73
    val xs = decls |> map (fn (c, _, mx) => Syntax.const_name c mx);
wenzelm@18744
    74
    val Ts = map #2 decls;
wenzelm@18744
    75
    fun const x T = Term.list_comb (Const (Sign.full_name thy x, Us ---> T), ps);
wenzelm@18744
    76
  in
wenzelm@18744
    77
    ctxt
wenzelm@18744
    78
    |> map_theory (Sign.add_consts_i (decls |> map (fn (c, T, mx) => (c, Us ---> T, mx))))
wenzelm@18744
    79
    |> ProofContext.add_fixes_i (decls |> map (fn (c, T, mx) => (c, SOME T, mx)))
wenzelm@18744
    80
    |-> (fn xs' => pair ((xs' ~~ Ts), map2 const xs Ts))
wenzelm@18744
    81
  end;
wenzelm@18744
    82
wenzelm@18744
    83
end;