80a67c5 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Fix implicit arguments in syntax rules

commit80a67c514c3393bb03295a6f63a529413d7209eb authorEdwin Brady <ecb10@st-andrews.ac.uk> dateFri 17 Jan 2014, 18:41 (13 years ago) parent70ee9ef

2 files changed+11−5

unifiedsplit

src/Idris/AbsSyntax.hs+2−1

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

13251325 case find n given [] of

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

13271327 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

13291330 case find n given [] of

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

13311332 Nothing -> if inpat

src/Idris/ElabTerm.hs+9−4

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

418418 ctxt <- get_context

419419 let guarded = isConName f ctxt

420420 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

422422 let (ns', eargs) = unzip $

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

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

425− (zip ns args)

423+ sortBy cmpArg (zip ns args)

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

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

428426 solve

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

442440 (ivs' \\ ivs)

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

444442 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

445450

446451 tacTm (PTactics _) = True

447452 tacTm (PProof _) = True