582afe1 · Idris-dev · git.iko.soy

CHANGELOGnew file+17

compare with master

unifiedsplit

@@ -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

475

476-- Syntactic sugar info

477

478−data DSL = DSL { dsl_bind :: Name,

478+data DSL = DSL { dsl_bind :: PTerm,

479− dsl_return :: Name }

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+ }

480 deriving Show

487 deriving Show

481

488

482data SynContext = PatternSyntax | TermSyntax | AnySyntax

489data SynContext = PatternSyntax | TermSyntax | AnySyntax

@@ -499,7 +506,15 @@ data SSymbol = Keyword Name

499deriving instance Binary SSymbol

506deriving instance Binary SSymbol

500!-}

507!-}

501

508

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

503

518

504data SyntaxInfo = Syn { using :: [(Name, PTerm)],

519data SyntaxInfo = Syn { using :: [(Name, PTerm)],

505 syn_params :: [(Name, PTerm)],

520 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)

915 (expandDo dsl r)

916expandDo dsl (PAlternative as) = PAlternative (map (expandDo dsl) as)

917expandDo 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

919expandDo dsl (PDoBlock ds) = expandDo dsl $ block (dsl_bind dsl) ds

920 where

921 block b [DoExp fc tm] = tm

922 block b [a] = PElabError "Last statement in do block must be an expression"

923 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))]

925 block b (DoLet fc n tm : rest)

926 = PLet n Placeholder tm (block b rest)

927 block b (DoExp fc tm : rest)

928− = PApp fc (PRef fc b)

928+ = PApp fc b

929 [pexp tm,

930 pexp (PLam (MN 0 "bindx") Placeholder (block b rest))]

931 block b _ = PElabError "Invalid statement in do block"