1b1a055 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Improved where; implicit arguments now expanded during elaboration

1b1a055Edwin Brady15 years ago

lib/io.idr+4−4

compare with master

unifiedsplit

@@ -19,10 +19,10 @@ interpFTy FPtr = Ptr;

19interpFTy FUnit = ();

21ForeignTy : (xs:List FTy) -> (t:FTy) -> Set;

22−ForeignTy xs t = mkForeign (rev xs) (IO (interpFTy t)) where {

22+ForeignTy xs t = mkForeign' (rev xs) (IO (interpFTy t)) where {

23− mkForeign : List FTy -> Set -> Set;

23+ mkForeign' : List FTy -> Set -> Set;

24− mkForeign Nil ty = ty;

24+ mkForeign' Nil ty = ty;

25− mkForeign (Cons s ss) ty = mkForeign ss (interpFTy s -> ty);

25+ mkForeign' (Cons s ss) ty = mkForeign' ss (interpFTy s -> ty);

26}

28data FEnv : List FTy -> Set where

lib/list.idr+11−6

@@ -3,12 +3,11 @@ import builtins;

3data List a = Nil | Cons a (List a);

5rev : List a -> List a;

6−rev xs = revAcc Nil xs

6+rev xs = revAcc Nil xs where {

7− where {

8− revAcc : List a -> List a -> List a;

7+ revAcc : List a -> List a -> List a;

9− revAcc acc Nil = acc;

8+ revAcc acc Nil = acc;

10− revAcc acc (Cons x xs) = revAcc (Cons x acc) xs;

9+ revAcc acc (Cons x xs) = revAcc (Cons x acc) xs;

11− }

10+}

13length : List a -> Int;

12length : List a -> Int;

14length Nil = 0;

13length Nil = 0;

@@ -24,3 +23,9 @@ drop 0 xs = xs;

24drop n Nil = Nil;

23drop n Nil = Nil;

25drop n (Cons x xs) = drop (n-1) xs;

24drop n (Cons x xs) = drop (n-1) xs;

26+filter : (y -> Bool) -> List y -> List y;

27+filter pred Nil = Nil;

28+filter pred (Cons x xs) with (pred x, filter pred xs) {

29+ filter pred (Cons x xs) | (True, fxs) = Cons x fxs;

30+ filter pred (Cons x xs) | (False, fxs) = fxs;

31+}

lib/vect.idr+7

@@ -18,3 +18,10 @@ vapp : Vect a n -> Vect a m -> Vect a (plus n m);

18vapp VNil ys = ys;

19vapp (x :: xs) ys = x :: vapp xs ys;

21+vfilter : (a -> Bool) -> Vect a n -> (p ** Vect a p);

22+vfilter p VNil = ( _ ** VNil );

23+vfilter p (x :: xs) with (vfilter p xs) {

24+ vfilter p (x :: xs) | ( _ ** xs' )

25+ = if (p x) then ( _ ** x :: xs' ) else ( _ ** xs' );

26+}

27+

src/Core/ProofState.hs+1

@@ -275,6 +275,7 @@ patvar :: Name -> RunTactic

275patvar n ctxt env (Bind x (Hole t) sc) =

276 do action (\ps -> ps { holes = holes ps \\ [x] })

277 return $ Bind n (PVar t) (instantiate (P Bound n t) (pToV x sc))

278+patvar n ctxt env tm = fail $ "Can't add pattern var at " ++ show tm

278

279

279letbind :: Name -> Raw -> Raw -> RunTactic

280letbind :: Name -> Raw -> Raw -> RunTactic

280letbind n ty val ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =

281letbind n ty val ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =

src/Core/Typecheck.hs+1−1

@@ -43,7 +43,7 @@ check ctxt env (RApp f a)

43 case fty' of

44 Bind x (Pi s) t ->

45 do converts ctxt env s aty

46− let apty = {- normalise ctxt env -} (Bind x (Let aty av) t)

46+ let apty = normalise ctxt env (Bind x (Let aty av) t)

47 return (App fv av, apty)

48 t -> fail "Can't apply a non-function type"

49 -- This rather unpleasant hack is needed because during incomplete

src/Idris/AbsSyntax.hs+147−41

@@ -166,15 +166,15 @@ impl = Imp False Dynamic

166expl = Exp False Dynamic

167

168data PDecl' t = PFix FC Fixity [String] -- fixity declaration

169− | PTy FC Name t -- type declaration

169+ | PTy SyntaxInfo FC Name t -- type declaration

170 | PClauses FC Name [PClause' t] -- pattern clause

171− | PData FC (PData' t) -- data declaration

171+ | PData SyntaxInfo FC (PData' t) -- data declaration

172− | PParams FC [(Name, PTerm)] [PDecl' t] -- params block

172+ | PParams FC [(Name, t)] [PDecl' t] -- params block

173 | PSyntax FC Syntax

174 deriving Functor

175

176−data PClause' t = PClause Name t [t] t [PDecl]

176+data PClause' t = PClause Name t [t] t [PDecl' t]

177− | PWith Name t [t] t [PDecl]

177+ | PWith Name t [t] t [PDecl' t]

178 deriving Functor

179

180data PData' t = PDatadecl { d_name :: Name,

@@ -193,15 +193,36 @@ type PClause = PClause' PTerm

193

194declared :: PDecl -> [Name]

195declared (PFix _ _ _) = []

196−declared (PTy _ n t) = [n]

196+declared (PTy _ _ n t) = [n]

197declared (PClauses _ n _) = [] -- not a declaration

198−declared (PData _ (PDatadecl n _ ts)) = n : map fstt ts

198+declared (PData _ _ (PDatadecl n _ ts)) = n : map fstt ts

199 where fstt (a, _, _) = a

200declared (PParams _ _ ds) = concatMap declared ds

201-- declared (PImport _) = []

202

203+updateN :: [(Name, Name)] -> Name -> Name

204+updateN ns n | Just n' <- lookup n ns = n'

205+updateN _ n = n

206+

207+updateNs :: [(Name, Name)] -> PTerm -> PTerm

208+updateNs [] t = t

209+updateNs ns t = mapPT updateRef t

210+ where updateRef (PRef fc f) = PRef fc (updateN ns f)

211+ updateRef t = t

212+

213+-- updateDNs :: [(Name, Name)] -> PDecl -> PDecl

214+-- updateDNs [] t = t

215+-- updateDNs ns (PTy s f n t) | Just n' <- lookup n ns = PTy s f n' t

216+-- updateDNs ns (PClauses f n c) | Just n' <- lookup n ns = PClauses f n' (map updateCNs c)

217+-- where updateCNs ns (PClause n l ts r ds)

218+-- = PClause (updateN ns n) (fmap (updateNs ns) l)

219+-- (map (fmap (updateNs ns)) ts)

220+-- (fmap (updateNs ns) r)

221+-- (map (updateDNs ns) ds)

222+-- updateDNs ns c = c

223+

203-- High level language terms

224-- High level language terms

204−--

225+

205data PTerm = PQuote Raw

226data PTerm = PQuote Raw

206 | PRef FC Name

227 | PRef FC Name

207 | PLam Name PTerm PTerm

228 | PLam Name PTerm PTerm

@@ -225,19 +246,38 @@ data PTerm = PQuote Raw

225 | PElabError String -- error to report on elaboration

246 | PElabError String -- error to report on elaboration

226 deriving Eq

247 deriving Eq

227

248

249+mapPT :: (PTerm -> PTerm) -> PTerm -> PTerm

250+mapPT f t = f (mpt t) where

251+ mpt (PLam n t s) = PLam n (mapPT f t) (mapPT f s)

252+ mpt (PPi p n t s) = PPi p n (mapPT f t) (mapPT f s)

253+ mpt (PLet n ty v s) = PLet n (mapPT f ty) (mapPT f v) (mapPT f s)

254+ mpt (PApp fc t as) = PApp fc (mapPT f t) (map (fmap (mapPT f)) as)

255+ mpt (PEq fc l r) = PEq fc (mapPT f l) (mapPT f r)

256+ mpt (PPair fc l r) = PPair fc (mapPT f l) (mapPT f r)

257+ mpt (PDPair fc l r) = PDPair fc (mapPT f l) (mapPT f r)

258+ mpt (PHidden t) = PHidden (mapPT f t)

259+ mpt (PDoBlock ds) = PDoBlock (map (fmap (mapPT f)) ds)

260+ mpt (PProof ts) = PProof (map (fmap (mapPT f)) ts)

261+ mpt x = x

262+

263+

228−data PTactic = Intro [Name] | Focus Name

264+data PTactic' t = Intro [Name] | Focus Name

229− | Refine Name [Bool] | Rewrite PTerm

265+ | Refine Name [Bool] | Rewrite t

230− | Exact PTerm | Compute | Trivial

266+ | Exact t | Compute | Trivial

231− | Solve

267+ | Solve

232− | Attack

268+ | Attack

233− | ProofState | ProofTerm | Undo

269+ | ProofState | ProofTerm | Undo

234− | Qed

270+ | Qed

235− deriving (Show, Eq)

271+ deriving (Show, Eq, Functor)

236

272

273+type PTactic = PTactic' PTerm

274+

237−data PDo = DoExp FC PTerm

275+data PDo' t = DoExp FC t

238− | DoBind FC Name PTerm

276+ | DoBind FC Name t

239− | DoLet FC Name PTerm

277+ | DoLet FC Name t

240− deriving Eq

278+ deriving (Eq, Functor)

279+

280+type PDo = PDo' PTerm

241

281

242data PArg' t = PImp { lazyarg :: Bool, pname :: Name, getTm :: t }

282data PArg' t = PImp { lazyarg :: Bool, pname :: Name, getTm :: t }

243 | PExp { lazyarg :: Bool, getTm :: t }

283 | PExp { lazyarg :: Bool, getTm :: t }

@@ -267,10 +307,11 @@ initDSL = DSL (UN ["io_bind"]) (UN ["io_return"])

267data SyntaxInfo = Syn { using :: [(Name, PTerm)],

307data SyntaxInfo = Syn { using :: [(Name, PTerm)],

268 syn_params :: [(Name, PTerm)],

308 syn_params :: [(Name, PTerm)],

269 no_imp :: [Name],

309 no_imp :: [Name],

310+ decoration :: Name -> Name,

270 dsl_info :: DSL }

311 dsl_info :: DSL }

271 deriving Show

312 deriving Show

272

313

273−defaultSyntax = Syn [] [] [] initDSL

314+defaultSyntax = Syn [] [] [] id initDSL

274

315

275--- Pretty printing declarations and terms

316--- Pretty printing declarations and terms

276

317

@@ -279,9 +320,9 @@ instance Show PTerm where

279

320

280instance Show PDecl where

321instance Show PDecl where

281 show (PFix _ f ops) = show f ++ " " ++ showSep ", " ops

322 show (PFix _ f ops) = show f ++ " " ++ showSep ", " ops

282− show (PTy _ n ty) = show n ++ " : " ++ show ty

323+ show (PTy _ _ n ty) = show n ++ " : " ++ show ty

283 show (PClauses _ n c) = showSep "\n" (map show c)

324 show (PClauses _ n c) = showSep "\n" (map show c)

284− show (PData _ d) = show d

325+ show (PData _ _ d) = show d

285

326

286instance Show PClause where

327instance Show PClause where

287 show c = showCImp True c

328 show c = showCImp True c

@@ -433,6 +474,10 @@ getInferType (App (App _ ty) _) = ty

433

474

434-- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign

475-- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign

435

476

477+primNames = [unitTy, unitCon,

478+ falseTy, pairTy, pairCon,

479+ eqTy, eqCon, inferTy, inferCon]

480+

436unitTy = MN 0 "__Unit"

481unitTy = MN 0 "__Unit"

437unitCon = MN 0 "__II"

482unitCon = MN 0 "__II"

438unitDecl = PDatadecl unitTy PSet

483unitDecl = PDatadecl unitTy PSet

@@ -473,6 +518,53 @@ piBind :: [(Name, PTerm)] -> PTerm -> PTerm

473piBind [] t = t

518piBind [] t = t

474piBind ((n, ty):ns) t = PPi expl n ty (piBind ns t)

519piBind ((n, ty):ns) t = PPi expl n ty (piBind ns t)

475

520

521+-- Dealing with parameters

522+

523+expandParams :: (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PTerm -> PTerm

524+expandParams dec ps ns tm = en tm

525+ where

526+ en (PLam n t s) = PLam n (en t) (en s)

527+ en (PPi p n t s) = PPi p n (en t) (en s)

528+ en (PLet n ty v s) = PLet n (en ty) (en v) (en s)

529+ en (PEq f l r) = PEq f (en l) (en r)

530+ en (PPair f l r) = PPair f (en l) (en r)

531+ en (PDPair f l r) = PDPair f (en l) (en r)

532+ en (PHidden t) = PHidden (en t)

533+ en (PDoBlock ds) = PDoBlock (map (fmap en) ds)

534+ en (PProof ts) = PProof (map (fmap en) ts)

535+

536+ en (PApp fc (PRef fc' n) as)

537+ | n `elem` ns = PApp fc (PRef fc' (dec n))

538+ (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))

539+ en (PRef fc n)

540+ | n `elem` ns = PApp fc (PRef fc (dec n))

541+ (map (pexp . (PRef fc)) (map fst ps))

542+ en (PApp fc f as) = PApp fc (en f) (map (fmap en) as)

543+ en t = t

544+

545+expandParamsD :: (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PDecl -> PDecl

546+expandParamsD dec ps ns (PTy syn fc n ty)

547+ = if n `elem` ns

548+ then PTy syn fc (dec n) (piBind ps (expandParams dec ps ns ty))

549+ else PTy syn fc n (expandParams dec ps ns ty)

550+expandParamsD dec ps ns (PClauses fc n cs)

551+ = let n' = if n `elem` ns then dec n else n in

552+ PClauses fc n' (map expandParamsC cs)

553+ where

554+ expandParamsC (PClause n lhs ws rhs ds)

555+ = let n' = if n `elem` ns then dec n else n in

556+ PClause n' (expandParams dec ps ns lhs)

557+ (map (expandParams dec ps ns) ws)

558+ (expandParams dec ps ns rhs)

559+ (map (expandParamsD dec ps ns) ds)

560+ expandParamsC (PWith n lhs ws wval ds)

561+ = let n' = if n `elem` ns then dec n else n in

562+ PWith n' (expandParams dec ps ns lhs)

563+ (map (expandParams dec ps ns) ws)

564+ (expandParams dec ps ns wval)

565+ (map (expandParamsD dec ps ns) ds)

566+expandParamsD dec ps ns d = d

567+

476-- Dealing with implicit arguments

568-- Dealing with implicit arguments

477

569

478-- Add implicit Pi bindings for any names in the term which appear in an

570-- Add implicit Pi bindings for any names in the term which appear in an

@@ -480,6 +572,17 @@ piBind ((n, ty):ns) t = PPi expl n ty (piBind ns t)

480

572

481-- This has become a right mess already. Better redo it some time...

573-- This has become a right mess already. Better redo it some time...

482

574

575+implicit :: SyntaxInfo -> Name -> PTerm -> Idris PTerm

576+implicit syn n ptm

577+ = do i <- get

578+ let (tm', impdata) = implicitise syn i ptm

579+ let (tm'', spos) = findStatics i tm'

580+ put (i { idris_implicits = addDef n impdata (idris_implicits i) })

581+ logLvl 5 ("Implicit " ++ show n ++ " " ++ show impdata)

582+ i <- get

583+ put (i { idris_statics = addDef n spos (idris_statics i) })

584+ return tm''

585+

483implicitise :: SyntaxInfo -> IState -> PTerm -> (PTerm, [PArg])

586implicitise :: SyntaxInfo -> IState -> PTerm -> (PTerm, [PArg])

484implicitise syn ist tm

587implicitise syn ist tm

485 = let uvars = using syn

588 = let uvars = using syn

@@ -545,7 +648,7 @@ implicitise syn ist tm

545addImpl :: IState -> PTerm -> PTerm

648addImpl :: IState -> PTerm -> PTerm

546addImpl ist ptm = ai [] ptm

649addImpl ist ptm = ai [] ptm

547 where

650 where

548− ai env (PRef fc f) = aiFn fc env (PRef fc f) []

651+ ai env (PRef fc f) = aiFn ist fc f []

549 ai env (PEq fc l r) = let l' = ai env l

652 ai env (PEq fc l r) = let l' = ai env l

550 r' = ai env r in

653 r' = ai env r in

551 PEq fc l' r'

654 PEq fc l' r'

@@ -557,10 +660,10 @@ addImpl ist ptm = ai [] ptm

557 PDPair fc l' r'

660 PDPair fc l' r'

558 ai env (PApp fc (PRef _ f) as)

661 ai env (PApp fc (PRef _ f) as)

559 = let as' = map (fmap (ai env)) as in

662 = let as' = map (fmap (ai env)) as in

560− aiFn fc env (PRef fc f) as'

663+ aiFn ist fc f as'

561 ai env (PApp fc f as) = let f' = ai env f

664 ai env (PApp fc f as) = let f' = ai env f

562 as' = map (fmap (ai env)) as in

665 as' = map (fmap (ai env)) as in

563− aiFn fc env f' as'

666+ mkPApp fc 1 f' as'

564 ai env (PLam n ty sc) = let ty' = ai env ty

667 ai env (PLam n ty sc) = let ty' = ai env ty

565 sc' = ai (n:env) sc in

668 sc' = ai (n:env) sc in

566 PLam n ty' sc'

669 PLam n ty' sc'

@@ -573,21 +676,17 @@ addImpl ist ptm = ai [] ptm

573 sc' = ai (n:env) sc in

676 sc' = ai (n:env) sc in

574 PPi p n ty' sc'

677 PPi p n ty' sc'

575 ai env (PHidden tm) = PHidden (ai env tm)

678 ai env (PHidden tm) = PHidden (ai env tm)

679+ ai env (PProof ts) = PProof (map (fmap (ai env)) ts)

576 ai env tm = tm

680 ai env tm = tm

577

681

578− aiFn _ env (PRef fc f) as | not (f `elem` env)

682+aiFn :: IState -> FC -> Name -> [PArg] -> PTerm

683+aiFn ist fc f as

684+ | f `elem` primNames = PApp fc (PRef fc f) as

685+aiFn ist fc f as

579 = case lookupCtxt f (idris_implicits ist) of

686 = case lookupCtxt f (idris_implicits ist) of

580− Just ns -> pApp fc (length ns) (PRef fc f) (insertImpl ns as)

687+ Just ns -> mkPApp fc (length ns) (PRef fc f) (insertImpl ns as)

581− Nothing -> pApp fc 1 (PRef fc f) as

688+ Nothing -> mkPApp fc 1 (PRef fc f) as

582− aiFn fc env f as = pApp fc 1 f as

689+ where

583−

584− pApp fc a f [] = f

585− pApp fc a f as = let rest = drop a as in

586− appRest fc (PApp fc f (take a as)) rest

587−

588− appRest fc f [] = f

589− appRest fc f (a : as) = appRest fc (PApp fc f [a]) as

590−

591 insertImpl :: [PArg] -> [PArg] -> [PArg]

690 insertImpl :: [PArg] -> [PArg] -> [PArg]

592 insertImpl (PExp l ty : ps) (PExp _ tm : given) =

691 insertImpl (PExp l ty : ps) (PExp _ tm : given) =

593 PExp l tm : insertImpl ps given

692 PExp l tm : insertImpl ps given

@@ -603,6 +702,13 @@ addImpl ist ptm = ai [] ptm

603 | n == n' = Just (t, reverse acc ++ gs)

702 | n == n' = Just (t, reverse acc ++ gs)

604 find n (g : gs) acc = find n gs (g : acc)

703 find n (g : gs) acc = find n gs (g : acc)

605

704

705+mkPApp fc a f [] = f

706+mkPApp fc a f as = let rest = drop a as in

707+ appRest fc (PApp fc f (take a as)) rest

708+ where

709+ appRest fc f [] = f

710+ appRest fc f (a : as) = appRest fc (PApp fc f [a]) as

711+

606-- Find 'static' argument positions

712-- Find 'static' argument positions

607-- (the declared ones, plus any names in argument position in the declared

713-- (the declared ones, plus any names in argument position in the declared

608-- statics)

714-- statics)

@@ -640,9 +746,9 @@ dumpDecls [] = ""

640dumpDecls (d:ds) = dumpDecl d ++ "\n" ++ dumpDecls ds

746dumpDecls (d:ds) = dumpDecl d ++ "\n" ++ dumpDecls ds

641

747

642dumpDecl (PFix _ f ops) = show f ++ " " ++ showSep ", " ops

748dumpDecl (PFix _ f ops) = show f ++ " " ++ showSep ", " ops

643−dumpDecl (PTy _ n t) = "tydecl " ++ show n ++ " : " ++ showImp True t

749+dumpDecl (PTy _ _ n t) = "tydecl " ++ show n ++ " : " ++ showImp True t

644−dumpDecl (PClauses _ n cs) = "pat\t" ++ showSep "\n\t" (map (showCImp True) cs)

750+dumpDecl (PClauses _ n cs) = "pat " ++ show n ++ "\t" ++ showSep "\n\t" (map (showCImp True) cs)

645−dumpDecl (PData _ d) = showDImp True d

751+dumpDecl (PData _ _ d) = showDImp True d

646dumpDecl (PParams _ ns ps) = "params {" ++ show ns ++ "\n" ++ dumpDecls ps ++ "}\n"

752dumpDecl (PParams _ ns ps) = "params {" ++ show ns ++ "\n" ++ dumpDecls ps ++ "}\n"

647dumpDecl (PSyntax _ syn) = "syntax " ++ show syn

753dumpDecl (PSyntax _ syn) = "syntax " ++ show syn

648-- dumpDecl (PImport i) = "import " ++ i

754-- dumpDecl (PImport i) = "import " ++ i

src/Idris/ElabDecls.hs+145−76

@@ -31,43 +31,52 @@ checkDef ns = do ctxt <- getContext

31 mapM (\(n, t) -> do (t', _) <- tclift $ recheck ctxt [] t

32 return (n, t')) ns

34−elabType :: ElabInfo -> FC -> Name -> PTerm -> Idris ()

34+elabType :: ElabInfo -> SyntaxInfo -> FC -> Name -> PTerm -> Idris ()

35−elabType info fc n_in ty_in = let ty = piBind (params info) ty_in

35+elabType info syn fc n ty' = {- let ty' = piBind (params info) ty_in

36− n = liftname info n_in in

36+ n = liftname info n_in in -}

37 do checkUndefined fc n

38 ctxt <- getContext

39+ i <- get

40+ ty' <- implicit syn n ty'

41+ let ty = addImpl i ty'

39− logLvl 2 $ "Type " ++ showImp True ty

42+ logLvl 2 $ show n ++ " type " ++ showImp True ty

40 ((ty', defer), log) <- tclift $ elaborate ctxt n (Set 0)

43 ((ty', defer), log) <- tclift $ elaborate ctxt n (Set 0)

41− (erun fc (build info False ty))

44+ (erun fc (build i info False ty))

42 (cty, _) <- tclift $ recheck ctxt [] ty'

45 (cty, _) <- tclift $ recheck ctxt [] ty'

43 logLvl 2 $ "---> " ++ show cty

46 logLvl 2 $ "---> " ++ show cty

44 let nty = normalise ctxt [] cty

47 let nty = normalise ctxt [] cty

45 ds <- checkDef ((n, nty):defer)

48 ds <- checkDef ((n, nty):defer)

46 addDeferred ds

49 addDeferred ds

48−elabData :: ElabInfo -> FC -> PData -> Idris ()

51+elabData :: ElabInfo -> SyntaxInfo -> FC -> PData -> Idris ()

49−elabData info fc (PDatadecl n t dcons)

52+elabData info syn fc (PDatadecl n t_in dcons)

50 = do iLOG (show fc)

53 = do iLOG (show fc)

51 checkUndefined fc n

54 checkUndefined fc n

52 ctxt <- getContext

55 ctxt <- getContext

56+ i <- get

57+ t_in <- implicit syn n t_in

58+ let t = addImpl i t_in

53 ((t', defer), log) <- tclift $ elaborate ctxt n (Set 0)

59 ((t', defer), log) <- tclift $ elaborate ctxt n (Set 0)

54− (erun fc (build info False t))

60+ (erun fc (build i info False t))

55 def' <- checkDef defer

61 def' <- checkDef defer

56 addDeferred def'

62 addDeferred def'

57 (cty, _) <- tclift $ recheck ctxt [] t'

63 (cty, _) <- tclift $ recheck ctxt [] t'

58 logLvl 2 $ "---> " ++ show cty

64 logLvl 2 $ "---> " ++ show cty

59 updateContext (addTyDecl n cty) -- temporary, to check cons

65 updateContext (addTyDecl n cty) -- temporary, to check cons

60− cons <- mapM (elabCon info) dcons

66+ cons <- mapM (elabCon info syn) dcons

61 ttag <- getName

67 ttag <- getName

62 setContext (addDatatype (Data n ttag cty cons) ctxt)

68 setContext (addDatatype (Data n ttag cty cons) ctxt)

64−elabCon :: ElabInfo -> (Name, PTerm, FC) -> Idris (Name, Type)

70+elabCon :: ElabInfo -> SyntaxInfo -> (Name, PTerm, FC) -> Idris (Name, Type)

65−elabCon info (n, t, fc)

71+elabCon info syn (n, t_in, fc)

66 = do checkUndefined fc n

72 = do checkUndefined fc n

67 ctxt <- getContext

73 ctxt <- getContext

74+ i <- get

75+ t_in <- implicit syn n t_in

76+ let t = addImpl i t_in

68 logLvl 2 $ show fc ++ ":Constructor " ++ show n ++ " : " ++ showImp True t

77 logLvl 2 $ show fc ++ ":Constructor " ++ show n ++ " : " ++ showImp True t

69 ((t', defer), log) <- tclift $ elaborate ctxt n (Set 0)

78 ((t', defer), log) <- tclift $ elaborate ctxt n (Set 0)

70− (erun fc (build info False t))

79+ (erun fc (build i info False t))

71 logLvl 2 $ "Rechecking " ++ show t'

80 logLvl 2 $ "Rechecking " ++ show t'

72 def' <- checkDef defer

81 def' <- checkDef defer

73 addDeferred def'

82 addDeferred def'

@@ -96,23 +105,28 @@ elabClauses info fc n_in cs = let n = liftname info n_in in

96 depat x = x

105 depat x = x

106

98elabVal :: ElabInfo -> PTerm -> Idris (Term, Type)

107elabVal :: ElabInfo -> PTerm -> Idris (Term, Type)

99−elabVal info tm

108+elabVal info tm_in

100 = do ctxt <- getContext

109 = do ctxt <- getContext

110+ i <- get

111+ let tm = addImpl i tm_in

101 logLvl 10 (showImp True tm)

112 logLvl 10 (showImp True tm)

102 ((tm', defer), _) <- tclift $ elaborate ctxt (MN 0 "val") infP

113 ((tm', defer), _) <- tclift $ elaborate ctxt (MN 0 "val") infP

103− (build info True (infTerm tm))

114+ (build i info True (infTerm tm))

104 logLvl 3 ("Value: " ++ show tm')

115 logLvl 3 ("Value: " ++ show tm')

105 let vtm = getInferTerm tm'

116 let vtm = getInferTerm tm'

106 logLvl 2 (show vtm)

117 logLvl 2 (show vtm)

107 tclift $ recheck ctxt [] vtm

118 tclift $ recheck ctxt [] vtm

108

119

109elabClause :: ElabInfo -> FC -> PClause -> Idris (Term, Term)

120elabClause :: ElabInfo -> FC -> PClause -> Idris (Term, Term)

110−elabClause info fc (PClause fname lhs withs rhs whereblock)

121+elabClause info fc (PClause fname lhs_in withs rhs_in whereblock)

111 = do ctxt <- getContext

122 = do ctxt <- getContext

112 -- Build the LHS as an "Infer", and pull out its type and

123 -- Build the LHS as an "Infer", and pull out its type and

113 -- pattern bindings

124 -- pattern bindings

125+ i <- get

126+ let lhs = addImpl i lhs_in

127+ logLvl 5 ("LHS: " ++ showImp True lhs)

114 ((lhs', dlhs), _) <- tclift $ elaborate ctxt (MN 0 "patLHS") infP

128 ((lhs', dlhs), _) <- tclift $ elaborate ctxt (MN 0 "patLHS") infP

115− (erun fc (build info True (infTerm lhs)))

129+ (erun fc (build i info True (infTerm lhs)))

116 let lhs_tm = getInferTerm lhs'

130 let lhs_tm = getInferTerm lhs'

117 let lhs_ty = getInferType lhs'

131 let lhs_ty = getInferType lhs'

118 logLvl 3 (show lhs_tm)

132 logLvl 3 (show lhs_tm)

@@ -122,14 +136,22 @@ elabClause info fc (PClause fname lhs withs rhs whereblock)

122 ist <- getIState

136 ist <- getIState

123 windex <- getName

137 windex <- getName

124 let winfo = pinfo (pvars ist lhs_tm) whereblock windex

138 let winfo = pinfo (pvars ist lhs_tm) whereblock windex

139+ let decls = concatMap declared whereblock

140+ let newargs = pvars ist lhs_tm

141+ let wb = map (expandParamsD decorate newargs decls) whereblock

142+ logLvl 5 $ show wb

125− mapM_ (elabDecl' winfo) whereblock

143+ mapM_ (elabDecl' info) wb

126 -- Now build the RHS, using the type of the LHS as the goal.

144 -- Now build the RHS, using the type of the LHS as the goal.

145+ i <- get -- new implicits from where block

146+ logLvl 5 (showImp True (expandParams decorate newargs decls rhs_in))

147+ let rhs = addImpl i (expandParams decorate newargs decls rhs_in)

148+ -- TODO: but don't do names in scope

127 logLvl 2 (showImp True rhs)

149 logLvl 2 (showImp True rhs)

128 ctxt <- getContext -- new context with where block added

150 ctxt <- getContext -- new context with where block added

129 ((rhs', defer), _) <-

151 ((rhs', defer), _) <-

130 tclift $ elaborate ctxt (MN 0 "patRHS") clhsty

152 tclift $ elaborate ctxt (MN 0 "patRHS") clhsty

131 (do pbinds lhs_tm

153 (do pbinds lhs_tm

132− (_, _) <- erun fc (build winfo False rhs)

154+ (_, _) <- erun fc (build i info False rhs)

133 psolve lhs_tm

155 psolve lhs_tm

134 tt <- get_term

156 tt <- get_term

135 return $ runState (collectDeferred tt) [])

157 return $ runState (collectDeferred tt) [])

@@ -141,6 +163,7 @@ elabClause info fc (PClause fname lhs withs rhs whereblock)

141 (crhs, crhsty) <- tclift $ recheck ctxt [] rhs'

163 (crhs, crhsty) <- tclift $ recheck ctxt [] rhs'

142 return (clhs, crhs)

164 return (clhs, crhs)

143 where

165 where

166+ decorate x = UN [show fname ++ "#" ++ show x]

144 pinfo ns ps i

167 pinfo ns ps i

145 = let ds = concatMap declared ps

168 = let ds = concatMap declared ps

146 newps = params info ++ ns

169 newps = params info ++ ns

@@ -149,32 +172,36 @@ elabClause info fc (PClause fname lhs withs rhs whereblock)

149 l = liftname info in

172 l = liftname info in

150 info { params = newps,

173 info { params = newps,

151 inblock = newb,

174 inblock = newb,

152− liftname = (\n -> case lookupCtxt n newb of

175+ liftname = id -- (\n -> case lookupCtxt n newb of

153− Nothing -> n

176+ -- Nothing -> n

154− _ -> MN i (show n)) . l

177+ -- _ -> MN i (show n)) . l

155 }

178 }

156

179

157−elabClause info fc (PWith fname lhs withs wval withblock)

180+elabClause info fc (PWith fname lhs_in withs wval_in withblock)

158 = do ctxt <- getContext

181 = do ctxt <- getContext

159 -- Build the LHS as an "Infer", and pull out its type and

182 -- Build the LHS as an "Infer", and pull out its type and

160 -- pattern bindings

183 -- pattern bindings

184+ i <- get

185+ let lhs = addImpl i lhs_in

186+ logLvl 5 ("LHS: " ++ showImp True lhs)

161 ((lhs', dlhs), _) <- tclift $ elaborate ctxt (MN 0 "patLHS") infP

187 ((lhs', dlhs), _) <- tclift $ elaborate ctxt (MN 0 "patLHS") infP

162− (erun fc (build info True (infTerm lhs)))

188+ (erun fc (build i info True (infTerm lhs)))

163 let lhs_tm = getInferTerm lhs'

189 let lhs_tm = getInferTerm lhs'

164 let lhs_ty = getInferType lhs'

190 let lhs_ty = getInferType lhs'

165 let ret_ty = getRetTy lhs_ty

191 let ret_ty = getRetTy lhs_ty

166 logLvl 3 (show lhs_tm)

192 logLvl 3 (show lhs_tm)

167 (clhs, clhsty) <- tclift $ recheck ctxt [] lhs_tm

193 (clhs, clhsty) <- tclift $ recheck ctxt [] lhs_tm

168 logLvl 5 ("Checked " ++ show clhs)

194 logLvl 5 ("Checked " ++ show clhs)

169− logLvl 5 ("Checking " ++ show wval)

170 let bargs = getPBtys lhs_tm

195 let bargs = getPBtys lhs_tm

196+ let wval = addImpl i wval_in

197+ logLvl 5 ("Checking " ++ showImp True wval)

171 -- Elaborate wval in this context

198 -- Elaborate wval in this context

172 ((wval', defer), _) <-

199 ((wval', defer), _) <-

173 tclift $ elaborate ctxt (MN 0 "withRHS")

200 tclift $ elaborate ctxt (MN 0 "withRHS")

174 (bindTyArgs PVTy bargs infP)

201 (bindTyArgs PVTy bargs infP)

175 (do pbinds lhs_tm

202 (do pbinds lhs_tm

176 -- TODO: may want where here - see winfo abpve

203 -- TODO: may want where here - see winfo abpve

177− (_', d) <- erun fc (build info False (infTerm wval))

204+ (_', d) <- erun fc (build i info False (infTerm wval))

178 psolve lhs_tm

205 psolve lhs_tm

179 tt <- get_term

206 tt <- get_term

180 return (tt, d))

207 return (tt, d))

@@ -188,6 +215,8 @@ elabClause info fc (PWith fname lhs withs wval withblock)

188 let wtype = bindTyArgs Pi (bargs ++ [(MN 0 "warg", getRetTy cwvalty)]) ret_ty

215 let wtype = bindTyArgs Pi (bargs ++ [(MN 0 "warg", getRetTy cwvalty)]) ret_ty

189 logLvl 3 ("New function type " ++ show wtype)

216 logLvl 3 ("New function type " ++ show wtype)

190 let wname = MN windex (show fname)

217 let wname = MN windex (show fname)

218+ let imps = getImps wtype -- add to implicits context

219+ put (i { idris_implicits = addDef wname imps (idris_implicits i) })

191 def' <- checkDef [(wname, wtype)]

220 def' <- checkDef [(wname, wtype)]

192 addDeferred def'

221 addDeferred def'

193

222

@@ -203,10 +232,11 @@ elabClause info fc (PWith fname lhs withs wval withblock)

203 [pexp wval])

232 [pexp wval])

204 logLvl 3 ("New RHS " ++ show rhs)

233 logLvl 3 ("New RHS " ++ show rhs)

205 ctxt <- getContext -- New context with block added

234 ctxt <- getContext -- New context with block added

235+ i <- get

206 ((rhs', defer), _) <-

236 ((rhs', defer), _) <-

207 tclift $ elaborate ctxt (MN 0 "wpatRHS") clhsty

237 tclift $ elaborate ctxt (MN 0 "wpatRHS") clhsty

208 (do pbinds lhs_tm

238 (do pbinds lhs_tm

209− (_, d) <- erun fc (build info False rhs)

239+ (_, d) <- erun fc (build i info False rhs)

210 psolve lhs_tm

240 psolve lhs_tm

211 tt <- get_term

241 tt <- get_term

212 return (tt, d))

242 return (tt, d))

@@ -215,21 +245,30 @@ elabClause info fc (PWith fname lhs withs wval withblock)

215 (crhs, crhsty) <- tclift $ recheck ctxt [] rhs'

245 (crhs, crhsty) <- tclift $ recheck ctxt [] rhs'

216 return (clhs, crhs)

246 return (clhs, crhs)

217 where

247 where

248+ getImps (Bind n (Pi _) t) = pexp Placeholder : getImps t

249+ getImps _ = []

250+

218 mkAuxC wname lhs ns (PClauses fc n cs)

251 mkAuxC wname lhs ns (PClauses fc n cs)

219 | n == fname = do cs' <- mapM (mkAux wname lhs ns) cs

252 | n == fname = do cs' <- mapM (mkAux wname lhs ns) cs

220 return $ PClauses fc wname cs'

253 return $ PClauses fc wname cs'

221 | otherwise = fail $ "with clause uses wrong function name " ++ show n

254 | otherwise = fail $ "with clause uses wrong function name " ++ show n

222 mkAuxC wname lhs ns d = return $ d

255 mkAuxC wname lhs ns d = return $ d

223

256

224− mkAux wname toplhs ns (PClause n tm (w:ws) rhs wheres)

257+ mkAux wname toplhs ns (PClause n tm_in (w:ws) rhs wheres)

258+ = do i <- get

259+ let tm = addImpl i tm_in

225− = do logLvl 2 ("Matching " ++ show tm ++ " against " ++ show toplhs)

260+ logLvl 2 ("Matching " ++ showImp True tm ++ " against " ++

261+ showImp True toplhs)

226 case matchClause toplhs tm of

262 case matchClause toplhs tm of

227 Nothing -> fail "with clause does not match top level"

263 Nothing -> fail "with clause does not match top level"

228 Just mvars -> do logLvl 3 ("Match vars : " ++ show mvars)

264 Just mvars -> do logLvl 3 ("Match vars : " ++ show mvars)

229 lhs <- updateLHS n wname mvars ns tm w

265 lhs <- updateLHS n wname mvars ns tm w

230 return $ PClause wname lhs ws rhs wheres

266 return $ PClause wname lhs ws rhs wheres

231− mkAux wname toplhs ns (PWith n tm (w:ws) wval wheres)

267+ mkAux wname toplhs ns (PWith n tm_in (w:ws) wval wheres)

268+ = do i <- get

269+ let tm = addImpl i tm_in

232− = do logLvl 2 ("Matching " ++ show tm ++ " against " ++ show toplhs)

270+ logLvl 2 ("Matching " ++ showImp True tm ++ " against " ++

271+ showImp True toplhs)

233 case matchClause toplhs tm of

272 case matchClause toplhs tm of

234 Nothing -> fail "with clause does not match top level"

273 Nothing -> fail "with clause does not match top level"

235 Just mvars -> do lhs <- updateLHS n wname mvars ns tm w

274 Just mvars -> do lhs <- updateLHS n wname mvars ns tm w

@@ -268,10 +307,10 @@ elabDecl info d = idrisCatch (elabDecl' info d) (\e -> iputStrLn (report e))

268

307

269elabDecl' info (PFix _ _ _) = return () -- nothing to elaborate

308elabDecl' info (PFix _ _ _) = return () -- nothing to elaborate

270elabDecl' info (PSyntax _ p) = return () -- nothing to elaborate

309elabDecl' info (PSyntax _ p) = return () -- nothing to elaborate

271−elabDecl' info (PTy f n ty) = do iLOG $ "Elaborating type decl " ++ show n

310+elabDecl' info (PTy s f n ty) = do iLOG $ "Elaborating type decl " ++ show n

272− elabType info f n ty

311+ elabType info s f n ty

273−elabDecl' info (PData f d) = do iLOG $ "Elaborating " ++ show (d_name d)

312+elabDecl' info (PData s f d) = do iLOG $ "Elaborating " ++ show (d_name d)

274− elabData info f d

313+ elabData info s f d

275elabDecl' info d@(PClauses f n ps) = do iLOG $ "Elaborating clause " ++ show n

314elabDecl' info d@(PClauses f n ps) = do iLOG $ "Elaborating clause " ++ show n

276 elabClauses info f n ps

315 elabClauses info f n ps

277elabDecl' info (PParams f ns ps) = mapM_ (elabDecl' pinfo) ps

316elabDecl' info (PParams f ns ps) = mapM_ (elabDecl' pinfo) ps

@@ -293,15 +332,17 @@ elabDecl' info (PParams f ns ps) = mapM_ (elabDecl' pinfo) ps

293

332

294-- Also find deferred names in the term and their types

333-- Also find deferred names in the term and their types

295

334

296−build :: ElabInfo -> Bool -> PTerm -> Elab (Term, [(Name, Type)])

335+build :: IState -> ElabInfo -> Bool -> PTerm -> Elab (Term, [(Name, Type)])

336+build ist info pattern tm

297−build info pattern tm = do elab info pattern tm

337+ = do elab ist info pattern tm

298− tt <- get_term

338+ tt <- get_term

299− return $ runState (collectDeferred tt) []

339+ return $ runState (collectDeferred tt) []

300−

340+

301−elab :: ElabInfo -> Bool -> PTerm -> Elab ()

341+elab :: IState -> ElabInfo -> Bool -> PTerm -> Elab ()

302−elab info pattern tm = do elab' tm

342+elab ist info pattern tm

343+ = do elabE tm

303− when pattern -- convert remaining holes to pattern vars

344+ when pattern -- convert remaining holes to pattern vars

304− mkPat

345+ mkPat

305 where

346 where

306 isph arg = case getTm arg of

347 isph arg = case getTm arg of

307 Placeholder -> True

348 Placeholder -> True

@@ -309,13 +350,39 @@ elab info pattern tm = do elab' tm

309

350

310 toElab arg = case getTm arg of

351 toElab arg = case getTm arg of

311 Placeholder -> Nothing

352 Placeholder -> Nothing

312− v -> Just (elab' v)

353+ v -> Just (elabE v)

313

354

314 mkPat = do hs <- get_holes

355 mkPat = do hs <- get_holes

315 case hs of

356 case hs of

316 (h: hs) -> do patvar h; mkPat

357 (h: hs) -> do patvar h; mkPat

317 [] -> return ()

358 [] -> return ()

318

359

360+ -- Expand implict arguments here, then move on to main elaborator

361+-- elabE (PRef fc n)

362+-- | Just ps <- lookupCtxt n (inblock info)

363+-- = -- let exp = (PApp fc (PRef fc n) (map (pexp . (PRef fc)) ps))

364+-- elabE (PApp fc (PRef fc n) [])

365+-- elabE f@(PApp fc fn args) = trace ("Elaborating " ++ show f) $ elab' f

366+-- elabE (PRef fc f)

367+-- = do l <- local f

368+-- elabN f l

369+-- where elabN f False = let afn = aiFn ist fc f [] in

370+-- -- trace ("Ref expanded to " ++ showImp True afn) $

371+-- elab' afn

372+-- elabN f True = elab' (PRef fc f)

373+-- elabE (PApp fc fn@(PRef _ f) args)

374+-- = do l <- local f

375+-- elabApp f args l -- no implicits

376+-- where elabApp f args False = let afn = aiFn ist fc f args in

377+-- -- trace ("Expanded to " ++ showImp True afn) $

378+-- elab' afn

379+-- elabApp f args True = elab' (PApp fc fn args)

380+-- elabE (PApp fc f as) = elab' (mkPApp fc 1 f as)

381+ elabE t = elab' t

382+

383+ local f = do e <- get_env

384+ return (f `elem` map fst e)

385+

319 elab' PSet = do fill (RSet 0); solve

386 elab' PSet = do fill (RSet 0); solve

320 elab' (PConstant c) = do apply (RConstant c) []; solve

387 elab' (PConstant c) = do apply (RConstant c) []; solve

321 elab' (PQuote r) = do fill r; solve

388 elab' (PQuote r) = do fill r; solve

@@ -327,9 +394,9 @@ elab info pattern tm = do elab' tm

327 elab' (PEq fc l r) = elab' (PApp fc (PRef fc eqTy) [pimp (MN 0 "a") Placeholder,

394 elab' (PEq fc l r) = elab' (PApp fc (PRef fc eqTy) [pimp (MN 0 "a") Placeholder,

328 pimp (MN 0 "b") Placeholder,

395 pimp (MN 0 "b") Placeholder,

329 pexp l, pexp r])

396 pexp l, pexp r])

330− elab' (PPair fc l r) = try (elab' (PApp fc (PRef fc pairTy)

397+ elab' (PPair fc l r) = try (elabE (PApp fc (PRef fc pairTy)

331 [pexp l,pexp r]))

398 [pexp l,pexp r]))

332− (elab' (PApp fc (PRef fc pairCon)

399+ (elabE (PApp fc (PRef fc pairCon)

333 [pimp (MN 0 "A") Placeholder,

400 [pimp (MN 0 "A") Placeholder,

334 pimp (MN 0 "B") Placeholder,

401 pimp (MN 0 "B") Placeholder,

335 pexp l, pexp r]))

402 pexp l, pexp r]))

@@ -352,21 +419,18 @@ elab info pattern tm = do elab' tm

352 where inparamBlock n = case lookupCtxt n (inblock info) of

419 where inparamBlock n = case lookupCtxt n (inblock info) of

353 Nothing -> False

420 Nothing -> False

354 _ -> True

421 _ -> True

355− elab' (PRef fc n)

356− | Just ps <- lookupCtxt n (inblock info)

357− = elab' (PApp fc (PRef fc n) [])

358− | otherwise = erun fc $ do apply (Var n) []; solve

422+ elab' (PRef fc n) = erun fc $ do apply (Var n) []; solve

359 elab' (PLam n Placeholder sc)

423 elab' (PLam n Placeholder sc)

360− = do attack; intro (Just n); elab' sc; solve

424+ = do attack; intro (Just n); elabE sc; solve

361 elab' (PPi _ n Placeholder sc)

425 elab' (PPi _ n Placeholder sc)

362− = do attack; arg n (MN 0 "ty"); elab' sc; solve

426+ = do attack; arg n (MN 0 "ty"); elabE sc; solve

363 elab' (PPi _ n ty sc)

427 elab' (PPi _ n ty sc)

364 = do attack; tyn <- unique_hole (MN 0 "ty")

428 = do attack; tyn <- unique_hole (MN 0 "ty")

365 claim tyn (RSet 0)

429 claim tyn (RSet 0)

366 forall n (Var tyn)

430 forall n (Var tyn)

367 focus tyn

431 focus tyn

368− elab' ty

432+ elabE ty

369− elab' sc

433+ elabE sc

370 solve

434 solve

371 elab' (PLet n Placeholder val sc)

435 elab' (PLet n Placeholder val sc)

372 = do attack; -- (h:_) <- get_holes

436 = do attack; -- (h:_) <- get_holes

@@ -377,29 +441,27 @@ elab info pattern tm = do elab' tm

377 claim valn (Var tyn)

441 claim valn (Var tyn)

378 letbind n (Var tyn) (Var valn)

442 letbind n (Var tyn) (Var valn)

379 focus valn

443 focus valn

380− elab' val

444+ elabE val

381− elab' sc

445+ elabE sc

382 -- end_unify

446 -- end_unify

383 solve

447 solve

384− elab' (PApp fc (PRef _ f) args)

448+ elab' (PApp fc (PRef _ f) args')

385− | Just ps <- lookupCtxt f (inblock info)

449+ = do let args = {- case lookupCtxt f (inblock info) of

386− = erun fc $

387− elabApp (liftname info f) (map (pexp . (PRef fc)) ps ++ args)

450+ Just ps -> (map (pexp . (PRef fc)) ps ++ args')

388− | otherwise = erun fc $ elabApp f args

451+ _ ->-} args'

389− where elabApp f args

390− = try (do ns <- apply (Var f) (map isph args)

452+ try (do ns <- apply (Var f) (map isph args)

391− solve

453+ solve

392− elabArgs ns (map (\x -> (lazyarg x, getTm x)) args))

454+ elabArgs ns (map (\x -> (lazyarg x, getTm x)) args))

393− (do apply_elab f (map toElab args)

455+ (do apply_elab f (map toElab args)

394− solve)

456+ solve)

395 elab' (PApp fc f [arg])

457 elab' (PApp fc f [arg])

396 = erun fc $

458 = erun fc $

397− do simple_app (elab' f) (elab' (getTm arg))

459+ do simple_app (elabE f) (elabE (getTm arg))

398 solve

460 solve

399 elab' Placeholder = do (h : hs) <- get_holes

461 elab' Placeholder = do (h : hs) <- get_holes

400 movelast h

462 movelast h

401 elab' (PMetavar n) = do attack; defer n; solve

463 elab' (PMetavar n) = do attack; defer n; solve

402− elab' (PProof ts) = do mapM_ (runTac True) ts

464+ elab' (PProof ts) = do mapM_ (runTac True ist) ts

403 elab' (PElabError e) = fail e

465 elab' (PElabError e) = fail e

404 elab' x = fail $ "Not implemented " ++ show x

466 elab' x = fail $ "Not implemented " ++ show x

405

467

@@ -412,7 +474,7 @@ elab info pattern tm = do elab' tm

412 pexp t]);

474 pexp t]);

413 elabArgs ns args

475 elabArgs ns args

414 | otherwise

476 | otherwise

415− = do focus n; elab' t; elabArgs ns args

477+ = do focus n; elabE t; elabArgs ns args

416

478

417

479

418collectDeferred :: Term -> State [(Name, Type)] Term

480collectDeferred :: Term -> State [(Name, Type)] Term

@@ -433,16 +495,23 @@ collectDeferred t = return t

433

495

434-- Running tactics directly

496-- Running tactics directly

435

497

436−runTac :: Bool -> PTactic -> Elab ()

498+runTac :: Bool -> IState -> PTactic -> Elab ()

437−runTac autoSolve = runT where

499+runTac autoSolve ist tac = runT (fmap (addImpl ist) tac) where

438 runT (Intro []) = do g <- goal

500 runT (Intro []) = do g <- goal

439 attack; intro (bname g)

501 attack; intro (bname g)

440 where

502 where

441 bname (Bind n _ _) = Just n

503 bname (Bind n _ _) = Just n

442 bname _ = Nothing

504 bname _ = Nothing

443 runT (Intro xs) = mapM_ (\x -> do attack; intro (Just x)) xs

505 runT (Intro xs) = mapM_ (\x -> do attack; intro (Just x)) xs

444− runT (Exact tm) = do elab toplevel False tm

506+ runT (Exact tm) = do elab ist toplevel False tm

445 when autoSolve solveAll

507 when autoSolve solveAll

508+ runT (Refine fn []) = do let imps = case lookupCtxt fn (idris_implicits ist) of

509+ Nothing -> []

510+ Just args -> map isImp args

511+ ns <- apply (Var fn) imps

512+ when autoSolve solveAll

513+ where isImp (PImp _ _ _) = True

514+ isImp _ = False

446 runT (Refine fn imps) = do ns <- apply (Var fn) imps

515 runT (Refine fn imps) = do ns <- apply (Var fn) imps

447 when autoSolve solveAll

516 when autoSolve solveAll

448 runT (Rewrite tm) -- to elaborate tm, let bind it, then rewrite by that

517 runT (Rewrite tm) -- to elaborate tm, let bind it, then rewrite by that

@@ -455,17 +524,17 @@ runTac autoSolve = runT where

455 letn <- unique_hole (MN 0 "rewrite_rule")

524 letn <- unique_hole (MN 0 "rewrite_rule")

456 letbind letn (Var tyn) (Var valn)

525 letbind letn (Var tyn) (Var valn)

457 focus valn

526 focus valn

458− elab toplevel False tm

527+ elab ist toplevel False tm

459 rewrite (Var letn)

528 rewrite (Var letn)

460 when autoSolve solveAll

529 when autoSolve solveAll

461 runT Compute = compute

530 runT Compute = compute

462− runT Trivial = try (do elab toplevel False (PRefl (FC "prf" 0))

531+ runT Trivial = try (do elab ist toplevel False (PRefl (FC "prf" 0))

463 when autoSolve solveAll)

532 when autoSolve solveAll)

464 (do env <- get_env

533 (do env <- get_env

465 tryAll (map fst env))

534 tryAll (map fst env))

466 where

535 where

467 tryAll [] = fail "No trivial solution"

536 tryAll [] = fail "No trivial solution"

468− tryAll (x:xs) = try (do elab toplevel False (PRef (FC "prf" 0) x)

537+ tryAll (x:xs) = try (do elab ist toplevel False (PRef (FC "prf" 0) x)

469 when autoSolve solveAll)

538 when autoSolve solveAll)

470 (tryAll xs)

539 (tryAll xs)

471 runT (Focus n) = focus n

540 runT (Focus n) = focus n

src/Idris/Parser.hs+40−46

@@ -67,6 +67,7 @@ loadSource f = do iLOG ("Reading " ++ f)

67 ds <- parseProg defaultSyntax f rest pos

68 logLvl 3 (dumpDecls ds)

69 i <- getIState

70+ logLvl 10 (show (toAlist (idris_implicits i)))

70 logLvl 3 (show (idris_infixes i))

71 logLvl 3 (show (idris_infixes i))

71 -- Now add all the declarations to the context

72 -- Now add all the declarations to the context

72 mapM_ (elabDecl toplevel) ds

73 mapM_ (elabDecl toplevel) ds

@@ -115,6 +116,7 @@ parseProg syn fname input pos

115 return (collect x)

116 return (collect x)

116

117

117-- Collect PClauses with the same function name

118-- Collect PClauses with the same function name

119+

118collect :: [PDecl] -> [PDecl]

120collect :: [PDecl] -> [PDecl]

119collect (c@(PClauses _ _ _) : ds)

121collect (c@(PClauses _ _ _) : ds)

120 = clauses (cname c) [] (c : ds)

122 = clauses (cname c) [] (c : ds)

@@ -210,11 +212,12 @@ pSynSym = try (do lchar '['; n <- pName; lchar ']'

210 return (Symbol sym)

212 return (Symbol sym)

211

213

212pFunDecl' :: SyntaxInfo -> IParser PDecl

214pFunDecl' :: SyntaxInfo -> IParser PDecl

213−pFunDecl' syn = try (do n <- pfName; ty <- pTSig syn

215+pFunDecl' syn = try (do n <- pfName;

216+ ty <- pTSig syn

214 fc <- pfc

217 fc <- pfc

215 lchar ';'

218 lchar ';'

216− ty' <- implicit syn n ty

219+-- ty' <- implicit syn n ty

217− return (PTy fc n ty'))

220+ return (PTy syn fc n ty))

218 <|> try (pPattern syn)

221 <|> try (pPattern syn)

219

222

220pUsing :: SyntaxInfo -> IParser [PDecl]

223pUsing :: SyntaxInfo -> IParser [PDecl]

@@ -475,10 +478,10 @@ pData :: SyntaxInfo -> IParser PDecl

475pData syn = try (do reserved "data"; fc <- pfc

478pData syn = try (do reserved "data"; fc <- pfc

476 tyn <- pfName; ty <- pTSig syn

479 tyn <- pfName; ty <- pTSig syn

477 reserved "where"

480 reserved "where"

478− ty' <- implicit syn tyn ty

481+-- ty' <- implicit syn tyn ty

479 cons <- sepBy (pConstructor syn) (lchar '|')

482 cons <- sepBy (pConstructor syn) (lchar '|')

480 lchar ';'

483 lchar ';'

481− return $ PData fc (PDatadecl tyn ty' cons))

484+ return $ PData syn fc (PDatadecl tyn ty cons))

482 <|> do reserved "data"; fc <- pfc

485 <|> do reserved "data"; fc <- pfc

483 tyn <- pfName; args <- many pName

486 tyn <- pfName; args <- many pName

484 lchar '='

487 lchar '='

@@ -486,15 +489,15 @@ pData syn = try (do reserved "data"; fc <- pfc

486 lchar ';'

489 lchar ';'

487 let conty = mkPApp fc (PRef fc tyn) (map (PRef fc) args)

490 let conty = mkPApp fc (PRef fc tyn) (map (PRef fc) args)

488 let ty = bindArgs (map (\a -> PSet) args) PSet

491 let ty = bindArgs (map (\a -> PSet) args) PSet

489− ty' <- implicit syn tyn ty

492+-- ty' <- implicit syn tyn ty

490 cons' <- mapM (\ (x, cargs, cfc) ->

493 cons' <- mapM (\ (x, cargs, cfc) ->

491 do let cty = bindArgs cargs conty

494 do let cty = bindArgs cargs conty

492− cty' <- implicit syn x cty

495+-- cty' <- implicit syn x cty

493− return (x, cty', cfc)) cons

496+ return (x, cty, cfc)) cons

494− return $ PData fc (PDatadecl tyn ty' cons')

497+ return $ PData syn fc (PDatadecl tyn ty cons')

495−

498+ where

496−mkPApp fc t [] = t

499+ mkPApp fc t [] = t

497−mkPApp fc t xs = PApp fc t (map pexp xs)

500+ mkPApp fc t xs = PApp fc t (map pexp xs)

498

501

499bindArgs :: [PTerm] -> PTerm -> PTerm

502bindArgs :: [PTerm] -> PTerm -> PTerm

500bindArgs [] t = t

503bindArgs [] t = t

@@ -504,8 +507,8 @@ pConstructor :: SyntaxInfo -> IParser (Name, PTerm, FC)

504pConstructor syn

507pConstructor syn

505 = do cn <- pfName; fc <- pfc

508 = do cn <- pfName; fc <- pfc

506 ty <- pTSig syn

509 ty <- pTSig syn

507− ty' <- implicit syn cn ty

510+-- ty' <- implicit syn cn ty

508− return (cn, ty', fc)

511+ return (cn, ty, fc)

509

512

510pSimpleCon :: SyntaxInfo -> IParser (Name, [PTerm], FC)

513pSimpleCon :: SyntaxInfo -> IParser (Name, [PTerm], FC)

511pSimpleCon syn

514pSimpleCon syn

@@ -524,7 +527,9 @@ pPattern syn = do clause <- pClause syn

524whereSyn :: Name -> SyntaxInfo -> [PTerm] -> SyntaxInfo

527whereSyn :: Name -> SyntaxInfo -> [PTerm] -> SyntaxInfo

525whereSyn n syn args = let ns = concatMap allNamesIn args

528whereSyn n syn args = let ns = concatMap allNamesIn args

526 ni = no_imp syn in

529 ni = no_imp syn in

530+ syn { decoration = \x -> decorate n (decoration syn x),

527− syn { no_imp = nub (ni ++ ns) }

531+ no_imp = nub (ni ++ ns) }

532+ where decorate n x = UN [(show n ++ "_" ++ show x)]

528

533

529pClause :: SyntaxInfo -> IParser PClause

534pClause :: SyntaxInfo -> IParser PClause

530pClause syn

535pClause syn

@@ -538,9 +543,10 @@ pClause syn

538 ist <- getState

543 ist <- getState

539 let ctxt = tt_ctxt ist

544 let ctxt = tt_ctxt ist

540 let wsyn = whereSyn n syn (map getTm iargs ++ args ++ wargs)

545 let wsyn = whereSyn n syn (map getTm iargs ++ args ++ wargs)

541− wheres <- choice [pWhereblock wsyn, do lchar ';'; return []]

546+ (wheres, nmap) <- choice [pWhereblock n syn, do lchar ';'

547+ return ([], [])]

542 return $ PClause n (PApp fc (PRef fc n)

548 return $ PClause n (PApp fc (PRef fc n)

543− (iargs ++ map pexp args)) wargs rhs wheres)

549+ (iargs ++ map pexp args)) wargs rhs wheres)

544 <|> try (do n <- pfName

550 <|> try (do n <- pfName

545 iargs <- many (pImplicitArg syn)

551 iargs <- many (pImplicitArg syn)

546 fc <- pfc

552 fc <- pfc

@@ -563,8 +569,11 @@ pClause syn

563 wargs <- many (pWExpr syn)

569 wargs <- many (pWExpr syn)

564 lchar '='

570 lchar '='

565 rhs <- pExpr syn

571 rhs <- pExpr syn

572+ let wsyn = whereSyn n syn []

566− wheres <- choice [pWhereblock syn, do lchar ';'; return []]

573+ (wheres, nmap) <- choice [pWhereblock n syn, do lchar ';'

574+ return ([], [])]

567− return $ PClause n (PApp fc (PRef fc n) [pexp l,pexp r]) wargs rhs wheres

575+ return $ PClause n (PApp fc (PRef fc n) [pexp l,pexp r])

576+ wargs rhs wheres

568

577

569 <|> do l <- pSimpleExpr syn

578 <|> do l <- pSimpleExpr syn

570 op <- operator

579 op <- operator

@@ -583,11 +592,13 @@ pClause syn

583pWExpr :: SyntaxInfo -> IParser PTerm

592pWExpr :: SyntaxInfo -> IParser PTerm

584pWExpr syn = do lchar '|'; pExpr' syn

593pWExpr syn = do lchar '|'; pExpr' syn

585

594

586−pWhereblock :: SyntaxInfo -> IParser [PDecl]

595+pWhereblock :: Name -> SyntaxInfo -> IParser ([PDecl], [(Name, Name)])

596+pWhereblock n syn

587−pWhereblock syn = do reserved "where"; lchar '{'

597+ = do reserved "where"; lchar '{'

588− ds <- many1 $ pFunDecl syn;

598+ ds <- many1 $ pFunDecl syn;

599+ let dns = concatMap (concatMap declared) ds

589− lchar '}';

600+ lchar '}';

590− return $ concat ds

601+ return (concat ds, map (\x -> (x, decoration syn x)) dns)

591

602

592pTactic :: SyntaxInfo -> IParser PTactic

603pTactic :: SyntaxInfo -> IParser PTactic

593pTactic syn = do reserved "intro"; ns <- sepBy pName (lchar ',')

604pTactic syn = do reserved "intro"; ns <- sepBy pName (lchar ',')

@@ -597,10 +608,7 @@ pTactic syn = do reserved "intro"; ns <- sepBy pName (lchar ',')

597 return $ Refine n imps)

608 return $ Refine n imps)

598 <|> do reserved "refine"; n <- pName

609 <|> do reserved "refine"; n <- pName

599 i <- getState

610 i <- getState

600− let imps = case lookupCtxt n (idris_implicits i) of

601− Nothing -> []

602− Just args -> map isImp args

603− return $ Refine n imps

611+ return $ Refine n []

604 <|> do reserved "rewrite"; t <- pExpr syn;

612 <|> do reserved "rewrite"; t <- pExpr syn;

605 i <- getState

613 i <- getState

606 return $ Rewrite (desugar syn i t)

614 return $ Rewrite (desugar syn i t)

@@ -617,27 +625,13 @@ pTactic syn = do reserved "intro"; ns <- sepBy pName (lchar ',')

617 <|> do reserved "term"; return ProofTerm

625 <|> do reserved "term"; return ProofTerm

618 <|> do reserved "undo"; return Undo

626 <|> do reserved "undo"; return Undo

619 <|> do reserved "qed"; return Qed

627 <|> do reserved "qed"; return Qed

620− where isImp (PImp _ _ _) = True

628+ where

621− isImp _ = False

622− imp = do lchar '?'; return False

629+ imp = do lchar '?'; return False

623− <|> do lchar '_'; return True

630+ <|> do lchar '_'; return True

624−

625−

626−-- Dealing with implicit arguments

627−

628−implicit :: SyntaxInfo -> Name -> PTerm -> IParser PTerm

629−implicit syn n ptm

630− = do i <- getState

631− let (tm', impdata) = implicitise syn i ptm

632− let (tm'', spos) = findStatics i tm'

633− setState (i { idris_implicits = addDef n impdata (idris_implicits i) })

634− i <- getState

635− setState (i { idris_statics = addDef n spos (idris_statics i) })

636− return tm''

637

631

638desugar :: SyntaxInfo -> IState -> PTerm -> PTerm

632desugar :: SyntaxInfo -> IState -> PTerm -> PTerm

639desugar syn i t = let t' = expandDo (dsl_info syn) t in

633desugar syn i t = let t' = expandDo (dsl_info syn) t in

640− addImpl i t'

634+ t' -- addImpl i t'

641

635

642expandDo :: DSL -> PTerm -> PTerm

636expandDo :: DSL -> PTerm -> PTerm

643expandDo dsl (PLam n ty tm) = PLam n (expandDo dsl ty) (expandDo dsl tm)

637expandDo dsl (PLam n ty tm) = PLam n (expandDo dsl ty) (expandDo dsl tm)

src/Idris/Primitives.hs+1−1

@@ -94,7 +94,7 @@ elabPrim (Prim n ty i def epic)

95elabPrims :: Idris ()

96elabPrims = do mapM_ (elabDecl toplevel)

97− (map (PData (FC "builtin" 0))

97+ (map (PData defaultSyntax (FC "builtin" 0))

98 [inferDecl, unitDecl, falseDecl, pairDecl, eqDecl])

99 mapM_ elabPrim primitives

100

src/Idris/Prover.hs+1−1

@@ -102,7 +102,7 @@ ploop d prompt prf e

102 when (not (null hs)) $ fail "Incomplete proof"

103 return (False, e, True, prf)

104 Right tac -> do (_, e) <- elabStep e saveState

105− (_, st) <- elabStep e (runTac True tac)

105+ (_, st) <- elabStep e (runTac True i tac)

106 return (True, st, False, prf ++ [step]))

107 (\err -> do iputStrLn (report err)

108 return (False, e, False, prf))