src/Pure/Syntax/syn_ext.ML
author wenzelm
Mon, 09 Nov 1998 15:42:08 +0100
changeset 5840 e2d2b896c717
parent 5690 4b056ee5435c
child 5870 5d4fc952be47
permissions -rw-r--r--
Object logic specific operations.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
240
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/Syntax/syn_ext.ML
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
911
55754d6d399c new in mixfix annotations: "' " (quote space) separates delimiters without
wenzelm
parents: 865
diff changeset
     3
    Author:     Markus Wenzel and Carsten Clasohm, TU Muenchen
240
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
     4
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
     5
Syntax extension (internal interface).
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
     6
*)
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
     7
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
     8
signature SYN_EXT0 =
4050
543df9687d7b added mixfix_args;
wenzelm
parents: 2913
diff changeset
     9
sig
240
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
    10
  val typeT: typ
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
    11
  val constrainC: string
5690
4b056ee5435c no open;
wenzelm
parents: 4938
diff changeset
    12
  val max_pri: int
4050
543df9687d7b added mixfix_args;
wenzelm
parents: 2913
diff changeset
    13
end;
240
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
    14
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
    15
signature SYN_EXT =
4050
543df9687d7b added mixfix_args;
wenzelm
parents: 2913
diff changeset
    16
sig
240
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
    17
  include SYN_EXT0
1510
4588ba1b1438 Elimination of fully-functorial style.
paulson
parents: 1178
diff changeset
    18
  val logic: string
4588ba1b1438 Elimination of fully-functorial style.
paulson
parents: 1178
diff changeset
    19
  val args: string
4588ba1b1438 Elimination of fully-functorial style.
paulson
parents: 1178
diff changeset
    20
  val cargs: string
4588ba1b1438 Elimination of fully-functorial style.
paulson
parents: 1178
diff changeset
    21
  val any: string
4588ba1b1438 Elimination of fully-functorial style.
paulson
parents: 1178
diff changeset
    22
  val sprop: string
4588ba1b1438 Elimination of fully-functorial style.
paulson
parents: 1178
diff changeset
    23
  val typ_to_nonterm: typ -> string
4588ba1b1438 Elimination of fully-functorial style.
paulson
parents: 1178
diff changeset
    24
  datatype xsymb =
4588ba1b1438 Elimination of fully-functorial style.
paulson
parents: 1178
diff changeset
    25
    Delim of string |
4588ba1b1438 Elimination of fully-functorial style.
paulson
parents: 1178
diff changeset
    26
    Argument of string * int |
4588ba1b1438 Elimination of fully-functorial style.
paulson
parents: 1178
diff changeset
    27
    Space of string |
4588ba1b1438 Elimination of fully-functorial style.
paulson
parents: 1178
diff changeset
    28
    Bg of int | Brk of int | En
4588ba1b1438 Elimination of fully-functorial style.
paulson
parents: 1178
diff changeset
    29
  datatype xprod = XProd of string * xsymb list * string * int
4588ba1b1438 Elimination of fully-functorial style.
paulson
parents: 1178
diff changeset
    30
  val chain_pri: int
4701
be8a8d60d962 adapted to new scanner and abroque chars;
wenzelm
parents: 4146
diff changeset
    31
  val delims_of: xprod list -> string list list
1510
4588ba1b1438 Elimination of fully-functorial style.
paulson
parents: 1178
diff changeset
    32
  datatype mfix = Mfix of string * typ * string * int list * int
4588ba1b1438 Elimination of fully-functorial style.
paulson
parents: 1178
diff changeset
    33
  datatype syn_ext =
4588ba1b1438 Elimination of fully-functorial style.
paulson
parents: 1178
diff changeset
    34
    SynExt of {
4588ba1b1438 Elimination of fully-functorial style.
paulson
parents: 1178
diff changeset
    35
      logtypes: string list,
4588ba1b1438 Elimination of fully-functorial style.
paulson
parents: 1178
diff changeset
    36
      xprods: xprod list,
4588ba1b1438 Elimination of fully-functorial style.
paulson
parents: 1178
diff changeset
    37
      consts: string list,
2913
ce271fa4d8e2 fixed diagnostic output of print modes;
wenzelm
parents: 2694
diff changeset
    38
      prmodes: string list,
1510
4588ba1b1438 Elimination of fully-functorial style.
paulson
parents: 1178
diff changeset
    39
      parse_ast_translation: (string * (Ast.ast list -> Ast.ast)) list,
4588ba1b1438 Elimination of fully-functorial style.
paulson
parents: 1178
diff changeset
    40
      parse_rules: (Ast.ast * Ast.ast) list,
4588ba1b1438 Elimination of fully-functorial style.
paulson
parents: 1178
diff changeset
    41
      parse_translation: (string * (term list -> term)) list,
4146
00136226f74b adapted syn_ext_trfunsT;
wenzelm
parents: 4054
diff changeset
    42
      print_translation: (string * (bool -> typ -> term list -> term)) list,
1510
4588ba1b1438 Elimination of fully-functorial style.
paulson
parents: 1178
diff changeset
    43
      print_rules: (Ast.ast * Ast.ast) list,
2694
b98365c6e869 added token_translation interface;
wenzelm
parents: 2382
diff changeset
    44
      print_ast_translation: (string * (Ast.ast list -> Ast.ast)) list,
b98365c6e869 added token_translation interface;
wenzelm
parents: 2382
diff changeset
    45
      token_translation: (string * string * (string -> string * int)) list}
4054
wenzelm
parents: 4050
diff changeset
    46
  val mfix_args: string -> int
1510
4588ba1b1438 Elimination of fully-functorial style.
paulson
parents: 1178
diff changeset
    47
  val mk_syn_ext: bool -> string list -> mfix list ->
4588ba1b1438 Elimination of fully-functorial style.
paulson
parents: 1178
diff changeset
    48
    string list -> (string * (Ast.ast list -> Ast.ast)) list *
4588ba1b1438 Elimination of fully-functorial style.
paulson
parents: 1178
diff changeset
    49
    (string * (term list -> term)) list *
4146
00136226f74b adapted syn_ext_trfunsT;
wenzelm
parents: 4054
diff changeset
    50
    (string * (bool -> typ -> term list -> term)) list * (string * (Ast.ast list -> Ast.ast)) list
2694
b98365c6e869 added token_translation interface;
wenzelm
parents: 2382
diff changeset
    51
    -> (string * string * (string -> string * int)) list
1510
4588ba1b1438 Elimination of fully-functorial style.
paulson
parents: 1178
diff changeset
    52
    -> (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext
4588ba1b1438 Elimination of fully-functorial style.
paulson
parents: 1178
diff changeset
    53
  val syn_ext: string list -> mfix list -> string list ->
4588ba1b1438 Elimination of fully-functorial style.
paulson
parents: 1178
diff changeset
    54
    (string * (Ast.ast list -> Ast.ast)) list * (string * (term list -> term)) list *
4146
00136226f74b adapted syn_ext_trfunsT;
wenzelm
parents: 4054
diff changeset
    55
    (string * (bool -> typ -> term list -> term)) list * (string * (Ast.ast list -> Ast.ast)) list
2694
b98365c6e869 added token_translation interface;
wenzelm
parents: 2382
diff changeset
    56
    -> (string * string * (string -> string * int)) list
1510
4588ba1b1438 Elimination of fully-functorial style.
paulson
parents: 1178
diff changeset
    57
    -> (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext
4588ba1b1438 Elimination of fully-functorial style.
paulson
parents: 1178
diff changeset
    58
  val syn_ext_logtypes: string list -> syn_ext
4588ba1b1438 Elimination of fully-functorial style.
paulson
parents: 1178
diff changeset
    59
  val syn_ext_const_names: string list -> string list -> syn_ext
4588ba1b1438 Elimination of fully-functorial style.
paulson
parents: 1178
diff changeset
    60
  val syn_ext_rules: string list -> (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext
4146
00136226f74b adapted syn_ext_trfunsT;
wenzelm
parents: 4054
diff changeset
    61
  val fix_tr': (term list -> term) -> bool -> typ -> term list -> term
1510
4588ba1b1438 Elimination of fully-functorial style.
paulson
parents: 1178
diff changeset
    62
  val syn_ext_trfuns: string list ->
4588ba1b1438 Elimination of fully-functorial style.
paulson
parents: 1178
diff changeset
    63
    (string * (Ast.ast list -> Ast.ast)) list * (string * (term list -> term)) list *
4588ba1b1438 Elimination of fully-functorial style.
paulson
parents: 1178
diff changeset
    64
    (string * (term list -> term)) list * (string * (Ast.ast list -> Ast.ast)) list
4588ba1b1438 Elimination of fully-functorial style.
paulson
parents: 1178
diff changeset
    65
    -> syn_ext
4146
00136226f74b adapted syn_ext_trfunsT;
wenzelm
parents: 4054
diff changeset
    66
  val syn_ext_trfunsT: string list ->
00136226f74b adapted syn_ext_trfunsT;
wenzelm
parents: 4054
diff changeset
    67
    (string * (bool -> typ -> term list -> term)) list -> syn_ext
2694
b98365c6e869 added token_translation interface;
wenzelm
parents: 2382
diff changeset
    68
  val syn_ext_tokentrfuns: string list
b98365c6e869 added token_translation interface;
wenzelm
parents: 2382
diff changeset
    69
    -> (string * string * (string -> string * int)) list -> syn_ext
1510
4588ba1b1438 Elimination of fully-functorial style.
paulson
parents: 1178
diff changeset
    70
  val pure_ext: syn_ext
4050
543df9687d7b added mixfix_args;
wenzelm
parents: 2913
diff changeset
    71
end;
240
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
    72
1510
4588ba1b1438 Elimination of fully-functorial style.
paulson
parents: 1178
diff changeset
    73
structure SynExt : SYN_EXT =
240
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
    74
struct
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
    75
2694
b98365c6e869 added token_translation interface;
wenzelm
parents: 2382
diff changeset
    76
240
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
    77
(** misc definitions **)
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
    78
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
    79
(* syntactic categories *)
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
    80
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
    81
val logic = "logic";
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
    82
val logicT = Type (logic, []);
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
    83
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
    84
val args = "args";
1178
b28c6ecc3e6d added cargs for curried function application
clasohm
parents: 1145
diff changeset
    85
val cargs = "cargs";
240
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
    86
330
2fda15dd1e0f changed the way a grammar is generated to allow the new parser to work;
clasohm
parents: 240
diff changeset
    87
val typeT = Type ("type", []);
240
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
    88
764
b60e77395d1a changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents: 624
diff changeset
    89
val sprop = "#prop";
b60e77395d1a changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents: 624
diff changeset
    90
val spropT = Type (sprop, []);
240
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
    91
764
b60e77395d1a changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents: 624
diff changeset
    92
val any = "any";
624
33b9b5da3e6f made major changes to grammar;
clasohm
parents: 555
diff changeset
    93
val anyT = Type (any, []);
33b9b5da3e6f made major changes to grammar;
clasohm
parents: 555
diff changeset
    94
780
567f1fe7ea39 removed "logic1";
wenzelm
parents: 764
diff changeset
    95
240
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
    96
(* constants *)
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
    97
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
    98
val constrainC = "_constrain";
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
    99
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   100
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   101
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   102
(** datatype xprod **)
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   103
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   104
(*Delim s: delimiter s
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   105
  Argument (s, p): nonterminal s requiring priority >= p, or valued token
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   106
  Space s: some white space for printing
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   107
  Bg, Brk, En: blocks and breaks for pretty printing*)
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   108
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   109
datatype xsymb =
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   110
  Delim of string |
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   111
  Argument of string * int |
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   112
  Space of string |
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   113
  Bg of int | Brk of int | En;
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   114
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   115
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   116
(*XProd (lhs, syms, c, p):
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   117
    lhs: name of nonterminal on the lhs of the production
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   118
    syms: list of symbols on the rhs of the production
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   119
    c: head of parse tree
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   120
    p: priority of this production*)
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   121
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   122
datatype xprod = XProd of string * xsymb list * string * int;
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   123
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   124
val max_pri = 1000;   (*maximum legal priority*)
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   125
val chain_pri = ~1;   (*dummy for chain productions*)
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   126
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   127
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   128
(* delims_of *)
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   129
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   130
fun delims_of xprods =
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   131
  let
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   132
    fun del_of (Delim s) = Some s
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   133
      | del_of _ = None;
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   134
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   135
    fun dels_of (XProd (_, xsymbs, _, _)) =
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   136
      mapfilter del_of xsymbs;
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   137
  in
4701
be8a8d60d962 adapted to new scanner and abroque chars;
wenzelm
parents: 4146
diff changeset
   138
    map Symbol.explode (distinct (flat (map dels_of xprods)))
240
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   139
  end;
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   140
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   141
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   142
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   143
(** datatype mfix **)
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   144
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   145
(*Mfix (sy, ty, c, ps, p):
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   146
    sy: rhs of production as symbolic string
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   147
    ty: type description of production
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   148
    c: head of parse tree
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   149
    ps: priorities of arguments in sy
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   150
    p: priority of production*)
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   151
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   152
datatype mfix = Mfix of string * typ * string * int list * int;
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   153
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   154
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   155
(* typ_to_nonterm *)
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   156
865
b38c67991122 added optional precedence for body of binder;
clasohm
parents: 780
diff changeset
   157
fun typ_to_nt _ (Type (c, _)) = c
b38c67991122 added optional precedence for body of binder;
clasohm
parents: 780
diff changeset
   158
  | typ_to_nt default _ = default;
b38c67991122 added optional precedence for body of binder;
clasohm
parents: 780
diff changeset
   159
764
b60e77395d1a changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents: 624
diff changeset
   160
(*get nonterminal for rhs*)
865
b38c67991122 added optional precedence for body of binder;
clasohm
parents: 780
diff changeset
   161
val typ_to_nonterm = typ_to_nt any;
240
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   162
764
b60e77395d1a changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents: 624
diff changeset
   163
(*get nonterminal for lhs*)
865
b38c67991122 added optional precedence for body of binder;
clasohm
parents: 780
diff changeset
   164
val typ_to_nonterm1 = typ_to_nt logic;
240
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   165
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   166
4701
be8a8d60d962 adapted to new scanner and abroque chars;
wenzelm
parents: 4146
diff changeset
   167
(* read_mixfix, mfix_args *)
4050
543df9687d7b added mixfix_args;
wenzelm
parents: 2913
diff changeset
   168
543df9687d7b added mixfix_args;
wenzelm
parents: 2913
diff changeset
   169
local
543df9687d7b added mixfix_args;
wenzelm
parents: 2913
diff changeset
   170
  fun is_meta c = c mem ["(", ")", "/", "_"];
543df9687d7b added mixfix_args;
wenzelm
parents: 2913
diff changeset
   171
4701
be8a8d60d962 adapted to new scanner and abroque chars;
wenzelm
parents: 4146
diff changeset
   172
  val scan_delim_char =
be8a8d60d962 adapted to new scanner and abroque chars;
wenzelm
parents: 4146
diff changeset
   173
    $$ "'" |-- Scan.one ((not o Symbol.is_blank) andf Symbol.not_eof) ||
be8a8d60d962 adapted to new scanner and abroque chars;
wenzelm
parents: 4146
diff changeset
   174
    Scan.one ((not o is_meta) andf (not o Symbol.is_blank) andf Symbol.not_eof);
4050
543df9687d7b added mixfix_args;
wenzelm
parents: 2913
diff changeset
   175
543df9687d7b added mixfix_args;
wenzelm
parents: 2913
diff changeset
   176
  val scan_sym =
543df9687d7b added mixfix_args;
wenzelm
parents: 2913
diff changeset
   177
    $$ "_" >> K (Argument ("", 0)) ||
4701
be8a8d60d962 adapted to new scanner and abroque chars;
wenzelm
parents: 4146
diff changeset
   178
    $$ "(" |-- Scan.any Symbol.is_digit >> (Bg o #1 o Term.read_int) ||
4050
543df9687d7b added mixfix_args;
wenzelm
parents: 2913
diff changeset
   179
    $$ ")" >> K En ||
543df9687d7b added mixfix_args;
wenzelm
parents: 2913
diff changeset
   180
    $$ "/" -- $$ "/" >> K (Brk ~1) ||
4701
be8a8d60d962 adapted to new scanner and abroque chars;
wenzelm
parents: 4146
diff changeset
   181
    $$ "/" |-- Scan.any Symbol.is_blank >> (Brk o length) ||
be8a8d60d962 adapted to new scanner and abroque chars;
wenzelm
parents: 4146
diff changeset
   182
    Scan.any1 Symbol.is_blank >> (Space o implode) ||
be8a8d60d962 adapted to new scanner and abroque chars;
wenzelm
parents: 4146
diff changeset
   183
    Scan.repeat1 scan_delim_char >> (Delim o implode);
4050
543df9687d7b added mixfix_args;
wenzelm
parents: 2913
diff changeset
   184
543df9687d7b added mixfix_args;
wenzelm
parents: 2913
diff changeset
   185
  val scan_symb =
543df9687d7b added mixfix_args;
wenzelm
parents: 2913
diff changeset
   186
    scan_sym >> Some ||
4701
be8a8d60d962 adapted to new scanner and abroque chars;
wenzelm
parents: 4146
diff changeset
   187
    $$ "'" -- Scan.one Symbol.is_blank >> K None;
4050
543df9687d7b added mixfix_args;
wenzelm
parents: 2913
diff changeset
   188
4701
be8a8d60d962 adapted to new scanner and abroque chars;
wenzelm
parents: 4146
diff changeset
   189
  val scan_symbs = Scan.repeat scan_symb --| Scan.ahead (Scan.one (not_equal "'"));
4938
c8bbbf3c59fa Symbol.stopper;
wenzelm
parents: 4701
diff changeset
   190
  val read_symbs = mapfilter I o #1 o Scan.error (Scan.finite Symbol.stopper scan_symbs);
4050
543df9687d7b added mixfix_args;
wenzelm
parents: 2913
diff changeset
   191
in
4701
be8a8d60d962 adapted to new scanner and abroque chars;
wenzelm
parents: 4146
diff changeset
   192
  val read_mixfix = read_symbs o Symbol.explode;
4050
543df9687d7b added mixfix_args;
wenzelm
parents: 2913
diff changeset
   193
end;
543df9687d7b added mixfix_args;
wenzelm
parents: 2913
diff changeset
   194
4054
wenzelm
parents: 4050
diff changeset
   195
fun mfix_args sy =
4701
be8a8d60d962 adapted to new scanner and abroque chars;
wenzelm
parents: 4146
diff changeset
   196
  foldl (fn (i, Argument _) => i + 1 | (i, _) => i) (0, read_mixfix sy);
4050
543df9687d7b added mixfix_args;
wenzelm
parents: 2913
diff changeset
   197
543df9687d7b added mixfix_args;
wenzelm
parents: 2913
diff changeset
   198
240
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   199
(* mfix_to_xprod *)
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   200
764
b60e77395d1a changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents: 624
diff changeset
   201
fun mfix_to_xprod convert logtypes (Mfix (sy, typ, const, pris, pri)) =
240
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   202
  let
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   203
    fun err msg =
4050
543df9687d7b added mixfix_args;
wenzelm
parents: 2913
diff changeset
   204
      (if msg = "" then () else error_msg msg;
543df9687d7b added mixfix_args;
wenzelm
parents: 2913
diff changeset
   205
        error ("in mixfix annotation " ^ quote sy ^ " for " ^ quote const));
240
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   206
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   207
    fun check_pri p =
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   208
      if p >= 0 andalso p <= max_pri then ()
4050
543df9687d7b added mixfix_args;
wenzelm
parents: 2913
diff changeset
   209
      else err ("Precedence out of range: " ^ string_of_int p);
240
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   210
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   211
    fun blocks_ok [] 0 = true
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   212
      | blocks_ok [] _ = false
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   213
      | blocks_ok (Bg _ :: syms) n = blocks_ok syms (n + 1)
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   214
      | blocks_ok (En :: _) 0 = false
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   215
      | blocks_ok (En :: syms) n = blocks_ok syms (n - 1)
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   216
      | blocks_ok (_ :: syms) n = blocks_ok syms n;
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   217
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   218
    fun check_blocks syms =
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   219
      if blocks_ok syms 0 then ()
4050
543df9687d7b added mixfix_args;
wenzelm
parents: 2913
diff changeset
   220
      else err "Unbalanced block parentheses";
240
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   221
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   222
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   223
    val cons_fst = apfst o cons;
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   224
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   225
    fun add_args [] ty [] = ([], typ_to_nonterm1 ty)
4050
543df9687d7b added mixfix_args;
wenzelm
parents: 2913
diff changeset
   226
      | add_args [] _ _ = err "Too many precedences"
240
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   227
      | add_args (Argument _ :: syms) (Type ("fun", [ty, tys])) [] =
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   228
          cons_fst (Argument (typ_to_nonterm ty, 0)) (add_args syms tys [])
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   229
      | add_args (Argument _ :: syms) (Type ("fun", [ty, tys])) (p :: ps) =
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   230
          cons_fst (Argument (typ_to_nonterm ty, p)) (add_args syms tys ps)
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   231
      | add_args (Argument _ :: _) _ _ =
4050
543df9687d7b added mixfix_args;
wenzelm
parents: 2913
diff changeset
   232
          err "More arguments than in corresponding type"
240
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   233
      | add_args (sym :: syms) ty ps = cons_fst sym (add_args syms ty ps);
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   234
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   235
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   236
    fun is_arg (Argument _) = true
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   237
      | is_arg _ = false;
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   238
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   239
    fun is_term (Delim _) = true
5690
4b056ee5435c no open;
wenzelm
parents: 4938
diff changeset
   240
      | is_term (Argument (s, _)) = Lexicon.is_terminal s
240
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   241
      | is_term _ = false;
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   242
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   243
    fun rem_pri (Argument (s, _)) = Argument (s, chain_pri)
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   244
      | rem_pri sym = sym;
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   245
764
b60e77395d1a changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents: 624
diff changeset
   246
    fun is_delim (Delim _) = true
b60e77395d1a changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents: 624
diff changeset
   247
      | is_delim _ = false;
b60e77395d1a changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents: 624
diff changeset
   248
4054
wenzelm
parents: 4050
diff changeset
   249
    fun logify_types copy_prod (a as (Argument (s, p))) =
wenzelm
parents: 4050
diff changeset
   250
          if s mem logtypes then Argument (logic, p) else a
wenzelm
parents: 4050
diff changeset
   251
      | logify_types _ a = a;
240
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   252
2364
821f44a0abba mfix_to_xprod: now uses read_charnames;
wenzelm
parents: 2254
diff changeset
   253
4701
be8a8d60d962 adapted to new scanner and abroque chars;
wenzelm
parents: 4146
diff changeset
   254
    val raw_symbs = read_mixfix sy handle ERROR => err "";
240
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   255
    val (symbs, lhs) = add_args raw_symbs typ pris;
2364
821f44a0abba mfix_to_xprod: now uses read_charnames;
wenzelm
parents: 2254
diff changeset
   256
    val copy_prod =
821f44a0abba mfix_to_xprod: now uses read_charnames;
wenzelm
parents: 2254
diff changeset
   257
      lhs mem ["prop", "logic"]
821f44a0abba mfix_to_xprod: now uses read_charnames;
wenzelm
parents: 2254
diff changeset
   258
        andalso const <> ""
821f44a0abba mfix_to_xprod: now uses read_charnames;
wenzelm
parents: 2254
diff changeset
   259
        andalso not (null symbs)
821f44a0abba mfix_to_xprod: now uses read_charnames;
wenzelm
parents: 2254
diff changeset
   260
        andalso not (exists is_delim symbs);
821f44a0abba mfix_to_xprod: now uses read_charnames;
wenzelm
parents: 2254
diff changeset
   261
    val lhs' =
821f44a0abba mfix_to_xprod: now uses read_charnames;
wenzelm
parents: 2254
diff changeset
   262
      if convert andalso not copy_prod then
821f44a0abba mfix_to_xprod: now uses read_charnames;
wenzelm
parents: 2254
diff changeset
   263
       (if lhs mem logtypes then logic
821f44a0abba mfix_to_xprod: now uses read_charnames;
wenzelm
parents: 2254
diff changeset
   264
        else if lhs = "prop" then sprop else lhs)
821f44a0abba mfix_to_xprod: now uses read_charnames;
wenzelm
parents: 2254
diff changeset
   265
      else lhs;
4054
wenzelm
parents: 4050
diff changeset
   266
    val symbs' = map (logify_types copy_prod) symbs;
764
b60e77395d1a changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents: 624
diff changeset
   267
    val xprod = XProd (lhs', symbs', const, pri);
240
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   268
  in
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   269
    seq check_pri pris;
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   270
    check_pri pri;
764
b60e77395d1a changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents: 624
diff changeset
   271
    check_blocks symbs';
240
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   272
5690
4b056ee5435c no open;
wenzelm
parents: 4938
diff changeset
   273
    if Lexicon.is_terminal lhs' then err ("Illegal lhs: " ^ lhs')
240
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   274
    else if const <> "" then xprod
764
b60e77395d1a changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents: 624
diff changeset
   275
    else if length (filter is_arg symbs') <> 1 then
4050
543df9687d7b added mixfix_args;
wenzelm
parents: 2913
diff changeset
   276
      err "Copy production must have exactly one argument"
764
b60e77395d1a changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents: 624
diff changeset
   277
    else if exists is_term symbs' then xprod
b60e77395d1a changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents: 624
diff changeset
   278
    else XProd (lhs', map rem_pri symbs', "", chain_pri)
240
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   279
  end;
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   280
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   281
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   282
(** datatype syn_ext **)
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   283
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   284
datatype syn_ext =
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   285
  SynExt of {
764
b60e77395d1a changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents: 624
diff changeset
   286
    logtypes: string list,
240
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   287
    xprods: xprod list,
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   288
    consts: string list,
2913
ce271fa4d8e2 fixed diagnostic output of print modes;
wenzelm
parents: 2694
diff changeset
   289
    prmodes: string list,
1510
4588ba1b1438 Elimination of fully-functorial style.
paulson
parents: 1178
diff changeset
   290
    parse_ast_translation: (string * (Ast.ast list -> Ast.ast)) list,
4588ba1b1438 Elimination of fully-functorial style.
paulson
parents: 1178
diff changeset
   291
    parse_rules: (Ast.ast * Ast.ast) list,
240
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   292
    parse_translation: (string * (term list -> term)) list,
4146
00136226f74b adapted syn_ext_trfunsT;
wenzelm
parents: 4054
diff changeset
   293
    print_translation: (string * (bool -> typ -> term list -> term)) list,
1510
4588ba1b1438 Elimination of fully-functorial style.
paulson
parents: 1178
diff changeset
   294
    print_rules: (Ast.ast * Ast.ast) list,
2694
b98365c6e869 added token_translation interface;
wenzelm
parents: 2382
diff changeset
   295
    print_ast_translation: (string * (Ast.ast list -> Ast.ast)) list,
2913
ce271fa4d8e2 fixed diagnostic output of print modes;
wenzelm
parents: 2694
diff changeset
   296
    token_translation: (string * string * (string -> string * int)) list}
240
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   297
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   298
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   299
(* syn_ext *)
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   300
2694
b98365c6e869 added token_translation interface;
wenzelm
parents: 2382
diff changeset
   301
fun mk_syn_ext convert logtypes mfixes consts trfuns tokentrfuns rules =
240
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   302
  let
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   303
    val (parse_ast_translation, parse_translation, print_translation,
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   304
      print_ast_translation) = trfuns;
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   305
    val (parse_rules, print_rules) = rules;
764
b60e77395d1a changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents: 624
diff changeset
   306
    val logtypes' = logtypes \ "prop";
240
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   307
624
33b9b5da3e6f made major changes to grammar;
clasohm
parents: 555
diff changeset
   308
    val mfix_consts = distinct (map (fn (Mfix (_, _, c, _, _)) => c) mfixes);
764
b60e77395d1a changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents: 624
diff changeset
   309
    val xprods = map (mfix_to_xprod convert logtypes') mfixes;
240
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   310
  in
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   311
    SynExt {
764
b60e77395d1a changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents: 624
diff changeset
   312
      logtypes = logtypes',
624
33b9b5da3e6f made major changes to grammar;
clasohm
parents: 555
diff changeset
   313
      xprods = xprods,
5690
4b056ee5435c no open;
wenzelm
parents: 4938
diff changeset
   314
      consts = filter Lexicon.is_xid (consts union mfix_consts),
2913
ce271fa4d8e2 fixed diagnostic output of print modes;
wenzelm
parents: 2694
diff changeset
   315
      prmodes = distinct (map (fn (m, _, _) => m) tokentrfuns),
240
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   316
      parse_ast_translation = parse_ast_translation,
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   317
      parse_rules = parse_rules,
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   318
      parse_translation = parse_translation,
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   319
      print_translation = print_translation,
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   320
      print_rules = print_rules,
2694
b98365c6e869 added token_translation interface;
wenzelm
parents: 2382
diff changeset
   321
      print_ast_translation = print_ast_translation,
b98365c6e869 added token_translation interface;
wenzelm
parents: 2382
diff changeset
   322
      token_translation = tokentrfuns}
240
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   323
  end;
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   324
2382
e7c2bce815ba added fix_tr', syn_ext_trfunsT;
wenzelm
parents: 2364
diff changeset
   325
764
b60e77395d1a changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents: 624
diff changeset
   326
val syn_ext = mk_syn_ext true;
240
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   327
764
b60e77395d1a changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents: 624
diff changeset
   328
fun syn_ext_logtypes logtypes =
2694
b98365c6e869 added token_translation interface;
wenzelm
parents: 2382
diff changeset
   329
  syn_ext logtypes [] [] ([], [], [], []) [] ([], []);
764
b60e77395d1a changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents: 624
diff changeset
   330
b60e77395d1a changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents: 624
diff changeset
   331
fun syn_ext_const_names logtypes cs =
2694
b98365c6e869 added token_translation interface;
wenzelm
parents: 2382
diff changeset
   332
  syn_ext logtypes [] cs ([], [], [], []) [] ([], []);
555
a7f397a14b16 removed idT, varT, tidT, tvarT (now in lexicon.ML);
wenzelm
parents: 441
diff changeset
   333
764
b60e77395d1a changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents: 624
diff changeset
   334
fun syn_ext_rules logtypes rules =
2694
b98365c6e869 added token_translation interface;
wenzelm
parents: 2382
diff changeset
   335
  syn_ext logtypes [] [] ([], [], [], []) [] rules;
764
b60e77395d1a changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents: 624
diff changeset
   336
4146
00136226f74b adapted syn_ext_trfunsT;
wenzelm
parents: 4054
diff changeset
   337
fun fix_tr' f _ _ ts = f ts;
2382
e7c2bce815ba added fix_tr', syn_ext_trfunsT;
wenzelm
parents: 2364
diff changeset
   338
e7c2bce815ba added fix_tr', syn_ext_trfunsT;
wenzelm
parents: 2364
diff changeset
   339
fun syn_ext_trfuns logtypes (atrs, trs, tr's, atr's) =
2694
b98365c6e869 added token_translation interface;
wenzelm
parents: 2382
diff changeset
   340
  syn_ext logtypes [] [] (atrs, trs, map (apsnd fix_tr') tr's, atr's) [] ([], []);
2382
e7c2bce815ba added fix_tr', syn_ext_trfunsT;
wenzelm
parents: 2364
diff changeset
   341
e7c2bce815ba added fix_tr', syn_ext_trfunsT;
wenzelm
parents: 2364
diff changeset
   342
fun syn_ext_trfunsT logtypes tr's =
2694
b98365c6e869 added token_translation interface;
wenzelm
parents: 2382
diff changeset
   343
  syn_ext logtypes [] [] ([], [], tr's, []) [] ([], []);
b98365c6e869 added token_translation interface;
wenzelm
parents: 2382
diff changeset
   344
b98365c6e869 added token_translation interface;
wenzelm
parents: 2382
diff changeset
   345
fun syn_ext_tokentrfuns logtypes tokentrfuns =
b98365c6e869 added token_translation interface;
wenzelm
parents: 2382
diff changeset
   346
  syn_ext logtypes [] [] ([], [], [], []) tokentrfuns ([], []);
2382
e7c2bce815ba added fix_tr', syn_ext_trfunsT;
wenzelm
parents: 2364
diff changeset
   347
240
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   348
764
b60e77395d1a changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents: 624
diff changeset
   349
(* pure_ext *)
240
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   350
764
b60e77395d1a changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents: 624
diff changeset
   351
val pure_ext = mk_syn_ext false []
b60e77395d1a changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents: 624
diff changeset
   352
  [Mfix ("_", spropT --> propT, "", [0], 0),
b60e77395d1a changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents: 624
diff changeset
   353
   Mfix ("_", logicT --> anyT, "", [0], 0),
b60e77395d1a changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents: 624
diff changeset
   354
   Mfix ("_", spropT --> anyT, "", [0], 0),
b60e77395d1a changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents: 624
diff changeset
   355
   Mfix ("'(_')", logicT --> logicT, "", [0], max_pri),
b60e77395d1a changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents: 624
diff changeset
   356
   Mfix ("'(_')", spropT --> spropT, "", [0], max_pri),
b60e77395d1a changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents: 624
diff changeset
   357
   Mfix ("_::_",  [logicT, typeT] ---> logicT, "_constrain", [4, 0], 3),
b60e77395d1a changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents: 624
diff changeset
   358
   Mfix ("_::_",  [spropT, typeT] ---> spropT, "_constrain", [4, 0], 3)]
b60e77395d1a changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents: 624
diff changeset
   359
  []
b60e77395d1a changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents: 624
diff changeset
   360
  ([], [], [], [])
2694
b98365c6e869 added token_translation interface;
wenzelm
parents: 2382
diff changeset
   361
  []
764
b60e77395d1a changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents: 624
diff changeset
   362
  ([], []);
240
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   363
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   364
end;