src/Pure/Syntax/parser.ML
changeset 80968 a9e18ab3a625
parent 80965 f74aecc6ef9c
child 80969 667f5072ed2d
equal deleted inserted replaced
80967:980cc422526e 80968:a9e18ab3a625
    81 fun chains_all_preds (chains: chains) = Int_Graph.all_preds chains;
    81 fun chains_all_preds (chains: chains) = Int_Graph.all_preds chains;
    82 fun chains_all_succs (chains: chains) = Int_Graph.all_succs chains;
    82 fun chains_all_succs (chains: chains) = Int_Graph.all_succs chains;
    83 val chains_empty: chains = Int_Graph.empty;
    83 val chains_empty: chains = Int_Graph.empty;
    84 fun chains_member (chains: chains) = Int_Graph.is_edge chains;
    84 fun chains_member (chains: chains) = Int_Graph.is_edge chains;
    85 fun chains_declare nt : chains -> chains = Int_Graph.default_node (nt, ());
    85 fun chains_declare nt : chains -> chains = Int_Graph.default_node (nt, ());
       
    86 
       
    87 fun chains_declares (Terminal _) = I
       
    88   | chains_declares (Nonterminal (nt, _)) = chains_declare nt
       
    89 
    86 fun chains_insert (from, to) =
    90 fun chains_insert (from, to) =
    87   chains_declare from #> chains_declare to #> Int_Graph.add_edge (from, to);
    91   chains_declare from #> chains_declare to #> Int_Graph.add_edge (from, to);
    88 
    92 
    89 datatype gram =
    93 datatype gram =
    90   Gram of
    94   Gram of
   107     SOME tk => tk
   111     SOME tk => tk
   108   | NONE => unknown_start);
   112   | NONE => unknown_start);
   109 
   113 
   110 fun add_production array_prods (lhs, new_prod as (rhs, _, pri)) (chains, lambdas) =
   114 fun add_production array_prods (lhs, new_prod as (rhs, _, pri)) (chains, lambdas) =
   111   let
   115   let
   112     (*store chain if it does not already exist*)
       
   113     val (chain, new_chain, chains') =
   116     val (chain, new_chain, chains') =
   114       (case (pri, rhs) of
   117       (case (pri, rhs) of
   115         (~1, [Nonterminal (from, ~1)]) =>
   118         (~1, [Nonterminal (from, ~1)]) =>
   116           if chains_member chains (from, lhs)
   119           if chains_member chains (from, lhs)
   117           then (SOME from, false, chains)
   120           then (SOME from, false, chains)
   118           else (SOME from, true, chains_insert (from, lhs) chains)
   121           else (SOME from, true, chains_insert (from, lhs) chains)
   119       | _ =>
   122       | _ => (NONE, false, chains |> chains_declare lhs |> fold chains_declares rhs));
   120         let
       
   121           val chains' = chains
       
   122             |> chains_declare lhs
       
   123             |> fold (fn Nonterminal (nt, _) => chains_declare nt | _ => I) rhs;
       
   124         in (NONE, false, chains') end);
       
   125 
   123 
   126     (*propagate new chain in lookahead and lambdas;
   124     (*propagate new chain in lookahead and lambdas;
   127       added_starts is used later to associate existing
   125       added_starts is used later to associate existing
   128       productions with new starting tokens*)
   126       productions with new starting tokens*)
   129     val (added_starts, lambdas') =
   127     val (added_starts, lambdas') =