Merge pull request #2906 from ahmadsalim/feature/uniformstaticanotation
Changed the '[static]' annotation to '%static', for uniformity with the rest of the language.
commitfaf0b57a826c276c22e2ffd682b293c10110b632
authorJan de Muijnck-Hughes <jfdm@users.noreply.github.com>
dateThu 28 Jan 2016, 13:33 (11 years ago)
parent92882c38fb4f7f
docs/reference/language-features.rst+1−1
@@ -46,7 +46,7 @@ Core Language Features
4646 using the ``UniqueType`` universe.
4747- `Partial
4848 evaluation <https://github.com/idris-lang/Idris-dev/wiki/Static-Arguments-and-Partial-Evaluation>`__
49− by ``[static]`` argument annotations.
49+ by ``%static`` argument annotations.
5050- Error message reflection
5151- Eliminators
5252- Label types ``'name``
samples/tutorial/interp.idr+1−1
@@ -33,7 +33,7 @@ using (G : Vect n Ty)
3333 Expr G c
3434 If : Expr G TyBool -> Lazy (Expr G a) -> Lazy (Expr G a) -> Expr G a
3535
36− interp : Env G -> [static] (e : Expr G t) -> interpTy t
36+ interp : Env G -> %static (e : Expr G t) -> interpTy t
3737 interp env (Var i) = lookup i env
3838 interp env (Val x) = x
3939 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
17381738
17391739 st =
17401740 case s of
1741− Static -> text "[static]" <> space
1741+ Static -> text "%static" <> space
17421742 _ -> empty
17431743 prettySe d p bnd (PPi (Imp l s _ fa) n _ ty sc)
17441744 | ppopt_impl ppo =
@@ -1749,7 +1749,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd
17491749 where
17501750 st =
17511751 case s of
1752− Static -> text "[static]" <> space
1752+ Static -> text "%static" <> space
17531753 _ -> empty
17541754 prettySe d p bnd (PPi (Constraint _ _) n _ ty sc) =
17551755 depth d . bracket p startPrec $
src/Idris/ParseExpr.hs+1−1
@@ -1389,7 +1389,7 @@ Static ::=
13891389@
13901390-}
13911391static :: IdrisParser Static
1392−static = do reserved "[static]"; return Static
1392+static = do reserved "%static"; return Static
13931393 <|> return Dynamic
13941394 <?> "static modifier"
13951395
test/dsl001/test001.idr+1−1
@@ -45,7 +45,7 @@ using (G : Vect n Ty)
4545 index_next = Pop
4646
4747 total
48− interp : Env G -> [static] (e : Expr G t) -> interpTy t
48+ interp : Env G -> %static (e : Expr G t) -> interpTy t
4949 interp env (Var i) = lookup i env
5050 interp env (Val x) = x
5151 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)
122122 ioret : a -> IO a
123123 ioret = return
124124
125− interp : Env gam -> [static] (e : Res gam gam' t) ->
125+ interp : Env gam -> %static (e : Res gam gam' t) ->
126126 (Env gam' -> interpTy t -> IO u) -> IO u
127127
128128 interp env (Let val scope) k