Skip to content

Instantly share code, notes, and snippets.

@jimwhite

jimwhite/proteins.lisp

Last active August 16, 2025 19:18
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save jimwhite/d987e669d567a48c92e8105523f625bc to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save jimwhite/d987e669d567a48c92e8105523f625bc to your computer and use it in GitHub Desktop.
Download ZIP
Raw
proteins.lisp
(include-book "centaur/fty/top" :dir :system)
;;; https://github.com/acl2/acl2/tree/master/books/centaur/fty
;;; FTY introduced in *Fix Your Types* by Swords & Davis at 2015 ACL2 workshop - https://arxiv.org/abs/1509.06079
;;; A bigger type book which includes FTY: https://github.com/acl2/acl2/tree/master/books/coi/types
(fty::defprod protein
((name stringp)
(description stringp)
(source symbolp) ;; e.g., 'milk, 'plant
(dose natp))
)
(fty::deflist protein-list
:elt-type protein
)
(defthm get-dose-of-protein-nonneg
(<= 0 (protein->dose x)))
(defconst *whey*
(protein "Whey"
"Milk-derived, fast absorption"
'milk
25))
(fty::deftypes supplement-ontology
(fty::defprod supplement
((name stringp)
(effect stringp)))
(fty::deftagsum supplement-or-protein
(:protein ((val protein)))
(:supplement ((val supplement)))))
Raw
~failed-out.txt
ACL2 !>(fty::deftypes supplement-ontology
(fty::defprod supplement
((name stringp)
(effect stringp)))
(fty::deftagsum supplement-or-protein
(:protein ((val protein)))
(:supplement ((val supplement)))))
Form: ( TABLE XDOC ...)
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
Form: ( TABLE STD::DEFAULT-HINTS-TABLE ...)
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
Form: ( TABLE STD::DEFAULT-HINTS-TABLE ...)
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
Form: ( TABLE STD::DEFAULT-HINTS-TABLE ...)
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
Form: ( TABLE STD::DEFAULT-HINTS-TABLE ...)
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
Form: ( DEFTHEORY FTY::DEFTYPES-ORIG-THEORY ...)
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
Form: ( DEFTHEORY FTY::DEFTYPES-TYPE-THEORY ...)
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
Form: ( MAKE-EVENT (CONS ...))
Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
Form: ( IN-THEORY (ENABLE ...))
Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
Form: ( DEFLABEL FTY::DEFTYPES-BEFORE-TEMP-THMS ...)
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
Form: ( DEFTHM TMP-DEFTYPES-STRINGP-OF-STR-FIX$INLINE ...)
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
Form: ( MAKE-EVENT (QUOTE ...))
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
Form: ( PROGN (LOCAL ...) ...)
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
Form: ( DEFTHEORY FTY::DEFTYPES-TEMP-THMS ...)
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
ACL2 Warning [Theory] in ( IN-THEORY (DISABLE ...)): The :DEFINITION
rules for the built-in functions DOUBLE-REWRITE, THE-CHECK, CONS-WITH-HINT,
IFF, FROM-DF, WORMHOLE-EVAL, MV-LIST, MINUSP, PLUSP, ZEROP, LISTP,
SYNP, CASE-SPLIT, FORCE, /=, =, RETURN-LAST, NULL, ENDP, ATOM, EQL,
NOT, IMPLIES and EQ are disabled by the theory expression
(DISABLE FTY::DEFTYPES-ORIG-THEORY), but some expansions of their calls
may still occur. See :DOC theories-and-primitives.
ACL2 Warning [Theory] in ( IN-THEORY (DISABLE ...)): The :EXECUTABLE-
COUNTERPART rules for the built-in functions NOT, SYMBOLP,
SYMBOL-PACKAGE-NAME, SYMBOL-NAME, STRINGP, REALPART, RATIONALP, PKG-WITNESS,
PKG-IMPORTS, NUMERATOR, INTERN-IN-PACKAGE-OF-SYMBOL, INTEGERP, IMAGPART,
IF, EQUAL, DENOMINATOR, CONSP, CONS, COERCE, COMPLEX-RATIONALP, COMPLEX,
CODE-CHAR, CHARACTERP, CHAR-CODE, CDR, CAR, <, UNARY-/, UNARY--, BINARY-+,
BINARY-* and ACL2-NUMBERP are disabled by the theory expression
(DISABLE FTY::DEFTYPES-ORIG-THEORY), but some evaluations of their
calls may still occur. See :DOC theories-and-primitives.
Form: ( IN-THEORY (DISABLE ...))
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
Form: ( IN-THEORY (ENABLE ...))
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
Form: ( IN-THEORY (ENABLE* ...))
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
Form: ( TABLE DEFINE ...)
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
Form: ( PROGN)
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
ACL2 Error in ( MUTUAL-RECURSION ( DEFUN SUPPLEMENT-P ...) ...): The
definition of SUPPLEMENT-P does not call any of the other functions
being defined via mutual recursion. The theorem prover will perform
better if you define SUPPLEMENT-P without the appearance of mutual
recursion. See :DOC set-bogus-mutual-recursion-ok to get ACL2 to handle
this situation differently.
Form: ( MUTUAL-RECURSION ( DEFUN SUPPLEMENT-P ...) ...)
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
Form: ( PROGN (LOCAL ...) ...)
Time: 0.03 seconds (prove: 0.00, print: 0.00, other: 0.03)
ACL2 Warning in ( ENCAPSULATE NIL (WITH-OUTPUT :SUMMARY-OFF ...) ...):
The attempted ENCAPSULATE has failed while trying to establish the
admissibility of one of the (local or non-local) forms in the body
of the ENCAPSULATE.
Form: ( ENCAPSULATE NIL (WITH-OUTPUT :SUMMARY-OFF ...) ...)
Time: 0.03 seconds (prove: 0.00, print: 0.00, other: 0.03)
Summary
Form: ( MAKE-EVENT (FTY::DEFTYPES-FN ...))
Rules: NIL
Warnings: Theory
Time: 0.03 seconds (prove: 0.00, print: 0.00, other: 0.03)
ACL2 Error [Failure] in ( MAKE-EVENT (FTY::DEFTYPES-FN ...)): See
:DOC failure.
******** FAILED ********
ACL2 !>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment