From b135b85201d11c78c66e6f438259f659f6900a13 Mon Sep 17 00:00:00 2001 From: Denis Buzdalov Date: Thu, 24 Oct 2024 18:11:59 +0300 Subject: [PATCH] [ fix ] Fix ability to declare fixities in `do` --- src/Idris/Desugar.idr | 12 ++++----- tests/idris2/operators/operators012/Y.idr | 27 ++++++++++++++++++++ tests/idris2/operators/operators012/expected | 1 + tests/idris2/operators/operators012/run | 3 +++ 4 files changed, 37 insertions(+), 6 deletions(-) create mode 100644 tests/idris2/operators/operators012/Y.idr create mode 100644 tests/idris2/operators/operators012/expected create mode 100755 tests/idris2/operators/operators012/run diff --git a/src/Idris/Desugar.idr b/src/Idris/Desugar.idr index 02b41723e1..8f317d1d9c 100644 --- a/src/Idris/Desugar.idr +++ b/src/Idris/Desugar.idr @@ -737,10 +737,10 @@ mutual pure $ seqFun fc ns tm' rest' expandDo side ps topfc ns (DoBind fc nameFC n rig ty tm :: rest) = do tm' <- desugarDo side ps ns tm - rest' <- expandDo side ps topfc ns rest whenJust (isConcreteFC nameFC) $ \nfc => addSemanticDecorations [(nfc, Bound, Just n)] ty' <- maybe (pure $ Implicit (virtualiseFC fc) False) (\ty => desugarDo side ps ns ty) ty + rest' <- expandDo side ps topfc ns rest pure $ bindFun fc ns tm' $ ILam nameFC rig Explicit (Just n) ty' rest' expandDo side ps topfc ns (DoBindPat fc pat ty exp alts :: rest) @@ -749,12 +749,12 @@ mutual exp' <- desugarDo side ps ns exp alts' <- traverse (map snd . desugarClause ps True) alts let ps' = newps ++ ps - rest' <- expandDo side ps' topfc ns rest let fcOriginal = fc let fc = virtualiseFC fc let patFC = virtualiseFC (getFC bpat) ty' <- maybe (pure $ Implicit fc False) (\ty => desugarDo side ps ns ty) ty + rest' <- expandDo side ps' topfc ns rest pure $ bindFun fc ns exp' $ ILam EmptyFC top Explicit (Just (MN "_" 0)) ty' @@ -788,12 +788,12 @@ mutual (PatClause fc bpat rest' :: alts') expandDo side ps topfc ns (DoLetLocal fc decls :: rest) - = do rest' <- expandDo side ps topfc ns rest - decls' <- traverse (desugarDecl ps) decls + = do decls' <- traverse (desugarDecl ps) decls + rest' <- expandDo side ps topfc ns rest pure $ ILocal fc (concat decls') rest' expandDo side ps topfc ns (DoRewrite fc rule :: rest) - = do rest' <- expandDo side ps topfc ns rest - rule' <- desugarDo side ps ns rule + = do rule' <- desugarDo side ps ns rule + rest' <- expandDo side ps topfc ns rest pure $ IRewrite fc rule' rest' -- Replace all operator by function application diff --git a/tests/idris2/operators/operators012/Y.idr b/tests/idris2/operators/operators012/Y.idr new file mode 100644 index 0000000000..0b9459ec5b --- /dev/null +++ b/tests/idris2/operators/operators012/Y.idr @@ -0,0 +1,27 @@ +f : Nat +f = + let (%^%) : Nat -> Nat -> Nat + (%^%) = (+) + private infixl 1 %^% + in 1 %^% 2 + +g : Nat +g = do + let (%^%%) : Nat -> Nat -> Nat + (%^%%) = (+) + private infixl 1 %^%% + 1 %^%% 2 + +crazy1 : Nat +crazy1 = do + let (%^%%%) : Nat -> Nat -> Nat + (%^%%%) = (+) + rewrite let private infixl 1 %^%%% in the (Nat = Nat) Refl + 1 %^%%% 2 + +crazy2 : List Nat +crazy2 = do + let (%^%%%%) : Nat -> Nat -> Nat + (%^%%%%) = (+) + x : (let private infixl 1 %^%%%% in Nat) <- [1] + pure $ x %^%%%% 2 diff --git a/tests/idris2/operators/operators012/expected b/tests/idris2/operators/operators012/expected new file mode 100644 index 0000000000..257dbc7427 --- /dev/null +++ b/tests/idris2/operators/operators012/expected @@ -0,0 +1 @@ +1/1: Building Y (Y.idr) diff --git a/tests/idris2/operators/operators012/run b/tests/idris2/operators/operators012/run new file mode 100755 index 0000000000..946196f02f --- /dev/null +++ b/tests/idris2/operators/operators012/run @@ -0,0 +1,3 @@ +. ../../../testutils.sh + +check Y.idr