src/Pure/context.ML
author berghofe
Thu Apr 21 19:12:03 2005 +0200 (2005-04-21)
changeset 15797 a63605582573
parent 15531 08c8dad8e399
child 15801 d2f5ca3c048d
permissions -rw-r--r--
- Eliminated nodup_vars check.
- Unification and matching functions now check types of term variables / sorts
of type variables when applying a substitution.
- Thm.instantiate now takes (ctyp * ctyp) list instead of (indexname * ctyp) list
as argument, to allow for proper instantiation of theorems containing
type variables with same name but different sorts.
     1 (*  Title:      Pure/context.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4 
     5 Global theory context.
     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 use_setup: string -> theory -> theory
    30 end;
    31 
    32 structure Context: CONTEXT =
    33 struct
    34 
    35 
    36 (* theory context *)
    37 
    38 local
    39   val current_theory = ref (NONE: theory option);
    40 in
    41   fun get_context () = ! current_theory;
    42   fun set_context opt_thy = current_theory := opt_thy;
    43   fun setmp opt_thy f x = Library.setmp current_theory opt_thy f x;
    44 end;
    45 
    46 fun the_context () =
    47   (case get_context () of
    48     SOME thy => thy
    49   | _ => error "Unknown theory context");
    50 
    51 fun context thy = set_context (SOME thy);
    52 fun reset_context () = set_context NONE;
    53 
    54 fun pass opt_thy f x =
    55   setmp opt_thy (fn x => let val y = f x in (y, get_context ()) end) x;
    56 
    57 fun pass_theory thy f x =
    58   (case pass (SOME thy) f x of
    59     (y, SOME thy') => (y, thy')
    60   | (_, NONE) => error "Lost theory context in ML");
    61 
    62 fun save f x = setmp (get_context ()) f x;
    63 
    64 
    65 (* map context *)
    66 
    67 nonfix >>;
    68 fun >> f = set_context (SOME (f (the_context ())));
    69 
    70 
    71 (* use ML text *)
    72 
    73 val ml_output = (writeln, error_msg: string -> unit);
    74 
    75 fun use_output verb txt = use_text ml_output verb (Symbol.escape txt);
    76 
    77 fun use_mltext txt verb opt_thy = setmp opt_thy (fn () => use_output verb txt) ();
    78 fun use_mltext_theory txt verb thy = #2 (pass_theory thy (use_output verb) txt);
    79 
    80 fun use_context txt = use_mltext_theory ("Context.>> (" ^ txt ^ ");") false;
    81 
    82 fun use_let bind body txt =
    83   use_context ("let " ^ bind ^ " = " ^ txt ^ " in\n" ^ body ^ " end");
    84 
    85 val use_setup =
    86   use_let "val setup: (theory -> theory) list" "Library.apply setup";
    87 
    88 
    89 end;
    90 
    91 structure BasicContext: BASIC_CONTEXT = Context;
    92 open BasicContext;