diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Termination.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Termination.hs index 83e48ca1d0..1130257935 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Termination.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Termination.hs @@ -40,6 +40,7 @@ import Language.Haskell.Liquid.Types.Types toRTypeRep, structuralTerm, bkArrowDeep, mkArrow, bkUniv, bkArrow, fromRTypeRep) import Language.Haskell.Liquid.Types.RefType (isDecreasing, makeDecrType, makeLexRefa, makeNumEnv) import Language.Haskell.Liquid.Misc (safeFromLeft, replaceN, (<->), zip4, safeFromJust, fst5) +import qualified Liquid.GHC.API as GHC data TCheck = TerminationCheck | StrataCheck | NoCheck @@ -78,7 +79,7 @@ makeTermEnvs γ xtes xes ts ts' = setTRec γ . zip xs <$> rts rts = zipWith (addObligation OTerm) ts' <$> rss (xs, ces) = unzip xes mkSub ys ys' = F.mkSubst [(x, F.EVar y) | (x, y) <- zip ys ys'] - collectArgs' = GM.collectArguments . length . ty_binds . toRTypeRep + collectArgs' = collectArguments . length . ty_binds . toRTypeRep err x = "Constant: makeTermEnvs: no terminating expression for " ++ GM.showPpr x addObligation :: Oblig -> SpecType -> RReft -> SpecType @@ -200,7 +201,7 @@ consCBSizedTys consBind γ xes allowTC = typeclass (getConfig γ) (vars, es) = unzip xes dxs = F.pprint <$> vars - collectArgs' = GM.collectArguments . length . ty_binds . toRTypeRep . unOCons . unTemplate + collectArgs' = collectArguments . length . ty_binds . toRTypeRep . unOCons . unTemplate checkEqTypes :: [Maybe SpecType] -> CG [SpecType] checkEqTypes x = checkAllVsHead err1 toRSort (catMaybes x) err1 = ErrTermin loc dxs $ text "The decreasing parameters should be of same type" @@ -215,6 +216,26 @@ consCBSizedTys consBind γ xes | all (== f x) (f <$> xs) = return (x:xs) | otherwise = addWarning err >> return [] +-- See Note [Shape of normalized terms] in +-- Language.Haskell.Liquid.Transforms.ANF +collectArguments :: Int -> CoreExpr -> [Var] +collectArguments n e = take n (vs' ++ vs) + where + (vs', e') = collectValBinders' $ snd $ GHC.collectTyBinders e + vs = fst $ GHC.collectBinders $ ignoreLetBinds e' + +collectValBinders' :: CoreExpr -> ([Var], CoreExpr) +collectValBinders' = go [] + where + go tvs (GHC.Lam b e) | GHC.isTyVar b = go tvs e + go tvs (GHC.Lam b e) | GHC.isId b = go (b:tvs) e + go tvs (GHC.Tick _ e) = go tvs e + go tvs e = (reverse tvs, e) + +ignoreLetBinds :: GHC.Expr b -> GHC.Expr b +ignoreLetBinds (GHC.Let (GHC.NonRec _ _) e') = ignoreLetBinds e' +ignoreLetBinds e = e + consCBWithExprs :: (Bool -> CGEnv -> (Var, CoreExpr, Template SpecType) -> CG (Template SpecType)) -> CGEnv -> [(Var, CoreExpr)] -> CG CGEnv consCBWithExprs consBind γ xes diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Misc.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Misc.hs index bef854e6b0..ec0deb77cb 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Misc.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Misc.hs @@ -325,39 +325,6 @@ varLocInfo f x = f . varType <$> locNamedThing x namedPanic :: (NamedThing a) => a -> String -> b namedPanic x msg = panic (Just (getSrcSpan x)) msg --------------------------------------------------------------------------------- --- | Manipulating CoreExpr ----------------------------------------------------- --------------------------------------------------------------------------------- - -collectArguments :: Int -> CoreExpr -> [Var] -collectArguments n e = take n (vs' ++ vs) - where - (vs', e') = collectValBinders' $ snd $ collectTyBinders e - vs = fst $ collectBinders $ ignoreLetBinds e' - -{- -collectTyBinders :: CoreExpr -> ([Var], CoreExpr) -collectTyBinders expr - = go [] expr - where - go tvs (Lam b e) | isTyVar b = go (b:tvs) e - go tvs e = (reverse tvs, e) --} - -collectValBinders' :: Ghc.Expr Var -> ([Var], Ghc.Expr Var) -collectValBinders' = go [] - where - go tvs (Lam b e) | isTyVar b = go tvs e - go tvs (Lam b e) | isId b = go (b:tvs) e - go tvs (Tick _ e) = go tvs e - go tvs e = (reverse tvs, e) - -ignoreLetBinds :: Ghc.Expr t -> Ghc.Expr t -ignoreLetBinds (Let (NonRec _ _) e') - = ignoreLetBinds e' -ignoreLetBinds e - = e - -------------------------------------------------------------------------------- -- | Predicates on CoreExpr and DataCons --------------------------------------- -------------------------------------------------------------------------------- diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Transforms/ANF.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Transforms/ANF.hs index 8d5acb376d..6d53350c0a 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Transforms/ANF.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Transforms/ANF.hs @@ -255,8 +255,9 @@ stitch γ e -- Note [Shape of normalized terms] -- --- The termination checker in Termination.collectArguments expects the type --- binders to come before lets: +-- The termination checker in +-- Language.Haskell.Liquid.Constraint.Termination.collectArguments expects the +-- type binders to come before lets: -- -- > \ (@a) -> let ... in \ b c d -> ... --