bd793e2 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Better elaboration of Sigma (for better error messages)

commitbd793e2603ddf1ca7ec23ead380cddd4b6af1e21 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateFri 18 Nov 2011, 13:36 (15 years ago) parent1807c65

2 files changed+14−7

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+2 src/Idris/ElabDecls.hs+12−7

src/Idris/AbsSyntax.hs+2

@@ -526,6 +526,7 @@ allNamesIn tm = nub $ ni [] tm

526526 ni env (PHidden tm) = ni env tm

527527 ni env (PEq _ l r) = ni env l ++ ni env r

528528 ni env (PPair _ l r) = ni env l ++ ni env r

529+ ni env (PDPair _ (PRef _ n) t r) = ni env t ++ ni (n:env) r

529530 ni env (PDPair _ l t r) = ni env l ++ ni env t ++ ni env r

530531 ni env _ = []

531532

@@ -542,6 +543,7 @@ namesIn ist tm = nub $ ni [] tm

542543 ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc

543544 ni env (PEq _ l r) = ni env l ++ ni env r

544545 ni env (PPair _ l r) = ni env l ++ ni env r

546+ ni env (PDPair _ (PRef _ n) t r) = ni env t ++ ni (n:env) r

545547 ni env (PDPair _ l t r) = ni env l ++ ni env t ++ ni env r

546548 ni env (PHidden tm) = ni env tm

547549 ni env _ = []

src/Idris/ElabDecls.hs+12−7

@@ -527,13 +527,16 @@ elab ist info pattern tm

527527 pimp (MN 0 "B") Placeholder,

528528 pexp l, pexp r]))

529529 elab' (PDPair fc l@(PRef _ n) t r)

530− = try (elab' (PApp fc (PRef fc sigmaTy)

530+ = case t of

531+ Placeholder -> try asType asValue

532+ _ -> asType

533+ where asType = elab' (PApp fc (PRef fc sigmaTy)

531534 [pexp t,

532− pexp (PLam n Placeholder r)]))

533− (elab' (PApp fc (PRef fc existsCon)

534− [pimp (MN 0 "a") t,

535− pimp (MN 0 "P") Placeholder,

536− pexp l, pexp r]))

535+ pexp (PLam n Placeholder r)])

536+ asValue = elab' (PApp fc (PRef fc existsCon)

537+ [pimp (MN 0 "a") t,

538+ pimp (MN 0 "P") Placeholder,

539+ pexp l, pexp r])

537540 elab' (PDPair fc l t r) = elab' (PApp fc (PRef fc existsCon)

538541 [pimp (MN 0 "a") t,

539542 pimp (MN 0 "P") Placeholder,

@@ -559,7 +562,9 @@ elab ist info pattern tm

559562 elab' (PPi _ n ty sc)

560563 = do attack; tyn <- unique_hole (MN 0 "ty")

561564 claim tyn (RSet 0)

562− n' <- unique_hole n

565+ n' <- case n of

566+ MN _ _ -> unique_hole n

567+ _ -> return n

563568 forall n' (Var tyn)

564569 focus tyn

565570 elabE ty