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

Re: help with a typechecking error message




Mark -

> where n is some natural below 128.  Is that right?  It would be nice if
> there were single quote character terms--'A', 'a', 'B', 'b',... correlated
> to strings in the expected way, so that, for example,
> 
> 	char2stringA: lemma 'A' = seq("A")(0)


The parser doesn't support input of single characters like that
at the moment (and I'm not sure it is worth adding).  Just use
double quotes and let the typechecker insert the conversion
extract1:

 char2stringA : lemma "A" = seq("A")(0)


char2stringA :

  |-------
{1}   extract1("A") = seq("A")(0)

Rule? (grind)
length rewrites length(null)
  to 0
length rewrites length(cons(char(65), null))
  to 1
list2finseq rewrites "A"
  to (# length := 1,
         seq
           := LAMBDA (x: below[length(cons(char(65), null))]):
                nth(cons(char(65), null), x) #)
nth rewrites nth(cons(char(65), null), 0)
  to char(65)
extract1 rewrites
  extract1((# length := 1,
              seq
                := LAMBDA (x: below[length(cons(char(65), null))]):
                     nth(cons(char(65), null), x) #))
  to char(65)
Trying repeated skolemization, instantiation, and if-lifting,
Q.E.D.



The conversion "extract1" is defined in the prelude as:

  extract1(fs:{fs | fs`length = 1}): T = fs`seq(0)

  CONVERSION extract1

in the finite sequences theory (the strange ` is the new (alternative) PVS
2.3 syntax for record and projection accessors).  Strings in PVS are
finite sequences of characters.

Hope that helps,
Dave

---
Dr Dave Stringer-Calvert, Sr. Systems Admin, Computer Science Laboratory
SRI International, 333 Ravenswood Avenue, Menlo Park, CA 94025-3493, USA
Phone: (650) 859-3291 Fax: (650) 859-2844 David.Stringer-Calvert@sri.com