idris 0.9.19.1 → 0.9.20

raw patch · 196 files changed

+4332/−1271 lines, 196 filesdep ~vectorPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependency ranges changed: vector

API changes (from Hackage documentation)

Files

• CHANGELOG +33/−4
• CONTRIBUTING.md +1/−1
• CONTRIBUTORS +2/−0
• Makefile +1/−1
• idris.cabal +27/−4
• jsrts/Runtime-browser.js +4/−0
• libs/Makefile +6/−1
• libs/base/Control/Catchable.idr +4/−4
• libs/base/Control/IOExcept.idr +10/−19
• libs/base/Data/Fin.idr +2/−20
• libs/base/Data/HVect.idr +9/−9
• libs/base/Data/String.idr +54/−0
• libs/base/Data/Vect.idr +5/−5
• libs/base/Debug/Error.idr +1/−1
• libs/base/Language/Reflection/Utils.idr +13/−19
• libs/base/base.ipkg +2/−2
• libs/contrib/Data/Heap.idr +10/−19
• libs/contrib/Network/Socket.idr +0/−4
• libs/effects/Effect/Exception.idr +2/−1
• libs/effects/Effect/File.idr +74/−29
• libs/effects/Effect/Logging/Category.idr +0/−3
• libs/effects/Effect/Perf.idr +230/−0
• libs/effects/Effect/Random.idr +7/−7
• libs/effects/Effects.idr +34/−27
• libs/effects/effects.ipkg +1/−0
• libs/prelude/IO.idr +15/−6
• libs/prelude/Language/Reflection.idr +90/−55
• libs/prelude/Language/Reflection/Elab.idr +203/−152
• libs/prelude/Prelude.idr +1/−0
• libs/prelude/Prelude/Applicative.idr +4/−0
• libs/prelude/Prelude/File.idr +81/−44
• libs/prelude/Prelude/Functor.idr +10/−8
• libs/prelude/Prelude/Interactive.idr +41/−14
• libs/prelude/Prelude/Monad.idr +1/−1
• libs/prelude/Prelude/Nat.idr +10/−10
• libs/prelude/Prelude/Show.idr +5/−0
• libs/prelude/Prelude/Stream.idr +9/−0
• libs/prelude/prelude.ipkg +1/−1
• libs/pruviloj/Makefile +21/−0
• libs/pruviloj/Pruviloj.idr +8/−0
• libs/pruviloj/Pruviloj/Core.idr +268/−0
• libs/pruviloj/Pruviloj/Derive/DecEq.idr +198/−0
• libs/pruviloj/Pruviloj/Derive/Eliminators.idr +268/−0
• libs/pruviloj/Pruviloj/Disjoint.idr +85/−0
• libs/pruviloj/Pruviloj/Induction.idr +157/−0
• libs/pruviloj/Pruviloj/Injective.idr +122/−0
• libs/pruviloj/Pruviloj/Internals.idr +154/−0
• libs/pruviloj/Pruviloj/Internals/TyConInfo.idr +108/−0
• libs/pruviloj/Pruviloj/Renamers.idr +42/−0
• libs/pruviloj/pruviloj.ipkg +13/−0
• rts/idris_main.c +1/−0
• rts/idris_rts.c +16/−0
• rts/idris_rts.h +8/−0
• rts/idris_stdfgn.c +20/−0
• rts/idris_stdfgn.h +2/−0
• src/IRTS/CodegenC.hs +3/−3
• src/IRTS/CodegenJavaScript.hs +14/−6
• src/IRTS/Compiler.hs +2/−2
• src/Idris/AbsSyntax.hs +27/−7
• src/Idris/AbsSyntaxTree.hs +11/−5
• src/Idris/CaseSplit.hs +59/−32
• src/Idris/Chaser.hs +80/−37
• src/Idris/CmdOptions.hs +2/−0
• src/Idris/Completion.hs +2/−8
• src/Idris/Core/Binary.hs +27/−22
• src/Idris/Core/DeepSeq.hs +9/−6
• src/Idris/Core/Elaborate.hs +6/−6
• src/Idris/Core/Evaluate.hs +10/−1
• src/Idris/Core/Execute.hs +11/−0
• src/Idris/Core/ProofState.hs +16/−8
• src/Idris/Core/TT.hs +52/−25
• src/Idris/Core/Typecheck.hs +0/−3
• src/Idris/Core/Unify.hs +1/−1
• src/Idris/Core/WHNF.hs +8/−8
• src/Idris/Coverage.hs +2/−2
• src/Idris/DSL.hs +1/−1
• src/Idris/DataOpts.hs +0/−1
• src/Idris/DeepSeq.hs +6/−3
• src/Idris/Delaborate.hs +18/−4
• src/Idris/Directives.hs +4/−1
• src/Idris/Elab/Class.hs +1/−1
• src/Idris/Elab/Clause.hs +78/−58
• src/Idris/Elab/Data.hs +19/−9
• src/Idris/Elab/Instance.hs +1/−1
• src/Idris/Elab/Record.hs +1/−1
• src/Idris/Elab/Term.hs +163/−104
• src/Idris/Elab/Transform.hs +1/−1
• src/Idris/Elab/Type.hs +5/−4
• src/Idris/Elab/Utils.hs +16/−0
• src/Idris/Elab/Value.hs +2/−1
• src/Idris/IBC.hs +11/−4
• src/Idris/Interactive.hs +34/−17
• src/Idris/ParseData.hs +12/−2
• src/Idris/ParseExpr.hs +13/−3
• src/Idris/ParseHelpers.hs +2/−1
• src/Idris/Parser.hs +32/−12
• src/Idris/ProofSearch.hs +16/−9
• src/Idris/Prover.hs +24/−20
• src/Idris/REPL.hs +44/−24
• src/Idris/REPLParser.hs +26/−13
• src/Idris/Reflection.hs +36/−40
• src/Pkg/PParser.hs +81/−31
• src/Pkg/Package.hs +3/−6
• src/Util/System.hs +4/−3
• test/basic002/expected +4/−0
• test/basic002/run +1/−1
• test/basic002/test006.idr +8/−8
• test/basic006/expected +4/−1
• test/basic009/expected +4/−1
• test/basic010/Main.idr +13/−13
• test/basic010/expected +3/−3
• test/basic016/CycleA.idr +4/−0
• test/basic016/CycleB.idr +5/−0
• test/basic016/CycleC.idr +4/−0
• test/basic016/expected +1/−0
• test/basic016/run +3/−0
• test/docs003/expected +5/−3
• test/dsl001/test001.idr +10/−10
• test/dsl002/Resimp.idr +15/−15
• test/dsl002/test014.idr +6/−5
• test/effects003/expected +2/−0
• test/effects003/hangman.idr +5/−1
• test/effects003/run +1/−1
• test/error003/expected +4/−1
• test/error004/expected +8/−2
• test/error005/expected +20/−5
• test/ffi004/test026.idr +2/−1
• test/interactive001/expected +6/−0
• test/interactive001/input +2/−0
• test/interactive001/test032.idr +9/−0
• test/interactive010/expected +22/−0
• test/interactive010/input +10/−0
• test/interactive010/run +2/−0
• test/io001/test004.idr +4/−4
• test/meta002/AgdaStyleReflection.idr +247/−0
• test/meta002/Deriving.idr +31/−0
• test/meta002/Tacs.idr +12/−4
• test/meta002/expected +9/−2
• test/meta002/run +3/−1
• test/pkg001/Main.idr +8/−0
• test/pkg001/expected +0/−0
• test/pkg001/run +3/−0
• test/pkg001/test.ipkg +7/−0
• test/proof001/expected +4/−0
• test/proof001/run +1/−1
• test/proof002/expected +9/−1
• test/proof003/Parity.idr +6/−6
• test/proof003/expected +12/−0
• test/proof003/run +1/−1
• test/proof003/test015.idr +22/−22
• test/proof005/DefaultArgSubstitutionSuccess.idr +4/−4
• test/proof006/DefaultArgSubstitutionSyntax.idr +4/−4
• test/proof007/expected +3/−1
• test/proof008/expected +2/−0
• test/proof008/run +1/−1
• test/proof009/expected +1/−0
• test/proofsearch002/Process.idr +3/−3
• test/pruviloj001/expected +0/−0
• test/pruviloj001/pruviloj001.idr +69/−0
• test/pruviloj001/run +3/−0
• test/quasiquote003/expected +4/−1
• test/quasiquote004/expected +9/−1
• test/quasiquote006/expected +9/−3
• test/reg001/reg001.idr +6/−1
• test/reg006/expected +1/−1
• test/reg007/expected +4/−1
• test/reg017/expected +4/−0
• test/reg017/run +1/−1
• test/reg023/expected +4/−1
• test/reg028/expected +2/−0
• test/reg035/reg035a.lidr +5/−5
• test/reg041/expected +1/−1
• test/reg041/ott.idr +23/−23
• test/reg044/expected +6/−1
• test/reg046/reg046.idr +7/−7
• test/reg047/reg047.idr +2/−2
• test/reg047/reg047a.idr +3/−3
• test/reg049/expected +4/−1
• test/sourceLocation001/expected +8/−0
• test/sourceLocation001/run +1/−1
• test/syntax001/expected +8/−2
• test/totality002/expected +2/−0
• test/totality002/test017.idr +6/−6
• test/totality003/run +2/−2
• test/totality004/totality004.idr +7/−7
• test/totality004/totality004a.idr +7/−7
• test/totality008/expected +1/−1
• test/totality008/totality008.idr +4/−4
• test/totality009/expected +8/−8
• test/tutorial002/expected +6/−0
• test/tutorial002/run +1/−1
• test/tutorial002/tutorial002.idr +15/−15
• test/tutorial004/expected +4/−0
• test/tutorial004/run +1/−1
• test/tutorial006/expected +8/−3
• test/tutorial006/tutorial006b.idr +6/−6

@@ -9,31 +9,60 @@   for defining new names. `{n} still quotes n to an existing name in scope. * A new primitive operator prim__strSubstr for more efficient extraction of   substrings. External code generators should implement this.+* The previous syntax for tactic proofs and the previous interactive prover+  are now deprecated in favour of reflected elaboration. They will be removed+  at some point in the future. * Changed scoping rules for unbound implicits: any name which would be a   valid unbound implicit is now *always* an unbound implicit. This is much   more resilient to changes in inputs, but does require that function names   be explicitly qualified when in argument position.+* Name binding in patterns follows the same rule as name binding for implicits+  in types: names which begin with lower case letters, not applied to any+  arguments, are treated as bound pattern variables.+* Added %deprecate directive, which gives a warning and a message when a +  deprecated name is referenced.  Library updates ---------------  * The 'Neg' class now represents numeric types which can be negative. As-such, the (-) operator and 'abs' have been moved there from 'Num'.+  such, the (-) operator and 'abs' have been moved there from 'Num'. * A special version of (-) on 'Nat' requires that the second argument is-smaller than or equal to the first. 'minus' retains the old behaviour,-returning Z if there is an underflow.+  smaller than or equal to the first. 'minus' retains the old behaviour,+  returning Z if there is an underflow.+* The (+), (-), and (*) operations on Fin have been removed. * New Logging Effects have been added to facilitate logging of effectful   programmes.+* Elaborator reflection is now a part of the prelude. It is no longer+  necessary to import Language.Reflection.Elab.+* The `PERF` effect allows for simple performance metrics to be collected+  from Effectful programs.+* Some constructors that never actually occurred have been removed from+  the TT and Raw reflection datatypes in Language.Reflection.+* File IO operations (for example openFile/fread/fwrite) now return +  'Either FileError ty' where the return type was previously 'ty' to indicate+  that they may fail.  Tool updates ------------ * Records are now shown as records in :doc, rather than as the underlying   datatype+* iPKG files have a new option `pkgs` which takes a comma-separated list+  of package names that the idris project depends on. This reduces bloat+  in the `opts` option with multiple package declarations.+* iPKG files now allow `executable = "your filename here"` in addition to+  the existing `executable = yourFilenameHere` style. While the unquoted+  version is limited to filenames that look like namespaced Idris identifiers+  (`your.filename.here`), the quoted version accepts any valid filename.+* Add definition command (\d in Vim, Ctrl-Alt-A in Atom, C-c C-s in Emacs) now+  adds missing clauses if there is already a definition.  Miscellaneous updates ---------------------+* Disable the deprecation warnings for %elim and old-style tactic scripts+  with the --no-elim-deprecation-warnings and --no-tactic-deprecation-warnings+  flags. -[None so far]  New in 0.9.19: --------------

@@ -166,4 +166,4 @@ * [General GitHub Documentation](https://help.github.com/).  -Adapted from the most excellent contributing files from the [Puppet project](https://github.com/puppetlabs/puppet) and [Factroy Girl Rails](https://github.com/thoughtbot/factory_girl_rails/blob/master/CONTRIBUTING.md)+Adapted from the most excellent contributing files from the [Puppet project](https://github.com/puppetlabs/puppet) and [Factory Girl Rails](https://github.com/thoughtbot/factory_girl_rails/blob/master/CONTRIBUTING.md)

@@ -15,6 +15,7 @@ Guglielmo Fachini Simon Fowler Google+Zack Grannan Cezar Ionescu Heath Johns Irene Knapp@@ -35,6 +36,7 @@ Seo Sanghyeon Benjamin Saunders Alexander Shabalin+Jeremy W. Sherman Timo Petteri Sinnemäki JP Smith startling

@@ -43,7 +43,7 @@ 	$(CABAL) install $(CABALFLAGS)  linecount:-	wc -l src/Idris/*.hs src/Idris/Core/*.hs src/IRTS/*.hs src/Pkg/*.hs+	wc -l src/Idris/*.hs src/Idris/Elab/*.hs src/Idris/Core/*.hs src/IRTS/*.hs src/Pkg/*.hs src/Util/*.hs  #Note: this doesn't yet link to Hackage properly doc: dist/setup-config

@@ -1,5 +1,5 @@ Name:           idris-Version:        0.9.19.1+Version:        0.9.20 License:        BSD3 License-file:   LICENSE Author:         Edwin Brady@@ -140,9 +140,16 @@                        libs/effects/Makefile                        libs/effects/effects.ipkg                        libs/effects/Effect/*.idr-		       libs/effects/Effect/Logging/*.idr+		               libs/effects/Effect/Logging/*.idr                        libs/effects/*.idr +                       libs/pruviloj/Makefile+                       libs/pruviloj/pruviloj.ipkg+                       libs/pruviloj/*.idr+                       libs/pruviloj/Pruviloj/*.idr+                       libs/pruviloj/Pruviloj/Derive/*.idr+                       libs/pruviloj/Pruviloj/Internals/*.idr+                        test/Makefile                        test/runtest.pl                        test/reg001/run@@ -349,6 +356,9 @@                        test/basic015/run                        test/basic015/*.idr                        test/basic015/expected+                       test/basic016/run+                       test/basic016/*.idr+                       test/basic016/expected                         test/bignum001/run                        test/bignum001/*.idr@@ -528,6 +538,9 @@                        test/interactive009/input                        test/interactive009/*.idr                        test/interactive009/expected+                       test/interactive010/expected+                       test/interactive010/input+                       test/interactive010/run                         test/io001/run                        test/io001/*.idr@@ -560,6 +573,11 @@                        test/primitives003/*.idr                        test/primitives003/expected +                       test/pkg001/run+                       test/pkg001/test.ipkg+                       test/pkg001/*.idr+                       test/pkg001/expected+                        test/proof001/run                        test/proof001/*.idr                        test/proof001/expected@@ -591,7 +609,7 @@                        test/proof010/run                        test/proof010/*.idr                        test/proof010/expected-                       +                        test/proofsearch001/run                        test/proofsearch001/*.idr                        test/proofsearch001/expected@@ -602,6 +620,10 @@                        test/proofsearch003/*.idr                        test/proofsearch003/expected +                       test/pruviloj001/run+                       test/pruviloj001/*.idr+                       test/pruviloj001/expected+                        test/quasiquote001/run                        test/quasiquote001/*.idr                        test/quasiquote001/expected@@ -938,7 +960,7 @@                 , uniplate >=1.6 && < 1.7                 , unordered-containers < 0.3                 , utf8-string < 1.1-                , vector < 0.11+                , vector < 0.12                 , vector-binary-instances < 0.3                 , zip-archive > 0.2.3.5 && < 0.2.4                 , zlib < 0.6@@ -974,6 +996,7 @@      cpp-options:   -DIDRIS_FFI   if flag(GMP)      build-depends: libffi < 0.2+     extra-libraries: gmp      cpp-options:   -DIDRIS_GMP   if flag(curses)      build-depends: hscurses < 1.5

@@ -1,3 +1,7 @@+var i$getLine = function() {+    return prompt("Prelude.getLine");+}+ var i$putStr = function(s) {   console.log(s); };

@@ -3,6 +3,7 @@ 	$(MAKE) -C base build 	$(MAKE) -C contrib build 	$(MAKE) -C effects build+	$(MAKE) -C pruviloj build   install:@@ -10,24 +11,28 @@ 	$(MAKE) -C base install 	$(MAKE) -C contrib install 	$(MAKE) -C effects install+	$(MAKE) -C pruviloj install  clean: 	$(MAKE) -C prelude clean 	$(MAKE) -C base clean 	$(MAKE) -C contrib clean 	$(MAKE) -C effects clean+	$(MAKE) -C pruviloj clean  doc: 	$(MAKE)	-C prelude doc 	$(MAKE)	-C base doc 	$(MAKE)	-C contrib doc 	$(MAKE)	-C effects doc+	$(MAKE)	-C pruviloj doc  doc_clean: 	$(MAKE)	-C prelude doc_clean 	$(MAKE)	-C base doc_clean 	$(MAKE)	-C contrib doc_clean-	$(MAKE)	-C effects  doc_clean+	$(MAKE)	-C effects doc_clean+	$(MAKE)	-C pruviloj doc_clean   .PHONY: build install clean doc doc_clean

@@ -16,14 +16,14 @@     catch (Left err) h = h err     catch (Right x)  h = (Right x) -    throw x = Left x+    throw = Left  instance Catchable (IOExcept err) err where-    catch (ioM prog) h = ioM (do p' <- prog+    catch (IOM prog) h = IOM (do p' <- prog                                  case p' of-                                      Left e => let ioM he = h e in he+                                      Left e => let IOM he = h e in he                                       Right val => return (Right val))-    throw x = ioM (return (Left x))+    throw = ioe_fail  instance Catchable List () where     catch [] h = h ()

@@ -2,34 +2,25 @@  -- An IO monad with exception handling -data IOExcept : Type -> Type -> Type where-     ioM : IO (Either err a) -> IOExcept err a+record IOExcept err a where+     constructor IOM+     runIOExcept : IO (Either err a)  instance Functor (IOExcept e) where-     map f (ioM fn) = ioM (map (map f) fn)+     map f (IOM fn) = IOM (map (map f) fn)  instance Applicative (IOExcept e) where-     pure x = ioM (pure (pure x))-     (ioM f) <*> (ioM a) = ioM (do f' <- f; a' <- a-                                   return (f' <*> a'))+     pure x = IOM (pure (pure x))+     (IOM f) <*> (IOM a) = IOM [| f <*> a |]  instance Monad (IOExcept e) where-     (ioM x) >>= k = ioM (do x' <- x;-                             case x' of-                                  Right a => let (ioM ka) = k a in-                                                 ka-                                  Left err => return (Left err))+     (IOM x) >>= f = IOM $ x >>= either (pure . Left) (runIOExcept . f)  ioe_lift : IO a -> IOExcept err a-ioe_lift op = ioM (do op' <- op-                      return (Right op'))+ioe_lift op = IOM $ map Right op  ioe_fail : err -> IOExcept err a-ioe_fail e = ioM (return (Left e))+ioe_fail e = IOM $ pure (Left e)  ioe_run : IOExcept err a -> (err -> IO b) -> (a -> IO b) -> IO b-ioe_run (ioM act) err ok = do act' <- act-                              case act' of-                                   Left e => err e-                                   Right v => ok v-+ioe_run (IOM act) err ok = either err ok !act

@@ -42,7 +42,7 @@ finToNatInjective (FS m) FZ     Refl impossible finToNatInjective FZ     (FS n) Refl impossible finToNatInjective (FS m) (FS n) prf  =-  cong (finToNatInjective m n (succInjective (finToNat m) (finToNat n) prf)) +  cong (finToNatInjective m n (succInjective (finToNat m) (finToNat n) prf))  instance Cast (Fin n) Nat where     cast x = finToNat x@@ -94,31 +94,13 @@   compare  FZ    (FS _) = LT   compare (FS _)  FZ    = GT   compare (FS x) (FS y) = compare x y-  + instance MinBound (Fin (S n)) where   minBound = FZ  instance MaxBound (Fin (S n)) where   maxBound = last --||| Add two Fins, extending the bound-(+) : Fin n -> Fin m -> Fin (n + m)-(+) {n=S n} {m=m} FZ f' = rewrite plusCommutative n m in weaken (weakenN n f')-(+) (FS f) f' = FS (f + f')--||| Substract two Fins, keeping the bound of the minuend-(-) : Fin n -> Fin m -> Fin n-FZ - _ = FZ-f - FZ = f-(FS f) - (FS f') = weaken $ f - f'--||| Multiply two Fins, extending the bound-(*) : Fin n -> Fin m -> Fin (n * m)-(*) {n=Z} f f' = FinZElim f-(*) {m=Z} f f' = FinZElim f'-(*) {n=S n} {m=S m} FZ     f' = FZ-(*) {n=S n} {m=S m} (FS f) f' = f' + (f * f')  -- Construct a Fin from an integer literal which must fit in the given Fin 

@@ -73,17 +73,17 @@  ||| Extract an arbitrary element of the correct type. ||| @ t the goal type-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+get : HVect ts -> {auto p : Elem t ts} -> t+get (x :: xs) {p = Here} = x+get (x :: xs) {p = There p'} = get {p = p'} xs  ||| Replace an element with the correct type.-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+put : t -> HVect ts -> {auto p : Elem t ts} -> HVect ts+put y (x::xs) {p = Here} = y :: xs+put y (x::xs) {p = There p'} = x :: put {p = p'} y xs  ||| Update an element with the correct type.-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+update : (t -> u) -> HVect ts -> {auto p : Elem t ts} -> HVect (replaceByElem ts p u)+update f (x::xs) {p = Here} = f x :: xs+update f (x::xs) {p = There p'} = x :: update {p = p'} f xs 

@@ -0,0 +1,54 @@+module Data.String++||| Convert a positive number string to a Num.+|||+||| ```idris example+||| parsePositive "123"+||| ```+||| ```idris example+||| parsePositive {a=Int} " +123"+||| ```+parsePositive : Num a => String -> Maybe a+parsePositive s = parsePosTrimmed (trim s) +  where+    parsePosTrimmed s with (strM s)+      parsePosTrimmed ""             | StrNil         = Nothing+      parsePosTrimmed (strCons x xs) | (StrCons x xs) = +        if (x == '+') +          then map fromInteger (parsePosAux (unpack xs) 0)+          else map fromInteger (parsePosAux (unpack xs)  (cast (ord x - ord '0')))+            where+              parsePosAux : List Char -> Integer -> Maybe Integer+              parsePosAux []        acc = Just acc+              parsePosAux (c :: cs) acc = +                if (c >= '0' && c <= '9') +                  then parsePosAux cs ((acc * 10) + (cast ((ord c) - (ord '0'))))+                  else Nothing+++||| Convert a number string to a Num.+|||+||| ```idris example+||| parseInteger " 123"+||| ```+||| ```idris example+||| parseInteger {a=Int} " -123"+||| ```+parseInteger : (Num a, Neg a) => String -> Maybe a+parseInteger s = parseIntTrimmed (trim s) +  where+    parseIntTrimmed s with (strM s)+      parseIntTrimmed ""             | StrNil         = Nothing+      parseIntTrimmed (strCons x xs) | (StrCons x xs) = +        if (x == '-') +          then map (\y => negate (fromInteger y)) (parseIntegerAux (unpack xs) 0)+          else if (x == '+') +            then map fromInteger (parseIntegerAux (unpack xs) (cast {from=Int} 0))+            else map fromInteger (parseIntegerAux (unpack xs) (cast (ord x - ord '0')))+              where+                parseIntegerAux : List Char -> Integer -> Maybe Integer+                parseIntegerAux []        acc = Just acc+                parseIntegerAux (c :: cs) acc = +                  if (c >= '0' && c <= '9') +                    then parseIntegerAux cs ((acc * 10) + (cast ((ord c) - (ord '0'))))+                    else Nothing

@@ -614,11 +614,11 @@ ||| @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+exactLength : {m : Nat} -> -- expected at run-time+              (len : Nat) -> (xs : Vect m a) -> Maybe (Vect len a)+exactLength {m} len xs with (decEq m len)+  exactLength {m = m} m xs | (Yes Refl) = Just xs+  exactLength {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

@@ -8,7 +8,7 @@ ||| @ loc     The source location to display for the error ||| @ message The error to print partial-error : {default tactics {sourceLocation} loc : SourceLocation} ->+error : {default (%runElab sourceLocation) loc : SourceLocation} ->         (message : String) ->         a error {loc = FileLoc filename (line, col) _} message =

@@ -55,13 +55,18 @@ binderTy (Lam t)       = t binderTy (Pi t _)      = t binderTy (Let t1 t2)   = t1-binderTy (NLet t1 t2)  = t1 binderTy (Hole t)      = t binderTy (GHole t)     = t binderTy (Guess t1 t2) = t1 binderTy (PVar t)      = t binderTy (PVTy t)      = t +instance Show SourceLocation where+  showPrec d (FileLoc filename line col) = showCon d "FileLoc" $ showArg filename ++ showArg line ++ showArg col++instance Eq SourceLocation where+  (FileLoc fn s e) == (FileLoc fn' s' e') = fn == fn' && s == s' && e == e'+ mutual   instance Show SpecialName where     showPrec d (WhereN i n1 n2) = showCon d "WhereN" $ showArg i ++@@ -70,7 +75,7 @@     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 (CaseN fc n) = showCon d "CaseN" $ showArg fc ++ 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@@ -80,14 +85,12 @@     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     (UN str1)  == (UN str2)     = str1 == str2     (NS n ns)  == (NS n' ns')   = n == n' && ns == ns'     (MN i str) == (MN i' str')  = i == i' && str == str'-    NErased    == NErased       = True     (SN sn)    == (SN sn')      = assert_total $ sn == sn'     x          == y             = False @@ -97,7 +100,7 @@     (InstanceN i ss)    == (InstanceN i' ss')    = i == i' && ss == ss'     (ParentN n s)       == (ParentN n' s')       = n == n' && s == s'     (MethodN n)         == (MethodN n')          = n == n'-    (CaseN n)           == (CaseN n')            = n == n'+    (CaseN fc n)        == (CaseN fc' n')        = fc == fc' && n == n'     (ElimN n)           == (ElimN n')            = n == n'     (InstanceCtorN n)   == (InstanceCtorN n')    = n == n'     (MetaN parent meta) == (MetaN parent' meta') = parent == parent' && meta == meta'@@ -196,7 +199,6 @@   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@@ -207,7 +209,6 @@   (Lam t)       == (Lam t')         = t == t'   (Pi t k)      == (Pi t' k')       = t == t' && k == k'   (Let t1 t2)   == (Let t1' t2')    = t1 == t1' && t2 == t2'-  (NLet t1 t2)  == (NLet t1' t2')   = t1 == t1' && t2 == t2'   (Hole t)      == (Hole t')        = t == t'   (GHole t)     == (GHole t')       = t == t'   (Guess t1 t2) == (Guess t1' t2')  = t1 == t1' && t2 == t2'@@ -223,9 +224,7 @@           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@@ -236,9 +235,7 @@           equalp (Bind n b t) (Bind n' b' t')  = n == n' && b == b' && t == t'           equalp (App t1 t2)  (App t1' t2')    = t1 == t1' && t2 == t2'           equalp (TConst c)   (TConst c')      = c == c'-          equalp (Proj tm i)  (Proj tm' i')    = tm == tm' && i == i'           equalp Erased       Erased           = True-          equalp Impossible   Impossible       = True           equalp (TType u)    (TType u')       = u == u'           equalp x            y                = False @@ -260,17 +257,17 @@         LT => Nothing         GT => atIndex xs (n-1) -    %assert_total     fe : List TTName -> TT -> Maybe Raw     fe env (P _ n _)     = Just $ Var n-    fe env (V i)         = map Var (atIndex env i)-    fe env (Bind n b sc) = [| RBind (pure n) (traverse (fe env) b) (fe (n::env) sc) |]+    fe env (V i)         = [| Var (atIndex env i) |]+    fe env (Bind n b sc) = [| RBind (pure n)+                                    (assert_total $ traverse (fe env) b)+                                    (fe (n::env) sc) |]     fe env (App f a)     = [| RApp (fe env f) (fe env a) |]     fe env (TConst c)    = Just $ RConstant c-    fe env (Proj tm i)   = Nothing -- runtime only, not useful for metaprogramming     fe env (TType i)     = Just RType+    fe env (UType uni)   = Just (RUType uni)     fe env Erased        = Just $ RConstant Forgot-    fe env Impossible    = Nothing  instance Show Raw where   showPrec = my_show@@ -279,11 +276,8 @@           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-  showPrec d (FileLoc filename line col) = showCon d "FileLoc" $ showArg filename ++ showArg line ++ showArg col  instance Show Err where   showPrec d (Msg x) = showCon d "Msg" $ showArg x

@@ -1,6 +1,6 @@ package base -opts = "--nobasepkgs --total -i ../prelude"+opts = "--nobasepkgs --total --no-elim-deprecation-warnings -i ../prelude" modules = System,            Debug.Error, Debug.Trace,@@ -17,7 +17,7 @@           Data.HVect, Data.Vect.Quantifiers,           Data.Complex,           Data.Erased, Data.List,-          Data.So,+          Data.So, Data.String,            Control.Isomorphism,           Control.Monad.Identity,

@@ -133,21 +133,21 @@ -- Properties -------------------------------------------------------------------------------- -total absurdBoolDischarge : False = True -> Void-absurdBoolDischarge p = replace {P = disjointTy} p ()-  where-    total disjointTy : Bool -> Type-    disjointTy False  = ()-    disjointTy True   = Void+total+absurdBoolDischarge : False = True -> Void+absurdBoolDischarge Refl impossible -total isEmptySizeZero : (h : MaxiphobicHeap a) -> (isEmpty h = True) -> size h = Z+total+isEmptySizeZero : (h : MaxiphobicHeap a) -> (isEmpty h = True) -> size h = Z isEmptySizeZero Empty          p = Refl-isEmptySizeZero (Node s l e r) p = ?isEmptySizeZeroNodeAbsurd+isEmptySizeZero (Node s l e r) Refl impossible -total emptyHeapValid : Ord a => isValidHeap (empty {a}) = True+total+emptyHeapValid : Ord a => isValidHeap (empty {a}) = True emptyHeapValid = Refl -total singletonHeapValid : Ord a => (e : a) -> isValidHeap $ singleton e = True+total+singletonHeapValid : Ord a => (e : a) -> isValidHeap $ singleton e = True singletonHeapValid e = Refl  {-@@ -161,16 +161,7 @@   ?mergePreservesValidHeapsBody -} ------------------------------------------------------------------------------------ Proofs--------------------------------------------------------------------------------- -isEmptySizeZeroNodeAbsurd = proof {-    intros;-    refine void;-    refine absurdBoolDischarge;-    exact p;-}  -------------------------------------------------------------------------------- -- Debug

@@ -143,10 +143,6 @@   socketType : SocketType   protocalNumber : ProtocolNumber -||| Get the C error number-getErrno : IO Int-getErrno = foreign FFI_C "idrnet_errno" (IO Int)- ||| Creates a UNIX socket with the given family, socket type and protocol ||| number. Returns either a socket or an error. socket : SocketFamily -> SocketType -> ProtocolNumber -> IO (Either SocketError Socket)

@@ -18,7 +18,7 @@                                believe_me (exit 1)  instance Handler (Exception a) (IOExcept a) where-     handle _ (Raise e) k = ioM (return (Left e))+     handle _ (Raise e) k = ioe_fail e  instance Handler (Exception a) (Either a) where      handle _ (Raise e) k = Left e@@ -28,3 +28,4 @@  raise : a -> Eff b [EXCEPTION a] raise err = call $ Raise err+

@@ -8,8 +8,8 @@ ||| A Dependent type to describe File Handles. File handles are ||| parameterised with the current state of the file: Closed; Open for ||| reading; and Open for writing.-||| -||| @ m The file mode. +|||+||| @ m The file mode. data OpenFile : (m : Mode) -> Type where      FH : File -> OpenFile m @@ -21,27 +21,27 @@  ||| Here the protocol for resource access is defined as an effect. ||| The state transitions diagram for the protocol is as follows:-||| +||| |||     digraph G {-||| +||| |||       empty; read; write; // States-||| +||| |||       empty -> read [label="Open R"]; |||       read -> empty [label="Close"]; |||       read -> read [label="ReadLine"]; |||       read -> read [label="EOF"];-|||           +||| |||       empty -> write [label="Open W"]; |||       write -> empty [label="Close"]; |||       write -> write [label="WriteLine"];-||| +||| |||     } data FileIO : Effect where   ||| Open a file with the specified mode.-  ||| +  |||   ||| Opening a file successful moves the state from 'empty' to the   ||| specified mode. If not successful the state is still 'empty'.-  ||| +  |||   ||| @ fname The file name to be opened.   ||| @ m The file mode.   Open : (fname: String)@@ -51,22 +51,22 @@                                              False => ())    ||| Close a file.-  ||| +  |||   ||| Closing a file moves the state from Open to closed.-  Close : sig FileIO () (OpenFile m) () +  Close : sig FileIO () (OpenFile m) ()    ||| Read a line from the file.-  ||| +  |||   ||| Only files that are open for reading can be read.   ReadLine : sig FileIO String (OpenFile Read)-  +   ||| Write a string to a file.-  ||| +  |||   ||| Only file that are open for writing can be written to.   WriteString : String -> sig FileIO () (OpenFile Write)    ||| End of file?-  ||| +  |||   ||| Only files open for reading can be tested for EOF   EOF : sig FileIO Bool (OpenFile Read) @@ -74,29 +74,33 @@  --- An implementation of the resource access protocol for the IO Context. instance Handler FileIO IO where-    handle () (Open fname m) k = do h <- openFile fname m-                                    valid <- validFile h-                                    if valid then k True (FH h) -                                             else k False ()+    handle () (Open fname m) k = do Right h <- openFile fname m+                                        | Left err => k False ()+                                    k True (FH h)     handle (FH h) Close      k = do closeFile h                                     k () ()-    handle (FH h) ReadLine        k = do str <- fread h+    handle (FH h) ReadLine        k = do Right str <- fread h+                                         -- Need proper error handling!+                                             | Left err => k "" (FH h)                                          k str (FH h)-    handle (FH h) (WriteString str) k = do fwrite h str+    handle (FH h) (WriteString str) k = do Right () <- fwrite h str+                                             | Left err => k () (FH h)                                            k () (FH h)     handle (FH h) EOF             k = do e <- feof h                                          k e (FH h)  instance Handler FileIO (IOExcept a) where-    handle () (Open fname m) k = do h <- ioe_lift $ openFile fname m-                                    valid <- ioe_lift $ validFile h-                                    if valid then k True (FH h)-                                             else k False ()+    handle () (Open fname m) k = do Right h <- ioe_lift $ openFile fname m+                                        | Left err => k False ()+                                    k True (FH h)     handle (FH h) Close      k = do ioe_lift $ closeFile h                                     k () ()-    handle (FH h) ReadLine        k = do str <- ioe_lift $ fread h+    handle (FH h) ReadLine        k = do Right str <- ioe_lift $ fread h+                                         -- Need proper error handling!+                                             | Left err => k "" (FH h)                                          k str (FH h)-    handle (FH h) (WriteString str) k = do ioe_lift $ fwrite h str+    handle (FH h) (WriteString str) k = do Right () <- ioe_lift $ fwrite h str+                                             | Left err => k () (FH h)                                            k () (FH h)     handle (FH h) EOF             k = do e <- ioe_lift $ feof h                                          k e (FH h)@@ -112,12 +116,12 @@ --  ||| Open a file with the specified mode.-||| +||| ||| @ fname The file name to be opened. ||| @ m The file mode. open : (fname : String)        -> (m : Mode)-       -> Eff Bool [FILE_IO ()] +       -> Eff Bool [FILE_IO ()]                    (\res => [FILE_IO (case res of                                            True => OpenFile m                                            False => ())])@@ -144,4 +148,45 @@ eof : Eff Bool [FILE_IO (OpenFile Read)] eof = call $ EOF +||| Read a complete file, returning a user defined error if+||| unsuccesful.+|||+readFile : (errFunc : String -> e)+        -> (fname   : String)+        -> Eff (Either e String) [FILE_IO ()]+readFile errFunc fname = do+    case !(open fname Read) of+      False => pure $ Left (errFunc fname)+      True => do+        src <- readAcc ""+        close+        pure $ Right src+  where+    readAcc : String -> Eff String [FILE_IO (OpenFile Read)]+    readAcc acc = if (not !(eof))+                     then readAcc (acc ++ !(readLine))+                     else pure acc++||| Write a file containing the provided string, returning a user+||| defined error if unsuccesful.+|||+writeFile : (errFunc : String -> e)+         -> (fname   : String)+         -> (content : String)+         -> Eff (Either e ()) [FILE_IO ()]+writeFile errFunc fname content = do+    case !(open fname Write) of+      True => do+        writeString content+        close+        pure $ Right ()+      False => pure $ Left (errFunc fname)+++namespace Default+  readFile : String -> Eff (Either String String) [FILE_IO ()]+  readFile = File.readFile id++  writeFile : String -> String -> Eff (Either String ()) [FILE_IO ()]+  writeFile = File.writeFile id -- --------------------------------------------------------------------- [ EOF ]

@@ -25,9 +25,6 @@   getLevel      : LogLevel n   getCategories : List a -instance (Show a) => Show (LogRes a) where-  show (MkLogRes l cs) = unwords ["Log Settings:", show l, show cs]- instance Default (LogRes a) where   default = MkLogRes OFF Nil 

@@ -0,0 +1,230 @@+-- ---------------------------------------------------------------- [ Perf.idr ]+-- Module    : Perf.idr+-- Copyright : (c) Jan de Muijnck-Hughes+-- License   : see LICENSE+-- --------------------------------------------------------------------- [ EOH ]+||| A naive performance effect for gathering data about the+||| performance of effectful programmes.+module Effect.Perf++import System++import Effects+import Effect.Default++%access public++-- ---------------------------------------------------- [ Timer Data Structure ]++||| A Simple timer.+record Timer where+  constructor MkTimer+  desc   : String+  start  : Integer+  stop   : Integer+  splits : List (Integer, Maybe String)++displayTimer : Timer -> String+displayTimer (MkTimer d a z bcd) = unlines+      [ unwords ["Timer:", d]+      , unwords ["\tStart:\t", show a, (displaySplits bcd)]+      , unwords ["\tStop:\t",  show z]+      , unwords ["\tDifference:\t", show (z - a)]+      ]+    where+      displaySplit : (Integer, Maybe String) -> String+      displaySplit (v, Nothing)  = with List unwords ["\tSplit:\t",show v]+      displaySplit (v, Just msg) = with List unwords ["\tSplit:\t",show v, show msg]++      displaySplits : List (Integer, Maybe String) -> String+      displaySplits Nil = ""+      displaySplits ss  = "\n" ++ unlines (map displaySplit $ reverse ss)+++defaultTimer : String -> Timer+defaultTimer n = MkTimer n 0 0 Nil++-- ---------------------------------------------------------------- [ Resource ]++||| Performance Metrics to keep during program lifetime.+record PMetrics where+  constructor MkPMetrics+  canPerf  : Bool+  livePerf : Bool+  counters : List (String, Nat)+  timers   : List (String, Timer)+  stime    : Integer+  stamps   : List (String, Integer)+++instance Default PMetrics where+  default = MkPMetrics False False Nil Nil 0 Nil++displayPerfMetrics : PMetrics -> String+displayPerfMetrics (MkPMetrics c l cs ts _ ss) =+    unlines [ "Perf Data:"+            , unlines $ map displayMarker cs+            , unlines $ map (\(x,y) => displayTimer y) ts+            , unlines $ map displayMarker ss]+  where+    displayMarker : Show a => Pair String a -> String+    displayMarker (d,v) = unwords [show v, "\t<==\t", show d]++-- ------------------------------------------------------- [ Utility functions ]++incCounter' : String -> PMetrics -> PMetrics+incCounter' x st = record {counters = cs} st+  where+    cs : List (String, Nat)+    cs = map (\(y,c) => if x == y then (y,S c) else (y,c)) (counters st)+++data TOpt = START | STOP | SPLIT++displayTimerOpt : TOpt -> String+displayTimerOpt START = "Starting"+displayTimerOpt STOP  = "Stopping"+displayTimerOpt SPLIT = "Splitting"++timerStuff' : TOpt -> Integer -> String -> Maybe String -> PMetrics -> PMetrics+timerStuff' opt val x msg st = record {timers = ts} st+  where+    doThing : (String,Timer) -> (String,Timer)+    doThing (y,t) =+      if not (x == y)+        then (y, t)+        else case opt of+          START => MkPair y $ record {start  = val} t+          STOP  => MkPair y $ record {stop   = val} t+          SPLIT => MkPair y $ record {splits = (val, msg) :: splits t} t++    ts : List (String, Timer)+    ts = map doThing (timers st)+++perfLog : PMetrics -> String -> IO ()+perfLog res msg =+    if livePerf res+      then putStrLn $ unwords ["PERF:", msg]+      else return ()++-- ------------------------------------------------------- [ Effect Definition ]++data Perf : Effect where+  GetMetrics  : sig Perf (PMetrics) (PMetrics)+  TurnOn      : Bool -> sig Perf () (PMetrics) (PMetrics)+  MkCounter   : String -> sig Perf () (PMetrics) (PMetrics)+  IncCounter  : String -> sig Perf () (PMetrics) (PMetrics)+  Timestamp   : String -> sig Perf () (PMetrics) (PMetrics)+  MkStopWatch : String -> sig Perf () (PMetrics) (PMetrics)+  TimerStuff  : TOpt -> String -> Maybe String -> sig Perf () (PMetrics) (PMetrics)++-- ---------------------------------------------------------- [ Handler for IO ]++instance Handler Perf IO where+  handle res (TurnOn b) k = do+      v <- time+      let res' = record {canPerf = True, livePerf = b, stime = v} res+      perfLog res' $ unwords [ "Turning on Perf with at", show v]+      k () (res')++  handle res (GetMetrics)  k = k res res++  handle res (MkCounter n) k = do+      if not (canPerf res)+        then k () res+        else do+          let res' = record {counters = (n,Z) :: counters res} res+          perfLog res' $ unwords ["Creating counter:", show n]+          k () (res')++  handle res (IncCounter n) k = do+      if not (canPerf res)+        then k () res+        else do+          let res' = incCounter' n res+          perfLog res' $ unwords ["Incriminating counter:", show n]+          k () (res')++  handle res (MkStopWatch n) k = do+      if not (canPerf res)+        then k () res+        else do+          let res' = record {timers = (n, defaultTimer n) :: timers res} res+          perfLog res' $ unwords ["Creating Timer:", show n]+          k () (res')++  handle res (TimerStuff opt n msg) k = do+      v <- time+      if not (canPerf res)+        then k () res+        else do+          let res' = timerStuff' opt v n msg res+          perfLog res' $ unwords [displayTimerOpt opt, "timer", show n, "at", show v, fromMaybe "" msg]+          k () (res')++  handle res (Timestamp s) k = do+      v <- time+      let stamp = v - (stime res)+      if not (canPerf res)+        then k () res+        else do+          let res' = record {stamps = (s,stamp) :: stamps res} res+          perfLog res' $ unlines [ "Creating Timestamp:"+                                 , "\tTIMESTAMP:", show v+                                 , "\tMESSAGE:", show s]+          k () (res')++-- ------------------------------------------------------- [ Effect Descriptor ]++PERF : EFFECT+PERF = MkEff PMetrics Perf++-- --------------------------------------------------------------------- [ API ]++||| Turn on performance metrics.+collectPMetricsOnly : Eff () [PERF]+collectPMetricsOnly = call $ TurnOn False++collectPMetrics : Bool -> Eff () [PERF]+collectPMetrics b = call $ TurnOn b++||| Turn on performance metrics and show during operation+collectPMetricsAndShow : Eff () [PERF]+collectPMetricsAndShow = call $ TurnOn True++||| Return gatheres metrics+getPerfMetrics : Eff PMetrics [PERF]+getPerfMetrics = call $ GetMetrics++||| Create a counter+mkCounter : String -> Eff () [PERF]+mkCounter n = call $ MkCounter n++||| Increment the counter+incCounter : String -> Eff () [PERF]+incCounter n = call $ IncCounter n++mkTimer : String -> Eff () [PERF]+mkTimer n = call $ MkStopWatch n++||| Stop a timer+stopTimer : String -> Eff () [PERF]+stopTimer n = call $ TimerStuff STOP n Nothing++||| Start a timer+startTimer : String -> Eff () [PERF]+startTimer n = call $ TimerStuff START n Nothing++||| Split a timer+splitTimer : String -> Eff () [PERF]+splitTimer n = call $ TimerStuff SPLIT n Nothing++splitTimerMsg : String -> String -> Eff () [PERF]+splitTimerMsg n msg = call $ TimerStuff SPLIT n (Just msg)++||| Create a time stamp.+timestamp : String -> Eff () [PERF]+timestamp msg = call $ Timestamp msg++-- --------------------------------------------------------------------- [ EOF ]

@@ -4,28 +4,28 @@ import Data.Vect  data Random : Effect where -     getRandom : sig Random Integer Integer-     setSeed   : Integer -> sig Random () Integer+     GetRandom : sig Random Integer Integer+     SetSeed   : Integer -> sig Random () Integer  instance Handler Random m where-  handle seed getRandom k+  handle seed GetRandom k            = let seed' = assert_total ((1664525 * seed + 1013904223) `prim__sremBigInt` (pow 2 32)) in                  k seed' seed'-  handle seed (setSeed n) k = k () n+  handle seed (SetSeed n) k = k () n  RND : EFFECT RND = MkEff Integer Random  ||| Generates a random Integer in a given range rndInt : Integer -> Integer -> Eff Integer [RND]-rndInt lower upper = do v <- call $ getRandom+rndInt lower upper = do v <- call $ GetRandom                         return ((v `prim__sremBigInt` (upper - lower)) + lower)  ||| Generate a random number in Fin (S `k`) |||  ||| Note that rndFin k takes values 0, 1, ..., k. rndFin : (k : Nat) -> Eff (Fin (S k)) [RND]-rndFin k = do let v = assert_total $ !(call getRandom) `prim__sremBigInt` (cast (S k))+rndFin k = do let v = assert_total $ !(call GetRandom) `prim__sremBigInt` (cast (S k))               return (toFin v)  where toFin : Integer -> Fin (S k)         toFin x = case integerToFin x (S k) of@@ -43,5 +43,5 @@  ||| Sets the random seed srand : Integer -> Eff () [RND]-srand n = call $ setSeed n+srand n = call $ SetSeed n 

@@ -12,9 +12,9 @@ ||| The Effect type describes effectful computations. ||| ||| This type is parameterised by:-||| + The input resource. ||| + The return type of the computation.-||| + The computation to run on the resource.+||| + The input resource.+||| + The computation to run on the resource given the return value. Effect : Type Effect = (x : Type) -> Type -> (x -> Type) -> Type @@ -159,17 +159,17 @@ data EffM : (m : Type -> Type) -> (x : Type)             -> (es : List EFFECT)             -> (ce : x -> List EFFECT) -> Type where-     value    : (val : a) -> EffM m a (xs val) xs-     ebind    : EffM m a xs xs' ->+     Value    : (val : a) -> EffM m a (xs val) xs+     EBind    : EffM m a xs xs' ->                 ((val : a) -> EffM m b (xs' val) xs'') -> EffM m b xs xs''-     callP    : (prf : EffElem e a xs) ->+     CallP    : (prf : EffElem e a xs) ->                 (eff : e t a b) ->                 EffM m t xs (\v => updateResTy v xs prf eff) -     liftP    : (prf : SubList ys xs) ->+     LiftP    : (prf : SubList ys xs) ->                 EffM m t ys ys' -> EffM m t xs (\v => updateWith (ys' v) xs prf) -     new      : Handler e' m => (e : EFFECT) -> resTy ->+     New      : Handler e' m => (e : EFFECT) -> resTy ->                 {auto prf : e = MkEff resTy e'} ->                 EffM m t (e :: es) (\v => e :: es) ->                 EffM m t es (\v => es)@@ -211,12 +211,12 @@ %no_implicit (>>=)   : EffM m a xs xs' ->           ((val : a) -> EffM m b (xs' val) xs'') -> EffM m b xs xs''-(>>=) = ebind+(>>=) = EBind  -- namespace SimpleBind --   (>>=) : Eff m a xs (\v => xs) -> --           ((val : a) -> Eff m b xs xs') -> Eff m b xs xs'---   (>>=) = ebind+--   (>>=) = EBind  ||| Run a subprogram which results in an effect state the same as the input. staticEff : EffM m a xs (\v => xs) -> EffM m a xs (\v => xs)@@ -228,17 +228,17 @@ toEff xs' = id  return : a -> EffM m a xs (\v => xs)-return x = value x+return x = Value x  -- ------------------------------------------------------ [ for idiom brackets ]  infixl 2 <*>  pure : a -> EffM m a xs (\v => xs)-pure = value+pure = Value  pureM : (val : a) -> EffM m a (xs val) xs-pureM = value+pureM = Value  (<*>) : EffM m (a -> b) xs (\v => xs) ->         EffM m a xs (\v => xs) -> EffM m b xs (\v => xs)@@ -246,6 +246,17 @@                   arg <- v                   return (fn arg) +(*>) : EffM m a xs (\v => xs) ->+       EffM m b xs (\v => xs) -> EffM m b xs (\v => xs)+a *> b = do a+            b+     +new : Handler e' m => (e : EFFECT) -> resTy ->+      {auto prf : e = MkEff resTy e'} ->+      EffM m t (e :: es) (\v => e :: es) ->+      EffM m t es (\v => es)+new = New+ -- ---------------------------------------------------------- [ an interpreter ]  private@@ -254,28 +265,23 @@           ((v : a) -> Env m (updateResTy v xs p eff) -> m t) -> m t execEff (val :: env) Here eff' k     = handle val eff' (\v, res => k v (res :: env))--- FIXME: Teach the elaborator to propagate parameters here-execEff {e} {a} {res} {resk} (val :: env) (There p) eff k-    = execEff {e} {a} {res} {resk} env p eff (\v, env' => k v (val :: env'))+execEff (val :: env) (There p) eff k+    = execEff env p eff (\v, env' => k v (val :: env'))  -- Q: Instead of m b, implement as StateT (Env m xs') m b, so that state -- updates can be propagated even through failing computations?  eff : Env m xs -> EffM m a xs xs' -> ((x : a) -> Env m (xs' x) -> m b) -> m b-eff env (value x) k = k x env-eff env (prog `ebind` c) k+eff env (Value x) k = k x env+eff env (prog `EBind` c) k    = eff env prog (\p', env' => eff env' (c p') k)-eff env (callP prf effP) k = execEff env prf effP k-eff env (liftP prf effP) k+eff env (CallP prf effP) k = execEff env prf effP k+eff env (LiftP prf effP) k    = let env' = dropEnv env prf in          eff env' effP (\p', envk => k p' (rebuildEnv envk prf env))-eff env (new (MkEff resTy newEff) res {prf=Refl} effP) k+eff env (New (MkEff resTy newEff) res {prf=Refl} effP) k    = eff (res :: env) effP (\p', (val :: envk) => k p' envk)--- FIXME:--- xs is needed explicitly because otherwise the pattern binding for--- 'l' appears too late. Solution seems to be to reorder patterns at the--- end so that everything is in scope when it needs to be.-eff {xs = [l ::: x]} env (l :- prog) k+eff env (l :- prog) k    = let env' = unlabel env in          eff env' prog (\p', envk => k p' (relabel l envk)) @@ -291,17 +297,18 @@                           [default, default, default, default, default, default, default],                           [default, default, default, default, default, default, default, default] |) +%no_implicit call : {a, b: _} -> {e : Effect} ->        (eff : e t a b) ->        {auto prf : EffElem e a xs} ->       EffM m t xs (\v => updateResTy v xs prf eff)-call e {prf} = callP prf e+call e {prf} = CallP prf e  implicit lift : EffM m t ys ys' ->        {auto prf : SubList ys xs} ->        EffM m t xs (\v => updateWith (ys' v) xs prf)-lift e {prf} = liftP prf e+lift e {prf} = LiftP prf e   -- --------------------------------------------------------- [ Running Effects ]

@@ -18,3 +18,4 @@         , Effect.Logging.Level         , Effect.Logging.Default         , Effect.Logging.Category+        , Effect.Perf

@@ -8,7 +8,7 @@ ||| Idris's primitive IO, for building abstractions on top of abstract data PrimIO : Type -> Type where-     prim__IO : a -> PrimIO a+     Prim__IO : a -> PrimIO a  ||| A token representing the world, for use in `IO` abstract data World = TheWorld prim__WorldType@@ -93,14 +93,14 @@  abstract prim_io_bind : PrimIO a -> (a -> PrimIO b) -> PrimIO b-prim_io_bind (prim__IO v) k = k v+prim_io_bind (Prim__IO v) k = k v  unsafePerformPrimIO : PrimIO a -> a -- compiled as primitive  abstract prim_io_return : a -> PrimIO a-prim_io_return x = prim__IO x+prim_io_return x = Prim__IO x  abstract io_bind : IO' l a -> (a -> IO' l b) -> IO' l b@@ -116,11 +116,11 @@ liftPrimIO : (World -> PrimIO a) -> IO' l a liftPrimIO = MkIO -call__IO : IO' l a -> PrimIO a+call__IO : IO' ffi a -> PrimIO a call__IO (MkIO f) = f (TheWorld prim__TheWorld)  -- Concrete type makes it easier to elaborate at top level-run__IO : IO' l () -> PrimIO ()+run__IO : IO' ffi () -> PrimIO () run__IO f = call__IO f  unsafePerformIO : IO' ffi a -> a@@ -171,10 +171,14 @@    ||| A descriptor for the C FFI. See the constructors of `C_Types`   ||| and `C_IntTypes` for the concrete types that are available.+  %error_reverse   FFI_C : FFI   FFI_C = MkFFI C_Types String String -IO : Type -> Type+||| Interactive programs, describing I/O actions and returning a value.+||| @res The result type of the program +%error_reverse+IO : (res : Type) -> Type IO = IO' FFI_C  -- Cannot be relaxed as is used by type providers and they expect IO a@@ -195,6 +199,9 @@   forceGC : IO ()   forceGC = foreign FFI_C "idris_forceGC" (Ptr -> IO ()) prim__vm +  getErrno : IO Int+  getErrno = foreign FFI_C "idris_errno" (IO Int)+ --------- The Javascript/Node FFI  @@ -228,9 +235,11 @@ ||| 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.+%error_reverse FFI_JS : FFI FFI_JS = MkFFI JS_Types String String +%error_reverse JS_IO : Type -> Type JS_IO = IO' FFI_JS 

@@ -11,6 +11,22 @@  %access public +||| A source location in an Idris file+record SourceLocation where+  ||| Either a source span or a source location. `start` and `end`+  ||| will be the same if it's a point location.+  constructor FileLoc++  ||| The file name of the source location+  filename : String+  ||| The line and column of the beginning of the source span+  start : (Int, Int)+  ||| The line and column of the end of the source span+  end : (Int, Int)++%name SourceLocation loc++ mutual   data TTName =               ||| A user-provided name@@ -24,9 +40,7 @@               MN Int String |               ||| Special names, to make conflicts impossible and language features               ||| predictable-              SN SpecialName |-              ||| Name of something which is never used in scope-              NErased+              SN SpecialName   %name TTName n, n'    data SpecialName = WhereN Int TTName TTName@@ -34,7 +48,7 @@                    | InstanceN TTName (List String)                    | ParentN TTName String                    | MethodN TTName-                   | CaseN TTName+                   | CaseN SourceLocation TTName                    | ElimN TTName                    | InstanceCtorN TTName                    | MetaN TTName TTName@@ -116,22 +130,62 @@  ||| Types annotations for bound variables in different ||| binding contexts-data Binder a = Lam a-              | Pi a a-              | Let a a-              | NLet a a-              | Hole a-              | GHole a-              | Guess a a-              | PVar a-              | PVTy a+|||+||| @ tmTy the terms that can occur inside the binder, as type+|||        annotations or bound values+data Binder : (tmTy : Type) -> Type where+  ||| Lambdas+  |||+  ||| @ ty the type of the argument+  Lam : (ty : a) -> Binder a++  ||| Function types.+  |||+  ||| @ kind The kind of arrow. Only relevant when dealing with+  |||        uniqueness, so you can usually pretend that this+  |||        field doesn't exist. For ordinary functions, use the+  |||        type of types here.+  Pi : (ty, kind : a) -> Binder a++  ||| A let binder+  |||+  ||| @ ty the type of the bound variable+  ||| @ val the bound value+  Let : (ty, val : a) -> Binder a++  ||| A hole that can occur during elaboration, and must be filled+  |||+  ||| @ ty the type of the value that will eventually be put into the hole+  Hole : (ty : a) -> Binder a++  ||| A hole that will later become a top-level metavariable+  GHole : (ty : a) -> Binder a++  ||| A hole with a solution in it. Computationally inert.+  |||+  ||| @ ty the type of the value in the hole+  ||| @ val the value in the hole+  Guess : (ty, val : a) -> Binder a++  ||| A pattern variable. These bindings surround the terms that make+  ||| up the left and right sides of pattern-matching definition+  ||| clauses.+  |||+  ||| @ ty the type of the pattern variable+  PVar : (ty : a) -> Binder a++  ||| The type of a pattern binding. This is to `PVar` as `Pi` is to+  ||| `Lam`.+  |||+  ||| @ ty the type of the pattern variable+  PVTy : (ty : a) -> Binder a+ %name Binder b, b'  instance Functor Binder where   map f (Lam x) = Lam (f x)   map f (Pi x k) = Pi (f x) (f k)   map f (Let x y) = Let (f x) (f y)-  map f (NLet x y) = NLet (f x) (f y)   map f (Hole x) = Hole (f x)   map f (GHole x) = GHole (f x)   map f (Guess x y) = Guess (f x) (f y)@@ -142,7 +196,6 @@   foldr f z (Lam x) = f x z   foldr f z (Pi x k) = f x (f k z)   foldr f z (Let x y) = f x (f y z)-  foldr f z (NLet x y) = f x (f y z)   foldr f z (Hole x) = f x z   foldr f z (GHole x) = f x z   foldr f z (Guess x y) = f x (f y z)@@ -153,14 +206,13 @@   traverse f (Lam x) = [| Lam (f x) |]   traverse f (Pi x k) = [| Pi (f x) (f k) |]   traverse f (Let x y) = [| Let (f x) (f y) |]-  traverse f (NLet x y) = [| NLet (f x) (f y) |]   traverse f (Hole x) = [| Hole (f x) |]   traverse f (GHole x) = [| GHole (f x) |]   traverse f (Guess x y) = [| Guess (f x) (f y) |]   traverse f (PVar x) = [| PVar (f x) |]   traverse f (PVTy x) = [| PVTy (f x) |] -||| Universes+||| The various universes involved in the uniqueness mechanism data Universe = NullType | UniqueType | AllTypes  ||| Reflection of the well typed core language@@ -175,14 +227,11 @@         App TT TT |         ||| Embed a constant         TConst Const |-        ||| Argument projection; runtime only-        Proj TT Int |         ||| Erased terms         Erased |-        ||| Impossible terms-        Impossible |         ||| The type of types along (with universe constraints)         TType TTUExp |+        ||| Alternative universes for dealing with uniqueness         UType Universe %name TT tm, tm' @@ -196,17 +245,12 @@          RApp Raw Raw |          ||| The type of types          RType |+         ||| Alternative universes for dealing with uniqueness          RUType Universe |-         RForce Raw |          ||| Embed a constant          RConstant Const %name Raw tm, tm' -data SourceLocation : Type where-  FileLoc : (filename : String) -> (start : (Int, Int)) -> (end : (Int, Int)) -> SourceLocation--%name SourceLocation loc- ||| Error reports are a list of report parts data ErrorReportPart =                      ||| A human-readable string@@ -221,7 +265,7 @@                      SubReport (List ErrorReportPart) %name ErrorReportPart part, p -||| A representation of Idris's tactics that can be returned from custom+||| A representation of Idris's old tactics that can be returned from custom ||| tactic implementations. Generate these using `applyTactic`. data Tactic =             ||| Try the first tactic and resort to the second one on failure@@ -280,6 +324,7 @@             Fail (List ErrorReportPart) |             ||| Attempt to fill the hole with source code information             SourceFC+ %name Tactic tac, tac'  @@ -409,6 +454,21 @@   quote [] = `(List.Nil {elem=~(quotedTy {a})})   quote (x :: xs) = `(List.(::) {elem=~(quotedTy {a})} ~(quote x) ~(quote xs)) +instance Quotable SourceLocation TT where+  quotedTy = `(SourceLocation)+  quote (FileLoc fn (sl, sc) (el, ec)) =+    `(FileLoc ~(quote fn)+              (~(quote sl), ~(quote sc))+              (~(quote el), ~(quote ec)))++instance Quotable SourceLocation Raw where+  quotedTy = `(SourceLocation)+  quote (FileLoc fn (sl, sc) (el, ec)) =+    `(FileLoc ~(quote {t=Raw} fn)+              (~(quote {t=Raw} sl), ~(quote {t=Raw} sc))+              (~(quote {t=Raw} el), ~(quote {t=Raw} ec)))++ mutual   instance Quotable TTName TT where     quotedTy = `(TTName)@@ -416,7 +476,6 @@     quote (NS n xs) = `(NS ~(quote n) ~(quote xs))     quote (MN x y) = `(MN ~(quote x) ~(quote y))     quote (SN sn) = `(SN ~(assert_total $ quote sn))-    quote NErased = `(NErased)    instance Quotable SpecialName TT where     quotedTy = `(SpecialName)@@ -425,7 +484,7 @@     quote (InstanceN i ss) = `(InstanceN ~(quote i) ~(quote ss))     quote (ParentN n s) = `(ParentN ~(quote n) ~(quote s))     quote (MethodN n) = `(MethodN ~(quote n))-    quote (CaseN n) = `(CaseN ~(quote n))+    quote (CaseN fc n) = `(CaseN ~(quote fc) ~(quote n))     quote (ElimN n) = `(ElimN ~(quote n))     quote (InstanceCtorN n) = `(InstanceCtorN ~(quote n))     quote (MetaN parent meta) = `(MetaN ~(quote parent) ~(quote meta))@@ -437,7 +496,6 @@     quote (NS n xs) = `(NS ~(quote {t=Raw} n) ~(quote {t=Raw} xs))     quote (MN x y) = `(MN ~(quote {t=Raw} x) ~(quote {t=Raw} y))     quote (SN sn) = `(SN ~(assert_total $ quote sn))-    quote NErased = `(NErased)    instance Quotable SpecialName Raw where     quotedTy = `(SpecialName)@@ -446,7 +504,7 @@     quote (InstanceN i ss) = `(InstanceN ~(quote i) ~(quote ss))     quote (ParentN n s) = `(ParentN ~(quote n) ~(quote s))     quote (MethodN n) = `(MethodN ~(quote n))-    quote (CaseN n) = `(CaseN ~(quote n))+    quote (CaseN fc n) = `(CaseN ~(quote fc) ~(quote n))     quote (ElimN n) = `(ElimN ~(quote n))     quote (InstanceCtorN n) = `(InstanceCtorN ~(quote n))     quote (MetaN parent meta) = `(MetaN ~(quote parent) ~(quote meta))@@ -556,9 +614,7 @@     quote (Bind n b tm) = `(Bind ~(quote n) ~(assert_total (quote b)) ~(quote tm))     quote (App f x) = `(App ~(quote f) ~(quote x))     quote (TConst c) = `(TConst ~(quote c))-    quote (Proj tm x) = `(Proj ~(quote tm) ~(quote x))     quote Erased = `(Erased)-    quote Impossible = `(Impossible)     quote (TType uexp) = `(TType ~(quote uexp))     quote (UType u) = `(UType ~(quote u)) @@ -569,8 +625,6 @@                                  ~(assert_total (quote k)))     quote (Let x y) = `(Let {a=TT} ~(assert_total (quote x))                                            ~(assert_total (quote y)))-    quote (NLet x y) = `(NLet {a=TT} ~(assert_total (quote x))-                                           ~(assert_total (quote y)))     quote (Hole x) = `(Hole {a=TT} ~(assert_total (quote x)))     quote (GHole x) = `(GHole {a=TT} ~(assert_total (quote x)))     quote (Guess x y) = `(Guess {a=TT} ~(assert_total (quote x))@@ -585,14 +639,12 @@   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))    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))@@ -614,14 +666,12 @@   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))@@ -673,18 +723,3 @@   quote Skip = `(Skip)   quote (Fail xs) = `(Fail ~(quote xs))   quote SourceFC = `(SourceFC)---instance Quotable SourceLocation TT where-  quotedTy = `(SourceLocation)-  quote (FileLoc fn (sl, sc) (el, ec)) =-    `(FileLoc ~(quote fn)-              (~(quote sl), ~(quote sc))-              (~(quote el), ~(quote ec)))--instance Quotable SourceLocation Raw where-  quotedTy = `(SourceLocation)-  quote (FileLoc fn (sl, sc) (el, ec)) =-    `(FileLoc ~(quote {t=Raw} fn)-              (~(quote {t=Raw} sl), ~(quote {t=Raw} sc))-              (~(quote {t=Raw} el), ~(quote {t=Raw} ec)))

@@ -34,11 +34,13 @@ ||| Function arguments ||| ||| These are the simplest representation of argument lists, and are-||| used for functions.+||| used for functions. Additionally, because a FunArg provides enough+||| information to build an application, a generic type lookup of a+||| top-level identifier will return its FunArgs, if applicable. record FunArg where   constructor MkFunArg-  argName : TTName-  argTy   : Raw+  name    : TTName+  type    : Raw   plicity : Plicity   erasure : Erasure @@ -54,25 +56,30 @@   TyConIndex FunArg  ||| A type declaration-data TyDecl : Type where-  ||| A type declaration.-  |||-  ||| Each argument is in the scope of the names of previous-  ||| arguments, and the return type is in the scope of all the-  ||| argument names.-  |||-  ||| @ fn the name to be declared, fully-qualified-  ||| @ args the arguments to the function-  ||| @ ret the final return type-  Declare : (fn : TTName) -> (args : List FunArg) -> (ret : Raw) -> TyDecl+record TyDecl where+  constructor Declare +  ||| The name of the function being declared.+  name : TTName++  ||| Each argument is in the scope of the names of previous arguments.+  arguments : List FunArg++  ||| The return type is in the scope of all the argument names.+  returnType : Raw+++-- Note: FunClause is not a record because impossible clauses may be+-- added at some point. ||| A single pattern-matching clause data FunClause : Type where   MkFunClause : (lhs, rhs : Raw) -> FunClause  ||| A reflected function definition.-data FunDefn : Type where-  DefineFun : TTName -> List FunClause -> FunDefn+record FunDefn where+  constructor DefineFun+  name : TTName+  clauses : List FunClause   data CtorArg = CtorParameter FunArg | CtorField FunArg@@ -82,7 +89,7 @@   constructor MkDatatype    ||| The name of the type constructor-  familyName : TTName+  name : TTName    ||| The arguments to the type constructor   tyConArgs : List TyConArg@@ -97,61 +104,62 @@ abstract data Elab : Type -> Type where   -- obligatory control stuff-  prim__PureElab : a -> Elab a-  prim__BindElab : {a, b : Type} -> Elab a -> (a -> Elab b) -> Elab b--  prim__Try : {a : Type} -> Elab a -> Elab a -> Elab a-  prim__Fail : {a : Type} -> List ErrorReportPart -> Elab a+  Prim__PureElab : a -> Elab a+  Prim__BindElab : {a, b : Type} -> Elab a -> (a -> Elab b) -> Elab b -  prim__Env : Elab (List (TTName, Binder TT))-  prim__Goal : Elab (TTName, TT)-  prim__Holes : Elab (List TTName)-  prim__Guess : Elab (Maybe TT)-  prim__LookupTy : TTName -> Elab (List (TTName, NameType, TT))-  prim__LookupDatatype : TTName -> Elab (List Datatype)+  Prim__Try : {a : Type} -> Elab a -> Elab a -> Elab a+  Prim__Fail : {a : Type} -> List ErrorReportPart -> Elab a -  prim__Check : Raw -> Elab (TT, TT)+  Prim__Env : Elab (List (TTName, Binder TT))+  Prim__Goal : Elab (TTName, TT)+  Prim__Holes : Elab (List TTName)+  Prim__Guess : Elab TT+  Prim__LookupTy : TTName -> Elab (List (TTName, NameType, TT))+  Prim__LookupDatatype : TTName -> Elab (List Datatype)+  Prim__LookupArgs : TTName -> Elab (List (TTName, List FunArg, Raw)) -  prim__SourceLocation : Elab SourceLocation-  prim__Namespace : Elab (List String)+  Prim__Check : List (TTName, Binder TT) -> Raw -> Elab (TT, TT) -  prim__Forget : TT -> Elab Raw+  Prim__SourceLocation : Elab SourceLocation+  Prim__Namespace : Elab (List String) -  prim__Gensym : String -> Elab TTName+  Prim__Gensym : String -> Elab TTName -  prim__Solve : Elab ()-  prim__Fill : 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 ()+  Prim__Solve : Elab ()+  Prim__Fill : Raw -> Elab ()+  Prim__Apply : Raw -> List Bool -> Elab (List (TTName, TTName))+  Prim__MatchApply : Raw -> List Bool -> Elab (List (TTName, TTName))+  Prim__Focus : TTName -> Elab ()+  Prim__Unfocus : TTName -> Elab ()+  Prim__Attack : Elab () -  prim__Rewrite : Raw -> Elab ()+  Prim__Rewrite : Raw -> Elab () -  prim__Claim : TTName -> Raw -> Elab ()-  prim__Intro : Maybe TTName -> Elab ()-  prim__Forall : TTName -> Raw -> Elab ()-  prim__PatVar : TTName -> Elab ()-  prim__PatBind : TTName -> Elab ()-  prim__LetBind : TTName -> Raw -> Raw -> Elab ()+  Prim__Claim : TTName -> Raw -> Elab ()+  Prim__Intro : Maybe TTName -> Elab ()+  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__Compute : Elab ()+  Prim__Normalise : (List (TTName, Binder TT)) -> TT -> Elab TT+  Prim__Whnf : TT -> Elab TT+  Prim__Converts : (List (TTName, Binder TT)) -> TT -> TT -> Elab () -  prim__DeclareType : TyDecl -> Elab ()-  prim__DefineFunction : FunDefn -> Elab ()-  prim__AddInstance : TTName -> TTName -> Elab ()+  Prim__DeclareType : TyDecl -> Elab ()+  Prim__DefineFunction : FunDefn -> Elab ()+  Prim__AddInstance : TTName -> TTName -> Elab ()+  Prim__IsTCName : TTName -> Elab Bool -  prim__ResolveTC : TTName -> Elab ()-  prim__Search : Int -> List TTName -> Elab ()-  prim__RecursiveElab : Raw -> Elab () -> Elab (TT, TT)+  Prim__ResolveTC : TTName -> Elab ()+  Prim__Search : Int -> List TTName -> Elab ()+  Prim__RecursiveElab : Raw -> Elab () -> Elab (TT, TT) -  prim__Fixity : String -> Elab Fixity+  Prim__Fixity : String -> Elab Fixity -  prim__Debug : {a : Type} -> List ErrorReportPart -> Elab a-  prim__Metavar : TTName -> Elab ()+  Prim__Debug : {a : Type} -> List ErrorReportPart -> Elab a+  Prim__Metavar : TTName -> Elab ()  ------------- -- Public API@@ -159,49 +167,50 @@ %access public namespace Tactics   instance Functor Elab where-    map f t = prim__BindElab t (\x => prim__PureElab (f x))+    map f t = Prim__BindElab t (\x => Prim__PureElab (f x))    instance Applicative Elab where-    pure x  = prim__PureElab x-    f <*> x = prim__BindElab f $ \g =>-              prim__BindElab x $ \y =>-              prim__PureElab   $ g y+    pure x  = Prim__PureElab x+    f <*> x = Prim__BindElab f $ \g =>+              Prim__BindElab x $ \y =>+              Prim__PureElab   $ g y    ||| The Alternative instance on Elab represents left-biased error   ||| handling. In other words, `t <|> t'` will run `t`, and if it   ||| fails, roll back the elaboration state and run `t'`.   instance Alternative Elab where-    empty   = prim__Fail [TextPart "empty"]-    x <|> y = prim__Try x y+    empty   = Prim__Fail [TextPart "empty"]+    x <|> y = Prim__Try x y    instance Monad Elab where-    x >>= f = prim__BindElab x f+    x >>= f = Prim__BindElab x f    ||| Halt elaboration with an error   fail : List ErrorReportPart -> Elab a-  fail err = prim__Fail err+  fail err = Prim__Fail err -  ||| Look up the lexical binding at the focused hole+  ||| Look up the lexical binding at the focused hole. Fails if no holes are present.   getEnv : Elab (List (TTName, Binder TT))-  getEnv = prim__Env+  getEnv = Prim__Env -  ||| Get the name and type of the focused hole+  ||| Get the name and type of the focused hole. Fails if not holes are present.   getGoal : Elab (TTName, TT)-  getGoal = prim__Goal+  getGoal = Prim__Goal -  ||| Get the hole queue, in order+  ||| Get the hole queue, in order.   getHoles : Elab (List TTName)-  getHoles = prim__Holes+  getHoles = Prim__Holes -  ||| If the current hole contains a guess, return it-  getGuess : Elab (Maybe TT)-  getGuess = prim__Guess+  ||| If the current hole contains a guess, return it. Otherwise, fail.+  getGuess : Elab TT+  getGuess = Prim__Guess -  ||| Look up the types of every overloading of a name+  ||| Look up the types of every overloading of a name.   lookupTy :  TTName -> Elab (List (TTName, NameType, TT))-  lookupTy n = prim__LookupTy n+  lookupTy n = Prim__LookupTy n -  ||| Get the type of a fully-qualified name+  ||| Get the type of a fully-qualified name. Fail if it doesn not+  ||| resolve uniquely.   lookupTyExact : TTName -> Elab (TTName, NameType, TT)   lookupTyExact n = case !(lookupTy n) of                       [res] => return res@@ -209,55 +218,61 @@                       xs    => fail [NamePart n, TextPart "is ambiguous."]    ||| Find the reflected representation of all datatypes whose names-  ||| are overloadings of some name+  ||| are overloadings of some name.   lookupDatatype : TTName -> Elab (List Datatype)-  lookupDatatype n = prim__LookupDatatype n+  lookupDatatype n = Prim__LookupDatatype n    ||| Find the reflected representation of a datatype, given its-  ||| fully-qualified name.+  ||| fully-qualified name. Fail if the name does not uniquely resolve+  ||| to a datatype.   lookupDatatypeExact : TTName -> Elab Datatype   lookupDatatypeExact n = case !(lookupDatatype n) of                             [res] => return res                             []    => 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 argument specification for each overloading of a name.+  lookupArgs : TTName -> Elab (List (TTName, List FunArg, Raw))+  lookupArgs n = Prim__LookupArgs n -  ||| Get the goal type as a Raw term-  goalType : Elab Raw-  goalType = do g <- getGoal-                forgetTypes (snd g)+  ||| Get the argument specification for a name. Fail if the name does+  ||| not uniquely resolve.+  lookupArgsExact : TTName -> Elab (TTName, List FunArg, Raw)+  lookupArgsExact n = case !(lookupArgs n) of+                        [res] => return res+                        []    => fail [NamePart n, TextPart "is not defined."]+                        xs    => fail [NamePart n, TextPart "is ambiguous."] +  ||| Attempt to type-check a term, getting back itself and its type.+  |||+  ||| @ env the environment within which to check the type+  ||| @ tm the term to check+  check : (env : List (TTName, Binder TT)) -> (tm : Raw) -> Elab (TT, TT)+  check env tm = Prim__Check env tm +   ||| Generate a unique name based on some hint.   |||   ||| **NB**: the generated name is unique _for this run of the   ||| elaborator_. Do not assume that they are globally unique.   gensym : (hint : String) -> Elab TTName-  gensym hint = prim__Gensym hint+  gensym hint = Prim__Gensym hint    ||| Substitute a guess into a hole.   solve : Elab ()-  solve = prim__Solve+  solve = Prim__Solve -  ||| Place a term into a hole, unifying its type+  ||| Place a term into a hole, unifying its type. Fails if the focus+  ||| is not a hole.   fill : Raw -> Elab ()-  fill tm = prim__Fill tm+  fill tm = Prim__Fill 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.+  ||| The return value is the list of holes established for the+  ||| arguments to the function.   |||   ||| Note that not all of the returned hole names still exist, as   ||| they may have been solved.@@ -266,20 +281,15 @@   |||   ||| @ 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+  |||     the argument by unification.+  apply : (op : Raw) -> (argSpec : List Bool) -> Elab (List TTName)+  apply tm argSpec = map snd <$> Prim__Apply tm argSpec    ||| Attempt to apply an operator to fill the current hole,-  ||| potentially solving arugments by matching.+  ||| potentially solving arguments 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.+  ||| The return value is the list of holes established for the+  ||| arguments to the function.   |||   ||| Note that not all of the returned hole names still exist, as   ||| they may have been solved.@@ -288,39 +298,41 @@   |||   ||| @ 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+  |||     the argument by matching. -  ||| Move the focus to the specified hole+  matchApply : (op : Raw) -> (argSpec : List Bool) -> Elab (List TTName)+  matchApply tm argSpec = map snd <$> Prim__Apply tm argSpec++  ||| Move the focus to the specified hole. Fails if the hole does not+  ||| exist.   |||   ||| @ hole the hole to focus on   focus : (hole : TTName) -> Elab ()-  focus hole = prim__Focus hole+  focus hole = Prim__Focus hole    ||| Send the currently-focused hole to the end of the hole queue and   ||| focus on the next hole.   unfocus : TTName -> Elab ()-  unfocus hole = prim__Unfocus hole+  unfocus hole = Prim__Unfocus hole -  ||| Convert a hole to make it suitable for bindings.+  ||| Convert a hole to make it suitable for bindings - that is,+  ||| transform it such that it has the form `?h : t . h` as opposed to+  ||| `?h : t . f h`.   |||   ||| The binding tactics require that a hole be directly under its   ||| binding, or else the scopes of the generated terms won't make   ||| sense. This tactic creates a new hole of the proper form, and   ||| points the old hole at it.   attack : Elab ()-  attack = prim__Attack+  attack = Prim__Attack    ||| Introduce a new hole with a specified name and type.   |||   ||| The new hole will be focused, and the previously-focused hole-  ||| will be immediately after it in the hole queue.+  ||| will be immediately after it in the hole queue. Because this+  ||| tactic introduces a new binding, you may need to `attack` first.   claim : TTName -> Raw -> Elab ()-  claim n ty = prim__Claim n ty+  claim n ty = Prim__Claim n ty    ||| Introduce a lambda binding around the current hole and focus on   ||| the body. Requires that the hole be in binding form (use@@ -328,54 +340,83 @@   |||   ||| @ n the name to use for the argument   intro : (n : TTName) -> Elab ()-  intro n = prim__Intro (Just n)+  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.+  ||| the body, using the name provided by the type of the+  ||| hole.+  |||+  ||| Requires that the hole be immediately under its binder (use+  ||| `attack` if it might not be).   intro' : Elab ()-  intro' = prim__Intro Nothing+  intro' = Prim__Intro Nothing    ||| Introduce a dependent function type binding into the current hole,   ||| and focus on the body.+  |||+  ||| Requires that the hole be immediately under its binder (use+  ||| `attack` if it might not be).   forall : TTName -> Raw -> Elab ()-  forall n ty = prim__Forall n ty+  forall n ty = Prim__Forall n ty    ||| Convert a hole into a pattern variable.   patvar : TTName -> Elab ()-  patvar n = prim__PatVar n+  patvar n = Prim__PatVar n    ||| Introduce a new pattern binding.+  |||+  ||| Requires that the hole be immediately under its binder (use+  ||| `attack` if it might not be).   patbind : TTName -> Elab ()-  patbind n = prim__PatBind n+  patbind n = Prim__PatBind n -  ||| Introduce a new let binding+  ||| Introduce a new let binding.   |||+  ||| Requires that the hole be immediately under its binder (use+  ||| `attack` if it might not be).+  |||   ||| @ 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+  letbind n ty tm = Prim__LetBind n ty tm    ||| Normalise the goal.   compute : Elab ()-  compute = prim__Compute+  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+  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+  whnf term = Prim__Whnf term +  ||| Check that two terms are convertable in the current context and+  ||| in some environment.+  |||+  ||| @ env a lexical environment to compare the terms in (see `getEnv`)+  ||| @ term1 the first term to convert+  ||| @ term2 the second term to convert+  convertsInEnv : (env : List (TTName, Binder TT)) -> (term1, term2 : TT) -> Elab ()+  convertsInEnv env term1 term2 = Prim__Converts env term1 term2++  ||| Check that two terms are convertable in the current context and environment+  |||+  ||| @ term1 the first term to convert+  ||| @ term2 the second term to convert+  converts : (term1, term2 : TT) -> Elab ()+  converts term1 term2 = convertsInEnv !getEnv term1 term2+   ||| Find the source context for the elaboration script   getSourceLocation : Elab SourceLocation-  getSourceLocation = prim__SourceLocation+  getSourceLocation = Prim__SourceLocation    ||| Attempt to solve the current goal with the source code location   sourceLocation : Elab ()@@ -389,7 +430,7 @@   ||| 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+  currentNamespace = Prim__Namespace    ||| Attempt to rewrite the goal using an equality.   |||@@ -397,43 +438,53 @@   ||| constructs a context for `replace` using them. In some cases,   ||| this is not possible, and `replace` must be called manually with   ||| an appropriate context.+  |||+  ||| Because this tactic internally introduces a `let` binding, it+  ||| requires that the hole be immediately under its binder (use+  ||| `attack` if it might not be).   rewriteWith : Raw -> Elab ()-  rewriteWith rule = prim__Rewrite rule+  rewriteWith rule = Prim__Rewrite rule    ||| Add a type declaration to the global context.   declareType : TyDecl -> Elab ()-  declareType decl = prim__DeclareType decl+  declareType decl = Prim__DeclareType decl    ||| Define a function in the global context. The function must have   ||| already been declared, either in ordinary Idris code or using   ||| `declareType`.   defineFunction : FunDefn -> Elab ()-  defineFunction defun = prim__DefineFunction defun+  defineFunction defun = Prim__DefineFunction defun -  ||| Register a new instance for type class resolution+  ||| Register a new instance for type class resolution.   |||   ||| @ className the name of the class for which an instance is being registered   ||| @ instName the name of the definition to use in instance search   addInstance : (className, instName : TTName) -> Elab ()-  addInstance className instName = prim__AddInstance className instName+  addInstance className instName = Prim__AddInstance className instName +  ||| Determine whether a name denotes a class.+  |||+  ||| @ name a name that might denote a class.+  isTCName : (name : TTName) -> Elab Bool+  isTCName name = Prim__IsTCName name+   ||| Attempt to solve the current goal with a type class dictionary   |||   ||| @ fn the name of the definition being elaborated (to prevent Idris   ||| from looping)   resolveTC : (fn : TTName) -> Elab ()-  resolveTC fn = prim__ResolveTC fn+  resolveTC fn = Prim__ResolveTC fn    ||| Use Idris's internal proof search.   search : Elab ()-  search = prim__Search 100 []+  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+  search' depth hints = Prim__Search depth hints    ||| Look up the declared fixity for an operator.   |||@@ -442,14 +493,14 @@   |||   ||| @ operator the operator string to look up   operatorFixity : (operator : String) -> Elab Fixity-  operatorFixity operator = prim__Fixity operator+  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 []+  debug = Prim__Debug []    ||| Halt elaboration, dumping the internal state and displaying a   ||| message.@@ -459,17 +510,17 @@   |||   ||| @ msg the message to display   debugMessage : (msg : List ErrorReportPart) -> Elab a-  debugMessage msg = prim__Debug msg+  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+  metavar name = Prim__Metavar name    ||| Recursively invoke the reflected elaborator with some goal.   |||   ||| The result is the final term and its type.   runElab : Raw -> Elab () -> Elab (TT, TT)-  runElab goal script = prim__RecursiveElab goal script+  runElab goal script = Prim__RecursiveElab goal script 

@@ -30,6 +30,7 @@ import public Prelude.Doubles import public Decidable.Equality import public Language.Reflection+import public Language.Reflection.Elab import public Language.Reflection.Errors  %access public

@@ -72,3 +72,7 @@ ||| Note: In Haskell, `choice` is called `asum`. choice : (Foldable t, Alternative f) => t (f a) -> f a choice x = foldr (<|>) empty x++||| A fused version of choice and map.+choiceMap : (Foldable t, Alternative f) => (a -> f b) -> t a -> f b+choiceMap f x = foldr (\elt, acc => f elt <|> acc) empty x

@@ -10,7 +10,8 @@ import Prelude.Bool import Prelude.Basics import Prelude.Classes-import Prelude.Monad+import Prelude.Either+import Prelude.Show import IO  %access public@@ -19,6 +20,30 @@ abstract data File = FHandle Ptr +||| An error from a file operation+-- This is built in idris_mkFileError() in rts/idris_stdfgn.c. Make sure+-- the values correspond!+data FileError = FileReadError+               | FileWriteError+               | FileNotFound+               | PermissionDenied+               | GenericFileError Int -- errno++private+strError : Int -> String+strError err = unsafePerformIO -- yeah, yeah...+                  (foreign FFI_C "idris_showerror" (Int -> IO String) err)++getFileError : IO FileError+getFileError = do MkRaw err <- foreign FFI_C "idris_mkFileError" +                                    (Ptr -> IO (Raw FileError)) prim__vm+                  return err++instance Show FileError where+  show FileNotFound = "File Not Found"+  show PermissionDenied = "Permission Denied"+  show (GenericFileError errno) = strError errno+ ||| Standard input stdin : File stdin = FHandle prim__stdin@@ -31,6 +56,13 @@ stderr : File stderr = FHandle prim__stderr +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))+ ||| Call the RTS's file opening function do_fopen : String -> String -> IO Ptr do_fopen f m@@ -39,12 +71,14 @@ ||| 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 : String) -> (m : String) -> IO (Either FileError File) fopen f m = do h <- do_fopen f m-               return (FHandle h)+               if !(nullPtr h)+                  then do err <- getFileError+                          return (Left err)+                  else return (Right (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)@@ -55,33 +89,26 @@ ||| Open a file ||| @ f the filename ||| @ m the mode-partial-openFile : (f : String) -> (m : Mode) -> IO File+openFile : (f : String) -> (m : Mode) -> IO (Either FileError 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))+fgetc : File -> IO (Either FileError Char)+fgetc (FHandle h) = do let c = cast !(foreign FFI_C "fgetc" (Ptr -> IO Int) h)+                       if !(ferror (FHandle h))+                          then return (Left FileReadError)+                          else return (Right c)  fflush : File -> IO () fflush (FHandle h) = foreign FFI_C "fflush" (Ptr -> IO ()) h@@ -89,9 +116,12 @@ 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 : String -> Mode -> IO (Either FileError File) popen f m = do ptr <- do_popen f (modeStr m)-               return (FHandle ptr)+               if !(nullPtr ptr)+                  then do err <- getFileError+                          return (Left err)+                  else return (Right (FHandle ptr))   where     modeStr Read  = "r"     modeStr Write = "w"@@ -103,20 +133,25 @@ -- mkForeign (FFun "idris_readStr" [FPtr, FPtr] (FAny String)) --                        prim__vm h -partial-fread : File -> IO' l String-fread (FHandle h) = do_fread h+fread : File -> IO (Either FileError String)+fread (FHandle h) = do str <- do_fread h+                       if !(ferror (FHandle h))+                          then return (Left FileReadError)+                          else return (Right str) -partial-do_fwrite : Ptr -> String -> IO ()-do_fwrite h s = do prim_fwrite h s-                   return ()+do_fwrite : Ptr -> String -> IO (Either FileError ())+do_fwrite h s = do res <- prim_fwrite h s+                   if (res /= 0)+                      then do errno <- getErrno+                              if errno == 0 +                                 then return (Left FileWriteError)+                                 else do err <- getFileError+                                         return (Left err)+                      else return (Right ()) -partial-fwrite : File -> String -> IO ()+fwrite : File -> String -> IO (Either FileError ()) 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 @@ -125,32 +160,34 @@ 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+partial -- might be reading something infinitely long like /dev/null ... +covering+readFile : String -> IO (Either FileError String)+readFile fn = do Right h <- openFile fn Read+                    | Left err => return (Left err)                  c <- readFile' h ""                  closeFile h                  return c   where     partial-    readFile' : File -> String -> IO String+    readFile' : File -> String -> IO (Either FileError String)     readFile' h contents =        do x <- feof h-          if not x then do l <- fread h+          if not x then do Right l <- fread h+                               | Left err => return (Left err)                            readFile' h (contents ++ l)-                   else return contents-+                   else return (Right contents) +||| Write a string to a file+writeFile : (filepath : String) -> (contents : String) -> +            IO (Either FileError ())+writeFile fn contents = do+     Right h <- openFile fn Write | Left err => return (Left err)+     Right () <- fwrite h contents | Left err => return (Left err)+     closeFile h+     return (Right ())

@@ -2,19 +2,21 @@  import Prelude.Basics -||| Functors-||| @ f the action of the functor on objects+||| Functors allow a uniform action over a parameterised type.+||| @ f a parameterised type  class Functor (f : Type -> Type) where-    ||| The action of the functor on morphisms-    ||| @ f the functor-    ||| @ m the morphism+    ||| Apply a function across everything of type 'a' in a +    ||| parameterised type+    ||| @ f the parameterised type+    ||| @ m the function to apply     map : (m : a -> b) -> f a -> f b  infixl 4 <$> -||| An infix alias for `map`: the action of a functor on morphisms.-||| @ f the functor-||| @ m the morphism+||| An infix alias for `map`, applying a function across everything of+||| type 'a' in a parameterised type+||| @ f the parameterised type+||| @ m the function to apply (<$>) : Functor f => (m : a -> b) -> f a -> f b m <$> x = map m x 

@@ -17,6 +17,7 @@ import Prelude.Cast import Prelude.Maybe import Prelude.Functor+import Prelude.Either import Prelude.Monad import IO @@ -24,33 +25,58 @@  ---- some basic io +||| Output a string to stdout without a trailing newline, for any FFI+||| descriptor+putStr' : String -> IO' ffi ()+putStr' x = do prim_write x+               return ()+ ||| Output a string to stdout without a trailing newline-putStr : String -> IO' ffi ()-putStr x = do prim_write x-              return ()+putStr : String -> IO ()+putStr = putStr' +||| Output a string to stdout with a trailing newline, for any FFI+||| descriptor+putStrLn' : String -> IO' ffi ()+putStrLn' x = putStr' (x ++ "\n")+ ||| Output a string to stdout with a trailing newline-putStrLn : String -> IO' ffi ()-putStrLn x = putStr (x ++ "\n")+putStrLn : String -> IO ()+putStrLn = putStrLn' +||| Output something showable to stdout, without a trailing newline, for any FFI+||| descriptor+print' : Show a => a -> IO' ffi ()+print' x = putStr' (show x)+ ||| Output something showable to stdout, without a trailing newline-print : Show a => a -> IO' ffi ()-print x = putStr (show x)+print : Show a => a -> IO ()+print = print' +||| Output something showable to stdout, with a trailing newline, for any FFI+||| descriptor+printLn' : Show a => a -> IO' ffi ()+printLn' x = putStrLn' (show x)+ ||| Output something showable to stdout, with a trailing newline-printLn : Show a => a -> IO' ffi ()-printLn x = putStrLn (show x)+printLn : Show a => a -> IO ()+printLn = printLn' -||| 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)))+||| Read one line of input from stdin, without the trailing newline, for any FFI+||| descriptor+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 +||| Read one line of input from stdin, without the trailing newline+getLine : IO String+getLine = getLine'+ ||| Write a single character to stdout putChar : Char -> IO () putChar c = foreign FFI_C "putchar" (Int -> IO ()) (cast c)@@ -97,7 +123,8 @@ processHandle h acc onRead onEOF     = if !(feof h)         then putStr (onEOF acc)-        else do x <- fread h+        else do Right x <- fread h+                    | Left err => putStr (onEOF acc)                 let (out, acc') = onRead acc x                 putStr out                 processHandle h acc' onRead onEOF    

@@ -13,7 +13,7 @@ infixl 5 >>=  class Applicative m => Monad (m : Type -> Type) where-    (>>=)  : m a -> (a -> m b) -> m b+    (>>=)  : m a -> ((result : a) -> m b) -> m b  ||| Also called `join` or mu flatten : Monad m => m (m a) -> m a

@@ -216,45 +216,45 @@  ||| A wrapper for Nat that specifies the semigroup and monad instances that use (*) record Multiplicative where-  constructor getMultiplicative+  constructor GetMultiplicative   _ : Nat  ||| A wrapper for Nat that specifies the semigroup and monad instances that use (+) record Additive where-  constructor getAdditive  +  constructor GetAdditive     _ : Nat    instance Semigroup Multiplicative where-  (<+>) left right = getMultiplicative $ left' * right'+  (<+>) left right = GetMultiplicative $ left' * right'     where       left'  : Nat       left'  =        case left of-          getMultiplicative m => m+          GetMultiplicative m => m        right' : Nat       right' =         case right of-          getMultiplicative m => m+          GetMultiplicative m => m  instance Semigroup Additive where-  left <+> right = getAdditive $ left' + right'+  left <+> right = GetAdditive $ left' + right'     where       left'  : Nat       left'  =         case left of-          getAdditive m => m+          GetAdditive m => m        right' : Nat       right' =         case right of-          getAdditive m => m+          GetAdditive m => m  instance Monoid Multiplicative where-  neutral = getMultiplicative $ S Z+  neutral = GetMultiplicative $ S Z  instance Monoid Additive where-  neutral = getAdditive Z+  neutral = GetAdditive Z  ||| Casts negative `Ints` to 0. instance Cast Int Nat where

@@ -10,6 +10,7 @@ import Prelude.Classes import Prelude.List import Prelude.Maybe+import Prelude.Either import Prelude.Nat import Prelude.Strings @@ -184,6 +185,10 @@ instance Show a => Show (Maybe a) where   showPrec d Nothing  = "Nothing"   showPrec d (Just x) = showCon d "Just" $ showArg x++instance (Show a, Show b) => Show (Either a b) where+  showPrec d (Left x)  = showCon d "Left" $ showArg x+  showPrec d (Right x) = showCon d "Right" $ showArg x  instance (Show a, {y : a} -> Show (p y)) => Show (Sigma a p) where     show (y ** prf) = "(" ++ show y ++ " ** " ++ show prf ++ ")"

@@ -109,6 +109,15 @@ scanr : (f : a -> Inf b -> b) -> (xs : Stream a) -> Stream b scanr f (x :: xs) = f x (foldr f xs) :: scanr f xs +||| Produce a Stream repeating a sequence+||| @ xs the sequence to repeat+||| @ ok proof that the list is non-empty+cycle : (xs : List a) -> {auto ok : NonEmpty xs} -> Stream a+cycle {a} (x :: xs) {ok = IsNonEmpty} = x :: cycle' xs+  where cycle' : List a -> Stream a+        cycle' []        = x :: cycle' xs+        cycle' (y :: ys) = y :: cycle' ys+ instance Applicative Stream where   pure = repeat   (<*>) = zipWith apply

@@ -1,6 +1,6 @@ package prelude -opts = "--nobuiltins --total"+opts = "--nobuiltins --total --no-elim-deprecation-warnings" modules = Builtins, Prelude, IO,            Prelude.Algebra, Prelude.Basics, Prelude.Bool, Prelude.Cast,

@@ -0,0 +1,21 @@+IDRIS     := idris+PKG       := pruviloj++build:+	$(IDRIS) --build ${PKG}.ipkg++clean:+	$(IDRIS) --clean ${PKG}.ipkg++install:+	$(IDRIS) --install ${PKG}.ipkg++rebuild: clean build++doc:+	$(IDRIS) --mkdoc ${PKG}.ipkg++doc_clean:+	rm -rf ${PKG}_doc++.PHONY: build clean install rebuild doc doc_clean

@@ -0,0 +1,8 @@+||| Provides the whole public interface of the proof tools. Import+||| `Pruviloj.Core` for just the simplest tactics.+module Pruviloj++import public Pruviloj.Core+import public Pruviloj.Disjoint+import public Pruviloj.Induction+import public Pruviloj.Injective

@@ -0,0 +1,268 @@+||| Core tactics for working with Elab reflection. These will be used+||| by most reasonable scripts, and they may be candidates for+||| eventual Prelude inclusion.+module Pruviloj.Core++import Language.Reflection.Utils++||| Run something for effects, throwing away the return value+ignore : Functor f => f a -> f ()+ignore x = map (const ()) x++||| Do nothing+skip : Applicative f => f ()+skip = pure ()++||| Attempt to apply a tactic. If it fails, do nothing.+try : Alternative f => f a -> f ()+try tac = ignore tac <|> pure ()++||| Remove type information from a `TT` term, in a context. Fails if+||| de Bruijn indices are out of scope.+forget' : List TTName -> TT -> Elab Raw+forget' env (P nt n tm) = pure (Var n)+forget' env (V x) = Var <$> getName x env+  where getName : Int -> List a -> Elab a+        getName _ [] = fail [TextPart "Scope error when forget'ting types"]+        getName i (n::ns) = if i <= 0 then pure n else getName (i-1) ns+forget' env (Bind n b tm) =+    [| (RBind n)+       (assert_total $ traverse (forget' env) b)+       (forget' (n::env) tm) |]+forget' env (App tm tm') = [| RApp (forget' env tm) (forget' env tm') |]+forget' env (TConst c) = pure (RConstant c)+forget' env Erased = pure (RConstant Forgot)+forget' env (TType uexp) = pure RType+forget' env (UType uni) = pure (RUType uni)++||| Remove type information from a `TT` term. Fails if de Bruijn+||| indices are out of scope.+forget : TT -> Elab Raw+forget tm = forget' [] tm++||| Get the goal type as a Raw term. Fails if there are no holes.+goalType : Elab Raw+goalType = do g <- getGoal+              forget (snd g)++||| Solve the goal using the most recent applicable hypothesis+hypothesis : Elab ()+hypothesis =+    do hyps <- map fst <$> getEnv+       flip choiceMap hyps $ \n =>+         do fill (Var n)+            solve+++||| Generate a unique name (using `gensym`) that looks like some+||| previous name, for ease of debugging code generators.+nameFrom : TTName -> Elab TTName+nameFrom (UN x) =+    gensym $ if length x == 0 || ("_" `isPrefixOf` x)+               then "x"+               else x+nameFrom (NS n ns) =+    nameFrom n -- throw out namespaces here, because we want to+               -- generate bound var names+nameFrom (MN x n) =+    gensym $ if length n == 0 || ("_" `isPrefixOf` n)+               then "n"+               else n+nameFrom (SN x) = gensym "SN"++||| Get the name at the head of the term, if it exists.+headName : Raw -> Maybe TTName+headName (RApp f _) = headName f+headName (Var n) = Just n+headName x = Nothing++||| Create a new hole with a given type without changing the+||| focus. Return the name of the hole.+|||+||| @ hint the hint to pass to `gensym`+||| @ ty the type of the new hole+newHole : (hint : String) -> (ty : Raw) -> Elab TTName+newHole hint ty =+    do hn <- gensym hint+       claim hn ty+       return hn++||| Use a term to solve a hole+|||+||| @ tm the term that has the right type for the hole+exact : (tm : Raw) -> Elab ()+exact tm = do apply tm []+              solve++||| Introduce as many names as possible, returning them.+intros : Elab (List TTName)+intros = do g <- snd <$> getGoal+            go g+  where go : TT -> Elab (List TTName)+        go (Bind n (Pi _ _) body) =+            do n' <- nameFrom n+               intro n'+               (n' ::) <$> go body+        go _ = return []++||| Run a tactic inside of a particular hole, if it still exists. If+||| it has been solved, do nothing.+inHole : TTName -> Elab a -> Elab (Maybe a)+inHole h todo =+  if (h `elem` !getHoles)+    then do focus h; Just <$> todo+    else return Nothing++||| Restrict a polymorphic type to () for contexts where it doesn't+||| matter. This is nice for sticking `debug` in a context where+||| Idris can't solve the type.+simple : {m : Type -> Type} -> m () -> m ()+simple x = x++||| Replace the current goal with one that's definitionally+||| equal. Return the name of the new goal, and ensure that it's+||| focused.+|||+||| @ newGoal A type that is equivalent to the current goal+equiv : (newGoal : Raw) -> Elab TTName+equiv newGoal =+    do h <- gensym "goal"+       claim h newGoal+       fill (Var h); solve+       focus h+       return h++||| Remember a term built with elaboration for later use. If the+||| current goal is `h`, then `remember n ty` puts a fresh hole at+||| the front of the queue, with the old goal `h` second. The+||| contents of this hole end up let-bound in the scope of+||| `h`. Return the name of the new hole, in case it will be used+||| later.+|||+||| @ n the name to be used to save the term+||| @ ty the type to inhabit+remember : (n : TTName) -> (ty : Raw) -> Elab TTName+remember n ty =+    do todo <- gensym "rememberThis"+       claim todo ty+       letbind n ty (Var todo)+       focus todo+       return todo++||| Repeat a given tactic until it fails. Fails if the tactic fails on+||| the first attempt; succeeds otherwise.+repeatUntilFail : Elab () -> Elab ()+repeatUntilFail tac =+    do tac+       repeatUntilFail tac <|> return ()++||| If the current goal is a pattern-bound variable, bind it with the+||| expected name. Otherwise fail.+bindPat : Elab ()+bindPat = do compute+             g <- snd <$> getGoal+             case g of+               Bind n (PVTy _) _ => patbind n+               _ => fail [TermPart g, TextPart "isn't looking for a pattern."]++||| The underlying implementation type for the inferType operator.+data Infer : Type where+  MkInfer : (a : Type) -> a -> Infer++||| Run a tactic script in a context where the type of the resulting+||| expression must be solvable via unification. Return the term and+||| its type.+|||+||| @ tac a tactic script that will be run with focus on the hole+|||       whose type is to be inferred.+total+inferType : (tac : Elab ()) -> Elab (TT, TT)+inferType tac =+    case fst !(runElab `(Infer) (startInfer *> tac)) of+        `(MkInfer ~ty ~tm) => return (tm, ty)+        _ => fail [TextPart "Not infer"]+  where+    startInfer : Elab ()+    startInfer = do [_, tmH] <- apply (Var `{MkInfer}) [True, False]+                       | err => fail [TextPart "Type inference failure"]+                    solve+                    focus tmH++||| Given one tactic that produces a list of subgoal names and another+||| that produces some result, run the second tactic in each hole+||| produced by the first and return the resulting values.+|||+||| Elab has no built-in notion of "subgoals", so this simulates the+||| Coq or JonPRL semicolon operators.+|||+||| @ first run this tactic to produce subgoals+||| @ after run this tactic in each subgoal+andThen : (first : Elab (List TTName)) -> (after : Elab a) -> Elab (List a)+andThen first after =+    do hs <- first+       catMaybes <$> for hs (flip inHole after)++||| Refine the current goal using some term, constructing holes for+||| all arguments that can't be inferred. Return the list of generated+||| holes.+|||+||| @ tm the term to apply to some number of goals+refine : (tm : Raw) -> Elab (List TTName)+refine tm =+    do ty <- (snd <$> check !getEnv tm) >>= forget+       g <- goalType++       -- we don't care about negative results because it'll just fail anyway+       let argCount = minus (countPi ty) (countPi g)+       newHoles <- apply tm (replicate argCount True)+       solve+       actualHoles <- getHoles+       return (filter (flip elem actualHoles) newHoles)++  where countPi : Raw -> Nat+        countPi (RBind _ (Pi _ _) body) = S (countPi body)+        countPi _ = Z+++||| Split a pair into its projections, binding them in the context+||| with the supplied names. A special case of Coq's `inversion`.+both : Raw -> TTName -> TTName -> Elab ()+both tm n1 n2 =+    do -- We don't know that the term is canonical, so let-bind projections applied to it+       (A, B) <- isPairTy (snd !(check !getEnv tm))+       remember n1 A; apply `(fst {a=~A} {b=~B} ~tm) []; solve+       remember n2 B; apply `(snd {a=~A} {b=~B} ~tm) []; solve+  where+    isPairTy : TT -> Elab (Raw, Raw)+    isPairTy `((~A, ~B) : Type) = [| MkPair (forget A) (forget B) |]+    isPairTy tm = fail [TermPart tm, TextPart "is not a pair"]++||| Let-bind all results of completely destructuring nested tuples.+|||+||| This makes them available to the `hypothesis` tactic, among others.+|||+||| @ tm the nested tuple to destructure+covering+unproduct : (tm : Raw) -> Elab ()+unproduct tm =+    do n1 <- gensym "left"+       n2 <- gensym "right"+       both tm n1 n2+       try (unproduct (Var n1))+       try (unproduct (Var n2))+++||| A special-purpose tactic that attempts to solve a goal using+||| `Refl`. This is useful for ensuring that goals in fact are trivial+||| when developing or testing other tactics; otherwise, consider+||| using `search`.+reflexivity : Elab ()+reflexivity =+    case !goalType of+      `((=) {A=~A} {B=~_} ~x ~_) =>+        do fill `(Refl {A=~A} {x=~x})+           solve+      _ => fail [ TextPart "The goal is not an equality, so"+                , NamePart `{reflexivity}+                , TextPart "is not applicable."+                ]

@@ -0,0 +1,198 @@+||| Derive implementations of decidable equality.+module Pruviloj.Derive.DecEq++import Data.Fin+import Data.Vect++import Language.Reflection.Utils++import Pruviloj.Core++import Pruviloj.Renamers+import Pruviloj.Internals++import Pruviloj.Derive.Eliminators++import Pruviloj.Disjoint+import Pruviloj.Induction+import Pruviloj.Injective++%default total+%access private+++covering+noCase : TTName -> Elab ()+noCase contra =+  do [_, nope] <- apply (Var `{No}) [True, False]+       | _ => fail [TextPart "Bad holes from", NamePart `{Tactics.apply}]+     solve+     focus nope++     -- Construct a lambda binding an assumption from which we can+     -- derive the contradiction+     h <- gensym "h"+     inj <- gensym "inj"+     attack+     intro h+     injective (Var h) inj+     unproduct (Var inj)+     ignore $ refine (Var contra) `andThen` hypothesis+     solve -- attack++partial -- TODO make covering/total+matchCase : List Raw -> Elab ()+matchCase []          = search+matchCase (tm :: tms) =+    do hs <- induction tm+       y <- unsafeNth 0 hs+       n <- unsafeNth 1 hs++       focus n; compute+       contra <- gensym "contra"+       attack; intro contra+       noCase contra; solve++       focus y; compute+       prf <- gensym "prf"+       attack; intro prf+       rewriteWith (Var prf)+       matchCase tms+       solve++spanM : (Monad m) => (a -> m Bool) -> List a -> m (List a, List a)+spanM p [] = pure ([], [])+spanM p (x::xs) =+    if !(p x)+      then do (yes, no) <- spanM p xs+              pure (x :: yes, no)+      else pure ([], x::xs)++partitionM : Monad m => (a -> m Bool) -> List a -> m (List a, List a)+partitionM p [] = pure ([], [])+partitionM p (x :: xs) =+    do (y, n) <- partitionM p xs+       if !(p x) then pure (x :: y, n) else pure (y, x :: n)++perhaps : (Alternative f) => (f a) -> (f (Maybe a))+perhaps x = (Just <$> x) <|> pure Nothing++headIs : Raw -> TTName -> Bool+headIs tm n = maybe False (==n) (headName tm)++partial+mkRhs : (fn, fam : TTName) -> Nat -> Elab ()+mkRhs fn fam k =+    case snd !getGoal of+      `(Dec ((=) {A=~A} {B=~_} ~x ~y)) =>+        let (c1, args1) = unApply x+            (c2, args2) = unApply y+        in if c1 /= c2+             then do (h :: _) <- refine (Var `{No})+                       | _ => empty+                     focus h+                     disjoint+             else do let toMakeEqual = List.filter (uncurry (/=)) (zip args1 args2)+                     tms <- for {b=Raw} toMakeEqual $ \(tm1, tm2) =>+                       do env <- getEnv+                          (tm1', ty1') <- forget tm1 >>= check env+                          (tm2', ty2') <- forget tm2 >>= check env+                          -- assume they have the same type here -+                          -- reasonable due to same constructor, but+                          -- this means order is important when+                          -- traversing+                          eq <- gensym "eq"+                          rTy <- forget ty1'+                          rTm1 <- forget tm1'+                          rTm2 <- forget tm2'+                          remember eq `(Dec ((=) {A=~rTy} {B=~rTy} ~rTm1 ~rTm2))+                          simple $+                            if headIs rTy fam+                              then do (a2::a1::hs) <- reverse <$> apply (Var fn) (replicate k True ++ [False, False])+                                      solve+                                      focus a1; fill rTm1; solve+                                      focus a2; fill rTm2; solve+                                      for_ hs $ \h => inHole h (resolveTC fn)+                              else do [_, dH, a1, a2] <- apply (Var `{decEq}) [True, False, False, False]+                                      solve+                                      focus a1; fill rTm1; solve+                                      focus a2; fill rTm2; solve+                                      focus dH; resolveTC fn+                          return (Var eq)+                     matchCase tms+      _ => fail [TextPart "Inapplicable"]++||| Attempt to derive the body of an implementation of decidable+||| equality based on an existing type signature.+|||+||| The function signature must provide enough information for the+||| deriving to occur. It must consist of zero or more non-constraint+||| arguments followed by zero or more constraint arguments, followed+||| by the two values to compare. The constraint arguments must+||| provide sufficient instances of `DecEq` to decide the equality of+||| each constructor field. The final two arguments to the function+||| declaration must be the two values that will be compared for+||| equality.+|||+||| @ fn the name of the function whose type has been declared+abstract partial -- because of mkRhs+deriveDecEq : (fn : TTName) -> Elab ()+deriveDecEq fn =+    do (_, Ref, sig') <- lookupTyExact fn+       sig <- forget sig'+       (args, `(Dec ((=) {A=~A} {B=~_} ~(Var x) ~(Var y)))) <- stealBindings sig noRenames+         | other => fail [ TextPart "Return type"+                         , RawPart (snd other)+                         , TextPart "isn't decidable equality"+                         ]++       datatype <- maybe (fail [ RawPart A+                               , TextPart "is not an application of a TC"+                               ])+                         lookupDatatypeExact+                         (headName A)++       -- the signature must be like this:+       -- 1. a collection of variable bindings (will be implicit)+       -- 2. a collection of constraints+       -- 3. the arguments x and y from the return type+       (bindings, constrs, arg1, arg2) <-+         the (Elab (List (TTName, Binder Raw),+                    List (TTName, Binder Raw),+                    (TTName, Binder Raw),+                    (TTName, Binder Raw))) $+           case reverse args of+             [] => fail [TextPart "Invalid signature"]+             [_] => fail [TextPart "Invalid signaure"]+             (a2 :: a1 :: rest) =>+               do (constrs, bindings) <- partitionM (\x => isConstr (binderTy (snd x)))+                                                    (reverse rest)+                  return (bindings, constrs, a1, a2)+       let todo = [(c1, c2) | c1 <- constructors datatype+                            , c2 <- constructors datatype]+       clauses <- for todo+                      (uncurry $ mkCase (length bindings + length constrs)+                                        (name datatype))+       defineFunction $ DefineFun fn (catMaybes clauses)+       skip++  where+    isConstr : Raw -> Elab Bool+    isConstr tm = case headName tm of+                    Just n => isTCName n+                    Nothing => return False++    partial -- mkRhs+    mkCase : Nat -> TTName -> (x, y : (TTName, List CtorArg, Raw)) -> Elab (Maybe FunClause)+    mkCase k fam (cn1, args1, _) (cn2, args2, _) =+        perhaps $ elabPatternClause+          (do (h2 :: h1 :: _) <- reverse <$>+                                   apply (Var fn) (replicate k True ++ [False, False])+              solve+              focus h1+              apply (Var cn1) (replicate (length args1) True)+              solve+              focus h2+              apply (Var cn2) (replicate (length args2) True)+              solve)+          (mkRhs fn fam k)

@@ -0,0 +1,268 @@+module Pruviloj.Derive.Eliminators++import Language.Reflection.Utils+import Data.Vect++import Pruviloj.Core+import Pruviloj.Internals.TyConInfo+import Pruviloj.Internals+import Pruviloj.Renamers+++%access private++bindParams : TyConInfo -> Elab ()+bindParams info = traverse_ (uncurry forall) (getParams info)++||| Bind indices at new names and return a renamer that's used to+||| rewrite an application of something to their designated global+||| names+bindIndices : TyConInfo -> Elab Renamer+bindIndices info = bind' (getIndices info) noRenames+  where bind' : List (TTName, Raw) -> Renamer -> Elab Renamer+        bind' []              ren = return ren+        bind' ((n, t) :: ixs) ren = do n' <- nameFrom n+                                       forall n' (alphaRaw ren t)+                                       bind' ixs (extend ren n n')++||| Return the renaming required to use the result type for this+||| binding of the indices+bindTarget : TyConInfo -> Elab (TTName, Renamer)+bindTarget info = do ren <- bindIndices info+                     tn <- gensym "target"+                     forall tn (alphaRaw ren $ result info)+                     return (tn, ren)++elabMotive : TyConInfo -> Elab ()+elabMotive info = do attack+                     ren <- bindIndices info+                     x <- gensym "scrutinee"+                     forall x (alphaRaw ren $ result info)+                     fill `(Type)+                     solve -- the attack+                     solve -- the motive type hole+++++headsMatch : Raw -> Raw -> Bool+headsMatch x y =+  case (headName x, headName y) of+    (Just n1, Just n2) => n1 == n2+    _ => False++||| Make an induction hypothesis if one is called for+mkIh : TyConInfo -> (motiveName : TTName) -> (recArg : TTName) -> (argty, fam : Raw) -> Elab ()+mkIh info motiveName recArg argty fam =+  case !(stealBindings argty noRenames) of+    (argArgs, argRes) =>+      if headsMatch argRes fam+        then do ih <- gensym "ih"+                ihT <- newHole "ihT" `(Type)+                forall ih (Var ihT)+                focus ihT+                attack+                for_ {b=()} argArgs $ \(n, b) =>+                  forall n (getBinderTy b)+                let argTm : Raw = mkApp (Var recArg) (map (Var . fst) argArgs)+                argTmTy <- forget (snd !(check !getEnv argTm))+                argHoles <- apply (Var motiveName)+                                  (replicate (length (getIndices info))+                                             True +++                                   [False])+                argH <- last argHoles+                focus argH+                fill argTm; solve+                solve -- attack+                solve -- ihT+        else return ()++elabMethodTy : TyConInfo -> TTName -> List CtorArg -> Raw -> Raw -> Elab ()+elabMethodTy info motiveName [] res ctorApp =+  do argHoles <- apply (Var motiveName)+                       (replicate (length (getIndices info)) True +++                        [False])+     argH <- last argHoles+     focus argH; fill ctorApp; solve+     solve+elabMethodTy info motiveName (CtorParameter arg  :: args) res ctorApp =+  elabMethodTy info motiveName args  res (RApp ctorApp (Var (name arg)))+elabMethodTy info motiveName (CtorField arg :: args) res ctorApp =+  do let n = name arg+     let t = type arg+     attack; forall n t+     mkIh info motiveName n t (result info)+     elabMethodTy info motiveName args res (RApp ctorApp (Var n))+     solve+++||| Bind a method for a constructor+bindMethod : TyConInfo -> (motiveName, cn : TTName) -> List CtorArg -> Raw -> Elab ()+bindMethod info motiveName cn cargs cty =+  do n <- nameFrom cn+     h <- newHole "methTy" `(Type)+     forall n (Var h)+     focus h; elabMethodTy info motiveName cargs cty (Var cn)++getElimTy : TyConInfo -> List (TTName, List CtorArg, Raw) -> Elab Raw+getElimTy info ctors =+  do ty <- runElab `(Type) $+             do bindParams info+                (scrut, iren) <- bindTarget info+                motiveN <- gensym "P"+                motiveH <- newHole "motive" `(Type)+                forall motiveN (Var motiveH)+                focus motiveH+                elabMotive info++                for_ {b=()} ctors $ \(cn, cargs, cresty) =>+                  bindMethod info motiveN cn cargs cresty+                let ret = mkApp (Var motiveN)+                                (map (Var . fst)+                                     (getIndices info) +++                                 [Var scrut])+                apply (alphaRaw iren ret) []+                solve+     forget (fst ty)++++data ElimArg = IHArgument TTName | NormalArgument TTName++instance Show ElimArg where+  show (IHArgument x) = "IHArgument " ++ show x+  show (NormalArgument x) = "NormalArgument " ++ show x++getElimClause : TyConInfo -> (elimn : TTName) -> (methCount : Nat) ->+                (TTName, List CtorArg, Raw) -> Nat -> Elab FunClause+getElimClause info elimn methCount (cn, args, resTy) whichCon =+  elabPatternClause+    (do -- Establish a hole for each parameter+        for (getParams info) {b=()} $ \(n, ty) =>+          do claim n ty+             unfocus n+++        -- Establish a hole for each argument to the constructor+        for {b=()} args $ \arg =>+          case arg of+            CtorParameter _ => return ()+            CtorField arg => do claim (name arg) (type arg)+                                unfocus (name arg)++        -- Establish a hole for the scrutinee (infer type)+        scrutinee <- newHole "scrutinee" resTy+++        -- Apply the eliminator to the proper holes+        let paramApp : Raw = mkApp (Var elimn) $+                             map (Var . fst) (getParams info)++        -- We leave the RHS with a function type: motive -> method* -> res+        -- to make it easier to map methods to constructors+        holes <- apply paramApp (replicate (length (getIndices info))+                                           True +++                                 [False])+        scr <- last holes+        focus scr; fill (Var scrutinee); solve+        solve++        -- Fill the scrutinee with the concrete constructor pattern+        focus scrutinee+        apply (mkApp (Var cn) $+                 map (\x => case x of+                              CtorParameter param => Var (name param)+                              CtorField arg => Var (name arg))+                     args)+              []+        solve)+    (do motiveN <- gensym "motive"+        intro motiveN+        prevMethods <- doTimes whichCon intro1+        methN <- gensym "useThisMethod"+        intro methN+        nextMethods <- intros++        argSpec <- Foldable.concat <$>+                     for args+                         (\x =>+                            case x of+                              CtorParameter _ => return List.Nil+                              CtorField arg =>+                                do let n = name arg+                                   let t = type arg+                                   (argArgs, argRes) <- stealBindings t noRenames+                                   if headsMatch argRes (result info) --recursive+                                     then return [ NormalArgument n+                                                 , IHArgument n+                                                 ]+                                     else return [NormalArgument n])++        argHs <- apply (Var methN) (replicate (List.length argSpec) True)+        solve++        -- Now build the recursive calls for the induction hypotheses+        for_ {a=(ElimArg, TTName)} {b=()}+             !(zipH argSpec argHs)+             (\(spec, nh) =>+                case spec of+                  NormalArgument n => do focus nh+                                         apply (Var n) []+                                         solve+                  IHArgument n =>+                    do focus nh+                       attack+                       local <- intros+                       ihHs <- apply (Var elimn) $+                         replicate (length (TyConInfo.args info)) True +++                         [False] +++                         replicate (S methCount) True+                       solve -- application++                       let (arg::motive::methods) = drop (length (TyConInfo.args info)) ihHs+                       focus arg++                       apply (mkApp (Var n) (map Var local)) []; solve+                       solve -- attack+++                       focus motive; fill (Var motiveN); solve+                       let methodArgs : List TTName = toList prevMethods ++ [methN] ++ nextMethods+                       remaining <- zipH methods methodArgs++                       for_ {b=()} remaining $ \todo =>+                         do focus (fst todo)+                            fill (Var (snd todo))+                            solve))++++  where bindLam : List (TTName, Binder Raw) -> Raw -> Raw+        bindLam [] x = x+        bindLam ((n, b)::rest) x = RBind n (Lam (getBinderTy b)) $ bindLam rest x++getElimClauses : TyConInfo -> (elimn : TTName) ->+                 List (TTName, List CtorArg, Raw) -> Elab (List FunClause)+getElimClauses info elimn ctors =+  let methodCount = length ctors+  in traverse (\(i, con) => getElimClause info elimn methodCount con i)+              (enumerate ctors)++instance Show FunClause where+  show (MkFunClause x y) = "(MkFunClause " ++ show x ++ " " ++ show y ++ ")"++abstract+deriveElim : (tyn, elimn : TTName) -> Elab ()+deriveElim tyn elimn =+  do -- Begin with some basic sanity checking: the type name uniquely+     -- determines a datatype+     (MkDatatype tyn tyconArgs tyconRes ctors') <- lookupDatatypeExact tyn++     info <- getTyConInfo tyconArgs (Var tyn)+     ctors <- traverse (processCtorArgs info) ctors'+     declareType $ Declare elimn [] !(getElimTy info ctors)+     clauses <- getElimClauses info elimn ctors++     defineFunction $ DefineFun elimn clauses+     return ()+

@@ -0,0 +1,85 @@+||| Provides a tactic for solving constructor disjointness goals.+module Pruviloj.Disjoint++import Language.Reflection.Utils++import Pruviloj.Core+import Pruviloj.Internals+import Pruviloj.Renamers++%default total+%access private++-------------------+-- PRIVATE GUTS  --+-------------------++||| Compute the name to use for a disjointness lemma.+disjointName : TTName -> TTName -> TTName+disjointName l r = NS (SN (MetaN (UN "disjoint") (SN (MetaN l r))))+                      ["Disjoint", "Pruviloj"]++||| Return the name of the disjointness lemma for two constructors,+||| defining it if necessary.+|||+||| @ l one of the constructor names+||| @ r the other constructor name+covering+getDisjointness : (l, r : TTName) -> Elab TTName+getDisjointness l r = exists <|> declare++  where exists : Elab TTName+        exists = do (yep, _, _) <- lookupTyExact (disjointName l r)+                    return yep++        notConstructor : TTName -> Elab a+        notConstructor c = fail [NamePart c, TextPart "is not a constructor"]++        covering+        declare : Elab TTName+        declare = do (l', DCon _ _, lty) <- lookupTyExact l+                       | _ => notConstructor l+                     (r', DCon _ _, rty) <- lookupTyExact r+                       | _ => notConstructor r+                     let fn = disjointName l' r'+                     when (l' == r') $+                       fail [ NamePart l', TextPart "and"+                            , NamePart r', TextPart "are clearly not disjoint!"+                            ]+                     (argsl, resl) <- stealBindings !(forget lty) noRenames+                     (argsr, resr) <- stealBindings !(forget rty) noRenames+                     let args = map {b=FunArg}+                                    (\(n, b) => MkFunArg n (binderTy b) Implicit NotErased)+                                    (argsl ++ argsr)+                     let eq : Raw = `((=) {A=~resl}+                                          {B=~resr}+                                          ~(mkApp (Var l') (map (Var . fst) argsl))+                                          ~(mkApp (Var r') (map (Var . fst) argsr)))+                     h <- gensym "h"+                     declareType $ Declare fn (args ++ [MkFunArg h eq Explicit NotErased]) `(Void)+                     defineFunction $ DefineFun fn []+                     return fn++----------------------+-- PUBLIC INTERFACE --+----------------------+++||| Solve a goal of the form `(C1 x1 x2 ... xn = C2 x1 x2 ... xn) ->+||| Void` for disjoint constructors `C1` and `C2`.+public covering+disjoint : Elab ()+disjoint =+  do compute+     g <- snd <$> getGoal+     case g of+       `(((=) {A=~A} {B=~B} ~a ~b) -> Void) =>+         do Just lHead <- headName <$> forget a+              | Nothing => fail [TermPart a, TextPart "doesn't have a name at the head"]+            Just rHead <- headName <$> forget b+              | Nothing => fail [TermPart b, TextPart "doesn't have a name at the head"]+            [] <- refine (Var !(getDisjointness lHead rHead))+              | _ => fail [TextPart "Didn't solve argument to disjointness lemma"]+            skip+       ty =>+         fail [NamePart `{disjoint}, TextPart "is not applicable to goal", TermPart ty]

@@ -0,0 +1,157 @@+module Pruviloj.Induction++import Language.Reflection.Utils++import Pruviloj.Core+import Pruviloj.Derive.Eliminators+import Pruviloj.Internals.TyConInfo+import Pruviloj.Internals+import Pruviloj.Renamers+++%access private++-- To perform induction:+--  1. Type check the thing to do induction on+--  2. If its type is not an inductive family, error+--  3. Ensure that there exists an eliminator for the family+--  4. Abstract the goal over the scrutinee to get the motive+--  5. Apply the eliminator to the scrutinee and motive, with holes for methods+--  6. Return these holes+++elimN : TTName -> TTName+elimN n = NS (SN $ MetaN (UN "elim") n) ["Eliminators", "Induction", "Pruviloj"]++mutual+  alphaEqual : (subst : TTName -> Maybe TTName) -> Raw -> Raw -> Bool+  alphaEqual subst (Var n) (Var m)  =+    case subst n of+      Just n' => n' == m -- both are bound if this has been put in the subst+      Nothing => n == m -- free+  alphaEqual subst (RBind n b tm) (RBind m b' tm') =+      alphaEqualBinders subst b b' &&+      alphaEqual (extend subst n m) tm tm'+  alphaEqual subst (RApp f x) (RApp g y) =+      alphaEqual subst f g && alphaEqual subst x y+  alphaEqual subst RType RType  = True+  alphaEqual subst (RUType u) (RUType u') = u == u'+  alphaEqual subst (RConstant c) (RConstant c')  = c == c'+  alphaEqual subst _ _ = False++  alphaEqualBinders : (subst : TTName -> Maybe TTName) -> Binder Raw -> Binder Raw -> Bool+  alphaEqualBinders subst (Lam tm) (Lam tm') =+      alphaEqual subst tm tm'+  alphaEqualBinders subst (Pi tm1 tm2) (Pi tm1' tm2') =+      alphaEqual subst tm1 tm1' &&+      alphaEqual subst tm2 tm2'+  alphaEqualBinders subst (Let tm1 tm2) (Let tm1' tm2') =+      alphaEqual subst tm1 tm1' &&+      alphaEqual subst tm2 tm2'+  alphaEqualBinders subst (Hole tm) (Hole tm') =+      alphaEqual subst tm tm'+  alphaEqualBinders subst (GHole tm) (GHole tm') =+      alphaEqual subst tm tm'+  alphaEqualBinders subst (Guess tm1 tm2) (Guess tm1' tm2') =+      alphaEqual subst tm1 tm1' &&+      alphaEqual subst tm2 tm2'+  alphaEqualBinders subst (PVar tm) (PVar tm') =+      alphaEqual subst tm tm'+  alphaEqualBinders subst (PVTy tm) (PVTy tm') =+      alphaEqual subst tm tm'+  alphaEqualBinders subst _ _ = False++generalize : (hint : String) -> (ctxt, subject : Raw) -> Elab (TTName, Raw)+generalize hint ctxt subj = do n <- gensym hint+                               return (n, !(gen' n ctxt subj))+  where+    mutual+      gen' : TTName -> Raw -> Raw -> Elab Raw+      gen' var outer inner = if alphaEqual (const Nothing) outer inner+                               then return (Var var)+                               else breakAndRecurse var outer inner++      genB : TTName -> Binder Raw -> Raw -> Elab (Binder Raw)+      genB n (Lam ty)       inner = [| Lam (gen' n ty inner) |]+      genB n (Pi ty ty')    inner = [| Pi (gen' n ty inner) (gen' n ty' inner) |]+      genB n (Let ty val)   inner = [| Let (gen' n ty inner) (gen' n val inner) |]+      genB n (Hole ty)      inner = [| Hole (gen' n ty inner) |]+      genB n (GHole ty)     inner = [| GHole (gen' n ty inner) |]+      genB n (Guess ty val) inner = [| Guess (gen' n ty inner) (gen' n val inner) |]+      genB n (PVar ty)      inner = [| PVar (gen' n ty inner) |]+      genB n (PVTy ty)      inner = [| PVTy (gen' n ty inner) |]++      breakAndRecurse : TTName -> Raw -> Raw -> Elab Raw+      breakAndRecurse var (RBind n b tm) inner =+          -- Prevent variable capture by alpha-converting to a unique name+          do n' <- nameFrom n+             b' <- genB var b inner+             body' <- gen' var (alphaRaw (rename n n') tm) inner+             return $ RBind n' b' body'+      breakAndRecurse var (RApp tm tm') inner =+          [| RApp (gen' var tm inner) (gen' var tm' inner) |]+      breakAndRecurse var other inner = return other+++countBinders : TT -> Nat+countBinders (Bind _ _ tm) = S (countBinders tm)+countBinders _ = Z++++indexVals : Raw -> TyConInfo -> List Raw+indexVals tm info =+  do let (var, tyArgs) = unApply tm+     let argsTogether = zip tyArgs (args info)+     (argVal, TyConIndex _) <- argsTogether+             | _ => empty+     return argVal++makeMotive : (info : TyConInfo) -> (subj, subjTy, goal : Raw) -> Elab ()+makeMotive info sub subjTy goal =+    makeMotive' (indexVals subjTy info) goal+  where+    makeMotive' : List Raw -> Raw -> Elab ()+    makeMotive' [] r = do (n, r') <- generalize "subj" r sub+                          attack+                          intro n+                          exact r'+                          solve -- attack+    makeMotive' (i :: is) r = do (n, r') <- generalize "i" r i+                                 attack+                                 intro n+                                 makeMotive' is r'+                                 solve --attack++||| Perform induction on some expression to solve the current+||| goal. Return a list of new holes to be solved.+public+induction : Raw -> Elab (List TTName)+induction subj =+    do g <- goalType+       (_, ty) <- check !getEnv subj+       ty' <- forget ty+       case headName ty' of+         Nothing => fail [TermPart ty, TextPart "is not an inductive family"]+         Just fam =>+           do let elim = elimN fam+              (_,_,elimTy) <- (lookupTyExact elim) <|> (do deriveElim fam elim+                                                           lookupTyExact elim)+              tydef <- lookupDatatypeExact fam+              info <- getTyConInfo (tyConArgs tydef) (tyConRes tydef)+              argHoles <- apply (Var elim)+                                (replicate (length (args info)) True +++                                 [False, False] ++ -- scrutinee, motive+                                 replicate (length (constructors tydef)) False)+              solve++              -- Apply the eliminator to our scrutinee+              scrutH <- unsafeNth (length (args info)) argHoles+              focus scrutH+              apply subj []+              solve++              motiveH <- unsafeNth (length (args info) + 1) argHoles+              focus motiveH; makeMotive info subj ty' g++              return (drop (2 + length (tyConArgs tydef)) argHoles)

@@ -0,0 +1,122 @@+module Pruviloj.Injective++import Language.Reflection.Utils++import Pruviloj.Core+import Pruviloj.Internals+import Pruviloj.Renamers++%default total+%access private++-------------------+-- PRIVATE GUTS  --+-------------------++||| Compute the name for a constructor's injectivity lemma+injName : TTName -> TTName+injName cn = NS (SN (MetaN `{{injectivity}} cn)) ["Injective", "Pruviloj"]++||| Provide an error message for when non-constructor names are passed+notConstructor : TTName -> Elab a+notConstructor c = fail [NamePart c, TextPart "is not a constructor"]++covering+getInjectivity : (cn : TTName) -> Elab TTName+getInjectivity cn = exists <|> declare+  where exists : Elab TTName+        exists = do (fn, Ref, _) <- lookupTyExact (injName cn)+                      | (fn, _, _) => fail [TextPart "Bad earlier declaration of", NamePart fn]+                    return fn++        covering+        declare : Elab TTName+        declare = do (cn', DCon _ _, cty) <- lookupTyExact cn+                       | _ => notConstructor cn+                     let fn = injName cn'+                     (args1, res1) <- stealBindings !(forget cty) noRenames+                     (args2, res2) <- stealBindings !(forget cty) noRenames+                     let impls1 = map (\(n, b) => MkFunArg n (binderTy b) Implicit NotErased)+                                      args1+                     let impls2 = map (\(n, b) => MkFunArg n (binderTy b) Implicit NotErased)+                                      args2+                     let res = foldr (\t1, t2 => RApp (RApp (Var `{Pair}) t1) t2)+                                     `(() : Type)+                                     (map (\(a1, a2) =>+                                            `((=) {A=~(type a1)}+                                                  {B=~(type a2)}+                                                  ~(Var (name a1))+                                                  ~(Var (name a2))))+                                          (zip impls1 impls2))++                     declareType $ Declare fn (impls1 ++ impls2 +++                                               [ MkFunArg !(gensym "arg")+                                                          `((=) {A=~res1}+                                                                {B=~res2}+                                                                ~(mkApp (Var cn)+                                                                        (map (Var . fst) args1))+                                                                ~(mkApp (Var cn)+                                                                        (map (Var . fst) args2)))+                                                          Explicit+                                                          NotErased])++                                           res+                     clause <- elabPatternClause+                                 (do (h::_) <- reverse <$>+                                                 apply (Var fn)+                                                       (replicate (2 * length args1)+                                                                  True +++                                                        [False])+                                       | _ => fail [TextPart "Missing hole"]+                                     solve+                                     focus h; search)+                                 search -- rhs is conjunction of Refls+                     defineFunction $+                       DefineFun fn [clause]+                     return fn++countBinders : TT -> Nat+countBinders (Bind _ _ body) = S (countBinders body)+countBinders _ = Z+++----------------------+-- PUBLIC INTERFACE --+----------------------+++||| Given an equality of the form `(C x1 ... xn = C y1 ... yn)`,+||| generate an product of the equalities `(x1 = y1)` ... `(xn = yn)`.+|||+||| The equalities are let-bound to the provided name.+|||+||| @ tm the equality to exploit injectivity on+||| @ n the name at which to bind the result+covering public+injective : (tm : Raw) -> (n : TTName) -> Elab ()+injective tm n =+  do (_, ty) <- check !getEnv tm+     case !(forget ty) of+       `((=) {A=~A} {B=~B} ~x ~y) =>+         case (headName x, headName y) of+           (Just xHd, Just yHd) =>+             if xHd /= yHd+               then fail [ TextPart "Mismatch between", NamePart xHd+                         , TextPart "and", NamePart yHd+                         ]+               else do fn <- getInjectivity xHd+                       tyH <- newHole "ty" `(Type)+                       tmH <- newHole "tm" (Var tyH)++                       letbind n (Var tyH) (Var tmH)+                       focus tmH+                       (_, _, fnTy) <- lookupTyExact fn++                       (arg :: _) <- reverse <$> apply (Var fn) (replicate (pred (countBinders fnTy)) True ++ [False])+                         | _ => fail [TextPart "No hole for argument"]+                       solve++                       focus arg; apply tm []; solve+           _ => fail [TextPart "oops"]++       _ => fail [TextPart "can't use injectivity on non-equality"]

@@ -0,0 +1,154 @@+||| Internal details of the library, not for public consumption.+module Pruviloj.Internals+++import Pruviloj.Core+import Pruviloj.Renamers++import Data.Vect++||| Get the name of a reflected type constructor argument.+tyConArgName : TyConArg -> TTName+tyConArgName (TyConParameter a) = name a+tyConArgName (TyConIndex a) = name a++||| Modify the name of a reflected type constructor argument.+setTyConArgName : TyConArg -> TTName -> TyConArg+setTyConArgName (TyConParameter a) n = TyConParameter (record {name = n} a)+setTyConArgName (TyConIndex a) n = TyConIndex (record {name = n} a)++||| Modify the type of a reflected type constructor argument using some function.+updateTyConArgTy : (Raw -> Raw) -> TyConArg -> TyConArg+updateTyConArgTy f (TyConParameter a) =+    TyConParameter (record {type = f (type a) } a)+updateTyConArgTy f (TyConIndex a) =+    TyConIndex (record {type = f (type a) } a)++unApply : Raw -> (Raw, List Raw)+unApply tm = unApply' tm []+  where unApply' : Raw -> List Raw -> (Raw, List Raw)+        unApply' (RApp f x) xs = unApply' f (x::xs)+        unApply' notApp xs = (notApp, xs)++mkApp : Raw -> List Raw -> Raw+mkApp f [] = f+mkApp f (x :: xs) = mkApp (RApp f x) xs++||| Grab the binders from around a term, alpha-converting to make+||| their names unique+partial+stealBindings : Raw -> (nsubst : TTName -> Maybe TTName) -> Elab (List (TTName, Binder Raw), Raw)+stealBindings (RBind n b tm) nsubst =+  do n' <- nameFrom n+     (bindings, result) <- stealBindings tm (extend nsubst n n')+     return ((n', map (alphaRaw nsubst) b) :: bindings, result)+stealBindings tm nsubst = return ([], alphaRaw nsubst tm)++||| Get the last element of a list. Fail on empty lists.+last : List a -> Elab a+last [] = fail [TextPart "Unexpected empty list"]+last [x] = return x+last (_::x::xs) = last (x::xs)++||| Grab the binders from around a term, assuming that they have been+||| previously uniquified+extractBinders : Raw -> (List (TTName, Binder Raw), Raw)+extractBinders (RBind n b tm) = let (bs, res) = extractBinders tm+                                in ((n, b) :: bs, res)+extractBinders tm = ([], tm)+++||| Get the type annotation from a binder+getBinderTy : Binder t -> t+getBinderTy (Lam t) = t+getBinderTy (Pi t _) = t+getBinderTy (Let t _) = t+getBinderTy (Hole t) = t+getBinderTy (GHole t) = t+getBinderTy (Guess t _) = t+getBinderTy (PVar t) = t+getBinderTy (PVTy t) = t++||| Map a list `[x1, x2, ..., xn]` to `[(0, x1), (1, x2), ..., (n-1, xn)]`+enumerate : List a -> List (Nat, a)+enumerate xs = enumerate' xs 0+  where enumerate' : List a -> Nat -> List (Nat, a)+        enumerate' [] _ = []+        enumerate' (x::xs) n = (n, x) :: enumerate' xs (S n)++bindPats : List (TTName, Binder Raw) -> Raw -> Raw+bindPats [] res = res+bindPats ((n, b)::bs) res = RBind n (PVar (getBinderTy b)) $ bindPats bs res++bindPatTys : List (TTName, Binder Raw) -> Raw -> Raw+bindPatTys [] res = res+bindPatTys ((n, b)::bs) res = RBind n (PVTy (getBinderTy b)) $ bindPatTys bs res+++||| Helper for elaborating pattern clauses. This helper takes care of+||| inferring the type of the left-hand side and bringing that+||| information onward to the right-hand side.+|||+||| While elaborating the left-hand side, the proof term contains a+||| Sigma type. This is part of the type inference going on and will+||| be removed.+|||+||| @ lhs the tactic script to establish the left-hand side of the+|||       clause. It should cause an application of the term being+|||       defined. Any holes left behind will be converted to pattern+|||       variables with the same name.+||| @ rhs the tactic script to establish the right side of the clause.+|||       It will be run in a context where the pattern variables are+|||       already bound, and should leave behind no holes.+partial+elabPatternClause : (lhs, rhs : Elab ()) -> Elab FunClause+elabPatternClause lhs rhs =+  do -- Elaborate the LHS in a context where its type will be solved via unification+     (pat, _) <- runElab `(Infer) $+                    do th <- newHole "finalTy" `(Type)+                       patH <- newHole "pattern" (Var th)+                       fill `(MkInfer ~(Var th) ~(Var patH))+                       solve+                       focus patH+                       lhs+                       -- Convert all remaining holes to pattern variables+                       for_ {b=()} !getHoles $ \h =>+                         do focus h; patvar h+     (pvars, `(MkInfer ~rhsTy ~lhsTm)) <- extractBinders <$> forget pat+        | fail [TextPart "Couldn't infer type of left-hand pattern"]+     rhsTm <- runElab (bindPatTys pvars rhsTy) $+                do -- Introduce all the pattern variables from the LHS+                   repeatUntilFail bindPat <|> return ()+                   rhs+     realRhs <- forget (fst rhsTm)+     return $ MkFunClause (bindPats pvars lhsTm) realRhs++||| Introduce a unique binder name, returning it+intro1 : Elab TTName+intro1 = do g <- snd <$> getGoal+            case g of+              Bind n (Pi _ _) _ => do n' <- nameFrom n+                                      intro n'+                                      return n'+              _ => fail [ TextPart "Can't intro1 because goal"+                        , TermPart g+                        , TextPart "isn't a function type."]+++||| Repeat an action some number of times, saving the results.+doTimes : Applicative m => (n : Nat) -> m a -> m (Vect n a)+doTimes Z     x = pure []+doTimes (S k) x = [| x :: (doTimes k x) |]++||| Zip two lists, failing if their lengths don't match.+zipH : List a -> List b -> Elab (List (a, b))+zipH [] [] = return []+zipH (x::xs) (y::ys) = ((x, y) ::) <$> zipH xs ys+zipH _ _ = fail [TextPart "length mismatch"]++unsafeNth : Nat -> List a -> Elab a+unsafeNth _     []        = fail [TextPart "Ran out of list elements"]+unsafeNth Z     (x :: _)  = return x+unsafeNth (S k) (_ :: xs) = unsafeNth k xs++

@@ -0,0 +1,108 @@+module Pruviloj.Derive.TyConInfo++import Pruviloj.Core+import Pruviloj.Internals+import Pruviloj.Renamers++import Language.Reflection.Utils++++||| A representation of a type constructor in which all argument names+||| are made unique and they are separated into params and then+||| indices.+record TyConInfo where+  constructor MkTyConInfo+  ||| Invariant: the names of the args have been made unique+  args : List TyConArg+  ||| The type constructor, applied to its arguments+  result : Raw++%name TyConInfo info++getParams : TyConInfo -> List (TTName, Raw)+getParams info = mapMaybe param (args info)+  where param : TyConArg -> Maybe (TTName, Raw)+        param (TyConParameter a) = Just (name a, type a)+        param _ = Nothing++getIndices : TyConInfo -> List (TTName, Raw)+getIndices info = mapMaybe index (args info)+  where index : TyConArg -> Maybe (TTName, Raw)+        index (TyConIndex a) = Just (name a, type a)+        index _ = Nothing++||| Rename a bound variable across a telescope+renameIn : (from, to : TTName) -> List (TTName, Raw) -> List (TTName, Raw)+renameIn from to [] = []+renameIn from to ((n, ty)::tele) =+    (n, alphaRaw (rename from to) ty) ::+      if from == n+        then tele+        else renameIn from to tele++||| Rename a free variable in type constructor info (used to implement+||| alpha-conversion for unique binder names, hence the odd name)+alphaTyConInfo : (TTName -> Maybe TTName) -> TyConInfo -> TyConInfo+alphaTyConInfo ren (MkTyConInfo [] res) = MkTyConInfo [] (alphaRaw ren res)+alphaTyConInfo ren (MkTyConInfo (tcArg::tcArgs) res) =+  let MkTyConInfo tcArgs' res' = alphaTyConInfo (restrict ren (tyConArgName tcArg)) (MkTyConInfo tcArgs res)+      tcArg' = updateTyConArgTy (alphaRaw ren) tcArg+  in MkTyConInfo (tcArg'::tcArgs') res'++getTyConInfo' : List TyConArg -> Raw -> (TTName -> Maybe TTName) -> Elab TyConInfo+getTyConInfo' [] res _ = return (MkTyConInfo [] res)+getTyConInfo' (tcArg::tcArgs) res ren =+  do let n = tyConArgName tcArg+     n' <- nameFrom n+     let ren' = extend ren n n'+     -- n' is globally unique so we don't worry about scope+     next <- getTyConInfo' tcArgs (RApp res (Var n')) ren'+     return $ alphaTyConInfo ren' $+       record {args = setTyConArgName tcArg n' :: args next} next++getTyConInfo : List TyConArg -> Raw -> Elab TyConInfo+getTyConInfo args res = getTyConInfo' args res (const Nothing)++||| Convert the parameter names in a constructor to their global unique versions+processCtorArgs : TyConInfo -> (TTName, List CtorArg, Raw) -> Elab (TTName, List CtorArg, Raw)+processCtorArgs info (cn, cargs, resTy) =+    do (args', ty') <- convert' (const Nothing) cargs resTy info+       return (cn, args', ty')+  where+    ||| Find the name that was assigned to a given parameter+    ||| by comparing positions in the TyConInfo+    findParam : TTName -> List Raw -> List TyConArg -> Elab TTName+    findParam paramN (Var n :: args) (TyConParameter a :: tcArgs) =+      if n == paramN+        then return (name a)+        else findParam paramN args tcArgs+    findParam paramN (_ :: args) (_ :: tcArgs) =+      findParam paramN args tcArgs+    findParam paramN _ _ = fail [ TextPart "Parameter"+                                , NamePart paramN+                                , TextPart "not found."+                                ]++    convert' : (TTName -> Maybe TTName) ->+               List CtorArg -> Raw ->+               TyConInfo -> Elab (List CtorArg, Raw)+    convert' subst [] ty info = return ([], alphaRaw subst ty)+    convert' subst (CtorField a :: args) ty info =+      do n' <- nameFrom (name a)+         let a' = record {+                    name = n'+                  , type = alphaRaw subst (type a)+                  } a+         let subst' = extend subst (name a) n'+         (args', ty') <- convert' subst' args ty info+         return (CtorField a' :: args', ty')+    convert' subst (CtorParameter a :: ctorArgs) ty info =+      do n' <- findParam (name a) (snd (unApply ty)) (args info)+         let a' = record {+                    name = n'+                  , type = alphaRaw subst (type a)+                  } a+         let subst' = extend subst (name a) n'+         (args', ty') <- convert' subst' ctorArgs ty info+         return (CtorParameter a' :: args', ty')

@@ -0,0 +1,42 @@+module Pruviloj.Renamers++import Language.Reflection.Utils++||| A renamer keeps track of names to be substituted+Renamer : Type+Renamer = TTName -> Maybe TTName++||| A renamer that renames nothing+noRenames : Renamer+noRenames = const Nothing++||| Cause a renamer to forget a renaming+restrict : Renamer -> TTName -> Renamer+restrict f n n' = if n == n' then Nothing else f n'++||| Extend a renamer with a new renaming+extend : Renamer -> TTName -> TTName -> Renamer+extend f n n' n'' = if n'' == n then Just n' else f n''++||| Create a new renamer+|||+||| @ from the old name+||| @ to the new name+rename : (from, to : TTName) -> Renamer+rename from to = extend noRenames from to++||| Alpha-convert `Raw` terms+||| @ subst a renamer+partial+alphaRaw : (subst : Renamer) -> Raw -> Raw+alphaRaw subst (Var n) with (subst n)+  alphaRaw subst (Var n) | Nothing = Var n+  alphaRaw subst (Var n) | Just n' = Var n'+alphaRaw subst (RBind n b tm) =+  let subst' = restrict subst n+      b' = map (alphaRaw subst) b+  in RBind n b' (alphaRaw subst' tm)+alphaRaw subst (RApp tm tm') = RApp (alphaRaw subst tm) (alphaRaw subst tm')+alphaRaw subst RType = RType+alphaRaw subst (RUType x) = RUType x+alphaRaw subst (RConstant c) = RConstant c

@@ -0,0 +1,13 @@+package pruviloj++opts    = "--nobasepkgs -i ../prelude -i ../base"+modules = Pruviloj+        , Pruviloj.Core+        , Pruviloj.Derive.DecEq+        , Pruviloj.Derive.Eliminators+        , Pruviloj.Disjoint+        , Pruviloj.Induction+        , Pruviloj.Injective+        , Pruviloj.Internals+        , Pruviloj.Internals.TyConInfo+        , Pruviloj.Renamers

@@ -21,6 +21,7 @@     init_gmpalloc();      init_nullaries();+    init_signals();      _idris__123_runMain0_125_(vm, NULL); 

@@ -1,4 +1,5 @@ #include <assert.h>+#include <errno.h>  #include "idris_rts.h" #include "idris_gc.h"@@ -72,6 +73,7 @@     init_threaddata(vm);     init_gmpalloc();     init_nullaries();+    init_signals();      return vm; }@@ -92,6 +94,12 @@ #endif } +void init_signals() {+#if (__linux__ || __APPLE__ || __FreeBSD__)+    signal(SIGPIPE, SIG_IGN);+#endif+}+ Stats terminate(VM* vm) {     Stats stats = vm->stats;     STATS_ENTER_EXIT(stats)@@ -925,6 +933,14 @@  void idris_freeMsg(Msg* msg) {     free(msg);+}++int idris_errno() {+    return errno;+}++char* idris_showerror(int err) {+    return strerror(err); }  VAL* nullary_cons;

@@ -9,6 +9,9 @@ #include <pthread.h> #endif #include <stdint.h>+#if (__linux__ || __APPLE__ || __FreeBSD__)+#include <signal.h>+#endif  #include "idris_heap.h" #include "idris_stats.h"@@ -252,9 +255,14 @@  #define NULL_CON(x) nullary_cons[x] +int idris_errno();+char* idris_showerror(int err);+ extern VAL* nullary_cons; void init_nullaries(); void free_nullaries();++void init_signals();  void* vmThread(VM* callvm, func f, VAL arg); 

@@ -4,6 +4,7 @@ #include "idris_gc.h" #include <sys/select.h> #include <fcntl.h>+#include <errno.h> #include <stdio.h> #include <time.h> @@ -84,6 +85,25 @@ VAL idris_time() {     time_t t = time(NULL);     return MKBIGI(t);+}++VAL idris_mkFileError(VM* vm) {+    VAL result;+    switch(errno) {+        // Make sure this corresponds to the FileError structure in+        // Prelude.File+        case ENOENT:+            idris_constructor(result, vm, 2, 0, 0);+            break;+        case EACCES:+            idris_constructor(result, vm, 3, 0, 0);+            break;+        default:+            idris_constructor(result, vm, 4, 1, 0);+            idris_setConArg(result, 0, MKINT((intptr_t)errno));+            break;+    }+    return result; }  void idris_forceGC(void* vm) {

@@ -14,6 +14,8 @@ int fileError(void* h); // return 0 on success int idris_writeStr(void*h, char* str);+// construct a file error structure (see Prelude.File) from errno+VAL idris_mkFileError(VM* vm);  void* do_popen(const char* cmd, const char* mode); int fpoll(void* h);

@@ -66,7 +66,7 @@            MavenProject -> putStrLn ("FAILURE: output type not supported")            Raw -> writeSource out cout            _ -> do-             (tmpn, tmph) <- tempfile+             (tmpn, tmph) <- tempfile ".c"              hPutStr tmph cout              hFlush tmph              hClose tmph@@ -78,7 +78,7 @@                         gccFlags iface ++                         -- # Any flags defined here which alter the RTS API must also be added to config.mk                         ["-DHAS_PTHREAD", "-DIDRIS_ENABLE_STATS",-                         "-I."] ++ objs ++ ["-x", "c"] ++ envFlags +++                         "-I."] ++ objs ++ envFlags ++                         (if (exec == Executable) then [] else ["-c"]) ++                         [tmpn] ++                         (if not iface then concatMap words libFlags else []) ++@@ -95,7 +95,7 @@  headers xs =   concatMap-    (\h -> "#include <" ++ h ++ ">\n")+    (\h -> "#include \"" ++ h ++ "\"\n")     (xs ++ ["idris_rts.h", "idris_bitstring.h", "idris_stdfgn.h"])  debug TRACE = "#define IDRIS_TRACE\n\n"

@@ -27,6 +27,7 @@ import Data.Traversable hiding (mapM) import System.IO import System.Directory+import System.FilePath  import qualified Data.Map.Strict as M import qualified Data.Text as T@@ -113,6 +114,10 @@   let js = concatMap (translateDecl info) bytecode   let full = concatMap processFunction js   let code = deadCodeElim full+  let ext = takeExtension filename+  let isHtml = target == JavaScript && ext == ".html"+  let htmlPrologue = T.pack "<!doctype html><html><head><script>\n"+  let htmlEpilogue = T.pack "\n</script></head><body></body></html>"   let (cons, opt) = optimizeConstructors code   let (header, rt) = case target of                           Node -> ("#!/usr/bin/env node\n", "-node")@@ -132,12 +137,15 @@                 ++ idrRuntime                 ++ tgtRuntime                 )-  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-                           )+  let jsSource = T.pack runtime+                 `T.append` T.concat (map compileJS opt)+                 `T.append` T.concat (map compileJS cons)+                 `T.append` main+                 `T.append` invokeMain+  let source = if isHtml+                    then htmlPrologue `T.append` jsSource `T.append` htmlEpilogue+                    else jsSource+  writeSourceText filename source   setPermissions filename (emptyPermissions { readable   = True                                             , executable = target == Node                                             , writable   = True

@@ -167,7 +167,7 @@     snRank (InstanceN n args) = "2" ++ nameRank n ++ concatMap show args     snRank (ParentN n s) = "3" ++ nameRank n ++ show s     snRank (MethodN n) = "4" ++ nameRank n-    snRank (CaseN n) = "5" ++ nameRank n+    snRank (CaseN _ n) = "5" ++ nameRank n     snRank (ElimN n) = "6" ++ nameRank n     snRank (InstanceCtorN n) = "7" ++ nameRank n     snRank (WithN i n) = "8" ++ nameRank n ++ show i@@ -205,7 +205,7 @@     (args, sc) = cases_runtime cd      -- Always attempt to inline functions arising from 'case' expressions-    caseName (SN (CaseN _)) = True+    caseName (SN (CaseN _ _)) = True     caseName (SN (WithN _ _)) = True     caseName (NS n _) = caseName n     caseName _ = False

@@ -346,6 +346,14 @@ addToCalledG :: Name -> [Name] -> Idris () addToCalledG n ns = return () -- TODO +addDeprecated :: Name -> String -> Idris ()+addDeprecated n reason = do i <- getIState+                            putIState $ i { idris_deprecated = addDef n reason (idris_deprecated i) }++getDeprecated :: Name -> Idris (Maybe String)+getDeprecated n = do i <- getIState+                     return $ lookupCtxtExact n (idris_deprecated i)+ push_estack :: Name -> Bool -> Idris () push_estack n inst     = do i <- getIState@@ -1344,7 +1352,7 @@         let badnames = filter (\n -> not (implicitable n) &&                                      n `notElem` (map iname uimpls)) ns         when (not (null badnames)) $-           throwError (At fc (Elaborating "type of " n+           throwError (At fc (Elaborating "type of " n Nothing                          (NoSuchVariable (head badnames))))         let cs = getArgnames t -- get already bound names         let addimpls = filter (\n -> iname n `notElem` cs) uimpls@@ -1385,7 +1393,11 @@             = (n, (p, t)) : collectImps sc         collectImps _ = [] -        getImps (Bind n (Pi (Just _) _ _) sc) imps = getImps sc imps+        scopedimpl (Just i) = not (toplevel_imp i)+        scopedimpl _ = False++        getImps (Bind n (Pi i _ _) sc) imps +             | scopedimpl i = getImps sc imps         getImps (Bind n (Pi _ t _) sc) imps             | Just (p, t') <- lookup n imps = argInfo n p t' : getImps sc imps          where@@ -1548,9 +1560,9 @@     pibind using []     sc = sc     pibind using (n:ns) sc       = case lookup n using of-            Just ty -> PPi (Imp [] Dynamic False Nothing)+            Just ty -> PPi (Imp [] Dynamic False (Just (Impl False True)))                            n NoFC ty (pibind using ns sc)-            Nothing -> PPi (Imp [InaccessibleArg] Dynamic False Nothing)+            Nothing -> PPi (Imp [InaccessibleArg] Dynamic False (Just (Impl False True)))                            n NoFC Placeholder (pibind using ns sc)  -- Add implicit arguments in function calls@@ -1694,7 +1706,9 @@      -> [PArg] -- ^ initial arguments (if in an expression)      -> Either Err PTerm aiFn topname inpat True qq imp_meths ist fc f ffc ds [] _-  = case lookupDef f (tt_ctxt ist) of+  | inpat && implicitable f && unqualified f = Right $ PPatvar ffc f+  | otherwise +     = case lookupDef f (tt_ctxt ist) of         [] -> Right $ PPatvar ffc f         alts -> let ialts = lookupCtxtName f (idris_implicits ist) in                     -- trace (show f ++ " " ++ show (fc, any (all imp) ialts, ialts, any constructor alts)) $@@ -1707,6 +1721,10 @@           imp _ = True --           allImp [] = False           allImp xs = all imp xs++          unqualified (NS _ _) = False+          unqualified _ = True+           constructor (TyDecl (DCon _ _ _) _) = True           constructor _ = False @@ -1887,9 +1905,11 @@     su tm@(PRef fc hl f)        | (Bind n (Pi _ t _) sc :_) <- lookupTy f (tt_ctxt i)           = Placeholder-       | (TType _ : _) <- lookupTy f (tt_ctxt i)+       | (TType _ : _) <- lookupTy f (tt_ctxt i),+         not (implicitable f)           = PHidden tm-       | (UType _ : _) <- lookupTy f (tt_ctxt i)+       | (UType _ : _) <- lookupTy f (tt_ctxt i),+         not (implicitable f)           = PHidden tm     su (PApp fc f@(PRef _ _ fn) args)        -- here we use canBeDConName because the impossible pattern

@@ -259,7 +259,8 @@     idris_symbols :: M.Map Name Name, -- ^ Symbol table (preserves sharing of names)     idris_exports :: [Name], -- ^ Functions with ExportList     idris_highlightedRegions :: [(FC, OutputAnnotation)], -- ^ Highlighting information to output-    idris_parserHighlights :: [(FC, OutputAnnotation)] -- ^ Highlighting information from the parser+    idris_parserHighlights :: [(FC, OutputAnnotation)], -- ^ Highlighting information from the parser+    idris_deprecated :: Ctxt String -- ^ Deprecated names and explanation    }  -- Required for parsers library, and therefore trifecta@@ -335,6 +336,7 @@               | IBCUsage (Name, Int)               | IBCExport Name               | IBCAutoHint Name Name+              | IBCDeprecate Name String   deriving Show  -- | The initial state for the compiler@@ -349,6 +351,7 @@                    [] [] Nothing [] Nothing [] [] Nothing Nothing [] Hidden False [] Nothing [] []                    (RawOutput stdout) True defaultTheme [] (0, emptyContext) emptyContext M.empty                    AutomaticWidth S.empty S.empty [] Nothing Nothing [] [] M.empty [] [] []+                   emptyContext  -- | The monad for the main REPL - reading and processing files and updating -- global state (hence the IO inner monad).@@ -506,10 +509,12 @@          | Client String          | ShowOrigErr          | AutoWidth -- ^ Automatically adjust terminal width-         | AutoSolve -- ^ Automatically issue "solve" tactic in interactive prover+         | AutoSolve -- ^ Automatically issue "solve" tactic in old-style interactive prover          | UseConsoleWidth ConsoleWidth          | DumpHighlights          | DesugarNats+         | NoElimDeprecationWarnings -- ^ Don't show deprecation warnings for %elim+         | NoOldTacticDeprecationWarnings -- ^ Don't show deprecation warnings for old-style tactics     deriving (Show, Eq)  data ElabShellCmd = EQED | EAbandon | EUndo | EProofState | EProofTerm@@ -582,9 +587,9 @@ is_scoped (Imp _ _ _ s) = s is_scoped _ = Nothing -impl = Imp [] Dynamic False Nothing-forall_imp = Imp [] Dynamic False (Just (Impl False))-forall_constraint = Imp [] Dynamic False (Just (Impl True))+impl = Imp [] Dynamic False (Just (Impl False True))+forall_imp = Imp [] Dynamic False (Just (Impl False False))+forall_constraint = Imp [] Dynamic False (Just (Impl True False)) expl = Exp [] Dynamic False expl_param = Exp [] Dynamic True constraint = Constraint [] Static@@ -706,6 +711,7 @@                  DNameHint Name FC [(Name, FC)] |                  DErrorHandlers Name FC Name FC [(Name, FC)] |                  DLanguage LanguageExt |+                 DDeprecate Name String |                  DUsed FC Name Name  -- | A set of instructions for things that need to happen in IState

@@ -50,8 +50,11 @@ -}  -- Given a variable to split, and a term application, return a list of--- variable updates-split :: Name -> PTerm -> Idris [[(Name, PTerm)]]+-- variable updates, paired with a flag to say whether the given update+-- typechecks (False = impossible)+-- if the flag is 'False' the splits should be output with the 'impossible'+-- flag, otherwise they should be output as normal+split :: Name -> PTerm -> Idris (Bool, [[(Name, PTerm)]]) split n t'    = do ist <- getIState         -- Make sure all the names in the term are accessible@@ -77,15 +80,26 @@                    logLvl 4 ("Working from " ++ show t)                    logLvl 4 ("Trying " ++ showSep "\n"                                 (map (showTmImpls) newPats_in))-                   newPats <- mapM elabNewPat newPats_in-                   logLvl 3 ("Original:\n" ++ show t)-                   logLvl 3 ("Split:\n" ++-                              (showSep "\n" (map show (mapMaybe id newPats))))-                   logLvl 3 "----"-                   let newPats' = mergeAllPats ist n t (mapMaybe id newPats)-                   logLvl 1 ("Name updates " ++ showSep "\n"-                         (map (\ (p, u) -> show u ++ " " ++ show p) newPats'))-                   return (map snd newPats')+                   newPats_in <- mapM elabNewPat newPats_in+                   case anyValid [] [] newPats_in of+                        Left fails -> do+                           let fails' = mergeAllPats ist n t fails+                           return (False, (map snd fails'))+                        Right newPats -> do+                           logLvl 3 ("Original:\n" ++ show t)+                           logLvl 3 ("Split:\n" +++                                      (showSep "\n" (map show newPats)))+                           logLvl 3 "----"+                           let newPats' = mergeAllPats ist n t newPats+                           logLvl 1 ("Name updates " ++ showSep "\n"+                                 (map (\ (p, u) -> show u ++ " " ++ show p) newPats'))+                           return (True, (map snd newPats'))+   where +     anyValid ok bad [] = if null ok then Left (reverse bad) +                                     else Right (reverse ok)+     anyValid ok bad ((tc, p) : ps)+         | tc = anyValid (p : ok) bad ps+         | otherwise = anyValid ok (p : bad) ps  data MergeState = MS { namemap :: [(Name, Name)],                        invented :: [(Name, Name)],@@ -208,13 +222,13 @@ --   where tidyVar (PRef _ _) = Placeholder --         tidyVar t = t -elabNewPat :: PTerm -> Idris (Maybe PTerm)+elabNewPat :: PTerm -> Idris (Bool, PTerm) elabNewPat t = idrisCatch (do (tm, ty) <- elabVal recinfo ELHS t                               i <- getIState-                              return (Just (delab i tm)))+                              return (True, delab i tm))                           (\e -> do i <- getIState                                     logLvl 5 $ "Not a valid split:\n" ++ pshow i e-                                    return Nothing)+                                    return (False, t))  findPats :: IState -> Type -> [PTerm] findPats ist t | (P _ n _, _) <- unApply t@@ -248,26 +262,27 @@ splitOnLine :: Int         -- ^ line number             -> Name        -- ^ variable             -> FilePath    -- ^ name of file-            -> Idris [[(Name, PTerm)]]+            -> Idris (Bool, [[(Name, PTerm)]]) splitOnLine l n fn = do---     let (before, later) = splitAt (l-1) (lines inp)---     i <- getIState     cl <- getInternalApp fn l     logLvl 3 ("Working with " ++ showTmImpls cl)     tms <- split n cl---     iputStrLn (showSep "\n" (map show tms))-    return tms -- "" -- not yet done...+    return tms  -replaceSplits :: String -> [[(Name, PTerm)]] -> Idris [String]-replaceSplits l ups = updateRHSs 1 (map (rep (expandBraces l)) ups)+replaceSplits :: String -> [[(Name, PTerm)]] -> Bool -> Idris [String]+replaceSplits l ups impossible+    = updateRHSs 1 (map (rep (expandBraces l)) ups)   where     rep str [] = str ++ "\n"     rep str ((n, tm) : ups) = rep (updatePat False (show n) (nshow tm) str) ups      updateRHSs i [] = return []-    updateRHSs i (x : xs) = do (x', i') <- updateRHS (null xs) i x-                               xs' <- updateRHSs i' xs-                               return (x' : xs')+    updateRHSs i (x : xs) +       | impossible = do xs' <- updateRHSs i xs+                         return (setImpossible False x : xs')+       | otherwise = do (x', i') <- updateRHS (null xs) i x+                        xs' <- updateRHSs i' xs+                        return (x' : xs')      updateRHS last i ('?':'=':xs) = do (xs', i') <- updateRHS last i xs                                        return ("?=" ++ xs', i')@@ -283,6 +298,11 @@                                    return (x : xs', i')     updateRHS last i [] = return ("", i) +    setImpossible brace ('}':xs) = '}' : setImpossible False xs+    setImpossible brace ('{':xs) = '{' : setImpossible True xs+    setImpossible False ('=':xs) = "impossible\n"+    setImpossible brace (x : xs) = x : setImpossible brace xs+    setImpossible brace [] = ""      -- TMP HACK: If there are Nats, we don't want to show as numerals since     -- this isn't supported in a pattern, so special case here@@ -337,17 +357,21 @@  getClause :: Int      -- ^ line number that the type is declared on           -> Name     -- ^ Function name+          -> Name     -- ^ User given name           -> FilePath -- ^ Source file name           -> Idris String-getClause l fn fp +getClause l fn un fp      = do i <- getIState          case lookupCtxt fn (idris_classes i) of               [c] -> return (mkClassBodies i (class_methods c))-              _ -> do ty <- getInternalApp fp l+              _ -> do ty_in <- getInternalApp fp l+                      let ty = case ty_in of+                                    PTyped n t -> t+                                    x -> x                       ist <- get                       let ap = mkApp ist ty []-                      return (show fn ++ " " ++ ap ++ "= ?" -                                      ++ show fn ++ "_rhs")+                      return (show un ++ " " ++ ap ++ "= ?" +                                      ++ show un ++ "_rhs")    where mkApp :: IState -> PTerm -> [Name] -> String          mkApp i (PPi (Exp _ _ False) (MN _ _) _ ty sc) used                = let n = getNameFrom i used ty in@@ -380,7 +404,7 @@                             def (show (nsroot n)) ++ " "                                  ++ mkApp i ty []                                  ++ "= ?" -                                 ++ show fn ++ "_rhs_" ++ show m) ns [1..])+                                 ++ show un ++ "_rhs_" ++ show m) ns [1..])           def n@(x:xs) | not (isAlphaNum x) = "(" ++ n ++ ")"          def n = n@@ -390,7 +414,10 @@                -> FilePath -- ^ Source file name                -> Idris String getProofClause l fn fp-                  = do ty <- getInternalApp fp l+                  = do ty_in <- getInternalApp fp l+                       let ty = case ty_in of+                                     PTyped n t -> t+                                     x -> x                        return (mkApp ty ++ " = ?" ++ show fn ++ "_rhs")    where mkApp (PPi _ _ _ _ sc) = mkApp sc          mkApp rt = "(" ++ show rt ++ ") <== " ++ show fn@@ -427,8 +454,8 @@      nm ptm = do mptm <- elabNewPat ptm                 case mptm of-                     Nothing -> return ptm-                     Just ptm' -> return ptm'+                     (False, _) -> return ptm+                     (True, ptm') -> return ptm'                          

@@ -1,5 +1,6 @@-module Idris.Chaser(buildTree, getModuleFiles, ModuleTree(..)) where+module Idris.Chaser(buildTree, getImports, getModuleFiles, ModuleTree(..)) where +import Idris.Core.TT import Idris.Parser import Idris.AbsSyntax import Idris.Imports@@ -79,42 +80,86 @@ getIModTime (IDR i) = getModificationTime i getIModTime (LIDR i) = getModificationTime i +getImports :: [(FilePath, [ImportInfo])] -> [FilePath] -> +              Idris [(FilePath, [ImportInfo])]+getImports acc [] = return acc+getImports acc (f : fs) = do +   i <- getIState+   let file = extractFileName f+   ibcsd <- valIBCSubDir i+   ids <- allImportDirs+   idrisCatch (do+       fp <- findImport ["."] ibcsd file+       let parsef = fname fp+       case lookup parsef acc of+            Just _ -> getImports acc fs+            _ -> do+               exist <- runIO $ doesFileExist parsef+               if exist then do+                   src_in <- runIO $ readSource parsef+                   src <- if lit fp then tclift $ unlit parsef src_in +                                    else return src_in+                   (_, _, modules, _) <- parseImports parsef src+                   clearParserWarnings+                   getImports ((parsef, modules) : acc)+                              (fs ++ map import_path modules)+                     else getImports ((parsef, []) : acc) fs)+        (\_ -> getImports acc fs) -- not in current soure tree, ignore+  where+    lit (LIDR _) = True+    lit _ = False++    fname (IDR fn) = fn+    fname (LIDR fn) = fn+    fname (IBC _ src) = fname src+ buildTree :: [FilePath] -> -- already guaranteed built+             [(FilePath, [ImportInfo])] -> -- import lists (don't reparse)              FilePath -> Idris [ModuleTree]-buildTree built fp = btree [] fp---                    = idrisCatch (btree [] fp)---                         (\e -> do now <- runIO $ getCurrentTime---                                   iputStrLn (show e)---                                   return [MTree (IDR fp) True now []])+buildTree built importlists fp = evalStateT (btree [] fp) []  where-  btree done f =-    do i <- getIState+  addFile :: FilePath -> [ModuleTree] -> +             StateT [(FilePath, [ModuleTree])] Idris [ModuleTree]+  addFile f m = do fs <- get+                   put ((f, m) : fs)+                   return m++  btree :: [FilePath] -> FilePath -> +           StateT [(FilePath, [ModuleTree])] Idris [ModuleTree]+  btree stk f =+    do i <- lift getIState        let file = extractFileName f-       logLvl 1 $ "CHASING " ++ show file-       ibcsd <- valIBCSubDir i-       ids <- allImportDirs-       fp <- findImport ids ibcsd file-       logLvl 1 $ "Found " ++ show fp-       mt <- runIO $ getIModTime fp+       lift $ logLvl 1 $ "CHASING " ++ show file ++ " (" ++ show fp ++ ")"+       ibcsd <- lift $ valIBCSubDir i+       ids <- lift $ allImportDirs+       fp <- lift $ findImport ids ibcsd file+       lift $ logLvl 1 $ "Found " ++ show fp+       mt <- lift $ runIO $ getIModTime fp        if (file `elem` built)           then return [MTree fp False mt []]-          else if file `elem` done-                  then return []-                  else mkChildren fp+               else if file `elem` stk then +                       do lift $ tclift $ tfail+                            (Msg $ "Cycle detected in imports: "+                                     ++ showSep " -> " (reverse (file : stk)))+                 else do donetree <- get+                         case lookup file donetree of+                            Just t -> return t+                            _ -> do ms <- mkChildren file fp+                                    addFile file ms -    where mkChildren (LIDR fn) = do ms <- children True fn (f:done)-                                    mt <- runIO $ getModificationTime fn-                                    return [MTree (LIDR fn) True mt ms]-          mkChildren (IDR fn) = do ms <- children False fn (f:done)-                                   mt <- runIO $ getModificationTime fn-                                   return [MTree (IDR fn) True mt ms]-          mkChildren (IBC fn src)-              = do srcexist <- runIO $ doesFileExist (getSrcFile src)+    where mkChildren file (LIDR fn) = do ms <- children True fn (file : stk)+                                         mt <- lift $ runIO $ getModificationTime fn+                                         return [MTree (LIDR fn) True mt ms]+          mkChildren file (IDR fn) = do ms <- children False fn (file : stk)+                                        mt <- lift $ runIO $ getModificationTime fn+                                        return [MTree (IDR fn) True mt ms]+          mkChildren file (IBC fn src)+              = do srcexist <- lift $ runIO $ doesFileExist (getSrcFile src)                    ms <- if srcexist then-                               do [MTree _ _ _ ms'] <- mkChildren src+                               do [MTree _ _ _ ms'] <- mkChildren file src                                   return ms'                              else return []-                   mt <- idrisCatch (runIO $ getModificationTime fn)+                   mt <- lift $ idrisCatch (runIO $ getModificationTime fn)                                     (\c -> runIO $ getIModTime src)                    -- FIXME: It's also not up to date if anything it imports has                    -- been modified since its own ibc has.@@ -122,7 +167,7 @@                    -- Issue #1592 on the issue tracker.                    --                    -- https://github.com/idris-lang/Idris-dev/issues/1592-                   ibcOutdated <- fn `younger` (getSrcFile src)+                   ibcOutdated <- lift $ fn `younger` (getSrcFile src)                    -- FIXME (EB): The below 'hasValidIBCVersion' that's                    -- commented out appears to be breaking reloading in vim                    -- mode. Until we know why, I've commented it out.@@ -140,16 +185,14 @@                                    return (srct > ibct)                                  else return False -  children :: Bool -> FilePath -> [FilePath] -> Idris [ModuleTree]-  children lit f done = -- idrisCatch-     do exist <- runIO $ doesFileExist f+  children :: Bool -> FilePath -> [FilePath] ->+              StateT [(FilePath, [ModuleTree])] Idris [ModuleTree]+  children lit f stk = -- idrisCatch+     do exist <- lift $ runIO $ doesFileExist f         if exist then do-            file_in <- runIO $ readSource f-            file <- if lit then tclift $ unlit f file_in else return file_in-            (_, _, modules, _) <- parseImports f file-            -- The chaser should never report warnings from sub-modules-            clearParserWarnings-            ms <- mapM (btree done . import_path) modules+            lift $ logLvl 1 $ "Reading source " ++ show f+            let modules = maybe [] id (lookup f importlists)+            ms <- mapM (btree stk . import_path) modules             return (concat ms)            else return [] -- IBC with no source available --     (\c -> return []) -- error, can't chase modules here

@@ -148,6 +148,8 @@    <|> (UseConsoleWidth <$> option (str >>= parseConsoleWidth) (long "consolewidth" <> metavar "WIDTH" <> help "Select console width: auto, infinite, nat"))   <|> flag' DumpHighlights (long "highlight" <> help "Emit source code highlighting")+  <|> flag' NoElimDeprecationWarnings (long "no-elim-deprecation-warnings" <> help "Disable deprecation warnings for %elim")+  <|> flag' NoOldTacticDeprecationWarnings (long "no-tactic-deprecation-warnings" <> help "Disable deprecation warnings for the old tactic sublanguage")    where     getExt s = case maybeRead s of

@@ -12,7 +12,7 @@ import Idris.ParseHelpers(opChars) import qualified Idris.ParseExpr (constants, tactics) import Idris.ParseExpr (TacticArg (..))-import Idris.REPLParser (allHelp)+import Idris.REPLParser (allHelp, setOptions) import Control.Monad.State.Strict  import Data.List@@ -82,13 +82,7 @@  completeOption :: CompletionFunc Idris completeOption = completeWord Nothing " \t" completeOpt-    where completeOpt = return . completeWith [ "errorcontext"-                                              , "showimplicits"-                                              , "originalerrors"-                                              , "autosolve"-                                              , "nobanner"-                                              , "desugarnats"-                                              ]+    where completeOpt = return . completeWith (map fst setOptions)  completeConsoleWidth :: CompletionFunc Idris completeConsoleWidth = completeWord Nothing " \t" completeW

@@ -145,10 +145,11 @@   put (At fc e) = do putWord8 27                      put fc                      put e-  put (Elaborating str n e) = do putWord8 28-                                 put str-                                 put n-                                 put e+  put (Elaborating str n ty e) = do putWord8 28+                                    put str+                                    put n+                                    put ty+                                    put e   put (ElaboratingArg n1 n2 ns e) = do putWord8 29                                        put n1                                        put n2@@ -188,7 +189,10 @@                             put ns   put (RunningElabScript e) = do putWord8 42                                  put e-+  put (ElabScriptStaging n) = do putWord8 43+                                 put n+  put (FancyMsg xs) = do putWord8 44+                         put xs   get = do i <- getWord8            case i of              0 -> fmap Msg get@@ -230,8 +234,8 @@              26 -> fmap NoRewriting get              27 -> do x <- get ; y <- get                       return $ At x y-             28 -> do x <- get ; y <- get ; z <- get-                      return $ Elaborating x y z+             28 -> do w <- get; x <- get ; y <- get ; z <- get+                      return $ Elaborating w x y z              29 -> do w <- get ; x <- get ; y <- get ; z <- get                       return $ ElaboratingArg w x y z              30 -> fmap ProviderError get@@ -259,6 +263,8 @@                       return $ UnknownImplicit x y              41 -> fmap NoValidAlts get              42 -> fmap RunningElabScript get+             43 -> fmap ElabScriptStaging get+             44 -> fmap FancyMsg get              _ -> error "Corrupted binary data for Err'" ----- Generated by 'derive' @@ -284,6 +290,9 @@                          return (FileFC x1)                  _ -> error "Corrupted binary data for FC" +instance Binary FC' where+    put (FC' fc) = put fc+    get = fmap FC' get  instance Binary Name where         put x@@ -296,10 +305,9 @@                 MN x1 x2 -> do putWord8 2                                put x1                                put x2-                NErased -> putWord8 3-                SN x1 -> do putWord8 4+                SN x1 -> do putWord8 3                             put x1-                SymRef x1 -> do putWord8 5+                SymRef x1 -> do putWord8 4                                 put x1         get           = do i <- getWord8@@ -312,10 +320,9 @@                    2 -> do x1 <- get                            x2 <- get                            return (MN x1 x2)-                   3 -> return NErased-                   4 -> do x1 <- get+                   3 -> do x1 <- get                            return (SN x1)-                   5 -> do x1 <- get+                   4 -> do x1 <- get                            return (SymRef x1)                    _ -> error "Corrupted binary data for Name" @@ -334,7 +341,7 @@                                     put x2                 MethodN x1 -> do putWord8 3                                  put x1-                CaseN x1 -> do putWord8 4; put x1+                CaseN x1 x2 -> do putWord8 4; put x1; put x2                 ElimN x1 -> do putWord8 5; put x1                 InstanceCtorN x1 -> do putWord8 6; put x1                 WithN x1 x2 -> do putWord8 7@@ -359,7 +366,8 @@                    3 -> do x1 <- get                            return (MethodN x1)                    4 -> do x1 <- get-                           return (CaseN x1)+                           x2 <- get+                           return (CaseN x1 x2)                    5 -> do x1 <- get                            return (ElimN x1)                    6 -> do x1 <- get@@ -452,9 +460,7 @@                 RType -> putWord8 3                 RConstant x1 -> do putWord8 4                                    put x1-                RForce x1 -> do putWord8 5-                                put x1-                RUType x1 -> do putWord8 6+                RUType x1 -> do putWord8 5                                 put x1         get           = do i <- getWord8@@ -472,18 +478,17 @@                    4 -> do x1 <- get                            return (RConstant x1)                    5 -> do x1 <- get-                           return (RForce x1)-                   6 -> do x1 <- get                            return (RUType x1)                    _ -> error "Corrupted binary data for Raw"  instance Binary ImplicitInfo where         put x           = case x of-                Impl x1 -> put x1+                Impl x1 x2 -> do put x1; put x2         get           = do x1 <- get-               return (Impl x1)+               x2 <- get+               return (Impl x1 x2)  instance (Binary b) => Binary (Binder b) where         put x

@@ -13,7 +13,6 @@         rnf (UN x1) = rnf x1 `seq` ()         rnf (NS x1 x2) = rnf x1 `seq` rnf x2 `seq` ()         rnf (MN x1 x2) = rnf x1 `seq` rnf x2 `seq` ()-        rnf NErased = ()         rnf (SN x1) = rnf x1 `seq` ()         rnf (SymRef x1) = rnf x1 `seq` () @@ -65,7 +64,7 @@         rnf (InstanceN x1 x2) = rnf x1 `seq` rnf x2 `seq` ()         rnf (ParentN x1 x2) = rnf x1 `seq` rnf x2 `seq` ()         rnf (MethodN x1) = rnf x1 `seq` ()-        rnf (CaseN x1) = rnf x1 `seq` ()+        rnf (CaseN x1 x2) = rnf x1 `seq` rnf x2 `seq` ()         rnf (ElimN x1) = rnf x1 `seq` ()         rnf (InstanceCtorN x1) = rnf x1 `seq` ()         rnf (MetaN x1 x2) = rnf x1 `seq` rnf x2 `seq` ()@@ -81,7 +80,6 @@         rnf (RApp x1 x2) = rnf x1 `seq` rnf x2 `seq` ()         rnf RType = ()         rnf (RUType x1) = rnf x1 `seq` ()-        rnf (RForce x1) = rnf x1 `seq` ()         rnf (RConstant x1) = x1 `seq` ()  instance NFData FC where@@ -89,6 +87,9 @@         rnf NoFC = ()         rnf (FileFC f) = rnf f `seq` () +instance NFData FC' where+        rnf (FC' fc) = rnf fc `seq` ()+ instance NFData Provenance where         rnf ExpectedType = ()         rnf InferredVal = ()@@ -148,13 +149,15 @@         rnf (ProofSearchFail x1) = rnf x1 `seq` ()         rnf (NoRewriting x1) = rnf x1 `seq` ()         rnf (At x1 x2) = rnf x1 `seq` rnf x2 `seq` ()-        rnf (Elaborating x1 x2 x3)-          = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()+        rnf (Elaborating x1 x2 x3 x4)+          = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()         rnf (ProviderError x1) = rnf x1 `seq` ()         rnf (LoadingFailed x1 x2) = rnf x1 `seq` rnf x2 `seq` ()         rnf (ElabScriptDebug x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()         rnf (ElabScriptStuck x1) = rnf x1 `seq` ()         rnf (RunningElabScript x1) = rnf x1 `seq` ()+        rnf (ElabScriptStaging x1) = rnf x1 `seq` ()+        rnf (FancyMsg x1) = rnf x1 `seq` ()  instance NFData ErrorReportPart where   rnf (TextPart x1) = rnf x1 `seq` ()@@ -164,7 +167,7 @@   rnf (SubReport x1) = rnf x1 `seq` ()  instance NFData ImplicitInfo where-        rnf (Impl x1) = rnf x1 `seq` ()+        rnf (Impl x1 x2) = rnf x1 `seq` rnf x2 `seq` ()  instance (NFData b) => NFData (Binder b) where         rnf (Lam x1) = rnf x1 `seq` ()

@@ -119,8 +119,8 @@       rewriteErr (ProofSearchFail e) = ProofSearchFail (rewriteErr e)       rewriteErr e = f e -errAt :: String -> Name -> Elab' aux a -> Elab' aux a-errAt thing n = transformErr (Elaborating thing n)+errAt :: String -> Name -> Maybe Type -> Elab' aux a -> Elab' aux a+errAt thing n ty = transformErr (Elaborating thing n ty)   erun :: FC -> Elab' aux a -> Elab' aux a@@ -711,8 +711,8 @@             = do g <- goal                  case g of                     Bind _ (Pi _ _ _) _ -> return ()-                    _ -> do a <- getNameFrom (sMN 0 "pargTy")-                            b <- getNameFrom (sMN 0 "pretTy")+                    _ -> do a <- getNameFrom (sMN 0 "__pargTy")+                            b <- getNameFrom (sMN 0 "__pretTy")                             f <- getNameFrom (sMN 0 "pf")                             claim a RType                             claim b RType@@ -725,8 +725,8 @@  simple_app :: Bool -> Elab' aux () -> Elab' aux () -> String -> Elab' aux () simple_app infer fun arg str = -    do a <- getNameFrom (sMN 0 "argTy")-       b <- getNameFrom (sMN 0 "retTy")+    do a <- getNameFrom (sMN 0 "__argTy")+       b <- getNameFrom (sMN 0 "__retTy")        f <- getNameFrom (sMN 0 "f")        s <- getNameFrom (sMN 0 "s")        claim a RType

@@ -2,7 +2,8 @@              PatternGuards #-} {-# OPTIONS_GHC -fwarn-incomplete-patterns #-} -module Idris.Core.Evaluate(normalise, normaliseTrace, normaliseC, normaliseAll, toValue, quoteTerm,+module Idris.Core.Evaluate(normalise, normaliseTrace, normaliseC, +                normaliseAll, normaliseBlocking, toValue, quoteTerm,                 rt_simplify, simplify, specialise, hnf, convEq, convEq',                 Def(..), CaseInfo(..), CaseDefs(..),                 Accessibility(..), Totality(..), PReason(..), MetaInformation(..),@@ -79,9 +80,17 @@    = evalState (do val <- eval False ctxt [] (map finalEntry env) t []                    quote 0 val) initEval +-- | Normalise everything, whether abstract, private or public normaliseAll :: Context -> Env -> TT Name -> TT Name normaliseAll ctxt env t    = evalState (do val <- eval False ctxt [] (map finalEntry env) t [AtREPL]+                   quote 0 val) initEval++-- | As normaliseAll, but with an explicit list of names *not* to reduce+normaliseBlocking :: Context -> Env -> [Name] -> TT Name -> TT Name+normaliseBlocking ctxt env blocked t+   = evalState (do val <- eval False ctxt (map (\n -> (n, 0)) blocked)+                                          (map finalEntry env) t [AtREPL]                    quote 0 val) initEval  normalise :: Context -> Env -> TT Name -> TT Name

@@ -349,6 +349,17 @@                       "The argument to fileEOF should be a file handle, but it was " ++                       show handle ++                       ". Are all cases covered?"+    | Just (FFun "fileError" [(_,handle)] _) <- foreignFromTT arity ty fn xs+           = case handle of+             -- errors handled differently in Haskell than in C, so if+             -- there's been an error we'll have had an exception already.+             -- Therefore, assume we're okay.+               EHandle h -> do let res = ioWrap (EConstant (I 0))+                               execApp env ctxt res (drop arity xs)+               _ -> execFail . Msg $+                      "The argument to fileError should be a file handle, but it was " +++                      show handle +++                      ". Are all cases covered?"     | Just (FFun "fileClose" [(_,handle)] _) <- foreignFromTT arity ty fn xs            = case handle of                EHandle h -> do execIO $ hClose h

@@ -408,6 +408,8 @@                             ps { holes = (hs \\ [x]) ++ [x],                                  instances = x:is })          return (Bind x (Hole t) sc)+instanceArg n ctxt env _+    = fail "The current focus is not a hole."  autoArg :: Name -> RunTactic autoArg n ctxt env (Bind x (Hole t) sc)@@ -418,6 +420,8 @@                                     autos = (x, (while_elaborating ps, refsIn t)) : autos ps }                              Just _ -> ps)          return (Bind x (Hole t) sc)+autoArg n ctxt env _+    = fail "The current focus not a hole."  setinj :: Name -> RunTactic setinj n ctxt env (Bind x b sc)@@ -439,6 +443,7 @@     mkTy ((n,b) : bs) t = Bind n (Pi Nothing (binderTy b) (TType (UVar 0))) (mkTy bs t)      getP (n, b) = P Bound n (binderTy b)+defer dropped n ctxt env _ = fail "Can't defer a non-hole focus."  -- as defer, but build the type and application explicitly deferType :: Name -> Raw -> [Name] -> RunTactic@@ -454,6 +459,7 @@     getP n = case lookup n env of                   Just b -> P Bound n (binderTy b)                   Nothing -> error ("deferType can't find " ++ show n)+deferType _ _ _ _ _ _ = fail "Can't defer a non-hole focus."  regret :: RunTactic regret ctxt env (Bind x (Hole t) sc) | noOccurrence x sc =@@ -462,12 +468,14 @@        return sc regret ctxt env (Bind x (Hole t) _)     = fail $ show x ++ " : " ++ show t ++ " is not solved..."+regret _ _ _ = fail "The current focus is not a hole."  unifyGoal :: Raw -> RunTactic unifyGoal tm ctxt env h@(Bind x b sc) =     do (tmv, _) <- lift $ check ctxt env tm        ns' <- unify' ctxt env (binderTy b, Nothing) (tmv, Nothing)        return h+unifyGoal _ _ _ _ = fail "The focus is not a binder."  exact :: Raw -> RunTactic exact guess ctxt env (Bind x (Hole ty) sc) =@@ -621,19 +629,19 @@  intro :: Maybe Name -> RunTactic intro mn ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =-    do let n = case mn of-                  Just name -> name-                  Nothing -> x-       let t' = case t of+    do let t' = case t of                     x@(Bind y (Pi _ s _) _) -> x                     _ -> hnf ctxt env t        case t' of            Bind y (Pi _ s _) t ->+               let n = case mn of+                      Just name -> name+                      Nothing -> y                -- It's important that this be subst and not updsubst,                -- because we want to substitute even in portions of                -- terms that we know do not contain holes.-               let t' = subst y (P Bound n s) t in-                   return $ Bind n (Lam s) (Bind x (Hole t') (P Bound x t'))+                   t' = subst y (P Bound n s) t+               in return $ Bind n (Lam s) (Bind x (Hole t') (P Bound x t'))            _ -> lift $ tfail $ CantIntroduce t' intro n ctxt env _ = fail "Can't introduce here." @@ -714,7 +722,7 @@   let tmt' = normalise ctxt env tmt   let (tacn, tacstr, tactt) = if induction               then (ElimN, "eliminator", "Induction")-              else (CaseN, "case analysis", "Case analysis")+              else (CaseN (FC' emptyFC), "case analysis", "Case analysis")   case unApply tmt' of     (P _ tnm _, tyargs) -> do         case lookupTy (SN (tacn tnm)) ctxt of@@ -870,7 +878,7 @@  updateError [] err = err updateError ns (At f e) = At f (updateError ns e)-updateError ns (Elaborating s n e) = Elaborating s n (updateError ns e)+updateError ns (Elaborating s n ty e) = Elaborating s n ty (updateError ns e) updateError ns (ElaboratingArg f a env e)  = ElaboratingArg f a env (updateError ns e) updateError ns (CantUnify b (l,lp) (r,rp) e xs sc)