Received: from scaup.cl.cam.ac.uk by Steve.CL.Cam.AC.UK with SMTP/TCP/IP over Ethernet id a024674; 28 Oct 88 22:58 BST Via: uk.ac.ucl.cs.nss; 28 Oct 88 21:56 GMT (UK.AC.Cam.Cl.scaup) Received: from clover.ucdavis.edu by NSS.Cs.Ucl.AC.UK via Satnet with SMTP id aa06623; 28 Oct 88 22:38 BST Received: from [192.12.5.63] by clover.ucdavis.edu (5.59/UCD.EECS.1.1) id AA26225; Fri, 28 Oct 88 09:01:38 PDT Received: from cam.sri.com (cambridge) by drakes.ai.sri.com (3.2/4.16) id AA24429 for info-hol@clover.ucdavis.edu; Fri, 28 Oct 88 09:10:07 PDT Received: from gwyndir.cam.sri.com by cam.sri.com (3.2/4.16) id AA06691 for info-hol@clover.ucdavis.edu; Fri, 28 Oct 88 17:06:55 BST Received: by gwyndir.cam.sri.com (3.2/4.16) id AA01015 for info-hol@clover.ucdavis.edu; Fri, 28 Oct 88 17:06:51 BST Date: Fri, 28 Oct 88 17:05 BST From: Mike Gordon To: info-hol@edu.ucdavis.clover Subject: HOL88 Message-Id: Sender: mjcg Status: RO |============================| | | | HOL88 PROGRESS REPORT | | ---------------------- | | | | Mike Gordon | | Cambridge, 28 Oct 1988 | | | |============================| Here are some more features that will be in Version 1 HOL88. Please mail me any comments or complaints. Form feeds now skipped ---------------------- Files changed: lisp/hol-pars.l lisp/F-parser.l lisp/F-constants.l Form feed (^L, ascii 12) has been added (at RSRE's request) to the list of characters treated as separators (i.e. like spaces). The complete list of such characters (with ascii codes in brackets) is: space (32), carriage return (13), line feed (10), tab (9), form feed (12) Form feeds can be included inside ML strings (tokens) with \F. For example, `\F\F` is a string with two form feeds. More flexible lexical structure ------------------------------- Files changed: lisp/F-parser.l lisp/hol-pars.l An identifier in ML or HOL can be of two forms: (i) A sequence of alphanumerics (i.e. letters, digits, primes or underbars) starting with a letter. (ii) A special symbol (e.g. +, <, /\, ==>, ? etc.) It is a consequence of the way lexical analysis is done that any initial subsequence of a special symbol is also a special symbol (e.g. since ==> is a special symbol, so are == and =). The following functions provide some crude access and control over the lexical structure of HOL and ML. new_letter : string -> () Makes a new character behave like a letter. For example: new_letter `+`;; will make +int and foo+bar become an allowable names. Failure occurs if the argument string is longer than one character. is_letter : string -> bool Tests if a unit string is a letter; fails if the string has more than one character. new_alphanum : string -> () Makes a new character behave like an alphanumeric. For example: new_alphanum `+`;; will make foo+bar and foo+ become allowable names (but not +bar). Failure occurs if the argument string is longer than one character. is_alphanum : string -> bool Tests if a unit string is an alphanumeric; fails if the string has more than one character. new_special_symbol : string -> bool Makes the argument string, and all its substrings, special symbols; fails if (i) the argument string is a single character, or (ii) starts with a letter or alphanumeric. For example: new_allowable_symbol `===>>>`;; makes ===>>>, ===>>, ===> and === into new special symbols (== is already a special symbol because ==> is). special_symbols : void -> string list Gives the list of currently declared special symbols. Sections have gone ------------------ Files changed: lisp/F-parsml.l ML sections, which were buggy and not much used, have been deleted from HOL88. I will debug and restore them if there is an outcry!