src/Pure/Isar/expression.ML
author ballarin
Fri, 14 Nov 2008 16:49:52 +0100
changeset 28795 6891e273c33b
parent 28701 ca5840b1f7b3
child 28832 cf7237498e7a
permissions -rw-r--r--
Initial part of locale reimplementation.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
28697
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
     1
(*  Title:      Pure/Isar/expression.ML
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
     2
    ID:         $Id$
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
     3
    Author:     Clemens Ballarin, TU Muenchen
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
     4
28795
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
     5
New locale development --- experimental.
28697
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
     6
*)
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
     7
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
     8
signature EXPRESSION =
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
     9
sig
28795
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
    10
  type map
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
    11
  type 'morph expr
28697
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    12
28795
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
    13
  val empty_expr: 'morph expr
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
    14
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
    15
  type expression = (string * map) expr * (Name.binding * string option * mixfix) list
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
    16
  type expression_i = Morphism.morphism expr * (Name.binding * typ option * mixfix) list
28697
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    17
28795
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
    18
  (* Declaring locales *)
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
    19
  val add_locale: string -> bstring -> expression -> Element.context list -> theory ->
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
    20
    string * Proof.context
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
    21
(*
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
    22
  val add_locale_i: string -> bstring -> expression_i -> Element.context_i list -> theory ->
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
    23
    string * Proof.context
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
    24
*)
28697
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    25
28795
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
    26
  (* Debugging and development *)
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
    27
  val parse_expression: OuterParse.token list -> expression * OuterParse.token list
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
    28
  val debug_parameters: expression -> Proof.context -> Proof.context
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
    29
  val debug_context: expression -> Proof.context -> Proof.context
28697
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    30
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    31
end;
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    32
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    33
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    34
structure Expression: EXPRESSION =
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    35
struct
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    36
28795
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
    37
datatype ctxt = datatype Element.ctxt;
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
    38
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
    39
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
    40
(*** Expressions ***)
28697
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    41
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    42
datatype map =
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    43
  Positional of string option list |
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    44
  Named of (string * string) list;
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    45
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    46
datatype 'morph expr = Expr of (string * 'morph) list;
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    47
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    48
type expression = (string * map) expr * (Name.binding * string option * mixfix) list;
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    49
type expression_i = Morphism.morphism expr * (Name.binding * typ option * mixfix) list;
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    50
28795
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
    51
val empty_expr = Expr [];
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
    52
28697
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    53
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    54
(** Parsing and printing **)
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    55
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    56
local
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    57
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    58
structure P = OuterParse;
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    59
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    60
val loc_keyword = P.$$$ "fixes" || P.$$$ "constrains" || P.$$$ "assumes" ||
28795
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
    61
   P.$$$ "defines" || P.$$$ "notes";
28697
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    62
fun plus1_unless test scan =
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    63
  scan ::: Scan.repeat (P.$$$ "+" |-- Scan.unless test (P.!!! scan));
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    64
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    65
val prefix = P.name --| P.$$$ ":";
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    66
val named = P.name -- (P.$$$ "=" |-- P.term);
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    67
val position = P.maybe P.term;
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    68
val instance = P.$$$ "where" |-- P.and_list1 named >> Named ||
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    69
  Scan.repeat1 position >> Positional;
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    70
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    71
in
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    72
28795
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
    73
val parse_expression =
28697
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    74
  let
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    75
    fun expr2 x = P.xname x;
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    76
    fun expr1 x = (Scan.optional prefix "" -- expr2 --
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    77
      Scan.optional instance (Named []) >> (fn ((p, l), i) => (l, (p, i)))) x;
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    78
    fun expr0 x = (plus1_unless loc_keyword expr1 >> Expr) x;
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    79
  in expr0 -- P.for_fixes end;
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    80
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    81
end;
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    82
28795
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
    83
fun pretty_expr thy (Expr expr) =
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
    84
  let
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
    85
    fun pretty_pos NONE = Pretty.str "_"
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
    86
      | pretty_pos (SOME x) = Pretty.str x;
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
    87
    fun pretty_named (x, y) = [Pretty.str x, Pretty.brk 1, Pretty.str "=",
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
    88
          Pretty.brk 1, Pretty.str y] |> Pretty.block;
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
    89
    fun pretty_ren (Positional ps) = take_suffix is_none ps |> snd |>
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
    90
          map pretty_pos |> Pretty.breaks
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
    91
      | pretty_ren (Named []) = []
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
    92
      | pretty_ren (Named ps) = Pretty.str "where" :: Pretty.brk 1 ::
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
    93
          (ps |> map pretty_named |> Pretty.separate "and");
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
    94
    fun pretty_rename (loc, ("", ren)) =
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
    95
          Pretty.block (Pretty.str (NewLocale.extern thy loc) :: Pretty.brk 1 :: pretty_ren ren) 
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
    96
      | pretty_rename (loc, (prfx, ren)) =
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
    97
          Pretty.block (Pretty.str prfx :: Pretty.brk 1 :: Pretty.str (NewLocale.extern thy loc) ::
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
    98
            Pretty.brk 1 :: pretty_ren ren);
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
    99
  in Pretty.separate "+" (map pretty_rename expr) |> Pretty.block end;
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   100
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   101
fun err_in_expr thy msg (Expr expr) =
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   102
  let
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   103
    val err_msg =
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   104
      if null expr then msg
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   105
      else msg ^ "\n" ^ Pretty.string_of (Pretty.block
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   106
        [Pretty.str "The above error(s) occurred in expression:", Pretty.brk 1,
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   107
          pretty_expr thy (Expr expr)])
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   108
  in error err_msg end;
28697
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   109
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   110
28795
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   111
(** Internalise locale names **)
28697
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   112
28795
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   113
fun intern_expr thy (Expr instances) = Expr (map (apfst (NewLocale.intern thy)) instances);
28697
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   114
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   115
28795
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   116
(** Parameters of expression (not expression_i).
28697
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   117
   Sanity check of instantiations.
28795
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   118
   Positional instantiations are extended to match full length of parameter list. **)
28697
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   119
28701
ca5840b1f7b3 making SMLNJ happy
haftmann
parents: 28697
diff changeset
   120
fun parameters thy (expr, fixed : (Name.binding * string option * mixfix) list) =
28697
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   121
  let
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   122
    fun reject_dups message xs =
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   123
      let val dups = duplicates (op =) xs
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   124
      in
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   125
        if null dups then () else error (message ^ commas dups)
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   126
      end;
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   127
28795
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   128
    fun match_bind (n, b) = (n = Name.name_of b);
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   129
    fun bind_eq (b1, b2) = (Name.name_of b1 = Name.name_of b2);
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   130
      (* FIXME: cannot compare bindings for equality. *)
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   131
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   132
    fun params_loc loc =
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   133
          (NewLocale.params_of thy loc |> map (fn (p, _, mx) => (p, mx)), loc)
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   134
            handle ERROR msg => err_in_expr thy msg (Expr [(loc, ("", Named []))]);
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   135
    fun params_inst (expr as (loc, (prfx, Positional insts))) =
28697
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   136
          let
28795
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   137
            val (ps, loc') = params_loc loc;
28697
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   138
	    val d = length ps - length insts;
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   139
	    val insts' =
28795
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   140
	      if d < 0 then err_in_expr thy "More arguments than parameters in instantiation."
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   141
                (Expr [expr])
28697
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   142
	      else insts @ replicate d NONE;
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   143
            val ps' = (ps ~~ insts') |>
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   144
              map_filter (fn (p, NONE) => SOME p | (_, SOME _) => NONE);
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   145
          in
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   146
            (ps', (loc', (prfx, Positional insts')))
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   147
          end
28795
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   148
      | params_inst (expr as (loc, (prfx, Named insts))) =
28697
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   149
          let
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   150
            val _ = reject_dups "Duplicate instantiation of the following parameter(s): "
28795
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   151
              (map fst insts)
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   152
              handle ERROR msg => err_in_expr thy msg (Expr [expr]);
28697
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   153
28795
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   154
            val (ps, loc') = params_loc loc;
28697
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   155
            val ps' = fold (fn (p, _) => fn ps =>
28795
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   156
              if AList.defined match_bind ps p then AList.delete match_bind p ps
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   157
              else err_in_expr thy (quote p ^" not a parameter of instantiated expression.")
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   158
                (Expr [expr])) insts ps;
28697
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   159
          in
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   160
            (ps', (loc', (prfx, Named insts)))
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   161
          end;
28795
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   162
    fun params_expr (Expr is) =
28697
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   163
          let
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   164
            val (is', ps') = fold_map (fn i => fn ps =>
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   165
              let
28795
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   166
                val (ps', i') = params_inst i;
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   167
                val ps'' = AList.join bind_eq (fn p => fn (mx1, mx2) =>
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   168
                  (* FIXME: should check for bindings being the same.
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   169
                     Instead we check for equal name and syntax. *)
28697
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   170
                  if mx1 = mx2 then mx1
28795
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   171
                  else err_in_expr thy ("Conflicting syntax for parameter" ^ quote (Name.name_of p) ^ " in expression.")
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   172
                    (Expr is)) (ps, ps')
28697
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   173
              in (i', ps'') end) is []
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   174
          in
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   175
            (ps', Expr is')
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   176
          end;
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   177
28795
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   178
    val (parms, expr') = params_expr expr;
28697
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   179
28795
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   180
    val parms' = map (fst #> Name.name_of) parms;
28697
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   181
    val fixed' = map (#1 #> Name.name_of) fixed;
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   182
    val _ = reject_dups "Duplicate fixed parameter(s): " fixed';
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   183
    val _ = reject_dups "Parameter(s) declared simultaneously in expression and for clause: " (parms' @ fixed');
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   184
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   185
  in (expr', (parms, fixed)) end;
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   186
28795
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   187
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   188
(** Read instantiation **)
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   189
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   190
fun read_inst parse_term parms (prfx, insts) ctxt =
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   191
  let
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   192
    (* parameters *)
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   193
    val (parm_names, parm_types) = split_list parms;
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   194
    val type_parm_names = fold Term.add_tfreesT parm_types [] |> map fst;
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   195
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   196
    (* parameter instantiations *)
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   197
    val insts' = case insts of
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   198
      Positional insts => (insts ~~ parm_names) |> map (fn
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   199
        (NONE, p) => parse_term ctxt p |
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   200
        (SOME t, _) => parse_term ctxt t) |
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   201
      Named insts => parm_names |> map (fn
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   202
        p => case AList.lookup (op =) insts p of
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   203
          SOME t => parse_term ctxt t |
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   204
          NONE => parse_term ctxt p);
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   205
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   206
    (* type inference and contexts *)
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   207
    val parm_types' = map (TypeInfer.paramify_vars o Logic.varifyT) parm_types;
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   208
    val type_parms = fold Term.add_tvarsT parm_types' [] |> map (Logic.mk_type o TVar);
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   209
    val arg = type_parms @ map2 TypeInfer.constrain parm_types' insts';
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   210
    val res = Syntax.check_terms ctxt arg;
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   211
    val ctxt' = ctxt |> fold Variable.auto_fixes res;
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   212
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   213
    (* instantiation *)
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   214
    val (type_parms'', res') = chop (length type_parms) res;
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   215
    val insts'' = (parm_names ~~ res') |> map_filter
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   216
      (fn (inst as (x, Free (y, _))) => if x = y then NONE else SOME inst |
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   217
        inst => SOME inst);
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   218
    val instT = Symtab.make (type_parm_names ~~ map Logic.dest_type type_parms'');
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   219
    val inst = Symtab.make insts'';
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   220
  in
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   221
    (Element.inst_morphism (ProofContext.theory_of ctxt) (instT, inst) $>
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   222
      Morphism.name_morphism (Name.qualified prfx), ctxt')
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   223
  end;
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   224
        
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   225
        
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   226
(** Debugging **)
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   227
  
28697
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   228
fun debug_parameters raw_expr ctxt =
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   229
  let
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   230
    val thy = ProofContext.theory_of ctxt;
28795
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   231
    val expr = apfst (intern_expr thy) raw_expr;
28697
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   232
    val (expr', (parms, fixed)) = parameters thy expr;
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   233
  in ctxt end;
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   234
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   235
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   236
fun debug_context (raw_expr, fixed) ctxt =
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   237
  let
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   238
    val thy = ProofContext.theory_of ctxt;
28795
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   239
    val expr = intern_expr thy raw_expr;
28697
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   240
    val (expr', (parms, fixed)) = parameters thy (expr, fixed);
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   241
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   242
    fun declare_parameters (parms, fixed) ctxt =
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   243
      let
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   244
      val (parms', ctxt') =
28795
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   245
        ProofContext.add_fixes (map (fn (p, mx) => (p, NONE, mx)) parms) ctxt;
28697
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   246
      val (fixed', ctxt'') =
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   247
        ProofContext.add_fixes fixed ctxt';
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   248
      in
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   249
        (parms' @ fixed', ctxt'')
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   250
      end;
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   251
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   252
    fun rough_inst loc prfx insts ctxt =
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   253
      let
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   254
        (* locale data *)
28795
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   255
        val (parm_names, parm_types) = loc |> NewLocale.params_of thy |>
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   256
          map (fn (b, SOME T, _) => (Name.name_of b, T)) |> split_list;
28697
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   257
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   258
        (* type parameters *)
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   259
        val type_parm_names = fold Term.add_tfreesT parm_types [] |> map fst;
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   260
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   261
        (* parameter instantiations *)
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   262
        val insts' = case insts of
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   263
          Positional insts => (insts ~~ parm_names) |> map (fn
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   264
            (NONE, p) => Syntax.parse_term ctxt p |
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   265
            (SOME t, _) => Syntax.parse_term ctxt t) |
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   266
          Named insts => parm_names |> map (fn
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   267
            p => case AList.lookup (op =) insts p of
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   268
              SOME t => Syntax.parse_term ctxt t |
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   269
              NONE => Syntax.parse_term ctxt p);
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   270
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   271
	(* type inference and contexts *)
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   272
        val parm_types' = map (TypeInfer.paramify_vars o Logic.varifyT) parm_types;
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   273
        val type_parms = fold Term.add_tvarsT parm_types' [] |> map (Logic.mk_type o TVar);
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   274
	val arg = type_parms @ map2 TypeInfer.constrain parm_types' insts';
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   275
	val res = Syntax.check_terms ctxt arg;
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   276
	val ctxt' = ctxt |> fold Variable.auto_fixes res;
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   277
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   278
	(* instantiation *)
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   279
	val (type_parms'', res') = chop (length type_parms) res;
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   280
        val insts'' = (parm_names ~~ res') |> map_filter
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   281
          (fn (inst as (x, Free (y, _))) => if x = y then NONE else SOME inst |
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   282
            inst => SOME inst);
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   283
	val instT = Symtab.make (type_parm_names ~~ map Logic.dest_type type_parms'');
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   284
	val inst = Symtab.make insts'';
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   285
      in
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   286
        (Element.inst_morphism thy (instT, inst) $>
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   287
          Morphism.name_morphism (Name.qualified prfx), ctxt')
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   288
      end;
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   289
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   290
    fun add_declarations loc morph ctxt =
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   291
      let
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   292
        (* locale data *)
28795
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   293
        val parms = loc |> NewLocale.params_of thy |>
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   294
          map (fn (b, SOME T, mx) => ((Name.name_of b, T), mx));
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   295
        val (typ_decls, term_decls) = NewLocale.declarations_of thy loc;
28697
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   296
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   297
        (* declarations from locale *)
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   298
	val ctxt'' = ctxt |>
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   299
	  fold_rev (fn decl => Context.proof_map (decl morph)) typ_decls |>
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   300
	  fold_rev (fn decl => Context.proof_map (decl morph)) term_decls;
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   301
      in
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   302
        ctxt''
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   303
      end;
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   304
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   305
    val Expr [(loc1, (prfx1, insts1))] = expr';
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   306
    val ctxt0 = ProofContext.init thy;
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   307
    val (parms, ctxt') = declare_parameters (parms, fixed) ctxt0;
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   308
    val (morph1, ctxt'') = rough_inst loc1 prfx1 insts1 ctxt';
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   309
    val ctxt'' = add_declarations loc1 morph1 ctxt';
28795
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   310
  in ctxt0 end;
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   311
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   312
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   313
(*** Locale processing ***)
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   314
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   315
(** Prepare locale elements **)
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   316
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   317
local
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   318
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   319
fun declare_elem prep_vars (Fixes fixes) ctxt =
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   320
      let val (vars, _) = prep_vars fixes ctxt
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   321
      in ([], ctxt |> ProofContext.add_fixes_i vars |> snd) end
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   322
  | declare_elem prep_vars (Constrains csts) ctxt =
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   323
      let val (_, ctxt') = prep_vars (map (fn (x, T) => (Name.binding x, SOME T, NoSyn)) csts) ctxt
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   324
      in ([], ctxt') end
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   325
  | declare_elem _ (Assumes asms) ctxt = (map #2 asms, ctxt)
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   326
  | declare_elem _ (Defines defs) ctxt = (map (fn (_, (t, ps)) => [(t, ps)]) defs, ctxt)
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   327
  | declare_elem _ (Notes _) ctxt = ([], ctxt);
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   328
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   329
in
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   330
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   331
fun declare_elems prep_vars raw_elems ctxt =
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   332
  fold_map (declare_elem prep_vars) raw_elems ctxt;
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   333
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   334
end;
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   335
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   336
local
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   337
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   338
val norm_term = Envir.beta_norm oo Term.subst_atomic;
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   339
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   340
fun abstract_thm thy eq =
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   341
  Thm.assume (Thm.cterm_of thy eq) |> Drule.gen_all |> Drule.abs_def;
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   342
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   343
fun bind_def ctxt eq (xs, env, ths) =
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   344
  let
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   345
    val ((y, T), b) = LocalDefs.abs_def eq;
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   346
    val b' = norm_term env b;
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   347
    val th = abstract_thm (ProofContext.theory_of ctxt) eq;
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   348
    fun err msg = error (msg ^ ": " ^ quote y);
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   349
  in
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   350
    exists (fn (x, _) => x = y) xs andalso
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   351
      err "Attempt to define previously specified variable";
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   352
    exists (fn (Free (y', _), _) => y = y' | _ => false) env andalso
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   353
      err "Attempt to redefine variable";
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   354
    (Term.add_frees b' xs, (Free (y, T), b') :: env, th :: ths)
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   355
  end;
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   356
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   357
fun eval_text _ (Fixes _) text = text
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   358
  | eval_text _ (Constrains _) text = text
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   359
  | eval_text _ (Assumes asms)
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   360
        (((exts, exts'), (ints, ints')), (xs, env, defs)) =
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   361
      let
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   362
        val ts = maps (map #1 o #2) asms;
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   363
        val ts' = map (norm_term env) ts;
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   364
        val spec' = ((exts @ ts, exts' @ ts'), (ints, ints'));
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   365
      in (spec', (fold Term.add_frees ts' xs, env, defs)) end
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   366
  | eval_text ctxt (Defines defs) (spec, binds) =
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   367
      (spec, fold (bind_def ctxt o #1 o #2) defs binds)
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   368
  | eval_text _ (Notes _) text = text;
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   369
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   370
fun closeup _ false elem = elem
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   371
  | closeup ctxt true elem =
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   372
      let
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   373
        fun close_frees t =
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   374
          let
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   375
            val rev_frees =
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   376
              Term.fold_aterms (fn Free (x, T) =>
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   377
                if Variable.is_fixed ctxt x then I else insert (op =) (x, T) | _ => I) t [];
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   378
          in Term.list_all_free (rev rev_frees, t) end;
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   379
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   380
        fun no_binds [] = []
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   381
          | no_binds _ = error "Illegal term bindings in locale element";
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   382
      in
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   383
        (case elem of
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   384
          Assumes asms => Assumes (asms |> map (fn (a, propps) =>
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   385
            (a, map (fn (t, ps) => (close_frees t, no_binds ps)) propps)))
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   386
        | Defines defs => Defines (defs |> map (fn (a, (t, ps)) =>
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   387
            (a, (close_frees (#2 (LocalDefs.cert_def ctxt t)), no_binds ps))))
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   388
        | e => e)
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   389
      end;
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   390
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   391
fun finish_ext_elem parms _ (Fixes fixes, _) = Fixes (map (fn (binding, _, mx) =>
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   392
      let val x = Name.name_of binding
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   393
      in (binding, AList.lookup (op =) parms x, mx) end) fixes)
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   394
  | finish_ext_elem _ _ (Constrains _, _) = Constrains []
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   395
  | finish_ext_elem _ close (Assumes asms, propp) =
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   396
      close (Assumes (map #1 asms ~~ propp))
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   397
  | finish_ext_elem _ close (Defines defs, propp) =
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   398
      close (Defines (map #1 defs ~~ map (fn [(t, ps)] => (t, ps)) propp))
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   399
  | finish_ext_elem _ _ (Notes facts, _) = Notes facts;
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   400
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   401
fun finish_elem ctxt parms do_close (elem, propp) text =
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   402
  let
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   403
    val elem' = finish_ext_elem parms (closeup ctxt do_close) (elem, propp);
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   404
    val text' = eval_text ctxt elem' text;
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   405
  in (elem', text') end
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   406
  
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   407
in
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   408
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   409
fun finish_elems ctxt parms do_close elems text =
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   410
  fold_map (finish_elem ctxt parms do_close) elems text;
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   411
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   412
end;
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   413
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   414
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   415
local
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   416
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   417
fun param_types ps = map_filter (fn (_, NONE) => NONE | (x, SOME T) => SOME (x, T)) ps;
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   418
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   419
fun frozen_tvars ctxt Ts =
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   420
  #1 (Variable.importT_inst (map Logic.mk_type Ts) ctxt)
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   421
  |> map (fn ((xi, S), T) => (xi, (S, T)));
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   422
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   423
fun unify_frozen ctxt maxidx Ts Us =
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   424
  let
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   425
    fun paramify NONE i = (NONE, i)
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   426
      | paramify (SOME T) i = apfst SOME (TypeInfer.paramify_dummies T i);
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   427
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   428
    val (Ts', maxidx') = fold_map paramify Ts maxidx;
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   429
    val (Us', maxidx'') = fold_map paramify Us maxidx';
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   430
    val thy = ProofContext.theory_of ctxt;
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   431
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   432
    fun unify (SOME T, SOME U) env = (Sign.typ_unify thy (U, T) env
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   433
          handle Type.TUNIFY => raise TYPE ("unify_frozen: failed to unify types", [U, T], []))
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   434
      | unify _ env = env;
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   435
    val (unifier, _) = fold unify (Ts' ~~ Us') (Vartab.empty, maxidx'');
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   436
    val Vs = map (Option.map (Envir.norm_type unifier)) Us';
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   437
    val unifier' = Vartab.extend (unifier, frozen_tvars ctxt (map_filter I Vs));
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   438
  in map (Option.map (Envir.norm_type unifier')) Vs end;
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   439
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   440
fun prep_elems prep_vars prepp do_close context raw_elems raw_concl =
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   441
  let
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   442
    val (raw_propps, raw_ctxt) = declare_elems prep_vars raw_elems context;
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   443
      (* raw_ctxt is context enriched by syntax from raw_elems *)
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   444
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   445
    fun prep_prop raw_propp (raw_ctxt, raw_concl) =
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   446
      let
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   447
        (* process patterns (conclusion and external elements) *)
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   448
        val (ctxt, all_propp) = prepp (raw_ctxt, raw_concl @ raw_propp);
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   449
        (* add type information from conclusion and external elements to context *)
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   450
        val ctxt = fold Variable.declare_term (maps (map fst) all_propp) ctxt;
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   451
        (* resolve schematic variables (patterns) in conclusion and external elements. *)
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   452
        val all_propp' = map2 (curry (op ~~))
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   453
          (#1 (#2 (ProofContext.bind_propp_schematic_i (ctxt, all_propp)))) (map (map snd) all_propp);
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   454
        val (concl, propp) = chop (length raw_concl) all_propp';
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   455
      in (propp, (ctxt, concl)) end
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   456
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   457
    val (propps, (ctxt, concl)) = fold_burrow prep_prop raw_propps (raw_ctxt, raw_concl);
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   458
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   459
    (* Infer parameter types *) 
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   460
    val xs = fold (fn Fixes fixes => (fn ps => ps @ map (Name.name_of o #1) fixes) |
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   461
      _ => fn ps => ps) raw_elems [];
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   462
    val typing = unify_frozen ctxt 0
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   463
      (map (Variable.default_type raw_ctxt) xs)
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   464
      (map (Variable.default_type ctxt) xs);
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   465
    val parms = param_types (xs ~~ typing);
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   466
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   467
    (* CB: extract information from assumes and defines elements
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   468
       (fixes, constrains and notes in raw_elemss don't have an effect on
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   469
       text and elemss), compute final form of context elements. *)
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   470
   val (elems, text) = finish_elems ctxt parms do_close
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   471
      (raw_elems ~~ propps) ((([], []), ([], [])), ([], [], []));
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   472
    (* CB: text has the following structure:
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   473
           (((exts, exts'), (ints, ints')), (xs, env, defs))
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   474
       where
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   475
         exts: external assumptions (terms in external assumes elements)
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   476
         exts': dito, normalised wrt. env
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   477
         ints: internal assumptions (terms in internal assumes elements)
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   478
         ints': dito, normalised wrt. env
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   479
         xs: the free variables in exts' and ints' and rhss of definitions,
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   480
           this includes parameters except defined parameters
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   481
         env: list of term pairs encoding substitutions, where the first term
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   482
           is a free variable; substitutions represent defines elements and
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   483
           the rhs is normalised wrt. the previous env
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   484
         defs: theorems representing the substitutions from defines elements
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   485
           (thms are normalised wrt. env).
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   486
       elems is an updated version of raw_elems:
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   487
         - type info added to Fixes and modified in Constrains
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   488
         - axiom and definition statement replaced by corresponding one
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   489
           from proppss in Assumes and Defines
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   490
         - Facts unchanged
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   491
       *)
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   492
   in ((parms, elems, concl), text) end
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   493
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   494
in
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   495
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   496
fun read_elems x = prep_elems ProofContext.read_vars ProofContext.read_propp_schematic x;
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   497
fun cert_elems x = prep_elems ProofContext.cert_vars ProofContext.cert_propp_schematic x;
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   498
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   499
end;
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   500
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   501
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   502
(* facts and attributes *)
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   503
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   504
local
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   505
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   506
fun check_name name =
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   507
  if NameSpace.is_qualified name then error ("Illegal qualified name: " ^ quote name)
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   508
  else name;
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   509
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   510
fun prep_facts prep_name get intern ctxt elem = elem |> Element.map_ctxt
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   511
     {var = I, typ = I, term = I,
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   512
      name = Name.map_name prep_name,
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   513
      fact = get ctxt,
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   514
      attrib = Args.assignable o intern (ProofContext.theory_of ctxt)};
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   515
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   516
in
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   517
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   518
fun read_facts x = prep_facts check_name ProofContext.get_fact Attrib.intern_src x;
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   519
fun cert_facts x = prep_facts I (K I) (K I) x;
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   520
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   521
end;
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   522
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   523
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   524
(* activate elements in context, return elements and facts *)
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   525
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   526
local
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   527
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   528
fun axioms_export axs _ As =
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   529
  (Element.satisfy_thm axs #> Drule.implies_intr_list (Library.drop (length axs, As)), fn t => t);
28697
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   530
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   531
28795
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   532
(* NB: derived ids contain only facts at this stage *)
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   533
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   534
fun activate_elem (Fixes fixes) ctxt =
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   535
      ([], ctxt |> ProofContext.add_fixes_i fixes |> snd)
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   536
  | activate_elem (Constrains _) ctxt =
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   537
      ([], ctxt)
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   538
  | activate_elem (Assumes asms) ctxt =
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   539
      let
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   540
        val asms' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) asms;
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   541
        val ts = maps (map #1 o #2) asms';
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   542
        val (_, ctxt') =
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   543
          ctxt |> fold Variable.auto_fixes ts
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   544
          |> ProofContext.add_assms_i (axioms_export []) asms';
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   545
      in ([], ctxt') end
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   546
  | activate_elem (Defines defs) ctxt =
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   547
      let
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   548
        val defs' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) defs;
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   549
        val asms = defs' |> map (fn ((name, atts), (t, ps)) =>
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   550
            let val ((c, _), t') = LocalDefs.cert_def ctxt t
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   551
            in (t', ((Name.map_name (Thm.def_name_optional c) name, atts), [(t', ps)])) end);
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   552
        val (_, ctxt') =
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   553
          ctxt |> fold (Variable.auto_fixes o #1) asms
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   554
          |> ProofContext.add_assms_i LocalDefs.def_export (map #2 asms);
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   555
      in ([], ctxt') end
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   556
  | activate_elem (Notes (kind, facts)) ctxt =
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   557
      let
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   558
        val facts' = Attrib.map_facts (Attrib.attribute_i (ProofContext.theory_of ctxt)) facts;
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   559
        val (res, ctxt') = ctxt |> ProofContext.note_thmss_i kind facts';
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   560
      in ((map (#1 o #1) facts' ~~ map #2 res), ctxt') end;
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   561
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   562
in
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   563
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   564
fun activate_elems prep_facts raw_elems ctxt =
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   565
  let
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   566
    val elems = map (prep_facts ctxt) raw_elems;
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   567
    val (res, ctxt') = fold_map activate_elem elems (ProofContext.qualified_names ctxt);
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   568
    val elems' = elems |> map (Element.map_ctxt_attrib Args.closure);
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   569
  in ((elems', flat res), ProofContext.restore_naming ctxt ctxt') end;
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   570
28697
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   571
end;
28795
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   572
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   573
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   574
(* full context statements: import + elements + conclusion *)
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   575
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   576
local
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   577
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   578
fun prep_context_statement prep_expr prep_elems prep_facts
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   579
    do_close imprt elements raw_concl context =
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   580
  let
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   581
    val thy = ProofContext.theory_of context;
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   582
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   583
    val (expr, (params, fors)) = parameters thy (apfst (prep_expr thy) imprt);
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   584
    val ctxt = context |>
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   585
      ProofContext.add_fixes (map (fn (b, mx) => (b, NONE, mx)) params) |> snd |>
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   586
      ProofContext.add_fixes fors |> snd;
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   587
  in
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   588
    case expr of
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   589
        Expr [] => let
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   590
          val ((parms, elems, concl), (spec, (_, _, defs))) = prep_elems do_close
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   591
            context elements raw_concl;
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   592
          val ((elems', _), ctxt') =
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   593
            activate_elems prep_facts elems (ProofContext.set_stmt true ctxt);
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   594
        in
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   595
          (((ctxt', elems'), (parms, spec, defs)), concl)
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   596
        end
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   597
(*
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   598
        | Expr [(name, insts)] => let
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   599
          val parms = parameters_of thy name |> map (fn (b, SOME T, _) => (Name.name_of b, T));
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   600
          val (morph, ctxt') = read_inst parms insts context;
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   601
        in
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   602
          
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   603
        end
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   604
*)
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   605
end
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   606
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   607
in
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   608
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   609
fun read_context imprt body ctxt =
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   610
  #1 (prep_context_statement intern_expr read_elems read_facts true imprt body [] ctxt);
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   611
(*
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   612
fun cert_context imprt body ctxt =
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   613
  #1 (prep_context_statement (K I) cert_elems cert_facts true imprt body [] ctxt);
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   614
*)
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   615
end;
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   616
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   617
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   618
(** Dependencies **)
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   619
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   620
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   621
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   622
(*** Locale declarations ***)
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   623
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   624
local
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   625
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   626
(* introN: name of theorems for introduction rules of locale and
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   627
     delta predicates;
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   628
   axiomsN: name of theorem set with destruct rules for locale predicates,
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   629
     also name suffix of delta predicates. *)
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   630
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   631
val introN = "intro";
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   632
val axiomsN = "axioms";
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   633
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   634
fun atomize_spec thy ts =
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   635
  let
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   636
    val t = Logic.mk_conjunction_balanced ts;
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   637
    val body = ObjectLogic.atomize_term thy t;
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   638
    val bodyT = Term.fastype_of body;
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   639
  in
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   640
    if bodyT = propT then (t, propT, Thm.reflexive (Thm.cterm_of thy t))
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   641
    else (body, bodyT, ObjectLogic.atomize (Thm.cterm_of thy t))
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   642
  end;
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   643
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   644
(* achieve plain syntax for locale predicates (without "PROP") *)
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   645
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   646
fun aprop_tr' n c = (Syntax.constN ^ c, fn ctxt => fn args =>
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   647
  if length args = n then
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   648
    Syntax.const "_aprop" $
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   649
      Term.list_comb (Syntax.free (Consts.extern (ProofContext.consts_of ctxt) c), args)
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   650
  else raise Match);
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   651
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   652
(* CB: define one predicate including its intro rule and axioms
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   653
   - bname: predicate name
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   654
   - parms: locale parameters
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   655
   - defs: thms representing substitutions from defines elements
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   656
   - ts: terms representing locale assumptions (not normalised wrt. defs)
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   657
   - norm_ts: terms representing locale assumptions (normalised wrt. defs)
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   658
   - thy: the theory
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   659
*)
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   660
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   661
fun def_pred bname parms defs ts norm_ts thy =
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   662
  let
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   663
    val name = Sign.full_name thy bname;
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   664
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   665
    val (body, bodyT, body_eq) = atomize_spec thy norm_ts;
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   666
    val env = Term.add_term_free_names (body, []);
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   667
    val xs = filter (member (op =) env o #1) parms;
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   668
    val Ts = map #2 xs;
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   669
    val extraTs = (Term.term_tfrees body \\ fold Term.add_tfreesT Ts [])
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   670
      |> Library.sort_wrt #1 |> map TFree;
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   671
    val predT = map Term.itselfT extraTs ---> Ts ---> bodyT;
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   672
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   673
    val args = map Logic.mk_type extraTs @ map Free xs;
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   674
    val head = Term.list_comb (Const (name, predT), args);
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   675
    val statement = ObjectLogic.ensure_propT thy head;
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   676
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   677
    val ([pred_def], defs_thy) =
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   678
      thy
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   679
      |> bodyT = propT ? Sign.add_advanced_trfuns ([], [], [aprop_tr' (length args) name], [])
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   680
      |> Sign.declare_const [] ((Name.binding bname, predT), NoSyn) |> snd
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   681
      |> PureThy.add_defs false
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   682
        [((Thm.def_name bname, Logic.mk_equals (head, body)), [Thm.kind_internal])];
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   683
    val defs_ctxt = ProofContext.init defs_thy |> Variable.declare_term head;
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   684
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   685
    val cert = Thm.cterm_of defs_thy;
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   686
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   687
    val intro = Goal.prove_global defs_thy [] norm_ts statement (fn _ =>
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   688
      MetaSimplifier.rewrite_goals_tac [pred_def] THEN
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   689
      Tactic.compose_tac (false, body_eq RS Drule.equal_elim_rule1, 1) 1 THEN
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   690
      Tactic.compose_tac (false,
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   691
        Conjunction.intr_balanced (map (Thm.assume o cert) norm_ts), 0) 1);
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   692
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   693
    val conjuncts =
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   694
      (Drule.equal_elim_rule2 OF [body_eq,
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   695
        MetaSimplifier.rewrite_rule [pred_def] (Thm.assume (cert statement))])
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   696
      |> Conjunction.elim_balanced (length ts);
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   697
    val axioms = ts ~~ conjuncts |> map (fn (t, ax) =>
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   698
      Element.prove_witness defs_ctxt t
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   699
       (MetaSimplifier.rewrite_goals_tac defs THEN
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   700
        Tactic.compose_tac (false, ax, 0) 1));
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   701
  in ((statement, intro, axioms), defs_thy) end;
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   702
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   703
in
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   704
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   705
(* CB: main predicate definition function *)
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   706
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   707
fun define_preds pname (parms, ((exts, exts'), (ints, ints')), defs) thy =
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   708
  let
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   709
    val (a_pred, a_intro, a_axioms, thy'') =
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   710
      if null exts then (NONE, NONE, [], thy)
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   711
      else
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   712
        let
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   713
          val aname = if null ints then pname else pname ^ "_" ^ axiomsN;
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   714
          val ((statement, intro, axioms), thy') =
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   715
            thy
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   716
            |> def_pred aname parms defs exts exts';
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   717
          val (_, thy'') =
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   718
            thy'
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   719
            |> Sign.add_path aname
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   720
            |> Sign.no_base_names
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   721
            |> PureThy.note_thmss Thm.internalK [((Name.binding introN, []), [([intro], [])])]
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   722
            ||> Sign.restore_naming thy';
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   723
          in (SOME statement, SOME intro, axioms, thy'') end;
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   724
    val (b_pred, b_intro, b_axioms, thy'''') =
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   725
      if null ints then (NONE, NONE, [], thy'')
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   726
      else
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   727
        let
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   728
          val ((statement, intro, axioms), thy''') =
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   729
            thy''
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   730
            |> def_pred pname parms defs (ints @ the_list a_pred) (ints' @ the_list a_pred);
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   731
          val (_, thy'''') =
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   732
            thy'''
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   733
            |> Sign.add_path pname
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   734
            |> Sign.no_base_names
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   735
            |> PureThy.note_thmss Thm.internalK
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   736
                 [((Name.binding introN, []), [([intro], [])]),
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   737
                  ((Name.binding axiomsN, []),
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   738
                    [(map (Drule.standard o Element.conclude_witness) axioms, [])])]
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   739
            ||> Sign.restore_naming thy''';
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   740
        in (SOME statement, SOME intro, axioms, thy'''') end;
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   741
  in ((a_pred, a_intro, a_axioms), (b_pred, b_intro, b_axioms), thy'''') end;
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   742
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   743
end;
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   744
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   745
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   746
local
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   747
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   748
fun assumes_to_notes (Assumes asms) axms =
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   749
      fold_map (fn (a, spec) => fn axs =>
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   750
          let val (ps, qs) = chop (length spec) axs
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   751
          in ((a, [(ps, [])]), qs) end) asms axms
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   752
      |> apfst (curry Notes Thm.assumptionK)
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   753
  | assumes_to_notes e axms = (e, axms);
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   754
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   755
fun defines_to_notes thy (Defines defs) defns =
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   756
    let
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   757
      val defs' = map (fn (_, (def, _)) => def) defs
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   758
      val notes = map (fn (a, (def, _)) =>
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   759
        (a, [([assume (cterm_of thy def)], [])])) defs
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   760
    in
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   761
      (Notes (Thm.definitionK, notes), defns @ defs')
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   762
    end
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   763
  | defines_to_notes _ e defns = (e, defns);
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   764
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   765
fun gen_add_locale prep_ctxt
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   766
    bname predicate_name raw_imprt raw_body thy =
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   767
  let
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   768
    val thy_ctxt = ProofContext.init thy;
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   769
    val name = Sign.full_name thy bname;
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   770
    val _ = NewLocale.test_locale thy name andalso
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   771
      error ("Duplicate definition of locale " ^ quote name);
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   772
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   773
    val ((body_ctxt, body_elems), text as (parms, ((_, exts'), _), defs)) =
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   774
      prep_ctxt raw_imprt raw_body thy_ctxt;
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   775
    val ((statement, intro, axioms), _, thy') =
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   776
      define_preds predicate_name text thy;
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   777
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   778
    val extraTs = fold Term.add_tfrees exts' [] \\ fold Term.add_tfreesT (map snd parms) [];
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   779
    val _ = if null extraTs then ()
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   780
      else warning ("Additional type variable(s) in locale specification " ^ quote bname);
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   781
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   782
    val params = body_elems |>
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   783
      map_filter (fn Fixes fixes => SOME fixes | _ => NONE) |> flat;
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   784
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   785
    val (body_elems', defns) = fold_map (defines_to_notes thy) body_elems [];
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   786
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   787
    val notes = body_elems' |>
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   788
      (fn elems => fold_map assumes_to_notes elems (map Element.conclude_witness axioms)) |>
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   789
      fst |>
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   790
      map_filter (fn Notes notes => SOME notes | _ => NONE);
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   791
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   792
    val loc_ctxt = thy' |>
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   793
      NewLocale.register_locale name (extraTs, params) (statement, defns) ([], [])
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   794
        (map (fn n => (n, stamp ())) notes |> rev) [] |>
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   795
      NewLocale.init name
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   796
  in (name, loc_ctxt) end;
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   797
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   798
in
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   799
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   800
val add_locale = gen_add_locale read_context;
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   801
(* val add_locale_i = gen_add_locale cert_context; *)
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   802
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   803
end;
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   804
6891e273c33b Initial part of locale reimplementation.
ballarin
parents: 28701
diff changeset
   805
end;