Atj-type-conv-allowed-p
Ensure that a conversion between ATJ types is allowed.
- Signature
(atj-type-conv-allowed-p src-type dst-type) → yes/no
- Arguments
- src-type — Guard (atj-typep src-type).
- dst-type — Guard (atj-typep dst-type).
- Returns
- yes/no — Type (booleanp yes/no).
Not all [src>dst] wrappers are allowed during type annotation.
These wrappers server to generate Java code
to convert from the source to the destination types.
This conversion is ``automatic'' in the sense that
there is no corresponding conversion function
in the original (i.e. not-typed-annotated) ACL2 code.
For example,
we allow a conversion from :ainteger to :anumber,
which may happen when an integer is passed to a function
whose input type is that of numbers.
As another example,
we allow a conversion from :avalue to :astring,
which may be justified by guard verification,
since the inferred types are decidable over-approximations.
However, we do not allow conversions
between :astring and :anumber,
because those two types are disjoint:
it is never the case, even when guards are verified,
that a number may be (turned into) a string
or a string may be (turned into) a number.
This situation should only happen
with program-mode or non-guard-verified code.
Among the :acl2 types, we allow conversions exactly when
the two types have values in common.
Currently this is only the case when one is a subset of the other,
but future extensions of the ATJ types may result in
more general situations.
We disallow any conversions
involving the :jprim and :jprimarr types,
unless the two types are identical, of course.
That is, no :acl2 type can be converted to a :j... type,
and no :j... type can be converted to an :acl2 type.
Furthermore, no :j... type can be converted
to a different :j... type.
The reason for these restrictions is that we want to keep
the :j... types separate
from each other and from the :acl2 types,
and only allow explicit conversions between these,
i.e. via functions that the developer must write
in the original (i.e. non-typed-annotated) ACL2 code.
This predicate says whether
a conversion between two single types is allowed.
The predicate atj-types-conv-allowed-p
does the same for type lists,
which are actually used in the conversion functions
used to wrap ACL2 terms during type annotation.
Definitions and Theorems
Function: atj-type-conv-allowed-p
(defun atj-type-conv-allowed-p (src-type dst-type)
(declare (xargs :guard (and (atj-typep src-type)
(atj-typep dst-type))))
(let ((__function__ 'atj-type-conv-allowed-p))
(declare (ignorable __function__))
(if (and (atj-type-case src-type :acl2)
(atj-type-case dst-type :acl2))
(or (atj-type-<= src-type dst-type)
(atj-type-<= dst-type src-type))
(atj-type-equiv src-type dst-type))))
Theorem: booleanp-of-atj-type-conv-allowed-p
(defthm booleanp-of-atj-type-conv-allowed-p
(b* ((yes/no (atj-type-conv-allowed-p src-type dst-type)))
(booleanp yes/no))
:rule-classes :rewrite)
Theorem: atj-type-conv-allowed-p-of-atj-type-fix-src-type
(defthm atj-type-conv-allowed-p-of-atj-type-fix-src-type
(equal (atj-type-conv-allowed-p (atj-type-fix src-type)
dst-type)
(atj-type-conv-allowed-p src-type dst-type)))
Theorem: atj-type-conv-allowed-p-atj-type-equiv-congruence-on-src-type
(defthm
atj-type-conv-allowed-p-atj-type-equiv-congruence-on-src-type
(implies (atj-type-equiv src-type src-type-equiv)
(equal (atj-type-conv-allowed-p src-type dst-type)
(atj-type-conv-allowed-p src-type-equiv dst-type)))
:rule-classes :congruence)
Theorem: atj-type-conv-allowed-p-of-atj-type-fix-dst-type
(defthm atj-type-conv-allowed-p-of-atj-type-fix-dst-type
(equal (atj-type-conv-allowed-p src-type (atj-type-fix dst-type))
(atj-type-conv-allowed-p src-type dst-type)))
Theorem: atj-type-conv-allowed-p-atj-type-equiv-congruence-on-dst-type
(defthm
atj-type-conv-allowed-p-atj-type-equiv-congruence-on-dst-type
(implies (atj-type-equiv dst-type dst-type-equiv)
(equal (atj-type-conv-allowed-p src-type dst-type)
(atj-type-conv-allowed-p src-type dst-type-equiv)))
:rule-classes :congruence)