generalize the filter function

This commit is contained in:
Krasimir Angelov committed 2026-10-15 15:09:07 +02:00
1 parent 44a7f1bf7a
commit 7b10bee627
2 files changed
+20 -5

No files matched your search

+13 -1
View File
@@ -1037,7 +1037,8 @@ value2termM flat xs (VReset ctl mb_cv v mb_qid) = do
select n (t:ts) = select (n-1) ts select n (t:ts) = select (n-1) ts
_ -> evalError (pp "[select: .. | ..] requires an integer constant") _ -> evalError (pp "[select: .. | ..] requires an integer constant")
| ctl == cFilter = | ctl == cFilter =
let filter [] = mzero case mb_cv of
Nothing -> let filter [] = mzero
filter (t:ts) = filter (t:ts) =
case t of case t of
R rs -> case (lookup (ident2label cp1) rs, lookup (ident2label cp2) rs) of R rs -> case (lookup (ident2label cp1) rs, lookup (ident2label cp2) rs) of
@@ -1046,6 +1047,11 @@ value2termM flat xs (VReset ctl mb_cv v mb_qid) = do
_ -> filter ts _ -> filter ts
_ -> evalError (pp "The term must be a record") _ -> evalError (pp "The term must be a record")
in filter ts in filter ts
Just cv -> do cts <- reset (value2termM True xs cv)
case ts \\ cts of
[] -> mzero
[t] -> return t
ts -> return (FV ts)
| ctl == cDefault = | ctl == cDefault =
case (ts,mb_cv) of case (ts,mb_cv) of
([] ,Nothing) -> mzero ([] ,Nothing) -> mzero
@@ -1054,6 +1060,12 @@ value2termM flat xs (VReset ctl mb_cv v mb_qid) = do
| ctl == cList = | ctl == cList =
case (ts,mb_cv) of case (ts,mb_cv) of
([], _) -> mzero ([], _) -> mzero
([FV ts],Just cv) ->
do let Just (mn,id) = mb_qid
cat = showIdent id
ct <- value2termM flat xs cv
t <- listify mn cat ts
return (App (App (QC (mn,identS ("Conj"++cat))) ct) t)
([t], _) -> return t ([t], _) -> return t
(ts,Just cv) -> (ts,Just cv) ->
do let Just (mn,id) = mb_qid do let Just (mn,id) = mb_qid
+7 -4
View File
@@ -526,7 +526,13 @@ tcRho scope c (Reset ctl mb_ct t qid) mb_ty
Nothing -> evalError (pp "[select: .. | ..] requires an integer argument") Nothing -> evalError (pp "[select: .. | ..] requires an integer argument")
(t,_) <- tcRho scope c1 t (Just rec_ty) (t,_) <- tcRho scope c1 t (Just rec_ty)
return (Reset ctl mb_ct t qid,ty) return (Reset ctl mb_ct t qid,ty)
| ctl == cFilter = concreteOnly "Control operators" $ do | ctl == cFilter = concreteOnly "Control operators" $
case mb_ct of
Just ct -> do
(ct,ty) <- tcRho scope c ct mb_ty
(t, ty) <- tcRho scope c t (Just ty)
return (Reset ctl (Just ct) t qid,ty)
Nothing -> do
ty <- case mb_ty of ty <- case mb_ty of
Just ty -> return ty Just ty -> return ty
Nothing -> do i <- newResiduation scope Nothing -> do i <- newResiduation scope
@@ -534,9 +540,6 @@ tcRho scope c (Reset ctl mb_ct t qid) mb_ty
let rec_ty = VRecType [ (ident2label cp1, True, ty) let rec_ty = VRecType [ (ident2label cp1, True, ty)
, (ident2label cp2, True, VApp (cPredef,cBool) []) , (ident2label cp2, True, VApp (cPredef,cBool) [])
] False ] False
case mb_ct of
Just ct -> evalError (pp "[filter | ..] cannot take an argument")
Nothing -> return ()
(t,_) <- tcRho scope c t (Just rec_ty) (t,_) <- tcRho scope c t (Just rec_ty)
return (Reset ctl mb_ct t qid,ty) return (Reset ctl mb_ct t qid,ty)
| ctl == cDefault = concreteOnly "Control operators" $ do | ctl == cDefault = concreteOnly "Control operators" $ do