<commit_before>;; This file defines general utilities that are necessary to 
;; connect EXTENDED-SLANG specs with lisp code.
;; The functions here are referenced in code produced by 
;;  Specware4/Languages/MetaSlang/CodeGen/Lisp/SpecToLisp.sw

(defpackage :Specware)
(defpackage :SpecCalc)
(defpackage :List-Spec)
(defpackage :Slang-Built-In)
(defpackage :Assert-Spec)
(in-package :Slang-Built-In)

;; defvar specwareWizard? here (as opposed to def in Monad.sw) 
;; to avoid having CMUCL treat it as a constant, in which case
;; code under the false branch would be optimized away!
(defvar SpecCalc::specwareWizard? nil) ; see Specware4/Languages/SpecCalculus/Semantics/Monad.sw

(defparameter quotient-tag
  (list :|Quotient|))

(defun quotient (r)
  #'(lambda(x)  (vector quotient-tag r x)))

(defun quotient-1-1 (r x)
  (vector quotient-tag r x))

(defun quotient? (x)
  (and (vectorp x)
       (eq (svref x 0) quotient-tag)))

(defun quotient-relation (x)
  (svref x 1))

(defun quotient-element (x)
  (if (quotient? x)
      (svref x 2)
    (error "Expected an equivalence class, but got (presumably) a representative: ~S" x)))

(define-compiler-macro quotient-element (x)
  `(svref ,x 2))

(defun choose ()
  #'(lambda (f) #'(lambda(x) (funcall f (quotient-element x)))))

(defun choose-1 (f)
  #'(lambda(x) (funcall f (quotient-element x))))

(defun choose-1-1 (f x) 
  (funcall f (quotient-element x)))

(define-compiler-macro choose-1-1 (f x)
  `(funcall ,f (quotient-element ,x)))

#|
  
  slang-term-equals
  -----------------
     This function determines equality for lisp expressions that
     are generated from EXT-SLANG terms admitting equality.


     A translated ext-slang term admitting equality can be in one of the
     following forms:

  (vector t1 t2 ... tn)   - a product
  (cons t1 t2)            - a two tuple
  (cons t1 t2) , nil      - an element of a list type
  (list 'Quotient 'fn t)  - an element of a quotient type
  (cons 'Name t)          - an embedding
  atom                    - a string, char, or nat constant.

|#

;;;  (defun slang-term-equals (t1 t2)
;;;     (or 
;;;      (eq t1 t2)
;;;      (cond
;;;        ((null t1) (null t2))
;;;        ((stringp t1) (string= t1 t2))
;;;        ((symbolp t1) (eql t1 t2))
;;;        ((numberp t1) (eq t1 t2))
;;;        ((characterp t1) (eql t1 t2))
;;;  #| 
;;;     Determine equality by calling the quotient 
;;;     operator in the second position 
;;;     |#
;;;        ((and (quotient? t1)
;;;  	    (quotient? t2))
;;;         (funcall 
;;;  	(quotient-relation t1)
;;;  	(quotient-element t1) 
;;;  	(quotient-element t2)))
;;;       
;;;  #|
;;;     Cons cells are equal if their elements are equal too.
;;;  |#
;;;        ((consp t1) 	 
;;;             (and 
;;;  	    (consp t2) 
;;;  	    (slang-term-equals (car t1) (car t2))
;;;  	    (slang-term-equals (cdr t1) (cdr t2))))
;;;  #|
;;;     Two vectors (corresponding to tuple types)
;;;     are equal if all their elements are equal.
;;;  |#
;;;        ((vectorp t1)
;;;             (and 
;;;  	    (vectorp t2)
;;;  	    (let ((dim (array-dimension t1 0)))
;;;  	      (do ((i 0 (+ i 1))
;;;  		   (v-equal t (slang-term-equals (svref t1 i)  (svref t2 i))))
;;;  		  ((or (= i dim) (not v-equal)) v-equal)))))
;;;        (t (progn (format t "Ill formed terms~%") nil))
;;;        )
;;;      )
;;;     )

(defvar *warn-about-questionable-equality?* nil)
(defparameter sf-epsilon (* 10 single-float-epsilon))
(defparameter df-epsilon (* 10 double-float-epsilon))

;;; This is twice as fast as the version above...
(defun slang-term-equals-2 (t1 t2)
  #+sbcl (declare (optimize speed))
  (or (eq t1 t2)
      (typecase t1
        (array (typecase t1
                 (string    (string= t1 t2))
                 (simple-bit-vector (equal t1 t2))
                 (vector    (cond ((and   
                                    ;; (quotient? t1) 
                                    ;; (quotient? t2)
                                    (eq (svref t1 0) quotient-tag)
                                    (vectorp t2)
                                    (eq (svref t2 0) quotient-tag)
                                    )
                                   ;; Determine equality by calling the quotient 
                                   ;; operator in the second position 
                                   (funcall (svref t1 1) ; (quotient-relation t1)
                                            (cons (svref t1 2) ; (quotient-element t1) 
                                                  (svref t2 2) ; (quotient-element t2)
                                                  )))
                                  (t
                                   (and
                                    ;; Two vectors (corresponding to tuple types)
                                    ;; are equal if all their elements are equal.
                                    (vectorp t2)
                                    (let ((dim1 (array-dimension t1 0))
                                          (dim2 (array-dimension t2 0)))
                                      (and (eql dim1 dim2)
                                           (do ((i 0 (+ i 1))
                                                (v-equal t (slang-term-equals-2 (svref t1 i)  (svref t2 i))))<commit_msg>Fix slang-term-equals-2 for vectors of length 0<commit_after>;; This file defines general utilities that are necessary to 
;; connect EXTENDED-SLANG specs with lisp code.
;; The functions here are referenced in code produced by 
;;  Specware4/Languages/MetaSlang/CodeGen/Lisp/SpecToLisp.sw

(defpackage :Specware)
(defpackage :SpecCalc)
(defpackage :List-Spec)
(defpackage :Slang-Built-In)
(defpackage :Assert-Spec)
(in-package :Slang-Built-In)

;; defvar specwareWizard? here (as opposed to def in Monad.sw) 
;; to avoid having CMUCL treat it as a constant, in which case
;; code under the false branch would be optimized away!
(defvar SpecCalc::specwareWizard? nil) ; see Specware4/Languages/SpecCalculus/Semantics/Monad.sw

(defparameter quotient-tag
  (list :|Quotient|))

(defun quotient (r)
  #'(lambda(x)  (vector quotient-tag r x)))

(defun quotient-1-1 (r x)
  (vector quotient-tag r x))

(defun quotient? (x)
  (and (vectorp x)
       (eq (svref x 0) quotient-tag)))

(defun quotient-relation (x)
  (svref x 1))

(defun quotient-element (x)
  (if (quotient? x)
      (svref x 2)
    (error "Expected an equivalence class, but got (presumably) a representative: ~S" x)))

(define-compiler-macro quotient-element (x)
  `(svref ,x 2))

(defun choose ()
  #'(lambda (f) #'(lambda(x) (funcall f (quotient-element x)))))

(defun choose-1 (f)
  #'(lambda(x) (funcall f (quotient-element x))))

(defun choose-1-1 (f x) 
  (funcall f (quotient-element x)))

(define-compiler-macro choose-1-1 (f x)
  `(funcall ,f (quotient-element ,x)))

#|
  
  slang-term-equals
  -----------------
     This function determines equality for lisp expressions that
     are generated from EXT-SLANG terms admitting equality.


     A translated ext-slang term admitting equality can be in one of the
     following forms:

  (vector t1 t2 ... tn)   - a product
  (cons t1 t2)            - a two tuple
  (cons t1 t2) , nil      - an element of a list type
  (list 'Quotient 'fn t)  - an element of a quotient type
  (cons 'Name t)          - an embedding
  atom                    - a string, char, or nat constant.

|#

;;;  (defun slang-term-equals (t1 t2)
;;;     (or 
;;;      (eq t1 t2)
;;;      (cond
;;;        ((null t1) (null t2))
;;;        ((stringp t1) (string= t1 t2))
;;;        ((symbolp t1) (eql t1 t2))
;;;        ((numberp t1) (eq t1 t2))
;;;        ((characterp t1) (eql t1 t2))
;;;  #| 
;;;     Determine equality by calling the quotient 
;;;     operator in the second position 
;;;     |#
;;;        ((and (quotient? t1)
;;;  	    (quotient? t2))
;;;         (funcall 
;;;  	(quotient-relation t1)
;;;  	(quotient-element t1) 
;;;  	(quotient-element t2)))
;;;       
;;;  #|
;;;     Cons cells are equal if their elements are equal too.
;;;  |#
;;;        ((consp t1) 	 
;;;             (and 
;;;  	    (consp t2) 
;;;  	    (slang-term-equals (car t1) (car t2))
;;;  	    (slang-term-equals (cdr t1) (cdr t2))))
;;;  #|
;;;     Two vectors (corresponding to tuple types)
;;;     are equal if all their elements are equal.
;;;  |#
;;;        ((vectorp t1)
;;;             (and 
;;;  	    (vectorp t2)
;;;  	    (let ((dim (array-dimension t1 0)))
;;;  	      (do ((i 0 (+ i 1))
;;;  		   (v-equal t (slang-term-equals (svref t1 i)  (svref t2 i))))
;;;  		  ((or (= i dim) (not v-equal)) v-equal)))))
;;;        (t (progn (format t "Ill formed terms~%") nil))
;;;        )
;;;      )
;;;     )

(defvar *warn-about-questionable-equality?* nil)
(defparameter sf-epsilon (* 10 single-float-epsilon))
(defparameter df-epsilon (* 10 double-float-epsilon))

;;; This is twice as fast as the version above...
(defun slang-term-equals-2 (t1 t2)
  #+sbcl (declare (optimize speed))
  (or (eq t1 t2)
      (typecase t1
        (array (typecase t1
                 (string    (string= t1 t2))
                 (simple-bit-vector (equal t1 t2))
                 (vector    (cond ((and   
                                    ;; (quotient? t1) 
                                    ;; (quotient? t2)
                                    
                                    (> (array-dimension t1 0) 1)
                                    (eq (svref t1 0) quotient-tag)
                                    (vectorp t2)
                                    (> (array-dimension t2 0) 1)
                                    (eq (svref t2 0) quotient-tag)
                                    )
                                   ;; Determine equality by calling the quotient 
                                   ;; operator in the second position 
                                   (funcall (svref t1 1) ; (quotient-relation t1)
                                            (cons (svref t1 2) ; (quotient-element t1) 
                                                  (svref t2 2) ; (quotient-element t2)
                                                  )))
                                  (t
                                   (and
                                    ;; Two vectors (corresponding to tuple types)
                                    ;; are equal if all their elements are equal.
                                    (vectorp t2)
                                    (let ((dim1 (array-dimension t1 0))
                                          (dim2 (array-dimension t2 0)))
                                      (and (eql dim1 dim2)
                                           (do ((i 0 (+ i 1))
                                                (v-equal t (slang-term-equals-2 (svref t1 i)  (svref t2 i))))
{'fraction_non_alphanumeric': 0.13414070444670426, 'fraction_numerical': 0.019413885550522324, 'mean_word_length': 1.5665480427046263, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 5, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 63, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '1786136', 'n_tokens_mistral': 3591, 'n_tokens_neox': 3396, 'n_words': 1041}