e3a4097 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Fix eta problem

commite3a40970e7b8652c1387ffa579f3fa9c085e53c5 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateThu 28 Mar 2013, 11:08 (14 years ago) parentf174fd3

5 files changed+13−2

unifiedsplit

src/Core/Evaluate.hs+6

@@ -525,6 +525,12 @@ convEq ctxt = ceq [] where

525525 ceq ps (P xt x _) (P yt y _)

526526 | x == y || (x, y) `elem` ps || (y,x) `elem` ps = return True

527527 | otherwise = sameDefs ps x y

528+ ceq ps x (Bind n (Lam t) (App y (V 0))) = ceq ps x y

529+ ceq ps (Bind n (Lam t) (App x (V 0))) y = ceq ps x y

530+ ceq ps x (Bind n (Lam t) (App y (P Bound n' _)))

531+ | n == n' = ceq ps x y

532+ ceq ps (Bind n (Lam t) (App x (P Bound n' _))) y

533+ | n == n' = ceq ps x y

528534 ceq ps (V x) (V y) = return (x == y)

529535 ceq ps (Bind _ xb xs) (Bind _ yb ys)

530536 = liftM2 (&&) (ceqB ps xb yb) (ceq ps xs ys)

src/Core/ProofState.hs+1−2

@@ -358,9 +358,8 @@ exact _ _ _ _ = fail "Can't fill here."

358358-- As exact, but attempts to solve other goals by unification

359359

360360fill :: Raw -> RunTactic

361−fill guess ctxt env (Bind x (Hole ty) sc) =

361+fill guess ctxt env (Bind x (Hole ty) sc) =

362362 do (val, valty) <- lift $ check ctxt env guess

363− s <- get

364363-- let valtyn = normalise ctxt env valty

365364-- let tyn = normalise ctxt env ty

366365 ns <- unify' ctxt env valty ty

test/reg015/expectednew file

No changes to the content.

test/reg015/reg015.idrnew file+3

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

1+using (A : Type, B : A->Type, C : Type)

2+ foo : ((x:A) -> B x -> C) -> ((x:A ** B x) -> C)

3+ foo f p = f (getWitness p) (getProof p)

test/reg015/runnew file+3

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

1+#!/bin/bash

2+idris $@ reg015.idr --check

3+rm -f *.ibc