You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
m <- llvm_load_module "f.bc"
f <- llvm_extract m "f" llvm_pure
:type f
Given the type of llvm_extract one would expect to anticipate the type printed, but no! The type printed actually depends on the type of f and is not always Term. I'm not against there being a convenient way to inspect Term values but shouldn't the type honestly say Term? What black magic is this?
The text was updated successfully, but these errors were encountered:
Originally (dc9c858) the :type REPL command behaved exactly like the Cryptol REPL one (its code was a cut-and-paste job). It parsed the rest of the input with the Cryptol parser, and printed its Cryptol type.
Later (3f5e493) @atomb changed its behavior. Apparently, if the input consists of the name of a saw-script primitive, then :t will print its saw-script type. Otherwise, the input is parsed as a Cryptol expression and its Cryptol type is printed. I agree that this combination of behaviors is ridiculous.
By the way, there is already another way to inspect the types of Term values: The primitive type : Term -> Type. For example:
sawscript> :t 5+3
5+3 : {a} (fin a, a >= 3) => [a]
sawscript> type {{ 5+3 }}
{a} (fin a, a >= 3) => [a]
So the Cryptol-type functionality of :t is redundant with type, and should be removed. We should also make :t parse arbitrary saw-script expressions and print their saw-script types.
Consider:
Given the type of
llvm_extract
one would expect to anticipate the type printed, but no! The type printed actually depends on the type off
and is not alwaysTerm
. I'm not against there being a convenient way to inspectTerm
values but shouldn't the type honestly sayTerm
? What black magic is this?The text was updated successfully, but these errors were encountered: