Edwin Brady
90ec19f053
Merge pull request #1354 from edwinb/casetransform
...
Add case+lambda transformation
2021-04-29 14:59:11 +01:00
Johann Rudloff
18f9c5484d
[ refactor ] Pass through Used vars instead of creating and merging
2021-04-29 15:41:23 +02:00
Edwin Brady
3bb4333ac3
Fix whitespace error
2021-04-29 13:47:31 +01:00
Edwin Brady
c3e5689a62
Add case+lambda transformation
...
If all branches in a case block are a lambda, lift the lambda out. In
many cases, this can save creating a closure then evaluating it
immediately, because the function is already applied to the extra
argument.
This happens in particular with IO based code, where the extra argument
is the world token. One place where this transformation has a big effect
is 'evalRef' so the evaluator is now a bit faster (about 20% on the
small benchmark I tried it on - but no guarantees that's going to happen
on other examples!)
2021-04-29 13:44:13 +01:00
Johann Rudloff
8d21a292d0
Add Text.PrettyPrint.Prettyprinter.Render.HTML to contrib as well
2021-04-29 13:49:04 +02:00
Johann Rudloff
9591b147a4
[ cleanup ] Remove unused helper function
2021-04-29 13:41:34 +02:00
Johann Rudloff
f656b97928
[ refactor ] Move all HTML-related code out of the Idris.Package module
2021-04-29 11:56:47 +02:00
Johann Rudloff
8012736e83
[ fix ] Add new module to the ipkg file
2021-04-29 11:29:37 +02:00
Johann Rudloff
0b9831e3c5
[ refactor ] Move HTML docs specific code into its own module
2021-04-29 10:47:31 +02:00
Johann Rudloff
af26a73504
[ cleanup ] Most reAnnotate calls in Idris.REPL can be skipped
...
Since we have the locally overloaded `prettyTerm`, we can move most
functions in the `REPL` module back to `IdrisAnn`, reducing the overall
size of the PR.
2021-04-29 10:11:58 +02:00
Johann Rudloff
4e937246b7
[ cleanup ] Remove some (now) unused Doc annotations, restore original colors
2021-04-29 10:07:13 +02:00
Guillaume ALLAIS
d9176d47db
[ fix #633 ] Pattern-matching on functions is illegal
2021-04-28 20:25:45 +01:00
Guillaume ALLAIS
7c5944e811
[ cleanup ] if then else pure () is when
2021-04-28 20:25:45 +01:00
Guillaume ALLAIS
afb865f3de
[ debug ] cleanup the messages
2021-04-28 20:25:45 +01:00
Joey Eremondi
59975eb09d
[ refactor ] type inference and evaluation for the REPL ( #1348 )
2021-04-28 20:25:29 +01:00
Johann Rudloff
8550de29bb
Use Data.Strings instead of Data.String for compatibility with previous release
2021-04-28 20:05:51 +02:00
Johann Rudloff
fd0690dc08
Add parentheses around operator names in HTML docs
2021-04-28 18:46:20 +02:00
Johann Rudloff
1ac28921df
Merge remote-tracking branch 'origin/master' into mkdoc-rework
2021-04-28 18:45:24 +02:00
Johann Rudloff
906a353e0a
Finish mkdocs rework
2021-04-28 18:28:23 +02:00
Johann Rudloff
c1dd237679
Introduce IdrisSyntax annotation type
2021-04-28 16:38:45 +02:00
Giuseppe Lomurno
cab4403357
Typo in findInTree
2021-04-28 15:24:11 +01:00
Johann Rudloff
139940d837
[ refactor ] Remove Core from Used-manipulating functions
2021-04-28 13:44:49 +02:00
G. Allais
96a2809f62
[ fix #1169 ] primitive types are not NTCon ( #1340 )
2021-04-28 09:33:27 +01:00
Stefan Höck
bbea929cf3
[ refactor ] Cleanup integral primops ( #1211 )
2021-04-28 09:32:46 +01:00
G. Allais
d32daaf36a
[ fix ] properly handle Namespace blocks for DocStrings ( #1342 )
2021-04-28 09:31:01 +01:00
Johann Rudloff
17af0230ef
Update doc generation so it compiles with latest Idris master
2021-04-28 09:38:11 +02:00
Guillaume ALLAIS
4224c58651
[ fix ] print infix operators with parens
...
I noticed that e.g. List's (::) was not printed correctly in `:doc`
so here's a fix.
2021-04-27 14:12:48 +01:00
Jonathan Chan
72e45d959e
[ REPL ] Added commands :ti and :opts ( #1241 )
...
:ti does the same thing as :t, but shows the type as if showimplicits
were set. The value of REPLOpt.ShowImplicits is unchanged.
:opts shows the current values of the options that can be set or unset
with :set/:unset. (This already existed in REPLCmd.GetOpts, idk why it
just wasn't in Parser.parserCommandsForHelp.)
Also fixed the spacing of the help message.
2021-04-27 10:27:50 +01:00
Johann Rudloff
b0ede0f2b1
Get rid of multi-line strings to fix build from previous version
2021-04-26 23:02:28 +02:00
Johann Rudloff
3dd5878e22
[ wip ] Improve HTML docs with better annotations
2021-04-26 23:02:25 +02:00
Johann Rudloff
a012e64ef2
Add Libraries.Text.PrettyPrint.Prettyprinter.Render.HTML to idris2api's modules list
2021-04-26 22:59:23 +02:00
Johann Rudloff
e5a1898692
Fix tests for commit: Transition :doc command to use PrettyPrint instead of plain strings
2021-04-26 22:59:06 +02:00
Johann Rudloff
b978816b53
[lazy rebase] Update makeDocs for new getDocsForName implementation ((Doc IdrisAnn) instead of String)
2021-04-26 22:55:48 +02:00
Johann Rudloff
0b9c435aa7
Begin refactoring: extract HTML generation to separate module
2021-04-26 22:48:24 +02:00
Johann Rudloff
ae9da0e8ce
Reformat docs CSS file to comply with code style guide (and make the linter happy)
2021-04-26 22:48:24 +02:00
Johann Rudloff
e8ca7c85e3
Update to accomodate for latest Idris2 changes
2021-04-26 22:48:24 +02:00
Johann Rudloff
295b7638af
Initial implementation to get links working
...
The process is a bit hacky, but I could not find an easier way.
During desugaring we set the "fullNamespace" option, so that namespaces
are not lost. When the (pretty printed) Doc is rendered to HTML, the
namespaces are used to generate the link destination, but are removed
before generating the "user-visible" string (the text inside the "<a>"
tag).
2021-04-26 22:48:24 +02:00
Johann Rudloff
13cba46188
Show types, show names inside module without namespace
2021-04-26 22:48:21 +02:00
Johann Rudloff
68a5f1f1b7
Copy styles.css from support into generated docs/ folder
2021-04-26 22:45:14 +02:00
Johann Rudloff
1a025131e3
Exact namespace comparison to avoid duplicated entries for re-exported names
2021-04-26 22:44:03 +02:00
Johann Rudloff
1de8b4497c
HTML-Escape full documentation body
2021-04-26 22:44:03 +02:00
Johann Rudloff
3baab8abea
First draft version of --mkdoc CLI switch
2021-04-26 22:44:00 +02:00
Johann Rudloff
d66bbe030a
Improve LambdaLift by dropping unused variables
2021-04-26 09:57:13 +02:00
Johann Rudloff
1afece45c5
Move hand specialised foldlC into Core.Core
2021-04-26 09:55:56 +02:00
Tung Alissa
881a5e7fbc
[ fix #1328 ] print infix functions enclosed in grave accents ( #1331 )
2021-04-25 18:56:08 +01:00
stefan-hoeck
0858c26dcf
[ refactor ] renamed value to runConst
2021-04-25 10:41:36 +01:00
stefan-hoeck
7863636490
[ new ] add Contravariant interface
2021-04-25 10:41:36 +01:00
stefan-hoeck
047fdb50dd
[ new ] missing Identity implementations
2021-04-25 10:41:36 +01:00
stefan-hoeck
cb7add2eca
[ new ] add Const applicative functor
2021-04-25 10:41:36 +01:00
Guardian Spirit
15bd6823d2
Add identity cast ( #1332 )
2021-04-25 09:22:01 +01:00
