83 lines
1.9 KiB
Idris
83 lines
1.9 KiB
Idris
|
module Quox.Syntax.Term.Split
|
||
|
|
|
||
|
|
import Quox.Syntax.Term.Base
|
||
|
|
import Quox.Syntax.Term.Subst
|
||
|
|
|
||
|
|
import Data.So
|
||
|
|
import Data.Vect
|
||
|
|
|
||
|
|
%default total
|
||
|
|
|
||
|
|
|
||
|
|
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
|
||
|
|
|
||
|
|
export
|
||
|
|
getArgs' : Elim d n -> List (Term d n) -> GetArgs d n
|
||
|
|
getArgs' fun args with (choose $ isApp fun)
|
||
|
|
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 -> 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 $ TUsed $ 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 s@(Lam x body) | Left yes =
|
||
|
|
let inner = getLams $ assert_smaller s $ fromScopeTerm body 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}
|