src/Pure/Syntax/syn_ext.ML
author clasohm
Mon, 12 Jun 1995 15:01:03 +0200
changeset 1145 d25b863ab2ac
parent 922 196ca0973a6d
child 1178 b28c6ecc3e6d
permissions -rw-r--r--
fixed bug in mfix_to_xprod: lambda productions' lhs shouldn't be modified
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 =
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
     9
sig
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
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
    12
end;
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
    13
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
    14
signature SYN_EXT =
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
    15
sig
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
    16
  include SYN_EXT0
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
    17
  structure Ast: AST
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
    18
  local open Ast in
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
    19
    val logic: string
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
    20
    val args: string
780
567f1fe7ea39 removed "logic1";
wenzelm
parents: 764
diff changeset
    21
    val any: string
567f1fe7ea39 removed "logic1";
wenzelm
parents: 764
diff changeset
    22
    val sprop: string
240
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
    23
    val typ_to_nonterm: typ -> string
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
    24
    datatype xsymb =
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
    25
      Delim of string |
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
    26
      Argument of string * int |
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
    27
      Space of string |
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
    28
      Bg of int | Brk of int | En
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
    29
    datatype xprod = XProd of string * xsymb list * string * int
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
    30
    val max_pri: int
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
    31
    val chain_pri: int
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
    32
    val delims_of: xprod list -> string list
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
    33
    datatype mfix = Mfix of string * typ * string * int list * int
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
    34
    datatype syn_ext =
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
    35
      SynExt of {
764
b60e77395d1a changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents: 624
diff changeset
    36
        logtypes: string list,
240
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
    37
        xprods: xprod list,
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
    38
        consts: string list,
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
    39
        parse_ast_translation: (string * (ast list -> ast)) list,
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
    40
        parse_rules: (ast * ast) list,
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
    41
        parse_translation: (string * (term list -> term)) list,
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
    42
        print_translation: (string * (term list -> term)) list,
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
    43
        print_rules: (ast * ast) list,
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
    44
        print_ast_translation: (string * (ast list -> ast)) list}
764
b60e77395d1a changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents: 624
diff changeset
    45
    val mk_syn_ext: bool -> string list -> mfix list ->
780
567f1fe7ea39 removed "logic1";
wenzelm
parents: 764
diff changeset
    46
      string list -> (string * (ast list -> ast)) list *
764
b60e77395d1a changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents: 624
diff changeset
    47
      (string * (term list -> term)) list *
b60e77395d1a changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents: 624
diff changeset
    48
      (string * (term list -> term)) list * (string * (ast list -> ast)) list
b60e77395d1a changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents: 624
diff changeset
    49
      -> (ast * ast) list * (ast * ast) list -> syn_ext
b60e77395d1a changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents: 624
diff changeset
    50
    val syn_ext: string list -> mfix list -> string list ->
240
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
    51
      (string * (ast list -> ast)) list * (string * (term list -> term)) list *
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
    52
      (string * (term list -> term)) list * (string * (ast list -> ast)) list
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
    53
      -> (ast * ast) list * (ast * ast) list -> syn_ext
764
b60e77395d1a changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents: 624
diff changeset
    54
    val syn_ext_logtypes: string list -> syn_ext
555
a7f397a14b16 removed idT, varT, tidT, tvarT (now in lexicon.ML);
wenzelm
parents: 441
diff changeset
    55
    val syn_ext_const_names: string list -> string list -> syn_ext
330
2fda15dd1e0f changed the way a grammar is generated to allow the new parser to work;
clasohm
parents: 240
diff changeset
    56
    val syn_ext_rules: string list -> (ast * ast) list * (ast * ast) list -> syn_ext
555
a7f397a14b16 removed idT, varT, tidT, tvarT (now in lexicon.ML);
wenzelm
parents: 441
diff changeset
    57
    val syn_ext_trfuns: string list ->
a7f397a14b16 removed idT, varT, tidT, tvarT (now in lexicon.ML);
wenzelm
parents: 441
diff changeset
    58
      (string * (ast list -> ast)) list * (string * (term list -> term)) list *
a7f397a14b16 removed idT, varT, tidT, tvarT (now in lexicon.ML);
wenzelm
parents: 441
diff changeset
    59
      (string * (term list -> term)) list * (string * (ast list -> ast)) list
a7f397a14b16 removed idT, varT, tidT, tvarT (now in lexicon.ML);
wenzelm
parents: 441
diff changeset
    60
      -> syn_ext
764
b60e77395d1a changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents: 624
diff changeset
    61
    val pure_ext: syn_ext
240
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
    62
  end
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
    63
end;
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
    64
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
    65
functor SynExtFun(structure Lexicon: LEXICON and Ast: AST): SYN_EXT =
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
    66
struct
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
    67
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
    68
structure Ast = Ast;
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
    69
open Lexicon Ast;
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
    70
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
    71
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
    72
(** misc definitions **)
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
    73
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
    74
(* syntactic categories *)
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
    75
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
    76
val logic = "logic";
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
    77
val logicT = Type (logic, []);
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
val args = "args";
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
    80
330
2fda15dd1e0f changed the way a grammar is generated to allow the new parser to work;
clasohm
parents: 240
diff changeset
    81
val typeT = Type ("type", []);
240
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
    82
764
b60e77395d1a changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents: 624
diff changeset
    83
val sprop = "#prop";
b60e77395d1a changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents: 624
diff changeset
    84
val spropT = Type (sprop, []);
240
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
    85
764
b60e77395d1a changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents: 624
diff changeset
    86
val any = "any";
624
33b9b5da3e6f made major changes to grammar;
clasohm
parents: 555
diff changeset
    87
val anyT = Type (any, []);
33b9b5da3e6f made major changes to grammar;
clasohm
parents: 555
diff changeset
    88
780
567f1fe7ea39 removed "logic1";
wenzelm
parents: 764
diff changeset
    89
240
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
    90
(* constants *)
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
    91
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
    92
val constrainC = "_constrain";
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
    93
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
    94
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
    95
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
    96
(** datatype xprod **)
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
(*Delim s: delimiter s
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
    99
  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
   100
  Space s: some white space for printing
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   101
  Bg, Brk, En: blocks and breaks for pretty printing*)
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   102
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   103
datatype xsymb =
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   104
  Delim of string |
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   105
  Argument of string * int |
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   106
  Space of string |
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   107
  Bg of int | Brk of int | En;
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
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   110
(*XProd (lhs, syms, c, p):
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   111
    lhs: name of nonterminal on the lhs of the production
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   112
    syms: list of symbols on the rhs of the production
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   113
    c: head of parse tree
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   114
    p: priority of this production*)
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
datatype xprod = XProd of string * xsymb list * string * int;
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   117
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   118
val max_pri = 1000;   (*maximum legal priority*)
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   119
val chain_pri = ~1;   (*dummy for chain productions*)
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   120
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
(* delims_of *)
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
fun delims_of xprods =
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   125
  let
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   126
    fun del_of (Delim s) = Some s
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   127
      | del_of _ = None;
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   128
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   129
    fun dels_of (XProd (_, xsymbs, _, _)) =
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   130
      mapfilter del_of xsymbs;
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   131
  in
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   132
    distinct (flat (map dels_of xprods))
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   133
  end;
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
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   136
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   137
(** datatype mfix **)
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   138
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   139
(*Mfix (sy, ty, c, ps, p):
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   140
    sy: rhs of production as symbolic string
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   141
    ty: type description of production
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   142
    c: head of parse tree
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   143
    ps: priorities of arguments in sy
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   144
    p: priority of production*)
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   145
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   146
datatype mfix = Mfix of string * typ * string * int list * int;
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   147
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   148
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   149
(* typ_to_nonterm *)
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   150
865
b38c67991122 added optional precedence for body of binder;
clasohm
parents: 780
diff changeset
   151
fun typ_to_nt _ (Type (c, _)) = c
b38c67991122 added optional precedence for body of binder;
clasohm
parents: 780
diff changeset
   152
  | typ_to_nt default _ = default;
b38c67991122 added optional precedence for body of binder;
clasohm
parents: 780
diff changeset
   153
764
b60e77395d1a changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents: 624
diff changeset
   154
(*get nonterminal for rhs*)
865
b38c67991122 added optional precedence for body of binder;
clasohm
parents: 780
diff changeset
   155
val typ_to_nonterm = typ_to_nt any;
240
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   156
764
b60e77395d1a changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents: 624
diff changeset
   157
(*get nonterminal for lhs*)
865
b38c67991122 added optional precedence for body of binder;
clasohm
parents: 780
diff changeset
   158
val typ_to_nonterm1 = typ_to_nt logic;
240
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   159
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   160
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   161
(* mfix_to_xprod *)
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
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
   164
  let
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   165
    fun err msg =
780
567f1fe7ea39 removed "logic1";
wenzelm
parents: 764
diff changeset
   166
      (writeln ("Error in mixfix annotation " ^ quote sy ^ " for "
764
b60e77395d1a changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents: 624
diff changeset
   167
                ^ quote const);
240
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   168
        error msg);
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   169
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   170
    fun check_pri p =
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   171
      if p >= 0 andalso p <= max_pri then ()
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   172
      else err ("precedence out of range: " ^ string_of_int p);
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   173
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   174
    fun blocks_ok [] 0 = true
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   175
      | blocks_ok [] _ = false
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   176
      | blocks_ok (Bg _ :: syms) n = blocks_ok syms (n + 1)
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   177
      | blocks_ok (En :: _) 0 = false
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   178
      | blocks_ok (En :: syms) n = blocks_ok syms (n - 1)
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   179
      | blocks_ok (_ :: syms) n = blocks_ok syms n;
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   180
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   181
    fun check_blocks syms =
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   182
      if blocks_ok syms 0 then ()
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   183
      else err "unbalanced block parentheses";
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   184
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   185
911
55754d6d399c new in mixfix annotations: "' " (quote space) separates delimiters without
wenzelm
parents: 865
diff changeset
   186
    local
55754d6d399c new in mixfix annotations: "' " (quote space) separates delimiters without
wenzelm
parents: 865
diff changeset
   187
      fun is_meta c = c mem ["(", ")", "/", "_"];
240
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   188
911
55754d6d399c new in mixfix annotations: "' " (quote space) separates delimiters without
wenzelm
parents: 865
diff changeset
   189
      fun scan_delim_char ("'" :: c :: cs) =
55754d6d399c new in mixfix annotations: "' " (quote space) separates delimiters without
wenzelm
parents: 865
diff changeset
   190
            if is_blank c then raise LEXICAL_ERROR else (c, cs)
55754d6d399c new in mixfix annotations: "' " (quote space) separates delimiters without
wenzelm
parents: 865
diff changeset
   191
        | scan_delim_char ["'"] = err "trailing escape character"
55754d6d399c new in mixfix annotations: "' " (quote space) separates delimiters without
wenzelm
parents: 865
diff changeset
   192
        | scan_delim_char (chs as c :: cs) =
55754d6d399c new in mixfix annotations: "' " (quote space) separates delimiters without
wenzelm
parents: 865
diff changeset
   193
            if is_blank c orelse is_meta c then raise LEXICAL_ERROR else (c, cs)
55754d6d399c new in mixfix annotations: "' " (quote space) separates delimiters without
wenzelm
parents: 865
diff changeset
   194
        | scan_delim_char [] = raise LEXICAL_ERROR;
240
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   195
911
55754d6d399c new in mixfix annotations: "' " (quote space) separates delimiters without
wenzelm
parents: 865
diff changeset
   196
      val scan_sym =
55754d6d399c new in mixfix annotations: "' " (quote space) separates delimiters without
wenzelm
parents: 865
diff changeset
   197
        $$ "_" >> K (Argument ("", 0)) ||
55754d6d399c new in mixfix annotations: "' " (quote space) separates delimiters without
wenzelm
parents: 865
diff changeset
   198
        $$ "(" -- scan_int >> (Bg o #2) ||
55754d6d399c new in mixfix annotations: "' " (quote space) separates delimiters without
wenzelm
parents: 865
diff changeset
   199
        $$ ")" >> K En ||
55754d6d399c new in mixfix annotations: "' " (quote space) separates delimiters without
wenzelm
parents: 865
diff changeset
   200
        $$ "/" -- $$ "/" >> K (Brk ~1) ||
55754d6d399c new in mixfix annotations: "' " (quote space) separates delimiters without
wenzelm
parents: 865
diff changeset
   201
        $$ "/" -- scan_any is_blank >> (Brk o length o #2) ||
55754d6d399c new in mixfix annotations: "' " (quote space) separates delimiters without
wenzelm
parents: 865
diff changeset
   202
        scan_any1 is_blank >> (Space o implode) ||
55754d6d399c new in mixfix annotations: "' " (quote space) separates delimiters without
wenzelm
parents: 865
diff changeset
   203
        repeat1 scan_delim_char >> (Delim o implode);
55754d6d399c new in mixfix annotations: "' " (quote space) separates delimiters without
wenzelm
parents: 865
diff changeset
   204
55754d6d399c new in mixfix annotations: "' " (quote space) separates delimiters without
wenzelm
parents: 865
diff changeset
   205
      val scan_symb =
55754d6d399c new in mixfix annotations: "' " (quote space) separates delimiters without
wenzelm
parents: 865
diff changeset
   206
        scan_sym >> Some ||
55754d6d399c new in mixfix annotations: "' " (quote space) separates delimiters without
wenzelm
parents: 865
diff changeset
   207
        $$ "'" -- scan_one is_blank >> K None;
55754d6d399c new in mixfix annotations: "' " (quote space) separates delimiters without
wenzelm
parents: 865
diff changeset
   208
    in
55754d6d399c new in mixfix annotations: "' " (quote space) separates delimiters without
wenzelm
parents: 865
diff changeset
   209
      val scan_symbs = mapfilter I o #1 o repeat scan_symb;
55754d6d399c new in mixfix annotations: "' " (quote space) separates delimiters without
wenzelm
parents: 865
diff changeset
   210
    end;
240
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   211
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   212
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   213
    val cons_fst = apfst o cons;
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   214
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   215
    fun add_args [] ty [] = ([], typ_to_nonterm1 ty)
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   216
      | add_args [] _ _ = err "too many precedences"
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   217
      | add_args (Argument _ :: syms) (Type ("fun", [ty, tys])) [] =
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   218
          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
   219
      | add_args (Argument _ :: syms) (Type ("fun", [ty, tys])) (p :: ps) =
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   220
          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
   221
      | add_args (Argument _ :: _) _ _ =
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   222
          err "more arguments than in corresponding type"
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   223
      | 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
   224
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   225
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   226
    fun is_arg (Argument _) = true
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   227
      | is_arg _ = false;
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   228
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   229
    fun is_term (Delim _) = true
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   230
      | is_term (Argument (s, _)) = is_terminal s
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   231
      | is_term _ = false;
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   232
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   233
    fun rem_pri (Argument (s, _)) = Argument (s, chain_pri)
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   234
      | rem_pri sym = sym;
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   235
764
b60e77395d1a changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents: 624
diff changeset
   236
    fun is_delim (Delim _) = true
b60e77395d1a changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents: 624
diff changeset
   237
      | is_delim _ = false;
b60e77395d1a changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents: 624
diff changeset
   238
b60e77395d1a changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents: 624
diff changeset
   239
    (*replace logical types on rhs by "logic"*)
b60e77395d1a changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents: 624
diff changeset
   240
    fun unify_logtypes copy_prod (a as (Argument (s, p))) =
b60e77395d1a changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents: 624
diff changeset
   241
          if s mem logtypes then Argument (logic, p)
b60e77395d1a changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents: 624
diff changeset
   242
          else a
b60e77395d1a changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents: 624
diff changeset
   243
      | unify_logtypes _ a = a;
240
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   244
911
55754d6d399c new in mixfix annotations: "' " (quote space) separates delimiters without
wenzelm
parents: 865
diff changeset
   245
    val raw_symbs = scan_symbs (explode sy);
240
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   246
    val (symbs, lhs) = add_args raw_symbs typ pris;
764
b60e77395d1a changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents: 624
diff changeset
   247
    val copy_prod = lhs mem ["prop", "logic"]
b60e77395d1a changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents: 624
diff changeset
   248
          andalso const <> ""
1145
d25b863ab2ac fixed bug in mfix_to_xprod: lambda productions' lhs shouldn't be modified
clasohm
parents: 922
diff changeset
   249
          andalso not (null symbs)
764
b60e77395d1a changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents: 624
diff changeset
   250
          andalso not (exists is_delim symbs);
b60e77395d1a changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents: 624
diff changeset
   251
    val lhs' = if convert andalso not copy_prod then
b60e77395d1a changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents: 624
diff changeset
   252
                 (if lhs mem logtypes then logic
b60e77395d1a changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents: 624
diff changeset
   253
                  else if lhs = "prop" then sprop else lhs)
b60e77395d1a changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents: 624
diff changeset
   254
               else lhs;
b60e77395d1a changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents: 624
diff changeset
   255
    val symbs' = map (unify_logtypes copy_prod) symbs;
b60e77395d1a changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents: 624
diff changeset
   256
    val xprod = XProd (lhs', symbs', const, pri);
240
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   257
  in
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   258
    seq check_pri pris;
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   259
    check_pri pri;
764
b60e77395d1a changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents: 624
diff changeset
   260
    check_blocks symbs';
240
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   261
764
b60e77395d1a changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents: 624
diff changeset
   262
    if is_terminal lhs' then err ("illegal lhs: " ^ lhs')
240
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   263
    else if const <> "" then xprod
764
b60e77395d1a changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents: 624
diff changeset
   264
    else if length (filter is_arg symbs') <> 1 then
240
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   265
      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
   266
    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
   267
    else XProd (lhs', map rem_pri symbs', "", chain_pri)
240
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   268
  end;
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   269
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   270
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   271
(** datatype syn_ext **)
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   272
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   273
datatype syn_ext =
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   274
  SynExt of {
764
b60e77395d1a changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents: 624
diff changeset
   275
    logtypes: string list,
240
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   276
    xprods: xprod list,
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   277
    consts: string list,
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   278
    parse_ast_translation: (string * (ast list -> ast)) list,
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   279
    parse_rules: (ast * ast) list,
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   280
    parse_translation: (string * (term list -> term)) list,
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   281
    print_translation: (string * (term list -> term)) list,
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   282
    print_rules: (ast * ast) list,
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   283
    print_ast_translation: (string * (ast list -> ast)) list};
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   284
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   285
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   286
(* syn_ext *)
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   287
764
b60e77395d1a changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents: 624
diff changeset
   288
fun mk_syn_ext convert logtypes mfixes consts trfuns rules =
240
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   289
  let
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   290
    val (parse_ast_translation, parse_translation, print_translation,
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   291
      print_ast_translation) = trfuns;
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   292
    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
   293
    val logtypes' = logtypes \ "prop";
240
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   294
624
33b9b5da3e6f made major changes to grammar;
clasohm
parents: 555
diff changeset
   295
    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
   296
    val xprods = map (mfix_to_xprod convert logtypes') mfixes;
240
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   297
  in
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   298
    SynExt {
764
b60e77395d1a changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents: 624
diff changeset
   299
      logtypes = logtypes',
624
33b9b5da3e6f made major changes to grammar;
clasohm
parents: 555
diff changeset
   300
      xprods = xprods,
368
e11b893cb7b6 moved 'filter is_xid' in syn_ext
clasohm
parents: 345
diff changeset
   301
      consts = filter is_xid (consts union mfix_consts),
240
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   302
      parse_ast_translation = parse_ast_translation,
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   303
      parse_rules = parse_rules,
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   304
      parse_translation = parse_translation,
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   305
      print_translation = print_translation,
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   306
      print_rules = print_rules,
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   307
      print_ast_translation = print_ast_translation}
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   308
  end;
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   309
764
b60e77395d1a changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents: 624
diff changeset
   310
val syn_ext = mk_syn_ext true;
240
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   311
764
b60e77395d1a changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents: 624
diff changeset
   312
fun syn_ext_logtypes logtypes =
b60e77395d1a changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents: 624
diff changeset
   313
  syn_ext logtypes [] [] ([], [], [], []) ([], []);
b60e77395d1a changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents: 624
diff changeset
   314
b60e77395d1a changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents: 624
diff changeset
   315
fun syn_ext_const_names logtypes cs =
b60e77395d1a changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents: 624
diff changeset
   316
  syn_ext logtypes [] cs ([], [], [], []) ([], []);
555
a7f397a14b16 removed idT, varT, tidT, tvarT (now in lexicon.ML);
wenzelm
parents: 441
diff changeset
   317
764
b60e77395d1a changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents: 624
diff changeset
   318
fun syn_ext_rules logtypes rules =
b60e77395d1a changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents: 624
diff changeset
   319
  syn_ext logtypes [] [] ([], [], [], []) rules;
b60e77395d1a changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents: 624
diff changeset
   320
b60e77395d1a changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents: 624
diff changeset
   321
fun syn_ext_trfuns logtypes trfuns =
b60e77395d1a changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents: 624
diff changeset
   322
  syn_ext logtypes [] [] trfuns ([], []);
240
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   323
764
b60e77395d1a changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents: 624
diff changeset
   324
(* pure_ext *)
240
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   325
764
b60e77395d1a changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents: 624
diff changeset
   326
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
   327
  [Mfix ("_", spropT --> propT, "", [0], 0),
b60e77395d1a changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents: 624
diff changeset
   328
   Mfix ("_", logicT --> anyT, "", [0], 0),
b60e77395d1a changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents: 624
diff changeset
   329
   Mfix ("_", spropT --> anyT, "", [0], 0),
b60e77395d1a changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents: 624
diff changeset
   330
   Mfix ("'(_')", logicT --> logicT, "", [0], max_pri),
b60e77395d1a changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents: 624
diff changeset
   331
   Mfix ("'(_')", spropT --> spropT, "", [0], max_pri),
b60e77395d1a changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents: 624
diff changeset
   332
   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
   333
   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
   334
  []
b60e77395d1a changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents: 624
diff changeset
   335
  ([], [], [], [])
b60e77395d1a changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents: 624
diff changeset
   336
  ([], []);
240
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   337
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   338
end;