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

git.iko.soy/Idris-dev

on master help sign in

Merge branch 'master' of git://github.com/edwinb/Idris-dev

4b0c8a7Andreas Bogk13 years ago

effects/Effects.idr+3−1

compare with master

unifiedsplit

@@ -48,6 +48,8 @@ updateWith : (ys' : List a) -> (xs : List a) ->

48updateWith (y :: ys) (x :: xs) (Keep rest) = y :: updateWith ys xs rest

49updateWith ys (x :: xs) (Drop rest) = x :: updateWith ys xs rest

50updateWith [] [] SubNil = []

51+updateWith (y :: ys) [] SubNil = y :: ys

52+updateWith [] (x :: xs) (Keep rest) = []

52-- put things back, replacing old with new in the sub-environment

54-- put things back, replacing old with new in the sub-environment

53rebuildEnv : Env m ys' -> (prf : SubList ys xs) ->

55rebuildEnv : Env m ys' -> (prf : SubList ys xs) ->

@@ -55,6 +57,7 @@ rebuildEnv : Env m ys' -> (prf : SubList ys xs) ->

55rebuildEnv [] SubNil env = env

57rebuildEnv [] SubNil env = env

56rebuildEnv (x :: xs) (Keep rest) (y :: env) = x :: rebuildEnv xs rest env

58rebuildEnv (x :: xs) (Keep rest) (y :: env) = x :: rebuildEnv xs rest env

57rebuildEnv xs (Drop rest) (y :: env) = y :: rebuildEnv xs rest env

59rebuildEnv xs (Drop rest) (y :: env) = y :: rebuildEnv xs rest env

60+rebuildEnv (x :: xs) SubNil [] = x :: xs

59---- The Effect EDSL itself ----

62---- The Effect EDSL itself ----

@@ -210,4 +213,3 @@ mapE f (x :: xs) = [| f x :: mapE f xs |]

210when : Applicative m => Bool -> Eff m xs () -> Eff m xs ()

213when : Applicative m => Bool -> Eff m xs () -> Eff m xs ()

211when True e = e

214when True e = e

212when False e = pure ()

215when False e = pure ()

213−

lib/Prelude/List.idr+1

@@ -399,6 +399,7 @@ span p (x::xs) =

399break : (a -> Bool) -> List a -> (List a, List a)

400break p = span (not . p)

401

402+%assert_total

402split : (a -> Bool) -> List a -> List (List a)

403split : (a -> Bool) -> List a -> List (List a)

403split p [] = []

404split p [] = []

404split p xs =

405split p xs =

src/Core/CaseTree.hs+12−6

@@ -351,10 +351,13 @@ argsToAlt rs@((r, m) : rest)

351 return (newArgs, addRs rs)

352 where

353 getNewVars [] = return []

354− getNewVars ((PV n) : ns) = do v <- getVar

354+ getNewVars ((PV n) : ns) = do v <- getVar "e"

355 nsv <- getNewVars ns

356 return (v : nsv)

357+ getNewVars (PAny : ns) = do v <- getVar "i"

358+ nsv <- getNewVars ns

359+ return (v : nsv)

357− getNewVars (_ : ns) = do v <- getVar

360+ getNewVars (_ : ns) = do v <- getVar "e"

358 nsv <- getNewVars ns

361 nsv <- getNewVars ns

359 return (v : nsv)

362 return (v : nsv)

360 addRs [] = []

363 addRs [] = []

@@ -363,8 +366,8 @@ argsToAlt rs@((r, m) : rest)

363 uniq i (UN n) = MN i n

366 uniq i (UN n) = MN i n

364 uniq i n = n

367 uniq i n = n

365

368

366−getVar :: State CS Name

369+getVar :: String -> State CS Name

367−getVar = do (t, v) <- get; put (t, v+1); return (MN v "e")

370+getVar b = do (t, v) <- get; put (t, v+1); return (MN v b)

368

371

369groupCons :: [Clause] -> State CS [Group]

372groupCons :: [Clause] -> State CS [Group]

370groupCons cs = gc [] cs

373groupCons cs = gc [] cs

@@ -393,10 +396,12 @@ varRule (v : vs) alts err =

393 do let alts' = map (repVar v) alts

396 do let alts' = map (repVar v) alts

394 match vs alts' err

397 match vs alts' err

395 where

398 where

399+ repVar v (PV p : ps , (lhs, res))

396− repVar v (PV p : ps , (lhs, res)) = (ps, (lhs, subst p (P Bound v Erased) res))

400+ = (ps, (lhs, subst p (P Bound v Erased) res))

397 repVar v (PAny : ps , res) = (ps, res)

401 repVar v (PAny : ps , res) = (ps, res)

398

402

399-- fix: case e of S k -> f (S k) ==> case e of S k -> f e

403-- fix: case e of S k -> f (S k) ==> case e of S k -> f e

404+

400depatt :: [Name] -> SC -> SC

405depatt :: [Name] -> SC -> SC

401depatt ns tm = dp [] tm

406depatt ns tm = dp [] tm

402 where

407 where

@@ -419,8 +424,9 @@ depatt ns tm = dp [] tm

419 | and ((length args == length args') :

424 | and ((length args == length args') :

420 (n == cn) : zipWith same args args') = P Ref x Erased

425 (n == cn) : zipWith same args args') = P Ref x Erased

421 | otherwise = applyMap ms nt cn pty args'

426 | otherwise = applyMap ms nt cn pty args'

422− same n (P _ n' _) = n == n'

427+ same n (P _ n' _) = n == n'

423 same _ _ = False

428 same _ _ = False

429+

424 applyMaps ms (App f a) = App (applyMaps ms f) (applyMaps ms a)

430 applyMaps ms (App f a) = App (applyMaps ms f) (applyMaps ms a)

425 applyMaps ms t = t

431 applyMaps ms t = t

426

432

src/Core/Evaluate.hs+6−4

@@ -91,8 +91,9 @@ specialise ctxt env limits t

91simplify :: Context -> Bool -> Env -> TT Name -> TT Name

92simplify ctxt runtime env t

93 = evalState (do val <- eval False ctxt [(UN "lazy", 0),

94+ (UN "assert_smaller", 0),

94− (UN "par", 0),

95+ (UN "par", 0),

95− (UN "fork", 0)]

96+ (UN "fork", 0)]

96 (map finalEntry env) (finalise t)

97 (map finalEntry env) (finalise t)

97 [Simplify runtime]

98 [Simplify runtime]

98 quote 0 val) initEval

99 quote 0 val) initEval

@@ -751,11 +752,12 @@ simplifyCasedef n uctxt

751 [(CaseOp inl inr ty [] ps args sc args' sc', acc, tot)] ->

752 [(CaseOp inl inr ty [] ps args sc args' sc', acc, tot)] ->

752 ctxt -- nothing to simplify (or already done...)

753 ctxt -- nothing to simplify (or already done...)

753 [(CaseOp inl inr ty ps_in ps args sc args' sc', acc, tot)] ->

754 [(CaseOp inl inr ty ps_in ps args sc args' sc', acc, tot)] ->

755+ let ps_in' = map simpl ps_in

754− let pdef = map debind $ map simpl ps_in in

756+ pdef = map debind ps_in' in

755 case simpleCase False True CompileTime (FC "" 0) pdef of

757 case simpleCase False True CompileTime (FC "" 0) pdef of

756 OK (CaseDef args sc _) ->

758 OK (CaseDef args sc _) ->

757 addDef n (CaseOp inl inr

759 addDef n (CaseOp inl inr

758− ty ps_in ps args sc args' sc',

760+ ty ps_in' ps args sc args' sc',

759 acc, tot) ctxt

761 acc, tot) ctxt

760 _ -> ctxt in

762 _ -> ctxt in

761 uctxt { definitions = ctxt' }

763 uctxt { definitions = ctxt' }

src/IRTS/Compiler.hs+2

@@ -169,6 +169,8 @@ instance ToIR (TT Name) where

169 | (P _ (UN "lazy") _, [_, arg]) <- unApply tm

170 = do arg' <- ir' env arg

171 return $ LLazyExp arg'

172+ | (P _ (UN "assert_smaller") _, [_, _, _, arg]) <- unApply tm

173+ = ir' env arg

172 | (P _ (UN "par") _, [_, arg]) <- unApply tm

174 | (P _ (UN "par") _, [_, arg]) <- unApply tm

173 = do arg' <- ir' env arg

175 = do arg' <- ir' env arg

174 return $ LOp LPar [LLazyExp arg']

176 return $ LOp LPar [LLazyExp arg']

src/Idris/Coverage.hs+75−4

@@ -311,15 +311,85 @@ buildSCG (_, n) = do

311 ist <- getIState

312 case lookupCtxt n (idris_callgraph ist) of

313 [cg] -> case lookupDef n (tt_ctxt ist) of

314− [CaseOp _ _ _ _ _ args sc _ _] ->

314+ [CaseOp _ _ _ pats _ args sc _ _] ->

315− do logLvl 3 $ "Building SCG for " ++ show n ++ " from\n"

315+ do logLvl 2 $ "Building SCG for " ++ show n ++ " from\n"

316− ++ show sc

316+ ++ show pats ++ "\n" ++ show sc

317− let newscg = buildSCG' ist sc args

317+ let newscg = buildSCG' ist (rights pats) args

318 logLvl 5 $ show newscg

319 addToCG n ( cg { scg = newscg } )

320 [] -> logLvl 5 $ "Could not build SCG for " ++ show n ++ "\n"

321 x -> error $ "buildSCG: " ++ show (n, x)

322

323+buildSCG' :: IState -> [(Term, Term)] -> [Name] -> [SCGEntry]

324+buildSCG' ist pats args = nub $ concatMap scgPat pats where

325+ scgPat (lhs, rhs) = let (f, pargs) = unApply (dePat lhs) in

326+ findCalls (dePat rhs) (patvars lhs) pargs

327+

328+ findCalls ap@(App f a) pvs pargs

329+ | (P _ (UN "lazy") _, [_, arg]) <- unApply ap

330+ = findCalls arg pvs pargs

331+ | (P _ n _, args) <- unApply ap

332+ = mkChange n args pargs ++

333+ concatMap (\x -> findCalls x pvs pargs) args

334+ findCalls (App f a) pvs pargs

335+ = findCalls f pvs pargs ++ findCalls a pvs pargs

336+ findCalls (Bind n (Let t v) e) pvs pargs

337+ = findCalls v pvs pargs ++ findCalls e (n : pvs) pargs

338+ findCalls (Bind n _ e) pvs pargs

339+ = findCalls e (n : pvs) pargs

340+ findCalls (P _ f _ ) pvs pargs

341+ | not (f `elem` pvs) = [(f, [])]

342+ findCalls _ _ _ = []

343+

344+ mkChange n args pargs = [(n, sizes args)]

345+ where

346+ sizes [] = []

347+ sizes (a : as) = checkSize a pargs 0 : sizes as

348+

349+ -- find which argument in pargs <a> is smaller than, if any

350+ checkSize a (p : ps) i

351+ | a == p = Just (i, Same)

352+ | smaller Nothing a (p, Nothing) = Just (i, Smaller)

353+ | otherwise = checkSize a ps (i + 1)

354+ checkSize a [] i = Nothing

355+

356+ -- the smaller thing we find must be the same type as <a>, and

357+ -- not be coinductive - so carry the type of the constructor we've

358+ -- gone under.

359+

360+ smaller (Just tyn) a (t, Just tyt)

361+ | a == t = isInductive (fst (unApply (getRetTy tyn)))

362+ (fst (unApply (getRetTy tyt)))

363+ smaller ty a (ap@(App f s), _)

364+ | (P (DCon _ _) n _, args) <- unApply ap

365+ = let tyn = getType n in

366+ any (smaller (ty `mplus` Just tyn) a)

367+ (zip args (map toJust (getArgTys tyn)))

368+ -- check higher order recursive arguments

369+ smaller ty (App f s) a = smaller ty f a

370+ smaller _ _ _ = False

371+

372+ toJust (n, t) = Just t

373+

374+ getType n = case lookupTy n (tt_ctxt ist) of

375+ [ty] -> ty -- must exist

376+

377+ isInductive (P _ nty _) (P _ nty' _) =

378+ let co = case lookupCtxt nty (idris_datatypes ist) of

379+ [TI _ x _] -> x

380+ _ -> False in

381+ nty == nty' && not co

382+ isInductive _ _ = False

383+

384+-- getTypeFam t | (P _ n _, _) <- unApply t

385+

386+ dePat (Bind x (PVar ty) sc) = dePat (instantiate (P Bound x ty) sc)

387+ dePat t = t

388+

389+ patvars (Bind x (PVar _) sc) = x : patvars sc

390+ patvars _ = []

391+

392+{-

323buildSCG' :: IState -> SC -> [Name] -> [SCGEntry]

393buildSCG' :: IState -> SC -> [Name] -> [SCGEntry]

324buildSCG' ist sc args = -- trace ("Building SCG for " ++ show sc) $

394buildSCG' ist sc args = -- trace ("Building SCG for " ++ show sc) $

325 nub $ scg sc (zip args args)

395 nub $ scg sc (zip args args)

@@ -406,6 +476,7 @@ buildSCG' ist sc args = -- trace ("Building SCG for " ++ show sc) $

406 getArgPos i n [] = Nothing

476 getArgPos i n [] = Nothing

407 getArgPos i n (x : xs) | n == x = Just i

477 getArgPos i n (x : xs) | n == x = Just i

408 | otherwise = getArgPos (i + 1) n xs

478 | otherwise = getArgPos (i + 1) n xs

479+-}

409

480

410checkSizeChange :: Name -> Idris Totality

481checkSizeChange :: Name -> Idris Totality

411checkSizeChange n = do

482checkSizeChange n = do

src/Idris/ElabDecls.hs+4

@@ -458,6 +458,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

458 else stripCollapsed pats

459

460 logLvl 5 $ "Patterns:\n" ++ show pats

461+ logLvl 3 $ "SIMPLIFIED: \n" ++ show pdef

461

462

462 let optpdef = map debind $ map (simpl True (tt_ctxt ist)) optpats

463 let optpdef = map debind $ map (simpl True (tt_ctxt ist)) optpats

463 tree@(CaseDef scargs sc _) <- tclift $

464 tree@(CaseDef scargs sc _) <- tclift $

@@ -938,6 +939,9 @@ elabClass info syn doc fc constraints tn ps ds

938 -- build instance constructor type

939 -- build instance constructor type

939 -- decorate names of functions to ensure they can't be referred

940 -- decorate names of functions to ensure they can't be referred

940 -- to elsewhere in the class declaration

941 -- to elsewhere in the class declaration

942+ -- TODO: Remove mdec to make it a dependent record, which would

943+ -- allow dependent type classes, but building instances will

944+ -- then need some attention.

941 let cty = impbind ps $ conbind constraints

945 let cty = impbind ps $ conbind constraints

942 $ pibind (map (\ (n, ty) -> (mdec n, ty)) methods)

946 $ pibind (map (\ (n, ty) -> (mdec n, ty)) methods)

943 constraint

947 constraint