Return-Path: Delivery-Date: Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Thu, 19 May 1994 12:17:08 +0100 Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA25402; Thu, 19 May 1994 05:00:14 -0600 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: bulk Received: from oberon.inmos.co.uk by leopard.cs.byu.edu with SMTP (1.37.109.8/16.2) id AA25398; Thu, 19 May 1994 05:00:04 -0600 Received: from frogland.inmos.co.uk by oberon.inmos.co.uk; Thu, 19 May 1994 11:59:54 +0100 From: David Shepherd Message-Id: <15134.9405191058@frogland.inmos.co.uk> Subject: Re: converting hol-types to string in hol90.6 To: reetz@ira.uka.de (reetz) Date: Thu, 19 May 1994 11:58:00 +0100 (BST) Cc: info-hol@leopard.cs.byu.edu In-Reply-To: <"i80fs2.ira.880:19.04.94.09.58.43"@ira.uka.de> from "reetz" at May 19, 94 11:58:40 am X-Mailer: ELM [version 2.4 PL20] Content-Type: text Content-Length: 1432 reetz has said: > I wonder about how to convert a hol-type into a string of sml in hol90.6 > based on NJ/SML 0.93. For terms, I write: > > fun term_2_string t = > System.PrettyPrint.pp_to_string 80 pp_term t; ?? Hol_pp_sig already provides val term_to_string : Term.term -> string > Now, I would like to have something like: > > fun type_2_string t = > ... also val type_to_string : Term.Type.hol_type -> string > As far as I could see, pp_type similar to pp_term exists, but it needs > an additional parameter of type :int, which seems to be the ``depth'' > of the hol-type, so I would have to have a closer look into the hol-type > to convert. Does there exists a simpler solution? As you state, this goes via pp_type and uses !Globals.max_print_depth to control depth of the type printing. However, this seems to be by default to -1 -- which means as each loop decrements it and tests against 0 then there is no limit so it should be ok. If you a paranoid that someone will reset !Globals.max_print_depth to something "sensible" then you can always copy the code for type_to_string and stick in an explicit parameter of -1. -------------------------------------------------------------------------- david shepherd: des@inmos.co.uk tel: 0454-616616 x 625 inmos ltd, 1000 aztec west, almondsbury, bristol, bs12 4sq "I am not a nut --- I am a human being."