add some whnf stuff

src/Quox/Syntax/Term.idr

@@ -16,6 +16,7 @@ import Data.Maybe
 import Data.Nat
 import public Data.So
 import Data.String
+import Data.Vect
 
 %default total
 
@@ -87,24 +88,79 @@ BVT : (i : Nat) -> (0 _ : LT i n) => Term d n
 BVT i = E $ BV i
 
 
+public export %inline
+isLam : Term d n -> Bool
+isLam (Lam {}) = True
+isLam _        = False
+
+public export
+NotLam : Term d n -> Type
+NotLam = So . not . isLam
+
+
+public export %inline
+isApp : Elim d n -> Bool
+isApp ((:@) {}) = True
+isApp _         = False
+
+public export
+NotApp : Elim d n -> Type
+NotApp = So . not . isApp
+
+
 infixl 9 :@@
 ||| apply multiple arguments at once
 public export %inline
 (:@@) : Elim d n -> List (Term d n) -> Elim d n
 f :@@ ss = foldl (:@) f ss
 
+public export
+record GetArgs (d, n : Nat) where
+  constructor GotArgs
+  fun      : Elim d n
+  args     : List (Term d n)
+  0 notApp : NotApp fun
+
 private
-getArgs' : Elim d n -> List (Term d n) -> (Elim d n, List (Term d n))
+getArgs' : Elim d n -> List (Term d n) -> GetArgs d n
-getArgs' (f :@ s) args = getArgs' f (s :: args)
+getArgs' fun args with (choose $ isApp fun)
-getArgs' f        args = (f, args)
+  getArgs' (f :@ a) args | Left yes = getArgs' f (a :: args)
+  _ | Right no = GotArgs {fun, args, notApp = no}
 
 ||| splits an application into its head and arguments. if it's not an
 ||| application then the list is just empty
 export %inline
-getArgs : Elim d n -> (Elim d n, List (Term d n))
+getArgs : Elim d n -> GetArgs d n
 getArgs e = getArgs' e []
 
 
+infixr 1 :\\
+public export
+(:\\) : Vect m Name -> Term d (m + n) -> Term d n
+[]      :\\ t = t
+x :: xs :\\ t = let t' = replace {p = Term _} (plusSuccRightSucc {}) t in
+                Lam x $ xs :\\ t'
+
+public export
+record GetLams (d, n : Nat) where
+  constructor GotLams
+  names    : Vect lams Name
+  body     : Term d rest
+  0 eq     : lams + n = rest
+  0 notLam : NotLam body
+
+public export
+getLams : Term d n -> GetLams d n
+getLams s with (choose $ isLam s)
+  getLams (Lam x s) | Left yes =
+    let inner = getLams s in
+    GotLams {names  = x :: inner.names,
+             body   = inner.body,
+             eq     = plusSuccRightSucc {} `trans` inner.eq,
+             notLam = inner.notLam}
+  _ | Right no = GotLams {names = [], body = s, eq = Refl, notLam = no}
+
+
 parameters {auto _ : Pretty.HasEnv m}
   private %inline arrowD : m (Doc HL)
   arrowD = hlF Syntax $ ifUnicode "→" "->"
@@ -150,7 +206,7 @@ mutual
     prettyM (B i) =
       prettyVar TVar TVarErr (!ask).tnames i
     prettyM (e :@ s) =
-      let (f, args) = getArgs' e [s] in
+      let GotArgs f args _ = getArgs' e [s] in
       parensIfM App =<< withPrec Arg
         [|prettyM f <//> (align . sep <$> traverse prettyM args)|]
     prettyM (s :# a) =
@@ -315,7 +371,7 @@ mutual
   pushSubstsE : Elim d n -> NotCloElim d n
   pushSubstsE e = pushSubstsEWith id id e
 
-  private
+  export
   pushSubstsTWith : DSubst dfrom dto -> TSubst dto from to ->
                     Term dfrom from -> NotCloTerm dto to
   pushSubstsTWith th ph (TYPE l) =
@@ -331,7 +387,7 @@ mutual
   pushSubstsTWith th ph (DCloT s ps) =
     pushSubstsTWith (ps . th) ph s
 
-  private
+  export
   pushSubstsEWith : DSubst dfrom dto -> TSubst dto from to ->
                     Elim dfrom from -> NotCloElim dto to
   pushSubstsEWith th ph (F x) =
@@ -348,49 +404,149 @@ mutual
     pushSubstsEWith (ps . th) ph e
 
 
+parameters (th : DSubst dfrom dto) (ph : TSubst dto from to)
+  public export %inline
+  pushSubstsTWith' : Term dfrom from -> Term dto to
+  pushSubstsTWith' s = (pushSubstsTWith th ph s).fst
+
+  public export %inline
+  pushSubstsEWith' : Elim dfrom from -> Elim dto to
+  pushSubstsEWith' e = (pushSubstsEWith th ph e).fst
+
+
 public export %inline
 pushSubstsT' : Term d n -> Term d n
 pushSubstsT' s = (pushSubstsT s).fst
 
-
 public export %inline
 pushSubstsE' : Elim d n -> Elim d n
 pushSubstsE' e = (pushSubstsE e).fst
 
 
-parameters {auto _ : Alternative f}
+public export
-  ||| `(λx. t ⦂ (x: A) → B) s >>> (t ⦂ B)[x ≔ (s ⦂ A)]`
+data IsRedexT : Term d n -> Type where
-  export
+  IsUpsilon : IsRedexT $ E (_ :# _)
-  betaLam1 : Elim d n -> f (Elim d n)
+  IsCloT    : IsRedexT $ CloT {}
-  betaLam1 ((Lam {body, _} :# Pi {arg, res, _}) :@ s) =
+  IsDCloT   : IsRedexT $ DCloT {}
-    pure $ (body :# res) // (s :# arg ::: id)
-  betaLam1 _ = empty
 
-  ||| `(e ⦂ A) >>> e`    [if `e` is an elim]
+public export %inline
-  export
+NotRedexT : Term d n -> Type
-  upsilon1 : Elim d n -> f (Elim d n)
+NotRedexT = Not . IsRedexT
-  upsilon1 (E e :# _) = pure e
-  upsilon1 _          = empty
 
-  export
+public export
-  step : Elim d n -> f (Elim d n)
+data IsRedexE : Elim d n -> Type where
-  step e = betaLam1 e <|> upsilon1 e
+  IsBetaLam : IsRedexE $ (Lam {} :# Pi {}) :@ _
+  IsCloE    : IsRedexE $ CloE {}
+  IsDCloE   : IsRedexE $ DCloE {}
 
-export
+public export %inline
-step' : Elim d n -> Elim d n
+NotRedexE : Elim d n -> Type
-step' e = fromMaybe e $ step e
+NotRedexE = Not . IsRedexE
 
 
-public export Exists2 : (ty1 -> ty2 -> Type) -> Type
+export %inline
-Exists2 t = Exists (\a => Exists (\b => t a b))
+isRedexT : (t : Term d n) -> Dec (IsRedexT t)
+isRedexT (E (_ :# _))   = Yes IsUpsilon
+isRedexT (CloT {})      = Yes IsCloT
+isRedexT (DCloT {})     = Yes IsDCloT
+isRedexT (TYPE _)       = No $ \x => case x of {}
+isRedexT (Pi {})        = No $ \x => case x of {}
+isRedexT (Lam {})       = No $ \x => case x of {}
+isRedexT (E (F _))      = No $ \x => case x of {}
+isRedexT (E (B _))      = No $ \x => case x of {}
+isRedexT (E (_ :@ _))   = No $ \x => case x of {}
+isRedexT (E (CloE {}))  = No $ \x => case x of {}
+isRedexT (E (DCloE {})) = No $ \x => case x of {}
 
-parameters {0 t : ty -> Type}
+export %inline
-  public export %inline some : t a -> Exists t
+isRedexE : (e : Elim d n) -> Dec (IsRedexE e)
-  some t = Evidence _ t
+isRedexE ((Lam {} :# Pi {}) :@ _)      = Yes IsBetaLam
+isRedexE (CloE {})                     = Yes IsCloE
+isRedexE (DCloE {})                    = Yes IsDCloE
+isRedexE (F x)                         = No $ \x => case x of {}
+isRedexE (B i)                         = No $ \x => case x of {}
+isRedexE (F _                    :@ _) = No $ \x => case x of {}
+isRedexE (B _                    :@ _) = No $ \x => case x of {}
+isRedexE (_ :@ _                 :@ _) = No $ \x => case x of {}
+isRedexE ((TYPE _   :# _)        :@ _) = No $ \x => case x of {}
+isRedexE ((Pi {}    :# _)        :@ _) = No $ \x => case x of {}
+isRedexE ((Lam {}   :# TYPE _)   :@ _) = No $ \x => case x of {}
+isRedexE ((Lam {}   :# Lam {})   :@ _) = No $ \x => case x of {}
+isRedexE ((Lam {}   :# E _)      :@ _) = No $ \x => case x of {}
+isRedexE ((Lam {}   :# CloT {})  :@ _) = No $ \x => case x of {}
+isRedexE ((Lam {}   :# DCloT {}) :@ _) = No $ \x => case x of {}
+isRedexE ((E _      :# _)        :@ _) = No $ \x => case x of {}
+isRedexE ((CloT {}  :# _)        :@ _) = No $ \x => case x of {}
+isRedexE ((DCloT {} :# _)        :@ _) = No $ \x => case x of {}
+isRedexE (CloE {}                :@ _) = No $ \x => case x of {}
+isRedexE (DCloE {}               :@ _) = No $ \x => case x of {}
+isRedexE (_ :# _)                      = No $ \x => case x of {}
+
+
+public export %inline
+RedexTerm : Nat -> Nat -> Type
+RedexTerm d n = Subset (Term d n) IsRedexT
+
+public export %inline
+NonRedexTerm : Nat -> Nat -> Type
+NonRedexTerm d n = Subset (Term d n) NotRedexT
+
+
+public export %inline
+RedexElim : Nat -> Nat -> Type
+RedexElim d n = Subset (Elim d n) IsRedexE
+
+public export %inline
+NonRedexElim : Nat -> Nat -> Type
+NonRedexElim d n = Subset (Elim d n) NotRedexE
+
+
+public export %inline
+stepT' : (s : Term d n) -> IsRedexT s -> Term d n
+stepT' (E (s :# _)) IsUpsilon = s
+stepT' (CloT  s th) IsCloT    = pushSubstsTWith' id th s
+stepT' (DCloT s th) IsDCloT   = pushSubstsTWith' th id s
+
+public export %inline
+stepT : (s : Term d n) -> Either (NotRedexT s) (Term d n)
+stepT s = case isRedexT s of Yes y => Right $ stepT' s y; No n => Left n
+
+public export %inline
+stepE' : (e : Elim d n) -> IsRedexE e -> Elim d n
+stepE' ((Lam {body, _} :# Pi {arg, res, _}) :@ s) IsBetaLam =
+  (body :# res) // one (s :# arg)
+stepE' (CloE  e th) IsCloE  = pushSubstsEWith' id th e
+stepE' (DCloE e th) IsDCloE = pushSubstsEWith' th id e
+
+public export %inline
+stepE : (e : Elim d n) -> Either (NotRedexE e) (Elim d n)
+stepE e = case isRedexE e of Yes y => Right $ stepE' e y; No n => Left n
+
+public export
+whnfT : Term d n -> NonRedexTerm d n
+whnfT s = case stepT s of
+               Right s'   => whnfT $ assert_smaller s s'
+               Left  done => Element s done
+
+public export
+whnfE : Elim d n -> NonRedexElim d n
+whnfE e = case stepE e of
+               Right e'   => whnfE $ assert_smaller e e'
+               Left  done => Element e done
+
+
+public export
+Exists2 : (ty1 -> ty2 -> Type) -> Type
+Exists2 t = Exists $ Exists . t
+
+public export %inline
+some : {0 f : a -> Type} -> f x -> Exists f
+some p = Evidence _ p
+
+public export %inline
+some2 : {0 f : a -> b -> Type} -> f x y -> Exists2 f
+some2 p = some $ some p
 
-parameters {0 t : ty1 -> ty2 -> Type}
-  public export %inline some2 : t a b -> Exists2 t
-  some2 t = some $ some t
 
 ||| A term of some unknown scope sizes.
 public export