liquid-fixpoint 0.7.0.5 → 0.7.0.6

raw patch · 29 files changed

+689/−421 lines, 29 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• liquid-fixpoint.cabal +1/−1
• src/Language/Fixpoint/Minimize.hs +0/−5
• src/Language/Fixpoint/Misc.hs +5/−0
• src/Language/Fixpoint/Parse.hs +22/−4
• src/Language/Fixpoint/Smt/Interface.hs +8/−1
• src/Language/Fixpoint/Smt/Serialize.hs +1/−0
• src/Language/Fixpoint/Smt/Theories.hs +35/−61
• src/Language/Fixpoint/Solver.hs +15/−7
• src/Language/Fixpoint/Solver/GradualSolution.hs +10/−3
• src/Language/Fixpoint/Solver/Instantiate.hs +207/−113
• src/Language/Fixpoint/Solver/Solve.hs +5/−128
• src/Language/Fixpoint/SortCheck.hs +105/−20
• src/Language/Fixpoint/Types/Config.hs +34/−35
• src/Language/Fixpoint/Types/Constraints.hs +60/−34
• src/Language/Fixpoint/Types/Names.hs +6/−2
• src/Language/Fixpoint/Types/Refinements.hs +6/−1
• src/Language/Fixpoint/Types/Sorts.hs +5/−2
• src/Language/Fixpoint/Types/Spans.hs +7/−2
• src/Language/Fixpoint/Types/Substitutions.hs +5/−2
• src/Language/Fixpoint/Types/Visitor.hs +2/−0
• tests/neg/maps.fq +37/−0
• tests/pos/EqConstr0.fq +10/−0
• tests/pos/EqConstr1.fq +13/−0
• tests/pos/adt_pair_cast.fq +13/−0
• tests/pos/coerce0.fq +12/−0
• tests/pos/coerce1.fq +11/−0
• tests/pos/empty.fq +13/−0
• tests/pos/maps.fq +37/−0
• tests/testParser.hs +4/−0

@@ -1,5 +1,5 @@ name:                liquid-fixpoint-version:             0.7.0.5+version:             0.7.0.6 Copyright:           2010-17 Ranjit Jhala, University of California, San Diego. synopsis:            Predicate Abstraction-based Horn-Clause/Implication Constraint Solver homepage:            https://github.com/ucsd-progsys/liquid-fixpoint

@@ -13,7 +13,6 @@ import           Control.Monad                      (filterM) import           Language.Fixpoint.Types.Visitor    (mapKVars) import           Language.Fixpoint.Types.Config     (Config (..), queryFile)-import           Language.Fixpoint.Types.Errors import           Language.Fixpoint.Misc             (safeHead) import           Language.Fixpoint.Utils.Files      hiding (Result) import           Language.Fixpoint.Graph@@ -116,10 +115,6 @@ --------------------------------------------------------------------------- -- Helper functions ----------------------------------------------------------------------------isSafe :: Result a -> Bool-isSafe (Result Safe _ _) = True-isSafe _                 = False- addExt :: Ext -> Config -> Config addExt ext cfg = cfg { srcFile = queryFile ext cfg } 

@@ -399,6 +399,11 @@ powerset :: [a] -> [[a]] powerset xs = filterM (const [False, True]) xs +(=>>) :: Monad m => m b -> (b -> m a) -> m b+(=>>) m f = m >>= (\x -> f x >> return x)++(<<=) :: Monad m => (b -> m a) -> m b -> m b+(<<=) = flip (=>>)  (<$$>) ::  (Monad m) => (a -> m b) -> [a] -> m [b] _ <$$> []           = return []

@@ -158,6 +158,7 @@    -- reserved words used in liquid haskell   , "forall"+  , "coerce"   , "exists"   , "module"   , "spec"@@ -195,6 +196,7 @@   , "type"   , "using"   , "with"+  , "in"   ]  reservedOpNames :: [String]@@ -351,6 +353,7 @@   =  trueP  <|> falseP  <|> (fastIfP EIte exprP)+ <|> (coerceP exprP)  <|> (ESym <$> symconstP)  <|> (ECon <$> constantP)  <|> (reservedOp "_|_" >> return EBot)@@ -383,6 +386,15 @@        b2 <- bodyP        return $ f p b1 b2 +coerceP :: Parser Expr -> Parser Expr+coerceP p = do+  reserved "coerce"+  (s, t) <- parens (pairP sortP (reservedOp "~") sortP)+  e      <- p+  return $ ECoerc s t e+++ {- qmIfP f bodyP   = parens $ do@@ -694,13 +706,14 @@ qualifierP tP = do   pos    <- getPosition   n      <- upperIdP-  params <- parens $ sepBy1 (sortBindP tP) comma+  params <- parens $ sepBy1 (symBindP tP) comma   _      <- colon   body   <- predP   return  $ mkQual n params body pos-  where-    sortBindP = pairP symbolP colon +symBindP :: Parser a -> Parser (Symbol, a)+symBindP = pairP symbolP colon+ pairP :: Parser a -> Parser z -> Parser b -> Parser (a, b) pairP xP sepP yP = (,) <$> xP <* sepP <*> yP @@ -714,7 +727,12 @@ ---------------------------------------------------------------------  defineP :: Parser Equation-defineP = Equ <$> symbolP <*> many symbolP <*> (reserved "=" >> exprP)+defineP = do+  name   <- symbolP+  params <- parens        $ sepBy (symBindP sortP) comma+  sort   <- colon        *> sortP+  body   <- reserved "=" *> predP+  return  $ mkEquation name params body sort  matchP :: Parser Rewrite matchP = SMeasure <$> symbolP <*> symbolP <*> many symbolP <*> (reserved "=" >> exprP)

@@ -80,6 +80,7 @@ import           Data.Char import qualified Data.HashMap.Strict      as M import           Data.Monoid+import           Data.Maybe                  (fromMaybe) import qualified Data.Text                as T import           Data.Text.Format import qualified Data.Text.IO             as TIO@@ -442,9 +443,15 @@     thyXTs     =                    filter (isKind 1) xts     qryXTs     = Misc.mapSnd tx <$> filter (isKind 2) xts     isKind n   = (n ==)  . symKind env . fst-    xts        = F.toListSEnv           (F.seSort env)+    xts        = symbolSorts (F.seSort env) -- F.toListSEnv           (F.seSort env)     tx         = elaborate    "declare" env     ats        = funcSortVars env++symbolSorts :: F.SEnv F.Sort -> [(F.Symbol, F.Sort)]+symbolSorts env = [(x, tx t) | (x, t) <- F.toListSEnv env ]+ where+  tx t@(FObj a) = fromMaybe t (F.lookupSEnv a env)+  tx t          = t  dataDeclarations :: SymEnv -> [DataDecl] dataDeclarations = -- (if True then orderDeclarations else id) .

@@ -139,6 +139,7 @@   smt2 env (PAll   bs p)    = build "(forall ({}) {})"  (smt2s env bs, 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 _ _ e)   = smt2 env e   smt2 _   e                = panic ("smtlib2 Pred  " ++ show e)  -- | smt2Cast uses the 'as x T' pattern needed for polymorphic ADT constructors

@@ -13,6 +13,7 @@         -- * Convert theory symbols      , smt2Symbol+        -- * Preamble to initialize SMT      , preamble @@ -27,7 +28,7 @@         -- * Theories      , setEmpty, setEmp, setCap, setSub, setAdd, setMem-     , setCom, setCup, setDif, setSng, mapSel, mapSto+     , setCom, setCup, setDif, setSng, mapSel, mapCup, mapSto, mapDef        -- * Query Theories      , isSmt2App@@ -49,16 +50,23 @@ import qualified Data.Text import           Data.String                 (IsString(..)) ------------------------------------------------------------------------------ | Set Theory ------------------------------------------------------------------------------------------------------------------------------------- +{- | [NOTE:Adding-Theories] To add new (SMTLIB supported) theories to+     liquid-fixpoint and upstream, grep for "Map_default" and then add+     your corresponding symbol in all those places.+     This is currently far more complicated than it needs to be.+ -}++--------------------------------------------------------------------------------+-- | Theory Symbols ------------------------------------------------------------+--------------------------------------------------------------------------------+ elt, set, map :: Raw elt  = "Elt" set  = "Set" map  = "Map" -emp, add, cup, cap, mem, dif, sub, com, sel, sto :: Raw+emp, add, cup, cap, mem, dif, sub, com, sel, sto, mcup, mdef :: Raw emp   = "smt_set_emp" add   = "smt_set_add" cup   = "smt_set_cup"@@ -69,8 +77,11 @@ com   = "smt_set_com" sel   = "smt_map_sel" sto   = "smt_map_sto"+mcup  = "smt_map_cup"+mdef  = "smt_map_def" -setEmpty, setEmp, setCap, setSub, setAdd, setMem, setCom, setCup, setDif, setSng, mapSel, mapSto :: Symbol++setEmpty, setEmp, setCap, setSub, setAdd, setMem, setCom, setCup, setDif, setSng :: Symbol setEmpty = "Set_empty" setEmp   = "Set_emp" setCap   = "Set_cap"@@ -81,9 +92,12 @@ setCup   = "Set_cup" setDif   = "Set_dif" setSng   = "Set_sng"++mapSel, mapSto, mapCup, mapDef :: Symbol mapSel   = "Map_select" mapSto   = "Map_store"-+mapCup   = "Map_union"+mapDef   = "Map_default"  strLen, strSubstr, strConcat :: (IsString a) => a -- Symbol strLen    = "strLen"@@ -132,6 +146,10 @@         (sel, map, elt, elt)     , format "(define-fun {} ((m {}) (k {}) (v {})) {} (store m k v))"         (sto, map, elt, elt, map)+    , format "(define-fun {} ((m1 {}) (m2 {})) {} ((_ map (+ ({} {}) {})) m1 m2))"+        (mcup, map, map, map, elt, elt, elt)+    , format "(define-fun {} ((v {})) {} ((as const ({})) v))"+        (mdef, elt, map, map)     , format "(define-fun {} ((b Bool)) Int (ite b 1 0))"         (Only (boolToIntName :: T.Text))     , uifDef u (symbolText mulFuncName) ("*"   :: T.Text)@@ -254,10 +272,6 @@  smt2App _ _ _ _    = Nothing --- smt2App env (EVar f) (d:ds)---  | Just s <- {- tracepp ("SYMENVTHEORY: " ++ showpp f) $ -} symEnvTheory f env---  = Just $ build "({} {})" (tsRaw s, d <> mconcat [ " " <> d | d <- ds])- smt2AppArg :: VarAs -> SymEnv -> Expr -> Maybe Builder.Builder smt2AppArg k env (ECst (EVar f) t)   | Just fThy <- symEnvTheory f env@@ -265,10 +279,6 @@             then (k env f (ffuncOut t))             else (build "{}" (Only (tsRaw fThy))) --- // smt2AppArg _ env (EVar f)--- // | Just fThy <- symEnvTheory f env--- //  = Just (build "{}" (Only (tsRaw fThy)))- smt2AppArg _ _ _   = Nothing @@ -308,8 +318,6 @@ --   to avoid duplicate SMT definitions.  `uninterpSEnv` is for uninterpreted --   symbols, and `interpSEnv` is for interpreted symbols. ----------------------------------------------------------------------------------- theorySEnv :: SEnv Sort--- theorySEnv = fromListSEnv . M.toList . fmap tsSort $ theorySymbols  -- | `theorySymbols` contains the list of ALL SMT symbols with interpretations, --   i.e. which are given via `define-fun` (as opposed to `declare-fun`)@@ -333,6 +341,8 @@   , interpSym setCom   com   setCmpSort   , interpSym mapSel   sel   mapSelSort   , interpSym mapSto   sto   mapStoSort+  , interpSym mapCup   mcup  mapCupSort+  , interpSym mapDef   mdef  mapDefSort   , interpSym bvOrName "bvor"   bvBopSort   , interpSym bvAndName "bvand" bvBopSort   , interpSym strLen    strLen    strLenSort@@ -345,62 +355,26 @@     setBopSort = FAbs 0 $ FFunc (setSort $ FVar 0) $ FFunc (setSort $ FVar 0) (setSort $ FVar 0)     setMemSort = FAbs 0 $ FFunc (FVar 0) $ FFunc (setSort $ FVar 0) boolSort     setCmpSort = FAbs 0 $ FFunc (setSort $ FVar 0) $ FFunc (setSort $ FVar 0) boolSort-    mapSelSort = FAbs 0 $ FAbs 1 $ FFunc (mapSort (FVar 0) (FVar 1)) $ FFunc (FVar 0) (FVar 1)+    mapSelSort = FAbs 0 $ FAbs 1 $ FFunc (mapSort (FVar 0) (FVar 1))+                                 $ FFunc (FVar 0) (FVar 1)+    mapCupSort = FAbs 0          $ FFunc (mapSort (FVar 0) intSort)+                                 $ FFunc (mapSort (FVar 0) intSort)+                                         (mapSort (FVar 0) intSort)     mapStoSort = FAbs 0 $ FAbs 1 $ FFunc (mapSort (FVar 0) (FVar 1))                                  $ FFunc (FVar 0)                                  $ FFunc (FVar 1)                                          (mapSort (FVar 0) (FVar 1))+    mapDefSort = FAbs 0 $ FAbs 1 $ FFunc (FVar 1)+                                         (mapSort (FVar 0) (FVar 1))+     bvBopSort  = FFunc bitVecSort $ FFunc bitVecSort bitVecSort   interpSym :: Symbol -> Raw -> Sort -> (Symbol, TheorySymbol) interpSym x n t = (x, Thy x n t Theory) --- SHIFTLAM _uninterpSymbols :: [(Symbol, TheorySymbol)]--- SHIFTLAM _uninterpSymbols = [ (x, uninterpSym x t) | (x, t) <- _uninterpSymbols']--- SHIFTLAM--- SHIFTLAM ----------------------------------------------------------------------------------- SHIFTLAM _uninterpSym :: Symbol -> Sort -> TheorySymbol--- SHIFTLAM ----------------------------------------------------------------------------------- SHIFTLAM _uninterpSym x t =  Thy x (symbolRaw x) t Uninterp--- SHIFTLAM--- SHIFTLAM _uninterpSymbols' :: [(Symbol, Sort)]--- SHIFTLAM _uninterpSymbols' = [] -- [ (toIntName,  mkFFunc 1 [FVar 0, FInt]) ]--  -- SHIFTLAM  [ (setToIntName,    FFunc (setSort intSort)   intSort)-  -- SHIFTLAM  , (bitVecToIntName, FFunc bitVecSort intSort)-  -- SHIFTLAM  , (mapToIntName,    FFunc (mapSort intSort intSort) intSort)-  -- SHIFTLAM  , (realToIntName,   FFunc realSort   intSort)-  -- SHIFTLAM  , (lambdaName   ,   FFunc intSort (FFunc intSort intSort))-  -- SHIFTLAM  ]-  -- SHIFTLAM  ++ concatMap makeApplies [1..maxLamArg]-  -- SHIFTLAM  ++ [(lamArgSymbol i, s) | i <- [1..maxLamArg], s <- sorts]--- SHIFTLAM--- SHIFTLAM  -- THESE ARE DUPLICATED IN DEFUNCTIONALIZATION- maxLamArg :: Int maxLamArg = 7---- SHIFTLAM sorts :: [Sort]--- SHIFTLAM sorts = [intSort]---- NIKI TODO: allow non integer lambda arguments--- sorts = [setSort intSort, bitVecSort intSort, mapSort intSort intSort, boolSort, realSort, intSort]--- makeLamArg :: Sort -> Int  -> Symbol--- makeLamArg _ = intArgName---- SHIFTLAM makeApplies :: Int -> [(Symbol, Sort)]--- SHIFTLAM makeApplies i =-  -- SHIFTLAM [ (intApplyName i,    go i intSort)-  -- SHIFTLAM , (setApplyName i,    go i (setSort intSort))-  -- SHIFTLAM , (bitVecApplyName i, go i bitVecSort)-  -- SHIFTLAM , (mapApplyName i,    go i $ mapSort intSort intSort)-  -- SHIFTLAM , (realApplyName i,   go i realSort)-  -- SHIFTLAM , (boolApplyName i,   go i boolSort)-  -- SHIFTLAM ]-  -- SHIFTLAM where-    -- SHIFTLAM go 0 s = FFunc intSort s-    -- SHIFTLAM go i s = FFunc intSort $ go (i-1) s  axiomLiterals :: [(Symbol, Sort)] -> [Expr] axiomLiterals lts = catMaybes [ lenAxiom l <$> litLen l | (l, t) <- lts, isString t ]

@@ -16,15 +16,19 @@      -- * Parse Qualifiers from File   , parseFInfo++    -- * Simplified Info+  , simplifyFInfo ) where  import           Control.Concurrent import           Data.Binary import           System.Exit                        (ExitCode (..))-import           System.Console.CmdArgs.Verbosity   (whenNormal)+import           System.Console.CmdArgs.Verbosity   (whenNormal, whenLoud) import           Text.PrettyPrint.HughesPJ          (render) import           Control.Monad                      (when) import           Control.Exception                  (catch)+ import           Language.Fixpoint.Solver.Sanitize  (symbolEnv, sanitize) import           Language.Fixpoint.Solver.UniqifyBinds (renameAll) import           Language.Fixpoint.Defunctionalize (defunctionalize)@@ -174,7 +178,9 @@   where     msg           = "fq file after Uniqify & Rename " ++ show i ++ "\n" -solveNative' !cfg !fi0 = do+simplifyFInfo :: (NFData a, Fixpoint a, Show a, Loc a)+               => Config -> FInfo a -> IO (SInfo a)+simplifyFInfo !cfg !fi0 = do   -- writeLoud $ "fq file in: \n" ++ render (toFixpoint cfg fi)   -- rnf fi0 `seq` donePhase Loud "Read Constraints"   -- let qs   = quals fi0@@ -190,17 +196,19 @@   graphStatistics cfg si1   let si2  = {-# SCC "wfcUniqify" #-} wfcUniqify $!! si1   let si3  = {-# SCC "renameAll"  #-} renameAll  $!! si2-  rnf si3 `seq` donePhase Loud "Uniqify & Rename"+  rnf si3 `seq` whenLoud $ donePhase Loud "Uniqify & Rename"   loudDump 1 cfg si3   let si4  = {-# SCC "defunction" #-} defunctionalize cfg $!! si3+  -- putStrLn $ "AXIOMS: " ++ showpp (asserts si4)   loudDump 2 cfg si4-  rnf si4 `seq` donePhase Loud "Defunctionalize"   let si5  = {-# SCC "elaborate"  #-} elaborate "solver" (symbolEnv cfg si4) si4   loudDump 3 cfg si5-  rnf si5 `seq` donePhase Loud "Elaborate"-  si6 <- {-# SCC "Sol.inst"  #-} instantiate cfg $!! si5-  rnf si6 `seq` donePhase Loud "Instantiate"+  instantiate cfg $!! si5++solveNative' !cfg !fi0 = do+  si6 <- simplifyFInfo cfg fi0   res <- {-# SCC "Sol.solve" #-} Sol.solve cfg $!! si6+  -- rnf soln `seq` donePhase Loud "Solve2"   --let stat = resStatus res   saveSolution cfg res   -- when (save cfg) $ saveSolution cfg

@@ -11,6 +11,7 @@ import qualified Data.List                      as L import           Data.Maybe                     (maybeToList, isNothing) import           Data.Monoid                    ((<>))+import           Language.Fixpoint.Types.Config import           Language.Fixpoint.Types.PrettyPrint () import qualified Language.Fixpoint.SortCheck          as So import           Language.Fixpoint.Misc@@ -18,20 +19,26 @@ import qualified Language.Fixpoint.Types.Solutions    as Sol import           Language.Fixpoint.Types.Constraints  hiding (ws, bs) import           Prelude                              hiding (init, lookup)-+import           Language.Fixpoint.Solver.Sanitize  (symbolEnv)+import Language.Fixpoint.SortCheck  -------------------------------------------------------------------------------- -- | Initial Gradual Solution (from Qualifiers and WF constraints) ------------- ---------------------------------------------------------------------------------init :: (F.Fixpoint a) => F.SInfo a -> [(F.KVar, (F.GWInfo, [F.Expr]))]+init :: (F.Fixpoint a) => Config -> F.SInfo a -> [(F.KVar, (F.GWInfo, [F.Expr]))] ---------------------------------------------------------------------------------init si = map (refineG si qs genv) gs `using` parList rdeepseq +init cfg si = map (elab . refineG si qs genv) gs `using` parList rdeepseq    where     qs         = F.quals si     gs         = snd <$> gs0     genv       = instConstants si      gs0        = L.filter (isGWfc . snd) $ M.toList (F.ws si)++    elab (k,(x,es)) = ((k,) . (x,)) $ (elaborate "init" (sEnv (gsym x) (gsort x)) <$> es)+    +    sEnv x s    = isEnv {F.seSort = F.insertSEnv x s (F.seSort isEnv)}+    isEnv       = symbolEnv cfg si   --------------------------------------------------------------------------------

@@ -19,6 +19,7 @@ import           Language.Fixpoint.Types.Config  as FC import qualified Language.Fixpoint.Types.Visitor as Vis import qualified Language.Fixpoint.Misc          as Misc -- (mapFst)+import           Language.Fixpoint.Misc          ((<<=)) import qualified Language.Fixpoint.Smt.Interface as SMT import           Language.Fixpoint.Defunctionalize import           Language.Fixpoint.SortCheck@@ -31,15 +32,14 @@ import qualified Data.Text            as T import qualified Data.HashMap.Strict  as M import qualified Data.List            as L-import           Data.Maybe           (catMaybes, fromMaybe)+import           Data.Maybe           (isNothing, catMaybes, fromMaybe) import           Data.Char            (isUpper)--- import           Data.Foldable        (foldlM)+-- import           Text.Printf (printf)  (~>) :: (Expr, String) -> Expr -> EvalST Expr (_e,_str) ~> e' = do-    modify (\st -> st{evId = evId st + 1})-    -- traceM $ showpp _str ++ " : " ++ showpp _e ++ showpp e'-    return (η e')+    modify (\st -> st {evId = evId st + 1})+    return (wtf e')   --------------------------------------------------------------------------------@@ -54,10 +54,11 @@ instantiate' cfg fi = sInfo cfg fi env <$> withCtx cfg file env act   where     act ctx         = forM cstrs $ \(i, c) ->-                        (i,) . notracepp ("INSTANTIATE i = " ++ show i) <$> instSimpC cfg ctx (bs fi) (ae fi) i c+                        (i,) . notracepp ("INSTANTIATE i = " ++ show i) <$> instSimpC cfg ctx (bs fi) aenv i c     cstrs           = M.toList (cm fi)     file            = srcFile cfg ++ ".evals"     env             = symbolEnv cfg fi+    aenv            = {- tracepp "AXIOM-ENV" -} (ae fi)  sInfo :: Config -> GInfo SimpC a -> SymEnv -> [(SubcId, Expr)] -> SInfo a sInfo cfg fi env ips = strengthenHyp fi' (notracepp "ELAB-INST:  " $ zip is ps'')@@ -115,12 +116,8 @@ -------------------------------------------------------------------------------- -- | Knowledge (SMT Interaction) ----------------------------------------------------------------------------------- AT:@TODO: knSels and knEqs should really just be the same thing. In this way,--- we should also unify knSims and knAms, as well as their analogues in AxiomEnv data Knowledge-  = KN { knSels    :: ![(Expr, Expr)]-       , knEqs     :: ![(Expr, Expr)]-       , knSims    :: ![Rewrite]+  = KN { knSims    :: ![Rewrite]        , knAms     :: ![Equation]        , knContext :: IO SMT.Context        , knPreds   :: !([(Symbol, Sort)] -> Expr -> SMT.Context -> IO Bool)@@ -128,17 +125,7 @@        }  emptyKnowledge :: IO SMT.Context -> Knowledge-emptyKnowledge ctx = KN [] [] [] [] ctx (\_ _ _ -> return False) []--lookupKnowledge :: Knowledge -> Expr -> Maybe Expr-lookupKnowledge γ e-  -- Zero argument axioms like `mempty = N`-  | Just e' <- L.lookup e (knEqs γ)-  = Just e'-  | Just e' <- L.lookup e (knSels γ)-  = Just e'-  | otherwise-  = Nothing+emptyKnowledge ctx = KN [] [] ctx (\_ _ _ -> return False) []  isValid :: Knowledge -> Expr -> IO Bool isValid γ b = knPreds γ (knLams γ) b =<< knContext γ@@ -147,9 +134,7 @@                  -> [(Symbol, SortedReft)]                  -> ([(Expr, Expr)], Knowledge) makeKnowledge cfg ctx aenv es = (simpleEqs,) $ (emptyKnowledge context)-                                     { knSels   = sels-                                     , knEqs    = eqs-                                     , knSims   = aenvSimpl aenv+                                     { knSims   = aenvSimpl aenv                                      , knAms    = aenvEqs aenv                                      , knPreds  = \bs e c -> askSMT c bs e                                      }@@ -165,28 +150,13 @@                               ))       return ctx -    -- This creates the rewrite rule e1 -> e2-    -- when should I apply it?+    -- This creates the rewrite rule e1 -> e2. When should I apply it?     -- 1. when e2 is a data con and can lead to further reductions     -- 2. when size e2 < size e1-    -- @TODO: Can this be generalized?-    -- simpleEqs = []-    simpleEqs = {- tracepp "SIMPLEEQS" $ -} _makeSimplifications (aenvSimpl aenv) =<<-               L.nub (catMaybes [_getDCEquality e1 e2 | PAtom Eq e1 e2 <- atms])+    simpleEqs = {- tracepp "SIMPLEEQS" $ -} makeSimplifications (aenvSimpl aenv) =<<+               L.nub (catMaybes [_getDCEquality senv e1 e2 | PAtom Eq e1 e2 <- atms])     atms = splitPAnd =<< (expr <$> filter isProof es)     isProof (_, RR s _) = showpp s == "Tuple"-    sels = (go . expr) =<< es-    go e = let es   = splitPAnd e-               su   = mkSubst [(x, EVar y)  | PAtom Eq (EVar x) (EVar y) <- es ]-               sels = [(EApp (EVar s) x, e) | PAtom Eq (EApp (EVar s) x) e <- es-                                            , isSelector s ]-           in L.nub (sels ++ subst su sels)--    eqs = [(EVar x, ex) | Equ a _ bd <- filter (null . eqArgs) $ aenvEqs aenv-                        , PAtom Eq (EVar x) ex <- splitPAnd bd-                        , x == a-                        ]-     toSMT bs = defuncAny cfg senv . elaborate "makeKnowledge" (elabEnv bs)     elabEnv  = L.foldl' (\env (x, s) -> insertSymEnv x s env) senv @@ -195,7 +165,7 @@     askSMT :: SMT.Context -> [(Symbol, Sort)] -> Expr -> IO Bool     askSMT ctx bs e       | isTautoPred  e = return True-      | isContraPred e = return False+    -- // Why?  | isContraPred e = return False -- Why the f?       | null (Vis.kvars e) = do           SMT.smtPush ctx           b <- SMT.checkValid' ctx [] PTrue (toSMT bs e)@@ -203,13 +173,9 @@           return b       | otherwise      = return False -    -- TODO: Stringy hacks-    isSelector :: Symbol -> Bool-    isSelector  = L.isPrefixOf "select" . symbolString--_makeSimplifications :: [Rewrite] -> (Symbol, [Expr], Expr) -> [(Expr, Expr)]-_makeSimplifications sis (dc, es, e)- = go =<< sis+makeSimplifications :: [Rewrite] -> (Symbol, [Expr], Expr) -> [(Expr, Expr)]+makeSimplifications sis (dc, es, e)+     = go =<< sis  where    go (SMeasure f dc' xs bd)      | dc == dc', length xs == length es@@ -217,8 +183,8 @@    go _      = [] -_getDCEquality :: Expr -> Expr -> Maybe (Symbol, [Expr], Expr)-_getDCEquality e1 e2+_getDCEquality :: SymEnv -> Expr -> Expr -> Maybe (Symbol, [Expr], Expr)+_getDCEquality senv e1 e2     | Just dc1 <- f1     , Just dc2 <- f2     = if dc1 == dc2@@ -231,19 +197,23 @@     | otherwise     = Nothing   where-    (f1, es1) = Misc.mapFst getDC $ splitEApp e1-    (f2, es2) = Misc.mapFst getDC $ splitEApp e2+    (f1, es1) = Misc.mapFst (getDC senv) (splitEApp e1)+    (f2, es2) = Misc.mapFst (getDC senv) (splitEApp e2) -    -- TODO: Stringy hacks-    getDC (EVar x)-      = if isUpper $ head $ symbolString $ dropModuleNames x-          then Just x-          else Nothing-    getDC _-      = Nothing+-- TODO: Stringy hacks+getDC :: SymEnv -> Expr -> Maybe Symbol+getDC senv (EVar x)+  | isUpperSymbol x && isNothing (symEnvTheory x senv)+  = Just x+getDC _ _+  = Nothing -    dropModuleNames = mungeNames (symbol . last) "."+isUpperSymbol :: Symbol -> Bool+isUpperSymbol = isUpper . headSym . dropModuleNames +dropModuleNames :: Symbol -> Symbol+dropModuleNames = mungeNames (symbol . last) "."+  where     mungeNames _ _ ""  = ""     mungeNames f d s'@(symbolText -> s)       | s' == tupConName = tupConName@@ -260,20 +230,58 @@ -------------------------------------------------------------------------------- -- AT@TODO do this for all reflected functions, not just DataCons --- Insert measure info for every constructor--- that appears in the expression e--- required by PMEquivalence.mconcatChunk--- ADTs does this automatically+{- [NOTE:Datacon-Selectors] The 'assertSelectors' function+   insert measure information for every constructor that appears+   in the expression e.++   In theory, this is not required as the SMT ADT encoding takes+   care of it. However, in practice, some constructors, e.g. from+   GADTs cannot be directly encoded in SMT due to the lack of SMTLIB+   support for GADT. Hence, we still need to hang onto this code.++   See tests/proof/ple2.fq for a concrete example.+ -}+ assertSelectors :: Knowledge -> Expr -> EvalST ()-assertSelectors _ _ = return ()+-- assertSelectors _ _ = return ()+{- TODO: HEREHEREHEREHEREHEREHERE+  1. DOES this kill Unification.hs? (Guard under --no-adt)+  2. Use addEquality instead off _addSMTEquality.+-}+assertSelectors γ e = do+    sims <- aenvSimpl <$> gets _evAEnv+    -- cfg  <- gets evCfg+    -- _    <- foldlM (\_ s -> Vis.mapMExpr (go s) e) (tracepp "assertSelector" e) sims+    forM_ sims $ \s -> Vis.mapMExpr (go s) e+    return ()+  where+    go :: Rewrite -> Expr -> EvalST Expr+    go (SMeasure f dc xs bd) e@(EApp _ _)+      | (EVar dc', es) <- splitEApp e+      , dc == dc'+      , length xs == length es+      = do let e1 = (EApp (EVar f) e)+           let e2 = (subst (mkSubst $ zip xs es) bd)+           addEquality γ e1 e2+           return e+    go _ e+      = return e +-- _addSMTEquality :: Knowledge -> Expr -> Expr -> IO ()+-- _addSMTEquality γ e1 e2 = do+  -- ctx <- knContext γ+  -- SMT.smtAssert ctx (tracepp "addSMTEQ" (PAtom Eq (makeLam γ e1) (makeLam γ e2)))+ -------------------------------------------------------------------------------- -- | Symbolic Evaluation with SMT ---------------------------------------------------------------------------------data EvalEnv = EvalEnv { evId        :: Int-                       , evSequence  :: [(Expr,Expr)]-                       , _evAEnv     :: AxiomEnv-                       }+data EvalEnv = EvalEnv+  { evId        :: !Int+  , evSequence  :: [(Expr,Expr)]+  , _evAEnv     :: !AxiomEnv+  , evEnv       :: !SymEnv+  , _evCfg      :: !Config+  }  type EvalST a = StateT EvalEnv IO a @@ -285,13 +293,14 @@     (fmap join . sequence)     (evalOne <$> L.nub (grepTopApps =<< einit))   where-    (eqs, γ) = makeKnowledge cfg ctx aenv facts-    initEvalSt = EvalEnv 0 [] aenv+    (eqs, γ)   = makeKnowledge cfg ctx aenv facts+    senv       = SMT.ctxSymEnv ctx+    initEvalSt = EvalEnv 0 [] aenv senv cfg     -- This adds all intermediate unfoldings into the assumptions     -- no test needs it     -- TODO: add a flag to enable it     evalOne :: Expr -> IO [(Expr, Expr)]-    evalOne e = do+    evalOne e = {- notracepp ("evalOne e = " ++ showpp e) <$> -} do       (e', st) <- runStateT (eval γ e) initEvalSt       if e' == e then return [] else return ((e, e'):evSequence st) @@ -308,27 +317,24 @@ grepTopApps e@(EApp _ _)    = [e] grepTopApps _               = [] --- AT: I think makeLam is the adjoint of splitEApp?+-- makeLam is the adjoint of splitEApp makeLam :: Knowledge -> Expr -> Expr-makeLam γ e = foldl (flip ELam) e (knLams γ)+makeLam γ e = L.foldl' (flip ELam) e (knLams γ)  eval :: Knowledge -> Expr -> EvalST Expr-eval γ e | Just e' <- lookupKnowledge γ e-  = (e, "Knowledge") ~> e' eval γ (ELam (x,s) e)-  -- SHIFTLAM (assuming this shifting is redundant if DEFUNC has already happened)-  -- = do let x' = lamArgSymbol (1 + length (knLams γ))-       -- e'    <- eval γ{knLams = (x',s):knLams γ} (subst1 e (x, EVar x'))-       -- return $ ELam (x,s) $ subst1 e' (x', EVar x)-   = do e'    <- eval γ{knLams = (x, s) : knLams γ} e        return $ ELam (x, s) e'  eval γ e@(EIte b e1 e2)   = do b' <- eval γ b        evalIte γ e b' e1 e2+eval γ (ECoerc s t e)+  = ECoerc s t <$> eval γ e eval γ e@(EApp _ _)   = evalArgs γ e >>= evalApp γ e+eval γ e@(EVar _)+  = evalApp γ e (e,[]) eval γ (PAtom r e1 e2)   = PAtom r <$> eval γ e1 <*> eval γ e2 eval γ (ENeg e)@@ -368,53 +374,136 @@ evalApp :: Knowledge -> Expr -> (Expr, [Expr]) -> EvalST Expr evalApp γ e (EVar f, [ex])   | (EVar dc, es) <- splitEApp ex-  , Just simp <- L.find (\simp -> (smName simp == f) && (smDC simp == dc))-                        (knSims γ)+  , Just simp <- L.find (\simp -> (smName simp == f) && (smDC simp == dc)) (knSims γ)   , length (smArgs simp) == length es-  = do e'    <- eval γ $ η $ substPopIf (zip (smArgs simp) es) (smBody simp)+  = do e'    <- eval γ $ wtf $ substPopIf (zip (smArgs simp) es) (smBody simp)        (e, "Rewrite -" ++ showpp f) ~> e' evalApp γ _ (EVar f, es)+  -- we should move the lookupKnowledge stuff here into kmAms γ   | Just eq <- L.find ((==f) . eqName) (knAms γ)   , Just bd <- getEqBody eq   , length (eqArgs eq) == length es-  , f `notElem` syms bd -- not recursive-  = eval γ $ η $ substPopIf (zip (eqArgs eq) es) bd+  , f `notElem` syms bd               -- non-recursive equations+  = eval γ . wtf =<< assertSelectors γ <<= substEq PopIf eq es bd+ evalApp γ _e (EVar f, es)   | Just eq <- L.find ((==f) . eqName) (knAms γ)   , Just bd <- getEqBody eq-  , length (eqArgs eq) == length es  --  recursive-  = evalRecApplication γ (eApps (EVar f) es) $-    subst (mkSubst $ zip (eqArgs eq) es) bd+  , length (eqArgs eq) == length es   -- recursive equations+  = evalRecApplication γ (eApps (EVar f) es) =<< substEq Normal eq es bd evalApp _ _ (f, es)   = return $ eApps f es +--------------------------------------------------------------------------------+-- | 'substEq' unfolds or instantiates an equation at a particular list of+--   argument values. We must also substitute the sort-variables that appear+--   as coercions. See tests/proof/ple1.fq+--------------------------------------------------------------------------------+substEq :: SubstOp -> Equation -> [Expr] -> Expr -> EvalST Expr+substEq o eq es bd = substEqVal o eq es <$> substEqCoerce eq es bd++data SubstOp = PopIf | Normal++substEqVal :: SubstOp -> Equation -> [Expr] -> Expr -> Expr+substEqVal o eq es bd = case o of+    PopIf  -> substPopIf     xes  bd+    Normal -> subst (mkSubst xes) bd+  where+    xes    =  zip xs es+    xs     =  eqArgNames eq++substEqCoerce :: Equation -> [Expr] -> Expr -> EvalST Expr+substEqCoerce eq es bd = do+  env      <- seSort <$> gets evEnv+  let ts    = snd    <$> eqArgs eq+  let coSub = mkCoSub env es ts+  return    $ applyCoSub coSub bd++-- | @CoSub@ is a map from (coercion) ty-vars represented as 'FObj s'+--   to the ty-vars that they should be substituted with. Note the+--   domain and range are both Symbol and not the Int used for real ty-vars.++type CoSub = M.HashMap Symbol Symbol++mkCoSub :: SEnv Sort -> [Expr] -> [Sort] -> CoSub+mkCoSub env es xTs = Misc.safeFromList "mkCoSub" xys+  where+    eTs            = sortExpr sp env <$> es+    sp             = panicSpan "mkCoSub"+    xys            = concat (zipWith matchSorts xTs eTs)++matchSorts :: Sort -> Sort -> [(Symbol, Symbol)]+matchSorts = go+  where+    go (FObj x)      (FObj y)      = [(x, y)]+    go (FAbs _ t1)   (FAbs _ t2)   = go t1 t2+    go (FFunc s1 t1) (FFunc s2 t2) = go s1 s2 ++ go t1 t2+    go (FApp s1 t1)  (FApp s2 t2)  = go s1 s2 ++ go t1 t2+    go _             _             = []++applyCoSub :: CoSub -> Expr -> Expr+applyCoSub coSub      = Vis.mapExpr fE+  where+    fE (ECoerc s t e) = ECoerc (txS s) (txS t) e+    fE e              = e+    txS               = Vis.mapSort fS+    fS (FObj a)       = FObj   (txV a)+    fS t              = t+    txV a             = M.lookupDefault a a coSub++--------------------------------------------------------------------------------+getEqBody :: Equation -> Maybe Expr+getEqBody (Equ x xts b _ _)+  | Just (fxs, e) <- getEqBodyPred b+  , (EVar f, es)  <- splitEApp fxs+  , f == x+  , es == (EVar . fst <$> xts)+  = Just e+getEqBody _+  = Nothing++getEqBodyPred :: Expr -> Maybe (Expr, Expr)+getEqBodyPred (PAtom Eq fxs e)+  = Just (fxs, e)+getEqBodyPred (PAnd ((PAtom Eq fxs e):_))+  = Just (fxs, e)+getEqBodyPred _+  = Nothing++eqArgNames :: Equation -> [Symbol]+eqArgNames = map fst . eqArgs+ substPopIf :: [(Symbol, Expr)] -> Expr -> Expr-substPopIf xes e = η $ foldl go e xes+substPopIf xes e = wtf $ L.foldl' go e 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)  evalRecApplication :: Knowledge -> Expr -> Expr -> EvalST Expr-evalRecApplication γ e (EIte b e1 e2)-  = do b' <- eval γ b-       b'' <- liftIO (isValid γ b')-       if b''-          then addApplicationEq γ e e1 >>-               ({-# SCC "assertSelectors-1" #-} assertSelectors γ e1) >>-               eval γ e1 >>=-               ((e, "App") ~>)-          else do b''' <- liftIO (isValid γ (PNot b'))-                  if b'''-                     then addApplicationEq γ e e2 >>-                          ({-# SCC "assertSelectors-1" #-} assertSelectors γ e2) >>-                          eval γ e2 >>=-                          ((e, "App") ~>)-                     else return e+evalRecApplication γ e (EIte b e1 e2) = do+  contra <- {- tracepp ("CONTRA? " ++ showpp e) <$> -} liftIO (isValid γ PFalse)+  if contra+    then return e+    else do b' <- eval γ b+            b1 <- liftIO (isValid γ b')+            if b1+              then addEquality γ e e1 >>+                   ({-# SCC "assertSelectors-1" #-} assertSelectors γ e1) >>+                   eval γ e1 >>=+                   ((e, "App") ~>)+              else do+                   b2 <- liftIO (isValid γ (PNot b'))+                   if b2+                      then addEquality γ e e2 >>+                           ({-# SCC "assertSelectors-2" #-} assertSelectors γ e2) >>+                           eval γ e2 >>=+                           ((e, "App") ~>)+                      else return e evalRecApplication _ _ e   = return e -addApplicationEq :: Knowledge -> Expr -> Expr -> EvalST ()-addApplicationEq γ e1 e2 =+addEquality :: Knowledge -> Expr -> Expr -> EvalST ()+addEquality γ e1 e2 =   modify (\st -> st{evSequence = (makeLam γ e1, makeLam γ e2):evSequence st})  evalIte :: Knowledge -> Expr -> Expr -> Expr -> Expr -> EvalST Expr@@ -438,10 +527,14 @@        e2' <- eval γ e2        return $ EIte b e1' e2' +-------------------------------------------------------------------------------- -- normalization required by ApplicativeMaybe.composition-----------------------------------------------------------η :: Expr -> Expr-η = snd . go+--------------------------------------------------------------------------------+-- RJ: What on earth is this function doing?+wtf :: Expr -> Expr+wtf = id+{-+wtf = snd . go   where     go (EIte b t f)       | isTautoPred t && isFalse f@@ -465,5 +558,6 @@               else (False, EApp e1' e2')     go e = (False, e) +-} instance Expression (Symbol, SortedReft) where   expr (x, RR _ (Reft (v, r))) = subst1 (expr r) (v, EVar x)

@@ -8,7 +8,7 @@ -- | Solve a system of horn-clause constraints --------------------------------- -------------------------------------------------------------------------------- -module Language.Fixpoint.Solver.Solve (solve) where+module Language.Fixpoint.Solver.Solve (solve, solverInfo) where  import           Control.Monad (when, filterM) import           Control.Monad.State.Strict (lift)@@ -16,8 +16,6 @@ import qualified Language.Fixpoint.Misc            as Misc import qualified Language.Fixpoint.Types           as F import qualified Language.Fixpoint.Types.Solutions as Sol-import qualified Language.Fixpoint.Types.Graduals  as G-import qualified Language.Fixpoint.Solver.GradualSolution as GS import           Language.Fixpoint.Types.PrettyPrint import           Language.Fixpoint.Types.Config hiding (stats) import qualified Language.Fixpoint.Solver.Solution  as S@@ -33,22 +31,15 @@ import qualified Data.HashMap.Strict as M import qualified Data.HashSet        as S import qualified Data.List as L-import Control.Concurrent.ParallelIO.Global (parallel) -import qualified Language.Fixpoint.SortCheck       as So-import Language.Fixpoint.Solver.Sanitize (symbolEnv)--- DEBUG--- import           Debug.Trace (trace)- -------------------------------------------------------------------------------- solve :: (NFData a, F.Fixpoint a, Show a, F.Loc a) => Config -> F.SInfo a -> IO (F.Result (Integer, a)) ---------------------------------------------------------------------------------solve cfg fi | gradual cfg- = solveGradual cfg fi  solve cfg fi = do-    donePhase Misc.Loud "Worklist Initialize"-    (res, stat) <- withProgressFI sI $ runSolverM cfg sI act+    whenLoud $ donePhase Misc.Loud "Worklist Initialize"+    vb <- getVerbosity+    (res, stat) <- (if (Quiet == vb || gradual cfg) then id else withProgressFI sI) $ runSolverM cfg sI act     when (solverStats cfg) $ printStats fi wkl stat     -- print (numIter stat)     return res@@ -61,124 +52,10 @@   ---------------------------------------------------------------------------------solveGradual :: (NFData a, F.Fixpoint a, Show a, F.Loc a)-             => Config -> F.SInfo a -> IO (F.Result (Integer, a))----------------------------------------------------------------------------------solveGradual cfg fi = do-  -- graphStatistics cfg $ G.uniquify fi-  let fis = zip [1..] $ partition' Nothing $ G.uniquify fi-  if ginteractive cfg-    then snd . traceShow "FINAL SOLUTION\n"  <$> iSolveGradual cfg fis-    else snd . traceShow "FINAL SOLUTION\n" . mconcat <$> parallel (solveGradualOne cfg <$> fis)---iSolveGradual :: (NFData a, F.Fixpoint a, Show a, F.Loc a) => Config -> [(Int, F.SInfo a)] -> IO (Maybe G.GSol, F.Result (Integer, a))-iSolveGradual cfg fis-  = mconcat <$> parallel (solveGradualOne cfg <$> fis)---solveGradualOne :: (NFData a, F.Fixpoint a, Show a, F.Loc a) => Config -> (Int, F.SInfo a) -> IO (Maybe G.GSol, F.Result (Integer, a))-solveGradualOne cfg (_, fi) = do-  sols   <- makeSolutions cfg fi-  gradualLoop (cfg{gradual = False}) fi sols--gradualLoop :: (NFData a, F.Fixpoint a, Show a, F.Loc a) => Config -> F.SInfo a -> (Maybe [G.GSol]) -> IO (Maybe G.GSol, F.Result (Integer, a))-gradualLoop _ _ Nothing-  = return (Nothing, F.safe)-gradualLoop _ _ (Just [])-  = return (Nothing, F.unsafe)-gradualLoop cfg fi (Just (s:ss))-  = do whenLoud   $ putStrLn ("Solving for " ++ show s)-       whenNormal $ putStr "*"-       v <- getVerbosity-       -- putStr ("Substitution = " ++ show s)-       -- putStr ("BEFORE \n\n"  ++ (show $ F.toFixpoint cfg fi))-       -- putStr ("AFTER \n\n"  ++ (show $ F.toFixpoint cfg $ G.gsubst s fi))-       whenNormal $ setVerbosity Quiet-       r <- solve cfg (G.gsubst s fi)-       setVerbosity v-       whenLoud $ putStrLn ("Solution = " ++ if F.isUnsafe r then "UNSAFE" else "SAFE")-       if F.isUnsafe r-        then gradualLoop cfg fi (Just ss)-        else return (Just s, r)---makeSolutions :: (NFData a, F.Fixpoint a, Show a) => Config -> F.SInfo a -> IO (Maybe [G.GSol])-makeSolutions cfg fi-  = G.makeSolutions cfg fi <$> makeLocalLattice cfg fi (GS.init fi)----makeLocalLattice :: Config -> F.SInfo a-                 -> [(F.KVar, (F.GWInfo, [F.Expr]))]-                 -> IO [(F.KVar, (F.GWInfo, [[F.Expr]]))]-makeLocalLattice cfg fi kes = runSolverM cfg sI (act kes)-  where-    sI  = solverInfo cfg fi-    act = mapM (makeLocalLatticeOne cfg fi)---makeLocalLatticeOne :: Config -> F.SInfo a-            -> (F.KVar, (F.GWInfo, [F.Expr]))-            -> SolveM (F.KVar, (F.GWInfo, [[F.Expr]]))-makeLocalLatticeOne cfg fi (k, (e, es)) = do-   elems0  <- filterM (isLocal e) (map (:[]) es)-   elems   <- sortEquals elems0-   lattice <- makeLattice [] (map (:[]) elems) elems-   return $ ((k,) . (e,)) lattice-  where-    sEnv = symbolEnv cfg fi-    makeLattice acc new elems-      | null new-      = return {- traceShow ("LATTICE FROM ELEMENTS = " ++ showElems elems  ++ showElemss acc) -} acc-      | otherwise-      = do let cands = [e:es | e <- elems, es <- new]-           localCans <- filterM (isLocal e) cands-           newElems  <- filterM (notTrivial (new ++ acc)) localCans-           makeLattice (acc ++ new) newElems elems-    _showElem :: F.Expr -> String-    _showElem e1 = showpp $ F.subst (F.mkSubst [(x, F.EVar $ F.tidySymbol x) | x <- F.syms e1]) e1-    _showElems = unlines . map _showElem-    _showElemss = unlines. map _showElems--    notTrivial [] _     = return True-    notTrivial (x:xs) p = do v <- isValid F.dummySpan (mkPred x) (mkPred p)-                             if v then return False-                                  else notTrivial xs p--    mkPred es = So.elaborate "initBGind.mkPred" sEnv (F.pAnd es)--    isLocal i es = do-      let pp = So.elaborate "filterLocal" sEnv $ F.PExist [(F.gsym i, F.gsort i)] $ F.pAnd (F.gexpr i:es)-      isValid F.dummySpan mempty pp--    root      = mempty-    sortEquals xs = (bfs [0]) <$> makeEdges vs [] vs-      where-       vs        = zip [0..] (root:(head <$> xs))--       bfs []     _  = []-       bfs (i:is) es = (snd $ (vs!!i)) : bfs (is++map snd (filter (\(j,k) ->  (j==i && notElem k is)) es)) es--       makeEdges _   acc []    = return acc-       makeEdges vs acc (x:xs) = do ves  <- concat <$> mapM (makeEdgesOne x) vs-                                    if any (\(i,j) -> elem (j,i) acc) ves-                                      then makeEdges (filter ((/= fst x) . fst) vs) (filter (\(i,j) -> ((i /= fst x) && (j /= fst x))) acc) xs-                                      else makeEdges vs (mergeEdges (ves ++ acc)) xs--    makeEdgesOne (i,_) (j,_) | i == j = return []-    makeEdgesOne (i,x) (j,y) = do-      ij <- isValid F.dummySpan (mkPred [x]) (mkPred [y])-      return (if ij then [(j,i)] else [])--    mergeEdges es = filter (\(i,j) -> (not (any (\k -> ((i,k) `elem` es && (k,j) `elem` es)) (fst <$> es)))) es----------------------------------------------------------------------------------- -- | Progress Bar -------------------------------------------------------------------------------- withProgressFI :: SolverInfo a b -> IO b -> IO b-withProgressFI = withProgress . fromIntegral . cNumScc . siDeps+withProgressFI = withProgress . (+ 1) . fromIntegral . cNumScc . siDeps   --------------------------------------------------------------------------------  printStats :: F.SInfo a ->  W.Worklist a -> Stats -> IO ()

@@ -28,6 +28,7 @@   , sortExpr   , checkSortExpr   , exprSort+  , exprSort_maybe    -- * Unify   , unifyFast@@ -58,7 +59,7 @@  import qualified Data.HashMap.Strict       as M import qualified Data.List                 as L-import           Data.Maybe                (mapMaybe, fromMaybe)+import           Data.Maybe                (mapMaybe, fromMaybe, catMaybes)  import           Language.Fixpoint.Types.PrettyPrint import           Language.Fixpoint.Misc@@ -198,13 +199,14 @@     step (PAll   bs p)    = PAll   bs (go p)     step (PAtom r e1 e2)  = PAtom r (go e1) (go e2)     step e@(EApp {})      = go e-    step (ELam b e)       = ELam b (go e)+    step (ELam b e)       = ELam b       (go e)+    step (ECoerc a t e)   = ECoerc a t   (go e)     step (PGrad k su i e) = PGrad k su i (go e)     step e@(PKVar {})     = e     step e@(ESym {})      = e     step e@(ECon {})      = e     step e@(EVar {})      = e-    -- ELam, ETApp, ETAbs, PAll, PExist+    -- ETApp, ETAbs, PAll, PExist     step e                = error $ "TODO elabApply: " ++ showpp e  --------------------------------------------------------------------------------@@ -357,6 +359,7 @@ checkExpr f (PAll  bs e )  = checkExpr (addEnv f bs) e checkExpr f (PExist bs e)  = checkExpr (addEnv f bs) e checkExpr f (ELam (x,t) e) = FFunc t <$> checkExpr (addEnv f [(x,t)]) e+checkExpr f (ECoerc s t e) = checkExpr f (ECst e s) >> return t  checkExpr _ (ETApp _ _)    = error "SortCheck.checkExpr: TODO: implement ETApp" checkExpr _ (ETAbs _ _)    = error "SortCheck.checkExpr: TODO: implement ETAbs" @@ -379,11 +382,15 @@  elab f (EApp e1@(EApp _ _) e2) = do   (e1', _, e2', s2, s) <- notracepp "ELAB-EAPP" <$> elabEApp f e1 e2-  return (eAppC s e1'          (ECst e2' s2), s)+  let e = eAppC s e1' (ECst e2' s2)+  let θ = unifyExpr (snd f) e+  return (applyExpr θ e, maybe s (`apply` s) θ)  elab f (EApp e1 e2) = do   (e1', s1, e2', s2, s) <- elabEApp f e1 e2-  return (eAppC s (ECst e1' s1) (ECst e2' s2), s)+  let e = eAppC s (ECst e1' s1) (ECst e2' s2)+  let θ = unifyExpr (snd f) e+  return (applyExpr θ e, maybe s (`apply` s) θ)  elab _ e@(ESym _) =   return (e, strSort)@@ -477,6 +484,10 @@   let t' = elaborate "ELam Arg" mempty t   return (ELam (x, t') (ECst e' s), FFunc t s) +elab f (ECoerc s t e) = do+  (e', _) <- elab f e+  return     (ECoerc s t e', t)+ elab _ (ETApp _ _) =   error "SortCheck.elab: TODO: implement ETApp" elab _ (ETAbs _ _) =@@ -629,14 +640,24 @@ -- | Expressions sort  --------------------------------------------------------- -------------------------------------------------------------------------------- exprSort :: String -> Expr -> Sort-exprSort msg = go+exprSort msg e = fromMaybe (panic err) (exprSort_maybe e)   where-    go (ECst _ s) = s-    go (ELam (_, sx) e) = FFunc sx (go e)+    err        = printf "exprSort [%s] on unexpected expression %s" msg (show e)++  -- case exprSort_maybe e of+  --  Nothing -> errorstar ("\nexprSort [" ++ msg ++ "] on unexpected expressions " ++ show e)+  --  Just s  -> s+++exprSort_maybe :: Expr -> Maybe Sort+exprSort_maybe = go+  where+    go (ECst _ s) = Just s+    go (ELam (_, sx) e) = FFunc sx <$> go e     go (EApp e ex)-      | FFunc sx s <- genSort (go e)-      = maybe s (`apply` s) $ unifySorts (go ex) sx-    go e = errorstar ("\nexprSort [" ++ msg ++ "] on unexpected expressions " ++ show e)+      | Just (FFunc sx s) <- genSort <$> go e+      = maybe s (`apply` s) <$> ((`unifySorts` sx) <$> go ex)+    go _ = Nothing  genSort :: Sort -> Sort genSort (FAbs _ t) = genSort t@@ -650,10 +671,9 @@  -- | Helper for checking symbol occurrences checkSym :: Env -> Symbol -> CheckM Sort-checkSym f x-  = case f x of-     Found s -> instantiate s-     Alts xs -> throwError $ errUnboundAlts x xs+checkSym f x = case f x of+  Found s -> instantiate s+  Alts xs -> throwError (errUnboundAlts x xs)  -- | Helper for checking if-then-else expressions checkIte :: Env -> Expr -> Expr -> Expr -> CheckM Sort@@ -754,10 +774,20 @@ checkNumeric :: Env -> Sort -> CheckM () checkNumeric f s@(FObj l)   = do t <- checkSym f l-       unless (t == FNum || t == FFrac) (throwError $ errNonNumeric s)+       unless (t `elem` [FNum, FFrac, intSort, FInt]) (throwError $ errNonNumeric s) checkNumeric _ s   = unless (isNumeric s) (throwError $ errNonNumeric s) +checkEqConstr :: Env -> Maybe Expr -> a -> Symbol -> Sort -> CheckM a+checkEqConstr _ _  θ a (FObj b)+  | a == b+  = return θ+checkEqConstr f e θ a t = do+  case f a of+    Found tA -> do unless (tA == t) (throwError $ errUnify e tA t)+                   return θ+    _        -> throwError $ errUnify e (FObj a) t+ -------------------------------------------------------------------------------- -- | Checking Predicates ------------------------------------------------------- --------------------------------------------------------------------------------@@ -805,7 +835,34 @@  checkRelTy _ e _  t1 t2      = unless (t1 == t2) (throwError $ errRel e t1 t2) ++ --------------------------------------------------------------------------------+-- | Sort Unification on Expressions+--------------------------------------------------------------------------------++unifyExpr :: Env -> Expr -> Maybe TVSubst+unifyExpr f (EApp e1 e2) = Just $ mconcat $ catMaybes [θ1, θ2, θ]+  where+   θ1 = unifyExpr f e1+   θ2 = unifyExpr f e2+   θ  = unifyExprApp f e1 e2+unifyExpr f (ECst e _)+  = unifyExpr f e+unifyExpr _ _+  = Nothing++unifyExprApp :: Env -> Expr -> Expr -> Maybe TVSubst+unifyExprApp f e1 e2 = do+  t1 <- getArg $ exprSort_maybe e1+  t2 <- exprSort_maybe e2+  unify f (Just $ EApp e1 e2) t1 t2+  where+    getArg (Just (FFunc t1 _)) = Just t1+    getArg _                   = Nothing+++-------------------------------------------------------------------------------- -- | Sort Unification -------------------------------------------------------------------------------- unify :: Env -> Maybe Expr -> Sort -> Sort -> Maybe TVSubst@@ -880,12 +937,19 @@ unify1 f e !θ (FFunc !t1 !t2) (FFunc !t1' !t2') = do   unifyMany f e θ [t1, t2] [t1', t2'] +unify1 f e θ (FObj a) !t =+  checkEqConstr f e θ a t++unify1 f e θ !t (FObj a) =+  checkEqConstr f e θ a t+ unify1 _ e θ !t1 !t2   | t1 == t2   = return θ   | otherwise   = throwError $ errUnify e t1 t2 + subst :: Int -> Sort -> Sort -> Sort subst !j !tj !t@(FVar !i)   | i == j                  = tj@@ -944,7 +1008,24 @@     f t@(FVar i) = fromMaybe t (lookupVar i θ)     f t          = t +applyExpr :: Maybe TVSubst -> Expr -> Expr+applyExpr Nothing e  = e+applyExpr (Just θ) e = Vis.mapExpr f e+  where+    f (ECst e s) = ECst e (apply θ s)+    f e          = e+ --------------------------------------------------------------------------------+_applyCoercion :: Symbol -> Sort -> Sort -> Sort+--------------------------------------------------------------------------------+_applyCoercion a t = Vis.mapSort f+  where+    f (FObj b)+      | a == b    = t+    f s           = s+++-------------------------------------------------------------------------------- -- | Deconstruct a function-sort ----------------------------------------------- -------------------------------------------------------------------------------- checkFunSort :: Sort -> CheckM (Sort, Sort, TVSubst)@@ -961,6 +1042,10 @@  newtype TVSubst = Th (M.HashMap Int Sort) deriving (Show) +instance Monoid TVSubst where+  mempty                  = Th mempty+  mappend (Th s1) (Th s2) = Th (mappend s1 s2)+ lookupVar :: Int -> TVSubst -> Maybe Sort lookupVar i (Th m)   = M.lookup i m @@ -979,11 +1064,11 @@  errUnify :: Maybe Expr -> Sort -> Sort -> String errUnify eo t1 t2 = printf "Cannot unify %s with %s %s"-                      (showpp t1) (showpp t2) (unifyExpr eo)+                      (showpp t1) (showpp t2) (errUnifyExpr eo) -unifyExpr :: Maybe Expr -> String-unifyExpr Nothing  = ""-unifyExpr (Just e) = "in expression: " ++ showpp e+errUnifyExpr :: Maybe Expr -> String+errUnifyExpr Nothing  = ""+errUnifyExpr (Just e) = "in expression: " ++ showpp e  errUnifyMany :: [Sort] -> [Sort] -> String errUnifyMany ts ts'  = printf "Cannot unify types with different cardinalities %s and %s"

@@ -56,41 +56,40 @@ defaultMaxPartSize = 700  -data Config-  = Config {-      srcFile     :: FilePath            -- ^ src file (*.hs, *.ts, *.c, or even *.fq or *.bfq)-    , cores       :: Maybe Int           -- ^ number of cores used to solve constraints-    , minPartSize :: Int                 -- ^ Minimum size of a partition-    , maxPartSize :: Int                 -- ^ Maximum size of a partition. Overrides minPartSize-    , solver      :: SMTSolver           -- ^ which SMT solver to use-    , linear      :: Bool                -- ^ not interpret div and mul in SMT-    , stringTheory :: Bool               -- ^ interpretation of string theory by SMT-    , defunction  :: Bool                -- ^ defunctionalize (use 'apply' for all uninterpreted applications)-    , allowHO     :: Bool                -- ^ allow higher order binders in the logic environment-    , allowHOqs   :: Bool                -- ^ allow higher order qualifiers-    , eliminate   :: Eliminate           -- ^ eliminate non-cut KVars-    , elimBound   :: Maybe Int           -- ^ maximum length of KVar chain to eliminate-    , elimStats   :: Bool                -- ^ print eliminate stats-    , solverStats :: Bool                -- ^ print solver stats-    , metadata    :: Bool                -- ^ print meta-data associated with constraints-    , stats       :: Bool                -- ^ compute constraint statistics-    , parts       :: Bool                -- ^ partition FInfo into separate fq files-    , save        :: Bool                -- ^ save FInfo as .bfq and .fq file-    , minimize    :: Bool                -- ^ min .fq by delta debug (unsat with min constraints)-    , minimizeQs  :: Bool                -- ^ min .fq by delta debug (sat with min qualifiers)-    , minimizeKs  :: Bool                -- ^ min .fq by delta debug (sat with min kvars)-    , minimalSol  :: Bool                -- ^ shrink final solution by pruning redundant qualfiers from fixpoint-    , gradual     :: Bool                -- ^ solve "gradual" constraints-    , ginteractive :: Bool                -- ^ interactive gradual solving-    , extensionality   :: Bool           -- ^ allow function extensionality-    , alphaEquivalence :: Bool           -- ^ allow lambda alpha equivalence axioms-    , betaEquivalence  :: Bool           -- ^ allow lambda beta equivalence axioms-    , normalForm       :: Bool           -- ^ allow lambda normal-form equivalence axioms-    , autoKuts         :: Bool           -- ^ ignore given kut variables-    , nonLinCuts       :: Bool           -- ^ Treat non-linear vars as cuts-    , noslice          :: Bool           -- ^ Disable non-concrete KVar slicing-    , rewriteAxioms    :: Bool           -- ^ allow axiom instantiation via rewriting-    } deriving (Eq,Data,Typeable,Show,Generic)+data Config = Config+  { srcFile     :: FilePath            -- ^ src file (*.hs, *.ts, *.c, or even *.fq or *.bfq)+  , cores       :: Maybe Int           -- ^ number of cores used to solve constraints+  , minPartSize :: Int                 -- ^ Minimum size of a partition+  , maxPartSize :: Int                 -- ^ Maximum size of a partition. Overrides minPartSize+  , solver      :: SMTSolver           -- ^ which SMT solver to use+  , linear      :: Bool                -- ^ not interpret div and mul in SMT+  , stringTheory :: Bool               -- ^ interpretation of string theory by SMT+  , defunction  :: Bool                -- ^ defunctionalize (use 'apply' for all uninterpreted applications)+  , allowHO     :: Bool                -- ^ allow higher order binders in the logic environment+  , allowHOqs   :: Bool                -- ^ allow higher order qualifiers+  , eliminate   :: Eliminate           -- ^ eliminate non-cut KVars+  , elimBound   :: Maybe Int           -- ^ maximum length of KVar chain to eliminate+  , elimStats   :: Bool                -- ^ print eliminate stats+  , solverStats :: Bool                -- ^ print solver stats+  , metadata    :: Bool                -- ^ print meta-data associated with constraints+  , stats       :: Bool                -- ^ compute constraint statistics+  , parts       :: Bool                -- ^ partition FInfo into separate fq files+  , save        :: Bool                -- ^ save FInfo as .bfq and .fq file+  , minimize    :: Bool                -- ^ min .fq by delta debug (unsat with min constraints)+  , minimizeQs  :: Bool                -- ^ min .fq by delta debug (sat with min qualifiers)+  , minimizeKs  :: Bool                -- ^ min .fq by delta debug (sat with min kvars)+  , minimalSol  :: Bool                -- ^ shrink final solution by pruning redundant qualfiers from fixpoint+  , gradual     :: Bool                -- ^ solve "gradual" constraints+  , ginteractive :: Bool                -- ^ interactive gradual solving+  , extensionality   :: Bool           -- ^ allow function extensionality+  , alphaEquivalence :: Bool           -- ^ allow lambda alpha equivalence axioms+  , betaEquivalence  :: Bool           -- ^ allow lambda beta equivalence axioms+  , normalForm       :: Bool           -- ^ allow lambda normal-form equivalence axioms+  , autoKuts         :: Bool           -- ^ ignore given kut variables+  , nonLinCuts       :: Bool           -- ^ Treat non-linear vars as cuts+  , noslice          :: Bool           -- ^ Disable non-concrete KVar slicing+  , rewriteAxioms    :: Bool           -- ^ allow axiom instantiation via rewriting+  } deriving (Eq,Data,Typeable,Show,Generic)  instance Default Config where   def = defConfig

@@ -55,7 +55,7 @@   , FixSolution   , GFixSolution, toGFixSol   , Result (..)-  , unsafe, isUnsafe, safe+  , unsafe, isUnsafe, isSafe ,safe    -- * Cut KVars   , Kuts (..)@@ -69,8 +69,8 @@   -- * Axioms   , AxiomEnv (..)   , Equation (..)+  , mkEquation   , Rewrite  (..)-  , getEqBody    -- * Misc  [should be elsewhere but here due to dependencies]   , substVars@@ -142,6 +142,9 @@ isGWfc (GWfC {}) = True isGWfc (WfC  {}) = False +instance HasGradual (WfC a) where+  isGradual = isGWfc+ type SubcId = Integer  data SubC a = SubC@@ -263,6 +266,10 @@ unsafe = mempty {resStatus = Unsafe []} safe   = mempty {resStatus = Safe} +isSafe :: Result a -> Bool+isSafe (Result Safe _ _) = True+isSafe _                 = False+ isUnsafe :: Result a -> Bool isUnsafe r | Unsafe _ <- resStatus r   = True@@ -602,6 +609,9 @@      }   deriving (Eq, Show, Functor, Generic) +instance HasGradual (GInfo c a) where+  isGradual info = any isGradual (M.elems $ ws info)+ instance Monoid HOInfo where   mempty        = HOI False False   mappend i1 i2 = HOI { hoBinds = hoBinds i1 || hoBinds i2@@ -738,10 +748,11 @@ --------------------------------------------------------------------------- -- | Axiom Instantiation Information -------------------------------------- ----------------------------------------------------------------------------data AxiomEnv = AEnv { aenvEqs     :: ![Equation]-                     , aenvSimpl   :: ![Rewrite]-                     , aenvExpand  :: M.HashMap SubcId Bool-                     }+data AxiomEnv = AEnv+  { aenvEqs     :: ![Equation]+  , aenvSimpl   :: ![Rewrite]+  , aenvExpand  :: M.HashMap SubcId Bool+  }   deriving (Eq, Show, Generic)  instance B.Binary AxiomEnv@@ -756,43 +767,64 @@ instance NFData Eliminate  instance Monoid AxiomEnv where-  mempty = AEnv [] [] (M.fromList [])-  mappend a1 a2 = AEnv aenvEqs' aenvSimpl' aenvExpand'-    where aenvEqs'     = mappend (aenvEqs a1) (aenvEqs a2)-          aenvSimpl'   = mappend (aenvSimpl a1) (aenvSimpl a2)-          aenvExpand'  = mappend (aenvExpand a1) (aenvExpand a2)+  mempty           = AEnv [] [] (M.fromList [])+  mappend a1 a2    = AEnv aenvEqs' aenvSimpl' aenvExpand'+    where+      aenvEqs'     = mappend (aenvEqs a1) (aenvEqs a2)+      aenvSimpl'   = mappend (aenvSimpl a1) (aenvSimpl a2)+      aenvExpand'  = mappend (aenvExpand a1) (aenvExpand a2) -data Equation = Equ { eqName :: Symbol-                    , eqArgs :: [Symbol]-                    , eqBody :: Expr-                    }+instance PPrint AxiomEnv where+  pprintTidy _ = text . show++data Equation = Equ+  { eqName :: !Symbol           -- ^ name of reflected function+  , eqArgs :: [(Symbol, Sort)]  -- ^ names of parameters+  , eqBody :: !Expr             -- ^ definition of body+  , eqSort :: !Sort             -- ^ sort of body+  , eqRec  :: !Bool             -- ^ is this a recursive definition+  }   deriving (Eq, Show, Generic) +mkEquation :: Symbol -> [(Symbol, Sort)] -> Expr -> Sort -> Equation+mkEquation f xts e out = Equ f xts e out (f `elem` syms e)++instance Subable Equation where+  syms   a = syms (eqBody a) -- ++ F.syms (axiomEq a)+  subst su = mapEqBody (subst su)+  substf f = mapEqBody (substf f)+  substa f = mapEqBody (substa f)++mapEqBody :: (Expr -> Expr) -> Equation -> Equation+mapEqBody f a = a { eqBody = f (eqBody a) }+ instance PPrint Equation where-  pprintTidy k (Equ f xs e) = "def" <+> pprint f <+> intersperse " " (pprint <$> xs) <+> ":=" <+> pprintTidy k e+  pprintTidy _ = toFix +ppArgs :: (PPrint a) => [a] -> Doc+ppArgs = parens . intersperse ", " . fmap pprint  -- eg  SMeasure (f D [x1..xn] e) -- for f (D x1 .. xn) = e-data Rewrite  = SMeasure  { smName  :: Symbol         -- eg. f-                          , smDC    :: Symbol         -- eg. D-                          , smArgs  :: [Symbol]       -- eg. xs-                          , smBody  :: Expr           -- eg. e[xs]-                          }+data Rewrite  = SMeasure+  { smName  :: Symbol         -- eg. f+  , smDC    :: Symbol         -- eg. D+  , smArgs  :: [Symbol]       -- eg. xs+  , smBody  :: Expr           -- eg. e[xs]+  }   deriving (Eq, Show, Generic)  instance Fixpoint AxiomEnv where   toFix axe = vcat ((toFix <$> aenvEqs axe) ++ (toFix <$> aenvSimpl axe))               $+$ text "expand" <+> toFix (pairdoc <$> M.toList(aenvExpand axe))-    where pairdoc (x,y) = text $ show x ++ " : " ++ show y+    where+      pairdoc (x,y) = text $ show x ++ " : " ++ show y  instance Fixpoint Doc where   toFix = id  instance Fixpoint Equation where-  toFix (Equ f xs e)  = text "define"-                     <+> toFix f <+> hsep (toFix <$> xs) <+> text " = "-                     <+> lparen <> toFix e <> rparen+  toFix (Equ f xs e _ _) = "define" <+> toFix f <+> ppArgs xs <+> text "=" <+> parens (toFix e)  instance Fixpoint Rewrite where   toFix (SMeasure f d xs e)@@ -800,13 +832,7 @@    <+> toFix f    <+> parens (toFix d <+> hsep (toFix <$> xs))    <+> text " = "-   <+> lparen <> toFix e <> rparen+   <+> parens (toFix e) -getEqBody :: Equation -> Maybe Expr-getEqBody (Equ  x xs (PAnd ((PAtom Eq fxs e):_)))-  | (EVar f, es) <- splitEApp fxs-  , f == x-  , es == (EVar <$> xs)-  = Just e-getEqBody _-  = Nothing+instance PPrint Rewrite where+  pprintTidy _ = toFix

@@ -214,8 +214,10 @@ instance Fixpoint T.Text where   toFix = text . T.unpack --- RJ: Use `symbolSafeText` if you want it to machine-readable,---     but `symbolText`     if you want it to be human-readable.+{- | [NOTE: SymbolText]+	Use `symbolSafeText` if you want it to machine-readable,+        but `symbolText`     if you want it to be human-readable.+ -}  instance Fixpoint Symbol where   toFix = toFix . checkedText -- symbolSafeText@@ -603,6 +605,8 @@         , mapConName         , "Map_select"         , "Map_store"+        , "Map_union"+        , "Map_default"         , size32Name         , size64Name         , bitVecName

@@ -160,7 +160,9 @@ class HasGradual a where   isGradual :: a -> Bool   gVars     :: a -> [KVar]+  gVars _ = []    ungrad    :: a -> a+  ungrad x = x   instance HasGradual Expr where   isGradual (PGrad {}) = True@@ -278,6 +280,7 @@           | PAll   ![(Symbol, Sort)] !Expr           | PExist ![(Symbol, Sort)] !Expr           | PGrad  !KVar !Subst !GradInfo !Expr+          | ECoerc !Sort !Sort !Expr             deriving (Eq, Show, Data, Typeable, Generic)  type Pred = Expr@@ -339,7 +342,7 @@     go (PExist _ e)    = go e     go (PKVar _ _)     = 1     go (PGrad _ _ _ e) = go e-+    go (ECoerc _ _ e)  = go e  -- | Parsed refinement of @Symbol@ as @Expr@ --   e.g. in '{v: _ | e }' v is the @Symbol@ and e the @Expr@@@ -426,6 +429,7 @@   toFix (ETApp e s)      = text "tapp" <+> toFix e <+> toFix s   toFix (ETAbs e s)      = text "tabs" <+> toFix e <+> toFix s   toFix (PGrad k _ _ e)  = toFix e <+> text "&&" <+> toFix k -- text "??" -- <+> toFix k <+> toFix su+  toFix (ECoerc a t e)   = text "coerce" <+> toFix a <+> text "~" <+> toFix t <+> text "in" <+> toFix e -- text "??" -- <+> toFix k <+> toFix su   toFix (ELam (x,s) e)   = text "lam" <+> toFix x <+> ":" <+> toFix s <+> "." <+> toFix e    simplify (PAnd [])     = PTrue@@ -594,6 +598,7 @@   pprintPrec _ k (PAll xts p)    = pprintQuant k "forall" xts p   pprintPrec _ k (PExist xts p)  = pprintQuant k "exists" xts p   pprintPrec _ k (ELam (x,t) e)  = "lam" <+> toFix x <+> ":" <+> toFix t <+> text "." <+> pprintTidy k e+  pprintPrec _ k (ECoerc a t e)  = parens $ "coerce" <+> toFix a <+> "~" <+> toFix t <+> text "in" <+> pprintTidy k e   pprintPrec _ _ p@(PKVar {})    = toFix p   pprintPrec _ _ (ETApp e s)     = "ETApp" <+> toFix e <+> toFix s   pprintPrec _ _ (ETAbs e s)     = "ETAbs" <+> toFix e <+> toFix s

@@ -53,7 +53,7 @@   , mkFFunc   , bkFFunc -  , isNumeric, isReal, isString, isPolyInst +  , isNumeric, isReal, isString, isPolyInst    -- * User-defined ADTs   , DataField (..)@@ -81,7 +81,10 @@   data FTycon   = TC LocSymbol TCInfo deriving (Ord, Show, Data, Typeable, Generic)-type TCEmb a  = M.HashMap a FTycon+type TCEmb a  = M.HashMap a Sort -- FTycon++-- instance Show FTycon where+--   show (TC s _) = show (val s)  instance Symbolic FTycon where   symbol (TC s _) = symbol s

@@ -16,10 +16,12 @@    -- * Constructing spans   , dummySpan+  , panicSpan   , locAt   , dummyLoc   , dummyPos   , atLoc+  , toSourcePos    -- * Destructing spans   , sourcePosElts@@ -173,8 +175,11 @@   srcSpan _ = dummySpan  dummySpan :: SrcSpan-dummySpan = SS l l-  where l = initialPos ""+dummySpan = panicSpan ""++panicSpan :: String -> SrcSpan+panicSpan s = SS l l+  where l = initialPos s  -- atLoc :: Located a -> b -> Located b -- atLoc (Loc l l' _) = Loc l l'

@@ -39,10 +39,10 @@  mkSubst :: [(Symbol, Expr)] -> Subst -mkSubst = Su . M.fromList . reverse . filter notTrivial +mkSubst = Su . M.fromList . reverse . filter notTrivial   where     notTrivial (x, EVar y) = x /= y-    notTrivial _           = True  +    notTrivial _           = True  isEmptySubst :: Subst -> Bool isEmptySubst (Su xes) = M.null xes@@ -108,6 +108,7 @@   substa f                 = substf (EVar . f)   substf f (EApp s e)      = EApp (substf f s) (substf f e)   substf f (ELam x e)      = substfLam f x e+  substf f (ECoerc a t e)  = ECoerc a t (substf f e)   substf f (ENeg e)        = ENeg (substf f e)   substf f (EBin op e1 e2) = EBin op (substf f e1) (substf f e2)   substf f (EIte p e1 e2)  = EIte (substf f p) (substf f e1) (substf f e2)@@ -127,6 +128,7 @@    subst su (EApp f e)      = EApp (subst su f) (subst su e)   subst su (ELam x e)      = ELam x (subst (removeSubst su (fst x)) e)+  subst su (ECoerc a t e)  = ECoerc a t (subst su e)   subst su (ENeg e)        = ENeg (subst su e)   subst su (EBin op e1 e2) = EBin op (subst su e1) (subst su e2)   subst su (EIte p e1 e2)  = EIte (subst su p) (subst su e1) (subst su e2)@@ -268,6 +270,7 @@     go (EVar x)           = [x]     go (EApp f e)         = go f ++ go e     go (ELam (x,_) e)     = filter (/= x) (go e)+    go (ECoerc _ _ e)     = go e     go (ENeg e)           = go e     go (EBin _ e1 e2)     = go e1 ++ go e2     go (EIte p e1 e2)     = exprSymbols p ++ go e1 ++ go e2

@@ -172,6 +172,7 @@     step !c !(PAtom r e1 e2) = PAtom r     <$> vE c e1 <*> vE c e2     step !c !(PAll xts p)    = PAll   xts  <$> vE c p     step !c !(ELam (x,t) e)  = ELam (x,t)  <$> vE c e+    step !c !(ECoerc a t e)  = ECoerc a t  <$> vE c e     step !c !(PExist xts p)  = PExist xts  <$> vE c p     step !c !(ETApp e s)     = (`ETApp` s) <$> vE c e     step !c !(ETAbs e s)     = (`ETAbs` s) <$> vE c e@@ -220,6 +221,7 @@     go (ECst e t)      = f =<< ((`ECst` t)  <$>  go e                     )     go (PAll xts p)    = f =<< (PAll   xts  <$>  go p                     )     go (ELam (x,t) e)  = f =<< (ELam (x,t)  <$>  go e                     )+    go (ECoerc a t e)  = f =<< (ECoerc a t  <$>  go e                     )     go (PExist xts p)  = f =<< (PExist xts  <$>  go p                     )     go (ETApp e s)     = f =<< ((`ETApp` s) <$>  go e                     )     go (ETAbs e s)     = f =<< ((`ETAbs` s) <$>  go e                     )

@@ -0,0 +1,37 @@++bind 1 m1 : {v : Map_t Int Int | v = Map_default 0}+bind 2 m2 : {v : Map_t Int Int | v = (Map_store (Map_store m1 10 1) 20 1) } +bind 3 m3 : {v : Map_t Int Int | v = (Map_store (Map_store m1 20 1) 10 1) } +bind 4 m4 : {v : Map_t Int Int | v = (Map_store m1 10 1) } +bind 5 m5 : {v : Map_t Int Int | v = (Map_store m1 20 1) } ++constraint:+  env [ 1 ]+  lhs {v : int | v = Map_select m1 100 }+  rhs {v : int | v = 0 } +  id 1 tag []++constraint:+  env [ 1; 2 ]+  lhs {v : int | v = Map_select m2 100 }+  rhs {v : int | v = 0 } +  id 2 tag []++constraint:+  env [ 1; 2 ]+  lhs {v : int | v = Map_select m2 10 }+  rhs {v : int | v = 1 } +  id 3 tag []++constraint:+  env [ 1; 2; 3 ]+  lhs {v : int | true }+  rhs {v : int | m2 = m3 } +  id 4 tag []++constraint:+  env [ 1; 2; 3; 4; 5 ]+  lhs {v : int | true }+  rhs {v : int | m2 = Map_union m4 m4 } +  id 5 tag []+

@@ -0,0 +1,10 @@+ +bind 0 a : {v: int | true } +bind 1 x : {v: int | true } +bind 2 y : {v: a   | true } ++constraint:  +  env [0; 1; 2]+  lhs {v: int | x = y }+  rhs {v: Int | y = x }+  id 1 tag []

@@ -0,0 +1,13 @@+data Thing 0 = [+  | mkCons { head : int } +]+  +bind 0 a : {v: Thing | true } +bind 1 x : {v: Thing | true } +bind 2 y : {v: a     | true } ++constraint:  +  env [0; 1; 2]+  lhs {v: int | x = y }+  rhs {v: Int | y = x }+  id 1 tag []

@@ -0,0 +1,13 @@++data P 2 = [+   | P {pfst : @(0), psnd : @(1)}+   ]++bind 1 pig : {v : int  | true }+bind 2 dog : {v : bool | true }++constraint:+  env [1;2]+  lhs {v : int | psnd (P pig dog) }+  rhs {v:int | 12 = 4 + 8}+  id 1 tag []

@@ -0,0 +1,12 @@+constant f : (func(1, [(Foo int); int]))++bind 1 pig : {v : (Foo a) | true }++bind 2 dog : {v : int | v = f (coerce (Foo a ~ Foo int) pig) }+++constraint:+  env [1;2]+  lhs {v : int | v = 10 }+  rhs {v : int | v = 5 + 5}+  id 1 tag []

@@ -0,0 +1,11 @@+constant f : (func(1, [(Foo int); int]))++bind 1 pig : {v : (Foo a) | true }++bind 2 dog : {v : int | v = f (coerce (Foo a ~ Foo int) pig) }++constraint:+  env [1;2]+  lhs {v : int | v = 10 }+  rhs {v : int | v = 5 + 5}+  id 1 tag []

@@ -0,0 +1,13 @@+// Config {srcFile = "/Users/rjhala/research/stack/liquidhaskell/tests/pos/lit00.hs", cores = Nothing, minPartSize = 500, maxPartSize = 700, solver = z3, linear = False, stringTheory = False, defunction = False, allowHO = False, allowHOqs = False, eliminate = some, elimBound = Nothing, elimStats = False, solverStats = False, metadata = False, stats = False, parts = False, save = True, minimize = False, minimizeQs = False, minimizeKs = False, minimalSol = False, gradual = False, ginteractive = False, extensionality = False, alphaEquivalence = False, betaEquivalence = False, normalForm = False, autoKuts = False, nonLinCuts = True, noslice = False, rewriteAxioms = True, arithmeticAxioms = False}++constant Zero : (Peano) +constant One  : (Peano) ++distinct Zero : (Peano) +distinct One  : (Peano) +++bind 0 xZero : {v : Peano | v = Zero } +bind 1 xOne  : {v : Peano | v = One  } ++

@@ -0,0 +1,37 @@++bind 1 m1 : {v : Map_t Int Int | v = Map_default 0}+bind 2 m2 : {v : Map_t Int Int | v = (Map_store (Map_store m1 10 1) 20 1) } +bind 3 m3 : {v : Map_t Int Int | v = (Map_store (Map_store m1 20 1) 10 1) } +bind 4 m4 : {v : Map_t Int Int | v = (Map_store m1 10 1) } +bind 5 m5 : {v : Map_t Int Int | v = (Map_store m1 20 1) } ++constraint:+  env [ 1 ]+  lhs {v : int | v = Map_select m1 100 }+  rhs {v : int | v = 0 } +  id 1 tag []++constraint:+  env [ 1; 2 ]+  lhs {v : int | v = Map_select m2 100 }+  rhs {v : int | v = 0 } +  id 2 tag []++constraint:+  env [ 1; 2 ]+  lhs {v : int | v = Map_select m2 10 }+  rhs {v : int | v = 1 } +  id 3 tag []++constraint:+  env [ 1; 2; 3 ]+  lhs {v : int | true }+  rhs {v : int | m2 = m3 } +  id 4 tag []++constraint:+  env [ 1; 2; 3; 4; 5 ]+  lhs {v : int | true }+  rhs {v : int | m2 = Map_union m4 m5 } +  id 5 tag []+

@@ -106,6 +106,10 @@      , testCase "FObj " $         show (doParse' sortP "test" "_foo") @?= "FObj \"_foo\""++    , testCase "Coerce0" $+        show (doParse' predP "test" "v = (coerce (a ~ int) (f x))")+          @?= "PAtom Eq (EVar \"v\") (ECoerc (FObj \"a\") FInt (EApp (EVar \"f\") (EVar \"x\")))"     ]  -- ---------------------------------------------------------------------