msyds/gf-core
1
0
Fork 0
forked from GitHub/gf-core
Code Pull Requests Activity

overload rules and their documentation

Browse Source
This commit is contained in:
aarne
2006-12-21 09:25:02 +00:00
parent 15fd1d590a
commit fd90fe0791
5 changed files with 76 additions and 29 deletions
Download Patch File Download Diff File Expand all files Collapse all files

27
doc/gf-history.html
View File

@@ -14,6 +14,33 @@ Changes in functionality since May 17, 2005, release of GF Version 2.2
<p>
21/12 (AR) Overloading rules for GF version 2.7:
<ol>
<li> If a unique instance is found by exact match with argument types,
that instance is used.
<li> Otherwise, if exact match with the expected value type gives a
uniques instance, that instance is used.
<li> Otherwise, if among possible instances only one returns a non-function
type, that instance is used, but a warning is issued.
<li> Otherwise, an error results, and the list of possible instances is shown.
</ol>
These rules are still temporary, but all future developments will guarantee
that their type-correct use will work. Rule (3) is only needed because the
current type checker does not always know an expected type. It can give
an incorrect result which is captured later in the compilation. To be noticed,
in particular, is that exact match is required. Match by subtyping will be
investigated later.
<p>
20/11 (AR) Type error messages in concrete syntax are printed with a
heuristic where a type of the form <tt>{... ; lock_C : {} ; ...}</tt>
is printed as <tt>C</tt>. This gives more readable error messages, but
can produce wrong results if lock fields are hand-written or if subtypes
of lock-fielded categories are used.
<p>
17/11 (AR) Operation overloading: an <tt>oper</tt> can have many types,
from which one is picked at compile time. The types must have different
argument lists. Exact match with the arguments given to the <tt>oper</tt>

8
examples/logic/ArithmEng.gf
View File

@@ -24,8 +24,8 @@ lin
one = UsePN (regPN "one") ;
two = UsePN (regPN "two") ;
sum = appColl (regN2 "sum") ;
prod = appColl (regN2 "product") ;
sum = app (regN2 "sum") ;
prod = app (regN2 "product") ;
evax1 =
proof (by (ref (mkLabel ["the first axiom of evenness ,"])))
@@ -42,14 +42,14 @@ lin
eqax1 =
proof (by (ref (mkLabel ["the first axiom of equality ,"])))
(mkS (predA2 (mkA2 (regA "equal") (mkPrep "to"))
(mkS (pred (mkA2 (regA "equal") (mkPrep "to"))
(UsePN (regPN "zero"))
(UsePN (regPN "zero")))) ;
eqax2 m n c =
appendText c
(proof (by (ref (mkLabel ["the second axiom of equality ,"])))
(mkS (predA2 (mkA2 (regA "equal") (mkPrep "to"))
(mkS (pred (mkA2 (regA "equal") (mkPrep "to"))
(appN2 (regN2 "successor") m) (appN2 (regN2 "successor") n)))) ;
IndNat C d e = {s =

2
examples/logic/LogicI.gf
View File

@@ -28,7 +28,7 @@ lin
Univ A B =
AdvS
(mkAdv for_Prep (mkNP all_Predet
(mkNP (mkDet (PlQuant IndefArt) NoNum NoOrd) (mkCN A (symb B.$0)))))
(mkNP (mkDet (PlQuant IndefArt)) (mkCN A (symb B.$0)))))
B ;
DisjIl A B a = proof a (proof afortiori (coord or_Conj A B)) ;

2
examples/logic/Prooftext.gf
View File

@@ -55,7 +55,7 @@ oper
proof : Decl -> Proof
= \d -> d ;
proof : Proof -> Proof -> Proof
= \p,q -> appendText p q ;
= appendText ;
proof : Branching -> Proofs -> Proof
= \b,ps -> mkText (mkPhr b) ps
} ;

66
src/GF/Compile/CheckGrammar.hs
View File

@@ -211,7 +211,7 @@ checkResInfo gr mo (c,info) = do
checkUniq xss = case xss of
x:y:xs
| x == y -> raise $ "ambiguous for argument list" +++
unwords (map prtType x)
unwords (map (prtType gr) x)
| otherwise -> checkUniq $ y:xs
_ -> return ()
@@ -412,7 +412,7 @@ inferLType gr trm = case trm of
else substituteLType [(z,a')] val
return (App f' a',ty)
_ -> raise ("function type expected for"+++
prt f +++"instead of" +++ prtType fty)
prt f +++"instead of" +++ prtType env fty)
S f x -> do
(f', fty) <- infer f
@@ -596,14 +596,22 @@ getOverload env@gr mt t = case appForm t of
case [vf | vf@(v,f) <- vfs, elem mt [Nothing,Just v]] of
[(val,fun)] -> return (mkApp fun tts, val)
[] -> raise $ "no overload instance of" +++ prt f +++
maybe [] (("when expecting" +++) . prtType) mt +++
"for" +++ unwords (map prtType tys) +++ "among" ++++
unlines [unwords (map prtType ty) | (ty,_) <- typs]
maybe [] (("when expecting" +++) . prtType env) mt +++
"for" +++ unwords (map (prtType env) tys) +++ "among" ++++
unlines [unwords (map (prtType env) ty) | (ty,_) <- typs]
---- ++++ "DEBUG" +++ unwords (map show tys) +++ ";"
---- ++++ unlines (map (show . fst) typs) ----
_ -> raise $ "ambiguous overloading of" +++ prt f +++
"for" +++ unwords (map prtType tys) ++++ "with alternatives" ++++
unlines [prtType ty | (ty,_) <- vfs]
vfs' -> case [(v,f) | (v,f) <- vfs', noProd v] of
[(val,fun)] -> do
checkWarn $ "WARNING: overloading of" +++ prt f +++
"resolved by excluding partial applications:" ++++
unlines [prtType env ty | (ty,_) <- vfs', not (noProd ty)]
return (mkApp fun tts, val)
_ -> raise $ "ambiguous overloading of" +++ prt f +++
"for" +++ unwords (map (prtType env) tys) ++++ "with alternatives" ++++
unlines [prtType env ty | (ty,_) <- vfs']
---- TODO: accept subtypes
---- TODO: use a trie
@@ -614,6 +622,9 @@ getOverload env@gr mt t = case appForm t of
pre == tys
]
noProd ty = case ty of
Prod _ _ _ -> False
_ -> True
checkLType :: SourceGrammar -> Term -> Type -> Check (Term, Type)
checkLType env trm typ0 = do
@@ -633,7 +644,7 @@ checkLType env trm typ0 = do
check c b'
checkReset
return $ (Abs x c', Prod x a b')
_ -> raise $ "product expected instead of" +++ prtType typ
_ -> raise $ "product expected instead of" +++ prtType env typ
App f a -> do
over <- getOverload env (Just typ) trm
@@ -659,7 +670,7 @@ checkLType env trm typ0 = do
_ -> return () -- happens with variable types
cs' <- mapM (checkCase arg val) cs
return (T (TTyped arg) cs', typ)
_ -> raise $ "table type expected for table instead of" +++ prtType typ
_ -> raise $ "table type expected for table instead of" +++ prtType env typ
R r -> case typ of --- why needed? because inference may be too difficult
RecType rr -> do
@@ -715,7 +726,7 @@ checkLType env trm typ0 = do
checkEq typ t trm
return (S tab' arg', t)
_ -> raise $ "table type expected for applied table instead of" +++
prtType ty'
prtType env ty'
, do
(arg',ty) <- infer arg
ty' <- comp ty
@@ -844,21 +855,26 @@ check2 chk con a b t = do
checkEqLType :: LTEnv -> Type -> Type -> Term -> Check Type
checkEqLType env t u trm = do
(b,t',u',s) <- checkIfEqLType env t u trm
case b of
True -> return t'
False -> raise $ s +++ "type of" +++ prt trm +++
": expected:" +++ prtType env t ++++
"inferred:" +++ prtType env u
checkIfEqLType :: LTEnv -> Type -> Type -> Term -> Check (Bool,Type,Type,String)
checkIfEqLType env t u trm = do
t' <- comp t
u' <- comp u
case t' == u' || alpha [] t' u' of
True -> return t'
True -> return (True,t',u',[])
-- forgive missing lock fields by only generating a warning.
--- better: use a flag to forgive? (AR 31/1/2006)
_ -> case missingLock [] t' u' of
Ok lo -> do
checkWarn $ "WARNING: missing lock field" +++ unwords (map prt lo)
return t'
Bad s -> raise (s +++ "type of" +++ prt trm +++
": expected:" +++ prtType t' ++++
"inferred:" +++ prtType u'
---- +++++ "DEBUG:" ++++ show t' ++++ show u'
)
return (True,t',u',[])
Bad s -> return (False,t',u',s)
where
-- t is a subtype of u
@@ -920,13 +936,17 @@ checkEqLType env t u trm = do
comp = computeLType env
-- printing a type with a lock field lock_C as C
prtType :: Type -> String
prtType ty = case ty of
prtType :: LTEnv -> Type -> String
prtType env ty = case ty of
RecType fs -> case filter isLockLabel $ map fst fs of
[lock] -> (drop 5 $ prt lock) --- ++++ "Full form" +++ prt ty
_ -> prt ty
Prod x a b -> prtType a +++ "->" +++ prtType b
_ -> prt ty
_ -> prtt ty
Prod x a b -> prtType env a +++ "->" +++ prtType env b
_ -> prtt ty
where
prtt t = prt t
---- use computeLType gr to check if really equal to the cat with lock
-- | linearization types and defaults
linTypeOfType :: SourceGrammar -> Ident -> Type -> Check (Context,Type)