forked from GitHub/gf-core
oper overloading: first implemenatation using records
This commit is contained in:
@@ -171,7 +171,6 @@ checkResInfo :: SourceGrammar -> Ident -> (Ident,Info) -> Check (Ident,Info)
|
|||||||
checkResInfo gr mo (c,info) = do
|
checkResInfo gr mo (c,info) = do
|
||||||
checkReservedId c
|
checkReservedId c
|
||||||
case info of
|
case info of
|
||||||
|
|
||||||
ResOper pty pde -> chIn "operation" $ do
|
ResOper pty pde -> chIn "operation" $ do
|
||||||
(pty', pde') <- case (pty,pde) of
|
(pty', pde') <- case (pty,pde) of
|
||||||
(Yes ty, Yes de) -> do
|
(Yes ty, Yes de) -> do
|
||||||
@@ -187,6 +186,11 @@ checkResInfo gr mo (c,info) = do
|
|||||||
_ -> return (pty, pde) --- other cases are uninteresting
|
_ -> return (pty, pde) --- other cases are uninteresting
|
||||||
return (c, ResOper pty' pde')
|
return (c, ResOper pty' pde')
|
||||||
|
|
||||||
|
ResOverload tysts -> chIn "overloading" $ do
|
||||||
|
tysts' <- mapM (uncurry $ flip check) tysts
|
||||||
|
---- TODO: check uniqueness of arg type lists
|
||||||
|
return (c,ResOverload [(y,x) | (x,y) <- tysts'])
|
||||||
|
|
||||||
ResParam (Yes (pcs,_)) -> chIn "parameter type" $ do
|
ResParam (Yes (pcs,_)) -> chIn "parameter type" $ do
|
||||||
---- mapM ((mapM (computeLType gr . snd)) . snd) pcs
|
---- mapM ((mapM (computeLType gr . snd)) . snd) pcs
|
||||||
mapM_ ((mapM_ (checkIfParType gr . snd)) . snd) pcs
|
mapM_ ((mapM_ (checkIfParType gr . snd)) . snd) pcs
|
||||||
@@ -200,6 +204,8 @@ checkResInfo gr mo (c,info) = do
|
|||||||
chIn cat = checkIn ("Happened in" +++ cat +++ prt c +++ ":")
|
chIn cat = checkIn ("Happened in" +++ cat +++ prt c +++ ":")
|
||||||
comp = computeLType gr
|
comp = computeLType gr
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
checkCncInfo :: SourceGrammar -> Ident -> (Ident,SourceAbs) ->
|
checkCncInfo :: SourceGrammar -> Ident -> (Ident,SourceAbs) ->
|
||||||
(Ident,Info) -> Check (Ident,Info)
|
(Ident,Info) -> Check (Ident,Info)
|
||||||
checkCncInfo gr m (a,abs) (c,info) = do
|
checkCncInfo gr m (a,abs) (c,info) = do
|
||||||
@@ -378,16 +384,20 @@ inferLType gr trm = case trm of
|
|||||||
return (e,t')
|
return (e,t')
|
||||||
|
|
||||||
App f a -> do
|
App f a -> do
|
||||||
(f',fty) <- infer f
|
over <- getOverload trm
|
||||||
fty' <- comp fty
|
case over of
|
||||||
case fty' of
|
Just trty -> return trty
|
||||||
Prod z arg val -> do
|
_ -> do
|
||||||
a' <- justCheck a arg
|
(f',fty) <- infer f
|
||||||
ty <- if isWildIdent z
|
fty' <- comp fty
|
||||||
then return val
|
case fty' of
|
||||||
else substituteLType [(z,a')] val
|
Prod z arg val -> do
|
||||||
return (App f' a',ty)
|
a' <- justCheck a arg
|
||||||
_ -> prtFail ("function type expected for"+++ prt f +++"instead of") fty
|
ty <- if isWildIdent z
|
||||||
|
then return val
|
||||||
|
else substituteLType [(z,a')] val
|
||||||
|
return (App f' a',ty)
|
||||||
|
_ -> prtFail ("function type expected for"+++ prt f +++"instead of") fty
|
||||||
|
|
||||||
S f x -> do
|
S f x -> do
|
||||||
(f', fty) <- infer f
|
(f', fty) <- infer f
|
||||||
@@ -550,6 +560,27 @@ inferLType gr trm = case trm of
|
|||||||
PRep _ -> return $ typeTok
|
PRep _ -> return $ typeTok
|
||||||
_ -> infer (patt2term p) >>= return . snd
|
_ -> infer (patt2term p) >>= return . snd
|
||||||
|
|
||||||
|
getOverload t = case appForm t of
|
||||||
|
(f@(Q m c), ts) -> case lookupOverload gr m c of
|
||||||
|
Ok typs -> do
|
||||||
|
ttys <- mapM infer ts
|
||||||
|
v <- matchOverload f typs ttys
|
||||||
|
return $ Just v
|
||||||
|
_ -> return Nothing
|
||||||
|
_ -> return Nothing
|
||||||
|
|
||||||
|
matchOverload f typs ttys = do
|
||||||
|
let (tts,tys) = unzip ttys
|
||||||
|
case lookupOverloadInstance tys typs of
|
||||||
|
Just (val,fun) -> return (mkApp fun tts, val)
|
||||||
|
_ -> fail $ "no overload instance of" +++ prt f +++
|
||||||
|
"for" +++ unwords (map prt_ tys) +++ "among" ++++
|
||||||
|
unlines [unwords (map prt_ ty) | (ty,_) <- typs]
|
||||||
|
++++ "DEBUG" +++ unwords (map show tys) +++ ";" ++++
|
||||||
|
unlines (map (show . fst) typs) ----
|
||||||
|
|
||||||
|
lookupOverloadInstance tys typs = lookup tys typs ---- use Map
|
||||||
|
|
||||||
checkLType :: SourceGrammar -> Term -> Type -> Check (Term, Type)
|
checkLType :: SourceGrammar -> Term -> Type -> Check (Term, Type)
|
||||||
checkLType env trm typ0 = do
|
checkLType env trm typ0 = do
|
||||||
|
|
||||||
|
|||||||
@@ -159,6 +159,8 @@ renameInfo status (i,info) = errIn ("renaming definition of" +++ prt i) $
|
|||||||
AbsTrans f -> liftM AbsTrans (rent f)
|
AbsTrans f -> liftM AbsTrans (rent f)
|
||||||
|
|
||||||
ResOper pty ptr -> liftM2 ResOper (ren pty) (ren ptr)
|
ResOper pty ptr -> liftM2 ResOper (ren pty) (ren ptr)
|
||||||
|
ResOverload tysts -> liftM ResOverload $ mapM (pairM rent) tysts
|
||||||
|
|
||||||
ResParam (Yes (pp,m)) -> do
|
ResParam (Yes (pp,m)) -> do
|
||||||
pp' <- mapM (renameParam status) pp
|
pp' <- mapM (renameParam status) pp
|
||||||
return $ ResParam $ Yes (pp',m)
|
return $ ResParam $ Yes (pp',m)
|
||||||
|
|||||||
@@ -92,6 +92,8 @@ data Info =
|
|||||||
| ResValue (Perh (Type,Maybe Int)) -- ^ (/RES/) to mark parameter constructors for lookup
|
| ResValue (Perh (Type,Maybe Int)) -- ^ (/RES/) to mark parameter constructors for lookup
|
||||||
| ResOper (Perh Type) (Perh Term) -- ^ (/RES/)
|
| ResOper (Perh Type) (Perh Term) -- ^ (/RES/)
|
||||||
|
|
||||||
|
| ResOverload [(Type,Term)] -- ^ (/RES/)
|
||||||
|
|
||||||
-- judgements in concrete syntax
|
-- judgements in concrete syntax
|
||||||
| CncCat (Perh Type) (Perh Term) MPr -- ^ (/CNC/) lindef ini'zed,
|
| CncCat (Perh Type) (Perh Term) MPr -- ^ (/CNC/) lindef ini'zed,
|
||||||
| CncFun (Maybe (Ident,(Context,Type))) (Perh Term) MPr -- (/CNC/) type info added at 'TC'
|
| CncFun (Maybe (Ident,(Context,Type))) (Perh Term) MPr -- (/CNC/) type info added at 'TC'
|
||||||
|
|||||||
@@ -18,6 +18,7 @@ module GF.Grammar.Lookup (
|
|||||||
lookupResDef,
|
lookupResDef,
|
||||||
lookupResDefKind,
|
lookupResDefKind,
|
||||||
lookupResType,
|
lookupResType,
|
||||||
|
lookupOverload,
|
||||||
lookupParams,
|
lookupParams,
|
||||||
lookupParamValues,
|
lookupParamValues,
|
||||||
lookupFirstTag,
|
lookupFirstTag,
|
||||||
@@ -105,6 +106,20 @@ lookupResType gr m c = do
|
|||||||
AnyInd _ n -> lookFun e m c n
|
AnyInd _ n -> lookFun e m c n
|
||||||
_ -> prtBad "cannot find type of reused function" c
|
_ -> prtBad "cannot find type of reused function" c
|
||||||
|
|
||||||
|
lookupOverload :: SourceGrammar -> Ident -> Ident -> Err [([Type],(Type,Term))]
|
||||||
|
lookupOverload gr m c = do
|
||||||
|
mi <- lookupModule gr m
|
||||||
|
case mi of
|
||||||
|
ModMod mo -> do
|
||||||
|
info <- lookupIdentInfo mo c
|
||||||
|
case info of
|
||||||
|
ResOverload tysts ->
|
||||||
|
return [(map snd args,(val,tr)) |
|
||||||
|
(ty,tr) <- tysts, Ok (args,val) <- [typeFormCnc ty]]
|
||||||
|
|
||||||
|
AnyInd _ n -> lookupOverload gr n c
|
||||||
|
_ -> Bad $ prt c +++ "is not an overloaded operation"
|
||||||
|
_ -> Bad $ prt m +++ "is not a resource"
|
||||||
|
|
||||||
lookupParams :: SourceGrammar -> Ident -> Ident -> Err ([Param],Maybe PValues)
|
lookupParams :: SourceGrammar -> Ident -> Ident -> Err ([Param],Maybe PValues)
|
||||||
lookupParams gr = look True where
|
lookupParams gr = look True where
|
||||||
|
|||||||
@@ -94,6 +94,10 @@ trAnyDef (i,info) = let i' = tri i in case info of
|
|||||||
May b -> P.ParDefIndir i' $ tri b
|
May b -> P.ParDefIndir i' $ tri b
|
||||||
_ -> P.ParDefAbs i']]
|
_ -> P.ParDefAbs i']]
|
||||||
|
|
||||||
|
ResOverload tysts ->
|
||||||
|
[P.DefOper [P.DDef [mkName i'] (
|
||||||
|
P.ERecord [P.LDFull [i'] (trt ty) (trt fu) | (ty,fu) <- tysts])]]
|
||||||
|
|
||||||
CncCat (Yes ty) Nope _ ->
|
CncCat (Yes ty) Nope _ ->
|
||||||
[P.DefLincat [P.PrintDef [mkName i'] (trt ty)]]
|
[P.DefLincat [P.PrintDef [mkName i'] (trt ty)]]
|
||||||
CncCat pty ptr ppr ->
|
CncCat pty ptr ppr ->
|
||||||
|
|||||||
@@ -299,7 +299,7 @@ transResDef x = case x of
|
|||||||
(p,pars) <- pardefs', (f,co) <- pars]
|
(p,pars) <- pardefs', (f,co) <- pars]
|
||||||
DefOper defs -> do
|
DefOper defs -> do
|
||||||
defs' <- liftM concat $ mapM getDefs defs
|
defs' <- liftM concat $ mapM getDefs defs
|
||||||
returnl [(f, G.ResOper pt pe) | (f,(pt,pe)) <- defs']
|
returnl [mkOverload (f, G.ResOper pt pe) | (f,(pt,pe)) <- defs']
|
||||||
|
|
||||||
DefLintype defs -> do
|
DefLintype defs -> do
|
||||||
defs' <- liftM concat $ mapM getDefs defs
|
defs' <- liftM concat $ mapM getDefs defs
|
||||||
@@ -307,6 +307,12 @@ transResDef x = case x of
|
|||||||
|
|
||||||
DefFlag defs -> liftM Right $ mapM transFlagDef defs
|
DefFlag defs -> liftM Right $ mapM transFlagDef defs
|
||||||
_ -> Bad $ "illegal definition form in resource" +++ printTree x
|
_ -> Bad $ "illegal definition form in resource" +++ printTree x
|
||||||
|
where
|
||||||
|
mkOverload (c,j) = case j of
|
||||||
|
G.ResOper Nope (Yes (G.R fs@(_:_:_))) | isOverloading c fs ->
|
||||||
|
(c,G.ResOverload [(ty,fu) | (_,(Just ty,fu)) <- fs])
|
||||||
|
_ -> (c,j)
|
||||||
|
isOverloading c fs = all (== GP.prt c) (map (GP.prt . fst) fs)
|
||||||
|
|
||||||
transParDef :: ParDef -> Err (Ident, [G.Param])
|
transParDef :: ParDef -> Err (Ident, [G.Param])
|
||||||
transParDef x = case x of
|
transParDef x = case x of
|
||||||
|
|||||||
Reference in New Issue
Block a user