dca8f9f · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Normalise types before applying forcing

commitdca8f9fb445b01d9647f18442f5a92e5f0c7fb69 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateThu 1 Mar 2012, 10:49 (15 years ago) parenta94fd81

4 files changed+10−8

compare with master

unifiedsplit

src/Core/Evaluate.hs+1 src/Idris/ElabDecls.hs+6−5 src/Idris/Parser.hs+2−2 src/Idris/REPL.hs+1−1

src/Core/Evaluate.hs+1

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

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

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

8282

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

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

8485normaliseC ctxt env t

8586 = 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)

207207 mapM_ (elabCaseBlock info) is

208208 ctxt <- getContext

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

210− tyIs cty

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

210+ let cty' = normaliseC ctxt [] cty

211+ tyIs cty'

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

212213 addIBC (IBCDef n)

213− forceArgs n cty

214− return (n, cty)

214+ forceArgs n cty'

215+ return (n, cty')

215216 where

216217 tyIs (Bind n b sc) = tyIs sc

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

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

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

802803 dappname t = t

803804

805+

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

805807 pbinds sc

806808pbinds tm = return ()

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

862864 = do i <- get

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

864866 addIBC (IBCDSL n)

865−

866867elabDecl' info (PDirective i) = i

867868

868869elabCaseBlock 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;

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

12621262 return [PDirective (do i <- getIState

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

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

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

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

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

12661266

12671267pTactic :: SyntaxInfo -> IParser PTactic

12681268pTactic 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

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

189189 _ -> return ()

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

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

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

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

193193 let si = lookupCtxt Nothing n (idris_statics i)

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