idris 0.9.18.1 → 0.9.19

raw patch · 217 files changed

+7672/−4024 lines, 217 filesdep −lensdep −xmldep ~annotated-wl-pprintdep ~blaze-htmldep ~blaze-markupPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependencies removed: lens, xml

Dependency ranges changed: annotated-wl-pprint, blaze-html, blaze-markup, directory, utf8-string

API changes (from Hackage documentation)

Files

• Makefile +4/−1
• idris.cabal +39/−15
• jsrts/Runtime-browser.js +0/−1
• jsrts/Runtime-common.js +27/−13
• jsrts/Runtime-node.js +19/−0
• libs/base/Control/Monad/State.idr +1/−1
• libs/base/Data/Complex.idr +9/−2
• libs/base/Data/Fin.idr +2/−0
• libs/base/Data/HVect.idr +22/−5
• libs/base/Data/List.idr +8/−0
• libs/base/Data/Vect.idr +27/−0
• libs/base/Data/VectType.idr +8/−3
• libs/base/Language/Reflection/Utils.idr +138/−103
• libs/base/System.idr +4/−19
• libs/base/System/Concurrency/Raw.idr +12/−2
• libs/base/base.ipkg +1/−1
• libs/contrib/Control/Algebra.idr +10/−10
• libs/contrib/Control/Algebra/NumericInstances.idr +9/−0
• libs/contrib/Data/Fun.idr +1/−1
• libs/contrib/Data/Heap.idr +2/−2
• libs/contrib/Data/Matrix.idr +32/−124
• libs/contrib/Data/Matrix/Algebraic.idr +149/−0
• libs/contrib/Data/Matrix/Numeric.idr +129/−0
• libs/contrib/Data/Nat.idr +0/−166
• libs/contrib/Data/Nat/DivMod.idr +60/−0
• libs/contrib/Data/Nat/DivMod/IteratedSubtraction.idr +167/−0
• libs/contrib/System/Concurrency/Process.idr +4/−2
• libs/contrib/contrib.ipkg +3/−2
• libs/effects/Effect/Logging/Default.idr +57/−0
• libs/effects/Effect/Logging/Level.idr +49/−0
• libs/effects/Effect/Logging/Simple.idr +48/−0
• libs/effects/Effect/Monad.idr +19/−12
• libs/effects/Effect/Random.idr +0/−1
• libs/effects/Effect/System.idr +2/−2
• libs/effects/Effect/Trans.idr +20/−0
• libs/effects/Effects.idr +2/−4
• libs/effects/effects.ipkg +15/−4
• libs/prelude/Builtins.idr +4/−1
• libs/prelude/Decidable/Equality.idr +22/−1
• libs/prelude/IO.idr +34/−7
• libs/prelude/Language/Reflection.idr +63/−32
• libs/prelude/Language/Reflection/Elab.idr +184/−40
• libs/prelude/Language/Reflection/Errors.idr +1/−0
• libs/prelude/Prelude.idr +27/−310
• libs/prelude/Prelude/Applicative.idr +24/−0
• libs/prelude/Prelude/Basics.idr +3/−3
• libs/prelude/Prelude/Cast.idr +11/−5
• libs/prelude/Prelude/Classes.idr +6/−0
• libs/prelude/Prelude/File.idr +156/−0
• libs/prelude/Prelude/Interactive.idr +142/−0
• libs/prelude/Prelude/List.idr +129/−138
• libs/prelude/Prelude/Maybe.idr +6/−2
• libs/prelude/Prelude/Monad.idr +19/−1
• libs/prelude/Prelude/Nat.idr +80/−299
• libs/prelude/Prelude/Show.idr +190/−0
• libs/prelude/Prelude/Strings.idr +55/−14
• libs/prelude/prelude.ipkg +2/−1
• rts/idris_rts.c +35/−3
• rts/idris_rts.h +7/−1
• rts/idris_stdfgn.c +3/−2
• rts/idris_stdfgn.h +3/−1
• rts/windows/idris_stdfgn.c +2/−2
• src/IRTS/CodegenC.hs +5/−1
• src/IRTS/CodegenJavaScript.hs +90/−199
• src/IRTS/Compiler.hs +7/−7
• src/IRTS/JavaScript/AST.hs +5/−1
• src/Idris/ASTUtils.hs +4/−1
• src/Idris/AbsSyntax.hs +254/−203
• src/Idris/AbsSyntaxTree.hs +497/−255
• src/Idris/CaseSplit.hs +44/−38
• src/Idris/Chaser.hs +20/−20
• src/Idris/CmdOptions.hs +10/−5
• src/Idris/Colours.hs +22/−8
• src/Idris/Completion.hs +1/−1
• src/Idris/Core/Binary.hs +14/−4
• src/Idris/Core/CaseTree.hs +2/−0
• src/Idris/Core/DeepSeq.hs +12/−2
• src/Idris/Core/Elaborate.hs +78/−41
• src/Idris/Core/Evaluate.hs +46/−33
• src/Idris/Core/Execute.hs +1/−1
• src/Idris/Core/ProofState.hs +17/−8
• src/Idris/Core/TT.hs +122/−24
• src/Idris/Core/Typecheck.hs +4/−4
• src/Idris/Core/Unify.hs +12/−0
• src/Idris/Core/WHNF.hs +208/−0
• src/Idris/Coverage.hs +23/−21
• src/Idris/DSL.hs +31/−29
• src/Idris/DataOpts.hs +1/−1
• src/Idris/DeepSeq.hs +27/−20
• src/Idris/Delaborate.hs +172/−84
• src/Idris/Directives.hs +19/−9
• src/Idris/Docs.hs +37/−17
• src/Idris/Docstrings.hs +1/−2
• src/Idris/Elab/AsPat.hs +1/−1
• src/Idris/Elab/Class.hs +18/−18
• src/Idris/Elab/Clause.hs +58/−40
• src/Idris/Elab/Data.hs +25/−25
• src/Idris/Elab/Instance.hs +16/−16
• src/Idris/Elab/Provider.hs +4/−4
• src/Idris/Elab/Record.hs +31/−27
• src/Idris/Elab/RunElab.hs +49/−0
• src/Idris/Elab/Term.hs +458/−373
• src/Idris/Elab/Transform.hs +7/−3
• src/Idris/Elab/Type.hs +8/−7
• src/Idris/Elab/Utils.hs +26/−28
• src/Idris/Elab/Value.hs +17/−9
• src/Idris/ElabDecls.hs +27/−22
• src/Idris/ElabQuasiquote.hs +11/−9
• src/Idris/ErrReverse.hs +1/−1
• src/Idris/Error.hs +8/−7
• src/Idris/Help.hs +2/−2
• src/Idris/IBC.hs +132/−78
• src/Idris/IdeMode.hs +9/−2
• src/Idris/IdrisDoc.hs +9/−8
• src/Idris/Imports.hs +2/−1
• src/Idris/Inliner.hs +1/−1
• src/Idris/Interactive.hs +125/−31
• src/Idris/Output.hs +59/−12
• src/Idris/ParseData.hs +31/−29
• src/Idris/ParseExpr.hs +257/−149
• src/Idris/ParseHelpers.hs +27/−2
• src/Idris/ParseOps.hs +5/−5
• src/Idris/Parser.hs +306/−95
• src/Idris/PartialEval.hs +33/−5
• src/Idris/ProofSearch.hs +288/−27
• src/Idris/Prover.hs +299/−116
• src/Idris/Providers.hs +1/−1
• src/Idris/REPL.hs +94/−63
• src/Idris/REPLParser.hs +38/−21
• src/Idris/Reflection.hs +255/−97
• src/Pkg/PParser.hs +1/−4
• src/Pkg/Package.hs +58/−51
• src/Util/ScreenSize.hs +1/−1
• src/Util/System.hs +21/−3
• src/Util/Zlib.hs +0/−15
• test/Makefile +1/−1
• test/basic006/expected +4/−4
• test/basic009/expected +1/−1
• test/classes001/expected +2/−0
• test/disambig001/disambig001.idr +0/−12
• test/disambig001/expected +0/−1
• test/disambig001/run +0/−4
• test/docs001/expected +1/−0
• test/docs002/expected +3/−0
• test/docs003/expected +4/−3
• test/dsl002/Resimp.idr +1/−1
• test/dsl004/Door0.idr +33/−0
• test/dsl004/Door1.idr +37/−0
• test/dsl004/Door2.idr +37/−0
• test/dsl004/Door3.idr +30/−0
• test/dsl004/IOu.idr +19/−0
• test/dsl004/expected +0/−0
• test/dsl004/run +5/−0
• test/effects005/defaultlog.idr +18/−0
• test/effects005/expected +5/−0
• test/effects005/run +6/−0
• test/effects005/simplelog.idr +14/−0
• test/error003/expected +1/−2
• test/error004/FunErrTest.idr +8/−7
• test/error004/expected +5/−8
• test/error004/idx.idr +4/−0
• test/error005/expected +10/−10
• test/idrisdoc009/expected +1/−1
• test/interactive003/expected +1/−0
• test/interactive003/input +1/−0
• test/interactive003/interactive003.idr +5/−0
• test/interactive005/expected +9/−6
• test/interactive008/expected +204/−0
• test/interactive008/input +9/−0
• test/interactive008/run +2/−0
• test/interactive009/expected +1/−0
• test/interactive009/input +1/−0
• test/interactive009/interactive009.idr +27/−0
• test/interactive009/run +3/−0
• test/io003/test018.idr +3/−1
• test/io003/test018a.idr +2/−0
• test/meta001/Finite.idr +26/−24
• test/meta002/Tacs.idr +8/−4
• test/meta002/expected +2/−2
• test/primitives002/expected +13/−13
• test/primitives002/run +33/−29
• test/proof001/test029.idr +1/−1
• test/proof002/expected +7/−7
• test/proof003/test015.idr +1/−3
• test/proof007/expected +2/−2
• test/quasiquote001/expected +3/−3
• test/quasiquote003/expected +1/−1
• test/quasiquote004/expected +1/−1
• test/quasiquote006/expected +3/−3
• test/reg001/reg001.idr +1/−0
• test/reg003/expected +3/−3
• test/reg007/expected +5/−5
• test/reg010/expected +1/−1
• test/reg023/expected +3/−3
• test/reg034/expected +2/−2
• test/reg044/expected +5/−5
• test/reg049/expected +2/−2
• test/reg054/expected +10/−9
• test/reg054/reg054.idr +3/−0
• test/reg055/expected +5/−5
• test/reg066/expected +0/−0
• test/reg066/reg066.idr +7/−0
• test/reg066/run +3/−0
• test/syntax001/Syntax.idr +8/−0
• test/syntax001/SyntaxOk.idr +6/−0
• test/syntax001/SyntaxTest.idr +5/−0
• test/syntax001/expected +12/−0
• test/syntax001/run +4/−0
• test/syntax002/expected +2/−0
• test/syntax002/run +4/−0
• test/syntax002/syntax002.idr +22/−0
• test/tactics001/Tactics.idr +1/−1
• test/totality007/expected +2/−0
• test/tutorial006/expected +15/−16
• test/unique001/expected +6/−6
• test/unique002/expected +2/−2
• test/unique003/expected +2/−2

@@ -1,4 +1,4 @@-.PHONY: build configure doc install linecount nodefault pinstall lib_clean relib test_c test lib_doc lib_doc_clean user_doc_html user_doc_pdf user_docs+.PHONY: build configure doc install linecount nodefault pinstall lib_clean relib fast test_c test lib_doc lib_doc_clean user_doc_html user_doc_pdf user_docs  include config.mk -include custom.mk@@ -65,6 +65,9 @@  user_doc_pdf: 	$(MAKE) -C docs latexpdf++fast:+	$(CABAL) install $(CABALFLAGS) --ghc-option=-O0  dist/setup-config: 	$(CABAL) configure $(CABALFLAGS)

@@ -1,5 +1,5 @@ Name:           idris-Version:        0.9.18.1+Version:        0.9.19 License:        BSD3 License-file:   LICENSE Author:         Edwin Brady@@ -114,8 +114,11 @@                        libs/contrib/Classes/*.idr                        libs/contrib/Control/*.idr                        libs/contrib/Control/Isomorphism/*.idr-		       libs/contrib/Control/Algebra/*.idr+                       libs/contrib/Control/Algebra/*.idr                        libs/contrib/Data/*.idr+                       libs/contrib/Data/Nat/*.idr+                       libs/contrib/Data/Nat/DivMod/*.idr+                       libs/contrib/Data/Matrix/*.idr                        libs/contrib/Decidable/*.idr                        libs/contrib/Network/*.idr                        libs/contrib/System/Concurrency/*.idr@@ -123,6 +126,7 @@                        libs/effects/Makefile                        libs/effects/effects.ipkg                        libs/effects/Effect/*.idr+		       libs/effects/Effect/Logging/*.idr                        libs/effects/*.idr                         test/Makefile@@ -317,6 +321,9 @@                        test/reg065/run                        test/reg065/*.idr                        test/reg065/expected+                       test/reg066/run+                       test/reg066/*.idr+                       test/reg066/expected                         test/basic001/run                        test/basic001/*.idr@@ -383,9 +390,6 @@                        test/delab001/expected                        test/delab001/input -                       test/disambig001/run-                       test/disambig001/*.idr-                       test/disambig001/expected                        test/disambig002/run                        test/disambig002/*.idr                        test/disambig002/expected@@ -400,6 +404,9 @@                        test/dsl003/run                        test/dsl003/*.idr                        test/dsl003/expected+                       test/dsl004/run+                       test/dsl004/*.idr+                       test/dsl004/expected                         test/effects001/run                        test/effects001/*.idr@@ -416,7 +423,11 @@                        test/effects004/*.idr                        test/effects004/expected                        test/effects004/input+                       test/effects005/run+                       test/effects005/*.idr+                       test/effects005/expected +                        test/error001/run                        test/error001/*.idr                        test/error001/expected@@ -526,6 +537,13 @@                        test/interactive007/run                        test/interactive007/input                        test/interactive007/expected+                       test/interactive008/run+                       test/interactive008/input+                       test/interactive008/expected+                       test/interactive009/run+                       test/interactive009/input+                       test/interactive009/*.idr+                       test/interactive009/expected                         test/io001/run                        test/io001/*.idr@@ -638,6 +656,13 @@                        test/sugar005/*.idr                        test/sugar005/expected +                       test/syntax001/run+                       test/syntax001/*.idr+                       test/syntax001/expected+                       test/syntax002/run+                       test/syntax002/*.idr+                       test/syntax002/expected+                        test/tactics001/run                        test/tactics001/*.idr                        test/tactics001/expected@@ -770,6 +795,7 @@                 , Idris.Core.TT                 , Idris.Core.Typecheck                 , Idris.Core.Unify+                , Idris.Core.WHNF                  , Idris.Elab.Utils                 , Idris.Elab.Type@@ -780,6 +806,7 @@                 , Idris.Elab.Class                 , Idris.Elab.Instance                 , Idris.Elab.Provider+                , Idris.Elab.RunElab                 , Idris.Elab.Transform                 , Idris.Elab.Value                 , Idris.Elab.Term@@ -858,7 +885,6 @@   Other-modules:                   Util.Pretty                 , Util.Net-                , Util.Zlib                  , Pkg.PParser @@ -868,22 +894,21 @@                 , Tools_idris    Build-depends:  base >=4 && <5-                , annotated-wl-pprint >= 0.5.3 && < 0.7+                , annotated-wl-pprint >= 0.7 && < 0.8                 , ansi-terminal < 0.7                 , ansi-wl-pprint < 0.7                 , base64-bytestring < 1.1                 , binary >= 0.7 && < 0.8-                , blaze-html >= 0.6.1.3 && < 0.8-                , blaze-markup >= 0.5.2.1 && < 0.6.3.0+                , blaze-html >= 0.6.1.3 && < 0.9+                , blaze-markup >= 0.5.2.1 && < 0.8                 , bytestring < 0.11                 , cheapskate < 0.2                 , containers >= 0.5 && < 0.6                 , deepseq < 1.5-                , directory >= 1.2.2.0 && < 1.3+                , directory >= 1.2.2.0 && < 1.2.3.0 || > 1.2.3.0                 , filepath < 1.5                 , fingertree >= 0.1 && < 0.2                 , haskeline >= 0.7 && < 0.8-                , lens >= 4.1.1 && < 4.10                 , mtl >= 2.1 && < 2.3                 , network < 2.7                 , optparse-applicative >= 0.11 && < 0.12@@ -898,10 +923,9 @@                 , trifecta >= 1.1 && < 1.6                 , uniplate >=1.6 && < 1.7                 , unordered-containers < 0.3-                , utf8-string < 0.4+                , utf8-string <= 1                 , vector < 0.11                 , vector-binary-instances < 0.3-                , xml < 1.4                 , zip-archive > 0.2.3.5 && < 0.2.4                 , zlib < 0.6                 , safe@@ -984,7 +1008,7 @@                 , transformers    ghc-prof-options: -auto-all -caf-all-  ghc-options:      -threaded -rtsopts -funbox-strict-fields -O2+  ghc-options:      -threaded -rtsopts -funbox-strict-fields  Executable idris-node   Main-is:        Main.hs@@ -997,4 +1021,4 @@                 , transformers    ghc-prof-options: -auto-all -caf-all-  ghc-options:      -threaded -rtsopts -funbox-strict-fields -O2+  ghc-options:      -threaded -rtsopts -funbox-strict-fields

@@ -2,7 +2,6 @@   console.log(s); }; - var i$systemInfo = function(index) {   switch(index) {     case 0:

@@ -1,6 +1,6 @@ /** @constructor */ var i$VM = function() {-  this.valstack = [];+  this.valstack = {};   this.valstack_top = 0;   this.valstack_base = 0; @@ -63,26 +63,29 @@  var i$ffiWrap = function(fid,oldbase,myoldbase) {   return function() {+    var oldstack = i$callstack;     i$callstack = [];      var res = fid;      for(var i = 0; i < (arguments.length ? arguments.length : 1); ++i) {-      i$valstack_top += 1;-      i$valstack[i$valstack_top] = res;-      i$valstack[i$valstack_top + 1] = arguments[i];-      i$SLIDE(2);-      i$valstack_top = i$valstack_base + 2;-      i$CALL(_idris__123_APPLY0_125_,[oldbase])-      while (i$callstack.length) {-        var func = i$callstack.pop();-        var args = i$callstack.pop();-        func.apply(this,args);+      while (res instanceof i$CON) {+        i$valstack_top += 1;+        i$valstack[i$valstack_top] = res;+        i$valstack[i$valstack_top + 1] = arguments[i];+        i$SLIDE(2);+        i$valstack_top = i$valstack_base + 2;+        i$CALL(_idris__123_APPLY0_125_,[oldbase])+        while (i$callstack.length) {+          var func = i$callstack.pop();+          var args = i$callstack.pop();+          func.apply(this,args);+        }+        res = i$ret;       }-      res = i$ret;     } -    i$callstack = i$vm.callstack;+    i$callstack = oldstack;      return i$ret;   }@@ -100,4 +103,15 @@     return chr;   else     return String.fromCharCode(chr);+}++var i$RUN = function () {+  for (var i = 0; i < 10000 && i$callstack.length; i++) {+    var func = i$callstack.pop();+    var args = i$callstack.pop();+    func.apply(this,args);+  };++  if (i$callstack.length)+    setTimeout(i$RUN, 0); }

@@ -5,6 +5,25 @@   }; })(); +var i$getLine = (function() {+  var fs = require( "fs" )++  return function() {+    var ret = "";++    while(true) {+      var b = new Buffer(1);+      fs.readSync(0, b, 0, 1 )+      if (b[0] == 10)+        break;+      else+        ret += String.fromCharCode(b[0]);+    }++    return ret;+  };+})();+ var i$systemInfo = function(index) {   var os = require('os')     switch(index) {

@@ -1,7 +1,7 @@ module Control.Monad.State  import public Control.Monad.Identity-import Control.Monad.Trans+import public Control.Monad.Trans  %access public 

@@ -22,8 +22,9 @@     (==) a b = realPart a == realPart b && imagPart a == imagPart b  instance Show a => Show (Complex a) where-    show (r:+i) = "("++show r++":+"++show i++")"-+    showPrec d (r :+ i) = showParens (d >= plus_i) $ showPrec plus_i r ++ " :+ " ++ showPrec plus_i i+      where plus_i : Prec+            plus_i = User 6   -- when we have a type class 'Fractional' (which contains Float and Double),@@ -58,6 +59,12 @@  conjugate : Num a => Complex a -> Complex a conjugate (r:+i) = (r :+ (0-i))++instance Functor Complex where+  map f (r :+ i) = f r :+ f i++instance Neg a => Neg (Complex a) where+  negate = map negate  -- We can't do "instance Num a => Num (Complex a)" because -- we need "abs" which needs "magnitude" which needs "sqrt" which needs Float

@@ -129,6 +129,8 @@                           | Nothing = Nothing natToFin _ _ = Nothing +||| Convert an `Integer` to a `Fin`, provided the integer is within bounds.+||| @n The upper bound of the Fin integerToFin : Integer -> (n : Nat) -> Maybe (Fin n) integerToFin x Z = Nothing -- make sure 'n' is concrete, to save reduction! integerToFin x n = if x >= 0 then natToFin (cast x) n else Nothing

@@ -1,7 +1,6 @@ module Data.HVect -import Data.Fin-import Data.Vect+import public Data.Vect  %access public %default total@@ -42,6 +41,24 @@ instance (Eq t, Eq (HVect ts)) => Eq (HVect (t::ts)) where   (x::xs) == (y::ys) = x == y && xs == ys +total+hvectInjective1 : {xs, ys: HVect ts} -> {x, y:a} -> x :: xs = y :: ys -> x = y+hvectInjective1 Refl = Refl++total+hvectInjective2 : {xs, ys: HVect ts} -> {x, y:a} -> x :: xs = y :: ys -> xs = ys+hvectInjective2 Refl = Refl++instance DecEq (HVect []) where+  decEq [] [] = Yes Refl++instance (DecEq t, DecEq (HVect ts)) => DecEq (HVect (t::ts)) where+  decEq (x::xs) (y::ys) with (decEq x y)+    decEq (z::xs) (z::ys) | Yes Refl with (decEq xs ys)+      decEq (z::zs) (z::zs) | Yes Refl | Yes Refl = Yes Refl+      decEq (z::xs) (z::ys) | Yes Refl | No ctr = No (ctr . hvectInjective2)+    decEq (x::xs) (y::ys) | No ctr = No (ctr . hvectInjective1)+ class Shows (k : Nat) (ts : Vect k Type) where   shows : HVect ts -> Vect k String @@ -56,17 +73,17 @@  ||| Extract an arbitrary element of the correct type. ||| @ t the goal type-get : {default tactics { search 100; } p : Elem t ts} -> HVect ts -> t+get : {auto p : Elem t ts} -> HVect ts -> t get {p = Here} (x::xs) = x get {p = There p'} (x::xs) = get {p = p'} xs  ||| Replace an element with the correct type.-put : {default tactics { search 100; } p : Elem t ts} -> t -> HVect ts -> HVect ts+put : {auto p : Elem t ts} -> t -> HVect ts -> HVect ts put {p = Here} y (x::xs) = y :: xs put {p = There p'} y (x::xs) = x :: put {p = p'} y xs  ||| Update an element with the correct type.-update : {default tactics { search 100; } p : Elem t ts} -> (t -> u) -> HVect ts -> HVect (replaceByElem ts p u)+update : {auto p : Elem t ts} -> (t -> u) -> HVect ts -> HVect (replaceByElem ts p u) update {p = Here} f (x::xs) = f x :: xs update {p = There p'} f (x::xs) = x :: update {p = p'} f xs 

@@ -37,6 +37,14 @@         mkNo f g Here = f Refl         mkNo f g (There x) = g x +||| Remove the element at the given position.+|||+||| @xs The list to be removed from+||| @p A proof that the element to be removed is in the list+dropElem : (xs : List a) -> (p : Elem x xs) -> List a+dropElem (x :: ys) Here = ys +dropElem (x :: ys) (There p) = x :: dropElem ys p+ ||| The intersectBy function returns the intersect of two lists by user-supplied equality predicate. intersectBy : (a -> a -> Bool) -> List a -> List a -> List a intersectBy eq xs ys = [x | x <- xs, any (eq x) ys]

@@ -52,3 +52,30 @@ mapElem Here = Here mapElem (There e) = There (mapElem e) +-- Some convenience functions for testing lengths++||| If the given Vect is the required length, return a Vect with that+||| length in its type, otherwise return Nothing+||| @len the required length+||| @xs the vector with the desired length+-- Needs to be Maybe rather than Dec, because if 'n' is unequal to m, we +-- only know we don't know how to make a Vect n a, not that one can't exist.+isLength : {m : Nat} -> -- expected at run-time+           (len : Nat) -> (xs : Vect m a) -> Maybe (Vect len a)+isLength {m} len xs with (decEq m len)+  isLength {m = m} m xs | (Yes Refl) = Just xs+  isLength {m = m} len xs | (No contra) = Nothing++||| If the given Vect is at least the required length, return a Vect with+||| at least that length in its type, otherwise return Nothing+||| @len the required length+||| @xs the vector with the desired length+overLength : {m : Nat} -> -- expected at run-time+             (len : Nat) -> (xs : Vect m a) -> Maybe (p ** Vect (plus p len) a)+overLength {m} n xs with (cmp m n)+  overLength {m = m} (plus m (S y)) xs | (CmpLT y) = Nothing+  overLength {m = m} m xs | CmpEQ+         = Just (0 ** xs)+  overLength {m = plus n (S x)} n xs | (CmpGT x)+         = Just (S x ** rewrite plusCommutative (S x) n in xs)+

@@ -1,6 +1,6 @@ module Data.VectType -import Data.Fin+import public Data.Fin  %access public %default total@@ -9,9 +9,14 @@  infixr 7 :: -%elim data Vect : Nat -> Type -> Type where+||| Vectors: Generic lists with explicit length in the type+%elim +data Vect : Nat -> Type -> Type where+  ||| Empty vector    Nil  : Vect Z a-  (::) : (x : a) -> (xs : Vect n a) -> Vect (S n) a+  ||| A non-empty vector of length `S k`, consisting of a head element and +  ||| the rest of the list, of length `k`.+  (::) : (x : a) -> (xs : Vect k a) -> Vect (S k) a  -- Hints for interactive editing %name Vect xs,ys,zs,ws

@@ -64,23 +64,23 @@  mutual   instance Show SpecialName where-    show (WhereN i n1 n2) = "(WhereN " ++ show i ++ " " ++-                            show n1 ++ " " ++ show n2 ++ ")"-    show (WithN i n) = "(WithN " ++ show i ++ " " ++ show n ++ ")"-    show (InstanceN i ss) = "(InstanceN " ++ show i ++ " " ++ show ss ++ ")"-    show (ParentN n s) = "(ParentN " ++ show n ++ " " ++ show s ++ ")"-    show (MethodN n) = "(MethodN " ++ show n ++ ")"-    show (CaseN n) = "(CaseN " ++ show n ++ ")"-    show (ElimN n) = "(ElimN " ++ show n ++ ")"-    show (InstanceCtorN n) = "(InstanceCtorN " ++ show n ++ ")"-    show (MetaN parent meta) = "(MetaN " ++ show parent ++ " " ++ show meta ++ ")"+    showPrec d (WhereN i n1 n2) = showCon d "WhereN" $ showArg i +++                            showArg n1 ++ showArg n2+    showPrec d (WithN i n) = showCon d "WithN" $ showArg i ++ showArg n+    showPrec d (InstanceN i ss) = showCon d "InstanceN" $ showArg i ++ showArg ss+    showPrec d (ParentN n s) = showCon d "ParentN" $ showArg n ++ showArg s+    showPrec d (MethodN n) = showCon d "MethodN" $ showArg n+    showPrec d (CaseN n) = showCon d "CaseN" $ showArg n+    showPrec d (ElimN n) = showCon d "ElimN" $ showArg n+    showPrec d (InstanceCtorN n) = showCon d "InstanceCtorN" $ showArg n+    showPrec d (MetaN parent meta) = showCon d "MetaN" $ showArg parent ++ showArg meta    instance Show TTName where-    show (UN str)   = "(UN " ++ show str ++ ")"-    show (NS n ns)  = "(NS " ++ show n ++ " " ++ show ns ++ ")"-    show (MN i str) = "(MN " ++ show i ++ " " ++ show str ++ ")"-    show (SN sn)    = "(SN " ++ assert_total (show sn) ++ ")"-    show NErased    = "NErased"+    showPrec d (UN str)   = showCon d "UN" $ showArg str+    showPrec d (NS n ns)  = showCon d "NS" $ showArg n ++ showArg ns+    showPrec d (MN i str) = showCon d "MN" $ showArg i ++ showArg str+    showPrec d (SN sn)    = showCon d "SN" $ assert_total (showArg sn)+    showPrec d NErased    = "NErased"  mutual   instance Eq TTName where@@ -104,28 +104,44 @@     _                   == _                     = False  instance Show TTUExp where-  show (UVar i) = "(UVar " ++ show i ++ ")"-  show (UVal i) = "(UVal " ++ show i ++ ")"+  showPrec d (UVar i) = showCon d "UVar" $ showArg i+  showPrec d (UVal i) = showCon d "UVal" $ showArg i  instance Eq TTUExp where   (UVar i) == (UVar j) = i == j   (UVal i) == (UVal j) = i == j   x        == y        = False +instance Show NativeTy where+  show IT8  = "IT8"+  show IT16 = "IT16"+  show IT32 = "IT32"+  show IT64 = "IT64"++instance Show IntTy where+  showPrec d (ITFixed t) = showCon d "ITFixed" $ showArg t+  showPrec d ITNative    = "ITNative"+  showPrec d ITBig       = "ITBig"+  showPrec d ITChar      = "ITChar"++instance Show ArithTy where+  showPrec d (ATInt t) = showCon d "ATInt" $ showArg t+  showPrec d ATFloat   = "ATFloat"+ instance Show Const where-  show (I i)      = "(I " ++ show i ++ ")"-  show (BI n)     = "(BI " ++ show n ++ ")"-  show (Fl f)     = "(Fl " ++ show f ++ ")"-  show (Ch c)     = "(Ch " ++ show c ++ ")"-  show (Str str)  = "(Str " ++ show str ++ ")"-  show (B8 b)     = "(B8 ...)"-  show (B16 b)    = "(B16 ...)"-  show (B32 b)    = "(B32 ...)"-  show (B64 b)    = "(B64 ...)"-  show (AType x) = "(AType ...)"-  show StrType = "StrType"-  show VoidType = "VoidType"-  show Forgot = "Forgot"+  showPrec d (I i)      = showCon d "I" $ showArg i+  showPrec d (BI n)     = showCon d "BI" $ showArg n+  showPrec d (Fl f)     = showCon d "Fl" $ showArg f+  showPrec d (Ch c)     = showCon d "Ch" $ showArg c+  showPrec d (Str str)  = showCon d "Str" $ showArg str+  showPrec d (B8 b)     = showCon d "B8" $ showArg b+  showPrec d (B16 b)    = showCon d "B16" $ showArg b+  showPrec d (B32 b)    = showCon d "B32" $ showArg b+  showPrec d (B64 b)    = showCon d "B64" $ showArg b+  showPrec d (AType x)  = showCon d "AType" $ showArg x+  showPrec d StrType    = "StrType"+  showPrec d VoidType   = "VoidType"+  showPrec d Forgot     = "Forgot"  instance Eq NativeTy where   IT8  == IT8  = True@@ -164,10 +180,10 @@   instance Show NameType where-  show Bound = "Bound"-  show Ref = "Ref"-  show (DCon t ar) = "(DCon " ++ show t ++ " " ++ show ar ++ ")"-  show (TCon t ar) = "(TCon " ++ show t ++ " " ++ show ar ++ ")"+  showPrec d Bound = "Bound"+  showPrec d Ref = "Ref"+  showPrec d (DCon t ar) = showCon d "DCon" $ showArg t ++ showArg ar+  showPrec d (TCon t ar) = showCon d "TCon" $ showArg t ++ showArg ar  instance Eq NameType where   Bound       == Bound          = True@@ -177,15 +193,15 @@   x           == y              = False  instance (Show a) => Show (Binder a) where-  show (Lam t) = "(Lam " ++ show t ++ ")"-  show (Pi t _) = "(Pi " ++ show t ++ ")"-  show (Let t1 t2) = "(Let " ++ show t1 ++ " " ++ show t2 ++ ")"-  show (NLet t1 t2) = "(NLet " ++ show t1 ++ " " ++ show t2 ++ ")"-  show (Hole t) = "(Hole " ++ show t ++ ")"-  show (GHole t) = "(GHole " ++ show t ++ ")"-  show (Guess t1 t2) = "(Guess " ++ show t1 ++ " " ++ show t2 ++ ")"-  show (PVar t) = "(PVar " ++ show t ++ ")"-  show (PVTy t) = "(PVTy " ++ show t ++ ")"+  showPrec d (Lam t) = showCon d "Lam" $ showArg t+  showPrec d (Pi t1 t2) = showCon d "Pi" $ showArg t1 ++ showArg t2+  showPrec d (Let t1 t2) = showCon d "Let" $ showArg t1 ++ showArg t2+  showPrec d (NLet t1 t2) = showCon d "NLet" $ showArg t1 ++ showArg t2+  showPrec d (Hole t) = showCon d "Hole" $ showArg t+  showPrec d (GHole t) = showCon d "GHole" $ showArg t+  showPrec d (Guess t1 t2) = showCon d "Guess" $ showArg t1 ++ showArg t2+  showPrec d (PVar t) = showCon d "PVar" $ showArg t+  showPrec d (PVTy t) = showCon d "PVTy" $ showArg t  instance (Eq a) => Eq (Binder a) where   (Lam t)       == (Lam t')         = t == t'@@ -200,17 +216,17 @@   x             == y                = False  instance Show TT where-  show = my_show-    where %assert_total my_show : TT -> String-          my_show (P nt n t) = "(P " ++ show nt ++ " " ++ show n ++ " " ++ show t ++ ")"-          my_show (V i) = "(V " ++ show i ++ ")"-          my_show (Bind n b t) = "(Bind " ++ show n ++ " " ++ show b ++ " " ++ show t ++ ")"-          my_show (App t1 t2) = "(App " ++ show t1 ++ " " ++ show t2 ++ ")"-          my_show (TConst c) = "(TConst " ++ show c ++ ")"-          my_show (Proj tm i) = "(Proj " ++ show tm ++ " " ++ show i ++ ")"-          my_show Erased = "Erased"-          my_show Impossible = "Impossible"-          my_show (TType u) = "(TType " ++ show u ++ ")"+  showPrec = my_show+    where %assert_total my_show : Prec -> TT -> String+          my_show d (P nt n t) = showCon d "P" $ showArg nt ++ showArg n ++ showArg t+          my_show d (V i) = showCon d "V" $ showArg i+          my_show d (Bind n b t) = showCon d "Bind" $ showArg n ++ showArg b ++ showArg t+          my_show d (App t1 t2) = showCon d "App" $ showArg t1 ++ showArg t2+          my_show d (TConst c) = showCon d "TConst" $ showArg c+          my_show d (Proj tm i) = showCon d "Proj" $ showArg tm ++ showArg i+          my_show d Erased = "Erased"+          my_show d Impossible = "Impossible"+          my_show d (TType u) = showCon d "TType" $ showArg u  instance Eq TT where   a == b = equalp a b@@ -226,6 +242,12 @@           equalp (TType u)    (TType u')       = u == u'           equalp x            y                = False +instance Eq Universe where+  Reflection.NullType   == Reflection.NullType   = True+  Reflection.UniqueType == Reflection.UniqueType = True+  Reflection.AllTypes   == Reflection.AllTypes   = True+  _                     == _                     = False+ total forget : TT -> Maybe Raw forget tm = fe [] tm@@ -251,53 +273,54 @@     fe env Impossible    = Nothing  instance Show Raw where-  show r = my_show r-    where %assert_total my_show : Raw -> String-          my_show (Var n) = "(Var " ++ show n ++ ")"-          my_show (RBind n b tm) = "(RBind " ++ show n ++ " " ++ show b ++ " " ++ my_show tm ++ ")"-          my_show (RApp tm tm') = "(RApp " ++ my_show tm ++ " " ++ my_show tm' ++ ")"-          my_show RType = "RType"-          my_show (RForce tm) = "(RForce " ++ my_show tm ++ ")"-          my_show (RConstant c) = "(RConstant " ++ show c ++ ")"+  showPrec = my_show+    where %assert_total my_show : Prec -> Raw -> String+          my_show d (Var n) = showCon d "Var" $ showArg n+          my_show d (RBind n b tm) = showCon d "RBind" $ showArg n ++ showArg b ++ " " ++ my_show App tm+          my_show d (RApp tm tm') = showCon d "RApp" $ " " ++ my_show App tm ++ " " ++ my_show App tm'+          my_show d RType = "RType"+          my_show d (RForce tm) = showCon d "RForce" $ " " ++ my_show App tm+          my_show d (RConstant c) = showCon d "RConstant" $ showArg c  instance Show SourceLocation where-  show (FileLoc filename line col) = "FileLoc \"" ++ filename ++ "\" " ++ show line ++ " " ++ show col+  showPrec d (FileLoc filename line col) = showCon d "FileLoc" $ showArg filename ++ showArg line ++ showArg col  instance Show Err where-  show (Msg x) = "Msg \"" ++ x ++ "\""-  show (InternalMsg x) = "InternalMsg \"" ++ x ++ "\""-  show (CantUnify x tm tm' err xs y) = "CantUnify " ++ show x ++-                                       " ( " ++ show tm ++ ") (" ++ show tm' ++ ") (" ++ show err ++ ") " ++-                                       show xs ++ " " ++ show y-  show (InfiniteUnify n tm xs) = "InfiniteUnify " ++ show n ++ show tm ++ show xs-  show (CantConvert tm tm' xs) = "CantConvert " ++ show tm ++ show tm' ++ show xs-  show (CantSolveGoal tm ctxt) = "CantSolveGoal " ++ show tm ++ " " ++ show ctxt-  show (UnifyScope n n' tm xs) = "UnifyScope " ++ show n ++ " " ++ show n' ++ " " ++ show tm ++ " " ++ show xs-  show (CantInferType x) = "CantInferType " ++ show x-  show (NonFunctionType tm tm') = "NonFunctionType " ++ show tm ++ show tm'-  show (NotEquality tm tm') = "NotEquality " ++ show tm ++ " " ++ show tm'-  show (TooManyArguments n) = "TooManyArguments " ++ show n-  show (CantIntroduce tm) = "CantIntroduce " ++ show tm-  show (NoSuchVariable n) = "NoSuchVariable " ++ show n-  show (WithFnType tm) = "WithFnType " ++ show tm-  show (CantMatch tm) = "CantMatch " ++ show tm-  show (NoTypeDecl n) = "NoTypeDecl " ++ show n-  show (NotInjective tm tm' x) = "NotInjective " ++ show tm ++ " " ++ show tm'-  show (CantResolve tm) = "CantResolve " ++ show tm-  show (InvalidTCArg n tm) = "InvalidTCName " ++ show n ++ " (" ++ show tm ++ ")"-  show (CantResolveAlts xs) = "CantResolveAlts " ++ show xs-  show (IncompleteTerm tm) = "IncompleteTerm " ++ show tm-  show (NoEliminator s tm) = "NoEliminator " ++ show s ++ " " ++ show tm-  show UniverseError = "UniverseError"-  show ProgramLineComment = "ProgramLineComment"-  show (Inaccessible n) = "Inaccessible " ++ show n-  show (UnknownImplicit n f) = "UnknownImplicit " ++ show n ++ " "  ++ show f-  show (NonCollapsiblePostulate n) = "NonCollapsiblePostulate " ++ show n-  show (AlreadyDefined n) = "AlreadyDefined " ++ show n-  show (ProofSearchFail err) = "ProofSearchFail " ++ show err-  show (NoRewriting tm) = "NoRewriting " ++ show tm-  show (ProviderError x) = "ProviderError \"" ++ show x ++ "\""-  show (LoadingFailed x err) = "LoadingFailed " ++ show x ++ " (" ++ show err ++ ")"+  showPrec d (Msg x) = showCon d "Msg" $ showArg x+  showPrec d (InternalMsg x) = showCon d "InternalMsg" $ showArg x+  showPrec d (CantUnify x tm tm' err xs y) = showCon d "CantUnify" $ showArg x +++                                       showArg tm ++ showArg tm' ++ showArg err +++                                       showArg xs ++ showArg y+  showPrec d (InfiniteUnify n tm xs) = showCon d "InfiniteUnify" $ showArg n ++ showArg tm ++ showArg xs+  showPrec d (CantConvert tm tm' xs) = showCon d "CantConvert" $ showArg tm ++ showArg tm' ++ showArg xs+  showPrec d (CantSolveGoal tm ctxt) = showCon d "CantSolveGoal" $ showArg tm ++ showArg ctxt+  showPrec d (UnifyScope n n' tm xs) = showCon d "UnifyScope" $ showArg n ++ showArg n' ++ showArg tm ++ showArg xs+  showPrec d (CantInferType x) = showCon d "CantInferType" $ showArg x+  showPrec d (NonFunctionType tm tm') = showCon d "NonFunctionType" $ showArg tm ++ showArg tm'+  showPrec d (NotEquality tm tm') = showCon d "NotEquality" $ showArg tm ++ showArg tm'+  showPrec d (TooManyArguments n) = showCon d "TooManyArguments" $ showArg n+  showPrec d (CantIntroduce tm) = showCon d "CantIntroduce" $ showArg tm+  showPrec d (NoSuchVariable n) = showCon d "NoSuchVariable" $ showArg n+  showPrec d (WithFnType tm) = showCon d "WithFnType" $ showArg tm+  showPrec d (CantMatch tm) = showCon d "CantMatch" $ showArg tm+  showPrec d (NoTypeDecl n) = showCon d "NoTypeDecl" $ showArg n+  showPrec d (NotInjective tm tm' x) = showCon d "NotInjective" $ showArg tm ++ showArg tm'+  showPrec d (CantResolve tm) = showCon d "CantResolve" $ showArg tm+  showPrec d (InvalidTCArg n tm) = showCon d "InvalidTCName" $ showArg n ++ showArg tm+  showPrec d (CantResolveAlts xs) = showCon d "CantResolveAlts" $ showArg xs+  showPrec d (NoValidAlts xs) = showCon d "NoValidAlts" $ showArg xs+  showPrec d (IncompleteTerm tm) = showCon d "IncompleteTerm" $ showArg tm+  showPrec d (NoEliminator s tm) = showCon d "NoEliminator" $ showArg s ++ showArg tm+  showPrec d UniverseError = "UniverseError"+  showPrec d ProgramLineComment = "ProgramLineComment"+  showPrec d (Inaccessible n) = showCon d "Inaccessible" $ showArg n+  showPrec d (UnknownImplicit n f) = showCon d "UnknownImplicit" $ showArg n ++ showArg f+  showPrec d (NonCollapsiblePostulate n) = showCon d "NonCollapsiblePostulate" $ showArg n+  showPrec d (AlreadyDefined n) = showCon d "AlreadyDefined" $ showArg n+  showPrec d (ProofSearchFail err) = showCon d "ProofSearchFail" $ showArg err+  showPrec d (NoRewriting tm) = showCon d "NoRewriting" $ showArg tm+  showPrec d (ProviderError x) = showCon d "ProviderError" $ showArg x+  showPrec d (LoadingFailed x err) = showCon d "LoadingFailed" $ showArg x ++ showArg err  ------------------------- -- Idiom brackets for Raw@@ -312,11 +335,23 @@ -------------------------------------- -- Instances for definition reflection ---------------------------------------instance Show Arg where-  show (Explicit n t) = "(Explicit " ++ show n ++ " " ++ show t ++ ")"-  show (Implicit n t) = "(Implicit " ++ show n ++ " " ++ show t ++ ")"-  show (Constraint n t) = "(Constraint " ++ show n ++ " " ++ show t ++ ")"+instance Show Erasure where+  show Erased    = "Erased"+  show NotErased = "NotErased" +instance Show Plicity where+  show Explicit = "Explicit"+  show Implicit = "Implicit"+  show Constraint = "Constraint"++instance Show FunArg where+  showPrec d (MkFunArg n ty plic era) = showCon d "MkFunArg" $ showArg n +++                                        showArg ty ++ showArg plic ++ showArg era++instance Show CtorArg where+  showPrec d (CtorParameter fa) = showCon d "CtorParameter" $ showArg fa+  showPrec d (CtorField fa) = showCon d "CtorField" $ showArg fa+ instance Show TyDecl where-  show (Declare fn args ret) = "(Declare " ++ show fn ++ " " ++-                               show args ++ " " ++ show ret ++ ")"+  showPrec d (Declare fn args ret) = showCon d "Declare" $ showArg fn +++                                     showArg args ++ showArg ret

@@ -4,23 +4,7 @@ %default partial %access public -||| Get the command-line arguments that the program was called with.-getArgs : IO (List String)-getArgs = do n <- numArgs-             ga' [] 0 n-  where-    numArgs : IO Int-    numArgs = foreign FFI_C "idris_numArgs" (IO Int)--    getArg : Int -> IO String-    getArg x = foreign FFI_C "idris_getArg" (Int -> IO String) x--    ga' : List String -> Int -> Int -> IO (List String)-    ga' acc i n = if (i == n) then (return $ reverse acc) else-                    do arg <- getArg i-                       ga' (arg :: acc) (i+1) n--||| Retrieves an value from the environment, if the given key is present,+||| Retrieves a value from the environment if the given key is present, ||| otherwise it returns Nothing. getEnv : String -> IO (Maybe String) getEnv key = do@@ -73,8 +57,9 @@ exit code = foreign FFI_C "exit" (Int -> IO ()) code  ||| Get the Unix time-time : IO Int-time = foreign FFI_C "idris_time" (IO Int)+time : IO Integer+time = do MkRaw t <- foreign FFI_C "idris_time" (IO (Raw Integer))+          return t  usleep : Int -> IO () usleep i = foreign FFI_C "usleep" (Int -> IO ()) i

@@ -7,15 +7,25 @@ import System  ||| Send a message of any type to the thread with the given thread id-sendToThread : (thread_id : Ptr) -> a -> IO ()+||| Returns 1 if the message was sent successfully, 0 otherwise+sendToThread : (thread_id : Ptr) -> a -> IO Int sendToThread {a} dest val-   = foreign FFI_C "idris_sendMessage" (Ptr -> Ptr -> Raw a -> IO ())+   = foreign FFI_C "idris_sendMessage" (Ptr -> Ptr -> Raw a -> IO Int)                 prim__vm dest (MkRaw val)  ||| Check for messages in the process inbox checkMsgs : IO Bool checkMsgs = do msgs <- foreign FFI_C "idris_checkMessages" (Ptr -> IO Ptr)                             prim__vm+               null <- nullPtr msgs+               return (not null)++||| Check for messages in the process inbox+||| If no messages, waits for the given number of seconds+checkMsgsTimeout : Int -> IO Bool+checkMsgsTimeout timeout+          = do msgs <- foreign FFI_C "idris_checkMessagesTimeout" +                            (Ptr -> Int -> IO Ptr) prim__vm timeout                null <- nullPtr msgs                return (not null) 

@@ -5,7 +5,7 @@            Debug.Error, Debug.Trace, -          System.Info,+          System.Info,             Language.Reflection.Utils, 

@@ -54,7 +54,7 @@ |||     forall a,     inverse a <+> a == neutral ||| + Associativity of `<.>`: |||     forall a b c, a <.> (b <.> c) == (a <.> b) <.> c-||| + Distributivity of `<.>` and `<->`:+||| + Distributivity of `<.>` and `<+>`: |||     forall a b c, a <.> (b <+> c) == (a <.> b) <+> (a <.> c) |||     forall a b c, (a <+> b) <.> c == (a <.> c) <+> (b <.> c) class AbelianGroup a => Ring a where@@ -80,7 +80,7 @@ ||| + Neutral for `<.>`: |||     forall a,     a <.> unity     == a |||     forall a,     unity <.> a     == a-||| + Distributivity of `<.>` and `<->`:+||| + Distributivity of `<.>` and `<+>`: |||     forall a b c, a <.> (b <+> c) == (a <.> b) <+> (a <.> c) |||     forall a b c, (a <+> b) <.> c == (a <.> c) <+> (b <.> c) class Ring a => RingWithUnity a where@@ -109,21 +109,21 @@ ||| + InverseM of `<.>`, except for neutral |||     forall a /= neutral,  a <.> inverseM a == unity |||     forall a /= neutral,  inverseM a <.> a == unity-||| + Distributivity of `<.>` and `<->`:+||| + Distributivity of `<.>` and `<+>`: |||     forall a b c, a <.> (b <+> c) == (a <.> b) <+> (a <.> c) |||     forall a b c, (a <+> b) <.> c == (a <.> c) <+> (b <.> c) class RingWithUnity a => Field a where   inverseM : (x : a) -> Not (x = neutral) -> a -sum : (Foldable t, Monoid a) => t a -> a-sum = foldr (<+>) neutral+sum' : (Foldable t, Monoid a) => t a -> a+sum' = concat -product : (Foldable t, RingWithUnity a) => t a -> a-product = foldr (<.>) unity+product' : (Foldable t, RingWithUnity a) => t a -> a+product' = foldr (<.>) unity -power : RingWithUnity a => a -> Nat -> a-power _ Z     = unity-power x (S n) = x <.> (Algebra.power x n)+pow' : RingWithUnity a => a -> Nat -> a+pow' _ Z     = unity+pow' x (S n) = x <.> pow' x n   -- XXX todo:

@@ -1,6 +1,9 @@+||| Instances of algebraic classes (group, ring, etc) for numeric data types,+||| and Complex number types. module Control.Algebra.NumericInstances  import Control.Algebra+import Control.Algebra.VectorSpace import Data.Complex import Data.ZZ @@ -102,3 +105,9 @@  instance RingWithUnity a => RingWithUnity (Complex a) where   unity = (unity :+ neutral)++instance RingWithUnity a => Module a (Complex a) where+  (<#>) x = map (x <.>)++instance RingWithUnity a => InnerProductSpace a (Complex a) where+  (x :+ y) <||> z = realPart $ (x :+ inverse y) <.> z

@@ -1,6 +1,6 @@ module Data.Fun -import Data.Vect+import public Data.Vect  %default total 

@@ -114,8 +114,8 @@ --------------------------------------------------------------------------------  instance Show a => Show (MaxiphobicHeap a) where-  show Empty = "Empty"-  show (Node s l e r) = "Node (" ++ show l ++ " " ++ show e ++ " " ++ show r ++ ")"+  showPrec d Empty = "Empty"+  showPrec d (Node s l e r) = showCon d "Node" $ " _" ++ showArg l ++ showArg e ++ showArg r  instance Eq a => Eq (MaxiphobicHeap a) where   Empty              == Empty              = True

@@ -1,150 +1,58 @@+||| Basic matrix operations with dimensionalities enforced+||| at the type level module Data.Matrix -import        Control.Algebra-import        Control.Algebra.VectorSpace-import public Control.Algebra.NumericInstances--import Data.Complex-import Data.ZZ-import Data.Fin-import Data.Vect+import public Data.Vect  %default total -infixr 2 <:>  -- vector inner product-infixr 2 ><   -- vector outer product-infixr 2 <<>> -- matrix commutator-infixr 2 >><< -- matrix anticommutator-infixl 3 <\>  -- row times a matrix-infixr 4 </>  -- matrix times a column-infixr 5 <>   -- matrix multiplication-infixr 7 \&\  -- vector tensor product-infixr 7 <&>  -- matrix tensor product----------------------------------------------------------------------------               Vectors as members of algebraic classes--------------------------------------------------------------------------instance Semigroup a => Semigroup (Vect n a) where-  (<+>) v w = zipWith (<+>) v w--instance Monoid a => Monoid (Vect n a) where-  neutral {n} = replicate n neutral--instance Group a => Group (Vect n a) where-  inverse = map inverse--instance AbelianGroup a => AbelianGroup (Vect n a) where {}--instance Ring a => Ring (Vect n a) where-  (<.>) v w = zipWith (<.>) v w--instance RingWithUnity a => RingWithUnity (Vect n a) where-  unity {n} = replicate n unity----instance Field a => Field (Vect n a) where--instance RingWithUnity a => Module a (Vect n a) where-  (<#>) r v = map (r <.>) v--instance RingWithUnity a => Module a (Vect n (Vect l a)) where-  (<#>) r m = map (r <#>) m--- should be Module a b => Module a (Vect n b), but results in 'overlapping instance'----------------------------------------------------------------------------                       (Ring) Vector functions--------------------------------------------------------------------------||| Inner product of ring vectors-(<:>) : Ring a => Vect n a -> Vect n a -> a-(<:>) w v = foldr (<+>) neutral (zipWith (<.>) w v)--||| Tensor multiply (⊗) ring vectors-(\&\) : Ring a => Vect n a -> Vect m a -> Vect (n * m) a-(\&\) {n} {m} v w = zipWith (<.>) (oextend m v) (orep n w) where-  orep : (n : Nat) -> Vect m a -> Vect (n * m) a-  orep n v = concat $ replicate n v-  oextend : (n : Nat) -> Vect k a -> Vect (k * n) a-  oextend n w = concat $ map (replicate n) w--||| Standard basis vector with one nonzero entry, ring data type and vector-length unfixed-basis : RingWithUnity a => {d : Nat} -> (Fin d) -> Vect d a-basis i = replaceAt i unity $ neutral----------------------------------------------------------------------------                          Matrix functions------------------------------------------------------------------------- ||| Matrix with n rows and m columns Matrix : Nat -> Nat -> Type -> Type Matrix n m a = Vect n (Vect m a) -||| Gets the specified column of a matrix. For rows use the vector function 'index'+||| Get the specified column of a matrix getCol : Fin m -> Matrix n m a -> Vect n a-getCol fm q = map (index fm) q+getCol f = map (index f) -||| Deletes the specified column of a matrix. For rows use the vector function 'deleteAt'-deleteCol : Fin (S m) -> Matrix n (S m) a -> Matrix n m a-deleteCol f m = map (deleteAt f) m+||| Get the specified row of a matrix+getRow : Fin n -> Matrix n m a -> Vect m a+getRow = index -||| Matrix element at specified row and column indices-indices : Fin n -> Fin m -> Matrix n m a -> a-indices f1 f2 m = index f2 (index f1 m)+||| Delete the specified column of a matrix+deleteCol : Fin (S m) -> Matrix n (S m) a -> Matrix n m a+deleteCol f = map (deleteAt f) -||| Matrix times a column vector-(</>) : Ring a => Matrix n m a -> Vect m a -> Vect n a-(</>) m v = map (v <:>) m+||| Delete the specified row of a matrix+deleteRow : Fin (S n) -> Matrix (S n) m a -> Matrix n m a+deleteRow = deleteAt -||| Matrix times a row vector-(<\>) : Ring a => Vect n a -> Matrix n m a -> Vect m a-(<\>) r m = map (r <:>) $ transpose m+insertRow : Fin (S n) -> Vect m a -> Matrix n m a -> Matrix (S n) m a+insertRow = insertAt -||| Matrix multiplication-(<>) : Ring a => Matrix n k a ->-                 Matrix k m a ->-                 Matrix n m a-(<>) m1 m2 = map (<\> m2) m1+insertCol : Fin (S m) -> Vect n a -> Matrix n m a -> Matrix n (S m) a+insertCol f = zipWith (insertAt f) -||| Tensor multiply (⊗) for ring matrices-(<&>) : Ring a => Matrix h1 w1 a -> Matrix h2 w2 a -> Matrix (h1 * h2) (w1 * w2) a-(<&>) m1 m2 = zipWith (\&\) (stepOne m1 m2) (stepTwo m1 m2) where-  stepOne : Matrix h1 w1 a -> Matrix h2 w2 a -> Matrix (h1 * h2) w1 a-  stepOne {h2} m1 m2 = concat $ map (replicate h2) m1-  stepTwo : Matrix h1 w1 a -> Matrix h2 w2 a -> Matrix (h1 * h2) w2 a-  stepTwo {h1} m1 m2 = concat $ (Vect.replicate h1) m2+||| Matrix element at specified row and column indices+indices : Fin n -> Fin m -> Matrix n m a -> a+indices f1 f2 = index f2 . index f1  ||| Cast a vector from a standard Vect to a proper n x 1 matrix col : Vect n a -> Matrix n 1 a-col v = map (\x => [x]) v+col = map (\x => [x])  ||| Cast a row from a standard Vect to a proper 1 x n matrix row : Vect n a -> Matrix 1 n a row r = [r] -||| Outer product between ring vectors-(><) : Ring a => Vect n a -> Vect m a -> Matrix n m a-(><) x y = (col x) <> (row y)--||| All finite numbers up to the given bound-allN : (n : Nat) -> Vect n (Fin n)-allN Z     = Nil-allN (S n) = FZ :: (map FS $ allN n)--||| Identity matrix-Id : RingWithUnity a => {d : Nat} -> Matrix d d a-Id {d} = map (\n => basis n) $ allN d--||| Matrix commutator-(<<>>) : Ring a => Matrix n n a -> Matrix n n a -> Matrix n n a-(<<>>) m1 m2 = (m1 <> m2) <-> (m2 <> m1)--||| Matrix anti-commutator-(>><<) : Ring a => Matrix n n a -> Matrix n n a -> Matrix n n a-(>><<) m1 m2 = (m1 <> m2) <+> (m2 <> m1)----------------------------------------------------------------------------                      Matrix Algebra Properties------------------------------------------------------------------------+||| Matrix formed by deleting specified row and col+subMatrix : Fin (S n) -> Fin (S m) -> Matrix (S n) (S m) a -> Matrix n m a+subMatrix r c = deleteRow r . deleteCol c --- TODO: Prove properties of matrix algebra for 'Verified' algebraic classes+||| Flatten a matrix of matrices+concatMatrix : Matrix n m (Matrix x y a) -> Matrix (n * x) (m * y) a+concatMatrix = Vect.concat . map (map Vect.concat) . map transpose +||| All finite numbers of the specified level+fins : (n : Nat) -> Vect n (Fin n)+fins Z     = Nil+fins (S n) = FZ :: (map FS $ fins n)

@@ -0,0 +1,149 @@+||| Matrix operations with vector space dimensionalities enforced+||| at the type level. Uses operations from classes in `Control.Algebra`+||| and `Control.Algebra.VectorSpace`.+module Data.Matrix.Algebraic++import public Control.Algebra+import public Control.Algebra.VectorSpace+import public Control.Algebra.NumericInstances++import public Data.Matrix+++%default total++infixr 2 <:>  -- vector inner product+infixr 2 ><   -- vector outer product+infixr 2 <<>> -- matrix commutator+infixr 2 >><< -- matrix anticommutator+infixl 3 <\>  -- row times a matrix+infixr 4 </>  -- matrix times a column+infixr 5 <>   -- matrix multiplication+infixr 7 \&\  -- vector tensor product+infixr 7 <&>  -- matrix tensor product++-----------------------------------------------------------------------+--               Vectors as members of algebraic classes+-----------------------------------------------------------------------++instance Semigroup a => Semigroup (Vect n a) where+  (<+>)= zipWith (<+>)++instance Monoid a => Monoid (Vect n a) where+  neutral {n} = replicate n neutral++instance Group a => Group (Vect n a) where+  inverse = map inverse++instance AbelianGroup a => AbelianGroup (Vect n a) where {}++instance Ring a => Ring (Vect n a) where+  (<.>) = zipWith (<.>)++instance RingWithUnity a => RingWithUnity (Vect n a) where+  unity {n} = replicate n unity++instance RingWithUnity a => Module a (Vect n a) where+  (<#>) r = map (r <.>)++instance RingWithUnity a => Module a (Vect n (Vect l a)) where+  (<#>) r = map (r <#>)+-- should be Module a b => Module a (Vect n b), but results in 'overlapping instance'++-----------------------------------------------------------------------+--                        (Ring) Vector functions+-----------------------------------------------------------------------++||| Inner product of ring vectors+(<:>) : Ring a => Vect n a -> Vect n a -> a+(<:>) w v = foldr (<+>) neutral (zipWith (<.>) w v)++||| Tensor multiply (⊗) ring vectors+(\&\) : Ring a => Vect n a -> Vect m a -> Vect (n * m) a+(\&\) {n} {m} v w = zipWith (<.>) (oextend m v) (orep n w) where+  orep : (n : Nat) -> Vect m a -> Vect (n * m) a+  orep n v = concat $ replicate n v+  oextend : (n : Nat) -> Vect k a -> Vect (k * n) a+  oextend n w = concat $ map (replicate n) w++||| Standard basis vector with one nonzero entry, ring data type and vector-length unfixed+basis : RingWithUnity a => (Fin d) -> Vect d a+basis i = replaceAt i unity neutral++-----------------------------------------------------------------------+--                         Ring Matrix functions+-----------------------------------------------------------------------++||| Matrix times a column vector+(</>) : Ring a => Matrix n m a -> Vect m a -> Vect n a+(</>) m v = map (v <:>) m++||| Matrix times a row vector+(<\>) : Ring a => Vect n a -> Matrix n m a -> Vect m a+(<\>) r m = map (r <:>) $ transpose m++||| Matrix multiplication+(<>) : Ring a => Matrix n k a ->+                 Matrix k m a ->+                 Matrix n m a+(<>) m1 m2 = map (<\> m2) m1++||| Tensor multiply (⊗) for ring matrices+(<&>) : Ring a => Matrix h1 w1 a -> Matrix h2 w2 a -> Matrix (h1 * h2) (w1 * w2) a+(<&>) m1 m2 = zipWith (\&\) (stepOne m1 m2) (stepTwo m1 m2) where+  stepOne : Matrix h1 w1 a -> Matrix h2 w2 a -> Matrix (h1 * h2) w1 a+  stepOne {h2} m1 m2 = concat $ map (replicate h2) m1+  stepTwo : Matrix h1 w1 a -> Matrix h2 w2 a -> Matrix (h1 * h2) w2 a+  stepTwo {h1} m1 m2 = concat $ replicate h1 m2++||| Outer product between ring vectors+(><) : Ring a => Vect n a -> Vect m a -> Matrix n m a+(><) x y = col x <> row y++||| Matrix commutator+(<<>>) : Ring a => Matrix n n a -> Matrix n n a -> Matrix n n a+(<<>>) m1 m2 = (m1 <> m2) <-> (m2 <> m1)++||| Matrix anti-commutator+(>><<) : Ring a => Matrix n n a -> Matrix n n a -> Matrix n n a+(>><<) m1 m2 = (m1 <> m2) <+> (m2 <> m1)++||| Identity matrix+Id : RingWithUnity a => Matrix d d a+Id = map (\n => basis n) (fins _)++||| Square matrix from diagonal elements+diag_ : Monoid a => Vect n a -> Matrix n n a+diag_ = zipWith (\f => \x => replaceAt f x neutral) (fins _)++||| Combine two matrices to make a new matrix in block diagonal form+blockDiag : Monoid a => Matrix n n a -> Matrix m m a -> Matrix (n+m) (n+m) a+blockDiag g h = map (++ replicate _ neutral) g ++ map ((replicate _ neutral) ++) h+++-----------------------------------------------------------------------+--                           Determinants+-----------------------------------------------------------------------++||| Alternating sum+altSum : Group a => Vect n a -> a+altSum (x::y::zs) = (x <-> y) <+> altSum zs+altSum [x]        = x+altSum []         = neutral++||| Determinant of a 2-by-2 matrix+det2 : Ring a => Matrix 2 2 a -> a+det2 [[x1,x2],[y1,y2]] = x1 <.> y2 <-> x2 <.> y1++||| Determinant of a square matrix+det : Ring a => Matrix (S (S n)) (S (S n)) a -> a+det {n} m = case n of+  Z     => det2 m+  (S k) => altSum . map (\c => indices FZ c m <.> det (subMatrix FZ c m))+         $ fins (S (S (S k)))++-----------------------------------------------------------------------+--                      Matrix Algebra Properties+-----------------------------------------------------------------------++-- TODO: Prove properties of matrix algebra for 'Verified' algebraic classes

@@ -0,0 +1,129 @@+||| Matrix operations with vector space dimensionalities enforced+||| at the type level. Uses operations from the Num type class.+module Data.Matrix.Numeric++import public Data.Matrix++%default total++infixr 2 <:>  -- vector inner product+infixr 2 ><   -- vector outer product+infixr 2 <<>> -- matrix commutator+infixr 2 >><< -- matrix anticommutator+infixl 3 <\>  -- row times a matrix+infixr 4 </>  -- matrix times a column+infixr 5 <>   -- matrix multiplication+infixl 5 <#>  -- matrix rescale+infixl 5 <#   -- vector rescale+infixr 7 \&\  -- vector tensor product+infixr 7 <&>  -- matrix tensor product++-----------------------------------------------------------------------+--                   Vectors as members of Num+-----------------------------------------------------------------------++instance Num a => Num (Vect n a) where+  (+) = zipWith (+)+  (-) = zipWith (+)+  (*) = zipWith (*)+  abs = id+  fromInteger n = replicate _ (fromInteger n)++-----------------------------------------------------------------------+--                        Vector functions+-----------------------------------------------------------------------++||| Inner product of ring vectors+(<:>) : Num a => Vect n a -> Vect n a -> a+(<:>) w v = sum $ zipWith (*) w v++||| Scale a numeric vector by a scalar+(<#) : Num a => a -> Vect n a -> Vect n a+(<#) r = map (r *)++||| Tensor multiply (⊗) numeric vectors+(\&\) : Num a => Vect n a -> Vect m a -> Vect (n * m) a+(\&\) {n} {m} v w = zipWith (*) (oextend m v) (orep n w) where+  orep : (n : Nat) -> Vect m a -> Vect (n * m) a+  orep n v = concat $ replicate n v+  oextend : (n : Nat) -> Vect k a -> Vect (k * n) a+  oextend n w = concat $ map (replicate n) w++||| Standard basis vector with one nonzero entry, numeric data type and vector-length unfixed+basis : Num a => (Fin d) -> Vect d a+basis i = replaceAt i 1 0++-----------------------------------------------------------------------+--                          Matrix functions+-----------------------------------------------------------------------++||| Matrix times a column vector+(</>) : Num a => Matrix n m a -> Vect m a -> Vect n a+(</>) m v = map (v <:>) m++||| Matrix times a row vector+(<\>) : Num a => Vect n a -> Matrix n m a -> Vect m a+(<\>) r m = map (r <:>) $ transpose m++||| Matrix multiplication+(<>) : Num a => Matrix n k a ->+                Matrix k m a ->+                Matrix n m a+(<>) m1 m2 = map (<\> m2) m1++||| Scale matrix by a scalar+(<#>) : Num a => a -> Matrix n m a -> Matrix n m a+(<#>) r = map (r <#)++||| Tensor multiply (⊗) for numeric matrices+(<&>) : Num a => Matrix h1 w1 a -> Matrix h2 w2 a -> Matrix (h1 * h2) (w1 * w2) a+(<&>) m1 m2 = zipWith (\&\) (stepOne m1 m2) (stepTwo m1 m2) where+  stepOne : Matrix h1 w1 a -> Matrix h2 w2 a -> Matrix (h1 * h2) w1 a+  stepOne {h2} m1 m2 = concat $ map (replicate h2) m1+  stepTwo : Matrix h1 w1 a -> Matrix h2 w2 a -> Matrix (h1 * h2) w2 a+  stepTwo {h1} m1 m2 = concat $ replicate h1 m2++||| Outer product between numeric vectors+(><) : Num a => Vect n a -> Vect m a -> Matrix n m a+(><) x y = col x <> row y++||| Matrix commutator+(<<>>) : Num a => Matrix n n a -> Matrix n n a -> Matrix n n a+(<<>>) m1 m2 = (m1 <> m2) - (m2 <> m1)++||| Matrix anti-commutator+(>><<) : Num a => Matrix n n a -> Matrix n n a -> Matrix n n a+(>><<) m1 m2 = (m1 <> m2) + (m2 <> m1)++||| Identity matrix+Id : Num a => Matrix d d a+Id = map (\n => basis n) (fins _)++||| Square matrix from diagonal elements+diag_ : Num a => Vect n a -> Matrix n n a+diag_ = zipWith (\f => \x => replaceAt f x 0) (fins _)++||| Combine two matrices to make a new matrix in block diagonal form+blockDiag : Num a => Matrix n n a -> Matrix m m a -> Matrix (n+m) (n+m) a+blockDiag {n} {m} g h = map (++ replicate m 0) g ++ map ((replicate n 0) ++) h++-----------------------------------------------------------------------+--                           Determinants+-----------------------------------------------------------------------++||| Alternating sum+altSum : Num a => Vect n a -> a+altSum (x::y::zs) = (x - y) + altSum zs+altSum [x]        = x+altSum []         = 0++||| Determinant of a 2-by-2 matrix+det2 : Num a => Matrix 2 2 a -> a+det2 [[x1,x2],[y1,y2]] = x1*y2 - x2*y1++||| Determinant of a square matrix+det : Num a => Matrix (S (S n)) (S (S n)) a -> a+det {n} m = case n of+  Z     => det2 m+  (S k) => altSum . map (\c => indices FZ c m * det (subMatrix FZ c m))+         $ fins (S (S (S k)))

@@ -1,166 +0,0 @@-||| Extra utilities for working with Nats-module Data.Nat--import Data.Fin-import Data.So--import Control.WellFounded--%default total-%access public--||| A strict less-than relation on `Nat`.-|||-||| @ n the smaller number-||| @ m the larger number-data LT' : (n,m : Nat) -> Type where-  ||| n < 1 + n-  LTSucc : LT' n (S n)-  ||| n < m implies that n < m + 1-  LTStep : LT' n m -> LT' n (S m)--%name LT' lt, lt'--||| Nothing is strictly less than zero-instance Uninhabited (LT' n 0) where-  uninhabited LTSucc impossible--||| Zero is less than any non-zero number.-LTZeroLeast : LT' Z (S n)-LTZeroLeast {n = Z}   = LTSucc-LTZeroLeast {n = S n} = LTStep LTZeroLeast--||| If n < m, then 1 + n < 1 + m-ltSuccSucc : LT' n m -> LT' (S n) (S m)-ltSuccSucc LTSucc      = LTSucc-ltSuccSucc (LTStep lt) = LTStep $ ltSuccSucc lt--||| If n + 1 < m, then n < m-lteToLt' : LTE (S n) m -> LT' n m-lteToLt' {n = Z}   (LTESucc x) = LTZeroLeast-lteToLt' {n = S k} (LTESucc x) = ltSuccSucc $ lteToLt' x--||| Convert from LT' to LTE-ltToLTE : LT' n m -> LTE (S n) m-ltToLTE LTSucc      = lteRefl-ltToLTE (LTStep lt) = lteSuccRight $ ltToLTE lt--||| Subtraction gives a result that is actually smaller.-minusLT' : (x,y : Nat) -> x - y `LT'` S x-minusLT' Z     y = LTSucc-minusLT' (S k) Z = LTSucc-minusLT' (S k) (S j) = LTStep (minusLT' k j)--||| Strict less-than is well-founded, with the cascade stopping at-||| zero (because there's nothing less than zero). This can't be done-||| for LTE, because that one doesn't stop at zero (because `LTE 0 0`-||| is inhabited).-instance WellFounded LT' where-  wellFounded x = Access (acc x)-    where-      ||| Show accessibility by induction on the structure of the LT' witness-      acc : (x, y : Nat) -> LT' y x -> Accessible LT' y-      -- Zero is vacuously accessible: there's nothing smaller to check-      acc Z     y lt = absurd lt-      -- If the element being accessed is one smaller, we're done-      acc (S y) y LTSucc = Access (acc y)-      -- If the element is more than one smaller, we need to go further-      acc (S k) y (LTStep smaller) = acc k y smaller--||| The result of division on natural numbers.-|||-||| @ dividend the dividend-||| @ divisor the divisor-data DivMod : (dividend, divisor : Nat) -> Type where-  ||| The result of division, with a quotient and a remainder.-  |||-  ||| @ dividend the dividend-  ||| @ divisor the divisor-  ||| @ quotient the quotient-  ||| @ remainder the remainder (bounded by the divisor)-  ||| @ ok the fact that this is, in fact, a result of division-  DivModRes : {dividend, divisor : Nat} ->-              (quotient : Nat) -> (remainder : Fin divisor) ->-              (ok : dividend = finToNat remainder + quotient * divisor) ->-              DivMod dividend divisor---||| Any natural number can be a `Fin` where the bound is itself plus some difference.-private-toFin : (x : Nat) -> (diff : Nat) -> Fin (plus x (S diff))-toFin Z diff = FZ-toFin (S k) diff = FS $ toFin k diff--||| Converting to a `Fin` and back to `Nat` preserves the input. This is a correctness proof for `toFin`.-private-toFinAndBack : (x : Nat) -> (diff : Nat) -> finToNat (toFin x diff) = x-toFinAndBack Z diff = Refl-toFinAndBack (S k) diff = cong (toFinAndBack k diff)---||| The accessibilty predicate used for division.-private-accPlusLT' : LT' (S j) (S (plus k (S j)))-accPlusLT' {j = Z}   {k = Z}   = LTSucc-accPlusLT' {j = Z}   {k = S k} = LTStep (accPlusLT' {j = Z} {k = k})-accPlusLT' {j = S j} {k = k}   = rewrite sym $ plusSuccRightSucc k (S j) in-                                 ltSuccSucc accPlusLT'---||| Division and modulus on `Nat`, inspired by the definition in the-||| Agda standard library.-|||-||| This uses well-founded recursion on `LT'`.-|||-||| @ dividend the dividend-||| @ divisor the divisor-||| @ nonzero division by zero is nonsense-total -- yay!-divMod : (dividend, divisor : Nat) ->-         {auto nonzero : So (not (decAsBool (decEq divisor Z)))} ->-         DivMod dividend divisor-divMod _     Z     {nonzero} = absurd nonzero-divMod Z     (S k)           = DivModRes 0 FZ Refl-divMod (S j) (S k) {nonzero} = wfInd {P=P} stepDiv (S j) (S k) nonzero-  where-    ||| The goal passed to the accessibility eliminator.-    |||-    ||| This is responsible for generating the goal in the-    ||| well-founded fixed point.-    |||-    ||| @ dividend the dividend to recurse over-    P : (dividend : Nat) -> Type-    P dividend = (divisor : Nat) -> (nonzero : So (not (decAsBool (decEq divisor Z)))) -> DivMod dividend divisor---    ||| Well-founded recursion needs a recursion operator.-    |||-    ||| @ dividend the dividend we are recursing over-    ||| @ rec the recursive call provided by the well-founded induction operator-    stepDiv : (dividend : Nat) -> (rec : (d' : Nat) -> LT' d' dividend -> P d') -> P dividend-    -- We need not consider division by zero-    stepDiv dividend rec   Z     nonzero = absurd nonzero-    -- Dividing zero by anyting else gives 0, with 0 remainder-    stepDiv Z rec (S k) nonzero = DivModRes 0 0 Refl-    -- To divide two non-zero values, we must know which is larger-    stepDiv (S j) rec (S k) nonzero with (cmp j k)-      -- n / n = 1 remainder 0-      stepDiv (S j)                 rec (S j)                 nonzero | CmpEQ      =-        DivModRes 1 0 (sym $ cong (plusZeroRightNeutral j))-      -- if n < m, then m = n + r, and the quotient is 0 with remainder r-      stepDiv (S j)                 rec (S (plus j (S diff))) nonzero | CmpLT diff =-        DivModRes 0 (toFin (S j) diff) $-          rewrite toFinAndBack j diff-          in sym $ cong (plusZeroRightNeutral j)-      -- if n > m, then n = m + d, and the quotient is 1 + ((n - m) / m) with the same remainder-      stepDiv (S (plus k (S diff))) rec (S k)                 nonzero | CmpGT diff =-        let res = rec (S diff) accPlusLT' (S k) Oh-        in case res of-             DivModRes quotient remainder ok =>-               DivModRes (S quotient) remainder $-                 rewrite plusAssociative (finToNat remainder) (S k) (mult quotient (S k)) in-                 rewrite plusCommutative (finToNat remainder) (S k) in-                 rewrite sym $ plusAssociative (S k) (finToNat remainder) (mult quotient (S k)) in-                 rewrite ok in Refl--

@@ -0,0 +1,60 @@+||| Euclidean division using primitive recursion/induction.+module Data.Nat.DivMod++%default total++||| The result of euclidean division of natural numbers+|||+||| @ dividend the dividend+||| @ divisor the divisor+data DivMod : (dividend, divisor : Nat) -> Type where+  ||| The result of division. The order of operations and operands in the+  ||| result type was picked to not require any explicit proofs.+  |||+  ||| @ quotient the quotient+  ||| @ remainder the remainder+  ||| @ divisor the divisor+  ||| @ remainderSmall proof that the remainder is in the range+  ||| `[0 .. divisor - 1]`+  MkDivMod : (quotient, remainder : Nat) ->+             (remainderSmall : remainder `LT` divisor) ->+             DivMod (remainder + quotient * divisor) divisor++||| The base case, dividing zero by a successor.+|||+||| @ n the predecessor of the divisor+ZDivModSn : Z `DivMod` S n+ZDivModSn = MkDivMod 0 0 (LTESucc LTEZero)++||| Given a number less than or equal to a bound, is it equal, or less?+|||+||| @ m the lesser or equal number+||| @ n the greater or equal number+||| @ mLten proof that `m` is less than or equal to `n`+stepLT : (mLten : m `LTE` n) -> Either (m = n) (m `LT` n)+stepLT {m = Z} {n = Z} LTEZero = Left Refl+stepLT {m = Z} {n = (S n)} LTEZero = Right (LTESucc LTEZero)+stepLT {m = (S m)} {n = (S n)} (LTESucc mLten) with (stepLT mLten)+  stepLT {m = (S m)} {n = (S n)} (LTESucc mLten) | (Left mEqn) = Left $ cong mEqn+  stepLT {m = (S m)} {n = (S n)} (LTESucc mLten) | (Right mLtn) = Right $ LTESucc mLtn++||| The inductive step, taking a division of `m` to a division of `S m`+|||+||| @ m the dividend in the inductive hypothesis+||| @ n the divisor+||| @ hyp the inductive hypothesis+SmDivModn : (hyp : m `DivMod` n) -> (S m) `DivMod` n+SmDivModn (MkDivMod q r rLtn) with (stepLT rLtn)+  SmDivModn (MkDivMod q r rLtn) | (Left Refl) = MkDivMod (S q) 0 (LTESucc LTEZero)+  SmDivModn (MkDivMod q r rLtn) | (Right srLtn) = MkDivMod q (S r) srLtn++||| Euclidean division. Note that this takes the predecessor of the divisor to+||| avoid division by zero.+|||+||| @ dividend the dividend+||| @ predDivisor the predecessor of the desired divisor+divMod : (dividend, predDivisor : Nat) -> dividend `DivMod` S predDivisor+divMod Z n = ZDivModSn+divMod (S m) n = SmDivModn (m `divMod` n)++

@@ -0,0 +1,167 @@+||| Division of natural numbers, by iterated subtraction using well-founded+||| recursion+module Data.Nat.DivMod.IteratedSubtraction++import Data.Fin+import Data.So++import Control.WellFounded++%default total+%access public++||| A strict less-than relation on `Nat`.+|||+||| @ n the smaller number+||| @ m the larger number+data LT' : (n,m : Nat) -> Type where+  ||| n < 1 + n+  LTSucc : LT' n (S n)+  ||| n < m implies that n < m + 1+  LTStep : LT' n m -> LT' n (S m)++%name LT' lt, lt'++||| Nothing is strictly less than zero+instance Uninhabited (LT' n 0) where+  uninhabited LTSucc impossible++||| Zero is less than any non-zero number.+LTZeroLeast : LT' Z (S n)+LTZeroLeast {n = Z}   = LTSucc+LTZeroLeast {n = S n} = LTStep LTZeroLeast++||| If n < m, then 1 + n < 1 + m+ltSuccSucc : LT' n m -> LT' (S n) (S m)+ltSuccSucc LTSucc      = LTSucc+ltSuccSucc (LTStep lt) = LTStep $ ltSuccSucc lt++||| If n + 1 < m, then n < m+lteToLt' : LTE (S n) m -> LT' n m+lteToLt' {n = Z}   (LTESucc x) = LTZeroLeast+lteToLt' {n = S k} (LTESucc x) = ltSuccSucc $ lteToLt' x++||| Convert from LT' to LTE+ltToLTE : LT' n m -> LTE (S n) m+ltToLTE LTSucc      = lteRefl+ltToLTE (LTStep lt) = lteSuccRight $ ltToLTE lt++||| Subtraction gives a result that is actually smaller.+minusLT' : (x,y : Nat) -> x - y `LT'` S x+minusLT' Z     y = LTSucc+minusLT' (S k) Z = LTSucc+minusLT' (S k) (S j) = LTStep (minusLT' k j)++||| Strict less-than is well-founded, with the cascade stopping at+||| zero (because there's nothing less than zero). This can't be done+||| for LTE, because that one doesn't stop at zero (because `LTE 0 0`+||| is inhabited).+instance WellFounded LT' where+  wellFounded x = Access (acc x)+    where+      ||| Show accessibility by induction on the structure of the LT' witness+      acc : (x, y : Nat) -> LT' y x -> Accessible LT' y+      -- Zero is vacuously accessible: there's nothing smaller to check+      acc Z     y lt = absurd lt+      -- If the element being accessed is one smaller, we're done+      acc (S y) y LTSucc = Access (acc y)+      -- If the element is more than one smaller, we need to go further+      acc (S k) y (LTStep smaller) = acc k y smaller++||| The result of division on natural numbers.+|||+||| @ dividend the dividend+||| @ divisor the divisor+data DivMod : (dividend, divisor : Nat) -> Type where+  ||| The result of division, with a quotient and a remainder.+  |||+  ||| @ dividend the dividend+  ||| @ divisor the divisor+  ||| @ quotient the quotient+  ||| @ remainder the remainder (bounded by the divisor)+  ||| @ ok the fact that this is, in fact, a result of division+  DivModRes : {dividend, divisor : Nat} ->+              (quotient : Nat) -> (remainder : Fin divisor) ->+              (ok : dividend = finToNat remainder + quotient * divisor) ->+              DivMod dividend divisor+++||| Any natural number can be a `Fin` where the bound is itself plus some difference.+private+toFin : (x : Nat) -> (diff : Nat) -> Fin (plus x (S diff))+toFin Z diff = FZ+toFin (S k) diff = FS $ toFin k diff++||| Converting to a `Fin` and back to `Nat` preserves the input. This is a correctness proof for `toFin`.+private+toFinAndBack : (x : Nat) -> (diff : Nat) -> finToNat (toFin x diff) = x+toFinAndBack Z diff = Refl+toFinAndBack (S k) diff = cong (toFinAndBack k diff)+++||| The accessibilty predicate used for division.+private+accPlusLT' : LT' (S j) (S (plus k (S j)))+accPlusLT' {j = Z}   {k = Z}   = LTSucc+accPlusLT' {j = Z}   {k = S k} = LTStep (accPlusLT' {j = Z} {k = k})+accPlusLT' {j = S j} {k = k}   = rewrite sym $ plusSuccRightSucc k (S j) in+                                 ltSuccSucc accPlusLT'+++||| Division and modulus on `Nat`, inspired by the definition in the+||| Agda standard library.+|||+||| This uses well-founded recursion on `LT'`.+|||+||| @ dividend the dividend+||| @ divisor the divisor+||| @ nonzero division by zero is nonsense+total -- yay!+divMod : (dividend, divisor : Nat) ->+         {auto nonzero : So (not (decAsBool (decEq divisor Z)))} ->+         DivMod dividend divisor+divMod _     Z     {nonzero} = absurd nonzero+divMod Z     (S k)           = DivModRes 0 FZ Refl+divMod (S j) (S k) {nonzero} = wfInd {P=P} stepDiv (S j) (S k) nonzero+  where+    ||| The goal passed to the accessibility eliminator.+    |||+    ||| This is responsible for generating the goal in the+    ||| well-founded fixed point.+    |||+    ||| @ dividend the dividend to recurse over+    P : (dividend : Nat) -> Type+    P dividend = (divisor : Nat) -> (nonzero : So (not (decAsBool (decEq divisor Z)))) -> DivMod dividend divisor+++    ||| Well-founded recursion needs a recursion operator.+    |||+    ||| @ dividend the dividend we are recursing over+    ||| @ rec the recursive call provided by the well-founded induction operator+    stepDiv : (dividend : Nat) -> (rec : (d' : Nat) -> LT' d' dividend -> P d') -> P dividend+    -- We need not consider division by zero+    stepDiv dividend rec   Z     nonzero = absurd nonzero+    -- Dividing zero by anyting else gives 0, with 0 remainder+    stepDiv Z rec (S k) nonzero = DivModRes 0 0 Refl+    -- To divide two non-zero values, we must know which is larger+    stepDiv (S j) rec (S k) nonzero with (cmp j k)+      -- n / n = 1 remainder 0+      stepDiv (S j)                 rec (S j)                 nonzero | CmpEQ      =+        DivModRes 1 0 (sym $ cong (plusZeroRightNeutral j))+      -- if n < m, then m = n + r, and the quotient is 0 with remainder r+      stepDiv (S j)                 rec (S (plus j (S diff))) nonzero | CmpLT diff =+        DivModRes 0 (toFin (S j) diff) $+          rewrite toFinAndBack j diff+          in sym $ cong (plusZeroRightNeutral j)+      -- if n > m, then n = m + d, and the quotient is 1 + ((n - m) / m) with the same remainder+      stepDiv (S (plus k (S diff))) rec (S k)                 nonzero | CmpGT diff =+        let res = rec (S diff) accPlusLT' (S k) Oh+        in case res of+             DivModRes quotient remainder ok =>+               DivModRes (S quotient) remainder $+                 rewrite plusAssociative (finToNat remainder) (S k) (mult quotient (S k)) in+                 rewrite plusCommutative (finToNat remainder) (S k) in+                 rewrite sym $ plusAssociative (S k) (finToNat remainder) (mult quotient (S k)) in+                 rewrite ok in Refl++

@@ -34,8 +34,10 @@ myID = Lift (return (MkPID prim__vm))  ||| Send a message to another process-send : ProcID msg -> msg -> Process msg ()-send (MkPID p) m = Lift (sendToThread p (prim__vm, m))+||| Returns whether the send was unsuccessful.+send : ProcID msg -> msg -> Process msg Bool+send (MkPID p) m = Lift (do x <- sendToThread p (prim__vm, m)+                            return (x == 1))  ||| Return whether a message is waiting in the queue msgWaiting : Process msg Bool

@@ -9,8 +9,9 @@           Control.WellFounded,           Classes.Verified,           Data.Fun, Data.Rel,-          Data.Hash, Data.Matrix,-          Data.Nat,+          Data.Hash,+          Data.Matrix, Data.Matrix.Algebraic, Data.Matrix.Numeric,+          Data.Nat.DivMod, Data.Nat.DivMod.IteratedSubtraction,           Data.ZZ, Data.Sign,           Data.BoundedList,           Data.Heap,

@@ -0,0 +1,57 @@+-- ------------------------------------------------------------- [ Default.idr ]+-- Module    : Default.idr+-- Copyright : (c) The Idris Community+-- License   : see LICENSE+-- --------------------------------------------------------------------- [ EOH ]++||| A logging effect that allows messages to be logged using both+||| numerical levels and user specified categories. The higher the+||| logging level the grater in verbosity the logging.+|||+||| In this effect the resource we are computing over is the logging+||| level itself and the list of categories to show.+|||+module Effect.Logging.Default++import Effects+import public Effect.Logging.Level++import Control.IOExcept -- TODO Add IOExcept Logger.++||| A Logging effect to log levels and categories.+data Logging : Effect where+    Log : (Eq a, Show a) =>+          (lvl : Nat)+       -> (cats : List a)+       -> (msg : String)+       -> Logging () (Nat,List a) (\v => (Nat,List a))++||| The Logging effect.+|||+||| @cTy The type used to differentiate categories.+LOG : (cTy : Type) -> EFFECT+LOG a = MkEff (Nat, List a) Logging++instance Handler Logging IO where+    handle (l,cs) (Log lvl cs' msg) k = do+      case lvl <= l  of+        False => k () (l,cs)+        True  =>  do+          let res = and $ map (\x => elem x cs') cs+          let prompt = if isNil cs then "" else show cs+          if res || isNil cs+            then do+              printLn $ unwords [show lvl, ":", prompt, ":", msg]+              k () (l,cs)+            else k () (l,cs)++||| Log the given message at the given level and assign it the list of categories.+|||+||| @l The logging level.+||| @cs The logging categories.+||| @m THe message to be logged.+log : (Show a, Eq a) => (l : Nat)+    -> (cs : List a) -> (m : String) -> Eff () [LOG a]+log lvl cs msg = call $ Log lvl cs msg++-- --------------------------------------------------------------------- [ EOF ]

@@ -0,0 +1,49 @@+-- -------------------------------------------------------------- [ Levels.idr ]+-- Module    : Levels.idr+-- Copyright : (c) Jan de Muijnck-Hughes+-- License   : see LICENSE+-- --------------------------------------------------------------------- [ EOH ]+||| Common aliases and definitions of Logging Levels.+module Effect.Logging.Level++%access public+-- ---------------------------------------------- [ Nat Derived Logging Levels ]+--+-- Several aliases have been defined to aide in semantic use of the+-- logging levels. These aliases have come from the Log4j family of+-- loggers.++||| No events will be logged.+OFF : Nat+OFF = 0++||| A severe error that will prevent the application from continuing.+FATAL : Nat+FATAL = 1++||| An error in the application, possibly recoverable.+ERROR : Nat+ERROR = 2++||| An event that might possible lead to an error.+WARN : Nat+WARN = 3++|||  An event for informational purposes.+INFO : Nat+INFO = 4++||| A general debugging event.+DEBUG : Nat+DEBUG = 5++||| A fine-grained debug message, typically capturing the flow through+||| the application.+TRACE : Nat+TRACE = 6++||| All events should be logged.+ALL : Nat+ALL = 7++-- --------------------------------------------------------------------- [ EOF ]

@@ -0,0 +1,48 @@+-- -------------------------------------------------------------- [ Simple.idr ]+-- Module    : Logging.idr+-- Copyright : (c) The Idris Community+-- License   : see LICENSE+--------------------------------------------------------------------- [ EOH ]++||| A simple logging effect that allows messages to be logged at+||| different numerical level. The higher the number the grater in+||| verbosity the logging.+|||+||| In this effect the resource we are computing over is the logging+||| level itself.+|||+module Effect.Logging.Simple++import Effects+import public Effect.Logging.Level++import Control.IOExcept -- TODO Add IO Logging Handler++||| A Logging effect that displays a logging message to be logged at a+||| certain level.+data Logging : Effect where+    Log : (lvl : Nat)+       -> (msg : String)+       -> Logging () Nat (\v => Nat)++||| A Logging Effect.+LOG : EFFECT+LOG = MkEff Nat Logging++-- For logging in the IO context+instance Handler Logging IO where+    handle l (Log lvl msg) k = do+      case lvl <= l  of+        False   => k () l+        True  =>  do+          printLn $ unwords [show lvl, ":", msg]+          k () l++||| Log `msg` at the given level.+|||+||| @l The level to log.+||| @m The message to log.+log : (l : Nat) -> (m : String) -> Eff () [LOG]+log lvl msg = call $ Log lvl msg++-- --------------------------------------------------------------------- [ EOF ]

@@ -2,20 +2,27 @@  import Effects --- Eff is a monad too, so we can happily use it in a monad transformer.+data MonadEffT : List EFFECT -> (Type -> Type) -> Type -> Type where+     MkMonadEffT : EffM m a xs (\v => xs) -> MonadEffT xs m a -using (xs : List EFFECT, m : Type -> Type)-  instance Functor (\a => EffM m a xs (\v => xs)) where-    map f prog = do t <- prog-                    value (f t)+instance Functor (MonadEffT xs f) where+    map f (MkMonadEffT x) = MkMonadEffT (do x' <- x+                                            pure (f x')) -  instance Applicative (\a => EffM m a xs (\v => xs)) where-    pure = value-    (<*>) f a = do f' <- f-                   a' <- a-                   value (f' a')+instance Applicative (MonadEffT xs f) where+    pure x = MkMonadEffT (pure x)+    (<*>) (MkMonadEffT f) (MkMonadEffT x) +          = MkMonadEffT (do f' <- f+                            x' <- x+                            pure (f' x')) -  instance Monad (\a => Eff m a xs (\v => xs)) where-    (>>=) = Effects.(>>=)+instance Monad (MonadEffT xs f) where+    (>>=) (MkMonadEffT x) f = MkMonadEffT (do x' <- x+                                              let MkMonadEffT fx = f x'+                                              fx) +implicit monadEffT : EffM m a xs (\v => xs) -> MonadEffT xs m a+monadEffT = MkMonadEffT +MonadEff : List EFFECT -> Type -> Type+MonadEff xs = MonadEffT xs id

@@ -2,7 +2,6 @@  import Effects import Data.Vect-import Data.Fin  data Random : Effect where       getRandom : sig Random Integer Integer

@@ -9,7 +9,7 @@  data System : Effect where      Args : sig System (List String)-     Time : sig System Int+     Time : sig System Integer      GetEnv : String -> sig System (Maybe String)      CSystem : String -> sig System Int @@ -33,7 +33,7 @@ getArgs : Eff (List String) [SYSTEM] getArgs = call Args -time : Eff Int [SYSTEM]+time : Eff Integer [SYSTEM] time = call Time  getEnv : String -> Eff (Maybe String) [SYSTEM]

@@ -0,0 +1,20 @@+module Effect.Trans++import Effects++%access public++data Trans : (Type -> Type) -> Effect where+  Lift : m a -> sig (Trans m) a++-- using (m : Type -> Type)+instance Monad m => Handler (Trans m) m where+     handle st (Lift op) k = do x <- op+                                k x ()++TRANS : (Type -> Type) -> EFFECT+TRANS m = MkEff () (Trans m)++lift : m a -> Eff a [TRANS m]+lift op = call $ Lift op+

@@ -293,15 +293,13 @@  call : {a, b: _} -> {e : Effect} ->        (eff : e t a b) ->-       {default tactics { search 100; }-          prf : EffElem e a xs} ->+       {auto prf : EffElem e a xs} ->       EffM m t xs (\v => updateResTy v xs prf eff) call e {prf} = callP prf e  implicit lift : EffM m t ys ys' ->-       {default tactics { search 100; }-          prf : SubList ys xs} ->+       {auto prf : SubList ys xs} ->        EffM m t xs (\v => updateWith (ys' v) xs prf) lift e {prf} = liftP prf e 

@@ -1,9 +1,20 @@ package effects  opts    = "--nobasepkgs -i ../prelude -i ../base"-modules = Effects, Effect.Default, -          Effect.Exception, Effect.File, Effect.State,-          Effect.Random, Effect.StdIO, Effect.Select,-          Effect.Memory, Effect.System+modules = Effects+        , Effect.Default+        , Effect.Monad +        , Effect.Exception+        , Effect.File+        , Effect.State+        , Effect.Random+        , Effect.StdIO+        , Effect.Select+        , Effect.Memory+        , Effect.System+        , Effect.Trans+        , Effect.Logging.Level+        , Effect.Logging.Simple+        , Effect.Logging.Default

@@ -119,7 +119,8 @@    ||| Make a read-only version of a unique value, which can be passed to another   ||| function without the unique value being consumed.-  implicit+  implicit -- needs a special case in the coercion code, since implicits need+           -- a concrete type to coerce!   lend : {a : UniqueType} -> a -> Borrowed a   lend x = Read x @@ -170,6 +171,8 @@ %extern prim__stderr : Ptr  %extern prim__null : Ptr+%extern prim__eqPtr : Ptr -> Ptr -> Int+%extern prim__eqManagedPtr : ManagedPtr -> ManagedPtr -> Int %extern prim__registerPtr : Ptr -> Int -> ManagedPtr  

@@ -123,7 +123,7 @@ -- List -------------------------------------------------------------------------------- -lemma_val_not_nil : {x : t, xs : List t} -> ((x :: xs) = Prelude.List.Nil {a = t} -> Void)+lemma_val_not_nil : {x : t, xs : List t} -> ((x :: xs) = Prelude.List.Nil {elem = t} -> Void) lemma_val_not_nil Refl impossible  lemma_x_eq_xs_neq : {x : t, xs : List t, y : t, ys : List t} -> (x = y) -> (xs = ys -> Void) -> ((x :: xs) = (y :: ys) -> Void)@@ -191,5 +191,26 @@        where primitiveEq : x = y              primitiveEq = believe_me (Refl {x})              postulate primitiveNotEq : x = y -> Void++--------------------------------------------------------------------------------+-- Ptr+--------------------------------------------------------------------------------++instance DecEq Ptr where+    decEq x y = if x == y then Yes primitiveEq else No primitiveNotEq+       where primitiveEq : x = y+             primitiveEq = believe_me (Refl {x})+             postulate primitiveNotEq : x = y -> Void++--------------------------------------------------------------------------------+-- ManagedPtr+--------------------------------------------------------------------------------++instance DecEq ManagedPtr where+    decEq x y = if x == y then Yes primitiveEq else No primitiveNotEq+       where primitiveEq : x = y+             primitiveEq = believe_me (Refl {x})+             postulate primitiveNotEq : x = y -> Void+  

@@ -6,7 +6,7 @@ %access public  ||| Idris's primitive IO, for building abstractions on top of-abstract +abstract data PrimIO : Type -> Type where      prim__IO : a -> PrimIO a @@ -20,13 +20,22 @@ abstract WorldRes : Type -> Type WorldRes x = x +||| An FFI specifier, which describes how a particular compiler+||| backend handles foreign function calls. record FFI where   constructor MkFFI+  ||| A family describing which types are available in the FFI   ffi_types : Type -> Type++  ||| The type used to specify the names of foreign functions in this FFI   ffi_fn : Type++  ||| How this FFI describes exported datatypes   ffi_data : Type -abstract +||| The IO type, parameterised over the FFI that is available within+||| it.+abstract data IO' : (lang : FFI) -> Type -> Type where      MkIO : (World -> PrimIO (WorldRes a)) -> IO' lang a @@ -64,6 +73,19 @@ foreign_prim f fname (FFun arg sc) env         = \x => foreign_prim f fname sc ((arg, x) :: env) +||| Call a foreign function.+|||+||| The particular semantics of foreign function calls depend on the+||| Idris compiler backend in use. For the default C backend, see the+||| documentation for `FFI_C`.+|||+||| For more details, please consult [the Idris documentation](http://docs.idris-lang.org/en/latest/reference/ffi.html).+|||+||| @ f     an FFI descriptor, which is specific to the compiler backend.+||| @ fname the name of the foreign function+||| @ ty    the Idris type for the foreign function+||| @ fty   an automatically-found proof that the Idris type works with+|||         the FFI in question %inline foreign : (f : FFI) -> (fname : ffi_fn f) -> (ty : Type) ->           {auto fty : FTy f [] ty} -> ty@@ -128,7 +150,7 @@   -- Tell erasure analysis not to erase the argument   %used MkRaw x -  -- Supported C integer types+  ||| Supported C integer types   data C_IntTypes : Type -> Type where        C_IntChar   : C_IntTypes Char        C_IntNative : C_IntTypes Int@@ -137,7 +159,7 @@        C_IntBits32 : C_IntTypes Bits32        C_IntBits64 : C_IntTypes Bits64 -  -- Supported C foreign types+  ||| Supported C foreign types   data C_Types : Type -> Type where        C_Str   : C_Types String        C_Float : C_Types Float@@ -147,6 +169,8 @@        C_Any   : C_Types (Raw a)        C_IntT  : C_IntTypes i -> C_Types i +  ||| A descriptor for the C FFI. See the constructors of `C_Types`+  ||| and `C_IntTypes` for the concrete types that are available.   FFI_C : FFI   FFI_C = MkFFI C_Types String String @@ -201,14 +225,17 @@ -- pass we only have 'JsFn' and not the constructor. %used MkJsFn x -FFI_JS : FFI                                     +||| The JavaScript FFI. The strings naming functions in this API are+||| JavaScript code snippets, into which the arguments are substituted+||| for the placeholders `%0`, `%1`, etc.+FFI_JS : FFI FFI_JS = MkFFI JS_Types String String  JS_IO : Type -> Type JS_IO = IO' FFI_JS  ---------- Foreign Exports +--------- Foreign Exports  namespace FFI_Export -- It's just like Data.List.Elem, but we don't need all the other stuff@@ -226,7 +253,7 @@   %used FFI_Prim prim    data FFI_Exportable : (f : FFI) -> List (Type, ffi_data f) -> Type -> Type where-       FFI_IO : (b : FFI_Base f xs t) -> FFI_Exportable f xs (IO t)+       FFI_IO : (b : FFI_Base f xs t) -> FFI_Exportable f xs (IO' f t)        FFI_Fun : (b : FFI_Base f xs s) -> (a : FFI_Exportable f xs t) -> FFI_Exportable f xs (s -> t)        FFI_Ret : (b : FFI_Base f xs t) -> FFI_Exportable f xs t 

@@ -215,6 +215,8 @@                      NamePart TTName |                      ||| An Idris term, to be pretty printed                      TermPart TT |+                     ||| A Raw term to be displayed by the compiler+                     RawPart Raw |                      ||| An indented sub-report, to provide more details                      SubReport (List ErrorReportPart) %name ErrorReportPart part, p@@ -399,13 +401,13 @@  instance Quotable a TT => Quotable (List a) TT where   quotedTy = `(List ~(quotedTy {a}))-  quote [] = `(List.Nil {a=~(quotedTy {a})})-  quote (x :: xs) = `(List.(::) {a=~(quotedTy {a})} ~(quote x) ~(quote xs))+  quote [] = `(List.Nil {elem=~(quotedTy {a})})+  quote (x :: xs) = `(List.(::) {elem=~(quotedTy {a})} ~(quote x) ~(quote xs))  instance Quotable a Raw => Quotable (List a) Raw where   quotedTy = `(List ~(quotedTy {a}))-  quote [] = `(List.Nil {a=~(quotedTy {a})})-  quote (x :: xs) = `(List.(::) {a=~(quotedTy {a})} ~(quote x) ~(quote xs))+  quote [] = `(List.Nil {elem=~(quotedTy {a})})+  quote (x :: xs) = `(List.(::) {elem=~(quotedTy {a})} ~(quote x) ~(quote xs))  mutual   instance Quotable TTName TT where@@ -576,42 +578,71 @@     quote (PVar x) = `(PVar {a=TT} ~(assert_total (quote x)))     quote (PVTy x) = `(PVTy {a=TT} ~(assert_total (quote x))) --instance Quotable ErrorReportPart TT where-  quotedTy = `(ErrorReportPart)-  quote (TextPart x) = `(TextPart ~(quote x))-  quote (NamePart n) = `(NamePart ~(quote n))-  quote (TermPart tm) = `(TermPart ~(quote tm))-  quote (SubReport xs) = `(SubReport ~(assert_total $ quote xs))- mutual-  quoteRaw : Raw -> TT-  quoteRaw (Var n) = `(Var ~(quote n))-  quoteRaw (RBind n b tm) = `(RBind ~(quote n) ~(assert_total $ quoteRawBinder b) ~(quoteRaw tm))-  quoteRaw (RApp tm tm') = `(RApp ~(quoteRaw tm) ~(quoteRaw tm'))-  quoteRaw RType = `(RType)-  quoteRaw (RUType u) = `(RUType ~(quote u))-  quoteRaw (RForce tm) = `(RForce ~(quoteRaw tm))-  quoteRaw (RConstant c) = `(RConstant ~(quote c))+  quoteRawTT : Raw -> TT+  quoteRawTT (Var n) = `(Var ~(quote n))+  quoteRawTT (RBind n b tm) = `(RBind ~(quote n) ~(assert_total $ quoteRawBinderTT b) ~(quoteRawTT tm))+  quoteRawTT (RApp tm tm') = `(RApp ~(quoteRawTT tm) ~(quoteRawTT tm'))+  quoteRawTT RType = `(RType)+  quoteRawTT (RUType u) = `(RUType ~(quote u))+  quoteRawTT (RForce tm) = `(RForce ~(quoteRawTT tm))+  quoteRawTT (RConstant c) = `(RConstant ~(quote c)) -  quoteRawBinder : Binder Raw -> TT-  quoteRawBinder (Lam x) = `(Lam {a=Raw} ~(quoteRaw x))-  quoteRawBinder (Pi x k) = `(Pi {a=Raw} ~(quoteRaw x) ~(quoteRaw k))-  quoteRawBinder (Let x y) = `(Let {a=Raw} ~(quoteRaw x) ~(quoteRaw y))-  quoteRawBinder (NLet x y) = `(NLet {a=Raw} ~(quoteRaw x) ~(quoteRaw y))-  quoteRawBinder (Hole x) = `(Hole {a=Raw} ~(quoteRaw x))-  quoteRawBinder (GHole x) = `(GHole {a=Raw} ~(quoteRaw x))-  quoteRawBinder (Guess x y) = `(Guess {a=Raw} ~(quoteRaw x) ~(quoteRaw y))-  quoteRawBinder (PVar x) = `(PVar {a=Raw} ~(quoteRaw x))-  quoteRawBinder (PVTy x) = `(PVTy {a=Raw} ~(quoteRaw x))+  quoteRawBinderTT : Binder Raw -> TT+  quoteRawBinderTT (Lam x) = `(Lam {a=Raw} ~(quoteRawTT x))+  quoteRawBinderTT (Pi x k) = `(Pi {a=Raw} ~(quoteRawTT x) ~(quoteRawTT k))+  quoteRawBinderTT (Let x y) = `(Let {a=Raw} ~(quoteRawTT x) ~(quoteRawTT y))+  quoteRawBinderTT (NLet x y) = `(NLet {a=Raw} ~(quoteRawTT x) ~(quoteRawTT y))+  quoteRawBinderTT (Hole x) = `(Hole {a=Raw} ~(quoteRawTT x))+  quoteRawBinderTT (GHole x) = `(GHole {a=Raw} ~(quoteRawTT x))+  quoteRawBinderTT (Guess x y) = `(Guess {a=Raw} ~(quoteRawTT x) ~(quoteRawTT y))+  quoteRawBinderTT (PVar x) = `(PVar {a=Raw} ~(quoteRawTT x))+  quoteRawBinderTT (PVTy x) = `(PVTy {a=Raw} ~(quoteRawTT x))  instance Quotable Raw TT where   quotedTy = `(Raw)-  quote = quoteRaw+  quote = quoteRawTT  instance Quotable (Binder Raw) TT where   quotedTy = `(Binder Raw)-  quote = quoteRawBinder+  quote = quoteRawBinderTT++mutual+  quoteRawRaw : Raw -> Raw+  quoteRawRaw (Var n) = `(Var ~(quote n))+  quoteRawRaw (RBind n b tm) = `(RBind ~(quote n) ~(assert_total $ quoteRawBinderRaw b) ~(quoteRawRaw tm))+  quoteRawRaw (RApp tm tm') = `(RApp ~(quoteRawRaw tm) ~(quoteRawRaw tm'))+  quoteRawRaw RType = `(RType)+  quoteRawRaw (RUType u) = `(RUType ~(quote u))+  quoteRawRaw (RForce tm) = `(RForce ~(quoteRawRaw tm))+  quoteRawRaw (RConstant c) = `(RConstant ~(quote c))++  quoteRawBinderRaw : Binder Raw -> Raw+  quoteRawBinderRaw (Lam x) = `(Lam {a=Raw} ~(quoteRawRaw x))+  quoteRawBinderRaw (Pi x k) = `(Pi {a=Raw} ~(quoteRawRaw x) ~(quoteRawRaw k))+  quoteRawBinderRaw (Let x y) = `(Let {a=Raw} ~(quoteRawRaw x) ~(quoteRawRaw y))+  quoteRawBinderRaw (NLet x y) = `(NLet {a=Raw} ~(quoteRawRaw x) ~(quoteRawRaw y))+  quoteRawBinderRaw (Hole x) = `(Hole {a=Raw} ~(quoteRawRaw x))+  quoteRawBinderRaw (GHole x) = `(GHole {a=Raw} ~(quoteRawRaw x))+  quoteRawBinderRaw (Guess x y) = `(Guess {a=Raw} ~(quoteRawRaw x) ~(quoteRawRaw y))+  quoteRawBinderRaw (PVar x) = `(PVar {a=Raw} ~(quoteRawRaw x))+  quoteRawBinderRaw (PVTy x) = `(PVTy {a=Raw} ~(quoteRawRaw x))++instance Quotable Raw Raw where+  quotedTy = `(Raw)+  quote = quoteRawRaw++instance Quotable (Binder Raw) Raw where+  quotedTy = `(Binder Raw)+  quote = quoteRawBinderRaw++instance Quotable ErrorReportPart TT where+  quotedTy = `(ErrorReportPart)+  quote (TextPart x) = `(TextPart ~(quote x))+  quote (NamePart n) = `(NamePart ~(quote n))+  quote (TermPart tm) = `(TermPart ~(quote tm))+  quote (RawPart tm) = `(RawPart ~(quote tm))+  quote (SubReport xs) = `(SubReport ~(assert_total $ quote xs))  instance Quotable Tactic TT where   quotedTy = `(Tactic)

@@ -7,24 +7,52 @@  import Builtins import Prelude.Applicative+import Prelude.Basics+import Prelude.Bool import Prelude.Functor import Prelude.List import Prelude.Maybe import Prelude.Monad+import Prelude.Nat import Language.Reflection -||| Arguments, with plicity.-data Arg : Type where-  ||| An explicit argument-  Explicit : TTName -> Raw -> Arg+data Fixity = Infixl Nat | Infixr Nat | Infix Nat | Prefix Nat -  ||| An implicit argument, to be solved by unification-  Implicit : TTName -> Raw -> Arg+||| Erasure annotations reflect Idris's idea of what is intended to be+||| erased.+data Erasure = Erased | NotErased -  ||| A type-class constraint argument, to be solved by type class-  ||| resolution-  Constraint : TTName -> Raw -> Arg+||| How an argument is provided in high-level Idris+data Plicity =+  ||| The argument is directly provided at the application site+  Explicit |+  ||| The argument is found by Idris at the application site+  Implicit |+  ||| The argument is solved using type class resolution+  Constraint +||| Function arguments+|||+||| These are the simplest representation of argument lists, and are+||| used for functions.+record FunArg where+  constructor MkFunArg+  argName : TTName+  argTy   : Raw+  plicity : Plicity+  erasure : Erasure++||| Type constructor arguments+|||+||| Each argument is identified as being either a parameter that is+||| consistent in all constructors, or an index that varies based on+||| which constructor is selected.+data TyConArg =+  ||| Parameters are uniform across the constructors+  TyConParameter FunArg |+  ||| Indices are not uniform+  TyConIndex FunArg+ ||| A type declaration data TyDecl : Type where   ||| A type declaration.@@ -36,38 +64,35 @@   ||| @ fn the name to be declared, fully-qualified   ||| @ args the arguments to the function   ||| @ ret the final return type-  Declare : (fn : TTName) -> (args : List Arg) -> (ret : Raw) -> TyDecl+  Declare : (fn : TTName) -> (args : List FunArg) -> (ret : Raw) -> TyDecl  ||| A single pattern-matching clause data FunClause : Type where   MkFunClause : (lhs, rhs : Raw) -> FunClause-  MkImpossibleClause : (lhs : Raw) -> FunClause  ||| A reflected function definition. data FunDefn : Type where   DefineFun : TTName -> List FunClause -> FunDefn -||| An argument to a type constructor.-data TyConArg : Type where-  ||| Parameters are consistent across all constructors of the type-  Parameter : TTName -> Raw -> TyConArg -  ||| Indices are allowed to vary across constructors-  Index : TTName -> Raw -> TyConArg+data CtorArg = CtorParameter FunArg | CtorField FunArg  ||| A reflected datatype definition-data Datatype : Type where-  ||| A reflected datatype definition-  |||-  ||| @ familyName the name of the type constructor-  ||| @ tyConArgs the arguments to the type constructor-  ||| @ tyConRes the result of the type constructor-  ||| @ constrs the constructors, with their types-  MkDatatype : (familyName : TTName) ->-               (tyConArgs : List TyConArg) -> (tyConRes : Raw) ->-               (constrs : List (TTName, Raw)) ->-               Datatype+record Datatype where+  constructor MkDatatype +  ||| The name of the type constructor+  familyName : TTName++  ||| The arguments to the type constructor+  tyConArgs : List TyConArg++  ||| The result of the type constructor+  tyConRes : Raw++  ||| The constructors for the family+  constructors : List (TTName, List CtorArg, Raw)+ ||| A reflected elaboration script. abstract data Elab : Type -> Type where@@ -85,7 +110,10 @@   prim__LookupTy : TTName -> Elab (List (TTName, NameType, TT))   prim__LookupDatatype : TTName -> Elab (List Datatype) +  prim__Check : Raw -> Elab (TT, TT)+   prim__SourceLocation : Elab SourceLocation+  prim__Namespace : Elab (List String)    prim__Forget : TT -> Elab Raw @@ -93,7 +121,8 @@    prim__Solve : Elab ()   prim__Fill : Raw -> Elab ()-  prim__Apply : Raw -> Elab ()+  prim__Apply : Raw -> List (Bool, Int) -> Elab (List (TTName, TTName))+  prim__MatchApply : Raw -> List (Bool, Int) -> Elab (List (TTName, TTName))   prim__Focus : TTName -> Elab ()   prim__Unfocus : TTName -> Elab ()   prim__Attack : Elab ()@@ -105,18 +134,24 @@   prim__Forall : TTName -> Raw -> Elab ()   prim__PatVar : TTName -> Elab ()   prim__PatBind : TTName -> Elab ()+  prim__LetBind : TTName -> Raw -> Raw -> Elab ()    prim__Compute : Elab ()+  prim__Normalise : (List (TTName, Binder TT)) -> TT -> Elab TT+  prim__Whnf : TT -> Elab TT    prim__DeclareType : TyDecl -> Elab ()   prim__DefineFunction : FunDefn -> Elab ()   prim__AddInstance : TTName -> TTName -> Elab ()    prim__ResolveTC : TTName -> Elab ()+  prim__Search : Int -> List TTName -> Elab ()   prim__RecursiveElab : Raw -> Elab () -> Elab (TT, TT) -  prim__Debug : {a : Type} -> Maybe String -> Elab a+  prim__Fixity : String -> Elab Fixity +  prim__Debug : {a : Type} -> List ErrorReportPart -> Elab a+  prim__Metavar : TTName -> Elab ()  ------------- -- Public API@@ -186,11 +221,21 @@                             []    => fail [TextPart "No datatype named", NamePart n]                             xs    => fail [TextPart "More than one datatype named", NamePart n] +  ||| Attempt to type-check a term, getting back itself and its type+  check : (tm : Raw) -> Elab (TT, TT)+  check tm = prim__Check tm+   ||| Convert a type-annotated reflected term to its untyped   ||| equivalent   forgetTypes : TT -> Elab Raw   forgetTypes tt = prim__Forget tt +  ||| Get the goal type as a Raw term+  goalType : Elab Raw+  goalType = do g <- getGoal+                forgetTypes (snd g)++   ||| Generate a unique name based on some hint.   |||   ||| **NB**: the generated name is unique _for this run of the@@ -206,10 +251,50 @@   fill : Raw -> Elab ()   fill tm = prim__Fill tm -  ||| Fill with unification-  apply : Raw -> Elab ()-  apply tm = prim__Apply tm+  ||| Attempt to apply an operator to fill the current hole,+  ||| potentially solving arguments by unification.+  |||+  ||| The return value is a list of pairs of names, one for each input+  ||| argument. The first projection of these pairs is the original+  ||| name of the argument, from the type declaration, and the second+  ||| projection is the hole into which it is placed.+  |||+  ||| Note that not all of the returned hole names still exist, as+  ||| they may have been solved.+  |||+  ||| @ op the term to apply+  |||+  ||| @ argSpec instructions for finding the arguments to the term,+  |||     where the Boolean states whether or not to attempt to solve+  |||     the argument and the Int gives the priority in which to do+  |||     so+  apply : (op : Raw) ->+          (argSpec : List (Bool, Int)) ->+          Elab (List (TTName, TTName))+  apply tm argSpec = prim__Apply tm argSpec +  ||| Attempt to apply an operator to fill the current hole,+  ||| potentially solving arugments by matching.+  |||+  ||| The return value is a list of pairs of names, one for each input+  ||| argument. The first projection of these pairs is the original+  ||| name of the argument, from the type declaration, and the second+  ||| projection is the hole into which it is placed.+  |||+  ||| Note that not all of the returned hole names still exist, as+  ||| they may have been solved.+  |||+  ||| @ op the term to apply+  |||+  ||| @ argSpec instructions for finding the arguments to the term,+  |||     where the Boolean states whether or not to attempt to solve+  |||     the argument and the Int gives the priority in which to do+  |||     so+  matchApply : (op : Raw) ->+               (argSpec : List (Bool, Int)) ->+               Elab (List (TTName, TTName))+  matchApply tm argSpec = prim__Apply tm argSpec+   ||| Move the focus to the specified hole   |||   ||| @ hole the hole to focus on@@ -241,11 +326,15 @@   ||| the body. Requires that the hole be in binding form (use   ||| `attack`).   |||-  ||| @ n the name to use for the argument, or `Nothing` to use the name-  |||   in the corresponding hole type (a dependent function)-  intro : (n : Maybe TTName) -> Elab ()-  intro n = prim__Intro n+  ||| @ n the name to use for the argument+  intro : (n : TTName) -> Elab ()+  intro n = prim__Intro (Just n) +  ||| Introduce a lambda binding around the current hole and focus on+  ||| the body, using the name provided by the type of the hole.+  intro' : Elab ()+  intro' = prim__Intro Nothing+   ||| Introduce a dependent function type binding into the current hole,   ||| and focus on the body.   forall : TTName -> Raw -> Elab ()@@ -259,10 +348,31 @@   patbind : TTName -> Elab ()   patbind n = prim__PatBind n +  ||| Introduce a new let binding+  |||+  ||| @ n the name to let bind+  ||| @ ty the type of the term to be let-bound+  ||| @ tm the term to be bound+  letbind : (n : TTName) -> (ty, tm : Raw) -> Elab ()+  letbind n ty tm = prim__LetBind n ty tm+   ||| Normalise the goal.   compute : Elab ()   compute = prim__Compute +  ||| Normalise a term in some lexical environment+  |||+  ||| @ env the environment in which to compute (get one of these from `getEnv`)+  ||| @ term the term to normalise+  normalise : (env : List (TTName, Binder TT)) -> (term : TT) -> Elab TT+  normalise env term = prim__Normalise env term++  ||| Reduce a closed term to weak-head normal form+  |||+  ||| @ term the term to reduce+  whnf : (term : TT) -> Elab TT+  whnf term = prim__Whnf term+   ||| Find the source context for the elaboration script   getSourceLocation : Elab SourceLocation   getSourceLocation = prim__SourceLocation@@ -273,6 +383,14 @@                       fill (quote loc)                       solve +  ||| Get the current namespace at the point of tactic execution. This+  ||| allows scripts to define top-level names conveniently.+  |||+  ||| The namespace is represented as a reverse-order list of strings,+  ||| just as in the representation of names.+  currentNamespace : Elab (List String)+  currentNamespace = prim__Namespace+   ||| Attempt to rewrite the goal using an equality.   |||   ||| The tactic searches the goal for applicable subterms, and@@ -306,12 +424,32 @@   resolveTC : (fn : TTName) -> Elab ()   resolveTC fn = prim__ResolveTC fn +  ||| Use Idris's internal proof search.+  search : Elab ()+  search = prim__Search 100 []++  ||| Use Idris's internal proof search, with more control.+  |||+  ||| @ depth the search depth+  ||| @ hints additional names to try+  search' : (depth : Int) -> (hints : List TTName) -> Elab ()+  search' depth hints = prim__Search depth hints++  ||| Look up the declared fixity for an operator.+  |||+  ||| The lookup fails if the operator does not yet have a fixity or+  ||| if the string is not a valid operator.+  |||+  ||| @ operator the operator string to look up+  operatorFixity : (operator : String) -> Elab Fixity+  operatorFixity operator = prim__Fixity operator+   ||| Halt elaboration, dumping the internal state for inspection.   |||   ||| This is intended for elaboration script developers, not for   ||| end-users. Use `fail` for final scripts.   debug : Elab a-  debug = prim__Debug Nothing+  debug = prim__Debug []    ||| Halt elaboration, dumping the internal state and displaying a   ||| message.@@ -320,8 +458,14 @@   ||| end-users. Use `fail` for final scripts.   |||   ||| @ msg the message to display-  debugMessage : (msg : String) -> Elab a-  debugMessage msg = prim__Debug (Just msg)+  debugMessage : (msg : List ErrorReportPart) -> Elab a+  debugMessage msg = prim__Debug msg++  ||| Create a new top-level metavariable to solve the current hole.+  |||+  ||| @ name the name for the top-level variable+  metavar : (name : TTName) -> Elab ()+  metavar name = prim__Metavar name    ||| Recursively invoke the reflected elaborator with some goal.   |||

@@ -31,6 +31,7 @@          | CantResolve TT          | InvalidTCArg TTName TT          | CantResolveAlts (List TTName)+         | NoValidAlts (List TTName)          | IncompleteTerm TT          | NoEliminator String TT          | UniverseError

@@ -24,6 +24,9 @@ import public Prelude.Pairs import public Prelude.Stream import public Prelude.Providers+import public Prelude.Show+import public Prelude.Interactive+import public Prelude.File import public Decidable.Equality import public Language.Reflection import public Language.Reflection.Errors@@ -37,114 +40,11 @@ decAsBool (No _)  = False  --- Show and instances--class Show a where-    partial show : a -> String--instance Show Int where-    show = prim__toStrInt--instance Show Integer where-    show = prim__toStrBigInt--instance Show Float where-    show = prim__floatToStr---firstCharIs : (Char -> Bool) -> String -> Bool-firstCharIs p s with (strM s)-  firstCharIs p ""             | StrNil = False-  firstCharIs p (strCons c cs) | StrCons c cs = p c--protectEsc : (Char -> Bool) -> String -> String -> String-protectEsc p f s = f ++ (if firstCharIs p s then "\\&" else "") ++ s--showLitChar : Char -> String -> String-showLitChar '\a'   = ("\\a" ++)-showLitChar '\b'   = ("\\b" ++)-showLitChar '\f'   = ("\\f" ++)-showLitChar '\n'   = ("\\n" ++)-showLitChar '\r'   = ("\\r" ++)-showLitChar '\t'   = ("\\t" ++)-showLitChar '\v'   = ("\\v" ++)-showLitChar '\SO'  = protectEsc (== 'H') "\\SO"-showLitChar '\DEL' = ("\\DEL" ++)-showLitChar '\\'   = ("\\\\" ++)-showLitChar c      = case getAt (cast (cast {to=Int} c)) asciiTab of-                          Just k => strCons '\\' . (k ++)-                          Nothing => if (c > '\DEL')-                                        then strCons '\\' . protectEsc isDigit (show (cast {to=Int} c))-                                        else strCons c-  where asciiTab : List String-        asciiTab = ["NUL", "SOH", "STX", "ETX", "EOT", "ENQ", "ACK", "BEL",-                    "BS",  "HT",  "LF",  "VT",  "FF",  "CR",  "SO",  "SI",-                    "DLE", "DC1", "DC2", "DC3", "DC4", "NAK", "SYN", "ETB",-                    "CAN", "EM",  "SUB", "ESC", "FS",  "GS",  "RS",  "US"]--        getAt : Nat -> List String -> Maybe String-        getAt Z     (x :: xs) = Just x-        getAt (S k) (x :: xs) = getAt k xs-        getAt _     []        = Nothing--showLitString : List Char -> String -> String-showLitString []        = id-showLitString ('"'::cs) = ("\\\"" ++) . showLitString cs-showLitString (c  ::cs) = showLitChar c . showLitString cs--instance Show Char where-  show '\'' = "'\\''"-  show c    = strCons '\'' (showLitChar c "'")--instance Show String where-  show cs = strCons '"' (showLitString (cast cs) "\"")--instance Show Nat where-    show n = show (the Integer (cast n))--instance Show Bool where-    show True = "True"-    show False = "False"--instance Show () where-  show () = "()"--instance Show Bits8 where-  show b = b8ToString b--instance Show Bits16 where-  show b = b16ToString b--instance Show Bits32 where-  show b = b32ToString b--instance Show Bits64 where-  show b = b64ToString b--instance (Show a, Show b) => Show (a, b) where-    show (x, y) = "(" ++ show x ++ ", " ++ show y ++ ")"--instance Show a => Show (List a) where-    show xs = "[" ++ show' "" xs ++ "]" where-        show' acc []        = acc-        show' acc [x]       = acc ++ show x-        show' acc (x :: xs) = show' (acc ++ show x ++ ", ") xs--instance Show a => Show (Maybe a) where-    show Nothing = "Nothing"-    show (Just x) = "Just " ++ show x--instance (Show a, {y : a} -> Show (p y)) => Show (Sigma a p) where-    show (y ** prf) = "(" ++ show y ++ " ** " ++ show prf ++ ")"-       ---- Functor instances  instance Functor PrimIO where     map f io = prim_io_bind io (prim_io_return . f) -instance Functor (IO' ffi) where-    map f io = io_bind io (\b => io_return (f b))- instance Functor Maybe where     map f (Just x) = Just (f x)     map f Nothing  = Nothing@@ -160,12 +60,6 @@      am <*> bm = prim_io_bind am (\f => prim_io_bind bm (prim_io_return . f)) -instance Applicative (IO' ffi) where-    pure x = io_return x-    f <*> a = io_bind f (\f' =>-                io_bind a (\a' =>-                  io_return (f' a')))- instance Applicative Maybe where     pure = Just @@ -202,9 +96,6 @@ instance Monad PrimIO where     b >>= k = prim_io_bind b k -instance Monad (IO' ffi) where-    b >>= k = io_bind b k- instance Monad Maybe where     Nothing  >>= k = Nothing     (Just x) >>= k = k x@@ -328,183 +219,6 @@ uncurry : (a -> b -> c) -> (a, b) -> c uncurry f (a, b) = f a b ----- some basic io--||| Output a string to stdout without a trailing newline-putStr : String -> IO' ffi ()-putStr x = do prim_write x-              return ()--||| Output a string to stdout with a trailing newline-putStrLn : String -> IO' ffi ()-putStrLn x = putStr (x ++ "\n")--||| Output something showable to stdout, without a trailing newline-partial-print : Show a => a -> IO' ffi ()-print x = putStr (show x)--||| Output something showable to stdout, with a trailing newline-partial-printLn : Show a => a -> IO' ffi ()-printLn x = putStrLn (show x)--||| Read one line of input from stdin, without the trailing newline-partial-getLine : IO' ffi String-getLine = do x <- prim_read-             return (reverse (trimNL (reverse x)))-  where trimNL : String -> String-        trimNL str with (strM str)-          trimNL "" | StrNil = ""-          trimNL (strCons '\n' xs) | StrCons _ _ = xs-          trimNL (strCons x xs)    | StrCons _ _ = strCons x xs--||| Write a single character to stdout-partial-putChar : Char -> IO ()-putChar c = foreign FFI_C "putchar" (Int -> IO ()) (cast c)--||| Write a singel character to stdout, with a trailing newline-partial-putCharLn : Char -> IO ()-putCharLn c = putStrLn (singleton c)--||| Read a single character from stdin-partial-getChar : IO Char-getChar = map cast $ foreign FFI_C "getchar" (IO Int)------ some basic file handling--||| A file handle-abstract-data File = FHandle Ptr--||| Standard input-stdin : File-stdin = FHandle prim__stdin--||| Standard output-stdout : File-stdout = FHandle prim__stdout--||| Standard output-stderr : File-stderr = FHandle prim__stderr--||| Call the RTS's file opening function-do_fopen : String -> String -> IO Ptr-do_fopen f m-   = foreign FFI_C "fileOpen" (String -> String -> IO Ptr) f m--||| Open a file-||| @ f the filename-||| @ m the mode as a String (`"r"`, `"w"`, or `"r+"`)-fopen : (f : String) -> (m : String) -> IO File-fopen f m = do h <- do_fopen f m-               return (FHandle h)--||| Modes for opening files-data Mode = Read | Write | ReadWrite--||| Open a file-||| @ f the filename-||| @ m the mode-partial-openFile : (f : String) -> (m : Mode) -> IO File-openFile f m = fopen f (modeStr m) where-  modeStr Read  = "r"-  modeStr Write = "w"-  modeStr ReadWrite = "r+"--partial-do_fclose : Ptr -> IO ()-do_fclose h = foreign FFI_C "fileClose" (Ptr -> IO ()) h--partial-closeFile : File -> IO ()-closeFile (FHandle h) = do_fclose h--partial-do_fread : Ptr -> IO' l String-do_fread h = prim_fread h--fgetc : File -> IO Char-fgetc (FHandle h) = return (cast !(foreign FFI_C "fgetc" (Ptr -> IO Int) h))--fgetc' : File -> IO (Maybe Char)-fgetc' (FHandle h)-   = do x <- foreign FFI_C "fgetc" (Ptr -> IO Int) h-        if (x < 0) then return Nothing-                   else return (Just (cast x))--fflush : File -> IO ()-fflush (FHandle h) = foreign FFI_C "fflush" (Ptr -> IO ()) h--do_popen : String -> String -> IO Ptr-do_popen f m = foreign FFI_C "do_popen" (String -> String -> IO Ptr) f m--popen : String -> Mode -> IO File-popen f m = do ptr <- do_popen f (modeStr m)-               return (FHandle ptr)-  where-    modeStr Read  = "r"-    modeStr Write = "w"-    modeStr ReadWrite = "r+"--pclose : File -> IO ()-pclose (FHandle h) = foreign FFI_C "pclose" (Ptr -> IO ()) h---- mkForeign (FFun "idris_readStr" [FPtr, FPtr] (FAny String))---                        prim__vm h--partial-fread : File -> IO' l String-fread (FHandle h) = do_fread h--partial-do_fwrite : Ptr -> String -> IO ()-do_fwrite h s = do prim_fwrite h s-                   return ()--partial-fwrite : File -> String -> IO ()-fwrite (FHandle h) s = do_fwrite h s--partial-do_feof : Ptr -> IO Int-do_feof h = foreign FFI_C "fileEOF" (Ptr -> IO Int) h--||| Check if a file handle has reached the end-feof : File -> IO Bool-feof (FHandle h) = do eof <- do_feof h-                      return (not (eof == 0))--partial-do_ferror : Ptr -> IO Int-do_ferror h = foreign FFI_C "fileError" (Ptr -> IO Int) h--ferror : File -> IO Bool-ferror (FHandle h) = do err <- do_ferror h-                        return (not (err == 0))--fpoll : File -> IO Bool-fpoll (FHandle h) = do p <- foreign FFI_C "fpoll" (Ptr -> IO Int) h-                       return (p > 0)--||| Check if a foreign pointer is null-partial-nullPtr : Ptr -> IO Bool-nullPtr p = do ok <- foreign FFI_C "isNull" (Ptr -> IO Int) p-               return (ok /= 0)--||| Check if a supposed string was actually a null pointer-partial-nullStr : String -> IO Bool-nullStr p = do ok <- foreign FFI_C "isNull" (String -> IO Int) p-               return (ok /= 0)- namespace JSNull   ||| Check if a foreign pointer is null   partial@@ -524,12 +238,6 @@ eqPtr x y = do eq <- foreign FFI_C "idris_eqPtr" (Ptr -> Ptr -> IO Int) x y                return (eq /= 0) -||| Check whether a file handle is actually a null pointer-partial-validFile : File -> IO Bool-validFile (FHandle h) = do x <- nullPtr h-                           return (not x)- ||| Loop while some test is true ||| ||| @ test the condition of the loop@@ -541,18 +249,27 @@                             while t b                     else return () -||| Read the contents of a file into a string-partial -- no error checking!-readFile : String -> IO String-readFile fn = do h <- openFile fn Read-                 c <- readFile' h ""-                 closeFile h-                 return c-  where-    partial-    readFile' : File -> String -> IO String-    readFile' h contents =-       do x <- feof h-          if not x then do l <- fread h-                           readFile' h (contents ++ l)-                   else return contents+------- Some error rewriting++%language ErrorReflection+  +private+cast_part : TT -> ErrorReportPart+cast_part (P Bound n t) = TextPart "unknown type"+cast_part x = TermPart x+  +%error_handler+cast_error : Err -> Maybe (List ErrorReportPart)+cast_error (CantResolve `(Cast ~x ~y))+     = Just [TextPart "Can't cast from",+             cast_part x,+             TextPart "to",+             cast_part y]+cast_error _ = Nothing++%error_handler+num_error : Err -> Maybe (List ErrorReportPart)+num_error (CantResolve `(Num ~x))+     = Just [TermPart x, TextPart "is not a numeric type"]+num_error _ = Nothing+

@@ -5,6 +5,7 @@ import Prelude.Basics import Prelude.Bool import Prelude.Classes+import Prelude.Foldable import Prelude.Functor  ---- Applicative functors/Idioms@@ -48,3 +49,26 @@ when : Applicative f => Bool -> Lazy (f ()) -> f () when True f = Force f when False f = pure ()++||| Fold using Alternative+|||+||| If you have a left-biased alternative operator `<|>`, then `choice`+||| performs left-biased choice from a list of alternatives, which means that+||| it evaluates to the left-most non-`empty` alternative.+|||+||| If the list is empty, or all values in it are `empty`, then it+||| evaluates to `empty`.+|||+||| Example:+|||+||| ```+||| -- given a parser expression like:+||| expr = literal <|> keyword <|> funcall+|||+||| -- choice lets you write this as:+||| expr = choice [literal, keyword, funcall]+||| ```+|||+||| Note: In Haskell, `choice` is called `asum`.+choice : (Foldable t, Alternative f) => t (f a) -> f a+choice x = foldr (<|>) empty x

@@ -11,8 +11,8 @@  ||| Manually assign a type to an expression. ||| @ a the type to assign-||| @ x the element to get the type-the : (a : Type) -> (x : a) -> a+||| @ value the element to get the type+the : (a : Type) -> (value : a) -> a the _ = id  ||| Constant function. Ignores its second argument.@@ -20,7 +20,7 @@ const x = \v => x  ||| Return the first element of a pair.-fst : (s, t) -> s+fst : (a, b) -> a fst (x, y) = x  ||| Return the second element of a pair.

@@ -15,7 +15,7 @@ instance Cast String Int where     cast = prim__fromStrInt -instance Cast String Float where+instance Cast String Double where     cast = prim__strToFloat  instance Cast String Integer where@@ -26,24 +26,30 @@ instance Cast Int String where     cast = prim__toStrInt -instance Cast Int Float where+instance Cast Int Double where     cast = prim__toFloatInt  instance Cast Int Integer where     cast = prim__sextInt_BigInt --- Float casts+-- Double casts -instance Cast Float String where+instance Cast Double String where     cast = prim__floatToStr -instance Cast Float Int where+instance Cast Double Int where     cast = prim__fromFloatInt +instance Cast Double Integer where+    cast = prim__fromFloatBigInt+ -- Integer casts  instance Cast Integer String where     cast = prim__toStrBigInt++instance Cast Integer Double where+    cast = prim__toFloatBigInt  -- Char casts 

@@ -46,6 +46,12 @@ instance Eq String where     (==) = boolOp prim__eqString +instance Eq Ptr where+    (==) = boolOp prim__eqPtr++instance Eq ManagedPtr where+    (==) = boolOp prim__eqManagedPtr+ instance Eq Bool where     True  == True  = True     True  == False = False

@@ -0,0 +1,156 @@+module Prelude.File++import Builtins+import Prelude.List+import Prelude.Maybe+import Prelude.Monad+import Prelude.Chars+import Prelude.Strings+import Prelude.Cast+import Prelude.Bool+import Prelude.Basics+import Prelude.Classes+import Prelude.Monad+import IO++%access public++||| A file handle+abstract+data File = FHandle Ptr++||| Standard input+stdin : File+stdin = FHandle prim__stdin++||| Standard output+stdout : File+stdout = FHandle prim__stdout++||| Standard output+stderr : File+stderr = FHandle prim__stderr++||| Call the RTS's file opening function+do_fopen : String -> String -> IO Ptr+do_fopen f m+   = foreign FFI_C "fileOpen" (String -> String -> IO Ptr) f m++||| Open a file+||| @ f the filename+||| @ m the mode as a String (`"r"`, `"w"`, or `"r+"`)+fopen : (f : String) -> (m : String) -> IO File+fopen f m = do h <- do_fopen f m+               return (FHandle h)++||| Check whether a file handle is actually a null pointer+partial+validFile : File -> IO Bool+validFile (FHandle h) = do x <- nullPtr h+                           return (not x)++||| Modes for opening files+data Mode = Read | Write | ReadWrite++||| Open a file+||| @ f the filename+||| @ m the mode+partial+openFile : (f : String) -> (m : Mode) -> IO File+openFile f m = fopen f (modeStr m) where+  modeStr Read  = "r"+  modeStr Write = "w"+  modeStr ReadWrite = "r+"++partial+do_fclose : Ptr -> IO ()+do_fclose h = foreign FFI_C "fileClose" (Ptr -> IO ()) h++partial+closeFile : File -> IO ()+closeFile (FHandle h) = do_fclose h++partial+do_fread : Ptr -> IO' l String+do_fread h = prim_fread h++fgetc : File -> IO Char+fgetc (FHandle h) = return (cast !(foreign FFI_C "fgetc" (Ptr -> IO Int) h))++fgetc' : File -> IO (Maybe Char)+fgetc' (FHandle h)+   = do x <- foreign FFI_C "fgetc" (Ptr -> IO Int) h+        if (x < 0) then return Nothing+                   else return (Just (cast x))++fflush : File -> IO ()+fflush (FHandle h) = foreign FFI_C "fflush" (Ptr -> IO ()) h++do_popen : String -> String -> IO Ptr+do_popen f m = foreign FFI_C "do_popen" (String -> String -> IO Ptr) f m++popen : String -> Mode -> IO File+popen f m = do ptr <- do_popen f (modeStr m)+               return (FHandle ptr)+  where+    modeStr Read  = "r"+    modeStr Write = "w"+    modeStr ReadWrite = "r+"++pclose : File -> IO ()+pclose (FHandle h) = foreign FFI_C "pclose" (Ptr -> IO ()) h++-- mkForeign (FFun "idris_readStr" [FPtr, FPtr] (FAny String))+--                        prim__vm h++partial+fread : File -> IO' l String+fread (FHandle h) = do_fread h++partial+do_fwrite : Ptr -> String -> IO ()+do_fwrite h s = do prim_fwrite h s+                   return ()++partial+fwrite : File -> String -> IO ()+fwrite (FHandle h) s = do_fwrite h s++partial+do_feof : Ptr -> IO Int+do_feof h = foreign FFI_C "fileEOF" (Ptr -> IO Int) h++||| Check if a file handle has reached the end+feof : File -> IO Bool+feof (FHandle h) = do eof <- do_feof h+                      return (not (eof == 0))++partial+do_ferror : Ptr -> IO Int+do_ferror h = foreign FFI_C "fileError" (Ptr -> IO Int) h++ferror : File -> IO Bool+ferror (FHandle h) = do err <- do_ferror h+                        return (not (err == 0))++fpoll : File -> IO Bool+fpoll (FHandle h) = do p <- foreign FFI_C "fpoll" (Ptr -> IO Int) h+                       return (p > 0)++||| Read the contents of a file into a string+partial -- no error checking!+readFile : String -> IO String+readFile fn = do h <- openFile fn Read+                 c <- readFile' h ""+                 closeFile h+                 return c+  where+    partial+    readFile' : File -> String -> IO String+    readFile' h contents =+       do x <- feof h+          if not x then do l <- fread h+                           readFile' h (contents ++ l)+                   else return contents++

@@ -0,0 +1,142 @@+||| Various helper functions for creating simple interactive systems.+||| +||| These are mostly intended for helping with teaching, in that they will allow+||| the easy creation of interactive programs without needing to teach IO+||| or Effects first, but they also capture some common patterns of interactive+||| programming.+module Prelude.Interactive++import Builtins+import Prelude.List+import Prelude.File+import Prelude.Bool+import Prelude.Classes+import Prelude.Strings+import Prelude.Chars+import Prelude.Show+import Prelude.Cast+import Prelude.Maybe+import Prelude.Functor+import Prelude.Monad+import IO++%access public++---- some basic io++||| Output a string to stdout without a trailing newline+putStr : String -> IO' ffi ()+putStr x = do prim_write x+              return ()++||| Output a string to stdout with a trailing newline+putStrLn : String -> IO' ffi ()+putStrLn x = putStr (x ++ "\n")++||| Output something showable to stdout, without a trailing newline+print : Show a => a -> IO' ffi ()+print x = putStr (show x)++||| Output something showable to stdout, with a trailing newline+printLn : Show a => a -> IO' ffi ()+printLn x = putStrLn (show x)++||| Read one line of input from stdin, without the trailing newline+getLine : IO' ffi String+getLine = do x <- prim_read+             return (reverse (trimNL (reverse x)))+  where trimNL : String -> String+        trimNL str with (strM str)+          trimNL "" | StrNil = ""+          trimNL (strCons '\n' xs) | StrCons _ _ = xs+          trimNL (strCons x xs)    | StrCons _ _ = strCons x xs++||| Write a single character to stdout+putChar : Char -> IO ()+putChar c = foreign FFI_C "putchar" (Int -> IO ()) (cast c)++||| Write a singel character to stdout, with a trailing newline+putCharLn : Char -> IO ()+putCharLn c = putStrLn (singleton c)++||| Read a single character from stdin+getChar : IO Char+getChar = map cast $ foreign FFI_C "getchar" (IO Int)++||| Get the command-line arguments that the program was called with.+partial+getArgs : IO (List String)+getArgs = do n <- numArgs+             ga' [] 0 n+  where+    numArgs : IO Int+    numArgs = foreign FFI_C "idris_numArgs" (IO Int)++    getArg : Int -> IO String+    getArg x = foreign FFI_C "idris_getArg" (Int -> IO String) x++    partial+    ga' : List String -> Int -> Int -> IO (List String)+    ga' acc i n = if (i == n) then (return $ reverse acc) else+                    do arg <- getArg i+                       ga' (arg :: acc) (i+1) n+++||| Process input from an open file handle, while maintaining a state.+||| @ state the input state+||| @ onRead the function to run on reading a line, returning a String to+||| output and a new state+||| @ onEOF the function to run on reaching end of file, returning a String+||| to output+partial+processHandle : File -> +                (state : a) ->+                (onRead : a -> String -> (String, a)) -> +                (onEOF : a -> String) -> +                IO ()+processHandle h acc onRead onEOF +   = if !(feof h)+        then putStr (onEOF acc)+        else do x <- fread h+                let (out, acc') = onRead acc x+                putStr out+                processHandle h acc' onRead onEOF    ++||| Process input from the standard input stream, while maintaining a state.+||| @ state the input state+||| @ onRead the function to run on reading a line, returning a String to+||| output and a new state+||| @ onEOI the function to run on reaching end of input, returning a String+||| to output+partial+processStdin : (state : a) -> +               (onRead : a -> String -> (String, a)) -> +               (onEOI : a -> String) -> IO ()+processStdin = processHandle stdin++||| A basic read-eval-print loop, maintaining a state+||| @ state the input state+||| @ prompt the prompt to show +||| @ onInput the function to run on reading input, returning a String to+||| output and a new state. Returns Nothing if the repl should exit+partial+replWith : (state : a) -> (prompt : String) -> +           (onInput : a -> String -> Maybe (String, a)) -> IO ()+replWith acc prompt fn +   = do putStr prompt+        x <- getLine+        case fn acc x of+             Just (out, acc') => do putStr out +                                    replWith acc' prompt fn+             Nothing => return ()++||| A basic read-eval-print loop+||| @ prompt the prompt to show +||| @ onInput the function to run on reading input, returning a String to+||| output +partial+repl : (prompt : String) -> +       (onInput : String -> String) -> IO ()+repl prompt fn +   = replWith () prompt (\x, s => Just (fn s, ()))+

@@ -9,6 +9,7 @@ import Prelude.Foldable import Prelude.Functor import Prelude.Maybe+import Prelude.Uninhabited import Prelude.Nat  %access public@@ -17,12 +18,13 @@ infix 5 \\ infixr 7 ::,++ -||| Linked lists-%elim data List a =-  ||| The empty list+||| Generic lists+%elim data List elem =+  ||| Empty list   Nil |-  ||| Cons cell-  (::) a (List a)+  ||| A non-empty list, consisting of a head element and the rest of+  ||| the list.+  (::) elem (List elem)  -- Name hints for interactive editing %name List xs, ys, zs, ws@@ -42,6 +44,47 @@ isCons (x::xs) = True  --------------------------------------------------------------------------------+-- Decidable Predicates+--------------------------------------------------------------------------------++||| Satisfiable if `xs` is non-empty (e.g., if `xs` is a cons).+data NonEmpty : (xs : List a) -> Type where+    ||| The proof that a cons cell is non-empty+    IsNonEmpty : NonEmpty (x :: xs)++private+nonEmptyNil : NonEmpty [] -> Void+nonEmptyNil IsNonEmpty impossible++||| Decide whether a list is non-empty+nonEmpty : (xs : List a) -> Dec (NonEmpty xs)+nonEmpty [] = No nonEmptyNil+nonEmpty (x :: xs) = Yes IsNonEmpty++||| Satisfiable if `k` is a valid index into `xs`+|||+||| @ k the potential index+||| @ xs the list into which k may be an index+data InBounds : (k : Nat) -> (xs : List a) -> Type where+    ||| Z is a valid index into any cons cell+    InFirst : InBounds Z (x :: xs)+    ||| Valid indices can be extended+    InLater : InBounds k xs -> InBounds (S k) (x :: xs)++instance Uninhabited (InBounds k []) where+    uninhabited InFirst impossible++||| Decide whether `k` is a valid index into `xs`+inBounds : (k : Nat) -> (xs : List a) -> Dec (InBounds k xs)+inBounds k [] = No uninhabited+inBounds Z (x :: xs) = Yes InFirst+inBounds (S k) (x :: xs) with (inBounds k xs)+  inBounds (S k) (x :: xs) | (Yes prf) = Yes (InLater prf)+  inBounds (S k) (x :: xs) | (No contra)+      = No (\p => case p of+                       InLater y => contra y)++-------------------------------------------------------------------------------- -- Length -------------------------------------------------------------------------------- @@ -59,10 +102,9 @@ ||| Find a particular element of a list. ||| ||| @ ok a proof that the index is within bounds-index : (n : Nat) -> (l : List a) -> (ok : lt n (length l) = True) -> a-index Z     (x::xs) p    = x-index (S n) (x::xs) p    = index n xs ?indexTailProof-index _     []      Refl   impossible+index : (n : Nat) -> (xs : List a) -> {auto ok : InBounds n xs} -> a+index Z     (x :: xs) {ok} = x+index (S k) (x :: xs) {ok = InLater p} = index k xs  ||| Attempt to find a particular element of a list. |||@@ -74,8 +116,8 @@  ||| Get the first element of a non-empty list ||| @ ok proof that the list is non-empty-head : (l : List a) -> {auto ok : isCons l = True} -> a-head []      {ok=Refl}   impossible+head : (l : List a) -> {auto ok : NonEmpty l} -> a+head []      {ok=IsNonEmpty} impossible head (x::xs) {ok=p}    = x  ||| Attempt to get the first element of a list. If the list is empty, return@@ -86,8 +128,8 @@  ||| Get the tail of a non-empty list. ||| @ ok proof that the list is non-empty-tail : (l : List a) -> {auto ok : isCons l = True} -> List a-tail []      {ok=Refl}   impossible+tail : (l : List a) -> {auto ok : NonEmpty l} -> List a+tail []      {ok=IsNonEmpty} impossible tail (x::xs) {ok=p}    = xs  ||| Attempt to get the tail of a list.@@ -99,10 +141,10 @@  ||| Retrieve the last element of a non-empty list. ||| @ ok proof that the list is non-empty-last : (l : List a) -> {auto ok : isCons l = True} -> a-last []         {ok=Refl}   impossible+last : (l : List a) -> {auto ok : NonEmpty l} -> a+last []         {ok=IsNonEmpty} impossible last [x]        {ok=p}    = x-last (x::y::ys) {ok=p}    = last (y::ys) {ok=Refl}+last (x::y::ys) {ok=p}    = last (y::ys) {ok=IsNonEmpty}  ||| Attempt to retrieve the last element of a non-empty list. |||@@ -116,10 +158,10 @@  ||| Return all but the last element of a non-empty list. ||| @ ok proof that the list is non-empty-init : (l : List a) -> {auto ok : isCons l = True} -> List a-init []         {ok=Refl}   impossible+init : (l : List a) -> {auto ok : NonEmpty l} -> List a+init []         {ok=IsNonEmpty} impossible init [x]        {ok=p}    = []-init (x::y::ys) {ok=p}    = x :: init (y::ys) {ok=Refl}+init (x::y::ys) {ok=p}    = x :: init (y::ys) {ok=IsNonEmpty}  ||| Attempt to Return all but the last element of a list. |||@@ -129,8 +171,7 @@ init' (x::xs) =   case xs of     []    => Just []-    y::ys =>-      -- XXX: Problem with typechecking a "do" block here+    y::ys =>        case init' $ y::ys of         Nothing => Nothing         Just j  => Just $ x :: j@@ -242,42 +283,38 @@ -- Zips and unzips -------------------------------------------------------------------------------- -||| Combine two lists of the same length elementwise using some function.+||| Combine two lists elementwise using some function. If they are different+||| lengths, the result is truncated to the length of the shorter list. ||| @ f the function to combine elements with ||| @ l the first list ||| @ r the second list-||| @ ok a proof that the lengths of the inputs are equal-zipWith : (f : a -> b -> c) -> (l : List a) -> (r : List b) ->-  (ok : length l = length r) -> List c-zipWith f []      (y::ys) Refl   impossible-zipWith f (x::xs) []      Refl   impossible-zipWith f []      []      p    = []-zipWith f (x::xs) (y::ys) p    = f x y :: (zipWith f xs ys ?zipWithTailProof)+zipWith : (f : a -> b -> c) -> (l : List a) -> (r : List b) -> List c+zipWith f []      (y::ys) = []+zipWith f (x::xs) []      = []+zipWith f []      []      = []+zipWith f (x::xs) (y::ys) = f x y :: zipWith f xs ys -||| Combine three lists of the same length elementwise using some function.+||| Combine three lists elementwise using some function. If they are different+||| lengths, the result is truncated to the length of the shortest list. ||| @ f the function to combine elements with ||| @ x the first list ||| @ y the second list ||| @ z the third list-||| @ ok a proof that the lengths of the first two inputs are equal-||| @ ok' a proof that the lengths of the second and third inputs are equal zipWith3 : (f : a -> b -> c -> d) -> (x : List a) -> (y : List b) ->-  (z : List c) -> (ok : length x = length y) -> (ok' : length y = length z) -> List d-zipWith3 f _       []      (z::zs) p    Refl   impossible-zipWith3 f _       (y::ys) []      p    Refl   impossible-zipWith3 f []      (y::ys) _       Refl q      impossible-zipWith3 f (x::xs) []      _       Refl q      impossible-zipWith3 f []      []      []      p    q    = []-zipWith3 f (x::xs) (y::ys) (z::zs) p    q    =-  f x y z :: (zipWith3 f xs ys zs ?zipWith3TailProof ?zipWith3TailProof')+           (z : List c) -> List d+zipWith3 f _       []      (z::zs) = [] +zipWith3 f _       (y::ys) []      = []+zipWith3 f []      (y::ys) _       = []+zipWith3 f (x::xs) []      _       = []+zipWith3 f []      []      []      = []+zipWith3 f (x::xs) (y::ys) (z::zs) = f x y z :: zipWith3 f xs ys zs  ||| Combine two lists elementwise into pairs-zip : (l : List a) -> (r : List b) -> (length l = length r) -> List (a, b)+zip : (l : List a) -> (r : List b) -> List (a, b) zip = zipWith (\x,y => (x, y))  ||| Combine three lists elementwise into tuples-zip3 : (x : List a) -> (y : List b) -> (z : List c) -> (length x = length y) ->-  (length y = length z) -> List (a, b, c)+zip3 : (x : List a) -> (y : List b) -> (z : List c) -> List (a, b, c) zip3 = zipWith3 (\x,y,z => (x, y, z))  ||| Split a list of pairs into two lists@@ -312,7 +349,7 @@ instance Foldable List where   foldr c n [] = n   foldr c n (x::xs) = c x (foldr c n xs)-  +   foldl f q [] = q   foldl f q (x::xs) = foldl f (f q x) xs @@ -350,8 +387,13 @@     intersperse' sep []      = []     intersperse' sep (y::ys) = sep :: y :: intersperse' sep ys -intercalate : List a -> List (List a) -> List a-intercalate sep l = concat $ intersperse sep l+||| Given a separator list and some more lists, produce a new list by+||| placing the separator between each of the lists.+|||+||| @ sep the separator+||| @ xss the lists between which the separator will be placed+intercalate : (sep : List a) -> (xss : List (List a)) -> List a+intercalate sep xss = concat $ intersperse sep xss  ||| Transposes rows and columns of a list of lists. |||@@ -456,15 +498,20 @@       else         findIndices' (S cnt) p xs +||| Find the index of the first occurrence of an element in a list, using a custom equality test. elemIndexBy : (a -> a -> Bool) -> a -> List a -> Maybe Nat elemIndexBy p e = findIndex $ p e +||| Find the index of the first occurrence of an element in a list,+||| using the default equality test for the type of list elements. elemIndex : Eq a => a -> List a -> Maybe Nat elemIndex = elemIndexBy (==) +||| Find all indices for an element in a list, using a custom equality test. elemIndicesBy : (a -> a -> Bool) -> a -> List a -> List Nat elemIndicesBy p e = findIndices $ p e +||| Find all indices for an element in a list, using the default equality test for the type of list elements. elemIndices : Eq a => a -> List a -> List Nat elemIndices = elemIndicesBy (==) @@ -655,7 +702,12 @@ -- Predicates -------------------------------------------------------------------------------- -isPrefixOfBy : (a -> a -> Bool) -> List a -> List a -> Bool+||| Check whether a list is a prefix of another according to a user-supplied equality test.+|||+||| @ eq the equality comparison+||| @ left the potential prefix+||| @ right the list that may have `left` as its prefix+isPrefixOfBy : (eq : a -> a -> Bool) -> (left, right : List a) -> Bool isPrefixOfBy p [] right        = True isPrefixOfBy p left []         = False isPrefixOfBy p (x::xs) (y::ys) =@@ -691,6 +743,7 @@ -- Sorting -------------------------------------------------------------------------------- +||| Check whether a list is sorted with respect to the default ordering for the type of its elements. sorted : Ord a => List a -> Bool sorted []      = True sorted (x::xs) =@@ -698,6 +751,9 @@     Nil     => True     (y::ys) => x <= y && sorted (y::ys) +||| Merge two sorted lists using an arbitrary comparison+||| predicate. Note that the lists must have been sorted using this+||| predicate already. mergeBy : (a -> a -> Ordering) -> List a -> List a -> List a mergeBy order []      right   = right mergeBy order left    []      = left@@ -706,15 +762,21 @@      then x :: mergeBy order xs (y::ys)      else y :: mergeBy order (x::xs) ys +||| Merge two sorted lists using the default ordering for the type of their elements. merge : Ord a => List a -> List a -> List a merge = mergeBy compare -sort : Ord a => List a -> List a-sort []  = []-sort [x] = [x]-sort xs  = let (x, y) = split xs in-    merge (sort (assert_smaller xs x)) -          (sort (assert_smaller xs y)) -- not structurally smaller, hence assert+||| Sort a list using some arbitrary comparison predicate.+|||+||| @ cmp how to compare elements+||| @ xs the list to sort+sortBy : (cmp : a -> a -> Ordering) -> (xs : List a) -> List a+sortBy cmp []  = []+sortBy cmp [x] = [x]+sortBy cmp xs  = let (x, y) = split xs in+    mergeBy cmp+          (sortBy cmp (assert_smaller xs x))+          (sortBy cmp (assert_smaller xs y)) -- not structurally smaller, hence assert   where     splitRec : List a -> List a -> (List a -> List a) -> (List a, List a)     splitRec (_::_::xs) (y::ys) zs = splitRec xs ys (zs . ((::) y))@@ -723,6 +785,10 @@     split : List a -> (List a, List a)     split xs = splitRec xs xs id +||| Sort a list using the default ordering for the type of its elements.+sort : Ord a => List a -> List a+sort = sortBy compare+ -------------------------------------------------------------------------------- -- Conversions --------------------------------------------------------------------------------@@ -736,6 +802,7 @@ -- Misc -------------------------------------------------------------------------------- +||| Keep the `Just` elements in a list, discarding the `Nothing` elements. catMaybes : List (Maybe a) -> List a catMaybes []      = [] catMaybes (x::xs) =@@ -753,7 +820,7 @@ appendNilRightNeutral []      = Refl appendNilRightNeutral (x::xs) =   let inductiveHypothesis = appendNilRightNeutral xs in-    ?appendNilRightNeutralStepCase+    rewrite inductiveHypothesis in Refl  ||| Appending lists is associative. appendAssociative : (l : List a) -> (c : List a) -> (r : List a) ->@@ -761,7 +828,7 @@ appendAssociative []      c r = Refl appendAssociative (x::xs) c r =   let inductiveHypothesis = appendAssociative xs c r in-    ?appendAssociativeStepCase+    rewrite inductiveHypothesis in Refl  ||| The length of two lists that are appended is the sum of the lengths ||| of the input lists.@@ -770,7 +837,7 @@ lengthAppend []      right = Refl lengthAppend (x::xs) right =   let inductiveHypothesis = lengthAppend xs right in-    ?lengthAppendStepCase+    rewrite inductiveHypothesis in Refl  ||| Mapping a function over a list doesn't change its length. mapPreservesLength : (f : a -> b) -> (l : List a) ->@@ -778,7 +845,7 @@ mapPreservesLength f []      = Refl mapPreservesLength f (x::xs) =   let inductiveHypothesis = mapPreservesLength f xs in-    ?mapPreservesLengthStepCase+    rewrite inductiveHypothesis in Refl  ||| Mapping a function over two lists and appending them is equivalent ||| to appending them and then mapping the function.@@ -787,7 +854,7 @@ mapDistributesOverAppend f []      r = Refl mapDistributesOverAppend f (x::xs) r =   let inductiveHypothesis = mapDistributesOverAppend f xs r in-    ?mapDistributesOverAppendStepCase+    rewrite inductiveHypothesis in Refl  ||| Mapping two functions is the same as mapping their composition. mapFusion : (f : b -> c) -> (g : a -> b) -> (l : List a) ->@@ -795,7 +862,7 @@ mapFusion f g []      = Refl mapFusion f g (x::xs) =   let inductiveHypothesis = mapFusion f g xs in-    ?mapFusionStepCase+    rewrite inductiveHypothesis in Refl  ||| No list contains an element of the empty list by any predicate. hasAnyByNilFalse : (p : a -> a -> Bool) -> (l : List a) ->@@ -803,12 +870,13 @@ hasAnyByNilFalse p []      = Refl hasAnyByNilFalse p (x::xs) =   let inductiveHypothesis = hasAnyByNilFalse p xs in-    ?hasAnyByNilFalseStepCase+    rewrite inductiveHypothesis in Refl  ||| No list contains an element of the empty list. hasAnyNilFalse : Eq a => (l : List a) -> hasAny [] l = False-hasAnyNilFalse l = ?hasAnyNilFalseBody+hasAnyNilFalse l = rewrite (hasAnyByNilFalse (==) l) in Refl +||| Implement foldl using foldr, for a later equality proof. foldlAsFoldr : (b -> a -> b) -> b -> List a -> b foldlAsFoldr f z t = foldr (flip (.) . flip f) id t z @@ -817,81 +885,4 @@ foldlMatchesFoldr : (f : b -> a -> b) -> (q : b) -> (xs : List a) -> foldl f q xs = foldlAsFoldr f q xs foldlMatchesFoldr f q [] = Refl foldlMatchesFoldr f q (x :: xs) = foldlMatchesFoldr f (f q x) xs-------------------------------------------------------------------------------------- Proofs-----------------------------------------------------------------------------------indexTailProof = proof {-  intros;-  rewrite sym p;-  trivial;-}--lengthAppendStepCase = proof {-    intros;-    rewrite inductiveHypothesis;-    trivial;-}--hasAnyNilFalseBody = proof {-    intros;-    rewrite (hasAnyByNilFalse (==) l);-    trivial;-}--hasAnyByNilFalseStepCase = proof {-    intros;-    rewrite inductiveHypothesis;-    trivial;-}--appendNilRightNeutralStepCase = proof {-    intros;-    rewrite inductiveHypothesis;-    trivial;-}--appendAssociativeStepCase = proof {-    intros;-    rewrite inductiveHypothesis;-    trivial;-}--mapFusionStepCase = proof {-    intros;-    rewrite inductiveHypothesis;-    trivial;-}--mapDistributesOverAppendStepCase = proof {-    intros;-    rewrite inductiveHypothesis;-    trivial;-}--mapPreservesLengthStepCase = proof {-    intros;-    rewrite inductiveHypothesis;-    trivial;-}--zipWithTailProof = proof {-    intros;-    rewrite (succInjective (length xs) (length ys) p);-    trivial;-}--zipWith3TailProof = proof {-    intros;-    rewrite (succInjective (length xs) (length ys) p);-    trivial;-}--zipWith3TailProof' = proof {-    intros;-    rewrite (succInjective (length ys) (length zs) q);-    trivial;-} 

@@ -11,9 +11,13 @@ %access public %default total +||| An optional value. This can be used to represent the possibility of+||| failure, where a function may return a value, or not. data Maybe a-    = Nothing-    | Just a+    = ||| No value stored+      Nothing+    | ||| A value of type `a` is stored+      Just a  -------------------------------------------------------------------------------- -- Syntactic tests

@@ -3,9 +3,10 @@ -- Monads and Functors  import Builtins-import Prelude.List+import Prelude.Functor import Prelude.Applicative import Prelude.Basics+import IO  %access public @@ -22,3 +23,20 @@ ||| define `return` and `pure` differently! return : Monad m => a -> m a return = pure++-- Annoyingly, these need to be here, so that we can use them in other+-- Prelude modules other than the top level.++instance Functor (IO' ffi) where+    map f io = io_bind io (\b => io_return (f b))++instance Applicative (IO' ffi) where+    pure x = io_return x+    f <*> a = io_bind f (\f' =>+                io_bind a (\a' =>+                  io_return (f' a')))+++instance Monad (IO' ffi) where+    b >>= k = io_bind b k+

@@ -12,7 +12,8 @@ %access public %default total -||| Unary natural numbers+||| Natural numbers: unbounded, unsigned integers which can be pattern+||| matched. %elim data Nat =   ||| Zero   Z |@@ -213,12 +214,12 @@ instance Cast Integer Nat where   cast = fromInteger -||| A wrapper for Nat that specifies the semigroup and monad instances that use (+)+||| A wrapper for Nat that specifies the semigroup and monad instances that use (*) record Multiplicative where   constructor getMultiplicative   _ : Nat -||| A wrapper for Nat that specifies the semigroup and monad instances that use (*)+||| A wrapper for Nat that specifies the semigroup and monad instances that use (+) record Additive where   constructor getAdditive     _ : Nat@@ -262,6 +263,9 @@ instance Cast Nat Int where   cast = toIntNat +instance Cast Nat Double where+  cast = cast . toIntegerNat+ -------------------------------------------------------------------------------- -- Auxilliary notions --------------------------------------------------------------------------------@@ -403,28 +407,29 @@ plusZeroRightNeutral Z     = Refl plusZeroRightNeutral (S n) =   let inductiveHypothesis = plusZeroRightNeutral n in-    ?plusZeroRightNeutralStepCase+    rewrite inductiveHypothesis in Refl  total plusSuccRightSucc : (left : Nat) -> (right : Nat) ->   S (left + right) = left + (S right) plusSuccRightSucc Z right        = Refl plusSuccRightSucc (S left) right =   let inductiveHypothesis = plusSuccRightSucc left right in-    ?plusSuccRightSuccStepCase+    rewrite inductiveHypothesis in Refl  total plusCommutative : (left : Nat) -> (right : Nat) ->   left + right = right + left-plusCommutative Z        right = ?plusCommutativeBaseCase+plusCommutative Z        right = rewrite plusZeroRightNeutral right in Refl plusCommutative (S left) right =   let inductiveHypothesis = plusCommutative left right in-    ?plusCommutativeStepCase+    rewrite inductiveHypothesis in +      rewrite plusSuccRightSucc right left in Refl  total plusAssociative : (left : Nat) -> (centre : Nat) -> (right : Nat) ->   left + (centre + right) = (left + centre) + right plusAssociative Z        centre right = Refl plusAssociative (S left) centre right =   let inductiveHypothesis = plusAssociative left centre right in-    ?plusAssociativeStepCase+    rewrite inductiveHypothesis in Refl  total plusConstantRight : (left : Nat) -> (right : Nat) -> (c : Nat) ->   (p : left = right) -> left + c = right + c@@ -439,24 +444,26 @@  total plusLeftCancel : (left : Nat) -> (right : Nat) -> (right' : Nat) ->   (p : left + right = left + right') -> right = right'-plusLeftCancel Z        right right' p = ?plusLeftCancelBaseCase+plusLeftCancel Z        right right' p = p plusLeftCancel (S left) right right' p =   let inductiveHypothesis = plusLeftCancel left right right' in-    ?plusLeftCancelStepCase+    inductiveHypothesis (succInjective _ _ p)   total plusRightCancel : (left : Nat) -> (left' : Nat) -> (right : Nat) ->   (p : left + right = left' + right) -> left = left'-plusRightCancel left left' Z         p = ?plusRightCancelBaseCase+plusRightCancel left left' Z         p = rewrite sym (plusZeroRightNeutral left) in+                                         rewrite sym (plusZeroRightNeutral left') in+                                                 p  plusRightCancel left left' (S right) p =-  let inductiveHypothesis = plusRightCancel left left' right in-    ?plusRightCancelStepCase+  plusRightCancel left left' right +    (succInjective _ _ (rewrite plusSuccRightSucc left right in +                        rewrite plusSuccRightSucc left' right in p))  total plusLeftLeftRightZero : (left : Nat) -> (right : Nat) ->   (p : left + right = left) -> right = Z-plusLeftLeftRightZero Z        right p = ?plusLeftLeftRightZeroBaseCase+plusLeftLeftRightZero Z        right p = p  plusLeftLeftRightZero (S left) right p =-  let inductiveHypothesis = plusLeftLeftRightZero left right in-    ?plusLeftLeftRightZeroStepCase+  plusLeftLeftRightZero left right (succInjective _ _ p)  -- Mult total multZeroLeftZero : (right : Nat) -> Z * right = Z@@ -464,16 +471,18 @@  total multZeroRightZero : (left : Nat) -> left * Z = Z multZeroRightZero Z        = Refl-multZeroRightZero (S left) =-  let inductiveHypothesis = multZeroRightZero left in-    ?multZeroRightZeroStepCase+multZeroRightZero (S left) = multZeroRightZero left  total multRightSuccPlus : (left : Nat) -> (right : Nat) ->   left * (S right) = left + (left * right) multRightSuccPlus Z        right = Refl multRightSuccPlus (S left) right =   let inductiveHypothesis = multRightSuccPlus left right in-    ?multRightSuccPlusStepCase+    rewrite inductiveHypothesis in +    rewrite plusAssociative left right (mult left right) in+    rewrite plusAssociative right left (mult left right) in+    rewrite plusCommutative right left in+            Refl  total multLeftSuccPlus : (left : Nat) -> (right : Nat) ->   (S left) * right = right + (left * right)@@ -481,43 +490,57 @@  total multCommutative : (left : Nat) -> (right : Nat) ->   left * right = right * left-multCommutative Z right        = ?multCommutativeBaseCase+multCommutative Z right        = rewrite multZeroRightZero right in Refl  multCommutative (S left) right =   let inductiveHypothesis = multCommutative left right in-    ?multCommutativeStepCase+      rewrite inductiveHypothesis in+      rewrite multRightSuccPlus right left in +              Refl  total multDistributesOverPlusRight : (left : Nat) -> (centre : Nat) -> (right : Nat) ->   left * (centre + right) = (left * centre) + (left * right) multDistributesOverPlusRight Z        centre right = Refl multDistributesOverPlusRight (S left) centre right =   let inductiveHypothesis = multDistributesOverPlusRight left centre right in-    ?multDistributesOverPlusRightStepCase+    rewrite inductiveHypothesis in +    rewrite plusAssociative (plus centre (mult left centre)) right (mult left right) in+    rewrite sym (plusAssociative centre (mult left centre) right) in+    rewrite plusCommutative (mult left centre) right in+    rewrite plusAssociative centre right (mult left centre) in+    rewrite plusAssociative (plus centre right) (mult left centre) (mult left right) in+            Refl  total multDistributesOverPlusLeft : (left : Nat) -> (centre : Nat) -> (right : Nat) ->   (left + centre) * right = (left * right) + (centre * right) multDistributesOverPlusLeft Z        centre right = Refl multDistributesOverPlusLeft (S left) centre right =   let inductiveHypothesis = multDistributesOverPlusLeft left centre right in-    ?multDistributesOverPlusLeftStepCase+    rewrite inductiveHypothesis in+    rewrite plusAssociative right (mult left right) (mult centre right) in+            Refl  total multAssociative : (left : Nat) -> (centre : Nat) -> (right : Nat) ->   left * (centre * right) = (left * centre) * right multAssociative Z        centre right = Refl multAssociative (S left) centre right =   let inductiveHypothesis = multAssociative left centre right in-    ?multAssociativeStepCase+    rewrite inductiveHypothesis in +    rewrite multDistributesOverPlusLeft centre (mult left centre) right in+            Refl  total multOneLeftNeutral : (right : Nat) -> 1 * right = right multOneLeftNeutral Z         = Refl multOneLeftNeutral (S right) =   let inductiveHypothesis = multOneLeftNeutral right in-    ?multOneLeftNeutralStepCase+    rewrite inductiveHypothesis in+            Refl  total multOneRightNeutral : (left : Nat) -> left * 1 = left multOneRightNeutral Z        = Refl multOneRightNeutral (S left) =   let inductiveHypothesis = multOneRightNeutral left in-    ?multOneRightNeutralStepCase+    rewrite inductiveHypothesis in+            Refl  -- Minus total minusSuccSucc : (left : Nat) -> (right : Nat) ->@@ -554,29 +577,37 @@ minusMinusMinusPlus Z        (S centre) right = Refl minusMinusMinusPlus (S left) (S centre) right =   let inductiveHypothesis = minusMinusMinusPlus left centre right in-    ?minusMinusMinusPlusStepCase+    rewrite inductiveHypothesis in+            Refl  total plusMinusLeftCancel : (left : Nat) -> (right : Nat) -> (right' : Nat) ->   (left + right) - (left + right') = right - right' plusMinusLeftCancel Z right right'        = Refl plusMinusLeftCancel (S left) right right' =   let inductiveHypothesis = plusMinusLeftCancel left right right' in-    ?plusMinusLeftCancelStepCase+    rewrite inductiveHypothesis in+            Refl  total multDistributesOverMinusLeft : (left : Nat) -> (centre : Nat) -> (right : Nat) ->   (left - centre) * right = (left * right) - (centre * right) multDistributesOverMinusLeft Z        Z          right = Refl multDistributesOverMinusLeft (S left) Z          right =-  ?multDistributesOverMinusLeftBaseCase+    rewrite (minusZeroRight (plus right (mult left right))) in Refl multDistributesOverMinusLeft Z        (S centre) right = Refl multDistributesOverMinusLeft (S left) (S centre) right =   let inductiveHypothesis = multDistributesOverMinusLeft left centre right in-    ?multDistributesOverMinusLeftStepCase+    rewrite inductiveHypothesis in+    rewrite plusMinusLeftCancel right (mult left right) (mult centre right) in+            Refl  total multDistributesOverMinusRight : (left : Nat) -> (centre : Nat) -> (right : Nat) ->   left * (centre - right) = (left * centre) - (left * right) multDistributesOverMinusRight left centre right =-  ?multDistributesOverMinusRightBody+    rewrite multCommutative left (minus centre right) in+    rewrite multDistributesOverMinusLeft centre right left in+    rewrite multCommutative centre left in+    rewrite multCommutative right left in+            Refl  -- Power total powerSuccPowerLeft : (base : Nat) -> (exp : Nat) -> power base (S exp) =@@ -585,10 +616,13 @@  total multPowerPowerPlus : (base : Nat) -> (exp : Nat) -> (exp' : Nat) ->   (power base exp) * (power base exp') = power base (exp + exp')-multPowerPowerPlus base Z       exp' = ?multPowerPowerPlusBaseCase+multPowerPowerPlus base Z       exp' = +    rewrite sym (plusZeroRightNeutral (power base exp')) in Refl multPowerPowerPlus base (S exp) exp' =   let inductiveHypothesis = multPowerPowerPlus base exp exp' in-    ?multPowerPowerPlusStepCase+    rewrite sym inductiveHypothesis in+    rewrite sym (multAssociative base (power base exp) (power base exp')) in+            Refl  total powerZeroOne : (base : Nat) -> power base 0 = S Z powerZeroOne base = Refl@@ -597,26 +631,27 @@ powerOneNeutral Z        = Refl powerOneNeutral (S base) =   let inductiveHypothesis = powerOneNeutral base in-    ?powerOneNeutralStepCase+    rewrite inductiveHypothesis in Refl  total powerOneSuccOne : (exp : Nat) -> power 1 exp = S Z powerOneSuccOne Z       = Refl powerOneSuccOne (S exp) =   let inductiveHypothesis = powerOneSuccOne exp in-    ?powerOneSuccOneStepCase+    rewrite inductiveHypothesis in Refl  total powerSuccSuccMult : (base : Nat) -> power base 2 = mult base base powerSuccSuccMult Z        = Refl-powerSuccSuccMult (S base) =-  let inductiveHypothesis = powerSuccSuccMult base in-    ?powerSuccSuccMultStepCase+powerSuccSuccMult (S base) = rewrite multOneRightNeutral base in Refl  total powerPowerMultPower : (base : Nat) -> (exp : Nat) -> (exp' : Nat) ->   power (power base exp) exp' = power base (exp * exp')-powerPowerMultPower base exp Z        = ?powerPowerMultPowerBaseCase+powerPowerMultPower base exp Z        = rewrite multZeroRightZero exp in Refl powerPowerMultPower base exp (S exp') =   let inductiveHypothesis = powerPowerMultPower base exp exp' in-    ?powerPowerMultPowerStepCase+    rewrite inductiveHypothesis in +    rewrite multRightSuccPlus exp exp' in+    rewrite sym (multPowerPowerPlus base exp (mult exp exp')) in+            Refl  -- Pred total predSucc : (n : Nat) -> pred (S n) = n@@ -626,11 +661,10 @@   left - (S right) = pred (left - right) minusSuccPred Z        right = Refl minusSuccPred (S left) Z =-  let inductiveHypothesis = minusSuccPred left Z in-    ?minusSuccPredStepCase+    rewrite minusZeroRight left in Refl  minusSuccPred (S left) (S right) =   let inductiveHypothesis = minusSuccPred left right in-    ?minusSuccPredStepCase'+    rewrite inductiveHypothesis in Refl  -- ifThenElse total ifThenElseSuccSucc : (cond : Bool) -> (t : Nat) -> (f : Nat) ->@@ -713,9 +747,7 @@ minimumSuccSucc Z        Z         = Refl minimumSuccSucc (S left) Z         = Refl minimumSuccSucc Z        (S right) = Refl-minimumSuccSucc (S left) (S right) =-  let inductiveHypothesis = minimumSuccSucc left right in-    ?minimumSuccSuccStepCase+minimumSuccSucc (S left) (S right) = Refl  total maximumZeroNRight : (right : Nat) -> maximum Z right = right maximumZeroNRight Z         = Refl@@ -730,9 +762,7 @@ maximumSuccSucc Z        Z         = Refl maximumSuccSucc (S left) Z         = Refl maximumSuccSucc Z        (S right) = Refl-maximumSuccSucc (S left) (S right) =-  let inductiveHypothesis = maximumSuccSucc left right in-    ?maximumSuccSuccStepCase+maximumSuccSucc (S left) (S right) = Refl  total sucMaxL : (l : Nat) -> maximum (S l) l = (S l) sucMaxL Z = Refl@@ -750,252 +780,3 @@ sucMinR Z = Refl sucMinR (S l) = cong (sucMinR l) ------------------------------------------------------------------------------------ Proofs-----------------------------------------------------------------------------------powerPowerMultPowerStepCase = proof {-    intros;-    rewrite sym inductiveHypothesis;-    rewrite sym (multRightSuccPlus exp exp');-    rewrite (multPowerPowerPlus base exp (mult exp exp'));-    trivial;-}--powerPowerMultPowerBaseCase = proof {-    intros;-    rewrite sym (multZeroRightZero exp);-    trivial;-}--powerSuccSuccMultStepCase = proof {-    intros;-    rewrite (multOneRightNeutral base);-    rewrite sym (multOneRightNeutral base);-    trivial;-}--powerOneSuccOneStepCase = proof {-    intros;-    rewrite inductiveHypothesis;-    rewrite sym (plusZeroRightNeutral (power (S Z) exp));-    trivial;-}--powerOneNeutralStepCase = proof {-    intros;-    rewrite inductiveHypothesis;-    trivial;-}--multAssociativeStepCase = proof {-    intros;-    rewrite sym (multDistributesOverPlusLeft centre (mult left centre) right);-    rewrite inductiveHypothesis;-    trivial;-}--minusSuccPredStepCase' = proof {-    intros;-    rewrite sym inductiveHypothesis;-    trivial;-}--minusSuccPredStepCase = proof {-    intros;-    rewrite (minusZeroRight left);-    trivial;-}--multPowerPowerPlusStepCase = proof {-    intros;-    rewrite inductiveHypothesis;-    rewrite (multAssociative base (power base exp) (power base exp'));-    trivial;-}--multPowerPowerPlusBaseCase = proof {-    intros;-    rewrite (plusZeroRightNeutral (power base exp'));-    trivial;-}--multOneRightNeutralStepCase = proof {-    intros;-    rewrite inductiveHypothesis;-    trivial;-}--multOneLeftNeutralStepCase = proof {-    intros;-    rewrite (plusZeroRightNeutral right);-    trivial;-}--multDistributesOverPlusLeftStepCase = proof {-    intros;-    rewrite sym inductiveHypothesis;-    rewrite sym (plusAssociative right (mult left right) (mult centre right));-    trivial;-}--multDistributesOverPlusRightStepCase = proof {-    intros;-    rewrite sym inductiveHypothesis;-    rewrite sym (plusAssociative (plus centre (mult left centre)) right (mult left right));-    rewrite (plusAssociative centre (mult left centre) right);-    rewrite sym (plusCommutative (mult left centre) right);-    rewrite sym (plusAssociative centre right (mult left centre));-    rewrite sym (plusAssociative (plus centre right) (mult left centre) (mult left right));-    trivial;-}--multCommutativeStepCase = proof {-    intros;-    rewrite sym (multRightSuccPlus right left);-    rewrite inductiveHypothesis;-    trivial;-}--multCommutativeBaseCase = proof {-    intros;-    rewrite (multZeroRightZero right);-    trivial;-}--multRightSuccPlusStepCase = proof {-    intros;-    rewrite inductiveHypothesis;-    rewrite sym inductiveHypothesis;-    rewrite sym (plusAssociative right left (mult left right));-    rewrite sym (plusCommutative right left);-    rewrite (plusAssociative left right (mult left right));-    trivial;-}--multZeroRightZeroStepCase = proof {-    intros;-    rewrite inductiveHypothesis;-    trivial;-}--plusAssociativeStepCase = proof {-    intros;-    rewrite inductiveHypothesis;-    trivial;-}--plusCommutativeStepCase = proof {-    intros;-    rewrite (plusSuccRightSucc right left);-    rewrite inductiveHypothesis;-    trivial;-}--plusSuccRightSuccStepCase = proof {-    intros;-    rewrite inductiveHypothesis;-    trivial;-}--plusCommutativeBaseCase = proof {-    intros;-    rewrite sym (plusZeroRightNeutral right);-    trivial;-}--plusZeroRightNeutralStepCase = proof {-    intros;-    rewrite inductiveHypothesis;-    trivial;-}--maximumSuccSuccStepCase = proof {-    intros;-    rewrite sym (ifThenElseSuccSucc (lte left right) (S right) (S left));-    trivial;-}--minimumSuccSuccStepCase = proof {-    intros;-    rewrite (ifThenElseSuccSucc (lte left right) (S left) (S right));-    trivial;-}--multDistributesOverMinusRightBody = proof {-    intros;-    rewrite sym (multCommutative left (minus centre right));-    rewrite sym (multDistributesOverMinusLeft centre right left);-    rewrite sym (multCommutative centre left);-    rewrite sym (multCommutative right left);-    trivial;-}--multDistributesOverMinusLeftStepCase = proof {-    intros;-    rewrite sym (plusMinusLeftCancel right (mult left right) (mult centre right));-    trivial;-}--multDistributesOverMinusLeftBaseCase = proof {-    intros;-    rewrite (minusZeroRight (plus right (mult left right)));-    trivial;-}--plusMinusLeftCancelStepCase = proof {-    intros;-    rewrite inductiveHypothesis;-    trivial;-}--minusMinusMinusPlusStepCase = proof {-    intros;-    rewrite inductiveHypothesis;-    trivial;-}--plusLeftLeftRightZeroBaseCase = proof {-    intros;-    rewrite p;-    trivial;-}--plusLeftLeftRightZeroStepCase = proof {-    intros;-    refine inductiveHypothesis;-    let p' = succInjective (plus left right) left p;-    rewrite p';-    trivial;-}--plusRightCancelStepCase = proof {-    intros;-    refine inductiveHypothesis;-    refine succInjective _ _ ?;-    rewrite sym (plusSuccRightSucc left right);-    rewrite sym (plusSuccRightSucc left' right);-    rewrite p;-    trivial;-}--plusRightCancelBaseCase = proof {-    intros;-    rewrite (plusZeroRightNeutral left);-    rewrite (plusZeroRightNeutral left');-    rewrite p;-    trivial;-}--plusLeftCancelStepCase = proof {-    intros;-    let injectiveProof = succInjective (plus left right) (plus left right') p;-    rewrite (inductiveHypothesis injectiveProof);-    trivial;-}--plusLeftCancelBaseCase = proof {-    intros;-    rewrite p;-    trivial;-}

@@ -0,0 +1,190 @@+module Prelude.Show++import Builtins++import Prelude.Basics+import Prelude.Bits+import Prelude.Bool+import Prelude.Cast+import Prelude.Chars+import Prelude.Classes+import Prelude.List+import Prelude.Maybe+import Prelude.Nat+import Prelude.Strings++%default total++||| The precedence of an Idris operator or syntactic context.+data Prec = Open | Eq | Dollar | Backtick | User Nat | PrefixMinus | App++||| Gives the constructor index of the Prec as a helper for writing instances.+precCon : Prec -> Integer+precCon Open        = 0+precCon Eq          = 1+precCon Dollar      = 2+precCon Backtick    = 3+precCon (User n)    = 4+precCon PrefixMinus = 5+precCon App         = 6++instance Eq Prec where+  (==) (User m) (User n) = m == n+  (==) x        y        = precCon x == precCon y++instance Ord Prec where+  compare (User m) (User n) = compare m n+  compare x        y        = compare (precCon x) (precCon y)++||| Things that have a canonical `String` representation.+class Show a where+  ||| Convert a value to its `String` representation.+  |||+  ||| @ a the value to convert+  partial+  show : (x : a) -> String+  show = showPrec Open++  ||| Convert a value to its `String` representation in a certain precedence+  ||| context.+  |||+  ||| A value should produce parentheses around itself if and only if the given+  ||| precedence context is greater than or equal to the precedence of the+  ||| outermost operation represented in the produced `String`. *This is+  ||| different from Haskell*, which requires it to be strictly greater. `Open`+  ||| should thus always produce *no* outermost parens, `App` should always+  ||| produce outermost parens except on atomic values and those that provide+  ||| their own bracketing, like `Pair` and `List`.+  |||+  ||| @ d the precedence context.+  ||| @ a the value to convert+  partial+  showPrec : (d : Prec) -> (x : a) -> String+  showPrec _ = show++||| Surround a `String` with parentheses depending on a condition.+|||+||| @ b whether to add parentheses+showParens : (b : Bool) -> String -> String+showParens False s = s+showParens True  s = "(" ++ s ++ ")"++||| A helper for the common case of showing a non-infix constructor with at+||| least one argument, for use with `showArg`.+|||+||| Apply `showCon` to the precedence context, the constructor name, and the+||| args shown with `showArg` and concatenated. Example:+||| ```+||| data Ann a = MkAnn String a+|||+||| instance Show a => Show (Ann a) where+|||   showPrec d (MkAnn s x) = showCon d "MkAnn" $ showArg s ++ showArg x+||| ```+showCon : (d : Prec) -> (conName : String) -> (shownArgs : String) -> String+showCon d conName shownArgs = showParens (d >= App) $ conName ++ shownArgs++||| A helper for the common case of showing a non-infix constructor with at+||| least one argument, for use with `showCon`.+|||+||| This adds a space to the front so the results can be directly+||| concatenated. See `showCon` for details and an example.+showArg : Show a => (x : a) -> String+showArg x = " " ++ showPrec App x++firstCharIs : (Char -> Bool) -> String -> Bool+firstCharIs p s with (strM s)+  firstCharIs p ""             | StrNil = False+  firstCharIs p (strCons c cs) | StrCons c cs = p c++primNumShow : (a -> String) -> Prec -> a -> String+primNumShow f d x = let str = f x in showParens (d >= PrefixMinus && firstCharIs (== '-') str) str++instance Show Int where+  showPrec = primNumShow prim__toStrInt++instance Show Integer where+  showPrec = primNumShow prim__toStrBigInt++instance Show Double where+  showPrec = primNumShow prim__floatToStr++protectEsc : (Char -> Bool) -> String -> String -> String+protectEsc p f s = f ++ (if firstCharIs p s then "\\&" else "") ++ s++showLitChar : Char -> String -> String+showLitChar '\a'   = ("\\a" ++)+showLitChar '\b'   = ("\\b" ++)+showLitChar '\f'   = ("\\f" ++)+showLitChar '\n'   = ("\\n" ++)+showLitChar '\r'   = ("\\r" ++)+showLitChar '\t'   = ("\\t" ++)+showLitChar '\v'   = ("\\v" ++)+showLitChar '\SO'  = protectEsc (== 'H') "\\SO"+showLitChar '\DEL' = ("\\DEL" ++)+showLitChar '\\'   = ("\\\\" ++)+showLitChar c      = case getAt (cast (cast {to=Int} c)) asciiTab of+                          Just k => strCons '\\' . (k ++)+                          Nothing => if (c > '\DEL')+                                        then strCons '\\' . protectEsc isDigit (show (cast {to=Int} c))+                                        else strCons c+  where asciiTab : List String+        asciiTab = ["NUL", "SOH", "STX", "ETX", "EOT", "ENQ", "ACK", "BEL",+                    "BS",  "HT",  "LF",  "VT",  "FF",  "CR",  "SO",  "SI",+                    "DLE", "DC1", "DC2", "DC3", "DC4", "NAK", "SYN", "ETB",+                    "CAN", "EM",  "SUB", "ESC", "FS",  "GS",  "RS",  "US"]++        getAt : Nat -> List String -> Maybe String+        getAt Z     (x :: xs) = Just x+        getAt (S k) (x :: xs) = getAt k xs+        getAt _     []        = Nothing++showLitString : List Char -> String -> String+showLitString []        = id+showLitString ('"'::cs) = ("\\\"" ++) . showLitString cs+showLitString (c  ::cs) = showLitChar c . showLitString cs++instance Show Char where+  show '\'' = "'\\''"+  show c    = strCons '\'' (showLitChar c "'")++instance Show String where+  show cs = strCons '"' (showLitString (cast cs) "\"")++instance Show Nat where+    show n = show (the Integer (cast n))++instance Show Bool where+    show True = "True"+    show False = "False"++instance Show () where+  show () = "()"++instance Show Bits8 where+  show b = b8ToString b++instance Show Bits16 where+  show b = b16ToString b++instance Show Bits32 where+  show b = b32ToString b++instance Show Bits64 where+  show b = b64ToString b++instance (Show a, Show b) => Show (a, b) where+    show (x, y) = "(" ++ show x ++ ", " ++ show y ++ ")"++instance Show a => Show (List a) where+    show xs = "[" ++ show' "" xs ++ "]" where+        show' acc []        = acc+        show' acc [x]       = acc ++ show x+        show' acc (x :: xs) = show' (acc ++ show x ++ ", ") xs++instance Show a => Show (Maybe a) where+  showPrec d Nothing  = "Nothing"+  showPrec d (Just x) = showCon d "Just" $ showArg x++instance (Show a, {y : a} -> Show (p y)) => Show (Sigma a p) where+    show (y ** prf) = "(" ++ show y ++ " ** " ++ show prf ++ ")"+

@@ -1,6 +1,7 @@ module Prelude.Strings  import Builtins+import IO  import Prelude.Algebra import Prelude.Basics@@ -13,8 +14,18 @@ import Prelude.Functor import Prelude.List import Prelude.Nat+import Prelude.Monad import Decidable.Equality +partial+foldr1 : (a -> a -> a) -> List a -> a+foldr1 _ [x] = x+foldr1 f (x::xs) = f x (foldr1 f xs)++partial+foldl1 : (a -> a -> a) -> List a -> a+foldl1 f (x::xs) = foldl f x xs+ ||| Appends two strings together. ||| ||| ```idris example@@ -247,15 +258,6 @@ lines : String -> List String lines s = map pack $ lines' $ unpack s -partial-foldr1 : (a -> a -> a) -> List a -> a-foldr1 _ [x] = x-foldr1 f (x::xs) = f x (foldr1 f xs)--partial-foldl1 : (a -> a -> a) -> List a -> a-foldl1 f (x::xs) = foldl f x xs- ||| Joins the character lists by spaces into a single character list. ||| ||| ```idris example@@ -263,12 +265,11 @@ ||| ``` unwords' : List (List Char) -> List Char unwords' [] = []-unwords' ws = assert_total (foldr1 addSpace ws)-        where-            addSpace : List Char -> List Char -> List Char-            addSpace w s = w ++ (' ' :: s)+unwords' ws = assert_total (foldr1 addSpace ws) where+  addSpace : List Char -> List Char -> List Char+  addSpace w s = w ++ (' ' :: s) -||| Joins the strings by spaces into a single string. +||| Joins the strings by spaces into a single string. ||| ||| ```idris example ||| unwords ["A", "BC", "D", "E"]@@ -276,6 +277,25 @@ unwords : List String -> String unwords = pack . unwords' . map unpack +||| Joins the character lists by newlines into a single character list.+|||+||| ```idris example+||| unlines' [['l','i','n','e'], ['l','i','n','e','2'], ['l','n','3'], ['D']]+||| ```+unlines' : List (List Char) -> List Char+unlines' [] = []+unlines' ls = assert_total (foldr1 addLine ls) where+  addLine : List Char -> List Char -> List Char+  addLine l s = l ++ ('\n' :: s)++||| Joins the strings by newlines into a single string.+|||+||| ```idris example+||| unlines ["line", "line2", "ln3", "D"]+||| ```+unlines : List String -> String+unlines = pack . unlines' . map unpack+ ||| Returns the length of the string. ||| ||| ```idris example@@ -287,6 +307,14 @@ length : String -> Nat length = fromInteger . prim__zextInt_BigInt . prim_lenString +||| Returns a substring of a given string+||| @index The (zero based) index of the string to extract. If this is+||| beyond the end of the String, the function returns the empty string.+||| @len The desired length of the substring. Truncated if this exceeds+||| the length of the input.+substr : (index : Nat) -> (len : Nat) -> String -> String+substr i len = pack . List.take len . drop i . unpack+ ||| Lowercases all characters in the string. ||| ||| ```idris example@@ -321,3 +349,16 @@  isInfixOf : String -> String -> Bool isInfixOf a b = isInfixOf (unpack a) (unpack b)++||| Check if a foreign pointer is null+partial+nullPtr : Ptr -> IO Bool+nullPtr p = do ok <- foreign FFI_C "isNull" (Ptr -> IO Int) p+               return (ok /= 0)++||| Check if a supposed string was actually a null pointer+partial+nullStr : String -> IO Bool+nullStr p = do ok <- foreign FFI_C "isNull" (String -> IO Int) p+               return (ok /= 0)+

@@ -6,9 +6,10 @@           Prelude.Algebra, Prelude.Basics, Prelude.Bool, Prelude.Cast,           Prelude.Classes, Prelude.Nat, Prelude.List,           Prelude.Maybe, Prelude.Monad, Prelude.Applicative, Prelude.Either,-          Prelude.Strings, Prelude.Chars, Prelude.Functor,+          Prelude.Strings, Prelude.Chars, Prelude.Show, Prelude.Functor,           Prelude.Foldable, Prelude.Traversable, Prelude.Bits, Prelude.Stream,           Prelude.Uninhabited, Prelude.Pairs, Prelude.Providers,+          Prelude.Interactive, Prelude.File,            Language.Reflection, Language.Reflection.Errors, Language.Reflection.Elab, 

@@ -26,6 +26,7 @@      VAL* valstack = malloc(stack_size * sizeof(VAL)); +    vm->active = 1;     vm->valstack = valstack;     vm->valstack_top = valstack;     vm->valstack_base = valstack;@@ -104,7 +105,12 @@     pthread_mutex_destroy(&(vm -> inbox_block));     pthread_cond_destroy(&(vm -> inbox_waiting)); #endif-    free(vm);+    // free(vm); +    // Set the VM as inactive, so that if any message gets sent to it+    // it will not get there, rather than crash the entire system.+    // (TODO: We really need to be cleverer than this if we're going to+    // write programs than create lots of threads...)+    vm->active = 0;      STATS_LEAVE_EXIT(stats)     return stats;@@ -464,7 +470,7 @@     Closure* cl = allocate(sizeof(Closure) + sizeof(char)*32, 0);     SETTY(cl, STRING);     cl -> info.str = (char*)cl + sizeof(Closure);-    sprintf(cl -> info.str, "%g", GETFLOAT(i));+    snprintf(cl -> info.str, 32, "%.16g", GETFLOAT(i));     return cl; } @@ -738,7 +744,7 @@ }  // Add a message to another VM's message queue-void idris_sendMessage(VM* sender, VM* dest, VAL msg) {+int idris_sendMessage(VM* sender, VM* dest, VAL msg) {     // FIXME: If GC kicks in in the middle of the copy, we're in trouble.     // Probably best check there is enough room in advance. (How?) @@ -749,6 +755,8 @@     // So: we try to copy, if a collection happens, we do the copy again     // under the assumption there's enough space this time. +    if (dest->active == 0) { return 0; } // No VM to send to+     int gcs = dest->stats.collections;     pthread_mutex_lock(&dest->alloc_lock);     VAL dmsg = copyTo(dest, msg);@@ -784,6 +792,7 @@      pthread_mutex_unlock(&(dest->inbox_lock)); //    printf("Sending [unlock]...\n");+    return 1; }  VM* idris_checkMessages(VM* vm) {@@ -800,6 +809,29 @@     }     return 0; }++VM* idris_checkMessagesTimeout(VM* vm, int delay) {+    VM* sender = idris_checkMessagesFrom(vm, NULL);+    if (sender != NULL) {+        return sender;+    }++    struct timespec timeout;+    int status;++    // Wait either for a timeout or until we get a signal that a message+    // has arrived.+    pthread_mutex_lock(&vm->inbox_block);+    timeout.tv_sec = time (NULL) + delay;+    timeout.tv_nsec = 0;+    status = pthread_cond_timedwait(&vm->inbox_waiting, &vm->inbox_block,+                               &timeout);+    (void)(status); //don't emit 'unused' warning+    pthread_mutex_unlock(&vm->inbox_block);++    return idris_checkMessagesFrom(vm, NULL);+}+  Msg* idris_getMessageFrom(VM* vm, VM* sender) {     Msg* msg;

@@ -78,6 +78,10 @@ typedef struct Msg_t Msg;  struct VM_t {+    int active; // 0 if no longer running; keep for message passing+                // TODO: If we're going to have lots of concurrent threads,+                // we really need to be cleverer than this!+     VAL* valstack;     VAL* valstack_top;     VAL* valstack_base;@@ -253,12 +257,14 @@ VAL copyTo(VM* newVM, VAL x);  // Add a message to another VM's message queue-void idris_sendMessage(VM* sender, VM* dest, VAL msg);+int idris_sendMessage(VM* sender, VM* dest, VAL msg); // Check whether there are any messages in the queue and return PID of // sender if so (null if not) VM* idris_checkMessages(VM* vm); // Check whether there are any messages in the queue VM* idris_checkMessagesFrom(VM* vm, VM* sender);+// Check whether there are any messages in the queue, and wait if not+VM* idris_checkMessagesTimeout(VM* vm, int timeout); // block until there is a message in the queue Msg* idris_recvMessage(VM* vm); // block until there is a message in the queue

@@ -1,5 +1,6 @@ #include "idris_stdfgn.h" #include "idris_rts.h"+#include "idris_gmp.h" #include "idris_gc.h" #include <sys/select.h> #include <fcntl.h>@@ -80,9 +81,9 @@     return *(environ + i); } -int idris_time() {+VAL idris_time() {     time_t t = time(NULL);-    return (int)t;+    return MKBIGI(t); }  void idris_forceGC(void* vm) {

@@ -1,6 +1,8 @@ #ifndef _IDRISSTDFGN_H #define _IDRISSTDFGN_H +#include "idris_rts.h"+ // A collection of useful standard functions to be used by the prelude.  void putStr(char* str);@@ -22,7 +24,7 @@  char* getEnvPair(int i); -int idris_time();+VAL idris_time();  void idris_forceGC(); 

@@ -72,9 +72,9 @@     return *(environ + i); } -int idris_time() {+VAL idris_time() {     time_t t = time(NULL);-    return (int)t;+    return MKBIGI(t); }  void idris_forceGC(void* vm) {

@@ -64,7 +64,7 @@                      (if (exec == Executable) then mprog else hi)          case exec of            MavenProject -> putStrLn ("FAILURE: output type not supported")-           Raw -> writeFile out cout+           Raw -> writeSource out cout            _ -> do              (tmpn, tmph) <- tempfile              hPutStr tmph cout@@ -570,6 +570,10 @@ doOp v (LExternal se) [] | se == sUN "prim__stderr" = v ++ "MKPTR(vm, stderr)"  doOp v (LExternal nul) [] | nul == sUN "prim__null" = v ++ "MKPTR(vm, NULL)"+doOp v (LExternal eqp) [x, y] | eqp == sUN "prim__eqPtr" +    = v ++ "MKINT((i_int)(GETPTR(" ++ creg x ++ ") == GETPTR(" ++ creg y ++ ")))"+doOp v (LExternal eqp) [x, y] | eqp == sUN "prim__eqManagedPtr" +    = v ++ "MKINT((i_int)(GETMPTR(" ++ creg x ++ ") == GETMPTR(" ++ creg y ++ ")))" doOp v (LExternal rp) [p, i] | rp == sUN "prim__registerPtr"     = v ++ "MKMPTR(vm, GETPTR(" ++ creg p ++ "), GETINT(" ++ creg i ++ "))" 

@@ -132,12 +132,12 @@                 ++ idrRuntime                 ++ tgtRuntime                 )-  TIO.writeFile filename (  T.pack runtime-                         `T.append` T.concat (map compileJS opt)-                         `T.append` T.concat (map compileJS cons)-                         `T.append` main-                         `T.append` invokeMain-                         )+  writeSourceText filename (  T.pack runtime+                           `T.append` T.concat (map compileJS opt)+                           `T.append` T.concat (map compileJS cons)+                           `T.append` main+                           `T.append` invokeMain+                           )   setPermissions filename (emptyPermissions { readable   = True                                             , executable = target == Node                                             , writable   = True@@ -250,12 +250,7 @@               , JSApp (                   JSIdent (translateName (sMN 0 "runMain"))                 ) [JSNew "i$POINTER" [JSNum (JSInt 0)]]-              , JSWhile (JSProj jsCALLSTACK "length") (-                  JSSeq [ JSAlloc "func" (Just jsPOP)-                        , JSAlloc "args" (Just jsPOP)-                        , JSApp (JSProj (JSIdent "func") "apply") [JSThis, JSIdent "args"]-                        ]-                )+              , JSApp (JSIdent "i$RUN") []               ]        invokeMain :: T.Text@@ -601,7 +596,7 @@ jsBASETOP _ n = JSAssign jsSTACKBASE (JSBinOp "+" jsSTACKTOP (JSNum (JSInt n)))  jsNULL :: CompileInfo -> Reg -> JS-jsNULL _ r = JSAssign (translateReg r) JSNull+jsNULL _ r = JSDelete (translateReg r)  jsERROR :: CompileInfo -> String -> JS jsERROR _ = JSError@@ -680,9 +675,10 @@       | LNoOp <- op = translateReg (last args)        | LWriteStr <- op,-        (_:str:_) <- args = JSAssign (translateReg reg)-                               (JSApp (JSIdent "i$putStr") [translateReg str])+        (_:str:_) <- args = JSApp (JSIdent "i$putStr") [translateReg str] +      | LReadStr <- op  = JSApp (JSIdent "i$getLine") []+       | (LZExt (ITFixed IT8) ITNative)  <- op = jsUnPackBits $ translateReg (last args)       | (LZExt (ITFixed IT16) ITNative) <- op = jsUnPackBits $ translateReg (last args)       | (LZExt (ITFixed IT32) ITNative) <- op = jsUnPackBits $ translateReg (last args)@@ -699,15 +695,15 @@       | (LSRem (ATInt ITBig))  <- op       , (lhs:rhs:_)            <- args = invokeMeth lhs "mod" [rhs]       | (LEq (ATInt ITBig))    <- op-      , (lhs:rhs:_)            <- args = invokeMeth lhs "equals" [rhs]+      , (lhs:rhs:_)            <- args = JSPreOp "+" $ invokeMeth lhs "equals" [rhs]       | (LSLt (ATInt ITBig))   <- op-      , (lhs:rhs:_)            <- args = invokeMeth lhs "lesser" [rhs]+      , (lhs:rhs:_)            <- args = JSPreOp "+" $ invokeMeth lhs "lesser" [rhs]       | (LSLe (ATInt ITBig))   <- op-      , (lhs:rhs:_)            <- args = invokeMeth lhs "lesserOrEquals" [rhs]+      , (lhs:rhs:_)            <- args = JSPreOp "+" $ invokeMeth lhs "lesserOrEquals" [rhs]       | (LSGt (ATInt ITBig))   <- op-      , (lhs:rhs:_)            <- args = invokeMeth lhs "greater" [rhs]+      , (lhs:rhs:_)            <- args = JSPreOp "+" $ invokeMeth lhs "greater" [rhs]       | (LSGe (ATInt ITBig))   <- op-      , (lhs:rhs:_)            <- args = invokeMeth lhs "greaterOrEquals" [rhs]+      , (lhs:rhs:_)            <- args = JSPreOp "+" $ invokeMeth lhs "greaterOrEquals" [rhs]        | (LPlus ATFloat)  <- op       , (lhs:rhs:_)      <- args = translateBinaryOp "+" lhs rhs@@ -718,15 +714,15 @@       | (LSDiv ATFloat)  <- op       , (lhs:rhs:_)      <- args = translateBinaryOp "/" lhs rhs       | (LEq ATFloat)    <- op-      , (lhs:rhs:_)      <- args = translateBinaryOp "==" lhs rhs+      , (lhs:rhs:_)      <- args = translateCompareOp "==" lhs rhs       | (LSLt ATFloat)   <- op-      , (lhs:rhs:_)      <- args = translateBinaryOp "<" lhs rhs+      , (lhs:rhs:_)      <- args = translateCompareOp "<" lhs rhs       | (LSLe ATFloat)   <- op-      , (lhs:rhs:_)      <- args = translateBinaryOp "<=" lhs rhs+      , (lhs:rhs:_)      <- args = translateCompareOp "<=" lhs rhs       | (LSGt ATFloat)   <- op-      , (lhs:rhs:_)      <- args = translateBinaryOp ">" lhs rhs+      , (lhs:rhs:_)      <- args = translateCompareOp ">" lhs rhs       | (LSGe ATFloat)   <- op-      , (lhs:rhs:_)      <- args = translateBinaryOp ">=" lhs rhs+      , (lhs:rhs:_)      <- args = translateCompareOp ">=" lhs rhs        | (LPlus (ATInt ITChar)) <- op       , (lhs:rhs:_)            <- args =@@ -765,44 +761,26 @@           ]        | (LLSHR (ITFixed IT8)) <- op-      , (lhs:rhs:_)           <- args =-          jsPackUBits8 (-            JSBinOp ">>" (jsUnPackBits $ translateReg lhs) (jsUnPackBits $ translateReg rhs)-          )+      , (lhs:rhs:_)           <- args = jsPackUBits8 $ bitsBinaryOp ">>" lhs rhs        | (LLSHR (ITFixed IT16)) <- op-      , (lhs:rhs:_)            <- args =-          jsPackUBits16 (-            JSBinOp ">>" (jsUnPackBits $ translateReg lhs) (jsUnPackBits $ translateReg rhs)-          )+      , (lhs:rhs:_)            <- args = jsPackUBits16 $ bitsBinaryOp ">>" lhs rhs        | (LLSHR (ITFixed IT32)) <- op-      , (lhs:rhs:_)            <- args =-          jsPackUBits32  (-            JSBinOp ">>" (jsUnPackBits $ translateReg lhs) (jsUnPackBits $ translateReg rhs)-          )+      , (lhs:rhs:_)            <- args = jsPackUBits32 $ bitsBinaryOp ">>" lhs rhs        | (LLSHR (ITFixed IT64)) <- op       , (lhs:rhs:_)            <- args =           jsMeth (translateReg lhs) "shiftRight" [translateReg rhs]        | (LSHL (ITFixed IT8)) <- op-      , (lhs:rhs:_)          <- args =-          jsPackUBits8 (-            JSBinOp "<<" (jsUnPackBits $ translateReg lhs) (jsUnPackBits $ translateReg rhs)-          )+      , (lhs:rhs:_)          <- args = jsPackUBits8 $ bitsBinaryOp "<<" lhs rhs        | (LSHL (ITFixed IT16)) <- op-      , (lhs:rhs:_)           <- args =-          jsPackUBits16 (-            JSBinOp "<<" (jsUnPackBits $ translateReg lhs) (jsUnPackBits $ translateReg rhs)-          )+      , (lhs:rhs:_)           <- args = jsPackUBits16 $ bitsBinaryOp "<<" lhs rhs        | (LSHL (ITFixed IT32)) <- op-      , (lhs:rhs:_)           <- args =-          jsPackUBits32  (-            JSBinOp "<<" (jsUnPackBits $ translateReg lhs) (jsUnPackBits $ translateReg rhs)-          )+      , (lhs:rhs:_)           <- args = jsPackUBits32 $ bitsBinaryOp "<<" lhs rhs        | (LSHL (ITFixed IT64)) <- op       , (lhs:rhs:_)           <- args =@@ -811,88 +789,52 @@           ]        | (LAnd (ITFixed IT8)) <- op-      , (lhs:rhs:_)          <- args =-          jsPackUBits8 (-            JSBinOp "&" (jsUnPackBits (translateReg lhs)) (jsUnPackBits (translateReg rhs))-          )+      , (lhs:rhs:_)          <- args = jsPackUBits8 $ bitsBinaryOp "&" lhs rhs        | (LAnd (ITFixed IT16)) <- op-      , (lhs:rhs:_)           <- args =-          jsPackUBits16 (-            JSBinOp "&" (jsUnPackBits (translateReg lhs)) (jsUnPackBits (translateReg rhs))-          )+      , (lhs:rhs:_)           <- args = jsPackUBits16 $ bitsBinaryOp "&" lhs rhs        | (LAnd (ITFixed IT32)) <- op-      , (lhs:rhs:_)           <- args =-          jsPackUBits32 (-            JSBinOp "&" (jsUnPackBits (translateReg lhs)) (jsUnPackBits (translateReg rhs))-          )+      , (lhs:rhs:_)           <- args = jsPackUBits32 $ bitsBinaryOp "&" lhs rhs        | (LAnd (ITFixed IT64)) <- op       , (lhs:rhs:_)           <- args =           jsMeth (translateReg lhs) "and" [translateReg rhs]        | (LOr (ITFixed IT8)) <- op-      , (lhs:rhs:_)         <- args =-          jsPackUBits8 (-            JSBinOp "|" (jsUnPackBits (translateReg lhs)) (jsUnPackBits (translateReg rhs))-          )+      , (lhs:rhs:_)         <- args = jsPackUBits8 $ bitsBinaryOp "|" lhs rhs        | (LOr (ITFixed IT16)) <- op-      , (lhs:rhs:_)          <- args =-          jsPackUBits16 (-            JSBinOp "|" (jsUnPackBits (translateReg lhs)) (jsUnPackBits (translateReg rhs))-          )+      , (lhs:rhs:_)          <- args = jsPackUBits16 $ bitsBinaryOp "|" lhs rhs        | (LOr (ITFixed IT32)) <- op-      , (lhs:rhs:_)          <- args =-          jsPackUBits32 (-            JSBinOp "|" (jsUnPackBits (translateReg lhs)) (jsUnPackBits (translateReg rhs))-          )+      , (lhs:rhs:_)          <- args = jsPackUBits32 $ bitsBinaryOp "|" lhs rhs        | (LOr (ITFixed IT64)) <- op       , (lhs:rhs:_)          <- args =           jsMeth (translateReg lhs) "or" [translateReg rhs]        | (LXOr (ITFixed IT8)) <- op-      , (lhs:rhs:_)          <- args =-          jsPackUBits8 (-            JSBinOp "^" (jsUnPackBits (translateReg lhs)) (jsUnPackBits (translateReg rhs))-          )+      , (lhs:rhs:_)          <- args = jsPackUBits8 $ bitsBinaryOp "^" lhs rhs        | (LXOr (ITFixed IT16)) <- op-      , (lhs:rhs:_)           <- args =-          jsPackUBits16 (-            JSBinOp "^" (jsUnPackBits (translateReg lhs)) (jsUnPackBits (translateReg rhs))-          )+      , (lhs:rhs:_)           <- args = jsPackUBits16 $ bitsBinaryOp "^" lhs rhs        | (LXOr (ITFixed IT32)) <- op-      , (lhs:rhs:_)           <- args =-          jsPackUBits32 (-            JSBinOp "^" (jsUnPackBits (translateReg lhs)) (jsUnPackBits (translateReg rhs))-          )+      , (lhs:rhs:_)           <- args = jsPackUBits32 $ bitsBinaryOp "^" lhs rhs        | (LXOr (ITFixed IT64)) <- op       , (lhs:rhs:_)           <- args =           jsMeth (translateReg lhs) "xor" [translateReg rhs]        | (LPlus (ATInt (ITFixed IT8))) <- op-      , (lhs:rhs:_)                   <- args =-          jsPackUBits8 (-            JSBinOp "+" (jsUnPackBits (translateReg lhs)) (jsUnPackBits (translateReg rhs))-          )+      , (lhs:rhs:_)                   <- args = jsPackUBits8 $ bitsBinaryOp "+" lhs rhs        | (LPlus (ATInt (ITFixed IT16))) <- op-      , (lhs:rhs:_)                    <- args =-          jsPackUBits16 (-            JSBinOp "+" (jsUnPackBits (translateReg lhs)) (jsUnPackBits (translateReg rhs))-          )+      , (lhs:rhs:_)                    <- args = jsPackUBits16 $ bitsBinaryOp "+" lhs rhs        | (LPlus (ATInt (ITFixed IT32))) <- op-      , (lhs:rhs:_)                    <- args =-          jsPackUBits32 (-            JSBinOp "+" (jsUnPackBits (translateReg lhs)) (jsUnPackBits (translateReg rhs))-          )+      , (lhs:rhs:_)                    <- args = jsPackUBits32 $ bitsBinaryOp "+" lhs rhs        | (LPlus (ATInt (ITFixed IT64))) <- op       , (lhs:rhs:_)                    <- args =@@ -901,22 +843,13 @@           ]        | (LMinus (ATInt (ITFixed IT8))) <- op-      , (lhs:rhs:_)                    <- args =-          jsPackUBits8 (-            JSBinOp "-" (jsUnPackBits (translateReg lhs)) (jsUnPackBits (translateReg rhs))-          )+      , (lhs:rhs:_)                    <- args = jsPackUBits8 $ bitsBinaryOp "-" lhs rhs        | (LMinus (ATInt (ITFixed IT16))) <- op-      , (lhs:rhs:_)                     <- args =-          jsPackUBits16 (-            JSBinOp "-" (jsUnPackBits (translateReg lhs)) (jsUnPackBits (translateReg rhs))-          )+      , (lhs:rhs:_)                     <- args = jsPackUBits16 $ bitsBinaryOp "-" lhs rhs        | (LMinus (ATInt (ITFixed IT32))) <- op-      , (lhs:rhs:_)                     <- args =-          jsPackUBits32 (-            JSBinOp "-" (jsUnPackBits (translateReg lhs)) (jsUnPackBits (translateReg rhs))-          )+      , (lhs:rhs:_)                     <- args = jsPackUBits32 $ bitsBinaryOp "-" lhs rhs        | (LMinus (ATInt (ITFixed IT64))) <- op       , (lhs:rhs:_)                     <- args =@@ -925,22 +858,13 @@           ]        | (LTimes (ATInt (ITFixed IT8))) <- op-      , (lhs:rhs:_)                    <- args =-          jsPackUBits8 (-            JSBinOp "*" (jsUnPackBits (translateReg lhs)) (jsUnPackBits (translateReg rhs))-          )+      , (lhs:rhs:_)                    <- args = jsPackUBits8 $ bitsBinaryOp "*" lhs rhs        | (LTimes (ATInt (ITFixed IT16))) <- op-      , (lhs:rhs:_)                     <- args =-          jsPackUBits16 (-            JSBinOp "*" (jsUnPackBits (translateReg lhs)) (jsUnPackBits (translateReg rhs))-          )+      , (lhs:rhs:_)                     <- args = jsPackUBits16 $ bitsBinaryOp "*" lhs rhs        | (LTimes (ATInt (ITFixed IT32))) <- op-      , (lhs:rhs:_)                     <- args =-          jsPackUBits32 (-            JSBinOp "*" (jsUnPackBits (translateReg lhs)) (jsUnPackBits (translateReg rhs))-          )+      , (lhs:rhs:_)                     <- args = jsPackUBits32 $ bitsBinaryOp "*" lhs rhs        | (LTimes (ATInt (ITFixed IT64))) <- op       , (lhs:rhs:_)                     <- args =@@ -949,110 +873,62 @@           ]        | (LEq (ATInt (ITFixed IT8))) <- op-      , (lhs:rhs:_)                 <- args =-          jsPackUBits8 (-            JSBinOp "==" (jsUnPackBits (translateReg lhs)) (jsUnPackBits (translateReg rhs))-          )+      , (lhs:rhs:_)                 <- args = bitsCompareOp "==" lhs rhs        | (LEq (ATInt (ITFixed IT16))) <- op-      , (lhs:rhs:_)                  <- args =-          jsPackUBits16 (-            JSBinOp "==" (jsUnPackBits (translateReg lhs)) (jsUnPackBits (translateReg rhs))-          )+      , (lhs:rhs:_)                  <- args = bitsCompareOp "==" lhs rhs        | (LEq (ATInt (ITFixed IT32))) <- op-      , (lhs:rhs:_)                  <- args =-          jsPackUBits32 (-            JSBinOp "==" (jsUnPackBits (translateReg lhs)) (jsUnPackBits (translateReg rhs))-          )+      , (lhs:rhs:_)                  <- args = bitsCompareOp "==" lhs rhs        | (LEq (ATInt (ITFixed IT64))) <- op-      , (lhs:rhs:_)                   <- args =-          jsMeth (jsMeth (translateReg lhs) "equals" [translateReg rhs]) "and" [-            jsBigInt (JSString $ show 0xFFFFFFFFFFFFFFFF)-          ]+      , (lhs:rhs:_)                  <- args = JSPreOp "+" $ invokeMeth lhs "equals" [rhs]        | (LLt (ITFixed IT8)) <- op-      , (lhs:rhs:_)         <- args =-          jsPackUBits8 (-            JSBinOp "<" (jsUnPackBits (translateReg lhs)) (jsUnPackBits (translateReg rhs))-          )+      , (lhs:rhs:_)         <- args = bitsCompareOp "<" lhs rhs        | (LLt (ITFixed IT16)) <- op-      , (lhs:rhs:_)          <- args =-          jsPackUBits16 (-            JSBinOp "<" (jsUnPackBits (translateReg lhs)) (jsUnPackBits (translateReg rhs))-          )+      , (lhs:rhs:_)          <- args = bitsCompareOp "<" lhs rhs        | (LLt (ITFixed IT32)) <- op-      , (lhs:rhs:_)          <- args =-          jsPackUBits32 (-            JSBinOp "<" (jsUnPackBits (translateReg lhs)) (jsUnPackBits (translateReg rhs))-          )+      , (lhs:rhs:_)          <- args = bitsCompareOp "<" lhs rhs        | (LLt (ITFixed IT64)) <- op-      , (lhs:rhs:_)          <- args = invokeMeth lhs "lesser" [rhs]+      , (lhs:rhs:_)          <- args = JSPreOp "+" $ invokeMeth lhs "lesser" [rhs]        | (LLe (ITFixed IT8)) <- op-      , (lhs:rhs:_)         <- args =-          jsPackUBits8 (-            JSBinOp "<=" (jsUnPackBits (translateReg lhs)) (jsUnPackBits (translateReg rhs))-          )+      , (lhs:rhs:_)         <- args = bitsCompareOp "<=" lhs rhs        | (LLe (ITFixed IT16)) <- op-      , (lhs:rhs:_)          <- args =-          jsPackUBits16 (-            JSBinOp "<=" (jsUnPackBits (translateReg lhs)) (jsUnPackBits (translateReg rhs))-          )+      , (lhs:rhs:_)          <- args = bitsCompareOp "<=" lhs rhs        | (LLe (ITFixed IT32)) <- op-      , (lhs:rhs:_)          <- args =-          jsPackUBits32 (-            JSBinOp "<=" (jsUnPackBits (translateReg lhs)) (jsUnPackBits (translateReg rhs))-          )+      , (lhs:rhs:_)          <- args = bitsCompareOp "<=" lhs rhs        | (LLe (ITFixed IT64)) <- op-      , (lhs:rhs:_)          <- args = invokeMeth lhs "lesserOrEquals" [rhs]+      , (lhs:rhs:_)          <- args = JSPreOp "+" $ invokeMeth lhs "lesserOrEquals" [rhs]        | (LGt (ITFixed IT8)) <- op-      , (lhs:rhs:_)         <- args =-          jsPackUBits8 (-            JSBinOp ">" (jsUnPackBits (translateReg lhs)) (jsUnPackBits (translateReg rhs))-          )+      , (lhs:rhs:_)         <- args = bitsCompareOp ">" lhs rhs        | (LGt (ITFixed IT16)) <- op-      , (lhs:rhs:_)          <- args =-          jsPackUBits16 (-            JSBinOp ">" (jsUnPackBits (translateReg lhs)) (jsUnPackBits (translateReg rhs))-          )+      , (lhs:rhs:_)          <- args = bitsCompareOp ">" lhs rhs       | (LGt (ITFixed IT32)) <- op-      , (lhs:rhs:_)          <- args =-          jsPackUBits32 (-            JSBinOp ">" (jsUnPackBits (translateReg lhs)) (jsUnPackBits (translateReg rhs))-          )+      , (lhs:rhs:_)          <- args = bitsCompareOp ">" lhs rhs        | (LGt (ITFixed IT64)) <- op-      , (lhs:rhs:_)          <- args = invokeMeth lhs "greater" [rhs]+      , (lhs:rhs:_)          <- args = JSPreOp "+" $ invokeMeth lhs "greater" [rhs]        | (LGe (ITFixed IT8)) <- op-      , (lhs:rhs:_)         <- args =-          jsPackUBits8 (-            JSBinOp ">=" (jsUnPackBits (translateReg lhs)) (jsUnPackBits (translateReg rhs))-          )+      , (lhs:rhs:_)         <- args = bitsCompareOp ">=" lhs rhs        | (LGe (ITFixed IT16)) <- op-      , (lhs:rhs:_)          <- args =-          jsPackUBits16 (-            JSBinOp ">=" (jsUnPackBits (translateReg lhs)) (jsUnPackBits (translateReg rhs))-          )+      , (lhs:rhs:_)          <- args = bitsCompareOp ">=" lhs rhs       | (LGe (ITFixed IT32)) <- op-      , (lhs:rhs:_)          <- args =-          jsPackUBits32 (-            JSBinOp ">=" (jsUnPackBits (translateReg lhs)) (jsUnPackBits (translateReg rhs))-          )+      , (lhs:rhs:_)          <- args = bitsCompareOp ">=" lhs rhs        | (LGe (ITFixed IT64)) <- op-      , (lhs:rhs:_)          <- args = invokeMeth lhs "greaterOrEquals" [rhs]+      , (lhs:rhs:_)          <- args = JSPreOp "+" $ invokeMeth lhs "greaterOrEquals" [rhs]        | (LUDiv (ITFixed IT8)) <- op       , (lhs:rhs:_)           <- args =@@ -1154,8 +1030,7 @@           jsPackSBits32 $ JSPreOp "~" $ jsUnPackBits (translateReg arg)        | (LCompl (ITFixed IT64)) <- op-      , (arg:_)     <- args =-          invokeMeth arg "not" []+      , (arg:_)                 <- args = invokeMeth arg "not" []        | (LPlus _)   <- op       , (lhs:rhs:_) <- args = translateBinaryOp "+" lhs rhs@@ -1168,15 +1043,15 @@       | (LSRem _)   <- op       , (lhs:rhs:_) <- args = translateBinaryOp "%" lhs rhs       | (LEq _)     <- op-      , (lhs:rhs:_) <- args = translateBinaryOp "==" lhs rhs+      , (lhs:rhs:_) <- args = translateCompareOp "==" lhs rhs       | (LSLt _)    <- op-      , (lhs:rhs:_) <- args = translateBinaryOp "<" lhs rhs+      , (lhs:rhs:_) <- args = translateCompareOp "<" lhs rhs       | (LSLe _)    <- op-      , (lhs:rhs:_) <- args = translateBinaryOp "<=" lhs rhs+      , (lhs:rhs:_) <- args = translateCompareOp "<=" lhs rhs       | (LSGt _)    <- op-      , (lhs:rhs:_) <- args = translateBinaryOp ">" lhs rhs+      , (lhs:rhs:_) <- args = translateCompareOp ">" lhs rhs       | (LSGe _)    <- op-      , (lhs:rhs:_) <- args = translateBinaryOp ">=" lhs rhs+      , (lhs:rhs:_) <- args = translateCompareOp ">=" lhs rhs       | (LAnd _)    <- op       , (lhs:rhs:_) <- args = translateBinaryOp "&" lhs rhs       | (LOr _)     <- op@@ -1193,9 +1068,9 @@       | LStrConcat  <- op       , (lhs:rhs:_) <- args = translateBinaryOp "+" lhs rhs       | LStrEq      <- op-      , (lhs:rhs:_) <- args = translateBinaryOp "==" lhs rhs+      , (lhs:rhs:_) <- args = translateCompareOp "==" lhs rhs       | LStrLt      <- op-      , (lhs:rhs:_) <- args = translateBinaryOp "<" lhs rhs+      , (lhs:rhs:_) <- args = translateCompareOp "<" lhs rhs       | LStrLen     <- op       , (arg:_)     <- args = JSProj (translateReg arg) "length"       | (LStrInt ITNative)      <- op@@ -1270,13 +1145,28 @@       , (arg:_) <- args = jsCall "i$systemInfo"  [translateReg arg]       | LExternal nul <- op       , nul == sUN "prim__null"-      , (_)         <- args = JSNull+      , _ <- args = JSNull+      | LExternal ex <- op+      , ex == sUN "prim__eqPtr"+      , [lhs, rhs] <- args = translateCompareOp "==" lhs rhs       | otherwise = JSError $ "Not implemented: " ++ show op         where           translateBinaryOp :: String -> Reg -> Reg -> JS           translateBinaryOp op lhs rhs =             JSBinOp op (translateReg lhs) (translateReg rhs) +          translateCompareOp :: String -> Reg -> Reg -> JS+          translateCompareOp op lhs rhs =+            JSPreOp "+" $ translateBinaryOp op lhs rhs++          bitsBinaryOp :: String -> Reg -> Reg -> JS+          bitsBinaryOp op lhs rhs =+            JSBinOp op (jsUnPackBits (translateReg lhs)) (jsUnPackBits (translateReg rhs))++          bitsCompareOp :: String -> Reg -> Reg -> JS+          bitsCompareOp op lhs rhs =+            JSPreOp "+" $ bitsBinaryOp op lhs rhs+           invokeMeth :: Reg -> String -> [Reg] -> JS           invokeMeth obj meth args =             JSApp (JSProj (translateReg obj) meth) $ map translateReg args@@ -1331,6 +1221,7 @@   | TAILCALL n            <- bc = jsTAILCALL info n   | FOREIGNCALL r _ (FStr n) args                           <- bc = jsFOREIGN info r n (map fcall args)+  | FOREIGNCALL _ _ _ _   <- bc = error "JS FFI call not statically known"   | TOPBASE n             <- bc = jsTOPBASE info n   | BASETOP n             <- bc = jsBASETOP info n   | STOREOLD              <- bc = jsSTOREOLD info

@@ -60,7 +60,7 @@         maindef <- case mtm of                         Nothing -> return []                         Just tm -> do md <- irMain tm-                                      iLOG $ "MAIN: " ++ show md+                                      logLvl 1 $ "MAIN: " ++ show md                                       return [(sMN 0 "runMain", md)]         objs <- getObjectFiles codegen         libs <- getLibs codegen@@ -83,13 +83,13 @@         let (nexttag, tagged) = addTags 65536 (liftAll defsUniq)         let ctxtIn = addAlist tagged emptyContext -        iLOG "Defunctionalising"+        logLvl 1 "Defunctionalising"         let defuns_in = defunctionalise nexttag ctxtIn         logLvl 5 $ show defuns_in-        iLOG "Inlining"+        logLvl 1 "Inlining"         let defuns = inline defuns_in         logLvl 5 $ show defuns-        iLOG "Resolving variables for CG"+        logLvl 1 "Resolving variables for CG"         -- iputStrLn $ showSep "\n" (map show (toAlist defuns))         let checked = simplifyDefs defuns (toAlist defuns)         outty <- outputTy@@ -103,7 +103,7 @@             Just f -> runIO $ writeFile f (dumpDefuns defuns)         triple <- Idris.AbsSyntax.targetTriple         cpu <- Idris.AbsSyntax.targetCPU-        iLOG "Building output"+        logLvl 1 "Building output"         case checked of             OK c -> do return $ CodegenInfo f outty triple cpu                                             hdrs impdirs objs libs flags@@ -120,7 +120,7 @@   where checkMVs = do i <- getIState                       case map fst (idris_metavars i) \\ primDefs of                             [] -> return ()-                            ms -> ifail $ "There are undefined metavariables: " ++ show ms+                            ms -> ifail $ "There are undefined holes: " ++ show ms         checkTotality = do i <- getIState                            case idris_totcheckfail i of                              [] -> return ()@@ -136,7 +136,7 @@        Via "c" -> codegenC ir        -- Any external code generator        Via cg -> do let cmd = "idris-" ++ cg-                        args = [mainmod, "-o", outputFile ir]+                        args = [mainmod, "-o", outputFile ir] ++ compilerFlags ir                     exit <- rawSystem cmd args                     when (exit /= ExitSuccess) $                        putStrLn ("FAILURE: " ++ show cmd ++ " " ++ show args)

@@ -76,6 +76,7 @@         | JSWhile JS JS         | JSFFI String [JS]         | JSAnnotation JSAnnotation JS+        | JSDelete JS         | JSNoop         deriving Eq @@ -129,6 +130,9 @@   `T.append` " */\n"   `T.append` compileJS' indent js +compileJS' indent (JSDelete js) =+  "delete " `T.append` compileJS' 0 js+ compileJS' indent (JSFFI raw args) =   ffi raw (map (T.unpack . compileJS' indent) args) @@ -190,7 +194,7 @@   `T.append` compileJS' indent rhs  compileJS' indent (JSPreOp op val) =-  T.pack op `T.append` compileJS' indent val+  T.pack op `T.append` "(" `T.append` compileJS' indent val `T.append` ")"  compileJS' indent (JSProj obj field)   | JSFunction {} <- obj =

@@ -1,4 +1,7 @@-module Idris.ASTUtils where+module Idris.ASTUtils(Field(), cg_usedpos, ctxt_lookup, fgetState, fmodifyState,+                      fputState, idris_fixities, ist_callgraph, ist_optimisation,+                      known_classes, known_terms, opt_detaggable, opt_inaccessible, +                      opts_idrisCmdline, repl_definitions) where  -- This implements just a few basic lens-like concepts to ease state updates. -- Similar to fclabels in approach, just without the extra dependency.

@@ -16,6 +16,7 @@  import System.Console.Haskeline import System.IO+import System.Directory (canonicalizePath, doesFileExist)  import Control.Applicative import Control.Monad (liftM3)@@ -344,7 +345,7 @@ addToCalledG n ns = return () -- TODO  push_estack :: Name -> Bool -> Idris ()-push_estack n inst +push_estack n inst     = do i <- getIState          putIState (i { elab_stack = (n, inst) : elab_stack i }) @@ -400,10 +401,10 @@ addAutoHint n hint =     do ist <- getIState        case lookupCtxtExact n (idris_autohints ist) of-            Nothing -> +            Nothing ->                  do let hs = addDef n [hint] (idris_autohints ist)                     putIState $ ist { idris_autohints = hs }-            Just nhints -> +            Just nhints ->                  do let hs = addDef n (hint : nhints) (idris_autohints ist)                     putIState $ ist { idris_autohints = hs } @@ -516,14 +517,26 @@ addInternalApp :: FilePath -> Int -> PTerm -> Idris () addInternalApp fp l t     = do i <- getIState-         putIState (i { idris_lineapps = ((fp, l), t) : idris_lineapps i })+         -- We canonicalise the path to make "./Test/Module.idr" equal+         -- to "Test/Module.idr"+         exists <- runIO $ doesFileExist fp+         when exists $+           do fp' <- runIO $ canonicalizePath fp+              putIState (i { idris_lineapps = ((fp', l), t) : idris_lineapps i })  getInternalApp :: FilePath -> Int -> Idris PTerm getInternalApp fp l = do i <- getIState-                         case lookup (fp, l) (idris_lineapps i) of-                              Just n' -> return n'-                              Nothing -> return Placeholder-                              -- TODO: What if it's not there?+                         -- We canonicalise the path to make+                         -- "./Test/Module.idr" equal to+                         -- "Test/Module.idr"+                         exists <- runIO $ doesFileExist fp+                         if exists+                           then do fp' <- runIO $ canonicalizePath fp+                                   case lookup (fp', l) (idris_lineapps i) of+                                     Just n' -> return n'+                                     Nothing -> return Placeholder+                                     -- TODO: What if it's not there?+                           else return Placeholder  -- Pattern definitions are only used for coverage checking, so erase them -- when we're done@@ -576,7 +589,7 @@          putIState $ i { tt_ctxt = ctxt', idris_constraints = ics }   where     insertAll [] c = c-    insertAll ((c, fc) : cs) ics +    insertAll ((c, fc) : cs) ics        = insertAll cs $ S.insert (ConstraintFC c fc) ics  addDeferred = addDeferred' Ref@@ -584,7 +597,7 @@  -- | Save information about a name that is not yet defined addDeferred' :: NameType-             -> [(Name, (Int, Maybe Name, Type, Bool))]+             -> [(Name, (Int, Maybe Name, Type, [Name], Bool))]                 -- ^ The Name is the name being made into a metavar,                 -- the Int is the number of vars that are part of a                 -- putative proof context, the Maybe Name is the@@ -593,10 +606,10 @@                 -- allowed              -> Idris () addDeferred' nt ns-  = do mapM_ (\(n, (i, _, t, _)) -> updateContext (addTyDecl n nt (tidyNames S.empty t))) ns+  = do mapM_ (\(n, (i, _, t, _, _)) -> updateContext (addTyDecl n nt (tidyNames S.empty t))) ns        mapM_ (\(n, _) -> when (not (n `elem` primDefs)) $ addIBC (IBCMetavar n)) ns        i <- getIState-       putIState $ i { idris_metavars = map (\(n, (i, top, _, isTopLevel)) -> (n, (top, i, isTopLevel))) ns +++       putIState $ i { idris_metavars = map (\(n, (i, top, _, ns, isTopLevel)) -> (n, (top, i, ns, isTopLevel))) ns ++                                             idris_metavars i }   where         -- 'tidyNames' is to generate user accessible names in case they are@@ -637,7 +650,12 @@ setWidth w = do ist <- getIState                 put ist { idris_consolewidth = w } +setDepth :: Maybe Int -> Idris ()+setDepth d = do ist <- getIState+                put ist { idris_options = (idris_options ist) { opt_printdepth = d } } +typeDescription :: String+typeDescription = "The type of types"   type1Doc :: Doc OutputAnnotation@@ -676,6 +694,11 @@ getCmdLine = do i <- getIState                 return (opt_cmdline (idris_options i)) +getDumpHighlighting :: Idris Bool+getDumpHighlighting = do ist <- getIState+                         return (findC (opt_cmdline (idris_options ist)))+  where findC = elem DumpHighlights+ getDumpDefun :: Idris (Maybe FilePath) getDumpDefun = do i <- getIState                   return $ findC (opt_cmdline (idris_options i))@@ -767,6 +790,12 @@                  let opts = idris_options i                  return (opt_nobanner opts) +setEvalTypes :: Bool -> Idris ()+setEvalTypes n = do i <- getIState+                    let opts = idris_options i+                    let opt' = opts { opt_evaltypes = n }+                    putIState $ i { idris_options = opt' }+ setQuiet :: Bool -> Idris () setQuiet q = do i <- getIState                 let opts = idris_options i@@ -928,9 +957,6 @@ cmdOptType x = do i <- getIState                   return $ x `elem` opt_cmdline (idris_options i) -iLOG :: String -> Idris ()-iLOG = logLvl 1- noErrors :: Idris Bool noErrors = do i <- getIState               case errSpan i of@@ -978,15 +1004,15 @@                      PLet fc n' nfc (en ty) (en v) (en (shadow n n' s))        | otherwise = PLet fc n nfc (en ty) (en v) (en s)     -- FIXME: Should only do this in a type signature!-    en (PDPair f p (PRef f' n) t r)+    en (PDPair f hls p (PRef f' fcs n) t r)        | n `elem` (map fst ps ++ ns) && t /= Placeholder            = let n' = mkShadow n in-                 PDPair f p (PRef f' n') (en t) (en (shadow n n' r))+                 PDPair f hls p (PRef f' fcs n') (en t) (en (shadow n n' r))     en (PRewrite f l r g) = PRewrite f (en l) (en r) (fmap en g)     en (PTyped l r) = PTyped (en l) (en r)-    en (PPair f p l r) = PPair f p (en l) (en r)-    en (PDPair f p l t r) = PDPair f p (en l) (en t) (en r)-    en (PAlternative a as) = PAlternative a (map en as)+    en (PPair f hls p l r) = PPair f hls p (en l) (en r)+    en (PDPair f hls p l t r) = PDPair f hls p (en l) (en t) (en r)+    en (PAlternative ns a as) = PAlternative ns a (map en as)     en (PHidden t) = PHidden (en t)     en (PUnifyLog t) = PUnifyLog (en t)     en (PDisamb ds t) = PDisamb ds (en t)@@ -997,32 +1023,33 @@      en (PQuote (Var n))         | n `nselem` ns = PQuote (Var (dec n))-    en (PApp fc (PInferRef fc' n) as)-        | n `nselem` ns = PApp fc (PInferRef fc' (dec n))-                           (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))-    en (PApp fc (PRef fc' n) as)-        | n `elem` infs = PApp fc (PInferRef fc' (dec n))-                           (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))-        | n `nselem` ns = PApp fc (PRef fc' (dec n))-                           (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))-    en (PAppBind fc (PRef fc' n) as)-        | n `elem` infs = PAppBind fc (PInferRef fc' (dec n))-                           (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))-        | n `nselem` ns = PAppBind fc (PRef fc' (dec n))-                           (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))-    en (PRef fc n)-        | n `elem` infs = PApp fc (PInferRef fc (dec n))-                           (map (pexp . (PRef fc)) (map fst ps))-        | n `nselem` ns = PApp fc (PRef fc (dec n))-                           (map (pexp . (PRef fc)) (map fst ps))-    en (PInferRef fc n)-        | n `nselem` ns = PApp fc (PInferRef fc (dec n))-                           (map (pexp . (PRef fc)) (map fst ps))+    en (PApp fc (PInferRef fc' hl n) as)+        | n `nselem` ns = PApp fc (PInferRef fc' hl (dec n))+                           (map (pexp . (PRef fc hl)) (map fst ps) ++ (map (fmap en) as))+    en (PApp fc (PRef fc' hl n) as)+        | n `elem` infs = PApp fc (PInferRef fc' hl (dec n))+                           (map (pexp . (PRef fc hl)) (map fst ps) ++ (map (fmap en) as))+        | n `nselem` ns = PApp fc (PRef fc' hl (dec n))+                           (map (pexp . (PRef fc hl)) (map fst ps) ++ (map (fmap en) as))+    en (PAppBind fc (PRef fc' hl n) as)+        | n `elem` infs = PAppBind fc (PInferRef fc' hl (dec n))+                           (map (pexp . (PRef fc hl)) (map fst ps) ++ (map (fmap en) as))+        | n `nselem` ns = PAppBind fc (PRef fc' hl (dec n))+                           (map (pexp . (PRef fc hl)) (map fst ps) ++ (map (fmap en) as))+    en (PRef fc hl n)+        | n `elem` infs = PApp fc (PInferRef fc hl (dec n))+                           (map (pexp . (PRef fc hl)) (map fst ps))+        | n `nselem` ns = PApp fc (PRef fc hl (dec n))+                           (map (pexp . (PRef fc hl)) (map fst ps))+    en (PInferRef fc hl n)+        | n `nselem` ns = PApp fc (PInferRef fc hl (dec n))+                           (map (pexp . (PRef fc hl)) (map fst ps))     en (PApp fc f as) = PApp fc (en f) (map (fmap en) as)     en (PAppBind fc f as) = PAppBind fc (en f) (map (fmap en) as)     en (PCase fc c os) = PCase fc (en c) (map (pmap en) os)     en (PIfThenElse fc c t f) = PIfThenElse fc (en c) (en t) (en f)-    en (PRunElab fc tm) = PRunElab fc (en tm)+    en (PRunElab fc tm ns) = PRunElab fc (en tm) ns+    en (PConstSugar fc tm) = PConstSugar fc (en tm)     en t = t      nselem x [] = False@@ -1043,13 +1070,13 @@               PTy doc argdocs syn fc o (dec n) nfc (piBindp expl_param ps (expandParams dec ps ns [] ty))          else --trace (show (n, expandParams dec ps ns ty)) $               PTy doc argdocs syn fc o n nfc (expandParams dec ps ns [] ty)-expandParamsD rhsonly ist dec ps ns (PPostulate e doc syn fc o n ty)+expandParamsD rhsonly ist dec ps ns (PPostulate e doc syn fc nfc o n ty)     = if n `elem` ns && (not rhsonly)          then -- trace (show (n, expandParams dec ps ns ty)) $-              PPostulate e doc syn fc o (dec n) (piBind ps-                            (expandParams dec ps ns [] ty))+              PPostulate e doc syn fc nfc o (dec n)+                         (piBind ps (expandParams dec ps ns [] ty))          else --trace (show (n, expandParams dec ps ns ty)) $-              PPostulate e doc syn fc o n (expandParams dec ps ns [] ty)+              PPostulate e doc syn fc nfc o n (expandParams dec ps ns [] ty) expandParamsD rhsonly ist dec ps ns (PClauses fc opts n cs)     = let n' = if n `elem` ns then dec n else n in           PClauses fc opts n' (map expandParamsC cs)@@ -1083,10 +1110,10 @@      removeBound lhs ns = ns \\ nub (bnames lhs) -    bnames (PRef _ n) = [n]+    bnames (PRef _ _ n) = [n]     bnames (PApp _ _ args) = concatMap bnames (map getTm args)-    bnames (PPair _ _ l r) = bnames l ++ bnames r-    bnames (PDPair _ _ l Placeholder r) = bnames l ++ bnames r+    bnames (PPair _ _ _ l r) = bnames l ++ bnames r+    bnames (PDPair _ _ _ l Placeholder r) = bnames l ++ bnames r     bnames _ = []  -- | Expands parameters defined in parameter and where blocks inside of declarations@@ -1142,7 +1169,7 @@ getPriority :: IState -> PTerm -> Int getPriority i tm = 1 -- pri tm   where-    pri (PRef _ n) =+    pri (PRef _ _ n) =         case lookupP n (tt_ctxt i) of             ((P (DCon _ _ _) _ _):_) -> 1             ((P (TCon _ _) _ _):_) -> 1@@ -1155,9 +1182,9 @@     pri (PAppBind _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))     pri (PCase _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.snd) as)))     pri (PTyped l r) = pri l-    pri (PPair _ _ l r) = max 1 (max (pri l) (pri r))-    pri (PDPair _ _ l t r) = max 1 (max (pri l) (max (pri t) (pri r)))-    pri (PAlternative a as) = maximum (map pri as)+    pri (PPair _ _ _ l r) = max 1 (max (pri l) (pri r))+    pri (PDPair _ _ _ l t r) = max 1 (max (pri l) (max (pri t) (pri r)))+    pri (PAlternative _ a as) = maximum (map pri as)     pri (PConstant _ _) = 0     pri Placeholder = 1     pri _ = 3@@ -1268,20 +1295,20 @@                          (mkConst c args) (doAdd cs ns t)              | otherwise = doAdd cs ns t -         mkConst c args = PApp fc (PRef fc c)-                           (map (\n -> PExp 0 [] (sMN 0 "carg") (PRef fc n)) args)+         mkConst c args = PApp fc (PRef fc [] c)+                           (map (\n -> PExp 0 [] (sMN 0 "carg") (PRef fc [] n)) args)           getConstraints (PPi (Constraint _ _) _ _ c sc)              = getcapp c ++ getConstraints sc          getConstraints (PPi _ _ _ c sc) = getConstraints sc          getConstraints _ = [] -         getcapp (PApp _ (PRef _ c) args)+         getcapp (PApp _ (PRef _ _ c) args)              = do ns <- mapM getName args                   return (UConstraint c ns)          getcapp _ = [] -         getName (PExp _ _ _ (PRef _ n)) = return n+         getName (PExp _ _ _ (PRef _ _ n)) = return n          getName _ = []  -- Add implicit bindings from using block, and bind any missing names@@ -1318,7 +1345,7 @@          bindFree (n:ns) tm              | elem n (map iname uimpls) = bindFree ns tm              | otherwise-                    = PPi (Imp [] Dynamic False Nothing) n NoFC Placeholder (bindFree ns tm)+                    = PPi (Imp [InaccessibleArg] Dynamic False Nothing) n NoFC Placeholder (bindFree ns tm)           getArgnames (PPi _ n _ c sc)              = n : getArgnames sc@@ -1358,8 +1385,9 @@ -- argument position.  -- This has become a right mess already. Better redo it some time...--- TODO: This is obsoleted by the new way of elaborating types, but there's still--- a couple of places which use it. Clean them up!+-- TODO: This is obsoleted by the new way of elaborating types, (which+-- calls addUsingImpls) but there's still a couple of places which use+-- it. Clean them up! -- -- Issue 1739 in the issue tracker --     https://github.com/idris-lang/Idris-dev/issues/1739@@ -1437,7 +1465,7 @@              imps True (n:env) sc     imps top env (PPi (Exp l _ _) n _ ty sc)         = do let isn = nub (implNamesIn uvars ty ++ case sc of-                            (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]+                            (PRef _ _ x) -> namesIn uvars ist sc `dropAll` [n]                             _ -> [])              (decls, ns) <- get -- ignore decls in HO types              put (PExp (getPriority ist ty) l n Placeholder : decls,@@ -1445,7 +1473,7 @@              imps True (n:env) sc     imps top env (PPi (Constraint l _) n _ ty sc)         = do let isn = nub (implNamesIn uvars ty ++ case sc of-                            (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]+                            (PRef _ _ x) -> namesIn uvars ist sc `dropAll` [n]                             _ -> [])              (decls, ns) <- get -- ignore decls in HO types              put (PConstraint 10 l n Placeholder : decls,@@ -1453,7 +1481,7 @@              imps True (n:env) sc     imps top env (PPi (TacImp l _ scr) n _ ty sc)         = do let isn = nub (implNamesIn uvars ty ++ case sc of-                            (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]+                            (PRef _ _ x) -> namesIn uvars ist sc `dropAll` [n]                             _ -> [])              (decls, ns) <- get -- ignore decls in HO types              put (PTacImplicit 10 l n scr Placeholder : decls,@@ -1465,20 +1493,20 @@              put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))     imps top env (PTyped l r)         = imps top env l-    imps top env (PPair _ _ l r)+    imps top env (PPair _ _ _ l r)         = do (decls, ns) <- get              let isn = namesIn uvars ist l ++ namesIn uvars ist r              put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))-    imps top env (PDPair _ _ (PRef _ n) t r)+    imps top env (PDPair _ _ _ (PRef _ _ n) t r)         = do (decls, ns) <- get              let isn = nub (namesIn uvars ist t ++ namesIn uvars ist r) \\ [n]              put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))-    imps top env (PDPair _ _ l t r)+    imps top env (PDPair _ _ _ l t r)         = do (decls, ns) <- get              let isn = namesIn uvars ist l ++ namesIn uvars ist t ++                        namesIn uvars ist r              put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))-    imps top env (PAlternative a as)+    imps top env (PAlternative ms a as)         = do (decls, ns) <- get              let isn = concatMap (namesIn uvars ist) as              put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))@@ -1488,15 +1516,17 @@     imps top env (PHidden tm)    = imps False env tm     imps top env (PUnifyLog tm)  = imps False env tm     imps top env (PNoImplicits tm)  = imps False env tm-    imps top env (PRunElab fc tm) = imps False env tm+    imps top env (PRunElab fc tm ns) = imps False env tm+    imps top env (PConstSugar fc tm) = imps top env tm -- ignore PConstSugar - it's for highlighting only!     imps top env _               = return ()      pibind using []     sc = sc     pibind using (n:ns) sc       = case lookup n using of-            Just ty -> PPi (Imp [] Dynamic False Nothing) n NoFC ty (pibind using ns sc)-            Nothing -> PPi (Imp [] Dynamic False Nothing) n NoFC Placeholder-                                   (pibind using ns sc)+            Just ty -> PPi (Imp [] Dynamic False Nothing)+                           n NoFC ty (pibind using ns sc)+            Nothing -> PPi (Imp [InaccessibleArg] Dynamic False Nothing)+                           n NoFC Placeholder (pibind using ns sc)  -- Add implicit arguments in function calls addImplPat :: IState -> PTerm -> PTerm@@ -1520,13 +1550,13 @@  addImpl' :: Bool -> [Name] -> [Name] -> [Name] -> IState -> PTerm -> PTerm addImpl' inpat env infns imp_meths ist ptm-         = mkUniqueNames env (ai False (zip env (repeat Nothing)) [] ptm)+         = mkUniqueNames env [] (ai False (zip env (repeat Nothing)) [] ptm)   where     ai :: Bool -> [(Name, Maybe PTerm)] -> [[T.Text]] -> PTerm -> PTerm-    ai qq env ds (PRef fc f)-        | f `elem` infns = PInferRef fc f+    ai qq env ds (PRef fc fcs f)+        | f `elem` infns = PInferRef fc fcs f         | not (f `elem` map fst env) = handleErr $ aiFn inpat inpat qq imp_meths ist fc f fc ds []-    ai qq env ds (PHidden (PRef fc f))+    ai qq env ds (PHidden (PRef fc hl f))         | not (f `elem` map fst env) = PHidden (handleErr $ aiFn inpat False qq imp_meths ist fc f fc ds [])     ai qq env ds (PRewrite fc l r g)        = let l' = ai qq env ds l@@ -1537,24 +1567,24 @@       = let l' = ai qq env ds l             r' = ai qq env ds r in             PTyped l' r'-    ai qq env ds (PPair fc p l r)+    ai qq env ds (PPair fc hls p l r)       = let l' = ai qq env ds l             r' = ai qq env ds r in-            PPair fc p l' r'-    ai qq env ds (PDPair fc p l t r)+            PPair fc hls p l' r'+    ai qq env ds (PDPair fc hls p l t r)          = let l' = ai qq env ds l                t' = ai qq env ds t                r' = ai qq env ds r in-           PDPair fc p l' t' r'-    ai qq env ds (PAlternative a as)+           PDPair fc hls p l' t' r'+    ai qq env ds (PAlternative ms a as)            = let as' = map (ai qq env ds) as in-                 PAlternative a as'+                 PAlternative ms a as'     ai qq env _ (PDisamb ds' as) = ai qq env ds' as-    ai qq env ds (PApp fc (PInferRef ffc f) as)+    ai qq env ds (PApp fc (PInferRef ffc hl f) as)         = let as' = map (fmap (ai qq env ds)) as in-              PApp fc (PInferRef ffc f) as'-    ai qq env ds (PApp fc ftm@(PRef ffc f) as)-        | f `elem` infns = ai qq env ds (PApp fc (PInferRef ffc f) as)+              PApp fc (PInferRef ffc hl f) as'+    ai qq env ds (PApp fc ftm@(PRef ffc hl f) as)+        | f `elem` infns = ai qq env ds (PApp fc (PInferRef ffc hl f) as)         | not (f `elem` map fst env)                           = let as' = map (fmap (ai qq env ds)) as in                                 handleErr $ aiFn inpat False qq imp_meths ist fc f ffc ds as'@@ -1586,15 +1616,16 @@                        sc' = ai qq ((n, Just ty):env) ds sc in                        PLam fc n nfc ty' sc'              _ -> ai qq env ds (PLam fc (sMN 0 "lamp") NoFC ty-                                     (PCase fc (PRef fc (sMN 0 "lamp") )-                                        [(PRef fc n, sc)]))+                                     (PCase fc (PRef fc [] (sMN 0 "lamp") )+                                        [(PRef fc [] n, sc)]))     ai qq env ds (PLet fc n nfc ty val sc)       = case lookupDef n (tt_ctxt ist) of              [] -> let ty' = ai qq env ds ty                        val' = ai qq env ds val                        sc' = ai qq ((n, Just ty):env) ds sc in                        PLet fc n nfc ty' val' sc'-             _ -> ai qq env ds (PCase fc val [(PRef fc n, sc)])+             defs ->+               ai qq env ds (PCase fc val [(PRef fc [] n, sc)])     ai qq env ds (PPi p n nfc ty sc)       = let ty' = ai qq env ds ty             env' = if n `elem` imp_meths then env@@ -1613,7 +1644,8 @@     ai qq env ds (PQuasiquote tm g) = PQuasiquote (ai True env ds tm)                                                   (fmap (ai True env ds) g)     ai qq env ds (PUnquote tm) = PUnquote (ai False env ds tm)-    ai qq env ds (PRunElab fc tm) = PRunElab fc (ai False env ds tm)+    ai qq env ds (PRunElab fc tm ns) = PRunElab fc (ai False env ds tm) ns+    ai qq env ds (PConstSugar fc tm) = PConstSugar fc (ai qq env ds tm)     ai qq env ds tm = tm      handleErr (Left err) = PElabError err@@ -1652,7 +1684,7 @@           vname _ = False  aiFn inpat expat qq imp_meths ist fc f ffc ds as-    | f `elem` primNames = Right $ PApp fc (PRef ffc f) as+    | f `elem` primNames = Right $ PApp fc (PRef ffc [ffc] f) as aiFn inpat expat qq imp_meths ist fc f ffc ds as           -- This is where namespaces get resolved by adding PAlternative      = do let ns = lookupCtxtName f (idris_implicits ist)@@ -1661,13 +1693,13 @@                          [] -> nh                          x -> x           case ns' of-            [(f',ns)] -> Right $ mkPApp fc (length ns) (PRef ffc (isImpName f f')) (insertImpl ns as)+            [(f',ns)] -> Right $ mkPApp fc (length ns) (PRef ffc [ffc] (isImpName f f')) (insertImpl ns as)             [] -> if f `elem` (map fst (idris_metavars ist))-                    then Right $ PApp fc (PRef ffc f) as-                    else Right $ mkPApp fc (length as) (PRef ffc f) as+                    then Right $ PApp fc (PRef ffc [ffc] f) as+                    else Right $ mkPApp fc (length as) (PRef ffc [ffc] f) as             alts -> Right $-                         PAlternative (ExactlyOne True) $-                           map (\(f', ns) -> mkPApp fc (length ns) (PRef ffc (isImpName f f'))+                         PAlternative [] (ExactlyOne True) $+                           map (\(f', ns) -> mkPApp fc (length ns) (PRef ffc [ffc] (isImpName f f'))                                                   (insertImpl ns as)) alts   where     -- if the name is in imp_meths, we should actually refer to the bound@@ -1694,9 +1726,9 @@     insertImpl :: [PArg] -- ^ expected argument types (from idris_implicits)                -> [PArg] -- ^ given arguments                -> [PArg]-    insertImpl ps as +    insertImpl ps as         = let (as', badimpls) = partition (impIn ps) as in-              map addUnknownImp badimpls ++ +              map addUnknownImp badimpls ++               insImpAcc M.empty ps (filter expArg as') (filter (not . expArg) as')      insImpAcc :: M.Map Name PTerm -- accumulated param names & arg terms@@ -1715,7 +1747,7 @@         case find n imps [] of             Just (tm, imps') ->               PImp p False l n tm : insImpAcc (M.insert n tm pnas) ps given imps'-            Nothing -> let ph = if f `elem` imp_meths then PRef fc n else Placeholder in+            Nothing -> let ph = if f `elem` imp_meths then PRef fc [] n else Placeholder in               PImp p True l n ph :                 insImpAcc (M.insert n ph pnas) ps given imps     insImpAcc pnas (PTacImplicit p l n sc' ty : ps) given imps =@@ -1741,7 +1773,7 @@     find n (PTacImplicit _ _ n' _ t : gs) acc          | n == n' = Just (t, reverse acc ++ gs)     find n (g : gs) acc = find n gs (g : acc)-    + -- return True if the second argument is an implicit argument which is -- expected in the implicits, or if it's not an implicit impIn :: [PArg] -> PArg -> Bool@@ -1758,14 +1790,14 @@ stripLinear :: IState -> PTerm -> PTerm stripLinear i tm = evalState (sl tm) [] where     sl :: PTerm -> State [Name] PTerm-    sl (PRef fc f)+    sl (PRef fc hl f)          | (_:_) <- lookupTy f (tt_ctxt i)-              = return $ PRef fc f+              = return $ PRef fc hl f          | otherwise = do ns <- get                           if (f `elem` ns)-                             then return $ PHidden (PRef fc f) -- Placeholder+                             then return $ PHidden (PRef fc hl f) -- Placeholder                              else do put (f : ns)-                                     return (PRef fc f)+                                     return (PRef fc hl f)     sl (PPatvar fc f)                      = do ns <- get                           if (f `elem` ns)@@ -1773,22 +1805,22 @@                              else do put (f : ns)                                      return (PPatvar fc f)     -- Assumption is that variables are all the same in each alternative-    sl t@(PAlternative b as) = do ns <- get-                                  as' <- slAlts ns as-                                  return (PAlternative b as')+    sl t@(PAlternative ms b as) = do ns <- get+                                     as' <- slAlts ns as+                                     return (PAlternative ms b as')        where slAlts ns (a : as) = do put ns                                      a' <- sl a                                      as' <- slAlts ns as                                      return (a' : as')              slAlts ns [] = return []-    sl (PPair fc p l r) = do l' <- sl l; r' <- sl r; return (PPair fc p l' r')-    sl (PDPair fc p l t r) = do l' <- sl l-                                t' <- sl t-                                r' <- sl r-                                return (PDPair fc p l' t' r')+    sl (PPair fc hls p l r) = do l' <- sl l; r' <- sl r; return (PPair fc hls p l' r')+    sl (PDPair fc hls p l t r) = do l' <- sl l+                                    t' <- sl t+                                    r' <- sl r+                                    return (PDPair fc hls p l' t' r')     sl (PApp fc fn args) = do fn' <- case fn of                                      -- Just the args, fn isn't matchable as a var-                                          PRef _ _ -> return fn+                                          PRef _ _ _ -> return fn                                           t -> sl t                               args' <- mapM slA args                               return $ PApp fc fn' args'@@ -1810,10 +1842,14 @@ stripUnmatchable :: IState -> PTerm -> PTerm stripUnmatchable i (PApp fc fn args) = PApp fc fn (fmap (fmap su) args) where     su :: PTerm -> PTerm-    su (PRef fc f)+    su tm@(PRef fc hl f)        | (Bind n (Pi _ t _) sc :_) <- lookupTy f (tt_ctxt i)           = Placeholder-    su (PApp fc f@(PRef _ fn) args)+       | (TType _ : _) <- lookupTy f (tt_ctxt i)+          = PHidden tm+       | (UType _ : _) <- lookupTy f (tt_ctxt i)+          = PHidden tm+    su (PApp fc f@(PRef _ _ fn) args)        -- here we use canBeDConName because the impossible pattern        -- check will not necessarily fully resolve constructor names,        -- and these bare names will otherwise get in the way of@@ -1822,14 +1858,15 @@           = PApp fc f (fmap (fmap su) args)     su (PApp fc f args)           = PHidden (PApp fc f args)-    su (PAlternative b alts)+    su (PAlternative ms b alts)        = let alts' = filter (/= Placeholder) (map su alts) in              if null alts' then Placeholder-                           else PAlternative b alts'-    su (PPair fc p l r) = PPair fc p (su l) (su r)-    su (PDPair fc p l t r) = PDPair fc p (su l) (su t) (su r)+                           else PAlternative ms b alts'+    su (PPair fc hls p l r) = PPair fc hls p (su l) (su r)+    su (PDPair fc hls p l t r) = PDPair fc hls p (su l) (su t) (su r)     su t@(PLam fc _ _ _ _) = PHidden t     su t@(PPi _ _ _ _ _) = PHidden t+    su t@(PConstant _ c) | isTypeConst c = PHidden t     su t = t      ctxt = tt_ctxt i@@ -1850,9 +1887,8 @@ -- FIXME: It's possible that this really has to happen after elaboration  findStatics :: IState -> PTerm -> (PTerm, [Bool])-findStatics ist tm = trace (show tm) $-                      let (ns, ss) = fs tm in-                         runState (pos ns ss tm) []+findStatics ist tm = let (ns, ss) = fs tm+                     in runState (pos ns ss tm) []   where fs (PPi p n fc t sc)             | Static <- pstatic p                         = let (ns, ss) = fs sc in@@ -1903,24 +1939,24 @@     fullApp x = x      match' x y = match (fullApp x) (fullApp y)-    match (PApp _ (PRef _ (NS (UN fi) [b])) [_,_,x]) x'+    match (PApp _ (PRef _ _ (NS (UN fi) [b])) [_,_,x]) x'         | fi == txt "fromInteger" && b == txt "builtins",           PConstant _ (I _) <- getTm x = match (getTm x) x'-    match x' (PApp _ (PRef _ (NS (UN fi) [b])) [_,_,x])+    match x' (PApp _ (PRef _ _ (NS (UN fi) [b])) [_,_,x])         | fi == txt "fromInteger" && b == txt "builtins",           PConstant _ (I _) <- getTm x = match (getTm x) x'-    match (PApp _ (PRef _ (UN l)) [_,x]) x' | l == txt "lazy" = match (getTm x) x'-    match x (PApp _ (PRef _ (UN l)) [_,x']) | l == txt "lazy" = match x (getTm x')+    match (PApp _ (PRef _ _ (UN l)) [_,x]) x' | l == txt "lazy" = match (getTm x) x'+    match x (PApp _ (PRef _ _ (UN l)) [_,x']) | l == txt "lazy" = match x (getTm x')     match (PApp _ f args) (PApp _ f' args')         | length args == length args'             = do mf <- match' f f'                  ms <- zipWithM matchArg args args'                  return (mf ++ concat ms)-    match (PRef f n) (PApp _ x []) = match (PRef f n) x-    match (PPatvar f n) xr = match (PRef f n) xr-    match xr (PPatvar f n) = match xr (PRef f n)-    match (PApp _ x []) (PRef f n) = match x (PRef f n)-    match (PRef _ n) tm@(PRef _ n')+    match (PRef f hl n) (PApp _ x []) = match (PRef f hl n) x+    match (PPatvar f n) xr = match (PRef f [f] n) xr+    match xr (PPatvar f n) = match xr (PRef f [f] n)+    match (PApp _ x []) (PRef f hl n) = match x (PRef f hl n)+    match (PRef _ _ n) tm@(PRef _ _ n')         | n == n' && not names &&           (not (isConName n (tt_ctxt i) || isFnName n (tt_ctxt i))                 || tm == Placeholder)@@ -1929,7 +1965,7 @@         | n == n' || n == dropNS n' || dropNS n == n' = return []        where dropNS (NS n _) = n              dropNS n = n-    match (PRef _ n) tm+    match (PRef _ _ n) tm         | not names && (not (isConName n (tt_ctxt i) ||                              isFnName n (tt_ctxt i)) || tm == Placeholder)             = return [(n, tm)]@@ -1942,24 +1978,24 @@                                            return (ml ++ mr)     match (PTyped l r) x = match l x     match x (PTyped l r) = match x l-    match (PPair _ _ l r) (PPair _ _ l' r') = do ml <- match' l l'-                                                 mr <- match' r r'-                                                 return (ml ++ mr)-    match (PDPair _ _ l t r) (PDPair _ _ l' t' r') = do ml <- match' l l'-                                                        mt <- match' t t'-                                                        mr <- match' r r'-                                                        return (ml ++ mt ++ mr)-    match (PAlternative a as) (PAlternative a' as')+    match (PPair _ _ _ l r) (PPair _ _ _ l' r') = do ml <- match' l l'+                                                     mr <- match' r r'+                                                     return (ml ++ mr)+    match (PDPair _ _ _ l t r) (PDPair _ _ _ l' t' r') = do ml <- match' l l'+                                                            mt <- match' t t'+                                                            mr <- match' r r'+                                                            return (ml ++ mt ++ mr)+    match (PAlternative _ a as) (PAlternative _ a' as')         = do ms <- zipWithM match' as as'              return (concat ms)-    match a@(PAlternative _ as) b+    match a@(PAlternative _ _ as) b         = do let ms = zipWith match' as (repeat b)              case (rights (map toEither ms)) of                 (x: _) -> return x                 _ -> LeftErr (a, b)     match (PCase _ _ _) _ = return [] -- lifted out     match (PMetavar _ _) _ = return [] -- modified-    match (PInferRef _ _) _ = return [] -- modified+    match (PInferRef _ _ _) _ = return [] -- modified     match (PQuote _) _ = return []     match (PProof _) _ = return []     match (PTactics _) _ = return []@@ -2017,13 +2053,13 @@  substMatchShadow :: Name -> [Name] -> PTerm -> PTerm -> PTerm substMatchShadow n shs tm t = sm shs t where-    sm xs (PRef _ n') | n == n' = tm+    sm xs (PRef _ _ n') | n == n' = tm     sm xs (PLam fc x xfc t sc) = PLam fc x xfc (sm xs t) (sm xs sc)     sm xs (PPi p x fc t sc)          | x `elem` xs              = let x' = nextName x in-                   PPi p x' fc (sm (x':xs) (substMatch x (PRef emptyFC x') t))-                               (sm (x':xs) (substMatch x (PRef emptyFC x') sc))+                   PPi p x' fc (sm (x':xs) (substMatch x (PRef emptyFC [] x') t))+                               (sm (x':xs) (substMatch x (PRef emptyFC [] x') sc))          | otherwise = PPi p x fc (sm xs t) (sm (x : xs) sc)     sm xs (PApp f x as) = fullApp $ PApp f (sm xs x) (map (fmap (sm xs)) as)     sm xs (PCase f x as) = PCase f (sm xs x) (map (pmap (sm xs)) as)@@ -2031,13 +2067,14 @@     sm xs (PRewrite f x y tm) = PRewrite f (sm xs x) (sm xs y)                                            (fmap (sm xs) tm)     sm xs (PTyped x y) = PTyped (sm xs x) (sm xs y)-    sm xs (PPair f p x y) = PPair f p (sm xs x) (sm xs y)-    sm xs (PDPair f p x t y) = PDPair f p (sm xs x) (sm xs t) (sm xs y)-    sm xs (PAlternative a as) = PAlternative a (map (sm xs) as)+    sm xs (PPair f hls p x y) = PPair f hls p (sm xs x) (sm xs y)+    sm xs (PDPair f hls p x t y) = PDPair f hls p (sm xs x) (sm xs t) (sm xs y)+    sm xs (PAlternative ms a as) = PAlternative ms a (map (sm xs) as)     sm xs (PHidden x) = PHidden (sm xs x)     sm xs (PUnifyLog x) = PUnifyLog (sm xs x)     sm xs (PNoImplicits x) = PNoImplicits (sm xs x)-    sm xs (PRunElab fc script) = PRunElab fc (sm xs script)+    sm xs (PRunElab fc script ns) = PRunElab fc (sm xs script) ns+    sm xs (PConstSugar fc tm) = PConstSugar fc (sm xs tm)     sm xs x = x      fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))@@ -2045,7 +2082,7 @@  shadow :: Name -> Name -> PTerm -> PTerm shadow n n' t = sm t where-    sm (PRef fc x) | n == x = PRef fc n'+    sm (PRef fc hl x) | n == x = PRef fc hl n'     sm (PLam fc x xfc t sc) | n /= x = PLam fc x xfc (sm t) (sm sc)                             | otherwise = PLam fc x xfc (sm t) sc     sm (PPi p x fc t sc) | n /= x = PPi p x fc (sm t) (sm sc)@@ -2058,9 +2095,9 @@     sm (PIfThenElse fc c t f) = PIfThenElse fc (sm c) (sm t) (sm f)     sm (PRewrite f x y tm) = PRewrite f (sm x) (sm y) (fmap sm tm)     sm (PTyped x y) = PTyped (sm x) (sm y)-    sm (PPair f p x y) = PPair f p (sm x) (sm y)-    sm (PDPair f p x t y) = PDPair f p (sm x) (sm t) (sm y)-    sm (PAlternative a as) = PAlternative a (map sm as)+    sm (PPair f hls p x y) = PPair f hls p (sm x) (sm y)+    sm (PDPair f hls p x t y) = PDPair f hls p (sm x) (sm t) (sm y)+    sm (PAlternative ms a as) = PAlternative ms a (map sm as)     sm (PTactics ts) = PTactics (map (fmap sm) ts)     sm (PProof ts) = PProof (map (fmap sm) ts)     sm (PHidden x) = PHidden (sm x)@@ -2068,16 +2105,19 @@     sm (PNoImplicits x) = PNoImplicits (sm x)     sm x = x --- Rename any binders which are repeated (so that we don't have to mess+-- | Rename any binders which are repeated (so that we don't have to mess -- about with shadowing anywhere else).+mkUniqueNames :: [Name] -> [(Name, Name)] -> PTerm -> PTerm+mkUniqueNames env shadows tm +      = evalState (mkUniq initMap tm) (S.fromList env) where -mkUniqueNames :: [Name] -> PTerm -> PTerm-mkUniqueNames env tm = evalState (mkUniq tm) (S.fromList env) where+  initMap = M.fromList shadows+   inScope :: S.Set Name   inScope = S.fromList $ boundNamesIn tm -  mkUniqA arg = do t' <- mkUniq (getTm arg)-                   return (arg { getTm = t' })+  mkUniqA nmap arg = do t' <- mkUniq nmap (getTm arg)+                        return (arg { getTm = t' })    -- Initialise the unique name with the environment length (so we're not   -- looking for too long...)@@ -2087,84 +2127,95 @@    -- FIXME: Probably ought to do this for completeness! It's fine as   -- long as there are no bindings inside tactics though.-  mkUniqT tac = return tac+  mkUniqT nmap tac = return tac -  mkUniq :: PTerm -> State (S.Set Name) PTerm-  mkUniq (PLam fc n nfc ty sc)+  mkUniq :: M.Map Name Name -> PTerm -> State (S.Set Name) PTerm+  mkUniq nmap (PLam fc n nfc ty sc)          = do env <- get               (n', sc') <-                     if n `S.member` env                        then do let n' = uniqueNameSet (initN n (S.size env))                                                       (S.union env inScope)-                               return (n', shadow n n' sc)+                               return (n', sc) -- shadow n n' sc)                        else return (n, sc)               put (S.insert n' env)-              ty' <- mkUniq ty-              sc'' <- mkUniq sc'+              let nmap' = M.insert n n' nmap+              ty' <- mkUniq nmap ty+              sc'' <- mkUniq nmap' sc'               return $! PLam fc n' nfc ty' sc''-  mkUniq (PPi p n fc ty sc)+  mkUniq nmap (PPi p n fc ty sc)          = do env <- get               (n', sc') <-                     if n `S.member` env                        then do let n' = uniqueNameSet (initN n (S.size env))                                                       (S.union env inScope)-                               return (n', shadow n n' sc)+                               return (n', sc) -- shadow n n' sc)                        else return (n, sc)               put (S.insert n' env)-              ty' <- mkUniq ty-              sc'' <- mkUniq sc'+              let nmap' = M.insert n n' nmap+              ty' <- mkUniq nmap ty+              sc'' <- mkUniq nmap' sc'               return $! PPi p n' fc ty' sc''-  mkUniq (PLet fc n nfc ty val sc)+  mkUniq nmap (PLet fc n nfc ty val sc)          = do env <- get               (n', sc') <-                     if n `S.member` env                        then do let n' = uniqueNameSet (initN n (S.size env))                                                       (S.union env inScope)-                               return (n', shadow n n' sc)+                               return (n', sc) -- shadow n n' sc)                        else return (n, sc)               put (S.insert n' env)-              ty' <- mkUniq ty; val' <- mkUniq val-              sc'' <- mkUniq sc'+              let nmap' = M.insert n n' nmap+              ty' <- mkUniq nmap ty; val' <- mkUniq nmap val+              sc'' <- mkUniq nmap' sc'               return $! PLet fc n' nfc ty' val' sc''-  mkUniq (PApp fc t args)-         = do t' <- mkUniq t-              args' <- mapM mkUniqA args+  mkUniq nmap (PApp fc t args)+         = do t' <- mkUniq nmap t+              args' <- mapM (mkUniqA nmap) args               return $! PApp fc t' args'-  mkUniq (PAppBind fc t args)-         = do t' <- mkUniq t-              args' <- mapM mkUniqA args+  mkUniq nmap (PAppBind fc t args)+         = do t' <- mkUniq nmap t+              args' <- mapM (mkUniqA nmap) args               return $! PAppBind fc t' args'-  mkUniq (PCase fc t alts)-         = do t' <- mkUniq t-              alts' <- mapM (\(x,y)-> do x' <- mkUniq x; y' <- mkUniq y+  mkUniq nmap (PCase fc t alts)+         = do t' <- mkUniq nmap t+              alts' <- mapM (\(x,y)-> do x' <- mkUniq nmap x; y' <- mkUniq nmap y                                          return (x', y')) alts               return $! PCase fc t' alts'-  mkUniq (PIfThenElse fc c t f)-         = liftM3 (PIfThenElse fc) (mkUniq c) (mkUniq t) (mkUniq f)-  mkUniq (PPair fc p l r)-         = do l' <- mkUniq l; r' <- mkUniq r-              return $! PPair fc p l' r'-  mkUniq (PDPair fc p (PRef fc' n) t sc)+  mkUniq nmap (PIfThenElse fc c t f)+         = liftM3 (PIfThenElse fc) (mkUniq nmap c) (mkUniq nmap t) (mkUniq nmap f)+  mkUniq nmap (PPair fc hls p l r)+         = do l' <- mkUniq nmap l; r' <- mkUniq nmap r+              return $! PPair fc hls p l' r'+  mkUniq nmap (PDPair fc hls p (PRef fc' hls' n) t sc)       | t /= Placeholder          = do env <- get               (n', sc') <- if n `S.member` env                               then do let n' = uniqueNameSet n (S.union env inScope)-                                      return (n', shadow n n' sc)+                                      return (n', sc) -- shadow n n' sc)                               else return (n, sc)               put (S.insert n' env)-              t' <- mkUniq t-              sc'' <- mkUniq sc'-              return $! PDPair fc p (PRef fc' n') t' sc''-  mkUniq (PDPair fc p l t r)-         = do l' <- mkUniq l; t' <- mkUniq t; r' <- mkUniq r-              return $! PDPair fc p l' t' r'-  mkUniq (PAlternative b as)-         = liftM (PAlternative b) (mapM mkUniq as)-  mkUniq (PHidden t) = liftM PHidden (mkUniq t)-  mkUniq (PUnifyLog t) = liftM PUnifyLog (mkUniq t)-  mkUniq (PDisamb n t) = liftM (PDisamb n) (mkUniq t)-  mkUniq (PNoImplicits t) = liftM PNoImplicits (mkUniq t)-  mkUniq (PProof ts) = liftM PProof (mapM mkUniqT ts)-  mkUniq (PTactics ts) = liftM PTactics (mapM mkUniqT ts)-  mkUniq (PRunElab fc ts) = liftM (PRunElab fc ) (mkUniq ts)-  mkUniq t = return t+              let nmap' = M.insert n n' nmap+              t' <- mkUniq nmap t+              sc'' <- mkUniq nmap' sc'+              return $! PDPair fc hls p (PRef fc' hls' n') t' sc''+  mkUniq nmap (PDPair fc hls p l t r)+         = do l' <- mkUniq nmap l; t' <- mkUniq nmap t; r' <- mkUniq nmap r+              return $! PDPair fc hls p l' t' r'+  mkUniq nmap (PAlternative ns b as)+         -- store the nmap and defer the rest until we've pruned the set+         -- during elaboration+         = return $ PAlternative (M.toList nmap ++ ns) b as+  mkUniq nmap (PHidden t) = liftM PHidden (mkUniq nmap t)+  mkUniq nmap (PUnifyLog t) = liftM PUnifyLog (mkUniq nmap t)+  mkUniq nmap (PDisamb n t) = liftM (PDisamb n) (mkUniq nmap t)+  mkUniq nmap (PNoImplicits t) = liftM PNoImplicits (mkUniq nmap t)+  mkUniq nmap (PProof ts) = liftM PProof (mapM (mkUniqT nmap) ts)+  mkUniq nmap (PTactics ts) = liftM PTactics (mapM (mkUniqT nmap) ts)+  mkUniq nmap (PRunElab fc ts ns) = liftM (\tm -> PRunElab fc tm ns) (mkUniq nmap ts)+  mkUniq nmap (PConstSugar fc tm) = liftM (PConstSugar fc) (mkUniq nmap tm)+  mkUniq nmap t = return (shadowAll (M.toList nmap) t)+    where+      shadowAll [] t = t+      shadowAll ((n, n') : ns) t = shadow n n' (shadowAll ns t)+