liquid-fixpoint 0.9.4.7 → 0.9.6.3

raw patch · 21 files changed

+234/−254 lines, 21 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• CHANGES.md +4/−0
• liquid-fixpoint.cabal +1/−1
• src/Language/Fixpoint/Defunctionalize.hs +0/−2
• src/Language/Fixpoint/Horn/Solve.hs +12/−14
• src/Language/Fixpoint/Horn/Transformations.hs +73/−74
• src/Language/Fixpoint/Horn/Types.hs +3/−5
• src/Language/Fixpoint/Minimize.hs +0/−2
• src/Language/Fixpoint/Parse.hs +2/−4
• src/Language/Fixpoint/Smt/Interface.hs +7/−9
• src/Language/Fixpoint/Smt/Serialize.hs +7/−8
• src/Language/Fixpoint/Smt/Theories.hs +2/−3
• src/Language/Fixpoint/Smt/Types.hs +2/−3
• src/Language/Fixpoint/Solver.hs +3/−5
• src/Language/Fixpoint/Solver/Common.hs +7/−9
• src/Language/Fixpoint/Solver/EnvironmentReduction.hs +33/−37
• src/Language/Fixpoint/Solver/Extensionality.hs +17/−18
• src/Language/Fixpoint/Solver/GradualSolution.hs +5/−7
• src/Language/Fixpoint/Solver/Instantiate.hs +45/−47
• src/Language/Fixpoint/Solver/Simplify.hs +6/−2
• src/Language/Fixpoint/SortCheck.hs +0/−2
• tests/tasty/InterpretTests.hs +5/−2

@@ -2,6 +2,10 @@  ## NEXT +## 0.9.6.3 (2024-01-29)++- For now we stopped folding constants that contain NaN [#670](https://github.com/ucsd-progsys/liquid-fixpoint/pull/670)+ ## 0.9.4.7  - Support GHC 9.6 tuples with `--extensionality` [#666](https://github.com/ucsd-progsys/liquid-fixpoint/issues/641) [#667](https://github.com/ucsd-progsys/liquid-fixpoint/issues/641)

@@ -1,6 +1,6 @@ cabal-version:      2.4 name:               liquid-fixpoint-version:            0.9.4.7+version:            0.9.6.3 synopsis:           Predicate Abstraction-based Horn-Clause/Implication Constraint Solver description:   This package implements an SMTLIB based Horn-Clause\/Logical Implication constraint

@@ -3,8 +3,6 @@ {-# LANGUAGE TupleSections        #-} {-# LANGUAGE OverloadedStrings    #-} -{-# OPTIONS_GHC -Wno-name-shadowing #-}- -------------------------------------------------------------------------------- -- | `defunctionalize` traverses the query to: --      1. "normalize" lambda terms by renaming binders,

@@ -1,5 +1,3 @@-{-# OPTIONS_GHC -Wno-name-shadowing #-}- ------------------------------------------------------------------------------- -- | This module defines a function to solve NNF constraints, --   by reducing them to the standard FInfo.@@ -29,20 +27,20 @@ ---------------------------------------------------------------------------------- solveHorn :: F.Config -> IO ExitCode -----------------------------------------------------------------------------------solveHorn cfg = do-  (q, opts) <- parseQuery cfg+solveHorn baseCfg = do+  (q, opts) <- parseQuery baseCfg    -- If you want to set --eliminate=none, you better make it a pragma-  cfg <- if F.eliminate cfg == F.None-           then pure (cfg { F.eliminate =  F.Some })-           else pure cfg+  cfgElim <- if F.eliminate baseCfg == F.None+           then pure (baseCfg { F.eliminate =  F.Some })+           else pure baseCfg -  cfg <- F.withPragmas cfg opts+  cfgPragmas <- F.withPragmas cfgElim opts -  when (F.save cfg) (saveHornQuery cfg q)+  when (F.save cfgPragmas) (saveHornQuery cfgPragmas q) -  r <- solve cfg q-  Solver.resultExitCode cfg r+  r <- solve cfgPragmas q+  Solver.resultExitCode cfgPragmas r  parseQuery :: F.Config -> IO (H.Query H.Tag, [String]) parseQuery cfg@@ -73,9 +71,9 @@ solve :: (F.PPrint a, NFData a, F.Loc a, Show a, F.Fixpoint a) => F.Config -> H.Query a        -> IO (F.Result (Integer, a)) -----------------------------------------------------------------------------------solve cfg q = do-  let c = Tx.uniq $ Tx.flatten $ H.qCstr q+solve cfg qry = do+  let c = Tx.uniq $ Tx.flatten $ H.qCstr qry   whenLoud $ putStrLn "Horn Uniq:"   whenLoud $ putStrLn $ F.showpp c-  q <- eliminate cfg ({- void $ -} q { H.qCstr = c })+  q <- eliminate cfg ({- void $ -} qry { H.qCstr = c })   Solver.solve cfg (hornFInfo cfg q)

@@ -4,7 +4,6 @@ {-# LANGUAGE FlexibleInstances  #-}  {-# OPTIONS_GHC -Wno-orphans        #-}-{-# OPTIONS_GHC -Wno-name-shadowing #-}  module Language.Fixpoint.Horn.Transformations (     uniq@@ -53,8 +52,8 @@                M.HashMap a1 ((a4, a2), a3) -> IO () printPiSols piSols =   mapM_-    (\(piVar, ((_, args), cstr)) -> do-                  putStr $ F.showpp piVar+    (\(piVar', ((_, args), cstr)) -> do+                  putStr $ F.showpp piVar'                   putStr " := "                   putStrLn $ F.showpp args                   putStrLn $ F.showpp cstr@@ -74,14 +73,14 @@  solveEbs :: (F.PPrint a) => F.Config -> Query a -> IO (Query a) -------------------------------------------------------------------------------solveEbs cfg query@(Query qs vs c cons dist eqns mats dds) = do+solveEbs cfg query@(Query qs vs cstr cons dist eqns mats dds) = do   -- clean up-  let normalizedC = flatten . pruneTauts $ hornify c+  let normalizedC = flatten . pruneTauts $ hornify cstr   whenLoud $ putStrLn "Normalized EHC:"   whenLoud $ putStrLn $ F.showpp normalizedC    -- short circuit if no ebinds are present-  if isNNF c then pure $ Query qs vs normalizedC cons dist eqns mats dds else do+  if isNNF cstr then pure $ Query qs vs normalizedC cons dist eqns mats dds else do   let kvars = boundKvars normalizedC    whenLoud $ putStrLn "Skolemized:"@@ -105,17 +104,17 @@   let acyclicKs = kvars `S.difference` cuts    whenLoud $ putStrLn "solved acyclic kvars:"-  let (horn', side') = elimKs' (S.toList acyclicKs) (horn, side)-  whenLoud $ putStrLn $ F.showpp horn'-  whenLoud $ putStrLn $ F.showpp side'+  let (hornk, sidek) = elimKs' (S.toList acyclicKs) (horn, side)+  whenLoud $ putStrLn $ F.showpp hornk+  whenLoud $ putStrLn $ F.showpp sidek    -- if not $ S.null cuts then error $ F.showpp $ S.toList cuts else pure ()   let elimCutK k c = doelim k [] c-  horn' <- pure $ foldr elimCutK horn' cuts-  side' <- pure $ foldr elimCutK side' cuts+      hornCut = foldr elimCutK hornk cuts+      sideCut = foldr elimCutK sidek cuts    whenLoud $ putStrLn "pi defining constraints:"-  let piSols = M.fromList $ fmap (\pivar -> (pivar, piDefConstr pivar horn')) (S.toList pivars)+  let piSols = M.fromList $ fmap (\pivar -> (pivar, piDefConstr pivar hornCut)) (S.toList pivars)   whenLoud $ printPiSols piSols    whenLoud $ putStrLn "solved pis:"@@ -123,11 +122,11 @@   whenLoud $ putStrLn $ F.showpp solvedPiCstrs    whenLoud $ putStrLn "solved horn:"-  let solvedHorn = substPiSols solvedPiCstrs horn'+  let solvedHorn = substPiSols solvedPiCstrs hornCut   whenLoud $ putStrLn $ F.showpp solvedHorn    whenLoud $ putStrLn "solved side:"-  let solvedSide = substPiSols solvedPiCstrs side'+  let solvedSide = substPiSols solvedPiCstrs sideCut   whenLoud $ putStrLn $ F.showpp solvedSide    pure (Query qs vs (CAnd [solvedHorn, solvedSide]) cons dist eqns mats dds)@@ -135,14 +134,14 @@ -- | Collects the defining constraint for π -- that is, given `∀ Γ.∀ n.π => c`, returns `((π, n:Γ), c)` piDefConstr :: F.Symbol -> Cstr a -> ((F.Symbol, [F.Symbol]), Cstr a)-piDefConstr k c = ((head ns, head formals), defC)+piDefConstr k c = ((head syms, head formalSyms), defCStr)   where-    (ns, formals, defC) = case go c of+    (syms, formalSyms, defCStr) = case go c of       (ns, formals, Just defC) -> (ns, formals, defC)       (_, _, Nothing) -> error $ "pi variable " <> F.showpp k <> " has no defining constraint."      go :: Cstr a -> ([F.Symbol], [[F.Symbol]], Maybe (Cstr a))-    go (CAnd cs) = (\(as, bs, cs) -> (concat as, concat bs, cAndMaybes cs)) $ unzip3 $ go <$> cs+    go (CAnd cs) = (\(as, bs, mcs) -> (concat as, concat bs, cAndMaybes mcs)) $ unzip3 $ go <$> cs     go (All b@(Bind n _ (Var k' xs) _) c')       | k == k' = ([n], [S.toList $ S.fromList xs `S.difference` S.singleton n], Just c')       | otherwise = map3 (fmap (All b)) (go c')@@ -159,18 +158,18 @@  -- | Solve out the given pivars solPis :: S.Set F.Symbol -> M.HashMap F.Symbol ((F.Symbol, [F.Symbol]), Cstr a) -> M.HashMap F.Symbol Pred-solPis measures piSols = go (M.toList piSols) piSols+solPis measures piSolsMap = go (M.toList piSolsMap) piSolsMap   where-    go ((pi, ((n, xs), c)):pis) piSols = M.insert pi solved $ go pis piSols-      where solved = solPi measures pi n (S.fromList xs) piSols c+    go ((pi', ((n, xs), c)):pis) piSols = M.insert pi' solved $ go pis piSols+      where solved = solPi measures pi' n (S.fromList xs) piSols c     go [] _ = mempty  -- TODO: rewrite to use CC solPi :: S.Set F.Symbol -> F.Symbol -> F.Symbol -> S.Set F.Symbol -> M.HashMap F.Symbol ((F.Symbol, [F.Symbol]), Cstr a) -> Cstr a -> Pred-solPi measures basePi n args piSols c = trace ("\n\nsolPi: " <> F.showpp basePi <> "\n\n" <> F.showpp n <> "\n" <> F.showpp (S.toList args) <> "\n" <> F.showpp ((\(a, _, c) -> (a, c)) <$> edges) <> "\n" <> F.showpp (sols n) <> "\n" <> F.showpp rewritten <> "\n" <> F.showpp c <> "\n\n") $ PAnd rewritten+solPi measures basePi n args piSols cstr = trace ("\n\nsolPi: " <> F.showpp basePi <> "\n\n" <> F.showpp n <> "\n" <> F.showpp (S.toList args) <> "\n" <> F.showpp ((\(a, _, c) -> (a, c)) <$> edges) <> "\n" <> F.showpp (sols n) <> "\n" <> F.showpp rewritten <> "\n" <> F.showpp cstr <> "\n\n") $ PAnd rewritten   where     rewritten = rewriteWithEqualities measures n args equalities-    equalities = (nub . fst) $ go (S.singleton basePi) c+    equalities = (nub . fst) $ go (S.singleton basePi) cstr     edges = eqEdges args mempty equalities     (eGraph, vf, lookupVertex) = DG.graphFromEdges edges     sols x = case lookupVertex x of@@ -178,12 +177,12 @@       Just vertex -> nub $ filter (/= F.EVar x) $ mconcat [es | ((_, es), _, _) <- vf <$> DG.reachable eGraph vertex]      go :: S.Set F.Symbol -> Cstr a -> ([(F.Symbol, F.Expr)], S.Set F.Symbol)-    go visited (Head p _) = (collectEqualities p, visited)-    go visited (CAnd cs) = foldl' (\(eqs, visited) c -> let (eqs', visited') = go visited c in (eqs' <> eqs, visited')) (mempty, visited) cs-    go visited (All (Bind _ _ (Var pi _) _) c)-      | S.member pi visited = go visited c-      | otherwise = let (_, defC) = (piSols M.! pi)-                        (eqs', newVisited) = go (S.insert pi visited) defC+    go visitedSyms (Head p _) = (collectEqualities p, visitedSyms)+    go visitedSyms (CAnd cs) = foldl' (\(eqs, visited) c -> let (eqs', visited') = go visited c in (eqs' <> eqs, visited')) (mempty, visitedSyms) cs+    go visited (All (Bind _ _ (Var pi' _) _) c)+      | S.member pi' visited = go visited c+      | otherwise = let (_, defC) = (piSols M.! pi')+                        (eqs', newVisited) = go (S.insert pi' visited) defC                         (eqs'', newVisited') = go newVisited c in           (eqs' <> eqs'', newVisited')     go visited (All (Bind _ _ p _) c) = let (eqs, visited') = go visited c in@@ -242,11 +241,11 @@     go _ (Head c l) = Head c l     go xs (CAnd c)   = CAnd (go xs <$> c)     go xs (All b c2) = All b $ go (bSym b : xs) c2-    go xs (Any b@(Bind x t p ann) c2) = CAnd [All b' $ CAnd [Head p l, go (x:xs) c2], Any b (Head pi l)]+    go xs (Any b@(Bind x t p ann) c2) = CAnd [All b' $ CAnd [Head p l, go (x:xs) c2], Any b (Head pi' l)]       -- TODO: actually use the renamer?       where-        b' = Bind x t pi ann-        pi = piVar x xs+        b' = Bind x t pi' ann+        pi' = piVar x xs         l  = cLabel c2  piVar :: F.Symbol -> [F.Symbol] -> Pred@@ -330,7 +329,7 @@ split c@Head{} = (Just c, Nothing)  andMaybes :: [Maybe (Cstr a)] -> Maybe (Cstr a)-andMaybes cs = case catMaybes cs of+andMaybes mcs = case catMaybes mcs of                  [] -> Nothing                  [c] -> Just c                  cs -> Just $ CAnd cs@@ -386,31 +385,31 @@ elimPis [] cc = cc elimPis (n:ns) (horn, side) = elimPis ns (apply horn, apply side) -- TODO: handle this error?-  where nSol = case defs n horn of+  where nSol' = case defs n horn of                  Just nSol -> nSol                  Nothing -> error "Unexpected nothing elimPis" -        apply = applyPi (piSym n) nSol+        apply = applyPi (piSym n) nSol'  -- TODO: PAnd may be a problem applyPi :: F.Symbol -> Cstr a -> Cstr a -> Cstr a-applyPi k defs (All (Bind x t (Var k' _xs) ann) c)+applyPi k defCstr (All (Bind x t (Var k' _xs) ann) c)   | k == k'-  = All (Bind x t (Reft $ cstrToExpr defs) ann) c+  = All (Bind x t (Reft $ cstrToExpr defCstr) ann) c applyPi k bp (CAnd cs)   = CAnd $ applyPi k bp <$> cs applyPi k bp (All b c)   = All b (applyPi k bp c) applyPi k bp (Any b c)   = Any b (applyPi k bp c)-applyPi k defs (Head (Var k' _xs) a)+applyPi k defCstr (Head (Var k' _xs) a)   | k == k'   -- what happens when pi's appear inside the defs for other pis?   -- this shouldn't happen because there should be a strict   --  pi -> k -> pi structure   -- but that comes from the typing rules, not this format, so let's make   -- it an invariant of solveEbs above-  = Head (Reft $ cstrToExpr defs) a+  = Head (Reft $ cstrToExpr defCstr) a applyPi _ _ (Head p a) = Head p a  -- | The defining constraints for a pivar@@ -647,15 +646,15 @@     isWellFormed e = S.fromList (F.syms e) `S.isSubsetOf` argsAndPrims      makeWellFormed :: Int -> [F.Expr] -> [F.Expr]-    makeWellFormed 0 es = filter isWellFormed es -- We solved it. Maybe.-    makeWellFormed n es = makeWellFormed (n - 1) $ mconcat $ go <$> es+    makeWellFormed 0 exprs = filter isWellFormed exprs -- We solved it. Maybe.+    makeWellFormed m exprs = makeWellFormed (m - 1) $ mconcat $ go <$> exprs       where-        go e = if isWellFormed e then [e] else rewrite rewrites [e]+        go expr = if isWellFormed expr then [expr] else rewrite rewrites [expr]           where-            needSolving = S.fromList (F.syms e) `S.difference` argsAndPrims+            needSolving = S.fromList (F.syms expr) `S.difference` argsAndPrims             rewrites = (\x -> (x, filter (/= F.EVar x) $ sols x)) <$> S.toList needSolving             rewrite [] es = es-            rewrite ((x, rewrites):rewrites') es = rewrite rewrites' $ [F.subst (F.mkSubst [(x, e')]) e | e' <- rewrites, e <- es]+            rewrite ((x, rewriteExprs):rewriteExprs') es = rewrite rewriteExprs' $ [F.subst (F.mkSubst [(x, e')]) e | e' <- rewriteExprs, e <- es]  eqEdges :: S.Set F.Symbol ->            M.HashMap F.Symbol ([F.Symbol], [F.Expr]) ->@@ -694,14 +693,14 @@   | Var k _ <- p = All (Bind x t (M.lookupDefault p k piSols) l) (substPiSols piSols c)   | otherwise = All (Bind x t p l) (substPiSols piSols c) substPiSols piSols (Any (Bind n _ p _) c)-  | Head (Var pi _) label <- c, Just sol <- M.lookup pi piSols =+  | Head (Var pi' _) label <- c, Just sol <- M.lookup pi' piSols =     case findSol n sol of-      Just e -> Head (flatten $ PAnd $ (\pred -> F.subst1 pred (n, e)) <$> [p, sol]) label+      Just e -> Head (flatten $ PAnd $ (\predFn -> F.subst1 predFn (n, e)) <$> [p, sol]) label       Nothing -> Head (Reft $ F.PAnd []) label   | otherwise = error "missing piSol"  findSol :: F.Symbol -> Pred -> Maybe F.Expr-findSol x = go+findSol sym = go   where     go (Reft e) = findEq e     go Var{} = Nothing@@ -710,8 +709,8 @@       x:_ -> Just x      findEq (F.PAtom F.Eq left right)-      | F.EVar y <- left, y == x = Just right-      | F.EVar y <- right, y == x = Just left+      | F.EVar y <- left, y == sym = Just right+      | F.EVar y <- right, y == sym = Just left     findEq _ = Nothing  ------------------------------------------------------------------------------@@ -812,10 +811,10 @@     -- if kvar doesn't appear, then just return the left     -- if kvar appears in one child, that is the lca     -- but if kvar appear in multiple chlidren, this is the lca-    go c@(CAnd cs) = case rights (go <$> cs) of-                       [] -> Left $ cLabel c+    go cstr'@(CAnd cs) = case rights (go <$> cs) of+                       [] -> Left $ cLabel cstr'                        [c] -> Right c-                       _ -> Right c+                       _ -> Right cstr'   -- | A solution is a Hyp of binders (including one anonymous binder@@ -857,20 +856,20 @@ -- (forall ((v bool) (v)) (forall ((z int) (donkey)) ((z == x))))  doelim :: F.Symbol -> [([Bind a], [F.Expr])] -> Cstr a -> Cstr a-doelim k bss (CAnd cs)-  = CAnd $ doelim k bss <$> cs-doelim k bss (All (Bind x t p l) c) =-  case findKVarInGuard k p of-    Right _ -> All (Bind x t p l) (doelim k bss c)-    Left (kvars, preds) -> demorgan x t l kvars preds (doelim k bss c) bss+doelim sym bss (CAnd cs)+  = CAnd $ doelim sym bss <$> cs+doelim sym bss (All (Bind sym' sort' p l) cstr) =+  case findKVarInGuard sym p of+    Right _ -> All (Bind sym' sort' p l) (doelim sym bss cstr)+    Left (kvars, preds) -> demorgan sym' sort' l kvars preds (doelim sym bss cstr) bss   where     demorgan :: F.Symbol -> F.Sort -> a -> [(F.Symbol, [F.Symbol])] -> [Pred] -> Cstr a -> [([Bind a], [F.Expr])] -> Cstr a-    demorgan x t ann kvars preds c bss = mkAnd $ cubeSol <$> bss+    demorgan x t ann kvars preds cstr' bindExprs = mkAnd $ cubeSol <$> bindExprs       where su = F.Su $ M.fromList $ concatMap (\(k, xs) -> zip (kargs k) (F.EVar <$> xs)) kvars             mkAnd [c] = c             mkAnd cs = CAnd cs             cubeSol (b:bs, eqs) = All b $ cubeSol (bs, eqs)-            cubeSol ([], eqs) = All (Bind x t (PAnd $ (Reft <$> F.subst su eqs) ++ (F.subst su <$> preds)) ann) c+            cubeSol ([], eqs) = All (Bind x t (PAnd $ (Reft <$> F.subst su eqs) ++ (F.subst su <$> preds)) ann) cstr' doelim k _ (Head (Var k' _) a)   | k == k'   = Head (Reft F.PTrue) a@@ -879,7 +878,7 @@ doelim k bss (Any (Bind x t p l) c) =   case findKVarInGuard k p of     Right _ -> Any (Bind x t p l) (doelim k bss c)-    Left (_, rights) -> Any (Bind x t (PAnd rights) l) (doelim k bss c) -- TODO: for now we set the kvar to true. not sure if this is correct+    Left (_, rights') -> Any (Bind x t (PAnd rights') l) (doelim k bss c) -- TODO: for now we set the kvar to true. not sure if this is correct  -- If k is in the guard then returns a Left list of that k and the remaining preds in the guard -- If k is not in the guard returns a Right of the pred@@ -889,9 +888,9 @@     then Right (PAnd ps) -- kvar not found     else Left (newLefts, newRights)   where findResults = findKVarInGuard k <$> ps-        (lefts, rights) = partitionEithers findResults+        (lefts, rights') = partitionEithers findResults         newLefts = concatMap fst lefts-        newRights = concatMap snd lefts ++ rights+        newRights = concatMap snd lefts ++ rights' findKVarInGuard k p@(Var k' xs)   | k == k' = Left ([(k', xs)], [])   | otherwise = Right p@@ -970,7 +969,7 @@   flatten :: a -> a  instance Flatten (Cstr a) where-  flatten (CAnd cs) = case flatten cs of+  flatten (CAnd cstrs) = case flatten cstrs of                         [c] -> c                         cs -> CAnd cs   flatten (Head p a) = Head (flatten p) a@@ -987,7 +986,7 @@   flatten [] = []  instance Flatten Pred where-  flatten (PAnd ps) = case flatten ps of+  flatten (PAnd preds) = case flatten preds of                         [p] -> p                         ps  -> PAnd ps   flatten p = p@@ -1002,7 +1001,7 @@   flatten []              = []  instance Flatten F.Expr where-  flatten (F.PAnd ps) = case flatten ps of+  flatten (F.PAnd exprs) = case flatten exprs of                          [p] -> p                          ps  -> F.PAnd ps   flatten p = p@@ -1018,16 +1017,16 @@ -- | Split heads into one for each kvar so that queries are always horn constraints hornify :: Cstr a -> Cstr a hornify (Head (PAnd ps) a) = CAnd (flip Head a <$> ps')-  where ps' = let (ks, qs) = split [] [] (flatten ps) in PAnd qs : ks+  where ps' = let (ks, qs) = splitP [] [] (flatten ps) in PAnd qs : ks -        split kacc pacc ((Var x xs):qs) = split (Var x xs : kacc) pacc qs-        split kacc pacc (q:qs) = split kacc (q:pacc) qs-        split kacc pacc [] = (kacc, pacc)-hornify (Head (Reft r) a) = CAnd (flip Head a <$> (Reft (F.PAnd ps):(Reft <$> ks)))-  where (ks, ps) = split [] [] $ F.splitPAnd r-        split kacc pacc (r@F.PKVar{}:rs) = split (r:kacc) pacc rs-        split kacc pacc (r:rs) = split kacc (r:pacc) rs-        split kacc pacc [] = (kacc,pacc)+        splitP kacc pacc ((Var x xs):qs) = splitP (Var x xs : kacc) pacc qs+        splitP kacc pacc (q:qs) = splitP kacc (q:pacc) qs+        splitP kacc pacc [] = (kacc, pacc)+hornify (Head (Reft expr) a) = CAnd (flip Head a <$> (Reft (F.PAnd ps):(Reft <$> ks)))+  where (ks, ps) = splitP [] [] $ F.splitPAnd expr+        splitP kacc pacc (r@F.PKVar{}:rs) = splitP (r:kacc) pacc rs+        splitP kacc pacc (r:rs) = splitP kacc (r:pacc) rs+        splitP kacc pacc [] = (kacc,pacc) hornify (Head h a) = Head h a hornify (All b c) = All b $ hornify c hornify (Any b c) = Any b $ hornify c

@@ -9,8 +9,6 @@ {-# LANGUAGE DeriveGeneric              #-} {-# LANGUAGE DeriveTraversable          #-} -{-# OPTIONS_GHC -Wno-name-shadowing #-}- module Language.Fixpoint.Horn.Types   ( -- * Horn Constraints and their components     Query (..)@@ -231,13 +229,13 @@   toJSON (Tag s) = String (T.pack s)  instance F.PPrint (Query a) where-  pprintPrec k t q = P.vcat $ L.intersperse " "+  pprintPrec prec t q = P.vcat $ L.intersperse " "     [ P.vcat   (ppQual <$> qQuals q)     , P.vcat   [ppVar k   | k <- qVars q]-    , P.vcat   [ppCon x t | (x, t) <- M.toList (qCon q)]+    , P.vcat   [ppCon x sort' | (x, sort') <- M.toList (qCon q)]     , ppThings Nothing (qEqns  q)     , ppThings (Just "data ") (qData  q)-    , P.parens (P.vcat ["constraint", F.pprintPrec (k+2) t (qCstr q)])+    , P.parens (P.vcat ["constraint", F.pprintPrec (prec+2) t (qCstr q)])     ]  ppThings :: F.PPrint a => Maybe P.Doc -> [a] -> P.Doc

@@ -7,8 +7,6 @@  {-# LANGUAGE ScopedTypeVariables #-} -{-# OPTIONS_GHC -Wno-name-shadowing #-}- module Language.Fixpoint.Minimize ( minQuery, minQuals, minKvars ) where  import Prelude hiding (min, init)

@@ -5,8 +5,6 @@ {-# LANGUAGE DeriveGeneric             #-} {-# LANGUAGE OverloadedStrings         #-} -{-# OPTIONS_GHC -Wno-name-shadowing #-}- module Language.Fixpoint.Parse (    -- * Top Level Class for Parseable Values@@ -1026,9 +1024,9 @@   <|> (mkFTycon          =<<  locUpperIdP)  mkFTycon :: LocSymbol -> Parser FTycon-mkFTycon locSym = do+mkFTycon locSymbol = do   nums  <- gets numTyCons-  return (symbolNumInfoFTyCon locSym (val locSym `S.member` nums) False)+  return (symbolNumInfoFTyCon locSymbol (val locSymbol `S.member` nums) False)   --------------------------------------------------------------------------------

@@ -8,8 +8,6 @@ {-# LANGUAGE PatternGuards             #-} {-# LANGUAGE DoAndIfThenElse           #-} -{-# OPTIONS_GHC -Wno-name-shadowing #-}- -- | This module contains an SMTLIB2 interface for --   1. checking the validity, and, --   2. computing satisfying assignments@@ -272,17 +270,17 @@   -> Process.Config   -> IO (SMTLIB.Backends.Backend, IO ()) makeProcess ctxLog cfg-  = do handle@Process.Handle {hMaybeErr = Just hErr, ..} <- Process.new cfg+  = do handl@Process.Handle {hMaybeErr = Just hErr, ..} <- Process.new cfg        case ctxLog of          Nothing -> return ()          Just hLog -> void $ async $ forever-           (do err <- LTIO.hGetLine hErr-               LTIO.hPutStrLn hLog $ "OOPS, SMT solver error:" <> err+           (do errTxt <- LTIO.hGetLine hErr+               LTIO.hPutStrLn hLog $ "OOPS, SMT solver error:" <> errTxt            ) `catch` \ SomeException {} -> return ()-       let backend = Process.toBackend handle+       let backend = Process.toBackend handl        hSetBuffering hOut $ BlockBuffering $ Just $ 1024 * 1024 * 64        hSetBuffering hIn $ BlockBuffering $ Just $ 1024 * 1024 * 64-       return (backend, Process.close handle)+       return (backend, Process.close handl)  makeContext' :: Config -> Maybe Handle -> IO Context makeContext' cfg ctxLog@@ -399,12 +397,12 @@ smtAssert me p  = interact' me (Assert Nothing p)  smtDefineFunc :: Context -> Symbol -> [(Symbol, F.Sort)] -> F.Sort -> Expr -> IO ()-smtDefineFunc me name params rsort e =+smtDefineFunc me name symList rsort e =   let env = seData (ctxSymEnv me)    in interact' me $         DefineFunc           name-          (map (sortSmtSort False env <$>) params)+          (map (sortSmtSort False env <$>) symList)           (sortSmtSort False env rsort)           e 

@@ -6,7 +6,6 @@ {-# LANGUAGE DoAndIfThenElse      #-}  {-# OPTIONS_GHC -Wno-orphans        #-}-{-# OPTIONS_GHC -Wno-name-shadowing #-}  -- | This module contains the code for serializing Haskell values --   into SMTLIB2 format, that is, the instances for the @SMTLIB2@@@ -153,9 +152,9 @@   smt2 env (PImp p q)       = parenSeqs ["=>", smt2 env p, smt2 env q]   smt2 env (PIff p q)       = parenSeqs ["=", smt2 env p, smt2 env q]   smt2 env (PExist [] p)    = smt2 env p-  smt2 env (PExist bs p)    = parenSeqs ["exists", parens (smt2s env bs), smt2 env p]+  smt2 env (PExist xs p)    = parenSeqs ["exists", parens (smt2s env xs), smt2 env p]   smt2 env (PAll   [] p)    = smt2 env p-  smt2 env (PAll   bs p)    = parenSeqs ["forall", parens (smt2s env bs), smt2 env p]+  smt2 env (PAll   xs p)    = parenSeqs ["forall", parens (smt2s env xs), smt2 env p]   smt2 env (PAtom r e1 e2)  = mkRel env r e1 e2   smt2 env (ELam b e)       = smt2Lam   env b e   smt2 env (ECoerc t1 t2 e) = smt2Coerc env t1 t2 e@@ -231,8 +230,8 @@   smt2 env (DeclData ds)       = key "declare-datatypes" (smt2data env ds)   smt2 env (Declare x ts t)    = parenSeqs ["declare-fun", Builder.fromText x, parens (smt2many (smt2 env <$> ts)), smt2 env t]   smt2 env c@(Define t)        = key "declare-sort" (smt2SortMono c env t)-  smt2 env (DefineFunc name params rsort e) =-    let bParams = [ parenSeqs [smt2 env s, smt2 env t] | (s, t) <- params]+  smt2 env (DefineFunc name paramxs rsort e) =+    let bParams = [ parenSeqs [smt2 env s, smt2 env t] | (s, t) <- paramxs]      in parenSeqs ["define-fun", smt2 env name, parenSeqs bParams, smt2 env rsort, smt2 env e]   smt2 env (Assert Nothing p)  = {-# SCC "smt2-assert" #-} key "assert" (smt2 env p)   smt2 env (Assert (Just i) p) = {-# SCC "smt2-assert" #-} key "assert" (parens ("!"<+> smt2 env p <+> ":named p-" <> bShow i))@@ -251,14 +250,14 @@ instance SMTLIB2 (Triggered Expr) where   smt2 env (TR NoTrigger e)       = smt2 env e   smt2 env (TR _ (PExist [] p))   = smt2 env p-  smt2 env t@(TR _ (PExist bs p)) = smtTr env "exists" bs p t+  smt2 env t@(TR _ (PExist xs p)) = smtTr env "exists" xs p t   smt2 env (TR _ (PAll   [] p))   = smt2 env p-  smt2 env t@(TR _ (PAll   bs p)) = smtTr env "forall" bs p t+  smt2 env t@(TR _ (PAll   xs p)) = smtTr env "forall" xs p t   smt2 env (TR _ e)               = smt2 env e  {-# INLINE smtTr #-} smtTr :: SymEnv -> Builder -> [(Symbol, Sort)] -> Expr -> Triggered Expr -> Builder-smtTr env q bs p t = key q (parens (smt2s env bs) <+> key "!" (smt2 env p <+> ":pattern" <> parens (smt2s env (makeTriggers t))))+smtTr env q xs p t = key q (parens (smt2s env xs) <+> key "!" (smt2 env p <+> ":pattern" <> parens (smt2s env (makeTriggers t))))  {-# INLINE smt2s #-} smt2s    :: SMTLIB2 a => SymEnv -> [a] -> Builder

@@ -7,7 +7,6 @@ {-# LANGUAGE ViewPatterns              #-}  {-# OPTIONS_GHC -Wno-orphans           #-}-{-# OPTIONS_GHC -Wno-name-shadowing    #-}  module Language.Fixpoint.Smt.Theories      (@@ -443,9 +442,9 @@   | f == setEmp   = Just (key2 "=" (fromText emp) d)   | f == setSng   = Just (key (fromText sng) d) -- Just (key2 (bb add) (bb emp) d) -smt2App k env f (d:ds)+smt2App k env f (builder:builders)   | Just fb <- smt2AppArg k env f-  = Just $ key fb (d <> mconcat [ " " <> d | d <- ds])+  = Just $ key fb (builder <> mconcat [ " " <> d | d <- builders])  smt2App _ _ _ _    = Nothing 

@@ -4,7 +4,6 @@ {-# LANGUAGE OverloadedStrings         #-} {-# LANGUAGE UndecidableInstances      #-} -{-# OPTIONS_GHC -Wno-name-shadowing    #-}  -- | This module contains the types defining an SMTLIB2 interface. @@ -74,8 +73,8 @@ ppCmd (Declare x [] t) = text "Declare" <+> text (T.unpack x) <+> text ":" <+> pprint t ppCmd (Declare x ts t) = text "Declare" <+> text (T.unpack x) <+> text ":" <+> parens (pprint ts) <+> pprint t ppCmd Define {}   = text "Define ..."-ppCmd (DefineFunc name params rsort e) =-  text "DefineFunc" <+> pprint name <+> pprint params <+> pprint rsort <+> pprint e+ppCmd (DefineFunc name symList rsort e) =+  text "DefineFunc" <+> pprint name <+> pprint symList <+> pprint rsort <+> pprint e ppCmd (Assert _ e)  = text "Assert" <+> pprint e ppCmd (AssertAx _)  = text "AssertAxiom ..." ppCmd Distinct {} = text "Distinct ..."

@@ -6,8 +6,6 @@ {-# LANGUAGE OverloadedStrings   #-} {-# LANGUAGE ScopedTypeVariables #-} -{-# OPTIONS_GHC -Wno-name-shadowing #-}- module Language.Fixpoint.Solver (     -- * Invoke Solver on an FInfo     solve, Solver@@ -188,11 +186,11 @@                              (return . crashResult (errorMap fi0))  crashResult :: (PPrint a) => ErrorMap a -> Error -> Result (Integer, a)-crashResult m e = Result res mempty mempty mempty+crashResult m err' = Result res mempty mempty mempty   where     res           = Crash es msg-    es            = catMaybes [ findError m e | e <- errs e ]-    msg | null es = showpp e+    es            = catMaybes [ findError m e | e <- errs err' ]+    msg | null es = showpp err'         | otherwise = "Sorry, unexpected panic in liquid-fixpoint!" -- ++ showpp e  -- | Unpleasant hack to save meta-data that can be recovered from SrcSpan

@@ -1,7 +1,5 @@ {-# LANGUAGE OverloadedStrings #-} -{-# OPTIONS_GHC -Wno-name-shadowing #-}- module Language.Fixpoint.Solver.Common (askSMT, toSMT) where  import Language.Fixpoint.Types.Config (Config)@@ -15,20 +13,20 @@ mytracepp = notracepp  askSMT :: Config -> Context -> [(Symbol, Sort)] -> Expr -> IO Bool-askSMT cfg ctx bs e+askSMT cfg ctx xs e --   | isContraPred e  = return False   | isTautoPred  e     = return True   | null (kvarsExpr e) = checkValidWithContext ctx [] PTrue e'   | otherwise          = return False   where-    e' = toSMT "askSMT" cfg ctx bs e+    e' = toSMT "askSMT" cfg ctx xs e  toSMT :: String -> Config -> Context -> [(Symbol, Sort)] -> Expr -> Pred-toSMT msg cfg ctx bs e =-    defuncAny cfg senv .-        elaborate (dummyLoc msg) (elabEnv bs) .+toSMT msg cfg ctx xs e =+    defuncAny cfg symenv .+        elaborate (dummyLoc msg) (elabEnv xs) .             mytracepp ("toSMT from " ++ msg ++ showpp e) $                 e   where-    elabEnv = insertsSymEnv senv-    senv    = ctxSymEnv ctx+    elabEnv = insertsSymEnv symenv+    symenv  = ctxSymEnv ctx

@@ -6,8 +6,6 @@ {-# LANGUAGE ViewPatterns #-} {-# LANGUAGE TupleSections #-} -{-# OPTIONS_GHC -Wno-name-shadowing #-}- -- | Functions to make environments smaller module Language.Fixpoint.Solver.EnvironmentReduction   ( reduceEnvironments@@ -136,19 +134,19 @@ -- See #473 for more discussion. -- reduceEnvironments :: FInfo a -> FInfo a-reduceEnvironments fi =-  let constraints = HashMap.Strict.toList $ cm fi-      aenvMap = axiomEnvSymbols (ae fi)-      reducedEnvs = map (reduceConstraintEnvironment (bs fi) aenvMap) constraints-      (cm', ws') = reduceWFConstraintEnvironments (bs fi) (reducedEnvs, ws fi)-      bs' = (bs fi) { beBinds = dropBindsMissingFrom (beBinds $ bs fi) cm' ws' }+reduceEnvironments finfo =+  let constraints = HashMap.Strict.toList $ cm finfo+      aenvMap = axiomEnvSymbols (ae finfo)+      reducedEnvs = map (reduceConstraintEnvironment (bs finfo) aenvMap) constraints+      (cm', ws') = reduceWFConstraintEnvironments (bs finfo) (reducedEnvs, ws finfo)+      bs' = (bs finfo) { beBinds = dropBindsMissingFrom (beBinds $ bs finfo) cm' ws' } -   in fi+   in finfo      { bs = bs'      , cm = HashMap.fromList cm'      , ws = ws'-     , ebinds = updateEbinds bs' (ebinds fi)-     , bindInfo = updateBindInfoKeys bs' $ bindInfo fi+     , ebinds = updateEbinds bs' (ebinds finfo)+     , bindInfo = updateBindInfoKeys bs' $ bindInfo finfo      }    where@@ -157,10 +155,10 @@       -> [(SubcId, SubC a)]       -> HashMap KVar (WfC a)       -> HashMap BindId (Symbol, SortedReft, a)-    dropBindsMissingFrom be cs ws =+    dropBindsMissingFrom be cs wmap =       let ibindEnv = unionsIBindEnv $             map (senv . snd) cs ++-            map wenv (HashMap.elems ws)+            map wenv (HashMap.elems wmap)        in           HashMap.filterWithKey (\bId _ -> memberIBindEnv bId ibindEnv) be @@ -200,7 +198,7 @@        ws' =         HashMap.mapWithKey-          (reduceWFConstraintEnvironment bindEnv kvarsRelevantBinds)+          (reduceWFConstraintEnvironment kvarsRelevantBinds)           wfs        wsSymbols = HashMap.map (asSymbolSet bindEnv . wenv) ws'@@ -209,7 +207,7 @@         HashMap.unionWith HashSet.intersection wfBindsPlusSortSymbols wsSymbols        cs' = zipWith-              (updateSubcEnvsWithKVarBinds bindEnv kvarsWsBinds)+              (updateSubcEnvsWithKVarBinds kvarsWsBinds)               kvarsBySubC               cs    in@@ -221,23 +219,22 @@     -- additional bindings that are required by the kvar. These are added     -- in this function.     updateSubcEnvsWithKVarBinds-      :: BindEnv a-      -> HashMap KVar (HashSet Symbol)+      :: HashMap KVar (HashSet Symbol)       -> [KVar]       -> ReducedConstraint a       -> (SubcId, SubC a)-    updateSubcEnvsWithKVarBinds be kvarsBinds kvs c =+    updateSubcEnvsWithKVarBinds kvarsBinds kvs c =       let updateIBindEnv oldEnv =             unionIBindEnv (reducedEnv c) $             if null kvs then emptyIBindEnv             else fromListIBindEnv               [ bId               | bId <- elemsIBindEnv oldEnv-              , let (s, _sr, _) = lookupBindEnv bId be+              , let (s, _sr, _) = lookupBindEnv bId bindEnv               , any (neededByKVar s) kvs               ]-          neededByKVar s kv =-            case HashMap.lookup kv kvarsBinds of+          neededByKVar s kvar =+            case HashMap.lookup kvar kvarsBinds of               Nothing -> False               Just kbindSyms -> HashSet.member s kbindSyms        in (constraintId c, updateSEnv (originalConstraint c) updateIBindEnv)@@ -245,12 +242,11 @@     -- @reduceWFConstraintEnvironment be kbinds k c@ drops bindings from @c@     -- that aren't present in @kbinds ! k@.     reduceWFConstraintEnvironment-      :: BindEnv a-      -> HashMap KVar (HashSet Symbol)+      :: HashMap KVar (HashSet Symbol)       -> KVar       -> WfC a       -> WfC a-    reduceWFConstraintEnvironment bindEnv kvarBinds k c =+    reduceWFConstraintEnvironment kvarBinds k c =       case HashMap.lookup k kvarBinds of         Nothing -> c { wenv = emptyIBindEnv }         Just kbindSymbols ->@@ -320,10 +316,10 @@  -- | For each Equation and Rewrite, collects the symbols that it needs. axiomEnvSymbols :: AxiomEnv -> HashMap Symbol (HashSet Symbol)-axiomEnvSymbols ae =+axiomEnvSymbols axiomEnv =   HashMap.union-    (HashMap.fromList $ map eqSymbols $ aenvEqs ae)-    (HashMap.fromList $ map rewriteSymbols $ aenvSimpl ae)+    (HashMap.fromList $ map eqSymbols $ aenvEqs axiomEnv)+    (HashMap.fromList $ map rewriteSymbols $ aenvSimpl axiomEnv)   where     eqSymbols eq =       let bodySymbols =@@ -461,13 +457,13 @@ -- If 'inlineANFBindings cfg' is on, also runs 'undoANFAndVV' to inline -- @lq_anf@ bindings. simplifyBindings :: Config -> FInfo a -> FInfo a-simplifyBindings cfg fi =-  let (bs', cm', oldToNew) = simplifyConstraints (bs fi) (cm fi)-   in fi+simplifyBindings cfg finfo =+  let (bs', cm', oldToNew) = simplifyConstraints (bs finfo) (cm finfo)+   in finfo         { bs = bs'         , cm = cm'-        , ebinds = updateEbinds oldToNew (ebinds fi)-        , bindInfo = updateBindInfoKeys oldToNew $ bindInfo fi+        , ebinds = updateEbinds oldToNew (ebinds finfo)+        , bindInfo = updateBindInfoKeys oldToNew $ bindInfo finfo         }   where     updateEbinds :: HashMap BindId [BindId] -> [BindId] -> [BindId]@@ -518,7 +514,7 @@            modifiedBinds = HashMap.toList $ HashMap.union boolSimplEnv undoANFEnv -          modifiedBindIds = [ fst <$> bs | (_, (bs,_)) <- modifiedBinds ]+          modifiedBindIds = [ fst <$> bindIds | (_, (bindIds,_)) <- modifiedBinds ]            unchangedBindIds = senv c `diffIBindEnv` fromListIBindEnv (concat modifiedBindIds) @@ -632,10 +628,10 @@   -> SortedReft   -> SortedReft inlineInSortedReft srLookup sr =-    let reft = sr_reft sr-     in sr { sr_reft = mapPredReft (inlineInExpr (filterBind (reftBind reft) srLookup)) reft }+    let reft' = sr_reft sr+     in sr { sr_reft = mapPredReft (inlineInExpr (filterBind (reftBind reft'))) reft' }   where-    filterBind b srLookup sym = do+    filterBind b sym = do       guard (sym /= b)       srLookup sym @@ -713,7 +709,7 @@     findExpr e es = do       case partition (e ==) es of         ([], _) -> Nothing-        (e:_, rest) -> Just (e, rest)+        (f:_, rest) -> Just (f, rest)  -- | @dropLikelyIrrelevantBindings ss env@ is like @dropIrrelevantBindings@ -- but drops bindings that could potentially be necessary to validate a

@@ -3,7 +3,6 @@ {-# LANGUAGE PatternGuards        #-} {-# LANGUAGE FlexibleContexts     #-} -{-# OPTIONS_GHC -Wno-name-shadowing #-} {-# LANGUAGE MultiParamTypeClasses #-}  module Language.Fixpoint.Solver.Extensionality (expand) where@@ -58,22 +57,22 @@   extendExpr :: a -> Pos -> Expr -> Ex a Expr-extendExpr ann p e+extendExpr ann p expr'   | p == Pos   = mapMPosExpr Pos goP e' >>= mapMPosExpr Pos goN   | otherwise   = mapMPosExpr Neg goP e' >>= mapMPosExpr Neg goN     where-      e' = normalize e+      e' = normalize expr'       goP Pos (PAtom b e1 e2)        | b == Eq || b == Ne        , Just s <- getArg (exprSort "extensionality" e1)-       = mytracepp ("extending POS = " ++ showpp e) <$> (extendRHS ann b e1 e2 s >>= goP Pos)+       = mytracepp ("extending POS = " ++ showpp expr') <$> (extendRHS ann b e1 e2 s >>= goP Pos)       goP _ e = return e       goN Neg (PAtom b e1 e2)        | b == Eq || b == Ne        , Just s <- getArg (exprSort "extensionality" e1)-       = mytracepp ("extending NEG = " ++ showpp e) <$> (extendLHS ann b e1 e2 s >>= goN Neg)+       = mytracepp ("extending NEG = " ++ showpp expr') <$> (extendLHS ann b e1 e2 s >>= goN Neg)       goN _ e = return e  getArg :: Sort -> Maybe Sort@@ -93,9 +92,9 @@      mytracepp "extendLHS = " . pAnd . (PAtom b e1 e2:) <$> mapM (makeEq b e1 e2) (es ++ is)  generateArguments :: a -> Sort -> Ex a [Expr]-generateArguments ann s = do-  ddecls   <- gets exddecl-  case breakSort ddecls s of+generateArguments ann srt = do+  ddatadecls <- gets exddecl+  case breakSort ddatadecls srt of     Left dds -> mapM (freshArgDD ann) dds     Right s  -> (\x -> [EVar x]) <$> freshArgOne ann s @@ -130,7 +129,7 @@ negatePos Neg = Pos  mapMPosExpr :: (Monad m) => Pos -> (Pos -> Expr -> m Expr) -> Expr -> m Expr-mapMPosExpr p f = go p+mapMPosExpr pos f = go pos   where     go p e@(ESym _)      = f p e     go p e@(ECon _)      = f p e@@ -161,7 +160,7 @@     go p (PGrad k s i e) = f p . PGrad k s i =<< go p e  normalize :: Expr -> Expr-normalize e = mytracepp ("normalize: " ++ showpp e) $ go e+normalize expr' = mytracepp ("normalize: " ++ showpp expr') $ go expr'   where     go e@(ESym _)        = e     go e@(ECon _)        = e@@ -224,19 +223,19 @@   freshArgDD :: a -> (LocSymbol, [Sort]) -> Ex a Expr-freshArgDD ann (dc, xs) = do-  xs <- mapM (freshArgOne ann) xs+freshArgDD ann (dc, sorts) = do+  xs <- mapM (freshArgOne ann) sorts   return $ mkEApp dc (EVar <$> xs)   freshArgOne :: ann -> Sort -> Ex ann Symbol freshArgOne ann s = do-  st   <- get-  let x = symbol ("ext$" ++ show (unique st))-  let (id, benv') = insertBindEnv x (trueSortedReft s) ann (exbenv st)+  exst <- get+  let x = symbol ("ext$" ++ show (unique exst))+  let (bindId, benv') = insertBindEnv x (trueSortedReft s) ann (exbenv exst)   modify (\st -> st{ exenv   = insertSymEnv x s (exenv st)                    , exbenv  = benv'-                   , exbinds = insertsIBindEnv [id] (exbinds st)+                   , exbinds = insertsIBindEnv [bindId] (exbinds st)                    , unique   = 1 + unique st                    , excbs = (x,s) : excbs st                    })@@ -244,9 +243,9 @@   breakSort :: [DataDecl] -> Sort -> Either [(LocSymbol, [Sort])] Sort-breakSort ddecls s+breakSort ddatadecls s     | Just (tc, ts) <- splitTC s-    , [(dds,i)] <- [ (ddCtors dd,ddVars dd) | dd <- ddecls, ddTyCon dd == tc ]+    , [(dds,i)] <- [ (ddCtors dd,ddVars dd) | dd <- ddatadecls, ddTyCon dd == tc ]     = Left ((\dd -> (dcName dd, instSort  (Sub $ zip [0..(i-1)] ts) . dfSort <$> dcFields dd)) <$> dds)     | otherwise     = Right s

@@ -1,8 +1,6 @@ {-# LANGUAGE CPP                #-} {-# LANGUAGE FlexibleInstances  #-} -{-# OPTIONS_GHC -Wno-name-shadowing #-}- module Language.Fixpoint.Solver.GradualSolution   ( -- * Create Initial Solution     init@@ -18,7 +16,7 @@ import           Language.Fixpoint.Misc import qualified Language.Fixpoint.Types              as F import qualified Language.Fixpoint.Types.Solutions    as Sol-import           Language.Fixpoint.Types.Constraints  hiding (ws, bs)+import qualified Language.Fixpoint.Types.Constraints  as Cons import           Prelude                              hiding (init, lookup) import           Language.Fixpoint.Solver.Sanitize  (symbolEnv) import Language.Fixpoint.SortCheck@@ -34,9 +32,9 @@     gs         = snd <$> gs0     genv       = instConstants si -    gs0        = L.filter (isGWfc . snd) $ M.toList (F.ws si)+    gs0        = L.filter (Cons.isGWfc . snd) $ M.toList (F.ws si) -    elab (k, (x,es)) = (k, (x, elaborate (F.atLoc F.dummySpan "init") (sEnv (gsym x) (gsort x)) <$> es))+    elab (k, (x,es)) = (k, (x, elaborate (F.atLoc F.dummySpan "init") (sEnv (Cons.gsym x) (Cons.gsort x)) <$> es))      sEnv x s    = isEnv {F.seSort = F.insertSEnv x s (F.seSort isEnv)}     isEnv       = symbolEnv cfg si@@ -49,7 +47,7 @@     (k, qb) = refine fi qs genv w  refine :: F.SInfo a -> [F.Qualifier] -> F.SEnv F.Sort -> F.WfC a -> (F.KVar, Sol.QBind)-refine fi qs genv w = refineK (allowHOquals fi) env qs $ F.wrft w+refine fi qs genv w = refineK (Cons.allowHOquals fi) env qs $ F.wrft w   where     env             = wenv <> genv     wenv            = F.sr_sort <$> F.fromListSEnv (F.envCs (F.bs fi) (F.wenv w))@@ -85,7 +83,7 @@        -> F.Qualifier        -> [Sol.EQual] instKQ ho env v t q =-  case qpSort <$> F.qParams q of+  case Cons.qpSort <$> F.qParams q of     (qt:qts) -> do         (su0, v0) <- candidates senv [(t, [v])] qt         xs        <- match senv tyss [v0] (So.apply su0 <$> qts)

@@ -17,8 +17,6 @@ {-# LANGUAGE RecordWildCards           #-} {-# LANGUAGE ExistentialQuantification #-} -{-# OPTIONS_GHC -Wno-name-shadowing    #-}- module Language.Fixpoint.Solver.Instantiate (instantiate) where  import           Language.Fixpoint.Types@@ -54,15 +52,15 @@ -- | Strengthen Constraint Environments via PLE -------------------------------------------------------------------------------- instantiate :: (Loc a) => Config -> SInfo a -> Maybe [SubcId] -> IO (SInfo a)-instantiate cfg fi subcIds+instantiate cfg info subcIds   | not (oldPLE cfg)-  = PLE.instantiate cfg fi subcIds+  = PLE.instantiate cfg info subcIds    | noIncrPle cfg-  = instantiate' cfg fi subcIds+  = instantiate' cfg info subcIds    | otherwise-  = incrInstantiate' cfg fi subcIds+  = incrInstantiate' cfg info subcIds   -------------------------------------------------------------------------------@@ -79,27 +77,27 @@ ------------------------------------------------------------------------------- incrInstantiate' :: (Loc a) => Config -> SInfo a -> Maybe [SubcId] -> IO (SInfo a) --------------------------------------------------------------------------------incrInstantiate' cfg fi subcIds = do-    let cs = [ (i, c) | (i, c) <- M.toList (cm fi), isPleCstr aEnv i c+incrInstantiate' cfg info subcIds = do+    let cs = [ (i, c) | (i, c) <- M.toList (cm info), isPleCstr aEnv i c                       ,  maybe True (i `L.elem`) subcIds ]     let t  = mkCTrie cs                                               -- 1. BUILD the Trie     res   <- withProgress (1 + length cs) $-               withCtx cfg file sEnv (pleTrie t . instEnv cfg fi cs)  -- 2. TRAVERSE Trie to compute InstRes-    return $ resSInfo cfg sEnv fi res                                 -- 3. STRENGTHEN SInfo using InstRes+               withCtx cfg file sEnv (pleTrie t . instEnv cfg info cs)  -- 2. TRAVERSE Trie to compute InstRes+    return $ resSInfo cfg sEnv info res                                 -- 3. STRENGTHEN SInfo using InstRes   where     file   = srcFile cfg ++ ".evals"-    sEnv   = symbolEnv cfg fi-    aEnv   = ae fi+    sEnv   = symbolEnv cfg info+    aEnv   = ae info    ------------------------------------------------------------------------------- -- | Step 1a: @instEnv@ sets up the incremental-PLE environment instEnv :: (Loc a) => Config -> SInfo a -> [(SubcId, SimpC a)] -> SMT.Context -> InstEnv a-instEnv cfg fi cs ctx = InstEnv cfg ctx bEnv aEnv (M.fromList cs) γ s0+instEnv cfg info cs ctx = InstEnv cfg ctx bEnv aEnv (M.fromList cs) γ s0   where-    bEnv              = bs fi-    aEnv              = ae fi+    bEnv              = bs info+    aEnv              = ae info     γ                 = knowledge cfg ctx aEnv     s0                = EvalEnv 0 [] aEnv (SMT.ctxSymEnv ctx) cfg @@ -161,7 +159,7 @@ unfoldPred cfg ctx = toSMT cfg ctx [] . pAnd . concatMap snd  evalCandsLoop :: Config -> SMT.Context -> Knowledge -> EvalEnv -> [Expr] -> IO [Unfold]-evalCandsLoop cfg ctx γ s0 cands = go [] cands+evalCandsLoop cfg ctx γ s0 = go []   where     go acc []    = return acc     go acc cands = do eqss   <- SMT.smtBracket ctx "PLE.evaluate" $ do@@ -180,7 +178,7 @@ -- | Step 3: @resSInfo@ uses incremental PLE result @InstRes@ to produce the strengthened SInfo  resSInfo :: Config -> SymEnv -> SInfo a -> InstRes -> SInfo a-resSInfo cfg env fi res = strengthenBinds fi res'+resSInfo cfg env info res = strengthenBinds info res'   where     res'     = M.fromList $ mytracepp  "ELAB-INST:  " $ zip is ps''     ps''     = zipWith (\i -> elaborate (atLoc dummySpan ("PLE1 " ++ show i)) env) is ps'@@ -258,11 +256,11 @@                ]  debugResult :: InstEnv a -> InstRes -> SubcId -> String-debugResult InstEnv{..} res i = msg+debugResult InstEnv{..} res subId = msg   where-    msg                          = "INCR-INSTANTIATE i = " ++ show i ++ ": " ++ showpp cidEqs+    msg                          = "INCR-INSTANTIATE i = " ++ show subId ++ ": " ++ showpp cidEqs     cidEqs                       = pAnd [ e | i <- cBinds, e <- Mb.maybeToList $ M.lookup i res ]-    cBinds                       = L.sort . elemsIBindEnv . senv . getCstr ieCstrs $ i+    cBinds                       = L.sort . elemsIBindEnv . senv . getCstr ieCstrs $ subId   updRes :: InstRes -> Maybe BindId -> Expr -> InstRes@@ -298,35 +296,35 @@ -- | "Old" GLOBAL PLE -------------------------------------------------------------------------------- instantiate' :: (Loc a) => Config -> SInfo a -> Maybe [SubcId] -> IO (SInfo a)-instantiate' cfg fi subcIds = sInfo cfg env fi <$> withCtx cfg file env act+instantiate' cfg info subcIds = sInfo cfg env info <$> withCtx cfg file env act   where     act ctx         = forM cstrs $ \(i, c) ->-                        ((i,srcSpan c),) . mytracepp  ("INSTANTIATE i = " ++ show i) <$> instSimpC cfg ctx (bs fi) aenv i c-    cstrs           = [ (i, c) | (i, c) <- M.toList (cm fi) , isPleCstr aenv i c+                        ((i,srcSpan c),) . mytracepp  ("INSTANTIATE i = " ++ show i) <$> instSimpC cfg ctx (bs info) aenv i c+    cstrs           = [ (i, c) | (i, c) <- M.toList (cm info) , isPleCstr aenv i c                                ,  maybe True (i `L.elem`) subcIds ]     file            = srcFile cfg ++ ".evals"-    env             = symbolEnv cfg fi-    aenv            = {- mytracepp  "AXIOM-ENV" -} ae fi+    env             = symbolEnv cfg info+    aenv            = {- mytracepp  "AXIOM-ENV" -} ae info  sInfo :: Config -> SymEnv -> SInfo a -> [((SubcId, SrcSpan), Expr)] -> SInfo a-sInfo cfg env fi ips = strengthenHyp fi (mytracepp  "ELAB-INST:  " $ zip (fst <$> is) ps'')+sInfo cfg env info ips = strengthenHyp info (mytracepp  "ELAB-INST:  " $ zip (fst <$> is) ps'')   where     (is, ps)         = unzip ips     ps'              = defuncAny cfg env ps     ps''             = zipWith (\(i, sp) -> elaborate (atLoc sp ("PLE1 " ++ show i)) env) is ps'  instSimpC :: Config -> SMT.Context -> BindEnv a -> AxiomEnv -> SubcId -> SimpC a -> IO Expr-instSimpC cfg ctx bds aenv sid sub-  | isPleCstr aenv sid sub = do+instSimpC cfg ctx bds aenv subId sub+  | isPleCstr aenv subId sub = do     let is0       = mytracepp  "INITIAL-STUFF" $ eqBody <$> L.filter (null . eqArgs) (aenvEqs aenv)     let (bs, es0) = cstrExprs bds sub-    equalities   <- evaluate cfg ctx aenv bs es0 sid+    equalities   <- evaluate cfg ctx aenv bs es0 subId     let evalEqs   = [ EEq e1 e2 | (e1, e2) <- equalities, e1 /= e2 ]     return        $ pAnd (is0 ++ evalEqs)   | otherwise     = return PTrue  isPleCstr :: AxiomEnv -> SubcId -> SimpC a -> Bool-isPleCstr aenv sid c = isTarget c && M.lookupDefault False sid (aenvExpand aenv)+isPleCstr aenv subId c = isTarget c && M.lookupDefault False subId (aenvExpand aenv)  cstrExprs :: BindEnv a -> SimpC a -> ([(Symbol, SortedReft)], [Expr]) cstrExprs bds sub = (second unElabSortedReft <$> binds, unElab <$> es)@@ -343,10 +341,10 @@          -> SubcId                            -- ^ Constraint Id          -> IO [(Expr, Expr)]                 -- ^ Newly unfolded equalities ---------------------------------------------------------------------------------evaluate cfg ctx aenv facts es sid = do+evaluate cfg ctx aenv facts es subId = do   let eqs      = initEqualities ctx aenv facts   let γ        = knowledge cfg ctx aenv-  let cands    = mytracepp  ("evaluate-cands " ++ showpp sid) $ Misc.setNub (concatMap topApps es)+  let cands    = mytracepp  ("evaluate-cands " ++ showpp subId) $ Misc.setNub (concatMap topApps es)   let s0       = EvalEnv 0 [] aenv (SMT.ctxSymEnv ctx) cfg   let ctxEqs   = [ toSMT cfg ctx [] (EEq e1 e2) | (e1, e2)  <- eqs ]               ++ [ toSMT cfg ctx [] (expr xr)   | xr@(_, r) <- facts, null (Vis.kvarsExpr $ reftPred $ sr_reft r) ]@@ -356,7 +354,7 @@   _evalLoop :: Config -> SMT.Context -> Knowledge -> EvalEnv -> [Pred] -> [Expr] -> IO [(Expr, Expr)]-_evalLoop cfg ctx γ s0 ctxEqs cands = loop 0 [] cands+_evalLoop cfg ctx γ s0 ctxEqs = loop 0 []   where     loop _ acc []    = return acc     loop i acc cands = do let eqp = toSMT cfg ctx [] $ pAnd $ equalitiesPred acc@@ -463,7 +461,7 @@ --   TODO: distill a .fq test from the MOSSAKA-hw3 example.  evalArgs :: Knowledge -> CStack -> Expr -> EvalST (Expr, [Expr])-evalArgs γ stk e = go [] e+evalArgs γ stk = go []   where     go acc (EApp f e)       = do f' <- evalOk γ stk f@@ -565,14 +563,14 @@ mkCoSub :: SEnv Sort -> [Sort] -> [Sort] -> Vis.CoSub mkCoSub env eTs xTs = M.fromList [ (x, unite ys) | (x, ys) <- Misc.groupList xys ]   where-    unite ts    = mytracepp ("UNITE: " ++ showpp ts) $ Mb.fromMaybe (uError ts) (unifyTo1 senv ts)-    senv        = mkSearchEnv env+    unite ts    = mytracepp ("UNITE: " ++ showpp ts) $ Mb.fromMaybe (uError ts) (unifyTo1 symToSearch ts)+    symToSearch = mkSearchEnv env     uError ts   = panic ("mkCoSub: cannot build CoSub for " ++ showpp xys ++ " cannot unify " ++ showpp ts)     xys         = mytracepp "mkCoSubXXX" $ Misc.sortNub $ concat $ zipWith matchSorts _xTs _eTs     (_xTs,_eTs) = mytracepp "mkCoSub:MATCH" (xTs, eTs)  matchSorts :: Sort -> Sort -> [(Symbol, Sort)]-matchSorts s1 s2 = mytracepp  ("matchSorts :" ++ showpp (s1, s2)) $ go s1 s2+matchSorts sort1 sort2 = mytracepp  ("matchSorts :" ++ showpp (sort1, sort2)) $ go sort1 sort2   where     go (FObj x)      {-FObj-} y    = [(x, y)]     go (FAbs _ t1)   (FAbs _ t2)   = go t1 t2@@ -603,7 +601,7 @@ eqArgNames = map fst . eqArgs  substPopIf :: [(Symbol, Expr)] -> Expr -> Expr-substPopIf xes e = L.foldl' go e xes+substPopIf xes expr' = L.foldl' go expr' xes   where     go e (x, EIte b e1 e2) = EIte b (subst1 e (x, e1)) (subst1 e (x, e2))     go e (x, ex)           = subst1 e (x, ex)@@ -695,9 +693,9 @@ initEqualities :: SMT.Context -> AxiomEnv -> [(Symbol, SortedReft)] -> [(Expr, Expr)] initEqualities ctx aenv es = concatMap (makeSimplifications (aenvSimpl aenv)) dcEqs   where-    dcEqs                  = Misc.setNub (Mb.catMaybes [getDCEquality senv e1 e2 | EEq e1 e2 <- atoms])+    dcEqs                  = Misc.setNub (Mb.catMaybes [getDCEquality symEnv' e1 e2 | EEq e1 e2 <- atoms])     atoms                  = splitPAnd . expr =<< filter isProof es-    senv                   = SMT.ctxSymEnv ctx+    symEnv'                = SMT.ctxSymEnv ctx  -- AT: Non-obvious needed invariant: askSMT True is always the -- totality-effecting one.@@ -717,7 +715,7 @@      = []  getDCEquality :: SymEnv -> Expr -> Expr -> Maybe (Symbol, [Expr], Expr)-getDCEquality senv e1 e2+getDCEquality sEnv e1 e2   | Just dc1 <- f1   , Just dc2 <- f2   = if dc1 == dc2@@ -730,13 +728,13 @@   | otherwise   = Nothing   where-    (f1, es1) = Misc.mapFst (getDC senv) (splitEApp e1)-    (f2, es2) = Misc.mapFst (getDC senv) (splitEApp e2)+    (f1, es1) = Misc.mapFst (getDC sEnv) (splitEApp e1)+    (f2, es2) = Misc.mapFst (getDC sEnv) (splitEApp e2)  -- TODO: Stringy hacks getDC :: SymEnv -> Expr -> Maybe Symbol-getDC senv (EVar x)-  | isUpperSymbol x && Mb.isNothing (symEnvTheory x senv)+getDC sEnv (EVar x)+  | isUpperSymbol x && Mb.isNothing (symEnvTheory x sEnv)   = Just x getDC _ _   = Nothing@@ -773,11 +771,11 @@  -}  assertSelectors :: Knowledge -> Expr -> EvalST ()-assertSelectors γ e = do+assertSelectors γ expr' = do     sims <- gets (aenvSimpl . _evAEnv)     -- cfg  <- gets evCfg     -- _    <- foldlM (\_ s -> Vis.mapMExpr (go s) e) (mytracepp  "assertSelector" e) sims-    forM_ sims $ \s -> Vis.mapMExpr (go s) e+    forM_ sims $ \s -> Vis.mapMExpr (go s) expr'   where     go :: Rewrite -> Expr -> EvalST Expr     go (SMeasure f dc xs bd) e@(EApp _ _)

@@ -100,9 +100,13 @@     getOp _        = Nothing      cfR :: Bop -> Double -> Double -> Maybe Expr-    cfR bop left right = fmap go (getOp' bop)+    cfR bop left right = go (getOp' bop)       where-        go f = ECon $ R $ f left right+        go (Just f) =+          let x = f left right+           in if isNaN x || isInfinite x then Just $ ECon (R x)+              else Nothing+        go Nothing = Nothing          getOp' Div      = Just (/)         getOp' RDiv     = Just (/)

@@ -9,8 +9,6 @@ {-# LANGUAGE BangPatterns          #-} {-# LANGUAGE RankNTypes            #-} -{-# OPTIONS_GHC -Wno-name-shadowing #-}- -- | This module has the functions that perform sort-checking, and related -- operations on Fixpoint expressions and predicates. 

@@ -5,7 +5,7 @@ import qualified SimplifyInterpreter import Test.Tasty   ( TestTree,-    localOption,+    adjustOption,     testGroup,   ) import Test.Tasty.QuickCheck@@ -24,7 +24,10 @@       [ testProperty "computes a fixpoint" (prop_fixpoint SimplifyInterpreter.interpret')       ]   where-    withOptions tests' = localOption (QuickCheckMaxSize 4) (localOption (QuickCheckTests 500) tests')+    withOptions tests' =+      adjustOption (\(QuickCheckMaxSize n) -> QuickCheckMaxSize (div n 4)) $+      adjustOption (\(QuickCheckTests n) -> QuickCheckTests (n * 20))+      tests'  prop_fixpoint :: (Expr -> Expr) -> Expr -> Property prop_fixpoint f e = f e === f (f e)