1823cf9 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Postpone injectivity check until after unification

commit1823cf9e09f1ec3baa2efd553dfa53e930b52c15 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateWed 4 Jan 2012, 10:23 (15 years ago) parent7932e28

7 files changed+69−16

compare with master

unifiedsplit

src/Core/Elaborate.hs+8 src/Core/ProofState.hs+19−6 src/Core/TT.hs+10 src/Core/Unify.hs+25−8 src/Idris/Delaborate.hs+3 src/Idris/ElabTerm.hs+2 src/Idris/Prover.hs+2−2

src/Core/Elaborate.hs+8

@@ -111,6 +111,14 @@ get_deferred :: Elab [Name]

111111get_deferred = do ES p _ _ <- get

112112 return (deferred p)

113113

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+

114122-- get instance argument names

115123get_instances :: Elab [Name]

116124get_instances = do ES p _ _ <- get

src/Core/ProofState.hs+19−6

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

2323 pterm :: Term, -- current proof term

2424 ptype :: Type, -- original goal

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

26+ injective :: [(Term, Term, Term)],

2627 deferred :: [Name], -- names we'll need to define

2728 instances :: [Name], -- instance arguments (for type classes)

2829 previous :: Maybe ProofState, -- for undo

@@ -68,8 +69,8 @@ data Tactic = Attack

6869-- Some utilites on proof and tactic states

6970

7071instance Show ProofState where

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

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

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

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

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

7475 wkenv = premises g in

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

@@ -116,7 +117,7 @@ addLog str = action (\ps -> ps { plog = plog ps ++ str ++ "\n" })

116117newProof :: Name -> Context -> Type -> ProofState

117118newProof n ctxt ty = let h = holeName 0

118119 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, []) []

120121 [] []

121122 Nothing ctxt "" False

122123

@@ -243,6 +244,10 @@ defer n ctxt env (Bind x (Hole t) (P nt x' ty)) | x == x' =

243244regret :: RunTactic

244245regret = undefined

245246

247+addInj :: [(Term, Term, Term)] -> StateT TState TC ()

248+addInj inj = do ps <- get

249+ put (ps { injective = inj ++ injective ps })

250+

246251exact :: Raw -> RunTactic

247252exact guess ctxt env (Bind x (Hole ty) sc) =

248253 do (val, valty) <- lift $ check ctxt env guess

@@ -256,7 +261,8 @@ fill :: Raw -> RunTactic

256261fill guess ctxt env (Bind x (Hole ty) sc) =

257262 do (val, valty) <- lift $ check ctxt env guess

258263 s <- get

259− ns <- lift $ unify ctxt env valty ty

264+ (ns, inj) <- lift $ unify ctxt env valty ty

265+ addInj inj

260266 ps <- get

261267 let (uh, uns) = unified ps

262268 put (ps { unified = (uh, uns ++ ns) })

@@ -274,7 +280,8 @@ complete_fill :: RunTactic

274280complete_fill ctxt env (Bind x (Guess ty val) sc) =

275281 do let guess = forget val

276282 (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

278285 ps <- get

279286 let (uh, uns) = unified ps

280287 put (ps { unified = (uh, uns ++ ns) })

@@ -302,7 +309,8 @@ introTy ty mn ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =

302309-- ns <- lift $ unify ctxt env tyv t'

303310 case t' of

304311 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

306314 ps <- get

307315 let (uh, uns) = unified ps

308316 put (ps { unified = (uh, uns ++ ns) })

@@ -405,12 +413,15 @@ start_unify :: Name -> RunTactic

405413start_unify n ctxt env tm = do action (\ps -> ps { unified = (n, []) })

406414 return tm

407415

416+tmap f (a, b, c) = (f a, b, c)

417+

408418solve_unified :: RunTactic

409419solve_unified ctxt env tm =

410420 do ps <- get

411421 let (_, ns) = unified ps

412422 action (\ps -> ps { holes = holes ps \\ map fst ns })

413423 action (\ps -> ps { pterm = updateSolved ns (pterm ps) })

424+ action (\ps -> ps { injective = map (tmap (updateSolved ns)) (injective ps) })

414425 return (updateSolved ns tm)

415426

416427updateSolved xs (Bind n (Hole ty) t)

@@ -437,6 +448,8 @@ processTactic EndUnify ps = let (h, ns) = unified ps

437448 tm' = updateSolved ns (pterm ps) in

438449 return (ps { pterm = tm',

439450 unified = (h, []),

451+ injective = map (tmap (updateSolved ns))

452+ (injective ps),

440453 holes = holes ps \\ map fst ns }, "")

441454processTactic (Reorder n) ps

442455 = do ps' <- execStateT (tactic (Just n) reorder_claims) ps

src/Core/TT.hs+10

@@ -39,6 +39,7 @@ instance Show FC where

3939

4040data Err = Msg String

4141 | CantUnify Term Term Err

42+ | NotInjective Term Term Term

4243 | IncompleteTerm Term

4344 | UniverseError

4445 | ProgramLineComment

@@ -314,6 +315,15 @@ convEq _ _ = return False

314315

315316-- A few handy operations on well typed terms:

316317

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+

317327instantiate :: TT n -> TT n -> TT n

318328instantiate e = subst 0 where

319329 subst i (V x) | i == x = e

src/Core/Unify.hs+25−8

@@ -4,16 +4,25 @@ import Core.TT

44import Core.Evaluate

66import Control.Monad

7+import Control.Monad.State

78import Debug.Trace

910-- Unification is applied inside the theorem prover. We're looking for holes

1011-- 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.

1214

13−unify :: Context -> Env -> TT Name -> TT Name -> TC [(Name, TT Name)]

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+

19+unify :: Context -> Env -> TT Name -> TT Name -> TC ([(Name, TT Name)],

20+ UInfo)

1421unify ctxt env topx topy

15− = case un' False [] (normalise ctxt env topx) (normalise ctxt env topy) of

16− OK v -> return (filter notTrivial v)

22+ = case runStateT

23+ (un' False [] (normalise ctxt env topx) (normalise ctxt env topy))

24+ [] of

25+ OK (v, inj) -> return (filter notTrivial v, inj)

1726 Error e -> tfail $ CantUnify topx topy e

1827 where

1928 notTrivial (x, P _ x' _) = x /= x'

@@ -24,14 +33,22 @@ unify ctxt env topx topy

2433 injective (App f a) = injective f

2534 injective _ = False

2635

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)]

2742 un' fn bnames (P Bound x _) (P Bound y _)

2843 | (x,y) `elem` bnames = return []

2944 un' fn bnames (P Bound x _) tm

30− | (not fn || injective tm)

31− && holeIn env x = return [(x, tm)]

45+ | holeIn env x = do i <- get

46+ when (notP tm && fn) $ put ((tm, topx, topy) : i)

47+ return [(x, tm)]

3248 un' fn bnames tm (P Bound y _)

33− | (not fn || injective tm)

34− && holeIn env y = return [(y, tm)]

49+ | holeIn env y = do i <- get

50+ when (notP tm && fn) $ put ((tm, topx, topy) : i)

51+ return [(y, tm)]

3552 un' fn bnames (V i) (P Bound x _)

3653 | fst (bnames!!i) == x || snd (bnames!!i) == x = return []

3754 un' fn bnames (P Bound x _) (V i)

src/Idris/Delaborate.hs+3

@@ -57,6 +57,9 @@ pshow i (Msg s) = s

5757pshow i (CantUnify x y e) = "Can't unify " ++ show (delab i x)

5858 ++ " with " ++ show (delab i y)

5959-- ++ "\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)

6063pshow i (IncompleteTerm t) = "Incomplete term " ++ show t

6164pshow i UniverseError = "Universe inconsistency"

6265pshow i ProgramLineComment = "Program line next to comment"

src/Idris/ElabTerm.hs+2

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

5353 = do elabE False tm

5454 when pattern -- convert remaining holes to pattern vars

5555 mkPat

56+ inj <- get_inj

57+ mapM_ checkInjective inj

5658 where

5759 isph arg = case getTm arg of

5860 Placeholder -> (True, priority arg)

src/Idris/Prover.hs+2−2

@@ -51,8 +51,8 @@ elabStep st e = do case runStateT e st of

5151 fail (pshow i a)

5252

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

54−dumpState ist (PS nm [] _ tm _ _ _ _ _ _ _ _) = putStrLn $ (show nm) ++ ": no more goals"

55−dumpState ist ps@(PS nm (h:hs) _ tm _ _ i _ _ ctxy _ _)

54+dumpState ist (PS nm [] _ tm _ _ _ _ _ _ _ _ _) = putStrLn $ (show nm) ++ ": no more goals"

55+dumpState ist ps@(PS nm (h:hs) _ tm _ _ _ i _ _ ctxy _ _)

5656 = do let OK ty = goalAtFocus ps

5757 let OK env = envAtFocus ps

5858-- putStrLn $ "Other goals: " ++ show hs ++ "\n"