From 8447098f2899bc7162ef0a57eb5a3c20921860bc Mon Sep 17 00:00:00 2001 From: rhiannon morris Date: Sun, 26 Feb 2023 11:24:28 +0100 Subject: [PATCH] look through substitutions in Q.S.T.Split --- lib/Quox/Syntax/Term/Pretty.idr | 4 +- lib/Quox/Syntax/Term/Split.idr | 116 +++++++++++++++++++++++--------- 2 files changed, 85 insertions(+), 35 deletions(-) diff --git a/lib/Quox/Syntax/Term/Pretty.idr b/lib/Quox/Syntax/Term/Pretty.idr index 5d8e538..be3ac34 100644 --- a/lib/Quox/Syntax/Term/Pretty.idr +++ b/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 diff --git a/lib/Quox/Syntax/Term/Split.idr b/lib/Quox/Syntax/Term/Split.idr index 8c943da..dfe650e 100644 --- a/lib/Quox/Syntax/Term/Split.idr +++ b/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' [<]