(*
============================================================================= 

  Thanks to Aron Helser for the vast majority of this package 

============================================================================= 
*)

(*
============================================================================= 

  These routines will parse the fsm model data and construct the
  model as an internal structure

  the routine to use is

    getModel

  example
 
    val M = getModel "meet.fsm" ;

  now M is the fsm model but in internal ML data structure form.

============================================================================= 
*)

(*
============================================================================= 

getModel generates a value of this type: 

  string list *     list of all atomic predicate names
  (  
    int *               state number
    bool list *         which atomic predicates are true in this state
    int list *          list of next states
    string list         ???

  ) list            all states in the FSM

============================================================================= 
*)

(* type definitions *)
type State = int * bool list * int list * string list;
type Model = string list * State list;

fun fileToString fileName = let
  val stream = open_in fileName
  val str = input(stream, can_input stream)
  val _ = close_in stream
in str end;

fun fileToList fileName = let
  fun f fh = if end_of_stream fh then
    let val _ = close_in fh in nil end
    else (input_line fh)::(f fh)
in f(open_in fileName) end;

(* drops leading spaces *)
fun dropSpace nil   = nil
      |   dropSpace(h::t) = if h=" " then dropSpace t else h::t;
val skipSpace = implode o dropSpace o explode;

(* drops trailing new line *)
fun dropNL nil = nil
     |    dropNL(h::t) = if h="\n" then dropNL t else h::dropNL t;
val skipNL = implode o dropNL o explode;

(* drops all null strings from a list of strings *)
fun removeNull nil = nil
   |    removeNull(h::t) = if h="" then removeNull t else h::removeNull t;


(* gets rid of leading spaces, trailing newlines, and blank lines 
   from a list of strings where each string is a line. *)
val stripItDown = removeNull o map (skipNL o skipSpace);


val END = ~1;
val ATOMTOKS = [" ",","];

exception BadInput;

fun white(c) =
   c=" " orelse c="\n" orelse c="\t";

fun digit(c) =
   c >= "0" andalso c <= "9";

(* finds out if something is in a list *)
fun member x  nil  = false
      |   member x(h::t) = (x=h) orelse member x t;

(* returns the index, from zero, of the item if it is in the list.
   Otherwise, return ~1 *)
fun membernth x  nil  = ~1
      |   membernth x (h::t) = if (x=h) then 0 else 
         let val i = (membernth x t) in 
           if i = ~1 then ~1 else
              1 + i
end;

fun finishInt(i,s) = 
     (* return the integer whose first digits have value i and 
        whose remaining digits are found in s, up to the end or 
        the first white space *)
     if s="" then i
     else let val c = hd (explode(s))
          in if digit(c) then finishInt(10*i+ord(c)-ord("0"), substring(s, 1,size s-1))
             else i
          end;

fun getInt(s) = 
     (* get the first digit from string;
        return END if there is no integer *)
     if s="" then END
     else let val c = hd (explode(s))
          in  if digit(c) then finishInt(ord(c)-ord("0"), substring(s, 1,size s-1))
              else getInt(substring(s, 1,size s-1))
          end;

(* chop s into a list of strings separated by any of the chars in toks *)
fun token([], s) = (s, "")
    | token(toks, "") = ("", "")
    | token(toks, s) = 
        if member (substring(s, 0, 1)) toks then ("", substring(s, 1,size s-1))
             else let val (M,N) = token(toks, substring(s, 1,size s-1)) in
            ((substring(s,0,1))^M, N)
end;

     
fun tokenize [] s = [s]
    | tokenize toks "" = []
    | tokenize toks s = 
        let val (M,N) = token(toks, s) in 
           if M="" then (tokenize toks N) else
           M::(tokenize toks N)
end;

(* take list of lists and cats it together into just a list *)
fun flatten nil  = nil
      |   flatten(h::t) = h @ flatten t;

(* val k = map (tokenize[" ",","]) f; *)

(* these functions process a list of lists which represents the tokens
   on the individual lines of the model input file. They each read in a 
   different part of the model *)
fun makeAtomicList ((";"::xs)::xxs:string list list) = ([],xxs)
    | makeAtomicList (([])::xxs:string list list) = makeAtomicList(xxs)
    | makeAtomicList ((x::xs)::xxs:string list list) = 
          let val (M,N) = makeAtomicList( xs::xxs) in
	       (x::M, N)
end;
    
(* form a bool list from the bitstring in the input file *)
fun makeAtomTrueList("") = []
    | makeAtomTrueList(y) =
        if substring(y,0,1) = "1" then
           true::makeAtomTrueList(substring(y, 1, size y-1))
        else if substring(y,0,1) = "0" then
           false::makeAtomTrueList(substring(y, 1, size y-1))
        else raise BadInput;

(* form an int list list from the successors in the input file-
   This is the structure of the graph *)
fun makeNextList (nil) = ([], [])
    | makeNextList (x::xs) = 
        if (hd(explode(x)))= "#" then
            ([], x::xs)
        else let val (M,N) = makeNextList(xs) in 
            ((getInt(x)::M), N)
             end;

fun makeStateList (nil) = []
    | makeStateList (x::y::xs) = 
    if (hd(explode(x)))= "#" then
          let val (nextlist, rest) = makeNextList(xs) in
	  (getInt(x), makeAtomTrueList(y), nextlist,[""])::makeStateList(rest)
	  end
    else raise BadInput
    | makeStateList ("#END"::xs) = []
    | makeStateList (_) = raise BadInput;


fun makeModel (("STATES"::xs)::xxs:string list list) = makeModel(xxs)
     | makeModel (("ARCS"::xs)::xxs) = makeModel(xxs)
     | makeModel (("ATOMIC"::xs)::xxs) = 
            let val (M,N) = makeAtomicList(xs::xxs)
	        val P = makeStateList(flatten N) in
		(M,P)
end;

(* reads in a file and makes it into a tuple representing the model *)

val getModel = makeModel o map (tokenize ATOMTOKS) o stripItDown o fileToList;