Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
From: Konrad Slind <slind@informatik.tu-muenchen.de>
To: info-hol@cs.uidaho.edu
In-Reply-To: <"swan.cl.cam.:035350:940315120118"@cl.cam.ac.uk> (message from Richard Boulton on Tue, 15 Mar 1994 13:01:05 +0100)
Subject: Re: HOL90 - Syntax
Message-Id: <94Mar15.152423met.8111@sunbroy14.informatik.tu-muenchen.de>
Date: Tue, 15 Mar 1994 15:24:21 +0100


Richard has made a comparison between a couple of fragments of code that
shows how ugly and uncompact the use of records can be. However, I don't
find either example to be terribly attractive. With the definition of
some simple infix operators, the code becomes more readable no matter
what the underlying types:

    infixr -->;
    infix @;
    fun (ty1 --> ty2) = mk_type{Tyop = "fun", Args = [ty1,ty2]};
    fun (tm1 @ tm2) = mk_comb{Rator = tm1, Rand = tm2};
				    
(* Records *)
    fun mk_arith_op tok ftok =
       let val num = mk_type{Tyop = "num",Args = []}
           val arith_op = mk_const{Name = tok, Ty = num --> num --> num}
       in
       (fn {lhs,rhs} => arith_op @ lhs @ rhs handle _ => failwith ftok)
       end;

(* Paired *)
    fun mk_arith_op tok ftok =
       let val num = mk_type("num",[])
           val arith_op = mk_const(tok, num --> num --> num)
       in
       (fn (lhs,rhs) => arith_op @ lhs @ rhs handle _ => failwith ftok)
       end;

Perhaps "@" and "-->" should be in the base system.

I agree with Richard's point about the clumsiness of the non-uniform way
that records need to be broken down. But maybe that is good, for reading
complicated term manipulation code?

Konrad.