Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools

PVS Bug 448


Synopsis:        Typechecking problem
Severity:        serious
Priority:        medium
Responsible:     owre
State:           analyzed
Class:           sw-bug
Arrival-Date:    Sun Mar 12 12:40:01 2000
Originator:      Kellom{ki Pertti
Organization:    cs.tut.fi
Release:         PVS 2.3
Environment: 
 System:          
 Architecture: 

Description: 
  Hi,
  
  I am developing a deep embedding of DisCo in PVS.
  When trying to typecheck the following file, I get 
  
    Error: No methods applicable for generic function
  
  ----------------------------------------------------------------------
  temporal_expr[id : TYPE]: 
   DATATYPE WITH SUBTYPES temp_expr, DisCo_action, spec
   BEGIN
    IMPORTING bool_expr[id]
  
    box(e: temporal_expr): box?: temp_expr
    DisCo_action(roles: list[id], guard: bool_expr, body:
                 list[assign]): DisCo_action?: DisCo_action
    specification(initial_conditions: list[bool_expr], actions:
                  list[DisCo_action], fields: list[id]): specification?: spec
   END temporal_expr
  ----------------------------------------------------------------------
  
  Dump file containing datatypes bool_expr, int_expr and object_expr 
  follows.
  --
  pertti
  
  ----------------------------------------------------------------------
  %Patch files loaded: patch2 version 1.2.2.36
  
  $$$pvs-strategies
  (defstep my-rewrites ()
    (then (auto-rewrite "suffix")
          (auto-rewrite "TLA_tautology?")
          (auto-rewrite "val2bool")
          ;(auto-rewrite "is_participant")
          (auto-rewrite "variable_assignment")
          (auto-rewrite "variable_assignments")
          (auto-rewrite "val_equal")
          (auto-rewrite "type_preconditions")
          (auto-rewrite "one_role_inequalities")
          (auto-rewrite "role_inequalities")
          (auto-rewrite "role_of_object")
          (auto-rewrite "lift_bool")
  	(auto-rewrite "lift_int"))
    "Install rewrites"
    "Install rewrites")
  
  (defstep dg ()
    (grind ! nil nil ("length" "list2finseq"))
    "DisCo grind"
    "DisCo grind")
  
  $$$bool_expr.pvs
  bool_expr[id: TYPE]: DATATYPE WITH SUBTYPES assign, b_expr
   BEGIN
    IMPORTING int_expr[id], object_expr[id]
  
    forall_q(q_var: id, e: bool_expr): forall_q?: b_expr
    exists_q(q_var: id, e: bool_expr): exists_q?: b_expr
    boolconst(v: bool): boolconst?: b_expr
    bvar_ref(object: id, field: id): bvar_ref?: b_expr
    bpvar_ref(object: id, field: id): bpvar_ref?: b_expr
    AND(e1, e2: bool_expr): and?: b_expr
    OR(e1, e2: bool_expr): or?: b_expr
    IMPLIES(e1, e2: bool_expr): implies?: b_expr
    gt(e1, e2: int_expr): gt?: b_expr
    lt(e1, e2: int_expr): lt?: b_expr
    NOT(e: bool_expr): not?: b_expr
    iequal(e1, e2: int_expr): iequal?: b_expr
    bequal(e1, e2: bool_expr): bequal?: b_expr
    oequal(e1, e2: object_expr): oequal?: b_expr
    unchanged(obj, fld: id): unchanged?: assign
    iassign(obj: id, fld: id, rhs: int_expr): iassign?: assign
    bassign(obj: id, fld: id, rhs: bool_expr): bassign?: assign
   END bool_expr
  
  $$$object_expr.pvs
  object_expr[id : type] : DATATYPE
    BEGIN
      object(name : id) : object?
    END object_expr
  
  $$$int_expr.pvs
  int_expr [id : TYPE] : DATATYPE
    BEGIN
      intconst(v : int) : intconst? 
      ivar_ref(object : id, field: id) : ivar_ref?
      ipvar_ref(object : id, field: id) : ipvar_ref?
      plus(e1, e2 : int_expr) : plus?
      minus(e1, e2 : int_expr) : minus? 
    END int_expr

How-To-Repeat: 

Fix: 
1. Modified save-adt-file to provide information about the generated
   theories
2. Removed an artificial restriction on generating the map theory, that
   was breaking datatypes that imported the restricted datatype.
3. Fixed acc-reduce-selection* (type-name) to get the actuals from the
   supertype rather than from a subtype.
4. Removed no-adt-subtypes function and *no-adt-subtypes* global variable.
5. Modified typecheck-top-level-adt to ensure that proofs (of TCCs) get
   restored.
6. Minor mod to the message in generate-adt-map-theory
7. Modified generate-adt-map to allow mappings over accessors whose type
   involves a subtype of the datatype, and to generate the proper return
   type.
8. Added method mk-map-application (subtype).
9. Added find-adt-subtypes to look for subtypes of the adt within the
   accessor types.  Needed to support 7.

Note some of these fixes have little or nothing to do with the original
bug, but were noticed while debugging.
Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools