src/Pure/context.ML
author obua
Sun May 29 12:39:12 2005 +0200 (2005-05-29)
changeset 16108 cf468b93a02e
parent 15801 d2f5ca3c048d
child 16436 7eb6b6cbd166
permissions -rw-r--r--
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
     1 (*  Title:      Pure/context.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4 
     5 Theory contexts.
     6 *)
     7 
     8 signature BASIC_CONTEXT =
     9 sig
    10   val context: theory -> unit
    11   val the_context: unit -> theory
    12 end;
    13 
    14 signature CONTEXT =
    15 sig
    16   include BASIC_CONTEXT
    17   val get_context: unit -> theory option
    18   val set_context: theory option -> unit
    19   val reset_context: unit -> unit
    20   val setmp: theory option -> ('a -> 'b) -> 'a -> 'b
    21   val pass: theory option -> ('a -> 'b) -> 'a -> 'b * theory option
    22   val pass_theory: theory -> ('a -> 'b) -> 'a -> 'b * theory
    23   val save: ('a -> 'b) -> 'a -> 'b
    24   val >> : (theory -> theory) -> unit
    25   val ml_output: (string -> unit) * (string -> unit)
    26   val use_mltext: string -> bool -> theory option -> unit
    27   val use_mltext_theory: string -> bool -> theory -> theory
    28   val use_let: string -> string -> string -> theory -> theory
    29   val add_setup: (theory -> theory) list -> unit
    30   val setup: unit -> (theory -> theory) list
    31 end;
    32 
    33 structure Context: CONTEXT =
    34 struct
    35 
    36 
    37 (** implicit theory context in ML **)
    38 
    39 local
    40   val current_theory = ref (NONE: theory option);
    41 in
    42   fun get_context () = ! current_theory;
    43   fun set_context opt_thy = current_theory := opt_thy;
    44   fun setmp opt_thy f x = Library.setmp current_theory opt_thy f x;
    45 end;
    46 
    47 fun the_context () =
    48   (case get_context () of
    49     SOME thy => thy
    50   | _ => error "Unknown theory context");
    51 
    52 fun context thy = set_context (SOME thy);
    53 fun reset_context () = set_context NONE;
    54 
    55 fun pass opt_thy f x =
    56   setmp opt_thy (fn x => let val y = f x in (y, get_context ()) end) x;
    57 
    58 fun pass_theory thy f x =
    59   (case pass (SOME thy) f x of
    60     (y, SOME thy') => (y, thy')
    61   | (_, NONE) => error "Lost theory context in ML");
    62 
    63 fun save f x = setmp (get_context ()) f x;
    64 
    65 
    66 (* map context *)
    67 
    68 nonfix >>;
    69 fun >> f = set_context (SOME (f (the_context ())));
    70 
    71 
    72 (* use ML text *)
    73 
    74 val ml_output = (writeln, error_msg: string -> unit);
    75 
    76 fun use_output verb txt = use_text ml_output verb (Symbol.escape txt);
    77 
    78 fun use_mltext txt verb opt_thy = setmp opt_thy (fn () => use_output verb txt) ();
    79 fun use_mltext_theory txt verb thy = #2 (pass_theory thy (use_output verb) txt);
    80 
    81 fun use_context txt = use_mltext_theory ("Context.>> (" ^ txt ^ ");") false;
    82 
    83 fun use_let bind body txt =
    84   use_context ("let " ^ bind ^ " = " ^ txt ^ " in\n" ^ body ^ " end");
    85 
    86 
    87 
    88 (** delayed theory setup **)
    89 
    90 local
    91   val setup_fns = ref ([]: (theory -> theory) list);
    92 in
    93   fun add_setup fns = setup_fns := ! setup_fns @ fns;
    94   fun setup () = let val fns = ! setup_fns in setup_fns := []; fns end;
    95 end;
    96 
    97 
    98 end;
    99 
   100 structure BasicContext: BASIC_CONTEXT = Context;
   101 open BasicContext;