improve the syntax for options

This commit is contained in:
Krasimir Angelov
2025-08-19 18:01:37 +02:00
parent 1a512473cd
commit cbac8b4fd2
6 changed files with 34 additions and 21 deletions
@@ -94,7 +94,7 @@ data Value
data Variants
= VarFree [Value]
| VarOpts Value [(Value, Value)]
| VarOpts Value [(Maybe Value, Value)]
mapVariants :: (Value -> Value) -> Variants -> Variants
mapVariants f (VarFree vs) = VarFree (f <$> vs)
@@ -138,7 +138,7 @@ data ConstValue a
data ConstVariants a
= ConstFree [ConstValue a]
| ConstOpts Value [(Value, ConstValue a)]
| ConstOpts Value [(Maybe Value, ConstValue a)]
mapConstVs :: (ConstValue a -> ConstValue b) -> ConstVariants a -> ConstVariants b
mapConstVs f (ConstFree vs) = ConstFree (f <$> vs)
@@ -337,7 +337,8 @@ eval g env c t@(Opts n cs) vs = if null cs
vn = eval g env c1 n []
vcs = mapC evalOpt c cs
in VFV c3 (VarOpts vn vcs)
where evalOpt c' (l,t) = let (c1,c2) = split c' in (eval g env c1 l [], eval g env c2 t vs)
where evalOpt c' (Just l, t) = let (c1,c2) = split c' in (Just (eval g env c1 l []), eval g env c2 t vs)
evalOpt c' (Nothing,t) = let (c1,c2) = split c' in (Nothing, eval g env c2 t vs)
eval g env c t vs = VError ("Cannot reduce term" <+> pp t)
evalPredef :: Globals -> Choice -> Ident -> [Value] -> Value
@@ -423,7 +424,7 @@ bubble v = snd (bubble v)
bubble v@(VFV c (VarOpts n os))
| null os = (Map.empty, v)
| otherwise = let (union,os') = mapAccumL (\acc (k,v) -> second (k,) $ descend acc v) Map.empty os
in (Map.insert c (BubbleOpts n (fst <$> os),1) union, VFV c (VarOpts n os'))
in (Map.insert c (BubbleOpts n (map (\(l,t) -> fromMaybe t l) os),1) union, VFV c (VarOpts n os'))
bubble (VAlts v vs) = lift1L2 VAlts v vs
bubble (VStrs vs) = liftL VStrs vs
bubble (VMarkup tag attrs vs) =
@@ -508,7 +509,7 @@ bubble v = snd (bubble v)
addVariant c (bvs,cnt) v
| cnt > 1 = VFV c $ case bvs of
BubbleFree k -> VarFree (replicate k v)
BubbleOpts n os -> VarOpts n ((,v) <$> os)
BubbleOpts n os -> VarOpts n (map (\l -> (Just l,v)) os)
| otherwise = v
unitfy = fmap (\(n,_) -> (n,1))
@@ -924,7 +925,7 @@ value2termM flat xs (VFV i (VarOpts n os)) =
let j = fromMaybe 0 (Map.lookup i choices)
in case os `maybeAt` j of
Just (l,t) -> case value2termM flat xs t of
EvalM f -> let oi = OptionInfo i n (fst <$> os)
EvalM f -> let oi = OptionInfo i n (map (\(l,t) -> fromMaybe t l) os)
in f g k (State choices metas (oi:opts)) r msgs
Nothing -> Fail ("Index" <+> j <+> "out of bounds for option:" $$ ppValue Unqualified 0 n) msgs
value2termM flat xs (VPatt min max p) = return (EPatt min max p)
@@ -520,7 +520,7 @@ tcRho scope c (Reset ctl mb_ct t qid) mb_ty
tcRho scope s (Opts n cs) mb_ty = do
let (s1,s2,s3) = split3 s
(n,_) <- tcRho scope s1 n Nothing
(ls,_) <- tcUnifying scope s2 (fst <$> cs) Nothing
(ls,_) <- tcUnifyingMaybe scope s2 (fst <$> cs) Nothing
(ts,ty) <- tcUnifying scope s3 (snd <$> cs) mb_ty
return (Opts n (zip ls ts), ty)
tcRho scope s t _ = unimplemented ("tcRho "++show t)
@@ -546,6 +546,22 @@ tcUnifying scope c ts mb_ty = do
ts <- mapCM go c ts
return (ts,ty)
tcUnifyingMaybe :: Scope -> Choice -> [Maybe Term] -> Maybe Rho -> EvalM ([Maybe Term], Value)
tcUnifyingMaybe scope c ts mb_ty = do
(ty,subsume) <-
case mb_ty of
Just ty -> do return (ty, \t ty' -> return t)
Nothing -> do i <- newResiduation scope
let ty = VMeta i []
return (ty, \t ty' -> subsCheckRho scope t ty' ty >>= \(t,_,_) -> return t)
let go c (Just t) = do (t, ty) <- tcRho scope c t mb_ty
fmap Just $ subsume t ty
go c Nothing = do return Nothing
ts <- mapCM go c ts
return (ts,ty)
tcCases scope c [] (Just p_ty) (Just res_ty) = return ([],p_ty,res_ty)
tcCases scope c ((p,t):cs) mb_p_ty mb_res_ty = do
let (c1,c2,c3,c4) = split4 c
+1 -1
View File
@@ -466,7 +466,7 @@ type Equation = ([Patt],Term)
type Labelling = (Label, Type)
type Assign = (Label, (Maybe Type, Term))
type Option = (Term, Term)
type Option = (Maybe Term, Term)
type Case = (Patt, Term)
--type Cases = ([Patt], Term)
type LocalDef = (Ident, (Maybe Type, Term))
+2 -2
View File
@@ -404,7 +404,7 @@ composOp co trm =
RecType r -> liftM RecType (mapPairsM co r)
P t i -> liftM2 P (co t) (return i)
ExtR a c -> liftM2 ExtR (co a) (co c)
Opts t os -> liftM2 Opts (co t) (mapM (pairM co) os)
Opts t os -> liftM2 Opts (co t) (mapM (\(t1,t2) -> liftM2 (,) (maybe (return Nothing) (liftM Just . co) t1) (co t2)) os)
T i cc -> liftM2 (flip T) (mapPairsM co cc) (changeTableType co i)
V ty vs -> liftM2 V (co ty) (mapM co vs)
Let (x,(mt,a)) b -> liftM3 let' (co a) (T.mapM co mt) (co b)
@@ -451,7 +451,7 @@ collectOp co trm = case trm of
S c a -> co c <> co a
Table a c -> co a <> co c
ExtR a c -> co a <> co c
Opts t os -> co t <> mconcatMap (\(a,b) -> co a <> co b) os
Opts t os -> co t <> mconcatMap (\(a,b) -> maybe mempty co a <> co b) os
R r -> mconcatMap (\ (_,(mt,a)) -> maybe mempty co mt <> co a) r
RecType r -> mconcatMap (co . snd) r
P t i -> co t
+5 -10
View File
@@ -452,7 +452,11 @@ Exp4 :: { Term }
Exp4
: Exp4 Exp5 { App $1 $2 }
| Exp4 '{' Exp '}' { App $1 (ImplArg $3) }
| 'option' Exp 'of' '{' ListOpt '}' { Opts $2 $5 }
| 'option' Exp 'of' '{' ListExp '}' { let toOption t =
case t of
Table x y -> (Just x, y)
y -> (Nothing, y)
in Opts $2 (map toOption $5) }
| 'case' Exp 'of' '{' ListCase '}' { let annot = case $2 of
Typed _ t -> TTyped t
_ -> TRaw
@@ -608,15 +612,6 @@ ListPattTupleComp
| Patt { [$1] }
| Patt ',' ListPattTupleComp { $1 : $3 }
Opt :: { Option }
Opt
: '(' Exp ')' '=>' Exp { ($2,$5) }
ListOpt :: { [Option] }
ListOpt
: Opt { [$1] }
| Opt ';' ListOpt { $1 : $3 }
Case :: { Case }
Case
: Patt '=>' Exp { ($1,$3) }
+2 -1
View File
@@ -272,7 +272,8 @@ 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
ppOpt q (p,e) = '(' <> ppTerm q 0 p <> ')' <+> "=>" <+> ppTerm q 0 e
ppOpt q (Just p, e) = ppTerm q 0 p <+> "=>" <+> ppTerm q 0 e
ppOpt q (Nothing,e) = ppTerm q 0 e
ppControl q (id,Nothing) = pp id
ppControl q (id,Just t ) = pp id <> ':' <+> ppTerm q 6 t