git.iko.soy/Idris-dev
on master help sign in
Added system module (getArgs, getEnv, exit)
commit582afe16364177d0c8816c577f0e684edabcd0b0 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateTue 20 Dec 2011, 21:18 (15 years ago) parent4b63e6e
4 files changed+64−6
compare with master
unifiedsplit
CHANGELOG+17 lib/system.idr+26 src/Idris/AbsSyntax.hs+18−3 src/Idris/Parser.hs+3−3
CHANGELOGnew file+17
@@ -0,0 +1,17 @@
1+0.1.x to 0.9.0:
2+
3+Complete rewrite. User visible changes:
4+
5+* New proof/tactics syntax
6+* New syntax for pairs/dependent pairs
7+* Added type classes
8+* Added where clauses
9+* Added cumulativity and universe checking
10+* Ad-hoc name overloading
11+ - Resolved by type or explicit namespace
12+* Modules (Haskell-style)
13+* Separate type-checking
14+* Improved interactive environment
15+* Replaced 'do using' with Monad class
16+* Extended syntax macros
17+
lib/system.idrnew file+26
@@ -0,0 +1,26 @@
1+module system;
2+
3+import prelude;
4+
5+getArgs : IO (List String);
6+getArgs = do { n <- numArgs;
7+ ga' [] 0 n; }
8+ where {
9+ numArgs : IO Int;
10+ numArgs = mkForeign (FFun "epic_numArgs" [] FInt);
11+
12+ getArg : Int -> IO String;
13+ getArg x = mkForeign (FFun "epic_getArg" [FInt] FString) x;
14+
15+ ga' : List String -> Int -> Int -> IO (List String);
16+ ga' acc i n = if (i == n) then (return $ rev acc) else
17+ do { arg <- getArg i;
18+ ga' (arg :: acc) (i+1) n; };
19+ }
20+
21+getEnv : String -> IO String;
22+getEnv x = mkForeign (FFun "getenv" [FString] FString) x;
23+
24+exit : Int -> IO ();
25+exit code = mkForeign (FFun "exit" [FInt] FUnit) code;
26+
src/Idris/AbsSyntax.hs+18−3
@@ -475,8 +475,15 @@ deriving instance Binary ClassInfo
475475
476476-- Syntactic sugar info
477477
478−data DSL = DSL { dsl_bind :: Name,
479− dsl_return :: Name }
478+data DSL = DSL { dsl_bind :: PTerm,
479+ dsl_return :: PTerm,
480+ dsl_apply :: PTerm,
481+ dsl_pure :: PTerm,
482+ index_first :: Maybe PTerm,
483+ index_next :: Maybe PTerm,
484+ dsl_lambda :: Maybe PTerm,
485+ dsl_let :: Maybe PTerm
486+ }
480487 deriving Show
481488
482489data SynContext = PatternSyntax | TermSyntax | AnySyntax
@@ -499,7 +506,15 @@ data SSymbol = Keyword Name
499506deriving instance Binary SSymbol
500507!-}
501508
502−initDSL = DSL (UN ">>=") (UN "return")
509+initDSL = DSL (PRef f (UN ">>="))
510+ (PRef f (UN "return"))
511+ (PRef f (UN "<$>"))
512+ (PRef f (UN "pure"))
513+ Nothing
514+ Nothing
515+ Nothing
516+ Nothing
517+ where f = FC "(builtin)" 0
503518
504519data SyntaxInfo = Syn { using :: [(Name, PTerm)],
505520 syn_params :: [(Name, PTerm)],
src/Idris/Parser.hs+3−3
@@ -915,17 +915,17 @@ expandDo dsl (PDPair fc l t r) = PDPair fc (expandDo dsl l) (expandDo dsl t)
915915 (expandDo dsl r)
916916expandDo dsl (PAlternative as) = PAlternative (map (expandDo dsl) as)
917917expandDo dsl (PHidden t) = PHidden (expandDo dsl t)
918−expandDo dsl (PReturn fc) = PRef fc (dsl_return dsl)
918+expandDo dsl (PReturn fc) = dsl_return dsl
919919expandDo dsl (PDoBlock ds) = expandDo dsl $ block (dsl_bind dsl) ds
920920 where
921921 block b [DoExp fc tm] = tm
922922 block b [a] = PElabError "Last statement in do block must be an expression"
923923 block b (DoBind fc n tm : rest)
924− = PApp fc (PRef fc b) [pexp tm, pexp (PLam n Placeholder (block b rest))]
924+ = PApp fc b [pexp tm, pexp (PLam n Placeholder (block b rest))]
925925 block b (DoLet fc n tm : rest)
926926 = PLet n Placeholder tm (block b rest)
927927 block b (DoExp fc tm : rest)
928− = PApp fc (PRef fc b)
928+ = PApp fc b
929929 [pexp tm,
930930 pexp (PLam (MN 0 "bindx") Placeholder (block b rest))]
931931 block b _ = PElabError "Invalid statement in do block"