a simple selection operation

This commit is contained in:
Krasimir Angelov
2025-06-11 08:48:04 +00:00
parent b993931820
commit 4c8549d6dd
3 changed files with 40 additions and 0 deletions
@@ -959,6 +959,22 @@ value2termM flat xs (VReset ctl mb_cv v mb_qid) = do
([] ,Nothing) -> mzero
([] ,Just v) -> value2termM flat xs v
(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 =
case (ts,mb_cv) of
([] ,Nothing) -> mzero
@@ -985,6 +1001,11 @@ value2termM flat xs (VReset ctl mb_cv v mb_qid) = do
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)
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 (VCRecType lbls) = do
lbls <- mapM (\(lbl,_,v) -> fmap ((,) lbl) (value2termM flat xs v)) lbls
@@ -396,6 +396,21 @@ tcRho scope c (Reset ctl mb_ct t qid) mb_ty
return (Just ct,ty)
Nothing -> return (Nothing,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, ty)
, (ident2label cp2, VSort cStr)
]
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
let (c1,c2) = split c
(t,ty) <- tcRho scope c1 t mb_ty
+4
View File
@@ -65,10 +65,14 @@ cError = identS "error"
cConcat = identS "concat"
cConcat' = identS "concat'"
cOne = identS "one"
cSelect = identS "select"
cDefault = identS "default"
cList = identS "list"
cLen = identS "len"
cp1 = identS "p1"
cp2 = identS "p2"
-- * Hacks: dummy identifiers used in various places.
-- Not very nice!