Merge pull request #218 from edwinb/reflect-defs

More elaborator reflection primitives

CHANGELOG.md

@@ -9,6 +9,11 @@ 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`, including functions for getting types
+     of global names, constructors of data types, and adding new top level
+     declarations
 
 Changes since Idris 2 v0.1.0
 ----------------------------

libs/base/Language/Reflection.idr

@@ -7,6 +7,8 @@ export
 data Elab : Type -> Type where
      Pure : a -> Elab a
      Bind : Elab a -> (a -> Elab b) -> Elab b
+     Fail : String -> Elab a
+
      LogMsg : Nat -> String -> Elab ()
      LogTerm : Nat -> String -> TTImp -> Elab ()
 
@@ -15,6 +17,21 @@ data Elab : Type -> Type where
      -- Get the current goal type, if known 
      -- (it might need to be inferred from the solution)
      Goal : Elab (Maybe TTImp)
+     -- Generate a new unique name, based on the given string
+     GenSym : String -> Elab Name
+     -- Put a name in the current namespace
+     InCurrentNS : Name -> Elab Name
+
+     -- Get the types of every name which matches.
+     -- There may be ambiguities - returns a list of fully explicit names
+     -- 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. The name must be fully resolved.
+     GetCons : Name -> Elab (List Name)
+
+     -- Check a group of top level declarations
+     Declare : List Decl -> Elab ()
 
 mutual
   export
@@ -33,6 +50,10 @@ mutual
   Monad Elab where
     (>>=) = Bind
 
+export
+fail : String -> Elab a
+fail = Fail
+
 export
 logMsg : Nat -> String -> Elab ()
 logMsg = LogMsg
@@ -57,3 +78,23 @@ check = Check
 export
 goal : Elab (Maybe TTImp)
 goal = Goal
+
+export
+genSym : String -> Elab Name
+genSym = GenSym
+
+export
+inCurrentNS : Name -> Elab Name
+inCurrentNS = InCurrentNS
+
+export
+getType : Name -> Elab (List (Name, TTImp))
+getType = GetType
+
+export
+getCons : Name -> Elab (List Name)
+getCons = GetCons
+
+export
+declare : List Decl -> Elab ()
+declare = Declare

libs/base/Language/Reflection/TT.idr

@@ -1,5 +1,7 @@
 module Language.Reflection.TT
 
+import public Data.List
+
 public export
 FilePos : Type
 FilePos = (Int, Int)
@@ -24,6 +26,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 +37,10 @@ data Constant
 
     | IntType
     | IntegerType
+    | Bits8Type
+    | Bits16Type
+    | Bits32Type
+    | Bits64Type
     | StringType
     | CharType
     | DoubleType
@@ -41,6 +51,17 @@ data Name = UN String
           | MN String Int
           | NS (List String) Name
 
+export
+Show Name where
+  show (NS ns n) = showSep "." (reverse ns) ++ "." ++ show n
+    where
+      showSep : String -> List String -> String
+      showSep sep [] = ""
+      showSep sep [x] = x
+      showSep sep (x :: xs) = x ++ sep ++ showSep sep xs
+  show (UN x) = x
+  show (MN x y) = "{" ++ x ++ ":" ++ show y ++ "}"
+
 public export
 data Count = M0 | M1 | MW
 

libs/base/Language/Reflection/TTImp.idr

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

src/Core/Binary.idr

@@ -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 ()

src/Core/Reflect.idr

@@ -243,6 +243,10 @@ Reflect Name where
       = do ns' <- reflect fc defs env ns
            n' <- reflect fc defs env n
            appCon fc defs (reflectiontt "NS") [ns', n']
+  reflect fc defs env (Resolved i)
+      = case !(full (gamma defs) (Resolved i)) of
+             Resolved _ => cantReflect fc "Name"
+             n => reflect fc defs env n
   reflect fc defs env val = cantReflect fc "Name"
 
 export

src/Idris/Desugar.idr

@@ -248,10 +248,11 @@ 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
+      = 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

@@ -379,6 +379,18 @@ 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 "`["
+           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

@@ -240,11 +240,10 @@ 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 (IQuoteDecl fc d)
+  toPTerm p (IQuoteName fc n) = pure (PQuoteName fc n)
-      = do md <- toPDecl d
+  toPTerm p (IQuoteDecl fc ds)
-           case md of
+      = do ds' <- traverse toPDecl ds
-                Nothing => throw (InternalError "Can't resugar log or pragma")
+           pure $ PQuoteDecl fc (mapMaybe id ds')
-                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

@@ -53,7 +53,8 @@ mutual
        PSearch : FC -> (depth : Nat) -> PTerm
        PPrimVal : FC -> Constant -> PTerm
        PQuote : FC -> PTerm -> PTerm
-       PQuoteDecl : FC -> PDecl -> PTerm
+       PQuoteName : FC -> Name -> PTerm
+       PQuoteDecl : FC -> List PDecl -> PTerm
        PUnquote : FC -> PTerm -> PTerm
        PRunElab : FC -> PTerm -> PTerm
        PHole : FC -> (bracket : Bool) -> (holename : String) -> PTerm
@@ -439,7 +440,8 @@ mutual
         = showPrec d f ++ " {" ++ showPrec d n ++ " = " ++ showPrec d a ++ "}"
     showPrec _ (PSearch _ _) = "%search"
     showPrec d (PQuote _ tm) = "`(" ++ showPrec d tm ++ ")"
-    showPrec d (PQuoteDecl _ tm) = "`( <<declaration>> )"
+    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
     showPrec d (PPrimVal _ c) = showPrec d c
@@ -689,8 +691,9 @@ 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
+      PQuoteDecl fc <$> traverse goPDecl x
       >>= f
     goPTerm (PUnquote fc x) =
       PUnquote fc <$> goPTerm x

src/Parser/Lexer/Source.idr

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

src/TTImp/Elab/Quote.idr

@@ -199,3 +199,41 @@ 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
+
+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

@@ -17,6 +17,7 @@ import TTImp.Elab.Delayed
 import TTImp.Reflect
 import TTImp.TTImp
 import TTImp.Unelab
+import TTImp.Utils
 
 elabScript : {vars : _} ->
              {auto c : Ref Ctxt Defs} ->
@@ -56,6 +57,10 @@ elabScript fc elabinfo nest env (NDCon nfc nm t ar args) exp
                                  !(sc defs (toClosure withAll env
                                                  !(quote defs env act'))) exp
                   _ => failWith defs
+    elabCon defs "Fail" [_,msg]
+        = do msg' <- evalClosure defs msg
+             throw (GenericMsg fc ("Error during reflection: " ++
+                                      !(reify defs msg')))
     elabCon defs "LogMsg" [lvl, str]
         = do lvl' <- evalClosure defs lvl
              logC !(reify defs lvl') $
@@ -77,6 +82,34 @@ elabScript fc elabinfo nest env (NDCon nfc nm t ar args) exp
                                      !(reflect fc defs env (the (Maybe RawImp) Nothing))
              ty <- getTerm gty
              scriptRet (Just !(unelabNoSugar env ty))
+    elabCon defs "GenSym" [str]
+        = do str' <- evalClosure defs str
+             n <- uniqueName defs [] !(reify defs str')
+             scriptRet (UN n)
+    elabCon defs "InCurrentNS" [n]
+        = do n' <- evalClosure defs n
+             nsn <- inCurrentNS !(reify defs n')
+             scriptRet nsn
+    elabCon defs "GetType" [n]
+        = do n' <- evalClosure defs n
+             res <- lookupTyName !(reify defs n') (gamma defs)
+             scriptRet !(traverse unelabType res)
+      where
+        unelabType : (Name, Int, ClosedTerm) -> Core (Name, RawImp)
+        unelabType (n, _, ty)
+            = pure (n, !(unelabNoSugar [] ty))
+    elabCon defs "GetCons" [n]
+        = do n' <- evalClosure defs n
+             cn <- reify defs n'
+             Just (TCon _ _ _ _ _ _ cons _) <-
+                     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

@@ -178,8 +178,10 @@ 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 (IQuoteDecl fc tm) exp
+checkTerm rig elabinfo nest env (IQuoteName fc n) exp
-    = throw (GenericMsg fc "Declaration reflection not implemented yet")
+    = checkQuoteName rig elabinfo nest env fc n exp
+checkTerm rig elabinfo nest env (IQuoteDecl fc ds) exp
+    = 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/Reflect.idr

@@ -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

src/TTImp/TTImp.idr

@@ -91,7 +91,8 @@ mutual
 
        -- Quasiquoting
        IQuote : FC -> RawImp -> RawImp
-       IQuoteDecl : FC -> ImpDecl -> RawImp
+       IQuoteName : FC -> Name -> RawImp
+       IQuoteDecl : FC -> List 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)

tests/Main.idr

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

tests/idris2/reflection001/expected

@@ -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!

tests/idris2/reflection001/input

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

tests/idris2/reflection001/quote.idr

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

tests/idris2/reflection003/expected

@@ -0,0 +1,15 @@
+1/1: Building refprims (refprims.idr)
+LOG 0: Name: Prelude.List.++
+LOG 0: Type: (%pi Rig0 Implicit Just a %type (%pi Rig1 Explicit Just _ (Prelude.List a) (%pi RigW Explicit Nothing (Prelude.List a) (Prelude.List a))))
+LOG 0: Name: Prelude.Strings.++
+LOG 0: Type: (%pi Rig1 Explicit Just _ String (%pi Rig1 Explicit Just _ String String))
+LOG 0: Resolved name: Prelude.Nat
+LOG 0: Constructors: [Prelude.Z, Prelude.S]
+refprims.idr:37:10--39:1:While processing right hand side of dummy1 at refprims.idr:37:1--39:1:
+Error during reflection: Not really trying
+refprims.idr:40:10--42:1:While processing right hand side of dummy2 at refprims.idr:40:1--42:1:
+Error during reflection: Still not trying
+refprims.idr:43:10--45:1:While processing right hand side of dummy3 at refprims.idr:43:1--45:1:
+Error during reflection: Undefined name
+refprims.idr:46:10--48:1:While processing right hand side of dummy4 at refprims.idr:46:1--48:1:
+Error during reflection: failed after generating Main.plus_1

tests/idris2/reflection003/refprims.idr

@@ -0,0 +1,47 @@
+import Language.Reflection
+
+%language ElabReflection
+
+logPrims : Elab TT
+logPrims
+    = do ns <- getType `{{ (++) }} 
+         traverse (\ (n, ty) =>
+                        do logMsg 0 ("Name: " ++ show n)
+                           logTerm 0 "Type" ty) ns
+         fail "Not really trying"
+
+logDataCons : Elab TT
+logDataCons
+    = do [(n, _)] <- getType `{{ Nat }}
+             | _ => fail "Ambiguous name"
+         logMsg 0 ("Resolved name: " ++ show n)
+         logMsg 0 ("Constructors: " ++ show !(getCons n))
+         fail "Still not trying"
+
+logBad : Elab TT
+logBad
+    = do [(n, _)] <- getType `{{ DoesntExist }}
+             | [] => fail "Undefined name"
+             | _ => fail "Ambiguous name"
+         logMsg 0 ("Resolved name: " ++ show n)
+         logMsg 0 ("Constructors: " ++ show !(getCons n))
+         fail "Still not trying"
+
+tryGenSym : Elab TT
+tryGenSym
+   = do n <- genSym "plus"
+        ns <- inCurrentNS n
+        fail $ "failed after generating " ++ show ns
+
+dummy1 : a
+dummy1 = %runElab logPrims
+
+dummy2 : a
+dummy2 = %runElab logDataCons
+
+dummy3 : a
+dummy3 = %runElab logBad
+
+dummy4 : a
+dummy4 = %runElab tryGenSym
+

tests/idris2/reflection003/run

@@ -0,0 +1,3 @@
+$1 refprims.idr --check
+
+rm -rf build

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