bamboo/idris2dart

The Dart backend for Idris 2.

idris2dart

An Idris 2 code generator that outputs Dart code.

Why

To explore what cross-platform app development with Idris 2 powered by Flutter can look like and maybe build something beautiful along the way.

Status

• data types, pattern matching, etc
• basic Char, String and numeric primitives
• bidirectional FFI
• delay/force
• remaining cast primitives
• bounded int operations on Bits* values
• remaining IO primitives
• IOArray primitives

Building

1. Install the latest Idris 2 (must include the idris2api package)
2. make all
3. Add ./build/exec/idris2dart to your PATH or create an alias

Using

idris2dart is a fully functional Idris 2 environment except it comes with a single code generator, dart.

For example, to compile an Idris module to Dart, use:

$ idris2dart Main.idr -o main.dart

idris2dart's Issues

Foreign function argument values of type `Bool` should be converted to Dart `bool`

I don't know if this is something that it is just not implemented yet or its really a bug,

when I'm trying to use properties of flutter widgets that take a bool as parameter like obscureText from TextField widget, it compile to 0 or 1 instead of dart true or false

Make all stops with Error

Hi,

First of all, thanks very much for creating this project - it's a great idea and potentially beautiful thing!

However, I'm having an issues running Make all - I've tried on Mac and linux Ubuntu and I'm hitting the same issue.

I went through the steps here: https://github.com/idris-lang/Idris2/blob/master/INSTALL.md#2-installing-without-an-existing-idris-2 to install a self-hosted version of Idris2, I confirmed it was working by running the tests and then I ran Make install-api in clone of the Idris2 repo dir to install the API.

I also then followed the steps here https://github.com/idris-lang/Idris2/blob/master/INSTALL.md#2-installing-without-an-existing-idris-2 to check that I could make a new backend and it all seemed to be working.

But when I clone your project and run Make all and I get the following:

idris2 --build idris2dart.ipkg
1/3: Building Primitives (src/Primitives.idr)
2/3: Building Printer (src/Printer.idr)
Error: While processing right hand side of writeDocTo. While processing right hand side of writeDocTo,nSpaces. Undefined name replicate. 
Printer:131:17--131:26
 127 |   Nest w d => writeDocTo f d (nSpaces (fromInteger (cast w) + length i))
 128 |   Nil => pure ok
 129 |   where
 130 |     nSpaces : Nat -> String
 131 |     nSpaces i = replicate i ' '
                       ^^^^^^^^^
Did you mean: replace?
make: *** [Makefile:10: build/exec/idris2dart] Error 1

Any help with this would be much appreciated.

variable already declared in this scope

First, any way I can show support to your work? Really like what this project is doing.

I was playing around with idris2dart, and tried to compile itself to dart, but failed with some variable redefined errors:
https://gist.github.com/PoYen000227/59bd58f3b311122b6bdda4a9255b39e5

Is this a bug? Or is it planned to support self compiling?

Can't use named arguments inside defStatic

I'm trying to port the TextButton widget, but I get an error when I try to add the https://api.flutter.dev/flutter/material/TextButton/styleFrom.html static method

    defClass "TextButton" [
      extends "Widget",
      defConstructor "" [
        named (function [] void) "onPressed",
        named "ButtonStyle" "style",
        named "Widget" "child"
        ],
      defStatic "styleFrom" [ 
        named "Color" "primary",
        named "Color" "backgroundColor"
      ] "ButtonStyle"
    ]

error generated :

cd ./packages/flutter-ffi-generator && idris2 --build ./flutter-ffi-generator.ipkg
4/4: Building Main (src/Main.idr)
./packages/flutter-ffi-generator/build/exec/flutter-ffi-generator > ./packages/flutter/src/Flutter/FFI.idr
cd ./packages/flutter && idris2 --install ./flutter.ipkg
1/6: Building Flutter.FFI (src/Flutter/FFI.idr)
Error: Parse error at line 708:22:
Expected 'case', 'if', 'do', application or operator expression (next
tokens: [symbol ->, symbol ->, identifier PrimIO, identifier ButtonStyle, export, identifier styleFrom, symbol :, identifier HasIO, identifier io, symbol =>])
make: *** [Makefile:28: packages/flutter/build/installed] Error 1

if I make my argument positionnal like this

    defClass "TextButton" [
      extends "Widget",
      defConstructor "" [
        named (function [] void) "onPressed",
        named "ButtonStyle" "style",
        named "Widget" "child"
        ],
      defStatic "styleFrom" [ 
        positionnal "Color" "primary",
        positionnal "Color" "backgroundColor"
      ] "ButtonStyle"
    ]

I have no problems

A question regarding type safety of generated code

Hi @bamboo,

I'm new to Idris and was playing around with your code generator, seeing if it might be possible to generate dart library code:

I see that in the generated code, all generated dart types are dynamic, and in particular, primitive type information is lost. I was wondering if you could please explain why you implemented this way?

I realise that there will be many Idris types which cannot be canonically expressed in dart types, but for primitive types, might it be possible to map them to corresponding dart types? The aim would be to generate dart library code with more type information, so that e.g. the generated dart functions maintained some level of type safety.

This is probably more of a quest to try and understand things better myself rather than a feature request, however I would eventually be willing to help out if you thought this kind of thing would be possible/useful.

Your flutter examples doesn't compile anymore

Since you added these lines of code in flutter-ffi-generator

 defClass "Row" [
      extends "Widget",
      defConstructor "" [
        named (listOf "Widget") "children",
        named "MainAxisAlignment" "mainAxisAlignment"
      ]
    ],

I have this error

1/1: Building Main (lib/Main.idr)
Error: While processing right hand side of appHome. While processing right hand side of appHome,build. When unifying DartList Widget and typeOf ?p.
Undefined name Dart.Core.DartList. 

lib/Main.idr:19:23--24:13
 19 |           children @= !(widgets [
 20 |             !(Text.new "You have pushed the button this many times:" []),
 21 |             !(Text.new (show (get state)) [
 22 |               style @= headline4 (textTheme !(Theme.of_ context))
 23 |             ])
 24 |           ])

without it, I have no problem

Does not compile with latest Idris2

Idris2 version: Idris 2, version 0.2.1-b4b800e96

Older commits that compiles before are giving the same error, so perhaps it's something have changed in Idris2 itself?

Error log:

~ $ make
idris2 --build idris2dart.ipkg
2/2: Building Main (src/Main.idr)
Error: While processing right hand side of compileToDart. Undefined name .toList.

src/Main.idr:620:33--620:58
     |
 620 |   let imports' = dartImport <$> finalState.imports.toList
     |                                 ^^^^^^^^^^^^^^^^^^^^^^^^^

Error: dartCase is not covering.

src/Main.idr:514:3--517:11
 514 |   dartCase : {auto ctx : Ref Dart DartT}
 515 |     -> (Expression, Statement)
 516 |     -> Core Doc
 517 |   dartCase (e, s) = do

Calls non covering function Main.dartExp
Error: dartExp is not covering.

src/Main.idr:426:3--429:10
 426 |   dartExp : {auto ctx : Ref Dart DartT}
 427 |     -> Expression
 428 |     -> Core Doc
 429 |   dartExp e = case e of

Calls non covering functions: Main.dartName, Main.dartLambda
Error: dartForeign is not covering.

src/Main.idr:295:1--299:12
 295 | dartForeign : {auto ctx : Ref Dart DartT}
 296 |   -> Name -> ForeignDartSpec
 297 |   -> List CFType -> CFType
 298 |   -> Core Doc
 299 | dartForeign n (ForeignFunction f lib) args ret = do

Calls non covering function Main.dartName
Error: dartLambda is not covering.

src/Main.idr:423:3--424:13
 423 |   dartLambda : {auto ctx : Ref Dart DartT} -> List Name -> Statement -> Core Doc
 424 |   dartLambda ps s = pure (paramList ps <+> block !(dartStatement s))

Calls non covering function Main.paramList
Error: dartName is not covering.

src/Main.idr:67:1--68:9
 67 | dartName : Name -> Doc
 68 | dartName = text . dartNameString

Calls non covering function Main.dartNameString
Error: dartNameString is not covering.

src/Main.idr:55:1--56:15
 55 | dartNameString : Name -> String
 56 | dartNameString n = case n of

Calls non covering function Main.case block in dartNameString
Error: dartNamedParam is not covering.

src/Main.idr:492:3--493:17
 492 |   dartNamedParam : {auto ctx : Ref Dart DartT} -> (Expression, String, Expression) -> Core Doc
 493 |   dartNamedParam (ty, name, value) = do

Calls non covering function Main.dartExp
Error: dartPrimFnExt is not covering.

src/Main.idr:464:3--466:16
 464 |   dartPrimFnExt : {auto ctx : Ref Dart DartT}
 465 |     -> Name -> List Expression -> Core Doc
 466 |   dartPrimFnExt

Calls non covering function Main.dartExp
Error: dartStatement is not covering.

src/Main.idr:543:3--546:16
 543 |   dartStatement : {auto ctx : Ref Dart DartT}
 544 |     -> Statement
 545 |     -> Core Doc
 546 |   dartStatement s = case s of

Calls non covering functions: Main.dartName, Main.foreignDecl, Main.dartLambda, Main.dartExp, Main.dartSwitch
Error: dartSwitch is not covering.

src/Main.idr:533:3--538:13
 533 |   dartSwitch : {auto ctx : Ref Dart DartT}
 534 |     -> Doc
 535 |     -> List (Expression, Statement)
 536 |     -> Maybe Statement
 537 |     -> Core Doc
 538 |   dartSwitch e cases def = do

Calls non covering function Main.dartCase
Error: dartVar is not covering.

src/Main.idr:575:3--580:10
 575 |   dartVar : {auto ctx : Ref Dart DartT}
 576 |     -> (keyword : Doc)
 577 |     -> Name
 578 |     -> Maybe Expression
 579 |     -> Core Doc
 580 |   dartVar kw n init = case init of

Calls non covering functions: Main.dartName, Main.dartExp
Error: foreignDecl is not covering.

src/Main.idr:329:1--333:12
 329 | foreignDecl : {auto ctx : Ref Dart DartT}
 330 |   -> Name -> List String
 331 |   -> List CFType -> CFType
 332 |   -> Core Doc
 333 | foreignDecl n ss args ret = case n of

Calls non covering functions: Main.dartName, Main.dartName, Main.dartForeign
Error: paramList is not covering.

src/Main.idr:115:1--116:10
 115 | paramList : List Name -> Doc
 116 | paramList ps = tupled ((dynamic' <+>) . dartName <$> ps)

Calls non covering function Main.dartName
make: *** [build/exec/idris2dart] Error 1