aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--plugins/extraction/common.ml34
-rw-r--r--plugins/extraction/common.mli11
-rw-r--r--plugins/extraction/haskell.ml1
-rw-r--r--plugins/extraction/ocaml.ml28
4 files changed, 47 insertions, 27 deletions
diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
index 8b0b5338a..35873f5a9 100644
--- a/plugins/extraction/common.ml
+++ b/plugins/extraction/common.ml
@@ -547,4 +547,38 @@ let pp_module mp =
add_visible (Mod,s) l; s
| _ -> pp_ocaml_gen Mod mp (List.rev ls) None
+(** 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 mk_ind path s =
+ make_mind (MPfile (dirpath_of_string path)) empty_dirpath (mk_label s)
+
+let ind_ascii = mk_ind "Coq.Strings.Ascii" "ascii"
+
+let check_extract_ascii () =
+ try
+ let char_type = match lang () with
+ | Ocaml -> "char"
+ | Haskell -> "Char"
+ | _ -> raise Not_found
+ in
+ find_custom (IndRef (ind_ascii,0)) = char_type
+ with Not_found -> false
+
+let is_list_cons l =
+ List.for_all (function MLcons (_,ConstructRef(_,_),[]) -> true | _ -> false) l
+
+let is_native_char = function
+ | MLcons(_,ConstructRef ((kn,0),1),l) ->
+ kn = ind_ascii && check_extract_ascii () && is_list_cons l
+ | _ -> false
+
+let pp_native_char c =
+ let rec cumul = function
+ | [] -> 0
+ | MLcons(_,ConstructRef(_,j),[])::l -> (2-j) + 2 * (cumul l)
+ | _ -> assert false
+ in
+ let l = match c with MLcons(_,_,l) -> l | _ -> assert false in
+ str ("'"^Char.escaped (Char.chr (cumul l))^"'")
diff --git a/plugins/extraction/common.mli b/plugins/extraction/common.mli
index 7fc3279af..1d8fe77ab 100644
--- a/plugins/extraction/common.mli
+++ b/plugins/extraction/common.mli
@@ -60,3 +60,14 @@ type reset_kind = AllButExternal | Everything
val reset_renaming_tables : reset_kind -> unit
val set_keywords : Idset.t -> unit
+
+(** For instance: [mk_ind "Coq.Init.Datatypes" "nat"] *)
+
+val mk_ind : string -> string -> mutual_inductive
+
+(** 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 *)
+
+val is_native_char : ml_ast -> bool
+val pp_native_char : ml_ast -> std_ppcmds
diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml
index ef8a1f9b4..ffb3baf4a 100644
--- a/plugins/extraction/haskell.ml
+++ b/plugins/extraction/haskell.ml
@@ -137,6 +137,7 @@ let rec pp_expr par env args =
spc () ++ hov 0 pp_a2)))
| MLglob r ->
apply (pp_global Term r)
+ | MLcons _ as c when is_native_char c -> assert (args=[]); pp_native_char c
| MLcons (_,r,[]) ->
assert (args=[]); pp_global Cons r
| MLcons (_,r,[a]) ->
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index d3a6fceed..5bacddb97 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -118,9 +118,6 @@ 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 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
| Tmeta _ | Tvar' _ | Taxiom -> assert false
@@ -158,26 +155,6 @@ let expr_needs_par = function
| MLcase (_,_,pv) -> not (is_ifthenelse pv)
| _ -> 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
@@ -212,10 +189,7 @@ 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 _ as c when is_native_char c -> assert (args=[]); pp_native_char c
| MLcons ({c_kind = Coinductive},r,[]) ->
assert (args=[]);
pp_par par (str "lazy " ++ pp_global Cons r)