bd793e2 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Better elaboration of Sigma (for better error messages)

bd793e2Edwin Brady15 years ago

src/Idris/AbsSyntax.hs+2

compare with master

unifiedsplit

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

526 ni env (PHidden tm) = ni env tm

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

528 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

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

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

530 ni env _ = []

531 ni env _ = []

531

532

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

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

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

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

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

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

545 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

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

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

546 ni env (PHidden tm) = ni env tm

548 ni env (PHidden tm) = ni env tm

547 ni env _ = []

549 ni env _ = []

src/Idris/ElabDecls.hs+12−7

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

527 pimp (MN 0 "B") Placeholder,

528 pexp l, pexp r]))

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

530+ = case t of

531+ Placeholder -> try asType asValue

532+ _ -> asType

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

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

531 [pexp t,

534 [pexp t,

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

535+ pexp (PLam n Placeholder r)])

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

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

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

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

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

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

536− pexp l, pexp r]))

539+ pexp l, pexp r])

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

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

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

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

539 pimp (MN 0 "P") Placeholder,

542 pimp (MN 0 "P") Placeholder,

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

559 elab' (PPi _ n ty sc)

562 elab' (PPi _ n ty sc)

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

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

561 claim tyn (RSet 0)

564 claim tyn (RSet 0)

565+ n' <- case n of

562− n' <- unique_hole n

566+ MN _ _ -> unique_hole n

567+ _ -> return n

563 forall n' (Var tyn)

568 forall n' (Var tyn)

564 focus tyn

569 focus tyn

565 elabE ty

570 elabE ty