dca8f9f · Idris-dev · git.iko.soy

src/Core/Evaluate.hs+1

compare with master

unifiedsplit

@@ -80,6 +80,7 @@ instance Show (a -> b) where

80threshold = 1000 -- boredom threshold for evaluation, to prevent infinite typechecking

81 -- in fact it's a maximum recursion depth

82

83+-- Normalise fully type checked terms (so, assume all names/let bindings resolved)

83normaliseC :: Context -> Env -> TT Name -> TT Name

84normaliseC :: Context -> Env -> TT Name -> TT Name

84normaliseC ctxt env t

85normaliseC ctxt env t

85 = evalState (do val <- eval ctxt threshold [] env t []

86 = evalState (do val <- eval ctxt threshold [] env t []

src/Idris/ElabDecls.hs+6−5

@@ -207,11 +207,12 @@ elabCon info syn tn (n, t_in, fc)

207 mapM_ (elabCaseBlock info) is

208 ctxt <- getContext

209 (cty, _) <- recheckC fc [] t'

210+ let cty' = normaliseC ctxt [] cty

210− tyIs cty

211+ tyIs cty'

211− logLvl 2 $ "---> " ++ show n ++ " : " ++ show cty

212+ logLvl 2 $ "---> " ++ show n ++ " : " ++ show cty'

212 addIBC (IBCDef n)

213 addIBC (IBCDef n)

213− forceArgs n cty

214+ forceArgs n cty'

214− return (n, cty)

215+ return (n, cty')

215 where

216 where

216 tyIs (Bind n b sc) = tyIs sc

217 tyIs (Bind n b sc) = tyIs sc

217 tyIs t | (P _ n' _, _) <- unApply t

218 tyIs t | (P _ n' _, _) <- unApply t

@@ -801,6 +802,7 @@ decorateid decorate (PClauses f o n cs)

801 dappname (PApp fc (PRef fc' n) as) = PApp fc (PRef fc' (decorate n)) as

802 dappname (PApp fc (PRef fc' n) as) = PApp fc (PRef fc' (decorate n)) as

802 dappname t = t

803 dappname t = t

803

804

805+

804pbinds (Bind n (PVar t) sc) = do attack; patbind n

806pbinds (Bind n (PVar t) sc) = do attack; patbind n

805 pbinds sc

807 pbinds sc

806pbinds tm = return ()

808pbinds tm = return ()

@@ -862,7 +864,6 @@ elabDecl' info (PDSL n dsl)

862 = do i <- get

864 = do i <- get

863 put (i { idris_dsls = addDef n dsl (idris_dsls i) })

865 put (i { idris_dsls = addDef n dsl (idris_dsls i) })

864 addIBC (IBCDSL n)

866 addIBC (IBCDSL n)

865−

866elabDecl' info (PDirective i) = i

867elabDecl' info (PDirective i) = i

867

868

868elabCaseBlock info d@(PClauses f o n ps)

869elabCaseBlock info d@(PClauses f o n ps)

src/Idris/Parser.hs+2−2

@@ -1261,8 +1261,8 @@ pDirective = try (do lchar '%'; reserved "lib"; lib <- strlit;

1261 <|> try (do lchar '%'; reserved "access"; acc <- pAccessibility'

1262 return [PDirective (do i <- getIState

1263 putIState (i { default_access = acc }))])

1264− <|> do lchar '%'; reserved "logging"; i <- natural;

1264+ <|> try (do lchar '%'; reserved "logging"; i <- natural;

1265− return [PDirective (setLogLevel (fromInteger i))]

1265+ return [PDirective (setLogLevel (fromInteger i))])

1266

1267pTactic :: SyntaxInfo -> IParser PTactic

1268pTactic syn = do reserved "intro"; ns <- sepBy pName (lchar ',')

src/Idris/REPL.hs+1−1

@@ -188,7 +188,7 @@ process fn (TotCheck n) = do i <- get

188 [t] -> iputStrLn (showTotal t i)

189 _ -> return ()

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

191− let oi = lookupCtxt Nothing n (idris_optimisation i)

191+ let oi = lookupCtxtName Nothing n (idris_optimisation i)

192 when (not (null oi)) $ iputStrLn (show oi)

193 let si = lookupCtxt Nothing n (idris_statics i)

194 when (not (null si)) $ iputStrLn (show si)