[1] | 1 | #|
|
---|
| 2 | $Id: cgb-lisp.lisp,v 1.1 2009/01/19 07:44:57 marek Exp $
|
---|
| 3 | *--------------------------------------------------------------------------*
|
---|
| 4 | | Copyright (C) 1994, Marek Rychlik (e-mail: rychlik@math.arizona.edu) |
|
---|
| 5 | | Department of Mathematics, University of Arizona, Tucson, AZ 85721 |
|
---|
| 6 | | |
|
---|
| 7 | | Everyone is permitted to copy, distribute and modify the code in this |
|
---|
| 8 | | directory, as long as this copyright note is preserved verbatim. |
|
---|
| 9 | *--------------------------------------------------------------------------*
|
---|
| 10 | |#
|
---|
| 11 |
|
---|
| 12 | ;;----------------------------------------------------------------
|
---|
| 13 | ;; An example facility
|
---|
| 14 | ;;----------------------------------------------------------------
|
---|
| 15 | ;; It should be run from the CGB-LISP package and the symbols which appear in the variable
|
---|
| 16 | ;; otherwise it will not work because the variable names which appear in strings will not
|
---|
| 17 | ;; be in the same package as the variables appearing in the variable lists; well, this
|
---|
| 18 | ;; would not happen if variable lists were strings as well, but it is the price to pay for
|
---|
| 19 | ;; the convenience of being able to type variable lists quickly.
|
---|
| 20 | ;;----------------------------------------------------------------
|
---|
| 21 |
|
---|
| 22 | (defpackage "CGB-LISP"
|
---|
[40] | 23 | (:use "INFIX" "INFIX-PRINTER" "MAKELIST" "ORDER" "MONOM" "COEFFICIENT-RING" "TERM" "POLY"
|
---|
[1] | 24 | "MODULAR" "MODULAR-POLY" "DIVISION" "PARSE" "PRINTER"
|
---|
| 25 | "POLY-WITH-SUGAR" "GROBNER" "COLORED-POLY" "POLY-GCD" "RAT"
|
---|
| 26 | "RATPOLY" "STRING-GROBNER" "DYNAMICS" "PROVER" "COMMON-LISP"))
|
---|
| 27 |
|
---|
| 28 | (in-package "CGB-LISP")
|
---|
| 29 |
|
---|
| 30 | (defvar *examples*
|
---|
| 31 | '((string-grobner . ((string-grobner "[x^2+y,x-y]" '(x y))
|
---|
| 32 | (string-grobner "[y-x^2,z-x^3]" '(x y z) :order #'grevlex>)))
|
---|
| 33 | (string-grobner-system . ((string-grobner-system "[u*x+y,x+y]" '(x y) '(u))
|
---|
| 34 | (string-grobner-system "[u*x+y,x+y]" '(x y) '(u) :cover '(("[u-1]" "[]")))))
|
---|
| 35 | (string-read-poly . ((string-read-poly "[x^3+3*x^2+3*x+1]" '(x))))
|
---|
| 36 | (string-elimination-ideal . ((string-elimination-ideal "[x^2+y^2-2,x*y-1]" '(x y) 1)))
|
---|
| 37 | (string-ideal-saturation-1 . ((string-ideal-saturation-1 "[x^2*y,y^3]" "x" '(x y))))
|
---|
| 38 | (string-ideal-polysaturation-1 . ((string-ideal-polysaturation-1 "[x^2*y,y^3]" "[x,y]" '(x y))))
|
---|
| 39 | (string-cond . ((string-cond '("[u^2-v]" "[v-1]") '(u v) #'grevlex>)))
|
---|
| 40 | (string-cover . ((string-cover '(("[u^2-v]" "[u]") ("[u+v]" "[]")) '(u v) #'grevlex>)))
|
---|
| 41 | (string-determine . ((string-determine
|
---|
| 42 | "[u*x+y,v*x^2+y^2]"
|
---|
| 43 | '(x y)
|
---|
| 44 | '(u v)
|
---|
| 45 | :cond '("[u,v]" "[v-1]")
|
---|
| 46 | :main-order #'lex>)))
|
---|
| 47 | (parse-string-to-sorted-alist . ((parse-string-to-sorted-alist "x^2+y^3" '(x y) #'grevlex>)
|
---|
| 48 | (parse-string-to-sorted-alist "[x^2+y^3,x-y]" '(x y) #'grevlex>)))
|
---|
| 49 | (translate-statements . ((translate-statements (collinear a b c) (perpendicular a b a c))))
|
---|
| 50 | (translate-theorem . ((translate-theorem
|
---|
| 51 | ((perpendicular A B C D)
|
---|
| 52 | (perpendicular C D E F))
|
---|
| 53 | ((parallel A B E F)
|
---|
| 54 | (identical-points C D)))
|
---|
| 55 | (translate-theorem
|
---|
| 56 | ((perpendicular A B A C)
|
---|
| 57 | (midpoint B C M)
|
---|
| 58 | (midpoint A M O)
|
---|
| 59 | (collinear B H C)
|
---|
| 60 | (perpendicular A H B C))
|
---|
| 61 | ((equidistant M O H O)
|
---|
| 62 | (identical-points B C)
|
---|
| 63 | ))))
|
---|
| 64 | (prove-theorem . ((prove-theorem
|
---|
| 65 | ((perpendicular A B C D)
|
---|
| 66 | (perpendicular C D E F))
|
---|
| 67 | ((parallel A B E F)
|
---|
| 68 | (identical-points C D)))
|
---|
| 69 | (prove-theorem
|
---|
| 70 | ((perpendicular A B A C)
|
---|
| 71 | (midpoint B C M)
|
---|
| 72 | (midpoint A M O)
|
---|
| 73 | (collinear B H C)
|
---|
| 74 | (perpendicular A H B C))
|
---|
| 75 | ((equidistant M O H O)
|
---|
| 76 | (identical-points B C)))
|
---|
| 77 | (prove-theorem
|
---|
| 78 | ((perpendicular A B A C)
|
---|
| 79 | (identical-points B C))
|
---|
| 80 | ((identical-points A B)
|
---|
| 81 | (identical-points A C)))
|
---|
| 82 | (prove-theorem
|
---|
| 83 | ((perpendicular A B A C)
|
---|
| 84 | (identical-points B C))
|
---|
| 85 | ((identical-points A B)
|
---|
| 86 | (real-identical-points A C)))))
|
---|
| 87 | )
|
---|
| 88 | "A list of available examples.")
|
---|
| 89 |
|
---|
| 90 |
|
---|
| 91 | (defun example (symbol &optional (stream t))
|
---|
| 92 | "Run short examples associated with a symbol, which typically is a function name."
|
---|
| 93 | (dolist (e (cdr (assoc symbol *examples*)))
|
---|
| 94 | (run-example e stream))
|
---|
| 95 | (values))
|
---|
| 96 |
|
---|
| 97 | (defun run-example (e stream)
|
---|
| 98 | "Evaluate a single form E and send output to stream STREAM."
|
---|
| 99 | (format stream "~%;;----------------------------------------------------------------")
|
---|
| 100 | (format stream "~%;;")
|
---|
| 101 | (format stream "~%;;~1T~S" e)
|
---|
| 102 | (format stream "~%;;")
|
---|
| 103 | (format stream "~%;;----------------------------------------------------------------~&")
|
---|
| 104 | (let ((counter 0))
|
---|
| 105 | (dolist (val (multiple-value-list (eval e)))
|
---|
| 106 | (format stream "[ RETURN VALUE ~d]-->> ~S~&" (incf counter) val)))
|
---|
| 107 | (values))
|
---|
| 108 |
|
---|
| 109 | (defun all-examples (&optional (stream t))
|
---|
| 110 | "Run all available examples and send output to STREAM."
|
---|
| 111 | (dolist (a *examples*)
|
---|
| 112 | (dolist (e (cdr a))
|
---|
| 113 | (run-example e stream)))
|
---|
| 114 | (values))
|
---|
| 115 |
|
---|
| 116 |
|
---|
| 117 |
|
---|
| 118 |
|
---|