Browse thread
Polymorphic recursion
[
Home
]
[ Index:
by date
|
by threads
]
[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: | 2007-04-05 (09:33) |
From: | Roland Zumkeller <roland.zumkeller@g...> |
Subject: | Re: [Caml-list] Polymorphic recursion |
On 04/04/07, Alain Frisch <Alain.Frisch@inria.fr> wrote: > The fact that something is well-typed in Coq does not mean that you can > just translate it to OCaml by adding a few Obj.magic to make the > type-checker happy. As I understand Pierre Letouzey's PhD thesis explains how this can be done. Your example couldn't result from translating a Coq term, since "String.copy", "ref", and "Gc.major" are not part of its formalism (a flavour of lambda calculus with inductive types). > let () = > let x = if ("a" = "b") then Obj.magic 0 else String.copy "abc" in > for i = 0 to 100000 do ignore (ref [1]) done; > Gc.major (); > print_endline x > This code compiled with ocamlopt produces a segfault on my machine. On my machine it prints "$d$d$d$d$d$d$d$d$d$d$d$d$d$d$d" and when compiled with ocamlc "abc". Is this a bug? Roland -- http://www.lix.polytechnique.fr/~zumkeller/