Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] evaluating for typedecl-ed types

Email Gateway (Aug 23 2022 at 08:17):

From: Hira Taqdees Syeda <hira@chalmers.se>
Hi,

Can value in Isabelle evaluate for typedecl-ed types?

I have a setup as below:

typedecl physical
datatype ('a, 'p) addr_t = Addr 'a
type_synonym paddr = "(32 word,physical) addr_t”

With this,
value "(Addr 0)::paddr”
outputs the following error:

Wellsortedness error:
Type Test.physical not of sort typerep
No type arity Test.physical :: typerep

I understand that typedecl does the minimum for defining types,
but can I somehow make the type physical of sort typerep,
given that I do not have the option for changing its declaration?

Thanks
Hira

Email Gateway (Aug 23 2022 at 08:18):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
theory Scratch
imports Main "HOL-Word.Word"
begin

typedecl physical

consts dummy :: physical

code_datatype dummy

datatype ('a, 'p) addr_t = Addr 'a

type_synonym paddr = ‹(32 word,physical) addr_t›

value ‹Addr 0 :: paddr›

end

Hope this helps,
Florian
signature.asc

Email Gateway (Aug 23 2022 at 08:18):

From: Andreas Lochbihler <mail@andreas-lochbihler.de>
Dear Hira,

The type class typerep belongs to a number of definitional type classes the code generator
relies on. The simplest way to make code generation work for typedecls is to tell the code
generator that it should implement them trivially as the unit type. In your example, you
can write the following declarations and value should work thereafter.

consts Physical :: physical
code_datatype Physical

Note that these commands do not affect the minimality of typedecl from the logic
perspective. All types in HOL are inhabited, so declaring Physical as being an unspecified
element of physical is sound. The code_datatype then instantiates the relevant type
classes that the code generator needs. All of them are definitional, i.e., no new axioms
about physical are introduced on the way.

Hope this helps,
Andreas

Email Gateway (Aug 23 2022 at 08:18):

From: Hira Taqdees Syeda <hira@chalmers.se>
Hi Florain, Andreas,

Thanks for suggesting the solution and its explanation.

Thanks
Hira

Email Gateway (Aug 23 2022 at 08:18):

From: Hira Taqdees Syeda <hira@chalmers.se>
Hi Florian, Andreas,

Thanks for suggesting the solution and its explanation.

Thanks
Hira

Last updated: Apr 20 2024 at 01:05 UTC