src/Pure/Isar/expression.ML
author ballarin
Mon, 27 Oct 2008 16:23:54 +0100
changeset 28697 140bfb63f893
child 28701 ca5840b1f7b3
permissions -rw-r--r--
New-style locale expressions with instantiation (new file expression.ML).
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
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
     5
Locale expressions --- experimental.
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
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    10
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    11
type map
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    12
type 'morph expr
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    13
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    14
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
    15
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
    16
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    17
val parse_expr: OuterParse.token list -> expression * OuterParse.token list
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    18
val debug_parameters: expression -> Proof.context -> Proof.context
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    19
val debug_context: expression -> Proof.context -> Proof.context
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    20
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    21
end;
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    22
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    23
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    24
structure Expression: EXPRESSION =
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    25
struct
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    26
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    27
(* Locale expressions *)
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    28
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    29
datatype map =
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    30
  Positional of string option list |
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    31
  Named of (string * string) list;
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
datatype 'morph expr = Expr of (string * 'morph) list;
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    34
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    35
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
    36
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
    37
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    38
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    39
(** Parsing and printing **)
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    40
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    41
local
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    42
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    43
structure P = OuterParse;
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    44
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    45
val loc_keyword = P.$$$ "fixes" || P.$$$ "constrains" || P.$$$ "assumes" ||
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    46
   P.$$$ "defines" || P.$$$ "notes" || P.$$$ "includes";
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    47
fun plus1_unless test scan =
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    48
  scan ::: Scan.repeat (P.$$$ "+" |-- Scan.unless test (P.!!! scan));
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    49
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    50
val prefix = P.name --| P.$$$ ":";
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    51
val named = P.name -- (P.$$$ "=" |-- P.term);
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    52
val position = P.maybe P.term;
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    53
val instance = P.$$$ "where" |-- P.and_list1 named >> Named ||
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    54
  Scan.repeat1 position >> Positional;
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
in
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
val parse_expr =
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    59
  let
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    60
    fun expr2 x = P.xname x;
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    61
    fun expr1 x = (Scan.optional prefix "" -- expr2 --
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    62
      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
    63
    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
    64
  in expr0 -- P.for_fixes end;
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    65
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    66
end;
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    67
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    68
(*
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    69
fun pretty_expr thy (Locale loc) =
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    70
      [Pretty.str "Locale", Pretty.brk 1, Pretty.str (Locale.extern thy loc)]
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    71
  | pretty_expr thy (Instance (expr, (prfx, Positional insts))) =
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    72
      let
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    73
        val insts' = (* chop trailing NONEs *)
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    74
      
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    75
  | pretty_expr thy (Instance (expr, (prfx, Named insts))) =
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    76
*)
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    77
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    78
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    79
(** Processing of locale expression **)
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
fun intern thy (Expr instances) = Expr (map (apfst (Locale.intern thy)) instances);
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    82
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    83
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    84
(* Parameters of expression (not expression_i).
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    85
   Sanity check of instantiations.
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    86
   Positional instantiations are extended to match full length of parameter list. *)
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    87
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    88
fun parameters thy (expr, fixed) =
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    89
  let
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    90
    fun reject_dups message xs =
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    91
      let val dups = duplicates (op =) xs
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    92
      in
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    93
        if null dups then () else error (message ^ commas dups)
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    94
      end;
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    95
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    96
    fun params2 loc =
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    97
          (Locale.parameters_of thy loc |> map (fn ((p, _), mx) => (p, mx)), loc) ;
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    98
    fun params1 (loc, (prfx, Positional insts)) =
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
    99
          let
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   100
            val (ps, loc') = params2 loc;
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   101
	    val d = length ps - length insts;
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   102
	    val insts' =
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   103
	      if d < 0 then error ("More arguments than parameters in instantiation.")
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   104
(* FIXME print expr *)
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   105
	      else insts @ replicate d NONE;
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   106
            val ps' = (ps ~~ insts') |>
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   107
              map_filter (fn (p, NONE) => SOME p | (_, SOME _) => NONE);
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   108
          in
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   109
            (ps', (loc', (prfx, Positional insts')))
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   110
          end
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   111
      | params1 (loc, (prfx, Named insts)) =
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   112
          let
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   113
            val _ = reject_dups "Duplicate instantiation of the following parameter(s): "
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   114
              (map fst insts);
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   115
(* FIXME print expr *)
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   116
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   117
            val (ps, loc') = params2 loc;
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   118
            val ps' = fold (fn (p, _) => fn ps =>
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   119
              if AList.defined (op =) ps p then AList.delete (op =) p ps
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   120
              else error (quote p ^" not a parameter of instantiated expression.")) insts ps;
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   121
(* FIXME print expr *)
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   122
(* FIXME AList lacks a version of delete that signals the absence of the deleted item *)
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   123
          in
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   124
            (ps', (loc', (prfx, Named insts)))
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   125
          end;
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   126
    fun params0 (Expr is) =
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   127
          let
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   128
            val (is', ps') = fold_map (fn i => fn ps =>
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   129
              let
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   130
                val (ps', i') = params1 i;
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   131
                val ps'' = AList.join (op =) (fn p => fn (mx1, mx2) =>
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   132
                  if mx1 = mx2 then mx1
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   133
                  else error ("Conflicting syntax for parameter" ^ quote p ^ " in expression.")) (ps, ps')
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   134
(* FIXME print Expr is *)
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   135
              in (i', ps'') end) is []
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   136
          in
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   137
            (ps', Expr is')
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   138
          end;
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   139
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   140
    val (parms, expr') = params0 expr;
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   141
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   142
    val parms' = map fst parms;
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   143
    val fixed' = map (#1 #> Name.name_of) fixed;
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   144
    val _ = reject_dups "Duplicate fixed parameter(s): " fixed';
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   145
    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
   146
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   147
  in (expr', (parms, fixed)) end;
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   148
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   149
fun debug_parameters raw_expr ctxt =
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   150
  let
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   151
    val thy = ProofContext.theory_of ctxt;
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   152
    val expr = apfst (intern thy) raw_expr;
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   153
    val (expr', (parms, fixed)) = parameters thy expr;
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   154
  in ctxt end;
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   155
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   156
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   157
fun debug_context (raw_expr, fixed) ctxt =
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   158
  let
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   159
    val thy = ProofContext.theory_of ctxt;
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   160
    val expr = intern thy raw_expr;
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   161
    val (expr', (parms, fixed)) = parameters thy (expr, fixed);
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   162
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   163
    fun declare_parameters (parms, fixed) ctxt =
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   164
      let
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   165
      val (parms', ctxt') =
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   166
        ProofContext.add_fixes (map (fn (p, mx) => (Name.binding p, NONE, mx)) parms) ctxt;
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   167
      val (fixed', ctxt'') =
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   168
        ProofContext.add_fixes fixed ctxt';
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   169
      in
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   170
        (parms' @ fixed', ctxt'')
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   171
      end;
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   172
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   173
    fun rough_inst loc prfx insts ctxt =
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   174
      let
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   175
        (* locale data *)
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   176
        val (parm_names, parm_types) = loc |> Locale.parameters_of thy |>
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   177
          map fst |> split_list;
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   178
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   179
        (* type parameters *)
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   180
        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
   181
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   182
        (* parameter instantiations *)
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   183
        val insts' = case insts of
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   184
          Positional insts => (insts ~~ parm_names) |> map (fn
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   185
            (NONE, p) => Syntax.parse_term ctxt p |
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   186
            (SOME t, _) => Syntax.parse_term ctxt t) |
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   187
          Named insts => parm_names |> map (fn
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   188
            p => case AList.lookup (op =) insts p of
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   189
              SOME t => Syntax.parse_term ctxt t |
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   190
              NONE => Syntax.parse_term ctxt p);
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   191
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   192
	(* type inference and contexts *)
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   193
        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
   194
        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
   195
	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
   196
	val res = Syntax.check_terms ctxt arg;
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   197
	val ctxt' = ctxt |> fold Variable.auto_fixes res;
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   198
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   199
	(* instantiation *)
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   200
	val (type_parms'', res') = chop (length type_parms) res;
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   201
        val insts'' = (parm_names ~~ res') |> map_filter
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   202
          (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
   203
            inst => SOME inst);
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   204
	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
   205
	val inst = Symtab.make insts'';
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   206
      in
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   207
        (Element.inst_morphism thy (instT, inst) $>
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   208
          Morphism.name_morphism (Name.qualified prfx), ctxt')
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   209
      end;
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   210
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   211
    fun add_declarations loc morph ctxt =
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   212
      let
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   213
        (* locale data *)
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   214
        val parms = loc |> Locale.parameters_of thy;
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   215
        val (typ_decls, term_decls) = Locale.declarations_of thy loc;
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   216
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   217
        (* declarations from locale *)
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   218
	val ctxt'' = ctxt |>
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   219
	  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
   220
	  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
   221
      in
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   222
        ctxt''
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   223
      end;
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   224
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   225
    val Expr [(loc1, (prfx1, insts1))] = expr';
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   226
    val ctxt0 = ProofContext.init thy;
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   227
    val (parms, ctxt') = declare_parameters (parms, fixed) ctxt0;
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   228
    val (morph1, ctxt'') = rough_inst loc1 prfx1 insts1 ctxt';
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   229
    val ctxt'' = add_declarations loc1 morph1 ctxt';
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   230
  in ctxt'' end;
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   231
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   232
140bfb63f893 New-style locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff changeset
   233
end;