Re: [isabelle] code_include SML and eval



Florian Haftmann schrieb:
Hi Peter,

Actually, the structure contains a
functional array implementation
(using ML-references to store chains of undo-information for old
versions of the array) similar to Haskells Array.Diff package.

One possibility (not very convinving) is to leave everything outside the
structure.  But I guess there is a more direct way:  are your functional
arrays functional in the sense that from outside they behave functional?
Yes, exactly that.
  Then it would be feasible to implement them functionally in HOL,
together with some code_consts directives which implement some
operations destructively.

Ok, then I still need a trick how to include the
 datatype 'a FArray = A of 'a Array.array | U of (int*'a*'a FArray ref)
in the generated ML.

The code_datatype to that I map the Isabelle-array type is: "'a FArray ref", but the
above FArray-datatype has no counterpart in Isabelle.

Hmm? (not sure whether I understood your proposal)

regards + thank you,
 Peter






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