msyds/gf-core
1
0
Fork 0
forked from GitHub/gf-core
Code Pull Requests Activity

Merge branch 'majestic' of github.com:krangelov/gf-core into majestic

Browse Source
This commit is contained in:
Krasimir Angelov
2025-08-21 14:25:28 +02:00
parent 8ba7d7ba48 cbac8b4fd2
commit 272fc4bac1
9 changed files with 645 additions and 332 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 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 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 tysts0 <- lookupOverload gr (fst sm,c) -- check against inherited ones too
tysts1 <- mapM (uncurry $ flip (checkLType g)) tysts1 <- sequence
[(mkFunType args val,tr) | (args,(val,tr)) <- tysts0] [checkLType g tr (mkFunType args val) | (args,(val,tr)) <- tysts0]
--- this can only be a partial guarantee, since matching --- this can only be a partial guarantee, since matching
--- with value type is only possible if expected type is given --- with value type is only possible if expected type is given
checkUniq $ --checkUniq $
sort [let (xs,t) = typeFormCnc x in t : map (\(b,x,t) -> t) xs | (_,x) <- tysts1] -- 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']) update sm c (ResOverload os [(y,x) | (x,y) <- tysts'])
ResParam (Just (L loc pcs)) _ -> do ResParam (Just (L loc pcs)) _ -> do
src/compiler/api/GF/Compile/Compute/Concrete2.hs
+103 -43
View File
@@ -3,13 +3,13 @@
module GF.Compile.Compute.Concrete2 module GF.Compile.Compute.Concrete2
(Env, Scope, Value(..), Variants(..), OptionInfo(..), ChoiceMap, cleanOptions, (Env, Scope, Value(..), Variants(..), OptionInfo(..), ChoiceMap, cleanOptions,
ConstValue(..), ConstVariants(..), Globals(..), PredefTable, EvalM, ConstValue(..), ConstVariants(..), Globals(..), PredefTable, EvalM,
mapVariants, unvariants, variants2consts, consts2variants, mapVariants, mapVariantsC, unvariants, variants2consts, consts2variants,
runEvalM, runEvalMWithOpts, stdPredef, globals, withState, runEvalM, runEvalMWithOpts, stdPredef, globals,
PredefImpl, Predef(..), ($\), PredefImpl, Predef(..), ($\),
pdCanonicalArgs, pdArity, pdCanonicalArgs, pdArity,
normalForm, normalFlatForm, normalForm, normalFlatForm,
eval, apply, value2term, value2termM, bubble, patternMatch, vtableSelect, State(..), eval, apply, value2term, value2termM, value2int, value2float, bubble, patternMatch, vtableSelect, State(..),
newResiduation, getMeta, setMeta, MetaState(..), variants, try, newResiduation, checkpoint, getMeta, setMeta, MetaState(..), variants, try,
evalError, evalWarn, ppValue, Choice(..), unit, poison, split, split3, split4, mapC, mapCM) where evalError, evalWarn, ppValue, Choice(..), unit, poison, split, split3, split4, mapC, mapCM) where
import Prelude hiding ((<>)) -- GHC 8.4.1 clash with Text.PrettyPrint import Prelude hiding ((<>)) -- GHC 8.4.1 clash with Text.PrettyPrint
@@ -24,6 +24,7 @@ import GF.Grammar.Predef
import GF.Grammar.Printer hiding (ppValue) import GF.Grammar.Printer hiding (ppValue)
import GF.Grammar.Lockfield(lockLabel) import GF.Grammar.Lockfield(lockLabel)
import GF.Text.Pretty hiding (empty) import GF.Text.Pretty hiding (empty)
import qualified GF.Text.Pretty as PP
import Control.Monad import Control.Monad
import Control.Applicative hiding (Const) import Control.Applicative hiding (Const)
import qualified Control.Applicative as A import qualified Control.Applicative as A
@@ -65,7 +66,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, Bool, Value)] | VRecType [(Label, Bool, Value)] Bool
| VR [(Label, Value)] | VR [(Label, Value)]
| VP Value Label [Value] | VP Value Label [Value]
| VExtR Value Value | VExtR Value Value
@@ -89,16 +90,20 @@ 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
| VInts (Maybe Integer) (Maybe Integer) | VInts Integer Bool
data Variants data Variants
= VarFree [Value] = VarFree [Value]
| VarOpts Value [(Value, Value)] | VarOpts Value [(Maybe Value, Value)]
mapVariants :: (Value -> Value) -> Variants -> Variants mapVariants :: (Value -> Value) -> Variants -> Variants
mapVariants f (VarFree vs) = VarFree (f <$> vs) mapVariants f (VarFree vs) = VarFree (f <$> vs)
mapVariants f (VarOpts n cs) = VarOpts n (second f <$> cs) mapVariants f (VarOpts n cs) = VarOpts n (second f <$> cs)
mapVariantsC :: (Choice -> Value -> Value) -> Choice -> Variants -> Variants
mapVariantsC f c (VarFree vs) = VarFree (mapC f c vs)
mapVariantsC f c (VarOpts n cs) = VarOpts n (mapC (\c (x,y) -> (x,f c y)) c cs)
unvariants :: Variants -> [Value] unvariants :: Variants -> [Value]
unvariants (VarFree vs) = vs unvariants (VarFree vs) = vs
unvariants (VarOpts n cs) = snd <$> cs unvariants (VarOpts n cs) = snd <$> cs
@@ -106,7 +111,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 (\(l,_,ty) -> isCanonicalForm flat ty) 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
@@ -133,7 +138,7 @@ data ConstValue a
data ConstVariants a data ConstVariants a
= ConstFree [ConstValue a] = ConstFree [ConstValue a]
| ConstOpts Value [(Value, ConstValue a)] | ConstOpts Value [(Maybe Value, ConstValue a)]
mapConstVs :: (ConstValue a -> ConstValue b) -> ConstVariants a -> ConstVariants b mapConstVs :: (ConstValue a -> ConstValue b) -> ConstVariants a -> ConstVariants b
mapConstVs f (ConstFree vs) = ConstFree (f <$> vs) mapConstVs f (ConstFree vs) = ConstFree (f <$> vs)
@@ -200,7 +205,7 @@ eval g env s (Prod b x t1 t2)[]
| otherwise = let (s1,s2) = split s | 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, 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 (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 +219,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,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 (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) []
@@ -332,7 +337,8 @@ eval g env c t@(Opts n cs) vs = if null cs
vn = eval g env c1 n [] vn = eval g env c1 n []
vcs = mapC evalOpt c cs vcs = mapC evalOpt c cs
in VFV c3 (VarOpts vn vcs) in VFV c3 (VarOpts vn vcs)
where evalOpt c' (l,t) = let (c1,c2) = split c' in (eval g env c1 l [], eval g env c2 t vs) where evalOpt c' (Just l, t) = let (c1,c2) = split c' in (Just (eval g env c1 l []), eval g env c2 t vs)
evalOpt c' (Nothing,t) = let (c1,c2) = split c' in (Nothing, eval g env c2 t vs)
eval g env c t vs = VError ("Cannot reduce term" <+> pp t) eval g env c t vs = VError ("Cannot reduce term" <+> pp t)
evalPredef :: Globals -> Choice -> Ident -> [Value] -> Value evalPredef :: Globals -> Choice -> Ident -> [Value] -> Value
@@ -348,7 +354,7 @@ evalPredef g@(Gl gr pds) c n args =
stdPredef :: Globals -> PredefTable stdPredef :: Globals -> PredefTable
stdPredef g = Map.fromList 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)) ,(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))) ,(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))) ,(cDrop, pdArity 2 $\ \g c [v1,v2] -> fmap string2value (liftA2 genericDrop (value2int g v1) (value2string g v2)))
@@ -392,9 +398,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 v@(VRecType lbls) = bubble v@(VRecType lbls ext) =
let (union,lbls') = mapAccumL descendR Map.empty lbls 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 (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
@@ -414,18 +420,20 @@ bubble v = snd (bubble v)
bubble v@(VFV c (VarFree vs)) bubble v@(VFV c (VarFree vs))
| null vs = (Map.empty, v) | null vs = (Map.empty, v)
| otherwise = let (union,vs') = mapAccumL descend Map.empty vs | otherwise = let (union,vs') = mapAccumL descend Map.empty vs
in (Map.insert c (BubbleFree (length vs),1) union, addVariants (VFV c (VarFree vs')) union) in (Map.insert c (BubbleFree (length vs),1) union, VFV c (VarFree vs'))
bubble v@(VFV c (VarOpts n os)) bubble v@(VFV c (VarOpts n os))
| null os = (Map.empty, v) | null os = (Map.empty, v)
| otherwise = let (union,os') = mapAccumL (\acc (k,v) -> second (k,) $ descend acc v) Map.empty os | otherwise = let (union,os') = mapAccumL (\acc (k,v) -> second (k,) $ descend acc v) Map.empty os
in (Map.insert c (BubbleOpts n (fst <$> os),1) union, addVariants (VFV c (VarOpts n os')) union) in (Map.insert c (BubbleOpts n (map (\(l,t) -> fromMaybe t l) os),1) union, VFV c (VarOpts n os'))
bubble (VAlts v vs) = lift1L2 VAlts v vs bubble (VAlts v vs) = lift1L2 VAlts v vs
bubble (VStrs vs) = liftL VStrs vs bubble (VStrs vs) = liftL VStrs vs
bubble (VMarkup tag attrs vs) = bubble (VMarkup tag attrs vs) =
let (union1,attrs') = mapAccumL descend' Map.empty attrs let (union1,attrs') = mapAccumL descend' Map.empty attrs
(union2,vs') = mapAccumL descend union1 vs (union2,vs') = mapAccumL descend union1 vs
in (union2, VMarkup tag attrs' vs') in (union2, VMarkup tag attrs' vs')
bubble (VReset ctl mb_cv v id) = lift1 (\v -> VReset ctl mb_cv v id) v bubble (VReset ctl mb_cv v id) =
let (union,v') = bubble v
in (Map.empty,VReset ctl mb_cv v' id)
bubble (VSymCat d i0 vs) = bubble (VSymCat d i0 vs) =
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)
@@ -501,7 +509,7 @@ bubble v = snd (bubble v)
addVariant c (bvs,cnt) v addVariant c (bvs,cnt) v
| cnt > 1 = VFV c $ case bvs of | cnt > 1 = VFV c $ case bvs of
BubbleFree k -> VarFree (replicate k v) BubbleFree k -> VarFree (replicate k v)
BubbleOpts n os -> VarOpts n ((,v) <$> os) BubbleOpts n os -> VarOpts n (map (\l -> (Just l,v)) os)
| otherwise = v | otherwise = v
unitfy = fmap (\(n,_) -> (n,1)) unitfy = fmap (\(n,_) -> (n,1))
@@ -733,9 +741,6 @@ runEvalMWithOpts g cs (EvalM f) = Check $ \(es,ws) ->
where where
init = State cs Map.empty [] init = State cs Map.empty []
withState :: State -> EvalM a -> EvalM a
withState state (EvalM f) = EvalM $ \g k _ r ws -> f g k state r ws
reset :: EvalM a -> EvalM [a] reset :: EvalM a -> EvalM [a]
reset (EvalM f) = EvalM $ \g k state r ws -> reset (EvalM f) = EvalM $ \g k state r ws ->
case f g (\x state xs ws -> Success (x:xs) ws) state [] ws of case f g (\x state xs ws -> Success (x:xs) ws) state [] ws of
@@ -773,24 +778,36 @@ variants' c f xs = EvalM (\g k state@(State choices metas opts) r msgs ->
Fail msg msgs -> Fail msg msgs Fail msg msgs -> Fail msg msgs
Success ts msgs -> backtrack g (j+1) xs choices metas opts ts msgs Success ts msgs -> backtrack g (j+1) xs choices metas opts ts msgs
try :: (a -> EvalM b) -> ([(b,State)] -> EvalM b) -> [a] -> EvalM b try :: Int -> (a -> EvalM b) -> ([b] -> EvalM b) -> [a] -> EvalM b
try f select xs = EvalM (\g k state r msgs -> try sz f select xs = EvalM (\g k state r msgs ->
let (res,msgs') = backtrack g xs state [] msgs let (state',res,msgs') = backtrack sz g xs state [] msgs
in case select res of in case select res of
EvalM f' -> f' g k state r msgs') EvalM f' -> f' g k state' r msgs')
where where
backtrack g [] state res msgs = (res,msgs) backtrack sz g [] state res msgs = (state,res,msgs)
backtrack g (x:xs) state res msgs = backtrack sz g (x:xs) state res msgs =
case f x of case f x of
EvalM f -> case f g (\x state res msgs -> Success ((x,state):res) msgs) state res msgs of EvalM f -> case f g (\y state' (_,ys) msgs -> Success (cut sz state state',y:ys) msgs) state (state,res) msgs of
Fail msg _ -> backtrack g xs state res msgs Fail msg _ -> backtrack sz g xs state res msgs
Success res msgs -> backtrack g xs state res msgs Success (state,res) msgs -> backtrack sz g xs state res msgs
cut sz state state' = state'{metaVars=Map.mapWithKey select (metaVars state')}
where
select k ms
| k <= sz = ms
| otherwise = case Map.lookup k (metaVars state) of
Just ms -> ms
Nothing -> ms
newResiduation :: Scope -> EvalM MetaId newResiduation :: Scope -> EvalM MetaId
newResiduation scope = EvalM (\g k (State choices metas opts) r msgs -> newResiduation scope = EvalM (\g k (State choices metas opts) r msgs ->
let meta_id = Map.size metas+1 let meta_id = Map.size metas+1
in k meta_id (State choices (Map.insert meta_id (Residuation scope) metas) opts) r msgs) in k meta_id (State choices (Map.insert meta_id (Residuation scope) metas) opts) r msgs)
checkpoint :: EvalM Int
checkpoint = EvalM (\g k state r msgs ->
k (Map.size (metaVars state)) state r msgs)
getMeta :: MetaId -> EvalM MetaState getMeta :: MetaId -> EvalM MetaState
getMeta i = EvalM (\g k state r msgs -> getMeta i = EvalM (\g k state r msgs ->
case Map.lookup i (metaVars state) of case Map.lookup i (metaVars state) of
@@ -833,7 +850,7 @@ value2termM flat xs (VProd b x v1 v2) = do
t1 <- value2termM flat xs v1 t1 <- value2termM flat xs v1
t2 <- value2termM flat xs v2 t2 <- value2termM flat xs v2
return (Prod b x t1 t2) 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 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
@@ -908,7 +925,7 @@ value2termM flat xs (VFV i (VarOpts n os)) =
let j = fromMaybe 0 (Map.lookup i choices) let j = fromMaybe 0 (Map.lookup i choices)
in case os `maybeAt` j of in case os `maybeAt` j of
Just (l,t) -> case value2termM flat xs t of Just (l,t) -> case value2termM flat xs t of
EvalM f -> let oi = OptionInfo i n (fst <$> os) EvalM f -> let oi = OptionInfo i n (map (\(l,t) -> fromMaybe t l) os)
in f g k (State choices metas (oi:opts)) r msgs in f g k (State choices metas (oi:opts)) r msgs
Nothing -> Fail ("Index" <+> j <+> "out of bounds for option:" $$ ppValue Unqualified 0 n) msgs Nothing -> Fail ("Index" <+> j <+> "out of bounds for option:" $$ ppValue Unqualified 0 n) msgs
value2termM flat xs (VPatt min max p) = return (EPatt min max p) value2termM flat xs (VPatt min max p) = return (EPatt min max p)
@@ -941,11 +958,36 @@ value2termM flat xs (VReset ctl mb_cv v mb_qid) = do
case ts of case ts of
[t] -> return t [t] -> return t
ts -> return (Markup identW [] ts) ts -> return (Markup identW [] ts)
| ctl == cConcat' = do
ts <- case mb_cv of
Just (VInt n) -> return (genericTake n ts)
Nothing -> return ts
_ -> evalError (pp "[concat: .. | ..] requires an integer constant")
case ts of
[] -> mzero
[t] -> return t
ts -> return (Markup identW [] ts)
| ctl == cOne = | ctl == cOne =
case (ts,mb_cv) of case (ts,mb_cv) of
([] ,Nothing) -> mzero ([] ,Nothing) -> mzero
([] ,Just v) -> value2termM flat xs v ([] ,Just v) -> value2termM flat xs v
(t:ts,_) -> return t (t:ts,_) -> return t
| ctl == cSelect =
case mb_cv of
Just (VInt n) | n >= 0 -> select n ts'
| otherwise -> select (-n-1) (reverse ts')
where
ts' = sortBy compareKey ts
select _ [] = mzero
select 0 (t:ts) =
case t of
R rs -> case lookup (ident2label cp1) rs of
Just (_,t) -> return t
Nothing -> evalError (pp "Missing label p1")
_ -> evalError (pp "The term must be a record")
select n (t:ts) = select (n-1) ts
_ -> evalError (pp "[select: .. | ..] requires an integer constant")
| ctl == cDefault = | ctl == cDefault =
case (ts,mb_cv) of case (ts,mb_cv) of
([] ,Nothing) -> mzero ([] ,Nothing) -> mzero
@@ -962,15 +1004,23 @@ value2termM flat xs (VReset ctl mb_cv v mb_qid) = do
t <- listify mn cat ts t <- listify mn cat ts
return (App (App (QC (mn,identS ("Conj"++cat))) ct) t) return (App (App (QC (mn,identS ("Conj"++cat))) ct) t)
_ -> evalError (pp "[list: .. | ..] requires an argument") _ -> evalError (pp "[list: .. | ..] requires an argument")
| ctl == cLen =
case mb_cv of
Just cv -> do g <- globals
value2termM True xs (apply g cv [VInt (genericLength ts)])
Nothing -> return (EInt (genericLength ts))
| otherwise = evalError (pp "Operator" <+> pp ctl <+> pp "is not defined") | otherwise = evalError (pp "Operator" <+> pp ctl <+> pp "is not defined")
listify mn cat [t1,t2] = do return (App (App (QC (mn,identS ("Base"++cat))) t1) t2) listify mn cat [t1,t2] = do return (App (App (QC (mn,identS ("Base"++cat))) t1) t2)
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)
compareKey (R rs1) (R rs2) =
case (lookup (ident2label cp2) rs1, lookup (ident2label cp2) rs2) of
(Just (_,K s1), Just (_,K s2)) -> compare s1 s2
value2termM flat xs (VError msg) = evalError msg value2termM flat xs (VError msg) = evalError msg
value2termM flat xs (VInts Nothing Nothing) = return (App (Q (cPredef,cInts)) (Meta 0)) value2termM flat xs (VInts n _) = return (App (Q (cPredef,cInts)) (EInt n))
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 v = evalError ("value2termM" <+> ppValue Unqualified 5 v) value2termM flat xs v = evalError ("value2termM" <+> ppValue Unqualified 5 v)
@@ -986,6 +1036,7 @@ pattVars st (PSeq _ _ p1 _ _ p2) = pattVars (pattVars st p1) p2
pattVars st _ = st pattVars st _ = st
ppValue q d (VApp c f vs) = prec d 4 (hsep (ppQIdent q f : map (ppValue q 5) vs)) ppValue q d (VApp c f vs) = prec d 4 (hsep (ppQIdent q f : map (ppValue q 5) vs))
ppValue q d (VMeta i vs) = prec d 4 (hsep ((if i > 0 then pp "?" <> pp i else pp "?") : map (ppValue q 5) vs)) ppValue q d (VMeta i vs) = prec d 4 (hsep ((if i > 0 then pp "?" <> pp i else pp "?") : map (ppValue q 5) vs))
ppValue q d (VSusp i k vs) = prec d 4 (hsep (pp "#susp" : (if i > 0 then pp "?" <> pp i else pp "?") : map (ppValue q 5) vs)) ppValue q d (VSusp i k vs) = prec d 4 (hsep (pp "#susp" : (if i > 0 then pp "?" <> pp i else pp "?") : map (ppValue q 5) vs))
@@ -995,13 +1046,13 @@ ppValue q d (VProd bt x a b) =
if x == identW && bt == Explicit if x == identW && bt == Explicit
then prec d 0 (ppValue q 4 a <+> "->" <+> ppValue q 0 b) 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) 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 | q == Terse = case [cat | (l,_,_) <- xs, let (p,cat) = splitAt 5 (showIdent (label2ident l)), p == "lock_"] of
[cat] -> pp cat [cat] -> pp cat
_ -> doc _ -> doc
| otherwise = doc | otherwise = doc
where 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 (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"
@@ -1021,17 +1072,20 @@ 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 (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 (VGlue v1 v2) = prec d 2 (ppValue q 3 v1 <+> '+' <+> ppValue q 2 v2)
ppValue q d (VPatt _ _ _) = pp "VPatt" 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 (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 (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 (VStrs _) = pp "VStrs"
ppValue q d (VMarkup _ _ _) = pp "VMarkup" ppValue q d (VMarkup _ _ _) = pp "VMarkup"
ppValue q d (VReset ctl ct t _) = pp "[" <> pp ctl <>
maybe PP.empty (\v -> pp ':' <+> ppValue q 6 v) ct <>
pp "|" <> ppValue q 0 t <>
pp "]"
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 (VInts Nothing Nothing) = prec d 4 (pp "Ints ?") ppValue q d (VInts n ext)
ppValue q d (VInts (Just min) Nothing) = prec d 4 (pp "Ints" <+> brackets (pp min <> "..")) | ext = prec d 4 (pp "Ints" <+> brackets (pp n <> ".."))
ppValue q d (VInts Nothing (Just max)) = prec d 4 (pp "Ints" <+> brackets (".." <> pp max)) | otherwise = prec d 4 (pp "Ints" <+> pp n)
ppValue q d (VInts (Just min) (Just max)) = 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
@@ -1103,6 +1157,12 @@ value2int g (VInt n) = Const n
value2int g (VFV s vs) = CFV s (variants2consts (value2int g) vs) value2int g (VFV s vs) = CFV s (variants2consts (value2int g) vs)
value2int g _ = RunTime value2int g _ = RunTime
value2float g (VMeta i vs) = CSusp i (\v -> value2float g (apply g v vs))
value2float g (VSusp i k vs) = CSusp i (\v -> value2float g (apply g (k v) vs))
value2float g (VFlt f) = Const f
value2float g (VFV s vs) = CFV s (variants2consts (value2float g) vs)
value2float g _ = RunTime
newtype Choice = Choice { unchoice :: Integer } newtype Choice = Choice { unchoice :: Integer }
deriving (Eq,Ord,Pretty,Show) deriving (Eq,Ord,Pretty,Show)
src/compiler/api/GF/Compile/GeneratePMCFG.hs
+21 -4
View File
@@ -214,11 +214,28 @@ str2lin (VSymCat d r rs) = do (r, rs) <- compute r rs
str2lin (VSymVar d r) = return [SymVar d r] str2lin (VSymVar d r) = return [SymVar d r]
str2lin VEmpty = return [] str2lin VEmpty = return []
str2lin (VC v1 v2) = liftM2 (++) (str2lin v1) (str2lin v2) str2lin (VC v1 v2) = liftM2 (++) (str2lin v1) (str2lin v2)
str2lin (VAlts def alts) = do def <- str2lin def str2lin v0@(VAlts def alts)
alts <- forM alts $ \(v,VStrs vs) -> do = do def <- str2lin def
lin <- str2lin v alts <- forM alts $ \(v1,v2) -> do
return (lin,[s | VStr s <- vs]) lin <- str2lin v1
ss <- to_strs v2
return (lin,ss)
return [SymKP def alts] return [SymKP def alts]
where
to_strs (VStrs vs) = mapM to_str vs
to_strs (VPatt _ _ p) = from_patt p
to_strs v = fail
to_str (VStr s) = return s
to_str _ = fail
from_patt (PAlt p1 p2) = liftM2 (++) (from_patt p1) (from_patt p2)
from_patt (PSeq _ _ p1 _ _ p2) = liftM2 (liftM2 (++)) (from_patt p1) (from_patt p2)
from_patt (PString s) = return [s]
from_patt (PChars cs) = return (map (:[]) cs)
from_patt _ = fail
fail = evalError ("Complex patterns are not supported in:" $$ nest 2 (pp (showValue v0)))
str2lin v = do t <- value2term False [] v str2lin v = do t <- value2term False [] v
evalError ("the string:" <+> ppTerm Unqualified 0 t $$ evalError ("the string:" <+> ppTerm Unqualified 0 t $$
"cannot be evaluated at compile time.") "cannot be evaluated at compile time.")
src/compiler/api/GF/Compile/TypeCheck/Concrete.hs
+441 -226
View File
@@ -14,7 +14,7 @@ import GF.Compile.Compute.Concrete2
import GF.Infra.CheckM import GF.Infra.CheckM
import GF.Data.ErrM ( Err(Ok, Bad) ) import GF.Data.ErrM ( Err(Ok, Bad) )
import Control.Applicative(Applicative(..),(<|>)) import Control.Applicative(Applicative(..),(<|>))
import Control.Monad(ap,liftM,mplus,foldM,zipWithM,forM,filterM,unless) import Control.Monad(ap,liftM,liftM2,mplus,foldM,zipWithM,forM,filterM,unless)
import Control.Monad.ST import Control.Monad.ST
import GF.Text.Pretty import GF.Text.Pretty
import Data.STRef import Data.STRef
@@ -75,7 +75,7 @@ vtypePType = VSort cPType
vtypeMarkup= VApp poison (cPredef,cMarkup) [] vtypeMarkup= VApp poison (cPredef,cMarkup) []
tcRho :: Scope -> Choice -> Term -> Maybe Rho -> EvalM (Term, Rho) 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@(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@(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 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 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) =
@@ -200,7 +200,7 @@ tcRho scope c (FV ts) mb_ty = do
tcRho scope s t@(Sort _) mb_ty = do tcRho scope s t@(Sort _) mb_ty = do
instSigma scope s t vtypeType mb_ty instSigma scope s t vtypeType mb_ty
tcRho scope c t@(RecType rs) Nothing = do 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) return (RecType rs,fromMaybe vtypePType mb_ty)
tcRho scope c t@(RecType rs) (Just ty) = do tcRho scope c t@(RecType rs) (Just ty) = do
(scope,f,ty') <- skolemise scope ty (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 ty -> do ty <- value2termM False (scopeVars scope) ty
evalError ("The record type" <+> ppTerm Unqualified 0 t $$ evalError ("The record type" <+> ppTerm Unqualified 0 t $$
"cannot be of type" <+> ppTerm Unqualified 0 ty) "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) return (f (RecType rs),ty)
tcRho scope s t@(Table p res) mb_ty = do tcRho scope s t@(Table p res) mb_ty = do
let (s1,s23) = split s let (s1,s23) = split s
@@ -241,15 +241,13 @@ tcRho scope c (S t p) mb_ty = do
return (S t p, res_ty) return (S t p, res_ty)
tcRho scope c (T tt ps) Nothing = do -- ABS1/AABS1 for tables tcRho scope c (T tt ps) Nothing = do -- ABS1/AABS1 for tables
let (c1,c2) = split c let (c1,c2) = split c
let mk_val i = VMeta i [] mb_p_ty <- case tt of
p_ty <- case tt of TRaw -> return Nothing
TRaw -> fmap mk_val $ newResiduation scope
TTyped ty -> do let (c3,c4) = split c1 TTyped ty -> do let (c3,c4) = split c1
(ty, _) <- tcRho scope c3 ty (Just vtypeType) (ty, _) <- tcRho scope c3 ty (Just vtypeType)
g <- globals g <- globals
return (eval g (scopeEnv scope) c4 ty []) return (Just (eval g (scopeEnv scope) c4 ty []))
res_ty <- fmap mk_val $ newResiduation scope (ps,p_ty,res_ty) <- tcCases scope c2 ps mb_p_ty Nothing
ps <- tcCases scope c2 ps p_ty res_ty
p_ty_t <- value2termM True [] p_ty p_ty_t <- value2termM True [] p_ty
return (T (TTyped p_ty_t) ps, VTable p_ty res_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 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 TTyped ty -> do let (c1,c2) = split c12
(ty, _) <- tcRho scope c1 ty (Just vtypeType) (ty, _) <- tcRho scope c1 ty (Just vtypeType)
g <- globals g <- globals
unify scope (eval g (scopeEnv scope) c2 ty []) p_ty subsCheckRho scope (Meta 0) (eval g (scopeEnv scope) c2 ty []) p_ty
ps <- tcCases scope c3 ps p_ty res_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 p_ty_t <- value2termM True (scopeVars scope) p_ty
return (f (T (TTyped p_ty_t) ps), VTable p_ty res_ty) return (f (T (TTyped p_ty_t) ps), VTable p_ty res_ty)
tcRho scope c (V p_ty ts) Nothing = do 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 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) return (V p_ty0 ts, VTable p_ty res_ty)
tcRho scope c (R rs) Nothing = do 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,True,ty) | (l,t,ty) <- lttys] VRecType [(l,True,ty) | (l,t,ty) <- lttys] False
) )
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
case ty' of 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 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,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) 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 (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
@@ -313,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,True,l_ty)])) (t,t_ty) <- tcRho scope c t (Just (VRecType [(l,True,l_ty)] True))
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
@@ -325,33 +324,83 @@ tcRho scope c (Glue t1 t2) mb_ty = do
(t1,t1_ty) <- tcRho scope c1 t1 (Just vtypeStr) (t1,t1_ty) <- tcRho scope c1 t1 (Just vtypeStr)
(t2,t2_ty) <- tcRho scope c2 t2 (Just vtypeStr) (t2,t2_ty) <- tcRho scope c2 t2 (Just vtypeStr)
instSigma scope c3 (Glue t1 t2) vtypeStr mb_ty instSigma scope c3 (Glue t1 t2) vtypeStr mb_ty
tcRho scope c t@(ExtR t1 t2) mb_ty = do tcRho scope c t@(ExtR t1 t2) mb_ty =
case (t2,mb_ty) of
(R rs,Just (VRecType ltys ext)) -> do
let ll2 = map fst rs
(c1,c2) = split c
(t1,ty1@(VRecType ltys1 ext)) <- tcRho scope c1 t1 (Just (VRecType [field | field@(l,_,_) <- ltys, not (elem l ll2)] ext))
let (scope',proj1,wrap) = access scope t1 ty1
lttys2 <- checkRecFields scope' c2 [] rs [field | field@(l,_,_) <- ltys, elem l ll2]
let proj2 l =
case [(Nothing,t) | (l',t,_) <- lttys2, l'==l] of
[] -> Nothing
(x:_) -> Just x
return (wrap (R [(l,t) | (l,_,_) <- ltys, Just t <- [if elem l ll2 then proj2 l else proj1 l]]),
VRecType ltys False
)
_ -> do
let (c1,c2,c3,c4) = split4 c let (c1,c2,c3,c4) = split4 c
(t1,t1_ty) <- tcRho scope c1 t1 Nothing (t1,t1_ty) <- tcRho scope c1 t1 Nothing
(t2,t2_ty) <- tcRho scope c2 t2 Nothing (t2,t2_ty) <- tcRho scope c2 t2 Nothing
ty <- join t1_ty t2_ty ty <- join t1_ty t2_ty
instSigma scope c3 (ExtR t1 t2) ty mb_ty let (scope1,proj1,wrap1) = access scope t1 t1_ty
(scope2,proj2,wrap2) = access scope1 t2 t2_ty
let t = case (mb_ty,ty,t2_ty) of
(Just (VRecType ltys False), _, VRecType ltys2 False) ->
let ll2 = [l | (l,_,_) <- ltys2]
in (wrap1 . wrap2) (R [(l,t) | (l,_,_) <- ltys, Just t <- [if elem l ll2 then proj2 l else proj1 l]])
(_, VRecType ltys False, VRecType ltys2 False) ->
let ll2 = [l | (l,_,_) <- ltys2]
in (wrap1 . wrap2) (R [(l,t) | (l,_,_) <- ltys, Just t <- [if elem l ll2 then proj2 l else proj1 l]])
_ -> ExtR t1 t2
return (t,ty)
where where
access scope (R rs) ty = (scope
,\l -> lookup l rs
,id
)
access scope (RecType rs) ty
= (scope
,\l -> fmap ((,) Nothing) (lookup l rs)
,id
)
access scope t@(Vr x) ty
= (scope
,\l -> return (Nothing,P t l)
,id
)
access scope t ty = let x = newVar scope
in (((x,ty):scope)
,\l -> return (Nothing,P (Vr x) l)
,Let (x, (Nothing, t))
)
join (VMeta i vs) ty2 = do join (VMeta i vs) ty2 = do
mv <- getMeta i mv <- getMeta i
case mv of case mv of
Bound _ v -> do Bound _ v -> do
g <- globals g <- globals
join (apply g v vs) ty2 join (apply g v vs) ty2
_ -> evalError (pp "Cannot type check record extensions when one of the types is a meta variable")
join ty1 (VMeta j vs) = do join ty1 (VMeta j vs) = do
mv <- getMeta j mv <- getMeta j
case mv of case mv of
Bound _ v -> do Bound _ v -> do
g <- globals g <- globals
join ty1 (apply g v vs) join ty1 (apply g v vs)
_ -> evalError (pp "Cannot type check record extensions when one of the types is a meta variable")
join (VSort s1) (VSort s2) join (VSort s1) (VSort s2)
| (s1 == cType || s1 == cPType) && | (s1 == cType || s1 == cPType) &&
(s2 == cType || s2 == cPType) = let sort | s1 == cPType && s2 == cPType = cPType (s2 == cType || s2 == cPType) = let sort | s1 == cPType && s2 == cPType = cPType
| otherwise = cType | otherwise = cType
in return (VSort sort) 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 rs <- foldM (\rs (l,o,ctr) -> extend l o ctr rs) rs1 rs2
return (VRecType rs) return (VRecType rs (ext1 || ext2))
where where
extend l o1 ty1 [] = do return [(l,o1,ty1)] extend l o1 ty1 [] = do return [(l,o1,ty1)]
extend l o1 ty1 ((l',o2,ty2):rs) extend l o1 ty1 ((l',o2,ty2):rs)
@@ -387,16 +436,16 @@ tcRho scope c (EPattType ty) mb_ty = do
let (c1,c2) = split c let (c1,c2) = split c
(ty, _) <- tcRho scope c1 ty (Just vtypeType) (ty, _) <- tcRho scope c1 ty (Just vtypeType)
instSigma scope c2 (EPattType ty) vtypeType mb_ty instSigma scope c2 (EPattType ty) vtypeType mb_ty
tcRho scope c t@(EPatt min max p) mb_ty = do tcRho scope c t@(EPatt _ _ p) mb_ty = do
(scope,f,ty) <- case mb_ty of (scope,f,mb_ty) <- case mb_ty of
Nothing -> do i <- newResiduation scope Nothing -> return (scope,id,Nothing)
return (scope,id,VMeta i [])
Just ty -> do (scope,f,ty) <- skolemise scope ty Just ty -> do (scope,f,ty) <- skolemise scope ty
case ty of case ty of
VPattType ty -> return (scope,f,ty) VPattType ty -> return (scope,f,Just ty)
_ -> evalError (ppTerm Unqualified 0 t <+> "must be of pattern type but" <+> ppTerm Unqualified 0 t <+> "is expected") _ -> evalError (ppTerm Unqualified 0 t <+> "must be of pattern type but" <+> ppTerm Unqualified 0 t <+> "is expected")
tcPatt scope c p ty (_,ty) <- tcPatt scope c p mb_ty
return (f (EPatt min max p), ty) (min,max,p) <- measurePatt p
return (f (EPatt min max p), VPattType ty)
tcRho scope c (Markup tag attrs children) mb_ty = do tcRho scope c (Markup tag attrs children) mb_ty = do
let (c1,c2,c3,c4) = split4 c let (c1,c2,c3,c4) = split4 c
attrs <- mapCM (\c (id,t) -> do attrs <- mapCM (\c (id,t) -> do
@@ -406,7 +455,7 @@ tcRho scope c (Markup tag attrs children) mb_ty = do
res <- mapCM (\c child -> tcRho scope c child Nothing) c2 children res <- mapCM (\c child -> tcRho scope c child Nothing) c2 children
instSigma scope c3 (Markup tag attrs (map fst res)) vtypeMarkup mb_ty instSigma scope c3 (Markup tag attrs (map fst res)) vtypeMarkup mb_ty
tcRho scope c (Reset ctl mb_ct t qid) mb_ty tcRho scope c (Reset ctl mb_ct t qid) mb_ty
| ctl == cConcat = do | ctl == cConcat || ctl == cConcat' = do
let (c1,c23) = split c let (c1,c23) = split c
(c2,c3 ) = split c23 (c2,c3 ) = split c23
(t,_) <- tcRho scope c1 t Nothing (t,_) <- tcRho scope c1 t Nothing
@@ -423,6 +472,21 @@ tcRho scope c (Reset ctl mb_ct t qid) mb_ty
return (Just ct,ty) return (Just ct,ty)
Nothing -> return (Nothing,ty) Nothing -> return (Nothing,ty)
return (Reset ctl mb_ct t qid,ty) return (Reset ctl mb_ct t qid,ty)
| ctl == cSelect = do
let (c1,c2) = split c
ty <- case mb_ty of
Just ty -> return ty
Nothing -> do i <- newResiduation scope
return (VMeta i [])
let rec_ty = VRecType [ (ident2label cp1, True, ty)
, (ident2label cp2, True, VSort cStr)
] False
mb_ct <- case mb_ct of
Just ct -> do (ct,_) <- tcRho scope c2 ct (Just vtypeInt)
return (Just ct)
Nothing -> evalError (pp "[select: .. | ..] requires an integer argument")
(t,_) <- tcRho scope c1 t (Just rec_ty)
return (Reset ctl mb_ct t qid,ty)
| ctl == cDefault = do | ctl == cDefault = do
let (c1,c2) = split c let (c1,c2) = split c
(t,ty) <- tcRho scope c1 t mb_ty (t,ty) <- tcRho scope c1 t mb_ty
@@ -441,11 +505,22 @@ tcRho scope c (Reset ctl mb_ct t qid) mb_ty
case ty of case ty of
VApp c qid [] -> return (Reset ctl mb_ct t (Just qid), ty) VApp c qid [] -> return (Reset ctl mb_ct t (Just qid), ty)
_ -> evalError (pp "Needs atomic type"<+>ppValue Unqualified 0 ty) _ -> evalError (pp "Needs atomic type"<+>ppValue Unqualified 0 ty)
| ctl == cLen = do
do let (c1,c2) = split c
(t,_) <- tcRho scope c1 t Nothing
case mb_ct of
Just ct -> do res_ty <- case mb_ty of
Just ty -> return ty
Nothing -> do i <- newResiduation scope
return (VMeta i [])
(ct,_) <- tcRho scope c2 ct (Just (VProd Explicit identW vtypeInt res_ty))
return (Reset ctl (Just ct) t Nothing, res_ty)
Nothing -> instSigma scope c2 (Reset ctl Nothing t Nothing) vtypeInt mb_ty
| otherwise = evalError (pp "Operator" <+> pp ctl <+> pp "is not defined") | otherwise = evalError (pp "Operator" <+> pp ctl <+> pp "is not defined")
tcRho scope s (Opts n cs) mb_ty = do tcRho scope s (Opts n cs) mb_ty = do
let (s1,s2,s3) = split3 s let (s1,s2,s3) = split3 s
(n,_) <- tcRho scope s1 n Nothing (n,_) <- tcRho scope s1 n Nothing
(ls,_) <- tcUnifying scope s2 (fst <$> cs) Nothing (ls,_) <- tcUnifyingMaybe scope s2 (fst <$> cs) Nothing
(ts,ty) <- tcUnifying scope s3 (snd <$> cs) mb_ty (ts,ty) <- tcUnifying scope s3 (snd <$> cs) mb_ty
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)
@@ -471,13 +546,30 @@ tcUnifying scope c ts mb_ty = do
ts <- mapCM go c ts ts <- mapCM go c ts
return (ts,ty) return (ts,ty)
tcCases scope c [] p_ty res_ty = return [] tcUnifyingMaybe :: Scope -> Choice -> [Maybe Term] -> Maybe Rho -> EvalM ([Maybe Term], Value)
tcCases scope c ((p,t):cs) p_ty res_ty = do tcUnifyingMaybe scope c ts mb_ty = do
(ty,subsume) <-
case mb_ty of
Just ty -> do return (ty, \t ty' -> return t)
Nothing -> do i <- newResiduation scope
let ty = VMeta i []
return (ty, \t ty' -> subsCheckRho scope t ty' ty >>= \(t,_,_) -> return t)
let go c (Just t) = do (t, ty) <- tcRho scope c t mb_ty
fmap Just $ subsume t ty
go c Nothing = do return Nothing
ts <- mapCM go c ts
return (ts,ty)
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 let (c1,c2,c3,c4) = split4 c
scope' <- tcPatt scope c1 p p_ty (scope',p_ty) <- tcPatt scope c1 p mb_p_ty
(t,_) <- tcRho scope' c2 t (Just res_ty) (t,res_ty) <- tcRho scope' c2 t mb_res_ty
cs <- tcCases scope c3 cs p_ty res_ty (cs,p_ty,res_ty) <- tcCases scope c3 cs (Just p_ty) (Just res_ty)
return ((p,t):cs) (_,_,p) <- measurePatt p
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 (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) tcApp scope c t0 t@(Q id) args mb_ty = resolveOverloads scope c t0 id args mb_ty -- VAR (global)
@@ -521,9 +613,11 @@ resolveOverloads scope c t0 q args mb_ty = do
instSigma scope c3 t ty mb_ty instSigma scope c3 t ty mb_ty
Ok ttys -> do let (c1,c23) = split c Ok ttys -> do let (c1,c23) = split c
(c2,c3) = split c23 (c2,c3) = split c23
sz <- checkpoint
arg_tys <- mapCM (checkArg g) c1 args arg_tys <- mapCM (checkArg g) c1 args
let v_ttys = mapC (\c (t,ty) -> (t,eval g [] c ty [])) c2 ttys let v_ttys = mapC (\c (t,ty) -> (t,eval g [] c ty [])) c2 ttys
try (\(fun,fun_ty) -> reapply2 scope c3 fun fun_ty arg_tys mb_ty) try sz
(\(fun,fun_ty) -> reapply2 scope c3 fun fun_ty arg_tys mb_ty)
(\ttys -> fmap (\(ts,ty) -> (mkFV ts,ty)) (snd (minimum g ttys))) (\ttys -> fmap (\(ts,ty) -> (mkFV ts,ty)) (snd (minimum g ttys)))
v_ttys v_ttys
where where
@@ -544,43 +638,31 @@ resolveOverloads scope c t0 q args mb_ty = do
minimum g [] = (maxBound,err) minimum g [] = (maxBound,err)
where where
err = evalError (pp "Overload resolution failed") err = evalError (pp "Overload resolution failed")
minimum g (tty@((t,ty),state):ttys) = minimum g (tty@(t,ty):ttys) =
let ty' = zonk ty let a = arity ty
a = arity ty'
(a',res) = minimum g ttys (a',res) = minimum g ttys
in case compare a a' of in case compare a a' of
GT -> (a',res) GT -> (a',res)
EQ -> (a',join t ty' state res) EQ -> (a',join t ty res)
LT -> (a ,one t ty' state) LT -> (a ,one t ty)
where where
arity :: Value -> Int arity :: Value -> Int
arity (VProd _ _ _ ty) = 1 + arity ty arity (VProd _ _ _ ty) = 1 + arity ty
arity _ = 0 arity _ = 0
zonk :: Value -> Value one t ty = do
zonk (VProd bt x ty1 ty2) = VProd bt x (zonk ty1) (zonk ty2)
zonk (VMeta i vs) =
case Map.lookup i (metaVars state) of
Just (Bound _ v) -> zonk (apply g v vs)
_ -> VMeta i (map zonk vs)
zonk (VSusp i k vs) =
case Map.lookup i (metaVars state) of
Just (Bound _ v) -> zonk (apply g (k v) vs)
_ -> VSusp i k (map zonk vs)
zonk v = v
one t ty state = do
t <- withState state (zonkTerm [] t)
return ([t],ty) return ([t],ty)
join t ty state res = do join t ty res = do
t <- withState state (zonkTerm [] t)
(ts,ty') <- res (ts,ty') <- res
ty <- supertype scope (Just ty) ty' ty <- supertype scope (Just ty) ty'
return (t:ts,ty) return (t:ts,ty)
reapply2 :: Scope -> Choice -> Term -> Value -> [(Term,Value,Value)] -> Maybe Rho -> EvalM (Term,Rho) reapply2 :: Scope -> Choice -> Term -> Value -> [(Term,Value,Value)] -> Maybe Rho -> EvalM (Term,Rho)
reapply2 scope c fun fun_ty [] mb_ty = instSigma scope c fun fun_ty mb_ty reapply2 scope c fun fun_ty [] mb_ty = do
(fun,fun_ty) <- instSigma scope c fun fun_ty mb_ty
fun <- zonkTerm (scopeVars scope) fun
return (fun,fun_ty)
reapply2 scope c fun fun_ty ((ImplArg arg,arg_v,arg_ty):args) mb_ty = do -- Implicit arg case reapply2 scope c fun fun_ty ((ImplArg arg,arg_v,arg_ty):args) mb_ty = do -- Implicit arg case
(bt, x, arg_ty', res_ty) <- unifyFun scope fun_ty (bt, x, arg_ty', res_ty) <- unifyFun scope fun_ty
unless (bt == Implicit) $ unless (bt == Implicit) $
@@ -596,11 +678,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 res_ty <- evalCodomain x arg_v 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 Nothing = do
return scope i <- newResiduation scope
tcPatt scope c (PV x) ty0 = return (scope,VMeta i [])
return ((x,ty0):scope) tcPatt scope c PW (Just ty0) =
tcPatt scope c (PP q ps) ty0 = do 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 g@(Gl gr _) <- globals
ty <- case lookupResType gr q of ty <- case lookupResType gr q of
Ok ty -> return ty Ok ty -> return ty
@@ -608,110 +697,196 @@ tcPatt scope c (PP q ps) ty0 = do
let go scope c ty [] = return (scope,ty) let go scope c ty [] = return (scope,ty)
go scope c ty (p:ps) = do (_,_,arg_ty,res_ty) <- unifyFun scope ty go scope c ty (p:ps) = do (_,_,arg_ty,res_ty) <- unifyFun scope ty
let (c1,c2) = split c 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 go scope c2 res_ty ps
let (c1,c2) = split c let (c1,c2) = split c
(scope,ty) <- go scope c1 (eval g [] c2 ty []) ps (scope,res_ty) <- go scope c1 (eval g [] c2 ty []) ps
unify scope ty0 ty case mb_ty of
return scope Just ty -> unify scope ty res_ty
tcPatt scope c p@(PInt i) ty0 = Nothing -> return ()
case ty0 of return (scope,res_ty)
VInts min max tcPatt scope c p@(PInt i) mb_ty =
| i <= fromMaybe i max -> return scope 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) | otherwise -> evalError ("Ints" <+> i <+> "is not a subtype of" <+> ppValue Unqualified 0 ty0)
VMeta k vs -> do Just ty0@(VMeta k vs) -> do
mv <- getMeta k mv <- getMeta k
case mv of case mv of
Bound _ v -> do Bound scope1 v -> do
g <- globals 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 Residuation scope1 -> do
setMeta k (Bound scope1 (VInts (Just i) Nothing)) setMeta k (Bound scope1 (VInts i True))
return scope return (scope,ty0)
Nothing -> return (scope,VInts i True)
_ -> evalError (pp "An integer must have an Int or Ints n type") _ -> evalError (pp "An integer must have an Int or Ints n type")
tcPatt scope c (PString s) ty0 = do tcPatt scope c (PString s) mb_ty = do
unify scope ty0 vtypeStr case mb_ty of
return scope Just ty -> unify scope ty vtypeStr
tcPatt scope c PChar ty0 = do Nothing -> return ()
unify scope ty0 vtypeStr return (scope,vtypeStr)
return scope tcPatt scope c PChar mb_ty = do
tcPatt scope c (PChars cs) ty0 = do case mb_ty of
unify scope ty0 vtypeStr Just ty -> unify scope ty vtypeStr
return scope Nothing -> return ()
tcPatt scope c (PSeq _ _ p1 _ _ p2) ty0 = do return (scope,vtypeStr)
unify scope ty0 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 let (c1,c2) = split c
scope <- tcPatt scope c1 p1 vtypeStr (scope,_) <- tcPatt scope c1 p1 (Just vtypeStr)
scope <- tcPatt scope c2 p2 vtypeStr (scope,_) <- tcPatt scope c2 p2 (Just vtypeStr)
return scope return (scope,vtypeStr)
tcPatt scope c (PRep _ _ p) ty0 = do tcPatt scope c (PRep _ _ p) mb_ty = do
unify scope ty0 vtypeStr case mb_ty of
tcPatt scope c p vtypeStr Just ty -> unify scope ty vtypeStr
tcPatt scope c (PAs x p) ty0 = do Nothing -> return ()
tcPatt ((x,ty0):scope) c p ty0 tcPatt scope c p (Just vtypeStr)
tcPatt scope c p@(PR rs) ty0 = tcPatt scope c (PAs x p) mb_ty = do
case ty0 of ty <- case mb_ty of
VRecType ltys -> Just ty -> return ty
let go scope c [] = return scope Nothing -> do i <- newResiduation scope
go scope c ((l,p):rs) = return (VMeta i [])
case lookup3 l ltys of tcPatt ((x,ty):scope) c p (Just ty)
Just ty -> do let (c1,c2) = split c tcPatt scope c p@(PR rs) mb_ty =
scope <- tcPatt scope c1 p ty case mb_ty of
go scope c2 rs Just (VRecType ltys ext) -> check scope c rs ltys ext
Nothing -> do ty <- value2termM False (scopeVars scope) ty0 Just ty0@(VMeta i vs) -> do
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
mv <- getMeta i mv <- getMeta i
case mv of case mv of
Bound _ v -> Bound scope1 v ->
tcPatt scope c p (apply g v vs) do g <- globals
(scope,ty) <- tcPatt scope c p (Just (apply g v vs))
setMeta i (Bound scope1 ty)
return (scope,ty0)
Residuation scope1 -> Residuation scope1 ->
let go scope c [] = return (scope,[]) do (scope,ltys) <- infer scope c rs
go scope c ((l,p):rs) = do setMeta i (Bound scope1 (VRecType ltys True))
i <- newResiduation scope return (scope,ty0)
let ty = VMeta i [] Nothing ->do (scope,ltys) <- infer scope c rs
(c1,c2) = split c return (scope,VRecType ltys True)
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
_ -> evalError (pp "An record must have an record type") _ -> 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 let (c1,c2) = split c
tcPatt scope c1 p1 ty0 (scope,ty) <- tcPatt scope c1 p Nothing
tcPatt scope c2 p2 ty0 (scope,ltys) <- infer scope c2 rs
return scope return (scope,(l,True,ty):ltys)
tcPatt scope c (PM q) ty0 = do 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
(_,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 g@(Gl gr _) <- globals
ty <- case lookupResType gr q of ty <- case lookupResType gr q of
Ok ty -> return ty Ok ty -> return ty
Bad msg -> evalError (pp msg) Bad msg -> evalError (pp msg)
case ty of case ty of
EPattType ty EPattType ty
-> do unify scope ty0 (eval g [] c ty []) -> do let vty = eval g [] c ty []
return scope case mb_ty of
Just ty0 -> unify scope ty0 vty
Nothing -> return ()
return (scope,vty)
ty -> evalError ("Pattern type expected but " <+> pp ty <+> " found.") ty -> evalError ("Pattern type expected but " <+> pp ty <+> " found.")
tcPatt scope c p ty = unimplemented ("tcPatt "++show p) tcPatt scope c p ty = unimplemented ("tcPatt "++show p)
inferRecFields scope c rs = measurePatt p =
mapCM (\c (l,r) -> tcRecField scope c l r Nothing) c rs case p of
PM q -> do g <- globals
case eval g [] unit (Q q) [] of
VPatt minp maxp _ -> return (minp,maxp,p)
v -> evalError ("Expected pattern macro, but found:" $$ nest 2 (ppValue Unqualified 0 v))
PR ass -> do ass <- mapM (\(lbl,p) -> measurePatt p >>= \(_,_,p') -> return (lbl,p')) ass
return (0,Nothing,PR ass)
PString s -> do let len=length s
return (len,Just len,p)
PT t p -> do (min,max,p') <- measurePatt p
return (min,max,PT t p')
PAs x p -> do (min,max,p) <- measurePatt p
case p of
PW -> return (0,Nothing,PV x)
_ -> return (min,max,PAs x p)
PImplArg p -> do (min,max,p') <- measurePatt p
return (min,max,PImplArg p')
PNeg p -> do (_,_,p') <- measurePatt p
return (0,Nothing,PNeg p')
PAlt p1 p2 -> do (min1,max1,p1) <- measurePatt p1
(min2,max2,p2) <- measurePatt p2
case (p1,p2) of
(PString [c1],PString [c2]) -> return (1,Just 1,PChars [c1,c2])
(PString [c], PChars cs) -> return (1,Just 1,PChars ([c]++cs))
(PChars cs, PString [c]) -> return (1,Just 1,PChars (cs++[c]))
(PChars cs1, PChars cs2) -> return (1,Just 1,PChars (cs1++cs2))
_ -> return (min min1 min2,liftM2 max max1 max2,PAlt p1 p2)
PSeq _ _ p1 _ _ p2
-> do (min1,max1,p1) <- measurePatt p1
(min2,max2,p2) <- measurePatt p2
case (p1,p2) of
(PW, PW ) -> return (0,Nothing,PW)
(PString s1,PString s2) -> return (min1+min2,liftM2 (+) max1 max2,PString (s1++s2))
_ -> return (min1+min2,liftM2 (+) max1 max2,PSeq min1 max1 p1 min2 max2 p2)
PRep _ _ p -> do (minp,maxp,p) <- measurePatt p
case p of
PW -> return (0,Nothing,PW)
PChar -> return (0,Nothing,PW)
_ -> return (0,Nothing,PRep minp maxp p)
PChar -> return (1,Just 1,p)
PChars _ -> return (1,Just 1,p)
_ -> return (0,Nothing,p)
checkRecFields scope c [] ltys 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 ls [] ltys
| null ltys = return [] | null ltys = return []
| otherwise = evalError ("Missing fields:" <+> hsep [l | (l,_,_) <- ltys]) | otherwise = evalError ("Missing fields:" <+> hsep [l | (l,_,_) <- ltys])
checkRecFields scope c ((l,t):lts) ltys = checkRecFields scope c ls ((l,t):lts) ltys
| elem l ls = evalError ("Repeated definition for field" <+> l)
| otherwise =
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
ltty <- tcRecField scope c1 l t (Just ty) ltty <- tcRecField scope c1 l t (Just ty)
lttys <- checkRecFields scope c2 lts ltys lttys <- checkRecFields scope c2 ls lts ltys
return (ltty : lttys) return (ltty : lttys)
(Nothing,ltys) -> do evalWarn ("Discarded field:" <+> l) (Nothing,ltys) -> do evalWarn ("Discarded field:" <+> l)
lttys <- checkRecFields scope c lts ltys lttys <- checkRecFields scope c ls lts ltys
return lttys -- ignore the field return lttys -- ignore the field
where where
takeIt l1 [] = (Nothing, []) takeIt l1 [] = (Nothing, [])
@@ -731,8 +906,10 @@ tcRecField scope c l (mb_ann_ty,t) mb_ty = do
Nothing -> tcRho scope c t mb_ty Nothing -> tcRho scope c t mb_ty
return (l,t,ty) return (l,t,ty)
tcRecTypeFields scope c [] mb_ty = return ([],mb_ty) tcRecTypeFields scope c ls [] mb_ty = return ([],mb_ty)
tcRecTypeFields scope c ((l,ty):rs) mb_ty = do 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 let (c1,c2) = split c
(ty,sort) <- tcRho scope c1 ty mb_ty (ty,sort) <- tcRho scope c1 ty mb_ty
mb_ty <- case sort of mb_ty <- case sort of
@@ -743,7 +920,7 @@ tcRecTypeFields scope c ((l,ty):rs) mb_ty = do
_ -> do sort <- value2termM False (scopeVars scope) sort _ -> do sort <- value2termM False (scopeVars scope) sort
evalError ("The record type field" <+> l <+> ':' <+> ppTerm Unqualified 0 ty $$ evalError ("The record type field" <+> l <+> ':' <+> ppTerm Unqualified 0 ty $$
"cannot be of type" <+> ppTerm Unqualified 0 sort) "cannot be of type" <+> ppTerm Unqualified 0 sort)
(rs,mb_ty) <- tcRecTypeFields scope c2 rs mb_ty (rs,mb_ty) <- tcRecTypeFields scope c2 (l:ls) rs mb_ty
return ((l,ty):rs,mb_ty) return ((l,ty):rs,mb_ty)
-- | Invariant: if the third argument is (Just rho), -- | Invariant: if the third argument is (Just rho),
@@ -839,26 +1016,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. | p == (cPredef,cInt) = return (t,ty1,ty2) -- Should be only a temporary hack.
subsCheckRho scope t ty1@(VInts _ _) ty2@(VApp _ p _) -- Rule INT1 subsCheckRho scope t ty1@(VInts _ _) ty2@(VApp _ p _) -- Rule INT1
| p == (cPredef,cInt) = return (t,ty1,ty2) | p == (cPredef,cInt) = return (t,ty1,ty2)
subsCheckRho scope t ty1@(VInts i1 j1) ty2@(VInts i2 j2) -- Rule INT2 subsCheckRho scope t ty1@(VInts n1 ext1) ty2@(VInts n2 ext2) -- Rule INT2
| j1 `less1` i2 = return (t,ty1,ty2) | n1 <= n2 = return (t,ty1,ty2)
| j1' `less1` i2' = return (t,VInts i1 j1',VInts i2' j2) | ext2 = return (t,ty1,VInts n1 ext2)
| otherwise = evalError ("In the term" <+> ppTerm Unqualified 0 t $$ | otherwise = evalError ("In the term" <+> ppTerm Unqualified 0 t $$
ppValue Terse 0 ty1 <+> "is not a subtype of" <+> ppValue Terse 0 ty2) ppValue Terse 0 ty1 <+> "is not a subtype of" <+> ppValue Terse 0 ty2)
where subsCheckRho scope t ty1@(VRecType rs1 ext1) ty2@(VRecType rs2 ext2) = do -- Rule REC
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
let mkAccess scope t = let mkAccess scope t =
case t of case t of
ExtR t1 (R rs) -> ExtR t1 (R rs) ->
@@ -873,80 +1036,115 @@ subsCheckRho scope t ty1@(VRecType rs1) ty2@(VRecType rs2) = do -- Rule REC
,\l -> lookup l rs ,\l -> lookup l rs
,id ,id
) )
Vr x -> return (scope
,\l -> return (Nothing,P t l)
,\t' -> if is_trivial x t' then t else t'
)
t -> let x = newVar scope t -> let x = newVar scope
in return (((x,ty1):scope) in return (((x,ty1):scope)
,\l -> return (Nothing,P (Vr x) l) ,\l -> return (Nothing,P (Vr x) l)
,Let (x, (Nothing, t)) ,\t' -> if is_trivial x t' then t else Let (x, (Nothing, t)) t'
) )
mkField scope l (mb_ty,t) ty1 ty2 = do is_trivial x (R rs) = all is_selection rs
(t,_,_) <- subsCheckRho scope t ty1 ty2 where
return (l, (mb_ty,t)) is_selection (l, (_, P (Vr u) l'))
| l == l' && u == x = True
is_selection _ = False
is_trivial x _ = False
(scope,mkProj,mkWrap) <- mkAccess scope t mkField scope l (mb_ty,t) (Just ty1) ty2 = do
(t,ty1,ty2) <- subsCheckRho scope t ty1 ty2
return ((l, (mb_ty,t)), (l, True, ty1))
mkField scope l (mb_ty,t) Nothing ty2
| isLockLabel l = return ((l, (Just (RecType []),R [])), (l, True, ty2))
| otherwise = return ((l, (mb_ty,t)), (l, True, ty2))
let fields = [(l,ty2,lookup3 l rs1) | (l,o2,ty2) <- rs2] (scope,mkProj,wrap) <- mkAccess scope t
case [l | (l,_,Nothing) <- fields, not (isLockLabel l)] of
let fields = [(l,o2,ty2,lookup3 l rs1) | (l,o2,ty2) <- rs2]
case [l | (l,_,_,Nothing) <- fields, not ext1 && not (isLockLabel l)] of
[] -> return () [] -> return ()
missing -> evalError ("In the term" <+> pp t $$ missing -> evalError ("In the term" <+> pp t $$
"there are no values for fields:" <+> hsep missing) "there are no values for fields:" <+> hsep missing)
rs <- sequence [mkField scope l t ty1 ty2 | (l,ty2,Just ty1) <- fields, Just t <- [mkProj l]] rs <- sequence [mkField scope l t mb_ty1 ty2 | (l,_,ty2,mb_ty1) <- fields, Just t <- [mkProj l]]
return (mkWrap (R (rs++[(l, (Just (RecType []),R [])) | (l,_,Nothing) <- fields, isLockLabel l])),ty1,ty2) return (wrap (R (map fst rs)),VRecType (foldl (\rs (_,(l,o,ty)) -> update3 l o ty rs) rs1 rs) ext2,ty2)
subsCheckRho scope t ty1 (VFV c (VarFree vs)) = do subsCheckRho scope t ty1 (VFV c (VarFree vs)) = do
ty2 <- variants c vs ty2 <- variants c vs
subsCheckRho scope t ty1 ty2 subsCheckRho scope t ty1 ty2
subsCheckRho scope t (VFV c (VarFree vs)) ty2 = do subsCheckRho scope t (VFV c (VarFree vs)) ty2 = do
ty1 <- variants c vs ty1 <- variants c vs
subsCheckRho scope t ty1 ty2 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 subsCheckRho scope t ty1 ty2 = do -- Rule EQ
unify scope ty1 ty2 -- Revert to ordinary unification unify scope ty1 ty2 -- Revert to ordinary unification
return (t,ty1,ty2) return (t,ty1,ty2)
subsCheckFun :: Scope -> Term -> Sigma -> Value -> Sigma -> Value -> EvalM (Term,Value,Value) subsCheckFun :: Scope -> Term -> Sigma -> Value -> Sigma -> Value -> EvalM (Term,Value,Value)
subsCheckFun scope t a1 r1 a2 r2 = do subsCheckFun scope t a1 r1 a2 r2 = do
let v = newVar scope let x = newVar scope
(vt,a2,a1) <- subsCheckRho ((v,a2):scope) (Vr v) a2 a1 (xt,a2,a1) <- subsCheckRho ((x,a2):scope) (Vr x) a2 a1
g <- globals g <- globals
let (v1',r1') = case r1 of let (x1',r1') = case r1 of
VClosure env c r1 -> (v,eval g ((v,(VGen (length scope) [])):env) c r1 []) VClosure env c r1 -> (x,eval g ((x,(VGen (length scope) [])):env) c r1 [])
r1 -> (identW,r1) r1 -> (identW,r1)
(v2',r2') = case r2 of (x2',r2') = case r2 of
VClosure env c r2 -> (v,eval g ((v,(VGen (length scope) [])):env) c r2 []) VClosure env c r2 -> (x,eval g ((x,(VGen (length scope) [])):env) c r2 [])
r2 -> (identW,r2) r2 -> (identW,r2)
(t,r1,r2) <- subsCheckRho ((v,vtypeType):scope) (App t vt) r1' r2' (t,r1,r2) <- subsCheckRho ((x,a2):scope) (App t xt) r1' r2'
return (Abs Explicit v t, VProd Explicit v1' a1 r1, VProd Explicit v2' a2 r2) case t of
App t (Vr u) | u == x -> return (t, VProd Explicit x1' a1 r1, VProd Explicit x2' a2 r2)
_ -> return (Abs Explicit x t, VProd Explicit x1' a1 r1, VProd Explicit x2' a2 r2)
subsCheckTbl :: Scope -> Term -> Sigma -> Rho -> Sigma -> Rho -> EvalM (Term,Value,Value) subsCheckTbl :: Scope -> Term -> Sigma -> Rho -> Sigma -> Rho -> EvalM (Term,Value,Value)
subsCheckTbl scope t p1 r1 p2 r2 = do subsCheckTbl scope t p1 r1 p2 r2 = do
let x = newVar scope (scope,y,sel,wrap) <-
(xt,p2,p1) <- subsCheckRho ((x,p2):scope) (Vr x) p2 p1 case t of
(t,r1,r2) <- subsCheckRho ((x,p2):scope) (S t xt) r1 r2 Vr x -> let y = newVar scope
in return ((y,p2):scope
,y
,\t -> S (Vr x) t
,\p2 t' -> case t' of
S (Vr u) (Vr v) | u == x && v == y -> t
_ -> T (TTyped p2) [(PV y,t')]
)
T _ [(PV x,t')] ->
let scope' = (x,p1):scope
y = newVar scope'
in return (((y,p2):scope')
,y
,\t -> Let (x, (Nothing, t)) t'
,\p2 t -> case t of
Let (u, (Nothing, Vr v)) t | u == x && v == y -> T (TTyped p2) [(PV x,t)]
_ -> T (TTyped p2) [(PV y,t)]
)
t -> let x = newVar scope
scope' = (x,VTable p1 r1):scope
y = newVar scope'
in return (((y,VTable p1 r1):scope')
,y
,\t -> S (Vr x) t
,\p2 t' -> case t' of
S (Vr u) (Vr v) | u == x && v == y -> t
_ -> Let (x, (Nothing, t)) (T (TTyped p2) [(PV y,t')])
)
(yt,p2,p1) <- subsCheckRho scope (Vr y) p2 p1
(t,r1,r2) <- subsCheckRho scope (sel yt) r1 r2
p2_t <- value2termM True (scopeVars scope) p2 p2_t <- value2termM True (scopeVars scope) p2
return (T (TTyped p2_t) [(PV x,t)],VTable p1 r1,VTable p2 r2) return (wrap p2_t t,VTable p1 r1,VTable p2 r2)
{-subtype scope Nothing (VInts i2 j2) =
return (VInts Nothing j2) subtype scope Nothing (VInts i2 _) =
subtype scope (Just (VMeta i vs)) ty2 = do return (VInts i2 True)
g <- globals subtype scope (Just (VInts n1 _)) (VInts n2 _) =
mv <- getMeta i return (VInts (min n1 n2) False)
case mv of subtype scope Nothing (VRecType ltys ext) = do
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
lctrs <- mapM (\(l,o,ty) -> subtype scope Nothing ty >>= \ctr -> return (l,o,ctr)) ltys lctrs <- mapM (\(l,o,ty) -> subtype scope Nothing ty >>= \ctr -> return (l,o,ctr)) ltys
return (VRecType lctrs) return (VRecType lctrs ext)
subtype scope (Just (VRecType lctrs1)) (VRecType lctrs2) = do subtype scope (Just (VRecType lctrs1 ext1)) (VRecType lctrs2 ext2) = do
lctrs <- foldM (\lctrs (l,o,ctr) -> union l o ctr lctrs) lctrs1 lctrs2 lctrs <- foldM (\lctrs (l,o,ctr) -> union l o ctr lctrs) lctrs1 lctrs2
return (VRecType lctrs) return (VRecType lctrs (ext1 || ext2))
where where
union l o1 ctr1 [] = do ctr <- subtype scope Nothing ctr1 union l o1 ctr1 [] = do ctr <- subtype scope Nothing ctr1
return [(l,True,ctr)] return [(l,True,ctr)]
@@ -973,24 +1171,16 @@ subtype scope (Just ctr) ty = do
unify scope ctr ty unify scope ctr ty
return ty return ty
supertype scope Nothing (VInts i2 j2) = supertype scope Nothing (VInts n2 _) =
return (VInts i2 Nothing) return (VInts n2 True)
supertype scope (Just (VInts i1 j1)) (VInts i2 j2) = supertype scope (Just (VInts n1 _)) (VInts n2 _) =
case VInts (lift min i1 i2) (lift max j1 j2) of return (VInts (max n1 n2) True)
ty@(VInts (Just i) (Just j)) supertype scope Nothing (VRecType ltys ext) = do
| 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
lctrs <- mapM (\(l,o,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 (VRecType lctrs) return (VRecType lctrs ext)
supertype scope (Just (VRecType lctrs1)) (VRecType lctrs2) = do supertype scope (Just (VRecType lctrs1 ext1)) (VRecType lctrs2 ext2) = do
lctrs <- foldM (\lctrs (l,o,ctr) -> intersect l o ctr lctrs lctrs2) [] lctrs1 lctrs <- foldM (\lctrs (l,o,ctr) -> intersect l o ctr lctrs lctrs2) [] lctrs1
return (VRecType lctrs) return (VRecType lctrs (ext1 || ext2))
where where
intersect l o1 ctr1 lctrs [] = return lctrs intersect l o1 ctr1 lctrs [] = return lctrs
intersect l o1 ctr1 lctrs ((l',o2,ctr2):lctrs2) intersect l o1 ctr1 lctrs ((l',o2,ctr2):lctrs2)
@@ -1092,9 +1282,7 @@ unify scope (VFlt x) (VFlt y)
unify scope (VStr s1) (VStr s2) unify scope (VStr s1) (VStr s2)
| s1 == s2 = return () | s1 == s2 = return ()
unify scope VEmpty VEmpty = return () unify scope VEmpty VEmpty = return ()
unify scope v1 v2 = do unify scope v1 v2 =
t1 <- value2termM False (scopeVars scope) v1
t2 <- value2termM False (scopeVars scope) v2
evalError ("Cannot unify:" <+> ppValue Qualified 0 v1 $$ evalError ("Cannot unify:" <+> ppValue Qualified 0 v1 $$
" with:" <+> ppValue Qualified 0 v2) " with:" <+> ppValue Qualified 0 v2)
@@ -1139,7 +1327,7 @@ occursCheck scope' i0 scope v =
VClosure env c t -> do g <- globals VClosure env c t -> do g <- globals
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_ (\(_,_,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
@@ -1246,9 +1434,9 @@ quantify scope t tvs ty = do
return (x:xs,VProd bt x v1 (VClosure env c t)) return (x:xs,VProd bt x v1 (VClosure env c t))
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 ext) = do
(xs,as) <- mapAccumM (\xs (l,o,v) -> check m n xs v >>= \(xs,v) -> return (xs,(l,o,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 ext)
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
return (xs,VR as) return (xs,VR as)
@@ -1339,6 +1527,11 @@ lookup3 l ((l',_,v):rs)
| l == l' = Just v | l == l' = Just v
| otherwise = lookup3 l rs | 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 -> Ident
newVar scope = head [x | i <- [1..], newVar scope = head [x | i <- [1..],
let x = identS ('v':show i), let x = identS ('v':show i),
@@ -1360,7 +1553,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 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 (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
@@ -1373,6 +1566,7 @@ getMetaVars sc_tys = foldM (\acc (scope,ty) -> go acc ty) [] sc_tys
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 (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)) go acc v = unimplemented ("go "++show (ppValue Unqualified 5 v))
-- | Eliminate any substitutions in a term -- | Eliminate any substitutions in a term
@@ -1393,3 +1587,24 @@ zonkTerm xs (Meta i) = do
Bound _ v -> zonkTerm xs =<< value2termM False xs v Bound _ v -> zonkTerm xs =<< value2termM False xs v
_ -> return (Meta i) _ -> return (Meta i)
zonkTerm xs t = composOp (zonkTerm xs) t zonkTerm xs t = composOp (zonkTerm xs) t
zonkValue :: Value -> EvalM Value
zonkValue (VProd bt x ty1 ty2) = do
ty1 <- zonkValue ty1
ty2 <- zonkValue ty2
return (VProd bt x ty1 ty2)
zonkValue (VMeta i vs) = do
g <- globals
st <- getMeta i
case st of
Bound _ v -> zonkValue (apply g v vs)
_ -> do vs <- mapM zonkValue vs
return (VMeta i vs)
zonkValue (VSusp i k vs) = do
g <- globals
st <- getMeta i
case st of
Bound _ v -> zonkValue (apply g (k v) vs)
_ -> do vs <- mapM zonkValue vs
return (VSusp i k vs)
zonkValue v = return v
src/compiler/api/GF/Grammar/Grammar.hs
+1 -1
View File
@@ -466,7 +466,7 @@ type Equation = ([Patt],Term)
type Labelling = (Label, Type) type Labelling = (Label, Type)
type Assign = (Label, (Maybe Type, Term)) type Assign = (Label, (Maybe Type, Term))
type Option = (Term, Term) type Option = (Maybe Term, Term)
type Case = (Patt, Term) type Case = (Patt, Term)
--type Cases = ([Patt], Term) --type Cases = ([Patt], Term)
type LocalDef = (Ident, (Maybe Type, Term)) type LocalDef = (Ident, (Maybe Type, Term))
src/compiler/api/GF/Grammar/Macros.hs
+2 -1
View File
@@ -404,6 +404,7 @@ composOp co trm =
RecType r -> liftM RecType (mapPairsM co r) RecType r -> liftM RecType (mapPairsM co r)
P t i -> liftM2 P (co t) (return i) P t i -> liftM2 P (co t) (return i)
ExtR a c -> liftM2 ExtR (co a) (co c) ExtR a c -> liftM2 ExtR (co a) (co c)
Opts t os -> liftM2 Opts (co t) (mapM (\(t1,t2) -> liftM2 (,) (maybe (return Nothing) (liftM Just . co) t1) (co t2)) os)
T i cc -> liftM2 (flip T) (mapPairsM co cc) (changeTableType co i) T i cc -> liftM2 (flip T) (mapPairsM co cc) (changeTableType co i)
V ty vs -> liftM2 V (co ty) (mapM co vs) V ty vs -> liftM2 V (co ty) (mapM co vs)
Let (x,(mt,a)) b -> liftM3 let' (co a) (T.mapM co mt) (co b) Let (x,(mt,a)) b -> liftM3 let' (co a) (T.mapM co mt) (co b)
@@ -450,7 +451,7 @@ collectOp co trm = case trm of
S c a -> co c <> co a S c a -> co c <> co a
Table a c -> co a <> co c Table a c -> co a <> co c
ExtR a c -> co a <> co c ExtR a c -> co a <> co c
Opts t os -> co t <> mconcatMap (\(a,b) -> co a <> co b) os Opts t os -> co t <> mconcatMap (\(a,b) -> maybe mempty co a <> co b) os
R r -> mconcatMap (\ (_,(mt,a)) -> maybe mempty co mt <> co a) r R r -> mconcatMap (\ (_,(mt,a)) -> maybe mempty co mt <> co a) r
RecType r -> mconcatMap (co . snd) r RecType r -> mconcatMap (co . snd) r
P t i -> co t P t i -> co t
src/compiler/api/GF/Grammar/Parser.y
+26 -18
View File
@@ -276,9 +276,9 @@ ParamDef
OperDef :: { [(Ident,Info)] } OperDef :: { [(Ident,Info)] }
OperDef OperDef
: Posn LhsNames ':' Exp ';' Posn { [(i, info) | i <- $2, info <- mkOverload (Just (mkL $1 $6 $4)) Nothing ] } : Posn LhsNames ':' Exp ';' Posn { [(i, info) | i <- $2, info <- mkOverload (Just (mkL $1 $6 $4)) Nothing ] }
| Posn LhsNames '=' Markup Posn { [(i, info) | i <- $2, info <- mkOverload Nothing (Just (mkL $1 $5 $4))] } | Posn LhsNames '=' Exp ';' Posn { [(i, info) | i <- $2, info <- mkOverload Nothing (Just (mkL $1 $6 $4))] }
| Posn LhsName ListArg '=' Markup Posn { [(i, info) | i <- [$2], info <- mkOverload Nothing (Just (mkL $1 $6 (mkAbs $3 $5)))] } | Posn LhsName ListArg '=' Exp ';' Posn { [(i, info) | i <- [$2], info <- mkOverload Nothing (Just (mkL $1 $7 (mkAbs $3 $5)))] }
| Posn LhsNames ':' Exp '=' Markup Posn { [(i, info) | i <- $2, info <- mkOverload (Just (mkL $1 $7 $4)) (Just (mkL $1 $7 $6))] } | Posn LhsNames ':' Exp '=' Exp ';' Posn { [(i, info) | i <- $2, info <- mkOverload (Just (mkL $1 $8 $4)) (Just (mkL $1 $8 $6))] }
LinDef :: { [(Ident,Info)] } LinDef :: { [(Ident,Info)] }
LinDef LinDef
@@ -452,7 +452,11 @@ Exp4 :: { Term }
Exp4 Exp4
: Exp4 Exp5 { App $1 $2 } : Exp4 Exp5 { App $1 $2 }
| Exp4 '{' Exp '}' { App $1 (ImplArg $3) } | Exp4 '{' Exp '}' { App $1 (ImplArg $3) }
| 'option' Exp 'of' '{' ListOpt '}' { Opts $2 $5 } | 'option' Exp 'of' '{' ListExp '}' { let toOption t =
case t of
Table x y -> (Just x, y)
y -> (Nothing, y)
in Opts $2 (map toOption $5) }
| 'case' Exp 'of' '{' ListCase '}' { let annot = case $2 of | 'case' Exp 'of' '{' ListCase '}' { let annot = case $2 of
Typed _ t -> TTyped t Typed _ t -> TTyped t
_ -> TRaw _ -> TRaw
@@ -487,8 +491,7 @@ Exp6
| '{' ListLocDef '}' {% mkR $2 } | '{' ListLocDef '}' {% mkR $2 }
| '<' ListTupleComp '>' { R (tuple2record $2) } | '<' ListTupleComp '>' { R (tuple2record $2) }
| '<' Exp ':' Exp '>' { Typed $2 $4 } | '<' Exp ':' Exp '>' { Typed $2 $4 }
| '[' Control '|' Tag ']' { Reset (fst $2) (snd $2) $4 Nothing } | '[' Control '|' ListMarkup ']' { Reset (fst $2) (snd $2) (mkMarkup $4) Nothing }
| '[' Control '|' Exp ']' { Reset (fst $2) (snd $2) $4 Nothing }
| '(' Exp ')' { $2 } | '(' Exp ')' { $2 }
ListExp :: { [Term] } ListExp :: { [Term] }
@@ -609,15 +612,6 @@ ListPattTupleComp
| Patt { [$1] } | Patt { [$1] }
| Patt ',' ListPattTupleComp { $1 : $3 } | Patt ',' ListPattTupleComp { $1 : $3 }
Opt :: { Option }
Opt
: '(' Exp ')' '=>' Exp { ($2,$5) }
ListOpt :: { [Option] }
ListOpt
: Opt { [$1] }
| Opt ';' ListOpt { $1 : $3 }
Case :: { Case } Case :: { Case }
Case Case
: Patt '=>' Exp { ($1,$3) } : Patt '=>' Exp { ($1,$3) }
@@ -721,13 +715,20 @@ ERHS3 :: { ERHS }
NLG :: { Map.Map Ident Info } NLG :: { Map.Map Ident Info }
: ListNLGDef { Map.fromList $1 } : ListNLGDef { Map.fromList $1 }
| Posn Tag Posn { Map.singleton (identS "main") (ResOper Nothing (Just (mkL $1 $3 $2))) }
| Posn Exp Posn { Map.singleton (identS "main") (ResOper Nothing (Just (mkL $1 $3 $2))) } | Posn Exp Posn { Map.singleton (identS "main") (ResOper Nothing (Just (mkL $1 $3 $2))) }
| Posn ListMarkup2 Posn { Map.singleton (identS "main") (ResOper Nothing (Just (mkL $1 $3 (mkMarkup $2)))) }
ListNLGDef :: { [(Ident,Info)] } ListNLGDef :: { [(Ident,Info)] }
ListNLGDef ListNLGDef
: {- empty -} { [] } : 'oper' NLGDef { [] }
| 'oper' OperDef ListNLGDef { $2 ++ $3 } | 'oper' NLGDef ListNLGDef { $2 ++ $3 }
NLGDef :: { [(Ident,Info)] }
NLGDef
: Posn LhsNames ':' Exp ';' Posn { [(i, info) | i <- $2, info <- mkOverload (Just (mkL $1 $6 $4)) Nothing ] }
| Posn LhsNames '=' ListMarkup2 Posn { [(i, info) | i <- $2, info <- mkOverload Nothing (Just (mkL $1 $5 (mkMarkup $4)))] }
| Posn LhsName ListArg '=' ListMarkup2 Posn { [(i, info) | i <- [$2], info <- mkOverload Nothing (Just (mkL $1 $6 (mkAbs $3 (mkMarkup $5))))] }
| Posn LhsNames ':' Exp '=' ListMarkup2 Posn { [(i, info) | i <- $2, info <- mkOverload (Just (mkL $1 $7 $4)) (Just (mkL $1 $7 (mkMarkup $6)))] }
Markup :: { Term } Markup :: { Term }
Markup Markup
@@ -746,6 +747,10 @@ ListMarkup :: { [Term] }
| Exp { [$1] } | Exp { [$1] }
| Markup ListMarkup { $1 : $2 } | Markup ListMarkup { $1 : $2 }
ListMarkup2 :: { [Term] }
: Markup { [$1] }
| Markup ListMarkup2 { $1 : $2 }
Control :: { (Ident,Maybe Term) } Control :: { (Ident,Maybe Term) }
: Ident { ($1, Nothing) } : Ident { ($1, Nothing) }
| Ident ':' Exp6 { ($1, Just $3) } | Ident ':' Exp6 { ($1, Just $3) }
@@ -884,4 +889,7 @@ mkAlts cs = case cs of
mkL :: Posn -> Posn -> x -> L x mkL :: Posn -> Posn -> x -> L x
mkL (Pn l1 _) (Pn l2 _) x = L (Local l1 l2) x mkL (Pn l1 _) (Pn l2 _) x = L (Local l1 l2) x
mkMarkup [t] = t
mkMarkup ts = Markup identW [] ts
} }
src/compiler/api/GF/Grammar/Predef.hs
+6
View File
@@ -63,9 +63,15 @@ cError = identS "error"
-- * Used in the delimited continuations -- * Used in the delimited continuations
cConcat = identS "concat" cConcat = identS "concat"
cConcat' = identS "concat'"
cOne = identS "one" cOne = identS "one"
cSelect = identS "select"
cDefault = identS "default" cDefault = identS "default"
cList = identS "list" cList = identS "list"
cLen = identS "len"
cp1 = identS "p1"
cp2 = identS "p2"
-- * Hacks: dummy identifiers used in various places. -- * Hacks: dummy identifiers used in various places.
-- Not very nice! -- Not very nice!
src/compiler/api/GF/Grammar/Printer.hs
+6
View File
@@ -218,6 +218,9 @@ ppTerm q d (S x y) = case x of
'}' '}'
_ -> prec d 3 (hang (ppTerm q 3 x) 2 ("!" <+> ppTerm q 4 y)) _ -> prec d 3 (hang (ppTerm q 3 x) 2 ("!" <+> ppTerm q 4 y))
ppTerm q d (ExtR x y) = prec d 3 (ppTerm q 3 x <+> "**" <+> ppTerm q 4 y) ppTerm q d (ExtR x y) = prec d 3 (ppTerm q 3 x <+> "**" <+> ppTerm q 4 y)
ppTerm q d (Opts t opts) = "option" <+> ppTerm q 0 t <+>"of" <+> '{' $$
nest 2 (vcat (punctuate ';' (map (ppOpt q) opts))) $$
'}'
ppTerm q d (App x y) = prec d 4 (ppTerm q 4 x <+> ppTerm q 5 y) ppTerm q d (App x y) = prec d 4 (ppTerm q 4 x <+> ppTerm q 5 y)
ppTerm q d (V e es) = hang "table" 2 (sep [ppTerm q 6 e,brackets (fsep (punctuate ';' (map (ppTerm q 0) es)))]) ppTerm q d (V e es) = hang "table" 2 (sep [ppTerm q 6 e,brackets (fsep (punctuate ';' (map (ppTerm q 0) es)))])
ppTerm q d (FV es) = prec d 4 ("variants" <+> braces (fsep (punctuate ';' (map (ppTerm q 0) es)))) ppTerm q d (FV es) = prec d 4 ("variants" <+> braces (fsep (punctuate ';' (map (ppTerm q 0) es))))
@@ -269,6 +272,9 @@ ppEquation q (ps,e) = hcat (map (ppPatt q 2) ps) <+> "->" <+> ppTerm q 0 e
ppCase q (p,e) = ppPatt q 0 p <+> "=>" <+> ppTerm q 0 e ppCase q (p,e) = ppPatt q 0 p <+> "=>" <+> ppTerm q 0 e
ppOpt q (Just p, e) = ppTerm q 0 p <+> "=>" <+> ppTerm q 0 e
ppOpt q (Nothing,e) = ppTerm q 0 e
ppControl q (id,Nothing) = pp id ppControl q (id,Nothing) = pp id
ppControl q (id,Just t ) = pp id <> ':' <+> ppTerm q 6 t ppControl q (id,Just t ) = pp id <> ':' <+> ppTerm q 6 t