fbb201c · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge branch 'hl-kw' into wip/tactical

commitfbb201c5ffdf144efb5b88226a20d82911c9f6e0 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateThu 20 Aug 2015, 22:40 (11 years ago) parentba3fab0 d741a30

2 files changed+20−10

compare with master

unifiedsplit

src/Idris/Delaborate.hs+4−2 src/Idris/Elab/Term.hs+16−8

src/Idris/Delaborate.hs+4−2

@@ -289,7 +289,9 @@ pprintErr' i (CantUnify _ (x_in, xprov) (y_in, yprov) e sc s) =

289289 CantUnify _ (x_in', _) (y_in',_) _ _ _ | x_in == x_in' && y_in == y_in' -> empty

290290 _ -> line <> line <> text "Specifically:" <>

291291 indented (pprintErr' i e) <>

292− if (opt_errContext (idris_options i)) then showSc i sc else empty

292+ if (opt_errContext (idris_options i))

293+ then text "Unification failure" <$> showSc i sc

294+ else empty

293295pprintErr' i (CantConvert x_in y_in env) =

294296 let (x_ns, y_ns, nms) = renameMNs x_in y_in

295297 (x, y) = addImplicitDiffs (delabSugared i (flagUnique x_ns))

@@ -300,7 +302,7 @@ pprintErr' i (CantConvert x_in y_in env) =

300302 text "and" <>

301303 indented (annTm y_ns (pprintTerm' i (map (\ (n, b) -> (n, False)) env)

302304 y)) <>

303− if (opt_errContext (idris_options i)) then line <> showSc i env else empty

305+ if (opt_errContext (idris_options i)) then line <> text "Conversion failure" <$> showSc i env else empty

304306 where flagUnique (Bind n (Pi i t k@(UType u)) sc)

305307 = App Complete (P Ref (sUN (show u)) Erased)

306308 (Bind n (Pi i (flagUnique t) k) (flagUnique sc))

src/Idris/Elab/Term.hs+16−8

@@ -1928,11 +1928,15 @@ runElabAction ist fc env tm ns = do tm' <- eval tm

19281928 = do solve

19291929 returnUnit

19301930 | n == tacN "prim__Goal", [] <- args

1931− = do (h:_) <- get_holes

1932− t <- goal

1933− fmap fst . checkClosed $

1934− rawPair (Var (reflm "TTName"), Var (reflm "TT"))

1935− (reflectName h, reflect t)

1931+ = do hs <- get_holes

1932+ case hs of

1933+ (h : _) -> do t <- goal

1934+ fmap fst . checkClosed $

1935+ rawPair (Var (reflm "TTName"), Var (reflm "TT"))

1936+ (reflectName h, reflect t)

1937+ [] -> lift . tfail . Msg $

1938+ "Elaboration is complete. There are no goals."

1939+

19361940 | n == tacN "prim__Holes", [] <- args

19371941 = do hs <- get_holes

19381942 fmap fst . checkClosed $

@@ -2153,10 +2157,14 @@ runElabAction ist fc env tm ns = do tm' <- eval tm

21532157 datatypes <- get_datatypes

21542158 env <- get_env

21552159 (_, ES (p, aux') _ _) <-

2156− lift $ runElab aux (runElabAction ist fc [] script ns)

2157− (newProof recH ctxt datatypes goalTT)

2160+ do (ES (current_p, _) _ _) <- get

2161+ lift $ runElab aux (runElabAction ist fc [] script ns)

2162+ ((newProof recH ctxt datatypes goalTT)

2163+ { nextname = nextname current_p})

21582164 let tm_out = getProofTerm (pterm p)

2159− updateAux $ const aux'

2165+ do (ES (prf, _) s e) <- get

2166+ let p' = prf { nextname = nextname p }

2167+ put (ES (p', aux') s e)

21602168 env' <- get_env

21612169 (tm, ty, _) <- lift $ recheck ctxt env (forget tm_out) tm_out

21622170 let (tm', ty') = (reflect tm, reflect ty)