[ re #660 ] eta-contract parameter candidates

src/Core/Context/Data.idr

@@ -4,6 +4,7 @@ module Core.Context.Data
 
 import Core.Context
 import Core.Context.Log
+import Core.Normalise
 
 import Data.List
 import Data.Maybe
@@ -23,32 +24,34 @@ dropReps {vars} (Just (Local fc r x p) :: xs)
     toNothing tm = tm
 dropReps (x :: xs) = x :: dropReps xs
 
-updateParams : Maybe (List (Maybe (Term vars))) ->
+updateParams : {auto _ : Ref Ctxt Defs} -> {vars : _} ->
+               Maybe (List (Maybe (Term vars))) ->
                   -- arguments to the type constructor which could be
                   -- parameters
                   -- Nothing, as an argument, means this argument can't
                   -- be a parameter position
                List (Term vars) ->
                   -- arguments to an application
-               List (Maybe (Term vars))
-updateParams Nothing args = dropReps $ map couldBeParam args
+               Core (List (Maybe (Term vars)))
+updateParams Nothing args = dropReps <$> traverse couldBeParam args
   where
-    couldBeParam : Term vars -> Maybe (Term vars)
-    couldBeParam (Local fc r v p) = Just (Local fc r v p)
-    couldBeParam _ = Nothing
-updateParams (Just args) args' = dropReps $ zipWith mergeArg args args'
+    couldBeParam : Term vars -> Core (Maybe (Term vars))
+    couldBeParam tm = pure $ case !(etaContract tm) of
+      Local fc r v p => Just (Local fc r v p)
+      _ => Nothing
+updateParams (Just args) args' = pure $ dropReps $ zipWith mergeArg args args'
   where
     mergeArg : Maybe (Term vars) -> Term vars -> Maybe (Term vars)
     mergeArg (Just (Local fc r x p)) (Local _ _ y _)
         = if x == y then Just (Local fc r x p) else Nothing
     mergeArg _ _ = Nothing
 
-getPs : {vars : _} ->
+getPs : {auto _ : Ref Ctxt Defs} -> {vars : _} ->
         Maybe (List (Maybe (Term vars))) -> Name -> Term vars ->
-        Maybe (List (Maybe (Term vars)))
+        Core (Maybe (List (Maybe (Term vars))))
 getPs acc tyn (Bind _ x (Pi _ _ _ ty) sc)
-      = let scPs = getPs (Prelude.map (Prelude.map (Prelude.map weaken)) acc) tyn sc in
-            map (map shrink) scPs
+      = do scPs <- getPs (map (map (map weaken)) acc) tyn sc
+           pure $ map (map shrink) scPs
   where
     shrink : Maybe (Term (x :: vars)) -> Maybe (Term vars)
     shrink Nothing = Nothing
@@ -57,9 +60,9 @@ getPs acc tyn tm
     = case getFnArgs tm of
            (Ref _ _ n, args) =>
               if n == tyn
-                 then Just (updateParams acc args)
-                 else acc
-           _ => acc
+                 then Just <$> updateParams acc args
+                 else pure acc
+           _ => pure acc
 
 toPos : Maybe (List (Maybe a)) -> List Nat
 toPos Nothing = []
@@ -70,19 +73,22 @@ toPos (Just ns) = justPos 0 ns
     justPos i (Just x :: xs) = i :: justPos (1 + i) xs
     justPos i (Nothing :: xs) = justPos (1 + i) xs
 
-getConPs : {vars : _} ->
-           Maybe (List (Maybe (Term vars))) -> Name -> Term vars -> List Nat
+getConPs : {auto _ : Ref Ctxt Defs} -> {vars : _} ->
+           Maybe (List (Maybe (Term vars))) -> Name -> Term vars ->
+           Core (List Nat)
 getConPs acc tyn (Bind _ x (Pi _ _ _ ty) sc)
-    = let bacc = getPs acc tyn ty in
-          getConPs (map (map (map weaken)) bacc) tyn sc
+    = do bacc <- getPs acc tyn ty
+         getConPs (map (map (map weaken)) bacc) tyn sc
 getConPs acc tyn (Bind _ x (Let _ _ v ty) sc)
     = getConPs acc tyn (subst v sc)
-getConPs acc tyn tm = toPos (getPs acc tyn tm)
+getConPs acc tyn tm = toPos <$> getPs acc tyn tm
 
-paramPos : Name -> (dcons : List ClosedTerm) ->
-           Maybe (List Nat)
-paramPos tyn [] = Nothing -- no constructor!
-paramPos tyn dcons = Just $ intersectAll (map (getConPs Nothing tyn) dcons)
+paramPos : {auto _ : Ref Ctxt Defs} -> Name -> (dcons : List ClosedTerm) ->
+           Core (Maybe (List Nat))
+paramPos tyn [] = pure Nothing -- no constructor!
+paramPos tyn dcons = do
+  candidates <- traverse (getConPs Nothing tyn) dcons
+  pure $ Just $ intersectAll candidates
 
 export
 addData : {auto c : Ref Ctxt Defs} ->
@@ -92,7 +98,7 @@ addData vars vis tidx (MkData (MkCon dfc tyn arity tycon) datacons)
          tag <- getNextTypeTag
          let allPos = allDet arity
          -- In case there are no constructors, all the positions are parameter positions!
-         let paramPositions = fromMaybe allPos (paramPos (Resolved tidx) (map type datacons))
+         let paramPositions = fromMaybe allPos !(paramPos (Resolved tidx) (map type datacons))
          log "declare.data.parameters" 20 $
             "Positions of parameters for datatype" ++ show tyn ++
             ": [" ++ showSep ", " (map show paramPositions) ++ "]"

src/Core/Core.idr

@@ -447,6 +447,12 @@ export %inline
                                Left err => pure (Left err)
                                Right val => runCore (f val)))
 
+-- Flipped bind
+infixr 1 =<<
+export %inline
+(=<<) : (a -> Core b) -> Core a -> Core b
+(=<<) = flip (>>=)
+
 -- Applicative (specialised)
 export %inline
 pure : a -> Core a
@@ -536,6 +542,26 @@ namespace Binder
   traverse f (PLet fc c val ty) = pure $ PLet fc c !(f val) !(f ty)
   traverse f (PVTy fc c ty) = pure $ PVTy fc c !(f ty)
 
+export
+mapTermM : ({vars : _} -> Term vars -> Core (Term vars)) ->
+           ({vars : _} -> Term vars -> Core (Term vars))
+mapTermM f = goTerm where
+
+    goTerm : {vars : _} -> Term vars -> Core (Term vars)
+    goTerm tm@(Local _ _ _ _) = f tm
+    goTerm tm@(Ref _ _ _) = f tm
+    goTerm (Meta fc n i args) = f =<< Meta fc n i <$> traverse goTerm args
+    goTerm (Bind fc x bd sc) = f =<< Bind fc x <$> traverse goTerm bd <*> goTerm sc
+    goTerm (App fc fn arg) = f =<< App fc <$> goTerm fn <*> goTerm arg
+    goTerm (As fc u as pat) = f =<< As fc u <$> goTerm as <*> goTerm pat
+    goTerm (TDelayed fc la d) = f =<< TDelayed fc la <$> goTerm d
+    goTerm (TDelay fc la ty arg) = f =<< TDelay fc la <$> goTerm ty <*> goTerm arg
+    goTerm (TForce fc la t) = f =<< TForce fc la <$> goTerm t
+    goTerm tm@(PrimVal _ _) = f tm
+    goTerm tm@(Erased _ _) = f tm
+    goTerm tm@(TType _) = f tm
+
+
 export
 anyM : (a -> Core Bool) -> List a -> Core Bool
 anyM f [] = pure False

src/Core/Normalise.idr

@@ -734,6 +734,36 @@ normaliseScope defs env (Bind fc n b sc)
     = pure $ Bind fc n b !(normaliseScope defs (b :: env) sc)
 normaliseScope defs env tm = normalise defs env tm
 
+export
+etaContract : {auto _ : Ref Ctxt Defs} ->
+              {vars : _} -> Term vars -> Core (Term vars)
+etaContract tm = do
+  defs <- get Ctxt
+  logTerm "eval.eta" 5 "Attempting to eta contract subterms of" tm
+  nf <- normalise defs (mkEnv EmptyFC _) tm
+  logTerm "eval.eta" 5 "Evaluated to" nf
+  res <- mapTermM act tm
+  logTerm "eval.eta" 5 "Result of eta-contraction" res
+  pure res
+
+   where
+
+    act : {vars : _} -> Term vars -> Core (Term vars)
+    act tm = do
+      logTerm "eval.eta" 10 "  Considering" tm
+      case tm of
+        (Bind _ x (Lam _ _ _ _) (App _ fn (Local _ _ Z _))) => do
+          logTerm "eval.eta" 10 "  Shrinking candidate" fn
+          let shrunk = shrinkTerm fn (DropCons SubRefl)
+          case shrunk of
+            Nothing => do
+              log "eval.eta" 10 "  Failure!"
+              pure tm
+            Just tm' => do
+              logTerm "eval.eta" 10 "  Success!" tm'
+              pure tm'
+        _ => pure tm
+
 public export
 interface Convert (tm : List Name -> Type) where
   convert : {auto c : Ref Ctxt Defs} ->

src/Core/TT.idr

@@ -569,46 +569,6 @@ data Term : List Name -> Type where
               Term vars
      TType : FC -> Term vars
 
-export
-mapTermM : Monad m => (forall vars. Term vars -> m (Term vars)) ->
-                      forall vars. Term vars -> m (Term vars)
-mapTermM f = goTerm where
-
-  mutual
-
-    goTerm : forall vars. Term vars -> m (Term vars)
-    goTerm tm@(Local _ _ _ _) = f tm
-    goTerm tm@(Ref _ _ _) = f tm
-    goTerm (Meta fc n i args) = (>>= f) $ Meta fc n i <$> traverse goTerm args
-    goTerm (Bind fc x bd sc) = (>>= f) $ Bind fc x <$> goBinder bd <*> goTerm sc
-    goTerm (App fc fn arg) = (>>= f) $ App fc <$> goTerm fn <*> goTerm arg
-    goTerm (As fc u as pat) = (>>= f) $ As fc u <$> goTerm as <*> goTerm pat
-    goTerm (TDelayed fc la d) = (>>= f) $ TDelayed fc la <$> goTerm d
-    goTerm (TDelay fc la ty arg) = (>>= f) $ TDelay fc la <$> goTerm ty <*> goTerm arg
-    goTerm (TForce fc la t) = (>>= f) $ TForce fc la <$> goTerm t
-    goTerm tm@(PrimVal _ _) = f tm
-    goTerm tm@(Erased _ _) = f tm
-    goTerm tm@(TType _) = f tm
-
-    goBinder : forall vars. Binder (Term vars) -> m (Binder (Term vars))
-    goBinder (Lam fc rig info ty) = Lam fc rig <$> goPiInfo info <*> goTerm ty
-    goBinder (Let fc rig val ty) = Let fc rig <$> goTerm val <*> goTerm ty
-    goBinder (Pi fc rig info ty) = Pi fc rig <$> goPiInfo info <*> goTerm ty
-    goBinder (PVar fc rig info ty) = PVar fc rig <$> goPiInfo info <*> goTerm ty
-    goBinder (PLet fc rig val ty) = PLet fc rig <$> goTerm val <*> goTerm ty
-    goBinder (PVTy fc rig ty) = PVTy fc rig <$> goTerm ty
-
-    goPiInfo : forall vars. PiInfo (Term vars) -> m (PiInfo (Term vars))
-    goPiInfo (DefImplicit t) = DefImplicit <$> goTerm t
-    goPiInfo Implicit = pure Implicit
-    goPiInfo Explicit = pure Explicit
-    goPiInfo AutoImplicit = pure AutoImplicit
-
-export
-mapTerm : (forall vars. Term vars -> Term vars) ->
-          (forall vars. Term vars -> Term vars)
-mapTerm f = runIdentity . mapTermM (Id . f)
-
 export
 getLoc : Term vars -> FC
 getLoc (Local fc _ _ _) = fc

tests/Main.idr

@@ -93,7 +93,7 @@ idrisTests
        -- Packages and ipkg files
        "pkg001", "pkg002", "pkg003", "pkg004", "pkg005",
        -- Positivity checking
-       "positivity001", "positivity002",
+       "positivity001", "positivity002", "positivity003",
        -- Larger programs arising from real usage. Typically things with
        -- interesting interactions between features
        "real001", "real002",

tests/idris2/positivity003/Issue660.idr

@@ -0,0 +1,14 @@
+module Main
+
+%default total
+
+%logging declare.data.parameters 20
+%logging eval.eta 10
+
+
+-- explicit
+data Value : (value : Nat -> Type) -> Type where
+  EmptyV : {0 value : Nat -> Type} -> Value (\ n => value n)
+
+data TValue : Nat -> Type where
+  MkTupleV : Value (\n => TValue n) -> TValue n

tests/idris2/positivity003/expected

@@ -0,0 +1,17 @@
+1/1: Building Issue660 (Issue660.idr)
+LOG eval.eta:5: Attempting to eta contract subterms of: \(n : Prelude.Types.Nat) => (value[1] n[0])
+LOG eval.eta:5: Evaluated to: \(n : Prelude.Types.Nat) => (value[1] n[0])
+LOG eval.eta:10:   Considering: Prelude.Types.Nat
+LOG eval.eta:10:   Considering: value[1]
+LOG eval.eta:10:   Considering: n[0]
+LOG eval.eta:10:   Considering: (value[1] n[0])
+LOG eval.eta:10:   Considering: \(n : Prelude.Types.Nat) => (value[1] n[0])
+LOG eval.eta:10:   Shrinking candidate: value[1]
+LOG eval.eta:10:   Success!: value[0]
+LOG eval.eta:5: Result of eta-contraction: value[0]
+LOG declare.data.parameters:20: Positions of parameters for datatypeMain.Value: [0]
+LOG eval.eta:5: Attempting to eta contract subterms of: n[1]
+LOG eval.eta:5: Evaluated to: n[1]
+LOG eval.eta:10:   Considering: n[1]
+LOG eval.eta:5: Result of eta-contraction: n[1]
+LOG declare.data.parameters:20: Positions of parameters for datatypeMain.TValue: [0]

tests/idris2/positivity003/run

@@ -0,0 +1,3 @@
+$1 --no-banner --no-color --console-width 0 Issue660.idr --check
+
+rm -rf build