aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2004-07-14 22:42:41 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2004-07-14 22:42:41 +0000
commit3d95c838af3d648e4c32b0b4402e78bccdfa449f (patch)
tree18d944608fc5b747a6bc67315fb0096e750fb96f /contrib
parentd91b204112bf0c37a9827dc699de24d8d7118c37 (diff)
ajout des unsafeCoerce + 2 bugs haskell
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5904 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib')
-rw-r--r--contrib/extraction/haskell.ml19
-rw-r--r--contrib/extraction/modutil.ml8
2 files changed, 18 insertions, 9 deletions
diff --git a/contrib/extraction/haskell.ml b/contrib/extraction/haskell.ml
index 12f7fbb1a..219ebc011 100644
--- a/contrib/extraction/haskell.ml
+++ b/contrib/extraction/haskell.ml
@@ -27,7 +27,7 @@ let keywords =
[ "case"; "class"; "data"; "default"; "deriving"; "do"; "else";
"if"; "import"; "in"; "infix"; "infixl"; "infixr"; "instance";
"let"; "module"; "newtype"; "of"; "then"; "type"; "where"; "_"; "__";
- "as"; "qualified"; "hiding" ; "unit" ]
+ "as"; "qualified"; "hiding" ; "unit" ; "unsafeCoerce" ]
Idset.empty
let preamble prm used_modules (mldummy,tdummy,tunknown) =
@@ -38,8 +38,10 @@ let preamble prm used_modules (mldummy,tdummy,tunknown) =
str "module " ++ pr_upper_id prm.mod_name ++ str " where" ++ fnl ()
++ fnl() ++
str "import qualified Prelude" ++ fnl() ++
+ str "import qualified GHC.Base" ++ fnl() ++
prlist (fun mp -> str "import qualified " ++ pp_mp mp ++ fnl ()) used_modules
++ fnl () ++
+ str "unsafeCoerce = GHC.Base.unsafeCoerce#" ++ fnl() ++
(if mldummy then
str "__ = Prelude.error \"Logical or arity value used\""
++ fnl () ++ fnl()
@@ -146,7 +148,8 @@ let rec pp_expr par env args =
pp_par par (str "Prelude.error" ++ spc () ++ qs s)
| MLdummy ->
str "__" (* An [MLdummy] may be applied, but I don't really care. *)
- | MLmagic a -> pp_expr par env args a
+ | MLmagic a ->
+ pp_apply (str "unsafeCoerce") par (pp_expr true env [] a :: args)
| MLaxiom -> pp_par par (str "Prelude.error \"AXIOM TO BE REALIZED\"")
and pp_pat env pv =
@@ -210,7 +213,7 @@ let pp_one_ind ip pl cv =
| [] -> (mt ())
| _ -> (str " " ++
prlist_with_sep
- (fun () -> (str " ")) (pp_type true (List.rev pl)) l))
+ (fun () -> (str " ")) (pp_type true pl) l))
in
str (if cv = [||] then "type " else "data ") ++
pp_global (IndRef ip) ++ str " " ++
@@ -249,10 +252,9 @@ let pp_decl mpl =
if is_inline_custom r then mt ()
else
let l = rename_tvars keywords l in
- let l' = List.rev l in
hov 2 (str "type " ++ pp_global r ++ spc () ++
prlist (fun id -> pr_id id ++ str " ") l ++
- str "=" ++ spc () ++ pp_type false l' t) ++ fnl () ++ fnl ()
+ str "=" ++ spc () ++ pp_type false l t) ++ fnl () ++ fnl ()
| Dfix (rv, defs,_) ->
let ppv = Array.map pp_global rv in
prlist_with_sep (fun () -> fnl () ++ fnl ())
@@ -262,7 +264,12 @@ let pp_decl mpl =
| Dterm (r, a, _) ->
if is_inline_custom r then mt ()
else
- hov 0 (pp_function (empty_env ()) (pp_global r) a ++ fnl () ++ fnl ())
+ if is_custom r then
+ hov 0 (pp_global r ++ str " = " ++ str (find_custom r)
+ ++ fnl() ++ fnl ())
+ else
+ hov 0 (pp_function (empty_env ()) (pp_global r) a
+ ++ fnl () ++ fnl ())
let pp_structure_elem mpl = function
| (l,SEdecl d) -> pp_decl mpl d
diff --git a/contrib/extraction/modutil.ml b/contrib/extraction/modutil.ml
index f4b84361a..83e1f0f89 100644
--- a/contrib/extraction/modutil.ml
+++ b/contrib/extraction/modutil.ml
@@ -173,9 +173,11 @@ let ast_iter_references do_term do_cons do_type a =
ast_iter iter a;
match a with
| MLglob r -> do_term r
- | MLcons (i,r,_) -> record_iter_references do_term i; do_cons r
+ | MLcons (i,r,_) ->
+ if lang () = Ocaml then record_iter_references do_term i;
+ do_cons r
| MLcase (i,_,v) as a ->
- record_iter_references do_term i;
+ if lang () = Ocaml then record_iter_references do_term i;
Array.iter (fun (r,_,_) -> do_cons r) v
| _ -> ()
in iter a
@@ -186,7 +188,7 @@ let ind_iter_references do_term do_cons do_type kn ind =
let packet_iter ip p =
do_type (IndRef ip); Array.iteri (fun j -> cons_iter (ip,j+1)) p.ip_types
in
- record_iter_references do_term ind.ind_info;
+ if lang () = Ocaml then record_iter_references do_term ind.ind_info;
Array.iteri (fun i -> packet_iter (kn,i)) ind.ind_packets
let decl_iter_references do_term do_cons do_type =