Skip to content

Commit 3444816

Browse files
krangelovkrangelov
committed
the pure evaluator
1 parent 364c8c0 commit 3444816

File tree

6 files changed

+1507
-631
lines changed

6 files changed

+1507
-631
lines changed

‎src/compiler/api/GF/Compile/Compute/Concrete.hs‎

Lines changed: 75 additions & 74 deletions
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,7 @@ module GF.Compile.Compute.Concrete
88
, PredefImpl, Predef(..), PredefCombinator, ($\)
99
, pdForce, pdClosedArgs, pdArity, pdStandard
1010
, MetaThunks, Constraint, PredefTable, Globals(..), ConstValue(..)
11-
, EvalM(..), runEvalM, runEvalOneM, reset, evalError, evalWarn
11+
, EvalM(..), runEvalM, runEvalOneM, reset, try, evalError, evalWarn
1212
, eval, apply, force, value2term, patternMatch, stdPredef
1313
, unsafeIOToEvalM
1414
, newThunk, newEvaluatedThunk
@@ -19,7 +19,6 @@ module GF.Compile.Compute.Concrete
1919
) where
2020

2121
import Prelude hiding ((<>)) -- GHC 8.4.1 clash with Text.PrettyPrint
22-
2322
import GF.Grammar hiding (Env, VGen, VApp, VRecType)
2423
import GF.Grammar.Lookup(lookupResDef,lookupResType,
2524
lookupOrigInfo,lookupOverloadTypes,
@@ -117,7 +116,6 @@ data Value s
117116
| VCRecType [(Label, Bool, Constraint s)]
118117
| VCInts (Maybe Integer) (Maybe Integer)
119118

120-
121119
showValue (VApp q tnks) = "(VApp "++unwords (show q : map (const "_") tnks) ++ ")"
122120
showValue (VMeta _ _) = "VMeta"
123121
showValue (VSusp _ _ _) = "VSusp"
@@ -504,30 +502,30 @@ vtableSelect v0 ty tnks tnk2 vs = do
504502
"cannot be evaluated at compile time.")
505503

506504

507-
susp i ki = EvalM $ \globals@(Gl gr _) k mt d r msgs -> do
505+
susp i ki = EvalM $ \globals@(Gl gr _) k e mt d r msgs -> do
508506
s <- readSTRef i
509507
case s of
510508
Narrowing id (QC q) -> case lookupOrigInfo gr q of
511-
Ok (m,ResParam (Just (L _ ps)) _) -> bindParam globals k mt d r msgs s m ps
509+
Ok (m,ResParam (Just (L _ ps)) _) -> bindParam globals k e mt d r msgs s m ps
512510
Bad msg -> return (Fail (pp msg) msgs)
513511
Narrowing id ty
514512
| Just max <- isTypeInts ty
515-
-> bindInt globals k mt d r msgs s 0 max
513+
-> bindInt globals k e mt d r msgs s 0 max
516514
Evaluated _ v -> case ki v of
517-
EvalM f -> f globals k mt d r msgs
515+
EvalM f -> f globals k e mt d r msgs
518516
_ -> k (VSusp i ki []) mt d r msgs
519517
where
520-
bindParam gr k mt d r msgs s m [] = return (Success r msgs)
521-
bindParam gr k mt d r msgs s m ((p, ctxt):ps) = do
518+
bindParam gr k e mt d r msgs s m [] = return (Success r msgs)
519+
bindParam gr k e mt d r msgs s m ((p, ctxt):ps) = do
522520
(mt',tnks) <- mkArgs mt ctxt
523521
let v = VApp (m,p) tnks
524522
writeSTRef i (Evaluated 0 v)
525523
res <- case ki v of
526-
EvalM f -> f gr k mt' d r msgs
524+
EvalM f -> f gr k e mt' d r msgs
527525
writeSTRef i s
528526
case res of
529527
Fail msg msgs -> return (Fail msg msgs)
530-
Success r msgs -> bindParam gr k mt d r msgs s m ps
528+
Success r msgs -> bindParam gr k e mt d r msgs s m ps
531529

532530
mkArgs mt [] = return (mt,[])
533531
mkArgs mt ((_,_,ty):ctxt) = do
@@ -538,16 +536,16 @@ susp i ki = EvalM $ \globals@(Gl gr _) k mt d r msgs -> do
538536
(mt,tnks) <- mkArgs (Map.insert i tnk mt) ctxt
539537
return (mt,tnk:tnks)
540538

541-
bindInt gr k mt d r msgs s iv max
539+
bindInt gr k e mt d r msgs s iv max
542540
| iv <= max = do
543541
let v = VInt iv
544542
writeSTRef i (Evaluated 0 v)
545543
res <- case ki v of
546-
EvalM f -> f gr k mt d r msgs
544+
EvalM f -> f gr k e mt d r msgs
547545
writeSTRef i s
548546
case res of
549547
Fail msg msgs -> return (Fail msg msgs)
550-
Success r msgs -> bindInt gr k mt d r msgs s (iv+1) max
548+
Success r msgs -> bindInt gr k e mt d r msgs s (iv+1) max
551549
| otherwise = return (Success r msgs)
552550

553551

@@ -825,122 +823,122 @@ pdStandard n = pdArity n . pdForce . pdClosedArgs
825823
-- * Evaluation monad
826824

827825
type MetaThunks s = Map.Map MetaId (Thunk s)
828-
type Cont s r = MetaThunks s -> Int -> r -> [Message] -> ST s (CheckResult r [Message])
826+
type Do s r = [Message] -> ST s (CheckResult r [Message])
827+
type Cont s r = MetaThunks s -> Int -> r -> Do s r
829828
type PredefTable s = Map.Map Ident (Predef (Thunk s) s)
830829
data Globals = Gl Grammar (forall s . PredefTable s)
831-
newtype EvalM s a = EvalM (forall r . Globals -> (a -> Cont s r) -> Cont s r)
830+
newtype EvalM s a = EvalM (forall r . Globals -> (a -> Cont s r) -> (Message -> Do s r) -> Cont s r)
832831

833832
instance Functor (EvalM s) where
834-
fmap f (EvalM g) = EvalM (\gr k -> g gr (k . f))
833+
fmap f (EvalM g) = EvalM (\gr k e -> g gr (k . f) e)
835834

836835
instance Applicative (EvalM s) where
837-
pure x = EvalM (\gr k -> k x)
838-
(EvalM f) <*> (EvalM x) = EvalM (\gr k -> f gr (\f -> x gr (\x -> k (f x))))
836+
pure x = EvalM (\gr k e -> k x)
837+
(EvalM f) <*> (EvalM x) = EvalM (\gr k e -> f gr (\f -> x gr (\x -> k (f x)) e) e)
839838

840839
instance Monad (EvalM s) where
841-
(EvalM f) >>= g = EvalM (\gr k -> f gr (\x -> case g x of
842-
EvalM g -> g gr k))
843-
#if !(MIN_VERSION_base(4,13,0))
844-
-- Monad(fail) will be removed in GHC 8.8+
845-
fail = Fail.fail
846-
#endif
840+
(EvalM f) >>= g = EvalM (\gr k e -> f gr (\x -> case g x of
841+
EvalM g -> g gr k e) e)
847842

848843
instance Fail.MonadFail (EvalM s) where
849-
fail msg = EvalM (\gr k _ _ r msgs -> return (Fail (pp msg) msgs))
844+
fail msg = EvalM (\gr k e _ _ r -> e (pp msg))
850845

851846
instance Alternative (EvalM s) where
852-
empty = EvalM (\gr k _ _ r msgs -> return (Success r msgs))
853-
(EvalM f) <|> (EvalM g) = EvalM $ \gr k mt b r msgs -> do
854-
res <- f gr k mt b r msgs
847+
empty = EvalM (\gr k e _ _ r msgs -> return (Success r msgs))
848+
(EvalM f) <|> (EvalM g) = EvalM $ \gr k e mt b r msgs -> do
849+
res <- f gr k e mt b r msgs
855850
case res of
856851
Fail msg msgs -> return (Fail msg msgs)
857-
Success r msgs -> g gr k mt b r msgs
852+
Success r msgs -> g gr k e mt b r msgs
858853

859854
instance MonadPlus (EvalM s) where
860855

861856
runEvalM :: Globals -> (forall s . EvalM s a) -> Check [a]
862857
runEvalM gr f = Check $ \(es,ws) ->
863858
case runST (case f of
864-
EvalM f -> f gr (\x mt _ xs ws -> return (Success (x:xs) ws)) Map.empty maxBound [] ws) of
859+
EvalM f -> f gr (\x mt _ xs ws -> return (Success (x:xs) ws)) (\msg ws -> return (Fail msg ws)) Map.empty maxBound [] ws) of
865860
Fail msg ws -> Fail msg (es,ws)
866861
Success xs ws -> Success (reverse xs) (es,ws)
867862

868-
runEvalOneM :: Globals -> (forall s . EvalM s a) -> Check a
863+
runEvalOneM :: Globals -> (forall s . EvalM s (Term,Type)) -> Check (Term,Type)
869864
runEvalOneM gr f = Check $ \(es,ws) ->
870865
case runST (case f of
871-
EvalM f -> f gr (\x mt _ xs ws -> return (Success (x:xs) ws)) Map.empty maxBound [] ws) of
866+
EvalM f -> f gr (\x mt _ xs ws -> return (Success (x:xs) ws)) (\msg ws -> return (Fail msg ws)) Map.empty maxBound [] ws) of
872867
Fail msg ws -> Fail msg (es,ws)
873868
Success [] ws -> Fail (pp "The evaluation produced no results") (es,ws)
874-
Success (x:_) ws -> Success x (es,ws)
869+
Success xs ws -> Success (FV (map fst xs),snd (head xs)) (es,ws)
875870

876871
reset :: EvalM s a -> EvalM s [a]
877-
reset (EvalM f) = EvalM $ \gl k mt d r ws -> do
878-
res <- f gl (\x mt d xs ws -> return (Success (x:xs) ws)) mt d [] ws
872+
reset (EvalM f) = EvalM $ \gl k e mt d r ws -> do
873+
res <- f gl (\x mt d xs ws -> return (Success (x:xs) ws)) (\msg ws -> return (Fail msg ws)) mt d [] ws
879874
case res of
880-
Fail msg ws -> return (Fail msg ws)
875+
Fail msg ws -> e msg ws
881876
Success xs ws -> k (reverse xs) mt d r ws
882877

878+
try :: EvalM s a -> EvalM s a -> EvalM s a
879+
try (EvalM f) (EvalM g) = EvalM (\gl k e mt d r ws -> f gl k (\msg _ -> g gl k e mt d r ws) mt d r ws)
880+
883881
evalError :: Message -> EvalM s a
884-
evalError msg = EvalM (\gr k _ _ r msgs -> return (Fail msg msgs))
882+
evalError msg = EvalM (\gr k e _ _ r ws -> e msg ws)
885883

886884
evalWarn :: Message -> EvalM s ()
887-
evalWarn msg = EvalM (\gr k mt d r msgs -> k () mt d r (msg:msgs))
885+
evalWarn msg = EvalM (\gr k e mt d r msgs -> k () mt d r (msg:msgs))
888886

889887
evalPredef :: Env s -> Term -> Ident -> [Thunk s] -> EvalM s (ConstValue (Value s))
890-
evalPredef env h id args = EvalM (\globals@(Gl _ predef) k mt d r msgs ->
888+
evalPredef env h id args = EvalM (\globals@(Gl _ predef) k e mt d r msgs ->
891889
case fmap (\def -> runPredef def h env args) (Map.lookup id predef) of
892-
Just (EvalM f) -> f globals k mt d r msgs
890+
Just (EvalM f) -> f globals k e mt d r msgs
893891
Nothing -> k RunTime mt d r msgs)
894892

895893
getResDef :: QIdent -> EvalM s Term
896-
getResDef q = EvalM $ \(Gl gr _) k mt d r msgs -> do
894+
getResDef q = EvalM $ \(Gl gr _) k e mt d r msgs -> do
897895
case lookupResDef gr q of
898896
Ok t -> k t mt d r msgs
899-
Bad msg -> return (Fail (pp msg) msgs)
897+
Bad msg -> e (pp msg) msgs
900898

901899
getInfo :: QIdent -> EvalM s (ModuleName,Info)
902-
getInfo q = EvalM $ \(Gl gr _) k mt d r msgs -> do
900+
getInfo q = EvalM $ \(Gl gr _) k e mt d r msgs -> do
903901
case lookupOrigInfo gr q of
904902
Ok res -> k res mt d r msgs
905-
Bad msg -> return (Fail (pp msg) msgs)
903+
Bad msg -> e (pp msg) msgs
906904

907905
getResType :: QIdent -> EvalM s Type
908-
getResType q = EvalM $ \(Gl gr _) k mt d r msgs -> do
906+
getResType q = EvalM $ \(Gl gr _) k e mt d r msgs -> do
909907
case lookupResType gr q of
910908
Ok t -> k t mt d r msgs
911-
Bad msg -> return (Fail (pp msg) msgs)
909+
Bad msg -> e (pp msg) msgs
912910

913911
getOverload :: Term -> QIdent -> EvalM s (Term,Type)
914-
getOverload t q = EvalM $ \(Gl gr _) k mt d r msgs -> do
912+
getOverload t q = EvalM $ \(Gl gr _) k e mt d r msgs -> do
915913
case lookupOverloadTypes gr q of
916914
Ok ttys -> let err = "Overload resolution failed" $$
917915
"of term " <+> pp t $$
918916
"with types" <+> vcat [ppTerm Terse 0 ty | (_,ty) <- ttys]
919917

920-
go [] = return (Fail err msgs)
921-
go (tty:ttys) = do res <- k tty mt d r msgs
922-
case res of
923-
Fail _ _ -> go ttys
924-
Success r msgs -> return (Success r msgs)
918+
go r [] = return (Success r msgs)
919+
go r (tty:ttys) = do res <- k tty mt d r msgs
920+
case res of
921+
Fail _ _ -> go r ttys
922+
Success r msgs -> go r ttys
925923

926-
in go ttys
927-
Bad msg -> return (Fail (pp msg) msgs)
924+
in go r ttys
925+
Bad msg -> e (pp msg) msgs
928926

929927
getAllParamValues :: Type -> EvalM s [Term]
930-
getAllParamValues ty = EvalM $ \(Gl gr _) k mt d r msgs ->
928+
getAllParamValues ty = EvalM $ \(Gl gr _) k e mt d r msgs ->
931929
case allParamValues gr ty of
932930
Ok ts -> k ts mt d r msgs
933-
Bad msg -> return (Fail (pp msg) msgs)
931+
Bad msg -> e (pp msg) msgs
934932

935-
newThunk env t = EvalM $ \gr k mt d r msgs -> do
933+
newThunk env t = EvalM $ \gr k e mt d r msgs -> do
936934
tnk <- newSTRef (Unevaluated env t)
937935
k tnk mt d r msgs
938936

939-
newEvaluatedThunk v = EvalM $ \gr k mt d r msgs -> do
937+
newEvaluatedThunk v = EvalM $ \gr k e mt d r msgs -> do
940938
tnk <- newSTRef (Evaluated maxBound v)
941939
k tnk mt d r msgs
942940

943-
newHole i = EvalM $ \gr k mt d r msgs ->
941+
newHole i = EvalM $ \gr k e mt d r msgs ->
944942
if i == 0
945943
then do tnk <- newSTRef (Hole i)
946944
k tnk mt d r msgs
@@ -949,22 +947,22 @@ newHole i = EvalM $ \gr k mt d r msgs ->
949947
Nothing -> do tnk <- newSTRef (Hole i)
950948
k tnk (Map.insert i tnk mt) d r msgs
951949

952-
newResiduation scope = EvalM $ \gr k mt d r msgs -> do
950+
newResiduation scope = EvalM $ \gr k e mt d r msgs -> do
953951
let i = Map.size mt + 1
954952
tnk <- newSTRef (Residuation i scope Nothing)
955953
k (i,tnk) (Map.insert i tnk mt) d r msgs
956954

957-
newNarrowing ty = EvalM $ \gr k mt d r msgs -> do
955+
newNarrowing ty = EvalM $ \gr k e mt d r msgs -> do
958956
let i = Map.size mt + 1
959957
tnk <- newSTRef (Narrowing i ty)
960958
k (i,tnk) (Map.insert i tnk mt) d r msgs
961959

962-
withVar d0 (EvalM f) = EvalM $ \gr k mt d1 r msgs ->
960+
withVar d0 (EvalM f) = EvalM $ \gr k e mt d1 r msgs ->
963961
let !d = min d0 d1
964-
in f gr k mt d r msgs
962+
in f gr k e mt d r msgs
965963

966964
getVariables :: EvalM s [(LVar,LIndex)]
967-
getVariables = EvalM $ \(Gl gr _) k mt d ws r -> do
965+
getVariables = EvalM $ \(Gl gr _) k e mt d ws r -> do
968966
ps <- metas2params gr (Map.elems mt)
969967
k ps mt d ws r
970968
where
@@ -981,30 +979,30 @@ getVariables = EvalM $ \(Gl gr _) k mt d ws r -> do
981979
else return params
982980
_ -> metas2params gr tnks
983981

984-
getRef tnk = EvalM $ \gr k mt d r msgs -> readSTRef tnk >>= \st -> k st mt d r msgs
985-
setRef tnk st = EvalM $ \gr k mt d r msgs -> do
982+
getRef tnk = EvalM $ \gr k e mt d r msgs -> readSTRef tnk >>= \st -> k st mt d r msgs
983+
setRef tnk st = EvalM $ \gr k e mt d r msgs -> do
986984
old <- readSTRef tnk
987985
writeSTRef tnk st
988986
res <- k () mt d r msgs
989987
writeSTRef tnk old
990988
return res
991989

992-
force tnk = EvalM $ \gr k mt d r msgs -> do
990+
force tnk = EvalM $ \gr k e mt d r msgs -> do
993991
s <- readSTRef tnk
994992
case s of
995993
Unevaluated env t -> case eval env t [] of
996994
EvalM f -> f gr (\v mt b r msgs -> do let d = length env
997995
writeSTRef tnk (Evaluated d v)
998996
r <- k v mt d r msgs
999997
writeSTRef tnk s
1000-
return r) mt d r msgs
998+
return r) e mt d r msgs
1001999
Evaluated d v -> k v mt d r msgs
10021000
Hole _ -> k (VMeta tnk []) mt d r msgs
10031001
Residuation _ _ _ -> k (VMeta tnk []) mt d r msgs
10041002
Narrowing _ _ -> k (VMeta tnk []) mt d r msgs
10051003

10061004
tnk2term True xs tnk = force tnk >>= value2term True xs
1007-
tnk2term False xs tnk = EvalM $ \gr k mt d r msgs ->
1005+
tnk2term False xs tnk = EvalM $ \gr k e mt d r msgs ->
10081006
let join f g = do res <- f
10091007
case res of
10101008
Fail msg msgs -> return (Fail msg msgs)
@@ -1018,21 +1016,23 @@ tnk2term False xs tnk = EvalM $ \gr k mt d r msgs ->
10181016
| d < d0 = flush xs (\mt r msgs -> join (k x mt d r msgs) (\r msgs -> return (Success (r,c+1,[]) msgs))) mt r msgs
10191017
| otherwise = return (Success (r,c+1,x:xs) msgs)
10201018

1019+
err msg msgs = return (Fail msg msgs)
1020+
10211021
in do s <- readSTRef tnk
10221022
case s of
10231023
Unevaluated env t -> do let d0 = length env
10241024
res <- case eval env t [] of
10251025
EvalM f -> f gr (\v mt d msgs r -> do writeSTRef tnk (Evaluated d0 v)
10261026
r <- case value2term False xs v of
1027-
EvalM f -> f gr (acc d0) mt d msgs r
1027+
EvalM f -> f gr (acc d0) err mt d msgs r
10281028
writeSTRef tnk s
1029-
return r) mt maxBound (r,0,[]) msgs
1029+
return r) err mt maxBound (r,0,[]) msgs
10301030
case res of
10311031
Fail msg msgs -> return (Fail msg msgs)
10321032
Success (r,0,xs) msgs -> k (FV []) mt d r msgs
10331033
Success (r,c,xs) msgs -> flush xs (\mt msgs r -> return (Success msgs r)) mt r msgs
10341034
Evaluated d0 v -> do res <- case value2term False xs v of
1035-
EvalM f -> f gr (acc d0) mt maxBound (r,0,[]) msgs
1035+
EvalM f -> f gr (acc d0) err mt maxBound (r,0,[]) msgs
10361036
case res of
10371037
Fail msg msgs -> return (Fail msg msgs)
10381038
Success (r,0,xs) msgs -> k (FV []) mt d r msgs
@@ -1045,4 +1045,5 @@ scopeEnv scope = zipWithM (\x i -> newEvaluatedThunk (VGen i []) >>= \tnk -> r
10451045

10461046

10471047
unsafeIOToEvalM :: IO a -> EvalM s a
1048-
unsafeIOToEvalM f = EvalM (\gr k mt d r msgs -> unsafeIOToST f >>= \x -> k x mt d r msgs)
1048+
unsafeIOToEvalM f = EvalM (\gr k e mt d r msgs -> unsafeIOToST f >>= \x -> k x mt d r msgs)
1049+

0 commit comments

Comments
 (0)