From 1dd81ff10bbb122cd75b75a002def5d1ed28feea Mon Sep 17 00:00:00 2001 From: Edwin Brady Date: Thu, 5 Mar 2020 11:22:48 +0000 Subject: [PATCH] Look under . for function name on lhs Need this to rule out some ambiguous names. Fixes #204. --- docs/reference/envvars.rst | 7 +++++++ docs/reference/index.rst | 1 + src/TTImp/Elab/Ambiguity.idr | 1 + src/TTImp/TTImp.idr | 1 + tests/Main.idr | 2 +- tests/idris2/reg006/Cmd.idr | 20 ++++++++++++++++++++ tests/idris2/reg006/expected | 1 + tests/idris2/reg006/run | 3 +++ 8 files changed, 35 insertions(+), 1 deletion(-) create mode 100644 docs/reference/envvars.rst create mode 100644 tests/idris2/reg006/Cmd.idr create mode 100644 tests/idris2/reg006/expected create mode 100755 tests/idris2/reg006/run diff --git a/docs/reference/envvars.rst b/docs/reference/envvars.rst new file mode 100644 index 0000000..a044b1d --- /dev/null +++ b/docs/reference/envvars.rst @@ -0,0 +1,7 @@ +.. _ref-sect-envvars: + +********************* +Environment Variables +********************* + +[TODO: Fill in the environment variables recognised by Idris 2] diff --git a/docs/reference/index.rst b/docs/reference/index.rst index 00d2305..273f6f1 100644 --- a/docs/reference/index.rst +++ b/docs/reference/index.rst @@ -17,3 +17,4 @@ This is a placeholder, to get set up with readthedocs. :maxdepth: 1 packages + envvars diff --git a/src/TTImp/Elab/Ambiguity.idr b/src/TTImp/Elab/Ambiguity.idr index 187ed6b..9901290 100644 --- a/src/TTImp/Elab/Ambiguity.idr +++ b/src/TTImp/Elab/Ambiguity.idr @@ -262,6 +262,7 @@ pruneByType env target alts -- if there's any concrete matches, drop the non-concrete -- matches marked as '%allow_overloads' from the possible set then do keep <- filterCore (notOverloadable defs) matches + log 10 $ "Keep " ++ show keep pure (map snd keep) else pure (map snd matches) if isNil res diff --git a/src/TTImp/TTImp.idr b/src/TTImp/TTImp.idr index 81bdef7..ebe1713 100644 --- a/src/TTImp/TTImp.idr +++ b/src/TTImp/TTImp.idr @@ -562,6 +562,7 @@ getFn (IApp _ f arg) = getFn f getFn (IWithApp _ f arg) = getFn f getFn (IImplicitApp _ f _ _) = getFn f getFn (IAs _ _ _ f) = getFn f +getFn (IMustUnify _ _ f) = getFn f getFn f = f -- Everything below is TTC instances diff --git a/tests/Main.idr b/tests/Main.idr index f13f06f..df6c360 100644 --- a/tests/Main.idr +++ b/tests/Main.idr @@ -72,7 +72,7 @@ idrisTests -- Records, access and dependent update "record001", "record002", -- Miscellaneous regressions - "reg001", "reg002", "reg003", "reg004", "reg005", + "reg001", "reg002", "reg003", "reg004", "reg005", "reg006", -- Totality checking "total001", "total002", "total003", "total004", "total005", "total006", diff --git a/tests/idris2/reg006/Cmd.idr b/tests/idris2/reg006/Cmd.idr new file mode 100644 index 0000000..ab5928f --- /dev/null +++ b/tests/idris2/reg006/Cmd.idr @@ -0,0 +1,20 @@ +data MyCmd : Type -> Type where + Display : String -> MyCmd () + Input : MyCmd String + + Pure : ty -> MyCmd ty + (>>=) : MyCmd a -> (a -> MyCmd b) -> MyCmd b + +runMyCmd : MyCmd a -> IO a +runMyCmd (Display str) = putStrLn str +runMyCmd Input = do str <- getLine + pure str +runMyCmd (Pure x) = pure x +runMyCmd (c >>= f) = do res <- runMyCmd c + runMyCmd (f res) + +myCmdTest : MyCmd () +myCmdTest = do Display "Hello" + x <- Input + Display x + Pure () diff --git a/tests/idris2/reg006/expected b/tests/idris2/reg006/expected new file mode 100644 index 0000000..fde33c4 --- /dev/null +++ b/tests/idris2/reg006/expected @@ -0,0 +1 @@ +1/1: Building Cmd (Cmd.idr) diff --git a/tests/idris2/reg006/run b/tests/idris2/reg006/run new file mode 100755 index 0000000..272df49 --- /dev/null +++ b/tests/idris2/reg006/run @@ -0,0 +1,3 @@ +$1 --check Cmd.idr + +rm -rf build