efc5e25 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge branch 'master' of github.com:edwinb/Idris-dev

efc5e25Timo Petteri Sinnemäki13 years ago

src/Idris/AbsSyntax.hs+2−1

compare with master

unifiedsplit

@@ -1325,7 +1325,8 @@ aiFn inpat expat ist fc f as

1325 case find n given [] of

1326 Just (tm, given') -> PImp p False l n tm "" : insertImpl ps given'

1327 Nothing -> PImp p True l n Placeholder "" : insertImpl ps given

1328− insertImpl (PTacImplicit p l n sc ty d : ps) given =

1328+ insertImpl (PTacImplicit p l n sc' ty d : ps) given =

1329+ let sc = addImpl ist sc' in

1329 case find n given [] of

1330 case find n given [] of

1330 Just (tm, given') -> PTacImplicit p l n sc tm "" : insertImpl ps given'

1331 Just (tm, given') -> PTacImplicit p l n sc tm "" : insertImpl ps given'

1331 Nothing -> if inpat

1332 Nothing -> if inpat

src/Idris/ElabTerm.hs+9−4

@@ -418,11 +418,9 @@ elab ist info pattern opts fn tm

418 ctxt <- get_context

419 let guarded = isConName f ctxt

420 ns <- apply (Var f) (map isph args)

421− -- Sort so that the implicit tactics go last

421+ -- Sort so that the implicit tactics and alternatives go last

422 let (ns', eargs) = unzip $

423− sortBy (\(_,x) (_,y) ->

424− compare (priority x) (priority y))

425− (zip ns args)

423+ sortBy cmpArg (zip ns args)

426 elabArgs (ina || not isinf, guarded, inty)

424 elabArgs (ina || not isinf, guarded, inty)

427 [] fc False ns' (map (\x -> (lazyarg x, getTm x)) eargs)

425 [] fc False ns' (map (\x -> (lazyarg x, getTm x)) eargs)

428 solve

426 solve

@@ -442,6 +440,13 @@ elab ist info pattern opts fn tm

442 (ivs' \\ ivs)

440 (ivs' \\ ivs)

443 where tcArg (n, PConstraint _ _ Placeholder _) = True

441 where tcArg (n, PConstraint _ _ Placeholder _) = True

444 tcArg _ = False

442 tcArg _ = False

443+

444+ -- normal < tactic < default tactic

445+ cmpArg (_, x) (_, y)

446+ = compare (priority x + alt x) (priority y + alt y)

447+ where alt t = case getTm t of

448+ PAlternative False _ -> 5

449+ _ -> 0

445

450

446 tacTm (PTactics _) = True

451 tacTm (PTactics _) = True

447 tacTm (PProof _) = True

452 tacTm (PProof _) = True