fbb201c · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge branch 'hl-kw' into wip/tactical

fbb201cDavid Raymond Christiansen11 years ago

src/Idris/Delaborate.hs+4−2

compare with master

unifiedsplit

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

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

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

291 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

293pprintErr' i (CantConvert x_in y_in env) =

295pprintErr' i (CantConvert x_in y_in env) =

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

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

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

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

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

300 text "and" <>

302 text "and" <>

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

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

302 y)) <>

304 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

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

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

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

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

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

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

1928 = do solve

1929 returnUnit

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

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

1931+ = do hs <- get_holes

1932+ case hs of

1932− t <- goal

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

1933− fmap fst . checkClosed $

1934+ fmap fst . checkClosed $

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

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

1935− (reflectName h, reflect t)

1936+ (reflectName h, reflect t)

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

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

1939+

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

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

1937 = do hs <- get_holes

1941 = do hs <- get_holes

1938 fmap fst . checkClosed $

1942 fmap fst . checkClosed $

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

2153 datatypes <- get_datatypes

2157 datatypes <- get_datatypes

2154 env <- get_env

2158 env <- get_env

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

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

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

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

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

2157− (newProof recH ctxt datatypes goalTT)

2162+ ((newProof recH ctxt datatypes goalTT)

2163+ { nextname = nextname current_p})

2158 let tm_out = getProofTerm (pterm p)

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

2160 env' <- get_env

2168 env' <- get_env

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

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

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

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