look through substitutions in Q.S.T.Split

lib/Quox/Syntax/Term/Pretty.idr

@@ -107,8 +107,8 @@ mutual
     prettyM (Sig s (S [x] t)) =
       prettyBindType {q} [] x s !timesD t
     prettyM (Pair s t) =
-      let GotPairs {init, last, _} = getPairs t in
-      prettyTuple $ s :: init ++ [last]
+      let GotPairs {init, last, _} = getPairs' [< s] t in
+      prettyTuple $ toList $ init :< last
     prettyM (Enum tags) =
       pure $ delims "`{" "}" . aseparate comma $ map prettyTag $
         Prelude.toList tags

lib/Quox/Syntax/Term/Split.idr

@@ -72,14 +72,23 @@ record GetArgs q d n where
   args     : List (Term q d n)
   0 notApp : NotApp fun
 
-export
-getArgs' : Elim q d n -> List (Term q d n) -> GetArgs q d n
-getArgs' fun args = case nchoose $ isApp fun of
-  Left  y => let f :@ a = fun in getArgs' f (a :: args)
-  Right n => GotArgs {fun, args, notApp = n}
+mutual
+  export %inline
+  getArgs' : Elim q d n -> List (Term q d n) -> GetArgs q d n
+  getArgs' fun0 args =
+    let Element fun nc = pushSubsts fun0 in
+    getArgsNc (assert_smaller fun0 fun) args
+
+  private
+  getArgsNc : (e : Elim q d n) -> (0 nc : NotClo e) =>
+              List (Term q d n) -> GetArgs q d n
+  getArgsNc fun args = case nchoose $ isApp fun of
+    Left  y => let f :@ a = fun in getArgs' f (a :: args)
+    Right n => GotArgs {fun, args, notApp = n}
 
 ||| splits an application into its head and arguments. if it's not an
-||| application then the list is just empty
+||| application then the list is just empty.
+||| looks through substitutions for applications.
 export %inline
 getArgs : Elim q d n -> GetArgs q d n
 getArgs e = getArgs' e []
@@ -98,11 +107,19 @@ record GetDArgs q d n where
   args      : List (Dim d)
   0 notDApp : NotDApp fun
 
-export
-getDArgs' : Elim q d n -> List (Dim d) -> GetDArgs q d n
-getDArgs' fun args = case nchoose $ isDApp fun of
-  Left  y => let f :% d = fun in getDArgs' f (d :: args)
-  Right n => GotDArgs {fun, args, notDApp = n}
+mutual
+  export %inline
+  getDArgs' : Elim q d n -> List (Dim d) -> GetDArgs q d n
+  getDArgs' fun0 args =
+    let Element fun nc = pushSubsts fun0 in
+    getDArgsNc (assert_smaller fun0 fun) args
+
+  private
+  getDArgsNc : (e : Elim q d n) -> (0 nc : NotClo e) =>
+               List (Dim d) -> GetDArgs q d n
+  getDArgsNc fun args = case nchoose $ isDApp fun of
+    Left  y => let f :% d = fun in getDArgs' f (d :: args)
+    Right n => GotDArgs {fun, args, notDApp = n}
 
 ||| splits a dimension application into its head and arguments. if it's not an
 ||| d application then the list is just empty
@@ -144,14 +161,25 @@ record GetLams q d n where
   0 eq     : lams + n = rest
   0 notLam : NotLam body
 
-export
-getLams' : forall lams, rest.
-           Vect lams BaseName -> Term q d rest -> (0 eq : lams + n = rest) ->
-           GetLams q d n
-getLams' xs s Refl = case nchoose $ isLam s of
-  Left  y => let Lam (S [x] body) = s in
-             getLams' (x :: xs) (assert_smaller s body.term) Refl
-  Right n => GotLams xs s Refl n
+mutual
+  export %inline
+  getLams' : forall lams, rest.
+             Vect lams BaseName -> Term q d rest -> (0 eq : lams + n = rest) ->
+             GetLams q d n
+  getLams' xs s0 eq =
+    let Element s nc = pushSubsts s0 in
+    getLamsNc xs (assert_smaller s0 s) eq
+
+  private
+  getLamsNc : forall lams, rest.
+              Vect lams BaseName ->
+              (t : Term q d rest) -> (0 nc : NotClo t) =>
+              (0 eq : lams + n = rest) ->
+              GetLams q d n
+  getLamsNc xs s Refl = case nchoose $ isLam s of
+    Left  y => let Lam (S [x] body) = s in
+               getLams' (x :: xs) (assert_smaller s body.term) Refl
+    Right n => GotLams xs s Refl n
 
 export %inline
 getLams : Term q d n -> GetLams q d n
@@ -167,14 +195,25 @@ record GetDLams q d n where
   0 eq      : lams + d = rest
   0 notDLam : NotDLam body
 
-export
-getDLams' : forall lams, rest.
-            Vect lams BaseName -> Term q rest n -> (0 eq : lams + d = rest) ->
-            GetDLams q d n
-getDLams' is s Refl = case nchoose $ isDLam s of
-  Left  y => let DLam (S [i] body) = s in
-             getDLams' (i :: is) (assert_smaller s body.term) Refl
-  Right n => GotDLams is s Refl n
+mutual
+  export %inline
+  getDLams' : forall lams, rest.
+              Vect lams BaseName -> Term q rest n -> (0 eq : lams + d = rest) ->
+              GetDLams q d n
+  getDLams' xs s0 eq =
+    let Element s nc = pushSubsts s0 in
+    getDLamsNc xs (assert_smaller s0 s) eq
+
+  private
+  getDLamsNc : forall lams, rest.
+               Vect lams BaseName ->
+               (t : Term q rest n) -> (0 nc : NotClo t) =>
+               (0 eq : lams + d = rest) ->
+               GetDLams q d n
+  getDLamsNc is s Refl = case nchoose $ isDLam s of
+    Left  y => let DLam (S [i] body) = s in
+               getDLams' (i :: is) (assert_smaller s body.term) Refl
+    Right n => GotDLams is s Refl n
 
 export %inline
 getDLams : Term q d n -> GetDLams q d n
@@ -184,14 +223,25 @@ getDLams s = getDLams' [] s Refl
 public export
 record GetPairs q d n where
   constructor GotPairs
-  init : List $ Term q d n
+  init : SnocList $ Term q d n
   last : Term q d n
   notPair : NotPair last
 
+mutual
+  export %inline
+  getPairs' : SnocList (Term q d n) -> Term q d n -> GetPairs q d n
+  getPairs' ss t0 =
+    let Element t nc = pushSubsts t0 in getPairsNc ss (assert_smaller t0 t)
+
+  private
+  getPairsNc : SnocList (Term q d n) ->
+               (t : Term q d n) -> (0 nc : NotClo t) =>
+               GetPairs q d n
+  getPairsNc ss t = case nchoose $ isPair t of
+    Left  y => let Pair s t = t in
+               getPairs' (ss :< s) t
+    Right n => GotPairs ss t n
+
 export
 getPairs : Term q d n -> GetPairs q d n
-getPairs t = case nchoose $ isPair t of
-  Left y =>
-    let Pair s t = t; GotPairs ts t np = getPairs t in
-    GotPairs (s :: ts) t np
-  Right n => GotPairs [] t n
+getPairs = getPairs' [<]