801aa83 · Idris-dev · git.iko.soy

CHANGELOG+6

compare with master

unifiedsplit

@@ -1,3 +1,9 @@

1+New in 0.9.12:

2+--------------

3+

4+* Proof search now works for metavariables in types, giving some interactive

5+ type inference.

6+

1New in 0.9.11:

7New in 0.9.11:

2--------------

8--------------

3

9

src/Idris/AbsSyntax.hs+25−5

@@ -161,10 +161,10 @@ addTyInferred n

161 putIState $ i { idris_tyinfodata =

162 addDef n TIPartial (idris_tyinfodata i) }

163

164−addTyInfConstraints :: [(Term, Term)] -> Idris ()

164+addTyInfConstraints :: FC -> [(Term, Term)] -> Idris ()

165−addTyInfConstraints ts = do logLvl 2 $ "TI missing: " ++ show ts

165+addTyInfConstraints fc ts = do logLvl 2 $ "TI missing: " ++ show ts

166− mapM_ addConstraint ts

166+ mapM_ addConstraint ts

167− return ()

167+ return ()

168 where addConstraint (x, y) = findMVApps x y

169

170 findMVApps x y

@@ -189,7 +189,8 @@ addTyInfConstraints ts = do logLvl 2 $ "TI missing: " ++ show ts

189 logLvl 1 $ "TI constraint: " ++ show (n, t)

190 case lookupCtxt n (idris_tyinfodata ist) of

191 [TISolution ts] ->

192+ do mapM_ (checkConsistent t) ts

192− do let ti' = addDef n (TISolution (t : ts))

193+ let ti' = addDef n (TISolution (t : ts))

193 (idris_tyinfodata ist)

194 (idris_tyinfodata ist)

194 put $ ist { idris_tyinfodata = ti' }

195 put $ ist { idris_tyinfodata = ti' }

195 _ ->

196 _ ->

@@ -197,6 +198,25 @@ addTyInfConstraints ts = do logLvl 2 $ "TI missing: " ++ show ts

197 (idris_tyinfodata ist)

198 (idris_tyinfodata ist)

198 put $ ist { idris_tyinfodata = ti' }

199 put $ ist { idris_tyinfodata = ti' }

199

200

201+ -- Check a solution is consistent with previous solutions

202+ -- Meaning: If heads are both data types, they had better be the

203+ -- same.

204+ checkConsistent :: Term -> Term -> Idris ()

205+ checkConsistent x y =

206+ do let (fx, _) = unApply x

207+ let (fy, _) = unApply y

208+ case (fx, fy) of

209+ (P (TCon _ _) n _, P (TCon _ _) n' _) -> errWhen (n/=n)

210+ (P (TCon _ _) n _, Constant _) -> errWhen True

211+ (Constant _, P (TCon _ _) n' _) -> errWhen True

212+ (P (DCon _ _) n _, P (DCon _ _) n' _) -> errWhen (n/=n)

213+ _ -> return ()

214+

215+ where errWhen True

216+ = throwError (At fc

217+ (CantUnify False x y (Msg "") [] 0))

218+ errWhen False = return ()

219+

200isTyInferred :: Name -> Idris Bool

220isTyInferred :: Name -> Idris Bool

201isTyInferred n

221isTyInferred n

202 = do i <- getIState

222 = do i <- getIState

src/Idris/ElabDecls.hs+2−2

@@ -1295,7 +1295,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

1295 probs <- get_probs

1296 return (res, probs))

1297

1298− when inf $ addTyInfConstraints (map (\(x,y,_,_) -> (x,y)) probs)

1298+ when inf $ addTyInfConstraints fc (map (\(x,y,_,_) -> (x,y)) probs)

1299

1300 let lhs_tm = orderPats (getInferTerm lhs')

1301 let lhs_ty = getInferType lhs'

@@ -1357,7 +1357,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

1357 probs <- get_probs

1358 return (tm, ds, is, probs))

1359

1360− when inf $ addTyInfConstraints (map (\(x,y,_,_) -> (x,y)) probs)

1360+ when inf $ addTyInfConstraints fc (map (\(x,y,_,_) -> (x,y)) probs)

1361

1362 logLvl 5 "DONE CHECK"

1363 logLvl 2 $ "---> " ++ show rhs'

test/interactive002/expectednew file+9

@@ -0,0 +1,9 @@

1+Type checking ./interactive002.idr

2+Nat

3+Nat

4+Nat

5+Nat

6+Vect (n + m) a

7+Nat

8+Nat

9+S n

test/interactive002/inputnew file+9

@@ -0,0 +1,9 @@

1+:ps 2 foo_arg1

2+:ps 2 foo_arg2

3+:ps 2 foo_arg3

4+:ps 2 foo_ret

5+:ps 6 bar_out

6+:ps 9 plus_in1

7+:ps 9 plus_out

8+:ps 13 what

9+

test/interactive002/interactive002.idrnew file+17

@@ -0,0 +1,17 @@

1+

2+foo : ?foo_arg1 -> ?foo_arg2 -> ?foo_arg3 -> ?foo_ret

3+foo (S a) b c = plus (a + b + c) 42

4+foo Z b c = plus b c

5+

6+bar : Vect n a -> Vect m a -> ?bar_out

7+bar xs ys = xs ++ ys

8+

9+myplus : ?plus_in1 -> ?plus_in2 -> ?plus_out

10+myplus Z y = y

11+myplus (S k) y = S (myplus k y)

12+

13+vfun : a -> Vect n a -> Vect n a -> Vect ?what a

14+vfun v xs ys = v :: ys

15+

16+

17+

test/interactive002/runnew file+3

@@ -0,0 +1,3 @@

1+#!/usr/bin/env bash

2+idris --quiet interactive002.idr < input

3+rm -f *.ibc