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

git.iko.soy/Idris-dev

Try all names in refine to resolve ambiguity

Fixes #426

commit922fdd168fcc43b2fc7c3a36e4f38080d0afc4f2 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSun 4 Aug 2013, 14:55 (13 years ago) parent3ad3bd6

5 files changed+61−11

compare with master

unifiedsplit

src/Idris/ElabTerm.hs+18−11 test/README+2 test/test029/expected test/test029/run+3 test/test029/test029.idr+38

src/Idris/ElabTerm.hs+18−11

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

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

762762 when autoSolve solveAll

763763 runT (MatchRefine fn)

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

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

766− return (fn, a)

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

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

764+ = do fnimps <-

765+ case lookupCtxtName fn (idris_implicits ist) of

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

767+ return [(fn, a)]

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

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

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

771+ show fn')) fnimps

772+ tryAll tacs

769773 when autoSolve solveAll

770774 where envArgs n = do e <- get_env

771775 case lookup n e of

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

773777 (getArgTys (binderTy t))

774778 _ -> return []

775779 runT (Refine fn [])

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

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

778− return (fn, a)

779− -- FIXME: resolve ambiguities

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

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

780+ = do fnimps <-

781+ case lookupCtxtName fn (idris_implicits ist) of

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

783+ return [(fn, a)]

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

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

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

787+ show fn')) fnimps

788+ tryAll tacs

782789 when autoSolve solveAll

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

784791 isImp _ = False

test/README+2

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

2727025: memory effects

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

2929027: class constraints in using block

30+028:

31+029: match_refine and apply by type

3032

3133regxxx: various regression tests

3234reg020: 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

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

5+-- Base case

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

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

8+ (Z + m = m) in refl

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+