4ade674 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Fix disambiguation on LHS

There was a potential problem with ambiguity on the LHS with forced patterns, since the disambiguation happened at the wrong time. Any list of alternatives with PHidden need to have the PHidden lifted out.

commit4ade67482fb3a81a2df4330552c92b5e3c03d124 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateWed 15 Mar 2017, 18:46 (10 years ago) parent2debf36

3 files changed+28−6

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+15−1 src/Idris/Core/Elaborate.hs+2 src/Idris/Elab/Term.hs+11−5

src/Idris/AbsSyntax.hs+15−1

@@ -2204,7 +2204,7 @@ stripUnmatchable i (PApp fc fn args) = PApp fc fn (fmap (fmap su) args) where

22042204 su (PAlternative ms b alts)

22052205 = let alts' = filter (/= Placeholder) (map su alts) in

22062206 if null alts' then Placeholder

2207− else PAlternative ms b alts'

2207+ else liftHidden $ PAlternative ms b alts'

22082208 su (PPair fc hls p l r) = PPair fc hls p (su l) (su r)

22092209 su (PDPair fc hls p l t r) = PDPair fc hls p (su l) (su t) (su r)

22102210 su t@(PLam fc _ _ _ _) = PHidden t

@@ -2214,6 +2214,20 @@ stripUnmatchable i (PApp fc fn args) = PApp fc fn (fmap (fmap su) args) where

22142214

22152215 ctxt = tt_ctxt i

22162216

2217+ -- If the ambiguous terms are all hidden, the PHidden needs to be outside

2218+ -- because elaboration of PHidden gets delayed, and we need the elaboration

2219+ -- to resolve the ambiguity.

2220+ liftHidden tm@(PAlternative ms b as)

2221+ | allHidden as = PHidden (PAlternative ms b (map unHide as))

2222+ | otherwise = tm

2223+

2224+ allHidden [] = True

2225+ allHidden (PHidden _ : xs) = allHidden xs

2226+ allHidden (x : xs) = False

2227+

2228+ unHide (PHidden t) = t

2229+ unHide t = t

2230+

22172231stripUnmatchable i tm = tm

22182232

22192233mkPApp fc a f [] = f

src/Idris/Core/Elaborate.hs+2

@@ -963,12 +963,14 @@ tryAll' constrok xs = doAll [] 999999 xs

963963 = do s <- get

964964 ps <- get_probs

965965 ivs <- get_implementations

966+ g <- goal

966967 case prunStateT pmax True ps (if constrok then Nothing

967968 else Just ivs) x s of

968969 OK ((v, newps, probs), s') ->

969970 do let cs' = if (newps < pmax)

970971 then [do put s'; return $! v]

971972 else (do put s'; return $! v) : cs

973+ put s

972974 doAll cs' newps xs

973975 Error err -> do put s

974976 doAll cs pmax xs

src/Idris/Elab/Term.hs+11−5

@@ -505,6 +505,7 @@ elab ist info emode opts fn tm

505505 showHd (PApp _ (PRef _ _ n) _) = return n

506506 showHd (PRef _ _ n) = return n

507507 showHd (PApp _ h _) = showHd h

508+ showHd (PHidden h) = showHd h

508509 showHd x = getNameFrom (sMN 0 "_") -- We probably should do something better than this here

509510

510511 doPrune as =

@@ -1292,11 +1293,16 @@ elab ist info emode opts fn tm

12921293 -- Delay dotted things to the end, then when we elaborate them

12931294 -- we can check the result against what was inferred

12941295 movelast h

1295− delayElab 10 $ do hs <- get_holes

1296− when (h `elem` hs) $ do

1297− focus h

1298− dotterm

1299− elab' ina fc t

1296+ (h' : hs) <- get_holes

1297+ -- If we're at the end anyway, do it now

1298+ if h == h' then elabHidden h

1299+ else delayElab 10 $ elabHidden h

1300+ where

1301+ elabHidden h = do hs <- get_holes

1302+ when (h `elem` hs) $ do

1303+ focus h

1304+ dotterm

1305+ elab' ina fc t

13001306 elab' ina fc (PRunElab fc' tm ns) =

13011307 do unless (ElabReflection `elem` idris_language_extensions ist) $

13021308 lift $ tfail $ At fc' (Msg "You must turn on the ElabReflection extension to use %runElab")