aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2010-06-04 20:19:02 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2010-06-04 20:19:02 +0000
commite5034fbbf23edb17dd88175b2f44b2dc9b4110fa (patch)
treef76a76a5e14b01ba03277757273c7d69bd7649b4 /plugins
parent53f83dbdb371e6efe376e0e7be12f15b2886d707 (diff)
Extraction: attempt to provide nice extraction of chars and strings for Ocaml
When Requiring ExtrOcamlString : * ascii is mapped to Ocaml's char, the ugly translation of constructor and pattern-match should hopefully be seen very rarely (never ?). We add a hack in ocaml.ml for recognizing constant chars. * string is mapped to (list char). Extracting to Ocaml's string could be done, but would be really nasty (lots of non-trivial Extract Constant to add). For now, (list char) seems a good compromise. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13078 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins')
-rw-r--r--plugins/extraction/ExtrOcamlString.v38
-rw-r--r--plugins/extraction/ocaml.ml35
-rw-r--r--plugins/extraction/vo.itarget1
3 files changed, 67 insertions, 7 deletions
diff --git a/plugins/extraction/ExtrOcamlString.v b/plugins/extraction/ExtrOcamlString.v
new file mode 100644
index 000000000..f41d52432
--- /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 => "list char" [ "[]" "(::)" ].
+
+(*
+Definition test := "ceci est un test"%string.
+Recursive Extraction test Ascii.zero Ascii.one.
+*)
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index 137ae9047..39ec20617 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -118,9 +118,8 @@ let find_projections = function Record l -> l | _ -> raise NoRecord
(*s Pretty-printing of types. [par] is a boolean indicating whether parentheses
are needed or not. *)
-let kn_sig =
- let specif = MPfile (dirpath_of_string "Coq.Init.Specif") in
- make_mind specif empty_dirpath (mk_label "sig")
+let mk_ind path s =
+ make_mind (MPfile (dirpath_of_string path)) empty_dirpath (mk_label s)
let rec pp_type par vl t =
let rec pp_rec par = function
@@ -130,11 +129,10 @@ let rec pp_type par vl t =
| Tglob (r,[a1;a2]) when is_infix r ->
pp_par par (pp_rec true a1 ++ str (get_infix r) ++ pp_rec true a2)
| Tglob (r,[]) -> pp_global Type r
+ | Tglob (IndRef(kn,0),l) when kn = mk_ind "Coq.Init.Specif" "sig" ->
+ pp_tuple_light pp_rec l
| Tglob (r,l) ->
- if r = IndRef (kn_sig,0) then
- pp_tuple_light pp_rec l
- else
- pp_tuple_light pp_rec l ++ spc () ++ pp_global Type r
+ pp_tuple_light pp_rec l ++ spc () ++ pp_global Type r
| Tarr (t1,t2) ->
pp_par par
(pp_rec true t1 ++ spc () ++ str "->" ++ spc () ++ pp_rec false t2)
@@ -161,6 +159,25 @@ let expr_needs_par = function
| _ -> false
+(** Special hack for constants of type Ascii.ascii : if an
+ [Extract Inductive ascii => char] has been declared, then
+ the constants are directly turned into chars *)
+
+let ind_ascii = mk_ind "Coq.Strings.Ascii" "ascii"
+
+let check_extract_ascii () =
+ try find_custom (IndRef (ind_ascii,0)) = "char" with Not_found -> false
+
+let is_list_cons l =
+ List.for_all (function MLcons (_,ConstructRef(_,_),[]) -> true | _ -> false) l
+
+let pp_char l =
+ let rec cumul = function
+ | [] -> 0
+ | MLcons(_,ConstructRef(_,j),[])::l -> (2-j) + 2 * (cumul l)
+ | _ -> assert false
+ in str ("'"^Char.escaped (Char.chr (cumul l))^"'")
+
let rec pp_expr par env args =
let par' = args <> [] || par
and apply st = pp_apply st par args in
@@ -195,6 +212,10 @@ let rec pp_expr par env args =
let record = List.hd args in
pp_apply (record ++ str "." ++ pp_global Term r) par (List.tl args)
with _ -> apply (pp_global Term r))
+ | MLcons(_,ConstructRef ((kn,0),1),l)
+ when kn = ind_ascii && check_extract_ascii () & is_list_cons l ->
+ assert (args=[]);
+ pp_char l
| MLcons (Coinductive,r,[]) ->
assert (args=[]);
pp_par par (str "lazy " ++ pp_global Cons r)
diff --git a/plugins/extraction/vo.itarget b/plugins/extraction/vo.itarget
index f7168ff40..338b27684 100644
--- a/plugins/extraction/vo.itarget
+++ b/plugins/extraction/vo.itarget
@@ -3,3 +3,4 @@ ExtrOcamlIntConv.vo
ExtrOcamlBigIntConv.vo
ExtrOcamlNatInt.vo
ExtrOcamlNatBigInt.vo
+ExtrOcamlString.vo \ No newline at end of file