packages feed

liboleg 2009.9.1 → 2010.1.1

raw patch · 3 files changed

+745/−1 lines, 3 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

+ Control.ExtensibleDS: (:@) :: e1 -> e2 -> App e1 e2
+ Control.ExtensibleDS: Add1 :: Add1
+ Control.ExtensibleDS: BE_err :: BE_err
+ Control.ExtensibleDS: BE_omega :: BE_omega
+ Control.ExtensibleDS: Control :: e -> Control e
+ Control.ExtensibleDS: ControlAdmin :: e -> ControlAdmin e
+ Control.ExtensibleDS: Deref :: e -> Deref e
+ Control.ExtensibleDS: InFX :: (Value -> Comp) -> Action -> Comp
+ Control.ExtensibleDS: InV :: !Value -> Comp
+ Control.ExtensibleDS: IntC :: Int -> IntC
+ Control.ExtensibleDS: Lam :: V -> e -> Lam e
+ Control.ExtensibleDS: Loc :: Int -> Loc
+ Control.ExtensibleDS: Ref :: e -> Ref e
+ Control.ExtensibleDS: Set :: e1 -> e2 -> Set e1 e2
+ Control.ExtensibleDS: StoAdmin :: Sto -> e -> StoAdmin e
+ Control.ExtensibleDS: V :: String -> V
+ Control.ExtensibleDS: VF :: (Value -> Value) -> Value
+ Control.ExtensibleDS: VI :: Int -> Value
+ Control.ExtensibleDS: VP :: Value -> Value -> Value
+ Control.ExtensibleDS: VS :: String -> Value
+ Control.ExtensibleDS: VT :: Tag -> Value -> Value
+ Control.ExtensibleDS: class Interpretor exp
+ Control.ExtensibleDS: class PL u
+ Control.ExtensibleDS: class PN u
+ Control.ExtensibleDS: class PV u
+ Control.ExtensibleDS: data Add1
+ Control.ExtensibleDS: data App e1 e2
+ Control.ExtensibleDS: data BE_err
+ Control.ExtensibleDS: data BE_omega
+ Control.ExtensibleDS: data Comp
+ Control.ExtensibleDS: data Control e
+ Control.ExtensibleDS: data ControlAdmin e
+ Control.ExtensibleDS: data Deref e
+ Control.ExtensibleDS: data IntC
+ Control.ExtensibleDS: data Lam e
+ Control.ExtensibleDS: data Ref e
+ Control.ExtensibleDS: data Set e1 e2
+ Control.ExtensibleDS: data StoAdmin e
+ Control.ExtensibleDS: data Value
+ Control.ExtensibleDS: inComp :: Comp -> Value
+ Control.ExtensibleDS: inControl :: (Value -> Comp) -> Value
+ Control.ExtensibleDS: inL :: (PL u) => Loc -> u
+ Control.ExtensibleDS: inN :: (PN u) => Int -> u
+ Control.ExtensibleDS: inP :: (PV u) => Proc -> u
+ Control.ExtensibleDS: inSto :: Sto -> Value
+ Control.ExtensibleDS: init_sto :: Sto
+ Control.ExtensibleDS: instance (Interpretor e) => Interpretor (Control e)
+ Control.ExtensibleDS: instance (Interpretor e) => Interpretor (ControlAdmin e)
+ Control.ExtensibleDS: instance (Interpretor e) => Interpretor (Deref e)
+ Control.ExtensibleDS: instance (Interpretor e) => Interpretor (Lam e)
+ Control.ExtensibleDS: instance (Interpretor e) => Interpretor (Ref e)
+ Control.ExtensibleDS: instance (Interpretor e) => Interpretor (StoAdmin e)
+ Control.ExtensibleDS: instance (Interpretor e1, Interpretor e2) => Interpretor (App e1 e2)
+ Control.ExtensibleDS: instance (Interpretor e1, Interpretor e2) => Interpretor (Set e1 e2)
+ Control.ExtensibleDS: instance Eq Loc
+ Control.ExtensibleDS: instance Eq V
+ Control.ExtensibleDS: instance Interpretor Add1
+ Control.ExtensibleDS: instance Interpretor BE_err
+ Control.ExtensibleDS: instance Interpretor BE_omega
+ Control.ExtensibleDS: instance Interpretor IntC
+ Control.ExtensibleDS: instance Interpretor V
+ Control.ExtensibleDS: instance PL Value
+ Control.ExtensibleDS: instance PN Value
+ Control.ExtensibleDS: instance PV Value
+ Control.ExtensibleDS: instance Show Comp
+ Control.ExtensibleDS: instance Show Loc
+ Control.ExtensibleDS: instance Show V
+ Control.ExtensibleDS: instance Show Value
+ Control.ExtensibleDS: interpret :: (Interpretor exp) => exp -> Env Value -> Comp
+ Control.ExtensibleDS: newtype Loc
+ Control.ExtensibleDS: newtype V
+ Control.ExtensibleDS: prComp :: Value -> Maybe Comp
+ Control.ExtensibleDS: prControl :: Value -> Maybe (Value -> Comp)
+ Control.ExtensibleDS: prL :: (PL u) => u -> Maybe Loc
+ Control.ExtensibleDS: prN :: (PN u) => u -> Maybe Int
+ Control.ExtensibleDS: prP :: (PV u) => u -> Maybe (Proc)
+ Control.ExtensibleDS: prSto :: Value -> Maybe Sto
+ Control.ExtensibleDS: type Action = Value
+ Control.ExtensibleDS: type Env v = V -> v
+ Control.ExtensibleDS: type Proc = Value -> Comp
+ Control.ExtensibleDS: type Sto = (Int, Loc -> Value)
+ Control.ExtensibleDS: type Tag = String
+ Control.ExtensibleDS: type Var = V
+ Control.ExtensibleDS: vf :: Var
+ Control.ExtensibleDS: vr :: Var
+ Control.ExtensibleDS: vx :: Var
+ Control.ExtensibleDS: vy :: Var

Files

+ Control/ExtensibleDS.hs view
@@ -0,0 +1,527 @@+{-# LANGUAGE PatternGuards #-}+-- |+--  Extensible Denotational Semantics+--+--+-- This work is a generalization of +--   /Extensible Denotational Language Specifications+--    Robert Cartwright, Matthias Felleisen+--    Theor. Aspects of Computer Software, 1994/+--    <http://citeseer.ist.psu.edu/69837.html>+--+-- to be referred to as EDLS.+--+-- We implement the enhanced EDLS in Haskell and add delimited control.+-- To be precise, we implement the Base interpreter (whose sole+-- operations are Loop and Error) and the following extensions: CBV+-- lambda-calculus, Arithmetic, Storage, Control. The extensions can be+-- added to the Base interpreter in any order and in any combination.+-- +-- Our implementation has the following advantages over EDLS:+--+-- * support for delimited control+-- * support for a local storage (including `thread-local' storage and+--   general delimited dynamic binding)+-- * extensions do not have to be composed explicitly, and so the+--   composition order truly does not matter.  In the+--   original EDLS, one+--   had to write interpreter composition explicitly. In our approach, an+--   extension is pulled in automatically if the program includes the+--   corresponding syntactic forms. For example, if a program contains+--   storage cell creation and dereference operations, the Storage extension+--   will automatically be used to interpret the program.+--+-- Our main departure from EDLS is is the removal of the `central+-- authority'. There is no semantic `admin' function. Rather, admin is+-- part of the source language and can be used at any place in the+-- code. The `central authority' of EDLS must be an extensible function,+-- requiring meta-language facilities to implement (such as quite+-- non-standard Scheme modules). We do not have central+-- authority. Rather, we have bureaucracy: each specific effect handler+-- interprets its own effects as it can, throwing the rest `upstairs' for+-- higher-level bureaucrats to deal with. Extensibility arises+-- automatically.+-- +-- We take the meaning of a program to be the union of Values and+-- (unfulfilled) Actions. If the meaning of the program is a (non-bottom)+-- value, the program is terminating. If the meaning of the program is an+-- Action -- the program finished with an error, such as an action to+-- access a non-existing storage cell, or shift without reset, or a+-- user-raised error.+-- +-- Incidentally, EDLS stresses on p. 2 (the last full paragraph) that+-- their schema critically relies on the distinction between a complete+-- program and a nested program phrase. Our contribution (which is the+-- consequence of removing the central admin, making it first-class) is+-- eliminating such a distinction! EDLS says, at the very top of p. 3,+-- that the handle in the effect message ``is roughly a conventional+-- continuation.'' Because the admin of EDLS is `outside' of the program+-- (at the point of infinity, so to speak), its continuation indeed+-- appears undelimited. By making our `admin' a part of the source+-- language, we recognize the handle in the effect message for what it+-- is: a _delimited_ continuation.+-- +-- As we see below, the Control aspect is orthogonal to the CBV+-- aspect. So, we can just as easily replace the CBV extension with the+-- CBN extension, which will give us the denotation of delimited control+-- in CBN.+-- +-- +-- We shall be using Haskell to express denotations, taking advantage of+-- the fact that Haskell values are `lifted'. See also the remark on p21+-- of EDLS: someone (ref. [4]) showed that sets and partial functions can+-- suffice...+-- +-- +-- Our program denotations are stable: they have the same form regardless+-- of a particular composition of modular interpreters.  See Section 3.5+-- of EDLS for precise formulation (and the last paragraph of Section 3.4+-- for concise informal statement of stability). Also see the comparison+-- with the monads on p. 20: different monads assign numeral radically+-- different meanings, depending on the monad. But in EDLS, a numeral has+-- exactly the same denotation.+-- +-- The meaning of an expression is also the same and stable, no matter+-- what the interpreter is: it is a function from Env to Computations+-- (the latter being the union of values and unfulfilled effects -- the+-- same union mentioned above).+-- +-- However, by using handlers, some effect messages can be subtracted:+-- so, strictly speaking, the denotation of a fragment is V ++-- effect-message-issued - effect-messages handled.  There seem to be a+-- connection with effect systems.+-- +-- +-- Additional notes on EDLS:+-- +-- The abstract and p. 2 (especially the last full paragraph) are+-- so well-written!+-- +-- p. 5, bottom: ``It [ref \x.x, where ref means what it does in ML] +-- is a closed expression that does not diverge, is not a value, and+-- cannot be reduced to a value without affecting the context. We refer+-- to such results as _effects_.''+-- +-- Beginning of Section 3 and App A give a very good introduction+-- to the denotational semantics.+-- +-- p. 6: ``Algebraically speaking, the interpreter is (roughly) a+-- homomorphism from syntax to semantics''+-- +-- ``A straightforward representation of an evaluation context is a+-- function from values to computations, which directly corresponds to+-- its operational usage as a function from syntactic values to+-- expressions.'' (p. 8). EDLS then notices that the `handle' has+-- the same type as the denotation of a context. Footnote 6 notes that+-- handler is roughly the composition combinator for functions from values+-- to computations [contexts!] and it superficially relates to [bind]+-- but does not satisfy all monad laws.+-- +-- The last of EDLS Sec 3.5, p. 15: ``Informally speaking, this property+-- [stable denotations] asserts that in the framework of extensible+-- semantics, the addition of a programming construct corresponds to the+-- addition of a new ``dimension'' to the space of meaning. [The+-- equations, featuring injection and projection functions, make that+-- precise and clear.] The reader may want to contrast this general+-- statement with the numerous papers on the relationship between direct+-- and continuation semantics.''+-- +-- The practical consequence of the lack of stability of denotations for+-- monads is that monadic transformers put layers upon layers of thunks,+-- which have to be carried over _in full_ from one sub-expression into+-- the other, even if no single subexpression uses all of the features.+-- +-- The present code is not written in idiomatic Haskell and does not take+-- advantage of types at all. The ubiquitous projections from the+-- universal domain tantamount to ``dynamic typing.''  The code is+-- intentionally written to be close to the EDLS paper, emphasizing+-- denotational semantics (whose domains are untyped). One can certainly+-- do better, for example, employ user-defined datatypes for tagged+-- values, avoiding the ugly string-tagged VT.+--++module Control.ExtensibleDS where++import Data.Maybe++------------------------------------------------------------------------+-- The base interpreter+++-- | The universal domain+-- Yes, it is untyped... But Denot semantics is like this anyway...+-- Bottom is the implicit member of this domain.+data Value = VI Int                     -- integers+           | VS String                  -- strings+           | VP Value Value             -- pairs+           | VF (Value -> Value)        -- functions+           | VT Tag Value               -- tagged value++type Tag = String++type Action = Value                     -- only differently tagged++instance Show Value where+    show (VI x) = show x+    show (VS x) = show x+    show (VT tag v) = "{"++show tag++" "++show v++"}"+    show (VP x1 x2) = show (x1,x2)+    show (VF _)  = "<procedure>"++++-- | Computations: just like in EDLS+-- The strictness of inV guarantees that inV bottom = bottom, as+-- on Fig. 3 of EDLS+-- Error is always a part of the computation+--+data Comp = InV !Value | InFX (Value -> Comp) Action++instance Show Comp where+    show (InV v) = show v+    show (InFX _ a) = "Effect: " ++ show a+++-- | Auxiliary functions+newtype V = V String deriving (Eq, Show) -- Variables+type Env v = V -> v+empty_env x = error $ "impossible: an open program? var " ++ show x+ext_env env x v y | x == y = v+ext_env env x v y = env y+++-- | Note that inV is essentially the identity `partial' continuation+inAC action = InFX InV action++-- | The error `raise' action and its tag+tagErr = "Err"+raise err = inAC $ VT tagErr (VS err)++-- | The universal handler of actions+-- It propagates the action request InFX up.+-- Since we do case-analysis on the first argument, v, the handler+-- is strict in that argument. That is, handler bottom ==> bottom,+-- as required by Fig. 3 of EDLS.+-- The last clause is essentially the denotation of a `control channel'+handler (InV v) k = k v+handler (InFX ka a) k = InFX (\v -> handler (ka v) k) a+++-- | Expressions and their interpretations+-- This is an open data type and an open function. Haskell typeclasses+-- are ideal for that.+--+-- This is the function \curlyM of EDLS+class Interpretor exp where+    interpret ::  exp -> Env Value -> Comp++-- | The base language has only two expressions: omega and error+-- See Fig. 3 (p. 7) of EDLS+--+data BE_err   = BE_err+data BE_omega = BE_omega++instance Interpretor BE_omega where+    interpret _ _ = InV undefined++instance Interpretor BE_err where+    interpret _ _  = raise "error action"++-- | The meaning of a program+prog p = interpret p empty_env+++-- ----------------------------------------------------------------------+-- | Extension: Call-by-Value: see a part Fig. 4 of EDLS (or, Fig. 8)+--+-- We add closures (procedures) to the Base+type Proc = Value -> Comp++class PV u where                        -- and the corresponding injection/+  inP :: Proc -> u                      -- projection functions+  prP :: u -> Maybe (Proc)+++type Var = V+data Lam e = Lam V e+data App e1 e2 = e1 :@ e2+infixl 1 :@++instance Interpretor V where+    interpret v env = InV (env v)++instance Interpretor e => Interpretor (Lam e) where+    interpret (Lam x e) env = InV (inP (\d -> interpret e (ext_env env x d)))++instance (Interpretor e1, Interpretor e2) => Interpretor (App e1 e2) where+    interpret (e1 :@ e2) env =+        handler (interpret e1 env) $+                \f -> handler (interpret e2 env) $+                      \a -> maybe (raise "InP expected") (\g -> g a)+                                  (prP f)+++-- | Create a few variables for use in examples+vx, vy, vr, vf :: Var+(vx,vy,vr,vf) = (V "x", V "y", V "r", V "f")++-- Test of the extension+-- Instantiate this extension on the top of the base language+--+-- | Denotations of the new actions (inj/proj to/from the Universal Domain)+tagProc  = "Proc"+tagCompV = "CompV"+tagCompE = "CompE"++-- | inject and project computations+inComp :: Comp -> Value+inComp (InV v) = VT tagCompV v+inComp (InFX k a) = VT tagCompE (VP (VF (inComp . k)) a)++prComp :: Value -> Maybe Comp+prComp (VT tag v) | tag == tagCompV = Just (InV v)+prComp (VT tag v) | tag == tagCompE = pr v+   where pr (VP (VF k) a) = Just $ InFX (fromJust . prComp . k) a+         pr _ = Nothing+prComp _ = Nothing+++instance PV Value where+    inP f = VT tagProc (VF (inComp . f))+    prP (VT tag (VF k)) | tag == tagProc = Just $ fromJust . prComp . k+    prP _ = Nothing++test1 = Lam vx (vx :@ BE_err)++test1e = prog test1+-- {"Proc" <procedure>}+++------------------------------------------------------------------------+-- | Extension: Arithmetic: see a part Fig. 4 of EDLS +--+class PN u where                        -- inj/proj for numbers+  inN :: Int -> u+  prN :: u -> Maybe Int++data IntC = IntC Int                    -- an integer constant+data Add1 = Add1++instance Interpretor IntC where+    interpret (IntC v) _ = InV (inN v)++instance Interpretor Add1 where+    interpret Add1 _ = InV (inP $+                               \v -> maybe (raise "InN expected")+                                     (InV . inN . succ)+                                     (prN v))+++add1 x = Add1 :@ x++-- | Test of the extension+-- Instantiate this extension on the top of the CBV evaluator+--+instance PN Value where+    inN n = VI n+    prN (VI n) = Just n+    prN _ = Nothing+++test2 = (Lam vx $ add1 vx) :@ (IntC 1)+test2e = prog test2+-- 2++------------------------------------------------------------------------+-- | Extension: State: see Fig. 5 of EDLS +--+newtype Loc = Loc Int deriving (Eq, Show) -- locations++class PL u where+  inL :: Loc -> u+  prL :: u -> Maybe Loc++-- | a better idea is Loc -> Maybe Value, so that when lookup fails,+-- we can re-throw that Deref or Set message. That would make the+-- storage extensible...+-- The first component of the pair is the allocation counter+type Sto = (Int, Loc -> Value) ++tagSto = "Storage"++inSto :: Sto -> Value+inSto (cnt, st) = VT tagSto (VP (VI cnt) (VF (st . fromJust . prL)))+prSto :: Value -> Maybe Sto+prSto (VT tag (VP (VI cnt) (VF k))) | tag == tagSto = Just (cnt, k . inL)+prSto _ = Nothing++init_sto :: Sto+init_sto  = (0,\l->undefined)+++-- data StoAct v = InRef v | InDer Loc | InSet Loc v++-- | new expressions+data Ref e = Ref e+data Deref e = Deref e+data Set e1 e2 = Set e1 e2++-- | Denotations of the new actions (inj/proj to/from the Universal Domain)+tagInRef = "Ref"+tagInDer = "Deref"+tagInSet = "Set"++inRef v = VT tagInRef v+prRef (VT tag v) | tag == tagInRef = Just v+prRef _ = Nothing++inDer v = VT tagInDer (inL v)+prDer (VT tag v) | tag == tagInDer = prL v+prDer _ = Nothing++inSet l v = VT tagInSet (VP (inL l) v)+prSet (VT tag (VP l v)) | tag == tagInSet = fmap (\l -> (l,v)) (prL l)+prSet _ = Nothing++++instance Interpretor e => Interpretor (Ref e) where+    interpret (Ref e) env = handler (interpret e env) $+                              \v -> inAC(inRef v)+++instance Interpretor e => Interpretor (Deref e) where+    interpret (Deref e) env = handler (interpret e env) $+                              \v -> maybe (raise "InL expected")+                                    (inAC . inDer)+                                    (prL v)++instance (Interpretor e1, Interpretor e2) => Interpretor (Set e1 e2) where+    interpret (Set e1 e2) env = handler (interpret e1 env) $+                              \l -> handler (interpret e2 env) $+                                 \v -> maybe (raise "InL expected")+                                             (\l -> inAC (inSet l v))+                                             (prL l)+++-- | Now we need a storage admin+-- It is treated as an expression in the source language!+--+data StoAdmin e = StoAdmin Sto e++instance Interpretor e => Interpretor (StoAdmin e) where+    interpret (StoAdmin sto e) env = sto_handler sto (interpret e env) InV+++sto_handler (cnt,st) (InFX k a) f | Just v <- prRef a = +   let l = Loc cnt+       sto = (cnt+1, \l' -> if l' == l then v else st l')+   in sto_handler sto (k (inL l)) f+sto_handler sto@(cnt,st) (InFX k a) f | Just l <- prDer a = +   sto_handler sto (k (st l)) f+sto_handler (cnt,st) (InFX k a) f | Just (l,v) <- prSet a = +   sto_handler (cnt, \l' -> if l' == l then v else st l') (k (inL l)) f++sto_handler sto (InV v) f = f (VP v (inSto sto)) -- normal return+-- Propagate everything else+sto_handler sto (InFX k a) f = InFX (\v -> sto_handler sto (k v) f) a++                                       +tagLoc = "Loc"++instance PL Value where+    inL (Loc l) = VT tagLoc (VI l)+    prL (VT tag (VI l)) | tag == tagLoc = Just (Loc l)+    prL _ = Nothing+++-- Test of the extension+-- Note that we can use several local storages!+++test3 = (Lam vr $ Lam vf $ vf :@ (Deref vr)) :@+          (Ref (IntC 1)) :@ (Lam vx $ add1 vx)++-- we forgot the Admin..., so the program terminates with an effect+test31 = prog test3 +-- Effect: {"Ref" 1}++test32 = prog (StoAdmin init_sto test3)+-- (2,{"Storage" (1,<procedure>)})++test33 = prog (StoAdmin init_sto +               ((Lam vr $ (Lam (V "_") (Deref vr)) :@ (Deref (Set vr (IntC 2))))+                :@ (Ref (IntC 1))))+-- (2,{"Storage" (1,<procedure>)})++------------------------------------------------------------------------+-- Extension: Delimited continuation+-- That is new compared to EDLS++-- new effect message: Control ((Value->Comp)->Comp)+tagControl = "Control"++inControl :: (Value->Comp) -> Value+inControl f = VT tagControl (VF (inComp . f))+prControl :: Value -> Maybe (Value->Comp)+prControl (VT tag (VF f)) | tag == tagControl = Just (fromJust . prComp . f)+prControl _ = Nothing+++data Control e = Control e++instance Interpretor e => Interpretor (Control e) where+    interpret (Control e) env = handler (interpret e env) $+                      \a -> maybe (raise "InP expected")+                                  (\f -> inAC(inControl f))+                                  (prP a)++-- The administrator here is prompt, quite unsurprisingly++data ControlAdmin e = ControlAdmin e++instance Interpretor e => Interpretor (ControlAdmin e) where+    interpret (ControlAdmin e) env = ctl_handler (interpret e env) InV+++ctl_handler (InFX k a) f | Just e <- prControl a = +   ctl_handler (e (inP k)) f++ctl_handler (InV v) f = f v -- normal return+-- Propagate everything else+ctl_handler (InFX k a) f = InFX (\v -> ctl_handler (k v) f) a++-- Ken's tests++control v e = Control (Lam (V v) e)+prompt e = ControlAdmin e+succ0 = (add1 (IntC 0))++-- if we forget Reset...+test41 = prog $ add1 (Control (Lam vf succ0))+-- Effect: {"Control" <procedure>}++test42 = prog $ prompt (add1 (control "f" succ0))+-- 1++test43 = prog $ prompt (add1 (control "f" (vf :@ succ0)))+--2++test44 = prog $ prompt (add1 (add1 (control "f" (vf :@ succ0))))+-- 3++test45 = prog $ prompt (add1 (add1 (control "f" +                                    (vf :@ (vf :@ succ0)))))+-- 5++test46 = prog $ prompt (add1 ((Lam vx (add1 vx)) :@+                              (control "f" (vf :@ (vf :@ succ0)))))++-- 5+test47 = prog $ prompt (add1 ((Lam vx (control "f" (IntC 0))) :@+                              (control "f" (vf :@ (vf :@ succ0)))))+-- 0++test48 = prog $ add1 (prompt ((Lam vx (control "f" (IntC 0))) :@+                              (control "f" (vf :@ (vf :@ succ0)))))+-- 1
+ Language/Symantics1.hs view
@@ -0,0 +1,216 @@+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE Rank2Types, GeneralizedNewtypeDeriving #-}+{-# LANGUAGE NoMonomorphismRestriction, EmptyDataDecls  #-}++-- This is the Haskell version of symantics1.ml, for comparison+-- ACG with a more expressive semantic lexicon that includes+-- multi-prompt delimited continuations and the notion of evaluation.+-- Types are considered as a mere approximation rather than+-- the complete specification of grammatical composition.+--+-- * <http://okmij.org/ftp/gengo/index.html#CAG>+--++module Language.Symantics1 where++-- Part of the Dybvig, Sabry, Peyton-Jones' library+-- for multi-prompt delimited control+import CC_Frame -- ed. I don't know where this is.+import Control.Monad.Reader++-- The abstract form, to be interpreted in several ways.++-- | Abstract signature, which defines base types, constants and their types+--+data N                                  -- Base types+data NP+data S+data SM++-- | An interpretation of the base type btyp in the signature+-- labeled by lab+type family I lab btyp ++class Abstract c where+  john :: c (I c NP)                    -- constants+  bill :: c (I c NP)++  man   :: c (I c N)+  woman :: c (I c N)+  see   :: c (I c NP) -> c (I c NP) -> c (I c S)+  love  :: c (I c NP) -> c (I c NP) -> c (I c S)++  every :: c (I c N) -> c (I c NP)+  some  :: c (I c N) -> c (I c NP)++  dot   :: c (I c S) -> c (I c SM)      -- Terminating dot++{-+  everyone :: c (I c NP)+  someone  :: c (I c NP)++-}+++-- Sample phrases in the abstract language++-- term1 = see someone everyone++-- | Example from Sec 4.3 of the ESSLLI Advanced ACG course.+term43 = dot (love (some woman) (every man))+++-- | An interpretation of the abstract signature as the surface form: strings+--+newtype LString a = LString a deriving Show++-- All base type are interpreted as strings+type instance I LString N  = String+type instance I LString NP = String+type instance I LString S  = String+type instance I LString SM = String++ccat :: LString String -> LString String -> LString String+ccat (LString a) (LString b) = LString (a ++ b)++instance Abstract LString where+  john  = LString "John"+  bill  = LString "Bill"+  man   = LString "man"+  woman = LString "woman"++  every = \x -> LString "every " `ccat` x+  some  = \x -> LString "some " `ccat` x+  see   = \o s -> s `ccat` LString " saw " `ccat` o+  love  = \o s -> s `ccat` LString " loves " `ccat` o++  dot   = \s -> s `ccat` LString "."+++-- Surface forms of sample terms+term43S = case term43 of LString x -> x++-- ------------------------------------------------------------------------+-- | Semantic forms+--+data E = Ind String deriving Show+data T = Man E+       | Woman E+       | See E E+       | Love E E+       | And T T+       | Imply T T+       | Exists Varname T+       | Forall Varname T+         deriving Show+type Varname = String+++-- We now build the semantic signature and the lexicon -- stepwise++-- | The order of quantification+data QuantOrder = Uni_over_Exi | Exi_over_Uni++data SemEnv r = +    SemEnv{puni :: Prompt r T,+           pexi :: Prompt r T,+           quant_order :: QuantOrder,+           pcnt :: Prompt r (Int -> CC r T)     -- to generate variable names+          }++-- | The Semantic monad+newtype SemM r a = SemM (ReaderT (SemEnv r) (CC r) a)+  deriving Monad++unSem :: SemM r a -> SemEnv r -> CC r a+unSem (SemM m) env = runReaderT m env++-- | Interpretation of Basic types+type instance I (SemM r) NP = E+type instance I (SemM r) N  = E -> T+type instance I (SemM r) S  = T+type instance I (SemM r) SM = T++instance Abstract (SemM r) where+    john = return $ Ind "John'"+    bill = return $ Ind "Bill'"+    man  = return Man+    woman= return Woman+    love  = \o s -> (return Love) `ap` o `ap` s+    see   = \o s -> (return See)  `ap` o `ap` s++    every pred = pred >>= \pr -> +     make_ind_quant puni (\vn x -> +          return $ Forall vn $ Imply (pr (Ind vn)) x)+    some pred = pred >>= \pr -> +     make_ind_quant pexi (\vn x -> +          return $ Exists vn $ And (pr (Ind vn)) x)++    dot m = SemM $ do+            env <- ask+            lift $ do+             case quant_order env of+              Uni_over_Exi -> +                 pushPrompt (puni env) $+                   pushPrompt (pexi env) (unSem m env)+              Exi_over_Uni -> +                 pushPrompt (pexi env) $+                   pushPrompt (puni env) (unSem m env)++runSem :: QuantOrder -> (forall r. SemM r T) -> T+runSem qorder m = runCC init+ where+ init =  do+   uni <- newPrompt+   exi <- newPrompt+   cnt <- newPrompt+   -- initialize to 0 the counter to create variable names+   pushPrompt cnt (do+    v <- unSem m (SemEnv{puni=uni, pexi=exi, quant_order=qorder, pcnt=cnt})+    return $ const (return v)) `app` (return 0)++-- | /Movement/ into the position of the prompt selected by psel+make_ind_quant psel body = do+  vn <- genvar+  let v = Ind vn+  SemM $ do+   env <- ask+   lift $ shiftP (psel env) $ \sk -> +      body vn =<< sk (Ind vn)++-- | Logical forms of sample terms in different semantic environment+term43L1 = runSem Uni_over_Exi term43+{-+  Forall "v1" (Imply (Man (Ind "v1")) +     (Exists "v0" (And (Woman (Ind "v0")) +        (Love (Ind "v0") (Ind "v1")))))+-}++term43L2 = runSem Exi_over_Uni term43+{-+  Exists "v0" (And (Woman (Ind "v0")) +    (Forall "v1" (Imply (Man (Ind "v1")) +       (Love (Ind "v0") (Ind "v1")))))+-}+++-- | Auxiliary functions+--+app :: Monad m => m (a -> m b) -> m a -> m b+app m1 m2 = (m1 `ap` m2) >>= id++-- | Generate a new variable name+genvar :: SemM r Varname+genvar = SemM $ do+  env <- ask+  cnt <- lift $ shiftP (pcnt env) $ \sk ->+           return $ \cnt -> sk cnt `app` (return (succ cnt))+  return $ "v" ++ show cnt+++shiftP :: Prompt r b -> ((a -> CC r b) -> CC r b) -> CC r a+shiftP p f = letSubCont p $ \sk -> +               pushPrompt p (f (\v -> +                 pushPrompt p (pushSubCont sk (return v))))++
liboleg.cabal view
@@ -1,5 +1,5 @@ name:           liboleg-version:        2009.9.1+version:        2010.1.1 license:        BSD3 license-file:   LICENSE author:         Oleg Kiselyov@@ -28,6 +28,7 @@             Control.CaughtMonadIO             Control.ShiftResetGenuine             Control.VarStateM+            Control.ExtensibleDS              Codec.Image.Tiff