(* pl2gastex main loop.
   Copyright (C) 2004,2005 Jean Goubault-Larrecq and LSV, CNRS UMR 8643 & ENS Cachan.

   This file is part of h1.

   h1 is free software; you can redistribute it and/or modify
   it under the terms of the GNU General Public License as published by
   the Free Software Foundation; either version 2, or (at your option)
   any later version.

   h1 is distributed in the hope that it will be useful,
   but WITHOUT ANY WARRANTY; without even the implied warranty of
   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
   GNU General Public License for more details.

   You should have received a copy of the GNU General Public License
   along with h1; see the file COPYING.  If not, write to
   the Free Software Foundation, 675 Mass Ave, Cambridge, MA 02139, USA.
*)

open "plauto_h";
open "intersym_h";
open "sort_h";
open "gensym_h";
open "yyerror_h";

val version = "1.1 - Feb 28, 2007"; (* "1.0 - Dec 29, 2004";*)

exception TransitionShouldBeUnary of string * string;

fun alpha n = (* enumerate a, b, c, ..., z, aa, ab, ac, ..., az, ba, bb, ... *)
    if n=0
	then ""
    else let val (q, r) = (n-1) divmod 26
	 in
	     alpha q ^ (chr (r + 97))
	 end;

fun backslashize put P =
    iterate
      (case c of
	   "_" => #put stdout "\\_"
	 | "#" => #put stdout "\\#"
	 | "\\" => #put stdout "\\\\"
	 | _ => #put stdout c)
    | c in list explode P
    end;

fun print_f |[put, ...]| =
    let fun compile_f [] = []
	  | compile_f ["%"] = [fn _ => put "%"]
	  | compile_f ("%" :: "s" :: l) = (fn P => put P) :: compile_f l
	  | compile_f ("%" :: "S" :: l) = backslashize put :: compile_f l
	  | compile_f (c :: l) = (fn _ => put c) :: compile_f l
    in
	fn fstring =>
	   let val actions = compile_f (explode fstring)
	   in
	       fn P =>
		  iterate
		    f P
		  | f in list actions
		  end
	   end
    end;

fun infile_or_stdin "-" = stdin
  | infile_or_stdin name =
    let val |[get, getline, ...]| = infile name
    in
	|[get=get, getline=getline]|
    end;

val layout_engine = ref "neato";
val layout_options = ref ([] : string list);
val longname_re = ref "^...";
val verbose = ref 0;
val center = ref "";
val unary = ref true;
val Pformat = ref "\\mathtt{%S}";
val fformat = ref "\\mathtt{%S}";

fun usage () =
    (#put stderr "Usage: pl2gastex <flags>* filename.\n\
     \  Version ";
     #put stderr version;
     #put stderr (", Copyright (C) Jean Goubault-Larrecq;\n\
      \     see file COPYRIGHT.\n\
      \  pl2gastex comes with ABSOLUTELY NO WARRANTY; see file COPYING, sections 11, 12.\n\
      \  This is free software, and you are welcome to redistribute it\n\
      \  under certain conditions; see TERMS AND CONDITIONS in file COPYING.\n\
      \    Use '-' instead of filename to read from stdin.\n\
      \  Flags are:\n\
      \    -h prints this help.\n\
      \    -layout <engine>: use <engine> to layout node positions.\n\
      \       Default: neato.  The other standard possibilities are dot,\n\
      \       twopi.\n\
      \    -v0 runs silently (default).\n\
      \    -v1, -v: this option is passed verbatim to the layout\n\
      \       engine.\n\
      \    -v2: -v is passed to the layout engine, and its output\n\
      \       is printed on stderr.\n\
      \    -epsilon <n>: set cutoff for neato layout engine.\n\
      \       If pl2gastex does not terminate, use -v and adjust cutoff\n\
      \       accordingly.\n\
      \    -overlap false|scale|true: set overlap mode for twopi layout engine.\n\
      \    -center <predicate>: specifies center for twopi layout engine.\n\
      \    -unary-opt: display unary transitions in format compatible with usual\n\
      \       word automata conventions.\n\
      \    -no-unary-opt: display all transitions in the same way.\n\
      \       default: -unary-opt.\n\
      \    -P <format-string>: displays predicate using <format-string>.\n\
      \       default: " ^ (!Pformat) ^ "\n\
      \       %s will be replaced by predicate symbol, %S will additionally\n\
      \       replace _ and # characters by \\_ and \\#, %% will be replaced by %.\n\
      \    -f <format-string>: displays function symbols using <format-string>.\n\
      \       default: "^ (!fformat) ^ "\n\
      \       <format-string> is as for -P.\n");
     #flush stderr ());


local
    val nfa = re_make_nfa [(re_parse "^#q", fn _ => ())]
in
    fun matches_abbrv P =
	case nfa_run (nfa, P) of
	    SOME _ => true
	  | _ => false
end;

local
    val nfa = re_make_nfa [ (re_parse "^[ \t]*(block[0-9]+)[ \t]*\\[.*pos=\"([0-9]+),([0-9]+)\"[^]]*\\];",
			    fn (s,a) => (1, re_subst(s,a,1),
					 intofstring (re_subst(s,a,2)),
					 intofstring (re_subst(s,a,3)))),
			   (re_parse "^[ \t]*(trans[0-9]+)[ \t]*\\[.*pos=\"([0-9]+),([0-9]+)\"[^]]*\\];",
			    fn (s,a) => (2, re_subst(s,a,1),
					 intofstring (re_subst(s,a,2)),
					 intofstring (re_subst(s,a,3))))]
in
    fun match_block_or_trans P = nfa_run (nfa, P)
end;

local
    val nfa = re_make_nfa [(re_parse "^[ \t]*}",
			    fn _ => ())]
in
    fun matches_end s =
	case nfa_run (nfa, s) of
	    SOME _ => true
	  | _ => false
end;

local
    val nfa = re_make_nfa [ (re_parse "^__type_([0-9]+)$",
			     fn (s,a) => (1, intofstring (re_subst (s,a,1)))),
			   (re_parse "^__def_([0-9]+)$",
			    fn (s,a) => (2, intofstring (re_subst (s,a,1))))]
in
    fun match_type_or_def P =
	nfa_run (nfa, P)
end;

local
    val nfa = re_make_nfa [(re_parse "^#", fn _ => ())]
in
    fun invisible_fun P =
	case nfa_run (nfa, P) of
	    SOME _ => true
	  | _ => false
end;

local
    val nfa = re_make_nfa [(re_parse "[0-9]+(\\.[0-9]*)?([eEfFgG][~-]?[0-9]+)?",
			    fn _ => ())]
in
    fun matches_num s =
	case nfa_run (nfa, s) of
	    SOME _ => true
	  | _ => false
end;

fun pint n =
    if n<0
	then (#put stdout "-";
	      print stdout (pack (~n)))
    else print stdout (pack n);

fun preal (x : num) =
    if x #< 0.0
	then (#put stdout "-";
	      print stdout (pack (#~ x)))
    else print stdout (pack x);

fun numc (x, y) =
    num x #+ 0:1 #* num y;

fun print_pred (put, pname) =
    let fun print_pred_1 P =
	    ((case block_of_exact P of
		  {} => pname "\\bot"
		| blk => let val delimr = ref "\\{"
			 in
			     iterate
			       (put (!delimr);
				delimr := ", ";
				print_pred_1 Q)
			     | Q in list sort (op strless) blk
			     end;
				put "\\}"
			 end
			 )
		 handle BlockOfExactEvt =>
		 case block_of_inter P of
		     {} => pname "\\top"
		   | {Q} => pname Q
		   | blk => let val delimr = ref ""
			    in
				iterate
				  (put (!delimr);
				   delimr := "\\cap ";
				   print_pred_1 Q)
				| Q in list sort (op strless) blk
				end
			    end
			    )
    in
	print_pred_1
    end;

fun do_args ["-h"] = usage ()
  | do_args ("-h"::l) = (usage (); do_args l)
  | do_args ("-layout"::engine::l) = (layout_engine := engine; do_args l)
  | do_args ("-v0"::l) =
    (verbose := 0; do_args l)
  | do_args ("-v1"::l) =
    (verbose := 1; do_args l)
  | do_args ("-v"::l) =
    (verbose := 1; do_args l)
  | do_args ("-v2"::l) =
    (verbose := 2; do_args l)
  | do_args ("-no-unary-opt" :: l) =
    (unary := false; do_args l)
  | do_args ("-unary-opt" :: l) =
    (unary := true; do_args l)
  | do_args ("-P" :: s :: l) =
    (Pformat := s; do_args l)
  | do_args ("-f" :: s :: l) =
    (fformat := s; do_args l)
  | do_args ("-epsilon"::x::l) =
    (if matches_num x
	 then (layout_options := "-Gepsilon=" ^ x :: !layout_options;
	       do_args l)
     else (#put stderr "Expected cutoff level (real) after -epsilon.\n";
	   #flush stderr ();
	   quit 2))
  | do_args ("-overlap"::x::l) =
    (layout_options := "-Goverlap=" ^ x :: !layout_options;
     do_args l)
  | do_args ("-center"::x::l) =
    (center := x; do_args l)
  | do_args (filename :: l) =
    (if not (null l)
	 then (#put stderr "ignored junk after filename (";
	       #put stderr filename;
	       #put stderr ")\n";
	       #flush stderr ())
     else ();
	 let val f = infile_or_stdin filename
	     val yyd = glex_data (f, fn _ => true)
	     val yyloc = glex_loc yyd
	     val hyd = gyacc_data (yyd, plautolex, aplnone (), plauto_value, yyloc, yyerror yyloc)
	 in
	     case plautoparse hyd of
		 SOME (aplauto a0) =>
		 let val AUTO (auto0, univ0) = a0
		     val auto = {P => fmap
				| P => fmap in map auto0
				    such that not (matches_abbrv P)}
		     val univ = {P | P in set univ0
				 such that not (matches_abbrv P)}
		     val a = AUTO (auto, univ)
		     val preds = univ U dom auto
		     val blocks = union {union {union {elems blkl
						      | blkl in set blkls}
					       | f => (blkls, ...) in map fmap}
					| P => fmap in map auto}
		     val blk_names = {blk => gensym "block"
				     | blk in set blocks U {{P} | P in set preds U union blocks}}
		     val t_names = overwrite [overwrite [{(P, f, blkl) => gensym "trans"
							 | blkl in set blkls}
							| f => (blkls, k, ...) in map fmap]
					     | P => fmap in map auto]
		     val t_dirs = ref ({} : string -m> int) (* will map each transition to
							     preferred direction:
							     0: left-to-right (transition below nodes)
							     1: upwards (transition to the right of nodes)
							     2: right-to-left (transition to the left of nodes)
							     3: downwards (transition above nodes)
							     *)
		     val nfa_longname = re_make_nfa [(re_parse (!longname_re), fn _ => ())]
		     fun longp s = (case nfa_run (nfa_longname, s) of SOME _ => true | _ => false)
		     val opts = rev (!layout_options)
		     val opts = if !verbose>=1
				    then "-v" :: opts
				else opts
		     val opts = if !center=""
				    then opts
				else ("-Gcenter=" ^ ?blk_names (block_of_inter (!center)) :: opts
				      handle MapGet =>
				      (#put stderr "Center node ";
				       #put stderr (!center);
				       #put stderr " not found, ignoring -center option.\n";
				       #flush stderr ();
				       opts))
		     val cmd as |[getline = pgetline, put = pput, flush = pflush, kill = pkill, ...]|
			 = inoutprocess (!layout_engine, opts)
		 in
		     pput "digraph sample {\n";
		     iterate (* List the nodes corresponding to single predicates,
			      so that the layout engine knows roughly what size
			      they take each. *)
		       (pput blkn;
			pput "[name=";
			(case blk of
			     {P} =>
			     if invisible_fun P
				 then pput "\".\""
			     (*else if longp P
				 then pput "\".\""
			      *)
			     else pput P
			   | _ => pput "inter");
			pput "];\n")
		     | blk => blkn in map blk_names
		     end;
		     iterate (* List the nodes corresponding to transitions,
			      so that the layout engine knows roughly the size
			      of functions used to label them. *)
		     (pput trans;
		      pput "[name=";
		      if invisible_fun f
			  then pput "\".\""
		      else pput f;
		      pput "];\n")
		     | (P, f, blkl) => trans in map t_names
		     end;
		     iterate
		       iterate
			 (pput Pname; pput " -> "; pput blkn; pput ";\n")
		       | P in set blk
		       val Pname = ?blk_names {P}
		       end
		     | blk => blkn in map blk_names
		       such that card blk > 1
		     end;
		     iterate
		       iterate
			 iterate
			   (iterate
			      (pput (?blk_names blk); pput " -> ";
			       pput trans; pput ";\n")
			    | blk in list blkl
			    end;
			      pput trans;
			      pput " -> ";
			      pput Pname;
			      pput ";\n"
			      )
			 | blkl in set blkls
			 val Pfblkl = (P, f, blkl)
			 val trans = ?t_names Pfblkl
			 end
		       | f => (blkls, ...) in map fmap
		       end
		     | P => fmap in map auto
		     val Pname = ?blk_names {P}
		     end;
		     pput "};\n\n";
		     pflush ();
		     let val posr = ref {}
			 val minx = ref max_int and maxx = ref min_int
			 and miny = ref max_int and maxy = ref min_int
			 val tposr = ref {}
			 val liner = ref ""
			 val inv_blk_names = inv blk_names
			 val inv_t_names = inv t_names
			 val pname = print_f stdout (!Pformat)
			 val pfname = print_f stdout (!fformat)
			 val ir = ref 0
		     in
			 while (liner := pgetline (); !liner <> "" andalso not (matches_end (!liner))) do
			     (
			      case match_block_or_trans (!liner) of
				  SOME (1,b,x,y) => (* block *)
				  (let val blk = ?inv_blk_names b
				   in
				       if !verbose>=2
					   then (#put stderr (!liner);
						 #flush stderr ())
				       else ();
				       posr := !posr ++ {blk => (x, y)};
				       if x < !minx then minx := x else ();
				       if x > !maxx then maxx := x else ();
				       if y < !miny then miny := y else ();
				       if y > !maxy then maxy := y else ()
				   end handle MapGet => ())
				| SOME(2,trans,x,y) => (* trans *)
				  (tposr := !tposr ++ {trans => (x, y)};
				   if x < !minx then minx := x else ();
				   if x > !maxx then maxx := x else ();
				   if y < !miny then miny := y else ();
				   if y > !maxy then maxy := y else ())
				| NONE => ());
			     (* We now have all needed coordinates in !posr. *)
			     pkill ();
			     (* First, compute directions of all transitions in t_dirs. *)
			     iterate
			       (let val (P, f, blkl) = ?inv_t_names trans
				    val Pb = {P}
				    val zP = numc (?(!posr) Pb)
				in
				    if exists blk=Pb | blk in list blkl end (* loop *)
					then (* try to make the line from P to trans
					      orthogonal to the arrows adjacent to trans. *)
					    let val angle = int (floor (2.0 #* im (log (numc (x, y) #- zP))
									#/ pi #+ 5.5)) mod 4
					    in
						t_dirs := !t_dirs ++ {trans => angle}
					    end
				    else if null blkl (* otherwise try to make arrows adjacent to trans
						       closest to line from trans to P if blkl is empty. *)
					     then let val angle = int (floor (2.0 #* im (log (zP #- numc (x, y)))
									      #/ pi #+ 4.5)) mod 4
						  in
						      t_dirs := !t_dirs ++ {trans => angle}
						  end
					 else (* otherwise try to make arrows adjacent to trans
					       parallel to line from barycenter of input nodes to
					       output node. *)
					     let val bPr = ref 0.0
						 val bP = (iterate
							     bPr := !bPr #+ numc (?(!posr) blk)
							   | blk in list blkl
							   end;
							     !bPr #/ num (len blkl))
						 val angle = int (floor (2.0 #* im (log (zP #- bP))
									 #/ pi #+ 4.5)) mod 4
					     in
						 t_dirs := !t_dirs ++ {trans => angle}
					     end
				end handle MapGet => ())
			     | trans => (x, y) in map !tposr
			     end;
			     #put stdout "\\begin{picture}(";
			     pint (!maxx - !minx + 20);
			     #put stdout ",";
			     pint (!maxy - !miny + 20);
			     #put stdout ")(";
			     pint (!minx - 10);
			     #put stdout ",";
			     pint (!miny - 10);
			     #put stdout ")\n";
			     #put stdout "  \\gasset{Nadjust=n}\n";
			     iterate (* print nodes *)
			       (#put stdout "  \\node";
				let val opts = ref nil
				    val delimr = ref "["
				in
				    (case blk of
					 {} => opts := "Nadjust=wh" :: "Nmarks=r" :: !opts
				       | {P} => (if P inset univ
						     then opts := "Nmarks=r" :: !opts
						 else ();
						     (case match_type_or_def P of
							  SOME _ => opts := "Nadjust=wh" :: !opts
							| _ => if longp P
								   then opts := "Nadjust=w" :: !opts
							       else opts := "Nadjust=n" :: !opts))
				       | _ => opts := "Nadjust=wh" :: !opts);
				    if null (!opts)
					then ()
				    else (iterate
					    (#put stdout (!delimr);
					     delimr := ",";
					     #put stdout opt)
					  | opt in list !opts
					  end;
					    #put stdout "]")
				end;
				#put stdout "(";
				#put stdout (?blk_names blk);
				#put stdout ")(";
				pint x;
				#put stdout ",";
				pint y;
				#put stdout "){";
				(case blk of
				     {} => #put stdout "${\\scriptstyle{*}}$"
				   | {P} => (case match_type_or_def P of
						 SOME (1, n) => (#put stdout "$\\scriptstyle\\oldstylenums{";
								 pint n;
								 #put stdout "}$")
					       | SOME (2, n) => (#put stdout "$\\scriptstyle ";
								 #put stdout (alpha n);
								 #put stdout "$")
					       | _ => (#put stdout "$";
						       print_pred (#put stdout, pname) P;
						       #put stdout "$"))
				   | _ => #put stdout "${\\scriptstyle\\wedge}$");
				#put stdout "}\n")
			     | blk => (x, y) in map !posr
			     end;
			     iterate
			       (#put stdout "  \\gasset{Nadjust=n,Nw=";
				#put stdout (if angle mod 2=0 then "1" else "20");
				#put stdout ",Nh=";
				#put stdout (if angle mod 2=0 then "20" else "1");
				#put stdout ",Nmr=0,fillgray=0} % black rectangle\n";
				#put stdout "  \\gasset{ExtNL=y,NLdist=3,NLangle=";
				preal (45.0 #+ 90.0 #* num angle);
				#put stdout "} % external label right and above the node\n";
				iterate
				  let val (P, f, blkl) = ?inv_t_names trans
				  in
				      if !unary andalso (case blkl of [_] => true | _ => false)
					  then ()
				      else
					  (#put stdout "  \\node(";
					   #put stdout trans;
					   #put stdout ")(";
					   pint x;
					   #put stdout ",";
					   pint y;
					   if invisible_fun f
					       then #put stdout "){}\n"
					   else (#put stdout "){$";
						 pfname f;
						 #put stdout "$}\n")
					       )
				  end
				| trans => (x, y) in map !tposr
				    such that ?(!t_dirs) trans=angle
					handle MapGet => (#put stderr trans;
							  #put stderr " has no direction!\n t_dirs = ";
							  maxprintlines := max_int;
							  pretty stderr (pack t_dirs);
							  #flush stderr ();
							  quit 2)
				end)
			     | angle in list [0, 1, 2, 3]
			     end;
			     #put stdout "  \\gasset{ELpos=85,ELdistC=y,ELdist=0} \
			      \% put (argument number) labels on the edge, toward the end\n";
			     iterate
			       (ir := 0;
				if !unary andalso nargs=1
				    then let val [blk] = blkl
					     val blkn = ?blk_names blk
					 in
					     if blk={P} (* self loop *)
						 then let val (xp,yp) = ?(!posr) blk
							  val dx = num (x - xp)
							  val dy = num (y - yp)
							  val theta1 = if x=xp
									   then if y>yp
										    then 0.5 #* pi
										else ~0.5 #* pi
								       else atan (dy #/ dx)
							  val theta = if dx #< 0.0
									  then if dy #< 0.0
										   then theta1 #- pi
									       else theta1 #+ pi
								      else theta1
							  val angle = theta #* (180.0 #/ pi)
						      in
							  #put stdout "  \\drawloop[loopangle=";
							  preal angle;
							  #put stdout ",ELpos=50,ELdistC=n](";
							  #put stdout blkn
						      end
					     else (
						   #put stdout "  \\drawqbedge[";
						   #put stdout (if horiz then "eyo" else "exo");
						   #put stdout "=0,ELpos=50,ELdistC=n](";
						   #put stdout blkn;
						   #put stdout ",";
						   pint x;
						   #put stdout ",";
						   pint y;
						   #put stdout ",";
						   #put stdout (?blk_names {P})
						   );
						 #put stdout "){";
						 if invisible_fun f
						     then ()
						 else (#put stdout "$";
						       pfname f;
						       #put stdout "$");
						     #put stdout "}\n"
					 end
				else
				    (iterate
				       let val eyo = if nargs=1
							 then 0.0
						     else 1.0 #- num (2 * !ir) #/ num (nargs-1)
					   (* varies from -1 to 1 *)
					   val reyo = eo #* eyo
				       in
					   #put stdout "  \\drawqbedge[";
					   #put stdout (if horiz then "eyo" else "exo");
					   #put stdout "=";
					   preal reyo;
					   #put stdout "](";
					   #put stdout blkn;
					   #put stdout ",";
					   (if horiz then preal (num x #+ offyo #+ 4.0 #* reyo) else pint x);
					   #put stdout ",";
					   (if horiz then pint y else preal (num y #+ offyo #+ 4.0 #* reyo));
					   #put stdout ",";
					   #put stdout trans;
					   #put stdout "){";
					   inc ir;
					   if nargs>1
					       then (#put stdout "\\tiny ";
						     pint (!ir))
					   else ();
					       #put stdout "}\n";
					       if card blk > 1
						   then
						       iterate
							 (#put stdout "  \\drawedge(";
							  #put stdout (?blk_names {Q});
							  #put stdout ",";
							  #put stdout blkn;
							  #put stdout "){}\n"
							  )
						       | Q in set blk
						       end
					       else ()
				       end
				     | blk in list blkl
				     val blkn = ?blk_names blk
				     end;
				       #put stdout "  \\drawqbedge(";
				       #put stdout trans;
				       #put stdout ",";
				       (if horiz then preal (num x #- offyo) else pint x);
				       #put stdout ",";
				       (if horiz then pint y else preal (num y #- offyo));
				       #put stdout ",";
				       #put stdout (?blk_names {P});
				       #put stdout "){}\n")
				    )
			     | trans => (x, y) in map !tposr
			     val (P, f, blkl) = ?inv_t_names trans
			     val nargs = len blkl
			     val angle = ?(!t_dirs) trans
			     val horiz = (angle mod 2=0)
			     val eo = if angle inset {0, 3} then ~5.0 else 5.0
			     val offyo = if angle inset {0, 1} then ~60.0 else 60.0
			     end;
			     #put stdout "\\end{picture}\n"
		 (*pretty stderr (pack (!posr));
		  #flush stderr ()*)
		 end;
		 #flush stdout ();
		 quit 0
	 end
  | _ =>
    (#put stderr "Parsing failed: stop.\n"; #flush stderr ();
     quit 2)
				  end handle IO n => (#put stderr filename;
						      #put stderr ": ";
						      #put stderr (iomsg n);
						      #put stderr "\n";
						      #flush stderr ();
						      quit 2)
					   | RE n => (#put stderr "Bad regexp: ";
						      #put stderr (remsg n);
						      #put stderr "\n";
						      #flush stderr ();
						      quit 2)
					   | PlautoUnterminatedCommentEvt => (#put stderr "Unterminated comment: stop.\n";
									      #flush stderr ();
									      quit 2))
  | do_args nil = (#put stderr "Missing filename.\n"; usage (); quit 2)
  | do_args _ = (usage ();
		 quit 2)
    ;

fun main () =
    do_args (args ());
