Merge branch 'develop' into array-applys

liquidhaskell-boot/liquidhaskell-boot.cabal

@@ -126,7 +126,6 @@ library
                     , Diff                 >= 0.3 && < 0.6
                     , array
                     , aeson
-                    , base64
                     , binary
                     , bytestring           >= 0.10
                     , Cabal

liquidhaskell-boot/src-ghc/Liquid/GHC/API.hs

@@ -645,6 +645,7 @@ import GHC.Types.Name                 as Ghc
 import GHC.Types.Name.Env             as Ghc
     ( NameEnv
     , lookupNameEnv
+    , mkNameEnv
     , mkNameEnvWith
     )
 import GHC.Types.Name.Set             as Ghc

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

@@ -34,7 +34,7 @@ import qualified Language.Haskell.Liquid.Misc               as Misc -- (nubHashO
 import qualified Language.Haskell.Liquid.GHC.Misc           as GM
 import qualified Liquid.GHC.API            as Ghc
 import           Language.Haskell.Liquid.GHC.Types          (StableName)
-import           Language.Haskell.Liquid.LHNameResolution   (LogicNameEnv, toBareSpecLHName)
+import           Language.Haskell.Liquid.LHNameResolution
 import           Language.Haskell.Liquid.Types.Errors
 import           Language.Haskell.Liquid.Types.DataDecl
 import           Language.Haskell.Liquid.Types.Names
@@ -214,7 +214,7 @@ makeGhcSpec0 cfg ghcTyLookupEnv tcg instEnvs localVars src lmap targetSpec depen
     if allowTC then Bare.makeClassAuxTypes (elaborateSpecType coreToLg simplifier) datacons instMethods
                               >>= elaborateSig sig
                else pure sig
-  let (dg3, refl)    = withDiagnostics $ makeSpecRefl cfg src specs env name elaboratedSig tycEnv
+  let (dg3, refl)    = withDiagnostics $ makeSpecRefl 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
@@ -247,7 +247,10 @@ makeGhcSpec0 cfg ghcTyLookupEnv tcg instEnvs localVars src lmap targetSpec depen
     , _gsTerm   = spcTerm
 
     , _gsLSpec  = finalLiftedSpec
-                { expSigs   = [ (F.symbol v, F.sr_sort $ Bare.varSortedReft embs v) | v <- gsReflects refl ]
+                { expSigs   =
+                    [ (logicNameToSymbol $ reflectGHCName thisModule $ Ghc.getName v, F.sr_sort $ Bare.varSortedReft embs v)
+                    | v <- gsReflects refl
+                    ]
                 , dataDecls = Bare.dataDeclSize mySpec $ dataDecls mySpec
                 , measures  = Ms.measures mySpec
                   -- We want to export measures in a 'LiftedSpec', especially if they are
@@ -269,9 +272,11 @@ makeGhcSpec0 cfg ghcTyLookupEnv tcg instEnvs localVars src lmap targetSpec depen
                 , reflects = Ms.reflects mySpec0
                 , cmeasures = Ms.cmeasures targetSpec
                 , embeds = Ms.embeds targetSpec
+                , privateReflects = mconcat $ map (privateReflects . snd) mspecs
                 }
     })
   where
+    thisModule = Ghc.tcg_mod tcg
     -- typeclass elaboration
 
     coreToLg ce =
@@ -609,25 +614,23 @@ getSizeFuns decl
 
 
 ------------------------------------------------------------------------------------------
-makeSpecRefl :: Config -> GhcSrc -> Bare.ModSpecs -> Bare.Env -> ModName -> GhcSpecSig -> Bare.TycEnv
+makeSpecRefl :: GhcSrc -> Bare.ModSpecs -> Bare.Env -> ModName -> GhcSpecSig -> Bare.TycEnv
              -> Bare.Lookup GhcSpecRefl
 ------------------------------------------------------------------------------------------
-makeSpecRefl cfg src specs env name sig tycEnv = do
+makeSpecRefl src specs env name sig tycEnv = do
   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
+  xtes     <- Bare.makeHaskellAxioms src env tycEnv name lmap sig mySpec
+  asmReflAxioms <- Bare.makeAssumeReflectAxioms src env tycEnv sig mySpec
   let otherAxioms = thd3 <$> asmReflAxioms
   let myAxioms =
         [ Bare.qualifyTop
             env
             name
             (F.loc lt)
-            e {eqName = s, eqRec = S.member s (exprSymbolsSet (eqBody e))}
-        | (x, lt, e) <- xtes
-        , let s = symbol x
+            e {eqRec = S.member (eqName e) (exprSymbolsSet (eqBody e))}
+        | (_, lt, e) <- xtes
         ] ++ otherAxioms
   let asmReflEls = eqName <$> otherAxioms
   let impAxioms  = concatMap (filter ((`notElem` asmReflEls) . eqName) . Ms.axeqs . snd) (M.toList specs)
@@ -645,9 +648,8 @@ makeSpecRefl cfg src specs env name sig tycEnv = do
       , gsAutoInst   = autoInst
       , gsImpAxioms  = impAxioms
       , gsMyAxioms   = myAxioms
-      , gsReflects   = (fst3 <$> xtes) ++ (fst <$> gsAsmReflects sig) ++ wRefls
+      , gsReflects   = (fst3 <$> xtes) ++ (fst <$> gsAsmReflects sig)
       , gsHAxioms    = F.notracepp "gsHAxioms" $ xtes ++ asmReflAxioms
-      , gsWiredReft  = wRefls
       , gsRewrites   = rwr
       , gsRewritesWith = rwrWith
       }
@@ -667,7 +669,7 @@ addReflSigs :: Bare.Env -> ModName -> BareRTEnv -> Bare.MeasEnv -> GhcSpecRefl -
 ------------------------------------------------------------------------------------------
 addReflSigs env name rtEnv measEnv refl sig =
   sig { gsRefSigs = F.notracepp ("gsRefSigs for " ++ F.showpp name) $ map expandReflectedSignature reflSigs
-      , gsAsmSigs = F.notracepp ("gsAsmSigs for " ++ F.showpp name) combinedOpaqueAndReflectedAndWiredAsmSigs
+      , gsAsmSigs = F.notracepp ("gsAsmSigs for " ++ F.showpp name) combinedOpaqueAndReflectedAsmSigs
       }
   where
     -- We make sure that the reflected functions are excluded from `gsAsmSigs`, except for the signatures of
@@ -681,10 +683,9 @@ addReflSigs env name rtEnv measEnv refl sig =
     -- Based on `M.union`'s handling of duplicates, the leftmost elements in the chain of `M.union` will precede over those
     -- after, which is why we put the opaque reflection first in the chain. The signatures for opaque reflections are created
     -- by strengthening the post-conditions, as in (assume-)reflection.
-    combinedOpaqueAndReflectedAndWiredAsmSigs = M.toList $
+    combinedOpaqueAndReflectedAsmSigs = M.toList $
         M.fromList (createUpdatedSpecs . fst <$> Bare.meOpaqueRefl measEnv)
         `M.union` M.fromList (filter notReflected (gsAsmSigs sig))
-        `M.union` M.fromList wreflSigs
     -- Strengthen the post-condition of each of the opaque reflections.
     createUpdatedSpecs var = (var, Bare.aty <$> Bare.strengthenSpecWithMeasure sig env var (Bare.varLocSym var))
     -- See T1738. We need to expand and qualify any reflected signature /here/, after any
@@ -696,15 +697,14 @@ addReflSigs env name rtEnv measEnv refl sig =
     expandReflectedSignature :: (Ghc.Var, LocSpecType) -> (Ghc.Var, LocSpecType)
     expandReflectedSignature = fmap (Bare.qualifyExpand env name rtEnv (F.dummyPos "expand-refSigs") [])
 
-    (wreflSigs, reflSigs)   = L.partition ((`elem` gsWiredReft refl) . fst)
-                                 [ (x, t) | (x, t, _) <- gsHAxioms refl ]
+    reflSigs = [ (x, t) | (x, t, _) <- gsHAxioms refl ]
     -- Get the set of all the actual functions (in assume-reflects)
     actualFnsInAssmRefl     = S.fromList $ fst <$> gsAsmReflects sig
     isActualFn           x  = S.member x actualFnsInAssmRefl
     -- Get all the variables from the axioms that are not actual functions (in assume-reflects)
     notReflActualTySigs     = L.filter (not . isActualFn . fst) reflSigs
     -- Get the list of reflected elements. We do not count actual functions in assume reflect as reflected
-    reflected               = S.fromList $ fst <$> (wreflSigs ++ notReflActualTySigs)
+    reflected               = S.fromList $ fst <$> notReflActualTySigs
     notReflected xt         = fst xt `notElem` reflected
 
 makeAutoInst :: Bare.Env -> Ms.BareSpec ->
@@ -1287,7 +1287,7 @@ makeLiftedSpec name src env refl sData sig qual myRTE lSpec0 = lSpec0
     xbs           = toBare <$> reflTySigs
     sigVars       = S.difference defVars reflVars
     defVars       = S.fromList (_giDefVars src)
-    reflTySigs    = [(x, t) | (x,t,_) <- gsHAxioms refl, x `notElem` gsWiredReft refl]
+    reflTySigs    = [(x, t) | (x,t,_) <- gsHAxioms refl]
     reflVars      = S.fromList (fst <$> reflTySigs)
     -- myAliases fld = M.elems . fld $ myRTE
     srcF          = _giTarget src

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

@@ -8,7 +8,7 @@
 -- | This module contains the code that DOES reflection; i.e. converts Haskell
 --   definitions into refinements.
 
-module Language.Haskell.Liquid.Bare.Axiom ( makeHaskellAxioms, strengthenSpecWithMeasure, makeAssumeReflectAxioms, wiredReflects, AxiomType(..) ) where
+module Language.Haskell.Liquid.Bare.Axiom ( makeHaskellAxioms, strengthenSpecWithMeasure, makeAssumeReflectAxioms, AxiomType(..) ) where
 
 import Prelude hiding (error)
 import Prelude hiding (mapM)
@@ -62,13 +62,12 @@ findDuplicateBetweenLists key l1 l2 =
       [ (x, y) | x <- l2', Just y <- [Map.lookup (key' x) seen]]
 
 -----------------------------------------------------------------------------------------------
-makeHaskellAxioms :: Config -> GhcSrc -> Bare.Env -> Bare.TycEnv -> ModName -> LogicMap -> GhcSpecSig -> Ms.BareSpec
+makeHaskellAxioms :: GhcSrc -> Bare.Env -> Bare.TycEnv -> ModName -> LogicMap -> GhcSpecSig -> Ms.BareSpec
                   -> Bare.Lookup [(Ghc.Var, LocSpecType, F.Equation)]
 -----------------------------------------------------------------------------------------------
-makeHaskellAxioms cfg src env tycEnv name lmap spSig spec = do
-  wiDefs     <- wiredDefs cfg env name spSig
+makeHaskellAxioms src env tycEnv name lmap spSig spec = do
   let refDefs = getReflectDefs src spSig spec env
-  return (makeAxiom env tycEnv name lmap <$> (wiDefs ++ refDefs))
+  return (makeAxiom env tycEnv name lmap <$> refDefs)
 
 -----------------------------------------------------------------------------------------------
 --          Returns a list of elements, one per assume reflect                               --
@@ -78,17 +77,17 @@ makeHaskellAxioms cfg src env tycEnv name lmap spSig spec = do
 --   ``VV == pretendedFn arg1 arg2 ...`                                                      --
 -- * The assume reflect equation, linking the pretended and actual function:                 --
 --   `actualFn arg1 arg 2 ... = pretendedFn arg1 arg2 ...`                                   --
-makeAssumeReflectAxioms :: GhcSrc -> Bare.Env -> Bare.TycEnv -> ModName -> GhcSpecSig -> Ms.BareSpec
+makeAssumeReflectAxioms :: GhcSrc -> Bare.Env -> Bare.TycEnv -> GhcSpecSig -> Ms.BareSpec
                   -> Bare.Lookup [(Ghc.Var, LocSpecType, F.Equation)]
 -----------------------------------------------------------------------------------------------
-makeAssumeReflectAxioms src env tycEnv name spSig spec = do
+makeAssumeReflectAxioms src env tycEnv spSig spec = do
   -- Send an error message if we're redefining a reflection
   case findDuplicatePair val reflActSymbols <|> findDuplicateBetweenLists val refSymbols reflActSymbols of
     Just (x , y) -> Ex.throw $ mkError y $
                       "Duplicate reflection of " ++ show x ++ " and " ++ show y
     Nothing -> return $ turnIntoAxiom <$> Ms.asmReflectSigs spec
   where
-    turnIntoAxiom (actual, pretended) = makeAssumeReflectAxiom spSig env embs name (actual, pretended)
+    turnIntoAxiom (actual, pretended) = makeAssumeReflectAxiom spSig env embs (actual, pretended)
     refDefs                 = getReflectDefs src spSig spec env
     embs                    = Bare.tcEmbs       tycEnv
     refSymbols              =
@@ -99,11 +98,11 @@ makeAssumeReflectAxioms src env tycEnv name spSig spec = do
 -- Processes one `assume reflect` and returns its axiom element, as detailed in              --
 -- `makeAssumeReflectAxioms`. Can also be used to compute the updated SpecType of            --
 -- a type where we add the post-condition that actual and pretended are the same             --
-makeAssumeReflectAxiom :: GhcSpecSig -> Bare.Env -> F.TCEmb Ghc.TyCon -> ModName
+makeAssumeReflectAxiom :: GhcSpecSig -> Bare.Env -> F.TCEmb Ghc.TyCon
                        -> (Located LHName, Located LHName) -- actual function and pretended function
                        -> (Ghc.Var, LocSpecType, F.Equation)
 -----------------------------------------------------------------------------------------------
-makeAssumeReflectAxiom sig env tce name (actual, pretended) =
+makeAssumeReflectAxiom sig env tce (actual, pretended) =
    -- The actual and pretended function must have the same type
   if pretendedTy == actualTy then
     (actualV, actual{val = aty at}, actualEq)
@@ -122,8 +121,13 @@ makeAssumeReflectAxiom sig env tce name (actual, pretended) =
       Right x -> x
       Left _ -> panic (Just $ GM.fSrcSpan pretended) "function to reflect not in scope"
     -- Get the qualified name symbols for the actual and pretended functions
-    qActual = Bare.qualifyTop env name (F.loc actual) (getLHNameSymbol $ val actual)
-    qPretended = Bare.qualifyTop env name (F.loc pretended) (getLHNameSymbol $ val pretended)
+    lhNameToSymbol lx =
+      F.symbol $
+      Mb.fromMaybe (panic (Just $ GM.fSrcSpan lx) $ "expected a resolved Haskell name: " ++ show lx) $
+      getLHGHCName $
+      val lx
+    qActual = lhNameToSymbol actual
+    qPretended = lhNameToSymbol pretended
     -- Get the GHC type of the actual and pretended functions
     actualTy = Ghc.varType actualV
     pretendedTy = Ghc.varType pretendedV
@@ -145,7 +149,7 @@ strengthenSpecWithMeasure :: GhcSpecSig -> Bare.Env
                        -> Located AxiomType
 -----------------------------------------------------------------------------------------------
 strengthenSpecWithMeasure sig env actualV qPretended =
-    qPretended{ val = addSingletonApp allowTC qPretended rt}
+    qPretended{ val = addSingletonApp allowTC (val qPretended) rt}
   where
     -- Get the GHC type of the actual and pretended functions
     actualTy = Ghc.varType actualV
@@ -324,14 +328,15 @@ makeAssumeType
   -> Ghc.Var -> Ghc.CoreExpr
   -> (LocSpecType, F.Equation)
 makeAssumeType allowTC tce lmap dm sym mbT v def
-  = (sym {val = aty at `strengthenRes` F.subst su ref},  F.mkEquation (val sym) xts (F.subst su le) out)
+  = (sym {val = aty at `strengthenRes` F.subst su ref},  F.mkEquation symbolV xts (F.subst su le) out)
   where
+    symbolV = F.symbol v
     rt    = fromRTypeRep .
             (\trep@RTypeRep{..} ->
                 trep{ty_info = fmap (\i -> i{permitTC = Just allowTC}) ty_info}) .
             toRTypeRep $ Mb.fromMaybe (ofType τ) mbT
     τ     = Ghc.varType v
-    at    = addSingletonApp allowTC sym rt
+    at    = addSingletonApp allowTC symbolV rt
     out   = rTypeSort tce $ ares at
     xArgs = F.EVar . fst <$> aargs at
     _msg  = unwords [showpp sym, showpp mbT]
@@ -427,7 +432,7 @@ data AxiomType = AT { aty :: SpecType, aargs :: [(F.Symbol, SpecType)], ares ::
 -- @addSingletonApp allowTC f (x:_ -> y: -> {v:_ | p}@ produces a type
 -- @x:_ -> y:_ -> {v:_ | p && v = f x y}@
 --
-addSingletonApp :: Bool -> LocSymbol -> SpecType -> AxiomType
+addSingletonApp :: Bool -> F.Symbol -> SpecType -> AxiomType
 addSingletonApp allowTC s st = AT to (reverse xts) res
   where
     (to, (_,xts, Just res)) = runState (go st) (1,[], Nothing)
@@ -452,60 +457,7 @@ unDummy x i
   | x /= F.dummySymbol = x
   | otherwise          = F.symbol ("lq" ++ show i)
 
-singletonApp :: F.Symbolic a => LocSymbol -> [a] -> UReft F.Reft
+singletonApp :: F.Symbolic a => F.Symbol -> [a] -> UReft F.Reft
 singletonApp s ys = MkUReft r mempty
   where
-    r             = F.exprReft (F.mkEApp s (F.eVar <$> ys))
-
-
--------------------------------------------------------------------------------
--- | Hardcode imported reflected functions ------------------------------------
--------------------------------------------------------------------------------
-
-wiredReflects :: Config -> Bare.Env -> ModName -> GhcSpecSig ->
-                 Bare.Lookup [Ghc.Var]
-wiredReflects cfg env name sigs = do
-  vs <- wiredDefs cfg env name sigs
-  return [v | (_, _, v, _) <- vs]
-
-wiredDefs :: Config -> Bare.Env -> ModName -> GhcSpecSig
-          -> Bare.Lookup [(LocSymbol, Maybe SpecType, Ghc.Var, Ghc.CoreExpr)]
-wiredDefs cfg env name spSig
-  | reflection cfg = do
-    let x = F.dummyLoc functionComposisionSymbol
-    v    <- Bare.lookupGhcVar env name "wiredAxioms" x
-    return [ (x, F.val <$> lookup v (gsTySigs spSig), v, makeCompositionExpression v) ]
-  | otherwise =
-    return []
-
--------------------------------------------------------------------------------
--- | Expression Definitions of Prelude Functions ------------------------------
--- | NV: Currently Just Hacking Composition       -----------------------------
--------------------------------------------------------------------------------
-
-
-makeCompositionExpression :: Ghc.Id -> Ghc.CoreExpr
-makeCompositionExpression gid
-  =  go $ Ghc.varType $ F.notracepp ( -- tracing to find  the body of . from the inline spec,
-                                      -- replace F.notrace with F.trace to print
-      "\nv = " ++ GM.showPpr gid ++
-      "\n realIdUnfolding = " ++ GM.showPpr (Ghc.realIdUnfolding gid) ++
-      "\n maybeUnfoldingTemplate . realIdUnfolding = " ++ GM.showPpr (Ghc.maybeUnfoldingTemplate $ Ghc.realIdUnfolding gid ) ++
-      "\n inl_src . inlinePragInfo . Ghc.idInfo = "    ++ GM.showPpr (Ghc.inl_src $ Ghc.inlinePragInfo $ Ghc.idInfo gid) ++
-      "\n inl_inline . inlinePragInfo . Ghc.idInfo = " ++ GM.showPpr (Ghc.inl_inline $ Ghc.inlinePragInfo $ Ghc.idInfo gid) ++
-      "\n inl_sat . inlinePragInfo . Ghc.idInfo = "    ++ GM.showPpr (Ghc.inl_sat $ Ghc.inlinePragInfo $ Ghc.idInfo gid) ++
-      "\n inl_act . inlinePragInfo . Ghc.idInfo = "    ++ GM.showPpr (Ghc.inl_act $ Ghc.inlinePragInfo $ Ghc.idInfo gid) ++
-      "\n inl_rule . inlinePragInfo . Ghc.idInfo = "   ++ GM.showPpr (Ghc.inl_rule $ Ghc.inlinePragInfo $ Ghc.idInfo gid) ++
-      "\n inl_rule rule = " ++ GM.showPpr (Ghc.inl_rule $ Ghc.inlinePragInfo $ Ghc.idInfo gid) ++
-      "\n inline spec = " ++ GM.showPpr (Ghc.inl_inline $ Ghc.inlinePragInfo $ Ghc.idInfo gid)
-     ) gid
-   where
-    go (Ghc.ForAllTy a (Ghc.ForAllTy b (Ghc.ForAllTy c Ghc.FunTy{ Ghc.ft_arg = tf, Ghc.ft_res = Ghc.FunTy { Ghc.ft_arg = tg, Ghc.ft_res = tx}})))
-      = let f = stringVar "f" tf
-            g = stringVar "g" tg
-            x = stringVar "x" tx
-        in Ghc.Lam (Ghc.binderVar a) $
-           Ghc.Lam (Ghc.binderVar b) $
-           Ghc.Lam (Ghc.binderVar c) $
-           Ghc.Lam f $ Ghc.Lam g $ Ghc.Lam x $ Ghc.App (Ghc.Var f) (Ghc.App (Ghc.Var g) (Ghc.Var x))
-    go _ = error "Axioms.go"
+    r             = F.exprReft (F.eApps (F.EVar s) (F.eVar <$> ys))

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

@@ -16,6 +16,7 @@ module Language.Haskell.Liquid.Bare.Resolve
     makeEnv
   , makeLocalVars
   , makeGHCTyLookupEnv
+  , GHCTyLookupEnv(..)
 
     -- * Resolving symbols
   , ResolveSym (..)
@@ -88,8 +89,7 @@ import           Language.Haskell.Liquid.Types.RType
 import           Language.Haskell.Liquid.Types.RTypeOp
 import qualified Language.Haskell.Liquid.Types.RefType as RT
 import           Language.Haskell.Liquid.Types.Types
-import           Language.Haskell.Liquid.Measure       (BareSpec)
-import           Language.Haskell.Liquid.Types.Specs   hiding (BareSpec)
+import           Language.Haskell.Liquid.Types.Specs
 import           Language.Haskell.Liquid.Types.Visitors
 import           Language.Haskell.Liquid.Bare.Types
 import           Language.Haskell.Liquid.UX.Config