on master help sign in
Merge branch 'master' of github.com:edwinb/Idris-dev
commita11c591d42d0e3f96b58e24582f35e8fa86f0ae8 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateThu 4 Jul 2013, 19:45 (13 years ago) parent6924ceb576d33b
5 files changed+291−192
contribs/lib/SimpleParser/SimpleParser.idr+223 contribs/lib/simpleparser.idr−183 lib/Prelude/List.idr+2−2 src/IRTS/CodegenJavaScript.hs+16−7 test/Makefile+50
contribs/lib/SimpleParser/SimpleParser.idrnew file+223
@@ -0,0 +1,223 @@
1+{-
2+ Simple monadic parser module, based heavily on that by
3+ Graham Hutton.
4+-}
5+
6+module SimpleParser
7+
8+import Prelude
9+import Prelude.Monad
10+import Prelude.Applicative
11+import Prelude.List
12+import Builtins
13+
14+%access public
15+
16+infixr 5 |||
17+
18+{-
19+The monad of parsers
20+--------------------
21+-}
22+
23+data Parser a = P (String -> Either String (a, String))
24+
25+parse : Parser a -> String -> Either String (a, String)
26+parse (P p) inp = p inp
27+
28+instance Functor Parser where
29+ -- fmap : (a -> b) -> f a -> f b
30+ -- fmap : (a -> b) -> Parser a -> Parser b
31+ -- Given a function (a -> b), and a parser a, make a parser b
32+ fmap f p = P (\inp => case parse p inp of
33+ (Left err) => Left err
34+ -- Apply f to the v that we got from parsing
35+ (Right (v, rest)) => Right ((f v), rest))
36+
37+
38+instance Applicative Parser where
39+ pure v = P (\inp => Right (v, inp))
40+ -- Parse to get the function, then parse to get the first argument
41+ a <$> b = P (\inp => do (f, rest) <- parse a inp
42+ (x, rest') <- parse b rest
43+ pure ((f x), rest'))
44+
45+instance Monad Parser where
46+-- pure v = P (\inp => Right (v,inp))
47+ -- m a -> (a -> m b) -> m b
48+ p >>= f = P (\inp => case parse p inp of
49+ (Left err) => Left err
50+ (Right (v,rest)) => parse (f v) rest)
51+
52+--mplus : Monad m => m a -> m a -> m a
53+mplus : Parser a -> Parser a -> Parser a
54+mplus p q = P (\inp => case parse p inp of
55+ Left msg => parse q inp
56+ Right (v,out) => Right(v,out))
57+
58+
59+{-
60+Basic parsers
61+-------------
62+-}
63+
64+failure : String -> Parser a
65+failure msg = P (\inp => Left msg)
66+
67+item : Parser Char
68+item = P (\inp => case unpack inp of
69+ [] => Left "Error! Parsing empty list."
70+ (x::xs) => Right (x, pack xs))
71+
72+
73+{-
74+Choice
75+--------
76+---}
77+
78+(|||) : Parser a -> Parser a -> Parser a
79+p ||| q = p `mplus` q
80+
81+
82+--{-
83+--Derived primitives
84+---}
85+
86+sat : (Char -> Bool) -> Parser Char
87+sat p = item >>= (\x => if p x then pure x else failure "failed")
88+
89+oneof : List Char -> Parser Char
90+oneof xs = sat (\x => elem x xs)
91+
92+digit : Parser Char
93+digit = sat isDigit
94+
95+lower : Parser Char
96+lower = sat isLower
97+
98+upper : Parser Char
99+upper = sat isUpper
100+
101+letter : Parser Char
102+letter = sat isAlpha
103+
104+alphanum : Parser Char
105+alphanum = sat isAlphaNum
106+
107+char : Char -> Parser Char
108+char x = sat (== x)
109+
110+helper : List Char -> Parser (List Char)
111+string : String -> Parser String
112+string s = do result <- helper (unpack s)
113+ pure (pack result)
114+
115+helper [] = pure Prelude.List.Nil
116+helper (x::xs) = do char x
117+ string (cast xs)
118+ pure (x :: xs)
119+
120+many : Parser a -> Parser (List a)
121+many1 : Parser a -> Parser (List a)
122+many1 p = do v <- p
123+ vs <- many p
124+ pure $ Prelude.List.(::) v vs
125+
126+
127+bool : Parser Bool
128+bool = parseTrue ||| parseFalse
129+ where parseTrue : Parser Bool
130+ parseTrue = do oneof ['T', 't']
131+ string "rue"
132+ pure True
133+ parseFalse = do oneof ['F', 'f']
134+ string "alse"
135+ pure False
136+
137+
138+
139+
140+many p = many1 p `mplus` pure Prelude.List.Nil
141+
142+
143+
144+ident : Parser String
145+ident = do x <- letter
146+ xs <- many1 alphanum
147+ pure (pack(x::xs))
148+
149+nat : Parser Int
150+nat = do xs <- many digit
151+ pure (cast (cast xs))
152+
153+
154+int : Parser Int
155+int = neg ||| nat
156+ where neg : Parser Int
157+ neg = do char '-'
158+ n <- nat
159+ pure (-n)
160+
161+space : Parser ()
162+space = do many (sat isSpace)
163+ pure ()
164+--{-
165+--Ignoring spacing
166+---}
167+
168+token : Parser a -> Parser a
169+token p = do space
170+ v <- p
171+ space
172+ pure v
173+
174+identifier : Parser String
175+identifier = token ident
176+
177+natural : Parser Int
178+natural = token nat
179+
180+integer : Parser Int
181+integer = token int
182+
183+symbol : String -> Parser String
184+symbol xs = token (string xs)
185+
186+strToken : Parser String
187+strToken = fmap pack (token (many1 alphanum))
188+
189+--apply : Parser a -> String -> List (a,String)
190+--apply p = parse (space >>= (\_ => p))
191+
192+--{-
193+-- Expressions
194+---}
195+
196+factor : Parser Int
197+term : Parser Int
198+expr : Parser Int
199+expr = do t <- term
200+ do symbol "+"
201+ e <- expr
202+ pure $ t + e
203+ `mplus` pure t
204+
205+
206+factor = do symbol "("
207+ do e <- expr
208+ symbol ")"
209+ pure e
210+ `mplus` natural
211+
212+term = do f <- factor
213+ do symbol "*"
214+ t <- term
215+ pure (f * t)
216+ `mplus` pure f
217+
218+
219+
220+eval : String -> Maybe Int
221+eval xs = case (parse expr xs) of
222+ Right (n,rest) => if rest == "" then Just n else Nothing
223+ Left msg => Nothing
contribs/lib/simpleparser.idrdeleted−183
@@ -1,183 +0,0 @@
1−module Parsing
2−
3−import prelude
4−import builtins
5−
6−infixr 5 |||
7−
8−{-
9−The monad of parsers
10−--------------------
11−-}
12−
13−data Parser a = P (String -> Either String (a,String))
14−
15−parse : Parser a -> String ->Either String (a,String)
16−parse (P p) inp = p inp
17−
18−instance Monad Parser where
19− return v = P (\inp => Right (v,inp))
20− p >>= f = P (\inp => case parse p inp of
21− Left err => Left err
22− Right (v,rest) => parse (f v) rest)
23−
24−
25−instance MonadPlus Parser where
26− mzero = P (\inp => Left "Parse Error")
27− mplus p q = P (\inp => case parse p inp of
28− Left msg => parse q inp
29− Right (v,out) => Right(v,out))
30−
31−
32−{-
33−Basic parsers
34−-------------
35−-}
36−
37−failure : String -> Parser a
38−failure msg = P (\inp => Left msg)
39−
40−item : Parser Char
41−item = P (\inp => case unpack inp of
42− [] => Left "Error! Parsing empty list."
43− (x::xs) => Right (x, pack xs))
44−
45−
46−{-
47−Choice
48−--------
49−---}
50−
51−(|||) : Parser a -> Parser a -> Parser a
52−p ||| q = p `mplus` q
53−
54−
55−--{-
56−--Derived primitives
57−---}
58−
59−sat : (Char -> Bool) -> Parser Char
60−sat p = item >>= (\x => if p x then return x else failure "failed")
61−
62−oneof : List Char -> Parser Char
63−oneof xs = sat (\x => elem x xs)
64−
65−digit : Parser Char
66−digit = sat isDigit
67−
68−lower : Parser Char
69−lower = sat isLower
70−
71−upper : Parser Char
72−upper = sat isUpper
73−
74−letter : Parser Char
75−letter = sat isAlpha
76−
77−alphanum : Parser Char
78−alphanum = sat isAlphaNum
79−
80−char : Char -> Parser Char
81−char x = sat (== x)
82−
83−string : String -> Parser String
84−helper : List Char -> Parser (List Char)
85−string s = do result <- helper (unpack s)
86− return (pack result)
87−
88−helper [] = return []
89−helper (x::xs) = do char x
90− string (cast xs)
91− return (x :: xs)
92−
93−many1 : Parser a -> Parser (List a)
94−many : Parser a -> Parser (List a)
95−many1 p = do v <- p
96− vs <- many p
97− return (v::vs)
98−
99−
100−many p = many1 p `mplus` return []
101−
102−
103−
104−ident : Parser String
105−ident = do x <- letter
106− xs <- many1 alphanum
107− return (pack(x::xs))
108−
109−
110−nat : Parser Int
111−nat = do xs <- many digit
112− return (cast (cast xs))
113−
114−
115−int : Parser Int
116−int = do char '-'
117− n <- nat
118− return (-n)
119− `mplus` nat
120−
121−space : Parser ()
122−space = do many (sat isSpace)
123− return ()
124−--{-
125−--Ignoring spacing
126−---}
127−
128−token : Parser a -> Parser a
129−token p = do space
130− v <- p
131− space
132− return v
133−
134−identifier : Parser String
135−identifier = token ident
136−
137−natural : Parser Int
138−natural = token nat
139−
140−integer : Parser Int
141−integer = token int
142−
143−symbol : String -> Parser String
144−symbol xs = token (string xs)
145−
146−--apply : Parser a -> String -> List (a,String)
147−--apply p = parse (space >>= (\_ => p))
148−
149−--{-
150−-- Expressions
151−---}
152−
153−factor : Parser Int
154−term : Parser Int
155−expr : Parser Int
156−expr = do t <- term
157− do symbol "+"
158− e <- expr
159− Right (t+e)
160− ||| Right t
161−
162−
163−factor = do symbol "("
164− do e <- expr
165− symbol ")"
166− return e
167− ||| natural
168−
169−term = do f <- factor
170− do symbol "*"
171− t <- term
172− return (f * t)
173− ||| return f
174−
175−
176−
177−eval : String -> Maybe Int
178−eval xs = case (parse expr xs) of
179− Right (n,rest) => if rest == "" then Just n else Nothing
180− Left msg => Nothing
181−
182−
183−
lib/Prelude/List.idr+2−2
@@ -125,9 +125,9 @@ partial
125125repeat : a -> List a
126126repeat x = x :: lazy (repeat x)
127127
128−%assert_total
129128replicate : Nat -> a -> List a
130−replicate n x = take n (repeat x)
129+replicate O x = []
130+replicate (S n) x = x :: replicate n x
131131
132132--------------------------------------------------------------------------------
133133-- Instances
src/IRTS/CodegenJavaScript.hs+16−7
@@ -16,11 +16,12 @@ import Data.Char
1616import Data.List
1717import qualified Data.Map as Map
1818import System.IO
19+import System.Directory
1920
2021idrNamespace :: String
2122idrNamespace = "__IDR__"
2223
23−data JSTarget = Node | JavaScript
24+data JSTarget = Node | JavaScript deriving Eq
2425
2526codegenJavaScript
2627 :: JSTarget
@@ -29,17 +30,25 @@ codegenJavaScript
2930 -> OutputType
3031 -> IO ()
3132codegenJavaScript target definitions filename outputType = do
32− let runtime = case target of
33− Node -> "-node"
34− JavaScript -> "-browser"
33+ let (header, runtime) = case target of
34+ Node ->
35+ ("#!/usr/bin/env node\n", "-node")
36+ JavaScript ->
37+ ("", "-browser")
3538 path <- getDataDir
3639 idrRuntime <- readFile $ path ++ "/js/Runtime-common.js"
3740 tgtRuntime <- readFile $ concat [path, "/js/Runtime", runtime, ".js"]
38− writeFile filename (idrRuntime
41+ writeFile filename ( header
42+ ++ idrRuntime
3943 ++ tgtRuntime
4044 ++ modules
4145 ++ functions
4246 ++ mainLoop)
47+
48+ setPermissions filename (emptyPermissions { readable = True
49+ , executable = target == Node
50+ , writable = True
51+ })
4352 where
4453 def = map (first translateNamespace) definitions
4554
@@ -340,7 +349,7 @@ translateExpression (SOp op vars)
340349 , (arg:_) <- vars = translateVariableName arg ++ "[0]"
341350 | LStrRev <- op
342351 , (arg:_) <- vars = let v = translateVariableName arg in
343− v ++ "split('').reverse().join('')"
352+ v ++ ".split('').reverse().join('')"
344353 | LStrIndex <- op
345354 , (lhs:rhs:_) <- vars = let l = translateVariableName lhs
346355 r = translateVariableName rhs in
@@ -472,7 +481,7 @@ translateCase var (SConstCase ty e)
472481 matchHelper tyName = translateTypeMatch var tyName e
473482
474483translateCase var (SConstCase cst@(BI _) e) =
475− let cond = var ++ ".equals(" ++ translateConstant cst ++ ")" in
484+ let cond = "__IDRRT__.bigInt(" ++ var ++ ").equals(" ++ translateConstant cst ++ ")" in
476485 createIfBlock cond (translateExpression e)
477486
478487translateCase var (SConstCase cst e) =
test/Makefile+50
@@ -4,6 +4,56 @@ test:
44test_java:
55 perl ./runtest.pl all --target Java
66
7+test_js:
8+ @perl ./runtest.pl reg001 --target node
9+ @perl ./runtest.pl reg002 --target node
10+ @perl ./runtest.pl reg003 --target node
11+ @perl ./runtest.pl reg004 --target node
12+ @perl ./runtest.pl reg004 --target node
13+ @perl ./runtest.pl reg005 --target node
14+ @perl ./runtest.pl reg006 --target node
15+ @perl ./runtest.pl reg007 --target node
16+ @perl ./runtest.pl reg008 --target node
17+ @perl ./runtest.pl reg009 --target node
18+ @perl ./runtest.pl reg010 --target node
19+ @perl ./runtest.pl reg011 --target node
20+ @perl ./runtest.pl reg012 --target node
21+ @perl ./runtest.pl reg013 --target node
22+ @perl ./runtest.pl reg014 --target node
23+ @perl ./runtest.pl reg015 --target node
24+ @#perl ./runtest.pl reg016 --target node
25+ @perl ./runtest.pl reg017 --target node
26+ @perl ./runtest.pl reg018 --target node
27+ @perl ./runtest.pl reg019 --target node
28+ @perl ./runtest.pl test001 --target node
29+ @perl ./runtest.pl test002 --target node
30+ @perl ./runtest.pl test003 --target node
31+ @#perl ./runtest.pl test004 --target node
32+ @perl ./runtest.pl test005 --target node
33+ @perl ./runtest.pl test006 --target node
34+ @perl ./runtest.pl test007 --target node
35+ @perl ./runtest.pl test008 --target node
36+ @perl ./runtest.pl test009 --target node
37+ @perl ./runtest.pl test010 --target node
38+ @perl ./runtest.pl test011 --target node
39+ @perl ./runtest.pl test012 --target node
40+ @perl ./runtest.pl test013 --target node
41+ @#perl ./runtest.pl test014 --target node
42+ @perl ./runtest.pl test015 --target node
43+ @perl ./runtest.pl test016 --target node
44+ @perl ./runtest.pl test017 --target node
45+ @#perl ./runtest.pl test018 --target node
46+ @perl ./runtest.pl test019 --target node
47+ @perl ./runtest.pl test020 --target node
48+ @#perl ./runtest.pl test021 --target node
49+ @perl ./runtest.pl test022 --target node
50+ @perl ./runtest.pl test023 --target node
51+ @perl ./runtest.pl test024 --target node
52+ @#perl ./runtest.pl test025 --target node
53+ @perl ./runtest.pl test026 --target node
54+ @perl ./runtest.pl test027 --target node
55+ @perl ./runtest.pl test028 --target node
56+
757update:
858 perl ./runtest.pl all -u
959