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

idris.cabal+13

compare with master

unifiedsplit

@@ -516,9 +516,22 @@ Extra-source-files:

516 test/proof004/run

517 test/proof004/*.idr

518 test/proof004/expected

519+ test/proof005/run

520+ test/proof005/*.idr

521+ test/proof005/expected

522+ test/proof006/run

523+ test/proof006/*.idr

524+ test/proof006/expected

525+ test/proof007/run

526+ test/proof007/*.idr

527+ test/proof007/expected

519 test/proof008/run

528 test/proof008/run

520 test/proof008/*.idr

529 test/proof008/*.idr

521 test/proof008/expected

530 test/proof008/expected

531+ test/proof009/run

532+ test/proof009/*.idr

533+ test/proof009/expected

534+ test/proof009/input

522

535

523 test/quasiquote001/run

536 test/quasiquote001/run

524 test/quasiquote001/*.idr

537 test/quasiquote001/*.idr

src/Idris/Core/TT.hs+2

@@ -1193,6 +1193,8 @@ safeForgetEnv env (Bind n b sc)

1193 Just $ RBind n' b' sc'

1194 where safeForgetEnvB env (Let t v) = liftM2 Let (safeForgetEnv env t)

1195 (safeForgetEnv env v)

1196+ safeForgetEnvB env (Guess t v) = liftM2 Guess (safeForgetEnv env t)

1197+ (safeForgetEnv env v)

1196 safeForgetEnvB env b = do ty' <- safeForgetEnv env (binderTy b)

1198 safeForgetEnvB env b = do ty' <- safeForgetEnv env (binderTy b)

1197 Just $ fmap (\_ -> ty') b

1199 Just $ fmap (\_ -> ty') b

1198safeForgetEnv env (App f a) = liftM2 RApp (safeForgetEnv env f) (safeForgetEnv env a)

1200safeForgetEnv env (App f a) = liftM2 RApp (safeForgetEnv env f) (safeForgetEnv env a)

src/Idris/ElabTerm.hs+2−1

@@ -1734,7 +1734,8 @@ runTac autoSolve ist perhapsFC fn tac

1734 bname _ = Nothing

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

1736 runT Intros = do g <- goal

1737+ attack;

1737− attack; intro (bname g)

1738+ intro (bname g)

1738 try' (runT Intros)

1739 try' (runT Intros)

1739 (return ()) True

1740 (return ()) True

1740 where

1741 where

test/proof009/expectednew file+26

@@ -0,0 +1,26 @@

1+Type checking ./proof009.idr

2+

3+

4+---------- Goal: ----------

5+{hole0} : Int -> Int -> Int

6+-Main.arhs> ---------- Other goals: ----------

7+{hole0}

8+---------- Assumptions: ----------

9+ x : Int

10+---------- Goal: ----------

11+{hole1} : Int -> Int

12+-Main.arhs> ---------- Other goals: ----------

13+{hole1},{hole0}

14+---------- Assumptions: ----------

15+ x : Int

16+ y : Int

17+---------- Goal: ----------

18+{hole2} : Int

19+-Main.arhs> arhs: No more goals.

20+-Main.arhs> Proof completed!

21+Main.arhs = proof

22+ intro x

23+ intros

24+ trivial

25+

26+

test/proof009/inputnew file+6

@@ -0,0 +1,6 @@

1+:p arhs

2+intro x

3+intros

4+trivial

5+qed

6+:q

test/proof009/proof009.idrnew file+9

@@ -0,0 +1,9 @@

1+afn : Int -> Int -> Int

2+afn x y = ?arhs

3+

4+-- plus_comm_rhs_1 : y = plus y 0

5+--

6+-- plus_comm : (x, y : Nat) -> plus x y = plus y x

7+-- plus_comm Z y = plus_comm_rhs_1

8+-- plus_comm (S k) y = ?plus_comm_rhs_2

9+

test/proof009/runnew file+3

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

1+#!/usr/bin/env bash

2+idris $@ --quiet proof009.idr < input

3+rm -f *.ibc