diff options
Diffstat (limited to 'plugins/extraction/ExtrOcamlString.v')
-rw-r--r-- | plugins/extraction/ExtrOcamlString.v | 38 |
1 files changed, 38 insertions, 0 deletions
diff --git a/plugins/extraction/ExtrOcamlString.v b/plugins/extraction/ExtrOcamlString.v new file mode 100644 index 00000000..3fcd01b0 --- /dev/null +++ b/plugins/extraction/ExtrOcamlString.v @@ -0,0 +1,38 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* Extraction to Ocaml : special handling of ascii and strings *) + +Require Import Ascii String. + +Extract Inductive ascii => char +[ +"(* If this appears, you're using Ascii internals. Please don't *) + (fun (b0,b1,b2,b3,b4,b5,b6,b7) -> + let f b i = if b then 1 lsl i else 0 in + Char.chr (f b0 0 + f b1 1 + f b2 2 + f b3 3 + f b4 4 + f b5 5 + f b6 6 + f b7 7))" +] +"(* If this appears, you're using Ascii internals. Please don't *) + (fun f c -> + let n = Char.code c in + let h i = (n land (1 lsl i)) <> 0 in + f (h 0) (h 1) (h 2) (h 3) (h 4) (h 5) (h 6) (h 7))". + +Extract Constant zero => "'\000'". +Extract Constant one => "'\001'". +Extract Constant shift => + "fun b c -> Char.chr (((Char.code c) lsl 1) land 255 + if b then 1 else 0)". + +Extract Inlined Constant ascii_dec => "(=)". + +Extract Inductive string => "char list" [ "[]" "(::)" ]. + +(* +Definition test := "ceci est un test"%string. +Recursive Extraction test Ascii.zero Ascii.one. +*) |