tutorial semantics example works except one rul

examples-3.0/tutorial/semantics/Answer.hs

@@ -0,0 +1,21 @@
+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
+  case parse gr "BaseEng" "Question" s of
+    [] -> putStrLn "no parse"
+    ts -> mapM_ answer ts
+  loop gr
+ where
+   answer t = putStrLn $ linearize gr "BaseEng" $ gf $ question2answer $ fg t
+

examples-3.0/tutorial/semantics/AnswerBase.hs

@@ -0,0 +1,90 @@
+module AnswerBase where
+
+import GSyntax
+
+-- interpretation of Base
+
+type Prop = Bool
+type Ent = Int
+domain = [0 .. 100]
+
+iS :: GS -> Prop
+iS s = case s of
+  GPredAP np ap -> iNP np (iAP ap)
+
+iNP :: GNP -> (Ent -> 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
+  GNone     -> not (any (\x -> p x) domain)
+  GMany pns -> and (map p (iListPN pns))
+  GConjNP c np1 np2 -> iConj c (iNP np1 p) (iNP np2 p)
+  GUsePN a -> p (iPN a)
+
+iPN :: GPN -> Ent
+iPN pn = case pn of  
+  GUseInt i -> iInt i
+  GSum pns -> sum (iListPN pns)
+  GProduct pns -> product (iListPN pns)
+  GGCD pns -> foldl1 gcd (iListPN pns)
+
+iAP :: GAP -> Ent -> 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   -> odd e
+  GPrime -> prime e
+
+iCN :: GCN -> Ent -> 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 -> Ent -> Ent -> Prop
+iA2 a2 e1 e2 = case a2 of
+  GGreater -> e1 > e2
+  GSmaller -> e1 < e2 
+  GEqual   -> e1 == e2
+  GDivisible -> e2 /= 0 && mod e1 e2 == 0
+
+iListPN :: GListPN -> [Ent]
+iListPN gls = case gls of
+  GListPN pns -> map iPN pns
+
+iInt :: GInt -> Ent
+iInt gi = case gi of
+  GInt i -> fromInteger i
+
+-- questions and answers
+
+iQuestion :: GQuestion -> Either Bool [Ent]
+iQuestion q = case q of
+  GWhatIs pn      -> Right [iPN pn]  -- computes the value
+  GWhichAre cn ap -> Right [e | e <- domain, iCN cn e, iAP ap e]
+  GQuestS s       -> Left  (iS s)
+
+question2answer :: GQuestion -> GAnswer
+question2answer q = case iQuestion q of
+  Left True  -> GYes
+  Left False -> GNo
+  Right []   -> GValue GNone
+  Right [v]  -> GValue (GUsePN (ent2pn v))
+  Right vs   -> GValue (GMany (GListPN (map ent2pn vs)))
+
+ent2pn :: Ent -> GPN
+ent2pn e = GUseInt (GInt (toInteger e))
+
+
+-- auxiliary
+
+prime :: Int -> Bool
+prime x = elem x primes where
+  primes = sieve [2 .. x]
+  sieve (p:xs) = p : sieve [ n | n <- xs, n `mod` p > 0 ]
+  sieve [] = []

examples-3.0/tutorial/semantics/Base.gf

@@ -0,0 +1,60 @@
+-- abstract syntax of a query language
+
+abstract Base = {
+
+cat
+  S ; 
+  NP ; 
+  PN ;
+  CN ; 
+  AP ; 
+  A2 ; 
+  Conj ;
+fun 
+
+-- sentence syntax
+  PredAP  : NP -> AP -> S ;
+
+  ComplA2 : A2 -> NP -> AP ;
+
+  ModCN   : AP -> CN -> CN ;
+
+  ConjAP  : Conj -> AP -> AP -> AP ;
+  ConjNP  : Conj -> NP -> NP -> NP ;
+
+  UsePN   : PN -> NP ;
+  Every   : CN -> NP ;
+  Some    : CN -> NP ;
+
+  And, Or : Conj ;  
+
+-- lexicon
+
+  UseInt  : Int -> PN ;
+
+  Number : CN ;
+  Even, Odd, Prime : AP ;
+  Equal, Greater, Smaller, Divisible  : A2 ;
+
+  Sum, Product, GCD : ListPN -> PN ;
+
+-- adding questions
+
+cat
+  Question ;
+  Answer ;
+  ListPN ;
+fun
+  WhatIs   : PN -> Question ;
+  WhichAre : CN -> AP -> Question ;
+  QuestS   : S -> Question ;
+
+  Yes   : Answer ;
+  No    : Answer ;
+  Value : NP -> Answer ;
+
+  None  : NP ;
+  Many  : ListPN -> NP ;
+  BasePN : PN -> PN -> ListPN ;
+  ConsPN : PN -> ListPN -> ListPN ; 
+}

examples-3.0/tutorial/semantics/BaseEng.gf

@@ -0,0 +1,56 @@
+--# -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 ;
+
+  ConjAP c = infixSS c.s ;
+  ConjNP c = infixSS c.s ;
+
+  UsePN a = a ;
+  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") ;
+ 
+  Sum     = prefixSS ["the sum of"] ;
+  Product = prefixSS ["the product of"] ;
+  GCD     = prefixSS ["the greatest common divisor of"] ;
+
+  WhatIs = prefixSS ["what is"] ;
+  WhichAre cn ap = ss ("which" ++ cn.s ++ "is" ++ ap.s) ; ---- are
+  QuestS s = s ; ---- inversion
+
+  Yes = ss "yes" ;
+  No = ss "no" ;
+
+  Value np = np ;
+  None = ss "none" ;
+  Many list = list ;
+
+  BasePN = infixSS "and" ;
+  ConsPN = infixSS "," ;
+  
+}

examples-3.0/tutorial/semantics/BaseI.gf

@@ -0,0 +1,70 @@
+incomplete concrete BaseI of Base = 
+  open Syntax, (G = Grammar), Symbolic, LexBase in {
+
+flags lexer=literals ; unlexer=text ;
+
+lincat
+  Question = G.Phr ;
+  Answer = G.Phr ;
+  S  = G.Cl ;
+  NP = G.NP ;
+  PN = G.NP ;
+  CN = G.CN ;
+  AP = G.AP ;
+  A2 = G.A2 ;
+  Conj = G.Conj ;
+  ListPN = G.ListNP ;
+
+lin 
+  PredAP  = mkCl ;
+
+  ComplA2 = mkAP ;
+
+  ModCN   = mkCN ;
+
+  ConjAP = mkAP ;
+  ConjNP = mkNP ;
+
+  UsePN p = p ;
+  Every = mkNP every_Det ;
+  Some  = mkNP someSg_Det ;
+
+  And = and_Conj ;
+  Or  = or_Conj ;
+
+  UseInt i = symb (i ** {lock_Int = <>}) ; ---- terrible to need this
+
+  Number = mkCN number_N ;
+
+  Even = mkAP even_A ;
+  Odd  = mkAP odd_A ;
+  Prime = mkAP prime_A ;
+  Equal = equal_A2 ;
+  Greater = greater_A2 ;
+  Smaller = smaller_A2 ;
+  Divisible = divisible_A2 ;
+ 
+  Sum     = prefix sum_N2 ;
+  Product = prefix product_N2 ;
+  GCD nps = mkNP (mkDet DefArt (mkOrd great_A)) 
+              (mkCN common_A (mkCN divisor_N2 (mkNP and_Conj nps))) ;
+
+  WhatIs np = mkPhr (mkQS (mkQCl whatSg_IP (mkVP np))) ;
+--  WhichAre cn ap = mkPhr (mkQS (mkQCl (mkIP (mkIDet which_IQuant plNum) cn) (mkVP ap))) ;
+  QuestS s = mkPhr (mkQS (mkQCl s)) ;
+
+  Yes = mkPhr yes_Utt ;
+  No = mkPhr no_Utt ;
+
+  Value np = mkPhr (mkUtt np) ;
+  Many list = mkNP and_Conj list ;
+  None  = none_NP ;
+
+  BasePN = G.BaseNP ;
+  ConsPN = G.ConsNP ;
+
+oper
+  prefix : G.N2 -> G.ListNP -> G.NP = \n2,nps -> 
+    mkNP DefArt (mkCN n2 (mkNP and_Conj nps)) ;
+  
+}

examples-3.0/tutorial/semantics/BaseIEng.gf

@@ -0,0 +1,8 @@
+--# -path=.:prelude:present:api:mathematical
+
+concrete BaseIEng of Base = BaseI with
+  (Syntax = SyntaxEng), 
+  (Grammar = GrammarEng), 
+  (G = GrammarEng), 
+  (Symbolic = SymbolicEng), 
+  (LexBase = LexBaseEng) ;

examples-3.0/tutorial/semantics/BaseSwe.gf

@@ -0,0 +1,8 @@
+--# -path=.:prelude:present:api:mathematical
+
+concrete BaseSwe of Base = BaseI with
+  (Syntax = SyntaxSwe), 
+  (Grammar = GrammarSwe), 
+  (G = GrammarSwe), 
+  (Symbolic = SymbolicSwe), 
+  (LexBase = LexBaseSwe) ;

examples-3.0/tutorial/semantics/GSyntax.hs

@@ -0,0 +1,242 @@
+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 GAnswer =
+   GNo 
+ | GValue GNP 
+ | GYes 
+  deriving Show
+
+data GCN =
+   GModCN GAP GCN 
+ | GNumber 
+  deriving Show
+
+data GConj =
+   GAnd 
+ | GOr 
+  deriving Show
+
+newtype GListPN = GListPN [GPN] deriving Show
+
+data GNP =
+   GConjNP GConj GNP GNP 
+ | GEvery GCN 
+ | GMany GListPN 
+ | GNone 
+ | GSome GCN 
+ | GUsePN GPN 
+  deriving Show
+
+data GPN =
+   GGCD GListPN 
+ | GProduct GListPN 
+ | GSum GListPN 
+ | GUseInt GInt 
+  deriving Show
+
+data GQuestion =
+   GQuestS GS 
+ | GWhatIs GPN 
+ | GWhichAre GCN GAP 
+  deriving Show
+
+data 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 GAnswer where
+ gf GNo = DTr [] (AC (CId "No")) []
+ gf (GValue x1) = DTr [] (AC (CId "Value")) [gf x1]
+ gf GYes = DTr [] (AC (CId "Yes")) []
+
+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 GListPN where
+ gf (GListPN [x1,x2]) = DTr [] (AC (CId "BasePN")) [gf x1, gf x2]
+ gf (GListPN (x:xs)) = DTr [] (AC (CId "ConsPN")) [gf x, gf (GListPN xs)]
+
+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 (GMany x1) = DTr [] (AC (CId "Many")) [gf x1]
+ gf GNone = DTr [] (AC (CId "None")) []
+ gf (GSome x1) = DTr [] (AC (CId "Some")) [gf x1]
+ gf (GUsePN x1) = DTr [] (AC (CId "UsePN")) [gf x1]
+
+instance Gf GPN where
+ gf (GGCD x1) = DTr [] (AC (CId "GCD")) [gf x1]
+ gf (GProduct x1) = DTr [] (AC (CId "Product")) [gf x1]
+ gf (GSum x1) = DTr [] (AC (CId "Sum")) [gf x1]
+ gf (GUseInt x1) = DTr [] (AC (CId "UseInt")) [gf x1]
+
+instance Gf GQuestion where
+ gf (GQuestS x1) = DTr [] (AC (CId "QuestS")) [gf x1]
+ gf (GWhatIs x1) = DTr [] (AC (CId "WhatIs")) [gf x1]
+ gf (GWhichAre x1 x2) = DTr [] (AC (CId "WhichAre")) [gf x1, gf x2]
+
+instance Gf GS where 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 GAnswer where
+ fg t =
+  case t of
+    DTr [] (AC (CId "No")) [] -> GNo 
+    DTr [] (AC (CId "Value")) [x1] -> GValue (fg x1)
+    DTr [] (AC (CId "Yes")) [] -> GYes 
+    _ -> error ("no Answer " ++ 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 GListPN where
+ fg t =
+  case t of
+    DTr [] (AC (CId "BasePN")) [x1,x2] -> GListPN [fg x1, fg x2]
+    DTr [] (AC (CId "ConsPN")) [x1,x2] -> let GListPN xs = fg x2 in GListPN (fg x1:xs)
+    _ -> error ("no ListPN " ++ 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 "Many")) [x1] -> GMany (fg x1)
+    DTr [] (AC (CId "None")) [] -> GNone 
+    DTr [] (AC (CId "Some")) [x1] -> GSome (fg x1)
+    DTr [] (AC (CId "UsePN")) [x1] -> GUsePN (fg x1)
+    _ -> error ("no NP " ++ show t)
+
+instance Fg GPN where
+ fg t =
+  case t of
+    DTr [] (AC (CId "GCD")) [x1] -> GGCD (fg x1)
+    DTr [] (AC (CId "Product")) [x1] -> GProduct (fg x1)
+    DTr [] (AC (CId "Sum")) [x1] -> GSum (fg x1)
+    DTr [] (AC (CId "UseInt")) [x1] -> GUseInt (fg x1)
+    _ -> error ("no PN " ++ show t)
+
+instance Fg GQuestion where
+ fg t =
+  case t of
+    DTr [] (AC (CId "QuestS")) [x1] -> GQuestS (fg x1)
+    DTr [] (AC (CId "WhatIs")) [x1] -> GWhatIs (fg x1)
+    DTr [] (AC (CId "WhichAre")) [x1,x2] -> GWhichAre (fg x1) (fg x2)
+    _ -> error ("no Question " ++ show t)
+
+instance Fg GS where
+ fg t =
+  case t of
+    DTr [] (AC (CId "PredAP")) [x1,x2] -> GPredAP (fg x1) (fg x2)
+    _ -> error ("no S " ++ show t)
+
+

examples-3.0/tutorial/semantics/LexBase.gf

@@ -0,0 +1,19 @@
+interface LexBase = open Syntax in {
+
+oper
+  even_A : A ;
+  odd_A : A ;
+  prime_A : A ;
+  common_A : A ;
+  great_A : A ;
+  equal_A2 : A2 ;
+  greater_A2 : A2 ;
+  smaller_A2 : A2 ;
+  divisible_A2 : A2 ;
+  number_N : N ;
+  sum_N2 : N2 ;
+  product_N2 : N2 ;
+  divisor_N2 : N2 ;
+
+  none_NP : NP ; ---
+}

examples-3.0/tutorial/semantics/LexBaseEng.gf

@@ -0,0 +1,20 @@
+instance LexBaseEng of LexBase = open SyntaxEng, ParadigmsEng in {
+
+oper
+  even_A = mkA "even" ;
+  odd_A = mkA "odd" ;
+  prime_A = mkA "prime" ;
+  great_A = mkA "great" ;
+  common_A = mkA "common" ;
+  equal_A2 = mkA2 (mkA "equal") (mkPrep "to") ;
+  greater_A2 = mkA2 (mkA "greater") (mkPrep "than") ; ---
+  smaller_A2 = mkA2 (mkA "smaller") (mkPrep "than") ; ---
+  divisible_A2 = mkA2 (mkA "divisible") (mkPrep "by") ;
+  number_N = mkN "number" ;
+  sum_N2 = mkN2 (mkN "sum") (mkPrep "of") ;
+  product_N2 = mkN2 (mkN "product") (mkPrep "of") ;
+  divisor_N2 = mkN2 (mkN "divisor") (mkPrep "of") ;
+
+  none_NP = mkNP (mkPN "none") ; ---
+
+}

examples-3.0/tutorial/semantics/LexBaseSwe.gf

@@ -0,0 +1,22 @@
+instance LexBaseSwe of LexBase = open SyntaxSwe, ParadigmsSwe in {
+
+oper
+  even_A = mkA "jämn" ;
+  odd_A = invarA "udda" ;
+  prime_A = mkA "prim" ;
+  great_A = mkA "stor" "större" "störst" ;
+  common_A = mkA "gemensam" ;
+  equal_A2 = mkA2 (invarA "lika") (mkPrep "med") ;
+  greater_A2 = mkA2 (invarA "större") (mkPrep "än") ; ---
+  smaller_A2 = mkA2 (invarA "mindre") (mkPrep "än") ; ---
+  divisible_A2 = mkA2 (mkA "delbar") (mkPrep "med") ;
+  number_N = mkN "tal" "tal" ;
+  sum_N2 = mkN2 (mkN "summa") (mkPrep "av") ;
+  product_N2 = mkN2 (mkN "produkt") (mkPrep "av") ;
+  divisor_N2 = mkN2 (mkN "delare") (mkPrep "av") ;
+
+  none_NP = mkNP (mkPN "inget" neutrum) ; ---
+
+  invarA : Str -> A = \x -> mkA x x x x x ; ---
+ 
+}

examples-3.0/tutorial/semantics/Logic.hs

@@ -0,0 +1,101 @@
+module Logic where
+
+data Prop =
+    Pred Ident [Exp] 
+  | And Prop Prop
+  | Or  Prop Prop
+  | If  Prop Prop
+  | Not Prop
+  | All   Prop
+  | Exist Prop
+ deriving Show
+
+data Exp = 
+    App Ident [Exp]
+  | Var Int -- de Bruijn index
+ deriving Show
+
+type Ident = String
+
+data Model a = Model {
+  app  :: Ident -> [a] -> a,
+  prd  :: Ident -> [a] -> Bool,
+  dom  :: [a]
+  }
+
+type Assignment a = [a]
+
+update :: a -> Assignment a -> Assignment a
+update x assign = x : assign
+
+look :: Int -> Assignment a -> a
+look i assign = assign !! i
+
+valExp :: Model a -> Assignment a -> Exp -> a
+valExp model assign exp = case exp of
+  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
+  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
+  Not  a    -> not (v a)
+  All   p   -> all (\x -> valProp model (update x assign) p) (dom model)
+  Exist p   -> any (\x -> valProp model (update x assign) p) (dom model)
+ 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 {
+  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   = 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))
+
+ex2 :: Prop
+ex2 = All (Exist (lt (Var 1) (Var 0)))
+
+ex3 :: Prop
+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)))))
+

examples-3.0/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) (liftProp 0 (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

examples-3.0/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
+

lib/resource-1.4/mathematical/Symbolic.gf

@@ -10,8 +10,8 @@ incomplete resource Symbolic = open Symbol, Grammar in {
       symb : N  -> Digits -> NP ;              -- level 4
       symb : N  -> Card -> NP ;                -- level four
       symb : CN -> Card -> NP ;                -- advanced level four
-      symb : Det -> N  -> Num -> NP ;          -- the number four
-      symb : Det -> CN -> Num -> NP ;          -- the even number four
+      symb : Det -> N  -> Card -> NP ;         -- the number four
+      symb : Det -> CN -> Card -> NP ;         -- the even number four
       symb : Det -> N  -> Str -> Str -> NP ;   -- the levels i and j
       symb : Det -> CN -> [Symb] -> NP         -- the basic levels i, j, and k
       } ;
@@ -31,13 +31,13 @@ incomplete resource Symbolic = open Symbol, Grammar in {
                           = \i -> UsePN (FloatPN i) ;
       symb : N -> Digits -> NP 
                           = \c,i -> CNNumNP (UseN c) (NumDigits i) ;
-      symb : N -> Num -> NP 
+      symb : N -> Card -> NP 
                           = \c,n -> CNNumNP (UseN c) n ;
-      symb : CN -> Num -> NP 
+      symb : CN -> Card -> NP 
                           = \c,n -> CNNumNP c n ;
-      symb : Det -> N  -> Num -> NP
+      symb : Det -> N  -> Card -> NP
                           = \d,n,x -> DetCN d (ApposCN (UseN n) (UsePN (NumPN x))) ;
-      symb : Det -> CN -> Num -> NP
+      symb : Det -> CN -> Card -> NP
                           = \d,n,x -> DetCN d (ApposCN n (UsePN (NumPN x))) ;
       symb : Det -> N  -> Str -> Str -> NP 
                           = \c,n,x,y -> CNSymbNP c (UseN n) (BaseSymb (mkSymb x) (mkSymb y)) ;