src/Pure/Syntax/xgram.ML
author wenzelm
Mon, 09 Nov 1998 15:42:08 +0100
changeset 5840 e2d2b896c717
parent 18 c9ec452ff08f
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/xgram.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 representation (internal interface).
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
TODO:
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
     8
  prod, xsymb: 'a --> string
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
     9
  Terminal --> Literal, Nonterminal --> Argument (?)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
signature XGRAM =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
sig
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    14
  structure Ast: AST
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    15
  local open Ast in
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    16
    datatype 'a xsymb =
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    17
      Terminal of 'a |
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    18
      Nonterminal of string * int |
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    19
      Space of string |
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    20
      Bg of int | Brk of int | En
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    21
    datatype 'a prod = Prod of string * ('a xsymb list) * string * int
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    22
    val max_pri: int
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    23
    val chain_pri: int
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    24
    val literals_of: string prod list -> string list
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    25
    datatype xgram =
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    26
      XGram of {
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    27
        roots: string list,
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    28
        prods: string prod list,
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    29
        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_rules: (ast * ast) list,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    32
        parse_translation: (string * (term list -> term)) list,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    33
        print_translation: (string * (term list -> term)) list,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    34
        print_rules: (ast * ast) list,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    35
        print_ast_translation: (string * (ast list -> ast)) list}
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    36
  end
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    37
end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    38
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    39
functor XGramFun(Ast: AST): XGRAM =
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    40
struct
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    41
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    42
structure Ast = Ast;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    43
open Ast;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    44
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    45
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    46
(** datatype prod **)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    47
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    48
(*Terminal s: literal token s
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    49
  Nonterminal (s, p): nonterminal s requiring priority >= p, or valued token
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    50
  Space s: some white space for printing
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    51
  Bg, Brk, En: blocks and breaks for pretty printing*)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    52
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    53
datatype 'a xsymb =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    54
  Terminal of 'a |
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    55
  Nonterminal of string * int |
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    56
  Space of string |
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    57
  Bg of int | Brk of int | En;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    58
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    59
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    60
(*Prod (lhs, syms, c, p):
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    61
    lhs: name of nonterminal on the lhs of the production
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    62
    syms: list of symbols on the rhs of the production
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    63
    c: head of parse tree
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    64
    p: priority of this production*)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    65
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    66
datatype 'a prod = Prod of string * ('a xsymb list) * string * int;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    67
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    68
val max_pri = 1000;   (*maximum legal priority*)
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    69
val chain_pri = ~1;   (*dummy for chain productions*)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    70
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    71
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    72
(* literals_of *)
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    73
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    74
fun literals_of prods =
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    75
  let
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    76
    fun lits_of (Prod (_, syn, _, _)) =
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    77
      mapfilter (fn Terminal s => Some s | _ => None) syn;
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    78
  in
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    79
    distinct (flat (map lits_of prods))
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    80
  end;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    81
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    82
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    83
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    84
(** datatype xgram **)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    85
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    86
datatype xgram =
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    87
  XGram of {
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    88
    roots: string list,
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    89
    prods: string prod list,
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    90
    consts: string list,
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    91
    parse_ast_translation: (string * (ast list -> ast)) list,
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    92
    parse_rules: (ast * ast) list,
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    93
    parse_translation: (string * (term list -> term)) list,
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    94
    print_translation: (string * (term list -> term)) list,
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    95
    print_rules: (ast * ast) list,
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    96
    print_ast_translation: (string * (ast list -> ast)) list};
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    97
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    98
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    99
end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   100