Add fromTTImp, fromName, and fromDecls for custom TTImp, Name, and Decls literals

This commit is contained in:
Robert Wright 2023-03-22 15:17:53 +00:00 committed by G. Allais
parent 4fcb0fb4a7
commit cbbe761c51
15 changed files with 388 additions and 30 deletions

View File

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

View File

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

View File

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

View File

@ -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 ::) }

View File

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

View File

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

View File

@ -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 ",")

View File

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

View File

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

View File

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

View File

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

View File

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

View File

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

View File

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

View File

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