Skip to content

Commit

Permalink
Merge pull request #561 from typechecker/hlint/move-brackets-avoid-do…
Browse files Browse the repository at this point in the history
…llar

Follow hlint, move brackets to avoid $.
  • Loading branch information
nikivazou committed Apr 28, 2022
2 parents 83bcb76 + d5f28d8 commit db2c3c7
Show file tree
Hide file tree
Showing 5 changed files with 8 additions and 10 deletions.
2 changes: 0 additions & 2 deletions .hlint.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -4,14 +4,12 @@
- ignore: {name: "Evaluate"} # 1 hint
- ignore: {name: "Fix pragma markup"} # 38 hints
- ignore: {name: "Functor law"} # 3 hints
- ignore: {name: "Move brackets to avoid $"} # 8 hints
- ignore: {name: "Redundant $"} # 20 hints
- ignore: {name: "Redundant <$>"} # 29 hints
- ignore: {name: "Redundant bang pattern"} # 33 hints
- ignore: {name: "Redundant bracket"} # 198 hints
- ignore: {name: "Redundant flip"} # 1 hint
- ignore: {name: "Redundant if"} # 1 hint
- ignore: {name: "Unused LANGUAGE pragma"} # 29 hints
- ignore: {name: "Use $>"} # 7 hints
- ignore: {name: "Use ++"} # 1 hint
- ignore: {name: "Use <$"} # 2 hints
Expand Down
8 changes: 4 additions & 4 deletions src/Language/Fixpoint/Horn/Transformations.hs
Original file line number Diff line number Diff line change
Expand Up @@ -630,18 +630,18 @@ rewriteWithEqualities measures n args equalities = preds
Nothing -> []
Just vertex -> nub $ filter (/= F.EVar x) $ mconcat [es | ((_, es), _, _) <- vf <$> DG.reachable eGraph vertex]

argsAndPrims = args `S.union` (S.fromList $ map fst $ F.toListSEnv $ F.theorySymbols []) `S.union`measures
argsAndPrims = args `S.union` S.fromList (map fst $ F.toListSEnv $ F.theorySymbols []) `S.union`measures

isWellFormed :: F.Expr -> Bool
isWellFormed e = (S.fromList $ F.syms e) `S.isSubsetOf` argsAndPrims
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
where
go e = if isWellFormed e then [e] else rewrite rewrites [e]
where
needSolving = (S.fromList $ F.syms e) `S.difference` argsAndPrims
needSolving = S.fromList (F.syms e) `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]
Expand Down Expand Up @@ -1013,7 +1013,7 @@ hornify (Head (PAnd ps) a) = CAnd (flip Head a <$> ps')
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)))
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
Expand Down
4 changes: 2 additions & 2 deletions src/Language/Fixpoint/Solver/Instantiate.hs
Original file line number Diff line number Diff line change
Expand Up @@ -740,7 +740,7 @@ getDC _ _
= Nothing

isUpperSymbol :: Symbol -> Bool
isUpperSymbol x = (0 < lengthSym x') && (isUpper $ headSym x')
isUpperSymbol x = (0 < lengthSym x') && isUpper (headSym x')
where
x' = dropModuleNames x

Expand Down Expand Up @@ -804,6 +804,6 @@ withCtx cfg file env k = do
(~>) :: (Expr, String) -> Expr -> EvalST Expr
(e, _str) ~> e' = do
let msg = "PLE: " ++ _str ++ showpp (e, e')
modify (\st -> st {evId = (mytracepp msg $ evId st) + 1})
modify (\st -> st {evId = mytracepp msg (evId st) + 1})
return e'

2 changes: 1 addition & 1 deletion src/Language/Fixpoint/Solver/Interpreter.hs
Original file line number Diff line number Diff line change
Expand Up @@ -137,7 +137,7 @@ evalCandsLoop ie ictx0 γ env = go ictx0
rws = [rewrite e rw | rw <- snd <$> M.toList (knSims γ)
, e <- S.toList (snd `S.map` exprs)]
in
exprs <> (S.fromList $ concat rws)
exprs <> S.fromList (concat rws)
go ictx | S.null (icCands ictx) = return ictx
go ictx = do let cands = icCands ictx
let env' = env { evAccum = icEquals ictx <> evAccum env }
Expand Down
2 changes: 1 addition & 1 deletion src/Language/Fixpoint/Solver/Prettify.hs
Original file line number Diff line number Diff line change
Expand Up @@ -188,7 +188,7 @@ shortenVarNames env c =
sortSubst = FObj . (at symMap)
in reft (at m (reftBind r)) $
substSortInExpr sortSubst $
(substf (EVar . (at m)) $ reftPred r)
substf (EVar . (at m)) (reftPred r)

at :: HashMap Symbol Symbol -> Symbol -> Symbol
at m k = fromMaybe k $ HashMap.lookup k m
Expand Down

0 comments on commit db2c3c7

Please sign in to comment.