forked from NeuroCorgi/sop-satisfier
-
Notifications
You must be signed in to change notification settings - Fork 0
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
1 parent
5e85c81
commit c5cc76b
Showing
11 changed files
with
1,269 additions
and
1,011 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,55 @@ | ||
#!/usr/bin/env bash | ||
set -euo pipefail | ||
|
||
# Help message | ||
show_help() { | ||
local script_name | ||
script_name=$(basename "$0") | ||
echo "Fourmolu formatting Script. | ||
Usage: | ||
$script_name diff Format the current git diff. | ||
$script_name full Format all source files. | ||
$script_name check Check the formatting of the source files. | ||
$script_name (-h | --help) | ||
Options: | ||
-h --help Show this screen." | ||
} | ||
|
||
# Main script logic | ||
if [[ "$#" -eq 0 || "$1" == "-h" || "$1" == "--help" ]]; then | ||
show_help | ||
exit 0 | ||
fi | ||
|
||
exclude_files=( | ||
|
||
) | ||
|
||
# Make sure it doesn't matter from where this script is executed | ||
DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )" | ||
cd $DIR | ||
|
||
if [ $1 == "diff" ] ; then | ||
src_files=$(git diff --cached --name-only --diff-filter=ACMR -- '*.hs') | ||
else | ||
src_files=$(find src tests -type f -name "*.hs") | ||
fi | ||
|
||
src_files_str=$(printf "%s\n" "${src_files[@]}" | sed 's| |\\ |g') | ||
exclude_files_str=$(printf "%s\n" "${exclude_files[@]}" | sed 's| |\\ |g') | ||
src_files=$(echo "$src_files_str" | grep -vwE "$exclude_files_str") | ||
|
||
if [ -z "$src_files" ]; then | ||
exit 0; | ||
fi | ||
|
||
if [[ "$1" == "diff" || "$1" == "full" ]] ; then | ||
fourmolu --mode inplace $src_files | ||
elif [[ "$1" == "check" ]] ; then | ||
fourmolu --mode check $src_files | ||
else | ||
echo "Expected a single argument, \"full\", \"diff\", \"check\" or \"--help\"" >&2 | ||
exit 3 | ||
fi |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,2 @@ | ||
indentation: 2 | ||
column-limit: 90 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,133 +1,157 @@ | ||
{-# LANGUAGE ScopedTypeVariables #-} | ||
|
||
module SoPSat.Internal.NewtonsMethod | ||
where | ||
|
||
import Data.Map (Map) | ||
import qualified Data.Map as M | ||
import Data.Maybe (fromJust) | ||
|
||
import SoPSat.Internal.SoP ( | ||
Atom (..), | ||
Product (..), | ||
SoP (..), | ||
Symbol (..), | ||
) | ||
import SoPSat.SoP (atoms) | ||
import SoPSat.Internal.SoP | ||
(Atom(..), Symbol(..), Product(..), SoP(..)) | ||
|
||
|
||
-- | Evaluates SoP given atom bindings | ||
evalSoP :: (Ord f, Ord c, Floating n) | ||
=> SoP f c | ||
-- ^ Expression to evaluate | ||
-> Map (Atom f c) n | ||
-- ^ Bindings from atoms to values | ||
-> n | ||
-- ^ Evaluation result | ||
evalSoP :: | ||
(Ord f, Ord c, Floating n) => | ||
-- | Expression to evaluate | ||
SoP f c -> | ||
-- | Bindings from atoms to values | ||
Map (Atom f c) n -> | ||
-- | Evaluation result | ||
n | ||
evalSoP (S []) _ = 0 | ||
evalSoP (S ps) binds = sum $ map (`evalProduct` binds) ps | ||
|
||
{- | Evaluates product given atom bindings | ||
-- | Evaluates product given atom bindings | ||
-- | ||
-- Used by @evalSoP@ | ||
evalProduct :: (Ord f, Ord c, Floating n) | ||
=> Product f c | ||
-- ^ Product to evalute | ||
-> Map (Atom f c) n | ||
-- ^ Atom bindings | ||
-> n | ||
-- ^ Evaluation results | ||
Used by @evalSoP@ | ||
-} | ||
evalProduct :: | ||
(Ord f, Ord c, Floating n) => | ||
-- | Product to evalute | ||
Product f c -> | ||
-- | Atom bindings | ||
Map (Atom f c) n -> | ||
-- | Evaluation results | ||
n | ||
evalProduct (P ss) binds = product $ map (`evalSymbol` binds) ss | ||
|
||
-- | Evaluates symbol given atom bindings | ||
-- | ||
-- Used by @evalProduct@ | ||
evalSymbol :: (Ord f, Ord c, Floating n) | ||
=> Symbol f c | ||
-- ^ Symbol to evaluate | ||
-> Map (Atom f c) n | ||
-- ^ Atom bindings | ||
-> n | ||
-- ^ Evaluation result | ||
evalSymbol (I i) _ = fromInteger i | ||
{- | Evaluates symbol given atom bindings | ||
Used by @evalProduct@ | ||
-} | ||
evalSymbol :: | ||
(Ord f, Ord c, Floating n) => | ||
-- | Symbol to evaluate | ||
Symbol f c -> | ||
-- | Atom bindings | ||
Map (Atom f c) n -> | ||
-- | Evaluation result | ||
n | ||
evalSymbol (I i) _ = fromInteger i | ||
evalSymbol (A a) binds = f $ M.lookup a binds | ||
where f (Just n) = n | ||
f Nothing = 0 | ||
where | ||
f (Just n) = n | ||
f Nothing = 0 | ||
evalSymbol (E b p) binds = exp (evalProduct p binds * log (evalSoP b binds)) | ||
|
||
-- | Analitically computes derivative of an expression | ||
-- with respect to an atom | ||
-- | ||
-- Returns function similar to @evalSoP@ | ||
derivative :: (Ord f, Ord c, Floating n) | ||
=> SoP f c | ||
-- ^ Expression to take a derivative of | ||
-> Atom f c | ||
-- ^ Atom to take a derivetive with respect to | ||
-> (Map (Atom f c) n -> n) | ||
-- ^ Function from bindings, representing point, | ||
-- to value of the derivative at that point | ||
{- | Analitically computes derivative of an expression | ||
with respect to an atom | ||
Returns function similar to @evalSoP@ | ||
-} | ||
derivative :: | ||
(Ord f, Ord c, Floating n) => | ||
-- | Expression to take a derivative of | ||
SoP f c -> | ||
-- | Atom to take a derivetive with respect to | ||
Atom f c -> | ||
-- | Function from bindings, representing point, | ||
-- to value of the derivative at that point | ||
(Map (Atom f c) n -> n) | ||
derivative sop symb = \binds -> sum $ d <*> [binds] | ||
where d = map (`derivativeProduct` symb) $ unS sop | ||
|
||
-- | Analitically computes derivative of a product | ||
-- with respect to an atom | ||
-- | ||
-- Used by @derivative@ | ||
derivativeProduct :: (Ord f, Ord c, Floating n) | ||
=> Product f c | ||
-- ^ Product to take a derivative of | ||
-> Atom f c | ||
-- ^ Atom to take a derivative with respect to | ||
-> (Map (Atom f c) n -> n) | ||
-- ^ Function from bindings to a value | ||
derivativeProduct (P []) _ = const 0 | ||
derivativeProduct (P (s:ss)) symb = \binds -> derivativeSymbol s symb binds * evalProduct ps binds + evalSymbol s binds * derivativeProduct ps symb binds | ||
where ps = P ss | ||
|
||
-- | Analitically computes derivative of a symbol | ||
-- with respect to an atom | ||
-- | ||
-- Used by @derivativeProduct@ | ||
derivativeSymbol :: (Ord f, Ord c, Floating n) | ||
=> Symbol f c | ||
-- ^ Symbol to take a derivate of | ||
-> Atom f c | ||
-- ^ Atom to take a derivate with respect to | ||
-> (Map (Atom f c) n -> n) | ||
-- ^ Function from bindings to a value | ||
where | ||
d = map (`derivativeProduct` symb) $ unS sop | ||
|
||
{- | Analitically computes derivative of a product | ||
with respect to an atom | ||
Used by @derivative@ | ||
-} | ||
derivativeProduct :: | ||
(Ord f, Ord c, Floating n) => | ||
-- | Product to take a derivative of | ||
Product f c -> | ||
-- | Atom to take a derivative with respect to | ||
Atom f c -> | ||
-- | Function from bindings to a value | ||
(Map (Atom f c) n -> n) | ||
derivativeProduct (P []) _ = const 0 | ||
derivativeProduct (P (s : ss)) symb = \binds -> | ||
derivativeSymbol s symb binds * evalProduct ps binds | ||
+ evalSymbol s binds * derivativeProduct ps symb binds | ||
where | ||
ps = P ss | ||
|
||
{- | Analitically computes derivative of a symbol | ||
with respect to an atom | ||
Used by @derivativeProduct@ | ||
-} | ||
derivativeSymbol :: | ||
(Ord f, Ord c, Floating n) => | ||
-- | Symbol to take a derivate of | ||
Symbol f c -> | ||
-- | Atom to take a derivate with respect to | ||
Atom f c -> | ||
-- | Function from bindings to a value | ||
(Map (Atom f c) n -> n) | ||
derivativeSymbol (I _) _ = const 0 | ||
derivativeSymbol (A a) atom | ||
| a == atom = const 1 | ||
| otherwise = const 0 | ||
derivativeSymbol e@(E b p) atom = \binds -> | ||
expExpr binds * | ||
(derivative b atom binds * evalProduct p binds | ||
/ evalSoP b binds | ||
+ logExpr binds | ||
* derivativeProduct p atom binds) | ||
where expExpr = evalSymbol e | ||
logExpr = log. evalSoP b | ||
expExpr binds | ||
* ( derivative b atom binds | ||
* evalProduct p binds | ||
/ evalSoP b binds | ||
+ logExpr binds | ||
* derivativeProduct p atom binds | ||
) | ||
where | ||
expExpr = evalSymbol e | ||
logExpr = log . evalSoP b | ||
|
||
-- | Finds if an expression can be equal to zero | ||
newtonMethod :: forall f c n | ||
. (Ord f, Ord c, Ord n, Floating n) | ||
=> SoP f c | ||
-- ^ Expression to check | ||
-> Either (Map (Atom f c) n) (Map (Atom f c) n) | ||
-- ^ @Right binds@ - Atom bindings when expression is equal to zero | ||
-- @Left binds@ - Last checked bindings | ||
newtonMethod :: | ||
forall f c n. | ||
(Ord f, Ord c, Ord n, Floating n) => | ||
-- | Expression to check | ||
SoP f c -> | ||
-- | @Right binds@ - Atom bindings when expression is equal to zero | ||
-- @Left binds@ - Last checked bindings | ||
Either (Map (Atom f c) n) (Map (Atom f c) n) | ||
newtonMethod sop = go init_guess steps | ||
where | ||
consts = atoms sop | ||
derivs = M.fromSet (derivative sop) consts | ||
init_guess = M.fromSet (const 10) consts | ||
steps = 40 | ||
|
||
go :: Map (Atom f c) n -> Word -> Either (Map (Atom f c) n) (Map (Atom f c) n) | ||
go guess 0 = Left guess | ||
go guess n | ||
| val <= 0.1 = Right guess | ||
| otherwise = | ||
where | ||
consts = atoms sop | ||
derivs = M.fromSet (derivative sop) consts | ||
init_guess = M.fromSet (const 10) consts | ||
steps = 40 | ||
|
||
go :: Map (Atom f c) n -> Word -> Either (Map (Atom f c) n) (Map (Atom f c) n) | ||
go guess 0 = Left guess | ||
go guess n | ||
| val <= 0.1 = Right guess | ||
| otherwise = | ||
let | ||
new_guess = foldl (\binds (c,x) -> M.insert c (x - val / dsdc c) binds) guess $ M.toList guess | ||
in go new_guess (n - 1) | ||
where | ||
val = evalSoP sop guess | ||
dsdc c = fromJust (M.lookup c derivs) guess | ||
new_guess = foldl (\binds (c, x) -> M.insert c (x - val / dsdc c) binds) guess $ M.toList guess | ||
in | ||
go new_guess (n - 1) | ||
where | ||
val = evalSoP sop guess | ||
dsdc c = fromJust (M.lookup c derivs) guess |
Oops, something went wrong.