quox/lib/Quox/Syntax/Term/Split.idr

198 lines
4.5 KiB
Idris
Raw Normal View History

2022-04-23 18:21:30 -04:00
module Quox.Syntax.Term.Split
import Quox.Syntax.Term.Base
import Quox.Syntax.Term.Subst
2023-02-11 12:14:12 -05:00
import public Quox.No
import public Data.Vect
2022-04-23 18:21:30 -04:00
%default total
public export %inline
2023-01-22 21:39:46 -05:00
isLam : Term {} -> Bool
2023-02-22 01:40:19 -05:00
isLam (Lam _) = True
isLam _ = False
2022-04-23 18:21:30 -04:00
2023-01-20 20:34:28 -05:00
public export
0 NotLam : Pred $ Term {}
2023-01-22 21:39:46 -05:00
NotLam = No . isLam
2022-04-23 18:21:30 -04:00
2023-01-20 20:34:28 -05:00
public export %inline
2023-01-22 21:39:46 -05:00
isDLam : Term {} -> Bool
2023-02-22 01:40:19 -05:00
isDLam (DLam _) = True
isDLam _ = False
2023-01-20 20:34:28 -05:00
public export
0 NotDLam : Pred $ Term {}
2023-01-22 21:39:46 -05:00
NotDLam = No . isDLam
2023-01-20 20:34:28 -05:00
2023-01-26 13:54:46 -05:00
public export %inline
isPair : Term {} -> Bool
isPair (Pair {}) = True
isPair _ = False
public export
0 NotPair : Pred $ Term {}
NotPair = No . isPair
2022-04-23 18:21:30 -04:00
public export %inline
2023-01-22 21:39:46 -05:00
isApp : Elim {} -> Bool
isApp (_ :@ _) = True
isApp _ = False
2022-04-23 18:21:30 -04:00
public export
2023-01-20 20:34:28 -05:00
0 NotApp : Pred $ Elim {}
2023-01-22 21:39:46 -05:00
NotApp = No . isApp
2022-04-23 18:21:30 -04:00
2023-01-20 20:34:28 -05:00
public export %inline
2023-01-22 21:39:46 -05:00
isDApp : Elim {} -> Bool
isDApp (_ :% _) = True
isDApp _ = False
2023-01-20 20:34:28 -05:00
public export
0 NotDApp : Pred $ Elim {}
2023-01-22 21:39:46 -05:00
NotDApp = No . isDApp
2023-01-20 20:34:28 -05:00
2022-04-23 18:21:30 -04:00
infixl 9 :@@
||| apply multiple arguments at once
public export %inline
2023-01-08 14:44:25 -05:00
(:@@) : Elim q d n -> List (Term q d n) -> Elim q d n
2022-04-23 18:21:30 -04:00
f :@@ ss = foldl (:@) f ss
public export
2023-01-08 14:44:25 -05:00
record GetArgs q d n where
2022-04-23 18:21:30 -04:00
constructor GotArgs
2023-01-08 14:44:25 -05:00
fun : Elim q d n
args : List (Term q d n)
2022-04-23 18:21:30 -04:00
0 notApp : NotApp fun
export
2023-01-08 14:44:25 -05:00
getArgs' : Elim q d n -> List (Term q d n) -> GetArgs q d n
2023-01-22 21:39:46 -05:00
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}
2022-04-23 18:21:30 -04:00
||| splits an application into its head and arguments. if it's not an
||| application then the list is just empty
export %inline
2023-01-08 14:44:25 -05:00
getArgs : Elim q d n -> GetArgs q d n
2022-04-23 18:21:30 -04:00
getArgs e = getArgs' e []
2023-01-20 20:34:28 -05:00
infixl 9 :%%
||| apply multiple dimension arguments at once
public export %inline
(:%%) : Elim q d n -> List (Dim d) -> Elim q d n
f :%% ss = foldl (:%) f ss
public export
record GetDArgs q d n where
constructor GotDArgs
fun : Elim q d n
args : List (Dim d)
0 notDApp : NotDApp fun
export
getDArgs' : Elim q d n -> List (Dim d) -> GetDArgs q d n
2023-01-22 21:39:46 -05:00
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}
2023-01-20 20:34:28 -05:00
||| splits a dimension application into its head and arguments. if it's not an
||| d application then the list is just empty
export %inline
getDArgs : Elim q d n -> GetDArgs q d n
getDArgs e = getDArgs' e []
2022-04-23 18:21:30 -04:00
infixr 1 :\\
public export
2023-02-22 01:40:19 -05:00
absN : Vect m BaseName -> Term q d (m + n) -> Term q d n
2023-01-08 14:44:25 -05:00
absN {m = 0} [] s = s
2023-02-22 01:40:19 -05:00
absN {m = S m} (x :: xs) s =
Lam $ S [x] $ Y $ absN xs $ rewrite sym $ plusSuccRightSucc m n in s
2023-01-08 14:44:25 -05:00
public export %inline
2023-02-22 01:40:19 -05:00
(:\\) : Vect m BaseName -> Term q d (m + n) -> Term q d n
2023-01-08 14:44:25 -05:00
(:\\) = absN
2022-04-23 18:21:30 -04:00
2023-01-20 20:34:28 -05:00
infixr 1 :\\%
public export
2023-02-22 01:40:19 -05:00
dabsN : Vect m BaseName -> Term q (m + d) n -> Term q d n
2023-01-20 20:34:28 -05:00
dabsN {m = 0} [] s = s
2023-02-22 01:40:19 -05:00
dabsN {m = S m} (x :: xs) s =
DLam $ S [x] $ Y $ dabsN xs $ rewrite sym $ plusSuccRightSucc m d in s
2023-01-20 20:34:28 -05:00
public export %inline
2023-02-22 01:40:19 -05:00
(:\\%) : Vect m BaseName -> Term q (m + d) n -> Term q d n
2023-01-20 20:34:28 -05:00
(:\\%) = dabsN
2022-04-23 18:21:30 -04:00
public export
2023-01-08 14:44:25 -05:00
record GetLams q d n where
2022-04-23 18:21:30 -04:00
constructor GotLams
2023-01-20 20:34:28 -05:00
{0 lams, rest : Nat}
2023-02-22 01:40:19 -05:00
names : Vect lams BaseName
2023-01-08 14:44:25 -05:00
body : Term q d rest
2022-04-23 18:21:30 -04:00
0 eq : lams + n = rest
0 notLam : NotLam body
2023-01-08 14:44:25 -05:00
export
getLams' : forall lams, rest.
2023-02-22 01:40:19 -05:00
Vect lams BaseName -> Term q d rest -> (0 eq : lams + n = rest) ->
2023-01-20 20:34:28 -05:00
GetLams q d n
2023-01-22 21:39:46 -05:00
getLams' xs s Refl = case nchoose $ isLam s of
2023-02-22 01:40:19 -05:00
Left y => let Lam (S [x] body) = s in
2023-01-22 21:39:46 -05:00
getLams' (x :: xs) (assert_smaller s body.term) Refl
Right n => GotLams xs s Refl n
2023-01-08 14:44:25 -05:00
2023-01-20 20:34:28 -05:00
export %inline
2023-01-08 14:44:25 -05:00
getLams : Term q d n -> GetLams q d n
getLams s = getLams' [] s Refl
2023-01-20 20:34:28 -05:00
public export
record GetDLams q d n where
constructor GotDLams
{0 lams, rest : Nat}
2023-02-22 01:40:19 -05:00
names : Vect lams BaseName
2023-01-20 20:34:28 -05:00
body : Term q rest n
0 eq : lams + d = rest
0 notDLam : NotDLam body
export
getDLams' : forall lams, rest.
2023-02-22 01:40:19 -05:00
Vect lams BaseName -> Term q rest n -> (0 eq : lams + d = rest) ->
2023-01-26 13:54:46 -05:00
GetDLams q d n
2023-01-22 21:39:46 -05:00
getDLams' is s Refl = case nchoose $ isDLam s of
2023-02-22 01:40:19 -05:00
Left y => let DLam (S [i] body) = s in
2023-01-22 21:39:46 -05:00
getDLams' (i :: is) (assert_smaller s body.term) Refl
Right n => GotDLams is s Refl n
2023-01-20 20:34:28 -05:00
export %inline
getDLams : Term q d n -> GetDLams q d n
getDLams s = getDLams' [] s Refl
2023-01-26 13:54:46 -05:00
public export
record GetPairs q d n where
constructor GotPairs
init : List $ Term q d n
last : Term q d n
notPair : NotPair last
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