on master help sign in
Merge branch 'master' of github.com:edwinb/Idris-dev
25cd881Edwin Brady
js/Runtime.js+1
@@ -1,3 +1,4 @@
1+var require;
1var __IDRRT__ = {};
2var __IDRRT__ = {};
2
3
3/** @constructor */
4/** @constructor */
samples/binary.idr+2−2
@@ -1,6 +1,6 @@
1module main
1module main
2
2
3−data Bit : Nat -> Set where
3+data Bit : Nat -> Type where
4 b0 : Bit 0
4 b0 : Bit 0
5 b1 : Bit 1
5 b1 : Bit 1
6
6
@@ -10,7 +10,7 @@ instance Show (Bit n) where
10
10
11infixl 5 #
11infixl 5 #
12
12
13−data Binary : (width : Nat) -> (value : Nat) -> Set where
13+data Binary : (width : Nat) -> (value : Nat) -> Type where
14 zero : Binary O O
14 zero : Binary O O
15 (#) : Binary w v -> Bit bit -> Binary (S w) (bit + 2 * v)
15 (#) : Binary w v -> Bit bit -> Binary (S w) (bit + 2 * v)
16
16
samples/interp-alt.idr+4−4
@@ -2,18 +2,18 @@ module main
2
2
3data Ty = TyInt | TyBool| TyFun Ty Ty
3data Ty = TyInt | TyBool| TyFun Ty Ty
4
4
5−interpTy : Ty -> Set
5+interpTy : Ty -> Type
6interpTy TyInt = Int
6interpTy TyInt = Int
7interpTy TyBool = Bool
7interpTy TyBool = Bool
8interpTy (TyFun s t) = interpTy s -> interpTy t
8interpTy (TyFun s t) = interpTy s -> interpTy t
9
9
10using (G : Vect Ty n)
10using (G : Vect Ty n)
11
11
12− data Env : Vect Ty n -> Set where
12+ data Env : Vect Ty n -> Type where
13 Nil : Env Nil
13 Nil : Env Nil
14 (::) : interpTy a -> Env G -> Env (a :: G)
14 (::) : interpTy a -> Env G -> Env (a :: G)
15
15
16−-- data HasType : (i : Fin n) -> Vect Ty n -> Ty -> Set where
16+-- data HasType : (i : Fin n) -> Vect Ty n -> Ty -> Type where
17-- stop : HasType fO (t :: G) t
17-- stop : HasType fO (t :: G) t
18-- pop : HasType k G t -> HasType (fS k) (u :: G) t
18-- pop : HasType k G t -> HasType (fS k) (u :: G) t
19
19
@@ -21,7 +21,7 @@ using (G : Vect Ty n)
21 lookup fO (x :: xs) = x
21 lookup fO (x :: xs) = x
22 lookup (fS i) (x :: xs) = lookup i xs
22 lookup (fS i) (x :: xs) = lookup i xs
23
23
24− data Expr : Vect Ty n -> Ty -> Set where
24+ data Expr : Vect Ty n -> Ty -> Type where
25 Var : (i : Fin n) -> Expr G (lookup i G)
25 Var : (i : Fin n) -> Expr G (lookup i G)
26 Val : (x : Int) -> Expr G TyInt
26 Val : (x : Int) -> Expr G TyInt
27 Lam : Expr (a :: G) t -> Expr G (TyFun a t)
27 Lam : Expr (a :: G) t -> Expr G (TyFun a t)
samples/interp.idr+4−4
@@ -2,18 +2,18 @@ module main
2
2
3data Ty = TyInt | TyBool | TyFun Ty Ty
3data Ty = TyInt | TyBool | TyFun Ty Ty
4
4
5−interpTy : Ty -> Set
5+interpTy : Ty -> Type
6interpTy TyInt = Int
6interpTy TyInt = Int
7interpTy TyBool = Bool
7interpTy TyBool = Bool
8interpTy (TyFun s t) = interpTy s -> interpTy t
8interpTy (TyFun s t) = interpTy s -> interpTy t
9
9
10using (G : Vect Ty n)
10using (G : Vect Ty n)
11
11
12− data Env : Vect Ty n -> Set where
12+ data Env : Vect Ty n -> Type where
13 Nil : Env Nil
13 Nil : Env Nil
14 (::) : interpTy a -> Env G -> Env (a :: G)
14 (::) : interpTy a -> Env G -> Env (a :: G)
15
15
16− data HasType : (i : Fin n) -> Vect Ty n -> Ty -> Set where
16+ data HasType : (i : Fin n) -> Vect Ty n -> Ty -> Type where
17 stop : HasType fO (t :: G) t
17 stop : HasType fO (t :: G) t
18 pop : HasType k G t -> HasType (fS k) (u :: G) t
18 pop : HasType k G t -> HasType (fS k) (u :: G) t
19
19
@@ -21,7 +21,7 @@ using (G : Vect Ty n)
21 lookup stop (x :: xs) = x
21 lookup stop (x :: xs) = x
22 lookup (pop k) (x :: xs) = lookup k xs
22 lookup (pop k) (x :: xs) = lookup k xs
23
23
24− data Expr : Vect Ty n -> Ty -> Set where
24+ data Expr : Vect Ty n -> Ty -> Type where
25 Var : HasType i G t -> Expr G t
25 Var : HasType i G t -> Expr G t
26 Val : (x : Int) -> Expr G TyInt
26 Val : (x : Int) -> Expr G TyInt
27 Lam : Expr (a :: G) t -> Expr G (TyFun a t)
27 Lam : Expr (a :: G) t -> Expr G (TyFun a t)
src/IRTS/CodegenJavaScript.hs+97−36
@@ -51,39 +51,61 @@ codegenJavaScript definitions filename outputType = do
51
51
52translateIdentifier :: String -> String
52translateIdentifier :: String -> String
53translateIdentifier =
53translateIdentifier =
54− concatMap replaceBadChars
54+ replaceReserved . concatMap replaceBadChars
55 where replaceBadChars :: Char -> String
55 where replaceBadChars :: Char -> String
56− replaceBadChars ' ' = "_"
57− replaceBadChars '_' = "__"
58− replaceBadChars '@' = "_at"
59− replaceBadChars '[' = "_OSB"
60− replaceBadChars ']' = "_CSB"
61− replaceBadChars '(' = "_OP"
62− replaceBadChars ')' = "_CP"
63− replaceBadChars '{' = "_OB"
64− replaceBadChars '}' = "_CB"
65− replaceBadChars '!' = "_bang"
66− replaceBadChars '#' = "_hash"
67− replaceBadChars '.' = "_dot"
68− replaceBadChars ',' = "_comma"
69− replaceBadChars ':' = "_colon"
70− replaceBadChars '+' = "_plus"
71− replaceBadChars '-' = "_minus"
72− replaceBadChars '*' = "_times"
73− replaceBadChars '<' = "_lt"
74− replaceBadChars '>' = "_gt"
75− replaceBadChars '=' = "_eq"
76− replaceBadChars '|' = "_pipe"
77− replaceBadChars '&' = "_amp"
78− replaceBadChars '/' = "_SL"
79− replaceBadChars '\\' = "_BSL"
80− replaceBadChars '%' = "_per"
81− replaceBadChars '?' = "_que"
82− replaceBadChars '~' = "_til"
83− replaceBadChars '\'' = "_apo"
84 replaceBadChars c
56 replaceBadChars c
57+ | ' ' <- c = "_"
58+ | '_' <- c = "__"
85 | isDigit c = "_" ++ [c] ++ "_"
59 | isDigit c = "_" ++ [c] ++ "_"
60+ | not (isLetter c && isAscii c) = '_' : show (ord c)
86 | otherwise = [c]
61 | otherwise = [c]
62+ replaceReserved s
63+ | s `elem` reserved = '_' : s
64+ | otherwise = s
65+ reserved = [ "break"
66+ , "case"
67+ , "catch"
68+ , "continue"
69+ , "debugger"
70+ , "default"
71+ , "delete"
72+ , "do"
73+ , "else"
74+ , "finally"
75+ , "for"
76+ , "function"
77+ , "if"
78+ , "in"
79+ , "instanceof"
80+ , "new"
81+ , "return"
82+ , "switch"
83+ , "this"
84+ , "throw"
85+ , "try"
86+ , "typeof"
87+ , "var"
88+ , "void"
89+ , "while"
90+ , "with"
91+
92+ , "class"
93+ , "enum"
94+ , "export"
95+ , "extends"
96+ , "import"
97+ , "super"
98+
99+ , "implements"
100+ , "interface"
101+ , "let"
102+ , "package"
103+ , "private"
104+ , "protected"
105+ , "public"
106+ , "static"
107+ , "yield"
108+ ]
87
109
88translateNamespace :: Name -> [String]
110translateNamespace :: Name -> [String]
89translateNamespace (UN _) = [idrNamespace]
111translateNamespace (UN _) = [idrNamespace]
@@ -112,8 +134,8 @@ translateConstant c =
112
134
113translateParameterlist =
135translateParameterlist =
114 map translateParameter
136 map translateParameter
115− where translateParameter (MN i name) = name ++ show i
137+ where translateParameter (MN i name) = translateIdentifier name ++ show i
116− translateParameter (UN name) = name
138+ translateParameter (UN name) = translateIdentifier name
117
139
118translateDeclaration :: ([String], SDecl) -> String
140translateDeclaration :: ([String], SDecl) -> String
119translateDeclaration (path, SFun name params stackSize body) =
141translateDeclaration (path, SFun name params stackSize body) =
@@ -327,11 +349,50 @@ translateExpression (SError msg) =
327translateExpression (SForeign _ _ "putStr" [(FString, var)]) =
349translateExpression (SForeign _ _ "putStr" [(FString, var)]) =
328 "__IDRRT__.print(" ++ translateVariableName var ++ ");"
350 "__IDRRT__.print(" ++ translateVariableName var ++ ");"
329
351
330−translateExpression (SForeign _ _ fun args) =
352+translateExpression (SForeign _ _ fun args)
331− fun
353+ | "." `isPrefixOf` fun, "[]=" `isSuffixOf` fun
332− ++ "("
354+ , (obj:idx:val:[]) <- args =
355+ concat [object obj, field, index idx, assign val]
356+
357+ | "." `isPrefixOf` fun, "[]" `isSuffixOf` fun
358+ , (obj:idx:[]) <- args =
359+ concat [object obj, field, index idx]
360+
361+ | "." `isPrefixOf` fun, "=" `isSuffixOf` fun
362+ , (obj:val:[]) <- args =
363+ concat [object obj, field, assign val]
364+
365+ | "." `isPrefixOf` fun
366+ , (obj:[]) <- args =
367+ object obj ++ field
368+
369+ | "." `isPrefixOf` fun
370+ , (obj:[(FUnit, _)]) <- args =
371+ concat [object obj, method, "()"]
372+
373+ | "." `isPrefixOf` fun
374+ , (obj:as) <- args =
375+ concat [object obj, method, arguments as]
376+
377+ | "[]=" == fun
378+ , (idx:val:[]) <- args =
379+ concat [array, index idx, assign val]
380+
381+ | "[]" == fun
382+ , (idx:[]) <- args =
383+ array ++ index idx
384+
385+ | otherwise = fun ++ arguments args
386+ where
387+ name = filter (`notElem` "[]=") fun
388+ method = name
389+ field = name
390+ array = name
391+ object o = translateVariableName (snd o)
392+ index i = "[" ++ translateVariableName (snd i) ++ "]"
393+ assign v = '=' : translateVariableName (snd v)
394+ arguments as =
333− ++ intercalate "," (map (translateVariableName . snd) args)
395+ '(' : intercalate "," (map (translateVariableName . snd) as) ++ ")"
334− ++ ");"
335
396
336translateExpression (SChkCase var cases) =
397translateExpression (SChkCase var cases) =
337 "(function(e){\n"
398 "(function(e){\n"