git.iko.soy/Idris-dev
on master help sign in
New lambda lifter, and debug info in repl
541faf5Edwin Brady
src/Idris/REPL.hs+6
compare with master
unifiedsplit
@@ -20,6 +20,8 @@ import Core.ProofShell
20import Core.TT
20import Core.TT
21import Core.Constraints
21import Core.Constraints
22
22
23+import RTS.SC
24+
23import System.Console.Haskeline as H
25import System.Console.Haskeline as H
24import System.FilePath
26import System.FilePath
25import System.Environment
27import System.Environment
@@ -193,6 +195,10 @@ process fn (DebugInfo n)
193 when (not (null oi)) $ iputStrLn (show oi)
195 when (not (null oi)) $ iputStrLn (show oi)
194 let si = lookupCtxt Nothing n (idris_statics i)
196 let si = lookupCtxt Nothing n (idris_statics i)
195 when (not (null si)) $ iputStrLn (show si)
197 when (not (null si)) $ iputStrLn (show si)
198+ let d = lookupDef Nothing n (tt_ctxt i)
199+ when (not (null d)) $ liftIO $
200+ do print (head d)
201+ print (sclift (n, head d))
196process fn (Info n) = do i <- get
202process fn (Info n) = do i <- get
197 case lookupCtxt Nothing n (idris_classes i) of
203 case lookupCtxt Nothing n (idris_classes i) of
198 [c] -> classInfo c
204 [c] -> classInfo c
src/RTS/SC.hs+75−14
@@ -14,13 +14,14 @@ data SCDef = SCDef { sc_args :: [(Name, CType)],
14 sc_def :: SCExp }
14 sc_def :: SCExp }
15 deriving Show
15 deriving Show
16
16
17−data SCExp = SVar Name
17+data SCExp = SRef Name
18− | SApp Name [SCExp]
18+ | SApp SCExp [SCExp]
19+ | SLet Name SCExp SCExp
19 | SFCall String CType [(SCExp, CType)]
20 | SFCall String CType [(SCExp, CType)]
20 | SCon Tag [SCExp]
21 | SCon Tag [SCExp]
21 | SConst Const
22 | SConst Const
22− | SErased
23+ | SError String
23− | SCase [SAlt]
24+ | SCase Name [SAlt]
24 deriving Show
25 deriving Show
25
26
26data SAlt = SConCase Tag [Name] SCExp
27data SAlt = SConCase Tag [Name] SCExp
@@ -28,20 +29,80 @@ data SAlt = SConCase Tag [Name] SCExp
28 | SDefaultCase SCExp
29 | SDefaultCase SCExp
29 deriving Show
30 deriving Show
30
31
32+type SCState = ([(Name, SCDef)], Name)
33+
31sclift :: (Name, Def) -> [(Name, SCDef)]
34sclift :: (Name, Def) -> [(Name, SCDef)]
32−sclift d = execState (sc d) []
35+sclift (n, d) = fst (execState (sc [] d) ([], n))
36+
37+add x = do (xs, b) <- get
38+ put (x : xs, b)
39+
40+nextSC :: State SCState Name
41+nextSC = do (xs, n) <- get
42+ let n' = getNext n
43+ put (xs, n')
44+ return n'
45+ where getNext (UN n) = MN 0 n
46+ getNext (MN i n) = MN (i+1) n
47+ getNext (NS n ns) = NS (getNext n) ns
33
48
34−add :: a -> State [a] ()
49+sname :: State SCState Name
35−add x = do xs <- get
50+sname = do (xs, n) <- get
36− put (x : xs)
51+ return n
37
52
38class Lift s t | s -> t where
53class Lift s t | s -> t where
39− sc :: s -> State [(Name, SCDef)] t
54+ sc :: [Name] -> s -> State SCState t
55+
56+instance Lift Def () where
57+ sc env (Function ty tm) = do n <- sname
58+ tm' <- sc env tm
59+ add (n, SCDef (zip env (repeat Nothing)) tm')
60+ sc env (TyDecl _ _) = do n <- sname
61+ add (n, SCDef (zip env (repeat Nothing))
62+ (SError $ "undefined " ++ show n))
63+ sc env (Operator _ _ _) = return ()
64+ sc env (CaseOp _ _ _ _ _ args cases)
65+ = do n <- sname
66+ cases' <- sc (env ++ args) cases
67+ add (n, SCDef (zip (env ++ args) (repeat Nothing)) cases')
68+
69+instance Lift (TT Name) SCExp where
70+ sc env (P _ n _) = return $ SRef n
71+ sc env (V i) = return $ SRef (env!!i)
72+ sc env fn@(App _ _)
73+ = do let (f, args) = unApply fn
74+ args' <- mapM (sc env) args
75+ case f of
76+ (P (DCon t a) _ _) -> return $ SCon t args'
77+ (P (TCon t a) _ _) -> return $ SCon t args'
78+ _ -> do f' <- sc env f
79+ return $ SApp f' args'
80+ sc env (Constant c) = return $ SConst c
81+ sc env (Bind n (Let _ v) e) = do v' <- sc env v
82+ e' <- sc (n : env) e
83+ return (SLet n v' e')
84+ sc env (Bind n (Lam _) e) = scLam [n] e
85+ where
86+ scLam args (Bind n (Lam _) e) = scLam (n : args) e
87+ scLam args x = do x' <- sc (args ++ env) x
88+ fn <- nextSC
89+ add (fn, SCDef (zip (env ++ reverse args) (repeat Nothing)) x')
90+ return $ SApp (SRef fn) (map SRef env)
91+ sc _ _ = return $ SConst (I 42424242)
92+
40
93
41−instance Lift (Name, Def) () where
94+instance Lift SC SCExp where
42− sc (n, d) = do d' <- sc d
95+ sc env (Case n alts) = do alts' <- mapM (sc env) alts
43− add (n, d')
96+ return (SCase n alts')
97+ sc env (STerm t) = do t' <- sc env t
98+ return t'
99+ sc env (UnmatchedCase s) = return (SError s)
44
100
45−instance Lift Def SCDef where
101+instance Lift CaseAlt SAlt where
46− sc x = undefined
102+ sc env (ConCase n t args e) = do e' <- sc env e
103+ return (SConCase t args e')
104+ sc env (ConstCase c e) = do e' <- sc env e
105+ return (SConstCase c e')
106+ sc env (DefaultCase e) = do e' <- sc env e
107+ return (SDefaultCase e')
47
108