mirror of
https://github.com/GrammaticalFramework/gf-core.git
synced 2026-08-19 10:46:22 -06:00
use the same type checker and evaluator for abstract and concrete syntax
This commit is contained in:
Krasimir Angelov
@@ -19,8 +19,8 @@ import GF.Grammar.Analyse
|
||||
import GF.Grammar.ShowTerm
|
||||
import GF.Grammar.Lookup (allOpers,allOpersTo)
|
||||
import GF.Compile.Rename(renameSourceTerm)
|
||||
import GF.Compile.Compute.Concrete(normalForm,normalFlatForm,Globals(..),stdPredef)
|
||||
import GF.Compile.TypeCheck.Concrete as TC(inferLType)
|
||||
import GF.Compile.Compute(normalForm,normalFlatForm,Globals(..),stdPredef)
|
||||
import GF.Compile.TypeCheck as TC(inferLType)
|
||||
|
||||
import GF.Command.Abstract(Option(..),isOpt,listFlags,valueString,valStrOpts)
|
||||
import GF.Command.CommandInfo
|
||||
@@ -253,7 +253,7 @@ checkComputeTerm os sgr t =
|
||||
-- ** Try to compute pre{...} tokens in token sequences
|
||||
singleton x = [x]
|
||||
|
||||
g = Gl sgr (stdPredef g)
|
||||
g = Gl sgr (stdPredef g) False
|
||||
|
||||
evalStr t =
|
||||
case t of
|
||||
|
||||
@@ -26,9 +26,8 @@ import Prelude hiding ((<>))
|
||||
import GF.Infra.Ident
|
||||
import GF.Infra.Option
|
||||
|
||||
import GF.Compile.TypeCheck.Abstract
|
||||
import GF.Compile.TypeCheck.Concrete(checkLType,inferLType)
|
||||
import GF.Compile.Compute.Concrete(normalForm,Globals(..),stdPredef)
|
||||
import GF.Compile.TypeCheck(checkLType,inferLType,checkContext,checkDef)
|
||||
import GF.Compile.Compute(normalForm,Globals(..),noPredef,stdPredef)
|
||||
|
||||
import GF.Grammar
|
||||
import GF.Grammar.Lexer
|
||||
@@ -157,42 +156,43 @@ checkInfo opts cwd sgr sm (c,info) = checkInModule cwd (snd sm) NoLoc empty $ do
|
||||
checkReservedId c
|
||||
case info of
|
||||
AbsCat (Just (L loc cont)) ->
|
||||
mkCheck loc "the category" $
|
||||
checkContext gr cont
|
||||
chIn loc "the category" $ do
|
||||
cont <- checkContext ga cont
|
||||
update sm c (AbsCat (Just (L loc cont)))
|
||||
|
||||
AbsFun (Just (L loc typ)) ma md moper -> do
|
||||
mkCheck loc "the type of function" $
|
||||
checkTyp gr typ
|
||||
typ <- compAbsTyp [] typ -- to calculate let definitions
|
||||
chIn loc "the type of function" $
|
||||
checkLType ga typ typeType
|
||||
typ <- normalForm ga typ -- to calculate let definitions
|
||||
case md of
|
||||
Just eqs -> mapM_ (\(L loc eq) -> mkCheck loc "the definition of function" $
|
||||
checkDef gr (fst sm,c) typ eq) eqs
|
||||
Just eqs -> mapM_ (\(L loc eq) -> chIn loc "the definition of function" $
|
||||
checkDef ga (fst sm,c) typ eq) eqs
|
||||
Nothing -> return ()
|
||||
update sm c (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" $ do
|
||||
(typ,_) <- checkLType g typ typeType
|
||||
typ <- normalForm g typ
|
||||
(typ,_) <- checkLType gc typ typeType
|
||||
typ <- normalForm gc typ
|
||||
return (Just (L loc typ))
|
||||
Nothing -> return Nothing
|
||||
mdef <- case (mty,mdef) of
|
||||
(Just (L _ typ),Just (L loc def)) ->
|
||||
chIn loc "default linearization of" $ do
|
||||
(def,_) <- checkLType g def (mkFunType [typeStr] typ)
|
||||
(def,_) <- checkLType gc def (mkFunType [typeStr] typ)
|
||||
return (Just (L loc def))
|
||||
_ -> return Nothing
|
||||
mref <- case (mty,mref) of
|
||||
(Just (L _ typ),Just (L loc ref)) ->
|
||||
chIn loc "reference linearization of" $ do
|
||||
(ref,_) <- checkLType g ref (mkFunType [typ] typeStr)
|
||||
(ref,_) <- checkLType gc ref (mkFunType [typ] typeStr)
|
||||
return (Just (L loc ref))
|
||||
_ -> return Nothing
|
||||
mpr <- case mpr of
|
||||
(Just (L loc t)) ->
|
||||
chIn loc "print name of" $ do
|
||||
(t,_) <- checkLType g t typeStr
|
||||
(t,_) <- checkLType gc t typeStr
|
||||
return (Just (L loc t))
|
||||
_ -> return Nothing
|
||||
update sm c (CncCat mty mdef mref mpr mpmcfg)
|
||||
@@ -201,13 +201,13 @@ checkInfo opts cwd sgr sm (c,info) = checkInModule cwd (snd sm) NoLoc empty $ do
|
||||
mt <- case (mty,mt) of
|
||||
(Just (args,cat,cont,val),Just (L loc trm)) ->
|
||||
chIn loc "linearization of" $ do
|
||||
(trm,_) <- checkLType g trm (mkFunType (zipWith (\cat (_,_,ty) -> lock cat ty) args cont) val) -- erases arg vars
|
||||
(trm,_) <- checkLType gc trm (mkFunType (zipWith (\cat (_,_,ty) -> lock cat ty) args cont) val) -- erases arg vars
|
||||
return (Just (L loc (etaExpand [] trm cont)))
|
||||
_ -> return mt
|
||||
mpr <- case mpr of
|
||||
(Just (L loc t)) ->
|
||||
chIn loc "print name of" $ do
|
||||
(t,_) <- checkLType g t typeStr
|
||||
(t,_) <- checkLType gc t typeStr
|
||||
return (Just (L loc t))
|
||||
_ -> return Nothing
|
||||
update sm c (CncFun mty mt mpr mpmcfg)
|
||||
@@ -216,14 +216,14 @@ checkInfo opts cwd sgr sm (c,info) = checkInModule cwd (snd sm) NoLoc empty $ do
|
||||
(pty', pde') <- case (pty,pde) of
|
||||
(Just (L loct ty), Just (L locd de)) -> do
|
||||
ty' <- chIn loct "operation" $ do
|
||||
(ty,_) <- checkLType g ty typeType
|
||||
normalForm g ty
|
||||
(ty,_) <- checkLType gc ty typeType
|
||||
normalForm gc ty
|
||||
(de',_) <- chIn locd "operation" $
|
||||
checkLType g de ty'
|
||||
checkLType gc de ty'
|
||||
return (Just (L loct ty'), Just (L locd de'))
|
||||
(Nothing , Just (L locd de)) -> do
|
||||
(de',ty') <- chIn locd "operation" $
|
||||
inferLType g de
|
||||
inferLType gc de
|
||||
return (Just (L locd ty'), Just (L locd de'))
|
||||
(Just (L loct ty), Nothing) -> do
|
||||
chIn loct "operation" $
|
||||
@@ -231,10 +231,10 @@ checkInfo opts cwd sgr sm (c,info) = checkInModule cwd (snd sm) NoLoc empty $ do
|
||||
update sm c (ResOper pty' pde')
|
||||
|
||||
ResOverload os tysts -> chIn NoLoc "overloading" $ do
|
||||
tysts' <- mapM (uncurry $ flip (\(L loc1 t) (L loc2 ty) -> checkLType g t ty >>= \(t,ty) -> return (L loc1 t, L loc2 ty))) tysts -- return explicit ones
|
||||
tysts' <- mapM (uncurry $ flip (\(L loc1 t) (L loc2 ty) -> checkLType gc t ty >>= \(t,ty) -> return (L loc1 t, L loc2 ty))) tysts -- return explicit ones
|
||||
tysts0 <- lookupOverload gr (fst sm,c) -- check against inherited ones too
|
||||
tysts1 <- sequence
|
||||
[checkLType g tr (mkFunType args val) | (args,(val,tr)) <- tysts0]
|
||||
[checkLType gc tr (mkFunType args val) | (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 $
|
||||
@@ -249,12 +249,13 @@ checkInfo opts cwd sgr sm (c,info) = checkInModule cwd (snd sm) NoLoc empty $ do
|
||||
_ -> return sm
|
||||
where
|
||||
gr = prependModule sgr sm
|
||||
g = Gl gr (stdPredef g)
|
||||
ga = Gl gr noPredef True
|
||||
gc = Gl gr (stdPredef gc) False
|
||||
chIn loc cat = checkInModule cwd (snd sm) loc ("Happened in" <+> cat <+> c)
|
||||
|
||||
mkParamValues sm c cnt ts [] = return (sm,cnt,[],[])
|
||||
mkParamValues sm@(mn,mi) c cnt ts ((p,co):pcs) = do
|
||||
co <- mapM (\(b,v,ty) -> normalForm g ty >>= \ty -> return (b,v,ty)) co
|
||||
co <- mapM (\(b,v,ty) -> normalForm gc ty >>= \ty -> return (b,v,ty)) co
|
||||
sm <- case lookupIdent p (jments mi) of
|
||||
Ok (ResValue (L loc _) _) -> update sm p (ResValue (L loc (mkProdSimple co (QC (mn,c)))) cnt)
|
||||
Bad msg -> checkError (pp msg)
|
||||
@@ -269,22 +270,6 @@ checkInfo opts cwd sgr sm (c,info) = checkInModule cwd (snd sm) NoLoc empty $ do
|
||||
| otherwise -> checkUniq $ y:xs
|
||||
_ -> return ()
|
||||
|
||||
mkCheck loc cat ss = case ss of
|
||||
[] -> return sm
|
||||
_ -> chIn loc cat $ checkError (vcat ss)
|
||||
|
||||
compAbsTyp g t = case t of
|
||||
Vr x -> maybe (checkError ("no value given to variable" <+> x)) return $ lookup x g
|
||||
Let (x,(_,a)) b -> do
|
||||
a' <- compAbsTyp g a
|
||||
compAbsTyp ((x, a'):g) b
|
||||
Prod b x a t -> do
|
||||
a' <- compAbsTyp g a
|
||||
t' <- compAbsTyp ((x,Vr x):g) t
|
||||
return $ Prod b x a' t'
|
||||
Abs _ _ _ -> return t
|
||||
_ -> composOp (compAbsTyp g) t
|
||||
|
||||
etaExpand xs t [] = t
|
||||
etaExpand xs (Abs bt x t) (_ :cont) = Abs bt x (etaExpand (x:xs) t cont)
|
||||
etaExpand xs t ((bt,_,ty):cont) = Abs bt x (etaExpand (x:xs) (App t (Vr x)) cont)
|
||||
@@ -331,4 +316,4 @@ linTypeOfType cnc m (L loc typ) = do
|
||||
lookupLincat cnc m c >>= normalForm g
|
||||
,return defLinType
|
||||
]
|
||||
g = Gl cnc (stdPredef g)
|
||||
g = Gl cnc (stdPredef g) False
|
||||
|
||||
+17
-8
@@ -1,10 +1,10 @@
|
||||
{-# LANGUAGE RankNTypes, BangPatterns, GeneralizedNewtypeDeriving, TupleSections #-}
|
||||
|
||||
module GF.Compile.Compute.Concrete
|
||||
module GF.Compile.Compute
|
||||
(Env, Scope, Value(..), Variants(..), OptionInfo(..),
|
||||
ConstValue(..), Globals(..), PredefTable, EvalM,
|
||||
mapVariantsC, unvariants,
|
||||
runEvalM, runEvalMWithInput, stdPredef, globals,
|
||||
runEvalM, runEvalMWithInput, stdPredef, noPredef, globals,
|
||||
PredefImpl, Predef(..), ($\),
|
||||
pdCanonicalArgs, pdArity,
|
||||
normalForm, normalFlatForm,
|
||||
@@ -17,7 +17,7 @@ import GF.Infra.Ident
|
||||
import GF.Infra.CheckM
|
||||
import GF.Data.Operations(Err(..))
|
||||
import GF.Data.Utilities(maybeAt,splitAt',(<||>),anyM,secondM,bimapM)
|
||||
import GF.Grammar.Lookup(lookupResDef,lookupOrigInfo)
|
||||
import GF.Grammar.Lookup(lookupAbsDef,lookupResDef,lookupOrigInfo)
|
||||
import GF.Grammar.Grammar
|
||||
import GF.Grammar.Macros
|
||||
import GF.Grammar.Predef
|
||||
@@ -58,7 +58,7 @@ pdArity n def = Predef $ \g c args ->
|
||||
type Env = [(Ident,Value)]
|
||||
type Scope = [(Ident,Value)]
|
||||
type PredefTable = Map.Map Ident Predef
|
||||
data Globals = Gl Grammar PredefTable
|
||||
data Globals = Gl Grammar PredefTable Bool {- True for abstract, False for concrete -}
|
||||
|
||||
data Value
|
||||
= VApp Choice QIdent [Value]
|
||||
@@ -245,11 +245,17 @@ eval g env s (Let (x,(_,t1)) t2) vs = let (!s1,!s2) = split s
|
||||
in eval g ((x,eval g env s1 t1 []):env) s2 t2 vs
|
||||
eval g env c (Q q@(m,id)) vs
|
||||
| m == cPredef = evalPredef g c id vs
|
||||
| isAbstract = let v0 = VApp c q vs
|
||||
in case lookupAbsDef gr q of
|
||||
Ok (Just arity,Just eqs)
|
||||
| length vs < arity -> v0
|
||||
| otherwise -> patternMatch g c v0 (map (\(ps,t) -> (env,ps,vs,t)) eqs)
|
||||
Bad msg -> error msg
|
||||
| otherwise = case lookupResDef gr q of
|
||||
Ok t -> eval g env c t vs
|
||||
Bad msg -> error msg
|
||||
where
|
||||
Gl gr predef = g
|
||||
Gl gr predef isAbstract = g
|
||||
eval g env s (QC q) vs = VApp s q vs
|
||||
eval g env s (C t1 t2) [] = let (!s1,!s2) = split s
|
||||
|
||||
@@ -325,7 +331,7 @@ eval g env c t@(Opts n cs) vs = if null cs
|
||||
eval g env c t vs = VError ("Cannot reduce term" <+> pp t)
|
||||
|
||||
evalPredef :: Globals -> Choice -> Ident -> [Value] -> Value
|
||||
evalPredef g@(Gl gr pds) c n args =
|
||||
evalPredef g@(Gl gr pds _) c n args =
|
||||
case Map.lookup n pds of
|
||||
Nothing -> VApp c (cPredef,n) args
|
||||
Just def -> let valueOf (Const res) = res
|
||||
@@ -335,6 +341,9 @@ evalPredef g@(Gl gr pds) c n args =
|
||||
valueOf NonExist = VApp c (cPredef,cNonExist) []
|
||||
in valueOf (runPredef def g c args)
|
||||
|
||||
noPredef :: PredefTable
|
||||
noPredef = Map.empty
|
||||
|
||||
stdPredef :: Globals -> PredefTable
|
||||
stdPredef g = Map.fromList
|
||||
[(cInts, pdArity 1 $\ \g c vs -> Const (case vs of {[VInt i] -> VInts i False; vs -> VApp c (cPredef,cInts) vs}))
|
||||
@@ -540,7 +549,7 @@ patternMatch g s v0 ((env0,ps,args0,t):eqs) = match env0 ps eqs args0
|
||||
(pp t))
|
||||
Bad msg -> error msg
|
||||
where
|
||||
Gl gr _ = g
|
||||
Gl gr _ _ = g
|
||||
match env (PV v :ps) eqs (arg:args) = match ((v,arg):env) ps eqs args
|
||||
match env (PAs v p :ps) eqs (arg:args) = match ((v,arg):env) (p:ps) eqs (arg:args)
|
||||
match env (PW :ps) eqs (arg:args) = match env ps eqs args
|
||||
@@ -651,7 +660,7 @@ vtableSelect g v0 ty cs v2 vs =
|
||||
Ok res -> res
|
||||
Bad msg -> error msg
|
||||
|
||||
Gl gr _ = g
|
||||
Gl gr _ _ = g
|
||||
value2index (VInt n) (VApp _ c [VInt max])
|
||||
| Q c == cnPredef cInts = Const (fromIntegral n,fromIntegral max+1)
|
||||
value2index (VFV c vs) vty = CFV c (fmap (\v -> value2index v vty) vs)
|
||||
@@ -1,138 +0,0 @@
|
||||
----------------------------------------------------------------------
|
||||
-- |
|
||||
-- Module : GF.Compile.Abstract.Compute
|
||||
-- Maintainer : AR
|
||||
-- Stability : (stable)
|
||||
-- Portability : (portable)
|
||||
--
|
||||
-- > CVS $Date: 2005/10/02 20:50:19 $
|
||||
-- > CVS $Author: aarne $
|
||||
-- > CVS $Revision: 1.8 $
|
||||
--
|
||||
-- computation in abstract syntax w.r.t. explicit definitions.
|
||||
--
|
||||
-- old GF computation; to be updated
|
||||
-----------------------------------------------------------------------------
|
||||
|
||||
module GF.Compile.Compute.Abstract (LookDef,
|
||||
compute,
|
||||
computeAbsTerm,
|
||||
computeAbsTermIn,
|
||||
beta
|
||||
) where
|
||||
|
||||
import GF.Data.Operations
|
||||
|
||||
import GF.Grammar
|
||||
import GF.Grammar.Lookup
|
||||
|
||||
import Debug.Trace
|
||||
import Data.List(intersperse)
|
||||
import Control.Monad (liftM, liftM2)
|
||||
import GF.Text.Pretty
|
||||
|
||||
-- for debugging
|
||||
tracd m t = t
|
||||
-- tracd = trace
|
||||
|
||||
compute :: SourceGrammar -> Term -> Err Term
|
||||
compute = computeAbsTerm
|
||||
|
||||
computeAbsTerm :: SourceGrammar -> Term -> Err Term
|
||||
computeAbsTerm gr = computeAbsTermIn (lookupAbsDef gr) []
|
||||
|
||||
-- | a hack to make compute work on source grammar as well
|
||||
type LookDef = Ident -> Ident -> Err (Maybe Int,Maybe [Equation])
|
||||
|
||||
computeAbsTermIn :: LookDef -> [Ident] -> Term -> Err Term
|
||||
computeAbsTermIn lookd xs e = errIn (render (text "computing" <+> ppTerm Unqualified 0 e)) $ compt xs e where
|
||||
compt vv t = case t of
|
||||
-- Prod x a b -> liftM2 (Prod x) (compt vv a) (compt (x:vv) b)
|
||||
-- Abs x b -> liftM (Abs x) (compt (x:vv) b)
|
||||
_ -> do
|
||||
let t' = beta vv t
|
||||
(yy,f,aa) <- termForm t'
|
||||
let vv' = map snd yy ++ vv
|
||||
aa' <- mapM (compt vv') aa
|
||||
case look f of
|
||||
Just eqs -> tracd (text "\nmatching" <+> ppTerm Unqualified 0 f) $
|
||||
case findMatch eqs aa' of
|
||||
Ok (d,g) -> do
|
||||
--- let (xs,ts) = unzip g
|
||||
--- ts' <- alphaFreshAll vv' ts
|
||||
let g' = g --- zip xs ts'
|
||||
d' <- compt vv' $ substTerm vv' g' d
|
||||
tracd (text "by Egs:" <+> ppTerm Unqualified 0 d') $ return $ mkAbs yy $ d'
|
||||
_ -> tracd (text "no match" <+> ppTerm Unqualified 0 t') $
|
||||
do
|
||||
let v = mkApp f aa'
|
||||
return $ mkAbs yy $ v
|
||||
_ -> do
|
||||
let t2 = mkAbs yy $ mkApp f aa'
|
||||
tracd (text "not defined" <+> ppTerm Unqualified 0 t2) $ return t2
|
||||
|
||||
look t = case t of
|
||||
(Q (m,f)) -> case lookd m f of
|
||||
Ok (_,md) -> md
|
||||
_ -> Nothing
|
||||
_ -> Nothing
|
||||
|
||||
beta :: [Ident] -> Exp -> Exp
|
||||
beta vv c = case c of
|
||||
Let (x,(_,a)) b -> beta vv $ substTerm vv [(x,beta vv a)] (beta (x:vv) b)
|
||||
App f a ->
|
||||
let (a',f') = (beta vv a, beta vv f) in
|
||||
case f' of
|
||||
Abs _ x b -> beta vv $ substTerm vv [(x,a')] (beta (x:vv) b)
|
||||
_ -> (if a'==a && f'==f then id else beta vv) $ App f' a'
|
||||
Prod b x a t -> Prod b x (beta vv a) (beta (x:vv) t)
|
||||
Abs b x t -> Abs b x (beta (x:vv) t)
|
||||
_ -> c
|
||||
|
||||
-- special version of pattern matching, to deal with comp under lambda
|
||||
|
||||
findMatch :: [([Patt],Term)] -> [Term] -> Err (Term, Substitution)
|
||||
findMatch cases terms = case cases of
|
||||
[] -> Bad $ render (text "no applicable case for" <+> hcat (punctuate comma (map (ppTerm Unqualified 0) terms)))
|
||||
(patts,_):_ | length patts /= length terms ->
|
||||
Bad (render (text "wrong number of args for patterns :" <+>
|
||||
hsep (map (ppPatt Unqualified 0) patts) <+> text "cannot take" <+> hsep (map (ppTerm Unqualified 0) terms)))
|
||||
(patts,val):cc -> case mapM tryMatch (zip patts terms) of
|
||||
Ok substs -> return (tracd (text "value" <+> ppTerm Unqualified 0 val) val, concat substs)
|
||||
_ -> findMatch cc terms
|
||||
|
||||
tryMatch :: (Patt, Term) -> Err [(Ident, Term)]
|
||||
tryMatch (p,t) = do
|
||||
t' <- termForm t
|
||||
trym p t'
|
||||
where
|
||||
|
||||
trym p t' = err (\s -> tracd s (Bad s)) (\t -> tracd (prtm p t) (return t)) $ ----
|
||||
case (p,t') of
|
||||
(PW, _) | notMeta t -> return [] -- optimization with wildcard
|
||||
(PV x, _) | notMeta t -> return [(x,t)]
|
||||
(PString s, ([],K i,[])) | s==i -> return []
|
||||
(PInt s, ([],EInt i,[])) | s==i -> return []
|
||||
(PFloat s,([],EFloat i,[])) | s==i -> return [] --- rounding?
|
||||
(PP (q,p) pp, ([], QC (r,f), tt)) |
|
||||
p `eqStrIdent` f && length pp == length tt -> do
|
||||
matches <- mapM tryMatch (zip pp tt)
|
||||
return (concat matches)
|
||||
(PP (q,p) pp, ([], Q (r,f), tt)) |
|
||||
p `eqStrIdent` f && length pp == length tt -> do
|
||||
matches <- mapM tryMatch (zip pp tt)
|
||||
return (concat matches)
|
||||
(PT _ p',_) -> trym p' t'
|
||||
(PAs x p',_) -> do
|
||||
subst <- trym p' t'
|
||||
return $ (x,t) : subst
|
||||
_ -> Bad (render (text "no match in pattern" <+> ppPatt Unqualified 0 p <+> text "for" <+> ppTerm Unqualified 0 t))
|
||||
|
||||
notMeta e = case e of
|
||||
Meta _ -> False
|
||||
App f a -> notMeta f && notMeta a
|
||||
Abs _ _ b -> notMeta b
|
||||
_ -> True
|
||||
|
||||
prtm p g =
|
||||
ppPatt Unqualified 0 p <+> colon $$ hsep (punctuate semi [ppIdent x <+> char '=' <+> ppTerm Unqualified 0 y | (x,y) <- g])
|
||||
@@ -101,11 +101,11 @@ compileFun gr eval st vs (App e1 e2) h0 bs args =
|
||||
let (h1,bs1,arg,is1) = compileArg gr st vs e2 h0 bs
|
||||
(h2,bs2,is2) = compileFun gr eval st vs e1 h1 bs1 (arg:args)
|
||||
in (h2,bs2,is1++is2)
|
||||
compileFun gr eval st vs (Q (m,id)) h0 bs args =
|
||||
case lookupAbsDef gr m id of
|
||||
compileFun gr eval st vs (Q q@(m,id)) h0 bs args =
|
||||
case lookupAbsDef gr q of
|
||||
Ok (_,Just _)
|
||||
-> (h0,bs,eval st (GLOBAL (showIdent id)) args)
|
||||
_ -> let Ok ty = lookupFunType gr m id
|
||||
_ -> let Ok ty = lookupFunType gr q
|
||||
(ctxt,_,_) = typeForm ty
|
||||
c_arity = length ctxt
|
||||
n_args = length args
|
||||
@@ -164,10 +164,10 @@ compileFun gr eval st vs e@(Glue e1 e2) h0 bs args =
|
||||
in (h1,bs1,[PUSH_ACCUM (LFlt 0)]++is++[POP_ACCUM]++eval (st+1) (ARG_VAR st) [])
|
||||
compileFun gr eval st vs e _ _ _ = error (show e)
|
||||
|
||||
compileArg gr st vs (Q(m,id)) h0 bs =
|
||||
case lookupAbsDef gr m id of
|
||||
compileArg gr st vs (Q q@(m,id)) h0 bs =
|
||||
case lookupAbsDef gr q of
|
||||
Ok (_,Just _) -> (h0,bs,GLOBAL (showIdent id),[])
|
||||
_ -> let Ok ty = lookupFunType gr m id
|
||||
_ -> let Ok ty = lookupFunType gr q
|
||||
(ctxt,_,_) = typeForm ty
|
||||
c_arity = length ctxt
|
||||
in if c_arity == 0
|
||||
@@ -201,17 +201,9 @@ compileArg gr st vs (ImplArg e) h0 bs =
|
||||
compileArg gr st vs e h0 bs
|
||||
compileArg gr st vs e h0 bs =
|
||||
let (f,es) = appForm e
|
||||
isConstr = case f of
|
||||
Q c@(m,id) -> case lookupAbsDef gr m id of
|
||||
Ok (_,Just _) -> Nothing
|
||||
_ -> Just c
|
||||
QC c@(m,id) -> case lookupAbsDef gr m id of
|
||||
Ok (_,Just _) -> Nothing
|
||||
_ -> Just c
|
||||
_ -> Nothing
|
||||
in case isConstr of
|
||||
Just (m,id) ->
|
||||
let Ok ty = lookupFunType gr m id
|
||||
in case f of
|
||||
QC q@(m,id) ->
|
||||
let Ok ty = lookupFunType gr q
|
||||
(ctxt,_,_) = typeForm ty
|
||||
c_arity = length ctxt
|
||||
((h1,bs1,is1),args) = mapAccumL (\(h,bs,is) e -> let (h1,bs1,arg,is1) = compileArg gr st vs e h bs
|
||||
@@ -234,7 +226,7 @@ compileArg gr st vs e h0 bs =
|
||||
EVAL (HEAP h0) (TailCall diff) :
|
||||
[]
|
||||
in (h2,b:bs1,HEAP h1,is1 ++ (PUT_CLOSURE (length bs):is2))
|
||||
Nothing -> compileLambda gr st vs [] e h0 bs
|
||||
_ -> compileLambda gr st vs [] e h0 bs
|
||||
|
||||
compileLambda gr st vs xs (Abs _ x e) h0 bs =
|
||||
compileLambda gr st vs (x:xs) e h0 bs
|
||||
|
||||
@@ -13,7 +13,7 @@ import GF.Grammar.Macros
|
||||
import GF.Grammar.Predef
|
||||
import GF.Grammar.Printer hiding (ppValue)
|
||||
import GF.Text.Pretty hiding (empty)
|
||||
import GF.Compile.Compute.Concrete hiding ( getMeta, setMeta, globals, variants )
|
||||
import GF.Compile.Compute hiding ( getMeta, setMeta, globals, variants )
|
||||
import qualified GF.Text.Pretty as PP
|
||||
import qualified Data.Map as Map
|
||||
import qualified Data.Set as Set
|
||||
@@ -30,7 +30,7 @@ generatePMCFG :: Options -> FilePath -> SourceGrammar -> SourceModule -> Check S
|
||||
generatePMCFG opts cwd gr cmo@(cm,cmi)
|
||||
| mstatus cmi == MSComplete && isModCnc cmi =
|
||||
do let gr' = prependModule gr cmo
|
||||
g = Gl gr' (stdPredef g)
|
||||
g = Gl gr' (stdPredef g) False
|
||||
js <- Map.traverseWithKey (addPMCFG cwd g cmi) (jments cmi)
|
||||
return (cm,cmi{jments = js})
|
||||
| otherwise = return cmo
|
||||
@@ -55,7 +55,7 @@ addPMCFG cwd g cmi id (CncCat mty@(Just (L loc ty)) mdef mref mprn Nothing) = do
|
||||
return (Just (L loc prn))
|
||||
return (CncCat mty mdef mref mprn (Just (defs,refs)))
|
||||
where
|
||||
Gl sgr _ = g
|
||||
Gl sgr _ _ = g
|
||||
addPMCFG cwd g cmi id (CncFun (Just lty@(cats,cat,ctxt,ty)) mlin@(Just (L loc term)) mprn Nothing) = do
|
||||
rules <- checkInModule cwd cmi loc ("Happened in the rule generation for" <+> id) $
|
||||
pmcfgForm g term ctxt ty
|
||||
@@ -66,7 +66,7 @@ addPMCFG cwd g cmi id (CncFun (Just lty@(cats,cat,ctxt,ty)) mlin@(Just (L loc te
|
||||
return (Just (L loc prn))
|
||||
return (CncFun (Just lty) mlin mprn (Just rules))
|
||||
where
|
||||
Gl sgr _ = g
|
||||
Gl sgr _ _ = g
|
||||
|
||||
addPMCFG cwd g cmi id info = return info
|
||||
|
||||
@@ -83,9 +83,9 @@ pmcfgForm g t ctxt ty = do
|
||||
qs <- quantifiers (Map.toList subst)
|
||||
return (Rule qs res_params arg_params lin_idx seq)
|
||||
where
|
||||
Gl sgr _ = g
|
||||
Gl sgr _ _ = g
|
||||
|
||||
quantifiers vars = GenM (\(Gl sgr _) k svs ms ->
|
||||
quantifiers vars = GenM (\(Gl sgr _ _) k svs ms ->
|
||||
k [boundsOf sgr ms variable | (variable,v) <- sortOn snd vars]
|
||||
svs ms)
|
||||
where
|
||||
@@ -216,7 +216,7 @@ breakDown g ms c r rs v (Table p q) fn0 fn = do
|
||||
v2 = VMeta i []
|
||||
v0 = VS v v2 []
|
||||
(c1,c2) = split c
|
||||
Gl gr _ = g
|
||||
Gl gr _ _ = g
|
||||
cnt <- countParamValues gr p
|
||||
(ms,r',fn0,fn) <- mfix $ \(~(_,r',_,_)) ->
|
||||
breakDown g (Map.insert i (Narrowing c1 p) ms) c2 r ((r'-r,(v2,p)):rs) (select v0 v v2) q fn0 fn
|
||||
@@ -480,12 +480,12 @@ getMeta i = GenM $ \_ k svs ms r ->
|
||||
setMeta i st = GenM $ \_ k svs ms ->
|
||||
k () svs (Map.insert i st ms)
|
||||
|
||||
getCnt ty = GenM $ \(Gl gr _) k svs ms r ->
|
||||
getCnt ty = GenM $ \(Gl gr _ _) k svs ms r ->
|
||||
case countParamValues gr ty of
|
||||
Ok c -> k c svs ms r
|
||||
Bad msg -> checkError (pp msg)
|
||||
|
||||
getIdxCnt q = GenM $ \(Gl gr _) k svs ms r ->
|
||||
getIdxCnt q = GenM $ \(Gl gr _ _) k svs ms r ->
|
||||
case lookupOrigInfo gr q of
|
||||
Ok (_,ResValue (L _ ty) idx) ->
|
||||
let (ctxt,QC p) = typeFormCnc ty
|
||||
@@ -495,7 +495,7 @@ getIdxCnt q = GenM $ \(Gl gr _) k svs ms r ->
|
||||
Bad msg -> checkError (pp msg)
|
||||
|
||||
chooseMetaValue :: Choice -> Type -> GenM Value
|
||||
chooseMetaValue s ptyp = GenM $ \g@(Gl gr _) k svs ms r ->
|
||||
chooseMetaValue s ptyp = GenM $ \g@(Gl gr _ _) k svs ms r ->
|
||||
case ptyp of
|
||||
_ | Just n <- isTypeInts ptyp -> foldM (\r i -> k (VInt i) svs ms r) r [0..n]
|
||||
QC c -> do (mod,info) <- lookupOrigInfo gr c
|
||||
|
||||
@@ -9,7 +9,7 @@ import GF.Grammar
|
||||
import GF.Grammar.Lookup(allOrigInfos,lookupOrigInfo)
|
||||
import GF.Infra.Option(Options,noOptions)
|
||||
import GF.Infra.CheckM
|
||||
import GF.Compile.Compute.Concrete
|
||||
import GF.Compile.Compute
|
||||
import qualified Data.Map as Map
|
||||
import qualified Data.Set as Set
|
||||
import Data.Maybe(mapMaybe,fromMaybe)
|
||||
@@ -81,7 +81,7 @@ type QSet = Set.Set (ModuleName,Ident)
|
||||
-- | Generate Canonical GF for the given concrete module.
|
||||
concrete2canonical :: Grammar -> ModuleName -> ModuleName -> ModuleInfo -> Check (QSet,Module)
|
||||
concrete2canonical gr absname cncname modinfo = do
|
||||
let g = Gl gr (stdPredef g)
|
||||
let g = Gl gr (stdPredef g) False
|
||||
infos <- mapM (convInfo g) (allOrigInfos gr cncname)
|
||||
let pts = Set.unions (map fst infos)
|
||||
return (pts,
|
||||
|
||||
@@ -30,7 +30,6 @@ module GF.Compile.Rename (
|
||||
import GF.Infra.Ident
|
||||
import GF.Infra.CheckM
|
||||
import GF.Grammar.Grammar
|
||||
import GF.Grammar.Values
|
||||
import GF.Grammar.Predef
|
||||
import GF.Grammar.Lookup
|
||||
import GF.Grammar.Macros
|
||||
@@ -87,7 +86,7 @@ renameIdentTerm' env@(act,imps) t0 =
|
||||
|
||||
-- this facility is mainly for BWC with GF1: you need not import PredefAbs
|
||||
predefAbs c s
|
||||
| isPredefCat c = return (Q (cPredefAbs,c))
|
||||
| isPredefCat c = return (QC (cPredefAbs,c))
|
||||
| otherwise = checkError s
|
||||
|
||||
ident alt c =
|
||||
@@ -106,6 +105,7 @@ renameIdentTerm' env@(act,imps) t0 =
|
||||
|
||||
info2status :: Maybe ModuleName -> Ident -> Info -> Term
|
||||
info2status mq c i = case i of
|
||||
AbsCat _ -> maybe Con (curry QC) mq c
|
||||
AbsFun _ _ Nothing _ -> maybe Con (curry QC) mq c
|
||||
ResValue _ _ -> maybe Con (curry QC) mq c
|
||||
ResParam _ _ -> maybe Con (curry QC) mq c
|
||||
|
||||
+106
-52
@@ -1,5 +1,10 @@
|
||||
{-# LANGUAGE RankNTypes, CPP, TupleSections, LambdaCase #-}
|
||||
module GF.Compile.TypeCheck.Concrete ( checkLType, checkLType', inferLType, inferLType' ) where
|
||||
module GF.Compile.TypeCheck
|
||||
( checkLType, checkLType'
|
||||
, inferLType, inferLType'
|
||||
, checkContext
|
||||
, checkDef
|
||||
) where
|
||||
|
||||
-- The code here is based on the paper:
|
||||
-- Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich.
|
||||
@@ -11,7 +16,7 @@ import GF.Grammar hiding (Env, VGen, VApp, VRecType, ppValue)
|
||||
import GF.Grammar.Lookup
|
||||
import GF.Grammar.Predef
|
||||
import GF.Grammar.Lockfield
|
||||
import GF.Compile.Compute.Concrete
|
||||
import GF.Compile.Compute
|
||||
import GF.Infra.CheckM
|
||||
import GF.Data.ErrM ( Err(Ok, Bad) )
|
||||
import Control.Applicative(Applicative(..),(<|>))
|
||||
@@ -59,6 +64,42 @@ inferLType' t = do
|
||||
t <- zonkTerm [] t
|
||||
return (t,vty)
|
||||
|
||||
checkContext :: Globals -> Context -> Check Context
|
||||
checkContext g ctxt = do
|
||||
res <- runEvalM g $ check [] unit ctxt
|
||||
case res of
|
||||
[tty] -> return tty
|
||||
_ -> checkError (pp "Encountered variants while type checking")
|
||||
where
|
||||
check scope c [] = return []
|
||||
check scope c ((bt,x,ty):ctxt) = do
|
||||
let (c1,c23) = split c
|
||||
(c2,c3) = split c23
|
||||
(ty,_) <- tcRho scope c1 ty (Just vtypeType)
|
||||
g <- globals
|
||||
ctxt <- check ((x,eval g (scopeEnv scope) c2 ty []):scope) c3 ctxt
|
||||
return ((bt,x,ty):ctxt)
|
||||
|
||||
checkDef :: Globals -> QIdent -> Type -> Equation -> Check Equation
|
||||
checkDef g q ty (ps,t) = do
|
||||
let (c1,c23) = split unit
|
||||
(c2,c3) = split c23
|
||||
res <- runEvalM g $ do
|
||||
(scope,ty) <- go [] c1 (eval g [] c2 ty []) ps
|
||||
(t,_) <- tcRho scope c3 t (Just ty)
|
||||
return (ps,t)
|
||||
case res of
|
||||
[eq] -> return eq
|
||||
_ -> checkError (pp "Encountered variants while type checking")
|
||||
where
|
||||
go scope c ty [] = return (scope,ty)
|
||||
go scope c ty (p:ps) = do (_,_,arg_ty,res_ty) <- unifyFun scope ty
|
||||
let (c1,c2) = split c
|
||||
(scope,arg_ty) <- tcPatt scope c1 p (Just arg_ty)
|
||||
go scope c2 res_ty ps
|
||||
|
||||
-- tcPatt scope c PW Nothing = do
|
||||
|
||||
inferSigma :: Scope -> Choice -> Term -> EvalM (Term,Sigma)
|
||||
inferSigma scope s t = do -- GEN1
|
||||
(t,ty) <- tcRho scope s t Nothing
|
||||
@@ -195,15 +236,15 @@ tcRho scope c (Typed body ann_ty) mb_ty = do -- ANNOT
|
||||
let v_ann_ty = eval g (scopeEnv scope) c2 ann_ty []
|
||||
(body,_) <- tcRho scope c3 body (Just v_ann_ty)
|
||||
instSigma scope c4 (Typed body ann_ty) v_ann_ty mb_ty
|
||||
tcRho scope c (FV ts) mb_ty = do
|
||||
tcRho scope c (FV ts) mb_ty = concreteOnly "Variants" $ do
|
||||
(ts,ty) <- tcUnifying scope c ts mb_ty
|
||||
return (FV ts, ty)
|
||||
tcRho scope s t@(Sort _) mb_ty = do
|
||||
instSigma scope s t vtypeType mb_ty
|
||||
tcRho scope c t@(RecType rs) Nothing = do
|
||||
tcRho scope c t@(RecType rs) Nothing = concreteOnly "Record types" $ do
|
||||
(rs,mb_ty) <- tcRecTypeFields scope c rs Nothing
|
||||
return (RecType rs,fromMaybe vtypePType mb_ty)
|
||||
tcRho scope c t@(RecType rs) (Just ty) = do
|
||||
tcRho scope c t@(RecType rs) (Just ty) = concreteOnly "Record types" $ do
|
||||
(scope,f,ty') <- skolemise scope ty
|
||||
case ty' of
|
||||
VSort s
|
||||
@@ -217,7 +258,7 @@ tcRho scope c t@(RecType rs) (Just ty) = do
|
||||
"cannot be of type" <+> ppTerm Unqualified 0 ty)
|
||||
(rs,mb_ty) <- tcRecTypeFields scope c rs (Just ty')
|
||||
return (f (RecType rs),ty)
|
||||
tcRho scope s t@(Table p res) mb_ty = do
|
||||
tcRho scope s t@(Table p res) mb_ty = concreteOnly "Tables" $ do
|
||||
let (s1,s23) = split s
|
||||
(s2,s3) = split s23
|
||||
(p, p_ty) <- tcRho scope s1 p (Just vtypePType)
|
||||
@@ -240,7 +281,7 @@ tcRho scope c (S t p) mb_ty = do
|
||||
(t,t_ty) <- tcRho scope c1 t (Just t_ty)
|
||||
(p,_) <- tcRho scope c2 p (Just p_ty)
|
||||
return (S t p, res_ty)
|
||||
tcRho scope c (T tt ps) Nothing = do -- ABS1/AABS1 for tables
|
||||
tcRho scope c (T tt ps) Nothing = concreteOnly "Tables" $ do -- ABS1/AABS1 for tables
|
||||
let (c1,c2) = split c
|
||||
mb_p_ty <- case tt of
|
||||
TRaw -> return Nothing
|
||||
@@ -251,7 +292,7 @@ tcRho scope c (T tt ps) Nothing = do -- ABS1/AABS1 for
|
||||
(ps,p_ty,res_ty) <- tcCases scope c2 ps mb_p_ty Nothing
|
||||
p_ty_t <- value2termM True [] p_ty
|
||||
return (T (TTyped p_ty_t) ps, VTable p_ty res_ty)
|
||||
tcRho scope c (T tt ps) (Just ty) = do -- ABS2/AABS2 for tables
|
||||
tcRho scope c (T tt ps) (Just ty) = concreteOnly "Tables" $ do -- ABS2/AABS2 for tables
|
||||
let (c12,c34) = split c
|
||||
(c3,c4) = split c34
|
||||
(scope,f,ty') <- skolemise scope ty
|
||||
@@ -266,7 +307,7 @@ tcRho scope c (T tt ps) (Just ty) = do -- ABS2/AABS2 for
|
||||
(ps,p_ty,res_ty) <- tcCases scope c3 ps (Just p_ty) (Just res_ty)
|
||||
p_ty_t <- value2termM True (scopeVars scope) p_ty
|
||||
return (f (T (TTyped p_ty_t) ps), VTable p_ty res_ty)
|
||||
tcRho scope c (V p_ty ts) Nothing = do
|
||||
tcRho scope c (V p_ty ts) Nothing = concreteOnly "Tables" $ do
|
||||
let (c1,c2,c3,c4) = split4 c
|
||||
(p_ty, _) <- tcRho scope c1 p_ty (Just vtypeType)
|
||||
i <- newResiduation scope
|
||||
@@ -279,7 +320,7 @@ tcRho scope c (V p_ty ts) Nothing = do
|
||||
ts <- mapCM go c2 ts
|
||||
g <- globals
|
||||
return (V p_ty ts, VTable (eval g (scopeEnv scope) c3 p_ty []) res_ty)
|
||||
tcRho scope c (V p_ty0 ts) (Just ty) = do
|
||||
tcRho scope c (V p_ty0 ts) (Just ty) = concreteOnly "Tables" $ do
|
||||
let (c1,c2,c3,c4) = split4 c
|
||||
(scope,f,ty') <- skolemise scope ty
|
||||
(p_ty, res_ty) <- unifyTbl scope ty'
|
||||
@@ -289,13 +330,13 @@ tcRho scope c (V p_ty0 ts) (Just ty) = do
|
||||
unify scope p_ty p_vty0
|
||||
ts <- mapCM (\c t -> fmap fst $ tcRho scope c t (Just res_ty)) c3 ts
|
||||
return (V p_ty0 ts, VTable p_ty res_ty)
|
||||
tcRho scope c (R rs) Nothing = do
|
||||
tcRho scope c (R rs) Nothing = concreteOnly "Records" $ do
|
||||
lttys <- inferRecFields scope c [] rs
|
||||
rs <- mapM (\(l,t,ty) -> value2termM True (scopeVars scope) ty >>= \ty -> return (l, (Just ty, t))) lttys
|
||||
return (R rs,
|
||||
VRecType [(l,True,ty) | (l,t,ty) <- lttys] False
|
||||
)
|
||||
tcRho scope c (R rs) (Just ty) = do
|
||||
tcRho scope c (R rs) (Just ty) = concreteOnly "Records" $ do
|
||||
(scope,f,ty') <- skolemise scope ty
|
||||
case ty' of
|
||||
(VRecType ltys _)->do lttys <- checkRecFields scope c rs [] ltys
|
||||
@@ -315,12 +356,12 @@ tcRho scope c (P t l) mb_ty = do
|
||||
return (VMeta i [])
|
||||
(t,t_ty) <- tcRho scope c t (Just (VRecType [(l,True,l_ty)] True))
|
||||
return (P t l,l_ty)
|
||||
tcRho scope c (C t1 t2) mb_ty = do
|
||||
tcRho scope c (C t1 t2) mb_ty = concreteOnly "String operations" $ do
|
||||
let (c1,c2,c3,c4) = split4 c
|
||||
(t1,t1_ty) <- tcRho scope c1 t1 (Just vtypeStr)
|
||||
(t2,t2_ty) <- tcRho scope c2 t2 (Just vtypeStr)
|
||||
instSigma scope c3 (C t1 t2) vtypeStr mb_ty
|
||||
tcRho scope c (Glue t1 t2) mb_ty = do
|
||||
tcRho scope c (Glue t1 t2) mb_ty = concreteOnly "String operations" $ do
|
||||
let (c1,c2,c3,c4) = split4 c
|
||||
(t1,t1_ty) <- tcRho scope c1 t1 (Just vtypeStr)
|
||||
(t2,t2_ty) <- tcRho scope c2 t2 (Just vtypeStr)
|
||||
@@ -417,7 +458,7 @@ tcRho scope c (ELin cat t) mb_ty = do -- this could be done earlier, i.e. in th
|
||||
tcRho scope c (ExtR t (R [(lockLabel cat,(Just (RecType []),R []))])) mb_ty
|
||||
tcRho scope c (ELincat cat t) mb_ty = do -- this could be done earlier, i.e. in the parser
|
||||
tcRho scope c (ExtR t (RecType [(lockLabel cat,[],RecType [])])) mb_ty
|
||||
tcRho scope c (Alts t ss) mb_ty = do
|
||||
tcRho scope c (Alts t ss) mb_ty = concreteOnly "String operations" $ do
|
||||
let (c1,c2,c3,c4) = split4 c
|
||||
(t,_) <- tcRho scope c1 t (Just vtypeStr)
|
||||
ss <- mapCM (\c (t1,t2) -> do
|
||||
@@ -427,17 +468,17 @@ tcRho scope c (Alts t ss) mb_ty = do
|
||||
return (t1,t2))
|
||||
c2 ss
|
||||
instSigma scope c3 (Alts t ss) vtypeStr mb_ty
|
||||
tcRho scope c (Strs ss) mb_ty = do
|
||||
tcRho scope c (Strs ss) mb_ty = concreteOnly "String operations" $ do
|
||||
let (c1,c2) = split c
|
||||
ss <- mapCM (\c t -> do (t,_) <- tcRho scope c t (Just vtypeStr)
|
||||
return t)
|
||||
c1 ss
|
||||
instSigma scope c2 (Strs ss) vtypeStrs mb_ty
|
||||
tcRho scope c (EPattType ty) mb_ty = do
|
||||
tcRho scope c (EPattType ty) mb_ty = concreteOnly "Pattern types" $ do
|
||||
let (c1,c2) = split c
|
||||
(ty, _) <- tcRho scope c1 ty (Just vtypeType)
|
||||
instSigma scope c2 (EPattType ty) vtypeType mb_ty
|
||||
tcRho scope c t@(EPatt _ _ p) mb_ty = do
|
||||
tcRho scope c t@(EPatt _ _ p) mb_ty = concreteOnly "Patterns" $ do
|
||||
(scope,f,mb_ty) <- case mb_ty of
|
||||
Nothing -> return (scope,id,Nothing)
|
||||
Just ty -> do (scope,f,ty) <- skolemise scope ty
|
||||
@@ -447,7 +488,7 @@ tcRho scope c t@(EPatt _ _ p) mb_ty = do
|
||||
(_,ty) <- tcPatt scope c p mb_ty
|
||||
(min,max,p) <- measurePatt p
|
||||
return (f (EPatt min max p), VPattType ty)
|
||||
tcRho scope c (Markup tag attrs children) mb_ty = do
|
||||
tcRho scope c (Markup tag attrs children) mb_ty = concreteOnly "Markups" $ do
|
||||
let (c1,c2,c3,c4) = split4 c
|
||||
attrs <- mapCM (\c (id,t) -> do
|
||||
(t,_) <- tcRho scope c t Nothing
|
||||
@@ -456,7 +497,7 @@ tcRho scope c (Markup tag attrs children) mb_ty = do
|
||||
res <- mapCM (\c (L loc child) -> fmap (L loc . fst) (tcRho scope c child Nothing)) c2 children
|
||||
instSigma scope c3 (Markup tag attrs res) vtypeMarkup mb_ty
|
||||
tcRho scope c (Reset ctl mb_ct t qid) mb_ty
|
||||
| ctl == cConcat || ctl == cConcat' = do
|
||||
| ctl == cConcat || ctl == cConcat' = concreteOnly "Control operators" $ do
|
||||
let (c1,c23) = split c
|
||||
(c2,c3 ) = split c23
|
||||
(t,_) <- tcRho scope c1 t Nothing
|
||||
@@ -465,7 +506,7 @@ tcRho scope c (Reset ctl mb_ct t qid) mb_ty
|
||||
return (Just ct)
|
||||
Nothing -> return Nothing
|
||||
instSigma scope c2 (Reset ctl mb_ct t qid) vtypeMarkup mb_ty
|
||||
| ctl == cOne = do
|
||||
| ctl == cOne = concreteOnly "Control operators" $ do
|
||||
let (c1,c2) = split c
|
||||
(t,ty) <- tcRho scope c1 t mb_ty
|
||||
(mb_ct,ty) <- case mb_ct of
|
||||
@@ -473,7 +514,7 @@ tcRho scope c (Reset ctl mb_ct t qid) mb_ty
|
||||
return (Just ct,ty)
|
||||
Nothing -> return (Nothing,ty)
|
||||
return (Reset ctl mb_ct t qid,ty)
|
||||
| ctl == cSelect = do
|
||||
| ctl == cSelect = concreteOnly "Control operators" $ do
|
||||
let (c1,c2) = split c
|
||||
ty <- case mb_ty of
|
||||
Just ty -> return ty
|
||||
@@ -488,7 +529,7 @@ tcRho scope c (Reset ctl mb_ct t qid) mb_ty
|
||||
Nothing -> evalError (pp "[select: .. | ..] requires an integer argument")
|
||||
(t,_) <- tcRho scope c1 t (Just rec_ty)
|
||||
return (Reset ctl mb_ct t qid,ty)
|
||||
| ctl == cFilter = do
|
||||
| ctl == cFilter = concreteOnly "Control operators" $ do
|
||||
ty <- case mb_ty of
|
||||
Just ty -> return ty
|
||||
Nothing -> do i <- newResiduation scope
|
||||
@@ -501,7 +542,7 @@ tcRho scope c (Reset ctl mb_ct t qid) mb_ty
|
||||
Nothing -> return ()
|
||||
(t,_) <- tcRho scope c t (Just rec_ty)
|
||||
return (Reset ctl mb_ct t qid,ty)
|
||||
| ctl == cDefault = do
|
||||
| ctl == cDefault = concreteOnly "Control operators" $ do
|
||||
let (c1,c2) = split c
|
||||
(t,ty) <- tcRho scope c1 t mb_ty
|
||||
(mb_ct,ty) <- case mb_ct of
|
||||
@@ -509,7 +550,7 @@ tcRho scope c (Reset ctl mb_ct t qid) mb_ty
|
||||
return (Just ct,ty)
|
||||
Nothing -> evalError (pp "[list: .. | ..] requires an argument")
|
||||
return (Reset ctl mb_ct t qid,ty)
|
||||
| ctl == cList = do
|
||||
| ctl == cList = concreteOnly "Control operators" $ do
|
||||
do let (c1,c2) = split c
|
||||
mb_ct <- case mb_ct of
|
||||
Just ct -> do (ct,ty) <- tcRho scope c1 ct Nothing
|
||||
@@ -519,7 +560,7 @@ tcRho scope c (Reset ctl mb_ct t qid) mb_ty
|
||||
case ty of
|
||||
VApp c qid [] -> return (Reset ctl mb_ct t (Just qid), ty)
|
||||
_ -> evalError (pp "Needs atomic type"<+>ppValue Unqualified 0 ty)
|
||||
| ctl == cLen = do
|
||||
| ctl == cLen = concreteOnly "Control operators" $ do
|
||||
do let (c1,c2) = split c
|
||||
(t,_) <- tcRho scope c1 t Nothing
|
||||
case mb_ct of
|
||||
@@ -530,7 +571,7 @@ tcRho scope c (Reset ctl mb_ct t qid) mb_ty
|
||||
(ct,_) <- tcRho scope c2 ct (Just (VProd Explicit identW vtypeInt res_ty))
|
||||
return (Reset ctl (Just ct) t Nothing, res_ty)
|
||||
Nothing -> instSigma scope c2 (Reset ctl Nothing t Nothing) vtypeInt mb_ty
|
||||
| ctl == cConst = do
|
||||
| ctl == cConst = concreteOnly "Control operators" $ do
|
||||
let (c1,c2) = split c
|
||||
(t,_) <- tcRho scope c1 t Nothing
|
||||
(mb_ct,ty) <- case mb_ct of
|
||||
@@ -538,8 +579,8 @@ tcRho scope c (Reset ctl mb_ct t qid) mb_ty
|
||||
return (Just ct,ty)
|
||||
Nothing -> evalError (pp "[list: .. | ..] requires an argument")
|
||||
return (Reset ctl mb_ct t qid,ty)
|
||||
| otherwise = evalError (pp "Operator" <+> pp ctl <+> pp "is not defined")
|
||||
tcRho scope s (Opts n cs) mb_ty = do
|
||||
| otherwise = concreteOnly "Control operators" $ evalError (pp "Operator" <+> pp ctl <+> pp "is not defined")
|
||||
tcRho scope s (Opts n cs) mb_ty = concreteOnly "Options" $ do
|
||||
let (s1,s2,s3) = split3 s
|
||||
(n,_) <- tcRho scope s1 n Nothing
|
||||
(ls,_) <- tcUnifyingMaybe scope s2 (fst <$> cs) Nothing
|
||||
@@ -547,6 +588,12 @@ tcRho scope s (Opts n cs) mb_ty = do
|
||||
return (Opts n (zip ls ts), ty)
|
||||
tcRho scope s t _ = unimplemented ("tcRho "++show t)
|
||||
|
||||
concreteOnly msg f = do
|
||||
(Gl _ _ isAbstract) <- globals
|
||||
if isAbstract
|
||||
then evalError (pp (msg ++ " are not supported in the abstract syntax"))
|
||||
else f
|
||||
|
||||
evalCodomain :: Ident -> Value -> Value -> EvalM Value
|
||||
evalCodomain x v (VClosure env c ty) = do
|
||||
g <- globals
|
||||
@@ -594,8 +641,8 @@ tcCases scope c ((p,t):cs) mb_p_ty mb_res_ty = do
|
||||
return ((p,t):cs,p_ty,res_ty)
|
||||
|
||||
tcApp scope c t0 (App fun arg) args mb_ty = tcApp scope c t0 fun (arg:args) mb_ty -- APP
|
||||
tcApp scope c t0 t@(Q id) args mb_ty = resolveOverloads scope c t0 id args mb_ty -- VAR (global)
|
||||
tcApp scope c t0 t@(QC id) args mb_ty = resolveOverloads scope c t0 id args mb_ty -- VAR (global)
|
||||
tcApp scope c t0 t@(Q q) args mb_ty = resolveOverloads scope c t0 q args mb_ty -- VAR (global)
|
||||
tcApp scope c t0 t@(QC q) args mb_ty = resolveOverloads scope c t0 q args mb_ty -- VAR (global)
|
||||
tcApp scope c t0 t args mb_ty = do
|
||||
let (c1,c23) = split c
|
||||
let (c2,c3) = split c23
|
||||
@@ -626,22 +673,29 @@ reapply1 scope c fun fun_ty (arg:args) = do -- Explicit arg (fallthrough) case
|
||||
|
||||
resolveOverloads :: Scope -> Choice -> Term -> QIdent -> [Term] -> Maybe Rho -> EvalM (Term,Rho)
|
||||
resolveOverloads scope c t0 q args mb_ty = do
|
||||
g@(Gl gr _) <- globals
|
||||
case lookupOverloadTypes gr q of
|
||||
Bad msg -> evalError (pp msg)
|
||||
Ok [(t,ty)] -> do let (c1,c23) = split c
|
||||
(c2,c3) = split c23
|
||||
(t,ty) <- reapply1 scope c1 t (eval g [] c2 ty []) args
|
||||
instSigma scope c3 t ty mb_ty
|
||||
Ok ttys0 -> do let (c1,c23) = split c
|
||||
(c2,c3) = split c23
|
||||
sz <- checkpoint
|
||||
arg_tys <- mapCM (checkArg g) c1 args
|
||||
let v_ttys = mapC (\c (t,ty) -> (t,eval g [] c ty [])) c2 ttys0
|
||||
try sz
|
||||
(\(fun,fun_ty) -> reapply2 scope c3 fun fun_ty arg_tys mb_ty)
|
||||
(\ttys -> fmap (\(ts,ty) -> (mkFV ts,ty)) (snd (minimum g ttys0 arg_tys ttys)))
|
||||
v_ttys
|
||||
g@(Gl gr _ isAbstract) <- globals
|
||||
if isAbstract
|
||||
then case lookupAbsType gr q of
|
||||
Bad msg -> evalError (pp msg)
|
||||
Ok ty -> do let (c1,c23) = split c
|
||||
(c2,c3) = split c23
|
||||
(t,ty) <- reapply1 scope c1 t0 (eval g [] c2 ty []) args
|
||||
instSigma scope c3 t ty mb_ty
|
||||
else case lookupOverloadTypes gr q of
|
||||
Bad msg -> evalError (pp msg)
|
||||
Ok [(t,ty)] -> do let (c1,c23) = split c
|
||||
(c2,c3) = split c23
|
||||
(t,ty) <- reapply1 scope c1 t (eval g [] c2 ty []) args
|
||||
instSigma scope c3 t ty mb_ty
|
||||
Ok ttys0 -> do let (c1,c23) = split c
|
||||
(c2,c3) = split c23
|
||||
sz <- checkpoint
|
||||
arg_tys <- mapCM (checkArg g) c1 args
|
||||
let v_ttys = mapC (\c (t,ty) -> (t,eval g [] c ty [])) c2 ttys0
|
||||
try sz
|
||||
(\(fun,fun_ty) -> reapply2 scope c3 fun fun_ty arg_tys mb_ty)
|
||||
(\ttys -> fmap (\(ts,ty) -> (mkFV ts,ty)) (snd (minimum g ttys0 arg_tys ttys)))
|
||||
v_ttys
|
||||
where
|
||||
checkArg g c (ImplArg arg) = do
|
||||
let (c1,c2) = split c
|
||||
@@ -722,8 +776,8 @@ tcPatt scope c (PV x) Nothing = do
|
||||
tcPatt scope c (PV x) (Just ty) =
|
||||
return ((x,ty):scope,ty)
|
||||
tcPatt scope c (PP q ps) mb_ty = do
|
||||
g@(Gl gr _) <- globals
|
||||
ty <- case lookupResType gr q of
|
||||
g@(Gl gr _ isAbstract) <- globals
|
||||
ty <- case (if isAbstract then lookupFunType else lookupResType) gr q of
|
||||
Ok ty -> return ty
|
||||
Bad msg -> evalError (pp msg)
|
||||
let go scope c ty [] = return (scope,ty)
|
||||
@@ -839,7 +893,7 @@ tcPatt scope c (PAlt p1 p2) mb_ty = do
|
||||
(_,ty) <- tcPatt scope c2 p2 (Just ty)
|
||||
return (scope,ty)
|
||||
tcPatt scope c (PM q) mb_ty = do
|
||||
g@(Gl gr _) <- globals
|
||||
g@(Gl gr _ _) <- globals
|
||||
ty <- case lookupResType gr q of
|
||||
Ok ty -> return ty
|
||||
Bad msg -> evalError (pp msg)
|
||||
@@ -1344,8 +1398,8 @@ unify scope (VStr s1) (VStr s2)
|
||||
| s1 == s2 = return ()
|
||||
unify scope VEmpty VEmpty = return ()
|
||||
unify scope v1 v2 =
|
||||
evalError ("Cannot unify:" <+> ppValue Qualified 0 v1 $$
|
||||
" with:" <+> ppValue Qualified 0 v2)
|
||||
evalError ("Cannot unify:" <+> ppValue Unqualified 0 v1 $$
|
||||
" with:" <+> ppValue Unqualified 0 v2)
|
||||
|
||||
|
||||
-- | Invariant: tv1 is a flexible type variable
|
||||
@@ -1,82 +0,0 @@
|
||||
----------------------------------------------------------------------
|
||||
-- |
|
||||
-- Module : TypeCheck
|
||||
-- Maintainer : AR
|
||||
-- Stability : (stable)
|
||||
-- Portability : (portable)
|
||||
--
|
||||
-- > CVS $Date: 2005/09/15 16:22:02 $
|
||||
-- > CVS $Author: aarne $
|
||||
-- > CVS $Revision: 1.16 $
|
||||
--
|
||||
-- (Description of the module)
|
||||
-----------------------------------------------------------------------------
|
||||
|
||||
module GF.Compile.TypeCheck.Abstract (-- * top-level type checking functions; TC should not be called directly.
|
||||
checkContext,
|
||||
checkTyp,
|
||||
checkDef,
|
||||
checkConstrs,
|
||||
) where
|
||||
|
||||
import GF.Data.Operations
|
||||
|
||||
import GF.Infra.CheckM
|
||||
import GF.Grammar
|
||||
import GF.Grammar.Lookup
|
||||
import GF.Grammar.Unify
|
||||
--import GF.Compile.Refresh
|
||||
--import GF.Compile.Compute.Abstract
|
||||
import GF.Compile.TypeCheck.TC
|
||||
|
||||
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)
|
||||
|
||||
-- interface to TC type checker
|
||||
|
||||
type2val :: Type -> Val
|
||||
type2val = VClos []
|
||||
|
||||
cont2exp :: Context -> Term
|
||||
cont2exp c = mkProd c eType [] -- to check a context
|
||||
|
||||
cont2val :: Context -> Val
|
||||
cont2val = type2val . cont2exp
|
||||
|
||||
-- some top-level batch-mode checkers for the compiler
|
||||
|
||||
justTypeCheck :: SourceGrammar -> Term -> Val -> Err Constraints
|
||||
justTypeCheck gr e v = do
|
||||
(_,constrs0) <- checkExp (grammar2theory gr) (initTCEnv []) e v
|
||||
(constrs1,_) <- unifyVal constrs0
|
||||
return $ filter notJustMeta constrs1
|
||||
|
||||
notJustMeta (c,k) = case (c,k) of
|
||||
(VClos g1 (Meta m1), VClos g2 (Meta m2)) -> False
|
||||
_ -> True
|
||||
|
||||
grammar2theory :: SourceGrammar -> Theory
|
||||
grammar2theory gr (m,f) = case lookupFunType gr m f of
|
||||
Ok t -> return $ type2val t
|
||||
Bad s -> case lookupCatContext gr m f of
|
||||
Ok cont -> return $ cont2val cont
|
||||
_ -> Bad s
|
||||
|
||||
checkContext :: SourceGrammar -> Context -> [Message]
|
||||
checkContext st = checkTyp st . cont2exp
|
||||
|
||||
checkTyp :: SourceGrammar -> Type -> [Message]
|
||||
checkTyp gr typ = err (\x -> [pp x]) ppConstrs $ justTypeCheck gr typ vType
|
||||
|
||||
checkDef :: SourceGrammar -> Fun -> Type -> Equation -> [Message]
|
||||
checkDef gr (m,fun) typ eq = err (\x -> [pp x]) ppConstrs $ do
|
||||
(b,cs) <- checkBranch (grammar2theory gr) (initTCEnv []) eq (type2val typ)
|
||||
(constrs,_) <- unifyVal cs
|
||||
return $ filter notJustMeta constrs
|
||||
|
||||
checkConstrs :: SourceGrammar -> Cat -> [Ident] -> [String]
|
||||
checkConstrs gr cat _ = [] ---- check constructors!
|
||||
@@ -1,324 +0,0 @@
|
||||
----------------------------------------------------------------------
|
||||
-- |
|
||||
-- Module : TC
|
||||
-- Maintainer : AR
|
||||
-- Stability : (stable)
|
||||
-- Portability : (portable)
|
||||
--
|
||||
-- > 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
|
||||
|
||||
import GF.Data.Operations
|
||||
import GF.Grammar
|
||||
import GF.Grammar.Predef
|
||||
|
||||
import Control.Monad
|
||||
--import Data.List (sortBy)
|
||||
import Data.Maybe
|
||||
import GF.Text.Pretty
|
||||
|
||||
data AExp =
|
||||
AVr Ident Val
|
||||
| ACn QIdent Val
|
||||
| AType
|
||||
| AInt Integer
|
||||
| AFloat Double
|
||||
| AStr String
|
||||
| AMeta MetaId Val
|
||||
| ALet (Ident,(Val,AExp)) AExp
|
||||
| AApp AExp AExp Val
|
||||
| AAbs Ident Val AExp
|
||||
| AProd Ident AExp AExp
|
||||
-- -- | AEqs [([Exp],AExp)] --- not used
|
||||
| ARecType [ALabelling]
|
||||
| AR [AAssign]
|
||||
| AP AExp Label Val
|
||||
| AGlue AExp AExp
|
||||
| AData Val
|
||||
deriving (Eq,Show)
|
||||
|
||||
type ALabelling = (Label, AExp)
|
||||
type AAssign = (Label, (Val, AExp))
|
||||
|
||||
type Theory = QIdent -> Err Val
|
||||
|
||||
lookupConst :: Theory -> QIdent -> Err Val
|
||||
lookupConst th f = th f
|
||||
|
||||
lookupVar :: Env -> Ident -> Err Val
|
||||
lookupVar g x = maybe (Bad (render ("unknown variable" <+> x))) return $ lookup x ((identW,VClos [] (Meta 0)):g)
|
||||
-- wild card IW: no error produced, ?0 instead.
|
||||
|
||||
type TCEnv = (Int,Env,Env)
|
||||
|
||||
--emptyTCEnv :: TCEnv
|
||||
--emptyTCEnv = (0,[],[])
|
||||
|
||||
whnf :: Val -> Err Val
|
||||
whnf v = ---- errIn ("whnf" +++ prt v) $ ---- debug
|
||||
case v of
|
||||
VApp u w -> do
|
||||
u' <- whnf u
|
||||
w' <- whnf w
|
||||
app u' w'
|
||||
VClos env e -> eval env e
|
||||
_ -> return v
|
||||
|
||||
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) $
|
||||
case e of
|
||||
Vr x -> lookupVar env x
|
||||
Q c -> return $ VCn c
|
||||
QC c -> return $ VCn c ---- == Q ?
|
||||
Sort c -> return $ VType --- the only sort is Type
|
||||
App f a -> join $ liftM2 app (eval env f) (eval env a)
|
||||
RecType xs -> do xs <- mapM (\(l,_,e) -> eval env e >>= \e -> return (l,e)) xs
|
||||
return (VRecType xs)
|
||||
_ -> return $ VClos env e
|
||||
|
||||
eqVal :: Int -> Val -> Val -> Err [(Val,Val)]
|
||||
eqVal k u1 u2 = ---- errIn (prt u1 +++ "<>" +++ prBracket (show k) +++ prt u2) $
|
||||
do
|
||||
w1 <- whnf u1
|
||||
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 (++)
|
||||
(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]
|
||||
--- thus ignore qualifications; valid because inheritance cannot
|
||||
--- be qualified. Simplifies annotation. AR 17/3/2005
|
||||
_ -> return [(w1,w2) | w1 /= w2]
|
||||
-- invariant: constraints are in whnf
|
||||
|
||||
checkType :: Theory -> TCEnv -> Term -> Err (AExp,[(Val,Val)])
|
||||
checkType th tenv e = checkExp th tenv e vType
|
||||
|
||||
checkExp :: Theory -> TCEnv -> Term -> Val -> Err (AExp, [(Val,Val)])
|
||||
checkExp th tenv@(k,rho,gamma) e ty = do
|
||||
typ <- whnf ty
|
||||
let v = VGen k
|
||||
case e of
|
||||
Meta m -> return $ (AMeta m typ,[])
|
||||
|
||||
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)
|
||||
_ -> Bad (render ("function type expected for" <+> ppTerm Unqualified 0 e <+> "instead of" <+> ppValue Unqualified 0 typ))
|
||||
|
||||
Let (x, (mb_typ, e1)) e2 -> do
|
||||
(val,e1,cs1) <- case mb_typ of
|
||||
Just typ -> do (_,cs1) <- checkType th tenv typ
|
||||
val <- eval rho typ
|
||||
(e1,cs2) <- checkExp th tenv e1 val
|
||||
return (val,e1,cs1++cs2)
|
||||
Nothing -> do (e1,val,cs) <- inferExp th tenv e1
|
||||
return (val,e1,cs)
|
||||
(e2,cs2) <- checkExp th (k,rho,(x,val):gamma) e2 typ
|
||||
return (ALet (x,(val,e1)) e2, cs1++cs2)
|
||||
|
||||
Prod _ x a b -> do
|
||||
testErr (typ == vType) "expected Type"
|
||||
(a',csa) <- checkType th tenv a
|
||||
(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 ->
|
||||
case typ of
|
||||
VRecType ys -> do case [l | (l,_) <- ys, isNothing (lookup l xs)] of
|
||||
[] -> return ()
|
||||
ls -> fail (render ("no value given for label:" <+> fsep (punctuate ',' ls)))
|
||||
r <- mapM (checkAssign th tenv ys) xs
|
||||
let (xs,css) = unzip r
|
||||
return (AR xs, concat css)
|
||||
_ -> Bad (render ("record type expected for" <+> ppTerm Unqualified 0 e <+> "instead of" <+> ppValue Unqualified 0 typ))
|
||||
|
||||
P r l -> do (r',cs) <- checkExp th tenv r (VRecType [(l,typ)])
|
||||
return (AP r' l typ,cs)
|
||||
|
||||
Glue x y -> do cs1 <- eqVal k valAbsFloat typ
|
||||
(x,cs2) <- checkExp th tenv x typ
|
||||
(y,cs3) <- checkExp th tenv y typ
|
||||
return (AGlue x y,cs1++cs2++cs3)
|
||||
_ -> checkInferExp th tenv e typ
|
||||
|
||||
checkInferExp :: Theory -> TCEnv -> Term -> Val -> Err (AExp, [(Val,Val)])
|
||||
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
|
||||
Q (m,c) | m == cPredefAbs && isPredefCat c
|
||||
-> return (ACn (m,c) vType, vType, [])
|
||||
| otherwise -> mkAnnot (ACn (m,c)) $ noConstr $ lookupConst th (m,c)
|
||||
QC c -> mkAnnot (ACn c) $ noConstr $ lookupConst th c ----
|
||||
EInt i -> return (AInt i, valAbsInt, [])
|
||||
EFloat i -> return (AFloat i, valAbsFloat, [])
|
||||
K i -> return (AStr i, valAbsString, [])
|
||||
Sort _ -> return (AType, vType, [])
|
||||
RecType xs -> do r <- mapM (checkLabelling th tenv) xs
|
||||
let (xs,css) = unzip r
|
||||
return (ARecType xs, vType, concat css)
|
||||
Let (x, (mb_typ, e1)) e2 -> do
|
||||
(val1,e1,cs1) <- case mb_typ of
|
||||
Just typ -> do (_,cs1) <- checkType th tenv typ
|
||||
val <- eval rho typ
|
||||
(e1,cs2) <- checkExp th tenv e1 val
|
||||
return (val,e1,cs1++cs2)
|
||||
Nothing -> do (e1,val,cs) <- inferExp th tenv e1
|
||||
return (val,e1,cs)
|
||||
(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
|
||||
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)
|
||||
_ -> 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))
|
||||
|
||||
checkLabelling :: Theory -> TCEnv -> Labelling -> Err (ALabelling, [(Val,Val)])
|
||||
checkLabelling th tenv (lbl,_,typ) = do
|
||||
(atyp,cs) <- checkType th tenv typ
|
||||
return ((lbl,atyp),cs)
|
||||
|
||||
checkAssign :: Theory -> TCEnv -> [(Label,Val)] -> Assign -> Err (AAssign, [(Val,Val)])
|
||||
checkAssign th tenv@(k,rho,gamma) typs (lbl,(Just typ,exp)) = do
|
||||
(atyp,cs1) <- checkType th tenv typ
|
||||
val <- eval rho typ
|
||||
cs2 <- case lookup lbl typs of
|
||||
Nothing -> return []
|
||||
Just val0 -> eqVal k val val0
|
||||
(aexp,cs3) <- checkExp th tenv exp val
|
||||
return ((lbl,(val,aexp)),cs1++cs2++cs3)
|
||||
checkAssign th tenv@(k,rho,gamma) typs (lbl,(Nothing,exp)) = do
|
||||
case lookup lbl typs of
|
||||
Nothing -> do (aexp,val,cs) <- inferExp th tenv exp
|
||||
return ((lbl,(val,aexp)),cs)
|
||||
Just val -> do (aexp,cs) <- checkExp th tenv exp val
|
||||
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
|
||||
|
||||
(ps',_,rho2,k') = ps2ts k ps
|
||||
tenv' = (k, rho2++rho, gamma) ---- k' ?
|
||||
(k,rho,gamma) = tenv
|
||||
|
||||
chB tenv@(k,rho,gamma) ps ty = case ps of
|
||||
p:ps2 -> do
|
||||
typ <- whnf ty
|
||||
case typ of
|
||||
VClos env (Prod _ y a b) -> do
|
||||
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
|
||||
_ -> Bad (render ("Product expected for definiens" <+> ppTerm Unqualified 0 t <+> "instead of" <+> ppValue Unqualified 0 typ))
|
||||
[] -> do
|
||||
(e,cs) <- checkExp th tenv t ty
|
||||
return (([],e),cs)
|
||||
checkP env@(k,rho,gamma) t x a = do
|
||||
(delta,cs) <- checkPatt th env t a
|
||||
let sigma = [(x, VGen i x) | ((x,_),i) <- zip delta [k..]]
|
||||
return (VClos sigma t, sigma, delta, cs)
|
||||
|
||||
ps2ts k = foldr p2t ([],0,[],k)
|
||||
p2t p (ps,i,g,k) = case p of
|
||||
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')
|
||||
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)
|
||||
_ -> error $ render ("undefined p2t case" <+> ppPatt Unqualified 0 p <+> "in checkBranch")
|
||||
|
||||
upd x k g = (x, VGen k x) : g --- hack to recognize pattern variables
|
||||
|
||||
|
||||
checkPatt :: Theory -> TCEnv -> Term -> Val -> Err (Binds,[(Val,Val)])
|
||||
checkPatt th tenv exp val = do
|
||||
(aexp,_,cs) <- checkExpP tenv exp val
|
||||
let binds = extrBinds aexp
|
||||
return (binds,cs)
|
||||
where
|
||||
extrBinds aexp = case aexp of
|
||||
AVr i v -> [(i,v)]
|
||||
AApp f a _ -> extrBinds f ++ extrBinds a
|
||||
_ -> [] -- no other cases are possible
|
||||
|
||||
--- ad hoc, to find types of variables
|
||||
checkExpP tenv@(k,rho,gamma) exp val = case exp of
|
||||
Meta m -> return $ (AMeta m val, val, [])
|
||||
Vr x -> return $ (AVr x val, val, [])
|
||||
EInt i -> return (AInt i, valAbsInt, [])
|
||||
EFloat i -> return (AFloat i, valAbsFloat, [])
|
||||
K s -> return (AStr s, valAbsString, [])
|
||||
|
||||
Q c -> do
|
||||
typ <- lookupConst th c
|
||||
return $ (ACn c typ, typ, [])
|
||||
QC c -> do
|
||||
typ <- lookupConst th c
|
||||
return $ (ACn c typ, typ, []) ----
|
||||
App f t -> do
|
||||
(f',w,csf) <- checkExpP tenv f val
|
||||
typ <- whnf w
|
||||
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)
|
||||
_ -> 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))
|
||||
|
||||
-- auxiliaries
|
||||
|
||||
noConstr :: Err Val -> Err (Val,[(Val,Val)])
|
||||
noConstr er = er >>= (\v -> return (v,[]))
|
||||
|
||||
mkAnnot :: (Val -> AExp) -> Err (Val,[(Val,Val)]) -> Err (AExp,Val,[(Val,Val)])
|
||||
mkAnnot a ti = do
|
||||
(v,cs) <- ti
|
||||
return (a v, v, cs)
|
||||
@@ -14,7 +14,6 @@
|
||||
|
||||
module GF.Grammar
|
||||
( module GF.Grammar.Grammar,
|
||||
module GF.Grammar.Values,
|
||||
module GF.Grammar.Macros,
|
||||
module GF.Grammar.Parser,
|
||||
module GF.Grammar.Printer,
|
||||
@@ -23,7 +22,6 @@ module GF.Grammar
|
||||
) where
|
||||
|
||||
import GF.Grammar.Grammar
|
||||
import GF.Grammar.Values
|
||||
import GF.Grammar.Macros
|
||||
import GF.Grammar.Parser
|
||||
import GF.Grammar.Printer
|
||||
|
||||
@@ -26,6 +26,7 @@ module GF.Grammar.Lookup (
|
||||
allParamValues,
|
||||
countParamValues,
|
||||
lookupAbsDef,
|
||||
lookupAbsType,
|
||||
lookupLincat,
|
||||
lookupFunType,
|
||||
lookupCatContext,
|
||||
@@ -225,12 +226,12 @@ countParamValues gr ptyp =
|
||||
-- to normalize records and record types
|
||||
sortByLbl = sortBy (\(l1,_,_) (l2,_,_) -> compare l1 l2)
|
||||
|
||||
lookupAbsDef :: ErrorMonad m => Grammar -> ModuleName -> Ident -> m (Maybe Int,Maybe [Equation])
|
||||
lookupAbsDef gr m c = errIn (render ("looking up absdef of" <+> c)) $ do
|
||||
info <- lookupQIdentInfo gr (m,c)
|
||||
lookupAbsDef :: ErrorMonad m => Grammar -> QIdent -> m (Maybe Int,Maybe [Equation])
|
||||
lookupAbsDef gr q@(m,c) = errIn (render ("looking up absdef of" <+> c)) $ do
|
||||
info <- lookupQIdentInfo gr q
|
||||
case info of
|
||||
AbsFun _ a d _ -> return (a,fmap (map unLoc) d)
|
||||
AnyInd _ n -> lookupAbsDef gr n c
|
||||
AnyInd _ n -> lookupAbsDef gr (n,c)
|
||||
_ -> return (Nothing,Nothing)
|
||||
|
||||
lookupLincat :: ErrorMonad m => Grammar -> ModuleName -> Ident -> m Type
|
||||
@@ -243,12 +244,29 @@ lookupLincat gr m c = do
|
||||
_ -> raise (render (c <+> "has no linearization type in" <+> m))
|
||||
|
||||
-- | this is needed at compile time
|
||||
lookupFunType :: ErrorMonad m => Grammar -> ModuleName -> Ident -> m Type
|
||||
lookupFunType gr m c = do
|
||||
info <- lookupQIdentInfo gr (m,c)
|
||||
lookupAbsType :: ErrorMonad m => Grammar -> QIdent -> m Type
|
||||
lookupAbsType gr q@(m,c)
|
||||
| m == cPredefAbs =
|
||||
if elem c [cInt,cFloat,cString]
|
||||
then return typeType
|
||||
else no_type
|
||||
| otherwise = do
|
||||
info <- lookupQIdentInfo gr q
|
||||
case info of
|
||||
AbsCat (Just (L _ co)) -> return (mkProd co typeType [])
|
||||
AbsFun (Just (L _ t)) _ _ _ -> return t
|
||||
AnyInd _ n -> lookupAbsType gr (n,c)
|
||||
_ -> no_type
|
||||
where
|
||||
no_type = raise (render ("cannot find type of" <+> c))
|
||||
|
||||
-- | this is needed at compile time
|
||||
lookupFunType :: ErrorMonad m => Grammar -> QIdent -> m Type
|
||||
lookupFunType gr q@(m,c) = do
|
||||
info <- lookupQIdentInfo gr q
|
||||
case info of
|
||||
AbsFun (Just (L _ t)) _ _ _ -> return t
|
||||
AnyInd _ n -> lookupFunType gr n c
|
||||
AnyInd _ n -> lookupFunType gr (n,c)
|
||||
_ -> raise (render ("cannot find type of" <+> c))
|
||||
|
||||
-- | this is needed at compile time
|
||||
|
||||
@@ -16,9 +16,7 @@ module GF.Grammar.Printer
|
||||
, ppParams
|
||||
, ppTerm
|
||||
, ppPatt
|
||||
, ppValue
|
||||
, ppBind
|
||||
, ppConstrs
|
||||
, ppQIdent
|
||||
, ppMeta
|
||||
, ppLVar
|
||||
@@ -29,7 +27,6 @@ import Prelude hiding ((<>)) -- GHC 8.4.1 clash with Text.PrettyPrint
|
||||
import PGF2(Literal(..),pgfFilePath)
|
||||
import GF.Infra.Ident
|
||||
import GF.Infra.Option
|
||||
import GF.Grammar.Values
|
||||
import GF.Grammar.Predef
|
||||
import GF.Grammar.Grammar
|
||||
|
||||
@@ -305,22 +302,6 @@ ppPatt q d (PR xs) = braces (hsep (punctuate ';' [l <+> '=' <+> ppPatt q 0
|
||||
ppPatt q d (PImplArg p) = braces (ppPatt q 0 p)
|
||||
ppPatt q d (PTilde t) = prec d 2 ('~' <> ppTerm q 6 t)
|
||||
|
||||
ppValue :: TermPrintQual -> Int -> Val -> Doc
|
||||
ppValue q d (VGen i x) = x <> "{-" <> i <> "-}" ---- latter part for debugging
|
||||
ppValue q d (VApp u v) = prec d 4 (ppValue q 4 u <+> ppValue q 5 v)
|
||||
ppValue q d (VCn (_,c)) = pp c
|
||||
ppValue q d (VClos env e) = case e of
|
||||
Meta _ -> ppTerm q d e <> ppEnv env
|
||||
_ -> ppTerm q d e ---- ++ prEnv env ---- for debugging
|
||||
ppValue q d (VRecType xs) = braces (hsep (punctuate ',' [l <> '=' <> ppValue q 0 v | (l,v) <- xs]))
|
||||
ppValue q d VType = pp "Type"
|
||||
|
||||
ppConstrs :: Constraints -> [Doc]
|
||||
ppConstrs = map (\(v,w) -> braces (ppValue Unqualified 0 v <+> "<>" <+> ppValue Unqualified 0 w))
|
||||
|
||||
ppEnv :: Env -> Doc
|
||||
ppEnv e = hcat (map (\(x,t) -> braces (x <> ":=" <> ppValue Unqualified 0 t)) e)
|
||||
|
||||
str s = doubleQuotes (pp (foldr showLitChar "" s))
|
||||
where
|
||||
showLitChar c
|
||||
|
||||
@@ -1,115 +0,0 @@
|
||||
----------------------------------------------------------------------
|
||||
-- |
|
||||
-- Module : Unify
|
||||
-- Maintainer : AR
|
||||
-- Stability : (stable)
|
||||
-- Portability : (portable)
|
||||
--
|
||||
-- > CVS $Date: 2005/04/21 16:22:31 $
|
||||
-- > CVS $Author: bringert $
|
||||
-- > CVS $Revision: 1.4 $
|
||||
--
|
||||
-- (c) Petri Mäenpää & Aarne Ranta, 1998--2001
|
||||
--
|
||||
-- brute-force adaptation of the old-GF program AR 21\/12\/2001 ---
|
||||
-- the only use is in 'TypeCheck.splitConstraints'
|
||||
-----------------------------------------------------------------------------
|
||||
|
||||
module GF.Grammar.Unify (unifyVal) where
|
||||
|
||||
import GF.Grammar
|
||||
import GF.Data.Operations
|
||||
|
||||
import GF.Text.Pretty
|
||||
import Data.List (partition)
|
||||
|
||||
unifyVal :: Constraints -> Err (Constraints,MetaSubst)
|
||||
unifyVal cs0 = do
|
||||
let (cs1,cs2) = partition notSolvable cs0
|
||||
let (us,vs) = unzip cs2
|
||||
let us' = map val2term us
|
||||
let vs' = map val2term vs
|
||||
let (ms,cs) = unifyAll (zip us' vs') []
|
||||
return (cs1 ++ [(VClos [] t, VClos [] u) | (t,u) <- cs],
|
||||
[(m, VClos [] t) | (m,t) <- ms])
|
||||
where
|
||||
notSolvable (v,w) = case (v,w) of -- don't consider nonempty closures
|
||||
(VClos (_:_) _,_) -> True
|
||||
(_,VClos (_:_) _) -> True
|
||||
_ -> False
|
||||
|
||||
type Unifier = [(MetaId, Term)]
|
||||
type Constrs = [(Term, Term)]
|
||||
|
||||
unifyAll :: Constrs -> Unifier -> (Unifier,Constrs)
|
||||
unifyAll [] g = (g, [])
|
||||
unifyAll ((a@(s, t)) : l) g =
|
||||
let (g1, c) = unifyAll l g
|
||||
in case unify s t g1 of
|
||||
Ok g2 -> (g2, c)
|
||||
_ -> (g1, a : c)
|
||||
|
||||
unify :: Term -> Term -> Unifier -> Err Unifier
|
||||
unify e1 e2 g =
|
||||
case (e1, e2) of
|
||||
(Meta s, t) -> do
|
||||
tg <- subst_all g t
|
||||
let sg = maybe e1 id (lookup s g)
|
||||
if (sg == Meta s) then extend g s tg else unify sg tg g
|
||||
(t, Meta s) -> unify e2 e1 g
|
||||
(Q (_,a), Q (_,b)) | (a == b) -> return g ---- qualif?
|
||||
(QC (_,a), QC (_,b)) | (a == b)-> return g ----
|
||||
(Vr x, Vr y) | (x == y) -> return g
|
||||
(Abs _ x b, Abs _ y c) -> do let c' = substTerm [x] [(y,Vr x)] c
|
||||
unify b c' g
|
||||
(App c a, App d b) -> case unify c d g of
|
||||
Ok g1 -> unify a b g1
|
||||
_ -> Bad (render ("fail unify" <+> ppTerm Unqualified 0 e1))
|
||||
(RecType xs,RecType ys) | xs == ys -> return g
|
||||
_ -> Bad (render ("fail unify" <+> ppTerm Unqualified 0 e1))
|
||||
|
||||
extend :: Unifier -> MetaId -> Term -> Err Unifier
|
||||
extend g s t | (t == Meta s) = return g
|
||||
| occCheck s t = Bad (render ("occurs check" <+> ppTerm Unqualified 0 t))
|
||||
| True = return ((s, t) : g)
|
||||
|
||||
subst_all :: Unifier -> Term -> Err Term
|
||||
subst_all s u =
|
||||
case (s,u) of
|
||||
([], t) -> return t
|
||||
(a : l, t) -> do
|
||||
t' <- (subst_all l t) --- successive substs - why ?
|
||||
return $ substMetas [a] t'
|
||||
|
||||
substMetas :: [(MetaId,Term)] -> Term -> Term
|
||||
substMetas subst trm = case trm of
|
||||
Meta x -> case lookup x subst of
|
||||
Just t -> t
|
||||
_ -> trm
|
||||
_ -> composSafeOp (substMetas subst) trm
|
||||
|
||||
substTerm :: [Ident] -> Substitution -> Term -> Term
|
||||
substTerm ss g c = case c of
|
||||
Vr x -> maybe c id $ lookup x g
|
||||
App f a -> App (substTerm ss g f) (substTerm ss g a)
|
||||
Abs b x t -> let y = mkFreshVarX ss x in
|
||||
Abs b y (substTerm (y:ss) ((x, Vr y):g) t)
|
||||
Prod b x a t -> let y = mkFreshVarX ss x in
|
||||
Prod b y (substTerm ss g a) (substTerm (y:ss) ((x,Vr y):g) t)
|
||||
_ -> c
|
||||
|
||||
occCheck :: MetaId -> Term -> Bool
|
||||
occCheck s u = case u of
|
||||
Meta v -> s == v
|
||||
App c a -> occCheck s c || occCheck s a
|
||||
Abs _ x b -> occCheck s b
|
||||
_ -> False
|
||||
|
||||
val2term :: Val -> Term
|
||||
val2term v = case v of
|
||||
VClos g e -> substTerm [] (map (\(x,v) -> (x,val2term v)) g) e
|
||||
VApp f c -> App (val2term f) (val2term c)
|
||||
VCn c -> Q c
|
||||
VGen i x -> Vr x
|
||||
VRecType xs -> RecType (map (\(l,v) -> (l,[],val2term v)) xs)
|
||||
VType -> typeType
|
||||
@@ -1,57 +0,0 @@
|
||||
----------------------------------------------------------------------
|
||||
-- |
|
||||
-- Module : Values
|
||||
-- Maintainer : AR
|
||||
-- Stability : (stable)
|
||||
-- Portability : (portable)
|
||||
--
|
||||
-- > CVS $Date: 2005/04/21 16:22:32 $
|
||||
-- > CVS $Author: bringert $
|
||||
-- > CVS $Revision: 1.7 $
|
||||
--
|
||||
-- (Description of the module)
|
||||
-----------------------------------------------------------------------------
|
||||
|
||||
module GF.Grammar.Values (
|
||||
-- ** Values used in TC type checking
|
||||
Val(..), Env,
|
||||
-- ** Annotated tree used in editing
|
||||
Binds, Constraints, MetaSubst,
|
||||
-- ** For TC
|
||||
valAbsInt, valAbsFloat, valAbsString, vType,
|
||||
isPredefCat,
|
||||
eType,
|
||||
) where
|
||||
|
||||
import GF.Infra.Ident
|
||||
import GF.Grammar.Grammar
|
||||
import GF.Grammar.Predef
|
||||
|
||||
-- values used in TC type checking
|
||||
|
||||
data Val = VGen Int Ident | VApp Val Val | VCn QIdent | VRecType [(Label,Val)] | VType | VClos Env Term
|
||||
deriving (Eq,Show)
|
||||
|
||||
type Env = [(Ident,Val)]
|
||||
|
||||
type Binds = [(Ident,Val)]
|
||||
type Constraints = [(Val,Val)]
|
||||
type MetaSubst = [(MetaId,Val)]
|
||||
|
||||
|
||||
-- for TC
|
||||
|
||||
valAbsInt :: Val
|
||||
valAbsInt = VCn (cPredefAbs, cInt)
|
||||
|
||||
valAbsFloat :: Val
|
||||
valAbsFloat = VCn (cPredefAbs, cFloat)
|
||||
|
||||
valAbsString :: Val
|
||||
valAbsString = VCn (cPredefAbs, cString)
|
||||
|
||||
vType :: Val
|
||||
vType = VType
|
||||
|
||||
eType :: Term
|
||||
eType = Sort cType
|
||||
@@ -13,8 +13,8 @@ import GF.Command.Help(helpCommand)
|
||||
import GF.Command.Abstract
|
||||
import GF.Command.Parse(readCommandLine,pCommand,readTransactionCommand)
|
||||
import GF.Compile.Rename(renameSourceTerm)
|
||||
import GF.Compile.TypeCheck.Concrete(inferLType)
|
||||
import GF.Compile.Compute.Concrete(stdPredef,normalForm,Globals(..))
|
||||
import GF.Compile.TypeCheck(inferLType)
|
||||
import GF.Compile.Compute(stdPredef,normalForm,Globals(..))
|
||||
import GF.Compile.GeneratePMCFG(pmcfgForm,type2fields)
|
||||
import GF.Data.Operations (Err(..))
|
||||
import GF.Data.Utilities(whenM,repeatM)
|
||||
@@ -315,7 +315,7 @@ transactionCommand (CreateLin opts f mb_t is_alter) pgf mb_txnid = do
|
||||
hypos
|
||||
|
||||
compileLinTerm sgr mo f mb_t ty = do
|
||||
let g = Gl sgr (stdPredef g)
|
||||
let g = Gl sgr (stdPredef g) False
|
||||
(t,ty) <- case mb_t of
|
||||
Just t -> do t <- renameSourceTerm sgr mo (Typed t ty)
|
||||
|
||||
@@ -344,7 +344,7 @@ transactionCommand (CreateLincat opts c mb_t) pgf mb_txnid = do
|
||||
compileLincatTerm sgr mo mb_t = do
|
||||
t <- case mb_t of
|
||||
Just t -> do t <- renameSourceTerm sgr mo t
|
||||
let g = Gl sgr (stdPredef g)
|
||||
let g = Gl sgr (stdPredef g) False
|
||||
(t,_) <- inferLType g t
|
||||
return t
|
||||
Nothing -> case lookupResDef sgr (mo,identS c) of
|
||||
|
||||
@@ -104,7 +104,7 @@ library
|
||||
GF.Command.TreeOperations
|
||||
GF.Compile.CFGtoPGF
|
||||
GF.Compile.CheckGrammar
|
||||
GF.Compile.Compute.Concrete
|
||||
GF.Compile.Compute
|
||||
GF.Compile.ExampleBased
|
||||
GF.Compile.Export
|
||||
GF.Compile.GenerateBC
|
||||
@@ -122,9 +122,7 @@ library
|
||||
GF.Compile.SubExOpt
|
||||
GF.Compile.Tags
|
||||
GF.Compile.ToAPI
|
||||
GF.Compile.TypeCheck.Abstract
|
||||
GF.Compile.TypeCheck.Concrete
|
||||
GF.Compile.TypeCheck.TC
|
||||
GF.Compile.TypeCheck
|
||||
GF.Compile.Update
|
||||
GF.Data.BacktrackM
|
||||
GF.Data.Graph
|
||||
@@ -147,8 +145,6 @@ library
|
||||
GF.Grammar.Predef
|
||||
GF.Grammar.Printer
|
||||
GF.Grammar.ShowTerm
|
||||
GF.Grammar.Unify
|
||||
GF.Grammar.Values
|
||||
GF.Grammar.JSON
|
||||
GF.Infra.Concurrency
|
||||
GF.Infra.Dependencies
|
||||
|
||||
Reference in New Issue
Block a user