b642db5 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Almost working new back end

b642db5Edwin Brady14 years ago

idris.cabal+1−1

compare with master

unifiedsplit

@@ -72,7 +72,7 @@ Executable idris

73 RTS.Bytecode, RTS.SC, RTS.PreC, RTS.CodegenC,

74 IRTS.Lang, IRTS.LParser, IRTS.Bytecode, IRTS.Simplified,

75− IRTS.CodegenC, IRTS.Defunctionalise,

75+ IRTS.CodegenC, IRTS.Defunctionalise, IRTS.Compiler,

77 Paths_idris

lib/prelude/nat.idr+1−1

@@ -123,7 +123,7 @@ instance Num Nat where

123

124 abs x = x

125

126− fromInteger = fromInteger'

126+ fromInteger x = fromInteger' x

127 where

128 %assert_total

129 fromInteger' : Int -> Nat

rts/idris_main.c+2−2

@@ -1,7 +1,7 @@

1int main(int argc, char* argv[]) {

2 VM* vm = init_vm(1024000, 1024000);

3−

3+ _idris__123_runMain0_125_(vm, NULL);

4− _idris_main(vm, NULL);

4+ //_idris_main(vm, NULL);

5#ifdef IDRIS_TRACE

6 printf("\nStack: %p %p\n", vm->valstack, vm->valstack_top);

7 printf("Total allocations: %d\n", vm->allocations);

rts/idris_rts.c+9−2

@@ -124,6 +124,10 @@ void SLIDE(VM* vm, int args) {

124

125void dumpVal(VAL v) {

126 int i;

127+ if (ISINT(v)) {

128+ printf("%ld ", GETINT(v));

129+ return;

130+ }

127 switch(v->ty) {

131 switch(v->ty) {

128 case CON:

132 case CON:

129 printf("%d[", v->info.c.tag);

133 printf("%d[", v->info.c.tag);

@@ -132,6 +136,9 @@ void dumpVal(VAL v) {

132 dumpVal(args[i]);

136 dumpVal(args[i]);

133 }

137 }

134 printf("] ");

138 printf("] ");

139+ break;

140+ default:

141+ printf("val");

135 }

142 }

136

143

137}

144}

@@ -230,7 +237,7 @@ VAL idris_readStr(VM* vm, FILE* h) {

230}

237}

231

238

232VAL idris_strHead(VM* vm, VAL str) {

239VAL idris_strHead(VM* vm, VAL str) {

233− return MKINT(GETSTR(str)[0]);

240+ return MKINT((i_int)(GETSTR(str)[0]));

234}

241}

235

242

236VAL idris_strTail(VM* vm, VAL str) {

243VAL idris_strTail(VM* vm, VAL str) {

@@ -249,7 +256,7 @@ VAL idris_strCons(VM* vm, VAL x, VAL xs) {

249}

256}

250

257

251VAL idris_strIndex(VM* vm, VAL str, VAL i) {

258VAL idris_strIndex(VM* vm, VAL str, VAL i) {

252− return MKINT(GETSTR(str)[GETINT(i)]);

259+ return MKINT((i_int)(GETSTR(str)[GETINT(i)]));

253}

260}

254

261

255VAL idris_strRev(VM* vm, VAL str) {

262VAL idris_strRev(VM* vm, VAL str) {

src/IRTS/Bytecode.hs+3−1

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

40 | BASETOP Int -- set BASE = TOP + n

41 | STOREOLD -- set OLDBASE = BASE

42 | OP Reg PrimFn [Reg]

43+ | ERROR String

43 deriving Show

44 deriving Show

45toBC :: (Name, SDecl) -> (Name, [BC])

46toBC :: (Name, SDecl) -> (Name, [BC])

@@ -55,7 +56,7 @@ bc :: Reg -> SExp -> Bool -> -- returning

55 [BC]

56 [BC]

56bc reg (SV (Glob n)) r = bc reg (SApp False n []) r

57bc reg (SV (Glob n)) r = bc reg (SApp False n []) r

57bc reg (SV (Loc i)) r = assign reg (L i) ++ clean r

58bc reg (SV (Loc i)) r = assign reg (L i) ++ clean r

58−bc reg (SApp False f vs) r

59+bc reg (SApp _ f vs) r

59 = RESERVE (length vs) : moveReg 0 vs

60 = RESERVE (length vs) : moveReg 0 vs

60 ++ [STOREOLD, BASETOP 0, ADDTOP (length vs), CALL f] ++

61 ++ [STOREOLD, BASETOP 0, ADDTOP (length vs), CALL f] ++

61 assign reg RVal ++ clean r

62 assign reg RVal ++ clean r

@@ -71,6 +72,7 @@ bc reg (SCon i _ vs) r = MKCON reg i (map getL vs) : clean r

71bc reg (SConst i) r = ASSIGNCONST reg i : clean r

72bc reg (SConst i) r = ASSIGNCONST reg i : clean r

72bc reg (SOp p vs) r = OP reg p (map getL vs) : clean r

73bc reg (SOp p vs) r = OP reg p (map getL vs) : clean r

73 where getL (Loc x) = L x

74 where getL (Loc x) = L x

75+bc reg (SError str) r = [ERROR str]

74bc reg (SCase (Loc l) alts) r

76bc reg (SCase (Loc l) alts) r

75 | isConst alts = constCase reg (L l) alts r

77 | isConst alts = constCase reg (L l) alts r

76 | otherwise = conCase reg (L l) alts r

78 | otherwise = conCase reg (L l) alts r

src/IRTS/CodegenC.hs+2

@@ -135,6 +135,7 @@ bcc i (FOREIGNCALL l LANG_C rty fn args)

135 c_irts rty (creg l ++ " = ")

136 (fn ++ "(" ++ showSep "," (map fcall args) ++ ")") ++ ";\n"

137 where fcall (t, arg) = irts_c t (creg arg)

138+bcc i (ERROR str) = indent i ++ "fprintf(stderr, " ++ show str ++ "); exit(-1);"

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

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

139

140

140c_irts FInt l x = l ++ "MKINT((i_int)(" ++ x ++ ")"

141c_irts FInt l x = l ++ "MKINT((i_int)(" ++ x ++ ")"

@@ -220,6 +221,7 @@ doOp v LStrTail [x] = v ++ "idris_strTail(vm, " ++ creg x ++ ")"

220doOp v LStrCons [x, y] = v ++ "idris_strCons(vm, " ++ creg x ++ "," ++ creg y ++ ")"

221doOp v LStrCons [x, y] = v ++ "idris_strCons(vm, " ++ creg x ++ "," ++ creg y ++ ")"

221doOp v LStrIndex [x, y] = v ++ "idris_strIndex(vm, " ++ creg x ++ "," ++ creg y ++ ")"

222doOp v LStrIndex [x, y] = v ++ "idris_strIndex(vm, " ++ creg x ++ "," ++ creg y ++ ")"

222doOp v LStrRev [x] = v ++ "idris_strRev(vm, " ++ creg x ++ ")"

223doOp v LStrRev [x] = v ++ "idris_strRev(vm, " ++ creg x ++ ")"

224+doOp v LNoOp [x] = ""

223doOp _ _ _ = "FAIL"

225doOp _ _ _ = "FAIL"

224

226

225tempfile :: IO (FilePath, Handle)

227tempfile :: IO (FilePath, Handle)

src/IRTS/Defunctionalise.hs+23−20

@@ -38,28 +38,30 @@ addApps defs o@(n, LConstructor _ _ _) = o

38addApps defs (n, LFun _ args e) = (n, LFun n args (aa args e))

39 where

40 aa env (LV (Glob n)) | n `elem` env = LV (Glob n)

41− | otherwise = aa env (LApp False n [])

41+ | otherwise = aa env (LApp False (LV (Glob n)) [])

42-- aa env e@(LApp tc (MN 0 "EVAL") [a]) = e

43− aa env (LApp tc n args)

43+ aa env (LApp tc (LV (Glob n)) args)

44 = let args' = map (aa env) args in

45 case lookupCtxt Nothing n defs of

46− [LConstructor _ i ar] -> LApp tc n args'

46+ [LConstructor _ i ar] -> LApp tc (LV (Glob n)) args'

47 [LFun _ as _] -> let arity = length as in

48 fixApply tc n args' arity

49 [] -> chainAPPLY (LV (Glob n)) args'

50 aa env (LLazyApp n args)

51 = let args' = map (aa env) args in

52 case lookupCtxt Nothing n defs of

53− [LConstructor _ i ar] -> LApp False n args'

53+ [LConstructor _ i ar] -> LApp False (LV (Glob n)) args'

54 [LFun _ as _] -> let arity = length as in

55 fixLazyApply n args' arity

56 [] -> chainAPPLY (LV (Glob n)) args'

57+ aa env (LForce e) = eEVAL (aa env e)

57 aa env (LLet n v sc) = LLet n (aa env v) (aa (n : env) sc)

58 aa env (LLet n v sc) = LLet n (aa env v) (aa (n : env) sc)

58 aa env (LCon i n args) = LCon i n (map (aa env) args)

59 aa env (LCon i n args) = LCon i n (map (aa env) args)

59 aa env (LCase e alts) = LCase (eEVAL (aa env e)) (map (aaAlt env) alts)

60 aa env (LCase e alts) = LCase (eEVAL (aa env e)) (map (aaAlt env) alts)

60 aa env (LConst c) = LConst c

61 aa env (LConst c) = LConst c

61 aa env (LForeign l t n args) = LForeign l t n (map (aaF env) args)

62 aa env (LForeign l t n args) = LForeign l t n (map (aaF env) args)

62 aa env (LOp f args) = LOp f (map (eEVAL . (aa env)) args)

63 aa env (LOp f args) = LOp f (map (eEVAL . (aa env)) args)

64+ aa env (LError e) = LError e

64 aaF env (t, e) = (t, eEVAL (aa env e))

66 aaF env (t, e) = (t, eEVAL (aa env e))

@@ -67,20 +69,20 @@ addApps defs (n, LFun _ args e) = (n, LFun n args (aa args e))

67 aaAlt env (LConstCase c e) = LConstCase c (aa env e)

69 aaAlt env (LConstCase c e) = LConstCase c (aa env e)

68 aaAlt env (LDefaultCase e) = LDefaultCase (aa env e)

70 aaAlt env (LDefaultCase e) = LDefaultCase (aa env e)

70− eEVAL x = LApp False (MN 0 "EVAL") [x]

71−

72 fixApply tc n args ar

73− | length args == ar = LApp tc n args

73+ | length args == ar = LApp tc (LV (Glob n)) args

74− | length args < ar = LApp tc (mkUnderCon n (ar - length args)) args

74+ | length args < ar = LApp tc (LV (Glob (mkUnderCon n (ar - length args)))) args

75− | length args > ar = chainAPPLY (LApp tc n (take ar args)) (drop ar args)

75+ | length args > ar = chainAPPLY (LApp tc (LV (Glob n)) (take ar args)) (drop ar args)

77 fixLazyApply n args ar

78− | length args == ar = LApp False (mkFnCon n) args

78+ | length args == ar = LApp False (LV (Glob (mkFnCon n))) args

79− | length args < ar = LApp False (mkUnderCon n (ar - length args)) args

79+ | length args < ar = LApp False (LV (Glob (mkUnderCon n (ar - length args)))) args

80− | length args > ar = chainAPPLY (LApp False n (take ar args)) (drop ar args)

80+ | length args > ar = chainAPPLY (LApp False (LV (Glob n)) (take ar args)) (drop ar args)

82 chainAPPLY f [] = f

83− chainAPPLY f (a : as) = chainAPPLY (LApp False (MN 0 "APPLY") [f, a]) as

83+ chainAPPLY f (a : as) = chainAPPLY (LApp False (LV (Glob (MN 0 "APPLY"))) [f, a]) as

84+

85+eEVAL x = LApp False (LV (Glob (MN 0 "EVAL"))) [x]

85data EvalApply a = EvalCase a

87data EvalApply a = EvalCase a

86 | ApplyCase a

88 | ApplyCase a

@@ -90,17 +92,17 @@ data EvalApply a = EvalCase a

90-- data constuctors, and whether to handle them in EVAL or APPLY

92-- data constuctors, and whether to handle them in EVAL or APPLY

92toCons :: (Name, Int) -> [(Name, Int, EvalApply LAlt)]

94toCons :: (Name, Int) -> [(Name, Int, EvalApply LAlt)]

95+toCons (n, i)

93−toCons (n, i) = (mkFnCon n, i,

96+ = (mkFnCon n, i,

94− EvalCase (LConCase (-1) (mkFnCon n) (take i (genArgs 0))

97+ EvalCase (LConCase (-1) (mkFnCon n) (take i (genArgs 0))

95− (LApp False n (map (LV . Glob) (take i (genArgs 0))))))

98+ (eEVAL (LApp False (LV (Glob n)) (map (LV . Glob) (take i (genArgs 0)))))))

96− :

97− mkApplyCase n 0 i

99+ : mkApplyCase n 0 i

100

99mkApplyCase fname n ar | n == ar = []

101mkApplyCase fname n ar | n == ar = []

100mkApplyCase fname n ar

102mkApplyCase fname n ar

101 = let nm = mkUnderCon fname (ar - n) in

103 = let nm = mkUnderCon fname (ar - n) in

102 (nm, n, ApplyCase (LConCase (-1) nm (take n (genArgs 0))

104 (nm, n, ApplyCase (LConCase (-1) nm (take n (genArgs 0))

103− (LApp False (mkUnderCon fname (ar - (n + 1)))

105+ (LApp False (LV (Glob (mkUnderCon fname (ar - (n + 1)))))

104 (map (LV . Glob) (take n (genArgs 0) ++

106 (map (LV . Glob) (take n (genArgs 0) ++

105 [MN 0 "arg"])))))

107 [MN 0 "arg"])))))

106 : mkApplyCase fname (n + 1) ar

108 : mkApplyCase fname (n + 1) ar

@@ -116,7 +118,8 @@ mkEval xs = (MN 0 "EVAL", LFun (MN 0 "EVAL") [MN 0 "arg"]

116

118

117mkApply :: [(Name, Int, EvalApply LAlt)] -> (Name, LDecl)

119mkApply :: [(Name, Int, EvalApply LAlt)] -> (Name, LDecl)

118mkApply xs = (MN 0 "APPLY", LFun (MN 0 "APPLY") [MN 0 "fn", MN 0 "arg"]

120mkApply xs = (MN 0 "APPLY", LFun (MN 0 "APPLY") [MN 0 "fn", MN 0 "arg"]

119− (LCase (LApp False (MN 0 "EVAL") [LV (Glob (MN 0 "fn"))])

121+ (LCase (LApp False (LV (Glob (MN 0 "EVAL")))

122+ [LV (Glob (MN 0 "fn"))])

120 (mapMaybe applyCase xs)))

123 (mapMaybe applyCase xs)))

121 where

124 where

122 applyCase (n, t, ApplyCase x) = Just x

125 applyCase (n, t, ApplyCase x) = Just x

src/IRTS/LParser.hs+2−2

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

50 let (nexttag, tagged) = addTags 0 (liftAll defs)

51 let ctxtIn = addAlist tagged emptyContext

52 let defuns = defunctionalise nexttag ctxtIn

53−-- print defuns

53+ putStrLn $ showSep "\n" (map show (toAlist defuns))

54 let checked = checkDefs defuns (toAlist defuns)

55-- print checked

56 case checked of

@@ -135,7 +135,7 @@ pLExp' = try (do lchar '%'; pCast)

135 then if lazy then return (LLazyApp x [])

136 else return (LV (Glob x))

137 else if lazy then return (LLazyApp x args)

138− else return (LApp tc x args))

138+ else return (LApp tc (LV (Glob x)) args))

139 <|> do lchar '('; e <- pLExp; lchar ')'; return e

140 <|> pLConst

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

src/IRTS/Lang.hs+15−5

@@ -7,9 +7,10 @@ data LVar = Loc Int | Glob Name

7 deriving Show

9data LExp = LV LVar

10− | LApp Bool Name [LExp] -- True = tail call

10+ | LApp Bool LExp [LExp] -- True = tail call

11 | LLazyApp Name [LExp] -- True = tail call

12 | LLazyExp LExp

13+ | LForce LExp -- make sure Exp is evaluted

13 | LLet Name LExp LExp -- name just for pretty printing

14 | LLet Name LExp LExp -- name just for pretty printing

14 | LLam [Name] LExp -- lambda, lifted out before compiling

15 | LLam [Name] LExp -- lambda, lifted out before compiling

15 | LCon Int Name [LExp]

16 | LCon Int Name [LExp]

@@ -17,6 +18,7 @@ data LExp = LV LVar

17 | LConst Const

18 | LConst Const

18 | LForeign FLang FType String [(FType, LExp)]

19 | LForeign FLang FType String [(FType, LExp)]

19 | LOp PrimFn [LExp]

20 | LOp PrimFn [LExp]

21+ | LError String

20 deriving Show

22 deriving Show

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

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

@@ -31,6 +33,7 @@ data PrimFn = LPlus | LMinus | LTimes | LDiv | LEq | LLt | LLe | LGt | LGe

31 | LFSqrt | LFFloor | LFCeil

33 | LFSqrt | LFFloor | LFCeil

36+ | LNoOp

34 deriving Show

37 deriving Show

36-- Supported target languages for foreign calls

39-- Supported target languages for foreign calls

@@ -85,8 +88,13 @@ addFn fn d = do LS n i ds <- get

86lift :: [Name] -> LExp -> State LiftState LExp

89lift :: [Name] -> LExp -> State LiftState LExp

87lift env (LV v) = return (LV v)

90lift env (LV v) = return (LV v)

91+lift env (LApp tc (LV (Glob n)) args) = do args' <- mapM (lift env) args

92+ return (LApp tc (LV (Glob n)) args')

93+lift env (LApp tc f args) = do f' <- lift env f

94+ fn <- getNextName

95+ addFn fn (LFun fn env f')

88−lift env (LApp tc n args) = do args' <- mapM (lift env) args

96+ args' <- mapM (lift env) args

89− return (LApp tc n args')

97+ return (LApp tc (LV (Glob fn)) (map (LV . Glob) env ++ args'))

90lift env (LLazyApp n args) = do args' <- mapM (lift env) args

98lift env (LLazyApp n args) = do args' <- mapM (lift env) args

91 return (LLazyApp n args')

99 return (LLazyApp n args')

92lift env (LLazyExp (LConst c)) = return (LConst c)

100lift env (LLazyExp (LConst c)) = return (LConst c)

@@ -94,13 +102,15 @@ lift env (LLazyExp e) = do e' <- lift env e

94 fn <- getNextName

102 fn <- getNextName

95 addFn fn (LFun fn env e')

103 addFn fn (LFun fn env e')

96 return (LLazyApp fn (map (LV . Glob) env))

104 return (LLazyApp fn (map (LV . Glob) env))

105+lift env (LForce e) = do e' <- lift env e

106+ return (LForce e')

97lift env (LLet n v e) = do v' <- lift env v

107lift env (LLet n v e) = do v' <- lift env v

98 e' <- lift (env ++ [n]) e

108 e' <- lift (env ++ [n]) e

99 return (LLet n v' e')

109 return (LLet n v' e')

100lift env (LLam args e) = do e' <- lift (env ++ args) e

110lift env (LLam args e) = do e' <- lift (env ++ args) e

101 fn <- getNextName

111 fn <- getNextName

102 addFn fn (LFun fn (env ++ args) e')

112 addFn fn (LFun fn (env ++ args) e')

103− return (LApp False fn (map (LV . Glob) env))

113+ return (LApp False (LV (Glob fn)) (map (LV . Glob) env))

104lift env (LCon i n args) = do args' <- mapM (lift env) args

114lift env (LCon i n args) = do args' <- mapM (lift env) args

105 return (LCon i n args')

115 return (LCon i n args')

106lift env (LCase e alts) = do alts' <- mapM liftA alts

116lift env (LCase e alts) = do alts' <- mapM liftA alts

@@ -121,7 +131,7 @@ lift env (LForeign l t s args) = do args' <- mapM (liftF env) args

121 return (t, e')

131 return (t, e')

122lift env (LOp f args) = do args' <- mapM (lift env) args

132lift env (LOp f args) = do args' <- mapM (lift env) args

123 return (LOp f args')

133 return (LOp f args')

124−

134+lift env (LError str) = return $ LError str

125

135

126

136

127

137

src/IRTS/Simplified.hs+10−5

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

16 | SConst Const

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

18 | SOp PrimFn [LVar]

19+ | SError String

19 deriving Show

20 deriving Show

21data SAlt = SConCase Int Int Name [Name] SExp

22data SAlt = SConCase Int Int Name [Name] SExp

@@ -42,7 +43,8 @@ simplify tl (LV (Glob x))

42 case lookupCtxt Nothing x ctxt of

43 case lookupCtxt Nothing x ctxt of

43 [LConstructor _ t 0] -> return $ SCon t x []

44 [LConstructor _ t 0] -> return $ SCon t x []

44 _ -> return $ SV (Glob x)

45 _ -> return $ SV (Glob x)

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

46+simplify tl (LApp tc (LV (Glob n)) args)

47+ = do args' <- mapM sVar args

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

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

47simplify tl (LForeign lang ty fn args)

49simplify tl (LForeign lang ty fn args)

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

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

@@ -62,6 +64,7 @@ simplify tl (LCase e alts) = do v <- sVar e

62simplify tl (LConst c) = return (SConst c)

64simplify tl (LConst c) = return (SConst c)

63simplify tl (LOp p args) = do args' <- mapM sVar args

65simplify tl (LOp p args) = do args' <- mapM sVar args

64 mkapp (SOp p) args'

66 mkapp (SOp p) args'

67+simplify tl (LError str) = return $ SError str

66sVar (LV (Glob x))

69sVar (LV (Glob x))

67 = do ctxt <- ldefs

70 = do ctxt <- ldefs

@@ -115,7 +118,8 @@ scopecheck ctxt env tm = sc env tm where

115 Just i -> do lvar i; return (SV (Loc i))

118 Just i -> do lvar i; return (SV (Loc i))

116 Nothing -> case lookupCtxt Nothing n ctxt of

119 Nothing -> case lookupCtxt Nothing n ctxt of

117 [LConstructor _ i ar] ->

120 [LConstructor _ i ar] ->

121+ if True -- ar == 0

118− if ar == 0 then return (SCon i n [])

122+ then return (SCon i n [])

119 else fail $ "Codegen error: Constructor " ++ show n ++

123 else fail $ "Codegen error: Constructor " ++ show n ++

120 " has arity " ++ show ar

124 " has arity " ++ show ar

121 [_] -> return (SV (Glob n))

125 [_] -> return (SV (Glob n))

@@ -124,7 +128,7 @@ scopecheck ctxt env tm = sc env tm where

124 = do args' <- mapM (scVar env) args

128 = do args' <- mapM (scVar env) args

125 case lookupCtxt Nothing f ctxt of

129 case lookupCtxt Nothing f ctxt of

126 [LConstructor n tag ar] ->

130 [LConstructor n tag ar] ->

127− if (ar == length args)

131+ if True -- (ar == length args)

128 then return $ SCon tag n args'

132 then return $ SCon tag n args'

129 else fail $ "Codegen error: Constructor " ++ show f ++

133 else fail $ "Codegen error: Constructor " ++ show f ++

130 " has arity " ++ show ar

134 " has arity " ++ show ar

@@ -138,7 +142,7 @@ scopecheck ctxt env tm = sc env tm where

138 = do args' <- mapM (scVar env) args

142 = do args' <- mapM (scVar env) args

139 case lookupCtxt Nothing f ctxt of

143 case lookupCtxt Nothing f ctxt of

140 [LConstructor n tag ar] ->

144 [LConstructor n tag ar] ->

141− if (ar == length args)

145+ if True -- (ar == length args)

142 then return $ SCon tag n args'

146 then return $ SCon tag n args'

143 else fail $ "Codegen error: Constructor " ++ show f ++

147 else fail $ "Codegen error: Constructor " ++ show f ++

144 " has arity " ++ show ar

148 " has arity " ++ show ar

@@ -172,7 +176,8 @@ scopecheck ctxt env tm = sc env tm where

172 = do let env' = env ++ zip args [length env..]

176 = do let env' = env ++ zip args [length env..]

173 tag <- case lookupCtxt Nothing n ctxt of

177 tag <- case lookupCtxt Nothing n ctxt of

174 [LConstructor _ i ar] ->

178 [LConstructor _ i ar] ->

175− if (length args == ar) then return i

179+ if True -- (length args == ar)

180+ then return i

176 else fail $ "Codegen error: Constructor " ++ show n ++

181 else fail $ "Codegen error: Constructor " ++ show n ++

177 " has arity " ++ show ar

182 " has arity " ++ show ar

178 _ -> fail $ "Codegen error: No constructor " ++ show n

183 _ -> fail $ "Codegen error: No constructor " ++ show n

src/Idris/AbsSyntaxTree.hs+2−2

@@ -7,7 +7,7 @@ import Core.TT

7import Core.Evaluate

8import Core.Elaborate hiding (Tactic(..))

9import Core.Typecheck

10−import RTS.SC

10+import IRTS.Lang

11import Util.Pretty

13import Paths_idris

@@ -66,7 +66,7 @@ data IState = IState { tt_ctxt :: Context,

66 syntax_keywords :: [String],

67 imported :: [FilePath],

68 idris_prims :: [(Name, ([E.Name], E.Term))],

69− idris_scprims :: Prims,

69+ idris_scprims :: [(Name, (Int, PrimFn))],

70 idris_objs :: [FilePath],

71 idris_libs :: [String],

72 idris_hdrs :: [String],

src/Idris/Primitives.hs+66−66

@@ -6,7 +6,7 @@ import Idris.ElabDecls

6import Idris.ElabTerm

7import Idris.AbsSyntax

9−import RTS.SC

9+import IRTS.Lang

11import Core.TT

12import Core.Evaluate

@@ -19,7 +19,7 @@ data Prim = Prim { p_name :: Name,

19 p_arity :: Int,

20 p_def :: [Value] -> Maybe Value,

21 p_epic :: ([E.Name], E.Term),

22− p_sc :: ([CType], CType, SPrim),

22+ p_lexp :: (Int, PrimFn),

23 p_total :: Totality

24 }

@@ -82,146 +82,146 @@ partial = Partial NotCovering

82primitives =

83 -- operators

84 [Prim (UN "prim__addInt") (ty [IType, IType] IType) 2 (iBin (+))

85− (eOp E.plus_) ([sInt, sInt], sInt, AddI) total,

85+ (eOp E.plus_) (2, LPlus) total,

86 Prim (UN "prim__subInt") (ty [IType, IType] IType) 2 (iBin (-))

87 (eOp E.minus_)

88− ([sInt, sInt], sInt, SubI) total,

88+ (2, LMinus) total,

89 Prim (UN "prim__mulInt") (ty [IType, IType] IType) 2 (iBin (*))

90− (eOp E.times_) ([sInt, sInt], sInt, MulI) total,

90+ (eOp E.times_) (2, LTimes) total,

91 Prim (UN "prim__divInt") (ty [IType, IType] IType) 2 (iBin (div))

92− (eOp E.divide_) ([sInt, sInt], sInt, DivI) partial,

92+ (eOp E.divide_) (2, LDiv) partial,

93 Prim (UN "prim__eqInt") (ty [IType, IType] IType) 2 (biBin (==))

94− (eOp E.eq_) ([sInt, sInt], sInt, EqI) total,

94+ (eOp E.eq_) (2, LEq) total,

95 Prim (UN "prim__ltInt") (ty [IType, IType] IType) 2 (biBin (<))

96− (eOp E.lt_) ([sInt, sInt], sInt, LtI) total,

96+ (eOp E.lt_) (2, LLt) total,

97 Prim (UN "prim__lteInt") (ty [IType, IType] IType) 2 (biBin (<=))

98− (eOp E.lte_) ([sInt, sInt], sInt, LteI) total,

98+ (eOp E.lte_) (2, LLe) total,

99 Prim (UN "prim__gtInt") (ty [IType, IType] IType) 2 (biBin (>))

100− (eOp E.gt_) ([sInt, sInt], sInt, GtI) total,

100+ (eOp E.gt_) (2, LGt) total,

101 Prim (UN "prim__gteInt") (ty [IType, IType] IType) 2 (biBin (>=))

102− (eOp E.gte_) ([sInt, sInt], sInt, GteI) total,

102+ (eOp E.gte_) (2, LGe) total,

103 Prim (UN "prim__eqChar") (ty [ChType, ChType] IType) 2 (bcBin (==))

104− (eOp E.eq_) ([sChar, sChar], sInt, EqC) total,

104+ (eOp E.eq_) (2, LEq) total,

105 Prim (UN "prim__ltChar") (ty [ChType, ChType] IType) 2 (bcBin (<))

106− (eOp E.lt_) ([sChar, sChar], sInt, LtC) total,

106+ (eOp E.lt_) (2, LLt) total,

107 Prim (UN "prim__lteChar") (ty [ChType, ChType] IType) 2 (bcBin (<=))

108− (eOp E.lte_) ([sChar, sChar], sInt, LteC) total,

108+ (eOp E.lte_) (2, LLe) total,

109 Prim (UN "prim__gtChar") (ty [ChType, ChType] IType) 2 (bcBin (>))

110− (eOp E.gt_) ([sChar, sChar], sInt, GtC) total,

110+ (eOp E.gt_) (2, LGt) total,

111 Prim (UN "prim__gteChar") (ty [ChType, ChType] IType) 2 (bcBin (>=))

112− (eOp E.gte_) ([sChar, sChar], sInt, GteC) total,

112+ (eOp E.gte_) (2, LGe) total,

113 Prim (UN "prim__addBigInt") (ty [BIType, BIType] BIType) 2 (bBin (+))

114 (eOpFn tyBigInt tyBigInt "addBig")

115− ([sBigInt, sBigInt], sBigInt, AddBI) total,

115+ (2, LBPlus) total,

116 Prim (UN "prim__subBigInt") (ty [BIType, BIType] BIType) 2 (bBin (-))

117− (eOpFn tyBigInt tyBigInt "subBig") ([sBigInt, sBigInt], sBigInt, SubBI) total,

117+ (eOpFn tyBigInt tyBigInt "subBig") (2, LBMinus) total,

118 Prim (UN "prim__mulBigInt") (ty [BIType, BIType] BIType) 2 (bBin (*))

119− (eOpFn tyBigInt tyBigInt "mulBig") ([sBigInt, sBigInt], sBigInt, MulBI) total,

119+ (eOpFn tyBigInt tyBigInt "mulBig") (2, LBTimes) total,

120 Prim (UN "prim__divBigInt") (ty [BIType, BIType] BIType) 2 (bBin (div))

121− (eOpFn tyBigInt tyBigInt "divBig") ([sBigInt, sBigInt], sBigInt,DivBI) partial,

121+ (eOpFn tyBigInt tyBigInt "divBig") (2, LBDiv) partial,

122 Prim (UN "prim__eqBigInt") (ty [BIType, BIType] IType) 2 (bbBin (==))

123− (eOpFn tyBigInt tyInt "eqBig") ([sBigInt, sBigInt], sInt, EqBI) total,

123+ (eOpFn tyBigInt tyInt "eqBig") (2, LBEq) total,

124 Prim (UN "prim__ltBigInt") (ty [BIType, BIType] IType) 2 (bbBin (<))

125− (eOpFn tyBigInt tyInt "ltBig") ([sBigInt, sBigInt], sInt, LtBI) total,

125+ (eOpFn tyBigInt tyInt "ltBig") (2, LBLt) total,

126 Prim (UN "prim__lteBigInt") (ty [BIType, BIType] IType) 2 (bbBin (<=))

127− (eOpFn tyBigInt tyInt "leBig") ([sBigInt, sBigInt], sInt, LteBI) total,

127+ (eOpFn tyBigInt tyInt "leBig") (2, LBLe) total,

128 Prim (UN "prim__gtBigInt") (ty [BIType, BIType] IType) 2 (bbBin (>))

129− (eOpFn tyBigInt tyInt "gtBig") ([sBigInt, sBigInt], sInt, GtBI) total,

129+ (eOpFn tyBigInt tyInt "gtBig") (2, LBGt) total,

130 Prim (UN "prim__gtBigInt") (ty [BIType, BIType] IType) 2 (bbBin (>=))

131− (eOpFn tyBigInt tyInt "geBig") ([sBigInt, sBigInt], sInt, GteBI) total,

131+ (eOpFn tyBigInt tyInt "geBig") (2, LBGe) total,

132 Prim (UN "prim__addFloat") (ty [FlType, FlType] FlType) 2 (fBin (+))

133− (eOp E.plusF_) ([sFloat, sFloat], sFloat, AddF) total,

133+ (eOp E.plusF_) (2, LFPlus) total,

134 Prim (UN "prim__subFloat") (ty [FlType, FlType] FlType) 2 (fBin (-))

135− (eOp E.minusF_) ([sFloat, sFloat], sFloat, SubF) total,

135+ (eOp E.minusF_) (2, LFMinus) total,

136 Prim (UN "prim__mulFloat") (ty [FlType, FlType] FlType) 2 (fBin (*))

137− (eOp E.timesF_) ([sFloat, sFloat], sFloat, MulF) total,

137+ (eOp E.timesF_) (2, LFTimes) total,

138 Prim (UN "prim__divFloat") (ty [FlType, FlType] FlType) 2 (fBin (/))

139− (eOp E.divideF_) ([sFloat, sFloat], sFloat, DivF) total,

139+ (eOp E.divideF_) (2, LFDiv) total,

140 Prim (UN "prim__eqFloat") (ty [FlType, FlType] IType) 2 (bfBin (==))

141− (eOp E.eqF_) ([sFloat, sFloat], sInt, EqF) total,

141+ (eOp E.eqF_) (2, LFEq) total,

142 Prim (UN "prim__ltFloat") (ty [FlType, FlType] IType) 2 (bfBin (<))

143− (eOp E.ltF_) ([sFloat, sFloat], sInt, LtF) total,

143+ (eOp E.ltF_) (2, LFLt) total,

144 Prim (UN "prim__lteFloat") (ty [FlType, FlType] IType) 2 (bfBin (<=))

145− (eOp E.lteF_) ([sFloat, sFloat], sInt, LteF) total,

145+ (eOp E.lteF_) (2, LFLe) total,

146 Prim (UN "prim__gtFloat") (ty [FlType, FlType] IType) 2 (bfBin (>))

147− (eOp E.gtF_) ([sFloat, sFloat], sInt, GtF) total,

147+ (eOp E.gtF_) (2, LFGt) total,

148 Prim (UN "prim__gteFloat") (ty [FlType, FlType] IType) 2 (bfBin (>=))

149− (eOp E.gteF_) ([sFloat, sFloat], sInt, GteF) total,

149+ (eOp E.gteF_) (2, LFGe) total,

150 Prim (UN "prim__concat") (ty [StrType, StrType] StrType) 2 (sBin (++))

151 ([E.name "x", E.name "y"], (fun "append") @@ fun "x" @@ fun "y")

152− ([sString, sString], sString, ConcatS) total,

152+ (2, LStrConcat) total,

153 Prim (UN "prim__eqString") (ty [StrType, StrType] IType) 2 (bsBin (==))

154 ([E.name "x", E.name "y"], strEq (fun "x") (fun "y"))

155− ([sString, sString], sInt, EqS) total,

155+ (2, LStrEq) total,

156 Prim (UN "prim__ltString") (ty [StrType, StrType] IType) 2 (bsBin (<))

157 ([E.name "x", E.name "y"], strLt (fun "x") (fun "y"))

158− ([sString, sString], sInt, LtS) total,

158+ (2, LStrLt) total,

159 -- Conversions

160 Prim (UN "prim__strToInt") (ty [StrType] IType) 1 (c_strToInt)

161− ([E.name "x"], strToInt (fun "x")) ([sString], sInt, StoI) total,

161+ ([E.name "x"], strToInt (fun "x")) (1, LStrInt) total,

162 Prim (UN "prim__intToStr") (ty [IType] StrType) 1 (c_intToStr)

163− ([E.name "x"], intToStr (fun "x")) ([sInt], sString, ItoS) total,

163+ ([E.name "x"], intToStr (fun "x")) (1, LIntStr) total,

164 Prim (UN "prim__charToInt") (ty [ChType] IType) 1 (c_charToInt)

165− ([E.name "x"], charToInt (fun "x")) ([sChar], sInt, CtoI) total,

165+ ([E.name "x"], charToInt (fun "x")) (1, LNoOp) total,

166 Prim (UN "prim__intToChar") (ty [IType] ChType) 1 (c_intToChar)

167− ([E.name "x"], intToChar (fun "x")) ([sInt], sChar, ItoC) total,

167+ ([E.name "x"], intToChar (fun "x")) (1, LNoOp) total,

168 Prim (UN "prim__intToBigInt") (ty [IType] BIType) 1 (c_intToBigInt)

169− ([E.name "x"], intToBigInt (fun "x")) ([sInt], sBigInt, ItoBI) total,

169+ ([E.name "x"], intToBigInt (fun "x")) (1, LIntBig) total,

170 Prim (UN "prim__bigIntToInt") (ty [BIType] IType) 1 (c_bigIntToInt)

171− ([E.name "x"], bigIntToInt (fun "x")) ([sBigInt], sInt, BItoI) total,

171+ ([E.name "x"], bigIntToInt (fun "x")) (1, LBigInt) total,

172 Prim (UN "prim__strToBigInt") (ty [StrType] BIType) 1 (c_strToBigInt)

173− ([E.name "x"], strToBigInt (fun "x")) ([sString], sBigInt, StoBI) total,

173+ ([E.name "x"], strToBigInt (fun "x")) (1, LStrBig) total,

174 Prim (UN "prim__bigIntToStr") (ty [BIType] StrType) 1 (c_bigIntToStr)

175− ([E.name "x"], bigIntToStr (fun "x")) ([sBigInt], sString, BItoS) total,

175+ ([E.name "x"], bigIntToStr (fun "x")) (1, LBigStr) total,

176 Prim (UN "prim__strToFloat") (ty [StrType] FlType) 1 (c_strToFloat)

177− ([E.name "x"], strToFloat (fun "x")) ([sString], sFloat, StoF) total,

177+ ([E.name "x"], strToFloat (fun "x")) (1, LStrFloat) total,

178 Prim (UN "prim__floatToStr") (ty [FlType] StrType) 1 (c_floatToStr)

179− ([E.name "x"], floatToStr (fun "x")) ([sFloat], sString, FtoS) total,

179+ ([E.name "x"], floatToStr (fun "x")) (1, LFloatStr) total,

180 Prim (UN "prim__intToFloat") (ty [IType] FlType) 1 (c_intToFloat)

181− ([E.name "x"], intToFloat (fun "x")) ([sInt], sFloat, ItoF) total,

181+ ([E.name "x"], intToFloat (fun "x")) (1, LIntFloat) total,

182 Prim (UN "prim__floatToInt") (ty [FlType] IType) 1 (c_floatToInt)

183− ([E.name "x"], floatToInt (fun "x")) ([sFloat], sInt, FtoI) total,

183+ ([E.name "x"], floatToInt (fun "x")) (1, LFloatInt) total,

184

185 Prim (UN "prim__floatExp") (ty [FlType] FlType) 1 (p_floatExp)

186− ([E.name "x"], floatExp (fun "x")) ([sFloat], sFloat, ExpF) total,

186+ ([E.name "x"], floatExp (fun "x")) (1, LFExp) total,

187 Prim (UN "prim__floatLog") (ty [FlType] FlType) 1 (p_floatLog)

188− ([E.name "x"], floatLog (fun "x")) ([sFloat], sFloat, LogF) total,

188+ ([E.name "x"], floatLog (fun "x")) (1, LFLog) total,

189 Prim (UN "prim__floatSin") (ty [FlType] FlType) 1 (p_floatSin)

190− ([E.name "x"], floatSin (fun "x")) ([sFloat], sFloat, SinF) total,

190+ ([E.name "x"], floatSin (fun "x")) (1, LFSin) total,

191 Prim (UN "prim__floatCos") (ty [FlType] FlType) 1 (p_floatCos)

192− ([E.name "x"], floatCos (fun "x")) ([sFloat], sFloat, CosF) total,

192+ ([E.name "x"], floatCos (fun "x")) (1, LFCos) total,

193 Prim (UN "prim__floatTan") (ty [FlType] FlType) 1 (p_floatTan)

194− ([E.name "x"], floatTan (fun "x")) ([sFloat], sFloat, TanF) total,

194+ ([E.name "x"], floatTan (fun "x")) (1, LFTan) total,

195 Prim (UN "prim__floatASin") (ty [FlType] FlType) 1 (p_floatASin)

196− ([E.name "x"], floatASin (fun "x")) ([sFloat], sFloat, ASinF) total,

196+ ([E.name "x"], floatASin (fun "x")) (1, LFASin) total,

197 Prim (UN "prim__floatACos") (ty [FlType] FlType) 1 (p_floatACos)

198− ([E.name "x"], floatACos (fun "x")) ([sFloat], sFloat, ACosF) total,

198+ ([E.name "x"], floatACos (fun "x")) (1, LFACos) total,

199 Prim (UN "prim__floatATan") (ty [FlType] FlType) 1 (p_floatATan)

200− ([E.name "x"], floatATan (fun "x")) ([sFloat], sFloat, ATanF) total,

200+ ([E.name "x"], floatATan (fun "x")) (1, LFATan) total,

201 Prim (UN "prim__floatSqrt") (ty [FlType] FlType) 1 (p_floatSqrt)

202− ([E.name "x"], floatSqrt (fun "x")) ([sFloat], sFloat, SqrtF) total,

202+ ([E.name "x"], floatSqrt (fun "x")) (1, LFSqrt) total,

203 Prim (UN "prim__floatFloor") (ty [FlType] FlType) 1 (p_floatFloor)

204− ([E.name "x"], floatFloor (fun "x")) ([sFloat], sFloat, FloorF) total,

204+ ([E.name "x"], floatFloor (fun "x")) (1, LFFloor) total,

205 Prim (UN "prim__floatCeil") (ty [FlType] FlType) 1 (p_floatCeil)

206− ([E.name "x"], floatCeil (fun "x")) ([sFloat], sFloat, CeilF) total,

206+ ([E.name "x"], floatCeil (fun "x")) (1, LFCeil) total,

207

208 Prim (UN "prim__strHead") (ty [StrType] ChType) 1 (p_strHead)

209− ([E.name "x"], strHead (fun "x")) ([sString], sChar, HeadS) partial,

209+ ([E.name "x"], strHead (fun "x")) (1, LStrHead) partial,

210 Prim (UN "prim__strTail") (ty [StrType] StrType) 1 (p_strTail)

211− ([E.name "x"], strTail (fun "x")) ([sString], sString, TailS) partial,

211+ ([E.name "x"], strTail (fun "x")) (1, LStrTail) partial,

212 Prim (UN "prim__strCons") (ty [ChType, StrType] StrType) 2 (p_strCons)

213 ([E.name "x", E.name "xs"], strCons (fun "x") (fun "xs"))

214− ([sChar, sString], sString, ConsS) total,

214+ (2, LStrCons) total,

215 Prim (UN "prim__strIndex") (ty [StrType, IType] ChType) 2 (p_strIndex)

216 ([E.name "x", E.name "i"], strIndex (fun "x") (fun "i"))

217− ([sString, sInt], sChar, IndexS) partial,

217+ (2, LStrIndex) partial,

218 Prim (UN "prim__strRev") (ty [StrType] StrType) 1 (p_strRev)

219 ([E.name "x"], strRev (fun "x"))

220− ([sString], sString, RevS) total,

220+ (1, LStrRev) total,

221

222 Prim (UN "prim__believe_me") believeTy 3 (p_believeMe)

223 ([E.name "a", E.name "b", E.name "x"], fun "x")

224− ([Nothing], Nothing, BelieveMe) total -- ahem

224+ (1, LNoOp) total -- ahem

225 ]

226

227p_believeMe [_,_,x] = Just x

src/Idris/REPL.hs+6−17

@@ -20,10 +20,12 @@ import Core.ProofShell

20import Core.TT

21import Core.Constraints

23+import IRTS.Compiler

24+

23−import RTS.SC

25+-- import RTS.SC

24−import RTS.Bytecode

26+-- import RTS.Bytecode

25−import RTS.PreC

27+-- import RTS.PreC

26−import RTS.CodegenC

28+-- import RTS.CodegenC

28import System.Console.Haskeline as H

30import System.Console.Haskeline as H

29import System.FilePath

31import System.FilePath

@@ -223,19 +225,6 @@ process fn (DebugInfo n)

223 let d = lookupDef Nothing n (tt_ctxt i)

225 let d = lookupDef Nothing n (tt_ctxt i)

224 when (not (null d)) $ liftIO $

226 when (not (null d)) $ liftIO $

225 do print (head d)

227 do print (head d)

226− let prims = idris_scprims i

227− let scs = toSC prims (n, head d)

228− let bcs = bcdefs scs

229− let pcs = preCdefs bcs

230− let code = cdefs pcs

231− putStrLn "Supercombinators:\n"

232− print (toSC prims (n, head d))

233− putStrLn "\nBytecode:\n"

234− putStrLn (showSep "\n" (map show bcs))

235− putStrLn "\nPre-C:\n"

236− putStrLn (showSep "\n" (map show pcs))

237− putStrLn "\nCode:\n"

238− putStrLn code

239process fn (Info n) = do i <- get

228process fn (Info n) = do i <- get

240 case lookupCtxt Nothing n (idris_classes i) of

229 case lookupCtxt Nothing n (idris_classes i) of

241 [c] -> classInfo c

230 [c] -> classInfo c