ocaml error when using 'list_of_string' function

[alex4482]

Hello
I have this function below:

It is supposed to read lines from a file, until a line starts with the character 'p'.
Btw, i wrote pChar like this let pChar = hd (list_of_string "p"), because i couldn't figure out how to actually write a simple character. (which of these to use ' " `` ).
If no lines that start with p are found and it reaches EOF, give an error.
If line is found then return the last number from that line (its the one i need), and the fd_read, so that other functions may continue reading from the file from where it left off.
example of such line: p cnf 42 133

1.I am not sure if I correctly wrote this case: 'reached EOF', and if this is how fd_read actually works, that it remembers where in the file it read last.
2.
Below the function, I put a screenshot of an error as i was trying to get OCaml code from FStar code, and create an executable.
I did not get any 'fstar errors' (i solved the ones i got), but i got that, and im not sure it is my fault or a bug.
Is there a workaround?

val getNumberOfClauses : fd_read -> ML( int & fd_read)
let rec getNumberOfClauses (fileStream: fd_read)  = 
    let line = read_line fileStream in
        if strlen line = 0
        then
            failwith "did not find line that starts with 'p' to indicate number of clauses"
        else
            if hd (list_of_string line) = pChar
                then  
                    let lineParts = String.split spaceSeparator line in
                        let numberOfClauses = last lineParts in
                            let numberOfVariables = last (init lineParts) in
                                (stringToInt (list_of_string numberOfClauses)), fileStream 
                else  
                    getNumberOfClauses fileStream

I NEVER USE THE OPTION KEYWORD IN THE OTHER RELATED FUNCTIONS

Maybe there are multiple 'last' functions? One that returns Option?

[aseemr]

Sorry, this was a bug in the implementation of FStar_List.last. I have now pushed a fix for the same so your code should compile with the F* master branch.

Regarding your other two questions:

• You can write char constants with '. E.g. let pChar = 'p'
• For the EOF case, the read_line function in FStar.IO raises an exception EOF when the file ends, so something like this:

let rec read_all (fd:fd_read) : ML unit =
  try
    let s = read_line fd in
    //operate on s
    read_all fd
  with
    | _ -> ()

We will add documentation for it. Hope this helps, thanks for reporting the issue!