git.iko.soy/Idris-dev
on master help sign in
Changed the '[static]' annotation to '%static', for uniformity with the rest of the language.
8fb4f7fAhmad Salim Al-Sibahi
docs/reference/language-features.rst+1−1
compare with master
unifiedsplit
@@ -46,7 +46,7 @@ Core Language Features
46 using the ``UniqueType`` universe.
46 using the ``UniqueType`` universe.
47- `Partial
47- `Partial
48 evaluation <https://github.com/idris-lang/Idris-dev/wiki/Static-Arguments-and-Partial-Evaluation>`__
48 evaluation <https://github.com/idris-lang/Idris-dev/wiki/Static-Arguments-and-Partial-Evaluation>`__
49− by ``[static]`` argument annotations.
49+ by ``%static`` argument annotations.
50- Error message reflection
50- Error message reflection
51- Eliminators
51- Eliminators
52- Label types ``'name``
52- Label types ``'name``
samples/tutorial/interp.idr+1−1
@@ -33,7 +33,7 @@ using (G : Vect n Ty)
33 Expr G c
33 Expr G c
34 If : Expr G TyBool -> Lazy (Expr G a) -> Lazy (Expr G a) -> Expr G a
34 If : Expr G TyBool -> Lazy (Expr G a) -> Lazy (Expr G a) -> Expr G a
35
35
36− interp : Env G -> [static] (e : Expr G t) -> interpTy t
36+ interp : Env G -> %static (e : Expr G t) -> interpTy t
37 interp env (Var i) = lookup i env
37 interp env (Var i) = lookup i env
38 interp env (Val x) = x
38 interp env (Val x) = x
39 interp env (Lam sc) = \x => interp (x :: env) sc
39 interp env (Lam sc) = \x => interp (x :: env) sc
src/Idris/AbsSyntaxTree.hs+2−2
@@ -1738,7 +1738,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd
1738
1738
1739 st =
1739 st =
1740 case s of
1740 case s of
1741− Static -> text "[static]" <> space
1741+ Static -> text "%static" <> space
1742 _ -> empty
1742 _ -> empty
1743 prettySe d p bnd (PPi (Imp l s _ fa) n _ ty sc)
1743 prettySe d p bnd (PPi (Imp l s _ fa) n _ ty sc)
1744 | ppopt_impl ppo =
1744 | ppopt_impl ppo =
@@ -1749,7 +1749,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd
1749 where
1749 where
1750 st =
1750 st =
1751 case s of
1751 case s of
1752− Static -> text "[static]" <> space
1752+ Static -> text "%static" <> space
1753 _ -> empty
1753 _ -> empty
1754 prettySe d p bnd (PPi (Constraint _ _) n _ ty sc) =
1754 prettySe d p bnd (PPi (Constraint _ _) n _ ty sc) =
1755 depth d . bracket p startPrec $
1755 depth d . bracket p startPrec $
src/Idris/ParseExpr.hs+1−1
@@ -1389,7 +1389,7 @@ Static ::=
1389@
1389@
1390-}
1390-}
1391static :: IdrisParser Static
1391static :: IdrisParser Static
1392−static = do reserved "[static]"; return Static
1392+static = do reserved "%static"; return Static
1393 <|> return Dynamic
1393 <|> return Dynamic
1394 <?> "static modifier"
1394 <?> "static modifier"
1395
1395
test/dsl001/test001.idr+1−1
@@ -45,7 +45,7 @@ using (G : Vect n Ty)
45 index_next = Pop
45 index_next = Pop
46
46
47 total
47 total
48− interp : Env G -> [static] (e : Expr G t) -> interpTy t
48+ interp : Env G -> %static (e : Expr G t) -> interpTy t
49 interp env (Var i) = lookup i env
49 interp env (Var i) = lookup i env
50 interp env (Val x) = x
50 interp env (Val x) = x
51 interp env (Lam sc) = \x => interp (x :: env) sc
51 interp env (Lam sc) = \x => interp (x :: env) sc
test/dsl002/Resimp.idr+1−1
@@ -122,7 +122,7 @@ using (i: Fin n, gam : Vect n Ty, gam' : Vect n Ty, gam'' : Vect n Ty)
122 ioret : a -> IO a
122 ioret : a -> IO a
123 ioret = return
123 ioret = return
124
124
125− interp : Env gam -> [static] (e : Res gam gam' t) ->
125+ interp : Env gam -> %static (e : Res gam gam' t) ->
126 (Env gam' -> interpTy t -> IO u) -> IO u
126 (Env gam' -> interpTy t -> IO u) -> IO u
127
127
128 interp env (Let val scope) k
128 interp env (Let val scope) k