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