(* $Header: /users/lal/black/hol/Disser/RCS/c2holParse.sml,v 1.11 1997/02/12 22:45:20 black Exp black $ *)
(* *created  "Mon Nov 18 14:51:31 1996" *by "Paul E. Black" *)
(* *modified "Mon Dec  8 08:21:14 1997" *by "Paul E. Black" *)

(*---------------------------------------------------------------------------
	     Recursive descent parser functions for C to HOL90 AST
 ---------------------------------------------------------------------------*)

(**** code adapted from Chapter 9 of

  ML for the Working Programmer, 2nd edition
  by Lawrence C. Paulson, Computer Laboratory, University of Cambridge.
  (Cambridge University Press, 1996)

****)

(* Infix directives: made globally *)
infix 6 $++;
infix 5 ++;
infix 5 ++$;
infix 3 >>;
infix 0 ||;

exception SyntaxErr of string;

(*---------------------------------------------------------------------------
		      parse tracing functions
 ---------------------------------------------------------------------------*)

val traceParse = ref false;
val indentLevels = ref 0;

fun popLevel () = if !indentLevels > 0 then
			indentLevels := !indentLevels - 1
		  else raise Fail "popping from trace level 0" and
    pushLevel () = indentLevels :=  !indentLevels + 1;


local
fun spaces 0 = ()
  | spaces n = (print " "; spaces (n-1));

fun reallyReport (lbl:string) (a:string) =
    (spaces (!indentLevels); print lbl; print a; print "\n")
in
    fun report (msg, a) = if !traceParse then reallyReport msg a else ()
end;

  (* Phrase consisting of an identifier *)
  fun id (Id a :: toks) = (report("Id: ", a);
			   (a,toks))
    | id _ = (report("Seeking Id", ""); raise SyntaxErr "Identifier expected");

  (* Phrase consisting of an integer *)
  fun num (Integer a :: toks) = (report("Int: ", a);
				 (a,toks))
    | num _ = (report("Seeking Int", ""); raise SyntaxErr "Integer expected");

  (* Phrase consisting of the keyword "kw" *)
  fun $ kw (Key b :: toks) = if kw=b then (report("Key: ", b); (kw,toks))
			     else (report("Didn't find ", kw);
						raise SyntaxErr kw)
    | $ kw _ = (report("Didn't find Key ", kw);
					raise SyntaxErr "Keyword expected");

  (* Alternative phrases *)
  fun (ph1 || ph2) toks = ph1 toks 
			  handle SyntaxErr _ => (report("||", ""); ph2 toks);

  (* abort if ph has a syntax error *)
  fun !! ph toks = ph toks
      handle SyntaxErr msg => raise Fail ("Syntax error: " ^ msg);

  (* One phrase then another *)
  fun (ph1 ++ ph2) toks = 
      let val (x,toks2) = ph1 toks
	  val (y,toks3) = (report("++", "");
			   (ph2 toks2 handle SyntaxErr a => raise SyntaxErr a))
      in ((x,y), toks3)  end;

  (* Application of f to the result of a phrase *)
  fun (ph>>f) toks = 
      let val (x,toks2) = ph toks
      in  (f x, toks2)  end;

  (* keyword then phrase, and only leave the result of ph. *)
  fun (a $++ ph) = ($ a ++ ph >> #2);

  (* phrase then keyword, leaving only the result of ph. *)
  fun (ph ++$ a) = (ph ++ $ a >> #1);

  (* The empty phrase! *)
  fun empty toks = (report("empty", ""); ([],toks));

  (* Zero or more phrases *)
  fun repeat ph toks = (ph ++ repeat ph >> (op::)
                        || empty) toks;

  fun infixes (ph,prec_of,apply) = 
    let fun over k toks = next k (ph toks)
        and next k (x, Key(a)::toks) = 
              if prec_of a < k then (x, Key a :: toks)
              else next k ((over (prec_of a) >> apply a x) toks)
          | next k (x, toks) = (x, toks)
    in  over 0  end;

val numUpcomingToks = ref 7;

(* print the next few tokens *)
local
fun token2str (String s) = "\"" ^ s ^ "\"" |
    token2str (CharConst c) = "'" ^ c ^ "'" |
    token2str (Id i) = i |
    token2str (Integer i) = i |
    token2str (Key k) = k |
    token2str (ErrUnk e) = e;

fun upc toks n =
    if length toks < 1 then (* nothing more *)
	""
    else if n > 0 then
	token2str (hd toks) ^ " " ^ upc (tl toks) (n-1)
    else (* more tokens, but stop here *)
	"..."
in
fun upcoming toks = upc toks (!numUpcomingToks)
end;

(* remember the furthest we got in the tokens.  If something fails to
   parse, the problem is often at or close to this point. *)
val fewestRemaining = ref 0;
val remainingToks = ref ([]:tokenType list);

(* report when entering and leaving productions *)
fun @@ (nm:string) ph toks =
    if !traceParse then (
	report("Entering '", nm ^ "' with " ^ upcoming toks); pushLevel();
	if length toks < (!fewestRemaining) then
	    (fewestRemaining := length toks;
	     remainingToks := toks)
	else
	    ();
	let val r = ph toks handle SyntaxErr a => (
		popLevel(); report("phrase failed ", nm); raise SyntaxErr a) in
	    popLevel(); report("Done with ", nm);
	    r
	end
    ) else
	ph toks;

(* Scan and parse, checking that no tokens remain *)
fun reader ph a = 
    (indentLevels := 0;
     fewestRemaining := 999999999;
     case ph (scan a) of 
	 (x, []) => x |
	 (_, _::_) => raise SyntaxErr "Extra characters in phrase");

(* end of $Source: /users/lal/black/hol/Disser/RCS/c2holParse.sml,v $ *)