96e583c · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Fix compilation of Delay pattern

When there's a Delay on the LHS, we put a Force on the RHS, but it needs to be forced at the last moment otherwise it's possible to end up forcing too early, and ending up with total programs that nevertheless don't terminate... Also a minor elaboration tweak, simplifying automatic insertion of Force/Delay by putting more Delays on the left

commit96e583cf32f8571046312cdf2fd1776c6e09b9b1 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateTue 12 Jul 2016, 14:49 (10 years ago) parent7a67b5b

3 files changed+42−16

compare with master

unifiedsplit

src/IRTS/Compiler.hs+2−2 src/IRTS/Lang.hs+24 src/Idris/Elab/Term.hs+16−14

src/IRTS/Compiler.hs+2−2

@@ -529,8 +529,8 @@ irSC top vs (ProjCase tm alts) = do

529529-- Transform matching on Delay to applications of Force.

530530irSC top vs (Case up n [ConCase (UN delay) i [_, _, n'] sc])

531531 | delay == txt "Delay"

532− = do sc' <- irSC top vs $ mkForce n' n sc

533− return $ LLet n' (LForce (LV (Glob n))) sc'

532+ = do sc' <- irSC top vs sc -- mkForce n' n sc

533+ return $ lsubst n' (LForce (LV (Glob n))) sc'

534534

535535-- There are two transformations in this case:

536536--

src/IRTS/Lang.hs+24

@@ -303,6 +303,30 @@ usedIn env (LForeign _ _ args) = concatMap (usedIn env) (map snd args)

303303usedIn env (LOp f args) = concatMap (usedIn env) args

304304usedIn env _ = []

305305

306+lsubst :: Name -> LExp -> LExp -> LExp

307+lsubst n new (LV (Glob x)) | n == x = new

308+lsubst n new (LApp t e args) = let e' = lsubst n new e

309+ args' = map (lsubst n new) args in

310+ LApp t e' args'

311+lsubst n new (LLazyApp fn args) = let args' = map (lsubst n new) args in

312+ LLazyApp fn args'

313+lsubst n new (LLazyExp e) = LLazyExp (lsubst n new e)

314+lsubst n new (LForce e) = LForce (lsubst n new e)

315+lsubst n new (LLet v val sc) = LLet v (lsubst n new val) (lsubst n new sc)

316+lsubst n new (LLam ns sc) = LLam ns (lsubst n new sc)

317+lsubst n new (LProj e i) = LProj (lsubst n new e) i

318+lsubst n new (LCon lv t cn args) = let args' = map (lsubst n new) args in

319+ LCon lv t cn args'

320+lsubst n new (LOp op args) = let args' = map (lsubst n new) args in

321+ LOp op args'

322+lsubst n new (LForeign fd rd args)

323+ = let args' = map (\(d, a) -> (d, lsubst n new a)) args in

324+ LForeign fd rd args'

325+lsubst n new (LCase t e alts) = let e' = lsubst n new e

326+ alts' = map (fmap (lsubst n new)) alts in

327+ LCase t e' alts'

328+lsubst n new tm = tm

329+

306330instance Show LExp where

307331 show e = show' [] "" e where

308332 show' env ind (LV (Loc i)) = env!!i

src/Idris/Elab/Term.hs+16−14

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

310310 apt <- expandToArity t

311311 itm <- if not pattern then insertImpLam ina apt else return apt

312312 ct <- insertCoerce ina itm

313− t' <- insertLazy ct

313+ t' <- insertLazy ina ct

314314 g <- goal

315315 tm <- get_term

316316 ps <- get_probs

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

624624 do patvar n

625625 update_term liftPats

626626 highlightSource fc (AnnBoundName n False)

627− else if (defined && not guarded)

627+ else if defined

628628 then do apply (Var n) []

629629 annot <- findHighlight n

630630 solve

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

834834 ty <- goal

835835 fty <- get_type (Var f)

836836 ctxt <- get_context

837+ let dataCon = isDConName f ctxt

837838 annot <- findHighlight f

838839 mapM_ checkKnownImplicit args_in

839840 let args = insertScopedImps fc (normalise ctxt env fty) args_in

@@ -849,7 +850,8 @@ elab ist info emode opts fn tm

849850 then -- simple app, as below

850851 do simple_app False

851852 (elabE (ina { e_isfn = True }) (Just fc) (PRef ffc hls f))

852− (elabE (ina { e_inarg = True }) (Just fc) (getTm (head args)))

853+ (elabE (ina { e_inarg = True,

854+ e_guarded = dataCon }) (Just fc) (getTm (head args)))

853855 (show tm)

854856 solve

855857 mapM (uncurry highlightSource) $

@@ -883,7 +885,8 @@ elab ist info emode opts fn tm

883885 mapM (uncurry highlightSource) $

884886 (ffc, annot) : map (\f -> (f, annot)) hls

885887

886− elabArgs ist (ina { e_inarg = e_inarg ina || not isinf })

888+ elabArgs ist (ina { e_inarg = e_inarg ina || not isinf,

889+ e_guarded = dataCon })

887890 [] fc False f

888891 (zip ns (unmatchableArgs ++ repeat False))

889892 (f == sUN "Force")

@@ -910,8 +913,7 @@ elab ist info emode opts fn tm

910913 ivs' <- get_instances

911914 -- Attempt to resolve any type classes which have 'complete' types,

912915 -- i.e. no holes in them

913− when (not pattern || (e_inarg ina && not tcgen &&

914− not (e_guarded ina))) $

916+ when (not pattern || (e_inarg ina && not tcgen)) $

915917 mapM_ (\n -> do focus n

916918 g <- goal

917919 env <- get_env

@@ -1412,14 +1414,14 @@ elab ist info emode opts fn tm

14121414 -- first. We need to do this brute force approach, rather than anything

14131415 -- more precise, since there may be various other ambiguities to resolve

14141416 -- first.

1415− insertLazy :: PTerm -> ElabD PTerm

1416− insertLazy t@(PApp _ (PRef _ _ (UN l)) _) | l == txt "Delay" = return t

1417− insertLazy t@(PApp _ (PRef _ _ (UN l)) _) | l == txt "Force" = return t

1418− insertLazy (PCoerced t) = return t

1419− -- Don't add a delay to pattern variables, since they can be forced

1420− -- on the rhs

1421− insertLazy t@(PPatvar _ _) | pattern = return t

1422− insertLazy t =

1417+ insertLazy :: ElabCtxt -> PTerm -> ElabD PTerm

1418+ insertLazy ina t@(PApp _ (PRef _ _ (UN l)) _) | l == txt "Delay" = return t

1419+ insertLazy ina t@(PApp _ (PRef _ _ (UN l)) _) | l == txt "Force" = return t

1420+ insertLazy ina (PCoerced t) = return t

1421+ -- Don't add a delay to top level pattern variables, since they

1422+ -- can be forced on the rhs if needed

1423+ insertLazy ina t@(PPatvar _ _) | pattern && not (e_guarded ina) = return t

1424+ insertLazy ina t =

14231425 do ty <- goal

14241426 env <- get_env

14251427 let (tyh, _) = unApply (normalise (tt_ctxt ist) env ty)