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

git.iko.soy/Idris-dev

on master help sign in

Fix compilation of Delay pattern

96e583cEdwin Brady10 years ago

src/IRTS/Compiler.hs+2−2

compare with master

unifiedsplit

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

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

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

531 | delay == txt "Delay"

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

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

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

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

534

535-- There are two transformations in this case:

536--

src/IRTS/Lang.hs+24

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

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

304usedIn env _ = []

305

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+

306instance Show LExp where

330instance Show LExp where

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

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

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

332 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

310 apt <- expandToArity t

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

312 ct <- insertCoerce ina itm

313− t' <- insertLazy ct

313+ t' <- insertLazy ina ct

314 g <- goal

315 tm <- get_term

316 ps <- get_probs

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

624 do patvar n

625 update_term liftPats

626 highlightSource fc (AnnBoundName n False)

627− else if (defined && not guarded)

627+ else if defined

628 then do apply (Var n) []

629 annot <- findHighlight n

630 solve

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

834 ty <- goal

835 fty <- get_type (Var f)

836 ctxt <- get_context

837+ let dataCon = isDConName f ctxt

837 annot <- findHighlight f

838 annot <- findHighlight f

838 mapM_ checkKnownImplicit args_in

839 mapM_ checkKnownImplicit args_in

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

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

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

849 then -- simple app, as below

850 then -- simple app, as below

850 do simple_app False

851 do simple_app False

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

852 (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)))

853 (show tm)

855 (show tm)

854 solve

856 solve

855 mapM (uncurry highlightSource) $

857 mapM (uncurry highlightSource) $

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

883 mapM (uncurry highlightSource) $

885 mapM (uncurry highlightSource) $

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

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

885

887

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 })

887 [] fc False f

890 [] fc False f

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

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

889 (f == sUN "Force")

892 (f == sUN "Force")

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

910 ivs' <- get_instances

913 ivs' <- get_instances

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

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

912 -- i.e. no holes in them

915 -- i.e. no holes in them

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

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

914− not (e_guarded ina))) $

915 mapM_ (\n -> do focus n

917 mapM_ (\n -> do focus n

916 g <- goal

918 g <- goal

917 env <- get_env

919 env <- get_env

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

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

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

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

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

1414 -- first.

1416 -- first.

1415− insertLazy :: PTerm -> ElabD PTerm

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

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

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

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

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

1418− insertLazy (PCoerced t) = return t

1420+ insertLazy ina (PCoerced t) = return t

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

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

1420− -- on the rhs

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

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

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

1422− insertLazy t =

1424+ insertLazy ina t =

1423 do ty <- goal

1425 do ty <- goal

1424 env <- get_env

1426 env <- get_env

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

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