Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

#140 Support creating Java lambdas, export Idris functions as Java classes, constructors, fields and functions #170

Merged
merged 10 commits into from
Jan 31, 2024

Conversation

mmhelloworld
Copy link
Owner

@mmhelloworld mmhelloworld commented Jan 25, 2024

  • Support passing Idris functions as Java lambdas like:
Stream.fromCollection list >>=
            (flip map (\s => toPrim $ pure $ (s ++ " idris"))) >>=
            (flip filter (\s => toPrim $ pure $ (length s > 15))) >>=
            count
  • Export Idris functions as Java classes, constructors, fields and functions
  • Support adding annotions on the exported Java classes, constructors, fields and functions. We would now be able to write Spring Boot applications in Idris!
namespace Employee
    %export """
            jvm:public Employee
            {
                "annotations": [
                    {"Data": {}},
                    {"AllArgsConstructor": {
                        "exclude": ["id"]}},
                    {"NoArgsConstructor": {}},
                    {"Entity": {}}
                ],
                "fields": {
                    "id": {
                        "type": "java/lang/Long",
                        "annotations": [
                            {"Id": {}},
                            {"GeneratedValue": {}}
                        ]
                    },
                    "name": "String",
                    "role": "String"
                }
            }
            """
    public export
    Employee : Type
    Employee = Struct "io/github/mmhelloworld/helloworld/Employee" []

namespace EmployeeController

    %export """
            jvm:public EmployeeController
            {
                "fields": {
                    "employeeRepository": {
                        "modifiers": ["private", "final"],
                        "type": "EmployeeRepository"
                    }
                },
                "annotations": [
                    {"AllArgsConstructor": {}},
                    {"Getter": {}},
                    {"RestController": {}}
                ]
            }
            """
    public export
    EmployeeController : Type
    EmployeeController = Struct "io/github/mmhelloworld/helloworld/EmployeeController" []

    %foreign "jvm:.getEmployeeRepository"
    repository : EmployeeController -> PrimIO EmployeeRepository

    %export """
         jvm:public getEmployees!
         {
             "annotations": [
                 {"Get": ["/employees"]}
             ],
             "enclosingType": "EmployeeController",
              "arguments": [
                  {
                      "type": "EmployeeController"
                  }
              ],
              "returnType": "List<Employee>"
         }
     """
    employees : EmployeeController -> PrimIO (JList Employee)
    employees this = toPrim $ do
        employeeRepository <- fromPrim $ repository this
        findAll {id=Int64} (subtyping employeeRepository)
  • Support generic type parameters like JpaRepository<Employee, Long>. Type variables are not supported in this PR.
  • Generate no args constructor, all args constructor, required args constructor, equals, hashCode, toString , getters and setters from Idris while exporting a Java class
  • Support accessing Java fields
  • Support accessing class literals in Idris like classLiteral {ty=PayrollApplication}. Equivalent Java would be PayrollApplication.class
  • Support Java's instanceof and reference equality to be able to implement Java methods like equals in Idris
  • Support JVM arrays
  • Avoid requiring explicit types for foreign calls. For the functions below, we, no longer, have to provide parameter and return types
namespace JInteger
    public export
    JInteger : Type
    JInteger = Struct "java/lang/Integer" []

    export
    %foreign "jvm:valueOf,java/lang/Integer"
    box : Int -> JInteger

    export
    %foreign "jvm:.intValue"
    unbox : JInteger -> Int

@mmhelloworld mmhelloworld force-pushed the feature/issue-140-idris-from-java branch 6 times, most recently from 4817c2b to bd905e8 Compare January 26, 2024 04:52
@mmhelloworld mmhelloworld force-pushed the feature/issue-140-idris-from-java branch from bd905e8 to 4509561 Compare January 30, 2024 23:12
@mmhelloworld mmhelloworld self-assigned this Jan 31, 2024
@mmhelloworld mmhelloworld merged commit 7702c45 into main Jan 31, 2024
8 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

1 participant