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

Re: [PVS-Help] problems with an uncertainty number of parameters in functions

Hi Huangchao,

There is really no difficulty here, as Vars can be instantiated with tuple
types.  Here's an example:

rels: THEORY
 importing predicates
 R1, R2: Predicate[[int, int]]
 S1, S2: Predicate[[real, [int -> int], [real, int]]]

 f: formula
   (R1 and R2)(3, 4)
     and (S1 and S2)(3/5, (lambda (x: int): x + 2), (2/5, 5))
END rels

Of course, you can't say 'R1 and S1', as there is no single type to use
for Vars in the 'and'.

Hope this helps,

huangchao <huangchao@xxxxxxxxxxxxxx> wrote:

> Hi,
> I define a theory about predicates as follows:
> predicates[Vars: TYPE]: THEORY
>      Predicate: TYPE+=[Vars -> boolean]
>      and(p:Predicate, q:Predicate): Predicate = LAMBDA (v: Vars): p(v) and q
> (v)   
> END predicates
> I get a problem on how to use this theory. The number of variables in
> predicates can be different.
> I mean if I define the theory in this way, I can not handle
> the predicates with two or more variables.
> What can I do to it? Is this a wrong way to cope  with predicates?
> Really appreciate!
> Thank you!
> Huangchao
> -----------------------------------------------------------------------------
> huangchao via foxmail