diff --git a/CHANGELOG.md b/CHANGELOG.md index cb0d93e86..f8ef7951c 100644 --- a/CHANGELOG.md +++ b/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 ---------------------------- diff --git a/libs/base/Language/Reflection.idr b/libs/base/Language/Reflection.idr index 2fc30882f..d4d617d43 100644 --- a/libs/base/Language/Reflection.idr +++ b/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 diff --git a/libs/base/Language/Reflection/TT.idr b/libs/base/Language/Reflection/TT.idr index 14980bfe2..76b8fdc76 100644 --- a/libs/base/Language/Reflection/TT.idr +++ b/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 diff --git a/libs/base/Language/Reflection/TTImp.idr b/libs/base/Language/Reflection/TTImp.idr index 00f1adbf9..56d4074ba 100644 --- a/libs/base/Language/Reflection/TTImp.idr +++ b/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 diff --git a/src/Core/Binary.idr b/src/Core/Binary.idr index 31147a7ee..46737b91b 100644 --- a/src/Core/Binary.idr +++ b/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 () diff --git a/src/Core/Reflect.idr b/src/Core/Reflect.idr index a31ec0f85..2061d1533 100644 --- a/src/Core/Reflect.idr +++ b/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 diff --git a/src/Idris/Desugar.idr b/src/Idris/Desugar.idr index 8578a6346..3f51e99c2 100644 --- a/src/Idris/Desugar.idr +++ b/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 - | _ => throw (GenericMsg fc "Can't quote this declaration") - pure $ IQuoteDecl fc x' + = do xs <- traverse (desugarDecl ps) x + pure $ IQuoteDecl fc (concat xs) desugarB side ps (PUnquote fc tm) = pure $ IUnquote fc !(desugarB side ps tm) desugarB side ps (PRunElab fc tm) diff --git a/src/Idris/Parser.idr b/src/Idris/Parser.idr index 81ba79c74..d2046bb7c 100644 --- a/src/Idris/Parser.idr +++ b/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 diff --git a/src/Idris/Resugar.idr b/src/Idris/Resugar.idr index 0d2843281..39783bf2b 100644 --- a/src/Idris/Resugar.idr +++ b/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) - = do md <- toPDecl d - case md of - Nothing => throw (InternalError "Can't resugar log or pragma") - Just d' => pure (PQuoteDecl fc d') + toPTerm p (IQuoteName fc n) = pure (PQuoteName fc n) + toPTerm p (IQuoteDecl fc ds) + = do ds' <- traverse toPDecl ds + pure $ PQuoteDecl fc (mapMaybe id ds') toPTerm p (IUnquote fc tm) = pure (PUnquote fc !(toPTerm argPrec tm)) toPTerm p (IRunElab fc tm) = pure (PRunElab fc !(toPTerm argPrec tm)) diff --git a/src/Idris/Syntax.idr b/src/Idris/Syntax.idr index cbee738ae..928a1506b 100644 --- a/src/Idris/Syntax.idr +++ b/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) = "`( <> )" + showPrec d (PQuoteName _ n) = "`{{" ++ showPrec d n ++ "}}" + showPrec d (PQuoteDecl _ tm) = "`[ <> ]" 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 diff --git a/src/Parser/Lexer/Source.idr b/src/Parser/Lexer/Source.idr index 9a6b25b67..468416c7a 100644 --- a/src/Parser/Lexer/Source.idr +++ b/src/Parser/Lexer/Source.idr @@ -158,8 +158,8 @@ symbols = [".(", -- for things such as Foo.Bar.(+) "@{", "[|", "|]", - "(", ")", "{", "}", "[", "]", ",", ";", "_", - "`(", "`"] + "(", ")", "{", "}}", "}", "[", "]", ",", ";", "_", + "`(", "`{{", "`[", "`"] export isOpChar : Char -> Bool diff --git a/src/TTImp/Elab/Quote.idr b/src/TTImp/Elab/Quote.idr index 709e23d6b..181d5f9e1 100644 --- a/src/TTImp/Elab/Quote.idr +++ b/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 diff --git a/src/TTImp/Elab/RunElab.idr b/src/TTImp/Elab/RunElab.idr index 3e9762920..90afab4d7 100644 --- a/src/TTImp/Elab/RunElab.idr +++ b/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 diff --git a/src/TTImp/Elab/Term.idr b/src/TTImp/Elab/Term.idr index d5e3101ac..a4af5f6d1 100644 --- a/src/TTImp/Elab/Term.idr +++ b/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 - = throw (GenericMsg fc "Declaration reflection not implemented yet") +checkTerm rig elabinfo nest env (IQuoteName fc n) exp + = 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 diff --git a/src/TTImp/Reflect.idr b/src/TTImp/Reflect.idr index cd80d0529..0f7768cda 100644 --- a/src/TTImp/Reflect.idr +++ b/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 diff --git a/src/TTImp/TTImp.idr b/src/TTImp/TTImp.idr index a15035282..ef9ad7126 100644 --- a/src/TTImp/TTImp.idr +++ b/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) diff --git a/tests/Main.idr b/tests/Main.idr index b5b03bf1a..d0010de40 100644 --- a/tests/Main.idr +++ b/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", diff --git a/tests/idris2/reflection001/expected b/tests/idris2/reflection001/expected index 6d2d902c0..388168ca1 100644 --- a/tests/idris2/reflection001/expected +++ b/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! diff --git a/tests/idris2/reflection001/input b/tests/idris2/reflection001/input index 36a1594f5..dcd920553 100644 --- a/tests/idris2/reflection001/input +++ b/tests/idris2/reflection001/input @@ -2,4 +2,5 @@ test add `(True) `(False) bigger `(the Int 99994) bigger' 99994 +names :q diff --git a/tests/idris2/reflection001/quote.idr b/tests/idris2/reflection001/quote.idr index 8f1f9ea33..466995f36 100644 --- a/tests/idris2/reflection001/quote.idr +++ b/tests/idris2/reflection001/quote.idr @@ -24,3 +24,5 @@ bad val xfn var = var * 2 in xfn ~(val)) +names : List Name +names = [ `{{ names }}, `{{ Prelude.(+) }} ] diff --git a/tests/idris2/reflection003/expected b/tests/idris2/reflection003/expected new file mode 100644 index 000000000..bba3c69dc --- /dev/null +++ b/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 diff --git a/tests/idris2/reflection003/refprims.idr b/tests/idris2/reflection003/refprims.idr new file mode 100644 index 000000000..3648a2556 --- /dev/null +++ b/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 + diff --git a/tests/idris2/reflection003/run b/tests/idris2/reflection003/run new file mode 100755 index 000000000..223173a47 --- /dev/null +++ b/tests/idris2/reflection003/run @@ -0,0 +1,3 @@ +$1 refprims.idr --check + +rm -rf build diff --git a/tests/idris2/reflection004/expected b/tests/idris2/reflection004/expected new file mode 100644 index 000000000..2aa014a28 --- /dev/null +++ b/tests/idris2/reflection004/expected @@ -0,0 +1,5 @@ +1/1: Building refdecl (refdecl.idr) +Main> 9 +Main> 12 +Main> 5 +Main> Bye for now! diff --git a/tests/idris2/reflection004/input b/tests/idris2/reflection004/input new file mode 100644 index 000000000..f00c1b8b7 --- /dev/null +++ b/tests/idris2/reflection004/input @@ -0,0 +1,4 @@ +foo 4 5 +mkMult 3 +myplus 2 3 +:q diff --git a/tests/idris2/reflection004/refdecl.idr b/tests/idris2/reflection004/refdecl.idr new file mode 100644 index 000000000..d4bd1a8b1 --- /dev/null +++ b/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) diff --git a/tests/idris2/reflection004/run b/tests/idris2/reflection004/run new file mode 100755 index 000000000..facaa98e2 --- /dev/null +++ b/tests/idris2/reflection004/run @@ -0,0 +1,3 @@ +$1 --no-banner refdecl.idr < input + +rm -rf build