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