mirror of
https://github.com/GrammaticalFramework/gf-core.git
synced 2026-04-09 04:59:31 -06:00
the exhaustive/random generator now knows how to handle computable functions in the types
This commit is contained in:
krasimir
@@ -133,9 +133,9 @@ getAbsTrees (Forest abs cnc forest root) arg@(PArg _ fid) ty =
|
||||
case isLindefCId fn of
|
||||
Just _ -> do arg <- go (Set.insert fid rec_) scope (head args) mb_tty
|
||||
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)
|
||||
(EFun fn,tty_fn) args
|
||||
(EFun fn,TTyp [] ty_fn) args
|
||||
case mb_tty of
|
||||
Just tty -> runTcM abs fid $ do
|
||||
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)]
|
||||
|
||||
|
||||
newtype TcFM a = TcFM {unTcFM :: MetaStore -> ([(MetaStore,a)],[(FId,TcError)])}
|
||||
newtype TcFM a = TcFM {unTcFM :: MetaStore () -> ([(MetaStore (),a)],[(FId,TcError)])}
|
||||
|
||||
instance Functor TcFM where
|
||||
fmap f g = TcFM (\ms -> let (res_g,err_g) = unTcFM g ms
|
||||
@@ -201,10 +201,10 @@ instance MonadPlus TcFM where
|
||||
(res_g,err_g) = unTcFM g ms
|
||||
in (res_f++res_g,err_f++err_g))
|
||||
|
||||
runTcM :: Abstr -> FId -> TcM a -> TcFM a
|
||||
runTcM abstr fid f = TcFM (\ms -> case unTcM f abstr ms of
|
||||
Ok ms x -> ([(ms,x)],[] )
|
||||
Fail err -> ([], [(fid,err)]))
|
||||
runTcM :: Abstr -> FId -> TcM () a -> TcFM a
|
||||
runTcM abstr fid f = TcFM (\ms -> case unTcM f abstr () ms of
|
||||
Ok _ ms x -> ([(ms,x)],[] )
|
||||
Fail err -> ([], [(fid,err)]))
|
||||
|
||||
foldForest :: (FunId -> [PArg] -> b -> b) -> (Expr -> [String] -> b -> b) -> b -> FId -> IntMap.IntMap (Set.Set Production) -> b
|
||||
foldForest f g b fcat forest =
|
||||
|
||||
@@ -67,41 +67,52 @@ generateRandomFromDepth g pgf e dp =
|
||||
generate :: Selector sel => sel -> PGF -> Type -> Maybe Int -> [Expr]
|
||||
generate sel pgf ty dp =
|
||||
[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 sel pgf e dp =
|
||||
case unTcM (infExpr emptyScope e) abs emptyMetaStore of
|
||||
Ok ms (e,_) -> let gen = do fillinVariables (runTcM abs) $ \scope tty -> do
|
||||
v <- prove abs scope tty dp
|
||||
return (value2expr (funs abs,lookupMeta ms) 0 v)
|
||||
runTcM abs (refineExpr e)
|
||||
in [e | (ms,e) <- runGenM gen sel ms]
|
||||
Fail _ -> []
|
||||
case unTcM (infExpr emptyScope e) abs sel emptyMetaStore of
|
||||
Ok sel ms (e,_) -> let gen = do fillinVariables $ \scope tty -> do
|
||||
v <- prove scope tty dp
|
||||
return (value2expr (funs abs,lookupMeta ms) 0 v)
|
||||
refineExpr e
|
||||
in [e | (ms,e) <- runGenM abs gen sel ms]
|
||||
Fail _ -> []
|
||||
where
|
||||
abs = abstract pgf
|
||||
|
||||
prove :: Selector sel => Abstr -> Scope -> TType -> Maybe Int -> GenM sel MetaStore Value
|
||||
prove abs scope tty@(TTyp env (DTyp [] cat es)) dp = do
|
||||
(fn,DTyp hypos cat es) <- clauses cat
|
||||
prove :: Selector sel => Scope -> TType -> Maybe Int -> TcM sel Value
|
||||
prove scope (TTyp env1 (DTyp [] cat es1)) dp = do
|
||||
(fn,DTyp hypos _ es2) <- clauses cat
|
||||
case dp of
|
||||
Just 0 | not (null hypos) -> mzero
|
||||
_ -> return ()
|
||||
(env,args) <- mkEnv [] hypos
|
||||
runTcM abs (eqType scope (scopeSize scope) 0 (TTyp env (DTyp [] cat es)) tty)
|
||||
(env2,args) <- mkEnv [] hypos
|
||||
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
|
||||
return (VApp fn vs)
|
||||
where
|
||||
clauses cat =
|
||||
do fn <- select abs cat
|
||||
case Map.lookup fn (funs abs) of
|
||||
Just (ty,_,_,_) -> return (fn,ty)
|
||||
Nothing -> mzero
|
||||
suspend i c = do
|
||||
mv <- getMeta i
|
||||
case mv of
|
||||
MBound e -> c e
|
||||
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 ((bt,x,ty):hypos) = do
|
||||
(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 []
|
||||
return (v : env,Right v)
|
||||
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
|
||||
v <- case arg of
|
||||
Right v -> return v
|
||||
Left tty -> prove abs scope tty dp'
|
||||
Left tty -> prove scope tty dp'
|
||||
v <- case bt of
|
||||
Implicit -> return (VImplArg v)
|
||||
Explicit -> return v
|
||||
@@ -121,75 +132,15 @@ prove abs scope tty@(TTyp env (DTyp [] cat es)) dp = do
|
||||
------------------------------------------------------------------------------
|
||||
-- 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
|
||||
return x = GenM (\sel s -> COk sel s x)
|
||||
f >>= g = GenM (\sel s -> iter (unGen f sel s))
|
||||
where
|
||||
iter (COk sel s x) = unGen (g x) sel s
|
||||
iter (CBranch b1 b2) = CBranch (iter b1) (iter b2)
|
||||
iter CFail = CFail
|
||||
fail _ = GenM (\sel s -> CFail)
|
||||
|
||||
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) []
|
||||
runGenM :: Abstr -> TcM s a -> s -> MetaStore s -> [(MetaStore s,a)]
|
||||
runGenM abs f s ms = toList (unTcM f abs s ms) []
|
||||
where
|
||||
toList (COk sel s x) xs = (s,x) : xs
|
||||
toList (CFail) xs = xs
|
||||
toList (CBranch b1 b2) xs = toList b1 (toList b2 xs)
|
||||
toList (Ok s ms x) xs = (ms,x) : xs
|
||||
toList (Fail _) xs = xs
|
||||
toList (Zero) xs = xs
|
||||
toList (Plus 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
|
||||
-- success we must restart the search to find sufficiently different solution.
|
||||
|
||||
@@ -18,10 +18,10 @@ module PGF.TypeCheck ( checkType, checkExpr, inferExpr
|
||||
, ppTcError, TcError(..)
|
||||
|
||||
-- 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
|
||||
, TcM(..), TcResult(..), TType(..), tcError
|
||||
, tcExpr, infExpr, eqType
|
||||
, TcM(..), TcResult(..), TType(..), Selector(..), tcError
|
||||
, tcExpr, infExpr, eqType, eqValue
|
||||
, lookupFunType, eval
|
||||
, refineExpr, checkResolvedMetaStore, lookupMeta
|
||||
) where
|
||||
@@ -37,7 +37,9 @@ import Data.IntMap as IntMap
|
||||
import Data.Maybe as Maybe
|
||||
import Data.List as List
|
||||
import Control.Monad
|
||||
import Control.Monad.Identity
|
||||
import Text.PrettyPrint
|
||||
import System.Random as Random
|
||||
|
||||
-----------------------------------------------------
|
||||
-- The Scope
|
||||
@@ -73,55 +75,69 @@ scopeSize (Scope gamma) = length gamma
|
||||
-- The Monad
|
||||
-----------------------------------------------------
|
||||
|
||||
type MetaStore = IntMap MetaValue
|
||||
data MetaValue
|
||||
= MUnbound Scope TType [Expr -> TcM ()]
|
||||
type MetaStore s = IntMap (MetaValue s)
|
||||
data MetaValue s
|
||||
= MUnbound Scope TType [Expr -> TcM s ()]
|
||||
| MBound Expr
|
||||
| MGuarded Expr [Expr -> TcM ()] {-# UNPACK #-} !Int -- the Int is the number of constraints that have to be solved
|
||||
-- to unlock this meta variable
|
||||
| MGuarded Expr [Expr -> TcM s ()] {-# UNPACK #-} !Int -- the Int is the number of constraints that have to be solved
|
||||
-- to unlock this meta variable
|
||||
|
||||
newtype TcM a = TcM {unTcM :: Abstr -> MetaStore -> TcResult a}
|
||||
data TcResult a
|
||||
= Ok MetaStore a
|
||||
newtype TcM s a = TcM {unTcM :: Abstr -> s -> MetaStore s -> TcResult s a}
|
||||
data TcResult s a
|
||||
= Ok s (MetaStore s) a
|
||||
| Fail TcError
|
||||
| Zero
|
||||
| Plus (TcResult s a) (TcResult s a)
|
||||
|
||||
instance Monad TcM where
|
||||
return x = TcM (\abstr ms -> Ok ms x)
|
||||
f >>= g = TcM (\abstr ms -> case unTcM f abstr ms of
|
||||
Ok ms x -> unTcM (g x) abstr ms
|
||||
Fail e -> Fail e)
|
||||
instance Monad (TcM s) where
|
||||
return x = TcM (\abstr s ms -> Ok s ms x)
|
||||
f >>= g = TcM (\abstr s ms -> iter abstr (unTcM f abstr s ms))
|
||||
where
|
||||
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
|
||||
fmap f x = TcM (\abstr ms -> case unTcM x abstr ms of
|
||||
Ok ms x -> Ok ms (f x)
|
||||
Fail e -> Fail e)
|
||||
instance Selector s => MonadPlus (TcM s) where
|
||||
mzero = TcM (\abstr s ms -> Zero)
|
||||
mplus f g = TcM (\abstr s ms -> let (s1,s2) = splitSelector s
|
||||
in Plus (unTcM f abstr s1 ms) (unTcM g abstr s2 ms))
|
||||
|
||||
lookupCatHyps :: CId -> TcM [Hypo]
|
||||
lookupCatHyps cat = TcM (\abstr ms -> case Map.lookup cat (cats abstr) of
|
||||
Just (hyps,_) -> Ok ms hyps
|
||||
Nothing -> Fail (UnknownCat cat))
|
||||
instance Functor (TcM s) where
|
||||
fmap f x = TcM (\abstr s ms -> iter (unTcM x abstr s ms))
|
||||
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)
|
||||
|
||||
lookupFunType :: CId -> TcM TType
|
||||
lookupFunType fun = TcM (\abstr ms -> case Map.lookup fun (funs abstr) of
|
||||
Just (ty,_,_,_) -> Ok ms (TTyp [] ty)
|
||||
Nothing -> Fail (UnknownFun fun))
|
||||
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))
|
||||
|
||||
emptyMetaStore :: MetaStore
|
||||
lookupFunType :: CId -> TcM s Type
|
||||
lookupFunType fun = TcM (\abstr s ms -> case Map.lookup fun (funs abstr) of
|
||||
Just (ty,_,_,_) -> Ok s ms ty
|
||||
Nothing -> Fail (UnknownFun fun))
|
||||
|
||||
emptyMetaStore :: MetaStore s
|
||||
emptyMetaStore = IntMap.empty
|
||||
|
||||
newMeta :: Scope -> TType -> TcM MetaId
|
||||
newMeta scope tty = TcM (\abstr ms -> let metaid = IntMap.size ms + 1
|
||||
in Ok (IntMap.insert metaid (MUnbound scope tty []) ms) metaid)
|
||||
newMeta :: Scope -> TType -> TcM s MetaId
|
||||
newMeta scope tty = TcM (\abstr s ms -> let metaid = IntMap.size ms + 1
|
||||
in Ok s (IntMap.insert metaid (MUnbound scope tty []) ms) metaid)
|
||||
|
||||
newGuardedMeta :: Expr -> TcM MetaId
|
||||
newGuardedMeta e = TcM (\abstr ms -> let metaid = IntMap.size ms + 1
|
||||
in Ok (IntMap.insert metaid (MGuarded e [] 0) ms) metaid)
|
||||
newGuardedMeta :: Expr -> TcM s MetaId
|
||||
newGuardedMeta e = TcM (\abstr s ms -> let metaid = IntMap.size ms + 1
|
||||
in Ok s (IntMap.insert metaid (MGuarded e [] 0) ms) metaid)
|
||||
|
||||
getMeta :: MetaId -> TcM MetaValue
|
||||
getMeta i = TcM (\abstr ms -> Ok ms $! case IntMap.lookup i ms of
|
||||
Just mv -> mv)
|
||||
setMeta :: MetaId -> MetaValue -> TcM ()
|
||||
setMeta i mv = TcM (\abstr ms -> Ok (IntMap.insert i mv ms) ())
|
||||
getMeta :: MetaId -> TcM s (MetaValue s)
|
||||
getMeta i = TcM (\abstr s ms -> Ok s ms $! case IntMap.lookup i ms of
|
||||
Just mv -> mv)
|
||||
|
||||
setMeta :: MetaId -> MetaValue s -> TcM s ()
|
||||
setMeta i mv = TcM (\abstr s ms -> Ok s (IntMap.insert i mv ms) ())
|
||||
|
||||
lookupMeta ms i =
|
||||
case IntMap.lookup i ms of
|
||||
@@ -131,35 +147,35 @@ lookupMeta ms i =
|
||||
Just (MUnbound _ _ _) -> Nothing
|
||||
Nothing -> Nothing
|
||||
|
||||
fillinVariables :: Monad m => (forall a . TcM a -> m a) -> (Scope -> TType -> m Expr) -> m ()
|
||||
fillinVariables runTcM f = do
|
||||
fvs <- runTcM (TcM (\abstr ms -> Ok ms [(i,scope,tty,cs) | (i,MUnbound scope tty cs) <- IntMap.toList ms]))
|
||||
fillinVariables :: (Scope -> TType -> TcM s Expr) -> TcM s ()
|
||||
fillinVariables f = do
|
||||
fvs <- TcM (\abstr s ms -> Ok s ms [(i,scope,tty,cs) | (i,MUnbound scope tty cs) <- IntMap.toList ms])
|
||||
case fvs of
|
||||
[] -> return ()
|
||||
(i,scope,tty,cs):_ -> do e <- f scope tty
|
||||
runTcM $ do setMeta i (MBound e)
|
||||
sequence_ [c e | c <- cs]
|
||||
fillinVariables runTcM f
|
||||
setMeta i (MBound e)
|
||||
sequence_ [c e | c <- cs]
|
||||
fillinVariables f
|
||||
|
||||
tcError :: TcError -> TcM a
|
||||
tcError e = TcM (\abstr ms -> Fail e)
|
||||
tcError :: TcError -> TcM s a
|
||||
tcError e = TcM (\abstr s ms -> Fail e)
|
||||
|
||||
addConstraint :: MetaId -> MetaId -> Env -> [Value] -> (Value -> TcM ()) -> TcM ()
|
||||
addConstraint i j env vs c = do
|
||||
addConstraint :: MetaId -> MetaId -> (Expr -> TcM s ()) -> TcM s ()
|
||||
addConstraint i j c = do
|
||||
mv <- getMeta j
|
||||
case mv of
|
||||
MUnbound scope tty cs -> addRef >> setMeta j (MUnbound scope tty ((\e -> release >> apply env e vs >>= c) : cs))
|
||||
MBound e -> apply env e vs >>= c
|
||||
MGuarded e cs x | x == 0 -> apply env e vs >>= c
|
||||
| otherwise -> addRef >> setMeta j (MGuarded e ((\e -> release >> apply env e vs >>= c) : cs) x)
|
||||
MUnbound scope tty cs -> addRef >> setMeta j (MUnbound scope tty ((\e -> release >> c e) : cs))
|
||||
MBound e -> c e
|
||||
MGuarded e cs x | x == 0 -> c e
|
||||
| otherwise -> addRef >> setMeta j (MGuarded e ((\e -> release >> c e) : cs) x)
|
||||
where
|
||||
addRef = TcM (\abstr ms -> case IntMap.lookup i ms of
|
||||
Just (MGuarded e cs x) -> Ok (IntMap.insert i (MGuarded e cs (x+1)) ms) ())
|
||||
addRef = TcM (\abstr s ms -> case IntMap.lookup i ms of
|
||||
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
|
||||
Just (MGuarded e cs x) -> if x == 1
|
||||
then unTcM (sequence_ [c e | c <- cs]) abstr (IntMap.insert i (MGuarded e [] 0) ms)
|
||||
else Ok (IntMap.insert i (MGuarded e cs (x-1)) ms) ())
|
||||
release = TcM (\abstr s ms -> case IntMap.lookup i ms of
|
||||
Just (MGuarded e cs x) -> if x == 1
|
||||
then unTcM (sequence_ [c e | c <- cs]) abstr s (IntMap.insert i (MGuarded e [] 0) ms)
|
||||
else Ok s (IntMap.insert i (MGuarded e cs (x-1)) ms) ())
|
||||
|
||||
-----------------------------------------------------
|
||||
-- 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 $$
|
||||
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
|
||||
-----------------------------------------------------
|
||||
@@ -213,11 +266,11 @@ ppTcError (UnsolvableGoal xs metaid ty)= text "The goal:" <+> ppMeta metaid <+>
|
||||
-- syntax of the grammar.
|
||||
checkType :: PGF -> Type -> Either TcError Type
|
||||
checkType pgf ty =
|
||||
case unTcM (tcType emptyScope ty >>= refineType) (abstract pgf) emptyMetaStore of
|
||||
Ok ms ty -> Right ty
|
||||
Fail err -> Left err
|
||||
case unTcM (tcType emptyScope ty >>= refineType) (abstract pgf) () emptyMetaStore of
|
||||
Ok s ms ty -> Right ty
|
||||
Fail err -> Left err
|
||||
|
||||
tcType :: Scope -> Type -> TcM Type
|
||||
tcType :: Scope -> Type -> TcM s Type
|
||||
tcType scope ty@(DTyp hyps cat es) = do
|
||||
(scope,hyps) <- tcHypos scope hyps
|
||||
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
|
||||
return (DTyp hyps cat es)
|
||||
|
||||
tcHypos :: Scope -> [Hypo] -> TcM (Scope,[Hypo])
|
||||
tcHypos :: Scope -> [Hypo] -> TcM s (Scope,[Hypo])
|
||||
tcHypos scope [] = return (scope,[])
|
||||
tcHypos scope (h:hs) = do
|
||||
(scope,h ) <- tcHypo scope h
|
||||
(scope,hs) <- tcHypos scope hs
|
||||
return (scope,h:hs)
|
||||
|
||||
tcHypo :: Scope -> Hypo -> TcM (Scope,Hypo)
|
||||
tcHypo :: Scope -> Hypo -> TcM s (Scope,Hypo)
|
||||
tcHypo scope (b,x,ty) = do
|
||||
ty <- tcType scope ty
|
||||
if x == wildCId
|
||||
@@ -275,11 +328,11 @@ checkExpr pgf e ty =
|
||||
case unTcM (do e <- tcExpr emptyScope e (TTyp [] ty)
|
||||
e <- refineExpr e
|
||||
checkResolvedMetaStore emptyScope e
|
||||
return e) (abstract pgf) emptyMetaStore of
|
||||
Ok ms e -> Right e
|
||||
Fail err -> Left err
|
||||
return e) (abstract pgf) () emptyMetaStore of
|
||||
Ok _ ms e -> Right e
|
||||
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 =
|
||||
case tty of
|
||||
TTyp delta (DTyp ((Implicit,y,ty):hs) c es) -> do e <- if y == wildCId
|
||||
@@ -331,11 +384,11 @@ inferExpr pgf e =
|
||||
e <- refineExpr e
|
||||
checkResolvedMetaStore emptyScope e
|
||||
ty <- evalType 0 tty
|
||||
return (e,ty)) (abstract pgf) emptyMetaStore of
|
||||
Ok ms (e,ty) -> Right (e,ty)
|
||||
Fail err -> Left err
|
||||
return (e,ty)) (abstract pgf) () emptyMetaStore of
|
||||
Ok _ ms (e,ty) -> Right (e,ty)
|
||||
Fail err -> Left err
|
||||
|
||||
infExpr :: Scope -> Expr -> TcM (Expr,TType)
|
||||
infExpr :: Scope -> Expr -> TcM s (Expr,TType)
|
||||
infExpr scope e0@(EApp e1 e2) = do
|
||||
(e1,TTyp delta ty) <- infExpr scope e1
|
||||
(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
|
||||
case lookupVar x scope of
|
||||
Just (i,tty) -> return (EVar i,tty)
|
||||
Nothing -> do tty <- lookupFunType x
|
||||
return (e0,tty)
|
||||
Nothing -> do ty <- lookupFunType x
|
||||
return (e0,TTyp [] ty)
|
||||
infExpr scope e0@(EVar i) = do
|
||||
return (e0,snd (getVar i scope))
|
||||
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 :: 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))
|
||||
| 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
|
||||
where
|
||||
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)
|
||||
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 [] =
|
||||
return (k,delta1,delta2)
|
||||
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
|
||||
eqHyps k delta1 h1s delta2 h2s = raiseTypeMatchError
|
||||
|
||||
eqExpr :: Int -> Env -> Expr -> Env -> Expr -> TcM ()
|
||||
eqExpr k env1 e1 env2 e2 = do
|
||||
v1 <- eval env1 e1
|
||||
v2 <- eval env2 e2
|
||||
eqValue k v1 v2
|
||||
|
||||
eqValue :: Int -> Value -> Value -> TcM ()
|
||||
eqValue k v1 v2 = do
|
||||
v1 <- deRef v1
|
||||
v2 <- deRef v2
|
||||
eqValue' k v1 v2
|
||||
eqExpr :: (forall a . TcM s a) -> (MetaId -> (Expr -> TcM s ()) -> TcM s ()) -> Int -> Env -> Expr -> Env -> Expr -> TcM s ()
|
||||
eqExpr fail suspend k env1 e1 env2 e2 = do
|
||||
v1 <- eval env1 e1
|
||||
v2 <- eval env2 e2
|
||||
eqValue fail suspend k v1 v2
|
||||
|
||||
eqValue :: (forall a . TcM s a) -> (MetaId -> (Expr -> TcM s ()) -> TcM s ()) -> Int -> Value -> Value -> TcM s ()
|
||||
eqValue fail suspend k v1 v2 = do
|
||||
v1 <- deRef v1
|
||||
v2 <- deRef v2
|
||||
eqValue' k v1 v2
|
||||
where
|
||||
deRef v@(VMeta i env vs) = do
|
||||
mv <- getMeta i
|
||||
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
|
||||
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 v1 (VSusp i env vs2 c) = addConstraint i0 i env vs2 (\v2 -> eqValue k v1 (c v2))
|
||||
eqValue' k (VMeta i env1 vs1) (VMeta j env2 vs2) | i == j = zipWithM_ (eqValue k) vs1 vs2
|
||||
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) = 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 fail suspend k) vs1 vs2
|
||||
eqValue' k (VMeta i env1 vs1) v2 = do mv <- getMeta i
|
||||
case mv of
|
||||
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)
|
||||
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)
|
||||
eqValue' k (VApp f1 vs1) (VApp f2 vs2) | f1 == f2 = zipWithM_ (eqValue k) vs1 vs2
|
||||
eqValue' k (VConst f1 vs1) (VConst 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 fail suspend k) vs1 vs2
|
||||
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 []
|
||||
in eqExpr (k+1) (v:env1) e1 (v:env2) e2
|
||||
eqValue' k v1 v2 = raiseTypeMatchError
|
||||
in eqExpr fail suspend (k+1) (v:env1) e1 (v:env2) e2
|
||||
eqValue' k v1 v2 = fail
|
||||
|
||||
mkLam i scope env vs0 v = do
|
||||
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]
|
||||
if length vs == length xs
|
||||
then return ()
|
||||
else raiseTypeMatchError
|
||||
else fail
|
||||
v <- occurCheck i k xs v
|
||||
e <- value2expr (length xs) v
|
||||
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)
|
||||
occurCheck i0 k xs (VLit l) = return (VLit l)
|
||||
occurCheck i0 k xs (VMeta i env vs) = do if i == i0
|
||||
then raiseTypeMatchError
|
||||
then fail
|
||||
else return ()
|
||||
mv <- getMeta i
|
||||
case mv of
|
||||
MBound 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
|
||||
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)
|
||||
occurCheck i0 k xs (VGen i vs) = case List.findIndex (==i) xs of
|
||||
Just i -> do vs <- mapM (occurCheck i0 k xs) vs
|
||||
return (VGen i vs)
|
||||
Nothing -> raiseTypeMatchError
|
||||
Nothing -> fail
|
||||
occurCheck i0 k xs (VConst f vs) = do vs <- mapM (occurCheck i0 k xs) vs
|
||||
return (VConst f vs)
|
||||
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
|
||||
-----------------------------------------------------------
|
||||
|
||||
checkResolvedMetaStore :: Scope -> Expr -> TcM ()
|
||||
checkResolvedMetaStore scope e = TcM (\abstr ms ->
|
||||
checkResolvedMetaStore :: Scope -> Expr -> TcM s ()
|
||||
checkResolvedMetaStore scope e = TcM (\abstr s ms ->
|
||||
let xs = [i | (i,mv) <- IntMap.toList ms, not (isResolved mv)]
|
||||
in if List.null xs
|
||||
then Ok ms ()
|
||||
then Ok s ms ()
|
||||
else Fail (UnresolvedMetaVars (scopeVars scope) e xs))
|
||||
where
|
||||
isResolved (MUnbound _ _ []) = True
|
||||
@@ -516,7 +569,7 @@ checkResolvedMetaStore scope e = TcM (\abstr ms ->
|
||||
-- evalType
|
||||
-----------------------------------------------------
|
||||
|
||||
evalType :: Int -> TType -> TcM Type
|
||||
evalType :: Int -> TType -> TcM s Type
|
||||
evalType k (TTyp delta ty) = evalTy funs k delta ty
|
||||
where
|
||||
evalTy sig k delta (DTyp hyps cat es) = do
|
||||
@@ -537,8 +590,8 @@ evalType k (TTyp delta ty) = evalTy funs k delta ty
|
||||
-- refinement
|
||||
-----------------------------------------------------
|
||||
|
||||
refineExpr :: Expr -> TcM Expr
|
||||
refineExpr e = TcM (\abstr ms -> Ok ms (refineExpr_ ms e))
|
||||
refineExpr :: Expr -> TcM s Expr
|
||||
refineExpr e = TcM (\abstr s ms -> Ok s ms (refineExpr_ ms e))
|
||||
|
||||
refineExpr_ ms e = refine e
|
||||
where
|
||||
@@ -554,16 +607,16 @@ refineExpr_ ms e = refine e
|
||||
refine (ETyped e ty) = ETyped (refine e) (refineType_ ms ty)
|
||||
refine (EImplArg e) = EImplArg (refine e)
|
||||
|
||||
refineType :: Type -> TcM Type
|
||||
refineType ty = TcM (\abstr ms -> Ok ms (refineType_ ms ty))
|
||||
refineType :: Type -> TcM s Type
|
||||
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)
|
||||
|
||||
eval :: Env -> Expr -> TcM Value
|
||||
eval env e = TcM (\abstr ms -> Ok ms (Expr.eval (funs abstr,lookupMeta ms) env e))
|
||||
eval :: Env -> Expr -> TcM s Value
|
||||
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 e vs = TcM (\abstr ms -> Ok ms (Expr.apply (funs abstr,lookupMeta ms) env e vs))
|
||||
apply :: Env -> Expr -> [Value] -> TcM s Value
|
||||
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 i v = TcM (\abstr ms -> Ok ms (Expr.value2expr (funs abstr,lookupMeta ms) i v))
|
||||
value2expr :: Int -> Value -> TcM s Expr
|
||||
value2expr i v = TcM (\abstr s ms -> Ok s ms (Expr.value2expr (funs abstr,lookupMeta ms) i v))
|
||||
|
||||
@@ -35,3 +35,7 @@ executable pgf-server
|
||||
ghc-options: -threaded
|
||||
if os(windows)
|
||||
ghc-options: -optl-mwindows
|
||||
|
||||
executable content-server
|
||||
build-depends: base >=4.2 && <5
|
||||
main-is: ContentService.hs
|
||||
|
||||
@@ -53,6 +53,36 @@ public class JSONRequestBuilder {
|
||||
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) /*-{
|
||||
return eval('(' + json + ')');
|
||||
}-*/;
|
||||
|
||||
Reference in New Issue
Block a user