mirror of
https://github.com/GrammaticalFramework/gf-core.git
synced 2026-04-23 03:32:51 -06:00
sketch an implementation for reset
This commit is contained in:
@@ -64,6 +64,7 @@ data Value
|
|||||||
| VAlts Value [(Value, Value)]
|
| VAlts Value [(Value, Value)]
|
||||||
| VStrs [Value]
|
| VStrs [Value]
|
||||||
| VMarkup Ident [(Ident,Value)] [Value]
|
| VMarkup Ident [(Ident,Value)] [Value]
|
||||||
|
| VReset Control Value
|
||||||
| VSymCat Int LIndex [(LIndex, (Value, Type))]
|
| VSymCat Int LIndex [(LIndex, (Value, Type))]
|
||||||
| VError Doc
|
| VError Doc
|
||||||
-- These two constructors are only used internally
|
-- These two constructors are only used internally
|
||||||
@@ -254,10 +255,7 @@ eval g env c (Markup tag as ts) [] =
|
|||||||
vas = mapC (\c (id,t) -> (id,eval g env c t [])) c1 as
|
vas = mapC (\c (id,t) -> (id,eval g env c t [])) c1 as
|
||||||
vs = mapC (\c t -> eval g env c t []) c2 ts
|
vs = mapC (\c t -> eval g env c t []) c2 ts
|
||||||
in (VMarkup tag vas vs)
|
in (VMarkup tag vas vs)
|
||||||
eval g env c (Reset ctl t) [] =
|
eval g env c (Reset ctl t) [] = VReset ctl (eval g env c t [])
|
||||||
let limit All = id
|
|
||||||
limit (Limit n) = fmap (genericTake n)
|
|
||||||
in (VMarkup identW [] [eval g env c t []])
|
|
||||||
eval g env c (TSymCat d r rs) []= VSymCat d r [(i,(fromJust (lookup pv env),ty)) | (i,(pv,ty)) <- rs]
|
eval g env c (TSymCat d r rs) []= VSymCat d r [(i,(fromJust (lookup pv env),ty)) | (i,(pv,ty)) <- rs]
|
||||||
eval g env c t vs = VError ("Cannot reduce term" <+> pp t)
|
eval g env c t vs = VError ("Cannot reduce term" <+> pp t)
|
||||||
|
|
||||||
@@ -325,6 +323,7 @@ bubble v = snd (bubble v)
|
|||||||
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 v) = lift1 (VReset ctl) v
|
||||||
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)
|
||||||
@@ -610,6 +609,14 @@ runEvalM g (EvalM f) = Check $ \(es,ws) ->
|
|||||||
where
|
where
|
||||||
empty = State Map.empty Map.empty
|
empty = State Map.empty Map.empty
|
||||||
|
|
||||||
|
reset :: EvalM a -> EvalM [a]
|
||||||
|
reset (EvalM f) = EvalM $ \g k state r ws ->
|
||||||
|
case f g (\x state xs ws -> Success (x:xs) ws) state [] ws of
|
||||||
|
Fail msg ws -> Fail msg ws
|
||||||
|
Success xs ws -> k (reverse xs) state r ws
|
||||||
|
where
|
||||||
|
empty = State Map.empty Map.empty
|
||||||
|
|
||||||
globals :: EvalM Globals
|
globals :: EvalM Globals
|
||||||
globals = EvalM (\g k -> k g)
|
globals = EvalM (\g k -> k g)
|
||||||
|
|
||||||
@@ -784,6 +791,29 @@ value2termM flat xs (VMarkup tag as vs) = do
|
|||||||
as <- mapM (\(id,v) -> value2termM flat xs v >>= \t -> return (id,t)) as
|
as <- mapM (\(id,v) -> value2termM flat xs v >>= \t -> return (id,t)) as
|
||||||
ts <- mapM (value2termM flat xs) vs
|
ts <- mapM (value2termM flat xs) vs
|
||||||
return (Markup tag as ts)
|
return (Markup tag as ts)
|
||||||
|
value2termM flat xs (VReset ctl v) = do
|
||||||
|
ts <- reset (value2termM True xs v)
|
||||||
|
case ctl of
|
||||||
|
All -> case ts of
|
||||||
|
[t] -> return t
|
||||||
|
ts -> return (Markup identW [] ts)
|
||||||
|
One -> case ts of
|
||||||
|
[] -> mzero
|
||||||
|
(t:ts) -> return t
|
||||||
|
Limit n -> case genericTake n ts of
|
||||||
|
[t] -> return t
|
||||||
|
ts -> return (Markup identW [] ts)
|
||||||
|
Coordination (Just mn) conj id ->
|
||||||
|
case ts of
|
||||||
|
[] -> mzero
|
||||||
|
[t] -> return t
|
||||||
|
ts -> do let cat = showIdent id
|
||||||
|
t <- listify mn cat ts
|
||||||
|
return (App (App (QC (mn,identS ("Conj"++cat))) (QC (mn,conj))) t)
|
||||||
|
where
|
||||||
|
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 id ts
|
||||||
|
return (App (App (QC (mn,identS ("Cons"++cat))) t1) t2)
|
||||||
value2termM flat xs (VError msg) = evalError msg
|
value2termM flat xs (VError msg) = evalError msg
|
||||||
value2termM flat xs (VCRecType lbls) = do
|
value2termM flat xs (VCRecType lbls) = do
|
||||||
lbls <- mapM (\(lbl,_,v) -> fmap ((,) lbl) (value2termM flat xs v)) lbls
|
lbls <- mapM (\(lbl,_,v) -> fmap ((,) lbl) (value2termM flat xs v)) lbls
|
||||||
|
|||||||
@@ -238,6 +238,22 @@ renameTerm env vars = ren vars where
|
|||||||
(p',_) <- renpatt p
|
(p',_) <- renpatt p
|
||||||
return $ EPatt minp maxp p'
|
return $ EPatt minp maxp p'
|
||||||
|
|
||||||
|
Reset ctl t -> do
|
||||||
|
ctl <- case ctl of
|
||||||
|
Coordination _ conj cat ->
|
||||||
|
checks [ do t <- renid' (Cn conj)
|
||||||
|
case t of
|
||||||
|
Q (mn,id) -> return (Coordination (Just mn) conj cat)
|
||||||
|
QC (mn,id) -> return (Coordination (Just mn) conj cat)
|
||||||
|
_ -> return (Coordination Nothing conj cat)
|
||||||
|
, if showIdent conj == "one"
|
||||||
|
then return One
|
||||||
|
else checkError ("Undefined control" <+> pp conj)
|
||||||
|
]
|
||||||
|
ctl -> do return ctl
|
||||||
|
t <- ren vs t
|
||||||
|
return (Reset ctl t)
|
||||||
|
|
||||||
_ -> composOp (ren vs) trm
|
_ -> composOp (ren vs) trm
|
||||||
|
|
||||||
renid = renameIdentTerm env
|
renid = renameIdentTerm env
|
||||||
|
|||||||
@@ -388,10 +388,21 @@ tcRho scope c (Markup tag attrs children) mb_ty = do
|
|||||||
c1 attrs
|
c1 attrs
|
||||||
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 t) mb_ty = do
|
tcRho scope c (Reset ctl t) mb_ty =
|
||||||
let (c1,c2) = split c
|
let (c1,c2) = split c
|
||||||
(t,_) <- tcRho scope c1 t Nothing
|
in case ctl of
|
||||||
instSigma scope c2 (Reset ctl t) vtypeMarkup mb_ty
|
All -> do (t,_) <- tcRho scope c1 t Nothing
|
||||||
|
instSigma scope c2 (Reset ctl t) vtypeMarkup mb_ty
|
||||||
|
One -> do (t,ty) <- tcRho scope c t mb_ty
|
||||||
|
return (Reset ctl t,ty)
|
||||||
|
Limit n -> do (t,_) <- tcRho scope c1 t Nothing
|
||||||
|
instSigma scope c2 (Reset ctl t) vtypeMarkup mb_ty
|
||||||
|
Coordination mb_mn@(Just mn) conj _
|
||||||
|
-> do tcRho scope c1 (QC (mn,conj)) (Just (VApp (mn,identS "Conj") []))
|
||||||
|
(t,ty) <- tcRho scope c2 t mb_ty
|
||||||
|
case ty of
|
||||||
|
VApp id [] -> return (Reset (Coordination mb_mn conj (snd id)) t, ty)
|
||||||
|
_ -> evalError (pp "Needs atomic type"<+>ppValue Unqualified 0 ty)
|
||||||
tcRho scope s t _ = unimplemented ("tcRho "++show t)
|
tcRho scope s t _ = unimplemented ("tcRho "++show t)
|
||||||
|
|
||||||
evalCodomain :: Scope -> Ident -> Value -> EvalM Value
|
evalCodomain :: Scope -> Ident -> Value -> EvalM Value
|
||||||
|
|||||||
@@ -407,7 +407,9 @@ data Term =
|
|||||||
|
|
||||||
data Control
|
data Control
|
||||||
= All
|
= All
|
||||||
|
| One
|
||||||
| Limit Integer
|
| Limit Integer
|
||||||
|
| Coordination (Maybe ModuleName) Ident Ident
|
||||||
deriving (Show, Eq, Ord)
|
deriving (Show, Eq, Ord)
|
||||||
|
|
||||||
-- | Patterns
|
-- | Patterns
|
||||||
|
|||||||
@@ -739,6 +739,7 @@ ListMarkup :: { [Term] }
|
|||||||
Control :: { Control }
|
Control :: { Control }
|
||||||
: { All }
|
: { All }
|
||||||
| Integer { Limit (fromIntegral $1) }
|
| Integer { Limit (fromIntegral $1) }
|
||||||
|
| Ident { Coordination Nothing $1 identW }
|
||||||
|
|
||||||
Attributes :: { [(Ident,Term)] }
|
Attributes :: { [(Ident,Term)] }
|
||||||
Attributes
|
Attributes
|
||||||
|
|||||||
@@ -256,8 +256,8 @@ ppTerm q d (Markup tag attrs children)
|
|||||||
| otherwise = pp "<" <> pp tag <+> hsep (map (ppMarkupAttr q) attrs) <> pp ">" $$
|
| otherwise = pp "<" <> pp tag <+> hsep (map (ppMarkupAttr q) attrs) <> pp ">" $$
|
||||||
nest 3 (ppMarkupChildren q children) $$
|
nest 3 (ppMarkupChildren q children) $$
|
||||||
pp "</" <> pp tag <> pp ">"
|
pp "</" <> pp tag <> pp ">"
|
||||||
ppTerm q d (Reset c t)
|
ppTerm q d (Reset ctl t)
|
||||||
= pp "[:" <> ppControl c <+> pp "|" <> ppTerm q 0 t <> pp "]"
|
= pp "[:" <> ppControl q ctl <+> pp "|" <> ppTerm q 0 t <> pp "]"
|
||||||
ppTerm q d (TSymCat i r rs) = pp '<' <> pp i <> pp ',' <> ppLinFun (pp.fst) r rs <> pp '>'
|
ppTerm q d (TSymCat i r rs) = pp '<' <> pp i <> pp ',' <> ppLinFun (pp.fst) r rs <> pp '>'
|
||||||
ppTerm q d (TSymVar i r) = pp '<' <> pp i <> pp ',' <> pp '$' <> pp r <> pp '>'
|
ppTerm q d (TSymVar i r) = pp '<' <> pp i <> pp ',' <> pp '$' <> pp r <> pp '>'
|
||||||
|
|
||||||
@@ -265,8 +265,12 @@ 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
|
||||||
|
|
||||||
ppControl All = empty
|
ppControl q All = empty
|
||||||
ppControl (Limit n) = pp n
|
ppControl q One = pp "one"
|
||||||
|
ppControl q (Limit n) = pp n
|
||||||
|
ppControl q (Coordination mb_mn n _) = ppTerm q 0 (case mb_mn of
|
||||||
|
Just mn -> QC (mn,n)
|
||||||
|
Nothing -> Cn n)
|
||||||
|
|
||||||
instance Pretty Patt where pp = ppPatt Unqualified 0
|
instance Pretty Patt where pp = ppPatt Unqualified 0
|
||||||
|
|
||||||
|
|||||||
Reference in New Issue
Block a user