491633b · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Syntax for linear arguments

491633bEdwin Brady10 years ago

src/Idris/AbsSyntaxTree.hs+5

compare with master

unifiedsplit

@@ -186,6 +186,7 @@ ppOptionIst = ppOption . idris_options

186

187data LanguageExt = TypeProviders | ErrorReflection | UniquenessTypes

188 | DSLNotation | ElabReflection | FCReflection

189+ | LinearTypes

189 deriving (Show, Eq, Read, Ord, Generic)

190 deriving (Show, Eq, Read, Ord, Generic)

190

191

191-- | The output mode in use

192-- | The output mode in use

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

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

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

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

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

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

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

1824+ | Rig1 <- rig =

1825+ depth d . bracket p startPrec . group $

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

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

1823 | n `elem` allNamesIn sc || ppopt_impl ppo && uname n || n `elem` docArgs

1828 | n `elem` allNamesIn sc || ppopt_impl ppo && uname n || n `elem` docArgs

1824 || ppopt_pinames ppo && uname n =

1829 || ppopt_pinames ppo && uname n =

1825 depth d . bracket p startPrec . group $

1830 depth d . bracket p startPrec . group $

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

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

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

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

443

444−forall :: Name -> Maybe ImplicitInfo -> Raw -> Elab' aux ()

444+forall :: Name -> RigCount -> Maybe ImplicitInfo -> Raw -> Elab' aux ()

445−forall n i t = processTactic' (Forall n i t)

445+forall n r i t = processTactic' (Forall n r i t)

446

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

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

@@ -845,11 +845,11 @@ dep_app fun arg str =

845

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

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

848−arg :: Name -> Maybe ImplicitInfo -> Name -> Elab' aux ()

848+arg :: Name -> RigCount -> Maybe ImplicitInfo -> Name -> Elab' aux ()

849−arg n i tyhole = do ty <- unique_hole tyhole

849+arg n r i tyhole = do ty <- unique_hole tyhole

850− claim ty RType

850+ claim ty RType

851− movelast ty

851+ movelast ty

852− forall n i (Var ty)

852+ forall n r i (Var ty)

853

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

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

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

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

88 | CheckIn Raw

89 | Intro (Maybe Name)

90 | IntroTy Raw (Maybe Name)

91− | Forall Name (Maybe ImplicitInfo) Raw

91+ | Forall Name RigCount (Maybe ImplicitInfo) Raw

92 | LetBind Name Raw Raw

93 | ExpandLet Name Term

94 | Rewrite Raw

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

684 _ -> lift $ tfail $ CantIntroduce t'

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

686

687−forall :: Name -> Maybe ImplicitInfo -> Raw -> RunTactic

687+forall :: Name -> RigCount -> Maybe ImplicitInfo -> Raw -> RunTactic

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

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

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

690 unify' ctxt env (tyt, Nothing) (TType (UVar [] 0), Nothing)

691 unify' ctxt env (t, Nothing) (TType (UVar [] 0), Nothing)

692− return $ Bind n (Pi RigW impl tyv (TType (UVar [] 0))) (Bind x (Hole t) (P Bound x t))

692+ return $ Bind n (Pi rig impl tyv (TType (UVar [] 0))) (Bind x (Hole t) (P Bound x t))

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

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

694

695patvar :: Name -> RunTactic

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

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

1149 mktac WHNF_ComputeArgs = whnf_compute_args

1150 mktac (Intro n) = intro n

1151 mktac (IntroTy ty n) = introTy ty n

1152− mktac (Forall n i t) = forall n i t

1152+ mktac (Forall n r i t) = forall n r i t

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

1154 mktac (ExpandLet n b) = expandLet n b

1155 mktac (Rewrite t) = rewrite t

src/Idris/Elab/Term.hs+14−3

@@ -705,7 +705,13 @@ elab ist info emode opts fn tm

705 solve

706 highlightSource nfc (AnnBoundName n False)

707 elab' ina fc (PPi p n nfc Placeholder sc)

708+ = do attack;

709+ case pcount p of

710+ RigW -> return ()

711+ _ -> unless (LinearTypes `elem` idris_language_extensions ist

712+ || e_qq ina) $

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

708− = do attack; arg n (is_scoped p) (sMN 0 "phTy")

714+ arg n (pcount p) (is_scoped p) (sMN 0 "phTy")

709 addAutoBind p n

715 addAutoBind p n

710 addPSname n -- okay for proof search

716 addPSname n -- okay for proof search

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

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

@@ -717,7 +723,12 @@ elab ist info emode opts fn tm

717 n' <- case n of

723 n' <- case n of

718 MN _ _ -> unique_hole n

724 MN _ _ -> unique_hole n

719 _ -> return n

725 _ -> return n

726+ case pcount p of

727+ RigW -> return ()

728+ _ -> unless (LinearTypes `elem` idris_language_extensions ist

729+ || e_qq ina) $

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

720− forall n' (is_scoped p) (Var tyn)

731+ forall n' (pcount p) (is_scoped p) (Var tyn)

721 addAutoBind p n'

732 addAutoBind p n'

722 addPSname n' -- okay for proof search

733 addPSname n' -- okay for proof search

723 focus tyn

734 focus tyn

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

2250 = do ~[n, ty] <- tacTmArgs 2 tac args

2261 = do ~[n, ty] <- tacTmArgs 2 tac args

2251 n' <- reifyTTName n

2262 n' <- reifyTTName n

2252 ty' <- reifyRaw ty

2263 ty' <- reifyRaw ty

2253− forall n' Nothing ty'

2264+ forall n' RigW Nothing ty'

2254 returnUnit

2265 returnUnit

2255 | n == tacN "Prim__PatVar"

2266 | n == tacN "Prim__PatVar"

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

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

src/Idris/Parser.hs+5−4

@@ -763,7 +763,7 @@ Params ::=

763params :: SyntaxInfo -> IdrisParser [PDecl]

764params syn =

765 do reservedHL "parameters"; lchar '('; ns <- typeDeclList syn; lchar ')'

766− let ns' = [(n, ty) | (n, _, ty) <- ns]

766+ let ns' = [(n, ty) | (_, n, _, ty) <- ns]

767 openBlock

768 let pvars = syn_params syn

769 ds <- many (decl syn { syn_params = pvars ++ ns' })

@@ -903,7 +903,7 @@ interface_ syn = do (doc, argDocs, acc)

903 return (doc, argDocs, acc))

904 fc <- getFC

905 cons <- constraintList syn

906− let cons' = [(c, ty) | (c, _, ty) <- cons]

906+ let cons' = [(c, ty) | (_, c, _, ty) <- cons]

907 (n_in, nfc) <- fnName

908 let n = expandNS syn n_in

909 cs <- many carg

@@ -953,11 +953,11 @@ implementation kwopt syn

953 fc <- getFC

954 en <- optional implementationName

955 cs <- constraintList syn

956− let cs' = [(c, ty) | (c, _, ty) <- cs]

956+ let cs' = [(c, ty) | (_, c, _, ty) <- cs]

957 (cn, cnfc) <- fnName

958 args <- many (simpleExpr syn)

959 let sc = PApp fc (PRef cnfc [cnfc] cn) (map pexp args)

960− let t = bindList (PPi constraint) cs sc

960+ let t = bindList (\r -> PPi constraint { pcount = r }) cs sc

961 pnames <- implementationUsing

962 ds <- implementationBlock syn

963 return [PImplementation doc argDocs syn fc cs' pnames acc opts cn cnfc args [] t en ds]

@@ -1430,6 +1430,7 @@ pLangExt :: IdrisParser LanguageExt

1430pLangExt = (reserved "TypeProviders" >> return TypeProviders)

1431 <|> (reserved "ErrorReflection" >> return ErrorReflection)

1432 <|> (reserved "UniquenessTypes" >> return UniquenessTypes)

1433+ <|> (reserved "LinearTypes" >> return LinearTypes)

1433 <|> (reserved "DSLNotation" >> return DSLNotation)

1434 <|> (reserved "DSLNotation" >> return DSLNotation)

1434 <|> (reserved "ElabReflection" >> return ElabReflection)

1435 <|> (reserved "ElabReflection" >> return ElabReflection)

1435 <|> (reserved "FirstClassReflection" >> return FCReflection)

1436 <|> (reserved "FirstClassReflection" >> return FCReflection)

src/Idris/Parser/Expr.hs+23−21

@@ -914,7 +914,7 @@ TypeExpr ::= ConstraintList? Expr;

914typeExpr :: SyntaxInfo -> IdrisParser PTerm

915typeExpr syn = do cs <- if implicitAllowed syn then constraintList syn else return []

916 sc <- expr (allowConstr syn)

917− return (bindList (PPi constraint) cs sc)

917+ return (bindList (\r -> PPi (constraint { pcount = r })) cs sc)

918 <?> "type signature"

919

920{- | Parses a lambda expression

@@ -941,7 +941,7 @@ lambda syn = do lchar '\\' <?> "lambda expression"

941 ((do xt <- try $ tyOptDeclList (disallowImp syn)

942 fc <- getFC

943 sc <- lambdaTail

944− return (bindList (PLam fc) xt sc))

944+ return (bindList (\r -> PLam fc) xt sc))

945 <|>

946 (do ps <- sepBy (do fc <- getFC

947 e <- simpleExpr (disallowImp (syn { inPattern = True }))

@@ -1078,7 +1078,7 @@ explicitPi opts st syn

1078 = do xt <- try (lchar '(' *> typeDeclList syn <* lchar ')')

1079 binder <- bindsymbol opts st syn

1080 sc <- expr (allowConstr syn)

1081− return (bindList (PPi binder) xt sc)

1081+ return (bindList (\r -> PPi (binder { pcount = r })) xt sc)

1082

1083autoImplicit opts st syn

1084 = do kw <- reservedFC "auto"

@@ -1088,8 +1088,8 @@ autoImplicit opts st syn

1088 symbol "->"

1089 sc <- expr (allowConstr syn)

1090 highlightP kw AnnKeyword

1091− return (bindList (PPi

1091+ return (bindList (\r -> PPi

1092− (TacImp [] Dynamic (PTactics [ProofSearch True True 100 Nothing [] []]) RigW)) xt sc)

1092+ (TacImp [] Dynamic (PTactics [ProofSearch True True 100 Nothing [] []]) r)) xt sc)

1093

1094defaultImplicit opts st syn = do

1095 kw <- reservedFC "default"

@@ -1102,7 +1102,7 @@ defaultImplicit opts st syn = do

1102 symbol "->"

1103 sc <- expr (allowConstr syn)

1104 highlightP kw AnnKeyword

1105− return (bindList (PPi (TacImp [] Dynamic script RigW)) xt sc)

1105+ return (bindList (\r -> PPi (TacImp [] Dynamic script r)) xt sc)

1106

1107normalImplicit opts st syn = do

1108 xt <- typeDeclList syn <* lchar '}'

@@ -1115,15 +1115,15 @@ normalImplicit opts st syn = do

1115 constraint)

1116 else (Imp opts st False (Just (Impl False False False)) True RigW,

1117 Imp opts st False (Just (Impl True False False)) True RigW)

1118− return (bindList (PPi im) xt

1118+ return (bindList (\r -> PPi (im { pcount = r })) xt

1119− (bindList (PPi cl) cs sc))

1119+ (bindList (\r -> PPi (cl { pcount = r })) cs sc))

1120

1121constraintPi opts st syn =

1122 do cs <- constraintList1 syn

1123 sc <- expr syn

1124 if implicitAllowed syn

1125− then return (bindList (PPi constraint) cs sc)

1125+ then return (bindList (\r -> PPi constraint { pcount = r }) cs sc)

1126− else return (bindList (PPi (Imp opts st False (Just (Impl True False False)) True RigW))

1126+ else return (bindList (\r -> PPi (Imp opts st False (Just (Impl True False False)) True r))

1127 cs sc)

1128

1129implicitPi opts st syn =

@@ -1181,11 +1181,11 @@ ConstraintList ::=

1181 ;

1182@

1183-}

1184−constraintList :: SyntaxInfo -> IdrisParser [(Name, FC, PTerm)]

1184+constraintList :: SyntaxInfo -> IdrisParser [(RigCount, Name, FC, PTerm)]

1185constraintList syn = try (constraintList1 syn)

1186 <|> return []

1187

1188−constraintList1 :: SyntaxInfo -> IdrisParser [(Name, FC, PTerm)]

1188+constraintList1 :: SyntaxInfo -> IdrisParser [(RigCount, Name, FC, PTerm)]

1189constraintList1 syn = try (do lchar '('

1190 tys <- sepBy1 nexpr (lchar ',')

1191 lchar ')'

@@ -1193,13 +1193,13 @@ constraintList1 syn = try (do lchar '('

1193 return tys)

1194 <|> try (do t <- opExpr (disallowImp syn)

1195 reservedOp "=>"

1196− return [(defname, NoFC, t)])

1196+ return [(RigW, defname, NoFC, t)])

1197 <?> "type constraint list"

1198 where nexpr = try (do (n, fc) <- name; lchar ':'

1199 e <- expr (disallowImp syn)

1200− return (n, fc, e))

1200+ return (RigW, n, fc, e))

1201 <|> do e <- expr (disallowImp syn)

1202− return (defname, NoFC, e)

1202+ return (RigW, defname, NoFC, e)

1203 defname = sMN 0 "constraint"

1204

1205{- | Parses a type declaration list

@@ -1217,16 +1217,18 @@ FunctionSignatureList ::=

1217 ;

1218@

1219-}

1220−typeDeclList :: SyntaxInfo -> IdrisParser [(Name, FC, PTerm)]

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

1221−typeDeclList syn = try (sepBy1 (do (x, xfc) <- fnName

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

1222+ return Rig1)

1223+ (x, xfc) <- fnName

1222 lchar ':'

1224 lchar ':'

1223 t <- typeExpr (disallowImp syn)

1225 t <- typeExpr (disallowImp syn)

1224− return (x, xfc, t))

1226+ return (rig, x, xfc, t))

1225 (lchar ','))

1227 (lchar ','))

1226 <|> do ns <- sepBy1 name (lchar ',')

1228 <|> do ns <- sepBy1 name (lchar ',')

1227 lchar ':'

1229 lchar ':'

1228 t <- typeExpr (disallowImp syn)

1230 t <- typeExpr (disallowImp syn)

1229− return (map (\(x, xfc) -> (x, xfc, t)) ns)

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

1230 <?> "type declaration list"

1232 <?> "type declaration list"

1231

1233

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

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

@@ -1241,11 +1243,11 @@ TypeOptDeclList ::=

1241NameOrPlaceHolder ::= Name | '_';

1243NameOrPlaceHolder ::= Name | '_';

1242@

1244@

1243-}

1245-}

1244−tyOptDeclList :: SyntaxInfo -> IdrisParser [(Name, FC, PTerm)]

1246+tyOptDeclList :: SyntaxInfo -> IdrisParser [(RigCount, Name, FC, PTerm)]

1245tyOptDeclList syn = sepBy1 (do (x, fc) <- nameOrPlaceholder

1247tyOptDeclList syn = sepBy1 (do (x, fc) <- nameOrPlaceholder

1246 t <- option Placeholder (do lchar ':'

1248 t <- option Placeholder (do lchar ':'

1247 expr syn)

1249 expr syn)

1248− return (x, fc, t))

1250+ return (RigW, x, fc, t))

1249 (lchar ',')

1251 (lchar ',')

1250 <?> "type declaration list"

1252 <?> "type declaration list"

1251 where nameOrPlaceholder :: IdrisParser (Name, FC)

1253 where nameOrPlaceholder :: IdrisParser (Name, FC)

src/Idris/Parser/Helpers.hs+3−3

@@ -455,9 +455,9 @@ getFC = do s <- position

455

456{-* Syntax helpers-}

457-- | Bind constraints to term

458−bindList :: (Name -> FC -> PTerm -> PTerm -> PTerm) -> [(Name, FC, PTerm)] -> PTerm -> PTerm

458+bindList :: (RigCount -> Name -> FC -> PTerm -> PTerm -> PTerm) -> [(RigCount, Name, FC, PTerm)] -> PTerm -> PTerm

459−bindList b [] sc = sc

459+bindList b [] sc = sc

460−bindList b ((n, fc, t):bs) sc = b n fc t (bindList b bs sc)

460+bindList b ((r, n, fc, t):bs) sc = b r n fc t (bindList b bs sc)

461

462{- | @commaSeparated p@ parses one or more occurences of `p`,

463 separated by commas and optional whitespace. -}