added the const control

This commit is contained in:
Krasimir Angelov
2025-10-16 09:20:21 +00:00
parent 6f3182d0cf
commit 6e529e74d9
3 changed files with 14 additions and 0 deletions
@@ -1004,6 +1004,11 @@ value2termM flat xs (VReset ctl mb_cv v mb_qid) = do
Just cv -> do g <- globals
value2termM True xs (apply g cv [VInt (genericLength ts)])
Nothing -> return (EInt (genericLength ts))
| ctl == cConst =
case mb_cv of
Just cv -> do ct <- value2termM flat xs cv
msum (map (pure . const ct) ts)
_ -> evalError (pp "[const: .. | ..] 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)
@@ -529,6 +529,14 @@ tcRho scope c (Reset ctl mb_ct t qid) mb_ty
(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
| ctl == cConst = do
let (c1,c2) = split c
(t,_) <- tcRho scope c1 t Nothing
(mb_ct,ty) <- case mb_ct of
Just ct -> do (ct,ty) <- tcRho scope c2 ct mb_ty
return (Just ct,ty)
Nothing -> evalError (pp "[list: .. | ..] requires an argument")
return (Reset ctl mb_ct t qid,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
+1
View File
@@ -73,6 +73,7 @@ cFilter = identS "filter"
cDefault = identS "default"
cList = identS "list"
cLen = identS "len"
cConst = identS "const"
cp1 = identS "p1"
cp2 = identS "p2"