diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2007-08-04 07:27:50 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2007-08-04 07:27:50 +0000 |
commit | 355b4abcee015c3fae9ac5653c25259e104a886c (patch) | |
tree | cfdb5b17f36b815bb358699cf420f64eba9dfe25 /caml/Camlcoq.ml | |
parent | 22ff08b38616ceef336f5f974d4edc4d37d955e8 (diff) | |
download | compcert-355b4abcee015c3fae9ac5653c25259e104a886c.tar.gz compcert-355b4abcee015c3fae9ac5653c25259e104a886c.zip |
Fusion des modifications faites sur les branches "tailcalls" et "smallstep".
En particulier:
- Semantiques small-step depuis RTL jusqu'a PPC
- Cminor independant du processeur
- Ajout passes Selection et Reload
- Ajout des langages intermediaires CminorSel et LTLin correspondants
- Ajout des tailcalls depuis Cminor jusqu'a PPC
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@384 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'caml/Camlcoq.ml')
-rw-r--r-- | caml/Camlcoq.ml | 45 |
1 files changed, 26 insertions, 19 deletions
diff --git a/caml/Camlcoq.ml b/caml/Camlcoq.ml index c2115dfb..ec2447fa 100644 --- a/caml/Camlcoq.ml +++ b/caml/Camlcoq.ml @@ -41,7 +41,7 @@ let z_of_camlint n = let coqint_of_camlint : int32 -> Integers.int = z_of_camlint -(* Strings *) +(* Atoms (positive integers representing strings) *) let atom_of_string = (Hashtbl.create 17 : (string, positive) Hashtbl.t) let string_of_atom = (Hashtbl.create 17 : (positive, string) Hashtbl.t) @@ -69,24 +69,6 @@ let rec coqlist_iter f = function Coq_nil -> () | Coq_cons(a,l) -> f a; coqlist_iter f l -(* Helpers *) - -let rec list_iter f = function - [] -> () - | a::l -> f a; list_iter f l - -let rec list_memq x = function - [] -> false - | a::l -> a == x || list_memq x l - -let rec list_exists p = function - [] -> false - | a::l -> p a || list_exists p l - -let rec list_filter p = function - [] -> [] - | x :: l -> if p x then x :: list_filter p l else list_filter p l - let rec length_coqlist = function | Coq_nil -> 0 | Coq_cons (x, l) -> 1 + length_coqlist l @@ -100,6 +82,31 @@ let array_of_coqlist = function | Coq_cons(hd, tl) -> a.(i) <- hd; fill (i + 1) tl in fill 1 tl +(* Strings *) + +let char_of_ascii (Ascii.Ascii(a0, a1, a2, a3, a4, a5, a6, a7)) = + Char.chr( (if a0 then 1 else 0) + + (if a1 then 2 else 0) + + (if a2 then 4 else 0) + + (if a3 then 8 else 0) + + (if a4 then 16 else 0) + + (if a5 then 32 else 0) + + (if a6 then 64 else 0) + + (if a7 then 128 else 0)) + +let coqstring_length s = + let rec len accu = function + | CString.EmptyString -> accu + | CString.CString(_, s) -> len (accu + 1) s + in len 0 s + +let camlstring_of_coqstring s = + let r = String.create (coqstring_length s) in + let rec fill pos = function + | CString.EmptyString -> r + | CString.CString(c, s) -> r.[pos] <- char_of_ascii c; fill (pos + 1) s + in fill 0 s + (* Timing facility *) (* |