Email Gateway (Aug 18 2022 at 14:05): Email Gateway (Aug 18 2022 at 14:05):From: Johannes Hölzl <hoelzl@in.tum.de>
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
Email Gateway (Aug 18 2022 at 14:05):From: Norbert Schirmer <schirmer@in.tum.de>
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
Last updated: Apr 24 2024 at 08:20 UTC