Skip to content

Commit 084ffa1

Browse files
krangelovkrangelov
committed
fix quantification
1 parent 3444816 commit 084ffa1

File tree

2 files changed

+15
-58
lines changed

2 files changed

+15
-58
lines changed

‎src/compiler/api/GF/Compile/Compute/Concrete2.hs‎

Lines changed: 8 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@ module GF.Compile.Compute.Concrete2
55
runEvalM, stdPredef, globals, pdArity,
66
normalForm, normalFlatForm,
77
eval, apply, value2term, value2termM, patternMatch, vtableSelect,
8-
newBinding, newResiduation, getMeta, setMeta, MetaState(..), variants, try,
8+
newResiduation, getMeta, setMeta, MetaState(..), variants, try,
99
evalError, evalWarn, ppValue, Choice, unit, split, split4, mapC, mapCM) where
1010

1111
import Prelude hiding ((<>)) -- GHC 8.4.1 clash with Text.PrettyPrint
@@ -437,7 +437,7 @@ value2term g xs v = do
437437

438438
type Constraint = Value
439439
data MetaState
440-
= Bound Int Value
440+
= Bound Scope Value
441441
| Narrowing Type
442442
| Residuation Scope (Maybe Constraint)
443443
data State
@@ -517,11 +517,6 @@ try f xs msg = EvalM (\g k state r msgs ->
517517
Fail msg msgs -> Fail msg msgs
518518
Success r msgs -> continue g k res r msgs
519519

520-
newBinding :: Value -> EvalM MetaId
521-
newBinding v = EvalM (\g k (State choices metas) r msgs ->
522-
let meta_id = Map.size metas+1
523-
in k meta_id (State choices (Map.insert meta_id (Bound 0 v) metas)) r msgs)
524-
525520
newResiduation :: Scope -> EvalM MetaId
526521
newResiduation scope = EvalM (\g k (State choices metas) r msgs ->
527522
let meta_id = Map.size metas+1
@@ -544,8 +539,8 @@ value2termM flat xs (VApp q vs) =
544539
value2termM flat xs (VMeta i vs) = do
545540
mv <- getMeta i
546541
case mv of
547-
Bound _ v -> do g <- globals
548-
value2termM flat xs (apply g v vs)
542+
Bound scope v -> do g <- globals
543+
value2termM flat (map fst scope) (apply g v vs)
549544
Residuation _ mb_ctr ->
550545
case mb_ctr of
551546
Just ctr -> do g <- globals
@@ -640,6 +635,9 @@ value2termM flat xs (VStrs vs) = do
640635
ts <- mapM (value2termM flat xs) vs
641636
return (Strs ts)
642637
value2termM flat xs (VError msg) = evalError msg
638+
value2termM flat xs (VCRecType lbls) = do
639+
lbls <- mapM (\(lbl,_,v) -> fmap ((,) lbl) (value2termM flat xs v)) lbls
640+
return (RecType lbls)
643641
value2termM flat xs (VCInts Nothing Nothing) = return (App (QC (cPredef,cInts)) (Meta 0))
644642
value2termM flat xs (VCInts (Just min) Nothing) = return (App (QC (cPredef,cInts)) (EInt min))
645643
value2termM flat xs (VCInts _ (Just max)) = return (App (QC (cPredef,cInts)) (EInt max))
@@ -690,6 +688,7 @@ ppValue q d (VAlts e xs) = prec d 4 ("pre" <+> braces (ppValue q 0 e <> ';' <+>
690688
ppValue q d (VStrs _) = pp "VStrs"
691689
ppValue q d (VSymCat i r rs) = pp '<' <> pp i <> pp ',' <> pp r <> pp '>'
692690
ppValue q d (VError msg) = prec d 4 (pp "error" <+> ppTerm q 5 (K (show msg)))
691+
ppValue q d (VCRecType ass) = pp "VCRecType"
693692
ppValue q d (VCInts Nothing Nothing) = prec d 4 (pp "Ints ?")
694693
ppValue q d (VCInts (Just min) Nothing) = prec d 4 (pp "Ints" <+> brackets (pp min <> ".."))
695694
ppValue q d (VCInts Nothing (Just max)) = prec d 4 (pp "Ints" <+> brackets (".." <> pp max))

‎src/compiler/api/GF/Compile/TypeCheck/ConcreteNew.hs‎

Lines changed: 7 additions & 49 deletions
Original file line numberDiff line numberDiff line change
@@ -487,48 +487,6 @@ reapply2 scope fun fun_ty ((arg,arg_v,arg_ty):args) = do -- Explicit arg (fallth
487487
res_ty -> return res_ty
488488
reapply2 scope (App fun arg) res_ty args
489489

490-
{-tcApp scope c t0 t@(App fun (ImplArg arg)) = do -- APP1
491-
let (c1,c2,c3,c4) = split4 c
492-
(fun,fun_ty) <- tcApp scope c1 t0 fun
493-
(bt, x, arg_ty, res_ty) <- unifyFun scope fun_ty
494-
if (bt == Implicit)
495-
then return ()
496-
else evalError (ppTerm Unqualified 0 t <+> "is an implicit argument application, but no implicit argument is expected")
497-
(arg,_) <- tcRho scope c2 arg (Just arg_ty)
498-
res_ty <- case res_ty of
499-
VClosure res_env res_c res_ty -> do g <- globals
500-
return (eval g ((x,eval g (scopeEnv scope) c3 arg []):res_env) res_c res_ty [])
501-
res_ty -> return res_ty
502-
return (App fun (ImplArg arg), res_ty)
503-
tcApp scope c t0 (App fun arg) = do -- APP2
504-
let (c1,c2,c3,c4) = split4 c
505-
(fun,fun_ty) <- tcApp scope c1 t0 fun
506-
(fun,fun_ty) <- instantiate scope fun fun_ty
507-
(_, x, arg_ty, res_ty) <- unifyFun scope fun_ty
508-
(arg,_) <- tcRho scope c2 arg (Just arg_ty)
509-
g <- globals
510-
let res_ty' = foo g (x,eval g (scopeEnv scope) c3 arg []) res_ty
511-
return (App fun arg, res_ty')
512-
where
513-
foo g arg (VClosure env c res_ty) = eval g (arg:env) c res_ty []
514-
foo g arg (VFV c vs) = VFV c (map (foo g arg) vs)
515-
foo g arg res_ty = res_ty
516-
tcApp scope c t0 (Q id) = getOverloads scope c t0 id -- VAR (global)
517-
tcApp scope c t0 (QC id) = getOverloads scope c t0 id -- VAR (global)
518-
tcApp scope c t0 t = tcRho scope c t Nothing
519-
-}
520-
getOverloads :: Scope -> Choice -> Term -> QIdent -> EvalM (Term,Rho)
521-
getOverloads scope c t q = do
522-
g@(Gl gr _) <- globals
523-
case lookupOverloadTypes gr q of
524-
Bad msg -> evalError (pp msg)
525-
Ok [(t,ty)] -> return (t, eval g [] c ty [])
526-
Ok ttys -> do let (c1,c2,c3,c4) = split4 c
527-
vs = mapC (\c (t,ty) -> eval g [] c t []) c1 ttys
528-
vtys = mapC (\c (t,ty) -> eval g [] c ty []) c2 ttys
529-
i <- newBinding (VFV c3 vs)
530-
return (Meta i, VFV c3 vtys)
531-
532490
tcPatt scope c PW ty0 =
533491
return scope
534492
tcPatt scope c (PV x) ty0 =
@@ -669,9 +627,9 @@ subsCheckRho scope t (VMeta i vs1) (VMeta j vs2)
669627
g <- globals
670628
subsCheckRho scope t (VMeta i vs1) (apply g v2 vs2)
671629
Residuation scope2 _
672-
| m > n -> do setMeta i (Bound m (VMeta j vs2))
630+
| m > n -> do setMeta i (Bound scope1 (VMeta j vs2))
673631
return t
674-
| otherwise -> do setMeta j (Bound n (VMeta i vs2))
632+
| otherwise -> do setMeta j (Bound scope2 (VMeta i vs2))
675633
return t
676634
where
677635
m = length scope1
@@ -895,8 +853,8 @@ unify scope (VMeta i vs1) (VMeta j vs2)
895853
g <- globals
896854
unify scope (VMeta i vs1) (apply g v2 vs2)
897855
Residuation scope2 _
898-
| m > n -> setMeta i (Bound m (VMeta j vs2))
899-
| otherwise -> setMeta j (Bound n (VMeta i vs2))
856+
| m > n -> setMeta i (Bound scope1 (VMeta j vs2))
857+
| otherwise -> setMeta j (Bound scope2 (VMeta i vs2))
900858
where
901859
m = length scope1
902860
n = length scope2
@@ -937,7 +895,7 @@ unifyVar scope metaid vs ty2 = do -- Check whether i is bound
937895
Bound _ ty1 -> do g <- globals
938896
unify scope (apply g ty1 vs) ty2
939897
Residuation scope' _ -> do occursCheck scope' metaid scope ty2
940-
setMeta metaid (Bound (length scope') ty2)
898+
setMeta metaid (Bound scope' ty2)
941899

942900
occursCheck scope' i0 scope v =
943901
let m = length scope'
@@ -1047,11 +1005,11 @@ quantify scope t tvs ty = do
10471005
n = length scope
10481006
(used_bndrs,ty) <- check m n [] ty
10491007
let new_bndrs = take m (allBinders \\ used_bndrs)
1050-
mapM_ bind (zip3 [0..] tvs new_bndrs)
1008+
mapM_ (bind ([(var,VSort cType)|var <- new_bndrs]++scope)) (zip3 [0..] tvs new_bndrs)
10511009
let ty' = foldr (\ty -> VProd Implicit ty vtypeType) ty new_bndrs
10521010
return (foldr (Abs Implicit) t new_bndrs,ty')
10531011
where
1054-
bind (i, meta_id, name) = setMeta meta_id (Bound (length scope) (VGen i []))
1012+
bind scope (i, meta_id, name) = setMeta meta_id (Bound scope (VGen i []))
10551013

10561014
check m n xs (VApp f vs) = do
10571015
(xs,vs) <- mapAccumM (check m n) xs vs

0 commit comments

Comments
 (0)