[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [PVS-Help] outfix operators



Hi Rob,

This is obviously a bug.  I'm including a fix below, which you can add
to your ~/.pvs.lisp file (create it if necessary).  I also submitted
your message to the PVS bugs list.

Thanks,
Sam

(defun xt-expr (expr)
  (case (sim-term-op expr)
    (NUMBER-EXPR (xt-number-expr expr))
    (STRING-EXPR (xt-string-expr expr))
    (NAME-EXPR (xt-name-expr expr))
    (LIST-EXPR (xt-list-expr expr))
    ;;(true (xt-true expr))
    ;;(false (xt-false expr))
    (REC-EXPR (xt-rec-expr expr))
    (TUPLE-EXPR (xt-tuple-expr expr))
    (TERM-EXPR (xt-term-expr expr))
    (UNARY-TERM-EXPR (xt-unary-term-expr expr))
    (FIELDEX (xt-fieldex expr))
    (PROJEX (xt-projex expr))
    (FIELDAPPL (xt-fieldappl expr))
    (PROJAPPL (xt-projappl expr))
    ;;(intype (xt-intype expr))
    (COERCION (xt-coercion expr))
    (IF-EXPR (xt-if-expr expr))
    (APPLICATION (xt-application expr))
    (BIND-EXPR (xt-bind-expr expr))
    (NAME-BIND-EXPR (xt-name-bind-expr expr))
    (SET-EXPR (xt-set-expr expr))
    (LET-EXPR (xt-let-expr expr))
    (WHERE-EXPR (xt-where-expr expr))
    (UPDATE-EXPR (xt-update-expr expr))
    ;;(override-expr (xt-override-expr expr))
    (CASES-EXPR (xt-cases-expr expr))
    (COND-EXPR (xt-cond-expr expr))
    (TABLE-EXPR (xt-table-expr expr))
    (SKOVAR (xt-skovar expr))
    (BRACK-EXPR (xt-brack-expr expr))
    (PAREN-VBAR-EXPR (xt-paren-vbar-expr expr))
    (BRACE-VBAR-EXPR (xt-brace-vbar-expr expr))
    (t (error "Unrecognized expr - ~a" expr))))


robert <robert@itee.uq.edu.au> wrote:

> How can I use outfix operators?  The following theory causes 
> 
> "Error: Unrecognized expr -"
> 
> to be output in buffer *Error Output*, and gives me the choice:
> 
> SPC-scroll, I-ignore, K-keep, A-abort sends and keep or B-break:
> 
> The theory is:
> 
> test_thy: THEORY
> BEGIN
> 
> 	{||}: [int -> int] = (lambda (n: int): n+n)
> 
> 	six: int = {| 3 |}
> 	six2: int = {| 3 |}
> 
> 
> END test_thy
> 
> Using {||} as a prefix operator appears to work fine
> 
> Thanks,
> Rob