Stream: Beginner Questions

Topic: Controlling OCaml code export


view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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: Mar 29 2024 at 12:28 UTC