mirror of
https://github.com/GrammaticalFramework/gf-core.git
synced 2026-04-09 04:59:31 -06:00
new overload resolution, taking care of ad hoc overloading.
This commit is contained in:
@@ -26,6 +26,12 @@ computeLType gr g0 t = comp (reverse [(b,x, Vr x) | (b,x,_) <- g0] ++ g0) t
|
||||
ty' <- lookupResDef gr (m,ident)
|
||||
if ty' == ty then return ty else comp g ty' --- is this necessary to test?
|
||||
|
||||
AdHocOverload ts -> do
|
||||
over <- getOverload gr g (Just typeType) t
|
||||
case over of
|
||||
Just (tr,_) -> return tr
|
||||
_ -> checkError (text "unresolved overloading of constants" <+> ppTerm Qualified 0 t)
|
||||
|
||||
Vr ident -> checkLookup ident g -- never needed to compute!
|
||||
|
||||
App f a -> do
|
||||
@@ -101,6 +107,12 @@ inferLType gr g trm = case trm of
|
||||
t' <- computeLType gr g t
|
||||
checkLType gr g e t'
|
||||
|
||||
AdHocOverload ts -> do
|
||||
over <- getOverload gr g Nothing trm
|
||||
case over of
|
||||
Just trty -> return trty
|
||||
_ -> checkError (text "unresolved overloading of constants" <+> ppTerm Qualified 0 trm)
|
||||
|
||||
App f a -> do
|
||||
over <- getOverload gr g Nothing trm
|
||||
case over of
|
||||
@@ -298,7 +310,6 @@ inferLType gr g trm = case trm of
|
||||
PChars _ -> return $ typeStr
|
||||
_ -> inferLType gr g (patt2term p) >>= return . snd
|
||||
|
||||
|
||||
-- type inference: Nothing, type checking: Just t
|
||||
-- the latter permits matching with value type
|
||||
getOverload :: SourceGrammar -> Context -> Maybe Type -> Term -> Check (Maybe (Term,Type))
|
||||
@@ -309,8 +320,21 @@ getOverload gr g mt ot = case appForm ot of
|
||||
v <- matchOverload f typs ttys
|
||||
return $ Just v
|
||||
_ -> return Nothing
|
||||
(AdHocOverload cs@(f:_), ts) -> do --- the function name f is only used in error messages
|
||||
let typs = concatMap collectOverloads cs
|
||||
ttys <- mapM (inferLType gr g) ts
|
||||
v <- matchOverload f typs ttys
|
||||
return $ Just v
|
||||
_ -> return Nothing
|
||||
|
||||
where
|
||||
collectOverloads tr@(Q c) = case lookupOverload gr c of
|
||||
Ok typs -> typs
|
||||
_ -> case lookupResType gr c of
|
||||
Ok ty -> let (args,val) = typeFormCnc ty in [(map (\(b,x,t) -> t) args,(val,tr))]
|
||||
_ -> []
|
||||
collectOverloads _ = [] --- constructors QC
|
||||
|
||||
matchOverload f typs ttys = do
|
||||
let (tts,tys) = unzip ttys
|
||||
let vfs = lookupOverloadInstance tys typs
|
||||
@@ -354,11 +378,15 @@ getOverload gr g mt ot = case appForm ot of
|
||||
----- "resolved by excluding partial applications:" ++++
|
||||
----- unlines [prtType env ty | (ty,_) <- vfs', not (noProd ty)]
|
||||
|
||||
|
||||
_ -> checkError $ text "ambiguous overloading of" <+> ppTerm Unqualified 0 f <+>
|
||||
text "for" <+> hsep (map ppType tys) $$
|
||||
text "with alternatives" $$
|
||||
nest 2 (vcat [ppType ty | (_,ty,_) <- if null vfs1 then vfs2 else vfs2])
|
||||
--- now forgiving ambiguity with a warning AR 1/2/2014
|
||||
-- This gives ad hoc overloading the same behaviour as the choice of the first match in renaming did before.
|
||||
-- But it also gives a chance to ambiguous overloadings that were banned before.
|
||||
(nps1,nps2) -> do
|
||||
checkWarn $ text "ambiguous overloading of" <+> ppTerm Unqualified 0 f <+>
|
||||
---- text "with argument types" <+> hsep (map (ppTerm Qualified 0) tys) $$
|
||||
text "resolved by selecting the first of the alternatives" $$
|
||||
nest 2 (vcat [ppTerm Qualified 0 fun | (_,ty,fun) <- vfs1 ++ if null vfs1 then vfs2 else []])
|
||||
return $ head [(mkApp fun tts,val) | (val,fun) <- nps1 ++ nps2]
|
||||
|
||||
matchVal mt v = elem mt [Nothing,Just v,Just (unlocked v)]
|
||||
|
||||
@@ -406,6 +434,12 @@ checkLType gr g trm typ0 = do
|
||||
(trm',ty') <- inferLType gr g trm
|
||||
termWith trm' $ checkEqLType gr g typ ty' trm'
|
||||
|
||||
AdHocOverload ts -> do
|
||||
over <- getOverload gr g Nothing trm
|
||||
case over of
|
||||
Just trty -> return trty
|
||||
_ -> checkError (text "unresolved overloading of constants" <+> ppTerm Qualified 0 trm)
|
||||
|
||||
Q _ -> do
|
||||
over <- getOverload gr g (Just typ) trm
|
||||
case over of
|
||||
@@ -499,7 +533,8 @@ checkLType gr g trm typ0 = do
|
||||
]
|
||||
Let (x,(mty,def)) body -> case mty of
|
||||
Just ty -> do
|
||||
(def',ty') <- checkLType gr g def ty
|
||||
(ty0,_) <- checkLType gr g ty typeType
|
||||
(def',ty') <- checkLType gr g def ty0
|
||||
body' <- justCheck ((Explicit,x,ty'):g) body typ
|
||||
return (Let (x,(Just ty',def')) body', typ)
|
||||
_ -> do
|
||||
@@ -596,8 +631,8 @@ checkEqLType gr g t u trm = do
|
||||
case b of
|
||||
True -> return t'
|
||||
False -> checkError $ text s <+> text "type of" <+> ppTerm Unqualified 0 trm $$
|
||||
text "expected:" <+> ppType t $$
|
||||
text "inferred:" <+> ppType u
|
||||
text "expected:" <+> ppTerm Qualified 0 t $$ -- ppqType t u $$
|
||||
text "inferred:" <+> ppTerm Qualified 0 u -- ppqType u t
|
||||
|
||||
checkIfEqLType :: SourceGrammar -> Context -> Type -> Type -> Term -> Check (Bool,Type,Type,String)
|
||||
checkIfEqLType gr g t u trm = do
|
||||
@@ -705,6 +740,11 @@ ppType ty =
|
||||
Prod _ x a b -> ppType a <+> text "->" <+> ppType b
|
||||
_ -> ppTerm Unqualified 0 ty
|
||||
|
||||
ppqType :: Type -> Type -> Doc
|
||||
ppqType t u = case (ppType t, ppType u) of
|
||||
(pt,pu) | render pt == render pu -> ppTerm Qualified 0 t
|
||||
(pt,_) -> pt
|
||||
|
||||
checkLookup :: Ident -> Context -> Check Type
|
||||
checkLookup x g =
|
||||
case [ty | (b,y,ty) <- g, x == y] of
|
||||
|
||||
@@ -209,6 +209,7 @@ ppTerm q d (ExtR x y) = prec d 3 (ppTerm q 3 x <+> text "**" <+> ppTerm q 4 y)
|
||||
ppTerm q d (App x y) = prec d 4 (ppTerm q 4 x <+> ppTerm q 5 y)
|
||||
ppTerm q d (V e es) = hang (text "table") 2 (sep [ppTerm q 6 e,brackets (fsep (punctuate semi (map (ppTerm q 0) es)))])
|
||||
ppTerm q d (FV es) = text "variants" <+> braces (fsep (punctuate semi (map (ppTerm q 0) es)))
|
||||
ppTerm q d (AdHocOverload es) = text "overload" <+> braces (fsep (punctuate semi (map (ppTerm q 0) es)))
|
||||
ppTerm q d (Alts e xs) = prec d 4 (text "pre" <+> braces (ppTerm q 0 e <> semi <+> fsep (punctuate semi (map (ppAltern q) xs))))
|
||||
ppTerm q d (Strs es) = text "strs" <+> braces (fsep (punctuate semi (map (ppTerm q 0) es)))
|
||||
ppTerm q d (EPatt p) = prec d 4 (char '#' <+> ppPatt q 2 p)
|
||||
|
||||
Reference in New Issue
Block a user