d4df20e · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

More primitives; started FFI in IRTS

commitd4df20e24745c1012c2bc9040057a7d6f56a9f1d authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateFri 31 Aug 2012, 18:08 (14 years ago) parent93d645a

8 files changed+220−14

compare with master

unifiedsplit

iif/testvm.iif+2−1 rts/idris_rts.c+67 rts/idris_rts.h+21−2 src/IRTS/Bytecode.hs+4 src/IRTS/CodegenC.hs+43−1 src/IRTS/LParser.hs+57−8 src/IRTS/Lang.hs+14−2 src/IRTS/Simplified.hs+12

iif/testvm.iif+2−1

@@ -23,5 +23,6 @@ fun intToNat(x) = case x of {

2323 | _ => S (intToNat (x - 1))

2424 }

2525

26−fun main() = printNum(natToInt(plus(intToNat(fact(6)), S(S(O)))))

26+fun main() = let val = natToInt(plus(intToNat(fact(6)), S(S(O)))) in

27+ %WriteString("Answer: " ++ %IntString(val))

2728

rts/idris_rts.c+67

@@ -57,6 +57,13 @@ VAL MKSTR(VM* vm, char* str) {

5757 return cl;

5858}

5959

60+VAL MKPTR(VM* vm, void* ptr) {

61+ Closure* cl = allocate(vm, sizeof(ClosureType) + sizeof(void*));

62+ cl -> ty = PTR;

63+ cl -> info.ptr = ptr;

64+ return cl;

65+}

66+

6067VAL MKCON(VM* vm, int tag, int arity, ...) {

6168 Closure* cl;

6269 int i;

@@ -109,6 +116,66 @@ void dumpVal(VAL v) {

109116

110117}

111118

119+VAL idris_castIntStr(VM* vm, VAL i) {

120+ Closure* cl = allocate(vm, sizeof(ClosureType) + sizeof(char*));

121+ cl -> ty = STRING;

122+ cl -> info.str = allocate(vm, sizeof(char)*16);

123+ sprintf(cl -> info.str, "%ld", GETINT(i));

124+ return cl;

125+}

126+

127+VAL idris_castStrInt(VM* vm, VAL i) {

128+ char *end;

129+ i_int v = strtol(GETSTR(i), &end, 10);

130+ if (*end != '\0') return MKINT(0); else return MKINT(v);

131+}

132+

133+VAL idris_castFloatStr(VM* vm, VAL i) {

134+ Closure* cl = allocate(vm, sizeof(ClosureType) + sizeof(char*));

135+ cl -> ty = STRING;

136+ cl -> info.str = allocate(vm, sizeof(char)*32);

137+ sprintf(cl -> info.str, "%g", GETFLOAT(i));

138+ return cl;

139+}

140+

141+VAL idris_castStrFloat(VM* vm, VAL i) {

142+ return MKFLOAT(vm, strtod(GETSTR(i), NULL));

143+}

144+

145+VAL idris_concat(VM* vm, VAL l, VAL r) {

146+ char *ls = GETSTR(l);

147+ char *rs = GETSTR(r);

148+

149+ Closure* cl = allocate(vm, sizeof(ClosureType) + sizeof(char*));

150+ cl -> ty = STRING;

151+ cl -> info.str = allocate(vm, sizeof(char)*(strlen(ls)+strlen(rs)+1));

152+ strcpy(cl -> info.str, ls);

153+ strcat(cl -> info.str, rs);

154+ return cl;

155+}

156+

157+VAL idris_strlt(VM* vm, VAL l, VAL r) {

158+ char *ls = GETSTR(l);

159+ char *rs = GETSTR(r);

160+

161+ return MKINT((i_int)(strcmp(ls, rs) < 0));

162+}

163+

164+VAL idris_streq(VM* vm, VAL l, VAL r) {

165+ char *ls = GETSTR(l);

166+ char *rs = GETSTR(r);

167+

168+ return MKINT((i_int)(strcmp(ls, rs) == 0));

169+}

170+

171+VAL idris_strlen(VM* vm, VAL l) {

172+ return MKINT((i_int)(strlen(GETSTR(l))));

173+}

174+

175+VAL idris_readStr(VM* vm, FILE* h) {

176+}

177+

178+

112179void stackOverflow() {

113180 fprintf(stderr, "Stack overflow");

114181 exit(-1);

rts/idris_rts.h+21−2

@@ -61,8 +61,8 @@ typedef void(*func)(VM*, VAL*);

6161// Retrieving values

6262

6363#define GETSTR(x) (((VAL)(x))->info.str)

64−#define GETPTR(x) (((void*)(x))->info.ptr)

65−#define GETFLOAT(x) (((double)(x))->info.f)

64+#define GETPTR(x) (((VAL)(x))->info.ptr)

65+#define GETFLOAT(x) (((VAL)(x))->info.f)

6666

6767#define TAG(x) ((x)->info.c.tag)

6868

@@ -96,6 +96,7 @@ typedef intptr_t i_int;

9696// Creating new values (each value placed at the top of the stack)

9797VAL MKFLOAT(VM* vm, double val);

9898VAL MKSTR(VM* vm, char* str);

99+VAL MKPTR(VM* vm, void* ptr);

99100

100101VAL MKCON(VM* vm, int tag, int arity, ...);

101102

@@ -104,6 +105,24 @@ void SLIDE(VM* vm, int args);

104105

105106void dumpVal(VAL r);

106107

108+// Casts

109+

110+#define idris_castIntFloat(x) MKFLOAT(vm, (double)(GETINT(x)))

111+#define idris_castFloatInt(x) MKINT((i_int)(GETFLOAT(x)))

112+

113+VAL idris_castIntStr(VM* vm, VAL i);

114+VAL idris_castStrInt(VM* vm, VAL i);

115+VAL idris_castFloatStr(VM* vm, VAL i);

116+VAL idris_castStrFloat(VM* vm, VAL i);

117+

118+// String primitives

119+

120+VAL idris_concat(VM* vm, VAL l, VAL r);

121+VAL idris_strlt(VM* vm, VAL l, VAL r);

122+VAL idris_streq(VM* vm, VAL l, VAL r);

123+VAL idris_strlen(VM* vm, VAL l);

124+VAL idris_readStr(VM* vm, FILE* h);

125+

107126// Handle stack overflow.

108127// Just reports an error and exits.

109128

src/IRTS/Bytecode.hs+4

@@ -30,6 +30,7 @@ data BC = ASSIGN Reg Reg

3030 | CONSTCASE Reg [(Const, [BC])] (Maybe [BC])

3131 | CALL Name

3232 | TAILCALL Name

33+ | FOREIGNCALL Reg FLang FType String [(FType, Reg)]

3334 | SLIDE Int -- move this number from TOP to BASE

3435 | REBASE -- set BASE = OLDBASE

3536 | RESERVE Int -- reserve n more stack items

@@ -61,6 +62,9 @@ bc reg (SApp False f vs) r

6162bc reg (SApp True f vs) r

6263 = RESERVE (length vs) : moveReg 0 vs

6364 ++ [SLIDE (length vs), TOPBASE (length vs), TAILCALL f]

65+bc reg (SForeign l t fname args) r

66+ = FOREIGNCALL reg l t fname (map farg args) : clean r

67+ where farg (ty, Loc i) = (ty, L i)

6468bc reg (SLet (Loc i) e sc) r = bc (L i) e False ++ bc reg sc r

6569bc reg (SCon i _ vs) r = MKCON reg i (map getL vs) : clean r

6670 where getL (Loc x) = L x

src/IRTS/CodegenC.hs+43−1

@@ -79,12 +79,54 @@ bcc i STOREOLD = indent i ++ "STOREOLD;\n"

7979bcc i (OP l fn args) = indent i ++ creg l ++ " = " ++ doOp fn args ++ ";\n"

8080-- bcc i _ = indent i ++ "// not done yet\n"

8181

82+c_irts FInt x = "MKINT((i_int)(" ++ x ++ ")"

83+c_irts FString x = "MKSTR(" ++ x ++ ")"

84+c_irts FUnit x = "MKINT(42424242)"

85+c_irts FPtr x = "MKPTR(" ++ x ++ ")"

86+c_irts FDouble x = "MKFLOAT(vm, " ++ x ++ ")"

87+c_irts FAny x = x

88+

89+irts_c FInt x = "GETINT(" ++ x ++ ")"

90+irts_c FString x = "GETSTR(" ++ x ++ ")"

91+irts_c FUnit x = x

92+irts_c FPtr x = "GETPTR(" ++ x ++ ")"

93+irts_c FDouble x = "GETFLOAT(" ++ x ++ ")"

94+irts_c FAny x = x

95+

8296doOp LPlus [l, r] = "ADD(" ++ creg l ++ ", " ++ creg r ++ ")"

8397doOp LMinus [l, r] = "INTOP(-," ++ creg l ++ ", " ++ creg r ++ ")"

8498doOp LTimes [l, r] = "MULT(" ++ creg l ++ ", " ++ creg r ++ ")"

8599doOp LDiv [l, r] = "INTOP(/," ++ creg l ++ ", " ++ creg r ++ ")"

86100doOp LEq [l, r] = "INTOP(==," ++ creg l ++ ", " ++ creg r ++ ")"

101+doOp LLt [l, r] = "INTOP(<," ++ creg l ++ ", " ++ creg r ++ ")"

102+doOp LLe [l, r] = "INTOP(<=," ++ creg l ++ ", " ++ creg r ++ ")"

103+doOp LGt [l, r] = "INTOP(>," ++ creg l ++ ", " ++ creg r ++ ")"

104+doOp LGe [l, r] = "INTOP(>=," ++ creg l ++ ", " ++ creg r ++ ")"

105+

106+doOp LFPlus [l, r] = "FLOATOP(+" ++ creg l ++ ", " ++ creg r ++ ")"

107+doOp LFMinus [l, r] = "FLOATOP(-," ++ creg l ++ ", " ++ creg r ++ ")"

108+doOp LFTimes [l, r] = "FLOATOP(*" ++ creg l ++ ", " ++ creg r ++ ")"

109+doOp LFDiv [l, r] = "FLOATOP(/," ++ creg l ++ ", " ++ creg r ++ ")"

110+doOp LFEq [l, r] = "FLOATBOP(==," ++ creg l ++ ", " ++ creg r ++ ")"

111+doOp LFLt [l, r] = "FLOATBOP(<," ++ creg l ++ ", " ++ creg r ++ ")"

112+doOp LFLe [l, r] = "FLOATBOP(<=," ++ creg l ++ ", " ++ creg r ++ ")"

113+doOp LFGt [l, r] = "FLOATBOP(>," ++ creg l ++ ", " ++ creg r ++ ")"

114+doOp LFGe [l, r] = "FLOATBOP(>=," ++ creg l ++ ", " ++ creg r ++ ")"

115+

116+doOp LStrConcat [l,r] = "idris_concat(vm, " ++ creg l ++ ", " ++ creg r ++ ")"

117+doOp LStrLt [l,r] = "idris_strlt(vm, " ++ creg l ++ ", " ++ creg r ++ ")"

118+doOp LStrEq [l,r] = "idris_streq(vm, " ++ creg l ++ ", " ++ creg r ++ ")"

119+doOp LStrLen [x] = "idris_strlen(vm, " ++ creg x ++ ")"

120+

121+doOp LIntFloat [x] = "idris_castIntFloat(" ++ creg x ++ ")"

122+doOp LFloatInt [x] = "idris_castFloatInt(" ++ creg x ++ ")"

123+doOp LIntStr [x] = "idris_castIntStr(vm, " ++ creg x ++ ")"

124+doOp LStrInt [x] = "idris_castFloatStr(vm, " ++ creg x ++ ")"

125+doOp LFloatStr [x] = "idris_castFloatStr(vm, " ++ creg x ++ ")"

126+doOp LStrFloat [x] = "idris_castStrFloat(vm, " ++ creg x ++ ")"

127+

128+doOp LReadStr [] = "idris_readStr(vm, stdin)"

87129doOp LPrintNum [x] = "NULL; printf(\"%ld\\n\", GETINT(" ++ creg x ++ "))"

88−doOp LPrintStr [x] = "NULL; printf(GETSTR(" ++ creg x ++ "))"

130+doOp LPrintStr [x] = "NULL; puts(GETSTR(" ++ creg x ++ "))"

89131doOp _ _ = "FAIL"

90132

src/IRTS/LParser.hs+57−8

@@ -62,6 +62,7 @@ fovm f = do defs <- parseFOVM f

6262 d <- getDataDir

6363 mprog <- readFile (d ++ "/rts/idris_main.c")

6464 putStrLn mprog

65+ err -> print err

6566

6667parseFOVM :: FilePath -> IO [(Name, LDecl)]

6768parseFOVM fname = do -- putStrLn $ "Reading " ++ fname

@@ -92,18 +93,35 @@ pLDecl = do reserved "data"

9293pLExp = buildExpressionParser optable pLExp'

9394

9495optable = [[binary "*" (\x y -> LOp LTimes [x,y]) AssocLeft,

95− binary "/" (\x y -> LOp LDiv [x,y]) AssocLeft],

96− [binary "+" (\x y -> LOp LPlus [x,y]) AssocLeft,

97− binary "-" (\x y -> LOp LMinus [x,y]) AssocLeft],

98− [binary "==" (\x y -> LOp LEq [x, y]) AssocNone]]

96+ binary "/" (\x y -> LOp LDiv [x,y]) AssocLeft,

97+ binary "*." (\x y -> LOp LFTimes [x,y]) AssocLeft,

98+ binary "/." (\x y -> LOp LFTimes [x,y]) AssocLeft

99+ ],

100+ [

101+ binary "+" (\x y -> LOp LPlus [x,y]) AssocLeft,

102+ binary "-" (\x y -> LOp LMinus [x,y]) AssocLeft,

103+ binary "++" (\x y -> LOp LStrConcat [x,y]) AssocLeft,

104+ binary "+." (\x y -> LOp LFPlus [x,y]) AssocLeft,

105+ binary "-." (\x y -> LOp LFMinus [x,y]) AssocLeft

106+ ],

107+ [

108+ binary "==" (\x y -> LOp LEq [x, y]) AssocNone,

109+ binary "==." (\x y -> LOp LFEq [x, y]) AssocNone,

110+ binary "<" (\x y -> LOp LLt [x, y]) AssocNone,

111+ binary "<." (\x y -> LOp LFLt [x, y]) AssocNone,

112+ binary ">" (\x y -> LOp LGt [x, y]) AssocNone,

113+ binary ">." (\x y -> LOp LFGt [x, y]) AssocNone,

114+ binary "<=" (\x y -> LOp LLe [x, y]) AssocNone,

115+ binary "<=." (\x y -> LOp LFLe [x, y]) AssocNone,

116+ binary ">=" (\x y -> LOp LGe [x, y]) AssocNone,

117+ binary ">=." (\x y -> LOp LFGe [x, y]) AssocNone

118+ ]]

99119

100120binary name f assoc = Infix (do reservedOp name; return f) assoc

101121

102122pLExp' :: LParser LExp

103−pLExp' = try (do reserved "printNum"; e <- pLExp

104− return (LOp LPrintNum [e]))

105− <|> try (do reserved "print"; e <- pLExp

106− return (LOp LPrintStr [e]))

123+pLExp' = try (do lchar '%'; pCast)

124+ <|> try (do lchar '%'; pPrim)

107125 <|> try (do tc <- option False (do lchar '%'; reserved "tc"; return True)

108126 x <- iName [];

109127 lchar '('

@@ -115,10 +133,25 @@ pLExp' = try (do reserved "printNum"; e <- pLExp

115133 <|> do reserved "let"; x <- iName []; lchar '='; v <- pLExp

116134 reserved "in"; e <- pLExp

117135 return (LLet x v e)

136+ <|> do reserved "foreign"; l <- pLang; t <- pType

137+ fname <- strlit

138+ lchar '('

139+ fargs <- sepBy (do t' <- pType; e <- pLExp; return (t', e)) (lchar ',')

140+ lchar ')'

141+ return (LForeign l t fname fargs)

118142 <|> pCase

119143 <|> do x <- iName []

120144 return (LV (Glob x))

121145

146+pLang = do reserved "C"; return LANG_C

147+

148+pType = do reserved "Int"; return FInt

149+ <|> do reserved "Float"; return FDouble

150+ <|> do reserved "String"; return FString

151+ <|> do reserved "Unit"; return FUnit

152+ <|> do reserved "Ptr"; return FPtr

153+ <|> do reserved "Any"; return FAny

154+

122155pCase :: LParser LExp

123156pCase = do reserved "case"; e <- pLExp; reserved "of"

124157 lchar '{'

@@ -126,6 +159,22 @@ pCase = do reserved "case"; e <- pLExp; reserved "of"

126159 lchar '}'

127160 return (LCase e alts)

128161

162+pCast :: LParser LExp

163+pCast = do reserved "FloatString"; e <- pLExp; return (LOp LFloatStr [e])

164+ <|> do reserved "StringFloat"; e <- pLExp; return (LOp LStrFloat [e])

165+ <|> do reserved "FloatInt"; e <- pLExp; return (LOp LFloatInt [e])

166+ <|> do reserved "IntFloat"; e <- pLExp; return (LOp LIntFloat [e])

167+ <|> do reserved "StringInt"; e <- pLExp; return (LOp LStrInt [e])

168+ <|> do reserved "IntString"; e <- pLExp; return (LOp LIntStr [e])

169+

170+pPrim :: LParser LExp

171+pPrim = do reserved "StrEq"; e <- pLExp; e' <- pLExp; return (LOp LStrEq [e, e'])

172+ <|> do reserved "StrLt"; e <- pLExp; e' <- pLExp; return (LOp LStrLt [e, e'])

173+ <|> do reserved "StrLen"; e <- pLExp; return (LOp LStrLen [e])

174+ <|> do reserved "ReadString"; return (LOp LReadStr [])

175+ <|> do reserved "WriteString"; e <- pLExp; return (LOp LPrintStr [e])

176+ <|> do reserved "WriteInt"; e <- pLExp; return (LOp LPrintNum [e])

177+

129178pAlt :: LParser LAlt

130179pAlt = try (do x <- iName []

131180 lchar '('; args <- sepBy1 (iName []) (lchar ','); lchar ')'

src/IRTS/Lang.hs+14−2

@@ -11,11 +11,23 @@ data LExp = LV LVar

1111 | LCon Int Name [LExp]

1212 | LCase LExp [LAlt]

1313 | LConst Const

14+ | LForeign FLang FType String [(FType, LExp)]

1415 | LOp PrimFn [LExp]

1516 deriving Show

1617

17−data PrimFn = LPlus | LMinus | LTimes | LDiv | LEq

18− | LPrintNum | LPrintStr

18+data PrimFn = LPlus | LMinus | LTimes | LDiv | LEq | LLt | LLe | LGt | LGe

20+ | LStrConcat | LStrLt | LStrEq | LStrLen

22+ | LPrintNum | LPrintStr | LReadStr

23+ deriving Show

24+

25+-- Supported target languages for foreign calls

26+

27+data FLang = LANG_C

28+ deriving Show

29+

1931 deriving Show

2032

2133data LAlt = LConCase Int Name [Name] LExp

src/IRTS/Simplified.hs+12

@@ -14,6 +14,7 @@ data SExp = SV LVar

1414 | SCon Int Name [LVar]

1515 | SCase LVar [SAlt]

1616 | SConst Const

17+ | SForeign FLang FType String [(FType, LVar)]

1718 | SOp PrimFn [LVar]

1819 deriving Show

1920

@@ -43,6 +44,10 @@ simplify tl (LV (Glob x))

4344 _ -> return $ SV (Glob x)

4445simplify tl (LApp tc n args) = do args' <- mapM sVar args

4546 mkapp (SApp (tl || tc) n) args'

47+simplify tl (LForeign lang ty fn args)

48+ = do args' <- mapM sVar (map snd args)

49+ let fargs = zip (map fst args) args'

50+ mkfapp (SForeign lang ty fn) fargs

4651simplify tl (LLet n v e) = do v' <- simplify False v

4752 e' <- simplify tl e

4853 return (SLet (Glob n) v' e')

@@ -75,6 +80,13 @@ mkapp f args = mkapp' f args [] where

7580 = do sc <- mkapp' f xs (x : args)

7681 return (SLet x e sc)

7782

83+mkfapp f args = mkapp' f args [] where

84+ mkapp' f [] args = return $ f (reverse args)

85+ mkapp' f ((ty, (x, Nothing)) : xs) args = mkapp' f xs ((ty, x) : args)

86+ mkapp' f ((ty, (x, Just e)) : xs) args

87+ = do sc <- mkapp' f xs ((ty, x) : args)

88+ return (SLet x e sc)

89+

7890sAlt tl (LConCase i n args e) = do e' <- simplify tl e

7991 return (SConCase (-1) i n args e')

8092sAlt tl (LConstCase c e) = do e' <- simplify tl e