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

git.iko.soy/Idris-dev

Improved where; implicit arguments now expanded during elaboration

commit1b1a0553ca0d65c802020725a4032da6dce94b7a authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateThu 3 Nov 2011, 00:34 (15 years ago) parent188dda5

10 files changed+358−176

compare with master

unifiedsplit

lib/io.idr+4−4 lib/list.idr+11−6 lib/vect.idr+7 src/Core/ProofState.hs+1 src/Core/Typecheck.hs+1−1 src/Idris/AbsSyntax.hs+147−41 src/Idris/ElabDecls.hs+145−76 src/Idris/Parser.hs+40−46 src/Idris/Primitives.hs+1−1 src/Idris/Prover.hs+1−1

lib/io.idr+4−4

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

1919interpFTy FUnit = ();

2020

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

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

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

24− mkForeign Nil ty = ty;

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

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

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

24+ mkForeign' Nil ty = ty;

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

2626}

2727

2828data FEnv : List FTy -> Set where

lib/list.idr+11−6

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

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

55rev : List a -> List a;

6−rev xs = revAcc Nil xs

7− where {

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

9− revAcc acc Nil = acc;

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

11− }

6+rev xs = revAcc Nil xs where {

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

8+ revAcc acc Nil = acc;

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

10+}

1211

1312length : List a -> Int;

1413length Nil = 0;

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

2423drop n Nil = Nil;

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

2625

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

1818vapp VNil ys = ys;

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

2020

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

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

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

277277 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

278279

279280letbind :: Name -> Raw -> Raw -> RunTactic

280281letbind 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)

4343 case fty' of

4444 Bind x (Pi s) t ->

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

4747 return (App fv av, apty)

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

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

src/Idris/AbsSyntax.hs+147−41

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

166166expl = Exp False Dynamic

167167

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

169− | PTy FC Name t -- type declaration

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

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

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

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

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

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

173173 | PSyntax FC Syntax

174174 deriving Functor

175175

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

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

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

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

178178 deriving Functor

179179

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

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

193193

194194declared :: PDecl -> [Name]

195195declared (PFix _ _ _) = []

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

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

197197declared (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

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

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

201201-- declared (PImport _) = []

202202

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+

203224-- High level language terms

204−--

225+

205226data PTerm = PQuote Raw

206227 | PRef FC Name

207228 | PLam Name PTerm PTerm

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

225246 | PElabError String -- error to report on elaboration

226247 deriving Eq

227248

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

229− | Refine Name [Bool] | Rewrite PTerm

230− | Exact PTerm | Compute | Trivial

231− | Solve

232− | Attack

233− | ProofState | ProofTerm | Undo

234− | Qed

235− deriving (Show, Eq)

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+

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

265+ | Refine Name [Bool] | Rewrite t

266+ | Exact t | Compute | Trivial

267+ | Solve

268+ | Attack

269+ | ProofState | ProofTerm | Undo

270+ | Qed

271+ deriving (Show, Eq, Functor)

236272

237−data PDo = DoExp FC PTerm

238− | DoBind FC Name PTerm

239− | DoLet FC Name PTerm

240− deriving Eq

273+type PTactic = PTactic' PTerm

274+

275+data PDo' t = DoExp FC t

276+ | DoBind FC Name t

277+ | DoLet FC Name t

278+ deriving (Eq, Functor)

279+

280+type PDo = PDo' PTerm

241281

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

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

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

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

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

269309 no_imp :: [Name],

310+ decoration :: Name -> Name,

270311 dsl_info :: DSL }

271312 deriving Show

272313

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

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

274315

275316--- Pretty printing declarations and terms

276317

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

279320

280321instance Show PDecl where

281322 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

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

284− show (PData _ d) = show d

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

285326

286327instance Show PClause where

287328 show c = showCImp True c

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

433474

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

435476

477+primNames = [unitTy, unitCon,

478+ falseTy, pairTy, pairCon,

479+ eqTy, eqCon, inferTy, inferCon]

480+

436481unitTy = MN 0 "__Unit"

437482unitCon = MN 0 "__II"

438483unitDecl = PDatadecl unitTy PSet

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

473518piBind [] t = t

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

475520

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+

476568-- Dealing with implicit arguments

477569

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

480572

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

482574

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+

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

484587implicitise syn ist tm

485588 = let uvars = using syn

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

545648addImpl :: IState -> PTerm -> PTerm

546649addImpl ist ptm = ai [] ptm

547650 where

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

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

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

550653 r' = ai env r in

551654 PEq fc l' r'

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

557660 PDPair fc l' r'

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

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

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

663+ aiFn ist fc f as'

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

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

563− aiFn fc env f' as'

666+ mkPApp fc 1 f' as'

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

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

566669 PLam n ty' sc'

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

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

574677 PPi p n ty' sc'

575678 ai env (PHidden tm) = PHidden (ai env tm)

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

576680 ai env tm = tm

577681

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

579686 = case lookupCtxt f (idris_implicits ist) of

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

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

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

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−

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

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

689+ where

591690 insertImpl :: [PArg] -> [PArg] -> [PArg]

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

593692 PExp l tm : insertImpl ps given

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

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

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

605704

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+

606712-- Find 'static' argument positions

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

608714-- statics)

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

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

641747

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

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

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

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

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

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

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

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

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

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

src/Idris/ElabDecls.hs+145−76

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

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

3232 return (n, t')) ns

3333

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

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

36− n = liftname info n_in in

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

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

36+ n = liftname info n_in in -}

3737 do checkUndefined fc n

3838 ctxt <- getContext

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

39+ i <- get

40+ ty' <- implicit syn n ty'

41+ let ty = addImpl i ty'

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

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

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

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

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

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

4447 let nty = normalise ctxt [] cty

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

4649 addDeferred ds

4750

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

49−elabData info fc (PDatadecl n t dcons)

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

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

5053 = do iLOG (show fc)

5154 checkUndefined fc n

5255 ctxt <- getContext

56+ i <- get

57+ t_in <- implicit syn n t_in

58+ let t = addImpl i t_in

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

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

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

5561 def' <- checkDef defer

5662 addDeferred def'

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

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

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

60− cons <- mapM (elabCon info) dcons

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

6167 ttag <- getName

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

6369

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

65−elabCon info (n, t, fc)

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

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

6672 = do checkUndefined fc n

6773 ctxt <- getContext

74+ i <- get

75+ t_in <- implicit syn n t_in

76+ let t = addImpl i t_in

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

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

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

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

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

7281 def' <- checkDef defer

7382 addDeferred def'

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

96105 depat x = x

97106

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

99−elabVal info tm

108+elabVal info tm_in

100109 = do ctxt <- getContext

110+ i <- get

111+ let tm = addImpl i tm_in

101112 logLvl 10 (showImp True tm)

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

103− (build info True (infTerm tm))

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

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

105116 let vtm = getInferTerm tm'

106117 logLvl 2 (show vtm)

107118 tclift $ recheck ctxt [] vtm

108119

109120elabClause :: 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)

111122 = do ctxt <- getContext

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

113124 -- pattern bindings

125+ i <- get

126+ let lhs = addImpl i lhs_in

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

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

116130 let lhs_tm = getInferTerm lhs'

117131 let lhs_ty = getInferType lhs'

118132 logLvl 3 (show lhs_tm)

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

122136 ist <- getIState

123137 windex <- getName

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

125− mapM_ (elabDecl' winfo) whereblock

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

143+ mapM_ (elabDecl' info) wb

126144 -- 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

127149 logLvl 2 (showImp True rhs)

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

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

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

131153 (do pbinds lhs_tm

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

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

133155 psolve lhs_tm

134156 tt <- get_term

135157 return $ runState (collectDeferred tt) [])

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

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

142164 return (clhs, crhs)

143165 where

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

144167 pinfo ns ps i

145168 = let ds = concatMap declared ps

146169 newps = params info ++ ns

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

149172 l = liftname info in

150173 info { params = newps,

151174 inblock = newb,

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

153− Nothing -> n

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

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

176+ -- Nothing -> n

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

155178 }

156179

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

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

158181 = do ctxt <- getContext

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

160183 -- pattern bindings

184+ i <- get

185+ let lhs = addImpl i lhs_in

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

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

163189 let lhs_tm = getInferTerm lhs'

164190 let lhs_ty = getInferType lhs'

165191 let ret_ty = getRetTy lhs_ty

166192 logLvl 3 (show lhs_tm)

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

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

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

170195 let bargs = getPBtys lhs_tm

196+ let wval = addImpl i wval_in

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

171198 -- Elaborate wval in this context

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

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

174201 (bindTyArgs PVTy bargs infP)

175202 (do pbinds lhs_tm

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

178205 psolve lhs_tm

179206 tt <- get_term

180207 return (tt, d))

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

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

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

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

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

192221 addDeferred def'

193222

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

203232 [pexp wval])

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

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

235+ i <- get

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

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

208238 (do pbinds lhs_tm

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

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

210240 psolve lhs_tm

211241 tt <- get_term

212242 return (tt, d))

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

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

216246 return (clhs, crhs)

217247 where

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

249+ getImps _ = []

250+

218251 mkAuxC wname lhs ns (PClauses fc n cs)

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

220253 return $ PClauses fc wname cs'

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

222255 mkAuxC wname lhs ns d = return $ d

223256

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

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

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

258+ = do i <- get

259+ let tm = addImpl i tm_in

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

261+ showImp True toplhs)

226262 case matchClause toplhs tm of

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

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

229265 lhs <- updateLHS n wname mvars ns tm w

230266 return $ PClause wname lhs ws rhs wheres

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

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

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

268+ = do i <- get

269+ let tm = addImpl i tm_in

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

271+ showImp True toplhs)

233272 case matchClause toplhs tm of

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

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

268307

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

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

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

272− elabType info f n ty

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

274− elabData info f d

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

311+ elabType info s f n ty

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

313+ elabData info s f d

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

276315 elabClauses info f n ps

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

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

293332

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

295334

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

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

298− tt <- get_term

299− return $ runState (collectDeferred tt) []

300−

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

302−elab info pattern tm = do elab' tm

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

304− mkPat

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

336+build ist info pattern tm

337+ = do elab ist info pattern tm

338+ tt <- get_term

339+ return $ runState (collectDeferred tt) []

340+

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

342+elab ist info pattern tm

343+ = do elabE tm

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

345+ mkPat

305346 where

306347 isph arg = case getTm arg of

307348 Placeholder -> True

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

309350

310351 toElab arg = case getTm arg of

311352 Placeholder -> Nothing

312− v -> Just (elab' v)

353+ v -> Just (elabE v)

313354

314355 mkPat = do hs <- get_holes

315356 case hs of

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

317358 [] -> return ()

318359

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+

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

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

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

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

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

328395 pimp (MN 0 "b") Placeholder,

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

331398 [pexp l,pexp r]))

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

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

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

334401 pimp (MN 0 "B") Placeholder,

335402 pexp l, pexp r]))

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

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

353420 Nothing -> False

354421 _ -> 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

359423 elab' (PLam n Placeholder sc)

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

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

361425 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

363427 elab' (PPi _ n ty sc)

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

365429 claim tyn (RSet 0)

366430 forall n (Var tyn)

367431 focus tyn

368− elab' ty

369− elab' sc

432+ elabE ty

433+ elabE sc

370434 solve

371435 elab' (PLet n Placeholder val sc)

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

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

377441 claim valn (Var tyn)

378442 letbind n (Var tyn) (Var valn)

379443 focus valn

380− elab' val

381− elab' sc

444+ elabE val

445+ elabE sc

382446 -- end_unify

383447 solve

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

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

386− = erun fc $

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

388− | otherwise = erun fc $ elabApp f args

389− where elabApp f args

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

391− solve

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

393− (do apply_elab f (map toElab args)

394− solve)

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

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

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

451+ _ ->-} args'

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

453+ solve

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

455+ (do apply_elab f (map toElab args)

456+ solve)

395457 elab' (PApp fc f [arg])

396458 = erun fc $

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

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

398460 solve

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

400462 movelast h

401463 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

403465 elab' (PElabError e) = fail e

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

405467

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

412474 pexp t]);

413475 elabArgs ns args

414476 | otherwise

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

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

416478

417479

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

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

433495

434496-- Running tactics directly

435497

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

437−runTac autoSolve = runT where

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

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

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

439501 attack; intro (bname g)

440502 where

441503 bname (Bind n _ _) = Just n

442504 bname _ = Nothing

443505 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

445507 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

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

447516 when autoSolve solveAll

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

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

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

456525 letbind letn (Var tyn) (Var valn)

457526 focus valn

458− elab toplevel False tm

527+ elab ist toplevel False tm

459528 rewrite (Var letn)

460529 when autoSolve solveAll

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

463532 when autoSolve solveAll)

464533 (do env <- get_env

465534 tryAll (map fst env))

466535 where

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

469538 when autoSolve solveAll)

470539 (tryAll xs)

471540 runT (Focus n) = focus n

src/Idris/Parser.hs+40−46

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

6767 ds <- parseProg defaultSyntax f rest pos

6868 logLvl 3 (dumpDecls ds)

6969 i <- getIState

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

7071 logLvl 3 (show (idris_infixes i))

7172 -- Now add all the declarations to the context

7273 mapM_ (elabDecl toplevel) ds

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

115116 return (collect x)

116117

117118-- Collect PClauses with the same function name

119+

118120collect :: [PDecl] -> [PDecl]

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

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

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

210212 return (Symbol sym)

211213

212214pFunDecl' :: SyntaxInfo -> IParser PDecl

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

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

216+ ty <- pTSig syn

214217 fc <- pfc

215218 lchar ';'

216− ty' <- implicit syn n ty

217− return (PTy fc n ty'))

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

220+ return (PTy syn fc n ty))

218221 <|> try (pPattern syn)

219222

220223pUsing :: SyntaxInfo -> IParser [PDecl]

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

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

476479 tyn <- pfName; ty <- pTSig syn

477480 reserved "where"

478− ty' <- implicit syn tyn ty

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

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

480483 lchar ';'

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

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

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

483486 tyn <- pfName; args <- many pName

484487 lchar '='

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

486489 lchar ';'

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

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

489− ty' <- implicit syn tyn ty

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

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

491494 do let cty = bindArgs cargs conty

492− cty' <- implicit syn x cty

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

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

495−

496−mkPApp fc t [] = t

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

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

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

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

498+ where

499+ mkPApp fc t [] = t

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

498501

499502bindArgs :: [PTerm] -> PTerm -> PTerm

500503bindArgs [] t = t

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

504507pConstructor syn

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

506509 ty <- pTSig syn

507− ty' <- implicit syn cn ty

508− return (cn, ty', fc)

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

511+ return (cn, ty, fc)

509512

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

511514pSimpleCon syn

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

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

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

526529 ni = no_imp syn in

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

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

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

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

528533

529534pClause :: SyntaxInfo -> IParser PClause

530535pClause syn

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

538543 ist <- getState

539544 let ctxt = tt_ctxt ist

540545 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 ([], [])]

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

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

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

544550 <|> try (do n <- pfName

545551 iargs <- many (pImplicitArg syn)

546552 fc <- pfc

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

563569 wargs <- many (pWExpr syn)

564570 lchar '='

565571 rhs <- pExpr syn

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

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

572+ let wsyn = whereSyn n syn []

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

574+ return ([], [])]

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

576+ wargs rhs wheres

568577

569578 <|> do l <- pSimpleExpr syn

570579 op <- operator

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

583592pWExpr :: SyntaxInfo -> IParser PTerm

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

585594

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

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

588− ds <- many1 $ pFunDecl syn;

589− lchar '}';

590− return $ concat ds

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

596+pWhereblock n syn

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

598+ ds <- many1 $ pFunDecl syn;

599+ let dns = concatMap (concatMap declared) ds

600+ lchar '}';

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

591602

592603pTactic :: SyntaxInfo -> IParser PTactic

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

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

597608 return $ Refine n imps)

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

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

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

605613 i <- getState

606614 return $ Rewrite (desugar syn i t)

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

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

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

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

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

621− isImp _ = False

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

623− <|> 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''

628+ where

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

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

637631

638632desugar :: SyntaxInfo -> IState -> PTerm -> PTerm

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

640− addImpl i t'

634+ t' -- addImpl i t'

641635

642636expandDo :: DSL -> PTerm -> PTerm

643637expandDo 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)

9494

9595elabPrims :: Idris ()

9696elabPrims = do mapM_ (elabDecl toplevel)

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

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

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

9999 mapM_ elabPrim primitives

100100

src/Idris/Prover.hs+1−1

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

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

103103 return (False, e, True, prf)

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

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

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

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

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

108108 return (False, e, False, prf))