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

git.iko.soy/Idris-dev

:d to display elaborated pattern definition

commit42ca0639bdfeaee84b29867fbe0f7df82c533f26 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateTue 10 Jan 2012, 13:02 (15 years ago) parentbaaba44

3 files changed+14−3

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+2−1 src/Idris/ElabDecls.hs+2 src/Idris/REPL.hs+10−2

src/Idris/AbsSyntax.hs+2−1

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

4040 idris_statics :: Ctxt [Bool],

4141 idris_classes :: Ctxt ClassInfo,

4242 idris_optimisation :: Ctxt OptInfo,

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

4344 idris_log :: String,

4445 idris_options :: IOption,

4546 idris_name :: Int,

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

7980 deriving Show

8081

8182idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

82− emptyContext

83+ emptyContext emptyContext

8384 "" defaultOpts 6 [] [] [] [] [] [] [] []

8485 Nothing Nothing Nothing [] [] [] Hidden [] Nothing

8586

src/Idris/ElabDecls.hs+2

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

114114 logLvl 3 (show tree)

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

116116 ctxt <- getContext

117+ ist <- get

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

117119 case lookupTy (namespace info) n ctxt of

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

119121 tcase pdef pdef' ty)

src/Idris/REPL.hs+10−2

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

163163 case ucheck cs of

164164 Error e -> iputStrLn $ pshow i e

165165 OK _ -> iputStrLn "Universes OK"

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

167− liftIO $ print (lookupDef Nothing n ctxt)

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

167+ iputStrLn "Compiled patterns:\n"

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)

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

169177 let oi = lookupCtxt Nothing n (idris_optimisation i)

170178 liftIO $ print oi