Extraction: allow extracting Ascii.ascii to native Char in Haskell (fix #2515)

 We simply factorize code that was already existing for Ocaml.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14011 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 1 insertions, 27 deletions

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)