Commit d66b59c9 authored by Michael Hanus 's avatar Michael Hanus
Browse files

libs and examples updated

parent 40224e7a
......@@ -188,22 +188,22 @@ Ihr Name?
Hallo michael, rueckwaerts lautet Ihr Name: leahcim
Loading program "england"...
q1 x
{x=Gloucester} success
{x=Bath} success
{x=Gloucester} True
{x=Bath} True
q2 x y
{x=Bristol, y=Bath} success
{x=Sherbourne, y=Shaftesbury} success
{x=Dorchester, y=Sherbourne} success
{x=Cirencester, y=Cheltenham} success
{x=Cheltenham, y=Gloucester} success
{x=Bristol, y=Bath} True
{x=Sherbourne, y=Shaftesbury} True
{x=Dorchester, y=Sherbourne} True
{x=Cirencester, y=Cheltenham} True
{x=Cheltenham, y=Gloucester} True
q4l
[Bristol,Taunton,Bath,Bournemouth,Gloucester,Torquay,Penzance,Plymouth,Exeter,Winchester,Dorchester,Cirencester,Truro,Cheltenham,Shaftesbury,Sherbourne]
q5l
[Salisbury,Gloucester,Cirencester,Cheltenham]
q7 x
{x=Somerset} success
{x=Gloucestershire} success
{x=Avon} success
{x=Somerset} True
{x=Gloucestershire} True
{x=Avon} True
q10
6
Loading program "queens"...
......
......@@ -21,7 +21,7 @@
-- The current program can only deal with bars of type 4/4.
import Findall
import Findall(allValues)
------------------------ Data type declarations ----------------------------
......@@ -75,10 +75,10 @@ four_chord_bar :: [(Chord, Int)]
four_chord_bar = [(aChord, 2), (aChord, 2), (aChord, 2), (aChord, 2)]
-- Versions without demand-driven generation of the search space:
--two_chord_bar | [(aChord, 4), (aChord, 4)] =:= bar
--two_chord_bar | [(aChord, 4), (aChord, 4)] == bar
-- = bar
-- where bar free
--four_chord_bar | [(aChord, 2), (aChord, 2), (aChord, 2), (aChord, 2)] =:= bar
--four_chord_bar | [(aChord, 2), (aChord, 2), (aChord, 2), (aChord, 2)] == bar
-- = bar
-- where bar free
......@@ -339,13 +339,11 @@ compute_bar :: [(Note, Int)] -> [([(Chord, Int)],Int)]
compute_bar mbar =
if one_chord_solutions == []
then if two_chord_solutions == []
then bestOf (findall (\x -> checkBarDiss four_chord_bar mbar =:= x))
then bestOf (allValues (checkBarDiss four_chord_bar mbar))
else bestOf two_chord_solutions
else bestOf one_chord_solutions
where one_chord_solutions =
findall (\x -> checkBarDiss one_chord_bar mbar =:= x)
two_chord_solutions =
findall (\x -> checkBarDiss two_chord_bar mbar =:= x)
where one_chord_solutions = allValues (checkBarDiss one_chord_bar mbar)
two_chord_solutions = allValues (checkBarDiss two_chord_bar mbar)
-- Filter list of pairs with a minimal (up to variance 1) snd component:
......
import Findall
import Findall(allSolutions)
-- Geographical database (from John Lloyd's Escher report):
......@@ -15,57 +15,55 @@ data City = Bath | Bournemouth | Bristol | Cheltenham | Cirencester |
Truro | Winchester
neighbours :: County -> County -> Success
neighbours Devon Cornwall = success
neighbours Devon Dorset = success
neighbours Devon Somerset = success
neighbours Avon Somerset = success
neighbours Avon Wiltshire = success
neighbours Avon Gloucestershire = success
neighbours Dorset Wiltshire = success
neighbours Somerset Wiltshire = success
neighbours Gloucestershire Wiltshire = success
neighbours Dorset Somerset = success
neighbours Dorset Hampshire = success
neighbours Hampshire Wiltshire = success
neighbours Hampshire Berkshire = success
neighbours Hampshire Sussex = success
neighbours Hampshire Surrey = success
neighbours Sussex Surrey = success
neighbours Sussex Kent = success
neighbours London Surrey = success
neighbours London Kent = success
neighbours London Essex = success
neighbours London Hertfordshire = success
neighbours London Buckinghamshire = success
neighbours Surrey Buckinghamshire = success
neighbours Surrey Kent = success
neighbours Surrey Berkshire = success
neighbours Oxfordshire Berkshire = success
neighbours Oxfordshire Wiltshire = success
neighbours Oxfordshire Gloucestershire = success
neighbours Oxfordshire Warwickshire = success
neighbours Oxfordshire Northamptonshire = success
neighbours Oxfordshire Buckinghamshire = success
neighbours Berkshire Wiltshire = success
neighbours Berkshire Buckinghamshire = success
neighbours Gloucestershire Worcestershire = success
neighbours Worcestershire Herefordshire = success
neighbours Worcestershire Warwickshire = success
neighbours Bedfordshire Buckinghamshire = success
neighbours Bedfordshire Northamptonshire = success
neighbours Bedfordshire Cambridgeshire = success
neighbours Bedfordshire Hertfordshire = success
neighbours Hertfordshire Essex = success
neighbours Hertfordshire Cambridgeshire = success
neighbours Hertfordshire Buckinghamshire = success
neighbours Buckinghamshire Northamptonshire = success
neighbours :: County -> County -> Bool
neighbours Devon Cornwall = True
neighbours Devon Dorset = True
neighbours Devon Somerset = True
neighbours Avon Somerset = True
neighbours Avon Wiltshire = True
neighbours Avon Gloucestershire = True
neighbours Dorset Wiltshire = True
neighbours Somerset Wiltshire = True
neighbours Gloucestershire Wiltshire = True
neighbours Dorset Somerset = True
neighbours Dorset Hampshire = True
neighbours Hampshire Wiltshire = True
neighbours Hampshire Berkshire = True
neighbours Hampshire Sussex = True
neighbours Hampshire Surrey = True
neighbours Sussex Surrey = True
neighbours Sussex Kent = True
neighbours London Surrey = True
neighbours London Kent = True
neighbours London Essex = True
neighbours London Hertfordshire = True
neighbours London Buckinghamshire = True
neighbours Surrey Buckinghamshire = True
neighbours Surrey Kent = True
neighbours Surrey Berkshire = True
neighbours Oxfordshire Berkshire = True
neighbours Oxfordshire Wiltshire = True
neighbours Oxfordshire Gloucestershire = True
neighbours Oxfordshire Warwickshire = True
neighbours Oxfordshire Northamptonshire = True
neighbours Oxfordshire Buckinghamshire = True
neighbours Berkshire Wiltshire = True
neighbours Berkshire Buckinghamshire = True
neighbours Gloucestershire Worcestershire = True
neighbours Worcestershire Herefordshire = True
neighbours Worcestershire Warwickshire = True
neighbours Bedfordshire Buckinghamshire = True
neighbours Bedfordshire Northamptonshire = True
neighbours Bedfordshire Cambridgeshire = True
neighbours Bedfordshire Hertfordshire = True
neighbours Hertfordshire Essex = True
neighbours Hertfordshire Cambridgeshire = True
neighbours Hertfordshire Buckinghamshire = True
neighbours Buckinghamshire Northamptonshire = True
distance1 :: City -> City -> Int
distance1 Plymouth Exeter = 42
distance1 Exeter Bournemouth = 82
distance1 Bristol Taunton = 43
......@@ -99,82 +97,76 @@ distance1 Exeter Dorchester = 53
distance :: City -> City -> Int
distance city1 city2 | distance1 city1 city2 =:= d = d where d free
distance city1 city2 | distance1 city2 city1 =:= d = d where d free
isin :: City -> County -> Success
isin Bristol Avon = success
isin Taunton Somerset = success
isin Salisbury Wiltshire = success
isin Bath Avon = success
isin Bournemouth Dorset = success
isin Gloucester Gloucestershire = success
isin Torquay Devon = success
isin Penzance Cornwall = success
isin Plymouth Devon = success
isin Exeter Devon = success
isin Winchester Hampshire = success
isin Dorchester Dorset = success
isin Cirencester Gloucestershire = success
isin Truro Cornwall = success
isin Cheltenham Gloucestershire = success
isin Shaftesbury Dorset = success
isin Sherbourne Dorset = success
-- list membership:
member e xs = _ ++ (e:_) =:= xs
distance city1 city2 = distance1 city1 city2 ? distance1 city2 city1
isin :: City -> County -> Bool
isin Bristol Avon = True
isin Taunton Somerset = True
isin Salisbury Wiltshire = True
isin Bath Avon = True
isin Bournemouth Dorset = True
isin Gloucester Gloucestershire = True
isin Torquay Devon = True
isin Penzance Cornwall = True
isin Plymouth Devon = True
isin Exeter Devon = True
isin Winchester Hampshire = True
isin Dorchester Dorset = True
isin Cirencester Gloucestershire = True
isin Truro Cornwall = True
isin Cheltenham Gloucestershire = True
isin Shaftesbury Dorset = True
isin Sherbourne Dorset = True
-- Some queries and their expected results:
q1 x = (distance Bristol x < 40) =:= True
q1 x = solve $ distance Bristol x < 40
-- {x=Gloucester} | {x=Bath}
q2 x y = (distance1 x y < 20) =:= True
-- {y=Bath,X=Bristol} | {y=Shaftesbury,X=Sherbourne} | {y=Sherbourne,X=Dorchester} | {y=Cheltenham,X=Cirencester} | {y=Gloucester,X=Cheltenham}
q2 x y = solve $ distance1 x y < 20
-- {y=Bath,x=Bristol} | {y=Shaftesbury,x=Sherbourne} | {y=Sherbourne,x=Dorchester} | {y=Cheltenham,x=Cirencester} | {y=Gloucester,x=Cheltenham}
q3 x = (neighbours Oxfordshire x ? neighbours x Oxfordshire)
-- {x=Berkshire} | {x=Wiltshire} | {x=Gloucestershire} | {x=Warwickshire} | {x=Northamptonshire} | {x=Buckinghamshire}
q4 x = (isin x y & (y==Wiltshire)=:=False) where y free
q4 x = solve $ let y free in isin x y && y/=Wiltshire
-- {x=Bristol} | {x=Taunton} | {x=Bath} | {x=Bournemouth} | {x=Gloucester} | {x=Torquay} | {x=Penzance} | {x=Plymouth} | {x=Exeter} | {x=Winchester} | {x=Dorchester} | {x=Cirencester} | {x=Truro} | {x=Cheltenham} | {x=Shaftesbury} | {x=Sherbourne}
q4l = findall (\x -> let y free in (isin x y & (y==Wiltshire)=:=False))
q4l = allSolutions (\x -> let y free in isin x y && y /= Wiltshire)
-- [Bristol,Taunton,Bath,Bournemouth,Gloucester,Torquay,Penzance,Plymouth,Exeter,Winchester,Dorchester,Cirencester,Truro,Cheltenham,Shaftesbury,Sherbourne]
q5 x = ((neighbours Oxfordshire y ? neighbours y Oxfordshire)
& isin x y) where y free
q5 x = solve $ (neighbours Oxfordshire y ? neighbours y Oxfordshire)
&& isin x y where y free
-- {x=Salisbury} | {x=Gloucester} | {x=Cirencester} | {x=Cheltenham}
q5l = findall (\x-> let y free in
((neighbours Oxfordshire y ? neighbours y Oxfordshire)
& isin x y))
q5l = allSolutions
(\x -> let y free in
(neighbours Oxfordshire y ? neighbours y Oxfordshire) && isin x y)
-- [Salisbury,Gloucester,Cirencester,Cheltenham]
q6 x = member y [Devon,Cornwall,Somerset,Avon] & isin x y where y free
q6 x = solve $ let y free in y `elem` [Devon,Cornwall,Somerset,Avon] && isin x y
-- {x=Torquay} | {x=Plymouth} | {x=Exeter} | {x=Penzance} | {x=Truro} | {x=Taunton} | {x=Bristol} | {x=Bath}
q7 x = (distance Bristol y < 50)=:=True & isin y x where y free
q7 x = solve $ let y free in distance Bristol y < 50 && isin y x
-- {x=Somerset} | {x=Gloucestershire} | {x=Avon}
-- the further queries require encapsulated search:
-- implementation of Escher's forall-construct:
forall :: (a->Success) -> (a->Success) -> Success
forall domain cond = foldr (&) success (map cond (findall domain))
forall :: (a->Bool) -> (a->Bool) -> Bool
forall domain cond = all cond (allSolutions domain)
q8 = forall (\x->(neighbours Avon x ? neighbours x Avon))
(\x->let y free in isin y x)
-- success | success | success
q8 = forall (\x -> (neighbours Avon x ? neighbours x Avon))
(\x -> isin _ x)
-- True | True | True
q9 = let x free in
isin Bristol x &
forall (\z->(distance Bristol z < 40)=:=True)
(\z->(isin z x))
isin Bristol x &&
forall (\z -> distance Bristol z < 40)
(\z -> isin z x)
-- No solution.
q10 = length (findall (\x->(neighbours Oxfordshire x ? neighbours x Oxfordshire)))
q10 = length
(allSolutions (\x->neighbours Oxfordshire x ? neighbours x Oxfordshire))
-- 6
import Findall
-- natural numbers defined by s-terms (Z=zero, S=successor):
data Nat = Z | S Nat
......@@ -9,7 +7,7 @@ add Z n = n
add (S m) n = S(add m n)
-- subtraction defined by reversing the addition:
sub x y | add y z =:= x = z where z free
sub x y | add y z == x = z where z free
-- less-or-equal predicated on natural numbers:
leq Z _ = True
......@@ -19,5 +17,4 @@ leq (S x) (S y) = leq x y
goal1 = sub (S(S(S(S Z)))) (S(S Z))
goal2 = findall (\x -> leq x (S(S Z)) =:= True)
goal2 | leq x (S(S Z)) = x where x free
import Findall
import SetFunctions
-- Place n queens on a chessboard so that no queen can capture another queen:
-- (this solution is due to Sergio Antoy)
queens x | y=:=permute x & naf (capture x y) = y where y free
queens x | y==permute x && isEmpty (set2 capture x y) = y where y free
permute [] = []
permute (x:xs) | u ++ v =:= permute xs = u ++ [x] ++ v
where u,v free
capture x y = let l1,l2,l3,x1,x2,y1,y2 free in
l1 ++ [(x1,y1)] ++ l2 ++ [(x2,y2)] ++ l3 =:= zip x y &
(x1-y1 == x2-y2 || x1+y1 == x2+y2) =:= True
capture x y
| l1 ++ [(x1,y1)] ++ l2 ++ [(x2,y2)] ++ l3 == zip x y &&
(x1-y1 == x2-y2 || x1+y1 == x2+y2)
= True
where l1,l2,l3,x1,x2,y1,y2 free
-- negation as failure (implemented by encapsulated search):
naf c = (findall (\_->c)) =:= []
queens4 = queens [1,2,3,4]
queens5 = queens [1,2,3,4,5]
-- a simple example for encapsulated search:
import Findall(allSolutions)
append [] ys = ys
append (x:xs) ys = x : append xs ys
-- compute all solutions to equation append [0] l =:= [0,1,2]:
g1 = findall (\l -> append [0] l =:= [0,1,2])
-- compute all solutions to equation append [True] l == [True,False]:
g1 = allSolutions (\l -> append [True] l == [True,False])
-- compute all solutions for l2 to equation append l1 l2 =:= [0,1,2]
-- compute all solutions for l2 to equation append l1 l2 == [True,False]
-- where l1 is arbitrary:
g2 = findall (\l2 -> let l1 free in append l1 l2 =:= [0,1])
g2 = allSolutions (\l2 -> let l1 free in append l1 l2 == [True,False])
-- compute the list of all splittings of the list [0,1]:
g3 = findall (\(l1,l2) -> append l1 l2 =:= [0,1])
-- compute the list of all splittings of the list [True,False]:
g3 = allSolutions (\(l1,l2) -> append l1 l2 == [True,False])
-- Module SportsDB from Escher report
import Findall(allSolutions)
data Person = Mary | Bill | Joe | Fred
data Sport = Cricket | Football | Tennis
likes :: Person -> Sport -> Success
likes Mary Cricket = success
likes Mary Tennis = success
likes Bill Cricket = success
likes Bill Tennis = success
likes Joe Tennis = success
likes Joe Football = success
likes :: Person -> Sport -> Bool
likes Mary Cricket = True
likes Mary Tennis = True
likes Bill Cricket = True
likes Bill Tennis = True
likes Joe Tennis = True
likes Joe Football = True
q1 s = likes Fred s --> no solution
-- Auxiliaries:
-- list membership defined by a conditional rule based on concatenation:
member(e,l) = let l1,l2 free in l1++(e:l2)=:=l
-- implementation of Escher's forall-construct:
forall :: (a->Success) -> (a->Success) -> Success
forall domain cond = foldr (&) success (map cond (findall domain))
forall :: (a->Bool) -> (a->Bool) -> Bool
forall domain cond = all cond (allSolutions domain)
q2 x = forall (\y-> member(y,[Cricket,Tennis]))
q2 x = forall (\y-> y `elem` [Cricket,Tennis])
(\y-> likes x y)
--> {x=Mary} | {x=Bill}
lib-trunk @ b0b63120
Subproject commit c5894ddd42a183aa9d68c0d034e71982b1f93f2a
Subproject commit b0b63120b0d61c9e4df1ea9a2609bfb6822d3a57
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment