|
|
|
|
@@ -1,9 +1,11 @@
|
|
|
|
|
{-# LANGUAGE RankNTypes #-}
|
|
|
|
|
|
|
|
|
|
-- | Functions for computing the values of terms in the concrete syntax, in
|
|
|
|
|
-- | preparation for PMCFG generation.
|
|
|
|
|
module GF.Compile.Compute.Concrete
|
|
|
|
|
(GlobalEnv, GLocation, resourceValues, geLoc, geGrammar,
|
|
|
|
|
normalForm,
|
|
|
|
|
Value(..), Bind(..), Env, value2term, eval, vapply
|
|
|
|
|
Value(..), Env, value2term, eval
|
|
|
|
|
) where
|
|
|
|
|
import Prelude hiding ((<>)) -- GHC 8.4.1 clash with Text.PrettyPrint
|
|
|
|
|
|
|
|
|
|
@@ -18,573 +20,140 @@ import GF.Data.Str(Str,glueStr,str2strings,str,sstr,plusStr,strTok)
|
|
|
|
|
import GF.Data.Operations(Err,err,errIn,maybeErr,mapPairsM)
|
|
|
|
|
import GF.Data.Utilities(mapFst,mapSnd)
|
|
|
|
|
import GF.Infra.Option
|
|
|
|
|
import Control.Monad(ap,liftM,liftM2) -- ,unless,mplus
|
|
|
|
|
import Data.List (findIndex,intersect,nub,elemIndex,(\\)) --,isInfixOf
|
|
|
|
|
--import Data.Char (isUpper,toUpper,toLower)
|
|
|
|
|
import GF.Text.Pretty
|
|
|
|
|
import Data.STRef
|
|
|
|
|
import Control.Monad
|
|
|
|
|
import Control.Monad.ST
|
|
|
|
|
import Control.Applicative
|
|
|
|
|
import qualified Data.Map as Map
|
|
|
|
|
import Debug.Trace(trace)
|
|
|
|
|
|
|
|
|
|
-- * Main entry points
|
|
|
|
|
|
|
|
|
|
normalForm :: GlobalEnv -> L Ident -> Term -> Term
|
|
|
|
|
normalForm (GE gr rv opts _) loc = err (bugloc loc) id . nfx (GE gr rv opts loc)
|
|
|
|
|
normalForm ge loc t =
|
|
|
|
|
case runEvalM (eval [] t [] >>= value2term 0) of
|
|
|
|
|
[t] -> t
|
|
|
|
|
ts -> FV ts
|
|
|
|
|
|
|
|
|
|
nfx :: GlobalEnv -> Term -> Err Term
|
|
|
|
|
nfx env@(GE _ _ _ loc) t = do
|
|
|
|
|
v <- eval env [] t
|
|
|
|
|
return (value2term loc [] v)
|
|
|
|
|
-- Old value2term error message:
|
|
|
|
|
-- Left i -> fail ("variable #"++show i++" is out of scope")
|
|
|
|
|
eval env (Vr x) vs = case lookup x env of
|
|
|
|
|
Just tnk -> force tnk vs
|
|
|
|
|
Nothing -> error "Unknown variable"
|
|
|
|
|
eval env (Con f) vs = return (VApp f vs)
|
|
|
|
|
eval env (K t) vs = return (VStr t)
|
|
|
|
|
eval env (App t1 t2) vs = do tnk <- newThunk env t2
|
|
|
|
|
eval env t1 (tnk : vs)
|
|
|
|
|
eval env (Abs b x t) [] = return (VClosure env (Abs b x t))
|
|
|
|
|
eval env (Abs b x t) (v:vs) = eval ((x,v):env) t vs
|
|
|
|
|
eval env (Meta i) vs = do tnk <- newMeta i
|
|
|
|
|
return (VMeta tnk env vs)
|
|
|
|
|
eval env (Typed t ty) vs = eval env t vs
|
|
|
|
|
eval env (C t1 t2) vs = do tnk1 <- newThunk env t1
|
|
|
|
|
tnk2 <- newThunk env t2
|
|
|
|
|
return (VC tnk1 tnk2)
|
|
|
|
|
eval env (FV ts) vs = msum [eval env t vs | t <- ts]
|
|
|
|
|
|
|
|
|
|
eval :: GlobalEnv -> Env -> Term -> Err Value
|
|
|
|
|
eval (GE gr rvs opts loc) env t = ($ (map snd env)) # value cenv t
|
|
|
|
|
where
|
|
|
|
|
cenv = CE gr rvs opts loc (map fst env)
|
|
|
|
|
apply v [] = return v
|
|
|
|
|
apply (VApp f vs0) vs = return (VApp f (vs0++vs))
|
|
|
|
|
apply (VMeta m env vs0) vs = return (VMeta m env (vs0++vs))
|
|
|
|
|
apply (VGen i vs0) vs = return (VGen i (vs0++vs))
|
|
|
|
|
apply (VClosure env (Abs b x t)) (v:vs) = eval ((x,v):env) t vs
|
|
|
|
|
|
|
|
|
|
--apply env = apply' env
|
|
|
|
|
|
|
|
|
|
--------------------------------------------------------------------------------
|
|
|
|
|
value2term i (VApp f tnks) =
|
|
|
|
|
foldM (\e1 tnk -> fmap (App e1) (force tnk [] >>= value2term i)) (Con f) tnks
|
|
|
|
|
value2term i (VMeta m env tnks) = do
|
|
|
|
|
res <- zonk m tnks
|
|
|
|
|
case res of
|
|
|
|
|
Right i -> foldM (\e1 tnk -> fmap (App e1) (force tnk [] >>= value2term i)) (Meta i) tnks
|
|
|
|
|
Left v -> value2term i v
|
|
|
|
|
value2term i (VGen j tnks) =
|
|
|
|
|
foldM (\e1 tnk -> fmap (App e1) (force tnk [] >>= value2term i)) (Vr (identS ('v':show j))) tnks
|
|
|
|
|
value2term i (VClosure env (Abs b x t)) = do
|
|
|
|
|
tnk <- newGen i
|
|
|
|
|
v <- eval ((x,tnk):env) t []
|
|
|
|
|
t <- value2term (i+1) v
|
|
|
|
|
return (Abs b (identS ('v':show i)) t)
|
|
|
|
|
value2term i (VStr tok) = return (K tok)
|
|
|
|
|
value2term i (VC tnk1 tnk2) = do
|
|
|
|
|
t1 <- force tnk1 [] >>= value2term i
|
|
|
|
|
t2 <- force tnk2 [] >>= value2term i
|
|
|
|
|
return (C t1 t2)
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
-----------------------------------------------------------------------
|
|
|
|
|
-- * Environments
|
|
|
|
|
|
|
|
|
|
type ResourceValues = Map.Map ModuleName (Map.Map Ident (Err Value))
|
|
|
|
|
|
|
|
|
|
data GlobalEnv = GE Grammar ResourceValues Options GLocation
|
|
|
|
|
data CompleteEnv = CE {srcgr::Grammar,rvs::ResourceValues,
|
|
|
|
|
opts::Options,
|
|
|
|
|
gloc::GLocation,local::LocalScope}
|
|
|
|
|
data GlobalEnv = GE Grammar Options GLocation
|
|
|
|
|
type GLocation = L Ident
|
|
|
|
|
type LocalScope = [Ident]
|
|
|
|
|
type Stack = [Value]
|
|
|
|
|
type OpenValue = Stack->Value
|
|
|
|
|
|
|
|
|
|
geLoc (GE _ _ _ loc) = loc
|
|
|
|
|
geGrammar (GE gr _ _ _) = gr
|
|
|
|
|
|
|
|
|
|
ext b env = env{local=b:local env}
|
|
|
|
|
extend bs env = env{local=bs++local env}
|
|
|
|
|
global env = GE (srcgr env) (rvs env) (opts env) (gloc env)
|
|
|
|
|
|
|
|
|
|
var :: CompleteEnv -> Ident -> Err OpenValue
|
|
|
|
|
var env x = maybe unbound pick' (elemIndex x (local env))
|
|
|
|
|
where
|
|
|
|
|
unbound = fail ("Unknown variable: "++showIdent x)
|
|
|
|
|
pick' i = return $ \ vs -> maybe (err i vs) ok (pick i vs)
|
|
|
|
|
err i vs = bug $ "Stack problem: "++showIdent x++": "
|
|
|
|
|
++unwords (map showIdent (local env))
|
|
|
|
|
++" => "++show (i,length vs)
|
|
|
|
|
ok v = --trace ("var "++show x++" = "++show v) $
|
|
|
|
|
v
|
|
|
|
|
|
|
|
|
|
pick :: Int -> Stack -> Maybe Value
|
|
|
|
|
pick 0 (v:_) = Just v
|
|
|
|
|
pick i (_:vs) = pick (i-1) vs
|
|
|
|
|
pick i vs = Nothing -- bug $ "pick "++show (i,vs)
|
|
|
|
|
|
|
|
|
|
resource env (m,c) =
|
|
|
|
|
-- err bug id $
|
|
|
|
|
if isPredefCat c
|
|
|
|
|
then value0 env =<< lockRecType c defLinType -- hmm
|
|
|
|
|
else maybe e id $ Map.lookup c =<< Map.lookup m (rvs env)
|
|
|
|
|
where e = fail $ "Not found: "++render m++"."++showIdent c
|
|
|
|
|
geLoc (GE _ _ loc) = loc
|
|
|
|
|
geGrammar (GE gr _ _ ) = gr
|
|
|
|
|
|
|
|
|
|
-- | Convert operators once, not every time they are looked up
|
|
|
|
|
resourceValues :: Options -> SourceGrammar -> GlobalEnv
|
|
|
|
|
resourceValues opts gr = env
|
|
|
|
|
where
|
|
|
|
|
env = GE gr rvs opts (L NoLoc identW)
|
|
|
|
|
rvs = Map.mapWithKey moduleResources (moduleMap gr)
|
|
|
|
|
moduleResources m = Map.mapWithKey (moduleResource m) . jments
|
|
|
|
|
moduleResource m c _info = do L l t <- lookupResDefLoc gr (m,c)
|
|
|
|
|
let loc = L l c
|
|
|
|
|
qloc = L l (Q (m,c))
|
|
|
|
|
eval (GE gr rvs opts loc) [] (traceRes qloc t)
|
|
|
|
|
|
|
|
|
|
traceRes = if flag optTrace opts
|
|
|
|
|
then traceResource
|
|
|
|
|
else const id
|
|
|
|
|
|
|
|
|
|
-- * Tracing
|
|
|
|
|
|
|
|
|
|
-- | Insert a call to the trace function under the top-level lambdas
|
|
|
|
|
traceResource (L l q) t =
|
|
|
|
|
case termFormCnc t of
|
|
|
|
|
(abs,body) -> mkAbs abs (mkApp traceQ [args,body])
|
|
|
|
|
where
|
|
|
|
|
args = R $ tuple2record (K lstr:[Vr x|(bt,x)<-abs,bt==Explicit])
|
|
|
|
|
lstr = render (l<>":"<>ppTerm Qualified 0 q)
|
|
|
|
|
traceQ = Q (cPredef,cTrace)
|
|
|
|
|
|
|
|
|
|
-- * Computing values
|
|
|
|
|
|
|
|
|
|
-- | Computing the value of a top-level term
|
|
|
|
|
value0 :: CompleteEnv -> Term -> Err Value
|
|
|
|
|
value0 env = eval (global env) []
|
|
|
|
|
|
|
|
|
|
-- | Computing the value of a term
|
|
|
|
|
value :: CompleteEnv -> Term -> Err OpenValue
|
|
|
|
|
value env t0 =
|
|
|
|
|
-- Each terms is traversed only once by this function, using only statically
|
|
|
|
|
-- available information. Notably, the values of lambda bound variables
|
|
|
|
|
-- will be unknown during the term traversal phase.
|
|
|
|
|
-- The result is an OpenValue, which is a function that may be applied many
|
|
|
|
|
-- times to different dynamic values, but without the term traversal overhead
|
|
|
|
|
-- and without recomputing other statically known information.
|
|
|
|
|
-- For this to work, there should be no recursive calls under lambdas here.
|
|
|
|
|
-- Whenever we need to construct the OpenValue function with an explicit
|
|
|
|
|
-- lambda, we have to lift the recursive calls outside the lambda.
|
|
|
|
|
-- (See e.g. the rules for Let, Prod and Abs)
|
|
|
|
|
{-
|
|
|
|
|
trace (render $ text "value"<+>sep [ppL (gloc env)<>text ":",
|
|
|
|
|
brackets (fsep (map ppIdent (local env))),
|
|
|
|
|
ppTerm Unqualified 10 t0]) $
|
|
|
|
|
--}
|
|
|
|
|
errIn (render t0) $
|
|
|
|
|
case t0 of
|
|
|
|
|
Vr x -> var env x
|
|
|
|
|
Q x@(m,f)
|
|
|
|
|
| m == cPredef -> if f==cErrorType -- to be removed
|
|
|
|
|
then let p = identS "P"
|
|
|
|
|
in const # value0 env (mkProd [(Implicit,p,typeType)] (Vr p) [])
|
|
|
|
|
else if f==cPBool
|
|
|
|
|
then const # resource env x
|
|
|
|
|
else const . flip VApp [] # predef f
|
|
|
|
|
| otherwise -> const # resource env x --valueResDef (fst env) x
|
|
|
|
|
QC x -> return $ const (VCApp x [])
|
|
|
|
|
App e1 e2 -> apply' env e1 . (:[]) =<< value env e2
|
|
|
|
|
Let (x,(oty,t)) body -> do vb <- value (ext x env) body
|
|
|
|
|
vt <- value env t
|
|
|
|
|
return $ \ vs -> vb (vt vs:vs)
|
|
|
|
|
Meta i -> return $ \ vs -> VMeta i (zip (local env) vs) []
|
|
|
|
|
Prod bt x t1 t2 ->
|
|
|
|
|
do vt1 <- value env t1
|
|
|
|
|
vt2 <- value (ext x env) t2
|
|
|
|
|
return $ \ vs -> VProd bt (vt1 vs) x $ Bind $ \ vx -> vt2 (vx:vs)
|
|
|
|
|
Abs bt x t -> do vt <- value (ext x env) t
|
|
|
|
|
return $ VAbs bt x . Bind . \ vs vx -> vt (vx:vs)
|
|
|
|
|
EInt n -> return $ const (VInt n)
|
|
|
|
|
EFloat f -> return $ const (VFloat f)
|
|
|
|
|
K s -> return $ const (VString s)
|
|
|
|
|
Empty -> return $ const (VString "")
|
|
|
|
|
Sort s | s == cTok -> return $ const (VSort cStr) -- to be removed
|
|
|
|
|
| otherwise -> return $ const (VSort s)
|
|
|
|
|
ImplArg t -> (VImplArg.) # value env t
|
|
|
|
|
Table p res -> liftM2 VTblType # value env p <# value env res
|
|
|
|
|
RecType rs -> do lovs <- mapPairsM (value env) rs
|
|
|
|
|
return $ \vs->VRecType $ mapSnd ($vs) lovs
|
|
|
|
|
t@(ExtR t1 t2) -> ((extR t.)# both id) # both (value env) (t1,t2)
|
|
|
|
|
FV ts -> ((vfv .) # sequence) # mapM (value env) ts
|
|
|
|
|
R as -> do lovs <- mapPairsM (value env.snd) as
|
|
|
|
|
return $ \ vs->VRec $ mapSnd ($vs) lovs
|
|
|
|
|
T i cs -> valueTable env i cs
|
|
|
|
|
V ty ts -> do pvs <- paramValues env ty
|
|
|
|
|
((VV ty pvs .) . sequence) # mapM (value env) ts
|
|
|
|
|
C t1 t2 -> ((ok2p vconcat.) # both id) # both (value env) (t1,t2)
|
|
|
|
|
S t1 t2 -> ((select env.) # both id) # both (value env) (t1,t2)
|
|
|
|
|
P t l -> --maybe (bug $ "project "++show l++" from "++show v) id $
|
|
|
|
|
do ov <- value env t
|
|
|
|
|
return $ \ vs -> let v = ov vs
|
|
|
|
|
in maybe (VP v l) id (proj l v)
|
|
|
|
|
Alts t tts -> (\v vts -> VAlts # v <# mapM (both id) vts) # value env t <# mapM (both (value env)) tts
|
|
|
|
|
Strs ts -> ((VStrs.) # sequence) # mapM (value env) ts
|
|
|
|
|
Glue t1 t2 -> ((ok2p (glue env).) # both id) # both (value env) (t1,t2)
|
|
|
|
|
ELin c r -> (unlockVRec (gloc env) c.) # value env r
|
|
|
|
|
EPatt p -> return $ const (VPatt p) -- hmm
|
|
|
|
|
EPattType ty -> do vt <- value env ty
|
|
|
|
|
return (VPattType . vt)
|
|
|
|
|
Typed t ty -> value env t
|
|
|
|
|
t -> fail.render $ "value"<+>ppTerm Unqualified 10 t $$ show t
|
|
|
|
|
|
|
|
|
|
vconcat vv@(v1,v2) =
|
|
|
|
|
case vv of
|
|
|
|
|
(VString "",_) -> v2
|
|
|
|
|
(_,VString "") -> v1
|
|
|
|
|
(VApp NonExist _,_) -> v1
|
|
|
|
|
(_,VApp NonExist _) -> v2
|
|
|
|
|
_ -> VC v1 v2
|
|
|
|
|
|
|
|
|
|
proj l v | isLockLabel l = return (VRec [])
|
|
|
|
|
---- a workaround 18/2/2005: take this away and find the reason
|
|
|
|
|
---- why earlier compilation destroys the lock field
|
|
|
|
|
proj l v =
|
|
|
|
|
case v of
|
|
|
|
|
VFV vs -> liftM vfv (mapM (proj l) vs)
|
|
|
|
|
VRec rs -> lookup l rs
|
|
|
|
|
-- VExtR v1 v2 -> proj l v2 `mplus` proj l v1 -- hmm
|
|
|
|
|
VS (VV pty pvs rs) v2 -> flip VS v2 . VV pty pvs # mapM (proj l) rs
|
|
|
|
|
_ -> return (ok1 VP v l)
|
|
|
|
|
|
|
|
|
|
ok1 f v1@(VError {}) _ = v1
|
|
|
|
|
ok1 f v1 v2 = f v1 v2
|
|
|
|
|
|
|
|
|
|
ok2 f v1@(VError {}) _ = v1
|
|
|
|
|
ok2 f _ v2@(VError {}) = v2
|
|
|
|
|
ok2 f v1 v2 = f v1 v2
|
|
|
|
|
|
|
|
|
|
ok2p f (v1@VError {},_) = v1
|
|
|
|
|
ok2p f (_,v2@VError {}) = v2
|
|
|
|
|
ok2p f vv = f vv
|
|
|
|
|
|
|
|
|
|
unlockVRec loc c0 v0 = v0
|
|
|
|
|
{-
|
|
|
|
|
unlockVRec loc c0 v0 = unlockVRec' c0 v0
|
|
|
|
|
where
|
|
|
|
|
unlockVRec' ::Ident -> Value -> Value
|
|
|
|
|
unlockVRec' c v =
|
|
|
|
|
case v of
|
|
|
|
|
-- VClosure env t -> err bug (VClosure env) (unlockRecord c t)
|
|
|
|
|
VAbs bt x (Bind f) -> VAbs bt x (Bind $ \ v -> unlockVRec' c (f v))
|
|
|
|
|
VRec rs -> plusVRec rs lock
|
|
|
|
|
-- _ -> VExtR v (VRec lock) -- hmm
|
|
|
|
|
_ -> {-trace (render $ ppL loc $ "unlock non-record "++show v0)-} v -- hmm
|
|
|
|
|
-- _ -> bugloc loc $ "unlock non-record "++show v0
|
|
|
|
|
where
|
|
|
|
|
lock = [(lockLabel c,VRec [])]
|
|
|
|
|
-}
|
|
|
|
|
|
|
|
|
|
-- suspicious, but backwards compatible
|
|
|
|
|
plusVRec rs1 rs2 = VRec ([(l,v)|(l,v)<-rs1,l `notElem` ls2] ++ rs2)
|
|
|
|
|
where ls2 = map fst rs2
|
|
|
|
|
|
|
|
|
|
extR t vv =
|
|
|
|
|
case vv of
|
|
|
|
|
(VFV vs,v2) -> vfv [extR t (v1,v2)|v1<-vs]
|
|
|
|
|
(v1,VFV vs) -> vfv [extR t (v1,v2)|v2<-vs]
|
|
|
|
|
(VRecType rs1, VRecType rs2) ->
|
|
|
|
|
case intersect (map fst rs1) (map fst rs2) of
|
|
|
|
|
[] -> VRecType (rs1 ++ rs2)
|
|
|
|
|
ls -> error $ "clash"<+>show ls
|
|
|
|
|
(VRec rs1, VRec rs2) -> plusVRec rs1 rs2
|
|
|
|
|
(v1 , VRec [(l,_)]) | isLockLabel l -> v1 -- hmm
|
|
|
|
|
(VS (VV t pvs vs) s,v2) -> VS (VV t pvs [extR t (v1,v2)|v1<-vs]) s
|
|
|
|
|
-- (v1,v2) -> ok2 VExtR v1 v2 -- hmm
|
|
|
|
|
(v1,v2) -> error $ "not records" $$ show v1 $$ show v2
|
|
|
|
|
where
|
|
|
|
|
error explain = ppbug $ "The term" <+> t
|
|
|
|
|
<+> "is not reducible" $$ explain
|
|
|
|
|
|
|
|
|
|
glue env (v1,v2) = glu v1 v2
|
|
|
|
|
where
|
|
|
|
|
glu v1 v2 =
|
|
|
|
|
case (v1,v2) of
|
|
|
|
|
(VFV vs,v2) -> vfv [glu v1 v2|v1<-vs]
|
|
|
|
|
(v1,VFV vs) -> vfv [glu v1 v2|v2<-vs]
|
|
|
|
|
(VString s1,VString s2) -> VString (s1++s2)
|
|
|
|
|
(v1,VAlts d vs) -> VAlts (glx d) [(glx v,c) | (v,c) <- vs]
|
|
|
|
|
where glx v2 = glu v1 v2
|
|
|
|
|
(v1@(VAlts {}),v2) ->
|
|
|
|
|
--err (const (ok2 VGlue v1 v2)) id $
|
|
|
|
|
err bug id $
|
|
|
|
|
do y' <- strsFromValue v2
|
|
|
|
|
x' <- strsFromValue v1
|
|
|
|
|
return $ vfv [foldr1 VC (map VString (str2strings (glueStr v u))) | v <- x', u <- y']
|
|
|
|
|
(VC va vb,v2) -> VC va (glu vb v2)
|
|
|
|
|
(v1,VC va vb) -> VC (glu v1 va) vb
|
|
|
|
|
(VS (VV ty pvs vs) vb,v2) -> VS (VV ty pvs [glu v v2|v<-vs]) vb
|
|
|
|
|
(v1,VS (VV ty pvs vs) vb) -> VS (VV ty pvs [glu v1 v|v<-vs]) vb
|
|
|
|
|
(v1@(VApp NonExist _),_) -> v1
|
|
|
|
|
(_,v2@(VApp NonExist _)) -> v2
|
|
|
|
|
-- (v1,v2) -> ok2 VGlue v1 v2
|
|
|
|
|
(v1,v2) -> if flag optPlusAsBind (opts env)
|
|
|
|
|
then VC v1 (VC (VApp BIND []) v2)
|
|
|
|
|
else let loc = gloc env
|
|
|
|
|
vt v = value2term loc (local env) v
|
|
|
|
|
-- Old value2term error message:
|
|
|
|
|
-- Left i -> Error ('#':show i)
|
|
|
|
|
originalMsg = render $ ppL loc (hang "unsupported token gluing" 4
|
|
|
|
|
(Glue (vt v1) (vt v2)))
|
|
|
|
|
term = render $ pp $ Glue (vt v1) (vt v2)
|
|
|
|
|
in error $ unlines
|
|
|
|
|
[originalMsg
|
|
|
|
|
,""
|
|
|
|
|
,"There was a problem in the expression `"++term++"`, either:"
|
|
|
|
|
,"1) You are trying to use + on runtime arguments, possibly via an oper."
|
|
|
|
|
,"2) One of the arguments in `"++term++"` is a bound variable from pattern matching a string, but the cases are non-exhaustive."
|
|
|
|
|
,"For more help see https://github.com/GrammaticalFramework/gf-core/tree/master/doc/errors/gluing.md"
|
|
|
|
|
]
|
|
|
|
|
resourceValues opts gr = GE gr opts (L NoLoc identW)
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
-- | to get a string from a value that represents a sequence of terminals
|
|
|
|
|
strsFromValue :: Value -> Err [Str]
|
|
|
|
|
strsFromValue t = case t of
|
|
|
|
|
VString s -> return [str s]
|
|
|
|
|
VC s t -> do
|
|
|
|
|
s' <- strsFromValue s
|
|
|
|
|
t' <- strsFromValue t
|
|
|
|
|
return [plusStr x y | x <- s', y <- t']
|
|
|
|
|
{-
|
|
|
|
|
VGlue s t -> do
|
|
|
|
|
s' <- strsFromValue s
|
|
|
|
|
t' <- strsFromValue t
|
|
|
|
|
return [glueStr x y | x <- s', y <- t']
|
|
|
|
|
-}
|
|
|
|
|
VAlts d vs -> do
|
|
|
|
|
d0 <- strsFromValue d
|
|
|
|
|
v0 <- mapM (strsFromValue . fst) vs
|
|
|
|
|
c0 <- mapM (strsFromValue . snd) vs
|
|
|
|
|
--let vs' = zip v0 c0
|
|
|
|
|
return [strTok (str2strings def) vars |
|
|
|
|
|
def <- d0,
|
|
|
|
|
vars <- [[(str2strings v, map sstr c) | (v,c) <- zip vv c0] |
|
|
|
|
|
vv <- sequence v0]
|
|
|
|
|
]
|
|
|
|
|
VFV ts -> concat # mapM strsFromValue ts
|
|
|
|
|
VStrs ts -> concat # mapM strsFromValue ts
|
|
|
|
|
-----------------------------------------------------------------------
|
|
|
|
|
-- * Evaluation monad
|
|
|
|
|
|
|
|
|
|
_ -> fail ("cannot get Str from value " ++ show t)
|
|
|
|
|
type MetaThunks s = Map.Map MetaId (Thunk s)
|
|
|
|
|
|
|
|
|
|
vfv vs = case nub vs of
|
|
|
|
|
[v] -> v
|
|
|
|
|
vs -> VFV vs
|
|
|
|
|
newtype EvalM s a = EvalM (forall r . (a -> MetaThunks s -> r -> ST s r) -> MetaThunks s -> r -> ST s r)
|
|
|
|
|
|
|
|
|
|
select env vv =
|
|
|
|
|
case vv of
|
|
|
|
|
(v1,VFV vs) -> vfv [select env (v1,v2)|v2<-vs]
|
|
|
|
|
(VFV vs,v2) -> vfv [select env (v1,v2)|v1<-vs]
|
|
|
|
|
(v1@(VV pty vs rs),v2) ->
|
|
|
|
|
err (const (VS v1 v2)) id $
|
|
|
|
|
do --ats <- allParamValues (srcgr env) pty
|
|
|
|
|
--let vs = map (value0 env) ats
|
|
|
|
|
i <- maybeErr "no match" $ findIndex (==v2) vs
|
|
|
|
|
return (ix (gloc env) "select" rs i)
|
|
|
|
|
(VT _ _ [(PW,Bind b)],_) -> {-trace "eliminate wild card table" $-} b []
|
|
|
|
|
(v1@(VT _ _ cs),v2) ->
|
|
|
|
|
err (\_->ok2 VS v1 v2) (err bug id . valueMatch env) $
|
|
|
|
|
match (gloc env) cs v2
|
|
|
|
|
(VS (VV pty pvs rs) v12,v2) -> VS (VV pty pvs [select env (v11,v2)|v11<-rs]) v12
|
|
|
|
|
(v1,v2) -> ok2 VS v1 v2
|
|
|
|
|
instance Functor (EvalM s) where
|
|
|
|
|
fmap f (EvalM g) = EvalM (\k -> g (k . f))
|
|
|
|
|
|
|
|
|
|
match loc cs v =
|
|
|
|
|
err bad return (matchPattern cs (value2term loc [] v))
|
|
|
|
|
-- Old value2term error message:
|
|
|
|
|
-- Left i -> bad ("variable #"++show i++" is out of scope")
|
|
|
|
|
where
|
|
|
|
|
bad = fail . ("In pattern matching: "++)
|
|
|
|
|
instance Applicative (EvalM s) where
|
|
|
|
|
pure x = EvalM (\k -> k x)
|
|
|
|
|
(EvalM f) <*> (EvalM x) = EvalM (\k -> f (\f -> x (\x -> k (f x))))
|
|
|
|
|
|
|
|
|
|
valueMatch :: CompleteEnv -> (Bind Env,Substitution) -> Err Value
|
|
|
|
|
valueMatch env (Bind f,env') = f # mapPairsM (value0 env) env'
|
|
|
|
|
instance Monad (EvalM s) where
|
|
|
|
|
(EvalM f) >>= g = EvalM (\k -> f (\x -> case g x of
|
|
|
|
|
EvalM g -> g k))
|
|
|
|
|
|
|
|
|
|
valueTable :: CompleteEnv -> TInfo -> [Case] -> Err OpenValue
|
|
|
|
|
valueTable env i cs =
|
|
|
|
|
case i of
|
|
|
|
|
TComp ty -> do pvs <- paramValues env ty
|
|
|
|
|
((VV ty pvs .) # sequence) # mapM (value env.snd) cs
|
|
|
|
|
_ -> do ty <- getTableType i
|
|
|
|
|
cs' <- mapM valueCase cs
|
|
|
|
|
err (dynamic cs' ty) return (convert cs' ty)
|
|
|
|
|
where
|
|
|
|
|
dynamic cs' ty _ = cases cs' # value env ty
|
|
|
|
|
instance Alternative (EvalM s) where
|
|
|
|
|
empty = EvalM (\k _ -> return)
|
|
|
|
|
(EvalM f) <|> (EvalM g) = EvalM (\k mt r -> f k mt r >>= \r -> g k mt r)
|
|
|
|
|
|
|
|
|
|
cases cs' vty vs = err keep ($vs) (convertv cs' (vty vs))
|
|
|
|
|
where
|
|
|
|
|
keep msg = --trace (msg++"\n"++render (ppTerm Unqualified 0 (T i cs))) $
|
|
|
|
|
VT wild (vty vs) (mapSnd ($vs) cs')
|
|
|
|
|
|
|
|
|
|
wild = case i of TWild _ -> True; _ -> False
|
|
|
|
|
|
|
|
|
|
convertv cs' vty =
|
|
|
|
|
convert' cs' =<< paramValues'' env (value2term (gloc env) [] vty)
|
|
|
|
|
-- Old value2term error message: Left i -> fail ("variable #"++show i++" is out of scope")
|
|
|
|
|
|
|
|
|
|
convert cs' ty = convert' cs' =<< paramValues' env ty
|
|
|
|
|
|
|
|
|
|
convert' cs' ((pty,vs),pvs) =
|
|
|
|
|
do sts <- mapM (matchPattern cs') vs
|
|
|
|
|
return $ \ vs -> VV pty pvs $ map (err bug id . valueMatch env)
|
|
|
|
|
(mapFst ($vs) sts)
|
|
|
|
|
|
|
|
|
|
valueCase (p,t) = do p' <- measurePatt # inlinePattMacro p
|
|
|
|
|
pvs <- linPattVars p'
|
|
|
|
|
vt <- value (extend pvs env) t
|
|
|
|
|
return (p',\vs-> Bind $ \bs-> vt (push' p' bs pvs vs))
|
|
|
|
|
|
|
|
|
|
inlinePattMacro p =
|
|
|
|
|
case p of
|
|
|
|
|
PM qc -> do r <- resource env qc
|
|
|
|
|
case r of
|
|
|
|
|
VPatt p' -> inlinePattMacro p'
|
|
|
|
|
_ -> ppbug $ hang "Expected pattern macro:" 4
|
|
|
|
|
(show r)
|
|
|
|
|
_ -> composPattOp inlinePattMacro p
|
|
|
|
|
instance MonadPlus (EvalM s) where
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
paramValues env ty = snd # paramValues' env ty
|
|
|
|
|
runEvalM :: (forall s . EvalM s a) -> [a]
|
|
|
|
|
runEvalM f = reverse $
|
|
|
|
|
runST (case f of
|
|
|
|
|
EvalM f -> f (\x mt xs -> return (x:xs)) Map.empty [])
|
|
|
|
|
|
|
|
|
|
paramValues' env ty = paramValues'' env =<< nfx (global env) ty
|
|
|
|
|
newThunk env t = EvalM $ \k mt r -> do
|
|
|
|
|
tnk <- newSTRef (Unevaluated env t)
|
|
|
|
|
k tnk mt r
|
|
|
|
|
|
|
|
|
|
paramValues'' env pty = do ats <- allParamValues (srcgr env) pty
|
|
|
|
|
pvs <- mapM (eval (global env) []) ats
|
|
|
|
|
return ((pty,ats),pvs)
|
|
|
|
|
newMeta i = EvalM $ \k mt r ->
|
|
|
|
|
if i == 0
|
|
|
|
|
then do tnk <- newSTRef (Unbound i)
|
|
|
|
|
k tnk mt r
|
|
|
|
|
else case Map.lookup i mt of
|
|
|
|
|
Just tnk -> k tnk mt r
|
|
|
|
|
Nothing -> do tnk <- newSTRef (Unbound i)
|
|
|
|
|
k tnk (Map.insert i tnk mt) r
|
|
|
|
|
|
|
|
|
|
push' p bs xs = if length bs/=length xs
|
|
|
|
|
then bug $ "push "++show (p,bs,xs)
|
|
|
|
|
else push bs xs
|
|
|
|
|
newGen i = EvalM $ \k mt r -> do
|
|
|
|
|
tnk <- newSTRef (Evaluated (VGen i []))
|
|
|
|
|
k tnk mt r
|
|
|
|
|
|
|
|
|
|
push :: Env -> LocalScope -> Stack -> Stack
|
|
|
|
|
push bs [] vs = vs
|
|
|
|
|
push bs (x:xs) vs = maybe err id (lookup x bs):push bs xs vs
|
|
|
|
|
where err = bug $ "Unbound pattern variable "++showIdent x
|
|
|
|
|
force tnk vs = EvalM $ \k mt r -> do
|
|
|
|
|
s <- readSTRef tnk
|
|
|
|
|
case s of
|
|
|
|
|
Unevaluated env t -> case eval env t vs of
|
|
|
|
|
EvalM f -> f (\v mt r -> do writeSTRef tnk (Evaluated v)
|
|
|
|
|
r <- k v mt r
|
|
|
|
|
writeSTRef tnk s
|
|
|
|
|
return r) mt r
|
|
|
|
|
Evaluated v -> case apply v vs of
|
|
|
|
|
EvalM f -> f k mt r
|
|
|
|
|
|
|
|
|
|
apply' :: CompleteEnv -> Term -> [OpenValue] -> Err OpenValue
|
|
|
|
|
apply' env t [] = value env t
|
|
|
|
|
apply' env t vs =
|
|
|
|
|
case t of
|
|
|
|
|
QC x -> return $ \ svs -> VCApp x (map ($svs) vs)
|
|
|
|
|
{-
|
|
|
|
|
Q x@(m,f) | m==cPredef -> return $
|
|
|
|
|
let constr = --trace ("predef "++show x) .
|
|
|
|
|
VApp x
|
|
|
|
|
in \ svs -> maybe constr id (Map.lookup f predefs)
|
|
|
|
|
$ map ($svs) vs
|
|
|
|
|
| otherwise -> do r <- resource env x
|
|
|
|
|
return $ \ svs -> vapply (gloc env) r (map ($svs) vs)
|
|
|
|
|
-}
|
|
|
|
|
App t1 t2 -> apply' env t1 . (:vs) =<< value env t2
|
|
|
|
|
_ -> do fv <- value env t
|
|
|
|
|
return $ \ svs -> vapply (gloc env) (fv svs) (map ($svs) vs)
|
|
|
|
|
|
|
|
|
|
vapply :: GLocation -> Value -> [Value] -> Value
|
|
|
|
|
vapply loc v [] = v
|
|
|
|
|
vapply loc v vs =
|
|
|
|
|
case v of
|
|
|
|
|
VError {} -> v
|
|
|
|
|
-- VClosure env (Abs b x t) -> beta gr env b x t vs
|
|
|
|
|
VAbs bt _ (Bind f) -> vbeta loc bt f vs
|
|
|
|
|
VApp pre vs1 -> delta' pre (vs1++vs)
|
|
|
|
|
where
|
|
|
|
|
delta' Trace (v1:v2:vs) = let vr = vapply loc v2 vs
|
|
|
|
|
in vtrace loc v1 vr
|
|
|
|
|
delta' pre vs = err msg vfv $ mapM (delta pre) (varyList vs)
|
|
|
|
|
--msg = const (VApp pre (vs1++vs))
|
|
|
|
|
msg = bug . (("Applying Predef."++showIdent (predefName pre)++": ")++)
|
|
|
|
|
VS (VV t pvs fs) s -> VS (VV t pvs [vapply loc f vs|f<-fs]) s
|
|
|
|
|
VFV fs -> vfv [vapply loc f vs|f<-fs]
|
|
|
|
|
VCApp f vs0 -> VCApp f (vs0++vs)
|
|
|
|
|
VMeta i env vs0 -> VMeta i env (vs0++vs)
|
|
|
|
|
VGen i vs0 -> VGen i (vs0++vs)
|
|
|
|
|
v -> bug $ "vapply "++show v++" "++show vs
|
|
|
|
|
|
|
|
|
|
vbeta loc bt f (v:vs) =
|
|
|
|
|
case (bt,v) of
|
|
|
|
|
(Implicit,VImplArg v) -> ap v
|
|
|
|
|
(Explicit, v) -> ap v
|
|
|
|
|
where
|
|
|
|
|
ap (VFV avs) = vfv [vapply loc (f v) vs|v<-avs]
|
|
|
|
|
ap v = vapply loc (f v) vs
|
|
|
|
|
|
|
|
|
|
vary (VFV vs) = vs
|
|
|
|
|
vary v = [v]
|
|
|
|
|
varyList = mapM vary
|
|
|
|
|
|
|
|
|
|
{-
|
|
|
|
|
beta env b x t (v:vs) =
|
|
|
|
|
case (b,v) of
|
|
|
|
|
(Implicit,VImplArg v) -> apply' (ext (x,v) env) t vs
|
|
|
|
|
(Explicit, v) -> apply' (ext (x,v) env) t vs
|
|
|
|
|
-}
|
|
|
|
|
|
|
|
|
|
vtrace loc arg res = trace (render (hang (pv arg) 4 ("->"<+>pv res))) res
|
|
|
|
|
where
|
|
|
|
|
pv v = case v of
|
|
|
|
|
VRec (f:as) -> hang (pf f) 4 (fsep (map pa as))
|
|
|
|
|
_ -> ppV v
|
|
|
|
|
pf (_,VString n) = pp n
|
|
|
|
|
pf (_,v) = ppV v
|
|
|
|
|
pa (_,v) = ppV v
|
|
|
|
|
ppV v = ppTerm Unqualified 10 (value2term' True loc [] v)
|
|
|
|
|
-- Old value2term error message:
|
|
|
|
|
-- Left i -> "variable #" <> pp i <+> "is out of scope"
|
|
|
|
|
|
|
|
|
|
-- | Convert a value back to a term
|
|
|
|
|
value2term :: GLocation -> [Ident] -> Value -> Term
|
|
|
|
|
value2term = value2term' False
|
|
|
|
|
|
|
|
|
|
value2term' :: Bool -> p -> [Ident] -> Value -> Term
|
|
|
|
|
value2term' stop loc xs v0 =
|
|
|
|
|
case v0 of
|
|
|
|
|
VApp pre vs -> applyMany (Q (cPredef,predefName pre)) vs
|
|
|
|
|
VCApp f vs -> applyMany (QC f) vs
|
|
|
|
|
VGen j vs -> applyMany (var j) vs
|
|
|
|
|
VMeta j env vs -> applyMany (Meta j) vs
|
|
|
|
|
VProd bt v x f -> Prod bt x (v2t v) (v2t' x f)
|
|
|
|
|
VAbs bt x f -> Abs bt x (v2t' x f)
|
|
|
|
|
VInt n -> EInt n
|
|
|
|
|
VFloat f -> EFloat f
|
|
|
|
|
VString s -> if null s then Empty else K s
|
|
|
|
|
VSort s -> Sort s
|
|
|
|
|
VImplArg v -> ImplArg (v2t v)
|
|
|
|
|
VTblType p res -> Table (v2t p) (v2t res)
|
|
|
|
|
VRecType rs -> RecType [(l, v2t v) | (l,v) <- rs]
|
|
|
|
|
VRec as -> R [(l, (Nothing, v2t v)) | (l,v) <- as]
|
|
|
|
|
VV t _ vs -> V t (map v2t vs)
|
|
|
|
|
VT wild v cs -> T ((if wild then TWild else TTyped) (v2t v)) (map nfcase cs)
|
|
|
|
|
VFV vs -> FV (map v2t vs)
|
|
|
|
|
VC v1 v2 -> C (v2t v1) (v2t v2)
|
|
|
|
|
VS v1 v2 -> S (v2t v1) (v2t v2)
|
|
|
|
|
VP v l -> P (v2t v) l
|
|
|
|
|
VPatt p -> EPatt p
|
|
|
|
|
VPattType v -> EPattType $ v2t v
|
|
|
|
|
VAlts v vvs -> Alts (v2t v) [(v2t x, v2t y) | (x,y) <- vvs]
|
|
|
|
|
VStrs vs -> Strs (map v2t vs)
|
|
|
|
|
-- VGlue v1 v2 -> Glue (v2t v1) (v2t v2)
|
|
|
|
|
-- VExtR v1 v2 -> ExtR (v2t v1) (v2t v2)
|
|
|
|
|
VError err -> Error err
|
|
|
|
|
where
|
|
|
|
|
applyMany f vs = foldl App f (map v2t vs)
|
|
|
|
|
v2t = v2txs xs
|
|
|
|
|
v2txs = value2term' stop loc
|
|
|
|
|
v2t' x f = v2txs (x:xs) (bind f (gen xs))
|
|
|
|
|
|
|
|
|
|
var j
|
|
|
|
|
| j<length xs = Vr (reverse xs !! j)
|
|
|
|
|
| otherwise = error ("variable #"++show j++" is out of scope")
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
pushs xs e = foldr push e xs
|
|
|
|
|
push x (env,xs) = ((x,gen xs):env,x:xs)
|
|
|
|
|
gen xs = VGen (length xs) []
|
|
|
|
|
|
|
|
|
|
nfcase (p,f) = (,) p (v2txs xs' (bind f env'))
|
|
|
|
|
where (env',xs') = pushs (pattVars p) ([],xs)
|
|
|
|
|
|
|
|
|
|
bind (Bind f) x = if stop
|
|
|
|
|
then VSort (identS "...") -- hmm
|
|
|
|
|
else f x
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
linPattVars p =
|
|
|
|
|
if null dups
|
|
|
|
|
then return pvs
|
|
|
|
|
else fail.render $ hang "Pattern is not linear. All variable names on the left-hand side must be distinct." 4 (ppPatt Unqualified 0 p)
|
|
|
|
|
where
|
|
|
|
|
allpvs = allPattVars p
|
|
|
|
|
pvs = nub allpvs
|
|
|
|
|
dups = allpvs \\ pvs
|
|
|
|
|
|
|
|
|
|
pattVars = nub . allPattVars
|
|
|
|
|
allPattVars p =
|
|
|
|
|
case p of
|
|
|
|
|
PV i -> [i]
|
|
|
|
|
PAs i p -> i:allPattVars p
|
|
|
|
|
_ -> collectPattOp allPattVars p
|
|
|
|
|
|
|
|
|
|
---
|
|
|
|
|
ix loc fn xs i =
|
|
|
|
|
if i<n
|
|
|
|
|
then xs !! i
|
|
|
|
|
else bugloc loc $ "(!!): index too large in "++fn++", "++show i++"<"++show n
|
|
|
|
|
where n = length xs
|
|
|
|
|
|
|
|
|
|
infixl 1 #,<# --,@@
|
|
|
|
|
|
|
|
|
|
f # x = fmap f x
|
|
|
|
|
mf <# mx = ap mf mx
|
|
|
|
|
--m1 @@ m2 = (m1 =<<) . m2
|
|
|
|
|
|
|
|
|
|
both f (x,y) = (,) # f x <# f y
|
|
|
|
|
|
|
|
|
|
bugloc loc s = ppbug $ ppL loc s
|
|
|
|
|
|
|
|
|
|
bug msg = ppbug msg
|
|
|
|
|
ppbug doc = error $ render $ hang "Internal error in Compute.Concrete:" 4 doc
|
|
|
|
|
zonk tnk vs = EvalM $ \k mt r -> do
|
|
|
|
|
s <- readSTRef tnk
|
|
|
|
|
case s of
|
|
|
|
|
Evaluated v -> case apply v vs of
|
|
|
|
|
EvalM f -> f (k . Left) mt r
|
|
|
|
|
Unbound i -> k (Right i) mt r
|
|
|
|
|
|
krangelov