Isabelle/HOL translation: record syntax incorrectly translated with multiple constructors and nested record patterns

[lukaszcz]

Example:

type MessagePacket (MessageType : Type) : Type := mkMessagePacket {
  target : Nat;
  mailbox : Maybe Nat;
  message : MessageType;
};

type EnvelopedMessage (MessageType : Type) : Type :=
  mkEnvelopedMessage {
    sender : Maybe Nat;
    packet : MessagePacket MessageType;
  };

type Timer (HandleType : Type): Type := mkTimer {
  time : Nat;
  handle : HandleType;
};

type Trigger (MessageType : Type) (HandleType : Type) :=
  | MessageArrived { envelope : EnvelopedMessage MessageType; }
  | Elapsed { timers : List (Timer HandleType) };

getMessageFromTrigger : {M H : Type} -> Trigger M H -> Maybe M
      | (MessageArrived@{
          envelope := (mkEnvelopedMessage@{
            packet := (mkMessagePacket@{
              message := m })})})
              := just m
      | _ := nothing;

gives

record 'MessageType MessagePacket =
  target :: nat
  mailbox :: "nat option"
  message :: 'MessageType

record 'MessageType EnvelopedMessage =
  sender :: "nat option"
  packet :: "'MessageType MessagePacket"

record 'HandleType Timer =
  time :: nat
  handle :: 'HandleType

datatype ('MessageType, 'HandleType) Trigger
  = MessageArrived "'MessageType EnvelopedMessage" |
    Elapsed "('HandleType Timer) list"

fun target :: "'MessageType MessagePacket \<Rightarrow> nat" where
  "target (| MessagePacket.target = target', MessagePacket.mailbox = mailbox', MessagePacket.message = message' |) =
    target'"

fun mailbox :: "'MessageType MessagePacket \<Rightarrow> nat option" where
  "mailbox (| MessagePacket.target = target', MessagePacket.mailbox = mailbox', MessagePacket.message = message' |) =
    mailbox'"

fun message :: "'MessageType MessagePacket \<Rightarrow> 'MessageType" where
  "message (| MessagePacket.target = target', MessagePacket.mailbox = mailbox', MessagePacket.message = message' |) =
    message'"

fun sender :: "'MessageType EnvelopedMessage \<Rightarrow> nat option" where
  "sender (| EnvelopedMessage.sender = sender', EnvelopedMessage.packet = packet' |) = sender'"

fun packet :: "'MessageType EnvelopedMessage \<Rightarrow> 'MessageType MessagePacket" where
  "packet (| EnvelopedMessage.sender = sender', EnvelopedMessage.packet = packet' |) = packet'"

fun time :: "'HandleType Timer \<Rightarrow> nat" where
  "time (| Timer.time = time', Timer.handle = handle' |) = time'"

fun handle :: "'HandleType Timer \<Rightarrow> 'HandleType" where
  "handle (| Timer.time = time', Timer.handle = handle' |) = handle'"

fun getMessageFromTrigger :: "('M, 'H) Trigger \<Rightarrow> 'M option" where
  "getMessageFromTrigger M H v_2 =
    (case (M, H, v_2) of
       ((| Trigger.envelope = v' |)) \<Rightarrow>
         (case (EnvelopedMessage.packet v') of
            (v'0) \<Rightarrow> Some (MessagePacket.message v'0) |
            _ \<Rightarrow>
              (case (M, H, v_2) of
                 (M', H', v'1) \<Rightarrow> None)) |
       (M', H', v'1) \<Rightarrow> None)"

end