Skip to content

Commit 9051b7b

Browse files
mmhelloworldmmhelloworld
committed
issue-64 issue-24 Automatic FFI with null safety, exception safety, optimize maybe
1 parent 7686742 commit 9051b7b

File tree

30 files changed

+1239
-380
lines changed

30 files changed

+1239
-380
lines changed

‎.travis.yml

+6-3
Original file line numberDiff line numberDiff line change
@@ -12,12 +12,15 @@ services:
1212
jdk:
1313
- oraclejdk8
1414

15+
env:
16+
- IDRIS_JVM_HOME=${HOME}/bin/idris-jvm
17+
1518
before_install:
1619
- docker pull mmhelloworld/idris:1.2.0
17-
- mkdir -p $HOME/bin/idris-packages $HOME/bin/idris-jvm
18-
- wget https://github.com/mmhelloworld/idris-jvm/releases/download/1.0-SNAPSHOT-20180114/idris-jvm-1.0-SNAPSHOT-20180114.zip
20+
- mkdir -p $HOME/bin/idris-packages $IDRIS_JVM_HOME
21+
- wget https://github.com/mmhelloworld/idris-jvm/releases/download/1.0-SNAPSHOT-20180207.beta/idris-jvm-1.0-SNAPSHOT-20180207.beta.zip
1922
- unzip -o idris-jvm-*.zip -d $HOME/bin
20-
- export PATH=`pwd`/bin/travis:$HOME/bin/idris-jvm/codegen/bin:$HOME/.local/bin:$PATH
23+
- export PATH=`pwd`/bin/travis:$IDRIS_JVM_HOME/codegen/bin:$HOME/.local/bin:$PATH
2124
- export PROJECT_ROOT=`pwd`
2225
- docker run --name idris mmhelloworld/idris:1.2.0 idris -v && docker cp idris:/.stack-work/install/x86_64-linux/lts-10.0/8.2.2/share/x86_64-linux-ghc-8.2.2/idris-1.2.0/libs/. $HOME/bin/idris-packages && docker rm idris
2326

‎bin/travis/idris

+11-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,14 @@
11
#!/usr/bin/env bash
22

3-
travis_long docker run -v $HOME/bin/idris-packages:/.stack-work/install/x86_64-linux/lts-10.0/8.2.2/share/x86_64-linux-ghc-8.2.2/idris-1.2.0/libs -v $PROJECT_ROOT:$PROJECT_ROOT -v $JAVA_HOME:/bin/jdk -v $HOME/bin/idris-jvm:/bin/idris-jvm -w `pwd` mmhelloworld/idris:1.2.0 idris "$@"
3+
export IDRIS_JVM_HOME=${HOME}/bin/idris-jvm
4+
5+
travis_long docker run \
6+
-e IDRIS_JVM_HOME=/bin/idris-jvm \
7+
-v $HOME/bin/idris-packages:/.stack-work/install/x86_64-linux/lts-10.0/8.2.2/share/x86_64-linux-ghc-8.2.2/idris-1.2.0/libs \
8+
-v $PROJECT_ROOT:$PROJECT_ROOT \
9+
-v $JAVA_HOME:/bin/jdk \
10+
-v $IDRIS_JVM_HOME:/bin/idris-jvm \
11+
-w `pwd` \
12+
mmhelloworld/idris:1.2.0 idris \
13+
"$@"
414

‎idris-jvm-codegen-launcher/pom.xml

+11-3
Original file line numberDiff line numberDiff line change
@@ -31,13 +31,21 @@
3131
<build>
3232
<plugins>
3333
<plugin>
34-
<groupId>org.springframework.boot</groupId>
35-
<artifactId>spring-boot-maven-plugin</artifactId>
34+
<groupId>org.apache.maven.plugins</groupId>
35+
<artifactId>maven-shade-plugin</artifactId>
3636
<executions>
3737
<execution>
38+
<phase>package</phase>
3839
<goals>
39-
<goal>repackage</goal>
40+
<goal>shade</goal>
4041
</goals>
42+
<configuration>
43+
<transformers>
44+
<transformer implementation="org.apache.maven.plugins.shade.resource.ManifestResourceTransformer">
45+
<mainClass>io.github.mmhelloworld.idrisjvm.codegen.launcher.IdrisJvmCodegenLauncher</mainClass>
46+
</transformer>
47+
</transformers>
48+
</configuration>
4149
</execution>
4250
</executions>
4351
</plugin>

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

+28-7
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,9 @@
11
package io.github.mmhelloworld.idrisjvm.codegen.launcher;
22

33
import org.springframework.http.HttpEntity;
4+
import org.springframework.http.ResponseEntity;
5+
import org.springframework.http.client.ClientHttpResponse;
6+
import org.springframework.web.client.DefaultResponseErrorHandler;
47
import org.springframework.web.client.RestTemplate;
58

69
import java.io.BufferedReader;
@@ -21,15 +24,24 @@
2124
import static java.lang.Integer.parseInt;
2225
import static java.lang.String.format;
2326
import static java.util.stream.Collectors.toList;
24-
import static org.springframework.http.HttpMethod.POST;
2527

2628
public class IdrisJvmCodegenLauncher {
27-
private static final String IDRIS_JVM_HOME = System.getProperty("IDRIS_JVM_HOME", System.getProperty("user.home"));
29+
private static final String IDRIS_JVM_HOME = Optional.ofNullable(System.getProperty("IDRIS_JVM_HOME"))
30+
.orElseGet(() -> Optional.ofNullable(System.getenv("IDRIS_JVM_HOME"))
31+
.orElseGet(() -> System.getProperty("user.home")));
2832

2933
private final RestTemplate restTemplate;
3034

3135
public IdrisJvmCodegenLauncher() {
3236
restTemplate = new RestTemplate();
37+
restTemplate.setErrorHandler(new DefaultResponseErrorHandler() {
38+
@Override
39+
public void handleError(ClientHttpResponse response) throws IOException {
40+
if (response.getStatusText() != null) {
41+
System.err.println(response.getStatusText());
42+
}
43+
}
44+
});
3345
}
3446

3547
public static void main(String[] args) throws Exception {
@@ -47,8 +59,8 @@ private void run(String[] args) throws Exception {
4759

4860
private void startServer() throws IOException, InterruptedException {
4961
final String basedir = System.getProperty("basedir");
50-
ProcessBuilder jvmProcessBuilder = new ProcessBuilder("java", "-jar",
51-
basedir + File.separator + "idris-jvm-server.jar");
62+
String serverPath = basedir + File.separator + "idris-jvm-server.jar";
63+
ProcessBuilder jvmProcessBuilder = new ProcessBuilder("java", "-jar", serverPath);
5264
jvmProcessBuilder.redirectErrorStream(true);
5365
File jvmOut = new File(basedir, "idris-jvm-server.log");
5466
jvmProcessBuilder.redirectOutput(ProcessBuilder.Redirect.to(jvmOut));
@@ -86,7 +98,11 @@ private void send(final String[] args) {
8698
List<String> endpointArgs = new ArrayList<>(Arrays.asList(args));
8799
endpointArgs.add(System.getProperty("user.dir"));
88100
int port = getPort().orElseThrow(() -> new RuntimeException("Idris JVM codegen server is not running"));
89-
new RestTemplate().exchange("http://localhost:" + port, POST, new HttpEntity<>(endpointArgs), Void.class);
101+
ResponseEntity<String> response = restTemplate.postForEntity("http://localhost:" + port,
102+
new HttpEntity<>(endpointArgs), String.class);
103+
if (!response.getStatusCode().is2xxSuccessful()) {
104+
System.err.println(response.getBody());
105+
}
90106
}
91107

92108
private List<String> readFile(File f) throws IOException {
@@ -97,9 +113,14 @@ private List<String> readFile(File f) throws IOException {
97113

98114
private Optional<Integer> getPort() {
99115
try {
100-
return Optional.of(parseInt(readFile(new File(IDRIS_JVM_HOME, ".idrisjvmport")).get(0)));
116+
File portFile = new File(IDRIS_JVM_HOME, ".idrisjvmport");
117+
if (portFile.exists()) {
118+
return Optional.of(parseInt(readFile(portFile).get(0)));
119+
} else {
120+
return Optional.empty();
121+
}
101122
} catch (IOException e) {
102-
return Optional.empty();
123+
throw new RuntimeException(e);
103124
}
104125
}
105126

‎idris-jvm-core/pom.xml

+2-18
Original file line numberDiff line numberDiff line change
@@ -44,22 +44,6 @@
4444
</arguments>
4545
</configuration>
4646
</execution>
47-
<execution>
48-
<id>install-idris-package</id>
49-
<phase>compile</phase>
50-
<goals>
51-
<goal>exec</goal>
52-
</goals>
53-
<configuration>
54-
<executable>idris</executable>
55-
<workingDirectory>${idris.srcdir}</workingDirectory>
56-
<arguments>
57-
<argument>--install</argument>
58-
<argument>${idris.srcdir}/idris-jvm-core.ipkg</argument>
59-
</arguments>
60-
</configuration>
61-
</execution>
62-
6347
<execution>
6448
<id>generate-idris-interface</id>
6549
<phase>compile</phase>
@@ -80,14 +64,14 @@
8064
<argument>-p</argument>
8165
<argument>contrib</argument>
8266
<argument>${idris.srcdir}/IdrisJvm/Core/Asm.idr</argument>
67+
<argument>${idris.srcdir}/IdrisJvm/Core/Codegen.idr</argument>
8368
<argument>${idris.srcdir}/IdrisJvm/Core/Common.idr</argument>
8469
<argument>${idris.srcdir}/IdrisJvm/Core/Constant.idr</argument>
85-
<argument>${idris.srcdir}/IdrisJvm/Core/Operator.idr</argument>
8670
<argument>${idris.srcdir}/IdrisJvm/Core/ControlFlow.idr</argument>
8771
<argument>${idris.srcdir}/IdrisJvm/Core/Foreign.idr</argument>
8872
<argument>${idris.srcdir}/IdrisJvm/Core/Function.idr</argument>
8973
<argument>${idris.srcdir}/IdrisJvm/Core/JAsm.idr</argument>
90-
<argument>${idris.srcdir}/IdrisJvm/Core/Codegen.idr</argument>
74+
<argument>${idris.srcdir}/IdrisJvm/Core/Operator.idr</argument>
9175
<argument>-o</argument>
9276
<argument>${project.build.outputDirectory}</argument>
9377
</arguments>

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

+16-12
Original file line numberDiff line numberDiff line change
@@ -32,7 +32,7 @@ mutual
3232
| FieldTyDescLong
3333
| FieldTyDescReference ReferenceTypeDescriptor
3434

35-
data TypeDescriptor = FieldDescriptor FieldTypeDescriptor | VoidDescriptor
35+
data TypeDescriptor = FieldDescriptor FieldTypeDescriptor | VoidDescriptor | ThrowableDescriptor TypeDescriptor
3636

3737
data MethodDescriptor = MkMethodDescriptor (List FieldTypeDescriptor) TypeDescriptor
3838

@@ -134,6 +134,7 @@ mutual
134134
Show TypeDescriptor where
135135
show (FieldDescriptor fieldTypeDescriptor) = "FieldDescriptor(" ++ show fieldTypeDescriptor ++ ")"
136136
show VoidDescriptor = "VoidDescriptor"
137+
show (ThrowableDescriptor tyDesc) = "ThrowableDescriptor(" ++ show tyDesc ++ ")"
137138

138139
record JMethodName where
139140
constructor MkJMethodName
@@ -164,20 +165,21 @@ mutual
164165
refTyClassName arr@(ArrayDesc _) = asmRefTyDesc arr
165166

166167
asmFieldTypeDesc : FieldTypeDescriptor -> String
167-
asmFieldTypeDesc FieldTyDescByte = "B"
168-
asmFieldTypeDesc FieldTyDescChar = "C"
169-
asmFieldTypeDesc FieldTyDescShort = "S"
170-
asmFieldTypeDesc FieldTyDescBoolean = "Z"
171-
asmFieldTypeDesc FieldTyDescArray = "["
172-
asmFieldTypeDesc FieldTyDescDouble = "D"
173-
asmFieldTypeDesc FieldTyDescFloat = "F"
174-
asmFieldTypeDesc FieldTyDescInt = "I"
175-
asmFieldTypeDesc FieldTyDescLong = "J"
176-
asmFieldTypeDesc (FieldTyDescReference f) = asmRefTyDesc f
168+
asmFieldTypeDesc FieldTyDescByte = "B"
169+
asmFieldTypeDesc FieldTyDescChar = "C"
170+
asmFieldTypeDesc FieldTyDescShort = "S"
171+
asmFieldTypeDesc FieldTyDescBoolean = "Z"
172+
asmFieldTypeDesc FieldTyDescArray = "["
173+
asmFieldTypeDesc FieldTyDescDouble = "D"
174+
asmFieldTypeDesc FieldTyDescFloat = "F"
175+
asmFieldTypeDesc FieldTyDescInt = "I"
176+
asmFieldTypeDesc FieldTyDescLong = "J"
177+
asmFieldTypeDesc (FieldTyDescReference f) = asmRefTyDesc f
177178

178179
asmTypeDesc : TypeDescriptor -> String
179180
asmTypeDesc (FieldDescriptor t) = asmFieldTypeDesc t
180181
asmTypeDesc VoidDescriptor = "V"
182+
asmTypeDesc (ThrowableDescriptor tyDesc) = asmTypeDesc tyDesc
181183

182184
asmMethodDesc : MethodDescriptor -> String
183185
asmMethodDesc (MkMethodDescriptor args returns) = "(" ++ asmArgs ++ ")" ++ r where
@@ -256,8 +258,11 @@ data Asm : Type -> Type where
256258
Ificmpgt : Label -> Asm ()
257259
Ificmple : Label -> Asm ()
258260
Ificmplt : Label -> Asm ()
261+
Ifnonnull : Label -> Asm ()
262+
Ifnull : Label -> Asm ()
259263
Iload : Int -> Asm ()
260264
Imul : Asm ()
265+
InstanceOf : ClassName -> Asm ()
261266
InvokeMethod : InvocType -> ClassName -> MethodName -> Descriptor -> Bool -> Asm ()
262267
InvokeDynamic : MethodName -> Descriptor -> Handle -> List BsmArg -> Asm ()
263268
Irem : Asm ()
@@ -292,7 +297,6 @@ data Asm : Type -> Type where
292297
MethodCodeEnd : Asm ()
293298
Multianewarray : Descriptor -> Nat -> Asm ()
294299
New : ClassName -> Asm ()
295-
InstanceOf : ClassName -> Asm ()
296300
Pop : Asm ()
297301
Pop2 : Asm ()
298302
Return : Asm ()

‎idris-jvm-core/src/main/idris/IdrisJvm/Core/Codegen.idr

+2-2
Original file line numberDiff line numberDiff line change
@@ -18,11 +18,11 @@ generateDependencyMethods assembler (subroutine :: subroutines) = do
1818
generateDependencyMethods assembler (newSubroutines ++ subroutines)
1919

2020
generateMethod' : Assembler -> SDecl -> JVM_IO ()
21-
generateMethod' assembler (SFun name args _ def) = do
21+
generateMethod' assembler (SFun name args locs def) = do
2222
let jmethodName = jname name
2323
let fname = jmethName jmethodName
2424
let clsName = jmethClsName jmethodName
25-
(_, subroutines) <- runAsm [] assembler $ cgFun [Public, Static] name clsName fname args def
25+
(_, subroutines) <- runAsm [] assembler $ cgFun [Public, Static] name clsName fname args locs def
2626
generateDependencyMethods assembler subroutines
2727

2828
generateMethod : Assembler -> SDecl -> JVM_IO ()

‎idris-jvm-core/src/main/idris/IdrisJvm/Core/ControlFlow.idr

+79-15
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
module IdrisJvm.Codegen.ControlFlow
1+
module IdrisJvm.Core.ControlFlow
22

33
import IdrisJvm.Core.Asm
44
import IdrisJvm.Core.Common
@@ -43,17 +43,36 @@ mutual
4343

4444
cgIf : Lazy (Asm ()) -> (Lazy (Asm ()) -> SExp -> Asm ()) -> LVar -> List SAlt -> Asm ()
4545
cgIf ret cgBody e alts = do
46-
ifIndex <- FreshIfIndex
47-
let ifExpr = ifCasesWithLbls ifIndex alts
48-
let fallbackLabels = drop 1 ((\(lbl, _, _) => lbl) <$> ifExpr) ++ [ifEndLabel ifIndex]
49-
sequence_ $ CreateLabel . (\(lbl, _, _) => lbl) <$> ifExpr
50-
CreateLabel $ ifEndLabel ifIndex
51-
sequence_ $ (uncurry $ cgIfCase ifIndex ret cgBody e) <$> zip fallbackLabels ifExpr
52-
LabelStart (ifEndLabel ifIndex)
53-
Frame FSame 0 [] 0 []
54-
55-
cgIfCase : Nat -> Lazy (Asm ()) -> (Lazy (Asm ()) -> SExp -> Asm ()) -> LVar -> String -> (String, Maybe (Asm ()), SAlt) -> Asm ()
56-
cgIfCase ifIndex ret cgBody e nextLabel (label, Just ifExpr, SConstCase _ expr) = do
46+
ifIndex <- FreshIfIndex
47+
let ifExpr = ifCasesWithLbls ifIndex alts
48+
let fallbackLabels = drop 1 ((\(lbl, _, _) => lbl) <$> ifExpr) ++ [ifEndLabel ifIndex]
49+
sequence_ $ CreateLabel . (\(lbl, _, _) => lbl) <$> ifExpr
50+
CreateLabel $ ifEndLabel ifIndex
51+
sequence_ $ gen ifIndex ret cgBody e <$> zip fallbackLabels ifExpr
52+
LabelStart (ifEndLabel ifIndex)
53+
Frame FSame 0 [] 0 []
54+
where
55+
gen : Nat
56+
-> Lazy (Asm ())
57+
-> (Lazy (Asm ()) -> SExp -> Asm ())
58+
-> LVar
59+
-> (String, String, Maybe (Asm ()), SAlt)
60+
-> Asm ()
61+
gen ifIndex ret cgBody e (nextLabel, label, ifExpr, expr)
62+
= maybe (cgElseCase ifIndex ret cgBody e nextLabel label expr)
63+
(\condition => cgIfElseIfCase ifIndex ret cgBody e nextLabel label condition expr)
64+
ifExpr
65+
66+
cgIfElseIfCase : Nat
67+
-> Lazy (Asm ())
68+
-> (Lazy (Asm ()) -> SExp -> Asm ())
69+
-> LVar
70+
-> String
71+
-> String
72+
-> Asm ()
73+
-> SAlt
74+
-> Asm ()
75+
cgIfElseIfCase ifIndex ret cgBody e nextLabel label ifExpr (SConstCase _ expr) = do
5776
LabelStart label
5877
addFrame
5978
Aload $ locIndex e
@@ -63,12 +82,18 @@ mutual
6382
cgBody ret expr
6483
Goto $ ifEndLabel ifIndex
6584

66-
cgIfCase ifIndex ret cgBody _ _ (label, Nothing, SDefaultCase expr) = do
85+
cgElseCase : Nat
86+
-> Lazy (Asm ())
87+
-> (Lazy (Asm ()) -> SExp -> Asm ())
88+
-> LVar
89+
-> String
90+
-> String
91+
-> SAlt
92+
-> Asm ()
93+
cgElseCase ifIndex ret cgBody _ _ label (SDefaultCase expr) = do
6794
cgCase ret cgBody label expr
6895
Goto $ ifEndLabel ifIndex
6996

70-
cgIfCase _ _ _ _ _ _ = invokeError "Unexpected if expression"
71-
7297
cgCase : Lazy (Asm ()) -> (Lazy (Asm ()) -> SExp -> Asm ()) -> Label -> SExp -> Asm ()
7398
cgCase ret cgBody label expr = do
7499
LabelStart label
@@ -216,3 +241,42 @@ mutual
216241
constCaseExpr VoidType = jerror "Constant VoidType cannot be compiled to 'if' yet"
217242
constCaseExpr Forgot = jerror "Constant Forgot cannot be compiled to 'if' yet"
218243
ifCaseExpr _ = Nothing
244+
245+
cgIfElse : Lazy (Asm ())
246+
-> (Lazy (Asm ()) -> SExp -> Asm ())
247+
-> LVar
248+
-> (Label -> Asm ())
249+
-> Maybe Int
250+
-> SExp
251+
-> SExp
252+
-> Asm ()
253+
cgIfElse ret cgBody e condition valueStore case1 case2 = do
254+
ifIndex <- FreshIfIndex
255+
let ifLabel = ifLabelName ifIndex 0
256+
let elseLabel = ifLabelName ifIndex 1
257+
let endLabel = ifEndLabel ifIndex
258+
CreateLabel ifLabel
259+
CreateLabel elseLabel
260+
CreateLabel endLabel
261+
Aload $ locIndex e
262+
condition elseLabel
263+
LabelStart ifLabel
264+
maybe (pure ()) store valueStore
265+
cgBody ret case1
266+
Goto endLabel
267+
LabelStart elseLabel
268+
addFrame
269+
cgBody ret case2
270+
LabelStart endLabel
271+
Frame FSame 0 [] 0 []
272+
where
273+
store : Int -> Asm ()
274+
store loc = do
275+
Aload $ locIndex e
276+
Astore loc
277+
278+
cgIfNonNull : Lazy (Asm ()) -> (Lazy (Asm ()) -> SExp -> Asm ()) -> LVar -> Int -> SExp -> SExp -> Asm ()
279+
cgIfNonNull ret cgBody e loc ifExp elseExp = cgIfElse ret cgBody e Ifnull (Just loc) ifExp elseExp
280+
281+
cgIfNull : Lazy (Asm ()) -> (Lazy (Asm ()) -> SExp -> Asm ()) -> LVar -> SExp -> SExp -> Asm ()
282+
cgIfNull ret cgBody e ifExp elseExp = cgIfElse ret cgBody e Ifnonnull Nothing ifExp elseExp

0 commit comments

Comments
 (0)