85e68a7 · Idris-dev · git.iko.soy

src/Idris/Core/Unify.hs+16−7

compare with master

unifiedsplit

@@ -379,9 +379,10 @@ unify ctxt env topx topy dont holes =

379 unArgs vs xs ys

380

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

382− metavar f &&

382+ (metavar f &&

383− all (\x -> metavarApp x) args

383+ all (\x -> metavarApp x) args

384− && nub args == args

384+ && nub args == args) ||

385+ globmetavar tm

385 metavarArgs tm = let (f, args) = unApply tm in

386 metavarArgs tm = let (f, args) = unApply tm in

386 all (\x -> metavar x || inenv x) args

387 all (\x -> metavar x || inenv x) args

387 && nub args == args

388 && nub args == args

@@ -413,14 +414,22 @@ unify ctxt env topx topy dont holes =

413

414

414 rigid (P (DCon _ _) _ _) = True

415 rigid (P (DCon _ _) _ _) = True

415 rigid (P (TCon _ _) _ _) = True

416 rigid (P (TCon _ _) _ _) = True

416− rigid t@(P Ref _ _) = inenv t

417+ rigid t@(P Ref _ _) = inenv t || globmetavar t

417 rigid (Constant _) = True

418 rigid (Constant _) = True

418 rigid (App f a) = rigid f && rigid a

419 rigid (App f a) = rigid f && rigid a

419− rigid t = not (metavar t)

420+ rigid t = not (metavar t) || globmetavar t

421+

422+ globmetavar t = case unApply t of

423+ (P _ x _, _) ->

424+ case lookupDef x ctxt of

425+ [TyDecl _ _] -> True

426+ _ -> False

427+ _ -> False

420

428

421 metavar t = case t of

429 metavar t = case t of

422− P _ x _ -> (x `elem` holes || holeIn env x) &&

430+ P _ x _ -> ((x `elem` holes || holeIn env x) &&

423− not (x `elem` dont)

431+ not (x `elem` dont))

432+ || globmetavar t

424 _ -> False

433 _ -> False

425 pat t = case t of

434 pat t = case t of

426 P _ x _ -> x `elem` holes || patIn env x

435 P _ x _ -> x `elem` holes || patIn env x

src/Idris/ProofSearch.hs+5−1

@@ -1,3 +1,5 @@

1+{-# LANGUAGE PatternGuards #-}

2+

1module Idris.ProofSearch(trivial, proofSearch) where

3module Idris.ProofSearch(trivial, proofSearch) where

2

4

3import Idris.Core.Elaborate hiding (Tactic(..))

5import Idris.Core.Elaborate hiding (Tactic(..))

@@ -45,7 +47,9 @@ proofSearch elab fn nroot hints ist

45

47

46 findInferredTy (t : _) = elab (delab ist (toUN t))

48 findInferredTy (t : _) = elab (delab ist (toUN t))

47

49

48− toUN (P nt (MN i n) ty) = P nt (UN n) ty

50+ toUN t@(P nt (MN i n) ty)

51+ | ('_':xs) <- str n = t

52+ | otherwise = P nt (UN n) ty

49 toUN (App f a) = App (toUN f) (toUN a)

53 toUN (App f a) = App (toUN f) (toUN a)

50 toUN t = t

54 toUN t = t

51

55

test/interactive002/expected+2

@@ -7,3 +7,5 @@ Vect (n + m) a

7Nat

8Nat

9S n

10+String

11+()

test/interactive002/input+2

@@ -6,4 +6,6 @@

6:ps 9 plus_in1

7:ps 9 plus_out

8:ps 13 what

9+:ps 16 ifoo_arg1

10+:ps 16 ifoo_out

9

11

test/interactive002/interactive002.idr+3

@@ -13,5 +13,8 @@ myplus (S k) y = S (myplus k y)

13vfun : a -> Vect n a -> Vect n a -> Vect ?what a

14vfun v xs ys = v :: ys

15

16+ifoo : ?ifoo_arg1 -> IO ?ifoo_out

17+ifoo x = do putStrLn x

18+ putStrLn "World"

16

19

17

20