fix idiom brackets to account for IAlternative

Things like (,) () aren't straightforward IVar's but are IAlternative's
which present options about how the term should resolve. [| |] was not
accounting for this.
This commit is contained in:
MarcelineVQ 2020-09-17 01:48:28 -07:00 committed by G. Allais
parent 315fc8ce2d
commit 961a28ee64
7 changed files with 28 additions and 6 deletions

View File

@ -114,6 +114,8 @@ bindBangs ((n, fc, btm) :: bs) tm
(Implicit fc False) tm)
idiomise : FC -> RawImp -> RawImp
idiomise fc (IAlternative afc u alts)
= IAlternative afc (mapAltType (idiomise afc) u) (idiomise afc <$> alts)
idiomise fc (IApp afc f a)
= IApp fc (IApp fc (IVar fc (UN "<*>"))
(idiomise afc f))

View File

@ -105,11 +105,7 @@ doBind ns (IQuote fc tm)
doBind ns (IUnquote fc tm)
= IUnquote fc (doBind ns tm)
doBind ns (IAlternative fc u alts)
= IAlternative fc (doBindAlt u) (map (doBind ns) alts)
where
doBindAlt : AltType -> AltType
doBindAlt (UniqueDefault t) = UniqueDefault (doBind ns t)
doBindAlt u = u
= IAlternative fc (mapAltType (doBind ns) u) (map (doBind ns) alts)
doBind ns tm = tm
export

View File

@ -379,6 +379,11 @@ data ImpREPL : Type where
DebugInfo : Name -> ImpREPL
Quit : ImpREPL
export
mapAltType : (RawImp -> RawImp) -> AltType -> AltType
mapAltType f (UniqueDefault x) = UniqueDefault (f x)
mapAltType _ u = u
export
lhsInCurrentNS : {auto c : Ref Ctxt Defs} ->
NestedNames vars -> RawImp -> Core RawImp

View File

@ -12,4 +12,3 @@ export
addm : Maybe Int -> Maybe Int -> Maybe Int
addm x y = [| x + y |]

View File

@ -0,0 +1,17 @@
-- Things like ( , ) ( ** ) () are special in that they denote more than
-- one thing at once. () can mean Unit or MkUnit, (,) can mean Pair or MkPair
-- Idiom brackets need to be able to work despite that, which is tested here
fez : IO Int
fez = pure 1
fez1 : IO (Int, ())
fez1 = [| MkPair fez (pure ()) |]
fez2 : IO (Int, Maybe Int)
fez2 = [| ( fez , (pure Nothing) ) |]
fuzz : IO ()
fuzz = do
fez1 >>= printLn
fez2 >>= printLn

View File

@ -1,3 +1,5 @@
1/1: Building Idiom (Idiom.idr)
Main> Just 7
Main> Bye for now!
(1, ())
(1, Nothing)

View File

@ -1,3 +1,4 @@
$1 --no-color --console-width 0 --no-banner Idiom.idr < input
$1 --no-color --console-width 0 --no-banner Idiom2.idr --exec fuzz
rm -rf build