f885274 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Fix ordering of auto-implicits with 'using'

'using' arguments always now appear before fully implicit arguments, rather than the order we happen to find them in. TODO: Better would be to sort according to which ones we know depend on each other...

commitf88527481364f91064255b24d2a69dbaed31ee55 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSat 22 Jun 2013, 23:23 (13 years ago) parent894db6f

1 file changed+7−4

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+7−4

src/Idris/AbsSyntax.hs+7−4

@@ -796,17 +796,20 @@ implicit' syn ignore n ptm

796796 return tm'

797797

798798implicitise :: SyntaxInfo -> [Name] -> IState -> PTerm -> (PTerm, [PArg])

799−implicitise syn ignore ist tm

800− = let (declimps, ns') = execState (imps True [] tm) ([], [])

799+implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $

800+ let (declimps, ns') = execState (imps True [] tm) ([], [])

801801 ns = filter (\n -> implicitable n || elem n (map fst uvars)) $

802− ns' \\ (map fst pvars ++ no_imp syn ++ ignore) in

802+ ns' \\ (map fst pvars ++ no_imp syn ++ ignore)

803+ nsOrder = filter (not . inUsing) ns ++ filter inUsing ns in

803804 if null ns

804805 then (tm, reverse declimps)

805− else implicitise syn ignore ist (pibind uvars ns tm)

806+ else implicitise syn ignore ist (pibind uvars nsOrder tm)

806807 where

807808 uvars = map ipair (filter uimplicit (using syn))

808809 pvars = syn_params syn

809810

811+ inUsing n = n `elem` map fst uvars

812+

810813 ipair (UImplicit x y) = (x, y)

811814 uimplicit (UImplicit _ _) = True

812815 uimplicit _ = False