From 917e40d0468ef7ce1d4dda9e412b0dbf4cff0bc7 Mon Sep 17 00:00:00 2001
From: Chantal Keller <Chantal.Keller@lri.fr>
Date: Mon, 7 Jun 2021 14:29:45 +0200
Subject: Lia + factorize code

---
 src/trace/smtMisc.ml | 47 +++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 47 insertions(+)

(limited to 'src/trace/smtMisc.ml')

diff --git a/src/trace/smtMisc.ml b/src/trace/smtMisc.ml
index 165814b..67c705f 100644
--- a/src/trace/smtMisc.ml
+++ b/src/trace/smtMisc.ml
@@ -56,3 +56,50 @@ type logic = SL.t
 let rec filter_map f = function
   | [] -> []
   | x::xs -> match f x with Some x -> x::(filter_map f xs) | None -> filter_map f xs
+
+
+(** Lexing *)
+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 (lexbuf:Lexing.lexbuf) diff =
+  lexbuf.Lexing.lex_curr_p <-
+    {
+      lexbuf.Lexing.lex_curr_p with
+      Lexing.pos_lnum = lexbuf.Lexing.lex_curr_p.Lexing.pos_lnum + 1;
+      Lexing.pos_bol = lexbuf.Lexing.lex_curr_p.Lexing.pos_cnum - diff;
+    }
+
+(* same length computation as in [Lexing.lexeme] *)
+let lexeme_len { Lexing.lex_start_pos; Lexing.lex_curr_pos; _ } = lex_curr_pos - lex_start_pos
+
+let main_failure lexbuf msg =
+  let { Lexing.pos_lnum; Lexing.pos_bol; Lexing.pos_cnum; Lexing.pos_fname = _ } = Lexing.lexeme_start_p lexbuf in
+  let msg =
+    Printf.sprintf
+      "Sexplib.Lexer.main: %s at line %d char %d"
+      msg pos_lnum (pos_cnum - pos_bol)
+  in
+  failwith msg
-- 
cgit