intermediary replace types from solved constraints

andreinaku / SpyType

MIT License

0 stars 0 forks source link

Closed andreinaku closed 4 months ago

andreinaku commented 5 months ago

still need a method to substitute spec variable types a:list< bt > and a:list< T?0 > should replace T?0 in the specification and add constraints only when the replacement is different.

andreinaku commented 4 months ago

2ff0fb64a8832ea3d6dd20bedcb33dd2ec5462f1 replacements got from maude result subst

andreinaku commented 4 months ago

bug:

(T3 <= list< T?0 >) /\ (T6 <= list< T?0 >) /\ (T6 <= list< T4 + T5 >) solve:

((T3 <= list< T?0 >) /\ T6 <= list< T4 + T5 >)[T?0 |-> T4 + T5]

solution: add replacements to constraints as well, because not all entries will be replaced by maude.

andreinaku commented 4 months ago

this has been solved alongside #37 (commit b4ec90a4a3e6db9a2ab242564fda2be7a469fdd6)