Skip to content

Commit d3105a1

Browse files
committed
#104 Enhancements, bug fixes to support Idris 2
1 parent bdedea3 commit d3105a1

File tree

60 files changed

+979
-418
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

60 files changed

+979
-418
lines changed

.gitignore

+2
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,6 @@
11
# Java
22
*.class
3+
*.jar
34

45
# Idris
56
*.ibc
@@ -28,3 +29,4 @@ buildNumber.properties
2829
.mvn/timing.properties
2930

3031
.DS_Store
32+
*.log

.travis.yml

+3-2
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,7 @@ env:
1212
before_install:
1313
- docker pull mmhelloworld/idris:1.3.2
1414
- mkdir -p $HOME/bin/idris-packages $IDRIS_JVM_HOME
15-
- wget https://github.com/mmhelloworld/idris-jvm/releases/download/v1.0-SNAPSHOT-20190525/idris-jvm.zip
15+
- wget https://github.com/mmhelloworld/idris-jvm/releases/download/v1.0-SNAPSHOT-20190914/idris-jvm.zip
1616
- unzip -o idris-jvm.zip -d $HOME/bin
1717
- export PATH=`pwd`/bin/travis:$IDRIS_JVM_HOME/codegen/bin:$HOME/.local/bin:$PATH
1818
- export PROJECT_ROOT=`pwd`
@@ -21,7 +21,8 @@ before_install:
2121
script:
2222
- lsof -ti ":$(cat $IDRIS_JVM_HOME/.idrisjvmport)" | xargs --no-run-if-empty kill
2323
- unzip -o idris-jvm-codegen-launcher/target/idris-jvm.zip -d $HOME/bin
24-
- mvn -pl :idris-jvm-integration-test test -B
24+
- export IDRIS_JVM_HOME=${HOME}/bin/idris-jvm
25+
- bin/travis/travis_long mvn -pl :idris-jvm-integration-test test -B
2526
before_deploy:
2627
- git config --local user.name mmhelloworld
2728
- git config --local user.email $USER_EMAIL

idris-jvm-codegen-launcher/src/main/java/io/github/mmhelloworld/idrisjvm/codegen/launcher/IdrisJvmCodegenLauncher.java

+2-1
Original file line numberDiff line numberDiff line change
@@ -23,6 +23,7 @@
2323

2424
import static java.lang.Integer.parseInt;
2525
import static java.lang.String.format;
26+
import static java.util.Arrays.asList;
2627
import static java.util.stream.Collectors.toList;
2728

2829
public class IdrisJvmCodegenLauncher {
@@ -95,7 +96,7 @@ public void run() {
9596
}
9697

9798
private void send(final String[] args) {
98-
List<String> endpointArgs = new ArrayList<>(Arrays.asList(args));
99+
List<String> endpointArgs = new ArrayList<>(asList(args));
99100
endpointArgs.add(System.getProperty("user.dir"));
100101
int port = getPort().orElseThrow(() -> new RuntimeException("Idris JVM codegen server is not running"));
101102
ResponseEntity<String> response = restTemplate.postForEntity("http://localhost:" + port,

idris-jvm-core/pom.xml

+3-1
Original file line numberDiff line numberDiff line change
@@ -106,8 +106,10 @@
106106
<argument>${idris.srcdir}/IdrisJvm/Core/Function.idr</argument>
107107
<argument>${idris.srcdir}/IdrisJvm/Core/JAsm.idr</argument>
108108
<argument>${idris.srcdir}/IdrisJvm/Core/Operator.idr</argument>
109+
<argument>--cg-opt</argument>
110+
<argument>--classes-dir=classes</argument>
109111
<argument>-o</argument>
110-
<argument>${project.build.outputDirectory}</argument>
112+
<argument>${project.build.directory}/idrisjvmcore</argument>
111113
</arguments>
112114
</configuration>
113115
</execution>

idris-jvm-core/src/main/idris/IdrisJvm/Core/Asm.idr

-10
Original file line numberDiff line numberDiff line change
@@ -165,8 +165,6 @@ mutual
165165
| InterfaceDesc ClassName
166166
| ArrayDesc FieldTypeDescriptor
167167
| IdrisExportDesc ClassName
168-
| NullableStrDesc
169-
| NullableRefDesc ClassName
170168

171169
data FieldTypeDescriptor = FieldTyDescByte
172170
| FieldTyDescChar
@@ -185,8 +183,6 @@ mutual
185183
(InterfaceDesc className1 ) == (InterfaceDesc className2 ) = className1 == className2
186184
(ArrayDesc elemDesc1 ) == (ArrayDesc elemDesc2 ) = elemDesc1 == elemDesc2
187185
(IdrisExportDesc className1 ) == (IdrisExportDesc className2 ) = className1 == className2
188-
(NullableStrDesc ) == (NullableStrDesc ) = True
189-
(NullableRefDesc className1 ) == (NullableRefDesc className2 ) = className1 == className2
190186
_ == _ = False
191187

192188
Eq FieldTypeDescriptor where
@@ -272,8 +268,6 @@ mutual
272268
show (InterfaceDesc className) = "InterfaceDesc " ++ show className
273269
show (ArrayDesc tyDesc) = "ArrayDesc " ++ show tyDesc
274270
show (IdrisExportDesc className) = "IdrisExportDesc " ++ show className
275-
show NullableStrDesc = "NullableStrDesc"
276-
show (NullableRefDesc className) = "NullableRefDesc" ++ show className
277271

278272
Show FieldTypeDescriptor where
279273
show FieldTyDescByte = "FieldTyDescByte"
@@ -296,16 +290,12 @@ mutual
296290
asmRefTyDesc (ClassDesc c) = "L" ++ c ++ ";"
297291
asmRefTyDesc (IdrisExportDesc c) = "L" ++ c ++ ";"
298292
asmRefTyDesc (InterfaceDesc c) = "L" ++ c ++ ";"
299-
asmRefTyDesc (NullableRefDesc c) = "L" ++ c ++ ";"
300-
asmRefTyDesc NullableStrDesc = "Ljava/lang/String;"
301293
asmRefTyDesc (ArrayDesc ty) = "[" ++ asmFieldTypeDesc ty
302294

303295
refTyClassName : ReferenceTypeDescriptor -> ClassName
304296
refTyClassName (ClassDesc c) = c
305297
refTyClassName (InterfaceDesc c) = c
306298
refTyClassName (IdrisExportDesc c) = c
307-
refTyClassName (NullableRefDesc c) = c
308-
refTyClassName NullableStrDesc = "java/lang/String"
309299
refTyClassName arr@(ArrayDesc _) = asmRefTyDesc arr
310300

311301
asmFieldTypeDesc : FieldTypeDescriptor -> String

idris-jvm-core/src/main/idris/IdrisJvm/Core/Common.idr

+52-58
Original file line numberDiff line numberDiff line change
@@ -313,6 +313,34 @@ cgCast (Ref ty1) (Ref ty2) = when (ty1 /= ty2) $ checkcast ty2
313313

314314
cgCast _ _ = pure ()
315315

316+
loadAndBox : (Int -> Asm ()) -> Asm () -> InferredTypeStore -> LVar -> Asm ()
317+
loadAndBox loadOp boxOp sourceLocTys var = let op = \index => do loadOp index; boxOp
318+
in opWithWordSize sourceLocTys op var
319+
320+
loadAndBoxBool : InferredTypeStore -> LVar -> Asm ()
321+
loadAndBoxBool = loadAndBox Iload boxBool
322+
323+
loadAndBoxByte : InferredTypeStore -> LVar -> Asm ()
324+
loadAndBoxByte = loadAndBox Iload boxByte
325+
326+
loadAndBoxChar : InferredTypeStore -> LVar -> Asm ()
327+
loadAndBoxChar = loadAndBox Iload boxChar
328+
329+
loadAndBoxShort : InferredTypeStore -> LVar -> Asm ()
330+
loadAndBoxShort = loadAndBox Iload boxShort
331+
332+
loadAndBoxInt : InferredTypeStore -> LVar -> Asm ()
333+
loadAndBoxInt = loadAndBox Iload boxInt
334+
335+
loadAndBoxLong : InferredTypeStore -> LVar -> Asm ()
336+
loadAndBoxLong = loadAndBox Lload boxLong
337+
338+
loadAndBoxFloat : InferredTypeStore -> LVar -> Asm ()
339+
loadAndBoxFloat = loadAndBox Fload boxFloat
340+
341+
loadAndBoxDouble : InferredTypeStore -> LVar -> Asm ()
342+
loadAndBoxDouble = loadAndBox Dload boxDouble
343+
316344
loadVar : InferredTypeStore -> (srcTy: InferredType) -> (targetTy: InferredType) -> LVar -> Asm ()
317345
loadVar sourceLocTys IBool IBool var = opWithWordSize sourceLocTys Iload var
318346
loadVar sourceLocTys IByte IByte var = opWithWordSize sourceLocTys Iload var
@@ -330,63 +358,29 @@ loadVar sourceLocTys IFloat IDouble var = opWithWordSize sourceLocTys (\var => d
330358
loadVar sourceLocTys IDouble IDouble var = opWithWordSize sourceLocTys Dload var
331359
loadVar sourceLocTys IDouble IFloat var = opWithWordSize sourceLocTys (\var => do Dload var; D2f) var
332360

333-
loadVar sourceLocTys IBool IUnknown var =
334-
let loadInstr = \index => do Iload index; boxBool
335-
in opWithWordSize sourceLocTys loadInstr var
336-
loadVar sourceLocTys IBool (Ref _) var =
337-
let loadInstr = \index => do Iload index; boxBool
338-
in opWithWordSize sourceLocTys loadInstr var
361+
loadVar sourceLocTys IBool IUnknown var = loadAndBoxBool sourceLocTys var
362+
loadVar sourceLocTys IBool (Ref _) var = loadAndBoxBool sourceLocTys var
339363

340-
loadVar sourceLocTys IByte IUnknown var =
341-
let loadInstr = \index => do Iload index; boxByte
342-
in opWithWordSize sourceLocTys loadInstr var
343-
loadVar sourceLocTys IByte (Ref _) var =
344-
let loadInstr = \index => do Iload index; boxByte
345-
in opWithWordSize sourceLocTys loadInstr var
364+
loadVar sourceLocTys IByte IUnknown var = loadAndBoxByte sourceLocTys var
365+
loadVar sourceLocTys IByte (Ref _) var = loadAndBoxByte sourceLocTys var
346366

347-
loadVar sourceLocTys IChar IUnknown var =
348-
let loadInstr = \index => do Iload index; boxChar
349-
in opWithWordSize sourceLocTys loadInstr var
350-
351-
loadVar sourceLocTys IChar (Ref _) var =
352-
let loadInstr = \index => do Iload index; boxChar
353-
in opWithWordSize sourceLocTys loadInstr var
367+
loadVar sourceLocTys IChar IUnknown var = loadAndBoxChar sourceLocTys var
368+
loadVar sourceLocTys IChar (Ref _) var = loadAndBoxChar sourceLocTys var
354369

355-
loadVar sourceLocTys IShort IUnknown var =
356-
let loadInstr = \index => do Iload index; boxShort
357-
in opWithWordSize sourceLocTys loadInstr var
358-
loadVar sourceLocTys IShort (Ref _) var =
359-
let loadInstr = \index => do Iload index; boxShort
360-
in opWithWordSize sourceLocTys loadInstr var
370+
loadVar sourceLocTys IShort IUnknown var = loadAndBoxShort sourceLocTys var
371+
loadVar sourceLocTys IShort (Ref _) var = loadAndBoxShort sourceLocTys var
361372

362-
loadVar sourceLocTys IInt IUnknown var =
363-
let loadInstr = \index => do Iload index; boxInt
364-
in opWithWordSize sourceLocTys loadInstr var
365-
loadVar sourceLocTys IInt (Ref _) var =
366-
let loadInstr = \index => do Iload index; boxInt
367-
in opWithWordSize sourceLocTys loadInstr var
368-
369-
loadVar sourceLocTys ILong IUnknown var =
370-
let loadInstr = \index => do Lload index; boxLong
371-
in opWithWordSize sourceLocTys loadInstr var
372-
373-
loadVar sourceLocTys ILong (Ref _) var =
374-
let loadInstr = \index => do Lload index; boxLong
375-
in opWithWordSize sourceLocTys loadInstr var
373+
loadVar sourceLocTys IInt IUnknown var = loadAndBoxInt sourceLocTys var
374+
loadVar sourceLocTys IInt (Ref _) var = loadAndBoxInt sourceLocTys var
376375

377-
loadVar sourceLocTys IFloat IUnknown var =
378-
let loadInstr = \index => do Fload index; boxFloat
379-
in opWithWordSize sourceLocTys loadInstr var
380-
loadVar sourceLocTys IFloat (Ref _) var =
381-
let loadInstr = \index => do Fload index; boxFloat
382-
in opWithWordSize sourceLocTys loadInstr var
376+
loadVar sourceLocTys ILong IUnknown var = loadAndBoxLong sourceLocTys var
377+
loadVar sourceLocTys ILong (Ref _) var = loadAndBoxLong sourceLocTys var
383378

384-
loadVar sourceLocTys IDouble IUnknown var =
385-
let loadInstr = \index => do Dload index; boxDouble
386-
in opWithWordSize sourceLocTys loadInstr var
387-
loadVar sourceLocTys IDouble (Ref _) var =
388-
let loadInstr = \index => do Dload index; boxDouble
389-
in opWithWordSize sourceLocTys loadInstr var
379+
loadVar sourceLocTys IFloat IUnknown var = loadAndBoxFloat sourceLocTys var
380+
loadVar sourceLocTys IFloat (Ref _) var = loadAndBoxFloat sourceLocTys var
381+
382+
loadVar sourceLocTys IDouble IUnknown var = loadAndBoxDouble sourceLocTys var
383+
loadVar sourceLocTys IDouble (Ref _) var = loadAndBoxDouble sourceLocTys var
390384

391385
loadVar sourceLocTys IUnknown IBool var =
392386
let loadInstr = \index => do Aload index; boolObjToBool
@@ -428,10 +422,10 @@ loadVar sourceLocTys (Ref _) IInt var =
428422
let loadInstr = \index => do Aload index; objToInt
429423
in opWithWordSize sourceLocTys loadInstr var
430424

431-
loadVar sourceLocTys IUnknown ILong var =
425+
loadVar sourceLocTys IUnknown ILong var =
432426
let loadInstr = \index => do Aload index; longObjToLong
433427
in opWithWordSize sourceLocTys loadInstr var
434-
loadVar sourceLocTys (Ref _) ILong var =
428+
loadVar sourceLocTys (Ref _) ILong var =
435429
let loadInstr = \index => do Aload index; longObjToLong
436430
in opWithWordSize sourceLocTys loadInstr var
437431

@@ -442,10 +436,10 @@ loadVar sourceLocTys (Ref _) IFloat var =
442436
let loadInstr = \index => do Aload index; objToFloat
443437
in opWithWordSize sourceLocTys loadInstr var
444438

445-
loadVar sourceLocTys IUnknown IDouble var =
439+
loadVar sourceLocTys IUnknown IDouble var =
446440
let loadInstr = \index => do Aload index; objToDouble
447441
in opWithWordSize sourceLocTys loadInstr var
448-
loadVar sourceLocTys (Ref _) IDouble var =
442+
loadVar sourceLocTys (Ref _) IDouble var =
449443
let loadInstr = \index => do Aload index; objToDouble
450444
in opWithWordSize sourceLocTys loadInstr var
451445

@@ -454,13 +448,13 @@ loadVar sourceLocTys IUnknown arr@(IArray _) var =
454448
in opWithWordSize sourceLocTys loadInstr var
455449
loadVar sourceLocTys (Ref _) arr@(IArray _) var =
456450
let loadInstr = \index => do Aload index; Checkcast $ getInferredTyDesc arr
457-
in opWithWordSize sourceLocTys loadInstr var
451+
in opWithWordSize sourceLocTys loadInstr var
458452

459-
loadVar sourceLocTys IUnknown (Ref ty2) var =
453+
loadVar sourceLocTys IUnknown (Ref ty2) var =
460454
let loadInstr = \index => do Aload index; checkcast ty2
461455
in opWithWordSize sourceLocTys loadInstr var
462456

463-
loadVar sourceLocTys (Ref ty1) (Ref ty2) var =
457+
loadVar sourceLocTys (Ref ty1) (Ref ty2) var =
464458
let loadInstr = \index => do Aload index; when (ty1 /= ty2) $ checkcast ty2
465459
in opWithWordSize sourceLocTys loadInstr var
466460

idris-jvm-core/src/main/idris/IdrisJvm/Core/Foreign.idr

-22
Original file line numberDiff line numberDiff line change
@@ -24,18 +24,6 @@ data JForeign = JStatic String String
2424
| JLambda String String
2525
| JInstanceOf String
2626

27-
javaToIdris : TypeDescriptor -> Asm ()
28-
javaToIdris (FieldDescriptor FieldTyDescBoolean) = pure ()
29-
javaToIdris (FieldDescriptor FieldTyDescByte) = pure ()
30-
javaToIdris (FieldDescriptor FieldTyDescShort) = pure ()
31-
javaToIdris (FieldDescriptor FieldTyDescInt) = pure ()
32-
javaToIdris (FieldDescriptor FieldTyDescChar) = pure ()
33-
javaToIdris (FieldDescriptor FieldTyDescLong) = pure ()
34-
javaToIdris (FieldDescriptor FieldTyDescFloat) = pure ()
35-
javaToIdris (FieldDescriptor FieldTyDescDouble) = pure ()
36-
javaToIdris VoidDescriptor = Aconstnull
37-
javaToIdris _ = pure ()
38-
3927
javaReturn : TypeDescriptor -> Asm ()
4028
javaReturn VoidDescriptor = Return
4129
javaReturn (FieldDescriptor FieldTyDescBoolean) = Ireturn
@@ -70,13 +58,9 @@ mutual
7058

7159
fdescRefDescriptor desc@(FApp "JVM_ArrayT" [_, elemDesc]) = ArrayDesc $ fdescFieldDescriptor elemDesc
7260

73-
fdescRefDescriptor desc@(FApp "JVM_Nullable" [FApp "Class" [FStr typeName]]) = NullableRefDesc typeName
74-
fdescRefDescriptor desc@(FApp "JVM_Nullable" [FApp "Interface" [FStr typeName]]) = NullableRefDesc typeName
75-
7661
fdescRefDescriptor (FCon "JVM_Str") = ClassDesc "java/lang/String"
7762
fdescRefDescriptor (FCon "JVM_BigInteger") = ClassDesc "java/math/BigInteger"
7863
fdescRefDescriptor (FStr exportedType) = IdrisExportDesc exportedType
79-
fdescRefDescriptor (FCon "JVM_NullableStr") = NullableStrDesc
8064
fdescRefDescriptor desc = jerror $ "Invalid reference type descriptor: " ++ show desc
8165

8266

@@ -192,10 +176,6 @@ parseDescriptor returns ffi argsDesc = tryParseStaticMethodDescriptor returns ff
192176
(FieldDescriptor (FieldTyDescReference (ArrayDesc _))) => jerror "No constructors for array types"
193177
(FieldDescriptor (FieldTyDescReference (IdrisExportDesc _))) =>
194178
jerror "Cannot invoke constructor of Idris exported type"
195-
(FieldDescriptor (FieldTyDescReference (NullableStrDesc))) =>
196-
jerror "A constructor cannot return a nullable string"
197-
(FieldDescriptor (FieldTyDescReference (NullableRefDesc _))) =>
198-
jerror "A constructor cannot return a nullable reference"
199179
else
200180
tryParseNewArrayDescriptor returns ffiDesc argsDesc
201181
tryParseConstructorDescriptor returns ffi argsDesc = tryParseNewArrayDescriptor returns ffi argsDesc
@@ -224,8 +204,6 @@ parseDescriptor returns ffi argsDesc = tryParseStaticMethodDescriptor returns ff
224204
then case fdescRefDescriptor declClass of
225205
ClassDesc cname => JVirtual cname fn
226206
InterfaceDesc cname => JInterface cname fn
227-
NullableStrDesc => jerror "Instance method cannot have the first argument as nullable string"
228-
NullableRefDesc _ => jerror "Instance method cannot have the first argument as nullable reference"
229207
ArrayDesc _ => jerror "No instance methods on an array"
230208
IdrisExportDesc _ => jerror "No instance methods on an Idris exported type"
231209
else tryParseGetInstanceFieldDescriptor returns ffiDesc argsDesc

idris-jvm-core/src/main/idris/IdrisJvm/Core/Function.idr

-24
Original file line numberDiff line numberDiff line change
@@ -247,13 +247,6 @@ mutual
247247
Iconst 1
248248
ret IBool
249249

250-
cgBody ret (SCon _ 0 "Prelude.Maybe.Nothing" []) = do Aconstnull; ret inferredObjectType
251-
cgBody ret (SCon _ 1 "Prelude.Maybe.Just" [var]) = do
252-
locTypes <- GetFunctionLocTypes
253-
let varTy = getLocTy locTypes var
254-
loadVar locTypes varTy inferredObjectType var
255-
ret inferredObjectType
256-
257250
cgBody ret (SCon _ t _ args) = do createIdrisObject t args; ret inferredIdrisObjectType
258251

259252
cgBody ret (SCase _ e ((SConCase _ 0 "Prelude.Bool.False" [] falseAlt) ::
@@ -271,23 +264,6 @@ mutual
271264
_))
272265
= cgIfTrueElse ret cgBody e trueAlt falseAlt
273266

274-
cgBody ret (SCase _ e ((SConCase justValueStore 1 "Prelude.Maybe.Just" [_] justExpr) ::
275-
(SConCase _ 0 "Prelude.Maybe.Nothing" [] nothingExpr) ::
276-
_))
277-
= cgIfNonNull ret cgBody e justValueStore justExpr nothingExpr
278-
279-
cgBody ret (SCase _ e ((SConCase justValueStore 1 "Prelude.Maybe.Just" [_] justExpr) ::
280-
(SDefaultCase defaultExpr) ::
281-
_))
282-
= cgIfNonNull ret cgBody e justValueStore justExpr defaultExpr
283-
284-
cgBody ret (SCase _ e ((SConCase _ 0 "Prelude.Maybe.Nothing" [] nothingExpr) ::
285-
(SDefaultCase defaultExpr) ::
286-
_))
287-
= cgIfNull ret cgBody e nothingExpr defaultExpr
288-
289-
cgBody ret (SCase _ e [SConCase lv _ _ args expr]) = cgConCase ret cgBody (locIndex e) lv args expr
290-
291267
cgBody ret (SCase _ e [SDefaultCase defaultCaseExpr]) = cgBody ret defaultCaseExpr
292268

293269
cgBody ret (SCase _ e alts) =

0 commit comments

Comments
 (0)