Merge pull request #2425 from ucsd-progsys/fd/no-laws

Remove dead code for class and instance laws

liquidhaskell-boot/liquidhaskell-boot.cabal

@@ -34,7 +34,6 @@ library
                       Language.Haskell.Liquid.Bare.Class
                       Language.Haskell.Liquid.Bare.DataType
                       Language.Haskell.Liquid.Bare.Expand
-                      Language.Haskell.Liquid.Bare.Laws
                       Language.Haskell.Liquid.Bare.Measure
                       Language.Haskell.Liquid.Bare.Misc
                       Language.Haskell.Liquid.Bare.Plugged
@@ -73,7 +72,6 @@ library
                       Language.Haskell.Liquid.GHC.TypeRep
                       Language.Haskell.Liquid.GHC.Plugin
                       Language.Haskell.Liquid.GHC.Plugin.Tutorial
-                      Language.Haskell.Liquid.LawInstances
                       Language.Haskell.Liquid.LHNameResolution
                       Language.Haskell.Liquid.Liquid
                       Language.Haskell.Liquid.Measure

liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs

@@ -65,11 +65,9 @@ import qualified Language.Haskell.Liquid.Bare.Axiom         as Bare
 import qualified Language.Haskell.Liquid.Bare.ToBare        as Bare
 import qualified Language.Haskell.Liquid.Bare.Class         as Bare
 import qualified Language.Haskell.Liquid.Bare.Check         as Bare
-import qualified Language.Haskell.Liquid.Bare.Laws          as Bare
 import qualified Language.Haskell.Liquid.Bare.Typeclass     as Bare
 import qualified Language.Haskell.Liquid.Transforms.CoreToLogic as CoreToLogic
 import           Language.Haskell.Liquid.UX.Config
-import           Control.Arrow                    (second)
 import Data.Hashable (Hashable)
 import Data.Bifunctor (bimap, first)
 import Data.Function (on)
@@ -280,14 +278,13 @@ makeGhcSpec0 cfg session tcg instEnvs localVars src lmap targetSpec dependencySp
     if allowTC then Bare.makeClassAuxTypes (elaborateSpecType coreToLg simplifier) datacons instMethods
                               >>= elaborateSig sig
                else pure sig
-  let (dg3, refl)    = withDiagnostics $ makeSpecRefl cfg src measEnv0 specs env name elaboratedSig tycEnv
+  let (dg3, refl)    = withDiagnostics $ makeSpecRefl cfg src specs env name elaboratedSig tycEnv
   let eqs            = gsHAxioms refl
   let (dg4, measEnv) = withDiagnostics $ addOpaqueReflMeas cfg tycEnv env mySpec measEnv0 specs eqs
   let qual     = makeSpecQual cfg env tycEnv measEnv rtEnv specs
   let (dg5, spcVars) = withDiagnostics $ makeSpecVars cfg src mySpec env measEnv
   let (dg6, spcTerm) = withDiagnostics $ makeSpecTerm cfg     mySpec env       name
   let sData    = makeSpecData  src env sigEnv measEnv elaboratedSig specs
-  let laws     = makeSpecLaws env sigEnv (gsTySigs elaboratedSig ++ gsAsmSigs elaboratedSig) measEnv specs
   let finalLiftedSpec = makeLiftedSpec name src env refl sData elaboratedSig qual myRTE (lSpec0 <> lSpec1)
   let diags    = mconcat [dg0, dg1, dg2, dg3, dg4, dg5, dg6]
 
@@ -307,7 +304,6 @@ makeGhcSpec0 cfg session tcg instEnvs localVars src lmap targetSpec dependencySp
     , _gsImps   = makeImports mspecs
     , _gsSig    = addReflSigs env name rtEnv measEnv refl elaboratedSig
     , _gsRefl   = refl
-    , _gsLaws   = laws
     , _gsData   = sData
     , _gsQual   = qual
     , _gsName   = makeSpecName env     tycEnv measEnv   name
@@ -677,19 +673,10 @@ getSizeFuns decl
 
 
 ------------------------------------------------------------------------------------------
-makeSpecLaws :: Bare.Env -> Bare.SigEnv -> [(Ghc.Var,LocSpecType)] -> Bare.MeasEnv -> Bare.ModSpecs
-             -> GhcSpecLaws
-------------------------------------------------------------------------------------------
-makeSpecLaws env sigEnv sigs menv specs = SpLaws
-  { gsLawDefs = second (map (\(_,x,y) -> (x,y))) <$> Bare.meCLaws menv
-  , gsLawInst = Bare.makeInstanceLaws env sigEnv sigs specs
-  }
-
-------------------------------------------------------------------------------------------
-makeSpecRefl :: Config -> GhcSrc -> Bare.MeasEnv -> Bare.ModSpecs -> Bare.Env -> ModName -> GhcSpecSig -> Bare.TycEnv
+makeSpecRefl :: Config -> GhcSrc -> Bare.ModSpecs -> Bare.Env -> ModName -> GhcSpecSig -> Bare.TycEnv
              -> Bare.Lookup GhcSpecRefl
 ------------------------------------------------------------------------------------------
-makeSpecRefl cfg src menv specs env name sig tycEnv = do
+makeSpecRefl cfg src specs env name sig tycEnv = do
   autoInst <- makeAutoInst env name mySpec
   rwr      <- makeRewrite env name mySpec
   rwrWith  <- makeRewriteWith env name mySpec
@@ -722,14 +709,13 @@ makeSpecRefl cfg src menv specs env name sig tycEnv = do
       , gsAutoInst   = autoInst
       , gsImpAxioms  = impAxioms
       , gsMyAxioms   = myAxioms
-      , gsReflects   = lawMethods ++ filter (isReflectVar rflSyms) sigVars ++ (fst <$> gsAsmReflects sig) ++ wRefls
+      , gsReflects   = filter (isReflectVar rflSyms) sigVars ++ (fst <$> gsAsmReflects sig) ++ wRefls
       , gsHAxioms    = F.notracepp "gsHAxioms" $ xtes ++ asmReflAxioms
       , gsWiredReft  = wRefls
       , gsRewrites   = rwr
       , gsRewritesWith = rwrWith
       }
   where
-    lawMethods   = F.notracepp "Law Methods" $ concatMap Ghc.classMethods (fst <$> Bare.meCLaws menv)
     mySpec       = M.lookupDefault mempty name specs
     -- Collect reflected symbols and fully qualify them
     rflLocSyms   = Bare.getLocReflects (Just env) specs
@@ -806,9 +792,7 @@ makeSpecSig :: Config -> ModName -> Ms.BareSpec -> Bare.ModSpecs -> Bare.Env ->
 makeSpecSig cfg name mySpec specs env sigEnv tycEnv measEnv cbs = do
   mySigs     <- makeTySigs  env sigEnv name mySpec
   aSigs      <- F.notracepp ("makeSpecSig aSigs " ++ F.showpp name) $ makeAsmSigs env sigEnv name allSpecs
-  let asmSigs =  Bare.tcSelVars tycEnv
-              ++ aSigs
-              ++ [ (x,t) | (_, x, t) <- concatMap snd (Bare.meCLaws measEnv) ]
+  let asmSigs =  Bare.tcSelVars tycEnv ++ aSigs
   let tySigs  = strengthenSigs . concat $
                   [ [(v, (0, t)) | (v, t,_) <- mySigs                         ]   -- NOTE: these weights are to priortize
                   , [(v, (1, t)) | (v, t  ) <- makeMthSigs measEnv            ]   -- user defined sigs OVER auto-generated
@@ -1273,7 +1257,6 @@ makeMeasEnv :: Bare.Env -> Bare.TycEnv -> Bare.SigEnv -> Bare.ModSpecs ->
                Bare.Lookup Bare.MeasEnv
 -------------------------------------------------------------------------------------------
 makeMeasEnv env tycEnv sigEnv specs = do
-  laws        <- Bare.makeCLaws env sigEnv name specs
   (cls, mts)  <- Bare.makeClasses        env sigEnv name specs
   let dms      = Bare.makeDefaultMethods env mts
   measures0   <- mapM (Bare.makeMeasureSpec env sigEnv name) (M.toList specs)
@@ -1291,7 +1274,6 @@ makeMeasEnv env tycEnv sigEnv specs = do
     , meDataCons    = cs'
     , meClasses     = cls
     , meMethods     = mts ++ dms
-    , meCLaws       = laws
     , meOpaqueRefl  = mempty
     }
   where

liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Check.hs

@@ -48,7 +48,6 @@ import           Language.Haskell.Liquid.Types.Specs
 import           Language.Haskell.Liquid.Types.Types
 import           Language.Haskell.Liquid.Types.Visitors
 import           Language.Haskell.Liquid.WiredIn
-import           Language.Haskell.Liquid.LawInstances      (checkLawInstances)
 
 import qualified Language.Haskell.Liquid.Measure           as Ms
 import qualified Language.Haskell.Liquid.Bare.Types        as Bare
@@ -174,7 +173,6 @@ checkTargetSpec specs src env cbs tsp
                      -- ++ checkRefinedClasses                        rClasses rInsts
                      <> checkSizeFun emb env                                      (gsTconsP (gsName tsp))
                      <> checkPlugged (catMaybes [ fmap (F.dropSym 2 $ GM.simplesymbol x,) (getMethodType t) | (x, t) <- gsMethods (gsSig tsp) ])
-                     <> checkLawInstances (gsLaws tsp)
                      <> checkRewrites tsp
 
     _rClasses         = concatMap Ms.classes specs

liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Class.hs

@@ -8,7 +8,6 @@
 
 module Language.Haskell.Liquid.Bare.Class
   ( makeClasses
-  , makeCLaws
   , makeSpecDictionaries
   , makeDefaultMethods
   , makeMethodTypes
@@ -134,28 +133,6 @@ splitDictionary = go [] []
     go _ _ _ = Nothing
 
 
--------------------------------------------------------------------------------
-makeCLaws :: Bare.Env -> Bare.SigEnv -> ModName -> Bare.ModSpecs
-          -> Bare.Lookup [(Ghc.Class, [(ModName, Ghc.Var, LocSpecType)])]
--------------------------------------------------------------------------------
-makeCLaws env sigEnv myName specs = do
-  zMbs <- forM classTcs $ \(name, clss, tc) -> do
-            clsMb <- mkClass env sigEnv myName name clss tc
-            case clsMb of
-              Nothing ->
-                return Nothing
-              Just cls -> do
-                gcls <- Mb.maybe (err tc) Right (Ghc.tyConClass_maybe tc)
-                return $ Just (gcls, snd cls)
-  return (Mb.catMaybes zMbs)
-  where
-    err tc   = error ("Not a type class: " ++ F.showpp tc)
-    classTc  = either (const Nothing) Just . Bare.lookupGhcTyConLHName env . btc_tc . rcName
-    classTcs = [ (name, cls, tc) | (name, spec) <- M.toList specs
-                                 , cls          <- Ms.claws spec
-                                 , tc           <- Mb.maybeToList (classTc cls)
-               ]
-
 -------------------------------------------------------------------------------
 makeClasses :: Bare.Env -> Bare.SigEnv -> ModName -> Bare.ModSpecs
             -> Bare.Lookup ([DataConP], [(ModName, Ghc.Var, LocSpecType)])

liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Types.hs

@@ -144,7 +144,6 @@ data MeasEnv = MeasEnv
   , meDataCons    :: ![(Ghc.Var,  LocSpecType)]           
   , meClasses     :: ![DataConP]                           
   , meMethods     :: ![(ModName, Ghc.Var, LocSpecType)]  
-  , meCLaws       :: ![(Ghc.Class, [(ModName, Ghc.Var, LocSpecType)])]  
   , meOpaqueRefl  :: ![(Ghc.Var, Measure (Located BareType) LocSymbol)] -- the opaque-reflected symbols and the corresponding measures
   }
 
@@ -156,7 +155,6 @@ instance Semigroup MeasEnv where
     , meDataCons    = meDataCons a <> meDataCons b  
     , meClasses     = meClasses a <> meClasses b                       
     , meMethods     = meMethods a <> meMethods b
-    , meCLaws       = meCLaws a <> meCLaws b
     , meOpaqueRefl  = meOpaqueRefl a <> meOpaqueRefl b
     }
 instance Monoid MeasEnv where
@@ -168,7 +166,6 @@ instance Monoid MeasEnv where
     , meDataCons    = mempty
     , meClasses     = mempty
     , meMethods     = mempty
-    , meCLaws       = mempty
     , meOpaqueRefl  = mempty
     }