mirror of
https://github.com/unisonweb/unison.git
synced 2024-10-04 13:47:26 +03:00
Merge pull request #2432 from unisonweb/topic/letblockparen
Add parens around let blocks, fix delayed effect parser
This commit is contained in:
commit
fdc6e8d382
@ -1,6 +1,7 @@
|
||||
{-# LANGUAGE OverloadedStrings #-}
|
||||
{-# LANGUAGE TypeFamilies #-}
|
||||
{-# LANGUAGE ViewPatterns #-}
|
||||
{-# LANGUAGE DeriveAnyClass #-}
|
||||
|
||||
module Unison.Parser where
|
||||
|
||||
@ -53,6 +54,7 @@ import qualified Unison.Hashable as Hashable
|
||||
import Unison.Referent (Referent)
|
||||
import Unison.Reference (Reference)
|
||||
import Unison.Parser.Ann (Ann(..))
|
||||
import Text.Megaparsec.Error (ShowErrorComponent)
|
||||
|
||||
debug :: Bool
|
||||
debug = False
|
||||
@ -125,6 +127,9 @@ data Error v
|
||||
| FloatPattern Ann
|
||||
deriving (Show, Eq, Ord)
|
||||
|
||||
instance (Ord v, Show v) => ShowErrorComponent (Error v) where
|
||||
showErrorComponent e = show e
|
||||
|
||||
tokenToPair :: L.Token a -> (Ann, a)
|
||||
tokenToPair t = (ann t, L.payload t)
|
||||
|
||||
|
@ -87,20 +87,20 @@ data BlockContext
|
||||
-- This ABT node is at the top level of a TermParser.block.
|
||||
= Block
|
||||
| Normal
|
||||
deriving (Eq)
|
||||
deriving (Eq, Show)
|
||||
|
||||
data InfixContext
|
||||
-- This ABT node is an infix operator being used in infix position.
|
||||
= Infix
|
||||
| NonInfix
|
||||
deriving (Eq)
|
||||
deriving (Eq, Show)
|
||||
|
||||
data DocLiteralContext
|
||||
-- We won't try and render this ABT node or anything under it as a [: @Doc literal :]
|
||||
= NoDoc
|
||||
-- We'll keep checking as we recurse down
|
||||
| MaybeDoc
|
||||
deriving (Eq)
|
||||
deriving (Eq, Show)
|
||||
|
||||
{- Explanation of precedence handling
|
||||
|
||||
@ -238,9 +238,13 @@ pretty0
|
||||
pblock tm = let (im', uses) = calcImports im tm
|
||||
in uses $ [pretty0 n (ac 0 Block im' doc) tm]
|
||||
App' x (Constructor' DD.UnitRef 0) ->
|
||||
paren (p >= 11) $ (fmt S.DelayForceChar $ l "!") <> pretty0 n (ac 11 Normal im doc) x
|
||||
Delay' x ->
|
||||
paren (p >= 11) $ (fmt S.DelayForceChar $ l "'") <> pretty0 n (ac 11 Normal im doc) x
|
||||
paren (p >= 11 || isBlock x && p >= 3) $
|
||||
fmt S.DelayForceChar (l "!")
|
||||
<> pretty0 n (ac (if isBlock x then 0 else 10) Normal im doc) x
|
||||
Delay' x ->
|
||||
paren (p >= 11 || isBlock x && p >= 3) $
|
||||
fmt S.DelayForceChar (l "'")
|
||||
<> pretty0 n (ac (if isBlock x then 0 else 10) Normal im doc) x
|
||||
List' xs -> PP.group $
|
||||
(fmt S.DelimiterChar $ l "[") <> optSpace
|
||||
<> intercalateMap ((fmt S.DelimiterChar $ l ",") <> PP.softbreak <> optSpace <> optSpace)
|
||||
@ -421,7 +425,7 @@ pretty0
|
||||
_ -> undefined
|
||||
ps = join $ [ r a f | (a, f) <- reverse xs ]
|
||||
r a f =
|
||||
[ pretty0 n (ac 3 Normal im doc) a
|
||||
[ pretty0 n (ac (if isBlock a then 12 else 3) Normal im doc) a
|
||||
, pretty0 n (AmbientContext 10 Normal Infix im doc False) f
|
||||
]
|
||||
|
||||
@ -1176,6 +1180,15 @@ isDestructuringBind scrutinee [MatchCase pat _ (ABT.AbsN' vs _)]
|
||||
Pattern.Unbound _ -> False
|
||||
isDestructuringBind _ _ = False
|
||||
|
||||
isBlock :: Ord v => Term2 vt at ap v a -> Bool
|
||||
isBlock tm =
|
||||
case tm of
|
||||
If' _ _ _ -> True
|
||||
Handle' _ _ -> True
|
||||
Match' _ _ -> True
|
||||
LetBlock _ _ -> True
|
||||
_ -> False
|
||||
|
||||
pattern LetBlock bindings body <- (unLetBlock -> Just (bindings, body))
|
||||
|
||||
-- Collects nested let/let rec blocks into one minimally nested block.
|
||||
|
@ -72,7 +72,7 @@ type2 = do
|
||||
effect :: Var v => TypeP v
|
||||
effect = do
|
||||
es <- effectList
|
||||
t <- valueTypeLeaf
|
||||
t <- type2
|
||||
pure (Type.effect1 (ann es <> ann t) es t)
|
||||
|
||||
effectList :: Var v => TypeP v
|
||||
|
@ -109,37 +109,37 @@ prettyRaw n im p tp = go n im p tp
|
||||
EffectfulArrows' fst rest ->
|
||||
case fst of
|
||||
Var' v | Var.name v == "()" ->
|
||||
PP.parenthesizeIf (p >= 10) $
|
||||
fmt S.DelayForceChar "'" <> arrows False True rest
|
||||
PP.parenthesizeIf (p >= 10) $ arrows True True rest
|
||||
_ -> PP.parenthesizeIf (p >= 0) $
|
||||
go n im 0 fst <> arrows False False rest
|
||||
_ -> "error"
|
||||
_ -> "error"
|
||||
effects Nothing = mempty
|
||||
effects (Just es) = PP.group $ (fmt S.AbilityBraces "{") <> PP.commas (go n im 0 <$> es) <> (fmt S.AbilityBraces "}")
|
||||
effects (Just es) = PP.group $ fmt S.AbilityBraces "{" <> PP.commas (go n im 0 <$> es) <> (fmt S.AbilityBraces "}")
|
||||
-- `first`: is this the first argument?
|
||||
-- `mes`: list of effects
|
||||
arrow delay first mes =
|
||||
(if first then mempty else PP.softbreak <> (fmt S.TypeOperator "->"))
|
||||
<> (if delay then (if first then (fmt S.DelayForceChar "'") else (fmt S.DelayForceChar " '")) else mempty)
|
||||
(if first then mempty else PP.softbreak <> fmt S.TypeOperator "->")
|
||||
<> (if delay then (if first then fmt S.DelayForceChar "'" else fmt S.DelayForceChar " '") else mempty)
|
||||
<> effects mes
|
||||
<> if (isJust mes) || (not delay) && (not first) then " " else mempty
|
||||
<> if isJust mes || not delay && not first then " " else mempty
|
||||
|
||||
arrows delay first [(mes, Ref' DD.UnitRef)] = arrow delay first mes <> (fmt S.Unit "()")
|
||||
arrows delay first [(mes, Ref' DD.UnitRef)] = arrow delay first mes <> fmt S.Unit "()"
|
||||
arrows delay first ((mes, Ref' DD.UnitRef) : rest) =
|
||||
arrow delay first mes <> (parenNoGroup delay $ arrows True True rest)
|
||||
arrow delay first mes <> parenNoGroup delay (arrows True True rest)
|
||||
arrows delay first ((mes, arg) : rest) =
|
||||
arrow delay first mes
|
||||
<> ( parenNoGroup (delay && (not $ null rest))
|
||||
$ go n im 0 arg
|
||||
<> arrows False False rest
|
||||
)
|
||||
arrow delay first mes <> parenNoGroup
|
||||
(delay && not (null rest))
|
||||
(go n im 0 arg <> arrows False False rest)
|
||||
|
||||
arrows False False [] = mempty
|
||||
arrows False True [] = mempty -- not reachable
|
||||
arrows True _ [] = mempty -- not reachable
|
||||
|
||||
paren True s = PP.group $ ( fmt S.Parenthesis "(" ) <> s <> ( fmt S.Parenthesis ")" )
|
||||
paren True s = PP.group $ fmt S.Parenthesis "(" <> s <> fmt S.Parenthesis ")"
|
||||
paren False s = PP.group s
|
||||
|
||||
parenNoGroup True s = ( fmt S.Parenthesis "(" ) <> s <> ( fmt S.Parenthesis ")" )
|
||||
parenNoGroup True s = fmt S.Parenthesis "(" <> s <> fmt S.Parenthesis ")"
|
||||
parenNoGroup False s = s
|
||||
|
||||
fmt :: S.Element r -> Pretty (S.SyntaxText' r) -> Pretty (S.SyntaxText' r)
|
||||
|
@ -344,13 +344,13 @@ test = scope "termprinter" $ tests
|
||||
, tc "!f a"
|
||||
, tcDiff "f () a ()" "!(!f a)"
|
||||
, tcDiff "f a b ()" "!(f a b)"
|
||||
, tcDiff "!f ()" "!(!f)"
|
||||
, tc "!(!foo)"
|
||||
, tcDiff "!f ()" "!!f"
|
||||
, tcDiff "!(!foo)" "!!foo"
|
||||
, tc "'bar"
|
||||
, tc "'(bar a b)"
|
||||
, tc "'('bar)"
|
||||
, tc "!('bar)"
|
||||
, tc "'(!foo)"
|
||||
, tcDiff "'('bar)" "''bar"
|
||||
, tcDiff "!('bar)" "!'bar"
|
||||
, tcDiff "'(!foo)" "'!foo"
|
||||
, tc "x -> '(y -> 'z)"
|
||||
, tc "'(x -> '(y -> z))"
|
||||
, tc "(\"a\", 2)"
|
||||
|
@ -443,7 +443,6 @@ unDelay tm = case ABT.out tm of
|
||||
| Set.notMember v (ABT.freeVars body)
|
||||
-> Just body
|
||||
_ -> Nothing
|
||||
|
||||
pattern LamNamed' v body <- (ABT.out -> ABT.Tm (Lam (ABT.Term _ _ (ABT.Abs v body))))
|
||||
pattern LamsNamed' vs body <- (unLams' -> Just (vs, body))
|
||||
pattern LamsNamedOpt' vs body <- (unLamsOpt' -> Just (vs, body))
|
||||
|
@ -114,7 +114,7 @@ Regression test for https://github.com/unisonweb/unison/issues/2392
|
||||
|
||||
```unison:hide
|
||||
unique ability Zonk where zonk : Nat
|
||||
unique type Foo x y =
|
||||
unique type Foo x y =
|
||||
|
||||
foo : Nat -> Foo ('{Zonk} a) ('{Zonk} b) -> Nat
|
||||
foo n _ = n
|
||||
@ -170,3 +170,45 @@ myDoc = {{ **my text** __my text__ **MY_TEXT** ___MY__TEXT___ ~~MY~TEXT~~ **MY*T
|
||||
.> load scratch.u
|
||||
```
|
||||
|
||||
## Parenthesized let-block with operator
|
||||
|
||||
Regression test for https://github.com/unisonweb/unison/issues/1778
|
||||
|
||||
```unison:hide
|
||||
|
||||
structural ability base.Abort where
|
||||
abort : a
|
||||
|
||||
(|>) : a -> (a ->{e} b) -> {e} b
|
||||
a |> f = f a
|
||||
|
||||
handler : a -> Request {Abort} a -> a
|
||||
handler default = cases
|
||||
{ a } -> a
|
||||
{abort -> _} -> default
|
||||
|
||||
Abort.toOptional : '{g, Abort} a -> '{g} Optional a
|
||||
Abort.toOptional thunk = '(toOptional! thunk)
|
||||
|
||||
Abort.toOptional! : '{g, Abort} a ->{g} (Optional a)
|
||||
Abort.toOptional! thunk = toDefault! None '(Some !thunk)
|
||||
|
||||
Abort.toDefault! : a -> '{g, Abort} a ->{g} a
|
||||
Abort.toDefault! default thunk =
|
||||
h x = Abort.toDefault! (handler default x) thunk
|
||||
handle (thunk ()) with h
|
||||
|
||||
x = '(let
|
||||
abort
|
||||
0) |> Abort.toOptional
|
||||
```
|
||||
|
||||
```ucm
|
||||
.> add
|
||||
.> edit x base.Abort |> handler Abort.toOptional Abort.toOptional! Abort.toDefault!
|
||||
.> undo
|
||||
```
|
||||
|
||||
``` ucm
|
||||
.> load scratch.u
|
||||
```
|
||||
|
@ -34,15 +34,15 @@ x = 1 + 1
|
||||
most recent, along with the command that got us there. Try:
|
||||
|
||||
`fork 2 .old`
|
||||
`fork #bt17giel42 .old` to make an old namespace
|
||||
`fork #m41m2ql36i .old` to make an old namespace
|
||||
accessible again,
|
||||
|
||||
`reset-root #bt17giel42` to reset the root namespace and
|
||||
`reset-root #m41m2ql36i` to reset the root namespace and
|
||||
its history to that of the
|
||||
specified namespace.
|
||||
|
||||
1. #agadr8gg6g : add
|
||||
2. #bt17giel42 : builtins.mergeio
|
||||
1. #j1vrihj69n : add
|
||||
2. #m41m2ql36i : builtins.mergeio
|
||||
3. #sjg2v58vn2 : (initial reflogged namespace)
|
||||
|
||||
.> reset-root 2
|
||||
@ -116,17 +116,17 @@ Without the above stanza, the `edit` will send the definition to the most recent
|
||||
most recent, along with the command that got us there. Try:
|
||||
|
||||
`fork 2 .old`
|
||||
`fork #bt17giel42 .old` to make an old namespace
|
||||
`fork #m41m2ql36i .old` to make an old namespace
|
||||
accessible again,
|
||||
|
||||
`reset-root #bt17giel42` to reset the root namespace and
|
||||
`reset-root #m41m2ql36i` to reset the root namespace and
|
||||
its history to that of the
|
||||
specified namespace.
|
||||
|
||||
1. #rhf1s808fb : add
|
||||
2. #bt17giel42 : reset-root #bt17giel42
|
||||
3. #agadr8gg6g : add
|
||||
4. #bt17giel42 : builtins.mergeio
|
||||
1. #sb99mm43ni : add
|
||||
2. #m41m2ql36i : reset-root #m41m2ql36i
|
||||
3. #j1vrihj69n : add
|
||||
4. #m41m2ql36i : builtins.mergeio
|
||||
5. #sjg2v58vn2 : (initial reflogged namespace)
|
||||
|
||||
.> reset-root 2
|
||||
@ -191,19 +191,19 @@ f x = let
|
||||
most recent, along with the command that got us there. Try:
|
||||
|
||||
`fork 2 .old`
|
||||
`fork #bt17giel42 .old` to make an old namespace
|
||||
`fork #m41m2ql36i .old` to make an old namespace
|
||||
accessible again,
|
||||
|
||||
`reset-root #bt17giel42` to reset the root namespace and
|
||||
`reset-root #m41m2ql36i` to reset the root namespace and
|
||||
its history to that of the
|
||||
specified namespace.
|
||||
|
||||
1. #gj5agagj7s : add
|
||||
2. #bt17giel42 : reset-root #bt17giel42
|
||||
3. #rhf1s808fb : add
|
||||
4. #bt17giel42 : reset-root #bt17giel42
|
||||
5. #agadr8gg6g : add
|
||||
6. #bt17giel42 : builtins.mergeio
|
||||
1. #t22r3l1hsh : add
|
||||
2. #m41m2ql36i : reset-root #m41m2ql36i
|
||||
3. #sb99mm43ni : add
|
||||
4. #m41m2ql36i : reset-root #m41m2ql36i
|
||||
5. #j1vrihj69n : add
|
||||
6. #m41m2ql36i : builtins.mergeio
|
||||
7. #sjg2v58vn2 : (initial reflogged namespace)
|
||||
|
||||
.> reset-root 2
|
||||
@ -273,21 +273,21 @@ h xs = match xs with
|
||||
most recent, along with the command that got us there. Try:
|
||||
|
||||
`fork 2 .old`
|
||||
`fork #bt17giel42 .old` to make an old namespace
|
||||
`fork #m41m2ql36i .old` to make an old namespace
|
||||
accessible again,
|
||||
|
||||
`reset-root #bt17giel42` to reset the root namespace and
|
||||
`reset-root #m41m2ql36i` to reset the root namespace and
|
||||
its history to that of the
|
||||
specified namespace.
|
||||
|
||||
1. #3igmh2it4p : add
|
||||
2. #bt17giel42 : reset-root #bt17giel42
|
||||
3. #gj5agagj7s : add
|
||||
4. #bt17giel42 : reset-root #bt17giel42
|
||||
5. #rhf1s808fb : add
|
||||
6. #bt17giel42 : reset-root #bt17giel42
|
||||
7. #agadr8gg6g : add
|
||||
8. #bt17giel42 : builtins.mergeio
|
||||
1. #ebh8598vf0 : add
|
||||
2. #m41m2ql36i : reset-root #m41m2ql36i
|
||||
3. #t22r3l1hsh : add
|
||||
4. #m41m2ql36i : reset-root #m41m2ql36i
|
||||
5. #sb99mm43ni : add
|
||||
6. #m41m2ql36i : reset-root #m41m2ql36i
|
||||
7. #j1vrihj69n : add
|
||||
8. #m41m2ql36i : builtins.mergeio
|
||||
9. #sjg2v58vn2 : (initial reflogged namespace)
|
||||
|
||||
.> reset-root 2
|
||||
@ -314,7 +314,7 @@ Regression test for https://github.com/unisonweb/unison/issues/2392
|
||||
|
||||
```unison
|
||||
unique ability Zonk where zonk : Nat
|
||||
unique type Foo x y =
|
||||
unique type Foo x y =
|
||||
|
||||
foo : Nat -> Foo ('{Zonk} a) ('{Zonk} b) -> Nat
|
||||
foo n _ = n
|
||||
@ -353,23 +353,23 @@ foo n _ = n
|
||||
most recent, along with the command that got us there. Try:
|
||||
|
||||
`fork 2 .old`
|
||||
`fork #bt17giel42 .old` to make an old namespace
|
||||
`fork #m41m2ql36i .old` to make an old namespace
|
||||
accessible again,
|
||||
|
||||
`reset-root #bt17giel42` to reset the root namespace and
|
||||
`reset-root #m41m2ql36i` to reset the root namespace and
|
||||
its history to that of the
|
||||
specified namespace.
|
||||
|
||||
1. #jsnoueu9le : add
|
||||
2. #bt17giel42 : reset-root #bt17giel42
|
||||
3. #3igmh2it4p : add
|
||||
4. #bt17giel42 : reset-root #bt17giel42
|
||||
5. #gj5agagj7s : add
|
||||
6. #bt17giel42 : reset-root #bt17giel42
|
||||
7. #rhf1s808fb : add
|
||||
8. #bt17giel42 : reset-root #bt17giel42
|
||||
9. #agadr8gg6g : add
|
||||
10. #bt17giel42 : builtins.mergeio
|
||||
1. #siglm9vcnk : add
|
||||
2. #m41m2ql36i : reset-root #m41m2ql36i
|
||||
3. #ebh8598vf0 : add
|
||||
4. #m41m2ql36i : reset-root #m41m2ql36i
|
||||
5. #t22r3l1hsh : add
|
||||
6. #m41m2ql36i : reset-root #m41m2ql36i
|
||||
7. #sb99mm43ni : add
|
||||
8. #m41m2ql36i : reset-root #m41m2ql36i
|
||||
9. #j1vrihj69n : add
|
||||
10. #m41m2ql36i : builtins.mergeio
|
||||
11. #sjg2v58vn2 : (initial reflogged namespace)
|
||||
|
||||
.> reset-root 2
|
||||
@ -432,25 +432,25 @@ foo =
|
||||
most recent, along with the command that got us there. Try:
|
||||
|
||||
`fork 2 .old`
|
||||
`fork #bt17giel42 .old` to make an old namespace
|
||||
`fork #m41m2ql36i .old` to make an old namespace
|
||||
accessible again,
|
||||
|
||||
`reset-root #bt17giel42` to reset the root namespace and
|
||||
`reset-root #m41m2ql36i` to reset the root namespace and
|
||||
its history to that of the
|
||||
specified namespace.
|
||||
|
||||
1. #vbmanbqtlh : add
|
||||
2. #bt17giel42 : reset-root #bt17giel42
|
||||
3. #jsnoueu9le : add
|
||||
4. #bt17giel42 : reset-root #bt17giel42
|
||||
5. #3igmh2it4p : add
|
||||
6. #bt17giel42 : reset-root #bt17giel42
|
||||
7. #gj5agagj7s : add
|
||||
8. #bt17giel42 : reset-root #bt17giel42
|
||||
9. #rhf1s808fb : add
|
||||
10. #bt17giel42 : reset-root #bt17giel42
|
||||
11. #agadr8gg6g : add
|
||||
12. #bt17giel42 : builtins.mergeio
|
||||
1. #re8lsbbg6o : add
|
||||
2. #m41m2ql36i : reset-root #m41m2ql36i
|
||||
3. #siglm9vcnk : add
|
||||
4. #m41m2ql36i : reset-root #m41m2ql36i
|
||||
5. #ebh8598vf0 : add
|
||||
6. #m41m2ql36i : reset-root #m41m2ql36i
|
||||
7. #t22r3l1hsh : add
|
||||
8. #m41m2ql36i : reset-root #m41m2ql36i
|
||||
9. #sb99mm43ni : add
|
||||
10. #m41m2ql36i : reset-root #m41m2ql36i
|
||||
11. #j1vrihj69n : add
|
||||
12. #m41m2ql36i : builtins.mergeio
|
||||
13. #sjg2v58vn2 : (initial reflogged namespace)
|
||||
|
||||
.> reset-root 2
|
||||
@ -523,3 +523,120 @@ myDoc = {{ **my text** __my text__ **MY_TEXT** ___MY__TEXT___ ~~MY~TEXT~~ **MY*T
|
||||
myDoc : Doc2
|
||||
|
||||
```
|
||||
## Parenthesized let-block with operator
|
||||
|
||||
Regression test for https://github.com/unisonweb/unison/issues/1778
|
||||
|
||||
```unison
|
||||
structural ability base.Abort where
|
||||
abort : a
|
||||
|
||||
(|>) : a -> (a ->{e} b) -> {e} b
|
||||
a |> f = f a
|
||||
|
||||
handler : a -> Request {Abort} a -> a
|
||||
handler default = cases
|
||||
{ a } -> a
|
||||
{abort -> _} -> default
|
||||
|
||||
Abort.toOptional : '{g, Abort} a -> '{g} Optional a
|
||||
Abort.toOptional thunk = '(toOptional! thunk)
|
||||
|
||||
Abort.toOptional! : '{g, Abort} a ->{g} (Optional a)
|
||||
Abort.toOptional! thunk = toDefault! None '(Some !thunk)
|
||||
|
||||
Abort.toDefault! : a -> '{g, Abort} a ->{g} a
|
||||
Abort.toDefault! default thunk =
|
||||
h x = Abort.toDefault! (handler default x) thunk
|
||||
handle (thunk ()) with h
|
||||
|
||||
x = '(let
|
||||
abort
|
||||
0) |> Abort.toOptional
|
||||
```
|
||||
|
||||
```ucm
|
||||
.> add
|
||||
|
||||
⍟ I've added these definitions:
|
||||
|
||||
structural ability base.Abort
|
||||
Abort.toDefault! : a -> '{g, Abort} a ->{g} a
|
||||
Abort.toOptional : '{g, Abort} a -> '{g} Optional a
|
||||
Abort.toOptional! : '{g, Abort} a ->{g} Optional a
|
||||
handler : a -> Request {Abort} a -> a
|
||||
x : 'Optional Nat
|
||||
|> : a -> (a ->{e} b) ->{e} b
|
||||
|
||||
.> edit x base.Abort |> handler Abort.toOptional Abort.toOptional! Abort.toDefault!
|
||||
|
||||
☝️
|
||||
|
||||
I added these definitions to the top of
|
||||
/Users/runar/work/unison/scratch.u
|
||||
|
||||
structural ability base.Abort where abort : {base.Abort} a
|
||||
|
||||
Abort.toDefault! : a -> '{g, Abort} a ->{g} a
|
||||
Abort.toDefault! default thunk =
|
||||
h x = Abort.toDefault! (handler default x) thunk
|
||||
handle !thunk with h
|
||||
|
||||
Abort.toOptional : '{g, Abort} a -> '{g} Optional a
|
||||
Abort.toOptional thunk = '(toOptional! thunk)
|
||||
|
||||
Abort.toOptional! : '{g, Abort} a ->{g} Optional a
|
||||
Abort.toOptional! thunk = toDefault! None '(Some !thunk)
|
||||
|
||||
handler : a -> Request {Abort} a -> a
|
||||
handler default = cases
|
||||
{ a } -> a
|
||||
{abort -> _} -> default
|
||||
|
||||
x : 'Optional Nat
|
||||
x =
|
||||
('let
|
||||
abort
|
||||
0) |> toOptional
|
||||
|
||||
(|>) : a -> (a ->{e} b) ->{e} b
|
||||
a |> f = f a
|
||||
|
||||
You can edit them there, then do `update` to replace the
|
||||
definitions currently in this namespace.
|
||||
|
||||
.> undo
|
||||
|
||||
Here are the changes I undid
|
||||
|
||||
Added definitions:
|
||||
|
||||
1. structural ability base.Abort
|
||||
2. base.Abort.abort : {#oup50kgmqv} a
|
||||
3. handler : a -> Request {#oup50kgmqv} a -> a
|
||||
4. Abort.toDefault! : a -> '{g, #oup50kgmqv} a ->{g} a
|
||||
5. Abort.toOptional : '{g, #oup50kgmqv} a
|
||||
-> '{g} Optional a
|
||||
6. Abort.toOptional! : '{g, #oup50kgmqv} a ->{g} Optional a
|
||||
7. x : 'Optional Nat
|
||||
8. |> : a -> (a ->{e} b) ->{e} b
|
||||
|
||||
```
|
||||
```ucm
|
||||
.> load scratch.u
|
||||
|
||||
I found and typechecked these definitions in scratch.u. If you
|
||||
do an `add` or `update`, here's how your codebase would
|
||||
change:
|
||||
|
||||
⍟ These new definitions are ok to `add`:
|
||||
|
||||
structural ability base.Abort
|
||||
Abort.toDefault! : a -> '{g, Abort} a ->{g} a
|
||||
Abort.toOptional : '{g, Abort} a -> '{g} Optional a
|
||||
Abort.toOptional! : '{g, Abort} a ->{g} Optional a
|
||||
handler : a -> Request {Abort} a -> a
|
||||
x : 'Optional Nat
|
||||
|> : a -> (a ->{e} b) ->{e} b
|
||||
|
||||
```
|
||||
|
Loading…
Reference in New Issue
Block a user