mirror of
https://github.com/GrammaticalFramework/gf-core.git
synced 2026-04-23 03:32:51 -06:00
the pure evaluator
This commit is contained in:
Krasimir Angelov
@@ -8,7 +8,7 @@ module GF.Compile.Compute.Concrete
|
||||
, PredefImpl, Predef(..), PredefCombinator, ($\)
|
||||
, pdForce, pdClosedArgs, pdArity, pdStandard
|
||||
, MetaThunks, Constraint, PredefTable, Globals(..), ConstValue(..)
|
||||
, EvalM(..), runEvalM, runEvalOneM, reset, evalError, evalWarn
|
||||
, EvalM(..), runEvalM, runEvalOneM, reset, try, evalError, evalWarn
|
||||
, eval, apply, force, value2term, patternMatch, stdPredef
|
||||
, unsafeIOToEvalM
|
||||
, newThunk, newEvaluatedThunk
|
||||
@@ -19,7 +19,6 @@ module GF.Compile.Compute.Concrete
|
||||
) where
|
||||
|
||||
import Prelude hiding ((<>)) -- GHC 8.4.1 clash with Text.PrettyPrint
|
||||
|
||||
import GF.Grammar hiding (Env, VGen, VApp, VRecType)
|
||||
import GF.Grammar.Lookup(lookupResDef,lookupResType,
|
||||
lookupOrigInfo,lookupOverloadTypes,
|
||||
@@ -117,7 +116,6 @@ data Value s
|
||||
| VCRecType [(Label, Bool, Constraint s)]
|
||||
| VCInts (Maybe Integer) (Maybe Integer)
|
||||
|
||||
|
||||
showValue (VApp q tnks) = "(VApp "++unwords (show q : map (const "_") tnks) ++ ")"
|
||||
showValue (VMeta _ _) = "VMeta"
|
||||
showValue (VSusp _ _ _) = "VSusp"
|
||||
@@ -504,30 +502,30 @@ vtableSelect v0 ty tnks tnk2 vs = do
|
||||
"cannot be evaluated at compile time.")
|
||||
|
||||
|
||||
susp i ki = EvalM $ \globals@(Gl gr _) k mt d r msgs -> do
|
||||
susp i ki = EvalM $ \globals@(Gl gr _) k e mt d r msgs -> do
|
||||
s <- readSTRef i
|
||||
case s of
|
||||
Narrowing id (QC q) -> case lookupOrigInfo gr q of
|
||||
Ok (m,ResParam (Just (L _ ps)) _) -> bindParam globals k mt d r msgs s m ps
|
||||
Ok (m,ResParam (Just (L _ ps)) _) -> bindParam globals k e mt d r msgs s m ps
|
||||
Bad msg -> return (Fail (pp msg) msgs)
|
||||
Narrowing id ty
|
||||
| Just max <- isTypeInts ty
|
||||
-> bindInt globals k mt d r msgs s 0 max
|
||||
-> bindInt globals k e mt d r msgs s 0 max
|
||||
Evaluated _ v -> case ki v of
|
||||
EvalM f -> f globals k mt d r msgs
|
||||
EvalM f -> f globals k e mt d r msgs
|
||||
_ -> k (VSusp i ki []) mt d r msgs
|
||||
where
|
||||
bindParam gr k mt d r msgs s m [] = return (Success r msgs)
|
||||
bindParam gr k mt d r msgs s m ((p, ctxt):ps) = do
|
||||
bindParam gr k e mt d r msgs s m [] = return (Success r msgs)
|
||||
bindParam gr k e mt d r msgs s m ((p, ctxt):ps) = do
|
||||
(mt',tnks) <- mkArgs mt ctxt
|
||||
let v = VApp (m,p) tnks
|
||||
writeSTRef i (Evaluated 0 v)
|
||||
res <- case ki v of
|
||||
EvalM f -> f gr k mt' d r msgs
|
||||
EvalM f -> f gr k e mt' d r msgs
|
||||
writeSTRef i s
|
||||
case res of
|
||||
Fail msg msgs -> return (Fail msg msgs)
|
||||
Success r msgs -> bindParam gr k mt d r msgs s m ps
|
||||
Success r msgs -> bindParam gr k e mt d r msgs s m ps
|
||||
|
||||
mkArgs mt [] = return (mt,[])
|
||||
mkArgs mt ((_,_,ty):ctxt) = do
|
||||
@@ -538,16 +536,16 @@ susp i ki = EvalM $ \globals@(Gl gr _) k mt d r msgs -> do
|
||||
(mt,tnks) <- mkArgs (Map.insert i tnk mt) ctxt
|
||||
return (mt,tnk:tnks)
|
||||
|
||||
bindInt gr k mt d r msgs s iv max
|
||||
bindInt gr k e mt d r msgs s iv max
|
||||
| iv <= max = do
|
||||
let v = VInt iv
|
||||
writeSTRef i (Evaluated 0 v)
|
||||
res <- case ki v of
|
||||
EvalM f -> f gr k mt d r msgs
|
||||
EvalM f -> f gr k e mt d r msgs
|
||||
writeSTRef i s
|
||||
case res of
|
||||
Fail msg msgs -> return (Fail msg msgs)
|
||||
Success r msgs -> bindInt gr k mt d r msgs s (iv+1) max
|
||||
Success r msgs -> bindInt gr k e mt d r msgs s (iv+1) max
|
||||
| otherwise = return (Success r msgs)
|
||||
|
||||
|
||||
@@ -825,122 +823,122 @@ pdStandard n = pdArity n . pdForce . pdClosedArgs
|
||||
-- * Evaluation monad
|
||||
|
||||
type MetaThunks s = Map.Map MetaId (Thunk s)
|
||||
type Cont s r = MetaThunks s -> Int -> r -> [Message] -> ST s (CheckResult r [Message])
|
||||
type Do s r = [Message] -> ST s (CheckResult r [Message])
|
||||
type Cont s r = MetaThunks s -> Int -> r -> Do s r
|
||||
type PredefTable s = Map.Map Ident (Predef (Thunk s) s)
|
||||
data Globals = Gl Grammar (forall s . PredefTable s)
|
||||
newtype EvalM s a = EvalM (forall r . Globals -> (a -> Cont s r) -> Cont s r)
|
||||
newtype EvalM s a = EvalM (forall r . Globals -> (a -> Cont s r) -> (Message -> Do s r) -> Cont s r)
|
||||
|
||||
instance Functor (EvalM s) where
|
||||
fmap f (EvalM g) = EvalM (\gr k -> g gr (k . f))
|
||||
fmap f (EvalM g) = EvalM (\gr k e -> g gr (k . f) e)
|
||||
|
||||
instance Applicative (EvalM s) where
|
||||
pure x = EvalM (\gr k -> k x)
|
||||
(EvalM f) <*> (EvalM x) = EvalM (\gr k -> f gr (\f -> x gr (\x -> k (f x))))
|
||||
pure x = EvalM (\gr k e -> k x)
|
||||
(EvalM f) <*> (EvalM x) = EvalM (\gr k e -> f gr (\f -> x gr (\x -> k (f x)) e) e)
|
||||
|
||||
instance Monad (EvalM s) where
|
||||
(EvalM f) >>= g = EvalM (\gr k -> f gr (\x -> case g x of
|
||||
EvalM g -> g gr k))
|
||||
#if !(MIN_VERSION_base(4,13,0))
|
||||
-- Monad(fail) will be removed in GHC 8.8+
|
||||
fail = Fail.fail
|
||||
#endif
|
||||
(EvalM f) >>= g = EvalM (\gr k e -> f gr (\x -> case g x of
|
||||
EvalM g -> g gr k e) e)
|
||||
|
||||
instance Fail.MonadFail (EvalM s) where
|
||||
fail msg = EvalM (\gr k _ _ r msgs -> return (Fail (pp msg) msgs))
|
||||
fail msg = EvalM (\gr k e _ _ r -> e (pp msg))
|
||||
|
||||
instance Alternative (EvalM s) where
|
||||
empty = EvalM (\gr k _ _ r msgs -> return (Success r msgs))
|
||||
(EvalM f) <|> (EvalM g) = EvalM $ \gr k mt b r msgs -> do
|
||||
res <- f gr k mt b r msgs
|
||||
empty = EvalM (\gr k e _ _ r msgs -> return (Success r msgs))
|
||||
(EvalM f) <|> (EvalM g) = EvalM $ \gr k e mt b r msgs -> do
|
||||
res <- f gr k e mt b r msgs
|
||||
case res of
|
||||
Fail msg msgs -> return (Fail msg msgs)
|
||||
Success r msgs -> g gr k mt b r msgs
|
||||
Success r msgs -> g gr k e mt b r msgs
|
||||
|
||||
instance MonadPlus (EvalM s) where
|
||||
|
||||
runEvalM :: Globals -> (forall s . EvalM s a) -> Check [a]
|
||||
runEvalM gr f = Check $ \(es,ws) ->
|
||||
case runST (case f of
|
||||
EvalM f -> f gr (\x mt _ xs ws -> return (Success (x:xs) ws)) Map.empty maxBound [] ws) of
|
||||
EvalM f -> f gr (\x mt _ xs ws -> return (Success (x:xs) ws)) (\msg ws -> return (Fail msg ws)) Map.empty maxBound [] ws) of
|
||||
Fail msg ws -> Fail msg (es,ws)
|
||||
Success xs ws -> Success (reverse xs) (es,ws)
|
||||
|
||||
runEvalOneM :: Globals -> (forall s . EvalM s a) -> Check a
|
||||
runEvalOneM :: Globals -> (forall s . EvalM s (Term,Type)) -> Check (Term,Type)
|
||||
runEvalOneM gr f = Check $ \(es,ws) ->
|
||||
case runST (case f of
|
||||
EvalM f -> f gr (\x mt _ xs ws -> return (Success (x:xs) ws)) Map.empty maxBound [] ws) of
|
||||
EvalM f -> f gr (\x mt _ xs ws -> return (Success (x:xs) ws)) (\msg ws -> return (Fail msg ws)) Map.empty maxBound [] ws) of
|
||||
Fail msg ws -> Fail msg (es,ws)
|
||||
Success [] ws -> Fail (pp "The evaluation produced no results") (es,ws)
|
||||
Success (x:_) ws -> Success x (es,ws)
|
||||
Success xs ws -> Success (FV (map fst xs),snd (head xs)) (es,ws)
|
||||
|
||||
reset :: EvalM s a -> EvalM s [a]
|
||||
reset (EvalM f) = EvalM $ \gl k mt d r ws -> do
|
||||
res <- f gl (\x mt d xs ws -> return (Success (x:xs) ws)) mt d [] ws
|
||||
reset (EvalM f) = EvalM $ \gl k e mt d r ws -> do
|
||||
res <- f gl (\x mt d xs ws -> return (Success (x:xs) ws)) (\msg ws -> return (Fail msg ws)) mt d [] ws
|
||||
case res of
|
||||
Fail msg ws -> return (Fail msg ws)
|
||||
Fail msg ws -> e msg ws
|
||||
Success xs ws -> k (reverse xs) mt d r ws
|
||||
|
||||
try :: EvalM s a -> EvalM s a -> EvalM s a
|
||||
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)
|
||||
|
||||
evalError :: Message -> EvalM s a
|
||||
evalError msg = EvalM (\gr k _ _ r msgs -> return (Fail msg msgs))
|
||||
evalError msg = EvalM (\gr k e _ _ r ws -> e msg ws)
|
||||
|
||||
evalWarn :: Message -> EvalM s ()
|
||||
evalWarn msg = EvalM (\gr k mt d r msgs -> k () mt d r (msg:msgs))
|
||||
evalWarn msg = EvalM (\gr k e mt d r msgs -> k () mt d r (msg:msgs))
|
||||
|
||||
evalPredef :: Env s -> Term -> Ident -> [Thunk s] -> EvalM s (ConstValue (Value s))
|
||||
evalPredef env h id args = EvalM (\globals@(Gl _ predef) k mt d r msgs ->
|
||||
evalPredef env h id args = EvalM (\globals@(Gl _ predef) k e mt d r msgs ->
|
||||
case fmap (\def -> runPredef def h env args) (Map.lookup id predef) of
|
||||
Just (EvalM f) -> f globals k mt d r msgs
|
||||
Just (EvalM f) -> f globals k e mt d r msgs
|
||||
Nothing -> k RunTime mt d r msgs)
|
||||
|
||||
getResDef :: QIdent -> EvalM s Term
|
||||
getResDef q = EvalM $ \(Gl gr _) k mt d r msgs -> do
|
||||
getResDef q = EvalM $ \(Gl gr _) k e mt d r msgs -> do
|
||||
case lookupResDef gr q of
|
||||
Ok t -> k t mt d r msgs
|
||||
Bad msg -> return (Fail (pp msg) msgs)
|
||||
Bad msg -> e (pp msg) msgs
|
||||
|
||||
getInfo :: QIdent -> EvalM s (ModuleName,Info)
|
||||
getInfo q = EvalM $ \(Gl gr _) k mt d r msgs -> do
|
||||
getInfo q = EvalM $ \(Gl gr _) k e mt d r msgs -> do
|
||||
case lookupOrigInfo gr q of
|
||||
Ok res -> k res mt d r msgs
|
||||
Bad msg -> return (Fail (pp msg) msgs)
|
||||
Bad msg -> e (pp msg) msgs
|
||||
|
||||
getResType :: QIdent -> EvalM s Type
|
||||
getResType q = EvalM $ \(Gl gr _) k mt d r msgs -> do
|
||||
getResType q = EvalM $ \(Gl gr _) k e mt d r msgs -> do
|
||||
case lookupResType gr q of
|
||||
Ok t -> k t mt d r msgs
|
||||
Bad msg -> return (Fail (pp msg) msgs)
|
||||
Bad msg -> e (pp msg) msgs
|
||||
|
||||
getOverload :: Term -> QIdent -> EvalM s (Term,Type)
|
||||
getOverload t q = EvalM $ \(Gl gr _) k mt d r msgs -> do
|
||||
getOverload t q = EvalM $ \(Gl gr _) k e mt d r msgs -> do
|
||||
case lookupOverloadTypes gr q of
|
||||
Ok ttys -> let err = "Overload resolution failed" $$
|
||||
"of term " <+> pp t $$
|
||||
"with types" <+> vcat [ppTerm Terse 0 ty | (_,ty) <- ttys]
|
||||
|
||||
go [] = return (Fail err msgs)
|
||||
go (tty:ttys) = do res <- k tty mt d r msgs
|
||||
case res of
|
||||
Fail _ _ -> go ttys
|
||||
Success r msgs -> return (Success r msgs)
|
||||
go r [] = return (Success r msgs)
|
||||
go r (tty:ttys) = do res <- k tty mt d r msgs
|
||||
case res of
|
||||
Fail _ _ -> go r ttys
|
||||
Success r msgs -> go r ttys
|
||||
|
||||
in go ttys
|
||||
Bad msg -> return (Fail (pp msg) msgs)
|
||||
in go r ttys
|
||||
Bad msg -> e (pp msg) msgs
|
||||
|
||||
getAllParamValues :: Type -> EvalM s [Term]
|
||||
getAllParamValues ty = EvalM $ \(Gl gr _) k mt d r msgs ->
|
||||
getAllParamValues ty = EvalM $ \(Gl gr _) k e mt d r msgs ->
|
||||
case allParamValues gr ty of
|
||||
Ok ts -> k ts mt d r msgs
|
||||
Bad msg -> return (Fail (pp msg) msgs)
|
||||
Bad msg -> e (pp msg) msgs
|
||||
|
||||
newThunk env t = EvalM $ \gr k mt d r msgs -> do
|
||||
newThunk env t = EvalM $ \gr k e mt d r msgs -> do
|
||||
tnk <- newSTRef (Unevaluated env t)
|
||||
k tnk mt d r msgs
|
||||
|
||||
newEvaluatedThunk v = EvalM $ \gr k mt d r msgs -> do
|
||||
newEvaluatedThunk v = EvalM $ \gr k e mt d r msgs -> do
|
||||
tnk <- newSTRef (Evaluated maxBound v)
|
||||
k tnk mt d r msgs
|
||||
|
||||
newHole i = EvalM $ \gr k mt d r msgs ->
|
||||
newHole i = EvalM $ \gr k e mt d r msgs ->
|
||||
if i == 0
|
||||
then do tnk <- newSTRef (Hole i)
|
||||
k tnk mt d r msgs
|
||||
@@ -949,22 +947,22 @@ newHole i = EvalM $ \gr k mt d r msgs ->
|
||||
Nothing -> do tnk <- newSTRef (Hole i)
|
||||
k tnk (Map.insert i tnk mt) d r msgs
|
||||
|
||||
newResiduation scope = EvalM $ \gr k mt d r msgs -> do
|
||||
newResiduation scope = EvalM $ \gr k e mt d r msgs -> do
|
||||
let i = Map.size mt + 1
|
||||
tnk <- newSTRef (Residuation i scope Nothing)
|
||||
k (i,tnk) (Map.insert i tnk mt) d r msgs
|
||||
|
||||
newNarrowing ty = EvalM $ \gr k mt d r msgs -> do
|
||||
newNarrowing ty = EvalM $ \gr k e mt d r msgs -> do
|
||||
let i = Map.size mt + 1
|
||||
tnk <- newSTRef (Narrowing i ty)
|
||||
k (i,tnk) (Map.insert i tnk mt) d r msgs
|
||||
|
||||
withVar d0 (EvalM f) = EvalM $ \gr k mt d1 r msgs ->
|
||||
withVar d0 (EvalM f) = EvalM $ \gr k e mt d1 r msgs ->
|
||||
let !d = min d0 d1
|
||||
in f gr k mt d r msgs
|
||||
in f gr k e mt d r msgs
|
||||
|
||||
getVariables :: EvalM s [(LVar,LIndex)]
|
||||
getVariables = EvalM $ \(Gl gr _) k mt d ws r -> do
|
||||
getVariables = EvalM $ \(Gl gr _) k e mt d ws r -> do
|
||||
ps <- metas2params gr (Map.elems mt)
|
||||
k ps mt d ws r
|
||||
where
|
||||
@@ -981,15 +979,15 @@ getVariables = EvalM $ \(Gl gr _) k mt d ws r -> do
|
||||
else return params
|
||||
_ -> metas2params gr tnks
|
||||
|
||||
getRef tnk = EvalM $ \gr k mt d r msgs -> readSTRef tnk >>= \st -> k st mt d r msgs
|
||||
setRef tnk st = EvalM $ \gr k mt d r msgs -> do
|
||||
getRef tnk = EvalM $ \gr k e mt d r msgs -> readSTRef tnk >>= \st -> k st mt d r msgs
|
||||
setRef tnk st = EvalM $ \gr k e mt d r msgs -> do
|
||||
old <- readSTRef tnk
|
||||
writeSTRef tnk st
|
||||
res <- k () mt d r msgs
|
||||
writeSTRef tnk old
|
||||
return res
|
||||
|
||||
force tnk = EvalM $ \gr k mt d r msgs -> do
|
||||
force tnk = EvalM $ \gr k e mt d r msgs -> do
|
||||
s <- readSTRef tnk
|
||||
case s of
|
||||
Unevaluated env t -> case eval env t [] of
|
||||
@@ -997,14 +995,14 @@ force tnk = EvalM $ \gr k mt d r msgs -> do
|
||||
writeSTRef tnk (Evaluated d v)
|
||||
r <- k v mt d r msgs
|
||||
writeSTRef tnk s
|
||||
return r) mt d r msgs
|
||||
return r) e mt d r msgs
|
||||
Evaluated d v -> k v mt d r msgs
|
||||
Hole _ -> k (VMeta tnk []) mt d r msgs
|
||||
Residuation _ _ _ -> k (VMeta tnk []) mt d r msgs
|
||||
Narrowing _ _ -> k (VMeta tnk []) mt d r msgs
|
||||
|
||||
tnk2term True xs tnk = force tnk >>= value2term True xs
|
||||
tnk2term False xs tnk = EvalM $ \gr k mt d r msgs ->
|
||||
tnk2term False xs tnk = EvalM $ \gr k e mt d r msgs ->
|
||||
let join f g = do res <- f
|
||||
case res of
|
||||
Fail msg msgs -> return (Fail msg msgs)
|
||||
@@ -1018,21 +1016,23 @@ tnk2term False xs tnk = EvalM $ \gr k mt d r msgs ->
|
||||
| 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
|
||||
| otherwise = return (Success (r,c+1,x:xs) msgs)
|
||||
|
||||
err msg msgs = return (Fail msg msgs)
|
||||
|
||||
in do s <- readSTRef tnk
|
||||
case s of
|
||||
Unevaluated env t -> do let d0 = length env
|
||||
res <- case eval env t [] of
|
||||
EvalM f -> f gr (\v mt d msgs r -> do writeSTRef tnk (Evaluated d0 v)
|
||||
r <- case value2term False xs v of
|
||||
EvalM f -> f gr (acc d0) mt d msgs r
|
||||
EvalM f -> f gr (acc d0) err mt d msgs r
|
||||
writeSTRef tnk s
|
||||
return r) mt maxBound (r,0,[]) msgs
|
||||
return r) err mt maxBound (r,0,[]) msgs
|
||||
case res of
|
||||
Fail msg msgs -> return (Fail msg msgs)
|
||||
Success (r,0,xs) msgs -> k (FV []) mt d r msgs
|
||||
Success (r,c,xs) msgs -> flush xs (\mt msgs r -> return (Success msgs r)) mt r msgs
|
||||
Evaluated d0 v -> do res <- case value2term False xs v of
|
||||
EvalM f -> f gr (acc d0) mt maxBound (r,0,[]) msgs
|
||||
EvalM f -> f gr (acc d0) err mt maxBound (r,0,[]) msgs
|
||||
case res of
|
||||
Fail msg msgs -> return (Fail msg msgs)
|
||||
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
|
||||
|
||||
|
||||
unsafeIOToEvalM :: IO a -> EvalM s a
|
||||
unsafeIOToEvalM f = EvalM (\gr k mt d r msgs -> unsafeIOToST f >>= \x -> k x mt d r msgs)
|
||||
unsafeIOToEvalM f = EvalM (\gr k e mt d r msgs -> unsafeIOToST f >>= \x -> k x mt d r msgs)
|
||||
|
||||
|
||||
808
src/compiler/api/GF/Compile/Compute/Concrete2.hs
Normal file
808
src/compiler/api/GF/Compile/Compute/Concrete2.hs
Normal file
@@ -0,0 +1,808 @@
|
||||
{-# LANGUAGE RankNTypes, BangPatterns, GeneralizedNewtypeDeriving #-}
|
||||
|
||||
module GF.Compile.Compute.Concrete2
|
||||
(Env, Scope, Value(..), Constraint, ConstValue(..), Globals(..), PredefTable, EvalM,
|
||||
runEvalM, stdPredef, globals, pdArity,
|
||||
normalForm, normalFlatForm,
|
||||
eval, apply, value2term, value2termM, patternMatch, vtableSelect,
|
||||
newBinding, newResiduation, getMeta, setMeta, MetaState(..), variants, try,
|
||||
evalError, evalWarn, ppValue, Choice, unit, split, split4, mapC, mapCM) where
|
||||
|
||||
import Prelude hiding ((<>)) -- GHC 8.4.1 clash with Text.PrettyPrint
|
||||
import GF.Infra.Ident
|
||||
import GF.Infra.CheckM
|
||||
import GF.Data.Operations(Err(..))
|
||||
import GF.Data.Utilities(splitAt',(<||>),anyM)
|
||||
import GF.Grammar.Lookup(lookupResDef,lookupOrigInfo)
|
||||
import GF.Grammar.Grammar
|
||||
import GF.Grammar.Macros
|
||||
import GF.Grammar.Predef
|
||||
import GF.Grammar.Printer hiding (ppValue)
|
||||
import GF.Grammar.Lockfield(lockLabel)
|
||||
import GF.Text.Pretty hiding (empty)
|
||||
import Control.Monad
|
||||
import Control.Applicative hiding (Const)
|
||||
import qualified Control.Applicative as A
|
||||
import qualified Data.Map as Map
|
||||
import Data.Maybe (fromMaybe,fromJust)
|
||||
import Data.List
|
||||
import Data.Char
|
||||
|
||||
type Env = [(Ident,Value)]
|
||||
type Scope = [(Ident,Value)]
|
||||
type Predef a = Globals -> Choice -> [Value] -> ConstValue a
|
||||
type PredefCombinator a = Predef a -> Predef a
|
||||
type PredefTable = Map.Map Ident (Predef Value)
|
||||
data Globals = Gl Grammar PredefTable
|
||||
|
||||
data Value
|
||||
= VApp QIdent [Value]
|
||||
| VMeta MetaId [Value]
|
||||
| VSusp MetaId (Value -> Value) [Value]
|
||||
| VGen {-# UNPACK #-} !Int [Value]
|
||||
| VClosure Env Choice Term
|
||||
| VProd BindType Ident Value Value
|
||||
| VRecType [(Label, Value)]
|
||||
| VR [(Label, Value)]
|
||||
| VP Value Label [Value]
|
||||
| VExtR Value Value
|
||||
| VTable Value Value
|
||||
| VT Value Env Choice [Case]
|
||||
| VV Value [Value]
|
||||
| VS Value Value [Value]
|
||||
| VSort Ident
|
||||
| VInt Integer
|
||||
| VFlt Double
|
||||
| VStr String
|
||||
| VEmpty
|
||||
| VC Value Value
|
||||
| VGlue Value Value
|
||||
| VPatt Int (Maybe Int) Patt
|
||||
| VPattType Value
|
||||
| VFV Choice [Value]
|
||||
| VAlts Value [(Value, Value)]
|
||||
| VStrs [Value]
|
||||
| VSymCat Int LIndex [(LIndex, (Value, Type))]
|
||||
| VError Doc
|
||||
-- These two constructors are only used internally
|
||||
-- in the type checker.
|
||||
| VCRecType [(Label, Bool, Value)]
|
||||
| VCInts (Maybe Integer) (Maybe Integer)
|
||||
|
||||
data ConstValue a
|
||||
= Const a
|
||||
| CSusp MetaId (Value -> ConstValue a)
|
||||
| CFV Choice [ConstValue a]
|
||||
| RunTime
|
||||
| NonExist
|
||||
|
||||
instance Functor ConstValue where
|
||||
fmap f (Const c) = Const (f c)
|
||||
fmap f (CFV i vs) = CFV i (map (fmap f) vs)
|
||||
fmap f (CSusp i k) = CSusp i (fmap f . k)
|
||||
fmap f RunTime = RunTime
|
||||
fmap f NonExist = NonExist
|
||||
|
||||
instance Applicative ConstValue where
|
||||
pure = Const
|
||||
|
||||
(Const f) <*> (Const x) = Const (f x)
|
||||
(CFV s vs) <*> v2 = CFV s [v1 <*> v2 | v1 <- vs]
|
||||
v1 <*> (CFV s vs) = CFV s [v1 <*> v2 | v2 <- vs]
|
||||
(CSusp i k) <*> v2 = CSusp i (\v -> k v <*> v2)
|
||||
v1 <*> (CSusp i k) = CSusp i (\v -> v1 <*> k v)
|
||||
NonExist <*> _ = NonExist
|
||||
_ <*> NonExist = NonExist
|
||||
RunTime <*> _ = RunTime
|
||||
_ <*> RunTime = RunTime
|
||||
|
||||
normalForm :: Globals -> Term -> Check Term
|
||||
normalForm g t = value2term g [] (eval g [] unit t [])
|
||||
|
||||
normalFlatForm :: Globals -> Term -> Check [Term]
|
||||
normalFlatForm g t = runEvalM g (value2termM False [] (eval g [] unit t []))
|
||||
|
||||
eval :: Globals -> Env -> Choice -> Term -> [Value] -> Value
|
||||
eval g env s (Vr x) vs = case lookup x env of
|
||||
Nothing -> VError ("Variable" <+> pp x <+> "is not in scope")
|
||||
Just v -> apply g v vs
|
||||
eval g env s (Sort sort) []
|
||||
| sort == cTok = VSort cStr
|
||||
| otherwise = VSort sort
|
||||
eval g env s (EInt n) [] = VInt n
|
||||
eval g env s (EFloat d) [] = VFlt d
|
||||
eval g env s (K t) [] = VStr t
|
||||
eval g env s Empty [] = VEmpty
|
||||
eval g env s (App t1 t2) vs = let (s1,s2) = split s
|
||||
in eval g env s1 t1 (eval g env s2 t2 [] : vs)
|
||||
eval g env s (Abs b x t) [] = VClosure env s (Abs b x t)
|
||||
eval g env s (Abs b x t) (v:vs) = eval g ((x,v):env) s t vs
|
||||
eval g env s (Meta i) vs = VMeta i vs
|
||||
eval g env s (ImplArg t) [] = eval g env s t []
|
||||
eval g env s (Prod b x t1 t2)[] = let (s1,s2) = split s
|
||||
in VProd b x (eval g env s1 t1 []) (VClosure env s2 t2)
|
||||
eval g env s (Typed t ty) vs = eval g env s t vs
|
||||
eval g env s (RecType lbls) [] = VRecType (mapC (\s (lbl,ty) -> (lbl, eval g env s ty [])) s lbls)
|
||||
eval g env s (R as) [] = VR (mapC (\s (lbl,(ty,t)) -> (lbl, eval g env s t [])) s as)
|
||||
eval g env s (P t lbl) vs = let project (VR as) = case lookup lbl as of
|
||||
Nothing -> VError ("Missing value for label" <+> pp lbl $$
|
||||
"in" <+> pp (P t lbl))
|
||||
Just v -> apply g v vs
|
||||
project (VFV s fvs) = VFV s (map project fvs)
|
||||
project (VMeta i vs) = VSusp i (\v -> project (apply g v vs)) []
|
||||
project (VSusp i k vs) = VSusp i (\v -> project (apply g (k v) vs)) []
|
||||
project v = VP v lbl vs
|
||||
in project (eval g env s t [])
|
||||
eval g env s (ExtR t1 t2) [] = let (s1,s2) = split s
|
||||
|
||||
extend (VR as1) (VR as2) = VR (foldl (\as (lbl,v) -> update lbl v as) as1 as2)
|
||||
extend (VRecType as1) (VRecType as2) = VRecType (foldl (\as (lbl,v) -> update lbl v as) as1 as2)
|
||||
extend (VFV i fvs) v2 = VFV i [extend v1 v2 | v1 <- fvs]
|
||||
extend v1 (VFV i fvs) = VFV i [extend v1 v2 | v2 <- fvs]
|
||||
extend (VMeta i vs) v2 = VSusp i (\v -> extend (apply g v vs) v2) []
|
||||
extend v1 (VMeta i vs) = VSusp i (\v -> extend v1 (apply g v vs)) []
|
||||
extend (VSusp i k vs) v2 = VSusp i (\v -> extend (apply g (k v) vs) v2) []
|
||||
extend v1 (VSusp i k vs) = VSusp i (\v -> extend v1 (apply g (k v) vs)) []
|
||||
extend v1 v2 = VExtR v1 v2
|
||||
|
||||
in extend (eval g env s1 t1 []) (eval g env s2 t2 [])
|
||||
eval g env s (Table t1 t2) [] = let (!s1,!s2) = split s
|
||||
in VTable (eval g env s1 t1 []) (eval g env s2 t2 [])
|
||||
eval g env s (T (TTyped ty) cs)[]=let (!s1,!s2) = split s
|
||||
in VT (eval g env s1 ty []) env s2 cs
|
||||
eval g env s (T (TWild ty) cs) []=let (!s1,!s2) = split s
|
||||
in VT (eval g env s1 ty []) env s2 cs
|
||||
eval g env s (V ty ts) [] = let (!s1,!s2) = split s
|
||||
in VV (eval g env s1 ty []) (mapC (\s t -> eval g env s t []) s2 ts)
|
||||
eval g env s (S t1 t2) vs = let (!s1,!s2) = split s
|
||||
v1 = eval g env s1 t1 []
|
||||
v2 = eval g env s2 t2 []
|
||||
v0 = VS v1 v2 vs
|
||||
|
||||
select (VT _ env s cs) = patternMatch g s v0 (map (\(p,t) -> (env,[p],v2:vs,t)) cs)
|
||||
select (VV vty tvs) = case value2termM False (map fst env) vty of
|
||||
EvalM f -> case f g (\x state xs ws -> Success (x:xs) ws) empty [] [] of
|
||||
Fail msg ws -> VError msg
|
||||
Success tys ws -> case tys of
|
||||
[ty] -> vtableSelect g v0 ty tvs v2 vs
|
||||
tys -> vtableSelect g v0 (FV (reverse tys)) tvs v2 vs
|
||||
select (VFV i fvs) = VFV i [select v1 | v1 <- fvs]
|
||||
select (VMeta i vs) = VSusp i (\v -> select (apply g v vs)) []
|
||||
select (VSusp i k vs) = VSusp i (\v -> select (apply g (k v) vs)) []
|
||||
select v1 = v0
|
||||
|
||||
empty = State Map.empty Map.empty
|
||||
|
||||
in select v1
|
||||
eval g env s (Let (x,(_,t1)) t2) vs = let (!s1,!s2) = split s
|
||||
in eval g ((x,eval g env s1 t1 []):env) s2 t2 vs
|
||||
eval g env c (Q q@(m,id)) vs
|
||||
| m == cPredef = case Map.lookup id predef of
|
||||
Nothing -> VApp q vs
|
||||
Just fn -> let valueOf (Const res) = res
|
||||
valueOf (CFV i vs) = VFV i (map valueOf vs)
|
||||
valueOf (CSusp i k) = VSusp i (valueOf . k) []
|
||||
valueOf RunTime = VApp q vs
|
||||
valueOf NonExist = VApp (cPredef,cNonExist) []
|
||||
in valueOf (fn g c vs)
|
||||
| otherwise = case lookupResDef gr q of
|
||||
Ok t -> eval g env c t vs
|
||||
Bad msg -> error msg
|
||||
where
|
||||
Gl gr predef = g
|
||||
eval g env s (QC q) vs = VApp q vs
|
||||
eval g env s (C t1 t2) [] = let (!s1,!s2) = split s
|
||||
|
||||
concat v1 VEmpty = v1
|
||||
concat VEmpty v2 = v2
|
||||
concat (VFV i fvs) v2 = VFV i [concat v1 v2 | v1 <- fvs]
|
||||
concat v1 (VFV i fvs) = VFV i [concat v1 v2 | v2 <- fvs]
|
||||
concat (VMeta i vs) v2 = VSusp i (\v -> concat (apply g v vs) v2) []
|
||||
concat v1 (VMeta i vs) = VSusp i (\v -> concat v1 (apply g v vs)) []
|
||||
concat (VSusp i k vs) v2 = VSusp i (\v -> concat (apply g (k v) vs) v2) []
|
||||
concat v1 (VSusp i k vs) = VSusp i (\v -> concat v1 (apply g (k v) vs)) []
|
||||
concat v1 v2 = VC v1 v2
|
||||
|
||||
in concat (eval g env s1 t1 []) (eval g env s2 t2 [])
|
||||
eval g env s (Glue t1 t2) [] = let (!s1,!s2) = split s
|
||||
|
||||
glue VEmpty v = v
|
||||
glue (VC v1 v2) v = VC v1 (glue v2 v)
|
||||
glue (VApp q []) v
|
||||
| q == (cPredef,cNonExist) = VApp q []
|
||||
glue v VEmpty = v
|
||||
glue v (VC v1 v2) = VC (glue v v1) v2
|
||||
glue v (VApp q [])
|
||||
| q == (cPredef,cNonExist) = VApp q []
|
||||
glue (VStr s1) (VStr s2) = VStr (s1++s2)
|
||||
glue v (VAlts d vas) = VAlts (glue v d) [(glue v v',ss) | (v',ss) <- vas]
|
||||
glue (VAlts d vas) (VStr s) = pre d vas s
|
||||
glue (VAlts d vas) v = glue d v
|
||||
glue (VFV i fvs) v2 = VFV i [glue v1 v2 | v1 <- fvs]
|
||||
glue v1 (VFV i fvs) = VFV i [glue v1 v2 | v2 <- fvs]
|
||||
glue (VMeta i vs) v2 = VSusp i (\v -> glue (apply g v vs) v2) []
|
||||
glue v1 (VMeta i vs) = VSusp i (\v -> glue v1 (apply g v vs)) []
|
||||
glue (VSusp i k vs) v2 = VSusp i (\v -> glue (apply g (k v) vs) v2) []
|
||||
glue v1 (VSusp i k vs)= VSusp i (\v -> glue v1 (apply g (k v) vs)) []
|
||||
glue v1 v2 = VGlue v1 v2
|
||||
|
||||
pre vd [] s = glue vd (VStr s)
|
||||
pre vd ((v,VStrs ss):vas) s
|
||||
| or [startsWith s' s | VStr s' <- ss] = glue v (VStr s)
|
||||
| otherwise = pre vd vas s
|
||||
|
||||
in glue (eval g env s1 t1 []) (eval g env s2 t2 [])
|
||||
eval g env s (EPatt min max p) [] = VPatt min max p
|
||||
eval g env s (EPattType t) [] = VPattType (eval g env s t [])
|
||||
eval g env s (ELincat c ty) [] = let lbl = lockLabel c
|
||||
lty = RecType []
|
||||
in eval g env s (ExtR ty (RecType [(lbl,lty)])) []
|
||||
eval g env s (ELin c t) [] = let lbl = lockLabel c
|
||||
lt = R []
|
||||
in eval g env s (ExtR t (R [(lbl,(Nothing,lt))])) []
|
||||
eval g env s (FV ts) vs = VFV s (mapC (\s t -> eval g env s t vs) s ts)
|
||||
eval g env s (Alts d as) [] = let (!s1,!s2) = split s
|
||||
vd = eval g env s1 d []
|
||||
vas = mapC (\s (t1,t2) -> let (!s1,!s2) = split s
|
||||
in (eval g env s1 t1 [],eval g env s2 t2 [])) s2 as
|
||||
in VAlts vd vas
|
||||
eval g env s (Strs ts) [] = VStrs (mapC (\s t -> eval g env s t []) s ts)
|
||||
eval g env s (TSymCat d r rs) []= VSymCat d r [(i,(fromJust (lookup pv env),ty)) | (i,(pv,ty)) <- rs]
|
||||
eval g env s t vs = VError ("Cannot reduce term" <+> pp t)
|
||||
|
||||
stdPredef :: Globals -> PredefTable
|
||||
stdPredef g = Map.fromList
|
||||
[(cLength, pdArity 1 $ \g c [v] -> fmap (VInt . genericLength) (value2string g v))
|
||||
,(cTake, pdArity 2 $ \g c [v1,v2] -> fmap string2value (liftA2 genericTake (value2int g v1) (value2string g v2)))
|
||||
,(cDrop, pdArity 2 $ \g c [v1,v2] -> fmap string2value (liftA2 genericDrop (value2int g v1) (value2string g v2)))
|
||||
,(cTk, pdArity 2 $ \g c [v1,v2] -> fmap string2value (liftA2 genericTk (value2int g v1) (value2string g v2)))
|
||||
,(cDp, pdArity 2 $ \g c [v1,v2] -> fmap string2value (liftA2 genericDp (value2int g v1) (value2string g v2)))
|
||||
,(cIsUpper,pdArity 1 $ \g c [v] -> fmap toPBool (liftA (all isUpper) (value2string g v)))
|
||||
,(cToUpper,pdArity 1 $ \g c [v] -> fmap string2value (liftA (map toUpper) (value2string g v)))
|
||||
,(cToLower,pdArity 1 $ \g c [v] -> fmap string2value (liftA (map toLower) (value2string g v)))
|
||||
,(cEqStr, pdArity 2 $ \g c [v1,v2] -> fmap toPBool (liftA2 (==) (value2string g v1) (value2string g v2)))
|
||||
,(cOccur, pdArity 2 $ \g c [v1,v2] -> fmap toPBool (liftA2 occur (value2string g v1) (value2string g v2)))
|
||||
,(cOccurs, pdArity 2 $ \g c [v1,v2] -> fmap toPBool (liftA2 occurs (value2string g v1) (value2string g v2)))
|
||||
,(cEqInt, pdArity 2 $ \g c [v1,v2] -> fmap toPBool (liftA2 (==) (value2int g v1) (value2int g v2)))
|
||||
,(cLessInt,pdArity 2 $ \g c [v1,v2] -> fmap toPBool (liftA2 (<) (value2int g v1) (value2int g v2)))
|
||||
,(cPlus, pdArity 2 $ \g c [v1,v2] -> fmap VInt (liftA2 (+) (value2int g v1) (value2int g v2)))
|
||||
,(cError, pdArity 1 $ \g c [v] -> fmap (VError . pp) (value2string g v))
|
||||
]
|
||||
where
|
||||
genericTk n = reverse . genericDrop n . reverse
|
||||
genericDp n = reverse . genericTake n . reverse
|
||||
|
||||
apply g (VMeta i vs0) vs = VMeta i (vs0++vs)
|
||||
apply g (VSusp i k vs0) vs = VSusp i k (vs0++vs)
|
||||
apply g (VApp f vs0) vs = VApp f (vs0++vs)
|
||||
apply g (VGen i vs0) vs = VGen i (vs0++vs)
|
||||
apply g (VFV i fvs) vs = VFV i [apply g v vs | v <- fvs]
|
||||
apply g (VClosure env s (Abs b x t)) (v:vs) = eval g ((x,v):env) s t vs
|
||||
apply g v [] = v
|
||||
|
||||
toPBool True = VApp (cPredef,cPTrue) []
|
||||
toPBool False = VApp (cPredef,cPFalse) []
|
||||
|
||||
occur s1 [] = False
|
||||
occur s1 s2@(_:tail) = check s1 s2
|
||||
where
|
||||
check xs [] = False
|
||||
check [] ys = True
|
||||
check (x:xs) (y:ys)
|
||||
| x == y = check xs ys
|
||||
check _ _ = occur s1 tail
|
||||
|
||||
occurs cs s2 = any (\c -> elem c s2) cs
|
||||
|
||||
update lbl v [] = [(lbl,v)]
|
||||
update lbl v (a@(lbl',_):as)
|
||||
| lbl==lbl' = (lbl,v) : as
|
||||
| otherwise = a : update lbl v as
|
||||
|
||||
patternMatch g s v0 [] = v0
|
||||
patternMatch g s v0 ((env0,ps,args0,t):eqs) = match env0 ps eqs args0
|
||||
where
|
||||
match env [] eqs args = eval g env s t args
|
||||
match env (PT ty p :ps) eqs args = match env (p:ps) eqs args
|
||||
match env (PAlt p1 p2:ps) eqs args = match env (p1:ps) ((env,p2:ps,args,t):eqs) args
|
||||
match env (PM q :ps) eqs args = case lookupResDef gr q of
|
||||
Ok t -> case eval g [] unit t [] of
|
||||
VPatt _ _ p -> match env (p:ps) eqs args
|
||||
_ -> error $ render (hang "Expected pattern macro:" 4
|
||||
(pp t))
|
||||
Bad msg -> error msg
|
||||
where
|
||||
Gl gr _ = g
|
||||
match env (PV v :ps) eqs (arg:args) = match ((v,arg):env) ps eqs args
|
||||
match env (PAs v p :ps) eqs (arg:args) = match ((v,arg):env) (p:ps) eqs (arg:args)
|
||||
match env (PW :ps) eqs (arg:args) = match env ps eqs args
|
||||
match env (PTilde _ :ps) eqs (arg:args) = match env ps eqs args
|
||||
match env (p :ps) eqs (arg:args) = match' env p ps eqs arg args
|
||||
|
||||
match' env p ps eqs arg args =
|
||||
case (p,arg) of
|
||||
(p, VMeta i vs) -> VSusp i (\v -> match' env p ps eqs (apply g v vs) args) []
|
||||
(p, VGen i vs) -> v0
|
||||
(p, VSusp i k vs) -> VSusp i (\v -> match' env p ps eqs (apply g (k v) vs) args) []
|
||||
(p, VFV s vs) -> VFV s [match' env p ps eqs arg args | arg <- vs]
|
||||
(PP q qs, VApp r vs)
|
||||
| q == r -> match env (qs++ps) eqs (vs++args)
|
||||
(PR pas, VR as) -> matchRec env (reverse pas) as ps eqs args
|
||||
(PString s1, VStr s2)
|
||||
| s1 == s2 -> match env ps eqs args
|
||||
(PString s1, VEmpty)
|
||||
| null s1 -> match env ps eqs args
|
||||
(PSeq min1 max1 p1 min2 max2 p2,v)
|
||||
-> case value2string g v of
|
||||
Const str -> let n = length str
|
||||
lo = min1 `max` (n-fromMaybe n max2)
|
||||
hi = (n-min2) `min` fromMaybe n max1
|
||||
(ds,cs) = splitAt lo str
|
||||
|
||||
eqs' = matchStr env (p1:p2:ps) eqs (hi-lo) (reverse ds) cs args
|
||||
|
||||
in patternMatch g s v0 eqs'
|
||||
RunTime -> v0
|
||||
NonExist -> patternMatch g s v0 eqs
|
||||
(PRep minp maxp p, v)
|
||||
-> case value2string g v of
|
||||
Const str -> let n = length (str::String) `div` (max minp 1)
|
||||
eqs' = matchRep env n minp maxp p minp maxp p ps ((env,PString []:ps,(arg:args),t) : eqs) (arg:args)
|
||||
in patternMatch g s v0 eqs'
|
||||
RunTime -> v0
|
||||
NonExist -> patternMatch g s v0 eqs
|
||||
(PChar, VStr [_]) -> match env ps eqs args
|
||||
(PChars cs, VStr [c])
|
||||
| elem c cs -> match env ps eqs args
|
||||
(PInt n, VInt m)
|
||||
| n == m -> match env ps eqs args
|
||||
(PFloat n, VFlt m)
|
||||
| n == m -> match env ps eqs args
|
||||
_ -> patternMatch g s v0 eqs
|
||||
|
||||
matchRec env [] as ps eqs args = match env ps eqs args
|
||||
matchRec env ((lbl,p):pas) as ps eqs args =
|
||||
case lookup lbl as of
|
||||
Just tnk -> matchRec env pas as (p:ps) eqs (tnk:args)
|
||||
Nothing -> VError ("Missing value for label" <+> pp lbl)
|
||||
|
||||
matchStr env ps eqs i ds [] args =
|
||||
(env,ps,(string2value (reverse ds)):(string2value []):args,t) : eqs
|
||||
matchStr env ps eqs 0 ds cs args =
|
||||
(env,ps,(string2value (reverse ds)):(string2value cs):args,t) : eqs
|
||||
matchStr env ps eqs i ds (c:cs) args =
|
||||
(env,ps,(string2value (reverse ds)):(string2value (c:cs)):args,t) :
|
||||
matchStr env ps eqs (i-1 :: Int) (c:ds) cs args
|
||||
|
||||
matchRep env 0 minp maxp p minq maxq q ps eqs args = eqs
|
||||
matchRep env n minp maxp p minq maxq q ps eqs args =
|
||||
matchRep env (n-1) minp maxp p (minp+minq) (liftM2 (+) maxp maxq) (PSeq minp maxp p minq maxq q) ps ((env,q:ps,args,t) : eqs) args
|
||||
|
||||
vtableSelect g v0 ty cs v2 vs =
|
||||
apply g (select (value2index v2 ty)) vs
|
||||
where
|
||||
select (Const (i,_)) = cs !! i
|
||||
select (CSusp i k) = VSusp i (\v -> select (k v)) []
|
||||
select (CFV s vs) = VFV s (map select vs)
|
||||
select _ = VError ("the parameter:" <+> ppValue Unqualified 0 v2 $$
|
||||
"cannot be evaluated at compile time.")
|
||||
|
||||
value2index (VMeta i vs) ty = CSusp i (\v -> value2index (apply g v vs) ty)
|
||||
value2index (VSusp i k vs) ty = CSusp i (\v -> value2index (apply g (k v) vs) ty)
|
||||
value2index (VR as) (RecType lbls) = compute lbls
|
||||
where
|
||||
compute [] = pure (0,1)
|
||||
compute ((lbl,ty):lbls) =
|
||||
case lookup lbl as of
|
||||
Just v -> liftA2 (\(r, cnt) (r',cnt') -> (r*cnt'+r',cnt*cnt'))
|
||||
(value2index v ty)
|
||||
(compute lbls)
|
||||
Nothing -> error (show ("Missing value for label" <+> pp lbl $$
|
||||
"among" <+> hsep (punctuate (pp ',') (map fst as))))
|
||||
value2index (VApp q tnks) ty =
|
||||
let (r ,ctxt,cnt ) = getIdxCnt q
|
||||
in fmap (\(r', cnt') -> (r+r',cnt)) (compute ctxt tnks)
|
||||
where
|
||||
getIdxCnt q =
|
||||
let (_,ResValue (L _ ty) idx) = getInfo q
|
||||
(ctxt,QC p) = typeFormCnc ty
|
||||
(_,ResParam _ (Just (_,cnt))) = getInfo p
|
||||
in (idx,ctxt,cnt)
|
||||
|
||||
compute [] [] = pure (0,1)
|
||||
compute ((_,_,ty):ctxt) (v:vs) =
|
||||
liftA2 (\(r, cnt) (r',cnt') -> (r*cnt'+r',cnt*cnt'))
|
||||
(value2index v ty)
|
||||
(compute ctxt vs)
|
||||
|
||||
getInfo :: QIdent -> (ModuleName,Info)
|
||||
getInfo q =
|
||||
case lookupOrigInfo gr q of
|
||||
Ok res -> res
|
||||
Bad msg -> error msg
|
||||
|
||||
Gl gr _ = g
|
||||
value2index (VInt n) ty
|
||||
| Just max <- isTypeInts ty = Const (fromIntegral n,fromIntegral max+1)
|
||||
value2index (VFV i vs) ty = CFV i [value2index v ty | v <- vs]
|
||||
value2index v ty = RunTime
|
||||
|
||||
|
||||
value2term :: Globals -> [Ident] -> Value -> Check Term
|
||||
value2term g xs v = do
|
||||
res <- runEvalM g (value2termM False xs v)
|
||||
case res of
|
||||
[t] -> return t
|
||||
ts -> return (FV ts)
|
||||
|
||||
type Constraint = Value
|
||||
data MetaState
|
||||
= Bound Int Value
|
||||
| Narrowing Type
|
||||
| Residuation Scope (Maybe Constraint)
|
||||
data State
|
||||
= State
|
||||
{ choices :: Map.Map Choice Int
|
||||
, metaVars :: Map.Map MetaId MetaState
|
||||
}
|
||||
type Cont r = State -> r -> [Message] -> CheckResult r [Message]
|
||||
newtype EvalM a = EvalM (forall r . Globals -> (a -> Cont r) -> Cont r)
|
||||
|
||||
instance Functor EvalM where
|
||||
fmap f (EvalM m) = EvalM (\g k -> m g (k . f))
|
||||
|
||||
instance Applicative EvalM where
|
||||
pure x = EvalM (\g k -> k x)
|
||||
(EvalM f) <*> (EvalM h) = EvalM (\g k -> f g (\fn -> h g (\x -> k (fn x))))
|
||||
|
||||
instance Alternative EvalM where
|
||||
empty = EvalM (\g k _ r msgs -> Success r msgs)
|
||||
(EvalM f) <|> (EvalM g) = EvalM $ \gl k state r msgs ->
|
||||
case f gl k state r msgs of
|
||||
Fail msg msgs -> Fail msg msgs
|
||||
Success r msgs -> g gl k state r msgs
|
||||
|
||||
instance Monad EvalM where
|
||||
(EvalM f) >>= h = EvalM (\g k -> f g (\x -> case h x of {EvalM h -> h g k}))
|
||||
|
||||
instance MonadFail EvalM where
|
||||
fail msg = EvalM (\g k _ _ msgs -> Fail (pp msg) msgs)
|
||||
|
||||
instance MonadPlus EvalM where
|
||||
|
||||
evalError msg = EvalM (\g k _ _ msgs -> Fail msg msgs)
|
||||
|
||||
evalWarn msg = EvalM (\g k state r msgs -> k () state r (msg:msgs))
|
||||
|
||||
runEvalM :: Globals -> EvalM a -> Check [a]
|
||||
runEvalM g (EvalM f) = Check $ \(es,ws) ->
|
||||
case f g (\x state xs ws -> Success (x:xs) ws) empty [] ws of
|
||||
Fail msg ws -> Fail msg (es,ws)
|
||||
Success xs ws -> Success (reverse xs) (es,ws)
|
||||
where
|
||||
empty = State Map.empty Map.empty
|
||||
|
||||
globals :: EvalM Globals
|
||||
globals = EvalM (\g k -> k g)
|
||||
|
||||
variants :: Choice -> [a] -> EvalM a
|
||||
variants c xs = EvalM (\g k state@(State choices metas) r msgs ->
|
||||
case Map.lookup c choices of
|
||||
Just j -> k (xs !! j) state r msgs
|
||||
Nothing -> backtrack 0 xs k choices metas r msgs)
|
||||
where
|
||||
backtrack j [] k choices metas r msgs = Success r msgs
|
||||
backtrack j (x:xs) k choices metas r msgs =
|
||||
case k x (State (Map.insert c j choices) metas) r msgs of
|
||||
Fail msg msgs -> Fail msg msgs
|
||||
Success r msgs -> backtrack (j+1) xs k choices metas r msgs
|
||||
|
||||
try :: (a -> EvalM b) -> [a] -> Message -> EvalM b
|
||||
try f xs msg = EvalM (\g k state r msgs ->
|
||||
let (res,msgs') = backtrack g xs state [] msgs
|
||||
in case res of
|
||||
[] -> Fail msg msgs'
|
||||
res -> continue g k res r msgs')
|
||||
where
|
||||
backtrack g [] state res msgs = (res,msgs)
|
||||
backtrack g (x:xs) state res msgs =
|
||||
case f x of
|
||||
EvalM f -> case f g (\x state res msgs -> Success ((x,state):res) msgs) state res msgs of
|
||||
Fail msg _ -> backtrack g xs state res msgs
|
||||
Success res msgs -> backtrack g xs state res msgs
|
||||
|
||||
continue g k [] r msgs = Success r msgs
|
||||
continue g k ((x,state):res) r msgs =
|
||||
case k x state r msgs of
|
||||
Fail msg msgs -> Fail msg msgs
|
||||
Success r msgs -> continue g k res r msgs
|
||||
|
||||
newBinding :: Value -> EvalM MetaId
|
||||
newBinding v = EvalM (\g k (State choices metas) r msgs ->
|
||||
let meta_id = Map.size metas+1
|
||||
in k meta_id (State choices (Map.insert meta_id (Bound 0 v) metas)) r msgs)
|
||||
|
||||
newResiduation :: Scope -> EvalM MetaId
|
||||
newResiduation scope = EvalM (\g k (State choices metas) r msgs ->
|
||||
let meta_id = Map.size metas+1
|
||||
in k meta_id (State choices (Map.insert meta_id (Residuation scope Nothing) metas)) r msgs)
|
||||
|
||||
getMeta :: MetaId -> EvalM MetaState
|
||||
getMeta i = EvalM (\g k state r msgs ->
|
||||
case Map.lookup i (metaVars state) of
|
||||
Just ms -> k ms state r msgs
|
||||
Nothing -> Fail ("Metavariable ?"<>pp i<+>"is not defined") msgs)
|
||||
|
||||
setMeta :: MetaId -> MetaState -> EvalM ()
|
||||
setMeta i ms = EvalM (\g k (State choices metas) r msgs ->
|
||||
let state' = State choices (Map.insert i ms metas)
|
||||
in k () state' r msgs)
|
||||
|
||||
value2termM :: Bool -> [Ident] -> Value -> EvalM Term
|
||||
value2termM flat xs (VApp q vs) =
|
||||
foldM (\t v -> fmap (App t) (value2termM flat xs v)) (if fst q == cPredef then Q q else QC q) vs
|
||||
value2termM flat xs (VMeta i vs) = do
|
||||
mv <- getMeta i
|
||||
case mv of
|
||||
Bound _ v -> do g <- globals
|
||||
value2termM flat xs (apply g v vs)
|
||||
Residuation _ mb_ctr ->
|
||||
case mb_ctr of
|
||||
Just ctr -> do g <- globals
|
||||
value2termM flat xs (apply g ctr vs)
|
||||
Nothing -> foldM (\t v -> fmap (App t) (value2termM flat xs v)) (Meta i) vs
|
||||
value2termM flat xs (VSusp j k vs) =
|
||||
let v = k (VGen maxBound vs)
|
||||
in value2termM flat xs v
|
||||
value2termM flat xs (VGen j tnks) =
|
||||
foldM (\e1 tnk -> fmap (App e1) (value2termM flat xs tnk)) (Vr (reverse xs !! j)) tnks
|
||||
value2termM flat xs (VClosure env s (Abs b x t)) = do
|
||||
g <- globals
|
||||
let v = eval g ((x,VGen (length xs) []):env) s t []
|
||||
x' = mkFreshVar xs x
|
||||
t <- value2termM flat (x':xs) v
|
||||
return (Abs b x' t)
|
||||
value2termM flat xs (VProd b x v1 v2)
|
||||
| x == identW = do t1 <- value2termM flat xs v1
|
||||
v2 <- case v2 of
|
||||
VClosure env s t2 -> do g <- globals
|
||||
return (eval g env s t2 [])
|
||||
v2 -> return v2
|
||||
t2 <- value2termM flat xs v2
|
||||
return (Prod b x t1 t2)
|
||||
| otherwise = do t1 <- value2termM flat xs v1
|
||||
v2 <- case v2 of
|
||||
VClosure env s t2 -> do g <- globals
|
||||
return (eval g ((x,VGen (length xs) []):env) s t2 [])
|
||||
v2 -> return v2
|
||||
t2 <- value2termM flat (x:xs) v2
|
||||
return (Prod b (mkFreshVar xs x) t1 t2)
|
||||
value2termM flat xs (VRecType lbls) = do
|
||||
lbls <- mapM (\(lbl,v) -> fmap ((,) lbl) (value2termM flat xs v)) lbls
|
||||
return (RecType lbls)
|
||||
value2termM flat xs (VR as) = do
|
||||
as <- mapM (\(lbl,v) -> fmap (\t -> (lbl,(Nothing,t))) (value2termM flat xs v)) as
|
||||
return (R as)
|
||||
value2termM flat xs (VP v lbl vs) = do
|
||||
t <- value2termM flat xs v
|
||||
foldM (\e1 tnk -> fmap (App e1) (value2termM flat xs tnk)) (P t lbl) vs
|
||||
value2termM flat xs (VExtR v1 v2) = do
|
||||
t1 <- value2termM flat xs v1
|
||||
t2 <- value2termM flat xs v2
|
||||
return (ExtR t1 t2)
|
||||
value2termM flat xs (VTable v1 v2) = do
|
||||
t1 <- value2termM flat xs v1
|
||||
t2 <- value2termM flat xs v2
|
||||
return (Table t1 t2)
|
||||
value2termM flat xs (VT vty env s cs)= do
|
||||
ty <- value2termM flat xs vty
|
||||
cs <- forM cs $ \(p,t) -> do
|
||||
let (_,xs',env') = pattVars (length xs,xs,env) p
|
||||
g <- globals
|
||||
t <- value2termM flat xs' (eval g env' s t [])
|
||||
return (p,t)
|
||||
return (T (TTyped ty) cs)
|
||||
value2termM flat xs (VV vty vs)= do
|
||||
ty <- value2termM flat xs vty
|
||||
ts <- mapM (value2termM flat xs) vs
|
||||
return (V ty ts)
|
||||
value2termM flat xs (VS v1 v2 vs) = do
|
||||
t1 <- value2termM flat xs v1
|
||||
t2 <- value2termM flat xs v2
|
||||
foldM (\e1 tnk -> fmap (App e1) (value2termM flat xs tnk)) (S t1 t2) vs
|
||||
value2termM flat xs (VSort s) = return (Sort s)
|
||||
value2termM flat xs (VStr tok) = return (K tok)
|
||||
value2termM flat xs (VInt n) = return (EInt n)
|
||||
value2termM flat xs (VFlt n) = return (EFloat n)
|
||||
value2termM flat xs VEmpty = return Empty
|
||||
value2termM flat xs (VC v1 v2) = do
|
||||
t1 <- value2termM flat xs v1
|
||||
t2 <- value2termM flat xs v2
|
||||
return (C t1 t2)
|
||||
value2termM flat xs (VGlue v1 v2) = do
|
||||
t1 <- value2termM flat xs v1
|
||||
t2 <- value2termM flat xs v2
|
||||
return (Glue t1 t2)
|
||||
value2termM flat xs (VFV i vs) = do
|
||||
v <- variants i vs
|
||||
value2termM flat xs v
|
||||
value2termM flat xs (VPatt min max p) = return (EPatt min max p)
|
||||
value2termM flat xs (VPattType v) = do t <- value2termM flat xs v
|
||||
return (EPattType t)
|
||||
value2termM flat xs (VAlts vd vas) = do
|
||||
d <- value2termM flat xs vd
|
||||
as <- forM vas $ \(vt,vs) -> do
|
||||
t <- value2termM flat xs vt
|
||||
s <- value2termM flat xs vs
|
||||
return (t,s)
|
||||
return (Alts d as)
|
||||
value2termM flat xs (VStrs vs) = do
|
||||
ts <- mapM (value2termM flat xs) vs
|
||||
return (Strs ts)
|
||||
value2termM flat xs (VError msg) = evalError msg
|
||||
value2termM flat xs (VCInts Nothing Nothing) = return (App (QC (cPredef,cInts)) (Meta 0))
|
||||
value2termM flat xs (VCInts (Just min) Nothing) = return (App (QC (cPredef,cInts)) (EInt min))
|
||||
value2termM flat xs (VCInts _ (Just max)) = return (App (QC (cPredef,cInts)) (EInt max))
|
||||
value2termM flat xs v = evalError ("value2termM" <+> ppValue Unqualified 5 v)
|
||||
|
||||
|
||||
pattVars st (PP _ ps) = foldl pattVars st ps
|
||||
pattVars st (PV x) = case st of
|
||||
(i,xs,env) -> (i+1,x:xs,(x,VGen i []):env)
|
||||
pattVars st (PR as) = foldl (\st (_,p) -> pattVars st p) st as
|
||||
pattVars st (PT ty p) = pattVars st p
|
||||
pattVars st (PAs x p) = case st of
|
||||
(i,xs,env) -> pattVars (i+1,x:xs,(x,VGen i []):env) p
|
||||
pattVars st (PImplArg p) = pattVars st p
|
||||
pattVars st (PSeq _ _ p1 _ _ p2) = pattVars (pattVars st p1) p2
|
||||
pattVars st _ = st
|
||||
|
||||
|
||||
ppValue q d (VApp c vs) = prec d 4 (hsep (ppQIdent q c : map (ppValue q 5) vs))
|
||||
ppValue q d (VMeta i vs) = prec d 4 (hsep ((if i > 0 then pp "?" <> pp i else pp "?") : map (ppValue q 5) vs))
|
||||
ppValue q d (VSusp i k vs) = prec d 4 (hsep (pp "#susp" : (if i > 0 then pp "?" <> pp i else pp "?") : map (ppValue q 5) vs))
|
||||
ppValue q d (VGen _ _) = pp "VGen"
|
||||
ppValue q d (VClosure env c t) = pp "[|" <> ppTerm q 4 t <> pp "|]"
|
||||
ppValue q d (VProd _ _ _ _) = pp "VProd"
|
||||
ppValue q d (VRecType _) = pp "VRecType"
|
||||
ppValue q d (VR _) = pp "VR"
|
||||
ppValue q d (VP v l vs) = prec d 5 (hsep (ppValue q 5 v <> '.' <> l : map (ppValue q 5) vs))
|
||||
ppValue q d (VExtR _ _) = pp "VExtR"
|
||||
ppValue q d (VTable _ _) = pp "VTable"
|
||||
ppValue q d (VT t _ _ cs) = "table" <+> ppValue q 0 t <+> '{' $$
|
||||
nest 2 (vcat (punctuate ';' (map (ppCase q) cs))) $$
|
||||
'}'
|
||||
where
|
||||
ppCase q (p,e) = ppPatt q 0 p <+> "=>" <+> ppTerm q 0 e
|
||||
ppValue q d (VV _ _) = pp "VV"
|
||||
ppValue q d (VS v1 v2 vs) = prec d 3 (hsep (hang (ppValue q 3 v1) 2 ("!" <+> ppValue q 4 v2) : map (ppValue q 5) vs))
|
||||
ppValue q d (VSort s) = pp s
|
||||
ppValue q d (VInt n) = pp n
|
||||
ppValue q d (VFlt f) = pp f
|
||||
ppValue q d (VStr s) = ppTerm q d (K s)
|
||||
ppValue q d VEmpty = pp "[]"
|
||||
ppValue q d (VC v1 v2) = prec d 1 (hang (ppValue q 2 v1) 2 ("++" <+> ppValue q 1 v2))
|
||||
ppValue q d (VGlue v1 v2) = prec d 2 (ppValue q 3 v1 <+> '+' <+> ppValue q 2 v2)
|
||||
ppValue q d (VPatt _ _ _) = pp "VPatt"
|
||||
ppValue q d (VPattType _) = pp "VPattType"
|
||||
ppValue q d (VFV i vs) = prec d 4 ("variants" <+> pp i <+> braces (fsep (punctuate ';' (map (ppValue q 0) vs))))
|
||||
ppValue q d (VAlts e xs) = prec d 4 ("pre" <+> braces (ppValue q 0 e <> ';' <+> fsep (punctuate ';' (map (ppAltern q) xs))))
|
||||
ppValue q d (VStrs _) = pp "VStrs"
|
||||
ppValue q d (VSymCat i r rs) = pp '<' <> pp i <> pp ',' <> pp r <> pp '>'
|
||||
ppValue q d (VError msg) = prec d 4 (pp "error" <+> ppTerm q 5 (K (show msg)))
|
||||
ppValue q d (VCInts Nothing Nothing) = prec d 4 (pp "Ints ?")
|
||||
ppValue q d (VCInts (Just min) Nothing) = prec d 4 (pp "Ints" <+> brackets (pp min <> ".."))
|
||||
ppValue q d (VCInts Nothing (Just max)) = prec d 4 (pp "Ints" <+> brackets (".." <> pp max))
|
||||
ppValue q d (VCInts (Just min) (Just max))
|
||||
| min == max = prec d 4 (pp "Ints" <+> min)
|
||||
| otherwise = prec d 4 (pp "Ints" <+> brackets (pp min <> ".." <> pp max))
|
||||
|
||||
ppAltern q (x,y) = ppValue q 0 x <+> '/' <+> ppValue q 0 y
|
||||
|
||||
prec d1 d2 doc
|
||||
| d1 > d2 = parens doc
|
||||
| otherwise = doc
|
||||
|
||||
value2string g v = fmap (\(_,ws,_) -> unwords ws) (value2string' g v False [] [])
|
||||
|
||||
value2string' g (VMeta i vs) b ws qs = CSusp i (\v -> value2string' g (apply g v vs) b ws qs)
|
||||
value2string' g (VSusp i k vs) b ws qs = CSusp i (\v -> value2string' g (apply g (k v) vs) b ws qs)
|
||||
value2string' g (VStr w1) True (w2:ws) qs = Const (False,(w1++w2):ws,qs)
|
||||
value2string' g (VStr w) _ ws qs = Const (False,w :ws,qs)
|
||||
value2string' g VEmpty b ws qs = Const (b,ws,qs)
|
||||
value2string' g (VC v1 v2) b ws qs = concat v1 (value2string' g v2 b ws qs)
|
||||
where
|
||||
concat v1 (Const (b,ws,qs)) = value2string' g v1 b ws qs
|
||||
concat v1 (CFV i vs) = CFV i [concat v1 v2 | v2 <- vs]
|
||||
concat v1 res = res
|
||||
value2string' g (VApp q []) b ws qs
|
||||
| q == (cPredef,cNonExist) = NonExist
|
||||
value2string' g (VApp q []) b ws qs
|
||||
| q == (cPredef,cSOFT_SPACE) = if null ws
|
||||
then Const (b,ws,q:qs)
|
||||
else Const (b,ws,qs)
|
||||
value2string' g (VApp q []) b ws qs
|
||||
| q == (cPredef,cBIND) || q == (cPredef,cSOFT_BIND)
|
||||
= if null ws
|
||||
then Const (True,ws,q:qs)
|
||||
else Const (True,ws,qs)
|
||||
value2string' g (VApp q []) b ws qs
|
||||
| q == (cPredef,cCAPIT) = capit ws
|
||||
where
|
||||
capit [] = Const (b,[],q:qs)
|
||||
capit ((c:cs) : ws) = Const (b,(toUpper c : cs) : ws,qs)
|
||||
capit ws = Const (b,ws,qs)
|
||||
value2string' g (VApp q []) b ws qs
|
||||
| q == (cPredef,cALL_CAPIT) = all_capit ws
|
||||
where
|
||||
all_capit [] = Const (b,[],q:qs)
|
||||
all_capit (w : ws) = Const (b,map toUpper w : ws,qs)
|
||||
value2string' g (VAlts vd vas) b ws qs =
|
||||
case ws of
|
||||
[] -> value2string' g vd b ws qs
|
||||
(w:_) -> pre vd vas w b ws qs
|
||||
where
|
||||
pre vd [] w = value2string' g vd
|
||||
pre vd ((v,VStrs ss):vas) w
|
||||
| or [startsWith s w | VStr s <- ss] = value2string' g v
|
||||
| otherwise = pre vd vas w
|
||||
value2string' g (VFV s vs) b ws qs =
|
||||
CFV s [value2string' g v b ws qs | v <- vs]
|
||||
value2string' _ _ _ _ _ = RunTime
|
||||
|
||||
startsWith [] _ = True
|
||||
startsWith (x:xs) (y:ys)
|
||||
| x == y = startsWith xs ys
|
||||
startsWith _ _ = False
|
||||
|
||||
string2value s = string2value' (words s)
|
||||
|
||||
string2value' [] = VEmpty
|
||||
string2value' [w] = VStr w
|
||||
string2value' (w:ws) = VC (VStr w) (string2value' ws)
|
||||
|
||||
value2int g (VMeta i vs) = CSusp i (\v -> value2int g (apply g v vs))
|
||||
value2int g (VSusp i k vs) = CSusp i (\v -> value2int g (apply g (k v) vs))
|
||||
value2int g (VInt n) = Const n
|
||||
value2int g (VFV s vs) = CFV s (map (value2int g) vs)
|
||||
value2int g _ = RunTime
|
||||
|
||||
newtype Choice = Choice Integer deriving (Eq,Ord,Pretty)
|
||||
|
||||
unit :: Choice
|
||||
unit = Choice 1
|
||||
|
||||
split :: Choice -> (Choice,Choice)
|
||||
split (Choice c) = (Choice (2*c), Choice (2*c+1))
|
||||
|
||||
split4 :: Choice -> (Choice,Choice,Choice,Choice)
|
||||
split4 (Choice c) = (Choice (4*c), Choice (4*c+1), Choice (4*c+2), Choice (4*c+3))
|
||||
|
||||
mapC :: (Choice -> a -> b) -> Choice -> [a] -> [b]
|
||||
mapC f c [] = []
|
||||
mapC f c [x] = [f c x]
|
||||
mapC f c (x:xs) =
|
||||
let (!c1,!c2) = split c
|
||||
in f c1 x : mapC f c2 xs
|
||||
|
||||
mapCM :: Monad m => (Choice -> a -> m b) -> Choice -> [a] -> m [b]
|
||||
mapCM f c [] = return []
|
||||
mapCM f c [x] = do y <- f c x
|
||||
return [y]
|
||||
mapCM f c (x:xs) = do
|
||||
let (!c1,!c2) = split c
|
||||
y <- f c1 x
|
||||
ys <- mapCM f c2 xs
|
||||
return (y:ys)
|
||||
|
||||
pdArity :: Int -> PredefCombinator Value
|
||||
pdArity n def = \g c args ->
|
||||
case splitAt' n args of
|
||||
Nothing -> RunTime
|
||||
Just (usedArgs, remArgs) ->
|
||||
fmap (\v -> apply g v remArgs) (def g c usedArgs)
|
||||
where
|
||||
abstract i n t
|
||||
| n <= 0 = t
|
||||
| otherwise = let x = identV (rawIdentS "a") i
|
||||
in Abs Explicit x (abstract (i + 1) (n - 1) (App t (Vr x)))
|
||||
@@ -15,7 +15,7 @@ import System.Console.Haskeline (InputT, Settings(..), noCompletion, runInputT,
|
||||
import System.Directory (getAppUserDataDirectory)
|
||||
|
||||
import GF.Compile (batchCompile)
|
||||
import GF.Compile.Compute.Concrete (Globals(Gl), stdPredef, normalFlatForm)
|
||||
import GF.Compile.Compute.Concrete2 (Globals(Gl), stdPredef, normalFlatForm)
|
||||
import GF.Compile.Rename (renameSourceTerm)
|
||||
import GF.Compile.TypeCheck.ConcreteNew (inferLType)
|
||||
import GF.Data.ErrM (Err(..))
|
||||
@@ -30,7 +30,7 @@ import GF.Grammar.Grammar
|
||||
, ModuleStatus(MSComplete)
|
||||
, OpenSpec(OSimple)
|
||||
, Location (NoLoc)
|
||||
, Term
|
||||
, Term(Typed)
|
||||
, prependModule
|
||||
)
|
||||
import GF.Grammar.Lexer (Posn(..), Lang(GF), runLangP)
|
||||
@@ -99,8 +99,12 @@ runRepl' gl@(Gl g _) = do
|
||||
|
||||
command "t" arg = do
|
||||
parseThen g arg $ \main ->
|
||||
execCheck (inferLType gl main) $ \(_, ty) ->
|
||||
outputStrLn $ render (ppTerm Unqualified 0 ty)
|
||||
execCheck (inferLType gl main) $ \res ->
|
||||
forM_ res $ \(t, ty) ->
|
||||
let t' = case t of
|
||||
Typed _ _ -> t
|
||||
t -> Typed t ty
|
||||
in outputStrLn $ render (ppTerm Unqualified 0 t')
|
||||
outputStrLn "" >> repl
|
||||
|
||||
command "q" _ = outputStrLn "Bye!"
|
||||
@@ -111,7 +115,7 @@ runRepl' gl@(Gl g _) = do
|
||||
|
||||
evalPrintLoop code = do -- TODO bindings
|
||||
parseThen g code $ \main ->
|
||||
execCheck (inferLType gl main >>= \(t, _) -> normalFlatForm gl t) $ \nfs ->
|
||||
execCheck (inferLType gl main >>= \((t, _):_) -> normalFlatForm gl t) $ \nfs ->
|
||||
forM_ (zip [1..] nfs) $ \(i, nf) ->
|
||||
outputStrLn $ show i ++ ". " ++ render (ppTerm Unqualified 0 nf)
|
||||
outputStrLn "" >> repl
|
||||
@@ -138,4 +142,5 @@ runRepl (ReplOpts noPrelude inputFiles) = do
|
||||
, mseqs = Nothing
|
||||
, jments = Map.empty
|
||||
}
|
||||
runRepl' (Gl (prependModule g0 (replModName, modInfo)) (if noPrelude then Map.empty else stdPredef))
|
||||
g = Gl (prependModule g0 (replModName, modInfo)) (if noPrelude then Map.empty else stdPredef g)
|
||||
runRepl' g
|
||||
|
||||
File diff suppressed because it is too large
Load Diff
@@ -711,8 +711,8 @@ ERHS3 :: { ERHS }
|
||||
|
||||
NLG :: { Map.Map Ident Info }
|
||||
: ListNLGDef { Map.fromList $1 }
|
||||
| Posn Tag Posn { Map.singleton (identS "main") (ResOper Nothing (Just (mkL $1 $3 (Abs Explicit (identS "qid") (Abs Explicit (identS "lang") $2))))) }
|
||||
| Posn Exp Posn { Map.singleton (identS "main") (ResOper Nothing (Just (mkL $1 $3 (Abs Explicit (identS "qid") (Abs Explicit (identS "lang") $2))))) }
|
||||
| Posn Tag Posn { Map.singleton (identS "main") (ResOper Nothing (Just (mkL $1 $3 $2))) }
|
||||
| Posn Exp Posn { Map.singleton (identS "main") (ResOper Nothing (Just (mkL $1 $3 $2))) }
|
||||
|
||||
ListNLGDef :: { [(Ident,Info)] }
|
||||
ListNLGDef
|
||||
|
||||
@@ -107,6 +107,7 @@ library
|
||||
GF.Compile.CFGtoPGF
|
||||
GF.Compile.CheckGrammar
|
||||
GF.Compile.Compute.Concrete
|
||||
GF.Compile.Compute.Concrete2
|
||||
GF.Compile.ExampleBased
|
||||
GF.Compile.Export
|
||||
GF.Compile.GenerateBC
|
||||
|
||||
Reference in New Issue
Block a user