From 1a51d3afc40ab3b154a2c66902606811f4db01db Mon Sep 17 00:00:00 2001
From: Edwin Brady <ecb10@st-andrews.ac.uk>
Date: Sat, 1 Dec 2018 17:15:10 +0000
Subject: [PATCH] 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                      |  7 ++++---
 src/Idris/IDEMode/Commands.idr |  5 ++++-
 src/Idris/IDEMode/REPL.idr     |  3 +++
 src/Idris/REPL.idr             |  2 ++
 src/Idris/Syntax.idr           |  1 +
 src/TTImp/ProcessDef.idr       | 13 ++++++++++---
 6 files changed, 24 insertions(+), 7 deletions(-)

diff --git a/README.md b/README.md
index dbe1aa0..9e2ff4a 100644
--- a/README.md
+++ b/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
diff --git a/src/Idris/IDEMode/Commands.idr b/src/Idris/IDEMode/Commands.idr
index 1aa93fa..b818ecc 100644
--- a/src/Idris/IDEMode/Commands.idr
+++ b/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
diff --git a/src/Idris/IDEMode/REPL.idr b/src/Idris/IDEMode/REPL.idr
index f21c134..f80466f 100644
--- a/src/Idris/IDEMode/REPL.idr
+++ b/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)} ->
diff --git a/src/Idris/REPL.idr b/src/Idris/REPL.idr
index 96d2844..5e1f3c3 100644
--- a/src/Idris/REPL.idr
+++ b/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} ->
diff --git a/src/Idris/Syntax.idr b/src/Idris/Syntax.idr
index 359fd5d..abcd110 100644
--- a/src/Idris/Syntax.idr
+++ b/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
diff --git a/src/TTImp/ProcessDef.idr b/src/TTImp/ProcessDef.idr
index 41259af..7a03d27 100644
--- a/src/TTImp/ProcessDef.idr
+++ b/src/TTImp/ProcessDef.idr
@@ -311,6 +311,8 @@ 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)
@@ -318,12 +320,17 @@ checkClause {c} {u} {i} {m} {vars} elab incase mult hashit defining env nest (Wi
          -- 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.