mirror of
https://github.com/GrammaticalFramework/gf-core.git
synced 2026-04-23 11:42:49 -06:00
fixed PredefAbs in TC
This commit is contained in:
@@ -1,4 +1,4 @@
|
|||||||
abstract Imper = PredefAbs ** {
|
abstract Imper = {
|
||||||
|
|
||||||
cat
|
cat
|
||||||
Program ;
|
Program ;
|
||||||
|
|||||||
@@ -116,13 +116,16 @@ checkInferExp th tenv@(k,_,_) e typ = do
|
|||||||
|
|
||||||
inferExp :: Theory -> TCEnv -> Exp -> Err (AExp, Val, [(Val,Val)])
|
inferExp :: Theory -> TCEnv -> Exp -> Err (AExp, Val, [(Val,Val)])
|
||||||
inferExp th tenv@(k,rho,gamma) e = case e of
|
inferExp th tenv@(k,rho,gamma) e = case e of
|
||||||
Vr x -> mkAnnot (AVr x) $ noConstr $ lookupVar gamma x
|
Vr x -> mkAnnot (AVr x) $ noConstr $ lookupVar gamma x
|
||||||
Q m c -> mkAnnot (ACn (m,c)) $ noConstr $ lookupConst th (m,c)
|
Q m c
|
||||||
QC m c -> mkAnnot (ACn (m,c)) $ noConstr $ lookupConst th (m,c) ----
|
| m == cPredefAbs && (elem c (map identC ["Int","String"])) ->
|
||||||
EInt i -> return (AInt i, valAbsInt, [])
|
return (ACn (m,c) vType, vType, [])
|
||||||
K i -> return (AStr i, valAbsString, [])
|
| otherwise -> mkAnnot (ACn (m,c)) $ noConstr $ lookupConst th (m,c)
|
||||||
Sort _ -> return (AType, vType, [])
|
QC m c -> mkAnnot (ACn (m,c)) $ noConstr $ lookupConst th (m,c) ----
|
||||||
App f t -> do
|
EInt i -> return (AInt i, valAbsInt, [])
|
||||||
|
K i -> return (AStr i, valAbsString, [])
|
||||||
|
Sort _ -> return (AType, vType, [])
|
||||||
|
App f t -> do
|
||||||
(f',w,csf) <- inferExp th tenv f
|
(f',w,csf) <- inferExp th tenv f
|
||||||
typ <- whnf w
|
typ <- whnf w
|
||||||
case typ of
|
case typ of
|
||||||
@@ -131,7 +134,13 @@ inferExp th tenv@(k,rho,gamma) e = case e of
|
|||||||
b' <- whnf $ VClos ((x,VClos rho t):env) b
|
b' <- whnf $ VClos ((x,VClos rho t):env) b
|
||||||
return $ (AApp f' a' b', b', csf ++ csa)
|
return $ (AApp f' a' b', b', csf ++ csa)
|
||||||
_ -> prtBad ("Prod expected for function" +++ prt f +++ "instead of") typ
|
_ -> prtBad ("Prod expected for function" +++ prt f +++ "instead of") typ
|
||||||
_ -> prtBad "cannot infer type of expression" e
|
_ -> prtBad "cannot infer type of expression" e
|
||||||
|
where
|
||||||
|
predefAbs c s = case c of
|
||||||
|
IC "Int" -> return $ const $ Q cPredefAbs cInt
|
||||||
|
IC "String" -> return $ const $ Q cPredefAbs cString
|
||||||
|
_ -> Bad s
|
||||||
|
|
||||||
|
|
||||||
checkBranch :: Theory -> TCEnv -> Equation -> Val -> Err (([Exp],AExp),[(Val,Val)])
|
checkBranch :: Theory -> TCEnv -> Equation -> Val -> Err (([Exp],AExp),[(Val,Val)])
|
||||||
checkBranch th tenv b@(ps,t) ty = errIn ("branch" +++ show b) $
|
checkBranch th tenv b@(ps,t) ty = errIn ("branch" +++ show b) $
|
||||||
|
|||||||
Reference in New Issue
Block a user