acl2-books-certs 6.3-5 / usr / share / acl2-6.3 / books / system / extend-pathname.cert

(IN-PACKAGE "ACL2")
"ACL2 Version 6.3"
:BEGIN-PORTCULLIS-CMDS
:END-PORTCULLIS-CMDS
:EXPANSION-ALIST
((7 RECORD-EXPANSION (VERIFY-TERMINATION REMOVE-AFTER-LAST-DIRECTORY-SEPARATOR) (DEFUN REMOVE-AFTER-LAST-DIRECTORY-SEPARATOR (P) (LET* ((P-REV (REVERSE P)) (POSN (POSITION *DIRECTORY-SEPARATOR* P-REV))) (IF POSN (SUBSEQ P 0 (1- (- (LENGTH P) POSN))) (ER HARD (QUOTE REMOVE-AFTER-LAST-DIRECTORY-SEPARATOR) "Implementation error!  Unable to handle a directory string."))))) (8 RECORD-EXPANSION (VERIFY-TERMINATION MERGE-USING-DOT-DOT) (DEFUN MERGE-USING-DOT-DOT (P S) (COND ((EQUAL P "") S) ((EQUAL S "..") (CONCATENATE (QUOTE STRING) (REMOVE-AFTER-LAST-DIRECTORY-SEPARATOR P) *DIRECTORY-SEPARATOR-STRING*)) ((EQUAL S ".") (CONCATENATE (QUOTE STRING) P *DIRECTORY-SEPARATOR-STRING*)) ((AND (>= (LENGTH S) 3) (EQL (CHAR S 0) #\.) (EQL (CHAR S 1) #\.) (EQL (CHAR S 2) #\/)) (MERGE-USING-DOT-DOT (REMOVE-AFTER-LAST-DIRECTORY-SEPARATOR P) (SUBSEQ S 3 (LENGTH S)))) ((AND (>= (LENGTH S) 2) (EQL (CHAR S 0) #\.) (EQL (CHAR S 1) #\/)) (MERGE-USING-DOT-DOT P (SUBSEQ S 2 (LENGTH S)))) (T (CONCATENATE (QUOTE STRING) P *DIRECTORY-SEPARATOR-STRING* S))))) (9 RECORD-EXPANSION (VERIFY-TERMINATION OUR-MERGE-PATHNAMES) (DEFUN OUR-MERGE-PATHNAMES (P S) (COND ((AND (NOT (EQUAL S "")) (EQL (CHAR S 0) *DIRECTORY-SEPARATOR*)) (ER HARD (QUOTE OUR-MERGE-PATHNAMES) "Attempt to merge with an absolute filename, ~p0.  Please contact the ~
         ACL2 implementors." S)) ((OR (NULL P) (EQUAL P "")) S) ((STRINGP P) (MERGE-USING-DOT-DOT (IF (EQL (CHAR P (1- (LENGTH P))) *DIRECTORY-SEPARATOR*) (SUBSEQ P 0 (1- (LENGTH P))) P) S)) (T (ER HARD (QUOTE OUR-MERGE-PATHNAMES) "The first argument of our-merge-pathnames must be a string, ~
         but the following is not:  ~p0." P))))) (10 RECORD-EXPANSION (VERIFY-TERMINATION DIRECTORY-OF-ABSOLUTE-PATHNAME) (DEFUN DIRECTORY-OF-ABSOLUTE-PATHNAME (PATHNAME) (LET* ((LST (COERCE PATHNAME (QUOTE LIST))) (RLST (REVERSE LST)) (TEMP (MEMBER *DIRECTORY-SEPARATOR* RLST))) (COERCE (REVERSE TEMP) (QUOTE STRING))))) (11 RECORD-EXPANSION (VERIFY-TERMINATION EXPAND-TILDE-TO-USER-HOME-DIR) (DEFUN EXPAND-TILDE-TO-USER-HOME-DIR (STR OS CTX STATE) (COND ((OR (EQUAL STR "~") (AND (< 1 (LENGTH STR)) (EQL (CHAR STR 0) #\~) (EQL (CHAR STR 1) #\/))) (LET ((USER-HOME-DIR (F-GET-GLOBAL (QUOTE USER-HOME-DIR) STATE))) (COND (USER-HOME-DIR (CONCATENATE (QUOTE STRING) USER-HOME-DIR (SUBSEQ STR 1 (LENGTH STR)))) (T (LET ((CERTIFY-BOOK-INFO (F-GET-GLOBAL (QUOTE CERTIFY-BOOK-INFO) STATE))) (PROG2$ (AND (OR CERTIFY-BOOK-INFO (NOT (EQ OS :MSWINDOWS))) (ER HARD CTX "The use of ~~/ for the user home directory ~
                                 in filenames is not supported ~@0." (IF CERTIFY-BOOK-INFO "inside books being certified" "for this host Common Lisp"))) STR)))))) (T STR)))) (12 RECORD-EXPANSION (VERIFY-TERMINATION EXTEND-PATHNAME) (DEFUN EXTEND-PATHNAME (DIR FILE-NAME STATE) (LET* ((OS (OS (W STATE))) (FILE-NAME1 (EXPAND-TILDE-TO-USER-HOME-DIR FILE-NAME OS (QUOTE EXTEND-PATHNAME) STATE)) (ABS-FILENAME (COND ((ABSOLUTE-PATHNAME-STRING-P FILE-NAME1 NIL OS) FILE-NAME1) (T (OUR-MERGE-PATHNAMES DIR FILE-NAME1)))) (CANONICAL-FILENAME (CANONICAL-PATHNAME ABS-FILENAME NIL STATE))) (OR CANONICAL-FILENAME (LET ((LEN (LENGTH ABS-FILENAME))) (ASSERT$ (NOT (EQL LEN 0)) (COND ((EQL (CHAR ABS-FILENAME (1- (LENGTH ABS-FILENAME))) #\/) ABS-FILENAME) (T (LET* ((DIR0 (DIRECTORY-OF-ABSOLUTE-PATHNAME ABS-FILENAME)) (LEN0 (LENGTH DIR0)) (DIR1 (ASSERT$ (AND (NOT (EQL LEN0 0)) (EQL (CHAR DIR0 (1- LEN0)) #\/)) (CANONICAL-PATHNAME DIR0 T STATE)))) (COND (DIR1 (CONCATENATE (QUOTE STRING) DIR1 (SUBSEQ ABS-FILENAME LEN0 LEN))) (T ABS-FILENAME))))))))))))
NIL
(("/usr/share/acl2-6.3/books/system/extend-pathname.lisp" "extend-pathname" "extend-pathname" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 479638026))
1632648717