[isabelle] Simple with hoarestate and multiple procedures



Hi, 

I currently do some experimentation with AFP/Simpl and tried the
following snipped:

---- 8< ------------------------

hoarestate stspace =
  list :: "ref => ref"
  fini :: ref
  pos :: ref

procedures (imports stspace)
  A(fini :: ref)
  "´fini->´list :== Null"

and

  B(pos :: ref)
  "CALL A(´pos)"

---- 8< ------------------------


Resulting in:

*** Type unification failed
*** Type error in application: Incompatible operand type
*** 
*** Operator:
***   update project_Ref_ref inject_Ref_ref fini_'A_'
***    (K_statefun (lookup project_Ref_ref pos_' (locals s))) ::
***   ('a => 'b) => 'a => 'b
*** Operand:   locals s :: 'c => 'b
*** 
*** At command "procedures".

Is there anything wrong in my Simpl example, or is this a bug in Simpl?

The Isabelle repository and the AFP snapshot are from 2009-09-03.


  Johannes






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.