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
|
||||
checkReservedId c
|
||||
case info of
|
||||
|
||||
ResOper pty pde -> chIn "operation" $ do
|
||||
(pty', pde') <- case (pty,pde) of
|
||||
(Yes ty, Yes de) -> do
|
||||
@@ -187,6 +186,11 @@ checkResInfo gr mo (c,info) = do
|
||||
_ -> return (pty, pde) --- other cases are uninteresting
|
||||
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
|
||||
---- mapM ((mapM (computeLType 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 +++ ":")
|
||||
comp = computeLType gr
|
||||
|
||||
|
||||
|
||||
checkCncInfo :: SourceGrammar -> Ident -> (Ident,SourceAbs) ->
|
||||
(Ident,Info) -> Check (Ident,Info)
|
||||
checkCncInfo gr m (a,abs) (c,info) = do
|
||||
@@ -378,16 +384,20 @@ inferLType gr trm = case trm of
|
||||
return (e,t')
|
||||
|
||||
App f a -> do
|
||||
(f',fty) <- infer f
|
||||
fty' <- comp fty
|
||||
case fty' of
|
||||
Prod z arg val -> do
|
||||
a' <- justCheck a arg
|
||||
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
|
||||
over <- getOverload trm
|
||||
case over of
|
||||
Just trty -> return trty
|
||||
_ -> do
|
||||
(f',fty) <- infer f
|
||||
fty' <- comp fty
|
||||
case fty' of
|
||||
Prod z arg val -> do
|
||||
a' <- justCheck a arg
|
||||
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
|
||||
(f', fty) <- infer f
|
||||
@@ -550,6 +560,27 @@ inferLType gr trm = case trm of
|
||||
PRep _ -> return $ typeTok
|
||||
_ -> 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 env trm typ0 = do
|
||||
|
||||
|
||||
@@ -159,6 +159,8 @@ renameInfo status (i,info) = errIn ("renaming definition of" +++ prt i) $
|
||||
AbsTrans f -> liftM AbsTrans (rent f)
|
||||
|
||||
ResOper pty ptr -> liftM2 ResOper (ren pty) (ren ptr)
|
||||
ResOverload tysts -> liftM ResOverload $ mapM (pairM rent) tysts
|
||||
|
||||
ResParam (Yes (pp,m)) -> do
|
||||
pp' <- mapM (renameParam status) pp
|
||||
return $ ResParam $ Yes (pp',m)
|
||||
|
||||
@@ -92,6 +92,8 @@ data Info =
|
||||
| ResValue (Perh (Type,Maybe Int)) -- ^ (/RES/) to mark parameter constructors for lookup
|
||||
| ResOper (Perh Type) (Perh Term) -- ^ (/RES/)
|
||||
|
||||
| ResOverload [(Type,Term)] -- ^ (/RES/)
|
||||
|
||||
-- judgements in concrete syntax
|
||||
| CncCat (Perh Type) (Perh Term) MPr -- ^ (/CNC/) lindef ini'zed,
|
||||
| CncFun (Maybe (Ident,(Context,Type))) (Perh Term) MPr -- (/CNC/) type info added at 'TC'
|
||||
|
||||
@@ -18,6 +18,7 @@ module GF.Grammar.Lookup (
|
||||
lookupResDef,
|
||||
lookupResDefKind,
|
||||
lookupResType,
|
||||
lookupOverload,
|
||||
lookupParams,
|
||||
lookupParamValues,
|
||||
lookupFirstTag,
|
||||
@@ -105,6 +106,20 @@ lookupResType gr m c = do
|
||||
AnyInd _ n -> lookFun e m c n
|
||||
_ -> 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 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
|
||||
_ -> 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 _ ->
|
||||
[P.DefLincat [P.PrintDef [mkName i'] (trt ty)]]
|
||||
CncCat pty ptr ppr ->
|
||||
|
||||
@@ -299,7 +299,7 @@ transResDef x = case x of
|
||||
(p,pars) <- pardefs', (f,co) <- pars]
|
||||
DefOper defs -> do
|
||||
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
|
||||
defs' <- liftM concat $ mapM getDefs defs
|
||||
@@ -307,6 +307,12 @@ transResDef x = case x of
|
||||
|
||||
DefFlag defs -> liftM Right $ mapM transFlagDef defs
|
||||
_ -> 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 x = case x of
|
||||
|
||||
Reference in New Issue
Block a user