parse_env.ml

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

open Formula

let debug_parsing = true
  
type read_arc = Arc of node * arc_info * node

type label_ce = (string * Control.expr) 

type read_automata = Automata of 
  node        (* Initial node *)
  * vnt list  (* Input var list *)
  * vnt list  (* Output var list *)
  * vnt list  (* Local var list *)
  * vnt list  (* pre var list *)
  * label_ce list  (* Definition of labels representing control expressions *)
  * read_arc list  (* Transition list *)

(* Keywords of the automata format *)
let lexer = Genlex.make_lexer ["("; ")"; ","; ";"; ".";
			       "&&"; "||"; "#"; "!"; "true"; "false"; 
			       "IfThenElseNum";"IfThenElse";
			       "="; ">"; ">="; "<"; "<="; 
			       "+"; "-"; "*"; "/"; "%"]

type aut_token = Genlex.token Stream.t

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

let print_err_msg tok_list func =
  if debug_parsing then
    begin
      print_string ("* Parse error in " ^ func ^ ". ");
      print_string ("The next 10 tokens are:\n\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_list with  
	  | (Genlex.Kwd ";")::(Genlex.Kwd ",")::_ ->  Stream.junk tok; [] (* empty list *)   
	  | (Genlex.Kwd ";")::(Genlex.Kwd ".")::_ ->  Stream.junk tok; [] (* empty list *)   
	  | (Genlex.Kwd "," )::_ -> [] (* empty list *)   
	  | (Genlex.Kwd "." )::_ -> [] (* empty list *) 
	  | (Genlex.Kwd "%" )::_ -> [] (* empty list *)  
	  | (Genlex.Kwd ")" )::_ -> [] (* empty list *)  
	  | _ -> (
	      match tok with parser
		| [< vnt = parse ; tail = (parse_list_var_tail (parse)) >]
		  -> vnt :: tail  
	    )
	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_list with 
	  | (Genlex.Kwd ";")::(Genlex.Kwd ",")::_ ->  Stream.junk tok; [] (* end of the list *)
	  | (Genlex.Kwd ";")::(Genlex.Kwd ".")::_ ->  Stream.junk tok; [] (* end of the list *)
	  | (Genlex.Kwd "," )::_ -> [] (* end of the list *)  
	  | (Genlex.Kwd "." )::_ -> [] (* end of the list *)  
	  | (Genlex.Kwd "%" )::_ -> [] (* end of the list *)  
	  | (Genlex.Kwd ")" )::_ -> [] (* end of the list *)  
	  | _ -> (
	      match tok with parser
		  [< 'Genlex.Kwd ";" ;  tail = (parse_list_var_tail2 (parse)) >]
		  -> tail  
	    )
	with e ->
	  print_err_msg tok_list "parse_list_var_tail";
	  raise e

and (parse_list_var_tail2: (aut_token -> 'a) -> aut_token -> 'a list) = 
  fun parse tok -> 
    (* This function is introduced to allow lists to be ended by a `;'... *)
    let tok_list = Stream.npeek 10 tok in
      try
	match tok with parser 
	  | [< 'Genlex.Kwd ";"; _ = (parse_list_var_tail3 (parse)) >] -> [] 
	  | [< 'Genlex.Kwd "," >] -> [] 
	  | [< 'Genlex.Kwd "." >] -> [] 
	  | [< a = parse ; tail = (parse_list_var_tail (parse)) >]
	    -> a :: tail  
	with e ->
	  print_err_msg tok_list "parse_list_var_tail2";
	  raise e
and (parse_list_var_tail3: (aut_token -> 'a) -> aut_token -> 'a list) = 
  fun parse tok -> 
    (* This function is also introduced to allow lists to be ended by a `;'... *)
    let tok_list = Stream.npeek 10 tok in
      try
	match tok with parser 
	  | [< 'Genlex.Kwd "." >] -> [] 
	  | [< 'Genlex.Kwd "," >] -> [] 
	with e ->
	  print_err_msg tok_list "parse_list_var_tail3";
	  raise e


(** Parsing pragmas *)

type pragma = string * string

let rec (parse_pragma: aut_token -> pragma) =
  fun tok -> 
    let tok_list = Stream.npeek 10 tok in
      try
	match tok with parser  
	    [< 'Genlex.String label ; 'Genlex.Ident ":"; 
	       'Genlex.String pragma  >] -> (label, pragma)
	with e ->
	  print_err_msg tok_list "parse_pragma" ;
	  raise e
and
  (parse_pragma_list: aut_token -> pragma list) =
  fun tok -> 
    let tok_list = Stream.npeek 10 tok in
      try
	( match (Stream.npeek 1 tok) with 
	      [Genlex.Kwd "%"] -> 
		( match tok with parser  
		      [< 'Genlex.Kwd "%" ; 
			 pl = (parse_list (parse_pragma));
			 'Genlex.Kwd "%" 
		      >] 
		      -> pl
		)
	    | _ -> []
	)
      with e ->
	print_err_msg tok_list "parse_pragma_list" ;
	raise e

let rec (parse_automata: aut_token -> read_automata) = 
  fun tok -> 
    let tok_list = Stream.npeek 20 tok in
      try
	match tok with parser  
	    [< 'Genlex.Ident "inputs"; 'Genlex.Kwd "="; li = parse_list_var ; 
	       'Genlex.Kwd ",";
	       'Genlex.Ident "outputs"; 'Genlex.Kwd "="; lo = parse_list_genvar ;
	       'Genlex.Kwd ",";
	       'Genlex.Ident "locals"; 'Genlex.Kwd "="; ll = parse_list_genvar ;
	       'Genlex.Kwd ",";
	       'Genlex.Ident "pre"; 'Genlex.Kwd "="; lpre = parse_list_prevar ;
	       'Genlex.Kwd ",";
	       'Genlex.Ident "ctrl_expr"; 'Genlex.Kwd "="; llabel_ce = parse_list_label_ce ;
	       'Genlex.Kwd ",";
	       'Genlex.Ident "start_node"; 'Genlex.Kwd "="; 'Genlex.Int node_id ; 
	       'Genlex.Kwd "," ;
	       'Genlex.Ident "arcs_nb"; 'Genlex.Kwd "="; 'Genlex.Int arcs_nb ; 
	       'Genlex.Kwd "," ;
	       'Genlex.Ident "nodes_nb"; 'Genlex.Kwd "="; 'Genlex.Int nodes_nb ; 
	       'Genlex.Kwd "," ;
	       'Genlex.Ident "arcs"; 'Genlex.Kwd "="; la = parse_list_arc 
		      (List.append li (List.append lo (List.append ll lpre))) ;
	       'Genlex.Kwd ".";
	    >]
            -> Automata(node_id, li, lo, ll, lpre, llabel_ce, 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; 
	       prag_var = parse_pragma_list ; 
	       'Genlex.Kwd ",";  
	       'Genlex.Ident typ ; 
	       'Genlex.Kwd ")" >]
	    -> 
	      ( match typ with
		  "bool" -> (var, BoolT)
		| "float" -> (var, FloatT(-.max_float /. 2., max_float /. 2.))
		| "int" -> (var, IntT(min_int / 2, max_int / 2))
		    (* We divide by 2 so that domains are always smaller 
		       than max_int resp max_float *)
		| str -> failwith ("*** Bad type in .env: " ^ str )
	      )
	with e ->
	  print_err_msg tok_list "parse_var" ;
	  raise e

and (parse_list_genvar: aut_token -> vnt list) = 
  fun tok -> 
    let tok_list = Stream.npeek 10 tok in
      try
	parse_list (parse_genvar) tok
      with e ->
	print_err_msg tok_list "parse_list_genvar" ;
	raise e
and (parse_genvar: aut_token -> vnt) = 
  fun tok -> 
    let tok_list = Stream.npeek 10 tok in
      try
	match tok with parser  
	    [< 'Genlex.Kwd "("; 'Genlex.Ident var; pl = parse_pragma_list ;
	       'Genlex.Kwd ","; 'Genlex.Ident typ ;
	       vnt = parse_type var typ >]
	    -> vnt
	with e ->
	  print_err_msg tok_list "parse_genvar" ;
	  raise e
and (parse_type:  string -> string -> aut_token -> vnt) =
  fun var typ tok -> 
    let tok_list = Stream.npeek 10 tok in
      try
	match tok with parser  
	    [< 'Genlex.Kwd ")" >] -> 
	      ( match typ with
		    "bool" -> (var, BoolT)
		  | "float" -> (var, FloatT(-.max_float /. 2., max_float /. 2.))
		  | "int" -> (var, IntT(min_int / 2, max_int / 2))
		  | str -> failwith ("*** Bad type in .env: " ^ str )
	      )
	  | [< 'Genlex.Kwd ","; vnt = parse_type_more var typ >] -> vnt
	with e ->
	  print_err_msg tok_list "parse_type" ;
	  raise e
	    
and (parse_type_more:  string -> string -> aut_token -> vnt) =
  fun var typ tok -> 
    let tok_list = Stream.npeek 10 tok in
      try
	match tok with parser  
	    [< 'Genlex.Int min; 'Genlex.Kwd ","; 'Genlex.Int max;  'Genlex.Kwd ")" >] -> 
	      ( match typ with
		    "bool" -> failwith ("*** int expected in .env" )
		  | "float" -> failwith ("*** int expected in .env " )
		  | "int" -> (var, IntT(min, max))
		  | str -> failwith ("*** Bad type in .env: " ^ str )
	      )
	  | [< 'Genlex.Float min; 'Genlex.Kwd ","; 'Genlex.Float max;  'Genlex.Kwd ")" >] -> 
	      ( match typ with
		    "bool" -> failwith ("*** float expected in .env " )
		  | "float" -> (var, FloatT(min, max))
		  | "int" -> failwith ("*** float expected in .env " )
		  | str -> failwith ("*** Bad type in .env: " ^ str )
	      )
	with e ->
	  print_err_msg tok_list "parse_type_more" ;
	  raise e
	    

and (parse_list_prevar: aut_token -> vnt list) = 
  fun tok -> 
    let tok_list = Stream.npeek 10 tok in
      try
	parse_list (parse_prevar) tok
      with e ->
	print_err_msg tok_list "parse_list_prevar" ;
	raise e
and (parse_prevar: aut_token -> vnt) = 
  fun tok -> 
    let tok_list = Stream.npeek 10 tok in
      try
	match tok with parser  
	    [< 'Genlex.Kwd "("; 'Genlex.Ident "pre"; 'Genlex.Kwd "("; 
	       'Genlex.Int i ; 'Genlex.Kwd "," ; 'Genlex.Ident var;  
	       'Genlex.Kwd ")"; pl = parse_pragma_list ; 
	       'Genlex.Kwd ","; 'Genlex.Ident typ ; 'Genlex.Kwd ")" >]
	    -> 
	      let pre_var = ("_pre" ^ (string_of_int i) ^ var) in
	      ( match typ with
		  "bool" -> (pre_var, BoolT)
		| "float" -> (pre_var, FloatT(-.max_float /. 2., max_float /. 2.))
		| "int" -> (pre_var, IntT(min_int / 2, max_int / 2))
		| str -> failwith ("*** Bad type in .env: " ^ str )
	      )
	with e ->
	  print_err_msg tok_list "parse_prevar" ;
	  raise e

and (parse_list_label_ce: aut_token -> label_ce list) =
  fun tok -> 
    let tok_list = Stream.npeek 10 tok in
      try
	parse_list (parse_ce) tok
      with e ->
	print_err_msg tok_list "parse_list_label_ce" ;
	raise e
and (parse_ce: aut_token -> label_ce) = 
  fun tok -> 
    let tok_list = Stream.npeek 10 tok in
      try
	match tok with parser  
	    [< 'Genlex.Kwd "(" ; 
	       'Genlex.Ident label ;	 
	       'Genlex.Kwd "," ; 
	       expr = parse_list_ctrl_expr ; 
	       'Genlex.Kwd ")" 
	    >]
	    -> 
	      (label, expr)
	with e ->
	  print_err_msg tok_list "parse_ce" ;
	  raise e
and (parse_list_ctrl_expr : aut_token -> Control.expr) =
  fun tok -> 
    let tok_list = Stream.npeek 10 tok in
    let ce_list =
      try
	parse_list (parse_ctrl_expr) tok
      with e ->
	print_err_msg tok_list "parse_list_ctrl_expr" ;
	raise e
    in
      if ce_list = [] then (fun x -> x)
      else
	List.fold_left 
	  (fun ce1 ce2 -> (fun st -> ce2 (ce1 st)))
	  (List.hd ce_list) 
	  (List.tl ce_list)
and (parse_ctrl_expr: aut_token -> Control.expr) = 
  fun tok -> 
    let tok_list = Stream.npeek 10 tok in
      try
	match tok with parser  
	    [< 'Genlex.Ident "Set" ; 'Genlex.Ident varname ; 'Genlex.Int i 
	    >] ->
	      (Control.set varname i)
	  | [< 'Genlex.Ident "Set_between" ; 'Genlex.Ident varname ;
	       'Genlex.Int i ; 'Genlex.Int min ; 'Genlex.Int max 
	    >] -> 
	      (Control.set_between varname i min max)
	  | [< 'Genlex.Ident "Draw_between" ; 'Genlex.Ident varname ;
	       'Genlex.Int min ; 'Genlex.Int max 
	    >] -> 
	      (Control.draw_between varname min max)
	  | [< 'Genlex.Ident "Draw_gauss" ; 'Genlex.Ident varname ; 
	       m = parse_float ; dev = parse_float 
	    >] -> 
	      (Control.draw_gauss varname m dev)
	  | [< 'Genlex.Ident "Dec" ; 'Genlex.Ident varname 
	    >] -> 
	      (Control.dec varname)
	  | [< 'Genlex.Kwd "IfThenElse" ; test = parse_test_expr ; 
	       'Genlex.Kwd "(" ;  
	       cel_then = parse_list_ctrl_expr ; 
	       'Genlex.Kwd ")" ;  
	       'Genlex.Kwd "(" ;  
	       cel_else = parse_list_ctrl_expr ; 
	       'Genlex.Kwd ")" 
	    >] ->  
	      Control.ite test cel_then cel_else
	with e ->
	  print_err_msg tok_list "parse_ctrl_expr" ;
	  raise e

and (parse_float: aut_token -> float) =
  fun tok -> 
    let tok_list = Stream.npeek 10 tok in
      try
	match tok with parser  
	    [< 'Genlex.Float f >] -> f
	  | [< 'Genlex.Int i >] -> (float_of_int i)
	with e ->
	  print_err_msg tok_list "parse_float" ;
	  raise e


and (parse_int_or_var: aut_token -> Control.number) =
  fun tok -> 
    let tok_list = Stream.npeek 10 tok in
      try
	match tok with parser  
	    [< 'Genlex.Int i >] -> Control.IntExpr(i)
	  | [< 'Genlex.Ident id >] -> Control.VarExpr(id)
	with e ->
	  print_err_msg tok_list "parse_int_or_var" ;
	  raise e
	    
and (parse_test_expr: aut_token -> Control.test) =
  fun tok -> 
    let tok_list = Stream.npeek 10 tok in
      try
	match tok with parser
	    [< n1 = parse_int_or_var ; 'Genlex.Kwd op ; n2 = parse_int_or_var>] 
	    -> 
	      match op with
		| "<"  -> Control.GtExpr(n2, n1)
		| "<=" -> Control.GeExpr(n2, n1)
		| ">"  -> Control.GtExpr(n1, n2)
		| ">=" -> Control.GeExpr(n1, n2)
		| "="  -> Control.EqExpr(n1, n2)
		| _ -> assert false
	with e ->
	  print_err_msg tok_list "parse_test_expr" ;
	  raise e
	    

and (parse_list_arc: vnt list -> aut_token -> read_arc list) = 
  fun vars tok -> 
    let tok_list = Stream.npeek 10 tok in
      try
	parse_list (parse_arc vars) tok
      with e ->
	print_err_msg tok_list "parse_list_arc" ;
	raise e
and (parse_arc: vnt list -> aut_token -> read_arc) = 
  fun vars tok -> 
    let tok_list = Stream.npeek 10 tok in
      try
	match tok with parser  
	    [< 'Genlex.Ident "From"; 
	       'Genlex.Int node_from ; 
	       'Genlex.Ident "To"; 
	       'Genlex.Int node_to ; 
	       'Genlex.Ident "With"; 
	       arc_info = parse_arc_info vars
	    >]
	    -> Arc(node_from, arc_info, node_to)
	with e ->
	  print_err_msg tok_list "parse_arc" ;
	  raise e
and (parse_arc_info: vnt list -> aut_token -> arc_info) = 
  fun vars tok -> 
    let tok_list = Stream.npeek 10 tok in
      try
	match tok with parser  
	    [< weight = (parse_weight vars) ; 
	       'Genlex.Ident ":"; 
	       expr = parse_formula_eps vars ; 
	       pc = parse_post_cond_id
	    >] 
	    -> (weight, expr, pc)
	with e ->
	  print_err_msg tok_list "parse_arc_info" ;
	  raise e
and (parse_post_cond_id: aut_token -> string) =
  fun tok -> 
     let tok_list = Stream.npeek 10 tok in
      try
	match (Stream.npeek 2 tok) with
	    [ Genlex.Ident ":"; Genlex.Ident label ] -> 
	      Stream.junk tok;
	      Stream.junk tok;
	      label
	  | _ -> "identity"
	with e ->
	  print_err_msg tok_list "parse_post_cond_id" ;
	  raise e
and (parse_weight: vnt list -> aut_token -> weight) = 
  fun vars tok -> 
    let tok_list = Stream.npeek 10 tok in
      try
	match tok with parser  
	    [< 'Genlex.Int w >] -> Wint(w)
	  | [< 'Genlex.Kwd "!" ; 
	       'Genlex.Ident lbl >] 
	    -> Wident_not_sig(lbl)
	  | [< 'Genlex.Ident lbl >] -> Wident(lbl)
 	with e ->
	  print_err_msg tok_list "parse_weight" ;
	  raise e


and (parse_formula_eps: vnt list -> aut_token -> formula_eps) = 
  fun vars tok -> 
    let tok_list = Stream.npeek 10 tok in
      try
	match tok with parser   
	  | [< 'Genlex.Ident "eps" >] -> Eps
	  | [< 'Genlex.Ident "("; 'Genlex.Ident "eps"; 'Genlex.Ident ")" >] -> Eps
	  | [< f = parse_formula vars >] -> Form(f)
	with e ->
	  print_err_msg tok_list "parse_formula_eps" ;
	  raise e
	    
and (parse_formula: vnt list -> aut_token -> formula) = 
  fun vars tok -> 
    let tok_list = Stream.npeek 10 tok in
      try
	match tok with parser  
	    [< 'Genlex.Kwd "!"; pl = parse_pragma_list ;
	       f1 = parse_formula vars; 
	       f = parse_more_formula (Not(f1)) vars 
	                                         >] -> f  
	  | [< 'Genlex.Kwd "IfThenElse";  pl = parse_pragma_list ;
	       f1 = parse_formula vars; 
	       f2 = parse_formula vars; 
	       f3 = parse_formula vars           >] -> IteB(f1, f2, f3)
	  | [< 'Genlex.Kwd "("; 
	       f1 = parse_formula vars ; 'Genlex.Kwd ")" ; 
	       f = parse_more_formula f1 vars    >] -> f 
	  | [< 'Genlex.Kwd "true" ; pl = parse_pragma_list ;
	       f = parse_more_formula True vars  >] -> f
	  | [< 'Genlex.Kwd "false" ; pl = parse_pragma_list ;
	       f = parse_more_formula False vars >] -> f

	  | [< 'Genlex.Ident "pre"; 'Genlex.Kwd "("; 'Genlex.Int i ; 
	       'Genlex.Kwd "," ; 'Genlex.Ident id; 'Genlex.Kwd ")"; 
	       pl = parse_pragma_list ;  
	       f = parse_expr_or_bool_ident ("_pre" ^ (string_of_int i) ^ id) vars
	                                         >] -> f
	  | [< 'Genlex.Ident id ; 
	       pl = parse_pragma_list ; 
	       f1 = parse_expr_or_bool_ident id vars; 
	       f = parse_more_formula f1 vars    >] -> f
	  | [< e1 = parse_expr vars ; f = parse_expr_right e1 vars 
	                                         >] -> f
	with e ->
	  print_err_msg tok_list "parse_formula" ;
	  raise e

and (parse_expr_or_bool_ident: string -> vnt list -> aut_token -> formula) = 
  fun id vars tok -> 
    let tok_list = Stream.npeek 10 tok in
    let (_, vt) = List.find (fun (vn,vt) -> vn = id) vars in
    let some_var =
      match vt with
	  BoolT -> None
	| IntT(_,_) -> Some(Ivar(id))
	| FloatT(_,_) -> Some(Fvar(id))
    in
      ( match some_var with
	    None -> 
	      ( try
		 match tok with parser
		      [< f = parse_more_formula (Bvar(id)) vars >] -> f 
		 with e ->
		   print_err_msg tok_list "parse_expr_or_bool_ident" ;
		   raise e
	      )
	  | Some(var) -> 
	      ( try
		  match tok with parser  
		      [< 'Genlex.Kwd "=";  pl = parse_pragma_list ; e2 = parse_expr vars >] -> Eq(var, e2) 
		    | [< 'Genlex.Kwd ">";  pl = parse_pragma_list ; e2 = parse_expr vars >] -> Sup(var, e2) 
		    | [< 'Genlex.Kwd ">="; pl = parse_pragma_list ; e2 = parse_expr vars >] -> SupEq(var, e2)
		    | [< 'Genlex.Kwd "<";  pl = parse_pragma_list ; e2 = parse_expr vars >] -> Inf(var, e2) 
		    | [< 'Genlex.Kwd "<="; pl = parse_pragma_list ; e2 = parse_expr vars >] -> InfEq(var, e2)
	      with e ->
		print_err_msg tok_list "parse_expr_or_bool_ident" ;
		raise e
	      )
      )

and (parse_more_formula: formula -> vnt list -> aut_token -> formula) = 
  fun f1 vars tok -> 
    let tok_list = Stream.npeek 10 tok in
      try
	match tok with parser  
	    [< 'Genlex.Kwd "||"; pl = parse_pragma_list ; 
	       f2 = parse_formula vars >] -> Or(f1, f2)
	  | [< 'Genlex.Kwd "&&"; pl = parse_pragma_list ; 
	       f2 = parse_formula vars >] -> And(f1, f2)
	  | [< 'Genlex.Kwd "#"; pl = parse_pragma_list ; 
	       f2 = parse_formula vars >] -> And(Or(f1, f2), Not(And(f1, f2))) (* xor *)
	  | [< 'Genlex.Kwd "="; pl = parse_pragma_list ; 
	       f2 = parse_formula vars >] -> Or(And(f1, f2), And(Not(f1), Not(f2))) 
	  | [< >] -> f1
	with e ->
	  print_err_msg tok_list "parse_more_formula" ;
	  raise e
and (parse_expr_right : expr -> vnt list -> aut_token -> formula) = 
  fun e1 vars tok -> 
    let tok_list = Stream.npeek 10 tok in
      try
	match tok with parser
	    [< 'Genlex.Kwd "=";  pl = parse_pragma_list ; e2 = parse_expr vars >] -> Eq(e1, e2) 
	  | [< 'Genlex.Kwd ">";  pl = parse_pragma_list ; e2 = parse_expr vars >] -> Sup(e1, e2) 
	  | [< 'Genlex.Kwd ">="; pl = parse_pragma_list ; e2 = parse_expr vars >] -> SupEq(e1, e2)
	  | [< 'Genlex.Kwd "<";  pl = parse_pragma_list ; e2 = parse_expr vars >] -> Inf(e1, e2) 
	  | [< 'Genlex.Kwd "<="; pl = parse_pragma_list ; e2 = parse_expr vars >] -> InfEq(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: vnt list -> aut_token -> expr) = 
  fun vars tok -> 
    match tok with parser  
	[< e1 = parse_mult vars; e = parse_more_adds e1 vars >] -> e
and (parse_more_adds: expr -> vnt list -> aut_token -> expr) = 
  fun e1 vars tok -> 
    match tok with parser  
	[< 'Genlex.Kwd "+"; pl = parse_pragma_list ;
	   e2 = parse_mult vars; 
	   e = parse_more_adds (Sum(e1, e2)) vars >] -> e
      | [< 'Genlex.Kwd "-"; pl = parse_pragma_list ;
	   e2 = parse_mult vars; 
	   e = parse_more_adds (Diff(e1, e2)) vars >] -> e
      | [<  >] -> e1
and (parse_mult: vnt list -> aut_token -> expr) = 
  fun vars tok -> 
    match tok with parser  
	[< e1 = parse_simple vars; e = parse_more_mults e1 vars >] -> e
and (parse_more_mults: expr -> vnt list -> aut_token -> expr) = 
  fun e1 vars tok -> 
    match tok with parser  
	[< 'Genlex.Kwd "*"; pl = parse_pragma_list ;  
	   e2 = parse_simple vars; 
	   e = parse_more_mults (Prod(e1, e2)) vars >] -> e
      | [< 'Genlex.Kwd "/"; pl = parse_pragma_list ;  
	   e2 = parse_simple vars; 
	   e = parse_more_mults (Quot(e1, e2)) vars >] -> e
      | [< 'Genlex.Ident "mod"; pl = parse_pragma_list ; 
	   e2 = parse_simple vars; 
	   e = parse_more_mults (Mod(e1, e2)) vars >] -> e
      | [<  >] -> e1
and (parse_simple: vnt list -> aut_token -> expr) = 
  fun vars tok -> 
    match tok with parser  
      
      | [< 'Genlex.Ident "pre"; 'Genlex.Kwd "(";  
	   'Genlex.Int i ; 'Genlex.Kwd "," ; 'Genlex.Ident id;   
	   'Genlex.Kwd ")"; pl = parse_pragma_list  >] -> 
	  let s = ("_pre" ^ (string_of_int i) ^ id) in 
	  let (_, vt) = List.find (fun (vn,vt) -> vn = s) vars in 
	  let var = 
	    match vt with 
		BoolT -> assert false  
	      | IntT(_,_) -> Ivar(s) 
	      | FloatT(_,_) -> Fvar(s) 
	  in 
	    var 

      | [< 'Genlex.Ident s ; pl = parse_pragma_list >] -> 
	  let (_, vt) = List.find (fun (vn,vt) -> vn = s) vars in
	  let var =
	    match vt with
		BoolT -> assert false 
	      | IntT(_,_) -> Ivar(s)
	      | FloatT(_,_) -> Fvar(s)
	  in
	    var
  
      | [< 'Genlex.Int i;   pl = parse_pragma_list >] -> Ival(i)
      | [< 'Genlex.Float f; pl = parse_pragma_list >] -> Fval(f)
      | [< 'Genlex.Kwd "IfThenElseNum";  pl = parse_pragma_list ; 
	   f1 = parse_formula vars; 
	   e2 = parse_expr vars; 
	   e3 = parse_expr vars >] -> Ite(f1, e2, e3) 
      | [< 'Genlex.Kwd "("; e = parse_expr vars; 'Genlex.Kwd ")" >] -> e