ilyakooo0/Idris-dev
1
0
Fork 0
mirror of https://github.com/ilyakooo0/Idris-dev.git synced 2024-09-21 22:17:19 +03:00
Code Issues Projects Releases Wiki Activity

Improve inference in monadic code

Browse Source 
This makes unification treat global metavariables the same way as local
metavariables. Maybe be slightly dubious if the metavariable is not
intended for type inference...
This commit is contained in:
Edwin Brady 2014-02-10 10:11:00 +00:00
parent ad178cf58b
commit 85e68a7b69
5 changed files with 28 additions and 8 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

23
src/Idris/Core/Unify.hs
View File

@ -379,9 +379,10 @@ unify ctxt env topx topy dont holes =
unArgs vs xs ys
metavarApp tm = let (f, args) = unApply tm in
metavar f &&
all (\x -> metavarApp x) args
&& nub args == args
(metavar f &&
all (\x -> metavarApp x) args
&& nub args == args) ||
globmetavar tm
metavarArgs tm = let (f, args) = unApply tm in
all (\x -> metavar x || inenv x) args
&& nub args == args
@ -413,14 +414,22 @@ unify ctxt env topx topy dont holes =
rigid (P (DCon _ _) _ _) = True
rigid (P (TCon _ _) _ _) = True
rigid t@(P Ref _ _) = inenv t
rigid t@(P Ref _ _) = inenv t || globmetavar t
rigid (Constant _) = True
rigid (App f a) = rigid f && rigid a
rigid t = not (metavar t)
rigid t = not (metavar t) || globmetavar t
globmetavar t = case unApply t of
(P _ x _, _) ->
case lookupDef x ctxt of
[TyDecl _ _] -> True
_ -> False
_ -> False
metavar t = case t of
P _ x _ -> (x `elem` holes || holeIn env x) &&
not (x `elem` dont)
P _ x _ -> ((x `elem` holes || holeIn env x) &&
not (x `elem` dont))
|| globmetavar t
_ -> False
pat t = case t of
P _ x _ -> x `elem` holes || patIn env x

6
src/Idris/ProofSearch.hs
View File

@ -1,3 +1,5 @@
{-# LANGUAGE PatternGuards #-}
module Idris.ProofSearch(trivial, proofSearch) where
import Idris.Core.Elaborate hiding (Tactic(..))
@ -45,7 +47,9 @@ proofSearch elab fn nroot hints ist
findInferredTy (t : _) = elab (delab ist (toUN t))
toUN (P nt (MN i n) ty) = P nt (UN n) ty
toUN t@(P nt (MN i n) ty)
| ('_':xs) <- str n = t
| otherwise = P nt (UN n) ty
toUN (App f a) = App (toUN f) (toUN a)
toUN t = t

2
test/interactive002/expected
View File

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

2
test/interactive002/input
View File

@ -6,4 +6,6 @@
:ps 9 plus_in1
:ps 9 plus_out
:ps 13 what
:ps 16 ifoo_arg1
:ps 16 ifoo_out

3
test/interactive002/interactive002.idr
View File

@ -13,5 +13,8 @@ myplus (S k) y = S (myplus k y)
vfun : a -> Vect n a -> Vect n a -> Vect ?what a
vfun v xs ys = v :: ys
ifoo : ?ifoo_arg1 -> IO ?ifoo_out
ifoo x = do putStrLn x
putStrLn "World"