Merge branch 'main' into impossible-lam

CHANGELOG_NEXT.md

@@ -49,6 +49,9 @@ This CHANGELOG describes the merged but unreleased changes. Please see [CHANGELO
 * The compiler now supports `impossible` in a non-case lambda. You can now
   write `\ Refl impossible`.
 
+* The compiler now parses `~x.fun` as unquoting `x` rather than `x.fun`
+  and `~(f 5).fun` as unquoting `(f 5)` rather than `(f 5).fun`.
+
 ### Backend changes
 
 #### RefC Backend

Makefile

@@ -158,7 +158,7 @@ test: testenv
 	@echo "NOTE: \`${MAKE} test\` does not rebuild Idris or the libraries packaged with it; to do that run \`${MAKE}\`"
 	@if [ ! -x "${TARGET}" ]; then echo "ERROR: Missing IDRIS2 executable. Cannot run tests!\n"; exit 1; fi
 	@echo
-	@${MAKE} -C tests only=$(only) except=$(except) IDRIS2=${TARGET} IDRIS2_PREFIX=${TEST_PREFIX}
+	@${MAKE} -C tests only=$(only) except=$(except) IDRIS2=${TARGET} IDRIS2_PREFIX=${TEST_PREFIX} CPPFLAGS="${CPPFLAGS}" LDFLAGS="${LDFLAGS}"
 
 
 retest: testenv

config.mk

@@ -36,6 +36,12 @@ else
 	SHLIB_SUFFIX := .so
 endif
 
+# Find homebrew's libgmp on ARM macs
+ifneq (,$(wildcard ${HOMEBREW_PREFIX}/include/gmp.h))
+	CPPFLAGS += -I${HOMEBREW_PREFIX}/include
+	LDFLAGS += -L${HOMEBREW_PREFIX}/lib
+endif
+
 ifneq (, $(findstring freebsd, $(MACHINE)))
 	CFLAGS += -I$(shell /sbin/sysctl -n user.localbase)/include
 	LDFLAGS += -L$(shell /sbin/sysctl -n user.localbase)/lib

src/Idris/Parser.idr

@@ -631,7 +631,7 @@ mutual
                   decoratedSymbol fname "]"
                   pure ts
            pure (PQuoteDecl (boundToFC fname b) (collectDefs (concat b.val)))
-    <|> do b <- bounds (decoratedSymbol fname "~" *> simpleExpr fname indents)
+    <|> do b <- bounds (decoratedSymbol fname "~" *> simplerExpr fname indents)
            pure (PUnquote (boundToFC fname b) b.val)
     <|> do start <- bounds (symbol "(")
            bracketedExpr fname start indents

tests/idris2/error/perror031/Issue3251.idr

@@ -0,0 +1,19 @@
+import Language.Reflection
+
+(.fun) : Nat -> Nat
+
+x : TTImp
+
+f : Nat -> TTImp
+
+useX : TTImp
+useX = `(g (~x).fun)
+
+useX' : TTImp
+useX' = `(g ~x.fun)
+
+useFX : TTImp
+useFX = `(g (~(f 5)).fun)
+
+useFX' : TTImp
+useFX' = `(g ~(f 5).fun)

tests/idris2/error/perror031/expected

@@ -0,0 +1 @@
+1/1: Building Issue3251 (Issue3251.idr)

tests/idris2/error/perror031/run

@@ -0,0 +1,3 @@
+. ../../../testutils.sh
+
+check Issue3251.idr

tests/refc/ccompilerArgs/run

@@ -20,8 +20,8 @@ cd ./library/
     make > /dev/null
 cd ..
 
-export CFLAGS="-I./library/ -O3"
-export LDFLAGS="-L./library/ -Wl,-S"
+export CFLAGS="-I./library/ -O3 ${CFLAGS}"
+export LDFLAGS="-L./library/ -Wl,-S ${LDFLAGS}"
 export LDLIBS="-lexternalc"
 export LD_LIBRARY_PATH="$LD_LIBRARY_PATH:./library/"
 export DYLD_LIBRARY_PATH="$DYLD_LIBRARY_PATH:./library/"