diff --git a/examples-3.0/tutorial/semantics/Answer.hs b/examples-3.0/tutorial/semantics/Answer.hs new file mode 100644 index 000000000..08a76c5f1 --- /dev/null +++ b/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 + diff --git a/examples-3.0/tutorial/semantics/AnswerBase.hs b/examples-3.0/tutorial/semantics/AnswerBase.hs new file mode 100644 index 000000000..56e2b5451 --- /dev/null +++ b/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 [] = [] diff --git a/examples-3.0/tutorial/semantics/Base.gf b/examples-3.0/tutorial/semantics/Base.gf new file mode 100644 index 000000000..4586c3106 --- /dev/null +++ b/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 ; +} diff --git a/examples-3.0/tutorial/semantics/BaseEng.gf b/examples-3.0/tutorial/semantics/BaseEng.gf new file mode 100644 index 000000000..bd79bc98c --- /dev/null +++ b/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 "," ; + +} diff --git a/examples-3.0/tutorial/semantics/BaseI.gf b/examples-3.0/tutorial/semantics/BaseI.gf new file mode 100644 index 000000000..d90431e2f --- /dev/null +++ b/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)) ; + +} diff --git a/examples-3.0/tutorial/semantics/BaseIEng.gf b/examples-3.0/tutorial/semantics/BaseIEng.gf new file mode 100644 index 000000000..a73bd44c6 --- /dev/null +++ b/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) ; diff --git a/examples-3.0/tutorial/semantics/BaseSwe.gf b/examples-3.0/tutorial/semantics/BaseSwe.gf new file mode 100644 index 000000000..6329c1c9c --- /dev/null +++ b/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) ; diff --git a/examples-3.0/tutorial/semantics/GSyntax.hs b/examples-3.0/tutorial/semantics/GSyntax.hs new file mode 100644 index 000000000..6c67e40aa --- /dev/null +++ b/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) + + diff --git a/examples-3.0/tutorial/semantics/LexBase.gf b/examples-3.0/tutorial/semantics/LexBase.gf new file mode 100644 index 000000000..83713a35f --- /dev/null +++ b/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 ; --- +} diff --git a/examples-3.0/tutorial/semantics/LexBaseEng.gf b/examples-3.0/tutorial/semantics/LexBaseEng.gf new file mode 100644 index 000000000..aea3a838b --- /dev/null +++ b/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") ; --- + +} diff --git a/examples-3.0/tutorial/semantics/LexBaseSwe.gf b/examples-3.0/tutorial/semantics/LexBaseSwe.gf new file mode 100644 index 000000000..6ac1904aa --- /dev/null +++ b/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 ; --- + +} diff --git a/examples-3.0/tutorial/semantics/Logic.hs b/examples-3.0/tutorial/semantics/Logic.hs new file mode 100644 index 000000000..b5c615da5 --- /dev/null +++ b/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))))) + diff --git a/examples-3.0/tutorial/semantics/SemBase.hs b/examples-3.0/tutorial/semantics/SemBase.hs new file mode 100644 index 000000000..24073894b --- /dev/null +++ b/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 diff --git a/examples-3.0/tutorial/semantics/Top.hs b/examples-3.0/tutorial/semantics/Top.hs new file mode 100644 index 000000000..6027b238c --- /dev/null +++ b/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 +