GitHub/gf-core
1
0
Fork 1
mirror of https://github.com/GrammaticalFramework/gf-core.git synced 2026-08-19 10:46:22 -06:00
Code Issues Packages Projects Releases Wiki Activity

progress on the type checker

Browse Source
This commit is contained in:
Krasimir Angelov
2025-08-07 13:38:38 +02:00
parent ceb07da0c0
commit f2de64cd34
3 changed files with 258 additions and 232 deletions
Download Patch File Download Diff File Expand all files Collapse all files
src/compiler/api/GF/Compile/CheckGrammar.hs
+4 -4
View File
@@ -232,12 +232,12 @@ checkInfo opts cwd sgr sm (c,info) = checkInModule cwd (snd sm) NoLoc empty $ do
ResOverload os tysts -> chIn NoLoc "overloading" $ do
tysts' <- mapM (uncurry $ flip (\(L loc1 t) (L loc2 ty) -> checkLType g t ty >>= \(t,ty) -> return (L loc1 t, L loc2 ty))) tysts -- return explicit ones
tysts0 <- lookupOverload gr (fst sm,c) -- check against inherited ones too
tysts1 <- mapM (uncurry $ flip (checkLType g))
[(mkFunType args val,tr) | (args,(val,tr)) <- tysts0]
tysts1 <- sequence
[checkLType g tr (mkFunType args val) | (args,(val,tr)) <- tysts0]
--- this can only be a partial guarantee, since matching
--- with value type is only possible if expected type is given
checkUniq $
sort [let (xs,t) = typeFormCnc x in t : map (\(b,x,t) -> t) xs | (_,x) <- tysts1]
--checkUniq $
-- sort [let (xs,t) = typeFormCnc x in t : map (\(b,x,t) -> t) xs | (_,x) <- tysts1]
update sm c (ResOverload os [(y,x) | (x,y) <- tysts'])
ResParam (Just (L loc pcs)) _ -> do
src/compiler/api/GF/Compile/Compute/Concrete2.hs
+16 -19
View File
@@ -65,7 +65,7 @@ data Value
| VGen {-# UNPACK #-} !Int [Value]
| VClosure Env Choice Term
| VProd BindType Ident Value Value
| VRecType [(Label, Bool, Value)]
| VRecType [(Label, Bool, Value)] Bool
| VR [(Label, Value)]
| VP Value Label [Value]
| VExtR Value Value
@@ -89,7 +89,7 @@ data Value
| VReset Ident (Maybe Value) Value (Maybe QIdent)
| VSymCat Int LIndex [(LIndex, (Value, Type))]
| VError Doc
| VInts (Maybe Integer) (Maybe Integer)
| VInts Integer Bool
data Variants
= VarFree [Value]
@@ -106,7 +106,7 @@ unvariants (VarOpts n cs) = snd <$> cs
isCanonicalForm :: Bool -> Value -> Bool
isCanonicalForm flat (VClosure {}) = True
isCanonicalForm flat (VProd b x d cod) = isCanonicalForm flat d && isCanonicalForm flat cod
isCanonicalForm flat (VRecType fs) = all (\(l,_,ty) -> isCanonicalForm flat ty) fs
isCanonicalForm flat (VRecType fs _) = all (\(l,_,ty) -> isCanonicalForm flat ty) fs
isCanonicalForm flat (VR {}) = True
isCanonicalForm flat (VTable d cod) = isCanonicalForm flat d && isCanonicalForm flat cod
isCanonicalForm flat (VT {}) = True
@@ -200,7 +200,7 @@ eval g env s (Prod b x t1 t2)[]
| otherwise = let (s1,s2) = split s
in VProd b x (eval g env s1 t1 []) (VClosure env s2 t2)
eval g env s (Typed t ty) vs = eval g env s t vs
eval g env s (RecType lbls) [] = VRecType (mapC (\s (lbl,ty) -> (lbl, True, eval g env s ty [])) s lbls)
eval g env s (RecType lbls) [] = VRecType (mapC (\s (lbl,ty) -> (lbl, True, eval g env s ty [])) s lbls) False
eval g env s (R as) [] = VR (mapC (\s (lbl,(ty,t)) -> (lbl, eval g env s t [])) s as)
eval g env s (P t lbl) vs = let project (VR as) = case lookup lbl as of
Nothing -> VError ("Missing value for label" <+> pp lbl $$
@@ -214,7 +214,7 @@ eval g env s (P t lbl) vs = let project (VR as) = case lookup lbl a
eval g env s (ExtR t1 t2) [] = let (s1,s2) = split s
extend (VR as1) (VR as2) = VR (foldl (\as (lbl,v) -> update lbl v as) as1 as2)
extend (VRecType as1) (VRecType as2) = VRecType (foldl (\as (lbl,o,v) -> update3 lbl o v as) as1 as2)
extend (VRecType as1 e1) (VRecType as2 e2)=VRecType (foldl (\as (lbl,o,v) -> update3 lbl o v as) as1 as2) (e1 || e2)
extend (VFV i fvs) v2 = VFV i (mapVariants (`extend` v2) fvs)
extend v1 (VFV i fvs) = VFV i (mapVariants (v1 `extend`) fvs)
extend (VMeta i vs) v2 = VSusp i (\v -> extend (apply g v vs) v2) []
@@ -348,7 +348,7 @@ evalPredef g@(Gl gr pds) c n args =
stdPredef :: Globals -> PredefTable
stdPredef g = Map.fromList
[(cInts, pdArity 1 $\ \g c vs -> Const (case vs of {[VInt i] -> VInts (Just i) (Just i); vs -> VApp c (cPredef,cInts) vs}))
[(cInts, pdArity 1 $\ \g c vs -> Const (case vs of {[VInt i] -> VInts i False; vs -> VApp c (cPredef,cInts) vs}))
,(cLength, pdArity 1 $\ \g c [v] -> fmap (VInt . genericLength) (value2string g v))
,(cTake, pdArity 2 $\ \g c [v1,v2] -> fmap string2value (liftA2 genericTake (value2int g v1) (value2string g v2)))
,(cDrop, pdArity 2 $\ \g c [v1,v2] -> fmap string2value (liftA2 genericDrop (value2int g v1) (value2string g v2)))
@@ -392,9 +392,9 @@ bubble v = snd (bubble v)
bubble (VGen i vs) = liftL (VGen i) vs
bubble (VClosure env c t) = liftL' (\env -> VClosure env c t) env
bubble (VProd bt x v1 v2) = lift2 (VProd bt x) v1 v2
bubble v@(VRecType lbls) =
bubble v@(VRecType lbls ext) =
let (union,lbls') = mapAccumL descendR Map.empty lbls
in (union, addVariants (VRecType lbls') union)
in (union, addVariants (VRecType lbls' ext) union)
bubble (VR as) = liftL' VR as
bubble (VP v l vs) = lift1L (\v vs -> VP v l vs) v vs
bubble (VExtR v1 v2) = lift2 VExtR v1 v2
@@ -830,7 +830,7 @@ value2termM flat xs (VProd b x v1 v2) = do
t1 <- value2termM flat xs v1
t2 <- value2termM flat xs v2
return (Prod b x t1 t2)
value2termM flat xs (VRecType lbls) = do
value2termM flat xs (VRecType lbls _) = do
lbls <- mapM (\(lbl,_,v) -> fmap ((,) lbl) (value2termM flat xs v)) lbls
return (RecType lbls)
value2termM flat xs (VR as) = do
@@ -974,9 +974,7 @@ value2termM flat xs (VReset ctl mb_cv v mb_qid) = do
listify mn cat (t1:ts) = do t2 <- listify mn cat ts
return (App (App (QC (mn,identS ("Cons"++cat))) t1) t2)
value2termM flat xs (VError msg) = evalError msg
value2termM flat xs (VInts Nothing Nothing) = return (App (Q (cPredef,cInts)) (Meta 0))
value2termM flat xs (VInts (Just min) Nothing) = return (App (Q (cPredef,cInts)) (EInt min))
value2termM flat xs (VInts _ (Just max)) = return (App (Q (cPredef,cInts)) (EInt max))
value2termM flat xs (VInts n _) = return (App (Q (cPredef,cInts)) (EInt n))
value2termM flat xs v = evalError ("value2termM" <+> ppValue Unqualified 5 v)
@@ -1001,13 +999,13 @@ ppValue q d (VProd bt x a b) =
if x == identW && bt == Explicit
then prec d 0 (ppValue q 4 a <+> "->" <+> ppValue q 0 b)
else prec d 0 (parens (ppBind (bt,x) <+> ':' <+> ppValue q 0 a) <+> "->" <+> ppValue q 0 b)
ppValue q d (VRecType xs)
ppValue q d (VRecType xs ext)
| q == Terse = case [cat | (l,_,_) <- xs, let (p,cat) = splitAt 5 (showIdent (label2ident l)), p == "lock_"] of
[cat] -> pp cat
_ -> doc
| otherwise = doc
where
doc = braces (fsep (punctuate ';' [l <+> (if o then ":" else ":?") <+> ppValue q 0 v | (l,o,v) <- xs]))
doc = braces (fsep (punctuate ';' ([l <+> (if o then ":" else ":?") <+> ppValue q 0 v | (l,o,v) <- xs] ++ [pp ".." | ext])))
ppValue q d (VR _) = pp "VR"
ppValue q d (VP v l vs) = prec d 5 (hsep (ppValue q 5 v <> '.' <> l : map (ppValue q 5) vs))
ppValue q d (VExtR _ _) = pp "VExtR"
@@ -1027,17 +1025,16 @@ ppValue q d VEmpty = pp "[]"
ppValue q d (VC v1 v2) = prec d 1 (hang (ppValue q 2 v1) 2 ("++" <+> ppValue q 1 v2))
ppValue q d (VGlue v1 v2) = prec d 2 (ppValue q 3 v1 <+> '+' <+> ppValue q 2 v2)
ppValue q d (VPatt _ _ _) = pp "VPatt"
ppValue q d (VPattType _) = pp "VPattType"
ppValue q d (VPattType v) = prec d 4 ("pattern" <+> ppValue q 0 v)
ppValue q d (VFV i vs) = prec d 4 ("variants" <+> pp i <+> braces (fsep (punctuate ';' (map (ppValue q 0) (unvariants vs)))))
ppValue q d (VAlts e xs) = prec d 4 ("pre" <+> braces (ppValue q 0 e <> ';' <+> fsep (punctuate ';' (map (ppAltern q) xs))))
ppValue q d (VStrs _) = pp "VStrs"
ppValue q d (VMarkup _ _ _) = pp "VMarkup"
ppValue q d (VSymCat i r rs) = pp '<' <> pp i <> pp ',' <> pp r <> pp '>'
ppValue q d (VError msg) = prec d 4 (pp "error" <+> ppTerm q 5 (K (show msg)))
ppValue q d (VInts Nothing Nothing) = prec d 4 (pp "Ints ?")
ppValue q d (VInts (Just min) Nothing) = prec d 4 (pp "Ints" <+> brackets (pp min <> ".."))
ppValue q d (VInts Nothing (Just max)) = prec d 4 (pp "Ints" <+> brackets (".." <> pp max))
ppValue q d (VInts (Just min) (Just max)) = prec d 4 (pp "Ints" <+> brackets (pp min <> ".." <> pp max))
ppValue q d (VInts n ext)
| ext = prec d 4 (pp "Ints" <+> brackets (pp n <> ".."))
| otherwise = prec d 4 (pp "Ints" <+> pp n)
ppAltern q (x,y) = ppValue q 0 x <+> '/' <+> ppValue q 0 y
src/compiler/api/GF/Compile/TypeCheck/Concrete.hs
+238 -209
View File
@@ -75,7 +75,7 @@ vtypePType = VSort cPType
vtypeMarkup= VApp poison (cPredef,cMarkup) []
tcRho :: Scope -> Choice -> Term -> Maybe Rho -> EvalM (Term, Rho)
tcRho scope s t@(EInt i) mb_ty = instSigma scope s t (VInts (Just i) Nothing) mb_ty -- INT
tcRho scope s t@(EInt i) mb_ty = instSigma scope s t (VInts i True) mb_ty -- INT
tcRho scope s t@(EFloat _) mb_ty = instSigma scope s t vtypeFloat mb_ty -- FLOAT
tcRho scope s t@(K _) mb_ty = instSigma scope s t vtypeStr mb_ty -- STR
tcRho scope s t@(Empty) mb_ty = instSigma scope s t vtypeStr mb_ty
@@ -117,7 +117,7 @@ tcRho scope c (Abs bt var body) Nothing = do -- ABS1
VClosure env c t -> do g <- globals
check m (n+1) (b,x:xs) (eval g ((x,VGen n []):env) c t [])
v2 -> check m n st v2
check m n st (VRecType as) = foldM (\st (l,_,v) -> check m n st v) st as
check m n st (VRecType as _) = foldM (\st (l,_,v) -> check m n st v) st as
check m n st (VR as) =
foldM (\st (lbl,tnk) -> check m n st tnk) st as
check m n st (VP v l vs) =
@@ -200,7 +200,7 @@ tcRho scope c (FV ts) mb_ty = do
tcRho scope s t@(Sort _) mb_ty = do
instSigma scope s t vtypeType mb_ty
tcRho scope c t@(RecType rs) Nothing = do
(rs,mb_ty) <- tcRecTypeFields scope c rs Nothing
(rs,mb_ty) <- tcRecTypeFields scope c [] rs Nothing
return (RecType rs,fromMaybe vtypePType mb_ty)
tcRho scope c t@(RecType rs) (Just ty) = do
(scope,f,ty') <- skolemise scope ty
@@ -214,7 +214,7 @@ tcRho scope c t@(RecType rs) (Just ty) = do
ty -> do ty <- value2termM False (scopeVars scope) ty
evalError ("The record type" <+> ppTerm Unqualified 0 t $$
"cannot be of type" <+> ppTerm Unqualified 0 ty)
(rs,mb_ty) <- tcRecTypeFields scope c rs (Just ty')
(rs,mb_ty) <- tcRecTypeFields scope c [] rs (Just ty')
return (f (RecType rs),ty)
tcRho scope s t@(Table p res) mb_ty = do
let (s1,s23) = split s
@@ -241,15 +241,13 @@ tcRho scope c (S t p) mb_ty = do
return (S t p, res_ty)
tcRho scope c (T tt ps) Nothing = do -- ABS1/AABS1 for tables
let (c1,c2) = split c
let mk_val i = VMeta i []
p_ty <- case tt of
TRaw -> fmap mk_val $ newResiduation scope
TTyped ty -> do let (c3,c4) = split c1
(ty, _) <- tcRho scope c3 ty (Just vtypeType)
g <- globals
return (eval g (scopeEnv scope) c4 ty [])
res_ty <- fmap mk_val $ newResiduation scope
ps <- tcCases scope c2 ps p_ty res_ty
mb_p_ty <- case tt of
TRaw -> return Nothing
TTyped ty -> do let (c3,c4) = split c1
(ty, _) <- tcRho scope c3 ty (Just vtypeType)
g <- globals
return (Just (eval g (scopeEnv scope) c4 ty []))
(ps,p_ty,res_ty) <- tcCases scope c2 ps mb_p_ty Nothing
p_ty_t <- value2termM True [] p_ty
return (T (TTyped p_ty_t) ps, VTable p_ty res_ty)
tcRho scope c (T tt ps) (Just ty) = do -- ABS2/AABS2 for tables
@@ -262,8 +260,9 @@ tcRho scope c (T tt ps) (Just ty) = do -- ABS2/AABS2 for
TTyped ty -> do let (c1,c2) = split c12
(ty, _) <- tcRho scope c1 ty (Just vtypeType)
g <- globals
unify scope (eval g (scopeEnv scope) c2 ty []) p_ty
ps <- tcCases scope c3 ps p_ty res_ty
subsCheckRho scope (Meta 0) (eval g (scopeEnv scope) c2 ty []) p_ty
return ()
(ps,p_ty,res_ty) <- tcCases scope c3 ps (Just p_ty) (Just res_ty)
p_ty_t <- value2termM True (scopeVars scope) p_ty
return (f (T (TTyped p_ty_t) ps), VTable p_ty res_ty)
tcRho scope c (V p_ty ts) Nothing = do
@@ -290,22 +289,22 @@ tcRho scope c (V p_ty0 ts) (Just ty) = do
ts <- mapCM (\c t -> fmap fst $ tcRho scope c t (Just res_ty)) c3 ts
return (V p_ty0 ts, VTable p_ty res_ty)
tcRho scope c (R rs) Nothing = do
lttys <- inferRecFields scope c rs
lttys <- inferRecFields scope c [] rs
rs <- mapM (\(l,t,ty) -> value2termM True (scopeVars scope) ty >>= \ty -> return (l, (Just ty, t))) lttys
return (R rs,
VRecType [(l,True,ty) | (l,t,ty) <- lttys]
VRecType [(l,True,ty) | (l,t,ty) <- lttys] False
)
tcRho scope c (R rs) (Just ty) = do
(scope,f,ty') <- skolemise scope ty
case ty' of
(VRecType ltys) -> do lttys <- checkRecFields scope c rs ltys
(VRecType ltys _)->do lttys <- checkRecFields scope c [] rs ltys
rs <- mapM (\(l,t,ty) -> value2termM True (scopeVars scope) ty >>= \ty -> return (l, (Just ty, t))) lttys
return ((f . R) rs,
VRecType [(l,True,ty) | (l,t,ty) <- lttys]
VRecType [(l,True,ty) | (l,t,ty) <- lttys] False
)
ty -> do lttys <- inferRecFields scope c rs
ty -> do lttys <- inferRecFields scope c [] rs
t <- liftM (f . R) (mapM (\(l,t,ty) -> value2termM True (scopeVars scope) ty >>= \ty -> return (l, (Just ty, t))) lttys)
let ty' = VRecType [(l,True,ty) | (l,t,ty) <- lttys]
let ty' = VRecType [(l,True,ty) | (l,t,ty) <- lttys] False
(t,_,_) <- subsCheckRho scope t ty' ty
return (t, ty')
tcRho scope c (P t l) mb_ty = do
@@ -313,7 +312,7 @@ tcRho scope c (P t l) mb_ty = do
Just ty -> return ty
Nothing -> do i <- newResiduation scope
return (VMeta i [])
(t,t_ty) <- tcRho scope c t (Just (VRecType [(l,True,l_ty)]))
(t,t_ty) <- tcRho scope c t (Just (VRecType [(l,True,l_ty)] True))
return (P t l,l_ty)
tcRho scope c (C t1 t2) mb_ty = do
let (c1,c2,c3,c4) = split4 c
@@ -325,12 +324,21 @@ tcRho scope c (Glue t1 t2) mb_ty = do
(t1,t1_ty) <- tcRho scope c1 t1 (Just vtypeStr)
(t2,t2_ty) <- tcRho scope c2 t2 (Just vtypeStr)
instSigma scope c3 (Glue t1 t2) vtypeStr mb_ty
tcRho scope c t@(ExtR t1 t2) mb_ty = do
let (c1,c2,c3,c4) = split4 c
(t1,t1_ty) <- tcRho scope c1 t1 Nothing
(t2,t2_ty) <- tcRho scope c2 t2 Nothing
ty <- join t1_ty t2_ty
instSigma scope c3 (ExtR t1 t2) ty mb_ty
tcRho scope c t@(ExtR t1 t2) mb_ty =
case (mb_ty,t2) of
(Just (VRecType ltys ext),R ss) -> do
let ll2 = map fst ss
(c1,c2) = split c
(t1,t1_ty) <- tcRho scope c1 t1 (Just (VRecType [field | field@(l,_,_) <- ltys, not (elem l ll2)] ext))
(t2,t2_ty) <- tcRho scope c2 t2 (Just (VRecType [field | field@(l,_,_) <- ltys, elem l ll2] ext))
ty <- join t1_ty t2_ty
return (ExtR t1 t2, ty)
_ -> do
let (c1,c2,c3,c4) = split4 c
(t1,t1_ty) <- tcRho scope c1 t1 Nothing
(t2,t2_ty) <- tcRho scope c2 t2 Nothing
ty <- join t1_ty t2_ty
instSigma scope c3 (ExtR t1 t2) ty mb_ty
where
join (VMeta i vs) ty2 = do
mv <- getMeta i
@@ -349,9 +357,9 @@ tcRho scope c t@(ExtR t1 t2) mb_ty = do
(s2 == cType || s2 == cPType) = let sort | s1 == cPType && s2 == cPType = cPType
| otherwise = cType
in return (VSort sort)
join (VRecType rs1) (VRecType rs2) = do
join (VRecType rs1 ext1) (VRecType rs2 ext2) = do
rs <- foldM (\rs (l,o,ctr) -> extend l o ctr rs) rs1 rs2
return (VRecType rs)
return (VRecType rs (ext1 || ext2))
where
extend l o1 ty1 [] = do return [(l,o1,ty1)]
extend l o1 ty1 ((l',o2,ty2):rs)
@@ -388,15 +396,14 @@ tcRho scope c (EPattType ty) mb_ty = do
(ty, _) <- tcRho scope c1 ty (Just vtypeType)
instSigma scope c2 (EPattType ty) vtypeType mb_ty
tcRho scope c t@(EPatt min max p) mb_ty = do
(scope,f,ty) <- case mb_ty of
Nothing -> do i <- newResiduation scope
return (scope,id,VMeta i [])
Just ty -> do (scope,f,ty) <- skolemise scope ty
case ty of
VPattType ty -> return (scope,f,ty)
_ -> evalError (ppTerm Unqualified 0 t <+> "must be of pattern type but" <+> ppTerm Unqualified 0 t <+> "is expected")
tcPatt scope c p ty
return (f (EPatt min max p), ty)
(scope,f,mb_ty) <- case mb_ty of
Nothing -> return (scope,id,Nothing)
Just ty -> do (scope,f,ty) <- skolemise scope ty
case ty of
VPattType ty -> return (scope,f,Just ty)
_ -> evalError (ppTerm Unqualified 0 t <+> "must be of pattern type but" <+> ppTerm Unqualified 0 t <+> "is expected")
(_,ty) <- tcPatt scope c p mb_ty
return (f (EPatt min max p), VPattType ty)
tcRho scope c (Markup tag attrs children) mb_ty = do
let (c1,c2,c3,c4) = split4 c
attrs <- mapCM (\c (id,t) -> do
@@ -471,13 +478,13 @@ tcUnifying scope c ts mb_ty = do
ts <- mapCM go c ts
return (ts,ty)
tcCases scope c [] p_ty res_ty = return []
tcCases scope c ((p,t):cs) p_ty res_ty = do
tcCases scope c [] (Just p_ty) (Just res_ty) = return ([],p_ty,res_ty)
tcCases scope c ((p,t):cs) mb_p_ty mb_res_ty = do
let (c1,c2,c3,c4) = split4 c
scope' <- tcPatt scope c1 p p_ty
(t,_) <- tcRho scope' c2 t (Just res_ty)
cs <- tcCases scope c3 cs p_ty res_ty
return ((p,t):cs)
(scope',p_ty) <- tcPatt scope c1 p mb_p_ty
(t,res_ty) <- tcRho scope' c2 t mb_res_ty
(cs,p_ty,res_ty) <- tcCases scope c3 cs (Just p_ty) (Just res_ty)
return ((p,t):cs,p_ty,res_ty)
tcApp scope c t0 (App fun arg) args mb_ty = tcApp scope c t0 fun (arg:args) mb_ty -- APP
tcApp scope c t0 t@(Q id) args mb_ty = resolveOverloads scope c t0 id args mb_ty -- VAR (global)
@@ -581,11 +588,18 @@ reapply2 scope c fun fun_ty ((arg,arg_v,arg_ty):args) mb_ty = do -- Explicit arg
res_ty <- evalCodomain x arg_v res_ty
reapply2 scope c (App fun arg) res_ty args mb_ty
tcPatt scope c PW ty0 =
return scope
tcPatt scope c (PV x) ty0 =
return ((x,ty0):scope)
tcPatt scope c (PP q ps) ty0 = do
tcPatt scope c PW Nothing = do
i <- newResiduation scope
return (scope,VMeta i [])
tcPatt scope c PW (Just ty0) =
return (scope,ty0)
tcPatt scope c (PV x) Nothing = do
i <- newResiduation scope
let ty = VMeta i []
return ((x,ty):scope,ty)
tcPatt scope c (PV x) (Just ty) =
return ((x,ty):scope,ty)
tcPatt scope c (PP q ps) mb_ty = do
g@(Gl gr _) <- globals
ty <- case lookupResType gr q of
Ok ty -> return ty
@@ -593,111 +607,153 @@ tcPatt scope c (PP q ps) ty0 = do
let go scope c ty [] = return (scope,ty)
go scope c ty (p:ps) = do (_,_,arg_ty,res_ty) <- unifyFun scope ty
let (c1,c2) = split c
scope <- tcPatt scope c1 p arg_ty
(scope,arg_ty) <- tcPatt scope c1 p (Just arg_ty)
go scope c2 res_ty ps
let (c1,c2) = split c
(scope,ty) <- go scope c1 (eval g [] c2 ty []) ps
unify scope ty0 ty
return scope
tcPatt scope c p@(PInt i) ty0 =
case ty0 of
VInts min max
| i <= fromMaybe i max -> return scope
| otherwise -> evalError ("Ints" <+> i <+> "is not a subtype of" <+> ppValue Unqualified 0 ty0)
VMeta k vs -> do
(scope,res_ty) <- go scope c1 (eval g [] c2 ty []) ps
case mb_ty of
Just ty -> unify scope ty res_ty
Nothing -> return ()
return (scope,res_ty)
tcPatt scope c p@(PInt i) mb_ty =
case mb_ty of
Just ty0@(VInts n ext)
| i <= n -> return (scope,ty0)
| ext -> return (scope,VInts i ext)
| otherwise -> evalError ("Ints" <+> i <+> "is not a subtype of" <+> ppValue Unqualified 0 ty0)
Just ty0@(VMeta k vs) -> do
mv <- getMeta k
case mv of
Bound _ v -> do
Bound scope1 v -> do
g <- globals
tcPatt scope c p (apply g v vs)
(scope,ty) <- tcPatt scope c p (Just (apply g v vs))
setMeta k (Bound scope1 ty)
return (scope,ty0)
Residuation scope1 -> do
setMeta k (Bound scope1 (VInts (Just i) Nothing))
return scope
setMeta k (Bound scope1 (VInts i True))
return (scope,ty0)
Nothing -> return (scope,VInts i True)
_ -> evalError (pp "An integer must have an Int or Ints n type")
tcPatt scope c (PString s) ty0 = do
unify scope ty0 vtypeStr
return scope
tcPatt scope c PChar ty0 = do
unify scope ty0 vtypeStr
return scope
tcPatt scope c (PChars cs) ty0 = do
unify scope ty0 vtypeStr
return scope
tcPatt scope c (PSeq _ _ p1 _ _ p2) ty0 = do
unify scope ty0 vtypeStr
tcPatt scope c (PString s) mb_ty = do
case mb_ty of
Just ty -> unify scope ty vtypeStr
Nothing -> return ()
return (scope,vtypeStr)
tcPatt scope c PChar mb_ty = do
case mb_ty of
Just ty -> unify scope ty vtypeStr
Nothing -> return ()
return (scope,vtypeStr)
tcPatt scope c (PChars cs) mb_ty = do
case mb_ty of
Just ty -> unify scope ty vtypeStr
Nothing -> return ()
return (scope,vtypeStr)
tcPatt scope c (PSeq _ _ p1 _ _ p2) mb_ty = do
case mb_ty of
Just ty -> unify scope ty vtypeStr
Nothing -> return ()
let (c1,c2) = split c
scope <- tcPatt scope c1 p1 vtypeStr
scope <- tcPatt scope c2 p2 vtypeStr
return scope
tcPatt scope c (PRep _ _ p) ty0 = do
unify scope ty0 vtypeStr
tcPatt scope c p vtypeStr
tcPatt scope c (PAs x p) ty0 = do
tcPatt ((x,ty0):scope) c p ty0
tcPatt scope c p@(PR rs) ty0 =
case ty0 of
VRecType ltys ->
let go scope c [] = return scope
go scope c ((l,p):rs) =
case lookup3 l ltys of
Just ty -> do let (c1,c2) = split c
scope <- tcPatt scope c1 p ty
go scope c2 rs
Nothing -> do ty <- value2termM False (scopeVars scope) ty0
evalError (pp "Label" <+> pp l <+> " is not defined in the type of the pattern:" $$
nest 4 (ppTerm Unqualified 0 ty))
in go scope c rs
VMeta i vs -> do
g <- globals
(scope,_) <- tcPatt scope c1 p1 (Just vtypeStr)
(scope,_) <- tcPatt scope c2 p2 (Just vtypeStr)
return (scope,vtypeStr)
tcPatt scope c (PRep _ _ p) mb_ty = do
case mb_ty of
Just ty -> unify scope ty vtypeStr
Nothing -> return ()
tcPatt scope c p (Just vtypeStr)
tcPatt scope c (PAs x p) mb_ty = do
ty <- case mb_ty of
Just ty -> return ty
Nothing -> do i <- newResiduation scope
return (VMeta i [])
tcPatt ((x,ty):scope) c p (Just ty)
tcPatt scope c p@(PR rs) mb_ty =
case mb_ty of
Just (VRecType ltys ext) -> check scope c rs ltys ext
Just ty0@(VMeta i vs) -> do
mv <- getMeta i
case mv of
Bound _ v ->
tcPatt scope c p (apply g v vs)
Bound scope1 v ->
do g <- globals
(scope,ty) <- tcPatt scope c p (Just (apply g v vs))
setMeta i (Bound scope1 ty)
return (scope,ty0)
Residuation scope1 ->
let go scope c [] = return (scope,[])
go scope c ((l,p):rs) = do
i <- newResiduation scope
let ty = VMeta i []
(c1,c2) = split c
scope <- tcPatt scope c1 p ty
(scope,ltys) <- go scope c2 rs
return (scope,(l,True,ty):ltys)
in do (scope,ltys) <- go scope c rs
setMeta i (Bound scope1 (VRecType ltys))
return scope
do (scope,ltys) <- infer scope c rs
setMeta i (Bound scope1 (VRecType ltys True))
return (scope,ty0)
Nothing ->do (scope,ltys) <- infer scope c rs
return (scope,VRecType ltys True)
_ -> evalError (pp "An record must have an record type")
tcPatt scope c (PAlt p1 p2) ty0 = do
where
check scope c [] ltys ext = return (scope,VRecType ltys ext)
check scope c ((l,p):rs) ltys ext =
case lookup3 l ltys of
Just ty -> do let (c1,c2) = split c
(scope,ty) <- tcPatt scope c1 p (Just ty)
check scope c2 rs (update3 l True ty ltys) ext
Nothing
| ext -> do let (c1,c2) = split c
(scope,ty) <- tcPatt scope c1 p Nothing
check scope c2 rs (ltys++[(l,True,ty)]) ext
| otherwise
-> do ty <- value2termM False (scopeVars scope) (VRecType ltys ext)
evalError (pp "Label" <+> pp l <+> " is not defined in the type of the pattern:" $$
nest 4 (ppTerm Unqualified 0 ty))
infer scope c [] = return (scope,[])
infer scope c ((l,p):rs) = do
let (c1,c2) = split c
(scope,ty) <- tcPatt scope c1 p Nothing
(scope,ltys) <- infer scope c2 rs
return (scope,(l,True,ty):ltys)
tcPatt scope c (PNeg p) mb_ty = do
(_,ty) <- tcPatt scope c p mb_ty
return (scope, ty)
tcPatt scope c (PAlt p1 p2) mb_ty = do
let (c1,c2) = split c
tcPatt scope c1 p1 ty0
tcPatt scope c2 p2 ty0
return scope
tcPatt scope c (PM q) ty0 = do
(_,ty) <- tcPatt scope c1 p1 mb_ty
(_,ty) <- tcPatt scope c2 p2 (Just ty)
return (scope,ty)
tcPatt scope c (PM q) mb_ty = do
g@(Gl gr _) <- globals
ty <- case lookupResType gr q of
Ok ty -> return ty
Bad msg -> evalError (pp msg)
case ty of
EPattType ty
-> do unify scope ty0 (eval g [] c ty [])
return scope
-> do let vty = eval g [] c ty []
case mb_ty of
Just ty0 -> unify scope ty0 vty
Nothing -> return ()
return (scope,vty)
ty -> evalError ("Pattern type expected but " <+> pp ty <+> " found.")
tcPatt scope c p ty = unimplemented ("tcPatt "++show p)
inferRecFields scope c rs =
mapCM (\c (l,r) -> tcRecField scope c l r Nothing) c rs
inferRecFields scope c ls [] = return []
inferRecFields scope c ls ((l,t):lts)
| elem l ls = evalError ("Repeated definition for field" <+> l)
| otherwise = do
let (c1,c2) = split c
lt <- tcRecField scope c1 l t Nothing
lts <- inferRecFields scope c2 (l:ls) lts
return (lt:lts)
checkRecFields scope c [] ltys
checkRecFields scope c ls [] ltys
| null ltys = return []
| otherwise = evalError ("Missing fields:" <+> hsep [l | (l,_,_) <- ltys])
checkRecFields scope c ((l,t):lts) ltys =
case takeIt l ltys of
(Just ty,ltys) -> do let (c1,c2) = split c
ltty <- tcRecField scope c1 l t (Just ty)
lttys <- checkRecFields scope c2 lts ltys
return (ltty : lttys)
(Nothing,ltys) -> do evalWarn ("Discarded field:" <+> l)
lttys <- checkRecFields scope c lts ltys
return lttys -- ignore the field
checkRecFields scope c ls ((l,t):lts) ltys
| elem l ls = evalError ("Repeated definition for field" <+> l)
| otherwise =
case takeIt l ltys of
(Just ty,ltys) -> do let (c1,c2) = split c
ltty <- tcRecField scope c1 l t (Just ty)
lttys <- checkRecFields scope c2 ls lts ltys
return (ltty : lttys)
(Nothing,ltys) -> do evalWarn ("Discarded field:" <+> l)
lttys <- checkRecFields scope c ls lts ltys
return lttys -- ignore the field
where
takeIt l1 [] = (Nothing, [])
takeIt l1 (lty@(l2,_,ty):ltys)
@@ -716,20 +772,22 @@ tcRecField scope c l (mb_ann_ty,t) mb_ty = do
Nothing -> tcRho scope c t mb_ty
return (l,t,ty)
tcRecTypeFields scope c [] mb_ty = return ([],mb_ty)
tcRecTypeFields scope c ((l,ty):rs) mb_ty = do
let (c1,c2) = split c
(ty,sort) <- tcRho scope c1 ty mb_ty
mb_ty <- case sort of
VSort s
| s == cType -> return (Just sort)
| s == cPType -> return mb_ty
VMeta _ _ -> return mb_ty
_ -> do sort <- value2termM False (scopeVars scope) sort
evalError ("The record type field" <+> l <+> ':' <+> ppTerm Unqualified 0 ty $$
"cannot be of type" <+> ppTerm Unqualified 0 sort)
(rs,mb_ty) <- tcRecTypeFields scope c2 rs mb_ty
return ((l,ty):rs,mb_ty)
tcRecTypeFields scope c ls [] mb_ty = return ([],mb_ty)
tcRecTypeFields scope c ls ((l,ty):rs) mb_ty
| elem l ls = evalError ("Repeated definition for field" <+> l)
| otherwise = do
let (c1,c2) = split c
(ty,sort) <- tcRho scope c1 ty mb_ty
mb_ty <- case sort of
VSort s
| s == cType -> return (Just sort)
| s == cPType -> return mb_ty
VMeta _ _ -> return mb_ty
_ -> do sort <- value2termM False (scopeVars scope) sort
evalError ("The record type field" <+> l <+> ':' <+> ppTerm Unqualified 0 ty $$
"cannot be of type" <+> ppTerm Unqualified 0 sort)
(rs,mb_ty) <- tcRecTypeFields scope c2 (l:ls) rs mb_ty
return ((l,ty):rs,mb_ty)
-- | Invariant: if the third argument is (Just rho),
-- then rho is in weak-prenex form
@@ -824,26 +882,12 @@ subsCheckRho scope t ty1@(VApp _ p _) ty2@(VInts _ _) -- This is not cor
| p == (cPredef,cInt) = return (t,ty1,ty2) -- Should be only a temporary hack.
subsCheckRho scope t ty1@(VInts _ _) ty2@(VApp _ p _) -- Rule INT1
| p == (cPredef,cInt) = return (t,ty1,ty2)
subsCheckRho scope t ty1@(VInts i1 j1) ty2@(VInts i2 j2) -- Rule INT2
| j1 `less1` i2 = return (t,ty1,ty2)
| j1' `less1` i2' = return (t,VInts i1 j1',VInts i2' j2)
| otherwise = evalError ("In the term" <+> ppTerm Unqualified 0 t $$
ppValue Terse 0 ty1 <+> "is not a subtype of" <+> ppValue Terse 0 ty2)
where
less1 (Just x) (Just y) = x <= y
less1 _ _ = False
less2 (Just x) (Just y) = x <= y
less2 Nothing (Just y) = True
less2 _ _ = False
less3 (Just x) (Just y) = x <= y
less3 (Just x) Nothing = True
less3 _ _ = False
j1' = if i1 `less2` i2 then i2 else j1
i2' = if j1 `less3` j2 then j1 else i2
subsCheckRho scope t ty1@(VRecType rs1) ty2@(VRecType rs2) = do -- Rule REC
subsCheckRho scope t ty1@(VInts n1 ext1) ty2@(VInts n2 ext2) -- Rule INT2
| n1 <= n2 = return (t,ty1,ty2)
| ext2 = return (t,ty1,VInts n1 ext2)
| otherwise = evalError ("In the term" <+> ppTerm Unqualified 0 t $$
ppValue Terse 0 ty1 <+> "is not a subtype of" <+> ppValue Terse 0 ty2)
subsCheckRho scope t ty1@(VRecType rs1 ext1) ty2@(VRecType rs2 ext2) = do -- Rule REC
let mkAccess scope t =
case t of
ExtR t1 (R rs) ->
@@ -883,6 +927,8 @@ subsCheckRho scope t ty1 (VFV c (VarFree vs)) = do
subsCheckRho scope t (VFV c (VarFree vs)) ty2 = do
ty1 <- variants c vs
subsCheckRho scope t ty1 ty2
subsCheckRho scope t ty1@(VPattType (VSort s1)) ty2@(VSort s2) -- for backwards compatibility
| s1 == cStr && s2 == cStrs = return (t,ty1,ty2)
subsCheckRho scope t ty1 ty2 = do -- Rule EQ
unify scope ty1 ty2 -- Revert to ordinary unification
return (t,ty1,ty2)
@@ -909,29 +955,16 @@ subsCheckTbl scope t p1 r1 p2 r2 = do
p2_t <- value2termM True (scopeVars scope) p2
return (T (TTyped p2_t) [(PV x,t)],VTable p1 r1,VTable p2 r2)
{-subtype scope Nothing (VInts i2 j2) =
return (VInts Nothing j2)
subtype scope (Just (VMeta i vs)) ty2 = do
g <- globals
mv <- getMeta i
case mv of
Bound _ v -> subtype scope (Just (apply g v vs)) ty2-}
subtype scope (Just (VInts i1 j1)) (VInts i2 j2) =
case VInts (lift max i1 i2) (lift min j1 j2) of
ty@(VInts (Just i) (Just j))
| i > j -> evalError (ppValue Unqualified 0 ty <+> "is an empty type")
ty -> return ty
where
lift f Nothing Nothing = Nothing
lift f (Just x) Nothing = Just x
lift f Nothing (Just y) = Just y
lift f (Just x) (Just y) = Just (f x y)
subtype scope Nothing (VRecType ltys) = do
subtype scope Nothing (VInts i2 _) =
return (VInts i2 True)
subtype scope (Just (VInts n1 _)) (VInts n2 _) =
return (VInts (min n1 n2) False)
subtype scope Nothing (VRecType ltys ext) = do
lctrs <- mapM (\(l,o,ty) -> subtype scope Nothing ty >>= \ctr -> return (l,o,ctr)) ltys
return (VRecType lctrs)
subtype scope (Just (VRecType lctrs1)) (VRecType lctrs2) = do
return (VRecType lctrs ext)
subtype scope (Just (VRecType lctrs1 ext1)) (VRecType lctrs2 ext2) = do
lctrs <- foldM (\lctrs (l,o,ctr) -> union l o ctr lctrs) lctrs1 lctrs2
return (VRecType lctrs)
return (VRecType lctrs (ext1 || ext2))
where
union l o1 ctr1 [] = do ctr <- subtype scope Nothing ctr1
return [(l,True,ctr)]
@@ -958,24 +991,16 @@ subtype scope (Just ctr) ty = do
unify scope ctr ty
return ty
supertype scope Nothing (VInts i2 j2) =
return (VInts i2 Nothing)
supertype scope (Just (VInts i1 j1)) (VInts i2 j2) =
case VInts (lift min i1 i2) (lift max j1 j2) of
ty@(VInts (Just i) (Just j))
| i > j -> evalError (ppValue Unqualified 0 ty <+> "is an empty type")
ty -> return ty
where
lift f Nothing Nothing = Nothing
lift f (Just x) Nothing = Nothing
lift f Nothing (Just y) = Nothing
lift f (Just x) (Just y) = Just (f x y)
supertype scope Nothing (VRecType ltys) = do
supertype scope Nothing (VInts n2 _) =
return (VInts n2 True)
supertype scope (Just (VInts n1 _)) (VInts n2 _) =
return (VInts (max n1 n2) True)
supertype scope Nothing (VRecType ltys ext) = do
lctrs <- mapM (\(l,o,ty) -> supertype scope Nothing ty >>= \ctr -> return (l,False,ctr)) ltys
return (VRecType lctrs)
supertype scope (Just (VRecType lctrs1)) (VRecType lctrs2) = do
return (VRecType lctrs ext)
supertype scope (Just (VRecType lctrs1 ext1)) (VRecType lctrs2 ext2) = do
lctrs <- foldM (\lctrs (l,o,ctr) -> intersect l o ctr lctrs lctrs2) [] lctrs1
return (VRecType lctrs)
return (VRecType lctrs (ext1 || ext2))
where
intersect l o1 ctr1 lctrs [] = return lctrs
intersect l o1 ctr1 lctrs ((l',o2,ctr2):lctrs2)
@@ -1077,9 +1102,7 @@ unify scope (VFlt x) (VFlt y)
unify scope (VStr s1) (VStr s2)
| s1 == s2 = return ()
unify scope VEmpty VEmpty = return ()
unify scope v1 v2 = do
t1 <- value2termM False (scopeVars scope) v1
t2 <- value2termM False (scopeVars scope) v2
unify scope v1 v2 =
evalError ("Cannot unify:" <+> ppValue Qualified 0 v1 $$
" with:" <+> ppValue Qualified 0 v2)
@@ -1124,7 +1147,7 @@ occursCheck scope' i0 scope v =
VClosure env c t -> do g <- globals
check (m+1) (n+1) (eval g ((x,VGen n []):env) c t [])
_ -> check m n ty2
check m n (VRecType as) =
check m n (VRecType as _) =
mapM_ (\(_,_,v) -> check m n v) as
check m n (VR as) =
mapM_ (\(lbl,v) -> check m n v) as
@@ -1231,9 +1254,9 @@ quantify scope t tvs ty = do
return (x:xs,VProd bt x v1 (VClosure env c t))
v2 -> do (xs,v2) <- check m (n+1) xs v2
return (x:xs,VProd bt x v1 v2)
check m n xs (VRecType as) = do
check m n xs (VRecType as ext) = do
(xs,as) <- mapAccumM (\xs (l,o,v) -> check m n xs v >>= \(xs,v) -> return (xs,(l,o,v))) xs as
return (xs,VRecType as)
return (xs,VRecType as ext)
check m n xs (VR as) = do
(xs,as) <- mapAccumM (\xs (lbl,tnk) -> check m n xs tnk >>= \(xs,tnk) -> return (xs,(lbl,tnk))) xs as
return (xs,VR as)
@@ -1324,6 +1347,11 @@ lookup3 l ((l',_,v):rs)
| l == l' = Just v
| otherwise = lookup3 l rs
update3 l o v [] = [(l,o,v)]
update3 l o v (r@(l',_,_):rs)
| l == l' = (l,o,v) : rs
| otherwise = r : update3 l o v rs
newVar :: Scope -> Ident
newVar scope = head [x | i <- [1..],
let x = identS ('v':show i),
@@ -1345,7 +1373,7 @@ getMetaVars sc_tys = foldM (\acc (scope,ty) -> go acc ty) [] sc_tys
go acc (VGen i args) = foldM go acc args
go acc (VSort s) = return acc
go acc (VInt _) = return acc
go acc (VRecType vs) = foldM (\acc (lbl,_,v) -> go acc v) acc vs
go acc (VRecType vs _) = foldM (\acc (lbl,_,v) -> go acc v) acc vs
go acc (VClosure _ _ _) = return acc
go acc (VProd b x v1 v2) = go acc v2 >>= \acc -> go acc v1
go acc (VTable v1 v2) = go acc v2 >>= \acc -> go acc v1
@@ -1357,7 +1385,8 @@ getMetaVars sc_tys = foldM (\acc (scope,ty) -> go acc ty) [] sc_tys
_ -> foldM go (m:acc) args
go acc (VApp c f args) = foldM go acc args
go acc (VFV c vs) = foldM go acc (unvariants vs)
go acc (VInts _ _) = return acc
go acc (VInts _ _) = return acc
go acc (VPattType v) = go acc v
go acc v = unimplemented ("go "++show (ppValue Unqualified 5 v))
-- | Eliminate any substitutions in a term