From cbbe761c5193c538251490fe287709a84c41fc3e Mon Sep 17 00:00:00 2001 From: Robert Wright Date: Wed, 22 Mar 2023 15:17:53 +0000 Subject: [PATCH] Add fromTTImp, fromName, and fromDecls for custom TTImp, Name, and Decls literals --- CHANGELOG.md | 2 + src/Core/Binary.idr | 24 ++++++-- src/Core/Context.idr | 44 +++++++++++++- src/Core/Options.idr | 21 ++++++- src/Core/TTC.idr | 8 ++- src/Idris/Desugar.idr | 39 +++++++----- src/Idris/Parser.idr | 12 ++++ src/Idris/Syntax.idr | 3 + src/TTImp/Elab/Ambiguity.idr | 16 +++-- tests/Main.idr | 2 +- tests/idris2/reflection020/FromDecls.idr | 76 ++++++++++++++++++++++++ tests/idris2/reflection020/FromName.idr | 53 +++++++++++++++++ tests/idris2/reflection020/FromTTImp.idr | 72 ++++++++++++++++++++++ tests/idris2/reflection020/expected | 23 +++++++ tests/idris2/reflection020/run | 23 +++++++ 15 files changed, 388 insertions(+), 30 deletions(-) create mode 100644 tests/idris2/reflection020/FromDecls.idr create mode 100644 tests/idris2/reflection020/FromName.idr create mode 100644 tests/idris2/reflection020/FromTTImp.idr create mode 100644 tests/idris2/reflection020/expected create mode 100644 tests/idris2/reflection020/run diff --git a/CHANGELOG.md b/CHANGELOG.md index 78e7d9b5f..2a1315fa3 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -16,6 +16,8 @@ * Rudimentary support for defining lazy functions (addressing issue [#1066](https://github.com/idris-lang/idris2/issues/1066)). * `%hide` directives can now hide conflicting fixities from other modules. +* New fromTTImp, fromName, and fromDecls names for custom TTImp, Name, and Decls + literals. ### REPL changes diff --git a/src/Core/Binary.idr b/src/Core/Binary.idr index 46e74a7fd..1c3a1cec3 100644 --- a/src/Core/Binary.idr +++ b/src/Core/Binary.idr @@ -29,7 +29,7 @@ import public Libraries.Utils.Binary ||| version number if you're changing the version more than once in the same day. export ttcVersion : Int -ttcVersion = 20230331 * 100 + 0 +ttcVersion = 20230414 * 100 + 0 export checkTTCVersion : String -> Int -> Int -> Core () @@ -125,8 +125,14 @@ HasNames e => HasNames (TTCFile e) where = pure $ Just $ MkRewriteNs !(full gam e) !(full gam r) fullPrim : Context -> PrimNames -> Core PrimNames - fullPrim gam (MkPrimNs mi ms mc md) - = [| MkPrimNs (full gam mi) (full gam ms) (full gam mc) (full gam md) |] + fullPrim gam (MkPrimNs mi ms mc md mt mn mdl) + = [| MkPrimNs (full gam mi) + (full gam ms) + (full gam mc) + (full gam md) + (full gam mt) + (full gam mn) + (full gam mdl) |] -- I don't think we ever actually want to call this, because after we read @@ -164,11 +170,14 @@ HasNames e => HasNames (TTCFile e) where = pure $ Just $ MkRewriteNs !(resolved gam e) !(resolved gam r) resolvedPrim : Context -> PrimNames -> Core PrimNames - resolvedPrim gam (MkPrimNs mi ms mc md) + resolvedPrim gam (MkPrimNs mi ms mc md mt mn mdl) = pure $ MkPrimNs !(resolved gam mi) !(resolved gam ms) !(resolved gam mc) !(resolved gam md) + !(resolved gam mt) + !(resolved gam mn) + !(resolved gam mdl) -- NOTE: TTC files are only compatible if the version number is the same, -- *and* the 'annot/extra' type are the same, or there are no holes/constraints @@ -224,7 +233,7 @@ readTTCFile readall file as b incData [] [] [] [] [] 0 (mkNamespace "") [] Nothing Nothing - (MkPrimNs Nothing Nothing Nothing Nothing) + (MkPrimNs Nothing Nothing Nothing Nothing Nothing Nothing Nothing) [] [] [] [] ex) else do defs <- fromBuf b @@ -374,7 +383,10 @@ updatePrimNames p = { fromIntegerName $= (p.fromIntegerName <+>), fromStringName $= (p.fromStringName <+>), fromCharName $= (p.fromCharName <+>), - fromDoubleName $= (p.fromDoubleName <+>) + fromDoubleName $= (p.fromDoubleName <+>), + fromTTImpName $= (p.fromTTImpName <+>), + fromNameName $= (p.fromNameName <+>), + fromDeclsName $= (p.fromDeclsName <+>) } export diff --git a/src/Core/Context.idr b/src/Core/Context.idr index 34ca8a8a9..4ce119459 100644 --- a/src/Core/Context.idr +++ b/src/Core/Context.idr @@ -2308,6 +2308,21 @@ setFromDouble : {auto c : Ref Ctxt Defs} -> Name -> Core () setFromDouble n = update Ctxt { options $= setFromDouble n } +export +setFromTTImp : {auto c : Ref Ctxt Defs} -> + Name -> Core () +setFromTTImp n = update Ctxt { options $= setFromTTImp n } + +export +setFromName : {auto c : Ref Ctxt Defs} -> + Name -> Core () +setFromName n = update Ctxt { options $= setFromName n } + +export +setFromDecls : {auto c : Ref Ctxt Defs} -> + Name -> Core () +setFromDecls n = update Ctxt { options $= setFromDecls n } + export addNameDirective : {auto c : Ref Ctxt Defs} -> FC -> Name -> List String -> Core () @@ -2384,9 +2399,36 @@ fromDoubleName = do defs <- get Ctxt pure $ fromDoubleName (primnames (options defs)) +export +fromTTImpName : {auto c : Ref Ctxt Defs} -> + Core (Maybe Name) +fromTTImpName + = do defs <- get Ctxt + pure $ fromTTImpName (primnames (options defs)) + +export +fromNameName : {auto c : Ref Ctxt Defs} -> + Core (Maybe Name) +fromNameName + = do defs <- get Ctxt + pure $ fromNameName (primnames (options defs)) + +export +fromDeclsName : {auto c : Ref Ctxt Defs} -> + Core (Maybe Name) +fromDeclsName + = do defs <- get Ctxt + pure $ fromDeclsName (primnames (options defs)) + export getPrimNames : {auto c : Ref Ctxt Defs} -> Core PrimNames -getPrimNames = [| MkPrimNs fromIntegerName fromStringName fromCharName fromDoubleName |] +getPrimNames = [| MkPrimNs fromIntegerName + fromStringName + fromCharName + fromDoubleName + fromTTImpName + fromNameName + fromDeclsName |] export getPrimitiveNames : {auto c : Ref Ctxt Defs} -> Core (List Name) diff --git a/src/Core/Options.idr b/src/Core/Options.idr index 28817f682..5bbe901dc 100644 --- a/src/Core/Options.idr +++ b/src/Core/Options.idr @@ -107,10 +107,13 @@ record PrimNames where fromStringName : Maybe Name fromCharName : Maybe Name fromDoubleName : Maybe Name + fromTTImpName : Maybe Name + fromNameName : Maybe Name + fromDeclsName : Maybe Name export primNamesToList : PrimNames -> List Name -primNamesToList (MkPrimNs i s c d) = catMaybes [i,s,c,d] +primNamesToList (MkPrimNs i s c d t n dl) = catMaybes [i,s,c,d,t,n,dl] -- Other options relevant to the current session (so not to be saved in a TTC) public export @@ -250,14 +253,14 @@ defaults -- it to fail gracefully. pure $ MkOptions defaultDirs defaultPPrint defaultSession defaultElab Nothing Nothing - (MkPrimNs Nothing Nothing Nothing Nothing) [] [] Nothing + (MkPrimNs Nothing Nothing Nothing Nothing Nothing Nothing Nothing) [] [] Nothing -- Reset the options which are set by source files export clearNames : Options -> Options clearNames = { pairnames := Nothing, rewritenames := Nothing, - primnames := MkPrimNs Nothing Nothing Nothing Nothing, + primnames := MkPrimNs Nothing Nothing Nothing Nothing Nothing Nothing Nothing, extensions := [] } @@ -286,6 +289,18 @@ export setFromDouble : Name -> Options -> Options setFromDouble n = { primnames->fromDoubleName := Just n } +export +setFromTTImp : Name -> Options -> Options +setFromTTImp n = { primnames->fromTTImpName := Just n } + +export +setFromName : Name -> Options -> Options +setFromName n = { primnames->fromNameName := Just n } + +export +setFromDecls : Name -> Options -> Options +setFromDecls n = { primnames->fromDeclsName := Just n } + export setExtension : LangExt -> Options -> Options setExtension e = { extensions $= (e ::) } diff --git a/src/Core/TTC.idr b/src/Core/TTC.idr index d54e29003..fcc6f7934 100644 --- a/src/Core/TTC.idr +++ b/src/Core/TTC.idr @@ -916,12 +916,18 @@ TTC PrimNames where toBuf b (fromStringName l) toBuf b (fromCharName l) toBuf b (fromDoubleName l) + toBuf b (fromTTImpName l) + toBuf b (fromNameName l) + toBuf b (fromDeclsName l) fromBuf b = do i <- fromBuf b str <- fromBuf b c <- fromBuf b d <- fromBuf b - pure (MkPrimNs i str c d) + t <- fromBuf b + n <- fromBuf b + dl <- fromBuf b + pure (MkPrimNs i str c d t n dl) export TTC HoleInfo where diff --git a/src/Idris/Desugar.idr b/src/Idris/Desugar.idr index 1f066e3c0..22b5fb8d1 100644 --- a/src/Idris/Desugar.idr +++ b/src/Idris/Desugar.idr @@ -345,12 +345,21 @@ mutual pure $ IApp vfc (IVar vfc f) (IPrimVal fc (Db x)) desugarB side ps (PPrimVal fc x) = pure $ IPrimVal fc x desugarB side ps (PQuote fc tm) - = pure $ IQuote fc !(desugarB side ps tm) + = do let q = IQuote fc !(desugarB side ps tm) + case side of + AnyExpr => pure $ maybeIApp fc !fromTTImpName q + _ => pure q desugarB side ps (PQuoteName fc n) - = pure $ IQuoteName fc n + = do let q = IQuoteName fc n + case side of + AnyExpr => pure $ maybeIApp fc !fromNameName q + _ => pure q desugarB side ps (PQuoteDecl fc x) = do xs <- traverse (desugarDecl ps) x - pure $ IQuoteDecl fc (concat xs) + let dls = IQuoteDecl fc (concat xs) + case side of + AnyExpr => pure $ maybeIApp fc !fromDeclsName dls + _ => pure dls desugarB side ps (PUnquote fc tm) = pure $ IUnquote fc !(desugarB side ps tm) desugarB side ps (PRunElab fc tm) @@ -369,17 +378,17 @@ mutual throw (GenericMsg fc "? is not a valid pattern") pure $ Implicit fc False desugarB side ps (PMultiline fc hashtag indent lines) - = addFromString fc !(expandString side ps fc hashtag !(trimMultiline fc indent lines)) + = pure $ maybeIApp fc !fromStringName !(expandString side ps fc hashtag !(trimMultiline fc indent lines)) -- We only add `fromString` if we are looking at a plain string literal. -- Interpolated string literals don't have a `fromString` call since they -- are always concatenated with other strings and therefore can never use -- another `fromString` implementation that differs from `id`. desugarB side ps (PString fc hashtag []) - = addFromString fc (IPrimVal fc (Str "")) + = pure $ maybeIApp fc !fromStringName (IPrimVal fc (Str "")) desugarB side ps (PString fc hashtag [StrLiteral fc' str]) = case unescape hashtag str of - Just str => addFromString fc (IPrimVal fc' (Str str)) + Just str => pure $ maybeIApp fc !fromStringName (IPrimVal fc' (Str str)) Nothing => throw (GenericMsg fc "Invalid escape sequence: \{show str}") desugarB side ps (PString fc hashtag strs) = expandString side ps fc hashtag strs @@ -517,14 +526,13 @@ mutual = pure $ apply (IVar consFC (UN $ Basic ":<")) [!(expandSnocList side ps nilFC xs) , !(desugarB side ps x)] - addFromString : {auto c : Ref Ctxt Defs} -> - FC -> RawImp -> Core RawImp - addFromString fc tm - = pure $ case !fromStringName of - Nothing => tm - Just f => - let fc = virtualiseFC fc in - IApp fc (IVar fc f) tm + maybeIApp : FC -> Maybe Name -> RawImp -> RawImp + maybeIApp fc nm tm + = case nm of + Nothing => tm + Just f => + let fc = virtualiseFC fc in + IApp fc (IVar fc f) tm expandString : {auto s : Ref Syn SyntaxInfo} -> {auto b : Ref Bang BangData} -> @@ -1183,6 +1191,9 @@ mutual PrimString n => pure [IPragma fc [] (\nest, env => setFromString n)] PrimChar n => pure [IPragma fc [] (\nest, env => setFromChar n)] PrimDouble n => pure [IPragma fc [] (\nest, env => setFromDouble n)] + PrimTTImp n => pure [IPragma fc [] (\nest, env => setFromTTImp n)] + PrimName n => pure [IPragma fc [] (\nest, env => setFromName n)] + PrimDecls n => pure [IPragma fc [] (\nest, env => setFromDecls n)] CGAction cg dir => pure [IPragma fc [] (\nest, env => addDirective cg dir)] Names n ns => pure [IPragma fc [] (\nest, env => addNameDirective fc n ns)] StartExpr tm => pure [IPragma fc [] (\nest, env => throw (InternalError "%start not implemented"))] -- TODO! diff --git a/src/Idris/Parser.idr b/src/Idris/Parser.idr index f3a5ad230..8e47a2649 100644 --- a/src/Idris/Parser.idr +++ b/src/Idris/Parser.idr @@ -1376,6 +1376,18 @@ directive fname indents n <- name atEnd indents pure (PrimDouble n) + <|> do decoratedPragma fname "TTImpLit" + n <- name + atEnd indents + pure (PrimTTImp n) + <|> do decoratedPragma fname "nameLit" + n <- name + atEnd indents + pure (PrimName n) + <|> do decoratedPragma fname "declsLit" + n <- name + atEnd indents + pure (PrimDecls n) <|> do decoratedPragma fname "name" n <- name ns <- sepBy1 (decoratedSymbol fname ",") diff --git a/src/Idris/Syntax.idr b/src/Idris/Syntax.idr index c4ad75201..ff0423c9c 100644 --- a/src/Idris/Syntax.idr +++ b/src/Idris/Syntax.idr @@ -347,6 +347,9 @@ mutual PrimString : Name -> Directive PrimChar : Name -> Directive PrimDouble : Name -> Directive + PrimTTImp : Name -> Directive + PrimName : Name -> Directive + PrimDecls : Name -> Directive CGAction : String -> String -> Directive Names : Name -> List String -> Directive StartExpr : PTerm' nm -> Directive diff --git a/src/TTImp/Elab/Ambiguity.idr b/src/TTImp/Elab/Ambiguity.idr index 5d24bea28..3e45e772c 100644 --- a/src/TTImp/Elab/Ambiguity.idr +++ b/src/TTImp/Elab/Ambiguity.idr @@ -91,14 +91,22 @@ expandAmbigName mode nest env orig args (IVar fc x) exp -- If there's multiple alternatives and all else fails, resort to using -- the primitive directly uniqType : PrimNames -> Name -> List (FC, Maybe (Maybe Name), RawImp) -> AltType - uniqType (MkPrimNs (Just fi) _ _ _) n [(_, _, IPrimVal fc (BI x))] + uniqType (MkPrimNs (Just fi) _ _ _ _ _ _) n [(_, _, IPrimVal fc (BI x))] = UniqueDefault (IPrimVal fc (BI x)) - uniqType (MkPrimNs _ (Just si) _ _) n [(_, _, IPrimVal fc (Str x))] + uniqType (MkPrimNs _ (Just si) _ _ _ _ _) n [(_, _, IPrimVal fc (Str x))] = UniqueDefault (IPrimVal fc (Str x)) - uniqType (MkPrimNs _ _ (Just ci) _) n [(_, _, IPrimVal fc (Ch x))] + uniqType (MkPrimNs _ _ (Just ci) _ _ _ _) n [(_, _, IPrimVal fc (Ch x))] = UniqueDefault (IPrimVal fc (Ch x)) - uniqType (MkPrimNs _ _ _ (Just di)) n [(_, _, IPrimVal fc (Db x))] + uniqType (MkPrimNs _ _ _ (Just di) _ _ _) n [(_, _, IPrimVal fc (Db x))] = UniqueDefault (IPrimVal fc (Db x)) + uniqType (MkPrimNs _ _ _ _ (Just dt) _ _) n [(_, _, IQuote fc tm)] + = UniqueDefault (IQuote fc tm) + {- + uniqType (MkPrimNs _ _ _ _ _ (Just dn) _) n [(_, _, IQuoteName fc tm)] + = UniqueDefault (IQuoteName fc tm) + uniqType (MkPrimNs _ _ _ _ _ _ (Just ddl)) n [(_, _, IQuoteDecl fc tm)] + = UniqueDefault (IQuoteDecl fc tm) + -} uniqType _ _ _ = Unique buildAlt : RawImp -> List (FC, Maybe (Maybe Name), RawImp) -> diff --git a/tests/Main.idr b/tests/Main.idr index 030fd22ea..ff6b3362f 100644 --- a/tests/Main.idr +++ b/tests/Main.idr @@ -250,7 +250,7 @@ idrisTestsReflection = MkTestPool "Quotation and Reflection" [] Nothing "reflection005", "reflection006", "reflection007", "reflection008", "reflection009", "reflection010", "reflection011", "reflection012", "reflection013", "reflection014", "reflection015", "reflection016", - "reflection017", "reflection018", "reflection019"] + "reflection017", "reflection018", "reflection019", "reflection020"] idrisTestsWith : TestPool idrisTestsWith = MkTestPool "With abstraction" [] Nothing diff --git a/tests/idris2/reflection020/FromDecls.idr b/tests/idris2/reflection020/FromDecls.idr new file mode 100644 index 000000000..b8e1e205a --- /dev/null +++ b/tests/idris2/reflection020/FromDecls.idr @@ -0,0 +1,76 @@ +import Data.List.Quantifiers + +import Language.Reflection + +import FromTTImp + +%language ElabReflection + +%declsLit fromDecls + +record NatDecl where + constructor MkNatDecl + var : String + expr : NatExpr + +natDecl : Decl -> Elab NatDecl +natDecl (IDef _ (UN (Basic nm)) [PatClause _ (IVar _ _) def]) = pure $ MkNatDecl nm !(natExpr def) +natDecl decl = fail "Invalid NatDecl" + +natDecls : List Decl -> Elab (List NatDecl) +natDecls decls = traverse natDecl decls + +namespace AsMacro + %macro + fromDecls : List Decl -> Elab (List NatDecl) + fromDecls = natDecls + + export + natDeclsMacroTest : List NatDecl + natDeclsMacroTest = `[ + x = 1 + 2 + a + y = 1 + 2 * 3 + 4 + ] + + failing "Invalid NatDecl" + natDeclsInvalid : List NatDecl + natDeclsInvalid = `[f x = 1 + 2] + + failing "Invalid NatDecl" + natDeclsInvalid : List NatDecl + natDeclsInvalid = `[x : 1] + +namespace AsScript + fromDecls : List Decl -> Elab (List NatDecl) + fromDecls = natDecls + + export + natDeclsScriptTest : List NatDecl + natDeclsScriptTest = %runElab `[x = 1 + 2 * 3 + 4] + + failing "Invalid NatDecl" + natDeclsInvalid : List NatDecl + natDeclsInvalid = %runElab `[f x = 1 + 2] + +namespace AsFunction + data IsNatDecl : Decl -> Type where + ItIsNatDecl : IsNatExpr def -> IsNatDecl (IDef fc1 (UN (Basic nm)) [PatClause fc2 (IVar fc3 (UN (Basic nm))) def]) + + fromDecl : (decl : Decl) -> + IsNatDecl decl => + NatDecl + fromDecl @{ItIsNatDecl _} (IDef _ (UN (Basic nm)) [PatClause _ (IVar _ (UN (Basic nm))) def]) = MkNatDecl nm $ fromTTImp def + + fromDecls : (decls : List Decl) -> + All IsNatDecl decls => + List NatDecl + fromDecls [] = [] + fromDecls @{_ :: _} (decl :: decls) = fromDecl decl :: fromDecls decls + + export + natDeclsFunctionTest : List NatDecl + natDeclsFunctionTest = `[x = 1 + 2 * 3 + 4] + + failing "Can't find an implementation for All IsNatDecl" + natDeclsInvalid : List NatDecl + natDeclsInvalid = `[f x = 1 + 2] diff --git a/tests/idris2/reflection020/FromName.idr b/tests/idris2/reflection020/FromName.idr new file mode 100644 index 000000000..2c9bd405a --- /dev/null +++ b/tests/idris2/reflection020/FromName.idr @@ -0,0 +1,53 @@ +import Language.Reflection + +%language ElabReflection + +%nameLit fromName + +data MyName = MkMyName String + +myName : Name -> Elab MyName +myName (UN (Basic nm)) = pure $ MkMyName nm +myName nm = fail "Invalid MyName" + +namespace AsMacro + %macro + fromName : Name -> Elab MyName + fromName = myName + + export + myNameMacroTest : MyName + myNameMacroTest = `{x} + + failing "Invalid MyName" + myNameInvalid : MyName + myNameInvalid = `{A.x} + +namespace AsScript + fromName : Name -> Elab MyName + fromName = myName + + export + myNameScriptTest : MyName + myNameScriptTest = %runElab `{y} + + failing "Invalid MyName" + myNameInvalid : MyName + myNameInvalid = %runElab `{A.y} + +namespace AsFunction + data IsMyName : Name -> Type where + ItIsMyName : IsMyName (UN (Basic nm)) + + fromName : (nm : Name) -> + IsMyName nm => + MyName + fromName (UN (Basic nm)) @{ItIsMyName} = MkMyName nm + + export + myNameFunctionTest : MyName + myNameFunctionTest = `{z} + + failing "Can't find an implementation for IsMyName" + myNameInvalid : MyName + myNameInvalid = `{A.z} diff --git a/tests/idris2/reflection020/FromTTImp.idr b/tests/idris2/reflection020/FromTTImp.idr new file mode 100644 index 000000000..ea224afae --- /dev/null +++ b/tests/idris2/reflection020/FromTTImp.idr @@ -0,0 +1,72 @@ +import Language.Reflection + +%language ElabReflection + +%TTImpLit fromTTImp + +public export +data NatExpr : Type where + Plus : NatExpr -> NatExpr -> NatExpr + Mult : NatExpr -> NatExpr -> NatExpr + Val : Nat -> NatExpr + Var : String -> NatExpr + +public export +natExpr : TTImp -> Elab NatExpr +natExpr `(~(l) + ~(r)) = [| Plus (natExpr l) (natExpr r) |] +natExpr `(~(l) * ~(r)) = [| Mult (natExpr l) (natExpr r) |] +natExpr `(fromInteger ~(IPrimVal _ (BI n))) = pure $ Val $ fromInteger n +natExpr (IVar _ (UN (Basic nm))) = pure $ Var nm +natExpr s = failAt (getFC s) "Invalid NatExpr" + +namespace AsMacro + %macro + fromTTImp : TTImp -> Elab NatExpr + fromTTImp = natExpr + + export + natExprMacroTest : NatExpr + natExprMacroTest = `(1 + 2 + x) + + export + natExprPrecedenceTest : NatExpr + natExprPrecedenceTest = `(1 + 2 * 3 + 4) + + failing "Invalid NatExpr" + natExprInvalid : NatExpr + natExprInvalid = `(f x) + +namespace AsScript + fromTTImp : TTImp -> Elab NatExpr + fromTTImp = natExpr + + export + natExprScriptTest : NatExpr + natExprScriptTest = %runElab `(3 + 4) + + failing "Invalid NatExpr" + natExprInvalid : NatExpr + natExprInvalid = %runElab `(f x) + +namespace AsFunction + public export + data IsNatExpr : TTImp -> Type where + IsPlus : IsNatExpr l -> IsNatExpr r -> IsNatExpr (IApp fc1 (IApp fc2 (IVar fc3 (UN (Basic "+"))) l) r) + IsMult : IsNatExpr l -> IsNatExpr r -> IsNatExpr (IApp fc1 (IApp fc2 (IVar fc3 (UN (Basic "*"))) l) r) + IsVal : (n : Integer) -> IsNatExpr (IApp fc1 (IVar fc2 (UN (Basic "fromInteger"))) (IPrimVal fc3 (BI n))) + + export + fromTTImp : (0 s : TTImp) -> + IsNatExpr s => + NatExpr + fromTTImp (IApp _ (IApp _ (IVar _ (UN (Basic "+"))) l) r) @{IsPlus _ _} = Plus (fromTTImp l) (fromTTImp r) + fromTTImp (IApp _ (IApp _ (IVar _ (UN (Basic "*"))) l) r) @{IsMult _ _} = Mult (fromTTImp l) (fromTTImp r) + fromTTImp (IApp _ (IVar _ (UN (Basic "fromInteger"))) (IPrimVal _ (BI n))) @{IsVal n} = Val $ cast n + + export + natExprFunctionTest : NatExpr + natExprFunctionTest = `(1 + 2 * 3 + 4) + + failing "Can't find an implementation for IsNatExpr" + natExprInvalid : NatExpr + natExprInvalid = `(f x) diff --git a/tests/idris2/reflection020/expected b/tests/idris2/reflection020/expected new file mode 100644 index 000000000..05b0be461 --- /dev/null +++ b/tests/idris2/reflection020/expected @@ -0,0 +1,23 @@ +1/1: Building FromTTImp (FromTTImp.idr) +Main> Main.AsMacro.natExprMacroTest : NatExpr +natExprMacroTest = Plus (Plus (Val 1) (Val 2)) (Var "x") +Main> Main.AsMacro.natExprPrecedenceTest : NatExpr +natExprPrecedenceTest = Plus (Plus (Val 1) (Mult (Val 2) (Val 3))) (Val 4) +Main> Main.AsScript.natExprScriptTest : NatExpr +natExprScriptTest = Plus (Val 3) (Val 4) +Main> Plus (Plus (Val 1) (Mult (Val 2) (Val 3))) (Val 4) +Main> Bye for now! +1/1: Building FromName (FromName.idr) +Main> Main.AsMacro.myNameMacroTest : MyName +myNameMacroTest = MkMyName "x" +Main> Main.AsScript.myNameScriptTest : MyName +myNameScriptTest = MkMyName "y" +Main> MkMyName "z" +Main> Bye for now! +2/2: Building FromDecls (FromDecls.idr) +Main> Main.AsMacro.natDeclsMacroTest : List NatDecl +natDeclsMacroTest = [MkNatDecl "x" (Plus (Plus (Val 1) (Val 2)) (Var "a")), MkNatDecl "y" (Plus (Plus (Val 1) (Mult (Val 2) (Val 3))) (Val 4))] +Main> Main.AsScript.natDeclsScriptTest : List NatDecl +natDeclsScriptTest = [MkNatDecl "x" (Plus (Plus (Val 1) (Mult (Val 2) (Val 3))) (Val 4))] +Main> [MkNatDecl "x" (Plus (Plus (Val 1) (Mult (Val 2) (Val 3))) (Val 4))] +Main> Bye for now! diff --git a/tests/idris2/reflection020/run b/tests/idris2/reflection020/run new file mode 100644 index 000000000..9306d1e8d --- /dev/null +++ b/tests/idris2/reflection020/run @@ -0,0 +1,23 @@ +rm -rf build + +$1 --no-color --console-width 0 --no-banner FromTTImp.idr << EOF + :printdef natExprMacroTest + :printdef natExprPrecedenceTest + :printdef natExprScriptTest + natExprFunctionTest + :q +EOF + +$1 --no-color --console-width 0 --no-banner FromName.idr << EOF + :printdef myNameMacroTest + :printdef myNameScriptTest + myNameFunctionTest + :q +EOF + +$1 --no-color --console-width 0 --no-banner FromDecls.idr << EOF + :printdef natDeclsMacroTest + :printdef natDeclsScriptTest + natDeclsFunctionTest + :q +EOF