HasCASL subtype relation and membership problem

[sternk]

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

---

hets -v2 -o -l HasCASL th -n SymmetricGroup Basic/LinearAlgebra_I.casl

creates a file with (only one) subtyping of

Index[n] < Int

instead of

Index[n] < Pos

as happens for CASL Subsequent

hets -v2 -l HasCASL Basic/LinearAlgebra_I_SymmetricGroup.th

fails with

/home/maeder/Hets-lib/Basic/LinearAlgebra_I_SymmetricGroup.th:657.4,
no typing for

forall i : Pos
. (i in Index[n]) <=> (pred __<=__ : Int * Int) (i, n);    %(Ax1)%

rejected 'Pos < Index[n]' of '((var i : Pos) in Index[n], ...

The file goes through if the formula is changed to

. ((i : Int) in Index[n])

but this intermediate type Int should be inferred, too. (CASL does this)

[sternk]

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

---

spechub/Hets@1ae7298170b7a26dce9acc6d2c864fb01f0cb347 now produces

types
Index[n] < Int;
Index[n] < Pos;
Nat < Int;
Pos < Nat

which avoids the final failure, but the subtype relation should be stored uniquely and type inference should find a common supertype.