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

git.iko.soy/Idris-dev

on master help sign in

Fix disambiguation on LHS

4ade674Edwin Brady10 years ago

src/Idris/AbsSyntax.hs+15−1

compare with master

unifiedsplit

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

2204 su (PAlternative ms b alts)

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

2206 if null alts' then Placeholder

2207− else PAlternative ms b alts'

2207+ else liftHidden $ PAlternative ms b alts'

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

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

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

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

2214

2215 ctxt = tt_ctxt i

2216

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+

2217stripUnmatchable i tm = tm

2231stripUnmatchable i tm = tm

2218

2232

2219mkPApp fc a f [] = f

2233mkPApp fc a f [] = f

src/Idris/Core/Elaborate.hs+2

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

963 = do s <- get

964 ps <- get_probs

965 ivs <- get_implementations

966+ g <- goal

966 case prunStateT pmax True ps (if constrok then Nothing

967 case prunStateT pmax True ps (if constrok then Nothing

967 else Just ivs) x s of

968 else Just ivs) x s of

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

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

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

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

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

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

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

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

973+ put s

972 doAll cs' newps xs

974 doAll cs' newps xs

973 Error err -> do put s

975 Error err -> do put s

974 doAll cs pmax xs

976 doAll cs pmax xs

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

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

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

506 showHd (PRef _ _ n) = return n

507 showHd (PApp _ h _) = showHd h

508+ showHd (PHidden h) = showHd h

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

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

509

510

510 doPrune as =

511 doPrune as =

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

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

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

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

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

1294 movelast h

1295 movelast h

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

1295− delayElab 10 $ do hs <- get_holes

1301+ elabHidden h = do hs <- get_holes

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

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

1297− focus h

1303+ focus h

1298− dotterm

1304+ dotterm

1299− elab' ina fc t

1305+ elab' ina fc t

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

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

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

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

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

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