module Language.Fixpoint.Solver.Validate
(
validate
, symbolSorts
)
where
import Language.Fixpoint.Config
import Language.Fixpoint.PrettyPrint
import qualified Language.Fixpoint.Misc as Misc
import qualified Language.Fixpoint.Types as F
import qualified Language.Fixpoint.Errors as E
import qualified Data.HashMap.Strict as M
import qualified Data.List as L
import Text.Printf
validate :: Config -> F.FInfo a -> Either E.Error (F.FInfo a)
validate _ = Right . renameVV
symbolSorts :: F.FInfo a -> Either E.Error [(F.Symbol, F.Sort)]
symbolSorts fi = compact . (\z -> lits ++ consts ++ z) =<< bindSorts fi
where
lits = F.lits fi
consts = [(x, t) | (x, F.RR t _) <- F.toListSEnv $ F.gs fi]
compact :: [(F.Symbol, F.Sort)] -> Either E.Error [(F.Symbol, F.Sort)]
compact xts
| null bad = Right [(x, t) | (x, [t]) <- ok ]
| otherwise = Left $ dupBindErrors bad
where
(bad, ok) = L.partition multiSorted . binds $ xts
binds = M.toList . M.map Misc.sortNub . Misc.group
bindSorts :: F.FInfo a -> Either E.Error [(F.Symbol, F.Sort)]
bindSorts fi
| null bad = Right [ (x, t) | (x, [(t, _)]) <- ok ]
| otherwise = Left $ dupBindErrors [ (x, map fst ts) | (x, ts) <- bad]
where
(bad, ok) = L.partition multiSorted . binds $ fi
binds = symBinds . F.bs
multiSorted :: (x, [t]) -> Bool
multiSorted = (1 <) . length . snd
dupBindErrors :: [(F.Symbol, [F.Sort])] -> E.Error
dupBindErrors = foldr1 E.catError . map dbe
where
dbe (x, y) = E.err E.dummySpan $ printf "Multiple sorts for %s : %s \n" (showpp x) (showpp y)
symBinds :: F.BindEnv -> [SymBinds]
symBinds = M.toList
. M.map Misc.groupList
. Misc.group
. binders
type SymBinds = (F.Symbol, [(F.Sort, [F.BindId])])
binders :: F.BindEnv -> [(F.Symbol, (F.Sort, F.BindId))]
binders be = [(x, (F.sr_sort t, i)) | (i, x, t) <- F.bindEnvToList be]
renameVV :: F.FInfo a -> F.FInfo a
renameVV fi = fi {F.bs = be'}
where
vts = map subcVV $ M.elems $ F.cm fi
be' = L.foldl' addVV be vts
be = F.bs fi
addVV :: F.BindEnv -> (F.Symbol, F.SortedReft) -> F.BindEnv
addVV b (x, t) = snd $ F.insertBindEnv x t b
subcVV :: F.SubC a -> (F.Symbol, F.SortedReft)
subcVV c = (x, sr)
where
sr = F.slhs c
x = F.reftBind $ F.sr_reft sr