RSolve: A general solver for equations

[ language, library, logic, mit, program, unification ] [ Propose Tags ]

A general solver for type checkers of programming languages and real world puzzles with complex constraints.

Versions [faq] 0.1.0.0, 0.1.0.1, 2.0.0.0 base (==4.*), containers [details] MIT 2018 thautwarm thautwarm twshere@outlook.com Language https://github.com/thautwarm/Rsolver#readme head: git clone https://github.com/thautwarm/Rsolver.git by ice1000 at Tue Dec 25 07:46:00 UTC 2018 NixOS:2.0.0.0 314 total (47 in the last 30 days) 2.0 (votes: 1) [estimated by rule of succession] λ λ λ Docs available Last success reported on 2018-12-25

Modules

[Index] [Quick Jump]

• RSolve

Maintainer's Corner

For package maintainers and hackage trustees

[back to package description]

RSolve

A general solver for type checkers of programming languages and real world puzzles with complex constraints.

Preview

Here are 2 special cases presented in the following sections to show how powerful RSolve is.

The Most Graceful Hindley-Milner Unification

Check RSolve.HM.Core and RSolve.HM.Example.

Uncomment the code in Main.hs could reproduce following program:

check = do
let i = Prim Int
let f = Prim Float
let arrow = Op Arrow i f
-- u means undecided
u1 <- new
u2 <- new
u3 <- new
u4 <- new
-- u1 -> u2 where u1, u2 is not generic
let arrow_var = Op Arrow (Var u1) (Var u2)
-- int -> int
let arrow_inst1 = Op Arrow i i
-- float -> float
let arrow_inst2 = Op Arrow f f
-- a generic function
let arrow_generic = Forall [u3] $Op Arrow (Var u3) (Var u3) let arrow_match = Op Arrow (Var u4) (Var u4) _ <- solve$ Unify arrow arrow_var
_ <- solve $Unify arrow_inst1 arrow_match _ <- solve$ Unify arrow_generic arrow_inst1
_ <- solve $Unify arrow_generic arrow_inst2 _ <- solveNeg mapM require [Var u1, Var u2, arrow_inst1, arrow_inst2, arrow_generic, arrow_match]  output: u1 : Int u2 : Float arrow_inst1 : (Int -> Int) arrow_inst2 : (Float -> Float) arrow_generic : forall a2.(a2 -> a2) arrow_match : (Int -> Int)  N-Option Puzzles This implementation is presented at RSolve.Options, which provides the abstractions to solve all kinds of puzzles described with options. A Hello World program could be found at src/Main.hs which solves a complex problem described with following link: However, the much easier cases taking the same background as above problem (logic constraints described with four options A, B, C, D) could be enjoyale: test2 = do a <- store$ sol [A, B, C]
b <- store $sol [B, C, D] c <- store$ sol [C]
_ <- solve $a eq b _ <- solve$ b neq c
_ <- solveNeg  -- Not condition requires this
_ <- solvePred -- unnecessary
mapM require [a, b, c]

main = do
format ["a", "b", "c"] . nub . L.map fst
\$ runBr test2 emptyLState


output:

λ stack exec RSolve
====
"a" : Sol (fromList [B])
"b" : Sol (fromList [B])
"c" : Sol (fromList [C])