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

git.iko.soy/Idris-dev

More consistency checking on inference constraints

Also added a test for simple interactive type inference

commit801aa8347a389190b3b959cfe15f0752e74fbe90 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSun 9 Feb 2014, 19:06 (13 years ago) parent71d7de0

7 files changed+71−7

compare with master

unifiedsplit

CHANGELOG+6 src/Idris/AbsSyntax.hs+25−5 src/Idris/ElabDecls.hs+2−2 test/interactive002/expected+9 test/interactive002/input+9 test/interactive002/interactive002.idr+17 test/interactive002/run+3

CHANGELOG+6

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

1+New in 0.9.12:

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

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

5+ type inference.

17New in 0.9.11:

28--------------

src/Idris/AbsSyntax.hs+25−5

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

161161 putIState $ i { idris_tyinfodata =

162162 addDef n TIPartial (idris_tyinfodata i) }

163163

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

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

166− mapM_ addConstraint ts

167− return ()

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

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

166+ mapM_ addConstraint ts

167+ return ()

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

169169

170170 findMVApps x y

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

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

190190 case lookupCtxt n (idris_tyinfodata ist) of

191191 [TISolution ts] ->

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

192+ do mapM_ (checkConsistent t) ts

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

193194 (idris_tyinfodata ist)

194195 put $ ist { idris_tyinfodata = ti' }

195196 _ ->

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

197198 (idris_tyinfodata ist)

198199 put $ ist { idris_tyinfodata = ti' }

199200

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+

200220isTyInferred :: Name -> Idris Bool

201221isTyInferred n

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

12951295 probs <- get_probs

12961296 return (res, probs))

12971297

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

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

12991299

13001300 let lhs_tm = orderPats (getInferTerm lhs')

13011301 let lhs_ty = getInferType lhs'

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

13571357 probs <- get_probs

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

13591359

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

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

13611361

13621362 logLvl 5 "DONE CHECK"

13631363 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

test/interactive002/interactive002.idrnew file+17

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

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

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

7+bar xs ys = xs ++ ys

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