e0cab49 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Allow implicits to appear anywhere

This is still limited: in particular, there are no implicit lambdas and you can't give values of scoped implicits explicitl, unlike top level implicits. Basically, if the elaborator sees it's making something of type ({x : _} -> y} it will wrap an implicit lambda around it. If it sees any scoped implicits in the name it's elaborating, it will add an implicit _.

commite0cab49c176be889d8abe8049d996443e54e7287 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSun 11 Jan 2015, 19:32 (12 years ago) parent17fe233

13 files changed+89−51

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+6−6 src/Idris/AbsSyntaxTree.hs+10−3 src/Idris/Core/Elaborate.hs+17−12 src/Idris/Core/ProofState.hs+6−6 src/Idris/DeepSeq.hs+2−2 src/Idris/Delaborate.hs+1−1 src/Idris/Elab/Class.hs+5−4 src/Idris/Elab/Instance.hs+2−2 src/Idris/Elab/Record.hs+4−4 src/Idris/Elab/Utils.hs+1−1 src/Idris/ElabTerm.hs+27−6 src/Idris/IBC.hs+4−2 src/Idris/ParseExpr.hs+4−2

src/Idris/AbsSyntax.hs+6−6

@@ -1242,7 +1242,7 @@ addUsingImpls syn n fc t

12421242 -- if all of args in ns, then add it

12431243 doAdd (UImplicit n ty : cs) ns t

12441244 | elem n ns

1245− = PPi (Imp [] Dynamic False) n ty (doAdd cs ns t)

1245+ = PPi (Imp [] Dynamic False False) n ty (doAdd cs ns t)

12461246 | otherwise = doAdd cs ns t

12471247

12481248 -- bind the free names which weren't in the using block

@@ -1250,7 +1250,7 @@ addUsingImpls syn n fc t

12501250 bindFree (n:ns) tm

12511251 | elem n (map iname uimpls) = bindFree ns tm

12521252 | otherwise

1253− = PPi (Imp [] Dynamic False) n Placeholder (bindFree ns tm)

1253+ = PPi (Imp [] Dynamic False False) n Placeholder (bindFree ns tm)

12541254

12551255 getArgnames (PPi _ n c sc)

12561256 = n : getArgnames sc

@@ -1269,7 +1269,7 @@ getUnboundImplicits i t tm = getImps t (collectImps tm)

12691269 getImps (Bind n (Pi _ t _) sc) imps

12701270 | Just (p, t') <- lookup n imps = argInfo n p t' : getImps sc imps

12711271 where

1272− argInfo n (Imp opt _ _) t'

1272+ argInfo n (Imp opt _ _ _) t'

12731273 = (True, PImp (getPriority i t') True opt n t')

12741274 argInfo n (Exp opt _ _) t'

12751275 = (InaccessibleArg `elem` opt,

@@ -1359,7 +1359,7 @@ implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $

13591359 = do (decls, ns) <- get

13601360 let isn = concatMap (namesIn uvars ist) (map getTm as)

13611361 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))

1362− imps top env (PPi (Imp l _ _) n ty sc)

1362+ imps top env (PPi (Imp l _ _ _) n ty sc)

13631363 = do let isn = nub (implNamesIn uvars ty) `dropAll` [n]

13641364 (decls , ns) <- get

13651365 put (PImp (getPriority ist ty) True l n Placeholder : decls,

@@ -1427,8 +1427,8 @@ implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $

14271427 pibind using [] sc = sc

14281428 pibind using (n:ns) sc

14291429 = case lookup n using of

1430− Just ty -> PPi (Imp [] Dynamic False) n ty (pibind using ns sc)

1431− Nothing -> PPi (Imp [] Dynamic False) n Placeholder

1430+ Just ty -> PPi (Imp [] Dynamic False False) n ty (pibind using ns sc)

1431+ Nothing -> PPi (Imp [] Dynamic False False) n Placeholder

14321432 (pibind using ns sc)

14331433

14341434-- Add implicit arguments in function calls

src/Idris/AbsSyntaxTree.hs+10−3

@@ -488,7 +488,9 @@ deriving instance NFData Static

488488-- Mark bindings with their explicitness, and laziness

489489data Plicity = Imp { pargopts :: [ArgOpt],

490490 pstatic :: Static,

491− pparam :: Bool }

491+ pparam :: Bool,

492+ pscoped :: Bool -- forall bound

493+ }

492494 | Exp { pargopts :: [ArgOpt],

493495 pstatic :: Static,

494496 pparam :: Bool } -- this is a param (rather than index)

@@ -504,7 +506,12 @@ deriving instance Binary Plicity

504506deriving instance NFData Plicity

505507!-}

506508

507−impl = Imp [] Dynamic False

509+is_scoped :: Plicity -> Bool

510+is_scoped (Imp _ _ _ s) = s

511+is_scoped _ = False

512+

513+impl = Imp [] Dynamic False False

514+forall_imp = Imp [] Dynamic False True

508515expl = Exp [] Dynamic False

509516expl_param = Exp [] Dynamic True

510517constraint = Constraint [] Static

@@ -1326,7 +1333,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd

13261333 case s of

13271334 Static -> text "[static]" <> space

13281335 _ -> empty

1329− prettySe p bnd (PPi (Imp l s _) n ty sc)

1336+ prettySe p bnd (PPi (Imp l s _ fa) n ty sc)

13301337 | ppopt_impl ppo =

13311338 bracket p startPrec $

13321339 lbrace <> bindingOf n True <+> colon <+> prettySe startPrec bnd ty <> rbrace <+>

src/Idris/Core/Elaborate.hs+17−12

@@ -369,8 +369,8 @@ intro n = processTactic' (Intro n)

369369introTy :: Raw -> Maybe Name -> Elab' aux ()

370370introTy ty n = processTactic' (IntroTy ty n)

371371

372−forall :: Name -> Raw -> Elab' aux ()

373−forall n t = processTactic' (Forall n t)

372+forall :: Name -> Bool -> Raw -> Elab' aux ()

373+forall n i t = processTactic' (Forall n i t)

374374

375375letbind :: Name -> Raw -> Raw -> Elab' aux ()

376376letbind n t v = processTactic' (LetBind n t v)

@@ -493,7 +493,9 @@ prepare_apply fn imps =

493493 env <- get_env

494494 -- let claims = getArgs ty imps

495495 -- claims <- mkClaims (normalise ctxt env ty) imps []

496− claims <- mkClaims (finalise ty) imps [] (map fst env)

496+ claims <- mkClaims (finalise ty)

497+ (normalise ctxt env (finalise ty))

498+ imps [] (map fst env)

497499 ES (p, a) s prev <- get

498500 -- reverse the claims we made so that args go left to right

499501 let n = length (filter not imps)

@@ -502,11 +504,12 @@ prepare_apply fn imps =

502504 return $! claims

503505 where

504506 mkClaims :: Type -- ^ The type of the operation being applied

507+ -> Type -- ^ Normalised version if we need it

505508 -> [Bool] -- ^ Whether the arguments are implicit

506509 -> [(Name, Name)] -- ^ Accumulator for produced claims

507510 -> [Name] -- ^ Hypotheses

508511 -> Elab' aux [(Name, Name)] -- ^ The names of the arguments and their holes, resp.

509− mkClaims (Bind n' (Pi _ t_in _) sc) (i : is) claims hs =

512+ mkClaims (Bind n' (Pi _ t_in _) sc) (Bind _ _ scn) (i : is) claims hs =

510513 do let t = rebind hs t_in

511514 n <- getNameFrom (mkMN n')

512515-- when (null claims) (start_unify n)

@@ -514,9 +517,11 @@ prepare_apply fn imps =

514517-- trace ("CLAIMING " ++ show (n, t) ++ " with " ++ show (fn, hs)) $

515518 claim n (forget t)

516519 when i (movelast n)

517− mkClaims sc' is ((n', n) : claims) hs

518− mkClaims t [] claims _ = return $! (reverse claims)

519− mkClaims _ _ _ _

520+ mkClaims sc' scn is ((n', n) : claims) hs

521+ -- if we run out of arguments, we need the normalised version...

522+ mkClaims t tn@(Bind _ _ sc) (i : is) cs hs = mkClaims tn tn (i : is) cs hs

523+ mkClaims t _ [] claims _ = return $! (reverse claims)

524+ mkClaims _ _ _ _ _

520525 | Var n <- fn

521526 = do ctxt <- get_context

522527 case lookupTy n ctxt of

@@ -693,11 +698,11 @@ simple_app fun arg appstr =

693698

694699-- Abstract over an argument of unknown type, giving a name for the hole

695700-- which we'll fill with the argument type too.

696−arg :: Name -> Name -> Elab' aux ()

697−arg n tyhole = do ty <- unique_hole tyhole

698− claim ty RType

699− movelast ty

700− forall n (Var ty)

701+arg :: Name -> Bool -> Name -> Elab' aux ()

702+arg n i tyhole = do ty <- unique_hole tyhole

703+ claim ty RType

704+ movelast ty

705+ forall n i (Var ty)

701706

702707-- try a tactic, if it adds any unification problem, return an error

703708no_errors :: Elab' aux () -> Maybe Err -> Elab' aux ()

src/Idris/Core/ProofState.hs+6−6

@@ -69,7 +69,7 @@ data Tactic = Attack

6969 | CheckIn Raw

7070 | Intro (Maybe Name)

7171 | IntroTy Raw (Maybe Name)

72− | Forall Name Raw

72+ | Forall Name Bool Raw

7373 | LetBind Name Raw Raw

7474 | ExpandLet Name Term

7575 | Rewrite Raw

@@ -569,13 +569,13 @@ intro mn ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =

569569 _ -> lift $ tfail $ CantIntroduce t'

570570intro n ctxt env _ = fail "Can't introduce here."

571571

572−forall :: Name -> Raw -> RunTactic

573−forall n ty ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =

572+forall :: Name -> Bool -> Raw -> RunTactic

573+forall n impl ty ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =

574574 do (tyv, tyt) <- lift $ check ctxt env ty

575575 unify' ctxt env tyt (TType (UVar 0))

576576 unify' ctxt env t (TType (UVar 0))

577− return $ Bind n (Pi False tyv (TType (UVar 0))) (Bind x (Hole t) (P Bound x t))

578−forall n ty ctxt env _ = fail "Can't pi bind here"

577+ return $ Bind n (Pi impl tyv (TType (UVar 0))) (Bind x (Hole t) (P Bound x t))

578+forall n impl ty ctxt env _ = fail "Can't pi bind here"

579579

580580patvar :: Name -> RunTactic

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

@@ -973,7 +973,7 @@ process t h = tactic (Just h) (mktac t)

973973 mktac HNF_Compute = hnf_compute

974974 mktac (Intro n) = intro n

975975 mktac (IntroTy ty n) = introTy ty n

976− mktac (Forall n t) = forall n t

976+ mktac (Forall n i t) = forall n i t

977977 mktac (LetBind n t v) = letbind n t v

978978 mktac (ExpandLet n b) = expandLet n b

979979 mktac (Rewrite t) = rewrite t

src/Idris/DeepSeq.hs+2−2

@@ -94,8 +94,8 @@ instance NFData ArgOpt where

9494 rnf _ = ()

9595

9696instance NFData Plicity where

97− rnf (Imp x1 x2 x3)

98− = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

97+ rnf (Imp x1 x2 x3 x4)

98+ = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

9999 rnf (Exp x1 x2 x3)

100100 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

101101 rnf (Constraint x1 x2)

src/Idris/Delaborate.hs+1−1

@@ -58,7 +58,7 @@ delabTy' ist imps tm fullname mvs = de [] imps tm

5858 de env _ (Bind n (Lam ty) sc)

5959 = PLam un n (de env [] ty) (de ((n,n):env) [] sc)

6060 de env ((PImp { argopts = opts }):is) (Bind n (Pi _ ty _) sc)

61− = PPi (Imp opts Dynamic False) n (de env [] ty) (de ((n,n):env) is sc)

61+ = PPi (Imp opts Dynamic False False) n (de env [] ty) (de ((n,n):env) is sc)

6262 de env (PConstraint _ _ _ _:is) (Bind n (Pi _ ty _) sc)

6363 = PPi constraint n (de env [] ty) (de ((n,n):env) is sc)

6464 de env (PTacImplicit _ _ _ tac _:is) (Bind n (Pi _ ty _) sc)

src/Idris/Elab/Class.hs+5−4

@@ -133,7 +133,8 @@ elabClass info syn_in doc fc constraints tn ps pDocs ds

133133 = do t' <- implicit' info syn allmeths n t

134134 logLvl 5 $ "Method " ++ show n ++ " : " ++ showTmImpls t'

135135 return ( (n, (toExp (map fst ps) Exp t')),

136− (n, (doc, o, (toExp (map fst ps) Imp t'))),

136+ (n, (doc, o, (toExp (map fst ps)

137+ (\ l s p -> Imp l s p False) t'))),

137138 (n, (syn, o, t) ) )

138139 tdecl _ _ = ifail "Not allowed in a class declaration"

139140

@@ -200,7 +201,7 @@ elabClass info syn_in doc fc constraints tn ps pDocs ds

200201 return [PTy doc [] syn fc o m ty',

201202 PClauses fc [Inlinable] m [PClause fc m lhs [] rhs []]]

202203

203− getMArgs (PPi (Imp _ _ _) n ty sc) = IA : getMArgs sc

204+ getMArgs (PPi (Imp _ _ _ _) n ty sc) = IA : getMArgs sc

204205 getMArgs (PPi (Exp _ _ _) n ty sc) = EA : getMArgs sc

205206 getMArgs (PPi (Constraint _ _) n ty sc) = CA : getMArgs sc

206207 getMArgs _ = []

@@ -218,13 +219,13 @@ elabClass info syn_in doc fc constraints tn ps pDocs ds

218219 rhsArgs (CA : xs) ns = pconst (PResolveTC fc) : rhsArgs xs ns

219220 rhsArgs [] _ = []

220221

221− insertConstraint c (PPi p@(Imp _ _ _) n ty sc)

222+ insertConstraint c (PPi p@(Imp _ _ _ _) n ty sc)

222223 = PPi p n ty (insertConstraint c sc)

223224 insertConstraint c sc = PPi (constraint { pstatic = Static })

224225 (sMN 0 "class") c sc

225226

226227 -- make arguments explicit and don't bind class parameters

227− toExp ns e (PPi (Imp l s p) n ty sc)

228+ toExp ns e (PPi (Imp l s p _) n ty sc)

228229 | n `elem` ns = toExp ns e sc

229230 | otherwise = PPi (e l s p) n ty (toExp ns e sc)

230231 toExp ns e (PPi p n ty sc) = PPi p n ty (toExp ns e sc)

src/Idris/Elab/Instance.hs+2−2

@@ -199,7 +199,7 @@ elabInstance info syn what fc cs n ps t expn ds = do

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

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

201201 lamBind i _ sc = sc

202− methArgs i (PPi (Imp _ _ _) n ty sc)

202+ methArgs i (PPi (Imp _ _ _ _) n ty sc)

203203 = PImp 0 True [] n (PRef fc (sMN i "meth")) : methArgs (i+1) sc

204204 methArgs i (PPi (Exp _ _ _) n ty sc)

205205 = PExp 0 [] (sMN 0 "marg") (PRef fc (sMN i "meth")) : methArgs (i+1) sc

@@ -230,7 +230,7 @@ elabInstance info syn what fc cs n ps t expn ds = do

230230 conbind [] x = x

231231

232232 coninsert :: [(Name, PTerm)] -> PTerm -> PTerm

233− coninsert cs (PPi p@(Imp _ _ _) n t sc) = PPi p n t (coninsert cs sc)

233+ coninsert cs (PPi p@(Imp _ _ _ _) n t sc) = PPi p n t (coninsert cs sc)

234234 coninsert cs sc = conbind cs sc

235235

236236 insertDefaults :: IState -> Name ->

src/Idris/Elab/Record.hs+4−4

@@ -130,13 +130,13 @@ elabRecord info syn doc fc tyn ty opts cdoc cn cty_in

130130-- ++ "\n" ++ pshow i v

131131 putIState i)

132132

133− getBoundImpls (PPi (Imp _ _ _) n ty sc) = (n, ty) : getBoundImpls sc

133+ getBoundImpls (PPi (Imp _ _ _ _) n ty sc) = (n, ty) : getBoundImpls sc

134134 getBoundImpls _ = []

135135

136− getImplB k (PPi (Imp l s _) n Placeholder sc)

136+ getImplB k (PPi (Imp l s _ _) n Placeholder sc)

137137 = getImplB k sc

138− getImplB k (PPi (Imp l s p) n ty sc)

139− = getImplB (\x -> k (PPi (Imp l s p) n ty x)) sc

138+ getImplB k (PPi (Imp l s p fa) n ty sc)

139+ = getImplB (\x -> k (PPi (Imp l s p fa) n ty x)) sc

140140 getImplB k (PPi _ n ty sc)

141141 = getImplB k sc

142142 getImplB k _ = k

src/Idris/Elab/Utils.hs+1−1

@@ -56,7 +56,7 @@ inaccessibleImps _ _ _ = []

5656

5757-- Get the list of (index, name) of inaccessible arguments from the type.

5858inaccessibleArgs :: Int -> PTerm -> [(Int, Name)]

59−inaccessibleArgs i (PPi (Imp _ _ _) n Placeholder t)

59+inaccessibleArgs i (PPi (Imp _ _ _ _) n Placeholder t)

6060 = (i,n) : inaccessibleArgs (i+1) t -- unbound implicit

6161inaccessibleArgs i (PPi plicity n ty t)

6262 | InaccessibleArg `elem` pargopts plicity

src/Idris/ElabTerm.hs+27−6

@@ -244,7 +244,8 @@ elab ist info emode opts fn tm

244244 then solveAuto ist fn False a

245245 else return ()) as

246246

247− ct <- insertCoerce ina t

247+ itm <- if not pattern then insertImpLam t else return t

248+ ct <- insertCoerce ina itm

248249 t' <- insertLazy ct

249250 g <- goal

250251 tm <- get_term

@@ -468,17 +469,17 @@ elab ist info emode opts fn tm

468469 elabE (ec { e_inarg = True, e_intype = True }) (Just fc) ty

469470 elabE (ec { e_inarg = True }) (Just fc) sc

470471 solve

471− elab' ina fc (PPi _ n Placeholder sc)

472− = do attack; arg n (sMN 0 "ty")

472+ elab' ina fc (PPi p n Placeholder sc)

473+ = do attack; arg n (is_scoped p) (sMN 0 "ty")

473474 elabE (ina { e_inarg = True, e_intype = True }) fc sc

474475 solve

475− elab' ina fc (PPi _ n ty sc)

476+ elab' ina fc (PPi p n ty sc)

476477 = do attack; tyn <- getNameFrom (sMN 0 "ty")

477478 claim tyn RType

478479 n' <- case n of

479480 MN _ _ -> unique_hole n

480481 _ -> return n

481− forall n' (Var tyn)

482+ forall n' (is_scoped p) (Var tyn)

482483 focus tyn

483484 let ec' = ina { e_inarg = True, e_intype = True }

484485 elabE ec' fc ty

@@ -594,13 +595,15 @@ elab ist info emode opts fn tm

594595-- | isTConName f (tt_ctxt ist) && pattern && not reflection && not inty && not qq

595596-- = lift $ tfail (Msg "Typecase is not allowed")

596597 -- if f is local, just do a simple_app

597− elab' ina _ tm@(PApp fc (PRef _ f) args)

598+ elab' ina _ tm@(PApp fc (PRef _ f) args_in)

598599 | pattern && not reflection && e_nomatching ina

599600 = lift $ tfail $ Msg ("Attempting concrete match on polymorphic argument: " ++ show tm)

600601 | otherwise

601602 = do env <- get_env

602603 ty <- goal

604+ fty <- get_type (Var f)

603605 ctxt <- get_context

606+ let args = insertScopedImps (normalise ctxt env fty) args_in

604607 let unmatchableArgs = if pattern

605608 then getUnmatchable (tt_ctxt ist) f

606609 else []

@@ -1049,6 +1052,24 @@ elab ist info emode opts fn tm

10491052 notImplicitable (PCase _ _ _) = True

10501053 notImplicitable _ = False

10511054

1055+ insertScopedImps (Bind n (Pi True _ _) sc) xs

1056+ = pimp n Placeholder True : insertScopedImps sc xs

1057+ insertScopedImps (Bind n (Pi _ _ _) sc) (x : xs)

1058+ = x : insertScopedImps sc xs

1059+ insertScopedImps _ xs = xs

1060+

1061+ insertImpLam t =

1062+ do ty <- goal

1063+ env <- get_env

1064+ let ty' = normalise (tt_ctxt ist) env ty

1065+ addLam ty' t

1066+ where

1067+ addLam (Bind n (Pi True _ _) sc) t

1068+ = do impn <- unique_hole (sUN "imp")

1069+ t' <- addLam sc t

1070+ return (PLam emptyFC impn Placeholder t')

1071+ addLam _ t = return t

1072+

10521073 insertCoerce ina t@(PCase _ _ _) = return t

10531074 insertCoerce ina t | notImplicitable t = return t

10541075 insertCoerce ina t =

src/Idris/IBC.hs+4−2

@@ -1111,11 +1111,12 @@ instance Binary Static where

11111111instance Binary Plicity where

11121112 put x

11131113 = case x of

1114− Imp x1 x2 x3 ->

1114+ Imp x1 x2 x3 x4 ->

11151115 do putWord8 0

11161116 put x1

11171117 put x2

11181118 put x3

1119+ put x4

11191120 Exp x1 x2 x3 ->

11201121 do putWord8 1

11211122 put x1

@@ -1136,7 +1137,8 @@ instance Binary Plicity where

11361137 0 -> do x1 <- get

11371138 x2 <- get

11381139 x3 <- get

1139− return (Imp x1 x2 x3)

1140+ x4 <- get

1141+ return (Imp x1 x2 x3 x4)

11401142 1 -> do x1 <- get

11411143 x2 <- get

11421144 x3 <- get

src/Idris/ParseExpr.hs+4−2

@@ -883,8 +883,10 @@ pi syn =

883883 symbol "->"

884884 sc <- expr syn

885885 if implicitAllowed syn

886− then return (bindList (PPi (Imp opts st False)) xt sc)

887− else fail "no implicit arguments allowed here"))

886+ then return (bindList (PPi (Imp opts st False False)) xt sc)

887+ -- TODO: TIDY BEFORE COMMITTING!

888+ else return (bindList (PPi (Imp opts st False True)) xt sc)))

889+ -- fail "no implicit arguments allowed here"))

888890 <|> (do x <- opExpr syn

889891 (do symbol "->"

890892 sc <- expr syn