explicitly move and attribute compcert code

bin/modal_expressions_parser.ml

@@ -1,19 +1,7 @@
 open Angstrom
 open UIML.Formulas
 open UIML.Datatypes
-
-(* from compcert ! *)
-let camlstring_of_coqstring (s: char list) =
-  let r = Bytes.create (List.length s) in
-  let rec fill pos = function
-  | [] -> r
-  | c :: s -> Bytes.set r pos c; fill (pos + 1) s
-  in Bytes.to_string (fill 0 s)
-
-let coqstring_of_camlstring s =
-  let rec cstring accu pos =
-    if pos < 0 then accu else cstring (s.[pos] :: accu) (pos - 1)
-  in cstring [] (String.length s - 1)
+open Stringconversion
 
 let is_space =
   function | ' ' | '\t' | '\n' -> true | _ -> false

bin/stringconversion.ml

@@ -0,0 +1,29 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the GNU Lesser General Public License as        *)
+(*  published by the Free Software Foundation, either version 2.1 of   *)
+(*  the License, or  (at your option) any later version.               *)
+(*  This file is also distributed under the terms of the               *)
+(*  INRIA Non-Commercial License Agreement.                            *)
+(*                                                                     *)
+(* *********************************************************************)
+
+let camlstring_of_coqstring (s: char list) =
+  let r = Bytes.create (List.length s) in
+  let rec fill pos = function
+  | [] -> r
+  | c :: s -> Bytes.set r pos c; fill (pos + 1) s
+  in Bytes.to_string (fill 0 s)
+
+
+let coqstring_of_camlstring s =
+  let rec cstring accu pos =
+    if pos < 0 then accu else cstring (s.[pos] :: accu) (pos - 1)
+  in cstring [] (String.length s - 1)
+

bin/uiml_demo.ml

@@ -3,14 +3,7 @@ open UIML.Datatypes
 open UIML.Formulas
 open Js_of_ocaml
 open Modal_expressions_parser
-
-(* from compcert !*)
-let camlstring_of_coqstring (s: char list) =
-  let r = Bytes.create (List.length s) in
-  let rec fill pos = function
-  | [] -> r
-  | c :: s -> Bytes.set r pos c; fill (pos + 1) s
-  in Bytes.to_string (fill 0 s)
+open Stringconversion
 
 let rec string_of_formula ?(classical = false) = function
 | Var v -> camlstring_of_coqstring v