Add Natural/isZero
This commit is contained in:
Gabriel Gonzalez
parent
b8909addf4
commit
c09a586117
|
|
@ -175,6 +175,8 @@ data Expr a
|
|||
| NaturalLit Natural
|
||||
-- | > NaturalFold ~ Natural/fold
|
||||
| NaturalFold
|
||||
-- | > NaturalIsZero ~ Natural/isZero
|
||||
| NaturalIsZero
|
||||
-- | > NaturalPlus x y ~ x + y
|
||||
| NaturalPlus (Expr a) (Expr a)
|
||||
-- | > NaturalTimes x y ~ x * y
|
||||
|
|
@ -260,6 +262,7 @@ instance Monad Expr where
|
|||
Natural >>= _ = Natural
|
||||
NaturalLit n >>= _ = NaturalLit n
|
||||
NaturalFold >>= _ = NaturalFold
|
||||
NaturalIsZero >>= _ = NaturalIsZero
|
||||
NaturalPlus l r >>= k = NaturalPlus (l >>= k) (r >>= k)
|
||||
NaturalTimes l r >>= k = NaturalTimes (l >>= k) (r >>= k)
|
||||
Integer >>= _ = Integer
|
||||
|
|
@ -416,6 +419,8 @@ buildExpr5 Natural =
|
|||
"Natural"
|
||||
buildExpr5 NaturalFold =
|
||||
"Natural/fold"
|
||||
buildExpr5 NaturalIsZero =
|
||||
"Natural/isZero"
|
||||
buildExpr5 Integer =
|
||||
"Integer"
|
||||
buildExpr5 Double =
|
||||
|
|
@ -1373,6 +1378,8 @@ typeWith _ NaturalFold = do
|
|||
(Pi "natural" (Const Type)
|
||||
(Pi "succ" (Pi "pred" "natural" "natural")
|
||||
(Pi "zero" "natural" "natural") ) ) )
|
||||
typeWith _ NaturalIsZero = do
|
||||
return (Pi "_" Natural Bool)
|
||||
typeWith ctx e@(NaturalPlus l r) = do
|
||||
tl <- fmap normalize (typeWith ctx l)
|
||||
case tl of
|
||||
|
|
@ -1558,6 +1565,7 @@ normalize e = case e of
|
|||
where
|
||||
go !0 = zero
|
||||
go !n = App succ' (go (n - 1))
|
||||
App NaturalIsZero (NaturalLit n) -> BoolLit (n == 0)
|
||||
App (App ListBuild t) k
|
||||
| check -> ListLit t (buildVector k')
|
||||
| otherwise -> App f' a'
|
||||
|
|
|
|||
|
|
@ -83,6 +83,7 @@ tokens :-
|
|||
"else" { emit Else }
|
||||
"Natural" { emit Natural }
|
||||
"Natural/fold" { emit NaturalFold }
|
||||
"Natural/isZero" { emit NaturalIsZero }
|
||||
"Integer" { emit Integer }
|
||||
"Double" { emit Double }
|
||||
"Text" { emit Text }
|
||||
|
|
@ -195,6 +196,7 @@ data Token
|
|||
| Natural
|
||||
| NaturalLit Natural
|
||||
| NaturalFold
|
||||
| NaturalIsZero
|
||||
| Integer
|
||||
| Text
|
||||
| Double
|
||||
|
|
@ -288,6 +290,8 @@ instance Buildable Token where
|
|||
= "+" <> Data.Text.Buildable.build (fromIntegral n :: Integer)
|
||||
build NaturalFold
|
||||
= "Natural/fold"
|
||||
build NaturalIsZero
|
||||
= "Natural/isZero"
|
||||
build Integer
|
||||
= "Integer"
|
||||
build Text
|
||||
|
|
|
|||
|
|
@ -40,59 +40,60 @@ import qualified NeatInterpolation
|
|||
%monad { Alex }
|
||||
|
||||
%token
|
||||
'(' { Dhall.Lexer.OpenParen }
|
||||
')' { Dhall.Lexer.CloseParen }
|
||||
'{' { Dhall.Lexer.OpenBrace }
|
||||
'}' { Dhall.Lexer.CloseBrace }
|
||||
'{:}' { Dhall.Lexer.EmptyRecord }
|
||||
'{=}' { Dhall.Lexer.EmptyRecordLit }
|
||||
'[' { 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.Plus }
|
||||
'<>' { Dhall.Lexer.Diamond }
|
||||
'++' { Dhall.Lexer.DoublePlus }
|
||||
'*' { Dhall.Lexer.Star }
|
||||
'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 }
|
||||
'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/index' { Dhall.Lexer.ListIndex }
|
||||
'List/indexed' { Dhall.Lexer.ListIndexed }
|
||||
'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.EmptyRecordLit }
|
||||
'[' { 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.Plus }
|
||||
'<>' { Dhall.Lexer.Diamond }
|
||||
'++' { Dhall.Lexer.DoublePlus }
|
||||
'*' { Dhall.Lexer.Star }
|
||||
'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/index' { Dhall.Lexer.ListIndex }
|
||||
'List/indexed' { Dhall.Lexer.ListIndexed }
|
||||
'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 '&&'
|
||||
|
|
@ -170,6 +171,8 @@ Expr5
|
|||
{ Natural }
|
||||
| 'Natural/fold'
|
||||
{ NaturalFold }
|
||||
| 'Natural/isZero'
|
||||
{ NaturalIsZero }
|
||||
| 'Integer'
|
||||
{ Integer }
|
||||
| 'Double'
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user