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

minimal set of changes to make Bulgarian compile with the new typechecker

Browse Source
This commit is contained in:
Krasimir Angelov
2025-05-21 13:39:03 +02:00
parent 6f9f187c70
commit fd27a2ebd3
2 changed files with 131 additions and 120 deletions
Download Patch File Download Diff File Expand all files Collapse all files
src/compiler/api/GF/Compile/Compute/Concrete2.hs
+47 -45
View File
@@ -65,7 +65,7 @@ data Value
| VGen {-# UNPACK #-} !Int [Value] | VGen {-# UNPACK #-} !Int [Value]
| VClosure Env Choice Term | VClosure Env Choice Term
| VProd BindType Ident Value Value | VProd BindType Ident Value Value
| VRecType [(Label, Value)] | VRecType [(Label, Bool, Value)]
| VR [(Label, Value)] | VR [(Label, Value)]
| VP Value Label [Value] | VP Value Label [Value]
| VExtR Value Value | VExtR Value Value
@@ -89,10 +89,7 @@ data Value
| VReset Ident (Maybe Value) Value (Maybe QIdent) | VReset Ident (Maybe Value) Value (Maybe QIdent)
| VSymCat Int LIndex [(LIndex, (Value, Type))] | VSymCat Int LIndex [(LIndex, (Value, Type))]
| VError Doc | VError Doc
-- These two constructors are only used internally | VInts (Maybe Integer) (Maybe Integer)
-- in the type checker.
| VCRecType [(Label, Bool, Value)]
| VCInts (Maybe Integer) (Maybe Integer)
data Variants data Variants
= VarFree [Value] = VarFree [Value]
@@ -109,7 +106,7 @@ unvariants (VarOpts n cs) = snd <$> cs
isCanonicalForm :: Bool -> Value -> Bool isCanonicalForm :: Bool -> Value -> Bool
isCanonicalForm flat (VClosure {}) = True isCanonicalForm flat (VClosure {}) = True
isCanonicalForm flat (VProd b x d cod) = isCanonicalForm flat d && isCanonicalForm flat cod isCanonicalForm flat (VProd b x d cod) = isCanonicalForm flat d && isCanonicalForm flat cod
isCanonicalForm flat (VRecType fs) = all (isCanonicalForm flat . snd) fs isCanonicalForm flat (VRecType fs) = all (\(l,_,ty) -> isCanonicalForm flat ty) fs
isCanonicalForm flat (VR {}) = True isCanonicalForm flat (VR {}) = True
isCanonicalForm flat (VTable d cod) = isCanonicalForm flat d && isCanonicalForm flat cod isCanonicalForm flat (VTable d cod) = isCanonicalForm flat d && isCanonicalForm flat cod
isCanonicalForm flat (VT {}) = True isCanonicalForm flat (VT {}) = True
@@ -197,10 +194,13 @@ eval g env s (Abs b x t) [] = VClosure env s (Abs b x t)
eval g env s (Abs b x t) (v:vs) = eval g ((x,v):env) s t vs eval g env s (Abs b x t) (v:vs) = eval g ((x,v):env) s t vs
eval g env s (Meta i) vs = VMeta i vs eval g env s (Meta i) vs = VMeta i vs
eval g env s (ImplArg t) [] = eval g env s t [] eval g env s (ImplArg t) [] = eval g env s t []
eval g env s (Prod b x t1 t2)[] = let (s1,s2) = split s eval g env s (Prod b x t1 t2)[]
| x == identW = let (s1,s2) = split s
in VProd b x (eval g env s1 t1 []) (eval g env s2 t2 [])
| otherwise = let (s1,s2) = split s
in VProd b x (eval g env s1 t1 []) (VClosure env s2 t2) 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 (Typed t ty) vs = eval g env s t vs
eval g env s (RecType lbls) [] = VRecType (mapC (\s (lbl,ty) -> (lbl, 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)
eval g env s (R as) [] = VR (mapC (\s (lbl,(ty,t)) -> (lbl, eval g env s t [])) s as) 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 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 $$ 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 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 (VR as1) (VR as2) = VR (foldl (\as (lbl,v) -> update lbl v as) as1 as2)
extend (VRecType as1) (VRecType as2) = VRecType (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 (VFV i fvs) v2 = VFV i (mapVariants (`extend` v2) fvs) extend (VFV i fvs) v2 = VFV i (mapVariants (`extend` v2) fvs)
extend v1 (VFV i fvs) = VFV i (mapVariants (v1 `extend`) 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) [] extend (VMeta i vs) v2 = VSusp i (\v -> extend (apply g v vs) v2) []
@@ -391,7 +391,9 @@ bubble v = snd (bubble v)
bubble (VGen i vs) = liftL (VGen i) vs bubble (VGen i vs) = liftL (VGen i) vs
bubble (VClosure env c t) = liftL' (\env -> VClosure env c t) env 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 (VProd bt x v1 v2) = lift2 (VProd bt x) v1 v2
bubble (VRecType as) = liftL' VRecType as bubble v@(VRecType lbls) =
let (union,lbls') = mapAccumL descendR Map.empty lbls
in (union, addVariants (VRecType lbls') union)
bubble (VR as) = liftL' VR as bubble (VR as) = liftL' VR as
bubble (VP v l vs) = lift1L (\v vs -> VP v l vs) v vs bubble (VP v l vs) = lift1L (\v vs -> VP v l vs) v vs
bubble (VExtR v1 v2) = lift2 VExtR v1 v2 bubble (VExtR v1 v2) = lift2 VExtR v1 v2
@@ -427,10 +429,7 @@ bubble v = snd (bubble v)
let (union,vs') = mapAccumL descendC Map.empty vs let (union,vs') = mapAccumL descendC Map.empty vs
in (union, addVariants (VSymCat d i0 vs') union) in (union, addVariants (VSymCat d i0 vs') union)
bubble v@(VError _) = lift0 v bubble v@(VError _) = lift0 v
bubble v@(VCRecType lbls) = bubble v@(VInts _ _) = lift0 v
let (union,lbls') = mapAccumL descendR Map.empty lbls
in (union, addVariants (VCRecType lbls') union)
bubble v@(VCInts _ _) = lift0 v
lift0 v = (Map.empty, v) lift0 v = (Map.empty, v)
@@ -527,6 +526,11 @@ update lbl v (a@(lbl',_):as)
| lbl==lbl' = (lbl,v) : as | lbl==lbl' = (lbl,v) : as
| otherwise = a : update lbl v as | otherwise = a : update lbl v as
update3 lbl o v [] = [(lbl,o,v)]
update3 lbl o v (a@(lbl',o',_):as)
| lbl==lbl' = (lbl,o||o',v) : as
| otherwise = a : update3 lbl o v as
patternMatch g s v0 [] = v0 patternMatch g s v0 [] = v0
patternMatch g s v0 ((env0,ps,args0,t):eqs) = match env0 ps eqs args0 patternMatch g s v0 ((env0,ps,args0,t):eqs) = match env0 ps eqs args0
where where
@@ -822,23 +826,19 @@ value2termM flat xs (VClosure env s (Abs b x t)) = do
x' = mkFreshVar xs x x' = mkFreshVar xs x
t <- value2termM flat (x':xs) v t <- value2termM flat (x':xs) v
return (Abs b x' t) return (Abs b x' t)
value2termM flat xs (VProd b x v1 v2) value2termM flat xs (VClosure env s t) = do
| x == identW = do t1 <- value2termM flat xs v1 return t
v2 <- case v2 of value2termM flat xs (VProd b x v1 (VClosure env c2 t2)) = do
VClosure env s t2 -> do g <- globals g <- globals
return (eval g env s t2 []) t1 <- value2termM flat xs v1
v2 -> return v2 t2 <- value2termM flat (x:xs) (eval g ((x,VGen (length xs) []):env) c2 t2 [])
t2 <- value2termM flat xs v2 return (Prod b (mkFreshVar xs x) t1 t2)
return (Prod b x t1 t2) value2termM flat xs (VProd b x v1 v2) = do
| otherwise = do t1 <- value2termM flat xs v1 t1 <- value2termM flat xs v1
v2 <- case v2 of t2 <- value2termM flat xs v2
VClosure env s t2 -> do g <- globals return (Prod b x t1 t2)
return (eval g ((x,VGen (length xs) []):env) s t2 [])
v2 -> return v2
t2 <- value2termM flat (x:xs) v2
return (Prod b (mkFreshVar xs 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 lbls <- mapM (\(lbl,_,v) -> fmap ((,) lbl) (value2termM flat xs v)) lbls
return (RecType lbls) return (RecType lbls)
value2termM flat xs (VR as) = do value2termM flat xs (VR as) = do
as <- mapM (\(lbl,v) -> fmap (\t -> (lbl,(Nothing,t))) (value2termM flat xs v)) as as <- mapM (\(lbl,v) -> fmap (\t -> (lbl,(Nothing,t))) (value2termM flat xs v)) as
@@ -972,12 +972,9 @@ value2termM flat xs (VReset ctl mb_cv v mb_qid) = do
listify mn cat (t1:ts) = do t2 <- listify mn cat ts listify mn cat (t1:ts) = do t2 <- listify mn cat ts
return (App (App (QC (mn,identS ("Cons"++cat))) t1) t2) return (App (App (QC (mn,identS ("Cons"++cat))) t1) t2)
value2termM flat xs (VError msg) = evalError msg value2termM flat xs (VError msg) = evalError msg
value2termM flat xs (VCRecType lbls) = do value2termM flat xs (VInts Nothing Nothing) = return (App (QC (cPredef,cInts)) (Meta 0))
lbls <- mapM (\(lbl,_,v) -> fmap ((,) lbl) (value2termM flat xs v)) lbls value2termM flat xs (VInts (Just min) Nothing) = return (App (QC (cPredef,cInts)) (EInt min))
return (RecType lbls) value2termM flat xs (VInts _ (Just max)) = return (App (QC (cPredef,cInts)) (EInt max))
value2termM flat xs (VCInts Nothing Nothing) = return (App (QC (cPredef,cInts)) (Meta 0))
value2termM flat xs (VCInts (Just min) Nothing) = return (App (QC (cPredef,cInts)) (EInt min))
value2termM flat xs (VCInts _ (Just max)) = return (App (QC (cPredef,cInts)) (EInt max))
value2termM flat xs v = evalError ("value2termM" <+> ppValue Unqualified 5 v) value2termM flat xs v = evalError ("value2termM" <+> ppValue Unqualified 5 v)
@@ -999,11 +996,17 @@ ppValue q d (VSusp i k vs) = prec d 4 (hsep (pp "#susp" : (if i > 0 then pp "?"
ppValue q d (VGen _ _) = pp "VGen" ppValue q d (VGen _ _) = pp "VGen"
ppValue q d (VClosure env c t) = pp "[|" <> ppTerm q 4 t <> pp "|]" ppValue q d (VClosure env c t) = pp "[|" <> ppTerm q 4 t <> pp "|]"
ppValue q d (VProd _ _ _ _) = pp "VProd" ppValue q d (VProd _ _ _ _) = pp "VProd"
ppValue q d (VRecType _) = pp "VRecType" ppValue q d (VRecType xs)
| 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]))
ppValue q d (VR _) = pp "VR" 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 (VP v l vs) = prec d 5 (hsep (ppValue q 5 v <> '.' <> l : map (ppValue q 5) vs))
ppValue q d (VExtR _ _) = pp "VExtR" ppValue q d (VExtR _ _) = pp "VExtR"
ppValue q d (VTable _ _) = pp "VTable" ppValue q d (VTable kt vt) = prec d 0 (ppValue q 3 kt <+> "=>" <+> ppValue q 0 vt)
ppValue q d (VT t _ _ cs) = "table" <+> ppValue q 0 t <+> '{' $$ ppValue q d (VT t _ _ cs) = "table" <+> ppValue q 0 t <+> '{' $$
nest 2 (vcat (punctuate ';' (map (ppCase q) cs))) $$ nest 2 (vcat (punctuate ';' (map (ppCase q) cs))) $$
'}' '}'
@@ -1026,13 +1029,12 @@ ppValue q d (VStrs _) = pp "VStrs"
ppValue q d (VMarkup _ _ _) = pp "VMarkup" ppValue q d (VMarkup _ _ _) = pp "VMarkup"
ppValue q d (VSymCat i r rs) = pp '<' <> pp i <> pp ',' <> pp r <> pp '>' 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 (VError msg) = prec d 4 (pp "error" <+> ppTerm q 5 (K (show msg)))
ppValue q d (VCRecType ass) = pp "VCRecType" ppValue q d (VInts Nothing Nothing) = prec d 4 (pp "Ints ?")
ppValue q d (VCInts 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 (VCInts (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 (VCInts Nothing (Just max)) = prec d 4 (pp "Ints" <+> brackets (".." <> pp max)) ppValue q d (VInts (Just min) (Just max))
ppValue q d (VCInts (Just min) (Just max)) | min == max = prec d 4 (pp "Ints" <+> min)
| min == max = prec d 4 (pp "Ints" <+> min) | otherwise = prec d 4 (pp "Ints" <+> brackets (pp min <> ".." <> pp max))
| otherwise = prec d 4 (pp "Ints" <+> brackets (pp min <> ".." <> pp max))
ppAltern q (x,y) = ppValue q 0 x <+> '/' <+> ppValue q 0 y ppAltern q (x,y) = ppValue q 0 x <+> '/' <+> ppValue q 0 y
src/compiler/api/GF/Compile/TypeCheck/ConcreteNew.hs
+84 -75
View File
@@ -118,7 +118,7 @@ tcRho scope c (Abs bt var body) Nothing = do -- ABS1
VClosure env c t -> do g <- globals VClosure env c t -> do g <- globals
check m (n+1) (b,x:xs) (eval g ((x,VGen n []):env) c t []) check m (n+1) (b,x:xs) (eval g ((x,VGen n []):env) c t [])
v2 -> check m n st v2 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) = check m n st (VR as) =
foldM (\st (lbl,tnk) -> check m n st tnk) st as foldM (\st (lbl,tnk) -> check m n st tnk) st as
check m n st (VP v l vs) = check m n st (VP v l vs) =
@@ -156,13 +156,13 @@ tcRho scope c t@(Abs Implicit var body) (Just ty) = do -- ABS2
if bt == Implicit if bt == Implicit
then return () then return ()
else evalError (ppTerm Unqualified 0 t <+> "is an implicit function, but no implicit function is expected") else evalError (ppTerm Unqualified 0 t <+> "is an implicit function, but no implicit function is expected")
body_ty <- evalCodomain scope x body_ty body_ty <- evalCodomain x (VGen (length scope) []) body_ty
(body, body_ty) <- tcRho ((var,var_ty):scope) c body (Just body_ty) (body, body_ty) <- tcRho ((var,var_ty):scope) c body (Just body_ty)
return (Abs Implicit var body,ty) return (Abs Implicit var body,ty)
tcRho scope c (Abs Explicit var body) (Just ty) = do -- ABS3 tcRho scope c (Abs Explicit var body) (Just ty) = do -- ABS3
(scope,f,ty') <- skolemise scope ty (scope,f,ty') <- skolemise scope ty
(_,x,var_ty,body_ty) <- unifyFun scope ty' (_,x,var_ty,body_ty) <- unifyFun scope ty'
body_ty <- evalCodomain scope x body_ty body_ty <- evalCodomain x (VGen (length scope) []) body_ty
(body, body_ty) <- tcRho ((var,var_ty):scope) c body (Just body_ty) (body, body_ty) <- tcRho ((var,var_ty):scope) c body (Just body_ty)
return (f (Abs Explicit var body),ty) return (f (Abs Explicit var body),ty)
tcRho scope c (Meta _) mb_ty = do tcRho scope c (Meta _) mb_ty = do
@@ -292,7 +292,7 @@ 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 rs <- mapM (\(l,t,ty) -> value2termM True (scopeVars scope) ty >>= \ty -> return (l, (Just ty, t))) lttys
return (R rs, return (R rs,
VRecType [(l, ty) | (l,t,ty) <- lttys] VRecType [(l,True,ty) | (l,t,ty) <- lttys]
) )
tcRho scope c (R rs) (Just ty) = do tcRho scope c (R rs) (Just ty) = do
(scope,f,ty') <- skolemise scope ty (scope,f,ty') <- skolemise scope ty
@@ -300,11 +300,11 @@ tcRho scope c (R rs) (Just ty) = do
(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 rs <- mapM (\(l,t,ty) -> value2termM True (scopeVars scope) ty >>= \ty -> return (l, (Just ty, t))) lttys
return ((f . R) rs, return ((f . R) rs,
VRecType [(l, ty) | (l,t,ty) <- lttys] VRecType [(l,True,ty) | (l,t,ty) <- lttys]
) )
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) t <- liftM (f . R) (mapM (\(l,t,ty) -> value2termM True (scopeVars scope) ty >>= \ty -> return (l, (Just ty, t))) lttys)
let ty' = VRecType [(l, ty) | (l,t,ty) <- lttys] let ty' = VRecType [(l,True,ty) | (l,t,ty) <- lttys]
t <- subsCheckRho scope t ty' ty t <- subsCheckRho scope t ty' ty
return (t, ty') return (t, ty')
tcRho scope c (P t l) mb_ty = do tcRho scope c (P t l) mb_ty = do
@@ -312,7 +312,7 @@ tcRho scope c (P t l) mb_ty = do
Just ty -> return ty Just ty -> return ty
Nothing -> do i <- newResiduation scope Nothing -> do i <- newResiduation scope
return (VMeta i []) return (VMeta i [])
(t,t_ty) <- tcRho scope c t (Just (VRecType [(l,l_ty)])) (t,t_ty) <- tcRho scope c t (Just (VRecType [(l,True,l_ty)]))
return (P t l,l_ty) return (P t l,l_ty)
tcRho scope c (C t1 t2) mb_ty = do tcRho scope c (C t1 t2) mb_ty = do
let (c1,c2,c3,c4) = split4 c let (c1,c2,c3,c4) = split4 c
@@ -423,11 +423,11 @@ tcRho scope s (Opts n cs) mb_ty = do
return (Opts n (zip ls ts), ty) return (Opts n (zip ls ts), ty)
tcRho scope s t _ = unimplemented ("tcRho "++show t) tcRho scope s t _ = unimplemented ("tcRho "++show t)
evalCodomain :: Scope -> Ident -> Value -> EvalM Value evalCodomain :: Ident -> Value -> Value -> EvalM Value
evalCodomain scope x (VClosure env c t) = do evalCodomain x v (VClosure env c ty) = do
g <- globals g <- globals
return (eval g ((x,VGen (length scope) []):env) c t []) return (eval g ((x,v):env) c ty [])
evalCodomain scope x t = return t evalCodomain x _ ty = return ty
tcUnifying :: Scope -> Choice -> [Term] -> Maybe Rho -> EvalM ([Term], Constraint) tcUnifying :: Scope -> Choice -> [Term] -> Maybe Rho -> EvalM ([Term], Constraint)
tcUnifying scope c ts mb_ty = do tcUnifying scope c ts mb_ty = do
@@ -471,20 +471,16 @@ reapply1 scope c fun fun_ty ((ImplArg arg):args) = do -- Implicit arg case
evalError (ppTerm Unqualified 0 (App fun (ImplArg arg)) <+> evalError (ppTerm Unqualified 0 (App fun (ImplArg arg)) <+>
"is an implicit argument application, but no implicit argument is expected") "is an implicit argument application, but no implicit argument is expected")
(arg,_) <- tcRho scope c1 arg (Just arg_ty) (arg,_) <- tcRho scope c1 arg (Just arg_ty)
res_ty <- case res_ty of g <- globals
VClosure res_env res_c res_ty -> do g <- globals res_ty <- evalCodomain x (eval g (scopeEnv scope) c2 arg []) res_ty
return (eval g ((x,eval g (scopeEnv scope) c2 arg []):res_env) res_c res_ty [])
res_ty -> return res_ty
reapply1 scope c3 (App fun (ImplArg arg)) res_ty args reapply1 scope c3 (App fun (ImplArg arg)) res_ty args
reapply1 scope c fun fun_ty (arg:args) = do -- Explicit arg (fallthrough) case reapply1 scope c fun fun_ty (arg:args) = do -- Explicit arg (fallthrough) case
let (c1,c2,c3,c4) = split4 c let (c1,c2,c3,c4) = split4 c
(fun,fun_ty) <- instantiate scope fun fun_ty (fun,fun_ty) <- instantiate scope fun fun_ty
(_, x, arg_ty, res_ty) <- unifyFun scope fun_ty (_, x, arg_ty, res_ty) <- unifyFun scope fun_ty
(arg,_) <- tcRho scope c1 arg (Just arg_ty) (arg,_) <- tcRho scope c1 arg (Just arg_ty)
res_ty <- case res_ty of g <- globals
VClosure res_env res_c res_ty -> do g <- globals res_ty <- evalCodomain x (eval g (scopeEnv scope) c2 arg []) res_ty
return (eval g ((x,eval g (scopeEnv scope) c2 arg []):res_env) res_c res_ty [])
res_ty -> return res_ty
reapply1 scope c3 (App fun arg) res_ty args reapply1 scope c3 (App fun arg) res_ty args
resolveOverloads :: Scope -> Choice -> Term -> QIdent -> [Term] -> Maybe Rho -> EvalM (Term,Rho) resolveOverloads :: Scope -> Choice -> Term -> QIdent -> [Term] -> Maybe Rho -> EvalM (Term,Rho)
@@ -566,19 +562,13 @@ reapply2 scope c fun fun_ty ((ImplArg arg,arg_v,arg_ty):args) mb_ty = do -- Impl
evalError (ppTerm Unqualified 0 (App fun (ImplArg arg)) <+> evalError (ppTerm Unqualified 0 (App fun (ImplArg arg)) <+>
"is an implicit argument application, but no implicit argument is expected") "is an implicit argument application, but no implicit argument is expected")
arg <- subsCheckRho scope arg arg_ty' arg_ty arg <- subsCheckRho scope arg arg_ty' arg_ty
res_ty <- case res_ty of res_ty <- evalCodomain x arg_v res_ty
VClosure res_env res_c res_ty -> do g <- globals
return (eval g ((x,arg_v):res_env) res_c res_ty [])
res_ty -> return res_ty
reapply2 scope c (App fun (ImplArg arg)) res_ty args mb_ty reapply2 scope c (App fun (ImplArg arg)) res_ty args mb_ty
reapply2 scope c fun fun_ty ((arg,arg_v,arg_ty):args) mb_ty = do -- Explicit arg (fallthrough) case reapply2 scope c fun fun_ty ((arg,arg_v,arg_ty):args) mb_ty = do -- Explicit arg (fallthrough) case
(fun,fun_ty) <- instantiate scope fun fun_ty (fun,fun_ty) <- instantiate scope fun fun_ty
(_, x, arg_ty', res_ty) <- unifyFun scope fun_ty (_, x, arg_ty', res_ty) <- unifyFun scope fun_ty
arg <- subsCheckRho scope arg arg_ty arg_ty' arg <- subsCheckRho scope arg arg_ty arg_ty'
res_ty <- case res_ty of res_ty <- evalCodomain x arg_v res_ty
VClosure res_env res_c res_ty -> do g <- globals
return (eval g ((x,arg_v):res_env) res_c res_ty [])
res_ty -> return res_ty
reapply2 scope c (App fun arg) res_ty args mb_ty reapply2 scope c (App fun arg) res_ty args mb_ty
tcPatt scope c PW ty0 = tcPatt scope c PW ty0 =
@@ -600,7 +590,7 @@ tcPatt scope c (PP q ps) ty0 = do
unify scope ty0 ty unify scope ty0 ty
return scope return scope
tcPatt scope c (PInt i) ty0 = do tcPatt scope c (PInt i) ty0 = do
unify scope (vtypeInts i) ty0 subsCheckRho scope (EInt i) (vtypeInts i) ty0
return scope return scope
tcPatt scope c (PString s) ty0 = do tcPatt scope c (PString s) ty0 = do
unify scope ty0 vtypeStr unify scope ty0 vtypeStr
@@ -608,12 +598,18 @@ tcPatt scope c (PString s) ty0 = do
tcPatt scope c PChar ty0 = do tcPatt scope c PChar ty0 = do
unify scope ty0 vtypeStr unify scope ty0 vtypeStr
return scope return scope
tcPatt scope c (PChars cs) ty0 = do
unify scope ty0 vtypeStr
return scope
tcPatt scope c (PSeq _ _ p1 _ _ p2) ty0 = do tcPatt scope c (PSeq _ _ p1 _ _ p2) ty0 = do
unify scope ty0 vtypeStr unify scope ty0 vtypeStr
let (c1,c2) = split c let (c1,c2) = split c
scope <- tcPatt scope c1 p1 vtypeStr scope <- tcPatt scope c1 p1 vtypeStr
scope <- tcPatt scope c2 p2 vtypeStr scope <- tcPatt scope c2 p2 vtypeStr
return scope 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 scope c (PAs x p) ty0 = do
tcPatt ((x,ty0):scope) c p ty0 tcPatt ((x,ty0):scope) c p ty0
tcPatt scope c (PR rs) ty0 = do tcPatt scope c (PR rs) ty0 = do
@@ -626,7 +622,7 @@ tcPatt scope c (PR rs) ty0 = do
scope <- tcPatt scope c1 p ty scope <- tcPatt scope c1 p ty
go scope c2 rs go scope c2 rs
ltys <- mk_ltys rs ltys <- mk_ltys rs
subsCheckRho scope (EPatt 0 Nothing (PR rs)) (VRecType [(l,ty) | (l,p,ty) <- ltys]) ty0 subsCheckRho scope (EPatt 0 Nothing (PR rs)) (VRecType [(l,True,ty) | (l,p,ty) <- ltys]) ty0
go scope c ltys go scope c ltys
tcPatt scope c (PAlt p1 p2) ty0 = do tcPatt scope c (PAlt p1 p2) ty0 = do
let (c1,c2) = split c let (c1,c2) = split c
@@ -650,7 +646,7 @@ inferRecFields scope c rs =
checkRecFields scope c [] ltys checkRecFields scope c [] ltys
| null ltys = return [] | null ltys = return []
| otherwise = evalError ("Missing fields:" <+> hsep (map fst ltys)) | otherwise = evalError ("Missing fields:" <+> hsep [l | (l,_,_) <- ltys])
checkRecFields scope c ((l,t):lts) ltys = checkRecFields scope c ((l,t):lts) ltys =
case takeIt l ltys of case takeIt l ltys of
(Just ty,ltys) -> do let (c1,c2) = split c (Just ty,ltys) -> do let (c1,c2) = split c
@@ -664,7 +660,7 @@ checkRecFields scope c ((l,t):lts) ltys =
return lttys -- ignore the field return lttys -- ignore the field
where where
takeIt l1 [] = (Nothing, []) takeIt l1 [] = (Nothing, [])
takeIt l1 (lty@(l2,ty):ltys) takeIt l1 (lty@(l2,_,ty):ltys)
| l1 == l2 = (Just ty,ltys) | l1 == l2 = (Just ty,ltys)
| otherwise = let (mb_ty,ltys') = takeIt l1 ltys | otherwise = let (mb_ty,ltys') = takeIt l1 ltys
in (mb_ty,lty:ltys') in (mb_ty,lty:ltys')
@@ -765,7 +761,7 @@ subsCheckRho scope t (VProd Implicit x ty1 ty2) rho2 = do -- Rule SPEC
subsCheckRho scope (App t (ImplArg (Meta i))) ty2' rho2 subsCheckRho scope (App t (ImplArg (Meta i))) ty2' rho2
subsCheckRho scope t rho1 (VProd Implicit x ty1 ty2) = do -- Rule SKOL subsCheckRho scope t rho1 (VProd Implicit x ty1 ty2) = do -- Rule SKOL
let v = newVar scope let v = newVar scope
ty2 <- evalCodomain scope x ty2 ty2 <- evalCodomain x (VGen (length scope) []) ty2
t <- subsCheckRho ((v,ty1):scope) t rho1 ty2 t <- subsCheckRho ((v,ty1):scope) t rho1 ty2
return (Abs Implicit v t) return (Abs Implicit v t)
subsCheckRho scope t rho1 (VProd Explicit _ a2 r2) = do -- Rule FUN subsCheckRho scope t rho1 (VProd Explicit _ a2 r2) = do -- Rule FUN
@@ -802,14 +798,14 @@ subsCheckRho scope t ty1@(VRecType rs1) ty2@(VRecType rs2) = do -- Rule REC
,\l -> mkProj2 l `mplus` mkProj1 l ,\l -> mkProj2 l `mplus` mkProj1 l
,mkWrap1 . mkWrap2 ,mkWrap1 . mkWrap2
) )
R rs -> do sequence_ [evalWarn ("Discarded field:" <+> l) | (l,_) <- rs, isNothing (lookup l rs2)] R rs -> do sequence_ [evalWarn ("Discarded field:" <+> l) | (l,_) <- rs, isNothing (lookup3 l rs2)]
return (scope return (scope
,\l -> lookup l rs ,\l -> lookup l rs
,id ,id
) )
Vr x -> do return (scope Vr x -> do return (scope
,\l -> do VRecType rs <- lookup x scope ,\l -> do VRecType rs <- lookup x scope
ty <- lookup l rs ty <- lookup3 l rs
return (Nothing,P t l) return (Nothing,P t l)
,id ,id
) )
@@ -823,9 +819,14 @@ subsCheckRho scope t ty1@(VRecType rs1) ty2@(VRecType rs2) = do -- Rule REC
t <- subsCheckRho scope t ty1 ty2 t <- subsCheckRho scope t ty1 ty2
return (l, (mb_ty,t)) return (l, (mb_ty,t))
lookup3 l [] = Nothing
lookup3 l ((l',_,v):rs)
| l == l' = Just v
| otherwise = lookup3 l rs
(scope,mkProj,mkWrap) <- mkAccess scope t (scope,mkProj,mkWrap) <- mkAccess scope t
let fields = [(l,ty2,lookup l rs1) | (l,ty2) <- rs2] let fields = [(l,ty2,lookup3 l rs1) | (l,o2,ty2) <- rs2]
case [l | (l,_,Nothing) <- fields] of case [l | (l,_,Nothing) <- fields] of
[] -> return () [] -> return ()
missing -> evalError ("In the term" <+> pp t $$ missing -> evalError ("In the term" <+> pp t $$
@@ -859,31 +860,35 @@ subsCheckFun scope t a1 r1 a2 r2 = do
subsCheckTbl :: Scope -> Term -> Sigma -> Rho -> Sigma -> Rho -> EvalM Term subsCheckTbl :: Scope -> Term -> Sigma -> Rho -> Sigma -> Rho -> EvalM Term
subsCheckTbl scope t p1 r1 p2 r2 = do subsCheckTbl scope t p1 r1 p2 r2 = do
let x = newVar scope let x = newVar scope
xt <- subsCheckRho scope (Vr x) p2 p1 xt <- subsCheckRho ((x,p2):scope) (Vr x) p2 p1
t <- subsCheckRho ((x,vtypePType):scope) (S t xt) r1 r2 t <- subsCheckRho ((x,p2):scope) (S t xt) r1 r2
p2 <- value2termM True (scopeVars scope) p2 p2 <- value2termM True (scopeVars scope) p2
return (T (TTyped p2) [(PV x,t)]) return (T (TTyped p2) [(PV x,t)])
subtype scope Nothing (VApp c p [VInt i]) subtype scope Nothing (VApp c p [VInt i])
| p == (cPredef,cInts) = do | p == (cPredef,cInts) = do
return (VCInts Nothing (Just i)) return (VInts Nothing (Just i))
subtype scope (Just (VCInts i j)) (VApp c p [VInt k]) subtype scope (Just (VInts i j)) (VApp c p [VInt k])
| p == (cPredef,cInts) = do | p == (cPredef,cInts) = do
return (VCInts j (Just (maybe k (min k) i))) return (VInts j (Just (maybe k (min k) i)))
subtype scope Nothing (VRecType ltys) = do subtype scope Nothing (VRecType ltys) = do
lctrs <- mapM (\(l,ty) -> supertype scope Nothing ty >>= \ctr -> return (l,True,ctr)) ltys lctrs <- mapM (\(l,o,ty) -> subtype scope Nothing ty >>= \ctr -> return (l,o,ctr)) ltys
return (VCRecType lctrs) return (VRecType lctrs)
subtype scope (Just (VCRecType lctrs)) (VRecType ltys) = do subtype scope (Just (VRecType lctrs1)) (VRecType lctrs2) = do
lctrs <- foldM (\lctrs (l,ty) -> union l ty lctrs) lctrs ltys lctrs <- foldM (\lctrs (l,o,ctr) -> union l o ctr lctrs) lctrs1 lctrs2
return (VCRecType lctrs) return (VRecType lctrs)
where where
union l ty [] = do ctr <- subtype scope Nothing ty union l o1 ctr1 [] = do ctr <- subtype scope Nothing ctr1
return [(l,True,ctr)] return [(l,True,ctr)]
union l ty ((l',o,ctr):lctrs) union l o1 ctr1 ((l',o2,ctr2):lctrs)
| l == l' = do ctr <- subtype scope (Just ctr) ty | l == l' = do ctr <- subtype scope (Just ctr1) ctr2
return ((l,True,ctr):lctrs) return ((l,o1||o2,ctr):lctrs)
| otherwise = do lctrs <- union l ty lctrs | otherwise = do lctrs <- union l o1 ctr1 lctrs
return ((l',o,ctr):lctrs) return ((l',o2,ctr2):lctrs)
subtype scope (Just (VTable a1 r1)) (VTable a2 r2) = do
a <- supertype scope (Just a1) a2
r <- subtype scope (Just r1) r2
return (VTable a r)
subtype scope Nothing ty = return ty subtype scope Nothing ty = return ty
subtype scope (Just ctr) ty = do subtype scope (Just ctr) ty = do
unify scope ctr ty unify scope ctr ty
@@ -891,22 +896,26 @@ subtype scope (Just ctr) ty = do
supertype scope Nothing (VApp c p [VInt i]) supertype scope Nothing (VApp c p [VInt i])
| p == (cPredef,cInts) = do | p == (cPredef,cInts) = do
return (VCInts (Just i) Nothing) return (VInts (Just i) Nothing)
supertype scope (Just (VCInts i j)) (VApp c p [VInt k]) supertype scope (Just (VInts i j)) (VApp c p [VInt k])
| p == (cPredef,cInts) = do | p == (cPredef,cInts) = do
return (VCInts (Just (maybe k (max k) i)) j) return (VInts (Just (maybe k (max k) i)) j)
supertype scope Nothing (VRecType ltys) = do supertype scope Nothing (VRecType ltys) = do
lctrs <- mapM (\(l,ty) -> supertype scope Nothing ty >>= \ctr -> return (l,False,ctr)) ltys lctrs <- mapM (\(l,o,ty) -> supertype scope Nothing ty >>= \ctr -> return (l,False,ctr)) ltys
return (VCRecType lctrs) return (VRecType lctrs)
supertype scope (Just (VCRecType lctrs)) (VRecType ltys) = do supertype scope (Just (VRecType lctrs1)) (VRecType lctrs2) = do
lctrs <- foldM (\lctrs (l,o,ctr) -> intersect l o ctr lctrs ltys) [] lctrs lctrs <- foldM (\lctrs (l,o,ctr) -> intersect l o ctr lctrs lctrs2) [] lctrs1
return (VCRecType lctrs) return (VRecType lctrs)
where where
intersect l o ctr lctrs [] = return lctrs intersect l o1 ctr1 lctrs [] = return lctrs
intersect l o ctr lctrs ((l',ty):ltys2) intersect l o1 ctr1 lctrs ((l',o2,ctr2):lctrs2)
| l == l' = do ctr <- supertype scope (Just ctr) ty | l == l' = do ctr <- supertype scope (Just ctr1) ctr2
return ((l,o,ctr):lctrs) return ((l,o1 && o2,ctr):lctrs)
| otherwise = do intersect l o ctr lctrs ltys2 | otherwise = do intersect l o1 ctr1 lctrs lctrs2
supertype scope (Just (VTable a1 r1)) (VTable a2 r2) = do
a <- subtype scope (Just a1) a2
r <- supertype scope (Just r1) r2
return (VTable a r)
supertype scope Nothing ty = return ty supertype scope Nothing ty = return ty
supertype scope (Just ctr) ty = do supertype scope (Just ctr) ty = do
unify scope ctr ty unify scope ctr ty
@@ -974,8 +983,8 @@ unify scope (VGen i vs1) (VGen j vs2)
unify scope (VProd b x d cod) (VProd b' x' d' cod') unify scope (VProd b x d cod) (VProd b' x' d' cod')
| b == b' = do | b == b' = do
unify scope d d' unify scope d d'
cod <- evalCodomain scope x cod cod <- evalCodomain x (VGen (length scope) []) cod
cod' <- evalCodomain scope x' cod' cod' <- evalCodomain x' (VGen (length scope) []) cod'
unify scope cod cod' unify scope cod cod'
unify scope (VTable p1 res1) (VTable p2 res2) = do unify scope (VTable p1 res1) (VTable p2 res2) = do
unify scope p2 p1 unify scope p2 p1
@@ -992,8 +1001,8 @@ unify scope VEmpty VEmpty = return ()
unify scope v1 v2 = do unify scope v1 v2 = do
t1 <- value2termM False (scopeVars scope) v1 t1 <- value2termM False (scopeVars scope) v1
t2 <- value2termM False (scopeVars scope) v2 t2 <- value2termM False (scopeVars scope) v2
evalError ("Cannot unify terms:" <+> (ppTerm Unqualified 0 t1 $$ evalError ("Cannot unify:" <+> show t1 $$
ppTerm Unqualified 0 t2)) " with:" <+> show t2)
-- | Invariant: tv1 is a flexible type variable -- | Invariant: tv1 is a flexible type variable
@@ -1037,7 +1046,7 @@ occursCheck scope' i0 scope v =
check (m+1) (n+1) (eval g ((x,VGen n []):env) c t []) check (m+1) (n+1) (eval g ((x,VGen n []):env) c t [])
_ -> check m n ty2 _ -> check m n ty2
check m n (VRecType as) = check m n (VRecType as) =
mapM_ (\(lbl,v) -> check m n v) as mapM_ (\(_,_,v) -> check m n v) as
check m n (VR as) = check m n (VR as) =
mapM_ (\(lbl,v) -> check m n v) as mapM_ (\(lbl,v) -> check m n v) as
check m n (VP v l vs) = check m n (VP v l vs) =
@@ -1070,6 +1079,7 @@ occursCheck scope' i0 scope v =
check m n v >> mapM_ (\(v1,v2) -> check m n v1 >> check m n v2) vs check m n v >> mapM_ (\(v1,v2) -> check m n v1 >> check m n v2) vs
check m n (VStrs vs) = check m n (VStrs vs) =
mapM_ (check m n) vs mapM_ (check m n) vs
check m n (VInts _ _) = return ()
----------------------------------------------------------------------- -----------------------------------------------------------------------
-- Instantiation and quantification -- Instantiation and quantification
@@ -1101,7 +1111,7 @@ skolemise scope ty@(VMeta i vs) = do
skolemise scope (apply g ty vs) skolemise scope (apply g ty vs)
skolemise scope (VProd Implicit x ty1 ty2) = do skolemise scope (VProd Implicit x ty1 ty2) = do
let v = newVar scope let v = newVar scope
ty2 <- evalCodomain scope x ty2 ty2 <- evalCodomain x (VGen (length scope) []) ty2
(scope,f,ty2) <- skolemise ((v,ty1):scope) ty2 (scope,f,ty2) <- skolemise ((v,ty1):scope) ty2
return (scope,Abs Implicit v . f,ty2) return (scope,Abs Implicit v . f,ty2)
skolemise scope ty = do skolemise scope ty = do
@@ -1144,7 +1154,7 @@ quantify scope t tvs ty = do
v2 -> do (xs,v2) <- check m (n+1) xs v2 v2 -> do (xs,v2) <- check m (n+1) xs v2
return (x:xs,VProd bt x v1 v2) return (x:xs,VProd bt x v1 v2)
check m n xs (VRecType as) = do check m n xs (VRecType as) = do
(xs,as) <- mapAccumM (\xs (l,v) -> check m n xs v >>= \(xs,v) -> return (xs,(l,v))) xs as (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)
check m n xs (VR as) = do 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 (xs,as) <- mapAccumM (\xs (lbl,tnk) -> check m n xs tnk >>= \(xs,tnk) -> return (xs,(lbl,tnk))) xs as
@@ -1251,7 +1261,7 @@ getMetaVars sc_tys = foldM (\acc (scope,ty) -> go acc ty) [] sc_tys
go acc (VGen i args) = foldM go acc args go acc (VGen i args) = foldM go acc args
go acc (VSort s) = return acc go acc (VSort s) = return acc
go acc (VInt _) = return acc go acc (VInt _) = return acc
go acc (VRecType as) = foldM (\acc (lbl,v) -> go acc v) acc as go acc (VRecType vs) = foldM (\acc (lbl,_,v) -> go acc v) acc vs
go acc (VClosure _ _ _) = return acc go acc (VClosure _ _ _) = return acc
go acc (VProd b x v1 v2) = go acc v2 >>= \acc -> go acc v1 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 go acc (VTable v1 v2) = go acc v2 >>= \acc -> go acc v1
@@ -1265,8 +1275,7 @@ getMetaVars sc_tys = foldM (\acc (scope,ty) -> go acc ty) [] sc_tys
_ -> return acc _ -> return acc
go acc (VApp c f args) = foldM go acc args go acc (VApp c f args) = foldM go acc args
go acc (VFV c vs) = foldM go acc (unvariants vs) go acc (VFV c vs) = foldM go acc (unvariants vs)
go acc (VCRecType vs) = foldM (\acc (lbl,b,v) -> go acc v) acc vs go acc (VInts _ _) = return acc
go acc (VCInts _ _) = return acc
go acc v = unimplemented ("go "++show (ppValue Unqualified 5 v)) go acc v = unimplemented ("go "++show (ppValue Unqualified 5 v))
-- | Eliminate any substitutions in a term -- | Eliminate any substitutions in a term