mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-12-26 17:32:30 +03:00
Move defaulting code to a separate module.
This commit is contained in:
Iavor Diatchki
parent
7bf0fa8222
commit
989e5734ef
@ -132,6 +132,7 @@ library
|
||||
Cryptol.TypeCheck.Depends,
|
||||
Cryptol.TypeCheck.PP,
|
||||
Cryptol.TypeCheck.Solve,
|
||||
Cryptol.TypeCheck.Default,
|
||||
Cryptol.TypeCheck.SimpleSolver,
|
||||
Cryptol.TypeCheck.TypeMap,
|
||||
Cryptol.TypeCheck.TypeOf,
|
||||
|
||||
174
src/Cryptol/TypeCheck/Default.hs
Normal file
174
src/Cryptol/TypeCheck/Default.hs
Normal file
@ -0,0 +1,174 @@
|
||||
module Cryptol.TypeCheck.Default where
|
||||
|
||||
import qualified Data.Set as Set
|
||||
import qualified Data.Map as Map
|
||||
import Control.Monad(guard)
|
||||
|
||||
import Cryptol.TypeCheck.Type
|
||||
import Cryptol.TypeCheck.SimpType(tMax)
|
||||
import Cryptol.TypeCheck.AST(Expr(..))
|
||||
import Cryptol.TypeCheck.Error(Warning(..))
|
||||
import Cryptol.TypeCheck.Subst(Subst,apSubst,listSubst,substBinds,singleSubst)
|
||||
import Cryptol.TypeCheck.InferTypes(Goal,goal)
|
||||
import Cryptol.TypeCheck.Solver.SMT(Solver,tryGetModel,shrinkModel)
|
||||
import Cryptol.Utils.Panic(panic)
|
||||
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
-- This is what we use to avoid ambiguity when generalizing.
|
||||
|
||||
{- If a variable, `a`, is:
|
||||
1. Of kind KNum
|
||||
2. Generic (i.e., does not appear in the environment)
|
||||
3. It appears only in constraints but not in the resulting type
|
||||
(i.e., it is not on the RHS of =>)
|
||||
4. It (say, the variable 'a') appears only in constraints like this:
|
||||
3.1 `a >= t` with (`a` not in `fvs t`)
|
||||
3.2 in the `s` of `fin s`
|
||||
|
||||
Then we replace `a` with `max(t1 .. tn)` where the `ts`
|
||||
are from the constraints `a >= t`.
|
||||
|
||||
If `t1 .. tn` is empty, then we replace `a` with 0.
|
||||
|
||||
This function assumes that 1-3 have been checked, and implements the rest.
|
||||
So, given some variables and constraints that are about to be generalized,
|
||||
we return:
|
||||
1. a new (same or smaller) set of variables to quantify,
|
||||
2. a new set of constraints,
|
||||
3. a substitution which indicates what got defaulted.
|
||||
-}
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
improveByDefaultingWithPure :: [TVar] -> [Goal] ->
|
||||
( [TVar] -- non-defaulted
|
||||
, [Goal] -- new constraints
|
||||
, Subst -- improvements from defaulting
|
||||
, [Warning] -- warnings about defaulting
|
||||
)
|
||||
improveByDefaultingWithPure as ps =
|
||||
classify (Map.fromList [ (a,([],Set.empty)) | a <- as ]) [] [] ps
|
||||
|
||||
where
|
||||
-- leq: candidate definitions (i.e. of the form x >= t, x `notElem` fvs t)
|
||||
-- for each of these, we keep the list of `t`, and the free vars in them.
|
||||
-- fins: all `fin` constraints
|
||||
-- others: any other constraints
|
||||
classify leqs fins others [] =
|
||||
let -- First, we use the `leqs` to choose some definitions.
|
||||
(defs, newOthers) = select [] [] (fvs others) (Map.toList leqs)
|
||||
su = listSubst defs
|
||||
warn (x,t) =
|
||||
case x of
|
||||
TVFree _ _ _ d -> DefaultingTo d t
|
||||
TVBound {} -> panic "Crypto.TypeCheck.Infer"
|
||||
[ "tryDefault attempted to default a quantified variable."
|
||||
]
|
||||
|
||||
names = substBinds su
|
||||
|
||||
in ( [ a | a <- as, not (a `Set.member` names) ]
|
||||
, newOthers ++ others ++ apSubst su fins
|
||||
, su
|
||||
, map warn defs
|
||||
)
|
||||
|
||||
|
||||
classify leqs fins others (prop : more) =
|
||||
case tNoUser (goal prop) of
|
||||
|
||||
-- We found a `fin` constraint.
|
||||
TCon (PC PFin) [ _ ] -> classify leqs (prop : fins) others more
|
||||
|
||||
-- Things of the form: x >= T(x) are not defaulted.
|
||||
TCon (PC PGeq) [ TVar x, t ]
|
||||
| x `elem` as && x `Set.notMember` freeRHS ->
|
||||
classify leqs' fins others more
|
||||
where freeRHS = fvs t
|
||||
add (xs1,vs1) (xs2,vs2) = (xs1 ++ xs2, Set.union vs1 vs2)
|
||||
leqs' = Map.insertWith add x ([(t,prop)],freeRHS) leqs
|
||||
|
||||
_ -> classify leqs fins (prop : others) more
|
||||
|
||||
|
||||
-- Pickout which variables may be defaulted and how.
|
||||
-- XXX: simpType t
|
||||
select yes no _ [] = ([ (x, t) | (x,t) <- yes ] ,no)
|
||||
select yes no otherFree ((x,(rhsG,vs)) : more) =
|
||||
select newYes newNo newFree newMore
|
||||
|
||||
where
|
||||
(ts,gs) = unzip rhsG
|
||||
|
||||
-- `x` selected only if appears nowehere else.
|
||||
-- this includes other candidates for defaulting.
|
||||
(newYes,newNo,newFree,newMore)
|
||||
|
||||
-- Mentioned in other constraints, definately not defaultable.
|
||||
| x `Set.member` otherFree = noDefaulting
|
||||
|
||||
| otherwise =
|
||||
let deps = [ y | (y,(_,yvs)) <- more, x `Set.member` yvs ]
|
||||
recs = filter (`Set.member` vs) deps
|
||||
in if not (null recs) || isBoundTV x -- x >= S(y), y >= T(x)
|
||||
then noDefaulting
|
||||
|
||||
-- x >= S, y >= T(x) or
|
||||
-- x >= S(y), y >= S
|
||||
else yesDefaulting
|
||||
|
||||
where
|
||||
noDefaulting = ( yes, gs ++ no, vs `Set.union` otherFree, more )
|
||||
|
||||
yesDefaulting =
|
||||
let ty = case ts of
|
||||
[] -> tNum (0::Int)
|
||||
_ -> foldr1 tMax ts
|
||||
su1 = singleSubst x ty
|
||||
in ( (x,ty) : [ (y,apSubst su1 t) | (y,t) <- yes ]
|
||||
, no -- We know that `x` does not appear here
|
||||
, otherFree -- We know that `x` did not appear here either
|
||||
|
||||
-- No need to update the `vs` because we've already
|
||||
-- checked that there are no recursive dependencies.
|
||||
, [ (y, (apSubst su1 ts1, vs1)) | (y,(ts1,vs1)) <- more ]
|
||||
)
|
||||
|
||||
|
||||
-- | Try to pick a reasonable instantiation for an expression, with
|
||||
-- the given type. This is useful when we do evaluation at the REPL.
|
||||
-- The resulting types should satisfy the constraints of the schema.
|
||||
defaultReplExpr :: Solver -> Expr -> Schema
|
||||
-> IO (Maybe ([(TParam,Type)], Expr))
|
||||
defaultReplExpr sol e s =
|
||||
if all (\v -> kindOf v == KNum) (sVars s)
|
||||
then do let params = map tpVar (sVars s)
|
||||
props = sProps s
|
||||
mb <- tryGetModel sol params props
|
||||
case mb of
|
||||
Nothing -> return Nothing
|
||||
Just mdl0 ->
|
||||
do mdl <- shrinkModel sol params props mdl0
|
||||
let su = listSubst [ (x, tNat' n) | (x,n) <- mdl ]
|
||||
return $
|
||||
do guard (null (concatMap pSplitAnd (apSubst su props)))
|
||||
tys <- mapM (bindParam su) params
|
||||
return (zip (sVars s) tys, appExpr tys)
|
||||
else return Nothing
|
||||
where
|
||||
bindParam su tp =
|
||||
do let ty = TVar tp
|
||||
ty' = apSubst su ty
|
||||
guard (ty /= ty')
|
||||
return ty'
|
||||
|
||||
appExpr tys = foldl (\e1 _ -> EProofApp e1) (foldl ETApp e tys) (sProps s)
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
@ -22,27 +22,24 @@ import Cryptol.Parser.Position(thing)
|
||||
import Cryptol.TypeCheck.PP(pp)
|
||||
import Cryptol.TypeCheck.AST
|
||||
import Cryptol.TypeCheck.Monad
|
||||
import Cryptol.TypeCheck.Default
|
||||
import Cryptol.TypeCheck.Error(Error(..),Warning(..))
|
||||
import Cryptol.TypeCheck.Subst
|
||||
(apSubst, singleSubst, isEmptySubst, substToList,
|
||||
emptySubst,Subst,listSubst, (@@), Subst,
|
||||
substBinds)
|
||||
(apSubst, isEmptySubst, substToList,
|
||||
emptySubst,Subst,(@@), Subst)
|
||||
import qualified Cryptol.TypeCheck.SimpleSolver as Simplify
|
||||
import Cryptol.TypeCheck.Solver.Types
|
||||
import Cryptol.TypeCheck.Solver.Selector(tryHasGoal)
|
||||
import Cryptol.TypeCheck.SimpType(tMax)
|
||||
|
||||
|
||||
import Cryptol.TypeCheck.Solver.SMT(Solver,proveImp,
|
||||
tryGetModel,shrinkModel)
|
||||
import Cryptol.TypeCheck.Solver.SMT(Solver,proveImp)
|
||||
import Cryptol.TypeCheck.Solver.Improve(improveProp,improveProps)
|
||||
import Cryptol.TypeCheck.Solver.Numeric.Interval
|
||||
import Cryptol.Utils.PP (text,vcat,(<+>))
|
||||
import Cryptol.Utils.Panic(panic)
|
||||
import Cryptol.Utils.Patterns(matchMaybe)
|
||||
|
||||
import Control.Applicative ((<|>))
|
||||
import Control.Monad(mzero,guard)
|
||||
import Control.Monad(mzero)
|
||||
import qualified Data.Map as Map
|
||||
import Data.Set ( Set )
|
||||
import qualified Data.Set as Set
|
||||
@ -272,12 +269,6 @@ cleanupError err =
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
assumptionIntervals :: Ctxt -> [Prop] -> Ctxt
|
||||
assumptionIntervals as ps =
|
||||
case computePropIntervals as ps of
|
||||
@ -290,159 +281,4 @@ assumptionIntervals as ps =
|
||||
|
||||
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
-- This is what we use to avoid ambiguity when generalizing.
|
||||
|
||||
{- If a variable, `a`, is:
|
||||
1. Of kind KNum
|
||||
2. Generic (i.e., does not appear in the environment)
|
||||
3. It appears only in constraints but not in the resulting type
|
||||
(i.e., it is not on the RHS of =>)
|
||||
4. It (say, the variable 'a') appears only in constraints like this:
|
||||
3.1 `a >= t` with (`a` not in `fvs t`)
|
||||
3.2 in the `s` of `fin s`
|
||||
|
||||
Then we replace `a` with `max(t1 .. tn)` where the `ts`
|
||||
are from the constraints `a >= t`.
|
||||
|
||||
If `t1 .. tn` is empty, then we replace `a` with 0.
|
||||
|
||||
This function assumes that 1-3 have been checked, and implements the rest.
|
||||
So, given some variables and constraints that are about to be generalized,
|
||||
we return:
|
||||
1. a new (same or smaller) set of variables to quantify,
|
||||
2. a new set of constraints,
|
||||
3. a substitution which indicates what got defaulted.
|
||||
-}
|
||||
|
||||
|
||||
|
||||
improveByDefaultingWithPure :: [TVar] -> [Goal] ->
|
||||
( [TVar] -- non-defaulted
|
||||
, [Goal] -- new constraints
|
||||
, Subst -- improvements from defaulting
|
||||
, [Warning] -- warnings about defaulting
|
||||
)
|
||||
improveByDefaultingWithPure as ps =
|
||||
classify (Map.fromList [ (a,([],Set.empty)) | a <- as ]) [] [] ps
|
||||
|
||||
where
|
||||
-- leq: candidate definitions (i.e. of the form x >= t, x `notElem` fvs t)
|
||||
-- for each of these, we keep the list of `t`, and the free vars in them.
|
||||
-- fins: all `fin` constraints
|
||||
-- others: any other constraints
|
||||
classify leqs fins others [] =
|
||||
let -- First, we use the `leqs` to choose some definitions.
|
||||
(defs, newOthers) = select [] [] (fvs others) (Map.toList leqs)
|
||||
su = listSubst defs
|
||||
warn (x,t) =
|
||||
case x of
|
||||
TVFree _ _ _ d -> DefaultingTo d t
|
||||
TVBound {} -> panic "Crypto.TypeCheck.Infer"
|
||||
[ "tryDefault attempted to default a quantified variable."
|
||||
]
|
||||
|
||||
names = substBinds su
|
||||
|
||||
in ( [ a | a <- as, not (a `Set.member` names) ]
|
||||
, newOthers ++ others ++ apSubst su fins
|
||||
, su
|
||||
, map warn defs
|
||||
)
|
||||
|
||||
|
||||
classify leqs fins others (prop : more) =
|
||||
case tNoUser (goal prop) of
|
||||
|
||||
-- We found a `fin` constraint.
|
||||
TCon (PC PFin) [ _ ] -> classify leqs (prop : fins) others more
|
||||
|
||||
-- Things of the form: x >= T(x) are not defaulted.
|
||||
TCon (PC PGeq) [ TVar x, t ]
|
||||
| x `elem` as && x `Set.notMember` freeRHS ->
|
||||
classify leqs' fins others more
|
||||
where freeRHS = fvs t
|
||||
add (xs1,vs1) (xs2,vs2) = (xs1 ++ xs2, Set.union vs1 vs2)
|
||||
leqs' = Map.insertWith add x ([(t,prop)],freeRHS) leqs
|
||||
|
||||
_ -> classify leqs fins (prop : others) more
|
||||
|
||||
|
||||
-- Pickout which variables may be defaulted and how.
|
||||
-- XXX: simpType t
|
||||
select yes no _ [] = ([ (x, t) | (x,t) <- yes ] ,no)
|
||||
select yes no otherFree ((x,(rhsG,vs)) : more) =
|
||||
select newYes newNo newFree newMore
|
||||
|
||||
where
|
||||
(ts,gs) = unzip rhsG
|
||||
|
||||
-- `x` selected only if appears nowehere else.
|
||||
-- this includes other candidates for defaulting.
|
||||
(newYes,newNo,newFree,newMore)
|
||||
|
||||
-- Mentioned in other constraints, definately not defaultable.
|
||||
| x `Set.member` otherFree = noDefaulting
|
||||
|
||||
| otherwise =
|
||||
let deps = [ y | (y,(_,yvs)) <- more, x `Set.member` yvs ]
|
||||
recs = filter (`Set.member` vs) deps
|
||||
in if not (null recs) || isBoundTV x -- x >= S(y), y >= T(x)
|
||||
then noDefaulting
|
||||
|
||||
-- x >= S, y >= T(x) or
|
||||
-- x >= S(y), y >= S
|
||||
else yesDefaulting
|
||||
|
||||
where
|
||||
noDefaulting = ( yes, gs ++ no, vs `Set.union` otherFree, more )
|
||||
|
||||
yesDefaulting =
|
||||
let ty = case ts of
|
||||
[] -> tNum (0::Int)
|
||||
_ -> foldr1 tMax ts
|
||||
su1 = singleSubst x ty
|
||||
in ( (x,ty) : [ (y,apSubst su1 t) | (y,t) <- yes ]
|
||||
, no -- We know that `x` does not appear here
|
||||
, otherFree -- We know that `x` did not appear here either
|
||||
|
||||
-- No need to update the `vs` because we've already
|
||||
-- checked that there are no recursive dependencies.
|
||||
, [ (y, (apSubst su1 ts1, vs1)) | (y,(ts1,vs1)) <- more ]
|
||||
)
|
||||
|
||||
|
||||
-- | Try to pick a reasonable instantiation for an expression, with
|
||||
-- the given type. This is useful when we do evaluation at the REPL.
|
||||
-- The resulting types should satisfy the constraints of the schema.
|
||||
defaultReplExpr :: Solver -> Expr -> Schema
|
||||
-> IO (Maybe ([(TParam,Type)], Expr))
|
||||
defaultReplExpr sol e s =
|
||||
if all (\v -> kindOf v == KNum) (sVars s)
|
||||
then do let params = map tpVar (sVars s)
|
||||
props = sProps s
|
||||
mb <- tryGetModel sol params props
|
||||
case mb of
|
||||
Nothing -> return Nothing
|
||||
Just mdl0 ->
|
||||
do mdl <- shrinkModel sol params props mdl0
|
||||
let su = listSubst [ (x, tNat' n) | (x,n) <- mdl ]
|
||||
return $
|
||||
do guard (null (concatMap pSplitAnd (apSubst su props)))
|
||||
tys <- mapM (bindParam su) params
|
||||
return (zip (sVars s) tys, appExpr tys)
|
||||
else return Nothing
|
||||
where
|
||||
bindParam su tp =
|
||||
do let ty = TVar tp
|
||||
ty' = apSubst su ty
|
||||
guard (ty /= ty')
|
||||
return ty'
|
||||
|
||||
appExpr tys = foldl (\e1 _ -> EProofApp e1) (foldl ETApp e tys) (sProps s)
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
Loading…
Reference in New Issue
Block a user