Commit Graph

2728 Commits

Author SHA1 Message Date
Alex Gryzlov
d4f4a74fbf add Data.Fuel 2020-06-02 17:20:42 +02:00
Giuseppe Lomurno
a9f334ef5c Added auto_implicit_depth pragma
By default, the search depth for auto implcit arguments is limited to
50. This patch adds a new pragma `%auto_implicit_depth` with which the
user can change the depth limit.
2020-06-02 15:46:26 +02:00
Edwin Brady
a2da617f84
Merge pull request #222 from edwinb/reflection-prims
A couple more elab reflection primitives
2020-06-02 13:07:55 +01:00
Edwin Brady
f46a4ed158
Merge pull request #224 from edwinb/reflection-fixes
Reflection fixes
2020-06-02 12:34:43 +01:00
Edwin Brady
c3ee2a3fac Change genSym behaviour
Instead of merely generating a locally unique name, use the existing
code for generating a new unique variable name in the unifier, which is
therefore globally unique.
2020-06-02 12:13:38 +01:00
Edwin Brady
e7f8e2df8c Fix reflection of PiInfo
It needs to account for the implicit parameter
2020-06-02 12:10:57 +01:00
Niklas Larsson
8e788658c4
Merge pull request #223 from dkeehl/fix-libidris2_support_loading
Try to load libidris2_support on older Windows
2020-06-02 09:50:58 +02:00
Thomas Lin
fc8e6b1fef Use GetSystemTimeAsFileTime on older Windows 2020-06-02 10:30:44 +08:00
Mark Barbone
c4cdebb578
Fix tests 2020-06-01 19:13:46 -04:00
Edwin Brady
30737f5ecc
Merge pull request #219 from normalcoder/gambit-ffi-callbacks
Fix "Can't pass argument of type %World to foreign function" issue in gambit ffi
2020-06-01 22:44:21 +01:00
Edwin Brady
a33136aa00 A couple more elab reflection primitives
Get the names of local variables. and add the ability to look up their
types.
When we get a reflected TTImp, either checking the Goal or looking up a
type, it's not impossible that there'll be some repeated binder names,
so also make sure binders are unique relative to the current context.
Ideally we'd also rename things in the environment to guarantee that all
names are unique, but we don't yet.

(This would be much easier if reflected terms were typed such that they
were well scoped, but that would also make reflection harder to use.)
2020-06-01 22:16:27 +01:00
Mark Barbone
18c6c4a385
Clarify assert_{total,smaller} docs 2020-06-01 15:37:34 -04:00
Mark Barbone
58532a6a6c
Explain multiplicity 0 in assert_smaller docs 2020-06-01 15:37:34 -04:00
Mark Barbone
4bf2d11f6c
Add appropriate linearity annotation to assert_smaller and assert_total 2020-06-01 15:37:33 -04:00
Edwin Brady
f33feecbea
Merge pull request #220 from edwinb/macros
Implement %macro flag
2020-06-01 19:35:33 +01:00
normalcoder
973a665629 Fix "Can't pass argument of type %World to foreign function" issue in gambit ffi
https://github.com/idris-lang/Idris2/issues/76
2020-06-01 21:18:37 +03:00
Edwin Brady
1c18fe589b Forgot to add the new test again, didn't I... 2020-06-01 19:13:46 +01:00
Edwin Brady
3d2765e930 Add top level %runElab
This invokes a script of type Elab (). %runElan in a term invokes a
script of type Elab TT. The elaborator now pushes in that type, so that
it'll report an appropriate error if you give it a script of the wrong
type.
2020-06-01 19:06:10 +01:00
Edwin Brady
d5b5af91d1 Implement %macro flag
A %macro must always be fully applied. Whenever the elaborator
encounters a %macro application (except in a function LHS) it evaluates
the application and sends the result to %runElab. So:

%macro
foo : args -> Elab TT
...
def = foo a b c

is equivalent to

foo : args -> Elab TT
...
def = %runElab foo a b c
2020-06-01 17:55:54 +01:00
Edwin Brady
adc449acb3
Merge pull request #218 from edwinb/reflect-defs
More elaborator reflection primitives
2020-06-01 15:43:56 +01:00
Edwin Brady
d45f92fd97 Add some reflected name manipulation
genSym, for generating a unique global name, and inCurrentNS for putting
a name in the current namespace.
2020-06-01 15:13:42 +01:00
Edwin Brady
02d371a94b Add reflection operation for adding declarations
Declarations can be quoted with `[ decl ]. See reflection004 for an
example.
2020-06-01 15:01:52 +01:00
Edwin Brady
e6f6c105d1 Reflection primitives for querying names/types
See reflection003 test for some examples
2020-06-01 14:26:37 +01:00
Edwin Brady
e2aabd6602 Add syntax for quoting names
`{{ n }} gives a value of type Name. No name resolution is attempted (so
no namespaces added etc)
2020-06-01 13:39:18 +01:00
Edwin Brady
d0021f7e48
Merge pull request #212 from normalcoder/gambit-ffi-callbacks
Gambit ffi callbacks
2020-06-01 12:41:58 +01:00
Sventimir
d796cfa126 Define the notion of Factor and GCD and prove some of their properties. 2020-06-01 13:41:00 +02:00
Edwin Brady
7944da4121
Merge pull request #216 from edwinb/bits-primitives
Bits primitives
2020-06-01 12:37:58 +01:00
Sventimir
9c97ab474b Add some helpers for transforming equations and inequalities on Nat. 2020-06-01 13:30:47 +02:00
Sventimir
932ea60dbc Port Data.Fin.Extra module from Idris1. 2020-06-01 13:29:59 +02:00
Edwin Brady
7f6de27f5c Update scheme/racket to deal with Bits types
We need to add Bits primitives to Idris2-boot to keep that at least able
to build this for bootstrapping purposes.
2020-06-01 11:58:22 +01:00
Edwin Brady
2eb2ce6097 Add Bits primitives
Including appropriate casts, and Num/Eq/Ord/Show implementations.
Also includes new primitives in Data.Buffer, and calls to foreign
functions in C as 'unsigned'.
2020-06-01 11:48:03 +01:00
Rohit Grover
e4c6aa282c
some proofs and views around lists (#133) 2020-06-01 08:28:37 +01:00
normalcoder
5e1c0f26bf Support callbacks in ffi for gambit 2020-06-01 02:59:16 +03:00
normalcoder
e001d266fe Add sys/time.h to satisfy xcode.
It seems relevant to all BSD systems.

In xcode the option -Wno-error-implicit-function-declaration is enabled. So the following error occured:
Idris2/support/c/idris_file.c:76:13: Missing '#include <sys/time.h>'; declaration of 'select' must be imported from module 'Darwin.POSIX.sys.time' before it is required

I hope it won't break anything on linux.
2020-06-01 00:48:19 +03:00
Edwin Brady
54119bc4e2
Merge pull request #210 from edwinb/elab-reflection
Initial steps to elaborator reflection
2020-05-31 15:06:50 +01:00
Edwin Brady
5b20fbd45c Workaround for bug in bootstrap version
The bootstrap version has an occasional bug with as patterns, which is
tripped by elabScript. This works around it.
(I'd rather do this than update the Scheme, since Idris2-boot will still
work this way!)
2020-05-31 14:48:40 +01:00
Edwin Brady
106235c165 Allow scripts to inspect goal
If available (sometimes, say a top level expression, it might need
inferring so there'll be no goal available). Also add the ability to log
the current goal, or indeed any term.
2020-05-31 14:33:34 +01:00
Edwin Brady
9544e05da1 Process elaborator scripts
Still all they can do is check and log. Now scripts must return
something of type TT, which is in practice a TTImp that goes to the
elaborator for final checking
2020-05-31 13:05:06 +01:00
Edwin Brady
85c002c771 Progress on elaborator reflection
Add %runElab and start on scripts, although all they can do so far is
check a term. This does gives us, sort of, "template Idris" (as
demonstrated in test reflection002)
2020-05-31 01:36:54 +01:00
Edwin Brady
bb240d4390
Merge pull request #206 from edwinb/coverage-fix
Calculate compile time references even in case
2020-05-30 22:15:18 +01:00
Edwin Brady
26e6e1ed82 Calculate compile time references even in case
If we don't do this, we don't look inside case blocks to check they
cover, and so we might miss coverage errors in nested case blocks.
Fixes #202
2020-05-30 21:53:29 +01:00
Edwin Brady
12aa6b6228
Merge pull request #204 from edwinb/fix-vim
findIpkg needs to set working directory
2020-05-30 19:22:01 +01:00
Edwin Brady
773d0dfdee findIpkg needs to set working directory
This makes vim mode work again.
I don't know a good way to test this, since it involves dealing with
absolute paths. If anyone has the bash skills to get this working in a
pkg test, please do...
2020-05-30 18:49:48 +01:00
Edwin Brady
e7baf313f0
Merge pull request #203 from edwinb/visibility
Add visibility rules on types
2020-05-30 18:01:24 +01:00
Edwin Brady
c212255290 IOArray needs to export max 2020-05-30 17:40:48 +01:00
Edwin Brady
ecaa73bad5 Update test result
Not sure why this didn't fail for me locally... possibly libraries out
of sync.
2020-05-30 17:30:31 +01:00
Edwin Brady
3f914889b8 Add visibility rules on types
Can't export a type which refers to a private name. This has caught a
couple of visibility errors in the libraries, code and tests, so they've
been updated too.
2020-05-30 17:03:15 +01:00
Edwin Brady
c90410334b
Merge pull request #201 from andylokandy/pathfix
Make pathToNS handle absolute path
2020-05-30 16:13:53 +01:00
Edwin Brady
6c37636c1b
Merge pull request #200 from edwinb/findipkg
Allow absolute paths in --find-ipkg
2020-05-30 16:13:02 +01:00
andylokandy
f007c7816e Sync Utils.Path with System.Path 2020-05-30 21:51:12 +08:00