4a4548e · Idris-dev · git.iko.soy

idris.cabal+4

compare with master

unifiedsplit

@@ -589,6 +589,10 @@ Extra-source-files:

589 test/interactive012/input

590 test/interactive012/run

591 test/interactive012/*.idr

592+ test/interactive013/expected

593+ test/interactive013/input

594+ test/interactive013/run

595+ test/interactive013/*.idr

592

596

593 test/io001/run

597 test/io001/run

594 test/io001/*.idr

598 test/io001/*.idr

src/Idris/Core/Unify.hs+8−10

@@ -529,13 +529,19 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =

529 (do hf <- un' env True bnames fx fy

530 let ax' = hnormalise hf ctxt env (substNames hf ax)

531 let ay' = hnormalise hf ctxt env (substNames hf ay)

532+ -- Don't normalise if we don't have to

533+ ha <- uplus (un' env False bnames (substNames hf ax)

534+ (substNames hf ay))

532− ha <- un' env False bnames ax' ay'

535+ (un' env False bnames ax' ay')

533 sc 1

536 sc 1

534 combine env bnames hf ha)

537 combine env bnames hf ha)

535 (do ha <- un' env False bnames ax ay

538 (do ha <- un' env False bnames ax ay

536 let fx' = hnormalise ha ctxt env (substNames ha fx)

539 let fx' = hnormalise ha ctxt env (substNames ha fx)

537 let fy' = hnormalise ha ctxt env (substNames ha fy)

540 let fy' = hnormalise ha ctxt env (substNames ha fy)

541+ -- Don't normalise if we don't have to

538− hf <- un' env False bnames fx' fy'

542+ hf <- uplus (un' env False bnames (substNames ha fx)

543+ (substNames ha fy))

544+ (un' env False bnames fx' fy')

539 sc 1

545 sc 1

540 combine env bnames hf ha)

546 combine env bnames hf ha)

541 | otherwise = unifyTmpFail appx appy

547 | otherwise = unifyTmpFail appx appy

@@ -551,14 +557,6 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =

551 = unifyFail appx appy

557 = unifyFail appx appy

552 checkHeads _ _ = return []

558 checkHeads _ _ = return []

553

559

554− unArgs as [] [] = return as

555− unArgs as (x : xs) (y : ys)

556− = do let x' = hnormalise as ctxt env (substNames as x)

557− let y' = hnormalise as ctxt env (substNames as y)

558− as' <- un' env False bnames x' y'

559− vs <- combine env bnames as as'

560− unArgs vs xs ys

561−

562 numArgs tm = let (f, args) = unApply tm in length args

560 numArgs tm = let (f, args) = unApply tm in length args

563

561

564 metavarApp tm = let (f, args) = unApply tm in

562 metavarApp tm = let (f, args) = unApply tm in

test/interactive013/expectednew file+4

@@ -0,0 +1,4 @@

1+gcd aa (aa + (S y)) (CmpLT y) = ?gcd_rhs_1

2+gcd bb bb CmpEQ = ?gcd_rhs_2

3+gcd (bb + (S x)) bb (CmpGT x) = ?gcd_rhs_3

4+

test/interactive013/inputnew file+1

@@ -0,0 +1 @@

1+:cs 3 cc

test/interactive013/interactive013.idrnew file+4

@@ -0,0 +1,4 @@

1+

2+gcd : (x : Nat) -> (y : Nat) -> CmpNat x y -> Nat

3+gcd aa bb cc = ?gcd_rhs

4+

test/interactive013/runnew file+3

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

1+#!/usr/bin/env bash

2+${IDRIS:-idris} --quiet interactive013.idr < input

3+rm -f *.ibc