Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from cs.uidaho.edu (actually ted.cs.uidaho.edu !OR! info-hol-request@cs.uidaho.edu) 
          by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk;
          Wed, 7 Jul 1993 02:26:45 +0100
Received: by cs.uidaho.edu (16.6/2.0) id AA24771; Tue, 6 Jul 93 18:14:38 -0700
Sender: info-hol-request@cs.uidaho.edu
Errors-To: info-hol-request@cs.uidaho.edu
Precedence: bulk
Received: from toadflax.cs.ucdavis.edu by cs.uidaho.edu (16.6/2.0) id AA24766;
          Tue, 6 Jul 93 18:14:33 -0700
Received: by toadflax.cs.ucdavis.edu (4.1/UCD.CS.2.3) id AA11787;
          Tue, 6 Jul 93 18:15:02 PDT
Date: Tue, 6 Jul 93 18:15:02 PDT
From: shaw@cs.ucdavis.edu (Rob Shaw)
Message-Id: <9307070115.AA11787@toadflax.cs.ucdavis.edu>
To: info-hol@cs.uidaho.edu
Subject: automatic con(de)structors ?


If I define:

let Vstate_Axiom = define_type 
    `Vstate`
    `Vstate = VSTATE registers memory pc`;;

Is there anyway to get the following automatically? Perhaps something
undocumented in contrib?

let get_regs = new_recursive_definition
    false Vstate_Axiom `get_regs`
   "get_regs (VSTATE regs mem pc) = regs";;

let get_mem = new_recursive_definition
    false Vstate_Axiom `get_mem`
   "get_mem (VSTATE regs mem pc) = mem";;

let get_pc = new_recursive_definition
    false Vstate_Axiom `get_pc`
   "get_pc (VSTATE regs mem pc) = pc";;

Just the obvious destructors corresponding the the type definition.

Rob