-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathKeller.hs
77 lines (53 loc) · 2.33 KB
/
Keller.hs
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
-- | Keller storage
module Keller where
import FOL
import GSyntax
import Input
import Control.Applicative (Applicative(..))
type NP = (Exp -> Prop) -> Prop
newtype Keller a = Keller [Store a]
data Store a = Core a
| Stored (Store (Exp -> a)) (Store NP)
instance Functor Keller where
fmap f s = pure f <*> s
instance Applicative Keller where
pure x = Keller [pure x]
Keller fs <*> Keller xs = Keller [f <*> x | f <- fs, x <- xs]
instance Functor Store where
fmap f (Core x) = Core (f x)
fmap f (Stored s np) = Stored (fmap (f .) s) np
instance Applicative Store where
pure x = Core x
Core f <*> s = fmap f s
Stored fs np <*> s = Stored (fmap flip fs <*> s) np
choiceKeller :: [Keller a] -> Keller a
choiceKeller xs = Keller $ concat [ys | Keller ys <- xs]
noStorage :: Keller (Exp -> Prop) -> Keller (Exp -> Prop)
noStorage k = Keller (map Core (retrieveKellerPred k))
store :: Keller NP -> Keller NP
store (Keller nps) = Keller [Stored (Core (\z u -> u z)) np | np <- nps]
--
-- * Retrieval
--
retrieveInput :: InputI Keller -> [Input]
retrieveInput (StatementI p) = map Statement (retrieveKellerProp p)
retrieveInput (QuestionI q) = map Question (retrieveQuestion q)
retrieveQuestion :: QuestI Keller -> [Quest]
retrieveQuestion (YNQuestI p) = map YNQuest (retrieveKellerProp p)
retrieveQuestion (WhQuestI q) = map WhQuest (retrieveKellerPred q)
retrieveQuestion (CountQuestI q) = map CountQuest (retrieveKellerPred q)
retrieveKellerProp :: Keller (Prop) -> [Prop]
retrieveKellerProp = retrieveKeller ($)
retrieveKellerPred :: Keller (Exp -> Prop) -> [Exp -> Prop]
retrieveKellerPred = retrieveKeller (\np f -> np . flip f)
retrieveKeller :: (NP -> (Exp -> a) -> a) -> Keller a -> [a]
retrieveKeller f (Keller ss) = map (retrieveStore f) $ concatMap storePermutations ss
retrieveStore :: (NP -> (Exp -> a) -> a) -> Store a -> a
retrieveStore _ (Core x) = x
retrieveStore f (Stored fs nps) = retrieveStore f (pure f <*> nps <*> fs)
storePermutations :: Store a -> [Store a]
storePermutations (Core x) = [Core x]
storePermutations (Stored s np) = [ zs | ys <- storePermutations s, zs <- everywhere np ys ]
everywhere :: Store NP -> Store (Exp -> a) -> [Store a]
everywhere x (Core f) = [Stored (Core f) x]
everywhere x (Stored s np) = Stored (Stored s np) x : [ Stored zs np | zs <- everywhere x (fmap flip s) ]