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

git.iko.soy/Idris-dev

Merge remote-tracking branch 'upstream/master'

commit14955ff8c50009c4564b1101c144bbf183720572 authorDominic Mulligan <dominic.p.mulligan@googlemail.com> dateThu 23 Feb 2012, 20:59 (15 years ago) parent8c29ac4 1c2098a

5 files changed+85−29

compare with master

unifiedsplit

CHANGELOG+2 lib/prelude.idr+8 src/Core/Evaluate.hs+59−20 src/Idris/AbsSyntax.hs+2 src/Idris/Parser.hs+14−9

CHANGELOG+2

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

44User visible changes:

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

67* case expressions allowed in type signatures

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

910Internal changes:

1011

1112* Some type class resolution fixes

13+* Several minor bug fixes

1214

1315New in 0.9.1:

1416-------------

lib/prelude.idr+8

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

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

159159 else []

160160

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

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

163+

161164syntax "[" [start] ".." [end] "]"

162165 = count start 1 end

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

164167 = count start (next - start) end

165168

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

170+ = countFrom start 1

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

172+ = countFrom start (next - start)

173+

166174---- More utilities

167175

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

src/Core/Evaluate.hs+59−20

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

2020import Core.CaseTree

2121

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

23− steps :: Int }

24−type Eval a = State EvalState a

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+

29+type Eval a = StateT EvalState Maybe a

2530

2631data EvalOpt = Spec | HNF | Simplify | AtREPL

2732 deriving (Show, Eq)

2833

2934initEval = ES [] 0

3035

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+

3146-- VALUES (as HOAS) ---------------------------------------------------------

3247

3348data Value = VP NameType Name Value

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

4964 deriving Show

5065

5166instance Show Value where

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

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

5368

5469instance Show (a -> b) where

5570 show x = "<<fn>>"

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

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

6277-- while building a proof.

6378

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

80+

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

6582normaliseC ctxt env t

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

67− quote 0 val) initEval

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

84+ quote 0 val) initEval of

85+ Just v -> v

86+ Nothing -> t

6887

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

7089normaliseAll ctxt env t

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

72− quote 0 val) initEval

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

91+ quote 0 val) initEval of

92+ Just v -> v

93+ Nothing -> t

7394

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

7596normalise ctxt env t

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

77− quote 0 val) initEval

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

98+ quote 0 val) initEval of

99+ Just v -> v

100+ Nothing -> t

78101

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

80103specialise ctxt env limits t

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

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

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

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

106+ Just v -> v

107+ Nothing -> t

83108

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

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

86111

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

88113simplify ctxt env t

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

90− quote 0 val) initEval

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

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

116+ quote 0 val) initEval of

117+ Just v -> v

118+ Nothing -> t

91119

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

93121hnf ctxt env t

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

95− quote 0 val) initEval

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

123+ quote 0 val) initEval of

124+ Just v -> v

125+ Nothing -> t

96126

97127

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

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

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

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

125155

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

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

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

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

128158 spec = Spec `elem` opts

129159 simpl = Simplify `elem` opts

130160 atRepl = AtREPL `elem` opts

131161

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

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

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

164+ ev ntimes stk top env v

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

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

136167 = do let val = lookupDefAcc Nothing n atRepl ctxt

168+ step maxred

137169 case val of

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

139171 ev ntimes (n:stk) True env tm

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

152184 | otherwise = return $ VV i

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

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

187+ step maxred

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

156189 wknV (-1) sc'

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

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

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

193+ step maxred

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

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

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

163197 = do b' <- vbind env b

198+ step maxred

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

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

166201 ev ntimes stk top env (App f a)

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

168203 a' <- ev ntimes stk False env a

204+ step maxred

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

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

171207 ev ntimes stk top env Erased = return VErased

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

173209

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

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

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

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

213+ apply ntimes stk top env f args

177214

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

179216 = do a' <- sc a

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

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

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

597634

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"

599638

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

601640addToCtxt 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

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

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

14031403 | 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')

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

14051407 | length args == length args'

14061408 = do mf <- match' f f'

src/Idris/Parser.hs+14−9

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

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

142142parseImports fname input

143143 = do i <- get

144− case (runParser (do mname <- pHeader

144+ case (runParser (do whiteSpace

145+ mname <- pHeader

145146 ps <- many pImport

146147 rest <- getInput

147148 pos <- getPosition

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

149− Left err -> fail (ishow err)

150+ Left err -> fail (show err)

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

151152 return x

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

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

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

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

155156

156157pHeader :: IParser [String]

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

158159 return (parseName i))

159− <|> return []

160+ <|> return []

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

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

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

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

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

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

942943 ++ toTable (reverse fixes) ++

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

944+ [[backtick],

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

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

945947

946948toTable fs = map (map toBin)

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

953955 assoc (Infixr _) = AssocRight

954956 assoc (InfixN _) = AssocNone

955957

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

957− return (f fc) }) assoc

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

959− return (f fc) })

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

959+ return (f fc)) assoc

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

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

960965

961966--------- Data declarations ---------

962967