14955ff · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge remote-tracking branch 'upstream/master'

14955ffDominic Mulligan15 years ago

CHANGELOG+2

compare with master

unifiedsplit

@@ -3,12 +3,14 @@ New in 0.9.2:

4User visible changes:

6+* backtick notation added: x `foo` y ==> foo x y

6* case expressions allowed in type signatures

7* case expressions allowed in type signatures

7* Library extensions in prelude.vect and prelude.algebra

8* Library extensions in prelude.vect and prelude.algebra

9Internal changes:

10Internal changes:

11* Some type class resolution fixes

12* Some type class resolution fixes

13+* Several minor bug fixes

13New in 0.9.1:

15New in 0.9.1:

14-------------

16-------------

lib/prelude.idr+8

@@ -158,11 +158,19 @@ count : Num a => a -> a -> a -> List a

158count a inc b = if a <= b then a :: count (a + inc) inc b

159 else []

160

161+countFrom : Num a => a -> a -> List a

162+countFrom a inc = a :: lazy (countFrom (a + inc) inc)

163+

161syntax "[" [start] ".." [end] "]"

164syntax "[" [start] ".." [end] "]"

162 = count start 1 end

165 = count start 1 end

163syntax "[" [start] "," [next] ".." [end] "]"

166syntax "[" [start] "," [next] ".." [end] "]"

164 = count start (next - start) end

167 = count start (next - start) end

165

168

169+syntax "[" [start] "..]"

170+ = countFrom start 1

171+syntax "[" [start] "," [next] "..]"

172+ = countFrom start (next - start)

173+

166---- More utilities

174---- More utilities

167

175

168sum : Num a => List a -> a

176sum : Num a => List a -> a

src/Core/Evaluate.hs+59−20

@@ -20,14 +20,29 @@ import Core.TT

20import Core.CaseTree

22data EvalState = ES { limited :: [(Name, Int)],

23− steps :: Int }

23+ steps :: Int -- number of applications/let reductions

24+ }

25+

26+-- Evaluation fails if we hit a boredom threshold - in which case, just return

27+-- the original (capture the failure in a Maybe)

28+

24−type Eval a = State EvalState a

29+type Eval a = StateT EvalState Maybe a

26data EvalOpt = Spec | HNF | Simplify | AtREPL

31data EvalOpt = Spec | HNF | Simplify | AtREPL

27 deriving (Show, Eq)

32 deriving (Show, Eq)

29initEval = ES [] 0

34initEval = ES [] 0

36+step :: Int -> Eval ()

37+step max = do e <- get

38+ put (e { steps = steps e + 1 })

39+ if steps e > max then fail "Threshold exceeded"

40+ else return ()

41+

42+getSteps :: Eval Int

43+getSteps = do e <- get

44+ return (steps e)

45+

31-- VALUES (as HOAS) ---------------------------------------------------------

46-- VALUES (as HOAS) ---------------------------------------------------------

33data Value = VP NameType Name Value

48data Value = VP NameType Name Value

@@ -49,7 +64,7 @@ data HNF = HP NameType Name (TT Name)

49 deriving Show

64 deriving Show

51instance Show Value where

66instance Show Value where

52− show x = show $ evalState (quote 100 x) initEval

67+ show x = show $ evalStateT (quote 100 x) initEval

54instance Show (a -> b) where

69instance Show (a -> b) where

55 show x = "<<fn>>"

70 show x = "<<fn>>"

@@ -61,38 +76,53 @@ instance Show (a -> b) where

61-- i.e. it's an intermediate environment that we have while type checking or

76-- i.e. it's an intermediate environment that we have while type checking or

62-- while building a proof.

77-- while building a proof.

79+threshold = 150000 -- boredom threshold for evaluation, to prevent infinite typechecking

80+

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

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

65normaliseC ctxt env t

82normaliseC ctxt env t

66− = evalState (do val <- eval ctxt [] env t []

83+ = case evalStateT (do val <- eval ctxt threshold [] env t []

67− quote 0 val) initEval

84+ quote 0 val) initEval of

85+ Just v -> v

86+ Nothing -> t

69normaliseAll :: Context -> Env -> TT Name -> TT Name

88normaliseAll :: Context -> Env -> TT Name -> TT Name

70normaliseAll ctxt env t

89normaliseAll ctxt env t

71− = evalState (do val <- eval ctxt [] env t [AtREPL]

90+ = case evalStateT (do val <- eval ctxt threshold [] env t [AtREPL]

72− quote 0 val) initEval

91+ quote 0 val) initEval of

92+ Just v -> v

93+ Nothing -> t

74normalise :: Context -> Env -> TT Name -> TT Name

95normalise :: Context -> Env -> TT Name -> TT Name

75normalise ctxt env t

96normalise ctxt env t

76− = evalState (do val <- eval ctxt [] (map finalEntry env) (finalise t) []

97+ = case evalStateT (do val <- eval ctxt threshold [] (map finalEntry env) (finalise t) []

77− quote 0 val) initEval

98+ quote 0 val) initEval of

99+ Just v -> v

100+ Nothing -> t

101

79specialise :: Context -> Env -> [(Name, Int)] -> TT Name -> TT Name

102specialise :: Context -> Env -> [(Name, Int)] -> TT Name -> TT Name

80specialise ctxt env limits t

103specialise ctxt env limits t

81− = evalState (do val <- eval ctxt limits (map finalEntry env) (finalise t) []

104+ = case evalStateT (do val <- eval ctxt threshold limits (map finalEntry env) (finalise t) []

82− quote 0 val) (initEval { limited = limits })

105+ quote 0 val) (initEval { limited = limits }) of

106+ Just v -> v

107+ Nothing -> t

108

84-- Like normalise, but we only reduce functions that are marked as okay to

109-- Like normalise, but we only reduce functions that are marked as okay to

85-- inline (and probably shouldn't reduce lets?)

110-- inline (and probably shouldn't reduce lets?)

111

87simplify :: Context -> Env -> TT Name -> TT Name

112simplify :: Context -> Env -> TT Name -> TT Name

88simplify ctxt env t

113simplify ctxt env t

114+ = case evalStateT (do val <- eval ctxt threshold []

89− = evalState (do val <- eval ctxt [] (map finalEntry env) (finalise t) [Simplify]

115+ (map finalEntry env) (finalise t) [Simplify]

90− quote 0 val) initEval

116+ quote 0 val) initEval of

117+ Just v -> v

118+ Nothing -> t

119

92hnf :: Context -> Env -> TT Name -> TT Name

120hnf :: Context -> Env -> TT Name -> TT Name

93hnf ctxt env t

121hnf ctxt env t

94− = evalState (do val <- eval ctxt [] (map finalEntry env) (finalise t) [HNF]

122+ = case evalStateT (do val <- eval ctxt threshold [] (map finalEntry env) (finalise t) [HNF]

95− quote 0 val) initEval

123+ quote 0 val) initEval of

124+ Just v -> v

125+ Nothing -> t

126

127

98-- unbindEnv env (quote 0 (eval ctxt (bindEnv env t)))

128-- unbindEnv env (quote 0 (eval ctxt (bindEnv env t)))

@@ -123,17 +153,19 @@ reduction = do ES ns s <- get

123-- Evaluate in a context of locally named things (i.e. not de Bruijn indexed,

153-- Evaluate in a context of locally named things (i.e. not de Bruijn indexed,

124-- such as we might have during construction of a proof)

154-- such as we might have during construction of a proof)

125

155

126−eval :: Context -> [(Name, Int)] -> Env -> TT Name -> [EvalOpt] -> Eval Value

156+eval :: Context -> Int -> [(Name, Int)] -> Env -> TT Name -> [EvalOpt] -> Eval Value

127−eval ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

157+eval ctxt maxred ntimes genv tm opts = ev ntimes [] True [] tm where

128 spec = Spec `elem` opts

158 spec = Spec `elem` opts

129 simpl = Simplify `elem` opts

159 simpl = Simplify `elem` opts

130 atRepl = AtREPL `elem` opts

160 atRepl = AtREPL `elem` opts

131

161

132 ev ntimes stk top env (P _ n ty)

162 ev ntimes stk top env (P _ n ty)

163+ | Just (Let t v) <- lookup n genv = do step maxred

133− | Just (Let t v) <- lookup n genv = ev ntimes stk top env v

164+ ev ntimes stk top env v

134 ev ntimes_in stk top env (P Ref n ty)

165 ev ntimes_in stk top env (P Ref n ty)

135 | (True, ntimes) <- usable n ntimes_in

166 | (True, ntimes) <- usable n ntimes_in

136 = do let val = lookupDefAcc Nothing n atRepl ctxt

167 = do let val = lookupDefAcc Nothing n atRepl ctxt

168+ step maxred

137 case val of

169 case val of

138 [(Function _ tm, Public)] ->

170 [(Function _ tm, Public)] ->

139 ev ntimes (n:stk) True env tm

171 ev ntimes (n:stk) True env tm

@@ -152,20 +184,24 @@ eval ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

152 | otherwise = return $ VV i

184 | otherwise = return $ VV i

153 ev ntimes stk top env (Bind n (Let t v) sc)

185 ev ntimes stk top env (Bind n (Let t v) sc)

154 = do v' <- ev ntimes stk top env v --(finalise v)

186 = do v' <- ev ntimes stk top env v --(finalise v)

187+ step maxred

155 sc' <- ev ntimes stk top (v' : env) sc

188 sc' <- ev ntimes stk top (v' : env) sc

156 wknV (-1) sc'

189 wknV (-1) sc'

157 ev ntimes stk top env (Bind n (NLet t v) sc)

190 ev ntimes stk top env (Bind n (NLet t v) sc)

158 = do t' <- ev ntimes stk top env (finalise t)

191 = do t' <- ev ntimes stk top env (finalise t)

159 v' <- ev ntimes stk top env (finalise v)

192 v' <- ev ntimes stk top env (finalise v)

193+ step maxred

160 sc' <- ev ntimes stk top (v' : env) sc

194 sc' <- ev ntimes stk top (v' : env) sc

161 return $ VBind n (Let t' v') (\x -> return sc')

195 return $ VBind n (Let t' v') (\x -> return sc')

162 ev ntimes stk top env (Bind n b sc)

196 ev ntimes stk top env (Bind n b sc)

163 = do b' <- vbind env b

197 = do b' <- vbind env b

198+ step maxred

164 return $ VBind n b' (\x -> ev ntimes stk top (x:env) sc)

199 return $ VBind n b' (\x -> ev ntimes stk top (x:env) sc)

165 where vbind env t = fmapMB (\tm -> ev ntimes stk top env (finalise tm)) t

200 where vbind env t = fmapMB (\tm -> ev ntimes stk top env (finalise tm)) t

166 ev ntimes stk top env (App f a)

201 ev ntimes stk top env (App f a)

167 = do f' <- ev ntimes stk top env f

202 = do f' <- ev ntimes stk top env f

168 a' <- ev ntimes stk False env a

203 a' <- ev ntimes stk False env a

204+ step maxred

169 evApply ntimes stk top env [a'] f'

205 evApply ntimes stk top env [a'] f'

170 ev ntimes stk top env (Constant c) = return $ VConstant c

206 ev ntimes stk top env (Constant c) = return $ VConstant c

171 ev ntimes stk top env Erased = return VErased

207 ev ntimes stk top env Erased = return VErased

@@ -173,7 +209,8 @@ eval ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

173

209

174 evApply ntimes stk top env args (VApp f a) =

210 evApply ntimes stk top env args (VApp f a) =

175 evApply ntimes stk top env (a:args) f

211 evApply ntimes stk top env (a:args) f

212+ evApply ntimes stk top env args f = do step maxred

176− evApply ntimes stk top env args f = apply ntimes stk top env f args

213+ apply ntimes stk top env f args

177

214

178 apply ntimes stk top env (VBind n (Lam t) sc) (a:as)

215 apply ntimes stk top env (VBind n (Lam t) sc) (a:as)

179 = do a' <- sc a

216 = do a' <- sc a

@@ -595,7 +632,9 @@ initContext = MkContext [] 0 emptyContext

595ctxtAlist :: Context -> [(Name, Def)]

632ctxtAlist :: Context -> [(Name, Def)]

596ctxtAlist ctxt = map (\(n, (d, a, t)) -> (n, d)) $ toAlist (definitions ctxt)

633ctxtAlist ctxt = map (\(n, (d, a, t)) -> (n, d)) $ toAlist (definitions ctxt)

597

634

598−veval ctxt env t = evalState (eval ctxt [] env t []) initEval

635+veval ctxt env t = case evalStateT (eval ctxt threshold [] env t []) initEval of

636+ Just v -> v

637+ Nothing -> error "Evaluation failed"

599

638

600addToCtxt :: Name -> Term -> Type -> Context -> Context

639addToCtxt :: Name -> Term -> Type -> Context -> Context

601addToCtxt n tm ty uctxt

640addToCtxt n tm ty uctxt

src/Idris/AbsSyntax.hs+2

@@ -1401,6 +1401,8 @@ matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where

1401 | PConstant (I _) <- getTm x = match (getTm x) x'

1402 match x' (PApp _ (PRef _ (NS (UN "fromInteger") ["builtins"])) [_,_,x])

1403 | PConstant (I _) <- getTm x = match (getTm x) x'

1404+ match (PApp _ (PRef _ (UN "lazy")) [_,x]) x' = match (getTm x) x'

1405+ match x (PApp _ (PRef _ (UN "lazy")) [_,x']) = match x (getTm x')

1404 match (PApp _ f args) (PApp _ f' args')

1406 match (PApp _ f args) (PApp _ f' args')

1405 | length args == length args'

1407 | length args == length args'

1406 = do mf <- match' f f'

1408 = do mf <- match' f f'

src/Idris/Parser.hs+14−9

@@ -141,22 +141,23 @@ parseTac i = runParser (do t <- pTactic defaultSyntax

141parseImports :: FilePath -> String -> Idris ([String], [String], String, SourcePos)

142parseImports fname input

143 = do i <- get

144+ case (runParser (do whiteSpace

144− case (runParser (do mname <- pHeader

145+ mname <- pHeader

145 ps <- many pImport

146 ps <- many pImport

146 rest <- getInput

147 rest <- getInput

147 pos <- getPosition

148 pos <- getPosition

148 return ((mname, ps, rest, pos), i)) i fname input) of

149 return ((mname, ps, rest, pos), i)) i fname input) of

149− Left err -> fail (ishow err)

150+ Left err -> fail (show err)

150 Right (x, i) -> do put i

151 Right (x, i) -> do put i

151 return x

152 return x

152 where ishow err = let ln = sourceLine (errorPos err) in

153 where ishow err = let ln = sourceLine (errorPos err) in

153 fname ++ ":" ++ show ln ++ ":parse error"

154 fname ++ ":" ++ show ln ++ ":parse error"

154−-- show (map messageString (errorMessages err))

155+-- ++ show (map messageString (errorMessages err))

155

156

156pHeader :: IParser [String]

157pHeader :: IParser [String]

157pHeader = try (do reserved "module"; i <- identifier; option ';' (lchar ';')

158pHeader = try (do reserved "module"; i <- identifier; option ';' (lchar ';')

158 return (parseName i))

159 return (parseName i))

159− <|> return []

160+ <|> return []

160 where parseName x = case span (/='.') x of

161 where parseName x = case span (/='.') x of

161 (x, "") -> [x]

162 (x, "") -> [x]

162 (x, '.':y) -> x : parseName y

163 (x, '.':y) -> x : parseName y

@@ -940,7 +941,8 @@ table fixes

940 = [[prefix "-" (\fc x -> PApp fc (PRef fc (UN "-"))

941 = [[prefix "-" (\fc x -> PApp fc (PRef fc (UN "-"))

941 [pexp (PApp fc (PRef fc (UN "fromInteger")) [pexp (PConstant (I 0))]), pexp x])]]

942 [pexp (PApp fc (PRef fc (UN "fromInteger")) [pexp (PConstant (I 0))]), pexp x])]]

942 ++ toTable (reverse fixes) ++

943 ++ toTable (reverse fixes) ++

944+ [[backtick],

943− [[binary "=" (\fc x y -> PEq fc x y) AssocLeft],

945+ [binary "=" (\fc x y -> PEq fc x y) AssocLeft],

944 [binary "->" (\fc x y -> PPi expl (MN 42 "__pi_arg") x y) AssocRight]]

946 [binary "->" (\fc x y -> PPi expl (MN 42 "__pi_arg") x y) AssocRight]]

945

947

946toTable fs = map (map toBin)

948toTable fs = map (map toBin)

@@ -953,10 +955,13 @@ toTable fs = map (map toBin)

953 assoc (Infixr _) = AssocRight

955 assoc (Infixr _) = AssocRight

954 assoc (InfixN _) = AssocNone

956 assoc (InfixN _) = AssocNone

955

957

956−binary name f assoc = Infix (do { reservedOp name; fc <- pfc;

958+binary name f assoc = Infix (do reservedOp name; fc <- pfc;

957− return (f fc) }) assoc

959+ return (f fc)) assoc

958−prefix name f = Prefix (do { reservedOp name; fc <- pfc;

960+prefix name f = Prefix (do reservedOp name; fc <- pfc;

959− return (f fc) })

961+ return (f fc))

962+backtick = Infix (do lchar '`'; n <- pfName; lchar '`'

963+ fc <- pfc

964+ return (\x y -> PApp fc (PRef fc n) [pexp x, pexp y])) AssocNone

960

965

961--------- Data declarations ---------

966--------- Data declarations ---------

962

967