From 9ea91721bc97542798da0d6ba9edfa7badf1df81 Mon Sep 17 00:00:00 2001 From: "waldemar%netscape.com" Date: Wed, 12 Jun 2002 00:23:45 +0000 Subject: [PATCH] Added optional test to unique-elt-of --- js2/semantics/Calculus.lisp | 32 +++++++++++++++++++++---------- js2/semantics/CalculusMarkup.lisp | 17 ++++++++++++---- 2 files changed, 35 insertions(+), 14 deletions(-) diff --git a/js2/semantics/Calculus.lisp b/js2/semantics/Calculus.lisp index 2265d76e79e..f06a25669f2 100644 --- a/js2/semantics/Calculus.lisp +++ b/js2/semantics/Calculus.lisp @@ -3655,18 +3655,30 @@ (error "unique-elt-of called on a set with other than one element")) (assert-non-null (nth (integer-length set) keywords))) -; (unique-elt-of ) -; Returns any element of , which must be a nonempty set. -(defun scan-unique-elt-of (world type-env special-form set-expr) +; (unique-elt-of [ ]) +; Returns the one element of , which must have exactly one element. If and are given, +; then return the one element of that satisfies ; there must be exactly one such element. +; may shadow an existing local variable. +(defun scan-unique-elt-of (world type-env special-form set-expr &optional var-source condition-expr) (multiple-value-bind (set-code set-type set-annotated-expr) (scan-set-value world type-env set-expr) (let ((elt-type (set-element-type set-type))) - (values - (ecase (type-kind set-type) - (:list-set (list 'unique-elt-of set-code)) - (:range-set (range-set-out-converter-expr elt-type (list 'range-set-unique-elt-of set-code))) - ((:bit-set :restricted-set) (list 'bit-set-unique-elt-of set-code (list 'quote (set-type-keywords set-type))))) - elt-type - (list 'expr-annotation:special-form special-form set-annotated-expr))))) + (if var-source + (let* ((var (scan-name world var-source)) + (local-type-env (type-env-add-binding type-env var elt-type :const t))) + (multiple-value-bind (condition-code condition-annotated-expr) (scan-typed-value world local-type-env condition-expr (world-boolean-type world)) + (unless (eq (type-kind set-type) :list-set) + (error "Not implemented")) + (values + `(unique-elt-of (remove-if-not #'(lambda (,var) ,condition-code) ,set-code)) + elt-type + (list 'expr-annotation:special-form special-form set-annotated-expr var condition-annotated-expr)))) + (values + (ecase (type-kind set-type) + (:list-set (list 'unique-elt-of set-code)) + (:range-set (range-set-out-converter-expr elt-type (list 'range-set-unique-elt-of set-code))) + ((:bit-set :restricted-set) (list 'bit-set-unique-elt-of set-code (list 'quote (set-type-keywords set-type))))) + elt-type + (list 'expr-annotation:special-form special-form set-annotated-expr)))))) ;;; Vectors or Sets diff --git a/js2/semantics/CalculusMarkup.lisp b/js2/semantics/CalculusMarkup.lisp index 8d3e394e293..8b205545f36 100644 --- a/js2/semantics/CalculusMarkup.lisp +++ b/js2/semantics/CalculusMarkup.lisp @@ -803,11 +803,20 @@ (depict-expression markup-stream world set-annotated-expr %prefix%))) -; (unique-elt-of ) -(defun depict-unique-elt-of (markup-stream world level set-annotated-expr) +; (unique-elt-of [ ]) +(defun depict-unique-elt-of (markup-stream world level set-annotated-expr &optional var condition-annotated-expr) (depict-expr-parentheses (markup-stream level %expr%) - (depict markup-stream "the one element of ") - (depict-expression markup-stream world set-annotated-expr %prefix%))) + (cond + (var + (depict markup-stream "the one element ") + (depict-local-variable markup-stream var) + (depict markup-stream " " :member-10 " ") + (depict-expression markup-stream world set-annotated-expr %term%) + (depict markup-stream " that satisfies ") + (depict-expression markup-stream world condition-annotated-expr %logical%)) + (t + (depict markup-stream "the one element of ") + (depict-expression markup-stream world set-annotated-expr %prefix%))))) ;;; Vectors or Sets