;;; Demos for "Whatâ€™s New in the ACL2 System: Versions 8.2 and 8.3".
;;; May 29, 2020
;;; Copyright (C) 2020, Matt Kaufmann
;;; Author: Matt Kaufmann (joint work with J Moore)
;;;;;;;;;; Demo #1 ;;;;;;;;;;
;;; Quoting :doc note-8-3:
#||
Since its earliest years, ACL2 uses evaluation to simplify ground
terms (terms with no free variables). ACL2 would sometimes generate a call of
hide around a term that fails to evaluate because of an attempt to call a
constrained function. Now, that call incorporates a comment saying which
constrained function is responsible for the failure. See comment....
||#
;;; Run the following three events first with acl2-8.2 (thm fails using HIDE
;;; alone), then acl2-8.3 (thm fails using COMMENT), and finally with recent
;;; github version of acl2 (thm succeeds).
(defstub f (x) t)
(defun g (x) (cons x (f x)))
(thm (equal (car (append (g 3) x)) 3))
;;;;;;;;;; Demo #2 ;;;;;;;;;;
;;; Quoting :doc note-8-3:
#||
A new utility, swap-stobjs, does what its name suggests: it swaps stobjs....
||#
(defstobj st1 fld1)
(defstobj st2 fld2 :congruent-to st1)
(defun foo (st1 st2)
(declare (xargs :stobjs (st1 st2)))
(swap-stobjs st1 st2))
(update-fld1 1 st1)
(update-fld2 2 st2)
(foo st1 st2)
(fld1 st1)
(fld2 st2)