search

spechub / Hets

The Heterogeneous Tool Set
http://hets.eu
GNU General Public License v2.0
56 stars 18 forks source link

Partiality translations #695

Open sternk opened 10 years ago

sternk commented 10 years ago

Reported by lschrode and assigned to maeder Migrated from http://trac.informatik.uni-bremen.de:8080/hets/ticket/695

Implement both the monadic-style and the p-term style translations as laid out in the ASE submission

sternk commented 10 years ago

Comment by maeder Migrated from http://trac.informatik.uni-bremen.de:8080/hets/ticket/695#comment:2

There's a new comorphism "MonadicTranslation" (spechub/Hets@4278792968573e39da24e8eb73f931ba9c15cd50) usable in Hets-lib like:

hets -v2 -t MonadicTranslation -o thy HasCASL/PartialityTest.hets

The file extension should be ".het" (rather than ".hets"). In the ASE paper the profile of the binary function is uncurried. For some reason "More fine grained selection ..." does not work yet in graphical mode. There are also problems left with Hets-lib/HasCASL/Map.het The normalising translation should be the default, but still uses MainHCPairs rather than MainHC, although this should not matter.

sternk commented 10 years ago

Comment by maeder Migrated from http://trac.informatik.uni-bremen.de:8080/hets/ticket/695#comment:3

"More fine grained selection ..." works now, after has_model_expansion was set (spechub/Hets@aa074a906c39b63c7177040378c0073dbac4e3ba)

sternk commented 10 years ago

Comment by maeder Migrated from http://trac.informatik.uni-bremen.de:8080/hets/ticket/695#comment:4

The translation of the (commented out) nsMap properties in Hets-lib/HasCASL/Map.het is problematic, because the types "List b" and "List (? b)" are not distinguished (yet) in HasCASL, leading to incompatible instance annotations (that misguide the translation to Isabelle).

sternk commented 10 years ago

Comment by maeder Migrated from http://trac.informatik.uni-bremen.de:8080/hets/ticket/695#comment:5

This remaining bug is not easily solvable, therefore I must postpone it

sternk commented 10 years ago

Comment by maeder Migrated from http://trac.informatik.uni-bremen.de:8080/hets/ticket/695#comment:6

I'm having a hard time to typecheck: (see Hets-lib/HasCASL/Map.het)

. map f l = nsMap f l

I suppose List a (lhs) must be recognized as a subtype of List (? a) (rhs), but how should I translate this type conversion to Isabelle? (see below) Alternatively, List a and List (? a) could be considered to be identical types and are both translated to 'a partial List (and the type 'a List will never occur). This approach is unsatisfying if the simpler 'a List would suffice. So, map functions need to be generated for polymorphic data types in Isabelle for the conversions from 'a List to 'a partial List (ì.e. by List_map mkPartial)