src/Pure/Isar/locale.ML
author haftmann
Sat, 10 Feb 2007 09:26:19 +0100
changeset 22300 596f49b70c70
parent 22241 5b2dc1b30e7a
child 22339 0dc6b45e5662
permissions -rw-r--r--
internal interfaces for interpretation and interpret
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
12014
035ab884b9e0 beginnings of new locales (not yet functional);
wenzelm
parents: 11896
diff changeset
     1
(*  Title:      Pure/Isar/locale.ML
11896
1ff33f896720 moved locale.ML to Isar/locale.ML;
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
15206
09d78ec709c7 Modified locales: improved implementation of "includes".
ballarin
parents: 15127
diff changeset
     3
    Author:     Clemens Ballarin, TU Muenchen; Markus Wenzel, LMU/TU Muenchen
11896
1ff33f896720 moved locale.ML to Isar/locale.ML;
wenzelm
parents:
diff changeset
     4
12058
cc182b43dd55 fixes: optional typ;
wenzelm
parents: 12046
diff changeset
     5
Locales -- Isar proof contexts as meta-level predicates, with local
12529
d99716a53f59 simultaneous type-inference of complete context/statement specifications;
wenzelm
parents: 12514
diff changeset
     6
syntax and implicit structures.
d99716a53f59 simultaneous type-inference of complete context/statement specifications;
wenzelm
parents: 12514
diff changeset
     7
19942
dc92e3aebc71 Improved handling of defines imported in duplicate.
ballarin
parents: 19932
diff changeset
     8
Draws basic ideas from Florian Kammueller's original version of
12529
d99716a53f59 simultaneous type-inference of complete context/statement specifications;
wenzelm
parents: 12514
diff changeset
     9
locales, but uses the richer infrastructure of Isar instead of the raw
20035
80c79876d2de Internal restructuring: identify no longer computes syntax.
ballarin
parents: 20032
diff changeset
    10
meta-logic.  Furthermore, structured import of contexts (with merge
80c79876d2de Internal restructuring: identify no longer computes syntax.
ballarin
parents: 20032
diff changeset
    11
and rename operations) are provided, as well as type-inference of the
13375
7cbf2dea46d0 proper predicate definitions of locale body;
wenzelm
parents: 13336
diff changeset
    12
signature parts, and predicate definitions of the specification text.
14446
0bc2519e9990 *** empty log message ***
ballarin
parents: 14291
diff changeset
    13
17437
9deaf32c83be interpretation uses primitive goal interface
ballarin
parents: 17412
diff changeset
    14
Interpretation enables the reuse of theorems of locales in other
9deaf32c83be interpretation uses primitive goal interface
ballarin
parents: 17412
diff changeset
    15
contexts, namely those defined by theories, structured proofs and
9deaf32c83be interpretation uses primitive goal interface
ballarin
parents: 17412
diff changeset
    16
locales themselves.
9deaf32c83be interpretation uses primitive goal interface
ballarin
parents: 17412
diff changeset
    17
14446
0bc2519e9990 *** empty log message ***
ballarin
parents: 14291
diff changeset
    18
See also:
0bc2519e9990 *** empty log message ***
ballarin
parents: 14291
diff changeset
    19
0bc2519e9990 *** empty log message ***
ballarin
parents: 14291
diff changeset
    20
[1] Clemens Ballarin. Locales and Locale Expressions in Isabelle/Isar.
0bc2519e9990 *** empty log message ***
ballarin
parents: 14291
diff changeset
    21
    In Stefano Berardi et al., Types for Proofs and Programs: International
15099
6d8619440ea0 Some comments added.
ballarin
parents: 14981
diff changeset
    22
    Workshop, TYPES 2003, Torino, Italy, LNCS 3085, pages 34-50, 2004.
19942
dc92e3aebc71 Improved handling of defines imported in duplicate.
ballarin
parents: 19932
diff changeset
    23
[2] Clemens Ballarin. Interpretation of Locales in Isabelle: Managing
dc92e3aebc71 Improved handling of defines imported in duplicate.
ballarin
parents: 19932
diff changeset
    24
    Dependencies between Locales. Technical Report TUM-I0607, Technische
dc92e3aebc71 Improved handling of defines imported in duplicate.
ballarin
parents: 19932
diff changeset
    25
    Universitaet Muenchen, 2006.
dc92e3aebc71 Improved handling of defines imported in duplicate.
ballarin
parents: 19932
diff changeset
    26
[3] Clemens Ballarin. Interpretation of Locales in Isabelle: Theories and
dc92e3aebc71 Improved handling of defines imported in duplicate.
ballarin
parents: 19932
diff changeset
    27
    Proof Contexts. In J.M. Borwein and W.M. Farmer, MKM 2006, LNAI 4108,
dc92e3aebc71 Improved handling of defines imported in duplicate.
ballarin
parents: 19932
diff changeset
    28
    pages 31-43, 2006.
11896
1ff33f896720 moved locale.ML to Isar/locale.ML;
wenzelm
parents:
diff changeset
    29
*)
1ff33f896720 moved locale.ML to Isar/locale.ML;
wenzelm
parents:
diff changeset
    30
16169
b59202511b8a Locales: new element constrains, parameter renaming with syntax,
ballarin
parents: 16144
diff changeset
    31
(* TODO:
b59202511b8a Locales: new element constrains, parameter renaming with syntax,
ballarin
parents: 16144
diff changeset
    32
- beta-eta normalisation of interpretation parameters
b59202511b8a Locales: new element constrains, parameter renaming with syntax,
ballarin
parents: 16144
diff changeset
    33
- dangling type frees in locales
16620
2a7f46324218 Proper treatment of beta-redexes in witness theorems.
ballarin
parents: 16458
diff changeset
    34
- test subsumption of interpretations when merging theories
16169
b59202511b8a Locales: new element constrains, parameter renaming with syntax,
ballarin
parents: 16144
diff changeset
    35
*)
b59202511b8a Locales: new element constrains, parameter renaming with syntax,
ballarin
parents: 16144
diff changeset
    36
11896
1ff33f896720 moved locale.ML to Isar/locale.ML;
wenzelm
parents:
diff changeset
    37
signature LOCALE =
1ff33f896720 moved locale.ML to Isar/locale.ML;
wenzelm
parents:
diff changeset
    38
sig
12273
7fb9840d358d beginnings of actual locale expressions;
wenzelm
parents: 12263
diff changeset
    39
  datatype expr =
7fb9840d358d beginnings of actual locale expressions;
wenzelm
parents: 12263
diff changeset
    40
    Locale of string |
16102
c5f6726d9bb1 Locale expressions: rename with optional mixfix syntax.
ballarin
parents: 16028
diff changeset
    41
    Rename of expr * (string * mixfix option) option list |
12273
7fb9840d358d beginnings of actual locale expressions;
wenzelm
parents: 12263
diff changeset
    42
    Merge of expr list
7fb9840d358d beginnings of actual locale expressions;
wenzelm
parents: 12263
diff changeset
    43
  val empty: expr
18137
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
    44
  datatype 'a element = Elem of 'a | Expr of expr
21035
326c15917a33 export map_elem;
wenzelm
parents: 21005
diff changeset
    45
  val map_elem: ('a -> 'b) -> 'a element -> 'b element
15206
09d78ec709c7 Modified locales: improved implementation of "includes".
ballarin
parents: 15127
diff changeset
    46
16458
4c6fd0c01d28 accomodate change of TheoryDataFun;
wenzelm
parents: 16346
diff changeset
    47
  val intern: theory -> xstring -> string
4c6fd0c01d28 accomodate change of TheoryDataFun;
wenzelm
parents: 16346
diff changeset
    48
  val extern: theory -> string -> xstring
19991
0c9650664d47 Locales no longer generate views. The following functions have changed
ballarin
parents: 19984
diff changeset
    49
  val init: string -> theory -> Proof.context
15206
09d78ec709c7 Modified locales: improved implementation of "includes".
ballarin
parents: 15127
diff changeset
    50
18795
303793f49b0f Interface to access the specification of a named locale.
ballarin
parents: 18782
diff changeset
    51
  (* The specification of a locale *)
303793f49b0f Interface to access the specification of a named locale.
ballarin
parents: 18782
diff changeset
    52
303793f49b0f Interface to access the specification of a named locale.
ballarin
parents: 18782
diff changeset
    53
  val parameters_of: theory -> string ->
18917
77e18862990f refined signature of locale module
haftmann
parents: 18907
diff changeset
    54
    ((string * typ) * mixfix) list
19276
ac90764bb654 New interface function parameters_of_expr.
ballarin
parents: 19061
diff changeset
    55
  val parameters_of_expr: theory -> expr ->
ac90764bb654 New interface function parameters_of_expr.
ballarin
parents: 19061
diff changeset
    56
    ((string * typ) * mixfix) list
18795
303793f49b0f Interface to access the specification of a named locale.
ballarin
parents: 18782
diff changeset
    57
  val local_asms_of: theory -> string ->
303793f49b0f Interface to access the specification of a named locale.
ballarin
parents: 18782
diff changeset
    58
    ((string * Attrib.src list) * term list) list
303793f49b0f Interface to access the specification of a named locale.
ballarin
parents: 18782
diff changeset
    59
  val global_asms_of: theory -> string ->
303793f49b0f Interface to access the specification of a named locale.
ballarin
parents: 18782
diff changeset
    60
    ((string * Attrib.src list) * term list) list
303793f49b0f Interface to access the specification of a named locale.
ballarin
parents: 18782
diff changeset
    61
18899
a8e913c93578 theorem(_in_locale): Element.statement, Obtain.statement;
wenzelm
parents: 18890
diff changeset
    62
  (* Processing of locale statements *)
18137
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
    63
  val read_context_statement: xstring option -> Element.context element list ->
19585
70a1ce3b23ae removed 'concl is' patterns;
wenzelm
parents: 19482
diff changeset
    64
    (string * string list) list list -> Proof.context ->
19991
0c9650664d47 Locales no longer generate views. The following functions have changed
ballarin
parents: 19984
diff changeset
    65
    string option * Proof.context * Proof.context * (term * term list) list list
21035
326c15917a33 export map_elem;
wenzelm
parents: 21005
diff changeset
    66
  val read_context_statement_i: string option -> Element.context element list ->
326c15917a33 export map_elem;
wenzelm
parents: 21005
diff changeset
    67
    (string * string list) list list -> Proof.context ->
326c15917a33 export map_elem;
wenzelm
parents: 21005
diff changeset
    68
    string option * Proof.context * Proof.context * (term * term list) list list
18137
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
    69
  val cert_context_statement: string option -> Element.context_i element list ->
19585
70a1ce3b23ae removed 'concl is' patterns;
wenzelm
parents: 19482
diff changeset
    70
    (term * term list) list list -> Proof.context ->
19991
0c9650664d47 Locales no longer generate views. The following functions have changed
ballarin
parents: 19984
diff changeset
    71
    string option * Proof.context * Proof.context * (term * term list) list list
19780
dce2168b0ea4 export read/cert_expr;
wenzelm
parents: 19732
diff changeset
    72
  val read_expr: expr -> Element.context list -> Proof.context ->
dce2168b0ea4 export read/cert_expr;
wenzelm
parents: 19732
diff changeset
    73
    Element.context_i list * Proof.context
dce2168b0ea4 export read/cert_expr;
wenzelm
parents: 19732
diff changeset
    74
  val cert_expr: expr -> Element.context_i list -> Proof.context ->
dce2168b0ea4 export read/cert_expr;
wenzelm
parents: 19732
diff changeset
    75
    Element.context_i list * Proof.context
15596
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
    76
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
    77
  (* Diagnostic functions *)
12758
f6aceb9d4b8e print_locale: allow full body specification;
wenzelm
parents: 12730
diff changeset
    78
  val print_locales: theory -> unit
18137
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
    79
  val print_locale: theory -> bool -> expr -> Element.context list -> unit
17138
ad4c98fd367b Interpretation in locales: extended back end;
ballarin
parents: 17109
diff changeset
    80
  val print_global_registrations: bool -> string -> theory -> unit
18617
8928e8722301 added init;
wenzelm
parents: 18569
diff changeset
    81
  val print_local_registrations': bool -> string -> Proof.context -> unit
8928e8722301 added init;
wenzelm
parents: 18569
diff changeset
    82
  val print_local_registrations: bool -> string -> Proof.context -> unit
18137
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
    83
18917
77e18862990f refined signature of locale module
haftmann
parents: 18907
diff changeset
    84
  val add_locale: bool -> bstring -> expr -> Element.context list -> theory
20965
75ffb934929d add_locale(_i): return actual result context;
wenzelm
parents: 20951
diff changeset
    85
    -> string * Proof.context
18917
77e18862990f refined signature of locale module
haftmann
parents: 18907
diff changeset
    86
  val add_locale_i: bool -> bstring -> expr -> Element.context_i list -> theory
20965
75ffb934929d add_locale(_i): return actual result context;
wenzelm
parents: 20951
diff changeset
    87
    -> string * Proof.context
15596
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
    88
21225
bf0b1e62cf60 exported intro_locales_tac
schirmer
parents: 21035
diff changeset
    89
  (* Tactics *)
bf0b1e62cf60 exported intro_locales_tac
schirmer
parents: 21035
diff changeset
    90
  val intro_locales_tac: bool -> Proof.context -> thm list -> tactic
bf0b1e62cf60 exported intro_locales_tac
schirmer
parents: 21035
diff changeset
    91
15696
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
    92
  (* Storing results *)
18806
0d2aa1cceb7d init: include view;
wenzelm
parents: 18795
diff changeset
    93
  val add_thmss: string -> string ->
0d2aa1cceb7d init: include view;
wenzelm
parents: 18795
diff changeset
    94
    ((string * Attrib.src list) * (thm list * Attrib.src list) list) list ->
21582
ac6af184bfb0 simplified add_thmss;
wenzelm
parents: 21530
diff changeset
    95
    Proof.context -> Proof.context
21665
ba07e24dc941 encode declarations as notes (attributes), which enables proper inheritance, interpretation etc.;
wenzelm
parents: 21602
diff changeset
    96
  val add_type_syntax: string -> (morphism -> Context.generic -> Context.generic) ->
21499
fbd6422a847a uniform interface for type_syntax/term_syntax/declaration, dependent on morphism;
wenzelm
parents: 21483
diff changeset
    97
    Proof.context -> Proof.context
21665
ba07e24dc941 encode declarations as notes (attributes), which enables proper inheritance, interpretation etc.;
wenzelm
parents: 21602
diff changeset
    98
  val add_term_syntax: string -> (morphism -> Context.generic -> Context.generic) ->
21499
fbd6422a847a uniform interface for type_syntax/term_syntax/declaration, dependent on morphism;
wenzelm
parents: 21483
diff changeset
    99
    Proof.context -> Proof.context
21665
ba07e24dc941 encode declarations as notes (attributes), which enables proper inheritance, interpretation etc.;
wenzelm
parents: 21602
diff changeset
   100
  val add_declaration: string -> (morphism -> Context.generic -> Context.generic) ->
21499
fbd6422a847a uniform interface for type_syntax/term_syntax/declaration, dependent on morphism;
wenzelm
parents: 21483
diff changeset
   101
    Proof.context -> Proof.context
18137
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
   102
22300
596f49b70c70 internal interfaces for interpretation and interpret
haftmann
parents: 22241
diff changeset
   103
  val interpretation_i: (Proof.context -> Proof.context) ->
596f49b70c70 internal interfaces for interpretation and interpret
haftmann
parents: 22241
diff changeset
   104
    string * Attrib.src list -> expr -> typ Symtab.table * term Symtab.table ->
596f49b70c70 internal interfaces for interpretation and interpret
haftmann
parents: 22241
diff changeset
   105
    theory -> Proof.state
21005
8f3896f0e5af interpretation_in_locale: standalone goal setup;
wenzelm
parents: 20965
diff changeset
   106
  val interpretation: (Proof.context -> Proof.context) ->
8f3896f0e5af interpretation_in_locale: standalone goal setup;
wenzelm
parents: 20965
diff changeset
   107
    string * Attrib.src list -> expr -> string option list ->
8f3896f0e5af interpretation_in_locale: standalone goal setup;
wenzelm
parents: 20965
diff changeset
   108
    theory -> Proof.state
8f3896f0e5af interpretation_in_locale: standalone goal setup;
wenzelm
parents: 20965
diff changeset
   109
  val interpretation_in_locale: (Proof.context -> Proof.context) ->
8f3896f0e5af interpretation_in_locale: standalone goal setup;
wenzelm
parents: 20965
diff changeset
   110
    xstring * expr -> theory -> Proof.state
22300
596f49b70c70 internal interfaces for interpretation and interpret
haftmann
parents: 22241
diff changeset
   111
  val interpret_i: (Proof.state -> Proof.state Seq.seq) ->
596f49b70c70 internal interfaces for interpretation and interpret
haftmann
parents: 22241
diff changeset
   112
    string * Attrib.src list -> expr -> typ Symtab.table * term Symtab.table ->
596f49b70c70 internal interfaces for interpretation and interpret
haftmann
parents: 22241
diff changeset
   113
    bool -> Proof.state -> Proof.state
21005
8f3896f0e5af interpretation_in_locale: standalone goal setup;
wenzelm
parents: 20965
diff changeset
   114
  val interpret: (Proof.state -> Proof.state Seq.seq) ->
8f3896f0e5af interpretation_in_locale: standalone goal setup;
wenzelm
parents: 20965
diff changeset
   115
    string * Attrib.src list -> expr -> string option list ->
8f3896f0e5af interpretation_in_locale: standalone goal setup;
wenzelm
parents: 20965
diff changeset
   116
    bool -> Proof.state -> Proof.state
11896
1ff33f896720 moved locale.ML to Isar/locale.ML;
wenzelm
parents:
diff changeset
   117
end;
12839
584a3e0b00f2 reorganized code for predicate text;
wenzelm
parents: 12834
diff changeset
   118
12289
ec2dafd0a6a9 clarified locale operations (rename, merge);
wenzelm
parents: 12277
diff changeset
   119
structure Locale: LOCALE =
11896
1ff33f896720 moved locale.ML to Isar/locale.ML;
wenzelm
parents:
diff changeset
   120
struct
1ff33f896720 moved locale.ML to Isar/locale.ML;
wenzelm
parents:
diff changeset
   121
19931
fb32b43e7f80 Restructured locales with predicates: import is now an interpretation.
ballarin
parents: 19914
diff changeset
   122
fun legacy_unvarifyT thm =
fb32b43e7f80 Restructured locales with predicates: import is now an interpretation.
ballarin
parents: 19914
diff changeset
   123
  let
fb32b43e7f80 Restructured locales with predicates: import is now an interpretation.
ballarin
parents: 19914
diff changeset
   124
    val cT = Thm.ctyp_of (Thm.theory_of_thm thm);
20307
a44096c94b3c removed obsolete Drule.frees/vars_of etc.;
wenzelm
parents: 20243
diff changeset
   125
    val tvars = rev (Drule.fold_terms Term.add_tvars thm []);
a44096c94b3c removed obsolete Drule.frees/vars_of etc.;
wenzelm
parents: 20243
diff changeset
   126
    val tfrees = map (fn ((x, _), S) => SOME (cT (TFree (x, S)))) tvars;
19931
fb32b43e7f80 Restructured locales with predicates: import is now an interpretation.
ballarin
parents: 19914
diff changeset
   127
  in Drule.instantiate' tfrees [] thm end;
fb32b43e7f80 Restructured locales with predicates: import is now an interpretation.
ballarin
parents: 19914
diff changeset
   128
fb32b43e7f80 Restructured locales with predicates: import is now an interpretation.
ballarin
parents: 19914
diff changeset
   129
fun legacy_unvarify raw_thm =
fb32b43e7f80 Restructured locales with predicates: import is now an interpretation.
ballarin
parents: 19914
diff changeset
   130
  let
fb32b43e7f80 Restructured locales with predicates: import is now an interpretation.
ballarin
parents: 19914
diff changeset
   131
    val thm = legacy_unvarifyT raw_thm;
fb32b43e7f80 Restructured locales with predicates: import is now an interpretation.
ballarin
parents: 19914
diff changeset
   132
    val ct = Thm.cterm_of (Thm.theory_of_thm thm);
20307
a44096c94b3c removed obsolete Drule.frees/vars_of etc.;
wenzelm
parents: 20243
diff changeset
   133
    val vars = rev (Drule.fold_terms Term.add_vars thm []);
a44096c94b3c removed obsolete Drule.frees/vars_of etc.;
wenzelm
parents: 20243
diff changeset
   134
    val frees = map (fn ((x, _), T) => SOME (ct (Free (x, T)))) vars;
19931
fb32b43e7f80 Restructured locales with predicates: import is now an interpretation.
ballarin
parents: 19914
diff changeset
   135
  in Drule.instantiate' [] frees thm end;
19780
dce2168b0ea4 export read/cert_expr;
wenzelm
parents: 19732
diff changeset
   136
20307
a44096c94b3c removed obsolete Drule.frees/vars_of etc.;
wenzelm
parents: 20243
diff changeset
   137
12273
7fb9840d358d beginnings of actual locale expressions;
wenzelm
parents: 12263
diff changeset
   138
(** locale elements and expressions **)
11896
1ff33f896720 moved locale.ML to Isar/locale.ML;
wenzelm
parents:
diff changeset
   139
18137
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
   140
datatype ctxt = datatype Element.ctxt;
17355
5b31131c0365 load late, after proof.ML;
wenzelm
parents: 17316
diff changeset
   141
12273
7fb9840d358d beginnings of actual locale expressions;
wenzelm
parents: 12263
diff changeset
   142
datatype expr =
7fb9840d358d beginnings of actual locale expressions;
wenzelm
parents: 12263
diff changeset
   143
  Locale of string |
16102
c5f6726d9bb1 Locale expressions: rename with optional mixfix syntax.
ballarin
parents: 16028
diff changeset
   144
  Rename of expr * (string * mixfix option) option list |
12273
7fb9840d358d beginnings of actual locale expressions;
wenzelm
parents: 12263
diff changeset
   145
  Merge of expr list;
11896
1ff33f896720 moved locale.ML to Isar/locale.ML;
wenzelm
parents:
diff changeset
   146
12273
7fb9840d358d beginnings of actual locale expressions;
wenzelm
parents: 12263
diff changeset
   147
val empty = Merge [];
7fb9840d358d beginnings of actual locale expressions;
wenzelm
parents: 12263
diff changeset
   148
18137
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
   149
datatype 'a element =
15206
09d78ec709c7 Modified locales: improved implementation of "includes".
ballarin
parents: 15127
diff changeset
   150
  Elem of 'a | Expr of expr;
12273
7fb9840d358d beginnings of actual locale expressions;
wenzelm
parents: 12263
diff changeset
   151
18137
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
   152
fun map_elem f (Elem e) = Elem (f e)
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
   153
  | map_elem _ (Expr e) = Expr e;
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
   154
21665
ba07e24dc941 encode declarations as notes (attributes), which enables proper inheritance, interpretation etc.;
wenzelm
parents: 21602
diff changeset
   155
type decl = (morphism -> Context.generic -> Context.generic) * stamp;
21499
fbd6422a847a uniform interface for type_syntax/term_syntax/declaration, dependent on morphism;
wenzelm
parents: 21483
diff changeset
   156
12070
c72fe1edc9e7 proper treatment of local syntax;
wenzelm
parents: 12063
diff changeset
   157
type locale =
19931
fb32b43e7f80 Restructured locales with predicates: import is now an interpretation.
ballarin
parents: 19914
diff changeset
   158
 {axiom: Element.witness list,
19942
dc92e3aebc71 Improved handling of defines imported in duplicate.
ballarin
parents: 19932
diff changeset
   159
    (* For locales that define predicates this is [A [A]], where A is the locale
20317
6e070b33e72b Updated comments.
ballarin
parents: 20307
diff changeset
   160
       specification.  Otherwise [].
6e070b33e72b Updated comments.
ballarin
parents: 20307
diff changeset
   161
       Only required to generate the right witnesses for locales with predicates. *)
19018
88b4979193d8 added abbreviations: activated by init, no expressions yet;
wenzelm
parents: 18964
diff changeset
   162
  import: expr,                                                     (*dynamic import*)
19783
82f365a14960 Improved parameter management of locales.
ballarin
parents: 19780
diff changeset
   163
  elems: (Element.context_i * stamp) list,
82f365a14960 Improved parameter management of locales.
ballarin
parents: 19780
diff changeset
   164
    (* Static content, neither Fixes nor Constrains elements *)
21499
fbd6422a847a uniform interface for type_syntax/term_syntax/declaration, dependent on morphism;
wenzelm
parents: 21483
diff changeset
   165
  params: ((string * typ) * mixfix) list,                             (*all params*)
19931
fb32b43e7f80 Restructured locales with predicates: import is now an interpretation.
ballarin
parents: 19914
diff changeset
   166
  lparams: string list,                                             (*local params*)
21665
ba07e24dc941 encode declarations as notes (attributes), which enables proper inheritance, interpretation etc.;
wenzelm
parents: 21602
diff changeset
   167
  decls: decl list * decl list,                    (*type/term_syntax declarations*)
19931
fb32b43e7f80 Restructured locales with predicates: import is now an interpretation.
ballarin
parents: 19914
diff changeset
   168
  regs: ((string * string list) * Element.witness list) list,
19780
dce2168b0ea4 export read/cert_expr;
wenzelm
parents: 19732
diff changeset
   169
    (* Registrations: indentifiers and witnesses of locales interpreted in the locale. *)
19931
fb32b43e7f80 Restructured locales with predicates: import is now an interpretation.
ballarin
parents: 19914
diff changeset
   170
  intros: thm list * thm list}
fb32b43e7f80 Restructured locales with predicates: import is now an interpretation.
ballarin
parents: 19914
diff changeset
   171
    (* Introduction rules: of delta predicate and locale predicate. *)
11896
1ff33f896720 moved locale.ML to Isar/locale.ML;
wenzelm
parents:
diff changeset
   172
15703
727ef1b8b3ee *** empty log message ***
wenzelm
parents: 15696
diff changeset
   173
(* CB: an internal (Int) locale element was either imported or included,
727ef1b8b3ee *** empty log message ***
wenzelm
parents: 15696
diff changeset
   174
   an external (Ext) element appears directly in the locale text. *)
727ef1b8b3ee *** empty log message ***
wenzelm
parents: 15696
diff changeset
   175
727ef1b8b3ee *** empty log message ***
wenzelm
parents: 15696
diff changeset
   176
datatype ('a, 'b) int_ext = Int of 'a | Ext of 'b;
727ef1b8b3ee *** empty log message ***
wenzelm
parents: 15696
diff changeset
   177
727ef1b8b3ee *** empty log message ***
wenzelm
parents: 15696
diff changeset
   178
727ef1b8b3ee *** empty log message ***
wenzelm
parents: 15696
diff changeset
   179
16736
1e792b32abef Preparations for interpretation of locales in locales.
ballarin
parents: 16620
diff changeset
   180
(** management of registrations in theories and proof contexts **)
11896
1ff33f896720 moved locale.ML to Isar/locale.ML;
wenzelm
parents:
diff changeset
   181
15837
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   182
structure Registrations :
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   183
  sig
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   184
    type T
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   185
    val empty: T
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   186
    val join: T * T -> T
20069
77a6b62418bb Witness theorems of interpretations now transfered to current theory.
ballarin
parents: 20059
diff changeset
   187
    val dest: theory -> T ->
77a6b62418bb Witness theorems of interpretations now transfered to current theory.
ballarin
parents: 20059
diff changeset
   188
      (term list * ((string * Attrib.src list) * Element.witness list)) list
16458
4c6fd0c01d28 accomodate change of TheoryDataFun;
wenzelm
parents: 16346
diff changeset
   189
    val lookup: theory -> T * term list ->
19780
dce2168b0ea4 export read/cert_expr;
wenzelm
parents: 19732
diff changeset
   190
      ((string * Attrib.src list) * Element.witness list) option
16458
4c6fd0c01d28 accomodate change of TheoryDataFun;
wenzelm
parents: 16346
diff changeset
   191
    val insert: theory -> term list * (string * Attrib.src list) -> T ->
19780
dce2168b0ea4 export read/cert_expr;
wenzelm
parents: 19732
diff changeset
   192
      T * (term list * ((string * Attrib.src list) * Element.witness list)) list
dce2168b0ea4 export read/cert_expr;
wenzelm
parents: 19732
diff changeset
   193
    val add_witness: term list -> Element.witness -> T -> T
15837
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   194
  end =
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   195
struct
20069
77a6b62418bb Witness theorems of interpretations now transfered to current theory.
ballarin
parents: 20059
diff changeset
   196
  (* a registration consists of theorems (actually, witnesses) instantiating locale
77a6b62418bb Witness theorems of interpretations now transfered to current theory.
ballarin
parents: 20059
diff changeset
   197
     assumptions and prefix and attributes, indexed by parameter instantiation *)
19780
dce2168b0ea4 export read/cert_expr;
wenzelm
parents: 19732
diff changeset
   198
  type T = ((string * Attrib.src list) * Element.witness list) Termtab.table;
15837
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   199
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   200
  val empty = Termtab.empty;
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   201
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   202
  (* term list represented as single term, for simultaneous matching *)
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   203
  fun termify ts =
18343
e36238ac5359 defines: beta/eta contract lhs;
wenzelm
parents: 18330
diff changeset
   204
    Term.list_comb (Const ("", map fastype_of ts ---> propT), ts);
15837
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   205
  fun untermify t =
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   206
    let fun ut (Const _) ts = ts
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   207
          | ut (s $ t) ts = ut s (t::ts)
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   208
    in ut t [] end;
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   209
16620
2a7f46324218 Proper treatment of beta-redexes in witness theorems.
ballarin
parents: 16458
diff changeset
   210
  (* joining of registrations: prefix and attributes of left theory,
15837
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   211
     thms are equal, no attempt to subsumption testing *)
19025
596fb1eb7856 simplified TableFun.join;
wenzelm
parents: 19018
diff changeset
   212
  fun join (r1, r2) = Termtab.join (fn _ => fn (reg, _) => reg) (r1, r2);
15837
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   213
20069
77a6b62418bb Witness theorems of interpretations now transfered to current theory.
ballarin
parents: 20059
diff changeset
   214
  fun dest_transfer thy regs =
77a6b62418bb Witness theorems of interpretations now transfered to current theory.
ballarin
parents: 20059
diff changeset
   215
    Termtab.dest regs |> map (apsnd (apsnd (map (Element.transfer_witness thy))));
77a6b62418bb Witness theorems of interpretations now transfered to current theory.
ballarin
parents: 20059
diff changeset
   216
77a6b62418bb Witness theorems of interpretations now transfered to current theory.
ballarin
parents: 20059
diff changeset
   217
  fun dest thy regs = dest_transfer thy regs |> map (apfst untermify);
15837
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   218
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   219
  (* registrations that subsume t *)
17203
29b2563f5c11 refer to theory instead of low-level tsig;
wenzelm
parents: 17142
diff changeset
   220
  fun subsumers thy t regs =
20069
77a6b62418bb Witness theorems of interpretations now transfered to current theory.
ballarin
parents: 20059
diff changeset
   221
    filter (fn (t', _) => Pattern.matches thy (t', t)) (dest_transfer thy regs);
15837
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   222
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   223
  (* look up registration, pick one that subsumes the query *)
19780
dce2168b0ea4 export read/cert_expr;
wenzelm
parents: 19732
diff changeset
   224
  fun lookup thy (regs, ts) =
15837
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   225
    let
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   226
      val t = termify ts;
19780
dce2168b0ea4 export read/cert_expr;
wenzelm
parents: 19732
diff changeset
   227
      val subs = subsumers thy t regs;
21483
e4be91feca50 replaced Args.map_values/Element.map_ctxt_values by general morphism application;
wenzelm
parents: 21441
diff changeset
   228
    in
e4be91feca50 replaced Args.map_values/Element.map_ctxt_values by general morphism application;
wenzelm
parents: 21441
diff changeset
   229
      (case subs of
15837
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   230
        [] => NONE
21483
e4be91feca50 replaced Args.map_values/Element.map_ctxt_values by general morphism application;
wenzelm
parents: 21441
diff changeset
   231
      | ((t', (attn, thms)) :: _) =>
e4be91feca50 replaced Args.map_values/Element.map_ctxt_values by general morphism application;
wenzelm
parents: 21441
diff changeset
   232
          let
19780
dce2168b0ea4 export read/cert_expr;
wenzelm
parents: 19732
diff changeset
   233
            val (tinst, inst) = Pattern.match thy (t', t) (Vartab.empty, Vartab.empty);
15837
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   234
            (* thms contain Frees, not Vars *)
21665
ba07e24dc941 encode declarations as notes (attributes), which enables proper inheritance, interpretation etc.;
wenzelm
parents: 21602
diff changeset
   235
            val tinst' = tinst |> Vartab.dest   (* FIXME Vartab.map (!?) *)
19810
dae765e552ce renamed Type.(un)varifyT to Logic.(un)varifyT;
wenzelm
parents: 19783
diff changeset
   236
                 |> map (fn ((x, 0), (_, T)) => (x, Logic.legacy_unvarifyT T))
15837
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   237
                 |> Symtab.make;
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   238
            val inst' = inst |> Vartab.dest
19810
dae765e552ce renamed Type.(un)varifyT to Logic.(un)varifyT;
wenzelm
parents: 19783
diff changeset
   239
                 |> map (fn ((x, 0), (_, t)) => (x, Logic.legacy_unvarify t))
15837
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   240
                 |> Symtab.make;
21483
e4be91feca50 replaced Args.map_values/Element.map_ctxt_values by general morphism application;
wenzelm
parents: 21441
diff changeset
   241
            val inst_witness = Element.morph_witness (Element.inst_morphism thy (tinst', inst'));
e4be91feca50 replaced Args.map_values/Element.map_ctxt_values by general morphism application;
wenzelm
parents: 21441
diff changeset
   242
          in SOME (attn, map inst_witness thms) end)
15837
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   243
    end;
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   244
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   245
  (* add registration if not subsumed by ones already present,
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   246
     additionally returns registrations that are strictly subsumed *)
20069
77a6b62418bb Witness theorems of interpretations now transfered to current theory.
ballarin
parents: 20059
diff changeset
   247
  fun insert thy (ts, attn) regs =
15837
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   248
    let
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   249
      val t = termify ts;
20069
77a6b62418bb Witness theorems of interpretations now transfered to current theory.
ballarin
parents: 20059
diff changeset
   250
      val subs = subsumers thy t regs ;
15837
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   251
    in (case subs of
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   252
        [] => let
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   253
                val sups =
20069
77a6b62418bb Witness theorems of interpretations now transfered to current theory.
ballarin
parents: 20059
diff changeset
   254
                  filter (fn (t', _) => Pattern.matches thy (t, t')) (dest_transfer thy regs);
15837
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   255
                val sups' = map (apfst untermify) sups
17412
e26cb20ef0cc TableFun/Symtab: curried lookup and update;
wenzelm
parents: 17384
diff changeset
   256
              in (Termtab.update (t, (attn, [])) regs, sups') end
15837
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   257
      | _ => (regs, []))
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   258
    end;
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   259
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   260
  (* add witness theorem to registration,
16169
b59202511b8a Locales: new element constrains, parameter renaming with syntax,
ballarin
parents: 16144
diff changeset
   261
     only if instantiation is exact, otherwise exception Option raised *)
15837
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   262
  fun add_witness ts thm regs =
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   263
    let
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   264
      val t = termify ts;
18343
e36238ac5359 defines: beta/eta contract lhs;
wenzelm
parents: 18330
diff changeset
   265
      val (x, thms) = the (Termtab.lookup regs t);
15837
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   266
    in
17412
e26cb20ef0cc TableFun/Symtab: curried lookup and update;
wenzelm
parents: 17384
diff changeset
   267
      Termtab.update (t, (x, thm::thms)) regs
15837
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   268
    end;
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   269
end;
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   270
16736
1e792b32abef Preparations for interpretation of locales in locales.
ballarin
parents: 16620
diff changeset
   271
15837
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   272
(** theory data **)
15596
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
   273
16458
4c6fd0c01d28 accomodate change of TheoryDataFun;
wenzelm
parents: 16346
diff changeset
   274
structure GlobalLocalesData = TheoryDataFun
4c6fd0c01d28 accomodate change of TheoryDataFun;
wenzelm
parents: 16346
diff changeset
   275
(struct
12014
035ab884b9e0 beginnings of new locales (not yet functional);
wenzelm
parents: 11896
diff changeset
   276
  val name = "Isar/locales";
15837
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   277
  type T = NameSpace.T * locale Symtab.table * Registrations.T Symtab.table;
15596
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
   278
    (* 1st entry: locale namespace,
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
   279
       2nd entry: locales of the theory,
15837
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   280
       3rd entry: registrations, indexed by locale name *)
11896
1ff33f896720 moved locale.ML to Isar/locale.ML;
wenzelm
parents:
diff changeset
   281
15596
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
   282
  val empty = (NameSpace.empty, Symtab.empty, Symtab.empty);
12063
4c16bdee47d4 added add_locale(_i) and store_thm;
wenzelm
parents: 12058
diff changeset
   283
  val copy = I;
16458
4c6fd0c01d28 accomodate change of TheoryDataFun;
wenzelm
parents: 16346
diff changeset
   284
  val extend = I;
12289
ec2dafd0a6a9 clarified locale operations (rename, merge);
wenzelm
parents: 12277
diff changeset
   285
21665
ba07e24dc941 encode declarations as notes (attributes), which enables proper inheritance, interpretation etc.;
wenzelm
parents: 21602
diff changeset
   286
  fun join_locales _
ba07e24dc941 encode declarations as notes (attributes), which enables proper inheritance, interpretation etc.;
wenzelm
parents: 21602
diff changeset
   287
    ({axiom, import, elems, params, lparams, decls = (decls1, decls2), regs, intros}: locale,
ba07e24dc941 encode declarations as notes (attributes), which enables proper inheritance, interpretation etc.;
wenzelm
parents: 21602
diff changeset
   288
      {elems = elems', decls = (decls1', decls2'), regs = regs', ...}: locale) =
19931
fb32b43e7f80 Restructured locales with predicates: import is now an interpretation.
ballarin
parents: 19914
diff changeset
   289
     {axiom = axiom,
19018
88b4979193d8 added abbreviations: activated by init, no expressions yet;
wenzelm
parents: 18964
diff changeset
   290
      import = import,
17496
26535df536ae slight adaptions to library changes
haftmann
parents: 17485
diff changeset
   291
      elems = gen_merge_lists (eq_snd (op =)) elems elems',
16736
1e792b32abef Preparations for interpretation of locales in locales.
ballarin
parents: 16620
diff changeset
   292
      params = params,
19278
4d762b77d319 Internal restructuring: local parameters.
ballarin
parents: 19276
diff changeset
   293
      lparams = lparams,
21499
fbd6422a847a uniform interface for type_syntax/term_syntax/declaration, dependent on morphism;
wenzelm
parents: 21483
diff changeset
   294
      decls =
21665
ba07e24dc941 encode declarations as notes (attributes), which enables proper inheritance, interpretation etc.;
wenzelm
parents: 21602
diff changeset
   295
       (Library.merge (eq_snd (op =)) (decls1, decls1'),
ba07e24dc941 encode declarations as notes (attributes), which enables proper inheritance, interpretation etc.;
wenzelm
parents: 21602
diff changeset
   296
        Library.merge (eq_snd (op =)) (decls2, decls2')),
19931
fb32b43e7f80 Restructured locales with predicates: import is now an interpretation.
ballarin
parents: 19914
diff changeset
   297
      regs = merge_alists regs regs',
fb32b43e7f80 Restructured locales with predicates: import is now an interpretation.
ballarin
parents: 19914
diff changeset
   298
      intros = intros};
16458
4c6fd0c01d28 accomodate change of TheoryDataFun;
wenzelm
parents: 16346
diff changeset
   299
  fun merge _ ((space1, locs1, regs1), (space2, locs2, regs2)) =
21499
fbd6422a847a uniform interface for type_syntax/term_syntax/declaration, dependent on morphism;
wenzelm
parents: 21483
diff changeset
   300
    (NameSpace.merge (space1, space2), Symtab.join join_locales (locs1, locs2),
19025
596fb1eb7856 simplified TableFun.join;
wenzelm
parents: 19018
diff changeset
   301
     Symtab.join (K Registrations.join) (regs1, regs2));
12289
ec2dafd0a6a9 clarified locale operations (rename, merge);
wenzelm
parents: 12277
diff changeset
   302
15596
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
   303
  fun print _ (space, locs, _) =
16346
baa7b5324fc1 NameSpace.extern_table;
wenzelm
parents: 16325
diff changeset
   304
    Pretty.strs ("locales:" :: map #1 (NameSpace.extern_table (space, locs)))
12014
035ab884b9e0 beginnings of new locales (not yet functional);
wenzelm
parents: 11896
diff changeset
   305
    |> Pretty.writeln;
16458
4c6fd0c01d28 accomodate change of TheoryDataFun;
wenzelm
parents: 16346
diff changeset
   306
end);
11896
1ff33f896720 moved locale.ML to Isar/locale.ML;
wenzelm
parents:
diff changeset
   307
18708
4b3dadb4fe33 setup: theory -> theory;
wenzelm
parents: 18698
diff changeset
   308
val _ = Context.add_setup GlobalLocalesData.init;
15801
d2f5ca3c048d superceded by Pure.thy and CPure.thy;
wenzelm
parents: 15798
diff changeset
   309
d2f5ca3c048d superceded by Pure.thy and CPure.thy;
wenzelm
parents: 15798
diff changeset
   310
15624
484178635bd8 Further work on interpretation commands. New command `interpret' for
ballarin
parents: 15623
diff changeset
   311
484178635bd8 Further work on interpretation commands. New command `interpret' for
ballarin
parents: 15623
diff changeset
   312
(** context data **)
11896
1ff33f896720 moved locale.ML to Isar/locale.ML;
wenzelm
parents:
diff changeset
   313
16458
4c6fd0c01d28 accomodate change of TheoryDataFun;
wenzelm
parents: 16346
diff changeset
   314
structure LocalLocalesData = ProofDataFun
4c6fd0c01d28 accomodate change of TheoryDataFun;
wenzelm
parents: 16346
diff changeset
   315
(struct
15624
484178635bd8 Further work on interpretation commands. New command `interpret' for
ballarin
parents: 15623
diff changeset
   316
  val name = "Isar/locales";
15837
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   317
  type T = Registrations.T Symtab.table;
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   318
    (* registrations, indexed by locale name *)
15624
484178635bd8 Further work on interpretation commands. New command `interpret' for
ballarin
parents: 15623
diff changeset
   319
  fun init _ = Symtab.empty;
484178635bd8 Further work on interpretation commands. New command `interpret' for
ballarin
parents: 15623
diff changeset
   320
  fun print _ _ = ();
16458
4c6fd0c01d28 accomodate change of TheoryDataFun;
wenzelm
parents: 16346
diff changeset
   321
end);
15624
484178635bd8 Further work on interpretation commands. New command `interpret' for
ballarin
parents: 15623
diff changeset
   322
18708
4b3dadb4fe33 setup: theory -> theory;
wenzelm
parents: 18698
diff changeset
   323
val _ = Context.add_setup LocalLocalesData.init;
12289
ec2dafd0a6a9 clarified locale operations (rename, merge);
wenzelm
parents: 12277
diff changeset
   324
12277
2b28d7dd91f5 improved ordering of evaluated elements;
wenzelm
parents: 12273
diff changeset
   325
2b28d7dd91f5 improved ordering of evaluated elements;
wenzelm
parents: 12273
diff changeset
   326
(* access locales *)
2b28d7dd91f5 improved ordering of evaluated elements;
wenzelm
parents: 12273
diff changeset
   327
15624
484178635bd8 Further work on interpretation commands. New command `interpret' for
ballarin
parents: 15623
diff changeset
   328
val print_locales = GlobalLocalesData.print;
484178635bd8 Further work on interpretation commands. New command `interpret' for
ballarin
parents: 15623
diff changeset
   329
16458
4c6fd0c01d28 accomodate change of TheoryDataFun;
wenzelm
parents: 16346
diff changeset
   330
val intern = NameSpace.intern o #1 o GlobalLocalesData.get;
4c6fd0c01d28 accomodate change of TheoryDataFun;
wenzelm
parents: 16346
diff changeset
   331
val extern = NameSpace.extern o #1 o GlobalLocalesData.get;
15624
484178635bd8 Further work on interpretation commands. New command `interpret' for
ballarin
parents: 15623
diff changeset
   332
16144
e339119f4261 renamed cond_extern to extern;
wenzelm
parents: 16105
diff changeset
   333
fun declare_locale name thy =
e339119f4261 renamed cond_extern to extern;
wenzelm
parents: 16105
diff changeset
   334
  thy |> GlobalLocalesData.map (fn (space, locs, regs) =>
16458
4c6fd0c01d28 accomodate change of TheoryDataFun;
wenzelm
parents: 16346
diff changeset
   335
    (Sign.declare_name thy name space, locs, regs));
11896
1ff33f896720 moved locale.ML to Isar/locale.ML;
wenzelm
parents:
diff changeset
   336
15596
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
   337
fun put_locale name loc =
15624
484178635bd8 Further work on interpretation commands. New command `interpret' for
ballarin
parents: 15623
diff changeset
   338
  GlobalLocalesData.map (fn (space, locs, regs) =>
17412
e26cb20ef0cc TableFun/Symtab: curried lookup and update;
wenzelm
parents: 17384
diff changeset
   339
    (space, Symtab.update (name, loc) locs, regs));
e26cb20ef0cc TableFun/Symtab: curried lookup and update;
wenzelm
parents: 17384
diff changeset
   340
e26cb20ef0cc TableFun/Symtab: curried lookup and update;
wenzelm
parents: 17384
diff changeset
   341
fun get_locale thy name = Symtab.lookup (#2 (GlobalLocalesData.get thy)) name;
11896
1ff33f896720 moved locale.ML to Isar/locale.ML;
wenzelm
parents:
diff changeset
   342
12014
035ab884b9e0 beginnings of new locales (not yet functional);
wenzelm
parents: 11896
diff changeset
   343
fun the_locale thy name =
035ab884b9e0 beginnings of new locales (not yet functional);
wenzelm
parents: 11896
diff changeset
   344
  (case get_locale thy name of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15456
diff changeset
   345
    SOME loc => loc
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15456
diff changeset
   346
  | NONE => error ("Unknown locale " ^ quote name));
11896
1ff33f896720 moved locale.ML to Isar/locale.ML;
wenzelm
parents:
diff changeset
   347
18806
0d2aa1cceb7d init: include view;
wenzelm
parents: 18795
diff changeset
   348
fun change_locale name f thy =
0d2aa1cceb7d init: include view;
wenzelm
parents: 18795
diff changeset
   349
  let
21499
fbd6422a847a uniform interface for type_syntax/term_syntax/declaration, dependent on morphism;
wenzelm
parents: 21483
diff changeset
   350
    val {axiom, import, elems, params, lparams, decls, regs, intros} =
19931
fb32b43e7f80 Restructured locales with predicates: import is now an interpretation.
ballarin
parents: 19914
diff changeset
   351
        the_locale thy name;
21499
fbd6422a847a uniform interface for type_syntax/term_syntax/declaration, dependent on morphism;
wenzelm
parents: 21483
diff changeset
   352
    val (axiom', import', elems', params', lparams', decls', regs', intros') =
fbd6422a847a uniform interface for type_syntax/term_syntax/declaration, dependent on morphism;
wenzelm
parents: 21483
diff changeset
   353
      f (axiom, import, elems, params, lparams, decls, regs, intros);
18806
0d2aa1cceb7d init: include view;
wenzelm
parents: 18795
diff changeset
   354
  in
19931
fb32b43e7f80 Restructured locales with predicates: import is now an interpretation.
ballarin
parents: 19914
diff changeset
   355
    put_locale name {axiom = axiom', import = import', elems = elems',
21499
fbd6422a847a uniform interface for type_syntax/term_syntax/declaration, dependent on morphism;
wenzelm
parents: 21483
diff changeset
   356
      params = params', lparams = lparams', decls = decls', regs = regs',
19931
fb32b43e7f80 Restructured locales with predicates: import is now an interpretation.
ballarin
parents: 19914
diff changeset
   357
      intros = intros'} thy
18806
0d2aa1cceb7d init: include view;
wenzelm
parents: 18795
diff changeset
   358
  end;
0d2aa1cceb7d init: include view;
wenzelm
parents: 18795
diff changeset
   359
12046
a404358fd965 locale elements;
wenzelm
parents: 12014
diff changeset
   360
15596
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
   361
(* access registrations *)
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
   362
15696
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   363
(* Ids of global registrations are varified,
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   364
   Ids of local registrations are not.
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   365
   Thms of registrations are never varified. *)
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   366
15624
484178635bd8 Further work on interpretation commands. New command `interpret' for
ballarin
parents: 15623
diff changeset
   367
(* retrieve registration from theory or context *)
484178635bd8 Further work on interpretation commands. New command `interpret' for
ballarin
parents: 15623
diff changeset
   368
20069
77a6b62418bb Witness theorems of interpretations now transfered to current theory.
ballarin
parents: 20059
diff changeset
   369
fun gen_get_registrations get thy_of thy_ctxt name =
17412
e26cb20ef0cc TableFun/Symtab: curried lookup and update;
wenzelm
parents: 17384
diff changeset
   370
  case Symtab.lookup (get thy_ctxt) name of
15696
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   371
      NONE => []
20069
77a6b62418bb Witness theorems of interpretations now transfered to current theory.
ballarin
parents: 20059
diff changeset
   372
    | SOME reg => Registrations.dest (thy_of thy_ctxt) reg;
15696
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   373
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   374
val get_global_registrations =
20069
77a6b62418bb Witness theorems of interpretations now transfered to current theory.
ballarin
parents: 20059
diff changeset
   375
     gen_get_registrations (#3 o GlobalLocalesData.get) I;
15696
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   376
val get_local_registrations =
20069
77a6b62418bb Witness theorems of interpretations now transfered to current theory.
ballarin
parents: 20059
diff changeset
   377
     gen_get_registrations LocalLocalesData.get ProofContext.theory_of;
15696
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   378
16458
4c6fd0c01d28 accomodate change of TheoryDataFun;
wenzelm
parents: 16346
diff changeset
   379
fun gen_get_registration get thy_of thy_ctxt (name, ps) =
17412
e26cb20ef0cc TableFun/Symtab: curried lookup and update;
wenzelm
parents: 17384
diff changeset
   380
  case Symtab.lookup (get thy_ctxt) name of
15624
484178635bd8 Further work on interpretation commands. New command `interpret' for
ballarin
parents: 15623
diff changeset
   381
      NONE => NONE
16458
4c6fd0c01d28 accomodate change of TheoryDataFun;
wenzelm
parents: 16346
diff changeset
   382
    | SOME reg => Registrations.lookup (thy_of thy_ctxt) (reg, ps);
15624
484178635bd8 Further work on interpretation commands. New command `interpret' for
ballarin
parents: 15623
diff changeset
   383
484178635bd8 Further work on interpretation commands. New command `interpret' for
ballarin
parents: 15623
diff changeset
   384
val get_global_registration =
16458
4c6fd0c01d28 accomodate change of TheoryDataFun;
wenzelm
parents: 16346
diff changeset
   385
     gen_get_registration (#3 o GlobalLocalesData.get) I;
15624
484178635bd8 Further work on interpretation commands. New command `interpret' for
ballarin
parents: 15623
diff changeset
   386
val get_local_registration =
16458
4c6fd0c01d28 accomodate change of TheoryDataFun;
wenzelm
parents: 16346
diff changeset
   387
     gen_get_registration LocalLocalesData.get ProofContext.theory_of;
15596
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
   388
18343
e36238ac5359 defines: beta/eta contract lhs;
wenzelm
parents: 18330
diff changeset
   389
val test_global_registration = is_some oo get_global_registration;
e36238ac5359 defines: beta/eta contract lhs;
wenzelm
parents: 18330
diff changeset
   390
val test_local_registration = is_some oo get_local_registration;
15624
484178635bd8 Further work on interpretation commands. New command `interpret' for
ballarin
parents: 15623
diff changeset
   391
fun smart_test_registration ctxt id =
484178635bd8 Further work on interpretation commands. New command `interpret' for
ballarin
parents: 15623
diff changeset
   392
  let
484178635bd8 Further work on interpretation commands. New command `interpret' for
ballarin
parents: 15623
diff changeset
   393
    val thy = ProofContext.theory_of ctxt;
484178635bd8 Further work on interpretation commands. New command `interpret' for
ballarin
parents: 15623
diff changeset
   394
  in
484178635bd8 Further work on interpretation commands. New command `interpret' for
ballarin
parents: 15623
diff changeset
   395
    test_global_registration thy id orelse test_local_registration ctxt id
484178635bd8 Further work on interpretation commands. New command `interpret' for
ballarin
parents: 15623
diff changeset
   396
  end;
484178635bd8 Further work on interpretation commands. New command `interpret' for
ballarin
parents: 15623
diff changeset
   397
484178635bd8 Further work on interpretation commands. New command `interpret' for
ballarin
parents: 15623
diff changeset
   398
15837
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   399
(* add registration to theory or context, ignored if subsumed *)
15624
484178635bd8 Further work on interpretation commands. New command `interpret' for
ballarin
parents: 15623
diff changeset
   400
16458
4c6fd0c01d28 accomodate change of TheoryDataFun;
wenzelm
parents: 16346
diff changeset
   401
fun gen_put_registration map_data thy_of (name, ps) attn thy_ctxt =
15837
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   402
  map_data (fn regs =>
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   403
    let
16458
4c6fd0c01d28 accomodate change of TheoryDataFun;
wenzelm
parents: 16346
diff changeset
   404
      val thy = thy_of thy_ctxt;
18343
e36238ac5359 defines: beta/eta contract lhs;
wenzelm
parents: 18330
diff changeset
   405
      val reg = the_default Registrations.empty (Symtab.lookup regs name);
16458
4c6fd0c01d28 accomodate change of TheoryDataFun;
wenzelm
parents: 16346
diff changeset
   406
      val (reg', sups) = Registrations.insert thy (ps, attn) reg;
15837
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   407
      val _ = if not (null sups) then warning
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   408
                ("Subsumed interpretation(s) of locale " ^
16458
4c6fd0c01d28 accomodate change of TheoryDataFun;
wenzelm
parents: 16346
diff changeset
   409
                 quote (extern thy name) ^
15837
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   410
                 "\nby interpretation(s) with the following prefix(es):\n" ^
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   411
                  commas_quote (map (fn (_, ((s, _), _)) => s) sups))
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   412
              else ();
17412
e26cb20ef0cc TableFun/Symtab: curried lookup and update;
wenzelm
parents: 17384
diff changeset
   413
    in Symtab.update (name, reg') regs end) thy_ctxt;
15624
484178635bd8 Further work on interpretation commands. New command `interpret' for
ballarin
parents: 15623
diff changeset
   414
484178635bd8 Further work on interpretation commands. New command `interpret' for
ballarin
parents: 15623
diff changeset
   415
val put_global_registration =
484178635bd8 Further work on interpretation commands. New command `interpret' for
ballarin
parents: 15623
diff changeset
   416
     gen_put_registration (fn f =>
16458
4c6fd0c01d28 accomodate change of TheoryDataFun;
wenzelm
parents: 16346
diff changeset
   417
       GlobalLocalesData.map (fn (space, locs, regs) => (space, locs, f regs))) I;
15837
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   418
val put_local_registration =
16458
4c6fd0c01d28 accomodate change of TheoryDataFun;
wenzelm
parents: 16346
diff changeset
   419
     gen_put_registration LocalLocalesData.map ProofContext.theory_of;
15596
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
   420
18806
0d2aa1cceb7d init: include view;
wenzelm
parents: 18795
diff changeset
   421
fun put_registration_in_locale name id =
21499
fbd6422a847a uniform interface for type_syntax/term_syntax/declaration, dependent on morphism;
wenzelm
parents: 21483
diff changeset
   422
  change_locale name (fn (axiom, import, elems, params, lparams, decls, regs, intros) =>
fbd6422a847a uniform interface for type_syntax/term_syntax/declaration, dependent on morphism;
wenzelm
parents: 21483
diff changeset
   423
    (axiom, import, elems, params, lparams, decls, regs @ [(id, [])], intros));
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   424
15624
484178635bd8 Further work on interpretation commands. New command `interpret' for
ballarin
parents: 15623
diff changeset
   425
484178635bd8 Further work on interpretation commands. New command `interpret' for
ballarin
parents: 15623
diff changeset
   426
(* add witness theorem to registration in theory or context,
15596
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
   427
   ignored if registration not present *)
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
   428
18123
1bb572e8cee9 avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents: 18038
diff changeset
   429
fun add_witness (name, ps) thm =
1bb572e8cee9 avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents: 18038
diff changeset
   430
  Symtab.map_entry name (Registrations.add_witness ps thm);
1bb572e8cee9 avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents: 18038
diff changeset
   431
1bb572e8cee9 avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents: 18038
diff changeset
   432
fun add_global_witness id thm =
1bb572e8cee9 avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents: 18038
diff changeset
   433
  GlobalLocalesData.map (fn (space, locs, regs) => (space, locs, add_witness id thm regs));
1bb572e8cee9 avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents: 18038
diff changeset
   434
1bb572e8cee9 avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents: 18038
diff changeset
   435
val add_local_witness = LocalLocalesData.map oo add_witness;
15596
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
   436
18806
0d2aa1cceb7d init: include view;
wenzelm
parents: 18795
diff changeset
   437
fun add_witness_in_locale name id thm =
21499
fbd6422a847a uniform interface for type_syntax/term_syntax/declaration, dependent on morphism;
wenzelm
parents: 21483
diff changeset
   438
  change_locale name (fn (axiom, import, elems, params, lparams, decls, regs, intros) =>
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   439
    let
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   440
      fun add (id', thms) =
18806
0d2aa1cceb7d init: include view;
wenzelm
parents: 18795
diff changeset
   441
        if id = id' then (id', thm :: thms) else (id', thms);
21499
fbd6422a847a uniform interface for type_syntax/term_syntax/declaration, dependent on morphism;
wenzelm
parents: 21483
diff changeset
   442
    in (axiom, import, elems, params, lparams, decls, map add regs, intros) end);
15596
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
   443
14215
ebf291f3b449 Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents: 13629
diff changeset
   444
15624
484178635bd8 Further work on interpretation commands. New command `interpret' for
ballarin
parents: 15623
diff changeset
   445
(* printing of registrations *)
15596
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
   446
17138
ad4c98fd367b Interpretation in locales: extended back end;
ballarin
parents: 17109
diff changeset
   447
fun gen_print_registrations get_regs mk_ctxt msg show_wits loc thy_ctxt =
15596
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
   448
  let
15703
727ef1b8b3ee *** empty log message ***
wenzelm
parents: 15696
diff changeset
   449
    val ctxt = mk_ctxt thy_ctxt;
727ef1b8b3ee *** empty log message ***
wenzelm
parents: 15696
diff changeset
   450
    val thy = ProofContext.theory_of ctxt;
727ef1b8b3ee *** empty log message ***
wenzelm
parents: 15696
diff changeset
   451
727ef1b8b3ee *** empty log message ***
wenzelm
parents: 15696
diff changeset
   452
    val prt_term = Pretty.quote o ProofContext.pretty_term ctxt;
17096
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   453
    fun prt_inst ts =
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   454
        Pretty.enclose "(" ")" (Pretty.breaks (map prt_term ts));
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   455
    fun prt_attn (prfx, atts) =
21035
326c15917a33 export map_elem;
wenzelm
parents: 21005
diff changeset
   456
        Pretty.breaks (Pretty.str prfx :: Attrib.pretty_attribs ctxt atts);
19780
dce2168b0ea4 export read/cert_expr;
wenzelm
parents: 19732
diff changeset
   457
    fun prt_witns witns = Pretty.enclose "[" "]"
dce2168b0ea4 export read/cert_expr;
wenzelm
parents: 19732
diff changeset
   458
      (Pretty.breaks (map (prt_term o Element.witness_prop) witns));
dce2168b0ea4 export read/cert_expr;
wenzelm
parents: 19732
diff changeset
   459
    fun prt_reg (ts, (("", []), witns)) =
17138
ad4c98fd367b Interpretation in locales: extended back end;
ballarin
parents: 17109
diff changeset
   460
        if show_wits
19780
dce2168b0ea4 export read/cert_expr;
wenzelm
parents: 19732
diff changeset
   461
          then Pretty.block [prt_inst ts, Pretty.fbrk, prt_witns witns]
17096
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   462
          else prt_inst ts
19780
dce2168b0ea4 export read/cert_expr;
wenzelm
parents: 19732
diff changeset
   463
      | prt_reg (ts, (attn, witns)) =
17138
ad4c98fd367b Interpretation in locales: extended back end;
ballarin
parents: 17109
diff changeset
   464
        if show_wits
17096
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   465
          then Pretty.block ((prt_attn attn @
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   466
            [Pretty.str ":", Pretty.brk 1, prt_inst ts, Pretty.fbrk,
19780
dce2168b0ea4 export read/cert_expr;
wenzelm
parents: 19732
diff changeset
   467
              prt_witns witns]))
17096
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   468
          else Pretty.block ((prt_attn attn @
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   469
            [Pretty.str ":", Pretty.brk 1, prt_inst ts]));
15703
727ef1b8b3ee *** empty log message ***
wenzelm
parents: 15696
diff changeset
   470
16458
4c6fd0c01d28 accomodate change of TheoryDataFun;
wenzelm
parents: 16346
diff changeset
   471
    val loc_int = intern thy loc;
15624
484178635bd8 Further work on interpretation commands. New command `interpret' for
ballarin
parents: 15623
diff changeset
   472
    val regs = get_regs thy_ctxt;
17412
e26cb20ef0cc TableFun/Symtab: curried lookup and update;
wenzelm
parents: 17384
diff changeset
   473
    val loc_regs = Symtab.lookup regs loc_int;
15596
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
   474
  in
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
   475
    (case loc_regs of
17355
5b31131c0365 load late, after proof.ML;
wenzelm
parents: 17316
diff changeset
   476
        NONE => Pretty.str ("no interpretations in " ^ msg)
15763
b901a127ac73 Interpretation supports statically scoped attributes; documentation.
ballarin
parents: 15749
diff changeset
   477
      | SOME r => let
20069
77a6b62418bb Witness theorems of interpretations now transfered to current theory.
ballarin
parents: 20059
diff changeset
   478
            val r' = Registrations.dest thy r;
15763
b901a127ac73 Interpretation supports statically scoped attributes; documentation.
ballarin
parents: 15749
diff changeset
   479
            val r'' = Library.sort_wrt (fn (_, ((prfx, _), _)) => prfx) r';
17355
5b31131c0365 load late, after proof.ML;
wenzelm
parents: 17316
diff changeset
   480
          in Pretty.big_list ("interpretations in " ^ msg ^ ":")
17096
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   481
            (map prt_reg r'')
15763
b901a127ac73 Interpretation supports statically scoped attributes; documentation.
ballarin
parents: 15749
diff changeset
   482
          end)
15596
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
   483
    |> Pretty.writeln
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
   484
  end;
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
   485
15624
484178635bd8 Further work on interpretation commands. New command `interpret' for
ballarin
parents: 15623
diff changeset
   486
val print_global_registrations =
484178635bd8 Further work on interpretation commands. New command `interpret' for
ballarin
parents: 15623
diff changeset
   487
     gen_print_registrations (#3 o GlobalLocalesData.get)
15703
727ef1b8b3ee *** empty log message ***
wenzelm
parents: 15696
diff changeset
   488
       ProofContext.init "theory";
15624
484178635bd8 Further work on interpretation commands. New command `interpret' for
ballarin
parents: 15623
diff changeset
   489
val print_local_registrations' =
484178635bd8 Further work on interpretation commands. New command `interpret' for
ballarin
parents: 15623
diff changeset
   490
     gen_print_registrations LocalLocalesData.get
15703
727ef1b8b3ee *** empty log message ***
wenzelm
parents: 15696
diff changeset
   491
       I "context";
17138
ad4c98fd367b Interpretation in locales: extended back end;
ballarin
parents: 17109
diff changeset
   492
fun print_local_registrations show_wits loc ctxt =
ad4c98fd367b Interpretation in locales: extended back end;
ballarin
parents: 17109
diff changeset
   493
  (print_global_registrations show_wits loc (ProofContext.theory_of ctxt);
ad4c98fd367b Interpretation in locales: extended back end;
ballarin
parents: 17109
diff changeset
   494
   print_local_registrations' show_wits loc ctxt);
15624
484178635bd8 Further work on interpretation commands. New command `interpret' for
ballarin
parents: 15623
diff changeset
   495
15596
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
   496
12277
2b28d7dd91f5 improved ordering of evaluated elements;
wenzelm
parents: 12273
diff changeset
   497
(* diagnostics *)
12273
7fb9840d358d beginnings of actual locale expressions;
wenzelm
parents: 12263
diff changeset
   498
12277
2b28d7dd91f5 improved ordering of evaluated elements;
wenzelm
parents: 12273
diff changeset
   499
fun err_in_locale ctxt msg ids =
2b28d7dd91f5 improved ordering of evaluated elements;
wenzelm
parents: 12273
diff changeset
   500
  let
16458
4c6fd0c01d28 accomodate change of TheoryDataFun;
wenzelm
parents: 16346
diff changeset
   501
    val thy = ProofContext.theory_of ctxt;
12529
d99716a53f59 simultaneous type-inference of complete context/statement specifications;
wenzelm
parents: 12514
diff changeset
   502
    fun prt_id (name, parms) =
16458
4c6fd0c01d28 accomodate change of TheoryDataFun;
wenzelm
parents: 16346
diff changeset
   503
      [Pretty.block (Pretty.breaks (map Pretty.str (extern thy name :: parms)))];
19482
9f11af8f7ef9 tuned basic list operators (flat, maps, map_filter);
wenzelm
parents: 19423
diff changeset
   504
    val prt_ids = flat (separate [Pretty.str " +", Pretty.brk 1] (map prt_id ids));
12502
9e7f72e25022 beginning support for type instantiation;
wenzelm
parents: 12323
diff changeset
   505
    val err_msg =
12529
d99716a53f59 simultaneous type-inference of complete context/statement specifications;
wenzelm
parents: 12514
diff changeset
   506
      if forall (equal "" o #1) ids then msg
12502
9e7f72e25022 beginning support for type instantiation;
wenzelm
parents: 12323
diff changeset
   507
      else msg ^ "\n" ^ Pretty.string_of (Pretty.block
9e7f72e25022 beginning support for type instantiation;
wenzelm
parents: 12323
diff changeset
   508
        (Pretty.str "The error(s) above occurred in locale:" :: Pretty.brk 1 :: prt_ids));
18678
dd0c569fa43d sane ERROR handling;
wenzelm
parents: 18671
diff changeset
   509
  in error err_msg end;
12063
4c16bdee47d4 added add_locale(_i) and store_thm;
wenzelm
parents: 12058
diff changeset
   510
15206
09d78ec709c7 Modified locales: improved implementation of "includes".
ballarin
parents: 15127
diff changeset
   511
fun err_in_locale' ctxt msg ids' = err_in_locale ctxt msg (map fst ids');
12277
2b28d7dd91f5 improved ordering of evaluated elements;
wenzelm
parents: 12273
diff changeset
   512
2b28d7dd91f5 improved ordering of evaluated elements;
wenzelm
parents: 12273
diff changeset
   513
19783
82f365a14960 Improved parameter management of locales.
ballarin
parents: 19780
diff changeset
   514
fun pretty_ren NONE = Pretty.str "_"
82f365a14960 Improved parameter management of locales.
ballarin
parents: 19780
diff changeset
   515
  | pretty_ren (SOME (x, NONE)) = Pretty.str x
82f365a14960 Improved parameter management of locales.
ballarin
parents: 19780
diff changeset
   516
  | pretty_ren (SOME (x, SOME syn)) =
82f365a14960 Improved parameter management of locales.
ballarin
parents: 19780
diff changeset
   517
      Pretty.block [Pretty.str x, Pretty.brk 1, Syntax.pretty_mixfix syn];
82f365a14960 Improved parameter management of locales.
ballarin
parents: 19780
diff changeset
   518
82f365a14960 Improved parameter management of locales.
ballarin
parents: 19780
diff changeset
   519
fun pretty_expr thy (Locale name) = Pretty.str (extern thy name)
82f365a14960 Improved parameter management of locales.
ballarin
parents: 19780
diff changeset
   520
  | pretty_expr thy (Rename (expr, xs)) =
82f365a14960 Improved parameter management of locales.
ballarin
parents: 19780
diff changeset
   521
      Pretty.block [pretty_expr thy expr, Pretty.brk 1, Pretty.block (map pretty_ren xs |> Pretty.breaks)]
82f365a14960 Improved parameter management of locales.
ballarin
parents: 19780
diff changeset
   522
  | pretty_expr thy (Merge es) =
82f365a14960 Improved parameter management of locales.
ballarin
parents: 19780
diff changeset
   523
      Pretty.separate "+" (map (pretty_expr thy) es) |> Pretty.block;
82f365a14960 Improved parameter management of locales.
ballarin
parents: 19780
diff changeset
   524
82f365a14960 Improved parameter management of locales.
ballarin
parents: 19780
diff changeset
   525
fun err_in_expr _ msg (Merge []) = error msg
82f365a14960 Improved parameter management of locales.
ballarin
parents: 19780
diff changeset
   526
  | err_in_expr ctxt msg expr =
82f365a14960 Improved parameter management of locales.
ballarin
parents: 19780
diff changeset
   527
    error (msg ^ "\n" ^ Pretty.string_of (Pretty.block
82f365a14960 Improved parameter management of locales.
ballarin
parents: 19780
diff changeset
   528
      [Pretty.str "The error(s) above occured in locale expression:", Pretty.brk 1,
82f365a14960 Improved parameter management of locales.
ballarin
parents: 19780
diff changeset
   529
       pretty_expr (ProofContext.theory_of ctxt) expr]));
82f365a14960 Improved parameter management of locales.
ballarin
parents: 19780
diff changeset
   530
12046
a404358fd965 locale elements;
wenzelm
parents: 12014
diff changeset
   531
12529
d99716a53f59 simultaneous type-inference of complete context/statement specifications;
wenzelm
parents: 12514
diff changeset
   532
(** structured contexts: rename + merge + implicit type instantiation **)
d99716a53f59 simultaneous type-inference of complete context/statement specifications;
wenzelm
parents: 12514
diff changeset
   533
d99716a53f59 simultaneous type-inference of complete context/statement specifications;
wenzelm
parents: 12514
diff changeset
   534
(* parameter types *)
d99716a53f59 simultaneous type-inference of complete context/statement specifications;
wenzelm
parents: 12514
diff changeset
   535
d99716a53f59 simultaneous type-inference of complete context/statement specifications;
wenzelm
parents: 12514
diff changeset
   536
fun frozen_tvars ctxt Ts =
19914
fde2b5c0b42b Variable.importT_inst;
wenzelm
parents: 19900
diff changeset
   537
  #1 (Variable.importT_inst (map Logic.mk_type Ts) ctxt)
19900
21a99d88d925 ProofContext: moved variable operations to struct Variable;
wenzelm
parents: 19873
diff changeset
   538
  |> map (fn ((xi, S), T) => (xi, (S, T)));
12529
d99716a53f59 simultaneous type-inference of complete context/statement specifications;
wenzelm
parents: 12514
diff changeset
   539
d99716a53f59 simultaneous type-inference of complete context/statement specifications;
wenzelm
parents: 12514
diff changeset
   540
fun unify_frozen ctxt maxidx Ts Us =
d99716a53f59 simultaneous type-inference of complete context/statement specifications;
wenzelm
parents: 12514
diff changeset
   541
  let
18343
e36238ac5359 defines: beta/eta contract lhs;
wenzelm
parents: 18330
diff changeset
   542
    fun paramify NONE i = (NONE, i)
e36238ac5359 defines: beta/eta contract lhs;
wenzelm
parents: 18330
diff changeset
   543
      | paramify (SOME T) i = apfst SOME (TypeInfer.paramify_dummies T i);
12529
d99716a53f59 simultaneous type-inference of complete context/statement specifications;
wenzelm
parents: 12514
diff changeset
   544
18343
e36238ac5359 defines: beta/eta contract lhs;
wenzelm
parents: 18330
diff changeset
   545
    val (Ts', maxidx') = fold_map paramify Ts maxidx;
e36238ac5359 defines: beta/eta contract lhs;
wenzelm
parents: 18330
diff changeset
   546
    val (Us', maxidx'') = fold_map paramify Us maxidx';
16947
c6a90f04924e Sign.typ_unify;
wenzelm
parents: 16861
diff changeset
   547
    val thy = ProofContext.theory_of ctxt;
14215
ebf291f3b449 Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents: 13629
diff changeset
   548
18190
b7748c77562f tuned Pattern.match/unify;
wenzelm
parents: 18137
diff changeset
   549
    fun unify (SOME T, SOME U) env = (Sign.typ_unify thy (U, T) env
b7748c77562f tuned Pattern.match/unify;
wenzelm
parents: 18137
diff changeset
   550
          handle Type.TUNIFY => raise TYPE ("unify_frozen: failed to unify types", [U, T], []))
b7748c77562f tuned Pattern.match/unify;
wenzelm
parents: 18137
diff changeset
   551
      | unify _ env = env;
b7748c77562f tuned Pattern.match/unify;
wenzelm
parents: 18137
diff changeset
   552
    val (unifier, _) = fold unify (Ts' ~~ Us') (Vartab.empty, maxidx'');
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   553
    val Vs = map (Option.map (Envir.norm_type unifier)) Us';
19482
9f11af8f7ef9 tuned basic list operators (flat, maps, map_filter);
wenzelm
parents: 19423
diff changeset
   554
    val unifier' = Vartab.extend (unifier, frozen_tvars ctxt (map_filter I Vs));
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   555
  in map (Option.map (Envir.norm_type unifier')) Vs end;
12529
d99716a53f59 simultaneous type-inference of complete context/statement specifications;
wenzelm
parents: 12514
diff changeset
   556
21665
ba07e24dc941 encode declarations as notes (attributes), which enables proper inheritance, interpretation etc.;
wenzelm
parents: 21602
diff changeset
   557
fun params_of elemss =
ba07e24dc941 encode declarations as notes (attributes), which enables proper inheritance, interpretation etc.;
wenzelm
parents: 21602
diff changeset
   558
  distinct (eq_fst (op = : string * string -> bool)) (maps (snd o fst) elemss);
ba07e24dc941 encode declarations as notes (attributes), which enables proper inheritance, interpretation etc.;
wenzelm
parents: 21602
diff changeset
   559
ba07e24dc941 encode declarations as notes (attributes), which enables proper inheritance, interpretation etc.;
wenzelm
parents: 21602
diff changeset
   560
fun params_of' elemss =
ba07e24dc941 encode declarations as notes (attributes), which enables proper inheritance, interpretation etc.;
wenzelm
parents: 21602
diff changeset
   561
  distinct (eq_fst (op = : string * string -> bool)) (maps (snd o fst o fst) elemss);
ba07e24dc941 encode declarations as notes (attributes), which enables proper inheritance, interpretation etc.;
wenzelm
parents: 21602
diff changeset
   562
ba07e24dc941 encode declarations as notes (attributes), which enables proper inheritance, interpretation etc.;
wenzelm
parents: 21602
diff changeset
   563
ba07e24dc941 encode declarations as notes (attributes), which enables proper inheritance, interpretation etc.;
wenzelm
parents: 21602
diff changeset
   564
fun params_prefix params = space_implode "_" params;
16102
c5f6726d9bb1 Locale expressions: rename with optional mixfix syntax.
ballarin
parents: 16028
diff changeset
   565
14508
859b11514537 Experimental command for instantiation of locales in proof contexts:
ballarin
parents: 14446
diff changeset
   566
859b11514537 Experimental command for instantiation of locales in proof contexts:
ballarin
parents: 14446
diff changeset
   567
(* CB: param_types has the following type:
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15456
diff changeset
   568
  ('a * 'b option) list -> ('a * 'b) list *)
19482
9f11af8f7ef9 tuned basic list operators (flat, maps, map_filter);
wenzelm
parents: 19423
diff changeset
   569
fun param_types ps = map_filter (fn (_, NONE) => NONE | (x, SOME T) => SOME (x, T)) ps;
12529
d99716a53f59 simultaneous type-inference of complete context/statement specifications;
wenzelm
parents: 12514
diff changeset
   570
d99716a53f59 simultaneous type-inference of complete context/statement specifications;
wenzelm
parents: 12514
diff changeset
   571
19932
63bd0eeb4e0d fixed sml/nj value restriction problem
haftmann
parents: 19931
diff changeset
   572
fun merge_syntax ctxt ids ss = Symtab.merge (op = : mixfix * mixfix -> bool) ss
16102
c5f6726d9bb1 Locale expressions: rename with optional mixfix syntax.
ballarin
parents: 16028
diff changeset
   573
  handle Symtab.DUPS xs => err_in_locale ctxt
16105
a44801c499cb SML/NJ compatibility.
ballarin
parents: 16103
diff changeset
   574
    ("Conflicting syntax for parameter(s): " ^ commas_quote xs) (map fst ids);
16102
c5f6726d9bb1 Locale expressions: rename with optional mixfix syntax.
ballarin
parents: 16028
diff changeset
   575
c5f6726d9bb1 Locale expressions: rename with optional mixfix syntax.
ballarin
parents: 16028
diff changeset
   576
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   577
(* Distinction of assumed vs. derived identifiers.
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   578
   The former may have axioms relating assumptions of the context to
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   579
   assumptions of the specification fragment (for locales with
19780
dce2168b0ea4 export read/cert_expr;
wenzelm
parents: 19732
diff changeset
   580
   predicates).  The latter have witnesses relating assumptions of the
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   581
   specification fragment to assumptions of other (assumed) specification
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   582
   fragments. *)
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   583
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   584
datatype 'a mode = Assumed of 'a | Derived of 'a;
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   585
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   586
fun map_mode f (Assumed x) = Assumed (f x)
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   587
  | map_mode f (Derived x) = Derived (f x);
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   588
18123
1bb572e8cee9 avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents: 18038
diff changeset
   589
12529
d99716a53f59 simultaneous type-inference of complete context/statement specifications;
wenzelm
parents: 12514
diff changeset
   590
(* flatten expressions *)
11896
1ff33f896720 moved locale.ML to Isar/locale.ML;
wenzelm
parents:
diff changeset
   591
12510
172d18ec3b54 proper treatment of internal parameters;
wenzelm
parents: 12502
diff changeset
   592
local
12502
9e7f72e25022 beginning support for type instantiation;
wenzelm
parents: 12323
diff changeset
   593
18137
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
   594
fun unify_parms ctxt fixed_parms raw_parmss =
12502
9e7f72e25022 beginning support for type instantiation;
wenzelm
parents: 12323
diff changeset
   595
  let
16458
4c6fd0c01d28 accomodate change of TheoryDataFun;
wenzelm
parents: 16346
diff changeset
   596
    val thy = ProofContext.theory_of ctxt;
12502
9e7f72e25022 beginning support for type instantiation;
wenzelm
parents: 12323
diff changeset
   597
    val maxidx = length raw_parmss;
9e7f72e25022 beginning support for type instantiation;
wenzelm
parents: 12323
diff changeset
   598
    val idx_parmss = (0 upto maxidx - 1) ~~ raw_parmss;
9e7f72e25022 beginning support for type instantiation;
wenzelm
parents: 12323
diff changeset
   599
9e7f72e25022 beginning support for type instantiation;
wenzelm
parents: 12323
diff changeset
   600
    fun varify i = Term.map_type_tfree (fn (a, S) => TVar ((a, i), S));
12529
d99716a53f59 simultaneous type-inference of complete context/statement specifications;
wenzelm
parents: 12514
diff changeset
   601
    fun varify_parms (i, ps) = map (apsnd (varify i)) (param_types ps);
19482
9f11af8f7ef9 tuned basic list operators (flat, maps, map_filter);
wenzelm
parents: 19423
diff changeset
   602
    val parms = fixed_parms @ maps varify_parms idx_parmss;
12502
9e7f72e25022 beginning support for type instantiation;
wenzelm
parents: 12323
diff changeset
   603
18137
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
   604
    fun unify T U envir = Sign.typ_unify thy (U, T) envir
15206
09d78ec709c7 Modified locales: improved implementation of "includes".
ballarin
parents: 15127
diff changeset
   605
      handle Type.TUNIFY =>
18137
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
   606
        let val prt = Sign.string_of_typ thy in
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
   607
          raise TYPE ("unify_parms: failed to unify types " ^
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
   608
            prt U ^ " and " ^ prt T, [U, T], [])
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
   609
        end;
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
   610
    fun unify_list (T :: Us) = fold (unify T) Us
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
   611
      | unify_list [] = I;
18952
0388d0b0f3d5 TableFun: renamed xxx_multi to xxx_list;
wenzelm
parents: 18917
diff changeset
   612
    val (unifier, _) = fold unify_list (map #2 (Symtab.dest (Symtab.make_list parms)))
18137
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
   613
      (Vartab.empty, maxidx);
12502
9e7f72e25022 beginning support for type instantiation;
wenzelm
parents: 12323
diff changeset
   614
19061
ffbbac0261c9 removed distinct, renamed gen_distinct to distinct;
wenzelm
parents: 19025
diff changeset
   615
    val parms' = map (apsnd (Envir.norm_type unifier)) (distinct (eq_fst (op =)) parms);
12502
9e7f72e25022 beginning support for type instantiation;
wenzelm
parents: 12323
diff changeset
   616
    val unifier' = Vartab.extend (unifier, frozen_tvars ctxt (map #2 parms'));
9e7f72e25022 beginning support for type instantiation;
wenzelm
parents: 12323
diff changeset
   617
9e7f72e25022 beginning support for type instantiation;
wenzelm
parents: 12323
diff changeset
   618
    fun inst_parms (i, ps) =
19482
9f11af8f7ef9 tuned basic list operators (flat, maps, map_filter);
wenzelm
parents: 19423
diff changeset
   619
      foldr Term.add_typ_tfrees [] (map_filter snd ps)
9f11af8f7ef9 tuned basic list operators (flat, maps, map_filter);
wenzelm
parents: 19423
diff changeset
   620
      |> map_filter (fn (a, S) =>
12502
9e7f72e25022 beginning support for type instantiation;
wenzelm
parents: 12323
diff changeset
   621
          let val T = Envir.norm_type unifier' (TVar ((a, i), S))
18137
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
   622
          in if T = TFree (a, S) then NONE else SOME (a, T) end)
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
   623
      |> Symtab.make;
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
   624
  in map inst_parms idx_parmss end;
12502
9e7f72e25022 beginning support for type instantiation;
wenzelm
parents: 12323
diff changeset
   625
12529
d99716a53f59 simultaneous type-inference of complete context/statement specifications;
wenzelm
parents: 12514
diff changeset
   626
in
12502
9e7f72e25022 beginning support for type instantiation;
wenzelm
parents: 12323
diff changeset
   627
12529
d99716a53f59 simultaneous type-inference of complete context/statement specifications;
wenzelm
parents: 12514
diff changeset
   628
fun unify_elemss _ _ [] = []
d99716a53f59 simultaneous type-inference of complete context/statement specifications;
wenzelm
parents: 12514
diff changeset
   629
  | unify_elemss _ [] [elems] = [elems]
d99716a53f59 simultaneous type-inference of complete context/statement specifications;
wenzelm
parents: 12514
diff changeset
   630
  | unify_elemss ctxt fixed_parms elemss =
12502
9e7f72e25022 beginning support for type instantiation;
wenzelm
parents: 12323
diff changeset
   631
      let
18137
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
   632
        val thy = ProofContext.theory_of ctxt;
21483
e4be91feca50 replaced Args.map_values/Element.map_ctxt_values by general morphism application;
wenzelm
parents: 21441
diff changeset
   633
        val phis = unify_parms ctxt fixed_parms (map (snd o fst o fst) elemss)
e4be91feca50 replaced Args.map_values/Element.map_ctxt_values by general morphism application;
wenzelm
parents: 21441
diff changeset
   634
          |> map (Element.instT_morphism thy);
e4be91feca50 replaced Args.map_values/Element.map_ctxt_values by general morphism application;
wenzelm
parents: 21441
diff changeset
   635
        fun inst ((((name, ps), mode), elems), phi) =
e4be91feca50 replaced Args.map_values/Element.map_ctxt_values by general morphism application;
wenzelm
parents: 21441
diff changeset
   636
          (((name, map (apsnd (Option.map (Morphism.typ phi))) ps),
e4be91feca50 replaced Args.map_values/Element.map_ctxt_values by general morphism application;
wenzelm
parents: 21441
diff changeset
   637
              map_mode (map (Element.morph_witness phi)) mode),
e4be91feca50 replaced Args.map_values/Element.map_ctxt_values by general morphism application;
wenzelm
parents: 21441
diff changeset
   638
            map (Element.morph_ctxt phi) elems);
e4be91feca50 replaced Args.map_values/Element.map_ctxt_values by general morphism application;
wenzelm
parents: 21441
diff changeset
   639
      in map inst (elemss ~~ phis) end;
12502
9e7f72e25022 beginning support for type instantiation;
wenzelm
parents: 12323
diff changeset
   640
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   641
19810
dae765e552ce renamed Type.(un)varifyT to Logic.(un)varifyT;
wenzelm
parents: 19783
diff changeset
   642
fun renaming xs parms = zip_options parms xs
dae765e552ce renamed Type.(un)varifyT to Logic.(un)varifyT;
wenzelm
parents: 19783
diff changeset
   643
  handle Library.UnequalLengths =>
dae765e552ce renamed Type.(un)varifyT to Logic.(un)varifyT;
wenzelm
parents: 19783
diff changeset
   644
    error ("Too many arguments in renaming: " ^
dae765e552ce renamed Type.(un)varifyT to Logic.(un)varifyT;
wenzelm
parents: 19783
diff changeset
   645
      commas (map (fn NONE => "_" | SOME x => quote (fst x)) xs));
dae765e552ce renamed Type.(un)varifyT to Logic.(un)varifyT;
wenzelm
parents: 19783
diff changeset
   646
dae765e552ce renamed Type.(un)varifyT to Logic.(un)varifyT;
wenzelm
parents: 19783
diff changeset
   647
19783
82f365a14960 Improved parameter management of locales.
ballarin
parents: 19780
diff changeset
   648
(* params_of_expr:
82f365a14960 Improved parameter management of locales.
ballarin
parents: 19780
diff changeset
   649
   Compute parameters (with types and syntax) of locale expression.
82f365a14960 Improved parameter management of locales.
ballarin
parents: 19780
diff changeset
   650
*)
82f365a14960 Improved parameter management of locales.
ballarin
parents: 19780
diff changeset
   651
82f365a14960 Improved parameter management of locales.
ballarin
parents: 19780
diff changeset
   652
fun params_of_expr ctxt fixed_params expr (prev_parms, prev_types, prev_syn) =
82f365a14960 Improved parameter management of locales.
ballarin
parents: 19780
diff changeset
   653
  let
82f365a14960 Improved parameter management of locales.
ballarin
parents: 19780
diff changeset
   654
    val thy = ProofContext.theory_of ctxt;
82f365a14960 Improved parameter management of locales.
ballarin
parents: 19780
diff changeset
   655
82f365a14960 Improved parameter management of locales.
ballarin
parents: 19780
diff changeset
   656
    fun merge_tenvs fixed tenv1 tenv2 =
82f365a14960 Improved parameter management of locales.
ballarin
parents: 19780
diff changeset
   657
        let
82f365a14960 Improved parameter management of locales.
ballarin
parents: 19780
diff changeset
   658
          val [env1, env2] = unify_parms ctxt fixed
82f365a14960 Improved parameter management of locales.
ballarin
parents: 19780
diff changeset
   659
                [tenv1 |> Symtab.dest |> map (apsnd SOME),
82f365a14960 Improved parameter management of locales.
ballarin
parents: 19780
diff changeset
   660
                 tenv2 |> Symtab.dest |> map (apsnd SOME)]
82f365a14960 Improved parameter management of locales.
ballarin
parents: 19780
diff changeset
   661
        in
82f365a14960 Improved parameter management of locales.
ballarin
parents: 19780
diff changeset
   662
          Symtab.merge (op =) (Symtab.map (Element.instT_type env1) tenv1,
82f365a14960 Improved parameter management of locales.
ballarin
parents: 19780
diff changeset
   663
            Symtab.map (Element.instT_type env2) tenv2)
82f365a14960 Improved parameter management of locales.
ballarin
parents: 19780
diff changeset
   664
        end;
82f365a14960 Improved parameter management of locales.
ballarin
parents: 19780
diff changeset
   665
82f365a14960 Improved parameter management of locales.
ballarin
parents: 19780
diff changeset
   666
    fun merge_syn expr syn1 syn2 =
19932
63bd0eeb4e0d fixed sml/nj value restriction problem
haftmann
parents: 19931
diff changeset
   667
        Symtab.merge (op = : mixfix * mixfix -> bool) (syn1, syn2)
19783
82f365a14960 Improved parameter management of locales.
ballarin
parents: 19780
diff changeset
   668
        handle Symtab.DUPS xs => err_in_expr ctxt
82f365a14960 Improved parameter management of locales.
ballarin
parents: 19780
diff changeset
   669
          ("Conflicting syntax for parameter(s): " ^ commas_quote xs) expr;
20366
867696dc64fc global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents: 20317
diff changeset
   670
19783
82f365a14960 Improved parameter management of locales.
ballarin
parents: 19780
diff changeset
   671
    fun params_of (expr as Locale name) =
82f365a14960 Improved parameter management of locales.
ballarin
parents: 19780
diff changeset
   672
          let
82f365a14960 Improved parameter management of locales.
ballarin
parents: 19780
diff changeset
   673
            val {import, params, ...} = the_locale thy name;
82f365a14960 Improved parameter management of locales.
ballarin
parents: 19780
diff changeset
   674
            val parms = map (fst o fst) params;
82f365a14960 Improved parameter management of locales.
ballarin
parents: 19780
diff changeset
   675
            val (parms', types', syn') = params_of import;
82f365a14960 Improved parameter management of locales.
ballarin
parents: 19780
diff changeset
   676
            val all_parms = merge_lists parms' parms;
82f365a14960 Improved parameter management of locales.
ballarin
parents: 19780
diff changeset
   677
            val all_types = merge_tenvs [] types' (params |> map fst |> Symtab.make);
82f365a14960 Improved parameter management of locales.
ballarin
parents: 19780
diff changeset
   678
            val all_syn = merge_syn expr syn' (params |> map (apfst fst) |> Symtab.make);
82f365a14960 Improved parameter management of locales.
ballarin
parents: 19780
diff changeset
   679
          in (all_parms, all_types, all_syn) end
82f365a14960 Improved parameter management of locales.
ballarin
parents: 19780
diff changeset
   680
      | params_of (expr as Rename (e, xs)) =
82f365a14960 Improved parameter management of locales.
ballarin
parents: 19780
diff changeset
   681
          let
82f365a14960 Improved parameter management of locales.
ballarin
parents: 19780
diff changeset
   682
            val (parms', types', syn') = params_of e;
82f365a14960 Improved parameter management of locales.
ballarin
parents: 19780
diff changeset
   683
            val ren = renaming xs parms';
82f365a14960 Improved parameter management of locales.
ballarin
parents: 19780
diff changeset
   684
            (* renaming may reduce number of parameters *)
82f365a14960 Improved parameter management of locales.
ballarin
parents: 19780
diff changeset
   685
            val new_parms = map (Element.rename ren) parms' |> distinct (op =);
82f365a14960 Improved parameter management of locales.
ballarin
parents: 19780
diff changeset
   686
            val ren_syn = syn' |> Symtab.dest |> map (Element.rename_var ren);
82f365a14960 Improved parameter management of locales.
ballarin
parents: 19780
diff changeset
   687
            val new_syn = fold (Symtab.insert (op =)) ren_syn Symtab.empty
82f365a14960 Improved parameter management of locales.
ballarin
parents: 19780
diff changeset
   688
                handle Symtab.DUP x =>
82f365a14960 Improved parameter management of locales.
ballarin
parents: 19780
diff changeset
   689
                  err_in_expr ctxt ("Conflicting syntax for parameter: " ^ quote x) expr;
82f365a14960 Improved parameter management of locales.
ballarin
parents: 19780
diff changeset
   690
            val syn_types = map (apsnd (fn mx => SOME (Type.freeze_type (#1 (TypeInfer.paramify_dummies (TypeInfer.mixfixT mx) 0))))) (Symtab.dest new_syn);
82f365a14960 Improved parameter management of locales.
ballarin
parents: 19780
diff changeset
   691
            val ren_types = types' |> Symtab.dest |> map (apfst (Element.rename ren));
20366
867696dc64fc global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents: 20317
diff changeset
   692
            val (env :: _) = unify_parms ctxt []
19783
82f365a14960 Improved parameter management of locales.
ballarin
parents: 19780
diff changeset
   693
                ((ren_types |> map (apsnd SOME)) :: map single syn_types);
82f365a14960 Improved parameter management of locales.
ballarin
parents: 19780
diff changeset
   694
            val new_types = fold (Symtab.insert (op =))
82f365a14960 Improved parameter management of locales.
ballarin
parents: 19780
diff changeset
   695
                (map (apsnd (Element.instT_type env)) ren_types) Symtab.empty;
82f365a14960 Improved parameter management of locales.
ballarin
parents: 19780
diff changeset
   696
          in (new_parms, new_types, new_syn) end
82f365a14960 Improved parameter management of locales.
ballarin
parents: 19780
diff changeset
   697
      | params_of (Merge es) =
82f365a14960 Improved parameter management of locales.
ballarin
parents: 19780
diff changeset
   698
          fold (fn e => fn (parms, types, syn) =>
82f365a14960 Improved parameter management of locales.
ballarin
parents: 19780
diff changeset
   699
                   let
82f365a14960 Improved parameter management of locales.
ballarin
parents: 19780
diff changeset
   700
                     val (parms', types', syn') = params_of e
82f365a14960 Improved parameter management of locales.
ballarin
parents: 19780
diff changeset
   701
                   in
82f365a14960 Improved parameter management of locales.
ballarin
parents: 19780
diff changeset
   702
                     (merge_lists parms parms', merge_tenvs [] types types',
82f365a14960 Improved parameter management of locales.
ballarin
parents: 19780
diff changeset
   703
                      merge_syn e syn syn')
82f365a14960 Improved parameter management of locales.
ballarin
parents: 19780
diff changeset
   704
                   end)
82f365a14960 Improved parameter management of locales.
ballarin
parents: 19780
diff changeset
   705
            es ([], Symtab.empty, Symtab.empty)
82f365a14960 Improved parameter management of locales.
ballarin
parents: 19780
diff changeset
   706
82f365a14960 Improved parameter management of locales.
ballarin
parents: 19780
diff changeset
   707
      val (parms, types, syn) = params_of expr;
82f365a14960 Improved parameter management of locales.
ballarin
parents: 19780
diff changeset
   708
    in
82f365a14960 Improved parameter management of locales.
ballarin
parents: 19780
diff changeset
   709
      (merge_lists prev_parms parms, merge_tenvs fixed_params prev_types types,
82f365a14960 Improved parameter management of locales.
ballarin
parents: 19780
diff changeset
   710
       merge_syn expr prev_syn syn)
82f365a14960 Improved parameter management of locales.
ballarin
parents: 19780
diff changeset
   711
    end;
82f365a14960 Improved parameter management of locales.
ballarin
parents: 19780
diff changeset
   712
82f365a14960 Improved parameter management of locales.
ballarin
parents: 19780
diff changeset
   713
fun make_params_ids params = [(("", params), ([], Assumed []))];
82f365a14960 Improved parameter management of locales.
ballarin
parents: 19780
diff changeset
   714
fun make_raw_params_elemss (params, tenv, syn) =
82f365a14960 Improved parameter management of locales.
ballarin
parents: 19780
diff changeset
   715
    [((("", map (fn p => (p, Symtab.lookup tenv p)) params), Assumed []),
82f365a14960 Improved parameter management of locales.
ballarin
parents: 19780
diff changeset
   716
      Int [Fixes (map (fn p =>
82f365a14960 Improved parameter management of locales.
ballarin
parents: 19780
diff changeset
   717
        (p, Symtab.lookup tenv p, Symtab.lookup syn p |> the)) params)])];
82f365a14960 Improved parameter management of locales.
ballarin
parents: 19780
diff changeset
   718
82f365a14960 Improved parameter management of locales.
ballarin
parents: 19780
diff changeset
   719
15596
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
   720
(* flatten_expr:
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
   721
   Extend list of identifiers by those new in locale expression expr.
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
   722
   Compute corresponding list of lists of locale elements (one entry per
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
   723
   identifier).
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
   724
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
   725
   Identifiers represent locale fragments and are in an extended form:
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
   726
     ((name, ps), (ax_ps, axs))
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
   727
   (name, ps) is the locale name with all its parameters.
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
   728
   (ax_ps, axs) is the locale axioms with its parameters;
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
   729
     axs are always taken from the top level of the locale hierarchy,
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
   730
     hence axioms may contain additional parameters from later fragments:
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
   731
     ps subset of ax_ps.  axs is either singleton or empty.
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
   732
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
   733
   Elements are enriched by identifier-like information:
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
   734
     (((name, ax_ps), axs), elems)
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
   735
   The parameters in ax_ps are the axiom parameters, but enriched by type
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
   736
   info: now each entry is a pair of string and typ option.  Axioms are
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
   737
   type-instantiated.
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
   738
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
   739
*)
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
   740
16102
c5f6726d9bb1 Locale expressions: rename with optional mixfix syntax.
ballarin
parents: 16028
diff changeset
   741
fun flatten_expr ctxt ((prev_idents, prev_syntax), expr) =
12014
035ab884b9e0 beginnings of new locales (not yet functional);
wenzelm
parents: 11896
diff changeset
   742
  let
035ab884b9e0 beginnings of new locales (not yet functional);
wenzelm
parents: 11896
diff changeset
   743
    val thy = ProofContext.theory_of ctxt;
12263
6f2acf10e2a2 locale expressions;
wenzelm
parents: 12143
diff changeset
   744
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   745
    fun rename_parms top ren ((name, ps), (parms, mode)) =
19783
82f365a14960 Improved parameter management of locales.
ballarin
parents: 19780
diff changeset
   746
        ((name, map (Element.rename ren) ps),
82f365a14960 Improved parameter management of locales.
ballarin
parents: 19780
diff changeset
   747
         if top
82f365a14960 Improved parameter management of locales.
ballarin
parents: 19780
diff changeset
   748
         then (map (Element.rename ren) parms,
21483
e4be91feca50 replaced Args.map_values/Element.map_ctxt_values by general morphism application;
wenzelm
parents: 21441
diff changeset
   749
               map_mode (map (Element.morph_witness (Element.rename_morphism ren))) mode)
19783
82f365a14960 Improved parameter management of locales.
ballarin
parents: 19780
diff changeset
   750
         else (parms, mode));
12263
6f2acf10e2a2 locale expressions;
wenzelm
parents: 12143
diff changeset
   751
20167
fe5fd4fd4114 Strict dfs traversal of imported and registered identifiers.
ballarin
parents: 20092
diff changeset
   752
    (* add (name, ps) and its registrations, recursively; adjust hyps of witnesses *)
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   753
20167
fe5fd4fd4114 Strict dfs traversal of imported and registered identifiers.
ballarin
parents: 20092
diff changeset
   754
    fun add_with_regs ((name, pTs), mode) (wits, ids, visited) =
fe5fd4fd4114 Strict dfs traversal of imported and registered identifiers.
ballarin
parents: 20092
diff changeset
   755
        if member (fn (a, (b, _)) => a = b) visited (name, map #1 pTs)
fe5fd4fd4114 Strict dfs traversal of imported and registered identifiers.
ballarin
parents: 20092
diff changeset
   756
        then (wits, ids, visited)
fe5fd4fd4114 Strict dfs traversal of imported and registered identifiers.
ballarin
parents: 20092
diff changeset
   757
        else
20366
867696dc64fc global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents: 20317
diff changeset
   758
          let
867696dc64fc global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents: 20317
diff changeset
   759
            val {params, regs, ...} = the_locale thy name;
867696dc64fc global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents: 20317
diff changeset
   760
            val pTs' = map #1 params;
867696dc64fc global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents: 20317
diff changeset
   761
            val ren = map #1 pTs' ~~ map (fn (x, _) => (x, NONE)) pTs;
867696dc64fc global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents: 20317
diff changeset
   762
              (* dummy syntax, since required by rename *)
867696dc64fc global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents: 20317
diff changeset
   763
            val pTs'' = map (fn ((p, _), (_, T)) => (p, T)) (pTs ~~ pTs');
867696dc64fc global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents: 20317
diff changeset
   764
            val [env] = unify_parms ctxt pTs [map (apsnd SOME) pTs''];
867696dc64fc global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents: 20317
diff changeset
   765
              (* propagate parameter types, to keep them consistent *)
867696dc64fc global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents: 20317
diff changeset
   766
            val regs' = map (fn ((name, ps), wits) =>
867696dc64fc global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents: 20317
diff changeset
   767
                ((name, map (Element.rename ren) ps),
867696dc64fc global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents: 20317
diff changeset
   768
                 map (Element.transfer_witness thy) wits)) regs;
867696dc64fc global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents: 20317
diff changeset
   769
            val new_regs = regs';
867696dc64fc global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents: 20317
diff changeset
   770
            val new_ids = map fst new_regs;
21483
e4be91feca50 replaced Args.map_values/Element.map_ctxt_values by general morphism application;
wenzelm
parents: 21441
diff changeset
   771
            val new_idTs =
e4be91feca50 replaced Args.map_values/Element.map_ctxt_values by general morphism application;
wenzelm
parents: 21441
diff changeset
   772
              map (apsnd (map (fn p => (p, (the o AList.lookup (op =) pTs) p)))) new_ids;
17096
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   773
20366
867696dc64fc global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents: 20317
diff changeset
   774
            val new_wits = new_regs |> map (#2 #> map
21483
e4be91feca50 replaced Args.map_values/Element.map_ctxt_values by general morphism application;
wenzelm
parents: 21441
diff changeset
   775
              (Element.morph_witness
e4be91feca50 replaced Args.map_values/Element.map_ctxt_values by general morphism application;
wenzelm
parents: 21441
diff changeset
   776
                (Element.instT_morphism thy env $>
e4be91feca50 replaced Args.map_values/Element.map_ctxt_values by general morphism application;
wenzelm
parents: 21441
diff changeset
   777
                  Element.rename_morphism ren $>
e4be91feca50 replaced Args.map_values/Element.map_ctxt_values by general morphism application;
wenzelm
parents: 21441
diff changeset
   778
                  Element.satisfy_morphism wits)));
20366
867696dc64fc global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents: 20317
diff changeset
   779
            val new_ids' = map (fn (id, wits) =>
867696dc64fc global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents: 20317
diff changeset
   780
                (id, ([], Derived wits))) (new_ids ~~ new_wits);
867696dc64fc global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents: 20317
diff changeset
   781
            val new_idTs' = map (fn ((n, pTs), (_, ([], mode))) =>
867696dc64fc global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents: 20317
diff changeset
   782
                ((n, pTs), mode)) (new_idTs ~~ new_ids');
867696dc64fc global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents: 20317
diff changeset
   783
            val new_id = ((name, map #1 pTs), ([], mode));
867696dc64fc global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents: 20317
diff changeset
   784
            val (wits', ids', visited') = fold add_with_regs new_idTs'
20167
fe5fd4fd4114 Strict dfs traversal of imported and registered identifiers.
ballarin
parents: 20092
diff changeset
   785
              (wits @ flat new_wits, ids, visited @ [new_id]);
20366
867696dc64fc global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents: 20317
diff changeset
   786
          in
867696dc64fc global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents: 20317
diff changeset
   787
            (wits', ids' @ [new_id], visited')
867696dc64fc global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents: 20317
diff changeset
   788
          end;
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   789
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   790
    (* distribute top-level axioms over assumed ids *)
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   791
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   792
    fun axiomify all_ps ((name, parms), (_, Assumed _)) axioms =
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   793
        let
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   794
          val {elems, ...} = the_locale thy name;
19482
9f11af8f7ef9 tuned basic list operators (flat, maps, map_filter);
wenzelm
parents: 19423
diff changeset
   795
          val ts = maps
9f11af8f7ef9 tuned basic list operators (flat, maps, map_filter);
wenzelm
parents: 19423
diff changeset
   796
            (fn (Assumes asms, _) => maps (map #1 o #2) asms
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   797
              | _ => [])
19482
9f11af8f7ef9 tuned basic list operators (flat, maps, map_filter);
wenzelm
parents: 19423
diff changeset
   798
            elems;
19018
88b4979193d8 added abbreviations: activated by init, no expressions yet;
wenzelm
parents: 18964
diff changeset
   799
          val (axs1, axs2) = chop (length ts) axioms;
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   800
        in (((name, parms), (all_ps, Assumed axs1)), axs2) end
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   801
      | axiomify all_ps (id, (_, Derived ths)) axioms =
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   802
          ((id, (all_ps, Derived ths)), axioms);
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   803
17096
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   804
    (* identifiers of an expression *)
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   805
15206
09d78ec709c7 Modified locales: improved implementation of "includes".
ballarin
parents: 15127
diff changeset
   806
    fun identify top (Locale name) =
15596
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
   807
    (* CB: ids_ax is a list of tuples of the form ((name, ps), axs),
15206
09d78ec709c7 Modified locales: improved implementation of "includes".
ballarin
parents: 15127
diff changeset
   808
       where name is a locale name, ps a list of parameter names and axs
09d78ec709c7 Modified locales: improved implementation of "includes".
ballarin
parents: 15127
diff changeset
   809
       a list of axioms relating to the identifier, axs is empty unless
09d78ec709c7 Modified locales: improved implementation of "includes".
ballarin
parents: 15127
diff changeset
   810
       identify at top level (top = true);
14215
ebf291f3b449 Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents: 13629
diff changeset
   811
       parms is accumulated list of parameters *)
12289
ec2dafd0a6a9 clarified locale operations (rename, merge);
wenzelm
parents: 12277
diff changeset
   812
          let
20035
80c79876d2de Internal restructuring: identify no longer computes syntax.
ballarin
parents: 20032
diff changeset
   813
            val {axiom, import, params, ...} = the_locale thy name;
19278
4d762b77d319 Internal restructuring: local parameters.
ballarin
parents: 19276
diff changeset
   814
            val ps = map (#1 o #1) params;
20035
80c79876d2de Internal restructuring: identify no longer computes syntax.
ballarin
parents: 20032
diff changeset
   815
            val (ids', parms') = identify false import;
15206
09d78ec709c7 Modified locales: improved implementation of "includes".
ballarin
parents: 15127
diff changeset
   816
                (* acyclic import dependencies *)
19931
fb32b43e7f80 Restructured locales with predicates: import is now an interpretation.
ballarin
parents: 19914
diff changeset
   817
20167
fe5fd4fd4114 Strict dfs traversal of imported and registered identifiers.
ballarin
parents: 20092
diff changeset
   818
            val (_, ids'', _) = add_with_regs ((name, map #1 params), Assumed []) ([], ids', ids');
fe5fd4fd4114 Strict dfs traversal of imported and registered identifiers.
ballarin
parents: 20092
diff changeset
   819
            val ids_ax = if top then fst (fold_map (axiomify ps) ids'' axiom) else ids'';
20035
80c79876d2de Internal restructuring: identify no longer computes syntax.
ballarin
parents: 20032
diff changeset
   820
            in (ids_ax, merge_lists parms' ps) end
15206
09d78ec709c7 Modified locales: improved implementation of "includes".
ballarin
parents: 15127
diff changeset
   821
      | identify top (Rename (e, xs)) =
12273
7fb9840d358d beginnings of actual locale expressions;
wenzelm
parents: 12263
diff changeset
   822
          let
20035
80c79876d2de Internal restructuring: identify no longer computes syntax.
ballarin
parents: 20032
diff changeset
   823
            val (ids', parms') = identify top e;
12839
584a3e0b00f2 reorganized code for predicate text;
wenzelm
parents: 12834
diff changeset
   824
            val ren = renaming xs parms'
18678
dd0c569fa43d sane ERROR handling;
wenzelm
parents: 18671
diff changeset
   825
              handle ERROR msg => err_in_locale' ctxt msg ids';
17096
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   826
19061
ffbbac0261c9 removed distinct, renamed gen_distinct to distinct;
wenzelm
parents: 19025
diff changeset
   827
            val ids'' = distinct (eq_fst (op =)) (map (rename_parms top ren) ids');
19482
9f11af8f7ef9 tuned basic list operators (flat, maps, map_filter);
wenzelm
parents: 19423
diff changeset
   828
            val parms'' = distinct (op =) (maps (#2 o #1) ids'');
20035
80c79876d2de Internal restructuring: identify no longer computes syntax.
ballarin
parents: 20032
diff changeset
   829
          in (ids'', parms'') end
15206
09d78ec709c7 Modified locales: improved implementation of "includes".
ballarin
parents: 15127
diff changeset
   830
      | identify top (Merge es) =
20035
80c79876d2de Internal restructuring: identify no longer computes syntax.
ballarin
parents: 20032
diff changeset
   831
          fold (fn e => fn (ids, parms) =>
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   832
                   let
20035
80c79876d2de Internal restructuring: identify no longer computes syntax.
ballarin
parents: 20032
diff changeset
   833
                     val (ids', parms') = identify top e
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   834
                   in
20035
80c79876d2de Internal restructuring: identify no longer computes syntax.
ballarin
parents: 20032
diff changeset
   835
                     (merge_alists ids ids', merge_lists parms parms')
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   836
                   end)
20035
80c79876d2de Internal restructuring: identify no longer computes syntax.
ballarin
parents: 20032
diff changeset
   837
            es ([], []);
15206
09d78ec709c7 Modified locales: improved implementation of "includes".
ballarin
parents: 15127
diff changeset
   838
20035
80c79876d2de Internal restructuring: identify no longer computes syntax.
ballarin
parents: 20032
diff changeset
   839
    fun inst_wit all_params (t, th) = let
15206
09d78ec709c7 Modified locales: improved implementation of "includes".
ballarin
parents: 15127
diff changeset
   840
         val {hyps, prop, ...} = Thm.rep_thm th;
16861
7446b4be013b tuned fold on terms;
wenzelm
parents: 16850
diff changeset
   841
         val ps = map (apsnd SOME) (fold Term.add_frees (prop :: hyps) []);
15206
09d78ec709c7 Modified locales: improved implementation of "includes".
ballarin
parents: 15127
diff changeset
   842
         val [env] = unify_parms ctxt all_params [ps];
18137
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
   843
         val t' = Element.instT_term env t;
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
   844
         val th' = Element.instT_thm thy env th;
18123
1bb572e8cee9 avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents: 18038
diff changeset
   845
       in (t', th') end;
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   846
20035
80c79876d2de Internal restructuring: identify no longer computes syntax.
ballarin
parents: 20032
diff changeset
   847
    fun eval all_params tenv syn ((name, params), (locale_params, mode)) =
80c79876d2de Internal restructuring: identify no longer computes syntax.
ballarin
parents: 20032
diff changeset
   848
      let
80c79876d2de Internal restructuring: identify no longer computes syntax.
ballarin
parents: 20032
diff changeset
   849
        val {params = ps_mx, elems = elems_stamped, ...} = the_locale thy name;
80c79876d2de Internal restructuring: identify no longer computes syntax.
ballarin
parents: 20032
diff changeset
   850
        val elems = map fst elems_stamped;
80c79876d2de Internal restructuring: identify no longer computes syntax.
ballarin
parents: 20032
diff changeset
   851
        val ps = map fst ps_mx;
80c79876d2de Internal restructuring: identify no longer computes syntax.
ballarin
parents: 20032
diff changeset
   852
        fun lookup_syn x = (case Symtab.lookup syn x of SOME Structure => NONE | opt => opt);
80c79876d2de Internal restructuring: identify no longer computes syntax.
ballarin
parents: 20032
diff changeset
   853
        val locale_params' = map (fn p => (p, Symtab.lookup tenv p |> the)) locale_params;
80c79876d2de Internal restructuring: identify no longer computes syntax.
ballarin
parents: 20032
diff changeset
   854
        val mode' = map_mode (map (Element.map_witness (inst_wit all_params))) mode;
80c79876d2de Internal restructuring: identify no longer computes syntax.
ballarin
parents: 20032
diff changeset
   855
        val ren = map fst ps ~~ map (fn p => (p, lookup_syn p)) params;
80c79876d2de Internal restructuring: identify no longer computes syntax.
ballarin
parents: 20032
diff changeset
   856
        val [env] = unify_parms ctxt all_params [map (apfst (Element.rename ren) o apsnd SOME) ps];
21499
fbd6422a847a uniform interface for type_syntax/term_syntax/declaration, dependent on morphism;
wenzelm
parents: 21483
diff changeset
   857
        val elem_morphism =
fbd6422a847a uniform interface for type_syntax/term_syntax/declaration, dependent on morphism;
wenzelm
parents: 21483
diff changeset
   858
          Element.rename_morphism ren $>
21665
ba07e24dc941 encode declarations as notes (attributes), which enables proper inheritance, interpretation etc.;
wenzelm
parents: 21602
diff changeset
   859
          Morphism.name_morphism (NameSpace.qualified (params_prefix params)) $>
21499
fbd6422a847a uniform interface for type_syntax/term_syntax/declaration, dependent on morphism;
wenzelm
parents: 21483
diff changeset
   860
          Element.instT_morphism thy env;
fbd6422a847a uniform interface for type_syntax/term_syntax/declaration, dependent on morphism;
wenzelm
parents: 21483
diff changeset
   861
        val elems' = map (Element.morph_ctxt elem_morphism) elems;
fbd6422a847a uniform interface for type_syntax/term_syntax/declaration, dependent on morphism;
wenzelm
parents: 21483
diff changeset
   862
      in (((name, map (apsnd SOME) locale_params'), mode'), elems') end;
20035
80c79876d2de Internal restructuring: identify no longer computes syntax.
ballarin
parents: 20032
diff changeset
   863
80c79876d2de Internal restructuring: identify no longer computes syntax.
ballarin
parents: 20032
diff changeset
   864
    (* parameters, their types and syntax *)
80c79876d2de Internal restructuring: identify no longer computes syntax.
ballarin
parents: 20032
diff changeset
   865
    val (all_params', tenv, syn) = params_of_expr ctxt [] expr ([], Symtab.empty, Symtab.empty);
80c79876d2de Internal restructuring: identify no longer computes syntax.
ballarin
parents: 20032
diff changeset
   866
    val all_params = map (fn p => (p, Symtab.lookup tenv p |> the)) all_params';
80c79876d2de Internal restructuring: identify no longer computes syntax.
ballarin
parents: 20032
diff changeset
   867
    (* compute identifiers and syntax, merge with previous ones *)
80c79876d2de Internal restructuring: identify no longer computes syntax.
ballarin
parents: 20032
diff changeset
   868
    val (ids, _) = identify true expr;
20951
868120282837 gen_rem(s) abandoned in favour of remove / subtract
haftmann
parents: 20911
diff changeset
   869
    val idents = subtract (eq_fst (op =)) prev_idents ids;
20035
80c79876d2de Internal restructuring: identify no longer computes syntax.
ballarin
parents: 20032
diff changeset
   870
    val syntax = merge_syntax ctxt ids (syn, prev_syntax);
80c79876d2de Internal restructuring: identify no longer computes syntax.
ballarin
parents: 20032
diff changeset
   871
    (* type-instantiate elements *)
80c79876d2de Internal restructuring: identify no longer computes syntax.
ballarin
parents: 20032
diff changeset
   872
    val final_elemss = map (eval all_params tenv syntax) idents;
16102
c5f6726d9bb1 Locale expressions: rename with optional mixfix syntax.
ballarin
parents: 16028
diff changeset
   873
  in ((prev_idents @ idents, syntax), final_elemss) end;
12046
a404358fd965 locale elements;
wenzelm
parents: 12014
diff changeset
   874
12510
172d18ec3b54 proper treatment of internal parameters;
wenzelm
parents: 12502
diff changeset
   875
end;
172d18ec3b54 proper treatment of internal parameters;
wenzelm
parents: 12502
diff changeset
   876
12070
c72fe1edc9e7 proper treatment of local syntax;
wenzelm
parents: 12063
diff changeset
   877
12529
d99716a53f59 simultaneous type-inference of complete context/statement specifications;
wenzelm
parents: 12514
diff changeset
   878
(* activate elements *)
12273
7fb9840d358d beginnings of actual locale expressions;
wenzelm
parents: 12263
diff changeset
   879
12510
172d18ec3b54 proper treatment of internal parameters;
wenzelm
parents: 12502
diff changeset
   880
local
172d18ec3b54 proper treatment of internal parameters;
wenzelm
parents: 12502
diff changeset
   881
21686
4f5f6c685ab4 export: added explicit term operation;
wenzelm
parents: 21665
diff changeset
   882
fun axioms_export axs _ As =
4f5f6c685ab4 export: added explicit term operation;
wenzelm
parents: 21665
diff changeset
   883
  (Element.satisfy_thm axs #> Drule.implies_intr_list (Library.drop (length axs, As)), fn t => t);
12263
6f2acf10e2a2 locale expressions;
wenzelm
parents: 12143
diff changeset
   884
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   885
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   886
(* NB: derived ids contain only facts at this stage *)
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   887
19931
fb32b43e7f80 Restructured locales with predicates: import is now an interpretation.
ballarin
parents: 19914
diff changeset
   888
fun activate_elem _ _ ((ctxt, mode), Fixes fixes) =
18671
621efeed255b uniform handling of fixes;
wenzelm
parents: 18617
diff changeset
   889
      ((ctxt |> ProofContext.add_fixes_i fixes |> snd, mode), [])
19931
fb32b43e7f80 Restructured locales with predicates: import is now an interpretation.
ballarin
parents: 19914
diff changeset
   890
  | activate_elem _ _ ((ctxt, mode), Constrains _) =
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   891
      ((ctxt, mode), [])
19931
fb32b43e7f80 Restructured locales with predicates: import is now an interpretation.
ballarin
parents: 19914
diff changeset
   892
  | activate_elem ax_in_ctxt _ ((ctxt, Assumed axs), Assumes asms) =
13399
c136276dc847 support locale ``views'' (for cumulative predicates);
wenzelm
parents: 13394
diff changeset
   893
      let
18728
6790126ab5f6 simplified type attribute;
wenzelm
parents: 18708
diff changeset
   894
        val asms' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) asms;
19482
9f11af8f7ef9 tuned basic list operators (flat, maps, map_filter);
wenzelm
parents: 19423
diff changeset
   895
        val ts = maps (map #1 o #2) asms';
19018
88b4979193d8 added abbreviations: activated by init, no expressions yet;
wenzelm
parents: 18964
diff changeset
   896
        val (ps, qs) = chop (length ts) axs;
17856
0551978bfda5 goal statements: accomodate before_qed argument;
wenzelm
parents: 17756
diff changeset
   897
        val (_, ctxt') =
21370
d9dd7b4e5e69 replaced Variable.fix_frees by Variable.auto_fixes (depends on body mode);
wenzelm
parents: 21361
diff changeset
   898
          ctxt |> fold Variable.auto_fixes ts
19931
fb32b43e7f80 Restructured locales with predicates: import is now an interpretation.
ballarin
parents: 19914
diff changeset
   899
          |> ProofContext.add_assms_i (axioms_export (if ax_in_ctxt then ps else [])) asms';
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   900
      in ((ctxt', Assumed qs), []) end
19931
fb32b43e7f80 Restructured locales with predicates: import is now an interpretation.
ballarin
parents: 19914
diff changeset
   901
  | activate_elem _ _ ((ctxt, Derived ths), Assumes asms) =
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   902
      ((ctxt, Derived ths), [])
19931
fb32b43e7f80 Restructured locales with predicates: import is now an interpretation.
ballarin
parents: 19914
diff changeset
   903
  | activate_elem _ _ ((ctxt, Assumed axs), Defines defs) =
15596
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
   904
      let
18728
6790126ab5f6 simplified type attribute;
wenzelm
parents: 18708
diff changeset
   905
        val defs' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) defs;
19732
1c37d117a25d activate Defines: fix frees;
wenzelm
parents: 19662
diff changeset
   906
        val asms = defs' |> map (fn ((name, atts), (t, ps)) =>
1c37d117a25d activate Defines: fix frees;
wenzelm
parents: 19662
diff changeset
   907
            let val ((c, _), t') = LocalDefs.cert_def ctxt t
20872
wenzelm
parents: 20664
diff changeset
   908
            in (t', ((Thm.def_name_optional c name, atts), [(t', ps)])) end);
17856
0551978bfda5 goal statements: accomodate before_qed argument;
wenzelm
parents: 17756
diff changeset
   909
        val (_, ctxt') =
21370
d9dd7b4e5e69 replaced Variable.fix_frees by Variable.auto_fixes (depends on body mode);
wenzelm
parents: 21361
diff changeset
   910
          ctxt |> fold (Variable.auto_fixes o #1) asms
19732
1c37d117a25d activate Defines: fix frees;
wenzelm
parents: 19662
diff changeset
   911
          |> ProofContext.add_assms_i LocalDefs.def_export (map #2 asms);
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   912
      in ((ctxt', Assumed axs), []) end
19931
fb32b43e7f80 Restructured locales with predicates: import is now an interpretation.
ballarin
parents: 19914
diff changeset
   913
  | activate_elem _ _ ((ctxt, Derived ths), Defines defs) =
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   914
      ((ctxt, Derived ths), [])
21441
940ef3e85c5a notes: proper kind;
wenzelm
parents: 21393
diff changeset
   915
  | activate_elem _ is_ext ((ctxt, mode), Notes (kind, facts)) =
15596
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
   916
      let
18728
6790126ab5f6 simplified type attribute;
wenzelm
parents: 18708
diff changeset
   917
        val facts' = Attrib.map_facts (Attrib.attribute_i (ProofContext.theory_of ctxt)) facts;
21441
940ef3e85c5a notes: proper kind;
wenzelm
parents: 21393
diff changeset
   918
        val (res, ctxt') = ctxt |> ProofContext.note_thmss_i kind facts';
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   919
      in ((ctxt', mode), if is_ext then res else []) end;
12502
9e7f72e25022 beginning support for type instantiation;
wenzelm
parents: 12323
diff changeset
   920
19931
fb32b43e7f80 Restructured locales with predicates: import is now an interpretation.
ballarin
parents: 19914
diff changeset
   921
fun activate_elems ax_in_ctxt (((name, ps), mode), elems) ctxt =
17033
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   922
  let
18123
1bb572e8cee9 avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents: 18038
diff changeset
   923
    val thy = ProofContext.theory_of ctxt;
17033
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   924
    val ((ctxt', _), res) =
21441
940ef3e85c5a notes: proper kind;
wenzelm
parents: 21393
diff changeset
   925
      foldl_map (activate_elem ax_in_ctxt (name = ""))
940ef3e85c5a notes: proper kind;
wenzelm
parents: 21393
diff changeset
   926
        ((ProofContext.qualified_names ctxt, mode), elems)
940ef3e85c5a notes: proper kind;
wenzelm
parents: 21393
diff changeset
   927
      handle ERROR msg => err_in_locale ctxt msg [(name, map fst ps)];
15696
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   928
    val ctxt'' = if name = "" then ctxt'
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   929
          else let
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   930
              val ps' = map (fn (n, SOME T) => Free (n, T)) ps;
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   931
              val ctxt'' = put_local_registration (name, ps') ("", []) ctxt'
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   932
            in case mode of
18123
1bb572e8cee9 avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents: 18038
diff changeset
   933
                Assumed axs =>
19780
dce2168b0ea4 export read/cert_expr;
wenzelm
parents: 19732
diff changeset
   934
                  fold (add_local_witness (name, ps') o
dce2168b0ea4 export read/cert_expr;
wenzelm
parents: 19732
diff changeset
   935
                    Element.assume_witness thy o Element.witness_prop) axs ctxt''
18123
1bb572e8cee9 avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents: 18038
diff changeset
   936
              | Derived ths => fold (add_local_witness (name, ps')) ths ctxt''
15696
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   937
            end
16144
e339119f4261 renamed cond_extern to extern;
wenzelm
parents: 16105
diff changeset
   938
  in (ProofContext.restore_naming ctxt ctxt'', res) end;
13399
c136276dc847 support locale ``views'' (for cumulative predicates);
wenzelm
parents: 13394
diff changeset
   939
19931
fb32b43e7f80 Restructured locales with predicates: import is now an interpretation.
ballarin
parents: 19914
diff changeset
   940
fun activate_elemss ax_in_ctxt prep_facts =
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   941
    fold_map (fn (((name, ps), mode), raw_elems) => fn ctxt =>
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   942
      let
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   943
        val elems = map (prep_facts ctxt) raw_elems;
19482
9f11af8f7ef9 tuned basic list operators (flat, maps, map_filter);
wenzelm
parents: 19423
diff changeset
   944
        val (ctxt', res) = apsnd flat
19931
fb32b43e7f80 Restructured locales with predicates: import is now an interpretation.
ballarin
parents: 19914
diff changeset
   945
            (activate_elems ax_in_ctxt (((name, ps), mode), elems) ctxt);
21530
9e2ff9d4b2b0 Element.map_ctxt_attrib;
wenzelm
parents: 21523
diff changeset
   946
        val elems' = elems |> map (Element.map_ctxt_attrib Args.closure);
19931
fb32b43e7f80 Restructured locales with predicates: import is now an interpretation.
ballarin
parents: 19914
diff changeset
   947
      in (((((name, ps), mode), elems'), res), ctxt') end);
12834
e5bec3268932 added locale_facts(_i) interface (useful for simple ML proof tools);
wenzelm
parents: 12806
diff changeset
   948
12546
wenzelm
parents: 12532
diff changeset
   949
in
wenzelm
parents: 12532
diff changeset
   950
15206
09d78ec709c7 Modified locales: improved implementation of "includes".
ballarin
parents: 15127
diff changeset
   951
(* CB: activate_facts prep_facts (ctxt, elemss),
09d78ec709c7 Modified locales: improved implementation of "includes".
ballarin
parents: 15127
diff changeset
   952
   where elemss is a list of pairs consisting of identifiers and
09d78ec709c7 Modified locales: improved implementation of "includes".
ballarin
parents: 15127
diff changeset
   953
   context elements, extends ctxt by the context elements yielding
09d78ec709c7 Modified locales: improved implementation of "includes".
ballarin
parents: 15127
diff changeset
   954
   ctxt' and returns (ctxt', (elemss', facts)).
09d78ec709c7 Modified locales: improved implementation of "includes".
ballarin
parents: 15127
diff changeset
   955
   Identifiers in the argument are of the form ((name, ps), axs) and
09d78ec709c7 Modified locales: improved implementation of "includes".
ballarin
parents: 15127
diff changeset
   956
   assumptions use the axioms in the identifiers to set up exporters
09d78ec709c7 Modified locales: improved implementation of "includes".
ballarin
parents: 15127
diff changeset
   957
   in ctxt'.  elemss' does not contain identifiers and is obtained
09d78ec709c7 Modified locales: improved implementation of "includes".
ballarin
parents: 15127
diff changeset
   958
   from elemss and the intermediate context with prep_facts.
15703
727ef1b8b3ee *** empty log message ***
wenzelm
parents: 15696
diff changeset
   959
   If read_facts or cert_facts is used for prep_facts, these also remove
14508
859b11514537 Experimental command for instantiation of locales in proof contexts:
ballarin
parents: 14446
diff changeset
   960
   the internal/external markers from elemss. *)
859b11514537 Experimental command for instantiation of locales in proof contexts:
ballarin
parents: 14446
diff changeset
   961
19931
fb32b43e7f80 Restructured locales with predicates: import is now an interpretation.
ballarin
parents: 19914
diff changeset
   962
fun activate_facts ax_in_ctxt prep_facts (ctxt, args) =
fb32b43e7f80 Restructured locales with predicates: import is now an interpretation.
ballarin
parents: 19914
diff changeset
   963
  let val ((elemss, factss), ctxt') = activate_elemss ax_in_ctxt prep_facts args ctxt |>> split_list
19482
9f11af8f7ef9 tuned basic list operators (flat, maps, map_filter);
wenzelm
parents: 19423
diff changeset
   964
  in (ctxt', (elemss, flat factss)) end;
15703
727ef1b8b3ee *** empty log message ***
wenzelm
parents: 15696
diff changeset
   965
12510
172d18ec3b54 proper treatment of internal parameters;
wenzelm
parents: 12502
diff changeset
   966
end;
172d18ec3b54 proper treatment of internal parameters;
wenzelm
parents: 12502
diff changeset
   967
12307
459aa05af6be qualify imported facts;
wenzelm
parents: 12289
diff changeset
   968
15696
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   969
18137
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
   970
(** prepare locale elements **)
12529
d99716a53f59 simultaneous type-inference of complete context/statement specifications;
wenzelm
parents: 12514
diff changeset
   971
d99716a53f59 simultaneous type-inference of complete context/statement specifications;
wenzelm
parents: 12514
diff changeset
   972
(* expressions *)
d99716a53f59 simultaneous type-inference of complete context/statement specifications;
wenzelm
parents: 12514
diff changeset
   973
16458
4c6fd0c01d28 accomodate change of TheoryDataFun;
wenzelm
parents: 16346
diff changeset
   974
fun intern_expr thy (Locale xname) = Locale (intern thy xname)
4c6fd0c01d28 accomodate change of TheoryDataFun;
wenzelm
parents: 16346
diff changeset
   975
  | intern_expr thy (Merge exprs) = Merge (map (intern_expr thy) exprs)
4c6fd0c01d28 accomodate change of TheoryDataFun;
wenzelm
parents: 16346
diff changeset
   976
  | intern_expr thy (Rename (expr, xs)) = Rename (intern_expr thy expr, xs);
12529
d99716a53f59 simultaneous type-inference of complete context/statement specifications;
wenzelm
parents: 12514
diff changeset
   977
d99716a53f59 simultaneous type-inference of complete context/statement specifications;
wenzelm
parents: 12514
diff changeset
   978
d99716a53f59 simultaneous type-inference of complete context/statement specifications;
wenzelm
parents: 12514
diff changeset
   979
(* propositions and bindings *)
d99716a53f59 simultaneous type-inference of complete context/statement specifications;
wenzelm
parents: 12514
diff changeset
   980
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   981
(* flatten (ctxt, prep_expr) ((ids, syn), expr)
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   982
   normalises expr (which is either a locale
14508
859b11514537 Experimental command for instantiation of locales in proof contexts:
ballarin
parents: 14446
diff changeset
   983
   expression or a single context element) wrt.
859b11514537 Experimental command for instantiation of locales in proof contexts:
ballarin
parents: 14446
diff changeset
   984
   to the list ids of already accumulated identifiers.
19783
82f365a14960 Improved parameter management of locales.
ballarin
parents: 19780
diff changeset
   985
   It returns ((ids', syn'), elemss) where ids' is an extension of ids
14508
859b11514537 Experimental command for instantiation of locales in proof contexts:
ballarin
parents: 14446
diff changeset
   986
   with identifiers generated for expr, and elemss is the list of
16102
c5f6726d9bb1 Locale expressions: rename with optional mixfix syntax.
ballarin
parents: 16028
diff changeset
   987
   context elements generated from expr.
c5f6726d9bb1 Locale expressions: rename with optional mixfix syntax.
ballarin
parents: 16028
diff changeset
   988
   syn and syn' are symtabs mapping parameter names to their syntax.  syn'
c5f6726d9bb1 Locale expressions: rename with optional mixfix syntax.
ballarin
parents: 16028
diff changeset
   989
   is an extension of syn.
c5f6726d9bb1 Locale expressions: rename with optional mixfix syntax.
ballarin
parents: 16028
diff changeset
   990
   For details, see flatten_expr.
c5f6726d9bb1 Locale expressions: rename with optional mixfix syntax.
ballarin
parents: 16028
diff changeset
   991
15596
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
   992
   Additionally, for a locale expression, the elems are grouped into a single
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
   993
   Int; individual context elements are marked Ext.  In this case, the
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
   994
   identifier-like information of the element is as follows:
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
   995
   - for Fixes: (("", ps), []) where the ps have type info NONE
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
   996
   - for other elements: (("", []), []).
15206
09d78ec709c7 Modified locales: improved implementation of "includes".
ballarin
parents: 15127
diff changeset
   997
   The implementation of activate_facts relies on identifier names being
09d78ec709c7 Modified locales: improved implementation of "includes".
ballarin
parents: 15127
diff changeset
   998
   empty strings for external elements.
15596
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
   999
*)
14508
859b11514537 Experimental command for instantiation of locales in proof contexts:
ballarin
parents: 14446
diff changeset
  1000
16102
c5f6726d9bb1 Locale expressions: rename with optional mixfix syntax.
ballarin
parents: 16028
diff changeset
  1001
fun flatten (ctxt, _) ((ids, syn), Elem (Fixes fixes)) = let
18137
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
  1002
        val ids' = ids @ [(("", map #1 fixes), ([], Assumed []))]
16102
c5f6726d9bb1 Locale expressions: rename with optional mixfix syntax.
ballarin
parents: 16028
diff changeset
  1003
      in
18137
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
  1004
        ((ids',
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
  1005
         merge_syntax ctxt ids'
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
  1006
           (syn, Symtab.make (map (fn fx => (#1 fx, #3 fx)) fixes))
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
  1007
           handle Symtab.DUPS xs => err_in_locale ctxt
19931
fb32b43e7f80 Restructured locales with predicates: import is now an interpretation.
ballarin
parents: 19914
diff changeset
  1008
             ("Conflicting syntax for parameters: " ^ commas_quote xs)
16102
c5f6726d9bb1 Locale expressions: rename with optional mixfix syntax.
ballarin
parents: 16028
diff changeset
  1009
             (map #1 ids')),
18137
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
  1010
         [((("", map (rpair NONE o #1) fixes), Assumed []), Ext (Fixes fixes))])
16102
c5f6726d9bb1 Locale expressions: rename with optional mixfix syntax.
ballarin
parents: 16028
diff changeset
  1011
      end
c5f6726d9bb1 Locale expressions: rename with optional mixfix syntax.
ballarin
parents: 16028
diff changeset
  1012
  | flatten _ ((ids, syn), Elem elem) =
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
  1013
      ((ids @ [(("", []), ([], Assumed []))], syn), [((("", []), Assumed []), Ext elem)])
16102
c5f6726d9bb1 Locale expressions: rename with optional mixfix syntax.
ballarin
parents: 16028
diff changeset
  1014
  | flatten (ctxt, prep_expr) ((ids, syn), Expr expr) =
c5f6726d9bb1 Locale expressions: rename with optional mixfix syntax.
ballarin
parents: 16028
diff changeset
  1015
      apsnd (map (apsnd Int)) (flatten_expr ctxt ((ids, syn), prep_expr expr));
14508
859b11514537 Experimental command for instantiation of locales in proof contexts:
ballarin
parents: 14446
diff changeset
  1016
12529
d99716a53f59 simultaneous type-inference of complete context/statement specifications;
wenzelm
parents: 12514
diff changeset
  1017
local
d99716a53f59 simultaneous type-inference of complete context/statement specifications;
wenzelm
parents: 12514
diff changeset
  1018
12839
584a3e0b00f2 reorganized code for predicate text;
wenzelm
parents: 12834
diff changeset
  1019
local
584a3e0b00f2 reorganized code for predicate text;
wenzelm
parents: 12834
diff changeset
  1020
12727
330cb92aaea3 unify_frozen: proper use of maxidx';
wenzelm
parents: 12711
diff changeset
  1021
fun declare_int_elem (ctxt, Fixes fixes) =
18671
621efeed255b uniform handling of fixes;
wenzelm
parents: 18617
diff changeset
  1022
      (ctxt |> ProofContext.add_fixes_i (map (fn (x, T, mx) =>
621efeed255b uniform handling of fixes;
wenzelm
parents: 18617
diff changeset
  1023
        (x, Option.map (Term.map_type_tfree (TypeInfer.param 0)) T, mx)) fixes) |> snd, [])
12727
330cb92aaea3 unify_frozen: proper use of maxidx';
wenzelm
parents: 12711
diff changeset
  1024
  | declare_int_elem (ctxt, _) = (ctxt, []);
12529
d99716a53f59 simultaneous type-inference of complete context/statement specifications;
wenzelm
parents: 12514
diff changeset
  1025
18671
621efeed255b uniform handling of fixes;
wenzelm
parents: 18617
diff changeset
  1026
fun declare_ext_elem prep_vars (ctxt, Fixes fixes) =
621efeed255b uniform handling of fixes;
wenzelm
parents: 18617
diff changeset
  1027
      let val (vars, _) = prep_vars fixes ctxt
621efeed255b uniform handling of fixes;
wenzelm
parents: 18617
diff changeset
  1028
      in (ctxt |> ProofContext.add_fixes_i vars |> snd, []) end
621efeed255b uniform handling of fixes;
wenzelm
parents: 18617
diff changeset
  1029
  | declare_ext_elem prep_vars (ctxt, Constrains csts) =
621efeed255b uniform handling of fixes;
wenzelm
parents: 18617
diff changeset
  1030
      let val (_, ctxt') = prep_vars (map (fn (x, T) => (x, SOME T, NoSyn)) csts) ctxt
621efeed255b uniform handling of fixes;
wenzelm
parents: 18617
diff changeset
  1031
      in (ctxt', []) end
12529
d99716a53f59 simultaneous type-inference of complete context/statement specifications;
wenzelm
parents: 12514
diff changeset
  1032
  | declare_ext_elem _ (ctxt, Assumes asms) = (ctxt, map #2 asms)
19585
70a1ce3b23ae removed 'concl is' patterns;
wenzelm
parents: 19482
diff changeset
  1033
  | declare_ext_elem _ (ctxt, Defines defs) = (ctxt, map (fn (_, (t, ps)) => [(t, ps)]) defs)
21441
940ef3e85c5a notes: proper kind;
wenzelm
parents: 21393
diff changeset
  1034
  | declare_ext_elem _ (ctxt, Notes _) = (ctxt, []);
12529
d99716a53f59 simultaneous type-inference of complete context/statement specifications;
wenzelm
parents: 12514
diff changeset
  1035
18671
621efeed255b uniform handling of fixes;
wenzelm
parents: 18617
diff changeset
  1036
fun declare_elems prep_vars (ctxt, (((name, ps), Assumed _), elems)) =
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
  1037
    let val (ctxt', propps) =
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
  1038
      (case elems of
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
  1039
        Int es => foldl_map declare_int_elem (ctxt, es)
18671
621efeed255b uniform handling of fixes;
wenzelm
parents: 18617
diff changeset
  1040
      | Ext e => foldl_map (declare_ext_elem prep_vars) (ctxt, [e]))
18678
dd0c569fa43d sane ERROR handling;
wenzelm
parents: 18671
diff changeset
  1041
      handle ERROR msg => err_in_locale ctxt msg [(name, map fst ps)]
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
  1042
    in (ctxt', propps) end
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
  1043
  | declare_elems _ (ctxt, ((_, Derived _), elems)) = (ctxt, []);
12727
330cb92aaea3 unify_frozen: proper use of maxidx';
wenzelm
parents: 12711
diff changeset
  1044
12839
584a3e0b00f2 reorganized code for predicate text;
wenzelm
parents: 12834
diff changeset
  1045
in
584a3e0b00f2 reorganized code for predicate text;
wenzelm
parents: 12834
diff changeset
  1046
18671
621efeed255b uniform handling of fixes;
wenzelm
parents: 18617
diff changeset
  1047
fun declare_elemss prep_vars fixed_params raw_elemss ctxt =
12727
330cb92aaea3 unify_frozen: proper use of maxidx';
wenzelm
parents: 12711
diff changeset
  1048
  let
14215
ebf291f3b449 Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents: 13629
diff changeset
  1049
    (* CB: fix of type bug of goal in target with context elements.
ebf291f3b449 Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents: 13629
diff changeset
  1050
       Parameters new in context elements must receive types that are
ebf291f3b449 Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents: 13629
diff changeset
  1051
       distinct from types of parameters in target (fixed_params).  *)
ebf291f3b449 Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents: 13629
diff changeset
  1052
    val ctxt_with_fixed =
19900
21a99d88d925 ProofContext: moved variable operations to struct Variable;
wenzelm
parents: 19873
diff changeset
  1053
      fold Variable.declare_term (map Free fixed_params) ctxt;
12727
330cb92aaea3 unify_frozen: proper use of maxidx';
wenzelm
parents: 12711
diff changeset
  1054
    val int_elemss =
330cb92aaea3 unify_frozen: proper use of maxidx';
wenzelm
parents: 12711
diff changeset
  1055
      raw_elemss
19482
9f11af8f7ef9 tuned basic list operators (flat, maps, map_filter);
wenzelm
parents: 19423
diff changeset
  1056
      |> map_filter (fn (id, Int es) => SOME (id, es) | _ => NONE)
14215
ebf291f3b449 Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents: 13629
diff changeset
  1057
      |> unify_elemss ctxt_with_fixed fixed_params;
12727
330cb92aaea3 unify_frozen: proper use of maxidx';
wenzelm
parents: 12711
diff changeset
  1058
    val (_, raw_elemss') =
330cb92aaea3 unify_frozen: proper use of maxidx';
wenzelm
parents: 12711
diff changeset
  1059
      foldl_map (fn ((_, es) :: elemss, (id, Int _)) => (elemss, (id, Int es)) | x => x)
330cb92aaea3 unify_frozen: proper use of maxidx';
wenzelm
parents: 12711
diff changeset
  1060
        (int_elemss, raw_elemss);
18671
621efeed255b uniform handling of fixes;
wenzelm
parents: 18617
diff changeset
  1061
  in foldl_map (declare_elems prep_vars) (ctxt, raw_elemss') end;
12529
d99716a53f59 simultaneous type-inference of complete context/statement specifications;
wenzelm
parents: 12514
diff changeset
  1062
12839
584a3e0b00f2 reorganized code for predicate text;
wenzelm
parents: 12834
diff changeset
  1063
end;
12529
d99716a53f59 simultaneous type-inference of complete context/statement specifications;
wenzelm
parents: 12514
diff changeset
  1064
12839
584a3e0b00f2 reorganized code for predicate text;
wenzelm
parents: 12834
diff changeset
  1065
local
584a3e0b00f2 reorganized code for predicate text;
wenzelm
parents: 12834
diff changeset
  1066
584a3e0b00f2 reorganized code for predicate text;
wenzelm
parents: 12834
diff changeset
  1067
val norm_term = Envir.beta_norm oo Term.subst_atomic;
584a3e0b00f2 reorganized code for predicate text;
wenzelm
parents: 12834
diff changeset
  1068
16458
4c6fd0c01d28 accomodate change of TheoryDataFun;
wenzelm
parents: 16346
diff changeset
  1069
fun abstract_thm thy eq =
4c6fd0c01d28 accomodate change of TheoryDataFun;
wenzelm
parents: 16346
diff changeset
  1070
  Thm.assume (Thm.cterm_of thy eq) |> Drule.gen_all |> Drule.abs_def;
12502
9e7f72e25022 beginning support for type instantiation;
wenzelm
parents: 12323
diff changeset
  1071
18190
b7748c77562f tuned Pattern.match/unify;
wenzelm
parents: 18137
diff changeset
  1072
fun bind_def ctxt (name, ps) eq (xs, env, ths) =
12839
584a3e0b00f2 reorganized code for predicate text;
wenzelm
parents: 12834
diff changeset
  1073
  let
18831
f1315d118059 LocalDefs;
wenzelm
parents: 18806
diff changeset
  1074
    val ((y, T), b) = LocalDefs.abs_def eq;
13308
1dbed9ea764b clarified text content of locale body;
wenzelm
parents: 13297
diff changeset
  1075
    val b' = norm_term env b;
16458
4c6fd0c01d28 accomodate change of TheoryDataFun;
wenzelm
parents: 16346
diff changeset
  1076
    val th = abstract_thm (ProofContext.theory_of ctxt) eq;
13308
1dbed9ea764b clarified text content of locale body;
wenzelm
parents: 13297
diff changeset
  1077
    fun err msg = err_in_locale ctxt (msg ^ ": " ^ quote y) [(name, map fst ps)];
12839
584a3e0b00f2 reorganized code for predicate text;
wenzelm
parents: 12834
diff changeset
  1078
  in
21962
279b129498b6 removed conditional combinator;
wenzelm
parents: 21708
diff changeset
  1079
    exists (equal y o #1) xs andalso
279b129498b6 removed conditional combinator;
wenzelm
parents: 21708
diff changeset
  1080
      err "Attempt to define previously specified variable";
279b129498b6 removed conditional combinator;
wenzelm
parents: 21708
diff changeset
  1081
    exists (fn (Free (y', _), _) => y = y' | _ => false) env andalso
279b129498b6 removed conditional combinator;
wenzelm
parents: 21708
diff changeset
  1082
      err "Attempt to redefine variable";
16861
7446b4be013b tuned fold on terms;
wenzelm
parents: 16850
diff changeset
  1083
    (Term.add_frees b' xs, (Free (y, T), b') :: env, th :: ths)
12839
584a3e0b00f2 reorganized code for predicate text;
wenzelm
parents: 12834
diff changeset
  1084
  end;
12575
34985eee55b1 fixed inst_thm: proper domain of env;
wenzelm
parents: 12546
diff changeset
  1085
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
  1086
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
  1087
(* CB: for finish_elems (Int and Ext),
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
  1088
   extracts specification, only of assumed elements *)
15206
09d78ec709c7 Modified locales: improved implementation of "includes".
ballarin
parents: 15127
diff changeset
  1089
18190
b7748c77562f tuned Pattern.match/unify;
wenzelm
parents: 18137
diff changeset
  1090
fun eval_text _ _ _ (Fixes _) text = text
b7748c77562f tuned Pattern.match/unify;
wenzelm
parents: 18137
diff changeset
  1091
  | eval_text _ _ _ (Constrains _) text = text
b7748c77562f tuned Pattern.match/unify;
wenzelm
parents: 18137
diff changeset
  1092
  | eval_text _ (_, Assumed _) is_ext (Assumes asms)
b7748c77562f tuned Pattern.match/unify;
wenzelm
parents: 18137
diff changeset
  1093
        (((exts, exts'), (ints, ints')), (xs, env, defs)) =
13394
b39347206719 define cumulative predicate view;
wenzelm
parents: 13375
diff changeset
  1094
      let
19482
9f11af8f7ef9 tuned basic list operators (flat, maps, map_filter);
wenzelm
parents: 19423
diff changeset
  1095
        val ts = maps (map #1 o #2) asms;
13394
b39347206719 define cumulative predicate view;
wenzelm
parents: 13375
diff changeset
  1096
        val ts' = map (norm_term env) ts;
b39347206719 define cumulative predicate view;
wenzelm
parents: 13375
diff changeset
  1097
        val spec' =
b39347206719 define cumulative predicate view;
wenzelm
parents: 13375
diff changeset
  1098
          if is_ext then ((exts @ ts, exts' @ ts'), (ints, ints'))
b39347206719 define cumulative predicate view;
wenzelm
parents: 13375
diff changeset
  1099
          else ((exts, exts'), (ints @ ts, ints' @ ts'));
16861
7446b4be013b tuned fold on terms;
wenzelm
parents: 16850
diff changeset
  1100
      in (spec', (fold Term.add_frees ts' xs, env, defs)) end
18190
b7748c77562f tuned Pattern.match/unify;
wenzelm
parents: 18137
diff changeset
  1101
  | eval_text _ (_, Derived _) _ (Assumes _) text = text
b7748c77562f tuned Pattern.match/unify;
wenzelm
parents: 18137
diff changeset
  1102
  | eval_text ctxt (id, Assumed _) _ (Defines defs) (spec, binds) =
b7748c77562f tuned Pattern.match/unify;
wenzelm
parents: 18137
diff changeset
  1103
      (spec, fold (bind_def ctxt id o #1 o #2) defs binds)
b7748c77562f tuned Pattern.match/unify;
wenzelm
parents: 18137
diff changeset
  1104
  | eval_text _ (_, Derived _) _ (Defines _) text = text
b7748c77562f tuned Pattern.match/unify;
wenzelm
parents: 18137
diff changeset
  1105
  | eval_text _ _ _ (Notes _) text = text;
13308
1dbed9ea764b clarified text content of locale body;
wenzelm
parents: 13297
diff changeset
  1106
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
  1107
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
  1108
(* for finish_elems (Int),
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
  1109
   remove redundant elements of derived identifiers,
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
  1110
   turn assumptions and definitions into facts,
21483
e4be91feca50 replaced Args.map_values/Element.map_ctxt_values by general morphism application;
wenzelm
parents: 21441
diff changeset
  1111
   satisfy hypotheses of facts *)
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
  1112
17096
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
  1113
fun finish_derived _ _ (Assumed _) (Fixes fixes) = SOME (Fixes fixes)
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
  1114
  | finish_derived _ _ (Assumed _) (Constrains csts) = SOME (Constrains csts)
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
  1115
  | finish_derived _ _ (Assumed _) (Assumes asms) = SOME (Assumes asms)
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
  1116
  | finish_derived _ _ (Assumed _) (Defines defs) = SOME (Defines defs)
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
  1117
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
  1118
  | finish_derived _ _ (Derived _) (Fixes _) = NONE
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
  1119
  | finish_derived _ _ (Derived _) (Constrains _) = NONE
21483
e4be91feca50 replaced Args.map_values/Element.map_ctxt_values by general morphism application;
wenzelm
parents: 21441
diff changeset
  1120
  | finish_derived sign satisfy (Derived _) (Assumes asms) = asms
17096
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
  1121
      |> map (apsnd (map (fn (a, _) => ([Thm.assume (cterm_of sign a)], []))))
21441
940ef3e85c5a notes: proper kind;
wenzelm
parents: 21393
diff changeset
  1122
      |> pair Thm.assumptionK |> Notes
21483
e4be91feca50 replaced Args.map_values/Element.map_ctxt_values by general morphism application;
wenzelm
parents: 21441
diff changeset
  1123
      |> Element.morph_ctxt satisfy |> SOME
e4be91feca50 replaced Args.map_values/Element.map_ctxt_values by general morphism application;
wenzelm
parents: 21441
diff changeset
  1124
  | finish_derived sign satisfy (Derived _) (Defines defs) = defs
17096
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
  1125
      |> map (apsnd (fn (d, _) => [([Thm.assume (cterm_of sign d)], [])]))
21441
940ef3e85c5a notes: proper kind;
wenzelm
parents: 21393
diff changeset
  1126
      |> pair Thm.definitionK |> Notes
21483
e4be91feca50 replaced Args.map_values/Element.map_ctxt_values by general morphism application;
wenzelm
parents: 21441
diff changeset
  1127
      |> Element.morph_ctxt satisfy |> SOME
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
  1128
21483
e4be91feca50 replaced Args.map_values/Element.map_ctxt_values by general morphism application;
wenzelm
parents: 21441
diff changeset
  1129
  | finish_derived _ satisfy _ (Notes facts) = Notes facts
e4be91feca50 replaced Args.map_values/Element.map_ctxt_values by general morphism application;
wenzelm
parents: 21441
diff changeset
  1130
      |> Element.morph_ctxt satisfy |> SOME;
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
  1131
15206
09d78ec709c7 Modified locales: improved implementation of "includes".
ballarin
parents: 15127
diff changeset
  1132
(* CB: for finish_elems (Ext) *)
09d78ec709c7 Modified locales: improved implementation of "includes".
ballarin
parents: 15127
diff changeset
  1133
13308
1dbed9ea764b clarified text content of locale body;
wenzelm
parents: 13297
diff changeset
  1134
fun closeup _ false elem = elem
1dbed9ea764b clarified text content of locale body;
wenzelm
parents: 13297
diff changeset
  1135
  | closeup ctxt true elem =
12839
584a3e0b00f2 reorganized code for predicate text;
wenzelm
parents: 12834
diff changeset
  1136
      let
13308
1dbed9ea764b clarified text content of locale body;
wenzelm
parents: 13297
diff changeset
  1137
        fun close_frees t =
19900
21a99d88d925 ProofContext: moved variable operations to struct Variable;
wenzelm
parents: 19873
diff changeset
  1138
          let val frees = rev (filter_out (Variable.is_fixed ctxt o #1) (Term.add_frees t []))
13308
1dbed9ea764b clarified text content of locale body;
wenzelm
parents: 13297
diff changeset
  1139
          in Term.list_all_free (frees, t) end;
1dbed9ea764b clarified text content of locale body;
wenzelm
parents: 13297
diff changeset
  1140
1dbed9ea764b clarified text content of locale body;
wenzelm
parents: 13297
diff changeset
  1141
        fun no_binds [] = []
18678
dd0c569fa43d sane ERROR handling;
wenzelm
parents: 18671
diff changeset
  1142
          | no_binds _ = error "Illegal term bindings in locale element";
13308
1dbed9ea764b clarified text content of locale body;
wenzelm
parents: 13297
diff changeset
  1143
      in
1dbed9ea764b clarified text content of locale body;
wenzelm
parents: 13297
diff changeset
  1144
        (case elem of
1dbed9ea764b clarified text content of locale body;
wenzelm
parents: 13297
diff changeset
  1145
          Assumes asms => Assumes (asms |> map (fn (a, propps) =>
19585
70a1ce3b23ae removed 'concl is' patterns;
wenzelm
parents: 19482
diff changeset
  1146
            (a, map (fn (t, ps) => (close_frees t, no_binds ps)) propps)))
13308
1dbed9ea764b clarified text content of locale body;
wenzelm
parents: 13297
diff changeset
  1147
        | Defines defs => Defines (defs |> map (fn (a, (t, ps)) =>
18831
f1315d118059 LocalDefs;
wenzelm
parents: 18806
diff changeset
  1148
            (a, (close_frees (#2 (LocalDefs.cert_def ctxt t)), no_binds ps))))
13308
1dbed9ea764b clarified text content of locale body;
wenzelm
parents: 13297
diff changeset
  1149
        | e => e)
1dbed9ea764b clarified text content of locale body;
wenzelm
parents: 13297
diff changeset
  1150
      end;
12839
584a3e0b00f2 reorganized code for predicate text;
wenzelm
parents: 12834
diff changeset
  1151
12502
9e7f72e25022 beginning support for type instantiation;
wenzelm
parents: 12323
diff changeset
  1152
12839
584a3e0b00f2 reorganized code for predicate text;
wenzelm
parents: 12834
diff changeset
  1153
fun finish_ext_elem parms _ (Fixes fixes, _) = Fixes (map (fn (x, _, mx) =>
17271
2756a73f63a5 introduced some new-style AList operations
haftmann
parents: 17257
diff changeset
  1154
      (x, AList.lookup (op =) parms x, mx)) fixes)
18899
a8e913c93578 theorem(_in_locale): Element.statement, Obtain.statement;
wenzelm
parents: 18890
diff changeset
  1155
  | finish_ext_elem parms _ (Constrains _, _) = Constrains []
12839
584a3e0b00f2 reorganized code for predicate text;
wenzelm
parents: 12834
diff changeset
  1156
  | finish_ext_elem _ close (Assumes asms, propp) =
584a3e0b00f2 reorganized code for predicate text;
wenzelm
parents: 12834
diff changeset
  1157
      close (Assumes (map #1 asms ~~ propp))
584a3e0b00f2 reorganized code for predicate text;
wenzelm
parents: 12834
diff changeset
  1158
  | finish_ext_elem _ close (Defines defs, propp) =
19585
70a1ce3b23ae removed 'concl is' patterns;
wenzelm
parents: 19482
diff changeset
  1159
      close (Defines (map #1 defs ~~ map (fn [(t, ps)] => (t, ps)) propp))
12839
584a3e0b00f2 reorganized code for predicate text;
wenzelm
parents: 12834
diff changeset
  1160
  | finish_ext_elem _ _ (Notes facts, _) = Notes facts;
584a3e0b00f2 reorganized code for predicate text;
wenzelm
parents: 12834
diff changeset
  1161
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
  1162
15206
09d78ec709c7 Modified locales: improved implementation of "includes".
ballarin
parents: 15127
diff changeset
  1163
(* CB: finish_parms introduces type info from parms to identifiers *)
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15456
diff changeset
  1164
(* CB: only needed for types that have been NONE so far???
15206
09d78ec709c7 Modified locales: improved implementation of "includes".
ballarin
parents: 15127
diff changeset
  1165
   If so, which are these??? *)
09d78ec709c7 Modified locales: improved implementation of "includes".
ballarin
parents: 15127
diff changeset
  1166
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
  1167
fun finish_parms parms (((name, ps), mode), elems) =
19932
63bd0eeb4e0d fixed sml/nj value restriction problem
haftmann
parents: 19931
diff changeset
  1168
  (((name, map (fn (x, _) => (x, AList.lookup (op = : string * string -> bool) parms x)) ps), mode), elems);
12839
584a3e0b00f2 reorganized code for predicate text;
wenzelm
parents: 12834
diff changeset
  1169
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
  1170
fun finish_elems ctxt parms _ ((text, wits), ((id, Int e), _)) =
12839
584a3e0b00f2 reorganized code for predicate text;
wenzelm
parents: 12834
diff changeset
  1171
      let
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
  1172
        val [(id' as (_, mode), es)] = unify_elemss ctxt parms [(id, e)];
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
  1173
        val wits' = case mode of Assumed _ => wits | Derived ths => wits @ ths;
18190
b7748c77562f tuned Pattern.match/unify;
wenzelm
parents: 18137
diff changeset
  1174
        val text' = fold (eval_text ctxt id' false) es text;
19482
9f11af8f7ef9 tuned basic list operators (flat, maps, map_filter);
wenzelm
parents: 19423
diff changeset
  1175
        val es' = map_filter
21483
e4be91feca50 replaced Args.map_values/Element.map_ctxt_values by general morphism application;
wenzelm
parents: 21441
diff changeset
  1176
          (finish_derived (ProofContext.theory_of ctxt) (Element.satisfy_morphism wits') mode) es;
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
  1177
      in ((text', wits'), (id', map Int es')) end
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
  1178
  | finish_elems ctxt parms do_close ((text, wits), ((id, Ext e), [propp])) =
13308
1dbed9ea764b clarified text content of locale body;
wenzelm
parents: 13297
diff changeset
  1179
      let
1dbed9ea764b clarified text content of locale body;
wenzelm
parents: 13297
diff changeset
  1180
        val e' = finish_ext_elem parms (closeup ctxt do_close) (e, propp);
18190
b7748c77562f tuned Pattern.match/unify;
wenzelm
parents: 18137
diff changeset
  1181
        val text' = eval_text ctxt id true e' text;
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
  1182
      in ((text', wits), (id, [Ext e'])) end
12839
584a3e0b00f2 reorganized code for predicate text;
wenzelm
parents: 12834
diff changeset
  1183
584a3e0b00f2 reorganized code for predicate text;
wenzelm
parents: 12834
diff changeset
  1184
in
12510
172d18ec3b54 proper treatment of internal parameters;
wenzelm
parents: 12502
diff changeset
  1185
15206
09d78ec709c7 Modified locales: improved implementation of "includes".
ballarin
parents: 15127
diff changeset
  1186
(* CB: only called by prep_elemss *)
09d78ec709c7 Modified locales: improved implementation of "includes".
ballarin
parents: 15127
diff changeset
  1187
13375
7cbf2dea46d0 proper predicate definitions of locale body;
wenzelm
parents: 13336
diff changeset
  1188
fun finish_elemss ctxt parms do_close =
7cbf2dea46d0 proper predicate definitions of locale body;
wenzelm
parents: 13336
diff changeset
  1189
  foldl_map (apsnd (finish_parms parms) o finish_elems ctxt parms do_close);
12839
584a3e0b00f2 reorganized code for predicate text;
wenzelm
parents: 12834
diff changeset
  1190
584a3e0b00f2 reorganized code for predicate text;
wenzelm
parents: 12834
diff changeset
  1191
end;
584a3e0b00f2 reorganized code for predicate text;
wenzelm
parents: 12834
diff changeset
  1192
16736
1e792b32abef Preparations for interpretation of locales in locales.
ballarin
parents: 16620
diff changeset
  1193
19942
dc92e3aebc71 Improved handling of defines imported in duplicate.
ballarin
parents: 19932
diff changeset
  1194
(* Remove duplicate Defines elements: temporary workaround to fix Afp/Category. *)
dc92e3aebc71 Improved handling of defines imported in duplicate.
ballarin
parents: 19932
diff changeset
  1195
dc92e3aebc71 Improved handling of defines imported in duplicate.
ballarin
parents: 19932
diff changeset
  1196
fun defs_ord (defs1, defs2) =
dc92e3aebc71 Improved handling of defines imported in duplicate.
ballarin
parents: 19932
diff changeset
  1197
    list_ord (fn ((_, (d1, _)), (_, (d2, _))) =>
dc92e3aebc71 Improved handling of defines imported in duplicate.
ballarin
parents: 19932
diff changeset
  1198
      Term.fast_term_ord (d1, d2)) (defs1, defs2);
dc92e3aebc71 Improved handling of defines imported in duplicate.
ballarin
parents: 19932
diff changeset
  1199
structure Defstab =
dc92e3aebc71 Improved handling of defines imported in duplicate.
ballarin
parents: 19932
diff changeset
  1200
    TableFun(type key = ((string * Attrib.src list) * (term * term list)) list
dc92e3aebc71 Improved handling of defines imported in duplicate.
ballarin
parents: 19932
diff changeset
  1201
        val ord = defs_ord);
dc92e3aebc71 Improved handling of defines imported in duplicate.
ballarin
parents: 19932
diff changeset
  1202
dc92e3aebc71 Improved handling of defines imported in duplicate.
ballarin
parents: 19932
diff changeset
  1203
fun rem_dup_defs es ds =
dc92e3aebc71 Improved handling of defines imported in duplicate.
ballarin
parents: 19932
diff changeset
  1204
    fold_map (fn e as (Defines defs) => (fn ds =>
dc92e3aebc71 Improved handling of defines imported in duplicate.
ballarin
parents: 19932
diff changeset
  1205
                 if Defstab.defined ds defs
dc92e3aebc71 Improved handling of defines imported in duplicate.
ballarin
parents: 19932
diff changeset
  1206
                 then (Defines [], ds)
dc92e3aebc71 Improved handling of defines imported in duplicate.
ballarin
parents: 19932
diff changeset
  1207
                 else (e, Defstab.update (defs, ()) ds))
dc92e3aebc71 Improved handling of defines imported in duplicate.
ballarin
parents: 19932
diff changeset
  1208
               | e => (fn ds => (e, ds))) es ds;
dc92e3aebc71 Improved handling of defines imported in duplicate.
ballarin
parents: 19932
diff changeset
  1209
fun rem_dup_elemss (Int es) ds = apfst Int (rem_dup_defs es ds)
dc92e3aebc71 Improved handling of defines imported in duplicate.
ballarin
parents: 19932
diff changeset
  1210
  | rem_dup_elemss (Ext e) ds = (Ext e, ds);
dc92e3aebc71 Improved handling of defines imported in duplicate.
ballarin
parents: 19932
diff changeset
  1211
fun rem_dup_defines raw_elemss =
dc92e3aebc71 Improved handling of defines imported in duplicate.
ballarin
parents: 19932
diff changeset
  1212
    fold_map (fn (id as (_, (Assumed _)), es) => (fn ds =>
dc92e3aebc71 Improved handling of defines imported in duplicate.
ballarin
parents: 19932
diff changeset
  1213
                     apfst (pair id) (rem_dup_elemss es ds))
dc92e3aebc71 Improved handling of defines imported in duplicate.
ballarin
parents: 19932
diff changeset
  1214
               | (id as (_, (Derived _)), es) => (fn ds =>
dc92e3aebc71 Improved handling of defines imported in duplicate.
ballarin
parents: 19932
diff changeset
  1215
                     ((id, es), ds))) raw_elemss Defstab.empty |> #1;
dc92e3aebc71 Improved handling of defines imported in duplicate.
ballarin
parents: 19932
diff changeset
  1216
16736
1e792b32abef Preparations for interpretation of locales in locales.
ballarin
parents: 16620
diff changeset
  1217
(* CB: type inference and consistency checks for locales.
1e792b32abef Preparations for interpretation of locales in locales.
ballarin
parents: 16620
diff changeset
  1218
1e792b32abef Preparations for interpretation of locales in locales.
ballarin
parents: 16620
diff changeset
  1219
   Works by building a context (through declare_elemss), extracting the
1e792b32abef Preparations for interpretation of locales in locales.
ballarin
parents: 16620
diff changeset
  1220
   required information and adjusting the context elements (finish_elemss).
1e792b32abef Preparations for interpretation of locales in locales.
ballarin
parents: 16620
diff changeset
  1221
   Can also universally close free vars in assms and defs.  This is only
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
  1222
   needed for Ext elements and controlled by parameter do_close.
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
  1223
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
  1224
   Only elements of assumed identifiers are considered.
16736
1e792b32abef Preparations for interpretation of locales in locales.
ballarin
parents: 16620
diff changeset
  1225
*)
15127
2550a5578d39 Disallowed "includes" in locale declarations.
ballarin
parents: 15104
diff changeset
  1226
18671
621efeed255b uniform handling of fixes;
wenzelm
parents: 18617
diff changeset
  1227
fun prep_elemss prep_vars prepp do_close context fixed_params raw_elemss raw_concl =
12529
d99716a53f59 simultaneous type-inference of complete context/statement specifications;
wenzelm
parents: 12514
diff changeset
  1228
  let
15127
2550a5578d39 Disallowed "includes" in locale declarations.
ballarin
parents: 15104
diff changeset
  1229
    (* CB: contexts computed in the course of this function are discarded.
2550a5578d39 Disallowed "includes" in locale declarations.
ballarin
parents: 15104
diff changeset
  1230
       They are used for type inference and consistency checks only. *)
15206
09d78ec709c7 Modified locales: improved implementation of "includes".
ballarin
parents: 15127
diff changeset
  1231
    (* CB: fixed_params are the parameters (with types) of the target locale,
09d78ec709c7 Modified locales: improved implementation of "includes".
ballarin
parents: 15127
diff changeset
  1232
       empty list if there is no target. *)
14508
859b11514537 Experimental command for instantiation of locales in proof contexts:
ballarin
parents: 14446
diff changeset
  1233
    (* CB: raw_elemss are list of pairs consisting of identifiers and
859b11514537 Experimental command for instantiation of locales in proof contexts:
ballarin
parents: 14446
diff changeset
  1234
       context elements, the latter marked as internal or external. *)
19942
dc92e3aebc71 Improved handling of defines imported in duplicate.
ballarin
parents: 19932
diff changeset
  1235
    val raw_elemss = rem_dup_defines raw_elemss;
18671
621efeed255b uniform handling of fixes;
wenzelm
parents: 18617
diff changeset
  1236
    val (raw_ctxt, raw_proppss) = declare_elemss prep_vars fixed_params raw_elemss context;
14508
859b11514537 Experimental command for instantiation of locales in proof contexts:
ballarin
parents: 14446
diff changeset
  1237
    (* CB: raw_ctxt is context with additional fixed variables derived from
859b11514537 Experimental command for instantiation of locales in proof contexts:
ballarin
parents: 14446
diff changeset
  1238
       the fixes elements in raw_elemss,
859b11514537 Experimental command for instantiation of locales in proof contexts:
ballarin
parents: 14446
diff changeset
  1239
       raw_proppss contains assumptions and definitions from the
15206
09d78ec709c7 Modified locales: improved implementation of "includes".
ballarin
parents: 15127
diff changeset
  1240
       external elements in raw_elemss. *)
18550
59b89f625d68 add_local_context now yields imported and body elements seperatly; additional slight clenup in code
haftmann
parents: 18546
diff changeset
  1241
    fun prep_prop raw_propp (raw_ctxt, raw_concl)  =
18450
e57731ba01dd discontinued unflat in favour of burrow and burrow_split
haftmann
parents: 18421
diff changeset
  1242
      let
e57731ba01dd discontinued unflat in favour of burrow and burrow_split
haftmann
parents: 18421
diff changeset
  1243
        (* CB: add type information from fixed_params to context (declare_term) *)
e57731ba01dd discontinued unflat in favour of burrow and burrow_split
haftmann
parents: 18421
diff changeset
  1244
        (* CB: process patterns (conclusion and external elements only) *)
e57731ba01dd discontinued unflat in favour of burrow and burrow_split
haftmann
parents: 18421
diff changeset
  1245
        val (ctxt, all_propp) =
19900
21a99d88d925 ProofContext: moved variable operations to struct Variable;
wenzelm
parents: 19873
diff changeset
  1246
          prepp (fold Variable.declare_term (map Free fixed_params) raw_ctxt, raw_concl @ raw_propp);
18450
e57731ba01dd discontinued unflat in favour of burrow and burrow_split
haftmann
parents: 18421
diff changeset
  1247
        (* CB: add type information from conclusion and external elements to context *)
19900
21a99d88d925 ProofContext: moved variable operations to struct Variable;
wenzelm
parents: