1.1 --- a/src/Pure/Syntax/parser.ML Mon Apr 25 11:20:25 1994 +0200
1.2 +++ b/src/Pure/Syntax/parser.ML Tue Apr 26 14:48:41 1994 +0200
1.3 @@ -1,6 +1,6 @@
1.4 (* Title: Pure/Syntax/parser.ML
1.5 ID: $Id$
1.6 - Author: Sonia Mahjoub and Markus Wenzel, TU Muenchen
1.7 + Author: Sonia Mahjoub, Markus Wenzel and Carsten Clasohm, TU Muenchen
1.8
1.9 Isabelle's main parser (used for terms and typs).
1.10
1.11 @@ -102,30 +102,31 @@
1.12 chains @ (list_chain ps)
1.13 end;
1.14
1.15 - (*convert a list of pairs to an association list*)
1.16 - fun compress chains =
1.17 + (*convert a list of pairs to an association list
1.18 + by using the first element as the key*)
1.19 + fun mk_assoc pairs =
1.20 let fun doit [] result = result
1.21 | doit ((id1, id2) :: ps) result =
1.22 doit ps
1.23 (overwrite (result, (id1, id2 :: (assocs result id1))));
1.24 - in doit chains [] end;
1.25 + in doit pairs [] end;
1.26
1.27 (*replace reference by list of rhss in chain pairs*)
1.28 - fun unref (id1, ids) =
1.29 - let fun unref1 [] = []
1.30 - | unref1 (id :: ids) =
1.31 + fun deref (id1, ids) =
1.32 + let fun deref1 [] = []
1.33 + | deref1 (id :: ids) =
1.34 let val (_, rhss) = hd (!id);
1.35 - in rhss @ (unref1 ids) end;
1.36 - in (id1, unref1 ids) end;
1.37 + in rhss @ (deref1 ids) end;
1.38 + in (id1, deref1 ids) end;
1.39
1.40 val chain_pairs =
1.41 - map unref (transitive_closure (compress (list_chain ref_gram)));
1.42 + map deref (transitive_closure (mk_assoc (list_chain ref_gram)));
1.43
1.44 (*add new rhss to productions*)
1.45 - fun mk_chain (rhss_ref, rhss) =
1.46 + fun elim (rhss_ref, rhss) =
1.47 let val (dummy, old_rhss) = hd (!rhss_ref);
1.48 in rhss_ref := [(dummy, old_rhss @ rhss)] end;
1.49 - in map mk_chain chain_pairs;
1.50 + in map elim chain_pairs;
1.51 ref_gram
1.52 end;
1.53
1.54 @@ -139,10 +140,10 @@
1.55 if rhss_ref mem result then
1.56 lambda nts result
1.57 else
1.58 - let (*test if a list of rhss contains a production
1.59 - consisting only of lambda NTs*)
1.60 - fun only_lambdas _ [] = []
1.61 - | only_lambdas result ((_, rhss_ref) :: ps) =
1.62 + let (*list all NTs that can be produced by a rhs
1.63 + containing only lambda NTs*)
1.64 + fun only_lambdas [] result = result
1.65 + | only_lambdas ((_, rhss_ref) :: ps) result =
1.66 let fun only (symbs, _, _) =
1.67 forall (fn (Nonterm (id, _)) => id mem result
1.68 | (Term _) => false) symbs;
1.69 @@ -150,25 +151,15 @@
1.70 val (_, rhss) = hd (!rhss_ref);
1.71 in if not (rhss_ref mem result) andalso
1.72 exists only rhss then
1.73 - rhss_ref :: (only_lambdas result ps)
1.74 + only_lambdas ref_gram (rhss_ref :: result)
1.75 else
1.76 - only_lambdas result ps
1.77 - end;
1.78 -
1.79 - (*search for NTs that can be produced by a list of
1.80 - lambda NTs*)
1.81 - fun produced_by [] result = result
1.82 - | produced_by (rhss_ref :: rhss_refs) result =
1.83 - let val new_lambdas =
1.84 - only_lambdas result ref_gram;
1.85 - in produced_by (rhss_refs union new_lambdas)
1.86 - (result @ new_lambdas)
1.87 + only_lambdas ps result
1.88 end;
1.89
1.90 val (_, rhss) = hd (!rhss_ref);
1.91 in if exists (fn (symbs, _, _) => null symbs) rhss
1.92 then lambda nts
1.93 - (produced_by [rhss_ref] (rhss_ref :: result))
1.94 + (only_lambdas ref_gram (rhss_ref :: result))
1.95 else lambda nts result
1.96 end;
1.97 in lambda ref_gram [] end;
1.98 @@ -219,23 +210,23 @@
1.99 (*add list of allowed starting tokens to productions*)
1.100 fun mk_lookahead (_, rhss_ref) =
1.101 let (*add item to lookahead list (a list containing pairs of token and
1.102 - rhss that can be started with this token*)
1.103 - fun add_start _ [] table = table
1.104 - | add_start new_rhs (token :: tks) table =
1.105 - let fun add [] =
1.106 - [(token, [new_rhs])]
1.107 - | add ((tk, rhss) :: ss) =
1.108 - if token = tk then
1.109 - (tk, new_rhs :: rhss) :: ss
1.110 + rhss that can be started with it*)
1.111 + fun add_start new_rhs tokens table =
1.112 + let fun add [] [] = []
1.113 + | add (tk :: tks) [] =
1.114 + (tk, [new_rhs]) :: (add tks [])
1.115 + | add tokens ((tk, rhss) :: ss) =
1.116 + if tk mem tokens then
1.117 + (tk, new_rhs :: rhss) :: (add (tokens \ tk) ss)
1.118 else
1.119 - (tk, rhss) :: (add ss);
1.120 - in add_start new_rhs tks (add table) end;
1.121 + (tk, rhss) :: (add tokens ss);
1.122 + in add tokens table end;
1.123
1.124 (*combine all lookaheads of a list of nonterminals*)
1.125 - fun combine_starts [] = []
1.126 - | combine_starts (rhss_ref :: ps) =
1.127 - let val Some tks = assoc (starts, rhss_ref)
1.128 - in tks union combine_starts ps end;
1.129 + fun combine_starts rhss_refs =
1.130 + foldr (op union)
1.131 + ((map (fn rhss_ref => let val Some tks = assoc (starts, rhss_ref)
1.132 + in tks end) rhss_refs), []);
1.133
1.134 (*get lookahead for a rhs and update lhs' lookahead list*)
1.135 fun look_rhss [] table = table
1.136 @@ -244,9 +235,7 @@
1.137 val starts = case start_token of
1.138 Some tk => Some tk
1.139 ins (combine_starts skipped)
1.140 - | None => if skipped = []
1.141 - orelse forall (fn id => id mem lambdas) skipped then
1.142 - (*lambda production?*)
1.143 + | None => if skipped subset lambdas then
1.144 [None]
1.145 else
1.146 combine_starts skipped;
2.1 --- a/src/Pure/Syntax/syn_ext.ML Mon Apr 25 11:20:25 1994 +0200
2.2 +++ b/src/Pure/Syntax/syn_ext.ML Tue Apr 26 14:48:41 1994 +0200
2.3 @@ -268,14 +268,14 @@
2.4
2.5 fun change_name T ext =
2.6 let val Type (name, ts) = T
2.7 - in Type (space_implode "" [name, ext], ts) end;
2.8 + in Type (implode [name, ext], ts) end;
2.9
2.10 (* Append "_H" to lhs if production is not a copy or chain production *)
2.11 fun hide_xprod roots (XProd (lhs, symbs, const, pri)) =
2.12 let fun is_delim (Delim _) = true
2.13 | is_delim _ = false
2.14 in if const <> "" andalso lhs mem roots andalso exists is_delim symbs then
2.15 - XProd (space_implode "" [lhs, "_H"], symbs, const, pri)
2.16 + XProd (implode [lhs, "_H"], symbs, const, pri)
2.17 else XProd (lhs, symbs, const, pri)
2.18 end;
2.19