1
0
forked from GitHub/gf-core

a draft for the generalized control operators

This commit is contained in:
Krasimir Angelov
2025-05-09 18:58:27 +02:00
parent 544bbd9049
commit 3d7c8ade17
11 changed files with 105 additions and 103 deletions

View File

@@ -287,10 +287,6 @@ eval env (Markup tag as ts) [] =
do as <- mapM (\(id,t) -> eval env t [] >>= \v -> return (id,v)) as
vs <- mapM (\t -> eval env t []) ts
return (VMarkup tag as vs)
eval env (Reset c t) [] = do let limit All = id
limit (Limit n) = fmap (genericTake n)
vs <- limit c (reset (eval env t []))
return (VMarkup identW [] vs)
eval env (TSymCat d r rs) []= do rs <- forM rs $ \(i,(pv,ty)) ->
case lookup pv env of
Just tnk -> return (i,(tnk,ty))

View File

@@ -86,7 +86,7 @@ data Value
| VAlts Value [(Value, Value)]
| VStrs [Value]
| VMarkup Ident [(Ident,Value)] [Value]
| VReset Control Value
| VReset Ident (Maybe Value) Value QIdent
| VSymCat Int LIndex [(LIndex, (Value, Type))]
| VError Doc
-- These two constructors are only used internally
@@ -124,7 +124,7 @@ isCanonicalForm False (VFV c vs) = all (isCanonicalForm False) (unvaria
isCanonicalForm flat (VAlts d vs) = all (isCanonicalForm flat . snd) vs
isCanonicalForm flat (VStrs vs) = all (isCanonicalForm flat) vs
isCanonicalForm flat (VMarkup tag as vs) = all (isCanonicalForm flat . snd) as && all (isCanonicalForm flat) vs
isCanonicalForm flat (VReset ctl v) = isCanonicalForm flat v
isCanonicalForm flat (VReset ctl cv v _) = maybe True (isCanonicalForm flat) cv && isCanonicalForm flat v
isCanonicalForm flat _ = False
data ConstValue a
@@ -324,7 +324,7 @@ eval g env c (Markup tag as ts) [] =
vas = mapC (\c (id,t) -> (id,eval g env c t [])) c1 as
vs = mapC (\c t -> eval g env c t []) c2 ts
in (VMarkup tag vas vs)
eval g env c (Reset ctl t) [] = VReset ctl (eval g env c t [])
eval g env c (Reset ctl mb_ct t qid) [] = VReset ctl (fmap (\t -> eval g env c t []) mb_ct) (eval g env c t []) qid
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@(Opts n cs) vs = if null cs
then VError ("No options in expression:" $$ ppTerm Unqualified 0 t)
@@ -422,7 +422,7 @@ bubble v = snd (bubble v)
let (union1,attrs') = mapAccumL descend' Map.empty attrs
(union2,vs') = mapAccumL descend union1 vs
in (union2, VMarkup tag attrs' vs')
bubble (VReset ctl v) = lift1 (VReset ctl) v
bubble (VReset ctl mb_cv v id) = lift1 (\v -> VReset ctl mb_cv v id) v
bubble (VSymCat d i0 vs) =
let (union,vs') = mapAccumL descendC Map.empty vs
in (union, addVariants (VSymCat d i0 vs') union)
@@ -932,26 +932,42 @@ value2termM flat xs (VMarkup tag as vs) = do
as <- mapM (\(id,v) -> value2termM flat xs v >>= \t -> return (id,t)) as
ts <- mapM (value2termM flat xs) vs
return (Markup tag as ts)
value2termM flat xs (VReset ctl v) = do
value2termM flat xs (VReset ctl mb_cv v qid) = 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)
reduce ctl mb_cv ts
where
reduce ctl mb_cv 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
[t] -> return t
ts -> return (Markup identW [] ts)
| ctl == cOne =
case (ts,mb_cv) of
([] ,Nothing) -> mzero
([] ,Just v) -> value2termM flat xs v
(t:ts,_) -> return t
| ctl == cDefault =
case (ts,mb_cv) of
([] ,Nothing) -> mzero
([] ,Just v) -> value2termM flat xs v
(ts,_) -> msum (map pure ts)
| ctl == cList =
case (ts,mb_cv) of
([], _) -> mzero
([t], _) -> return t
(ts,Just cv) ->
do let cat = showIdent (snd qid)
mn = fst qid
ct <- value2termM flat xs cv
t <- listify mn cat ts
return (App (App (QC (mn,identS ("Conj"++cat))) ct) t)
_ -> evalError (pp "[list: .. | ..] requires an argument")
| 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:ts) = do t2 <- listify mn cat ts
return (App (App (QC (mn,identS ("Cons"++cat))) t1) t2)

View File

@@ -238,21 +238,12 @@ renameTerm env vars = ren vars where
(p',_) <- renpatt 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
Reset ctl mb_ct t qid -> do
mv_ct <- case mb_ct of
Just ct -> liftM Just $ ren vs ct
Nothing -> return mb_ct
t <- ren vs t
return (Reset ctl t)
return (Reset ctl mv_ct t qid)
_ -> composOp (ren vs) trm

View File

@@ -370,21 +370,43 @@ tcRho scope c (Markup tag attrs children) mb_ty = do
c1 attrs
res <- mapCM (\c child -> tcRho scope c child Nothing) c2 children
instSigma scope c3 (Markup tag attrs (map fst res)) vtypeMarkup mb_ty
tcRho scope c (Reset ctl t) mb_ty =
let (c1,c2) = split c
in case ctl of
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 poison (mn,identS "Conj") []))
(t,ty) <- tcRho scope c2 t mb_ty
case ty of
VApp c id [] -> return (Reset (Coordination mb_mn conj (snd id)) t, ty)
_ -> evalError (pp "Needs atomic type"<+>ppValue Unqualified 0 ty)
tcRho scope c (Reset ctl mb_ct t qid) mb_ty
| ctl == cConcat = do
let (c1,c23) = split c
(c2,c3 ) = split c23
(t,_) <- tcRho scope c1 t Nothing
mb_ct <- case mb_ct of
Just ct -> do (ct,_) <- tcRho scope c2 ct (Just vtypeInt)
return (Just ct)
Nothing -> return Nothing
instSigma scope c2 (Reset ctl mb_ct t qid) vtypeMarkup mb_ty
| ctl == cOne = do
let (c1,c2) = split c
(t,ty) <- tcRho scope c1 t mb_ty
mb_ct <- case mb_ct of
Just ct -> do (ct,ty) <- tcRho scope c2 ct (Just ty)
return (Just ct)
Nothing -> return Nothing
return (Reset ctl mb_ct t qid,ty)
| ctl == cDefault = do
let (c1,c2) = split c
(t,ty) <- tcRho scope c1 t mb_ty
mb_ct <- case mb_ct of
Just ct -> do (ct,ty) <- tcRho scope c2 ct (Just ty)
return (Just ct)
Nothing -> evalError (pp "[list: .. | ..] requires an argument")
return (Reset ctl mb_ct t qid,ty)
| ctl == cList = do
do let (c1,c2) = split c
mb_ct <- case mb_ct of
Just ct -> do (ct,ty) <- tcRho scope c1 ct Nothing
return (Just ct)
Nothing -> evalError (pp "[list: .. | ..] requires an argument")
(t,ty) <- tcRho scope c2 t mb_ty
case ty of
VApp c qid [] -> return (Reset ctl mb_ct t qid, ty)
_ -> evalError (pp "Needs atomic type"<+>ppValue Unqualified 0 ty)
| otherwise = evalError (pp "Operator" <+> pp ctl <+> pp "is not defined")
tcRho scope s (Opts n cs) mb_ty = do
let (s1,s2,s3) = split3 s
(n,_) <- tcRho scope s1 n Nothing