src/Pure/Syntax/extension.ML
author wenzelm
Wed Oct 31 21:59:07 2001 +0100 (2001-10-31)
changeset 12004 1703de633aaf
parent 171 ab0f93a291b5
permissions -rw-r--r--
IsarThy.theorem_i: no locale;
wenzelm@18
     1
(*  Title:      Pure/Syntax/extension.ML
clasohm@0
     2
    ID:         $Id$
clasohm@0
     3
    Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen
clasohm@0
     4
wenzelm@18
     5
External grammar definition (internal interface).
clasohm@0
     6
*)
clasohm@0
     7
clasohm@0
     8
signature EXTENSION0 =
clasohm@0
     9
sig
clasohm@0
    10
  val typeT: typ
clasohm@0
    11
  val constrainC: string
clasohm@0
    12
end;
clasohm@0
    13
clasohm@0
    14
signature EXTENSION =
clasohm@0
    15
sig
clasohm@0
    16
  include EXTENSION0
clasohm@0
    17
  structure XGram: XGRAM
clasohm@0
    18
  local open XGram XGram.Ast in
clasohm@0
    19
    datatype mfix = Mfix of string * typ * string * int list * int
clasohm@0
    20
    datatype ext =
clasohm@0
    21
      Ext of {
clasohm@0
    22
        roots: string list,
clasohm@0
    23
        mfix: mfix list,
clasohm@0
    24
        extra_consts: string list,
clasohm@0
    25
        parse_ast_translation: (string * (ast list -> ast)) list,
clasohm@0
    26
        parse_translation: (string * (term list -> term)) list,
clasohm@0
    27
        print_translation: (string * (term list -> term)) list,
wenzelm@166
    28
        print_ast_translation: (string * (ast list -> ast)) list} |
wenzelm@166
    29
      ExtRules of {
clasohm@0
    30
        parse_rules: (ast * ast) list,
wenzelm@166
    31
        print_rules: (ast * ast) list} |
wenzelm@166
    32
      ExtRoots of string list
clasohm@0
    33
    val logic: string
wenzelm@18
    34
    val args: string
clasohm@0
    35
    val idT: typ
clasohm@0
    36
    val varT: typ
clasohm@0
    37
    val tfreeT: typ
clasohm@0
    38
    val tvarT: typ
wenzelm@18
    39
    val typ_to_nonterm: typ -> string
clasohm@0
    40
    val applC: string
wenzelm@18
    41
    val empty_xgram: xgram
wenzelm@166
    42
    val extend_xgram: xgram -> ext -> xgram
wenzelm@166
    43
    val mk_xgram: ext -> xgram
clasohm@0
    44
  end
clasohm@0
    45
end;
clasohm@0
    46
wenzelm@18
    47
functor ExtensionFun(structure XGram: XGRAM and Lexicon: LEXICON): EXTENSION =
clasohm@0
    48
struct
clasohm@0
    49
clasohm@0
    50
structure XGram = XGram;
wenzelm@18
    51
open XGram XGram.Ast Lexicon;
clasohm@0
    52
clasohm@0
    53
clasohm@0
    54
(** datatype ext **)
clasohm@0
    55
wenzelm@18
    56
(*Mfix (sy, ty, c, ps, p):
wenzelm@18
    57
    sy: rhs of production as symbolic string
clasohm@0
    58
    ty: type description of production
wenzelm@18
    59
    c: head of parse tree
wenzelm@18
    60
    ps: priorities of arguments in sy
wenzelm@18
    61
    p: priority of production*)
clasohm@0
    62
clasohm@0
    63
datatype mfix = Mfix of string * typ * string * int list * int;
clasohm@0
    64
clasohm@0
    65
datatype ext =
clasohm@0
    66
  Ext of {
clasohm@0
    67
    roots: string list,
clasohm@0
    68
    mfix: mfix list,
clasohm@0
    69
    extra_consts: string list,
clasohm@0
    70
    parse_ast_translation: (string * (ast list -> ast)) list,
clasohm@0
    71
    parse_translation: (string * (term list -> term)) list,
clasohm@0
    72
    print_translation: (string * (term list -> term)) list,
wenzelm@166
    73
    print_ast_translation: (string * (ast list -> ast)) list} |
wenzelm@166
    74
  ExtRules of {
clasohm@0
    75
    parse_rules: (ast * ast) list,
wenzelm@166
    76
    print_rules: (ast * ast) list} |
wenzelm@166
    77
  ExtRoots of string list;
clasohm@0
    78
clasohm@0
    79
wenzelm@166
    80
(* ext_components *)
clasohm@0
    81
wenzelm@171
    82
fun ext_components (Ext ext) = {
wenzelm@171
    83
      roots = #roots ext,
wenzelm@171
    84
      mfix = #mfix ext,
wenzelm@171
    85
      extra_consts = #extra_consts ext,
wenzelm@166
    86
      parse_ast_translation = #parse_ast_translation ext,
wenzelm@171
    87
      parse_rules = [],
wenzelm@166
    88
      parse_translation = #parse_translation ext,
wenzelm@166
    89
      print_translation = #print_translation ext,
wenzelm@171
    90
      print_rules = [],
wenzelm@171
    91
      print_ast_translation = #print_ast_translation ext}
wenzelm@171
    92
  | ext_components (ExtRules {parse_rules, print_rules}) = {
wenzelm@171
    93
      roots = [],
wenzelm@171
    94
      mfix = [],
wenzelm@171
    95
      extra_consts = [],
wenzelm@171
    96
      parse_ast_translation = [],
wenzelm@171
    97
      parse_rules = parse_rules,
wenzelm@171
    98
      parse_translation = [],
wenzelm@171
    99
      print_translation = [],
wenzelm@171
   100
      print_rules = print_rules,
wenzelm@171
   101
      print_ast_translation = []}
wenzelm@171
   102
  | ext_components (ExtRoots roots) = {
wenzelm@171
   103
      roots = roots,
wenzelm@171
   104
      mfix = [],
wenzelm@171
   105
      extra_consts = [],
wenzelm@171
   106
      parse_ast_translation = [],
wenzelm@171
   107
      parse_rules = [],
wenzelm@171
   108
      parse_translation = [],
wenzelm@171
   109
      print_translation = [],
wenzelm@171
   110
      print_rules = [],
wenzelm@171
   111
      print_ast_translation = []};
clasohm@0
   112
clasohm@0
   113
wenzelm@18
   114
(* empty_xgram *)
clasohm@0
   115
wenzelm@18
   116
val empty_xgram =
clasohm@0
   117
  XGram {
clasohm@0
   118
    roots = [], prods = [], consts = [],
clasohm@0
   119
    parse_ast_translation = [],
clasohm@0
   120
    parse_rules = [],
clasohm@0
   121
    parse_translation = [],
clasohm@0
   122
    print_translation = [],
clasohm@0
   123
    print_rules = [],
clasohm@0
   124
    print_ast_translation = []};
clasohm@0
   125
clasohm@0
   126
wenzelm@18
   127
(* syntactic categories *)
clasohm@0
   128
clasohm@0
   129
val logic = "logic";
clasohm@0
   130
val logicT = Type (logic, []);
clasohm@0
   131
clasohm@0
   132
val logic1 = "logic1";
clasohm@0
   133
val logic1T = Type (logic1, []);
clasohm@0
   134
wenzelm@18
   135
val args = "args";
wenzelm@18
   136
val argsT = Type (args, []);
wenzelm@18
   137
clasohm@0
   138
val funT = Type ("fun", []);
clasohm@0
   139
wenzelm@18
   140
val typeT = Type ("type", []);
wenzelm@18
   141
clasohm@0
   142
clasohm@0
   143
(* terminals *)
clasohm@0
   144
clasohm@0
   145
val idT = Type (id, []);
clasohm@0
   146
val varT = Type (var, []);
clasohm@0
   147
val tfreeT = Type (tfree, []);
clasohm@0
   148
val tvarT = Type (tvar, []);
clasohm@0
   149
clasohm@0
   150
wenzelm@18
   151
(* constants *)
clasohm@0
   152
clasohm@0
   153
val applC = "_appl";
clasohm@0
   154
val constrainC = "_constrain";
clasohm@0
   155
clasohm@0
   156
wenzelm@18
   157
(* typ_to_nonterm *)
wenzelm@18
   158
wenzelm@18
   159
fun typ_to_nonterm (Type (c, _)) = c
wenzelm@18
   160
  | typ_to_nonterm _ = logic;
wenzelm@18
   161
wenzelm@18
   162
fun typ_to_nonterm1 (Type (c, _)) = c
wenzelm@18
   163
  | typ_to_nonterm1 _ = logic1;
clasohm@0
   164
clasohm@0
   165
clasohm@0
   166
wenzelm@18
   167
(** mfix_to_prod **)
clasohm@0
   168
wenzelm@18
   169
fun mfix_to_prod (Mfix (sy, typ, const, pris, pri)) =
wenzelm@18
   170
  let
wenzelm@18
   171
    fun err msg =
wenzelm@18
   172
      (writeln ("Error in mixfix annotation " ^ quote sy ^ " for " ^ quote const);
wenzelm@18
   173
        error msg);
clasohm@0
   174
wenzelm@18
   175
    fun check_pri p =
wenzelm@18
   176
      if p >= 0 andalso p <= max_pri then ()
wenzelm@18
   177
      else err ("precedence out of range: " ^ string_of_int p);
clasohm@0
   178
wenzelm@18
   179
    fun blocks_ok [] 0 = true
wenzelm@18
   180
      | blocks_ok [] _ = false
wenzelm@18
   181
      | blocks_ok (Bg _ :: syms) n = blocks_ok syms (n + 1)
wenzelm@18
   182
      | blocks_ok (En :: _) 0 = false
wenzelm@18
   183
      | blocks_ok (En :: syms) n = blocks_ok syms (n - 1)
wenzelm@18
   184
      | blocks_ok (_ :: syms) n = blocks_ok syms n;
clasohm@0
   185
wenzelm@18
   186
    fun check_blocks syms =
wenzelm@18
   187
      if blocks_ok syms 0 then ()
wenzelm@18
   188
      else err "unbalanced block parentheses";
clasohm@0
   189
clasohm@0
   190
wenzelm@18
   191
    fun is_meta c = c mem ["(", ")", "/", "_"];
wenzelm@18
   192
wenzelm@18
   193
    fun scan_delim_char ("'" :: c :: cs) =
wenzelm@18
   194
          if is_blank c then err "illegal spaces in delimiter" else (c, cs)
wenzelm@18
   195
      | scan_delim_char ["'"] = err "trailing escape character"
wenzelm@18
   196
      | scan_delim_char (chs as c :: cs) =
wenzelm@18
   197
          if is_blank c orelse is_meta c then raise LEXICAL_ERROR else (c, cs)
wenzelm@18
   198
      | scan_delim_char [] = raise LEXICAL_ERROR;
wenzelm@18
   199
wenzelm@18
   200
    val scan_symb =
wenzelm@18
   201
      $$ "_" >> K (Nonterminal ("", 0)) ||
wenzelm@18
   202
      $$ "(" -- scan_int >> (Bg o #2) ||
wenzelm@18
   203
      $$ ")" >> K En ||
wenzelm@18
   204
      $$ "/" -- $$ "/" >> K (Brk ~1) ||
wenzelm@18
   205
      $$ "/" -- scan_any is_blank >> (Brk o length o #2) ||
wenzelm@18
   206
      scan_any1 is_blank >> (Space o implode) ||
wenzelm@18
   207
      repeat1 scan_delim_char >> (Terminal o implode);
wenzelm@18
   208
wenzelm@18
   209
wenzelm@18
   210
    val cons_fst = apfst o cons;
clasohm@0
   211
wenzelm@18
   212
    fun add_args [] ty [] = ([], typ_to_nonterm1 ty)
wenzelm@18
   213
      | add_args [] _ _ = err "too many precedences"
wenzelm@18
   214
      | add_args (Nonterminal _ :: syms) (Type ("fun", [ty, tys])) [] =
wenzelm@18
   215
          cons_fst (Nonterminal (typ_to_nonterm ty, 0)) (add_args syms tys [])
wenzelm@18
   216
      | add_args (Nonterminal _ :: syms) (Type ("fun", [ty, tys])) (p :: ps) =
wenzelm@18
   217
          cons_fst (Nonterminal (typ_to_nonterm ty, p)) (add_args syms tys ps)
wenzelm@18
   218
      | add_args (Nonterminal _ :: _) _ _ =
wenzelm@18
   219
          err "more arguments than in corresponding type"
wenzelm@18
   220
      | add_args (sym :: syms) ty ps = cons_fst sym (add_args syms ty ps);
wenzelm@18
   221
wenzelm@18
   222
wenzelm@18
   223
    fun is_arg (Nonterminal _) = true
wenzelm@18
   224
      | is_arg _ = false;
wenzelm@18
   225
wenzelm@18
   226
    fun is_term (Terminal _) = true
wenzelm@18
   227
      | is_term (Nonterminal (s, _)) = is_terminal s
wenzelm@18
   228
      | is_term _ = false;
wenzelm@18
   229
wenzelm@18
   230
    fun rem_pri (Nonterminal (s, _)) = Nonterminal (s, chain_pri)
wenzelm@18
   231
      | rem_pri sym = sym;
wenzelm@18
   232
wenzelm@18
   233
wenzelm@18
   234
    val (raw_symbs, _) = repeat scan_symb (explode sy);
wenzelm@18
   235
    val (symbs, lhs) = add_args raw_symbs typ pris;
wenzelm@18
   236
    val prod = Prod (lhs, symbs, const, pri);
wenzelm@18
   237
  in
wenzelm@18
   238
    seq check_pri pris;
wenzelm@18
   239
    check_pri pri;
wenzelm@18
   240
    check_blocks symbs;
wenzelm@18
   241
wenzelm@166
   242
    if is_terminal lhs then err ("illegal lhs: " ^ lhs)
wenzelm@166
   243
    else if const <> "" then prod
wenzelm@18
   244
    else if length (filter is_arg symbs) <> 1 then
wenzelm@18
   245
      err "copy production must have exactly one argument"
wenzelm@18
   246
    else if exists is_term symbs then prod
wenzelm@18
   247
    else Prod (lhs, map rem_pri symbs, "", chain_pri)
wenzelm@18
   248
  end;
clasohm@0
   249
clasohm@0
   250
clasohm@0
   251
wenzelm@18
   252
(** extend_xgram **)
clasohm@0
   253
wenzelm@166
   254
fun extend_xgram (XGram xgram) ext =
wenzelm@18
   255
  let
clasohm@0
   256
    fun descend (from, to) = Mfix ("_", to --> from, "", [0], 0);
clasohm@0
   257
wenzelm@117
   258
    fun parents T = Mfix ("'(_')", T --> T, "", [0], max_pri);
clasohm@0
   259
clasohm@0
   260
    fun mkappl T =
nipkow@116
   261
      Mfix ("(1_/(1'(_')))", [funT, argsT] ---> T, applC, [max_pri, 0], max_pri);
clasohm@0
   262
clasohm@0
   263
    fun mkid T = Mfix ("_", idT --> T, "", [], max_pri);
clasohm@0
   264
clasohm@0
   265
    fun mkvar T = Mfix ("_", varT --> T, "", [], max_pri);
clasohm@0
   266
clasohm@0
   267
    fun constrain T =
wenzelm@18
   268
      Mfix ("_::_", [T, typeT] ---> T, constrainC, [max_pri, 0], max_pri - 1);
clasohm@0
   269
clasohm@0
   270
clasohm@0
   271
    val {roots = roots1, prods, consts,
clasohm@0
   272
      parse_ast_translation = parse_ast_translation1,
clasohm@0
   273
      parse_rules = parse_rules1,
clasohm@0
   274
      parse_translation = parse_translation1,
clasohm@0
   275
      print_translation = print_translation1,
clasohm@0
   276
      print_rules = print_rules1,
clasohm@0
   277
      print_ast_translation = print_ast_translation1} = xgram;
clasohm@0
   278
clasohm@0
   279
    val {roots = roots2, mfix, extra_consts,
clasohm@0
   280
      parse_ast_translation = parse_ast_translation2,
wenzelm@166
   281
      parse_rules = parse_rules2,
clasohm@0
   282
      parse_translation = parse_translation2,
clasohm@0
   283
      print_translation = print_translation2,
wenzelm@166
   284
      print_rules = print_rules2,
wenzelm@166
   285
      print_ast_translation = print_ast_translation2} = ext_components ext;
clasohm@0
   286
clasohm@0
   287
    val Troots = map (apr (Type, [])) (roots2 \\ roots1);
clasohm@0
   288
    val Troots' = Troots \\ [typeT, propT, logicT];
clasohm@0
   289
    val mfix' = mfix @ map parents (Troots \ logicT) @ map mkappl Troots' @
clasohm@0
   290
      map mkid Troots' @ map mkvar Troots' @ map constrain Troots' @
clasohm@0
   291
      map (apl (logicT, descend)) (Troots \\ [typeT, logicT]) @
clasohm@0
   292
      map (apr (descend, logic1T)) Troots';
wenzelm@18
   293
    val mfix_consts =
wenzelm@18
   294
      distinct (filter is_xid (map (fn (Mfix (_, _, c, _, _)) => c) mfix'));
clasohm@0
   295
  in
clasohm@0
   296
    XGram {
clasohm@0
   297
      roots = distinct (roots1 @ roots2),
wenzelm@18
   298
      prods = prods @ map mfix_to_prod mfix',
wenzelm@18
   299
      consts = extra_consts union (mfix_consts union consts),
clasohm@0
   300
      parse_ast_translation = parse_ast_translation1 @ parse_ast_translation2,
clasohm@0
   301
      parse_rules = parse_rules1 @ parse_rules2,
clasohm@0
   302
      parse_translation = parse_translation1 @ parse_translation2,
clasohm@0
   303
      print_translation = print_translation1 @ print_translation2,
clasohm@0
   304
      print_rules = print_rules1 @ print_rules2,
clasohm@0
   305
      print_ast_translation = print_ast_translation1 @ print_ast_translation2}
clasohm@0
   306
  end;
clasohm@0
   307
clasohm@0
   308
wenzelm@18
   309
(* mk_xgram *)
wenzelm@18
   310
wenzelm@18
   311
val mk_xgram = extend_xgram empty_xgram;
wenzelm@18
   312
wenzelm@18
   313
clasohm@0
   314
end;
clasohm@0
   315