forked from GitHub/gf-core
552 lines
22 KiB
Plaintext
552 lines
22 KiB
Plaintext
Compiler.hs
|
|
mainGFC :: Options -> [FilePath] -> IO ()
|
|
_ | null fs -> fail $ "No input files."
|
|
_ | all (extensionIs ".pgf") fs -> unionPGFFiles opts fs
|
|
_ -> fail $ "Don't know what to do with these input files: " ++ unwords fs)
|
|
|
|
|
|
----------------------------------------
|
|
Compile.hs
|
|
|
|
compileModule
|
|
case length file1s of
|
|
0 -> raise (render ("Unable to find: " $$ nest 2 candidates))
|
|
1 -> do return $ head file1s
|
|
_ -> do putIfVerb opts1 ("matched multiple candidates: " +++ show file1s)
|
|
return $ head file1s
|
|
else raise (render ("File" <+> file <+> "does not exist"))
|
|
|
|
---------------------------------------
|
|
Grammar.Lexer.x
|
|
token :: P Token
|
|
AlexError (AI pos _ _) -> PFailed pos "lexical error"
|
|
|
|
|
|
---------------------------------------
|
|
Grammar.Parser.y
|
|
|
|
happyError = fail "syntax error"
|
|
|
|
tryLoc (c,mty,Just e) = return (c,(mty,e))
|
|
tryLoc (c,_ ,_ ) = fail ("local definition of" +++ showIdent c +++ "without value")
|
|
|
|
mkR [] = return $ RecType [] --- empty record always interpreted as record type
|
|
mkR fs@(f:_) =
|
|
case f of
|
|
(lab,Just ty,Nothing) -> mapM tryRT fs >>= return . RecType
|
|
_ -> mapM tryR fs >>= return . R
|
|
where
|
|
tryRT (lab,Just ty,Nothing) = return (ident2label lab,ty)
|
|
tryRT (lab,_ ,_ ) = fail $ "illegal record type field" +++ showIdent lab --- manifest fields ?!
|
|
|
|
tryR (lab,mty,Just t) = return (ident2label lab,(mty,t))
|
|
tryR (lab,_ ,_ ) = fail $ "illegal record field" +++ showIdent lab
|
|
|
|
|
|
---------------------------------------
|
|
ModDeps.hs
|
|
|
|
mkSourceGrammar :: [SourceModule] -> Err SourceGrammar
|
|
deplist <- either
|
|
return
|
|
(\ms -> Bad $ "circular modules" +++ unwords (map show ms)) $
|
|
|
|
|
|
checkUniqueImportNames :: [Ident] -> SourceModInfo -> Err ()
|
|
test ms = testErr (all (`notElem` ns) ms)
|
|
("import names clashing with module names among" +++ unwords (map prt ms))
|
|
|
|
|
|
moduleDeps :: [SourceModule] -> Err Dependencies
|
|
deps (c,m) = errIn ("checking dependencies of module" +++ prt c) $ case mtype m of
|
|
MTConcrete a -> do
|
|
am <- lookupModuleType gr a
|
|
testErr (mtype am == MTAbstract) "the of-module is not an abstract syntax"
|
|
|
|
testErr (all (compatMType ety . mtype) ests) "inappropriate extension module type"
|
|
|
|
|
|
---------------------------------------
|
|
Update.hs
|
|
|
|
buildAnyTree
|
|
Just i -> case unifyAnyInfo m i j of
|
|
Ok k -> go (Map.insert c k map) is
|
|
Bad _ -> fail $ render ("conflicting information in module"<+>m $$
|
|
nest 4 (ppJudgement Qualified (c,i)) $$
|
|
"and" $+$
|
|
nest 4 (ppJudgement Qualified (c,j)))
|
|
extendModule
|
|
unless (sameMType (mtype m) (mtype mo))
|
|
(checkError ("illegal extension type to module" <+> name))
|
|
|
|
rebuildModule
|
|
unless (null is || mstatus mi == MSIncomplete)
|
|
(checkError ("module" <+> i <+>
|
|
"has open interfaces and must therefore be declared incomplete"))
|
|
|
|
unless (isModRes m1)
|
|
(checkError ("interface expected instead of" <+> i0))
|
|
js' <- extendMod gr False ((i0,m1), isInherited mincl) i (jments mi)
|
|
|
|
unless (stat' == MSComplete || stat == MSIncomplete)
|
|
(checkError ("module" <+> i <+> "remains incomplete"))
|
|
|
|
|
|
extendMod
|
|
checkError ("cannot unify the information" $$
|
|
nest 4 (ppJudgement Qualified (c,i)) $$
|
|
"in module" <+> name <+> "with" $$
|
|
nest 4 (ppJudgement Qualified (c,j)) $$
|
|
"in module" <+> base)
|
|
|
|
unifyAnyInfo
|
|
(ResValue (L l1 t1), ResValue (L l2 t2))
|
|
| t1==t2 -> return (ResValue (L l1 t1))
|
|
| otherwise -> fail ""
|
|
|
|
(AnyInd b1 m1, AnyInd b2 m2) -> do
|
|
testErr (b1 == b2) $ "indirection status"
|
|
testErr (m1 == m2) $ "different sources of indirection"
|
|
|
|
unifAbsDefs _ _ = fail ""
|
|
|
|
----------------------------------
|
|
|
|
Rename.hs
|
|
|
|
renameIdentTerm'
|
|
_ -> case lookupTreeManyAll showIdent opens c of
|
|
[f] -> return (f c)
|
|
[] -> alt c ("constant not found:" <+> c $$
|
|
"given" <+> fsep (punctuate ',' (map fst qualifs)))
|
|
|
|
ts@(t:_) -> do checkWarn ("atomic term" <+> ppTerm Qualified 0 t0 $$
|
|
"conflict" <+> hsep (punctuate ',' (map (ppTerm Qualified 0) ts)) $$
|
|
"given" <+> fsep (punctuate ',' (map fst qualifs)))
|
|
return t
|
|
|
|
renameInfo
|
|
renLoc ren (L loc x) =
|
|
checkInModule cwd mi loc ("Happened in the renaming of" <+> i) $ do
|
|
|
|
renameTerm
|
|
| otherwise -> checks [ renid' (Q (MN r,label2ident l)) -- .. and qualified expression second.
|
|
, renid' t >>= \t -> return (P t l) -- try as a constant at the end
|
|
, checkError ("unknown qualified constant" <+> trm)
|
|
]
|
|
|
|
renamePattern env patt =
|
|
do r@(p',vs) <- renp patt
|
|
let dupl = vs \\ nub vs
|
|
unless (null dupl) $ checkError (hang ("[C.4.13] Pattern is not linear:") 4
|
|
patt)
|
|
return r
|
|
|
|
case c' of
|
|
Q d -> renp $ PM d
|
|
_ -> checkError ("unresolved pattern" <+> patt)
|
|
|
|
Q _ -> checkError ("data constructor expected but" <+> ppTerm Qualified 0 c' <+> "is found instead")
|
|
_ -> checkError ("unresolved data constructor" <+> ppTerm Qualified 0 c')
|
|
|
|
PM c -> do
|
|
x <- renid (Q c)
|
|
c' <- case x of
|
|
(Q c') -> return c'
|
|
_ -> checkError ("not a pattern macro" <+> ppPatt Qualified 0 patt)
|
|
|
|
PV x -> checks [ renid' (Vr x) >>= \t' -> case t' of
|
|
QC c -> return (PP c [],[])
|
|
_ -> checkError (pp "not a constructor")
|
|
, return (patt, [x])
|
|
|
|
|
|
|
|
-----------------------------------
|
|
CheckGrammar.hs
|
|
|
|
checkRestrictedInheritance :: FilePath -> SourceGrammar -> SourceModule -> Check ()
|
|
let illegals = [(f,is) |
|
|
(f,cs) <- allDeps, incld f, let is = filter illegal cs, not (null is)]
|
|
case illegals of
|
|
[] -> return ()
|
|
cs -> checkWarn ("In inherited module" <+> i <> ", dependence of excluded constants:" $$
|
|
nest 2 (vcat [f <+> "on" <+> fsep is | (f,is) <- cs]))
|
|
|
|
checkCompleteGrammar :: Options -> FilePath -> Grammar -> Module -> Module -> Check Module
|
|
case info of
|
|
CncCat (Just (L loc (RecType []))) _ _ _ _ -> return (foldr (\_ -> Abs Explicit identW) (R []) cxt)
|
|
_ -> Bad "no def lin"
|
|
|
|
where noLinOf c = checkWarn ("no linearization of" <+> c)
|
|
|
|
Ok (CncCat Nothing md mr mp mpmcfg) -> do
|
|
checkWarn ("no linearization type for" <+> c <> ", inserting default {s : Str}")
|
|
return $ updateTree (c,CncCat (Just (L NoLoc defLinType)) md mr mp mpmcfg) js
|
|
_ -> do
|
|
checkWarn ("no linearization type for" <+> c <> ", inserting default {s : Str}")
|
|
|
|
_ -> do checkWarn ("function" <+> c <+> "is not in abstract")
|
|
|
|
Ok (_,AbsFun {}) ->
|
|
checkError ("lincat:"<+>c<+>"is a fun, not a cat")
|
|
-}
|
|
_ -> do checkWarn ("category" <+> c <+> "is not in abstract")
|
|
|
|
checkInfo :: Options -> FilePath -> SourceGrammar -> SourceModule -> Ident -> Info -> Check Info
|
|
(Just (L loct ty), Nothing) -> do
|
|
chIn loct "operation" $
|
|
checkError (pp "No definition given to the operation")
|
|
|
|
ResOverload os tysts -> chIn NoLoc "overloading" $ do
|
|
|
|
checkUniq xss = case xss of
|
|
x:y:xs
|
|
| x == y -> checkError $ "ambiguous for type" <+>
|
|
ppType (mkFunType (tail x) (head x))
|
|
|
|
compAbsTyp g t = case t of
|
|
Vr x -> maybe (checkError ("no value given to variable" <+> x)) return $ lookup x g
|
|
|
|
checkReservedId x =
|
|
when (isReservedWord x) $
|
|
checkWarn ("reserved word used as identifier:" <+> x)
|
|
|
|
|
|
--------------------------------
|
|
TypeCheck/Abstract.hs
|
|
|
|
grammar2theory :: SourceGrammar -> Theory
|
|
Bad s -> case lookupCatContext gr m f of
|
|
Ok cont -> return $ cont2val cont
|
|
_ -> Bad s
|
|
|
|
|
|
--------------------------------
|
|
TypeCheck/ConcreteNew.hs
|
|
-- Concrete.hs has all its code commented out
|
|
|
|
|
|
--------------------------------
|
|
TypeCheck/RConcrete.hs
|
|
-- seems to be used more than ConcreteNew
|
|
|
|
computeLType :: SourceGrammar -> Context -> Type -> Check Type
|
|
AdHocOverload ts -> do
|
|
over <- getOverload gr g (Just typeType) t
|
|
case over of
|
|
Just (tr,_) -> return tr
|
|
_ -> checkError ("unresolved overloading of constants" <+> ppTerm Qualified 0 t)
|
|
|
|
inferLType :: SourceGrammar -> Context -> Term -> Check (Term, Type)
|
|
Q (m,ident) | isPredef m -> termWith trm $ case typPredefined ident of
|
|
Nothing -> checkError ("unknown in Predef:" <+> ident)
|
|
|
|
Q ident -> checks [
|
|
checkError ("cannot infer type of constant" <+> ppTerm Unqualified 0 trm)
|
|
]
|
|
|
|
QC ident -> checks [
|
|
checkError ("cannot infer type of canonical constant" <+> ppTerm Unqualified 0 trm)
|
|
]
|
|
|
|
Vr ident -> termWith trm $ checkLookup ident g
|
|
|
|
AdHocOverload ts -> do
|
|
_ -> checkError ("unresolved overloading of constants" <+> ppTerm Qualified 0 trm)
|
|
|
|
App f a -> do
|
|
case fty' of
|
|
Prod bt z arg val -> do
|
|
_ -> checkError ("A function type is expected for" <+> ppTerm Unqualified 0 f <+> "instead of type" <+> ppType fty)
|
|
|
|
S f x -> do
|
|
_ -> checkError ("table lintype expected for the table in" $$ nest 2 (ppTerm Unqualified 0 trm))
|
|
|
|
P t i -> do
|
|
Nothing -> checkError ("unknown label" <+> i <+> "in" $$ nest 2 (ppTerm Unqualified 0 ty'))
|
|
_ -> checkError ("record type expected for:" <+> ppTerm Unqualified 0 t $$
|
|
" instead of the inferred:" <+> ppTerm Unqualified 0 ty')
|
|
|
|
R r -> do
|
|
checkCond ("cannot infer type of record" $$ nest 2 (ppTerm Unqualified 0 trm)) (length ts == length fsts)
|
|
|
|
T ti pts -> do -- tries to guess: good in oper type inference
|
|
[] -> checkError ("cannot infer table type of" <+> ppTerm Unqualified 0 trm)
|
|
|
|
---- hack from Rename.identRenameTerm, to live with files with naming conflicts 18/6/2007
|
|
Strs (Cn c : ts) | c == cConflict -> do
|
|
checkWarn ("unresolved constant, could be any of" <+> hcat (map (ppTerm Unqualified 0) ts))
|
|
|
|
ExtR r s -> do
|
|
case (rT', sT') of
|
|
(RecType rs, RecType ss) -> do
|
|
_ -> checkError ("records or record types expected in" <+> ppTerm Unqualified 0 trm)
|
|
|
|
_ -> checkError ("cannot infer lintype of" <+> ppTerm Unqualified 0 trm)
|
|
|
|
|
|
getOverload :: SourceGrammar -> Context -> Maybe Type -> Term -> Check (Maybe (Term,Type))
|
|
matchOverload f typs ttys = do
|
|
checkWarn $ "ignoring lock fields in resolving" <+> ppTerm Unqualified 0 ot $$
|
|
"for" $$
|
|
nest 2 (showTypes tys) $$
|
|
"using" $$
|
|
nest 2 (showTypes pre)
|
|
([],[]) -> do
|
|
checkError $ "no overload instance of" <+> ppTerm Unqualified 0 f $$
|
|
"for" $$
|
|
nest 2 stysError $$
|
|
"among" $$
|
|
nest 2 (vcat stypsError) $$
|
|
maybe empty (\x -> "with value type" <+> ppType x) mt
|
|
([],[(val,fun)]) -> do
|
|
checkWarn ("ignoring lock fields in resolving" <+> ppTerm Unqualified 0 ot)
|
|
(nps1,nps2) -> do
|
|
checkWarn $ "ambiguous overloading of" <+> ppTerm Unqualified 0 f <+>
|
|
---- "with argument types" <+> hsep (map (ppTerm Qualified 0) tys) $$
|
|
"resolved by selecting the first of the alternatives" $$
|
|
nest 2 (vcat [ppTerm Qualified 0 fun | (_,ty,fun) <- vfs1 ++ if null vfs1 then vfs2 else []])
|
|
case [(mkApp fun tts,val) | (val,fun) <- nps1 ++ nps2] of
|
|
[] -> checkError $ "no alternatives left when resolving" <+> ppTerm Unqualified 0 f
|
|
|
|
checkLType :: SourceGrammar -> Context -> Term -> Type -> Check (Term, Type)
|
|
Abs bt x c -> do
|
|
case typ of
|
|
Prod bt' z a b -> do
|
|
_ -> checkError $ "function type expected instead of" <+> ppType typ
|
|
AdHocOverload ts -> do
|
|
_ -> checkError ("unresolved overloading of constants" <+> ppTerm Qualified 0 trm)
|
|
T _ [] ->
|
|
checkError ("found empty table in type" <+> ppTerm Unqualified 0 typ)
|
|
T _ cs -> case typ of
|
|
else checkWarn ("patterns never reached:" $$
|
|
nest 2 (vcat (map (ppPatt Unqualified 0) ps)))
|
|
_ -> checkError $ "table type expected for table instead of" $$ nest 2 (ppType typ)
|
|
V arg0 vs ->
|
|
if length vs1 == length vs
|
|
then return ()
|
|
else checkError $ "wrong number of values in table" <+> ppTerm Unqualified 0 trm
|
|
|
|
R r -> case typ of --- why needed? because inference may be too difficult
|
|
RecType rr -> do
|
|
_ -> checkError ("record type expected in type checking instead of" $$ nest 2 (ppTerm Unqualified 0 typ))
|
|
|
|
ExtR r s -> case typ of
|
|
case trm' of
|
|
RecType _ -> termWith trm' $ return typeType
|
|
ExtR (Vr _) (RecType _) -> termWith trm' $ return typeType
|
|
-- ext t = t ** ...
|
|
_ -> checkError ("invalid record type extension" <+> nest 2 (ppTerm Unqualified 0 trm))
|
|
|
|
case typ2 of
|
|
RecType ss -> return $ map fst ss
|
|
_ -> checkError ("cannot get labels from" $$ nest 2 (ppTerm Unqualified 0 typ2))
|
|
_ -> checkError ("record extension not meaningful for" <+> ppTerm Unqualified 0 typ)
|
|
|
|
S tab arg -> checks [ do
|
|
_ -> checkError ("table type expected for applied table instead of" <+> ppType ty')
|
|
|
|
_ -> do
|
|
(trm',ty') <- inferLType gr g trm
|
|
termWith trm' $ checkEqLType gr g typ ty' trm'
|
|
|
|
checkM rms (l,ty) = case lookup l rms of
|
|
_ -> checkError $
|
|
if isLockLabel l
|
|
then let cat = drop 5 (showIdent (label2ident l))
|
|
in ppTerm Unqualified 0 (R rms) <+> "is not in the lincat of" <+> cat <>
|
|
"; try wrapping it with lin" <+> cat
|
|
else "cannot find value for label" <+> l <+> "in" <+> ppTerm Unqualified 0 (R rms)
|
|
|
|
checkEqLType :: SourceGrammar -> Context -> Type -> Type -> Term -> Check Type
|
|
False -> checkError $ s <+> "type of" <+> ppTerm Unqualified 0 trm $$
|
|
"expected:" <+> ppTerm Qualified 0 t $$ -- ppqType t u $$
|
|
"inferred:" <+> ppTerm Qualified 0 u -- ppqType u t
|
|
|
|
checkIfEqLType :: SourceGrammar -> Context -> Type -> Type -> Term -> Check (Bool,Type,Type,String)
|
|
Ok lo -> do
|
|
checkWarn $ "missing lock field" <+> fsep lo
|
|
|
|
missingLock g t u = case (t,u) of
|
|
_:_ -> Bad $ render ("missing record fields:" <+> fsep (punctuate ',' (others)))
|
|
|
|
|
|
|
|
pattContext :: SourceGrammar -> Context -> Type -> Patt -> Check Context
|
|
checkCond ("wrong number of arguments for constructor in" <+> ppPatt Unqualified 0 p)
|
|
(length cont == length ps)
|
|
PR r -> do
|
|
_ -> checkError ("record type expected for pattern instead of" <+> ppTerm Unqualified 0 typ')
|
|
|
|
PAlt p' q -> do
|
|
g1 <- pattContext env g typ p'
|
|
g2 <- pattContext env g typ q
|
|
let pts = nub ([x | pt@(_,x,_) <- g1, notElem pt g2] ++ [x | pt@(_,x,_) <- g2, notElem pt g1])
|
|
checkCond
|
|
("incompatible bindings of" <+>
|
|
fsep pts <+>
|
|
"in pattern alterantives" <+> ppPatt Unqualified 0 p) (null pts)
|
|
return g1 -- must be g1 == g2
|
|
|
|
noBind typ p' = do
|
|
co <- pattContext env g typ p'
|
|
if not (null co)
|
|
then checkWarn ("no variable bound inside pattern" <+> ppPatt Unqualified 0 p)
|
|
>> return []
|
|
else return []
|
|
|
|
checkLookup :: Ident -> Context -> Check Type -- used for looking up Vr x type in context
|
|
[] -> checkError ("unknown variable" <+> x)
|
|
|
|
|
|
|
|
-------------------------------
|
|
Grammar/Lookup.hs
|
|
|
|
lookupIdent :: ErrorMonad m => Ident -> BinTree Ident b -> m b
|
|
Bad _ -> raise ("unknown identifier" +++ showIdent c)
|
|
|
|
lookupResDefLoc
|
|
_ -> raise $ render (c <+> "is not defined in resource" <+> m)
|
|
|
|
lookupResType :: ErrorMonad m => Grammar -> QIdent -> m Type
|
|
_ -> raise $ render (c <+> "has no type defined in resource" <+> m)
|
|
|
|
lookupOverloadTypes :: ErrorMonad m => Grammar -> QIdent -> m [(Term,Type)]
|
|
_ -> raise $ render (c <+> "has no types defined in resource" <+> m)
|
|
|
|
lookupOverload :: ErrorMonad m => Grammar -> QIdent -> m [([Type],(Type,Term))]
|
|
_ -> raise $ render (c <+> "is not an overloaded operation")
|
|
|
|
|
|
lookupParamValues :: ErrorMonad m => Grammar -> QIdent -> m [Term]
|
|
case info of
|
|
ResParam _ (Just pvs) -> return pvs
|
|
_ -> raise $ render (ppQIdent Qualified c <+> "has no parameter values defined")
|
|
|
|
|
|
allParamValues :: ErrorMonad m => Grammar -> Type -> m [Term]
|
|
_ -> raise (render ("cannot find parameter values for" <+> ptyp))
|
|
|
|
|
|
lookupFunType :: ErrorMonad m => Grammar -> ModuleName -> Ident -> m Type
|
|
_ -> raise (render ("cannot find type of" <+> c))
|
|
|
|
lookupCatContext :: ErrorMonad m => Grammar -> ModuleName -> Ident -> m Context
|
|
_ -> raise (render ("unknown category" <+> c))
|
|
|
|
|
|
-------------------------
|
|
PatternMatch.hs
|
|
|
|
matchPattern :: ErrorMonad m => [(Patt,rhs)] -> Term -> m (rhs, Substitution)
|
|
if not (isInConstantForm term)
|
|
then raise (render ("variables occur in" <+> pp term))
|
|
|
|
findMatch :: ErrorMonad m => [([Patt],rhs)] -> [Term] -> m (rhs, Substitution)
|
|
[] -> raise (render ("no applicable case for" <+> hsep (punctuate ',' terms)))
|
|
(patts,_):_ | length patts /= length terms ->
|
|
raise (render ("wrong number of args for patterns :" <+> hsep patts <+>
|
|
"cannot take" <+> hsep terms))
|
|
|
|
tryMatch :: (Patt, Term) -> Err [(Ident, Term)]
|
|
(PNeg p',_) -> case tryMatch (p',t) of
|
|
Bad _ -> return []
|
|
_ -> raise (render ("no match with negative pattern" <+> p))
|
|
|
|
|
|
---------------------------------------------
|
|
Compile.Optimize.hs
|
|
|
|
mkLinDefault :: SourceGrammar -> Type -> Err Term
|
|
_ -> Bad (render ("no parameter values given to type" <+> ppQIdent Qualified p))
|
|
_ -> Bad (render ("linearization type field cannot be" <+> typ))
|
|
|
|
mkLinReference :: SourceGrammar -> Type -> Err Term
|
|
[] -> Bad "no string"
|
|
|
|
|
|
---------------------------------------------
|
|
Compile.Compute.Concrete.hs
|
|
|
|
nfx env@(GE _ _ _ loc) t = do
|
|
Left i -> fail ("variable #"++show i++" is out of scope")
|
|
|
|
var :: CompleteEnv -> Ident -> Err OpenValue
|
|
var env x = maybe unbound pick' (elemIndex x (local env))
|
|
where
|
|
unbound = fail ("Unknown variable: "++showIdent x)
|
|
pick' i = return $ \ vs -> maybe (err i vs) ok (pick i vs)
|
|
err i vs = bug $ "Stack problem: "++showIdent x++": "
|
|
++unwords (map showIdent (local env))
|
|
++" => "++show (i,length vs)
|
|
|
|
resource env (m,c) =
|
|
where e = fail $ "Not found: "++render m++"."++showIdent c
|
|
|
|
extR t vv =
|
|
(VRecType rs1, VRecType rs2) ->
|
|
case intersect (map fst rs1) (map fst rs2) of
|
|
[] -> VRecType (rs1 ++ rs2)
|
|
ls -> error $ "clash"<+>show ls
|
|
(v1,v2) -> error $ "not records" $$ show v1 $$ show v2
|
|
where
|
|
error explain = ppbug $ "The term" <+> t
|
|
<+> "is not reducible" $$ explain
|
|
|
|
glue env (v1,v2) = glu v1 v2
|
|
ppL loc (hang "unsupported token gluing:" 4
|
|
(Glue (vt v1) (vt v2)))
|
|
|
|
strsFromValue :: Value -> Err [Str]
|
|
_ -> fail ("cannot get Str from value " ++ show t)
|
|
|
|
match loc cs v =
|
|
case value2term loc [] v of
|
|
Left i -> bad ("variable #"++show i++" is out of scope")
|
|
Right t -> err bad return (matchPattern cs t)
|
|
where
|
|
bad = fail . ("In pattern matching: "++)
|
|
|
|
inlinePattMacro p =
|
|
VPatt p' -> inlinePattMacro p'
|
|
_ -> ppbug $ hang "Expected pattern macro:" 4
|
|
|
|
linPattVars p =
|
|
if null dups
|
|
then return pvs
|
|
else fail.render $ hang "Pattern is not linear:" 4 (ppPatt Unqualified 0 p)
|
|
|
|
---------------------------------------------
|
|
Compile.Compute.Abstract.hs
|
|
|
|
|
|
---------------------------------------------
|
|
PGF.Linearize.hs
|
|
|
|
bracketedLinearize :: PGF -> Language -> Tree -> [BracketedString]
|
|
cnc = lookMap (error "no lang") lang (concretes pgf)
|
|
|
|
|
|
---------------------------------------------
|
|
PGF.TypeCheck.hs
|
|
|
|
ppTcError :: TcError -> Doc
|
|
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
|
|
ppTcError (UnexpectedImplArg xs e) = braces (ppExpr 0 xs e) <+> text "is implicit argument but not implicit argument is expected here"
|
|
ppTcError (UnsolvableGoal xs metaid ty)= text "The goal:" <+> ppMeta metaid <+> colon <+> ppType 0 xs ty $$
|
|
text "cannot be solved"
|
|
|