src/Pure/locale.ML
author wenzelm
Mon, 09 Nov 1998 15:42:08 +0100
changeset 5840 e2d2b896c717
parent 5782 7559f116cb10
child 6022 259e4f2114e1
permissions -rw-r--r--
Object logic specific operations.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
5244
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/locale.ML
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
     3
    Author:     Florian Kammueller, University of Cambridge
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
     4
5782
7559f116cb10 locales now implicitly quantify over free variables
paulson
parents: 5749
diff changeset
     5
Locales. The theory section 'locale' declarings constants, assumptions and
7559f116cb10 locales now implicitly quantify over free variables
paulson
parents: 5749
diff changeset
     6
definitions that have local scope.  Typical form is
7559f116cb10 locales now implicitly quantify over free variables
paulson
parents: 5749
diff changeset
     7
7559f116cb10 locales now implicitly quantify over free variables
paulson
parents: 5749
diff changeset
     8
    locale Locale_name =
7559f116cb10 locales now implicitly quantify over free variables
paulson
parents: 5749
diff changeset
     9
      fixes   (*variables that are fixed in the locale's scope*)
7559f116cb10 locales now implicitly quantify over free variables
paulson
parents: 5749
diff changeset
    10
	v :: T
7559f116cb10 locales now implicitly quantify over free variables
paulson
parents: 5749
diff changeset
    11
      assumes (*meta-hypothesis that hold in the locale*)
7559f116cb10 locales now implicitly quantify over free variables
paulson
parents: 5749
diff changeset
    12
	Asm_name "meta-formula"  
7559f116cb10 locales now implicitly quantify over free variables
paulson
parents: 5749
diff changeset
    13
      defines (*local definitions of fixed variables in terms of others*)
7559f116cb10 locales now implicitly quantify over free variables
paulson
parents: 5749
diff changeset
    14
	v_def "v x == ...x..."
5244
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
    15
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
    16
TODO:
5782
7559f116cb10 locales now implicitly quantify over free variables
paulson
parents: 5749
diff changeset
    17
  - operations on locales: extension, renaming.
5244
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
    18
*)
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
    19
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
    20
signature BASIC_LOCALE =
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
    21
sig
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
    22
  val print_locales: theory -> unit
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
    23
  val print_goals: int -> thm -> unit
5729
5d66410cceae support current_goals_markers ref variable for print_current_goals;
wenzelm
parents: 5244
diff changeset
    24
  val print_goals_marker: string -> int -> thm -> unit
5244
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
    25
end;
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
    26
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
    27
signature LOCALE =
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
    28
sig
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
    29
  include BASIC_LOCALE
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
    30
  val get_thm: theory -> xstring -> thm
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
    31
  val get_thms: theory -> xstring -> thm list
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
    32
  type locale
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
    33
  val add_locale: bstring -> (string * string * mixfix) list ->
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
    34
    (string * string) list -> (string * string) list -> theory -> theory
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
    35
  val add_locale_i: bstring -> (string * typ * mixfix) list ->
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
    36
    (string * term) list -> (string * term) list -> theory -> theory
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
    37
  val open_locale: xstring -> theory -> theory
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
    38
  val close_locale: theory -> theory
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
    39
  val in_locale: term list -> Sign.sg -> bool
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
    40
  val is_open_loc_sg: Sign.sg -> bool
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
    41
  val is_open_loc: theory -> bool
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
    42
  val read_cterm: Sign.sg -> string * typ -> cterm
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
    43
  val get_scope: theory -> (string * locale) list
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
    44
  val get_scope_sg: Sign.sg -> (string * locale) list
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
    45
  val collect_consts: Sign.sg -> string list
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
    46
  val setup: (theory -> theory) list
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
    47
end;
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
    48
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
    49
structure Locale: LOCALE =
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
    50
struct
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
    51
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
    52
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
    53
(** type locale **)
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
    54
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
    55
type locale =
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
    56
 {consts: (string * typ) list,
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
    57
  nosyn: string list,
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
    58
  rules: (string * term) list,
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
    59
  defs: (string * term) list,
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
    60
  thms: (string * thm) list,
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
    61
  defaults: (string * sort) list * (string * typ) list * string list};
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
    62
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
    63
fun make_locale consts nosyn rules defs thms defaults =
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
    64
  {consts = consts, nosyn = nosyn, rules = rules, defs = defs,
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
    65
    thms = thms, defaults = defaults}: locale;
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
    66
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
    67
fun pretty_locale sg (name, {consts, rules, defs, nosyn = _, thms = _, defaults = _}) =
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
    68
  let
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
    69
    val prt_typ = Pretty.quote o Sign.pretty_typ sg;
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
    70
    val prt_term = Pretty.quote o Sign.pretty_term sg;
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
    71
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
    72
    fun pretty_const (c, T) = Pretty.block
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
    73
      [Pretty.str (c ^ " ::"), Pretty.brk 1, prt_typ T];
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
    74
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
    75
    fun pretty_axiom (a, t) = Pretty.block
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
    76
      [Pretty.str (a ^ ":"), Pretty.brk 1, prt_term t];
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
    77
  in
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
    78
    Pretty.big_list (name ^ " =")
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
    79
     [Pretty.big_list "consts:" (map pretty_const consts),
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
    80
      Pretty.big_list "rules:" (map pretty_axiom rules),
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
    81
      Pretty.big_list "defs:" (map pretty_axiom defs)]
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
    82
  end;
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
    83
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
    84
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
    85
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
    86
(** theory data **)
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
    87
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
    88
(* data kind 'Pure/locales' *)
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
    89
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
    90
type locale_data =
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
    91
  {space: NameSpace.T,
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
    92
    locales: locale Symtab.table,
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
    93
    scope: (string * locale) list ref};
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
    94
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
    95
fun make_locale_data space locales scope =
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
    96
  {space = space, locales = locales, scope = scope}: locale_data;
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
    97
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
    98
structure LocalesArgs =
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
    99
struct
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   100
  val name = "Pure/locales";
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   101
  type T = locale_data;
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   102
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   103
  val empty = make_locale_data NameSpace.empty Symtab.empty (ref []);
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   104
  fun prep_ext {space, locales, scope = _} = make_locale_data space locales (ref []);
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   105
  fun merge ({space = space1, locales = locales1, scope = _},
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   106
    {space = space2, locales = locales2, scope = _}) =
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   107
      make_locale_data (NameSpace.merge (space1, space2))
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   108
        (Symtab.merge (K true) (locales1, locales2))
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   109
        (ref []);
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   110
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   111
  fun print sg {space, locales, scope} =
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   112
    let
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   113
      fun extrn name =
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   114
        if ! long_names then name else NameSpace.extern space name;
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   115
      val locs = map (apfst extrn) (Symtab.dest locales);
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   116
      val scope_names = rev (map (extrn o fst) (! scope));
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   117
    in
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   118
      Pretty.writeln (Display.pretty_name_space ("locale name space", space));
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   119
      Pretty.writeln (Pretty.big_list "locales:" (map (pretty_locale sg) locs));
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   120
      Pretty.writeln (Pretty.strs ("current scope:" :: scope_names))
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   121
    end;
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   122
end;
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   123
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   124
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   125
structure LocalesData = TheoryDataFun(LocalesArgs);
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   126
val print_locales = LocalesData.print;
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   127
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   128
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   129
(* access locales *)
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   130
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   131
fun get_locale_sg sg name = Symtab.lookup (#locales (LocalesData.get_sg sg), name);
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   132
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   133
val get_locale = get_locale_sg o Theory.sign_of;
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   134
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   135
fun put_locale (name, locale) thy =
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   136
  let
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   137
    val {space, locales, scope} = LocalesData.get thy;
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   138
    val space' = NameSpace.extend (space, [name]);
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   139
    val locales' = Symtab.update ((name, locale), locales);
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   140
  in thy |> LocalesData.put (make_locale_data space' locales' scope) end;
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   141
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   142
fun lookup_locale thy xname =
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   143
  let
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   144
    val {space, locales, ...} = LocalesData.get thy;
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   145
    val name = NameSpace.intern space xname;
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   146
  in apsome (pair name) (get_locale thy name) end;
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   147
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   148
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   149
(* access scope *)
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   150
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   151
val get_scope_sg = ! o #scope o LocalesData.get_sg;
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   152
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   153
val get_scope = get_scope_sg o Theory.sign_of;
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   154
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   155
fun change_scope f thy =
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   156
  let val {scope, ...} = LocalesData.get thy
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   157
  in scope := f (! scope) end;
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   158
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   159
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   160
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   161
(** scope operations **)
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   162
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   163
(* change scope *)
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   164
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   165
fun the_locale thy xname =
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   166
  (case lookup_locale thy xname of
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   167
    Some loc => loc
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   168
  | None => error ("Unknown locale " ^ quote xname));
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   169
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   170
fun open_locale xname thy =
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   171
  (change_scope (cons (the_locale thy xname)) thy; thy);
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   172
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   173
fun pop_locale [] = error "Currently no open locales"
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   174
  | pop_locale (_ :: locs) = locs;
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   175
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   176
fun close_locale thy = (change_scope pop_locale thy; thy);
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   177
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   178
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   179
(** functions for goals.ML **)
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   180
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   181
(* in_locale: check if hyps (: term list) of a proof are contained in the
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   182
   (current) scope. This function is needed in prepare_proof. It needs to
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   183
   refer to the signature, because theory is not available in prepare_proof. *)
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   184
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   185
fun in_locale hyps sg =
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   186
    let val cur_sc = get_scope_sg sg;
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   187
        val rule_lists = map (#rules o snd) cur_sc;
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   188
        val def_lists = map (#defs o snd) cur_sc;
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   189
        val rules = map snd (foldr (op union) (rule_lists, []));
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   190
        val defs = map snd (foldr (op union) (def_lists, []));
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   191
        val defnrules = rules @ defs;
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   192
    in
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   193
        hyps subset defnrules
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   194
    end;
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   195
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   196
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   197
(* is_open_loc: check if any locale is open, i.e. in the scope of the current thy *)
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   198
fun is_open_loc_sg sign =
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   199
    let val cur_sc = get_scope_sg sign
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   200
    in not(null(cur_sc)) end;
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   201
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   202
val is_open_loc = is_open_loc_sg o Theory.sign_of;
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   203
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   204
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   205
(* get theorems *)
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   206
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   207
fun get_thm_locale name ((_, {thms, ...}: locale)) = assoc (thms, name);
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   208
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   209
fun get_thmx f get thy name =
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   210
  (case get_first (get_thm_locale name) (get_scope thy) of
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   211
    Some thm => f thm
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   212
  | None => get thy name);
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   213
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   214
val get_thm = get_thmx I PureThy.get_thm;
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   215
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   216
val get_thms = get_thmx (fn x => [x]) PureThy.get_thms;
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   217
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   218
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   219
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   220
(** define locales **)
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   221
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   222
(* prepare types *)
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   223
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   224
fun read_typ sg (envT, s) =
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   225
  let
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   226
    fun def_sort (x, ~1) = assoc (envT, x)
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   227
      | def_sort _ = None;
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   228
    val T = Type.no_tvars (Sign.read_typ (sg, def_sort) s) handle TYPE (msg, _, _) => error msg;
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   229
  in (Term.add_typ_tfrees (T, envT), T) end;
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   230
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   231
fun cert_typ sg (envT, raw_T) =
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   232
  let val T = Type.no_tvars (Sign.certify_typ sg raw_T) handle TYPE (msg, _, _) => error msg
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   233
  in (Term.add_typ_tfrees (T, envT), T) end;
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   234
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   235
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   236
(* prepare props *)
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   237
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   238
val add_frees = foldl_aterms (fn (vs, Free v) => v ins vs | (vs, _) => vs);
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   239
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   240
fun enter_term t (envS, envT, used) =
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   241
  (Term.add_term_tfrees (t, envS), add_frees (envT, t), Term.add_term_tfree_names (t, used));
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   242
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   243
fun read_axm sg ((envS, envT, used), (name, s)) =
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   244
  let
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   245
    fun def_sort (x, ~1) = assoc (envS, x)
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   246
      | def_sort _ = None;
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   247
    fun def_type (x, ~1) = assoc (envT, x)
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   248
      | def_type _ = None;
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   249
    val (_, t) = Theory.read_def_axm (sg, def_type, def_sort) used (name, s);
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   250
  in
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   251
    (enter_term t (envS, envT, used), t)
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   252
  end;
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   253
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   254
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   255
fun cert_axm sg ((envS, envT, used), (name, raw_t)) =
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   256
  let val (_, t) = Theory.cert_axm sg (name, raw_t)
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   257
  in (enter_term t (envS, envT, used), t) end;
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   258
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   259
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   260
(* Locale.read_cterm: read in a string as a certified term, and respect the bindings
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   261
   that already exist for subterms. If no locale is open, this function is equal to
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   262
   Thm.read_cterm  *)
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   263
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   264
fun read_cterm sign =
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   265
    let val cur_sc = get_scope_sg sign;
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   266
        val defaults = map (#defaults o snd) cur_sc;
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   267
        val envS = flat (map #1 defaults);
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   268
        val envT = flat (map #2 defaults);
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   269
        val used = flat (map #3 defaults);
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   270
        fun def_sort (x, ~1) = assoc (envS, x)
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   271
          | def_sort _ = None;
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   272
        fun def_type (x, ~1) = assoc (envT, x)
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   273
          | def_type _ = None;
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   274
    in (if (is_open_loc_sg sign)
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   275
        then (#1 o read_def_cterm (sign, def_type, def_sort) used true)
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   276
        else Thm.read_cterm sign)
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   277
    end;
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   278
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   279
(* basic functions needed for definitions and display *)
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   280
(* collect all locale constants of a scope, i.e. a list of locales *)
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   281
fun collect_consts sg =
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   282
    let val cur_sc = get_scope_sg sg;
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   283
        val locale_list = map snd cur_sc;
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   284
        val const_list = flat (map #consts locale_list)
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   285
    in map fst const_list end;
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   286
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   287
(* filter out the Free's in a term *)
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   288
fun list_frees t =
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   289
    case t of Const(c,T) => []
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   290
  | Var(v,T) => []
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   291
  | Free(v,T)=> [Free(v,T)]
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   292
  | Bound x  => []
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   293
  | Abs(a,T,u) => list_frees u
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   294
  | t1 $ t2  => (list_frees t1)  @ (list_frees t2);
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   295
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   296
(* filter out all Free's in a term that are not contained
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   297
   in a list of strings. Used to prepare definitions. The list of strings
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   298
   will be the consts of the scope. We filter out the "free" Free's to be
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   299
   able to bind them *)
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   300
fun difflist term clist =
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   301
    let val flist = list_frees term;
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   302
        fun builddiff [] sl = []
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   303
          | builddiff (t :: tl) sl =
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   304
            let val Free(v,T) = t
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   305
            in
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   306
                if (v mem sl)
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   307
                then builddiff tl sl
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   308
                else t :: (builddiff tl sl)
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   309
            end;
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   310
    in distinct(builddiff flist clist) end;
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   311
5782
7559f116cb10 locales now implicitly quantify over free variables
paulson
parents: 5749
diff changeset
   312
(* Bind a term with !! over a list of "free" Free's.
7559f116cb10 locales now implicitly quantify over free variables
paulson
parents: 5749
diff changeset
   313
   To enable definitions like x + y == .... (without quantifier).
7559f116cb10 locales now implicitly quantify over free variables
paulson
parents: 5749
diff changeset
   314
   Complications, because x and y have to be removed from defaults *)
7559f116cb10 locales now implicitly quantify over free variables
paulson
parents: 5749
diff changeset
   315
fun abs_over_free clist ((defaults: (string * sort) list * (string * typ) list * string list), (s, term)) =
5244
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   316
    let val diffl = rev(difflist term clist);
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   317
        fun abs_o (t, (x as Free(v,T))) = all(T) $ Abs(v, T, abstract_over (x,t))
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   318
          | abs_o (_ , _) = error ("Can't be: abs_over_free");
5782
7559f116cb10 locales now implicitly quantify over free variables
paulson
parents: 5749
diff changeset
   319
        val diffl' = map (fn (Free (s, T)) => s) diffl;
7559f116cb10 locales now implicitly quantify over free variables
paulson
parents: 5749
diff changeset
   320
        val defaults' = (#1 defaults, filter (fn x => not((fst x) mem diffl')) (#2 defaults), #3 defaults)
7559f116cb10 locales now implicitly quantify over free variables
paulson
parents: 5749
diff changeset
   321
    in (defaults', (s, foldl abs_o (term, diffl))) end;
5244
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   322
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   323
(* assume a definition, i.e assume the cterm of a definiton term and then eliminate
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   324
   the binding !!, so that the def can be applied as rewrite. The meta hyp will still contain !! *)
5782
7559f116cb10 locales now implicitly quantify over free variables
paulson
parents: 5749
diff changeset
   325
fun prep_hyps clist sg = forall_elim_vars(0) o Thm.assume o (Thm.cterm_of sg);
5244
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   326
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   327
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   328
(* concrete syntax *)
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   329
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   330
fun mark_syn c = "\\<^locale>" ^ c;
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   331
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   332
fun mk_loc_tr c ts = list_comb (Free (c, dummyT), ts);
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   333
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   334
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   335
(* add_locale *)
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   336
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   337
fun gen_add_locale prep_typ prep_term bname raw_consts raw_rules raw_defs thy =
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   338
  let val sign = Theory.sign_of thy;
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   339
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   340
    val name = Sign.full_name sign bname;
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   341
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   342
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   343
    (* prepare locale consts *)
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   344
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   345
    fun prep_const (envS, (raw_c, raw_T, raw_mx)) =
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   346
      let
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   347
        val c = Syntax.const_name raw_c raw_mx;
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   348
        val c_syn = mark_syn c;
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   349
        val mx = Syntax.fix_mixfix raw_c raw_mx;
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   350
        val (envS', T) = prep_typ sign (envS, raw_T) handle ERROR =>
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   351
          error ("The error(s) above occured in locale constant " ^ quote c);
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   352
        val trfun = if mx = Syntax.NoSyn then None else Some (c_syn, mk_loc_tr c);
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   353
      in (envS', ((c, T), (c_syn, T, mx), trfun)) end;
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   354
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   355
    val (envS0, loc_consts_syn) = foldl_map prep_const ([], raw_consts);
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   356
    val loc_consts = map #1 loc_consts_syn;
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   357
    val loc_syn = map #2 loc_consts_syn;
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   358
    val nosyn = map (#1 o #1) (filter (fn x => (#3(#2 x)) = NoSyn) loc_consts_syn);
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   359
    val loc_trfuns = mapfilter #3 loc_consts_syn;
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   360
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   361
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   362
    (* 1st stage: syntax_thy *)
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   363
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   364
    val syntax_thy =
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   365
      thy
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   366
      |> Theory.add_modesyntax_i ("", true) loc_syn
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   367
      |> Theory.add_trfuns ([], loc_trfuns, [], []);
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   368
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   369
    val syntax_sign = Theory.sign_of syntax_thy;
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   370
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   371
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   372
    (* prepare rules and defs *)
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   373
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   374
    fun prep_axiom (env, (a, raw_t)) =
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   375
      let
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   376
        val (env', t) = prep_term syntax_sign (env, (a, raw_t)) handle ERROR =>
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   377
          error ("The error(s) above occured in locale rule / definition " ^ quote a);
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   378
      in (env', (a, t)) end;
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   379
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   380
    val ((envS1, envT1, used1), loc_rules) =
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   381
      foldl_map prep_axiom ((envS0, loc_consts, map fst envS0), raw_rules);
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   382
    val (defaults, loc_defs) = foldl_map prep_axiom ((envS1, envT1, used1), raw_defs);
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   383
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   384
    val old_loc_consts = collect_consts syntax_sign;
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   385
    val new_loc_consts = (map #1 loc_consts);
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   386
    val all_loc_consts = old_loc_consts @ new_loc_consts;
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   387
5782
7559f116cb10 locales now implicitly quantify over free variables
paulson
parents: 5749
diff changeset
   388
    val (defaults, loc_defs_terms) = foldl_map (abs_over_free all_loc_consts) (defaults, loc_defs);
7559f116cb10 locales now implicitly quantify over free variables
paulson
parents: 5749
diff changeset
   389
    val loc_defs_thms = map (apsnd (prep_hyps (map #1 loc_consts) syntax_sign)) loc_defs_terms;
7559f116cb10 locales now implicitly quantify over free variables
paulson
parents: 5749
diff changeset
   390
    val (defaults, loc_thms_terms) = foldl_map (abs_over_free all_loc_consts) (defaults, loc_rules);
7559f116cb10 locales now implicitly quantify over free variables
paulson
parents: 5749
diff changeset
   391
    val loc_thms = (map (apsnd (prep_hyps (map #1 loc_consts) syntax_sign)) (loc_thms_terms)) 
7559f116cb10 locales now implicitly quantify over free variables
paulson
parents: 5749
diff changeset
   392
                   @ loc_defs_thms;
5244
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   393
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   394
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   395
    (* error messages *)        (* FIXME improve *)
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   396
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   397
    val err_dup_locale =
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   398
      if is_none (get_locale thy name) then []
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   399
      else ["Duplicate definition of locale " ^ quote name];
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   400
5782
7559f116cb10 locales now implicitly quantify over free variables
paulson
parents: 5749
diff changeset
   401
    (* check if definientes are locale constants (in the same locale, so no redefining!) *)
5749
fb846bcb80ce better checking of "defines" in a locale
paulson
parents: 5729
diff changeset
   402
    val err_def_head =
fb846bcb80ce better checking of "defines" in a locale
paulson
parents: 5729
diff changeset
   403
      let fun peal_appl t = 
fb846bcb80ce better checking of "defines" in a locale
paulson
parents: 5729
diff changeset
   404
            case t of 
fb846bcb80ce better checking of "defines" in a locale
paulson
parents: 5729
diff changeset
   405
                 t1 $ t2 => peal_appl t1
fb846bcb80ce better checking of "defines" in a locale
paulson
parents: 5729
diff changeset
   406
               | Free(t) => t
fb846bcb80ce better checking of "defines" in a locale
paulson
parents: 5729
diff changeset
   407
               | _ => error ("a bad locale definition");
fb846bcb80ce better checking of "defines" in a locale
paulson
parents: 5729
diff changeset
   408
	  fun lhs (_, Const ("==" , _) $  d1 $ d2) = peal_appl d1
fb846bcb80ce better checking of "defines" in a locale
paulson
parents: 5729
diff changeset
   409
	    | lhs _ = error ("an illegal definition");
fb846bcb80ce better checking of "defines" in a locale
paulson
parents: 5729
diff changeset
   410
          val defs = map lhs loc_defs;
fb846bcb80ce better checking of "defines" in a locale
paulson
parents: 5729
diff changeset
   411
          val check = defs subset loc_consts
fb846bcb80ce better checking of "defines" in a locale
paulson
parents: 5729
diff changeset
   412
      in if check then [] 
fb846bcb80ce better checking of "defines" in a locale
paulson
parents: 5729
diff changeset
   413
         else ["defined item not declared fixed in locale " ^ quote name]
fb846bcb80ce better checking of "defines" in a locale
paulson
parents: 5729
diff changeset
   414
      end; 
fb846bcb80ce better checking of "defines" in a locale
paulson
parents: 5729
diff changeset
   415
5782
7559f116cb10 locales now implicitly quantify over free variables
paulson
parents: 5749
diff changeset
   416
    (* check that variables on rhs of definitions are either fixed or on lhs *)
7559f116cb10 locales now implicitly quantify over free variables
paulson
parents: 5749
diff changeset
   417
    val err_var_rhs = 
7559f116cb10 locales now implicitly quantify over free variables
paulson
parents: 5749
diff changeset
   418
      let fun compare_var_sides (t, (_, Const ("==", _) $ d1 $ d2)) = 
7559f116cb10 locales now implicitly quantify over free variables
paulson
parents: 5749
diff changeset
   419
            let val varl1 = difflist d1 all_loc_consts;
7559f116cb10 locales now implicitly quantify over free variables
paulson
parents: 5749
diff changeset
   420
                val varl2 = difflist d2 all_loc_consts
7559f116cb10 locales now implicitly quantify over free variables
paulson
parents: 5749
diff changeset
   421
            in t andalso (varl2 subset varl1)
7559f116cb10 locales now implicitly quantify over free variables
paulson
parents: 5749
diff changeset
   422
            end
7559f116cb10 locales now implicitly quantify over free variables
paulson
parents: 5749
diff changeset
   423
            | compare_var_sides (_,_) = error ("an illegal definition");
7559f116cb10 locales now implicitly quantify over free variables
paulson
parents: 5749
diff changeset
   424
          val check = foldl compare_var_sides (true, loc_defs)
7559f116cb10 locales now implicitly quantify over free variables
paulson
parents: 5749
diff changeset
   425
      in if check then []
7559f116cb10 locales now implicitly quantify over free variables
paulson
parents: 5749
diff changeset
   426
         else ["nonfixed variable on right hand side of a locale definition in locale" ^ quote name]
7559f116cb10 locales now implicitly quantify over free variables
paulson
parents: 5749
diff changeset
   427
      end;
7559f116cb10 locales now implicitly quantify over free variables
paulson
parents: 5749
diff changeset
   428
7559f116cb10 locales now implicitly quantify over free variables
paulson
parents: 5749
diff changeset
   429
    val errs = err_dup_locale @ err_def_head @ err_var_rhs;
5244
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   430
  in
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   431
    if null errs then ()
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   432
    else error (cat_lines errs);
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   433
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   434
    syntax_thy
5749
fb846bcb80ce better checking of "defines" in a locale
paulson
parents: 5729
diff changeset
   435
    |> put_locale (name, 
5782
7559f116cb10 locales now implicitly quantify over free variables
paulson
parents: 5749
diff changeset
   436
		   make_locale loc_consts nosyn loc_thms_terms loc_defs_terms
5749
fb846bcb80ce better checking of "defines" in a locale
paulson
parents: 5729
diff changeset
   437
		               loc_thms defaults)
5244
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   438
  end;
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   439
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   440
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   441
val add_locale = gen_add_locale read_typ read_axm;
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   442
val add_locale_i = gen_add_locale cert_typ cert_axm;
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   443
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   444
(** print functions **)
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   445
(* idea: substitute all locale contants (Free's) that are syntactical by their
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   446
         "real" constant representation (i.e. \\<^locale>constname).
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   447
   - function const_ssubst does this substitution
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   448
   - function Locale.pretty_term:
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   449
             if locale is open then do this substitution & then call Sign.pretty_term
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   450
             else call Sign.pretty_term
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   451
*)
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   452
(* substitutes all Free variables s in t by Const's s *)
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   453
fun const_ssubst t s =
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   454
    case t  of
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   455
        Free(v,T) => if v = s then Const("\\<^locale>" ^ s,T) else Free(v,T)
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   456
      | Const(c,T) => Const(c,T)
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   457
      | Var(v,T) => Var(v,T)
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   458
      | Bound x  => Bound x
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   459
      | Abs(a,T,u) => Abs(a,T, const_ssubst u s)
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   460
      | t1 $ t2  => const_ssubst t1 s $ const_ssubst t2 s;
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   461
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   462
(* FIXME: improve: can be expressed with foldl *)
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   463
fun const_ssubst_list [] t = t
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   464
  | const_ssubst_list (s :: l) t = const_ssubst_list l (const_ssubst t s);
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   465
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   466
(* Locale.pretty_term *)
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   467
fun pretty_term sign =
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   468
    if (is_open_loc_sg sign) then
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   469
        let val locale_list = map snd(get_scope_sg sign);
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   470
            val nosyn = flat (map #nosyn locale_list);
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   471
            val str_list = (collect_consts sign) \\ nosyn
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   472
        in Sign.pretty_term sign o (const_ssubst_list str_list)
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   473
        end
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   474
    else Sign.pretty_term sign;
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   475
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   476
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   477
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   478
(** print_goals **)
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   479
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   480
(*print thm A1,...,An/B in "goal style" -- premises as numbered subgoals*)
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   481
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   482
local
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   483
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   484
  (* utils *)
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   485
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   486
  fun ins_entry (x, y) [] = [(x, [y])]
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   487
    | ins_entry (x, y) ((pair as (x', ys')) :: pairs) =
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   488
        if x = x' then (x', y ins ys') :: pairs
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   489
        else pair :: ins_entry (x, y) pairs;
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   490
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   491
  fun add_consts (Const (c, T), env) = ins_entry (T, (c, T)) env
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   492
    | add_consts (t $ u, env) = add_consts (u, add_consts (t, env))
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   493
    | add_consts (Abs (_, _, t), env) = add_consts (t, env)
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   494
    | add_consts (_, env) = env;
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   495
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   496
  fun add_vars (Free (x, T), env) = ins_entry (T, (x, ~1)) env
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   497
    | add_vars (Var (xi, T), env) = ins_entry (T, xi) env
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   498
    | add_vars (Abs (_, _, t), env) = add_vars (t, env)
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   499
    | add_vars (t $ u, env) = add_vars (u, add_vars (t, env))
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   500
    | add_vars (_, env) = env;
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   501
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   502
  fun add_varsT (Type (_, Ts), env) = foldr add_varsT (Ts, env)
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   503
    | add_varsT (TFree (x, S), env) = ins_entry (S, (x, ~1)) env
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   504
    | add_varsT (TVar (xi, S), env) = ins_entry (S, xi) env;
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   505
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   506
  fun sort_idxs vs = map (apsnd (sort (prod_ord string_ord int_ord))) vs;
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   507
  fun sort_cnsts cs = map (apsnd (sort_wrt fst)) cs;
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   508
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   509
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   510
  (* prepare atoms *)
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   511
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   512
  fun consts_of t = sort_cnsts (add_consts (t, []));
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   513
  fun vars_of t = sort_idxs (add_vars (t, []));
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   514
  fun varsT_of t = rev (sort_idxs (it_term_types add_varsT (t, [])));
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   515
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   516
in
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   517
5729
5d66410cceae support current_goals_markers ref variable for print_current_goals;
wenzelm
parents: 5244
diff changeset
   518
  fun print_goals_marker begin_goal maxgoals state =
5244
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   519
    let
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   520
      val {sign, ...} = rep_thm state;
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   521
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   522
      val prt_term = pretty_term sign;
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   523
      val prt_typ = Sign.pretty_typ sign;
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   524
      val prt_sort = Sign.pretty_sort sign;
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   525
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   526
      fun prt_atoms prt prtT (X, xs) = Pretty.block
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   527
        [Pretty.block (Pretty.commas (map prt xs)), Pretty.str " ::",
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   528
          Pretty.brk 1, prtT X];
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   529
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   530
      fun prt_var (x, ~1) = prt_term (Syntax.free x)
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   531
        | prt_var xi = prt_term (Syntax.var xi);
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   532
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   533
      fun prt_varT (x, ~1) = prt_typ (TFree (x, []))
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   534
        | prt_varT xi = prt_typ (TVar (xi, []));
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   535
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   536
      val prt_consts = prt_atoms (prt_term o Const) prt_typ;
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   537
      val prt_vars = prt_atoms prt_var prt_typ;
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   538
      val prt_varsT = prt_atoms prt_varT prt_sort;
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   539
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   540
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   541
      fun print_list _ _ [] = ()
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   542
        | print_list name prt lst = (writeln "";
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   543
            Pretty.writeln (Pretty.big_list name (map prt lst)));
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   544
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   545
      fun print_subgoals (_, []) = ()
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   546
        | print_subgoals (n, A :: As) = (Pretty.writeln (Pretty.blk (0,
5729
5d66410cceae support current_goals_markers ref variable for print_current_goals;
wenzelm
parents: 5244
diff changeset
   547
            [Pretty.str (begin_goal ^ " " ^ string_of_int n ^ ". "), prt_term A]));
5244
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   548
              print_subgoals (n + 1, As));
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   549
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   550
      val print_ffpairs =
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   551
        print_list "Flex-flex pairs:" (prt_term o Logic.mk_flexpair);
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   552
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   553
      val print_consts = print_list "Constants:" prt_consts o consts_of;
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   554
      val print_vars = print_list "Variables:" prt_vars o vars_of;
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   555
      val print_varsT = print_list "Type variables:" prt_varsT o varsT_of;
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   556
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   557
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   558
      val {prop, ...} = rep_thm state;
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   559
      val (tpairs, As, B) = Logic.strip_horn prop;
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   560
      val ngoals = length As;
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   561
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   562
      fun print_gs (types, sorts) =
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   563
       (Pretty.writeln (prt_term B);
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   564
        if ngoals = 0 then writeln "No subgoals!"
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   565
        else if ngoals > maxgoals then
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   566
          (print_subgoals (1, take (maxgoals, As));
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   567
            writeln ("A total of " ^ string_of_int ngoals ^ " subgoals..."))
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   568
        else print_subgoals (1, As);
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   569
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   570
        print_ffpairs tpairs;
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   571
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   572
        if types andalso ! show_consts then print_consts prop else ();
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   573
        if types then print_vars prop else ();
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   574
        if sorts then print_varsT prop else ());
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   575
    in
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   576
      setmp show_no_free_types true
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   577
        (setmp show_types (! show_types orelse ! show_sorts)
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   578
          (setmp show_sorts false print_gs))
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   579
     (! show_types orelse ! show_sorts, ! show_sorts)
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   580
  end;
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   581
5729
5d66410cceae support current_goals_markers ref variable for print_current_goals;
wenzelm
parents: 5244
diff changeset
   582
  val print_goals = print_goals_marker "";
5d66410cceae support current_goals_markers ref variable for print_current_goals;
wenzelm
parents: 5244
diff changeset
   583
5244
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   584
end;
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   585
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   586
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   587
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   588
(** locale theory setup **)
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   589
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   590
val setup =
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   591
 [LocalesData.init];
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   592
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   593
end;
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   594
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   595
structure BasicLocale: BASIC_LOCALE = Locale;
5313f781efe0 added locale.ML;
wenzelm
parents:
diff changeset
   596
open BasicLocale;