src/Pure/Syntax/syn_ext.ML
author wenzelm
Mon, 31 May 2010 21:06:57 +0200
changeset 37216 3165bc303f66
parent 35429 afa8cf9e63d8
child 40959 49765c1104d4
permissions -rw-r--r--
modernized some structure names, keeping a few legacy aliases;
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
911
55754d6d399c new in mixfix annotations: "' " (quote space) separates delimiters without
wenzelm
parents: 865
diff changeset
     2
    Author:     Markus Wenzel and Carsten Clasohm, TU Muenchen
240
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
     3
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
     4
Syntax extension (internal interface).
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
     5
*)
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
signature SYN_EXT0 =
4050
543df9687d7b added mixfix_args;
wenzelm
parents: 2913
diff changeset
     8
sig
6760
1c56eb841afe added dddot_indexname;
wenzelm
parents: 6322
diff changeset
     9
  val dddot_indexname: indexname
1c56eb841afe added dddot_indexname;
wenzelm
parents: 6322
diff changeset
    10
  val constrainC: string
240
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
    11
  val typeT: typ
28856
5e009a80fe6d Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents: 26704
diff changeset
    12
  val spropT: typ
5690
4b056ee5435c no open;
wenzelm
parents: 4938
diff changeset
    13
  val max_pri: int
15754
f867c48de2e1 added stamp_trfun, mk_trfun, eq_trfun;
wenzelm
parents: 15570
diff changeset
    14
  val stamp_trfun: stamp -> string * 'a -> string * ('a * stamp)
f867c48de2e1 added stamp_trfun, mk_trfun, eq_trfun;
wenzelm
parents: 15570
diff changeset
    15
  val mk_trfun: string * 'a -> string * ('a * stamp)
f867c48de2e1 added stamp_trfun, mk_trfun, eq_trfun;
wenzelm
parents: 15570
diff changeset
    16
  val eq_trfun: ('a * stamp) * ('a * stamp) -> bool
35390
efad0e364738 use simplified Syntax.escape;
wenzelm
parents: 35351
diff changeset
    17
  val escape: string -> string
26704
51ee753cc2e3 token translations: context dependent, result Pretty.T;
wenzelm
parents: 25075
diff changeset
    18
  val tokentrans_mode:
51ee753cc2e3 token translations: context dependent, result Pretty.T;
wenzelm
parents: 25075
diff changeset
    19
    string -> (string * (Proof.context -> string -> Pretty.T)) list ->
51ee753cc2e3 token translations: context dependent, result Pretty.T;
wenzelm
parents: 25075
diff changeset
    20
    (string * string * (Proof.context -> string -> Pretty.T)) list
15835
fdf678bec567 added tokentrans_mode, standard_token_classes, standard_token_markers (from token_trans.ML);
wenzelm
parents: 15754
diff changeset
    21
  val standard_token_classes: string list
4050
543df9687d7b added mixfix_args;
wenzelm
parents: 2913
diff changeset
    22
end;
240
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
    23
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
    24
signature SYN_EXT =
4050
543df9687d7b added mixfix_args;
wenzelm
parents: 2913
diff changeset
    25
sig
240
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
    26
  include SYN_EXT0
1510
4588ba1b1438 Elimination of fully-functorial style.
paulson
parents: 1178
diff changeset
    27
  val logic: string
4588ba1b1438 Elimination of fully-functorial style.
paulson
parents: 1178
diff changeset
    28
  val args: string
4588ba1b1438 Elimination of fully-functorial style.
paulson
parents: 1178
diff changeset
    29
  val cargs: string
30189
3633f560f4c3 discontinued experimental support for Alice -- too hard to maintain its many language incompatibilities, never really worked anyway;
wenzelm
parents: 29565
diff changeset
    30
  val any: string
1510
4588ba1b1438 Elimination of fully-functorial style.
paulson
parents: 1178
diff changeset
    31
  val sprop: string
35351
7425aece4ee3 allow general mixfix syntax for type constructors;
wenzelm
parents: 35110
diff changeset
    32
  datatype mfix = Mfix of string * typ * string * int list * int
7425aece4ee3 allow general mixfix syntax for type constructors;
wenzelm
parents: 35110
diff changeset
    33
  val err_in_mfix: string -> mfix -> 'a
1510
4588ba1b1438 Elimination of fully-functorial style.
paulson
parents: 1178
diff changeset
    34
  val typ_to_nonterm: typ -> string
4588ba1b1438 Elimination of fully-functorial style.
paulson
parents: 1178
diff changeset
    35
  datatype xsymb =
4588ba1b1438 Elimination of fully-functorial style.
paulson
parents: 1178
diff changeset
    36
    Delim of string |
4588ba1b1438 Elimination of fully-functorial style.
paulson
parents: 1178
diff changeset
    37
    Argument of string * int |
4588ba1b1438 Elimination of fully-functorial style.
paulson
parents: 1178
diff changeset
    38
    Space of string |
4588ba1b1438 Elimination of fully-functorial style.
paulson
parents: 1178
diff changeset
    39
    Bg of int | Brk of int | En
4588ba1b1438 Elimination of fully-functorial style.
paulson
parents: 1178
diff changeset
    40
  datatype xprod = XProd of string * xsymb list * string * int
4588ba1b1438 Elimination of fully-functorial style.
paulson
parents: 1178
diff changeset
    41
  val chain_pri: int
4701
be8a8d60d962 adapted to new scanner and abroque chars;
wenzelm
parents: 4146
diff changeset
    42
  val delims_of: xprod list -> string list list
1510
4588ba1b1438 Elimination of fully-functorial style.
paulson
parents: 1178
diff changeset
    43
  datatype syn_ext =
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 35429
diff changeset
    44
    Syn_Ext of {
1510
4588ba1b1438 Elimination of fully-functorial style.
paulson
parents: 1178
diff changeset
    45
      xprods: xprod list,
4588ba1b1438 Elimination of fully-functorial style.
paulson
parents: 1178
diff changeset
    46
      consts: string list,
2913
ce271fa4d8e2 fixed diagnostic output of print modes;
wenzelm
parents: 2694
diff changeset
    47
      prmodes: string list,
21772
7c7ade4f537b advanced translation functions: Proof.context;
wenzelm
parents: 20675
diff changeset
    48
      parse_ast_translation: (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list,
1510
4588ba1b1438 Elimination of fully-functorial style.
paulson
parents: 1178
diff changeset
    49
      parse_rules: (Ast.ast * Ast.ast) list,
21772
7c7ade4f537b advanced translation functions: Proof.context;
wenzelm
parents: 20675
diff changeset
    50
      parse_translation: (string * ((Proof.context -> term list -> term) * stamp)) list,
18857
c4b4fbd74ffb advanced translations: Context.generic;
wenzelm
parents: 18678
diff changeset
    51
      print_translation:
21772
7c7ade4f537b advanced translation functions: Proof.context;
wenzelm
parents: 20675
diff changeset
    52
        (string * ((Proof.context -> bool -> typ -> term list -> term) * stamp)) list,
1510
4588ba1b1438 Elimination of fully-functorial style.
paulson
parents: 1178
diff changeset
    53
      print_rules: (Ast.ast * Ast.ast) list,
21772
7c7ade4f537b advanced translation functions: Proof.context;
wenzelm
parents: 20675
diff changeset
    54
      print_ast_translation: (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list,
26704
51ee753cc2e3 token translations: context dependent, result Pretty.T;
wenzelm
parents: 25075
diff changeset
    55
      token_translation: (string * string * (Proof.context -> string -> Pretty.T)) list}
19004
a72c7a1eb129 added mfix_delims;
wenzelm
parents: 18977
diff changeset
    56
  val mfix_delims: string -> string list
4054
wenzelm
parents: 4050
diff changeset
    57
  val mfix_args: string -> int
14903
d264b8ad3eec removed separate logtypes field of syntax;
wenzelm
parents: 14819
diff changeset
    58
  val syn_ext': bool -> (string -> bool) -> mfix list ->
21772
7c7ade4f537b advanced translation functions: Proof.context;
wenzelm
parents: 20675
diff changeset
    59
    string list -> (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list *
7c7ade4f537b advanced translation functions: Proof.context;
wenzelm
parents: 20675
diff changeset
    60
    (string * ((Proof.context -> term list -> term) * stamp)) list *
7c7ade4f537b advanced translation functions: Proof.context;
wenzelm
parents: 20675
diff changeset
    61
    (string * ((Proof.context -> bool -> typ -> term list -> term) * stamp)) list *
7c7ade4f537b advanced translation functions: Proof.context;
wenzelm
parents: 20675
diff changeset
    62
    (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list
26704
51ee753cc2e3 token translations: context dependent, result Pretty.T;
wenzelm
parents: 25075
diff changeset
    63
    -> (string * string * (Proof.context -> string -> Pretty.T)) list
1510
4588ba1b1438 Elimination of fully-functorial style.
paulson
parents: 1178
diff changeset
    64
    -> (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext
14903
d264b8ad3eec removed separate logtypes field of syntax;
wenzelm
parents: 14819
diff changeset
    65
  val syn_ext: mfix list -> string list ->
21772
7c7ade4f537b advanced translation functions: Proof.context;
wenzelm
parents: 20675
diff changeset
    66
    (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list *
7c7ade4f537b advanced translation functions: Proof.context;
wenzelm
parents: 20675
diff changeset
    67
    (string * ((Proof.context -> term list -> term) * stamp)) list *
7c7ade4f537b advanced translation functions: Proof.context;
wenzelm
parents: 20675
diff changeset
    68
    (string * ((Proof.context -> bool -> typ -> term list -> term) * stamp)) list *
7c7ade4f537b advanced translation functions: Proof.context;
wenzelm
parents: 20675
diff changeset
    69
    (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list
26704
51ee753cc2e3 token translations: context dependent, result Pretty.T;
wenzelm
parents: 25075
diff changeset
    70
    -> (string * string * (Proof.context -> string -> Pretty.T)) list
1510
4588ba1b1438 Elimination of fully-functorial style.
paulson
parents: 1178
diff changeset
    71
    -> (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext
14903
d264b8ad3eec removed separate logtypes field of syntax;
wenzelm
parents: 14819
diff changeset
    72
  val syn_ext_const_names: string list -> syn_ext
d264b8ad3eec removed separate logtypes field of syntax;
wenzelm
parents: 14819
diff changeset
    73
  val syn_ext_rules: (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext
d264b8ad3eec removed separate logtypes field of syntax;
wenzelm
parents: 14819
diff changeset
    74
  val syn_ext_trfuns:
15754
f867c48de2e1 added stamp_trfun, mk_trfun, eq_trfun;
wenzelm
parents: 15570
diff changeset
    75
    (string * ((Ast.ast list -> Ast.ast) * stamp)) list *
f867c48de2e1 added stamp_trfun, mk_trfun, eq_trfun;
wenzelm
parents: 15570
diff changeset
    76
    (string * ((term list -> term) * stamp)) list *
f867c48de2e1 added stamp_trfun, mk_trfun, eq_trfun;
wenzelm
parents: 15570
diff changeset
    77
    (string * ((bool -> typ -> term list -> term) * stamp)) list *
f867c48de2e1 added stamp_trfun, mk_trfun, eq_trfun;
wenzelm
parents: 15570
diff changeset
    78
    (string * ((Ast.ast list -> Ast.ast) * stamp)) list -> syn_ext
16610
58bf09036a6d accomodate advanced trfuns;
wenzelm
parents: 15973
diff changeset
    79
  val syn_ext_advanced_trfuns:
21772
7c7ade4f537b advanced translation functions: Proof.context;
wenzelm
parents: 20675
diff changeset
    80
    (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list *
7c7ade4f537b advanced translation functions: Proof.context;
wenzelm
parents: 20675
diff changeset
    81
    (string * ((Proof.context -> term list -> term) * stamp)) list *
7c7ade4f537b advanced translation functions: Proof.context;
wenzelm
parents: 20675
diff changeset
    82
    (string * ((Proof.context -> bool -> typ -> term list -> term) * stamp)) list *
7c7ade4f537b advanced translation functions: Proof.context;
wenzelm
parents: 20675
diff changeset
    83
    (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list -> syn_ext
26704
51ee753cc2e3 token translations: context dependent, result Pretty.T;
wenzelm
parents: 25075
diff changeset
    84
  val syn_ext_tokentrfuns: (string * string * (Proof.context -> string -> Pretty.T)) list -> syn_ext
15835
fdf678bec567 added tokentrans_mode, standard_token_classes, standard_token_markers (from token_trans.ML);
wenzelm
parents: 15754
diff changeset
    85
  val standard_token_markers: string list
1510
4588ba1b1438 Elimination of fully-functorial style.
paulson
parents: 1178
diff changeset
    86
  val pure_ext: syn_ext
4050
543df9687d7b added mixfix_args;
wenzelm
parents: 2913
diff changeset
    87
end;
240
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
    88
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 35429
diff changeset
    89
structure Syn_Ext: SYN_EXT =
240
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
    90
struct
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
    91
2694
b98365c6e869 added token_translation interface;
wenzelm
parents: 2382
diff changeset
    92
240
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
    93
(** misc definitions **)
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
    94
7472
f1208505d837 removed binding;
wenzelm
parents: 6760
diff changeset
    95
val dddot_indexname = ("dddot", 0);
6760
1c56eb841afe added dddot_indexname;
wenzelm
parents: 6322
diff changeset
    96
val constrainC = "_constrain";
1c56eb841afe added dddot_indexname;
wenzelm
parents: 6322
diff changeset
    97
1c56eb841afe added dddot_indexname;
wenzelm
parents: 6322
diff changeset
    98
240
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
    99
(* syntactic categories *)
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
val logic = "logic";
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   102
val logicT = Type (logic, []);
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
val args = "args";
1178
b28c6ecc3e6d added cargs for curried function application
clasohm
parents: 1145
diff changeset
   105
val cargs = "cargs";
240
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   106
330
2fda15dd1e0f changed the way a grammar is generated to allow the new parser to work;
clasohm
parents: 240
diff changeset
   107
val typeT = Type ("type", []);
240
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   108
764
b60e77395d1a changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents: 624
diff changeset
   109
val sprop = "#prop";
b60e77395d1a changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents: 624
diff changeset
   110
val spropT = Type (sprop, []);
240
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   111
30189
3633f560f4c3 discontinued experimental support for Alice -- too hard to maintain its many language incompatibilities, never really worked anyway;
wenzelm
parents: 29565
diff changeset
   112
val any = "any";
3633f560f4c3 discontinued experimental support for Alice -- too hard to maintain its many language incompatibilities, never really worked anyway;
wenzelm
parents: 29565
diff changeset
   113
val anyT = Type (any, []);
624
33b9b5da3e6f made major changes to grammar;
clasohm
parents: 555
diff changeset
   114
780
567f1fe7ea39 removed "logic1";
wenzelm
parents: 764
diff changeset
   115
240
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   116
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   117
(** datatype xprod **)
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   118
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   119
(*Delim s: delimiter s
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   120
  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
   121
  Space s: some white space for printing
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   122
  Bg, Brk, En: blocks and breaks for pretty printing*)
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
datatype xsymb =
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   125
  Delim of string |
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   126
  Argument of string * int |
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   127
  Space of string |
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   128
  Bg of int | Brk of int | En;
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   129
12513
0ffb824dc95c support for ``indexed syntax'' (using "\<index>" argument instead of "_");
wenzelm
parents: 11546
diff changeset
   130
fun is_delim (Delim _) = true
0ffb824dc95c support for ``indexed syntax'' (using "\<index>" argument instead of "_");
wenzelm
parents: 11546
diff changeset
   131
  | is_delim _ = false;
0ffb824dc95c support for ``indexed syntax'' (using "\<index>" argument instead of "_");
wenzelm
parents: 11546
diff changeset
   132
0ffb824dc95c support for ``indexed syntax'' (using "\<index>" argument instead of "_");
wenzelm
parents: 11546
diff changeset
   133
fun is_terminal (Delim _) = true
0ffb824dc95c support for ``indexed syntax'' (using "\<index>" argument instead of "_");
wenzelm
parents: 11546
diff changeset
   134
  | is_terminal (Argument (s, _)) = Lexicon.is_terminal s
0ffb824dc95c support for ``indexed syntax'' (using "\<index>" argument instead of "_");
wenzelm
parents: 11546
diff changeset
   135
  | is_terminal _ = false;
0ffb824dc95c support for ``indexed syntax'' (using "\<index>" argument instead of "_");
wenzelm
parents: 11546
diff changeset
   136
0ffb824dc95c support for ``indexed syntax'' (using "\<index>" argument instead of "_");
wenzelm
parents: 11546
diff changeset
   137
fun is_argument (Argument _) = true
0ffb824dc95c support for ``indexed syntax'' (using "\<index>" argument instead of "_");
wenzelm
parents: 11546
diff changeset
   138
  | is_argument _ = false;
0ffb824dc95c support for ``indexed syntax'' (using "\<index>" argument instead of "_");
wenzelm
parents: 11546
diff changeset
   139
0ffb824dc95c support for ``indexed syntax'' (using "\<index>" argument instead of "_");
wenzelm
parents: 11546
diff changeset
   140
fun is_index (Argument ("index", _)) = true
0ffb824dc95c support for ``indexed syntax'' (using "\<index>" argument instead of "_");
wenzelm
parents: 11546
diff changeset
   141
  | is_index _ = false;
0ffb824dc95c support for ``indexed syntax'' (using "\<index>" argument instead of "_");
wenzelm
parents: 11546
diff changeset
   142
0ffb824dc95c support for ``indexed syntax'' (using "\<index>" argument instead of "_");
wenzelm
parents: 11546
diff changeset
   143
val index = Argument ("index", 1000);
0ffb824dc95c support for ``indexed syntax'' (using "\<index>" argument instead of "_");
wenzelm
parents: 11546
diff changeset
   144
240
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
(*XProd (lhs, syms, c, p):
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   147
    lhs: name of nonterminal on the lhs of the production
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   148
    syms: list of symbols on the rhs of the production
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   149
    c: head of parse tree
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   150
    p: priority of this 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 xprod = XProd of string * xsymb list * string * 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
val max_pri = 1000;   (*maximum legal priority*)
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   155
val chain_pri = ~1;   (*dummy for chain productions*)
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   156
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   157
fun delims_of xprods =
19004
a72c7a1eb129 added mfix_delims;
wenzelm
parents: 18977
diff changeset
   158
  fold (fn XProd (_, xsymbs, _, _) =>
a72c7a1eb129 added mfix_delims;
wenzelm
parents: 18977
diff changeset
   159
    fold (fn Delim s => insert (op =) s | _ => I) xsymbs) xprods []
a72c7a1eb129 added mfix_delims;
wenzelm
parents: 18977
diff changeset
   160
  |> map Symbol.explode;
240
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   161
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   162
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   163
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   164
(** datatype mfix **)
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
(*Mfix (sy, ty, c, ps, p):
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   167
    sy: rhs of production as symbolic string
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   168
    ty: type description of production
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   169
    c: head of parse tree
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   170
    ps: priorities of arguments in sy
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   171
    p: priority of production*)
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   172
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   173
datatype mfix = Mfix of string * typ * string * int list * int;
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   174
12513
0ffb824dc95c support for ``indexed syntax'' (using "\<index>" argument instead of "_");
wenzelm
parents: 11546
diff changeset
   175
fun err_in_mfix msg (Mfix (sy, _, const, _, _)) =
18678
dd0c569fa43d sane ERROR handling;
wenzelm
parents: 18566
diff changeset
   176
  cat_error msg ("in mixfix annotation " ^ quote sy ^ " for " ^ quote const);
12513
0ffb824dc95c support for ``indexed syntax'' (using "\<index>" argument instead of "_");
wenzelm
parents: 11546
diff changeset
   177
240
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   178
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   179
(* typ_to_nonterm *)
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   180
865
b38c67991122 added optional precedence for body of binder;
clasohm
parents: 780
diff changeset
   181
fun typ_to_nt _ (Type (c, _)) = c
b38c67991122 added optional precedence for body of binder;
clasohm
parents: 780
diff changeset
   182
  | typ_to_nt default _ = default;
b38c67991122 added optional precedence for body of binder;
clasohm
parents: 780
diff changeset
   183
764
b60e77395d1a changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents: 624
diff changeset
   184
(*get nonterminal for rhs*)
30189
3633f560f4c3 discontinued experimental support for Alice -- too hard to maintain its many language incompatibilities, never really worked anyway;
wenzelm
parents: 29565
diff changeset
   185
val typ_to_nonterm = typ_to_nt any;
240
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   186
764
b60e77395d1a changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents: 624
diff changeset
   187
(*get nonterminal for lhs*)
865
b38c67991122 added optional precedence for body of binder;
clasohm
parents: 780
diff changeset
   188
val typ_to_nonterm1 = typ_to_nt logic;
240
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   189
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   190
19004
a72c7a1eb129 added mfix_delims;
wenzelm
parents: 18977
diff changeset
   191
(* read mixfix annotations *)
4050
543df9687d7b added mixfix_args;
wenzelm
parents: 2913
diff changeset
   192
543df9687d7b added mixfix_args;
wenzelm
parents: 2913
diff changeset
   193
local
19004
a72c7a1eb129 added mfix_delims;
wenzelm
parents: 18977
diff changeset
   194
20675
cb19d18aef01 member (op =);
wenzelm
parents: 20076
diff changeset
   195
val is_meta = member (op =) ["(", ")", "/", "_", "\\<index>"];
19004
a72c7a1eb129 added mfix_delims;
wenzelm
parents: 18977
diff changeset
   196
a72c7a1eb129 added mfix_delims;
wenzelm
parents: 18977
diff changeset
   197
val scan_delim_char =
23784
75e6b9dd5336 Symbol.not_eof/sync is superceded by Symbol.is_regular (rules out further control symbols);
wenzelm
parents: 23660
diff changeset
   198
  $$ "'" |-- Scan.one ((not o Symbol.is_blank) andf Symbol.is_regular) ||
75e6b9dd5336 Symbol.not_eof/sync is superceded by Symbol.is_regular (rules out further control symbols);
wenzelm
parents: 23660
diff changeset
   199
  Scan.one ((not o is_meta) andf (not o Symbol.is_blank) andf Symbol.is_regular);
19004
a72c7a1eb129 added mfix_delims;
wenzelm
parents: 18977
diff changeset
   200
a72c7a1eb129 added mfix_delims;
wenzelm
parents: 18977
diff changeset
   201
fun read_int ["0", "0"] = ~1
a72c7a1eb129 added mfix_delims;
wenzelm
parents: 18977
diff changeset
   202
  | read_int cs = #1 (Library.read_int cs);
4050
543df9687d7b added mixfix_args;
wenzelm
parents: 2913
diff changeset
   203
19004
a72c7a1eb129 added mfix_delims;
wenzelm
parents: 18977
diff changeset
   204
val scan_sym =
a72c7a1eb129 added mfix_delims;
wenzelm
parents: 18977
diff changeset
   205
  $$ "_" >> K (Argument ("", 0)) ||
a72c7a1eb129 added mfix_delims;
wenzelm
parents: 18977
diff changeset
   206
  $$ "\\<index>" >> K index ||
21858
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 21772
diff changeset
   207
  $$ "(" |-- Scan.many Symbol.is_digit >> (Bg o read_int) ||
19004
a72c7a1eb129 added mfix_delims;
wenzelm
parents: 18977
diff changeset
   208
  $$ ")" >> K En ||
a72c7a1eb129 added mfix_delims;
wenzelm
parents: 18977
diff changeset
   209
  $$ "/" -- $$ "/" >> K (Brk ~1) ||
21858
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 21772
diff changeset
   210
  $$ "/" |-- Scan.many Symbol.is_blank >> (Brk o length) ||
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 21772
diff changeset
   211
  Scan.many1 Symbol.is_blank >> (Space o implode) ||
19004
a72c7a1eb129 added mfix_delims;
wenzelm
parents: 18977
diff changeset
   212
  Scan.repeat1 scan_delim_char >> (Delim o implode);
14819
4dae1cb304a4 Library.read_int;
wenzelm
parents: 14697
diff changeset
   213
19004
a72c7a1eb129 added mfix_delims;
wenzelm
parents: 18977
diff changeset
   214
val scan_symb =
a72c7a1eb129 added mfix_delims;
wenzelm
parents: 18977
diff changeset
   215
  scan_sym >> SOME ||
a72c7a1eb129 added mfix_delims;
wenzelm
parents: 18977
diff changeset
   216
  $$ "'" -- Scan.one Symbol.is_blank >> K NONE;
a72c7a1eb129 added mfix_delims;
wenzelm
parents: 18977
diff changeset
   217
19305
5c16895d548b avoid polymorphic equality;
wenzelm
parents: 19046
diff changeset
   218
val scan_symbs = Scan.repeat scan_symb --| Scan.ahead (~$$ "'");
19482
9f11af8f7ef9 tuned basic list operators (flat, maps, map_filter);
wenzelm
parents: 19305
diff changeset
   219
val read_symbs = map_filter I o the o Scan.read Symbol.stopper scan_symbs;
4050
543df9687d7b added mixfix_args;
wenzelm
parents: 2913
diff changeset
   220
19004
a72c7a1eb129 added mfix_delims;
wenzelm
parents: 18977
diff changeset
   221
fun unique_index xsymbs =
33317
b4534348b8fd standardized filter/filter_out;
wenzelm
parents: 33042
diff changeset
   222
  if length (filter is_index xsymbs) <= 1 then xsymbs
19004
a72c7a1eb129 added mfix_delims;
wenzelm
parents: 18977
diff changeset
   223
  else error "Duplicate index arguments (\\<index>)";
4050
543df9687d7b added mixfix_args;
wenzelm
parents: 2913
diff changeset
   224
19004
a72c7a1eb129 added mfix_delims;
wenzelm
parents: 18977
diff changeset
   225
in
12513
0ffb824dc95c support for ``indexed syntax'' (using "\<index>" argument instead of "_");
wenzelm
parents: 11546
diff changeset
   226
19004
a72c7a1eb129 added mfix_delims;
wenzelm
parents: 18977
diff changeset
   227
val read_mfix = unique_index o read_symbs o Symbol.explode;
a72c7a1eb129 added mfix_delims;
wenzelm
parents: 18977
diff changeset
   228
a72c7a1eb129 added mfix_delims;
wenzelm
parents: 18977
diff changeset
   229
fun mfix_delims sy = fold_rev (fn Delim s => cons s | _ => I) (read_mfix sy) [];
33317
b4534348b8fd standardized filter/filter_out;
wenzelm
parents: 33042
diff changeset
   230
val mfix_args = length o filter is_argument o read_mfix;
19004
a72c7a1eb129 added mfix_delims;
wenzelm
parents: 18977
diff changeset
   231
35390
efad0e364738 use simplified Syntax.escape;
wenzelm
parents: 35351
diff changeset
   232
val escape = implode o map (fn s => if is_meta s then "'" ^ s else s) o Symbol.explode;
19004
a72c7a1eb129 added mfix_delims;
wenzelm
parents: 18977
diff changeset
   233
4050
543df9687d7b added mixfix_args;
wenzelm
parents: 2913
diff changeset
   234
end;
543df9687d7b added mixfix_args;
wenzelm
parents: 2913
diff changeset
   235
543df9687d7b added mixfix_args;
wenzelm
parents: 2913
diff changeset
   236
240
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   237
(* mfix_to_xprod *)
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   238
14903
d264b8ad3eec removed separate logtypes field of syntax;
wenzelm
parents: 14819
diff changeset
   239
fun mfix_to_xprod convert is_logtype (mfix as Mfix (sy, typ, const, pris, pri)) =
240
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   240
  let
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   241
    fun check_pri p =
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   242
      if p >= 0 andalso p <= max_pri then ()
12513
0ffb824dc95c support for ``indexed syntax'' (using "\<index>" argument instead of "_");
wenzelm
parents: 11546
diff changeset
   243
      else err_in_mfix ("Precedence out of range: " ^ string_of_int p) mfix;
240
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   244
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   245
    fun blocks_ok [] 0 = true
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   246
      | blocks_ok [] _ = false
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   247
      | blocks_ok (Bg _ :: syms) n = blocks_ok syms (n + 1)
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   248
      | blocks_ok (En :: _) 0 = false
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   249
      | blocks_ok (En :: syms) n = blocks_ok syms (n - 1)
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   250
      | blocks_ok (_ :: syms) n = blocks_ok syms n;
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   251
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   252
    fun check_blocks syms =
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   253
      if blocks_ok syms 0 then ()
12513
0ffb824dc95c support for ``indexed syntax'' (using "\<index>" argument instead of "_");
wenzelm
parents: 11546
diff changeset
   254
      else err_in_mfix "Unbalanced block parentheses" mfix;
240
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   255
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   256
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   257
    val cons_fst = apfst o cons;
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   258
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   259
    fun add_args [] ty [] = ([], typ_to_nonterm1 ty)
12513
0ffb824dc95c support for ``indexed syntax'' (using "\<index>" argument instead of "_");
wenzelm
parents: 11546
diff changeset
   260
      | add_args [] _ _ = err_in_mfix "Too many precedences" mfix
0ffb824dc95c support for ``indexed syntax'' (using "\<index>" argument instead of "_");
wenzelm
parents: 11546
diff changeset
   261
      | add_args ((arg as Argument ("index", _)) :: syms) ty ps =
0ffb824dc95c support for ``indexed syntax'' (using "\<index>" argument instead of "_");
wenzelm
parents: 11546
diff changeset
   262
          cons_fst arg (add_args syms ty ps)
240
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   263
      | add_args (Argument _ :: syms) (Type ("fun", [ty, tys])) [] =
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   264
          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
   265
      | add_args (Argument _ :: syms) (Type ("fun", [ty, tys])) (p :: ps) =
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   266
          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
   267
      | add_args (Argument _ :: _) _ _ =
12513
0ffb824dc95c support for ``indexed syntax'' (using "\<index>" argument instead of "_");
wenzelm
parents: 11546
diff changeset
   268
          err_in_mfix "More arguments than in corresponding type" mfix
240
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   269
      | 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
   270
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   271
    fun rem_pri (Argument (s, _)) = Argument (s, chain_pri)
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   272
      | rem_pri sym = sym;
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   273
32785
ec5292653aff eliminated redundant parameters;
wenzelm
parents: 30189
diff changeset
   274
    fun logify_types (a as (Argument (s, p))) =
14903
d264b8ad3eec removed separate logtypes field of syntax;
wenzelm
parents: 14819
diff changeset
   275
          if s <> "prop" andalso is_logtype s then Argument (logic, p) else a
32785
ec5292653aff eliminated redundant parameters;
wenzelm
parents: 30189
diff changeset
   276
      | logify_types a = a;
240
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   277
2364
821f44a0abba mfix_to_xprod: now uses read_charnames;
wenzelm
parents: 2254
diff changeset
   278
19004
a72c7a1eb129 added mfix_delims;
wenzelm
parents: 18977
diff changeset
   279
    val raw_symbs = read_mfix sy handle ERROR msg => err_in_mfix msg mfix;
33317
b4534348b8fd standardized filter/filter_out;
wenzelm
parents: 33042
diff changeset
   280
    val args = filter (fn Argument _ => true | _ => false) raw_symbs;
12513
0ffb824dc95c support for ``indexed syntax'' (using "\<index>" argument instead of "_");
wenzelm
parents: 11546
diff changeset
   281
    val (const', typ', parse_rules) =
0ffb824dc95c support for ``indexed syntax'' (using "\<index>" argument instead of "_");
wenzelm
parents: 11546
diff changeset
   282
      if not (exists is_index args) then (const, typ, [])
0ffb824dc95c support for ``indexed syntax'' (using "\<index>" argument instead of "_");
wenzelm
parents: 11546
diff changeset
   283
      else
0ffb824dc95c support for ``indexed syntax'' (using "\<index>" argument instead of "_");
wenzelm
parents: 11546
diff changeset
   284
        let
35429
afa8cf9e63d8 authentic syntax for classes and type constructors;
wenzelm
parents: 35390
diff changeset
   285
          val indexed_const =
afa8cf9e63d8 authentic syntax for classes and type constructors;
wenzelm
parents: 35390
diff changeset
   286
            if const <> "" then const ^ "_indexed"
12513
0ffb824dc95c support for ``indexed syntax'' (using "\<index>" argument instead of "_");
wenzelm
parents: 11546
diff changeset
   287
            else err_in_mfix "Missing constant name for indexed syntax" mfix;
14697
5ad13d05049b improved indexed syntax / implicit structures;
wenzelm
parents: 14647
diff changeset
   288
          val rangeT = Term.range_type typ handle Match =>
12513
0ffb824dc95c support for ``indexed syntax'' (using "\<index>" argument instead of "_");
wenzelm
parents: 11546
diff changeset
   289
            err_in_mfix "Missing structure argument for indexed syntax" mfix;
0ffb824dc95c support for ``indexed syntax'' (using "\<index>" argument instead of "_");
wenzelm
parents: 11546
diff changeset
   290
20076
def4ad161528 Name.invent_list;
wenzelm
parents: 19482
diff changeset
   291
          val xs = map Ast.Variable (Name.invent_list [] "xa" (length args - 1));
19012
wenzelm
parents: 19004
diff changeset
   292
          val (xs1, xs2) = chop (find_index is_index args) xs;
12513
0ffb824dc95c support for ``indexed syntax'' (using "\<index>" argument instead of "_");
wenzelm
parents: 11546
diff changeset
   293
          val i = Ast.Variable "i";
14697
5ad13d05049b improved indexed syntax / implicit structures;
wenzelm
parents: 14647
diff changeset
   294
          val lhs = Ast.mk_appl (Ast.Constant indexed_const)
5ad13d05049b improved indexed syntax / implicit structures;
wenzelm
parents: 14647
diff changeset
   295
            (xs1 @ [Ast.mk_appl (Ast.Constant "_index") [i]] @ xs2);
5ad13d05049b improved indexed syntax / implicit structures;
wenzelm
parents: 14647
diff changeset
   296
          val rhs = Ast.mk_appl (Ast.Constant const) (i :: xs);
5ad13d05049b improved indexed syntax / implicit structures;
wenzelm
parents: 14647
diff changeset
   297
        in (indexed_const, rangeT, [(lhs, rhs)]) end;
12513
0ffb824dc95c support for ``indexed syntax'' (using "\<index>" argument instead of "_");
wenzelm
parents: 11546
diff changeset
   298
0ffb824dc95c support for ``indexed syntax'' (using "\<index>" argument instead of "_");
wenzelm
parents: 11546
diff changeset
   299
    val (symbs, lhs) = add_args raw_symbs typ' pris;
0ffb824dc95c support for ``indexed syntax'' (using "\<index>" argument instead of "_");
wenzelm
parents: 11546
diff changeset
   300
2364
821f44a0abba mfix_to_xprod: now uses read_charnames;
wenzelm
parents: 2254
diff changeset
   301
    val copy_prod =
20675
cb19d18aef01 member (op =);
wenzelm
parents: 20076
diff changeset
   302
      (lhs = "prop" orelse lhs = "logic")
2364
821f44a0abba mfix_to_xprod: now uses read_charnames;
wenzelm
parents: 2254
diff changeset
   303
        andalso const <> ""
821f44a0abba mfix_to_xprod: now uses read_charnames;
wenzelm
parents: 2254
diff changeset
   304
        andalso not (null symbs)
821f44a0abba mfix_to_xprod: now uses read_charnames;
wenzelm
parents: 2254
diff changeset
   305
        andalso not (exists is_delim symbs);
821f44a0abba mfix_to_xprod: now uses read_charnames;
wenzelm
parents: 2254
diff changeset
   306
    val lhs' =
821f44a0abba mfix_to_xprod: now uses read_charnames;
wenzelm
parents: 2254
diff changeset
   307
      if convert andalso not copy_prod then
14903
d264b8ad3eec removed separate logtypes field of syntax;
wenzelm
parents: 14819
diff changeset
   308
       (if lhs = "prop" then sprop else if is_logtype lhs then logic else lhs)
2364
821f44a0abba mfix_to_xprod: now uses read_charnames;
wenzelm
parents: 2254
diff changeset
   309
      else lhs;
32785
ec5292653aff eliminated redundant parameters;
wenzelm
parents: 30189
diff changeset
   310
    val symbs' = map logify_types symbs;
12513
0ffb824dc95c support for ``indexed syntax'' (using "\<index>" argument instead of "_");
wenzelm
parents: 11546
diff changeset
   311
    val xprod = XProd (lhs', symbs', const', pri);
240
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   312
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   313
    val _ = (List.app check_pri pris; check_pri pri; check_blocks symbs');
12513
0ffb824dc95c support for ``indexed syntax'' (using "\<index>" argument instead of "_");
wenzelm
parents: 11546
diff changeset
   314
    val xprod' =
0ffb824dc95c support for ``indexed syntax'' (using "\<index>" argument instead of "_");
wenzelm
parents: 11546
diff changeset
   315
      if Lexicon.is_terminal lhs' then err_in_mfix ("Illegal lhs: " ^ lhs') mfix
0ffb824dc95c support for ``indexed syntax'' (using "\<index>" argument instead of "_");
wenzelm
parents: 11546
diff changeset
   316
      else if const <> "" then xprod
33317
b4534348b8fd standardized filter/filter_out;
wenzelm
parents: 33042
diff changeset
   317
      else if length (filter is_argument symbs') <> 1 then
12513
0ffb824dc95c support for ``indexed syntax'' (using "\<index>" argument instead of "_");
wenzelm
parents: 11546
diff changeset
   318
        err_in_mfix "Copy production must have exactly one argument" mfix
0ffb824dc95c support for ``indexed syntax'' (using "\<index>" argument instead of "_");
wenzelm
parents: 11546
diff changeset
   319
      else if exists is_terminal symbs' then xprod
0ffb824dc95c support for ``indexed syntax'' (using "\<index>" argument instead of "_");
wenzelm
parents: 11546
diff changeset
   320
      else XProd (lhs', map rem_pri symbs', "", chain_pri);
0ffb824dc95c support for ``indexed syntax'' (using "\<index>" argument instead of "_");
wenzelm
parents: 11546
diff changeset
   321
0ffb824dc95c support for ``indexed syntax'' (using "\<index>" argument instead of "_");
wenzelm
parents: 11546
diff changeset
   322
  in (xprod', parse_rules) end;
0ffb824dc95c support for ``indexed syntax'' (using "\<index>" argument instead of "_");
wenzelm
parents: 11546
diff changeset
   323
240
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   324
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   325
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   326
(** datatype syn_ext **)
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   327
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   328
datatype syn_ext =
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 35429
diff changeset
   329
  Syn_Ext of {
240
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   330
    xprods: xprod list,
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   331
    consts: string list,
2913
ce271fa4d8e2 fixed diagnostic output of print modes;
wenzelm
parents: 2694
diff changeset
   332
    prmodes: string list,
21772
7c7ade4f537b advanced translation functions: Proof.context;
wenzelm
parents: 20675
diff changeset
   333
    parse_ast_translation: (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list,
1510
4588ba1b1438 Elimination of fully-functorial style.
paulson
parents: 1178
diff changeset
   334
    parse_rules: (Ast.ast * Ast.ast) list,
21772
7c7ade4f537b advanced translation functions: Proof.context;
wenzelm
parents: 20675
diff changeset
   335
    parse_translation: (string * ((Proof.context -> term list -> term) * stamp)) list,
18857
c4b4fbd74ffb advanced translations: Context.generic;
wenzelm
parents: 18678
diff changeset
   336
    print_translation:
21772
7c7ade4f537b advanced translation functions: Proof.context;
wenzelm
parents: 20675
diff changeset
   337
      (string * ((Proof.context -> bool -> typ -> term list -> term) * stamp)) list,
1510
4588ba1b1438 Elimination of fully-functorial style.
paulson
parents: 1178
diff changeset
   338
    print_rules: (Ast.ast * Ast.ast) list,
21772
7c7ade4f537b advanced translation functions: Proof.context;
wenzelm
parents: 20675
diff changeset
   339
    print_ast_translation: (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list,
26704
51ee753cc2e3 token translations: context dependent, result Pretty.T;
wenzelm
parents: 25075
diff changeset
   340
    token_translation: (string * string * (Proof.context -> string -> Pretty.T)) list};
240
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   341
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   342
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   343
(* syn_ext *)
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   344
14903
d264b8ad3eec removed separate logtypes field of syntax;
wenzelm
parents: 14819
diff changeset
   345
fun syn_ext' convert is_logtype mfixes consts trfuns tokentrfuns (parse_rules, print_rules) =
240
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   346
  let
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   347
    val (parse_ast_translation, parse_translation, print_translation,
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   348
      print_ast_translation) = trfuns;
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   349
14903
d264b8ad3eec removed separate logtypes field of syntax;
wenzelm
parents: 14819
diff changeset
   350
    val (xprods, parse_rules') = map (mfix_to_xprod convert is_logtype) mfixes
19482
9f11af8f7ef9 tuned basic list operators (flat, maps, map_filter);
wenzelm
parents: 19305
diff changeset
   351
      |> split_list |> apsnd (rev o flat);
19046
bc5c6c9b114e removed distinct, renamed gen_distinct to distinct;
wenzelm
parents: 19012
diff changeset
   352
    val mfix_consts =
bc5c6c9b114e removed distinct, renamed gen_distinct to distinct;
wenzelm
parents: 19012
diff changeset
   353
      distinct (op =) (map (fn Mfix x => #3 x) mfixes @ map (fn XProd x => #3 x) xprods);
240
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   354
  in
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 35429
diff changeset
   355
    Syn_Ext {
624
33b9b5da3e6f made major changes to grammar;
clasohm
parents: 555
diff changeset
   356
      xprods = xprods,
33042
ddf1f03a9ad9 curried union as canonical list operation
haftmann
parents: 33038
diff changeset
   357
      consts = union (op =) consts mfix_consts,
19046
bc5c6c9b114e removed distinct, renamed gen_distinct to distinct;
wenzelm
parents: 19012
diff changeset
   358
      prmodes = distinct (op =) (map (fn (m, _, _) => m) tokentrfuns),
240
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   359
      parse_ast_translation = parse_ast_translation,
12513
0ffb824dc95c support for ``indexed syntax'' (using "\<index>" argument instead of "_");
wenzelm
parents: 11546
diff changeset
   360
      parse_rules = parse_rules' @ parse_rules,
240
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   361
      parse_translation = parse_translation,
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   362
      print_translation = print_translation,
12513
0ffb824dc95c support for ``indexed syntax'' (using "\<index>" argument instead of "_");
wenzelm
parents: 11546
diff changeset
   363
      print_rules = map swap parse_rules' @ print_rules,
2694
b98365c6e869 added token_translation interface;
wenzelm
parents: 2382
diff changeset
   364
      print_ast_translation = print_ast_translation,
b98365c6e869 added token_translation interface;
wenzelm
parents: 2382
diff changeset
   365
      token_translation = tokentrfuns}
240
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   366
  end;
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   367
2382
e7c2bce815ba added fix_tr', syn_ext_trfunsT;
wenzelm
parents: 2364
diff changeset
   368
14903
d264b8ad3eec removed separate logtypes field of syntax;
wenzelm
parents: 14819
diff changeset
   369
val syn_ext = syn_ext' true (K false);
555
a7f397a14b16 removed idT, varT, tidT, tvarT (now in lexicon.ML);
wenzelm
parents: 441
diff changeset
   370
14903
d264b8ad3eec removed separate logtypes field of syntax;
wenzelm
parents: 14819
diff changeset
   371
fun syn_ext_const_names cs = syn_ext [] cs ([], [], [], []) [] ([], []);
d264b8ad3eec removed separate logtypes field of syntax;
wenzelm
parents: 14819
diff changeset
   372
fun syn_ext_rules rules = syn_ext [] [] ([], [], [], []) [] rules;
16610
58bf09036a6d accomodate advanced trfuns;
wenzelm
parents: 15973
diff changeset
   373
fun syn_ext_advanced_trfuns trfuns = syn_ext [] [] trfuns [] ([], []);
14903
d264b8ad3eec removed separate logtypes field of syntax;
wenzelm
parents: 14819
diff changeset
   374
fun syn_ext_tokentrfuns trfuns = syn_ext [] [] ([], [], [], []) trfuns ([], []);
2382
e7c2bce815ba added fix_tr', syn_ext_trfunsT;
wenzelm
parents: 2364
diff changeset
   375
16610
58bf09036a6d accomodate advanced trfuns;
wenzelm
parents: 15973
diff changeset
   376
fun syn_ext_trfuns (atrs, trs, tr's, atr's) =
58bf09036a6d accomodate advanced trfuns;
wenzelm
parents: 15973
diff changeset
   377
  let fun simple (name, (f, s)) = (name, (K f, s)) in
58bf09036a6d accomodate advanced trfuns;
wenzelm
parents: 15973
diff changeset
   378
    syn_ext_advanced_trfuns (map simple atrs, map simple trs, map simple tr's, map simple atr's)
58bf09036a6d accomodate advanced trfuns;
wenzelm
parents: 15973
diff changeset
   379
  end;
58bf09036a6d accomodate advanced trfuns;
wenzelm
parents: 15973
diff changeset
   380
15754
f867c48de2e1 added stamp_trfun, mk_trfun, eq_trfun;
wenzelm
parents: 15570
diff changeset
   381
fun stamp_trfun s (c, f) = (c, (f, s));
f867c48de2e1 added stamp_trfun, mk_trfun, eq_trfun;
wenzelm
parents: 15570
diff changeset
   382
fun mk_trfun tr = stamp_trfun (stamp ()) tr;
29318
6337d1cb2ba0 added numeral, which supercedes num, xnum, float;
wenzelm
parents: 28904
diff changeset
   383
fun eq_trfun ((_, s1: stamp), (_, s2)) = s1 = s2;
15754
f867c48de2e1 added stamp_trfun, mk_trfun, eq_trfun;
wenzelm
parents: 15570
diff changeset
   384
240
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   385
15835
fdf678bec567 added tokentrans_mode, standard_token_classes, standard_token_markers (from token_trans.ML);
wenzelm
parents: 15754
diff changeset
   386
(* token translations *)
fdf678bec567 added tokentrans_mode, standard_token_classes, standard_token_markers (from token_trans.ML);
wenzelm
parents: 15754
diff changeset
   387
fdf678bec567 added tokentrans_mode, standard_token_classes, standard_token_markers (from token_trans.ML);
wenzelm
parents: 15754
diff changeset
   388
fun tokentrans_mode m trs = map (fn (s, f) => (m, s, f)) trs;
fdf678bec567 added tokentrans_mode, standard_token_classes, standard_token_markers (from token_trans.ML);
wenzelm
parents: 15754
diff changeset
   389
fdf678bec567 added tokentrans_mode, standard_token_classes, standard_token_markers (from token_trans.ML);
wenzelm
parents: 15754
diff changeset
   390
val standard_token_classes =
35429
afa8cf9e63d8 authentic syntax for classes and type constructors;
wenzelm
parents: 35390
diff changeset
   391
  ["tfree", "tvar", "free", "bound", "var", "numeral", "inner_string"];
15835
fdf678bec567 added tokentrans_mode, standard_token_classes, standard_token_markers (from token_trans.ML);
wenzelm
parents: 15754
diff changeset
   392
fdf678bec567 added tokentrans_mode, standard_token_classes, standard_token_markers (from token_trans.ML);
wenzelm
parents: 15754
diff changeset
   393
val standard_token_markers = map (fn s => "_" ^ s) standard_token_classes;
fdf678bec567 added tokentrans_mode, standard_token_classes, standard_token_markers (from token_trans.ML);
wenzelm
parents: 15754
diff changeset
   394
fdf678bec567 added tokentrans_mode, standard_token_classes, standard_token_markers (from token_trans.ML);
wenzelm
parents: 15754
diff changeset
   395
764
b60e77395d1a changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents: 624
diff changeset
   396
(* pure_ext *)
240
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   397
14903
d264b8ad3eec removed separate logtypes field of syntax;
wenzelm
parents: 14819
diff changeset
   398
val pure_ext = syn_ext' false (K false)
764
b60e77395d1a changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents: 624
diff changeset
   399
  [Mfix ("_", spropT --> propT, "", [0], 0),
b60e77395d1a changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents: 624
diff changeset
   400
   Mfix ("_", logicT --> anyT, "", [0], 0),
b60e77395d1a changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents: 624
diff changeset
   401
   Mfix ("_", spropT --> anyT, "", [0], 0),
b60e77395d1a changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents: 624
diff changeset
   402
   Mfix ("'(_')", logicT --> logicT, "", [0], max_pri),
b60e77395d1a changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents: 624
diff changeset
   403
   Mfix ("'(_')", spropT --> spropT, "", [0], max_pri),
b60e77395d1a changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents: 624
diff changeset
   404
   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
   405
   Mfix ("_::_",  [spropT, typeT] ---> spropT, "_constrain", [4, 0], 3)]
35110
dc4f61a7918a treat inner token markers as syntax consts;
wenzelm
parents: 33317
diff changeset
   406
  standard_token_markers
764
b60e77395d1a changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents: 624
diff changeset
   407
  ([], [], [], [])
2694
b98365c6e869 added token_translation interface;
wenzelm
parents: 2382
diff changeset
   408
  []
764
b60e77395d1a changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents: 624
diff changeset
   409
  ([], []);
240
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   410
8b2a8c52242d contains remaining parts of xgram.ML and extension.ML;
wenzelm
parents:
diff changeset
   411
end;