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

  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
    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 
  %Patch files loaded: patch2 version
  (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[id: TYPE]: DATATYPE WITH SUBTYPES assign, b_expr
    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[id : type] : DATATYPE
      object(name : id) : object?
    END object_expr
  int_expr [id : TYPE] : DATATYPE
      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


1. Modified save-adt-file to provide information about the generated
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
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
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