mirror of
https://github.com/GrammaticalFramework/gf-core.git
synced 2026-04-23 11:42:49 -06:00
Rename GF.Compile.Compute.ConcreteNew to GF.Compile.Compute.Concrete
This commit is contained in:
2
gf.cabal
2
gf.cabal
@@ -178,7 +178,7 @@ library
|
|||||||
GF.Command.TreeOperations
|
GF.Command.TreeOperations
|
||||||
GF.Compile.CFGtoPGF
|
GF.Compile.CFGtoPGF
|
||||||
GF.Compile.CheckGrammar
|
GF.Compile.CheckGrammar
|
||||||
GF.Compile.Compute.ConcreteNew
|
GF.Compile.Compute.Concrete
|
||||||
GF.Compile.Compute.Predef
|
GF.Compile.Compute.Predef
|
||||||
GF.Compile.Compute.Value
|
GF.Compile.Compute.Value
|
||||||
GF.Compile.ExampleBased
|
GF.Compile.ExampleBased
|
||||||
|
|||||||
@@ -18,7 +18,7 @@ import GF.Grammar.Parser (runP, pExp)
|
|||||||
import GF.Grammar.ShowTerm
|
import GF.Grammar.ShowTerm
|
||||||
import GF.Grammar.Lookup (allOpers,allOpersTo)
|
import GF.Grammar.Lookup (allOpers,allOpersTo)
|
||||||
import GF.Compile.Rename(renameSourceTerm)
|
import GF.Compile.Rename(renameSourceTerm)
|
||||||
import qualified GF.Compile.Compute.ConcreteNew as CN(normalForm,resourceValues)
|
import GF.Compile.Compute.Concrete(normalForm,resourceValues)
|
||||||
import GF.Compile.TypeCheck.RConcrete as TC(inferLType,ppType)
|
import GF.Compile.TypeCheck.RConcrete as TC(inferLType,ppType)
|
||||||
import GF.Infra.Dependencies(depGraph)
|
import GF.Infra.Dependencies(depGraph)
|
||||||
import GF.Infra.CheckM(runCheck)
|
import GF.Infra.CheckM(runCheck)
|
||||||
@@ -259,7 +259,7 @@ checkComputeTerm os sgr t =
|
|||||||
((t,_),_) <- runCheck $ do t <- renameSourceTerm sgr mo t
|
((t,_),_) <- runCheck $ do t <- renameSourceTerm sgr mo t
|
||||||
inferLType sgr [] t
|
inferLType sgr [] t
|
||||||
let opts = modifyFlags (\fs->fs{optTrace=isOpt "trace" os})
|
let opts = modifyFlags (\fs->fs{optTrace=isOpt "trace" os})
|
||||||
t1 = CN.normalForm (CN.resourceValues opts sgr) (L NoLoc identW) t
|
t1 = normalForm (resourceValues opts sgr) (L NoLoc identW) t
|
||||||
t2 = evalStr t1
|
t2 = evalStr t1
|
||||||
checkPredefError t2
|
checkPredefError t2
|
||||||
where
|
where
|
||||||
|
|||||||
@@ -5,7 +5,7 @@
|
|||||||
-- Stability : (stable)
|
-- Stability : (stable)
|
||||||
-- Portability : (portable)
|
-- Portability : (portable)
|
||||||
--
|
--
|
||||||
-- > CVS $Date: 2005/11/11 23:24:33 $
|
-- > CVS $Date: 2005/11/11 23:24:33 $
|
||||||
-- > CVS $Author: aarne $
|
-- > CVS $Author: aarne $
|
||||||
-- > CVS $Revision: 1.31 $
|
-- > CVS $Revision: 1.31 $
|
||||||
--
|
--
|
||||||
@@ -29,7 +29,7 @@ import GF.Infra.Option
|
|||||||
import GF.Compile.TypeCheck.Abstract
|
import GF.Compile.TypeCheck.Abstract
|
||||||
import GF.Compile.TypeCheck.RConcrete
|
import GF.Compile.TypeCheck.RConcrete
|
||||||
import qualified GF.Compile.TypeCheck.ConcreteNew as CN
|
import qualified GF.Compile.TypeCheck.ConcreteNew as CN
|
||||||
import qualified GF.Compile.Compute.ConcreteNew as CN
|
import qualified GF.Compile.Compute.Concrete as CN
|
||||||
|
|
||||||
import GF.Grammar
|
import GF.Grammar
|
||||||
import GF.Grammar.Lexer
|
import GF.Grammar.Lexer
|
||||||
@@ -74,9 +74,9 @@ checkRestrictedInheritance cwd sgr (name,mo) = checkInModule cwd mo NoLoc empty
|
|||||||
let (incl,excl) = partition (isInherited mi) (Map.keys (jments m))
|
let (incl,excl) = partition (isInherited mi) (Map.keys (jments m))
|
||||||
let incld c = Set.member c (Set.fromList incl)
|
let incld c = Set.member c (Set.fromList incl)
|
||||||
let illegal c = Set.member c (Set.fromList excl)
|
let illegal c = Set.member c (Set.fromList excl)
|
||||||
let illegals = [(f,is) |
|
let illegals = [(f,is) |
|
||||||
(f,cs) <- allDeps, incld f, let is = filter illegal cs, not (null is)]
|
(f,cs) <- allDeps, incld f, let is = filter illegal cs, not (null is)]
|
||||||
case illegals of
|
case illegals of
|
||||||
[] -> return ()
|
[] -> return ()
|
||||||
cs -> checkWarn ("In inherited module" <+> i <> ", dependence of excluded constants:" $$
|
cs -> checkWarn ("In inherited module" <+> i <> ", dependence of excluded constants:" $$
|
||||||
nest 2 (vcat [f <+> "on" <+> fsep is | (f,is) <- cs]))
|
nest 2 (vcat [f <+> "on" <+> fsep is | (f,is) <- cs]))
|
||||||
@@ -92,12 +92,12 @@ checkCompleteGrammar opts cwd gr (am,abs) (cm,cnc) = checkInModule cwd cnc NoLoc
|
|||||||
|
|
||||||
-- check that all abstract constants are in concrete; build default lin and lincats
|
-- check that all abstract constants are in concrete; build default lin and lincats
|
||||||
jsc <- foldM checkAbs jsc (Map.toList jsa)
|
jsc <- foldM checkAbs jsc (Map.toList jsa)
|
||||||
|
|
||||||
return (cm,cnc{jments=jsc})
|
return (cm,cnc{jments=jsc})
|
||||||
where
|
where
|
||||||
checkAbs js i@(c,info) =
|
checkAbs js i@(c,info) =
|
||||||
case info of
|
case info of
|
||||||
AbsFun (Just (L loc ty)) _ _ _
|
AbsFun (Just (L loc ty)) _ _ _
|
||||||
-> do let mb_def = do
|
-> do let mb_def = do
|
||||||
let (cxt,(_,i),_) = typeForm ty
|
let (cxt,(_,i),_) = typeForm ty
|
||||||
info <- lookupIdent i js
|
info <- lookupIdent i js
|
||||||
@@ -136,11 +136,11 @@ checkCompleteGrammar opts cwd gr (am,abs) (cm,cnc) = checkInModule cwd cnc NoLoc
|
|||||||
checkWarn ("no linearization type for" <+> c <> ", inserting default {s : Str}")
|
checkWarn ("no linearization type for" <+> c <> ", inserting default {s : Str}")
|
||||||
return $ Map.insert c (CncCat (Just (L NoLoc defLinType)) Nothing Nothing Nothing Nothing) js
|
return $ Map.insert c (CncCat (Just (L NoLoc defLinType)) Nothing Nothing Nothing Nothing) js
|
||||||
_ -> return js
|
_ -> return js
|
||||||
|
|
||||||
checkCnc js (c,info) =
|
checkCnc js (c,info) =
|
||||||
case info of
|
case info of
|
||||||
CncFun _ d mn mf -> case lookupOrigInfo gr (am,c) of
|
CncFun _ d mn mf -> case lookupOrigInfo gr (am,c) of
|
||||||
Ok (_,AbsFun (Just (L _ ty)) _ _ _) ->
|
Ok (_,AbsFun (Just (L _ ty)) _ _ _) ->
|
||||||
do (cont,val) <- linTypeOfType gr cm ty
|
do (cont,val) <- linTypeOfType gr cm ty
|
||||||
let linty = (snd (valCat ty),cont,val)
|
let linty = (snd (valCat ty),cont,val)
|
||||||
return $ Map.insert c (CncFun (Just linty) d mn mf) js
|
return $ Map.insert c (CncFun (Just linty) d mn mf) js
|
||||||
@@ -159,14 +159,14 @@ checkCompleteGrammar opts cwd gr (am,abs) (cm,cnc) = checkInModule cwd cnc NoLoc
|
|||||||
_ -> return $ Map.insert c info js
|
_ -> return $ Map.insert c info js
|
||||||
|
|
||||||
|
|
||||||
-- | General Principle: only Just-values are checked.
|
-- | General Principle: only Just-values are checked.
|
||||||
-- A May-value has always been checked in its origin module.
|
-- A May-value has always been checked in its origin module.
|
||||||
checkInfo :: Options -> FilePath -> SourceGrammar -> SourceModule -> Ident -> Info -> Check Info
|
checkInfo :: Options -> FilePath -> SourceGrammar -> SourceModule -> Ident -> Info -> Check Info
|
||||||
checkInfo opts cwd sgr (m,mo) c info = checkInModule cwd mo NoLoc empty $ do
|
checkInfo opts cwd sgr (m,mo) c info = checkInModule cwd mo NoLoc empty $ do
|
||||||
checkReservedId c
|
checkReservedId c
|
||||||
case info of
|
case info of
|
||||||
AbsCat (Just (L loc cont)) ->
|
AbsCat (Just (L loc cont)) ->
|
||||||
mkCheck loc "the category" $
|
mkCheck loc "the category" $
|
||||||
checkContext gr cont
|
checkContext gr cont
|
||||||
|
|
||||||
AbsFun (Just (L loc typ0)) ma md moper -> do
|
AbsFun (Just (L loc typ0)) ma md moper -> do
|
||||||
@@ -181,7 +181,7 @@ checkInfo opts cwd sgr (m,mo) c info = checkInModule cwd mo NoLoc empty $ do
|
|||||||
|
|
||||||
CncCat mty mdef mref mpr mpmcfg -> do
|
CncCat mty mdef mref mpr mpmcfg -> do
|
||||||
mty <- case mty of
|
mty <- case mty of
|
||||||
Just (L loc typ) -> chIn loc "linearization type of" $
|
Just (L loc typ) -> chIn loc "linearization type of" $
|
||||||
(if False --flag optNewComp opts
|
(if False --flag optNewComp opts
|
||||||
then do (typ,_) <- CN.checkLType (CN.resourceValues opts gr) typ typeType
|
then do (typ,_) <- CN.checkLType (CN.resourceValues opts gr) typ typeType
|
||||||
typ <- computeLType gr [] typ
|
typ <- computeLType gr [] typ
|
||||||
@@ -191,19 +191,19 @@ checkInfo opts cwd sgr (m,mo) c info = checkInModule cwd mo NoLoc empty $ do
|
|||||||
return (Just (L loc typ)))
|
return (Just (L loc typ)))
|
||||||
Nothing -> return Nothing
|
Nothing -> return Nothing
|
||||||
mdef <- case (mty,mdef) of
|
mdef <- case (mty,mdef) of
|
||||||
(Just (L _ typ),Just (L loc def)) ->
|
(Just (L _ typ),Just (L loc def)) ->
|
||||||
chIn loc "default linearization of" $ do
|
chIn loc "default linearization of" $ do
|
||||||
(def,_) <- checkLType gr [] def (mkFunType [typeStr] typ)
|
(def,_) <- checkLType gr [] def (mkFunType [typeStr] typ)
|
||||||
return (Just (L loc def))
|
return (Just (L loc def))
|
||||||
_ -> return Nothing
|
_ -> return Nothing
|
||||||
mref <- case (mty,mref) of
|
mref <- case (mty,mref) of
|
||||||
(Just (L _ typ),Just (L loc ref)) ->
|
(Just (L _ typ),Just (L loc ref)) ->
|
||||||
chIn loc "reference linearization of" $ do
|
chIn loc "reference linearization of" $ do
|
||||||
(ref,_) <- checkLType gr [] ref (mkFunType [typ] typeStr)
|
(ref,_) <- checkLType gr [] ref (mkFunType [typ] typeStr)
|
||||||
return (Just (L loc ref))
|
return (Just (L loc ref))
|
||||||
_ -> return Nothing
|
_ -> return Nothing
|
||||||
mpr <- case mpr of
|
mpr <- case mpr of
|
||||||
(Just (L loc t)) ->
|
(Just (L loc t)) ->
|
||||||
chIn loc "print name of" $ do
|
chIn loc "print name of" $ do
|
||||||
(t,_) <- checkLType gr [] t typeStr
|
(t,_) <- checkLType gr [] t typeStr
|
||||||
return (Just (L loc t))
|
return (Just (L loc t))
|
||||||
@@ -212,13 +212,13 @@ checkInfo opts cwd sgr (m,mo) c info = checkInModule cwd mo NoLoc empty $ do
|
|||||||
|
|
||||||
CncFun mty mt mpr mpmcfg -> do
|
CncFun mty mt mpr mpmcfg -> do
|
||||||
mt <- case (mty,mt) of
|
mt <- case (mty,mt) of
|
||||||
(Just (cat,cont,val),Just (L loc trm)) ->
|
(Just (cat,cont,val),Just (L loc trm)) ->
|
||||||
chIn loc "linearization of" $ do
|
chIn loc "linearization of" $ do
|
||||||
(trm,_) <- checkLType gr [] trm (mkFunType (map (\(_,_,ty) -> ty) cont) val) -- erases arg vars
|
(trm,_) <- checkLType gr [] trm (mkFunType (map (\(_,_,ty) -> ty) cont) val) -- erases arg vars
|
||||||
return (Just (L loc trm))
|
return (Just (L loc trm))
|
||||||
_ -> return mt
|
_ -> return mt
|
||||||
mpr <- case mpr of
|
mpr <- case mpr of
|
||||||
(Just (L loc t)) ->
|
(Just (L loc t)) ->
|
||||||
chIn loc "print name of" $ do
|
chIn loc "print name of" $ do
|
||||||
(t,_) <- checkLType gr [] t typeStr
|
(t,_) <- checkLType gr [] t typeStr
|
||||||
return (Just (L loc t))
|
return (Just (L loc t))
|
||||||
@@ -251,16 +251,16 @@ checkInfo opts cwd sgr (m,mo) c info = checkInModule cwd mo NoLoc empty $ do
|
|||||||
ResOverload os tysts -> chIn NoLoc "overloading" $ do
|
ResOverload os tysts -> chIn NoLoc "overloading" $ do
|
||||||
tysts' <- mapM (uncurry $ flip (\(L loc1 t) (L loc2 ty) -> checkLType gr [] t ty >>= \(t,ty) -> return (L loc1 t, L loc2 ty))) tysts -- return explicit ones
|
tysts' <- mapM (uncurry $ flip (\(L loc1 t) (L loc2 ty) -> checkLType gr [] t ty >>= \(t,ty) -> return (L loc1 t, L loc2 ty))) tysts -- return explicit ones
|
||||||
tysts0 <- lookupOverload gr (m,c) -- check against inherited ones too
|
tysts0 <- lookupOverload gr (m,c) -- check against inherited ones too
|
||||||
tysts1 <- mapM (uncurry $ flip (checkLType gr []))
|
tysts1 <- mapM (uncurry $ flip (checkLType gr []))
|
||||||
[(mkFunType args val,tr) | (args,(val,tr)) <- tysts0]
|
[(mkFunType args val,tr) | (args,(val,tr)) <- tysts0]
|
||||||
--- this can only be a partial guarantee, since matching
|
--- this can only be a partial guarantee, since matching
|
||||||
--- with value type is only possible if expected type is given
|
--- with value type is only possible if expected type is given
|
||||||
checkUniq $
|
checkUniq $
|
||||||
sort [let (xs,t) = typeFormCnc x in t : map (\(b,x,t) -> t) xs | (_,x) <- tysts1]
|
sort [let (xs,t) = typeFormCnc x in t : map (\(b,x,t) -> t) xs | (_,x) <- tysts1]
|
||||||
return (ResOverload os [(y,x) | (x,y) <- tysts'])
|
return (ResOverload os [(y,x) | (x,y) <- tysts'])
|
||||||
|
|
||||||
ResParam (Just (L loc pcs)) _ -> do
|
ResParam (Just (L loc pcs)) _ -> do
|
||||||
ts <- chIn loc "parameter type" $
|
ts <- chIn loc "parameter type" $
|
||||||
liftM concat $ mapM mkPar pcs
|
liftM concat $ mapM mkPar pcs
|
||||||
return (ResParam (Just (L loc pcs)) (Just ts))
|
return (ResParam (Just (L loc pcs)) (Just ts))
|
||||||
|
|
||||||
@@ -274,9 +274,9 @@ checkInfo opts cwd sgr (m,mo) c info = checkInModule cwd mo NoLoc empty $ do
|
|||||||
return $ map (mkApp (QC (m,f))) vs
|
return $ map (mkApp (QC (m,f))) vs
|
||||||
|
|
||||||
checkUniq xss = case xss of
|
checkUniq xss = case xss of
|
||||||
x:y:xs
|
x:y:xs
|
||||||
| x == y -> checkError $ "ambiguous for type" <+>
|
| x == y -> checkError $ "ambiguous for type" <+>
|
||||||
ppType (mkFunType (tail x) (head x))
|
ppType (mkFunType (tail x) (head x))
|
||||||
| otherwise -> checkUniq $ y:xs
|
| otherwise -> checkUniq $ y:xs
|
||||||
_ -> return ()
|
_ -> return ()
|
||||||
|
|
||||||
@@ -294,7 +294,7 @@ checkInfo opts cwd sgr (m,mo) c info = checkInModule cwd mo NoLoc empty $ do
|
|||||||
t' <- compAbsTyp ((x,Vr x):g) t
|
t' <- compAbsTyp ((x,Vr x):g) t
|
||||||
return $ Prod b x a' t'
|
return $ Prod b x a' t'
|
||||||
Abs _ _ _ -> return t
|
Abs _ _ _ -> return t
|
||||||
_ -> composOp (compAbsTyp g) t
|
_ -> composOp (compAbsTyp g) t
|
||||||
|
|
||||||
|
|
||||||
-- | for grammars obtained otherwise than by parsing ---- update!!
|
-- | for grammars obtained otherwise than by parsing ---- update!!
|
||||||
|
|||||||
@@ -1,3 +1,588 @@
|
|||||||
module GF.Compile.Compute.Concrete{-(module M)-} where
|
-- | Functions for computing the values of terms in the concrete syntax, in
|
||||||
--import GF.Compile.Compute.ConcreteLazy as M -- New
|
-- | preparation for PMCFG generation.
|
||||||
--import GF.Compile.Compute.ConcreteStrict as M -- Old, inefficient
|
module GF.Compile.Compute.Concrete
|
||||||
|
(GlobalEnv, GLocation, resourceValues, geLoc, geGrammar,
|
||||||
|
normalForm,
|
||||||
|
Value(..), Bind(..), Env, value2term, eval, vapply
|
||||||
|
) where
|
||||||
|
import Prelude hiding ((<>)) -- GHC 8.4.1 clash with Text.PrettyPrint
|
||||||
|
|
||||||
|
import GF.Grammar hiding (Env, VGen, VApp, VRecType)
|
||||||
|
import GF.Grammar.Lookup(lookupResDefLoc,allParamValues)
|
||||||
|
import GF.Grammar.Predef(cPredef,cErrorType,cTok,cStr,cTrace,cPBool)
|
||||||
|
import GF.Grammar.PatternMatch(matchPattern,measurePatt)
|
||||||
|
import GF.Grammar.Lockfield(isLockLabel,lockRecType) --unlockRecord,lockLabel
|
||||||
|
import GF.Compile.Compute.Value hiding (Error)
|
||||||
|
import GF.Compile.Compute.Predef(predef,predefName,delta)
|
||||||
|
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 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)
|
||||||
|
|
||||||
|
nfx env@(GE _ _ _ loc) t = do
|
||||||
|
v <- eval env [] t
|
||||||
|
case value2term loc [] v of
|
||||||
|
Left i -> fail ("variable #"++show i++" is out of scope")
|
||||||
|
Right t -> return t
|
||||||
|
|
||||||
|
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 env = apply' env
|
||||||
|
|
||||||
|
--------------------------------------------------------------------------------
|
||||||
|
|
||||||
|
-- * 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}
|
||||||
|
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
|
||||||
|
|
||||||
|
-- | 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 = case value2term loc (local env) v of
|
||||||
|
Left i -> Error ('#':show i)
|
||||||
|
Right t -> t
|
||||||
|
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"
|
||||||
|
]
|
||||||
|
|
||||||
|
|
||||||
|
-- | 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
|
||||||
|
|
||||||
|
_ -> fail ("cannot get Str from value " ++ show t)
|
||||||
|
|
||||||
|
vfv vs = case nub vs of
|
||||||
|
[v] -> v
|
||||||
|
vs -> VFV vs
|
||||||
|
|
||||||
|
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
|
||||||
|
|
||||||
|
match loc cs v =
|
||||||
|
case value2term loc [] v of
|
||||||
|
Left i -> bad ("variable #"++show i++" is out of scope")
|
||||||
|
Right t -> err bad return (matchPattern cs t)
|
||||||
|
where
|
||||||
|
bad = fail . ("In pattern matching: "++)
|
||||||
|
|
||||||
|
valueMatch :: CompleteEnv -> (Bind Env,Substitution) -> Err Value
|
||||||
|
valueMatch env (Bind f,env') = f # mapPairsM (value0 env) env'
|
||||||
|
|
||||||
|
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
|
||||||
|
|
||||||
|
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 =
|
||||||
|
case value2term (gloc env) [] vty of
|
||||||
|
Left i -> fail ("variable #"++show i++" is out of scope")
|
||||||
|
Right pty -> convert' cs' =<< paramValues'' env pty
|
||||||
|
|
||||||
|
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
|
||||||
|
|
||||||
|
|
||||||
|
paramValues env ty = snd # paramValues' env ty
|
||||||
|
|
||||||
|
paramValues' env ty = paramValues'' env =<< nfx (global env) ty
|
||||||
|
|
||||||
|
paramValues'' env pty = do ats <- allParamValues (srcgr env) pty
|
||||||
|
pvs <- mapM (eval (global env) []) ats
|
||||||
|
return ((pty,ats),pvs)
|
||||||
|
|
||||||
|
push' p bs xs = if length bs/=length xs
|
||||||
|
then bug $ "push "++show (p,bs,xs)
|
||||||
|
else push bs xs
|
||||||
|
|
||||||
|
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
|
||||||
|
|
||||||
|
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 = case value2term' True loc [] v of
|
||||||
|
Left i -> "variable #" <> pp i <+> "is out of scope"
|
||||||
|
Right t -> ppTerm Unqualified 10 t
|
||||||
|
|
||||||
|
-- | Convert a value back to a term
|
||||||
|
value2term :: GLocation -> [Ident] -> Value -> Either Int Term
|
||||||
|
value2term = value2term' False
|
||||||
|
value2term' stop loc xs v0 =
|
||||||
|
case v0 of
|
||||||
|
VApp pre vs -> liftM (foldl App (Q (cPredef,predefName pre))) (mapM v2t vs)
|
||||||
|
VCApp f vs -> liftM (foldl App (QC f)) (mapM v2t vs)
|
||||||
|
VGen j vs -> liftM2 (foldl App) (var j) (mapM v2t vs)
|
||||||
|
VMeta j env vs -> liftM (foldl App (Meta j)) (mapM v2t vs)
|
||||||
|
VProd bt v x f -> liftM2 (Prod bt x) (v2t v) (v2t' x f)
|
||||||
|
VAbs bt x f -> liftM (Abs bt x) (v2t' x f)
|
||||||
|
VInt n -> return (EInt n)
|
||||||
|
VFloat f -> return (EFloat f)
|
||||||
|
VString s -> return (if null s then Empty else K s)
|
||||||
|
VSort s -> return (Sort s)
|
||||||
|
VImplArg v -> liftM ImplArg (v2t v)
|
||||||
|
VTblType p res -> liftM2 Table (v2t p) (v2t res)
|
||||||
|
VRecType rs -> liftM RecType (mapM (\(l,v) -> fmap ((,) l) (v2t v)) rs)
|
||||||
|
VRec as -> liftM R (mapM (\(l,v) -> v2t v >>= \t -> return (l,(Nothing,t))) as)
|
||||||
|
VV t _ vs -> liftM (V t) (mapM v2t vs)
|
||||||
|
VT wild v cs -> v2t v >>= \t -> liftM (T ((if wild then TWild else TTyped) t)) (mapM nfcase cs)
|
||||||
|
VFV vs -> liftM FV (mapM v2t vs)
|
||||||
|
VC v1 v2 -> liftM2 C (v2t v1) (v2t v2)
|
||||||
|
VS v1 v2 -> liftM2 S (v2t v1) (v2t v2)
|
||||||
|
VP v l -> v2t v >>= \t -> return (P t l)
|
||||||
|
VPatt p -> return (EPatt p)
|
||||||
|
VPattType v -> v2t v >>= return . EPattType
|
||||||
|
VAlts v vvs -> liftM2 Alts (v2t v) (mapM (\(x,y) -> liftM2 (,) (v2t x) (v2t y)) vvs)
|
||||||
|
VStrs vs -> liftM Strs (mapM v2t vs)
|
||||||
|
-- VGlue v1 v2 -> Glue (v2t v1) (v2t v2)
|
||||||
|
-- VExtR v1 v2 -> ExtR (v2t v1) (v2t v2)
|
||||||
|
VError err -> return (Error err)
|
||||||
|
|
||||||
|
where
|
||||||
|
v2t = v2txs xs
|
||||||
|
v2txs = value2term' stop loc
|
||||||
|
v2t' x f = v2txs (x:xs) (bind f (gen xs))
|
||||||
|
|
||||||
|
var j
|
||||||
|
| j<length xs = Right (Vr (reverse xs !! j))
|
||||||
|
| otherwise = Left j
|
||||||
|
|
||||||
|
|
||||||
|
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) = liftM ((,) 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
|
||||||
|
|||||||
@@ -1,588 +0,0 @@
|
|||||||
-- | Functions for computing the values of terms in the concrete syntax, in
|
|
||||||
-- | preparation for PMCFG generation.
|
|
||||||
module GF.Compile.Compute.ConcreteNew
|
|
||||||
(GlobalEnv, GLocation, resourceValues, geLoc, geGrammar,
|
|
||||||
normalForm,
|
|
||||||
Value(..), Bind(..), Env, value2term, eval, vapply
|
|
||||||
) where
|
|
||||||
import Prelude hiding ((<>)) -- GHC 8.4.1 clash with Text.PrettyPrint
|
|
||||||
|
|
||||||
import GF.Grammar hiding (Env, VGen, VApp, VRecType)
|
|
||||||
import GF.Grammar.Lookup(lookupResDefLoc,allParamValues)
|
|
||||||
import GF.Grammar.Predef(cPredef,cErrorType,cTok,cStr,cTrace,cPBool)
|
|
||||||
import GF.Grammar.PatternMatch(matchPattern,measurePatt)
|
|
||||||
import GF.Grammar.Lockfield(isLockLabel,lockRecType) --unlockRecord,lockLabel
|
|
||||||
import GF.Compile.Compute.Value hiding (Error)
|
|
||||||
import GF.Compile.Compute.Predef(predef,predefName,delta)
|
|
||||||
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 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)
|
|
||||||
|
|
||||||
nfx env@(GE _ _ _ loc) t = do
|
|
||||||
v <- eval env [] t
|
|
||||||
case value2term loc [] v of
|
|
||||||
Left i -> fail ("variable #"++show i++" is out of scope")
|
|
||||||
Right t -> return t
|
|
||||||
|
|
||||||
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 env = apply' env
|
|
||||||
|
|
||||||
--------------------------------------------------------------------------------
|
|
||||||
|
|
||||||
-- * 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}
|
|
||||||
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
|
|
||||||
|
|
||||||
-- | 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 = case value2term loc (local env) v of
|
|
||||||
Left i -> Error ('#':show i)
|
|
||||||
Right t -> t
|
|
||||||
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"
|
|
||||||
]
|
|
||||||
|
|
||||||
|
|
||||||
-- | 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
|
|
||||||
|
|
||||||
_ -> fail ("cannot get Str from value " ++ show t)
|
|
||||||
|
|
||||||
vfv vs = case nub vs of
|
|
||||||
[v] -> v
|
|
||||||
vs -> VFV vs
|
|
||||||
|
|
||||||
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
|
|
||||||
|
|
||||||
match loc cs v =
|
|
||||||
case value2term loc [] v of
|
|
||||||
Left i -> bad ("variable #"++show i++" is out of scope")
|
|
||||||
Right t -> err bad return (matchPattern cs t)
|
|
||||||
where
|
|
||||||
bad = fail . ("In pattern matching: "++)
|
|
||||||
|
|
||||||
valueMatch :: CompleteEnv -> (Bind Env,Substitution) -> Err Value
|
|
||||||
valueMatch env (Bind f,env') = f # mapPairsM (value0 env) env'
|
|
||||||
|
|
||||||
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
|
|
||||||
|
|
||||||
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 =
|
|
||||||
case value2term (gloc env) [] vty of
|
|
||||||
Left i -> fail ("variable #"++show i++" is out of scope")
|
|
||||||
Right pty -> convert' cs' =<< paramValues'' env pty
|
|
||||||
|
|
||||||
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
|
|
||||||
|
|
||||||
|
|
||||||
paramValues env ty = snd # paramValues' env ty
|
|
||||||
|
|
||||||
paramValues' env ty = paramValues'' env =<< nfx (global env) ty
|
|
||||||
|
|
||||||
paramValues'' env pty = do ats <- allParamValues (srcgr env) pty
|
|
||||||
pvs <- mapM (eval (global env) []) ats
|
|
||||||
return ((pty,ats),pvs)
|
|
||||||
|
|
||||||
push' p bs xs = if length bs/=length xs
|
|
||||||
then bug $ "push "++show (p,bs,xs)
|
|
||||||
else push bs xs
|
|
||||||
|
|
||||||
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
|
|
||||||
|
|
||||||
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 = case value2term' True loc [] v of
|
|
||||||
Left i -> "variable #" <> pp i <+> "is out of scope"
|
|
||||||
Right t -> ppTerm Unqualified 10 t
|
|
||||||
|
|
||||||
-- | Convert a value back to a term
|
|
||||||
value2term :: GLocation -> [Ident] -> Value -> Either Int Term
|
|
||||||
value2term = value2term' False
|
|
||||||
value2term' stop loc xs v0 =
|
|
||||||
case v0 of
|
|
||||||
VApp pre vs -> liftM (foldl App (Q (cPredef,predefName pre))) (mapM v2t vs)
|
|
||||||
VCApp f vs -> liftM (foldl App (QC f)) (mapM v2t vs)
|
|
||||||
VGen j vs -> liftM2 (foldl App) (var j) (mapM v2t vs)
|
|
||||||
VMeta j env vs -> liftM (foldl App (Meta j)) (mapM v2t vs)
|
|
||||||
VProd bt v x f -> liftM2 (Prod bt x) (v2t v) (v2t' x f)
|
|
||||||
VAbs bt x f -> liftM (Abs bt x) (v2t' x f)
|
|
||||||
VInt n -> return (EInt n)
|
|
||||||
VFloat f -> return (EFloat f)
|
|
||||||
VString s -> return (if null s then Empty else K s)
|
|
||||||
VSort s -> return (Sort s)
|
|
||||||
VImplArg v -> liftM ImplArg (v2t v)
|
|
||||||
VTblType p res -> liftM2 Table (v2t p) (v2t res)
|
|
||||||
VRecType rs -> liftM RecType (mapM (\(l,v) -> fmap ((,) l) (v2t v)) rs)
|
|
||||||
VRec as -> liftM R (mapM (\(l,v) -> v2t v >>= \t -> return (l,(Nothing,t))) as)
|
|
||||||
VV t _ vs -> liftM (V t) (mapM v2t vs)
|
|
||||||
VT wild v cs -> v2t v >>= \t -> liftM (T ((if wild then TWild else TTyped) t)) (mapM nfcase cs)
|
|
||||||
VFV vs -> liftM FV (mapM v2t vs)
|
|
||||||
VC v1 v2 -> liftM2 C (v2t v1) (v2t v2)
|
|
||||||
VS v1 v2 -> liftM2 S (v2t v1) (v2t v2)
|
|
||||||
VP v l -> v2t v >>= \t -> return (P t l)
|
|
||||||
VPatt p -> return (EPatt p)
|
|
||||||
VPattType v -> v2t v >>= return . EPattType
|
|
||||||
VAlts v vvs -> liftM2 Alts (v2t v) (mapM (\(x,y) -> liftM2 (,) (v2t x) (v2t y)) vvs)
|
|
||||||
VStrs vs -> liftM Strs (mapM v2t vs)
|
|
||||||
-- VGlue v1 v2 -> Glue (v2t v1) (v2t v2)
|
|
||||||
-- VExtR v1 v2 -> ExtR (v2t v1) (v2t v2)
|
|
||||||
VError err -> return (Error err)
|
|
||||||
|
|
||||||
where
|
|
||||||
v2t = v2txs xs
|
|
||||||
v2txs = value2term' stop loc
|
|
||||||
v2t' x f = v2txs (x:xs) (bind f (gen xs))
|
|
||||||
|
|
||||||
var j
|
|
||||||
| j<length xs = Right (Vr (reverse xs !! j))
|
|
||||||
| otherwise = Left j
|
|
||||||
|
|
||||||
|
|
||||||
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) = liftM ((,) 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.ConcreteNew:" 4 doc
|
|
||||||
@@ -12,8 +12,8 @@ data Value
|
|||||||
| VGen Int [Value] -- for lambda bound variables, possibly applied
|
| VGen Int [Value] -- for lambda bound variables, possibly applied
|
||||||
| VMeta MetaId Env [Value]
|
| VMeta MetaId Env [Value]
|
||||||
-- -- | VClosure Env Term -- used in Typecheck.ConcreteNew
|
-- -- | VClosure Env Term -- used in Typecheck.ConcreteNew
|
||||||
| VAbs BindType Ident Binding -- used in Compute.ConcreteNew
|
| VAbs BindType Ident Binding -- used in Compute.Concrete
|
||||||
| VProd BindType Value Ident Binding -- used in Compute.ConcreteNew
|
| VProd BindType Value Ident Binding -- used in Compute.Concrete
|
||||||
| VInt Int
|
| VInt Int
|
||||||
| VFloat Double
|
| VFloat Double
|
||||||
| VString String
|
| VString String
|
||||||
@@ -47,10 +47,10 @@ type Env = [(Ident,Value)]
|
|||||||
|
|
||||||
-- | Predefined functions
|
-- | Predefined functions
|
||||||
data Predefined = Drop | Take | Tk | Dp | EqStr | Occur | Occurs | ToUpper
|
data Predefined = Drop | Take | Tk | Dp | EqStr | Occur | Occurs | ToUpper
|
||||||
| ToLower | IsUpper | Length | Plus | EqInt | LessInt
|
| ToLower | IsUpper | Length | Plus | EqInt | LessInt
|
||||||
{- | Show | Read | ToStr | MapStr | EqVal -}
|
{- | Show | Read | ToStr | MapStr | EqVal -}
|
||||||
| Error | Trace
|
| Error | Trace
|
||||||
-- Canonical values below:
|
-- Canonical values below:
|
||||||
| PBool | PFalse | PTrue | Int | Float | Ints | NonExist
|
| PBool | PFalse | PTrue | Int | Float | Ints | NonExist
|
||||||
| BIND | SOFT_BIND | SOFT_SPACE | CAPIT | ALL_CAPIT
|
| BIND | SOFT_BIND | SOFT_SPACE | CAPIT | ALL_CAPIT
|
||||||
deriving (Show,Eq,Ord,Ix,Bounded,Enum)
|
deriving (Show,Eq,Ord,Ix,Bounded,Enum)
|
||||||
|
|||||||
@@ -25,7 +25,7 @@ import GF.Data.BacktrackM
|
|||||||
import GF.Data.Operations
|
import GF.Data.Operations
|
||||||
import GF.Infra.UseIO (ePutStr,ePutStrLn) -- IOE,
|
import GF.Infra.UseIO (ePutStr,ePutStrLn) -- IOE,
|
||||||
import GF.Data.Utilities (updateNthM) --updateNth
|
import GF.Data.Utilities (updateNthM) --updateNth
|
||||||
import GF.Compile.Compute.ConcreteNew(normalForm,resourceValues)
|
import GF.Compile.Compute.Concrete(normalForm,resourceValues)
|
||||||
import qualified Data.Map as Map
|
import qualified Data.Map as Map
|
||||||
import qualified Data.Set as Set
|
import qualified Data.Set as Set
|
||||||
import qualified Data.List as List
|
import qualified Data.List as List
|
||||||
@@ -82,7 +82,7 @@ addPMCFG opts gr cenv opath am cm seqs id (GF.Grammar.CncFun mty@(Just (cat,cont
|
|||||||
(goB b1 CNil [])
|
(goB b1 CNil [])
|
||||||
(pres,pargs)
|
(pres,pargs)
|
||||||
pmcfg = getPMCFG pmcfgEnv1
|
pmcfg = getPMCFG pmcfgEnv1
|
||||||
|
|
||||||
stats = let PMCFG prods funs = pmcfg
|
stats = let PMCFG prods funs = pmcfg
|
||||||
(s,e) = bounds funs
|
(s,e) = bounds funs
|
||||||
!prods_cnt = length prods
|
!prods_cnt = length prods
|
||||||
@@ -103,7 +103,7 @@ addPMCFG opts gr cenv opath am cm seqs id (GF.Grammar.CncFun mty@(Just (cat,cont
|
|||||||
newArgs = map getFIds newArgs'
|
newArgs = map getFIds newArgs'
|
||||||
in addFunction env0 newCat fun newArgs
|
in addFunction env0 newCat fun newArgs
|
||||||
|
|
||||||
addPMCFG opts gr cenv opath am cm seqs id (GF.Grammar.CncCat mty@(Just (L _ lincat))
|
addPMCFG opts gr cenv opath am cm seqs id (GF.Grammar.CncCat mty@(Just (L _ lincat))
|
||||||
mdef@(Just (L loc1 def))
|
mdef@(Just (L loc1 def))
|
||||||
mref@(Just (L loc2 ref))
|
mref@(Just (L loc2 ref))
|
||||||
mprn
|
mprn
|
||||||
@@ -162,7 +162,7 @@ pgfCncCat :: SourceGrammar -> Type -> Int -> CncCat
|
|||||||
pgfCncCat gr lincat index =
|
pgfCncCat gr lincat index =
|
||||||
let ((_,size),schema) = computeCatRange gr lincat
|
let ((_,size),schema) = computeCatRange gr lincat
|
||||||
in PGF.CncCat index (index+size-1)
|
in PGF.CncCat index (index+size-1)
|
||||||
(mkArray (map (renderStyle style{mode=OneLineMode} . ppPath)
|
(mkArray (map (renderStyle style{mode=OneLineMode} . ppPath)
|
||||||
(getStrPaths schema)))
|
(getStrPaths schema)))
|
||||||
where
|
where
|
||||||
getStrPaths :: Schema Identity s c -> [Path]
|
getStrPaths :: Schema Identity s c -> [Path]
|
||||||
@@ -243,7 +243,7 @@ choices nr path = do (args,_) <- get
|
|||||||
| (value,index) <- values])
|
| (value,index) <- values])
|
||||||
descend schema path rpath = bug $ "descend "++show (schema,path,rpath)
|
descend schema path rpath = bug $ "descend "++show (schema,path,rpath)
|
||||||
|
|
||||||
updateEnv path value gr c (args,seq) =
|
updateEnv path value gr c (args,seq) =
|
||||||
case updateNthM (restrictProtoFCat path value) nr args of
|
case updateNthM (restrictProtoFCat path value) nr args of
|
||||||
Just args -> c value (args,seq)
|
Just args -> c value (args,seq)
|
||||||
Nothing -> bug "conflict in updateEnv"
|
Nothing -> bug "conflict in updateEnv"
|
||||||
@@ -606,7 +606,7 @@ restrictProtoFCat path v (PFCat cat f schema) = do
|
|||||||
Just index -> return (CPar (m,[(v,index)]))
|
Just index -> return (CPar (m,[(v,index)]))
|
||||||
Nothing -> mzero
|
Nothing -> mzero
|
||||||
addConstraint CNil v (CStr _) = bug "restrictProtoFCat: string path"
|
addConstraint CNil v (CStr _) = bug "restrictProtoFCat: string path"
|
||||||
|
|
||||||
update k0 f [] = return []
|
update k0 f [] = return []
|
||||||
update k0 f (x@(k,Identity v):xs)
|
update k0 f (x@(k,Identity v):xs)
|
||||||
| k0 == k = do v <- f v
|
| k0 == k = do v <- f v
|
||||||
|
|||||||
@@ -19,7 +19,7 @@ import GF.Compile.Compute.Value(Predefined(..))
|
|||||||
import GF.Infra.Ident(ModuleName(..),Ident,prefixIdent,showIdent,isWildIdent)
|
import GF.Infra.Ident(ModuleName(..),Ident,prefixIdent,showIdent,isWildIdent)
|
||||||
import GF.Infra.Option(optionsPGF)
|
import GF.Infra.Option(optionsPGF)
|
||||||
import PGF.Internal(Literal(..))
|
import PGF.Internal(Literal(..))
|
||||||
import GF.Compile.Compute.ConcreteNew(normalForm,resourceValues)
|
import GF.Compile.Compute.Concrete(normalForm,resourceValues)
|
||||||
import GF.Grammar.Canonical as C
|
import GF.Grammar.Canonical as C
|
||||||
import Debug.Trace
|
import Debug.Trace
|
||||||
|
|
||||||
@@ -72,7 +72,7 @@ concrete2canonical gr cenv absname cnc modinfo =
|
|||||||
[lincat|(_,Left lincat)<-defs]
|
[lincat|(_,Left lincat)<-defs]
|
||||||
[lin|(_,Right lin)<-defs]
|
[lin|(_,Right lin)<-defs]
|
||||||
where
|
where
|
||||||
defs = concatMap (toCanonical gr absname cenv) .
|
defs = concatMap (toCanonical gr absname cenv) .
|
||||||
M.toList $
|
M.toList $
|
||||||
jments modinfo
|
jments modinfo
|
||||||
|
|
||||||
@@ -189,7 +189,7 @@ convert' gr vs = ppT
|
|||||||
_ -> VarValue (gQId cPredef n) -- hmm
|
_ -> VarValue (gQId cPredef n) -- hmm
|
||||||
where
|
where
|
||||||
p = PredefValue . PredefId
|
p = PredefValue . PredefId
|
||||||
|
|
||||||
ppP p =
|
ppP p =
|
||||||
case p of
|
case p of
|
||||||
PC c ps -> ParamPattern (Param (gId c) (map ppP ps))
|
PC c ps -> ParamPattern (Param (gId c) (map ppP ps))
|
||||||
|
|||||||
@@ -6,7 +6,7 @@
|
|||||||
-- Stability : (stable)
|
-- Stability : (stable)
|
||||||
-- Portability : (portable)
|
-- Portability : (portable)
|
||||||
--
|
--
|
||||||
-- > CVS $Date: 2005/09/16 13:56:13 $
|
-- > CVS $Date: 2005/09/16 13:56:13 $
|
||||||
-- > CVS $Author: aarne $
|
-- > CVS $Author: aarne $
|
||||||
-- > CVS $Revision: 1.18 $
|
-- > CVS $Revision: 1.18 $
|
||||||
--
|
--
|
||||||
@@ -21,7 +21,7 @@ import GF.Grammar.Printer
|
|||||||
import GF.Grammar.Macros
|
import GF.Grammar.Macros
|
||||||
import GF.Grammar.Lookup
|
import GF.Grammar.Lookup
|
||||||
import GF.Grammar.Predef
|
import GF.Grammar.Predef
|
||||||
import GF.Compile.Compute.ConcreteNew(GlobalEnv,normalForm,resourceValues)
|
import GF.Compile.Compute.Concrete(GlobalEnv,normalForm,resourceValues)
|
||||||
import GF.Data.Operations
|
import GF.Data.Operations
|
||||||
import GF.Infra.Option
|
import GF.Infra.Option
|
||||||
|
|
||||||
@@ -90,7 +90,7 @@ evalInfo opts resenv sgr m c info = do
|
|||||||
let ppr' = fmap (evalPrintname resenv c) ppr
|
let ppr' = fmap (evalPrintname resenv c) ppr
|
||||||
return $ CncFun mt pde' ppr' mpmcfg -- only cat in type actually needed
|
return $ CncFun mt pde' ppr' mpmcfg -- only cat in type actually needed
|
||||||
{-
|
{-
|
||||||
ResOper pty pde
|
ResOper pty pde
|
||||||
| not new && OptExpand `Set.member` optim -> do
|
| not new && OptExpand `Set.member` optim -> do
|
||||||
pde' <- case pde of
|
pde' <- case pde of
|
||||||
Just (L loc de) -> do de <- computeConcrete gr de
|
Just (L loc de) -> do de <- computeConcrete gr de
|
||||||
@@ -171,13 +171,13 @@ mkLinDefault gr typ = liftM (Abs Explicit varStr) $ mkDefField typ
|
|||||||
_ -> Bad (render ("linearization type field cannot be" <+> typ))
|
_ -> Bad (render ("linearization type field cannot be" <+> typ))
|
||||||
|
|
||||||
mkLinReference :: SourceGrammar -> Type -> Err Term
|
mkLinReference :: SourceGrammar -> Type -> Err Term
|
||||||
mkLinReference gr typ =
|
mkLinReference gr typ =
|
||||||
liftM (Abs Explicit varStr) $
|
liftM (Abs Explicit varStr) $
|
||||||
case mkDefField typ (Vr varStr) of
|
case mkDefField typ (Vr varStr) of
|
||||||
Bad "no string" -> return Empty
|
Bad "no string" -> return Empty
|
||||||
x -> x
|
x -> x
|
||||||
where
|
where
|
||||||
mkDefField ty trm =
|
mkDefField ty trm =
|
||||||
case ty of
|
case ty of
|
||||||
Table pty ty -> do ps <- allParamValues gr pty
|
Table pty ty -> do ps <- allParamValues gr pty
|
||||||
case ps of
|
case ps of
|
||||||
@@ -203,7 +203,7 @@ factor param c i t =
|
|||||||
T (TComp ty) cs -> factors ty [(p, factor param c (i+1) v) | (p, v) <- cs]
|
T (TComp ty) cs -> factors ty [(p, factor param c (i+1) v) | (p, v) <- cs]
|
||||||
_ -> composSafeOp (factor param c i) t
|
_ -> composSafeOp (factor param c i) t
|
||||||
where
|
where
|
||||||
factors ty pvs0
|
factors ty pvs0
|
||||||
| not param = V ty (map snd pvs0)
|
| not param = V ty (map snd pvs0)
|
||||||
factors ty [] = V ty []
|
factors ty [] = V ty []
|
||||||
factors ty pvs0@[(p,v)] = V ty [v]
|
factors ty pvs0@[(p,v)] = V ty [v]
|
||||||
@@ -224,7 +224,7 @@ factor param c i t =
|
|||||||
replace :: Term -> Term -> Term -> Term
|
replace :: Term -> Term -> Term -> Term
|
||||||
replace old new trm =
|
replace old new trm =
|
||||||
case trm of
|
case trm of
|
||||||
-- these are the important cases, since they can correspond to patterns
|
-- these are the important cases, since they can correspond to patterns
|
||||||
QC _ | trm == old -> new
|
QC _ | trm == old -> new
|
||||||
App _ _ | trm == old -> new
|
App _ _ | trm == old -> new
|
||||||
R _ | trm == old -> new
|
R _ | trm == old -> new
|
||||||
|
|||||||
@@ -10,7 +10,7 @@ import GF.Grammar hiding (Env, VGen, VApp, VRecType)
|
|||||||
import GF.Grammar.Lookup
|
import GF.Grammar.Lookup
|
||||||
import GF.Grammar.Predef
|
import GF.Grammar.Predef
|
||||||
import GF.Grammar.Lockfield
|
import GF.Grammar.Lockfield
|
||||||
import GF.Compile.Compute.ConcreteNew
|
import GF.Compile.Compute.Concrete
|
||||||
import GF.Compile.Compute.Predef(predef,predefName)
|
import GF.Compile.Compute.Predef(predef,predefName)
|
||||||
import GF.Infra.CheckM
|
import GF.Infra.CheckM
|
||||||
import GF.Data.Operations
|
import GF.Data.Operations
|
||||||
@@ -133,7 +133,7 @@ tcRho ge scope t@(RecType rs) (Just ty) = do
|
|||||||
[] -> unifyVar ge scope i env vs vtypePType
|
[] -> unifyVar ge scope i env vs vtypePType
|
||||||
_ -> return ()
|
_ -> return ()
|
||||||
ty -> do ty <- zonkTerm =<< tc_value2term (geLoc ge) (scopeVars scope) ty
|
ty -> do ty <- zonkTerm =<< tc_value2term (geLoc ge) (scopeVars scope) ty
|
||||||
tcError ("The record type" <+> ppTerm Unqualified 0 t $$
|
tcError ("The record type" <+> ppTerm Unqualified 0 t $$
|
||||||
"cannot be of type" <+> ppTerm Unqualified 0 ty)
|
"cannot be of type" <+> ppTerm Unqualified 0 ty)
|
||||||
(rs,mb_ty) <- tcRecTypeFields ge scope rs (Just ty')
|
(rs,mb_ty) <- tcRecTypeFields ge scope rs (Just ty')
|
||||||
return (f (RecType rs),ty)
|
return (f (RecType rs),ty)
|
||||||
@@ -187,7 +187,7 @@ tcRho ge scope (R rs) (Just ty) = do
|
|||||||
case ty' of
|
case ty' of
|
||||||
(VRecType ltys) -> do lttys <- checkRecFields ge scope rs ltys
|
(VRecType ltys) -> do lttys <- checkRecFields ge scope rs ltys
|
||||||
rs <- mapM (\(l,t,ty) -> tc_value2term (geLoc ge) (scopeVars scope) ty >>= \ty -> return (l, (Just ty, t))) lttys
|
rs <- mapM (\(l,t,ty) -> tc_value2term (geLoc ge) (scopeVars scope) ty >>= \ty -> return (l, (Just ty, t))) lttys
|
||||||
return ((f . R) rs,
|
return ((f . R) rs,
|
||||||
VRecType [(l, ty) | (l,t,ty) <- lttys]
|
VRecType [(l, ty) | (l,t,ty) <- lttys]
|
||||||
)
|
)
|
||||||
ty -> do lttys <- inferRecFields ge scope rs
|
ty -> do lttys <- inferRecFields ge scope rs
|
||||||
@@ -277,11 +277,11 @@ tcApp ge scope (App fun arg) = -- APP2
|
|||||||
varg <- liftErr (eval ge (scopeEnv scope) arg)
|
varg <- liftErr (eval ge (scopeEnv scope) arg)
|
||||||
return (App fun arg, res_ty varg)
|
return (App fun arg, res_ty varg)
|
||||||
tcApp ge scope (Q id) = -- VAR (global)
|
tcApp ge scope (Q id) = -- VAR (global)
|
||||||
mkTcA (lookupOverloadTypes (geGrammar ge) id) `bindTcA` \(t,ty) ->
|
mkTcA (lookupOverloadTypes (geGrammar ge) id) `bindTcA` \(t,ty) ->
|
||||||
do ty <- liftErr (eval ge [] ty)
|
do ty <- liftErr (eval ge [] ty)
|
||||||
return (t,ty)
|
return (t,ty)
|
||||||
tcApp ge scope (QC id) = -- VAR (global)
|
tcApp ge scope (QC id) = -- VAR (global)
|
||||||
mkTcA (lookupOverloadTypes (geGrammar ge) id) `bindTcA` \(t,ty) ->
|
mkTcA (lookupOverloadTypes (geGrammar ge) id) `bindTcA` \(t,ty) ->
|
||||||
do ty <- liftErr (eval ge [] ty)
|
do ty <- liftErr (eval ge [] ty)
|
||||||
return (t,ty)
|
return (t,ty)
|
||||||
tcApp ge scope t =
|
tcApp ge scope t =
|
||||||
@@ -350,7 +350,7 @@ tcPatt ge scope (PM q) ty0 = do
|
|||||||
Bad err -> tcError (pp err)
|
Bad err -> tcError (pp err)
|
||||||
tcPatt ge scope p ty = unimplemented ("tcPatt "++show p)
|
tcPatt ge scope p ty = unimplemented ("tcPatt "++show p)
|
||||||
|
|
||||||
inferRecFields ge scope rs =
|
inferRecFields ge scope rs =
|
||||||
mapM (\(l,r) -> tcRecField ge scope l r Nothing) rs
|
mapM (\(l,r) -> tcRecField ge scope l r Nothing) rs
|
||||||
|
|
||||||
checkRecFields ge scope [] ltys
|
checkRecFields ge scope [] ltys
|
||||||
@@ -368,7 +368,7 @@ checkRecFields ge scope ((l,t):lts) ltys =
|
|||||||
where
|
where
|
||||||
takeIt l1 [] = (Nothing, [])
|
takeIt l1 [] = (Nothing, [])
|
||||||
takeIt l1 (lty@(l2,ty):ltys)
|
takeIt l1 (lty@(l2,ty):ltys)
|
||||||
| l1 == l2 = (Just ty,ltys)
|
| l1 == l2 = (Just ty,ltys)
|
||||||
| otherwise = let (mb_ty,ltys') = takeIt l1 ltys
|
| otherwise = let (mb_ty,ltys') = takeIt l1 ltys
|
||||||
in (mb_ty,lty:ltys')
|
in (mb_ty,lty:ltys')
|
||||||
|
|
||||||
@@ -390,7 +390,7 @@ tcRecTypeFields ge scope ((l,ty):rs) mb_ty = do
|
|||||||
| s == cPType -> return mb_ty
|
| s == cPType -> return mb_ty
|
||||||
VMeta _ _ _ -> return mb_ty
|
VMeta _ _ _ -> return mb_ty
|
||||||
_ -> do sort <- zonkTerm =<< tc_value2term (geLoc ge) (scopeVars scope) sort
|
_ -> do sort <- zonkTerm =<< tc_value2term (geLoc ge) (scopeVars scope) sort
|
||||||
tcError ("The record type field" <+> l <+> ':' <+> ppTerm Unqualified 0 ty $$
|
tcError ("The record type field" <+> l <+> ':' <+> ppTerm Unqualified 0 ty $$
|
||||||
"cannot be of type" <+> ppTerm Unqualified 0 sort)
|
"cannot be of type" <+> ppTerm Unqualified 0 sort)
|
||||||
(rs,mb_ty) <- tcRecTypeFields ge scope rs mb_ty
|
(rs,mb_ty) <- tcRecTypeFields ge scope rs mb_ty
|
||||||
return ((l,ty):rs,mb_ty)
|
return ((l,ty):rs,mb_ty)
|
||||||
@@ -444,11 +444,11 @@ subsCheckRho ge scope t (VApp p1 _) (VApp p2 _) -- Rule
|
|||||||
| predefName p1 == cInts && predefName p2 == cInt = return t
|
| predefName p1 == cInts && predefName p2 == cInt = return t
|
||||||
subsCheckRho ge scope t (VApp p1 [VInt i]) (VApp p2 [VInt j]) -- Rule INT2
|
subsCheckRho ge scope t (VApp p1 [VInt i]) (VApp p2 [VInt j]) -- Rule INT2
|
||||||
| predefName p1 == cInts && predefName p2 == cInts =
|
| predefName p1 == cInts && predefName p2 == cInts =
|
||||||
if i <= j
|
if i <= j
|
||||||
then return t
|
then return t
|
||||||
else tcError ("Ints" <+> i <+> "is not a subtype of" <+> "Ints" <+> j)
|
else tcError ("Ints" <+> i <+> "is not a subtype of" <+> "Ints" <+> j)
|
||||||
subsCheckRho ge scope t ty1@(VRecType rs1) ty2@(VRecType rs2) = do -- Rule REC
|
subsCheckRho ge scope t ty1@(VRecType rs1) ty2@(VRecType rs2) = do -- Rule REC
|
||||||
let mkAccess scope t =
|
let mkAccess scope t =
|
||||||
case t of
|
case t of
|
||||||
ExtR t1 t2 -> do (scope,mkProj1,mkWrap1) <- mkAccess scope t1
|
ExtR t1 t2 -> do (scope,mkProj1,mkWrap1) <- mkAccess scope t1
|
||||||
(scope,mkProj2,mkWrap2) <- mkAccess scope t2
|
(scope,mkProj2,mkWrap2) <- mkAccess scope t2
|
||||||
@@ -557,7 +557,7 @@ unify ge scope v (VMeta i env vs) = unifyVar ge scope i env vs v
|
|||||||
unify ge scope v1 v2 = do
|
unify ge scope v1 v2 = do
|
||||||
t1 <- zonkTerm =<< tc_value2term (geLoc ge) (scopeVars scope) v1
|
t1 <- zonkTerm =<< tc_value2term (geLoc ge) (scopeVars scope) v1
|
||||||
t2 <- zonkTerm =<< tc_value2term (geLoc ge) (scopeVars scope) v2
|
t2 <- zonkTerm =<< tc_value2term (geLoc ge) (scopeVars scope) v2
|
||||||
tcError ("Cannot unify terms:" <+> (ppTerm Unqualified 0 t1 $$
|
tcError ("Cannot unify terms:" <+> (ppTerm Unqualified 0 t1 $$
|
||||||
ppTerm Unqualified 0 t2))
|
ppTerm Unqualified 0 t2))
|
||||||
|
|
||||||
-- | Invariant: tv1 is a flexible type variable
|
-- | Invariant: tv1 is a flexible type variable
|
||||||
@@ -609,7 +609,7 @@ quantify ge scope t tvs ty0 = do
|
|||||||
ty <- tc_value2term (geLoc ge) (scopeVars scope) ty0
|
ty <- tc_value2term (geLoc ge) (scopeVars scope) ty0
|
||||||
let used_bndrs = nub (bndrs ty) -- Avoid quantified type variables in use
|
let used_bndrs = nub (bndrs ty) -- Avoid quantified type variables in use
|
||||||
new_bndrs = take (length tvs) (allBinders \\ used_bndrs)
|
new_bndrs = take (length tvs) (allBinders \\ used_bndrs)
|
||||||
mapM_ bind (tvs `zip` new_bndrs) -- 'bind' is just a cunning way
|
mapM_ bind (tvs `zip` new_bndrs) -- 'bind' is just a cunning way
|
||||||
ty <- zonkTerm ty -- of doing the substitution
|
ty <- zonkTerm ty -- of doing the substitution
|
||||||
vty <- liftErr (eval ge [] (foldr (\v ty -> Prod Implicit v typeType ty) ty new_bndrs))
|
vty <- liftErr (eval ge [] (foldr (\v ty -> Prod Implicit v typeType ty) ty new_bndrs))
|
||||||
return (foldr (Abs Implicit) t new_bndrs,vty)
|
return (foldr (Abs Implicit) t new_bndrs,vty)
|
||||||
@@ -619,7 +619,7 @@ quantify ge scope t tvs ty0 = do
|
|||||||
bndrs (Prod _ x t1 t2) = [x] ++ bndrs t1 ++ bndrs t2
|
bndrs (Prod _ x t1 t2) = [x] ++ bndrs t1 ++ bndrs t2
|
||||||
bndrs _ = []
|
bndrs _ = []
|
||||||
|
|
||||||
allBinders :: [Ident] -- a,b,..z, a1, b1,... z1, a2, b2,...
|
allBinders :: [Ident] -- a,b,..z, a1, b1,... z1, a2, b2,...
|
||||||
allBinders = [ identS [x] | x <- ['a'..'z'] ] ++
|
allBinders = [ identS [x] | x <- ['a'..'z'] ] ++
|
||||||
[ identS (x : show i) | i <- [1 :: Integer ..], x <- ['a'..'z']]
|
[ identS (x : show i) | i <- [1 :: Integer ..], x <- ['a'..'z']]
|
||||||
|
|
||||||
@@ -688,12 +688,12 @@ runTcM f = case unTcM f IntMap.empty [] of
|
|||||||
TcFail (msg:msgs) -> do checkWarnings msgs; checkError msg
|
TcFail (msg:msgs) -> do checkWarnings msgs; checkError msg
|
||||||
|
|
||||||
newMeta :: Scope -> Sigma -> TcM MetaId
|
newMeta :: Scope -> Sigma -> TcM MetaId
|
||||||
newMeta scope ty = TcM (\ms msgs ->
|
newMeta scope ty = TcM (\ms msgs ->
|
||||||
let i = IntMap.size ms
|
let i = IntMap.size ms
|
||||||
in TcOk i (IntMap.insert i (Unbound scope ty) ms) msgs)
|
in TcOk i (IntMap.insert i (Unbound scope ty) ms) msgs)
|
||||||
|
|
||||||
getMeta :: MetaId -> TcM MetaValue
|
getMeta :: MetaId -> TcM MetaValue
|
||||||
getMeta i = TcM (\ms msgs ->
|
getMeta i = TcM (\ms msgs ->
|
||||||
case IntMap.lookup i ms of
|
case IntMap.lookup i ms of
|
||||||
Just mv -> TcOk mv ms msgs
|
Just mv -> TcOk mv ms msgs
|
||||||
Nothing -> TcFail (("Unknown metavariable" <+> ppMeta i) : msgs))
|
Nothing -> TcFail (("Unknown metavariable" <+> ppMeta i) : msgs))
|
||||||
@@ -702,7 +702,7 @@ setMeta :: MetaId -> MetaValue -> TcM ()
|
|||||||
setMeta i mv = TcM (\ms msgs -> TcOk () (IntMap.insert i mv ms) msgs)
|
setMeta i mv = TcM (\ms msgs -> TcOk () (IntMap.insert i mv ms) msgs)
|
||||||
|
|
||||||
newVar :: Scope -> Ident
|
newVar :: Scope -> Ident
|
||||||
newVar scope = head [x | i <- [1..],
|
newVar scope = head [x | i <- [1..],
|
||||||
let x = identS ('v':show i),
|
let x = identS ('v':show i),
|
||||||
isFree scope x]
|
isFree scope x]
|
||||||
where
|
where
|
||||||
@@ -721,7 +721,7 @@ getMetaVars loc sc_tys = do
|
|||||||
return (foldr go [] tys)
|
return (foldr go [] tys)
|
||||||
where
|
where
|
||||||
-- Get the MetaIds from a term; no duplicates in result
|
-- Get the MetaIds from a term; no duplicates in result
|
||||||
go (Vr tv) acc = acc
|
go (Vr tv) acc = acc
|
||||||
go (App x y) acc = go x (go y acc)
|
go (App x y) acc = go x (go y acc)
|
||||||
go (Meta i) acc
|
go (Meta i) acc
|
||||||
| i `elem` acc = acc
|
| i `elem` acc = acc
|
||||||
@@ -741,7 +741,7 @@ getFreeVars loc sc_tys = do
|
|||||||
tys <- mapM (\(scope,ty) -> zonkTerm =<< tc_value2term loc (scopeVars scope) ty) sc_tys
|
tys <- mapM (\(scope,ty) -> zonkTerm =<< tc_value2term loc (scopeVars scope) ty) sc_tys
|
||||||
return (foldr (go []) [] tys)
|
return (foldr (go []) [] tys)
|
||||||
where
|
where
|
||||||
go bound (Vr tv) acc
|
go bound (Vr tv) acc
|
||||||
| tv `elem` bound = acc
|
| tv `elem` bound = acc
|
||||||
| tv `elem` acc = acc
|
| tv `elem` acc = acc
|
||||||
| otherwise = tv : acc
|
| otherwise = tv : acc
|
||||||
@@ -771,7 +771,7 @@ tc_value2term loc xs v =
|
|||||||
|
|
||||||
|
|
||||||
|
|
||||||
data TcA x a
|
data TcA x a
|
||||||
= TcSingle (MetaStore -> [Message] -> TcResult a)
|
= TcSingle (MetaStore -> [Message] -> TcResult a)
|
||||||
| TcMany [x] (MetaStore -> [Message] -> [(a,MetaStore,[Message])])
|
| TcMany [x] (MetaStore -> [Message] -> [(a,MetaStore,[Message])])
|
||||||
|
|
||||||
|
|||||||
Reference in New Issue
Block a user