Merge branch 'master' into prelude-inline-doc

CHANGELOG.md

@@ -6,6 +6,20 @@ Compiler updates:
 * Data types with a single constructor, with a single unerased arguments,
   are translated to just that argument, to save repeated packing and unpacking.
   (c.f. `newtype` in Haskell)
+* 0-multiplicity constructor arguments are now properly erased, not just
+  given a placeholder null value.
+
+Other improvements:
+
+* Various performance improvements in the typechecker:
+  + Noting which metavariables are blocking unification constraints, so that
+    they only get retried if those metavariables make progress.
+  + Evaluating `fromInteger` at compile time.
+  + In the run-time, reuse the old heap after garbage collection if it
+    hasn't been resized, to avoid unnecessary system calls.
+
+* Extend Idris2's literate mode to support reading Markdown and OrgMode files.
+  For more details see: https://idris2.readthedocs.io/en/latest/reference/literate.html
 
 Changes since Idris 1
 ---------------------

dist/rts/idris_gc.c

@@ -103,11 +103,10 @@ void idris_gc(VM* vm) {
     HEAP_CHECK(vm)
     STATS_ENTER_GC(vm->stats, vm->heap.size)
 
-    if (vm->heap.old != NULL)
-        free(vm->heap.old);
-
-    /* Allocate swap heap. */
-    alloc_heap(&vm->heap, vm->heap.size, vm->heap.growth, vm->heap.heap);
+    /* Allocate swap heap, possibly reusing the old heap if it's
+       big enough */
+    alloc_heap(&vm->heap, vm->heap.size, vm->heap.growth,
+               vm->heap.heap, vm->heap.end);
 
     VAL* root;
 

dist/rts/idris_heap.c

@@ -107,9 +107,20 @@ void c_heap_destroy(CHeap * heap)
 }
 
 /* Used for initializing the FP heap. */
-void alloc_heap(Heap * h, size_t heap_size, size_t growth, char * old)
+void alloc_heap(Heap * h, size_t heap_size, size_t growth,
+                char* old, char* old_end)
 {
-    char * mem = malloc(heap_size);
+    char * mem;
+    // If the old heap is big enough, use that
+    // Otherwise, free it and allocate a new chunk
+    if (h->old != NULL) {
+        if (h->old_end - h->old >= heap_size) {
+            mem = h->old;
+        } else {
+            mem = realloc(h->old, heap_size);
+        }
+    }
+    else mem = malloc(heap_size);
 
     if (mem == NULL) {
         fprintf(stderr,
@@ -127,6 +138,7 @@ void alloc_heap(Heap * h, size_t heap_size, size_t growth, char * old)
     h->growth = growth;
 
     h->old = old;
+    h->old_end = old_end;
 }
 
 void free_heap(Heap * h) {

dist/rts/idris_heap.h

@@ -93,10 +93,12 @@ typedef struct {
     size_t growth; // Quantity of heap growth in bytes.
 
     char* old;
+    char* old_end;
 } Heap;
 
 
-void alloc_heap(Heap * heap, size_t heap_size, size_t growth, char * old);
+void alloc_heap(Heap * heap, size_t heap_size, size_t growth,
+                char * old, char * old_end);
 void free_heap(Heap * heap);
 char* aligned_heap_pointer(char * heap);
 

dist/rts/idris_rts.c

@@ -42,8 +42,9 @@ VM* init_vm(int stack_size, size_t heap_size,
     vm->valstack_top = valstack;
     vm->valstack_base = valstack;
     vm->stack_max = valstack + stack_size;
+    vm->heap.old = NULL;
 
-    alloc_heap(&(vm->heap), heap_size, heap_size, NULL);
+    alloc_heap(&(vm->heap), heap_size, heap_size, NULL, NULL);
 
     c_heap_init(&vm->c_heap);
 

docs/reference/literate.rst

@@ -0,0 +1,55 @@
+.. _ref-sect-literate:
+
+**********************
+Literate Programming
+**********************
+
+Idris2 supports several types of literate mode styles.
+
+The unlit'n has been designed based such that we assume that we are parsing markdown-like languages
+The unlit'n is performed by a Lexer that uses a provided literate style to recognise code blocks and code lines.
+Anything else is ignored.
+
+A literate style consists of:
+
++ a list of String encoded code block deliminators;
++ a list of line indicators; and
++ a list of valid file extensions.
+
+Lexing is simple and greedy in that when consuming anything that is a code blocks we treat everything as code until we reach the closing deliminator.
+This means that use of verbatim modes in a literate file will also be treated as active code.
+
+In future we should add support for literate ``LaTeX`` files, and potentially other common document formats.
+But more importantly, a more intelligent processing of literate documents using a pandoc like library in Idris such as: `Edda <https://github.com/jfdm/edda>` would also be welcome.
+
+Bird Style Literate Files
+=========================
+
+Bird notation is a classic literate mode found in Haskell, (and Orwell) in which code lines begin with ``>``.
+Other lines are treated as documentation.
+
+We treat files with an extension of ``.lidr`` as bird style literate files.
+
+Embedding in Markdown-like documents
+====================================
+
+While Bird Style literate mode is useful, it does not lend itself well
+to more modern markdown-like notations such as Org-Mode and CommonMark.
+
+Idris2 also provides support for recognising both 'visible' and 'invisible' code blocks and lines in both CommonMark and OrgMode documents.
+
+OrgMode
+*******
+
++ Org mode source blocks for idris are recognised as visible code blocks,
++ Comment blocks that begin with ``#+COMMENT: idris`` are treated as invisible code blocks.
++ Invisible code lines are denoted with ``#+IDRIS:``.
+
+We treat files with an extension of ``.org`` as org-mode style literate files.
+
+CommonMark
+************
+
+Only code blocks denoted by standard code blocks labelled as idris are recognised.
+
+We treat files with an extension of ``.md`` and ``.markdown`` as org-mode style literate files.

docs/source/reference/index.rst

@@ -18,3 +18,4 @@ This is a placeholder, to get set up with readthedocs.
 
    packages
    envvars
+   literate

idris2.ipkg

@@ -79,6 +79,7 @@ modules =
 
     Text.Lexer,
     Text.Lexer.Core,
+    Text.Literate,
     Text.Parser,
     Text.Parser.Core,
     Text.Quantity,

libs/base/Data/Fin.idr

@@ -103,7 +103,7 @@ last : {n : _} -> Fin (S n)
 last {n=Z} = FZ
 last {n=S _} = FS last
 
-export total
+public export total
 FSinjective : {f : Fin n} -> {f' : Fin n} -> (FS f = FS f') -> f = f'
 FSinjective Refl = Refl
 

libs/prelude/Prelude.idr

@@ -1416,6 +1416,7 @@ Applicative IO where
           io_bind a (\a' =>
             io_pure (f' a')))
 
+%inline
 public export
 Monad IO where
   b >>= k = io_bind b k

src/Compiler/CompileExpr.idr

@@ -296,16 +296,19 @@ mutual
                     !(constCases tags n ns)
   constCases tags n (_ :: ns) = constCases tags n ns
 
-  getDef : {auto c : Ref Ctxt Defs} ->
-           FC -> CExp vars ->
-           NameTags -> Name -> List (CaseAlt vars) ->
-           Core (Bool, Maybe (CExp vars))
-  getDef fc scr tags n [] = pure (False, Nothing)
-  getDef fc scr tags n (DefaultCase sc :: ns)
-      = pure $ (False, Just !(toCExpTree tags n sc))
-  getDef fc scr tags n (ConstCase WorldVal sc :: ns)
-      = pure $ (False, Just !(toCExpTree tags n sc))
-  getDef {vars} fc scr tags n (ConCase x tag args sc :: ns)
+  -- If there's a case which matches on a 'newtype', return the RHS
+  -- without matching.
+  -- Take some care if the newtype involves a WorldVal - in that case we
+  -- still need to let bind the scrutinee to ensure it's evaluated exactly
+  -- once.
+  getNewType : {auto c : Ref Ctxt Defs} ->
+               FC -> CExp vars ->
+               NameTags -> Name -> List (CaseAlt vars) ->
+               Core (Maybe (CExp vars))
+  getNewType fc scr tags n [] = pure Nothing
+  getNewType fc scr tags n (DefaultCase sc :: ns)
+      = pure $ Nothing
+  getNewType {vars} fc scr tags n (ConCase x tag args sc :: ns)
       = do defs <- get Ctxt
            case !(lookupDefExact x (gamma defs)) of
                 -- If the flag is False, we still take the
@@ -315,18 +318,41 @@ mutual
                 -- outside world, so we need to evaluate to keep the
                 -- side effect.
                 Just (DCon _ arity (Just (noworld, pos))) =>
-                     let env : SubstCEnv args vars = mkSubst 0 pos args in
-                         pure $ (not noworld,
-                                 Just (substs env !(toCExpTree tags n sc)))
-                _ => getDef fc scr tags n ns
+                     if noworld -- just substitute the scrutinee into
+                                -- the RHS
+                        then let env : SubstCEnv args vars
+                                     = mkSubst 0 scr pos args in
+                                 pure $ Just (substs env !(toCExpTree tags n sc))
+                        else -- let bind the scrutinee, and substitute the
+                             -- name into the RHS
+                             let env : SubstCEnv args (MN "eff" 0 :: vars)
+                                     = mkSubst 0 (CLocal fc First) pos args in
+                             do sc' <- toCExpTree tags n sc
+                                let scope = thin {outer=args}
+                                                 {inner=vars}
+                                                 (MN "eff" 0) sc'
+                                pure $ Just (CLet fc (MN "eff" 0) False scr
+                                                  (substs env scope))
+                _ => pure Nothing -- there's a normal match to do
     where
-      mkSubst : Nat -> Nat -> (args : List Name) -> SubstCEnv args vars
-      mkSubst _ _ [] = Nil
-      mkSubst i pos (a :: as)
+      mkSubst : Nat -> CExp vs ->
+                Nat -> (args : List Name) -> SubstCEnv args vs
+      mkSubst _ _ _ [] = Nil
+      mkSubst i scr pos (a :: as)
           = if i == pos
-               then scr :: mkSubst (1 + i) pos as
-               else CErased fc :: mkSubst (1 + i) pos as
-  getDef fc scr tags n (_ :: ns) = getDef fc scr tags n ns
+               then scr :: mkSubst (1 + i) scr pos as
+               else CErased fc :: mkSubst (1 + i) scr pos as
+  getNewType fc scr tags n (_ :: ns) = getNewType fc scr tags n ns
+
+  getDef : {auto c : Ref Ctxt Defs} ->
+           NameTags -> Name -> List (CaseAlt vars) ->
+           Core (Maybe (CExp vars))
+  getDef tags n [] = pure Nothing
+  getDef tags n (DefaultCase sc :: ns)
+      = pure $ Just !(toCExpTree tags n sc)
+  getDef tags n (ConstCase WorldVal sc :: ns)
+      = pure $ Just !(toCExpTree tags n sc)
+  getDef tags n (_ :: ns) = getDef tags n ns
 
   toCExpTree : {auto c : Ref Ctxt Defs} ->
                NameTags -> Name -> CaseTree vars ->
@@ -337,22 +363,21 @@ mutual
               CLet fc arg True (CForce fc (CLocal (getLoc scTy) x)) $
               CLet fc ty True (CErased fc)
                    !(toCExpTree tags n sc)
-  toCExpTree tags n alts = toCExpTree' tags n alts
+  toCExpTree tags n alts
+      = toCExpTree' tags n alts
 
   toCExpTree' : {auto c : Ref Ctxt Defs} ->
                 NameTags -> Name -> CaseTree vars ->
                 Core (CExp vars)
-  toCExpTree' tags n (Case fc x scTy alts@(ConCase _ _ _ _ :: _))
+  toCExpTree' tags n (Case _ x scTy alts@(ConCase _ _ _ _ :: _))
       = let fc = getLoc scTy in
-            do defs <- get Ctxt
+            do Nothing <- getNewType fc (CLocal fc x) tags n alts
+                   | Just def => pure def
+               defs <- get Ctxt
                cases <- conCases tags n alts
-               (keepSc, def) <- getDef fc (CLocal fc x) tags n alts
+               def <- getDef tags n alts
                if isNil cases
-                  then (if keepSc
-                           then pure $ CLet fc (MN "eff" 0) False
-                                            (CLocal fc x)
-                                            (weaken (fromMaybe (CErased fc) def))
-                           else pure (fromMaybe (CErased fc) def))
+                  then pure (fromMaybe (CErased fc) def)
                   else pure $ natHackTree $
                             CConCase fc (CLocal fc x) cases def
   toCExpTree' tags n (Case _ x scTy alts@(DelayCase _ _ _ :: _))
@@ -360,13 +385,9 @@ mutual
   toCExpTree' tags n (Case fc x scTy alts@(ConstCase _ _ :: _))
       = let fc = getLoc scTy in
             do cases <- constCases tags n alts
-               (keepSc, def) <- getDef fc (CLocal fc x) tags n alts
+               def <- getDef tags n alts
                if isNil cases
-                  then (if keepSc
-                           then pure $ CLet fc (MN "eff" 0) False
-                                            (CLocal fc x)
-                                            (weaken (fromMaybe (CErased fc) def))
-                           else pure (fromMaybe (CErased fc) def))
+                  then pure (fromMaybe (CErased fc) def)
                   else pure $ CConstCase fc (CLocal fc x) cases def
   toCExpTree' tags n (Case _ x scTy alts@(DefaultCase sc :: _))
       = toCExpTree tags n sc

src/Compiler/Inline.idr

@@ -58,29 +58,44 @@ genName n
 refToLocal : Name -> (x : Name) -> CExp vars -> CExp (x :: vars)
 refToLocal x new tm = refsToLocals (Add new x None) tm
 
+largest : Ord a => a -> List a -> a
+largest x [] = x
+largest x (y :: ys)
+    = if y > x
+         then largest y ys
+         else largest x ys
+
 mutual
-  used : Name -> CExp free -> Bool
-  used n (CRef _ n') = n == n'
-  used n (CLam _ _ sc) = used n sc
-  used n (CLet _ _ _ val sc) = used n val || used n sc
-  used n (CApp _ x args) = used n x || or (map Delay (map (used n) args))
-  used n (CCon _ _ _ args) = or (map Delay (map (used n) args))
-  used n (COp _ _ args) = or (map Delay (map (used n) args))
-  used n (CExtPrim _ _ args) = or (map Delay (map (used n) args))
+  used : {idx : Nat} -> .(IsVar n idx free) -> CExp free -> Int
+  used {idx} n (CLocal _ {idx=pidx} prf) = if idx == pidx then 1 else 0
+  used n (CLam _ _ sc) = used (Later n) sc
+  used n (CLet _ _ False val sc)
+      = let usedl = used n val + used (Later n) sc in
+            if usedl > 0
+               then 1000 -- Don't do any inlining of the name, because if it's
+                         -- used under a non-inlinable let things might go wrong
+               else usedl
+  used n (CLet _ _ True val sc) = used n val + used (Later n) sc
+  used n (CApp _ x args) = foldr (+) (used n x) (map (used n) args)
+  used n (CCon _ _ _ args) = foldr (+) 0 (map (used n) args)
+  used n (COp _ _ args) = foldr (+) 0 (map (used n) args)
+  used n (CExtPrim _ _ args) = foldr (+) 0 (map (used n) args)
   used n (CForce _ x) = used n x
   used n (CDelay _ x) = used n x
   used n (CConCase fc sc alts def)
-     = used n sc || or (map Delay (map (usedCon n) alts))
-                 || maybe False (used n) def
+     = used n sc +
+          largest (maybe 0 (used n) def) (map (usedCon n) alts)
   used n (CConstCase fc sc alts def)
-     = used n sc || or (map Delay (map (usedConst n) alts))
-                 || maybe False (used n) def
-  used _ tm = False
+     = used n sc +
+          largest (maybe 0 (used n) def) (map (usedConst n) alts)
+  used _ tm = 0
 
-  usedCon : Name -> CConAlt free -> Bool
-  usedCon n (MkConAlt _ _ _ sc) = used n sc
+  usedCon : {idx : Nat} -> .(IsVar n idx free) -> CConAlt free -> Int
+  usedCon n (MkConAlt _ _ args sc)
+      = let MkVar n' = weakenNs args (MkVar n) in
+            used n' sc
 
-  usedConst : Name -> CConstAlt free -> Bool
+  usedConst : {idx : Nat} -> .(IsVar n idx free) -> CConstAlt free -> Int
   usedConst n (MkConstAlt _ sc) = used n sc
 
 mutual
@@ -133,13 +148,22 @@ mutual
            sc' <- eval rec (CRef fc xn :: env) [] sc
            pure $ CLam fc x (refToLocal xn x sc')
   eval rec env (e :: stk) (CLam fc x sc) = eval rec (e :: env) stk sc
-  eval {vars} {free} rec env stk (CLet fc x inl val sc)
+  eval {vars} {free} rec env stk (CLet fc x False val sc)
       = do xn <- genName "letv"
            sc' <- eval rec (CRef fc xn :: env) [] sc
-           if inl && used xn sc'
+           val' <- eval rec env [] val
+           pure (unload stk $ CLet fc x False val' (refToLocal xn x sc'))
+  eval {vars} {free} rec env stk (CLet fc x True val sc)
+      = do let u = used First sc
+           if u < 1 -- TODO: Can make this <= as long as we know *all* inlinings
+                    -- are guaranteed not to duplicate work. (We don't know
+                    -- that yet).
               then do val' <- eval rec env [] val
-                      pure (unload stk $ CLet fc x inl val' (refToLocal xn x sc'))
-              else pure sc'
+                      eval rec (val' :: env) stk sc
+              else do xn <- genName "letv"
+                      sc' <- eval rec (CRef fc xn :: env) stk sc
+                      val' <- eval rec env [] val
+                      pure (CLet fc x True val' (refToLocal xn x sc'))
   eval rec env stk (CApp fc f args)
       = eval rec env (!(traverse (eval rec env []) args) ++ stk) f
   eval rec env stk (CCon fc n t args)

src/Compiler/Scheme/Common.idr

@@ -310,6 +310,12 @@ parameters (schExtPrim : Int -> ExtPrim -> List NamedCExp -> Core String,
         = schExtPrim i (toPrim p) args
     schExp i (NmForce fc t) = pure $ "(" ++ !(schExp i t) ++ ")"
     schExp i (NmDelay fc t) = pure $ "(lambda () " ++ !(schExp i t) ++ ")"
+    schExp i (NmConCase fc sc [] def)
+        = do tcode <- schExp (i+1) sc
+             defc <- maybe (pure "'erased") (schExp i) def
+             let n = "sc" ++ show i
+             pure $ "(let ((" ++ n ++ " " ++ tcode ++ ")) "
+                     ++ defc ++ ")"
     schExp i (NmConCase fc sc alts def)
         = do tcode <- schExp (i+1) sc
              defc <- maybe (pure Nothing) (\v => pure (Just !(schExp i v))) def

src/Core/Binary.idr

@@ -27,7 +27,7 @@ import Data.Buffer
 -- TTC files can only be compatible if the version number is the same
 export
 ttcVersion : Int
-ttcVersion = 22
+ttcVersion = 23
 
 export
 checkTTCVersion : String -> Int -> Int -> Core ()
@@ -39,9 +39,6 @@ record TTCFile extra where
   version : Int
   ifaceHash : Int
   importHashes : List (List String, Int)
-  holes : List (Int, (FC, Name))
-  guesses : List (Int, (FC, Name))
-  constraints : List (Int, Constraint)
   context : List (Name, Binary)
   userHoles : List Name
   autoHints : List (Name, Bool)
@@ -86,7 +83,6 @@ HasNames (Name, Name, Bool) where
 
 HasNames e => HasNames (TTCFile e) where
   full gam (MkTTCFile version ifaceHash iHashes
-                      holes guesses constraints
                       context userHoles
                       autoHints typeHints
                       imported nextVar currentNS nestedNS
@@ -94,9 +90,6 @@ HasNames e => HasNames (TTCFile e) where
                       namedirectives cgdirectives
                       extra)
       = pure $ MkTTCFile version ifaceHash iHashes
-                         !(traverse (full gam) holes)
-                         !(traverse (full gam) guesses)
-                         constraints
                          context userHoles
                          !(traverse (full gam) autoHints)
                          !(traverse (full gam) typeHints)
@@ -127,7 +120,6 @@ HasNames e => HasNames (TTCFile e) where
   -- from the file we're going to add them to learn what the resolved names
   -- are supposed to be! But for completeness, let's do it right.
   resolved gam (MkTTCFile version ifaceHash iHashes
-                      holes guesses constraints
                       context userHoles
                       autoHints typeHints
                       imported nextVar currentNS nestedNS
@@ -135,9 +127,6 @@ HasNames e => HasNames (TTCFile e) where
                       namedirectives cgdirectives
                       extra)
       = pure $ MkTTCFile version ifaceHash iHashes
-                         !(traverse (resolved gam) holes)
-                         !(traverse (resolved gam) guesses)
-                         constraints
                          context userHoles
                          !(traverse (resolved gam) autoHints)
                          !(traverse (resolved gam) typeHints)
@@ -182,9 +171,6 @@ writeTTCFile b file_in
            toBuf b (version file)
            toBuf b (ifaceHash file)
            toBuf b (importHashes file)
---            toBuf b (holes file)
---            toBuf b (guesses file)
---            toBuf b (constraints file)
            toBuf b (context file)
            toBuf b (userHoles file)
            toBuf b (autoHints file)
@@ -211,12 +197,6 @@ readTTCFile modns as b
            checkTTCVersion (show modns) ver ttcVersion
            ifaceHash <- fromBuf b
            importHashes <- fromBuf b
---            holes <- fromBuf b
---            coreLift $ putStrLn $ "Read " ++ show (length holes) ++ " holes"
---            guesses <- fromBuf b
---            coreLift $ putStrLn $ "Read " ++ show (length guesses) ++ " guesses"
---            constraints <- the (Core (List (Int, Constraint))) $ fromBuf b
---            coreLift $ putStrLn $ "Read " ++ show (length constraints) ++ " constraints"
            defs <- logTime ("Definitions " ++ show modns) $ fromBuf b
            uholes <- fromBuf b
            autohs <- fromBuf b
@@ -234,7 +214,7 @@ readTTCFile modns as b
            cgds <- fromBuf b
            ex <- fromBuf b
            pure (MkTTCFile ver ifaceHash importHashes
-                           [] [] [] defs uholes -- holes guesses constraints defs
+                           defs uholes
                            autohs typehs imp nextv cns nns
                            pns rws prims nds cgds ex)
 
@@ -250,7 +230,8 @@ getSaveDefs (n :: ns) acc defs
               Builtin _ => getSaveDefs ns acc defs
               _ => do bin <- initBinaryS 16384
                       toBuf bin !(full (gamma defs) gdef)
-                      getSaveDefs ns ((fullname gdef, !(get Bin)) :: acc) defs
+                      b <- get Bin
+                      getSaveDefs ns ((fullname gdef, b) :: acc) defs
 
 -- Write out the things in the context which have been defined in the
 -- current source file
@@ -267,9 +248,6 @@ writeToTTC extradata fname
          log 5 $ "Writing " ++ fname ++ " with hash " ++ show (ifaceHash defs)
          writeTTCFile buf
                    (MkTTCFile ttcVersion (ifaceHash defs) (importHashes defs)
-                              (toList (holes ust))
-                              (toList (guesses ust))
-                              (toList (constraints ust))
                               gdefs
                               (keys (userHoles defs))
                               (saveAutoHints defs)
@@ -436,9 +414,7 @@ readFromTTC loc reexp fname modNS importAs
                -- Finally, update the unification state with the holes from the
                -- ttc
                ust <- get UST
-               put UST (record { holes = fromList (holes ttc),
-                                 constraints = fromList (constraints ttc),
-                                 nextName = nextVar ttc } ust)
+               put UST (record { nextName = nextVar ttc } ust)
                pure (Just (ex, ifaceHash ttc, imported ttc))
 
 getImportHashes : String -> Ref Bin Binary ->

src/Core/Core.idr

@@ -48,7 +48,7 @@ data Error
     | CantConvert FC (Env Term vars) (Term vars) (Term vars)
     | CantSolveEq FC (Env Term vars) (Term vars) (Term vars)
     | PatternVariableUnifies FC (Env Term vars) Name (Term vars)
-    | CyclicMeta FC Name
+    | CyclicMeta FC (Env Term vars) Name (Term vars)
     | WhenUnifying FC (Env Term vars) (Term vars) (Term vars) Error
     | ValidCase FC (Env Term vars) (Either (Term vars) Error)
     | UndefinedName FC Name
@@ -124,8 +124,9 @@ Show Error where
       = show fc ++ ":" ++ show x ++ " and " ++ show y ++ " are not equal"
   show (PatternVariableUnifies fc env n x)
       = show fc ++ ":Pattern variable " ++ show n ++ " unifies with " ++ show x
-  show (CyclicMeta fc n)
+  show (CyclicMeta fc env n tm)
       = show fc ++ ":Cycle detected in metavariable solution " ++ show n
+             ++ " = " ++ show tm
   show (WhenUnifying fc _ x y err)
       = show fc ++ ":When unifying: " ++ show x ++ " and " ++ show y ++ "\n\t" ++ show err
   show (ValidCase fc _ prob)
@@ -275,7 +276,7 @@ getErrorLoc (Fatal err) = getErrorLoc err
 getErrorLoc (CantConvert loc _ _ _) = Just loc
 getErrorLoc (CantSolveEq loc _ _ _) = Just loc
 getErrorLoc (PatternVariableUnifies loc _ _ _) = Just loc
-getErrorLoc (CyclicMeta loc _) = Just loc
+getErrorLoc (CyclicMeta loc _ _ _) = Just loc
 getErrorLoc (WhenUnifying loc _ _ _ _) = Just loc
 getErrorLoc (ValidCase loc _ _) = Just loc
 getErrorLoc (UndefinedName loc _) = Just loc

src/Core/Directory.idr

@@ -83,7 +83,7 @@ nsToSource loc ns
          let fnameOrig = showSep dirSep (reverse ns)
          let fnameBase = maybe fnameOrig (\srcdir => srcdir ++ dirSep ++ fnameOrig) (source_dir d)
          let fs = map (\ext => fnameBase ++ ext)
-                      [".idr", ".lidr", ".yaff"]
+                      [".idr", ".lidr", ".yaff", ".org", ".md"]
          Just f <- firstAvailable fs
             | Nothing => throw (ModuleNotFound loc ns)
          pure f
@@ -192,7 +192,7 @@ getEntries d
              | Left err => pure []
          ds <- assert_total $ getEntries d
          pure (f :: ds)
-  
+
 dirEntries : String -> IO (Either FileError (List String))
 dirEntries dir
     = do Right d <- dirOpen dir
@@ -200,7 +200,7 @@ dirEntries dir
          ds <- getEntries d
          dirClose d
          pure (Right ds)
-  
+
 findIpkg : List String -> Maybe String
 findIpkg [] = Nothing
 findIpkg (f :: fs)

src/Core/Normalise.idr

@@ -54,15 +54,16 @@ export
 toClosure : EvalOpts -> Env Term outer -> Term outer -> Closure outer
 toClosure opts env tm = MkClosure opts [] env tm
 
-useMeta : FC -> Name -> Defs -> EvalOpts -> Core EvalOpts
-useMeta fc (Resolved i) defs opts
+useMeta : Bool -> FC -> Name -> Defs -> EvalOpts -> Core (Maybe EvalOpts)
+useMeta False _ _ _ opts = pure $ Just opts
+useMeta True fc (Resolved i) defs opts
     = case lookup i (usedMetas opts) of
-           Nothing => pure (record { usedMetas $= insert i () } opts)
-           Just _ => throw (CyclicMeta fc (Resolved i))
-useMeta fc n defs opts
+           Nothing => pure (Just (record { usedMetas $= insert i () } opts))
+           Just _ => pure Nothing
+useMeta True fc n defs opts
     = do let Just i = getNameID n (gamma defs)
               | Nothing => throw (UndefinedName fc n)
-         useMeta fc (Resolved i) defs opts
+         useMeta True fc (Resolved i) defs opts
 
 parameters (defs : Defs, topopts : EvalOpts)
   mutual
@@ -195,9 +196,8 @@ parameters (defs : Defs, topopts : EvalOpts)
                                         (visibility res)
              if redok
                 then do
-                   opts' <- if noCycles res
-                               then useMeta fc n defs topopts
-                               else pure topopts
+                   Just opts' <- useMeta (noCycles res) fc n defs topopts
+                        | Nothing => pure def
                    evalDef env opts' meta fc
                            (multiplicity res) (definition res) (flags res) stk def
                 else pure def
@@ -600,6 +600,8 @@ normaliseHoles defs env tm
 
 export
 normaliseLHS : Defs -> Env Term free -> Term free -> Core (Term free)
+normaliseLHS defs env (Bind fc n b sc)
+    = pure $ Bind fc n b !(normaliseLHS defs (b :: env) sc)
 normaliseLHS defs env tm
     = quote defs env !(nfOpts onLHS defs env tm)
 

src/Core/Unify.idr

@@ -12,6 +12,7 @@ import Core.Value
 
 import Data.IntMap
 import Data.List.Views
+import Data.NameMap
 
 %default covering
 
@@ -183,11 +184,35 @@ convertErrorS s loc env x y
     = if s then convertError loc env y x
            else convertError loc env x y
 
+-- Find all the metavariables required by each of the given names.
+-- We'll assume all meta solutions are of the form STerm exp.
+chaseMetas : {auto c : Ref Ctxt Defs} ->
+             List Name -> NameMap () -> Core (List Name)
+chaseMetas [] all = pure (keys all)
+chaseMetas (n :: ns) all
+    = case lookup n all of
+           Just _ => chaseMetas ns all
+           _ => do defs <- get Ctxt
+                   Just (PMDef _ _ (STerm soln) _ _) <-
+                                  lookupDefExact n (gamma defs)
+                        | _ => chaseMetas ns (insert n () all)
+                   let sns = keys (getMetas soln)
+                   chaseMetas (sns ++ ns) (insert n () all)
+
+-- Get all the metavariable names used by the term (recursively, so we
+-- can do the occurs check)
+getMetaNames : {auto c : Ref Ctxt Defs} ->
+               Term vars -> Core (List Name)
+getMetaNames tm
+    = let metas = getMetas tm in
+          chaseMetas (keys metas) empty
+
 postpone : {auto c : Ref Ctxt Defs} ->
            {auto u : Ref UST UState} ->
+           (blockedMeta : Bool) ->
            FC -> UnifyInfo -> String ->
            Env Term vars -> NF vars -> NF vars -> Core UnifyResult
-postpone loc mode logstr env x y
+postpone blockedMetas loc mode logstr env x y
     = do defs <- get Ctxt
          empty <- clearDefs defs
          logC 10 $
@@ -195,19 +220,42 @@ postpone loc mode logstr env x y
                  yq <- quote defs env y
                  pure (logstr ++ ": " ++ show !(toFullNames xq) ++
                                     " =?= " ++ show !(toFullNames yq))
-         c <- addConstraint (MkConstraint loc (atTop mode) env
-                                          !(quote empty env x)
-                                          !(quote empty env y))
+         xtm <- quote empty env x
+         ytm <- quote empty env y
+         -- Need to find all the metas in the constraint since solving any one
+         -- of them might stop the constraint being blocked.
+         metas <-
+             if blockedMetas
+                then let xmetas = getMetas xtm in
+                         chaseMetas (keys (addMetas xmetas ytm)) NameMap.empty
+                else pure []
+         blocked <- filterM undefinedN metas
+         c <- addConstraint (MkConstraint loc (atTop mode) blocked env
+                                          xtm
+                                          ytm)
+         log 10 $ show c ++ " NEW CONSTRAINT " ++ show loc ++
+                 " blocked on " ++ show metas
+         logTerm 10 "X" xtm
+         logTerm 10 "Y" ytm
          pure (constrain c)
+  where
+    undefinedN : Name -> Core Bool
+    undefinedN n
+        = do defs <- get Ctxt
+             case !(lookupDefExact n (gamma defs)) of
+                  Just (Hole _ _) => pure True
+                  Just (BySearch _ _ _) => pure True
+                  Just (Guess _ _ _) => pure True
+                  _ => pure False
 
 postponeS : {auto c : Ref Ctxt Defs} ->
             {auto u : Ref UST UState} ->
-            Bool -> FC -> UnifyInfo -> String -> Env Term vars ->
+            Bool -> Bool -> FC -> UnifyInfo -> String -> Env Term vars ->
             NF vars -> NF vars ->
             Core UnifyResult
-postponeS s loc mode logstr env x y
-    = if s then postpone loc (lower mode) logstr env y x
-           else postpone loc mode logstr env x y
+postponeS b s loc mode logstr env x y
+    = if s then postpone b loc (lower mode) logstr env y x
+           else postpone b loc mode logstr env x y
 
 unifyArgs : (Unify tm, Quote tm) =>
             {auto c : Ref Ctxt Defs} ->
@@ -340,6 +388,44 @@ patternEnvTm {vars} env args
                Nothing => updateVars ps svs
                Just p' => p' :: updateVars ps svs
 
+-- Check that the metavariable name doesn't occur in the solution.
+-- If it does, normalising might help. If it still does, that's an error.
+
+-- Also block if there's an unsolved meta under a function application,
+-- because that might cause future problems to get stuck even if they're
+-- solvable.
+occursCheck : {auto c : Ref Ctxt Defs} ->
+              FC -> Env Term vars -> UnifyInfo ->
+              Name -> Term vars -> Core (Maybe (Term vars))
+occursCheck fc env mode mname tm
+    = do solmetas <- getMetaNames tm
+         let False = mname `elem` solmetas
+             | _ => do defs <- get Ctxt
+                       tmnf <- normalise defs env tm
+                       solmetas <- getMetaNames tmnf
+                       if mname `elem` solmetas
+                          then do failOnStrongRigid False
+                                     (throw (CyclicMeta fc env mname tmnf))
+                                     tmnf
+                                  pure Nothing
+                          else pure $ Just tmnf
+         pure $ Just tm
+  where
+    -- Throw an occurs check failure if the name appears 'strong rigid',
+    -- that is, under a constructor form rather than a function, in the
+    -- term
+    failOnStrongRigid : Bool -> Core () -> Term vars -> Core ()
+    failOnStrongRigid bad err (Meta _ n _ _)
+        = if bad && n == mname
+             then err
+             else pure ()
+    failOnStrongRigid bad err tm
+        = case getFnArgs tm of
+               (f, []) => pure ()
+               (Ref _ Func _, _) => pure () -- might reduce away, just block
+               (Ref _ _ _, args) => traverse_ (failOnStrongRigid True err) args
+               (f, args) => traverse_ (failOnStrongRigid bad err) args
+
 -- Instantiate a metavariable by binding the variables in 'newvars'
 -- and returning the term
 -- If the type of the metavariable doesn't have enough arguments, fail, because
@@ -488,7 +574,8 @@ mutual
              if !(convert defs env x y)
                 then pure success
                 else if post
-                        then postpone loc mode ("Postponing unifyIfEq " ++
+                        then postpone True
+                                      loc mode ("Postponing unifyIfEq " ++
                                                  show (atTop mode)) env x y
                         else convertError loc env x y
 
@@ -564,14 +651,14 @@ mutual
                                        (con (reverse fargs))
                                        (NApp fc (NMeta mname mref margs) (reverse hargs))
                                  pure (union ures uargs))
-                          (postponeS swap fc mode "Postponing hole application [1]" env
+                          (postponeS True swap fc mode "Postponing hole application [1]" env
                                 (NApp fc (NMeta mname mref margs) margs')
                                 (con args'))
-                     _ => postponeS swap fc mode "Postponing hole application [2]" env
+                     _ => postponeS True swap fc mode "Postponing hole application [2]" env
                                 (NApp fc (NMeta mname mref margs) margs')
                                 (con args')
               else -- TODO: Cancellable function applications
-                   postpone fc mode "Postponing hole application [3]" env
+                   postpone True fc mode "Postponing hole application [3]" env
                             (NApp fc (NMeta mname mref margs) margs') (con args')
 
   -- Unify a hole application - we have already checked that the hole is
@@ -606,7 +693,7 @@ mutual
            if inv
               then unifyInvertible swap mode loc env mname mref margs margs' Nothing
                                    (NApp nfc (NMeta n i margs2)) args2'
-              else postponeS swap loc mode "Postponing hole application" env
+              else postponeS True swap loc mode "Postponing hole application" env
                              (NApp loc (NMeta mname mref margs) margs') tm
     where
       isPatName : Name -> Bool
@@ -614,7 +701,7 @@ mutual
       isPatName _ = False
 
   unifyHoleApp swap mode loc env mname mref margs margs' tm
-      = postponeS swap loc mode "Postponing hole application" env
+      = postponeS True swap loc mode "Postponing hole application" env
                  (NApp loc (NMeta mname mref margs) margs') tm
 
   postponePatVar : {auto c : Ref Ctxt Defs} ->
@@ -632,7 +719,8 @@ mutual
            defs <- get Ctxt
            if !(convert defs env x tm)
               then pure success
-              else postponeS swap loc mode "Not in pattern fragment" env
+              else postponeS False -- it's not the metavar that's blocked
+                             swap loc mode "Not in pattern fragment" env
                              x tm
 
   solveHole : {auto c : Ref Ctxt Defs} ->
@@ -704,10 +792,15 @@ mutual
                   do Just hdef <- lookupCtxtExact (Resolved mref) (gamma defs)
                          | _ => postponePatVar swap mode loc env mname mref margs margs' tmnf
                      let Hole _ _ = definition hdef
-                         | _ => postponeS swap loc mode "Delayed hole" env
+                         | _ => postponeS True swap loc mode "Delayed hole" env
                                           (NApp loc (NMeta mname mref margs) margs')
                                           tmnf
                      tm <- quote empty env tmnf
+                     Just tm <- occursCheck loc env mode mname tm
+                         | _ => postponeS True swap loc mode "Occurs check failed" env
+                                          (NApp loc (NMeta mname mref margs) margs')
+                                          tmnf
+
                      case shrinkTerm tm submv of
                           Just stm => solveHole fc mode env mname mref
                                                 margs margs' locs submv
@@ -715,7 +808,7 @@ mutual
                           Nothing =>
                             do tm' <- normalise defs env tm
                                case shrinkTerm tm' submv of
-                                    Nothing => postponeS swap loc mode "Can't shrink" env
+                                    Nothing => postponeS True swap loc mode "Can't shrink" env
                                                (NApp loc (NMeta mname mref margs) margs')
                                                tmnf
                                     Just stm => solveHole fc mode env mname mref
@@ -738,13 +831,14 @@ mutual
   -- Postpone if a name application against an application, unless they are
   -- convertible
   unifyApp swap mode loc env fc (NRef nt n) args tm
-      = if not swap
-           then unifyIfEq True loc mode env (NApp fc (NRef nt n) args) tm
-           else unifyIfEq True loc mode env tm (NApp fc (NRef nt n) args)
+      = do log 10 $ "Name against app, unifyIfEq"
+           if not swap
+              then unifyIfEq True loc mode env (NApp fc (NRef nt n) args) tm
+              else unifyIfEq True loc mode env tm (NApp fc (NRef nt n) args)
   unifyApp swap mode loc env xfc (NLocal rx x xp) [] (NApp yfc (NLocal ry y yp) [])
       = do gam <- get Ctxt
            if x == y then pure success
-             else postponeS swap loc mode "Postponing var"
+             else postponeS True swap loc mode "Postponing var"
                             env (NApp xfc (NLocal rx x xp) [])
                                 (NApp yfc (NLocal ry y yp) [])
   -- A local against something canonical (binder or constructor) is bad
@@ -764,13 +858,13 @@ mutual
       = do gam <- get Ctxt
            if !(convert gam env (NApp fc hd args) tm)
               then pure success
-              else postponeS False loc mode "Postponing constraint"
+              else postponeS True False loc mode "Postponing constraint"
                              env (NApp fc hd args) tm
   unifyApp True mode loc env fc hd args tm
       = do gam <- get Ctxt
            if !(convert gam env tm (NApp fc hd args))
               then pure success
-              else postponeS True loc mode "Postponing constraint"
+              else postponeS True True loc mode "Postponing constraint"
                              env (NApp fc hd args) tm
 
   unifyBothApps : {auto c : Ref Ctxt Defs} ->
@@ -790,12 +884,13 @@ mutual
   unifyBothApps mode@(MkUnifyInfo p t InTerm) loc env xfc (NLocal xr x xp) xargs yfc (NLocal yr y yp) yargs
       = if x == y
            then unifyArgs mode loc env xargs yargs
-           else postpone loc mode "Postponing local app"
+           else postpone True loc mode "Postponing local app"
                          env (NApp xfc (NLocal xr x xp) xargs)
                              (NApp yfc (NLocal yr y yp) yargs)
   unifyBothApps mode loc env xfc (NLocal xr x xp) xargs yfc (NLocal yr y yp) yargs
-      = unifyIfEq True loc mode env (NApp xfc (NLocal xr x xp) xargs)
-                                    (NApp yfc (NLocal yr y yp) yargs)
+      = do log 10 $ "Both local apps, unifyIfEq"
+           unifyIfEq True loc mode env (NApp xfc (NLocal xr x xp) xargs)
+                                       (NApp yfc (NLocal yr y yp) yargs)
   -- If they're both holes, solve the one with the bigger context
   unifyBothApps mode loc env xfc (NMeta xn xi xargs) xargs' yfc (NMeta yn yi yargs) yargs'
       = do invx <- isDefInvertible xi
@@ -994,7 +1089,7 @@ mutual
              -- If we don't know it's injective, need to postpone the
              -- constraint. But before then, we need some way to decide
              -- what's injective...
---                then postpone loc mode env (quote empty env (NTCon x tagx ax xs))
+--                then postpone True loc mode env (quote empty env (NTCon x tagx ax xs))
 --                                           (quote empty env (NTCon y tagy ay ys))
            else convertError loc env
                      (NTCon xfc x tagx ax xs)
@@ -1014,13 +1109,15 @@ mutual
   unifyNoEta mode loc env y (NApp yfc hd args)
       = if umode mode /= InMatch
            then unifyApp True mode loc env yfc hd args y
-           else unifyIfEq True loc mode env y (NApp yfc hd args)
+           else do log 10 $ "Unify if Eq due to something with app"
+                   unifyIfEq True loc mode env y (NApp yfc hd args)
   -- Only try stripping as patterns as a last resort
   unifyNoEta mode loc env x (NAs _ _ _ y) = unifyNoEta mode loc env x y
   unifyNoEta mode loc env (NAs _ _ _ x) y = unifyNoEta mode loc env x y
   unifyNoEta mode loc env x y
       = do defs <- get Ctxt
            empty <- clearDefs defs
+           log 10 $ "Nothing else worked, unifyIfEq"
            unifyIfEq (isDelay x || isDelay y) loc mode env x y
     where
       -- If one of them is a delay, and they're not equal, we'd better
@@ -1172,8 +1269,13 @@ retry mode c
          case lookup c (constraints ust) of
               Nothing => pure success
               Just Resolved => pure success
-              Just (MkConstraint loc withLazy env x y)
-                  => catch (do logTermNF 5 ("Retrying " ++ show c) env x
+              Just (MkConstraint loc withLazy blocked env x y)
+                => if umode mode /= InTerm ||
+                         !(anyM definedN blocked) || isNil blocked
+                      -- only go if any of the blocked names are defined now
+                      then
+                        catch
+                           (do logTermNF 5 ("Retrying " ++ show c ++ " " ++ show (umode mode)) env x
                                logTermNF 5 "....with" env y
                                log 5 $ if withLazy
                                           then "(lazy allowed)"
@@ -1187,13 +1289,29 @@ retry mode c
                                           pure cs
                                  _ => do log 5 $ "Constraints " ++ show (addLazy cs)
                                          pure cs)
-                       (\err => throw (WhenUnifying loc env x y err))
+                          (\err => throw (WhenUnifying loc env x y err))
+                      else
+                        do log 10 $ show c ++ " still blocked on " ++ show blocked
+                           logTermNF 10 "X" env x
+                           logTermNF 10 "Y" env y
+                           pure (constrain c)
               Just (MkSeqConstraint loc env xs ys)
                   => do cs <- unifyArgs mode loc env xs ys
                         case constraints cs of
                              [] => do deleteConstraint c
                                       pure cs
                              _ => pure cs
+  where
+    definedN : Name -> Core Bool
+    definedN n
+        = do defs <- get Ctxt
+             Just gdef <- lookupCtxtExact n (gamma defs)
+                  | _ => pure False
+             case definition gdef of
+                  Hole _ _ => pure (invertible gdef)
+                  BySearch _ _ _ => pure False
+                  Guess _ _ _ => pure False
+                  _ => pure True
 
 delayMeta : LazyReason -> Nat -> Term vars -> Term vars -> Term vars
 delayMeta r (S k) ty (Bind fc n b sc)
@@ -1372,7 +1490,7 @@ checkDots
          put UST (record { dotConstraints = [] } ust)
   where
     checkConstraint : (Name, DotReason, Constraint) -> Core ()
-    checkConstraint (n, reason, MkConstraint fc wl env x y)
+    checkConstraint (n, reason, MkConstraint fc wl blocked env x y)
         = do logTermNF 10 "Dot" env y
              logTermNF 10 "  =" env x
              -- A dot is okay if the constraint is solvable *without solving

src/Core/UnifyState.idr

@@ -24,6 +24,7 @@ data Constraint : Type where
      MkConstraint : {vars : _} ->
                     FC ->
                     (withLazy : Bool) ->
+                    (blockedOn : List Name) ->
                     (env : Env Term vars) ->
                     (x : Term vars) -> (y : Term vars) ->
                     Constraint
@@ -41,8 +42,9 @@ data Constraint : Type where
 
 export
 TTC Constraint where
-  toBuf b (MkConstraint {vars} fc l env x y)
-     = do tag 0; toBuf b vars; toBuf b l;
+  toBuf b (MkConstraint {vars} fc l block env x y)
+     = do tag 0; toBuf b vars; toBuf b l
+          toBuf b block
           toBuf b fc; toBuf b env; toBuf b x; toBuf b y
   toBuf b (MkSeqConstraint {vars} fc env xs ys)
      = do tag 1; toBuf b vars; toBuf b fc; toBuf b env; toBuf b xs; toBuf b ys
@@ -51,9 +53,11 @@ TTC Constraint where
   fromBuf b
       = case !getTag of
              0 => do vars <- fromBuf b
-                     fc <- fromBuf b; l <- fromBuf b; env <- fromBuf b
+                     fc <- fromBuf b; l <- fromBuf b
+                     block <- fromBuf b
+                     env <- fromBuf b
                      x <- fromBuf b; y <- fromBuf b
-                     pure (MkConstraint {vars} fc l env x y)
+                     pure (MkConstraint {vars} fc l block env x y)
              1 => do vars <- fromBuf b
                      fc <- fromBuf b; env <- fromBuf b
                      xs <- fromBuf b; ys <- fromBuf b
@@ -279,7 +283,7 @@ addDot : {auto u : Ref UST UState} ->
 addDot fc env dotarg x reason y
     = do ust <- get UST
          put UST (record { dotConstraints $=
-                             ((dotarg, reason, MkConstraint fc False env x y) ::)
+                             ((dotarg, reason, MkConstraint fc False [] env x y) ::)
                          } ust)
 
 mkConstantAppArgs : Bool -> FC -> Env Term vars ->
@@ -540,7 +544,7 @@ checkValidHole (idx, (fc, n))
                      let Just c = lookup con (constraints ust)
                           | Nothing => pure ()
                      case c of
-                          MkConstraint fc l env x y =>
+                          MkConstraint fc l blocked env x y =>
                              do put UST (record { guesses = empty } ust)
                                 xnf <- normaliseHoles defs env x
                                 ynf <- normaliseHoles defs env y
@@ -641,7 +645,7 @@ dumpHole lvl hole
              case lookup n (constraints ust) of
                   Nothing => pure ()
                   Just Resolved => log lvl "\tResolved"
-                  Just (MkConstraint _ lazy env x y) =>
+                  Just (MkConstraint _ lazy _ env x y) =>
                     do log lvl $ "\t  " ++ show !(toFullNames !(normalise defs env x))
                                       ++ " =?= " ++ show !(toFullNames !(normalise defs env y))
                        log 5 $ "\t    from " ++ show !(toFullNames x)

src/Idris/Desugar.idr

@@ -533,8 +533,8 @@ mutual
   --         implementation headers (i.e. note their existence, but not the bodies)
   -- Everything else on the second pass
   getDecl : Pass -> PDecl -> Maybe PDecl
-  getDecl p (PImplementation fc vis _ is cons n ps iname nusing ds)
-      = Just (PImplementation fc vis p is cons n ps iname nusing ds)
+  getDecl p (PImplementation fc vis opts _ is cons n ps iname nusing ds)
+      = Just (PImplementation fc vis opts p is cons n ps iname nusing ds)
 
   getDecl p (PNamespace fc ns ds)
       = Just (PNamespace fc ns (mapMaybe (getDecl p) ds))
@@ -689,8 +689,9 @@ mutual
       expandConstraint (Nothing, p)
           = map (\x => (Nothing, x)) (pairToCons p)
 
-  desugarDecl ps (PImplementation fc vis pass is cons tn params impname nusing body)
-      = do is' <- traverse (\ (n,c,tm) => do tm' <- desugar AnyExpr ps tm
+  desugarDecl ps (PImplementation fc vis fnopts pass is cons tn params impname nusing body)
+      = do opts <- traverse (desugarFnOpt ps) fnopts
+           is' <- traverse (\ (n,c,tm) => do tm' <- desugar AnyExpr ps tm
                                              pure (n, c, tm')) is
            let _ = the (List (Name, RigCount, RawImp)) is'
            cons' <- traverse (\ (n, tm) => do tm' <- desugar AnyExpr ps tm
@@ -715,7 +716,7 @@ mutual
                           (\b => do b' <- traverse (desugarDecl ps) b
                                     pure (Just (concat b'))) body
            pure [IPragma (\c, nest, env =>
-                             elabImplementation fc vis pass env nest isb consb
+                             elabImplementation fc vis opts pass env nest isb consb
                                                 tn paramsb impname nusing
                                                 body')]
 

src/Idris/Elab/Implementation.idr

@@ -93,7 +93,7 @@ elabImplementation : {auto c : Ref Ctxt Defs} ->
                      {auto u : Ref UST UState} ->
                      {auto s : Ref Syn SyntaxInfo} ->
                      {auto m : Ref MD Metadata} ->
-                     FC -> Visibility -> Pass ->
+                     FC -> Visibility -> List FnOpt -> Pass ->
                      Env Term vars -> NestedNames vars ->
                      (implicits : List (Name, RigCount, RawImp)) ->
                      (constraints : List (Maybe Name, RawImp)) ->
@@ -104,7 +104,7 @@ elabImplementation : {auto c : Ref Ctxt Defs} ->
                      Maybe (List ImpDecl) ->
                      Core ()
 -- TODO: Refactor all these steps into separate functions
-elabImplementation {vars} fc vis pass env nest is cons iname ps impln nusing mbody
+elabImplementation {vars} fc vis opts_in pass env nest is cons iname ps impln nusing mbody
     = do let impName_in = maybe (mkImpl fc iname ps) id impln
          impName <- inCurrentNS impName_in
          syn <- get Syn
@@ -137,7 +137,8 @@ elabImplementation {vars} fc vis pass env nest is cons iname ps impln nusing mbo
          -- given when using named implementations
          --    (cs : Constraints) -> Impl params
          -- Don't make it a hint if it's a named implementation
-         let opts = maybe [Inline, Hint True] (const [Inline]) impln
+         let opts = maybe (opts_in ++ [Inline, Hint True])
+                          (const (opts_in ++ [Inline])) impln
 
          let initTy = bindImpls fc is $ bindConstraints fc AutoImplicit cons
                          (apply (IVar fc iname) ps)
@@ -354,7 +355,7 @@ elabImplementation {vars} fc vis pass env nest is cons iname ps impln nusing mbo
 
     mkTopMethDecl : (Name, Name, List (String, String), RigCount, RawImp) -> ImpDecl
     mkTopMethDecl (mn, n, upds, c, mty)
-        = IClaim fc c vis [] (MkImpTy fc n mty)
+        = IClaim fc c vis opts_in (MkImpTy fc n mty)
 
     -- Given the method type (result of topMethType) return the mapping from
     -- top level method name to current implementation's method name

src/Idris/Error.idr

@@ -46,8 +46,10 @@ perror (PatternVariableUnifies _ env n tm)
     showPVar : Name -> String
     showPVar (PV n _) = showPVar n
     showPVar n = show n
-perror (CyclicMeta _ n)
-    = pure $ "Cycle detected in solution of metavariable " ++ show n
+perror (CyclicMeta _ env n tm)
+    = pure $ "Cycle detected in solution of metavariable "
+               ++ show !(prettyName n) ++ " = "
+               ++ !(pshow env tm)
 perror (WhenUnifying _ env x y err)
     = pure $ "When unifying " ++ !(pshow env x) ++ " and " ++ !(pshow env y) ++ "\n"
        ++ !(perror err)

src/Idris/IDEMode/CaseSplit.idr

@@ -176,10 +176,10 @@ getClause l n
          argns <- getEnvArgNames defs envlen !(nf defs [] ty)
          Just srcLine <- getSourceLine l
            | Nothing => pure Nothing
-         let (lit, src) = isLit srcLine
-         pure (Just (indent lit loc ++ fnName True n ++ concat (map (" " ++) argns) ++
+         let (mark, src) = isLitLine srcLine
+         pure (Just (indent mark loc ++ fnName True n ++ concat (map (" " ++) argns) ++
                   " = ?" ++ fnName False n ++ "_rhs"))
   where
-    indent : Bool -> FC -> String
-    indent True fc = ">" ++ pack (replicate (cast (max 0 (snd (startPos fc) - 1))) ' ')
-    indent False fc = pack (replicate (cast (snd (startPos fc))) ' ')
+    indent : Maybe String -> FC -> String
+    indent (Just mark) fc = relit (Just mark) $ pack (replicate (cast (max 0 (snd (startPos fc) - 1))) ' ')
+    indent Nothing fc = pack (replicate (cast (snd (startPos fc))) ' ')

src/Idris/IDEMode/MakeClause.idr

@@ -16,15 +16,15 @@ showRHSName n
 export
 makeWith : Name -> String -> String
 makeWith n srcline
-    = let (lit, src) = isLit srcline
+    = let (markerM, src) = isLitLine srcline
           isrc : (Nat, String) =
              case span isSpace src of
                   (spc, rest) => (length spc, rest)
           indent = fst isrc
           src = snd isrc
           lhs = pack (readLHS 0 (unpack src)) in
-          mkWithArg lit indent lhs ++ "\n" ++
-          mkWithPat lit indent lhs ++ "\n"
+          mkWithArg markerM indent lhs ++ "\n" ++
+          mkWithPat markerM indent lhs ++ "\n"
   where
     readLHS : (brackets : Nat) -> List Char -> List Char
     readLHS Z ('=' :: rest) = []
@@ -35,17 +35,14 @@ makeWith n srcline
     readLHS n (x :: rest) = x :: readLHS n rest
     readLHS n [] = []
 
-    pref : Bool -> Nat -> String
-    pref l ind
-        = (if l then ">" else "") ++
-          pack (replicate ind ' ')
+    pref : Maybe String -> Nat -> String
+    pref mark ind = relit mark $ pack (replicate ind ' ')
 
-    mkWithArg : Bool -> Nat -> String -> String
-    mkWithArg lit indent lhs
-        = pref lit indent ++ lhs ++ "with (_)"
+    mkWithArg : Maybe String -> Nat -> String -> String
+    mkWithArg mark indent lhs
+        = pref mark indent ++ lhs ++ "with (_)"
 
-    mkWithPat : Bool -> Nat -> String -> String
-    mkWithPat lit indent lhs
-        = pref lit (indent + 2) ++ lhs ++ "| with_pat = ?" ++
+    mkWithPat : Maybe String -> Nat -> String -> String
+    mkWithPat mark indent lhs
+        = pref mark (indent + 2) ++ lhs ++ "| with_pat = ?" ++
               showRHSName n ++ "_rhs"
-

src/Idris/IDEMode/REPL.idr

@@ -258,7 +258,8 @@ displayIDEResult outf i  (VersionIs x) = printIDEResult outf i versionSExp
 
 displayIDEResult outf i  (Edited (DisplayEdit xs)) = printIDEResult outf i $ StringAtom $ showSep "\n" xs
 displayIDEResult outf i  (Edited (EditError x)) = printIDEError outf i x
-displayIDEResult outf i  (Edited (MadeLemma lit name pty pappstr)) = printIDEResult outf i $ StringAtom $ (if lit then "> " else "") ++ show name ++ " : " ++ show pty ++ "\n" ++ pappstr
+displayIDEResult outf i  (Edited (MadeLemma lit name pty pappstr)) =
+  printIDEResult outf i $ StringAtom $ (relit lit $ show name ++ " : " ++ show pty ++ "\n") ++ pappstr
 displayIDEResult outf i  _ = pure ()
 
 

src/Idris/Parser.idr

@@ -1221,7 +1221,9 @@ ifaceDecl fname indents
 implDecl : FileName -> IndentInfo -> Rule PDecl
 implDecl fname indents
     = do start <- location
-         vis <- visibility
+         visOpts <- many (visOpt fname)
+         vis <- getVisibility Nothing visOpts
+         let opts = mapMaybe getRight visOpts
          col <- column
          option () (keyword "implementation")
          iname <- option Nothing (do symbol "["
@@ -1240,7 +1242,7 @@ implDecl fname indents
          atEnd indents
          end <- location
          pure (PImplementation (MkFC fname start end)
-                         vis Single impls cons n params iname nusing
+                         vis opts Single impls cons n params iname nusing
                          (map (collectDefs . concat) body))
 
 fieldDecl : FileName -> IndentInfo -> Rule (List PField)

src/Idris/ProcessIdr.idr

@@ -194,7 +194,7 @@ export
 getParseErrorLoc : String -> ParseError -> FC
 getParseErrorLoc fname (ParseFail _ (Just pos) _) = MkFC fname pos pos
 getParseErrorLoc fname (LexFail (l, c, _)) = MkFC fname (l, c) (l, c)
-getParseErrorLoc fname (LitFail (l :: _)) = MkFC fname (l, 0) (l, 0)
+getParseErrorLoc fname (LitFail (MkLitErr l c _)) = MkFC fname (l, 0) (l, 0)
 getParseErrorLoc fname _ = replFC
 
 export
@@ -203,7 +203,7 @@ readHeader : {auto c : Ref Ctxt Defs} ->
 readHeader path
     = do Right res <- coreLift (readFile path)
             | Left err => throw (FileErr path err)
-         case runParserTo (isLitFile path) False isColon res (progHdr path) of
+         case runParserTo (isLitFile path) isColon res (progHdr path) of
               Left err => throw (ParseFail (getParseErrorLoc path err) err)
               Right mod => pure mod
   where
@@ -227,10 +227,10 @@ processMod : {auto c : Ref Ctxt Defs} ->
              (sourcecode : String) ->
              Core (Maybe (List Error))
 processMod srcf ttcf msg sourcecode
-    = catch (do 
+    = catch (do
         -- Just read the header to start with (this is to get the imports and
         -- see if we can avoid rebuilding if none have changed)
-        modh <- readHeader srcf 
+        modh <- readHeader srcf
         -- Add an implicit prelude import
         let imps =
              if (noprelude !getSession || moduleNS modh == ["Prelude"])
@@ -261,7 +261,7 @@ processMod srcf ttcf msg sourcecode
            else -- needs rebuilding
              do iputStrLn msg
                 Right mod <- logTime ("Parsing " ++ srcf) $
-                            pure (runParser (isLitFile srcf) True sourcecode (do p <- prog srcf; eoi; pure p))
+                            pure (runParser (isLitFile srcf) sourcecode (do p <- prog srcf; eoi; pure p))
                       | Left err => pure (Just [ParseFail (getParseErrorLoc srcf err) err])
                 initHash
                 resetNextVar

src/Idris/REPL.idr

@@ -246,21 +246,21 @@ anyAt p loc y = p loc
 
 printClause : {auto c : Ref Ctxt Defs} ->
               {auto s : Ref Syn SyntaxInfo} ->
-              Bool -> Nat -> ImpClause ->
+              Maybe String -> Nat -> ImpClause ->
               Core String
 printClause l i (PatClause _ lhsraw rhsraw)
     = do lhs <- pterm lhsraw
          rhs <- pterm rhsraw
-         pure ((if l then ">" else "") ++ (pack (replicate i ' ') ++ show lhs ++ " = " ++ show rhs))
+         pure (relit l (pack (replicate i ' ') ++ show lhs ++ " = " ++ show rhs))
 printClause l i (WithClause _ lhsraw wvraw csraw)
     = do lhs <- pterm lhsraw
          wval <- pterm wvraw
          cs <- traverse (printClause l (i + 2)) csraw
-         pure ((if l then ">" else "") ++ (pack (replicate i ' ') ++ show lhs ++ " with (" ++ show wval ++ ")\n" ++
+         pure ((relit l ((pack (replicate i ' ') ++ show lhs ++ " with (" ++ show wval ++ ")\n")) ++
                  showSep "\n" cs))
 printClause l i (ImpossibleClause _ lhsraw)
     = do lhs <- pterm lhsraw
-         pure ((if l then ">" else "") ++ (pack (replicate i ' ') ++ show lhs ++ " impossible"))
+         pure (relit l (pack (replicate i ' ') ++ show lhs ++ " impossible"))
 
 
 lookupDefTyName : Name -> Context ->
@@ -271,7 +271,7 @@ public export
 data EditResult : Type where
   DisplayEdit : List String -> EditResult
   EditError : String -> EditResult
-  MadeLemma : Bool -> Name -> PTerm -> String -> EditResult
+  MadeLemma : Maybe String -> Name -> PTerm -> String -> EditResult
 
 updateFile : {auto r : Ref ROpts REPLOpts} ->
              (List String -> List String) -> Core EditResult
@@ -311,19 +311,19 @@ proofSearch n res Z (x :: xs) = replaceStr ("?" ++ show n) res x :: xs
 proofSearch n res (S k) (x :: xs) = x :: proofSearch n res k xs
 proofSearch n res _ [] = []
 
-addMadeLemma : Bool -> Name -> String -> String -> Nat -> List String -> List String
+addMadeLemma : Maybe String -> Name -> String -> String -> Nat -> List String -> List String
 addMadeLemma lit n ty app line content
     = addApp lit line [] (proofSearch n app line content)
   where
     -- Put n : ty in the first blank line
-    insertInBlank : Bool -> List String -> List String
-    insertInBlank lit [] = [(if lit then "> " else "") ++ show n ++ " : " ++ ty ++ "\n"]
+    insertInBlank : Maybe String -> List String -> List String
+    insertInBlank lit [] = [relit lit $ show n ++ " : " ++ ty ++ "\n"]
     insertInBlank lit (x :: xs)
         = if trim x == ""
-             then ("\n" ++ (if lit then "> " else "") ++ show n ++ " : " ++ ty ++ "\n") :: xs
+             then ("\n" ++ (relit lit $ show n ++ " : " ++ ty ++ "\n")) :: xs
              else x :: insertInBlank lit xs
 
-    addApp : Bool -> Nat -> List String -> List String -> List String
+    addApp : Maybe String -> Nat -> List String -> List String -> List String
     addApp lit Z acc rest = reverse (insertInBlank lit acc) ++ rest
     addApp lit (S k) acc (x :: xs) = addApp lit k (x :: acc) xs
     addApp _ (S k) acc [] = reverse acc
@@ -420,9 +420,9 @@ processEdit (GenerateDef upd line name)
                            | Nothing => processEdit (AddClause upd line name)
                         Just srcLine <- getSourceLine line
                            | Nothing => pure (EditError "Source line not found")
-                        let (lit, _) = isLit srcLine
-                        let l : Nat = if lit then cast (max 0 (snd (startPos fc) - 1)) else cast (snd (startPos fc))
-                        ls <- traverse (printClause lit l) cs
+                        let (markM, srcLineUnlit) = isLitLine srcLine
+                        let l : Nat =  cast (snd (startPos fc))
+                        ls <- traverse (printClause markM l) cs
                         if upd
                            then updateFile (addClause (unlines ls) (cast line))
                            else pure $ DisplayEdit ls)
@@ -444,11 +444,12 @@ processEdit (MakeLemma upd line name)
                                             else papp)
                      Just srcLine <- getSourceLine line
                        | Nothing => pure (EditError "Source line not found")
-                     let (lit, _) = isLit srcLine
+                     let (markM,_) = isLitLine srcLine
+                     let markML : Nat = length (fromMaybe "" markM)
                      if upd
-                        then updateFile (addMadeLemma lit name (show pty) pappstr
-                                                      (cast (line - 1)))
-                        else pure $ MadeLemma lit name pty pappstr
+                        then updateFile (addMadeLemma markM name (show pty) pappstr
+                                                      (max 0 (cast (line - 1))))
+                        else pure $ MadeLemma markM name pty pappstr
               _ => pure $ EditError "Can't make lifted definition"
 processEdit (MakeCase upd line name)
     = pure $ EditError "Not implemented yet"
@@ -739,7 +740,7 @@ export
 parseRepl : String -> Either ParseError (Maybe REPLCmd)
 parseRepl inp
     = case fnameCmd [(":load ", Load), (":l ", Load), (":cd ", CD)] inp of
-           Nothing => runParser False False inp (parseEmptyCmd <|> parseCmd)
+           Nothing => runParser Nothing inp (parseEmptyCmd <|> parseCmd)
            Just cmd => Right $ Just cmd
   where
     -- a right load of hackery - we can't tokenise the filename using the
@@ -855,7 +856,7 @@ mutual
   displayResult  (Edited (DisplayEdit [])) = pure ()
   displayResult  (Edited (DisplayEdit xs)) = printResult $ showSep "\n" xs
   displayResult  (Edited (EditError x)) = printError x
-  displayResult  (Edited (MadeLemma lit name pty pappstr)) = printResult ((if lit then "> " else "") ++ show name ++ " : " ++ show pty ++ "\n" ++ pappstr)
+  displayResult  (Edited (MadeLemma lit name pty pappstr)) = printResult (relit lit (show name ++ " : " ++ show pty ++ "\n") ++ pappstr)
   displayResult  (OptionsSet opts) = printResult $ showSep "\n" $ map show opts
   displayResult  _ = pure ()
 

src/Idris/Syntax.idr

@@ -211,7 +211,7 @@ mutual
                     List PDecl ->
                     PDecl
        PImplementation : FC ->
-                         Visibility -> Pass ->
+                         Visibility -> List PFnOpt -> Pass ->
                          (implicits : List (Name, RigCount, PTerm)) ->
                          (constraints : List (Maybe Name, PTerm)) ->
                          Name ->
@@ -819,14 +819,14 @@ mapPTermM f = goPTerm where
                       <*> pure ns
                       <*> pure mn
                       <*> goPDecls ps
-    goPDecl (PImplementation fc v p is cs n ts mn ns mps) =
-      PImplementation fc v p <$> go3TupledPTerms is
-                             <*> goPairedPTerms cs
-                             <*> pure n
-                             <*> goPTerms ts
-                             <*> pure mn
-                             <*> pure ns
-                             <*> goMPDecls mps
+    goPDecl (PImplementation fc v opts p is cs n ts mn ns mps) =
+      PImplementation fc v opts p <$> go3TupledPTerms is
+                                  <*> goPairedPTerms cs
+                                  <*> pure n
+                                  <*> goPTerms ts
+                                  <*> pure mn
+                                  <*> pure ns
+                                  <*> goMPDecls mps
     goPDecl (PRecord fc v n nts mn fs) =
       PRecord fc v n <$> go4TupledPTerms nts
                      <*> pure mn

src/Parser/Support.idr

@@ -22,7 +22,7 @@ public export
 data ParseError = ParseFail String (Maybe (Int, Int)) (List Token)
                 | LexFail (Int, Int, String)
                 | FileFail FileError
-                | LitFail (List Int)
+                | LitFail LiterateError
 
 export
 Show ParseError where
@@ -33,8 +33,8 @@ Show ParseError where
       = "Lex error at " ++ show (c, l) ++ " input: " ++ str
   show (FileFail err)
       = "File error: " ++ show err
-  show (LitFail l)
-      = "Lit error(s) at " ++ show l
+  show (LitFail (MkLitErr l c str))
+      = "Lit error(s) at " ++ show (c, l) ++ " input: " ++ str
 
 export
 eoi : EmptyRule ()
@@ -47,10 +47,10 @@ eoi
     isEOI _ = False
 
 export
-runParserTo : Bool -> Bool -> (TokenData Token -> Bool) ->
+runParserTo : Maybe LiterateStyle -> (TokenData Token -> Bool) ->
               String -> Grammar (TokenData Token) e ty -> Either ParseError ty
-runParserTo lit enforce pred str p
-    = case unlit lit enforce str of
+runParserTo lit pred str p
+    = case unlit lit str of
            Left l => Left $ LitFail l
            Right str =>
              case lexTo pred str of
@@ -65,15 +65,15 @@ runParserTo lit enforce pred str p
                        Right (val, _) => Right val
 
 export
-runParser : Bool -> Bool -> String -> Grammar (TokenData Token) e ty -> Either ParseError ty
-runParser lit enforce = runParserTo lit enforce (const False)
+runParser : Maybe LiterateStyle -> String -> Grammar (TokenData Token) e ty -> Either ParseError ty
+runParser lit = runParserTo lit (const False)
 
 export
 parseFile : (fn : String) -> Rule ty -> IO (Either ParseError ty)
 parseFile fn p
     = do Right str <- readFile fn
              | Left err => pure (Left (FileFail err))
-         pure (runParser (isLitFile fn) True str p)
+         pure (runParser (isLitFile fn) str p)
 
 
 -- Some basic parsers used by all the intermediate forms
@@ -590,5 +590,3 @@ nonEmptyBlock item
          res <- blockEntry (AtPos col) item
          ps <- blockEntries (snd res) item
          pure (fst res :: ps)
-
-

src/Parser/Unlit.idr

@@ -1,44 +1,67 @@
 module Parser.Unlit
 
+import public Text.Literate
+
 %default total
+%access export
+
+public export
+data LiterateModes = Bird | Org | CMark
 
 export
-isLitFile : String -> Bool
-isLitFile file = isSuffixOf ".lidr" file
-
-data LineType = Blank | Code | Text
-
-lineType : String -> (LineType, String)
-lineType str = if length str > 0
-  then
-    if assert_total (strHead str) == '>'
-       then (Code, assert_total (strTail str))
-       else
-         if all isSpace (unpack str)
-            then (Blank, str)
-            else (Text, str)
-  else (Blank, str)
+styleBird : LiterateStyle
+styleBird = MkLitStyle Nil [">", "<"] [".lidr"]
 
 export
-isLit : String -> (Bool, String)
-isLit str = case lineType str of
-               (Code, tail) => (True, tail)
-               _ => (False, str)
+styleOrg : LiterateStyle
+styleOrg = MkLitStyle
+              [ ("#+BEGIN_SRC idris","#+END_SRC")
+              , ("#+begin_src idris","#+end_src")
+              , ("#+COMMENT idris","#+END_COMMENT")
+              , ("#+comment idris","#+end_comment")]
+              ["#+IDRIS:"]
+              [".org"]
 
 export
-unlit : Bool -> Bool -> String -> Either (List Int) String
-unlit lit enforce str = if lit
-  then let (_, lns, errors) = foldr unlit' (Blank, [], []) (lines str) in
-           if enforce
-              then case errors of
-                        [] => Right (unlines lns)
-                        _ => let l : Int = cast (length lns) in Left (map (l -) errors)
-              else Right (unlines lns)
-  else Right str where
-    unlit' : String -> (LineType, List String, List Int) -> (LineType, List String, List Int)
-    unlit' str (type, ls, errs) with (lineType str)
-      unlit' str (Code, ls, errs) | (Text, _) = (Text, "" :: ls, cast (length ls) :: errs)
-      unlit' str (Text, ls, errs) | (Code, s) = (Code, (strCons ' ' s) :: ls, cast (length ls) :: errs)
-      unlit' str (type, ls, errs) | (Code, s) = (Code, (strCons ' ' s) :: ls, errs)
-      unlit' str (type, ls, errs) | (new, s) = (new, "" :: ls, errs)
+styleCMark : LiterateStyle
+styleCMark = MkLitStyle [("```idris", "```")] Nil [".md"]
 
+export
+isLitFile : String -> Maybe LiterateStyle
+isLitFile fname =
+    case isStyle styleBird of
+      Just s => Just s
+      Nothing => case isStyle styleOrg of
+                     Just s => Just s
+                     Nothing => isStyle styleCMark
+
+  where
+   hasSuffix : String -> Bool
+   hasSuffix ext = isSuffixOf ext fname
+
+   isStyle : LiterateStyle -> Maybe LiterateStyle
+   isStyle style =
+     if any hasSuffix (file_extensions style)
+      then Just style
+      else Nothing
+
+export
+isLitLine : String -> (Maybe String, String)
+isLitLine str =
+  case isLiterateLine styleBird str of
+     (Just l, s) => (Just l, s)
+     otherwise => case isLiterateLine styleOrg str of
+                    (Just l, s) => (Just l, s)
+                    otherwise => case isLiterateLine styleCMark str of
+                                   (Just l, s) => (Just l, s)
+                                   otherwise => (Nothing, str)
+
+export
+unlit : Maybe LiterateStyle -> String -> Either LiterateError String
+unlit Nothing  str = Right str
+unlit (Just s) str = unlit s str
+
+export
+relit : Maybe String -> String -> String
+relit Nothing     str = str
+relit (Just mark) str = unwords [mark, str]

src/TTImp/Elab/App.idr

@@ -612,7 +612,10 @@ checkApp rig elabinfo nest env fc (IImplicitApp fc' fn nm arg) expargs impargs e
 checkApp rig elabinfo nest env fc (IVar fc' n) expargs impargs exp
    = do (ntm, arglen, nty_in) <- getVarType rig nest env fc n
         nty <- getNF nty_in
-        elabinfo <- updateElabInfo (elabMode elabinfo) n expargs elabinfo
+        let prims = mapMaybe id
+                     [!fromIntegerName, !fromStringName, !fromCharName]
+        elabinfo <- updateElabInfo prims (elabMode elabinfo) n expargs elabinfo
+
         logC 10 (do defs <- get Ctxt
                     fnty <- quote defs env nty
                     exptyt <- maybe (pure Nothing)
@@ -628,24 +631,47 @@ checkApp rig elabinfo nest env fc (IVar fc' n) expargs impargs exp
         let fn = case lookup n (names nest) of
                       Just (Just n', _) => n'
                       _ => n
-        checkAppWith rig elabinfo nest env fc ntm nty (Just fn, arglen) expargs impargs False exp
+        normalisePrims prims env
+           !(checkAppWith rig elabinfo nest env fc ntm nty (Just fn, arglen) expargs impargs False exp)
   where
     isPrimName : List Name -> Name -> Bool
     isPrimName [] fn = False
     isPrimName (p :: ps) fn
         = dropNS fn == p || isPrimName ps fn
 
-    updateElabInfo : ElabMode -> Name -> List RawImp -> ElabInfo -> Core ElabInfo
+    boundSafe : Constant -> Bool
+    boundSafe (BI x) = abs x < 100 -- only do this for relatively small bounds.
+                           -- Once it gets too big, we might be making the term
+                           -- bigger than it would have been without evaluating!
+    boundSafe _ = True
+
+    -- If the term is an application of a primitive conversion (fromInteger etc)
+    -- and it's applied to a constant, fully normalise the term.
+    normalisePrims : List Name -> Env Term vs ->
+                     (Term vs, Glued vs) ->
+                     Core (Term vs, Glued vs)
+    normalisePrims prims env res
+        = if isPrimName prims !(getFullName n)
+             then case reverse expargs of
+                       (IPrimVal _ c :: _) =>
+                          if boundSafe c
+                             then do defs <- get Ctxt
+                                     tm <- normalise defs env (fst res)
+                                     pure (tm, snd res)
+                             else pure res
+                       _ => pure res
+             else pure res
+
+    updateElabInfo : List Name -> ElabMode -> Name ->
+                     List RawImp -> ElabInfo -> Core ElabInfo
     -- If it's a primitive function applied to a constant on the LHS, treat it
     -- as an expression because we'll normalise the function away and match on
     -- the result
-    updateElabInfo (InLHS _) n [IPrimVal fc c] elabinfo =
-        do let prims = mapMaybe id
-                          [!fromIntegerName, !fromStringName, !fromCharName]
-           if isPrimName prims !(getFullName n)
+    updateElabInfo prims (InLHS _) n [IPrimVal fc c] elabinfo =
+        do if isPrimName prims !(getFullName n)
               then pure (record { elabMode = InExpr } elabinfo)
               else pure elabinfo
-    updateElabInfo _ _ _ info = pure info
+    updateElabInfo _ _ _ _ info = pure info
 
 checkApp rig elabinfo nest env fc fn expargs impargs exp
    = do (fntm, fnty_in) <- checkImp rig elabinfo nest env fn Nothing

src/TTImp/Elab/Binders.idr

@@ -163,7 +163,7 @@ checkLambda rig_in elabinfo nest env fc rigl info n argTy scope (Just expty_in)
                              (gnf env
                                   (Bind fc n (Pi rigb info' tyv) !(getTerm scopet)))
                              (Just (gnf env
-                                       (Bind fc bn (Pi rigb info' pty) psc)))
+                                       (Bind fc bn (Pi c info' pty) psc)))
               _ => inferLambda rig elabinfo nest env fc rigl info n argTy scope (Just expty_in)
 
 weakenExp : Env Term (x :: vars) ->

src/TTImp/Elab/Case.idr

@@ -200,6 +200,13 @@ caseBlock {vars} rigc elabinfo fc nest env scr scrtm scrty caseRig alts expected
                                       [] casefnty Private None)
          let caseRef : Term vars = Ref fc Func (Resolved cidx)
 
+         -- If there's no duplication of the scrutinee in the block,
+         -- inline it.
+         -- This will be the case either if the scrutinee is a variable, in
+         -- which case the duplication won't hurt, or if (TODO) none of the
+         -- case patterns in alts are just a variable
+         maybe (pure ()) (const (setFlag fc casen Inline)) splitOn
+
          let applyEnv = applyToFull fc caseRef env
          let appTm : Term vars
                    = maybe (App fc applyEnv scrtm)

src/TTImp/ProcessDef.idr

@@ -79,7 +79,7 @@ impossibleErrOK defs (CantSolveEq fc env l r)
          impossibleOK defs !(nf defs env l)
                            !(nf defs env r)
 impossibleErrOK defs (BadDotPattern _ _ ErasedArg _ _) = pure True
-impossibleErrOK defs (CyclicMeta _ _) = pure True
+impossibleErrOK defs (CyclicMeta _ _ _ _) = pure True
 impossibleErrOK defs (AllFailed errs)
     = anyM (impossibleErrOK defs) (map snd errs)
 impossibleErrOK defs (WhenUnifying _ _ _ _ err)
@@ -239,10 +239,13 @@ checkLHS {vars} mult hashit n opts nest env fc lhs_in
          logTerm 5 "Checked LHS term" lhstm
          lhsty <- getTerm lhstyg
 
-         -- Normalise the LHS to get any functions or let bindings evaluated
-         -- (this might be allowed, e.g. for 'fromInteger')
          defs <- get Ctxt
-         lhstm <- normaliseLHS defs (letToLam env) lhstm
+         let lhsenv = letToLam env
+         -- we used to fully normalise the LHS, to make sure fromInteger
+         -- patterns were allowed, but now they're fully normalised anyway
+         -- so we only need to do the holes. If there's a lot of type level
+         -- computation, this is a huge saving!
+         lhstm <- normaliseHoles defs lhsenv lhstm
          lhsty <- normaliseHoles defs env lhsty
          linvars_in <- findLinear True 0 Rig1 lhstm
          logTerm 10 "Checked LHS term after normalise" lhstm
@@ -557,22 +560,28 @@ mkRunTime n
            let PMDef r cargs tree_ct _ pats = definition gdef
                 | _ => pure () -- not a function definition
            let ty = type gdef
+           pats' <- traverse (toErased (location gdef)) pats
+
            (rargs ** tree_rt) <- getPMDef (location gdef) RunTime n ty
-                                          !(traverse (toClause (location gdef)) pats)
+                                          (map (toClause (location gdef)) pats')
            log 5 $ "Runtime tree for " ++ show (fullname gdef) ++ ": " ++ show tree_rt
            let Just Refl = nameListEq cargs rargs
                    | Nothing => throw (InternalError "WAT")
-           addDef n (record { definition = PMDef r cargs tree_ct tree_rt pats
+           addDef n (record { definition = PMDef r cargs tree_ct tree_rt pats'
                             } gdef)
            pure ()
   where
-    toClause : FC -> (vars ** (Env Term vars, Term vars, Term vars)) ->
-               Core Clause
-    toClause fc (_ ** (env, lhs, rhs))
+    toErased : FC -> (vars ** (Env Term vars, Term vars, Term vars)) ->
+               Core (vars ** (Env Term vars, Term vars, Term vars))
+    toErased fc (_ ** (env, lhs, rhs))
         = do lhs_erased <- linearCheck fc Rig1 True env lhs
              rhs' <- applySpecialise env rhs
              rhs_erased <- linearCheck fc Rig1 True env rhs'
-             pure $ MkClause env lhs_erased rhs_erased
+             pure (_ ** (env, lhs_erased, rhs_erased))
+
+    toClause : FC -> (vars ** (Env Term vars, Term vars, Term vars)) -> Clause
+    toClause fc (_ ** (env, lhs, rhs))
+        = MkClause env lhs rhs
 
 compileRunTime : {auto c : Ref Ctxt Defs} ->
                  {auto m : Ref MD Metadata} ->
@@ -624,12 +633,14 @@ processDef opts nest env fc n_in cs_in
                   (record { definition = PMDef defaultPI cargs tree_ct tree_ct pats
                           } gdef)
 
-         let rmetas = getMetas tree_ct
-         traverse_ addToSave (keys rmetas)
-         let tymetas = getMetas (type gdef)
-         traverse_ addToSave (keys tymetas)
+         when (visibility gdef == Public) $
+             do let rmetas = getMetas tree_ct
+                log 10 $ "Saving from " ++ show n ++ ": " ++ show (keys rmetas)
+                traverse_ addToSave (keys rmetas)
+         when (isUserName n && visibility gdef /= Private) $
+             do let tymetas = getMetas (type gdef)
+                traverse_ addToSave (keys tymetas)
          addToSave n
-         log 10 $ "Saving from " ++ show n ++ ": " ++ show (keys rmetas)
 
          -- Flag this name as one which needs compiling
          defs <- get Ctxt

src/Text/Literate.idr

@@ -0,0 +1,211 @@
+||| A simple module to process 'literate' documents.
+|||
+||| The module uses a lexer to split the document into code blocks,
+||| delineated by user-defined markers, and code lines that are
+||| indicated be a line marker. The lexer returns a document stripped
+||| of non-code elements but preserving the original document's line
+||| count. Column numbering of code lines are not preserved.
+|||
+||| The underlying tokeniser is greedy.
+|||
+||| Once it identifies a line marker it reads a prettifying space then
+||| consumes until the end of line. Once identifies a starting code
+||| block marker, the lexer will consume input until the next
+||| identifiable end block is encountered. Any other content is
+||| treated as part of the original document.
+|||
+||| Thus, the input literate files *must* be well-formed w.r.t
+||| to code line markers and code blocks.
+|||
+||| A further restriction is that literate documents cannot contain
+||| the markers within the document's main text: This will confuse the
+||| lexer.
+|||
+module Text.Literate
+
+import Text.Lexer
+
+import Data.List.Views
+
+%default total
+
+untilEOL : Recognise False
+untilEOL = manyUntil (is '\n') any
+
+line : String -> Lexer
+line s = exact s <+> space <+> untilEOL
+
+block : String -> String -> Lexer
+block s e = surround (exact s <+> untilEOL) (exact e <+> untilEOL) any
+
+data Token = CodeBlock String String String
+           | Any String
+           | CodeLine String String
+
+Show Token where
+  showPrec d (CodeBlock l r x) = showCon d "CodeBlock" $ showArg l ++ showArg r ++ showArg x
+  showPrec d (Any x)           = showCon d "Any" $ showArg x
+  showPrec d (CodeLine m x)    = showCon d "CodeLine" $ showArg m ++ showArg x
+
+rawTokens : (delims  : List (String, String))
+         -> (markers : List String)
+         -> TokenMap (Token)
+rawTokens delims ls =
+          map (\(l,r) => (block l r, CodeBlock (trim l) (trim r))) delims
+       ++ map (\m => (line m, CodeLine (trim m))) ls
+       ++ [(any, Any)]
+
+||| Merge the tokens into a single source file.
+reduce : List (TokenData Token) -> String -> String
+reduce [] acc = acc
+reduce (MkToken _ _ (Any x) :: rest) acc = reduce rest (acc ++ blank_content)
+  where
+    -- Preserve the original document's line count.
+    blank_content : String
+    blank_content = if elem '\n' (unpack x)
+      then concat $ replicate (length (lines x)) "\n"
+      else ""
+reduce (MkToken _ _ (CodeLine m src) :: rest) acc =
+    reduce rest (acc ++ (substr
+                           (length m + 1) -- remove space to right of marker.
+                           (length src)
+                           src))
+
+reduce (MkToken _ _ (CodeBlock l r src) :: rest) acc with (lines src) -- Strip the deliminators surrounding the block.
+  reduce (MkToken _ _ (CodeBlock l r src) :: rest) acc | [] = reduce rest acc -- 1
+  reduce (MkToken _ _ (CodeBlock l r src) :: rest) acc | (s :: ys) with (snocList ys)
+    reduce (MkToken _ _ (CodeBlock l r src) :: rest) acc | (s :: []) | Empty = reduce rest acc -- 2
+    reduce (MkToken _ _ (CodeBlock l r src) :: rest) acc | (s :: (srcs ++ [f])) | (Snoc rec) =
+        reduce rest (acc ++ "\n" ++ unlines srcs)
+
+-- [ NOTE ] 1 & 2 shouldn't happen as code blocks are well formed i.e. have two deliminators.
+
+
+public export
+record LiterateError where
+  constructor MkLitErr
+  line   : Int
+  column : Int
+  input  : String
+
+||| Description of literate styles.
+|||
+||| A 'literate' style comprises of
+|||
+||| + a list of code block deliminators (`deliminators`);
+||| + a list of code line markers (`line_markers`); and
+||| + a list of known file extensions `file_extensions`.
+|||
+||| Some example specifications:
+|||
+||| + Bird Style
+|||
+|||```
+|||MkLitStyle Nil [">"] [".lidr"]
+|||```
+|||
+||| + Literate Haskell (for LaTeX)
+|||
+|||```
+|||MkLitStyle [("\\begin{code}", "\\end{code}"),("\\begin{spec}","\\end{spec}")]
+|||           Nil
+|||           [".lhs", ".tex"]
+|||```
+|||
+||| + OrgMode
+|||
+|||```
+|||MkLitStyle [("#+BEGIN_SRC idris","#+END_SRC"), ("#+COMMENT idris","#+END_COMMENT")]
+|||           ["#+IDRIS:"]
+|||           [".org"]
+|||```
+|||
+||| + Common Mark
+|||
+|||```
+|||MkLitStyle [("```idris","```"), ("<!-- idris","--!>")]
+|||           Nil
+|||           [".md", ".markdown"]
+|||```
+|||
+public export
+record LiterateStyle where
+  constructor MkLitStyle
+  ||| The pairs of start and end tags for code blocks.
+  deliminators : List (String, String)
+
+  ||| Line markers that indicate a line contains code.
+  line_markers : List String
+
+  ||| Recognised file extensions. Not used by the module, but will be
+  ||| of use when connecting to code that reads in the original source
+  ||| files.
+  file_extensions : List String
+
+||| Given a 'literate specification' extract the code from the
+||| literate source file (`litStr`) that follows the presented style.
+|||
+||| @specification The literate specification to use.
+||| @litStr  The literate source file.
+|||
+||| Returns a `LiterateError` if the literate file contains malformed
+||| code blocks or code lines.
+|||
+export
+extractCode : (specification : LiterateStyle)
+           -> (litStr        : String)
+           -> Either LiterateError String
+extractCode (MkLitStyle delims markers exts) str =
+      case lex (rawTokens delims markers) str of
+        (toks, (_,_,"")) => Right $ reduce toks ""
+        (_, (l,c,i))     => Left (MkLitErr l c i)
+
+||| Synonym for `extractCode`.
+export
+unlit : (specification : LiterateStyle)
+     -> (litStr        : String)
+     -> Either LiterateError String
+unlit = extractCode
+
+||| Is the provided line marked up using a line marker?
+|||
+||| If the line is suffixed by any one of the style's set of line
+||| markers then return length of literate line marker, and the code stripped from the line
+||| marker. Otherwise, return Nothing and the unmarked line.
+export
+isLiterateLine : (specification : LiterateStyle)
+              -> (str : String)
+              -> Pair (Maybe String) String
+isLiterateLine (MkLitStyle delims markers _) str with (lex (rawTokens delims markers) str)
+  isLiterateLine (MkLitStyle delims markers _) str | ([MkToken _ _ (CodeLine m str')], (_,_, "")) = (Just m, str')
+  isLiterateLine (MkLitStyle delims markers _) str | (_, _) = (Nothing, str)
+
+||| Given a 'literate specification' embed the given code using the
+||| literate style provided.
+|||
+||| If the style uses deliminators to denote code blocks use the first
+||| pair of deliminators in the style. Otherwise use first linemarker
+||| in the style. If there is **no style** return the presented code
+||| string unembedded.
+|||
+|||
+||| @specification The literate specification to use.
+||| @code  The code to embed,
+|||
+|||
+export
+embedCode : (specification : LiterateStyle)
+         -> (code : String)
+         -> String
+embedCode (MkLitStyle ((s,e)::delims) _            _) str = unlines [s,str,e]
+embedCode (MkLitStyle Nil             (m::markers) _) str = unwords [m, str]
+embedCode (MkLitStyle _               _            _) str = str
+
+||| Synonm for `embedCode`
+export
+relit : (specification : LiterateStyle)
+     -> (code : String)
+     -> String
+relit = embedCode
+
+-- --------------------------------------------------------------------- [ EOF ]

src/Yaffle/REPL.idr

@@ -151,12 +151,10 @@ repl : {auto c : Ref Ctxt Defs} ->
 repl
     = do coreLift (putStr "Yaffle> ")
          inp <- coreLift getLine
-         case runParser False False inp command of
+         case runParser Nothing inp command of
               Left err => do coreLift (printLn err)
                              repl
               Right cmd =>
                   do if !(processCatch cmd)
                         then repl
                         else pure ()
-
-

tests/Main.idr

@@ -50,7 +50,7 @@ idrisTests
        -- Literate
        "literate001", "literate002", "literate003", "literate004",
        "literate005", "literate006", "literate007", "literate008",
-       "literate009",
+       "literate009", "literate010", "literate011", "literate012",
        -- Interfaces
        "interface001", "interface002", "interface003", "interface004",
        "interface005", "interface006", "interface007", "interface008",
@@ -81,7 +81,7 @@ idrisTests
        -- Miscellaneous regressions
        "reg001", "reg002", "reg003", "reg004", "reg005", "reg006", "reg007",
        "reg008", "reg009", "reg010", "reg011", "reg012", "reg013", "reg014",
-       "reg015", "reg016",
+       "reg015", "reg016", "reg017",
        -- Totality checking
        "total001", "total002", "total003", "total004", "total005",
        "total006",

tests/ideMode/ideMode001/expected

@@ -2,13 +2,13 @@
 000038(:write-string "1/1: Building LocType (LocType.idr)" 1)
 0000ca(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 23) (:end 7 25)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "a")))))) 1)
 0000d8(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 38) (:end 8 1)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect m a)")))))) 1)
-0000df(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 35) (:end 7 38)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect {k:190} a)")))))) 1)
-0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 9) (:end 7 11)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "?{_:191}_[]")))))) 1)
-0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 14) (:end 7 16)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{k:190}_[] ?{_:191}_[])")))))) 1)
-0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 18) (:end 7 21)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:192}_[] ?{_:191}_[])")))))) 1)
+0000df(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 35) (:end 7 38)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect {k:221} a)")))))) 1)
+0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 9) (:end 7 11)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "?{_:222}_[]")))))) 1)
+0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 14) (:end 7 16)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{k:221}_[] ?{_:222}_[])")))))) 1)
+0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 18) (:end 7 21)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:223}_[] ?{_:222}_[])")))))) 1)
 0000d8(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 16) (:end 7 1)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect m a)")))))) 1)
-0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 11) (:end 6 14)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:182}_[] ?{_:181}_[])")))))) 1)
-0001ca(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 1) (:end 6 1)) ((:name "Main.append") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "{0 m : Prelude.Nat} -> {0 a : Type} -> {0 n : Prelude.Nat} -> (({arg:172} : (Main.Vect n[0] a[1])) -> (({arg:173} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.+ Prelude.Nat Prelude.Num implementation at Prelude.idr:735:1--742:1 n[2] m[4]) a[3])))")))))) 1)
+0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 11) (:end 6 14)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:212}_[] ?{_:211}_[])")))))) 1)
+0001ca(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 1) (:end 6 1)) ((:name "Main.append") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "{0 m : Prelude.Nat} -> {0 a : Type} -> {0 n : Prelude.Nat} -> (({arg:202} : (Main.Vect n[0] a[1])) -> (({arg:203} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.+ Prelude.Nat Prelude.Num implementation at Prelude.idr:631:1--638:1 n[2] m[4]) a[3])))")))))) 1)
 0000cb(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 47) (:end 6 1)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
 0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 44) (:end 5 45)) ((:name "m") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)
 0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 40) (:end 5 42)) ((:name "n") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)

tests/ideMode/ideMode003/expected

@@ -2,13 +2,13 @@
 000038(:write-string "1/1: Building LocType (LocType.idr)" 1)
 0000ca(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 23) (:end 7 25)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "a")))))) 1)
 0000d8(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 38) (:end 8 1)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect m a)")))))) 1)
-0000df(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 35) (:end 7 38)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect {k:190} a)")))))) 1)
-0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 9) (:end 7 11)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "?{_:191}_[]")))))) 1)
-0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 14) (:end 7 16)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{k:190}_[] ?{_:191}_[])")))))) 1)
-0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 18) (:end 7 21)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:192}_[] ?{_:191}_[])")))))) 1)
+0000df(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 35) (:end 7 38)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect {k:221} a)")))))) 1)
+0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 9) (:end 7 11)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "?{_:222}_[]")))))) 1)
+0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 14) (:end 7 16)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{k:221}_[] ?{_:222}_[])")))))) 1)
+0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 18) (:end 7 21)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:223}_[] ?{_:222}_[])")))))) 1)
 0000d8(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 16) (:end 7 1)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect m a)")))))) 1)
-0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 11) (:end 6 14)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:182}_[] ?{_:181}_[])")))))) 1)
-0001ca(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 1) (:end 6 1)) ((:name "Main.append") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "{0 m : Prelude.Nat} -> {0 a : Type} -> {0 n : Prelude.Nat} -> (({arg:172} : (Main.Vect n[0] a[1])) -> (({arg:173} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.+ Prelude.Nat Prelude.Num implementation at Prelude.idr:735:1--742:1 n[2] m[4]) a[3])))")))))) 1)
+0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 11) (:end 6 14)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:212}_[] ?{_:211}_[])")))))) 1)
+0001ca(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 1) (:end 6 1)) ((:name "Main.append") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "{0 m : Prelude.Nat} -> {0 a : Type} -> {0 n : Prelude.Nat} -> (({arg:202} : (Main.Vect n[0] a[1])) -> (({arg:203} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.+ Prelude.Nat Prelude.Num implementation at Prelude.idr:631:1--638:1 n[2] m[4]) a[3])))")))))) 1)
 0000cb(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 47) (:end 6 1)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
 0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 44) (:end 5 45)) ((:name "m") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)
 0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 40) (:end 5 42)) ((:name "n") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)

tests/idris2/basic018/expected

@@ -1,3 +1,3 @@
 1/1: Building Fin (Fin.idr)
 Fin.idr:33:7--35:1:While processing right hand side of bar at Fin.idr:33:1--35:1:
-Can't find an implementation for IsJust (integerToFin 8 (S (assert_total (integerToNat (prim__sub_Integer 5 (fromInteger 1))))))
+Can't find an implementation for IsJust (integerToFin 8 5)

tests/idris2/basic030/expected

@@ -1,7 +1,7 @@
 1/1: Building arity (arity.idr)
 arity.idr:4:16--4:22:While processing right hand side of foo at arity.idr:4:1--7:1:
-When unifying (1 {arg:169} : Nat) -> MyN and MyN
+When unifying (1 {arg:199} : Nat) -> MyN and MyN
 Mismatch between:
-	(1 {arg:169} : Nat) -> MyN
+	(1 {arg:199} : Nat) -> MyN
 and
 	MyN

tests/idris2/basic036/expected

@@ -1,5 +1,5 @@
 1/1: Building defimp (defimp.idr)
-Main> Main.dvec : (n : Nat) -> {default (replicate n (fromInteger 1)) xs : Vect n Nat} -> Nat
+Main> Main.dvec : (n : Nat) -> {default (replicate n 1) xs : Vect n Nat} -> Nat
 Main> 3
 Main> 6
 Main> Bye for now!

tests/idris2/literate001/IEdit.lidr

@@ -16,4 +16,3 @@
 
 > suc' : x = y -> S x = S y
 > suc' {x} {y} prf = ?quuz
-

tests/idris2/literate007/IEdit.lidr

@@ -8,4 +8,3 @@
 > dupAll xs = zipHere xs xs
 >   where
 >     zipHere : forall n . Vect n a -> Vect n b -> Vect n (a, b)
-

tests/idris2/literate007/IEdit.org

@@ -0,0 +1,12 @@
+#+begin_src idris
+data Vect : Nat -> Type -> Type where
+     Nil : Vect Z a
+     (::) : a -> Vect k a -> Vect (S k) a
+#+end_src
+
+#+IDRIS: %name Vect xs, ys, zs
+
+#+IDRIS: dupAll : Vect n a -> Vect n (a, a)
+#+IDRIS: dupAll xs = zipHere xs xs
+#+IDRIS:   where
+#+IDRIS:     zipHere : forall n . Vect n a -> Vect n b -> Vect n (a, b)

tests/idris2/literate007/IEditOrg.org

@@ -0,0 +1,12 @@
+#+begin_src idris
+data Vect : Nat -> Type -> Type where
+     Nil : Vect Z a
+     (::) : a -> Vect k a -> Vect (S k) a
+#+end_src
+
+#+IDRIS: %name Vect xs, ys, zs
+
+#+IDRIS: dupAll : Vect n a -> Vect n (a, a)
+#+IDRIS: dupAll xs = zipHere xs xs
+#+IDRIS:   where
+#+IDRIS:     zipHere : forall n . Vect n a -> Vect n b -> Vect n (a, b)

tests/idris2/literate007/expected

@@ -2,3 +2,7 @@
 Main> >     zipHere [] ys = []
 >     zipHere (x :: xs) (y :: ys) = (x, y) :: zipHere xs ys
 Main> Bye for now!
+1/1: Building IEditOrg (IEditOrg.org)
+Main> #+IDRIS:     zipHere [] ys = []
+#+IDRIS:     zipHere (x :: xs) (y :: ys) = (x, y) :: zipHere xs ys
+Main> Bye for now!

tests/idris2/literate007/input2

@@ -0,0 +1,2 @@
+:gd 12 zipHere
+:q

tests/idris2/literate007/run

@@ -1,3 +1,4 @@
 $1 --no-banner IEdit.lidr < input
+$1 --no-banner IEditOrg.org < input2
 
 rm -rf build

tests/idris2/literate010/MyFirstIdrisProgram.org

@@ -0,0 +1,44 @@
+#+TITLE: My First Idris2 Program
+
+This is a literate Idris2 Org-Mode file that the Idris2 understands.
+
+We can have visibile code blocks using source blocks in idris.
+
+#+BEGIN_SRC idris
+data Natural = Zero | Succ Natural
+#+END_SRC
+
+#+BEGIN_SRC idris
+data Vect : Natural -> Type -> Type where
+  Empty : Vect Zero a
+  Cons  : a -> Vect k a -> Vect (Succ k) a
+#+END_SRC
+
+We can have hidden literate lines that Idris will understand.
+
+#+IDRIS: %name Vect xs, ys
+
+However, we Idris2' literate support is greedy and does not understand all of the supported literate modes comments and verbatim blocks.
+
+Thus:
+
+#+begin_example
+
+#+IDRIS: plus : Natural -> Natural -> Natural
+
+#+end_example
+
+is also an active code line.
+
+We can also abuse org-mode comments to hide code not required for publication.
+
+#+begin_comment idris
+
+cannotSeeThis : Natural -> Natural
+
+#+end_comment
+
+#+BEGIN_SRC idris
+main : IO ()
+main = putStrLn "Hello!"
+#+END_SRC

tests/idris2/literate010/expected

@@ -0,0 +1 @@
+1/1: Building MyFirstIdrisProgram (MyFirstIdrisProgram.org)

tests/idris2/literate010/run

@@ -0,0 +1,3 @@
+$1 --check --no-banner MyFirstIdrisProgram.org
+
+rm -rf build

tests/idris2/literate011/IEdit.md

@@ -0,0 +1,16 @@
+```idris
+data Vect : Nat -> Type -> Type where
+     Nil : Vect Z a
+     (::) : a -> Vect k a -> Vect (S k) a
+```
+
+```idris
+%name Vect xs, ys, zs
+```
+
+```idris
+dupAll : Vect n a -> Vect n (a, a)
+dupAll xs = zipHere xs xs
+  where
+    zipHere : forall n . Vect n a -> Vect n b -> Vect n (a, b)
+```

tests/idris2/literate011/expected

@@ -0,0 +1,4 @@
+1/1: Building IEdit (IEdit.md)
+Main>     zipHere [] ys = []
+    zipHere (x :: xs) (y :: ys) = (x, y) :: zipHere xs ys
+Main> Bye for now!

tests/idris2/literate011/input

@@ -0,0 +1,2 @@
+:gd 15 zipHere
+:q

tests/idris2/literate011/run

@@ -0,0 +1,3 @@
+$1 --no-banner IEdit.md < input
+
+rm -rf build

tests/idris2/literate012/IEdit.org

@@ -0,0 +1,30 @@
+#+TITLE: Interactive Editing Working
+
+#+begin_src idris
+data Vect : Nat -> Type -> Type where
+     Nil : Vect Z a
+     (::) : a -> Vect k a -> Vect (S k) a
+#+end_src
+
+#+IDRIS: %name Vect xs, ys, zs
+
+#+begin_src idris
+append : Vect n a -> Vect m a -> Vect (n + m) a
+append {n} xs ys = ?foo
+#+end_src
+
+#+begin_src idris
+vadd : Num a => Vect n a -> Vect n a -> Vect n a
+vadd [] ys = ?bar
+vadd (x :: xs) ys = ?baz
+#+end_src
+
+#+begin_src idris
+suc : (x : Nat) -> (y : Nat) -> x = y -> S x = S y
+suc x y prf = ?quux
+#+end_src
+
+#+begin_src idris
+suc' : x = y -> S x = S y
+suc' {x} {y} prf = ?quuz
+#+end_src

tests/idris2/literate012/IEdit2.org

@@ -0,0 +1,31 @@
+#+TITLE: Interactive Editing Working
+
+#+begin_src idris
+data Vect : Nat -> Type -> Type where
+     Nil : Vect Z a
+     (::) : a -> Vect k a -> Vect (S k) a
+#+end_src
+
+#+IDRIS: %name Vect xs, ys, zs
+
+#+begin_src idris
+append : Vect n a -> Vect m a -> Vect (n + m) a
+append {n = Z} [] ys = ?foo_1
+append {n = (S k)} (x :: xs) ys = ?foo_2
+#+end_src
+
+#+begin_src idris
+vadd : Num a => Vect n a -> Vect n a -> Vect n a
+vadd [] [] = ?bar_1
+vadd (x :: xs) (y :: ys) = ?baz_1
+#+end_src
+
+#+begin_src idris
+suc : (x : Nat) -> (y : Nat) -> x = y -> S x = S y
+suc x x Refl = ?quux_1
+#+end_src
+
+#+begin_src idris
+suc' : x = y -> S x = S y
+suc' {x = y} {y = y} Refl = ?quuz_1
+#+end_src

tests/idris2/literate012/expected

@@ -0,0 +1,8 @@
+1/1: Building IEdit (IEdit.org)
+Main> append {n = 0} [] ys = ?foo_1
+append {n = (S k)} (x :: xs) ys = ?foo_2
+Main> vadd [] [] = ?bar_1
+Main> vadd (x :: xs) (y :: ys) = ?baz_1
+Main> suc x x Refl = ?quux_1
+Main> suc' {x = y} {y = y} Refl = ?quuz_1
+Main> Bye for now!

tests/idris2/literate012/input

@@ -0,0 +1,6 @@
+:cs 13 11 xs
+:cs 18 8 ys
+:cs 19 15 ys
+:cs 24 8 prf
+:cs 29 13 prf
+:q

tests/idris2/literate012/run

@@ -0,0 +1,3 @@
+$1 --no-banner IEdit.org < input
+
+rm -rf build

tests/idris2/reg007/expected

@@ -1,7 +1,7 @@
 1/1: Building Main (Main.idr)
 Main.idr:27:26--27:72:While processing right hand side of dpairWithExtraInfoBad at Main.idr:27:1--28:1:
-When unifying [MN (fromInteger 0), MN (fromInteger 0)] and [MN (fromInteger 0)]
+When unifying [MN 0, MN 0] and [MN 0]
 Mismatch between:
-	[MN (fromInteger 0)]
+	[MN 0]
 and
 	[]

tests/idris2/reg017/expected

@@ -0,0 +1,7 @@
+1/1: Building lammult (lammult.idr)
+lammult.idr:2:15--2:24:While processing right hand side of badmap at lammult.idr:2:1--3:1:
+When unifying (0 x : ?a) -> ?b and ?a -> ?b
+Mismatch between:
+	(0 x : ?a) -> ?b
+and
+	?a -> ?b

tests/idris2/reg017/lammult.idr

@@ -0,0 +1,2 @@
+badmap : List Int -> List Int
+badmap = map (\0 x => 2)

tests/idris2/reg017/run

@@ -0,0 +1,3 @@
+$1 lammult.idr --check
+
+rm -rf build

tests/ttimp/basic003/expected

@@ -1,8 +1,8 @@
 Processing as TTImp
 Written TTC
-Yaffle> Main.foo : (%pi Rig0 Explicit Just m Main.Nat (%pi Rig0 Explicit Just a %type (%pi Rig0 Explicit Just {k:25} Main.Nat (%pi RigW Explicit Nothing a (%pi RigW Explicit Nothing ((Main.Vect {k:25}) a) (%pi RigW Explicit Nothing ((Main.Vect m) a) (%pi Rig0 Explicit Just n Main.Nat ((Main.Vect ((Main.plus {k:25}) m)) a))))))))
+Yaffle> Main.foo : (%pi Rig0 Explicit Just m Main.Nat (%pi Rig0 Explicit Just a %type (%pi Rig0 Explicit Just {k:26} Main.Nat (%pi RigW Explicit Nothing a (%pi RigW Explicit Nothing ((Main.Vect {k:26}) a) (%pi RigW Explicit Nothing ((Main.Vect m) a) (%pi Rig0 Explicit Just n Main.Nat ((Main.Vect ((Main.plus {k:26}) m)) a))))))))
 Yaffle> Bye for now!
 Processing as TTC
 Read TTC
-Yaffle> Main.foo : (%pi Rig0 Explicit Just m Main.Nat (%pi Rig0 Explicit Just a %type (%pi Rig0 Explicit Just {k:25} Main.Nat (%pi RigW Explicit Nothing a (%pi RigW Explicit Nothing ((Main.Vect {k:25}) a) (%pi RigW Explicit Nothing ((Main.Vect m) a) (%pi Rig0 Explicit Just n Main.Nat ((Main.Vect ((Main.plus {k:25}) m)) a))))))))
+Yaffle> Main.foo : (%pi Rig0 Explicit Just m Main.Nat (%pi Rig0 Explicit Just a %type (%pi Rig0 Explicit Just {k:26} Main.Nat (%pi RigW Explicit Nothing a (%pi RigW Explicit Nothing ((Main.Vect {k:26}) a) (%pi RigW Explicit Nothing ((Main.Vect m) a) (%pi Rig0 Explicit Just n Main.Nat ((Main.Vect ((Main.plus {k:26}) m)) a))))))))
 Yaffle> Bye for now!

tests/ttimp/basic006/expected

@@ -2,5 +2,5 @@ Processing as TTImp
 Written TTC
 Yaffle> ((Main.Just [Just a = ((Main.Vect.Vect (Main.S Main.Z)) Integer)]) ((((Main.Vect.Cons [Just k = Main.Z]) [Just a = Integer]) 1) (Main.Vect.Nil [Just a = Integer])))
 Yaffle> ((Main.MkInfer [Just a = (Main.List.List Integer)]) (((Main.List.Cons [Just a = Integer]) 1) (Main.List.Nil [Just a = Integer])))
-Yaffle> (repl):1:9--1:12:Ambiguous elaboration [($resolved117 ?Main.{a:59}_[]), ($resolved98 ?Main.{a:59}_[])]
+Yaffle> (repl):1:9--1:12:Ambiguous elaboration [($resolved119 ?Main.{a:62}_[]), ($resolved99 ?Main.{a:62}_[])]
 Yaffle> Bye for now!

tests/ttimp/coverage002/expected

@@ -2,6 +2,6 @@ Processing as TTImp
 Written TTC
 Yaffle> Main.lookup: All cases covered
 Yaffle> Main.lookup':
-($resolved144 [__] [__] (Main.FZ [__]) {arg:3})
+($resolved146 [__] [__] (Main.FZ [__]) {arg:3})
 Yaffle> Main.lookup'': Calls non covering function Main.lookup'
 Yaffle> Bye for now!

tests/ttimp/eta001/expected

@@ -1,5 +1,5 @@
 Processing as TTImp
 Written TTC
-Yaffle> ((Main.Refl [Just {b:9} = Main.Nat]) [Just x = (Main.S (Main.S (Main.S (Main.S Main.Z))))])
+Yaffle> ((Main.Refl [Just {b:10} = Main.Nat]) [Just x = (Main.S (Main.S (Main.S (Main.S Main.Z))))])
 Yaffle> Main.etaGood1 : ((((Main.Eq [Just b = (%pi RigW Explicit Nothing Integer (%pi RigW Explicit Nothing Integer Main.Test))]) [Just a = (%pi RigW Explicit Nothing Integer (%pi RigW Explicit Nothing Integer Main.Test))]) Main.MkTest) (%lam RigW Explicit Just x Integer (%lam RigW Explicit Just y Integer ((Main.MkTest x) y))))
 Yaffle> Bye for now!

tests/ttimp/eta002/expected

@@ -1,5 +1,5 @@
 Processing as TTImp
 Eta.yaff:16:1--17:1:When elaborating right hand side of Main.etaBad:
-Eta.yaff:16:10--17:1:When unifying: ($resolved98 ((x : Char) -> ((y : ?Main.{_:14}_[x[0]]) -> $resolved106)) ((x : Char) -> ((y : ?Main.{_:14}_[x[0]]) -> $resolved106)) ?Main.{x:18}_[] ?Main.{x:18}_[]) and ($resolved98 ((x : Char) -> ((y : ?Main.{_:14}_[x[0]]) -> $resolved106)) (({arg:10} : Integer) -> (({arg:11} : Integer) -> $resolved106)) $resolved107 \x : Char => \y : ?Main.{_:14}_[x[0]] => ($resolved107 ?Main.{_:15}_[x[1], y[0]] ?Main.{_:16}_[x[1], y[0]]))
+Eta.yaff:16:10--17:1:When unifying: ($resolved98 ((x : Char) -> ((y : ?Main.{_:15}_[x[0]]) -> $resolved107)) ((x : Char) -> ((y : ?Main.{_:15}_[x[0]]) -> $resolved107)) ?Main.{x:19}_[] ?Main.{x:19}_[]) and ($resolved98 ((x : Char) -> ((y : ?Main.{_:15}_[x[0]]) -> $resolved107)) (({arg:11} : Integer) -> (({arg:12} : Integer) -> $resolved107)) $resolved108 \x : Char => \y : ?Main.{_:15}_[x[0]] => ($resolved108 ?Main.{_:16}_[x[1], y[0]] ?Main.{_:17}_[x[1], y[0]]))
 	Eta.yaff:16:10--17:1:Type mismatch: Char and Integer
 Yaffle> Bye for now!

tests/ttimp/qtt002/expected

@@ -1,6 +1,6 @@
 Processing as TTImp
 Written TTC
-Yaffle> Main.foo : (%pi Rig0 Explicit Just m Main.Nat (%pi Rig0 Explicit Just a %type (%pi Rig0 Explicit Just {k:19} Main.Nat (%pi RigW Explicit Nothing a (%pi Rig0 Explicit Just y a (%pi Rig0 Explicit Just ws ((Main.Vect {k:19}) a) (%pi Rig1 Explicit Just zs ((Main.Vect (Main.S {k:19})) a) (%pi RigW Explicit Nothing ((Main.Vect m) a) (%pi Rig0 Explicit Just n Main.Nat ((Main.Vect ((Main.plus (Main.S (Main.S {k:19}))) m)) a))))))))))
-Yaffle> Main.bar : (%pi Rig0 Explicit Just m Main.Nat (%pi Rig0 Explicit Just a %type (%pi RigW Explicit Nothing ((Main.Vect m) a) (%pi Rig0 Explicit Just {k:49} Main.Nat (%pi RigW Explicit Nothing a (%pi Rig1 Explicit Just zs ((Main.Vect {k:49}) a) (%pi Rig0 Explicit Just xs ((Main.Vect (Main.S {k:49})) a) (%pi Rig0 Explicit Just n Main.Nat ((Main.Vect ((Main.plus (Main.S {k:49})) m)) a)))))))))
-Yaffle> Main.baz : (%pi Rig0 Explicit Just m Main.Nat (%pi Rig0 Explicit Just a %type (%pi RigW Explicit Nothing ((Main.Vect m) a) (%pi Rig0 Explicit Just {k:80} Main.Nat (%pi RigW Explicit Nothing a (%pi Rig0 Explicit Just zs ((Main.Vect {k:80}) a) (%pi Rig0 Explicit Just xs ((Main.Vect (Main.S {k:80})) a) (%pi Rig0 Explicit Just n Main.Nat (%pi Rig1 Explicit Just ts ((Main.Vect {k:80}) a) ((Main.Vect ((Main.plus (Main.S {k:80})) m)) a))))))))))
+Yaffle> Main.foo : (%pi Rig0 Explicit Just m Main.Nat (%pi Rig0 Explicit Just a %type (%pi Rig0 Explicit Just {k:21} Main.Nat (%pi RigW Explicit Nothing a (%pi Rig0 Explicit Just y a (%pi Rig0 Explicit Just ws ((Main.Vect {k:21}) a) (%pi Rig1 Explicit Just zs ((Main.Vect (Main.S {k:21})) a) (%pi RigW Explicit Nothing ((Main.Vect m) a) (%pi Rig0 Explicit Just n Main.Nat ((Main.Vect ((Main.plus (Main.S (Main.S {k:21}))) m)) a))))))))))
+Yaffle> Main.bar : (%pi Rig0 Explicit Just m Main.Nat (%pi Rig0 Explicit Just a %type (%pi RigW Explicit Nothing ((Main.Vect m) a) (%pi Rig0 Explicit Just {k:52} Main.Nat (%pi RigW Explicit Nothing a (%pi Rig1 Explicit Just zs ((Main.Vect {k:52}) a) (%pi Rig0 Explicit Just xs ((Main.Vect (Main.S {k:52})) a) (%pi Rig0 Explicit Just n Main.Nat ((Main.Vect ((Main.plus (Main.S {k:52})) m)) a)))))))))
+Yaffle> Main.baz : (%pi Rig0 Explicit Just m Main.Nat (%pi Rig0 Explicit Just a %type (%pi RigW Explicit Nothing ((Main.Vect m) a) (%pi Rig0 Explicit Just {k:84} Main.Nat (%pi RigW Explicit Nothing a (%pi Rig0 Explicit Just zs ((Main.Vect {k:84}) a) (%pi Rig0 Explicit Just xs ((Main.Vect (Main.S {k:84})) a) (%pi Rig0 Explicit Just n Main.Nat (%pi Rig1 Explicit Just ts ((Main.Vect {k:84}) a) ((Main.Vect ((Main.plus (Main.S {k:84})) m)) a))))))))))
 Yaffle> Bye for now!

tests/ttimp/search001/expected

@@ -1,6 +1,6 @@
 Processing as TTImp
 Written TTC
-Yaffle> (((((Main.There [Just {a:15} = Main.Nat]) [Just y = (Main.S Main.Z)]) [Just xs = (((Main.Cons [Just a = Main.Nat]) Main.Z) (Main.Nil [Just a = Main.Nat]))]) [Just x = Main.Z]) (((Main.Here [Just {a:9} = Main.Nat]) [Just xs = (Main.Nil [Just a = Main.Nat])]) [Just x = Main.Z]))
-Yaffle> (((Main.Here [Just {a:9} = Main.Nat]) [Just xs = (((Main.Cons [Just a = Main.Nat]) Main.Z) (Main.Nil [Just a = Main.Nat]))]) [Just x = (Main.S Main.Z)])
+Yaffle> (((((Main.There [Just {a:19} = Main.Nat]) [Just y = (Main.S Main.Z)]) [Just xs = (((Main.Cons [Just a = Main.Nat]) Main.Z) (Main.Nil [Just a = Main.Nat]))]) [Just x = Main.Z]) (((Main.Here [Just {a:11} = Main.Nat]) [Just xs = (Main.Nil [Just a = Main.Nat])]) [Just x = Main.Z]))
+Yaffle> (((Main.Here [Just {a:11} = Main.Nat]) [Just xs = (((Main.Cons [Just a = Main.Nat]) Main.Z) (Main.Nil [Just a = Main.Nat]))]) [Just x = (Main.S Main.Z)])
 Yaffle> ((((Main.MkPair [Just b = Integer]) [Just a = String]) "b") 94)
 Yaffle> Bye for now!

tests/ttimp/search005/expected

@@ -1,8 +1,8 @@
 Processing as TTImp
 Written TTC
 Yaffle> \0 m : Main.Nat => \0 a : Type => \ys : (Main.Vect m[1] a[0]) => \0 n : Main.Nat => ys[1]
-Yaffle> \0 m : Main.Nat => \0 a : Type => \0 {k:29} : Main.Nat => \x : a[1] => \xs : (Main.Vect {k:29}[1] a[2]) => \ys : (Main.Vect m[4] a[3]) => \0 n : Main.Nat => (Main.Cons (Main.plus {k:29}[4] m[6]) a[5] x[3] (Main.append m[6] a[5] {k:29}[4] xs[2] ys[1]))
-Yaffle> [((Main.app2 (Main.Nil [Just a = _])) $y) = y, ((Main.app2 ((((Main.Cons [Just k = _]) [Just a = _]) $x) $z)) $y) = ((((Main.Cons [Just k = ((Main.plus {_:201}) m)]) [Just a = a]) x) (((((Main.app2 [Just m = m]) [Just a = a]) [Just n = {_:201}]) z) y))]
-Yaffle> [((Main.zip (Main.Nil [Just a = _])) $y) = (Main.Nil [Just a = ((Main.Pair a) b)]), ((Main.zip ((((Main.Cons [Just k = _]) [Just a = _]) $x) $z)) ((((Main.Cons [Just k = _]) [Just a = _]) $y) $w)) = ((((Main.Cons [Just k = {_:314}]) [Just a = ((Main.Pair a) b)]) ((((Main.MkPair [Just b = b]) [Just a = a]) x) y)) (((((Main.zip [Just b = b]) [Just a = a]) [Just n = {_:314}]) z) w))]
-Yaffle> [(((Main.zipWith $f) (Main.Nil [Just a = _])) $y) = (Main.Nil [Just a = c]), (((Main.zipWith $f) ((((Main.Cons [Just k = _]) [Just a = _]) $x) $z)) ((((Main.Cons [Just k = _]) [Just a = _]) $y) $w)) = ((((Main.Cons [Just k = {_:464}]) [Just a = c]) ((f x) y)) (((((((Main.zipWith [Just n = {_:464}]) [Just c = c]) [Just b = b]) [Just a = a]) f) z) w))]
+Yaffle> \0 m : Main.Nat => \0 a : Type => \0 {k:30} : Main.Nat => \x : a[1] => \xs : (Main.Vect {k:30}[1] a[2]) => \ys : (Main.Vect m[4] a[3]) => \0 n : Main.Nat => (Main.Cons (Main.plus {k:30}[4] m[6]) a[5] x[3] (Main.append m[6] a[5] {k:30}[4] xs[2] ys[1]))
+Yaffle> [((Main.app2 (Main.Nil [Just a = _])) $y) = y, ((Main.app2 ((((Main.Cons [Just k = _]) [Just a = _]) $x) $z)) $y) = ((((Main.Cons [Just k = ((Main.plus {_:203}) m)]) [Just a = a]) x) (((((Main.app2 [Just m = m]) [Just a = a]) [Just n = {_:203}]) z) y))]
+Yaffle> [((Main.zip (Main.Nil [Just a = _])) $y) = (Main.Nil [Just a = ((Main.Pair a) b)]), ((Main.zip ((((Main.Cons [Just k = _]) [Just a = _]) $x) $z)) ((((Main.Cons [Just k = _]) [Just a = _]) $y) $w)) = ((((Main.Cons [Just k = {_:319}]) [Just a = ((Main.Pair a) b)]) ((((Main.MkPair [Just b = b]) [Just a = a]) x) y)) (((((Main.zip [Just b = b]) [Just a = a]) [Just n = {_:319}]) z) w))]
+Yaffle> [(((Main.zipWith $f) (Main.Nil [Just a = _])) $y) = (Main.Nil [Just a = c]), (((Main.zipWith $f) ((((Main.Cons [Just k = _]) [Just a = _]) $x) $z)) ((((Main.Cons [Just k = _]) [Just a = _]) $y) $w)) = ((((Main.Cons [Just k = {_:481}]) [Just a = c]) ((f x) y)) (((((((Main.zipWith [Just n = {_:481}]) [Just c = c]) [Just b = b]) [Just a = a]) f) z) w))]
 Yaffle> Bye for now!

tests/ttimp/with001/expected

@@ -3,5 +3,5 @@ Written TTC
 Yaffle> (Main.Odd (Main.S Main.Z))
 Yaffle> (Main.Even (Main.S Main.Z))
 Yaffle> (Main.Nothing [Just a = ((((Main.Eq [Just b = ((Main.Pair Main.Nat) Main.Nat)]) [Just a = ((Main.Pair Main.Nat) Main.Nat)]) ((((Main.MkPair [Just b = Main.Nat]) [Just a = Main.Nat]) Main.Z) (Main.S Main.Z))) ((((Main.MkPair [Just b = Main.Nat]) [Just a = Main.Nat]) (Main.S Main.Z)) (Main.S (Main.S Main.Z))))])
-Yaffle> ((Main.Just [Just a = ((((Main.Eq [Just b = ((Main.Pair Main.Nat) Main.Nat)]) [Just a = ((Main.Pair Main.Nat) Main.Nat)]) ((((Main.MkPair [Just b = Main.Nat]) [Just a = Main.Nat]) Main.Z) (Main.S Main.Z))) ((((Main.MkPair [Just b = Main.Nat]) [Just a = Main.Nat]) Main.Z) (Main.S Main.Z)))]) ((Main.Refl [Just {b:9} = ((Main.Pair Main.Nat) Main.Nat)]) [Just x = ((((Main.MkPair [Just b = Main.Nat]) [Just a = Main.Nat]) Main.Z) (Main.S Main.Z))]))
+Yaffle> ((Main.Just [Just a = ((((Main.Eq [Just b = ((Main.Pair Main.Nat) Main.Nat)]) [Just a = ((Main.Pair Main.Nat) Main.Nat)]) ((((Main.MkPair [Just b = Main.Nat]) [Just a = Main.Nat]) Main.Z) (Main.S Main.Z))) ((((Main.MkPair [Just b = Main.Nat]) [Just a = Main.Nat]) Main.Z) (Main.S Main.Z)))]) ((Main.Refl [Just {b:10} = ((Main.Pair Main.Nat) Main.Nat)]) [Just x = ((((Main.MkPair [Just b = Main.Nat]) [Just a = Main.Nat]) Main.Z) (Main.S Main.Z))]))
 Yaffle> Bye for now!