(*-----------------------------------------------------------------------
** Copyright (C) 2001 - Verimag.
** This file may only be copied under the terms of the GNU Library General
** Public License 
**-----------------------------------------------------------------------
**
** File: parse_env.ml
** Main author: jahier@imag.fr
*)

open Formula

  
type read_arc = Arc of node * arc_info * node

type read_automata = Automata of 
  node        (* Initial node *)
  * vnt list  (* Input var list *)
  * vnt list  (* Output var list *)
  * vnt list  (* Local var list *)
  * vne list  (* pre var list of expression *)
  * vnf list  (* pre var list of formula *)
  * read_arc list  (* Transition list *)

(* Keywords of the automata format *)
let lexer = Genlex.make_lexer ["automata"; "["; "]"; "("; ")"; ","; ":"; ";";
			       "arc"; "eps"; "pre";
			       "And"; "Or"; "Not"; "true"; "false";
			       "="; ">"; ">=";
			       "+"; "-"; "*"; "/"; "mod"; "%"]

type aut_token = Genlex.token Stream.t

let print_genlex_token = 
  fun tok -> 
    let _ =
      match tok with
	  Genlex.Kwd(str)    -> print_string str
	| Genlex.Ident(str)  -> print_string str
	| Genlex.Int(i)      -> print_int i
	| Genlex.Float(f)    -> print_float f
	| Genlex.String(str) -> print_string str
	| Genlex.Char(c)     -> print_char c  
    in
      print_string " "

let debug_parsing = false

let print_err_msg tok_list func =
  if debug_parsing then
    begin
      print_string ("* Parse error in " ^ func ^ ".\n\t\t\t\t");
      print_string ("The next 10 tokens are:\t``");
      List.iter (print_genlex_token) tok_list ;
      print_string ("''\n");
      flush stdout
    end 
  else ()
  

(** Parsing lists *)
let rec
  (parse_list: (aut_token -> 'a) -> aut_token -> 'a list) = 
  fun parse tok -> 
    let tok_list = Stream.npeek 10 tok in
      try
	match tok with parser  
            [< vnt = parse ; tail = (parse_list_var_tail (parse)) >]
	    -> vnt :: tail  
	  | [< >] -> [] (* empty list *)
	with e ->
	  print_err_msg tok_list "parse_list";
	  raise e
and (parse_list_var_tail: (aut_token -> 'a) -> aut_token -> 'a list) = 
  fun parse tok -> 
    let tok_list = Stream.npeek 10 tok in
      try
	match tok with parser 
	  | [< 'Genlex.Kwd ";" ; a = parse ;
	       tail = (parse_list_var_tail (parse)) >]
	    -> a :: tail  
	  | [< >] -> [] (* end of the list *)
	with e ->
	  print_err_msg tok_list "parse_list_var_tail";
	  raise e



let rec (parse_automata: aut_token -> read_automata) = 
  fun tok -> 
    let tok_list = Stream.npeek 10 tok in
      try
	match tok with parser  
	    [< 'Genlex.Kwd "automata" ;
	       'Genlex.Kwd "(" ; 
	       'Genlex.Int node_id ; 'Genlex.Kwd "," ;
	       'Genlex.Kwd "[" ; li = parse_list_var ; 'Genlex.Kwd "]" ; 
	       'Genlex.Kwd "," ;
	       'Genlex.Kwd "[" ; lo = parse_list_var ; 'Genlex.Kwd "]" ; 
	       'Genlex.Kwd "," ;
	       'Genlex.Kwd "[" ; ll = parse_list_var ; 'Genlex.Kwd "]" ; 
	       'Genlex.Kwd "," ;
	       'Genlex.Kwd "[" ; lpe = parse_list_pre_expr ; 'Genlex.Kwd "]" ; 
	       'Genlex.Kwd "," ;
	       'Genlex.Kwd "[" ; lpf = parse_list_pre_form ; 'Genlex.Kwd "]" ; 
	       'Genlex.Kwd "," ;
	       'Genlex.Kwd "[" ; la = parse_list_arc ; 'Genlex.Kwd "]" ;
	       'Genlex.Kwd ")" >] 
            -> Automata(node_id, li, lo, ll, lpe, lpf, la)
	with e ->
	  print_err_msg tok_list "parse_automata";
	  raise e
	    

and (parse_list_var: aut_token -> vnt list) = 
  fun tok -> 
    let tok_list = Stream.npeek 10 tok in
      try
	parse_list (parse_var) tok
      with e ->
	print_err_msg tok_list "parse_list_var" ;
	raise e
and (parse_var: aut_token -> vnt) = 
  fun tok -> 
    let tok_list = Stream.npeek 10 tok in
      try
	match tok with parser  
	    [< 'Genlex.Kwd "("; 'Genlex.Ident var; 'Genlex.Kwd ","; 
	       'Genlex.Ident typ ; 'Genlex.Kwd ")" >]
	    -> (var, typ)
	with e ->
	  print_err_msg tok_list "parse_var" ;
	  raise e

and (parse_list_pre_expr: aut_token -> vne list) = 
  fun tok -> 
    let tok_list = Stream.npeek 10 tok in
      try
	parse_list (parse_pre_expr) tok
      with e ->
	print_err_msg tok_list "parse_list_pre_expr" ;
	raise e
and (parse_pre_expr: aut_token -> vne) = 
  fun tok -> 
    let tok_list = Stream.npeek 10 tok in
      try
	match tok with parser  
	    [< 'Genlex.Kwd "("; 'Genlex.Ident var; 'Genlex.Kwd ","; 
	       e = parse_expr ; 'Genlex.Kwd ","; init = parse_expr ; 'Genlex.Kwd ")" >]
	    -> (var, (e, init))
	with e ->
	  print_err_msg tok_list "parse_pre_expr" ;
	  raise e

and (parse_list_pre_form: aut_token -> vnf list) = 
  fun tok -> 
    let tok_list = Stream.npeek 10 tok in
      try
	parse_list (parse_pre_form) tok
      with e ->
	  print_err_msg tok_list "parse_list_pre_form" ;
	raise e
and (parse_pre_form: aut_token -> vnf) = 
  fun tok -> 
    let tok_list = Stream.npeek 10 tok in
      try
	match tok with parser  
	    [< 'Genlex.Kwd "("; 'Genlex.Ident var; 'Genlex.Kwd ","; 
	       f = parse_formula ; 'Genlex.Kwd ","; init = parse_formula; 'Genlex.Kwd ")" >]
	    -> (var, (f, init))
	with e ->
	  print_err_msg tok_list "parse_pre_form" ;
	  raise e


and (parse_list_arc: aut_token -> read_arc list) = 
  fun tok -> 
    let tok_list = Stream.npeek 10 tok in
      try
	parse_list (parse_arc) tok
      with e ->
	print_err_msg tok_list "parse_list_arc" ;
	raise e
and (parse_arc: aut_token -> read_arc) = 
  fun tok -> 
    let tok_list = Stream.npeek 10 tok in
      try
	match tok with parser  
	    [< 'Genlex.Kwd "arc"; 'Genlex.Kwd "("; 'Genlex.Int node_from ; 
	       'Genlex.Kwd ","; arc_info = parse_arc_info ; 
	       'Genlex.Kwd "," ; 'Genlex.Int node_to ; 'Genlex.Kwd ")";  >]
	    -> Arc(node_from, arc_info, node_to)
	with e ->
	  print_err_msg tok_list "parse_arc" ;
	  raise e
and (parse_arc_info: aut_token -> arc_info) = 
  fun tok -> 
    let tok_list = Stream.npeek 10 tok in
      try
	match tok with parser  
	    [< 'Genlex.Int weigth ; 'Genlex.Kwd ":"; expr = parse_formula_eps >] 
	    -> (weigth, expr)
	with e ->
	  print_err_msg tok_list "parse_arc_info" ;
	  raise e

and (parse_formula_eps: aut_token -> formula_eps) = 
  fun tok -> 
    let tok_list = Stream.npeek 10 tok in
      try
	match tok with parser   
	    [< 'Genlex.Kwd "eps" >] -> Eps
	  | [< f = parse_formula >] -> Form(f)
	with e ->
	  print_err_msg tok_list "parse_formula_eps" ;
	  raise e
	    
and (parse_formula: aut_token -> formula) = 
  fun tok -> 
    let tok_list = Stream.npeek 10 tok in
      try
	match tok with parser  
	    [< 'Genlex.Kwd "Not"; f1 = parse_formula ; 
	       f = parse_more_formula (Not(f1)) >] -> f  
	  | [< 'Genlex.Kwd "("; f1 = parse_formula; 'Genlex.Kwd ")" ; 
	       f = parse_more_formula f1 >] -> f 
	  | [< 'Genlex.Kwd "true" ; f = parse_more_formula True >] -> f
	  | [< 'Genlex.Kwd "false" ; f = parse_more_formula False >] -> f
	  | [< 'Genlex.Ident b ; f = parse_more_formula (Bvar(b)) >] -> f
	  | [< e1 = parse_expr; f1 = parse_expr_right e1 ; 
	       f = parse_more_formula f1 >] -> f
	with e ->
	  print_err_msg tok_list "parse_formula" ;
	  raise e

and (parse_more_formula: formula -> aut_token -> formula) = 
  fun f1 tok -> 
    let tok_list = Stream.npeek 10 tok in
      try
	match tok with parser  
	    [< 'Genlex.Kwd "Or";  f2 = parse_formula >] -> Or(f1, f2)
	  | [< 'Genlex.Kwd "And"; f2 = parse_formula >] -> And(f1, f2) 
	  | [< >] -> f1
	with e ->
	  print_err_msg tok_list "parse_more_formula" ;
	  raise e
and (parse_expr_right : expr -> aut_token -> formula) = 
  fun e1 tok -> 
    let tok_list = Stream.npeek 10 tok in
      try
	match tok with parser
	    [< 'Genlex.Kwd "=";  e2 = parse_expr >] -> Eq(e1, e2) 
	  | [< 'Genlex.Kwd ">";  e2 = parse_expr >] -> G(e1, e2) 
	  | [< 'Genlex.Kwd ">="; e2 = parse_expr >] -> Ge(e1, e2)
	with e ->
	  print_err_msg tok_list "parse_expr_rigth" ;
	  raise e
	    

(* 
 ** The following is copy-paste-adapted from sec 1.8 of the ocaml ref man 
 ** untitled ``pretty printing and parsing''.
 *)
and (parse_expr: aut_token -> expr) = 
  fun tok -> 
    match tok with parser  
	[< e1 = parse_mult; e = parse_more_adds e1 >] -> e
and (parse_more_adds: expr -> aut_token -> expr) = 
  fun e1 tok -> 
    match tok with parser  
	[< 'Genlex.Kwd "+"; e2 = parse_mult; 
	   e = parse_more_adds (Sum(e1, e2)) >] -> e
      | [< 'Genlex.Kwd "-"; e2 = parse_mult; 
	   e = parse_more_adds (Diff(e1, e2)) >] -> e
      | [<  >] -> e1
and (parse_mult: aut_token -> expr) = 
  fun tok -> 
    match tok with parser  
	[< e1 = parse_simple; e = parse_more_mults e1 >] -> e
and (parse_more_mults: expr -> aut_token -> expr) = 
  fun e1 tok -> 
    match tok with parser  
	[< 'Genlex.Kwd "*";   e2 = parse_simple; 
	   e = parse_more_mults (Prod(e1, e2)) >] -> e
      | [< 'Genlex.Kwd "/";   e2 = parse_simple; 
	   e = parse_more_mults (Quot(e1, e2)) >] -> e
      | [< 'Genlex.Kwd "mod"; e2 = parse_simple; 
	   e = parse_more_mults (Mod(e1, e2)) >] -> e
      | [<  >] -> e1
and (parse_simple: aut_token -> expr) = 
  fun tok -> 
    match tok with parser  
	[< 'Genlex.Ident s >] -> Nvar(s)
      | [< 'Genlex.Int i >]   -> Ival(i)
      | [< 'Genlex.Float f >] -> Fval(f)
      | [< 'Genlex.Kwd "("; e = parse_expr; 'Genlex.Kwd ")" >] -> e