922fdd1 · Idris-dev · git.iko.soy

src/Idris/ElabTerm.hs+18−11

compare with master

unifiedsplit

@@ -761,11 +761,15 @@ runTac autoSolve ist tac

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

762 when autoSolve solveAll

763 runT (MatchRefine fn)

764+ = do fnimps <-

764− = do (fn', imps) <- case lookupCtxtName fn (idris_implicits ist) of

765+ case lookupCtxtName fn (idris_implicits ist) of

765− [] -> do a <- envArgs fn

766+ [] -> do a <- envArgs fn

766− return (fn, a)

767+ return [(fn, a)]

767− [(n, args)] -> return $ (n, map (const True) args)

768+ ns -> return (map (\ (n, a) -> (n, map (const True) a)) ns)

769+ let tacs = map (\ (fn', imps) ->

768− ns <- match_apply (Var fn') (map (\x -> (x, 0)) imps)

770+ (match_apply (Var fn') (map (\x -> (x, 0)) imps),

771+ show fn')) fnimps

772+ tryAll tacs

769 when autoSolve solveAll

773 when autoSolve solveAll

770 where envArgs n = do e <- get_env

774 where envArgs n = do e <- get_env

771 case lookup n e of

775 case lookup n e of

@@ -773,12 +777,15 @@ runTac autoSolve ist tac

773 (getArgTys (binderTy t))

777 (getArgTys (binderTy t))

774 _ -> return []

778 _ -> return []

775 runT (Refine fn [])

779 runT (Refine fn [])

780+ = do fnimps <-

776− = do (fn', imps) <- case lookupCtxtName fn (idris_implicits ist) of

781+ case lookupCtxtName fn (idris_implicits ist) of

777− [] -> do a <- envArgs fn

782+ [] -> do a <- envArgs fn

778− return (fn, a)

783+ return [(fn, a)]

779− -- FIXME: resolve ambiguities

780− [(n, args)] -> return $ (n, map isImp args)

784+ ns -> return (map (\ (n, a) -> (n, map isImp a)) ns)

785+ let tacs = map (\ (fn', imps) ->

781− ns <- apply (Var fn') (map (\x -> (x, 0)) imps)

786+ (apply (Var fn') (map (\x -> (x, 0)) imps),

787+ show fn')) fnimps

788+ tryAll tacs

782 when autoSolve solveAll

789 when autoSolve solveAll

783 where isImp (PImp _ _ _ _ _) = True

790 where isImp (PImp _ _ _ _ _) = True

784 isImp _ = False

791 isImp _ = False

test/README+2

@@ -27,6 +27,8 @@ Tests:

27025: memory effects

28026: simple file-I/O-based type provider

29027: class constraints in using block

30+028:

31+029: match_refine and apply by type

30

32

31regxxx: various regression tests

33regxxx: various regression tests

32reg020: working strlen

34reg020: working strlen

test/test029/expectednew file

No changes to the content.

test/test029/runnew file+3

@@ -0,0 +1,3 @@

1+#!/bin/bash

2+idris $@ test029.idr --check test029

3+rm -f *.ibc

test/test029/test029.idrnew file+38

@@ -0,0 +1,38 @@

1+module simple

2+

3+plus_comm : (n : Nat) -> (m : Nat) -> (n + m = m + n)

4+

5+-- Base case

6+(Z + m = m + Z) <== plus_comm =

7+ rewrite ((m + Z = m) <== plusZeroRightNeutral) ==>

8+ (Z + m = m) in refl

9+

10+-- Step case

11+(S k + m = m + S k) <== plus_comm =

12+ rewrite ((k + m = m + k) <== plus_comm) in

13+ rewrite ((S (m + k) = m + S k) <== plusSuccRightSucc) in

14+ refl

15+-- QED

16+

17+append : Vect n a -> Vect m a -> Vect (m + n) a

18+append [] ys ?= ys

19+append (x :: xs) ys ?= x :: append xs ys

20+

21+

22+

23+---------- Proofs ----------

24+

25+simple.append_lemma_2 = proof {

26+ intros;

27+ compute;

28+ rewrite (plusSuccRightSucc m n);

29+ trivial;

30+}

31+

32+simple.append_lemma_1 = proof {

33+ intros;

34+ compute;

35+ rewrite sym (plusZeroRightNeutral m);

36+ exact value;

37+}

38+