git.iko.soy/Idris-dev
on master help sign in
Postpone injectivity check until after unification
1823cf9Edwin Brady
src/Core/Elaborate.hs+8
compare with master
unifiedsplit
@@ -111,6 +111,14 @@ get_deferred :: Elab [Name]
111get_deferred = do ES p _ _ <- get
111get_deferred = do ES p _ _ <- get
112 return (deferred p)
112 return (deferred p)
113
113
114+get_inj :: Elab [(Term, Term, Term)]
115+get_inj = do ES p _ _ <- get
116+ return (injective p)
117+
118+checkInjective :: (Term, Term, Term) -> Elab ()
119+checkInjective (tm, l, r) = if isInjective tm then return ()
120+ else lift $ tfail (NotInjective tm l r)
121+
114-- get instance argument names
122-- get instance argument names
115get_instances :: Elab [Name]
123get_instances :: Elab [Name]
116get_instances = do ES p _ _ <- get
124get_instances = do ES p _ _ <- get
src/Core/ProofState.hs+19−6
@@ -23,6 +23,7 @@ data ProofState = PS { thname :: Name,
23 pterm :: Term, -- current proof term
23 pterm :: Term, -- current proof term
24 ptype :: Type, -- original goal
24 ptype :: Type, -- original goal
25 unified :: (Name, [(Name, Term)]),
25 unified :: (Name, [(Name, Term)]),
26+ injective :: [(Term, Term, Term)],
26 deferred :: [Name], -- names we'll need to define
27 deferred :: [Name], -- names we'll need to define
27 instances :: [Name], -- instance arguments (for type classes)
28 instances :: [Name], -- instance arguments (for type classes)
28 previous :: Maybe ProofState, -- for undo
29 previous :: Maybe ProofState, -- for undo
@@ -68,8 +69,8 @@ data Tactic = Attack
68-- Some utilites on proof and tactic states
69-- Some utilites on proof and tactic states
69
70
70instance Show ProofState where
71instance Show ProofState where
71− show (PS nm [] _ tm _ _ _ _ _ _ _ _) = show nm ++ ": no more goals"
72+ show (PS nm [] _ tm _ _ _ _ _ _ _ _ _) = show nm ++ ": no more goals"
72− show (PS nm (h:hs) _ tm _ _ i _ _ ctxt _ _)
73+ show (PS nm (h:hs) _ tm _ _ _ i _ _ ctxt _ _)
73 = let OK g = goal (Just h) tm
74 = let OK g = goal (Just h) tm
74 wkenv = premises g in
75 wkenv = premises g in
75 "Other goals: " ++ show hs ++ "\n" ++
76 "Other goals: " ++ show hs ++ "\n" ++
@@ -116,7 +117,7 @@ addLog str = action (\ps -> ps { plog = plog ps ++ str ++ "\n" })
116newProof :: Name -> Context -> Type -> ProofState
117newProof :: Name -> Context -> Type -> ProofState
117newProof n ctxt ty = let h = holeName 0
118newProof n ctxt ty = let h = holeName 0
118 ty' = vToP ty in
119 ty' = vToP ty in
119− PS n [h] 1 (Bind h (Hole ty') (P Bound h ty')) ty (h, [])
120+ PS n [h] 1 (Bind h (Hole ty') (P Bound h ty')) ty (h, []) []
120 [] []
121 [] []
121 Nothing ctxt "" False
122 Nothing ctxt "" False
122
123
@@ -243,6 +244,10 @@ defer n ctxt env (Bind x (Hole t) (P nt x' ty)) | x == x' =
243regret :: RunTactic
244regret :: RunTactic
244regret = undefined
245regret = undefined
245
246
247+addInj :: [(Term, Term, Term)] -> StateT TState TC ()
248+addInj inj = do ps <- get
249+ put (ps { injective = inj ++ injective ps })
250+
246exact :: Raw -> RunTactic
251exact :: Raw -> RunTactic
247exact guess ctxt env (Bind x (Hole ty) sc) =
252exact guess ctxt env (Bind x (Hole ty) sc) =
248 do (val, valty) <- lift $ check ctxt env guess
253 do (val, valty) <- lift $ check ctxt env guess
@@ -256,7 +261,8 @@ fill :: Raw -> RunTactic
256fill guess ctxt env (Bind x (Hole ty) sc) =
261fill guess ctxt env (Bind x (Hole ty) sc) =
257 do (val, valty) <- lift $ check ctxt env guess
262 do (val, valty) <- lift $ check ctxt env guess
258 s <- get
263 s <- get
259− ns <- lift $ unify ctxt env valty ty
264+ (ns, inj) <- lift $ unify ctxt env valty ty
265+ addInj inj
260 ps <- get
266 ps <- get
261 let (uh, uns) = unified ps
267 let (uh, uns) = unified ps
262 put (ps { unified = (uh, uns ++ ns) })
268 put (ps { unified = (uh, uns ++ ns) })
@@ -274,7 +280,8 @@ complete_fill :: RunTactic
274complete_fill ctxt env (Bind x (Guess ty val) sc) =
280complete_fill ctxt env (Bind x (Guess ty val) sc) =
275 do let guess = forget val
281 do let guess = forget val
276 (val', valty) <- lift $ check ctxt env guess
282 (val', valty) <- lift $ check ctxt env guess
277− ns <- lift $ unify ctxt env valty ty
283+ (ns, inj) <- lift $ unify ctxt env valty ty
284+ addInj inj
278 ps <- get
285 ps <- get
279 let (uh, uns) = unified ps
286 let (uh, uns) = unified ps
280 put (ps { unified = (uh, uns ++ ns) })
287 put (ps { unified = (uh, uns ++ ns) })
@@ -302,7 +309,8 @@ introTy ty mn ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
302-- ns <- lift $ unify ctxt env tyv t'
309-- ns <- lift $ unify ctxt env tyv t'
303 case t' of
310 case t' of
304 Bind y (Pi s) t -> let t' = instantiate (P Bound n s) (pToV y t) in
311 Bind y (Pi s) t -> let t' = instantiate (P Bound n s) (pToV y t) in
305− do ns <- lift $ unify ctxt env s tyv
312+ do (ns, inj) <- lift $ unify ctxt env s tyv
313+ addInj inj
306 ps <- get
314 ps <- get
307 let (uh, uns) = unified ps
315 let (uh, uns) = unified ps
308 put (ps { unified = (uh, uns ++ ns) })
316 put (ps { unified = (uh, uns ++ ns) })
@@ -405,12 +413,15 @@ start_unify :: Name -> RunTactic
405start_unify n ctxt env tm = do action (\ps -> ps { unified = (n, []) })
413start_unify n ctxt env tm = do action (\ps -> ps { unified = (n, []) })
406 return tm
414 return tm
407
415
416+tmap f (a, b, c) = (f a, b, c)
417+
408solve_unified :: RunTactic
418solve_unified :: RunTactic
409solve_unified ctxt env tm =
419solve_unified ctxt env tm =
410 do ps <- get
420 do ps <- get
411 let (_, ns) = unified ps
421 let (_, ns) = unified ps
412 action (\ps -> ps { holes = holes ps \\ map fst ns })
422 action (\ps -> ps { holes = holes ps \\ map fst ns })
413 action (\ps -> ps { pterm = updateSolved ns (pterm ps) })
423 action (\ps -> ps { pterm = updateSolved ns (pterm ps) })
424+ action (\ps -> ps { injective = map (tmap (updateSolved ns)) (injective ps) })
414 return (updateSolved ns tm)
425 return (updateSolved ns tm)
415
426
416updateSolved xs (Bind n (Hole ty) t)
427updateSolved xs (Bind n (Hole ty) t)
@@ -437,6 +448,8 @@ processTactic EndUnify ps = let (h, ns) = unified ps
437 tm' = updateSolved ns (pterm ps) in
448 tm' = updateSolved ns (pterm ps) in
438 return (ps { pterm = tm',
449 return (ps { pterm = tm',
439 unified = (h, []),
450 unified = (h, []),
451+ injective = map (tmap (updateSolved ns))
452+ (injective ps),
440 holes = holes ps \\ map fst ns }, "")
453 holes = holes ps \\ map fst ns }, "")
441processTactic (Reorder n) ps
454processTactic (Reorder n) ps
442 = do ps' <- execStateT (tactic (Just n) reorder_claims) ps
455 = do ps' <- execStateT (tactic (Just n) reorder_claims) ps
src/Core/TT.hs+10
@@ -39,6 +39,7 @@ instance Show FC where
39
39
40data Err = Msg String
40data Err = Msg String
41 | CantUnify Term Term Err
41 | CantUnify Term Term Err
42+ | NotInjective Term Term Term
42 | IncompleteTerm Term
43 | IncompleteTerm Term
43 | UniverseError
44 | UniverseError
44 | ProgramLineComment
45 | ProgramLineComment
@@ -314,6 +315,15 @@ convEq _ _ = return False
314
315
315-- A few handy operations on well typed terms:
316-- A few handy operations on well typed terms:
316
317
318+isInjective :: TT n -> Bool
319+isInjective (P (DCon _ _) _ _) = True
320+isInjective (P (TCon _ _) _ _) = True
321+isInjective (Constant _) = True
322+isInjective (Set x) = True
323+isInjective (Bind _ (Pi _) sc) = True
324+isInjective (App f a) = isInjective f
325+isInjective _ = False
326+
317instantiate :: TT n -> TT n -> TT n
327instantiate :: TT n -> TT n -> TT n
318instantiate e = subst 0 where
328instantiate e = subst 0 where
319 subst i (V x) | i == x = e
329 subst i (V x) | i == x = e
src/Core/Unify.hs+25−8
@@ -4,16 +4,25 @@ import Core.TT
4import Core.Evaluate
4import Core.Evaluate
5
5
6import Control.Monad
6import Control.Monad
7+import Control.Monad.State
7import Debug.Trace
8import Debug.Trace
8
9
9-- Unification is applied inside the theorem prover. We're looking for holes
10-- Unification is applied inside the theorem prover. We're looking for holes
10-- which can be filled in, by matching one term's normal form against another.
11-- which can be filled in, by matching one term's normal form against another.
11−-- Returns a list of hole names paired with the term which solves them.
12+-- Returns a list of hole names paired with the term which solves them, and
13+-- a list of things which need to be injective.
12
14
15+-- terms which need to be injective, with the things we're trying to unify
16+-- at the time
17+type UInfo = [(TT Name, TT Name, TT Name)]
18+
13−unify :: Context -> Env -> TT Name -> TT Name -> TC [(Name, TT Name)]
19+unify :: Context -> Env -> TT Name -> TT Name -> TC ([(Name, TT Name)],
20+ UInfo)
14unify ctxt env topx topy
21unify ctxt env topx topy
22+ = case runStateT
15− = case un' False [] (normalise ctxt env topx) (normalise ctxt env topy) of
23+ (un' False [] (normalise ctxt env topx) (normalise ctxt env topy))
24+ [] of
16− OK v -> return (filter notTrivial v)
25+ OK (v, inj) -> return (filter notTrivial v, inj)
17 Error e -> tfail $ CantUnify topx topy e
26 Error e -> tfail $ CantUnify topx topy e
18 where
27 where
19 notTrivial (x, P _ x' _) = x /= x'
28 notTrivial (x, P _ x' _) = x /= x'
@@ -24,14 +33,22 @@ unify ctxt env topx topy
24 injective (App f a) = injective f
33 injective (App f a) = injective f
25 injective _ = False
34 injective _ = False
26
35
36+ notP (P _ _ _) = False
37+ notP _ = True
38+
39+ un' :: Bool -> [(Name, Name)] -> TT Name -> TT Name ->
40+ StateT UInfo
41+ TC [(Name, TT Name)]
27 un' fn bnames (P Bound x _) (P Bound y _)
42 un' fn bnames (P Bound x _) (P Bound y _)
28 | (x,y) `elem` bnames = return []
43 | (x,y) `elem` bnames = return []
29 un' fn bnames (P Bound x _) tm
44 un' fn bnames (P Bound x _) tm
30− | (not fn || injective tm)
45+ | holeIn env x = do i <- get
46+ when (notP tm && fn) $ put ((tm, topx, topy) : i)
31− && holeIn env x = return [(x, tm)]
47+ return [(x, tm)]
32 un' fn bnames tm (P Bound y _)
48 un' fn bnames tm (P Bound y _)
33− | (not fn || injective tm)
49+ | holeIn env y = do i <- get
50+ when (notP tm && fn) $ put ((tm, topx, topy) : i)
34− && holeIn env y = return [(y, tm)]
51+ return [(y, tm)]
35 un' fn bnames (V i) (P Bound x _)
52 un' fn bnames (V i) (P Bound x _)
36 | fst (bnames!!i) == x || snd (bnames!!i) == x = return []
53 | fst (bnames!!i) == x || snd (bnames!!i) == x = return []
37 un' fn bnames (P Bound x _) (V i)
54 un' fn bnames (P Bound x _) (V i)
src/Idris/Delaborate.hs+3
@@ -57,6 +57,9 @@ pshow i (Msg s) = s
57pshow i (CantUnify x y e) = "Can't unify " ++ show (delab i x)
57pshow i (CantUnify x y e) = "Can't unify " ++ show (delab i x)
58 ++ " with " ++ show (delab i y)
58 ++ " with " ++ show (delab i y)
59-- ++ "\n\t(" ++ pshow i e ++ ")"
59-- ++ "\n\t(" ++ pshow i e ++ ")"
60+pshow i (NotInjective p x y) = "Can't verify injectivity of " ++ show (delab i p) ++
61+ " when unifying " ++ show (delab i x) ++ " and " ++
62+ show (delab i y)
60pshow i (IncompleteTerm t) = "Incomplete term " ++ show t
63pshow i (IncompleteTerm t) = "Incomplete term " ++ show t
61pshow i UniverseError = "Universe inconsistency"
64pshow i UniverseError = "Universe inconsistency"
62pshow i ProgramLineComment = "Program line next to comment"
65pshow i ProgramLineComment = "Program line next to comment"
src/Idris/ElabTerm.hs+2
@@ -53,6 +53,8 @@ elab ist info pattern tcgen fn tm
53 = do elabE False tm
53 = do elabE False tm
54 when pattern -- convert remaining holes to pattern vars
54 when pattern -- convert remaining holes to pattern vars
55 mkPat
55 mkPat
56+ inj <- get_inj
57+ mapM_ checkInjective inj
56 where
58 where
57 isph arg = case getTm arg of
59 isph arg = case getTm arg of
58 Placeholder -> (True, priority arg)
60 Placeholder -> (True, priority arg)
src/Idris/Prover.hs+2−2
@@ -51,8 +51,8 @@ elabStep st e = do case runStateT e st of
51 fail (pshow i a)
51 fail (pshow i a)
52
52
53dumpState :: IState -> ProofState -> IO ()
53dumpState :: IState -> ProofState -> IO ()
54−dumpState ist (PS nm [] _ tm _ _ _ _ _ _ _ _) = putStrLn $ (show nm) ++ ": no more goals"
54+dumpState ist (PS nm [] _ tm _ _ _ _ _ _ _ _ _) = putStrLn $ (show nm) ++ ": no more goals"
55−dumpState ist ps@(PS nm (h:hs) _ tm _ _ i _ _ ctxy _ _)
55+dumpState ist ps@(PS nm (h:hs) _ tm _ _ _ i _ _ ctxy _ _)
56 = do let OK ty = goalAtFocus ps
56 = do let OK ty = goalAtFocus ps
57 let OK env = envAtFocus ps
57 let OK env = envAtFocus ps
58-- putStrLn $ "Other goals: " ++ show hs ++ "\n"
58-- putStrLn $ "Other goals: " ++ show hs ++ "\n"