Alex Weisberger (Sep 16 2022 at 21:16): Alex Weisberger (Sep 16 2022 at 21:16):When exporting constants to OCaml, I'm seeing that the corresponding type definitions that a function operates on are serialized to OCaml within a module. In the case of datatype, this means that the datatype constructors aren't accessible outside of the module.
Here's what I mean:
theory CodeTest
imports Main
begin
datatype color = Red | Green
definition "is_red c = (case c of Red ⇒ True | _ ⇒ False)"
export_code is_red in OCaml
end
This is the theory in Isabelle, and here's the generate OCaml code:
module CodeTest : sig
type color
val is_red : color -> bool
end = struct
type color = Red | Green;;
let rec is_red c = (match c with Red -> true | Green -> false);;
end;; (*struct CodeTest*)
type color in the module signature means that some code outside of the CodeTest module can't create values of that type.
I've found a good amount of documentation of the code generation process, but can't find anything about this specific scenario. Is this something that I'd need to write custom code equations for, or is there some configuration that could control this?
Simon Roßkopf (Sep 16 2022 at 21:44):I am not sure if there is a nicer solution, but usually export one constructor of the datatype. This leads to the type being part of the signature
Simon Roßkopf (Sep 16 2022 at 21:52):There is also the keyword open (export open ..., See chapter 13 in the isar-ref), but that leads to exposing everything in the modules.
Alex Weisberger (Sep 17 2022 at 01:58):Exporting one of the constructors works perfectly, and makes enough sense that I have no problem doing that. That solves my problem exactly. Thanks!
Last updated: Dec 21 2024 at 16:20 UTC