Fix interaction between as patterns and case

There was a check on evaluating lets which was in Blodwen but I hadn't
added to the normaliser yet! Also, normalisation needs to reduce as
patterns for unification, but not when reducing finished LHS and
argument terms. This is a bit of a hack (but then, so is the
implementation of as patterns in general...).

So, when we're checking a nested expression, we have the as pattern as a
let bound variable (so that it has the necessary computational force)
but when we compile we just pass it as an ordinary argument, then it
gets the desired behaviour in case trees.

src/Core/Normalise.idr

@@ -82,9 +82,11 @@ parameters (defs : Defs, topopts : EvalOpts)
     eval env locs (App fc fn p arg) stk 
         = eval env locs fn ((p, MkClosure topopts locs env arg) :: stk)
     eval env locs (As fc n tm) stk 
-        = do n' <- eval env locs n stk
-             tm' <- eval env locs tm stk 
-             pure (NAs fc n' tm')
+        = if removeAs topopts
+             then eval env locs tm stk
+             else do n' <- eval env locs n stk
+                     tm' <- eval env locs tm stk 
+                     pure (NAs fc n' tm')
     eval env locs (TDelayed fc r ty) stk 
         = pure (NDelayed fc r (MkClosure topopts locs env ty))
     eval env locs (TDelay fc r tm) stk 
@@ -106,7 +108,10 @@ parameters (defs : Defs, topopts : EvalOpts)
                 Core (NF free)
     evalLocal {vars = []} env locs fc mrig idx prf stk
         = case getBinder prf env of
-               Let _ val _ => eval env [] val stk
+               Let _ val _ => 
+                   if not (holesOnly topopts)
+                      then eval env [] val stk
+                      else pure $ NApp fc (NLocal mrig idx prf) stk
                _ => pure $ NApp fc (NLocal mrig idx prf) stk
     evalLocal env (MkClosure opts locs' env' tm' :: locs) fc mrig Z First stk
         = evalWithOpts defs opts env' locs' tm' stk
@@ -359,9 +364,17 @@ nfOpts opts defs env tm = eval defs opts env [] tm []
 
 export
 gnf : Env Term vars -> Term vars -> Glued vars
-gnf env tm = MkGlue (pure tm) 
-                    (\c => do defs <- get Ctxt
-                              nf defs env tm)
+gnf env tm 
+    = MkGlue (pure tm) 
+             (\c => do defs <- get Ctxt
+                       nf defs env tm)
+
+export
+gnfOpts : EvalOpts -> Env Term vars -> Term vars -> Glued vars
+gnfOpts opts env tm 
+    = MkGlue (pure tm) 
+             (\c => do defs <- get Ctxt
+                       nfOpts opts defs env tm)
 
 export
 gType : FC -> Glued vars
@@ -527,6 +540,11 @@ normaliseHoles : Defs -> Env Term free -> Term free -> Core (Term free)
 normaliseHoles defs env tm 
     = quote defs env !(nfOpts withHoles defs env tm)
 
+export
+normaliseLHS : Defs -> Env Term free -> Term free -> Core (Term free)
+normaliseLHS defs env tm 
+    = quote defs env !(nfOpts onLHS defs env tm)
+
 export
 normaliseArgHoles : Defs -> Env Term free -> Term free -> Core (Term free)
 normaliseArgHoles defs env tm 
@@ -728,4 +746,24 @@ logGlueNF lvl msg env gtm
                                           ++ ": " ++ show tm'
             else pure ()
 
+export
+logEnv : {vars : _} ->
+         {auto c : Ref Ctxt Defs} ->
+         Nat -> String -> Env Term vars -> Core ()
+logEnv lvl msg env
+    = do opts <- getOpts
+         if logLevel opts >= lvl
+            then dumpEnv env
+            else pure ()
+  where
+    dumpEnv : {vs : List Name} -> Env Term vs -> Core ()
+    dumpEnv [] = pure ()
+    dumpEnv {vs = x :: _} (Let _ val ty :: bs)
+        = do logTermNF lvl (msg ++ ": let " ++ show x) bs val
+             logTermNF lvl (msg ++ ":" ++ show x) bs ty
+             dumpEnv bs
+    dumpEnv {vs = x :: _} (b :: bs)
+        = do logTermNF lvl (msg ++ ":" ++ show x) bs (binderType b)
+             dumpEnv bs
+
 

src/Core/Value.idr

@@ -12,6 +12,7 @@ record EvalOpts where
   constructor MkEvalOpts
   holesOnly : Bool -- only evaluate hole solutions
   argHolesOnly : Bool -- only evaluate holes which are relevant arguments
+  removeAs : Bool -- reduce 'as' patterns (don't do this on LHS)
   usedMetas : IntMap () -- Metavariables we're under, to detect cycles
   evalAll : Bool -- evaluate everything, including private names
   tcInline : Bool -- inline for totality checking
@@ -19,15 +20,19 @@ record EvalOpts where
 
 export
 defaultOpts : EvalOpts
-defaultOpts = MkEvalOpts False False empty True False Nothing
+defaultOpts = MkEvalOpts False False True empty True False Nothing
 
 export
 withHoles : EvalOpts
-withHoles = MkEvalOpts True True empty True False Nothing
+withHoles = MkEvalOpts True True False empty True False Nothing
 
 export
 withArgHoles : EvalOpts
-withArgHoles = MkEvalOpts False True empty True False Nothing
+withArgHoles = MkEvalOpts False True False empty True False Nothing
+
+export
+onLHS : EvalOpts
+onLHS = record { removeAs = False } defaultOpts
 
 mutual
   public export

src/TTImp/Elab/App.idr

@@ -70,7 +70,9 @@ getVarType rigc nest env fc x
                              tm = tmf fc nt
                              tyenv = useVars (map snd (getArgs tm))
                                              (embed (type ndef)) in
-                             pure (tm, gnf env tyenv)
+                             do logTerm 10 ("Type of " ++ show n') tyenv
+                                logTerm 10 ("Expands to") tm
+                                pure (tm, gnf env tyenv)
     where
       useVars : List (Term vars) -> Term vars -> Term vars
       useVars [] sc = sc
@@ -182,27 +184,21 @@ mutual
              (argv, argt) <- check argRig (nextLevel elabinfo)
                                    nest env arg (Just (glueBack defs env aty'))
              defs <- get Ctxt
-             -- If we're on the LHS, and the metaval was solved at this
-             -- point, reinstantiate it with 'argv' because it *may* have
-             -- as patterns in it and we need to retain them.
+             -- If we're on the LHS, reinstantiate it with 'argv' because it
+             -- *may* have as patterns in it and we need to retain them.
              -- (As patterns are a bit of a hack but I don't yet see a 
              -- better way that leads to good code...)
-             isHole <- the (Core Bool) $ case elabMode elabinfo of
-                            InLHS _ => 
-                              do Just (Hole _) <- lookupDefExact (Resolved idx)
-                                                                 (gamma defs)
-                                        | _ => pure False
-                                 pure True
-                            _ => pure True
              [] <- convert fc elabinfo env (gnf env metaval)
                                            (gnf env argv)
                 | cs => throw (CantConvert fc env metaval argv)
-             if not isHole -- reset hole and redo it
-                then do updateDef (Resolved idx) (const (Just (Hole False)))
-                        convert fc elabinfo env (gnf env metaval) 
-                                                (gnf env argv)
+             case elabMode elabinfo of
+                  InLHS _ => -- reset hole and redo it with the unexpanded definition
+                     do updateDef (Resolved idx) (const (Just (Hole False)))
+                        convert fc elabinfo env 
+                                   (gnfOpts withHoles (noLet env) metaval) 
+                                   (gnfOpts withHoles (noLet env) argv)
                         pure ()
-                else pure ()
+                  _ => pure ()
              removeHoleName nm
              pure (tm, gty)
            else do
@@ -220,6 +216,12 @@ mutual
              fnty <- sc defs (toClosure defaultOpts env argv)
              checkAppWith rig elabinfo nest env fc
                           fntm fnty expargs impargs kr expty
+    where
+      noLet : Env Term vs -> Env Term vs
+      noLet [] = []
+      noLet (Let c v t :: env) = Lam c Explicit t :: noLet env
+      noLet (b :: env) = b :: noLet env
+
 
   -- Check an application of 'fntm', with type 'fnty' to the given list
   -- of explicit and implicit arguments.

src/TTImp/Elab/Case.idr

@@ -76,11 +76,21 @@ changeVar (MkVar {i=x} old) (MkVar new) (Local fc r idx p)
     = if x == idx
          then Local fc r _ new
          else Local fc r _ p
+changeVar old new (Meta fc nm i args)
+    = Meta fc nm i (map (changeVar old new) args)
 changeVar (MkVar old) (MkVar new) (Bind fc x b sc) 
     = Bind fc x (assert_total (map (changeVar (MkVar old) (MkVar new)) b)) 
 		            (changeVar (MkVar (Later old)) (MkVar (Later new)) sc)
 changeVar old new (App fc fn p arg) 
     = App fc (changeVar old new fn) p (changeVar old new arg)
+changeVar old new (As fc nm p)
+    = As fc (changeVar old new nm) (changeVar old new p)
+changeVar old new (TDelayed fc r p)
+    = TDelayed fc r (changeVar old new p)
+changeVar old new (TDelay fc r p)
+    = TDelay fc r (changeVar old new p)
+changeVar old new (TForce fc p)
+    = TForce fc (changeVar old new p)
 changeVar old new tm = tm
 
 findLater : (x : Name) -> (newer : List Name) -> Var (newer ++ x :: older)
@@ -335,6 +345,7 @@ caseBlock {vars} rigc elabinfo fc nest env scr scrtm scrty caseRig alts expected
          casefnty <- abstractOver fc defs (implicitMode elabinfo)
                                      env (Just (subEnv est)) fullImps envscope
 
+         logEnv 10 "Case env" env
          logTermNF 2 ("Case function type: " ++ show casen) [] casefnty
 
          -- If we've had to add implicits to the case type (because there

src/TTImp/ProcessDef.idr

@@ -145,14 +145,16 @@ checkClause mult hashit n nest env (ImpossibleClause fc lhs)
 checkClause mult hashit n nest env (PatClause fc lhs_in rhs)
     = do lhs <- lhsInCurrentNS nest lhs_in 
          log 5 $ "Checking " ++ show lhs
+         logEnv 5 "In env" env
          (lhstm, lhstyg) <- elabTerm n (InLHS mult) nest env 
                                 (IBindHere fc PATTERN lhs) Nothing
+         logTerm 10 "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 <- normalise defs (noLet env) lhstm
+         lhstm <- normaliseLHS defs (noLet env) lhstm
          lhsty <- normaliseHoles defs env lhsty
          linvars_in <- findLinear True 0 Rig1 lhstm
          log 5 $ "Linearity of names in " ++ show n ++ ": " ++ 

tests/ttimp/nest002/Case.yaff

@@ -32,16 +32,9 @@ cvec {n = $n} $xs
            Nil => n
            Cons $x $xs => n
 
--- Doesn't quite work yet...
--- cvec2 : {n : _} -> Vect n $a -> Nat
--- cvec2 {n = n@(_)} $xs
---     = case xs of
---            Nil => n
---            Cons $x $xs => n
-
-simpleAs : Nat -> Nat
-simpleAs x@(_) = x
-
-cas : (n : Nat) -> Vect $n $a -> Nat
-cas n@(_) Nil = n
+cvec2 : {n : _} -> Vect n $a -> Nat
+cvec2 {n = n@(_)} $xs
+    = case xs of
+           Nil => n
+           Cons $x $xs => n
 

tests/ttimp/nest002/expected

@@ -3,4 +3,5 @@ Written TTC
 Yaffle> (Main.S (Main.S (Main.S (Main.S (Main.S Main.Z)))))
 Yaffle> ((((Main.Cons [Just k = (Main.S Main.Z)]) [Just a = Integer]) 1) ((((Main.Cons [Just k = Main.Z]) [Just a = Integer]) 2) (Main.Nil [Just a = Integer])))
 Yaffle> (Main.S (Main.S (Main.S Main.Z)))
+Yaffle> (Main.S (Main.S (Main.S Main.Z)))
 Yaffle> Bye for now!

tests/ttimp/nest002/input

@@ -1,4 +1,5 @@
 cplus (S (S Z)) (S (S (S Z)))
 cappend (Cons 1 Nil) (Cons 2 Nil)
 cvec (Cons 1 (Cons 2 (Cons 3 Nil)))
+cvec2 (Cons 1 (Cons 2 (Cons 3 Nil)))
 :q