Add reflection operation for adding declarations

Declarations can be quoted with `[ decl ]. See reflection004 for an
example.

libs/base/Language/Reflection.idr

@@ -23,9 +23,12 @@ data Elab : Type -> Type where
      -- and their types. If there's no results, the name is undefined.
      GetType : Name -> Elab (List (Name, TTImp))
 
-     -- Get the constructors of a data type
+     -- Get the constructors of a data type. The name must be fully resolved.
      GetCons : Name -> Elab (List Name)
 
+     -- Check a group of top level declarations
+     Declare : List Decl -> Elab ()
+
 mutual
   export
   Functor Elab where
@@ -79,3 +82,7 @@ getType = GetType
 export
 getCons : Name -> Elab (List Name)
 getCons = GetCons
+
+export
+declare : List Decl -> Elab ()
+declare = Declare

src/Idris/Desugar.idr

@@ -251,9 +251,8 @@ mutual
   desugarB side ps (PQuoteName fc n)
       = pure $ IQuoteName fc n
   desugarB side ps (PQuoteDecl fc x)
-      = do [x'] <- desugarDecl ps x
+      = do xs <- traverse (desugarDecl ps) x
-              | _ => throw (GenericMsg fc "Can't quote this declaration")
+           pure $ IQuoteDecl fc (concat xs)
-           pure $ IQuoteDecl fc x'
   desugarB side ps (PUnquote fc tm)
       = pure $ IUnquote fc !(desugarB side ps tm)
   desugarB side ps (PRunElab fc tm)

src/Idris/Parser.idr

@@ -385,6 +385,12 @@ mutual
            symbol "}}"
            end <- location
            pure (PQuoteName (MkFC fname start end) n)
+    <|> do start <- location
+           symbol "`["
+           ns <- nonEmptyBlock (topDecl fname)
+           symbol "]"
+           end <- location
+           pure (PQuoteDecl (MkFC fname start end) (collectDefs (concat ns)))
     <|> do start <- location
            symbol "~"
            e <- simpleExpr fname indents

src/Idris/Resugar.idr

@@ -241,11 +241,9 @@ mutual
   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)
+  toPTerm p (IQuoteDecl fc ds)
-      = do md <- toPDecl d
+      = do ds' <- traverse toPDecl ds
-           case md of
+           pure $ PQuoteDecl fc (mapMaybe id ds')
-                Nothing => throw (InternalError "Can't resugar log or pragma")
-                Just d' => pure (PQuoteDecl fc d')
   toPTerm p (IUnquote fc tm) = pure (PUnquote fc !(toPTerm argPrec tm))
   toPTerm p (IRunElab fc tm) = pure (PRunElab fc !(toPTerm argPrec tm))
 

src/Idris/Syntax.idr

@@ -54,7 +54,7 @@ mutual
        PPrimVal : FC -> Constant -> PTerm
        PQuote : FC -> PTerm -> PTerm
        PQuoteName : FC -> Name -> PTerm
-       PQuoteDecl : FC -> PDecl -> PTerm
+       PQuoteDecl : FC -> List PDecl -> PTerm
        PUnquote : FC -> PTerm -> PTerm
        PRunElab : FC -> PTerm -> PTerm
        PHole : FC -> (bracket : Bool) -> (holename : String) -> PTerm
@@ -441,7 +441,7 @@ mutual
     showPrec _ (PSearch _ _) = "%search"
     showPrec d (PQuote _ tm) = "`(" ++ showPrec d tm ++ ")"
     showPrec d (PQuoteName _ n) = "`{{" ++ showPrec d n ++ "}}"
-    showPrec d (PQuoteDecl _ tm) = "`( <<declaration>> )"
+    showPrec d (PQuoteDecl _ tm) = "`[ <<declaration>> ]"
     showPrec d (PUnquote _ tm) = "~(" ++ showPrec d tm ++ ")"
     showPrec d (PRunElab _ tm) = "%runElab " ++ showPrec d tm
     showPrec d (PPrimVal _ c) = showPrec d c
@@ -693,7 +693,7 @@ mapPTermM f = goPTerm where
       >>= f
     goPTerm t@(PQuoteName _ _) = f t
     goPTerm (PQuoteDecl fc x) =
-      PQuoteDecl fc <$> goPDecl x
+      PQuoteDecl fc <$> traverse goPDecl x
       >>= f
     goPTerm (PUnquote fc x) =
       PUnquote fc <$> goPTerm x

src/Parser/Lexer/Source.idr

@@ -159,7 +159,7 @@ symbols
        "@{",
        "[|", "|]",
        "(", ")", "{", "}}", "}", "[", "]", ",", ";", "_",
-       "`(", "`{{", "`"]
+       "`(", "`{{", "`[", "`"]
 
 export
 isOpChar : Char -> Bool

src/TTImp/Elab/Quote.idr

@@ -215,3 +215,25 @@ checkQuoteName rig elabinfo nest env fc n exp
          qnm <- reflect fc defs env n
          qty <- getCon fc defs (reflectiontt "Name")
          checkExp rig elabinfo env fc qnm (gnf env qty) exp
+
+export
+checkQuoteDecl : {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 -> List ImpDecl -> Maybe (Glued vars) ->
+                 Core (Term vars, Glued vars)
+checkQuoteDecl rig elabinfo nest env fc ds exp
+    = do defs <- get Ctxt
+         q <- newRef Unq (the (List (Name, FC, RawImp)) [])
+         ds' <- traverse getUnquoteDecl ds
+         qds <- reflect fc defs env ds'
+         unqs <- get Unq
+         qd <- getCon fc defs (reflectionttimp "Decl")
+         qty <- appCon fc defs (prelude "List") [qd]
+         checkExp rig elabinfo env fc
+                  !(bindUnqs unqs rig elabinfo nest env qds)
+                  (gnf env qty) exp

src/TTImp/Elab/RunElab.idr

@@ -96,6 +96,11 @@ elabScript fc elabinfo nest env (NDCon nfc nm t ar args) exp
                      lookupDefExact cn (gamma defs)
                  | _ => throw (GenericMsg fc (show cn ++ " is not a type"))
              scriptRet cons
+    elabCon defs "Declare" [d]
+        = do d' <- evalClosure defs d
+             decls <- reify defs d'
+             traverse_ (processDecl [] (MkNested []) []) decls
+             scriptRet ()
     elabCon defs n args = failWith defs
 elabScript fc elabinfo nest env script exp
     = do defs <- get Ctxt

src/TTImp/Elab/Term.idr

@@ -180,8 +180,8 @@ 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
+checkTerm rig elabinfo nest env (IQuoteDecl fc ds) exp
-    = throw (GenericMsg fc "Declaration reflection not implemented yet")
+    = checkQuoteDecl rig elabinfo nest env fc ds exp
 checkTerm rig elabinfo nest env (IUnquote fc tm) exp
     = throw (GenericMsg fc "Can't escape outside a quoted term")
 checkTerm rig elabinfo nest env (IRunElab fc tm) exp

src/TTImp/TTImp.idr

@@ -92,7 +92,7 @@ mutual
        -- Quasiquoting
        IQuote : FC -> RawImp -> RawImp
        IQuoteName : FC -> Name -> RawImp
-       IQuoteDecl : FC -> ImpDecl -> RawImp
+       IQuoteDecl : FC -> List ImpDecl -> RawImp
        IUnquote : FC -> RawImp -> RawImp
        IRunElab : FC -> RawImp -> RawImp
 

tests/Main.idr

@@ -86,7 +86,7 @@ idrisTests
        -- Records, access and dependent update
        "record001", "record002", "record003", "record004",
        -- Quotation and reflection
-       "reflection001", "reflection002", "reflection003",
+       "reflection001", "reflection002", "reflection003", "reflection004",
        -- Miscellaneous regressions
        "reg001", "reg002", "reg003", "reg004", "reg005", "reg006", "reg007",
        "reg008", "reg009", "reg010", "reg011", "reg012", "reg013", "reg014",

tests/idris2/reflection004/expected

@@ -0,0 +1,5 @@
+1/1: Building refdecl (refdecl.idr)
+Main> 9
+Main> 12
+Main> 5
+Main> Bye for now!

tests/idris2/reflection004/input

@@ -0,0 +1,4 @@
+foo 4 5
+mkMult 3
+myplus 2 3
+:q

tests/idris2/reflection004/refdecl.idr

@@ -0,0 +1,21 @@
+import Language.Reflection
+
+%language ElabReflection
+
+logDecls : TTImp -> Elab TT
+logDecls v
+    = do declare [IClaim EmptyFC MW Public []
+                 (MkTy EmptyFC `{{ Main.foo }}
+                               `(Int -> Int -> Int) )]
+
+         declare `[ foo x y = x + y ]
+
+         declare `[ multBy : Int -> Int
+                    multBy x = x * ~(v) ]
+         declare `[ myplus : Nat -> Nat -> Nat
+                    myplus Z y = y
+                    myplus (S k) y = S (myplus k y) ]
+         check `( multBy )
+
+mkMult : Int -> Int
+mkMult = %runElab logDecls `(4)

tests/idris2/reflection004/run

@@ -0,0 +1,3 @@
+$1 --no-banner refdecl.idr < input
+
+rm -rf build