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