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

git.iko.soy/Idris-dev

Change elaboration of interfaces

Instead of a function to build the dictionary with a where block, build the method types, then the function, then the method bodies. This way, the method bodies can use the reduction behaviour of other methods, which they couldn't before as the methods were defined before the dictionary.

commit57136cc0f131d0dacd52b0eebd81469a13785757 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSat 7 May 2016, 15:32 (10 years ago) parent9540f1a

13 files changed+211−61

compare with master

unifiedsplit

idris.cabal+8−5 src/Idris/Coverage.hs+22−2 src/Idris/Elab/Clause.hs+3−31 src/Idris/Elab/Instance.hs+98−20 src/Idris/Elab/Utils.hs+24 src/Idris/Parser.hs+7−2 test/classes001/ClassName.idr → test/interfaces001/ClassName.idr test/classes001/expected → test/interfaces001/expected test/classes001/input → test/interfaces001/input test/classes001/run → test/interfaces001/run+1−1 test/interfaces002/expected+5 test/interfaces002/interfaces002.idr+39 test/interfaces002/run+4

idris.cabal+8−5

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

399399 test/bignum002/*.idr

400400 test/bignum002/expected

401401

402− test/classes001/*.idr

403− test/classes001/run

404− test/classes001/expected

405− test/classes001/input

406−

407402 test/corecords001/*.idr

408403 test/corecords001/run

409404 test/corecords001/expected

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

608603 test/interactive013/input

609604 test/interactive013/run

610605 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

611614

612615 test/io001/run

613616 test/io001/*.idr

src/Idris/Coverage.hs+22−2

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

518518 -- that it is total.

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

520520 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 = []

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

522526 -- check under guarded constructors.

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

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

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

746750 = Total []

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

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

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

749754 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])

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

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

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

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

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

782789 collapse pathres

783790

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

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

786791 | otherwise = Unchecked

787792

788793allNothing :: [Maybe a] -> Bool

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

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

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

810815collapse' 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 =

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

195195

196196 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 []

199199 | PEGenerated `elem` opts = Generated

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

201201

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

208202 case tree of

209203 CaseDef _ _ [] -> return ()

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

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

506500 else return (validCoverageCase ctxt err ||

507501 recoverableCoverage ctxt err)

508502

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−

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

533504findUnique ctxt env (Bind n b sc)

534505 = 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

583554

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

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

557+

586558-- let lhs = mkLHSapp $

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

588560 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

101101 ist <- getIState

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

103103 concatMap (namesIn [] ist) ps

104+

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

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

106107 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

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

129130 show (concat (nub wparams))

130131

131− -- Bring variables in instance head into scope

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

133− PRef _ _ n ->

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)

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

133+ -- dictionary

134+ let headVars = nub $ concatMap getHeadVars ps

135+

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

137+

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

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

142− (map (pexp . mkMethApp) mtys)

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

143141

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

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

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

146144

147− let idecls = [PClauses fc totopts iname

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

149− logElab 1 (show idecls)

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

151153 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+

152171 pop_estack

153− ist <- getIState

172+-- totalityCheckBlock

173+

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

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

156176

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

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

227247 keepDets dets t = t

228248

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

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

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

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

251+ (ps ++ methArgs 0 ty))

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

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

233254 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

254275 _ -> return ps'

255276 getWParams (_ : ps) = getWParams ps

256277

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

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

278+ decorate ns iname (UN nm)

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

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

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

259282

260283 mkTyDecl (n, op, t, _)

261284 = 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

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

315338 = decorate ns iname m == decorate ns iname m'

316339 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

317395

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

319397checkInjectiveArgs fc n ds Nothing = return ()

src/Idris/Elab/Utils.hs+24

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

426426 displayImpWarning (fc, n) =

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

428428 ++ "\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

17681768

17691769 -- Redo totality check for deferred names

17701770 let deftots = idris_defertotcheck i

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

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

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

17731773 case tot of

1774− Total _ -> setTotality x Unchecked

1774+ Total _ ->

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

1776+ Just os -> os

1777+ Nothing -> []

1778+ when (AssertTotal `notElem` opts) $

1779+ setTotality x Unchecked

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

17761781 mapM_ buildSCG deftots

17771782 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 @@

11#!/usr/bin/env bash

22${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