ilyakooo0/Idris-dev
1
0
Fork 0
mirror of https://github.com/ilyakooo0/Idris-dev.git synced 2024-11-11 14:57:30 +03:00
Code Issues Projects Releases Wiki Activity
6,722 Commits 4 Branches 42 Tags 40 MiB
50878fa319
Commit Graph

6722 Commits

This Branch
This Branch
All Branches
Author SHA1 Message Date
Niklas Larsson
50878fa319 Merge pull request #2638 from NightRa/patch-2 
Fix Char-Ascii docs
 2015-09-20 01:15:13 +02:00
Ilan Godik
56afb44034 Fix Char-Ascii docs 2015-09-20 00:45:09 +03:00
David Christiansen
aba225c3f5 Merge pull request #2635 from david-christiansen/coverage-default 
Use elaborated form of cases to check for defaults
 2015-09-19 13:23:53 +02:00
David Christiansen
f1ff8fb728 Merge pull request #2634 from david-christiansen/namesInQQ 
Respect quotation when expanding parameters
 2015-09-19 13:17:13 +02:00
David Raymond Christiansen
aeb703e015 Use elaborated form of cases to check for defaults 
Before, the check for a default catch-all case was done using PTerm and
the Placeholder constructor. Now, universal cases at the end are found
by checking that all arguments are elaborated to pattern variables. This
can catch cases where it's not an explicit placeholder, and it avoids
confusion with constructors by checking the binders of the elaborated
case.
 2015-09-19 12:23:42 +02:00
David Raymond Christiansen
92c195961c Respect quotation when expanding parameters 
This keeps where-bound names from occaisionally failing in
antiquotations because they weren't expanded to where-names.
 2015-09-19 10:52:27 +02:00
David Christiansen
6d7d3bdba1 Merge pull request #2630 from david-christiansen/namesInQQ 
Make name operations on PTerm quotation-aware
 2015-09-19 08:54:55 +02:00
David Raymond Christiansen
071d34b3fc Make name operations on PTerm quotation-aware 
This fixes an obscure issue where certain do-bound names that did not
shadow, but were identical to, other do-bound names in different
subexpressions of one larger expression would fail when referred to in
antiquotations. Example:

    (do h <- gensym
        claim h a
        fill `(C1 ~(Var h)); solve) <|>
      (do h <- gensym
          claim h b
          fill `(C2 ~(Var h)); solve)

The second antiquoted h would throw a "No Such Variable" error, because
the second lambda-bound h was renamed at one point without its use site
being renamed similarly.
 2015-09-18 23:20:02 +02:00
Niklas Larsson
9243fdfc42 Merge pull request #2629 from melted/fix_completion 
Add desugarnats to completion
 2015-09-18 00:45:32 +02:00
Niklas Larsson
81a73e95e9 Add desugarnats to completion 2015-09-17 22:57:18 +02:00
David Christiansen
2535873e47 Merge pull request #2627 from comco/patch-1 
Add Vim command for declaration documentation
 2015-09-17 19:17:00 +02:00
comco
98d6a8750a Add Vim command for declaration documentation 2015-09-17 18:30:30 +02:00
Niklas Larsson
0345e41479 Merge pull request #2624 from juhp/patch-3 
allow utf8-string 1.0.*
 2015-09-17 16:31:48 +02:00
Jens Petersen
ce8b625ede allow utf8-string 1.0.* 2015-09-17 10:00:45 +09:00
Niklas Larsson
1c24404553 Merge pull request #2618 from cbiffle/cbiffle-syntax-guide-imports 
syntax guide: discuss modules, imports.
 2015-09-17 00:42:13 +02:00
Niklas Larsson
abc76e137a Merge pull request #2619 from david-christiansen/substr-2 
Be more thorough in substring testing
 2015-09-17 00:41:44 +02:00
Niklas Larsson
724e78bfd5 Merge pull request #2620 from ben-schulz/fix/master/repl_desugarnats 
Add option to desugar nats in REPL output
 2015-09-17 00:41:31 +02:00
Cliff L. Biffle
33fb42675a syntax guide: discuss modules, imports. 
This discusses the previously-undocumented "import X as Y" facility.
This seemed like a good time to discuss the high-level file structure,
so I added a bit of that.
 2015-09-15 20:09:37 -07:00
ben-schulz
49fae22e4b Add option to desugar nats in REPL output 
Added option 'desugarnats' to REPL's ':set' and ':unset' commands.
Setting this option prevents the pretty-printer from resugaring terms
of type Nat, as resugaring may obscure unification performed by an
implicit search.  The 'desugarnats' option is set to 'false' by default.

Resolves: #2507
 2015-09-15 22:07:12 -05:00
David Christiansen
3a32759711 Merge pull request #2603 from Melvar/shift-vect 
Merge Data.VectType into Data.Vect, and cleanup
 2015-09-15 17:05:28 +02:00
David Raymond Christiansen
e9d9041f6b Be more thorough in substring testing 
Now it is also tested what happens with a positive offset and negative
length (the empty string should be returned).
 2015-09-15 15:57:46 +02:00
Niklas Larsson
f4352a75ba Merge pull request #2617 from david-christiansen/substr-2 
Substring as primitive
 2015-09-15 12:42:41 +02:00
David Raymond Christiansen
066e890a68 Substring as primitive 
Introduce a new primitive for taking substrings. This can't really be
done efficiently with strTail and strCons, so I think it deserves to
exist as a primitive. Implementations are included for the evaluator as
well as the C and JS backends. Other backends will need to implement it.
 2015-09-15 09:48:31 +02:00
Niklas Larsson
69d4b2a997 Merge pull request #2615 from melted/js_unicode 
Make a utf-8 string in getLine for Node
 2015-09-14 15:03:45 +02:00
Niklas Larsson
2869be1dec Make a utf-8 string in getLine for Node 2015-09-14 14:01:04 +02:00
David Christiansen
6fc713d2a9 Merge pull request #2606 from NightRa/patch-1 
Fix a typo in the Cast documentation
 2015-09-12 09:19:45 +02:00
David Christiansen
d583ff0ef8 Merge pull request #2607 from sdroege/faq-typo 
faq: Fix typo in argument name of ifThenElse
 2015-09-12 09:19:21 +02:00
Sebastian Dröge
f121da7417 faq: Fix typo in argument name of ifThenElse 2015-09-11 23:59:24 +02:00
Ilan Godik
053ffdce08 Fix a typo in the Cast documentation 2015-09-11 22:10:39 +03:00
Niklas Larsson
be157aabd7 Merge pull request #2604 from melted/clean_compile 
Remove the --yes-really flag from codegens
 2015-09-11 19:09:04 +02:00
Niklas Larsson
b19d03cfb9 Remove --yes-really 
See discussion on #2579
 2015-09-11 17:59:27 +02:00
Niklas Larsson
cb11c39a1c Cleanup in Compiler.hs 2015-09-11 15:50:12 +02:00
Melvar Chen
319d143697 Remove obsolete reflected tactic 
The search tactic and thus auto will do the same thing.
 2015-09-11 14:56:30 +02:00
Melvar Chen
6e49c84c5e Add Ordering composition and use it for Ord (Vect n a) 2015-09-11 14:56:30 +02:00
Melvar Chen
6b4c4d27b7 Give Vect.findIndices & Co a more useful type 2015-09-11 14:56:30 +02:00
Melvar Chen
3f24fac101 Clean up various Data.Vect functions 2015-09-11 14:56:30 +02:00
Melvar Chen
50b5031405 Merge VectType into Vect to be more like other Data.* 2015-09-11 14:56:30 +02:00
David Christiansen
fa6a50ad5e Merge pull request #2599 from scshunt/master 
Use uninhabited instance for nonempty.
 2015-09-10 17:32:20 +02:00
Sean Hunt
b9e9c52803 Add myself to CONTRIBUTORS. 2015-09-10 09:25:39 -04:00
Sean Hunt
8501e6d93b Use uninhabited instance for nonempty. 2015-09-10 09:18:04 -04:00
David Christiansen
70d197efd4 Merge pull request #2595 from Melvar/fix-tests 
Make test totality010 work when ncurses is enabled
 2015-09-09 08:22:53 +02:00
David Christiansen
0600e99ee9 Merge pull request #2596 from Melvar/fix-chr 
Make chr check for the correct range
 2015-09-09 08:22:21 +02:00
David Christiansen
1f8944f6da Merge pull request #2594 from david-christiansen/various-updates 
Updates and fixes
 2015-09-09 06:54:41 +02:00
Melvar Chen
52dd3090ed Make chr check for the correct range 2015-09-09 03:29:15 +02:00
Melvar Chen
d846ce79de Make test totality010 work when ncurses is enabled 2015-09-09 01:51:49 +02:00
David Raymond Christiansen
1cdc9ddfdc Reduce space leak through ugly DeepSeq hack 
The space leak documented in issue #2386 is helped by forcing the state
in a few places. Now, with the empty module, no space leak occurs, while
it grows by about 1 MB per 200 reloads with a large module. While
deepseqing the state is a hack, and should be better, I've not yet
improved on this and it does make Idris usable for repeated reloads of
large modules when using the interactive editing features.
 2015-09-08 20:13:52 +02:00
Niklas Larsson
c6acf7fe31 Merge pull request #2593 from melted/issue-2568 
Add exe to windows executables without extension when cleaning.
 2015-09-08 02:56:05 +02:00
Niklas Larsson
98eb1af0b6 Add exe to windows executables without extension when cleaning. 
So if it already has .exe, .js or something else it will not
be added.

Fixes #2568
 2015-09-08 02:03:12 +02:00
Niklas Larsson
73c6bb4e96 Merge pull request #2592 from melted/bit-pattern 
Allow pattern matching on BitX constants
 2015-09-07 23:54:40 +02:00
Niklas Larsson
8564250334 Allow pattern matching on BitX constants 2015-09-07 21:59:26 +02:00