Merge remote-tracking branch 'upstream/master' into providers

CHANGELOG

@@ -3,6 +3,7 @@ New in 0.9.8:
 
 User visible changes:
 
+* Added "rewrite ... in ..." construct
 * Renamed EFF to EFFECT in Effect package
 * Experimental Java backend
 * Tab completion in REPL

contribs/tool-support/sublime-text/Idris/Idris.JSON-tmLanguage

@@ -0,0 +1,70 @@
+{ "name": "Idris",
+  "scopeName": "source.idris",
+  "fileTypes": ["idr"],
+  "patterns": [
+     {  "name": "keyword.control.idris",
+       "match": "\\b(if|then|else|do|let|in|data|codata|record|dsl|import)\\b"        
+
+    },
+    {  "name": "keyword.control.idris",
+       "match": "\\b(impossible|case|of|total|partial|mutual|infix|infixl|infixr)\\b"      
+
+    },
+    {  "name": "keyword.control.idris",
+       "match": "\\b(where|with|syntax|proof|postulate|using|namespace|class|instance)\\b"       
+
+    },
+    {  "name": "keyword.control.idris",
+       "match":  "\\b(public|private|abstract|implicit)\\b"      
+
+    },
+    {  "name": "keyword.other.idris",
+       "match": "\\b(Type|Int|Integer|Float|Char|String|Ptr|Bits8|Bits16|Bits32|Bits64)\\b"
+    },
+    {  "name": "constant.numeric.idris",
+       "match": "\\b(S|O)\\b"
+    },
+  	{ "match": "\\b([0-9]+|0([xX][0-9a-fA-F]+|[oO][0-7]+))\\b",
+  	  "name": "constant.numeric.idris", 
+  	  "comment": "integers"
+    },
+    {
+    	"match": "\\b([0-9]+\\.[0-9]+([eE][+-]?[0-9]+)?|[0-9]+[eE][+-]?[0-9]+)\\b",
+    	"name": "constant.numeric.float.idris",
+    	"comment": "floats"
+    },
+    {
+      "name": "comment.line.idris",
+      "match": "(--).*$\n?",
+      "comment": "Line comment"
+    },
+    { "name": "comment.block.idris",
+      "begin": "\\{-",
+      "end": "-\\}",
+      "comment": "Block comment"
+    },
+    { 
+      "name": "string.quoted.idris",
+      "begin": "\"",
+      "beginCaptures": {
+          "0": { "name": "punctuation.definition.string.begin.idris"}
+        },
+      "end": "\"",
+      "endCaptures": {
+          "0": { "name": "punctuation.definition.string.end.idris"}
+        },
+      "patterns": [
+        {  "name": "constant.character.escape.idris",
+           "match": "\\\\\""
+        }
+      ]
+
+    }
+
+
+  ],
+  "repository": {
+
+  },
+  "uuid": "4dd16092-ffa5-4ba4-8075-e5da9f368a72"
+}

contribs/tool-support/sublime-text/Idris/Idris.tmLanguage

@@ -0,0 +1,126 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!DOCTYPE plist PUBLIC "-//Apple Computer//DTD PLIST 1.0//EN" "http://www.apple.com/DTDs/PropertyList-1.0.dtd">
+<plist version="1.0">
+<dict>
+	<key>fileTypes</key>
+	<array>
+		<string>idr</string>
+	</array>
+	<key>name</key>
+	<string>Idris</string>
+	<key>patterns</key>
+	<array>
+		<dict>
+			<key>match</key>
+			<string>\b(if|then|else|do|let|in|data|codata|record|dsl|import)\b</string>
+			<key>name</key>
+			<string>keyword.control.idris</string>
+		</dict>
+		<dict>
+			<key>match</key>
+			<string>\b(impossible|case|of|total|partial|mutual|infix|infixl|infixr)\b</string>
+			<key>name</key>
+			<string>keyword.control.idris</string>
+		</dict>
+		<dict>
+			<key>match</key>
+			<string>\b(where|with|syntax|proof|postulate|using|namespace|class|instance)\b</string>
+			<key>name</key>
+			<string>keyword.control.idris</string>
+		</dict>
+		<dict>
+			<key>match</key>
+			<string>\b(public|private|abstract|implicit)\b</string>
+			<key>name</key>
+			<string>keyword.control.idris</string>
+		</dict>
+		<dict>
+			<key>match</key>
+			<string>\b(Type|Int|Integer|Float|Char|String|Ptr|Bits8|Bits16|Bits32|Bits64)\b</string>
+			<key>name</key>
+			<string>keyword.other.idris</string>
+		</dict>
+		<dict>
+			<key>match</key>
+			<string>\b(S|O)\b</string>
+			<key>name</key>
+			<string>constant.numeric.idris</string>
+		</dict>
+		<dict>
+			<key>comment</key>
+			<string>integers</string>
+			<key>match</key>
+			<string>\b([0-9]+|0([xX][0-9a-fA-F]+|[oO][0-7]+))\b</string>
+			<key>name</key>
+			<string>constant.numeric.idris</string>
+		</dict>
+		<dict>
+			<key>comment</key>
+			<string>floats</string>
+			<key>match</key>
+			<string>\b([0-9]+\.[0-9]+([eE][+-]?[0-9]+)?|[0-9]+[eE][+-]?[0-9]+)\b</string>
+			<key>name</key>
+			<string>constant.numeric.float.idris</string>
+		</dict>
+		<dict>
+			<key>comment</key>
+			<string>Line comment</string>
+			<key>match</key>
+			<string>(--).*$
+?</string>
+			<key>name</key>
+			<string>comment.line.idris</string>
+		</dict>
+		<dict>
+			<key>begin</key>
+			<string>\{-</string>
+			<key>comment</key>
+			<string>Block comment</string>
+			<key>end</key>
+			<string>-\}</string>
+			<key>name</key>
+			<string>comment.block.idris</string>
+		</dict>
+		<dict>
+			<key>begin</key>
+			<string>"</string>
+			<key>beginCaptures</key>
+			<dict>
+				<key>0</key>
+				<dict>
+					<key>name</key>
+					<string>punctuation.definition.string.begin.idris</string>
+				</dict>
+			</dict>
+			<key>end</key>
+			<string>"</string>
+			<key>endCaptures</key>
+			<dict>
+				<key>0</key>
+				<dict>
+					<key>name</key>
+					<string>punctuation.definition.string.end.idris</string>
+				</dict>
+			</dict>
+			<key>name</key>
+			<string>string.quoted.idris</string>
+			<key>patterns</key>
+			<array>
+				<dict>
+					<key>match</key>
+					<string>\\"</string>
+					<key>name</key>
+					<string>constant.character.escape.idris</string>
+				</dict>
+			</array>
+		</dict>
+	</array>
+	<key>repository</key>
+	<dict>
+	</dict>
+	<key>scopeName</key>
+	<string>source.idris</string>
+	<key>uuid</key>
+	<string>4dd16092-ffa5-4ba4-8075-e5da9f368a72</string>
+</dict>
+</plist>

contribs/tool-support/sublime-text/Idris/idris.sublime-build

@@ -0,0 +1,5 @@
+{
+	"cmd": ["idris", "$file"],
+	"file_regex": "^(...*?):([0-9]*):?([0-9]*)",
+	"selector": "source.idris"
+}

contribs/tool-support/sublime-text/README.md

@@ -0,0 +1,11 @@
+#### Idris support for Sublime Text 2
+
+To install, copy the Idris directory to Sublime Text's Packages directory.
+
+To build a new Idris.tmLanguage file from the Idris.JSON-tmLanguage file, Sublime Text needs to have the AAAPackageDev package installed.
+
+Syntax Definitions tutorial: https://sublime-text-unofficial-documentation.readthedocs.org/en/latest/extensibility/syntaxdefs.html
+
+Syntax Definitions reference: https://sublime-text-unofficial-documentation.readthedocs.org/en/latest/reference/syntaxdefs.html
+
+Most used scopes: http://manual.macromates.com/en/language_grammars#naming_conventions

contribs/tool-support/vim/indent/idris.vim

@@ -3,7 +3,7 @@
 " Based on haskell indentation by motemen <motemen@gmail.com>
 " 
 " author: raichoo (raichoo@googlemail.com)
-" date: Nov 2 2012
+" date: Mar 19 2013
 "
 " Modify g:idris_indent_if and g:idris_indent_case to
 " change indentation for `if'(default 3) and `case'(default 5).
@@ -36,6 +36,12 @@ if !exists('g:idris_indent_let')
   let g:idris_indent_let = 4
 endif
 
+if !exists('g:idris_indent_rewrite')
+  " rewrite prf in expr
+  " >>>>x
+  let g:idris_indent_rewrite = 8
+endif
+
 if !exists('g:idris_indent_where')
   " where f : Nat -> Nat
   " >>>>>>f x = x
@@ -71,6 +77,10 @@ function! GetIdrisIndent()
     return match(prevline, 'let') + g:idris_indent_let
   endif
 
+  if prevline =~ '\<rewrite\>\s\+.\+\<in\>\s*$'
+    return match(prevline, 'rewrite') + g:idris_indent_rewrite
+  endif
+
   if prevline !~ '\<else\>'
     let s = match(prevline, '\<if\>.*\&.*\zs\<then\>')
     if s > 0

contribs/tool-support/vim/syntax/idris.vim

@@ -4,15 +4,15 @@
 " highlighter to support idris.
 "
 " author: raichoo (raichoo@googlemail.com)
-" date: Mar 12 2013
+" date: Mar 20 2013
 
 syn match idrisModule "\<\(module\|namespace\)\>"
 syn match idrisImport "\<import\>"
 syn match idrisStructure "\<\(class\|\(co\)\?data\|instance\|where\|record\|dsl\)\>"
 syn match idrisVisibility "\<\(public\|abstract\|private\)\>"
 syn match idrisBlock "\<\(parameters\|mutual\|postulate\|using\)\>"
 syn match idrisAnnotation "\<\(total\|partial\|auto\|impossible\|static\|implicit\)\>"
-syn match idrisStatement "\<\(do\|case\|of\|let\|in\|with\)\>"
+syn match idrisStatement "\<\(do\|case\|of\|rewrite\|let\|in\|with\)\>"
 syn match idrisSyntax "\(pattern \+\|term \+\)\?syntax"
 syn match idrisConditional "\<\(if\|then\|else\)\>"
 syn match idrisTactic contained "\<\(intros\?\|rewrite\|exact\|refine\|trivial\|let\|focus\|try\|compute\|solve\|attack\|reflect\)\>"
@@ -28,7 +28,7 @@ syn match idrisLink "%\(lib\|link\|include\)"
 syn match idrisDirective "%\(access\|default\|assert_total\)"
 syn match idrisDSL "\(lambda\|variable\|\index_first\|index_next\)"
 syn region idrisString start=+"+ skip=+\\\\\|\\"+ end=+"+
-syn region idrisBlockComment start="{-" end="-}"
+syn region idrisBlockComment start="{-" end="-}" contains=idrisBlockComment
 syn region idrisProofBlock start="\(default\s\+\)\?\(proof\|tactics\) *{" end="}" contains=idrisTactic
 
 syn match idrisBadLeadingWhiteSpace "^\s*\t\+"

effects/Effect/Exception.idr

@@ -17,6 +17,9 @@ instance Show a => Handler (Exception a) IO where
 instance Handler (Exception a) (IOExcept a) where
      handle _ (Raise e) k = ioM (return (Left e))
 
+instance Handler (Exception a) (Either a) where
+     handle _ (Raise e) k = Left e
+
 EXCEPTION : Type -> EFFECT
 EXCEPTION t = MkEff () (Exception t) 
 

effects/Effect/StdIO.idr

@@ -19,9 +19,6 @@ instance Handler StdIO (IOExcept a) where
 
 data IOStream a = MkStream (List String -> (a, List String))
 
-injStream : a -> IOStream a
-injStream v = MkStream (\x => (v, []))
-
 instance Handler StdIO IOStream where
     handle () (PutStr s) k
        = MkStream (\x => case k () () of
@@ -55,5 +52,9 @@ mkStrFn : Env IOStream xs ->
           List String -> (a, List String)
 mkStrFn {a} env p input = case mkStrFn' of
                                MkStream f => f input
-  where mkStrFn' : IOStream a
+  where injStream : a -> IOStream a
+        injStream v = MkStream (\x => (v, []))
+        mkStrFn' : IOStream a
         mkStrFn' = runWith injStream env p
+
+

effects/Effects.idr

@@ -100,8 +100,7 @@ data EffM : (m : Type -> Type) ->
             List EFFECT -> List EFFECT -> Type -> Type where
      value   : a -> EffM m xs xs a
      ebind   : EffM m xs xs' a -> (a -> EffM m xs' xs'' b) -> EffM m xs xs'' b
-     effect  : {a, b: _} -> {e : Effect} ->
-               (prf : EffElem e a xs) -> 
+     effect  : (prf : EffElem e a xs) -> 
                (eff : e a b t) -> 
                EffM m xs (updateResTy xs prf eff) t
      lift    : (prf : SubList ys xs) ->
@@ -189,6 +188,9 @@ runEnv env prog = eff env prog (\env, r => pure (env, r))
 runPure : Env id xs -> EffM id xs xs' a -> a
 runPure env prog = eff env prog (\env, r => r)
 
+runPureEnv : Env id xs -> EffM id xs xs' a -> (Env id xs', a)
+runPureEnv env prog = eff env prog (\env, r => (env, r))
+
 runWith : (a -> m a) -> Env m xs -> EffM m xs xs' a -> m a
 runWith inj env prog = eff env prog (\env, r => inj r)
 

java/executable_pom_template.xml

@@ -17,6 +17,7 @@
     	<artifactId>idris</artifactId>
     	<version>$RTS-VERSION$</version>
     </dependency>
+$DEPENDENCIES$
   </dependencies>