Commit Graph

112 Commits

Author SHA1 Message Date
Rui Barreiro
cb7dc7bffc test node004 passes 2020-06-17 23:29:54 +01:00
Rui Barreiro
184dce2312 fixed my tests messup 2020-06-13 11:45:53 +01:00
Rui Barreiro
c015aa82b0 test node003 passes 2020-06-13 11:42:28 +01:00
Rui Barreiro
fa7b6f12d2 Merge branch 'master' of github.com:idris-lang/Idris2 into javascript 2020-06-12 21:43:09 +01:00
Rui Barreiro
33014403eb tests everywhere 2020-06-12 21:35:08 +01:00
Niklas Larsson
a33fc1ec16
Merge pull request #256 from vilunov/repl-package
"--repl" command for opening a REPL in a package
2020-06-12 17:50:50 +02:00
Edwin Brady
c3c556f192 Merge https://github.com/idris-lang/Idris2 into linear-things 2020-06-12 14:16:01 +01:00
Niklas Larsson
4b7fbb0371 Fix overly nitpicky reflection test
See #287
2020-06-12 12:46:19 +02:00
Edwin Brady
c9b20911e1 Add linear pair/dependent pair to the prelude
I'm playing with some linear structures and finding these useful a lot,
so good to have a consistent syntax for it. '#' is chosen because it's
short, looks a bit like a cross if you look at it from the right angle
(!) and so as not to clash with '@@' in preorder reasoning syntax.
2020-06-12 11:18:12 +01:00
Edwin Brady
361d2e4d88
Merge pull request #275 from idris-lang/issue-270
[ re #270 ] Mention the target type of the auto search
2020-06-11 16:14:16 +01:00
Guillaume ALLAIS
43738c172d [ re #270 ] Mention the target type of the auto search 2020-06-11 14:28:34 +01:00
Guillaume ALLAIS
f3c0e89ae8 [ re #238 ] Adding --no-index and --word-diff=color
Without --no-index, git compares the files with their state in HEAD.
But we want to compare them to each other! This explain why we were
getting no output whatsoever.

With --word-diff=color, we can easily spot the small changes anywhere in
a line.
2020-06-11 14:23:47 +01:00
Niklas Larsson
015f195b87
Merge pull request #272 from melted/fix_primitive_bootstrap
Use 2^64 constant instead of calculation
2020-06-11 15:13:40 +02:00
Niklas Larsson
b5f67b94ae Use constants instead of calculation for upper bounds
Add wrapping to 8-bit adding.

This is a workaround to fix the bootstrap
Fixes #268
2020-06-11 14:23:41 +02:00
Jan de Muijnck-Hughes
63e127094e Improved parsing for literate modes.
The tokenizer for literate modes was incorretly detecting code lines in text.
This PR fixes that, and allows for empty code lines.
2020-06-11 12:51:47 +01:00
Rui Barreiro
c2d994ad5c first test 2020-06-11 10:52:54 +01:00
Edwin Brady
df3449f44b Fix the other clashing test output
I don't understand the difference here - there's probably a commit I
hadn't merged earlier that affected the name generation.
2020-06-10 13:08:50 +01:00
Edwin Brady
c07876d1a3 Fix clashing test output 2020-06-10 12:53:18 +01:00
Edwin Brady
004b41a3d8 Merge https://github.com/idris-lang/Idris2 into vis-case-with 2020-06-10 12:50:30 +01:00
Edwin Brady
42676d2504
Merge pull request #265 from edwinb/find-ipkg-ide
In IDE mode, look for a ipkg file before loading
2020-06-10 12:42:59 +01:00
Edwin Brady
0cc54ff145 Propagate visibility appropriately to case/with
If a function is public export, the local definitions also need to be
public export for it to reduce properly. But if they're not, we don't
want them exported or they might affect the module hash and cause
unnecessary rebuilds.
2020-06-10 12:41:02 +01:00
Jan de Muijnck-Hughes
90fb901c8f Fix test reporting when in interactive mode.
When runing in interactive mode, the diff between expected and output is not being show,
Supposedly, Git-diff returns 0 on successful run and a non-zero for error.
However, this is not being picked up by the test suite.

We change git-diff's error reporting to be more diff like in which:

+ +ve indicates that there is a diff.
+ 0 indicates the files are the same.
+ -ve program error.

This should make diff reporting more robust.
2020-06-10 09:30:02 +01:00
Edwin Brady
cf23bae7d6 In IDE mode, look for a ipkg file before loading
This takes the responsibilty of finding the ipkg away from IDE mode,
which seems sensible given that we can do it ourselves. If there isn't
one, it'll load from the local directory as always.
2020-06-09 23:31:30 +01:00
Edwin Brady
ca28dab1d7 Add finalisers for Racket back end
Like Chez, we also need an explicit call to the garbage collector at the
end to ensure that all the finalisers get run on exit.
2020-06-08 22:13:24 +01:00
Edwin Brady
e32f039227 Fix includes in chez022 test 2020-06-08 20:46:25 +01:00
Edwin Brady
d60feaace0 Add finalisers to Chez back end
This involves new primitives GCPtr and GCAnyPtr which are pointer types
that have finalisers attached. The finalisers are run when the
associated pointer goes out of scope.

In the test, I am assuming that the GC will only be called once, right
at the end. Otherwise, the output isn't guaranteed to be deterministic!
Let's see how this assumption holds...

This is currently Chez only. I think it'll be easy enough to add to
the Racket and Gambit back ends too.
2020-06-08 20:34:23 +01:00
Nikita Vilunov
560d472502 add a test for --repl 2020-06-08 19:21:22 +03:00
Edwin Brady
85bd751283 Update reflection test again 2020-06-08 13:22:18 +01:00
Edwin Brady
abcb1b417f
Merge pull request #248 from vilunov/repl-let
":let" command for REPL
2020-06-08 12:00:15 +01:00
Edwin Brady
73de552776
Merge pull request #239 from MarcelineVQ/elab-changes
add parens for some TTImp Shows
2020-06-08 11:54:19 +01:00
Edwin Brady
4834f2f78c Update test output
Clash in a reflection test due to conflicting merges. I'd like to find a
way to make the internally generated numbers not matter here (and
elsewhere) but I don't see an obvious way.
2020-06-08 10:39:58 +01:00
Edwin Brady
e033609310
Merge pull request #207 from mb64/assert_smaller-linear
Make assert_smaller and assert_total linear
2020-06-08 10:19:33 +01:00
Edwin Brady
d47d495744 Free standing case blocks return ()
Fixes #116. This is the solution Idris 1 took, and while it is a special
case, the syntax does make it explicit (in a way) that the result of the
case is unused - if you mean something other than (), you must now say
so!
2020-06-07 22:49:19 +01:00
Nikita Vilunov
018c17b69a Add :let test 2020-06-07 16:40:45 +03:00
MarcelineVQ
6993c6df6b add parens for some TTImp Shows
helps with readability since these, especially named-IPi, come up a lot
didn't change everything that could need it like PiInfo or BindMode
PiInfo rarely has DefImplicit (so far) and BindMode hasn't come up a lot (so far)
reduced indentation for TTImp Show implementation
2020-06-06 17:16:43 -07:00
Edwin Brady
93022af74e More explicitness in evaluator return type
Another one from the "stop trying to be clever" files :). Instead of a
continuation for fallthrough in the evaluator, be explicit about whether
there's a result, no match, or evaluation is stuck.
Fixes #70
2020-06-06 22:20:25 +01:00
Edwin Brady
252e07833b Fix case trees at multiplicity zero
Can't ignore a constructor a multiplicity zero if the whole function is
multiplicity zero
2020-06-06 20:45:20 +01:00
Edwin Brady
c17d4ff0a5 Look inside case blocks in conversion check
This is quite fiddly as it the blocks might be in different contexts so
we need to keep track of which variables correspond in the scrutinees of
the blocks. Once that's done, check the terms at the leaves convert,
then check the corresponding variables convert.

This may not be perfect yet, because we only look at case scrutinees to
find correspondence. It might also be a bit slower than it could be, but
at least these checks are quite rare.

Fixes #208 and maybe some others?
2020-06-04 18:21:44 +01:00
Edwin Brady
946e1b3a51 Slightly neater reflection008 test 2020-06-03 09:25:09 +01:00
Edwin Brady
3a7aedf0f4 Add reflection under (explicit) binders
This allows writing a staged well typed interpreter, for example (see
reflection008 test)
2020-06-03 09:17:37 +01:00
Edwin Brady
c682ded9c4 Reduce amount of normalisation in elab scripts
We don't want to unfold definitions in 'pure' or 'check' or 'bind' since
we want the exact expression that the script author has used.
2020-06-03 00:22:03 +01:00
Edwin Brady
d8d13d912e Add alternative example to reflection002
A bit more typesafe...
2020-06-02 23:56:30 +01:00
Edwin Brady
08b56e9e75 Add quote operation to Elab
Allows quoting a term back to a TTImp. Test reflection007 shows one
possible use for this, building a reflected, type safe, representation
of an expression.
2020-06-02 23:36:20 +01:00
Edwin Brady
2a75731916 In reflection, check now takes a concrete type
So the type of Elab now gives the expected type that's being elaborated
to, meaning that we can run 'check' in the middle of scripts and use the
result.
2020-06-02 22:41:37 +01:00
Edwin Brady
9fab367f0f Reflect differently on LHS
On the LHS, we want to match against the reflected thing, so FC and
implicits need to turn into match anything patterns, or we won't match
anything at all. This means we can put quoted terms on the LHS, with
pattern variables under ~().
2020-06-02 19:21:46 +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
Mark Barbone
c4cdebb578
Fix tests 2020-06-01 19:13:46 -04: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