2ce525e · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

intros tactic; some library tinkering

commit2ce525edac7e469defef6e5811e24294f3889742 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateSun 8 Jan 2012, 14:35 (15 years ago) parenta33b4c2

10 files changed+43−15

compare with master

unifiedsplit

lib/prelude/list.idr+2−2 lib/prelude/nat.idr+2−6 lib/prelude/vect.idr+19 src/Core/TT.hs+8−1 src/Idris/AbsSyntax.hs+1−1 src/Idris/ElabTerm.hs+7 src/Idris/Parser.hs+1 tutorial/idris-tutorial.pdf tutorial/miscellany.tex+1−2 tutorial/theorems.tex+2−3

lib/prelude/list.idr+2−2

@@ -12,11 +12,11 @@ data List a = Nil | (::) a (List a)

1212rev : List a -> List a

1313rev xs = revAcc [] xs where

1414 revAcc : List a -> List a -> List a

15− revAcc acc [] = acc

15+ revAcc acc [] = acc

1616 revAcc acc (x :: xs) = revAcc (x :: acc) xs

1717

1818app : List a -> List a -> List a

19−app [] xs = xs

19+app [] xs = xs

2020app (x :: xs) ys = x :: app xs ys

2121

2222length : List a -> Int

lib/prelude/nat.idr+2−6

@@ -100,9 +100,7 @@ mult_commutes O m = ?mult_commO

100100mult_commutes (S k) m = let ih = mult_commutes k m in ?mult_commSk

101101

102102mult_commSk = proof {

103− intro;

104− intro;

105− intro;

103+ intros;

106104 rewrite sym ih;

107105 rewrite multn_Sm m k;

108106 trivial;

@@ -115,9 +113,7 @@ mult_commO = proof {

115113}

116114

117115multnSmSk = proof {

118− intro;

119− intro;

120− intro;

116+ intros;

121117 rewrite plus_commutes (mult k m) m;

122118 rewrite sym (plus_assoc k (mult k m) m);

123119 rewrite ih;

lib/prelude/vect.idr+19

@@ -31,4 +31,23 @@ map : (a -> b) -> Vect a n -> Vect b n

3131map f [] = []

3232map f (x :: xs) = f x :: map f xs

3333

34+rev : Vect a n -> Vect a n

35+rev xs = revAcc [] xs where

36+ revAcc : Vect a n -> Vect a m -> Vect a (n + m)

37+ revAcc acc [] ?= acc

38+ revAcc acc (x :: xs) ?= revAcc (x :: acc) xs

39+

40+---------- Proofs ----------

41+

42+revAcc_lemma_2 = proof {

43+ intros;

44+ rewrite sym (plusn_Sm n k);

45+ exact value;

46+}

47+

48+revAcc_lemma_1 = proof {

49+ intros;

50+ rewrite sym (plusnO n);

51+ exact value;

52+}

3453

src/Core/TT.hs+8−1

@@ -267,11 +267,18 @@ instance Show UConstraint where

267267type UCs = (Int, [UConstraint])

268268

269269data NameType = Bound | Ref | DCon Int Int | TCon Int Int

270− deriving (Show, Eq)

270+ deriving (Show)

271271{-!

272272deriving instance Binary NameType

273273!-}

274274

275+instance Eq NameType where

276+ Bound == Bound = True

277+ Ref == Ref = True

278+ DCon _ a == DCon _ b = (a == b) -- ignore tag

279+ TCon _ a == TCon _ b = (a == b) -- ignore tag

280+ _ == _ = False

281+

275282data TT n = P NameType n (TT n) -- embed type

276283 | V Int

277284 | Bind n (Binder (TT n)) (TT n)

src/Idris/AbsSyntax.hs+1−1

@@ -460,7 +460,7 @@ mapPT f t = f (mpt t) where

460460 mpt x = x

461461

462462

463−data PTactic' t = Intro [Name] | Focus Name

463+data PTactic' t = Intro [Name] | Intros | Focus Name

464464 | Refine Name [Bool] | Rewrite t | LetTac Name t

465465 | Exact t | Compute | Trivial

466466 | Solve

src/Idris/ElabTerm.hs+7

@@ -371,6 +371,13 @@ runTac autoSolve ist tac = runT (fmap (addImpl ist) tac) where

371371 bname (Bind n _ _) = Just n

372372 bname _ = Nothing

373373 runT (Intro xs) = mapM_ (\x -> do attack; intro (Just x)) xs

374+ runT Intros = do g <- goal

375+ attack; intro (bname g)

376+ try (runT Intros)

377+ (return ())

378+ where

379+ bname (Bind n _ _) = Just n

380+ bname _ = Nothing

374381 runT (Exact tm) = do elab ist toplevel False False (MN 0 "tac") tm

375382 when autoSolve solveAll

376383 runT (Refine fn [])

src/Idris/Parser.hs+1

@@ -1124,6 +1124,7 @@ pDirective = try (do lchar '%'; reserved "lib"; lib <- strlit;

11241124pTactic :: SyntaxInfo -> IParser PTactic

11251125pTactic syn = do reserved "intro"; ns <- sepBy pName (lchar ',')

11261126 return $ Intro ns

1127+ <|> do reserved "intros"; return Intros

11271128 <|> try (do reserved "refine"; n <- pName

11281129 imps <- many1 imp

11291130 return $ Refine n imps)

tutorial/idris-tutorial.pdf

Binary file not shown.

tutorial/miscellany.tex+1−2

@@ -176,8 +176,7 @@ Universes are \emph{cumulative}, that is, if \texttt{x : Set n} we can also have

176176The typechecker generates such universe

177177constraints and reports an error if any inconsistencies are found. Ordinarily, a

178178programmer does not need to worry about this, but it does prevent (contrived)

179−programs such as

180−the following:

179+programs such as the following:

181180

182181\begin{SaveVerbatim}{idid}

183182

tutorial/theorems.tex+2−3

@@ -241,7 +241,7 @@ Let us now prove the other required lemma, \texttt{plusredO\_S}:

241241In this case, the goal is a function type, using \texttt{k} (the argument accessible by

242242pattern matching) and \texttt{ih} (the local variable containing the result of

243243the recursive call). We can introduce these as premisses using the \texttt{intro} tactic

244−twice. This gives:

244+twice (or \texttt{intros}, which introduces all arguments as premisses). This gives:

245245

246246\begin{SaveVerbatim}{prSintros}

247247

@@ -282,8 +282,7 @@ the goal using that proof. Here, it results in an equality which is trivially pr

282282plusredO_S: no more goals

283283-plusredO_S> qed

284284plusredO_S = proof {

285− intro;

286− intro;

285+ intros;

287286 rewrite ih;

288287 trivial;

289288}