msyds/gf-core
1
0
Fork 0
forked from GitHub/gf-core
Code Pull Requests Activity

the exhaustive/random generator now knows how to handle computable functions in the types

Browse Source
This commit is contained in:
krasimir
2010-10-11 17:18:28 +00:00
parent 3ac637ddcb
commit de0354f991
5 changed files with 248 additions and 210 deletions
Download Patch File Download Diff File Expand all files Collapse all files

12
src/runtime/haskell/PGF/Forest.hs
View File

@@ -133,9 +133,9 @@ getAbsTrees (Forest abs cnc forest root) arg@(PArg _ fid) ty =
case isLindefCId fn of case isLindefCId fn of
Just _ -> do arg <- go (Set.insert fid rec_) scope (head args) mb_tty Just _ -> do arg <- go (Set.insert fid rec_) scope (head args) mb_tty
return (mkAbs arg) return (mkAbs arg)
Nothing -> do tty_fn <- runTcM abs fid (lookupFunType fn) Nothing -> do ty_fn <- runTcM abs fid (lookupFunType fn)
(e,tty0) <- foldM (\(e1,tty) arg -> goArg (Set.insert fid rec_) scope fid e1 arg tty) (e,tty0) <- foldM (\(e1,tty) arg -> goArg (Set.insert fid rec_) scope fid e1 arg tty)
(EFun fn,tty_fn) args (EFun fn,TTyp [] ty_fn) args
case mb_tty of case mb_tty of
Just tty -> runTcM abs fid $ do Just tty -> runTcM abs fid $ do
i <- newGuardedMeta e i <- newGuardedMeta e
@@ -183,7 +183,7 @@ getAbsTrees (Forest abs cnc forest root) arg@(PArg _ fid) ty =
| otherwise = [x | PConst _ (EFun x) _ <- maybe [] Set.toList (IntMap.lookup fid forest)] | otherwise = [x | PConst _ (EFun x) _ <- maybe [] Set.toList (IntMap.lookup fid forest)]
newtype TcFM a = TcFM {unTcFM :: MetaStore -> ([(MetaStore,a)],[(FId,TcError)])} newtype TcFM a = TcFM {unTcFM :: MetaStore () -> ([(MetaStore (),a)],[(FId,TcError)])}
instance Functor TcFM where instance Functor TcFM where
fmap f g = TcFM (\ms -> let (res_g,err_g) = unTcFM g ms fmap f g = TcFM (\ms -> let (res_g,err_g) = unTcFM g ms
@@ -201,9 +201,9 @@ instance MonadPlus TcFM where
(res_g,err_g) = unTcFM g ms (res_g,err_g) = unTcFM g ms
in (res_f++res_g,err_f++err_g)) in (res_f++res_g,err_f++err_g))
runTcM :: Abstr -> FId -> TcM a -> TcFM a runTcM :: Abstr -> FId -> TcM () a -> TcFM a
runTcM abstr fid f = TcFM (\ms -> case unTcM f abstr ms of runTcM abstr fid f = TcFM (\ms -> case unTcM f abstr () ms of
Ok ms x -> ([(ms,x)],[] ) Ok _ ms x -> ([(ms,x)],[] )
Fail err -> ([], [(fid,err)])) Fail err -> ([], [(fid,err)]))
foldForest :: (FunId -> [PArg] -> b -> b) -> (Expr -> [String] -> b -> b) -> b -> FId -> IntMap.IntMap (Set.Set Production) -> b foldForest :: (FunId -> [PArg] -> b -> b) -> (Expr -> [String] -> b -> b) -> b -> FId -> IntMap.IntMap (Set.Set Production) -> b

119
src/runtime/haskell/PGF/Generate.hs
View File

@@ -67,41 +67,52 @@ generateRandomFromDepth g pgf e dp =
generate :: Selector sel => sel -> PGF -> Type -> Maybe Int -> [Expr] generate :: Selector sel => sel -> PGF -> Type -> Maybe Int -> [Expr]
generate sel pgf ty dp = generate sel pgf ty dp =
[value2expr (funs (abstract pgf),lookupMeta ms) 0 v | [value2expr (funs (abstract pgf),lookupMeta ms) 0 v |
(ms,v) <- runGenM (prove (abstract pgf) emptyScope (TTyp [] ty) dp) sel emptyMetaStore] (ms,v) <- runGenM (abstract pgf) (prove emptyScope (TTyp [] ty) dp) sel emptyMetaStore]
generateForMetas :: Selector sel => sel -> PGF -> Expr -> Maybe Int -> [Expr] generateForMetas :: Selector sel => sel -> PGF -> Expr -> Maybe Int -> [Expr]
generateForMetas sel pgf e dp = generateForMetas sel pgf e dp =
case unTcM (infExpr emptyScope e) abs emptyMetaStore of case unTcM (infExpr emptyScope e) abs sel emptyMetaStore of
Ok ms (e,_) -> let gen = do fillinVariables (runTcM abs) $ \scope tty -> do Ok sel ms (e,_) -> let gen = do fillinVariables $ \scope tty -> do
v <- prove abs scope tty dp v <- prove scope tty dp
return (value2expr (funs abs,lookupMeta ms) 0 v) return (value2expr (funs abs,lookupMeta ms) 0 v)
runTcM abs (refineExpr e) refineExpr e
in [e | (ms,e) <- runGenM gen sel ms] in [e | (ms,e) <- runGenM abs gen sel ms]
Fail _ -> [] Fail _ -> []
where where
abs = abstract pgf abs = abstract pgf
prove :: Selector sel => Abstr -> Scope -> TType -> Maybe Int -> GenM sel MetaStore Value prove :: Selector sel => Scope -> TType -> Maybe Int -> TcM sel Value
prove abs scope tty@(TTyp env (DTyp [] cat es)) dp = do prove scope (TTyp env1 (DTyp [] cat es1)) dp = do
(fn,DTyp hypos cat es) <- clauses cat (fn,DTyp hypos _ es2) <- clauses cat
case dp of case dp of
Just 0 | not (null hypos) -> mzero Just 0 | not (null hypos) -> mzero
_ -> return () _ -> return ()
(env,args) <- mkEnv [] hypos (env2,args) <- mkEnv [] hypos
runTcM abs (eqType scope (scopeSize scope) 0 (TTyp env (DTyp [] cat es)) tty) vs1 <- mapM (PGF.TypeCheck.eval env1) es1
vs2 <- mapM (PGF.TypeCheck.eval env2) es2
sequence_ [eqValue mzero suspend (scopeSize scope) v1 v2 | (v1,v2) <- zip vs1 vs2]
vs <- mapM descend args vs <- mapM descend args
return (VApp fn vs) return (VApp fn vs)
where where
clauses cat = suspend i c = do
do fn <- select abs cat mv <- getMeta i
case Map.lookup fn (funs abs) of case mv of
Just (ty,_,_,_) -> return (fn,ty) MBound e -> c e
Nothing -> mzero MUnbound scope tty cs -> do v <- prove scope tty dp
e <- TcM (\abs sel ms -> Ok sel ms (value2expr (funs abs,lookupMeta ms) 0 v))
setMeta i (MBound e)
sequence_ [c e | c <- (c:cs)]
clauses cat = do
fn <- select cat
if fn == mkCId "plus" then mzero else return ()
ty <- lookupFunType fn
return (fn,ty)
mkEnv env [] = return (env,[]) mkEnv env [] = return (env,[])
mkEnv env ((bt,x,ty):hypos) = do mkEnv env ((bt,x,ty):hypos) = do
(env,arg) <- if x /= wildCId (env,arg) <- if x /= wildCId
then do i <- runTcM abs (newMeta scope (TTyp env ty)) then do i <- newMeta scope (TTyp env ty)
let v = VMeta i env [] let v = VMeta i env []
return (v : env,Right v) return (v : env,Right v)
else return (env,Left (TTyp env ty)) else return (env,Left (TTyp env ty))
@@ -111,7 +122,7 @@ prove abs scope tty@(TTyp env (DTyp [] cat es)) dp = do
descend (bt,arg) = do let dp' = fmap (flip (-) 1) dp descend (bt,arg) = do let dp' = fmap (flip (-) 1) dp
v <- case arg of v <- case arg of
Right v -> return v Right v -> return v
Left tty -> prove abs scope tty dp' Left tty -> prove scope tty dp'
v <- case bt of v <- case bt of
Implicit -> return (VImplArg v) Implicit -> return (VImplArg v)
Explicit -> return v Explicit -> return v
@@ -121,75 +132,15 @@ prove abs scope tty@(TTyp env (DTyp [] cat es)) dp = do
------------------------------------------------------------------------------ ------------------------------------------------------------------------------
-- Generation Monad -- Generation Monad
newtype GenM sel s a = GenM {unGen :: sel -> s -> Choice sel s a}
data Choice sel s a = COk sel s a
| CFail
| CBranch (Choice sel s a) (Choice sel s a)
instance Monad (GenM sel s) where runGenM :: Abstr -> TcM s a -> s -> MetaStore s -> [(MetaStore s,a)]
return x = GenM (\sel s -> COk sel s x) runGenM abs f s ms = toList (unTcM f abs s ms) []
f >>= g = GenM (\sel s -> iter (unGen f sel s))
where where
iter (COk sel s x) = unGen (g x) sel s toList (Ok s ms x) xs = (ms,x) : xs
iter (CBranch b1 b2) = CBranch (iter b1) (iter b2) toList (Fail _) xs = xs
iter CFail = CFail toList (Zero) xs = xs
fail _ = GenM (\sel s -> CFail) toList (Plus b1 b2) xs = toList b1 (toList b2 xs)
instance Selector sel => MonadPlus (GenM sel s) where
mzero = GenM (\sel s -> CFail)
mplus f g = GenM (\sel s -> let (sel1,sel2) = splitSelector sel
in CBranch (unGen f sel1 s) (unGen g sel2 s))
runGenM :: GenM sel s a -> sel -> s -> [(s,a)]
runGenM f sel s = toList (unGen f sel s) []
where
toList (COk sel s x) xs = (s,x) : xs
toList (CFail) xs = xs
toList (CBranch b1 b2) xs = toList b1 (toList b2 xs)
runTcM :: Abstr -> TcM a -> GenM sel MetaStore a
runTcM abs f = GenM (\sel ms ->
case unTcM f abs ms of
Ok ms a -> COk sel ms a
Fail _ -> CFail)
------------------------------------------------------------------------------
-- Selectors
class Selector sel where
splitSelector :: sel -> (sel,sel)
select :: Abstr -> CId -> GenM sel s CId
instance Selector () where
splitSelector sel = (sel,sel)
select abs cat = GenM (\sel s -> case Map.lookup cat (cats abs) of
Just (_,fns) -> iter s fns
Nothing -> CFail)
where
iter s [] = CFail
iter s ((_,fn):fns) = CBranch (COk () s fn) (iter s fns)
instance RandomGen g => Selector (Identity g) where
splitSelector (Identity g) = let (g1,g2) = split g
in (Identity g1, Identity g2)
select abs cat = GenM (\(Identity g) s ->
case Map.lookup cat (cats abs) of
Just (_,fns) -> do_rand g s 1.0 fns
Nothing -> CFail)
where
do_rand g s p [] = CFail
do_rand g s p fns = let (d,g') = randomR (0.0,p) g
(g1,g2) = split g'
(p',fn,fns') = hit d fns
in CBranch (COk (Identity g1) s fn) (do_rand g2 s (p-p') fns')
hit :: Double -> [(Double,a)] -> (Double,a,[(Double,a)])
hit d (px@(p,x):xs)
| d < p = (p,x,xs)
| otherwise = let (p',x',xs') = hit (d-p) xs
in (p,x',px:xs')
-- Helper function for random generation. After every -- Helper function for random generation. After every
-- success we must restart the search to find sufficiently different solution. -- success we must restart the search to find sufficiently different solution.

259
src/runtime/haskell/PGF/TypeCheck.hs
View File

@@ -18,10 +18,10 @@ module PGF.TypeCheck ( checkType, checkExpr, inferExpr
, ppTcError, TcError(..) , ppTcError, TcError(..)
-- internals needed for the typechecking of forests -- internals needed for the typechecking of forests
, MetaStore, emptyMetaStore, newMeta, newGuardedMeta, fillinVariables , MetaStore, emptyMetaStore, newMeta, newGuardedMeta, fillinVariables, getMeta, setMeta, MetaValue(..)
, Scope, emptyScope, scopeSize, scopeEnv, addScopedVar , Scope, emptyScope, scopeSize, scopeEnv, addScopedVar
, TcM(..), TcResult(..), TType(..), tcError , TcM(..), TcResult(..), TType(..), Selector(..), tcError
, tcExpr, infExpr, eqType , tcExpr, infExpr, eqType, eqValue
, lookupFunType, eval , lookupFunType, eval
, refineExpr, checkResolvedMetaStore, lookupMeta , refineExpr, checkResolvedMetaStore, lookupMeta
) where ) where
@@ -37,7 +37,9 @@ import Data.IntMap as IntMap
import Data.Maybe as Maybe import Data.Maybe as Maybe
import Data.List as List import Data.List as List
import Control.Monad import Control.Monad
import Control.Monad.Identity
import Text.PrettyPrint import Text.PrettyPrint
import System.Random as Random
----------------------------------------------------- -----------------------------------------------------
-- The Scope -- The Scope
@@ -73,55 +75,69 @@ scopeSize (Scope gamma) = length gamma
-- The Monad -- The Monad
----------------------------------------------------- -----------------------------------------------------
type MetaStore = IntMap MetaValue type MetaStore s = IntMap (MetaValue s)
data MetaValue data MetaValue s
= MUnbound Scope TType [Expr -> TcM ()] = MUnbound Scope TType [Expr -> TcM s ()]
| MBound Expr | MBound Expr
| MGuarded Expr [Expr -> TcM ()] {-# UNPACK #-} !Int -- the Int is the number of constraints that have to be solved | MGuarded Expr [Expr -> TcM s ()] {-# UNPACK #-} !Int -- the Int is the number of constraints that have to be solved
-- to unlock this meta variable -- to unlock this meta variable
newtype TcM a = TcM {unTcM :: Abstr -> MetaStore -> TcResult a} newtype TcM s a = TcM {unTcM :: Abstr -> s -> MetaStore s -> TcResult s a}
data TcResult a data TcResult s a
= Ok MetaStore a = Ok s (MetaStore s) a
| Fail TcError | Fail TcError
| Zero
| Plus (TcResult s a) (TcResult s a)
instance Monad TcM where instance Monad (TcM s) where
return x = TcM (\abstr ms -> Ok ms x) return x = TcM (\abstr s ms -> Ok s ms x)
f >>= g = TcM (\abstr ms -> case unTcM f abstr ms of f >>= g = TcM (\abstr s ms -> iter abstr (unTcM f abstr s ms))
Ok ms x -> unTcM (g x) abstr ms where
Fail e -> Fail e) iter abstr (Ok s ms x) = unTcM (g x) abstr s ms
iter abstr (Fail e) = Fail e
iter abstr Zero = Zero
iter abstr (Plus b1 b2) = Plus (iter abstr b1) (iter abstr b2)
instance Functor TcM where instance Selector s => MonadPlus (TcM s) where
fmap f x = TcM (\abstr ms -> case unTcM x abstr ms of mzero = TcM (\abstr s ms -> Zero)
Ok ms x -> Ok ms (f x) mplus f g = TcM (\abstr s ms -> let (s1,s2) = splitSelector s
Fail e -> Fail e) in Plus (unTcM f abstr s1 ms) (unTcM g abstr s2 ms))
lookupCatHyps :: CId -> TcM [Hypo] instance Functor (TcM s) where
lookupCatHyps cat = TcM (\abstr ms -> case Map.lookup cat (cats abstr) of fmap f x = TcM (\abstr s ms -> iter (unTcM x abstr s ms))
Just (hyps,_) -> Ok ms hyps where
iter (Ok s ms x) = Ok s ms (f x)
iter (Fail e) = Fail e
iter Zero = Zero
iter (Plus b1 b2) = Plus (iter b1) (iter b2)
lookupCatHyps :: CId -> TcM s [Hypo]
lookupCatHyps cat = TcM (\abstr s ms -> case Map.lookup cat (cats abstr) of
Just (hyps,_) -> Ok s ms hyps
Nothing -> Fail (UnknownCat cat)) Nothing -> Fail (UnknownCat cat))
lookupFunType :: CId -> TcM TType lookupFunType :: CId -> TcM s Type
lookupFunType fun = TcM (\abstr ms -> case Map.lookup fun (funs abstr) of lookupFunType fun = TcM (\abstr s ms -> case Map.lookup fun (funs abstr) of
Just (ty,_,_,_) -> Ok ms (TTyp [] ty) Just (ty,_,_,_) -> Ok s ms ty
Nothing -> Fail (UnknownFun fun)) Nothing -> Fail (UnknownFun fun))
emptyMetaStore :: MetaStore emptyMetaStore :: MetaStore s
emptyMetaStore = IntMap.empty emptyMetaStore = IntMap.empty
newMeta :: Scope -> TType -> TcM MetaId newMeta :: Scope -> TType -> TcM s MetaId
newMeta scope tty = TcM (\abstr ms -> let metaid = IntMap.size ms + 1 newMeta scope tty = TcM (\abstr s ms -> let metaid = IntMap.size ms + 1
in Ok (IntMap.insert metaid (MUnbound scope tty []) ms) metaid) in Ok s (IntMap.insert metaid (MUnbound scope tty []) ms) metaid)
newGuardedMeta :: Expr -> TcM MetaId newGuardedMeta :: Expr -> TcM s MetaId
newGuardedMeta e = TcM (\abstr ms -> let metaid = IntMap.size ms + 1 newGuardedMeta e = TcM (\abstr s ms -> let metaid = IntMap.size ms + 1
in Ok (IntMap.insert metaid (MGuarded e [] 0) ms) metaid) in Ok s (IntMap.insert metaid (MGuarded e [] 0) ms) metaid)
getMeta :: MetaId -> TcM MetaValue getMeta :: MetaId -> TcM s (MetaValue s)
getMeta i = TcM (\abstr ms -> Ok ms $! case IntMap.lookup i ms of getMeta i = TcM (\abstr s ms -> Ok s ms $! case IntMap.lookup i ms of
Just mv -> mv) Just mv -> mv)
setMeta :: MetaId -> MetaValue -> TcM ()
setMeta i mv = TcM (\abstr ms -> Ok (IntMap.insert i mv ms) ()) setMeta :: MetaId -> MetaValue s -> TcM s ()
setMeta i mv = TcM (\abstr s ms -> Ok s (IntMap.insert i mv ms) ())
lookupMeta ms i = lookupMeta ms i =
case IntMap.lookup i ms of case IntMap.lookup i ms of
@@ -131,35 +147,35 @@ lookupMeta ms i =
Just (MUnbound _ _ _) -> Nothing Just (MUnbound _ _ _) -> Nothing
Nothing -> Nothing Nothing -> Nothing
fillinVariables :: Monad m => (forall a . TcM a -> m a) -> (Scope -> TType -> m Expr) -> m () fillinVariables :: (Scope -> TType -> TcM s Expr) -> TcM s ()
fillinVariables runTcM f = do fillinVariables f = do
fvs <- runTcM (TcM (\abstr ms -> Ok ms [(i,scope,tty,cs) | (i,MUnbound scope tty cs) <- IntMap.toList ms])) fvs <- TcM (\abstr s ms -> Ok s ms [(i,scope,tty,cs) | (i,MUnbound scope tty cs) <- IntMap.toList ms])
case fvs of case fvs of
[] -> return () [] -> return ()
(i,scope,tty,cs):_ -> do e <- f scope tty (i,scope,tty,cs):_ -> do e <- f scope tty
runTcM $ do setMeta i (MBound e) setMeta i (MBound e)
sequence_ [c e | c <- cs] sequence_ [c e | c <- cs]
fillinVariables runTcM f fillinVariables f
tcError :: TcError -> TcM a tcError :: TcError -> TcM s a
tcError e = TcM (\abstr ms -> Fail e) tcError e = TcM (\abstr s ms -> Fail e)
addConstraint :: MetaId -> MetaId -> Env -> [Value] -> (Value -> TcM ()) -> TcM () addConstraint :: MetaId -> MetaId -> (Expr -> TcM s ()) -> TcM s ()
addConstraint i j env vs c = do addConstraint i j c = do
mv <- getMeta j mv <- getMeta j
case mv of case mv of
MUnbound scope tty cs -> addRef >> setMeta j (MUnbound scope tty ((\e -> release >> apply env e vs >>= c) : cs)) MUnbound scope tty cs -> addRef >> setMeta j (MUnbound scope tty ((\e -> release >> c e) : cs))
MBound e -> apply env e vs >>= c MBound e -> c e
MGuarded e cs x | x == 0 -> apply env e vs >>= c MGuarded e cs x | x == 0 -> c e
| otherwise -> addRef >> setMeta j (MGuarded e ((\e -> release >> apply env e vs >>= c) : cs) x) | otherwise -> addRef >> setMeta j (MGuarded e ((\e -> release >> c e) : cs) x)
where where
addRef = TcM (\abstr ms -> case IntMap.lookup i ms of addRef = TcM (\abstr s ms -> case IntMap.lookup i ms of
Just (MGuarded e cs x) -> Ok (IntMap.insert i (MGuarded e cs (x+1)) ms) ()) Just (MGuarded e cs x) -> Ok s (IntMap.insert i (MGuarded e cs (x+1)) ms) ())
release = TcM (\abstr ms -> case IntMap.lookup i ms of release = TcM (\abstr s ms -> case IntMap.lookup i ms of
Just (MGuarded e cs x) -> if x == 1 Just (MGuarded e cs x) -> if x == 1
then unTcM (sequence_ [c e | c <- cs]) abstr (IntMap.insert i (MGuarded e [] 0) ms) then unTcM (sequence_ [c e | c <- cs]) abstr s (IntMap.insert i (MGuarded e [] 0) ms)
else Ok (IntMap.insert i (MGuarded e cs (x-1)) ms) ()) else Ok s (IntMap.insert i (MGuarded e cs (x-1)) ms) ())
----------------------------------------------------- -----------------------------------------------------
-- Type errors -- Type errors
@@ -205,6 +221,43 @@ ppTcError (UnexpectedImplArg xs e) = braces (ppExpr 0 xs e) <+> text "is imp
ppTcError (UnsolvableGoal xs metaid ty)= text "The goal:" <+> ppMeta metaid <+> colon <+> ppType 0 xs ty $$ ppTcError (UnsolvableGoal xs metaid ty)= text "The goal:" <+> ppMeta metaid <+> colon <+> ppType 0 xs ty $$
text "cannot be solved" text "cannot be solved"
------------------------------------------------------------------------------
-- Selectors
class Selector s where
splitSelector :: s -> (s,s)
select :: CId -> TcM s CId
instance Selector () where
splitSelector s = (s,s)
select cat = TcM (\abstr s ms -> case Map.lookup cat (cats abstr) of
Just (_,fns) -> iter ms fns
Nothing -> Fail (UnknownCat cat))
where
iter ms [] = Zero
iter ms ((_,fn):fns) = Plus (Ok () ms fn) (iter ms fns)
instance RandomGen g => Selector (Identity g) where
splitSelector (Identity g) = let (g1,g2) = Random.split g
in (Identity g1, Identity g2)
select cat = TcM (\abstr (Identity g) ms ->
case Map.lookup cat (cats abstr) of
Just (_,fns) -> do_rand g ms 1.0 fns
Nothing -> Fail (UnknownCat cat))
where
do_rand g ms p [] = Zero
do_rand g ms p fns = let (d,g') = randomR (0.0,p) g
(g1,g2) = Random.split g'
(p',fn,fns') = hit d fns
in Plus (Ok (Identity g1) ms fn) (do_rand g2 ms (p-p') fns')
hit :: Double -> [(Double,a)] -> (Double,a,[(Double,a)])
hit d (px@(p,x):xs)
| d < p = (p,x,xs)
| otherwise = let (p',x',xs') = hit (d-p) xs
in (p,x',px:xs')
----------------------------------------------------- -----------------------------------------------------
-- checkType -- checkType
----------------------------------------------------- -----------------------------------------------------
@@ -213,11 +266,11 @@ ppTcError (UnsolvableGoal xs metaid ty)= text "The goal:" <+> ppMeta metaid <+>
-- syntax of the grammar. -- syntax of the grammar.
checkType :: PGF -> Type -> Either TcError Type checkType :: PGF -> Type -> Either TcError Type
checkType pgf ty = checkType pgf ty =
case unTcM (tcType emptyScope ty >>= refineType) (abstract pgf) emptyMetaStore of case unTcM (tcType emptyScope ty >>= refineType) (abstract pgf) () emptyMetaStore of
Ok ms ty -> Right ty Ok s ms ty -> Right ty
Fail err -> Left err Fail err -> Left err
tcType :: Scope -> Type -> TcM Type tcType :: Scope -> Type -> TcM s Type
tcType scope ty@(DTyp hyps cat es) = do tcType scope ty@(DTyp hyps cat es) = do
(scope,hyps) <- tcHypos scope hyps (scope,hyps) <- tcHypos scope hyps
c_hyps <- lookupCatHyps cat c_hyps <- lookupCatHyps cat
@@ -226,14 +279,14 @@ tcType scope ty@(DTyp hyps cat es) = do
(delta,es) <- tcCatArgs scope es [] c_hyps ty n m (delta,es) <- tcCatArgs scope es [] c_hyps ty n m
return (DTyp hyps cat es) return (DTyp hyps cat es)
tcHypos :: Scope -> [Hypo] -> TcM (Scope,[Hypo]) tcHypos :: Scope -> [Hypo] -> TcM s (Scope,[Hypo])
tcHypos scope [] = return (scope,[]) tcHypos scope [] = return (scope,[])
tcHypos scope (h:hs) = do tcHypos scope (h:hs) = do
(scope,h ) <- tcHypo scope h (scope,h ) <- tcHypo scope h
(scope,hs) <- tcHypos scope hs (scope,hs) <- tcHypos scope hs
return (scope,h:hs) return (scope,h:hs)
tcHypo :: Scope -> Hypo -> TcM (Scope,Hypo) tcHypo :: Scope -> Hypo -> TcM s (Scope,Hypo)
tcHypo scope (b,x,ty) = do tcHypo scope (b,x,ty) = do
ty <- tcType scope ty ty <- tcType scope ty
if x == wildCId if x == wildCId
@@ -275,11 +328,11 @@ checkExpr pgf e ty =
case unTcM (do e <- tcExpr emptyScope e (TTyp [] ty) case unTcM (do e <- tcExpr emptyScope e (TTyp [] ty)
e <- refineExpr e e <- refineExpr e
checkResolvedMetaStore emptyScope e checkResolvedMetaStore emptyScope e
return e) (abstract pgf) emptyMetaStore of return e) (abstract pgf) () emptyMetaStore of
Ok ms e -> Right e Ok _ ms e -> Right e
Fail err -> Left err Fail err -> Left err
tcExpr :: Scope -> Expr -> TType -> TcM Expr tcExpr :: Scope -> Expr -> TType -> TcM s Expr
tcExpr scope e0@(EAbs Implicit x e) tty = tcExpr scope e0@(EAbs Implicit x e) tty =
case tty of case tty of
TTyp delta (DTyp ((Implicit,y,ty):hs) c es) -> do e <- if y == wildCId TTyp delta (DTyp ((Implicit,y,ty):hs) c es) -> do e <- if y == wildCId
@@ -331,11 +384,11 @@ inferExpr pgf e =
e <- refineExpr e e <- refineExpr e
checkResolvedMetaStore emptyScope e checkResolvedMetaStore emptyScope e
ty <- evalType 0 tty ty <- evalType 0 tty
return (e,ty)) (abstract pgf) emptyMetaStore of return (e,ty)) (abstract pgf) () emptyMetaStore of
Ok ms (e,ty) -> Right (e,ty) Ok _ ms (e,ty) -> Right (e,ty)
Fail err -> Left err Fail err -> Left err
infExpr :: Scope -> Expr -> TcM (Expr,TType) infExpr :: Scope -> Expr -> TcM s (Expr,TType)
infExpr scope e0@(EApp e1 e2) = do infExpr scope e0@(EApp e1 e2) = do
(e1,TTyp delta ty) <- infExpr scope e1 (e1,TTyp delta ty) <- infExpr scope e1
(e0,delta,ty) <- tcArg scope e1 e2 delta ty (e0,delta,ty) <- tcArg scope e1 e2 delta ty
@@ -343,8 +396,8 @@ infExpr scope e0@(EApp e1 e2) = do
infExpr scope e0@(EFun x) = do infExpr scope e0@(EFun x) = do
case lookupVar x scope of case lookupVar x scope of
Just (i,tty) -> return (EVar i,tty) Just (i,tty) -> return (EVar i,tty)
Nothing -> do tty <- lookupFunType x Nothing -> do ty <- lookupFunType x
return (e0,tty) return (e0,TTyp [] ty)
infExpr scope e0@(EVar i) = do infExpr scope e0@(EVar i) = do
return (e0,snd (getVar i scope)) return (e0,snd (getVar i scope))
infExpr scope e0@(ELit l) = do infExpr scope e0@(ELit l) = do
@@ -388,10 +441,10 @@ tcArg scope e1 e2 delta ty0@(DTyp ((Implicit,x,ty):hs) c es) = do
-- eqType -- eqType
----------------------------------------------------- -----------------------------------------------------
eqType :: Scope -> Int -> MetaId -> TType -> TType -> TcM () eqType :: Scope -> Int -> MetaId -> TType -> TType -> TcM s ()
eqType scope k i0 tty1@(TTyp delta1 ty1@(DTyp hyps1 cat1 es1)) tty2@(TTyp delta2 ty2@(DTyp hyps2 cat2 es2)) eqType scope k i0 tty1@(TTyp delta1 ty1@(DTyp hyps1 cat1 es1)) tty2@(TTyp delta2 ty2@(DTyp hyps2 cat2 es2))
| cat1 == cat2 = do (k,delta1,delta2) <- eqHyps k delta1 hyps1 delta2 hyps2 | cat1 == cat2 = do (k,delta1,delta2) <- eqHyps k delta1 hyps1 delta2 hyps2
sequence_ [eqExpr k delta1 e1 delta2 e2 | (e1,e2) <- zip es1 es2] sequence_ [eqExpr raiseTypeMatchError (addConstraint i0) k delta1 e1 delta2 e2 | (e1,e2) <- zip es1 es2]
| otherwise = raiseTypeMatchError | otherwise = raiseTypeMatchError
where where
raiseTypeMatchError = do ty1 <- evalType k tty1 raiseTypeMatchError = do ty1 <- evalType k tty1
@@ -399,7 +452,7 @@ eqType scope k i0 tty1@(TTyp delta1 ty1@(DTyp hyps1 cat1 es1)) tty2@(TTyp delta2
e <- refineExpr (EMeta i0) e <- refineExpr (EMeta i0)
tcError (TypeMismatch (scopeVars scope) e ty1 ty2) tcError (TypeMismatch (scopeVars scope) e ty1 ty2)
eqHyps :: Int -> Env -> [Hypo] -> Env -> [Hypo] -> TcM (Int,Env,Env) eqHyps :: Int -> Env -> [Hypo] -> Env -> [Hypo] -> TcM s (Int,Env,Env)
eqHyps k delta1 [] delta2 [] = eqHyps k delta1 [] delta2 [] =
return (k,delta1,delta2) return (k,delta1,delta2)
eqHyps k delta1 ((_,x,ty1) : h1s) delta2 ((_,y,ty2) : h2s) = do eqHyps k delta1 ((_,x,ty1) : h1s) delta2 ((_,y,ty2) : h2s) = do
@@ -411,18 +464,18 @@ eqType scope k i0 tty1@(TTyp delta1 ty1@(DTyp hyps1 cat1 es1)) tty2@(TTyp delta2
else raiseTypeMatchError else raiseTypeMatchError
eqHyps k delta1 h1s delta2 h2s = raiseTypeMatchError eqHyps k delta1 h1s delta2 h2s = raiseTypeMatchError
eqExpr :: Int -> Env -> Expr -> Env -> Expr -> TcM () eqExpr :: (forall a . TcM s a) -> (MetaId -> (Expr -> TcM s ()) -> TcM s ()) -> Int -> Env -> Expr -> Env -> Expr -> TcM s ()
eqExpr k env1 e1 env2 e2 = do eqExpr fail suspend k env1 e1 env2 e2 = do
v1 <- eval env1 e1 v1 <- eval env1 e1
v2 <- eval env2 e2 v2 <- eval env2 e2
eqValue k v1 v2 eqValue fail suspend k v1 v2
eqValue :: Int -> Value -> Value -> TcM () eqValue :: (forall a . TcM s a) -> (MetaId -> (Expr -> TcM s ()) -> TcM s ()) -> Int -> Value -> Value -> TcM s ()
eqValue k v1 v2 = do eqValue fail suspend k v1 v2 = do
v1 <- deRef v1 v1 <- deRef v1
v2 <- deRef v2 v2 <- deRef v2
eqValue' k v1 v2 eqValue' k v1 v2
where
deRef v@(VMeta i env vs) = do deRef v@(VMeta i env vs) = do
mv <- getMeta i mv <- getMeta i
case mv of case mv of
@@ -432,9 +485,9 @@ eqType scope k i0 tty1@(TTyp delta1 ty1@(DTyp hyps1 cat1 es1)) tty2@(TTyp delta2
MUnbound _ _ _ -> return v MUnbound _ _ _ -> return v
deRef v = return v deRef v = return v
eqValue' k (VSusp i env vs1 c) v2 = addConstraint i0 i env vs1 (\v1 -> eqValue k (c v1) v2) eqValue' k (VSusp i env vs1 c) v2 = suspend i (\e -> apply env e vs1 >>= \v1 -> eqValue fail suspend k (c v1) v2)
eqValue' k v1 (VSusp i env vs2 c) = addConstraint i0 i env vs2 (\v2 -> eqValue k v1 (c v2)) eqValue' k v1 (VSusp i env vs2 c) = suspend i (\e -> apply env e vs2 >>= \v2 -> eqValue fail suspend k v1 (c v2))
eqValue' k (VMeta i env1 vs1) (VMeta j env2 vs2) | i == j = zipWithM_ (eqValue k) vs1 vs2 eqValue' k (VMeta i env1 vs1) (VMeta j env2 vs2) | i == j = zipWithM_ (eqValue fail suspend k) vs1 vs2
eqValue' k (VMeta i env1 vs1) v2 = do mv <- getMeta i eqValue' k (VMeta i env1 vs1) v2 = do mv <- getMeta i
case mv of case mv of
MUnbound scopei _ cs -> do e2 <- mkLam i scopei env1 vs1 v2 MUnbound scopei _ cs -> do e2 <- mkLam i scopei env1 vs1 v2
@@ -447,13 +500,13 @@ eqType scope k i0 tty1@(TTyp delta1 ty1@(DTyp hyps1 cat1 es1)) tty2@(TTyp delta2
setMeta i (MBound e1) setMeta i (MBound e1)
sequence_ [c e1 | c <- cs] sequence_ [c e1 | c <- cs]
MGuarded e cs x -> setMeta i (MGuarded e ((\e -> apply env2 e vs2 >>= \v2 -> eqValue' k v1 v2) : cs) x) MGuarded e cs x -> setMeta i (MGuarded e ((\e -> apply env2 e vs2 >>= \v2 -> eqValue' k v1 v2) : cs) x)
eqValue' k (VApp f1 vs1) (VApp f2 vs2) | f1 == f2 = zipWithM_ (eqValue k) vs1 vs2 eqValue' k (VApp f1 vs1) (VApp f2 vs2) | f1 == f2 = zipWithM_ (eqValue fail suspend k) vs1 vs2
eqValue' k (VConst f1 vs1) (VConst f2 vs2) | f1 == f2 = zipWithM_ (eqValue k) vs1 vs2 eqValue' k (VConst f1 vs1) (VConst f2 vs2) | f1 == f2 = zipWithM_ (eqValue fail suspend k) vs1 vs2
eqValue' k (VLit l1) (VLit l2 ) | l1 == l2 = return () eqValue' k (VLit l1) (VLit l2 ) | l1 == l2 = return ()
eqValue' k (VGen i vs1) (VGen j vs2) | i == j = zipWithM_ (eqValue k) vs1 vs2 eqValue' k (VGen i vs1) (VGen j vs2) | i == j = zipWithM_ (eqValue fail suspend k) vs1 vs2
eqValue' k (VClosure env1 (EAbs _ x1 e1)) (VClosure env2 (EAbs _ x2 e2)) = let v = VGen k [] eqValue' k (VClosure env1 (EAbs _ x1 e1)) (VClosure env2 (EAbs _ x2 e2)) = let v = VGen k []
in eqExpr (k+1) (v:env1) e1 (v:env2) e2 in eqExpr fail suspend (k+1) (v:env1) e1 (v:env2) e2
eqValue' k v1 v2 = raiseTypeMatchError eqValue' k v1 v2 = fail
mkLam i scope env vs0 v = do mkLam i scope env vs0 v = do
let k = scopeSize scope let k = scopeSize scope
@@ -461,7 +514,7 @@ eqType scope k i0 tty1@(TTyp delta1 ty1@(DTyp hyps1 cat1 es1)) tty2@(TTyp delta2
xs = nub [i | VGen i [] <- vs] xs = nub [i | VGen i [] <- vs]
if length vs == length xs if length vs == length xs
then return () then return ()
else raiseTypeMatchError else fail
v <- occurCheck i k xs v v <- occurCheck i k xs v
e <- value2expr (length xs) v e <- value2expr (length xs) v
return (addLam vs0 e) return (addLam vs0 e)
@@ -475,21 +528,21 @@ eqType scope k i0 tty1@(TTyp delta1 ty1@(DTyp hyps1 cat1 es1)) tty2@(TTyp delta2
return (VApp f vs) return (VApp f vs)
occurCheck i0 k xs (VLit l) = return (VLit l) occurCheck i0 k xs (VLit l) = return (VLit l)
occurCheck i0 k xs (VMeta i env vs) = do if i == i0 occurCheck i0 k xs (VMeta i env vs) = do if i == i0
then raiseTypeMatchError then fail
else return () else return ()
mv <- getMeta i mv <- getMeta i
case mv of case mv of
MBound e -> apply env e vs >>= occurCheck i0 k xs MBound e -> apply env e vs >>= occurCheck i0 k xs
MGuarded e _ _ -> apply env e vs >>= occurCheck i0 k xs MGuarded e _ _ -> apply env e vs >>= occurCheck i0 k xs
MUnbound scopei _ _ | scopeSize scopei > k -> raiseTypeMatchError MUnbound scopei _ _ | scopeSize scopei > k -> fail
| otherwise -> do vs <- mapM (occurCheck i0 k xs) vs | otherwise -> do vs <- mapM (occurCheck i0 k xs) vs
return (VMeta i env vs) return (VMeta i env vs)
occurCheck i0 k xs (VSusp i env vs cnt) = do addConstraint i0 i env vs (\v -> occurCheck i0 k xs (cnt v) >> return ()) occurCheck i0 k xs (VSusp i env vs cnt) = do suspend i (\e -> apply env e vs >>= \v -> occurCheck i0 k xs (cnt v) >> return ())
return (VSusp i env vs cnt) return (VSusp i env vs cnt)
occurCheck i0 k xs (VGen i vs) = case List.findIndex (==i) xs of occurCheck i0 k xs (VGen i vs) = case List.findIndex (==i) xs of
Just i -> do vs <- mapM (occurCheck i0 k xs) vs Just i -> do vs <- mapM (occurCheck i0 k xs) vs
return (VGen i vs) return (VGen i vs)
Nothing -> raiseTypeMatchError Nothing -> fail
occurCheck i0 k xs (VConst f vs) = do vs <- mapM (occurCheck i0 k xs) vs occurCheck i0 k xs (VConst f vs) = do vs <- mapM (occurCheck i0 k xs) vs
return (VConst f vs) return (VConst f vs)
occurCheck i0 k xs (VClosure env e) = do env <- mapM (occurCheck i0 k xs) env occurCheck i0 k xs (VClosure env e) = do env <- mapM (occurCheck i0 k xs) env
@@ -500,11 +553,11 @@ eqType scope k i0 tty1@(TTyp delta1 ty1@(DTyp hyps1 cat1 es1)) tty2@(TTyp delta2
-- check for meta variables that still have to be resolved -- check for meta variables that still have to be resolved
----------------------------------------------------------- -----------------------------------------------------------
checkResolvedMetaStore :: Scope -> Expr -> TcM () checkResolvedMetaStore :: Scope -> Expr -> TcM s ()
checkResolvedMetaStore scope e = TcM (\abstr ms -> checkResolvedMetaStore scope e = TcM (\abstr s ms ->
let xs = [i | (i,mv) <- IntMap.toList ms, not (isResolved mv)] let xs = [i | (i,mv) <- IntMap.toList ms, not (isResolved mv)]
in if List.null xs in if List.null xs
then Ok ms () then Ok s ms ()
else Fail (UnresolvedMetaVars (scopeVars scope) e xs)) else Fail (UnresolvedMetaVars (scopeVars scope) e xs))
where where
isResolved (MUnbound _ _ []) = True isResolved (MUnbound _ _ []) = True
@@ -516,7 +569,7 @@ checkResolvedMetaStore scope e = TcM (\abstr ms ->
-- evalType -- evalType
----------------------------------------------------- -----------------------------------------------------
evalType :: Int -> TType -> TcM Type evalType :: Int -> TType -> TcM s Type
evalType k (TTyp delta ty) = evalTy funs k delta ty evalType k (TTyp delta ty) = evalTy funs k delta ty
where where
evalTy sig k delta (DTyp hyps cat es) = do evalTy sig k delta (DTyp hyps cat es) = do
@@ -537,8 +590,8 @@ evalType k (TTyp delta ty) = evalTy funs k delta ty
-- refinement -- refinement
----------------------------------------------------- -----------------------------------------------------
refineExpr :: Expr -> TcM Expr refineExpr :: Expr -> TcM s Expr
refineExpr e = TcM (\abstr ms -> Ok ms (refineExpr_ ms e)) refineExpr e = TcM (\abstr s ms -> Ok s ms (refineExpr_ ms e))
refineExpr_ ms e = refine e refineExpr_ ms e = refine e
where where
@@ -554,16 +607,16 @@ refineExpr_ ms e = refine e
refine (ETyped e ty) = ETyped (refine e) (refineType_ ms ty) refine (ETyped e ty) = ETyped (refine e) (refineType_ ms ty)
refine (EImplArg e) = EImplArg (refine e) refine (EImplArg e) = EImplArg (refine e)
refineType :: Type -> TcM Type refineType :: Type -> TcM s Type
refineType ty = TcM (\abstr ms -> Ok ms (refineType_ ms ty)) refineType ty = TcM (\abstr s ms -> Ok s ms (refineType_ ms ty))
refineType_ ms (DTyp hyps cat es) = DTyp [(b,x,refineType_ ms ty) | (b,x,ty) <- hyps] cat (List.map (refineExpr_ ms) es) refineType_ ms (DTyp hyps cat es) = DTyp [(b,x,refineType_ ms ty) | (b,x,ty) <- hyps] cat (List.map (refineExpr_ ms) es)
eval :: Env -> Expr -> TcM Value eval :: Env -> Expr -> TcM s Value
eval env e = TcM (\abstr ms -> Ok ms (Expr.eval (funs abstr,lookupMeta ms) env e)) eval env e = TcM (\abstr s ms -> Ok s ms (Expr.eval (funs abstr,lookupMeta ms) env e))
apply :: Env -> Expr -> [Value] -> TcM Value apply :: Env -> Expr -> [Value] -> TcM s Value
apply env e vs = TcM (\abstr ms -> Ok ms (Expr.apply (funs abstr,lookupMeta ms) env e vs)) apply env e vs = TcM (\abstr s ms -> Ok s ms (Expr.apply (funs abstr,lookupMeta ms) env e vs))
value2expr :: Int -> Value -> TcM Expr value2expr :: Int -> Value -> TcM s Expr
value2expr i v = TcM (\abstr ms -> Ok ms (Expr.value2expr (funs abstr,lookupMeta ms) i v)) value2expr i v = TcM (\abstr s ms -> Ok s ms (Expr.value2expr (funs abstr,lookupMeta ms) i v))

4
src/server/gf-server.cabal
View File

@@ -35,3 +35,7 @@ executable pgf-server
ghc-options: -threaded ghc-options: -threaded
if os(windows) if os(windows)
ghc-options: -optl-mwindows ghc-options: -optl-mwindows
executable content-server
build-depends: base >=4.2 && <5
main-is: ContentService.hs

30
src/ui/gwt/src/org/grammaticalframework/ui/gwt/client/JSONRequestBuilder.java
View File

@@ -53,6 +53,36 @@ public class JSONRequestBuilder {
return new JSONRequest(request); return new JSONRequest(request);
} }
public static <T extends JavaScriptObject> JSONRequest sendDataRequest (String base, List<Arg> vars, String content, final JSONCallback<T> callback) {
String url = getQueryURL(base,vars);
RequestBuilder builder = new RequestBuilder(RequestBuilder.POST, url);
builder.setRequestData(content);
builder.setTimeoutMillis(30000);
builder.setHeader("Accept","text/plain, text/html;q=0.5, */*;q=0.1");
Request request = null;
try {
request = builder.sendRequest(null, new RequestCallback() {
public void onError(Request request, Throwable e) {
callback.onError(e);
}
public void onResponseReceived(Request request, Response response) {
if (200 == response.getStatusCode()) {
callback.onResult(JSONRequestBuilder.<T>eval(response.getText()));
} else {
RequestException e = new RequestException("Response not OK: " + response.getStatusCode() + ". " + response.getText());
callback.onError(e);
}
}
});
} catch (RequestException e) {
callback.onError(e);
}
return new JSONRequest(request);
}
private static native <T extends JavaScriptObject> T eval(String json) /*-{ private static native <T extends JavaScriptObject> T eval(String json) /*-{
return eval('(' + json + ')'); return eval('(' + json + ')');
}-*/; }-*/;