Re: [isabelle] Defining Union Types



Dear Christian,

datatype 'a err = Error | OK 'a

definition Raise_error :: "String.literal => 'a err"
where "Raise_error msg = Error"

code_datatype Raise_error OK

In the logic, all errors are the same "Error" value, but the generated
code uses Raise_error as constructor which also stores the error
message. Hence, the logical problem with different error messages no
longer occurs.
This looks nice. However, we do compose error messages incrementally (i.e., add
more precise information to errors at different places). I do not immediately
see how this could be achieved with a single error constructor. Any hints?
In code equations, you can "pattern-match" on the pseudo-constructor Raise_error. If you need more structured types than String.literal, the following with phantom type variables should work for you:

datatype ('a, 'b) err = Error | OK 'b

definition Raise_error :: "'a => ('a, 'b) err"
where [simp]: "Raise_error msg = Error"

code_datatype Raise_error OK

primrec more_info :: "('a, 'b) err => ('a * String.literal, 'b) err"
where
  "more_info Error = Error"
| [code]: "more_info (OK b) = (OK b)"

lemma more_info_Raise_error [code]:
  "more_info (Raise_error a) = Raise_error (a, STR ''info'')"
by simp

Cheers,
Andreas

--
Karlsruher Institut für Technologie
IPD Snelting

Andreas Lochbihler
wissenschaftlicher Mitarbeiter
Adenauerring 20a, Geb. 50.41, Raum 031
76131 Karlsruhe

Telefon: +49 721 608-47399
Fax: +49 721 608-48457
E-Mail: andreas.lochbihler at kit.edu
http://pp.info.uni-karlsruhe.de
KIT - Universität des Landes Baden-Württemberg und nationales Forschungszentrum in der Helmholtz-Gemeinschaft





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