b642db5 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Almost working new back end

commitb642db52acfe6140cbebae8ab54a2ba3cc899089 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateSat 8 Sep 2012, 00:49 (14 years ago) parente99339c

13 files changed+142−124

compare with master

unifiedsplit

idris.cabal+1−1 lib/prelude/nat.idr+1−1 rts/idris_main.c+2−2 rts/idris_rts.c+9−2 src/IRTS/Bytecode.hs+3−1 src/IRTS/CodegenC.hs+2 src/IRTS/Defunctionalise.hs+23−20 src/IRTS/LParser.hs+2−2 src/IRTS/Lang.hs+15−5 src/IRTS/Simplified.hs+10−5 src/Idris/AbsSyntaxTree.hs+2−2 src/Idris/Primitives.hs+66−66 src/Idris/REPL.hs+6−17

idris.cabal+1−1

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

7272

7373 RTS.Bytecode, RTS.SC, RTS.PreC, RTS.CodegenC,

7474 IRTS.Lang, IRTS.LParser, IRTS.Bytecode, IRTS.Simplified,

75− IRTS.CodegenC, IRTS.Defunctionalise,

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

7676

7777 Paths_idris

7878

lib/prelude/nat.idr+1−1

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

123123

124124 abs x = x

125125

126− fromInteger = fromInteger'

126+ fromInteger x = fromInteger' x

127127 where

128128 %assert_total

129129 fromInteger' : Int -> Nat

rts/idris_main.c+2−2

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

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

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

3−

4− _idris_main(vm, NULL);

3+ _idris__123_runMain0_125_(vm, NULL);

4+ //_idris_main(vm, NULL);

55#ifdef IDRIS_TRACE

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

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

rts/idris_rts.c+9−2

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

124124

125125void dumpVal(VAL v) {

126126 int i;

127+ if (ISINT(v)) {

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

129+ return;

130+ }

127131 switch(v->ty) {

128132 case CON:

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

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

132136 dumpVal(args[i]);

133137 }

134138 printf("] ");

139+ break;

140+ default:

141+ printf("val");

135142 }

136143

137144}

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

230237}

231238

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

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

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

234241}

235242

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

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

249256}

250257

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

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

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

253260}

254261

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

src/IRTS/Bytecode.hs+3−1

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

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

4141 | STOREOLD -- set OLDBASE = BASE

4242 | OP Reg PrimFn [Reg]

43+ | ERROR String

4344 deriving Show

4445

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

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

5556 [BC]

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

5758bc 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

5960 = RESERVE (length vs) : moveReg 0 vs

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

6162 assign reg RVal ++ clean r

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

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

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

7374 where getL (Loc x) = L x

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

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

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

7678 | 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)

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

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

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

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

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

139140

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

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

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

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

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

224+doOp v LNoOp [x] = ""

223225doOp _ _ _ = "FAIL"

224226

225227tempfile :: IO (FilePath, Handle)

src/IRTS/Defunctionalise.hs+23−20

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

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

3939 where

4040 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)) [])

4242-- 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)

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

4545 case lookupCtxt Nothing n defs of

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

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

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

4848 fixApply tc n args' arity

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

5050 aa env (LLazyApp n args)

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

5252 case lookupCtxt Nothing n defs of

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

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

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

5555 fixLazyApply n args' arity

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

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

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

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

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

6061 aa env (LConst c) = LConst c

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

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

64+ aa env (LError e) = LError e

6365

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

6567

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

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

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

6971

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

71−

7272 fixApply tc n args ar

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

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

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

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

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

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

7676

7777 fixLazyApply n args ar

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

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

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

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

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

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

8181

8282 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]

8486

8587data EvalApply a = EvalCase a

8688 | ApplyCase a

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

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

9193

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

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

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

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

96− :

97− mkApplyCase n 0 i

95+toCons (n, i)

96+ = (mkFnCon n, i,

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

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

99+ : mkApplyCase n 0 i

98100

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

100102mkApplyCase fname n ar

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

102104 (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)))))

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

105107 [MN 0 "arg"])))))

106108 : mkApplyCase fname (n + 1) ar

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

116118

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

118120mkApply 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"))])

120123 (mapMaybe applyCase xs)))

121124 where

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

src/IRTS/LParser.hs+2−2

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

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

5151 let ctxtIn = addAlist tagged emptyContext

5252 let defuns = defunctionalise nexttag ctxtIn

53−-- print defuns

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

5454 let checked = checkDefs defuns (toAlist defuns)

5555-- print checked

5656 case checked of

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

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

136136 else return (LV (Glob x))

137137 else if lazy then return (LLazyApp x args)

138− else return (LApp tc x args))

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

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

140140 <|> pLConst

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

src/IRTS/Lang.hs+15−5

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

77 deriving Show

99data LExp = LV LVar

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

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

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

1212 | LLazyExp LExp

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

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

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

1516 | LCon Int Name [LExp]

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

1718 | LConst Const

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

1920 | LOp PrimFn [LExp]

21+ | LError String

2022 deriving Show

2123

2224data 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

3133 | LFSqrt | LFFloor | LFCeil

3234

36+ | LNoOp

3437 deriving Show

3538

3639-- Supported target languages for foreign calls

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

8588

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

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

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

89− return (LApp tc n args')

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')

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

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

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

9199 return (LLazyApp n args')

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

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

94102 fn <- getNextName

95103 addFn fn (LFun fn env e')

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

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

106+ return (LForce e')

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

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

99109 return (LLet n v' e')

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

101111 fn <- getNextName

102112 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))

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

105115 return (LCon i n args')

106116lift 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

121131 return (t, e')

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

123133 return (LOp f args')

124−

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

125135

126136

127137

src/IRTS/Simplified.hs+10−5

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

1616 | SConst Const

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

1818 | SOp PrimFn [LVar]

19+ | SError String

1920 deriving Show

2021

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

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

4243 case lookupCtxt Nothing x ctxt of

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

4445 _ -> 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

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

4749simplify tl (LForeign lang ty fn args)

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

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

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

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

6466 mkapp (SOp p) args'

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

6568

6669sVar (LV (Glob x))

6770 = do ctxt <- ldefs

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

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

116119 Nothing -> case lookupCtxt Nothing n ctxt of

117120 [LConstructor _ i ar] ->

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

121+ if True -- ar == 0

122+ then return (SCon i n [])

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

120124 " has arity " ++ show ar

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

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

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

125129 case lookupCtxt Nothing f ctxt of

126130 [LConstructor n tag ar] ->

127− if (ar == length args)

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

128132 then return $ SCon tag n args'

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

130134 " has arity " ++ show ar

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

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

139143 case lookupCtxt Nothing f ctxt of

140144 [LConstructor n tag ar] ->

141− if (ar == length args)

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

142146 then return $ SCon tag n args'

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

144148 " has arity " ++ show ar

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

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

173177 tag <- case lookupCtxt Nothing n ctxt of

174178 [LConstructor _ i ar] ->

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

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

180+ then return i

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

177182 " has arity " ++ show ar

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

src/Idris/AbsSyntaxTree.hs+2−2

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

77import Core.Evaluate

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

99import Core.Typecheck

10−import RTS.SC

10+import IRTS.Lang

1111import Util.Pretty

1212

1313import Paths_idris

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

6666 syntax_keywords :: [String],

6767 imported :: [FilePath],

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

69− idris_scprims :: Prims,

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

7070 idris_objs :: [FilePath],

7171 idris_libs :: [String],

7272 idris_hdrs :: [String],

src/Idris/Primitives.hs+66−66

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

66import Idris.ElabTerm

77import Idris.AbsSyntax

9−import RTS.SC

9+import IRTS.Lang

1010

1111import Core.TT

1212import Core.Evaluate

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

1919 p_arity :: Int,

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

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

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

22+ p_lexp :: (Int, PrimFn),

2323 p_total :: Totality

2424 }

2525

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

8282primitives =

8383 -- operators

8484 [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,

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

8787 (eOp E.minus_)

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

88+ (2, LMinus) total,

8989 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,

9191 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,

9393 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,

9595 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,

9797 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,

9999 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,

101101 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,

103103 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,

105105 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,

107107 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,

109109 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,

111111 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,

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

114114 (eOpFn tyBigInt tyBigInt "addBig")

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

115+ (2, LBPlus) total,

116116 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,

118118 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,

120120 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,

122122 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,

124124 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,

126126 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,

128128 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,

130130 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,

132132 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,

134134 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,

136136 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,

138138 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,

140140 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,

142142 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,

144144 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,

146146 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,

148148 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,

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

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

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

152+ (2, LStrConcat) total,

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

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

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

155+ (2, LStrEq) total,

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

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

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

158+ (2, LStrLt) total,

159159 -- Conversions

160160 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,

162162 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,

164164 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,

166166 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,

168168 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,

170170 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,

172172 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,

174174 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,

176176 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,

178178 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,

180180 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,

182182 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,

184184

185185 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,

187187 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,

189189 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,

191191 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,

193193 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,

195195 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,

197197 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,

199199 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,

201201 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,

203203 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,

205205 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,

207207

208208 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,

210210 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,

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

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

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

214+ (2, LStrCons) total,

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

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

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

217+ (2, LStrIndex) partial,

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

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

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

220+ (1, LStrRev) total,

221221

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

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

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

224+ (1, LNoOp) total -- ahem

225225 ]

226226

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

src/Idris/REPL.hs+6−17

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

2020import Core.TT

2121import Core.Constraints

2222

23−import RTS.SC

24−import RTS.Bytecode

25−import RTS.PreC

26−import RTS.CodegenC

23+import IRTS.Compiler

24+

25+-- import RTS.SC

26+-- import RTS.Bytecode

27+-- import RTS.PreC

28+-- import RTS.CodegenC

2729

2830import System.Console.Haskeline as H

2931import System.FilePath

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

223225 let d = lookupDef Nothing n (tt_ctxt i)

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

225227 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

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

240229 case lookupCtxt Nothing n (idris_classes i) of

241230 [c] -> classInfo c