GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-12-16 20:03:27 +03:00
Code Issues Projects Releases Wiki Activity

Adapt fastSchemaOf function to avoid simplifying when instantiating props.

Browse Source 
Previously, checking the type of e.g. "(&&) `{[2]b}" would not return
"(Logic [2]b) => [2]b -> [2]b -> [2]b" as expected, but
"Logic b => [2]b -> [2]b -> [2]b". This made it impossible to reconstruct
the instances necessary to produce the required Logic dictionary when
translating to saw-core.
This commit is contained in:
Brian Huffman 2017-09-18 15:54:35 -07:00
parent c6db409837
commit b4cf793e7f
1 changed files with 22 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

24
src/Cryptol/TypeCheck/TypeOf.hs
View File

@ -65,10 +65,19 @@ fastSchemaOf tyenv expr =
ETAbs tparam e -> case fastSchemaOf tyenv e of
Forall tparams props ty -> Forall (tparam : tparams) props ty
ETApp e t -> case fastSchemaOf tyenv e of
Forall (tparam : tparams) props ty -> Forall tparams (apSubst s props) (apSubst s ty)
where s = singleSubst (tpVar tparam) t
Forall (tparam : tparams) props ty
-> Forall tparams (map (plainSubst s) props) (apSubst s ty)
where s = singleSubst (tpVar tparam) t
_ -> panic "Cryptol.TypeCheck.TypeOf.fastSchemaOf"
[ "ETApp body with no type parameters" ]
-- When calling 'fastSchemaOf' on a
-- polymorphic function with instantiated type
-- variables but undischarged type
-- constraints, we would prefer to see the
-- instantiated constraints in an
-- un-simplified form. Thus we use
-- 'plainSubst' instead of 'apSubst' on the
-- type constraints.
EProofAbs p e -> case fastSchemaOf tyenv e of
Forall [] props ty -> Forall [] (p : props) ty
_ -> panic "Cryptol.TypeCheck.TypeOf.fastSchemaOf"
@ -95,6 +104,17 @@ fastSchemaOf tyenv expr =
where
monomorphic = Forall [] [] (fastTypeOf tyenv expr)
-- | Apply a substitution to a type *without* simplifying
-- constraints like @Arith [n]a@ to @Arith a@. (This is in contrast to
-- 'apSubst', which performs simplifications wherever possible.)
plainSubst :: Subst -> Type -> Type
plainSubst s ty =
case ty of
TCon tc ts -> TCon tc (map (plainSubst s) ts)
TUser f ts t -> TUser f (map (plainSubst s) ts) (plainSubst s t)
TRec fs -> TRec [ (x, plainSubst s t) | (x, t) <- fs ]
TVar x -> apSubst s (TVar x)
-- | Yields the return type of the selector on the given argument type.
typeSelect :: Type -> Selector -> Type
typeSelect (TUser _ _ ty) sel = typeSelect ty sel