Allow local logical aliases (defines) #2463
Conversation
|
|
There was a problem hiding this comment.
Nice to see this feature in the works.
Import aliases are ignored when resolving defines. This made sense when they were global, but now that they are defined in modules, it would be best to treat them the same as measures or reflected functions.
There are other things to adjust that I mentioned in comments. But if name resolution looks too difficult, I could try contributing some of it, probably in January.
Another thing needed would be some user documentation for the new define annotation.
clayrat
changed the title
liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/CoreToLogic.hs
Outdated
Show resolved
Hide resolved
liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/CoreToLogic.hs
Outdated
Show resolved
Hide resolved
liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/CoreToLogic.hs
Outdated
Show resolved
Hide resolved
clayrat
changed the title
| , "define Language.Haskell.Liquid.Bag.empty = (Bag_empty 0)" | ||
| , "" | ||
| [ "define GHC.Types.True = (true)" | ||
| , "define GHC.Classes.not x = (~ x)" |
There was a problem hiding this comment.
Maybe this can go in src/GHC/Classes_LHAssumptions.hs.
| , "define Language.Haskell.Liquid.Equational.eq x y = (y)" | ||
| , "" | ||
| , "define GHC.CString.unpackCString# x = x" | ||
| , "define Language.Haskell.Liquid.ProofCombinators.cast x y = (y)" | ||
| , "define Liquid.ProofCombinators.cast x y = (y)" | ||
| , "define ProofCombinators.cast x y = (y)" |
There was a problem hiding this comment.
And perhaps these can be migrated to liquid-prelude.
| , "define Language.Haskell.Liquid.ProofCombinators.cast x y = (y)" | ||
| , "define Language.Haskell.Liquid.ProofCombinators.withProof x y = (x)" | ||
| , "define ProofCombinators.cast x y = (y)" | ||
| , "define Liquid.ProofCombinators.cast x y = (y)" | ||
| , "define Control.Parallel.Strategies.withStrategy s x = (x)" |
There was a problem hiding this comment.
Could it be migrated to liquid-parallel/src/Control/Parallel/Strategies_LHAssumptions.hs?
| , "" | ||
| [ "define GHC.Types.True = (true)" | ||
| , "define GHC.Classes.not x = (~ x)" | ||
| , "define GHC.Internal.Base.$ f x = (f x)" | ||
| , "define Main.mempty = (mempty)" |
There was a problem hiding this comment.
Does this one have any effect on tests?
| , "define Language.Haskell.Liquid.Bag.sub a b = (Bag_sub a b)" | ||
| , "define Language.Haskell.Liquid.Bag.empty = (Bag_empty 0)" | ||
| , "" | ||
| [ "define GHC.Types.True = (true)" |
There was a problem hiding this comment.
To migrate to src/GHC/Types_LHAssumptions.hs (?)
| , "" | ||
| [ "define GHC.Types.True = (true)" | ||
| , "define GHC.Classes.not x = (~ x)" | ||
| , "define GHC.Internal.Base.$ f x = (f x)" |
There was a problem hiding this comment.
Maybe this can be migrated to src/GHC/Base_LHAssumptions.hs.
This PR adds the ability to define logic aliases with a new
defineannotation outside of the built-inLanguage.Haskell.Liquid.GHC.CoreToLogicmodule. The declarations re-use the name resolution machinery, allowing for partial qualification. The local aliases are re-exported to the dependencies.Following this, some defines have been moved out of
CoreToLogic:SetandBagoperationsGHC.CString.unpackCString#Language.Haskell.Liquid.ProofCombinators.withProofRealand a localIntegeralias needed intests/pos/NumRefl.hs