summaryrefslogtreecommitdiff
path: root/examples/tutorial/old/semantics/SemBase.hs
diff options
context:
space:
mode:
authoraarne <aarne@cs.chalmers.se>2008-11-11 10:28:32 +0000
committeraarne <aarne@cs.chalmers.se>2008-11-11 10:28:32 +0000
commita5300ad062b82154f3f9533e143ea35515e6c39e (patch)
treea7eddd52596e0d216f17c9c7581d6ea67f9d8879 /examples/tutorial/old/semantics/SemBase.hs
parentdb18350b1e55f7edfca8f02b0b233a6a7dcbb1ec (diff)
tutorial complete with server and js
Diffstat (limited to 'examples/tutorial/old/semantics/SemBase.hs')
-rw-r--r--examples/tutorial/old/semantics/SemBase.hs42
1 files changed, 42 insertions, 0 deletions
diff --git a/examples/tutorial/old/semantics/SemBase.hs b/examples/tutorial/old/semantics/SemBase.hs
new file mode 100644
index 000000000..b682010e1
--- /dev/null
+++ b/examples/tutorial/old/semantics/SemBase.hs
@@ -0,0 +1,42 @@
+module SemBase where
+
+import Base
+import Logic
+
+-- translation of Base syntax to Logic
+
+iS :: GS -> Prop
+iS s = case s of
+ GPredAP np ap -> iNP np (iAP ap)
+
+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