[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
- To: email@example.com
- Subject: help
- From: Anna Petryk <firstname.lastname@example.org>
- Date: Fri, 14 Apr 2000 12:29:44 +0200 (CEST)
- Delivery-Date: Fri Apr 14 03:33:29 2000
- In-Reply-To: <Pine.ULT.email@example.com>
I would be very grateful if you could help me to solve my problem.
As part of my Master Thesis I want to write an application-specific
strategy for PVS.
Inside this strategy, I need to construct my
own PVS expressions. But to use several functions from PVS package
(for example a gensubst function - used to apply substitutions to
these expressions need to be correctly
typed and "resolved" i.e. fields RESOLUTION and TYPE have to be non-nil.
It is not enough for me to use function pc-typecheck and pc-parse because
I use expressions like (: :) of type list[T], which are polymorphic.
In every situation I know exactly the type (or an instance of this type)
of the expression I want to create.
Is there a possibility to obtain a resolution for a variable or constant
using function resolve, knowing the instance of a parametrized theory
where these constants or variables are declared?
What parameters do I have do apply to this function to get the
right resolution? What values can be applied to the argument kind
(I know only two of them: 'type and 'formula)?
What is the meaning of the argument ARGS?
The function takes arguments (NAME
Thank you in advance for your help,
Student of Warsaw University, Institute of Informatics