idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-25 04:33:45 +03:00
Code Issues Projects Releases Wiki Activity

Add syntax for quoting names

Browse Source 
`{{ n }} gives a value of type Name. No name resolution is attempted (so
no namespaces added etc)
This commit is contained in:
Edwin Brady 2020-06-01 13:39:18 +01:00
parent d0021f7e48
commit e2aabd6602
16 changed files with 79 additions and 18 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
CHANGELOG.md
View File

@ -9,6 +9,9 @@ Language changes:
+ Casts to `Int` (except `Bits64` which might not fit), `Integer` and `String`
+ Passed to C FFI as `unsigned`
+ Primitives added in `Data.Buffer`
* Elaborator reflection and quoting terms
+ Requires extension `%language ElabReflection`
+ API defined in `Language.Reflection`
Changes since Idris 2 v0.1.0
----------------------------

8
libs/base/Language/Reflection/TT.idr
View File

@ -24,6 +24,10 @@ public export
data Constant
= I Int
| BI Integer
| B8 Int
| B16 Int
| B32 Int
| B64 Integer
| Str String
| Ch Char
| Db Double
@ -31,6 +35,10 @@ data Constant
| IntType
| IntegerType
| Bits8Type
| Bits16Type
| Bits32Type
| Bits64Type
| StringType
| CharType
| DoubleType

1
libs/base/Language/Reflection/TTImp.idr
View File

@ -61,6 +61,7 @@ mutual
-- Quasiquotation
IQuote : FC -> TTImp -> TTImp
IQuoteName : FC -> Name -> TTImp
IQuoteDecl : FC -> TTImp -> TTImp
IUnquote : FC -> TTImp -> TTImp

2
src/Core/Binary.idr
View File

@ -30,7 +30,7 @@ import Data.Buffer
-- TTC files can only be compatible if the version number is the same
export
ttcVersion : Int
ttcVersion = 32
ttcVersion = 33
export
checkTTCVersion : String -> Int -> Int -> Core ()

2
src/Idris/Desugar.idr
View File

@ -248,6 +248,8 @@ mutual
desugarB side ps (PPrimVal fc x) = pure $ IPrimVal fc x
desugarB side ps (PQuote fc tm)
= pure $ IQuote fc !(desugarB side ps tm)
desugarB side ps (PQuoteName fc n)
= pure $ IQuoteName fc n
desugarB side ps (PQuoteDecl fc x)
= do [x'] <- desugarDecl ps x
| _ => throw (GenericMsg fc "Can't quote this declaration")

6
src/Idris/Parser.idr
View File

@ -379,6 +379,12 @@ mutual
symbol ")"
end <- location
pure (PQuote (MkFC fname start end) e)
<|> do start <- location
symbol "`{{"
n <- name
symbol "}}"
end <- location
pure (PQuoteName (MkFC fname start end) n)
<|> do start <- location
symbol "~"
e <- simpleExpr fname indents

1
src/Idris/Resugar.idr
View File

@ -240,6 +240,7 @@ mutual
toPTerm p (IDelay fc tm) = pure (PDelay fc !(toPTerm argPrec tm))
toPTerm p (IForce fc tm) = pure (PForce fc !(toPTerm argPrec tm))
toPTerm p (IQuote fc tm) = pure (PQuote fc !(toPTerm argPrec tm))
toPTerm p (IQuoteName fc n) = pure (PQuoteName fc n)
toPTerm p (IQuoteDecl fc d)
= do md <- toPDecl d
case md of

3
src/Idris/Syntax.idr
View File

@ -53,6 +53,7 @@ mutual
PSearch : FC -> (depth : Nat) -> PTerm
PPrimVal : FC -> Constant -> PTerm
PQuote : FC -> PTerm -> PTerm
PQuoteName : FC -> Name -> PTerm
PQuoteDecl : FC -> PDecl -> PTerm
PUnquote : FC -> PTerm -> PTerm
PRunElab : FC -> PTerm -> PTerm
@ -439,6 +440,7 @@ mutual
= showPrec d f ++ " {" ++ showPrec d n ++ " = " ++ showPrec d a ++ "}"
showPrec _ (PSearch _ _) = "%search"
showPrec d (PQuote _ tm) = "`(" ++ showPrec d tm ++ ")"
showPrec d (PQuoteName _ n) = "`{{" ++ showPrec d n ++ "}}"
showPrec d (PQuoteDecl _ tm) = "`( <<declaration>> )"
showPrec d (PUnquote _ tm) = "~(" ++ showPrec d tm ++ ")"
showPrec d (PRunElab _ tm) = "%runElab " ++ showPrec d tm
@ -689,6 +691,7 @@ mapPTermM f = goPTerm where
goPTerm (PQuote fc x) =
PQuote fc <$> goPTerm x
>>= f
goPTerm t@(PQuoteName _ _) = f t
goPTerm (PQuoteDecl fc x) =
PQuoteDecl fc <$> goPDecl x
>>= f

4
src/Parser/Lexer/Source.idr
View File

@ -158,8 +158,8 @@ symbols
= [".(", -- for things such as Foo.Bar.(+)
"@{",
"[|", "|]",
"(", ")", "{", "}", "[", "]", ",", ";", "_",
"`(", "`"]
"(", ")", "{", "}}", "}", "[", "]", ",", ";", "_",
"`(", "`{{", "`"]
export
isOpChar : Char -> Bool

16
src/TTImp/Elab/Quote.idr
View File

@ -199,3 +199,19 @@ checkQuote rig elabinfo nest env fc tm exp
checkExp rig elabinfo env fc
!(bindUnqs unqs rig elabinfo nest env qtm)
(gnf env qty) exp
export
checkQuoteName : {vars : _} ->
{auto c : Ref Ctxt Defs} ->
{auto m : Ref MD Metadata} ->
{auto u : Ref UST UState} ->
{auto e : Ref EST (EState vars)} ->
RigCount -> ElabInfo ->
NestedNames vars -> Env Term vars ->
FC -> Name -> Maybe (Glued vars) ->
Core (Term vars, Glued vars)
checkQuoteName rig elabinfo nest env fc n exp
= do defs <- get Ctxt
qnm <- reflect fc defs env n
qty <- getCon fc defs (reflectiontt "Name")
checkExp rig elabinfo env fc qnm (gnf env qty) exp

2
src/TTImp/Elab/Term.idr
View File

@ -178,6 +178,8 @@ checkTerm rig elabinfo nest env (IForce fc tm) exp
= checkForce rig elabinfo nest env fc tm exp
checkTerm rig elabinfo nest env (IQuote fc tm) exp
= checkQuote rig elabinfo nest env fc tm exp
checkTerm rig elabinfo nest env (IQuoteName fc n) exp
= checkQuoteName rig elabinfo nest env fc n exp
checkTerm rig elabinfo nest env (IQuoteDecl fc tm) exp
= throw (GenericMsg fc "Declaration reflection not implemented yet")
checkTerm rig elabinfo nest env (IUnquote fc tm) exp

8
src/TTImp/Reflect.idr
View File

@ -193,6 +193,10 @@ mutual
=> do fc' <- reify defs !(evalClosure defs fc)
t' <- reify defs !(evalClosure defs t)
pure (IQuote fc' t')
(NS _ (UN "IQuoteName"), [fc, t])
=> do fc' <- reify defs !(evalClosure defs fc)
t' <- reify defs !(evalClosure defs t)
pure (IQuoteName fc' t')
(NS _ (UN "IQuoteDecl"), [fc, t])
=> do fc' <- reify defs !(evalClosure defs fc)
t' <- reify defs !(evalClosure defs t)
@ -540,6 +544,10 @@ mutual
= do fc' <- reflect fc defs env tfc
t' <- reflect fc defs env t
appCon fc defs (reflectionttimp "IQuote") [fc', t']
reflect fc defs env (IQuoteName tfc t)
= do fc' <- reflect fc defs env tfc
t' <- reflect fc defs env t
appCon fc defs (reflectionttimp "IQuoteName") [fc', t']
reflect fc defs env (IQuoteDecl tfc t)
= do fc' <- reflect fc defs env tfc
t' <- reflect fc defs env t

37
src/TTImp/TTImp.idr
View File

@ -91,6 +91,7 @@ mutual
-- Quasiquoting
IQuote : FC -> RawImp -> RawImp
IQuoteName : FC -> Name -> RawImp
IQuoteDecl : FC -> ImpDecl -> RawImp
IUnquote : FC -> RawImp -> RawImp
IRunElab : FC -> RawImp -> RawImp
@ -164,6 +165,7 @@ mutual
show (IDelay fc tm) = "(%delay " ++ show tm ++ ")"
show (IForce fc tm) = "(%force " ++ show tm ++ ")"
show (IQuote fc tm) = "(%quote " ++ show tm ++ ")"
show (IQuoteName fc tm) = "(%quotename " ++ show tm ++ ")"
show (IQuoteDecl fc tm) = "(%quotedecl " ++ show tm ++ ")"
show (IUnquote fc tm) = "(%unquote " ++ show tm ++ ")"
show (IRunElab fc tm) = "(%runelab " ++ show tm ++ ")"
@ -600,6 +602,7 @@ getFC (IDelayed x _ _) = x
getFC (IDelay x _) = x
getFC (IForce x _) = x
getFC (IQuote x _) = x
getFC (IQuoteName x _) = x
getFC (IQuoteDecl x _) = x
getFC (IUnquote x _) = x
getFC (IRunElab x _) = x
@ -678,25 +681,27 @@ mutual
toBuf b (IQuote fc t)
= do tag 21; toBuf b fc; toBuf b t
toBuf b (IQuoteDecl fc t)
toBuf b (IQuoteName fc t)
= do tag 22; toBuf b fc; toBuf b t
toBuf b (IUnquote fc t)
toBuf b (IQuoteDecl fc t)
= do tag 23; toBuf b fc; toBuf b t
toBuf b (IRunElab fc t)
toBuf b (IUnquote fc t)
= do tag 24; toBuf b fc; toBuf b t
toBuf b (IRunElab fc t)
= do tag 25; toBuf b fc; toBuf b t
toBuf b (IPrimVal fc y)
= do tag 25; toBuf b fc; toBuf b y
= do tag 26; toBuf b fc; toBuf b y
toBuf b (IType fc)
= do tag 26; toBuf b fc
= do tag 27; toBuf b fc
toBuf b (IHole fc y)
= do tag 27; toBuf b fc; toBuf b y
= do tag 28; toBuf b fc; toBuf b y
toBuf b (IUnifyLog fc lvl x) = toBuf b x
toBuf b (Implicit fc i)
= do tag 28; toBuf b fc; toBuf b i
= do tag 29; toBuf b fc; toBuf b i
toBuf b (IWithUnambigNames fc ns rhs)
= do tag 29; toBuf b ns; toBuf b rhs
= do tag 30; toBuf b ns; toBuf b rhs
fromBuf b
= case !getTag of
@ -766,22 +771,24 @@ mutual
21 => do fc <- fromBuf b; y <- fromBuf b
pure (IQuote fc y)
22 => do fc <- fromBuf b; y <- fromBuf b
pure (IQuoteDecl fc y)
pure (IQuoteName fc y)
23 => do fc <- fromBuf b; y <- fromBuf b
pure (IUnquote fc y)
pure (IQuoteDecl fc y)
24 => do fc <- fromBuf b; y <- fromBuf b
pure (IUnquote fc y)
25 => do fc <- fromBuf b; y <- fromBuf b
pure (IRunElab fc y)
25 => do fc <- fromBuf b; y <- fromBuf b
26 => do fc <- fromBuf b; y <- fromBuf b
pure (IPrimVal fc y)
26 => do fc <- fromBuf b
27 => do fc <- fromBuf b
pure (IType fc)
27 => do fc <- fromBuf b; y <- fromBuf b
28 => do fc <- fromBuf b; y <- fromBuf b
pure (IHole fc y)
28 => do fc <- fromBuf b
29 => do fc <- fromBuf b
i <- fromBuf b
pure (Implicit fc i)
29 => do fc <- fromBuf b
30 => do fc <- fromBuf b
ns <- fromBuf b
rhs <- fromBuf b
pure (IWithUnambigNames fc ns rhs)

1
tests/idris2/reflection001/expected
View File

@ -9,4 +9,5 @@ Main> IApp (MkFC "quote.idr" (3, 12) (3, 23)) (IApp (MkFC "quote.idr" (3, 12) (3
Main> IApp (MkFC "quote.idr" (3, 12) (3, 23)) (IApp (MkFC "quote.idr" (3, 12) (3, 23)) (IVar (MkFC "quote.idr" (3, 12) (3, 23)) (UN "+")) (IVar (MkFC "(interactive)" (0, 6) (0, 10)) (UN "True"))) (IVar (MkFC "(interactive)" (0, 14) (0, 19)) (UN "False"))
Main> ILocal (MkFC "quote.idr" (10, 8) (12, 22)) [IClaim (MkFC "quote.idr" (10, 12) (11, 12)) MW Private [] (MkTy (MkFC "quote.idr" (10, 12) (11, 12)) (UN "xfn") (IPi (MkFC "quote.idr" (10, 18) (11, 12)) MW ExplicitArg Nothing (IPrimVal (MkFC "quote.idr" (10, 18) (10, 22)) IntType) (IPrimVal (MkFC "quote.idr" (10, 25) (11, 12)) IntType))), IDef (MkFC "quote.idr" (11, 12) (11, 30)) (UN "xfn") [PatClause (MkFC "quote.idr" (11, 12) (11, 30)) (IApp (MkFC "quote.idr" (11, 12) (11, 20)) (IVar (MkFC "quote.idr" (11, 12) (11, 16)) (UN "xfn")) (IBindVar (MkFC "quote.idr" (11, 16) (11, 20)) "var")) (IApp (MkFC "quote.idr" (11, 22) (11, 30)) (IApp (MkFC "quote.idr" (11, 22) (11, 30)) (IVar (MkFC "quote.idr" (11, 22) (11, 30)) (UN "*")) (IVar (MkFC "quote.idr" (11, 22) (11, 26)) (UN "var"))) (IApp (MkFC "quote.idr" (11, 28) (11, 30)) (IVar (MkFC "quote.idr" (11, 28) (11, 30)) (UN "fromInteger")) (IPrimVal (MkFC "quote.idr" (11, 28) (11, 30)) (BI 2))))]] (IApp (MkFC "quote.idr" (12, 12) (12, 22)) (IVar (MkFC "quote.idr" (12, 12) (12, 16)) (UN "xfn")) (IApp (MkFC "(interactive)" (0, 9) (0, 22)) (IApp (MkFC "(interactive)" (0, 9) (0, 22)) (IVar (MkFC "(interactive)" (0, 9) (0, 13)) (UN "the")) (IPrimVal (MkFC "(interactive)" (0, 13) (0, 17)) IntType)) (IApp (MkFC "(interactive)" (0, 17) (0, 22)) (IVar (MkFC "(interactive)" (0, 17) (0, 22)) (UN "fromInteger")) (IPrimVal (MkFC "(interactive)" (0, 17) (0, 22)) (BI 99994)))))
Main> ILocal (MkFC "quote.idr" (16, 8) (18, 43)) [IClaim (MkFC "quote.idr" (16, 12) (17, 12)) MW Private [] (MkTy (MkFC "quote.idr" (16, 12) (17, 12)) (UN "xfn") (IPi (MkFC "quote.idr" (16, 18) (17, 12)) MW ExplicitArg Nothing (IPrimVal (MkFC "quote.idr" (16, 18) (16, 22)) IntType) (IPrimVal (MkFC "quote.idr" (16, 25) (17, 12)) IntType))), IDef (MkFC "quote.idr" (17, 12) (17, 30)) (UN "xfn") [PatClause (MkFC "quote.idr" (17, 12) (17, 30)) (IApp (MkFC "quote.idr" (17, 12) (17, 20)) (IVar (MkFC "quote.idr" (17, 12) (17, 16)) (UN "xfn")) (IBindVar (MkFC "quote.idr" (17, 16) (17, 20)) "var")) (IApp (MkFC "quote.idr" (17, 22) (17, 30)) (IApp (MkFC "quote.idr" (17, 22) (17, 30)) (IVar (MkFC "quote.idr" (17, 22) (17, 30)) (UN "*")) (IVar (MkFC "quote.idr" (17, 22) (17, 26)) (UN "var"))) (IApp (MkFC "quote.idr" (17, 28) (17, 30)) (IVar (MkFC "quote.idr" (17, 28) (17, 30)) (UN "fromInteger")) (IPrimVal (MkFC "quote.idr" (17, 28) (17, 30)) (BI 2))))]] (IApp (MkFC "quote.idr" (18, 12) (18, 43)) (IVar (MkFC "quote.idr" (18, 12) (18, 16)) (UN "xfn")) (IPrimVal EmptyFC (I 99994)))
Main> [UN "names", NS ["Prelude"] (UN "+")]
Main> Bye for now!

1
tests/idris2/reflection001/input
View File

@ -2,4 +2,5 @@ test
add `(True) `(False)
bigger `(the Int 99994)
bigger' 99994
names
:q

2
tests/idris2/reflection001/quote.idr
View File

@ -24,3 +24,5 @@ bad val
xfn var = var * 2 in
xfn ~(val))
names : List Name
names = [ `{{ names }}, `{{ Prelude.(+) }} ]