[acl2/acl2] df56e5: Case-match handles keywords in patterns. Sys-call...

[GitHub]

Branch: refs/heads/master
Home: https://github.com/acl2/acl2
Commit: df56e5be1059c0bdf8b9f811241fef69f75641ed
https://github.com/acl2/acl2/commit/df56e5be1059c0bdf8b9f811241fef69f75641ed
Author: Matt Kaufmann <matthew.j...@gmail.com>
Date: 2017-04-21 (Fri, 21 Apr 2017)

Changed paths:
M axioms.lisp
M basis-a.lisp
M books/system/doc/acl2-doc.lisp
M doc.lisp

Log Message:
-----------
Case-match handles keywords in patterns. Sys-call no longer call the OS during a proof.

The macro, [case-match], now treats keywords as constants when they
occur in patterns. For example, the following form evaluates to 3
where formerly an error occurred:

(let ((x '(:foo 3)))
(case-match x
((:foo y) y)
(& 17)))

Thanks to Keshav Kini for suggesting this improvement.

When [sys-call] is invoked during a proof, it no longer makes a
(potentially dangerous) call to the operating system. (However,
[sys-call+] continues to do so, which could be useful for computed
hints and clause-processors.) Thanks to Eric Smith for suggesting
this change.

[GitHub]

Branch: refs/heads/testing