Re: [isabelle] Simple with hoarestate and multiple procedures



Hi Johannes,

there is some syntax magic going on with global variables (cf. p 715 in the documentation).
The hoarestate has to start with string 'globals', eg. globals_stsspace.


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

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

and

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

   Cheers,

   Norbert

On 18.09.2009, at 09:29, Johannes Hölzl wrote:

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.