From 0a529dff54f6df5ec866e38ff49b5d4304db2ec1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Facundo=20Dom=C3=ADnguez?= Date: Wed, 6 Nov 2024 22:13:48 +0000 Subject: [PATCH 1/9] Factor out dataConLHNameP in Parse.hs --- .../src/Language/Haskell/Liquid/Parse.hs | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs index cfccc2e4e..4ff2255c1 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs @@ -1491,16 +1491,16 @@ bbindP = lowerIdP <* reservedOp "::" 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 @@ -1523,6 +1523,9 @@ 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) From 4fd8be998adeb7a8af46b1e1f07146452329bd88 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Facundo=20Dom=C3=ADnguez?= Date: Wed, 6 Nov 2024 22:14:26 +0000 Subject: [PATCH 2/9] Use LHName for autosize --- liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs | 8 ++++---- .../src/Language/Haskell/Liquid/Parse.hs | 10 +++++----- .../src/Language/Haskell/Liquid/Types/Specs.hs | 4 ++-- 3 files changed, 11 insertions(+), 11 deletions(-) diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs index 1dd9c3abe..6c29310cc 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs @@ -596,7 +596,7 @@ 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 + autos <- makeAutoSize env mySpec gfail <- makeFail env mySpec return $ SpTerm { gsLazy = S.insert dictionaryVar (lazies `mappend` sizes) @@ -649,10 +649,10 @@ makeRewriteWith' env name spec = xvs <- mapM (Bare.lookupGhcVar env name "Var2") 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 diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs index 4ff2255c1..914062d2f 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs @@ -864,7 +864,7 @@ data Pspec ty ctor | 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 + | 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 @@ -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 @@ -1190,9 +1190,6 @@ hboundP = locBinderP inlineP :: Parser LocSymbol inlineP = locBinderP -asizeP :: Parser LocSymbol -asizeP = locBinderP - datavarianceP :: Parser (Located LHName, [Variance]) datavarianceP = liftM2 (,) (locUpperIdLHNameP LHTcName) (many varianceP) @@ -1489,6 +1486,9 @@ predTypeDDP = (,) <$> bbindP <*> bareTypeP bbindP :: Parser Symbol bbindP = lowerIdP <* reservedOp "::" +tyConBindLHNameP :: Parser (Located LHName) +tyConBindLHNameP = locUpperIdLHNameP LHTcName + dataConP :: [Symbol] -> Parser DataCtor dataConP as = do x <- dataConLHNameP diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs index 6a46726a1..20674ae35 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs @@ -402,7 +402,7 @@ data Spec ty bndr = Spec , 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 + , 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 @@ -571,7 +571,7 @@ data LiftedSpec = LiftedSpec -- ^ Variables that should be checked in the environment they are used , liftedAutois :: S.HashSet F.LocSymbol -- ^ 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 From 8e4808da7e3e2387f7902e8ccf49c380159e33ce Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Facundo=20Dom=C3=ADnguez?= Date: Wed, 6 Nov 2024 22:59:11 +0000 Subject: [PATCH 3/9] Use LHName for ignore annotations --- liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs | 2 +- liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs | 4 ++-- liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs | 2 +- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs index 6c29310cc..7029893ea 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs @@ -501,7 +501,7 @@ 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) + igVars <- sMapM (Bare.lookupGhcIdLHName env) (Ms.ignores mySpec) lVars <- sMapM (Bare.lookupGhcVar env name "gs-lvars" ) (Ms.lvars mySpec) return (SpVar tgtVars igVars lVars cMethods) where diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs index 914062d2f..c91d43306 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs @@ -863,7 +863,7 @@ data Pspec ty ctor | 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 + | 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 @@ -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 ) diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs index 20674ae35..267dfe627 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs @@ -401,7 +401,7 @@ data Spec ty bndr = Spec , 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. + , 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 From 94cd36a2a24dba921c4edc3ca78c5bc347a457df Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Facundo=20Dom=C3=ADnguez?= Date: Thu, 7 Nov 2024 00:02:08 +0000 Subject: [PATCH 4/9] Use LHName for lazy annotations --- liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs | 8 ++++---- liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs | 4 ++-- .../src/Language/Haskell/Liquid/Types/Specs.hs | 2 +- 3 files changed, 7 insertions(+), 7 deletions(-) diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs index 7029893ea..d5a40a4b6 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs @@ -595,7 +595,7 @@ 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 + lazies <- makeLazy env mySpec autos <- makeAutoSize env mySpec gfail <- makeFail env mySpec return $ SpTerm @@ -623,9 +623,9 @@ 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 = diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs index c91d43306..d7be896c9 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs @@ -854,7 +854,7 @@ data Pspec ty ctor | 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 + | 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, @@ -1142,7 +1142,7 @@ specP <|> fallbackSpecP "qualif" (fmap Qualif (qualifierP sortP)) <|> (reserved "lazyvar" >> fmap LVars lazyVarP ) - <|> (reserved "lazy" >> fmap Lazy lazyVarP ) + <|> (reserved "lazy" >> fmap Lazy locBinderLHNameP) <|> (reserved "rewrite" >> fmap Rewrite rewriteVarP ) <|> (reserved "rewriteWith" >> fmap Rewritewith rewriteWithP ) <|> (reserved "fail" >> fmap Fail locBinderLHNameP ) diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs index 267dfe627..e4ec86d17 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs @@ -391,7 +391,7 @@ data Spec ty bndr = Spec , 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 + , lazy :: !(S.HashSet (F.Located LHName)) -- ^ 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 , fails :: !(S.HashSet (F.Located LHName)) -- ^ These Functions should be unsafe From 4dbb8491e365d448b1d9b386bb3708b41727a57a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Facundo=20Dom=C3=ADnguez?= Date: Thu, 7 Nov 2024 00:53:03 +0000 Subject: [PATCH 5/9] Use LHName to resolve lazyvar annotations --- liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs | 2 +- liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs | 8 ++------ .../src/Language/Haskell/Liquid/Types/Specs.hs | 4 ++-- tests/todo/LazyVar.hs | 4 ++-- 4 files changed, 7 insertions(+), 11 deletions(-) diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs index d5a40a4b6..5fc7febee 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs @@ -502,7 +502,7 @@ 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.lookupGhcIdLHName env) (Ms.ignores mySpec) - lVars <- sMapM (Bare.lookupGhcVar env name "gs-lvars" ) (Ms.lvars mySpec) + lVars <- sMapM (Bare.lookupGhcIdLHName env) (Ms.lvars mySpec) return (SpVar tgtVars igVars lVars cMethods) where name = _giTargetMod src diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs index d7be896c9..c83941dbd 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs @@ -853,7 +853,7 @@ 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 + | 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 @@ -1140,7 +1140,7 @@ 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 locBinderLHNameP) <|> (reserved "rewrite" >> fmap Rewrite rewriteVarP ) @@ -1171,10 +1171,6 @@ tyBindsRemP sy = do pragmaP :: Parser (Located String) pragmaP = locStringLiteral -lazyVarP :: Parser LocSymbol -lazyVarP = locBinderP - - rewriteVarP :: Parser LocSymbol rewriteVarP = locBinderP diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs index e4ec86d17..a9cb6d3c8 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs @@ -390,7 +390,7 @@ 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 + , 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.LocSymbol) -- ^ Theorems turned into rewrite rules , rewriteWith :: !(M.HashMap F.LocSymbol [F.LocSymbol]) -- ^ Definitions using rewrite rules @@ -567,7 +567,7 @@ 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 -- ^ Automatically instantiate axioms in these Functions diff --git a/tests/todo/LazyVar.hs b/tests/todo/LazyVar.hs index cff7f4ace..4c997327c 100644 --- a/tests/todo/LazyVar.hs +++ b/tests/todo/LazyVar.hs @@ -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 From eeb88f51ae1500cf44c4132dd5e9c6e5c35a638b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Facundo=20Dom=C3=ADnguez?= Date: Thu, 7 Nov 2024 11:33:36 +0000 Subject: [PATCH 6/9] Use LHName to resolve relational annotations --- liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs | 6 +++--- .../src/Language/Haskell/Liquid/Parse.hs | 10 +++++----- .../src/Language/Haskell/Liquid/Types/Specs.hs | 4 ++-- tests/relational/pos/Abs.hs | 2 ++ 4 files changed, 12 insertions(+), 10 deletions(-) diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs index 5fc7febee..2a2bf2d4a 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs @@ -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 diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs index c83941dbd..677ec6cb8 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs @@ -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 @@ -1527,11 +1527,11 @@ 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 diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs index a9cb6d3c8..d9b06c87b 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs @@ -410,8 +410,8 @@ data Spec ty bndr = Spec -- 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 ?! diff --git a/tests/relational/pos/Abs.hs b/tests/relational/pos/Abs.hs index d80bef435..a56a6dace 100644 --- a/tests/relational/pos/Abs.hs +++ b/tests/relational/pos/Abs.hs @@ -1,5 +1,7 @@ module Abs where +import Prelude hiding (abs) + abs :: Int -> Int abs x = if x < 0 then -x else x From a4d0a93ea764f740d6d517d28346dd29f56783c1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Facundo=20Dom=C3=ADnguez?= Date: Thu, 7 Nov 2024 11:40:36 +0000 Subject: [PATCH 7/9] Use LHName to resolve rewrite annotations --- liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs | 8 ++++---- liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs | 7 ++----- .../src/Language/Haskell/Liquid/Types/Specs.hs | 2 +- 3 files changed, 7 insertions(+), 10 deletions(-) diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs index 2a2bf2d4a..ee134ed38 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs @@ -633,10 +633,10 @@ makeFail env spec = 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]) @@ -678,7 +678,7 @@ makeSpecRefl :: Config -> GhcSrc -> Bare.ModSpecs -> Bare.Env -> ModName -> GhcS ------------------------------------------------------------------------------------------ makeSpecRefl cfg src specs env name sig tycEnv = do autoInst <- makeAutoInst env name mySpec - rwr <- makeRewrite env name mySpec + rwr <- makeRewrite env mySpec rwrWith <- makeRewriteWith env name mySpec wRefls <- Bare.wiredReflects cfg env name sig xtes <- Bare.makeHaskellAxioms cfg src env tycEnv name lmap sig mySpec diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs index 677ec6cb8..222cda5c8 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs @@ -856,7 +856,7 @@ data Pspec ty ctor | 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 + | Rewrite (Located LHName) -- ^ '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 | HMeas LocSymbol -- ^ 'measure' annotation; lift Haskell binder as measure @@ -1143,7 +1143,7 @@ specP <|> (reserved "lazyvar" >> fmap LVars locBinderLHNameP) <|> (reserved "lazy" >> fmap Lazy locBinderLHNameP) - <|> (reserved "rewrite" >> fmap Rewrite rewriteVarP ) + <|> (reserved "rewrite" >> fmap Rewrite locBinderLHNameP) <|> (reserved "rewriteWith" >> fmap Rewritewith rewriteWithP ) <|> (reserved "fail" >> fmap Fail locBinderLHNameP ) <|> (reserved "ple" >> fmap Insts locBinderP ) @@ -1171,9 +1171,6 @@ tyBindsRemP sy = do pragmaP :: Parser (Located String) pragmaP = locStringLiteral -rewriteVarP :: Parser LocSymbol -rewriteVarP = locBinderP - rewriteWithP :: Parser (LocSymbol, [LocSymbol]) rewriteWithP = (,) <$> locBinderP <*> brackets (sepBy1 locBinderP comma) diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs index d9b06c87b..79c14669d 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs @@ -392,7 +392,7 @@ data Spec ty bndr = Spec , qualifiers :: ![F.Qualifier] -- ^ Qualifiers in source files , 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.LocSymbol) -- ^ Theorems turned into rewrite rules + , rewrites :: !(S.HashSet (F.Located LHName)) -- ^ Theorems turned into rewrite rules , rewriteWith :: !(M.HashMap F.LocSymbol [F.LocSymbol]) -- ^ Definitions using rewrite rules , fails :: !(S.HashSet (F.Located LHName)) -- ^ These Functions should be unsafe , reflects :: !(S.HashSet F.LocSymbol) -- ^ Binders to reflect From adccdc70544edced416651e7167c62fc5f9ac8d9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Facundo=20Dom=C3=ADnguez?= Date: Thu, 7 Nov 2024 11:46:21 +0000 Subject: [PATCH 8/9] Use LHName to resolve ple annotations --- liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs | 8 ++++---- liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs | 6 +++--- .../src/Language/Haskell/Liquid/Types/Specs.hs | 4 ++-- 3 files changed, 9 insertions(+), 9 deletions(-) diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs index ee134ed38..baad85c3f 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs @@ -677,7 +677,7 @@ 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 + autoInst <- makeAutoInst env mySpec rwr <- makeRewrite env mySpec rwrWith <- makeRewriteWith env name mySpec wRefls <- Bare.wiredReflects cfg env name sig @@ -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 ---------------------------------------------------------------------------------------- diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs index 222cda5c8..a268722dd 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs @@ -858,7 +858,7 @@ data Pspec ty ctor | Fail (Located LHName) -- ^ 'fail' annotation, the binder should be unsafe | Rewrite (Located LHName) -- ^ '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 + | 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 @@ -1146,8 +1146,8 @@ specP <|> (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 diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs index 79c14669d..ecdf34f69 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs @@ -397,7 +397,7 @@ data Spec ty bndr = Spec , 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 @@ -569,7 +569,7 @@ data LiftedSpec = LiftedSpec -- ^ Qualifiers in source/spec files , 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.Located LHName) -- ^ Type Constructors that get automatically sizing info From 912f3d62a8013157392c01fbf47f1b90ea1138bd Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Facundo=20Dom=C3=ADnguez?= Date: Thu, 7 Nov 2024 12:28:33 +0000 Subject: [PATCH 9/9] Use LHName to resolve rewriteWith annotations --- .../src/Language/Haskell/Liquid/Bare.hs | 14 +++++++------- .../src/Language/Haskell/Liquid/Parse.hs | 6 +++--- .../src/Language/Haskell/Liquid/Types/Specs.hs | 2 +- 3 files changed, 11 insertions(+), 11 deletions(-) diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs index baad85c3f..5895e66f7 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs @@ -639,14 +639,14 @@ makeRewrite env spec = 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 -> Ms.BareSpec -> Bare.Lookup (S.HashSet Ghc.TyCon) @@ -679,7 +679,7 @@ makeSpecRefl :: Config -> GhcSrc -> Bare.ModSpecs -> Bare.Env -> ModName -> GhcS makeSpecRefl cfg src specs env name sig tycEnv = do autoInst <- makeAutoInst env mySpec rwr <- makeRewrite env mySpec - rwrWith <- makeRewriteWith env name 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 diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs index a268722dd..1df173b56 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs @@ -857,7 +857,7 @@ data Pspec ty ctor | Lazy (Located LHName) -- ^ 'lazy' annotation, skip termination check on binder | Fail (Located LHName) -- ^ 'fail' annotation, the binder should be unsafe | Rewrite (Located LHName) -- ^ '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, + | 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 @@ -1171,8 +1171,8 @@ tyBindsRemP sy = do pragmaP :: Parser (Located String) pragmaP = locStringLiteral -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 diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs index ecdf34f69..531ff5244 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs @@ -393,7 +393,7 @@ data Spec ty bndr = Spec , 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.LocSymbol [F.LocSymbol]) -- ^ Definitions using 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