8984d49 · Idris-dev · git.iko.soy

src/Idris/AbsSyntax.hs−3

compare with master

unifiedsplit

@@ -1140,7 +1140,6 @@ getPriority i tm = 1 -- pri tm

1140 [] -> 0 -- must be locally bound, if it's not an error...

1141 pri (PPi _ _ x y) = max 5 (max (pri x) (pri y))

1142 pri (PTrue _ _) = 0

1143− pri (PRefl _ _) = 1

1144 pri (PEq _ _ _ l r) = max 1 (max (pri l) (pri r))

1143 pri (PEq _ _ _ l r) = max 1 (max (pri l) (pri r))

1145 pri (PRewrite _ l r _) = max 1 (max (pri l) (pri r))

1144 pri (PRewrite _ l r _) = max 1 (max (pri l) (pri r))

1146 pri (PApp _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))

1145 pri (PApp _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))

@@ -1608,7 +1607,6 @@ addImpl' inpat env infns imp_meths ist ptm

1608 ai qq env ds (PHidden tm) = PHidden (ai qq env ds tm)

1607 ai qq env ds (PHidden tm) = PHidden (ai qq env ds tm)

1609 -- Don't do PProof or PTactics since implicits get added when scope is

1608 -- Don't do PProof or PTactics since implicits get added when scope is

1610 -- properly known in ElabTerm.runTac

1609 -- properly known in ElabTerm.runTac

1611− ai qq env ds (PRefl fc tm) = PRefl fc (ai qq env ds tm)

1612 ai qq env ds (PUnifyLog tm) = PUnifyLog (ai qq env ds tm)

1610 ai qq env ds (PUnifyLog tm) = PUnifyLog (ai qq env ds tm)

1613 ai qq env ds (PNoImplicits tm) = PNoImplicits (ai qq env ds tm)

1611 ai qq env ds (PNoImplicits tm) = PNoImplicits (ai qq env ds tm)

1614 ai qq env ds (PQuasiquote tm g) = PQuasiquote (ai True env ds tm)

1612 ai qq env ds (PQuasiquote tm g) = PQuasiquote (ai True env ds tm)

@@ -1952,7 +1950,6 @@ matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where

1952 match (PQuote _) _ = return []

1950 match (PQuote _) _ = return []

1953 match (PProof _) _ = return []

1951 match (PProof _) _ = return []

1954 match (PTactics _) _ = return []

1952 match (PTactics _) _ = return []

1955− match (PRefl _ _) (PRefl _ _) = return []

1956 match (PResolveTC _) (PResolveTC _) = return []

1953 match (PResolveTC _) (PResolveTC _) = return []

1957 match (PTrue _ _) (PTrue _ _) = return []

1954 match (PTrue _ _) (PTrue _ _) = return []

1958 match (PReturn _) (PReturn _) = return []

1955 match (PReturn _) (PReturn _) = return []

src/Idris/AbsSyntaxTree.hs−4

@@ -818,7 +818,6 @@ data PTerm = PQuote Raw -- ^ Inclusion of a core term into the high-level langua

818 | PIfThenElse FC PTerm PTerm PTerm -- ^ Conditional expressions - elaborated to an overloading of ifThenElse

819 | PCase FC PTerm [(PTerm, PTerm)] -- ^ A case expression. Args are source location, scrutinee, and a list of pattern/RHS pairs

820 | PTrue FC PunInfo -- ^ Unit type..?

821− | PRefl FC PTerm -- ^ The canonical proof of the equality type

822 | PResolveTC FC -- ^ Solve this dictionary by type class resolution

821 | PResolveTC FC -- ^ Solve this dictionary by type class resolution

823 | PEq FC PTerm PTerm PTerm PTerm -- ^ Heterogeneous equality type: A = B

822 | PEq FC PTerm PTerm PTerm PTerm -- ^ Heterogeneous equality type: A = B

824 | PRewrite FC PTerm PTerm (Maybe PTerm) -- ^ "rewrite" syntax, with optional result type

823 | PRewrite FC PTerm PTerm (Maybe PTerm) -- ^ "rewrite" syntax, with optional result type

@@ -1027,7 +1026,6 @@ highestFC (PMatchApp fc _) = Just fc

1027highestFC (PCase fc _ _) = Just fc

1026highestFC (PCase fc _ _) = Just fc

1028highestFC (PIfThenElse fc _ _ _) = Just fc

1027highestFC (PIfThenElse fc _ _ _) = Just fc

1029highestFC (PTrue fc _) = Just fc

1028highestFC (PTrue fc _) = Just fc

1030−highestFC (PRefl fc _) = Just fc

1031highestFC (PResolveTC fc) = Just fc

1029highestFC (PResolveTC fc) = Just fc

1032highestFC (PEq fc _ _ _ _) = Just fc

1030highestFC (PEq fc _ _ _ _) = Just fc

1033highestFC (PRewrite fc _ _ _) = Just fc

1031highestFC (PRewrite fc _ _ _) = Just fc

@@ -1556,7 +1554,6 @@ pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd

1556 , kwd "else" <+> prettySe startPrec bnd f

1554 , kwd "else" <+> prettySe startPrec bnd f

1557 ]

1555 ]

1558 prettySe p bnd (PHidden tm) = text "." <> prettySe funcAppPrec bnd tm

1556 prettySe p bnd (PHidden tm) = text "." <> prettySe funcAppPrec bnd tm

1559− prettySe p bnd (PRefl _ _) = annName eqCon $ text "Refl"

1560 prettySe p bnd (PResolveTC _) = kwd "%instance"

1557 prettySe p bnd (PResolveTC _) = kwd "%instance"

1561 prettySe p bnd (PTrue _ IsType) = annName unitTy $ text "()"

1558 prettySe p bnd (PTrue _ IsType) = annName unitTy $ text "()"

1562 prettySe p bnd (PTrue _ IsTerm) = annName unitCon $ text "()"

1559 prettySe p bnd (PTrue _ IsTerm) = annName unitCon $ text "()"

@@ -1872,7 +1869,6 @@ instance Sized PTerm where

1872 size (PCase fc trm bdy) = 1 + size trm + size bdy

1869 size (PCase fc trm bdy) = 1 + size trm + size bdy

1873 size (PIfThenElse fc c t f) = 1 + sum (map size [c, t, f])

1870 size (PIfThenElse fc c t f) = 1 + sum (map size [c, t, f])

1874 size (PTrue fc _) = 1

1871 size (PTrue fc _) = 1

1875− size (PRefl fc _) = 1

1876 size (PResolveTC fc) = 1

1872 size (PResolveTC fc) = 1

1877 size (PEq fc _ _ left right) = 1 + size left + size right

1873 size (PEq fc _ _ left right) = 1 + size left + size right

1878 size (PRewrite fc left right _) = 1 + size left + size right

1874 size (PRewrite fc left right _) = 1 + size left + size right

src/Idris/DeepSeq.hs−1

@@ -219,7 +219,6 @@ instance NFData PTerm where

219 rnf (PCase x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

220 rnf (PIfThenElse x1 x2 x3 x4) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

221 rnf (PTrue x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

222− rnf (PRefl x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

223 rnf (PResolveTC x1) = rnf x1 `seq` ()

222 rnf (PResolveTC x1) = rnf x1 `seq` ()

224 rnf (PEq x1 x2 x3 x4 x5) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()

223 rnf (PEq x1 x2 x3 x4 x5) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()

225 rnf (PRewrite x1 x2 x3 x4)

224 rnf (PRewrite x1 x2 x3 x4)

src/Idris/Delaborate.hs−5

@@ -107,7 +107,6 @@ delabTy' ist imps tm fullname mvs = de [] imps tm

107 deFn env (App _ f a) args = deFn env f (a:args)

108 deFn env (P _ n _) [l,r]

109 | n == pairTy = PPair un IsType (de env [] l) (de env [] r)

110− | n == eqCon = PRefl un (de env [] r)

111 | n == sUN "lazy" = de env [] r -- TODO: Fix string based matching

110 | n == sUN "lazy" = de env [] r -- TODO: Fix string based matching

112 deFn env (P _ n _) [ty, Bind x (Lam _) r]

111 deFn env (P _ n _) [ty, Bind x (Lam _) r]

113 | n == sigmaTy

112 | n == sigmaTy

@@ -485,9 +484,6 @@ addImplicitDiffs x y

485 = let (a', c') = addI a c

484 = let (a', c') = addI a c

486 (b', d') = addI b d in

485 (b', d') = addI b d in

487 (PPi p n a' b', PPi p' n' c' d')

486 (PPi p n a' b', PPi p' n' c' d')

488− addI (PRefl fc a) (PRefl fc' b)

489− = let (a', b') = addI a b in

490− (PRefl fc a', PRefl fc' b')

491 addI (PEq fc at bt a b) (PEq fc' ct dt c d)

487 addI (PEq fc at bt a b) (PEq fc' ct dt c d)

492 | trace (show (at,bt)) False = undefined

488 | trace (show (at,bt)) False = undefined

493 | at `expLike` ct && bt `expLike` dt

489 | at `expLike` ct && bt `expLike` dt

@@ -536,7 +532,6 @@ addImplicitDiffs x y

536 expLike (PDPair _ _ x _ y) (PDPair _ _ x' _ y') = expLike x x' && expLike y y'

532 expLike (PDPair _ _ x _ y) (PDPair _ _ x' _ y') = expLike x x' && expLike y y'

537 expLike (PEq _ xt yt x y) (PEq _ xt' yt' x' y')

533 expLike (PEq _ xt yt x y) (PEq _ xt' yt' x' y')

538 = expLike x x' && expLike y y'

534 = expLike x x' && expLike y y'

539− expLike (PRefl _ x) (PRefl _ x') = expLike x x'

540 expLike x y = x == y

535 expLike x y = x == y

541

536

542-- Issue #1589 on the issue tracker

537-- Issue #1589 on the issue tracker

src/Idris/Elab/Clause.hs+1−1

@@ -885,7 +885,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

885 (map (pexp . (PRef fc) . fst) bargs_post) ++

886 case mpn of

887 Nothing -> []

888− Just _ -> [pexp (PRefl fc Placeholder)])

888+ Just _ -> [pexp (PRef fc eqCon)])

889 logLvl 5 ("New RHS " ++ showTmImpls rhs)

890 ctxt <- getContext -- New context with block added

891 i <- getIState

src/Idris/Elab/Term.hs−3

@@ -343,9 +343,6 @@ elab ist info emode opts fn tm

343 elab' ina fc (PResolveTC fc')

344 = do c <- getNameFrom (sMN 0 "class")

345 instanceArg c

346− elab' ina _ (PRefl fc t)

347− = elab' ina (Just fc) (PApp fc (PRef fc eqCon) [pimp (sMN 0 "A") Placeholder True,

348− pimp (sMN 0 "x") t False])

349 elab' ina _ (PEq fc Placeholder Placeholder l r)

346 elab' ina _ (PEq fc Placeholder Placeholder l r)

350 = try (do tyn <- getNameFrom (sMN 0 "aqty")

347 = try (do tyn <- getNameFrom (sMN 0 "aqty")

351 claim tyn RType

348 claim tyn RType

src/Idris/ElabQuasiquote.hs−3

@@ -109,9 +109,6 @@ extractUnquotes n (PIfThenElse fc c t f)

109 (t', ex2) <- extractUnquotes n t

110 (f', ex3) <- extractUnquotes n f

111 return (PIfThenElse fc c' t' f', ex1 ++ ex2 ++ ex3)

112−extractUnquotes n (PRefl fc x)

113− = do (x', ex) <- extractUnquotes n x

114− return (PRefl fc x', ex)

115extractUnquotes n (PEq fc at bt a b)

112extractUnquotes n (PEq fc at bt a b)

116 = do (at', ex1) <- extractUnquotes n at

113 = do (at', ex1) <- extractUnquotes n at

117 (bt', ex2) <- extractUnquotes n bt

114 (bt', ex2) <- extractUnquotes n bt

src/Idris/Error.hs−1

@@ -104,7 +104,6 @@ warnDisamb ist (PCase _ tm cases) = warnDisamb ist tm >>

104 mapM_ (\(x,y)-> warnDisamb ist x >> warnDisamb ist y) cases

105warnDisamb ist (PIfThenElse _ c t f) = mapM_ (warnDisamb ist) [c, t, f]

106warnDisamb ist (PTrue _ _) = return ()

107−warnDisamb ist (PRefl _ tm) = warnDisamb ist tm

108warnDisamb ist (PResolveTC _) = return ()

107warnDisamb ist (PResolveTC _) = return ()

109warnDisamb ist (PEq _ a b x y) = warnDisamb ist a >> warnDisamb ist b >>

108warnDisamb ist (PEq _ a b x y) = warnDisamb ist a >> warnDisamb ist b >>

110 warnDisamb ist x >> warnDisamb ist y

109 warnDisamb ist x >> warnDisamb ist y

src/Idris/IBC.hs−6

@@ -1542,9 +1542,6 @@ instance Binary PTerm where

1542 PTrue x1 x2 -> do putWord8 12

1543 put x1

1544 put x2

1545− PRefl x1 x2 -> do putWord8 14

1546− put x1

1547− put x2

1548 PResolveTC x1 -> do putWord8 15

1545 PResolveTC x1 -> do putWord8 15

1549 put x1

1546 put x1

1550 PEq x1 x2 x3 x4 x5 -> do putWord8 16

1547 PEq x1 x2 x3 x4 x5 -> do putWord8 16

@@ -1681,9 +1678,6 @@ instance Binary PTerm where

1681 12 -> do x1 <- get

1678 12 -> do x1 <- get

1682 x2 <- get

1679 x2 <- get

1683 return (PTrue x1 x2)

1680 return (PTrue x1 x2)

1684− 14 -> do x1 <- get

1685− x2 <- get

1686− return (PRefl x1 x2)

1687 15 -> do x1 <- get

1681 15 -> do x1 <- get

1688 return (PResolveTC x1)

1682 return (PResolveTC x1)

1689 16 -> do x1 <- get

1683 16 -> do x1 <- get

src/Idris/IdrisDoc.hs−1

@@ -303,7 +303,6 @@ extractPTermNames (PMatchApp _ n) = [n]

303extractPTermNames (PCase _ p ps) = let (ps1, ps2) = unzip ps

304 in concatMap extract (p:(ps1 ++ ps2))

305extractPTermNames (PIfThenElse _ c t f) = concatMap extract [c, t, f]

306−extractPTermNames (PRefl _ p) = extract p

307extractPTermNames (PEq _ _ _ p1 p2) = concatMap extract [p1, p2]

306extractPTermNames (PEq _ _ _ p1 p2) = concatMap extract [p1, p2]

308extractPTermNames (PRewrite _ a b m) | Just c <- m =

307extractPTermNames (PRewrite _ a b m) | Just c <- m =

309 concatMap extract [a, b, c]

308 concatMap extract [a, b, c]

src/Idris/ParseExpr.hs−4

@@ -326,10 +326,6 @@ simpleExpr syn =

326 try (simpleExternalExpr syn)

327 <|> do x <- try (lchar '?' *> name); return (PMetavar x)

328 <|> do lchar '%'; fc <- getFC; reserved "instance"; return (PResolveTC fc)

329− <|> do reserved "Refl"; fc <- getFC;

330− tm <- option Placeholder (do lchar '{'; t <- expr syn; lchar '}';

331− return t)

332− return (PRefl fc tm)

333 <|> do reserved "elim_for"; fc <- getFC; t <- fnName; return (PRef fc (SN $ ElimN t))

329 <|> do reserved "elim_for"; fc <- getFC; t <- fnName; return (PRef fc (SN $ ElimN t))

334 <|> proofExpr syn

330 <|> proofExpr syn

335 <|> tacticsExpr syn

331 <|> tacticsExpr syn

src/Idris/ProofSearch.hs+1−1

@@ -22,7 +22,7 @@ import Debug.Trace

22-- Pass in a term elaborator to avoid a cyclic dependency with ElabTerm

23

24trivial :: (PTerm -> ElabD ()) -> IState -> ElabD ()

25−trivial elab ist = try' (do elab (PRefl (fileFC "prf") Placeholder)

25+trivial elab ist = try' (do elab (PApp (fileFC "prf") (PRef (fileFC "prf") eqCon) [pimp (sUN "A") Placeholder False, pimp (sUN "x") Placeholder False])

26 return ())

27 (do env <- get_env

28 g <- goal

test/reg047/reg047.idr+1−1

@@ -9,7 +9,7 @@ Id : (A : Type) -> A -> A -> Type

9Id A = (=) {A = A} {B = A}

10

11IdRefl : (A : Type) -> (a : A) -> Id A a a

12−IdRefl A a = Refl {a}

12+IdRefl A a = Refl {x = a}

13

14zzz : Id Nat zero zero

15zzz = IdRefl Nat zero

test/reg047/reg047a.idr+1−1

@@ -9,7 +9,7 @@ Id : (A : Type) -> A -> A -> Type

9Id = \A,x,y => x = y -- {a = A} {b = A}

10

11IdRefl : (A : Type) -> (a : A) -> Id A a a

12−IdRefl A a = Refl {a}

12+IdRefl A a = Refl {x = a}

13

14zzzz : Id MNat zero zero

15zzzz = IdRefl MNat zero

test/reg056/reg056.idr+1−1

@@ -6,7 +6,7 @@ postulate trap : Z = Z

6dodgy : (a, b : ()) -> a = b -> Void

7dodgy n m Refl impossible

8

9−nonk : (trap = Refl {Z}) -> Void

9+nonk : (trap = Refl {x = Z}) -> Void

10nonk Refl impossible

11

12false : Void