idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-19 09:12:34 +03:00
Code Issues Projects Releases Wiki Activity
19bc798952
Idris2/tests/idris2/reflection004/refdecl.idr

50 lines
1.4 KiB
Idris
Raw Normal View History

Fix MkRecord signature Otherwise we'd get: When unifying Name and Maybe Name Mismatch between: Name and Maybe Name Can't reify as Decl
2020-06-11 22:30:16 +03:00
import Data.Nat
import Data.Vect
Add reflection operation for adding declarations Declarations can be quoted with `[ decl ]. See reflection004 for an example.
2020-06-01 17:01:52 +03:00
import Language.Reflection
%language ElabReflection
Add simple test for implicit binding around quotes
2020-08-07 03:58:02 +03:00
fc : FC
fc = EmptyFC
quoteTest : TTImp -> TTImp -> List Decl
quoteTest f arg = `[ myFunc : ~(IApp fc f arg) ]
Fix MkRecord signature Otherwise we'd get: When unifying Name and Maybe Name Mismatch between: Name and Maybe Name Can't reify as Decl
2020-06-11 22:30:16 +03:00
axes : (n : Nat) -> {auto gt : GT n 0} -> {auto lte : LTE n 4} -> Vect n String
axes 1 = ["x"]
axes 2 = "y" :: axes 1
axes 3 = "z" :: axes 2
axes 4 = "w" :: axes 3
[ fix #899 ] Be careful when generating an impossible LHS (#1081)
2021-02-22 12:53:30 +03:00
axes (S (S (S (S (S _))))) {lte} = absurd lte
Fix MkRecord signature Otherwise we'd get: When unifying Name and Maybe Name Mismatch between: Name and Maybe Name Can't reify as Decl
2020-06-11 22:30:16 +03:00
mkPoint : (n : Nat) -> {auto gt : GT n 0} -> {auto lte : LTE n 4} -> Decl
mkPoint n
= let type = "Point" ++ show n ++ "D" in
[ refactor ] introduce UserName for (UN/RF) (#1926) Instead of having UN & RF (& Hole in the near future & maybe even more later e.g. operator names) we have a single UN constructor that takes a UserName instead of a String. UserName is (for now) ```idris data UserName : Type where Basic : String -> UserName -- default name constructor e.g. map Field : String -> UserName -- field accessor e.g. .fst Underscore : UserName -- no name e.g. _ ``` This is extracted from the draft PR #1852 which is too big to easily debug. Once this is working, I can go back to it.
2021-09-15 15:20:58 +03:00
let mkMainUN = NS (MkNS ["Main"]) . UN . Basic in
[ fix #1404 ] Totality annotation for data type definitions (#2179) Co-authored-by: G. Allais <guillaume.allais@ens-lyon.org> Co-authored-by: stefan-hoeck <hock@zhaw.ch>
2021-12-08 19:08:26 +03:00
IRecord emptyFC Nothing Public Nothing
[ refactor ] introduce UserName for (UN/RF) (#1926) Instead of having UN & RF (& Hole in the near future & maybe even more later e.g. operator names) we have a single UN constructor that takes a UserName instead of a String. UserName is (for now) ```idris data UserName : Type where Basic : String -> UserName -- default name constructor e.g. map Field : String -> UserName -- field accessor e.g. .fst Underscore : UserName -- no name e.g. _ ``` This is extracted from the draft PR #1852 which is too big to easily debug. Once this is working, I can go back to it.
2021-09-15 15:20:58 +03:00
(MkRecord emptyFC (mkMainUN type) [] (mkMainUN ("Mk" ++ type))
(toList $ map (\axis => MkIField emptyFC MW ExplicitArg (UN (Field axis)) `(Double)) (axes n)))
Fix MkRecord signature Otherwise we'd get: When unifying Name and Maybe Name Mismatch between: Name and Maybe Name Can't reify as Decl
2020-06-11 22:30:16 +03:00
In reflection, check now takes a concrete type So the type of Elab now gives the expected type that's being elaborated to, meaning that we can run 'check' in the middle of scripts and use the result.
2020-06-03 00:41:37 +03:00
logDecls : TTImp -> Elab (Int -> Int)
Add reflection operation for adding declarations Declarations can be quoted with `[ decl ]. See reflection004 for an example.
2020-06-01 17:01:52 +03:00
logDecls v
= do declare [IClaim EmptyFC MW Public []
Name quotes were made to use single braces instead of double ones.
2021-01-12 15:23:28 +03:00
(MkTy EmptyFC EmptyFC `{ Main.foo }
Add reflection operation for adding declarations Declarations can be quoted with `[ decl ]. See reflection004 for an example.
2020-06-01 17:01:52 +03:00
`(Int -> Int -> Int) )]
declare `[ foo x y = x + y ]
Fix MkRecord signature Otherwise we'd get: When unifying Name and Maybe Name Mismatch between: Name and Maybe Name Can't reify as Decl
2020-06-11 22:30:16 +03:00
declare [ mkPoint 3 ]
Add reflection operation for adding declarations Declarations can be quoted with `[ decl ]. See reflection004 for an example.
2020-06-01 17:01:52 +03:00
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)
Fix MkRecord signature Otherwise we'd get: When unifying Name and Maybe Name Mismatch between: Name and Maybe Name Can't reify as Decl
2020-06-11 22:30:16 +03:00
point : Point3D
point = MkPoint3D 1.0 2.0 3.0
Reference in New Issue Copy Permalink