src/Pure/Syntax/parser.ML
changeset 377 ab8917806779
parent 373 68400ea32f7b
child 395 712dceb1ecc7
     1.1 --- a/src/Pure/Syntax/parser.ML	Wed May 18 15:24:39 1994 +0200
     1.2 +++ b/src/Pure/Syntax/parser.ML	Thu May 19 13:13:27 1994 +0200
     1.3 @@ -178,27 +178,29 @@
     1.4  
     1.5        (*list all terminals that can start the given rhss*)
     1.6        fun look_rhss starts rhss_ref =
     1.7 -        let fun look [] _ = []
     1.8 -              | look ((symbs, _, _) :: todos) done =
     1.9 +        let fun look [] _ result = result
    1.10 +              | look ((symbs, _, _) :: todos) done result =
    1.11                    let val (start_token, skipped) = rhss_start symbs [];
    1.12  
    1.13                        (*process all nonterminals on which the lookahead
    1.14                          depends and build the new todo and done lists for
    1.15                          the look function*)
    1.16 -                      fun look2 [] todos = look todos (done union skipped)
    1.17 -                        | look2 (rhss_ref :: ls) todos =
    1.18 -                            if rhss_ref mem done then look2 ls todos
    1.19 +                      fun look2 [] todos result = 
    1.20 +                            look todos (done union skipped) result
    1.21 +                        | look2 (rhss_ref :: ls) todos result =
    1.22 +                            if rhss_ref mem done then look2 ls todos result
    1.23                              else case assoc (starts, rhss_ref) of
    1.24 -                                Some tks => tks union (look2 ls todos)
    1.25 -                              | None => let val (_, rhss) = hd (!rhss_ref);
    1.26 -                                        in look2 ls (rhss union todos) end;
    1.27 +                                Some tks => look2 ls todos (tks union result)
    1.28 +                              | None => 
    1.29 +                                  let val (_, rhss) = hd (!rhss_ref);
    1.30 +                                  in look2 ls (rhss @ todos) result end;
    1.31                    in case start_token of
    1.32 -                         Some tk => start_token ins (look2 skipped todos)
    1.33 -                       | None => look2 skipped todos
    1.34 +                         Some tk => look2 skipped todos (start_token ins result)
    1.35 +                       | None => look2 skipped todos result
    1.36                    end;
    1.37   
    1.38              val (_, rhss) = hd (!rhss_ref);
    1.39 -        in look rhss [rhss_ref] end;                       
    1.40 +        in look rhss [rhss_ref] [] end;                       
    1.41  
    1.42        (*make a table that contains all possible starting terminals
    1.43          for each nonterminal*)
    1.44 @@ -210,14 +212,20 @@
    1.45  
    1.46        (*add list of allowed starting tokens to productions*)
    1.47        fun mk_lookahead (_, rhss_ref) =
    1.48 -        let (*add item to lookahead list (a list containing pairs of token and 
    1.49 -              rhss that can be started with it*)
    1.50 +        let (*compares two values of type token option 
    1.51 +              (used for speed reasons)*)
    1.52 +            fun matching_opt_tks (Some tk1, Some tk2) =
    1.53 +                  matching_tokens (tk1, tk2)
    1.54 +              | matching_opt_tks _ = false;
    1.55 +
    1.56 +            (*add item to lookahead list (a list containing pairs of token and 
    1.57 +              rhss that can be started with it)*)
    1.58              fun add_start new_rhs tokens table =
    1.59                    let fun add [] [] = []
    1.60                          | add (tk :: tks) [] =
    1.61                              (tk, [new_rhs]) :: (add tks [])
    1.62                          | add tokens ((tk, rhss) :: ss) =
    1.63 -                            if tk mem tokens then 
    1.64 +                            if gen_mem matching_opt_tks (tk, tokens) then 
    1.65                                (tk, new_rhs :: rhss) :: (add (tokens \ tk) ss)
    1.66                              else
    1.67                                (tk, rhss) :: (add tokens ss);
    1.68 @@ -225,7 +233,7 @@
    1.69  
    1.70              (*combine all lookaheads of a list of nonterminals*)
    1.71              fun combine_starts rhss_refs =
    1.72 -              foldr (op union) 
    1.73 +              foldr (gen_union matching_opt_tks)
    1.74                ((map (fn rhss_ref => let val Some tks = assoc (starts, rhss_ref)
    1.75                                      in tks end) rhss_refs), []);
    1.76  
    1.77 @@ -234,8 +242,8 @@
    1.78                | look_rhss ((rhs as (symbs, id, prec)) :: rs) table =
    1.79                    let val (start_token, skipped) = rhss_start symbs [];
    1.80                        val starts = case start_token of
    1.81 -                                     Some tk => Some tk 
    1.82 -                                                ins (combine_starts skipped)
    1.83 +                                     Some tk => gen_ins matching_opt_tks 
    1.84 +                                             (Some tk, combine_starts skipped)
    1.85                                     | None => if skipped subset lambdas then
    1.86                                                 [None]
    1.87                                               else