idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2025-01-08 08:52:22 +03:00
Code Issues Projects Releases Wiki Activity

arrays

Browse Source
This commit is contained in:
Rui Barreiro 2020-06-20 13:05:58 +01:00
parent 525011eaff
commit a8a3681ee9
2 changed files with 10 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -231,6 +231,9 @@ jsPrim : {auto c : Ref ESs ESSt} -> Name -> List String -> Core String
jsPrim (NS _ (UN "prim__newIORef")) [_,v,_] = pure $ "({value: "++ v ++"})"
jsPrim (NS _ (UN "prim__readIORef")) [_,r,_] = pure $ "(" ++ r ++ ".value)"
jsPrim (NS _ (UN "prim__writeIORef")) [_,r,v,_] = pure $ "(" ++ r ++ ".value=" ++ v ++ ")"
jsPrim (NS _ (UN "prim__newArray")) [_,s,v,_] = pure $ "(Array(Number(" ++ s ++ ")).fill(" ++ v ++ "))"
jsPrim (NS _ (UN "prim__arrayGet")) [_,x,p,_] = pure $ "(" ++ x ++ "[" ++ p ++ "])"
jsPrim (NS _ (UN "prim__arraySet")) [_,x,p,v,_] = pure $ "(" ++ x ++ "[" ++ p ++ "] = " ++ v ++ ")"
jsPrim (NS _ (UN "prim__os")) [] =
do
os <- addRequireToPreamble "os"
@ -305,6 +308,8 @@ mutual
pure $ nSpaces indent ++ "throw new Error("++ jsString msg ++");"
imperative2es indent (EvalExpStatement e) =
pure $ nSpaces indent ++ !(impExp2es e) ++ ";"
imperative2es indent (CommentStatement x) =
pure $ "\n/*" ++ x ++ "*/\n"
alt2es : {auto c : Ref ESs ESSt} -> Nat -> (ImperativeExp, ImperativeStatement) -> Core String
alt2es indent (e, b) = pure $ nSpaces indent ++ "case " ++ !(impExp2es e) ++ ":\n" ++

6
src/Compiler/ES/Imperative.idr
View File

@ -41,6 +41,7 @@ mutual
| MutateStatement Name ImperativeExp
| ErrorStatement String
| EvalExpStatement ImperativeExp
| CommentStatement String
Semigroup ImperativeStatement where
DoNothing <+> y = y
@ -80,6 +81,7 @@ mutual
show (MutateStatement n v) = "(MutateStatement " ++ show n ++ " " ++ show v ++ ")"
show (ErrorStatement s) = "(ErrorStatement " ++ s ++ ")"
show (EvalExpStatement x) = "(EvalExpStatement " ++ show x ++ ")"
show (CommentStatement x) = "(CommentStatement " ++ show x ++ ")"
mutual
replaceNamesExp : List (Name, ImperativeExp) -> ImperativeExp -> ImperativeExp
@ -139,6 +141,8 @@ mutual
ErrorStatement s
replaceNamesExpS reps (EvalExpStatement x) =
EvalExpStatement $ replaceNamesExp reps x
replaceNamesExpS reps (CommentStatement x) =
CommentStatement x
data Imps : Type where
@ -278,4 +282,4 @@ compileToImperative c tm =
s <- newRef Imps (MkImpSt 0)
compdefs <- traverse getImp (defsUsedByNamedCExp ctm ndefs)
(s, main) <- impExp ctm
pure $ concat compdefs <+> s <+> EvalExpStatement main
pure $ concat compdefs <+> s <+> EvalExpStatement main <+> CommentStatement (show ndefs)