two versions of semantics (the Logic version incomplete)

9 files changed, 416 insertions, 14 deletions

diff --git a/examples/tutorial/semantics/Answer.hs b/examples/tutorial/semantics/Answer.hs
new file mode 100644
index 000000000..b874b8bd2
--- /dev/null
+++ b/examples/tutorial/semantics/Answer.hs
@@ -0,0 +1,20 @@
+module Main where
+
+import GSyntax
+import AnswerBase
+import GF.GFCC.API
+
+main :: IO ()
+main = do
+  gr <- file2grammar "base.gfcc"
+  loop gr
+
+loop :: MultiGrammar -> IO ()
+loop gr = do
+  s <- getLine
+  let t:_ = parse gr "BaseEng" "S" s
+  putStrLn $ showTree t
+  let p = iS $ fg t
+  putStrLn $ show p
+  loop gr
+
diff --git a/examples/tutorial/semantics/AnswerBase.hs b/examples/tutorial/semantics/AnswerBase.hs
new file mode 100644
index 000000000..dbad37e5e
--- /dev/null
+++ b/examples/tutorial/semantics/AnswerBase.hs
@@ -0,0 +1,44 @@
+module AnswerBase where
+
+import GSyntax
+
+-- interpretation of Base
+
+type Prop = Bool
+type Exp = Int
+domain = [0 .. 100]
+
+iS :: GS -> Prop
+iS s = case s of
+  GPredAP np ap -> iNP np (iAP ap)
+  GConjS c s t  -> iConj c (iS s) (iS t)
+
+iNP :: GNP -> (Exp -> Prop) -> Prop
+iNP np p = case np of
+  GEvery cn -> all (\x -> not (iCN cn x) || p x) domain
+  GSome  cn -> any (\x ->      iCN cn x  && p x) domain
+  GConjNP c np1 np2 -> iConj c (iNP np1 p) (iNP np2 p)
+  GUseInt (GInt i) -> p (fromInteger i)
+
+iAP :: GAP -> Exp -> Prop
+iAP ap e = case ap of
+  GComplA2 a2 np    -> iNP np (iA2 a2 e)
+  GConjAP c ap1 ap2 -> iConj c (iAP ap1 e) (iAP ap2 e)
+  GEven -> even e
+  GOdd -> not (even e)
+
+iCN :: GCN -> Exp -> Prop
+iCN cn e = case cn of
+  GModCN ap cn0 -> (iCN cn0 e) && (iAP ap e)
+  GNumber -> True
+
+iConj :: GConj -> Prop -> Prop -> Prop
+iConj c = case c of
+  GAnd -> (&&)
+  GOr  -> (||)
+
+iA2 :: GA2 -> Exp -> Exp -> Prop
+iA2 a2 e1 e2 = case a2 of
+  GGreater -> e1 > e1
+  GSmaller -> e1 < e2 
+  GEqual   -> e1 == e2
diff --git a/examples/tutorial/semantics/Base.gf b/examples/tutorial/semantics/Base.gf
new file mode 100644
index 000000000..b99587e96
--- /dev/null
+++ b/examples/tutorial/semantics/Base.gf
@@ -0,0 +1,37 @@
+-- abstract syntax of a query language
+
+abstract Base = {
+
+cat
+  S ; 
+  NP ; 
+  CN ; 
+  AP ; 
+  A2 ; 
+  Conj ;
+fun 
+  PredAP  : NP -> AP -> S ;
+
+  ComplA2 : A2 -> NP -> AP ;
+
+  ModCN   : AP -> CN -> CN ;
+
+  ConjS   : Conj -> S -> S -> S ;
+  ConjAP  : Conj -> AP -> AP -> AP ;
+  ConjNP  : Conj -> NP -> NP -> NP ;
+
+  Every   : CN -> NP ;
+  Some    : CN -> NP ;
+
+  And, Or : Conj ;  
+
+-- lexicon
+
+  UseInt  : Int -> NP ;
+
+  Number : CN ;
+  Even, Odd, Prime : AP ;
+  Equal, Greater, Smaller, Divisible  : A2 ;
+
+}
+
diff --git a/examples/tutorial/semantics/BaseEng.gf b/examples/tutorial/semantics/BaseEng.gf
new file mode 100644
index 000000000..71b2b91dc
--- /dev/null
+++ b/examples/tutorial/semantics/BaseEng.gf
@@ -0,0 +1,38 @@
+--# -path=.:prelude
+
+concrete BaseEng of Base = open Prelude in {
+
+flags lexer=literals ; unlexer=text ;
+
+-- English concrete syntax; greatly simplified - just for demo purposes
+
+lin 
+  PredAP  = infixSS "is" ;
+
+  ComplA2 = cc2 ;
+
+  ModCN   = cc2 ;
+
+  ConjS  c = infixSS c.s ;
+  ConjAP c = infixSS c.s ;
+  ConjNP c = infixSS c.s ;
+
+  Every = prefixSS "every" ;
+  Some  = prefixSS "some" ;
+
+  And = ss "and" ;
+  Or  = ss "or" ;
+
+  UseInt n = n ;
+
+  Number = ss "number" ;
+
+  Even   = ss "even" ;
+  Odd    = ss "odd" ;
+  Prime  = ss "prime" ;
+  Equal  = ss ("equal" ++ "to") ;
+  Greater = ss ("greater" ++ "than") ;
+  Smaller = ss ("smaller" ++ "than") ;
+  Divisible = ss ("divisible" ++ "by") ;
+ 
+}
diff --git a/examples/tutorial/semantics/Core.gf b/examples/tutorial/semantics/Core.gf
new file mode 100644
index 000000000..975cf827f
--- /dev/null
+++ b/examples/tutorial/semantics/Core.gf
@@ -0,0 +1,6 @@
+abstract Core = {
+
+  cat
+    
+
+}
diff --git a/examples/tutorial/semantics/GSyntax.hs b/examples/tutorial/semantics/GSyntax.hs
new file mode 100644
index 000000000..c16a0b97c
--- /dev/null
+++ b/examples/tutorial/semantics/GSyntax.hs
@@ -0,0 +1,168 @@
+module GSyntax where
+
+import GF.GFCC.DataGFCC
+import GF.GFCC.AbsGFCC
+----------------------------------------------------
+-- automatic translation from GF to Haskell
+----------------------------------------------------
+
+class Gf a where gf :: a -> Exp
+class Fg a where fg :: Exp -> a
+
+newtype GString = GString String  deriving Show
+
+instance Gf GString where
+  gf (GString s) = DTr [] (AS s) []
+
+instance Fg GString where
+  fg t =
+    case t of
+      DTr [] (AS s) []  -> GString s
+      _ -> error ("no GString " ++ show t)
+
+newtype GInt = GInt Integer  deriving Show
+
+instance Gf GInt where
+  gf (GInt s) = DTr [] (AI s) []
+
+instance Fg GInt where
+  fg t =
+    case t of
+      DTr [] (AI s) []  -> GInt s
+      _ -> error ("no GInt " ++ show t)
+
+newtype GFloat = GFloat Double  deriving Show
+
+instance Gf GFloat where
+  gf (GFloat s) = DTr [] (AF s) []
+
+instance Fg GFloat where
+  fg t =
+    case t of
+      DTr [] (AF s) []  -> GFloat s
+      _ -> error ("no GFloat " ++ show t)
+
+----------------------------------------------------
+-- below this line machine-generated
+----------------------------------------------------
+
+data GA2 =
+   GDivisible 
+ | GEqual 
+ | GGreater 
+ | GSmaller 
+  deriving Show
+
+data GAP =
+   GComplA2 GA2 GNP 
+ | GConjAP GConj GAP GAP 
+ | GEven 
+ | GOdd 
+ | GPrime 
+  deriving Show
+
+data GCN =
+   GModCN GAP GCN 
+ | GNumber 
+  deriving Show
+
+data GConj =
+   GAnd 
+ | GOr 
+  deriving Show
+
+data GNP =
+   GConjNP GConj GNP GNP 
+ | GEvery GCN 
+ | GSome GCN 
+ | GUseInt GInt 
+  deriving Show
+
+data GS =
+   GConjS GConj GS GS 
+ | GPredAP GNP GAP 
+  deriving Show
+
+
+instance Gf GA2 where
+ gf GDivisible = DTr [] (AC (CId "Divisible")) []
+ gf GEqual = DTr [] (AC (CId "Equal")) []
+ gf GGreater = DTr [] (AC (CId "Greater")) []
+ gf GSmaller = DTr [] (AC (CId "Smaller")) []
+
+instance Gf GAP where
+ gf (GComplA2 x1 x2) = DTr [] (AC (CId "ComplA2")) [gf x1, gf x2]
+ gf (GConjAP x1 x2 x3) = DTr [] (AC (CId "ConjAP")) [gf x1, gf x2, gf x3]
+ gf GEven = DTr [] (AC (CId "Even")) []
+ gf GOdd = DTr [] (AC (CId "Odd")) []
+ gf GPrime = DTr [] (AC (CId "Prime")) []
+
+instance Gf GCN where
+ gf (GModCN x1 x2) = DTr [] (AC (CId "ModCN")) [gf x1, gf x2]
+ gf GNumber = DTr [] (AC (CId "Number")) []
+
+instance Gf GConj where
+ gf GAnd = DTr [] (AC (CId "And")) []
+ gf GOr = DTr [] (AC (CId "Or")) []
+
+instance Gf GNP where
+ gf (GConjNP x1 x2 x3) = DTr [] (AC (CId "ConjNP")) [gf x1, gf x2, gf x3]
+ gf (GEvery x1) = DTr [] (AC (CId "Every")) [gf x1]
+ gf (GSome x1) = DTr [] (AC (CId "Some")) [gf x1]
+ gf (GUseInt x1) = DTr [] (AC (CId "UseInt")) [gf x1]
+
+instance Gf GS where
+ gf (GConjS x1 x2 x3) = DTr [] (AC (CId "ConjS")) [gf x1, gf x2, gf x3]
+ gf (GPredAP x1 x2) = DTr [] (AC (CId "PredAP")) [gf x1, gf x2]
+
+
+instance Fg GA2 where
+ fg t =
+  case t of
+    DTr [] (AC (CId "Divisible")) [] -> GDivisible 
+    DTr [] (AC (CId "Equal")) [] -> GEqual 
+    DTr [] (AC (CId "Greater")) [] -> GGreater 
+    DTr [] (AC (CId "Smaller")) [] -> GSmaller 
+    _ -> error ("no A2 " ++ show t)
+
+instance Fg GAP where
+ fg t =
+  case t of
+    DTr [] (AC (CId "ComplA2")) [x1,x2] -> GComplA2 (fg x1) (fg x2)
+    DTr [] (AC (CId "ConjAP")) [x1,x2,x3] -> GConjAP (fg x1) (fg x2) (fg x3)
+    DTr [] (AC (CId "Even")) [] -> GEven 
+    DTr [] (AC (CId "Odd")) [] -> GOdd 
+    DTr [] (AC (CId "Prime")) [] -> GPrime 
+    _ -> error ("no AP " ++ show t)
+
+instance Fg GCN where
+ fg t =
+  case t of
+    DTr [] (AC (CId "ModCN")) [x1,x2] -> GModCN (fg x1) (fg x2)
+    DTr [] (AC (CId "Number")) [] -> GNumber 
+    _ -> error ("no CN " ++ show t)
+
+instance Fg GConj where
+ fg t =
+  case t of
+    DTr [] (AC (CId "And")) [] -> GAnd 
+    DTr [] (AC (CId "Or")) [] -> GOr 
+    _ -> error ("no Conj " ++ show t)
+
+instance Fg GNP where
+ fg t =
+  case t of
+    DTr [] (AC (CId "ConjNP")) [x1,x2,x3] -> GConjNP (fg x1) (fg x2) (fg x3)
+    DTr [] (AC (CId "Every")) [x1] -> GEvery (fg x1)
+    DTr [] (AC (CId "Some")) [x1] -> GSome (fg x1)
+    DTr [] (AC (CId "UseInt")) [x1] -> GUseInt (fg x1)
+    _ -> error ("no NP " ++ show t)
+
+instance Fg GS where
+ fg t =
+  case t of
+    DTr [] (AC (CId "ConjS")) [x1,x2,x3] -> GConjS (fg x1) (fg x2) (fg x3)
+    DTr [] (AC (CId "PredAP")) [x1,x2] -> GPredAP (fg x1) (fg x2)
+    _ -> error ("no S " ++ show t)
+
+
diff --git a/examples/tutorial/semantics/Logic.hs b/examples/tutorial/semantics/Logic.hs
index e3d72f069..b5c615da5 100644
--- a/examples/tutorial/semantics/Logic.hs
+++ b/examples/tutorial/semantics/Logic.hs
@@ -1,7 +1,7 @@
 module Logic where
 
 data Prop =
-    Atom Ident [Exp] 
+    Pred Ident [Exp] 
   | And Prop Prop
   | Or  Prop Prop
   | If  Prop Prop
@@ -11,17 +11,16 @@ data Prop =
  deriving Show
 
 data Exp = 
-    Const Ident
+    App Ident [Exp]
   | Var Int -- de Bruijn index
  deriving Show
 
-
 type Ident = String
 
 data Model a = Model {
-  ind :: Ident -> a,
-  val :: Ident -> [a] -> Bool,
-  dom :: [a]
+  app  :: Ident -> [a] -> a,
+  prd  :: Ident -> [a] -> Bool,
+  dom  :: [a]
   }
 
 type Assignment a = [a]
@@ -34,12 +33,12 @@ look i assign = assign !! i
 
 valExp :: Model a -> Assignment a -> Exp -> a
 valExp model assign exp = case exp of
-  Const c -> ind model c
-  Var i   -> look i assign
+  App f xs -> app model f (map (valExp model assign) xs)
+  Var i    -> look i assign
 
 valProp :: Model a -> Assignment a -> Prop -> Bool
 valProp model assign prop = case prop of
-  Atom f xs -> val model f (map (valExp model assign) xs)
+  Pred f xs -> prd model f (map (valExp model assign) xs)
   And  a b  -> v a && v b
   Or   a b  -> v a || v b
   If   a b  -> if v a then v b else True
@@ -49,20 +48,44 @@ valProp model assign prop = case prop of
  where
    v = valProp model assign
 
+liftProp :: Int -> Prop -> Prop
+liftProp i p = case p of
+  Pred f xs -> Pred f (map liftExp xs)
+  And a b   -> And (lift a) (lift b)
+  Or  a b   -> Or (lift a) (lift b)
+  If  a b   -> If (lift a) (lift b)
+  Not a     -> Not (lift a)
+  All p     -> All (liftProp (i+1) p)
+  Exist p   -> Exist (liftProp (i+1) p)
+ where
+   lift = liftProp i
+   liftExp e = case e of
+     App f xs -> App f (map liftExp xs)
+     Var j    -> Var (j + i)
+     _ -> e
+
+
+-- example: initial segments of integers
+
 intModel :: Int -> Model Int
 intModel mx = Model {
-  ind = read,
-  val = \f xs -> case (f,xs) of
+  app = \f xs -> case (f,xs) of
+    ("+",_) -> sum xs
+    (_,[])  -> read f,
+  prd = \f xs -> case (f,xs) of
     ("E",[x])   -> even x
     ("<",[x,y]) -> x < y
+    ("=",[x,y]) -> x == y
     _ -> error "undefined val",
   dom = [0 .. mx]
   }
 
 exModel = intModel 100
 
-ev x   = Atom "E" [x]
-lt x y = Atom "<" [x,y]
+ev x   = Pred "E" [x]
+lt x y = Pred "<" [x,y]
+eq x y = Pred "=" [x,y]
+int i = App (show i) []
 
 ex1 :: Prop
 ex1 = Exist (ev (Var 0))
@@ -71,7 +94,7 @@ ex2 :: Prop
 ex2 = All (Exist (lt (Var 1) (Var 0)))
 
 ex3 :: Prop
-ex3 = All (If (lt (Var 0) (Const "100")) (Exist (lt (Var 1) (Var 0))))
+ex3 = All (If (lt (Var 0) (int 100)) (Exist (lt (Var 1) (Var 0))))
 
 ex4 :: Prop
 ex4 = All (All (If (lt (Var 1) (Var 0)) (Not (lt (Var 0) (Var 1)))))
diff --git a/examples/tutorial/semantics/SemBase.hs b/examples/tutorial/semantics/SemBase.hs
new file mode 100644
index 000000000..699c4942c
--- /dev/null
+++ b/examples/tutorial/semantics/SemBase.hs
@@ -0,0 +1,43 @@
+module SemBase where
+
+import GSyntax
+import Logic
+
+-- translation of Base syntax to Logic
+
+iS :: GS -> Prop
+iS s = case s of
+  GPredAP np ap -> iNP np (iAP ap)
+  GConjS c s t  -> iConj c (iS s) (iS t)
+
+iNP :: GNP -> (Exp -> Prop) -> Prop
+iNP np p = case np of
+  GEvery cn -> All   (If  (iCN cn var) (p var)) ----
+  GSome  cn -> Exist (And (iCN cn var) (p var)) ----
+  GConjNP c np1 np2 -> iConj c (iNP np1 p) (iNP np2 p)
+  GUseInt (GInt i) -> p (int i)
+
+iAP :: GAP -> Exp -> Prop
+iAP ap e = case ap of
+  GComplA2 a2 np    -> iNP np (iA2 a2 e)
+  GConjAP c ap1 ap2 -> iConj c (iAP ap1 e) (iAP ap2 e)
+  GEven -> ev e
+  GOdd -> Not (ev e)
+
+iCN :: GCN -> Exp -> Prop
+iCN cn e = case cn of
+  GModCN ap cn0 -> And (iCN cn0 e) (iAP ap e)
+  GNumber -> eq e e
+
+iConj :: GConj -> Prop -> Prop -> Prop
+iConj c = case c of
+  GAnd -> And
+  GOr  -> Or
+
+iA2 :: GA2 -> Exp -> Exp -> Prop
+iA2 a2 e1 e2 = case a2 of
+  GGreater -> lt e2 e1
+  GSmaller -> lt e1 e2 
+  GEqual   -> eq e1 e2
+
+var = Var 0
diff --git a/examples/tutorial/semantics/Top.hs b/examples/tutorial/semantics/Top.hs
new file mode 100644
index 000000000..6027b238c
--- /dev/null
+++ b/examples/tutorial/semantics/Top.hs
@@ -0,0 +1,23 @@
+module Main where
+
+import GSyntax
+import SemBase
+import Logic
+import GF.GFCC.API
+
+main :: IO ()
+main = do
+  gr <- file2grammar "base.gfcc"
+  loop gr
+
+loop :: MultiGrammar -> IO ()
+loop gr = do
+  s <- getLine
+  let t:_ = parse gr "BaseEng" "S" s
+  putStrLn $ showTree t
+  let p = iS $ fg t
+  putStrLn $ show p
+  let v = valProp exModel [] p
+  putStrLn $ show v
+  loop gr
+