99a8a66 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Check that explicitly given implicit args unify with inferred versions

Also exposed a unification bug which unified things which shouldn't be: f x = f y does not imply x = y unless f is injective, and this was not properly checked. Fixes issue #127, as it caused a related problem in the coverage checker.

commit99a8a6657e1986e48857ccb179ed9422780fa157 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSat 11 May 2013, 21:03 (13 years ago) parentea11519

13 files changed+86−35

compare with master

unifiedsplit

src/Core/Elaborate.hs+6−3 src/Core/Evaluate.hs+3−3 src/Core/ProofState.hs+27−7 src/Core/Typecheck.hs+1−1 src/Core/Unify.hs+10−9 src/Idris/AbsSyntax.hs+8−4 src/Idris/ElabDecls.hs+5−4 src/Idris/ElabTerm.hs+2−1 src/Idris/Prover.hs+2−2 test/reg018/expected+1 test/reg018/reg018d.idr+12 test/reg018/run+1 test/test014/Resimp.idr+8−1

src/Core/Elaborate.hs+6−3

@@ -391,10 +391,13 @@ apply fn imps =

391391 else

392392 map fst (filter (not.snd) (zip args (map fst imps)))

393393 let (n, hunis) = -- trace ("AVOID UNIFY: " ++ show (fn, dont) ++ "\n" ++ show ptm) $

394− unified p

394+ unified p

395395 let unify = -- trace ("Not done " ++ show hs) $

396− dropGiven dont hunis hs

397− put (ES (p { dontunify = dont, unified = (n, unify) }, a) s prev)

396+ dropGiven dont hunis hs

397+ let notunify = -- trace ("Not done " ++ show hs) $

398+ keepGiven dont hunis hs

399+ put (ES (p { dontunify = dont, unified = (n, unify),

400+ notunified = notunify ++ notunified p }, a) s prev)

398401 ptm <- get_term

399402 g <- goal

400403-- trace ("Goal " ++ show g ++ "\n" ++ show (fn, imps, unify) ++ "\n" ++ show ptm) $

src/Core/Evaluate.hs+3−3

@@ -703,10 +703,10 @@ addCtxtDef n d c = let ctxt = definitions c

703703 ctxt' = addDef n (d, Public, Unchecked) ctxt in

704704 c { definitions = ctxt' }

705705

706−addTyDecl :: Name -> Type -> Context -> Context

707−addTyDecl n ty uctxt

706+addTyDecl :: Name -> NameType -> Type -> Context -> Context

707+addTyDecl n nt ty uctxt

708708 = let ctxt = definitions uctxt

709− ctxt' = addDef n (TyDecl Ref ty, Public, Unchecked) ctxt in

709+ ctxt' = addDef n (TyDecl nt ty, Public, Unchecked) ctxt in

710710 uctxt { definitions = ctxt' }

711711

712712addDatatype :: Datatype Name -> Context -> Context

src/Core/ProofState.hs+27−7

@@ -5,7 +5,8 @@

55 evaluation/checking inside the proof system, etc. --}

77module Core.ProofState(ProofState(..), newProof, envAtFocus, goalAtFocus,

8− Tactic(..), Goal(..), processTactic, dropGiven) where

8+ Tactic(..), Goal(..), processTactic,

9+ dropGiven, keepGiven) where

910

1011import Core.Typecheck

1112import Core.Evaluate

@@ -27,6 +28,7 @@ data ProofState = PS { thname :: Name,

2728 ptype :: Type, -- original goal

2829 dontunify :: [Name], -- explicitly given by programmer, leave it

2930 unified :: (Name, [(Name, Term)]),

31+ notunified :: [(Name, Term)],

3032 solved :: Maybe (Name, Term),

3133 problems :: Fails,

3234 injective :: [Name],

@@ -78,8 +80,8 @@ data Tactic = Attack

7880-- Some utilites on proof and tactic states

7981

8082instance Show ProofState where

81− show (PS nm [] _ _ tm _ _ _ _ _ _ _ _ _ _ _ _) = show nm ++ ": no more goals"

82− show (PS nm (h:hs) _ _ tm _ _ _ _ _ _ i _ _ ctxt _ _)

83+ show (PS nm [] _ _ tm _ _ _ _ _ _ _ _ _ _ _ _ _) = show nm ++ ": no more goals"

84+ show (PS nm (h:hs) _ _ tm _ _ _ _ _ _ _ i _ _ ctxt _ _)

8385 = let OK g = goal (Just h) tm

8486 wkenv = premises g in

8587 "Other goals: " ++ show hs ++ "\n" ++

@@ -102,12 +104,12 @@ instance Show ProofState where

102104 showG ps b = showEnv ps (binderTy b)

103105

104106instance Pretty ProofState where

105− pretty (PS nm [] _ _ trm _ _ _ _ _ _ _ _ _ _ _ _) =

107+ pretty (PS nm [] _ _ trm _ _ _ _ _ _ _ _ _ _ _ _ _) =

106108 if size nm > breakingSize then

107109 pretty nm <> colon $$ nest nestingSize (text " no more goals.")

108110 else

109111 pretty nm <> colon <+> text " no more goals."

110− pretty p@(PS nm (h:hs) _ _ tm _ _ _ _ _ _ i _ _ ctxt _ _) =

112+ pretty p@(PS nm (h:hs) _ _ tm _ _ _ _ _ _ _ i _ _ ctxt _ _) =

111113 let OK g = goal (Just h) tm in

112114 let wkEnv = premises g in

113115 text "Other goals" <+> colon <+> pretty hs $$

@@ -194,7 +196,7 @@ newProof :: Name -> Context -> Type -> ProofState

194196newProof n ctxt ty = let h = holeName 0

195197 ty' = vToP ty in

196198 PS n [h] [] 1 (Bind h (Hole ty')

197− (P Bound h ty')) ty [] (h, [])

199+ (P Bound h ty')) ty [] (h, []) []

198200 Nothing [] []

199201 [] []

200202 Nothing ctxt "" False

@@ -387,10 +389,19 @@ complete_fill ctxt env (Bind x (Guess ty val) sc) =

387389 return $ Bind x (Guess ty val) sc

388390complete_fill ctxt env t = fail $ "Can't complete fill at " ++ show t

389391

392+-- When solving something in the 'dont unify' set, we should check

393+-- that the guess we are solving it with unifies with the thing unification

394+-- found for it, if anything.

395+

390396solve :: RunTactic

391397solve ctxt env (Bind x (Guess ty val) sc)

392398 | True = do ps <- get

393399 let (uh, uns) = unified ps

400+ case lookup x (notunified ps) of

401+ Just tm -> do -- trace ("AVOIDED " ++ show (x, tm, val)) $

402+ -- return []

403+ unify' ctxt env tm val

404+ _ -> return []

394405 action (\ps -> ps { holes = holes ps \\ [x],

395406 solved = Just (x, val),

396407-- problems = solveInProblems

@@ -565,6 +576,15 @@ dropGiven du (u@(n, _) : us) hs

565576-- dropGiven du (u@(_, P a n ty) : us) | n `elem` du = dropGiven du us

566577dropGiven du (u : us) hs = u : dropGiven du us hs

567578

579+keepGiven du [] hs = []

580+keepGiven du ((n, P Bound t ty) : us) hs

581+ | n `elem` du && not (t `elem` du)

582+ && n `elem` hs && t `elem` hs

583+ = keepGiven du us hs

584+keepGiven du (u@(n, _) : us) hs

585+ | n `elem` du = u : keepGiven du us hs

586+keepGiven du (u : us) hs = keepGiven du us hs

587+

568588updateSolved xs x = -- trace ("Updating " ++ show xs ++ " in " ++ show x) $

569589 updateSolved' xs x

570590updateSolved' xs (Bind n (Hole ty) t)

@@ -618,7 +638,7 @@ processTactic EndUnify ps

618638 ns' = map (\ (n, t) -> (n, updateSolved ns t)) ns

619639 (ns'', probs') = updateProblems (context ps) ns' (problems ps)

620640 (injective ps) (holes ps)

621− tm' = -- trace ("Updating " ++ show ns' ++ "\n" ++ show ns'') $ -- ++ " in " ++ show (pterm ps)) $

641+ tm' = -- trace ("Updating " ++ show ns_in ++ "\n" ++ show ns'') $ -- ++ " in " ++ show (pterm ps)) $

622642 updateSolved ns'' (pterm ps) in

623643 return (ps { pterm = tm',

624644 unified = (h, []),

src/Core/Typecheck.hs+1−1

@@ -227,7 +227,7 @@ checkProgram ctxt [] = return ctxt

227227checkProgram ctxt ((n, RConst t) : xs)

228228 = do (t', tt') <- trace (show n) $ check ctxt [] t

229229 isType ctxt [] tt'

230− checkProgram (addTyDecl n t' ctxt) xs

230+ checkProgram (addTyDecl n Ref t' ctxt) xs

231231checkProgram ctxt ((n, RFunction (RawFun ty val)) : xs)

232232 = do (ty', tyt') <- trace (show n) $ check ctxt [] ty

233233 (val', valt') <- check ctxt [] val

src/Core/Unify.hs+10−9

@@ -56,7 +56,7 @@ unify ctxt env topx topy dont holes =

5656 injective (P (TCon _ _) _ _) = True

5757 injective (App f (P _ _ _)) = injective f

5858 injective (App f (Constant _)) = injective f

59− injective (App f a) = injective f && injective a

59+ injective (App f a) = injective f -- && injective a

6060 injective _ = False

6161

6262 notP (P _ _ _) = False

@@ -133,10 +133,9 @@ unify ctxt env topx topy dont holes =

133133 | fst (bnames!!i) == x || snd (bnames!!i) == x = do sc 1; return []

134134

135135 un' fn bnames appx@(App fx ax) appy@(App fy ay)

136− | injective fx && sameArgStruct appx appy && metavarApp appy

137− || injective fy && sameArgStruct appx appy && metavarApp appx

138− || injective fx && injective fy

139− || fx == fy

136+ | (injective fx && sameArgStruct appx appy && metavarApp appy)

137+ || (injective fy && sameArgStruct appx appy && metavarApp appx)

138+ || (injective fx && injective fy)

140139 = do let (headx, _) = unApply fx

141140 let (heady, _) = unApply fy

142141 -- fail quickly if the heads are disjoint

@@ -158,17 +157,19 @@ unify ctxt env topx topy dont holes =

158157 hf <- un' False bnames fx' fy'

159158 sc 1

160159 combine bnames hf ha)

161− | otherwise

162− = do let (headx, argsx) = unApply appx

160+ | otherwise =

161+ do let (headx, argsx) = unApply appx

163162 let (heady, argsy) = unApply appy

163+ -- traceWhen (headx == heady) (show (appx, appy)) $

164164 if (length argsx == length argsy &&

165− ((headx == heady) || (argsx == argsy) ||

165+ ((headx == heady && inenv headx) || (argsx == argsy) ||

166166 (and (zipWith sameStruct (headx:argsx) (heady:argsy)))))

167167 then

168168-- (notFn headx && notFn heady))) then

169169 do uf <- un' True bnames headx heady

170170 unArgs uf argsx argsy

171− else unifyTmpFail appx appy

171+ else -- trace ("TMPFAIL " ++ show (appx, appy, injective appx, injective appy)) $

172+ unifyTmpFail appx appy

172173 where hnormalise [] _ _ t = t

173174 hnormalise ns ctxt env t = normalise ctxt env t

174175 checkHeads (P (DCon _ _) x _) (P (DCon _ _) y _)

src/Idris/AbsSyntax.hs+8−4

@@ -222,10 +222,14 @@ addConstraints fc (v, cs)

222222 let ics = zip cs (repeat fc) ++ idris_constraints i

223223 putIState $ i { tt_ctxt = ctxt', idris_constraints = ics }

224224

225−addDeferred :: [(Name, Type)] -> Idris ()

226−addDeferred ns = do mapM_ (\(n, t) -> updateContext (addTyDecl n (tidyNames [] t))) ns

227− i <- getIState

228− putIState $ i { idris_metavars = map fst ns ++ idris_metavars i }

225+addDeferred = addDeferred' Ref

226+addDeferredTyCon = addDeferred' (TCon 0 0)

227+

228+addDeferred' :: NameType -> [(Name, Type)] -> Idris ()

229+addDeferred' nt ns

230+ = do mapM_ (\(n, t) -> updateContext (addTyDecl n nt (tidyNames [] t))) ns

231+ i <- getIState

232+ putIState $ i { idris_metavars = map fst ns ++ idris_metavars i }

229233 where tidyNames used (Bind (MN i x) b sc)

230234 = let n' = uniqueName (UN x) used in

231235 Bind n' b $ tidyNames (n':used) sc

src/Idris/ElabDecls.hs+5−4

@@ -121,11 +121,11 @@ elabData info syn doc fc codata (PLaterdecl n t_in)

121121 ((t', defer, is), log) <- tclift $ elaborate ctxt n (TType (UVal 0)) []

122122 (erun fc (build i info False n t))

123123 def' <- checkDef fc defer

124− addDeferred def'

124+ addDeferredTyCon def'

125125 mapM_ (elabCaseBlock info) is

126126 (cty, _) <- recheckC fc [] t'

127127 logLvl 2 $ "---> " ++ show cty

128− updateContext (addTyDecl n cty) -- temporary, to check cons

128+ updateContext (addTyDecl n (TCon 0 0) cty) -- temporary, to check cons

129129

130130elabData info syn doc fc codata (PDatadecl n t_in dcons)

131131 = do iLOG (show fc)

@@ -137,12 +137,12 @@ elabData info syn doc fc codata (PDatadecl n t_in dcons)

137137 ((t', defer, is), log) <- tclift $ elaborate ctxt n (TType (UVal 0)) []

138138 (erun fc (build i info False n t))

139139 def' <- checkDef fc defer

140− addDeferred def'

140+ addDeferredTyCon def'

141141 mapM_ (elabCaseBlock info) is

142142 (cty, _) <- recheckC fc [] t'

143143 logLvl 2 $ "---> " ++ show cty

144144 -- temporary, to check cons

145− when undef $ updateContext (addTyDecl n cty)

145+ when undef $ updateContext (addTyDecl n (TCon 0 0) cty)

146146 cons <- mapM (elabCon info syn n codata) dcons

147147 ttag <- getName

148148 i <- getIState

@@ -585,6 +585,7 @@ checkPossible info fc tcgen fname lhs_in

585585 case recheck ctxt [] (forget lhs_tm) lhs_tm of

586586 OK _ -> return True

587587 _ -> return False

588+

588589-- b <- inferredDiff fc (delab' i lhs_tm True) lhs

589590-- return (not b) -- then return (Just lhs_tm) else return Nothing

590591-- trace (show (delab' i lhs_tm True) ++ "\n" ++ show lhs) $ return (not b)

src/Idris/ElabTerm.hs+2−1

@@ -96,9 +96,10 @@ elab :: IState -> ElabInfo -> Bool -> Bool -> Name -> PTerm ->

9696 ElabD ()

9797elab ist info pattern tcgen fn tm

9898 = do elabE (False, False) tm -- (in argument, guarded)

99+ end_unify

99100 when pattern -- convert remaining holes to pattern vars

100101 (do update_term orderPats

101−-- tm <- get_term

102+ tm <- get_term

102103 mkPat)

103104 where

104105 isph arg = case getTm arg of

src/Idris/Prover.hs+2−2

@@ -78,9 +78,9 @@ elabStep st e = do case runStateT e st of

7878 fail (pshow i a)

7979

8080dumpState :: IState -> ProofState -> IO ()

81−dumpState ist (PS nm [] _ _ tm _ _ _ _ _ _ _ _ _ _ _ _) =

81+dumpState ist (PS nm [] _ _ tm _ _ _ _ _ _ _ _ _ _ _ _ _) =

8282 putStrLn . render $ pretty nm <> colon <+> text "No more goals."

83−dumpState ist ps@(PS nm (h:hs) _ _ tm _ _ _ _ _ problems i _ _ ctxy _ _) = do

83+dumpState ist ps@(PS nm (h:hs) _ _ tm _ _ _ _ _ _ problems i _ _ ctxy _ _) = do

8484 let OK ty = goalAtFocus ps

8585 let OK env = envAtFocus ps

8686 putStrLn . render $

test/reg018/expected+1

@@ -1,3 +1,4 @@

11reg018a.idr:16:conat.minusCoNat is not productive

22reg018b.idr:8:A.showB is possibly not total due to recursive path A.showB

33reg018c.idr:19:CodataTest.inf is not productive

4+reg018d.idr:5:Main.pull is not total as there are missing cases

test/reg018/reg018d.idrnew file+12

@@ -0,0 +1,12 @@

1+module Main

3+total

4+pull : Fin (S n) -> Vect a (S n) -> (a, Vect a n)

5+pull {n=O} _ (x :: xs) = (x, xs)

6+-- pull {n=S q} fO (Vect.(::) {n=S _} x xs) = (x, xs)

7+pull {n=S _} (fS n) (x :: xs) =

8+ let (v, vs) = pull n xs in

9+ (v, x::vs)

10+

11+main : IO ()

12+main = print (pull fO [0, 1, 2])

test/reg018/run+1

@@ -2,3 +2,4 @@

22idris $@ reg018a.idr --check

33idris $@ reg018b.idr --check

44idris $@ reg018c.idr --check

5+idris $@ reg018d.idr --check

test/test014/Resimp.idr+8−1

@@ -69,6 +69,13 @@ using (i: Fin n, gam : Vect Ty n, gam' : Vect Ty n, gam'' : Vect Ty n)

6969 envUpdate (pop k) val (x :: xs) = x :: envUpdate k val xs

7070 envUpdate stop _ Nil impossible

7171

72+ total

73+ envUpdateVal : (p:HasType gam i a) -> (val:b) ->

74+ Env gam -> Env (update gam p (Val b))

75+ envUpdateVal stop val (x :: xs) = val :: xs

76+ envUpdateVal (pop k) val (x :: xs) = x :: envUpdateVal k val xs

77+ envUpdateVal stop _ Nil impossible

78+

7279 envTail : Env (a :: gam) -> Env gam

7380 envTail (x :: xs) = xs

7481

@@ -121,7 +128,7 @@ using (i: Fin n, gam : Vect Ty n, gam' : Vect Ty n, gam'' : Vect Ty n)

121128 (\env', scope' => k (envTail env') scope')

122129 interp env (Update method x) k

123130 = do x' <- getUpdater (method (envLookup x env))

124− k (envUpdate x x' env) (return ())

131+ k (envUpdateVal x x' env) (return ())

125132 interp env (Use method x) k

126133 = do x' <- getReader (method (envLookup x env))

127134 k env (return x')