229a99c · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Better elaboration order; also changed instance argument syntax slightly

229a99cEdwin Brady15 years ago

interp.idr+9−12

compare with master

unifiedsplit

@@ -22,8 +22,8 @@ using (G : Vect Ty n) {

22 | App : Expr G (TyFun a t) -> Expr G a -> Expr G t

23 | Op : (Int -> Int -> interpTy c) ->

24 Expr G TyInt -> Expr G TyInt -> Expr G c

25− -- | Op' : (interpTy a -> interpTy b -> interpTy c) ->

25+ | Op' : (interpTy a -> interpTy b -> interpTy c) ->

26− -- Expr G a -> Expr G b -> Expr G c

26+ Expr G a -> Expr G b -> Expr G c

27 | If : Expr G TyBool -> Expr G a -> Expr G a -> Expr G a

28 | Bind : Expr G a -> (interpTy a -> Expr G b) -> Expr G b;

@@ -34,6 +34,7 @@ using (G : Vect Ty n) {

34 interp env (Lam sc) = \x => interp (Extend x env) sc;

35 interp env (App f s) = (interp env f) (interp env s);

36 interp env (Op op x y) = op (interp env x) (interp env y);

37+ interp env (Op' op x y) = op (interp env x) (interp env y);

37 interp env (If x t e) = if (interp env x) then (interp env t) else (interp env e);

38 interp env (If x t e) = if (interp env x) then (interp env t) else (interp env e);

38 interp env (Bind v f) = interp env (f (interp env v));

39 interp env (Bind v f) = interp env (f (interp env v));

@@ -41,13 +42,13 @@ using (G : Vect Ty n) {

41 eId = Lam (Var fO);

42 eId = Lam (Var fO);

43 eAdd : Expr G (TyFun TyInt (TyFun TyInt TyInt));

44 eAdd : Expr G (TyFun TyInt (TyFun TyInt TyInt));

44− eAdd = Lam (Lam (Op (+) (Var fO) (Var (fS fO))));

45+ eAdd = Lam (Lam (Op' (Var fO) (Var (fS fO)) prim__addInt));

46− eDouble : Expr G (TyFun TyInt TyInt);

47+-- eDouble : Expr G (TyFun TyInt TyInt);

47− eDouble = Lam (App (App (Lam (Lam (Op (+) (Var fO) (Var (fS fO))))) (Var fO)) (Var fO));

48+-- eDouble = Lam (App (App (Lam (Lam (Op' (+) (Var fO) (Var (fS fO))))) (Var fO)) (Var fO));

49− eDouble' : Expr G (TyFun TyInt TyInt);

50+ eDouble : Expr G (TyFun TyInt TyInt);

50− eDouble' = Lam (App (App eAdd (Var fO)) (Var fO));

51+ eDouble = Lam (App (App eAdd (Var fO)) (Var fO));

52 app : |(f : Expr G (TyFun a t)) -> Expr G a -> Expr G t;

53 app : |(f : Expr G (TyFun a t)) -> Expr G a -> Expr G t;

53 app = \f, a => App f a;

54 app = \f, a => App f a;

@@ -72,10 +73,6 @@ test = interp Empty eProg 2 2;

72testFac : Int;

73testFac : Int;

73testFac = interp Empty eFac 4;

74testFac = interp Empty eFac 4;

75−intToStr : Int -> String;

76−intToStr 0 = "O";

77−intToStr n = "s" ++ intToStr (n - 1);

78−

79main : IO ();

76main : IO ();

80−main = putStrLn (intToStr testFac);

77+main = print testFac;

lib/builtins.idr+6−6

@@ -82,13 +82,13 @@ data Num : Set -> Set where

82 Num a;

84 (+) : Num a => a -> a -> a;

85− (+) {{NumInstance p s m}} x y = p x y;

85+ (+) @{ NumInstance p s m } x y = p x y;

87 (-) : Num a => a -> a -> a;

88− (-) {{NumInstance p s m}} x y = s x y;

88+ (-) @{ NumInstance p s m } x y = s x y;

90 (*) : Num a => a -> a -> a;

91− (*) {{NumInstance p s m}} x y = m x y;

91+ (*) @{ NumInstance p s m } x y = m x y;

93instance numInt : Num Int;

94instance numInt = NumInstance prim__addInt prim__subInt prim__mulInt;

@@ -102,10 +102,10 @@ data Eq : Set -> Set where

102 Eq a;

103

104 (==) : Eq a => a -> a -> Bool;

105− (==) {{EqInstance eq neq}} x y = eq x y;

105+ (==) @{ EqInstance eq neq } x y = eq x y;

106

107 (/=) : Eq a => a -> a -> Bool;

108− (/=) {{EqInstance eq neq}} x y = neq x y;

108+ (/=) @{ EqInstance eq neq } x y = neq x y;

109

110instance EqInt : Eq Int;

111instance EqInt = EqInstance (boolOp prim__eqInt) (\x, y => not (x == y));

@@ -121,7 +121,7 @@ data Ord : Set -> Set where

121 Ord a;

122

123 compare : Ord a => a -> a -> Ordering;

124− compare {{OrdInstance c}} = c;

124+ compare @{ OrdInstance c } = c;

125

126instance OrdInt : Ord Int;

127instance OrdInt = OrdInstance cmpInt where {

lib/prelude.idr+18−13

@@ -5,24 +5,13 @@ import maybe;

5import vect;

6import io;

8−---- some basic io

9−

10−putStr : String -> IO ();

11−putStr x = mkForeign (FFun "putStr" (Cons FString Nil) FUnit) x;

12−

13−putStrLn : String -> IO ();

14−putStrLn x = putStr (x ++ "\n");

15−

16−readLine : IO String;

17−readLine = mkForeign (FFun "readStr" Nil FString);

18−

19-- Show and instances

8-- Show and instances

21data Show : Set -> Set where

10data Show : Set -> Set where

22 ShowInstance : (show : a -> String) -> Show a;

11 ShowInstance : (show : a -> String) -> Show a;

24show : Show a => a -> String;

13show : Show a => a -> String;

25−show {{ShowInstance s}} v = s v;

14+show @{ShowInstance s} v = s v;

27instance showNat : Show Nat;

16instance showNat : Show Nat;

28instance showNat = ShowInstance show where {

17instance showNat = ShowInstance show where {

@@ -50,6 +39,22 @@ instance showList = ShowInstance lshow where {

50 show' : Show a => List a -> String;

39 show' : Show a => List a -> String;

51 show' Nil = "";

40 show' Nil = "";

52 show' (Cons x Nil) = show x;

41 show' (Cons x Nil) = show x;

53− show' (Cons x xs) = show x ++ ", " ++ show' xs;

42+ show' (Cons x xs') = show x ++ ", " ++ show' xs';

54 }

43 }

55}

44}

45+

46+

47+---- some basic io

48+

49+putStr : String -> IO ();

50+putStr x = mkForeign (FFun "putStr" (Cons FString Nil) FUnit) x;

51+

52+putStrLn : String -> IO ();

53+putStrLn x = putStr (x ++ "\n");

54+

55+print : Show a => a -> IO ();

56+print = putStrLn . show;

57+

58+readLine : IO String;

59+readLine = mkForeign (FFun "readStr" Nil FString);

60+

src/Core/Elaborate.hs+19−5

@@ -18,6 +18,7 @@ import Core.Typecheck

19import Control.Monad.State

20import Data.Char

21+import Data.List

21import Debug.Trace

22import Debug.Trace

23-- I don't really want this here, but it's useful for the test shell

24-- I don't really want this here, but it's useful for the test shell

@@ -118,9 +119,16 @@ get_instances = do ES p _ _ <- get

118-- given a desired hole name, return a unique hole name

119-- given a desired hole name, return a unique hole name

119unique_hole :: Name -> Elab Name

120unique_hole :: Name -> Elab Name

120unique_hole n = do ES p _ _ <- get

121unique_hole n = do ES p _ _ <- get

121− env <- get_env

122+ let bs = bound_in (pterm p)

122− return (uniqueName n (holes p ++ map fst env))

123+ return (uniqueName n (holes p ++ bs))

123 where

124 where

125+ bound_in (Bind n b sc) = n : bi b ++ bound_in sc

126+ where

127+ bi (Let t v) = bound_in t ++ bound_in v

128+ bi (Guess t v) = bound_in t ++ bound_in v

129+ bi b = bound_in (binderTy b)

130+ bound_in (App f a) = bound_in f ++ bound_in a

131+ bound_in _ = []

124

132

125elog :: String -> Elab ()

133elog :: String -> Elab ()

126elog str = do ES p logs prev <- get

134elog str = do ES p logs prev <- get

@@ -251,17 +259,23 @@ apply fn imps =

251 end_unify

259 end_unify

252 return args

260 return args

253

261

254−apply_elab :: Name -> [Maybe (Elab ())] -> Elab ()

262+apply_elab :: Name -> [Maybe (Int, Elab ())] -> Elab ()

255apply_elab n args =

263apply_elab n args =

256 do ty <- get_type (Var n)

264 do ty <- get_type (Var n)

257 ctxt <- get_context

265 ctxt <- get_context

258 env <- get_env

266 env <- get_env

259 claims <- doClaims (normalise ctxt env ty) args []

267 claims <- doClaims (normalise ctxt env ty) args []

260 prep_fill n (map fst claims)

268 prep_fill n (map fst claims)

269+ let eclaims = sortBy (\ (_, x) (_,y) -> priOrder x y) claims

261− elabClaims [] True claims

270+ elabClaims [] False claims

262 complete_fill

271 complete_fill

263 end_unify

272 end_unify

264 where

273 where

274+ priOrder Nothing Nothing = EQ

275+ priOrder Nothing _ = LT

276+ priOrder _ Nothing = GT

277+ priOrder (Just (x, _)) (Just (y, _)) = compare x y

278+

265 doClaims (Bind n' (Pi t) sc) (i : is) claims =

279 doClaims (Bind n' (Pi t) sc) (i : is) claims =

266 do n <- unique_hole (mkMN n')

280 do n <- unique_hole (mkMN n')

267 when (null claims) (start_unify n)

281 when (null claims) (start_unify n)

@@ -276,7 +290,7 @@ apply_elab n args =

276 | otherwise = if r then elabClaims [] False failed

290 | otherwise = if r then elabClaims [] False failed

277 else return ()

291 else return ()

278 elabClaims failed r ((n, Nothing) : xs) = elabClaims failed r xs

292 elabClaims failed r ((n, Nothing) : xs) = elabClaims failed r xs

279− elabClaims failed r (e@(n, Just elaboration) : xs)

293+ elabClaims failed r (e@(n, Just (_, elaboration)) : xs)

280 | r = try (do ES p _ _ <- get

294 | r = try (do ES p _ _ <- get

281 focus n; elaboration; elabClaims failed r xs)

295 focus n; elaboration; elabClaims failed r xs)

282 (elabClaims (e : failed) r xs)

296 (elabClaims (e : failed) r xs)

src/Core/ProofState.hs+11−24

@@ -257,7 +257,8 @@ complete_fill ctxt env t = fail $ "Can't complete fill at " ++ show t

257

258solve :: RunTactic

259solve ctxt env (Bind x (Guess ty val) sc)

260+ | pureTerm val = do ps <- get

260− | pureTerm val = do action (\ps -> ps { holes = holes ps \\ [x],

261+ action (\ps -> ps { holes = holes ps \\ [x],

261 instances = instances ps \\ [x] })

262 instances = instances ps \\ [x] })

262 return $ {- Bind x (Let ty val) sc -} instantiate val (pToV x sc)

263 return $ {- Bind x (Let ty val) sc -} instantiate val (pToV x sc)

263 | otherwise = fail $ "I see a hole in your solution. " ++ showEnv env val

264 | otherwise = fail $ "I see a hole in your solution. " ++ showEnv env val

@@ -365,21 +366,15 @@ solve_unified ctxt env tm =

365 action (\ps -> ps { holes = holes ps \\ map fst ns })

366 action (\ps -> ps { holes = holes ps \\ map fst ns })

366-- action (\ps -> ps { pterm = updateSolved ns (pterm ps) })

367-- action (\ps -> ps { pterm = updateSolved ns (pterm ps) })

367 return (updateSolved ns tm)

368 return (updateSolved ns tm)

368− where

369+

369− updateSolved xs (Bind n (Hole ty) t)

370+updateSolved xs (Bind n (Hole ty) t)

370− | Just v <- lookup n xs = instantiate v (pToV n (updateSolved xs t))

371+ | Just v <- lookup n xs = instantiate v (pToV n (updateSolved xs t))

371− updateSolved xs (Bind n b t)

372+updateSolved xs (Bind n b t)

372− | otherwise = Bind n (fmap (updateSolved xs) b) (updateSolved xs t)

373+ | otherwise = Bind n (fmap (updateSolved xs) b) (updateSolved xs t)

373− updateSolved xs (App f a) = App (updateSolved xs f) (updateSolved xs a)

374+updateSolved xs (App f a) = App (updateSolved xs f) (updateSolved xs a)

374− updateSolved xs (P _ n _)

375+updateSolved xs (P _ n _)

375− | Just v <- lookup n xs = v

376+ | Just v <- lookup n xs = v

376− updateSolved xs t = t

377+updateSolved xs t = t

377−

378−-- shuffleHoles :: Term -> Term

379−-- shuffleHoles tm = shuffle [] tm

380−-- where

381−-- shuffle ns (Bind n b sc)

382−-- |

383

378

384processTactic :: Tactic -> ProofState -> TC (ProofState, String)

379processTactic :: Tactic -> ProofState -> TC (ProofState, String)

385processTactic QED ps = case holes ps of

380processTactic QED ps = case holes ps of

@@ -398,14 +393,6 @@ processTactic EndUnify ps = let (h, ns) = unified ps

398 unified = (h, []),

393 unified = (h, []),

399 holes = holes ps \\ map fst ns }, "")

394 holes = holes ps \\ map fst ns }, "")

400 where

395 where

401− updateSolved xs (Bind n (Hole ty) t)

402− | Just v <- lookup n xs = instantiate v (pToV n (updateSolved xs t))

403− updateSolved xs (Bind n b t)

404− | otherwise = Bind n (fmap (updateSolved xs) b) (updateSolved xs t)

405− updateSolved xs (App f a) = App (updateSolved xs f) (updateSolved xs a)

406− updateSolved xs (P _ n _)

407− | Just v <- lookup n xs = v

408− updateSolved xs t = t

409processTactic t ps

396processTactic t ps

410 = case holes ps of

397 = case holes ps of

411 [] -> fail "Nothing to fill in."

398 [] -> fail "Nothing to fill in."

src/Idris/AbsSyntax.hs+63−26

@@ -294,14 +294,21 @@ data PDo' t = DoExp FC t

294

295type PDo = PDo' PTerm

296

297+-- The priority gives a hint as to elaboration order. Best to elaborate

298+-- things early which will help give a more concrete type to other

299+-- variables, e.g. a before (interpTy a).

300+

301+data PArg' t = PImp { priority :: Int,

297−data PArg' t = PImp { lazyarg :: Bool, pname :: Name, getTm :: t }

302+ lazyarg :: Bool, pname :: Name, getTm :: t }

303+ | PExp { priority :: Int,

298− | PExp { lazyarg :: Bool, getTm :: t }

304+ lazyarg :: Bool, getTm :: t }

305+ | PConstraint { priority :: Int,

299− | PConstraint { lazyarg :: Bool, getTm :: t }

306+ lazyarg :: Bool, getTm :: t }

300 deriving (Show, Eq, Functor)

307 deriving (Show, Eq, Functor)

301

308

302−pimp = PImp False

309+pimp = PImp 0 False

303−pexp = PExp False

310+pexp = PExp 0 False

304−pconst = PConstraint False

311+pconst = PConstraint 0 False

305

312

306type PArg = PArg' PTerm

313type PArg = PArg' PTerm

307

314

@@ -370,17 +377,17 @@ showDImp impl (PDatadecl n ty cons)

370

377

371getImps :: [PArg] -> [(Name, PTerm)]

378getImps :: [PArg] -> [(Name, PTerm)]

372getImps [] = []

379getImps [] = []

373−getImps (PImp _ n tm : xs) = (n, tm) : getImps xs

380+getImps (PImp _ _ n tm : xs) = (n, tm) : getImps xs

374getImps (_ : xs) = getImps xs

381getImps (_ : xs) = getImps xs

375

382

376getExps :: [PArg] -> [PTerm]

383getExps :: [PArg] -> [PTerm]

377getExps [] = []

384getExps [] = []

378−getExps (PExp _ tm : xs) = tm : getExps xs

385+getExps (PExp _ _ tm : xs) = tm : getExps xs

379getExps (_ : xs) = getExps xs

386getExps (_ : xs) = getExps xs

380

387

381getConsts :: [PArg] -> [PTerm]

388getConsts :: [PArg] -> [PTerm]

382getConsts [] = []

389getConsts [] = []

383−getConsts (PConstraint _ tm : xs) = tm : getConsts xs

390+getConsts (PConstraint _ _ tm : xs) = tm : getConsts xs

384getConsts (_ : xs) = getConsts xs

391getConsts (_ : xs) = getConsts xs

385

392

386getAll :: [PArg] -> [PTerm]

393getAll :: [PArg] -> [PTerm]

@@ -420,10 +427,9 @@ showImp impl tm = se 10 tm where

420 = let [l, r] = getExps args in

427 = let [l, r] = getExps args in

421 bracket p 1 $ se 1 l ++ " " ++ show op ++ " " ++ se 0 r

428 bracket p 1 $ se 1 l ++ " " ++ show op ++ " " ++ se 0 r

422 se p (PApp _ f as)

429 se p (PApp _ f as)

423− = let (imps, cs, args) = (getImps as, getConsts as, getExps as) in

430+ = let args = getExps as in

424− bracket p 1 $ se 1 f ++ concatMap scArg cs

425− ++ (if impl then concatMap siArg imps else "")

431+ bracket p 1 $ se 1 f ++ if impl then concatMap sArg as

426− ++ concatMap seArg args

432+ else concatMap seArg args

427 se p (PHidden tm) = "." ++ se 0 tm

433 se p (PHidden tm) = "." ++ se 0 tm

428 se p (PRefl _) = "refl"

434 se p (PRefl _) = "refl"

429 se p (PResolveTC _) = "resolvetc"

435 se p (PResolveTC _) = "resolvetc"

@@ -438,6 +444,10 @@ showImp impl tm = se 10 tm where

438 se p (PMetavar n) = "?" ++ show n

444 se p (PMetavar n) = "?" ++ show n

439 se p Placeholder = "_"

445 se p Placeholder = "_"

440

446

447+ sArg (PImp _ _ n tm) = siArg (n, tm)

448+ sArg (PExp _ _ tm) = seArg tm

449+ sArg (PConstraint _ _ tm) = scArg tm

450+

441 seArg arg = " " ++ se 0 arg

451 seArg arg = " " ++ se 0 arg

442 siArg (n, val) = " {" ++ show n ++ " = " ++ se 10 val ++ "}"

452 siArg (n, val) = " {" ++ show n ++ " = " ++ se 10 val ++ "}"

443 scArg val = " {{" ++ se 10 val ++ "}}"

453 scArg val = " {{" ++ se 10 val ++ "}}"

@@ -592,6 +602,33 @@ expandParamsD dec ps ns (PClauses fc n cs)

592 (map (expandParamsD dec ps ns) ds)

602 (map (expandParamsD dec ps ns) ds)

593expandParamsD dec ps ns d = d

603expandParamsD dec ps ns d = d

594

604

605+-- Calculate a priority for a type, for deciding elaboration order

606+-- * if it's just a type variable or concrete type, do it early (0)

607+-- * if there's only type variables and injective constructors, do it next (1)

608+-- * if there's a function type, next (2)

609+-- * finally, everything else (3)

610+

611+getPriority :: IState -> PTerm -> Int

612+getPriority i tm = pri tm

613+ where

614+ pri (PRef _ n) =

615+ case lookupP n (tt_ctxt i) of

616+ Just (P (DCon _ _) _ _) -> 1

617+ Just (P (TCon _ _) _ _) -> 1

618+ Just (P Ref _ _) -> 3

619+ Nothing -> 0 -- must be locally bound, if it's not an error...

620+ pri (PPi _ _ x y) = max 4 (max (pri x) (pri y))

621+ pri (PTrue _) = 0

622+ pri (PFalse _) = 0

623+ pri (PRefl _) = 1

624+ pri (PEq _ l r) = max 1 (max (pri l) (pri r))

625+ pri (PApp _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))

626+ pri (PPair _ l r) = max 1 (max (pri l) (pri r))

627+ pri (PDPair _ l r) = max 1 (max (pri l) (pri r))

628+ pri (PConstant _) = 0

629+ pri Placeholder = 1

630+ pri _ = 3

631+

595-- Dealing with implicit arguments

632-- Dealing with implicit arguments

596

633

597-- Add implicit Pi bindings for any names in the term which appear in an

634-- Add implicit Pi bindings for any names in the term which appear in an

@@ -631,7 +668,7 @@ implicitise syn ist tm

631 imps top env (PPi (Imp l _) n ty sc)

668 imps top env (PPi (Imp l _) n ty sc)

632 = do let isn = nub (namesIn ist ty) `dropAll` [n]

669 = do let isn = nub (namesIn ist ty) `dropAll` [n]

633 (decls , ns) <- get

670 (decls , ns) <- get

634− put (PImp l n ty : decls,

671+ put (PImp (getPriority ist ty) l n ty : decls,

635 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))

672 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))

636 imps True (n:env) sc

673 imps True (n:env) sc

637 imps top env (PPi (Exp l _) n ty sc)

674 imps top env (PPi (Exp l _) n ty sc)

@@ -639,7 +676,7 @@ implicitise syn ist tm

639 (PRef _ x) -> namesIn ist sc `dropAll` [n]

676 (PRef _ x) -> namesIn ist sc `dropAll` [n]

640 _ -> [])

677 _ -> [])

641 (decls, ns) <- get -- ignore decls in HO types

678 (decls, ns) <- get -- ignore decls in HO types

642− put (PExp l ty : decls,

679+ put (PExp (getPriority ist ty) l ty : decls,

643 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))

680 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))

644 imps True (n:env) sc

681 imps True (n:env) sc

645 imps top env (PPi (Constraint l _) n ty sc)

682 imps top env (PPi (Constraint l _) n ty sc)

@@ -647,7 +684,7 @@ implicitise syn ist tm

647 (PRef _ x) -> namesIn ist sc `dropAll` [n]

684 (PRef _ x) -> namesIn ist sc `dropAll` [n]

648 _ -> [])

685 _ -> [])

649 (decls, ns) <- get -- ignore decls in HO types

686 (decls, ns) <- get -- ignore decls in HO types

650− put (PConstraint l ty : decls,

687+ put (PConstraint 10 l ty : decls,

651 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))

688 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))

652 imps True (n:env) sc

689 imps True (n:env) sc

653 imps top env (PEq _ l r)

690 imps top env (PEq _ l r)

@@ -723,21 +760,21 @@ aiFn ist fc f as

723 Nothing -> mkPApp fc 1 (PRef fc f) as

760 Nothing -> mkPApp fc 1 (PRef fc f) as

724 where

761 where

725 insertImpl :: [PArg] -> [PArg] -> [PArg]

762 insertImpl :: [PArg] -> [PArg] -> [PArg]

726− insertImpl (PExp l ty : ps) (PExp _ tm : given) =

763+ insertImpl (PExp p l ty : ps) (PExp _ _ tm : given) =

727− PExp l tm : insertImpl ps given

764+ PExp p l tm : insertImpl ps given

728− insertImpl (PConstraint l ty : ps) (PConstraint _ tm : given) =

765+ insertImpl (PConstraint p l ty : ps) (PConstraint _ _ tm : given) =

729− PConstraint l tm : insertImpl ps given

766+ PConstraint p l tm : insertImpl ps given

730− insertImpl (PConstraint l ty : ps) given =

767+ insertImpl (PConstraint p l ty : ps) given =

731− PConstraint l (PResolveTC fc) : insertImpl ps given

768+ PConstraint p l (PResolveTC fc) : insertImpl ps given

732− insertImpl (PImp l n ty : ps) given =

769+ insertImpl (PImp p l n ty : ps) given =

733 case find n given [] of

770 case find n given [] of

734− Just (tm, given') -> PImp l n tm : insertImpl ps given'

771+ Just (tm, given') -> PImp p l n tm : insertImpl ps given'

735− Nothing -> PImp l n Placeholder : insertImpl ps given

772+ Nothing -> PImp p l n Placeholder : insertImpl ps given

736 insertImpl expected [] = []

773 insertImpl expected [] = []

737 insertImpl [] given = given

774 insertImpl [] given = given

738

775

739 find n [] acc = Nothing

776 find n [] acc = Nothing

740− find n (PImp _ n' t : gs) acc

777+ find n (PImp _ _ n' t : gs) acc

741 | n == n' = Just (t, reverse acc ++ gs)

778 | n == n' = Just (t, reverse acc ++ gs)

742 find n (g : gs) acc = find n gs (g : acc)

779 find n (g : gs) acc = find n gs (g : acc)

743

780

src/Idris/Delaborate.hs+3−3

@@ -43,9 +43,9 @@ delab ist tm = de [] tm

43 = PApp un (PRef un n) (zipWith imp (imps ++ repeat (pexp undefined)) args)

44 | otherwise = PApp un (PRef un n) (map pexp args)

46− imp (PImp l n _) arg = PImp l n arg

46+ imp (PImp p l n _) arg = PImp p l n arg

47− imp (PExp l _) arg = PExp l arg

47+ imp (PExp p l _) arg = PExp p l arg

48− imp (PConstraint l _) arg = PConstraint l arg

48+ imp (PConstraint p l _) arg = PConstraint p l arg

50pshow :: IState -> Err -> String

51pshow i (Msg s) = s

src/Idris/ElabDecls.hs+13−6

@@ -354,14 +354,17 @@ elab ist info pattern tm

354

355 toElab arg = case getTm arg of

356 Placeholder -> Nothing

357− v -> Just (elabE v)

357+ v -> Just (priority arg, elabE v)

358

359 mkPat = do hs <- get_holes

360 case hs of

361 (h: hs) -> do patvar h; mkPat

362 [] -> return ()

363

364+ elabE t = {- do g <- goal

365+ tm <- get_term

366+ trace ("Elaborating " ++ show t ++ " : " ++ show g ++ "\n\tin " ++ show tm)

364− elabE t = elab' t

367+ $ -} elab' t

365

368

366 local f = do e <- get_env

369 local f = do e <- get_env

367 return (f `elem` map fst e)

370 return (f `elem` map fst e)

@@ -437,7 +440,11 @@ elab ist info pattern tm

437 ivs <- get_instances

440 ivs <- get_instances

438 try (do ns <- apply (Var f) (map isph args)

441 try (do ns <- apply (Var f) (map isph args)

439 solve

442 solve

443+ let (ns', eargs)

444+ = unzip $

445+ sortBy (\(_,x) (_,y) -> compare (priority x) (priority y))

446+ (zip ns args)

440− elabArgs [] True ns (map (\x -> (lazyarg x, getTm x)) args))

447+ elabArgs [] False ns' (map (\x -> (lazyarg x, getTm x)) eargs))

441 (do apply_elab f (map toElab args)

448 (do apply_elab f (map toElab args)

442 solve)

449 solve)

443 ivs' <- get_instances

450 ivs' <- get_instances

@@ -450,7 +457,7 @@ elab ist info pattern tm

450-- trace (show ivs ++ "\n" ++ show t) $

457-- trace (show ivs ++ "\n" ++ show t) $

451-- mapM_ (\n -> do focus n

458-- mapM_ (\n -> do focus n

452-- resolveTC ist) ivs

459-- resolveTC ist) ivs

453− where tcArg (n, PConstraint _ Placeholder) = True

460+ where tcArg (n, PConstraint _ _ Placeholder) = True

454 tcArg _ = False

461 tcArg _ = False

455

462

456 elab' (PApp fc f [arg])

463 elab' (PApp fc f [arg])

@@ -516,7 +523,7 @@ resolveTC depth ist

516 resolveTC (depth - 1) ist)

523 resolveTC (depth - 1) ist)

517 (filter (\ (x, y) -> not x) (zip imps args))

524 (filter (\ (x, y) -> not x) (zip imps args))

518 solve

525 solve

519− where isImp (PImp _ _ _) = True

526+ where isImp (PImp _ _ _ _) = True

520 isImp _ = False

527 isImp _ = False

521

528

522collectDeferred :: Term -> State [(Name, Type)] Term

529collectDeferred :: Term -> State [(Name, Type)] Term

@@ -552,7 +559,7 @@ runTac autoSolve ist tac = runT (fmap (addImpl ist) tac) where

552 Just args -> map isImp args

559 Just args -> map isImp args

553 ns <- apply (Var fn) imps

560 ns <- apply (Var fn) imps

554 when autoSolve solveAll

561 when autoSolve solveAll

555− where isImp (PImp _ _ _) = True

562+ where isImp (PImp _ _ _ _) = True

556 isImp _ = False

563 isImp _ = False

557 runT (Refine fn imps) = do ns <- apply (Var fn) imps

564 runT (Refine fn imps) = do ns <- apply (Var fn) imps

558 when autoSolve solveAll

565 when autoSolve solveAll

src/Idris/Parser.hs+5−5

@@ -393,7 +393,7 @@ pImplicitArg syn = do lchar '{'; n <- pName

393 lchar '}'

394 return (pimp n v)

395

396−pConstraintArg syn = do symbol "{{"; e <- pExpr syn; symbol "}}"

396+pConstraintArg syn = do symbol "@{"; e <- pExpr syn; symbol "}"

397 return (pconst e)

398

399pTSig syn = do lchar ':'

@@ -576,13 +576,13 @@ pClause syn

576 rhs <- pExpr syn

577 ist <- getState

578 let ctxt = tt_ctxt ist

579− let wsyn = whereSyn n syn (map getTm cargs ++

579+ let wsyn = whereSyn n syn (map getTm iargs ++

580− map getTm iargs ++

580+ map getTm cargs ++

581 args ++ wargs)

582 (wheres, nmap) <- choice [pWhereblock n syn, do lchar ';'

583 return ([], [])]

584 return $ PClause n (PApp fc (PRef fc n)

585− (cargs ++ iargs ++ map pexp args)) wargs rhs wheres)

585+ (iargs ++ cargs ++ map pexp args)) wargs rhs wheres)

586 <|> try (do n <- pfName

587 cargs <- many (pConstraintArg syn)

588 iargs <- many (pImplicitArg syn)

@@ -596,7 +596,7 @@ pClause syn

596 let withs = concat ds

597 lchar '}'

598 return $ PWith n (PApp fc (PRef fc n)

599− (cargs ++ iargs ++ map pexp args)) wargs wval withs)

599+ (iargs ++ cargs ++ map pexp args)) wargs wval withs)

600

601 <|> do l <- pSimpleExpr syn

602 op <- operator