msyds/gf-core
1
0
Fork 0
forked from GitHub/gf-core
Code Pull Requests Activity

Merge branch 'master' into c-runtime

Browse Source
This commit is contained in:
krangelov
2021-07-30 11:20:04 +02:00
parent eece3e86b3 265f08d6ee
commit 155657709a
211 changed files with 7161 additions and 58549 deletions
Download Patch File Download Diff File Expand all files Collapse all files

1
src/compiler/GF/Compile/CFGtoPGF.hs
View File

@@ -134,4 +134,3 @@ mkRuleName rule =
case ruleName rule of
CFObj n _ -> n
_ -> "_"

55
src/compiler/GF/Compile/CheckGrammar.hs
View File

@@ -5,7 +5,7 @@
-- Stability : (stable)
-- Portability : (portable)
--
-- > CVS $Date: 2005/11/11 23:24:33 $
-- > CVS $Date: 2005/11/11 23:24:33 $
-- > CVS $Author: aarne $
-- > CVS $Revision: 1.31 $
--
@@ -22,13 +22,14 @@
module GF.Compile.CheckGrammar(checkModule) where
import Prelude hiding ((<>))
import GF.Infra.Ident
import GF.Infra.Option
import GF.Compile.TypeCheck.Abstract
import GF.Compile.TypeCheck.RConcrete
import qualified GF.Compile.TypeCheck.ConcreteNew as CN
import qualified GF.Compile.Compute.ConcreteNew as CN
import GF.Compile.TypeCheck.Concrete(computeLType,checkLType,inferLType,ppType)
import qualified GF.Compile.TypeCheck.ConcreteNew as CN(checkLType,inferLType)
import qualified GF.Compile.Compute.Concrete as CN(normalForm,resourceValues)
import GF.Grammar
import GF.Grammar.Lexer
@@ -73,9 +74,9 @@ checkRestrictedInheritance cwd sgr (name,mo) = checkInModule cwd mo NoLoc empty
let (incl,excl) = partition (isInherited mi) (Map.keys (jments m))
let incld c = Set.member c (Set.fromList incl)
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)]
case illegals of
case illegals of
[] -> return ()
cs -> checkWarn ("In inherited module" <+> i <> ", dependence of excluded constants:" $$
nest 2 (vcat [f <+> "on" <+> fsep is | (f,is) <- cs]))
@@ -91,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
jsc <- foldM checkAbs jsc (Map.toList jsa)
return (cm,cnc{jments=jsc})
where
checkAbs js i@(c,info) =
case info of
AbsFun (Just (L loc ty)) _ _ _
AbsFun (Just (L loc ty)) _ _ _
-> do let mb_def = do
let (cxt,(_,i),_) = typeForm ty
info <- lookupIdent i js
@@ -135,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}")
return $ Map.insert c (CncCat (Just (L NoLoc defLinType)) Nothing Nothing Nothing Nothing) js
_ -> return js
checkCnc js (c,info) =
case info 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
let linty = (snd (valCat ty),cont,val)
return $ Map.insert c (CncFun (Just linty) d mn mf) js
@@ -158,14 +159,14 @@ checkCompleteGrammar opts cwd gr (am,abs) (cm,cnc) = checkInModule cwd cnc NoLoc
_ -> 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.
checkInfo :: Options -> FilePath -> SourceGrammar -> SourceModule -> Ident -> Info -> Check Info
checkInfo opts cwd sgr (m,mo) c info = checkInModule cwd mo NoLoc empty $ do
checkReservedId c
case info of
AbsCat (Just (L loc cont)) ->
mkCheck loc "the category" $
AbsCat (Just (L loc cont)) ->
mkCheck loc "the category" $
checkContext gr cont
AbsFun (Just (L loc typ0)) ma md moper -> do
@@ -174,13 +175,13 @@ checkInfo opts cwd sgr (m,mo) c info = checkInModule cwd mo NoLoc empty $ do
checkTyp gr typ
case md of
Just eqs -> mapM_ (\(L loc eq) -> mkCheck loc "the definition of function" $
checkDef gr (m,c) typ eq) eqs
checkDef gr (m,c) typ eq) eqs
Nothing -> return ()
return (AbsFun (Just (L loc typ)) ma md moper)
CncCat mty mdef mref mpr mpmcfg -> do
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
then do (typ,_) <- CN.checkLType (CN.resourceValues opts gr) typ typeType
typ <- computeLType gr [] typ
@@ -190,19 +191,19 @@ checkInfo opts cwd sgr (m,mo) c info = checkInModule cwd mo NoLoc empty $ do
return (Just (L loc typ)))
Nothing -> return Nothing
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
(def,_) <- checkLType gr [] def (mkFunType [typeStr] typ)
return (Just (L loc def))
_ -> return Nothing
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
(ref,_) <- checkLType gr [] ref (mkFunType [typ] typeStr)
return (Just (L loc ref))
_ -> return Nothing
mpr <- case mpr of
(Just (L loc t)) ->
(Just (L loc t)) ->
chIn loc "print name of" $ do
(t,_) <- checkLType gr [] t typeStr
return (Just (L loc t))
@@ -211,13 +212,13 @@ checkInfo opts cwd sgr (m,mo) c info = checkInModule cwd mo NoLoc empty $ do
CncFun mty mt mpr mpmcfg -> do
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
(trm,_) <- checkLType gr [] trm (mkFunType (map (\(_,_,ty) -> ty) cont) val) -- erases arg vars
return (Just (L loc trm))
_ -> return mt
mpr <- case mpr of
(Just (L loc t)) ->
(Just (L loc t)) ->
chIn loc "print name of" $ do
(t,_) <- checkLType gr [] t typeStr
return (Just (L loc t))
@@ -250,16 +251,16 @@ checkInfo opts cwd sgr (m,mo) c info = checkInModule cwd mo NoLoc empty $ 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
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]
--- this can only be a partial guarantee, since matching
--- 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]
return (ResOverload os [(y,x) | (x,y) <- tysts'])
ResParam (Just (L loc pcs)) _ -> do
ts <- chIn loc "parameter type" $
ts <- chIn loc "parameter type" $
liftM concat $ mapM mkPar pcs
return (ResParam (Just (L loc pcs)) (Just ts))
@@ -273,9 +274,9 @@ checkInfo opts cwd sgr (m,mo) c info = checkInModule cwd mo NoLoc empty $ do
return $ map (mkApp (QC (m,f))) vs
checkUniq xss = case xss of
x:y:xs
x:y:xs
| x == y -> checkError $ "ambiguous for type" <+>
ppType (mkFunType (tail x) (head x))
ppType (mkFunType (tail x) (head x))
| otherwise -> checkUniq $ y:xs
_ -> return ()
@@ -293,7 +294,7 @@ checkInfo opts cwd sgr (m,mo) c info = checkInModule cwd mo NoLoc empty $ do
t' <- compAbsTyp ((x,Vr x):g) t
return $ Prod b x a' t'
Abs _ _ _ -> return t
_ -> composOp (compAbsTyp g) t
_ -> composOp (compAbsTyp g) t
-- | for grammars obtained otherwise than by parsing ---- update!!
@@ -315,7 +316,7 @@ linTypeOfType cnc m typ = do
mkLinArg (i,(n,mc@(m,cat))) = do
val <- lookLin mc
let vars = mkRecType varLabel $ replicate n typeStr
symb = argIdent n cat i
symb = argIdent n cat i
rec <- if n==0 then return val else
errIn (render ("extending" $$
nest 2 vars $$

593
src/compiler/GF/Compile/Compute/Concrete.hs
View File

@@ -1,3 +1,590 @@
module GF.Compile.Compute.Concrete{-(module M)-} where
--import GF.Compile.Compute.ConcreteLazy as M -- New
--import GF.Compile.Compute.ConcreteStrict as M -- Old, inefficient
-- | 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
) 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 :: 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 :: 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 = 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"
]
-- | 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 =
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: "++)
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 =
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
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 = 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

579
src/compiler/GF/Compile/Compute/ConcreteNew.hs
View File

@@ -1,579 +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 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
in error . render $
ppL loc (hang "unsupported token gluing:" 4
(Glue (vt v1) (vt v2)))
-- | 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)
_ -> bug ("value2term "++show loc++" : "++show v0)
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:" 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

4
src/compiler/GF/Compile/Compute/Predef.hs
View File

@@ -27,6 +27,10 @@ instance Predef Int where
instance Predef Bool where
toValue = boolV
fromValue v = case v of
VCApp (mn,i) [] | mn == cPredef && i == cPTrue -> return True
VCApp (mn,i) [] | mn == cPredef && i == cPFalse -> return False
_ -> verror "Bool" v
instance Predef String where
toValue = string

8
src/compiler/GF/Compile/Compute/Value.hs
View File

@@ -12,8 +12,8 @@ data Value
| VGen Int [Value] -- for lambda bound variables, possibly applied
| VMeta MetaId Env [Value]
-- -- | VClosure Env Term -- used in Typecheck.ConcreteNew
| VAbs BindType Ident Binding -- used in Compute.ConcreteNew
| VProd BindType Value Ident Binding -- used in Compute.ConcreteNew
| VAbs BindType Ident Binding -- used in Compute.Concrete
| VProd BindType Value Ident Binding -- used in Compute.Concrete
| VInt Int
| VFloat Double
| VString String
@@ -47,10 +47,10 @@ type Env = [(Ident,Value)]
-- | Predefined functions
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 -}
| Error | Trace
-- 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
deriving (Show,Eq,Ord,Ix,Bounded,Enum)

47
src/compiler/GF/Compile/ConcreteToHaskell.hs
View File

@@ -7,7 +7,7 @@ import GF.Text.Pretty
--import GF.Grammar.Predef(cPredef,cInts)
--import GF.Compile.Compute.Predef(predef)
--import GF.Compile.Compute.Value(Predefined(..))
import GF.Infra.Ident(Ident,identS,identW,prefixIdent)
import GF.Infra.Ident(Ident,identC,identS,identW,prefixIdent,showRawIdent,rawIdentS)
import GF.Infra.Option
import GF.Haskell as H
import GF.Grammar.Canonical as C
@@ -21,7 +21,7 @@ concretes2haskell opts absname gr =
| let Grammar abstr cncs = grammar2canonical opts absname gr,
cncmod<-cncs,
let ModId name = concName cncmod
filename = name ++ ".hs" :: FilePath
filename = showRawIdent name ++ ".hs" :: FilePath
]
-- | Generate Haskell code for the given concrete module.
@@ -53,7 +53,7 @@ concrete2haskell opts
labels = S.difference (S.unions (map S.fromList recs)) common_labels
common_records = S.fromList [[label_s]]
common_labels = S.fromList [label_s]
label_s = LabelId "s"
label_s = LabelId (rawIdentS "s")
signature (CatDef c _) = TypeSig lf (Fun abs (pure lin))
where
@@ -69,7 +69,7 @@ concrete2haskell opts
where
--funcats = S.fromList [c | FunDef f (C.Type _ (TypeApp c _))<-funs]
allcats = S.fromList [c | CatDef c _<-cats]
gId :: ToIdent i => i -> Ident
gId = (if haskellOption opts HaskellNoPrefix then id else prefixIdent "G")
. toIdent
@@ -116,7 +116,7 @@ concrete2haskell opts
where (ls,ts) = unzip $ sortOn fst [(l,t)|RecordRow l t<-rs]
StrType -> tcon0 (identS "Str")
TableType pt lt -> Fun (ppT pt) (ppT lt)
-- TupleType lts ->
-- TupleType lts ->
lincatDef (LincatDef c t) = tsyn0 (lincatName c) (convLinType t)
@@ -126,7 +126,7 @@ concrete2haskell opts
linDefs = map eqn . sortOn fst . map linDef
where eqn (cat,(f,(ps,rhs))) = (cat,Eqn (f,ps) rhs)
linDef (LinDef f xs rhs0) =
linDef (LinDef f xs rhs0) =
(cat,(linfunName cat,(lhs,rhs)))
where
lhs = [ConP (aId f) (map VarP abs_args)]
@@ -144,7 +144,7 @@ concrete2haskell opts
where
vs = [(VarValueId (Unqual x),a)|(VarId x,a)<-zip xs args]
env= [(VarValueId (Unqual x),lc)|(VarId x,lc)<-zip xs (map arglincat absctx)]
letlin a (TypeBinding _ (C.Type _ (TypeApp acat _))) =
(a,Ap (Var (linfunName acat)) (Var (abs_arg a)))
@@ -187,7 +187,7 @@ concrete2haskell opts
pId p@(ParamId s) =
if "to_R_" `isPrefixOf` unqual s then toIdent p else gId p -- !! a hack
table cs =
if all (null.patVars) ps
then lets ds (LambdaCase [(ppP p,t')|(p,t')<-zip ps ts'])
@@ -315,13 +315,13 @@ instance Records rhs => Records (TableRow rhs) where
-- | Record subtyping is converted into explicit coercions in Haskell
coerce env ty t =
case (ty,t) of
case (ty,t) of
(_,VariantValue ts) -> VariantValue (map (coerce env ty) ts)
(TableType ti tv,TableValue _ cs) ->
TableValue ti [TableRow p (coerce env tv t)|TableRow p t<-cs]
(RecordType rt,RecordValue r) ->
RecordValue [RecordRow l (coerce env ft f) |
RecordRow l f<-r,ft<-[ft|RecordRow l' ft<-rt,l'==l]]
RecordRow l f<-r,ft<-[ft | RecordRow l' ft <- rt, l'==l]]
(RecordType rt,VarValue x)->
case lookup x env of
Just ty' | ty'/=ty -> -- better to compare to normal form of ty'
@@ -334,18 +334,17 @@ coerce env ty t =
_ -> t
where
app f ts = ParamConstant (Param f ts) -- !! a hack
to_rcon = ParamId . Unqual . to_rcon' . labels
to_rcon = ParamId . Unqual . rawIdentS . to_rcon' . labels
patVars p = []
labels r = [l|RecordRow l _<-r]
labels r = [l | RecordRow l _ <- r]
proj = Var . identS . proj'
proj' (LabelId l) = "proj_"++l
proj' (LabelId l) = "proj_" ++ showRawIdent l
rcon = Var . rcon'
rcon' = identS . rcon_name
rcon_name ls = "R"++concat (sort ['_':l|LabelId l<-ls])
rcon_name ls = "R"++concat (sort ['_':showRawIdent l | LabelId l <- ls])
to_rcon' = ("to_"++) . rcon_name
recordType ls =
@@ -400,17 +399,17 @@ linfunName c = prefixIdent "lin" (toIdent c)
class ToIdent i where toIdent :: i -> Ident
instance ToIdent ParamId where toIdent (ParamId q) = qIdentS q
instance ToIdent PredefId where toIdent (PredefId s) = identS s
instance ToIdent CatId where toIdent (CatId s) = identS s
instance ToIdent C.FunId where toIdent (FunId s) = identS s
instance ToIdent VarValueId where toIdent (VarValueId q) = qIdentS q
instance ToIdent ParamId where toIdent (ParamId q) = qIdentC q
instance ToIdent PredefId where toIdent (PredefId s) = identC s
instance ToIdent CatId where toIdent (CatId s) = identC s
instance ToIdent C.FunId where toIdent (FunId s) = identC s
instance ToIdent VarValueId where toIdent (VarValueId q) = qIdentC q
qIdentS = identS . unqual
qIdentC = identS . unqual
unqual (Qual (ModId m) n) = m++"_"++n
unqual (Unqual n) = n
unqual (Qual (ModId m) n) = showRawIdent m++"_"++ showRawIdent n
unqual (Unqual n) = showRawIdent n
instance ToIdent VarId where
toIdent Anonymous = identW
toIdent (VarId s) = identS s
toIdent (VarId s) = identC s

31
src/compiler/GF/Compile/GeneratePMCFG.hs
View File

@@ -26,7 +26,7 @@ import GF.Data.BacktrackM
import GF.Data.Operations
import GF.Infra.UseIO (ePutStr,ePutStrLn) -- IOE,
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.Set as Set
import qualified Data.List as List
@@ -42,6 +42,7 @@ import Control.Monad
import Control.Monad.Identity
--import Control.Exception
--import Debug.Trace(trace)
import qualified Control.Monad.Fail as Fail
----------------------------------------------------------------------
-- main conversion function
@@ -82,7 +83,7 @@ addPMCFG opts gr cenv opath am cm seqs id (CncFun mty@(Just (cat,cont,val)) mlin
(goB b1 CNil [])
(pres,pargs)
pmcfg = getPMCFG pmcfgEnv1
stats = let PMCFG prods funs = pmcfg
(s,e) = bounds funs
!prods_cnt = length prods
@@ -200,6 +201,9 @@ newtype CnvMonad a = CM {unCM :: SourceGrammar
-> ([ProtoFCat],[Symbol])
-> Branch b}
instance Fail.MonadFail CnvMonad where
fail = bug
instance Applicative CnvMonad where
pure = return
(<*>) = ap
@@ -243,7 +247,7 @@ choices nr path = do (args,_) <- get
| (value,index) <- values])
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
Just args -> c value (args,seq)
Nothing -> bug "conflict in updateEnv"
@@ -604,7 +608,7 @@ restrictProtoFCat path v (PFCat cat f schema) = do
Just index -> return (CPar (m,[(v,index)]))
Nothing -> mzero
addConstraint CNil v (CStr _) = bug "restrictProtoFCat: string path"
update k0 f [] = return []
update k0 f (x@(k,Identity v):xs)
| k0 == k = do v <- f v
@@ -616,6 +620,23 @@ mkArray lst = listArray (0,length lst-1) lst
mkSetArray map = array (0,Map.size map-1) [(v,k) | (k,v) <- Map.toList map]
bug msg = ppbug msg
ppbug msg = error . render $ hang "Internal error in GeneratePMCFG:" 4 msg
ppbug msg = error completeMsg
where
originalMsg = render $ hang "Internal error in GeneratePMCFG:" 4 msg
completeMsg =
case render msg of -- the error message for pattern matching a runtime string
"descend (CStr 0,CNil,CProj (LIdent (Id {rawId2utf8 = \"s\"})) CNil)"
-> unlines [originalMsg -- add more helpful output
,""
,"1) Check that you are not trying to pattern match a /runtime string/."
," These are illegal:"
," lin Test foo = case foo.s of {"
," \"str\" => … } ; <- explicit matching argument of a lin"
," lin Test foo = opThatMatches foo <- calling an oper that pattern matches"
,""
,"2) Not about pattern matching? Submit a bug report and we update the error message."
," https://github.com/GrammaticalFramework/gf-core/issues"
]
_ -> originalMsg -- any other message: just print it as is
ppU = ppTerm Unqualified

142
src/compiler/GF/Compile/GrammarToCanonical.hs
View File

@@ -6,30 +6,35 @@ module GF.Compile.GrammarToCanonical(
) where
import Data.List(nub,partition)
import qualified Data.Map as M
import Data.Maybe(fromMaybe)
import qualified Data.Set as S
import GF.Data.ErrM
import GF.Text.Pretty
import GF.Grammar.Grammar
import GF.Grammar.Grammar as G
import GF.Grammar.Lookup(lookupOrigInfo,allOrigInfos,allParamValues)
import GF.Grammar.Macros(typeForm,collectOp,collectPattOp,mkAbs,mkApp,term2patt)
import GF.Grammar.Macros(typeForm,collectOp,collectPattOp,composSafeOp,mkAbs,mkApp,term2patt,sortRec)
import GF.Grammar.Lockfield(isLockLabel)
import GF.Grammar.Predef(cPredef,cInts)
import GF.Compile.Compute.Predef(predef)
import GF.Compile.Compute.Value(Predefined(..))
import GF.Infra.Ident(ModuleName(..),Ident,prefixIdent,showIdent,isWildIdent)
import GF.Infra.Option(optionsPGF)
import GF.Infra.Ident(ModuleName(..),Ident,ident2raw,rawIdentS,showIdent,isWildIdent)
import GF.Infra.Option(Options,optionsPGF)
import PGF2.Internal(Literal(..))
import GF.Compile.Compute.ConcreteNew(normalForm,resourceValues)
import GF.Compile.Compute.Concrete(GlobalEnv,normalForm,resourceValues)
import GF.Grammar.Canonical as C
import Debug.Trace
import System.FilePath ((</>), (<.>))
import qualified Debug.Trace as T
-- | Generate Canonical code for the named abstract syntax and all associated
-- concrete syntaxes
grammar2canonical :: Options -> ModuleName -> G.Grammar -> C.Grammar
grammar2canonical opts absname gr =
Grammar (abstract2canonical absname gr)
(map snd (concretes2canonical opts absname gr))
-- | Generate Canonical code for the named abstract syntax
abstract2canonical :: ModuleName -> G.Grammar -> Abstract
abstract2canonical absname gr =
Abstract (modId absname) (convFlags gr absname) cats funs
where
@@ -44,6 +49,7 @@ abstract2canonical absname gr =
convHypo (bt,name,t) =
case typeForm t of
([],(_,cat),[]) -> gId cat -- !!
tf -> error $ "abstract2canonical convHypo: " ++ show tf
convType t =
case typeForm t of
@@ -54,25 +60,26 @@ abstract2canonical absname gr =
convHypo' (bt,name,t) = TypeBinding (gId name) (convType t)
-- | Generate Canonical code for the all concrete syntaxes associated with
-- the named abstract syntax in given the grammar.
concretes2canonical :: Options -> ModuleName -> G.Grammar -> [(FilePath, Concrete)]
concretes2canonical opts absname gr =
[(cncname,concrete2canonical gr cenv absname cnc cncmod)
| let cenv = resourceValues opts gr,
cnc<-allConcretes gr absname,
let cncname = "canonical/"++render cnc ++ ".gf" :: FilePath
let cncname = "canonical" </> render cnc <.> "gf"
Ok cncmod = lookupModule gr cnc
]
-- | Generate Canonical GF for the given concrete module.
concrete2canonical :: G.Grammar -> GlobalEnv -> ModuleName -> ModuleName -> ModuleInfo -> Concrete
concrete2canonical gr cenv absname cnc modinfo =
Concrete (modId cnc) (modId absname) (convFlags gr cnc)
(neededParamTypes S.empty (params defs))
[lincat|(_,Left lincat)<-defs]
[lin|(_,Right lin)<-defs]
[lincat | (_,Left lincat) <- defs]
[lin | (_,Right lin) <- defs]
where
defs = concatMap (toCanonical gr absname cenv) .
defs = concatMap (toCanonical gr absname cenv) .
M.toList $
jments modinfo
@@ -85,6 +92,7 @@ concrete2canonical gr cenv absname cnc modinfo =
else let ((got,need),def) = paramType gr q
in def++neededParamTypes (S.union got have) (S.toList need++qs)
-- toCanonical :: G.Grammar -> ModuleName -> GlobalEnv -> (Ident, Info) -> [(S.Set QIdent, Either LincatDef LinDef)]
toCanonical gr absname cenv (name,jment) =
case jment of
CncCat (Just (L loc typ)) _ _ pprn _ ->
@@ -97,7 +105,8 @@ toCanonical gr absname cenv (name,jment) =
where
tts = tableTypes gr [e']
e' = unAbs (length params) $
e' = cleanupRecordFields lincat $
unAbs (length params) $
nf loc (mkAbs params (mkApp def (map Vr args)))
params = [(b,x)|(b,x,_)<-ctx]
args = map snd params
@@ -108,12 +117,12 @@ toCanonical gr absname cenv (name,jment) =
_ -> []
where
nf loc = normalForm cenv (L loc name)
-- aId n = prefixIdent "A." (gId n)
unAbs 0 t = t
unAbs n (Abs _ _ t) = unAbs (n-1) t
unAbs _ t = t
tableTypes :: G.Grammar -> [Term] -> S.Set QIdent
tableTypes gr ts = S.unions (map tabtys ts)
where
tabtys t =
@@ -122,6 +131,7 @@ tableTypes gr ts = S.unions (map tabtys ts)
T (TTyped t) cs -> S.union (paramTypes gr t) (tableTypes gr (map snd cs))
_ -> collectOp tabtys t
paramTypes :: G.Grammar -> G.Type -> S.Set QIdent
paramTypes gr t =
case t of
RecType fs -> S.unions (map (paramTypes gr.snd) fs)
@@ -140,11 +150,26 @@ paramTypes gr t =
Ok (_,ResParam {}) -> S.singleton q
_ -> ignore
ignore = trace ("Ignore: "++show t) S.empty
ignore = T.trace ("Ignore: " ++ show t) S.empty
-- | Filter out record fields from definitions which don't appear in lincat.
cleanupRecordFields :: G.Type -> Term -> Term
cleanupRecordFields (RecType ls) (R as) =
let defnFields = M.fromList ls
in R
[ (lbl, (mty, t'))
| (lbl, (mty, t)) <- as
, M.member lbl defnFields
, let Just ty = M.lookup lbl defnFields
, let t' = cleanupRecordFields ty t
]
cleanupRecordFields ty t@(FV _) = composSafeOp (cleanupRecordFields ty) t
cleanupRecordFields _ t = t
convert :: G.Grammar -> Term -> LinValue
convert gr = convert' gr []
convert' :: G.Grammar -> [Ident] -> Term -> LinValue
convert' gr vs = ppT
where
ppT0 = convert' gr vs
@@ -162,20 +187,20 @@ convert' gr vs = ppT
S t p -> selection (ppT t) (ppT p)
C t1 t2 -> concatValue (ppT t1) (ppT t2)
App f a -> ap (ppT f) (ppT a)
R r -> RecordValue (fields r)
R r -> RecordValue (fields (sortRec r))
P t l -> projection (ppT t) (lblId l)
Vr x -> VarValue (gId x)
Cn x -> VarValue (gId x) -- hmm
Con c -> ParamConstant (Param (gId c) [])
Sort k -> VarValue (gId k)
EInt n -> LiteralValue (IntConstant n)
Q (m,n) -> if m==cPredef then ppPredef n else VarValue ((gQId m n))
QC (m,n) -> ParamConstant (Param ((gQId m n)) [])
Q (m,n) -> if m==cPredef then ppPredef n else VarValue (gQId m n)
QC (m,n) -> ParamConstant (Param (gQId m n) [])
K s -> LiteralValue (StrConstant s)
Empty -> LiteralValue (StrConstant "")
FV ts -> VariantValue (map ppT ts)
Alts t' vs -> alts vs (ppT t')
_ -> error $ "convert' "++show t
_ -> error $ "convert' ppT: " ++ show t
ppCase (p,t) = TableRow (ppP p) (ppTv (patVars p++vs) t)
@@ -188,12 +213,12 @@ convert' gr vs = ppT
Ok ALL_CAPIT -> p "ALL_CAPIT"
_ -> VarValue (gQId cPredef n) -- hmm
where
p = PredefValue . PredefId
p = PredefValue . PredefId . rawIdentS
ppP p =
case p of
PC c ps -> ParamPattern (Param (gId c) (map ppP ps))
PP (m,c) ps -> ParamPattern (Param ((gQId m c)) (map ppP ps))
PP (m,c) ps -> ParamPattern (Param (gQId m c) (map ppP ps))
PR r -> RecordPattern (fields r) {-
PW -> WildPattern
PV x -> VarP x
@@ -202,6 +227,7 @@ convert' gr vs = ppT
PFloat x -> Lit (show x)
PT _ p -> ppP p
PAs x p -> AsP x (ppP p) -}
_ -> error $ "convert' ppP: " ++ show p
where
fields = map field . filter (not.isLockLabel.fst)
field (l,p) = RecordRow (lblId l) (ppP p)
@@ -218,12 +244,12 @@ convert' gr vs = ppT
pre Empty = [""] -- Empty == K ""
pre (Strs ts) = concatMap pre ts
pre (EPatt p) = pat p
pre t = error $ "pre "++show t
pre t = error $ "convert' alts pre: " ++ show t
pat (PString s) = [s]
pat (PAlt p1 p2) = pat p1++pat p2
pat (PSeq p1 p2) = [s1++s2 | s1<-pat p1, s2<-pat p2]
pat p = error $ "pat "++show p
pat p = error $ "convert' alts pat: "++show p
fields = map field . filter (not.isLockLabel.fst)
field (l,(_,t)) = RecordRow (lblId l) (ppT t)
@@ -236,6 +262,7 @@ convert' gr vs = ppT
ParamConstant (Param p (ps++[a]))
_ -> error $ "convert' ap: "++render (ppA f <+> ppA a)
concatValue :: LinValue -> LinValue -> LinValue
concatValue v1 v2 =
case (v1,v2) of
(LiteralValue (StrConstant ""),_) -> v2
@@ -243,21 +270,24 @@ concatValue v1 v2 =
_ -> ConcatValue v1 v2
-- | Smart constructor for projections
projection r l = maybe (Projection r l) id (proj r l)
projection :: LinValue -> LabelId -> LinValue
projection r l = fromMaybe (Projection r l) (proj r l)
proj :: LinValue -> LabelId -> Maybe LinValue
proj r l =
case r of
RecordValue r -> case [v|RecordRow l' v<-r,l'==l] of
RecordValue r -> case [v | RecordRow l' v <- r, l'==l] of
[v] -> Just v
_ -> Nothing
_ -> Nothing
-- | Smart constructor for selections
selection :: LinValue -> LinValue -> LinValue
selection t v =
-- Note: impossible cases can become possible after grammar transformation
case t of
TableValue tt r ->
case nub [rv|TableRow _ rv<-keep] of
case nub [rv | TableRow _ rv <- keep] of
[rv] -> rv
_ -> Selection (TableValue tt r') v
where
@@ -276,13 +306,16 @@ selection t v =
(keep,discard) = partition (mightMatchRow v) r
_ -> Selection t v
impossible :: LinValue -> LinValue
impossible = CommentedValue "impossible"
mightMatchRow :: LinValue -> TableRow rhs -> Bool
mightMatchRow v (TableRow p _) =
case p of
WildPattern -> True
_ -> mightMatch v p
mightMatch :: LinValue -> LinPattern -> Bool
mightMatch v p =
case v of
ConcatValue _ _ -> False
@@ -294,16 +327,18 @@ mightMatch v p =
RecordValue rv ->
case p of
RecordPattern rp ->
and [maybe False (flip mightMatch p) (proj v l) | RecordRow l p<-rp]
and [maybe False (`mightMatch` p) (proj v l) | RecordRow l p<-rp]
_ -> False
_ -> True
patVars :: Patt -> [Ident]
patVars p =
case p of
PV x -> [x]
PAs x p -> x:patVars p
_ -> collectPattOp patVars p
convType :: Term -> LinType
convType = ppT
where
ppT t =
@@ -315,9 +350,9 @@ convType = ppT
Sort k -> convSort k
-- EInt n -> tcon0 (identS ("({-"++show n++"-})")) -- type level numeric literal
FV (t:ts) -> ppT t -- !!
QC (m,n) -> ParamType (ParamTypeId ((gQId m n)))
Q (m,n) -> ParamType (ParamTypeId ((gQId m n)))
_ -> error $ "Missing case in convType for: "++show t
QC (m,n) -> ParamType (ParamTypeId (gQId m n))
Q (m,n) -> ParamType (ParamTypeId (gQId m n))
_ -> error $ "convType ppT: " ++ show t
convFields = map convField . filter (not.isLockLabel.fst)
convField (l,r) = RecordRow (lblId l) (ppT r)
@@ -326,15 +361,20 @@ convType = ppT
"Float" -> FloatType
"Int" -> IntType
"Str" -> StrType
_ -> error ("convSort "++show k)
_ -> error $ "convType convSort: " ++ show k
toParamType :: Term -> ParamType
toParamType t = case convType t of
ParamType pt -> pt
_ -> error ("toParamType "++show t)
_ -> error $ "toParamType: " ++ show t
toParamId :: Term -> ParamId
toParamId t = case toParamType t of
ParamTypeId p -> p
paramType :: G.Grammar
-> (ModuleName, Ident)
-> ((S.Set (ModuleName, Ident), S.Set QIdent), [ParamDef])
paramType gr q@(_,n) =
case lookupOrigInfo gr q of
Ok (m,ResParam (Just (L _ ps)) _)
@@ -342,7 +382,7 @@ paramType gr q@(_,n) =
((S.singleton (m,n),argTypes ps),
[ParamDef name (map (param m) ps)]
)
where name = (gQId m n)
where name = gQId m n
Ok (m,ResOper _ (Just (L _ t)))
| m==cPredef && n==cInts ->
((S.empty,S.empty),[]) {-
@@ -350,36 +390,46 @@ paramType gr q@(_,n) =
[Type (ConAp ((gQId m n)) [identS "n"]) (TId (identS "Int"))])-}
| otherwise ->
((S.singleton (m,n),paramTypes gr t),
[ParamAliasDef ((gQId m n)) (convType t)])
[ParamAliasDef (gQId m n) (convType t)])
_ -> ((S.empty,S.empty),[])
where
param m (n,ctx) = Param ((gQId m n)) [toParamId t|(_,_,t)<-ctx]
param m (n,ctx) = Param (gQId m n) [toParamId t|(_,_,t)<-ctx]
argTypes = S.unions . map argTypes1
argTypes1 (n,ctx) = S.unions [paramTypes gr t|(_,_,t)<-ctx]
lblId = LabelId . render -- hmm
modId (MN m) = ModId (showIdent m)
lblId :: Label -> C.LabelId
lblId (LIdent ri) = LabelId ri
lblId (LVar i) = LabelId (rawIdentS (show i)) -- hmm
class FromIdent i where gId :: Ident -> i
modId :: ModuleName -> C.ModId
modId (MN m) = ModId (ident2raw m)
class FromIdent i where
gId :: Ident -> i
instance FromIdent VarId where
gId i = if isWildIdent i then Anonymous else VarId (showIdent i)
gId i = if isWildIdent i then Anonymous else VarId (ident2raw i)
instance FromIdent C.FunId where gId = C.FunId . showIdent
instance FromIdent CatId where gId = CatId . showIdent
instance FromIdent C.FunId where gId = C.FunId . ident2raw
instance FromIdent CatId where gId = CatId . ident2raw
instance FromIdent ParamId where gId = ParamId . unqual
instance FromIdent VarValueId where gId = VarValueId . unqual
class FromIdent i => QualIdent i where gQId :: ModuleName -> Ident -> i
class FromIdent i => QualIdent i where
gQId :: ModuleName -> Ident -> i
instance QualIdent ParamId where gQId m n = ParamId (qual m n)
instance QualIdent ParamId where gQId m n = ParamId (qual m n)
instance QualIdent VarValueId where gQId m n = VarValueId (qual m n)
qual m n = Qual (modId m) (showIdent n)
unqual n = Unqual (showIdent n)
qual :: ModuleName -> Ident -> QualId
qual m n = Qual (modId m) (ident2raw n)
unqual :: Ident -> QualId
unqual n = Unqual (ident2raw n)
convFlags :: G.Grammar -> ModuleName -> Flags
convFlags gr mn =
Flags [(n,convLit v) |
Flags [(rawIdentS n,convLit v) |
(n,v)<-err (const []) (optionsPGF.mflags) (lookupModule gr mn)]
where
convLit l =

16
src/compiler/GF/Compile/Optimize.hs
View File

@@ -6,7 +6,7 @@
-- Stability : (stable)
-- Portability : (portable)
--
-- > CVS $Date: 2005/09/16 13:56:13 $
-- > CVS $Date: 2005/09/16 13:56:13 $
-- > CVS $Author: aarne $
-- > CVS $Revision: 1.18 $
--
@@ -21,7 +21,7 @@ import GF.Grammar.Printer
import GF.Grammar.Macros
import GF.Grammar.Lookup
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.Infra.Option
@@ -90,7 +90,7 @@ evalInfo opts resenv sgr m c info = do
let ppr' = fmap (evalPrintname resenv c) ppr
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
pde' <- case pde of
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))
mkLinReference :: SourceGrammar -> Type -> Err Term
mkLinReference gr typ =
liftM (Abs Explicit varStr) $
mkLinReference gr typ =
liftM (Abs Explicit varStr) $
case mkDefField typ (Vr varStr) of
Bad "no string" -> return Empty
x -> x
where
mkDefField ty trm =
mkDefField ty trm =
case ty of
Table pty ty -> do ps <- allParamValues gr pty
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]
_ -> composSafeOp (factor param c i) t
where
factors ty pvs0
factors ty pvs0
| not param = V ty (map snd pvs0)
factors ty [] = V ty []
factors ty pvs0@[(p,v)] = V ty [v]
@@ -224,7 +224,7 @@ factor param c i t =
replace :: Term -> Term -> Term -> Term
replace old new trm =
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
App _ _ | trm == old -> new
R _ | trm == old -> new

164
src/compiler/GF/Compile/PGFtoHaskell.hs
View File

@@ -5,7 +5,7 @@
-- Stability : (stable)
-- Portability : (portable)
--
-- > CVS $Date: 2005/06/17 12:39:07 $
-- > CVS $Date: 2005/06/17 12:39:07 $
-- > CVS $Author: bringert $
-- > CVS $Revision: 1.8 $
--
@@ -22,55 +22,66 @@ import PGF2.Internal
import GF.Data.Operations
import GF.Infra.Option
import Data.List
import Data.List(isPrefixOf,find,intercalate,intersperse,groupBy,sortBy)
import Data.Maybe(mapMaybe)
import qualified Data.Map as Map
type Prefix = String -> String
type DerivingClause = String
-- | the main function
grammar2haskell :: Options
-> String -- ^ Module name.
-> PGF
-> String
grammar2haskell opts name gr = foldr (++++) [] $
pragmas ++ haskPreamble gadt name ++ [types, gfinstances gId lexical gr'] ++ compos
grammar2haskell opts name gr = foldr (++++) [] $
pragmas ++ haskPreamble gadt name derivingClause (extraImports ++ pgfImports) ++
[types, gfinstances gId lexical gr'] ++ compos
where gr' = hSkeleton gr
gadt = haskellOption opts HaskellGADT
dataExt = haskellOption opts HaskellData
pgf2 = haskellOption opts HaskellPGF2
lexical cat = haskellOption opts HaskellLexical && isLexicalCat opts cat
gId | haskellOption opts HaskellNoPrefix = id
| otherwise = ("G"++)
pragmas | gadt = ["{-# OPTIONS_GHC -fglasgow-exts #-}"]
gId | haskellOption opts HaskellNoPrefix = rmForbiddenChars
| otherwise = ("G"++) . rmForbiddenChars
-- GF grammars allow weird identifier names inside '', e.g. 'VP/Object'
rmForbiddenChars = filter (`notElem` "'!#$%&*+./<=>?@\\^|-~")
pragmas | gadt = ["{-# LANGUAGE GADTs, FlexibleInstances, KindSignatures, RankNTypes, TypeSynonymInstances #-}"]
| dataExt = ["{-# LANGUAGE DeriveDataTypeable #-}"]
| otherwise = []
derivingClause
| dataExt = "deriving (Show,Data)"
| otherwise = "deriving Show"
extraImports | gadt = ["import Control.Monad.Identity", "import Data.Monoid"]
| dataExt = ["import Data.Data"]
| otherwise = []
pgfImports | pgf2 = ["import PGF2 hiding (Tree)", "", "showCId :: CId -> String", "showCId = id"]
| otherwise = ["import PGF hiding (Tree)"]
types | gadt = datatypesGADT gId lexical gr'
| otherwise = datatypes gId lexical gr'
| otherwise = datatypes gId derivingClause lexical gr'
compos | gadt = prCompos gId lexical gr' ++ composClass
| otherwise = []
haskPreamble gadt name =
haskPreamble :: Bool -> String -> String -> [String] -> [String]
haskPreamble gadt name derivingClause imports =
[
"module " ++ name ++ " where",
""
] ++
(if gadt then [
"import Control.Monad.Identity",
"import Data.Monoid"
] else []) ++
[
"import PGF hiding (Tree)",
] ++ imports ++ [
"",
"----------------------------------------------------",
"-- automatic translation from GF to Haskell",
"----------------------------------------------------",
"",
"",
"class Gf a where",
" gf :: a -> Expr",
" fg :: Expr -> a",
"",
predefInst gadt "GString" "String" "unStr" "mkStr",
predefInst gadt derivingClause "GString" "String" "unStr" "mkStr",
"",
predefInst gadt "GInt" "Int" "unInt" "mkInt",
predefInst gadt derivingClause "GInt" "Int" "unInt" "mkInt",
"",
predefInst gadt "GFloat" "Double" "unFloat" "mkFloat",
predefInst gadt derivingClause "GFloat" "Double" "unFloat" "mkFloat",
"",
"----------------------------------------------------",
"-- below this line machine-generated",
@@ -78,11 +89,12 @@ haskPreamble gadt name =
""
]
predefInst gadt gtyp typ destr consr =
predefInst :: Bool -> String -> String -> String -> String -> String -> String
predefInst gadt derivingClause gtyp typ destr consr =
(if gadt
then []
else ("newtype" +++ gtyp +++ "=" +++ gtyp +++ typ +++ " deriving Show\n\n")
)
then []
else "newtype" +++ gtyp +++ "=" +++ gtyp +++ typ +++ derivingClause ++ "\n\n"
)
++
"instance Gf" +++ gtyp +++ "where" ++++
" gf (" ++ gtyp +++ "x) =" +++ consr +++ "x" ++++
@@ -95,24 +107,24 @@ type OIdent = String
type HSkeleton = [(OIdent, [(OIdent, [OIdent])])]
datatypes :: Prefix -> (OIdent -> Bool) -> (String,HSkeleton) -> String
datatypes gId lexical = (foldr (+++++) "") . (filter (/="")) . (map (hDatatype gId lexical)) . snd
datatypes :: Prefix -> DerivingClause -> (OIdent -> Bool) -> (String,HSkeleton) -> String
datatypes gId derivingClause lexical = foldr (+++++) "" . filter (/="") . map (hDatatype gId derivingClause lexical) . snd
gfinstances :: Prefix -> (OIdent -> Bool) -> (String,HSkeleton) -> String
gfinstances gId lexical (m,g) = (foldr (+++++) "") $ (filter (/="")) $ (map (gfInstance gId lexical m)) g
gfinstances gId lexical (m,g) = foldr (+++++) "" $ filter (/="") $ map (gfInstance gId lexical m) g
hDatatype :: Prefix -> (OIdent -> Bool) -> (OIdent, [(OIdent, [OIdent])]) -> String
hDatatype _ _ ("Cn",_) = "" ---
hDatatype gId _ (cat,[]) = "data" +++ gId cat
hDatatype gId _ (cat,rules) | isListCat (cat,rules) =
"newtype" +++ gId cat +++ "=" +++ gId cat +++ "[" ++ gId (elemCat cat) ++ "]"
+++ "deriving Show"
hDatatype gId lexical (cat,rules) =
hDatatype :: Prefix -> DerivingClause -> (OIdent -> Bool) -> (OIdent, [(OIdent, [OIdent])]) -> String
hDatatype _ _ _ ("Cn",_) = "" ---
hDatatype gId _ _ (cat,[]) = "data" +++ gId cat
hDatatype gId derivingClause _ (cat,rules) | isListCat (cat,rules) =
"newtype" +++ gId cat +++ "=" +++ gId cat +++ "[" ++ gId (elemCat cat) ++ "]"
+++ derivingClause
hDatatype gId derivingClause lexical (cat,rules) =
"data" +++ gId cat +++ "=" ++
(if length rules == 1 then "" else "\n ") +++
foldr1 (\x y -> x ++ "\n |" +++ y) constructors ++++
" deriving Show"
" " +++ derivingClause
where
constructors = [gId f +++ foldr (+++) "" (map (gId) xx) | (f,xx) <- nonLexicalRules (lexical cat) rules]
++ if lexical cat then [lexicalConstructor cat +++ "String"] else []
@@ -124,16 +136,17 @@ nonLexicalRules True rules = [r | r@(f,t) <- rules, not (null t)]
lexicalConstructor :: OIdent -> String
lexicalConstructor cat = "Lex" ++ cat
predefTypeSkel :: HSkeleton
predefTypeSkel = [(c,[]) | c <- ["String", "Int", "Float"]]
-- GADT version of data types
datatypesGADT :: Prefix -> (OIdent -> Bool) -> (String,HSkeleton) -> String
datatypesGADT gId lexical (_,skel) = unlines $
datatypesGADT gId lexical (_,skel) = unlines $
concatMap (hCatTypeGADT gId) (skel ++ predefTypeSkel) ++
[
"",
[
"",
"data Tree :: * -> * where"
] ++
] ++
concatMap (map (" "++) . hDatatypeGADT gId lexical) skel ++
[
" GString :: String -> Tree GString_",
@@ -157,23 +170,23 @@ hCatTypeGADT gId (cat,rules)
"data"+++gId cat++"_"]
hDatatypeGADT :: Prefix -> (OIdent -> Bool) -> (OIdent, [(OIdent, [OIdent])]) -> [String]
hDatatypeGADT gId lexical (cat, rules)
hDatatypeGADT gId lexical (cat, rules)
| isListCat (cat,rules) = [gId cat+++"::"+++"["++gId (elemCat cat)++"]" +++ "->" +++ t]
| otherwise =
[ gId f +++ "::" +++ concatMap (\a -> gId a +++ "-> ") args ++ t
[ gId f +++ "::" +++ concatMap (\a -> gId a +++ "-> ") args ++ t
| (f,args) <- nonLexicalRules (lexical cat) rules ]
++ if lexical cat then [lexicalConstructor cat +++ ":: String ->"+++ t] else []
where t = "Tree" +++ gId cat ++ "_"
hEqGADT :: Prefix -> (OIdent -> Bool) -> (OIdent, [(OIdent, [OIdent])]) -> [String]
hEqGADT gId lexical (cat, rules)
| isListCat (cat,rules) = let r = listr cat in ["(" ++ patt "x" r ++ "," ++ patt "y" r ++ ") -> " ++ listeqs]
| isListCat (cat,rules) = let r = listr cat in ["(" ++ patt "x" r ++ "," ++ patt "y" r ++ ") -> " ++ listeqs]
| otherwise = ["(" ++ patt "x" r ++ "," ++ patt "y" r ++ ") -> " ++ eqs r | r <- nonLexicalRules (lexical cat) rules]
++ if lexical cat then ["(" ++ lexicalConstructor cat +++ "x" ++ "," ++ lexicalConstructor cat +++ "y" ++ ") -> x == y"] else []
where
patt s (f,xs) = unwords (gId f : mkSVars s (length xs))
eqs (_,xs) = unwords ("and" : "[" : intersperse "," [x ++ " == " ++ y |
eqs (_,xs) = unwords ("and" : "[" : intersperse "," [x ++ " == " ++ y |
(x,y) <- zip (mkSVars "x" (length xs)) (mkSVars "y" (length xs)) ] ++ ["]"])
listr c = (c,["foo"]) -- foo just for length = 1
listeqs = "and [x == y | (x,y) <- zip x1 y1]"
@@ -182,25 +195,26 @@ prCompos :: Prefix -> (OIdent -> Bool) -> (String,HSkeleton) -> [String]
prCompos gId lexical (_,catrules) =
["instance Compos Tree where",
" compos r a f t = case t of"]
++
++
[" " ++ prComposCons (gId f) xs | (c,rs) <- catrules, not (isListCat (c,rs)),
(f,xs) <- rs, not (null xs)]
++
(f,xs) <- rs, not (null xs)]
++
[" " ++ prComposCons (gId c) ["x1"] | (c,rs) <- catrules, isListCat (c,rs)]
++
++
[" _ -> r t"]
where
prComposCons f xs = let vs = mkVars (length xs) in
prComposCons f xs = let vs = mkVars (length xs) in
f +++ unwords vs +++ "->" +++ rhs f (zip vs xs)
rhs f vcs = "r" +++ f +++ unwords (map (prRec f) vcs)
prRec f (v,c)
prRec f (v,c)
| isList f = "`a` foldr (a . a (r (:)) . f) (r [])" +++ v
| otherwise = "`a`" +++ "f" +++ v
isList f = (gId "List") `isPrefixOf` f
isList f = gId "List" `isPrefixOf` f
gfInstance :: Prefix -> (OIdent -> Bool) -> String -> (OIdent, [(OIdent, [OIdent])]) -> String
gfInstance gId lexical m crs = hInstance gId lexical m crs ++++ fInstance gId lexical m crs
hInstance :: (String -> String) -> (String -> Bool) -> String -> (String, [(OIdent, [OIdent])]) -> String
----hInstance m ("Cn",_) = "" --- seems to belong to an old applic. AR 18/5/2004
hInstance gId _ m (cat,[]) = unlines [
"instance Show" +++ gId cat,
@@ -209,15 +223,15 @@ hInstance gId _ m (cat,[]) = unlines [
" gf _ = undefined",
" fg _ = undefined"
]
hInstance gId lexical m (cat,rules)
hInstance gId lexical m (cat,rules)
| isListCat (cat,rules) =
"instance Gf" +++ gId cat +++ "where" ++++
" gf (" ++ gId cat +++ "[" ++ concat (intersperse "," baseVars) ++ "])"
" gf (" ++ gId cat +++ "[" ++ intercalate "," baseVars ++ "])"
+++ "=" +++ mkRHS ("Base"++ec) baseVars ++++
" gf (" ++ gId cat +++ "(x:xs)) = "
++ mkRHS ("Cons"++ec) ["x",prParenth (gId cat+++"xs")]
" gf (" ++ gId cat +++ "(x:xs)) = "
++ mkRHS ("Cons"++ec) ["x",prParenth (gId cat+++"xs")]
-- no show for GADTs
-- ++++ " gf (" ++ gId cat +++ "xs) = error (\"Bad " ++ cat ++ " value: \" ++ show xs)"
-- ++++ " gf (" ++ gId cat +++ "xs) = error (\"Bad " ++ cat ++ " value: \" ++ show xs)"
| otherwise =
"instance Gf" +++ gId cat +++ "where\n" ++
unlines ([mkInst f xx | (f,xx) <- nonLexicalRules (lexical cat) rules]
@@ -226,19 +240,22 @@ hInstance gId lexical m (cat,rules)
ec = elemCat cat
baseVars = mkVars (baseSize (cat,rules))
mkInst f xx = let xx' = mkVars (length xx) in " gf " ++
(if length xx == 0 then gId f else prParenth (gId f +++ foldr1 (+++) xx')) +++
(if null xx then gId f else prParenth (gId f +++ foldr1 (+++) xx')) +++
"=" +++ mkRHS f xx'
mkRHS f vars = "mkApp (mkCId \"" ++ f ++ "\")" +++
"[" ++ prTList ", " ["gf" +++ x | x <- vars] ++ "]"
mkRHS f vars = "mkApp (mkCId \"" ++ f ++ "\")" +++
"[" ++ prTList ", " ["gf" +++ x | x <- vars] ++ "]"
mkVars :: Int -> [String]
mkVars = mkSVars "x"
mkSVars :: String -> Int -> [String]
mkSVars s n = [s ++ show i | i <- [1..n]]
----fInstance m ("Cn",_) = "" ---
fInstance _ _ m (cat,[]) = ""
fInstance gId lexical m (cat,rules) =
" fg t =" ++++
(if isList
(if isList
then " " ++ gId cat ++ " (fgs t) where\n fgs t = case unApp t of"
else " case unApp t of") ++++
unlines [mkInst f xx | (f,xx) <- nonLexicalRules (lexical cat) rules] ++++
@@ -250,15 +267,16 @@ fInstance gId lexical m (cat,rules) =
" Just (i," ++
"[" ++ prTList "," xx' ++ "])" +++
"| i == mkCId \"" ++ f ++ "\" ->" +++ mkRHS f xx'
where xx' = ["x" ++ show i | (_,i) <- zip xx [1..]]
mkRHS f vars
| isList =
if "Base" `isPrefixOf` f
then "[" ++ prTList ", " [ "fg" +++ x | x <- vars ] ++ "]"
else "fg" +++ (vars !! 0) +++ ":" +++ "fgs" +++ (vars !! 1)
| otherwise =
gId f +++
prTList " " [prParenth ("fg" +++ x) | x <- vars]
where
xx' = ["x" ++ show i | (_,i) <- zip xx [1..]]
mkRHS f vars
| isList =
if "Base" `isPrefixOf` f
then "[" ++ prTList ", " [ "fg" +++ x | x <- vars ] ++ "]"
else "fg" +++ (vars !! 0) +++ ":" +++ "fgs" +++ (vars !! 1)
| otherwise =
gId f +++
prTList " " [prParenth ("fg" +++ x) | x <- vars]
--type HSkeleton = [(OIdent, [(OIdent, [OIdent])])]
hSkeleton :: PGF -> (String,HSkeleton)
@@ -287,9 +305,10 @@ updateSkeleton cat skel rule =
-}
isListCat :: (OIdent, [(OIdent, [OIdent])]) -> Bool
isListCat (cat,rules) = "List" `isPrefixOf` cat && length rules == 2
&& ("Base"++c) `elem` fs && ("Cons"++c) `elem` fs
where c = elemCat cat
fs = map fst rules
&& ("Base"++c) `elem` fs && ("Cons"++c) `elem` fs
where
c = elemCat cat
fs = map fst rules
-- | Gets the element category of a list category.
elemCat :: OIdent -> OIdent
@@ -306,7 +325,7 @@ baseSize (_,rules) = length bs
where Just (_,bs) = find (("Base" `isPrefixOf`) . fst) rules
composClass :: [String]
composClass =
composClass =
[
"",
"class Compos t where",
@@ -333,4 +352,3 @@ composClass =
"",
"newtype C b a = C { unC :: b }"
]

50
src/compiler/GF/Compile/Rename.hs
View File

@@ -5,7 +5,7 @@
-- Stability : (stable)
-- Portability : (portable)
--
-- > CVS $Date: 2005/05/30 18:39:44 $
-- > CVS $Date: 2005/05/30 18:39:44 $
-- > CVS $Author: aarne $
-- > CVS $Revision: 1.19 $
--
@@ -23,9 +23,9 @@
-----------------------------------------------------------------------------
module GF.Compile.Rename (
renameSourceTerm,
renameModule
) where
renameSourceTerm,
renameModule
) where
import GF.Infra.Ident
import GF.Infra.CheckM
@@ -39,6 +39,7 @@ import GF.Data.Operations
import Control.Monad
import Data.List (nub,(\\))
import qualified Data.List as L
import qualified Data.Map as Map
import Data.Maybe(mapMaybe)
import GF.Text.Pretty
@@ -67,7 +68,7 @@ renameIdentTerm env = accumulateError (renameIdentTerm' env)
-- Fails immediately on error, makes it possible to try other possibilities
renameIdentTerm' :: Status -> Term -> Check Term
renameIdentTerm' env@(act,imps) t0 =
renameIdentTerm' env@(act,imps) t0 =
case t0 of
Vr c -> ident predefAbs c
Cn c -> ident (\_ s -> checkError s) c
@@ -84,8 +85,8 @@ renameIdentTerm' env@(act,imps) t0 =
_ -> return t0
where
opens = [st | (OSimple _,st) <- imps]
qualifs = [(m, st) | (OQualif m _, st) <- imps] ++
[(m, st) | (OQualif _ m, st) <- imps] ++
qualifs = [(m, st) | (OQualif m _, st) <- imps] ++
[(m, st) | (OQualif _ m, st) <- imps] ++
[(m, st) | (OSimple m, st) <- imps] -- qualif is always possible
-- this facility is mainly for BWC with GF1: you need not import PredefAbs
@@ -93,7 +94,7 @@ renameIdentTerm' env@(act,imps) t0 =
| isPredefCat c = return (Q (cPredefAbs,c))
| otherwise = checkError s
ident alt c =
ident alt c =
case Map.lookup c act of
Just f -> return (f c)
_ -> case mapMaybe (Map.lookup c) opens of
@@ -105,7 +106,26 @@ renameIdentTerm' env@(act,imps) t0 =
ts@(t:_) -> do checkWarn ("atomic term" <+> ppTerm Qualified 0 t0 $$
"conflict" <+> hsep (punctuate ',' (map (ppTerm Qualified 0) ts)) $$
"given" <+> fsep (punctuate ',' (map fst qualifs)))
return t
return (bestTerm ts) -- Heuristic for resource grammar. Returns t for all others.
where
-- Hotfix for https://github.com/GrammaticalFramework/gf-core/issues/56
-- Real bug is probably somewhere deeper in recognising excluded functions. /IL 2020-06-06
notFromCommonModule :: Term -> Bool
notFromCommonModule term =
let t = render $ ppTerm Qualified 0 term :: String
in not $ any (\moduleName -> moduleName `L.isPrefixOf` t)
["CommonX", "ConstructX", "ExtendFunctor"
,"MarkHTMLX", "ParamX", "TenseX", "TextX"]
-- If one of the terms comes from the common modules,
-- we choose the other one, because that's defined in the grammar.
bestTerm :: [Term] -> Term
bestTerm [] = error "constant not found" -- not reached: bestTerm is only called for case ts@(t:_)
bestTerm ts@(t:_) =
let notCommon = [t | t <- ts, notFromCommonModule t]
in case notCommon of
[] -> t -- All terms are from common modules, return first of original list
(u:_) -> u -- ≥1 terms are not from common modules, return first of those
info2status :: Maybe ModuleName -> Ident -> Info -> StatusInfo
info2status mq c i = case i of
@@ -137,7 +157,7 @@ modInfo2status (o,mo) = (o,tree2status o (jments mo))
self2status :: ModuleName -> ModuleInfo -> StatusMap
self2status c m = Map.mapWithKey (info2status (Just c)) (jments m)
renameInfo :: FilePath -> Status -> Module -> Ident -> Info -> Check Info
renameInfo cwd status (m,mi) i info =
case info of
@@ -188,7 +208,7 @@ renameTerm env vars = ren vars where
Abs b x t -> liftM (Abs b x) (ren (x:vs) t)
Prod bt x a b -> liftM2 (Prod bt x) (ren vs a) (ren (x:vs) b)
Typed a b -> liftM2 Typed (ren vs a) (ren vs b)
Vr x
Vr x
| elem x vs -> return trm
| otherwise -> renid trm
Cn _ -> renid trm
@@ -199,7 +219,7 @@ renameTerm env vars = ren vars where
i' <- case i of
TTyped ty -> liftM TTyped $ ren vs ty -- the only annotation in source
_ -> return i
liftM (T i') $ mapM (renCase vs) cs
liftM (T i') $ mapM (renCase vs) cs
Let (x,(m,a)) b -> do
m' <- case m of
@@ -209,7 +229,7 @@ renameTerm env vars = ren vars where
b' <- ren (x:vs) b
return $ Let (x,(m',a')) b'
P t@(Vr r) l -- Here we have $r.l$ and this is ambiguous it could be either
P t@(Vr r) l -- Here we have $r.l$ and this is ambiguous it could be either
-- record projection from variable or constant $r$ or qualified expression with module $r$
| elem r vs -> return trm -- try var proj first ..
| otherwise -> checks [ renid' (Q (MN r,label2ident l)) -- .. and qualified expression second.
@@ -236,7 +256,7 @@ renamePattern :: Status -> Patt -> Check (Patt,[Ident])
renamePattern env patt =
do r@(p',vs) <- renp patt
let dupl = vs \\ nub vs
unless (null dupl) $ checkError (hang ("[C.4.13] Pattern is not linear:") 4
unless (null dupl) $ checkError (hang ("[C.4.13] Pattern is not linear. All variable names on the left-hand side must be distinct.") 4
patt)
return r
where
@@ -311,7 +331,7 @@ renamePattern env patt =
renameContext :: Status -> Context -> Check Context
renameContext b = renc [] where
renc vs cont = case cont of
(bt,x,t) : xts
(bt,x,t) : xts
| isWildIdent x -> do
t' <- ren vs t
xts' <- renc vs xts

16
src/compiler/GF/Compile/TypeCheck/Abstract.hs
View File

@@ -5,7 +5,7 @@
-- Stability : (stable)
-- Portability : (portable)
--
-- > CVS $Date: 2005/09/15 16:22:02 $
-- > CVS $Date: 2005/09/15 16:22:02 $
-- > CVS $Author: aarne $
-- > CVS $Revision: 1.16 $
--
@@ -13,11 +13,11 @@
-----------------------------------------------------------------------------
module GF.Compile.TypeCheck.Abstract (-- * top-level type checking functions; TC should not be called directly.
checkContext,
checkTyp,
checkDef,
checkConstrs,
) where
checkContext,
checkTyp,
checkDef,
checkConstrs,
) where
import GF.Data.Operations
@@ -33,8 +33,8 @@ import GF.Text.Pretty
--import Control.Monad (foldM, liftM, liftM2)
-- | invariant way of creating TCEnv from context
initTCEnv gamma =
(length gamma,[(x,VGen i x) | ((x,_),i) <- zip gamma [0..]], gamma)
initTCEnv gamma =
(length gamma,[(x,VGen i x) | ((x,_),i) <- zip gamma [0..]], gamma)
-- interface to TC type checker

365
src/compiler/GF/Compile/TypeCheck/Concrete.hs
View File

@@ -1,6 +1,7 @@
{-# LANGUAGE PatternGuards #-}
module GF.Compile.TypeCheck.Concrete( {-checkLType, inferLType, computeLType, ppType-} ) where
{-
module GF.Compile.TypeCheck.Concrete( checkLType, inferLType, computeLType, ppType ) where
import Prelude hiding ((<>)) -- GHC 8.4.1 clash with Text.PrettyPrint
import GF.Infra.CheckM
import GF.Data.Operations
@@ -22,10 +23,16 @@ computeLType gr g0 t = comp (reverse [(b,x, Vr x) | (b,x,_) <- g0] ++ g0) t
_ | Just _ <- isTypeInts ty -> return ty ---- shouldn't be needed
| isPredefConstant ty -> return ty ---- shouldn't be needed
Q (m,ident) -> checkIn (text "module" <+> ppIdent m) $ do
Q (m,ident) -> checkIn ("module" <+> m) $ do
ty' <- lookupResDef gr (m,ident)
if ty' == ty then return ty else comp g ty' --- is this necessary to test?
AdHocOverload ts -> do
over <- getOverload gr g (Just typeType) t
case over of
Just (tr,_) -> return tr
_ -> checkError ("unresolved overloading of constants" <+> ppTerm Qualified 0 t)
Vr ident -> checkLookup ident g -- never needed to compute!
App f a -> do
@@ -62,7 +69,6 @@ computeLType gr g0 t = comp (reverse [(b,x, Vr x) | (b,x,_) <- g0] ++ g0) t
lockRecType c t' ---- locking to be removed AR 20/6/2009
_ | ty == typeTok -> return typeStr
_ | isPredefConstant ty -> return ty
_ -> composOp (comp g) ty
@@ -73,26 +79,26 @@ inferLType gr g trm = case trm of
Q (m,ident) | isPredef m -> termWith trm $ case typPredefined ident of
Just ty -> return ty
Nothing -> checkError (text "unknown in Predef:" <+> ppIdent ident)
Nothing -> checkError ("unknown in Predef:" <+> ident)
Q ident -> checks [
termWith trm $ lookupResType gr ident >>= computeLType gr g
,
lookupResDef gr ident >>= inferLType gr g
,
checkError (text "cannot infer type of constant" <+> ppTerm Unqualified 0 trm)
checkError ("cannot infer type of constant" <+> ppTerm Unqualified 0 trm)
]
QC (m,ident) | isPredef m -> termWith trm $ case typPredefined ident of
Just ty -> return ty
Nothing -> checkError (text "unknown in Predef:" <+> ppIdent ident)
Nothing -> checkError ("unknown in Predef:" <+> ident)
QC ident -> checks [
termWith trm $ lookupResType gr ident >>= computeLType gr g
,
lookupResDef gr ident >>= inferLType gr g
,
checkError (text "cannot infer type of canonical constant" <+> ppTerm Unqualified 0 trm)
checkError ("cannot infer type of canonical constant" <+> ppTerm Unqualified 0 trm)
]
Vr ident -> termWith trm $ checkLookup ident g
@@ -100,7 +106,12 @@ inferLType gr g trm = case trm of
Typed e t -> do
t' <- computeLType gr g t
checkLType gr g e t'
return (e,t')
AdHocOverload ts -> do
over <- getOverload gr g Nothing trm
case over of
Just trty -> return trty
_ -> checkError ("unresolved overloading of constants" <+> ppTerm Qualified 0 trm)
App f a -> do
over <- getOverload gr g Nothing trm
@@ -110,13 +121,17 @@ inferLType gr g trm = case trm of
(f',fty) <- inferLType gr g f
fty' <- computeLType gr g fty
case fty' of
Prod bt z arg val -> do
Prod bt z arg val -> do
a' <- justCheck g a arg
ty <- if isWildIdent z
ty <- if isWildIdent z
then return val
else substituteLType [(bt,z,a')] val
return (App f' a',ty)
_ -> checkError (text "A function type is expected for" <+> ppTerm Unqualified 0 f <+> text "instead of type" <+> ppType fty)
return (App f' a',ty)
_ ->
let term = ppTerm Unqualified 0 f
funName = pp . head . words .render $ term
in checkError ("A function type is expected for" <+> term <+> "instead of type" <+> ppType fty $$
"\n ** Maybe you gave too many arguments to" <+> funName <+> "\n")
S f x -> do
(f', fty) <- inferLType gr g f
@@ -124,7 +139,7 @@ inferLType gr g trm = case trm of
Table arg val -> do
x'<- justCheck g x arg
return (S f' x', val)
_ -> checkError (text "table lintype expected for the table in" $$ nest 2 (ppTerm Unqualified 0 trm))
_ -> checkError ("table lintype expected for the table in" $$ nest 2 (ppTerm Unqualified 0 trm))
P t i -> do
(t',ty) <- inferLType gr g t --- ??
@@ -132,16 +147,16 @@ inferLType gr g trm = case trm of
let tr2 = P t' i
termWith tr2 $ case ty' of
RecType ts -> case lookup i ts of
Nothing -> checkError (text "unknown label" <+> ppLabel i <+> text "in" $$ nest 2 (ppTerm Unqualified 0 ty'))
Nothing -> checkError ("unknown label" <+> i <+> "in" $$ nest 2 (ppTerm Unqualified 0 ty'))
Just x -> return x
_ -> checkError (text "record type expected for:" <+> ppTerm Unqualified 0 t $$
text " instead of the inferred:" <+> ppTerm Unqualified 0 ty')
_ -> checkError ("record type expected for:" <+> ppTerm Unqualified 0 t $$
" instead of the inferred:" <+> ppTerm Unqualified 0 ty')
R r -> do
let (ls,fs) = unzip r
fsts <- mapM inferM fs
let ts = [ty | (Just ty,_) <- fsts]
checkCond (text "cannot infer type of record" $$ nest 2 (ppTerm Unqualified 0 trm)) (length ts == length fsts)
checkCond ("cannot infer type of record" $$ nest 2 (ppTerm Unqualified 0 trm)) (length ts == length fsts)
return $ (R (zip ls fsts), RecType (zip ls ts))
T (TTyped arg) pts -> do
@@ -152,10 +167,10 @@ inferLType gr g trm = case trm of
checkLType gr g trm (Table arg val)
T ti pts -> do -- tries to guess: good in oper type inference
let pts' = [pt | pt@(p,_) <- pts, isConstPatt p]
case pts' of
[] -> checkError (text "cannot infer table type of" <+> ppTerm Unqualified 0 trm)
---- PInt k : _ -> return $ Ints $ max [i | PInt i <- pts']
_ -> do
case pts' of
[] -> checkError ("cannot infer table type of" <+> ppTerm Unqualified 0 trm)
---- PInt k : _ -> return $ Ints $ max [i | PInt i <- pts']
_ -> do
(arg,val) <- checks $ map (inferCase Nothing) pts'
checkLType gr g trm (Table arg val)
V arg pts -> do
@@ -166,9 +181,9 @@ inferLType gr g trm = case trm of
K s -> do
if elem ' ' s
then do
let ss = foldr C Empty (map K (words s))
let ss = foldr C Empty (map K (words s))
----- removed irritating warning AR 24/5/2008
----- checkWarn ("token \"" ++ s ++
----- checkWarn ("token \"" ++ s ++
----- "\" converted to token list" ++ prt ss)
return (ss, typeStr)
else return (trm, typeStr)
@@ -179,50 +194,56 @@ inferLType gr g trm = case trm of
Empty -> return (trm, typeStr)
C s1 s2 ->
C s1 s2 ->
check2 (flip (justCheck g) typeStr) C s1 s2 typeStr
Glue s1 s2 ->
Glue s1 s2 ->
check2 (flip (justCheck g) typeStr) Glue s1 s2 typeStr ---- typeTok
---- hack from Rename.identRenameTerm, to live with files with naming conflicts 18/6/2007
Strs (Cn c : ts) | c == cConflict -> do
checkWarn (text "unresolved constant, could be any of" <+> hcat (map (ppTerm Unqualified 0) ts))
checkWarn ("unresolved constant, could be any of" <+> hcat (map (ppTerm Unqualified 0) ts))
inferLType gr g (head ts)
Strs ts -> do
ts' <- mapM (\t -> justCheck g t typeStr) ts
ts' <- mapM (\t -> justCheck g t typeStr) ts
return (Strs ts', typeStrs)
Alts t aa -> do
t' <- justCheck g t typeStr
aa' <- flip mapM aa (\ (c,v) -> do
c' <- justCheck g c typeStr
c' <- justCheck g c typeStr
v' <- checks $ map (justCheck g v) [typeStrs, EPattType typeStr]
return (c',v'))
return (Alts t' aa', typeStr)
RecType r -> do
let (ls,ts) = unzip r
ts' <- mapM (flip (justCheck g) typeType) ts
ts' <- mapM (flip (justCheck g) typeType) ts
return (RecType (zip ls ts'), typeType)
ExtR r s -> do
(r',rT) <- inferLType gr g r
--- over <- getOverload gr g Nothing r
--- let r1 = maybe r fst over
let r1 = r ---
(r',rT) <- inferLType gr g r1
rT' <- computeLType gr g rT
(s',sT) <- inferLType gr g s
sT' <- computeLType gr g sT
let trm' = ExtR r' s'
---- trm' <- plusRecord r' s'
case (rT', sT') of
(RecType rs, RecType ss) -> do
rt <- plusRecType rT' sT'
let rt = RecType ([field | field@(l,_) <- rs, notElem l (map fst ss)] ++ ss) -- select types of later fields
checkLType gr g trm' rt ---- return (trm', rt)
_ | rT' == typeType && sT' == typeType -> return (trm', typeType)
_ -> checkError (text "records or record types expected in" <+> ppTerm Unqualified 0 trm)
_ | rT' == typeType && sT' == typeType -> do
return (trm', typeType)
_ -> checkError ("records or record types expected in" <+> ppTerm Unqualified 0 trm)
Sort _ ->
Sort _ ->
termWith trm $ return typeType
Prod bt x a b -> do
@@ -231,7 +252,7 @@ inferLType gr g trm = case trm of
return (Prod bt x a' b', typeType)
Table p t -> do
p' <- justCheck g p typeType --- check p partype!
p' <- justCheck g p typeType --- check p partype!
t' <- justCheck g t typeType
return $ (Table p' t', typeType)
@@ -250,9 +271,9 @@ inferLType gr g trm = case trm of
ELin c trm -> do
(trm',ty) <- inferLType gr g trm
ty' <- lockRecType c ty ---- lookup c; remove lock AR 20/6/2009
return $ (ELin c trm', ty')
return $ (ELin c trm', ty')
_ -> checkError (text "cannot infer lintype of" <+> ppTerm Unqualified 0 trm)
_ -> checkError ("cannot infer lintype of" <+> ppTerm Unqualified 0 trm)
where
isPredef m = elem m [cPredef,cPredefAbs]
@@ -299,7 +320,6 @@ inferLType gr g trm = case trm of
PChars _ -> return $ typeStr
_ -> inferLType gr g (patt2term p) >>= return . snd
-- type inference: Nothing, type checking: Just t
-- the latter permits matching with value type
getOverload :: SourceGrammar -> Context -> Maybe Type -> Term -> Check (Maybe (Term,Type))
@@ -310,15 +330,28 @@ getOverload gr g mt ot = case appForm ot of
v <- matchOverload f typs ttys
return $ Just v
_ -> return Nothing
(AdHocOverload cs@(f:_), ts) -> do --- the function name f is only used in error messages
let typs = concatMap collectOverloads cs
ttys <- mapM (inferLType gr g) ts
v <- matchOverload f typs ttys
return $ Just v
_ -> return Nothing
where
collectOverloads tr@(Q c) = case lookupOverload gr c of
Ok typs -> typs
_ -> case lookupResType gr c of
Ok ty -> let (args,val) = typeFormCnc ty in [(map (\(b,x,t) -> t) args,(val,tr))]
_ -> []
collectOverloads _ = [] --- constructors QC
matchOverload f typs ttys = do
let (tts,tys) = unzip ttys
let vfs = lookupOverloadInstance tys typs
let matches = [vf | vf@((_,v,_),_) <- vfs, matchVal mt v]
let showTypes ty = hsep (map ppType ty)
let (stys,styps) = (showTypes tys, [showTypes ty | (ty,_) <- typs])
-- to avoid strange error msg e.g. in case of unmatch record extension, show whole types if needed AR 28/1/2013
@@ -329,50 +362,57 @@ getOverload gr g mt ot = case appForm ot of
case ([vf | (vf,True) <- matches],[vf | (vf,False) <- matches]) of
([(_,val,fun)],_) -> return (mkApp fun tts, val)
([],[(pre,val,fun)]) -> do
checkWarn $ text "ignoring lock fields in resolving" <+> ppTerm Unqualified 0 ot $$
text "for" $$
checkWarn $ "ignoring lock fields in resolving" <+> ppTerm Unqualified 0 ot $$
"for" $$
nest 2 (showTypes tys) $$
text "using" $$
"using" $$
nest 2 (showTypes pre)
return (mkApp fun tts, val)
([],[]) -> do
checkError $ text "no overload instance of" <+> ppTerm Unqualified 0 f $$
text "for" $$
checkError $ "no overload instance of" <+> ppTerm Qualified 0 f $$
maybe empty (\x -> "with value type" <+> ppType x) mt $$
"for argument list" $$
nest 2 stysError $$
text "among" $$
nest 2 (vcat stypsError) $$
maybe empty (\x -> text "with value type" <+> ppType x) mt
"among alternatives" $$
nest 2 (vcat stypsError)
(vfs1,vfs2) -> case (noProds vfs1,noProds vfs2) of
([(val,fun)],_) -> do
return (mkApp fun tts, val)
([],[(val,fun)]) -> do
checkWarn (text "ignoring lock fields in resolving" <+> ppTerm Unqualified 0 ot)
checkWarn ("ignoring lock fields in resolving" <+> ppTerm Unqualified 0 ot)
return (mkApp fun tts, val)
----- unsafely exclude irritating warning AR 24/5/2008
----- checkWarn $ "overloading of" +++ prt f +++
----- checkWarn $ "overloading of" +++ prt f +++
----- "resolved by excluding partial applications:" ++++
----- unlines [prtType env ty | (ty,_) <- vfs', not (noProd ty)]
_ -> checkError $ text "ambiguous overloading of" <+> ppTerm Unqualified 0 f <+>
text "for" <+> hsep (map ppType tys) $$
text "with alternatives" $$
nest 2 (vcat [ppType ty | (_,ty,_) <- if null vfs1 then vfs2 else vfs2])
--- now forgiving ambiguity with a warning AR 1/2/2014
-- This gives ad hoc overloading the same behaviour as the choice of the first match in renaming did before.
-- But it also gives a chance to ambiguous overloadings that were banned before.
(nps1,nps2) -> do
checkWarn $ "ambiguous overloading of" <+> ppTerm Unqualified 0 f <+>
---- "with argument types" <+> hsep (map (ppTerm Qualified 0) tys) $$
"resolved by selecting the first of the alternatives" $$
nest 2 (vcat [ppTerm Qualified 0 fun | (_,ty,fun) <- vfs1 ++ if null vfs1 then vfs2 else []])
case [(mkApp fun tts,val) | (val,fun) <- nps1 ++ nps2] of
[] -> checkError $ "no alternatives left when resolving" <+> ppTerm Unqualified 0 f
h:_ -> return h
matchVal mt v = elem mt [Nothing,Just v,Just (unlocked v)]
unlocked v = case v of
RecType fs -> RecType $ filter (not . isLockLabel . fst) fs
RecType fs -> RecType $ filter (not . isLockLabel . fst) (sortRec fs)
_ -> v
---- TODO: accept subtypes
---- TODO: use a trie
lookupOverloadInstance tys typs =
[((pre,mkFunType rest val, t),isExact) |
lookupOverloadInstance tys typs =
[((pre,mkFunType rest val, t),isExact) |
let lt = length tys,
(ty,(val,t)) <- typs, length ty >= lt,
let (pre,rest) = splitAt lt ty,
let (pre,rest) = splitAt lt ty,
let isExact = pre == tys,
isExact || map unlocked pre == map unlocked tys
]
@@ -385,20 +425,21 @@ getOverload gr g mt ot = case appForm ot of
checkLType :: SourceGrammar -> Context -> Term -> Type -> Check (Term, Type)
checkLType gr g trm typ0 = do
typ <- computeLType gr g typ0
case trm of
Abs bt x c -> do
case typ of
Prod bt' z a b -> do
Prod bt' z a b -> do
(c',b') <- if isWildIdent z
then checkLType gr ((bt,x,a):g) c b
else do b' <- checkIn (text "abs") $ substituteLType [(bt',z,Vr x)] b
else do b' <- checkIn (pp "abs") $ substituteLType [(bt',z,Vr x)] b
checkLType gr ((bt,x,a):g) c b'
return $ (Abs bt x c', Prod bt' x a b')
_ -> checkError $ text "function type expected instead of" <+> ppType typ
return $ (Abs bt x c', Prod bt' z a b')
_ -> checkError $ "function type expected instead of" <+> ppType typ $$
"\n ** Double-check that the type signature of the operation" $$
"matches the number of arguments given to it.\n"
App f a -> do
over <- getOverload gr g (Just typ) trm
@@ -408,6 +449,12 @@ checkLType gr g trm typ0 = do
(trm',ty') <- inferLType gr g trm
termWith trm' $ checkEqLType gr g typ ty' trm'
AdHocOverload ts -> do
over <- getOverload gr g Nothing trm
case over of
Just trty -> return trty
_ -> checkError ("unresolved overloading of constants" <+> ppTerm Qualified 0 trm)
Q _ -> do
over <- getOverload gr g (Just typ) trm
case over of
@@ -417,21 +464,21 @@ checkLType gr g trm typ0 = do
termWith trm' $ checkEqLType gr g typ ty' trm'
T _ [] ->
checkError (text "found empty table in type" <+> ppTerm Unqualified 0 typ)
T _ cs -> case typ of
Table arg val -> do
checkError ("found empty table in type" <+> ppTerm Unqualified 0 typ)
T _ cs -> case typ of
Table arg val -> do
case allParamValues gr arg of
Ok vs -> do
let ps0 = map fst cs
ps <- testOvershadow ps0 vs
if null ps
then return ()
else checkWarn (text "patterns never reached:" $$
if null ps
then return ()
else checkWarn ("patterns never reached:" $$
nest 2 (vcat (map (ppPatt Unqualified 0) ps)))
_ -> return () -- happens with variable types
cs' <- mapM (checkCase arg val) cs
return (T (TTyped arg) cs', typ)
_ -> checkError $ text "table type expected for table instead of" $$ nest 2 (ppType typ)
_ -> checkError $ "table type expected for table instead of" $$ nest 2 (ppType typ)
V arg0 vs ->
case typ of
Table arg1 val ->
@@ -439,51 +486,54 @@ checkLType gr g trm typ0 = do
vs1 <- allParamValues gr arg1
if length vs1 == length vs
then return ()
else checkError $ text "wrong number of values in table" <+> ppTerm Unqualified 0 trm
else checkError $ "wrong number of values in table" <+> ppTerm Unqualified 0 trm
vs' <- map fst `fmap` sequence [checkLType gr g v val|v<-vs]
return (V arg' vs',typ)
R r -> case typ of --- why needed? because inference may be too difficult
RecType rr -> do
let (ls,_) = unzip rr -- labels of expected type
--let (ls,_) = unzip rr -- labels of expected type
fsts <- mapM (checkM r) rr -- check that they are found in the record
return $ (R fsts, typ) -- normalize record
_ -> checkError (text "record type expected in type checking instead of" $$ nest 2 (ppTerm Unqualified 0 typ))
_ -> checkError ("record type expected in type checking instead of" $$ nest 2 (ppTerm Unqualified 0 typ))
ExtR r s -> case typ of
_ | typ == typeType -> do
trm' <- computeLType gr g trm
case trm' of
RecType _ -> termWith trm $ return typeType
ExtR (Vr _) (RecType _) -> termWith trm $ return typeType
RecType _ -> termWith trm' $ return typeType
ExtR (Vr _) (RecType _) -> termWith trm' $ return typeType
-- ext t = t ** ...
_ -> checkError (text "invalid record type extension" <+> nest 2 (ppTerm Unqualified 0 trm))
_ -> checkError ("invalid record type extension" <+> nest 2 (ppTerm Unqualified 0 trm))
RecType rr -> do
(r',ty,s') <- checks [
do (r',ty) <- inferLType gr g r
return (r',ty,s)
,
do (s',ty) <- inferLType gr g s
return (s',ty,r)
]
case ty of
RecType rr1 -> do
let (rr0,rr2) = recParts rr rr1
r2 <- justCheck g r' rr0
s2 <- justCheck g s' rr2
return $ (ExtR r2 s2, typ)
_ -> checkError (text "record type expected in extension of" <+> ppTerm Unqualified 0 r $$
text "but found" <+> ppTerm Unqualified 0 ty)
ll2 <- case s of
R ss -> return $ map fst ss
_ -> do
(s',typ2) <- inferLType gr g s
case typ2 of
RecType ss -> return $ map fst ss
_ -> checkError ("cannot get labels from" $$ nest 2 (ppTerm Unqualified 0 typ2))
let ll1 = [l | (l,_) <- rr, notElem l ll2]
--- over <- getOverload gr g Nothing r --- this would solve #66 but fail ParadigmsAra. AR 6/7/2020
--- let r1 = maybe r fst over
let r1 = r ---
(r',_) <- checkLType gr g r1 (RecType [field | field@(l,_) <- rr, elem l ll1])
(s',_) <- checkLType gr g s (RecType [field | field@(l,_) <- rr, elem l ll2])
let rec = R ([(l,(Nothing,P r' l)) | l <- ll1] ++ [(l,(Nothing,P s' l)) | l <- ll2])
return (rec, typ)
ExtR ty ex -> do
r' <- justCheck g r ty
s' <- justCheck g s ex
return $ (ExtR r' s', typ) --- is this all? it assumes the same division in trm and typ
_ -> checkError (text "record extension not meaningful for" <+> ppTerm Unqualified 0 typ)
_ -> checkError ("record extension not meaningful for" <+> ppTerm Unqualified 0 typ)
FV vs -> do
ttys <- mapM (flip (checkLType gr g) typ) vs
@@ -498,7 +548,7 @@ checkLType gr g trm typ0 = do
(arg',val) <- checkLType gr g arg p
checkEqLType gr g typ t trm
return (S tab' arg', t)
_ -> checkError (text "table type expected for applied table instead of" <+> ppType ty')
_ -> checkError ("table type expected for applied table instead of" <+> ppType ty')
, do
(arg',ty) <- inferLType gr g arg
ty' <- computeLType gr g ty
@@ -507,7 +557,8 @@ checkLType gr g trm typ0 = do
]
Let (x,(mty,def)) body -> case mty of
Just ty -> do
(def',ty') <- checkLType gr g def ty
(ty0,_) <- checkLType gr g ty typeType
(def',ty') <- checkLType gr g def ty0
body' <- justCheck ((Explicit,x,ty'):g) body typ
return (Let (x,(Just ty',def')) body', typ)
_ -> do
@@ -523,10 +574,10 @@ checkLType gr g trm typ0 = do
termWith trm' $ checkEqLType gr g typ ty' trm'
where
justCheck g ty te = checkLType gr g ty te >>= return . fst
recParts rr t = (RecType rr1,RecType rr2) where
(rr1,rr2) = partition (flip elem (map fst t) . fst) rr
{-
recParts rr t = (RecType rr1,RecType rr2) where
(rr1,rr2) = partition (flip elem (map fst t) . fst) rr
-}
checkM rms (l,ty) = case lookup l rms of
Just (Just ty0,t) -> do
checkEqLType gr g ty ty0 t
@@ -535,12 +586,12 @@ checkLType gr g trm typ0 = do
Just (_,t) -> do
(t',ty') <- checkLType gr g t ty
return (l,(Just ty',t'))
_ -> checkError $
if isLockLabel l
_ -> checkError $
if isLockLabel l
then let cat = drop 5 (showIdent (label2ident l))
in ppTerm Unqualified 0 (R rms) <+> text "is not in the lincat of" <+> text cat <>
text "; try wrapping it with lin" <+> text cat
else text "cannot find value for label" <+> ppLabel l <+> text "in" <+> ppTerm Unqualified 0 (R rms)
in ppTerm Unqualified 0 (R rms) <+> "is not in the lincat of" <+> cat <>
"; try wrapping it with lin" <+> cat
else "cannot find value for label" <+> l <+> "in" <+> ppTerm Unqualified 0 (R rms)
checkCase arg val (p,t) = do
cont <- pattContext gr g arg p
@@ -553,7 +604,7 @@ pattContext env g typ p = case p of
PP (q,c) ps | q /= cPredef -> do ---- why this /=? AR 6/1/2006
t <- lookupResType env (q,c)
let (cont,v) = typeFormCnc t
checkCond (text "wrong number of arguments for constructor in" <+> ppPatt Unqualified 0 p)
checkCond ("wrong number of arguments for constructor in" <+> ppPatt Unqualified 0 p)
(length cont == length ps)
checkEqLType env g typ v (patt2term p)
mapM (\((_,_,ty),p) -> pattContext env g ty p) (zip cont ps) >>= return . concat
@@ -564,7 +615,7 @@ pattContext env g typ p = case p of
let pts = [(ty,tr) | (l,tr) <- r, Just ty <- [lookup l t]]
----- checkWarn $ prt p ++++ show pts ----- debug
mapM (uncurry (pattContext env g)) pts >>= return . concat
_ -> checkError (text "record type expected for pattern instead of" <+> ppTerm Unqualified 0 typ')
_ -> checkError ("record type expected for pattern instead of" <+> ppTerm Unqualified 0 typ')
PT t p' -> do
checkEqLType env g typ t (patt2term p')
pattContext env g typ p'
@@ -577,10 +628,10 @@ pattContext env g typ p = case p of
g1 <- pattContext env g typ p'
g2 <- pattContext env g typ q
let pts = nub ([x | pt@(_,x,_) <- g1, notElem pt g2] ++ [x | pt@(_,x,_) <- g2, notElem pt g1])
checkCond
(text "incompatible bindings of" <+>
fsep (map ppIdent pts) <+>
text "in pattern alterantives" <+> ppPatt Unqualified 0 p) (null pts)
checkCond
("incompatible bindings of" <+>
fsep pts <+>
"in pattern alterantives" <+> ppPatt Unqualified 0 p) (null pts)
return g1 -- must be g1 == g2
PSeq p q -> do
g1 <- pattContext env g typ p
@@ -590,11 +641,11 @@ pattContext env g typ p = case p of
PNeg p' -> noBind typ p'
_ -> return [] ---- check types!
where
where
noBind typ p' = do
co <- pattContext env g typ p'
if not (null co)
then checkWarn (text "no variable bound inside pattern" <+> ppPatt Unqualified 0 p)
then checkWarn ("no variable bound inside pattern" <+> ppPatt Unqualified 0 p)
>> return []
else return []
@@ -603,9 +654,31 @@ checkEqLType gr g t u trm = do
(b,t',u',s) <- checkIfEqLType gr g t u trm
case b of
True -> return t'
False -> checkError $ text s <+> text "type of" <+> ppTerm Unqualified 0 trm $$
text "expected:" <+> ppType t $$
text "inferred:" <+> ppType u
False ->
let inferredType = ppTerm Qualified 0 u
expectedType = ppTerm Qualified 0 t
term = ppTerm Unqualified 0 trm
funName = pp . head . words .render $ term
helpfulMsg =
case (arrows inferredType, arrows expectedType) of
(0,0) -> pp "" -- None of the types is a function
_ -> "\n **" <+>
if expectedType `isLessApplied` inferredType
then "Maybe you gave too few arguments to" <+> funName
else pp "Double-check that type signature and number of arguments match."
in checkError $ s <+> "type of" <+> term $$
"expected:" <+> expectedType $$ -- ppqType t u $$
"inferred:" <+> inferredType $$ -- ppqType u t
helpfulMsg
where
-- count the number of arrows in the prettyprinted term
arrows :: Doc -> Int
arrows = length . filter (=="->") . words . render
-- If prettyprinted type t has fewer arrows then prettyprinted type u,
-- then t is "less applied", and we can print out more helpful error msg.
isLessApplied :: Doc -> Doc -> Bool
isLessApplied t u = arrows t < arrows u
checkIfEqLType :: SourceGrammar -> Context -> Type -> Type -> Term -> Check (Bool,Type,Type,String)
checkIfEqLType gr g t u trm = do
@@ -617,60 +690,62 @@ checkIfEqLType gr g t u trm = do
--- better: use a flag to forgive? (AR 31/1/2006)
_ -> case missingLock [] t' u' of
Ok lo -> do
checkWarn $ text "missing lock field" <+> fsep (map ppLabel lo)
checkWarn $ "missing lock field" <+> fsep lo
return (True,t',u',[])
Bad s -> return (False,t',u',s)
where
-- t is a subtype of u
-- check that u is a subtype of t
--- quick hack version of TC.eqVal
alpha g t u = case (t,u) of
alpha g t u = case (t,u) of
-- error (the empty type!) is subtype of any other type
(_,u) | u == typeError -> True
-- contravariance
(Prod _ x a b, Prod _ y c d) -> alpha g c a && alpha ((x,y):g) b d
(Prod _ x a b, Prod _ y c d) -> alpha g c a && alpha ((x,y):g) b d
-- record subtyping
(RecType rs, RecType ts) -> all (\ (l,a) ->
any (\ (k,b) -> alpha g a b && l == k) ts) rs
(RecType rs, RecType ts) -> all (\ (l,a) ->
any (\ (k,b) -> l == k && alpha g a b) ts) rs
(ExtR r s, ExtR r' s') -> alpha g r r' && alpha g s s'
(ExtR r s, t) -> alpha g r t || alpha g s t
-- the following say that Ints n is a subset of Int and of Ints m >= n
(t,u) | Just m <- isTypeInts t, Just n <- isTypeInts t -> m >= n
-- But why does it also allow Int as a subtype of Ints m? /TH 2014-04-04
(t,u) | Just m <- isTypeInts t, Just n <- isTypeInts u -> m >= n
| Just _ <- isTypeInts t, u == typeInt -> True ---- check size!
| t == typeInt, Just _ <- isTypeInts u -> True ---- why this ???? AR 11/12/2005
---- this should be made in Rename
(Q (m,a), Q (n,b)) | a == b -> elem m (allExtendsPlus gr n)
(Q (m,a), Q (n,b)) | a == b -> elem m (allExtendsPlus gr n)
|| elem n (allExtendsPlus gr m)
|| m == n --- for Predef
(QC (m,a), QC (n,b)) | a == b -> elem m (allExtendsPlus gr n)
(QC (m,a), QC (n,b)) | a == b -> elem m (allExtendsPlus gr n)
|| elem n (allExtendsPlus gr m)
(QC (m,a), Q (n,b)) | a == b -> elem m (allExtendsPlus gr n)
(QC (m,a), Q (n,b)) | a == b -> elem m (allExtendsPlus gr n)
|| elem n (allExtendsPlus gr m)
(Q (m,a), QC (n,b)) | a == b -> elem m (allExtendsPlus gr n)
(Q (m,a), QC (n,b)) | a == b -> elem m (allExtendsPlus gr n)
|| elem n (allExtendsPlus gr m)
(Table a b, Table c d) -> alpha g a c && alpha g b d
-- contravariance
(Table a b, Table c d) -> alpha g c a && alpha g b d
(Vr x, Vr y) -> x == y || elem (x,y) g || elem (y,x) g
_ -> t == u
_ -> t == u
--- the following should be one-way coercions only. AR 4/1/2001
|| elem t sTypes && elem u sTypes
|| (t == typeType && u == typePType)
|| (u == typeType && t == typePType)
|| (t == typeType && u == typePType)
|| (u == typeType && t == typePType)
missingLock g t u = case (t,u) of
(RecType rs, RecType ts) ->
let
ls = [l | (l,a) <- rs,
missingLock g t u = case (t,u) of
(RecType rs, RecType ts) ->
let
ls = [l | (l,a) <- rs,
not (any (\ (k,b) -> alpha g a b && l == k) ts)]
(locks,others) = partition isLockLabel ls
in case others of
_:_ -> Bad $ render (text "missing record fields:" <+> fsep (punctuate comma (map ppLabel others)))
_:_ -> Bad $ render ("missing record fields:" <+> fsep (punctuate ',' (others)))
_ -> return locks
-- contravariance
(Prod _ x a b, Prod _ y c d) -> do
@@ -696,7 +771,7 @@ termWith t ct = do
return (t,ty)
-- | compositional check\/infer of binary operations
check2 :: (Term -> Check Term) -> (Term -> Term -> Term) ->
check2 :: (Term -> Check Term) -> (Term -> Term -> Term) ->
Term -> Term -> Type -> Check (Term,Type)
check2 chk con a b t = do
a' <- chk a
@@ -708,14 +783,18 @@ ppType :: Type -> Doc
ppType ty =
case ty of
RecType fs -> case filter isLockLabel $ map fst fs of
[lock] -> text (drop 5 (showIdent (label2ident lock)))
[lock] -> pp (drop 5 (showIdent (label2ident lock)))
_ -> ppTerm Unqualified 0 ty
Prod _ x a b -> ppType a <+> text "->" <+> ppType b
Prod _ x a b -> ppType a <+> "->" <+> ppType b
_ -> ppTerm Unqualified 0 ty
{-
ppqType :: Type -> Type -> Doc
ppqType t u = case (ppType t, ppType u) of
(pt,pu) | render pt == render pu -> ppTerm Qualified 0 t
(pt,_) -> pt
-}
checkLookup :: Ident -> Context -> Check Type
checkLookup x g =
case [ty | (b,y,ty) <- g, x == y] of
[] -> checkError (text "unknown variable" <+> ppIdent x)
[] -> checkError ("unknown variable" <+> x)
(ty:_) -> return ty
-}

76
src/compiler/GF/Compile/TypeCheck/ConcreteNew.hs
View File

@@ -1,3 +1,4 @@
{-# LANGUAGE CPP #-}
module GF.Compile.TypeCheck.ConcreteNew( checkLType, inferLType ) where
-- The code here is based on the paper:
@@ -9,7 +10,7 @@ import GF.Grammar hiding (Env, VGen, VApp, VRecType)
import GF.Grammar.Lookup
import GF.Grammar.Predef
import GF.Grammar.Lockfield
import GF.Compile.Compute.ConcreteNew
import GF.Compile.Compute.Concrete
import GF.Compile.Compute.Predef(predef,predefName)
import GF.Infra.CheckM
import GF.Data.Operations
@@ -19,6 +20,7 @@ import GF.Text.Pretty
import Data.List (nub, (\\), tails)
import qualified Data.IntMap as IntMap
import Data.Maybe(fromMaybe,isNothing)
import qualified Control.Monad.Fail as Fail
checkLType :: GlobalEnv -> Term -> Type -> Check (Term, Type)
checkLType ge t ty = runTcM $ do
@@ -131,7 +133,7 @@ tcRho ge scope t@(RecType rs) (Just ty) = do
[] -> unifyVar ge scope i env vs vtypePType
_ -> return ()
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)
(rs,mb_ty) <- tcRecTypeFields ge scope rs (Just ty')
return (f (RecType rs),ty)
@@ -185,7 +187,7 @@ tcRho ge scope (R rs) (Just ty) = do
case ty' of
(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
return ((f . R) rs,
return ((f . R) rs,
VRecType [(l, ty) | (l,t,ty) <- lttys]
)
ty -> do lttys <- inferRecFields ge scope rs
@@ -275,11 +277,11 @@ tcApp ge scope (App fun arg) = -- APP2
varg <- liftErr (eval ge (scopeEnv scope) arg)
return (App fun arg, res_ty varg)
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)
return (t,ty)
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)
return (t,ty)
tcApp ge scope t =
@@ -348,7 +350,7 @@ tcPatt ge scope (PM q) ty0 = do
Bad err -> tcError (pp err)
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
checkRecFields ge scope [] ltys
@@ -366,7 +368,7 @@ checkRecFields ge scope ((l,t):lts) ltys =
where
takeIt l1 [] = (Nothing, [])
takeIt l1 (lty@(l2,ty):ltys)
| l1 == l2 = (Just ty,ltys)
| l1 == l2 = (Just ty,ltys)
| otherwise = let (mb_ty,ltys') = takeIt l1 ltys
in (mb_ty,lty:ltys')
@@ -388,13 +390,13 @@ tcRecTypeFields ge scope ((l,ty):rs) mb_ty = do
| s == cPType -> return mb_ty
VMeta _ _ _ -> return mb_ty
_ -> 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)
(rs,mb_ty) <- tcRecTypeFields ge scope rs mb_ty
return ((l,ty):rs,mb_ty)
-- | Invariant: if the third argument is (Just rho),
-- then rho is in weak-prenex form
-- then rho is in weak-prenex form
instSigma :: GlobalEnv -> Scope -> Term -> Sigma -> Maybe Rho -> TcM (Term, Rho)
instSigma ge scope t ty1 Nothing = return (t,ty1) -- INST1
instSigma ge scope t ty1 (Just ty2) = do -- INST2
@@ -442,11 +444,11 @@ subsCheckRho ge scope t (VApp p1 _) (VApp p2 _) -- Rule
| predefName p1 == cInts && predefName p2 == cInt = return t
subsCheckRho ge scope t (VApp p1 [VInt i]) (VApp p2 [VInt j]) -- Rule INT2
| predefName p1 == cInts && predefName p2 == cInts =
if i <= j
if i <= j
then return t
else tcError ("Ints" <+> i <+> "is not a subtype of" <+> "Ints" <+> j)
subsCheckRho ge scope t ty1@(VRecType rs1) ty2@(VRecType rs2) = do -- Rule REC
let mkAccess scope t =
let mkAccess scope t =
case t of
ExtR t1 t2 -> do (scope,mkProj1,mkWrap1) <- mkAccess scope t1
(scope,mkProj2,mkWrap2) <- mkAccess scope t2
@@ -555,7 +557,7 @@ unify ge scope v (VMeta i env vs) = unifyVar ge scope i env vs v
unify ge scope v1 v2 = do
t1 <- zonkTerm =<< tc_value2term (geLoc ge) (scopeVars scope) v1
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))
-- | Invariant: tv1 is a flexible type variable
@@ -566,9 +568,9 @@ unifyVar ge scope i env vs ty2 = do -- Check whether i is bound
Bound ty1 -> do v <- liftErr (eval ge env ty1)
unify ge scope (vapply (geLoc ge) v vs) ty2
Unbound scope' _ -> case value2term (geLoc ge) (scopeVars scope') ty2 of
Left i -> let (v,_) = reverse scope !! i
in tcError ("Variable" <+> pp v <+> "has escaped")
Right ty2' -> do ms2 <- getMetaVars (geLoc ge) [(scope,ty2)]
-- Left i -> let (v,_) = reverse scope !! i
-- in tcError ("Variable" <+> pp v <+> "has escaped")
ty2' -> do ms2 <- getMetaVars (geLoc ge) [(scope,ty2)]
if i `elem` ms2
then tcError ("Occurs check for" <+> ppMeta i <+> "in:" $$
nest 2 (ppTerm Unqualified 0 ty2'))
@@ -607,7 +609,7 @@ quantify ge scope t tvs ty0 = do
ty <- tc_value2term (geLoc ge) (scopeVars scope) ty0
let used_bndrs = nub (bndrs ty) -- Avoid quantified type variables in use
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
vty <- liftErr (eval ge [] (foldr (\v ty -> Prod Implicit v typeType ty) ty new_bndrs))
return (foldr (Abs Implicit) t new_bndrs,vty)
@@ -617,7 +619,7 @@ quantify ge scope t tvs ty0 = do
bndrs (Prod _ x t1 t2) = [x] ++ bndrs t1 ++ bndrs t2
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'] ] ++
[ identS (x : show i) | i <- [1 :: Integer ..], x <- ['a'..'z']]
@@ -629,8 +631,8 @@ allBinders = [ identS [x] | x <- ['a'..'z'] ] ++
type Scope = [(Ident,Value)]
type Sigma = Value
type Rho = Value -- No top-level ForAll
type Tau = Value -- No ForAlls anywhere
type Rho = Value -- No top-level ForAll
type Tau = Value -- No ForAlls anywhere
data MetaValue
= Unbound Scope Sigma
@@ -646,8 +648,16 @@ instance Monad TcM where
f >>= g = TcM (\ms msgs -> case unTcM f ms msgs of
TcOk x ms msgs -> unTcM (g x) ms msgs
TcFail msgs -> TcFail msgs)
#if !(MIN_VERSION_base(4,13,0))
-- Monad(fail) will be removed in GHC 8.8+
fail = Fail.fail
#endif
instance Fail.MonadFail TcM where
fail = tcError . pp
instance Applicative TcM where
pure = return
(<*>) = ap
@@ -678,12 +688,12 @@ runTcM f = case unTcM f IntMap.empty [] of
TcFail (msg:msgs) -> do checkWarnings msgs; checkError msg
newMeta :: Scope -> Sigma -> TcM MetaId
newMeta scope ty = TcM (\ms msgs ->
newMeta scope ty = TcM (\ms msgs ->
let i = IntMap.size ms
in TcOk i (IntMap.insert i (Unbound scope ty) ms) msgs)
getMeta :: MetaId -> TcM MetaValue
getMeta i = TcM (\ms msgs ->
getMeta i = TcM (\ms msgs ->
case IntMap.lookup i ms of
Just mv -> TcOk mv ms msgs
Nothing -> TcFail (("Unknown metavariable" <+> ppMeta i) : msgs))
@@ -692,7 +702,7 @@ setMeta :: MetaId -> MetaValue -> TcM ()
setMeta i mv = TcM (\ms msgs -> TcOk () (IntMap.insert i mv ms) msgs)
newVar :: Scope -> Ident
newVar scope = head [x | i <- [1..],
newVar scope = head [x | i <- [1..],
let x = identS ('v':show i),
isFree scope x]
where
@@ -711,11 +721,11 @@ getMetaVars loc sc_tys = do
return (foldr go [] tys)
where
-- 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 (Meta i) acc
| i `elem` acc = acc
| otherwise = i : acc
| i `elem` acc = acc
| otherwise = i : acc
go (Q _) acc = acc
go (QC _) acc = acc
go (Sort _) acc = acc
@@ -731,10 +741,10 @@ getFreeVars loc sc_tys = do
tys <- mapM (\(scope,ty) -> zonkTerm =<< tc_value2term loc (scopeVars scope) ty) sc_tys
return (foldr (go []) [] tys)
where
go bound (Vr tv) acc
| tv `elem` bound = acc
| tv `elem` acc = acc
| otherwise = tv : acc
go bound (Vr tv) acc
| tv `elem` bound = acc
| tv `elem` acc = acc
| otherwise = tv : acc
go bound (App x y) acc = go bound x (go bound y acc)
go bound (Meta _) acc = acc
go bound (Q _) acc = acc
@@ -755,13 +765,13 @@ zonkTerm (Meta i) = do
zonkTerm t = composOp zonkTerm t
tc_value2term loc xs v =
case value2term loc xs v of
Left i -> tcError ("Variable #" <+> pp i <+> "has escaped")
Right t -> return t
return $ value2term loc xs v
-- Old value2term error message:
-- Left i -> tcError ("Variable #" <+> pp i <+> "has escaped")
data TcA x a
data TcA x a
= TcSingle (MetaStore -> [Message] -> TcResult a)
| TcMany [x] (MetaStore -> [Message] -> [(a,MetaStore,[Message])])

761
src/compiler/GF/Compile/TypeCheck/RConcrete.hs
View File

@@ -1,761 +0,0 @@
{-# LANGUAGE PatternGuards #-}
module GF.Compile.TypeCheck.RConcrete( checkLType, inferLType, computeLType, ppType ) where
import GF.Infra.CheckM
import GF.Data.Operations
import GF.Grammar
import GF.Grammar.Lookup
import GF.Grammar.Predef
import GF.Grammar.PatternMatch
import GF.Grammar.Lockfield (isLockLabel, lockRecType, unlockRecord)
import GF.Compile.TypeCheck.Primitives
import Data.List
import Control.Monad
import GF.Text.Pretty
computeLType :: SourceGrammar -> Context -> Type -> Check Type
computeLType gr g0 t = comp (reverse [(b,x, Vr x) | (b,x,_) <- g0] ++ g0) t
where
comp g ty = case ty of
_ | Just _ <- isTypeInts ty -> return ty ---- shouldn't be needed
| isPredefConstant ty -> return ty ---- shouldn't be needed
Q (m,ident) -> checkIn ("module" <+> m) $ do
ty' <- lookupResDef gr (m,ident)
if ty' == ty then return ty else comp g ty' --- is this necessary to test?
AdHocOverload ts -> do
over <- getOverload gr g (Just typeType) t
case over of
Just (tr,_) -> return tr
_ -> checkError ("unresolved overloading of constants" <+> ppTerm Qualified 0 t)
Vr ident -> checkLookup ident g -- never needed to compute!
App f a -> do
f' <- comp g f
a' <- comp g a
case f' of
Abs b x t -> comp ((b,x,a'):g) t
_ -> return $ App f' a'
Prod bt x a b -> do
a' <- comp g a
b' <- comp ((bt,x,Vr x) : g) b
return $ Prod bt x a' b'
Abs bt x b -> do
b' <- comp ((bt,x,Vr x):g) b
return $ Abs bt x b'
Let (x,(_,a)) b -> comp ((Explicit,x,a):g) b
ExtR r s -> do
r' <- comp g r
s' <- comp g s
case (r',s') of
(RecType rs, RecType ss) -> plusRecType r' s' >>= comp g
_ -> return $ ExtR r' s'
RecType fs -> do
let fs' = sortRec fs
liftM RecType $ mapPairsM (comp g) fs'
ELincat c t -> do
t' <- comp g t
lockRecType c t' ---- locking to be removed AR 20/6/2009
_ | ty == typeTok -> return typeStr
_ | isPredefConstant ty -> return ty
_ -> composOp (comp g) ty
-- the underlying algorithms
inferLType :: SourceGrammar -> Context -> Term -> Check (Term, Type)
inferLType gr g trm = case trm of
Q (m,ident) | isPredef m -> termWith trm $ case typPredefined ident of
Just ty -> return ty
Nothing -> checkError ("unknown in Predef:" <+> ident)
Q ident -> checks [
termWith trm $ lookupResType gr ident >>= computeLType gr g
,
lookupResDef gr ident >>= inferLType gr g
,
checkError ("cannot infer type of constant" <+> ppTerm Unqualified 0 trm)
]
QC (m,ident) | isPredef m -> termWith trm $ case typPredefined ident of
Just ty -> return ty
Nothing -> checkError ("unknown in Predef:" <+> ident)
QC ident -> checks [
termWith trm $ lookupResType gr ident >>= computeLType gr g
,
lookupResDef gr ident >>= inferLType gr g
,
checkError ("cannot infer type of canonical constant" <+> ppTerm Unqualified 0 trm)
]
Vr ident -> termWith trm $ checkLookup ident g
Typed e t -> do
t' <- computeLType gr g t
checkLType gr g e t'
AdHocOverload ts -> do
over <- getOverload gr g Nothing trm
case over of
Just trty -> return trty
_ -> checkError ("unresolved overloading of constants" <+> ppTerm Qualified 0 trm)
App f a -> do
over <- getOverload gr g Nothing trm
case over of
Just trty -> return trty
_ -> do
(f',fty) <- inferLType gr g f
fty' <- computeLType gr g fty
case fty' of
Prod bt z arg val -> do
a' <- justCheck g a arg
ty <- if isWildIdent z
then return val
else substituteLType [(bt,z,a')] val
return (App f' a',ty)
_ -> checkError ("A function type is expected for" <+> ppTerm Unqualified 0 f <+> "instead of type" <+> ppType fty)
S f x -> do
(f', fty) <- inferLType gr g f
case fty of
Table arg val -> do
x'<- justCheck g x arg
return (S f' x', val)
_ -> checkError ("table lintype expected for the table in" $$ nest 2 (ppTerm Unqualified 0 trm))
P t i -> do
(t',ty) <- inferLType gr g t --- ??
ty' <- computeLType gr g ty
let tr2 = P t' i
termWith tr2 $ case ty' of
RecType ts -> case lookup i ts of
Nothing -> checkError ("unknown label" <+> i <+> "in" $$ nest 2 (ppTerm Unqualified 0 ty'))
Just x -> return x
_ -> checkError ("record type expected for:" <+> ppTerm Unqualified 0 t $$
" instead of the inferred:" <+> ppTerm Unqualified 0 ty')
R r -> do
let (ls,fs) = unzip r
fsts <- mapM inferM fs
let ts = [ty | (Just ty,_) <- fsts]
checkCond ("cannot infer type of record" $$ nest 2 (ppTerm Unqualified 0 trm)) (length ts == length fsts)
return $ (R (zip ls fsts), RecType (zip ls ts))
T (TTyped arg) pts -> do
(_,val) <- checks $ map (inferCase (Just arg)) pts
checkLType gr g trm (Table arg val)
T (TComp arg) pts -> do
(_,val) <- checks $ map (inferCase (Just arg)) pts
checkLType gr g trm (Table arg val)
T ti pts -> do -- tries to guess: good in oper type inference
let pts' = [pt | pt@(p,_) <- pts, isConstPatt p]
case pts' of
[] -> checkError ("cannot infer table type of" <+> ppTerm Unqualified 0 trm)
---- PInt k : _ -> return $ Ints $ max [i | PInt i <- pts']
_ -> do
(arg,val) <- checks $ map (inferCase Nothing) pts'
checkLType gr g trm (Table arg val)
V arg pts -> do
(_,val) <- checks $ map (inferLType gr g) pts
-- return (trm, Table arg val) -- old, caused issue 68
checkLType gr g trm (Table arg val)
K s -> do
if elem ' ' s
then do
let ss = foldr C Empty (map K (words s))
----- removed irritating warning AR 24/5/2008
----- checkWarn ("token \"" ++ s ++
----- "\" converted to token list" ++ prt ss)
return (ss, typeStr)
else return (trm, typeStr)
EInt i -> return (trm, typeInt)
EFloat i -> return (trm, typeFloat)
Empty -> return (trm, typeStr)
C s1 s2 ->
check2 (flip (justCheck g) typeStr) C s1 s2 typeStr
Glue s1 s2 ->
check2 (flip (justCheck g) typeStr) Glue s1 s2 typeStr ---- typeTok
---- hack from Rename.identRenameTerm, to live with files with naming conflicts 18/6/2007
Strs (Cn c : ts) | c == cConflict -> do
checkWarn ("unresolved constant, could be any of" <+> hcat (map (ppTerm Unqualified 0) ts))
inferLType gr g (head ts)
Strs ts -> do
ts' <- mapM (\t -> justCheck g t typeStr) ts
return (Strs ts', typeStrs)
Alts t aa -> do
t' <- justCheck g t typeStr
aa' <- flip mapM aa (\ (c,v) -> do
c' <- justCheck g c typeStr
v' <- checks $ map (justCheck g v) [typeStrs, EPattType typeStr]
return (c',v'))
return (Alts t' aa', typeStr)
RecType r -> do
let (ls,ts) = unzip r
ts' <- mapM (flip (justCheck g) typeType) ts
return (RecType (zip ls ts'), typeType)
ExtR r s -> do
(r',rT) <- inferLType gr g r
rT' <- computeLType gr g rT
(s',sT) <- inferLType gr g s
sT' <- computeLType gr g sT
let trm' = ExtR r' s'
case (rT', sT') of
(RecType rs, RecType ss) -> do
let rt = RecType ([field | field@(l,_) <- rs, notElem l (map fst ss)] ++ ss) -- select types of later fields
checkLType gr g trm' rt ---- return (trm', rt)
_ | rT' == typeType && sT' == typeType -> do
return (trm', typeType)
_ -> checkError ("records or record types expected in" <+> ppTerm Unqualified 0 trm)
Sort _ ->
termWith trm $ return typeType
Prod bt x a b -> do
a' <- justCheck g a typeType
b' <- justCheck ((bt,x,a'):g) b typeType
return (Prod bt x a' b', typeType)
Table p t -> do
p' <- justCheck g p typeType --- check p partype!
t' <- justCheck g t typeType
return $ (Table p' t', typeType)
FV vs -> do
(_,ty) <- checks $ map (inferLType gr g) vs
--- checkIfComplexVariantType trm ty
checkLType gr g trm ty
EPattType ty -> do
ty' <- justCheck g ty typeType
return (EPattType ty',typeType)
EPatt p -> do
ty <- inferPatt p
return (trm, EPattType ty)
ELin c trm -> do
(trm',ty) <- inferLType gr g trm
ty' <- lockRecType c ty ---- lookup c; remove lock AR 20/6/2009
return $ (ELin c trm', ty')
_ -> checkError ("cannot infer lintype of" <+> ppTerm Unqualified 0 trm)
where
isPredef m = elem m [cPredef,cPredefAbs]
justCheck g ty te = checkLType gr g ty te >>= return . fst
-- for record fields, which may be typed
inferM (mty, t) = do
(t', ty') <- case mty of
Just ty -> checkLType gr g t ty
_ -> inferLType gr g t
return (Just ty',t')
inferCase mty (patt,term) = do
arg <- maybe (inferPatt patt) return mty
cont <- pattContext gr g arg patt
(_,val) <- inferLType gr (reverse cont ++ g) term
return (arg,val)
isConstPatt p = case p of
PC _ ps -> True --- all isConstPatt ps
PP _ ps -> True --- all isConstPatt ps
PR ps -> all (isConstPatt . snd) ps
PT _ p -> isConstPatt p
PString _ -> True
PInt _ -> True
PFloat _ -> True
PChar -> True
PChars _ -> True
PSeq p q -> isConstPatt p && isConstPatt q
PAlt p q -> isConstPatt p && isConstPatt q
PRep p -> isConstPatt p
PNeg p -> isConstPatt p
PAs _ p -> isConstPatt p
_ -> False
inferPatt p = case p of
PP (q,c) ps | q /= cPredef -> liftM valTypeCnc (lookupResType gr (q,c))
PAs _ p -> inferPatt p
PNeg p -> inferPatt p
PAlt p q -> checks [inferPatt p, inferPatt q]
PSeq _ _ -> return $ typeStr
PRep _ -> return $ typeStr
PChar -> return $ typeStr
PChars _ -> return $ typeStr
_ -> inferLType gr g (patt2term p) >>= return . snd
-- type inference: Nothing, type checking: Just t
-- the latter permits matching with value type
getOverload :: SourceGrammar -> Context -> Maybe Type -> Term -> Check (Maybe (Term,Type))
getOverload gr g mt ot = case appForm ot of
(f@(Q c), ts) -> case lookupOverload gr c of
Ok typs -> do
ttys <- mapM (inferLType gr g) ts
v <- matchOverload f typs ttys
return $ Just v
_ -> return Nothing
(AdHocOverload cs@(f:_), ts) -> do --- the function name f is only used in error messages
let typs = concatMap collectOverloads cs
ttys <- mapM (inferLType gr g) ts
v <- matchOverload f typs ttys
return $ Just v
_ -> return Nothing
where
collectOverloads tr@(Q c) = case lookupOverload gr c of
Ok typs -> typs
_ -> case lookupResType gr c of
Ok ty -> let (args,val) = typeFormCnc ty in [(map (\(b,x,t) -> t) args,(val,tr))]
_ -> []
collectOverloads _ = [] --- constructors QC
matchOverload f typs ttys = do
let (tts,tys) = unzip ttys
let vfs = lookupOverloadInstance tys typs
let matches = [vf | vf@((_,v,_),_) <- vfs, matchVal mt v]
let showTypes ty = hsep (map ppType ty)
let (stys,styps) = (showTypes tys, [showTypes ty | (ty,_) <- typs])
-- to avoid strange error msg e.g. in case of unmatch record extension, show whole types if needed AR 28/1/2013
let (stysError,stypsError) = if elem (render stys) (map render styps)
then (hsep (map (ppTerm Unqualified 0) tys), [hsep (map (ppTerm Unqualified 0) ty) | (ty,_) <- typs])
else (stys,styps)
case ([vf | (vf,True) <- matches],[vf | (vf,False) <- matches]) of
([(_,val,fun)],_) -> return (mkApp fun tts, val)
([],[(pre,val,fun)]) -> do
checkWarn $ "ignoring lock fields in resolving" <+> ppTerm Unqualified 0 ot $$
"for" $$
nest 2 (showTypes tys) $$
"using" $$
nest 2 (showTypes pre)
return (mkApp fun tts, val)
([],[]) -> do
checkError $ "no overload instance of" <+> ppTerm Qualified 0 f $$
maybe empty (\x -> "with value type" <+> ppType x) mt $$
"for argument list" $$
nest 2 stysError $$
"among alternatives" $$
nest 2 (vcat stypsError)
(vfs1,vfs2) -> case (noProds vfs1,noProds vfs2) of
([(val,fun)],_) -> do
return (mkApp fun tts, val)
([],[(val,fun)]) -> do
checkWarn ("ignoring lock fields in resolving" <+> ppTerm Unqualified 0 ot)
return (mkApp fun tts, val)
----- unsafely exclude irritating warning AR 24/5/2008
----- checkWarn $ "overloading of" +++ prt f +++
----- "resolved by excluding partial applications:" ++++
----- unlines [prtType env ty | (ty,_) <- vfs', not (noProd ty)]
--- now forgiving ambiguity with a warning AR 1/2/2014
-- This gives ad hoc overloading the same behaviour as the choice of the first match in renaming did before.
-- But it also gives a chance to ambiguous overloadings that were banned before.
(nps1,nps2) -> do
checkWarn $ "ambiguous overloading of" <+> ppTerm Unqualified 0 f <+>
---- "with argument types" <+> hsep (map (ppTerm Qualified 0) tys) $$
"resolved by selecting the first of the alternatives" $$
nest 2 (vcat [ppTerm Qualified 0 fun | (_,ty,fun) <- vfs1 ++ if null vfs1 then vfs2 else []])
case [(mkApp fun tts,val) | (val,fun) <- nps1 ++ nps2] of
[] -> checkError $ "no alternatives left when resolving" <+> ppTerm Unqualified 0 f
h:_ -> return h
matchVal mt v = elem mt [Nothing,Just v,Just (unlocked v)]
unlocked v = case v of
RecType fs -> RecType $ filter (not . isLockLabel . fst) fs
_ -> v
---- TODO: accept subtypes
---- TODO: use a trie
lookupOverloadInstance tys typs =
[((pre,mkFunType rest val, t),isExact) |
let lt = length tys,
(ty,(val,t)) <- typs, length ty >= lt,
let (pre,rest) = splitAt lt ty,
let isExact = pre == tys,
isExact || map unlocked pre == map unlocked tys
]
noProds vfs = [(v,f) | (_,v,f) <- vfs, noProd v]
noProd ty = case ty of
Prod _ _ _ _ -> False
_ -> True
checkLType :: SourceGrammar -> Context -> Term -> Type -> Check (Term, Type)
checkLType gr g trm typ0 = do
typ <- computeLType gr g typ0
case trm of
Abs bt x c -> do
case typ of
Prod bt' z a b -> do
(c',b') <- if isWildIdent z
then checkLType gr ((bt,x,a):g) c b
else do b' <- checkIn (pp "abs") $ substituteLType [(bt',z,Vr x)] b
checkLType gr ((bt,x,a):g) c b'
return $ (Abs bt x c', Prod bt' z a b')
_ -> checkError $ "function type expected instead of" <+> ppType typ
App f a -> do
over <- getOverload gr g (Just typ) trm
case over of
Just trty -> return trty
_ -> do
(trm',ty') <- inferLType gr g trm
termWith trm' $ checkEqLType gr g typ ty' trm'
AdHocOverload ts -> do
over <- getOverload gr g Nothing trm
case over of
Just trty -> return trty
_ -> checkError ("unresolved overloading of constants" <+> ppTerm Qualified 0 trm)
Q _ -> do
over <- getOverload gr g (Just typ) trm
case over of
Just trty -> return trty
_ -> do
(trm',ty') <- inferLType gr g trm
termWith trm' $ checkEqLType gr g typ ty' trm'
T _ [] ->
checkError ("found empty table in type" <+> ppTerm Unqualified 0 typ)
T _ cs -> case typ of
Table arg val -> do
case allParamValues gr arg of
Ok vs -> do
let ps0 = map fst cs
ps <- testOvershadow ps0 vs
if null ps
then return ()
else checkWarn ("patterns never reached:" $$
nest 2 (vcat (map (ppPatt Unqualified 0) ps)))
_ -> return () -- happens with variable types
cs' <- mapM (checkCase arg val) cs
return (T (TTyped arg) cs', typ)
_ -> checkError $ "table type expected for table instead of" $$ nest 2 (ppType typ)
V arg0 vs ->
case typ of
Table arg1 val ->
do arg' <- checkEqLType gr g arg0 arg1 trm
vs1 <- allParamValues gr arg1
if length vs1 == length vs
then return ()
else checkError $ "wrong number of values in table" <+> ppTerm Unqualified 0 trm
vs' <- map fst `fmap` sequence [checkLType gr g v val|v<-vs]
return (V arg' vs',typ)
R r -> case typ of --- why needed? because inference may be too difficult
RecType rr -> do
--let (ls,_) = unzip rr -- labels of expected type
fsts <- mapM (checkM r) rr -- check that they are found in the record
return $ (R fsts, typ) -- normalize record
_ -> checkError ("record type expected in type checking instead of" $$ nest 2 (ppTerm Unqualified 0 typ))
ExtR r s -> case typ of
_ | typ == typeType -> do
trm' <- computeLType gr g trm
case trm' of
RecType _ -> termWith trm' $ return typeType
ExtR (Vr _) (RecType _) -> termWith trm' $ return typeType
-- ext t = t ** ...
_ -> checkError ("invalid record type extension" <+> nest 2 (ppTerm Unqualified 0 trm))
RecType rr -> do
ll2 <- case s of
R ss -> return $ map fst ss
_ -> do
(s',typ2) <- inferLType gr g s
case typ2 of
RecType ss -> return $ map fst ss
_ -> checkError ("cannot get labels from" $$ nest 2 (ppTerm Unqualified 0 typ2))
let ll1 = [l | (l,_) <- rr, notElem l ll2]
(r',_) <- checkLType gr g r (RecType [field | field@(l,_) <- rr, elem l ll1])
(s',_) <- checkLType gr g s (RecType [field | field@(l,_) <- rr, elem l ll2])
let rec = R ([(l,(Nothing,P r' l)) | l <- ll1] ++ [(l,(Nothing,P s' l)) | l <- ll2])
return (rec, typ)
ExtR ty ex -> do
r' <- justCheck g r ty
s' <- justCheck g s ex
return $ (ExtR r' s', typ) --- is this all? it assumes the same division in trm and typ
_ -> checkError ("record extension not meaningful for" <+> ppTerm Unqualified 0 typ)
FV vs -> do
ttys <- mapM (flip (checkLType gr g) typ) vs
--- checkIfComplexVariantType trm typ
return (FV (map fst ttys), typ) --- typ' ?
S tab arg -> checks [ do
(tab',ty) <- inferLType gr g tab
ty' <- computeLType gr g ty
case ty' of
Table p t -> do
(arg',val) <- checkLType gr g arg p
checkEqLType gr g typ t trm
return (S tab' arg', t)
_ -> checkError ("table type expected for applied table instead of" <+> ppType ty')
, do
(arg',ty) <- inferLType gr g arg
ty' <- computeLType gr g ty
(tab',_) <- checkLType gr g tab (Table ty' typ)
return (S tab' arg', typ)
]
Let (x,(mty,def)) body -> case mty of
Just ty -> do
(ty0,_) <- checkLType gr g ty typeType
(def',ty') <- checkLType gr g def ty0
body' <- justCheck ((Explicit,x,ty'):g) body typ
return (Let (x,(Just ty',def')) body', typ)
_ -> do
(def',ty) <- inferLType gr g def -- tries to infer type of local constant
checkLType gr g (Let (x,(Just ty,def')) body) typ
ELin c tr -> do
tr1 <- unlockRecord c tr
checkLType gr g tr1 typ
_ -> do
(trm',ty') <- inferLType gr g trm
termWith trm' $ checkEqLType gr g typ ty' trm'
where
justCheck g ty te = checkLType gr g ty te >>= return . fst
{-
recParts rr t = (RecType rr1,RecType rr2) where
(rr1,rr2) = partition (flip elem (map fst t) . fst) rr
-}
checkM rms (l,ty) = case lookup l rms of
Just (Just ty0,t) -> do
checkEqLType gr g ty ty0 t
(t',ty') <- checkLType gr g t ty
return (l,(Just ty',t'))
Just (_,t) -> do
(t',ty') <- checkLType gr g t ty
return (l,(Just ty',t'))
_ -> checkError $
if isLockLabel l
then let cat = drop 5 (showIdent (label2ident l))
in ppTerm Unqualified 0 (R rms) <+> "is not in the lincat of" <+> cat <>
"; try wrapping it with lin" <+> cat
else "cannot find value for label" <+> l <+> "in" <+> ppTerm Unqualified 0 (R rms)
checkCase arg val (p,t) = do
cont <- pattContext gr g arg p
t' <- justCheck (reverse cont ++ g) t val
return (p,t')
pattContext :: SourceGrammar -> Context -> Type -> Patt -> Check Context
pattContext env g typ p = case p of
PV x -> return [(Explicit,x,typ)]
PP (q,c) ps | q /= cPredef -> do ---- why this /=? AR 6/1/2006
t <- lookupResType env (q,c)
let (cont,v) = typeFormCnc t
checkCond ("wrong number of arguments for constructor in" <+> ppPatt Unqualified 0 p)
(length cont == length ps)
checkEqLType env g typ v (patt2term p)
mapM (\((_,_,ty),p) -> pattContext env g ty p) (zip cont ps) >>= return . concat
PR r -> do
typ' <- computeLType env g typ
case typ' of
RecType t -> do
let pts = [(ty,tr) | (l,tr) <- r, Just ty <- [lookup l t]]
----- checkWarn $ prt p ++++ show pts ----- debug
mapM (uncurry (pattContext env g)) pts >>= return . concat
_ -> checkError ("record type expected for pattern instead of" <+> ppTerm Unqualified 0 typ')
PT t p' -> do
checkEqLType env g typ t (patt2term p')
pattContext env g typ p'
PAs x p -> do
g' <- pattContext env g typ p
return ((Explicit,x,typ):g')
PAlt p' q -> do
g1 <- pattContext env g typ p'
g2 <- pattContext env g typ q
let pts = nub ([x | pt@(_,x,_) <- g1, notElem pt g2] ++ [x | pt@(_,x,_) <- g2, notElem pt g1])
checkCond
("incompatible bindings of" <+>
fsep pts <+>
"in pattern alterantives" <+> ppPatt Unqualified 0 p) (null pts)
return g1 -- must be g1 == g2
PSeq p q -> do
g1 <- pattContext env g typ p
g2 <- pattContext env g typ q
return $ g1 ++ g2
PRep p' -> noBind typeStr p'
PNeg p' -> noBind typ p'
_ -> return [] ---- check types!
where
noBind typ p' = do
co <- pattContext env g typ p'
if not (null co)
then checkWarn ("no variable bound inside pattern" <+> ppPatt Unqualified 0 p)
>> return []
else return []
checkEqLType :: SourceGrammar -> Context -> Type -> Type -> Term -> Check Type
checkEqLType gr g t u trm = do
(b,t',u',s) <- checkIfEqLType gr g t u trm
case b of
True -> return t'
False -> checkError $ s <+> "type of" <+> ppTerm Unqualified 0 trm $$
"expected:" <+> ppTerm Qualified 0 t $$ -- ppqType t u $$
"inferred:" <+> ppTerm Qualified 0 u -- ppqType u t
checkIfEqLType :: SourceGrammar -> Context -> Type -> Type -> Term -> Check (Bool,Type,Type,String)
checkIfEqLType gr g t u trm = do
t' <- computeLType gr g t
u' <- computeLType gr g u
case t' == u' || alpha [] t' u' of
True -> return (True,t',u',[])
-- forgive missing lock fields by only generating a warning.
--- better: use a flag to forgive? (AR 31/1/2006)
_ -> case missingLock [] t' u' of
Ok lo -> do
checkWarn $ "missing lock field" <+> fsep lo
return (True,t',u',[])
Bad s -> return (False,t',u',s)
where
-- check that u is a subtype of t
--- quick hack version of TC.eqVal
alpha g t u = case (t,u) of
-- error (the empty type!) is subtype of any other type
(_,u) | u == typeError -> True
-- contravariance
(Prod _ x a b, Prod _ y c d) -> alpha g c a && alpha ((x,y):g) b d
-- record subtyping
(RecType rs, RecType ts) -> all (\ (l,a) ->
any (\ (k,b) -> l == k && alpha g a b) ts) rs
(ExtR r s, ExtR r' s') -> alpha g r r' && alpha g s s'
(ExtR r s, t) -> alpha g r t || alpha g s t
-- the following say that Ints n is a subset of Int and of Ints m >= n
-- But why does it also allow Int as a subtype of Ints m? /TH 2014-04-04
(t,u) | Just m <- isTypeInts t, Just n <- isTypeInts u -> m >= n
| Just _ <- isTypeInts t, u == typeInt -> True ---- check size!
| t == typeInt, Just _ <- isTypeInts u -> True ---- why this ???? AR 11/12/2005
---- this should be made in Rename
(Q (m,a), Q (n,b)) | a == b -> elem m (allExtendsPlus gr n)
|| elem n (allExtendsPlus gr m)
|| m == n --- for Predef
(QC (m,a), QC (n,b)) | a == b -> elem m (allExtendsPlus gr n)
|| elem n (allExtendsPlus gr m)
(QC (m,a), Q (n,b)) | a == b -> elem m (allExtendsPlus gr n)
|| elem n (allExtendsPlus gr m)
(Q (m,a), QC (n,b)) | a == b -> elem m (allExtendsPlus gr n)
|| elem n (allExtendsPlus gr m)
-- contravariance
(Table a b, Table c d) -> alpha g c a && alpha g b d
(Vr x, Vr y) -> x == y || elem (x,y) g || elem (y,x) g
_ -> t == u
--- the following should be one-way coercions only. AR 4/1/2001
|| elem t sTypes && elem u sTypes
|| (t == typeType && u == typePType)
|| (u == typeType && t == typePType)
missingLock g t u = case (t,u) of
(RecType rs, RecType ts) ->
let
ls = [l | (l,a) <- rs,
not (any (\ (k,b) -> alpha g a b && l == k) ts)]
(locks,others) = partition isLockLabel ls
in case others of
_:_ -> Bad $ render ("missing record fields:" <+> fsep (punctuate ',' (others)))
_ -> return locks
-- contravariance
(Prod _ x a b, Prod _ y c d) -> do
ls1 <- missingLock g c a
ls2 <- missingLock g b d
return $ ls1 ++ ls2
_ -> Bad ""
sTypes = [typeStr, typeTok, typeString]
-- auxiliaries
-- | light-weight substitution for dep. types
substituteLType :: Context -> Type -> Check Type
substituteLType g t = case t of
Vr x -> return $ maybe t id $ lookup x [(x,t) | (_,x,t) <- g]
_ -> composOp (substituteLType g) t
termWith :: Term -> Check Type -> Check (Term, Type)
termWith t ct = do
ty <- ct
return (t,ty)
-- | compositional check\/infer of binary operations
check2 :: (Term -> Check Term) -> (Term -> Term -> Term) ->
Term -> Term -> Type -> Check (Term,Type)
check2 chk con a b t = do
a' <- chk a
b' <- chk b
return (con a' b', t)
-- printing a type with a lock field lock_C as C
ppType :: Type -> Doc
ppType ty =
case ty of
RecType fs -> case filter isLockLabel $ map fst fs of
[lock] -> pp (drop 5 (showIdent (label2ident lock)))
_ -> ppTerm Unqualified 0 ty
Prod _ x a b -> ppType a <+> "->" <+> ppType b
_ -> ppTerm Unqualified 0 ty
{-
ppqType :: Type -> Type -> Doc
ppqType t u = case (ppType t, ppType u) of
(pt,pu) | render pt == render pu -> ppTerm Qualified 0 t
(pt,_) -> pt
-}
checkLookup :: Ident -> Context -> Check Type
checkLookup x g =
case [ty | (b,y,ty) <- g, x == y] of
[] -> checkError ("unknown variable" <+> x)
(ty:_) -> return ty

88
src/compiler/GF/Compile/TypeCheck/TC.hs
View File

@@ -5,21 +5,22 @@
-- Stability : (stable)
-- Portability : (portable)
--
-- > CVS $Date: 2005/10/02 20:50:19 $
-- > CVS $Date: 2005/10/02 20:50:19 $
-- > CVS $Author: aarne $
-- > CVS $Revision: 1.11 $
--
-- Thierry Coquand's type checking algorithm that creates a trace
-----------------------------------------------------------------------------
module GF.Compile.TypeCheck.TC (AExp(..),
Theory,
checkExp,
inferExp,
checkBranch,
eqVal,
whnf
) where
module GF.Compile.TypeCheck.TC (
AExp(..),
Theory,
checkExp,
inferExp,
checkBranch,
eqVal,
whnf
) where
import GF.Data.Operations
import GF.Grammar
@@ -31,17 +32,17 @@ import Data.Maybe
import GF.Text.Pretty
data AExp =
AVr Ident Val
AVr Ident Val
| ACn QIdent Val
| AType
| AInt Int
| AType
| AInt Int
| AFloat Double
| AStr String
| AMeta MetaId Val
| ALet (Ident,(Val,AExp)) AExp
| AApp AExp AExp Val
| AAbs Ident Val AExp
| AProd Ident AExp AExp
| AApp AExp AExp Val
| AAbs Ident Val AExp
| AProd Ident AExp AExp
-- -- | AEqs [([Exp],AExp)] --- not used
| ARecType [ALabelling]
| AR [AAssign]
@@ -50,7 +51,7 @@ data AExp =
| AData Val
deriving (Eq,Show)
type ALabelling = (Label, AExp)
type ALabelling = (Label, AExp)
type AAssign = (Label, (Val, AExp))
type Theory = QIdent -> Err Val
@@ -71,7 +72,7 @@ whnf :: Val -> Err Val
whnf v = ---- errIn ("whnf" +++ prt v) $ ---- debug
case v of
VApp u w -> do
u' <- whnf u
u' <- whnf u
w' <- whnf w
app u' w'
VClos env e -> eval env e
@@ -81,9 +82,9 @@ app :: Val -> Val -> Err Val
app u v = case u of
VClos env (Abs _ x e) -> eval ((x,v):env) e
_ -> return $ VApp u v
eval :: Env -> Term -> Err Val
eval env e = ---- errIn ("eval" +++ prt e +++ "in" +++ prEnv env) $
eval env e = ---- errIn ("eval" +++ prt e +++ "in" +++ prEnv env) $
case e of
Vr x -> lookupVar env x
Q c -> return $ VCn c
@@ -95,23 +96,23 @@ eval env e = ---- errIn ("eval" +++ prt e +++ "in" +++ prEnv env) $
_ -> return $ VClos env e
eqVal :: Int -> Val -> Val -> Err [(Val,Val)]
eqVal k u1 u2 = ---- errIn (prt u1 +++ "<>" +++ prBracket (show k) +++ prt u2) $
eqVal k u1 u2 = ---- errIn (prt u1 +++ "<>" +++ prBracket (show k) +++ prt u2) $
do
w1 <- whnf u1
w2 <- whnf u2
w2 <- whnf u2
let v = VGen k
case (w1,w2) of
(VApp f1 a1, VApp f2 a2) -> liftM2 (++) (eqVal k f1 f2) (eqVal k a1 a2)
(VClos env1 (Abs _ x1 e1), VClos env2 (Abs _ x2 e2)) ->
eqVal (k+1) (VClos ((x1,v x1):env1) e1) (VClos ((x2,v x1):env2) e2)
(VClos env1 (Prod _ x1 a1 e1), VClos env2 (Prod _ x2 a2 e2)) ->
liftM2 (++)
liftM2 (++)
(eqVal k (VClos env1 a1) (VClos env2 a2))
(eqVal (k+1) (VClos ((x1,v x1):env1) e1) (VClos ((x2,v x1):env2) e2))
(VGen i _, VGen j _) -> return [(w1,w2) | i /= j]
(VCn (_, i), VCn (_,j)) -> return [(w1,w2) | i /= j]
(VCn (_, i), VCn (_,j)) -> return [(w1,w2) | i /= j]
--- thus ignore qualifications; valid because inheritance cannot
--- be qualified. Simplifies annotation. AR 17/3/2005
--- be qualified. Simplifies annotation. AR 17/3/2005
_ -> return [(w1,w2) | w1 /= w2]
-- invariant: constraints are in whnf
@@ -127,10 +128,10 @@ checkExp th tenv@(k,rho,gamma) e ty = do
Abs _ x t -> case typ of
VClos env (Prod _ y a b) -> do
a' <- whnf $ VClos env a ---
(t',cs) <- checkExp th
(k+1,(x,v x):rho, (x,a'):gamma) t (VClos ((y,v x):env) b)
return (AAbs x a' t', cs)
a' <- whnf $ VClos env a ---
(t',cs) <- checkExp th
(k+1,(x,v x):rho, (x,a'):gamma) t (VClos ((y,v x):env) b)
return (AAbs x a' t', cs)
_ -> Bad (render ("function type expected for" <+> ppTerm Unqualified 0 e <+> "instead of" <+> ppValue Unqualified 0 typ))
Let (x, (mb_typ, e1)) e2 -> do
@@ -150,7 +151,7 @@ checkExp th tenv@(k,rho,gamma) e ty = do
(b',csb) <- checkType th (k+1, (x,v x):rho, (x,VClos rho a):gamma) b
return (AProd x a' b', csa ++ csb)
R xs ->
R xs ->
case typ of
VRecType ys -> do case [l | (l,_) <- ys, isNothing (lookup l xs)] of
[] -> return ()
@@ -174,7 +175,7 @@ checkInferExp th tenv@(k,_,_) e typ = do
(e',w,cs1) <- inferExp th tenv e
cs2 <- eqVal k w typ
return (e',cs1 ++ cs2)
inferExp :: Theory -> TCEnv -> Term -> Err (AExp, Val, [(Val,Val)])
inferExp th tenv@(k,rho,gamma) e = case e of
Vr x -> mkAnnot (AVr x) $ noConstr $ lookupVar gamma x
@@ -200,13 +201,13 @@ inferExp th tenv@(k,rho,gamma) e = case e of
(e2,val2,cs2) <- inferExp th (k,rho,(x,val1):gamma) e2
return (ALet (x,(val1,e1)) e2, val2, cs1++cs2)
App f t -> do
(f',w,csf) <- inferExp th tenv f
(f',w,csf) <- inferExp th tenv f
typ <- whnf w
case typ of
VClos env (Prod _ x a b) -> do
(a',csa) <- checkExp th tenv t (VClos env a)
b' <- whnf $ VClos ((x,VClos rho t):env) b
return $ (AApp f' a' b', b', csf ++ csa)
b' <- whnf $ VClos ((x,VClos rho t):env) b
return $ (AApp f' a' b', b', csf ++ csa)
_ -> Bad (render ("Prod expected for function" <+> ppTerm Unqualified 0 f <+> "instead of" <+> ppValue Unqualified 0 typ))
_ -> Bad (render ("cannot infer type of expression" <+> ppTerm Unqualified 0 e))
@@ -232,9 +233,9 @@ checkAssign th tenv@(k,rho,gamma) typs (lbl,(Nothing,exp)) = do
return ((lbl,(val,aexp)),cs)
checkBranch :: Theory -> TCEnv -> Equation -> Val -> Err (([Term],AExp),[(Val,Val)])
checkBranch th tenv b@(ps,t) ty = errIn ("branch" +++ show b) $
chB tenv' ps' ty
where
checkBranch th tenv b@(ps,t) ty = errIn ("branch" +++ show b) $
chB tenv' ps' ty
where
(ps',_,rho2,k') = ps2ts k ps
tenv' = (k, rho2++rho, gamma) ---- k' ?
@@ -245,11 +246,11 @@ checkBranch th tenv b@(ps,t) ty = errIn ("branch" +++ show b) $
typ <- whnf ty
case typ of
VClos env (Prod _ y a b) -> do
a' <- whnf $ VClos env a
a' <- whnf $ VClos env a
(p', sigma, binds, cs1) <- checkP tenv p y a'
let tenv' = (length binds, sigma ++ rho, binds ++ gamma)
((ps',exp),cs2) <- chB tenv' ps2 (VClos ((y,p'):env) b)
return ((p:ps',exp), cs1 ++ cs2) -- don't change the patt
return ((p:ps',exp), cs1 ++ cs2) -- don't change the patt
_ -> Bad (render ("Product expected for definiens" <+> ppTerm Unqualified 0 t <+> "instead of" <+> ppValue Unqualified 0 typ))
[] -> do
(e,cs) <- checkExp th tenv t ty
@@ -259,15 +260,15 @@ checkBranch th tenv b@(ps,t) ty = errIn ("branch" +++ show b) $
let sigma = [(x, VGen i x) | ((x,_),i) <- zip delta [k..]]
return (VClos sigma t, sigma, delta, cs)
ps2ts k = foldr p2t ([],0,[],k)
ps2ts k = foldr p2t ([],0,[],k)
p2t p (ps,i,g,k) = case p of
PW -> (Meta i : ps, i+1,g,k)
PW -> (Meta i : ps, i+1,g,k)
PV x -> (Vr x : ps, i, upd x k g,k+1)
PAs x p -> p2t p (ps,i,g,k)
PString s -> (K s : ps, i, g, k)
PInt n -> (EInt n : ps, i, g, k)
PFloat n -> (EFloat n : ps, i, g, k)
PP c xs -> (mkApp (Q c) xss : ps, j, g',k')
PP c xs -> (mkApp (Q c) xss : ps, j, g',k')
where (xss,j,g',k') = foldr p2t ([],i,g,k) xs
PImplArg p -> p2t p (ps,i,g,k)
PTilde t -> (t : ps, i, g, k)
@@ -307,8 +308,8 @@ checkPatt th tenv exp val = do
case typ of
VClos env (Prod _ x a b) -> do
(a',_,csa) <- checkExpP tenv t (VClos env a)
b' <- whnf $ VClos ((x,VClos rho t):env) b
return $ (AApp f' a' b', b', csf ++ csa)
b' <- whnf $ VClos ((x,VClos rho t):env) b
return $ (AApp f' a' b', b', csf ++ csa)
_ -> Bad (render ("Prod expected for function" <+> ppTerm Unqualified 0 f <+> "instead of" <+> ppValue Unqualified 0 typ))
_ -> Bad (render ("cannot typecheck pattern" <+> ppTerm Unqualified 0 exp))
@@ -321,4 +322,3 @@ mkAnnot :: (Val -> AExp) -> Err (Val,[(Val,Val)]) -> Err (AExp,Val,[(Val,Val)])
mkAnnot a ti = do
(v,cs) <- ti
return (a v, v, cs)

69
src/compiler/GF/Compile/Update.hs
View File

@@ -5,7 +5,7 @@
-- Stability : (stable)
-- Portability : (portable)
--
-- > CVS $Date: 2005/05/30 18:39:44 $
-- > CVS $Date: 2005/05/30 18:39:44 $
-- > CVS $Author: aarne $
-- > CVS $Revision: 1.8 $
--
@@ -27,20 +27,21 @@ import Data.List
import qualified Data.Map as Map
import Control.Monad
import GF.Text.Pretty
import qualified Control.Monad.Fail as Fail
-- | combine a list of definitions into a balanced binary search tree
buildAnyTree :: Monad m => ModuleName -> [(Ident,Info)] -> m (Map.Map Ident Info)
buildAnyTree :: Fail.MonadFail m => ModuleName -> [(Ident,Info)] -> m (Map.Map Ident Info)
buildAnyTree m = go Map.empty
where
go map [] = return map
go map ((c,j):is) = do
go map ((c,j):is) =
case Map.lookup c map of
Just i -> case unifyAnyInfo m i j of
Ok k -> go (Map.insert c k map) is
Bad _ -> fail $ render ("conflicting information in module"<+>m $$
nest 4 (ppJudgement Qualified (c,i)) $$
"and" $+$
nest 4 (ppJudgement Qualified (c,j)))
Ok k -> go (Map.insert c k map) is
Bad _ -> fail $ render ("conflicting information in module"<+>m $$
nest 4 (ppJudgement Qualified (c,i)) $$
"and" $+$
nest 4 (ppJudgement Qualified (c,j)))
Nothing -> go (Map.insert c j map) is
extendModule :: FilePath -> SourceGrammar -> SourceModule -> Check SourceModule
@@ -50,14 +51,14 @@ extendModule cwd gr (name,m)
---- Should be replaced by real control. AR 4/2/2005
| mstatus m == MSIncomplete && isModCnc m = return (name,m)
| otherwise = checkInModule cwd m NoLoc empty $ do
m' <- foldM extOne m (mextend m)
m' <- foldM extOne m (mextend m)
return (name,m')
where
extOne mo (n,cond) = do
m0 <- lookupModule gr n
-- test that the module types match, and find out if the old is complete
unless (sameMType (mtype m) (mtype mo))
unless (sameMType (mtype m) (mtype mo))
(checkError ("illegal extension type to module" <+> name))
let isCompl = isCompleteModule m0
@@ -66,7 +67,7 @@ extendModule cwd gr (name,m)
js1 <- extendMod gr isCompl ((n,m0), isInherited cond) name (jments mo)
-- if incomplete, throw away extension information
return $
return $
if isCompl
then mo {jments = js1}
else mo {mextend= filter ((/=n) . fst) (mextend mo)
@@ -74,7 +75,7 @@ extendModule cwd gr (name,m)
,jments = js1
}
-- | rebuilding instance + interface, and "with" modules, prior to renaming.
-- | rebuilding instance + interface, and "with" modules, prior to renaming.
-- AR 24/10/2003
rebuildModule :: FilePath -> SourceGrammar -> SourceModule -> Check SourceModule
rebuildModule cwd gr mo@(i,mi@(ModInfo mt stat fs_ me mw ops_ med_ msrc_ env_ js_)) =
@@ -87,8 +88,8 @@ rebuildModule cwd gr mo@(i,mi@(ModInfo mt stat fs_ me mw ops_ med_ msrc_ env_ js
-- add the information given in interface into an instance module
Nothing -> do
unless (null is || mstatus mi == MSIncomplete)
(checkError ("module" <+> i <+>
unless (null is || mstatus mi == MSIncomplete)
(checkError ("module" <+> i <+>
"has open interfaces and must therefore be declared incomplete"))
case mt of
MTInstance (i0,mincl) -> do
@@ -112,7 +113,7 @@ rebuildModule cwd gr mo@(i,mi@(ModInfo mt stat fs_ me mw ops_ med_ msrc_ env_ js
let stat' = if all (flip elem infs) is
then MSComplete
else MSIncomplete
unless (stat' == MSComplete || stat == MSIncomplete)
unless (stat' == MSComplete || stat == MSIncomplete)
(checkError ("module" <+> i <+> "remains incomplete"))
ModInfo mt0 _ fs me' _ ops0 _ fpath _ js <- lookupModule gr ext
let ops1 = nub $
@@ -140,24 +141,24 @@ rebuildModule cwd gr mo@(i,mi@(ModInfo mt stat fs_ me mw ops_ med_ msrc_ env_ js
extendMod :: Grammar ->
Bool -> (Module,Ident -> Bool) -> ModuleName ->
Map.Map Ident Info -> Check (Map.Map Ident Info)
extendMod gr isCompl ((name,mi),cond) base new = foldM try new $ Map.toList (jments mi)
extendMod gr isCompl ((name,mi),cond) base new = foldM try new $ Map.toList (jments mi)
where
try new (c,i0)
| not (cond c) = return new
| otherwise = case Map.lookup c new of
Just j -> case unifyAnyInfo name i j of
Ok k -> return $ Map.insert c k new
Bad _ -> do (base,j) <- case j of
AnyInd _ m -> lookupOrigInfo gr (m,c)
_ -> return (base,j)
(name,i) <- case i of
Ok k -> return $ Map.insert c k new
Bad _ -> do (base,j) <- case j of
AnyInd _ m -> lookupOrigInfo gr (m,c)
_ -> return (base,j)
(name,i) <- case i of
AnyInd _ m -> lookupOrigInfo gr (m,c)
_ -> return (name,i)
checkError ("cannot unify the information" $$
nest 4 (ppJudgement Qualified (c,i)) $$
"in module" <+> name <+> "with" $$
nest 4 (ppJudgement Qualified (c,j)) $$
"in module" <+> base)
checkError ("cannot unify the information" $$
nest 4 (ppJudgement Qualified (c,i)) $$
"in module" <+> name <+> "with" $$
nest 4 (ppJudgement Qualified (c,j)) $$
"in module" <+> base)
Nothing-> if isCompl
then return $ Map.insert c (indirInfo name i) new
else return $ Map.insert c i new
@@ -165,11 +166,11 @@ extendMod gr isCompl ((name,mi),cond) base new = foldM try new $ Map.toList (jme
i = globalizeLoc (msrc mi) i0
indirInfo :: ModuleName -> Info -> Info
indirInfo n info = AnyInd b n' where
indirInfo n info = AnyInd b n' where
(b,n') = case info of
ResValue _ -> (True,n)
ResParam _ _ -> (True,n)
AbsFun _ _ Nothing _ -> (True,n)
AbsFun _ _ Nothing _ -> (True,n)
AnyInd b k -> (b,k)
_ -> (False,n) ---- canonical in Abs
@@ -193,24 +194,24 @@ globalizeLoc fpath i =
unifyAnyInfo :: ModuleName -> Info -> Info -> Err Info
unifyAnyInfo m i j = case (i,j) of
(AbsCat mc1, AbsCat mc2) ->
(AbsCat mc1, AbsCat mc2) ->
liftM AbsCat (unifyMaybeL mc1 mc2)
(AbsFun mt1 ma1 md1 moper1, AbsFun mt2 ma2 md2 moper2) ->
(AbsFun mt1 ma1 md1 moper1, AbsFun mt2 ma2 md2 moper2) ->
liftM4 AbsFun (unifyMaybeL mt1 mt2) (unifAbsArrity ma1 ma2) (unifAbsDefs md1 md2) (unifyMaybe moper1 moper2) -- adding defs
(ResParam mt1 mv1, ResParam mt2 mv2) ->
liftM2 ResParam (unifyMaybeL mt1 mt2) (unifyMaybe mv1 mv2)
(ResValue (L l1 t1), ResValue (L l2 t2))
(ResValue (L l1 t1), ResValue (L l2 t2))
| t1==t2 -> return (ResValue (L l1 t1))
| otherwise -> fail ""
(_, ResOverload ms t) | elem m ms ->
return $ ResOverload ms t
(ResOper mt1 m1, ResOper mt2 m2) ->
(ResOper mt1 m1, ResOper mt2 m2) ->
liftM2 ResOper (unifyMaybeL mt1 mt2) (unifyMaybeL m1 m2)
(CncCat mc1 md1 mr1 mp1 mpmcfg1, CncCat mc2 md2 mr2 mp2 mpmcfg2) ->
(CncCat mc1 md1 mr1 mp1 mpmcfg1, CncCat mc2 md2 mr2 mp2 mpmcfg2) ->
liftM5 CncCat (unifyMaybeL mc1 mc2) (unifyMaybeL md1 md2) (unifyMaybeL mr1 mr2) (unifyMaybeL mp1 mp2) (unifyMaybe mpmcfg1 mpmcfg2)
(CncFun m mt1 md1 mpmcfg1, CncFun _ mt2 md2 mpmcfg2) ->
(CncFun m mt1 md1 mpmcfg1, CncFun _ mt2 md2 mpmcfg2) ->
liftM3 (CncFun m) (unifyMaybeL mt1 mt2) (unifyMaybeL md1 md2) (unifyMaybe mpmcfg1 mpmcfg2)
(AnyInd b1 m1, AnyInd b2 m2) -> do