Merge trial

.gitignore

@@ -10,3 +10,4 @@ cabal-dev
 cabal.sandbox.config
 cabal.config
 .dist-buildwrapper/
+.idea/

src/LG/Base.hs

@@ -3,24 +3,24 @@ module LG.Base where
 type Name = String
 type Identifier = Int
 
-data Occurrence a = Identifier :@ a deriving (Eq)
+data Occurrence a = Identifier :@ a deriving (Eq, Ord)
 
 abstract :: Occurrence a -> a
 abstract (_ :@ x) = x
 
-data Formula = P PositiveFormula | N NegativeFormula deriving (Eq)
+data Formula = P PositiveFormula | N NegativeFormula deriving (Eq, Ord)
 
 data PositiveFormula = AtomP Name
                      | Formula :<×>: Formula
                      | Formula :<\>: Formula
                      | Formula :</>: Formula
-                     deriving (Eq)
+                     deriving (Eq, Ord)
 
 data NegativeFormula = AtomN Name
                      | Formula  :\:  Formula
                      | Formula  :/:  Formula
                      | Formula :<+>: Formula
-                     deriving (Eq)
+                     deriving (Eq, Ord)
 
 instance Show a => Show (Occurrence a) where
   show (k :@ a) = show k ++ " @ " ++ show a

src/LG/Graph.hs

@@ -94,7 +94,7 @@ data NodeInfo = Node { formula     :: Formula
                      , premiseOf   :: Maybe Link
                      , succedentOf :: Maybe Link
                      }
-              deriving (Eq, Show)
+              deriving (Eq, Show, Ord)
 
 
 -- Change the link above or below a node
@@ -147,6 +147,18 @@ cyclic g | Map.null g     = False
 isTree :: CompositionGraph -> Bool
 isTree = not . cyclic
 
+newtype LeafNode = Leaf (Occurrence NodeInfo) deriving (Eq, Ord)
+
+-- Return all leaf nodes for given composition graph
+-- Complexity: O(n)
+leafNodes :: CompositionGraph -> [LeafNode]
+leafNodes g = map Leaf $ map pairToOccurrence (Map.toList (Map.filter isOpenLeafNode g))
+
+isOpenLeafNode (Node _ _ Nothing _) = True
+isOpenLeafNode (Node _ _ _ Nothing) = True
+isOpenLeafNode _ = False
+
+pairToOccurrence (a, b) = a :@ b
 
 --------------------------------------------------------------------------------
 -- Graph manipulation

src/LG/Term.hs

@@ -2,34 +2,34 @@ module LG.Term where
 
 import LG.Base
 
-data Term = V ValueTerm | E ContextTerm | C CommandTerm deriving (Eq)
+data Term = V ValueTerm | E ContextTerm | C CommandTerm deriving (Eq, Ord)
 
-data NodeTerm = Va ValueTerm' | Ev ContextTerm' deriving (Eq)
+data NodeTerm = Va ValueTerm' | Ev ContextTerm' deriving (Eq, Ord)
 
 data ValueTerm'   = Variable Name
                   | ValueTerm   :<×> ValueTerm
                   | ContextTerm :<\> ValueTerm
                   | ValueTerm   :</> ContextTerm
-                  deriving (Eq)
+                  deriving (Eq, Ord)
 
 data ValueTerm    = V' ValueTerm'
                   | Mu Name CommandTerm
-                  deriving (Eq)
+                  deriving (Eq, Ord)
 
 data ContextTerm' = Covariable Name
                   | ValueTerm    :\  ContextTerm
                   | ContextTerm  :/  ValueTerm
                   | ContextTerm :<+> ContextTerm
-                  deriving (Eq)
+                  deriving (Eq, Ord)
 
 data ContextTerm  = E' ContextTerm'
                   | Comu Name CommandTerm
-                  deriving (Eq)
+                  deriving (Eq, Ord)
 
 data CommandTerm  = Cut Name Name Name CommandTerm  -- (first second) / third
                   | ValueTerm' :⌈ Name              -- Command right
                   | Name       :⌉ ContextTerm'      -- Command left
-                  deriving (Eq)
+                  deriving (Eq, Ord)
 
 fromNodeTerm :: NodeTerm -> Term
 fromNodeTerm (Va t) = V (V' t)

src/LG/Unfold.hs

@@ -7,33 +7,61 @@ import LG.Base
 import qualified Lexicon as Lexicon
 import qualified Data.Map as Map
 
--- 'unfold' will maximally unfold every given formula and add all generated formulae to a new composition graph.
--- Operator-specific rules are applied to create a link connecting the formula with its sub-formulae.
--- For every node generated, a twin node is created an connected to the original node through an axioma link. (See M&M, p. 23: Definition 3.2; bullet 1)
--- The process is repeated on these twin nodes until we have created nodes for atomic formulae.
--- See Moortgat & Moot (2012), p. 6-7 for unfolding on proof structures without terms, and p. 24 for their term-annotated counterparts. This function add terms to the nodes.
--- The terms generated by this module are guaranteed to be unique in the composition graph, because they are based on their node identifiers.
-unfold :: [Lexicon.Entry] -> [Lexicon.Entry] -> CompositionGraph
-unfold hypotheses conclusions = graph
+-- 'unfold' creates a maximally unfolded composition graph for every
+-- given formula. This corresponds roughly to subgraphs resulting from
+-- input words. The composition graphs are guaranteed to be
+-- identifier-compatible, and could be merged into one big composition
+-- graph. This merging happens in all possible ways in the module
+-- Identify.hs.
+--
+-- Operator-specific rules are applied to create a link connecting the
+-- formula with its sub-formulae.
+--
+-- For every node generated, a twin node is created an connected to the
+-- original node through an axioma link. (See M&M, p. 23: Definition 3.2;
+-- bullet 1)
+-- The process is repeated on these twin nodes until we have created nodes
+-- for atomic formulae.
+--
+-- See Moortgat & Moot (2012), p. 6-7 for unfolding on proof structures
+-- without terms, and p. 24 for their term-annotated counterparts. This
+-- function add terms to the nodes.
+--
+-- The terms generated by this module are guaranteed to be unique in the
+-- composition graph, because they are based on their node identifiers.
+unfold :: [Lexicon.Entry] -> [Lexicon.Entry] -> [CompositionGraph]
+unfold hypotheses conclusions = map (\(Unfolded _ g) -> g) graphPairs
   where
-    (hypothesisNodes, idCounter1) = unfoldHypotheses  hypotheses  0          []
-    (conclusionNodes, idCounter2) = unfoldConclusions conclusions idCounter1 []
-    graph = insertNodes (hypothesisNodes ++ conclusionNodes) Map.empty
+    (hypothesisGraphs, idCounter1) = unfoldHypotheses  hypotheses  0          []
+    (conclusionGraphs, idCounter2) = unfoldConclusions conclusions idCounter1 []
+    graphPairs = hypothesisGraphs ++ conclusionGraphs
 
 ---------------------
 --- UNFOLD HYPOTHESIS
 ---------------------
 
+data UnfoldedFormula = Unfolded Lexicon.Entry CompositionGraph
+
 -- Wrapper functions
-unfoldHypotheses []     idCounter acc = (acc, idCounter)
-unfoldHypotheses (x:xs) idCounter acc = unfoldHypotheses xs newCount (unfoldedNodes++acc)
-  where (_, unfoldedNodes, newCount) = unfoldHypothesis x idCounter
+unfoldHypotheses :: [Lexicon.Entry] -> Identifier -> [UnfoldedFormula] -> ([UnfoldedFormula], Identifier)
+unfoldHypotheses []     idCounter acc = (reverse acc, idCounter)
+unfoldHypotheses (x:xs) idCounter acc = unfoldHypotheses xs newCounter ((Unfolded x graph):acc)
+  where (graph, newCounter) = unfoldHypothesis x idCounter
+
+unfoldHypothesis :: Lexicon.Entry -> Identifier -> (CompositionGraph, Identifier)
+unfoldHypothesis lexEntry idCounter = ((insertNodes nodes Map.empty), newCount)
+  where (_, nodes, newCount) = unfoldHypothesis' (Lexicon.formula lexEntry) (Lexicon.term lexEntry) Nothing idCounter
 
-unfoldHypothesis lexEntry idCounter = unfoldHypothesis' (Lexicon.formula lexEntry) (Lexicon.term lexEntry) Nothing idCounter
+-- unfoldHypothesis' first creates a copy of the given formula and
+-- connects the original and the copy to each other through an axioma
+-- link. After that, it will see whether it can do an unfolding, based
+-- on whether the formula is complex and so has an operator link
+-- associated with it. (See M&M, p. 24 for a list of the links.)
 
--- unfoldHypothesis' first creates a copy of the given formula and connects the original and the copy to each other through an axioma link. After that, it will see whether it can do an unfolding, based on whether the formula is complex and so has an operator link associated with it. (See M&M, p. 24 for a list of the links.)
+unfoldHypothesis' :: Formula -> NodeTerm -> Maybe Link -> Identifier -> (Identifier, [Occurrence NodeInfo], Identifier)
 unfoldHypothesis' f defaultTerm l idCounter = (firstId, nodes++aNodes++bNodes, bCount)
     where -- Common to all unfoldings: first create an axioma link
+          idCount  = idCounter
           firstId  = idCounter+0
           mainId   = idCounter+1
           newCount = idCounter+2
@@ -136,11 +164,14 @@ getUnfoldInfoH mainFormula@(P (a :<\>: b)) mainId idCount = (mainTerm, operatorL
 ---------------------
 --- UNFOLD CONCLUSION
 ---------------------
-unfoldConclusions []     idCounter acc = (acc, idCounter)
-unfoldConclusions (x:xs) idCounter acc = unfoldConclusions xs newCount (unfoldedNodes++acc)
-  where (_, unfoldedNodes, newCount) = unfoldConclusion x idCounter
+unfoldConclusions :: [Lexicon.Entry] -> Identifier -> [UnfoldedFormula] -> ([UnfoldedFormula], Identifier)
+unfoldConclusions []     idCounter acc = (reverse acc, idCounter)
+unfoldConclusions (x:xs) idCounter acc = unfoldConclusions xs newCounter (Unfolded x graph:acc)
+  where (graph, newCounter) = unfoldConclusion x idCounter
 
-unfoldConclusion lexEntry idCounter = unfoldConclusion' (Lexicon.formula lexEntry) (Lexicon.term lexEntry) Nothing idCounter
+unfoldConclusion :: Lexicon.Entry -> Identifier -> (CompositionGraph, Identifier)
+unfoldConclusion lexEntry idCounter = (insertNodes nodes Map.empty, newCount)
+  where (_, nodes, newCount) = unfoldConclusion' (Lexicon.formula lexEntry) (Lexicon.term lexEntry) Nothing idCounter
 
 unfoldConclusion' f defaultTerm l idCounter = (firstId, nodes++aNodes++bNodes, bCount)
     where -- Common to all unfoldings: first create an axioma link

src/Lexicon.hs

@@ -6,7 +6,7 @@ module Lexicon where
     data Entry = LexEntry {
       term    :: NodeTerm,
       formula :: Formula
-    }
+    } deriving (Show)
 
     -- Returns the lexical entries to which the given strings map. We assume for simplicity that one word maps to at most one lexical entry.
     entries :: [String] -> Maybe [Entry]
@@ -18,24 +18,29 @@ module Lexicon where
 --    entries xs >>= (Lexicon.lookup x:)
 
     -- Some often used formulae
-    npP   = P (AtomP "np")
-    nP    = P (AtomP "n")
-    sP    = P (AtomP "s")
-    sN    = N (AtomN "s")
-    det   = N (npP :/: nP)
-    tv    = N (N (npP :\: sN) :/: npP)
-    sub   = P ((N (npP:/:nP)):<×>: nP)
+    npP        = P (AtomP "np")
+    nP         = P (AtomP "n")
+    sP         = P (AtomP "s")
+    sN         = N (AtomN "s")
+    det        = N (npP :/: nP)         -- np/n
+    simpleVerb = N (npP :\: sN)         -- np\s-
+    tv         = N (simpleVerb :/: npP) -- (np\s-) / np
+    tvs        = N (simpleVerb :/: sN)  -- (np\s-) / s-
+    sub        = P ((N (npP:/:nP)):<×>: nP)
 
     -- Utility functions for creating atomic terms
     va name = Va (Variable name)
     ev name = Ev (Covariable name)
 
     -- Example lexicon
-    lookup "Mary"  = Just $ LexEntry (va "m")     npP
-    lookup "likes" = Just $ LexEntry (va "likes") tv
-    lookup "John"  = Just $ LexEntry (va "j")     npP
-    lookup "the"   = Just $ LexEntry (va "the")   det
-    lookup "horse" = Just $ LexEntry (va "horse") nP
+    lookup "Mary"   = Just $ LexEntry (va "m")     npP
+    lookup "likes"  = Just $ LexEntry (va "likes") tv
+    lookup "thinks" = Just $ LexEntry (va "think") tvs
+    lookup "Sambam" = Just $ LexEntry (va "think") (P ((P (sN :</>: sN)) :<\>: npP))
+    lookup "left"   = Just $ LexEntry (va "left")  simpleVerb
+    lookup "John"   = Just $ LexEntry (va "j")     npP
+    lookup "the"    = Just $ LexEntry (va "the")   det
+    lookup "horse"  = Just $ LexEntry (va "horse") nP
 
     lookup "s"     = Just $ LexEntry (ev "s")     sN
 

src/Main.hs

@@ -24,9 +24,9 @@ main = do
 -- Parsing
 stage0 :: String -> IO ()
 stage0 sentence = do
-  case Lexicon.entries . wordsBy (not . isLetter) $ sentence of
-    Just hypotheses -> stage1 hypotheses conclusion
-    Nothing         -> putStrLn "The expression was not recognised."
+ case Lexicon.entries . wordsBy (not . isLetter) $ sentence of
+    Just hypotheses -> stage1 hypotheses conclusionSentence 
+    Nothing         -> putStrLn "The expression was not recognised."  
 
 
 -- Unfolding
@@ -65,8 +65,8 @@ figure15 = g1
 figure18 = stage0 "sub tv det noun"
 
 
-conclusion :: [Lexicon.Entry]
-conclusion = fromJust $ Lexicon.entries ["s"]
+conclusionSentence :: [Lexicon.Entry]
+conclusionSentence = fromJust $ Lexicon.entries ["s"]
 
 line :: String
 line = "\n------------------\n"