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


 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
                                   (CONTEXT *CURRENT-CONTEXT*))
 Thank you in advance for your help,
 Anna Petryk
 Student of Warsaw University, Institute of Informatics
 e-mail: Anna.Petryk@students.mimuw.edu.pl