diff options
Diffstat (limited to 'exportclight/ExportClight.ml')
-rw-r--r-- | exportclight/ExportClight.ml | 33 |
1 files changed, 15 insertions, 18 deletions
diff --git a/exportclight/ExportClight.ml b/exportclight/ExportClight.ml index b5877f8b..0e4f1fa3 100644 --- a/exportclight/ExportClight.ml +++ b/exportclight/ExportClight.ml @@ -17,12 +17,10 @@ open Format open Camlcoq -open Datatypes -open Values open AST -open Ctypes +open !Ctypes open Cop -open Clight +open !Clight (* Options, lists, pairs *) @@ -50,15 +48,15 @@ let print_list fn p l = exception Not_an_identifier let sanitize s = - let s' = String.create (String.length s) in + let s' = Bytes.create (String.length s) in for i = 0 to String.length s - 1 do - s'.[i] <- - match s.[i] with + Bytes.set s' i + (match String.get s i with | 'A'..'Z' | 'a'..'z' | '0'..'9' | '_' as c -> c | ' ' | '$' -> '_' - | _ -> raise Not_an_identifier + | _ -> raise Not_an_identifier) done; - s' + Bytes.to_string s' let temp_names : (ident, string) Hashtbl.t = Hashtbl.create 17 @@ -79,7 +77,7 @@ let iter_hashtbl_sorted (h: ('a, string) Hashtbl.t) (f: 'a * string -> unit) = (Hashtbl.fold (fun k d accu -> (k, d) :: accu) h [])) let define_idents p = - iter_hashtbl_sorted + iter_hashtbl_sorted string_of_atom (fun (id, name) -> try @@ -402,14 +400,14 @@ let print_variable p (id, v) = let print_globdef p (id, gd) = match gd with - | Gfun(Internal f) -> print_function p (id, f) - | Gfun(External _) -> () + | Gfun(Clight.Internal f) -> print_function p (id, f) + | Gfun(Clight.External _) -> () | Gvar v -> print_variable p (id, v) let print_ident_globdef p = function - | (id, Gfun(Internal f)) -> + | (id, Gfun(Clight.Internal f)) -> fprintf p "(%a, Gfun(Internal f_%s))" ident id (extern_atom id) - | (id, Gfun(External(ef, targs, tres, cc))) -> + | (id, Gfun(Clight.External(ef, targs, tres, cc))) -> fprintf p "@[<hov 2>(%a,@ @[<hov 2>Gfun(External %a@ %a@ %a@ %a))@]@]" ident id external_function ef typlist targs typ tres callconv cc | (id, Gvar v) -> @@ -529,12 +527,12 @@ let name_function f = let name_globdef (id, g) = match g with - | Gfun(Internal f) -> name_function f + | Gfun(Clight.Internal f) -> name_function f | _ -> () let name_program p = - List.iter name_globdef p.prog_defs - + List.iter name_globdef p.Clight.prog_defs + (* All together *) let print_program p prog = @@ -557,4 +555,3 @@ let print_program p prog = fprintf p "|}.@ "; print_assertions p; fprintf p "@]@." - |