b38bc03 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Add basic elaboration context tracking to unification

commitb38bc035c0921abd72b79ad2b9b25ea54f20ce5b authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateThu 20 Mar 2014, 10:02 (13 years ago) parentdaafe34

6 files changed+71−45

compare with master

unifiedsplit

src/Idris/Core/Elaborate.hs+3−3 src/Idris/Core/ProofState.hs+40−20 src/Idris/Core/Unify.hs+20−14 src/Idris/ElabDecls.hs+2−2 src/Idris/ElabTerm.hs+4−4 src/Idris/Prover.hs+2−2

src/Idris/Core/Elaborate.hs+3−3

@@ -627,7 +627,7 @@ no_errors tac err

627627 ps' <- get_probs

628628 if (length ps' > length ps) then

629629 case reverse ps' of

630− ((x,y,env,inerr,_) : _) ->

630+ ((x, y, env, inerr, while, _) : _) ->

631631 let env' = map (\(x, b) -> (x, binderTy b)) env in

632632 lift $ tfail $

633633 case err of

@@ -721,12 +721,12 @@ prunStateT pmax zok ps x s

721721 newpmax = if newps < 0 then 0 else newps in

722722 if (newpmax > pmax || (not zok && newps > 0)) -- length ps == 0 && newpmax > 0))

723723 then case reverse (problems p) of

724− ((_,_,_,e,_):_) -> Error e

724+ ((_,_,_,e,_,_):_) -> Error e

725725 else OK ((v, newpmax, problems p), s')

726726 Error e -> Error e

727727

728728qshow :: Fails -> String

729−qshow fs = show (map (\ (x, y, _, _, _) -> (x, y)) fs)

729+qshow fs = show (map (\ (x, y, _, _, _, _) -> (x, y)) fs)

730730

731731dumpprobs [] = ""

732732dumpprobs ((_,_,_,e):es) = show e ++ "\n" ++ dumpprobs es

src/Idris/Core/ProofState.hs+40−20

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

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

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

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

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

99 dropGiven, keepGiven) where

1010

1111import Idris.Core.Typecheck

@@ -39,7 +39,8 @@ data ProofState = PS { thname :: Name,

3939 context :: Context,

4040 plog :: String,

4141 unifylog :: Bool,

42− done :: Bool

42+ done :: Bool,

43+ while_elaborating :: [FailContext]

4344 }

4445

4546data Goal = GD { premises :: Env,

@@ -90,9 +91,9 @@ data Tactic = Attack

9091-- Some utilites on proof and tactic states

9192

9293instance Show ProofState where

93− show (PS nm [] _ _ tm _ _ _ _ _ _ _ _ _ _ _ _ _ _)

94+ show (PS nm [] _ _ tm _ _ _ _ _ _ _ _ _ _ _ _ _ _ _)

9495 = show nm ++ ": no more goals"

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

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

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

9798 wkenv = premises g in

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

@@ -115,9 +116,9 @@ instance Show ProofState where

115116 showG ps b = showEnv ps (binderTy b)

116117

117118instance Pretty ProofState OutputAnnotation where

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

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

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

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

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

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

122123 let wkEnv = premises g in

123124 text "Other goals" <+> colon <+> pretty hs <+>

@@ -148,12 +149,13 @@ hole _ = False

148149holeName i = sMN i "hole"

149150

150151qshow :: Fails -> String

151−qshow fs = show (map (\ (x, y, _, _, t) -> (t, x, y)) fs)

152+qshow fs = show (map (\ (x, y, _, _, _, t) -> (t, x, y)) fs)

152153

153154match_unify' :: Context -> Env -> TT Name -> TT Name ->

154155 StateT TState TC [(Name, TT Name)]

155156match_unify' ctxt env topx topy =

156157 do ps <- get

158+ let while = while_elaborating ps

157159 let dont = dontunify ps

158160 let inj = injective ps

159161 traceWhen (unifylog ps)

@@ -163,11 +165,11 @@ match_unify' ctxt env topx topy =

163165 ++ "\n"

164166 ++ "\n" ++ show (pterm ps) ++ "\n\n"

165167 ) $

166− case match_unify ctxt env topx topy inj (holes ps) of

168+ case match_unify ctxt env topx topy inj (holes ps) while of

167169 OK u -> do let (h, ns) = unified ps

168170 put (ps { unified = (h, u ++ ns) })

169171 return u

170− Error e -> do put (ps { problems = (topx, topy, env, e, Match) :

172+ Error e -> do put (ps { problems = (topx, topy, env, e, while, Match) :

171173 problems ps })

172174 return []

173175-- traceWhen (unifylog ps)

@@ -181,24 +183,25 @@ unify' :: Context -> Env -> TT Name -> TT Name ->

181183 StateT TState TC [(Name, TT Name)]

182184unify' ctxt env topx topy =

183185 do ps <- get

186+ let while = while_elaborating ps

184187 let dont = dontunify ps

185188 let inj = injective ps

186189 (u, fails) <- traceWhen (unifylog ps)

187190 ("Trying " ++ show (topx, topy) ++

188191 "\nNormalised " ++ show (normalise ctxt env topx,

189− normalise ctxt env topy) ++

192+ normalise ctxt env topy) ++

190193 " in " ++ show env ++

191194 "\nHoles: " ++ show (holes ps)

192− ++ "\nInjective: " ++ show (injective ps)

195+ ++ "\nInjective: " ++ show (injective ps)

193196 ++ "\n") $

194− lift $ unify ctxt env topx topy inj (holes ps)

197+ lift $ unify ctxt env topx topy inj (holes ps) while

195198 let notu = filter (\ (n, t) -> case t of

196199 P _ _ _ -> False

197200 _ -> n `elem` dont) u

198201 traceWhen (unifylog ps)

199202 ("Unified " ++ show (topx, topy) ++ " without " ++ show dont ++

200203 "\nSolved: " ++ show u ++ "\nNew problems: " ++ qshow fails

201− ++ "\nNot unified:\n" ++ show (notunified ps)

204+ ++ "\nNot unified:\n" ++ show (notunified ps)

202205 ++ "\nCurrent problems:\n" ++ qshow (problems ps)

203206-- ++ show (pterm ps)

204207 ++ "\n----------") $

@@ -221,6 +224,21 @@ unify' ctxt env topx topy =

221224 updateInj (_ : us) inj = updateInj us inj

222225 updateInj [] inj = inj

223226

227+now_elaborating :: Monad m => FC -> Name -> Name -> StateT TState m ()

228+now_elaborating fc f arg = do ps <- get

229+ put ps {

230+ while_elaborating = FailContext fc f arg : while_elaborating ps

231+ }

232+

233+done_elaborating :: Monad m => Name -> Name -> StateT TState m ()

234+done_elaborating f x = do ps <- get

235+ let while = while_elaborating ps

236+ let while' = dropUntil (\ (FailContext _ f' x') -> f == f' && x == x') while

237+ put ps { while_elaborating = while' }

238+ where dropUntil p [] = []

239+ dropUntil p (x:xs) | p x = xs

240+ | otherwise = dropUntil p xs

241+

224242getName :: Monad m => String -> StateT TState m Name

225243getName tag = do ps <- get

226244 let n = nextname ps

@@ -245,7 +263,7 @@ newProof n ctxt ty = let h = holeName 0

245263 (P Bound h ty')) ty [] (h, []) []

246264 Nothing [] []

247265 [] []

248− Nothing ctxt "" False False

266+ Nothing ctxt "" False False []

249267

250268type TState = ProofState -- [TacticAction])

251269type RunTactic = Context -> Env -> Term -> StateT TState TC Term

@@ -795,36 +813,38 @@ updateNotunified ns nu = up nu where

795813 up ((n, t) : nus) = let t' = updateSolved ns t in

796814 ((n, t') : up nus)

797815

816+updateProblems :: Context -> [(Name, TT Name)] -> Fails -> [Name] -> [Name]

817+ -> ([(Name, TT Name)], Fails)

798818updateProblems ctxt [] ps inj holes = ([], ps)

799819updateProblems ctxt ns ps inj holes = up ns ps where

800820 up ns [] = (ns, [])

801− up ns ((x, y, env, err, um) : ps) =

821+ up ns ((x, y, env, err, while, um) : ps) =

802822 let x' = updateSolved ns x

803823 y' = updateSolved ns y

804824 err' = updateError ns err

805825 env' = updateEnv ns env in

806826-- trace ("Updating " ++ show (x',y')) $

807− case unify ctxt env' x' y' inj holes of

827+ case unify ctxt env' x' y' inj holes while of

808828 OK (v, []) -> -- trace ("Added " ++ show v ++ " from " ++ show (x', y')) $

809829 up (ns ++ v) ps

810830 e -> -- trace ("Failed " ++ show e) $

811831 let (ns', ps') = up ns ps in

812− (ns', (x',y',env',err', um) : ps')

832+ (ns', (x',y',env',err', while, um) : ps')

813833

814834-- attempt to solve remaining problems with match_unify

815835matchProblems all ns ctxt ps inj holes = up ns ps where

816836 up ns [] = (ns, [])

817− up ns ((x, y, env, err, um) : ps)

837+ up ns ((x, y, env, err, while, um) : ps)

818838 | all || um == Match =

819839 let x' = updateSolved ns x

820840 y' = updateSolved ns y

821841 err' = updateError ns err

822842 env' = updateEnv ns env in

823− case match_unify ctxt env' x' y' inj holes of

843+ case match_unify ctxt env' x' y' inj holes while of

824844 OK v -> -- trace ("Added " ++ show v ++ " from " ++ show (x', y')) $

825845 up (ns ++ v) ps

826846 _ -> let (ns', ps') = up ns ps in

827− (ns', (x',y',env',err',um) : ps')

847+ (ns', (x', y', env', err', while, um) : ps')

828848 up ns (p : ps) = let (ns', ps') = up ns ps in

829849 (ns', p : ps')

830850

src/Idris/Core/Unify.hs+20−14

@@ -1,6 +1,6 @@

11{-# LANGUAGE PatternGuards #-}

3−module Idris.Core.Unify(match_unify, unify, Fails, FailAt(..)) where

3+module Idris.Core.Unify(match_unify, unify, Fails, FailContext(..), FailAt(..)) where

55import Idris.Core.TT

66import Idris.Core.Evaluate

@@ -21,8 +21,14 @@ import Debug.Trace

2121data FailAt = Match | Unify

2222 deriving (Show, Eq)

2323

24+data FailContext = FailContext { fail_sourceloc :: FC,

25+ fail_fn :: Name,

26+ fail_param :: Name

27+ }

28+ deriving (Eq, Show)

29+

2430type Injs = [(TT Name, TT Name, TT Name)]

25−type Fails = [(TT Name, TT Name, Env, Err, FailAt)]

31+type Fails = [(TT Name, TT Name, Env, Err, [FailContext], FailAt)]

2632

2733data UInfo = UI Int Fails

2834 deriving Show

@@ -34,10 +40,10 @@ data UResult a = UOK a

3440-- Solve metavariables by matching terms against each other

3541-- Not really unification, of course!

3642

37−match_unify :: Context -> Env -> TT Name -> TT Name -> [Name] -> [Name] ->

43+match_unify :: Context -> Env -> TT Name -> TT Name -> [Name] -> [Name] -> [FailContext] ->

3844 TC [(Name, TT Name)]

39−match_unify ctxt env topx topy inj holes =

40− case runStateT (un [] (renameBindersTm env topx)

45+match_unify ctxt env topx topy inj holes from =

46+ case runStateT (un [] (renameBindersTm env topx)

4147 (renameBindersTm env topy)) (UI 0 []) of

4248 OK (v, UI _ []) -> return (map (renameBinders env) (trimSolutions v))

4349 res ->

@@ -86,7 +92,7 @@ match_unify ctxt env topx topy inj holes =

8692 let err = CantUnify r

8793 topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s

8894 if (not r) then lift $ tfail err

89− else do put (UI s ((x, y, env, err, Match) : f))

95+ else do put (UI s ((x, y, env, err, from, Match) : f))

9096 lift $ tfail err

9197

9298

@@ -100,7 +106,7 @@ match_unify ctxt env topx topy inj holes =

100106 let err = CantUnify r topx topy

101107 (CantUnify r (binderTy x) (binderTy y) (Msg "") (errEnv env) s)

102108 (errEnv env) s

103− put (UI s ((binderTy x, binderTy y, env, err, Match) : f))

109+ put (UI s ((binderTy x, binderTy y, env, err, from, Match) : f))

104110 return []

105111

106112 -- TODO: there's an annoying amount of repetition between this and the

@@ -113,7 +119,7 @@ match_unify ctxt env topx topy inj holes =

113119 let r = recoverable x y

114120 let err = CantUnify r

115121 topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s

116− put (UI s ((x, y, env, err, Match) : f))

122+ put (UI s ((x, y, env, err, from, Match) : f))

117123 lift $ tfail err

118124 combine bnames as [] = return as

119125 combine bnames as ((n, t) : bs)

@@ -188,9 +194,9 @@ expandLets env (x, tm) = (x, doSubst (reverse env) tm)

188194 = doSubst env tm

189195

190196

191−unify :: Context -> Env -> TT Name -> TT Name -> [Name] -> [Name] ->

197+unify :: Context -> Env -> TT Name -> TT Name -> [Name] -> [Name] -> [FailContext] ->

192198 TC ([(Name, TT Name)], Fails)

193−unify ctxt env topx topy inj holes =

199+unify ctxt env topx topy inj holes from =

194200-- trace ("Unifying " ++ show (topx, topy)) $

195201 -- don't bother if topx and topy are different at the head

196202 case runStateT (un False [] (renameBindersTm env topx)

@@ -367,7 +373,7 @@ unify ctxt env topx topy inj holes =

367373 let err = CantUnify r

368374 topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s

369375 if (not r) then lift $ tfail err

370− else do put (UI s ((x, y, env, err, Unify) : f))

376+ else do put (UI s ((x, y, env, err, from, Unify) : f))

371377 return [] -- lift $ tfail err

372378

373379 unApp fn bnames appx@(App fx ax) appy@(App fy ay)

@@ -466,7 +472,7 @@ unify ctxt env topx topy inj holes =

466472 let r = recoverable x y

467473 let err = CantUnify r

468474 topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s

469− put (UI s ((topx, topy, env, err, Unify) : f))

475+ put (UI s ((topx, topy, env, err, from, Unify) : f))

470476 return []

471477

472478 -- shortcut failure, if we *know* nothing can fix it

@@ -474,7 +480,7 @@ unify ctxt env topx topy inj holes =

474480 let r = recoverable x y

475481 let err = CantUnify r

476482 topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s

477− put (UI s ((topx, topy, env, err, Unify) : f))

483+ put (UI s ((topx, topy, env, err, from, Unify) : f))

478484 lift $ tfail err

479485

480486

@@ -497,7 +503,7 @@ unify ctxt env topx topy inj holes =

497503 let err = CantUnify r topx topy

498504 (CantUnify r (binderTy x) (binderTy y) (Msg "") (errEnv env) s)

499505 (errEnv env) s

500− put (UI s ((binderTy x, binderTy y, env, err, Unify) : f))

506+ put (UI s ((binderTy x, binderTy y, env, err, from, Unify) : f))

501507 return [] -- lift $ tfail err

502508

503509 checkCycle ns p@(x, P _ _ _) = return [p]

src/Idris/ElabDecls.hs+2−2

@@ -1389,7 +1389,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

13891389 inj <- get_inj

13901390 return (res, probs, inj))

13911391

1392− when inf $ addTyInfConstraints fc (map (\(x,y,_,_,_) -> (x,y)) probs)

1392+ when inf $ addTyInfConstraints fc (map (\(x,y,_,_,_,_) -> (x,y)) probs)

13931393

13941394 let lhs_tm = orderPats (getInferTerm lhs')

13951395 let lhs_ty = getInferType lhs'

@@ -1453,7 +1453,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

14531453 probs <- get_probs

14541454 return (tm, ds, is, probs))

14551455

1456− when inf $ addTyInfConstraints fc (map (\(x,y,_,_,_) -> (x,y)) probs)

1456+ when inf $ addTyInfConstraints fc (map (\(x,y,_,_,_,_) -> (x,y)) probs)

14571457

14581458 logLvl 5 "DONE CHECK"

14591459 logLvl 2 $ "---> " ++ show rhs'

src/Idris/ElabTerm.hs+4−4

@@ -81,8 +81,8 @@ build ist info pattern opts fn tm

8181 probs <- get_probs

8282 case probs of

8383 [] -> return ()

84− ((_,_,_,e,_):es) -> if inf then return ()

85− else lift (Error e)

84+ ((_,_,_,e,_,_):es) -> if inf then return ()

85+ else lift (Error e)

8686 is <- getAux

8787 tt <- get_term

8888 let (tm, ds) = runState (collectDeferred (Just fn) tt) []

@@ -109,8 +109,8 @@ buildTC ist info pattern opts fn tm

109109 tm <- get_term

110110 case probs of

111111 [] -> return ()

112− ((_,_,_,e,_):es) -> if inf then return ()

113− else lift (Error e)

112+ ((_,_,_,e,_,_):es) -> if inf then return ()

113+ else lift (Error e)

114114 is <- getAux

115115 tt <- get_term

116116 let (tm, ds) = runState (collectDeferred (Just fn) tt) []

src/Idris/Prover.hs+2−2

@@ -89,10 +89,10 @@ elabStep st e = do case runStateT e st of

8989 Error a -> ierror a

9090

9191dumpState :: IState -> ProofState -> Idris ()

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

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

9393 do rendered <- iRender $ prettyName False [] nm <> colon <+> text "No more goals."

9494 iputGoal rendered

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

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

9696 let OK ty = goalAtFocus ps

9797 let OK env = envAtFocus ps

9898 let state = prettyOtherGoals hs <> line <>