42ca063 · Idris-dev · git.iko.soy

src/Idris/AbsSyntax.hs+2−1

compare with master

unifiedsplit

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

40 idris_statics :: Ctxt [Bool],

41 idris_classes :: Ctxt ClassInfo,

42 idris_optimisation :: Ctxt OptInfo,

43+ idris_patdefs :: Ctxt [(Term, Term)], -- not exported

43 idris_log :: String,

44 idris_log :: String,

44 idris_options :: IOption,

45 idris_options :: IOption,

45 idris_name :: Int,

46 idris_name :: Int,

@@ -79,7 +80,7 @@ data IBCWrite = IBCFix FixDecl

79 deriving Show

80 deriving Show

80

81

81idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

82idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

82− emptyContext

83+ emptyContext emptyContext

83 "" defaultOpts 6 [] [] [] [] [] [] [] []

84 "" defaultOpts 6 [] [] [] [] [] [] [] []

84 Nothing Nothing Nothing [] [] [] Hidden [] Nothing

85 Nothing Nothing Nothing [] [] [] Hidden [] Nothing

85

86

src/Idris/ElabDecls.hs+2

@@ -114,6 +114,8 @@ elabClauses info fc opts n_in cs_in = let n = liftname info n_in in

114 logLvl 3 (show tree)

115 logLvl 3 $ "Optimised: " ++ show tree'

116 ctxt <- getContext

117+ ist <- get

118+ put (ist { idris_patdefs = addDef n pdef' (idris_patdefs ist) })

117 case lookupTy (namespace info) n ctxt of

119 case lookupTy (namespace info) n ctxt of

118 [ty] -> do updateContext (addCasedef n (inlinable opts)

120 [ty] -> do updateContext (addCasedef n (inlinable opts)

119 tcase pdef pdef' ty)

121 tcase pdef pdef' ty)

src/Idris/REPL.hs+10−2

@@ -163,8 +163,16 @@ process Universes = do i <- get

163 case ucheck cs of

164 Error e -> iputStrLn $ pshow i e

165 OK _ -> iputStrLn "Universes OK"

166−process (Defn n) = do ctxt <- getContext

166+process (Defn n) = do i <- get

167+ iputStrLn "Compiled patterns:\n"

167− liftIO $ print (lookupDef Nothing n ctxt)

168+ liftIO $ print (lookupDef Nothing n (tt_ctxt i))

169+ case lookupCtxt Nothing n (idris_patdefs i) of

170+ [] -> return ()

171+ [d] -> do iputStrLn "Original definiton:\n"

172+ mapM_ (printCase i) d

173+ where printCase i (lhs, rhs) = do liftIO $ putStr $ showImp True (delab i lhs)

174+ liftIO $ putStr " = "

175+ liftIO $ putStrLn $ showImp True (delab i rhs)

168process (Info n) = do i <- get

176process (Info n) = do i <- get

169 let oi = lookupCtxt Nothing n (idris_optimisation i)

177 let oi = lookupCtxt Nothing n (idris_optimisation i)

170 liftIO $ print oi

178 liftIO $ print oi