Skip to content

Commit

Permalink
Fix indentation, add output in documentation
Browse files Browse the repository at this point in the history
  • Loading branch information
mmhelloworld authored Jul 17, 2024
1 parent a008d55 commit 4da5129
Showing 1 changed file with 18 additions and 4 deletions.
22 changes: 18 additions & 4 deletions docs/source/ffi/calling-idris-from-java.rst
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,7 @@ Exporting Idris Functions
"returnType": "String"
}
"""
exportStringReplicate :Nat -> Char -> String
exportStringReplicate : Nat -> Char -> String
exportStringReplicate = String.replicate
This code exports ``replicate`` function from ``Data.String`` Idris module. The export block starting with ``%export``
Expand Down Expand Up @@ -87,7 +87,7 @@ integers which Java code shouldn't rely on.
idris/data/List
helloworld/Color
"""
typeExports: List String
typeExports : List String
typeExports = []
Similar to ``jvmExports`` block explained above, ``typeExports`` is a special export function that exports Idris types
Expand All @@ -112,7 +112,7 @@ Exporting Idris functions with Generic Types
jvm:export
IdrisList
"""
typeExports: List String
typeExports : List String
typeExports = []
%export """
Expand Down Expand Up @@ -239,7 +239,7 @@ Here is a complete example in Idris and Java:
Show
Color
"""
typeExports: List String
typeExports : List String
typeExports = []
%export """
Expand Down Expand Up @@ -462,6 +462,20 @@ Java calling the Idris functions:
}
This is the output:

.. code-block:: text
[23, 45]
["foo", "bar"]
[Red, Blue]
Green
Blue
Just Green
Nothing
AAAAAAAAAA
Here line numbers 29-33 retrieve type class instances for different types and the instances are passed in the lines
below when ``show`` function is called. Another thing to note here is that when we call generic Idris functions, Idris
types that are wrapped in Java types needs to be converted before passing to Idris functions. For example, line 23
Expand Down

0 comments on commit 4da5129

Please sign in to comment.