Abstract over 'with' expression

This gives "magic with" behaviour, allowing the type of the with clause
to be refined when matching on the new argument.

README.md

@@ -76,12 +76,13 @@ play. Good luck :).
 Things still missing
 ====================
 
-+ Some high level syntax, notably record update syntax, 'with', 
-  dependent pairs, and numeric ranges
-+ 'mutual' blocks
++ Some high level syntax, notably record update syntax, dependent pairs, and
+  numeric ranges
 + 'parameters' blocks
 + Cumulativity and totality checking
 + Codata (or rather, you can have it, but there's no productivity check...)
++ 'rewrite' doesn't yet work on dependent types
++ Some details of 'with' not yet done (notably recursive with call syntax)
 + Parts of the ide-mode
 + Documentation strings
 + ':search' and ':apropos' at the REPL

src/Idris/IDEMode/Commands.idr

@@ -23,6 +23,7 @@ data IDECommand
      | GenerateDef Integer String
      | MakeLemma Integer String
      | MakeCase Integer String
+     | MakeWith Integer String
 
 readHints : List SExp -> Maybe (List String)
 readHints [] = Just []
@@ -69,7 +70,9 @@ getIDECommand (SExpList [SymbolAtom "generate-def", IntegerAtom l, StringAtom n]
 getIDECommand (SExpList [SymbolAtom "make-lemma", IntegerAtom l, StringAtom n])
     = Just $ MakeLemma l n
 getIDECommand (SExpList [SymbolAtom "make-case", IntegerAtom l, StringAtom n])
-    = Just $ MakeLemma l n
+    = Just $ MakeCase l n
+getIDECommand (SExpList [SymbolAtom "make-with", IntegerAtom l, StringAtom n])
+    = Just $ MakeWith l n
 getIDECommand _ = Nothing
 
 export

src/Idris/IDEMode/REPL.idr

@@ -122,6 +122,9 @@ process (MakeLemma l n)
 process (MakeCase l n)
     = do Idris.REPL.process (Editing (MakeCase (fromInteger l) (UN n)))
          pure ()
+process (MakeWith l n)
+    = do Idris.REPL.process (Editing (MakeWith (fromInteger l) (UN n)))
+         pure ()
 
 processCatch : {auto c : Ref Ctxt Defs} ->
                {auto u : Ref UST (UState FC)} ->

src/Idris/REPL.idr

@@ -323,6 +323,8 @@ processEdit (MakeLemma line name)
               _ => printError "Can't make lifted definition"
 processEdit (MakeCase line name)
     = printError "Not implemented yet"
+processEdit (MakeWith line name)
+    = printError "Not implemented yet"
 
 export
 loadMainFile : {auto c : Ref Ctxt Defs} ->

src/Idris/Syntax.idr

@@ -319,6 +319,7 @@ data EditCmd : Type where
      GenerateDef : Int -> Name -> EditCmd
      MakeLemma : Int -> Name -> EditCmd
      MakeCase : Int -> Name -> EditCmd
+     MakeWith : Int -> Name -> EditCmd
 
 public export
 data REPLCmd : Type where

src/TTImp/ProcessDef.idr

@@ -311,19 +311,26 @@ checkClause {c} {u} {i} {m} {vars} elab incase mult hashit defining env nest (Wi
              | Nothing => throw (InternalError "Impossible happened: With abstraction failure #1")
          let Just wvalTy = shrinkTerm wvalTy withSub
              | Nothing => throw (InternalError "Impossible happened: With abstraction failure #2")
+         let Just wvalEnv = shrinkEnv env' withSub
+             | Nothing => throw (InternalError "Impossible happened: With abstraction failure #3")
          log 5 ("With value: " ++ show wval ++ " : " ++ show wvalTy)
          log 5 ("Uses env: " ++ show wevars)
          log 5 ("Required type: " ++ show reqty)
 
          -- TODO: Also abstract over 'wval' in the scope of bNotReq in order
          -- to get the 'magic with' behaviour
          let wargn = MN "warg" 0
-         let bNotReq = Bind wargn (Pi RigW Explicit wvalTy)
-                            (weaken (bindNotReq 0 env' withSub reqty))
+         let scenv = Pi RigW Explicit wvalTy :: wvalEnv
+
+         let wtyScope = replace gam scenv (nf gam scenv (weaken wval))
+                            (Local (Just RigW) Here)
+                            (nf gam scenv 
+                                (weaken (bindNotReq 0 env' withSub reqty)))
+         let bNotReq = Bind wargn (Pi RigW Explicit wvalTy) wtyScope
          log 10 ("Bound unrequired vars: " ++ show bNotReq)
 
          let Just wtype = bindReq env' withSub bNotReq
-             | Nothing => throw (InternalError "Impossible happened: With abstraction failure #3")
+             | Nothing => throw (InternalError "Impossible happened: With abstraction failure #4")
 
          -- list of argument names - 'Just' means we need to match the name
          -- in the with clauses to find out what the pattern should be.