2686158 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Be more careful when unifying metavariable applications

2686158Edwin Brady14 years ago

src/Core/ProofState.hs+7−5

compare with master

unifiedsplit

@@ -156,9 +156,11 @@ unify' :: Context -> Env -> TT Name -> TT Name -> StateT TState TC [(Name, TT Na

156unify' ctxt env topx topy =

157 do ps <- get

158 (u, fails) <- lift $ unify ctxt env topx topy (injective ps) (holes ps)

159−-- trace ("Unified " ++ show (topx, topy) ++ show (injective ps) ++

159+-- trace ("Unified " ++ show (topx, topy) ++ " in " ++ show env ++

160-- " " ++ show u ++ "\n" ++ qshow fails ++ "\nCurrent problems:\n"

161−-- ++ qshow (problems ps) ++ "\n" ++ show (holes ps)) $

161+-- ++ qshow (problems ps) ++ "\n" ++ show (holes ps) ++ "\n"

162+-- -- ++ show (pterm ps)

163+-- ++ "\n----------") $

162 case fails of

164 case fails of

163-- [] -> return u

165-- [] -> return u

164 err ->

166 err ->

@@ -396,9 +398,9 @@ solve ctxt env (Bind x (Guess ty val) sc)

396 instances = instances ps \\ [x] })

398 instances = instances ps \\ [x] })

397 return $ {- Bind x (Let ty val) sc -}

399 return $ {- Bind x (Let ty val) sc -}

398 instantiate val (pToV x sc)

400 instantiate val (pToV x sc)

399− | otherwise = do ps <- get

400− lift $ tfail $ IncompleteTerm val

401+ | otherwise = lift $ tfail $ IncompleteTerm val

402+solve _ _ h@(Bind x t sc)

401−solve _ _ h = do ps <- get

403+ = do ps <- get

402 fail $ "Not a guess " ++ show h ++ "\n" ++ show (holes ps, pterm ps)

404 fail $ "Not a guess " ++ show h ++ "\n" ++ show (holes ps, pterm ps)

403

405

404introTy :: Raw -> Maybe Name -> RunTactic

406introTy :: Raw -> Maybe Name -> RunTactic

src/Core/Unify.hs+30−2

@@ -158,7 +158,9 @@ unify ctxt env topx topy injtc holes =

158 let (heady, argsy) = unApply appy

159 if (length argsx == length argsy &&

160 ((headx == heady) || (argsx == argsy) ||

161+ (and (zipWith sameStruct (headx:argsx) (heady:argsy)))))

162+ then

161− (notFn headx && notFn heady))) then

163+-- (notFn headx && notFn heady))) then

162 do uf <- un' True bnames headx heady

164 do uf <- un' True bnames headx heady

163 unArgs uf argsx argsy

165 unArgs uf argsx argsy

164 else unifyTmpFail appx appy

166 else unifyTmpFail appx appy

@@ -183,10 +185,25 @@ unify ctxt env topx topy injtc holes =

183 unArgs vs xs ys

185 unArgs vs xs ys

184

186

185 metavarApp tm = let (f, args) = unApply tm in

187 metavarApp tm = let (f, args) = unApply tm in

186− all (\x -> metavar x || notFn x) (f : args)

188+ all (\x -> metavar x || inenv x) (f : args)

189+ metavarApp' tm = let (f, args) = unApply tm in

190+ all (\x -> pat x || metavar x) (f : args)

191+

192+ sameStruct (App f x) (App g y) = sameStruct f g && sameStruct x y

193+ sameStruct (P _ x _) (P _ y _) = True

194+ sameStruct (V i) (V j) = i == j

195+ sameStruct (Constant x) (Constant y) = True

196+ sameStruct (Bind n t sc) (P _ _ _) = True

197+ sameStruct (P _ _ _) (Bind n t sc) = True

198+ sameStruct (Bind n t sc) (Bind n' t' sc') = sameStruct sc sc'

199+ sameStruct _ _ = False

200+

187 metavar t = case t of

201 metavar t = case t of

188 P _ x _ -> x `elem` holes || holeIn env x

202 P _ x _ -> x `elem` holes || holeIn env x

189 _ -> False

203 _ -> False

204+ pat t = case t of

205+ P _ x _ -> x `elem` holes || patIn env x

206+ _ -> False

190 inenv t = case t of

207 inenv t = case t of

191 P _ x _ -> x `elem` (map fst env)

208 P _ x _ -> x `elem` (map fst env)

192 _ -> False

209 _ -> False

@@ -197,6 +214,10 @@ unify ctxt env topx topy injtc holes =

197 | n == n' = un' False bnames x y

214 | n == n' = un' False bnames x y

198 un' fn bnames (Bind n (Lam t) (App x (P Bound n' _))) y

215 un' fn bnames (Bind n (Lam t) (App x (P Bound n' _))) y

199 | n == n' = un' False bnames x y

216 | n == n' = un' False bnames x y

217+ un' fn bnames x (Bind n (Lam t) (App y (V 0)))

218+ = un' False bnames x y

219+ un' fn bnames (Bind n (Lam t) (App x (V 0))) y

220+ = un' False bnames x y

200-- un' fn bnames (Bind x (PVar _) sx) (Bind y (PVar _) sy)

221-- un' fn bnames (Bind x (PVar _) sx) (Bind y (PVar _) sy)

201-- = un' False ((x,y):bnames) sx sy

222-- = un' False ((x,y):bnames) sx sy

202-- un' fn bnames (Bind x (PVTy _) sx) (Bind y (PVTy _) sy)

223-- un' fn bnames (Bind x (PVTy _) sx) (Bind y (PVTy _) sy)

@@ -298,5 +319,12 @@ errEnv = map (\(x, b) -> (x, binderTy b))

298holeIn :: Env -> Name -> Bool

319holeIn :: Env -> Name -> Bool

299holeIn env n = case lookup n env of

320holeIn env n = case lookup n env of

300 Just (Hole _) -> True

321 Just (Hole _) -> True

322+ Just (Guess _ _) -> True

323+ _ -> False

324+

325+patIn :: Env -> Name -> Bool

326+patIn env n = case lookup n env of

327+ Just (PVar _) -> True

328+ Just (PVTy _) -> True

301 _ -> False

329 _ -> False

302

330

src/Idris/ElabTerm.hs+9

@@ -122,6 +122,13 @@ elab ist info pattern tcgen fn tm

122 trace ("Elaborating " ++ show t ++ " : " ++ show g ++ "\n\tin " ++ show tm)

123 $ -}

124 do t' <- insertCoerce ina t

125+ g <- goal

126+ tm <- get_term

127+ ps <- get_probs

128+-- trace ("Elaborating " ++ show t' ++ " in " ++ show g

129+-- ++ "\n" ++ show tm

130+-- ++ "\nproblems " ++ show ps

131+-- ++ "\n-----------\n") $

125 elab' ina t'

132 elab' ina t'

126

133

127 local f = do e <- get_env

134 local f = do e <- get_env

@@ -421,6 +428,8 @@ elab ist info pattern tcgen fn tm

421 -- fail $ "Not implemented " ++ show c ++ "\n" ++ show args

428 -- fail $ "Not implemented " ++ show c ++ "\n" ++ show args

422 -- elaborate case

429 -- elaborate case

423 updateAux (newdef : )

430 updateAux (newdef : )

431+ -- if we haven't got the type yet, hopefully we'll get it later!

432+ movelast tyn

424 solve

433 solve

425 where mkCaseName (NS n ns) = NS (mkCaseName n) ns

434 where mkCaseName (NS n ns) = NS (mkCaseName n) ns

426 mkCaseName (UN x) = UN (x ++ "_case")

435 mkCaseName (UN x) = UN (x ++ "_case")

test/reg011/expectednew file

No changes to the content.

test/reg011/reg011.idrnew file+10

@@ -0,0 +1,10 @@

1+vfoldl : (P : Nat -> Type) ->

2+ ((x : Nat) -> P x -> a -> P (S x)) -> P O

3+ -> Vect a m -> P m

4+-- vfoldl P cons nil []

5+-- = nil

6+vfoldl P cons nil (x :: xs)

7+ = vfoldl (\n => P (S n)) (\ n => cons (S n)) (cons O nil x) xs

8+%logging 0

9+-- vfoldl P cons nil (x :: xs)

10+-- = vfoldl (\n => P (S n)) (\ n => cons _) (cons _ nil x) xs

test/reg011/runnew file+3

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

1+#!/bin/bash

2+idris $@ reg011.idr --check

3+rm -f *.ibc