src/Pure/Syntax/earley0A.ML
author wenzelm
Mon, 09 Nov 1998 15:42:08 +0100
changeset 5840 e2d2b896c717
parent 330 2fda15dd1e0f
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/earley0A.ML
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     3
    Author:     Tobias Nipkow
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
     5
WARNING: This file is about to disappear.
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 PARSER =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     9
sig
237
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
    10
  structure Lexicon: LEXICON
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
    11
  structure SynExt: SYN_EXT
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
    12
  local open Lexicon SynExt SynExt.Ast in
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    13
    type gram
237
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
    14
    val empty_gram: gram
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
    15
    val extend_gram: gram -> string list -> xprod list -> gram
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
    16
    val merge_grams: gram -> gram -> gram
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
    17
    val pretty_gram: gram -> Pretty.T list
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
    18
    datatype parsetree =
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
    19
      Node of string * parsetree list |
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
    20
      Tip of token
330
2fda15dd1e0f changed the way a grammar is generated to allow the new parser to work;
clasohm
parents: 258
diff changeset
    21
    val parse: gram -> string -> token list -> parsetree list
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    22
  end
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    23
end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    24
237
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
    25
functor EarleyFun(structure Symtab: SYMTAB and Lexicon: LEXICON
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
    26
  and SynExt: SYN_EXT)(*: PARSER *) =  (* FIXME *)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    27
struct
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    28
237
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
    29
structure Pretty = SynExt.Ast.Pretty;
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
    30
structure Lexicon = Lexicon;
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
    31
structure SynExt = SynExt;
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
    32
open Lexicon;
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    33
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    34
237
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
    35
(** datatype parsetree **)
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
    36
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
    37
datatype parsetree =
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
    38
  Node of string * parsetree list |
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
    39
  Tip of token;
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    40
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    41
fun mk_pt ("", [pt]) = pt
237
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
    42
  | mk_pt ("", _) = sys_error "mk_pt: funny copy op in parse tree"
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    43
  | mk_pt (s, ptl) = Node (s, ptl);
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    44
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
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    47
(** token maps (from lexicon.ML) **)
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    48
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    49
type 'b TokenMap = (token * 'b list) list * 'b list;
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    50
val first_token = 0;
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    51
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    52
fun int_of_token(Token(tk)) = first_token |
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    53
    int_of_token(IdentSy _) = first_token - 1 |
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    54
    int_of_token(VarSy _) = first_token - 2 |
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    55
    int_of_token(TFreeSy _) = first_token - 3 |
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    56
    int_of_token(TVarSy _) = first_token - 4 |
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    57
    int_of_token(EndToken) = first_token - 5;
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    58
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    59
fun lesstk(s, t) = int_of_token(s) < int_of_token(t) orelse
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    60
                  (case (s, t) of (Token(a), Token(b)) => a<b | _ => false);
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    61
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    62
fun mkTokenMap(atll) =
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    63
    let val aill = atll;
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    64
        val dom = sort lesstk (distinct(flat(map snd aill)));
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    65
        val mt = map fst (filter (null o snd) atll);
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    66
        fun mktm(i) =
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    67
            let fun add(l, (a, il)) = if i mem il then a::l else l
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    68
            in (i, foldl add ([], aill)) end;
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    69
    in (map mktm dom, mt) end;
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    70
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    71
fun find_al (i) =
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    72
    let fun find((j, al)::l) = if lesstk(i, j) then [] else
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    73
                              if matching_tokens(i, j) then al else find l |
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    74
            find [] = [];
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    75
    in find end;
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    76
fun applyTokenMap((l, mt), tk:token) = mt@(find_al tk l);
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    77
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    78
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    79
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    80
(* Linked lists: *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    81
infix 5 &;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    82
datatype 'a LList = nilL | op & of 'a * ('a LListR)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    83
withtype 'a LListR = 'a LList ref;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    84
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    85
(* Apply proc to all elements in a linked list *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    86
fun seqll (proc: '_a -> unit) : ('_a LListR -> unit) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    87
    let fun seq (ref nilL) = () |
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    88
            seq (ref((a:'_a)&l)) = (proc a; seq l)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    89
    in seq end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    90
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    91
fun llist_to_list (ref nilL) = [] |
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    92
    llist_to_list (ref(a&ll)) = a::(llist_to_list ll);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    93
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    94
val len = length;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    95
237
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
    96
local open Array SynExt in
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    97
nonfix sub;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    98
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    99
fun forA(p: int -> unit, a: 'a array) : unit =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   100
    let val ub = length a
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   101
        fun step(i) = if i=ub then () else (p(i); step(i+1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   102
    in step 0 end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   103
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   104
fun itA(a0:'a, b: 'b array)(f:'a * 'b -> 'a) : 'a =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   105
    let val ub = length b
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   106
        fun acc(a,i) = if i=ub then a else acc(f(a,sub(b,i)),i+1)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   107
    in acc(a0,0) end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   108
237
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   109
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   110
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   111
(** grammars **)
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   112
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   113
datatype 'a symb =
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   114
  Dlm of 'a |
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   115
  Arg of string * int;
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   116
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   117
datatype 'a prod = Prod of string * 'a symb list * string * int;
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   118
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   119
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   120
datatype Symbol = T of token | NT of int * int
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   121
     and Op = Op of OpSyn * string * int
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   122
withtype OpSyn = Symbol array
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   123
     and OpListA = Op array * int TokenMap
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   124
     and FastAcc = int TokenMap;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   125
237
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   126
(*gram_tabs: name of nt -> number, nt number -> productions array,
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   127
  nt number -> list of nt's reachable via copy ops*)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   128
237
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   129
type gram_tabs = int Symtab.table * OpListA array * int list array;
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   130
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   131
type gram = string list * string prod list * gram_tabs;
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   132
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   133
237
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   134
fun non_term (Arg (s, _)) = if is_terminal s then None else Some s
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   135
  | non_term _ = None;
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   136
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   137
fun non_terms (Prod (_, symbs, _, _)) = mapfilter non_term symbs;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   138
237
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   139
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   140
(* mk_pre_grammar *)
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   141
(* converts a list of productions in external format into an
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   142
   internal gram object. *)
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   143
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   144
val dummyTM:FastAcc = mkTokenMap[];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   145
237
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   146
fun mk_pre_grammar prods : gram_tabs =
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   147
  let
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   148
    fun same_res (Prod(t1, _, _, _), Prod(t2, _, _, _)) = t1=t2;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   149
    val partitioned0 = partition_eq same_res prods;
237
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   150
    val nts0 = map (fn Prod(ty, _, _, _)::_ => ty) partitioned0;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   151
    val nts' = distinct(flat(map non_terms prods)) \\ nts0;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   152
    val nts = nts' @ nts0;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   153
    val partitioned = (replicate (len nts') []) @ partitioned0;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   154
    val ntis = nts ~~ (0 upto (len(nts)-1));
237
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   155
    val tab = foldr Symtab.update (ntis, Symtab.null);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   156
237
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   157
    fun nt_or_vt (s, p) =
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   158
      (case predef_term s of
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   159
        None => NT (the (Symtab.lookup (tab, s)), p)
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   160
      | Some tk => T tk);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   161
237
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   162
    fun mksyn(Dlm(t)) = T(t)
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   163
      | mksyn(Arg(t)) = nt_or_vt t;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   164
237
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   165
    fun prod2op(Prod(nt, sy, opn, p)) =
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   166
        let val syA = arrayoflist(map mksyn sy) in Op(syA, opn, p) end;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   167
237
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   168
    fun mkops prods = (arrayoflist(map prod2op prods), dummyTM);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   169
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   170
    val opLA = arrayoflist(map mkops partitioned);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   171
237
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   172
    val subs = array(length opLA, []) : int list array;
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   173
    fun newcp v (a, Op(syA, _, p)) =
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   174
        if p=chain_pri
237
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   175
        then let val NT(k, _) = sub(syA, 0)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   176
             in if k mem v then a else k ins a end
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   177
        else a;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   178
    fun reach v i =
237
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   179
        let val new = itA ([], #1(sub(opLA, i))) (newcp v)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   180
            val v' = new union v
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   181
        in flat(map (reach v') new) union v' end;
237
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   182
    fun rch(i) = update(subs, i, reach[i]i);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   183
237
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   184
  in
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   185
    forA(rch, subs); (tab, opLA, subs)
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   186
  end;
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   187
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   188
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   189
val RootPref = "__";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   190
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   191
(* Lookahead tables for speeding up parsing. Lkhd is a mapping from
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   192
nonterminals (in the form of OpList) to sets (lists) of token strings *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   193
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   194
type Lkhd = token list list list;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   195
237
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   196
(* subst_syn(s, k) syn = [ pref k ts | ts is a token string derivable from sy
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   197
                                      under substitution s ] *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   198
(* This is the general version.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   199
fun cross l1 l2 = flat(map (fn e2 => (map (fn e1 => e1@e2) l1)) l2);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   200
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   201
(* pref k [x1,...,xn] is [x1,...,xk] if 0<=k<=n and [x1,...,xn] otherwise *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   202
fun pref 0 l = []
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   203
  | pref _ [] = []
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   204
  | pref k (e::l) = e::(pref (k-1) l);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   205
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   206
fun subst_syn(s:Lkhd,k) =
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   207
    let fun subst(ref(symb & syn)):token list list =
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   208
              let val l1 = case symb of T t => [[t]] |
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   209
                         NT(oplr,_) => let val Some l = assoc(s,!oplr) in l end
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   210
              in distinct(map (pref k) (cross l1 (subst syn))) end |
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   211
            subst _ = [[]]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   212
    in subst end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   213
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   214
(* This one is specialized to lookahead 1 and a bit too generous *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   215
fun subst_syn(s:Lkhd,1) syA =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   216
    let fun subst i = if i = length(syA) then [[]] else
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   217
              case sub(syA,i) of
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   218
                NT(j,_) => let val pre = nth_elem(j,s)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   219
                         in if [] mem pre then (pre \ []) union subst(i+1)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   220
                            else pre end |
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   221
               T(tk) => [[tk]];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   222
    in subst 0 end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   223
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   224
(* mk_lkhd(G,k) returns a table which associates with every nonterminal N in
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   225
G the list of pref k s for all token strings s with N -G->* s *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   226
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   227
fun mk_lkhd(opLA:OpListA array,k:int):Lkhd =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   228
    let fun step(s:Lkhd):Lkhd =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   229
            let fun subst_op(l,Op(sy,_,_)) = subst_syn(s,k)sy union l;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   230
                fun step2(l,(opA,_)) = l@[itA([],opA)subst_op];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   231
            in writeln"."; itA([],opLA)step2 end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   232
        fun iterate(s:Lkhd):Lkhd = let val s' = step s
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   233
              in if map len s = map len s' then s
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   234
                 else iterate s' end
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   235
    in writeln"Computing lookahead tables ...";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   236
       iterate (replicate (length opLA) []) end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   237
237
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   238
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   239
(* mk_earley_gram *)       (* create look ahead tables *)
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   240
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   241
fun mk_earley_gram (g as (tab, opLA, _):gram_tabs):gram_tabs =
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   242
    let val lkhd = mk_lkhd(opLA, 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   243
        fun mk_fa(i):FastAcc =
237
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   244
            let val opA = #1(sub(opLA, i));
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   245
                fun start(j) = let val Op(sy, _, _) = sub(opA, j);
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   246
                                   val pre = subst_syn(lkhd, 1) sy
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   247
                        in (j, if [] mem pre then [] else map hd pre) end;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   248
            in mkTokenMap(map start (0 upto(length(opA)-1))) end;
237
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   249
        fun updt(i) = update(opLA, i, (#1(sub(opLA, i)), mk_fa(i)));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   250
237
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   251
    in forA(updt, opLA); g end;
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   252
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   253
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   254
(* compile_xgram *)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   255
237
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   256
fun compile_xgram (roots, prods) =
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   257
  let
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   258
    fun mk_root nt =
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   259
      Prod (RootPref ^ nt, [Arg (nt, 0), Dlm EndToken], "", 0);
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   260
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   261
    val prods' = (map mk_root roots) @ prods;
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   262
  in
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   263
    mk_earley_gram (mk_pre_grammar prods')
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   264
  end;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   265
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   266
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   267
(* translate (from xgram.ML) *)
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   268
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   269
fun translate trfn =
237
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   270
  map (fn Dlm t => Dlm (trfn t) | Arg s => Arg s);
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   271
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   272
237
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   273
(* mk_gram_tabs *)
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   274
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   275
fun str_to_tok (opl: string prod list): token prod list =
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   276
  map
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   277
    (fn Prod (t, syn, s, pa) => Prod (t, translate Token syn, s, pa))
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   278
    opl;
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   279
237
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   280
fun mk_gram_tabs roots prods = compile_xgram (roots, str_to_tok prods);
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   281
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   282
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   283
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   284
(** build gram **)
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   285
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   286
fun mk_gram roots prods = (roots, prods, mk_gram_tabs roots prods);
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   287
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   288
fun sub_gram (roots1, prods1, _) (roots2, prods2, _) =
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   289
  roots1 subset roots2 andalso prods1 subset prods2;
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   290
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   291
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   292
(* empty, extend, merge grams *)
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   293
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   294
val empty_gram = mk_gram [] [];
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   295
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   296
fun extend_gram (gram1 as (roots1, prods1, _)) roots2 xprods2 =
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   297
  let
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   298
    fun symb_of (Delim s) = Some (Dlm s)
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   299
      | symb_of (Argument s_p) = Some (Arg s_p)
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   300
      | symb_of _ = None;
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   301
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   302
    fun prod_of (XProd (lhs, xsymbs, const, pri)) =
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   303
      Prod (lhs, mapfilter symb_of xsymbs, const, pri);
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   304
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   305
    val prods2 = distinct (map prod_of xprods2);
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   306
  in
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   307
    if roots2 subset roots1 andalso prods2 subset prods1 then gram1
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   308
    else mk_gram (extend_list roots1 roots2) (extend_list prods1 prods2)
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   309
  end;
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   310
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   311
fun merge_grams (gram1 as (roots1, prods1, _)) (gram2 as (roots2, prods2, _)) =
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   312
  if sub_gram gram2 gram1 then gram1
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   313
  else if sub_gram gram1 gram2 then gram2
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   314
  else mk_gram (merge_lists roots1 roots2) (merge_lists prods1 prods2);
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   315
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   316
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   317
(* pretty_gram *)
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   318
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   319
fun pretty_gram (_, prods, _) =
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   320
  let
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   321
    fun pretty_name name = [Pretty.str (name ^ " =")];
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   322
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   323
    fun pretty_symb (Dlm s) = Pretty.str (quote s)
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   324
      | pretty_symb (Arg (s, p)) =
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   325
          if is_terminal s then Pretty.str s
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   326
          else Pretty.str (s ^ "[" ^ string_of_int p ^ "]");
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   327
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   328
    fun pretty_const "" = []
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   329
      | pretty_const c = [Pretty.str ("=> " ^ quote c)];
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   330
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   331
    fun pretty_pri p = [Pretty.str ("(" ^ string_of_int p ^ ")")];
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   332
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   333
    fun pretty_prod (Prod (name, symbs, const, pri)) =
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   334
      Pretty.block (Pretty.breaks (pretty_name name @
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   335
        map pretty_symb symbs @ pretty_const const @ pretty_pri pri));
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   336
  in
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   337
    map pretty_prod prods
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   338
  end;
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   339
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   340
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   341
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   342
(* State: nonterminal#, production#, index in production,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   343
          index of originating state set,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   344
          parse trees generated so far,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   345
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   346
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   347
datatype State = St of int * int * int * int * parsetree list
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   348
withtype StateSet  = State LListR * (State -> unit) LListR;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   349
type Compl = State -> unit;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   350
type StateSetList = StateSet array;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   351
(* Debugging:
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   352
val print_SL = seqll(fn St(nti,pi,ip,fs,ptl)=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   353
(print_int nti; prs" "; print_int pi; prs" "; print_int ip; prs" ";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   354
print_int fs; prs" "; print_int(len ptl); prs"\n"));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   355
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   356
fun print_SS(s1,delr) = (writeln"================="; print_SL s1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   357
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   358
fun count_ss(ref nilL) = 0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   359
  | count_ss(ref(_ & ss)) = count_ss(ss)+1;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   360
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   361
fun print_stat(state_sets) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   362
    let fun pr i = let val(s1,_)=sub(state_sets,i)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   363
                in prs" "; print_int(count_ss s1) end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   364
    in prs"["; forA(pr,state_sets); prs"]\n" end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   365
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   366
fun mt_stateS():StateSet = (ref nilL, ref nilL);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   367
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   368
fun mt_states(n):StateSetList = array(n,mt_stateS());
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   369
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   370
fun ismt_stateS((ref nilL,_):StateSet) = true | ismt_stateS _ = false;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   371
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   372
fun fst_state((ref(st & _),_): StateSet) = st;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   373
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   374
fun apply_all_states(f,(slr,_):StateSet) = seqll f slr;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   375
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   376
fun add_state(nti,pi,ip,from,ptl,(sllr,delr):StateSet) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   377
      let fun add(ref(St(nti',pi',ip',from',_) & rest)) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   378
                if nti=nti' andalso pi=pi' andalso ip=ip' andalso from=from'
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   379
                then ()
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   380
                else add rest |
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   381
              add(last as ref nilL) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   382
                let val newst = St(nti,pi,ip,from,ptl)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   383
                in last := newst & ref nilL;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   384
                   seqll (fn compl => compl newst) delr
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   385
                end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   386
      in add sllr end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   387
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   388
fun complete(nti,syA,opn,p,ptl,ss,si as (_,delr):StateSet,opLA,rchA) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   389
      let val pt = mk_pt(opn,ptl)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   390
          fun compl(St(ntj,pj,jp,from,ptl)) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   391
                let val Op(syj,_,_) = sub(fst(sub(opLA,ntj)),pj) in
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   392
                if jp=length(syj) then () else
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   393
                case sub(syj,jp) of
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   394
                  NT(nt,p') => if p >= p' andalso nti mem sub(rchA,nt)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   395
                        then add_state(ntj,pj,jp+1,from,ptl@[pt], si)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   396
                        else ()
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   397
                | _ => ()
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   398
                end
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   399
      in apply_all_states(compl,ss);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   400
         if length(syA)=0 (* delayed completion in case of empty production: *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   401
         then delr := compl & ref(!delr) else ()
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   402
      end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   403
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   404
fun predict(tk,isi,si,p',opLA) = fn nti =>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   405
    let val (opA,tm) = sub(opLA,nti);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   406
        fun add(pi) = let val opr as Op(syA,_,p) = sub(opA,pi)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   407
                in if p < p' then () else add_state(nti,pi,0,isi,[],si) end
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   408
    in seq add (applyTokenMap(tm,tk)) end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   409
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   410
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   411
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   412
fun unknown c = error ("Unparsable category: " ^ c);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   413
237
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   414
fun syn_err toks =
258
e540b7d4ecb1 minor internal changes;
wenzelm
parents: 237
diff changeset
   415
  error ("Syntax error at: " ^ quote (space_implode " " (map str_of_token toks)));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   416
330
2fda15dd1e0f changed the way a grammar is generated to allow the new parser to work;
clasohm
parents: 258
diff changeset
   417
fun parse ((_, _, (tab, opLA, rchA)):gram) (root:string) (tl: token list): parsetree list =
237
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   418
  let
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   419
    val tl' = tl;
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   420
    val state_sets = mt_states(len tl' + 1);
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   421
    val s0 = mt_stateS();
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   422
    val rooti = case Symtab.lookup(tab, RootPref^root) of
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   423
            Some(ri) => ri | None => unknown root;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   424
237
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   425
    fun lr (tl, isi, si, t) =
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   426
        if ismt_stateS(si) then syn_err (t::tl) else
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   427
        case tl of
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   428
          [] => () |
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   429
          t::tl =>
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   430
            let val si1 = mt_stateS();
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   431
                fun process(St(nti,pi,ip,from,ptl)) =
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   432
                      let val opA = #1(sub(opLA,nti))
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   433
                          val Op(syA,opn,p) = sub(opA,pi) in
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   434
                    if ip = length(syA)
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   435
                    then complete(nti,syA,opn,p,ptl,
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   436
                                    sub(state_sets,from),si,opLA,rchA)
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   437
                    else case sub(syA,ip) of
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   438
                      NT(ntj,p) =>
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   439
                            seq (predict(t,isi,si,p,opLA)) (sub(rchA,ntj))
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   440
                    | T(t') =>
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   441
                        if matching_tokens(t,t')
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   442
                        then add_state(nti,pi,ip+1,from,
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   443
                                       if valued_token(t)
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   444
                                       then ptl@[Tip(t)] else ptl,
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   445
                                       si1)
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   446
                        else () end;
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   447
237
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   448
        in apply_all_states(process,si);
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   449
           update(state_sets,isi+1,si1);
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   450
           lr(tl,isi+1,si1,t) end
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   451
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   452
  in
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   453
    update (state_sets, 0, s0);
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   454
    add_state (rooti, 0, 0, 0, [], s0);
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   455
    lr (tl', 0, s0, EndToken(*dummy*));
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   456
    (*print_stat state_sets;*)
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   457
    let val St(_, _, _, _, [pt]) = fst_state(sub(state_sets, len tl'))
330
2fda15dd1e0f changed the way a grammar is generated to allow the new parser to work;
clasohm
parents: 258
diff changeset
   458
    in [pt] end
237
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   459
  end;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   460
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   461
end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   462
237
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 18
diff changeset
   463
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   464
end;
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   465