Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Use GHC Name to resolve several annotations #2427

Merged
merged 9 commits into from
Nov 7, 2024
Merged

Use GHC Name to resolve several annotations #2427

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
9 commits
Select commit Hold shift + click to select a range
0a529df
Factor out dataConLHNameP in Parse.hs
facundominguez Nov 6, 2024
4fd8be9
Use LHName for autosize
facundominguez Nov 6, 2024
8e4808d
Use LHName for ignore annotations
facundominguez Nov 6, 2024
94cd36a
Use LHName for lazy annotations
facundominguez Nov 7, 2024
4dbb849
Use LHName to resolve lazyvar annotations
facundominguez Nov 7, 2024
eeb88f5
Use LHName to resolve relational annotations
facundominguez Nov 7, 2024
a4d0a93
Use LHName to resolve rewrite annotations
facundominguez Nov 7, 2024
adccdc7
Use LHName to resolve ple annotations
facundominguez Nov 7, 2024
912f3d6
Use LHName to resolve rewriteWith annotations
facundominguez Nov 7, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
56 changes: 28 additions & 28 deletions liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -501,8 +501,8 @@ makeSpecVars :: Config -> GhcSrc -> Ms.BareSpec -> Bare.Env -> Bare.MeasEnv
------------------------------------------------------------------------------------------
makeSpecVars cfg src mySpec env measEnv = do
tgtVars <- mapM (resolveStringVar env name) (checks cfg)
igVars <- sMapM (Bare.lookupGhcVar env name "gs-ignores") (Ms.ignores mySpec)
lVars <- sMapM (Bare.lookupGhcVar env name "gs-lvars" ) (Ms.lvars mySpec)
igVars <- sMapM (Bare.lookupGhcIdLHName env) (Ms.ignores mySpec)
lVars <- sMapM (Bare.lookupGhcIdLHName env) (Ms.lvars mySpec)
return (SpVar tgtVars igVars lVars cMethods)
where
name = _giTargetMod src
Expand Down Expand Up @@ -595,8 +595,8 @@ makeSpecTerm :: Config -> Ms.BareSpec -> Bare.Env -> ModName ->
------------------------------------------------------------------------------------------
makeSpecTerm cfg mySpec env name = do
sizes <- if structuralTerm cfg then pure mempty else makeSize env name mySpec
lazies <- makeLazy env name mySpec
autos <- makeAutoSize env name mySpec
lazies <- makeLazy env mySpec
autos <- makeAutoSize env mySpec
gfail <- makeFail env mySpec
return $ SpTerm
{ gsLazy = S.insert dictionaryVar (lazies `mappend` sizes)
Expand All @@ -607,12 +607,12 @@ makeSpecTerm cfg mySpec env name = do
}

makeRelation :: Bare.Env -> ModName -> Bare.SigEnv ->
[(LocSymbol, LocSymbol, LocBareType, LocBareType, RelExpr, RelExpr)] -> Bare.Lookup [(Ghc.Var, Ghc.Var, LocSpecType, LocSpecType, RelExpr, RelExpr)]
[(Located LHName, Located LHName, LocBareType, LocBareType, RelExpr, RelExpr)] -> Bare.Lookup [(Ghc.Var, Ghc.Var, LocSpecType, LocSpecType, RelExpr, RelExpr)]
makeRelation env name sigEnv = mapM go
where
go (x, y, tx, ty, a, e) = do
vx <- Bare.lookupGhcVar env name "Var" x
vy <- Bare.lookupGhcVar env name "Var" y
vx <- Bare.lookupGhcIdLHName env x
vy <- Bare.lookupGhcIdLHName env y
return
( vx
, vy
Expand All @@ -623,36 +623,36 @@ makeRelation env name sigEnv = mapM go
)


makeLazy :: Bare.Env -> ModName -> Ms.BareSpec -> Bare.Lookup (S.HashSet Ghc.Var)
makeLazy env name spec =
sMapM (Bare.lookupGhcVar env name "Var") (Ms.lazy spec)
makeLazy :: Bare.Env -> Ms.BareSpec -> Bare.Lookup (S.HashSet Ghc.Var)
makeLazy env spec =
sMapM (Bare.lookupGhcIdLHName env) (Ms.lazy spec)

makeFail :: Bare.Env -> Ms.BareSpec -> Bare.Lookup (S.HashSet (Located Ghc.Var))
makeFail env spec =
sForM (Ms.fails spec) $ \x -> do
vx <- Bare.lookupGhcIdLHName env x
return x { val = vx }

makeRewrite :: Bare.Env -> ModName -> Ms.BareSpec -> Bare.Lookup (S.HashSet (Located Ghc.Var))
makeRewrite env name spec =
makeRewrite :: Bare.Env -> Ms.BareSpec -> Bare.Lookup (S.HashSet (Located Ghc.Var))
makeRewrite env spec =
sForM (Ms.rewrites spec) $ \x -> do
vx <- Bare.lookupGhcVar env name "Var" x
vx <- Bare.lookupGhcIdLHName env x
return x { val = vx }

makeRewriteWith :: Bare.Env -> ModName -> Ms.BareSpec -> Bare.Lookup (M.HashMap Ghc.Var [Ghc.Var])
makeRewriteWith env name spec = M.fromList <$> makeRewriteWith' env name spec
makeRewriteWith :: Bare.Env -> Ms.BareSpec -> Bare.Lookup (M.HashMap Ghc.Var [Ghc.Var])
makeRewriteWith env spec = M.fromList <$> makeRewriteWith' env spec

makeRewriteWith' :: Bare.Env -> ModName -> Spec ty bndr -> Bare.Lookup [(Ghc.Var, [Ghc.Var])]
makeRewriteWith' env name spec =
makeRewriteWith' :: Bare.Env -> Spec ty bndr -> Bare.Lookup [(Ghc.Var, [Ghc.Var])]
makeRewriteWith' env spec =
forM (M.toList $ Ms.rewriteWith spec) $ \(x, xs) -> do
xv <- Bare.lookupGhcVar env name "Var1" x
xvs <- mapM (Bare.lookupGhcVar env name "Var2") xs
xv <- Bare.lookupGhcIdLHName env x
xvs <- mapM (Bare.lookupGhcIdLHName env) xs
return (xv, xvs)

makeAutoSize :: Bare.Env -> ModName -> Ms.BareSpec -> Bare.Lookup (S.HashSet Ghc.TyCon)
makeAutoSize env name
makeAutoSize :: Bare.Env -> Ms.BareSpec -> Bare.Lookup (S.HashSet Ghc.TyCon)
makeAutoSize env
= fmap S.fromList
. mapM (Bare.lookupGhcTyCon env name "TyCon")
. mapM (Bare.lookupGhcTyConLHName env)
. S.toList
. Ms.autosize

Expand All @@ -677,9 +677,9 @@ makeSpecRefl :: Config -> GhcSrc -> Bare.ModSpecs -> Bare.Env -> ModName -> GhcS
-> Bare.Lookup GhcSpecRefl
------------------------------------------------------------------------------------------
makeSpecRefl cfg src specs env name sig tycEnv = do
autoInst <- makeAutoInst env name mySpec
rwr <- makeRewrite env name mySpec
rwrWith <- makeRewriteWith env name mySpec
autoInst <- makeAutoInst env mySpec
rwr <- makeRewrite env mySpec
rwrWith <- makeRewriteWith env mySpec
wRefls <- Bare.wiredReflects cfg env name sig
xtes <- Bare.makeHaskellAxioms cfg src env tycEnv name lmap sig mySpec
asmReflAxioms <- Bare.makeAssumeReflectAxioms src env tycEnv name sig mySpec
Expand Down Expand Up @@ -777,12 +777,12 @@ addReflSigs env name rtEnv measEnv refl sig =
reflected = S.fromList $ fst <$> (wreflSigs ++ notReflActualTySigs)
notReflected xt = fst xt `notElem` reflected

makeAutoInst :: Bare.Env -> ModName -> Ms.BareSpec ->
makeAutoInst :: Bare.Env -> Ms.BareSpec ->
Bare.Lookup (S.HashSet Ghc.Var)
makeAutoInst env name spec = S.fromList <$> kvs
makeAutoInst env spec = S.fromList <$> kvs
where
kvs = forM (S.toList (Ms.autois spec)) $
Bare.lookupGhcVar env name "Var"
Bare.lookupGhcIdLHName env


----------------------------------------------------------------------------------------
Expand Down
66 changes: 31 additions & 35 deletions liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -843,8 +843,8 @@ data Pspec ty ctor
| Asrts ([Located LHName], (ty, Maybe [Located Expr])) -- ^ sym0, ..., symn :: ty / [m0,..., mn]
| DDecl DataDecl -- ^ refined 'data' declaration
| NTDecl DataDecl -- ^ refined 'newtype' declaration
| Relational (LocSymbol, LocSymbol, ty, ty, RelExpr, RelExpr) -- ^ relational signature
| AssmRel (LocSymbol, LocSymbol, ty, ty, RelExpr, RelExpr) -- ^ 'assume' relational signature
| Relational (Located LHName, Located LHName, ty, ty, RelExpr, RelExpr) -- ^ relational signature
| AssmRel (Located LHName, Located LHName, ty, ty, RelExpr, RelExpr) -- ^ 'assume' relational signature
| Class (RClass ty) -- ^ refined 'class' definition
| RInst (RInstance ty) -- ^ refined 'instance' definition
| Invt ty -- ^ 'invariant' specification
Expand All @@ -853,18 +853,18 @@ data Pspec ty ctor
| EAlias (Located (RTAlias Symbol Expr)) -- ^ 'predicate' alias declaration
| Embed (Located LHName, FTycon, TCArgs) -- ^ 'embed' declaration
| Qualif Qualifier -- ^ 'qualif' definition
| LVars LocSymbol -- ^ 'lazyvar' annotation, defer checks to *use* sites
| Lazy LocSymbol -- ^ 'lazy' annotation, skip termination check on binder
| LVars (Located LHName) -- ^ 'lazyvar' annotation, defer checks to *use* sites
| Lazy (Located LHName) -- ^ 'lazy' annotation, skip termination check on binder
| Fail (Located LHName) -- ^ 'fail' annotation, the binder should be unsafe
| Rewrite LocSymbol -- ^ 'rewrite' annotation, the binder generates a rewrite rule
| Rewritewith (LocSymbol, [LocSymbol]) -- ^ 'rewritewith' annotation, the first binder is using the rewrite rules of the second list,
| Insts LocSymbol -- ^ 'auto-inst' or 'ple' annotation; use ple locally on binder
| Rewrite (Located LHName) -- ^ 'rewrite' annotation, the binder generates a rewrite rule
| Rewritewith (Located LHName, [Located LHName]) -- ^ 'rewritewith' annotation, the first binder is using the rewrite rules of the second list,
| Insts (Located LHName) -- ^ 'auto-inst' or 'ple' annotation; use ple locally on binder
| HMeas LocSymbol -- ^ 'measure' annotation; lift Haskell binder as measure
| Reflect LocSymbol -- ^ 'reflect' annotation; reflect Haskell binder as function in logic
| OpaqueReflect LocSymbol -- ^ 'opaque-reflect' annotation
| Inline LocSymbol -- ^ 'inline' annotation; inline (non-recursive) binder as an alias
| Ignore LocSymbol -- ^ 'ignore' annotation; skip all checks inside this binder
| ASize LocSymbol -- ^ 'autosize' annotation; automatically generate size metric for this type
| Ignore (Located LHName) -- ^ 'ignore' annotation; skip all checks inside this binder
| ASize (Located LHName) -- ^ 'autosize' annotation; automatically generate size metric for this type
| HBound LocSymbol -- ^ 'bound' annotation; lift Haskell binder as an abstract-refinement "bound"
| PBound (Bound ty Expr) -- ^ 'bound' definition
| Pragma (Located String) -- ^ 'LIQUID' pragma, used to save configuration options in source files
Expand Down Expand Up @@ -1099,7 +1099,7 @@ specP
<|> (reserved "relational" >> fmap AssmRel relationalP)
<|> fmap Assm tyBindLHNameP )
<|> fallbackSpecP "assert" (fmap Asrt tyBindLHNameP)
<|> fallbackSpecP "autosize" (fmap ASize asizeP )
<|> fallbackSpecP "autosize" (fmap ASize tyConBindLHNameP)
<|> (reserved "local" >> fmap LAsrt tyBindP )

-- TODO: These next two are synonyms, kill one
Expand All @@ -1113,7 +1113,7 @@ specP
<|> (reserved "infixr" >> fmap BFix infixrP )
<|> (reserved "infix" >> fmap BFix infixP )
<|> fallbackSpecP "inline" (fmap Inline inlineP )
<|> fallbackSpecP "ignore" (fmap Ignore inlineP )
<|> fallbackSpecP "ignore" (fmap Ignore locBinderLHNameP)

<|> fallbackSpecP "bound" (fmap PBound boundP
<|> fmap HBound hboundP )
Expand All @@ -1140,14 +1140,14 @@ specP

<|> fallbackSpecP "embed" (fmap Embed embedP )
<|> fallbackSpecP "qualif" (fmap Qualif (qualifierP sortP))
<|> (reserved "lazyvar" >> fmap LVars lazyVarP )
<|> (reserved "lazyvar" >> fmap LVars locBinderLHNameP)

<|> (reserved "lazy" >> fmap Lazy lazyVarP )
<|> (reserved "rewrite" >> fmap Rewrite rewriteVarP )
<|> (reserved "lazy" >> fmap Lazy locBinderLHNameP)
<|> (reserved "rewrite" >> fmap Rewrite locBinderLHNameP)
<|> (reserved "rewriteWith" >> fmap Rewritewith rewriteWithP )
<|> (reserved "fail" >> fmap Fail locBinderLHNameP )
<|> (reserved "ple" >> fmap Insts locBinderP )
<|> (reserved "automatic-instances" >> fmap Insts locBinderP )
<|> (reserved "ple" >> fmap Insts locBinderLHNameP )
<|> (reserved "automatic-instances" >> fmap Insts locBinderLHNameP )
<|> (reserved "LIQUID" >> fmap Pragma pragmaP )
<|> (reserved "liquid" >> fmap Pragma pragmaP )
<|> {- DEFAULT -} fmap Asrts tyBindsP
Expand All @@ -1171,15 +1171,8 @@ tyBindsRemP sy = do
pragmaP :: Parser (Located String)
pragmaP = locStringLiteral

lazyVarP :: Parser LocSymbol
lazyVarP = locBinderP


rewriteVarP :: Parser LocSymbol
rewriteVarP = locBinderP

rewriteWithP :: Parser (LocSymbol, [LocSymbol])
rewriteWithP = (,) <$> locBinderP <*> brackets (sepBy1 locBinderP comma)
rewriteWithP :: Parser (Located LHName, [Located LHName])
rewriteWithP = (,) <$> locBinderLHNameP <*> brackets (sepBy1 locBinderLHNameP comma)

axiomP :: Parser LocSymbol
axiomP = locBinderP
Expand All @@ -1190,9 +1183,6 @@ hboundP = locBinderP
inlineP :: Parser LocSymbol
inlineP = locBinderP

asizeP :: Parser LocSymbol
asizeP = locBinderP

datavarianceP :: Parser (Located LHName, [Variance])
datavarianceP = liftM2 (,) (locUpperIdLHNameP LHTcName) (many varianceP)

Expand Down Expand Up @@ -1489,18 +1479,21 @@ predTypeDDP = (,) <$> bbindP <*> bareTypeP
bbindP :: Parser Symbol
bbindP = lowerIdP <* reservedOp "::"

tyConBindLHNameP :: Parser (Located LHName)
tyConBindLHNameP = locUpperIdLHNameP LHTcName

dataConP :: [Symbol] -> Parser DataCtor
dataConP as = do
x <- dataConNameP
x <- dataConLHNameP
xts <- dataConFieldsP
return $ DataCtor (makeUnresolvedLHName LHDataConName <$> x) as [] xts Nothing
return $ DataCtor x as [] xts Nothing

adtDataConP :: [Symbol] -> Parser DataCtor
adtDataConP as = do
x <- dataConNameP
x <- dataConLHNameP
reservedOp "::"
tr <- toRTypeRep <$> bareTypeP
return $ DataCtor (makeUnresolvedLHName LHDataConName <$> x) (tRepVars as tr) [] (tRepFields tr) (Just $ ty_res tr)
return $ DataCtor x (tRepVars as tr) [] (tRepFields tr) (Just $ ty_res tr)

tRepVars :: Symbolic a => [Symbol] -> RTypeRep c a r -> [Symbol]
tRepVars as tr = case fst <$> ty_vars tr of
Expand All @@ -1523,16 +1516,19 @@ dataConNameP
bad c = isSpace c || c `elem` ("(,)" :: String)
pwr s = symbol s

dataConLHNameP :: Parser (Located LHName)
dataConLHNameP = fmap (makeUnresolvedLHName LHDataConName) <$> dataConNameP

dataSizeP :: Parser (Maybe SizeFun)
dataSizeP
= brackets (Just . SymSizeFun <$> locLowerIdP)
<|> return Nothing

relationalP :: Parser (LocSymbol, LocSymbol, LocBareType, LocBareType, RelExpr, RelExpr)
relationalP :: Parser (Located LHName, Located LHName, LocBareType, LocBareType, RelExpr, RelExpr)
relationalP = do
x <- locBinderP
x <- locBinderLHNameP
reserved "~"
y <- locBinderP
y <- locBinderLHNameP
reserved "::"
braces $ do
tx <- located genBareTypeP
Expand Down
24 changes: 12 additions & 12 deletions liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -390,28 +390,28 @@ data Spec ty bndr = Spec
, ealiases :: ![F.Located (RTAlias F.Symbol F.Expr)] -- ^ Expression aliases
, embeds :: !(F.TCEmb (F.Located LHName)) -- ^ GHC-Tycon-to-fixpoint Tycon map
, qualifiers :: ![F.Qualifier] -- ^ Qualifiers in source files
, lvars :: !(S.HashSet F.LocSymbol) -- ^ Variables that should be checked in the environment they are used
, lazy :: !(S.HashSet F.LocSymbol) -- ^ Ignore Termination Check in these Functions
, rewrites :: !(S.HashSet F.LocSymbol) -- ^ Theorems turned into rewrite rules
, rewriteWith :: !(M.HashMap F.LocSymbol [F.LocSymbol]) -- ^ Definitions using rewrite rules
, lvars :: !(S.HashSet (F.Located LHName)) -- ^ Variables that should be checked in the environment they are used
, lazy :: !(S.HashSet (F.Located LHName)) -- ^ Ignore Termination Check in these Functions
, rewrites :: !(S.HashSet (F.Located LHName)) -- ^ Theorems turned into rewrite rules
, rewriteWith :: !(M.HashMap (F.Located LHName) [F.Located LHName]) -- ^ Definitions using rewrite rules
, fails :: !(S.HashSet (F.Located LHName)) -- ^ These Functions should be unsafe
, reflects :: !(S.HashSet F.LocSymbol) -- ^ Binders to reflect
, opaqueReflects :: !(S.HashSet F.LocSymbol) -- ^ Binders to opaque-reflect
, autois :: !(S.HashSet F.LocSymbol) -- ^ Automatically instantiate axioms in these Functions
, autois :: !(S.HashSet (F.Located LHName)) -- ^ Automatically instantiate axioms in these Functions
, hmeas :: !(S.HashSet F.LocSymbol) -- ^ Binders to turn into measures using haskell definitions
, hbounds :: !(S.HashSet F.LocSymbol) -- ^ Binders to turn into bounds using haskell definitions
, inlines :: !(S.HashSet F.LocSymbol) -- ^ Binders to turn into logic inline using haskell definitions
, ignores :: !(S.HashSet F.LocSymbol) -- ^ Binders to ignore during checking; that is DON't check the corebind.
, autosize :: !(S.HashSet F.LocSymbol) -- ^ Type Constructors that get automatically sizing info
, ignores :: !(S.HashSet (F.Located LHName)) -- ^ Binders to ignore during checking; that is DON't check the corebind.
, autosize :: !(S.HashSet (F.Located LHName)) -- ^ Type Constructors that get automatically sizing info
, pragmas :: ![F.Located String] -- ^ Command-line configurations passed in through source
, cmeasures :: ![Measure ty ()] -- ^ Measures attached to a type-class
, imeasures :: ![Measure ty bndr] -- ^ Mappings from (measure,type) -> measure
, omeasures :: ![Measure ty bndr] -- ^ Opaque reflection measures.
-- Separate field bc measures are checked for duplicates, and we want to allow for opaque-reflected measures to be duplicated.
-- See Note [Duplicate measures and opaque reflection] in "Language.Haskell.Liquid.Measure".
, classes :: ![RClass ty] -- ^ Refined Type-Classes
, relational :: ![(LocSymbol, LocSymbol, ty, ty, RelExpr, RelExpr)] -- ^ Relational types
, asmRel :: ![(LocSymbol, LocSymbol, ty, ty, RelExpr, RelExpr)] -- ^ Assumed relational types
, relational :: ![(F.Located LHName, F.Located LHName, ty, ty, RelExpr, RelExpr)] -- ^ Relational types
, asmRel :: ![(F.Located LHName, F.Located LHName, ty, ty, RelExpr, RelExpr)] -- ^ Assumed relational types
, termexprs :: ![(F.Located LHName, [F.Located F.Expr])] -- ^ Terminating Conditions for functions
, rinstance :: ![RInstance ty]
, dvariance :: ![(F.Located LHName, [Variance])] -- ^ TODO ? Where do these come from ?!
Expand Down Expand Up @@ -567,11 +567,11 @@ data LiftedSpec = LiftedSpec
-- ^ GHC-Tycon-to-fixpoint Tycon map
, liftedQualifiers :: HashSet F.Qualifier
-- ^ Qualifiers in source/spec files
, liftedLvars :: HashSet F.LocSymbol
, liftedLvars :: HashSet (F.Located LHName)
-- ^ Variables that should be checked in the environment they are used
, liftedAutois :: S.HashSet F.LocSymbol
, liftedAutois :: S.HashSet (F.Located LHName)
-- ^ Automatically instantiate axioms in these Functions
, liftedAutosize :: HashSet F.LocSymbol
, liftedAutosize :: HashSet (F.Located LHName)
-- ^ Type Constructors that get automatically sizing info
, liftedCmeasures :: HashSet (Measure LocBareType ())
-- ^ Measures attached to a type-class
Expand Down
2 changes: 2 additions & 0 deletions tests/relational/pos/Abs.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,7 @@
module Abs where

import Prelude hiding (abs)

abs :: Int -> Int
abs x = if x < 0 then -x else x

Expand Down
4 changes: 2 additions & 2 deletions tests/todo/LazyVar.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,9 +7,9 @@ foo = undefined
{-@ bar :: [a] -> Nat -> a @-}
bar :: [a] -> Int -> a
bar xs i
| i < l && foo x = x
| i < l = x
| otherwise = undefined
where
l = length xs
{-@ LAZYVAR x @-}
{-@ lazyvar x @-}
x = xs !! i
Loading