Return-Path: <john.harrison-request@uk.ac.cam.cl>
Delivery-Date: 
Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0) 
          id <21025-0@swan.cl.cam.ac.uk>; Wed, 8 Jul 1992 15:01:59 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA05174;
          Wed, 8 Jul 92 06:39:23 -0700
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA05169;
          Wed, 8 Jul 92 06:39:01 -0700
Received: from auk.cl.cam.ac.uk by swan.cl.cam.ac.uk with SMTP (PP-6.0) to cl 
          id <20591-0@swan.cl.cam.ac.uk>; Wed, 8 Jul 1992 14:31:34 +0100
To: info-hol@edu.uidaho.cs.ted
Subject: Re: constant name reuse
In-Reply-To: Your message of Tue, 07 Jul 92 22:40:53 -0700. <9207080540.AA09653@maui.cs.ucla.edu>
Date: Wed, 08 Jul 92 14:31:27 +0100
From: John Harrison <John.Harrison@uk.ac.cam.cl>
Message-Id: <"swan.cl.ca.593:08.06.92.13.31.37"@cl.cam.ac.uk>


Although you can't redefine constant names as constants, it *is* possible to
use constant names as variables. One can use explicit term constructors, or
hide constant names from the quotation parser with "hide_constant", e.g.

  #"\S. S + 1";;
  bad variable structure in quotation
  skipping: 1 " ;; parse failed

  #hide_constant `S`;;
  () : void

  #"\S. S + 1";;
  "\S. S + 1" : term

  #unhide_constant `S`;;
  () : void

  #"\S. S + 1";;
  bad variable structure in quotation
  skipping: 1 " ;; parse failed

As for having several constants with the same name, Konrad's solution seems
quite attractive. You can simulate this to some extent in the current HOL88 by
giving constants long unique names, e.g. prefixing them with the theory name,
then just use interface maps. This is rather crude, and doesn't address
overloading, but I have used this in a new version of the "wellorder" library
to define some notation that people might want to redefine. Here are the
functions to set and unset the interface maps:

  let set_wo_map,unset_wo_map =
    let extras =
     [`subset`,`wo_subset`;
      `Union`,`wo_Union`;
      `fl`,`wo_fl`;
      `poset`,`wo_poset`;
      `chain`,`wo_chain`;
      `woset`,`wo_woset`;
      `inseg`,`wo_inseg`] in
    (\():void. do set_interface_map(union (interface_map()) extras)),
    (\():void. do set_interface_map(subtract (interface_map()) extras));;

This amounts to hacking in a simple version of Konrad's solution, without
addressing overloading.

John.