mirror of
https://github.com/ilyakooo0/Idris-dev.git
synced 2024-11-15 01:25:05 +03:00
Almost working new back end
This commit is contained in:
Edwin Brady
parent
e99339cb9c
commit
b642db52ac
@ -72,7 +72,7 @@ Executable idris
|
||||
|
||||
RTS.Bytecode, RTS.SC, RTS.PreC, RTS.CodegenC,
|
||||
IRTS.Lang, IRTS.LParser, IRTS.Bytecode, IRTS.Simplified,
|
||||
IRTS.CodegenC, IRTS.Defunctionalise,
|
||||
IRTS.CodegenC, IRTS.Defunctionalise, IRTS.Compiler,
|
||||
|
||||
Paths_idris
|
||||
|
||||
|
||||
@ -123,7 +123,7 @@ instance Num Nat where
|
||||
|
||||
abs x = x
|
||||
|
||||
fromInteger = fromInteger'
|
||||
fromInteger x = fromInteger' x
|
||||
where
|
||||
%assert_total
|
||||
fromInteger' : Int -> Nat
|
||||
|
||||
@ -1,7 +1,7 @@
|
||||
int main(int argc, char* argv[]) {
|
||||
VM* vm = init_vm(1024000, 1024000);
|
||||
|
||||
_idris_main(vm, NULL);
|
||||
_idris__123_runMain0_125_(vm, NULL);
|
||||
//_idris_main(vm, NULL);
|
||||
#ifdef IDRIS_TRACE
|
||||
printf("\nStack: %p %p\n", vm->valstack, vm->valstack_top);
|
||||
printf("Total allocations: %d\n", vm->allocations);
|
||||
|
||||
@ -124,6 +124,10 @@ void SLIDE(VM* vm, int args) {
|
||||
|
||||
void dumpVal(VAL v) {
|
||||
int i;
|
||||
if (ISINT(v)) {
|
||||
printf("%ld ", GETINT(v));
|
||||
return;
|
||||
}
|
||||
switch(v->ty) {
|
||||
case CON:
|
||||
printf("%d[", v->info.c.tag);
|
||||
@ -132,6 +136,9 @@ void dumpVal(VAL v) {
|
||||
dumpVal(args[i]);
|
||||
}
|
||||
printf("] ");
|
||||
break;
|
||||
default:
|
||||
printf("val");
|
||||
}
|
||||
|
||||
}
|
||||
@ -230,7 +237,7 @@ VAL idris_readStr(VM* vm, FILE* h) {
|
||||
}
|
||||
|
||||
VAL idris_strHead(VM* vm, VAL str) {
|
||||
return MKINT(GETSTR(str)[0]);
|
||||
return MKINT((i_int)(GETSTR(str)[0]));
|
||||
}
|
||||
|
||||
VAL idris_strTail(VM* vm, VAL str) {
|
||||
@ -249,7 +256,7 @@ VAL idris_strCons(VM* vm, VAL x, VAL xs) {
|
||||
}
|
||||
|
||||
VAL idris_strIndex(VM* vm, VAL str, VAL i) {
|
||||
return MKINT(GETSTR(str)[GETINT(i)]);
|
||||
return MKINT((i_int)(GETSTR(str)[GETINT(i)]));
|
||||
}
|
||||
|
||||
VAL idris_strRev(VM* vm, VAL str) {
|
||||
|
||||
@ -40,6 +40,7 @@ data BC = ASSIGN Reg Reg
|
||||
| BASETOP Int -- set BASE = TOP + n
|
||||
| STOREOLD -- set OLDBASE = BASE
|
||||
| OP Reg PrimFn [Reg]
|
||||
| ERROR String
|
||||
deriving Show
|
||||
|
||||
toBC :: (Name, SDecl) -> (Name, [BC])
|
||||
@ -55,7 +56,7 @@ bc :: Reg -> SExp -> Bool -> -- returning
|
||||
[BC]
|
||||
bc reg (SV (Glob n)) r = bc reg (SApp False n []) r
|
||||
bc reg (SV (Loc i)) r = assign reg (L i) ++ clean r
|
||||
bc reg (SApp False f vs) r
|
||||
bc reg (SApp _ f vs) r
|
||||
= RESERVE (length vs) : moveReg 0 vs
|
||||
++ [STOREOLD, BASETOP 0, ADDTOP (length vs), CALL f] ++
|
||||
assign reg RVal ++ clean r
|
||||
@ -71,6 +72,7 @@ bc reg (SCon i _ vs) r = MKCON reg i (map getL vs) : clean r
|
||||
bc reg (SConst i) r = ASSIGNCONST reg i : clean r
|
||||
bc reg (SOp p vs) r = OP reg p (map getL vs) : clean r
|
||||
where getL (Loc x) = L x
|
||||
bc reg (SError str) r = [ERROR str]
|
||||
bc reg (SCase (Loc l) alts) r
|
||||
| isConst alts = constCase reg (L l) alts r
|
||||
| otherwise = conCase reg (L l) alts r
|
||||
|
||||
@ -135,6 +135,7 @@ bcc i (FOREIGNCALL l LANG_C rty fn args)
|
||||
c_irts rty (creg l ++ " = ")
|
||||
(fn ++ "(" ++ showSep "," (map fcall args) ++ ")") ++ ";\n"
|
||||
where fcall (t, arg) = irts_c t (creg arg)
|
||||
bcc i (ERROR str) = indent i ++ "fprintf(stderr, " ++ show str ++ "); exit(-1);"
|
||||
-- bcc i _ = indent i ++ "// not done yet\n"
|
||||
|
||||
c_irts FInt l x = l ++ "MKINT((i_int)(" ++ x ++ ")"
|
||||
@ -220,6 +221,7 @@ doOp v LStrTail [x] = v ++ "idris_strTail(vm, " ++ creg x ++ ")"
|
||||
doOp v LStrCons [x, y] = v ++ "idris_strCons(vm, " ++ creg x ++ "," ++ creg y ++ ")"
|
||||
doOp v LStrIndex [x, y] = v ++ "idris_strIndex(vm, " ++ creg x ++ "," ++ creg y ++ ")"
|
||||
doOp v LStrRev [x] = v ++ "idris_strRev(vm, " ++ creg x ++ ")"
|
||||
doOp v LNoOp [x] = ""
|
||||
doOp _ _ _ = "FAIL"
|
||||
|
||||
tempfile :: IO (FilePath, Handle)
|
||||
|
||||
@ -38,28 +38,30 @@ addApps defs o@(n, LConstructor _ _ _) = o
|
||||
addApps defs (n, LFun _ args e) = (n, LFun n args (aa args e))
|
||||
where
|
||||
aa env (LV (Glob n)) | n `elem` env = LV (Glob n)
|
||||
| otherwise = aa env (LApp False n [])
|
||||
| otherwise = aa env (LApp False (LV (Glob n)) [])
|
||||
-- aa env e@(LApp tc (MN 0 "EVAL") [a]) = e
|
||||
aa env (LApp tc n args)
|
||||
aa env (LApp tc (LV (Glob n)) args)
|
||||
= let args' = map (aa env) args in
|
||||
case lookupCtxt Nothing n defs of
|
||||
[LConstructor _ i ar] -> LApp tc n args'
|
||||
[LConstructor _ i ar] -> LApp tc (LV (Glob n)) args'
|
||||
[LFun _ as _] -> let arity = length as in
|
||||
fixApply tc n args' arity
|
||||
[] -> chainAPPLY (LV (Glob n)) args'
|
||||
aa env (LLazyApp n args)
|
||||
= let args' = map (aa env) args in
|
||||
case lookupCtxt Nothing n defs of
|
||||
[LConstructor _ i ar] -> LApp False n args'
|
||||
[LConstructor _ i ar] -> LApp False (LV (Glob n)) args'
|
||||
[LFun _ as _] -> let arity = length as in
|
||||
fixLazyApply n args' arity
|
||||
[] -> chainAPPLY (LV (Glob n)) args'
|
||||
aa env (LForce e) = eEVAL (aa env e)
|
||||
aa env (LLet n v sc) = LLet n (aa env v) (aa (n : env) sc)
|
||||
aa env (LCon i n args) = LCon i n (map (aa env) args)
|
||||
aa env (LCase e alts) = LCase (eEVAL (aa env e)) (map (aaAlt env) alts)
|
||||
aa env (LConst c) = LConst c
|
||||
aa env (LForeign l t n args) = LForeign l t n (map (aaF env) args)
|
||||
aa env (LOp f args) = LOp f (map (eEVAL . (aa env)) args)
|
||||
aa env (LError e) = LError e
|
||||
|
||||
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))
|
||||
aaAlt env (LConstCase c e) = LConstCase c (aa env e)
|
||||
aaAlt env (LDefaultCase e) = LDefaultCase (aa env e)
|
||||
|
||||
eEVAL x = LApp False (MN 0 "EVAL") [x]
|
||||
|
||||
fixApply tc n args ar
|
||||
| length args == ar = LApp tc n args
|
||||
| length args < ar = LApp tc (mkUnderCon n (ar - length args)) args
|
||||
| length args > ar = chainAPPLY (LApp tc n (take ar args)) (drop ar args)
|
||||
| length args == ar = LApp tc (LV (Glob n)) args
|
||||
| length args < ar = LApp tc (LV (Glob (mkUnderCon n (ar - length args)))) args
|
||||
| length args > ar = chainAPPLY (LApp tc (LV (Glob n)) (take ar args)) (drop ar args)
|
||||
|
||||
fixLazyApply n args ar
|
||||
| length args == ar = LApp False (mkFnCon n) args
|
||||
| length args < ar = LApp False (mkUnderCon n (ar - length args)) args
|
||||
| length args > ar = chainAPPLY (LApp False n (take ar args)) (drop ar args)
|
||||
| length args == ar = LApp False (LV (Glob (mkFnCon n))) args
|
||||
| length args < ar = LApp False (LV (Glob (mkUnderCon n (ar - length args)))) args
|
||||
| length args > ar = chainAPPLY (LApp False (LV (Glob n)) (take ar args)) (drop ar args)
|
||||
|
||||
chainAPPLY f [] = f
|
||||
chainAPPLY f (a : as) = chainAPPLY (LApp False (MN 0 "APPLY") [f, a]) as
|
||||
chainAPPLY f (a : as) = chainAPPLY (LApp False (LV (Glob (MN 0 "APPLY"))) [f, a]) as
|
||||
|
||||
eEVAL x = LApp False (LV (Glob (MN 0 "EVAL"))) [x]
|
||||
|
||||
data EvalApply a = EvalCase a
|
||||
| ApplyCase a
|
||||
@ -90,17 +92,17 @@ data EvalApply a = EvalCase a
|
||||
-- data constuctors, and whether to handle them in EVAL or APPLY
|
||||
|
||||
toCons :: (Name, Int) -> [(Name, Int, EvalApply LAlt)]
|
||||
toCons (n, i) = (mkFnCon n, i,
|
||||
EvalCase (LConCase (-1) (mkFnCon n) (take i (genArgs 0))
|
||||
(LApp False n (map (LV . Glob) (take i (genArgs 0))))))
|
||||
:
|
||||
mkApplyCase n 0 i
|
||||
toCons (n, i)
|
||||
= (mkFnCon n, i,
|
||||
EvalCase (LConCase (-1) (mkFnCon n) (take i (genArgs 0))
|
||||
(eEVAL (LApp False (LV (Glob n)) (map (LV . Glob) (take i (genArgs 0)))))))
|
||||
: mkApplyCase n 0 i
|
||||
|
||||
mkApplyCase fname n ar | n == ar = []
|
||||
mkApplyCase fname n ar
|
||||
= let nm = mkUnderCon fname (ar - n) in
|
||||
(nm, n, ApplyCase (LConCase (-1) nm (take n (genArgs 0))
|
||||
(LApp False (mkUnderCon fname (ar - (n + 1)))
|
||||
(LApp False (LV (Glob (mkUnderCon fname (ar - (n + 1)))))
|
||||
(map (LV . Glob) (take n (genArgs 0) ++
|
||||
[MN 0 "arg"])))))
|
||||
: mkApplyCase fname (n + 1) ar
|
||||
@ -116,7 +118,8 @@ mkEval xs = (MN 0 "EVAL", LFun (MN 0 "EVAL") [MN 0 "arg"]
|
||||
|
||||
mkApply :: [(Name, Int, EvalApply LAlt)] -> (Name, LDecl)
|
||||
mkApply xs = (MN 0 "APPLY", LFun (MN 0 "APPLY") [MN 0 "fn", MN 0 "arg"]
|
||||
(LCase (LApp False (MN 0 "EVAL") [LV (Glob (MN 0 "fn"))])
|
||||
(LCase (LApp False (LV (Glob (MN 0 "EVAL")))
|
||||
[LV (Glob (MN 0 "fn"))])
|
||||
(mapMaybe applyCase xs)))
|
||||
where
|
||||
applyCase (n, t, ApplyCase x) = Just x
|
||||
|
||||
@ -50,7 +50,7 @@ fovm f = do defs <- parseFOVM f
|
||||
let (nexttag, tagged) = addTags 0 (liftAll defs)
|
||||
let ctxtIn = addAlist tagged emptyContext
|
||||
let defuns = defunctionalise nexttag ctxtIn
|
||||
-- print defuns
|
||||
putStrLn $ showSep "\n" (map show (toAlist defuns))
|
||||
let checked = checkDefs defuns (toAlist defuns)
|
||||
-- print checked
|
||||
case checked of
|
||||
@ -135,7 +135,7 @@ pLExp' = try (do lchar '%'; pCast)
|
||||
then if lazy then return (LLazyApp x [])
|
||||
else return (LV (Glob x))
|
||||
else if lazy then return (LLazyApp x args)
|
||||
else return (LApp tc x args))
|
||||
else return (LApp tc (LV (Glob x)) args))
|
||||
<|> do lchar '('; e <- pLExp; lchar ')'; return e
|
||||
<|> pLConst
|
||||
<|> do reserved "let"; x <- iName []; lchar '='; v <- pLExp
|
||||
|
||||
@ -7,9 +7,10 @@ data LVar = Loc Int | Glob Name
|
||||
deriving Show
|
||||
|
||||
data LExp = LV LVar
|
||||
| LApp Bool Name [LExp] -- True = tail call
|
||||
| LApp Bool LExp [LExp] -- True = tail call
|
||||
| LLazyApp Name [LExp] -- True = tail call
|
||||
| LLazyExp LExp
|
||||
| LForce LExp -- make sure Exp is evaluted
|
||||
| LLet Name LExp LExp -- name just for pretty printing
|
||||
| LLam [Name] LExp -- lambda, lifted out before compiling
|
||||
| LCon Int Name [LExp]
|
||||
@ -17,6 +18,7 @@ data LExp = LV LVar
|
||||
| LConst Const
|
||||
| LForeign FLang FType String [(FType, LExp)]
|
||||
| LOp PrimFn [LExp]
|
||||
| LError String
|
||||
deriving Show
|
||||
|
||||
data 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
|
||||
| LFSqrt | LFFloor | LFCeil
|
||||
|
||||
| LStrHead | LStrTail | LStrCons | LStrIndex | LStrRev
|
||||
| LNoOp
|
||||
deriving Show
|
||||
|
||||
-- Supported target languages for foreign calls
|
||||
@ -85,8 +88,13 @@ addFn fn d = do LS n i ds <- get
|
||||
|
||||
lift :: [Name] -> LExp -> State LiftState LExp
|
||||
lift env (LV v) = return (LV v)
|
||||
lift env (LApp tc n args) = do args' <- mapM (lift env) args
|
||||
return (LApp tc n args')
|
||||
lift env (LApp tc (LV (Glob n)) args) = do args' <- mapM (lift env) args
|
||||
return (LApp tc (LV (Glob n)) args')
|
||||
lift env (LApp tc f args) = do f' <- lift env f
|
||||
fn <- getNextName
|
||||
addFn fn (LFun fn env f')
|
||||
args' <- mapM (lift env) args
|
||||
return (LApp tc (LV (Glob fn)) (map (LV . Glob) env ++ args'))
|
||||
lift env (LLazyApp n args) = do args' <- mapM (lift env) args
|
||||
return (LLazyApp n args')
|
||||
lift env (LLazyExp (LConst c)) = return (LConst c)
|
||||
@ -94,13 +102,15 @@ lift env (LLazyExp e) = do e' <- lift env e
|
||||
fn <- getNextName
|
||||
addFn fn (LFun fn env e')
|
||||
return (LLazyApp fn (map (LV . Glob) env))
|
||||
lift env (LForce e) = do e' <- lift env e
|
||||
return (LForce e')
|
||||
lift env (LLet n v e) = do v' <- lift env v
|
||||
e' <- lift (env ++ [n]) e
|
||||
return (LLet n v' e')
|
||||
lift env (LLam args e) = do e' <- lift (env ++ args) e
|
||||
fn <- getNextName
|
||||
addFn fn (LFun fn (env ++ args) e')
|
||||
return (LApp False fn (map (LV . Glob) env))
|
||||
return (LApp False (LV (Glob fn)) (map (LV . Glob) env))
|
||||
lift env (LCon i n args) = do args' <- mapM (lift env) args
|
||||
return (LCon i n args')
|
||||
lift 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
|
||||
return (t, e')
|
||||
lift env (LOp f args) = do args' <- mapM (lift env) args
|
||||
return (LOp f args')
|
||||
|
||||
lift env (LError str) = return $ LError str
|
||||
|
||||
|
||||
|
||||
|
||||
@ -16,6 +16,7 @@ data SExp = SV LVar
|
||||
| SConst Const
|
||||
| SForeign FLang FType String [(FType, LVar)]
|
||||
| SOp PrimFn [LVar]
|
||||
| SError String
|
||||
deriving Show
|
||||
|
||||
data SAlt = SConCase Int Int Name [Name] SExp
|
||||
@ -42,7 +43,8 @@ simplify tl (LV (Glob x))
|
||||
case lookupCtxt Nothing x ctxt of
|
||||
[LConstructor _ t 0] -> return $ SCon t x []
|
||||
_ -> return $ SV (Glob x)
|
||||
simplify tl (LApp tc n args) = do args' <- mapM sVar args
|
||||
simplify tl (LApp tc (LV (Glob n)) args)
|
||||
= do args' <- mapM sVar args
|
||||
mkapp (SApp (tl || tc) n) args'
|
||||
simplify tl (LForeign lang ty fn args)
|
||||
= do args' <- mapM sVar (map snd args)
|
||||
@ -62,6 +64,7 @@ simplify tl (LCase e alts) = do v <- sVar e
|
||||
simplify tl (LConst c) = return (SConst c)
|
||||
simplify tl (LOp p args) = do args' <- mapM sVar args
|
||||
mkapp (SOp p) args'
|
||||
simplify tl (LError str) = return $ SError str
|
||||
|
||||
sVar (LV (Glob x))
|
||||
= do ctxt <- ldefs
|
||||
@ -115,7 +118,8 @@ scopecheck ctxt env tm = sc env tm where
|
||||
Just i -> do lvar i; return (SV (Loc i))
|
||||
Nothing -> case lookupCtxt Nothing n ctxt of
|
||||
[LConstructor _ i ar] ->
|
||||
if ar == 0 then return (SCon i n [])
|
||||
if True -- ar == 0
|
||||
then return (SCon i n [])
|
||||
else fail $ "Codegen error: Constructor " ++ show n ++
|
||||
" has arity " ++ show ar
|
||||
[_] -> return (SV (Glob n))
|
||||
@ -124,7 +128,7 @@ scopecheck ctxt env tm = sc env tm where
|
||||
= do args' <- mapM (scVar env) args
|
||||
case lookupCtxt Nothing f ctxt of
|
||||
[LConstructor n tag ar] ->
|
||||
if (ar == length args)
|
||||
if True -- (ar == length args)
|
||||
then return $ SCon tag n args'
|
||||
else fail $ "Codegen error: Constructor " ++ show f ++
|
||||
" has arity " ++ show ar
|
||||
@ -138,7 +142,7 @@ scopecheck ctxt env tm = sc env tm where
|
||||
= do args' <- mapM (scVar env) args
|
||||
case lookupCtxt Nothing f ctxt of
|
||||
[LConstructor n tag ar] ->
|
||||
if (ar == length args)
|
||||
if True -- (ar == length args)
|
||||
then return $ SCon tag n args'
|
||||
else fail $ "Codegen error: Constructor " ++ show f ++
|
||||
" has arity " ++ show ar
|
||||
@ -172,7 +176,8 @@ scopecheck ctxt env tm = sc env tm where
|
||||
= do let env' = env ++ zip args [length env..]
|
||||
tag <- case lookupCtxt Nothing n ctxt of
|
||||
[LConstructor _ i ar] ->
|
||||
if (length args == ar) then return i
|
||||
if True -- (length args == ar)
|
||||
then return i
|
||||
else fail $ "Codegen error: Constructor " ++ show n ++
|
||||
" has arity " ++ show ar
|
||||
_ -> fail $ "Codegen error: No constructor " ++ show n
|
||||
|
||||
@ -7,7 +7,7 @@ import Core.TT
|
||||
import Core.Evaluate
|
||||
import Core.Elaborate hiding (Tactic(..))
|
||||
import Core.Typecheck
|
||||
import RTS.SC
|
||||
import IRTS.Lang
|
||||
import Util.Pretty
|
||||
|
||||
import Paths_idris
|
||||
@ -66,7 +66,7 @@ data IState = IState { tt_ctxt :: Context,
|
||||
syntax_keywords :: [String],
|
||||
imported :: [FilePath],
|
||||
idris_prims :: [(Name, ([E.Name], E.Term))],
|
||||
idris_scprims :: Prims,
|
||||
idris_scprims :: [(Name, (Int, PrimFn))],
|
||||
idris_objs :: [FilePath],
|
||||
idris_libs :: [String],
|
||||
idris_hdrs :: [String],
|
||||
|
||||
@ -6,7 +6,7 @@ import Idris.ElabDecls
|
||||
import Idris.ElabTerm
|
||||
import Idris.AbsSyntax
|
||||
|
||||
import RTS.SC
|
||||
import IRTS.Lang
|
||||
|
||||
import Core.TT
|
||||
import Core.Evaluate
|
||||
@ -19,7 +19,7 @@ data Prim = Prim { p_name :: Name,
|
||||
p_arity :: Int,
|
||||
p_def :: [Value] -> Maybe Value,
|
||||
p_epic :: ([E.Name], E.Term),
|
||||
p_sc :: ([CType], CType, SPrim),
|
||||
p_lexp :: (Int, PrimFn),
|
||||
p_total :: Totality
|
||||
}
|
||||
|
||||
@ -82,146 +82,146 @@ partial = Partial NotCovering
|
||||
primitives =
|
||||
-- operators
|
||||
[Prim (UN "prim__addInt") (ty [IType, IType] IType) 2 (iBin (+))
|
||||
(eOp E.plus_) ([sInt, sInt], sInt, AddI) total,
|
||||
(eOp E.plus_) (2, LPlus) total,
|
||||
Prim (UN "prim__subInt") (ty [IType, IType] IType) 2 (iBin (-))
|
||||
(eOp E.minus_)
|
||||
([sInt, sInt], sInt, SubI) total,
|
||||
(2, LMinus) total,
|
||||
Prim (UN "prim__mulInt") (ty [IType, IType] IType) 2 (iBin (*))
|
||||
(eOp E.times_) ([sInt, sInt], sInt, MulI) total,
|
||||
(eOp E.times_) (2, LTimes) total,
|
||||
Prim (UN "prim__divInt") (ty [IType, IType] IType) 2 (iBin (div))
|
||||
(eOp E.divide_) ([sInt, sInt], sInt, DivI) partial,
|
||||
(eOp E.divide_) (2, LDiv) partial,
|
||||
Prim (UN "prim__eqInt") (ty [IType, IType] IType) 2 (biBin (==))
|
||||
(eOp E.eq_) ([sInt, sInt], sInt, EqI) total,
|
||||
(eOp E.eq_) (2, LEq) total,
|
||||
Prim (UN "prim__ltInt") (ty [IType, IType] IType) 2 (biBin (<))
|
||||
(eOp E.lt_) ([sInt, sInt], sInt, LtI) total,
|
||||
(eOp E.lt_) (2, LLt) total,
|
||||
Prim (UN "prim__lteInt") (ty [IType, IType] IType) 2 (biBin (<=))
|
||||
(eOp E.lte_) ([sInt, sInt], sInt, LteI) total,
|
||||
(eOp E.lte_) (2, LLe) total,
|
||||
Prim (UN "prim__gtInt") (ty [IType, IType] IType) 2 (biBin (>))
|
||||
(eOp E.gt_) ([sInt, sInt], sInt, GtI) total,
|
||||
(eOp E.gt_) (2, LGt) total,
|
||||
Prim (UN "prim__gteInt") (ty [IType, IType] IType) 2 (biBin (>=))
|
||||
(eOp E.gte_) ([sInt, sInt], sInt, GteI) total,
|
||||
(eOp E.gte_) (2, LGe) total,
|
||||
Prim (UN "prim__eqChar") (ty [ChType, ChType] IType) 2 (bcBin (==))
|
||||
(eOp E.eq_) ([sChar, sChar], sInt, EqC) total,
|
||||
(eOp E.eq_) (2, LEq) total,
|
||||
Prim (UN "prim__ltChar") (ty [ChType, ChType] IType) 2 (bcBin (<))
|
||||
(eOp E.lt_) ([sChar, sChar], sInt, LtC) total,
|
||||
(eOp E.lt_) (2, LLt) total,
|
||||
Prim (UN "prim__lteChar") (ty [ChType, ChType] IType) 2 (bcBin (<=))
|
||||
(eOp E.lte_) ([sChar, sChar], sInt, LteC) total,
|
||||
(eOp E.lte_) (2, LLe) total,
|
||||
Prim (UN "prim__gtChar") (ty [ChType, ChType] IType) 2 (bcBin (>))
|
||||
(eOp E.gt_) ([sChar, sChar], sInt, GtC) total,
|
||||
(eOp E.gt_) (2, LGt) total,
|
||||
Prim (UN "prim__gteChar") (ty [ChType, ChType] IType) 2 (bcBin (>=))
|
||||
(eOp E.gte_) ([sChar, sChar], sInt, GteC) total,
|
||||
(eOp E.gte_) (2, LGe) total,
|
||||
Prim (UN "prim__addBigInt") (ty [BIType, BIType] BIType) 2 (bBin (+))
|
||||
(eOpFn tyBigInt tyBigInt "addBig")
|
||||
([sBigInt, sBigInt], sBigInt, AddBI) total,
|
||||
(2, LBPlus) total,
|
||||
Prim (UN "prim__subBigInt") (ty [BIType, BIType] BIType) 2 (bBin (-))
|
||||
(eOpFn tyBigInt tyBigInt "subBig") ([sBigInt, sBigInt], sBigInt, SubBI) total,
|
||||
(eOpFn tyBigInt tyBigInt "subBig") (2, LBMinus) total,
|
||||
Prim (UN "prim__mulBigInt") (ty [BIType, BIType] BIType) 2 (bBin (*))
|
||||
(eOpFn tyBigInt tyBigInt "mulBig") ([sBigInt, sBigInt], sBigInt, MulBI) total,
|
||||
(eOpFn tyBigInt tyBigInt "mulBig") (2, LBTimes) total,
|
||||
Prim (UN "prim__divBigInt") (ty [BIType, BIType] BIType) 2 (bBin (div))
|
||||
(eOpFn tyBigInt tyBigInt "divBig") ([sBigInt, sBigInt], sBigInt,DivBI) partial,
|
||||
(eOpFn tyBigInt tyBigInt "divBig") (2, LBDiv) partial,
|
||||
Prim (UN "prim__eqBigInt") (ty [BIType, BIType] IType) 2 (bbBin (==))
|
||||
(eOpFn tyBigInt tyInt "eqBig") ([sBigInt, sBigInt], sInt, EqBI) total,
|
||||
(eOpFn tyBigInt tyInt "eqBig") (2, LBEq) total,
|
||||
Prim (UN "prim__ltBigInt") (ty [BIType, BIType] IType) 2 (bbBin (<))
|
||||
(eOpFn tyBigInt tyInt "ltBig") ([sBigInt, sBigInt], sInt, LtBI) total,
|
||||
(eOpFn tyBigInt tyInt "ltBig") (2, LBLt) total,
|
||||
Prim (UN "prim__lteBigInt") (ty [BIType, BIType] IType) 2 (bbBin (<=))
|
||||
(eOpFn tyBigInt tyInt "leBig") ([sBigInt, sBigInt], sInt, LteBI) total,
|
||||
(eOpFn tyBigInt tyInt "leBig") (2, LBLe) total,
|
||||
Prim (UN "prim__gtBigInt") (ty [BIType, BIType] IType) 2 (bbBin (>))
|
||||
(eOpFn tyBigInt tyInt "gtBig") ([sBigInt, sBigInt], sInt, GtBI) total,
|
||||
(eOpFn tyBigInt tyInt "gtBig") (2, LBGt) total,
|
||||
Prim (UN "prim__gtBigInt") (ty [BIType, BIType] IType) 2 (bbBin (>=))
|
||||
(eOpFn tyBigInt tyInt "geBig") ([sBigInt, sBigInt], sInt, GteBI) total,
|
||||
(eOpFn tyBigInt tyInt "geBig") (2, LBGe) total,
|
||||
Prim (UN "prim__addFloat") (ty [FlType, FlType] FlType) 2 (fBin (+))
|
||||
(eOp E.plusF_) ([sFloat, sFloat], sFloat, AddF) total,
|
||||
(eOp E.plusF_) (2, LFPlus) total,
|
||||
Prim (UN "prim__subFloat") (ty [FlType, FlType] FlType) 2 (fBin (-))
|
||||
(eOp E.minusF_) ([sFloat, sFloat], sFloat, SubF) total,
|
||||
(eOp E.minusF_) (2, LFMinus) total,
|
||||
Prim (UN "prim__mulFloat") (ty [FlType, FlType] FlType) 2 (fBin (*))
|
||||
(eOp E.timesF_) ([sFloat, sFloat], sFloat, MulF) total,
|
||||
(eOp E.timesF_) (2, LFTimes) total,
|
||||
Prim (UN "prim__divFloat") (ty [FlType, FlType] FlType) 2 (fBin (/))
|
||||
(eOp E.divideF_) ([sFloat, sFloat], sFloat, DivF) total,
|
||||
(eOp E.divideF_) (2, LFDiv) total,
|
||||
Prim (UN "prim__eqFloat") (ty [FlType, FlType] IType) 2 (bfBin (==))
|
||||
(eOp E.eqF_) ([sFloat, sFloat], sInt, EqF) total,
|
||||
(eOp E.eqF_) (2, LFEq) total,
|
||||
Prim (UN "prim__ltFloat") (ty [FlType, FlType] IType) 2 (bfBin (<))
|
||||
(eOp E.ltF_) ([sFloat, sFloat], sInt, LtF) total,
|
||||
(eOp E.ltF_) (2, LFLt) total,
|
||||
Prim (UN "prim__lteFloat") (ty [FlType, FlType] IType) 2 (bfBin (<=))
|
||||
(eOp E.lteF_) ([sFloat, sFloat], sInt, LteF) total,
|
||||
(eOp E.lteF_) (2, LFLe) total,
|
||||
Prim (UN "prim__gtFloat") (ty [FlType, FlType] IType) 2 (bfBin (>))
|
||||
(eOp E.gtF_) ([sFloat, sFloat], sInt, GtF) total,
|
||||
(eOp E.gtF_) (2, LFGt) total,
|
||||
Prim (UN "prim__gteFloat") (ty [FlType, FlType] IType) 2 (bfBin (>=))
|
||||
(eOp E.gteF_) ([sFloat, sFloat], sInt, GteF) total,
|
||||
(eOp E.gteF_) (2, LFGe) total,
|
||||
Prim (UN "prim__concat") (ty [StrType, StrType] StrType) 2 (sBin (++))
|
||||
([E.name "x", E.name "y"], (fun "append") @@ fun "x" @@ fun "y")
|
||||
([sString, sString], sString, ConcatS) total,
|
||||
(2, LStrConcat) total,
|
||||
Prim (UN "prim__eqString") (ty [StrType, StrType] IType) 2 (bsBin (==))
|
||||
([E.name "x", E.name "y"], strEq (fun "x") (fun "y"))
|
||||
([sString, sString], sInt, EqS) total,
|
||||
(2, LStrEq) total,
|
||||
Prim (UN "prim__ltString") (ty [StrType, StrType] IType) 2 (bsBin (<))
|
||||
([E.name "x", E.name "y"], strLt (fun "x") (fun "y"))
|
||||
([sString, sString], sInt, LtS) total,
|
||||
(2, LStrLt) total,
|
||||
-- Conversions
|
||||
Prim (UN "prim__strToInt") (ty [StrType] IType) 1 (c_strToInt)
|
||||
([E.name "x"], strToInt (fun "x")) ([sString], sInt, StoI) total,
|
||||
([E.name "x"], strToInt (fun "x")) (1, LStrInt) total,
|
||||
Prim (UN "prim__intToStr") (ty [IType] StrType) 1 (c_intToStr)
|
||||
([E.name "x"], intToStr (fun "x")) ([sInt], sString, ItoS) total,
|
||||
([E.name "x"], intToStr (fun "x")) (1, LIntStr) total,
|
||||
Prim (UN "prim__charToInt") (ty [ChType] IType) 1 (c_charToInt)
|
||||
([E.name "x"], charToInt (fun "x")) ([sChar], sInt, CtoI) total,
|
||||
([E.name "x"], charToInt (fun "x")) (1, LNoOp) total,
|
||||
Prim (UN "prim__intToChar") (ty [IType] ChType) 1 (c_intToChar)
|
||||
([E.name "x"], intToChar (fun "x")) ([sInt], sChar, ItoC) total,
|
||||
([E.name "x"], intToChar (fun "x")) (1, LNoOp) total,
|
||||
Prim (UN "prim__intToBigInt") (ty [IType] BIType) 1 (c_intToBigInt)
|
||||
([E.name "x"], intToBigInt (fun "x")) ([sInt], sBigInt, ItoBI) total,
|
||||
([E.name "x"], intToBigInt (fun "x")) (1, LIntBig) total,
|
||||
Prim (UN "prim__bigIntToInt") (ty [BIType] IType) 1 (c_bigIntToInt)
|
||||
([E.name "x"], bigIntToInt (fun "x")) ([sBigInt], sInt, BItoI) total,
|
||||
([E.name "x"], bigIntToInt (fun "x")) (1, LBigInt) total,
|
||||
Prim (UN "prim__strToBigInt") (ty [StrType] BIType) 1 (c_strToBigInt)
|
||||
([E.name "x"], strToBigInt (fun "x")) ([sString], sBigInt, StoBI) total,
|
||||
([E.name "x"], strToBigInt (fun "x")) (1, LStrBig) total,
|
||||
Prim (UN "prim__bigIntToStr") (ty [BIType] StrType) 1 (c_bigIntToStr)
|
||||
([E.name "x"], bigIntToStr (fun "x")) ([sBigInt], sString, BItoS) total,
|
||||
([E.name "x"], bigIntToStr (fun "x")) (1, LBigStr) total,
|
||||
Prim (UN "prim__strToFloat") (ty [StrType] FlType) 1 (c_strToFloat)
|
||||
([E.name "x"], strToFloat (fun "x")) ([sString], sFloat, StoF) total,
|
||||
([E.name "x"], strToFloat (fun "x")) (1, LStrFloat) total,
|
||||
Prim (UN "prim__floatToStr") (ty [FlType] StrType) 1 (c_floatToStr)
|
||||
([E.name "x"], floatToStr (fun "x")) ([sFloat], sString, FtoS) total,
|
||||
([E.name "x"], floatToStr (fun "x")) (1, LFloatStr) total,
|
||||
Prim (UN "prim__intToFloat") (ty [IType] FlType) 1 (c_intToFloat)
|
||||
([E.name "x"], intToFloat (fun "x")) ([sInt], sFloat, ItoF) total,
|
||||
([E.name "x"], intToFloat (fun "x")) (1, LIntFloat) total,
|
||||
Prim (UN "prim__floatToInt") (ty [FlType] IType) 1 (c_floatToInt)
|
||||
([E.name "x"], floatToInt (fun "x")) ([sFloat], sInt, FtoI) total,
|
||||
([E.name "x"], floatToInt (fun "x")) (1, LFloatInt) total,
|
||||
|
||||
Prim (UN "prim__floatExp") (ty [FlType] FlType) 1 (p_floatExp)
|
||||
([E.name "x"], floatExp (fun "x")) ([sFloat], sFloat, ExpF) total,
|
||||
([E.name "x"], floatExp (fun "x")) (1, LFExp) total,
|
||||
Prim (UN "prim__floatLog") (ty [FlType] FlType) 1 (p_floatLog)
|
||||
([E.name "x"], floatLog (fun "x")) ([sFloat], sFloat, LogF) total,
|
||||
([E.name "x"], floatLog (fun "x")) (1, LFLog) total,
|
||||
Prim (UN "prim__floatSin") (ty [FlType] FlType) 1 (p_floatSin)
|
||||
([E.name "x"], floatSin (fun "x")) ([sFloat], sFloat, SinF) total,
|
||||
([E.name "x"], floatSin (fun "x")) (1, LFSin) total,
|
||||
Prim (UN "prim__floatCos") (ty [FlType] FlType) 1 (p_floatCos)
|
||||
([E.name "x"], floatCos (fun "x")) ([sFloat], sFloat, CosF) total,
|
||||
([E.name "x"], floatCos (fun "x")) (1, LFCos) total,
|
||||
Prim (UN "prim__floatTan") (ty [FlType] FlType) 1 (p_floatTan)
|
||||
([E.name "x"], floatTan (fun "x")) ([sFloat], sFloat, TanF) total,
|
||||
([E.name "x"], floatTan (fun "x")) (1, LFTan) total,
|
||||
Prim (UN "prim__floatASin") (ty [FlType] FlType) 1 (p_floatASin)
|
||||
([E.name "x"], floatASin (fun "x")) ([sFloat], sFloat, ASinF) total,
|
||||
([E.name "x"], floatASin (fun "x")) (1, LFASin) total,
|
||||
Prim (UN "prim__floatACos") (ty [FlType] FlType) 1 (p_floatACos)
|
||||
([E.name "x"], floatACos (fun "x")) ([sFloat], sFloat, ACosF) total,
|
||||
([E.name "x"], floatACos (fun "x")) (1, LFACos) total,
|
||||
Prim (UN "prim__floatATan") (ty [FlType] FlType) 1 (p_floatATan)
|
||||
([E.name "x"], floatATan (fun "x")) ([sFloat], sFloat, ATanF) total,
|
||||
([E.name "x"], floatATan (fun "x")) (1, LFATan) total,
|
||||
Prim (UN "prim__floatSqrt") (ty [FlType] FlType) 1 (p_floatSqrt)
|
||||
([E.name "x"], floatSqrt (fun "x")) ([sFloat], sFloat, SqrtF) total,
|
||||
([E.name "x"], floatSqrt (fun "x")) (1, LFSqrt) total,
|
||||
Prim (UN "prim__floatFloor") (ty [FlType] FlType) 1 (p_floatFloor)
|
||||
([E.name "x"], floatFloor (fun "x")) ([sFloat], sFloat, FloorF) total,
|
||||
([E.name "x"], floatFloor (fun "x")) (1, LFFloor) total,
|
||||
Prim (UN "prim__floatCeil") (ty [FlType] FlType) 1 (p_floatCeil)
|
||||
([E.name "x"], floatCeil (fun "x")) ([sFloat], sFloat, CeilF) total,
|
||||
([E.name "x"], floatCeil (fun "x")) (1, LFCeil) total,
|
||||
|
||||
Prim (UN "prim__strHead") (ty [StrType] ChType) 1 (p_strHead)
|
||||
([E.name "x"], strHead (fun "x")) ([sString], sChar, HeadS) partial,
|
||||
([E.name "x"], strHead (fun "x")) (1, LStrHead) partial,
|
||||
Prim (UN "prim__strTail") (ty [StrType] StrType) 1 (p_strTail)
|
||||
([E.name "x"], strTail (fun "x")) ([sString], sString, TailS) partial,
|
||||
([E.name "x"], strTail (fun "x")) (1, LStrTail) partial,
|
||||
Prim (UN "prim__strCons") (ty [ChType, StrType] StrType) 2 (p_strCons)
|
||||
([E.name "x", E.name "xs"], strCons (fun "x") (fun "xs"))
|
||||
([sChar, sString], sString, ConsS) total,
|
||||
(2, LStrCons) total,
|
||||
Prim (UN "prim__strIndex") (ty [StrType, IType] ChType) 2 (p_strIndex)
|
||||
([E.name "x", E.name "i"], strIndex (fun "x") (fun "i"))
|
||||
([sString, sInt], sChar, IndexS) partial,
|
||||
(2, LStrIndex) partial,
|
||||
Prim (UN "prim__strRev") (ty [StrType] StrType) 1 (p_strRev)
|
||||
([E.name "x"], strRev (fun "x"))
|
||||
([sString], sString, RevS) total,
|
||||
(1, LStrRev) total,
|
||||
|
||||
Prim (UN "prim__believe_me") believeTy 3 (p_believeMe)
|
||||
([E.name "a", E.name "b", E.name "x"], fun "x")
|
||||
([Nothing], Nothing, BelieveMe) total -- ahem
|
||||
(1, LNoOp) total -- ahem
|
||||
]
|
||||
|
||||
p_believeMe [_,_,x] = Just x
|
||||
|
||||
@ -20,10 +20,12 @@ import Core.ProofShell
|
||||
import Core.TT
|
||||
import Core.Constraints
|
||||
|
||||
import RTS.SC
|
||||
import RTS.Bytecode
|
||||
import RTS.PreC
|
||||
import RTS.CodegenC
|
||||
import IRTS.Compiler
|
||||
|
||||
-- import RTS.SC
|
||||
-- import RTS.Bytecode
|
||||
-- import RTS.PreC
|
||||
-- import RTS.CodegenC
|
||||
|
||||
import System.Console.Haskeline as H
|
||||
import System.FilePath
|
||||
@ -223,19 +225,6 @@ process fn (DebugInfo n)
|
||||
let d = lookupDef Nothing n (tt_ctxt i)
|
||||
when (not (null d)) $ liftIO $
|
||||
do print (head d)
|
||||
let prims = idris_scprims i
|
||||
let scs = toSC prims (n, head d)
|
||||
let bcs = bcdefs scs
|
||||
let pcs = preCdefs bcs
|
||||
let code = cdefs pcs
|
||||
putStrLn "Supercombinators:\n"
|
||||
print (toSC prims (n, head d))
|
||||
putStrLn "\nBytecode:\n"
|
||||
putStrLn (showSep "\n" (map show bcs))
|
||||
putStrLn "\nPre-C:\n"
|
||||
putStrLn (showSep "\n" (map show pcs))
|
||||
putStrLn "\nCode:\n"
|
||||
putStrLn code
|
||||
process fn (Info n) = do i <- get
|
||||
case lookupCtxt Nothing n (idris_classes i) of
|
||||
[c] -> classInfo c
|
||||
|
||||
Loading…
Reference in New Issue
Block a user