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