127db00 · Idris-dev · git.iko.soy

151 let dont = dontunify ps

152 let inj = injective ps

153 traceWhen (unifylog ps)

154− ("Matching " ++ show (topx, topy) ++

154+ ("Matching " ++ show (topx, topy) ++

155 " in " ++ show env ++

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

157− ++ "\n"

157+ ++ "\n"

158 ++ "\n" ++ show (getProofTerm (pterm ps)) ++ "\n\n"

159 ) $

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

170 return []

171-- traceWhen (unifylog ps)

172-- ("Matched " ++ show (topx, topy) ++ " without " ++ show dont ++

173−-- "\nSolved: " ++ show u

173+-- "\nSolved: " ++ show u

174-- ++ "\nCurrent problems:\n" ++ qshow (problems ps)

175-- -- ++ show (pterm ps)

176-- ++ "\n----------") $

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

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

205 ++ "\n") $

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

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

207 (map fst (notunified ps)) while

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

209 P _ _ _ -> False

416 Nothing -> error ("deferType can't find " ++ show n)

417

418regret :: RunTactic

419−regret ctxt env (Bind x (Hole t) sc) | noOccurrence x sc =

419+regret ctxt env (Bind x (Hole t) sc) | noOccurrence x sc =

420 do action (\ps -> let hs = holes ps in

421 ps { holes = hs \\ [x] })

422 return sc

495 notunified = updateNotunified [(x,val)]

496 (notunified ps),

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

498− let tm' = subst x val sc in

498+ let tm' = subst x val sc in

499 return tm'

500solve _ _ h@(Bind x t sc)

501 = do ps <- get

504 _ -> lift $ tfail (IncompleteTerm h)

505 where findType x (Bind n (Let t v) sc)

506 = findType x v `mplus` findType x sc

507− findType x (Bind n t sc)

507+ findType x (Bind n t sc)

508 | P _ x' _ <- binderTy t, x == x' = Just n

509 | otherwise = findType x sc

510 findType x _ = Nothing

553forall n ty ctxt env _ = fail "Can't pi bind here"

554

555patvar :: Name -> RunTactic

556−patvar n ctxt env (Bind x (Hole t) sc) =

556+patvar n ctxt env (Bind x (Hole t) sc) =

557 do action (\ps -> ps { holes = traceWhen (unifylog ps) ("Dropping pattern hole " ++ show x) $

558 holes ps \\ [x],

559 solved = Just (x, P Bound n t),

590 [lt, l, r, p, tmv, xp]))

591 (scv, sct) <- lift $ check ctxt env sc

592 return scv

593− _ -> lift $ tfail (NotEquality tmv tmt')

593+ _ -> lift $ tfail (NotEquality tmv tmt')

594 where rname = sMN 0 "replaced"

595rewrite _ _ _ _ = fail "Can't rewrite here"

596

769updateError [] err = err

770updateError ns (At f e) = At f (updateError ns e)

771updateError ns (Elaborating s n e) = Elaborating s n (updateError ns e)

772−updateError ns (ElaboratingArg f a env e)

772+updateError ns (ElaboratingArg f a env e)

773 = ElaboratingArg f a env (updateError ns e)

774updateError ns (CantUnify b l r e xs sc)

775 = CantUnify b (updateSolvedTerm ns l) (updateSolvedTerm ns r) (updateError ns e) xs sc

777

778solveInProblems x val [] = []

779solveInProblems x val ((l, r, env, err) : ps)

780− = ((psubst x val l, psubst x val r,

780+ = ((psubst x val l, psubst x val r,

781 updateEnv [(x, val)] env, err) : solveInProblems x val ps)

782

783mergeNotunified :: Env -> [(Name, Term)] -> ([(Name, Term)], Fails)

785 mnu [] ns_acc ps_acc = (reverse ns_acc, reverse ps_acc)

786 mnu ((n, t):ns) ns_acc ps_acc

787 | Just t' <- lookup n ns, t /= t'

788− = mnu ns ((n,t') : ns_acc)

788+ = mnu ns ((n,t') : ns_acc)

789 ((t,t',env,CantUnify True t t' (Msg "") [] 0, [],Match) : ps_acc)

790 | otherwise = mnu ns ((n,t) : ns_acc) ps_acc

791

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

797

798-- FIXME: Why not just pass the whole proof state?

799+-- Issue #1716 on the issue tracker.

800+-- https://github.com/idris-lang/Idris-dev/issues/1716

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

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

800 -> ([(Name, TT Name)], Fails)

802 -> ([(Name, TT Name)], Fails)

801-- updateProblems ctxt [] ps inj holes = ([], ps)

803-- updateProblems ctxt [] ps inj holes = ([], ps)

806 y' = updateSolvedTerm ns y

808 y' = updateSolvedTerm ns y

807 err' = updateError ns err

809 err' = updateError ns err

808 env' = updateEnv ns env in

810 env' = updateEnv ns env in

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

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

810 case unify ctxt env' x' y' inj holes usupp while of

812 case unify ctxt env' x' y' inj holes usupp while of

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

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

812 up (ns ++ v) ps

814 up (ns ++ v) ps

867 return (ps' { previous = Just ps, plog = "" }, plog ps')

869 return (ps' { previous = Just ps, plog = "" }, plog ps')

868processTactic (ComputeLet n) ps

870processTactic (ComputeLet n) ps

869 = return (ps { pterm = mkProofTerm $

871 = return (ps { pterm = mkProofTerm $

870− computeLet (context ps) n

872+ computeLet (context ps) n

871 (getProofTerm (pterm ps)) }, "")

873 (getProofTerm (pterm ps)) }, "")

872processTactic UnifyProblems ps

874processTactic UnifyProblems ps

873 = let (ns', probs') = updateProblems (context ps) []

875 = let (ns', probs') = updateProblems (context ps) []