mirror of
https://github.com/GrammaticalFramework/gf-core.git
synced 2026-05-05 01:02:51 -06:00
store and propagate the exact source location for all judgements in the grammar. It may not be used accurately in the error messages yet
This commit is contained in:
@@ -72,9 +72,9 @@ checkContext st = checkTyp st . cont2exp
|
||||
checkTyp :: SourceGrammar -> Type -> [Message]
|
||||
checkTyp gr typ = err (\x -> [text x]) ppConstrs $ justTypeCheck gr typ vType
|
||||
|
||||
checkDef :: SourceGrammar -> Fun -> Type -> [Equation] -> [Message]
|
||||
checkDef :: SourceGrammar -> Fun -> Type -> [L Equation] -> [Message]
|
||||
checkDef gr (m,fun) typ eqs = err (\x -> [text x]) ppConstrs $ do
|
||||
bcs <- mapM (\b -> checkBranch (grammar2theory gr) (initTCEnv []) b (type2val typ)) eqs
|
||||
bcs <- mapM (\(L _ b) -> checkBranch (grammar2theory gr) (initTCEnv []) b (type2val typ)) eqs
|
||||
let (bs,css) = unzip bcs
|
||||
(constrs,_) <- unifyVal (concat css)
|
||||
return $ filter notJustMeta constrs
|
||||
|
||||
@@ -94,7 +94,8 @@ checkCompleteGrammar gr (am,abs) (cm,cnc) = do
|
||||
where
|
||||
checkAbs js i@(c,info) =
|
||||
case info of
|
||||
AbsFun (Just ty) _ _ -> do let mb_def = do
|
||||
AbsFun (Just (L loc ty)) _ _
|
||||
-> do let mb_def = do
|
||||
let (cxt,(_,i),_) = typeForm ty
|
||||
info <- lookupIdent i js
|
||||
info <- case info of
|
||||
@@ -102,8 +103,8 @@ checkCompleteGrammar gr (am,abs) (cm,cnc) = do
|
||||
return info
|
||||
_ -> return info
|
||||
case info of
|
||||
CncCat (Just (RecType [])) _ _ -> return (foldr (\_ -> Abs Explicit identW) (R []) cxt)
|
||||
_ -> Bad "no def lin"
|
||||
CncCat (Just (L loc (RecType []))) _ _ -> return (foldr (\_ -> Abs Explicit identW) (R []) cxt)
|
||||
_ -> Bad "no def lin"
|
||||
|
||||
case lookupIdent c js of
|
||||
Ok (AnyInd _ _) -> return js
|
||||
@@ -111,14 +112,14 @@ checkCompleteGrammar gr (am,abs) (cm,cnc) = do
|
||||
return $ updateTree (c,CncFun ty (Just def) pn) js
|
||||
Ok (CncFun ty Nothing pn) ->
|
||||
case mb_def of
|
||||
Ok def -> return $ updateTree (c,CncFun ty (Just def) pn) js
|
||||
Ok def -> return $ updateTree (c,CncFun ty (Just (L (0,0) def)) pn) js
|
||||
Bad _ -> do checkWarn $ text "no linearization of" <+> ppIdent c
|
||||
return js
|
||||
_ -> do
|
||||
case mb_def of
|
||||
Ok def -> do (cont,val) <- linTypeOfType gr cm ty
|
||||
let linty = (snd (valCat ty),cont,val)
|
||||
return $ updateTree (c,CncFun (Just linty) (Just def) Nothing) js
|
||||
return $ updateTree (c,CncFun (Just linty) (Just (L (0,0) def)) Nothing) js
|
||||
Bad _ -> do checkWarn $ text "no linearization of" <+> ppIdent c
|
||||
return js
|
||||
AbsCat (Just _) -> case lookupIdent c js of
|
||||
@@ -127,17 +128,17 @@ checkCompleteGrammar gr (am,abs) (cm,cnc) = do
|
||||
Ok (CncCat _ mt mp) -> do
|
||||
checkWarn $
|
||||
text "no linearization type for" <+> ppIdent c <> text ", inserting default {s : Str}"
|
||||
return $ updateTree (c,CncCat (Just defLinType) mt mp) js
|
||||
return $ updateTree (c,CncCat (Just (L (0,0) defLinType)) mt mp) js
|
||||
_ -> do
|
||||
checkWarn $
|
||||
text "no linearization type for" <+> ppIdent c <> text ", inserting default {s : Str}"
|
||||
return $ updateTree (c,CncCat (Just defLinType) Nothing Nothing) js
|
||||
return $ updateTree (c,CncCat (Just (L (0,0) defLinType)) Nothing Nothing) js
|
||||
_ -> return js
|
||||
|
||||
checkCnc js i@(c,info) =
|
||||
case info of
|
||||
CncFun _ d pn -> case lookupOrigInfo gr am c of
|
||||
Ok (_,AbsFun (Just ty) _ _) ->
|
||||
Ok (_,AbsFun (Just (L _ ty)) _ _) ->
|
||||
do (cont,val) <- linTypeOfType gr cm ty
|
||||
let linty = (snd (valCat ty),cont,val)
|
||||
return $ updateTree (c,CncFun (Just linty) d pn) js
|
||||
@@ -156,50 +157,51 @@ checkInfo :: [SourceModule] -> SourceModule -> Ident -> Info -> Check Info
|
||||
checkInfo ms (m,mo) c info = do
|
||||
checkReservedId c
|
||||
case info of
|
||||
AbsCat (Just cont) -> mkCheck "category" $
|
||||
checkContext gr cont
|
||||
AbsCat (Just (L loc cont)) ->
|
||||
mkCheck loc "category" $
|
||||
checkContext gr cont
|
||||
|
||||
AbsFun (Just typ0) ma md -> do
|
||||
AbsFun (Just (L loc typ0)) ma md -> do
|
||||
typ <- compAbsTyp [] typ0 -- to calculate let definitions
|
||||
mkCheck "type of function" $
|
||||
mkCheck loc "type of function" $
|
||||
checkTyp gr typ
|
||||
case md of
|
||||
Just eqs -> mkCheck "definition of function" $
|
||||
Just eqs -> mkCheck loc "definition of function" $
|
||||
checkDef gr (m,c) typ eqs
|
||||
Nothing -> return info
|
||||
return (AbsFun (Just typ) ma md)
|
||||
return (AbsFun (Just (L loc typ)) ma md)
|
||||
|
||||
CncFun linty@(Just (cat,cont,val)) (Just trm) mpr -> chIn "linearization of" $ do
|
||||
CncFun linty@(Just (cat,cont,val)) (Just (L loc trm)) mpr -> chIn loc "linearization of" $ do
|
||||
(trm',_) <- checkLType gr [] trm (mkFunType (map (\(_,_,ty) -> ty) cont) val) -- erases arg vars
|
||||
mpr <- checkPrintname gr mpr
|
||||
return (CncFun linty (Just trm') mpr)
|
||||
return (CncFun linty (Just (L loc trm')) mpr)
|
||||
|
||||
CncCat (Just typ) mdef mpr -> chIn "linearization type of" $ do
|
||||
CncCat (Just (L loc typ)) mdef mpr -> chIn loc "linearization type of" $ do
|
||||
(typ,_) <- checkLType gr [] typ typeType
|
||||
typ <- computeLType gr [] typ
|
||||
mdef <- case mdef of
|
||||
Just def -> do
|
||||
Just (L loc def) -> do
|
||||
(def,_) <- checkLType gr [] def (mkFunType [typeStr] typ)
|
||||
return $ Just def
|
||||
return $ Just (L loc def)
|
||||
_ -> return mdef
|
||||
mpr <- checkPrintname gr mpr
|
||||
return (CncCat (Just typ) mdef mpr)
|
||||
return (CncCat (Just (L loc typ)) mdef mpr)
|
||||
|
||||
ResOper pty pde -> chIn "operation" $ do
|
||||
ResOper pty pde -> chIn (0,0) "operation" $ do
|
||||
(pty', pde') <- case (pty,pde) of
|
||||
(Just ty, Just de) -> do
|
||||
(Just (L loc1 ty), Just (L loc2 de)) -> do
|
||||
ty' <- checkLType gr [] ty typeType >>= computeLType gr [] . fst
|
||||
(de',_) <- checkLType gr [] de ty'
|
||||
return (Just ty', Just de')
|
||||
(_ , Just de) -> do
|
||||
return (Just (L loc1 ty'), Just (L loc2 de'))
|
||||
(_ , Just (L loc de)) -> do
|
||||
(de',ty') <- inferLType gr [] de
|
||||
return (Just ty', Just de')
|
||||
return (Just (L loc ty'), Just (L loc de'))
|
||||
(_ , Nothing) -> do
|
||||
checkError (text "No definition given to the operation")
|
||||
return (ResOper pty' pde')
|
||||
|
||||
ResOverload os tysts -> chIn "overloading" $ do
|
||||
tysts' <- mapM (uncurry $ flip (checkLType gr [])) tysts -- return explicit ones
|
||||
ResOverload os tysts -> chIn (0,0) "overloading" $ do
|
||||
tysts' <- mapM (uncurry $ flip (\(L loc1 t) (L loc2 ty) -> checkLType gr [] t ty >>= \(t,ty) -> return (L loc1 t, L loc2 ty))) tysts -- return explicit ones
|
||||
tysts0 <- checkErr $ lookupOverload gr m c -- check against inherited ones too
|
||||
tysts1 <- mapM (uncurry $ flip (checkLType gr []))
|
||||
[(mkFunType args val,tr) | (args,(val,tr)) <- tysts0]
|
||||
@@ -209,16 +211,16 @@ checkInfo ms (m,mo) c info = do
|
||||
sort [let (xs,t) = typeFormCnc x in t : map (\(b,x,t) -> t) xs | (_,x) <- tysts1]
|
||||
return (ResOverload os [(y,x) | (x,y) <- tysts'])
|
||||
|
||||
ResParam (Just pcs) _ -> chIn "parameter type" $ do
|
||||
ResParam (Just pcs) _ -> chIn (0,0) "parameter type" $ do
|
||||
ts <- checkErr $ liftM concat $ mapM mkPar pcs
|
||||
return (ResParam (Just pcs) (Just ts))
|
||||
|
||||
_ -> return info
|
||||
where
|
||||
gr = MGrammar ((m,mo) : ms)
|
||||
chIn cat = checkIn (text "Happened in" <+> text cat <+> ppIdent c <+> ppPosition mo c <> colon)
|
||||
chIn loc cat = checkIn (text "Happened in" <+> text cat <+> ppIdent c <+> ppPosition m loc <> colon)
|
||||
|
||||
mkPar (f,co) = do
|
||||
mkPar (L _ (f,co)) = do
|
||||
vs <- liftM combinations $ mapM (\(_,_,ty) -> allParamValues gr ty) co
|
||||
return $ map (mkApp (QC m f)) vs
|
||||
|
||||
@@ -229,9 +231,9 @@ checkInfo ms (m,mo) c info = do
|
||||
| otherwise -> checkUniq $ y:xs
|
||||
_ -> return ()
|
||||
|
||||
mkCheck cat ss = case ss of
|
||||
mkCheck loc cat ss = case ss of
|
||||
[] -> return info
|
||||
_ -> checkError (vcat ss $$ text "in" <+> text cat <+> ppIdent c <+> ppPosition mo c)
|
||||
_ -> checkError (vcat ss $$ text "in" <+> text cat <+> ppIdent c <+> ppPosition m loc)
|
||||
|
||||
compAbsTyp g t = case t of
|
||||
Vr x -> maybe (checkError (text "no value given to variable" <+> ppIdent x)) return $ lookup x g
|
||||
@@ -246,10 +248,10 @@ checkInfo ms (m,mo) c info = do
|
||||
_ -> composOp (compAbsTyp g) t
|
||||
|
||||
|
||||
checkPrintname :: SourceGrammar -> Maybe Term -> Check (Maybe Term)
|
||||
checkPrintname gr (Just t) = do (t,_) <- checkLType gr [] t typeStr
|
||||
return (Just t)
|
||||
checkPrintname gr Nothing = return Nothing
|
||||
checkPrintname :: SourceGrammar -> Maybe (L Term) -> Check (Maybe (L Term))
|
||||
checkPrintname gr (Just (L loc t)) = do (t,_) <- checkLType gr [] t typeStr
|
||||
return (Just (L loc t))
|
||||
checkPrintname gr Nothing = return Nothing
|
||||
|
||||
-- | for grammars obtained otherwise than by parsing ---- update!!
|
||||
checkReservedId :: Ident -> Check ()
|
||||
|
||||
@@ -25,13 +25,15 @@ codeSourceModule co (id,mo) = (id,replaceJudgements mo (mapTree codj (jments mo)
|
||||
CncFun mty pt mpr -> CncFun mty (fmap (codeTerm co) pt) (fmap (codeTerm co) mpr)
|
||||
_ -> info
|
||||
|
||||
codeTerm :: (String -> String) -> Term -> Term
|
||||
codeTerm co t = case t of
|
||||
K s -> K (co s)
|
||||
T ty cs -> T ty [(codp p,codeTerm co v) | (p,v) <- cs]
|
||||
EPatt p -> EPatt (codp p)
|
||||
_ -> composSafeOp (codeTerm co) t
|
||||
codeTerm :: (String -> String) -> L Term -> L Term
|
||||
codeTerm co (L loc t) = L loc (codt t)
|
||||
where
|
||||
codt t = case t of
|
||||
K s -> K (co s)
|
||||
T ty cs -> T ty [(codp p,codt v) | (p,v) <- cs]
|
||||
EPatt p -> EPatt (codp p)
|
||||
_ -> composSafeOp codt t
|
||||
|
||||
codp p = case p of --- really: composOpPatt
|
||||
PR rs -> PR [(l,codp p) | (l,p) <- rs]
|
||||
PString s -> PString (co s)
|
||||
|
||||
@@ -60,7 +60,7 @@ canon2pgf opts pars cgr@(M.MGrammar ((a,abm):cms)) = do
|
||||
gflags = Map.empty
|
||||
aflags = Map.fromList [(mkCId f,C.LStr x) | (f,x) <- optionsPGF (M.flags abm)]
|
||||
|
||||
mkDef (Just eqs) = Just [C.Equ ps' (mkExp scope' e) | (ps,e) <- eqs, let (scope',ps') = mapAccumL mkPatt [] ps]
|
||||
mkDef (Just eqs) = Just [C.Equ ps' (mkExp scope' e) | L _ (ps,e) <- eqs, let (scope',ps') = mapAccumL mkPatt [] ps]
|
||||
mkDef Nothing = Nothing
|
||||
|
||||
mkArrity (Just a) = a
|
||||
@@ -68,10 +68,10 @@ canon2pgf opts pars cgr@(M.MGrammar ((a,abm):cms)) = do
|
||||
|
||||
-- concretes
|
||||
lfuns = [(f', (mkType [] ty, mkArrity ma, mkDef pty)) |
|
||||
(f,AbsFun (Just ty) ma pty) <- tree2list (M.jments abm), let f' = i2i f]
|
||||
(f,AbsFun (Just (L _ ty)) ma pty) <- tree2list (M.jments abm), let f' = i2i f]
|
||||
funs = Map.fromAscList lfuns
|
||||
lcats = [(i2i c, snd (mkContext [] cont)) |
|
||||
(c,AbsCat (Just cont)) <- tree2list (M.jments abm)]
|
||||
(c,AbsCat (Just (L _ cont))) <- tree2list (M.jments abm)]
|
||||
cats = Map.fromAscList lcats
|
||||
catfuns = Map.fromList
|
||||
[(cat,[f | (f, (C.DTyp _ c _,_,_)) <- lfuns, c==cat]) | (cat,_) <- lcats]
|
||||
@@ -91,16 +91,16 @@ canon2pgf opts pars cgr@(M.MGrammar ((a,abm):cms)) = do
|
||||
---- then (trace "decode" D.convertStringsInTerm decodeUTF8) else id
|
||||
umkTerm = utf . mkTerm
|
||||
lins = Map.fromAscList
|
||||
[(f', umkTerm tr) | (f,CncFun _ (Just tr) _) <- js,
|
||||
[(f', umkTerm tr) | (f,CncFun _ (Just (L _ tr)) _) <- js,
|
||||
let f' = i2i f, exists f'] -- eliminating lins without fun
|
||||
-- needed even here because of restricted inheritance
|
||||
lincats = Map.fromAscList
|
||||
[(i2i c, mkCType ty) | (c,CncCat (Just ty) _ _) <- js]
|
||||
[(i2i c, mkCType ty) | (c,CncCat (Just (L _ ty)) _ _) <- js]
|
||||
lindefs = Map.fromAscList
|
||||
[(i2i c, umkTerm tr) | (c,CncCat _ (Just tr) _) <- js]
|
||||
[(i2i c, umkTerm tr) | (c,CncCat _ (Just (L _ tr)) _) <- js]
|
||||
printnames = Map.union
|
||||
(Map.fromAscList [(i2i f, realize (umkTerm tr)) | (f,CncFun _ _ (Just tr)) <- js])
|
||||
(Map.fromAscList [(i2i f, realize (umkTerm tr)) | (f,CncCat _ _ (Just tr)) <- js])
|
||||
(Map.fromAscList [(i2i f, realize (umkTerm tr)) | (f,CncFun _ _ (Just (L _ tr))) <- js])
|
||||
(Map.fromAscList [(i2i f, realize (umkTerm tr)) | (f,CncCat _ _ (Just (L _ tr))) <- js])
|
||||
params = Map.fromAscList
|
||||
[(i2i c, pars lang0 c) | (c,CncCat (Just ty) _ _) <- js]
|
||||
fcfg = Nothing
|
||||
@@ -236,16 +236,15 @@ mkParamLincat sgr lang cat = errVal (C.R [C.S []]) $ do
|
||||
|
||||
reorder :: Ident -> SourceGrammar -> SourceGrammar
|
||||
reorder abs cg = M.MGrammar $
|
||||
(abs, M.ModInfo M.MTAbstract M.MSComplete aflags [] Nothing [] [] adefs poss):
|
||||
[(c, M.ModInfo (M.MTConcrete abs) M.MSComplete fs [] Nothing [] [] (sorted2tree js) poss)
|
||||
(abs, M.ModInfo M.MTAbstract M.MSComplete aflags [] Nothing [] [] adefs):
|
||||
[(c, M.ModInfo (M.MTConcrete abs) M.MSComplete fs [] Nothing [] [] (sorted2tree js))
|
||||
| (c,(fs,js)) <- cncs]
|
||||
where
|
||||
poss = emptyBinTree -- positions no longer needed
|
||||
mos = M.modules cg
|
||||
adefs = sorted2tree $ sortIds $
|
||||
predefADefs ++ Look.allOrigInfos cg abs
|
||||
predefADefs =
|
||||
[(c, AbsCat (Just [])) | c <- [cFloat,cInt,cString]]
|
||||
[(c, AbsCat (Just (L (0,0) []))) | c <- [cFloat,cInt,cString]]
|
||||
aflags =
|
||||
concatOptions [M.flags mo | (_,mo) <- M.modules cg, M.isModAbs mo]
|
||||
|
||||
@@ -259,7 +258,7 @@ reorder abs cg = M.MGrammar $
|
||||
Just r <- [lookup i (M.allExtendSpecs cg la)]]
|
||||
|
||||
predefCDefs =
|
||||
[(c, CncCat (Just GM.defLinType) Nothing Nothing) | c <- [cInt,cFloat,cString]]
|
||||
[(c, CncCat (Just (L (0,0) GM.defLinType)) Nothing Nothing) | c <- [cInt,cFloat,cString]]
|
||||
|
||||
sortIds = sortBy (\ (f,_) (g,_) -> compare f g)
|
||||
|
||||
@@ -292,8 +291,8 @@ canon2canon opts abs cg0 =
|
||||
j2j cg (f,j) =
|
||||
let debug = if verbAtLeast opts Verbose then trace ("+ " ++ showIdent f) else id in
|
||||
case j of
|
||||
CncFun x (Just tr) z -> CncFun x (Just (debug (t2t (unfactor cg0 tr)))) z
|
||||
CncCat (Just ty) (Just x) y -> CncCat (Just (ty2ty ty)) (Just (t2t (unfactor cg0 x))) y
|
||||
CncFun x (Just (L loc tr)) z -> CncFun x (Just (L loc (debug (t2t (unfactor cg0 tr))))) z
|
||||
CncCat (Just (L locty ty)) (Just (L locx x)) y -> CncCat (Just (L locty (ty2ty ty))) (Just (L locx (t2t (unfactor cg0 x)))) y
|
||||
_ -> j
|
||||
where
|
||||
cg1 = cg
|
||||
@@ -315,7 +314,7 @@ canon2canon opts abs cg0 =
|
||||
-- flatten record arguments of param constructors
|
||||
p2p (f,j) = case j of
|
||||
ResParam (Just ps) (Just vs) ->
|
||||
ResParam (Just [(c,concatMap unRec cont) | (c,cont) <- ps]) (Just (map unrec vs))
|
||||
ResParam (Just [L loc (c,concatMap unRec cont) | L loc (c,cont) <- ps]) (Just (map unrec vs))
|
||||
_ -> j
|
||||
unRec (bt,x,ty) = case ty of
|
||||
RecType fs -> [ity | (_,typ) <- fs, ity <- unRec (Explicit,identW,typ)]
|
||||
@@ -359,13 +358,13 @@ paramValues cgr = (labels,untyps,typs) where
|
||||
partyps = nub $
|
||||
--- [App (Q (IC "Predef") (IC "Ints")) (EInt i) | i <- [1,9]] ---linTypeInt
|
||||
[ty |
|
||||
(_,(_,CncCat (Just ty0) _ _)) <- jments,
|
||||
(_,(_,CncCat (Just (L _ ty0)) _ _)) <- jments,
|
||||
ty <- typsFrom ty0
|
||||
] ++ [
|
||||
Q m ty |
|
||||
(m,(ty,ResParam _ _)) <- jments
|
||||
] ++ [ty |
|
||||
(_,(_,CncFun _ (Just tr) _)) <- jments,
|
||||
(_,(_,CncFun _ (Just (L _ tr)) _)) <- jments,
|
||||
ty <- err (const []) snd $ appSTM (typsFromTrm tr) []
|
||||
]
|
||||
params = [(ty, errVal (traceD ("UNKNOWN PARAM TYPE" +++ show ty) []) $
|
||||
@@ -407,7 +406,7 @@ paramValues cgr = (labels,untyps,typs) where
|
||||
[(cat,[f | let RecType fs = GM.defLinType, f <- fs]) | cat <- [cInt,cFloat, cString]] ++
|
||||
reverse ---- TODO: really those lincats that are reached
|
||||
---- reverse is enough to expel overshadowed ones...
|
||||
[(cat,ls) | (_,(cat,CncCat (Just ty) _ _)) <- jments,
|
||||
[(cat,ls) | (_,(cat,CncCat (Just (L _ ty)) _ _)) <- jments,
|
||||
RecType ls <- [unlockTy ty]]
|
||||
labels = Map.fromList $ concat
|
||||
[((cat,[lab]),(typ,i)):
|
||||
|
||||
@@ -64,24 +64,24 @@ evalInfo opts ms m c info = do
|
||||
|
||||
CncCat ptyp pde ppr -> do
|
||||
pde' <- case (ptyp,pde) of
|
||||
(Just typ, Just de) -> do
|
||||
(Just (L _ typ), Just (L loc de)) -> do
|
||||
de <- partEval opts gr ([(Explicit, varStr, typeStr)], typ) de
|
||||
return (Just (factor param c 0 de))
|
||||
(Just typ, Nothing) -> do
|
||||
return (Just (L loc (factor param c 0 de)))
|
||||
(Just (L loc typ), Nothing) -> do
|
||||
de <- mkLinDefault gr typ
|
||||
de <- partEval opts gr ([(Explicit, varStr, typeStr)], typ) de
|
||||
return (Just (factor param c 0 de))
|
||||
return (Just (L loc (factor param c 0 de)))
|
||||
_ -> return pde -- indirection
|
||||
|
||||
ppr' <- liftM Just $ evalPrintname gr c ppr (Just $ K $ showIdent c)
|
||||
ppr' <- liftM Just $ evalPrintname gr c ppr (Just (L (0,0) (K $ showIdent c)))
|
||||
|
||||
return (CncCat ptyp pde' ppr')
|
||||
|
||||
CncFun (mt@(Just (_,cont,val))) pde ppr -> --trace (prt c) $
|
||||
eIn (text "linearization in type" <+> ppTerm Unqualified 0 (mkProd cont val []) $$ text "of function") $ do
|
||||
pde' <- case pde of
|
||||
Just de -> do de <- partEval opts gr (cont,val) de
|
||||
return (Just (factor param c 0 de))
|
||||
Just (L loc de) -> do de <- partEval opts gr (cont,val) de
|
||||
return (Just (L loc (factor param c 0 de)))
|
||||
Nothing -> return pde
|
||||
ppr' <- liftM Just $ evalPrintname gr c ppr pde'
|
||||
return $ CncFun mt pde' ppr' -- only cat in type actually needed
|
||||
@@ -89,8 +89,8 @@ evalInfo opts ms m c info = do
|
||||
ResOper pty pde
|
||||
| OptExpand `Set.member` optim -> do
|
||||
pde' <- case pde of
|
||||
Just de -> do de <- computeConcrete gr de
|
||||
return (Just (factor param c 0 de))
|
||||
Just (L loc de) -> do de <- computeConcrete gr de
|
||||
return (Just (L loc (factor param c 0 de)))
|
||||
Nothing -> return Nothing
|
||||
return $ ResOper pty pde'
|
||||
|
||||
@@ -161,13 +161,14 @@ mkLinDefault gr typ = liftM (Abs Explicit varStr) $ mkDefField typ
|
||||
-- lin for functions, cat name for cats (dispatch made in evalCncDef above).
|
||||
--- We cannot use linearization at this stage, since we do not know the
|
||||
--- defaults we would need for question marks - and we're not yet in canon.
|
||||
evalPrintname :: SourceGrammar -> Ident -> Maybe Term -> Maybe Term -> Err Term
|
||||
evalPrintname :: SourceGrammar -> Ident -> Maybe (L Term) -> Maybe (L Term) -> Err (L Term)
|
||||
evalPrintname gr c ppr lin =
|
||||
case ppr of
|
||||
Just pr -> comp pr
|
||||
Just (L loc pr) -> do pr <- comp pr
|
||||
return (L loc pr)
|
||||
Nothing -> case lin of
|
||||
Just t -> return $ K $ clean $ render (ppTerm Unqualified 0 (oneBranch t))
|
||||
Nothing -> return $ K $ showIdent c ----
|
||||
Just (L loc t) -> return $ L loc (K $ clean $ render (ppTerm Unqualified 0 (oneBranch t)))
|
||||
Nothing -> return $ L (0,0) (K $ showIdent c) ----
|
||||
where
|
||||
comp = computeConcrete gr
|
||||
|
||||
|
||||
@@ -116,18 +116,18 @@ refreshModule (k,ms) mi@(i,mo)
|
||||
| otherwise = return (k, mi:ms)
|
||||
where
|
||||
refreshRes (k,cs) ci@(c,info) = case info of
|
||||
ResOper ptyp (Just trm) -> do ---- refresh ptyp
|
||||
ResOper ptyp (Just (L loc trm)) -> do ---- refresh ptyp
|
||||
(k',trm') <- refreshTermKN k trm
|
||||
return $ (k', (c, ResOper ptyp (Just trm')):cs)
|
||||
return $ (k', (c, ResOper ptyp (Just (L loc trm'))):cs)
|
||||
ResOverload os tyts -> do
|
||||
(k',tyts') <- liftM (\ (t,(_,i)) -> (i,t)) $
|
||||
appSTM (mapPairsM refresh tyts) (initIdStateN k)
|
||||
appSTM (mapPairsM (\(L loc t) -> liftM (L loc) (refresh t)) tyts) (initIdStateN k)
|
||||
return $ (k', (c, ResOverload os tyts'):cs)
|
||||
CncCat mt (Just trm) pn -> do ---- refresh mt, pn
|
||||
CncCat mt (Just (L loc trm)) pn -> do ---- refresh mt, pn
|
||||
(k',trm') <- refreshTermKN k trm
|
||||
return $ (k', (c, CncCat mt (Just trm') pn):cs)
|
||||
CncFun mt (Just trm) pn -> do ---- refresh pn
|
||||
return $ (k', (c, CncCat mt (Just (L loc trm')) pn):cs)
|
||||
CncFun mt (Just (L loc trm)) pn -> do ---- refresh pn
|
||||
(k',trm') <- refreshTermKN k trm
|
||||
return $ (k', (c, CncFun mt (Just trm') pn):cs)
|
||||
return $ (k', (c, CncFun mt (Just (L loc trm')) pn):cs)
|
||||
_ -> return (k, ci:cs)
|
||||
|
||||
|
||||
@@ -54,7 +54,7 @@ renameModule :: [SourceModule] -> SourceModule -> Check SourceModule
|
||||
renameModule ms (name,mo) = checkIn (text "renaming module" <+> ppIdent name) $ do
|
||||
let js1 = jments mo
|
||||
status <- buildStatus (MGrammar ms) name mo
|
||||
js2 <- checkMap (renameInfo mo status) js1
|
||||
js2 <- checkMap (renameInfo status name) js1
|
||||
return (name, mo {opens = map forceQualif (opens mo), jments = js2})
|
||||
|
||||
type Status = (StatusTree, [(OpenSpec, StatusTree)])
|
||||
@@ -137,31 +137,49 @@ forceQualif o = case o of
|
||||
OSimple i -> OQualif i i
|
||||
OQualif _ i -> OQualif i i
|
||||
|
||||
renameInfo :: SourceModInfo -> Status -> Ident -> Info -> Check Info
|
||||
renameInfo mo status i info = checkIn
|
||||
(text "renaming definition of" <+> ppIdent i <+> ppPosition mo i) $
|
||||
case info of
|
||||
AbsCat pco -> liftM AbsCat (renPerh (renameContext status) pco)
|
||||
AbsFun pty pa ptr -> liftM3 AbsFun (ren pty) (return pa) (renPerh (mapM (renameEquation status [])) ptr)
|
||||
ResOper pty ptr -> liftM2 ResOper (ren pty) (ren ptr)
|
||||
ResOverload os tysts ->
|
||||
liftM (ResOverload os) (mapM (pairM rent) tysts)
|
||||
renameInfo :: Status -> Ident -> Ident -> Info -> Check Info
|
||||
renameInfo status m i info =
|
||||
case info of
|
||||
AbsCat pco -> liftM AbsCat (renPerh (renameContext status) pco)
|
||||
AbsFun pty pa ptr -> liftM3 AbsFun (renTerm pty) (return pa) (renMaybe (mapM (renLoc (renEquation status))) ptr)
|
||||
ResOper pty ptr -> liftM2 ResOper (renTerm pty) (renTerm ptr)
|
||||
ResOverload os tysts -> liftM (ResOverload os) (mapM (renPair (renameTerm status [])) tysts)
|
||||
ResParam (Just pp) m -> do
|
||||
pp' <- mapM (renLoc (renParam status)) pp
|
||||
return (ResParam (Just pp') m)
|
||||
ResValue t -> do
|
||||
t <- renLoc (renameTerm status []) t
|
||||
return (ResValue t)
|
||||
CncCat pty ptr ppr -> liftM3 CncCat (renTerm pty) (renTerm ptr) (renTerm ppr)
|
||||
CncFun mt ptr ppr -> liftM2 (CncFun mt) (renTerm ptr) (renTerm ppr)
|
||||
_ -> return info
|
||||
where
|
||||
renTerm = renPerh (renameTerm status [])
|
||||
|
||||
ResParam (Just pp) m -> do
|
||||
pp' <- mapM (renameParam status) pp
|
||||
return (ResParam (Just pp') m)
|
||||
ResValue t -> do
|
||||
t <- rent t
|
||||
return (ResValue t)
|
||||
CncCat pty ptr ppr -> liftM3 CncCat (ren pty) (ren ptr) (ren ppr)
|
||||
CncFun mt ptr ppr -> liftM2 (CncFun mt) (ren ptr) (ren ppr)
|
||||
_ -> return info
|
||||
where
|
||||
ren = renPerh rent
|
||||
rent = renameTerm status []
|
||||
renPerh ren = renMaybe (renLoc ren)
|
||||
|
||||
renPerh ren (Just t) = liftM Just $ ren t
|
||||
renPerh ren Nothing = return Nothing
|
||||
renMaybe ren (Just x) = ren x >>= return . Just
|
||||
renMaybe ren Nothing = return Nothing
|
||||
|
||||
renLoc ren (L loc x) =
|
||||
checkIn (text "renaming of" <+> ppIdent i <+> ppPosition m loc) $ do
|
||||
x <- ren x
|
||||
return (L loc x)
|
||||
|
||||
renPair ren (L locx x, L locy y) = do x <- ren x
|
||||
y <- ren y
|
||||
return (L locx x, L locy y)
|
||||
|
||||
renEquation :: Status -> Equation -> Check Equation
|
||||
renEquation b (ps,t) = do
|
||||
(ps',vs) <- liftM unzip $ mapM (renamePattern b) ps
|
||||
t' <- renameTerm b (concat vs) t
|
||||
return (ps',t')
|
||||
|
||||
renParam :: Status -> Param -> Check Param
|
||||
renParam env (c,co) = do
|
||||
co' <- renameContext env co
|
||||
return (c,co')
|
||||
|
||||
renameTerm :: Status -> [Ident] -> Term -> Check Term
|
||||
renameTerm env vars = ren vars where
|
||||
@@ -283,11 +301,6 @@ renamePattern env patt = case patt of
|
||||
renp = renamePattern env
|
||||
renid = renameIdentTerm env
|
||||
|
||||
renameParam :: Status -> (Ident, Context) -> Check (Ident, Context)
|
||||
renameParam env (c,co) = do
|
||||
co' <- renameContext env co
|
||||
return (c,co')
|
||||
|
||||
renameContext :: Status -> Context -> Check Context
|
||||
renameContext b = renc [] where
|
||||
renc vs cont = case cont of
|
||||
@@ -303,10 +316,3 @@ renameContext b = renc [] where
|
||||
return $ (bt,x,t') : xts'
|
||||
_ -> return cont
|
||||
ren = renameTerm b
|
||||
|
||||
-- | vars not needed in env, since patterns always overshadow old vars
|
||||
renameEquation :: Status -> [Ident] -> Equation -> Check Equation
|
||||
renameEquation b vs (ps,t) = do
|
||||
(ps',vs') <- liftM unzip $ mapM (renamePattern b) ps
|
||||
t' <- renameTerm b (concat vs' ++ vs) t
|
||||
return (ps',t')
|
||||
|
||||
@@ -53,9 +53,9 @@ unsubexpModule sm@(i,mo)
|
||||
-- perform this iff the module has opers
|
||||
hasSub ljs = not $ null [c | (c,ResOper _ _) <- ljs]
|
||||
unparInfo (c,info) = case info of
|
||||
CncFun xs (Just t) m -> [(c, CncFun xs (Just (unparTerm t)) m)]
|
||||
ResOper (Just (EInt 8)) _ -> [] -- subexp-generated opers
|
||||
ResOper pty (Just t) -> [(c, ResOper pty (Just (unparTerm t)))]
|
||||
CncFun xs (Just (L loc t)) m -> [(c, CncFun xs (Just (L loc (unparTerm t))) m)]
|
||||
ResOper (Just (L loc (EInt 8))) _ -> [] -- subexp-generated opers
|
||||
ResOper pty (Just (L loc t)) -> [(c, ResOper pty (Just (L loc (unparTerm t))))]
|
||||
_ -> [(c,info)]
|
||||
unparTerm t = case t of
|
||||
Q m c | isOperIdent c -> --- name convention of subexp opers
|
||||
@@ -76,12 +76,12 @@ addSubexpConsts mo tree lins = do
|
||||
mapM mkOne $ opers ++ lins
|
||||
where
|
||||
mkOne (f,def) = case def of
|
||||
CncFun xs (Just trm) pn -> do
|
||||
CncFun xs (Just (L loc trm)) pn -> do
|
||||
trm' <- recomp f trm
|
||||
return (f,CncFun xs (Just trm') pn)
|
||||
ResOper ty (Just trm) -> do
|
||||
return (f,CncFun xs (Just (L loc trm')) pn)
|
||||
ResOper ty (Just (L loc trm)) -> do
|
||||
trm' <- recomp f trm
|
||||
return (f,ResOper ty (Just trm'))
|
||||
return (f,ResOper ty (Just (L loc trm')))
|
||||
_ -> return (f,def)
|
||||
recomp f t = case Map.lookup t tree of
|
||||
Just (_,id) | operIdent id /= f -> return $ Q mo (operIdent id)
|
||||
@@ -89,7 +89,7 @@ addSubexpConsts mo tree lins = do
|
||||
|
||||
list = Map.toList tree
|
||||
|
||||
oper id trm = (operIdent id, ResOper (Just (EInt 8)) (Just trm))
|
||||
oper id trm = (operIdent id, ResOper (Just (L (0,0) (EInt 8))) (Just (L (0,0) trm)))
|
||||
--- impossible type encoding generated opers
|
||||
|
||||
getSubtermsMod :: Ident -> [(Ident,Info)] -> TermM (Map Term (Int,Int))
|
||||
@@ -99,10 +99,10 @@ getSubtermsMod mo js = do
|
||||
return $ Map.filter (\ (nu,_) -> nu > 1) tree0
|
||||
where
|
||||
getInfo get fi@(f,i) = case i of
|
||||
CncFun xs (Just trm) pn -> do
|
||||
CncFun xs (Just (L _ trm)) pn -> do
|
||||
get trm
|
||||
return $ fi
|
||||
ResOper ty (Just trm) -> do
|
||||
ResOper ty (Just (L _ trm)) -> do
|
||||
get trm
|
||||
return $ fi
|
||||
_ -> return fi
|
||||
|
||||
@@ -77,7 +77,7 @@ extendModule gr (name,m)
|
||||
-- | rebuilding instance + interface, and "with" modules, prior to renaming.
|
||||
-- AR 24/10/2003
|
||||
rebuildModule :: SourceGrammar -> SourceModule -> Err SourceModule
|
||||
rebuildModule gr mo@(i,mi@(ModInfo mt stat fs_ me mw ops_ med_ js_ ps_)) = do
|
||||
rebuildModule gr mo@(i,mi@(ModInfo mt stat fs_ me mw ops_ med_ js_)) = do
|
||||
---- deps <- moduleDeps ms
|
||||
---- is <- openInterfaces deps i
|
||||
let is = [] ---- the method above is buggy: try "i -src" for two grs. AR 8/3/2005
|
||||
@@ -100,8 +100,7 @@ rebuildModule gr mo@(i,mi@(ModInfo mt stat fs_ me mw ops_ med_ js_ ps_)) = do
|
||||
m0s <- mapM (lookupModule gr) j0s
|
||||
let notInM0 c _ = all (not . isInBinTree c . jments) m0s
|
||||
let js2 = filterBinTree notInM0 js'
|
||||
return $ (replaceJudgements mi js2)
|
||||
{positions = Map.union (positions m1) (positions mi)}
|
||||
return $ replaceJudgements mi js2
|
||||
_ -> return mi
|
||||
|
||||
-- add the instance opens to an incomplete module "with" instances
|
||||
@@ -111,7 +110,7 @@ rebuildModule gr mo@(i,mi@(ModInfo mt stat fs_ me mw ops_ med_ js_ ps_)) = do
|
||||
[i | i <- is, notElem i infs]
|
||||
testErr (stat' == MSComplete || stat == MSIncomplete)
|
||||
("module" +++ showIdent i +++ "remains incomplete")
|
||||
ModInfo mt0 _ fs me' _ ops0 _ js ps0 <- lookupModule gr ext
|
||||
ModInfo mt0 _ fs me' _ ops0 _ js <- lookupModule gr ext
|
||||
let ops1 = nub $
|
||||
ops_ ++ -- N.B. js has been name-resolved already
|
||||
[OQualif i j | (i,j) <- ops] ++
|
||||
@@ -123,9 +122,8 @@ rebuildModule gr mo@(i,mi@(ModInfo mt stat fs_ me mw ops_ med_ js_ ps_)) = do
|
||||
let fs1 = fs `addOptions` fs_ -- new flags have priority
|
||||
let js0 = [ci | ci@(c,_) <- tree2list js, isInherited incl c]
|
||||
let js1 = buildTree (tree2list js_ ++ js0)
|
||||
let ps1 = Map.union ps_ ps0
|
||||
let med1= nub (ext : infs ++ insts ++ med_)
|
||||
return $ ModInfo mt0 stat' fs1 me Nothing ops1 med1 js1 ps1
|
||||
return $ ModInfo mt0 stat' fs1 me Nothing ops1 med1 js1
|
||||
|
||||
return (i,mi')
|
||||
|
||||
@@ -170,9 +168,9 @@ extendMod gr isCompl (name,cond) base old new = foldM try new $ Map.toList old
|
||||
unifyAnyInfo :: Ident -> Info -> Info -> Err Info
|
||||
unifyAnyInfo m i j = case (i,j) of
|
||||
(AbsCat mc1, AbsCat mc2) ->
|
||||
liftM AbsCat (unifMaybe mc1 mc2)
|
||||
liftM AbsCat (unifMaybeL mc1 mc2)
|
||||
(AbsFun mt1 ma1 md1, AbsFun mt2 ma2 md2) ->
|
||||
liftM3 AbsFun (unifMaybe mt1 mt2) (unifAbsArrity ma1 ma2) (unifAbsDefs md1 md2) -- adding defs
|
||||
liftM3 AbsFun (unifMaybeL mt1 mt2) (unifAbsArrity ma1 ma2) (unifAbsDefs md1 md2) -- adding defs
|
||||
|
||||
(ResParam mt1 mv1, ResParam mt2 mv2) ->
|
||||
liftM2 ResParam (unifMaybe mt1 mt2) (unifMaybe mv1 mv2)
|
||||
@@ -182,12 +180,12 @@ unifyAnyInfo m i j = case (i,j) of
|
||||
(_, ResOverload ms t) | elem m ms ->
|
||||
return $ ResOverload ms t
|
||||
(ResOper mt1 m1, ResOper mt2 m2) ->
|
||||
liftM2 ResOper (unifMaybe mt1 mt2) (unifMaybe m1 m2)
|
||||
liftM2 ResOper (unifMaybeL mt1 mt2) (unifMaybeL m1 m2)
|
||||
|
||||
(CncCat mc1 mf1 mp1, CncCat mc2 mf2 mp2) ->
|
||||
liftM3 CncCat (unifMaybe mc1 mc2) (unifMaybe mf1 mf2) (unifMaybe mp1 mp2)
|
||||
liftM3 CncCat (unifMaybeL mc1 mc2) (unifMaybeL mf1 mf2) (unifMaybeL mp1 mp2)
|
||||
(CncFun m mt1 md1, CncFun _ mt2 md2) ->
|
||||
liftM2 (CncFun m) (unifMaybe mt1 mt2) (unifMaybe md1 md2) ---- adding defs
|
||||
liftM2 (CncFun m) (unifMaybeL mt1 mt2) (unifMaybeL md1 md2) ---- adding defs
|
||||
|
||||
(AnyInd b1 m1, AnyInd b2 m2) -> do
|
||||
testErr (b1 == b2) $ "indirection status"
|
||||
@@ -205,6 +203,15 @@ unifMaybe (Just p1) (Just p2)
|
||||
| p1==p2 = return (Just p1)
|
||||
| otherwise = fail ""
|
||||
|
||||
-- | this is what happens when matching two values in the same module
|
||||
unifMaybeL :: Eq a => Maybe (L a) -> Maybe (L a) -> Err (Maybe (L a))
|
||||
unifMaybeL Nothing Nothing = return Nothing
|
||||
unifMaybeL (Just p1) Nothing = return (Just p1)
|
||||
unifMaybeL Nothing (Just p2) = return (Just p2)
|
||||
unifMaybeL (Just (L l1 p1)) (Just (L l2 p2))
|
||||
| p1==p2 = return (Just (L l1 p1))
|
||||
| otherwise = fail ""
|
||||
|
||||
unifAbsArrity :: Maybe Int -> Maybe Int -> Err (Maybe Int)
|
||||
unifAbsArrity Nothing Nothing = return Nothing
|
||||
unifAbsArrity (Just a ) Nothing = return (Just a )
|
||||
@@ -213,14 +220,8 @@ unifAbsArrity (Just a1) (Just a2)
|
||||
| a1==a2 = return (Just a1)
|
||||
| otherwise = fail ""
|
||||
|
||||
unifAbsDefs :: Maybe [Equation] -> Maybe [Equation] -> Err (Maybe [Equation])
|
||||
unifAbsDefs :: Maybe [L Equation] -> Maybe [L Equation] -> Err (Maybe [L Equation])
|
||||
unifAbsDefs Nothing Nothing = return Nothing
|
||||
unifAbsDefs (Just _ ) Nothing = fail ""
|
||||
unifAbsDefs Nothing (Just _ ) = fail ""
|
||||
unifAbsDefs (Just xs) (Just ys) = return (Just (xs ++ ys))
|
||||
|
||||
unifConstrs :: Maybe [Term] -> Maybe [Term] -> Err (Maybe [Term])
|
||||
unifConstrs p1 p2 = case (p1,p2) of
|
||||
(Nothing, _) -> return p2
|
||||
(_, Nothing) -> return p1
|
||||
(Just bs, Just ds) -> return $ Just $ bs ++ ds
|
||||
|
||||
Reference in New Issue
Block a user