2f3c9a5 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Add RigCount to pattern bindings

After elaborating LHS, mark pattern bindings which are used in a linear position ready for elaboration on the RHS.

commit2f3c9a5b76b1b761ea3466849a5331a13870acbc authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSun 18 Dec 2016, 15:19 (10 years ago) parent491633b

7 files changed+63−22

compare with master

unifiedsplit

src/Idris/AbsSyntaxTree.hs+9−1 src/Idris/Core/Elaborate.hs+2−2 src/Idris/Core/ProofState.hs+6−6 src/Idris/Elab/Clause.hs+1−1 src/Idris/Elab/Term.hs+13−8 src/Idris/Elab/Utils.hs+28−2 src/Idris/Parser/Expr.hs+4−2

src/Idris/AbsSyntaxTree.hs+9−1

@@ -1821,6 +1821,10 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd

18211821 kwd "let" <+> (group . align . hang 2 $ prettyBindingOf n False <+> text "=" <$> prettySe (decD d) startPrec bnd v) </>

18221822 kwd "in" <+> (group . align . hang 2 $ prettySe (decD d) startPrec ((n, False):bnd) sc)

18231823 prettySe d p bnd (PPi (Exp l s _ rig) n _ ty sc)

1824+ | Rig0 <- rig =

1825+ depth d . bracket p startPrec . group $

1826+ enclose lparen rparen (group . align $ text "0" <+> prettyBindingOf n False <+> colon <+> prettySe (decD d) startPrec bnd ty) <+>

1827+ st <> text "->" <$> prettySe (decD d) startPrec ((n, False):bnd) sc

18241828 | Rig1 <- rig =

18251829 depth d . bracket p startPrec . group $

18261830 enclose lparen rparen (group . align $ text "1" <+> prettyBindingOf n False <+> colon <+> prettySe (decD d) startPrec bnd ty) <+>

@@ -1847,10 +1851,14 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd

18471851 prettySe d p bnd (PPi (Imp l s _ fa _ rig) n _ ty sc)

18481852 | ppopt_impl ppo =

18491853 depth d . bracket p startPrec $

1850− lbrace <> prettyBindingOf n True <+> colon <+> prettySe (decD d) startPrec bnd ty <> rbrace <+>

1854+ lbrace <> showRig rig n <+> colon <+> prettySe (decD d) startPrec bnd ty <> rbrace <+>

18511855 st <> text "->" </> prettySe (decD d) startPrec ((n, True):bnd) sc

18521856 | otherwise = depth d $ prettySe (decD d) startPrec ((n, True):bnd) sc

18531857 where

1858+ showRig Rig0 n = text "0" <+> prettyBindingOf n True

1859+ showRig Rig1 n = text "1" <+> prettyBindingOf n True

1860+ showRig _ n = prettyBindingOf n True

1861+

18541862 st =

18551863 case s of

18561864 Static -> text "%static" <> space

src/Idris/Core/Elaborate.hs+2−2

@@ -484,8 +484,8 @@ patvar' n = do env <- get_env

484484 if (n `elem` map fstEnv env) then do apply (Var n) [] ; solve

485485 else processTactic' (PatVar n)

486486

487−patbind :: Name -> Elab' aux ()

488−patbind n = processTactic' (PatBind n)

487+patbind :: Name -> RigCount -> Elab' aux ()

488+patbind n r = processTactic' (PatBind n r)

489489

490490focus :: Name -> Elab' aux ()

491491focus n = processTactic' (Focus n)

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

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

9696 | CaseTac Raw

9797 | Equiv Raw

9898 | PatVar Name

99− | PatBind Name

99+ | PatBind Name RigCount

100100 | Focus Name

101101 | Defer [Name] Name

102102 | DeferType Name Raw [Name]

@@ -823,16 +823,16 @@ equiv tm ctxt env (Bind x (Hole t) sc) =

823823 return $ Bind x (Hole tmv) sc

824824equiv tm ctxt env _ = fail "Can't equiv here"

825825

826−patbind :: Name -> RunTactic

827−patbind n ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =

826+patbind :: Name -> RigCount -> RunTactic

827+patbind n rig ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =

828828 do let t' = case t of

829829 x@(Bind y (PVTy s) t) -> x

830830 _ -> normalise ctxt env t

831831 case t' of

832832 Bind y (PVTy s) t -> let t' = updsubst y (P Bound n s) t in

833− return $ Bind n (PVar RigW s) (Bind x (Hole t') (P Bound x t'))

833+ return $ Bind n (PVar rig s) (Bind x (Hole t') (P Bound x t'))

834834 _ -> fail "Nothing to pattern bind"

835−patbind n ctxt env _ = fail "Can't pattern bind here"

835+patbind n _ ctxt env _ = fail "Can't pattern bind here"

836836

837837compute :: RunTactic

838838compute ctxt env (Bind x (Hole ty) sc) =

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

11571157 mktac (CaseTac t) = casetac t False

11581158 mktac (Equiv t) = equiv t

11591159 mktac (PatVar n) = patvar n

1160− mktac (PatBind n) = patbind n

1160+ mktac (PatBind n rig) = patbind n rig

11611161 mktac (CheckIn r) = check_in r

11621162 mktac (EvalIn r) = eval_in r

11631163 mktac (Focus n) = focus n

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

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

848848

849849 when inf $ addTyInfConstraints fc (map (\(x,y,_,_,_,_,_) -> (x,y)) probs)

850850

851− logElab 5 "DONE CHECK"

851+ logElab 3 "DONE CHECK"

852852 logElab 3 $ "---> " ++ show rhsElab

853853 ctxt <- getContext

854854

src/Idris/Elab/Term.hs+13−8

@@ -251,13 +251,18 @@ elab ist info emode opts fn tm

251251 est <- getAux

252252 sequence_ (get_delayed_elab est)

253253 end_unify

254+ when (pattern || intransform) $

255+ -- convert remaining holes to pattern vars

256+ do unify_all

257+ matchProblems False -- only the ones we matched earlier

258+ unifyProblems

259+ mkPat

260+ update_term liftPats

254261 ptm <- get_term

255− when (pattern || intransform) -- convert remaining holes to pattern vars

256− (do unify_all

257− matchProblems False -- only the ones we matched earlier

258− unifyProblems

259− mkPat

260− update_term liftPats)

262+ when pattern $

263+ -- Look for Rig1 (linear) pattern bindings

264+ do let pnms = findLinear ist [] ptm

265+ update_term (setLinear pnms)

261266 where

262267 pattern = emode == ELHS || emode == EImpossible

263268 eimpossible = emode == EImpossible

@@ -710,7 +715,7 @@ elab ist info emode opts fn tm

710715 RigW -> return ()

711716 _ -> unless (LinearTypes `elem` idris_language_extensions ist

712717 || e_qq ina) $

713− lift $ tfail $ At nfc (Msg "You must turn on the LinearTypes extension to use a linear argument")

718+ lift $ tfail $ At nfc (Msg "You must turn on the LinearTypes extension to use a count")

714719 arg n (pcount p) (is_scoped p) (sMN 0 "phTy")

715720 addAutoBind p n

716721 addPSname n -- okay for proof search

@@ -2271,7 +2276,7 @@ runElabAction info ist fc env tm ns = do tm' <- eval tm

22712276 | n == tacN "Prim__PatBind"

22722277 = do ~[n] <- tacTmArgs 1 tac args

22732278 n' <- reifyTTName n

2274− patbind n'

2279+ patbind n' RigW

22752280 returnUnit

22762281 | n == tacN "Prim__LetBind"

22772282 = do ~[n, ty, tm] <- tacTmArgs 3 tac args

src/Idris/Elab/Utils.hs+28−2

@@ -11,6 +11,7 @@ module Idris.Elab.Utils where

1111import Idris.AbsSyntax

1212import Idris.Core.Elaborate hiding (Tactic(..))

1313import Idris.Core.Evaluate

14+import Idris.Core.WHNF

1415import Idris.Core.TT

1516import Idris.Core.Typecheck

1617import Idris.DeepSeq

@@ -184,8 +185,8 @@ decorateid decorate (PClauses f o n cs)

184185

185186-- if 't' is an interface application, assume its arguments are injective

186187pbinds :: IState -> Term -> ElabD ()

187−pbinds i (Bind n (PVar _ t) sc)

188− = do attack; patbind n

188+pbinds i (Bind n (PVar rig t) sc)

189+ = do attack; patbind n rig

189190 env <- get_env

190191 case unApply (normalise (tt_ctxt i) env t) of

191192 (P _ c _, args) -> case lookupCtxt c (idris_interfaces i) of

@@ -571,3 +572,28 @@ hasEmptyPat :: Context -> Ctxt TypeInfo -> Term -> Bool

571572hasEmptyPat ctxt tyctxt (Bind n (PVar _ ty) sc)

572573 = isEmpty ctxt tyctxt ty || hasEmptyPat ctxt tyctxt sc

573574hasEmptyPat ctxt tyctxt _ = False

575+

576+-- Find names which are applied to a function in a Rig1 position

577+findLinear :: IState -> [Name] -> Term -> [Name]

578+findLinear ist env tm | (P _ f _, args) <- unApply tm,

579+ f `notElem` env,

580+ Just ty_in <- lookupTyExact f (tt_ctxt ist)

581+ = let ty = whnfArgs (tt_ctxt ist) [] ty_in in

582+ nub $ concatMap (findLinear ist env) args ++ findLinArg ty args

583+ where

584+ findLinArg (Bind n (Pi c _ _ _) sc) (P _ a _ : as)

585+ | Rig1 <- c = a : findLinArg sc as

586+ findLinArg (Bind n (Pi _ _ _ _) sc) (a : as) = findLinArg sc as

587+ findLinArg _ _ = []

588+findLinear ist env (App _ f a)

589+ = nub $ findLinear ist env f ++ findLinear ist env a

590+findLinear ist env (Bind n b sc) = findLinear ist (n : env) sc

591+findLinear ist _ _ = []

592+

593+setLinear :: [Name] -> Term -> Term

594+setLinear ns (Bind n b@(PVar r t) sc)

595+ | n `elem` ns = Bind n (PVar Rig1 t) (setLinear ns sc)

596+ | otherwise = Bind n b (setLinear ns sc)

597+setLinear ns tm = tm

598+

599+

src/Idris/Parser/Expr.hs+4−2

@@ -1218,8 +1218,7 @@ FunctionSignatureList ::=

12181218@

12191219-}

12201220typeDeclList :: SyntaxInfo -> IdrisParser [(RigCount, Name, FC, PTerm)]

1221−typeDeclList syn = try (sepBy1 (do rig <- option RigW (do lchar '1'

1222− return Rig1)

1221+typeDeclList syn = try (sepBy1 (do rig <- option RigW rigCount

12231222 (x, xfc) <- fnName

12241223 lchar ':'

12251224 t <- typeExpr (disallowImp syn)

@@ -1230,6 +1229,9 @@ typeDeclList syn = try (sepBy1 (do rig <- option RigW (do lchar '1'

12301229 t <- typeExpr (disallowImp syn)

12311230 return (map (\(x, xfc) -> (RigW, x, xfc, t)) ns)

12321231 <?> "type declaration list"

1232+ where

1233+ rigCount = do lchar '1'; return Rig1

1234+ <|> do lchar '0'; return Rig0

12331235

12341236{- | Parses a type declaration list with optional parameters

12351237@