1 files changed, 18 insertions, 62 deletions

diff --git a/src/smtlib2/sExprLexer.mll b/src/smtlib2/sExprLexer.mll
index d926930..f45de19 100644
--- a/src/smtlib2/sExprLexer.mll
+++ b/src/smtlib2/sExprLexer.mll
@@ -24,50 +24,6 @@
   open Lexing
   open SExprParser
 
-  let char_for_backslash = function
-    | 'n' -> '\010'
-    | 'r' -> '\013'
-    | 'b' -> '\008'
-    | 't' -> '\009'
-    | c -> c
-
-  let lf = '\010'
-
-  let dec_code c1 c2 c3 =
-    100 * (Char.code c1 - 48) + 10 * (Char.code c2 - 48) + (Char.code c3 - 48)
-
-  let hex_code c1 c2 =
-    let d1 = Char.code c1 in
-    let val1 =
-      if d1 >= 97 then d1 - 87
-      else if d1 >= 65 then d1 - 55
-      else d1 - 48 in
-    let d2 = Char.code c2 in
-    let val2 =
-      if d2 >= 97 then d2 - 87
-      else if d2 >= 65 then d2 - 55
-      else d2 - 48 in
-    val1 * 16 + val2
-
-  let found_newline ({ lex_curr_p; _ } as lexbuf) diff =
-    lexbuf.lex_curr_p <-
-      {
-        lex_curr_p with
-        pos_lnum = lex_curr_p.pos_lnum + 1;
-        pos_bol = lex_curr_p.pos_cnum - diff;
-      }
-
-  (* same length computation as in [Lexing.lexeme] *)
-  let lexeme_len { lex_start_pos; lex_curr_pos; _ } = lex_curr_pos - lex_start_pos
-
-  let main_failure lexbuf msg =
-    let { pos_lnum; pos_bol; pos_cnum; pos_fname = _ } = lexeme_start_p lexbuf in
-    let msg =
-      sprintf
-        "Sexplib.Lexer.main: %s at line %d char %d"
-        msg pos_lnum (pos_cnum - pos_bol)
-    in
-    failwith msg
 }
 
 let lf = '\010'
@@ -82,7 +38,7 @@ let unquoted_start =
   unquoted # ['#' '|'] | '#' unquoted # ['|'] | '|' unquoted # ['#']
 
 rule main buf = parse
-  | lf | dos_newline { found_newline lexbuf 0; main buf lexbuf }
+  | lf | dos_newline { SmtMisc.found_newline lexbuf 0; main buf lexbuf }
   | blank+ | ';' (_ # lf_cr)* { main buf lexbuf }
   | '(' { LPAREN }
   | ')' { RPAREN }
@@ -99,7 +55,7 @@ rule main buf = parse
         scan_block_comment buf [lexeme_start_p lexbuf] lexbuf;
         main buf lexbuf
       }
-  | "|#" { main_failure lexbuf "illegal end of comment" }
+  | "|#" { SmtMisc.main_failure lexbuf "illegal end of comment" }
   | '|'
     {
       scan_quoted buf (lexeme_start_p lexbuf) lexbuf;
@@ -108,7 +64,7 @@ rule main buf = parse
       STRING ("|"^ str ^"|")
     }
   | unquoted_start unquoted* ("#|" | "|#") unquoted*
-      { main_failure lexbuf "comment tokens in unquoted atom" }
+      { SmtMisc.main_failure lexbuf "comment tokens in unquoted atom" }
   | "#" | unquoted_start unquoted* as str { STRING str }
   | eof { EOF }
 
@@ -116,22 +72,22 @@ and scan_string buf start = parse
   | '"' { () }
   | '\\' lf [' ' '\t']*
       {
-        found_newline lexbuf (lexeme_len lexbuf - 2);
+        SmtMisc.found_newline lexbuf (SmtMisc.lexeme_len lexbuf - 2);
         scan_string buf start lexbuf
       }
   | '\\' dos_newline [' ' '\t']*
       {
-        found_newline lexbuf (lexeme_len lexbuf - 3);
+        SmtMisc.found_newline lexbuf (SmtMisc.lexeme_len lexbuf - 3);
         scan_string buf start lexbuf
       }
   | '\\' (['\\' '\'' '"' 'n' 't' 'b' 'r' ' '] as c)
       {
-        Buffer.add_char buf (char_for_backslash c);
+        Buffer.add_char buf (SmtMisc.char_for_backslash c);
         scan_string buf start lexbuf
       }
   | '\\' (digit as c1) (digit as c2) (digit as c3)
       {
-        let v = dec_code c1 c2 c3 in
+        let v = SmtMisc.dec_code c1 c2 c3 in
         if v > 255 then (
           let { pos_lnum; pos_bol; pos_cnum; _ } = lexeme_end_p lexbuf in
           let msg =
@@ -146,7 +102,7 @@ and scan_string buf start = parse
       }
   | '\\' 'x' (hexdigit as c1) (hexdigit as c2)
       {
-        let v = hex_code c1 c2 in
+        let v = SmtMisc.hex_code c1 c2 in
         Buffer.add_char buf (Char.chr v);
         scan_string buf start lexbuf
       }
@@ -158,8 +114,8 @@ and scan_string buf start = parse
       }
   | lf
       {
-        found_newline lexbuf 0;
-        Buffer.add_char buf lf;
+        SmtMisc.found_newline lexbuf 0;
+        Buffer.add_char buf SmtMisc.lf;
         scan_string buf start lexbuf
       }
   | ([^ '\\' '"'] # lf)+
@@ -181,22 +137,22 @@ and scan_quoted buf start = parse
   | '|' { () }
   | '\\' lf [' ' '\t']*
       {
-        found_newline lexbuf (lexeme_len lexbuf - 2);
+        SmtMisc.found_newline lexbuf (SmtMisc.lexeme_len lexbuf - 2);
         scan_quoted buf start lexbuf
       }
   | '\\' dos_newline [' ' '\t']*
       {
-        found_newline lexbuf (lexeme_len lexbuf - 3);
+        SmtMisc.found_newline lexbuf (SmtMisc.lexeme_len lexbuf - 3);
         scan_quoted buf start lexbuf
       }
   | '\\' (['\\' '\'' '"' 'n' 't' 'b' 'r' ' ' '|'] as c)
       {
-        Buffer.add_char buf (char_for_backslash c);
+        Buffer.add_char buf (SmtMisc.char_for_backslash c);
         scan_quoted buf start lexbuf
       }
   | '\\' (digit as c1) (digit as c2) (digit as c3)
       {
-        let v = dec_code c1 c2 c3 in
+        let v = SmtMisc.dec_code c1 c2 c3 in
         if v > 255 then (
           let { pos_lnum; pos_bol; pos_cnum; _ } = lexeme_end_p lexbuf in
           let msg =
@@ -211,7 +167,7 @@ and scan_quoted buf start = parse
       }
   | '\\' 'x' (hexdigit as c1) (hexdigit as c2)
       {
-        let v = hex_code c1 c2 in
+        let v = SmtMisc.hex_code c1 c2 in
         Buffer.add_char buf (Char.chr v);
         scan_quoted buf start lexbuf
       }
@@ -223,8 +179,8 @@ and scan_quoted buf start = parse
       }
   | lf
       {
-        found_newline lexbuf 0;
-        Buffer.add_char buf lf;
+        SmtMisc.found_newline lexbuf 0;
+        Buffer.add_char buf SmtMisc.lf;
         scan_quoted buf start lexbuf
       }
   | ([^ '\\' '|'] # lf)+
@@ -244,7 +200,7 @@ and scan_quoted buf start = parse
 
 and scan_block_comment buf locs = parse
   | ('#'* | '|'*) lf
-      { found_newline lexbuf 0; scan_block_comment buf locs lexbuf }
+      { SmtMisc.found_newline lexbuf 0; scan_block_comment buf locs lexbuf }
   | (('#'* | '|'*) [^ '"' '#' '|'] # lf)+ { scan_block_comment buf locs lexbuf }
   | ('#'* | '|'*) '"'
       {