GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-12-17 21:11:35 +03:00
Code Issues Projects Releases Wiki Activity

A bit more simplification of types.

Browse Source
This commit is contained in:
Iavor S. Diatchki 2015-05-05 14:32:12 -07:00
parent c38608126b
commit e15cf8ce15
2 changed files with 14 additions and 22 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
src/Cryptol/TypeCheck/Infer.hs
View File

@ -705,7 +705,7 @@ generalize bs0 gs0 =
genE e = foldr ETAbs (foldr EProofAbs (apSubst su e) qs) asPs
genB d = d { dDefinition = genE (dDefinition d)
, dSignature = Forall asPs qs
$ apSubst su $ sType $ dSignature d
$ simpType $ apSubst su $ sType $ dSignature d
}
addGoals later
@ -777,7 +777,7 @@ checkSigB b (Forall as asmps0 t0, validSchema) =
return Decl
{ dName = thing (P.bName b)
, dSignature = Forall as asmps t
, dSignature = Forall as asmps $ simpType t
, dDefinition = foldr ETAbs (foldr EProofAbs e2 asmps) as
, dPragmas = P.bPragmas b
}

32
src/Cryptol/TypeCheck/Solve.hs
View File

@ -559,33 +559,25 @@ tryGetModel cfg xs ps =
--------------------------------------------------------------------------------
simpType :: Type -> Type
simpType ty =
simpType ty = fromMaybe ty (simpTypeMaybe ty)
simpTypeMaybe :: Type -> Maybe Type
simpTypeMaybe ty =
case ty of
TCon c ts ->
case c of
TF {} -> fromMaybe ty $
do (e,vm) <- Num.exportType ty
TF {} -> do (e,vm) <- Num.exportType ty
e1 <- Num.crySimpExprMaybe e
Num.importType vm e1
_ -> TCon c (map simpType ts)
TVar _ -> ty
TUser x ts t -> TUser x ts (simpType t)
TRec fs -> TRec [ (l, simpType t) | (l,t) <- fs ]
_ -> TCon c `fmap` anyJust simpTypeMaybe ts
TVar _ -> Nothing
TUser x ts t -> TUser x ts `fmap` simpTypeMaybe t
TRec fs ->
do let (ls,ts) = unzip fs
ts' <- anyJust simpTypeMaybe ts
return (TRec (zip ls ts'))