mirror of
https://github.com/GrammaticalFramework/gf-core.git
synced 2026-04-09 04:59:31 -06:00
fix quantification
This commit is contained in:
Krasimir Angelov
@@ -5,7 +5,7 @@ module GF.Compile.Compute.Concrete2
|
||||
runEvalM, stdPredef, globals, pdArity,
|
||||
normalForm, normalFlatForm,
|
||||
eval, apply, value2term, value2termM, patternMatch, vtableSelect,
|
||||
newBinding, newResiduation, getMeta, setMeta, MetaState(..), variants, try,
|
||||
newResiduation, getMeta, setMeta, MetaState(..), variants, try,
|
||||
evalError, evalWarn, ppValue, Choice, unit, split, split4, mapC, mapCM) where
|
||||
|
||||
import Prelude hiding ((<>)) -- GHC 8.4.1 clash with Text.PrettyPrint
|
||||
@@ -437,7 +437,7 @@ value2term g xs v = do
|
||||
|
||||
type Constraint = Value
|
||||
data MetaState
|
||||
= Bound Int Value
|
||||
= Bound Scope Value
|
||||
| Narrowing Type
|
||||
| Residuation Scope (Maybe Constraint)
|
||||
data State
|
||||
@@ -517,11 +517,6 @@ try f xs msg = EvalM (\g k state r msgs ->
|
||||
Fail msg msgs -> Fail msg msgs
|
||||
Success r msgs -> continue g k res r msgs
|
||||
|
||||
newBinding :: Value -> EvalM MetaId
|
||||
newBinding v = EvalM (\g k (State choices metas) r msgs ->
|
||||
let meta_id = Map.size metas+1
|
||||
in k meta_id (State choices (Map.insert meta_id (Bound 0 v) metas)) r msgs)
|
||||
|
||||
newResiduation :: Scope -> EvalM MetaId
|
||||
newResiduation scope = EvalM (\g k (State choices metas) r msgs ->
|
||||
let meta_id = Map.size metas+1
|
||||
@@ -544,8 +539,8 @@ value2termM flat xs (VApp q vs) =
|
||||
value2termM flat xs (VMeta i vs) = do
|
||||
mv <- getMeta i
|
||||
case mv of
|
||||
Bound _ v -> do g <- globals
|
||||
value2termM flat xs (apply g v vs)
|
||||
Bound scope v -> do g <- globals
|
||||
value2termM flat (map fst scope) (apply g v vs)
|
||||
Residuation _ mb_ctr ->
|
||||
case mb_ctr of
|
||||
Just ctr -> do g <- globals
|
||||
@@ -640,6 +635,9 @@ value2termM flat xs (VStrs vs) = do
|
||||
ts <- mapM (value2termM flat xs) vs
|
||||
return (Strs ts)
|
||||
value2termM flat xs (VError msg) = evalError msg
|
||||
value2termM flat xs (VCRecType lbls) = do
|
||||
lbls <- mapM (\(lbl,_,v) -> fmap ((,) lbl) (value2termM flat xs v)) lbls
|
||||
return (RecType lbls)
|
||||
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))
|
||||
@@ -690,6 +688,7 @@ ppValue q d (VAlts e xs) = prec d 4 ("pre" <+> braces (ppValue q 0 e <> ';' <+>
|
||||
ppValue q d (VStrs _) = pp "VStrs"
|
||||
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 (VCRecType ass) = pp "VCRecType"
|
||||
ppValue q d (VCInts Nothing Nothing) = prec d 4 (pp "Ints ?")
|
||||
ppValue q d (VCInts (Just min) Nothing) = prec d 4 (pp "Ints" <+> brackets (pp min <> ".."))
|
||||
ppValue q d (VCInts Nothing (Just max)) = prec d 4 (pp "Ints" <+> brackets (".." <> pp max))
|
||||
|
||||
@@ -487,48 +487,6 @@ reapply2 scope fun fun_ty ((arg,arg_v,arg_ty):args) = do -- Explicit arg (fallth
|
||||
res_ty -> return res_ty
|
||||
reapply2 scope (App fun arg) res_ty args
|
||||
|
||||
{-tcApp scope c t0 t@(App fun (ImplArg arg)) = do -- APP1
|
||||
let (c1,c2,c3,c4) = split4 c
|
||||
(fun,fun_ty) <- tcApp scope c1 t0 fun
|
||||
(bt, x, arg_ty, res_ty) <- unifyFun scope fun_ty
|
||||
if (bt == Implicit)
|
||||
then return ()
|
||||
else evalError (ppTerm Unqualified 0 t <+> "is an implicit argument application, but no implicit argument is expected")
|
||||
(arg,_) <- tcRho scope c2 arg (Just arg_ty)
|
||||
res_ty <- case res_ty of
|
||||
VClosure res_env res_c res_ty -> do g <- globals
|
||||
return (eval g ((x,eval g (scopeEnv scope) c3 arg []):res_env) res_c res_ty [])
|
||||
res_ty -> return res_ty
|
||||
return (App fun (ImplArg arg), res_ty)
|
||||
tcApp scope c t0 (App fun arg) = do -- APP2
|
||||
let (c1,c2,c3,c4) = split4 c
|
||||
(fun,fun_ty) <- tcApp scope c1 t0 fun
|
||||
(fun,fun_ty) <- instantiate scope fun fun_ty
|
||||
(_, x, arg_ty, res_ty) <- unifyFun scope fun_ty
|
||||
(arg,_) <- tcRho scope c2 arg (Just arg_ty)
|
||||
g <- globals
|
||||
let res_ty' = foo g (x,eval g (scopeEnv scope) c3 arg []) res_ty
|
||||
return (App fun arg, res_ty')
|
||||
where
|
||||
foo g arg (VClosure env c res_ty) = eval g (arg:env) c res_ty []
|
||||
foo g arg (VFV c vs) = VFV c (map (foo g arg) vs)
|
||||
foo g arg res_ty = res_ty
|
||||
tcApp scope c t0 (Q id) = getOverloads scope c t0 id -- VAR (global)
|
||||
tcApp scope c t0 (QC id) = getOverloads scope c t0 id -- VAR (global)
|
||||
tcApp scope c t0 t = tcRho scope c t Nothing
|
||||
-}
|
||||
getOverloads :: Scope -> Choice -> Term -> QIdent -> EvalM (Term,Rho)
|
||||
getOverloads scope c t q = do
|
||||
g@(Gl gr _) <- globals
|
||||
case lookupOverloadTypes gr q of
|
||||
Bad msg -> evalError (pp msg)
|
||||
Ok [(t,ty)] -> return (t, eval g [] c ty [])
|
||||
Ok ttys -> do let (c1,c2,c3,c4) = split4 c
|
||||
vs = mapC (\c (t,ty) -> eval g [] c t []) c1 ttys
|
||||
vtys = mapC (\c (t,ty) -> eval g [] c ty []) c2 ttys
|
||||
i <- newBinding (VFV c3 vs)
|
||||
return (Meta i, VFV c3 vtys)
|
||||
|
||||
tcPatt scope c PW ty0 =
|
||||
return scope
|
||||
tcPatt scope c (PV x) ty0 =
|
||||
@@ -669,9 +627,9 @@ subsCheckRho scope t (VMeta i vs1) (VMeta j vs2)
|
||||
g <- globals
|
||||
subsCheckRho scope t (VMeta i vs1) (apply g v2 vs2)
|
||||
Residuation scope2 _
|
||||
| m > n -> do setMeta i (Bound m (VMeta j vs2))
|
||||
| m > n -> do setMeta i (Bound scope1 (VMeta j vs2))
|
||||
return t
|
||||
| otherwise -> do setMeta j (Bound n (VMeta i vs2))
|
||||
| otherwise -> do setMeta j (Bound scope2 (VMeta i vs2))
|
||||
return t
|
||||
where
|
||||
m = length scope1
|
||||
@@ -895,8 +853,8 @@ unify scope (VMeta i vs1) (VMeta j vs2)
|
||||
g <- globals
|
||||
unify scope (VMeta i vs1) (apply g v2 vs2)
|
||||
Residuation scope2 _
|
||||
| m > n -> setMeta i (Bound m (VMeta j vs2))
|
||||
| otherwise -> setMeta j (Bound n (VMeta i vs2))
|
||||
| m > n -> setMeta i (Bound scope1 (VMeta j vs2))
|
||||
| otherwise -> setMeta j (Bound scope2 (VMeta i vs2))
|
||||
where
|
||||
m = length scope1
|
||||
n = length scope2
|
||||
@@ -937,7 +895,7 @@ unifyVar scope metaid vs ty2 = do -- Check whether i is bound
|
||||
Bound _ ty1 -> do g <- globals
|
||||
unify scope (apply g ty1 vs) ty2
|
||||
Residuation scope' _ -> do occursCheck scope' metaid scope ty2
|
||||
setMeta metaid (Bound (length scope') ty2)
|
||||
setMeta metaid (Bound scope' ty2)
|
||||
|
||||
occursCheck scope' i0 scope v =
|
||||
let m = length scope'
|
||||
@@ -1047,11 +1005,11 @@ quantify scope t tvs ty = do
|
||||
n = length scope
|
||||
(used_bndrs,ty) <- check m n [] ty
|
||||
let new_bndrs = take m (allBinders \\ used_bndrs)
|
||||
mapM_ bind (zip3 [0..] tvs new_bndrs)
|
||||
mapM_ (bind ([(var,VSort cType)|var <- new_bndrs]++scope)) (zip3 [0..] tvs new_bndrs)
|
||||
let ty' = foldr (\ty -> VProd Implicit ty vtypeType) ty new_bndrs
|
||||
return (foldr (Abs Implicit) t new_bndrs,ty')
|
||||
where
|
||||
bind (i, meta_id, name) = setMeta meta_id (Bound (length scope) (VGen i []))
|
||||
bind scope (i, meta_id, name) = setMeta meta_id (Bound scope (VGen i []))
|
||||
|
||||
check m n xs (VApp f vs) = do
|
||||
(xs,vs) <- mapAccumM (check m n) xs vs
|
||||
|
||||
Reference in New Issue
Block a user