Replace drop
/dropEnd
with splitAt
/splitAtEnd
This commit is contained in:
parent
1332f6cfb0
commit
11a06ab540
|
@ -203,10 +203,10 @@ data Expr a
|
|||
| ListFirst
|
||||
-- | > ListLast ~ List/last
|
||||
| ListLast
|
||||
-- | ListDrop ~ List/drop
|
||||
| ListDrop
|
||||
-- | ListDropEnd ~ List/dropEnd
|
||||
| ListDropEnd
|
||||
-- | ListSplitAt ~ List/splitAt
|
||||
| ListSplitAt
|
||||
-- | ListSplitAtEnd ~ List/splitAtEnd
|
||||
| ListSplitAtEnd
|
||||
-- | > ListIndexed ~ List/indexed
|
||||
| ListIndexed
|
||||
-- | > ListReverse ~ List/reverse
|
||||
|
@ -276,8 +276,8 @@ instance Monad Expr where
|
|||
ListLength >>= _ = ListLength
|
||||
ListFirst >>= _ = ListFirst
|
||||
ListLast >>= _ = ListLast
|
||||
ListDrop >>= _ = ListDrop
|
||||
ListDropEnd >>= _ = ListDropEnd
|
||||
ListSplitAt >>= _ = ListSplitAt
|
||||
ListSplitAtEnd >>= _ = ListSplitAtEnd
|
||||
ListIndexed >>= _ = ListIndexed
|
||||
ListReverse >>= _ = ListReverse
|
||||
ListConcat l r >>= k = ListConcat (l >>= k) (r >>= k)
|
||||
|
@ -458,10 +458,10 @@ buildExpr6 ListFirst =
|
|||
"List/first"
|
||||
buildExpr6 ListLast =
|
||||
"List/last"
|
||||
buildExpr6 ListDrop =
|
||||
"List/drop"
|
||||
buildExpr6 ListDropEnd =
|
||||
"List/dropEnd"
|
||||
buildExpr6 ListSplitAt =
|
||||
"List/splitAt"
|
||||
buildExpr6 ListSplitAtEnd =
|
||||
"List/splitAtEnd"
|
||||
buildExpr6 ListIndexed =
|
||||
"List/indexed"
|
||||
buildExpr6 ListReverse =
|
||||
|
@ -1677,14 +1677,26 @@ typeWith _ ListFirst = do
|
|||
return (Pi "a" (Const Type) (Pi "_" (App List "a") (App Maybe "a")))
|
||||
typeWith _ ListLast = do
|
||||
return (Pi "a" (Const Type) (Pi "_" (App List "a") (App Maybe "a")))
|
||||
typeWith _ ListDrop = do
|
||||
typeWith _ ListSplitAt = do
|
||||
let kts = Data.Map.fromList
|
||||
[ ("prefix", App List "a")
|
||||
, ("suffix", App List "a")
|
||||
]
|
||||
return
|
||||
(Pi "_" Natural
|
||||
(Pi "a" (Const Type) (Pi "_" (App List "a") (App List "a"))) )
|
||||
typeWith _ ListDropEnd = do
|
||||
(Pi "a" (Const Type)
|
||||
(Pi "_" (App List "a")
|
||||
(Record kts) ) ) )
|
||||
typeWith _ ListSplitAtEnd = do
|
||||
let kts = Data.Map.fromList
|
||||
[ ("prefix", App List "a")
|
||||
, ("suffix", App List "a")
|
||||
]
|
||||
return
|
||||
(Pi "_" Natural
|
||||
(Pi "a" (Const Type) (Pi "_" (App List "a") (App List "a"))) )
|
||||
(Pi "a" (Const Type)
|
||||
(Pi "_" (App List "a")
|
||||
(Record kts) ) ) )
|
||||
typeWith _ ListIndexed = do
|
||||
let kts = [("_1", Natural), ("_2", "a")]
|
||||
return
|
||||
|
@ -1823,12 +1835,23 @@ normalize e = case e of
|
|||
y = if Data.Vector.null ys
|
||||
then Data.Vector.empty
|
||||
else Data.Vector.singleton (Data.Vector.last ys)
|
||||
App (App (App ListDrop (NaturalLit n)) _) (ListLit t ys) ->
|
||||
normalize (ListLit t (Data.Vector.drop (fromIntegral n) ys))
|
||||
App (App (App ListDropEnd (NaturalLit n)) _) (ListLit t ys) ->
|
||||
normalize (ListLit t (Data.Vector.slice 0 end ys))
|
||||
App (App (App ListSplitAt (NaturalLit n)) _) (ListLit t ys) ->
|
||||
normalize (RecordLit kvs)
|
||||
where
|
||||
end = max 0 (Data.Vector.length ys - fromIntegral n)
|
||||
(prefix, suffix) = Data.Vector.splitAt (fromIntegral n) ys
|
||||
kvs = Data.Map.fromList
|
||||
[ ("prefix", ListLit t prefix)
|
||||
, ("suffix", ListLit t suffix)
|
||||
]
|
||||
App (App (App ListSplitAtEnd (NaturalLit n)) _) (ListLit t ys) ->
|
||||
normalize (RecordLit kvs)
|
||||
where
|
||||
n' = max 0 (Data.Vector.length ys - fromIntegral n)
|
||||
(prefix, suffix) = Data.Vector.splitAt n' ys
|
||||
kvs = Data.Map.fromList
|
||||
[ ("prefix", ListLit t prefix)
|
||||
, ("suffix", ListLit t suffix)
|
||||
]
|
||||
App (App ListIndexed _) (ListLit t xs) ->
|
||||
normalize (ListLit t' (fmap adapt (Data.Vector.indexed xs)))
|
||||
where
|
||||
|
|
|
@ -95,8 +95,8 @@ tokens :-
|
|||
"List/length" { emit ListLength }
|
||||
"List/first" { emit ListFirst }
|
||||
"List/last" { emit ListLast }
|
||||
"List/drop" { emit ListDrop }
|
||||
"List/dropEnd" { emit ListDropEnd }
|
||||
"List/splitAt" { emit ListSplitAt }
|
||||
"List/splitAtEnd" { emit ListSplitAtEnd }
|
||||
"List/indexed" { emit ListIndexed }
|
||||
"List/reverse" { emit ListReverse }
|
||||
"Maybe" { emit Maybe }
|
||||
|
@ -212,8 +212,8 @@ data Token
|
|||
| ListLength
|
||||
| ListFirst
|
||||
| ListLast
|
||||
| ListDrop
|
||||
| ListDropEnd
|
||||
| ListSplitAt
|
||||
| ListSplitAtEnd
|
||||
| ListIndexed
|
||||
| ListReverse
|
||||
| Maybe
|
||||
|
@ -319,10 +319,10 @@ instance Buildable Token where
|
|||
= "List/first"
|
||||
build ListLast
|
||||
= "List/last"
|
||||
build ListDrop
|
||||
= "List/drop"
|
||||
build ListDropEnd
|
||||
= "List/dropEnd"
|
||||
build ListSplitAt
|
||||
= "List/splitAt"
|
||||
build ListSplitAtEnd
|
||||
= "List/splitAtEnd"
|
||||
build ListIndexed
|
||||
= "List/indexed"
|
||||
build ListReverse
|
||||
|
|
|
@ -40,64 +40,64 @@ import qualified NeatInterpolation
|
|||
%monad { Alex }
|
||||
|
||||
%token
|
||||
'(' { Dhall.Lexer.OpenParen }
|
||||
')' { Dhall.Lexer.CloseParen }
|
||||
'{' { Dhall.Lexer.OpenBrace }
|
||||
'}' { Dhall.Lexer.CloseBrace }
|
||||
'{:}' { Dhall.Lexer.EmptyRecord }
|
||||
'[' { Dhall.Lexer.OpenBracket }
|
||||
']' { Dhall.Lexer.CloseBracket }
|
||||
':' { Dhall.Lexer.Colon }
|
||||
',' { Dhall.Lexer.Comma }
|
||||
'.' { Dhall.Lexer.Dot }
|
||||
'=' { Dhall.Lexer.Equals }
|
||||
'&&' { Dhall.Lexer.And }
|
||||
'||' { Dhall.Lexer.Or }
|
||||
'==' { Dhall.Lexer.DoubleEquals }
|
||||
'/=' { Dhall.Lexer.SlashEquals }
|
||||
'+' { Dhall.Lexer.Plus }
|
||||
'<>' { Dhall.Lexer.Diamond }
|
||||
'++' { Dhall.Lexer.DoublePlus }
|
||||
'*' { Dhall.Lexer.Star }
|
||||
'@' { Dhall.Lexer.At }
|
||||
'let' { Dhall.Lexer.Let }
|
||||
'in' { Dhall.Lexer.In }
|
||||
'Type' { Dhall.Lexer.Type }
|
||||
'Kind' { Dhall.Lexer.Kind }
|
||||
'->' { Dhall.Lexer.Arrow }
|
||||
'forall' { Dhall.Lexer.Forall }
|
||||
'\\' { Dhall.Lexer.Lambda }
|
||||
'Bool' { Dhall.Lexer.Bool }
|
||||
'True' { Dhall.Lexer.True_ }
|
||||
'False' { Dhall.Lexer.False_ }
|
||||
'if' { Dhall.Lexer.If }
|
||||
'then' { Dhall.Lexer.Then }
|
||||
'else' { Dhall.Lexer.Else }
|
||||
'Natural' { Dhall.Lexer.Natural }
|
||||
'Natural/fold' { Dhall.Lexer.NaturalFold }
|
||||
'Natural/isZero' { Dhall.Lexer.NaturalIsZero }
|
||||
'Integer' { Dhall.Lexer.Integer }
|
||||
'Double' { Dhall.Lexer.Double }
|
||||
'Text' { Dhall.Lexer.Text }
|
||||
'List' { Dhall.Lexer.List }
|
||||
'List/build' { Dhall.Lexer.ListBuild }
|
||||
'List/fold' { Dhall.Lexer.ListFold }
|
||||
'List/length' { Dhall.Lexer.ListLength }
|
||||
'List/first' { Dhall.Lexer.ListFirst }
|
||||
'List/last' { Dhall.Lexer.ListLast }
|
||||
'List/drop' { Dhall.Lexer.ListDrop }
|
||||
'List/dropEnd' { Dhall.Lexer.ListDropEnd }
|
||||
'List/indexed' { Dhall.Lexer.ListIndexed }
|
||||
'List/reverse' { Dhall.Lexer.ListReverse }
|
||||
'Maybe' { Dhall.Lexer.Maybe }
|
||||
'Maybe/fold' { Dhall.Lexer.MaybeFold }
|
||||
text { Dhall.Lexer.TextLit $$ }
|
||||
label { Dhall.Lexer.Label $$ }
|
||||
number { Dhall.Lexer.Number $$ }
|
||||
double { Dhall.Lexer.DoubleLit $$ }
|
||||
natural { Dhall.Lexer.NaturalLit $$ }
|
||||
url { Dhall.Lexer.URL $$ }
|
||||
file { Dhall.Lexer.File $$ }
|
||||
'(' { Dhall.Lexer.OpenParen }
|
||||
')' { Dhall.Lexer.CloseParen }
|
||||
'{' { Dhall.Lexer.OpenBrace }
|
||||
'}' { Dhall.Lexer.CloseBrace }
|
||||
'{:}' { Dhall.Lexer.EmptyRecord }
|
||||
'[' { Dhall.Lexer.OpenBracket }
|
||||
']' { Dhall.Lexer.CloseBracket }
|
||||
':' { Dhall.Lexer.Colon }
|
||||
',' { Dhall.Lexer.Comma }
|
||||
'.' { Dhall.Lexer.Dot }
|
||||
'=' { Dhall.Lexer.Equals }
|
||||
'&&' { Dhall.Lexer.And }
|
||||
'||' { Dhall.Lexer.Or }
|
||||
'==' { Dhall.Lexer.DoubleEquals }
|
||||
'/=' { Dhall.Lexer.SlashEquals }
|
||||
'+' { Dhall.Lexer.Plus }
|
||||
'<>' { Dhall.Lexer.Diamond }
|
||||
'++' { Dhall.Lexer.DoublePlus }
|
||||
'*' { Dhall.Lexer.Star }
|
||||
'@' { Dhall.Lexer.At }
|
||||
'let' { Dhall.Lexer.Let }
|
||||
'in' { Dhall.Lexer.In }
|
||||
'Type' { Dhall.Lexer.Type }
|
||||
'Kind' { Dhall.Lexer.Kind }
|
||||
'->' { Dhall.Lexer.Arrow }
|
||||
'forall' { Dhall.Lexer.Forall }
|
||||
'\\' { Dhall.Lexer.Lambda }
|
||||
'Bool' { Dhall.Lexer.Bool }
|
||||
'True' { Dhall.Lexer.True_ }
|
||||
'False' { Dhall.Lexer.False_ }
|
||||
'if' { Dhall.Lexer.If }
|
||||
'then' { Dhall.Lexer.Then }
|
||||
'else' { Dhall.Lexer.Else }
|
||||
'Natural' { Dhall.Lexer.Natural }
|
||||
'Natural/fold' { Dhall.Lexer.NaturalFold }
|
||||
'Natural/isZero' { Dhall.Lexer.NaturalIsZero }
|
||||
'Integer' { Dhall.Lexer.Integer }
|
||||
'Double' { Dhall.Lexer.Double }
|
||||
'Text' { Dhall.Lexer.Text }
|
||||
'List' { Dhall.Lexer.List }
|
||||
'List/build' { Dhall.Lexer.ListBuild }
|
||||
'List/fold' { Dhall.Lexer.ListFold }
|
||||
'List/length' { Dhall.Lexer.ListLength }
|
||||
'List/first' { Dhall.Lexer.ListFirst }
|
||||
'List/last' { Dhall.Lexer.ListLast }
|
||||
'List/splitAt' { Dhall.Lexer.ListSplitAt }
|
||||
'List/splitAtEnd' { Dhall.Lexer.ListSplitAtEnd }
|
||||
'List/indexed' { Dhall.Lexer.ListIndexed }
|
||||
'List/reverse' { Dhall.Lexer.ListReverse }
|
||||
'Maybe' { Dhall.Lexer.Maybe }
|
||||
'Maybe/fold' { Dhall.Lexer.MaybeFold }
|
||||
text { Dhall.Lexer.TextLit $$ }
|
||||
label { Dhall.Lexer.Label $$ }
|
||||
number { Dhall.Lexer.Number $$ }
|
||||
double { Dhall.Lexer.DoubleLit $$ }
|
||||
natural { Dhall.Lexer.NaturalLit $$ }
|
||||
url { Dhall.Lexer.URL $$ }
|
||||
file { Dhall.Lexer.File $$ }
|
||||
|
||||
%right '=='
|
||||
%right '/='
|
||||
|
@ -209,10 +209,10 @@ Expr6
|
|||
{ ListFirst }
|
||||
| 'List/last'
|
||||
{ ListLast }
|
||||
| 'List/drop'
|
||||
{ ListDrop }
|
||||
| 'List/dropEnd'
|
||||
{ ListDropEnd }
|
||||
| 'List/splitAt'
|
||||
{ ListSplitAt }
|
||||
| 'List/splitAtEnd'
|
||||
{ ListSplitAtEnd }
|
||||
| 'List/indexed'
|
||||
{ ListIndexed }
|
||||
| 'List/reverse'
|
||||
|
|
Loading…
Reference in New Issue
Block a user