57136cc · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Change elaboration of interfaces

57136ccEdwin Brady10 years ago

idris.cabal+8−5

compare with master

unifiedsplit

@@ -399,11 +399,6 @@ Extra-source-files:

399 test/bignum002/*.idr

400 test/bignum002/expected

401

402− test/classes001/*.idr

403− test/classes001/run

404− test/classes001/expected

405− test/classes001/input

406−

407 test/corecords001/*.idr

402 test/corecords001/*.idr

408 test/corecords001/run

403 test/corecords001/run

409 test/corecords001/expected

404 test/corecords001/expected

@@ -608,6 +603,14 @@ Extra-source-files:

608 test/interactive013/input

603 test/interactive013/input

609 test/interactive013/run

604 test/interactive013/run

610 test/interactive013/*.idr

605 test/interactive013/*.idr

606+

607+ test/interfaces001/*.idr

608+ test/interfaces001/run

609+ test/interfaces001/expected

610+ test/interfaces001/input

611+ test/interfaces002/*.idr

612+ test/interfaces002/run

613+ test/interfaces002/expected

611

614

612 test/io001/run

615 test/io001/run

613 test/io001/*.idr

616 test/io001/*.idr

src/Idris/Coverage.hs+22−2

@@ -518,6 +518,10 @@ buildSCG' ist topfn pats args = nub $ concatMap scgPat pats where

518 -- that it is total.

519 | (P _ (UN at) _, [_, _]) <- unApply ap,

520 at == txt "assert_total" = []

521+ -- don't go under calls to functions which are asserted total

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

523+ Just opts <- lookupCtxtExact n (idris_flags ist),

524+ AssertTotal `elem` opts = []

521 -- under a guarded call to "Delay LazyCodata", we are 'Delayed', so don't

525 -- under a guarded call to "Delay LazyCodata", we are 'Delayed', so don't

522 -- check under guarded constructors.

526 -- check under guarded constructors.

523 | (P _ (UN del) _, [_,_,arg]) <- unApply ap,

527 | (P _ (UN del) _, [_,_,arg]) <- unApply ap,

@@ -745,8 +749,11 @@ checkMP ist topfn i mp = if i > 0

745 | [TyDecl (TCon _ _) _] <- lookupDef f (tt_ctxt ist)

749 | [TyDecl (TCon _ _) _] <- lookupDef f (tt_ctxt ist)

746 = Total []

750 = Total []

747 tryPath desc path (e@(f, args) : es) arg

751 tryPath desc path (e@(f, args) : es) arg

752+ | [Total a] <- lookupTotal f (tt_ctxt ist) = Total a

748 | e `elem` es && allNothing args = Partial (Mutual [f])

753 | e `elem` es && allNothing args = Partial (Mutual [f])

749 tryPath desc path (e@(f, nextargs) : es) arg

754 tryPath desc path (e@(f, nextargs) : es) arg

755+ | [Total a] <- lookupTotal f (tt_ctxt ist) = Total a

756+ | [Partial _] <- lookupTotal f (tt_ctxt ist) = Partial (Other [f])

750 | Just d <- lookup (e, arg) path

757 | Just d <- lookup (e, arg) path

751 = if desc - d > 0 -- Now lower than when we were last here

758 = if desc - d > 0 -- Now lower than when we were last here

752 then -- trace ("Descent " ++ show (desc - d) ++ " "

759 then -- trace ("Descent " ++ show (desc - d) ++ " "

@@ -781,8 +788,6 @@ checkMP ist topfn i mp = if i > 0

781-- trace (show (desc, argspos, path, es, pathres)) $

788-- trace (show (desc, argspos, path, es, pathres)) $

782 collapse pathres

789 collapse pathres

783

790

784− | [Total a] <- lookupTotal f (tt_ctxt ist) = Total a

785− | [Partial _] <- lookupTotal f (tt_ctxt ist) = Partial (Other [f])

786 | otherwise = Unchecked

791 | otherwise = Unchecked

787

792

788allNothing :: [Maybe a] -> Bool

793allNothing :: [Maybe a] -> Bool

@@ -808,3 +813,18 @@ collapse' def (Unchecked : xs) = collapse' def xs

808collapse' def (d : xs) = collapse' d xs

813collapse' def (d : xs) = collapse' d xs

809-- collapse' Unchecked [] = Total []

814-- collapse' Unchecked [] = Total []

810collapse' def [] = def

815collapse' def [] = def

816+

817+totalityCheckBlock :: Idris ()

818+totalityCheckBlock = do

819+ ist <- getIState

820+ -- Do totality checking after entire mutual block

821+ mapM_ (\n -> do logElab 5 $ "Simplifying " ++ show n

822+ ctxt' <- do ctxt <- getContext

823+ tclift $ simplifyCasedef n (getErasureInfo ist) ctxt

824+ setContext ctxt')

825+ (map snd (idris_totcheck ist))

826+ mapM_ buildSCG (idris_totcheck ist)

827+ mapM_ checkDeclTotality (idris_totcheck ist)

828+ clear_totcheck

829+

830+

src/Idris/Elab/Clause.hs+3−31

@@ -194,17 +194,11 @@ elabClauses info' fc opts n_in cs =

194 logElab 5 $ "After data structure transformations:\n" ++ show pdef'

195

196 ist <- getIState

197− -- let wf = wellFounded ist n sc

198− let tot | pcover || AssertTotal `elem` opts = Unchecked -- finish later

197+ let tot | pcover = Unchecked -- finish later

198+ | AssertTotal `elem` opts = Total []

199 | PEGenerated `elem` opts = Generated

200 | otherwise = Partial NotCovering -- already know it's not total

201

202− -- case lookupCtxt (namespace info) n (idris_flags ist) of

203− -- [fs] -> if TotalFn `elem` fs

204− -- then case tot of

205− -- Total _ -> return ()

206− -- t -> tclift $ tfail (At fc (Msg (show n ++ " is " ++ show t)))

207− -- _ -> return ()

208 case tree of

202 case tree of

209 CaseDef _ _ [] -> return ()

203 CaseDef _ _ [] -> return ()

210 CaseDef _ _ xs -> mapM_ (\x ->

204 CaseDef _ _ xs -> mapM_ (\x ->

@@ -506,29 +500,6 @@ checkPossible info fc tcgen fname lhs_in

506 else return (validCoverageCase ctxt err ||

500 else return (validCoverageCase ctxt err ||

507 recoverableCoverage ctxt err)

501 recoverableCoverage ctxt err)

508

502

509−

510−propagateParams :: IState -> [Name] -> Type -> [Name] -> PTerm -> PTerm

511−propagateParams i ps t bound tm@(PApp _ (PRef fc hls n) args)

512− = PApp fc (PRef fc hls n) (addP t args)

513− where addP (Bind n _ sc) (t : ts)

514− | Placeholder <- getTm t,

515− n `elem` ps,

516− not (n `elem` bound)

517− = t { getTm = PPatvar NoFC n } : addP sc ts

518− addP (Bind n _ sc) (t : ts) = t : addP sc ts

519− addP _ ts = ts

520−propagateParams i ps t bound (PApp fc ap args)

521− = PApp fc (propagateParams i ps t bound ap) args

522−propagateParams i ps t bound (PRef fc hls n)

523− = case lookupCtxt n (idris_implicits i) of

524− [is] -> let ps' = filter (isImplicit is) ps in

525− PApp fc (PRef fc hls n) (map (\x -> pimp x (PRef fc [] x) True) ps')

526− _ -> PRef fc hls n

527− where isImplicit [] n = False

528− isImplicit (PImp _ _ _ x _ : is) n | x == n = True

529− isImplicit (_ : is) n = isImplicit is n

530−propagateParams i ps t bound x = x

531−

532findUnique :: Context -> Env -> Term -> [Name]

503findUnique :: Context -> Env -> Term -> [Name]

533findUnique ctxt env (Bind n b sc)

504findUnique ctxt env (Bind n b sc)

534 = let rawTy = forgetEnv (map fst env) (binderTy b)

505 = let rawTy = forgetEnv (map fst env) (binderTy b)

@@ -583,6 +554,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

583

554

584 let lhs = mkLHSapp $ stripLinear i $ stripUnmatchable i $

555 let lhs = mkLHSapp $ stripLinear i $ stripUnmatchable i $

585 propagateParams i params norm_ty (allNamesIn lhs_in) (addImplPat i lhs_in)

556 propagateParams i params norm_ty (allNamesIn lhs_in) (addImplPat i lhs_in)

557+

586-- let lhs = mkLHSapp $

558-- let lhs = mkLHSapp $

587-- propagateParams i params fn_ty (addImplPat i lhs_in)

559-- propagateParams i params fn_ty (addImplPat i lhs_in)

588 logElab 10 (show (params, fn_ty) ++ " " ++ showTmImpls (addImplPat i lhs_in))

560 logElab 10 (show (params, fn_ty) ++ " " ++ showTmImpls (addImplPat i lhs_in))

src/Idris/Elab/Instance.hs+98−20

@@ -101,6 +101,7 @@ elabInstance info syn doc argDocs what fc cs acc opts n nfc ps t expn ds = do

101 ist <- getIState

102 let pnames = nub $ map pname (concat (nub wparams)) ++

103 concatMap (namesIn [] ist) ps

104+

104 let superclassInstances = map (substInstance ips pnames) (class_default_superclasses ci)

105 let superclassInstances = map (substInstance ips pnames) (class_default_superclasses ci)

105 undefinedSuperclassInstances <- filterM (fmap not . isOverlapping ist) superclassInstances

106 undefinedSuperclassInstances <- filterM (fmap not . isOverlapping ist) superclassInstances

106 mapM_ (rec_elabDecl info EAll info) undefinedSuperclassInstances

107 mapM_ (rec_elabDecl info EAll info) undefinedSuperclassInstances

@@ -128,29 +129,48 @@ elabInstance info syn doc argDocs what fc cs acc opts n nfc ps t expn ds = do

128 logElab 3 $ "Instance is " ++ show ps ++ " implicits " ++

129 logElab 3 $ "Instance is " ++ show ps ++ " implicits " ++

129 show (concat (nub wparams))

130 show (concat (nub wparams))

130

131

131− -- Bring variables in instance head into scope

132+ -- Bring variables in instance head into scope when building the

133+ -- dictionary

132− let headVars = nub $ mapMaybe (\p -> case p of

134+ let headVars = nub $ concatMap getHeadVars ps

133− PRef _ _ n ->

135+

134− case lookupTy n (tt_ctxt ist) of

135− [] -> Just n

136− _ -> Nothing

137− _ -> Nothing) ps

138−-- let lhs = PRef fc iname

139− let lhs = PApp fc (PRef fc [] iname)

140− (map (\n -> pimp n (PRef fc [] n) True) headVars)

136+ let lhsImps = map (\n -> pimp n (PRef fc [] n) True) headVars

137+

138+ let lhs = PApp fc (PRef fc [] iname) lhsImps

141 let rhs = PApp fc (PRef fc [] (instanceCtorName ci))

139 let rhs = PApp fc (PRef fc [] (instanceCtorName ci))

142− (map (pexp . mkMethApp) mtys)

140+ (map (pexp . (mkMethApp lhsImps)) mtys)

143

141

144− logElab 5 $ "Instance LHS " ++ show totopts ++ "\n" ++ show lhs ++ " " ++ show headVars

142+ logElab 5 $ "Instance LHS " ++ show totopts ++ "\n" ++ showTmImpls lhs ++ " " ++ show headVars

145 logElab 5 $ "Instance RHS " ++ show rhs

143 logElab 5 $ "Instance RHS " ++ show rhs

146

144

147− let idecls = [PClauses fc totopts iname

148− [PClause fc iname lhs [] rhs wb]]

149− logElab 1 (show idecls)

150 push_estack iname True

145 push_estack iname True

146+ logElab 3 ("Method types: " ++ show wbTys)

147+ logElab 3 ("Method bodies: " ++ show wbVals)

148+

149+ let idecls = [PClauses fc totopts iname

150+ [PClause fc iname lhs [] rhs []]]

151+

152+ mapM_ (rec_elabDecl info EAll info) (map (impBind headVars) wbTys)

151 mapM_ (rec_elabDecl info EAll info) idecls

153 mapM_ (rec_elabDecl info EAll info) idecls

154+

155+ ctxt <- getContext

156+ let ifn_ty = case lookupTyExact iname ctxt of

157+ Just t -> t

158+ Nothing -> error "Can't happen (interface constructor)"

159+ let ifn_is = case lookupCtxtExact iname (idris_implicits ist) of

160+ Just t -> t

161+ Nothing -> []

162+ let prop_params = getParamsInType ist [] ifn_is ifn_ty

163+

164+ logElab 3 $ "Propagating parameters to methods: "

165+ ++ show (iname, prop_params)

166+

167+ let wbVals' = map (addParams prop_params) wbVals

168+

169+ mapM_ (rec_elabDecl info EAll info) wbVals'

170+

152 pop_estack

171 pop_estack

153− ist <- getIState

172+-- totalityCheckBlock

173+

154 checkInjectiveArgs fc n (class_determiners ci) (lookupTyExact iname (tt_ctxt ist))

174 checkInjectiveArgs fc n (class_determiners ci) (lookupTyExact iname (tt_ctxt ist))

155 addIBC (IBCInstance intInst (isNothing expn) n iname)

175 addIBC (IBCInstance intInst (isNothing expn) n iname)

156

176

@@ -226,8 +246,9 @@ elabInstance info syn doc argDocs what fc cs acc opts n nfc ps t expn ds = do

226 map snd (filter (\(i, _) -> i `elem` dets) a')

246 map snd (filter (\(i, _) -> i `elem` dets) a')

227 keepDets dets t = t

247 keepDets dets t = t

228

248

229− mkMethApp (n, _, _, ty)

249+ mkMethApp ps (n, _, _, ty)

230− = lamBind 0 ty (papp fc (PRef fc [] n) (methArgs 0 ty))

250+ = lamBind 0 ty (papp fc (PRef fc [] n)

251+ (ps ++ methArgs 0 ty))

231 lamBind i (PPi (Constraint _ _) _ _ _ sc) sc'

252 lamBind i (PPi (Constraint _ _) _ _ _ sc) sc'

232 = PLam fc (sMN i "meth") NoFC Placeholder (lamBind (i+1) sc sc')

253 = PLam fc (sMN i "meth") NoFC Placeholder (lamBind (i+1) sc sc')

233 lamBind i (PPi _ n _ ty sc) sc'

254 lamBind i (PPi _ n _ ty sc) sc'

@@ -254,8 +275,10 @@ elabInstance info syn doc argDocs what fc cs acc opts n nfc ps t expn ds = do

254 _ -> return ps'

275 _ -> return ps'

255 getWParams (_ : ps) = getWParams ps

276 getWParams (_ : ps) = getWParams ps

256

277

257− decorate ns iname (UN n) = NS (SN (MethodN (UN n))) ns

278+ decorate ns iname (UN nm)

279+ = NS (SN (WhereN 0 iname (SN (MethodN (UN nm))))) ns

258− decorate ns iname (NS (UN n) s) = NS (SN (MethodN (UN n))) ns

280+ decorate ns iname (NS (UN nm) s)

281+ = NS (SN (WhereN 0 iname (SN (MethodN (UN nm))))) ns

259

282

260 mkTyDecl (n, op, t, _)

283 mkTyDecl (n, op, t, _)

261 = PTy emptyDocstring [] syn fc op n NoFC

284 = PTy emptyDocstring [] syn fc op n NoFC

@@ -314,6 +337,61 @@ elabInstance info syn doc argDocs what fc cs acc opts n nfc ps t expn ds = do

314 clauseFor m iname ns (PClauses _ _ m' _)

337 clauseFor m iname ns (PClauses _ _ m' _)

315 = decorate ns iname m == decorate ns iname m'

338 = decorate ns iname m == decorate ns iname m'

316 clauseFor m iname ns _ = False

339 clauseFor m iname ns _ = False

340+

341+getHeadVars :: PTerm -> [Name]

342+getHeadVars (PRef _ _ n) | implicitable n = [n]

343+getHeadVars (PApp _ _ args) = concatMap getHeadVars (map getTm args)

344+getHeadVars (PPair _ _ _ l r) = getHeadVars l ++ getHeadVars r

345+getHeadVars (PDPair _ _ _ l t r) = getHeadVars l ++ getHeadVars t ++ getHeadVars t

346+getHeadVars _ = []

347+

348+-- Implicitly bind variables from the instance head in method types

349+impBind :: [Name] -> PDecl -> PDecl

350+impBind vs (PTy d ds syn fc opts n fc' t)

351+ = PTy d ds syn fc opts n fc' (doImpBind (vs \\ boundIn t) t)

352+ where

353+ doImpBind [] ty = ty

354+ doImpBind (n : ns) ty = PPi impl n NoFC Placeholder (doImpBind ns ty)

355+

356+ boundIn (PPi _ n _ _ sc) = n : boundIn sc

357+ boundIn _ = []

358+

359+

360+-- Propagate class parameters to method bodies, if they're not already

361+-- there

362+addParams :: [Name] -> PDecl -> PDecl

363+addParams ps (PClauses fc opts n cs) = PClauses fc opts n (map addCParams cs)

364+ where

365+ addCParams (PClause fc n lhs ws rhs wb)

366+ = PClause fc n (addTmParams (dropPs (allNamesIn lhs) ps) lhs) ws rhs wb

367+ addCParams (PWith fc n lhs ws sc pn ds)

368+ = PWith fc n (addTmParams (dropPs (allNamesIn lhs) ps) lhs) ws sc pn

369+ (map (addParams ps) ds)

370+ addCParams c = c

371+

372+ addTmParams ps (PRef fc hls n) = PApp fc (PRef fc hls n) (map toImp ps)

373+ addTmParams ps (PApp fc ap@(PRef fc' hls n) args)

374+ = PApp fc ap (mergePs (map toImp ps) args)

375+ addTmParams ps tm = tm

376+

377+ toImp n = pimp n (PRef fc [] n) True

378+

379+ mergePs [] args = args

380+ mergePs (p : ps) args

381+ | isImplicit p,

382+ pname p `notElem` map pname args

383+ = p : mergePs ps args

384+ where

385+ isImplicit (PExp{}) = False

386+ isImplicit _ = True

387+ mergePs (p : ps) args

388+ = mergePs ps args

389+

390+ -- Don't propagate a parameter if the name is rebound explicitly

391+ dropPs :: [Name] -> [Name] -> [Name]

392+ dropPs ns = filter (\x -> x `notElem` ns)

393+

394+addParams ps d = d

317

395

318checkInjectiveArgs :: FC -> Name -> [Int] -> Maybe Type -> Idris ()

396checkInjectiveArgs :: FC -> Name -> [Int] -> Maybe Type -> Idris ()

319checkInjectiveArgs fc n ds Nothing = return ()

397checkInjectiveArgs fc n ds Nothing = return ()

src/Idris/Elab/Utils.hs+24

@@ -426,3 +426,27 @@ displayWarnings est

426 displayImpWarning (fc, n) =

427 iputStrLn $ show fc ++ ":WARNING: " ++ show (nsroot n) ++ " is bound as an implicit\n"

428 ++ "\tDid you mean to refer to " ++ show n ++ "?"

429+

430+propagateParams :: IState -> [Name] -> Type -> [Name] -> PTerm -> PTerm

431+propagateParams i ps t bound tm@(PApp _ (PRef fc hls n) args)

432+ = PApp fc (PRef fc hls n) (addP t args)

433+ where addP (Bind n _ sc) (t : ts)

434+ | Placeholder <- getTm t,

435+ n `elem` ps,

436+ not (n `elem` bound)

437+ = t { getTm = PPatvar NoFC n } : addP sc ts

438+ addP (Bind n _ sc) (t : ts) = t : addP sc ts

439+ addP _ ts = ts

440+propagateParams i ps t bound (PApp fc ap args)

441+ = PApp fc (propagateParams i ps t bound ap) args

442+propagateParams i ps t bound (PRef fc hls n)

443+ = case lookupCtxt n (idris_implicits i) of

444+ [is] -> let ps' = filter (isImplicit is) ps in

445+ PApp fc (PRef fc hls n) (map (\x -> pimp x (PRef fc [] x) True) ps')

446+ _ -> PRef fc hls n

447+ where isImplicit [] n = False

448+ isImplicit (PImp _ _ _ x _ : is) n | x == n = True

449+ isImplicit (_ : is) n = isImplicit is n

450+propagateParams i ps t bound x = x

451+

452+

src/Idris/Parser.hs+7−2

@@ -1768,10 +1768,15 @@ loadSource lidr f toline

1768

1769 -- Redo totality check for deferred names

1770 let deftots = idris_defertotcheck i

1771− logLvl 1 $ "Totality checking " ++ show deftots

1771+ logLvl 2 $ "Totality checking " ++ show deftots

1772 mapM_ (\x -> do tot <- getTotality x

1773 case tot of

1774+ Total _ ->

1775+ do let opts = case lookupCtxtExact x (idris_flags i) of

1776+ Just os -> os

1777+ Nothing -> []

1778+ when (AssertTotal `notElem` opts) $

1774− Total _ -> setTotality x Unchecked

1779+ setTotality x Unchecked

1775 _ -> return ()) (map snd deftots)

1780 _ -> return ()) (map snd deftots)

1776 mapM_ buildSCG deftots

1781 mapM_ buildSCG deftots

1777 mapM_ checkDeclTotality deftots

1782 mapM_ checkDeclTotality deftots

test/classes001/ClassName.idr → test/interfaces001/ClassName.idrrenamed

The content is the same.

test/classes001/expected → test/interfaces001/expectedrenamed

The content is the same.

test/classes001/input → test/interfaces001/inputrenamed

The content is the same.

test/classes001/run → test/interfaces001/runrenamed+1−1

@@ -1,3 +1,3 @@

1#!/usr/bin/env bash

2${IDRIS:-idris} $@ --quiet --nocolour --consolewidth 70 ClassName.idr < input

3−rm -f bounded001 *.ibc

3+rm -f *.ibc

test/interfaces002/expectednew file+5

@@ -0,0 +1,5 @@

1+WARNING: There are incomplete holes:

2+ [Main.prf]

4+Evaluation of any of these will crash at run time.

5+41

test/interfaces002/interfaces002.idrnew file+39

@@ -0,0 +1,39 @@

1+import Data.Vect

3+interface ArrayM where

4+ Array : (n : Nat) -> (a : Type) -> Type

6+ create : (n : Nat) -> a -> Array n a

8+ lkp : (i : Nat) -> (prf : LTE (S i) n) -> Array n a -> a

9+ upd : a -> (i : Nat) -> (prf : LT i n) -> Array n a -> Array n a

10+

11+using (ArrayM)

12+ sumArrayHelp : Num a => (k : Nat) -> LT k (S n) -> Array n a -> a

13+ sumArrayHelp Z x y = 0

14+ sumArrayHelp (S k) (LTESucc prf) y

15+ = lkp k prf y + sumArrayHelp k (lteSuccRight prf) y

16+

17+ sumArray : Array n Int -> Int

18+ sumArray {n} x = sumArrayHelp n lteRefl x

19+

20+implementation ArrayM where

21+ Array = Vect

22+

23+ create n x = replicate n x

24+

25+ lkp Z (LTESucc x) (y :: xs) = y

26+ lkp (S k) (LTESucc x) (y :: xs) = lkp k x xs

27+

28+ upd val Z (LTESucc p) (_ :: xs) = val :: xs

29+ upd val (S k) (LTESucc p) (x :: xs) = x :: upd val k p xs

30+

31+-- using (ArrayM as vectArray)

32+

33+testSum : Array n Int -> Int

34+testSum = sumArray

35+

36+main : IO ()

37+main = printLn (testSum (upd 11 2 ?prf (create 4 10)))

38+

39+

test/interfaces002/runnew file+4

@@ -0,0 +1,4 @@

1+#!/usr/bin/env bash

2+${IDRIS:-idris} $@ --nocolour --consolewidth 70 interfaces002.idr -o interfaces002

3+./interfaces002

4+rm -f interfaces002 *.ibc