2686158 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Be more careful when unifying metavariable applications

Otherwise things get solved which shouldn't be. Fixes issue #227

commit2686158feae4c4ac4794935306e68ae706d69c6e authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSat 16 Mar 2013, 17:48 (14 years ago) parentfe207af

6 files changed+59−7

compare with master

unifiedsplit

src/Core/ProofState.hs+7−5 src/Core/Unify.hs+30−2 src/Idris/ElabTerm.hs+9 test/reg011/expected test/reg011/reg011.idr+10 test/reg011/run+3

src/Core/ProofState.hs+7−5

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

156156unify' ctxt env topx topy =

157157 do ps <- get

158158 (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 ++

160160-- " " ++ 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----------") $

162164 case fails of

163165-- [] -> return u

164166 err ->

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

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

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

398400 instantiate val (pToV x sc)

399− | otherwise = do ps <- get

400− lift $ tfail $ IncompleteTerm val

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

401+ | otherwise = lift $ tfail $ IncompleteTerm val

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

403+ = do ps <- get

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

403405

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

src/Core/Unify.hs+30−2

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

158158 let (heady, argsy) = unApply appy

159159 if (length argsx == length argsy &&

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

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

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

162+ then

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

162164 do uf <- un' True bnames headx heady

163165 unArgs uf argsx argsy

164166 else unifyTmpFail appx appy

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

183185 unArgs vs xs ys

184186

185187 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+

187201 metavar t = case t of

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

189203 _ -> False

204+ pat t = case t of

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

206+ _ -> False

190207 inenv t = case t of

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

192209 _ -> False

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

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

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

199216 | 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

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

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

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

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

298319holeIn :: Env -> Name -> Bool

299320holeIn env n = case lookup n env of

300321 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

301329 _ -> False

302330

src/Idris/ElabTerm.hs+9

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

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

123123 $ -}

124124 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") $

125132 elab' ina t'

126133

127134 local f = do e <- get_env

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

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

422429 -- elaborate case

423430 updateAux (newdef : )

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

432+ movelast tyn

424433 solve

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

426435 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