idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-01 01:09:03 +03:00
Code Issues Projects Releases Wiki Activity

Merge github.com:idris-lang/Idris2 into refcount-c

Browse Source
This commit is contained in:
Edwin Brady 2020-10-11 15:12:18 +01:00
commit 2a39a6461a
46 changed files with 725 additions and 391 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
CONTRIBUTING.md
View File

@ -27,6 +27,7 @@ beyond work on the language core, are (in no particular order):
to lex!
* An alternative, high performance, back end. OCaml seems worth a try.
* JS and Node back ends would be nice.
* A Jupyter kernel for Idris, to allow for more industry standard literate programming.
The default Prelude describes the rationale for what gets included and what
doesn't. Mostly what is there is copied from Idris 1, but it's not impossible

2
docs/source/reference/index.rst
View File

@ -18,6 +18,6 @@ This is a placeholder, to get set up with readthedocs.
packages
envvars
postfixprojs
records
literate
overloadedlit

196
docs/source/reference/postfixprojs.rst
View File

@ -1,196 +0,0 @@
Postfix projections
===================
.. role:: idris(code)
:language: idris
Postfix projections are syntactic forms that represent postfix application,
such as ``person.name``. They were originally motivated by the need of dot syntax
to access fields of records, and generalised also for non-record use cases later.
The more advanced features require ``%language PostfixProjections``,
at least until it's clear whether they should be present in the language.
Lexical structure
-----------------
* ``.foo`` starting with lowercase ``f``, single identifier, and no space after dot,
is a valid lexeme, which stands for postfix application of ``foo``
* ``Foo.Bar.baz`` with uppercase ``F`` and ``B`` is one lexeme: a namespaced
identifier.
* ``Foo.Bar.baz.boo`` is two lexemes: ``Foo.Bar.baz`` and ``.boo``.
* ``foo.bar.baz`` starting with lowercase ``f`` is three lexemes: ``foo``,
``.bar``, ``.baz``
* ``.foo.bar.baz`` is three lexemes: ``.foo``, ``.bar``, ``.baz``
* ``foo . bar``, as well as ``foo. bar`` is three lexemes: ``foo``, ``.``, ``bar``,
and represents function composition as usual
* Beware that ``True.not`` is lexed as "name ``not`` in module ``True``".
If you want the postfix application of ``not`` to constructor ``True``,
you have to write ``(True).not``.
* Spaces *before* dots are optional; spaces *after* dots are forbidden
in postfix projections: ``foo. bar`` is parsed as function composition.
* All module names must start with an uppercase letter.
New syntax of ``simpleExpr``
----------------------------
Expressions binding tighter than application (``simpleExpr``),
such as variables or parenthesised expressions, have been renamed to ``simplerExpr``,
and an extra layer of postfix dot syntax has been inserted in ``simpleExpr``.
.. code-block:: idris
postfixProj ::= .ident -- identifiers need not be bracketed
| .(expr) -- arbitrary expression in brackets
simpleExpr ::= simplerExpr postfixProj+ -- postfix projection
| (postfixProj+ simpleExpr+) -- section of postfix projection
| simplerExpr -- (parses as whatever it used to)
Desugaring rules
----------------
* Postfix projections:
``simpleExpr .proj1 .proj2 .proj3`` desugars to ``(proj3 (proj2 (proj1 simpleExpr))``
* Sections of postfix projections:
``(.proj1 .proj2 .proj3 arg1 arg2)`` desugars to ``(\x => x.proj1.proj2.proj3 arg1 arg2)``
Examples of desugaring:
* ``foo.bar`` desugars as ``bar foo``
* ``True.not`` is a single lexeme: qualified name
* ``(True).not`` desugars as ``not True``
* ``(True).(not . not)`` desugars as ``(not . not) True``
* ``(not True).(not . not)`` desugars as ``(not . not) (not True)``
* ``(checkFile fileName).runState initialState`` desugars as ``runState (checkFile fileName) initialState``
* ``(MkPoint 3 4).x`` desugars as ``x (MkPoint 3 4)``
Examples of desugaring sections:
* bare ``.foo`` is invalid syntax (e.g. in ``f $ .foo``)
* ``(.foo)`` desugars as ``(\x => x.foo)``, i.e. ``(\x => foo x)``
* ``(.foo.bar m n)`` desugars as ``(\x => bar (foo x) m n)``
Example code
------------
.. code-block:: idris
record Point where
constructor MkPoint
x : Double
y : Double
This record creates two projections:
* ``x : Point -> Double``
* ``y : Point -> Double``
We add another record:
.. code-block:: idris
record Rect where
constructor MkRect
topLeft : Point
bottomRight : Point
Let's define some constants:
.. code-block:: idris
pt : Point
pt = MkPoint 4.2 6.6
rect : Rect
rect =
MkRect
(MkPoint 1.1 2.5)
(MkPoint 4.3 6.3)
squared : Num a => a -> a
squared x = x * x
Finally, some examples:
.. code-block:: idris
main : IO ()
main = do
-- desugars to (x pt)
-- prints 4.2
printLn $ pt.x
-- prints 4.2, too
-- maybe we want to make this a parse error?
printLn $ pt .x
-- prints 10.8
printLn $ pt.x + pt.y
-- works fine with namespacing
-- both print 4.2
printLn $ Main.pt.x
printLn $ (Main.pt).x
-- the LHS can be an arbitrary expression
-- prints 4.2
printLn $ (MkPoint pt.y pt.x).y
-- the RHS can be an arbitrary expression, too
-- prints 17.64
printLn $ (MkPoint pt.y pt.x).(squared . y)
-- user-defined function
-- prints 17.64
printLn $ pt.x.squared
-- prints [1.0, 3.0]
printLn $ map (.x) [MkPoint 1 2, MkPoint 3 4]
-- .topLeft.y desugars to (\x => y (topLeft x))
-- prints [2.5, 2.5]
printLn $ map (.topLeft.y) [rect, rect]
-- desugars to (.topLeft.x rect + .bottomRight.y rect)
-- prints 7.4
printLn $ rect.topLeft.x + rect.bottomRight.y
-- complex projections
-- prints 7.4
printLn $ rect.(x . topLeft) + rect.(y . bottomRight)
-- haskell-style projections
printLn $ Main.Point.x pt
printLn $ Point.x pt
printLn $ (x) pt
printLn $ x pt
-- record update syntax uses dots now
-- prints 3.0
printLn $ (record { topLeft.x = 3 } rect).topLeft.x
-- but for compatibility, we support the old syntax, too
printLn $ (record { topLeft->x = 3 } rect).topLeft.x
-- prints 2.1
printLn $ (record { topLeft.x $= (+1) } rect).topLeft.x
printLn $ (record { topLeft->x $= (+1) } rect).topLeft.x
Parses but does not typecheck:
.. code-block:: idris
-- parses as: map.x [MkPoint 1 2, MkPoint 3 4]
-- maybe we should disallow spaces before dots?
--
printLn $ map .x [MkPoint 1 2, MkPoint 3 4]

195
docs/source/reference/records.rst Normal file
View File

@ -0,0 +1,195 @@
Dot syntax for records
======================
.. role:: idris(code)
:language: idris
Long story short, ``.field`` is a postfix projection operator that binds
tighter than function application.
Lexical structure
-----------------
* ``.foo`` is a valid name, which stands for record fields (new ``Name``
constructor ``RF "foo"``)
* ``Foo.bar.baz`` starting with uppercase ``F`` is one lexeme, a namespaced
identifier: ``DotSepIdent ["baz", "bar", "Foo"]``
* ``foo.bar.baz`` starting with lowercase ``f`` is three lexemes: ``foo``,
``.bar``, ``.baz``
* ``.foo.bar.baz`` is three lexemes: ``.foo``, ``.bar``, ``.baz``
* If you want ``Constructor.field``, you have to write ``(Constructor).field``.
* All module names must start with an uppercase letter.
New syntax of ``simpleExpr``
----------------------------
Expressions binding tighter than application (``simpleExpr``), such as variables or parenthesised expressions, have been renamed to ``simplerExpr``, and an extra layer of syntax has been inserted.
.. code-block:: idris
simpleExpr ::= (.field)+ -- parses as PPostfixAppPartial
| simplerExpr (.field)+ -- parses as PPostfixApp
| simplerExpr -- (parses as whatever it used to)
* ``(.foo)`` is a name, so you can use it to e.g. define a function called
``.foo`` (see ``.squared`` below)
* ``(.foo.bar)`` is a parenthesised expression
Desugaring rules
----------------
* ``(.field1 .field2 .field3)`` desugars to ``(\x => .field3 (.field2 (.field1
x)))``
* ``(simpleExpr .field1 .field2 .field3)`` desugars to ``((.field .field2
.field3) simpleExpr)``
Record elaboration
------------------
* there is a new pragma ``%prefix_record_projections``, which is ``on`` by
default
* for every field ``f`` of a record ``R``, we get:
* projection ``f`` in namespace ``R`` (exactly like now), unless
``%prefix_record_projections`` is ``off``
* projection ``.f`` in namespace ``R`` with the same definition
Example code
------------
.. code-block:: idris
record Point where
constructor MkPoint
x : Double
y : Double
This record creates two projections:
* ``.x : Point -> Double``
* ``.y : Point -> Double``
Because ``%prefix_record_projections`` are ``on`` by default, we also get:
* ``x : Point -> Double``
* ``y : Point -> Double``
To prevent cluttering the ordinary global name space with short identifiers, we can do this:
.. code-block:: idris
%prefix_record_projections off
record Rect where
constructor MkRect
topLeft : Point
bottomRight : Point
For ``Rect``, we don't get the prefix projections:
.. code-block:: idris
Main> :t topLeft
(interactive):1:4--1:11:Undefined name topLeft
Main> :t .topLeft
\{rec:0} => .topLeft rec : ?_ -> Point
Let's define some constants:
.. code-block:: idris
pt : Point
pt = MkPoint 4.2 6.6
rect : Rect
rect =
MkRect
(MkPoint 1.1 2.5)
(MkPoint 4.3 6.3)
User-defined projections work, too. (Should they?)
.. code-block:: idris
(.squared) : Double -> Double
(.squared) x = x * x
Finally, the examples:
.. code-block:: idris
main : IO ()
main = do
-- desugars to (.x pt)
-- prints 4.2
printLn $ pt.x
-- prints 4.2, too
-- maybe we want to make this a parse error?
printLn $ pt .x
-- prints 10.8
printLn $ pt.x + pt.y
-- works fine with namespacing
-- prints 4.2
printLn $ (Main.pt).x
-- the LHS can be an arbitrary expression
-- prints 4.2
printLn $ (MkPoint pt.y pt.x).y
-- user-defined projection
-- prints 17.64
printLn $ pt.x.squared
-- prints [1.0, 3.0]
printLn $ map (.x) [MkPoint 1 2, MkPoint 3 4]
-- .topLeft.y desugars to (\x => .y (.topLeft x))
-- prints [2.5, 2.5]
printLn $ map (.topLeft.y) [rect, rect]
-- desugars to (.topLeft.x rect + .bottomRight.y rect)
-- prints 7.4
printLn $ rect.topLeft.x + rect.bottomRight.y
-- qualified names work, too
-- all these print 4.2
printLn $ Main.Point.(.x) pt
printLn $ Point.(.x) pt
printLn $ (.x) pt
printLn $ .x pt
-- haskell-style projections work, too
printLn $ Main.Point.x pt
printLn $ Point.x pt
printLn $ (x) pt
printLn $ x pt
-- record update syntax uses dots now
-- prints 3.0
printLn $ (record { topLeft.x = 3 } rect).topLeft.x
-- but for compatibility, we support the old syntax, too
printLn $ (record { topLeft->x = 3 } rect).topLeft.x
-- prints 2.1
printLn $ (record { topLeft.x $= (+1) } rect).topLeft.x
printLn $ (record { topLeft->x $= (+1) } rect).topLeft.x
Parses but does not typecheck:
.. code-block:: idris
-- parses as: map.x [MkPoint 1 2, MkPoint 3 4]
-- maybe we should disallow spaces before dots?
--
printLn $ map .x [MkPoint 1 2, MkPoint 3 4]

12
docs/source/tutorial/typesfuns.rst
View File

@ -988,8 +988,8 @@ type. The field names can be used to access the field values:
"Fred" : String
*Record> fred.age
30 : Int
*Record> :t firstName
firstName : Person -> String
*Record> :t (.firstName)
Main.Person.(.firstName) : Person -> String
We can use prefix field projections, like in Haskell:
@ -999,6 +999,14 @@ We can use prefix field projections, like in Haskell:
"Fred" : String
*Record> age fred
30 : Int
*Record> :t firstName
firstName : Person -> String
Prefix field projections can be disabled per record definition
using pragma ``%prefix_record_projections off``, which makes
all subsequently defined records generate only dotted projections.
This pragma has effect until the end of the module
or until the closest occurrence of ``%prefix_record_projections on``.
We can also use the field names to update a record (or, more
precisely, produce a copy of the record with the given fields

14
libs/base/Data/Strings.idr
View File

@ -16,11 +16,21 @@ partial
foldl1 : (a -> a -> a) -> List a -> a
foldl1 f (x::xs) = foldl f x xs
-- This function runs fast when compiled but won't compute at compile time.
-- If you need to unpack strings at compile time, use Prelude.unpack.
%foreign
"scheme:string-unpack"
export
fastUnpack : String -> List Char
-- This works quickly because when string-concat builds the result, it allocates
-- enough room in advance so there's only one allocation, rather than lots!
--
-- Like fastUnpack, this function won't reduce at compile time.
-- If you need to concatenate strings at compile time, use Prelude.concat.
%foreign
"scheme:string-concat"
"javascript:lambda:(xs)=>''.concat(...__prim_idris2js_array(xs))"
"scheme:string-concat"
"javascript:lambda:(xs)=>''.concat(...__prim_idris2js_array(xs))"
export
fastConcat : List String -> String

2
libs/base/Language/Reflection/TT.idr
View File

@ -64,6 +64,7 @@ data Name = UN String -- user defined name
| MN String Int -- machine generated name
| NS Namespace Name -- name in a namespace
| DN String Name -- a name and how to display it
| RF String -- record field name
export
Show Name where
@ -71,6 +72,7 @@ Show Name where
show (UN x) = x
show (MN x y) = "{" ++ x ++ ":" ++ show y ++ "}"
show (DN str y) = str
show (RF n) = "." ++ n
public export
data Count = M0 | M1 | MW

55
libs/contrib/Data/List/Lazy.idr Normal file
View File

@ -0,0 +1,55 @@
module Data.List.Lazy
%default total
-- All functions here are public export
-- because their definitions are pretty much the specification.
public export
data LazyList : Type -> Type where
Nil : LazyList a
(::) : (1 x : a) -> (1 xs : Lazy (LazyList a)) -> LazyList a
public export
Semigroup (LazyList a) where
[] <+> ys = ys
(x :: xs) <+> ys = x :: (xs <+> ys)
public export
Monoid (LazyList a) where
neutral = []
public export
Foldable LazyList where
foldr op nil [] = nil
foldr op nil (x :: xs) = x `op` foldr op nil xs
foldl op acc [] = acc
foldl op acc (x :: xs) = foldl op (acc `op` x) xs
public export
Functor LazyList where
map f [] = []
map f (x :: xs) = f x :: map f xs
public export
Applicative LazyList where
pure x = [x]
fs <*> vs = concatMap (\f => map f vs) fs
public export
Alternative LazyList where
empty = []
(<|>) = (<+>)
public export
Monad LazyList where
m >>= f = concatMap f m
-- There is no Traversable instance for lazy lists.
-- The result of a traversal will be a non-lazy list in general
-- (you can't delay the "effect" of an applicative functor).
public export
traverse : Applicative f => (a -> f b) -> LazyList a -> f (List b)
traverse g [] = pure []
traverse g (x :: xs) = [| g x :: traverse g xs |]

8
libs/contrib/Data/SortedSet.idr
View File

@ -65,3 +65,11 @@ Ord k => Monoid (SortedSet k) where
export
keySet : SortedMap k v -> SortedSet k
keySet = SetWrapper . map (const ())
export
singleton : Ord k => k -> SortedSet k
singleton k = insert k empty
export
null : SortedSet k -> Bool
null (SetWrapper m) = SortedMap.null m

74
libs/contrib/Data/String/Iterator.idr Normal file
View File

@ -0,0 +1,74 @@
module Data.String.Iterator
import public Data.List.Lazy
%default total
-- Backend-dependent string iteration type,
-- parameterised by the string that it iterates over.
--
-- Beware: the index is checked only up to definitional equality.
-- In theory, you could run `decEq` on two strings
-- with the same content but allocated in different memory locations
-- and use the obtained Refl to coerce iterators between them.
--
-- The strictly correct solution is to make the iterators independent
-- from the exact memory location of the string given to `uncons`.
-- (For example, byte offsets satisfy this requirement.)
export
data StringIterator : String -> Type where [external]
-- This function is private
-- to avoid subverting the linearity guarantees of withString.
%foreign
"scheme:blodwen-string-iterator-new"
"javascript:stringIterator:new"
private
fromString : (str : String) -> StringIterator str
-- This function uses a linear string iterator
-- so that backends can use mutating iterators.
export
withString : (str : String) -> ((1 it : StringIterator str) -> a) -> a
withString str f = f (fromString str)
-- We use a custom data type instead of Maybe (Char, StringIterator)
-- to remove one level of pointer indirection
-- in every iteration of something that's likely to be a hot loop,
-- and to avoid one allocation per character.
--
-- The Char field of Character is unrestricted for flexibility.
public export
data UnconsResult : String -> Type where
EOF : UnconsResult str
Character : (c : Char) -> (1 it : StringIterator str) -> UnconsResult str
-- We pass the whole string to the uncons function
-- to avoid yet another allocation per character
-- because for many backends, StringIterator can be simply an integer
-- (e.g. byte offset into an UTF-8 string).
%foreign
"scheme:blodwen-string-iterator-next"
"javascript:stringIterator:next"
export
uncons : (str : String) -> (1 it : StringIterator str) -> UnconsResult str
export
foldl : (accTy -> Char -> accTy) -> accTy -> String -> accTy
foldl op acc str = withString str (loop acc)
where
loop : accTy -> (1 it : StringIterator str) -> accTy
loop acc it =
case uncons str it of
EOF => acc
Character c it' => loop (acc `op` c) (assert_smaller it it')
export
unpack : String -> LazyList Char
unpack str = withString str unpack'
where
unpack' : (1 it : StringIterator str) -> LazyList Char
unpack' it =
case uncons str it of
EOF => []
Character c it' => c :: Delay (unpack' $ assert_smaller it it')

4
libs/contrib/Text/Lexer/Core.idr
View File

@ -199,13 +199,13 @@ tokenise pred line col acc tmap str
export
lex : TokenMap a -> String -> (List (TokenData a), (Int, Int, String))
lex tmap str
= let (ts, (l, c, str')) = tokenise (const False) 0 0 [] tmap (unpack str) in
= let (ts, (l, c, str')) = tokenise (const False) 0 0 [] tmap (fastUnpack str) in
(ts, (l, c, pack str'))
export
lexTo : (TokenData a -> Bool) ->
TokenMap a -> String -> (List (TokenData a), (Int, Int, String))
lexTo pred tmap str
= let (ts, (l, c, str')) = tokenise pred 0 0 [] tmap (unpack str) in
= let (ts, (l, c, str')) = tokenise pred 0 0 [] tmap (fastUnpack str) in
(ts, (l, c, pack str'))

2
libs/contrib/contrib.ipkg
View File

@ -21,6 +21,7 @@ modules = Control.ANSI,
Data.List.TailRec,
Data.List.Equalities,
Data.List.Reverse,
Data.List.Lazy,
Data.List.Views.Extra,
Data.List.Palindrome,
@ -48,6 +49,7 @@ modules = Control.ANSI,
Data.Stream.Extra,
Data.String.Extra,
Data.String.Interpolation,
Data.String.Iterator,
Data.String.Parser,
Data.String.Parser.Expression,

25
libs/network/Network/Socket/Data.idr
View File

@ -110,14 +110,27 @@ Show SocketFamily where
show AF_INET = "AF_INET"
show AF_INET6 = "AF_INET6"
-- This is a bit of a hack to get the OS-dependent magic constants out of C and
-- into Idris without having to faff around on the preprocessor on the Idris
-- side.
%foreign "C:idrnet_af_unspec,libidris2_support"
prim__idrnet_af_unspec : PrimIO Int
%foreign "C:idrnet_af_unix,libidris2_support"
prim__idrnet_af_unix : PrimIO Int
%foreign "C:idrnet_af_inet,libidris2_support"
prim__idrnet_af_inet : PrimIO Int
%foreign "C:idrnet_af_inet6,libidris2_support"
prim__idrnet_af_inet6 : PrimIO Int
export
ToCode SocketFamily where
-- Don't know how to read a constant value from C code in idris2...
-- gotta to hardcode those for now
toCode AF_UNSPEC = 0 -- unsafePerformIO (cMacro "#AF_UNSPEC" Int)
toCode AF_UNIX = 1
toCode AF_INET = 2
toCode AF_INET6 = 10
toCode AF_UNSPEC = unsafePerformIO $ primIO $ prim__idrnet_af_unspec
toCode AF_UNIX = unsafePerformIO $ primIO $ prim__idrnet_af_unix
toCode AF_INET = unsafePerformIO $ primIO $ prim__idrnet_af_inet
toCode AF_INET6 = unsafePerformIO $ primIO $ prim__idrnet_af_inet6
export
getSocketFamily : Int -> Maybe SocketFamily

30
src/Compiler/ES/ES.idr
View File

@ -73,6 +73,28 @@ addSupportToPreamble : {auto c : Ref ESs ESSt} -> String -> String -> Core Strin
addSupportToPreamble name code =
addToPreamble name name code
addStringIteratorToPreamble : {auto c : Ref ESs ESSt} -> Core String
addStringIteratorToPreamble =
do
let defs = "
function __prim_stringIteratorNew(str) {
return str[Symbol.iterator]();
}
function __prim_stringIteratorNext(str, it) {
const char = it.next();
if (char.done) {
return {h: 0}; // EOF
} else {
return {
h: 1, // Character
a1: char.value,
a2: it
};
}
}"
let name = "stringIterator"
let newName = esName name
addToPreamble name newName defs
jsIdent : String -> String
jsIdent s = concatMap okchar (unpack s)
@ -92,6 +114,7 @@ jsName (UN n) = keywordSafe $ jsIdent n
jsName (MN n i) = jsIdent n ++ "_" ++ show i
jsName (PV n d) = "pat__" ++ jsName n
jsName (DN _ n) = jsName n
jsName (RF n) = "rf__" ++ jsIdent n
jsName (Nested (i, x) n) = "n__" ++ show i ++ "_" ++ show x ++ "_" ++ jsName n
jsName (CaseBlock x y) = "case__" ++ jsIdent x ++ "_" ++ show y
jsName (WithBlock x y) = "with__" ++ jsIdent x ++ "_" ++ show y
@ -311,6 +334,13 @@ makeForeign n x =
lib_code <- readDataFile ("js/" ++ lib ++ ".js")
addSupportToPreamble lib lib_code
pure $ "const " ++ jsName n ++ " = " ++ lib ++ "_" ++ name ++ "\n"
"stringIterator" =>
do
addStringIteratorToPreamble
case def of
"new" => pure $ "const " ++ jsName n ++ " = __prim_stringIteratorNew;\n"
"next" => pure $ "const " ++ jsName n ++ " = __prim_stringIteratorNext;\n"
_ => throw (InternalError $ "invalid string iterator function: " ++ def ++ ", supported functions are \"new\", \"next\"")
_ => throw (InternalError $ "invalid foreign type : " ++ ty ++ ", supported types are \"lambda\", \"lambdaRequire\", \"support\"")

1
src/Compiler/Scheme/Common.idr
View File

@ -36,6 +36,7 @@ schName (UN n) = schString n
schName (MN n i) = schString n ++ "-" ++ show i
schName (PV n d) = "pat--" ++ schName n
schName (DN _ n) = schName n
schName (RF n) = "rf--" ++ schString n
schName (Nested (i, x) n) = "n--" ++ show i ++ "-" ++ show x ++ "-" ++ schName n
schName (CaseBlock x y) = "case--" ++ schString x ++ "-" ++ show y
schName (WithBlock x y) = "with--" ++ schString x ++ "-" ++ show y

2
src/Core/Binary.idr
View File

@ -31,7 +31,7 @@ import Data.Buffer
-- TTC files can only be compatible if the version number is the same
export
ttcVersion : Int
ttcVersion = 41
ttcVersion = 42
export
checkTTCVersion : String -> Int -> Int -> Core ()

18
src/Core/Context.idr
View File

@ -361,7 +361,7 @@ initCtxtS : Int -> Core Context
initCtxtS s
= do arr <- coreLift $ newArray s
aref <- newRef Arr arr
pure (MkContext 0 0 empty empty aref 0 empty [partialEvalNS] False False empty)
pure $ MkContext 0 0 empty empty aref 0 empty [partialEvalNS] False False empty
export
initCtxt : Core Context
@ -1299,6 +1299,8 @@ visibleInAny nss n vis = any (\ns => visibleIn ns n vis) nss
reducibleIn : Namespace -> Name -> Visibility -> Bool
reducibleIn nspace (NS ns (UN n)) Export = isParentOf ns nspace
reducibleIn nspace (NS ns (UN n)) Private = isParentOf ns nspace
reducibleIn nspace (NS ns (RF n)) Export = isParentOf ns nspace
reducibleIn nspace (NS ns (RF n)) Private = isParentOf ns nspace
reducibleIn nspace n _ = True
export
@ -1806,6 +1808,9 @@ inCurrentNS n@(MN _ _)
inCurrentNS n@(DN _ _)
= do defs <- get Ctxt
pure (NS (currentNS defs) n)
inCurrentNS n@(RF _)
= do defs <- get Ctxt
pure (NS (currentNS defs) n)
inCurrentNS n = pure n
export
@ -2012,6 +2017,12 @@ setUnboundImplicits a
= do defs <- get Ctxt
put Ctxt (record { options->elabDirectives->unboundImplicits = a } defs)
export
setPrefixRecordProjections : {auto c : Ref Ctxt Defs} -> Bool -> Core ()
setPrefixRecordProjections b = do
defs <- get Ctxt
put Ctxt (record { options->elabDirectives->prefixRecordProjections = b } defs)
export
setDefaultTotalityOption : {auto c : Ref Ctxt Defs} ->
TotalReq -> Core ()
@ -2047,6 +2058,11 @@ isUnboundImplicits
= do defs <- get Ctxt
pure (unboundImplicits (elabDirectives (options defs)))
export
isPrefixRecordProjections : {auto c : Ref Ctxt Defs} -> Core Bool
isPrefixRecordProjections =
prefixRecordProjections . elabDirectives . options <$> get Ctxt
export
getDefaultTotalityOption : {auto c : Ref Ctxt Defs} ->
Core TotalReq

12
src/Core/Hash.idr
View File

@ -5,7 +5,9 @@ import Core.TT
import Data.List
import Data.List1
import Data.List.Lazy
import Data.Strings
import Data.String.Iterator
%default covering
@ -56,15 +58,7 @@ Hashable a => Hashable (Maybe a) where
export
Hashable String where
hashWithSalt h str = hashChars h 0 (cast (length str)) str
where
hashChars : Int -> Int -> Int -> String -> Int
hashChars h p len str
= assert_total $
if p == len
then h
else hashChars (h * 33 + cast (strIndex str p))
(p + 1) len str
hashWithSalt h = String.Iterator.foldl hashWithSalt h
export
Hashable Namespace where

21
src/Core/Name.idr
View File

@ -19,6 +19,7 @@ data Name : Type where
MN : String -> Int -> Name -- machine generated name
PV : Name -> Int -> Name -- pattern variable name; int is the resolved function id
DN : String -> Name -> Name -- a name and how to display it
RF : String -> Name -- record field name
Nested : (Int, Int) -> Name -> Name -- nested function name
CaseBlock : String -> Int -> Name -- case block nested in (resolved) name
WithBlock : String -> Int -> Name -- with block nested in (resolved) name
@ -57,6 +58,7 @@ userNameRoot : Name -> Maybe String
userNameRoot (NS _ n) = userNameRoot n
userNameRoot (UN n) = Just n
userNameRoot (DN _ n) = userNameRoot n
userNameRoot (RF n) = Just ("." ++ n) -- TMP HACK
userNameRoot _ = Nothing
export
@ -74,6 +76,7 @@ nameRoot (UN n) = n
nameRoot (MN n _) = n
nameRoot (PV n _) = nameRoot n
nameRoot (DN _ n) = nameRoot n
nameRoot (RF n) = n
nameRoot (Nested _ inner) = nameRoot inner
nameRoot (CaseBlock n _) = "$" ++ show n
nameRoot (WithBlock n _) = "$" ++ show n
@ -93,11 +96,13 @@ dropAllNS n = n
export
Show Name where
show (NS ns n@(RF _)) = show ns ++ ".(" ++ show n ++ ")"
show (NS ns n) = show ns ++ "." ++ show n
show (UN x) = x
show (MN x y) = "{" ++ x ++ ":" ++ show y ++ "}"
show (PV n d) = "{P:" ++ show n ++ ":" ++ show d ++ "}"
show (DN str n) = str
show (RF n) = "." ++ n
show (Nested (outer, idx) inner)
= show outer ++ ":" ++ show idx ++ ":" ++ show inner
show (CaseBlock outer i) = "case block in " ++ outer
@ -106,11 +111,13 @@ Show Name where
export
Pretty Name where
pretty (NS ns n@(RF _)) = pretty ns <+> dot <+> parens (pretty n)
pretty (NS ns n) = pretty ns <+> dot <+> pretty n
pretty (UN x) = pretty x
pretty (MN x y) = braces (pretty x <+> colon <+> pretty y)
pretty (PV n d) = braces (pretty 'P' <+> colon <+> pretty n <+> colon <+> pretty d)
pretty (DN str _) = pretty str
pretty (RF n) = "." <+> pretty n
pretty (Nested (outer, idx) inner) = pretty outer <+> colon <+> pretty idx <+> colon <+> pretty inner
pretty (CaseBlock outer _) = reflow "case block in" <++> pretty outer
pretty (WithBlock outer _) = reflow "with block in" <++> pretty outer
@ -123,6 +130,7 @@ Eq Name where
(==) (MN x y) (MN x' y') = y == y' && x == x'
(==) (PV x y) (PV x' y') = x == x' && y == y'
(==) (DN _ n) (DN _ n') = n == n'
(==) (RF n) (RF n') = n == n'
(==) (Nested x y) (Nested x' y') = x == x' && y == y'
(==) (CaseBlock x y) (CaseBlock x' y') = y == y' && x == x'
(==) (WithBlock x y) (WithBlock x' y') = y == y' && x == x'
@ -135,10 +143,11 @@ nameTag (UN _) = 1
nameTag (MN _ _) = 2
nameTag (PV _ _) = 3
nameTag (DN _ _) = 4
nameTag (Nested _ _) = 5
nameTag (CaseBlock _ _) = 6
nameTag (WithBlock _ _) = 7
nameTag (Resolved _) = 8
nameTag (RF _) = 5
nameTag (Nested _ _) = 6
nameTag (CaseBlock _ _) = 7
nameTag (WithBlock _ _) = 8
nameTag (Resolved _) = 9
export
Ord Name where
@ -161,6 +170,7 @@ Ord Name where
GT => GT
LT => LT
compare (DN _ n) (DN _ n') = compare n n'
compare (RF n) (RF n') = compare n n'
compare (Nested x y) (Nested x' y')
= case compare y y' of
EQ => compare x x'
@ -206,6 +216,9 @@ nameEq (DN x t) (DN y t') with (decEq x y)
nameEq (DN y t) (DN y t) | (Yes Refl) | (Just Refl) = Just Refl
nameEq (DN y t) (DN y t') | (Yes Refl) | Nothing = Nothing
nameEq (DN x t) (DN y t') | (No p) = Nothing
nameEq (RF x) (RF y) with (decEq x y)
nameEq (RF y) (RF y) | (Yes Refl) = Just Refl
nameEq (RF x) (RF y) | (No contra) = Nothing
nameEq (Nested x y) (Nested x' y') with (decEq x x')
nameEq (Nested x y) (Nested x' y') | (No p) = Nothing
nameEq (Nested x y) (Nested x y') | (Yes Refl) with (nameEq y y')

9
src/Core/Options.idr
View File

@ -101,13 +101,11 @@ public export
data LangExt
= ElabReflection
| Borrowing -- not yet implemented
| PostfixProjections
export
Eq LangExt where
ElabReflection == ElabReflection = True
Borrowing == Borrowing = True
PostfixProjections == PostfixProjections = True
_ == _ = False
-- Other options relevant to the current session (so not to be saved in a TTC)
@ -119,6 +117,11 @@ record ElabDirectives where
totality : TotalReq
ambigLimit : Nat
autoImplicitLimit : Nat
--
-- produce traditional (prefix) record projections,
-- in addition to postfix (dot) projections
-- default: yes
prefixRecordProjections : Bool
public export
record Session where
@ -186,7 +189,7 @@ defaultSession = MkSessionOpts False False False Chez [] defaultLogLevel
export
defaultElab : ElabDirectives
defaultElab = MkElabDirectives True True CoveringOnly 3 50
defaultElab = MkElabDirectives True True CoveringOnly 3 50 True
export
defaults : Options

6
src/Core/Reflect.idr
View File

@ -272,6 +272,9 @@ Reify Name where
=> do str' <- reify defs !(evalClosure defs str)
n' <- reify defs !(evalClosure defs n)
pure (DN str' n')
(NS _ (UN "RF"), [str])
=> do str' <- reify defs !(evalClosure defs str)
pure (RF str')
_ => cantReify val "Name"
reify defs val = cantReify val "Name"
@ -292,6 +295,9 @@ Reflect Name where
= do str' <- reflect fc defs lhs env str
n' <- reflect fc defs lhs env n
appCon fc defs (reflectiontt "DN") [str', n']
reflect fc defs lhs env (RF x)
= do x' <- reflect fc defs lhs env x
appCon fc defs (reflectiontt "RF") [x']
reflect fc defs lhs env (Resolved i)
= case !(full (gamma defs) (Resolved i)) of
Resolved _ => cantReflect fc "Name"

15
src/Core/TTC.idr
View File

@ -47,9 +47,10 @@ TTC Name where
toBuf b (MN x y) = do tag 2; toBuf b x; toBuf b y
toBuf b (PV x y) = do tag 3; toBuf b x; toBuf b y
toBuf b (DN x y) = do tag 4; toBuf b x; toBuf b y
toBuf b (Nested x y) = do tag 5; toBuf b x; toBuf b y
toBuf b (CaseBlock x y) = do tag 6; toBuf b x; toBuf b y
toBuf b (WithBlock x y) = do tag 7; toBuf b x; toBuf b y
toBuf b (RF x) = do tag 5; toBuf b x
toBuf b (Nested x y) = do tag 6; toBuf b x; toBuf b y
toBuf b (CaseBlock x y) = do tag 7; toBuf b x; toBuf b y
toBuf b (WithBlock x y) = do tag 8; toBuf b x; toBuf b y
toBuf b (Resolved x)
= throw (InternalError ("Can't write resolved name " ++ show x))
@ -70,12 +71,14 @@ TTC Name where
y <- fromBuf b
pure (DN x y)
5 => do x <- fromBuf b
y <- fromBuf b
pure (Nested x y)
pure (RF x)
6 => do x <- fromBuf b
y <- fromBuf b
pure (CaseBlock x y)
pure (Nested x y)
7 => do x <- fromBuf b
y <- fromBuf b
pure (CaseBlock x y)
8 => do x <- fromBuf b
y <- fromBuf b
pure (WithBlock x y)
_ => corrupt "Name"

1
src/Core/UnifyState.idr
View File

@ -125,6 +125,7 @@ genMVName : {auto c : Ref Ctxt Defs} ->
Name -> Core Name
genMVName (UN str) = genName str
genMVName (MN str _) = genName str
genMVName (RF str) = genName str
genMVName n
= do ust <- get UST
put UST (record { nextName $= (+1) } ust)

7
src/Data/StringMap.idr
View File

@ -293,6 +293,13 @@ export
mergeLeft : StringMap v -> StringMap v -> StringMap v
mergeLeft x y = mergeWith const x y
export
adjust : String -> (v -> v) -> StringMap v -> StringMap v
adjust k f m =
case lookup k m of
Nothing => m
Just v => insert k (f v) m
export
Show v => Show (StringMap v) where
show m = show $ map {b=String} (\(k,v) => k ++ "->" ++ show v) $ toList m

43
src/Idris/Desugar.idr
View File

@ -351,43 +351,12 @@ mutual
desugarB side ps (PApp fc (PApp fc (PRef fc (UN "rangeFromThen")) start) n)
desugarB side ps (PUnifyLog fc lvl tm)
= pure $ IUnifyLog fc lvl !(desugarB side ps tm)
desugarB side ps (PPostfixProjs fc rec projs)
= do
let isPRef = \case
PRef _ _ => True
_ => False
defs <- get Ctxt
when (not (isExtension PostfixProjections defs) && not (all isPRef projs)) $
throw (GenericMsg fc "complex postfix projections require %language PostfixProjections")
desugarB side ps $ foldl (\x, proj => PApp fc proj x) rec projs
desugarB side ps (PPostfixProjsSection fc projs args)
= do
let isPRef = \case
PRef _ _ => True
_ => False
defs <- get Ctxt
when (not (isExtension PostfixProjections defs)) $ do
when (not (all isPRef projs)) $
throw (GenericMsg fc "complex postfix projections require %language PostfixProjections")
case args of
[] => pure ()
_ => throw $ GenericMsg fc "postfix projection sections require %language PostfixProjections"
desugarB side ps $
desugarB side ps (PPostfixApp fc rec projs)
= desugarB side ps $ foldl (\x, proj => PApp fc (PRef fc proj) x) rec projs
desugarB side ps (PPostfixAppPartial fc projs)
= desugarB side ps $
PLam fc top Explicit (PRef fc (MN "paRoot" 0)) (PImplicit fc) $
foldl
(\r, arg => PApp fc r arg)
(foldl
(\r, proj => PApp fc proj r)
(PRef fc (MN "paRoot" 0))
projs)
args
foldl (\r, proj => PApp fc (PRef fc proj) r) (PRef fc (MN "paRoot" 0)) projs
desugarB side ps (PWithUnambigNames fc ns rhs)
= IWithUnambigNames fc ns <$> desugarB side ps rhs
@ -857,6 +826,8 @@ mutual
UnboundImplicits a => do
setUnboundImplicits a
pure [IPragma (\nest, env => setUnboundImplicits a)]
PrefixRecordProjections b => do
pure [IPragma (\nest, env => setPrefixRecordProjections b)]
AmbigDepth n => pure [IPragma (\nest, env => setAmbigLimit n)]
AutoImplicitDepth n => pure [IPragma (\nest, env => setAutoImplicitLimit n)]
PairNames ty f s => pure [IPragma (\nest, env => setPair fc ty f s)]

27
src/Idris/Parser.idr
View File

@ -241,10 +241,9 @@ mutual
(op, e) <- pure b.val
pure (PSectionL (boundToFC fname (mergeBounds s b)) op e)
<|> do -- (.y.z) -- section of projection (chain)
b <- bounds (MkPair <$> (some $ postfixApp fname indents) <*> (many $ simpleExpr fname indents))
(projs, args) <- pure b.val
b <- bounds $ some postfixProj
symbol ")"
pure $ PPostfixProjsSection (boundToFC fname b) projs args
pure $ PPostfixAppPartial (boundToFC fname b) b.val
-- unit type/value
<|> do b <- bounds (continueWith indents ")")
pure (PUnit (boundToFC fname (mergeBounds s b)))
@ -340,22 +339,24 @@ mutual
<|> do end <- bounds (continueWith indents ")")
pure (PBracketed (boundToFC fname (mergeBounds s end)) e)
postfixApp : FileName -> IndentInfo -> Rule PTerm
postfixApp fname indents
= do di <- bounds dotIdent
postfixProjection : FileName -> IndentInfo -> Rule PTerm
postfixProjection fname indents
= do di <- bounds postfixProj
pure $ PRef (boundToFC fname di) di.val
<|> (symbol ".(" *> commit *> expr pdef fname indents <* symbol ")")
simpleExpr : FileName -> IndentInfo -> Rule PTerm
simpleExpr fname indents
= do -- x.y.z
b <- bounds (do root <- simplerExpr fname indents
projs <- many $ postfixApp fname indents
projs <- many postfixProj
pure (root, projs))
(root, projs) <- pure b.val
pure $ case projs of
[] => root
_ => PPostfixProjs (boundToFC fname b) root projs
_ => PPostfixApp (boundToFC fname b) root projs
<|> do
b <- bounds (some postfixProj)
pure $ PPostfixAppPartial (boundToFC fname b) b.val
simplerExpr : FileName -> IndentInfo -> Rule PTerm
simplerExpr fname indents
@ -631,12 +632,13 @@ mutual
where
fieldName : Name -> String
fieldName (UN s) = s
fieldName (RF s) = s
fieldName _ = "_impossible"
-- this allows the dotted syntax .field
-- but also the arrowed syntax ->field for compatibility with Idris 1
recFieldCompat : Rule Name
recFieldCompat = dotIdent <|> (symbol "->" *> name)
recFieldCompat = postfixProj <|> (symbol "->" *> name)
rewrite_ : FileName -> IndentInfo -> Rule PTerm
rewrite_ fname indents
@ -932,7 +934,6 @@ onoff
extension : Rule LangExt
extension
= (exactIdent "ElabReflection" *> pure ElabReflection)
<|> (exactIdent "PostfixProjections" *> pure PostfixProjections)
<|> (exactIdent "Borrowing" *> pure Borrowing)
totalityOpt : Rule TotalReq
@ -964,6 +965,10 @@ directive fname indents
b <- onoff
atEnd indents
pure (UnboundImplicits b)
<|> do pragma "prefix_record_projections"
b <- onoff
atEnd indents
pure (PrefixRecordProjections b)
<|> do pragma "ambiguity_depth"
lvl <- intLit
atEnd indents

8
src/Idris/Pretty.idr
View File

@ -277,10 +277,10 @@ mutual
go d (PRangeStream _ start (Just next)) =
brackets (go startPrec start <+> comma <++> go startPrec next <++> pretty "..")
go d (PUnifyLog _ lvl tm) = go d tm
go d (PPostfixProjs fc rec fields) =
parenthesise (d > appPrec) $ go startPrec rec <++> dot <+> concatWith (surround dot) (go startPrec <$> fields)
go d (PPostfixProjsSection fc fields args) =
parens (dot <+> concatWith (surround dot) (go startPrec <$> fields) <+> fillSep (go appPrec <$> args))
go d (PPostfixApp fc rec fields) =
parenthesise (d > appPrec) $ go startPrec rec <++> dot <+> concatWith (surround dot) (map pretty fields)
go d (PPostfixAppPartial fc fields) =
parens (dot <+> concatWith (surround dot) (map pretty fields))
go d (PWithUnambigNames fc ns rhs) = parenthesise (d > appPrec) $ group $ with_ <++> pretty ns <+> line <+> go startPrec rhs
export

31
src/Idris/Syntax.idr
View File

@ -93,10 +93,10 @@ mutual
PRange : FC -> PTerm -> Maybe PTerm -> PTerm -> PTerm
-- A stream range [x,y..]
PRangeStream : FC -> PTerm -> Maybe PTerm -> PTerm
-- r.x.y, equivalent to (y (x r))
PPostfixProjs : FC -> PTerm -> List PTerm -> PTerm
-- (.x.y p q), equivalent to (\r => r.x.y p q)
PPostfixProjsSection : FC -> List PTerm -> List PTerm -> PTerm
-- r.x.y
PPostfixApp : FC -> PTerm -> List Name -> PTerm
-- .x.y
PPostfixAppPartial : FC -> List Name -> PTerm
-- Debugging
PUnifyLog : FC -> LogLevel -> PTerm -> PTerm
@ -150,8 +150,8 @@ mutual
getPTermLoc (PRewrite fc _ _) = fc
getPTermLoc (PRange fc _ _ _) = fc
getPTermLoc (PRangeStream fc _ _) = fc
getPTermLoc (PPostfixProjs fc _ _) = fc
getPTermLoc (PPostfixProjsSection fc _ _) = fc
getPTermLoc (PPostfixApp fc _ _) = fc
getPTermLoc (PPostfixAppPartial fc _) = fc
getPTermLoc (PUnifyLog fc _ _) = fc
getPTermLoc (PWithUnambigNames fc _ _) = fc
@ -237,6 +237,7 @@ mutual
Overloadable : Name -> Directive
Extension : LangExt -> Directive
DefaultTotality : TotalReq -> Directive
PrefixRecordProjections : Bool -> Directive
AutoImplicitDepth : Nat -> Directive
public export
@ -602,13 +603,10 @@ mutual
showPrec d (PRangeStream _ start (Just next))
= "[" ++ showPrec d start ++ ", " ++ showPrec d next ++ " .. ]"
showPrec d (PUnifyLog _ _ tm) = showPrec d tm
showPrec d (PPostfixProjs fc rec fields)
showPrec d (PPostfixApp fc rec fields)
= showPrec d rec ++ concatMap (\n => "." ++ show n) fields
showPrec d (PPostfixProjsSection fc fields args)
= "("
++ concatMap (\n => "." ++ show n) fields
++ concatMap (\x => " " ++ showPrec App x) args
++ ")"
showPrec d (PPostfixAppPartial fc fields)
= concatMap (\n => "." ++ show n) fields
showPrec d (PWithUnambigNames fc ns rhs)
= "with " ++ show ns ++ " " ++ showPrec d rhs
@ -906,12 +904,11 @@ mapPTermM f = goPTerm where
goPTerm (PUnifyLog fc k x) =
PUnifyLog fc k <$> goPTerm x
>>= f
goPTerm (PPostfixProjs fc rec fields) =
PPostfixProjs fc <$> goPTerm rec <*> pure fields
>>= f
goPTerm (PPostfixProjsSection fc fields args) =
PPostfixProjsSection fc fields <$> goPTerms args
goPTerm (PPostfixApp fc rec fields) =
PPostfixApp fc <$> goPTerm rec <*> pure fields
>>= f
goPTerm (PPostfixAppPartial fc fields) =
f (PPostfixAppPartial fc fields)
goPTerm (PWithUnambigNames fc ns rhs) =
PWithUnambigNames fc ns <$> goPTerm rhs
>>= f

8
src/Parser/Rule/Source.idr
View File

@ -96,8 +96,8 @@ aDotIdent = terminal "Expected dot+identifier"
export
dotIdent : Rule Name
dotIdent = UN <$> aDotIdent
postfixProj : Rule Name
postfixProj = RF <$> aDotIdent
export
symbol : String -> Rule ()
@ -215,12 +215,12 @@ name = opNonNS <|> do
else pure $ mkNamespacedName ns x
opNonNS : Rule Name
opNonNS = symbol "(" *> operator <* symbol ")"
opNonNS = symbol "(" *> (operator <|> postfixProj) <* symbol ")"
opNS : Namespace -> Rule Name
opNS ns = do
symbol ".("
n <- operator
n <- (operator <|> postfixProj)
symbol ")"
pure (NS ns n)

20
src/TTImp/ProcessRecord.idr
View File

@ -47,16 +47,21 @@ elabRecord {vars} eopts fc env nest newns vis tn params conName_in fields
defs <- get Ctxt
Just conty <- lookupTyExact conName (gamma defs)
| Nothing => throw (InternalError ("Adding " ++ show tn ++ "failed"))
-- Go into new namespace, if there is one, for getters
case newns of
Nothing =>
elabGetters conName 0 [] [] conty -- make projections
do elabGetters conName 0 [] RF [] conty -- make postfix projections
when !isPrefixRecordProjections $
elabGetters conName 0 [] UN [] conty -- make prefix projections
Just ns =>
do let cns = currentNS defs
let nns = nestedNS defs
extendNS (mkNamespace ns)
newns <- getNS
elabGetters conName 0 [] [] conty -- make projections
elabGetters conName 0 [] RF [] conty -- make postfix projections
when !isPrefixRecordProjections $
elabGetters conName 0 [] UN [] conty -- make prefix projections
defs <- get Ctxt
-- Record that the current namespace is allowed to look
-- at private names in the nested namespace
@ -122,17 +127,18 @@ elabRecord {vars} eopts fc env nest newns vis tn params conName_in fields
List (Name, RawImp) -> -- names to update in types
-- (for dependent records, where a field's type may depend
-- on an earlier projection)
(mkProjName : String -> Name) ->
Env Term vs -> Term vs ->
Core ()
elabGetters con done upds tyenv (Bind bfc n b@(Pi _ rc imp ty_chk) sc)
elabGetters con done upds mkProjName tyenv (Bind bfc n b@(Pi _ rc imp ty_chk) sc)
= if (n `elem` map fst params) || (n `elem` vars)
then elabGetters con
(if imp == Explicit && not (n `elem` vars)
then S done else done)
upds (b :: tyenv) sc
upds mkProjName (b :: tyenv) sc
else
do let fldNameStr = nameRoot n
projNameNS <- inCurrentNS (UN fldNameStr)
projNameNS <- inCurrentNS (mkProjName fldNameStr)
ty <- unelab tyenv ty_chk
let ty' = substNames vars upds ty
@ -173,9 +179,9 @@ elabRecord {vars} eopts fc env nest newns vis tn params conName_in fields
elabGetters con
(if imp == Explicit
then S done else done)
upds' (b :: tyenv) sc
upds' mkProjName (b :: tyenv) sc
elabGetters con done upds _ _ = pure ()
elabGetters con done upds _ _ _ = pure ()
export
processRecord : {vars : _} ->

17
src/TTImp/TTImp.idr
View File

@ -561,6 +561,7 @@ definedInBlock ns decls =
UN _ => NS ns n
MN _ _ => NS ns n
DN _ _ => NS ns n
RF _ => NS ns n
_ => n
defName : Namespace -> ImpDecl -> List Name
@ -576,11 +577,25 @@ definedInBlock ns decls =
fldns' : Namespace
fldns' = maybe ns (\ f => ns <.> mkNamespace f) fldns
toRF : Name -> Name
toRF (UN n) = RF n
toRF n = n
fnsUN : List Name
fnsUN = map getFieldName flds
fnsRF : List Name
fnsRF = map toRF fnsUN
-- Depending on %prefix_record_projections,
-- the record may or may not produce prefix projections (fnsUN).
--
-- However, since definedInBlock is pure, we can't check that flag
-- (and it would also be wrong if %prefix_record_projections appears
-- inside the parameter block)
-- so let's just declare all of them and some may go unused.
all : List Name
all = expandNS ns n :: map (expandNS fldns') fnsUN
all = expandNS ns n :: map (expandNS fldns') (fnsRF ++ fnsUN)
defName _ _ = []

4
src/Text/Lexer/Core.idr
View File

@ -171,12 +171,12 @@ tokenise pred line col acc tmap str
export
lex : TokenMap a -> String -> (List (WithBounds a), (Int, Int, String))
lex tmap str
= let (ts, (l, c, str')) = tokenise (const False) 0 0 [] tmap (unpack str) in
= let (ts, (l, c, str')) = tokenise (const False) 0 0 [] tmap (fastUnpack str) in
(ts, (l, c, fastPack str'))
export
lexTo : (WithBounds a -> Bool) ->
TokenMap a -> String -> (List (WithBounds a), (Int, Int, String))
lexTo pred tmap str
= let (ts, (l, c, str')) = tokenise pred 0 0 [] tmap (unpack str) in
= let (ts, (l, c, str')) = tokenise pred 0 0 [] tmap (fastUnpack str) in
(ts, (l, c, fastPack str'))

5
support/c/Makefile
View File

@ -52,4 +52,7 @@ cleandep: clean
install: build
mkdir -p ${PREFIX}/idris2-${IDRIS2_VERSION}/lib
install $(LIBTARGET) $(DYLIBTARGET) *.h ${PREFIX}/idris2-${IDRIS2_VERSION}/lib
mkdir -p ${PREFIX}/idris2-${IDRIS2_VERSION}/include
install -m 755 $(DYLIBTARGET) ${PREFIX}/idris2-${IDRIS2_VERSION}/lib
install -m 644 $(LIBTARGET) ${PREFIX}/idris2-${IDRIS2_VERSION}/lib
install -m 644 *.h ${PREFIX}/idris2-${IDRIS2_VERSION}/include

31
support/c/idris_buffer.c
View File

@ -4,7 +4,7 @@
typedef struct {
int size;
uint8_t data[0];
uint8_t data[];
} Buffer;
void* idris2_newBuffer(int bytes) {
@ -46,13 +46,17 @@ void idris2_setBufferByte(void* buffer, int loc, int byte) {
}
}
void idris2_setBufferInt(void* buffer, int loc, int val) {
void idris2_setBufferInt(void* buffer, int loc, int64_t val) {
Buffer* b = buffer;
if (loc >= 0 && loc+3 < b->size) {
b->data[loc] = val & 0xff;
b->data[loc+1] = (val >> 8) & 0xff;
b->data[loc ] = val & 0xff;
b->data[loc+1] = (val >> 8) & 0xff;
b->data[loc+2] = (val >> 16) & 0xff;
b->data[loc+3] = (val >> 24) & 0xff;
b->data[loc+4] = (val >> 32) & 0xff;
b->data[loc+5] = (val >> 40) & 0xff;
b->data[loc+6] = (val >> 48) & 0xff;
b->data[loc+7] = (val >> 56) & 0xff;
}
}
@ -77,7 +81,7 @@ void idris2_setBufferString(void* buffer, int loc, char* str) {
}
}
int idris2_getBufferByte(void* buffer, int loc) {
uint8_t idris2_getBufferByte(void* buffer, int loc) {
Buffer* b = buffer;
if (loc >= 0 && loc < b->size) {
return b->data[loc];
@ -86,13 +90,14 @@ int idris2_getBufferByte(void* buffer, int loc) {
}
}
int idris2_getBufferInt(void* buffer, int loc) {
int64_t idris2_getBufferInt(void* buffer, int loc) {
Buffer* b = buffer;
if (loc >= 0 && loc+3 < b->size) {
return b->data[loc] +
(b->data[loc+1] << 8) +
(b->data[loc+2] << 16) +
(b->data[loc+3] << 24);
if (loc >= 0 && loc+7 < b->size) {
int64_t result = 0;
for (size_t i=0; i<8; i++) {
result |= b->data[loc + i] << (8 * i);
}
return result;
} else {
return 0;
}
@ -124,10 +129,10 @@ char* idris2_getBufferString(void* buffer, int loc, int len) {
return rs;
}
int idris2_readBufferData(FILE* h, char* buffer, int loc, int max) {
size_t idris2_readBufferData(FILE* h, char* buffer, size_t loc, size_t max) {
return fread(buffer+loc, sizeof(uint8_t), (size_t)max, h);
}
int idris2_writeBufferData(FILE* h, char* buffer, int loc, int len) {
size_t idris2_writeBufferData(FILE* h, const char* buffer, size_t loc, size_t len) {
return fwrite(buffer+loc, sizeof(uint8_t), len, h);
}

11
support/c/idris_buffer.h
View File

@ -11,7 +11,7 @@ void idris2_freeBuffer(void* buf);
int idris2_getBufferSize(void* buffer);
void idris2_setBufferByte(void* buffer, int loc, int byte);
void idris2_setBufferInt(void* buffer, int loc, int val);
void idris2_setBufferInt(void* buffer, int loc, int64_t val);
void idris2_setBufferDouble(void* buffer, int loc, double val);
void idris2_setBufferString(void* buffer, int loc, char* str);
@ -19,11 +19,12 @@ void idris2_copyBuffer(void* from, int start, int len,
void* to, int loc);
// Reading and writing the raw data, to the pointer in the buffer
int idris2_readBufferData(FILE* h, char* buffer, int loc, int max);
int idris2_writeBufferData(FILE* h, char* buffer, int loc, int len);
size_t idris2_readBufferData(FILE* h, char* buffer, size_t loc, size_t max);
size_t idris2_writeBufferData(FILE* h, const char* buffer, size_t loc, size_t len);
int idris2_getBufferByte(void* buffer, int loc);
int idris2_getBufferInt(void* buffer, int loc);
uint8_t idris2_getBufferByte(void* buffer, int loc);
int64_t idris2_getBufferInt(void* buffer, int loc);
double idris2_getBufferDouble(void* buffer, int loc);
char* idris2_getBufferString(void* buffer, int loc, int len);

17
support/c/idris_net.c
View File

@ -76,6 +76,23 @@ int idrnet_socket(int domain, int type, int protocol) {
return socket(domain, type, protocol);
}
// Get the address family constants out of C and into Idris
int idrnet_af_unspec() {
return AF_UNSPEC;
}
int idrnet_af_unix() {
return AF_UNIX;
}
int idrnet_af_inet() {
return AF_INET;
}
int idrnet_af_inet6() {
return AF_INET6;
}
// We call this from quite a few functions. Given a textual host and an int port,
// populates a struct addrinfo.
int idrnet_getaddrinfo(struct addrinfo** address_res, char* host, int port,

6
support/c/idris_net.h
View File

@ -39,6 +39,12 @@ int idrnet_errno();
int idrnet_socket(int domain, int type, int protocol);
// Address family accessors
int idrnet_af_unspec(void);
int idrnet_af_unix(void);
int idrnet_af_inet(void);
int idrnet_af_inet6(void);
// Bind
int idrnet_bind(int sockfd, int family, int socket_type, char* host, int port);

15
support/chez/support.ss
View File

@ -66,8 +66,13 @@
(if (= (vector-ref xs 0) 0)
'()
(cons (vector-ref xs 1) (from-idris-list (vector-ref xs 2)))))
(define (string-concat xs) (apply string-append (from-idris-list xs)))
(define (string-pack xs) (apply string (from-idris-list xs)))
(define (to-idris-list-rev acc xs)
(if (null? xs)
acc
(to-idris-list-rev (vector 1 (car xs) acc) (cdr xs))))
(define (string-unpack s) (to-idris-list-rev (vector 0) (reverse (string->list s))))
(define (string-concat xs) (apply string-append (from-idris-list xs)))
(define string-cons (lambda (x y) (string-append (string x) y)))
(define get-tag (lambda (x) (vector-ref x 0)))
(define string-reverse (lambda (x)
@ -81,6 +86,14 @@
""
(substring s b end))))
(define (blodwen-string-iterator-new s)
0)
(define (blodwen-string-iterator-next s ofs)
(if (>= ofs (string-length s))
(vector 0) ; EOF
(vector 1 (string-ref s ofs) (+ ofs 1))))
(define either-left
(lambda (x)
(vector 0 x)))

17
support/gambit/support.scm
View File

@ -72,11 +72,16 @@
(if (= (vector-ref xs 0) 0)
'()
(cons (vector-ref xs 1) (from-idris-list (vector-ref xs 2)))))
(define-macro (string-concat xs)
`(apply string-append (from-idris-list ,xs)))
(define-macro (string-pack xs)
`(apply string (from-idris-list ,xs)))
(define (to-idris-list-rev acc xs)
(if (null? xs)
acc
(to-idris-list-rev (vector 1 (car xs) acc) (cdr xs))))
(define (string-unpack s) (to-idris-list-rev (vector 0) (reverse (string->list s))))
(define-macro (string-concat xs)
`(apply string-append (from-idris-list ,xs)))
(define-macro (string-cons x y)
`(string-append (string ,x) ,y))
@ -93,6 +98,14 @@
(define-macro (get-tag x) `(vector-ref ,x 0))
(define (blodwen-string-iterator-new s)
0)
(define (blodwen-string-iterator-next s ofs)
(if (>= ofs (string-length s))
(vector 0) ; EOF
(vector 1 (string-ref s ofs) (+ ofs 1))))
;; These two are only used in this file
(define-macro (either-left x) `(vector 0 ,x))
(define-macro (either-right x) `(vector 1 ,x))

13
support/racket/support.rkt
View File

@ -59,7 +59,12 @@
(if (= (vector-ref xs 0) 0)
'()
(cons (vector-ref xs 1) (from-idris-list (vector-ref xs 2)))))
(define (to-idris-list-rev acc xs)
(if (null? xs)
acc
(to-idris-list-rev (vector 1 (car xs) acc) (cdr xs))))
(define (string-concat xs) (apply string-append (from-idris-list xs)))
(define (string-unpack s) (to-idris-list-rev (vector 0) (reverse (string->list s))))
(define (string-pack xs) (list->string (from-idris-list xs)))
(define string-cons (lambda (x y) (string-append (string x) y)))
(define get-tag (lambda (x) (vector-ref x 0)))
@ -72,6 +77,14 @@
(end (min l (+ b x))))
(substring s b end)))
(define (blodwen-string-iterator-new s)
0)
(define (blodwen-string-iterator-next s ofs)
(if (>= ofs (string-length s))
(vector 0) ; EOF
(vector 1 (string-ref s ofs) (+ ofs 1))))
(define either-left
(lambda (x)
(vector 0 x)))

12
tests/ideMode/ideMode001/expected
View File

@ -2,13 +2,13 @@
000038(:write-string "1/1: Building LocType (LocType.idr)" 1)
0000ca(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 23) (:end 7 24)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "a")))))) 1)
0000d9(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 38) (:end 7 40)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect m a)")))))) 1)
0000df(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 35) (:end 7 37)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect {k:258} a)")))))) 1)
0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 9) (:end 7 10)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "?{_:259}_[]")))))) 1)
0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 14) (:end 7 16)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{k:258}_[] ?{_:259}_[])")))))) 1)
0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 18) (:end 7 20)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:260}_[] ?{_:259}_[])")))))) 1)
0000df(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 35) (:end 7 37)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect {k:295} a)")))))) 1)
0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 9) (:end 7 10)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "?{_:296}_[]")))))) 1)
0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 14) (:end 7 16)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{k:295}_[] ?{_:296}_[])")))))) 1)
0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 18) (:end 7 20)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:297}_[] ?{_:296}_[])")))))) 1)
0000d9(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 16) (:end 6 18)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect m a)")))))) 1)
0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 11) (:end 6 13)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:249}_[] ?{_:248}_[])")))))) 1)
0001eb(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 1) (:end 6 7)) ((:name "Main.append") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "{0 m : Prelude.Types.Nat} -> {0 a : Type} -> {0 n : Prelude.Types.Nat} -> ({arg:239} : (Main.Vect n[0] a[1])) -> ({arg:240} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.Num.+ Prelude.Types.Nat Prelude.Types.Num implementation at Prelude/Types.idr:57:1--64:7 n[2] m[4]) a[3]))))))")))))) 1)
0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 11) (:end 6 13)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:286}_[] ?{_:285}_[])")))))) 1)
0001eb(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 1) (:end 6 7)) ((:name "Main.append") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "{0 m : Prelude.Types.Nat} -> {0 a : Type} -> {0 n : Prelude.Types.Nat} -> ({arg:276} : (Main.Vect n[0] a[1])) -> ({arg:277} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.Num.+ Prelude.Types.Nat Prelude.Types.Num implementation at Prelude/Types.idr:57:1--64:7 n[2] m[4]) a[3]))))))")))))) 1)
0000cc(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 47) (:end 5 48)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
0000d9(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 44) (:end 5 45)) ((:name "m") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Types.Nat")))))) 1)
0000d9(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 40) (:end 5 41)) ((:name "n") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Types.Nat")))))) 1)

12
tests/ideMode/ideMode003/expected
View File

@ -2,13 +2,13 @@
000038(:write-string "1/1: Building LocType (LocType.idr)" 1)
0000ca(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 23) (:end 7 24)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "a")))))) 1)
0000d9(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 38) (:end 7 40)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect m a)")))))) 1)
0000df(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 35) (:end 7 37)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect {k:258} a)")))))) 1)
0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 9) (:end 7 10)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "?{_:259}_[]")))))) 1)
0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 14) (:end 7 16)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{k:258}_[] ?{_:259}_[])")))))) 1)
0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 18) (:end 7 20)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:260}_[] ?{_:259}_[])")))))) 1)
0000df(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 35) (:end 7 37)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect {k:295} a)")))))) 1)
0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 9) (:end 7 10)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "?{_:296}_[]")))))) 1)
0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 14) (:end 7 16)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{k:295}_[] ?{_:296}_[])")))))) 1)
0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 18) (:end 7 20)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:297}_[] ?{_:296}_[])")))))) 1)
0000d9(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 16) (:end 6 18)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect m a)")))))) 1)
0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 11) (:end 6 13)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:249}_[] ?{_:248}_[])")))))) 1)
0001eb(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 1) (:end 6 7)) ((:name "Main.append") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "{0 m : Prelude.Types.Nat} -> {0 a : Type} -> {0 n : Prelude.Types.Nat} -> ({arg:239} : (Main.Vect n[0] a[1])) -> ({arg:240} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.Num.+ Prelude.Types.Nat Prelude.Types.Num implementation at Prelude/Types.idr:57:1--64:7 n[2] m[4]) a[3]))))))")))))) 1)
0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 11) (:end 6 13)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:286}_[] ?{_:285}_[])")))))) 1)
0001eb(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 1) (:end 6 7)) ((:name "Main.append") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "{0 m : Prelude.Types.Nat} -> {0 a : Type} -> {0 n : Prelude.Types.Nat} -> ({arg:276} : (Main.Vect n[0] a[1])) -> ({arg:277} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.Num.+ Prelude.Types.Nat Prelude.Types.Num implementation at Prelude/Types.idr:57:1--64:7 n[2] m[4]) a[3]))))))")))))) 1)
0000cc(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 47) (:end 5 48)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
0000d9(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 44) (:end 5 45)) ((:name "m") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Types.Nat")))))) 1)
0000d9(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 40) (:end 5 41)) ((:name "n") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Types.Nat")))))) 1)

67
tests/idris2/record004/Main.idr
View File

@ -6,14 +6,34 @@ record Point where
y : Double
-- a record creates two projections:
--
-- .x : Point -> Double
-- .y : Point -> Double
--
-- because %prefix_record_projections are on by default, we also get:
--
-- x : Point -> Double
-- y : Point -> Double
-- to prevent cluttering the ordinary name space with short identifiers
%prefix_record_projections off
record Rect where
constructor MkRect
topLeft : Point
bottomRight : Point
-- .topLeft : Rect -> Point
-- .bottomRight : Rect -> Point
--
-- For Rect, we don't get the prefix projections:
--
-- Main> :t topLeft
-- (interactive):1:4--1:11:Undefined name topLeft
-- Main> :t .topLeft
-- \{rec:0} => .topLeft rec : ?_ -> Point
pt : Point
pt = MkPoint 4.2 6.6
@ -23,25 +43,46 @@ rect =
(MkPoint 1.1 2.5)
(MkPoint 4.3 6.3)
-- Foo.bar.baz with uppercase F is one lexeme: DotSepIdent ["baz", "bar", "Foo"]
-- New lexical structure:
--
-- Foo.bar.baz with uppercase F is one lexeme: NSIdent ["baz", "bar", "Foo"]
-- foo.bar.baz with lowercase f is three lexemes: foo, .bar, .baz
-- .foo.bar.baz is three lexemes: .foo, .bar, .baz
--
-- If you want Constructor.field, you have to write (Constructor).field.
--
-- New syntax of simpleExpr:
--
-- Expressions binding tighter than application (simpleExpr),
-- such as variables or parenthesised expressions,
-- have been renamed to simplerExpr,
-- and an extra layer of syntax has been inserted.
--
-- simpleExpr ::= (.field)+ -- parses as PPostfixAppPartial
-- | simplerExpr (.field)+ -- parses as PPostfixApp
-- | simplerExpr -- (parses as whatever it used to)
--
-- (.foo) is a name, so you can use it to e.g. define a function called .foo (see .squared below)
-- (.foo.bar) is a parenthesised expression
--
-- New desugaring rules
--
-- (.field1 .field2 .field3) desugars to (\x => .field3 (.field2 (.field1 x)))
-- (simpleExpr .field1 .field2 .field3) desugars to ((.field .field2 .field3) simpleExpr).
--
-- There are more details such as namespacing; see below.
add : Num a => a -> a -> a
add x y = x + y
-- user-defined projections work, too (should they?)
(.squared) : Double -> Double
(.squared) x = x * x
oopFoldl : List a -> b -> (b -> a -> b) -> b
oopFoldl xs z f = foldl f z xs
bad : Double
bad =
rect.x.topLeft -- should not throw errors
+ rect.(x . topLeft) -- disallowed without %language PostfixProjections
-- #649: Forced patterns remain unaffected by postfix projections.
test649 : (x, y : Bool) -> x = y -> Bool
test649 .(x) x Refl = x
bad2 : Double
bad2 = (.oopFoldl 0 (+)) -- disallowed without %language PostfixProjections
%language PostfixProjections
-- from now on, we can use complex projections
-- #441: Locals do not shadow record projections.
test441 : (Point -> Double) -> (Point -> Double) -> Point -> Double
test441 x y pt = pt.x + pt.y
-- no ambiguity errors: the locals "x" and "y" are not considered in pt.x and pt.y

26
tests/idris2/record004/expected
View File

@ -1,23 +1,10 @@
1/1: Building Main (Main.idr)
Error: complex postfix projections require %language PostfixProjections
Main.idr:41:5--41:23
|
41 | + rect.(x . topLeft) -- disallowed without %language PostfixProjections
| ^^^^^^^^^^^^^^^^^^
Error: postfix projection sections require %language PostfixProjections
Main.idr:44:9--44:24
|
44 | bad2 = (.oopFoldl 0 (+)) -- disallowed without %language PostfixProjections
| ^^^^^^^^^^^^^^^
Main> 4.2
Main> 4.2
Main> 10.8
Main> 4.2
Main> 4.2
Main> 17.64
Main> [1.1, 4.2]
Main> Error: When unifying (?a -> ?b) -> ?f ?a -> ?f ?b and Point.
Mismatch between: (?a -> ?b) -> ?f ?a -> ?f ?b and Point.
@ -28,14 +15,11 @@ Mismatch between: (?a -> ?b) -> ?f ?a -> ?f ?b and Point.
| ^^^
Main> [2.5, 2.5]
Main> 8.1
Main> [8.1, 8.1]
Main> 6
Main> [6, 15]
Main> 7.4
Main> 7.4
Main> 7.4
Main> MkPoint 1.1 2.5
Main> 4.2
Main> 4.2
Main> 4.2
Main> 4.2
Main> 4.2
Main> 4.2
Main> 4.2

12
tests/idris2/record004/input
View File

@ -3,17 +3,15 @@ pt .x
pt.x + pt.y
(Main.pt).x
(MkPoint pt.y pt.x).y
pt.x.squared
map (.x) [MkPoint 1.1 2.5, MkPoint 4.2 6.3]
map .x [MkPoint 1 2, MkPoint 3 4]
map (.topLeft.y) [rect, rect]
rect.topLeft.x.add 7
map (.topLeft.x.add 7) [rect, rect]
[1,2,3].oopFoldl 0 $ \x, y => x + y
map (.oopFoldl 0 (+)) [[1,2,3],[4,5,6]]
rect.topLeft.x + rect.bottomRight.y
rect.(x . topLeft) + rect.(y . bottomRight)
x rect.topLeft + y rect.bottomRight
rect.(Rect.topLeft)
Main.Point.(.x) pt
Point.(.x) pt
(.x) pt
.x pt
Main.Point.x pt
Point.x pt
(x) pt

2
tests/idris2/reflection004/refdecl.idr
View File

@ -16,7 +16,7 @@ mkPoint n
= let type = "Point" ++ show n ++ "D" in
IRecord emptyFC Public
(MkRecord emptyFC (NS (MkNS ["Main"]) (UN type)) [] (NS (MkNS ["Main"]) (UN ("Mk" ++ type)))
(toList $ map (\axis => MkIField emptyFC MW ExplicitArg (UN axis) `(Double)) (axes n)))
(toList $ map (\axis => MkIField emptyFC MW ExplicitArg (RF axis) `(Double)) (axes n)))
logDecls : TTImp -> Elab (Int -> Int)
logDecls v