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"