added comments
authorclasohm
Mon Jan 15 15:00:14 1996 +0100 (1996-01-15)
changeset 14383cc22794ce71
parent 1437 2ebbc23d49fa
child 1439 1f5949a43e82
added comments
src/Pure/Syntax/parser.ML
     1.1 --- a/src/Pure/Syntax/parser.ML	Mon Jan 15 14:56:38 1996 +0100
     1.2 +++ b/src/Pure/Syntax/parser.ML	Mon Jan 15 15:00:14 1996 +0100
     1.3 @@ -432,12 +432,15 @@
     1.4    in flat (map pretty_nt taglist) end;
     1.5  
     1.6  
     1.7 -(* empty, extend, merge grams *)
     1.8 +(** Operations on gramars **)
     1.9  
    1.10 +(*The mother of all grammars*)
    1.11  val empty_gram = Gram {nt_count = 0, prod_count = 0,
    1.12                         tags = Symtab.null, chains = [], lambdas = [],
    1.13                         prods = Array.array (0, (([], []), []))};
    1.14  
    1.15 +
    1.16 +(*Invert list of chain productions*)
    1.17  fun inverse_chains [] result = result
    1.18    | inverse_chains ((root, branches) :: cs) result =
    1.19      let fun add [] result = result
    1.20 @@ -446,16 +449,22 @@
    1.21              in add ids (overwrite (result, (id, root :: old))) end;
    1.22      in inverse_chains cs (add branches result) end;
    1.23  
    1.24 +
    1.25 +(*Add productions to a grammar*)
    1.26  fun extend_gram gram [] = gram
    1.27    | extend_gram (Gram {nt_count, prod_count, tags, chains, lambdas, prods})
    1.28                  xprods =
    1.29    let
    1.30 +    (*Get tag for existing nonterminal or create a new one*)
    1.31      fun get_tag nt_count tags nt =
    1.32        case Symtab.lookup (tags, nt) of
    1.33          Some tag => (nt_count, tags, tag)
    1.34        | None => (nt_count+1, Symtab.update_new ((nt, nt_count), tags),
    1.35                   nt_count);
    1.36 -  
    1.37 +
    1.38 +    (*Convert symbols to the form used by the parser;
    1.39 +      delimiters and predefined terms are stored as terminals,
    1.40 +      nonterminals are converted to integer tags*)
    1.41      fun symb_of [] nt_count tags result = (nt_count, tags, rev result)
    1.42        | symb_of ((Delim s) :: ss) nt_count tags result =
    1.43            symb_of ss nt_count tags ((Terminal (Token s)) :: result)
    1.44 @@ -471,6 +480,7 @@
    1.45        | symb_of (_ :: ss) nt_count tags result =
    1.46            symb_of ss nt_count tags result;
    1.47  
    1.48 +    (*Convert list of productions by invoking symb_of for each of them*)
    1.49      fun prod_of [] nt_count prod_count tags result =
    1.50            (nt_count, prod_count, tags, result)
    1.51        | prod_of ((XProd (lhs, xsymbs, const, pri)) :: ps)
    1.52 @@ -483,11 +493,14 @@
    1.53                     ((lhs_tag, (prods, const, pri)) :: result)
    1.54          end;
    1.55  
    1.56 -    val (nt_count', prod_count', tags', prods2) =
    1.57 +    val (nt_count', prod_count', tags', xprods') =
    1.58        prod_of xprods nt_count prod_count tags [];
    1.59  
    1.60      val dummy = writeln "Building new grammar...";
    1.61  
    1.62 +    (*Copy array containing productions of old grammar;
    1.63 +      this has to be done to preserve the old grammar while being able
    1.64 +      to change the array's content*)
    1.65      val prods' =
    1.66        let fun get_prod i = if i < nt_count then Array.sub (prods, i)
    1.67                             else (([], []), []);
    1.68 @@ -495,8 +508,9 @@
    1.69  
    1.70      val fromto_chains = inverse_chains chains [];
    1.71  
    1.72 +    (*Add new productions to old ones*)
    1.73      val (fromto_chains', lambdas', _) =
    1.74 -      add_prods prods' fromto_chains lambdas None prods2;
    1.75 +      add_prods prods' fromto_chains lambdas None xprods';
    1.76  
    1.77      val chains' = inverse_chains fromto_chains' [];
    1.78    in Gram {nt_count = nt_count', prod_count = prod_count', tags = tags',
    1.79 @@ -504,6 +518,7 @@
    1.80    end;
    1.81  
    1.82  
    1.83 +(*Merge two grammars*)
    1.84  fun merge_grams gram_a gram_b =
    1.85    let
    1.86      val dummy = writeln "Building new grammar...";
    1.87 @@ -599,7 +614,7 @@
    1.88    end;
    1.89  
    1.90  
    1.91 -(** parse **)
    1.92 +(** Parser **)
    1.93  
    1.94  datatype parsetree =
    1.95    Node of string * parsetree list |