#|
Many library primitives are implemented in Scheme here for efficiency.
(http://www.cs.utexas.edu/users/moore/acl2/v3-0/PROGRAMMING.html)
|#
#ci
(module acl2-prims-scheme mzscheme
  (require (lib "contract.ss")
           (prefix srfi: (lib "1.ss" "srfi"))
           (file "../constants.ss")
           (file "../nil-macros.ss"))
  (require-for-syntax "../checking-proc.ss")
  (require (only "../acl2-app.ss" acl2-expr))

  (provide dracula-language-symbol dracula-program-symbol)
  (define dracula-language-symbol '|Dracula Language|)
  (define dracula-program-symbol '|Dracula Program|)
  
  ;; Need to make these turn into macros that check for 1st-order usage.
  (define-syntax (define/c stx)
    (syntax-case stx (rename case-lambda)
      [(_ [rename local-id provided-id] contract-expr value-expr)
       (raise-syntax-error #f "define/c without arity" stx)
       #|
       #'(begin (define local-id value-expr)
                (provide/contract [rename local-id provided-id contract-expr]))
       |#
       ]
      
      [(_ id contract-expr function-expr)
       (identifier? #'id)
       #'(begin (provide [rename macro id])
                (define id function-expr)
                (define-syntax macro
                  ;; do this one without checking-proc b/c of variable arity.
                  (lambda (syn)
                    (syntax-case syn ()
                      [(_id x (... ...))
                       #'(acl2-expr
                          ((contract contract-expr id
                                     dracula-language-symbol
                                     dracula-program-symbol)
                           x (... ...)))]
                      [_else 
                       (raise-syntax-error 
                        #f
                        "Functions may only appear in operator position"
                        syn)]))))]
      
      [(_ ([rename local-id provided-id] formals ...) contract-expr body bodies ...)
       (with-syntax ([(formals* ...) (generate-temporaries #'(formals ...))])
         #'(begin (define (local-id formals ...) (begin body bodies ...))
                  (define-syntax macro-id
                    (checking-proc local-id
                                   contract-expr
                                   dracula-language-symbol
                                   dracula-program-symbol
                                   (formals* ...)))
                  (provide [rename macro-id provided-id])))]
      
      [(_ (id formals ...) contract-expr body bodies ...)
       (with-syntax ([(formals* ...) (generate-temporaries #'(formals ...))])
         #'(begin (define (id formals ...) (begin body bodies ...))
                  (define-syntax macro-id
                    (checking-proc id
                                   contract-expr
                                   dracula-language-symbol
                                   dracula-program-symbol
                                   (formals* ...)))
                  (provide [rename macro-id id])))]))
  
  (define-syntax bool->CL
    (syntax-rules ()
      [(_ x) (if x T nil)]))
  
  (define real/rational? rational?)
  (define (acl2-symbol? x) (or (symbol? x) (null? x)))
  (define symbolp/c (flat-named-contract "symbolp" acl2-symbol?))
  
  (define nil/c (flat-named-contract "nil" null?))
  
  (define (acl2-number? x) (number? x))
  (define acl2-number/c (flat-named-contract "acl2-numberp" acl2-number?))
  (define (non-zero-acl2-number? x) (and (acl2-number? x) (not (zero? x))))
  (define (non-zero-real/rational? x) (and (real/rational? x) (not (zero? x))))
  
  (define (eqlable? x)
    (or (acl2-number? x) (acl2-symbol? x) (char? x)))
  (define/c (eqlablep x) (any/c . -> . any) (bool->CL (eqlable? x)))
  (define eqlablep/c (flat-named-contract "eqlablep" eqlable?))
  
  (define/c (eq x y) 
    (([x any/c] [y (if (acl2-symbol? x) any/c symbolp/c)]) . ->r . any)
    (bool->CL (eq? x y)))
  (define/c (eql x y) 
    (([x any/c] [y (if (eqlable? x) any/c eqlablep/c)]) . ->r . any)
    (bool->CL (eqv? x y)))
  (define/c (equal x y) 
    (any/c any/c . -> . any)
    (bool->CL (equal? x y)))
  
  (define-syntax (acl2:* stx)
    (syntax-case stx (acl2:*)
      [(_ args ...) #'(acl2-expr (* args ...))]
      [acl2:* (raise-syntax-error #f "Functions are allowed only in operator position" stx)]))
  (provide [rename acl2:* *])
  
  (define-syntax (acl2:+ stx)
    (syntax-case stx (acl2:+)
      [(_ args ...) #'(acl2-expr (+ args ...))]
      [acl2:+ (raise-syntax-error #f "Functions are allowed only in operator position" stx)]))
  (provide [rename acl2:+ +])
  
  (define acl2:-
    (case-lambda
      [(x) (- x)]
      [(x y) (- x y)]
      ;; arity error detected by macro into which this defn expands.
      ))
  (define-syntax (macro- stx)
    (syntax-case stx ()
      [(_ x) #'(acl2-expr (acl2:- x))]
      [(_ x y) #'(acl2-expr (acl2:- x y))]
      [(_ x ...) (raise-syntax-error 
                  #f 
                  (format "Expects only one or two arguments, but given ~a"
                          (length (syntax->list #'(x ...))))
                  stx)]
      [_else (raise-syntax-error
              #f "Functions are allowed only in operator position" stx)]))
  (provide [rename macro- -])
  
  (provide not-nil)
  
  ;; SYMBOLS
  
  (define/c (symbolp x) (any/c . -> . any)
    (bool->CL (or (symbol? x) (null? x))))
  
  ;; LISTS
  
  (define-syntax (a:list stx)
    (syntax-case stx (a:list)
      [(_ x ...) #'(acl2-expr (list x ...))]
      [a:list (raise-syntax-error #f "Functions can only be used in operator position" stx)]))
  (define-syntax (a:list* stx)
    (syntax-case stx (a:list*)
      [(_ x ...) #'(acl2-expr (list* x ...))]
      [a:list* (raise-syntax-error #f "Functions can only be used in operator position" stx)]))
  (provide [rename a:list list]
           [rename a:list* list*])
  
  (define/c ([rename a:cons cons] x y) [any/c any/c . -> . any] (cons x y))
  
  (define/c make-list
    (case-> [natural-number/c . -> . any]
            [natural-number/c (symbols ':initial-element) any/c . -> . any])
    (case-lambda 
      [(size) (srfi:make-list size nil)]
      [(size :initial-element fill) (srfi:make-list size fill)]))
  
  (define/c (endp x) ((or/c nil/c pair?) . -> . any) (eq x nil))
  (define/c ([rename a:null null] x) (any/c . -> . any) (eq x nil))
  
  (define/c (consp x) (any/c . -> . any) (bool->CL (pair? x)))
  
  (define (true-list? x) (or (null? x) (eq? x 'nil)
                             (and (pair? x) (true-list? (cdr x)))))
  (define/c (true-listp x)
    (any/c . -> . any)
    (bool->CL (true-list? x)))
  
  (define/c ([rename a:car car] x) [(or/c nil/c (cons/c any/c any/c)) . -> . any]
    (if (pair? x) (car x) '()))
  (define/c ([rename a:cdr cdr] x) [(or/c nil/c (cons/c any/c any/c)) . -> . any]
    (if (pair? x) (cdr x) '()))
  
  (define/c (len x) (any/c . -> . any)
    (let loop ([x x] [answer 0]) 
      (if (pair? x) (loop (cdr x) (add1 answer)) answer)))
  
  (define-syntax (acl2:append stx)
    (syntax-case stx (acl2:append)
      [(_ x ...) #'(acl2-expr (append x ...))]
      [acl2:append (raise-syntax-error #f "Functions are only allowed on operator position" stx)]))
  (provide [rename acl2:append append])
  
  (define/c concatenate ;; FIX: this contract is too weak; needs to be ->r
    (case-> [(symbols 'string 'list) . -> . any]
            [((symbols 'string 'list))
             (or/c (listof string?) (listof (listof any/c)))
             . ->* .
             any])
    (case-lambda
      [(result-type) (if (eq? result-type 'list) '() "")]
      [(result-type . args)
       (apply (if (eq? result-type 'list) append string-append) args)]))
  
  (define/c (revappend lst acc) [(listof any/c) any/c . -> . any]
    (if (null? lst)
        acc
        (revappend (cdr lst) (cons (car lst) acc))))
  
  (define/c ([rename acl2-reverse reverse] lst-or-str) 
    [(or/c string? (listof any/c)) . -> . any]
    (if (string? lst-or-str)
        (list->string (revappend (string->list lst-or-str) '()))
        (revappend lst-or-str '())))
  
  ;; SET operations
  (define/c (intersectp-eq x y)
    ((listof acl2-symbol?) (listof acl2-symbol?) . -> . any)
    (cond [(nil? x) nil]
          [(memq (car x) y) t]
          [else (intersectp-eq (cdr x) y)]))
  
  (define/c (intersectp-equal x y)
    ((listof any/c) (listof any/c) . -> . any)
    (cond [(nil? x) nil]
          [(member (car x) y) t]
          [else (intersectp-equal (cdr x) y)]))
  
  (define/c (lognot x)
    [integer? . -> . any]
    (bitwise-not x))
  
  (define/c logand
    (case->
     (-> any/c any)
     (->* [] (listof integer?) any))
    (case-lambda
      [(x) x]
      [args (apply bitwise-and args)]))
  
  (define/c logior
    (case->
     (-> any/c any)
     (->* [] (listof integer?) any))
    (case-lambda
      [(x) x]
      [args (apply bitwise-ior args)]))
  
  (define/c (logorc1 i j)
    [integer? integer? . -> . any]
    (logior (lognot i) j))
  
  (define/c (logorc2 i j)
    [integer? integer? . -> . any]
    (logior i (lognot j)))
  
  (define (binary-logeqv x y) (logand (logorc1 x y) (logorc1 y x)))
  (define/c logeqv
    (case->
     (-> any/c any)
     (->* [] (listof integer?) any))
    (case-lambda
      [() -1]
      [args (srfi:fold binary-logeqv (car args) (cdr args))]))
  
  (define/c logxor
    (case->
     (-> any/c any)
     (->* [] (listof integer?) any))
    (case-lambda
      [(x) x]
      [args (apply bitwise-xor args)]))
  
  (define/c ([rename a:expt expt] x y) [acl2-number? integer? . -> . any]
    (expt x y))
  
  ;; Character Predicates
  (define/c (characterp x) [any/c . -> . any]
    (bool->CL (char? x)))
  (define/c (alpha-char-p x) [char? . -> . any]
    (bool->CL (char-alphabetic? x)))
  (define/c (char-equal c1 c2) [char? char? . -> . any]
    (bool->CL (char-ci=? c1 c2)))
  (define/c (char< c1 c2) [char? char? . -> . any]
    (bool->CL (char<? c1 c2)))
  (define/c (char<= c1 c2) [char? char? . -> . any]
    (bool->CL (char<=? c1 c2)))
  (define/c (char>= c1 c2) [char? char? . -> . any]
    (bool->CL (char>=? c1 c2)))
  (define/c (char> c1 c2) [char? char? . -> . any]
    (bool->CL (char>? c1 c2)))
  
  (define/c (char-code c) [char? . -> . any] (char->integer c))
  (define/c (code-char i) [integer? . -> . any] (integer->char i))
  
  (define/c digit-char-p
    (case-> (char? . -> . any)
            (char? (integer-in 2 36) . -> . any))
    (case-lambda
      [(x) (or (string->number (string x)) nil)]
      [(x base) (or (string->number (string x) base) nil)]))
  
  (define/c (make-character-list chars) [any/c . -> . any]
    (let loop ([chars chars]
               [result '()])
      (cond [(pair? chars) (loop (cdr chars) (cons (if (char? (car chars))
                                                       (car chars)
                                                       (code-char 0))
                                                   result))]
            [else (reverse result)])))
  
  ;; STRINGS
  (define/c (stringp x) [any/c . -> . any] (bool->CL (string? x)))
  
  (define *standard-chars*
    '(#\Newline #\Space #\! #\" #\# #\$
                #\% #\& #\' #\( #\) #\* #\+ #\, #\- #\.
                #\/ #\0 #\1 #\2 #\3 #\4 #\5 #\6 #\7 #\8
                #\9 #\: #\; #\< #\= #\> #\? #\@ #\A #\B
                #\C #\D #\E #\F #\G #\H #\I #\J #\K #\L
                #\M #\N #\O #\P #\Q #\R #\S #\T #\U #\V
                #\W #\X #\Y #\Z #\[ #\\ #\] #\^ #\_ #\`
                #\a #\b #\c #\d #\e #\f #\g #\h #\i #\j
                #\k #\l #\m #\n #\o #\p #\q #\r #\s #\t
                #\u #\v #\w #\x #\y #\z #\{ #\| #\} #\~))
  (define/c (standard-char-p c) [char? . -> . any]
    (if (memq c *standard-chars*) T nil))
  (define (standard-string? s)
    (and (string? s) (andmap (lambda (x) (memq x *standard-chars*)) (string->list s))))
  (define/c (standard-char-listp x) [any/c . -> . any]
    (bool->CL (let loop ([x x])
                (if (pair? x)
                    (and (memq (car x) *standard-chars*)
                         (loop (cdr x)))
                    (null? x)))))
  (define/c (string-equal s1 s2) ;; case insensitive!
    [standard-string? standard-string? . -> . any]
    (bool->CL (string-ci=? s1 s2)))
  (define/c (string< s1 s2) [string? string? . -> . any]
    (let loop ([posn 0]
               [s1 (string->list s1)]
               [s2 (string->list s2)])
      (cond [(null? s1) (if (null? s2) nil posn)]
            [(null? s2) nil]
            [(char<? (car s1) (car s2)) posn]
            [(char=? (car s1) (car s2)) (loop (add1 posn) (cdr s1) (cdr s2))]
            [else nil])))
  (define/c (string<= s1 s2) [string? string? . -> . any]
    (if (string=? s1 s2) (string-length s1) (string< s1 s2)))
  (define/c (string>= s1 s2) [string? string? . -> . any]
    (if (string=? s1 s2) (string-length s1) (string> s1 s2)))
  (define/c (string> s1 s2) [string? string? . -> . any]
    (string< s2 s1))
  
  (define/c (nth n l) (natural-number/c (listof any/c) . -> . any)
    (if (>= n (length l)) nil (list-ref l n)))
  
  (define/c (coerce x result-type)
    (([x (case result-type
           [(list) string?]
           [(string) (listof char?)]
           [else any/c])] ;; 2nd contract will fail in this case
      [result-type (symbols 'list 'string)])
     . ->r . any)
    (case result-type
      [(list) (string->list x)]
      [(string) (list->string x)]))
  
  (define/c (explode-nonnegative-integer n radix rest)
    [natural-number/c (or/c (=/c 2) (=/c 8) (=/c 10) (=/c 16)) any/c . -> . any]
    (append (string->list (number->string n radix)) rest))
  
  ;; Numeric Predicates
  (define/c (acl2-numberp x) [any/c . -> . any]
    (bool->CL (acl2-number? x)))
  (define/c (natp x) [any/c . -> . any]
    (bool->CL (and (integer? x) (<= 0 x))))
  
  (define (complex-rational? val)
    (and (complex? val)
         (let ([real (real-part val)]
               [imag (imag-part val)])
           (and (rational? real)
                (rational? imag)
                (not (zero? imag))))))
  (define/c (complex-rationalp x) [any/c . -> . any] (bool->CL (complex-rational? x)))
  
  (define/c (zp x) [natural-number/c . -> . any] (bool->CL (zero? x)))
  
  (define/c (evenp x) [integer? . -> . any] (bool->CL (even? x)))
  (define/c (oddp x) [integer? . -> . any] (bool->CL (odd? x)))
  
  (define/c (minusp x) [real/rational? . -> . any] (bool->CL (negative? x)))
  (define/c (plusp x) [real/rational? . -> . any] (bool->CL (positive? x)))
  (define/c (posp x) [any/c . -> . any] (bool->CL (and (integer? x) (positive? x))))
  
  (define/c (integerp x) (any/c . -> . any) (bool->CL (integer? x)))
  (define/c (rationalp x) (any/c . -> . any) (bool->CL (rational? x)))
  (define/c (real/rationalp x) (any/c . -> . any) (rationalp x))
  
  (define/c (integer-range-p low high int) (integer? integer? any/c . -> . any)
    (bool->CL (and (integer? int)
                   (<= low int)
                   (< int high))))
  
  (define/c ([rename a:min min] x y) [real/rational? real/rational? . -> . any]
    (min x y))
  (define/c ([rename a:max max] x y) [real/rational? real/rational? . -> . any]
    (max x y))
  
  (define/c (unary-/ x) (non-zero-acl2-number? . -> . any) (/ x))
  
  (define-syntax (macro/ stx)
    (syntax-case stx ()
      [(_ x) #'(acl2-expr (/ x))]
      [(_ num den) #'(acl2-expr (/ num den))]
      [(_ x ...) (raise-syntax-error
                  #f
                  (format "Expected one or two arguments, but got ~a"
                          (length (syntax->list #'(x ...))))
                  stx)]
      [_else (raise-syntax-error
              #f "Functions are allowed only in operator position" stx)]))
  (provide [rename macro/ /])
  
  (define/c (nonnegative-integer-quotient num den)
    (natural-number/c (and/c natural-number/c (>/c 0)) . -> . any)
    (quotient num den))
  
  (define/c ([rename acl2:= =] x y) (acl2-number? acl2-number? . -> . any)
    (bool->CL (= x y)))
  
  (define/c ([rename acl2:< <] x y) [real/rational? real/rational? . -> . any] (bool->CL (< x y)))
  (define/c ([rename acl2:<= <=] x y) [real/rational? real/rational? . -> . any] (bool->CL (<= x y)))
  (define/c ([rename acl2:>= >=] x y) [real/rational? real/rational? . -> . any] (bool->CL (>= x y)))
  (define/c ([rename acl2:> >] x y) [real/rational? real/rational? . -> . any] (bool->CL (> x y)))
  
  (define/c (fix x) [any/c . -> . any] (if (number? x) x 0))
  
  (define/c ([rename acl2:floor floor] num den) [real/rational? non-zero-real/rational? . -> . any]
    (floor (/ num den)))
  
  (define/c (mod i j) [real/rational? non-zero-real/rational? . -> . any]
    (- i (* (acl2:floor i j) j)))
  
  (provide/contract (rename acl2:not not [any/c . -> . any]))
  
  ;; ALISTS
  (define (alist? x)
    (or (null? x)
        (and (pair? x) (pair? (car x)) (alist? (cdr x)))))
  (define/c (alistp x) [any/c . -> . any] (bool->CL (alist? x)))
  
  ;; ORDERINGS
  (define (both pred? x y) (and (pred? x) (pred? y)))
  (define (complex/lex<= c1 c2)
    (let ([x1 (fix c1)]
          [y1 (fix c2)])
      (or (< (real-part x1) (real-part y1))
          (and (= (real-part x1) (real-part y1))
               (< (imag-part x1) (imag-part y1))))))
  (define (atom? x) (not (pair? x)))
  (define/c (alphorder a b) [atom? atom? . -> . any]
    ;(guard (and (atom a) (atom b)))
    (cond [(both rational? a b) (acl2:<= a b)]
          [(both complex-rational? a b) (complex/lex<= a b)]
          [(both char? a b) (bool->CL (char<=? a b))]
          [(both string? a b) (bool->CL (string<=? a b))]
          [(both symbol? a b) (bool->CL (string-ci<=? (symbol->string a) (symbol->string b)))]
          [(both null? a b) T]
          ;; type mismatch convention: rational < complex < char < string < symbol
          [(rational? a) T]
          [(rational? b) nil]
          [(complex-rational? a) T]
          [(complex-rational? b) nil]
          [(char? a) T]
          [(char? b) nil]
          [(string? a) T]
          [(string? b) nil]
          [(symbol? a) T]
          [(null? a) T]
          [else nil]))
  
  
  (define/c ([rename a:second second] x) [(or/c nil/c pair?) . -> . any] (a:cadr x))
  (define/c ([rename a:caar caar] x) [(or/c nil/c pair?) . -> . any] (a:car (a:car x)))
  (define/c ([rename a:cadr cadr] x) [(or/c nil/c pair?) . -> . any] (a:car (a:cdr x)))
  (define/c ([rename a:cdar cdar] x) [(or/c nil/c pair?) . -> . any] (a:cdr (a:car x)))
  (define/c ([rename a:cddr cddr] x) [(or/c nil/c pair?) . -> . any] (a:cdr (a:cdr x)))
  
  (define/c ([rename a:third third] x) [(or/c nil/c pair?) . -> . any] (caddr x))
  (define/c ([rename a:caaar caaar] x) [(or/c nil/c pair?) . -> . any] (a:car (a:caar x)))
  (define/c ([rename a:caadr caadr] x) [(or/c nil/c pair?) . -> . any] (a:car (a:cadr x)))
  (define/c ([rename a:cadar cadar] x) [(or/c nil/c pair?) . -> . any] (a:car (a:cdar x)))
  (define/c ([rename a:caddr caddr] x) [(or/c nil/c pair?) . -> . any] (a:car (a:cddr x)))
  (define/c ([rename a:cdaar cdaar] x) [(or/c nil/c pair?) . -> . any] (a:cdr (a:caar x)))
  (define/c ([rename a:cdadr cdadr] x) [(or/c nil/c pair?) . -> . any] (a:cdr (a:cadr x)))
  (define/c ([rename a:cddar cddar] x) [(or/c nil/c pair?) . -> . any] (a:cdr (a:cdar x)))
  (define/c ([rename a:cdddr cdddr] x) [(or/c nil/c pair?) . -> . any] (a:cdr (a:cddr x)))
  
  (define/c ([rename a:fourth fourth] x) [(or/c nil/c pair?) . -> . any] (cadddr x))
  (define/c ([rename a:caaaar caaaar] x) [(or/c nil/c pair?) . -> . any] (a:car (a:caaar x)))
  (define/c ([rename a:caaadr caaadr] x) [(or/c nil/c pair?) . -> . any] (a:car (a:caadr x)))
  (define/c ([rename a:caadar caadar] x) [(or/c nil/c pair?) . -> . any] (a:car (a:cadar x)))
  (define/c ([rename a:caaddr caaddr] x) [(or/c nil/c pair?) . -> . any] (a:car (a:caddr x)))
  (define/c ([rename a:cadaar cadaar] x) [(or/c nil/c pair?) . -> . any] (a:car (a:cdaar x)))
  (define/c ([rename a:cadadr cadadr] x) [(or/c nil/c pair?) . -> . any] (a:car (a:cdadr x)))
  (define/c ([rename a:caddar caddar] x) [(or/c nil/c pair?) . -> . any] (a:car (a:cddar x)))
  (define/c ([rename a:cadddr cadddr] x) [(or/c nil/c pair?) . -> . any] (a:car (a:cdddr x)))
  
  (define/c ([rename a:cdaaar cdaaar] x) [(or/c nil/c pair?) . -> . any] (a:cdr (a:caaar x)))
  (define/c ([rename a:cdaadr cdaadr] x) [(or/c nil/c pair?) . -> . any] (a:cdr (a:caadr x)))
  (define/c ([rename a:cdadar cdadar] x) [(or/c nil/c pair?) . -> . any] (a:cdr (a:cadar x)))
  (define/c ([rename a:cdaddr cdaddr] x) [(or/c nil/c pair?) . -> . any] (a:cdr (a:caddr x)))
  (define/c ([rename a:cddaar cddaar] x) [(or/c nil/c pair?) . -> . any] (a:cdr (a:cdaar x)))
  (define/c ([rename a:cddadr cddadr] x) [(or/c nil/c pair?) . -> . any] (a:cdr (a:cdadr x)))
  (define/c ([rename a:cdddar cdddar] x) [(or/c nil/c pair?) . -> . any] (a:cdr (a:cddar x)))
  (define/c ([rename a:cddddr cddddr] x) [(or/c nil/c pair?) . -> . any] (a:cdr (a:cdddr x)))
  
  )