mirror of
https://github.com/GrammaticalFramework/gf-core.git
synced 2026-05-06 17:52:51 -06:00
polish the PGF API and make Expr and Type abstract types. Tree is a type synonym of Expr
This commit is contained in:
@@ -1,16 +1,19 @@
|
||||
module PGF.CId (CId(..),
|
||||
mkCId, readCId, prCId,
|
||||
wildCId,
|
||||
pCId, pIdent) where
|
||||
mkCId, wildCId,
|
||||
readCId, showCId,
|
||||
|
||||
-- utils
|
||||
pCId, pIdent, ppCId) where
|
||||
|
||||
import Control.Monad
|
||||
import qualified Data.ByteString.Char8 as BS
|
||||
import Data.Char
|
||||
import qualified Text.ParserCombinators.ReadP as RP
|
||||
import qualified Text.PrettyPrint as PP
|
||||
|
||||
|
||||
-- | An abstract data type that represents
|
||||
-- function identifier in PGF.
|
||||
-- identifiers for functions and categories in PGF.
|
||||
newtype CId = CId BS.ByteString deriving (Eq,Ord)
|
||||
|
||||
wildCId :: CId
|
||||
@@ -20,17 +23,18 @@ wildCId = CId (BS.singleton '_')
|
||||
mkCId :: String -> CId
|
||||
mkCId s = CId (BS.pack s)
|
||||
|
||||
-- | Reads an identifier from 'String'. The function returns 'Nothing' if the string is not valid identifier.
|
||||
readCId :: String -> Maybe CId
|
||||
readCId s = case [x | (x,cs) <- RP.readP_to_S pCId s, all isSpace cs] of
|
||||
[x] -> Just x
|
||||
_ -> Nothing
|
||||
|
||||
-- | Renders the identifier as 'String'
|
||||
prCId :: CId -> String
|
||||
prCId (CId x) = BS.unpack x
|
||||
showCId :: CId -> String
|
||||
showCId (CId x) = BS.unpack x
|
||||
|
||||
instance Show CId where
|
||||
showsPrec _ = showString . prCId
|
||||
showsPrec _ = showString . showCId
|
||||
|
||||
instance Read CId where
|
||||
readsPrec _ = RP.readP_to_S pCId
|
||||
@@ -45,4 +49,7 @@ pIdent :: RP.ReadP String
|
||||
pIdent = liftM2 (:) (RP.satisfy isIdentFirst) (RP.munch isIdentRest)
|
||||
where
|
||||
isIdentFirst c = c == '_' || isLetter c
|
||||
isIdentRest c = c == '_' || c == '\'' || isAlphaNum c
|
||||
isIdentRest c = c == '_' || c == '\'' || isAlphaNum c
|
||||
|
||||
ppCId :: CId -> PP.Doc
|
||||
ppCId = PP.text . showCId
|
||||
|
||||
@@ -30,7 +30,7 @@ labelBoolErr ms iob = do
|
||||
|
||||
checkConcrete :: PGF -> (CId,Concr) -> Err ((CId,Concr),Bool)
|
||||
checkConcrete pgf (lang,cnc) =
|
||||
labelBoolErr ("happened in language " ++ prCId lang) $ do
|
||||
labelBoolErr ("happened in language " ++ showCId lang) $ do
|
||||
(rs,bs) <- mapM checkl (Map.assocs (lins cnc)) >>= return . unzip
|
||||
return ((lang,cnc{lins = Map.fromAscList rs}),and bs)
|
||||
where
|
||||
@@ -38,7 +38,7 @@ checkConcrete pgf (lang,cnc) =
|
||||
|
||||
checkLin :: PGF -> CId -> (CId,Term) -> Err ((CId,Term),Bool)
|
||||
checkLin pgf lang (f,t) =
|
||||
labelBoolErr ("happened in function " ++ prCId f) $ do
|
||||
labelBoolErr ("happened in function " ++ showCId f) $ do
|
||||
(t',b) <- checkTerm (lintype pgf lang f) t --- $ inline pgf lang t
|
||||
return ((f,t'),b)
|
||||
|
||||
|
||||
@@ -1,7 +1,7 @@
|
||||
module PGF.Data (module PGF.Data, module PGF.Expr, module PGF.Type, module PGF.PMCFG) where
|
||||
|
||||
import PGF.CId
|
||||
import PGF.Expr hiding (Value, Env)
|
||||
import PGF.Expr hiding (Value, Env, Tree)
|
||||
import PGF.Type
|
||||
import PGF.PMCFG
|
||||
|
||||
@@ -92,4 +92,4 @@ readLanguage :: String -> Maybe Language
|
||||
readLanguage = readCId
|
||||
|
||||
showLanguage :: Language -> String
|
||||
showLanguage = prCId
|
||||
showLanguage = showCId
|
||||
|
||||
@@ -1,4 +1,4 @@
|
||||
module PGF.Expr(Expr(..), Literal(..), Patt(..), Equation(..),
|
||||
module PGF.Expr(Tree, Expr(..), Literal(..), Patt(..), Equation(..),
|
||||
readExpr, showExpr, pExpr, ppExpr, ppPatt,
|
||||
|
||||
normalForm,
|
||||
@@ -31,8 +31,14 @@ data Literal =
|
||||
|
||||
type MetaId = Int
|
||||
|
||||
-- | An expression represents a potentially unevaluated expression
|
||||
-- in the abstract syntax of the grammar.
|
||||
-- | Tree is the abstract syntax representation of a given sentence
|
||||
-- in some concrete syntax. Technically 'Tree' is a type synonym
|
||||
-- of 'Expr'.
|
||||
type Tree = Expr
|
||||
|
||||
-- | An expression in the abstract syntax of the grammar. It could be
|
||||
-- both parameter of a dependent type or an abstract syntax tree for
|
||||
-- for some sentence.
|
||||
data Expr =
|
||||
EAbs CId Expr -- ^ lambda abstraction
|
||||
| EApp Expr Expr -- ^ application
|
||||
@@ -127,7 +133,7 @@ pStr = RP.char '"' >> (RP.manyTill (pEsc RP.<++ RP.get) (RP.char '"'))
|
||||
ppExpr :: Int -> [CId] -> Expr -> PP.Doc
|
||||
ppExpr d scope (EAbs x e) = let (xs,e1) = getVars [x] e
|
||||
in ppParens (d > 1) (PP.char '\\' PP.<>
|
||||
PP.hsep (PP.punctuate PP.comma (List.map (PP.text . prCId) (reverse xs))) PP.<+>
|
||||
PP.hsep (PP.punctuate PP.comma (List.map ppCId (reverse xs))) PP.<+>
|
||||
PP.text "->" PP.<+>
|
||||
ppExpr 1 (xs++scope) e1)
|
||||
where
|
||||
@@ -136,14 +142,14 @@ ppExpr d scope (EAbs x e) = let (xs,e1) = getVars [x] e
|
||||
ppExpr d scope (EApp e1 e2) = ppParens (d > 3) ((ppExpr 3 scope e1) PP.<+> (ppExpr 4 scope e2))
|
||||
ppExpr d scope (ELit l) = ppLit l
|
||||
ppExpr d scope (EMeta n) = ppMeta n
|
||||
ppExpr d scope (EFun f) = PP.text (prCId f)
|
||||
ppExpr d scope (EVar i) = PP.text (prCId (scope !! i))
|
||||
ppExpr d scope (EFun f) = ppCId f
|
||||
ppExpr d scope (EVar i) = ppCId (scope !! i)
|
||||
ppExpr d scope (ETyped e ty)= ppParens (d > 0) (ppExpr 0 scope e PP.<+> PP.colon PP.<+> ppType 0 scope ty)
|
||||
|
||||
ppPatt d scope (PApp f ps) = let (scope',ds) = mapAccumL (ppPatt 2) scope ps
|
||||
in (scope',ppParens (not (List.null ps) && d > 1) (PP.text (prCId f) PP.<+> PP.hsep ds))
|
||||
in (scope',ppParens (not (List.null ps) && d > 1) (ppCId f PP.<+> PP.hsep ds))
|
||||
ppPatt d scope (PLit l) = (scope,ppLit l)
|
||||
ppPatt d scope (PVar f) = (scope,PP.text (prCId f))
|
||||
ppPatt d scope (PVar f) = (scope,ppCId f)
|
||||
ppPatt d scope PWild = (scope,PP.char '_')
|
||||
|
||||
ppLit (LStr s) = PP.text (show s)
|
||||
@@ -200,7 +206,7 @@ eval funs env (EFun f) = case Map.lookup f funs of
|
||||
Equ [] e : _ -> eval funs [] e
|
||||
_ -> VApp f []
|
||||
else VApp f []
|
||||
Nothing -> error ("unknown function "++prCId f)
|
||||
Nothing -> error ("unknown function "++showCId f)
|
||||
eval funs env (EApp e1 e2) = apply funs env e1 [eval funs env e2]
|
||||
eval funs env (EAbs x e) = VClosure env (EAbs x e)
|
||||
eval funs env (EMeta i) = VMeta i env []
|
||||
@@ -215,7 +221,7 @@ apply funs env (EFun f) vs = case Map.lookup f funs of
|
||||
then let (as,vs') = splitAt a vs
|
||||
in match funs f eqs as vs'
|
||||
else VApp f vs
|
||||
Nothing -> error ("unknown function "++prCId f)
|
||||
Nothing -> error ("unknown function "++showCId f)
|
||||
apply funs env (EApp e1 e2) vs = apply funs env e1 (eval funs env e2 : vs)
|
||||
apply funs env (EAbs x e) (v:vs) = apply funs (v:env) e vs
|
||||
apply funs env (EMeta i) vs = VMeta i env vs
|
||||
|
||||
@@ -59,14 +59,14 @@ linTree :: PGF -> CId -> Expr -> Term
|
||||
linTree pgf lang = lin . expr2tree
|
||||
where
|
||||
lin (Abs xs e ) = case lin e of
|
||||
R ts -> R $ ts ++ (Data.List.map (kks . prCId) xs)
|
||||
TM s -> R $ (TM s) : (Data.List.map (kks . prCId) xs)
|
||||
R ts -> R $ ts ++ (Data.List.map (kks . showCId) xs)
|
||||
TM s -> R $ (TM s) : (Data.List.map (kks . showCId) xs)
|
||||
lin (Fun fun es) = let argVariants = mapM (liftVariants . lin) es
|
||||
in variants [compute pgf lang args $ look fun | args <- argVariants]
|
||||
lin (Lit (LStr s)) = R [kks (show s)] -- quoted
|
||||
lin (Lit (LInt i)) = R [kks (show i)]
|
||||
lin (Lit (LFlt d)) = R [kks (show d)]
|
||||
lin (Var x) = TM (prCId x)
|
||||
lin (Var x) = TM (showCId x)
|
||||
lin (Meta i) = TM (show i)
|
||||
|
||||
look = lookLin pgf lang
|
||||
@@ -130,15 +130,15 @@ linTreeMark :: PGF -> CId -> Expr -> Term
|
||||
linTreeMark pgf lang = lin [] . expr2tree
|
||||
where
|
||||
lin p (Abs xs e ) = case lin p e of
|
||||
R ts -> R $ ts ++ (Data.List.map (kks . prCId) xs)
|
||||
TM s -> R $ (TM s) : (Data.List.map (kks . prCId) xs)
|
||||
R ts -> R $ ts ++ (Data.List.map (kks . showCId) xs)
|
||||
TM s -> R $ (TM s) : (Data.List.map (kks . showCId) xs)
|
||||
lin p (Fun fun es) = let argVariants =
|
||||
mapM (\ (i,e) -> liftVariants $ lin (sub p i) e) (zip [0..] es)
|
||||
in variants [mark p $ compute pgf lang args $ look fun | args <- argVariants]
|
||||
lin p (Lit (LStr s)) = mark p $ R [kks (show s)] -- quoted
|
||||
lin p (Lit (LInt i)) = mark p $ R [kks (show i)]
|
||||
lin p (Lit (LFlt d)) = mark p $ R [kks (show d)]
|
||||
lin p (Var x) = mark p $ TM (prCId x)
|
||||
lin p (Var x) = mark p $ TM (showCId x)
|
||||
lin p (Meta i) = mark p $ TM (show i)
|
||||
|
||||
look = lookLin pgf lang
|
||||
|
||||
@@ -69,7 +69,7 @@ lookAbsFlag pgf f =
|
||||
|
||||
lookConcr :: PGF -> CId -> Concr
|
||||
lookConcr pgf cnc =
|
||||
lookMap (error $ "Missing concrete syntax: " ++ prCId cnc) cnc $ concretes pgf
|
||||
lookMap (error $ "Missing concrete syntax: " ++ showCId cnc) cnc $ concretes pgf
|
||||
|
||||
lookConcrFlag :: PGF -> CId -> CId -> Maybe String
|
||||
lookConcrFlag pgf lang f = Map.lookup f $ cflags $ lookConcr pgf lang
|
||||
@@ -129,7 +129,7 @@ contextLength ty = case ty of
|
||||
DTyp hyps _ _ -> length hyps
|
||||
|
||||
term0 :: CId -> Term
|
||||
term0 = TM . prCId
|
||||
term0 = TM . showCId
|
||||
|
||||
tm0 :: Term
|
||||
tm0 = TM "?"
|
||||
|
||||
@@ -72,13 +72,13 @@ ppProduction (fcat,FConst _ ss) =
|
||||
ppFCat fcat <+> text "->" <+> ppStrs ss
|
||||
|
||||
ppFun (funid,FFun fun _ arr) =
|
||||
ppFunId funid <+> text ":=" <+> parens (hcat (punctuate comma (map ppSeqId (elems arr)))) <+> brackets (text (prCId fun))
|
||||
ppFunId funid <+> text ":=" <+> parens (hcat (punctuate comma (map ppSeqId (elems arr)))) <+> brackets (ppCId fun)
|
||||
|
||||
ppSeq (seqid,seq) =
|
||||
ppSeqId seqid <+> text ":=" <+> hsep (map ppSymbol (elems seq))
|
||||
|
||||
ppStartCat (id,fcats) =
|
||||
text (prCId id) <+> text ":=" <+> brackets (hcat (punctuate comma (map ppFCat fcats)))
|
||||
ppCId id <+> text ":=" <+> brackets (hcat (punctuate comma (map ppFCat fcats)))
|
||||
|
||||
ppSymbol (FSymCat d r) = char '<' <> int d <> comma <> int r <> char '>'
|
||||
ppSymbol (FSymLit d r) = char '<' <> int d <> comma <> int r <> char '>'
|
||||
|
||||
@@ -16,7 +16,6 @@ module PGF.Paraphrase (
|
||||
import PGF.Data
|
||||
import PGF.Tree
|
||||
import PGF.Macros (lookDef,isData)
|
||||
import PGF.Expr
|
||||
import PGF.CId
|
||||
|
||||
import Data.List (nub,sort,group)
|
||||
|
||||
@@ -4,7 +4,7 @@ module PGF.Parsing.FCFG.Incremental
|
||||
, initState
|
||||
, nextState
|
||||
, getCompletions
|
||||
, extractExps
|
||||
, extractTrees
|
||||
, parse
|
||||
) where
|
||||
|
||||
@@ -21,12 +21,13 @@ import Control.Monad
|
||||
import GF.Data.SortedList
|
||||
import PGF.CId
|
||||
import PGF.Data
|
||||
import PGF.Expr(Tree)
|
||||
import PGF.Macros
|
||||
import PGF.TypeCheck
|
||||
import Debug.Trace
|
||||
|
||||
parse :: PGF -> Language -> Type -> [String] -> [Expr]
|
||||
parse pgf lang typ toks = maybe [] (\ps -> extractExps ps typ) (foldM nextState (initState pgf lang typ) toks)
|
||||
parse pgf lang typ toks = maybe [] (\ps -> extractTrees ps typ) (foldM nextState (initState pgf lang typ) toks)
|
||||
|
||||
-- | Creates an initial parsing state for a given language and
|
||||
-- startup category.
|
||||
@@ -43,7 +44,7 @@ initState pgf lang (DTyp _ start _) =
|
||||
pinfo =
|
||||
case lookParser pgf lang of
|
||||
Just pinfo -> pinfo
|
||||
_ -> error ("Unknown language: " ++ prCId lang)
|
||||
_ -> error ("Unknown language: " ++ showCId lang)
|
||||
|
||||
in State pgf
|
||||
pinfo
|
||||
@@ -97,8 +98,8 @@ getCompletions (State pgf pinfo chart items) w =
|
||||
-- that spans the whole input consumed so far. The trees are also
|
||||
-- limited by the category specified, which is usually
|
||||
-- the same as the startup category.
|
||||
extractExps :: ParseState -> Type -> [Expr]
|
||||
extractExps (State pgf pinfo chart items) ty@(DTyp _ start _) =
|
||||
extractTrees :: ParseState -> Type -> [Tree]
|
||||
extractTrees (State pgf pinfo chart items) ty@(DTyp _ start _) =
|
||||
nubsort [e1 | e <- exps, Right e1 <- [checkExpr pgf e ty]]
|
||||
where
|
||||
(mb_agenda,acc) = TMap.decompose items
|
||||
|
||||
@@ -103,11 +103,11 @@ collectWords pgf lang =
|
||||
[(f,c,0) | (f,(DTyp [] c _,_,_)) <- Map.toList $ funs $ abstract pgf]
|
||||
where
|
||||
collOne (f,c,i) =
|
||||
fromRec f [prCId c] (recLinearize pgf lang (foldl EApp (EFun f) (replicate i (EMeta 888))))
|
||||
fromRec f [showCId c] (recLinearize pgf lang (foldl EApp (EFun f) (replicate i (EMeta 888))))
|
||||
fromRec f v r = case r of
|
||||
RR rs -> concat [fromRec f v t | (_,t) <- rs]
|
||||
RT rs -> concat [fromRec f (p:v) t | (p,t) <- rs]
|
||||
RFV rs -> concatMap (fromRec f v) rs
|
||||
RS s -> [(s,[(prCId f,unwords (reverse v))])]
|
||||
RS s -> [(s,[(showCId f,unwords (reverse v))])]
|
||||
RCon c -> [] ---- inherent
|
||||
|
||||
|
||||
@@ -5,7 +5,7 @@ module PGF.Tree
|
||||
) where
|
||||
|
||||
import PGF.CId
|
||||
import PGF.Expr
|
||||
import PGF.Expr hiding (Tree)
|
||||
|
||||
import Data.Char
|
||||
import Data.List as List
|
||||
@@ -56,14 +56,14 @@ pTree isNested = RP.skipSpaces >> (pParen RP.<++ pAbs RP.<++ pApp RP.<++ fmap Li
|
||||
return (Fun f ts)
|
||||
|
||||
ppTree d (Abs xs t) = ppParens (d > 0) (PP.char '\\' PP.<>
|
||||
PP.hsep (PP.punctuate PP.comma (List.map (PP.text . prCId) xs)) PP.<+>
|
||||
PP.hsep (PP.punctuate PP.comma (List.map ppCId xs)) PP.<+>
|
||||
PP.text "->" PP.<+>
|
||||
ppTree 0 t)
|
||||
ppTree d (Fun f []) = PP.text (prCId f)
|
||||
ppTree d (Fun f ts) = ppParens (d > 0) (PP.text (prCId f) PP.<+> PP.hsep (List.map (ppTree 1) ts))
|
||||
ppTree d (Fun f []) = ppCId f
|
||||
ppTree d (Fun f ts) = ppParens (d > 0) (ppCId f PP.<+> PP.hsep (List.map (ppTree 1) ts))
|
||||
ppTree d (Lit l) = ppLit l
|
||||
ppTree d (Meta n) = ppMeta n
|
||||
ppTree d (Var id) = PP.text (prCId id)
|
||||
ppTree d (Var id) = ppCId id
|
||||
|
||||
|
||||
-----------------------------------------------------
|
||||
|
||||
@@ -75,10 +75,10 @@ ppType d scope (DTyp hyps cat args)
|
||||
| otherwise = let (scope',hdocs) = mapAccumL ppHypo scope hyps
|
||||
in ppParens (d > 0) (foldr (\hdoc doc -> hdoc PP.<+> PP.text "->" PP.<+> doc) (ppRes scope' cat args) hdocs)
|
||||
where
|
||||
ppRes scope cat es = PP.text (prCId cat) PP.<+> PP.hsep (map (ppExpr 4 scope) es)
|
||||
ppRes scope cat es = ppCId cat PP.<+> PP.hsep (map (ppExpr 4 scope) es)
|
||||
|
||||
ppHypo scope (Hyp typ) = ( scope,ppType 1 scope typ)
|
||||
ppHypo scope (HypV x typ) = let y = freshName x scope
|
||||
in (y:scope,PP.parens (PP.text (prCId y) PP.<+> PP.char ':' PP.<+> ppType 0 scope typ))
|
||||
in (y:scope,PP.parens (ppCId y PP.<+> PP.char ':' PP.<+> ppType 0 scope typ))
|
||||
ppHypo scope (HypI x typ) = let y = freshName x scope
|
||||
in (y:scope,PP.braces (PP.text (prCId y) PP.<+> PP.char ':' PP.<+> ppType 0 scope typ))
|
||||
in (y:scope,PP.braces (ppCId y PP.<+> PP.char ':' PP.<+> ppType 0 scope typ))
|
||||
|
||||
@@ -135,33 +135,46 @@ addConstraint i j env vs c = do
|
||||
-- Type errors
|
||||
-----------------------------------------------------
|
||||
|
||||
-- | If an error occurs in the typechecking phase
|
||||
-- the type checker returns not a plain text error message
|
||||
-- but a 'TcError' structure which describes the error.
|
||||
data TcError
|
||||
= UnknownCat CId
|
||||
| UnknownFun CId
|
||||
| WrongCatArgs Scope Type CId Int Int
|
||||
| TypeMismatch Scope Expr Type Type
|
||||
| NotFunType Scope Expr Type
|
||||
| CannotInferType Scope Expr
|
||||
| UnresolvedMetaVars Scope Expr [MetaId]
|
||||
= UnknownCat CId -- ^ Unknown category name was found.
|
||||
| UnknownFun CId -- ^ Unknown function name was found.
|
||||
| WrongCatArgs [CId] Type CId Int Int -- ^ A category was applied to wrong number of arguments.
|
||||
-- The first integer is the number of expected arguments and
|
||||
-- the second the number of given arguments.
|
||||
-- The @[CId]@ argument is the list of free variables
|
||||
-- in the type. It should be used for the 'showType' function.
|
||||
| TypeMismatch [CId] Expr Type Type -- ^ The expression is not of the expected type.
|
||||
-- The first type is the expected type, while
|
||||
-- the second is the inferred. The @[CId]@ argument is the list
|
||||
-- of free variables in both the expression and the type.
|
||||
-- It should be used for the 'showType' and 'showExpr' functions.
|
||||
| NotFunType [CId] Expr Type -- ^ Something that is not of function type was applied to an argument.
|
||||
| CannotInferType [CId] Expr -- ^ It is not possible to infer the type of an expression.
|
||||
| UnresolvedMetaVars [CId] Expr [MetaId] -- ^ Some metavariables have to be instantiated in order to complete the typechecking.
|
||||
|
||||
-- | Renders the type checking error to a document. See 'Text.PrettyPrint'.
|
||||
ppTcError :: TcError -> Doc
|
||||
ppTcError (UnknownCat cat) = text "Category" <+> text (prCId cat) <+> text "is not in scope"
|
||||
ppTcError (UnknownFun fun) = text "Function" <+> text (prCId fun) <+> text "is not in scope"
|
||||
ppTcError (WrongCatArgs scope ty cat m n) =
|
||||
text "Category" <+> text (prCId cat) <+> text "should have" <+> int m <+> text "argument(s), but has been given" <+> int n $$
|
||||
text "In the type:" <+> ppType 0 (scopeVars scope) ty
|
||||
ppTcError (TypeMismatch scope e ty1 ty2) = text "Couldn't match expected type" <+> ppType 0 (scopeVars scope) ty1 $$
|
||||
text " against inferred type" <+> ppType 0 (scopeVars scope) ty2 $$
|
||||
text "In the expression:" <+> ppExpr 0 (scopeVars scope) e
|
||||
ppTcError (NotFunType scope e ty) = text "A function type is expected for the expression" <+> ppExpr 0 (scopeVars scope) e <+> text "instead of type" <+> ppType 0 (scopeVars scope) ty
|
||||
ppTcError (CannotInferType scope e) = text "Cannot infer the type of expression" <+> ppExpr 0 (scopeVars scope) e
|
||||
ppTcError (UnresolvedMetaVars scope e xs) = text "Meta variable(s)" <+> fsep (List.map ppMeta xs) <+> text "should be resolved" $$
|
||||
text "in the expression:" <+> ppExpr 0 (scopeVars scope) e
|
||||
ppTcError (UnknownCat cat) = text "Category" <+> ppCId cat <+> text "is not in scope"
|
||||
ppTcError (UnknownFun fun) = text "Function" <+> ppCId fun <+> text "is not in scope"
|
||||
ppTcError (WrongCatArgs xs ty cat m n) = text "Category" <+> ppCId cat <+> text "should have" <+> int m <+> text "argument(s), but has been given" <+> int n $$
|
||||
text "In the type:" <+> ppType 0 xs ty
|
||||
ppTcError (TypeMismatch xs e ty1 ty2) = text "Couldn't match expected type" <+> ppType 0 xs ty1 $$
|
||||
text " against inferred type" <+> ppType 0 xs ty2 $$
|
||||
text "In the expression:" <+> ppExpr 0 xs e
|
||||
ppTcError (NotFunType xs e ty) = text "A function type is expected for the expression" <+> ppExpr 0 xs e <+> text "instead of type" <+> ppType 0 xs ty
|
||||
ppTcError (CannotInferType xs e) = text "Cannot infer the type of expression" <+> ppExpr 0 xs e
|
||||
ppTcError (UnresolvedMetaVars xs e ms) = text "Meta variable(s)" <+> fsep (List.map ppMeta ms) <+> text "should be resolved" $$
|
||||
text "in the expression:" <+> ppExpr 0 xs e
|
||||
|
||||
-----------------------------------------------------
|
||||
-- checkType
|
||||
-----------------------------------------------------
|
||||
|
||||
-- | Check whether a given type is consistent with the abstract
|
||||
-- syntax of the grammar.
|
||||
checkType :: PGF -> Type -> Either TcError Type
|
||||
checkType pgf ty =
|
||||
case unTcM (tcType emptyScope ty >>= refineType) (abstract pgf) 0 IntMap.empty of
|
||||
@@ -177,7 +190,7 @@ tcType scope ty@(DTyp hyps cat es) = do
|
||||
if m == n
|
||||
then do (delta,es) <- tcHypoExprs scope [] (zip es c_hyps)
|
||||
return (DTyp hyps cat es)
|
||||
else tcError (WrongCatArgs scope ty cat n m)
|
||||
else tcError (WrongCatArgs (scopeVars scope) ty cat n m)
|
||||
|
||||
tcHypos :: Scope -> [Hypo] -> TcM (Scope,[Hypo])
|
||||
tcHypos scope [] = return (scope,[])
|
||||
@@ -215,6 +228,7 @@ tcHypoExpr scope delta e (HypV x ty) = do
|
||||
-- checkExpr
|
||||
-----------------------------------------------------
|
||||
|
||||
-- | Checks an expression against a specified type.
|
||||
checkExpr :: PGF -> Expr -> Type -> Either TcError Expr
|
||||
checkExpr pgf e ty =
|
||||
case unTcM (do e <- tcExpr emptyScope e (TTyp [] ty)
|
||||
@@ -234,7 +248,7 @@ tcExpr scope e0@(EAbs x e) tty =
|
||||
e (TTyp ((VGen (scopeSize scope) []):delta) (DTyp hs c es))
|
||||
return (EAbs x e)
|
||||
_ -> do ty <- evalType (scopeSize scope) tty
|
||||
tcError (NotFunType scope e0 ty)
|
||||
tcError (NotFunType (scopeVars scope) e0 ty)
|
||||
tcExpr scope (EMeta _) tty = do
|
||||
i <- newMeta scope
|
||||
return (EMeta i)
|
||||
@@ -249,6 +263,10 @@ tcExpr scope e0 tty = do
|
||||
-- inferExpr
|
||||
-----------------------------------------------------
|
||||
|
||||
-- | Tries to infer the type of a given expression. Note that
|
||||
-- even if the expression is type correct it is not always
|
||||
-- possible to infer its type in the GF type system.
|
||||
-- In this case the function returns the 'CannotInferType' error.
|
||||
inferExpr :: PGF -> Expr -> Either TcError (Expr,Type)
|
||||
inferExpr pgf e =
|
||||
case unTcM (do (e,tty) <- infExpr emptyScope e
|
||||
@@ -266,7 +284,7 @@ infExpr scope e0@(EApp e1 e2) = do
|
||||
(TTyp delta1 (DTyp (h:hs) c es)) -> do (delta1,e2) <- tcHypoExpr scope delta1 e2 h
|
||||
return (EApp e1 e2,TTyp delta1 (DTyp hs c es))
|
||||
_ -> do ty1 <- evalType (scopeSize scope) tty1
|
||||
tcError (NotFunType scope e1 ty1)
|
||||
tcError (NotFunType (scopeVars scope) e1 ty1)
|
||||
infExpr scope e0@(EFun x) = do
|
||||
case lookupVar x scope of
|
||||
Just (i,tty) -> return (EVar i,tty)
|
||||
@@ -284,7 +302,7 @@ infExpr scope (ETyped e ty) = do
|
||||
ty <- tcType scope ty
|
||||
e <- tcExpr scope e (TTyp (scopeEnv scope) ty)
|
||||
return (ETyped e ty,TTyp (scopeEnv scope) ty)
|
||||
infExpr scope e = tcError (CannotInferType scope e)
|
||||
infExpr scope e = tcError (CannotInferType (scopeVars scope) e)
|
||||
|
||||
-----------------------------------------------------
|
||||
-- eqType
|
||||
@@ -299,7 +317,7 @@ eqType scope k i0 tty1@(TTyp delta1 ty1@(DTyp hyps1 cat1 es1)) tty2@(TTyp delta2
|
||||
raiseTypeMatchError = do ty1 <- evalType k tty1
|
||||
ty2 <- evalType k tty2
|
||||
e <- refineExpr (EMeta i0)
|
||||
tcError (TypeMismatch scope e ty1 ty2)
|
||||
tcError (TypeMismatch (scopeVars scope) e ty1 ty2)
|
||||
|
||||
eqHyps :: Int -> Env -> [Hypo] -> Env -> [Hypo] -> TcM (Int,Env,Env)
|
||||
eqHyps k delta1 [] delta2 [] =
|
||||
@@ -402,7 +420,7 @@ checkResolvedMetaStore scope e = TcM (\abstr metaid ms ->
|
||||
let xs = [i | (i,mv) <- IntMap.toList ms, not (isResolved mv)]
|
||||
in if List.null xs
|
||||
then Ok metaid ms ()
|
||||
else Fail (UnresolvedMetaVars scope e xs))
|
||||
else Fail (UnresolvedMetaVars (scopeVars scope) e xs))
|
||||
where
|
||||
isResolved (MUnbound _ []) = True
|
||||
isResolved (MGuarded _ _ _) = True
|
||||
|
||||
@@ -19,7 +19,7 @@ module PGF.VisualizeTree ( visualizeTrees, alignLinearize
|
||||
,PosText(..),readPosText
|
||||
) where
|
||||
|
||||
import PGF.CId (prCId)
|
||||
import PGF.CId (showCId)
|
||||
import PGF.Data
|
||||
import PGF.Tree
|
||||
import PGF.Linearize
|
||||
@@ -42,14 +42,14 @@ tree2graph pgf (funs,cats) = prf [] where
|
||||
concat [prf (j:ps) t | (j,t) <- zip [0..] trees]
|
||||
prn ps cid =
|
||||
let
|
||||
fun = if funs then prCId cid else ""
|
||||
fun = if funs then showCId cid else ""
|
||||
cat = if cats then prCat cid else ""
|
||||
colon = if funs && cats then " : " else ""
|
||||
lab = "\"" ++ fun ++ colon ++ cat ++ "\""
|
||||
in (show(show (ps :: [Int])),lab)
|
||||
pra i nod t@(Fun cid _) = nod ++ arr ++ fst (prn i cid) ++ " [style = \"solid\"];"
|
||||
arr = " -- " -- if digr then " -> " else " -- "
|
||||
prCat = prCId . lookValCat pgf
|
||||
prCat = showCId . lookValCat pgf
|
||||
|
||||
prGraph digr ns = concat $ map (++"\n") $ [graph ++ "{\n"] ++ ns ++ ["}"] where
|
||||
graph = if digr then "digraph" else "graph"
|
||||
|
||||
Reference in New Issue
Block a user