rhi/quox
rhi/quox
1
0
Fork 0
Code Issues 15 Pull requests 1 Releases Wiki Activity

WIP: quantity polymorphism #44

Draft
rhi wants to merge 9 commits from qpoly into 🐉
pull from: qpoly
merge into: rhi:🐉
Conversation 0 Commits 9 Files changed 34 +2314 -1369
34 changed files with 2314 additions and 1369 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

141
lib/Quox/Context.idr
View file

@ -3,15 +3,19 @@ module Quox.Context
import Quox.Syntax.Shift
import Quox.Pretty
import Quox.Name
import Quox.NatExtra
import Quox.PrettyValExtra
import Data.DPair
import Data.Nat
import Data.Singleton
import Quox.SingletonExtra
import Data.SnocList
import Data.SnocVect
import Data.Vect
import Control.Monad.Identity
import Derive.Prelude
%language ElabReflection
%default total
@ -45,6 +49,10 @@ public export
BContext : Nat -> Type
BContext = Context' BindName
public export
BTelescope : Nat -> Nat -> Type
BTelescope = Telescope' BindName
public export
unsnoc : Context tm (S n) -> (Context tm n, tm n)
@ -109,21 +117,31 @@ fromSnocVect [<] = [<]
fromSnocVect (sx :< x) = fromSnocVect sx :< x
public export
tabulateLT : (n : Nat) -> ((i : Nat) -> (0 p : i `LT` n) => tm i) ->
Context tm n
tabulateLT 0 f = [<]
tabulateLT (S k) f =
tabulateLT k (\i => f i @{lteSuccRight %search}) :< f k @{reflexive}
export
tabulateVar : (n : Nat) -> (Var n -> a) -> Context' a n
tabulateVar 0 f = [<]
tabulateVar (S k) f = tabulateVar k (f . VS) :< f VZ
public export
tabulate : ((n : Nat) -> tm n) -> (n : Nat) -> Context tm n
tabulate f n = tabulateLT n (\i => f i)
-- [todo] fixup argument order lol
export
allVars : (n : Nat) -> Context' (Var n) n
allVars n = tabulateVar n id
public export
replicate : (n : Nat) -> a -> Context' a n
replicate n x = tabulate (const x) n
replicate n x = tabulateVar n $ const x
public export
replicateLTE : from `LTE'` to => a -> Telescope' a from to
replicateLTE @{LTERefl} x = [<]
replicateLTE @{LTESuccR _} x = replicateLTE x :< x
public export
replicateTel : (from, to : Nat) -> a ->
Either (from `GT` to) (Telescope' a from to)
replicateTel from to x = case isLTE' from to of
Yes lte => Right $ replicateLTE x
No nlte => Left $ notLTEImpliesGT $ nlte . fromLTE
public export
@ -278,12 +296,16 @@ lengthPrf [<] = Element 0 Refl
lengthPrf (tel :< _) =
let len = lengthPrf tel in Element (S len.fst) (cong S len.snd)
export
public export
lengthPrfSing : Telescope _ from to -> Singleton from -> Singleton to
lengthPrfSing tel (Val from) =
let Element len prf = lengthPrf tel in
rewrite sym prf in
Val (len + from)
public export
lengthPrf0 : Context _ to -> Singleton to
lengthPrf0 ctx =
let Element len prf = lengthPrf ctx in
rewrite sym prf `trans` plusZeroRightNeutral len in
[|len|]
lengthPrf0 ctx = lengthPrfSing ctx (Val 0)
public export %inline
length : Telescope {} -> Nat
@ -330,14 +352,30 @@ export %inline
(forall n. Eq (tm n)) => Eq (Telescope tm from to) where
(==) = foldLazy @{All} .: zipWithLazy (==)
export %inline
(forall n. DecEq (tm n)) => DecEq (Telescope tm from to) where
decEq [<] [<] = Yes Refl
decEq (xs :< x) (ys :< y) = do
let Yes Refl = decEq xs ys
| No n => No $ \case Refl => n Refl
let Yes Refl = decEq x y
| No n => No $ \case Refl => n Refl
Yes Refl
decEq [<] (_ :< _) = No $ \case _ impossible
decEq (_ :< _) [<] = No $ \case _ impossible
export %inline
(forall n. Ord (tm n)) => Ord (Telescope tm from to) where
compare = foldLazy .: zipWithLazy compare
export %inline
(forall n. Show (tm n)) => Show (Telescope tm from to) where
showPrec d = showPrec d . toSnocList
where Show (Exists tm) where showPrec d t = showPrec d t.snd
showPrec d = showPrec d . toSnocList where
Show (Exists tm) where showPrec d t = showPrec d t.snd
export %inline
(forall n. PrettyVal (tm n)) => PrettyVal (Telescope tm from to) where
prettyVal xs = prettyVal $ toSnocList' $ map prettyVal xs
parameters {opts : LayoutOpts} {0 tm : Nat -> Type}
@ -364,5 +402,68 @@ parameters {opts : LayoutOpts} {0 tm : Nat -> Type}
namespace BContext
export
toNames : BContext n -> SnocList BaseName
toNames : BTelescope {} -> SnocList BaseName
toNames = foldl (\xs, x => xs :< x.val) [<]
public export
record NameContexts q d n where
constructor MkNameContexts
{auto qtyLen : Singleton q}
{auto dimLen : Singleton d}
{auto termLen : Singleton n}
qnames : BContext q
dnames : BContext d
tnames : BContext n
%runElab deriveIndexed "NameContexts" [Show]
namespace NameContexts
export
MkNameContexts' : (qnames : BContext q) -> (dnames : BContext d) ->
(tnames : BContext n) -> NameContexts q d n
MkNameContexts' {qnames, dnames, tnames} =
MkNameContexts {
qnames, dnames, tnames,
qtyLen = lengthPrf0 qnames,
dimLen = lengthPrf0 dnames,
termLen = lengthPrf0 tnames
}
export
fromQNames : BContext q -> NameContexts q 0 0
fromQNames qnames =
MkNameContexts qnames [<] [<] {qtyLen = lengthPrf0 qnames}
export %inline
empty : NameContexts 0 0 0
empty = fromQNames [<]
export
extendQtyN' : BTelescope q q' -> NameContexts q d n -> NameContexts q' d n
extendQtyN' xs = {qnames $= (. xs), qtyLen $= lengthPrfSing xs}
export
extendDimN' : BTelescope d d' -> NameContexts q d n -> NameContexts q d' n
extendDimN' xs = {dnames $= (. xs), dimLen $= lengthPrfSing xs}
export
extendDimN : {s : Nat} -> BContext s ->
NameContexts q d n -> NameContexts q (s + d) n
extendDimN xs = {dnames $= (++ toSnocVect' xs), dimLen $= map (s +)}
export
extendDim : BindName -> NameContexts q d n -> NameContexts q (S d) n
extendDim i = extendDimN [< i]
export
extendTermN' : BTelescope n n' -> NameContexts q d n -> NameContexts q d n'
extendTermN' xs = {tnames $= (. xs), termLen $= lengthPrfSing xs}
export
extendTermN : {s : Nat} -> BContext s ->
NameContexts q d n -> NameContexts q d (s + n)
extendTermN xs = {tnames $= (++ toSnocVect' xs), termLen $= map (s +)}
export
extendTerm : BindName -> NameContexts q d n -> NameContexts q d (S n)
extendTerm x = extendTermN [< x]

6
lib/Quox/Decidable.idr
View file

@ -47,6 +47,12 @@ Yes _ && No n2 = No $ n2 . snd
No n1 && _ = No $ n1 . fst
public export
map : p <=> q -> Dec p -> Dec q
map (MkEquivalence l r) (Yes y) = Yes $ l y
map (MkEquivalence l r) (No n) = No $ n . r
public export
reflectToDec : p `Reflects` b -> Dec p
reflectToDec (RTrue y) = Yes y

97
lib/Quox/Definition.idr
View file

@ -12,14 +12,16 @@ import Decidable.Decidable
public export
data DefBody =
Concrete (Term 0 0)
| Postulate
data DefBody : (q : Nat) -> Type where
MonoDef : Term 0 0 0 -> DefBody 0
PolyDef : (0 nz : IsSucc q) => Term q 0 0 -> DefBody q
Postulate : DefBody q
namespace DefBody
public export
(.term0) : DefBody -> Maybe (Term 0 0)
(Concrete t).term0 = Just t
(.term0) : DefBody q -> Maybe (Term q 0 0)
(MonoDef t).term0 = Just t
(PolyDef t).term0 = Just t
(Postulate).term0 = Nothing
@ -27,59 +29,76 @@ public export
record Definition where
constructor MkDef
qty : GQty
type0 : Term 0 0
body0 : DefBody
{qlen : Nat}
qargs : BContext qlen
type0 : Term qlen 0 0
body0 : DefBody qlen
scheme : Maybe String
isMain : Bool
loc_ : Loc
public export %inline
mkPostulate : GQty -> (type0 : Term 0 0) -> Maybe String -> Bool -> Loc ->
Definition
mkPostulate qty type0 scheme isMain loc_ =
MkDef {qty, type0, body0 = Postulate, scheme, isMain, loc_}
mkPostulate : GQty -> BContext q -> Term q 0 0 ->
Maybe String -> Bool -> Loc -> Definition
mkPostulate qty qargs type0 scheme isMain loc_ =
let Val q = lengthPrf0 qargs in
MkDef {qty, qargs, type0, body0 = Postulate, scheme, isMain, loc_}
public export %inline
mkDef : GQty -> (type0, term0 : Term 0 0) -> Maybe String -> Bool -> Loc ->
Definition
mkDef qty type0 term0 scheme isMain loc_ =
MkDef {qty, type0, body0 = Concrete term0, scheme, isMain, loc_}
mkDef : GQty -> BContext q -> (type0, term0 : Term q 0 0) -> Maybe String ->
Bool -> Loc -> Definition
mkDef qty qargs type0 term0 scheme isMain loc_ =
case (lengthPrf0 qargs) of
Val 0 =>
MkDef {qty, qargs, type0, body0 = MonoDef term0, scheme, isMain, loc_}
Val (S _) =>
MkDef {qty, qargs, type0, body0 = PolyDef term0, scheme, isMain, loc_}
export Located Definition where def.loc = def.loc_
export Relocatable Definition where setLoc loc = {loc_ := loc}
public export
record Poly (0 tm : TermLike) d n where
constructor P
qlen : Nat
type : tm qlen d n
parameters {d, n : Nat}
public export %inline
(.type) : Definition -> Term d n
g.type = g.type0 // shift0 d // shift0 n
(.type) : Definition -> Poly Term d n
def.type = P def.qlen $ def.type0 // shift0 d // shift0 n
public export %inline
(.typeAt) : Definition -> Universe -> Term d n
g.typeAt u = displace u g.type
(.typeAt) : Definition -> Universe -> Poly Term d n
def.typeAt u = {type $= displace u} def.type
public export %inline
(.term) : Definition -> Maybe (Term d n)
g.term = g.body0.term0 <&> \t => t // shift0 d // shift0 n
(.term) : Definition -> Maybe (Poly Term d n)
def.term = def.body0.term0 <&> \t => P def.qlen $ t // shift0 d // shift0 n
public export %inline
(.termAt) : Definition -> Universe -> Maybe (Term d n)
g.termAt u = displace u <$> g.term
(.termAt) : Definition -> Universe -> Maybe (Poly Term d n)
def.termAt u = {type $= displace u} <$> def.term
public export %inline
toElim : Definition -> Universe -> Maybe $ Elim d n
toElim def u = pure $ Ann !(def.termAt u) (def.typeAt u) def.loc
toElim : Definition -> Universe -> Maybe (Poly Elim d n)
toElim def u = do
tm <- def.body0.term0; let ty = def.type0
pure $ P def.qlen $ Ann tm ty def.loc // shift0 d // shift0 n
public export
(.typeWith) : Definition -> Singleton d -> Singleton n -> Term d n
g.typeWith (Val d) (Val n) = g.type
(.typeWith) : Definition -> Singleton d -> Singleton n -> Poly Term d n
def.typeWith (Val d) (Val n) = def.type
public export
(.typeWithAt) : Definition -> Singleton d -> Singleton n -> Universe -> Term d n
g.typeWithAt d n u = displace u $ g.typeWith d n
(.typeWithAt) : Definition -> Singleton d -> Singleton n ->
Universe -> Poly Term d n
def.typeWithAt (Val d) (Val n) u = def.typeAt u
public export
(.termWith) : Definition -> Singleton d -> Singleton n -> Maybe (Term d n)
(.termWith) : Definition -> Singleton d -> Singleton n -> Maybe (Poly Term d n)
g.termWith (Val d) (Val n) = g.term
@ -108,20 +127,28 @@ DefsState : Type -> Type
DefsState = StateL DEFS Definitions
public export %inline
lookupElim : {d, n : Nat} -> Name -> Universe -> Definitions -> Maybe (Elim d n)
lookupElim : {d, n : Nat} ->
Name -> Universe -> Definitions -> Maybe (Poly Elim d n)
lookupElim x u defs = toElim !(lookup x defs) u
public export %inline
lookupElim0 : Name -> Universe -> Definitions -> Maybe (Elim 0 0)
lookupElim0 : Name -> Universe -> Definitions -> Maybe (Poly Elim 0 0)
lookupElim0 = lookupElim
export
prettyQBinders : {opts : LayoutOpts} -> BContext q -> Eff Pretty (Doc opts)
prettyQBinders [<] = pure empty
prettyQBinders qnames =
qbrackets . separateTight !commaD =<< traverse prettyQBind (toList' qnames)
export
prettyDef : {opts : LayoutOpts} -> Name -> Definition -> Eff Pretty (Doc opts)
prettyDef name def = withPrec Outer $ do
qty <- prettyQty def.qty.qty
qty <- prettyQConst def.qty.qconst
dot <- dotD
name <- prettyFree name
qargs <- prettyQBinders def.qargs
colon <- colonD
type <- prettyTerm [<] [<] def.type
hangDSingle (hsep [hcat [qty, dot, name], colon]) type
type <- prettyTerm (fromQNames def.qargs) def.type0
hangDSingle (hsep [hcat [qty, dot, name, qargs], colon]) type

16
lib/Quox/Displace.idr
View file

@ -7,12 +7,12 @@ import Quox.Syntax
parameters (k : Universe)
namespace Term
export doDisplace : Term d n -> Term d n
export doDisplaceS : ScopeTermN s d n -> ScopeTermN s d n
export doDisplaceDS : DScopeTermN s d n -> DScopeTermN s d n
export doDisplace : Term q d n -> Term q d n
export doDisplaceS : ScopeTermN s q d n -> ScopeTermN s q d n
export doDisplaceDS : DScopeTermN s q d n -> DScopeTermN s q d n
namespace Elim
export doDisplace : Elim d n -> Elim d n
export doDisplace : Elim q d n -> Elim q d n
namespace Term
doDisplace (TYPE l loc) = TYPE (k + l) loc
@ -41,6 +41,8 @@ parameters (k : Universe)
CloT (Sub (doDisplace t) (assert_total $ map doDisplace th))
doDisplace (DCloT (Sub t th)) =
DCloT (Sub (doDisplace t) th)
doDisplace (QCloT (SubR t th)) =
QCloT (SubR (doDisplace t) th)
doDisplaceS (S names (Y body)) = S names $ Y $ doDisplace body
doDisplaceS (S names (N body)) = S names $ N $ doDisplace body
@ -80,16 +82,18 @@ parameters (k : Universe)
CloE (Sub (doDisplace e) (assert_total $ map doDisplace th))
doDisplace (DCloE (Sub e th)) =
DCloE (Sub (doDisplace e) th)
doDisplace (QCloE (SubR e th)) =
QCloE (SubR (doDisplace e) th)
namespace Term
export
displace : Universe -> Term d n -> Term d n
displace : Universe -> Term q d n -> Term q d n
displace 0 t = t
displace u t = doDisplace u t
namespace Elim
export
displace : Universe -> Elim d n -> Elim d n
displace : Universe -> Elim q d n -> Elim q d n
displace 0 t = t
displace u t = doDisplace u t

49
lib/Quox/FreeVars.idr
View file

@ -62,7 +62,7 @@ export %inline [AndM] {n : Nat} -> Monoid (FreeVars n) where neutral = all
private
self : {n : Nat} -> Context' (FreeVars n) n
self = tabulate (\i => FV $ tabulate (== i) n) n
self = tabulateVar n $ \i => FV $ tabulateVar n (== i)
export
shift : forall from, to. Shift from to -> FreeVars from -> FreeVars to
@ -74,13 +74,12 @@ shift by (FV xs) = FV $ shift' by xs where
export
fromSet : {n : Nat} -> SortedSet (Var n) -> FreeVars n
fromSet vs = FV $ tabulateLT n $ \i => contains (V i) vs
fromSet vs = FV $ tabulateVar n $ \i => contains i vs
export
toSet : {n : Nat} -> FreeVars n -> SortedSet (Var n)
toSet (FV vs) =
foldl_ (\s, i => maybe s (\i => insert i s) i) empty $
zipWith (\i, b => guard b $> i) (tabulateLT n V) vs
toSet (FV vs) = SortedSet.fromList $ fold $
Context.zipWith (\i, b => i <$ guard b) (allVars n) vs
public export
@ -89,7 +88,7 @@ interface HasFreeVars (0 tm : Nat -> Type) where
fv : {n : Nat} -> tm n -> FreeVars n
public export
interface HasFreeDVars (0 tm : TermLike) where
interface HasFreeDVars (0 tm : Nat -> Nat -> Type) where
constructor HFDV
fdv : {d, n : Nat} -> tm d n -> FreeVars d
@ -102,7 +101,7 @@ fdvWith : HasFreeDVars tm => Singleton d -> Singleton n -> tm d n -> FreeVars d
fdvWith (Val d) (Val n) = fdv
export
Fdv : (0 tm : TermLike) -> {n : Nat} ->
Fdv : (0 tm : _) -> {n : Nat} ->
HasFreeDVars tm => HasFreeVars (\d => tm d n)
Fdv tm @{HFDV fdv} = HFV fdv
@ -140,7 +139,7 @@ where
fdv (S _ (N body)) = fdv body
export
fvD : {0 tm : TermLike} -> {n : Nat} -> (forall d. HasFreeVars (tm d)) =>
fvD : {0 tm : _} -> {n : Nat} -> (forall d. HasFreeVars (tm d)) =>
Scoped s (\d => tm d n) d -> FreeVars n
fvD (S _ (Y body)) = fv body
fvD (S _ (N body)) = fv body
@ -175,11 +174,10 @@ where
foldMap (uncurry guardM) (zipWith (,) (fv term).vars (fdvEach subst))
export HasFreeVars (Term d)
export HasFreeVars (Elim d)
export HasFreeVars (Term q d)
export HasFreeVars (Elim q d)
export
HasFreeVars (Term d) where
HasFreeVars (Term q d) where
fv (TYPE {}) = none
fv (IOState {}) = none
fv (Pi {arg, res, _}) = fv arg <+> fv res
@ -201,9 +199,9 @@ HasFreeVars (Term d) where
fv (E e) = fv e
fv (CloT s) = fv s
fv (DCloT s) = fv s.term
fv (QCloT s) = fv s.term
export
HasFreeVars (Elim d) where
HasFreeVars (Elim q d) where
fv (F {}) = none
fv (B i _) = only i
fv (App {fun, arg, _}) = fv fun <+> fv arg
@ -225,12 +223,13 @@ HasFreeVars (Elim d) where
fv ty <+> fv ret <+> fv def <+> foldMap (\x => fv x.snd) (toList arms)
fv (CloE s) = fv s
fv (DCloE s) = fv s.term
fv (QCloE s) = fv s.term
private
expandDShift : {d1 : Nat} -> Shift d1 d2 -> Loc -> Context' (Dim d2) d1
expandDShift by loc = tabulateLT d1 (\i => BV i loc // by)
expandDShift by loc = tabulateVar d1 (\i => B i loc // by)
private
expandDSubst : {d1 : Nat} -> DSubst d1 d2 -> Loc -> Context' (Dim d2) d1
@ -254,11 +253,10 @@ fdvSubst : {d, n : Nat} -> (Located2 tm, HasFreeDVars tm) =>
fdvSubst (Sub t th) = let Val from = getFrom th in fdvSubst' t th
export HasFreeDVars Term
export HasFreeDVars Elim
export HasFreeDVars (Term q)
export HasFreeDVars (Elim q)
export
HasFreeDVars Term where
HasFreeDVars (Term q) where
fdv (TYPE {}) = none
fdv (IOState {}) = none
fdv (Pi {arg, res, _}) = fdv arg <+> fdvT res
@ -280,9 +278,9 @@ HasFreeDVars Term where
fdv (E e) = fdv e
fdv (CloT s) = fdv s @{WithSubst}
fdv (DCloT s) = fdvSubst s
fdv (QCloT s) = fdv s.term
export
HasFreeDVars Elim where
HasFreeDVars (Elim q) where
fdv (F {}) = none
fdv (B {}) = none
fdv (App {fun, arg, _}) = fdv fun <+> fdv arg
@ -299,12 +297,13 @@ HasFreeDVars Elim where
fdv fun <+> fv arg
fdv (Ann {tm, ty, _}) =
fdv tm <+> fdv ty
fdv (Coe {ty, p, q, val, _}) =
fdv @{DScope} ty <+> fv p <+> fv q <+> fdv val
fdv (Comp {ty, p, q, val, r, zero, one, _}) =
fdv ty <+> fv p <+> fv q <+> fdv val <+>
fdv (Coe {ty, p, p', val, _}) =
fdv @{DScope} ty <+> fv p <+> fv p' <+> fdv val
fdv (Comp {ty, p, p', val, r, zero, one, _}) =
fdv ty <+> fv p <+> fv p' <+> fdv val <+>
fv r <+> fdv @{DScope} zero <+> fdv @{DScope} one
fdv (TypeCase {ty, ret, arms, def, _}) =
fdv ty <+> fdv ret <+> fdv def <+> foldMap (\x => fdvT x.snd) (toList arms)
fdv (CloE s) = fdv s @{WithSubst}
fdv (DCloE s) = fdvSubst s
fdv (QCloE s) = fdv s.term

16
lib/Quox/Loc.idr
View file

@ -125,7 +125,9 @@ extendOr l1 l2 = (l1 `extendL` l2) `or` l2
public export
interface Located a where (.loc) : a -> Loc
interface Located a where
constructor MkLocated
(.loc) : a -> Loc
public export
0 Located1 : (a -> Type) -> Type
@ -136,7 +138,13 @@ public export
Located2 f = forall x, y. Located (f x y)
public export
interface Located a => Relocatable a where setLoc : Loc -> a -> a
0 Located3 : (a -> b -> c -> Type) -> Type
Located3 f = forall x, y, z. Located (f x y z)
public export
interface Located a => Relocatable a where
constructor MkRelocatable
setLoc : Loc -> a -> a
public export
0 Relocatable1 : (a -> Type) -> Type
@ -146,6 +154,10 @@ public export
0 Relocatable2 : (a -> b -> Type) -> Type
Relocatable2 f = forall x, y. Relocatable (f x y)
public export
0 Relocatable3 : (a -> b -> c -> Type) -> Type
Relocatable3 f = forall x, y, z. Relocatable (f x y z)
export
locs : Located a => Foldable t => t a -> Loc

40
lib/Quox/NatExtra.idr
View file

@ -5,6 +5,7 @@ import Data.Nat.Division
import Data.SnocList
import Data.Vect
import Data.String
import Quox.Decidable
%default total
@ -14,26 +15,53 @@ data LTE' : Nat -> Nat -> Type where
LTERefl : LTE' n n
LTESuccR : LTE' m n -> LTE' m (S n)
%builtin Natural LTE'
%name LTE' p, q
public export %hint
lteZero' : {n : Nat} -> LTE' 0 n
lteZero' {n = 0} = LTERefl
lteZero' {n = S n} = LTESuccR lteZero'
%transform "NatExtra.lteZero'" lteZero' {n} = believe_me n
public export %hint
lteSucc' : LTE' m n -> LTE' (S m) (S n)
lteSucc' LTERefl = LTERefl
lteSucc' (LTESuccR p) = LTESuccR $ lteSucc' p
%transform "NatExtra.lteSucc'" lteSucc' p = believe_me p
public export
fromLte : {n : Nat} -> LTE m n -> LTE' m n
fromLte LTEZero = lteZero'
fromLte (LTESucc p) = lteSucc' $ fromLte p
fromLTE : {n : Nat} -> LTE m n -> LTE' m n
fromLTE LTEZero = lteZero'
fromLTE (LTESucc p) = lteSucc' $ fromLTE p
-- %transform "NatExtra.fromLTE"
-- fromLTE {n} p = believe_me (n `minus` believe_me p)
public export
toLte : {n : Nat} -> m `LTE'` n -> m `LTE` n
toLte LTERefl = reflexive
toLte (LTESuccR p) = lteSuccRight (toLte p)
toLTE : {m : Nat} -> m `LTE'` n -> m `LTE` n
toLTE LTERefl = reflexive
toLTE (LTESuccR p) = lteSuccRight (toLTE p)
-- %transform "NatExtra.toLTE" toLTE {m} p = believe_me m
public export
lteLTE' : {m, n : Nat} -> LTE m n <=> LTE' m n
lteLTE' = MkEquivalence fromLTE toLTE
public export
isLTE' : (m, n : Nat) -> Dec (LTE' m n)
isLTE' m n = map lteLTE' $ isLTE m n
public export
data LT' : Nat -> Nat -> Type where
LTZero : LT' 0 (S n)
LTSucc : LT' m n -> LT' (S m) (S n)
%builtin Natural LT'
%name LT' p, q
public export
Transitive Nat LT' where
transitive LTZero (LTSucc q) = LTZero
transitive (LTSucc p) (LTSucc q) = LTSucc $ transitive p q
private

4
lib/Quox/No.idr
View file

@ -13,6 +13,10 @@ data No : Pred Bool where
export Uninhabited (No True) where uninhabited _ impossible
export Eq (No p) where _ == _ = True
export Ord (No p) where compare _ _ = EQ
export Show (No p) where showPrec _ _ = "Ah"
export %inline
soNo : So b -> No b -> Void
soNo Oh Ah impossible

2
lib/Quox/OPE.idr
View file

@ -50,7 +50,7 @@ dropInner' (LTESuccR p) = Drop $ dropInner' $ force p
public export
dropInner : {n : Nat} -> LTE m n -> OPE m n
dropInner = dropInner' . fromLte
dropInner = dropInner' . fromLTE
public export
dropInnerN : (m : Nat) -> OPE n (m + n)

189
lib/Quox/Polynomial.idr Normal file
View file

@ -0,0 +1,189 @@
module Quox.Polynomial
import public Quox.Syntax.Subst
import public Quox.Context
import public Quox.Semiring
import Data.Maybe
import Data.SortedMap
import Data.Singleton
import Quox.PrettyValExtra
%default total
%hide Prelude.toList
public export
Monom : Nat -> Type
Monom = Context' Nat
export %inline
mZero : {n : Nat} -> Monom n
mZero = replicate n 0
export %inline
mIsZero : Monom n -> Bool
mIsZero = all (== 0)
private
PolyBody : Type -> Nat -> Type
PolyBody coeff scope = SortedMap (Monom scope) coeff
private %inline
getScope : PolyBody coeff scope -> Maybe (Singleton scope)
getScope p = lengthPrf0 . fst <$> leftMost p
export
data Polynomial : (coeff : Type) -> (scope : Nat) -> Type where
Const : (k : coeff) -> Polynomial coeff scope
Many : (p : PolyBody coeff scope) -> Polynomial coeff scope
%name Polynomial p, q
-- the Const constructor exists so that `pconst` (and by extension, `one`, and
-- the TimesMonoid instance) doesn't need to know the scope size
export %inline
toConst' : List (Monom scope, coeff) -> Maybe coeff
toConst' [(m, k)] = k <$ guard (mIsZero m)
toConst' _ = Nothing
export %inline
toConst : PolyBody coeff scope -> Maybe coeff
toConst = toConst' . toList
export %inline
toTrimmedList : AddMonoid v => SortedMap k v -> List (k, v)
toTrimmedList = List.filter (not . isZero . snd) . toList
export %inline
toList : {scope : Nat} -> AddMonoid coeff =>
Polynomial coeff scope -> List (Monom scope, coeff)
toList (Const k) = [(mZero, k)]
toList (Many p) = toTrimmedList p
private %inline
addBody : AddMonoid coeff =>
PolyBody coeff scope -> PolyBody coeff scope -> PolyBody coeff scope
addBody = mergeWith (+.)
export %inline
fromList : AddMonoid coeff =>
List (Monom scope, coeff) -> Polynomial coeff scope
fromList xs = case toConst' xs of
Just k => Const k
Nothing => Many $ foldl add1 empty xs
where
add1 : PolyBody coeff scope -> (Monom scope, coeff) -> PolyBody coeff scope
add1 p (x, k) = p `addBody` singleton x k
export %inline
(AddMonoid coeff, Eq coeff) => Eq (Polynomial coeff scope) where
Const x == Const y = x == y
Const x == Many q = maybe False (== x) $ toConst q
Many p == Const y = maybe False (== y) $ toConst p
Many p == Many q = toTrimmedList p == toTrimmedList q
export %inline
(AddMonoid coeff, Ord coeff) => Ord (Polynomial coeff scope) where
compare (Const x) (Const y) = compare x y
compare (Const x) (Many q) = maybe LT (compare x) $ toConst q
compare (Many p) (Const y) = maybe GT (flip compare y) $ toConst p
compare (Many p) (Many q) = compare (toTrimmedList p) (toTrimmedList q)
export %inline
{scope : Nat} -> (AddMonoid coeff, Show coeff) =>
Show (Polynomial coeff scope) where
showPrec d p = showCon d "fromList" $ showArg (toList p)
export %inline
{scope : Nat} -> (AddMonoid coeff, PrettyVal coeff) =>
PrettyVal (Polynomial coeff scope) where
prettyVal p = Con "fromList" [prettyVal $ toList p]
export %inline
pconst : a -> Polynomial a n
pconst = Const
export %inline
(.at) : AddMonoid a => Polynomial a n -> Monom n -> a
(Const k).at m = if mIsZero m then k else zero
(Many p).at m = fromMaybe zero $ lookup m p
export %inline
(.at0) : AddMonoid a => Polynomial a n -> a
(Const k).at0 = k
(Many p).at0 = fromMaybe zero $ do
(m, k) <- leftMost p
guard $ mIsZero m
pure k
private %inline
addConstMany : AddMonoid coeff =>
coeff -> PolyBody coeff scope -> Polynomial coeff scope
addConstMany k p = case getScope p of
Nothing => Const k
Just (Val _) => Many $ p `addBody` singleton mZero k
export %inline
AddMonoid a => AddMonoid (Polynomial a n) where
zero = Const zero
isZero (Const k) = isZero k
isZero (Many p) = maybe False isZero $ toConst p
Const j +. Const k = Const $ j +. k
Const j +. Many q = addConstMany j q
Many p +. Const k = addConstMany k p
Many p +. Many q = Many $ p `addBody` q
export %inline
Semiring a => TimesMonoid (Polynomial a n) where
one = pconst one
Const j *. Const k = Const $ j *. k
Const j *. Many q = Many $ map (j *.) q
Many p *. Const k = Many $ map (*. k) p
Many p *. Many q = fromList $ do
(xs, i) <- toList p
(ys, j) <- toList q
let k = i *. j
guard $ not $ isZero k
pure (zipWith (+) xs ys, i *. j)
export %inline
Semiring a => VecSpace a (Polynomial a n) where
x *: xs = Const x *. xs
private
shiftMonom : Shift from to -> Monom from -> Monom to
shiftMonom SZ m = m
shiftMonom (SS by) m = shiftMonom by m :< 0
export
CanShift (Polynomial coeff) where
Const k // _ = Const k
Many p // by =
let xs = mapFst (shiftMonom by) <$> toList p in
Many $ fromList xs
export
TimesMonoid a => FromVarR (Polynomial a) where
fromVarR i l {n} =
let m = tabulateVar n $ \j => if i == j then 1 else 0 in
Many $ singleton m one
private
substMonom : Semiring a => {from, to : Nat} ->
Subst (Polynomial a) from to -> Monom from -> a -> Polynomial a to
substMonom th m k = sproduct {init = pconst k} $
zipWith (\i, p => getR th i noLoc ^. p) (allVars from) m
export
Semiring a => CanSubstSelfR (Polynomial a) where
Const k //? _ = Const k
Many p //? th = ssum $ map (uncurry $ substMonom th) $ toList p

33
lib/Quox/Pretty.idr
View file

@ -37,9 +37,10 @@ data PPrec
public export
data HL
= Delim
| Free | TVar | TVarErr
| Dim | DVar | DVarErr
| Qty | Universe
| Free | TVar
| Dim | DVar
| Qty | QVar
| Universe
| Syntax
| Constant
%runElab derive "HL" [Eq, Ord, Show]
@ -79,11 +80,10 @@ toSGR : HL -> List SGR
toSGR Delim = []
toSGR Free = [SetForeground BrightBlue]
toSGR TVar = [SetForeground BrightYellow]
toSGR TVarErr = [SetForeground BrightYellow, SetStyle SingleUnderline]
toSGR Dim = [SetForeground BrightGreen]
toSGR DVar = [SetForeground BrightGreen]
toSGR DVarErr = [SetForeground BrightGreen, SetStyle SingleUnderline]
toSGR Qty = [SetForeground BrightMagenta]
toSGR QVar = [SetForeground BrightMagenta]
toSGR Universe = [SetForeground BrightRed]
toSGR Syntax = [SetForeground BrightCyan]
toSGR Constant = [SetForeground BrightRed]
@ -97,11 +97,10 @@ toClass : HL -> String
toClass Delim = "dl"
toClass Free = "fr"
toClass TVar = "tv"
toClass TVarErr = "tv err"
toClass Dim = "dc"
toClass DVar = "dv"
toClass DVarErr = "dv err"
toClass Qty = "qt"
toClass QVar = "qv"
toClass Universe = "un"
toClass Syntax = "sy"
toClass Constant = "co"
@ -209,6 +208,10 @@ parameters {opts : LayoutOpts} {auto _ : Foldable t}
separateTight : Doc opts -> t (Doc opts) -> Doc opts
separateTight d = sep . exceptLast (<+> d) . toList
export
sepSingleTight : Doc opts -> t (Doc opts) -> Doc opts
sepSingleTight d = sepSingle . exceptLast (<+> d) . toList
export
hseparateTight : Doc opts -> t (Doc opts) -> Doc opts
hseparateTight d = hsep . exceptLast (<+> d) . toList
@ -242,6 +245,10 @@ export %inline
withPrec : PPrec -> Eff Pretty a -> Eff Pretty a
withPrec = localAt_ PREC
export %inline
qbrackets : {opts : LayoutOpts} -> Doc opts -> Eff Pretty (Doc opts)
qbrackets doc = tightDelims !(ifUnicode "‹" ".{") !(ifUnicode "›" "}") doc
export
prettyName : Name -> Doc opts
@ -263,12 +270,16 @@ export
prettyDBind : {opts : LayoutOpts} -> BindName -> Eff Pretty (Doc opts)
prettyDBind = hl DVar . prettyBind'
export
prettyQBind : {opts : LayoutOpts} -> BindName -> Eff Pretty (Doc opts)
prettyQBind = hl QVar . prettyBind'
export %inline
typeD, ioStateD, arrowD, darrowD, timesD, lamD, eqndD, dlamD, annD, natD,
stringD, eqD, colonD, commaD, semiD, atD, caseD, typecaseD, returnD, ofD, dotD,
zeroD, succD, coeD, compD, undD, cstD, pipeD, fstD, sndD, letD, inD :
zeroD, succD, coeD, compD, undD, cstD, pipeD, fstD, sndD, letD, inD,
qplusD, qtimesD :
{opts : LayoutOpts} -> Eff Pretty (Doc opts)
typeD = hl Syntax . text =<< ifUnicode "★" "Type"
ioStateD = hl Syntax $ text "IOState"
@ -302,6 +313,8 @@ fstD = hl Syntax $ text "fst"
sndD = hl Syntax $ text "snd"
letD = hl Syntax $ text "let"
inD = hl Syntax $ text "in"
qplusD = hl Syntax $ text "+"
qtimesD = hl Syntax . text =<< ifUnicode "·" "*"
export
@ -315,7 +328,7 @@ prettyApp ind f args =
export
prettyAppD : {opts : LayoutOpts} -> Doc opts -> List (Doc opts) ->
Eff Pretty (Doc opts)
prettyAppD f args = pure $ prettyApp !(askAt INDENT) f args
prettyAppD f args = parensIfM App $ prettyApp !(askAt INDENT) f args
export
@ -345,7 +358,7 @@ prettyBounds (MkBounds l1 c1 l2 c2) =
export
prettyLoc : {opts : LayoutOpts} -> Loc -> Eff Pretty (Doc opts)
prettyLoc (L NoLoc) =
hcat <$> sequence [hl TVarErr "no location", colonD]
hcat <$> sequence [hl TVar "no location", colonD]
prettyLoc (L (YesLoc file b)) =
hcat <$> sequence [hl Free $ text file, colonD, prettyBounds b]

122
lib/Quox/Semiring.idr Normal file
View file

@ -0,0 +1,122 @@
module Quox.Semiring
import Quox.Context
import public Quox.NatExtra
import Data.Bool.Decidable
import Quox.No
%hide Nat.isZero
export infixl 8 +.
export infixl 9 *., *:, :*
export infixr 10 ^.
public export
interface AddMonoid a where
zero : a
isZero : a -> Bool
(+.) : a -> a -> a
public export
interface TimesMonoid a where
one : a
(*.) : a -> a -> a
public export
0 Semiring : Type -> Type
Semiring a = (AddMonoid a, TimesMonoid a)
public export
interface (Semiring base, AddMonoid vec) => VecSpace base vec | vec where
(*:) : base -> vec -> vec
(:*) : vec -> base -> vec
x *: xs = xs :* x
xs :* x = x *: xs
namespace Foldable
public export %inline %tcinline
ssum : AddMonoid a => Foldable t => {default zero init : a} -> t a -> a
ssum = foldl (+.) init
public export %inline %tcinline
sproduct : TimesMonoid a => Foldable t => {default one init : a} -> t a -> a
sproduct = foldl (*.) init
namespace Context
public export %inline %tcinline
ssum : AddMonoid a => {default zero init : a} ->
Telescope' a from to -> a
ssum = foldl_ (+.) zero
public export %inline %tcinline
sproduct : TimesMonoid a => {default one init : a} ->
Telescope' a from to -> a
sproduct = foldl_ (*.) one
public export
(^.) : TimesMonoid a => a -> Nat -> a
x ^. 0 = one
x ^. S k = x *. x^.k
export %inline
[NumAdd] Eq a => Num a => AddMonoid a where
zero = 0; (+.) = (+); isZero = (== 0)
export %inline
[NumTimes] Num a => TimesMonoid a where
one = 1; (*.) = (*)
export %inline %hint
NatAM : AddMonoid Nat
NatAM = NumAdd
export %inline %hint
NatTM : TimesMonoid Nat
NatTM = NumTimes
export %inline %hint
IntegerAM : AddMonoid Integer
IntegerAM = NumAdd
export %inline %hint
IntegerTM : TimesMonoid Integer
IntegerTM = NumTimes
export %inline %hint
IntAM : AddMonoid Int
IntAM = NumAdd
export %inline %hint
IntTM : TimesMonoid Int
IntTM = NumTimes
export %inline
(from `LTE'` to, AddMonoid a) => AddMonoid (Telescope' a from to) where
zero = replicateLTE zero
(+.) = zipWith (+.)
isZero = all isZero
export %inline
(from `LTE'` to, Semiring a) => VecSpace a (Telescope' a from to) where
x *: xs = map (x *.) xs
public export
interface AddMonoid a => MonoAddMonoid a where
0 zeroPlus : (x, y : a) ->
No (isZero x) -> No (isZero y) -> No (isZero (x +. y))
export
MonoAddMonoid Nat where
zeroPlus (S _) (S _) Ah Ah = Ah
public export
0 MonoAddSemiring : Type -> Type
MonoAddSemiring a = (MonoAddMonoid a, TimesMonoid a)

11
lib/Quox/SingletonExtra.idr Normal file
View file

@ -0,0 +1,11 @@
module Quox.SingletonExtra
import public Data.Singleton
public export
map : (f : a -> b) -> Singleton x -> Singleton (f x)
map f x = [|f x|]
public export
(<$>) : (f : a -> b) -> Singleton x -> Singleton (f x)
(<$>) = map

4
lib/Quox/Syntax/Builtin.idr
View file

@ -21,7 +21,7 @@ builtinDesc Main = "a function declared as #[main]"
public export
builtinTypeDoc : {opts : LayoutOpts} -> Builtin -> Eff Pretty (Doc opts)
builtinTypeDoc Main =
prettyTerm [<] [<] $
Pi One (IOState noLoc)
prettyTerm empty $
Pi {q = 0} (one noLoc) (IOState noLoc)
(SN $ Sig (Enum (fromList [!(ifUnicode "𝑎" "a")]) noLoc)
(SN (IOState noLoc)) noLoc) noLoc

18
lib/Quox/Syntax/Dim.idr
View file

@ -84,7 +84,11 @@ DSubst : Nat -> Nat -> Type
DSubst = Subst Dim
public export FromVar Dim where fromVarLoc = B
public export
FromVarR Dim where fromVarR = B
public export
FromVar Dim where fromVar = B; fromVarSame _ _ = Refl
export
@ -92,10 +96,16 @@ CanShift Dim where
K e loc // _ = K e loc
B i loc // by = B (i // by) loc
private
substDim : Dim from -> Lazy (DSubst from to) -> Dim to
substDim (K e loc) _ = K e loc
substDim (B i loc) th = get th i loc
export
CanSubstSelf Dim where
K e loc // _ = K e loc
B i loc // th = getLoc th i loc
CanSubstSelfR Dim where (//?) = substDim
export
CanSubstSelf Dim where (//) = substDim; substSame _ _ = Refl
export Uninhabited (B i loc1 = K e loc2) where uninhabited _ impossible

202
lib/Quox/Syntax/Qty.idr
View file

@ -4,10 +4,14 @@
||| it's worth in a language that has other stuff going on too
module Quox.Syntax.Qty
import public Quox.Polynomial
import Quox.Name
import Quox.Syntax.Subst
import Quox.Pretty
import Quox.Decidable
import Quox.PrettyValExtra
import Data.DPair
import Data.Singleton
import Derive.Prelude
%default total
@ -20,61 +24,124 @@ import Derive.Prelude
||| - 1: a variable is used exactly once at run time
||| - ω (or #): don't care. an ω variable *can* also be used 0/1 time
public export
data Qty = Zero | One | Any
%runElab derive "Qty" [Eq, Ord, Show, PrettyVal]
%name Qty.Qty pi, rh
data QConst = Zero | One | Any
%runElab derive "QConst" [Eq, Ord, Show, PrettyVal]
%name QConst q, r
export
prettyQty : {opts : _} -> Qty -> Eff Pretty (Doc opts)
prettyQty Zero = hl Qty $ text "0"
prettyQty One = hl Qty $ text "1"
prettyQty Any = hl Qty =<< ifUnicode (text "ω") (text "#")
prettyQConst : {opts : _} -> QConst -> Eff Pretty (Doc opts)
prettyQConst Zero = hl Qty $ text "0"
prettyQConst One = hl Qty $ text "1"
prettyQConst Any = hl Qty =<< ifUnicode (text "ω") (text "#")
||| prints in a form that can be a suffix of "case"
public export
prettySuffix : {opts : _} -> Qty -> Eff Pretty (Doc opts)
prettySuffix = prettyQty
-- ||| prints in a form that can be a suffix of "case"
-- public export
-- prettySuffix : {opts : _} -> Qty -> Eff Pretty (Doc opts)
-- prettySuffix = prettyQty
namespace QConst
||| e.g. if in the expression `(s, t)`, the variable `x` is
||| used π times in `s` and ρ times in `t`, then it's used
||| (π + ρ) times in the whole expression
public export
(+) : Qty -> Qty -> Qty
Zero + rh = rh
pi + Zero = pi
_ + _ = Any
plus : QConst -> QConst -> QConst
plus Zero rh = rh
plus pi Zero = pi
plus _ _ = Any
||| e.g. if a function `f` uses its argument π times,
||| and `f x` occurs in a σ context, then `x` is used `πσ` times overall
public export
(*) : Qty -> Qty -> Qty
Zero * _ = Zero
_ * Zero = Zero
One * rh = rh
pi * One = pi
Any * Any = Any
times : QConst -> QConst -> QConst
times Zero _ = Zero
times _ Zero = Zero
times One rh = rh
times pi One = pi
times Any Any = Any
-- ||| "π ∨ ρ"
-- |||
-- ||| returns a quantity τ with π ≤ τ and ρ ≤ τ.
-- ||| if π = ρ, then it's that, otherwise it's ω.
-- public export
-- lub : QConst -> QConst -> QConst
-- lub p q = if p == q then p else Any
export %inline
AddMonoid QConst where zero = Zero; (+.) = plus; isZero = (== Zero)
export %inline
TimesMonoid QConst where one = One; (*.) = times
public export
record Qty n where
constructor Q
value : Polynomial QConst n
loc : Loc
%runElab deriveIndexed "Qty" [Eq, Ord]
export %hint
ShowQty : {n : Nat} -> Show (Qty n)
ShowQty = deriveShow
export %hint
PrettyValQty : {n : Nat} -> PrettyVal (Qty n)
PrettyValQty = derivePrettyVal
export
zero, one, any : {n : Nat} -> Loc -> Qty n
zero = Q zero
one = Q one
any = Q $ pconst Any
export
(+) : Qty n -> Qty n -> Qty n
Q xs l1 + Q ys l2 = Q (xs +. ys) (l1 `or` l2)
export
(*) : Qty n -> Qty n -> Qty n
Q xs l1 * Q ys l2 = Q (xs *. ys) (l1 `or` l2)
export
isAny : Qty n -> Bool
isAny (Q pi _) = pi.at0 == Any
export
lub : {n : Nat} -> Qty n -> Qty n -> Qty n
lub pi rh = if pi == rh then pi else any pi.loc
||| "π ≤ ρ"
|||
||| if a variable is bound with quantity ρ, then it can be used with a total
||| if a variable is bound with quantity ρ, then it can be used with an actual
||| quantity π as long as π ≤ ρ. for example, an ω variable can be used any
||| number of times, so π ≤ ω for any π.
public export
compat : Qty -> Qty -> Bool
compat pi Any = True
compat pi rh = pi == rh
compat : Qty n -> Qty n -> Bool
compat pi rh = isAny rh || pi == rh
||| "π ∨ ρ"
|||
||| returns a quantity τ with π ≤ τ and ρ ≤ τ.
||| if π = ρ, then it's that, otherwise it's ω.
public export
lub : Qty -> Qty -> Qty
lub p q = if p == q then p else Any
private
toVarString : BContext n -> Monom n -> List BindName
toVarString ns ds = fold $ zipWith replicate ds ns
private
prettyTerm : {opts : LayoutOpts} ->
BContext n -> Monom n -> QConst -> Eff Pretty (Doc opts)
prettyTerm ns ds pi = do
pi <- prettyQConst pi
xs <- traverse prettyQBind (toVarString ns ds)
pure $ separateTight !qtimesD $ pi :: xs
export
prettyQty : {opts : LayoutOpts} -> BContext n -> Qty n -> Eff Pretty (Doc opts)
prettyQty ns (Q q _) =
let Val _ = lengthPrf0 ns in
separateLoose !qplusD <$>
traverse (uncurry $ prettyTerm ns) (toList q)
||| to maintain subject reduction, only 0 or 1 can occur
||| for the subject of a typing judgment. see @qtt, §2.3 for more detail
@ -87,9 +154,8 @@ data SQty = SZero | SOne
|||
||| σ ⨴ π is 0 if either of σ or π are, otherwise it is σ.
public export
subjMult : SQty -> Qty -> SQty
subjMult _ Zero = SZero
subjMult sg _ = sg
subjMult : SQty -> Qty n -> SQty
subjMult sg pi = if isZero pi.value then SZero else sg
||| it doesn't make much sense for a top level declaration to have a
@ -100,12 +166,6 @@ data GQty = GZero | GAny
%runElab derive "GQty" [Eq, Ord, Show, PrettyVal]
%name GQty rh
public export
toGlobal : Qty -> Maybe GQty
toGlobal Zero = Just GZero
toGlobal Any = Just GAny
toGlobal One = Nothing
||| when checking a definition, a 0 definition is checked at 0,
||| but an ω definition is checked at 1 since ω isn't a subject quantity
public export %inline
@ -114,18 +174,6 @@ globalToSubj GZero = SZero
globalToSubj GAny = SOne
public export
DecEq Qty where
decEq Zero Zero = Yes Refl
decEq Zero One = No $ \case _ impossible
decEq Zero Any = No $ \case _ impossible
decEq One Zero = No $ \case _ impossible
decEq One One = Yes Refl
decEq One Any = No $ \case _ impossible
decEq Any Zero = No $ \case _ impossible
decEq Any One = No $ \case _ impossible
decEq Any Any = Yes Refl
public export
DecEq SQty where
decEq SZero SZero = Yes Refl
@ -143,12 +191,48 @@ DecEq GQty where
namespace SQty
public export %inline
(.qty) : SQty -> Qty
(SZero).qty = Zero
(SOne).qty = One
toQty : {n : Nat} -> Loc -> SQty -> Qty n
toQty loc SZero = zero loc
toQty loc SOne = one loc
public export %inline
(.qconst) : SQty -> QConst
(SZero).qconst = Zero
(SOne).qconst = One
namespace GQty
public export %inline
(.qty) : GQty -> Qty
(GZero).qty = Zero
(GAny).qty = Any
toQty : {n : Nat} -> Loc -> GQty -> Qty n
toQty loc GZero = zero loc
toQty loc GAny = any loc
public export %inline
(.qconst) : GQty -> QConst
(GZero).qconst = Zero
(GAny).qconst = Any
export
prettySQty : {opts : _} -> SQty -> Eff Pretty (Doc opts)
prettySQty sg = prettyQConst sg.qconst
export
prettyGQty : {opts : _} -> GQty -> Eff Pretty (Doc opts)
prettyGQty pi = prettyQConst pi.qconst
public export
QSubst : Nat -> Nat -> Type
QSubst = Subst Qty
export
FromVarR Qty where
fromVarR i loc = Q (fromVarR i loc) loc
export
CanShift Qty where
Q p loc // by = Q (p // by) loc
export
CanSubstSelfR Qty where
Q q loc //? th = Q (q //? map (.value) th) loc

103
lib/Quox/Syntax/Subst.idr
View file

@ -42,24 +42,46 @@ export Ord (f to) => Ord (Subst f from to) where compare = compare `on` repr
export Show (f to) => Show (Subst f from to) where show = show . repr
export infixl 8 //
export infixl 8 //?, //
public export
interface FromVar term => CanSubstSelf term where
interface FromVarR term => CanSubstSelfR term where
(//?) : {from, to : Nat} ->
term from -> Lazy (Subst term from to) -> term to
public export
interface (FromVar term, CanSubstSelfR term) => CanSubstSelf term where
(//) : term from -> Lazy (Subst term from to) -> term to
0 substSame : (t : term from) -> (th : Subst term from to) ->
t //? th === t // th
public export
getLoc : FromVar term => Subst term from to -> Var from -> Loc -> term to
getLoc (Shift by) i loc = fromVarLoc (shift by i) loc
getLoc (t ::: th) VZ _ = t
getLoc (t ::: th) (VS i) loc = getLoc th i loc
getR : {to : Nat} -> FromVarR term =>
Subst term from to -> Var from -> Loc -> term to
getR (Shift by) i loc = fromVarR (shift by i) loc
getR (t ::: th) VZ _ = t
getR (t ::: th) (VS i) loc = getR th i loc
public export
get : FromVar term => Subst term from to -> Var from -> Loc -> term to
get (Shift by) i loc = fromVar (shift by i) loc
get (t ::: th) VZ _ = t
get (t ::: th) (VS i) loc = get th i loc
public export
CanSubstSelf Var where
i // Shift by = shift by i
VZ // (t ::: th) = t
VS i // (t ::: th) = i // th
substVar : Var from -> Lazy (Subst Var from to) -> Var to
substVar i (Shift by) = shift by i
substVar VZ (t ::: th) = t
substVar (VS i) (t ::: th) = substVar i th
public export
CanSubstSelfR Var where (//?) = substVar
public export
CanSubstSelf Var where (//) = substVar; substSame _ _ = Refl
public export %inline
@ -71,6 +93,16 @@ shift0 : (by : Nat) -> Subst env 0 by
shift0 by = rewrite sym $ plusZeroRightNeutral by in Shift $ fromNat by
export infixr 9 .?
public export
(.?) : CanSubstSelfR f => {from, mid, to : Nat} ->
Subst f from mid -> Subst f mid to -> Subst f from to
Shift by .? Shift bz = Shift $ by . bz
Shift SZ .? ph = ph
Shift (SS by) .? (t ::: th) = Shift by .? th
(t ::: th) .? ph = (t //? ph) ::: (th .? ph)
public export
(.) : CanSubstSelf f => Subst f from mid -> Subst f mid to -> Subst f from to
Shift by . Shift bz = Shift $ by . bz
@ -78,6 +110,7 @@ Shift SZ . ph = ph
Shift (SS by) . (t ::: th) = Shift by . th
(t ::: th) . ph = (t // ph) ::: (th . ph)
public export %inline
id : Subst f n n
id = shift 0
@ -95,11 +128,20 @@ map f (Shift by) = Shift by
map f (t ::: th) = f t ::: map f th
public export %inline
push : CanSubstSelf f => Loc -> Subst f from to -> Subst f (S from) (S to)
push loc th = fromVarLoc VZ loc ::: (th . shift 1)
public export
pushNR : {from, to : Nat} -> CanSubstSelfR f => (s : Nat) -> Loc ->
Subst f from to -> Subst f (s + from) (s + to)
pushNR 0 _ th = th
pushNR (S s) loc th =
rewrite plusSuccRightSucc s from in
rewrite plusSuccRightSucc s to in
pushNR s loc $ fromVarR VZ loc ::: (th .? shift 1)
public export %inline
pushR : {from, to : Nat} -> CanSubstSelfR f =>
Loc -> Subst f from to -> Subst f (S from) (S to)
pushR = pushNR 1
-- [fixme] a better way to do this?
public export
pushN : CanSubstSelf f => (s : Nat) -> Loc ->
Subst f from to -> Subst f (s + from) (s + to)
@ -107,7 +149,11 @@ pushN 0 _ th = th
pushN (S s) loc th =
rewrite plusSuccRightSucc s from in
rewrite plusSuccRightSucc s to in
pushN s loc $ fromVarLoc VZ loc ::: (th . shift 1)
pushN s loc $ fromVar VZ loc ::: (th . shift 1)
public export %inline
push : CanSubstSelf f => Loc -> Subst f from to -> Subst f (S from) (S to)
push = pushN 1
public export
drop1 : Subst f (S from) to -> Subst f from to
@ -167,3 +213,30 @@ export %hint
ShowWithSubst : (Show (env n), forall n. Show (tm n)) =>
Show (WithSubst tm env n)
ShowWithSubst = deriveShow
public export
record WithSubstR tm env n where
constructor SubR
{from : Nat}
term : tm from
subst : Lazy (Subst env from n)
export
(Eq (env n), forall n. Eq (tm n)) => Eq (WithSubstR tm env n) where
SubR {from = m1} t1 s1 == SubR {from = m2} t2 s2 =
case decEq m1 m2 of
Yes Refl => t1 == t2 && s1 == s2
No _ => False
export
(Ord (env n), forall n. Ord (tm n)) => Ord (WithSubstR tm env n) where
SubR {from = m1} t1 s1 `compare` SubR {from = m2} t2 s2 =
case cmp m1 m2 of
CmpLT _ => LT
CmpEQ => compare (t1, s1) (t2, s2)
CmpGT _ => GT
export %hint
ShowWithSubstR : (Show (env n), forall n. Show (tm n)) =>
Show (WithSubstR tm env n)
ShowWithSubstR = deriveShow

227
lib/Quox/Syntax/Term/Base.idr
View file

@ -32,11 +32,11 @@ import Derive.Prelude
public export
TermLike : Type
TermLike = Nat -> Nat -> Type
TermLike = (q, d, n : Nat) -> Type
public export
TSubstLike : Type
TSubstLike = Nat -> Nat -> Nat -> Type
TSubstLike = (q, d, n1, n2 : Nat) -> Type
public export
Universe : Type
@ -50,156 +50,162 @@ TagVal = String
mutual
public export
TSubst : TSubstLike
TSubst d = Subst $ \n => Elim d n
TSubst q d = Subst $ \n => Elim q d n
||| first argument `d` is dimension scope size;
||| second `n` is term scope size
public export
data Term : (d, n : Nat) -> Type where
data Term : (q, d, n : Nat) -> Type where
||| type of types
TYPE : (l : Universe) -> (loc : Loc) -> Term d n
TYPE : (l : Universe) -> (loc : Loc) -> Term q d n
||| IO state token. this is a builtin because otherwise #[main] being a
||| builtin makes no sense
IOState : (loc : Loc) -> Term d n
IOState : (loc : Loc) -> Term q d n
||| function type
Pi : (qty : Qty) -> (arg : Term d n) ->
(res : ScopeTerm d n) -> (loc : Loc) -> Term d n
Pi : (qty : Qty q) -> (arg : Term q d n) ->
(res : ScopeTerm q d n) -> (loc : Loc) -> Term q d n
||| function term
Lam : (body : ScopeTerm d n) -> (loc : Loc) -> Term d n
Lam : (body : ScopeTerm q d n) -> (loc : Loc) -> Term q d n
||| pair type
Sig : (fst : Term d n) -> (snd : ScopeTerm d n) -> (loc : Loc) -> Term d n
Sig : (fst : Term q d n) -> (snd : ScopeTerm q d n) -> (loc : Loc) ->
Term q d n
||| pair value
Pair : (fst, snd : Term d n) -> (loc : Loc) -> Term d n
Pair : (fst, snd : Term q d n) -> (loc : Loc) -> Term q d n
||| enumeration type
Enum : (cases : SortedSet TagVal) -> (loc : Loc) -> Term d n
Enum : (cases : SortedSet TagVal) -> (loc : Loc) -> Term q d n
||| enumeration value
Tag : (tag : TagVal) -> (loc : Loc) -> Term d n
Tag : (tag : TagVal) -> (loc : Loc) -> Term q d n
||| equality type
Eq : (ty : DScopeTerm d n) -> (l, r : Term d n) -> (loc : Loc) -> Term d n
Eq : (ty : DScopeTerm q d n) -> (l, r : Term q d n) -> (loc : Loc) ->
Term q d n
||| equality term
DLam : (body : DScopeTerm d n) -> (loc : Loc) -> Term d n
DLam : (body : DScopeTerm q d n) -> (loc : Loc) -> Term q d n
||| natural numbers (temporary until 𝐖 gets added)
NAT : (loc : Loc) -> Term d n
Nat : (val : Nat) -> (loc : Loc) -> Term d n
Succ : (p : Term d n) -> (loc : Loc) -> Term d n
NAT : (loc : Loc) -> Term q d n
Nat : (val : Nat) -> (loc : Loc) -> Term q d n
Succ : (p : Term q d n) -> (loc : Loc) -> Term q d n
||| strings
STRING : (loc : Loc) -> Term d n
Str : (str : String) -> (loc : Loc) -> Term d n
STRING : (loc : Loc) -> Term q d n
Str : (str : String) -> (loc : Loc) -> Term q d n
||| "box" (package a value up with a certain quantity)
BOX : (qty : Qty) -> (ty : Term d n) -> (loc : Loc) -> Term d n
Box : (val : Term d n) -> (loc : Loc) -> Term d n
BOX : (qty : Qty q) -> (ty : Term q d n) -> (loc : Loc) -> Term q d n
Box : (val : Term q d n) -> (loc : Loc) -> Term q d n
Let : (qty : Qty) -> (rhs : Elim d n) ->
(body : ScopeTerm d n) -> (loc : Loc) -> Term d n
Let : (qty : Qty q) -> (rhs : Elim q d n) ->
(body : ScopeTerm q d n) -> (loc : Loc) -> Term q d n
||| elimination
E : (e : Elim d n) -> Term d n
E : (e : Elim q d n) -> Term q d n
||| term closure/suspended substitution
CloT : WithSubst (Term d) (Elim d) n -> Term d n
CloT : WithSubst (Term q d) (Elim q d) n -> Term q d n
||| dimension closure/suspended substitution
DCloT : WithSubst (\d => Term d n) Dim d -> Term d n
DCloT : WithSubst (\d => Term q d n) Dim d -> Term q d n
||| quantity closure/suspended substitution
QCloT : WithSubstR (\q => Term q d n) Qty q -> Term q d n
%name Term s, t, r
||| first argument `d` is dimension scope size, second `n` is term scope size
public export
data Elim : (d, n : Nat) -> Type where
data Elim : (q, d, n : Nat) -> Type where
||| free variable, possibly with a displacement (see @crude, or @mugen for a
||| more abstract and formalised take)
|||
||| e.g. if f : ★₀ → ★₁, then f¹ : ★₁ → ★₂
F : (x : Name) -> (u : Universe) -> (loc : Loc) -> Elim d n
F : (x : Name) -> (u : Universe) -> (loc : Loc) -> Elim q d n
||| bound variable
B : (i : Var n) -> (loc : Loc) -> Elim d n
B : (i : Var n) -> (loc : Loc) -> Elim q d n
||| term application
App : (fun : Elim d n) -> (arg : Term d n) -> (loc : Loc) -> Elim d n
App : (fun : Elim q d n) -> (arg : Term q d n) -> (loc : Loc) -> Elim q d n
||| pair destruction
|||
||| `CasePair 𝜋 𝑒 ([𝑟], 𝐴) ([𝑥, 𝑦], 𝑡)` is
||| `𝐜𝐚𝐬𝐞 𝜋 · 𝑒 𝐫𝐞𝐭𝐮𝐫𝐧 𝑟 ⇒ 𝐴 𝐨𝐟 { (𝑥, 𝑦) ⇒ 𝑡 }`
CasePair : (qty : Qty) -> (pair : Elim d n) ->
(ret : ScopeTerm d n) ->
(body : ScopeTermN 2 d n) ->
CasePair : (qty : Qty q) -> (pair : Elim q d n) ->
(ret : ScopeTerm q d n) ->
(body : ScopeTermN 2 q d n) ->
(loc : Loc) ->
Elim d n
Elim q d n
||| first element of a pair. only works in non-linear contexts.
Fst : (pair : Elim d n) -> (loc : Loc) -> Elim d n
Fst : (pair : Elim q d n) -> (loc : Loc) -> Elim q d n
||| second element of a pair. only works in non-linear contexts.
Snd : (pair : Elim d n) -> (loc : Loc) -> Elim d n
Snd : (pair : Elim q d n) -> (loc : Loc) -> Elim q d n
||| enum matching
CaseEnum : (qty : Qty) -> (tag : Elim d n) ->
(ret : ScopeTerm d n) ->
(arms : CaseEnumArms d n) ->
CaseEnum : (qty : Qty q) -> (tag : Elim q d n) ->
(ret : ScopeTerm q d n) ->
(arms : CaseEnumArms q d n) ->
(loc : Loc) ->
Elim d n
Elim q d n
||| nat matching
CaseNat : (qty, qtyIH : Qty) -> (nat : Elim d n) ->
(ret : ScopeTerm d n) ->
(zero : Term d n) ->
(succ : ScopeTermN 2 d n) ->
CaseNat : (qty, qtyIH : Qty q) -> (nat : Elim q d n) ->
(ret : ScopeTerm q d n) ->
(zero : Term q d n) ->
(succ : ScopeTermN 2 q d n) ->
(loc : Loc) ->
Elim d n
Elim q d n
||| unboxing
CaseBox : (qty : Qty) -> (box : Elim d n) ->
(ret : ScopeTerm d n) ->
(body : ScopeTerm d n) ->
CaseBox : (qty : Qty q) -> (box : Elim q d n) ->
(ret : ScopeTerm q d n) ->
(body : ScopeTerm q d n) ->
(loc : Loc) ->
Elim d n
Elim q d n
||| dim application
DApp : (fun : Elim d n) -> (arg : Dim d) -> (loc : Loc) -> Elim d n
DApp : (fun : Elim q d n) -> (arg : Dim d) -> (loc : Loc) -> Elim q d n
||| type-annotated term
Ann : (tm, ty : Term d n) -> (loc : Loc) -> Elim d n
Ann : (tm, ty : Term q d n) -> (loc : Loc) -> Elim q d n
||| coerce a value along a type equality, or show its coherence
||| [@xtt; §2.1.1]
Coe : (ty : DScopeTerm d n) -> (p, q : Dim d) ->
(val : Term d n) -> (loc : Loc) -> Elim d n
Coe : (ty : DScopeTerm q d n) -> (p, p' : Dim d) ->
(val : Term q d n) -> (loc : Loc) -> Elim q d n
||| "generalised composition" [@xtt; §2.1.2]
Comp : (ty : Term d n) -> (p, q : Dim d) ->
(val : Term d n) -> (r : Dim d) ->
(zero, one : DScopeTerm d n) -> (loc : Loc) -> Elim d n
Comp : (ty : Term q d n) -> (p, p' : Dim d) ->
(val : Term q d n) -> (r : Dim d) ->
(zero, one : DScopeTerm q d n) -> (loc : Loc) -> Elim q d n
||| match on types. needed for b.s. of coercions [@xtt; §2.2]
TypeCase : (ty : Elim d n) -> (ret : Term d n) ->
(arms : TypeCaseArms d n) -> (def : Term d n) ->
TypeCase : (ty : Elim q d n) -> (ret : Term q d n) ->
(arms : TypeCaseArms q d n) -> (def : Term q d n) ->
(loc : Loc) ->
Elim d n
Elim q d n
||| term closure/suspended substitution
CloE : WithSubst (Elim d) (Elim d) n -> Elim d n
CloE : WithSubst (Elim q d) (Elim q d) n -> Elim q d n
||| dimension closure/suspended substitution
DCloE : WithSubst (\d => Elim d n) Dim d -> Elim d n
DCloE : WithSubst (\d => Elim q d n) Dim d -> Elim q d n
||| quantity closure/suspended substitution
QCloE : WithSubstR (\q => Elim q d n) Qty q -> Elim q d n
%name Elim e, f
public export
CaseEnumArms : TermLike
CaseEnumArms d n = SortedMap TagVal (Term d n)
CaseEnumArms q d n = SortedMap TagVal (Term q d n)
public export
TypeCaseArms : TermLike
TypeCaseArms d n = SortedDMap TyConKind (\k => TypeCaseArmBody k d n)
TypeCaseArms q d n = SortedDMap TyConKind (\k => TypeCaseArmBody k q d n)
public export
TypeCaseArm : TermLike
TypeCaseArm d n = (k ** TypeCaseArmBody k d n)
TypeCaseArm q d n = (k ** TypeCaseArmBody k q d n)
public export
TypeCaseArmBody : TyConKind -> TermLike
@ -208,35 +214,27 @@ mutual
public export
ScopeTermN, DScopeTermN : Nat -> TermLike
ScopeTermN s d n = Scoped s (Term d) n
DScopeTermN s d n = Scoped s (\d => Term d n) d
ScopeTermN s q d n = Scoped s (Term q d) n
DScopeTermN s q d n = Scoped s (\d => Term q d n) d
public export
ScopeTerm, DScopeTerm : TermLike
ScopeTerm = ScopeTermN 1
DScopeTerm = DScopeTermN 1
mutual
export %hint
EqTerm : Eq (Term d n)
EqTerm = assert_total {a = Eq (Term d n)} deriveEq
export %hint EqTerm : Eq (Term q d n)
export %hint EqElim : Eq (Elim q d n)
EqTerm = assert_total {a = Eq (Term q d n)} deriveEq
EqElim = assert_total {a = Eq (Elim q d n)} deriveEq
export %hint
EqElim : Eq (Elim d n)
EqElim = assert_total {a = Eq (Elim d n)} deriveEq
mutual
export %hint
ShowTerm : Show (Term d n)
ShowTerm = assert_total {a = Show (Term d n)} deriveShow
export %hint
ShowElim : Show (Elim d n)
ShowElim = assert_total {a = Show (Elim d n)} deriveShow
-- export %hint ShowTerm : {q, d, n : Nat} -> Show (Term q d n)
-- export %hint ShowElim : {q, d, n : Nat} -> Show (Elim q d n)
-- ShowTerm = assert_total {a = Show (Term q d n)} deriveShow
-- ShowElim = assert_total {a = Show (Elim q d n)} deriveShow
export
Located (Elim d n) where
Located (Elim q d n) where
(F _ _ loc).loc = loc
(B _ loc).loc = loc
(App _ _ loc).loc = loc
@ -253,9 +251,10 @@ Located (Elim d n) where
(TypeCase _ _ _ _ loc).loc = loc
(CloE (Sub e _)).loc = e.loc
(DCloE (Sub e _)).loc = e.loc
(QCloE (SubR e _)).loc = e.loc
export
Located (Term d n) where
Located (Term q d n) where
(TYPE _ loc).loc = loc
(IOState loc).loc = loc
(Pi _ _ _ loc).loc = loc
@ -277,6 +276,7 @@ Located (Term d n) where
(E e).loc = e.loc
(CloT (Sub t _)).loc = t.loc
(DCloT (Sub t _)).loc = t.loc
(QCloT (SubR t _)).loc = t.loc
export
Located1 f => Located (ScopedBody s f n) where
@ -289,7 +289,7 @@ Located1 f => Located (Scoped s f n) where
export
Relocatable (Elim d n) where
Relocatable (Elim q d n) where
setLoc loc (F x u _) = F x u loc
setLoc loc (B i _) = B i loc
setLoc loc (App fun arg _) = App fun arg loc
@ -317,9 +317,11 @@ Relocatable (Elim d n) where
CloE $ Sub (setLoc loc term) subst
setLoc loc (DCloE (Sub term subst)) =
DCloE $ Sub (setLoc loc term) subst
setLoc loc (QCloE (SubR term subst)) =
QCloE $ SubR (setLoc loc term) subst
export
Relocatable (Term d n) where
Relocatable (Term q d n) where
setLoc loc (TYPE l _) = TYPE l loc
setLoc loc (IOState _) = IOState loc
setLoc loc (Pi qty arg res _) = Pi qty arg res loc
@ -341,6 +343,7 @@ Relocatable (Term d n) where
setLoc loc (E e) = E $ setLoc loc e
setLoc loc (CloT (Sub term subst)) = CloT $ Sub (setLoc loc term) subst
setLoc loc (DCloT (Sub term subst)) = DCloT $ Sub (setLoc loc term) subst
setLoc loc (QCloT (SubR term subst)) = QCloT $ SubR (setLoc loc term) subst
export
Relocatable1 f => Relocatable (ScopedBody s f n) where
@ -354,93 +357,93 @@ Relocatable1 f => Relocatable (Scoped s f n) where
||| more convenient Pi
public export %inline
PiY : (qty : Qty) -> (x : BindName) ->
(arg : Term d n) -> (res : Term d (S n)) -> (loc : Loc) -> Term d n
PiY : (qty : Qty q) -> (x : BindName) ->
(arg : Term q d n) -> (res : Term q d (S n)) -> (loc : Loc) -> Term q d n
PiY {qty, x, arg, res, loc} = Pi {qty, arg, res = SY [< x] res, loc}
||| more convenient Lam
public export %inline
LamY : (x : BindName) -> (body : Term d (S n)) -> (loc : Loc) -> Term d n
LamY : (x : BindName) -> (body : Term q d (S n)) -> (loc : Loc) -> Term q d n
LamY {x, body, loc} = Lam {body = SY [< x] body, loc}
public export %inline
LamN : (body : Term d n) -> (loc : Loc) -> Term d n
LamN : (body : Term q d n) -> (loc : Loc) -> Term q d n
LamN {body, loc} = Lam {body = SN body, loc}
||| non dependent function type
public export %inline
Arr : (qty : Qty) -> (arg, res : Term d n) -> (loc : Loc) -> Term d n
Arr : (qty : Qty q) -> (arg, res : Term q d n) -> (loc : Loc) -> Term q d n
Arr {qty, arg, res, loc} = Pi {qty, arg, res = SN res, loc}
||| more convenient Sig
public export %inline
SigY : (x : BindName) -> (fst : Term d n) ->
(snd : Term d (S n)) -> (loc : Loc) -> Term d n
SigY : (x : BindName) -> (fst : Term q d n) ->
(snd : Term q d (S n)) -> (loc : Loc) -> Term q d n
SigY {x, fst, snd, loc} = Sig {fst, snd = SY [< x] snd, loc}
||| non dependent pair type
public export %inline
And : (fst, snd : Term d n) -> (loc : Loc) -> Term d n
And : (fst, snd : Term q d n) -> (loc : Loc) -> Term q d n
And {fst, snd, loc} = Sig {fst, snd = SN snd, loc}
||| more convenient Eq
public export %inline
EqY : (i : BindName) -> (ty : Term (S d) n) ->
(l, r : Term d n) -> (loc : Loc) -> Term d n
EqY : (i : BindName) -> (ty : Term q (S d) n) ->
(l, r : Term q d n) -> (loc : Loc) -> Term q d n
EqY {i, ty, l, r, loc} = Eq {ty = SY [< i] ty, l, r, loc}
||| more convenient DLam
public export %inline
DLamY : (i : BindName) -> (body : Term (S d) n) -> (loc : Loc) -> Term d n
DLamY : (i : BindName) -> (body : Term q (S d) n) -> (loc : Loc) -> Term q d n
DLamY {i, body, loc} = DLam {body = SY [< i] body, loc}
public export %inline
DLamN : (body : Term d n) -> (loc : Loc) -> Term d n
DLamN : (body : Term q d n) -> (loc : Loc) -> Term q d n
DLamN {body, loc} = DLam {body = SN body, loc}
||| non dependent equality type
public export %inline
Eq0 : (ty, l, r : Term d n) -> (loc : Loc) -> Term d n
Eq0 : (ty, l, r : Term q d n) -> (loc : Loc) -> Term q d n
Eq0 {ty, l, r, loc} = Eq {ty = SN ty, l, r, loc}
||| same as `F` but as a term
public export %inline
FT : Name -> Universe -> Loc -> Term d n
FT : Name -> Universe -> Loc -> Term q d n
FT x u loc = E $ F x u loc
||| same as `B` but as a term
public export %inline
BT : Var n -> (loc : Loc) -> Term d n
BT : Var n -> (loc : Loc) -> Term q d n
BT i loc = E $ B i loc
||| abbreviation for a bound variable like `BV 4` instead of
||| `B (VS (VS (VS (VS VZ))))`
public export %inline
BV : (i : Nat) -> (0 _ : LT i n) => (loc : Loc) -> Elim d n
BV : (i : Nat) -> (0 _ : LT i n) => (loc : Loc) -> Elim q d n
BV i loc = B (V i) loc
||| same as `BV` but as a term
public export %inline
BVT : (i : Nat) -> (0 _ : LT i n) => (loc : Loc) -> Term d n
BVT : (i : Nat) -> (0 _ : LT i n) => (loc : Loc) -> Term q d n
BVT i loc = E $ BV i loc
public export %inline
Zero : Loc -> Term d n
Zero : Loc -> Term q d n
Zero = Nat 0
public export %inline
enum : List TagVal -> Loc -> Term d n
enum : List TagVal -> Loc -> Term q d n
enum ts loc = Enum (SortedSet.fromList ts) loc
public export %inline
typeCase : Elim d n -> Term d n ->
List (TypeCaseArm d n) -> Term d n -> Loc -> Elim d n
typeCase : Elim q d n -> Term q d n ->
List (TypeCaseArm q d n) -> Term q d n -> Loc -> Elim q d n
typeCase ty ret arms def loc = TypeCase ty ret (fromList arms) def loc
public export %inline
typeCase1Y : Elim d n -> Term d n ->
(k : TyConKind) -> BContext (arity k) -> Term d (arity k + n) ->
typeCase1Y : Elim q d n -> Term q d n ->
(k : TyConKind) -> BContext (arity k) -> Term q d (arity k + n) ->
(loc : Loc) ->
{default (NAT loc) def : Term d n} ->
Elim d n
{default (NAT loc) def : Term q d n} ->
Elim q d n
typeCase1Y ty ret k ns body loc = typeCase ty ret [(k ** SY ns body)] def loc

541
lib/Quox/Syntax/Term/Pretty.idr
View file

@ -5,6 +5,7 @@ import Quox.Syntax.Term.Subst
import Quox.Context
import Quox.Pretty
import Quox.SingletonExtra
import Data.Vect
import Derive.Prelude
@ -13,21 +14,23 @@ import Derive.Prelude
export
prettyUniverse : {opts : _} -> Universe -> Eff Pretty (Doc opts)
prettyUniverse : {opts : LayoutOpts} -> Universe -> Eff Pretty (Doc opts)
prettyUniverse = hl Universe . text . show
export
prettyTerm : {opts : _} -> BContext d -> BContext n -> Term d n ->
Eff Pretty (Doc opts)
prettyTerm : {opts : LayoutOpts} ->
NameContexts q d n -> Term q d n -> Eff Pretty (Doc opts)
export
prettyElim : {opts : _} -> BContext d -> BContext n -> Elim d n ->
Eff Pretty (Doc opts)
prettyElim : {opts : LayoutOpts} ->
NameContexts q d n -> Elim q d n -> Eff Pretty (Doc opts)
private
BTelescope : Nat -> Nat -> Type
BTelescope = Telescope' BindName
export
prettyQty : {opts : LayoutOpts} ->
NameContexts q d n -> Qty q -> Eff Pretty (Doc opts)
prettyQty names pi = let Val q = names.qtyLen in prettyQty names.qnames pi
private
@ -40,109 +43,111 @@ superscript = pack . map sup . unpack where
private
PiBind : Nat -> Nat -> Type
PiBind d n = (Qty, BindName, Term d n)
PiBind : TermLike
PiBind q d n = (Qty q, BindName, Term q d n)
private
pbname : PiBind d n -> BindName
pbname : PiBind q d n -> BindName
pbname (_, x, _) = x
private
record SplitPi d n where
record SplitPi q d n where
constructor MkSplitPi
{0 inner : Nat}
binds : Telescope (PiBind d) n inner
cod : Term d inner
binds : Telescope (PiBind q d) n inner
cod : Term q d inner
private
splitPi : Telescope (PiBind d) n n' -> Term d n' -> SplitPi d n
splitPi binds (Pi qty arg res _) =
splitPi : {q : Nat} ->
Telescope (PiBind q d) n n' -> Term q d n' -> SplitPi q d n
splitPi binds cod@(Pi qty arg res _) =
splitPi (binds :< (qty, res.name, arg)) $
assert_smaller res $ pushSubsts' res.term
assert_smaller cod $ pushSubsts' res.term
splitPi binds cod = MkSplitPi {binds, cod}
private
prettyPiBind1 : {opts : _} ->
Qty -> BindName -> BContext d -> BContext n -> Term d n ->
prettyPiBind1 : {opts : LayoutOpts} ->
NameContexts q d n -> Qty q -> BindName -> Term q d n ->
Eff Pretty (Doc opts)
prettyPiBind1 pi (BN Unused _) dnames tnames s =
prettyPiBind1 names pi (BN Unused _) s =
hcat <$> sequence
[prettyQty pi, dotD,
withPrec Arg $ assert_total prettyTerm dnames tnames s]
prettyPiBind1 pi x dnames tnames s = hcat <$> sequence
[prettyQty pi, dotD,
[prettyQty names pi, dotD,
withPrec Arg $ assert_total prettyTerm names s]
prettyPiBind1 names pi x s =
hcat <$> sequence
[prettyQty names pi, dotD,
hl Delim $ text "(",
hsep <$> sequence
[prettyTBind x, hl Delim $ text ":",
withPrec Outer $ assert_total prettyTerm dnames tnames s],
withPrec Outer $ assert_total prettyTerm names s],
hl Delim $ text ")"]
private
prettyPiBinds : {opts : _} ->
BContext d -> BContext n ->
Telescope (PiBind d) n n' ->
prettyPiBinds : {opts : LayoutOpts} ->
NameContexts q d n ->
Telescope (PiBind q d) n n' ->
Eff Pretty (SnocList (Doc opts))
prettyPiBinds _ _ [<] = pure [<]
prettyPiBinds dnames tnames (binds :< (q, x, t)) =
let tnames' = tnames . map pbname binds in
[|prettyPiBinds dnames tnames binds :<
prettyPiBind1 q x dnames tnames' t|]
prettyPiBinds _ [<] = pure [<]
prettyPiBinds names (binds :< (q, x, t)) =
let names' = extendTermN' (map pbname binds) names in
[|prettyPiBinds names binds :<
prettyPiBind1 names' q x t|]
private
SigBind : Nat -> Nat -> Type
SigBind d n = (BindName, Term d n)
SigBind : TermLike
SigBind q d n = (BindName, Term q d n)
private
record SplitSig d n where
record SplitSig q d n where
constructor MkSplitSig
{0 inner : Nat}
binds : Telescope (SigBind d) n inner
last : Term d inner
binds : Telescope (SigBind q d) n inner
last : Term q d inner
private
splitSig : Telescope (SigBind d) n n' -> Term d n' -> SplitSig d n
splitSig : {q : Nat} ->
Telescope (SigBind q d) n n' -> Term q d n' -> SplitSig q d n
splitSig binds (Sig fst snd _) =
splitSig (binds :< (snd.name, fst)) $
assert_smaller snd $ pushSubsts' snd.term
splitSig binds last = MkSplitSig {binds, last}
private
prettySigBind1 : {opts : _} ->
BindName -> BContext d -> BContext n -> Term d n ->
prettySigBind1 : {opts : LayoutOpts} ->
NameContexts q d n -> BindName -> Term q d n ->
Eff Pretty (Doc opts)
prettySigBind1 (BN Unused _) dnames tnames s =
withPrec InTimes $ assert_total prettyTerm dnames tnames s
prettySigBind1 x dnames tnames s = hcat <$> sequence
prettySigBind1 names (BN Unused _) s =
withPrec InTimes $ assert_total prettyTerm names s
prettySigBind1 names x s = hcat <$> sequence
[hl Delim $ text "(",
hsep <$> sequence
[prettyTBind x, hl Delim $ text ":",
withPrec Outer $ assert_total prettyTerm dnames tnames s],
withPrec Outer $ assert_total prettyTerm names s],
hl Delim $ text ")"]
private
prettySigBinds : {opts : _} ->
BContext d -> BContext n ->
Telescope (SigBind d) n n' ->
prettySigBinds : {opts : LayoutOpts} ->
NameContexts q d n -> Telescope (SigBind q d) n n' ->
Eff Pretty (SnocList (Doc opts))
prettySigBinds _ _ [<] = pure [<]
prettySigBinds dnames tnames (binds :< (x, t)) =
let tnames' = tnames . map fst binds in
[|prettySigBinds dnames tnames binds :<
prettySigBind1 x dnames tnames' t|]
prettySigBinds _ [<] = pure [<]
prettySigBinds names (binds :< (x, t)) =
let names' = extendTermN' (map fst binds) names in
[|prettySigBinds names binds :<
prettySigBind1 names' x t|]
private
prettyTypeLine : {opts : _} ->
BContext d -> BContext n ->
DScopeTerm d n ->
prettyTypeLine : {opts : LayoutOpts} ->
NameContexts q d n -> DScopeTerm q d n ->
Eff Pretty (Doc opts)
prettyTypeLine dnames tnames (S _ (N body)) =
withPrec Arg (prettyTerm dnames tnames body)
prettyTypeLine dnames tnames (S [< i] (Y body)) =
prettyTypeLine names (S _ (N body)) =
withPrec Arg (prettyTerm names body)
prettyTypeLine names (S [< i] (Y body)) =
parens =<< do
let names' = extendDim i names
i' <- prettyDBind i
ty' <- withPrec Outer $ prettyTerm (dnames :< i) tnames body
ty' <- withPrec Outer $ prettyTerm names' body
pure $ sep [hsep [i', !darrowD], ty']
@ -155,16 +160,16 @@ NameChunks : Type
NameChunks = SnocList (NameSort, SnocList BindName)
private
record SplitLams d n where
record SplitLams q d n where
constructor MkSplitLams
{0 dinner, ninner : Nat}
dnames : BTelescope d dinner
tnames : BTelescope n ninner
chunks : NameChunks
body : Term dinner ninner
body : Term q dinner ninner
private
splitLams : Term d n -> SplitLams d n
splitLams : {q : Nat} -> Term q d n -> SplitLams q d n
splitLams s = go [<] [<] [<] (pushSubsts' s)
where
push : NameSort -> BindName -> NameChunks -> NameChunks
@ -175,7 +180,7 @@ where
go : BTelescope d d' -> BTelescope n n' ->
SnocList (NameSort, SnocList BindName) ->
Term d' n' -> SplitLams d n
Term q d' n' -> SplitLams q d n
go dnames tnames chunks (Lam b _) =
go dnames (tnames :< b.name) (push T b.name chunks) $
assert_smaller b $ pushSubsts' b.term
@ -187,28 +192,31 @@ where
private
splitTuple : SnocList (Term d n) -> Term d n -> SnocList (Term d n)
splitTuple : {q : Nat} ->
SnocList (Term q d n) -> Term q d n -> SnocList (Term q d n)
splitTuple ss p@(Pair t1 t2 _) =
splitTuple (ss :< t1) $ assert_smaller p $ pushSubsts' t2
splitTuple ss t = ss :< t
private
prettyTArg : {opts : _} -> BContext d -> BContext n ->
Term d n -> Eff Pretty (Doc opts)
prettyTArg dnames tnames s =
withPrec Arg $ assert_total prettyTerm dnames tnames s
prettyTArg : {opts : LayoutOpts} ->
NameContexts q d n -> Term q d n -> Eff Pretty (Doc opts)
prettyTArg names s =
withPrec Arg $ assert_total prettyTerm names s
private
prettyDArg : {opts : _} -> BContext d -> Dim d -> Eff Pretty (Doc opts)
prettyDArg dnames p = [|atD <+> withPrec Arg (prettyDim dnames p)|]
prettyDArg : {opts : LayoutOpts} ->
NameContexts _ d _ -> Dim d -> Eff Pretty (Doc opts)
prettyDArg names p = [|atD <+> withPrec Arg (prettyDim names.dnames p)|]
private
splitApps : Elim d n -> (Elim d n, List (Either (Dim d) (Term d n)))
splitApps : {q : Nat} ->
Elim q d n -> (Elim q d n, List (Either (Dim d) (Term q d n)))
splitApps e = go [] (pushSubsts' e)
where
go : List (Either (Dim d) (Term d n)) -> Elim d n ->
(Elim d n, List (Either (Dim d) (Term d n)))
go : List (Either (Dim d) (Term q d n)) -> Elim q d n ->
(Elim q d n, List (Either (Dim d) (Term q d n)))
go xs e@(App f s _) =
go (Right s :: xs) $ assert_smaller e $ pushSubsts' f
go xs e@(DApp f p _) =
@ -216,49 +224,53 @@ where
go xs s = (s, xs)
private
prettyDTApps : {opts : _} ->
BContext d -> BContext n ->
Elim d n -> List (Either (Dim d) (Term d n)) ->
prettyDTApps : {opts : LayoutOpts} ->
NameContexts q d n ->
Elim q d n -> List (Either (Dim d) (Term q d n)) ->
Eff Pretty (Doc opts)
prettyDTApps dnames tnames f xs = do
f <- withPrec Arg $ assert_total prettyElim dnames tnames f
xs <- for xs $ either (prettyDArg dnames) (prettyTArg dnames tnames)
parensIfM App =<< prettyAppD f xs
prettyDTApps names f xs = do
f <- withPrec Arg $ assert_total prettyElim names f
xs <- for xs $ either (prettyDArg names) (prettyTArg names)
prettyAppD f xs
private
record CaseArm opts d n where
record CaseArm opts q d n where
constructor MkCaseArm
pat : Doc opts
dbinds : BTelescope d dinner -- 🍴
tbinds : BTelescope n ninner
body : Term dinner ninner
body : Term q dinner ninner
parameters {opts : LayoutOpts} (dnames : BContext d) (tnames : BContext n)
private
prettyCaseArm : CaseArm opts d n -> Eff Pretty (Doc opts)
prettyCaseArm (MkCaseArm pat dbinds tbinds body) = do
body <- withPrec Outer $ assert_total
prettyTerm (dnames . dbinds) (tnames . tbinds) body
prettyCaseArm : {opts : LayoutOpts} ->
NameContexts q d n -> CaseArm opts q d n ->
Eff Pretty (Doc opts)
prettyCaseArm names (MkCaseArm pat dbinds tbinds body) = do
let names' = extendDimN' dbinds $ extendTermN' tbinds names
body <- withPrec Outer $ assert_total prettyTerm names' body
header <- (pat <++>) <$> darrowD
pure $ ifMultiline (header <++> body) (vsep [header, !(indentD body)])
private
prettyCaseBody : List (CaseArm opts d n) -> Eff Pretty (List (Doc opts))
prettyCaseBody xs = traverse prettyCaseArm xs
prettyCaseBody : {opts : LayoutOpts} ->
NameContexts q d n -> List (CaseArm opts q d n) ->
Eff Pretty (List (Doc opts))
prettyCaseBody names xs = traverse (prettyCaseArm names) xs
private
prettyCompPat : {opts : _} -> DimConst -> BindName -> Eff Pretty (Doc opts)
prettyCompPat : {opts : LayoutOpts} ->
DimConst -> BindName -> Eff Pretty (Doc opts)
prettyCompPat e x = [|prettyDimConst e <++> prettyDBind x|]
private
prettyCompArm : {opts : _} -> BContext d -> BContext n ->
DimConst -> DScopeTerm d n -> Eff Pretty (Doc opts)
prettyCompArm dnames tnames e s = prettyCaseArm dnames tnames $
prettyCompArm : {opts : LayoutOpts} -> NameContexts q d n ->
DimConst -> DScopeTerm q d n -> Eff Pretty (Doc opts)
prettyCompArm names e s = prettyCaseArm names $
MkCaseArm !(prettyCompPat e s.name) [< s.name] [<] s.term
private
layoutComp : {opts : _} ->
layoutComp : {opts : LayoutOpts} ->
(typq : List (Doc opts)) -> (val, r : Doc opts) ->
(arms : List (Doc opts)) -> Eff Pretty (Doc opts)
layoutComp typq val r arms = do
@ -273,32 +285,33 @@ layoutComp typq val r arms = do
export
prettyEnum : {opts : _} -> List String -> Eff Pretty (Doc opts)
prettyEnum : {opts : LayoutOpts} -> List String -> Eff Pretty (Doc opts)
prettyEnum cases =
tightBraces =<<
fillSeparateTight !commaD <$>
traverse (hl Constant . Doc.text . quoteTag) cases
private
prettyCaseRet : {opts : _} ->
BContext d -> BContext n ->
ScopeTerm d n -> Eff Pretty (Doc opts)
prettyCaseRet dnames tnames body = withPrec Outer $ case body of
S _ (N tm) => assert_total prettyTerm dnames tnames tm
prettyCaseRet : {opts : LayoutOpts} ->
NameContexts q d n -> ScopeTerm q d n -> Eff Pretty (Doc opts)
prettyCaseRet names body = withPrec Outer $ case body of
S _ (N tm) => assert_total prettyTerm names tm
S [< x] (Y tm) => do
let names' = extendTerm x names
header <- [|prettyTBind x <++> darrowD|]
body <- assert_total prettyTerm dnames (tnames :< x) tm
body <- assert_total prettyTerm names' tm
hangDSingle header body
private
prettyCase_ : {opts : _} ->
BContext d -> BContext n ->
Doc opts -> Elim d n -> ScopeTerm d n -> List (CaseArm opts d n) ->
prettyCase_ : {opts : LayoutOpts} ->
NameContexts q d n ->
Doc opts -> Elim q d n -> ScopeTerm q d n ->
List (CaseArm opts q d n) ->
Eff Pretty (Doc opts)
prettyCase_ dnames tnames intro head ret body = do
head <- withPrec Outer $ assert_total prettyElim dnames tnames head
ret <- prettyCaseRet dnames tnames ret
bodys <- prettyCaseBody dnames tnames body
prettyCase_ names intro head ret body = do
head <- withPrec Outer $ assert_total prettyElim names head
ret <- prettyCaseRet names ret
bodys <- prettyCaseBody names body
return <- returnD; of_ <- ofD
lb <- hl Delim "{"; rb <- hl Delim "}"; semi <- semiD
ind <- askAt INDENT
@ -308,25 +321,27 @@ prettyCase_ dnames tnames intro head ret body = do
indent ind $ vseparateTight semi bodys, rb])
private
prettyCase : {opts : _} ->
BContext d -> BContext n ->
Qty -> Elim d n -> ScopeTerm d n -> List (CaseArm opts d n) ->
prettyCase : {opts : LayoutOpts} ->
NameContexts q d n ->
Qty q -> Elim q d n -> ScopeTerm q d n ->
List (CaseArm opts q d n) ->
Eff Pretty (Doc opts)
prettyCase dnames tnames qty head ret body =
prettyCase_ dnames tnames ![|caseD <+> prettyQty qty|] head ret body
prettyCase names qty head ret body =
prettyCase_ names ![|caseD <+> prettyQty names qty|] head ret body
private
LetBinder : Nat -> Nat -> Type
LetBinder d n = (Qty, BindName, Elim d n)
LetBinder : TermLike
LetBinder q d n = (Qty q, BindName, Elim q d n)
private
LetExpr : Nat -> Nat -> Nat -> Type
LetExpr d n n' = (Telescope (LetBinder d) n n', Term d n')
LetExpr : (q, d, n, n' : Nat) -> Type
LetExpr q d n n' = (Telescope (LetBinder q d) n n', Term q d n')
-- [todo] factor out this and the untyped version somehow
export
splitLet : Telescope (LetBinder d) n n' -> Term d n' -> Exists (LetExpr d n)
splitLet : Telescope (LetBinder q d) n n' -> Term q d n' ->
Exists (LetExpr q d n)
splitLet ys t@(Let qty rhs body _) =
splitLet (ys :< (qty, body.name, rhs)) (assert_smaller t body.term)
splitLet ys t =
@ -334,38 +349,40 @@ splitLet ys t =
private covering
prettyLets : {opts : LayoutOpts} ->
BContext d -> BContext a -> Telescope (LetBinder d) a b ->
NameContexts q d a -> Telescope (LetBinder q d) a b ->
Eff Pretty (SnocList (Doc opts))
prettyLets dnames xs lets = snd <$> go lets where
peelAnn : forall d, n. Elim d n -> Maybe (Term d n, Term d n)
prettyLets (MkNameContexts qnames dnames tnames) lets = snd <$> go lets where
peelAnn : forall d, n. Elim q d n -> Maybe (Term q d n, Term q d n)
peelAnn (Ann tm ty _) = Just (tm, ty)
peelAnn e = Nothing
letHeader : Qty -> BindName -> Eff Pretty (Doc opts)
letHeader : Qty q -> BindName -> Eff Pretty (Doc opts)
letHeader qty x = do
lett <- [|letD <+> prettyQty qty|]
lett <- [|letD <+> prettyQty qnames qty|]
x <- prettyTBind x
pure $ lett <++> x
letBody : forall n. BContext n ->
Doc opts -> Elim d n -> Eff Pretty (Doc opts)
letBody tnames hdr e = case peelAnn e of
Doc opts -> Elim q d n -> Eff Pretty (Doc opts)
letBody tnames hdr e =
let names = MkNameContexts' qnames dnames tnames in
case peelAnn e of
Just (tm, ty) => do
ty <- withPrec Outer $ assert_total prettyTerm dnames tnames ty
tm <- withPrec Outer $ assert_total prettyTerm dnames tnames tm
ty <- withPrec Outer $ assert_total prettyTerm names ty
tm <- withPrec Outer $ assert_total prettyTerm names tm
colon <- colonD; eq <- cstD; d <- askAt INDENT
pure $ hangSingle d (hangSingle d hdr (colon <++> ty)) (eq <++> tm)
Nothing => do
e <- withPrec Outer $ assert_total prettyElim dnames tnames e
e <- withPrec Outer $ assert_total prettyElim names e
eq <- cstD; d <- askAt INDENT
inn <- inD
pure $ ifMultiline
(hsep [hdr, eq, e, inn])
(vsep [hdr, indent d $ hsep [eq, e, inn]])
go : forall b. Telescope (LetBinder d) a b ->
go : forall b. Telescope (LetBinder q d) a b ->
Eff Pretty (BContext b, SnocList (Doc opts))
go [<] = pure (xs, [<])
go [<] = pure (tnames, [<])
go (lets :< (qty, x, rhs)) = do
(ys, docs) <- go lets
doc <- letBody ys !(letHeader qty x) rhs
@ -385,7 +402,7 @@ toTel [<] = [<]
toTel (ctx :< x) = toTel ctx :< x
private
prettyTyCasePat : {opts : _} ->
prettyTyCasePat : {opts : LayoutOpts} ->
(k : TyConKind) -> BContext (arity k) ->
Eff Pretty (Doc opts)
prettyTyCasePat KTYPE [<] = typeD
@ -402,13 +419,14 @@ prettyTyCasePat KString [<] = stringD
prettyTyCasePat KBOX [< a] = bracks =<< prettyTBind a
prettyLambda : {opts : _} -> BContext d -> BContext n ->
Term d n -> Eff Pretty (Doc opts)
prettyLambda dnames tnames s =
parensIfM Outer =<< do
let MkSplitLams {dnames = ds, tnames = ts, chunks, body} = splitLams s
hangDSingle !(header chunks)
!(assert_total prettyTerm (dnames . ds) (tnames . ts) body)
prettyLambda : {opts : LayoutOpts} ->
NameContexts q d n -> Term q d n -> Eff Pretty (Doc opts)
prettyLambda names s =
let Val q = names.qtyLen
MkSplitLams {dnames = ds, tnames = ts, chunks, body} = splitLams s
names' = extendDimN' ds $ extendTermN' ts names in
parensIfM Outer =<<
hangDSingle !(header chunks) !(assert_total prettyTerm names' body)
where
introChar : NameSort -> Eff Pretty (Doc opts)
introChar T = lamD
@ -426,198 +444,207 @@ where
header cs = sep <$> traverse (\(s, xs) => header1 s (toList xs)) (toList cs)
prettyDisp : {opts : _} -> Universe -> Eff Pretty (Maybe (Doc opts))
prettyDisp : {opts : LayoutOpts} -> Universe -> Eff Pretty (Maybe (Doc opts))
prettyDisp 0 = pure Nothing
prettyDisp u = map Just $ hl Universe =<<
ifUnicode (text $ superscript $ show u) (text $ "^" ++ show u)
prettyTerm dnames tnames (TYPE l _) = do
prettyTerm names (TYPE l _) = do
type <- hl Syntax . text =<< ifUnicode "★" "Type"
level <- prettyDisp l
pure $ maybe type (type <+>) level
prettyTerm dnames tnames (IOState _) =
prettyTerm _ (IOState _) =
ioStateD
prettyTerm dnames tnames (Pi qty arg res _) =
parensIfM Outer =<< do
let MkSplitPi {binds, cod} = splitPi [< (qty, res.name, arg)] res.term
prettyTerm names (Pi qty arg res _) = do
let Val q = names.qtyLen
MkSplitPi {binds, cod} = splitPi [< (qty, res.name, arg)] res.term
arr <- arrowD
lines <- map (<++> arr) <$> prettyPiBinds dnames tnames binds
let tnames = tnames . map pbname binds
cod <- withPrec Outer $ prettyTerm dnames tnames (assert_smaller res cod)
pure $ sepSingle $ toList $ lines :< cod
lines <- map (<++> arr) <$> prettyPiBinds names binds
let names' = extendTermN' (map pbname binds) names
cod <- withPrec Outer $ prettyTerm names' (assert_smaller res cod)
parensIfM Outer $ sepSingle $ toList $ lines :< cod
prettyTerm dnames tnames s@(Lam {}) =
prettyLambda dnames tnames s
prettyTerm names s@(Lam {}) =
prettyLambda names s
prettyTerm dnames tnames (Sig fst snd _) =
parensIfM Times =<< do
let MkSplitSig {binds, last} = splitSig [< (snd.name, fst)] snd.term
prettyTerm names (Sig tfst tsnd _) = do
let Val q = names.qtyLen
MkSplitSig {binds, last} = splitSig [< (tsnd.name, tfst)] tsnd.term
times <- timesD
lines <- map (<++> times) <$> prettySigBinds dnames tnames binds
let tnames = tnames . map Builtin.fst binds
last <- withPrec InTimes $
prettyTerm dnames tnames (assert_smaller snd last)
pure $ sepSingle $ toList $ lines :< last
lines <- map (<++> times) <$> prettySigBinds names binds
let names' = extendTermN' (map fst binds) names
last <- withPrec InTimes $ prettyTerm names' (assert_smaller tsnd last)
parensIfM Times $ sepSingle $ toList $ lines :< last
prettyTerm dnames tnames p@(Pair fst snd _) =
parens =<< do
let elems = splitTuple [< fst] snd
prettyTerm names p@(Pair s t _) = do
let Val q = names.qtyLen
elems = splitTuple [< s] t
lines <- for elems $ \t =>
withPrec Outer $ prettyTerm dnames tnames $ assert_smaller p t
pure $ separateTight !commaD lines
withPrec Outer $ prettyTerm names $ assert_smaller p t
parens $ separateTight !commaD lines
prettyTerm dnames tnames (Enum cases _) =
prettyTerm _ (Enum cases _) =
prettyEnum $ SortedSet.toList cases
prettyTerm dnames tnames (Tag tag _) =
prettyTerm _ (Tag tag _) =
prettyTag tag
prettyTerm dnames tnames (Eq (S _ (N ty)) l r _) =
parensIfM Eq =<< do
l <- withPrec InEq $ prettyTerm dnames tnames l
r <- withPrec InEq $ prettyTerm dnames tnames r
ty <- withPrec InEq $ prettyTerm dnames tnames ty
pure $ sep [l <++> !eqndD, r <++> !colonD, ty]
prettyTerm names (Eq (S _ (N ty)) l r _) = do
l <- withPrec InEq $ prettyTerm names l
r <- withPrec InEq $ prettyTerm names r
ty <- withPrec InEq $ prettyTerm names ty
parensIfM Eq $ sep [l <++> !eqndD, r <++> !colonD, ty]
prettyTerm dnames tnames (Eq ty l r _) =
parensIfM App =<< do
ty <- prettyTypeLine dnames tnames ty
l <- withPrec Arg $ prettyTerm dnames tnames l
r <- withPrec Arg $ prettyTerm dnames tnames r
prettyTerm names (Eq ty l r _) = do
ty <- prettyTypeLine names ty
l <- withPrec Arg $ prettyTerm names l
r <- withPrec Arg $ prettyTerm names r
prettyAppD !eqD [ty, l, r]
prettyTerm dnames tnames s@(DLam {}) =
prettyLambda dnames tnames s
prettyTerm names s@(DLam {}) =
prettyLambda names s
prettyTerm dnames tnames (NAT _) = natD
prettyTerm dnames tnames (Nat n _) = hl Syntax $ pshow n
prettyTerm dnames tnames (Succ p _) =
parensIfM App =<<
prettyAppD !succD [!(withPrec Arg $ prettyTerm dnames tnames p)]
prettyTerm _ (NAT _) = natD
prettyTerm _ (Nat n _) = hl Syntax $ pshow n
prettyTerm names (Succ p _) =
prettyAppD !succD [!(withPrec Arg $ prettyTerm names p)]
prettyTerm dnames tnames (STRING _) = stringD
prettyTerm dnames tnames (Str s _) = prettyStrLit s
prettyTerm _ (STRING _) = stringD
prettyTerm _ (Str s _) = prettyStrLit s
prettyTerm dnames tnames (BOX qty ty _) =
prettyTerm names (BOX qty ty _) =
bracks . hcat =<<
sequence [prettyQty qty, dotD,
withPrec Outer $ prettyTerm dnames tnames ty]
sequence [prettyQty names qty, dotD,
withPrec Outer $ prettyTerm names ty]
prettyTerm dnames tnames (Box val _) =
bracks =<< withPrec Outer (prettyTerm dnames tnames val)
prettyTerm names (Box val _) =
bracks =<< withPrec Outer (prettyTerm names val)
prettyTerm dnames tnames (Let qty rhs body _) = do
prettyTerm names (Let qty rhs body _) = do
let Evidence _ (lets, body) = splitLet [< (qty, body.name, rhs)] body.term
heads <- prettyLets dnames tnames lets
let tnames = tnames . map (\(_, x, _) => x) lets
body <- withPrec Outer $ assert_total prettyTerm dnames tnames body
heads <- prettyLets names lets
let names' = extendTermN' (map (fst . snd) lets) names
body <- withPrec Outer $ assert_total prettyTerm names' body
let lines = toList $ heads :< body
pure $ ifMultiline (hsep lines) (vsep lines)
prettyTerm dnames tnames (E e) =
case the (Elim d n) (pushSubsts' e) of
Ann tm _ _ => assert_total prettyTerm dnames tnames tm
_ => assert_total prettyElim dnames tnames e
prettyTerm names (E e) = do
-- [fixme] do this stuff somewhere else!!!
let Val q = names.qtyLen
case pushSubsts' e {tm = Elim} of
Ann tm _ _ => assert_total prettyTerm names tm
_ => assert_total prettyElim names e
prettyTerm dnames tnames t0@(CloT (Sub t ph)) =
prettyTerm dnames tnames $ assert_smaller t0 $ pushSubstsWith' id ph t
prettyTerm names t0@(CloT (Sub t ph)) = do
let Val q = names.qtyLen
prettyTerm names $ assert_smaller t0 $ pushSubstsWith' id id ph t
prettyTerm dnames tnames t0@(DCloT (Sub t ph)) =
prettyTerm dnames tnames $ assert_smaller t0 $ pushSubstsWith' ph id t
prettyTerm names t0@(DCloT (Sub t ph)) = do
let Val q = names.qtyLen
prettyTerm names $ assert_smaller t0 $ pushSubstsWith' id ph id t
prettyElim dnames tnames (F x u _) = do
prettyTerm names t0@(QCloT (SubR t ph)) = do
let Val q = names.qtyLen
prettyTerm names $ assert_smaller t0 $ pushSubstsWith' ph id id t
prettyElim names (F x u _) = do
x <- prettyFree x
u <- prettyDisp u
pure $ maybe x (x <+>) u
prettyElim dnames tnames (B i _) =
prettyTBind $ tnames !!! i
prettyElim names (B i _) =
prettyTBind $ names.tnames !!! i
prettyElim dnames tnames e@(App {}) =
let (f, xs) = splitApps e in
prettyDTApps dnames tnames f xs
prettyElim names e@(App {}) = do
let Val q = names.qtyLen
(f, xs) = splitApps e
prettyDTApps names f xs
prettyElim dnames tnames (CasePair qty pair ret body _) = do
prettyElim names (CasePair qty pair ret body _) = do
let [< x, y] = body.names
pat <- parens . hsep =<< sequence
[[|prettyTBind x <+> commaD|], prettyTBind y]
prettyCase dnames tnames qty pair ret
pat <- parens $ !(prettyTBind x) <+> !commaD <++> !(prettyTBind y)
prettyCase names qty pair ret
[MkCaseArm pat [<] [< x, y] body.term]
prettyElim dnames tnames (Fst pair _) =
parensIfM App =<< do
pair <- prettyTArg dnames tnames (E pair)
prettyElim names (Fst pair _) = do
pair <- prettyTArg names (E pair)
prettyAppD !fstD [pair]
prettyElim dnames tnames (Snd pair _) =
parensIfM App =<< do
pair <- prettyTArg dnames tnames (E pair)
prettyElim names (Snd pair _) = do
pair <- prettyTArg names (E pair)
prettyAppD !sndD [pair]
prettyElim dnames tnames (CaseEnum qty tag ret arms _) = do
prettyElim names (CaseEnum qty tag ret arms _) = do
arms <- for (SortedMap.toList arms) $ \(tag, body) =>
pure $ MkCaseArm !(prettyTag tag) [<] [<] body
prettyCase dnames tnames qty tag ret arms
prettyCase names qty tag ret arms
prettyElim dnames tnames (CaseNat qty qtyIH nat ret zero succ _) = do
prettyElim names (CaseNat qty qtyIH nat ret zero succ _) = do
let zarm = MkCaseArm !zeroD [<] [<] zero
[< p, ih] = succ.names
spat0 <- [|succD <++> prettyTBind p|]
ihpat0 <- map hcat $ sequence [prettyQty qtyIH, dotD, prettyTBind ih]
ihpat0 <- map hcat $ sequence [prettyQty names qtyIH, dotD, prettyTBind ih]
spat <- if ih.val == Unused
then pure spat0
else pure $ hsep [spat0 <+> !commaD, ihpat0]
else pure $ spat0 <+> !commaD <++> ihpat0
let sarm = MkCaseArm spat [<] [< p, ih] succ.term
prettyCase dnames tnames qty nat ret [zarm, sarm]
prettyCase names qty nat ret [zarm, sarm]
prettyElim dnames tnames (CaseBox qty box ret body _) = do
prettyElim names (CaseBox qty box ret body _) = do
pat <- bracks =<< prettyTBind body.name
let arm = MkCaseArm pat [<] [< body.name] body.term
prettyCase dnames tnames qty box ret [arm]
prettyCase names qty box ret [arm]
prettyElim dnames tnames e@(DApp {}) =
let (f, xs) = splitApps e in
prettyDTApps dnames tnames f xs
prettyElim names e@(DApp {}) = do
let Val q = names.qtyLen
(f, xs) = splitApps e
prettyDTApps names f xs
prettyElim dnames tnames (Ann tm ty _) =
case the (Term d n) (pushSubsts' tm) of
E e => assert_total prettyElim dnames tnames e
prettyElim names (Ann tm ty _) = do
-- [fixme] do this stuff somewhere else!!!
let Val q = names.qtyLen
case pushSubsts' tm {tm = Term} of
E e => assert_total prettyElim names e
_ => do
tm <- withPrec AnnL $ assert_total prettyTerm dnames tnames tm
ty <- withPrec Outer $ assert_total prettyTerm dnames tnames ty
tm <- withPrec AnnL $ assert_total prettyTerm names tm
ty <- withPrec Outer $ assert_total prettyTerm names ty
parensIfM Outer =<< hangDSingle (tm <++> !annD) ty
prettyElim dnames tnames (Coe ty p q val _) =
parensIfM App =<< do
ty <- prettyTypeLine dnames tnames ty
p <- prettyDArg dnames p
q <- prettyDArg dnames q
val <- prettyTArg dnames tnames val
prettyAppD !coeD [ty, sep [p, q], val]
prettyElim names (Coe ty p p' val _) = do
ty <- prettyTypeLine names ty
p <- prettyDArg names p
p' <- prettyDArg names p'
val <- prettyTArg names val
prettyAppD !coeD [ty, p <++> p', val]
prettyElim dnames tnames e@(Comp ty p q val r zero one _) =
parensIfM App =<< do
ty <- assert_total $ prettyTypeLine dnames tnames $ SN ty
pq <- sep <$> sequence [prettyDArg dnames p, prettyDArg dnames q]
val <- prettyTArg dnames tnames val
r <- prettyDArg dnames r
arm0 <- [|prettyCompArm dnames tnames Zero zero <+> semiD|]
arm1 <- prettyCompArm dnames tnames One one
prettyElim names e@(Comp ty p p' val r zero one _) = do
ty <- assert_total $ prettyTypeLine names $ SN ty
pp <- [|prettyDArg names p <++> prettyDArg names p'|]
val <- prettyTArg names val
r <- prettyDArg names r
arm0 <- [|prettyCompArm names Zero zero <+> semiD|]
arm1 <- prettyCompArm names One one
ind <- askAt INDENT
layoutComp [ty, pq] val r [arm0, arm1]
parensIfM App =<< layoutComp [ty, pp] val r [arm0, arm1]
prettyElim dnames tnames (TypeCase ty ret arms def _) = do
prettyElim names (TypeCase ty ret arms def _) = do
arms <- for (toList arms) $ \(k ** body) => do
pat <- prettyTyCasePat k body.names
pure $ MkCaseArm pat [<] (toTel body.names) body.term
let darm = MkCaseArm !undD [<] [<] def
prettyCase_ dnames tnames !typecaseD ty (SN ret) $ arms ++ [darm]
prettyCase_ names !typecaseD ty (SN ret) $ arms ++ [darm]
prettyElim dnames tnames e0@(CloE (Sub e ph)) =
prettyElim dnames tnames $ assert_smaller e0 $ pushSubstsWith' id ph e
prettyElim names e0@(CloE (Sub e ph)) = do
let Val q = names.qtyLen
prettyElim names $ assert_smaller e0 $ pushSubstsWith' id id ph e
prettyElim dnames tnames e0@(DCloE (Sub e ph)) =
prettyElim dnames tnames $ assert_smaller e0 $ pushSubstsWith' ph id e
prettyElim names e0@(DCloE (Sub e ph)) = do
let Val q = names.qtyLen
prettyElim names $ assert_smaller e0 $ pushSubstsWith' id ph id e
prettyElim names e0@(QCloE (SubR e ph)) = do
let Val q = names.qtyLen
prettyElim names $ assert_smaller e0 $ pushSubstsWith' ph id id e

358
lib/Quox/Syntax/Term/Subst.idr
View file

@ -6,10 +6,42 @@ import Data.SnocVect
%default total
namespace CanQSubst
public export
interface CanQSubst (0 tm : TermLike) where
(//) : {q1, q2 : Nat} -> tm q1 d n -> Lazy (QSubst q1 q2) -> tm q2 d n
||| does the minimal reasonable work:
||| - deletes the closure around an atomic constant like `TYPE`
||| - deletes an identity substitution
||| - composes (lazily) with an existing top-level dim-closure
||| - otherwise, wraps in a new closure
export
CanQSubst Term where
s // Shift SZ = s
TYPE l loc // _ = TYPE l loc
QCloT (SubR s ph) // th = QCloT $ SubR s $ ph .? th
s // th = QCloT $ SubR s th
||| does the minimal reasonable work:
||| - deletes the closure around a term variable
||| - deletes an identity substitution
||| - composes (lazily) with an existing top-level dim-closure
||| - immediately looks up bound variables in a
||| top-level sequence of dimension applications
||| - otherwise, wraps in a new closure
export
CanQSubst Elim where
e // Shift SZ = e
F x u loc // _ = F x u loc -- [todo] q args
B i loc // _ = B i loc
QCloE (SubR e ph) // th = QCloE $ SubR e $ ph .? th
e // th = QCloE $ SubR e th
namespace CanDSubst
public export
interface CanDSubst (0 tm : TermLike) where
(//) : tm d1 n -> Lazy (DSubst d1 d2) -> tm d2 n
(//) : tm q d1 n -> Lazy (DSubst d1 d2) -> tm q d2 n
||| does the minimal reasonable work:
||| - deletes the closure around an atomic constant like `TYPE`
@ -24,7 +56,7 @@ CanDSubst Term where
s // th = DCloT $ Sub s th
private
subDArgs : Elim d1 n -> DSubst d1 d2 -> Elim d2 n
subDArgs : Elim q d1 n -> DSubst d1 d2 -> Elim q d2 n
subDArgs (DApp f d loc) th = DApp (subDArgs f th) (d // th) loc
subDArgs e th = DCloE $ Sub e th
@ -44,25 +76,61 @@ CanDSubst Elim where
DCloE (Sub e ph) // th = DCloE $ Sub e $ ph . th
e // th = DCloE $ Sub e th
namespace QSubst.ScopeTermN
export %inline
(//) : {q1, q2 : Nat} -> ScopeTermN s q1 d n -> Lazy (QSubst q1 q2) ->
ScopeTermN s q2 d n
S ns (Y body) // th = S ns $ Y $ body // th
S ns (N body) // th = S ns $ N $ body // th
namespace DSubst.ScopeTermN
export %inline
(//) : ScopeTermN s d1 n -> Lazy (DSubst d1 d2) ->
ScopeTermN s d2 n
(//) : ScopeTermN s q d1 n -> Lazy (DSubst d1 d2) ->
ScopeTermN s q d2 n
S ns (Y body) // th = S ns $ Y $ body // th
S ns (N body) // th = S ns $ N $ body // th
namespace QSubst.DScopeTermN
export %inline
(//) : {q1, q2 : Nat} -> DScopeTermN s q1 d n -> Lazy (QSubst q1 q2) ->
DScopeTermN s q2 d n
S ns (Y body) // th = S ns $ Y $ body // th
S ns (N body) // th = S ns $ N $ body // th
namespace DSubst.DScopeTermN
export %inline
(//) : {s : Nat} ->
DScopeTermN s d1 n -> Lazy (DSubst d1 d2) ->
DScopeTermN s d2 n
DScopeTermN s q d1 n -> Lazy (DSubst d1 d2) ->
DScopeTermN s q d2 n
S ns (Y body) // th = S ns $ Y $ body // pushN s (locs $ toList' ns) th
S ns (N body) // th = S ns $ N $ body // th
export %inline FromVar (Elim d) where fromVarLoc = B
export %inline FromVar (Term d) where fromVarLoc = E .: fromVarLoc
export %inline
FromVarR (Elim q d) where fromVarR = B
export %inline
FromVar (Elim q d) where fromVar = B; fromVarSame _ _ = Refl
export %inline
FromVarR (Term q d) where fromVarR = E .: fromVarR
export %inline
FromVar (Term q d) where fromVar = E .: fromVar; fromVarSame _ _ = Refl
export
CanSubstSelf (Elim q d)
private
tsubstElim : Elim q d from -> Lazy (TSubst q d from to) -> Elim q d to
tsubstElim (F x u loc) _ = F x u loc
tsubstElim (B i loc) th = get th i loc
tsubstElim (CloE (Sub e ph)) th = assert_total CloE $ Sub e $ ph . th
tsubstElim e th =
case force th of
Shift SZ => e
th => CloE $ Sub e th
||| does the minimal reasonable work:
||| - deletes the closure around a *free* name
@ -70,19 +138,15 @@ export %inline FromVar (Term d) where fromVarLoc = E .: fromVarLoc
||| - composes (lazily) with an existing top-level closure
||| - immediately looks up a bound variable
||| - otherwise, wraps in a new closure
CanSubstSelfR (Elim q d) where (//?) = tsubstElim
export
CanSubstSelf (Elim d) where
F x u loc // _ = F x u loc
B i loc // th = getLoc th i loc
CloE (Sub e ph) // th = assert_total CloE $ Sub e $ ph . th
e // th = case force th of
Shift SZ => e
th => CloE $ Sub e th
CanSubstSelf (Elim q d) where (//) = tsubstElim; substSame _ _ = Refl
namespace CanTSubst
public export
interface CanTSubst (0 tm : TermLike) where
(//) : tm d n1 -> Lazy (TSubst d n1 n2) -> tm d n2
(//) : tm q d n1 -> Lazy (TSubst q d n1 n2) -> tm q d n2
||| does the minimal reasonable work:
||| - deletes the closure around an atomic constant like `TYPE`
@ -102,69 +166,89 @@ CanTSubst Term where
namespace ScopeTermN
export %inline
(//) : {s : Nat} ->
ScopeTermN s d n1 -> Lazy (TSubst d n1 n2) ->
ScopeTermN s d n2
ScopeTermN s q d n1 -> Lazy (TSubst q d n1 n2) ->
ScopeTermN s q d n2
S ns (Y body) // th = S ns $ Y $ body // pushN s (locs $ toList' ns) th
S ns (N body) // th = S ns $ N $ body // th
namespace DScopeTermN
export %inline
(//) : {s : Nat} ->
DScopeTermN s d n1 -> Lazy (TSubst d n1 n2) -> DScopeTermN s d n2
DScopeTermN s q d n1 -> Lazy (TSubst q d n1 n2) ->
DScopeTermN s q d n2
S ns (Y body) // th = S ns $ Y $ body // map (// shift s) th
S ns (N body) // th = S ns $ N $ body // th
export %inline CanShift (Term d) where s // by = s // Shift by
export %inline CanShift (Elim d) where e // by = e // Shift by
export %inline CanShift (Term q d) where s // by = s // Shift by
export %inline CanShift (Elim q d) where e // by = e // Shift by
export %inline CanShift (flip Term n) where s // by = s // Shift by
export %inline CanShift (flip Elim n) where e // by = e // Shift by
-- -- from is not accessible in this context
-- export %inline CanShift (\q => Term q d n) where s // by = s // Shift by
-- export %inline CanShift (\q => Elim q d n) where e // by = e // Shift by
export %inline CanShift (\d => Term q d n) where s // by = s // Shift by
export %inline CanShift (\d => Elim q d n) where e // by = e // Shift by
export %inline
{s : Nat} -> CanShift (ScopeTermN s d) where
{s : Nat} -> CanShift (ScopeTermN s q d) where
b // by = b // Shift by
export %inline
comp : DSubst d1 d2 -> TSubst d1 n1 mid -> TSubst d2 mid n2 -> TSubst d2 n1 n2
comp th ps ph = map (// th) ps . ph
comp : {q1, q2 : Nat} ->
QSubst q1 q2 -> DSubst d1 d2 ->
TSubst q1 d1 n1 mid -> TSubst q2 d2 mid n2 -> TSubst q2 d2 n1 n2
comp th ph ps ps' = map (\t => t // th // ph) ps . ps'
-- export %inline
-- compD : DSubst d1 d2 -> TSubst q d1 n1 mid ->
-- TSubst q d2 mid n2 -> TSubst q d2 n1 n2
-- compD th ps ph = map (// th) ps . ph
-- export %inline
-- compQ : {q1, q2 : Nat} -> QSubst q1 q2 -> TSubst q1 d n1 mid ->
-- TSubst q2 d mid n2 -> TSubst q2 d n1 n2
-- compQ th ps ph = map (// th) ps . ph
public export %inline
dweakT : (by : Nat) -> Term d n -> Term (by + d) n
dweakT : (by : Nat) -> Term q d n -> Term q (by + d) n
dweakT by t = t // shift by
public export %inline
dweakS : (by : Nat) -> ScopeTermN s d n -> ScopeTermN s (by + d) n
dweakS : (by : Nat) -> ScopeTermN s q d n -> ScopeTermN s q (by + d) n
dweakS by t = t // shift by
public export %inline
dweakDS : {s : Nat} -> (by : Nat) ->
DScopeTermN s d n -> DScopeTermN s (by + d) n
DScopeTermN s q d n -> DScopeTermN s q (by + d) n
dweakDS by t = t // shift by
public export %inline
dweakE : (by : Nat) -> Elim d n -> Elim (by + d) n
dweakE : (by : Nat) -> Elim q d n -> Elim q (by + d) n
dweakE by t = t // shift by
public export %inline
weakT : (by : Nat) -> Term d n -> Term d (by + n)
weakT : (by : Nat) -> Term q d n -> Term q d (by + n)
weakT by t = t // shift by
public export %inline
weakS : {s : Nat} -> (by : Nat) -> ScopeTermN s d n -> ScopeTermN s d (by + n)
weakS : {s : Nat} -> (by : Nat) ->
ScopeTermN s q d n -> ScopeTermN s q d (by + n)
weakS by t = t // shift by
public export %inline
weakDS : {s : Nat} -> (by : Nat) ->
DScopeTermN s d n -> DScopeTermN s d (by + n)
DScopeTermN s q d n -> DScopeTermN s q d (by + n)
weakDS by t = t // shift by
public export %inline
weakE : (by : Nat) -> Elim d n -> Elim d (by + n)
weakE : (by : Nat) -> Elim q d n -> Elim q d (by + n)
weakE by t = t // shift by
-- no weakQ etc because no first-class binder to push under
parameters {auto _ : CanShift f} {s : Nat}
export %inline
@ -188,69 +272,74 @@ namespace ScopeTermN
t.term0 = getTerm0 t.body
export %inline
subN : ScopeTermN s d n -> SnocVect s (Elim d n) -> Term d n
subN : ScopeTermN s q d n -> SnocVect s (Elim q d n) -> Term q d n
subN (S _ (Y body)) es = body // fromSnocVect es
subN (S _ (N body)) _ = body
export %inline
sub1 : ScopeTerm d n -> Elim d n -> Term d n
sub1 : ScopeTerm q d n -> Elim q d n -> Term q d n
sub1 t e = subN t [< e]
export %inline
dsubN : DScopeTermN s d n -> SnocVect s (Dim d) -> Term d n
dsubN : DScopeTermN s q d n -> SnocVect s (Dim d) -> Term q d n
dsubN (S _ (Y body)) ps = body // fromSnocVect ps
dsubN (S _ (N body)) _ = body
export %inline
dsub1 : DScopeTerm d n -> Dim d -> Term d n
dsub1 : DScopeTerm q d n -> Dim d -> Term q d n
dsub1 t p = dsubN t [< p]
public export %inline
(.zero) : (body : DScopeTerm d n) -> {default body.loc loc : Loc} -> Term d n
(.zero) : (body : DScopeTerm q d n) -> {default body.loc loc : Loc} ->
Term q d n
body.zero = dsub1 body $ K Zero loc
public export %inline
(.one) : (body : DScopeTerm d n) -> {default body.loc loc : Loc} -> Term d n
(.one) : (body : DScopeTerm q d n) -> {default body.loc loc : Loc} ->
Term q d n
body.one = dsub1 body $ K One loc
public export
0 CloTest : TermLike -> Type
CloTest tm = forall d, n. tm d n -> Bool
CloTest tm = forall q, d, n. tm q d n -> Bool
public export
interface PushSubsts (0 tm : TermLike) (0 isClo : CloTest tm) | tm where
pushSubstsWith : DSubst d1 d2 -> TSubst d2 n1 n2 ->
tm d1 n1 -> Subset (tm d2 n2) (No . isClo)
pushSubstsWith : {q1, q2 : Nat} ->
QSubst q1 q2 -> DSubst d1 d2 -> TSubst q2 d2 n1 n2 ->
tm q1 d1 n1 -> Subset (tm q2 d2 n2) (No . isClo)
public export
0 NotClo : {isClo : CloTest tm} -> PushSubsts tm isClo => Pred (tm d n)
0 NotClo : {isClo : CloTest tm} -> PushSubsts tm isClo => Pred (tm q d n)
NotClo = No . isClo
public export
0 NonClo : (tm : TermLike) -> {isClo : CloTest tm} ->
PushSubsts tm isClo => TermLike
NonClo tm d n = Subset (tm d n) NotClo
NonClo tm q d n = Subset (tm q d n) NotClo
public export %inline
nclo : {isClo : CloTest tm} -> (0 _ : PushSubsts tm isClo) =>
(t : tm d n) -> (0 nc : NotClo t) => NonClo tm d n
(t : tm q d n) -> (0 nc : NotClo t) => NonClo tm q d n
nclo t = Element t nc
parameters {0 isClo : CloTest tm} {auto _ : PushSubsts tm isClo}
||| if the input term has any top-level closures, push them under one layer of
||| syntax
export %inline
pushSubsts : tm d n -> NonClo tm d n
pushSubsts s = pushSubstsWith id id s
pushSubsts : {q : Nat} -> tm q d n -> NonClo tm q d n
pushSubsts s = pushSubstsWith id id id s
export %inline
pushSubstsWith' : DSubst d1 d2 -> TSubst d2 n1 n2 -> tm d1 n1 -> tm d2 n2
pushSubstsWith' th ph x = fst $ pushSubstsWith th ph x
pushSubstsWith' : {q1, q2 : Nat} ->
QSubst q1 q2 -> DSubst d1 d2 -> TSubst q2 d2 n1 n2 ->
tm q1 d1 n1 -> tm q2 d2 n2
pushSubstsWith' th ph ps x = fst $ pushSubstsWith th ph ps x
export %inline
pushSubsts' : tm d n -> tm d n
pushSubsts' : {q : Nat} -> tm q d n -> tm q d n
pushSubsts' s = fst $ pushSubsts s
mutual
@ -258,6 +347,7 @@ mutual
isCloT : CloTest Term
isCloT (CloT {}) = True
isCloT (DCloT {}) = True
isCloT (QCloT {}) = True
isCloT (E e) = isCloE e
isCloT _ = False
@ -265,92 +355,118 @@ mutual
isCloE : CloTest Elim
isCloE (CloE {}) = True
isCloE (DCloE {}) = True
isCloE (QCloE {}) = True
isCloE _ = False
export
PushSubsts Elim Subst.isCloE where
pushSubstsWith th ph (F x u loc) =
pushSubstsWith th ph ps (F x u loc) =
nclo $ F x u loc
pushSubstsWith th ph (B i loc) =
let res = getLoc ph i loc in
pushSubstsWith th ph ps (B i loc) =
let res = get ps i loc in
case nchoose $ isCloE res of
Left yes => assert_total pushSubsts res
Right no => Element res no
pushSubstsWith th ph (App f s loc) =
nclo $ App (f // th // ph) (s // th // ph) loc
pushSubstsWith th ph (CasePair pi p r b loc) =
nclo $ CasePair pi (p // th // ph) (r // th // ph) (b // th // ph) loc
pushSubstsWith th ph (Fst pair loc) =
nclo $ Fst (pair // th // ph) loc
pushSubstsWith th ph (Snd pair loc) =
nclo $ Snd (pair // th // ph) loc
pushSubstsWith th ph (CaseEnum pi t r arms loc) =
nclo $ CaseEnum pi (t // th // ph) (r // th // ph)
(map (\b => b // th // ph) arms) loc
pushSubstsWith th ph (CaseNat pi pi' n r z s loc) =
nclo $ CaseNat pi pi' (n // th // ph) (r // th // ph)
(z // th // ph) (s // th // ph) loc
pushSubstsWith th ph (CaseBox pi x r b loc) =
nclo $ CaseBox pi (x // th // ph) (r // th // ph) (b // th // ph) loc
pushSubstsWith th ph (DApp f d loc) =
nclo $ DApp (f // th // ph) (d // th) loc
pushSubstsWith th ph (Ann s a loc) =
nclo $ Ann (s // th // ph) (a // th // ph) loc
pushSubstsWith th ph (Coe ty p q val loc) =
nclo $ Coe (ty // th // ph) (p // th) (q // th) (val // th // ph) loc
pushSubstsWith th ph (Comp ty p q val r zero one loc) =
nclo $ Comp (ty // th // ph) (p // th) (q // th)
(val // th // ph) (r // th)
(zero // th // ph) (one // th // ph) loc
pushSubstsWith th ph (TypeCase ty ret arms def loc) =
nclo $ TypeCase (ty // th // ph) (ret // th // ph)
(map (\t => t // th // ph) arms) (def // th // ph) loc
pushSubstsWith th ph (CloE (Sub e ps)) =
pushSubstsWith th (comp th ps ph) e
pushSubstsWith th ph (DCloE (Sub e ps)) =
pushSubstsWith (ps . th) ph e
pushSubstsWith th ph ps (App f s loc) =
nclo $ App (f // th // ph // ps) (s // th // ph // ps) loc
pushSubstsWith th ph ps (CasePair pi p r b loc) =
nclo $ CasePair (pi //? th)
(p // th // ph // ps)
(r // th // ph // ps)
(b // th // ph // ps) loc
pushSubstsWith th ph ps (Fst pair loc) =
nclo $ Fst (pair // th // ph // ps) loc
pushSubstsWith th ph ps (Snd pair loc) =
nclo $ Snd (pair // th // ph // ps) loc
pushSubstsWith th ph ps (CaseEnum pi t r arms loc) =
nclo $ CaseEnum (pi //? th)
(t // th // ph // ps)
(r // th // ph // ps)
(map (\b => b // th // ph // ps) arms) loc
pushSubstsWith th ph ps (CaseNat pi pi' n r z s loc) =
nclo $ CaseNat (pi //? th) (pi' //? th)
(n // th // ph // ps)
(r // th // ph // ps)
(z // th // ph // ps)
(s // th // ph // ps) loc
pushSubstsWith th ph ps (CaseBox pi x r b loc) =
nclo $ CaseBox (pi //? th)
(x // th // ph // ps)
(r // th // ph // ps)
(b // th // ph // ps) loc
pushSubstsWith th ph ps (DApp f d loc) =
nclo $ DApp (f // th // ph // ps) (d // ph) loc
pushSubstsWith th ph ps (Ann s a loc) =
nclo $ Ann (s // th // ph // ps) (a // th // ph // ps) loc
pushSubstsWith th ph ps (Coe ty p q val loc) =
nclo $ Coe
(ty // th // ph // ps)
(p // ph) (q // ph)
(val // th // ph // ps) loc
pushSubstsWith th ph ps (Comp ty p q val r zero one loc) =
nclo $ Comp (ty // th // ph // ps) (p // ph) (q // ph)
(val // th // ph // ps) (r // ph)
(zero // th // ph // ps) (one // th // ph // ps) loc
pushSubstsWith th ph ps (TypeCase ty ret arms def loc) =
nclo $ TypeCase (ty // th // ph // ps) (ret // th // ph // ps)
(map (\t => t // th // ph // ps) arms) (def // th // ph // ps) loc
pushSubstsWith th ph ps (CloE (Sub e ps')) =
pushSubstsWith th ph (comp th ph ps' ps) e
pushSubstsWith th ph ps (DCloE (Sub e ph')) =
pushSubstsWith th (ph' . ph) ps e
pushSubstsWith th ph ps (QCloE (SubR e th')) =
pushSubstsWith (th' .? th) ph ps e
export
PushSubsts Term Subst.isCloT where
pushSubstsWith th ph (TYPE l loc) =
pushSubstsWith th ph ps (TYPE l loc) =
nclo $ TYPE l loc
pushSubstsWith th ph (IOState loc) =
pushSubstsWith _ _ _ (IOState loc) =
nclo $ IOState loc
pushSubstsWith th ph (Pi qty a body loc) =
nclo $ Pi qty (a // th // ph) (body // th // ph) loc
pushSubstsWith th ph (Lam body loc) =
nclo $ Lam (body // th // ph) loc
pushSubstsWith th ph (Sig a b loc) =
nclo $ Sig (a // th // ph) (b // th // ph) loc
pushSubstsWith th ph (Pair s t loc) =
nclo $ Pair (s // th // ph) (t // th // ph) loc
pushSubstsWith th ph (Enum tags loc) =
pushSubstsWith th ph ps (Pi qty a body loc) =
nclo $ Pi (qty //? th)
(a // th // ph // ps)
(body // th // ph // ps) loc
pushSubstsWith th ph ps (Lam body loc) =
nclo $ Lam (body // th // ph // ps) loc
pushSubstsWith th ph ps (Sig a b loc) =
nclo $ Sig (a // th // ph // ps) (b // th // ph // ps) loc
pushSubstsWith th ph ps (Pair s t loc) =
nclo $ Pair (s // th // ph // ps) (t // th // ph // ps) loc
pushSubstsWith th ph ps (Enum tags loc) =
nclo $ Enum tags loc
pushSubstsWith th ph (Tag tag loc) =
pushSubstsWith th ph ps (Tag tag loc) =
nclo $ Tag tag loc
pushSubstsWith th ph (Eq ty l r loc) =
nclo $ Eq (ty // th // ph) (l // th // ph) (r // th // ph) loc
pushSubstsWith th ph (DLam body loc) =
nclo $ DLam (body // th // ph) loc
pushSubstsWith _ _ (NAT loc) =
pushSubstsWith th ph ps (Eq ty l r loc) =
nclo $ Eq
(ty // th // ph // ps)
(l // th // ph // ps)
(r // th // ph // ps) loc
pushSubstsWith th ph ps (DLam body loc) =
nclo $ DLam (body // th // ph // ps) loc
pushSubstsWith _ _ _ (NAT loc) =
nclo $ NAT loc
pushSubstsWith _ _ (Nat n loc) =
pushSubstsWith _ _ _ (Nat n loc) =
nclo $ Nat n loc
pushSubstsWith th ph (Succ n loc) =
nclo $ Succ (n // th // ph) loc
pushSubstsWith _ _ (STRING loc) =
pushSubstsWith th ph ps (Succ n loc) =
nclo $ Succ (n // th // ph // ps) loc
pushSubstsWith _ _ _ (STRING loc) =
nclo $ STRING loc
pushSubstsWith _ _ (Str s loc) =
pushSubstsWith _ _ _ (Str s loc) =
nclo $ Str s loc
pushSubstsWith th ph (BOX pi ty loc) =
nclo $ BOX pi (ty // th // ph) loc
pushSubstsWith th ph (Box val loc) =
nclo $ Box (val // th // ph) loc
pushSubstsWith th ph (E e) =
let Element e nc = pushSubstsWith th ph e in nclo $ E e
pushSubstsWith th ph (Let qty rhs body loc) =
nclo $ Let qty (rhs // th // ph) (body // th // ph) loc
pushSubstsWith th ph (CloT (Sub s ps)) =
pushSubstsWith th (comp th ps ph) s
pushSubstsWith th ph (DCloT (Sub s ps)) =
pushSubstsWith (ps . th) ph s
pushSubstsWith th ph ps (BOX pi ty loc) =
nclo $ BOX (pi //? th) (ty // th // ph // ps) loc
pushSubstsWith th ph ps (Box val loc) =
nclo $ Box (val // th // ph // ps) loc
pushSubstsWith th ph ps (E e) =
let Element e nc = pushSubstsWith th ph ps e in nclo $ E e
pushSubstsWith th ph ps (Let qty rhs body loc) =
nclo $ Let (qty //? th)
(rhs // th // ph // ps)
(body // th // ph // ps) loc
pushSubstsWith th ph ps (CloT (Sub s ps')) =
pushSubstsWith th ph (comp th ph ps' ps) s
pushSubstsWith th ph ps (DCloT (Sub s ph')) =
pushSubstsWith th (ph' . ph) ps s
pushSubstsWith th ph ps (QCloT (SubR s th')) =
pushSubstsWith (th' .? th) ph ps s

118
lib/Quox/Syntax/Term/Tighten.idr
View file

@ -29,20 +29,20 @@ tightenDScope f p (S names (N body)) = S names . N <$> f p body
mutual
private
tightenT : OPE n1 n2 -> Term d n2 -> Maybe (Term d n1)
tightenT : {q : Nat} -> OPE n1 n2 -> Term q d n2 -> Maybe (Term q d n1)
tightenT p s =
let Element s' _ = pushSubsts s in
tightenT' p $ assert_smaller s s'
private
tightenE : OPE n1 n2 -> Elim d n2 -> Maybe (Elim d n1)
tightenE : {q : Nat} -> OPE n1 n2 -> Elim q d n2 -> Maybe (Elim q d n1)
tightenE p e =
let Element e' _ = pushSubsts e in
tightenE' p $ assert_smaller e e'
private
tightenT' : OPE n1 n2 -> (t : Term d n2) -> (0 nt : NotClo t) =>
Maybe (Term d n1)
tightenT' : {q : Nat} -> OPE n1 n2 -> (t : Term q d n2) -> (0 nt : NotClo t) =>
Maybe (Term q d n1)
tightenT' p (TYPE l loc) = pure $ TYPE l loc
tightenT' p (IOState loc) = pure $ IOState loc
tightenT' p (Pi qty arg res loc) =
@ -81,8 +81,9 @@ mutual
E <$> assert_total tightenE p e
private
tightenE' : OPE n1 n2 -> (e : Elim d n2) -> (0 ne : NotClo e) =>
Maybe (Elim d n1)
tightenE' : {q : Nat} ->
OPE n1 n2 -> (e : Elim q d n2) -> (0 ne : NotClo e) =>
Maybe (Elim q d n1)
tightenE' p (F x u loc) =
pure $ F x u loc
tightenE' p (B i loc) =
@ -140,34 +141,35 @@ mutual
<*> pure loc
export
tightenS : {s : Nat} -> OPE m n ->
ScopeTermN s f n -> Maybe (ScopeTermN s f m)
tightenS : {q, s : Nat} -> OPE m n ->
ScopeTermN s q d n -> Maybe (ScopeTermN s q d m)
tightenS = assert_total $ tightenScope tightenT
export
tightenDS : OPE m n -> DScopeTermN s f n -> Maybe (DScopeTermN s f m)
tightenDS = assert_total $ tightenDScope tightenT {f = \n, d => Term d n}
tightenDS : {q : Nat} ->
OPE m n -> DScopeTermN s q d n -> Maybe (DScopeTermN s q d m)
tightenDS = assert_total $ tightenDScope tightenT {f = \n, d => Term q d n}
export Tighten (Elim d) where tighten p e = tightenE p e
export Tighten (Term d) where tighten p t = tightenT p t
export {q : Nat} -> Tighten (Elim q d) where tighten p e = tightenE p e
export {q : Nat} -> Tighten (Term q d) where tighten p t = tightenT p t
mutual
export
dtightenT : OPE d1 d2 -> Term d2 n -> Maybe (Term d1 n)
dtightenT : {q : Nat} -> OPE d1 d2 -> Term q d2 n -> Maybe (Term q d1 n)
dtightenT p s =
let Element s' _ = pushSubsts s in
dtightenT' p $ assert_smaller s s'
export
dtightenE : OPE d1 d2 -> Elim d2 n -> Maybe (Elim d1 n)
dtightenE : {q : Nat} -> OPE d1 d2 -> Elim q d2 n -> Maybe (Elim q d1 n)
dtightenE p e =
let Element e' _ = pushSubsts e in
dtightenE' p $ assert_smaller e e'
private
dtightenT' : OPE d1 d2 -> (t : Term d2 n) -> (0 nt : NotClo t) =>
Maybe (Term d1 n)
dtightenT' : {q : Nat} -> OPE d1 d2 -> (t : Term q d2 n) -> (0 nt : NotClo t) =>
Maybe (Term q d1 n)
dtightenT' p (TYPE l loc) =
pure $ TYPE l loc
dtightenT' p (IOState loc) =
@ -208,8 +210,8 @@ mutual
E <$> assert_total dtightenE p e
export
dtightenE' : OPE d1 d2 -> (e : Elim d2 n) -> (0 ne : NotClo e) =>
Maybe (Elim d1 n)
dtightenE' : {q : Nat} -> OPE d1 d2 -> (e : Elim q d2 n) -> (0 ne : NotClo e) =>
Maybe (Elim q d1 n)
dtightenE' p (F x u loc) =
pure $ F x u loc
dtightenE' p (B i loc) =
@ -258,17 +260,18 @@ mutual
(traverse (dtightenS p) arms) (dtightenT p def) (pure loc)|]
export
dtightenS : OPE d1 d2 -> ScopeTermN s d2 n -> Maybe (ScopeTermN s d1 n)
dtightenS = assert_total $ tightenDScope dtightenT {f = Term}
dtightenS : {q : Nat} -> OPE d1 d2 -> ScopeTermN s q d2 n ->
Maybe (ScopeTermN s q d1 n)
dtightenS = assert_total $ tightenDScope dtightenT {f = Term q}
export
dtightenDS : {s : Nat} -> OPE d1 d2 ->
DScopeTermN s d2 n -> Maybe (DScopeTermN s d1 n)
dtightenDS : {q, s : Nat} -> OPE d1 d2 ->
DScopeTermN s q d2 n -> Maybe (DScopeTermN s q d1 n)
dtightenDS = assert_total $ tightenScope dtightenT
export Tighten (\d => Term d n) where tighten p t = dtightenT p t
export Tighten (\d => Elim d n) where tighten p e = dtightenE p e
export {q : Nat} -> Tighten (\d => Term q d n) where tighten p t = dtightenT p t
export {q : Nat} -> Tighten (\d => Elim q d n) where tighten p e = dtightenE p e
parameters {auto _ : Tighten f} {s : Nat}
@ -300,59 +303,64 @@ ST : Tighten f => {s : Nat} -> BContext s -> f (s + n) -> Scoped s f n
ST names body = squeeze' $ SY names body
public export %inline
DST : {s : Nat} -> BContext s -> Term (s + d) n -> DScopeTermN s d n
DST names body = dsqueeze' {f = Term} $ SY names body
DST : {s, q : Nat} -> BContext s -> Term q (s + d) n -> DScopeTermN s q d n
DST names body = dsqueeze' {f = Term q} $ SY names body
public export %inline
PiT : (qty : Qty) -> (x : BindName) ->
(arg : Term d n) -> (res : Term d (S n)) -> (loc : Loc) -> Term d n
PiT : {q : Nat} -> (qty : Qty q) -> (x : BindName) ->
(arg : Term q d n) -> (res : Term q d (S n)) -> (loc : Loc) -> Term q d n
PiT {qty, x, arg, res, loc} = Pi {qty, arg, res = ST [< x] res, loc}
public export %inline
LamT : (x : BindName) -> (body : Term d (S n)) -> (loc : Loc) -> Term d n
LamT : {q : Nat} ->
(x : BindName) -> (body : Term q d (S n)) -> (loc : Loc) -> Term q d n
LamT {x, body, loc} = Lam {body = ST [< x] body, loc}
public export %inline
SigT : (x : BindName) -> (fst : Term d n) ->
(snd : Term d (S n)) -> (loc : Loc) -> Term d n
SigT : {q : Nat} -> (x : BindName) -> (fst : Term q d n) ->
(snd : Term q d (S n)) -> (loc : Loc) -> Term q d n
SigT {x, fst, snd, loc} = Sig {fst, snd = ST [< x] snd, loc}
public export %inline
EqT : (i : BindName) -> (ty : Term (S d) n) ->
(l, r : Term d n) -> (loc : Loc) -> Term d n
EqT : {q : Nat} -> (i : BindName) -> (ty : Term q (S d) n) ->
(l, r : Term q d n) -> (loc : Loc) -> Term q d n
EqT {i, ty, l, r, loc} = Eq {ty = DST [< i] ty, l, r, loc}
public export %inline
DLamT : (i : BindName) -> (body : Term (S d) n) -> (loc : Loc) -> Term d n
DLamT : {q : Nat} ->
(i : BindName) -> (body : Term q (S d) n) -> (loc : Loc) -> Term q d n
DLamT {i, body, loc} = DLam {body = DST [< i] body, loc}
public export %inline
CoeT : (i : BindName) -> (ty : Term (S d) n) ->
(p, q : Dim d) -> (val : Term d n) -> (loc : Loc) -> Elim d n
CoeT {i, ty, p, q, val, loc} = Coe {ty = DST [< i] ty, p, q, val, loc}
CoeT : {q : Nat} -> (i : BindName) -> (ty : Term q (S d) n) ->
(p, p' : Dim d) -> (val : Term q d n) -> (loc : Loc) -> Elim q d n
CoeT {i, ty, p, p', val, loc} = Coe {ty = DST [< i] ty, p, p', val, loc}
public export %inline
typeCase1T : Elim d n -> Term d n ->
(k : TyConKind) -> BContext (arity k) -> Term d (arity k + n) ->
typeCase1T : {q : Nat} ->
Elim q d n -> Term q d n ->
(k : TyConKind) -> BContext (arity k) -> Term q d (arity k + n) ->
(loc : Loc) ->
{default (NAT loc) def : Term d n} ->
Elim d n
{default (NAT loc) def : Term q d n} ->
Elim q d n
typeCase1T ty ret k ns body loc {def} =
typeCase ty ret [(k ** ST ns body)] def loc
public export %inline
CompH' : (ty : DScopeTerm d n) -> (p, q : Dim d) -> (val : Term d n) ->
(r : Dim d) -> (zero, one : DScopeTerm d n) -> (loc : Loc) -> Elim d n
CompH' {ty, p, q, val, r, zero, one, loc} =
CompH' : {q : Nat} ->
(ty : DScopeTerm q d n) -> (p, p' : Dim d) -> (val : Term q d n) ->
(r : Dim d) -> (zero, one : DScopeTerm q d n) -> (loc : Loc) ->
Elim q d n
CompH' {ty, p, p', val, r, zero, one, loc} =
let ty' = DST ty.names $ ty.term // (B VZ ty.name.loc ::: shift 2) in
Comp {
ty = dsub1 ty q, p, q,
val = E $ Coe ty p q val val.loc, r,
ty = dsub1 ty p', p, p',
val = E $ Coe ty p p' val val.loc, r,
zero = DST zero.names $ E $
Coe ty' (B VZ zero.loc) (weakD 1 q) zero.term zero.loc,
Coe ty' (B VZ zero.loc) (weakD 1 p') zero.term zero.loc,
one = DST one.names $ E $
Coe ty' (B VZ one.loc) (weakD 1 q) one.term one.loc,
Coe ty' (B VZ one.loc) (weakD 1 p') one.term one.loc,
loc
}
@ -365,12 +373,12 @@ CompH' {ty, p, q, val, r, zero, one, loc} =
||| 1 j ⇒ coe [i ⇒ A] @j @q t₁
||| }
public export %inline
CompH : (i : BindName) -> (ty : Term (S d) n) ->
(p, q : Dim d) -> (val : Term d n) -> (r : Dim d) ->
(j0 : BindName) -> (zero : Term (S d) n) ->
(j1 : BindName) -> (one : Term (S d) n) ->
CompH : {q : Nat} -> (i : BindName) -> (ty : Term q (S d) n) ->
(p, p' : Dim d) -> (val : Term q d n) -> (r : Dim d) ->
(j0 : BindName) -> (zero : Term q (S d) n) ->
(j1 : BindName) -> (one : Term q (S d) n) ->
(loc : Loc) ->
Elim d n
CompH {i, ty, p, q, val, r, j0, zero, j1, one, loc} =
CompH' {ty = DST [< i] ty, p, q, val, r,
Elim q d n
CompH {i, ty, p, p', val, r, j0, zero, j1, one, loc} =
CompH' {ty = DST [< i] ty, p, p', val, r,
zero = DST [< j0] zero, one = DST [< j1] one, loc}

71
lib/Quox/Typing.idr
View file

@ -21,22 +21,22 @@ TTName = TT.Name
public export
CheckResult' : Nat -> Type
CheckResult' : Nat -> Nat -> Type
CheckResult' = QOutput
public export
CheckResult : DimEq d -> Nat -> Type
CheckResult eqs n = IfConsistent eqs $ CheckResult' n
CheckResult : DimEq d -> Nat -> Nat -> Type
CheckResult eqs q n = IfConsistent eqs $ CheckResult' q n
public export
record InferResult' d n where
record InferResult' q d n where
constructor InfRes
type : Term d n
qout : QOutput n
type : Term q d n
qout : QOutput q n
public export
InferResult : DimEq d -> TermLike
InferResult eqs d n = IfConsistent eqs $ InferResult' d n
InferResult eqs q d n = IfConsistent eqs $ InferResult' q d n
export
@ -45,21 +45,22 @@ lookupFree x loc defs = maybe (throw $ NotInScope loc x) pure $ lookup x defs
public export
substCasePairRet : BContext 2 -> Term d n -> ScopeTerm d n -> Term d (2 + n)
substCasePairRet : BContext 2 -> Term q d n -> ScopeTerm q d n ->
Term q d (2 + n)
substCasePairRet [< x, y] dty retty =
let tm = Pair (BVT 1 x.loc) (BVT 0 y.loc) $ x.loc `extendL` y.loc
arg = Ann tm (dty // fromNat 2) tm.loc in
retty.term // (arg ::: shift 2)
public export
substCaseSuccRet : BContext 2 -> ScopeTerm d n -> Term d (2 + n)
substCaseSuccRet : BContext 2 -> ScopeTerm q d n -> Term q d (2 + n)
substCaseSuccRet [< p, ih] retty =
let loc = p.loc `extendL` ih.loc
arg = Ann (Succ (BVT 1 p.loc) p.loc) (NAT p.loc) loc in
retty.term // (arg ::: shift 2)
public export
substCaseBoxRet : BindName -> Term d n -> ScopeTerm d n -> Term d (S n)
substCaseBoxRet : BindName -> Term q d n -> ScopeTerm q d n -> Term q d (S n)
substCaseBoxRet x dty retty =
let arg = Ann (Box (BVT 0 x.loc) x.loc) (weakT 1 dty) x.loc in
retty.term // (arg ::: shift 1)
@ -68,15 +69,15 @@ substCaseBoxRet x dty retty =
private
0 ExpectErrorConstructor : Type
ExpectErrorConstructor =
forall d, n. Loc -> NameContexts d n -> Term d n -> Error
forall q, d, n. Loc -> NameContexts q d n -> Term q d n -> Error
parameters (defs : Definitions)
{auto _ : (Has ErrorEff fs, Has NameGen fs, Has Log fs)}
namespace TyContext
parameters (ctx : TyContext d n) (sg : SQty) (loc : Loc)
parameters (ctx : TyContext q d n) (sg : SQty) (loc : Loc)
export covering
whnf : {0 isRedex : RedexTest tm} -> CanWhnf tm isRedex =>
tm d n -> Eff fs (NonRedex tm d n defs (toWhnfContext ctx) sg)
tm q d n -> Eff fs (NonRedex tm q d n defs (toWhnfContext ctx) sg)
whnf tm = do
let Val n = ctx.termLen; Val d = ctx.dimLen
res <- lift $ runExcept $ whnf defs (toWhnfContext ctx) sg tm
@ -84,7 +85,7 @@ parameters (defs : Definitions)
private covering %macro
expect : ExpectErrorConstructor -> TTImp -> TTImp ->
Elab (Term d n -> Eff fs a)
Elab (Term q d n -> Eff fs a)
expect err pat rhs = Prelude.do
match <- check `(\case ~(pat) => Just ~(rhs); _ => Nothing)
pure $ \term => do
@ -92,54 +93,54 @@ parameters (defs : Definitions)
maybe (throw $ err loc ctx.names term) pure $ match $ fst res
export covering %inline
expectTYPE : Term d n -> Eff fs Universe
expectTYPE : Term q d n -> Eff fs Universe
expectTYPE = expect ExpectedTYPE `(TYPE {l, _}) `(l)
export covering %inline
expectPi : Term d n -> Eff fs (Qty, Term d n, ScopeTerm d n)
expectPi : Term q d n -> Eff fs (Qty q, Term q d n, ScopeTerm q d n)
expectPi = expect ExpectedPi `(Pi {qty, arg, res, _}) `((qty, arg, res))
export covering %inline
expectSig : Term d n -> Eff fs (Term d n, ScopeTerm d n)
expectSig : Term q d n -> Eff fs (Term q d n, ScopeTerm q d n)
expectSig = expect ExpectedSig `(Sig {fst, snd, _}) `((fst, snd))
export covering %inline
expectEnum : Term d n -> Eff fs (SortedSet TagVal)
expectEnum : Term q d n -> Eff fs (SortedSet TagVal)
expectEnum = expect ExpectedEnum `(Enum {cases, _}) `(cases)
export covering %inline
expectEq : Term d n -> Eff fs (DScopeTerm d n, Term d n, Term d n)
expectEq : Term q d n -> Eff fs (DScopeTerm q d n, Term q d n, Term q d n)
expectEq = expect ExpectedEq `(Eq {ty, l, r, _}) `((ty, l, r))
export covering %inline
expectNAT : Term d n -> Eff fs ()
expectNAT : Term q d n -> Eff fs ()
expectNAT = expect ExpectedNAT `(NAT {}) `(())
export covering %inline
expectSTRING : Term d n -> Eff fs ()
expectSTRING : Term q d n -> Eff fs ()
expectSTRING = expect ExpectedSTRING `(STRING {}) `(())
export covering %inline
expectBOX : Term d n -> Eff fs (Qty, Term d n)
expectBOX : Term q d n -> Eff fs (Qty q, Term q d n)
expectBOX = expect ExpectedBOX `(BOX {qty, ty, _}) `((qty, ty))
export covering %inline
expectIOState : Term d n -> Eff fs ()
expectIOState : Term q d n -> Eff fs ()
expectIOState = expect ExpectedIOState `(IOState {}) `(())
namespace EqContext
parameters (ctx : EqContext n) (sg : SQty) (loc : Loc)
parameters (ctx : EqContext q n) (sg : SQty) (loc : Loc)
export covering
whnf : {0 isRedex : RedexTest tm} -> CanWhnf tm isRedex =>
tm 0 n -> Eff fs (NonRedex tm 0 n defs (toWhnfContext ctx) sg)
tm q 0 n -> Eff fs (NonRedex tm q 0 n defs (toWhnfContext ctx) sg)
whnf tm = do
res <- lift $ runExcept $ whnf defs (toWhnfContext ctx) sg tm
rethrow res
private covering %macro
expect : ExpectErrorConstructor -> TTImp -> TTImp ->
Elab (Term 0 n -> Eff fs a)
Elab (Term q 0 n -> Eff fs a)
expect err pat rhs = do
match <- check `(\case ~(pat) => Just ~(rhs); _ => Nothing)
pure $ \term => do
@ -148,37 +149,37 @@ parameters (defs : Definitions)
maybe (throw $ err loc ctx.names t0) pure $ match $ fst res
export covering %inline
expectTYPE : Term 0 n -> Eff fs Universe
expectTYPE : Term q 0 n -> Eff fs Universe
expectTYPE = expect ExpectedTYPE `(TYPE {l, _}) `(l)
export covering %inline
expectPi : Term 0 n -> Eff fs (Qty, Term 0 n, ScopeTerm 0 n)
expectPi : Term q 0 n -> Eff fs (Qty q, Term q 0 n, ScopeTerm q 0 n)
expectPi = expect ExpectedPi `(Pi {qty, arg, res, _}) `((qty, arg, res))
export covering %inline
expectSig : Term 0 n -> Eff fs (Term 0 n, ScopeTerm 0 n)
expectSig : Term q 0 n -> Eff fs (Term q 0 n, ScopeTerm q 0 n)
expectSig = expect ExpectedSig `(Sig {fst, snd, _}) `((fst, snd))
export covering %inline
expectEnum : Term 0 n -> Eff fs (SortedSet TagVal)
expectEnum : Term q 0 n -> Eff fs (SortedSet TagVal)
expectEnum = expect ExpectedEnum `(Enum {cases, _}) `(cases)
export covering %inline
expectEq : Term 0 n -> Eff fs (DScopeTerm 0 n, Term 0 n, Term 0 n)
expectEq : Term q 0 n -> Eff fs (DScopeTerm q 0 n, Term q 0 n, Term q 0 n)
expectEq = expect ExpectedEq `(Eq {ty, l, r, _}) `((ty, l, r))
export covering %inline
expectNAT : Term 0 n -> Eff fs ()
expectNAT : Term q 0 n -> Eff fs ()
expectNAT = expect ExpectedNAT `(NAT {}) `(())
export covering %inline
expectSTRING : Term 0 n -> Eff fs ()
expectSTRING : Term q 0 n -> Eff fs ()
expectSTRING = expect ExpectedSTRING `(STRING {}) `(())
export covering %inline
expectBOX : Term 0 n -> Eff fs (Qty, Term 0 n)
expectBOX : Term q 0 n -> Eff fs (Qty q, Term q 0 n)
expectBOX = expect ExpectedBOX `(BOX {qty, ty, _}) `((qty, ty))
export covering %inline
expectIOState : Term 0 n -> Eff fs ()
expectIOState : Term q 0 n -> Eff fs ()
expectIOState = expect ExpectedIOState `(IOState {}) `(())

337
lib/Quox/Typing/Context.idr
View file

@ -3,7 +3,7 @@ module Quox.Typing.Context
import Quox.Syntax
import Quox.Context
import Quox.Pretty
import public Data.Singleton
import public Quox.SingletonExtra
import Derive.Prelude
%default total
@ -11,48 +11,60 @@ import Derive.Prelude
public export
QContext : Nat -> Type
QContext = Context' Qty
QContext : (q, n : Nat) -> Type
QContext q n = Context' (Qty q) n
public export
record LocalVar d n where
record LocalVar q d n where
constructor MkLocal
type : Term d n
term : Maybe (Term d n) -- if from a `let`
%runElab deriveIndexed "LocalVar" [Show]
type : Term q d n
term : Maybe (Term q d n) -- if from a `let`
-- %runElab deriveIndexed "LocalVar" [Show]
export
[LocateVarType] Located (LocalVar q d n) where x.loc = x.type.loc
namespace LocalVar
export %inline
letVar : (type, term : Term d n) -> LocalVar d n
letVar : (type, term : Term q d n) -> LocalVar q d n
letVar type term = MkLocal {type, term = Just term}
export %inline
lamVar : (type : Term d n) -> LocalVar d n
lamVar : (type : Term q d n) -> LocalVar q d n
lamVar type = MkLocal {type, term = Nothing}
export %inline
mapVar : (Term d n -> Term d' n') -> LocalVar d n -> LocalVar d' n'
mapVar : (Term q d n -> Term q' d' n') -> LocalVar q d n -> LocalVar q' d' n'
mapVar f = {type $= f, term $= map f}
export %inline
subD : DSubst d1 d2 -> LocalVar d1 n -> LocalVar d2 n
subQ : {q1, q2 : Nat} -> QSubst q1 q2 -> LocalVar q1 d n -> LocalVar q2 d n
subQ th = mapVar (// th)
export %inline
weakQ : {q : Nat} -> LocalVar q d n -> LocalVar (S q) d n
weakQ = subQ $ shift 1
export %inline
subD : DSubst d1 d2 -> LocalVar q d1 n -> LocalVar q d2 n
subD th = mapVar (// th)
export %inline
weakD : LocalVar d n -> LocalVar (S d) n
weakD : LocalVar q d n -> LocalVar q (S d) n
weakD = subD $ shift 1
export %inline CanShift (LocalVar d) where l // by = mapVar (// by) l
export %inline CanDSubst LocalVar where l // by = mapVar (// by) l
export %inline CanTSubst LocalVar where l // by = mapVar (// by) l
export %inline CanShift (LocalVar q d) where l // by = mapVar (// by) l
export %inline CanQSubst LocalVar where l // th = mapVar (// th) l
export %inline CanDSubst LocalVar where l // th = mapVar (// th) l
export %inline CanTSubst LocalVar where l // th = mapVar (// th) l
public export
TContext : TermLike
TContext d = Context (LocalVar d)
TContext q d = Context (LocalVar q d)
public export
QOutput : Nat -> Type
QOutput = Context' Qty
QOutput : (q, n : Nat) -> Type
QOutput = QContext
public export
DimAssign : Nat -> Type
@ -60,48 +72,54 @@ DimAssign = Context' DimConst
public export
record TyContext d n where
record TyContext q d n where
constructor MkTyContext
{auto qtyLen : Singleton q}
{auto dimLen : Singleton d}
{auto termLen : Singleton n}
qnames : BContext q -- only used for printing
dctx : DimEq d
dnames : BContext d -- only used for printing
tctx : TContext d n
tctx : TContext q d n
tnames : BContext n -- only used for printing
qtys : QContext n -- only used for printing
qtys : QContext q n -- only used for printing
%name TyContext ctx
%runElab deriveIndexed "TyContext" [Show]
-- %runElab deriveIndexed "TyContext" [Show]
public export
record EqContext n where
record EqContext q n where
constructor MkEqContext
{auto qtyLen : Singleton q}
{dimLen : Nat}
{auto termLen : Singleton n}
qnames : BContext q -- only used for printing
dassign : DimAssign dimLen -- only used for printing
dnames : BContext dimLen -- only used for printing
tctx : TContext 0 n
tctx : TContext q 0 n
tnames : BContext n -- only used for printing
qtys : QContext n -- only used for printing
qtys : QContext q n -- only used for printing
%name EqContext ctx
%runElab deriveIndexed "EqContext" [Show]
-- %runElab deriveIndexed "EqContext" [Show]
public export
record WhnfContext d n where
record WhnfContext q d n where
constructor MkWhnfContext
{auto qtyLen : Singleton q}
{auto dimLen : Singleton d}
{auto termLen : Singleton n}
qnames : BContext q -- only used for printing
dnames : BContext d
tnames : BContext n
tctx : TContext d n
tctx : TContext q d n
%name WhnfContext ctx
%runElab deriveIndexed "WhnfContext" [Show]
-- %runElab deriveIndexed "WhnfContext" [Show]
namespace TContext
export %inline
zeroFor : Context tm n -> QOutput n
zeroFor ctx = Zero <$ ctx
zeroFor : {q : Nat} -> Located1 tm => Context tm n -> QOutput q n
zeroFor = map $ \x => zero x.loc
public export
extendLen : Telescope a n1 n2 -> Singleton n1 -> Singleton n2
@ -110,38 +128,40 @@ extendLen (tel :< _) x = [|S $ extendLen tel x|]
public export
CtxExtension : Nat -> Nat -> Nat -> Type
CtxExtension d = Telescope ((Qty, BindName,) . Term d)
CtxExtension : (q, d, n1, n2 : Nat) -> Type
CtxExtension q d = Telescope $ \n => (Qty q, BindName, Term q d n)
public export
CtxExtension0 : Nat -> Nat -> Nat -> Type
CtxExtension0 d = Telescope ((BindName,) . Term d)
CtxExtension0 : (q, d, n1, n2 : Nat) -> Type
CtxExtension0 q d = Telescope $ \n => (BindName, Term q d n)
public export
CtxExtensionLet : Nat -> Nat -> Nat -> Type
CtxExtensionLet d = Telescope ((Qty, BindName,) . LocalVar d)
CtxExtensionLet : (q, d, n1, n2 : Nat) -> Type
CtxExtensionLet q d = Telescope $ \n => (Qty q, BindName, LocalVar q d n)
public export
CtxExtensionLet0 : Nat -> Nat -> Nat -> Type
CtxExtensionLet0 d = Telescope ((BindName,) . LocalVar d)
CtxExtensionLet0 : (q, d, n1, n2 : Nat) -> Type
CtxExtensionLet0 q d = Telescope $ \n => (BindName, LocalVar q d n)
namespace TyContext
public export %inline
empty : TyContext 0 0
empty : TyContext 0 0 0
empty = MkTyContext {
dctx = new, dnames = [<], tctx = [<], tnames = [<], qtys = [<]
qnames = [<], dctx = new, dnames = [<], tctx = [<], tnames = [<], qtys = [<]
}
public export %inline
null : TyContext d n -> Bool
null ctx = null ctx.dnames && null ctx.tnames
null : TyContext q d n -> Bool
null ctx = null ctx.qnames && null ctx.dnames && null ctx.tnames
export %inline
extendTyLetN : CtxExtensionLet d n1 n2 -> TyContext d n1 -> TyContext d n2
extendTyLetN xss (MkTyContext {termLen, dctx, dnames, tctx, tnames, qtys}) =
extendTyLetN : CtxExtensionLet q d n1 n2 ->
TyContext q d n1 -> TyContext q d n2
extendTyLetN xss
(MkTyContext {termLen, qnames, dctx, dnames, tctx, tnames, qtys}) =
let (qs, xs, ls) = unzip3 xss in
MkTyContext {
dctx, dnames,
qnames, dctx, dnames,
termLen = extendLen xss termLen,
tctx = tctx . ls,
tnames = tnames . xs,
@ -149,63 +169,78 @@ namespace TyContext
}
export %inline
extendTyN : CtxExtension d n1 n2 -> TyContext d n1 -> TyContext d n2
extendTyN : CtxExtension q d n1 n2 -> TyContext q d n1 -> TyContext q d n2
extendTyN = extendTyLetN . map (\(q, x, s) => (q, x, lamVar s))
export %inline
extendTyLetN0 : CtxExtensionLet0 d n1 n2 -> TyContext d n1 -> TyContext d n2
extendTyLetN0 xss = extendTyLetN (map (Zero,) xss)
extendTyLetN0 : CtxExtensionLet0 q d n1 n2 ->
TyContext q d n1 -> TyContext q d n2
extendTyLetN0 xss ctx =
let Val q = ctx.qtyLen in
extendTyLetN (map (\(x, t) => (zero x.loc, x, t)) xss) ctx
export %inline
extendTyN0 : CtxExtension0 d n1 n2 -> TyContext d n1 -> TyContext d n2
extendTyN0 xss = extendTyN (map (Zero,) xss)
extendTyN0 : CtxExtension0 q d n1 n2 ->
TyContext q d n1 -> TyContext q d n2
extendTyN0 xss ctx =
let Val q = ctx.qtyLen in
extendTyN (map (\(x, t) => (zero x.loc, x, t)) xss) ctx
export %inline
extendTyLet : Qty -> BindName -> Term d n -> Term d n ->
TyContext d n -> TyContext d (S n)
extendTyLet : Qty q -> BindName -> Term q d n -> Term q d n ->
TyContext q d n -> TyContext q d (S n)
extendTyLet q x s e = extendTyLetN [< (q, x, letVar s e)]
export %inline
extendTy : Qty -> BindName -> Term d n -> TyContext d n -> TyContext d (S n)
extendTy : Qty q -> BindName -> Term q d n ->
TyContext q d n -> TyContext q d (S n)
extendTy q x s = extendTyN [< (q, x, s)]
export %inline
extendTy0 : BindName -> Term d n -> TyContext d n -> TyContext d (S n)
extendTy0 = extendTy Zero
extendTy0 : BindName -> Term q d n ->
TyContext q d n -> TyContext q d (S n)
extendTy0 x t ctx = let Val q = ctx.qtyLen in extendTy (zero x.loc) x t ctx
export %inline
extendDim : BindName -> TyContext d n -> TyContext (S d) n
extendDim x (MkTyContext {dimLen, dctx, dnames, tctx, tnames, qtys}) =
extendDim : BindName -> TyContext q d n -> TyContext q (S d) n
extendDim x (MkTyContext {dimLen, dctx, dnames, qnames, tctx, tnames, qtys}) =
MkTyContext {
dctx = dctx :<? Nothing,
dnames = dnames :< x,
dimLen = [|S dimLen|],
tctx = map weakD tctx,
tnames, qtys
qnames, tnames, qtys
}
export %inline
eqDim : Dim d -> Dim d -> TyContext d n -> TyContext d n
eqDim p q = {dctx $= set p q, dimLen $= id, termLen $= id}
eqDim : Dim d -> Dim d -> TyContext q d n -> TyContext q d n
eqDim p q = {dctx $= set p q}
export
toWhnfContext : TyContext d n -> WhnfContext d n
toWhnfContext (MkTyContext {dnames, tnames, tctx, _}) =
MkWhnfContext {dnames, tnames, tctx}
toWhnfContext : TyContext q d n -> WhnfContext q d n
toWhnfContext (MkTyContext {qnames, dnames, tnames, tctx, _}) =
MkWhnfContext {qnames, dnames, tnames, tctx}
public export
(.names) : TyContext q d n -> NameContexts q d n
(MkTyContext {qnames, dnames, tnames, _}).names =
MkNameContexts {qnames, dnames, tnames}
namespace QOutput
export %inline
(+) : QOutput n -> QOutput n -> QOutput n
(+) : QOutput q n -> QOutput q n -> QOutput q n
(+) = zipWith (+)
export %inline
(*) : Qty -> QOutput n -> QOutput n
(*) : Qty q -> QOutput q n -> QOutput q n
(*) pi = map (pi *)
export %inline
zeroFor : TyContext _ n -> QOutput n
zeroFor ctx = zeroFor ctx.tctx
zeroFor : TyContext q _ n -> QOutput q n
zeroFor ctx =
let Val q = ctx.qtyLen in
zeroFor ctx.tctx @{LocateVarType}
export
@ -214,8 +249,10 @@ makeDAssign (Shift SZ) = [<]
makeDAssign (K e _ ::: th) = makeDAssign th :< e
export
makeEqContext' : {d : Nat} -> TyContext d n -> DSubst d 0 -> EqContext n
makeEqContext' : {d : Nat} -> TyContext q d n -> DSubst d 0 -> EqContext q n
makeEqContext' ctx th = MkEqContext {
qtyLen = ctx.qtyLen,
qnames = ctx.qnames,
termLen = ctx.termLen,
dassign = makeDAssign th,
dnames = ctx.dnames,
@ -225,134 +262,160 @@ makeEqContext' ctx th = MkEqContext {
}
export
makeEqContext : TyContext d n -> DSubst d 0 -> EqContext n
makeEqContext : TyContext q d n -> DSubst d 0 -> EqContext q n
makeEqContext ctx@(MkTyContext {dnames, _}) th =
let Val d = lengthPrf0 dnames in makeEqContext' ctx th
namespace EqContext
public export %inline
empty : EqContext 0
empty : EqContext 0 0
empty = MkEqContext {
dassign = [<], dnames = [<], tctx = [<], tnames = [<], qtys = [<]
qnames = [<], dassign = [<], dnames = [<],
tctx = [<], tnames = [<], qtys = [<]
}
public export %inline
null : EqContext n -> Bool
null ctx = null ctx.dnames && null ctx.tnames
null : EqContext q n -> Bool
null ctx = null ctx.qnames && null ctx.dnames && null ctx.tnames
export %inline
extendTyLetN : CtxExtensionLet 0 n1 n2 -> EqContext n1 -> EqContext n2
extendTyLetN xss (MkEqContext {termLen, dassign, dnames, tctx, tnames, qtys}) =
extendTyLetN : CtxExtensionLet q 0 n1 n2 -> EqContext q n1 -> EqContext q n2
extendTyLetN xss
(MkEqContext {termLen, qnames, dassign, dnames, tctx, tnames, qtys}) =
let (qs, xs, ls) = unzip3 xss in
MkEqContext {
termLen = extendLen xss termLen,
tctx = tctx . ls,
tnames = tnames . xs,
qtys = qtys . qs,
dassign, dnames
dassign, dnames, qnames
}
export %inline
extendTyN : CtxExtension 0 n1 n2 -> EqContext n1 -> EqContext n2
extendTyN : CtxExtension q 0 n1 n2 -> EqContext q n1 -> EqContext q n2
extendTyN = extendTyLetN . map (\(q, x, s) => (q, x, lamVar s))
export %inline
extendTyLetN0 : CtxExtensionLet0 0 n1 n2 -> EqContext n1 -> EqContext n2
extendTyLetN0 xss = extendTyLetN (map (Zero,) xss)
extendTyLetN0 : CtxExtensionLet0 q 0 n1 n2 -> EqContext q n1 -> EqContext q n2
extendTyLetN0 xss ctx =
let Val q = ctx.qtyLen in
extendTyLetN (map (\(x, t) => (zero x.loc, x, t)) xss) ctx
export %inline
extendTyN0 : CtxExtension0 0 n1 n2 -> EqContext n1 -> EqContext n2
extendTyN0 xss = extendTyN (map (Zero,) xss)
extendTyN0 : CtxExtension0 q 0 n1 n2 -> EqContext q n1 -> EqContext q n2
extendTyN0 xss ctx =
let Val q = ctx.qtyLen in
extendTyN (map (\(x, t) => (zero x.loc, x, t)) xss) ctx
export %inline
extendTyLet : Qty -> BindName -> Term 0 n -> Term 0 n ->
EqContext n -> EqContext (S n)
extendTyLet : Qty q -> BindName -> Term q 0 n -> Term q 0 n ->
EqContext q n -> EqContext q (S n)
extendTyLet q x s e = extendTyLetN [< (q, x, letVar s e)]
export %inline
extendTy : Qty -> BindName -> Term 0 n -> EqContext n -> EqContext (S n)
extendTy : Qty q -> BindName -> Term q 0 n ->
EqContext q n -> EqContext q (S n)
extendTy q x s = extendTyN [< (q, x, s)]
export %inline
extendTy0 : BindName -> Term 0 n -> EqContext n -> EqContext (S n)
extendTy0 = extendTy Zero
extendTy0 : BindName -> Term q 0 n -> EqContext q n -> EqContext q (S n)
extendTy0 x t ctx = let Val q = ctx.qtyLen in extendTy (zero x.loc) x t ctx
export %inline
extendDim : BindName -> DimConst -> EqContext n -> EqContext n
extendDim x e (MkEqContext {dassign, dnames, tctx, tnames, qtys}) =
extendDim : BindName -> DimConst -> EqContext q n -> EqContext q n
extendDim x e (MkEqContext {dassign, dnames, qnames, tctx, tnames, qtys}) =
MkEqContext {dassign = dassign :< e, dnames = dnames :< x,
tctx, tnames, qtys}
qnames, tctx, tnames, qtys}
export
toTyContext : (e : EqContext n) -> TyContext e.dimLen n
toTyContext (MkEqContext {dimLen, dassign, dnames, tctx, tnames, qtys}) =
toTyContext : (e : EqContext q n) -> TyContext q e.dimLen n
toTyContext
(MkEqContext {dimLen, dassign, dnames, qnames, tctx, tnames, qtys}) =
MkTyContext {
dctx = fromGround dnames dassign,
tctx = map (subD $ shift0 dimLen) tctx,
dnames, tnames, qtys
dnames, qnames, tnames, qtys
}
export
toWhnfContext : (ectx : EqContext n) -> WhnfContext 0 n
toWhnfContext (MkEqContext {tnames, tctx, _}) =
MkWhnfContext {dnames = [<], tnames, tctx}
toWhnfContext : (ectx : EqContext q n) -> WhnfContext q 0 n
toWhnfContext (MkEqContext {qnames, tnames, tctx, _}) =
MkWhnfContext {dnames = [<], qnames, tnames, tctx}
export
injElim : WhnfContext d n -> Elim 0 0 -> Elim d n
injElim : WhnfContext q d n -> Elim q 0 0 -> Elim q d n
injElim ctx e =
let Val d = ctx.dimLen; Val n = ctx.termLen in
e // shift0 d // shift0 n
public export
(.names) : (e : EqContext q n) -> NameContexts q e.dimLen n
(MkEqContext {qnames, dnames, tnames, _}).names =
MkNameContexts {qnames, dnames, tnames}
public export
(.names0) : EqContext q n -> NameContexts q 0 n
(MkEqContext {qnames, tnames, _}).names0 =
MkNameContexts {qnames, dnames = [<], tnames}
namespace WhnfContext
public export %inline
empty : WhnfContext 0 0
empty = MkWhnfContext [<] [<] [<]
empty : WhnfContext 0 0 0
empty = MkWhnfContext [<] [<] [<] [<]
export
extendTy' : BindName -> LocalVar d n -> WhnfContext d n -> WhnfContext d (S n)
extendTy' x var (MkWhnfContext {termLen, dnames, tnames, tctx}) =
extendTy' : BindName -> LocalVar q d n ->
WhnfContext q d n -> WhnfContext q d (S n)
extendTy' x var (MkWhnfContext {termLen, qnames, dnames, tnames, tctx}) =
MkWhnfContext {
dnames,
dnames, qnames,
termLen = [|S termLen|],
tnames = tnames :< x,
tctx = tctx :< var
}
export %inline
extendTy : BindName -> Term d n -> WhnfContext d n -> WhnfContext d (S n)
extendTy : BindName -> Term q d n ->
WhnfContext q d n -> WhnfContext q d (S n)
extendTy x ty ctx = extendTy' x (lamVar ty) ctx
export %inline
extendTyLet : BindName -> (type, term : Term d n) ->
WhnfContext d n -> WhnfContext d (S n)
extendTyLet : BindName -> (type, term : Term q d n) ->
WhnfContext q d n -> WhnfContext q d (S n)
extendTyLet x type term ctx = extendTy' x (letVar {type, term}) ctx
export
extendDimN : {s : Nat} -> BContext s -> WhnfContext d n ->
WhnfContext (s + d) n
extendDimN ns (MkWhnfContext {dnames, tnames, tctx, dimLen}) =
extendDimN : {s : Nat} -> BContext s -> WhnfContext q d n ->
WhnfContext q (s + d) n
extendDimN ns (MkWhnfContext {qnames, dnames, tnames, tctx, dimLen}) =
MkWhnfContext {
dimLen = [|Val s + dimLen|],
dnames = dnames ++ toSnocVect' ns,
tctx = map (subD $ shift s) tctx,
tnames
qnames, tnames
}
export
extendDim : BindName -> WhnfContext d n -> WhnfContext (S d) n
extendDim : BindName -> WhnfContext q d n -> WhnfContext q (S d) n
extendDim i = extendDimN [< i]
public export
(.names) : WhnfContext q d n -> NameContexts q d n
(MkWhnfContext {qnames, dnames, tnames, _}).names =
MkNameContexts {qnames, dnames, tnames}
private
prettyTContextElt : {opts : _} ->
BContext d -> BContext n ->
Doc opts -> BindName -> LocalVar d n ->
NameContexts q d n ->
Doc opts -> BindName -> LocalVar q d n ->
Eff Pretty (Doc opts)
prettyTContextElt dnames tnames q x s = do
prettyTContextElt names q x s = do
let Val _ = lengthPrf0 names.qnames
dot <- dotD
x <- prettyTBind x; colon <- colonD
ty <- withPrec Outer $ prettyTerm dnames tnames s.type; eq <- cstD
tm <- traverse (withPrec Outer . prettyTerm dnames tnames) s.term
ty <- withPrec Outer $ prettyTerm names s.type; eq <- cstD
tm <- traverse (withPrec Outer . prettyTerm names) s.term
d <- askAt INDENT
let qx = hcat [q, dot, x]
pure $ case tm of
@ -364,39 +427,37 @@ prettyTContextElt dnames tnames q x s = do
private
prettyTContext' : {opts : _} ->
BContext d -> Context' (Doc opts) n -> BContext n ->
TContext d n -> Eff Pretty (SnocList (Doc opts))
prettyTContext' _ [<] [<] [<] = pure [<]
prettyTContext' dnames (qtys :< q) (tnames :< x) (tys :< t) =
[|prettyTContext' dnames qtys tnames tys :<
prettyTContextElt dnames tnames q x t|]
NameContexts q d n -> Context' (Doc opts) n ->
TContext q d n -> Eff Pretty (SnocList (Doc opts))
prettyTContext' _ [<] [<] = pure [<]
prettyTContext' names (qtys :< q) (tys :< t) =
let names' = {tnames $= tail, termLen $= map pred} names in
[|prettyTContext' names' qtys tys :<
prettyTContextElt names' q (head names.tnames) t|]
export
prettyTContext : {opts : _} ->
BContext d -> QContext n -> BContext n ->
TContext d n -> Eff Pretty (Doc opts)
prettyTContext dnames qtys tnames tys = do
comma <- commaD
qtys <- traverse prettyQty qtys
sepSingle . exceptLast (<+> comma) . toList <$>
prettyTContext' dnames qtys tnames tys
NameContexts q d n -> QContext q n ->
TContext q d n -> Eff Pretty (Doc opts)
prettyTContext names qtys tys = do
qtys <- traverse (prettyQty names.qnames) qtys
sepSingleTight !commaD . toList <$> prettyTContext' names qtys tys
export
prettyTyContext : {opts : _} -> TyContext d n -> Eff Pretty (Doc opts)
prettyTyContext (MkTyContext dctx dnames tctx tnames qtys) =
case dctx of
C [<] => prettyTContext dnames qtys tnames tctx
prettyTyContext : {opts : _} -> TyContext q d n -> Eff Pretty (Doc opts)
prettyTyContext ctx = case ctx.dctx of
C [<] => prettyTContext ctx.names ctx.qtys ctx.tctx
_ => pure $
sepSingle [!(prettyDimEq dnames dctx) <++> !pipeD,
!(prettyTContext dnames qtys tnames tctx)]
sepSingle [!(prettyDimEq ctx.dnames ctx.dctx) <++> !pipeD,
!(prettyTContext ctx.names ctx.qtys ctx.tctx)]
export
prettyEqContext : {opts : _} -> EqContext n -> Eff Pretty (Doc opts)
prettyEqContext : {opts : _} -> EqContext q n -> Eff Pretty (Doc opts)
prettyEqContext ctx = prettyTyContext $ toTyContext ctx
export
prettyWhnfContext : {opts : _} -> WhnfContext d n -> Eff Pretty (Doc opts)
prettyWhnfContext : {opts : _} -> WhnfContext q d n -> Eff Pretty (Doc opts)
prettyWhnfContext ctx =
let Val n = ctx.termLen in
sepSingle . exceptLast (<+> comma) . toList <$>
prettyTContext' ctx.dnames (replicate n "_") ctx.tnames ctx.tctx
sepSingleTight !commaD . toList <$>
prettyTContext' ctx.names (replicate n "_") ctx.tctx

237
lib/Quox/Typing/Error.idr
View file

@ -17,108 +17,64 @@ import Derive.Prelude
%default total
public export
record NameContexts d n where
constructor MkNameContexts
dnames : BContext d
tnames : BContext n
%runElab deriveIndexed "NameContexts" [Show]
namespace NameContexts
export
empty : NameContexts 0 0
empty = MkNameContexts [<] [<]
export
extendDimN : BContext s -> NameContexts d n -> NameContexts (s + d) n
extendDimN xs = {dnames $= (++ toSnocVect' xs)}
export
extendDim : BindName -> NameContexts d n -> NameContexts (S d) n
extendDim i = extendDimN [< i]
namespace TyContext
public export
(.names) : TyContext d n -> NameContexts d n
(MkTyContext {dnames, tnames, _}).names =
MkNameContexts {dnames, tnames}
namespace EqContext
public export
(.names) : (e : EqContext n) -> NameContexts e.dimLen n
(MkEqContext {dnames, tnames, _}).names =
MkNameContexts {dnames, tnames}
public export
(.names0) : EqContext n -> NameContexts 0 n
(MkEqContext {tnames, _}).names0 =
MkNameContexts {dnames = [<], tnames}
namespace WhnfContext
public export
(.names) : WhnfContext d n -> NameContexts d n
(MkWhnfContext {dnames, tnames, _}).names =
MkNameContexts {dnames, tnames}
public export
data Error
= ExpectedTYPE Loc (NameContexts d n) (Term d n)
| ExpectedPi Loc (NameContexts d n) (Term d n)
| ExpectedSig Loc (NameContexts d n) (Term d n)
| ExpectedEnum Loc (NameContexts d n) (Term d n)
| ExpectedEq Loc (NameContexts d n) (Term d n)
| ExpectedNAT Loc (NameContexts d n) (Term d n)
| ExpectedSTRING Loc (NameContexts d n) (Term d n)
| ExpectedBOX Loc (NameContexts d n) (Term d n)
| ExpectedIOState Loc (NameContexts d n) (Term d n)
= ExpectedTYPE Loc (NameContexts q d n) (Term q d n)
| ExpectedPi Loc (NameContexts q d n) (Term q d n)
| ExpectedSig Loc (NameContexts q d n) (Term q d n)
| ExpectedEnum Loc (NameContexts q d n) (Term q d n)
| ExpectedEq Loc (NameContexts q d n) (Term q d n)
| ExpectedNAT Loc (NameContexts q d n) (Term q d n)
| ExpectedSTRING Loc (NameContexts q d n) (Term q d n)
| ExpectedBOX Loc (NameContexts q d n) (Term q d n)
| ExpectedIOState Loc (NameContexts q d n) (Term q d n)
| BadUniverse Loc Universe Universe
| TagNotIn Loc TagVal (SortedSet TagVal)
| BadCaseEnum Loc (SortedSet TagVal) (SortedSet TagVal)
| BadQtys Loc String (TyContext d n) (List (QOutput n, Term d n))
| BadQtys Loc String (TyContext q d n) (List (QOutput q n, Term q d n))
-- first term arg of ClashT is the type
| ClashT Loc (EqContext n) EqMode (Term 0 n) (Term 0 n) (Term 0 n)
| ClashTy Loc (EqContext n) EqMode (Term 0 n) (Term 0 n)
| ClashE Loc (EqContext n) EqMode (Elim 0 n) (Elim 0 n)
| ClashT Loc (EqContext q n) EqMode (Term q 0 n) (Term q 0 n) (Term q 0 n)
| ClashTy Loc (EqContext q n) EqMode (Term q 0 n) (Term q 0 n)
| ClashE Loc (EqContext q n) EqMode (Elim q 0 n) (Elim q 0 n)
| ClashU Loc EqMode Universe Universe
| ClashQ Loc Qty Qty
| ClashQ Loc (BContext q) (Qty q) (Qty q)
| NotInScope Loc Name
| NotType Loc (TyContext d n) (Term d n)
| WrongType Loc (EqContext n) (Term 0 n) (Term 0 n)
| NotType Loc (TyContext q d n) (Term q d n)
| WrongType Loc (EqContext q n) (Term q 0 n) (Term q 0 n)
| WrongBuiltinType Builtin Error
| ExpectedSingleEnum Loc (NameContexts d n) (Term d n)
| ExpectedSingleEnum Loc (NameContexts q d n) (Term q d n)
| MissingEnumArm Loc TagVal (List TagVal)
-- extra context
| WhileChecking
(TyContext d n) SQty
(Term d n) -- term
(Term d n) -- type
(TyContext q d n) SQty
(Term q d n) -- term
(Term q d n) -- type
Error
| WhileCheckingTy
(TyContext d n)
(Term d n)
(TyContext q d n)
(Term q d n)
(Maybe Universe)
Error
| WhileInferring
(TyContext d n) SQty
(Elim d n)
(TyContext q d n) SQty
(Elim q d n)
Error
| WhileComparingT
(EqContext n) EqMode SQty
(Term 0 n) -- type
(Term 0 n) (Term 0 n) -- lhs/rhs
(EqContext q n) EqMode SQty
(Term q 0 n) -- type
(Term q 0 n) (Term q 0 n) -- lhs/rhs
Error
| WhileComparingE
(EqContext n) EqMode SQty
(Elim 0 n) (Elim 0 n)
(EqContext q n) EqMode SQty
(Elim q 0 n) (Elim q 0 n)
Error
%name Error err
%runElab derive "Error" [Show]
-- %runElab derive "Error" [Show]
public export
ErrorEff : Type -> Type
@ -144,7 +100,7 @@ Located Error where
(ClashTy loc _ _ _ _).loc = loc
(ClashE loc _ _ _ _).loc = loc
(ClashU loc _ _ _).loc = loc
(ClashQ loc _ _).loc = loc
(ClashQ loc _ _ _).loc = loc
(NotInScope loc _).loc = loc
(NotType loc _ _).loc = loc
(WrongType loc _ _ _).loc = loc
@ -192,14 +148,15 @@ expect : Has (Except e) fs =>
(a -> a -> e) -> (a -> a -> Bool) -> a -> a -> Eff fs ()
expect err cmp x y = unless (x `cmp` y) $ throw $ err x y
parameters {auto _ : Has ErrorEff fs} (loc : Loc)
parameters {auto _ : Has ErrorEff fs} (loc : Loc) (ctx : BContext q)
export %inline
expectEqualQ : Qty -> Qty -> Eff fs ()
expectEqualQ = expect (ClashQ loc) (==)
expectEqualQ : Qty q -> Qty q -> Eff fs ()
expectEqualQ = expect (ClashQ loc ctx) (==)
-- [fixme] probably replace (==)
export %inline
expectCompatQ : Qty -> Qty -> Eff fs ()
expectCompatQ = expect (ClashQ loc) compat
expectCompatQ : Qty q -> Qty q -> Eff fs ()
expectCompatQ = expect (ClashQ loc ctx) compat
export %inline
expectModeU : EqMode -> Universe -> Universe -> Eff fs ()
@ -225,8 +182,8 @@ isTypeInUniverse (Just k) = "is a type in universe \{show k}"
private
filterSameQtys : BContext n -> List (QOutput n, z) ->
Exists $ \n' => (BContext n', List (QOutput n', z))
filterSameQtys : BContext n -> List (QOutput q n, z) ->
Exists $ \n' => (BContext n', List (QOutput q n', z))
filterSameQtys [<] qts = Evidence 0 ([<], qts)
filterSameQtys (ns :< n) qts =
let (qs, qts) = unzip $ map (\(qs :< q, t) => (q, qs, t)) qts
@ -236,27 +193,29 @@ filterSameQtys (ns :< n) qts =
then Evidence l (ns, qts)
else Evidence (S l) (ns :< n, zipWith (\(qs, t), q => (qs :< q, t)) qts qs)
where
allSame : List Qty -> Bool
allSame : List (Qty q) -> Bool
allSame [] = True
allSame (q :: qs) = all (== q) qs
private
printCaseQtys : {opts : _} -> TyContext d n ->
BContext n' -> List (QOutput n', Term d n) ->
printCaseQtys : {opts : _} -> TyContext q d n ->
BContext n' -> List (QOutput q n', Term q d n) ->
Eff Pretty (List (Doc opts))
printCaseQtys ctx ns qts =
let Evidence _ (ns, qts) = filterSameQtys ns qts in
traverse (line ns) qts
where
line : BContext l -> (QOutput l, Term d n) -> Eff Pretty (Doc opts)
line ns (qs, t) = map (("-" <++>) . sep) $ sequence
line : BContext l -> (QOutput q l, Term q d n) -> Eff Pretty (Doc opts)
line ns (qs, t) =
let Val q = ctx.qtyLen; names = ctx.names in
map (("-" <++>) . sep) $ sequence
[hangDSingle "the term"
!(prettyTerm ctx.dnames ctx.tnames t),
!(prettyTerm names t),
hangDSingle "uses variables" $
separateTight !commaD $ toSnocList' !(traverse prettyTBind ns),
hangDSingle "with quantities" $
separateTight !commaD $ toSnocList' !(traverse prettyQty qs)]
separateTight !commaD $ toSnocList' !(traverse (prettyQty names) qs)]
parameters {opts : LayoutOpts} (showContext : Bool)
export
@ -268,11 +227,11 @@ parameters {opts : LayoutOpts} (showContext : Bool)
else pure doc
export %inline
inTContext : TyContext d n -> Doc opts -> Eff Pretty (Doc opts)
inTContext : TyContext q d n -> Doc opts -> Eff Pretty (Doc opts)
inTContext ctx = inContext' (null ctx) ctx prettyTyContext
export %inline
inEContext : EqContext n -> Doc opts -> Eff Pretty (Doc opts)
inEContext : EqContext q n -> Doc opts -> Eff Pretty (Doc opts)
inEContext ctx = inContext' (null ctx) ctx prettyEqContext
export
@ -280,43 +239,43 @@ parameters {opts : LayoutOpts} (showContext : Bool)
prettyErrorNoLoc err0 = case err0 of
ExpectedTYPE _ ctx s =>
hangDSingle "expected a type universe, but got"
!(prettyTerm ctx.dnames ctx.tnames s)
!(prettyTerm ctx s)
ExpectedPi _ ctx s =>
hangDSingle "expected a function type, but got"
!(prettyTerm ctx.dnames ctx.tnames s)
!(prettyTerm ctx s)
ExpectedSig _ ctx s =>
hangDSingle "expected a pair type, but got"
!(prettyTerm ctx.dnames ctx.tnames s)
!(prettyTerm ctx s)
ExpectedEnum _ ctx s =>
hangDSingle "expected an enumeration type, but got"
!(prettyTerm ctx.dnames ctx.tnames s)
!(prettyTerm ctx s)
ExpectedEq _ ctx s =>
hangDSingle "expected an equality type, but got"
!(prettyTerm ctx.dnames ctx.tnames s)
!(prettyTerm ctx s)
ExpectedNAT _ ctx s =>
hangDSingle
("expected the type" <++>
!(prettyTerm [<] [<] $ NAT noLoc) <+> ", but got")
!(prettyTerm ctx.dnames ctx.tnames s)
!(prettyTerm ctx $ NAT noLoc) <+> ", but got")
!(prettyTerm ctx s)
ExpectedSTRING _ ctx s =>
hangDSingle
("expected the type" <++>
!(prettyTerm [<] [<] $ STRING noLoc) <+> ", but got")
!(prettyTerm ctx.dnames ctx.tnames s)
!(prettyTerm ctx $ STRING noLoc) <+> ", but got")
!(prettyTerm ctx s)
ExpectedBOX _ ctx s =>
hangDSingle "expected a box type, but got"
!(prettyTerm ctx.dnames ctx.tnames s)
!(prettyTerm ctx s)
ExpectedIOState _ ctx s =>
hangDSingle "expected IOState, but got"
!(prettyTerm ctx.dnames ctx.tnames s)
!(prettyTerm ctx s)
BadUniverse _ k l => pure $
sep ["the universe level" <++> !(prettyUniverse k),
@ -324,57 +283,58 @@ parameters {opts : LayoutOpts} (showContext : Bool)
TagNotIn _ tag set =>
hangDSingle (hsep ["the tag", !(prettyTag tag), "is not contained in"])
!(prettyTerm [<] [<] $ Enum set noLoc)
!(prettyTerm empty $ Enum set noLoc)
BadCaseEnum _ head body => sep <$> sequence
[hangDSingle "case expression has head of type"
!(prettyTerm [<] [<] $ Enum head noLoc),
!(prettyTerm empty $ Enum head noLoc),
hangDSingle "but cases for"
!(prettyTerm [<] [<] $ Enum body noLoc)]
!(prettyTerm empty $ Enum body noLoc)]
BadQtys _ what ctx arms =>
hangDSingle (text "inconsistent variable usage in \{what}") $
sep !(printCaseQtys ctx ctx.tnames arms)
ClashT _ ctx mode ty s t =>
let names = ctx.names0 in
inEContext ctx . sep =<< sequence
[hangDSingle "the term" !(prettyTerm [<] ctx.tnames s),
hangDSingle (text "is not \{prettyMode mode}")
!(prettyTerm [<] ctx.tnames t),
hangDSingle "at type" !(prettyTerm [<] ctx.tnames ty)]
[hangDSingle "the term" !(prettyTerm names s),
hangDSingle (text "is not \{prettyMode mode}") !(prettyTerm names t),
hangDSingle "at type" !(prettyTerm names ty)]
ClashTy _ ctx mode a b =>
let names = ctx.names0 in
inEContext ctx . sep =<< sequence
[hangDSingle "the type" !(prettyTerm [<] ctx.tnames a),
hangDSingle (text "is not \{prettyMode mode}")
!(prettyTerm [<] ctx.tnames b)]
[hangDSingle "the type" !(prettyTerm names a),
hangDSingle (text "is not \{prettyMode mode}") !(prettyTerm names b)]
ClashE _ ctx mode e f =>
let names = ctx.names0 in
inEContext ctx . sep =<< sequence
[hangDSingle "the term" !(prettyElim [<] ctx.tnames e),
hangDSingle (text "is not \{prettyMode mode}")
!(prettyElim [<] ctx.tnames f)]
[hangDSingle "the term" !(prettyElim names e),
hangDSingle (text "is not \{prettyMode mode}") !(prettyElim names f)]
ClashU _ mode k l => pure $
sep ["the universe level" <++> !(prettyUniverse k),
text "is not \{prettyModeU mode}" <++> !(prettyUniverse l)]
ClashQ _ pi rh => pure $
sep ["the quantity" <++> !(prettyQty pi),
"is not equal to" <++> !(prettyQty rh)]
ClashQ _ ctx pi rh => pure $
sep ["the quantity" <++> !(prettyQty ctx pi),
"is not equal to" <++> !(prettyQty ctx rh)]
NotInScope _ x => pure $
hsep [!(prettyFree x), "is not in scope"]
NotType _ ctx s =>
inTContext ctx . sep =<< sequence
[hangDSingle "the term" !(prettyTerm ctx.dnames ctx.tnames s),
[hangDSingle "the term" !(prettyTerm ctx.names s),
pure "is not a type"]
WrongType _ ctx ty s =>
let names = ctx.names0 in
inEContext ctx . sep =<< sequence
[hangDSingle "the term" !(prettyTerm [<] ctx.tnames s),
hangDSingle "cannot have type" !(prettyTerm [<] ctx.tnames ty)]
[hangDSingle "the term" !(prettyTerm names s),
hangDSingle "cannot have type" !(prettyTerm names ty)]
WrongBuiltinType b err => pure $
vappend
@ -384,24 +344,25 @@ parameters {opts : LayoutOpts} (showContext : Bool)
ExpectedSingleEnum _ ctx s =>
hangDSingle "expected an enumeration type with one case, but got"
!(prettyTerm ctx.dnames ctx.tnames s)
!(prettyTerm ctx s)
MissingEnumArm _ tag tags => pure $
sep [hsep ["the tag", !(prettyTag tag), "is not contained in"],
!(prettyTerm [<] [<] $ Enum (fromList tags) noLoc)]
!(prettyTerm empty $ Enum (fromList tags) noLoc)]
WhileChecking ctx sg s a err =>
let names = ctx.names in
[|vappendBlank
(inTContext ctx . sep =<< sequence
[hangDSingle "while checking" !(prettyTerm ctx.dnames ctx.tnames s),
hangDSingle "has type" !(prettyTerm ctx.dnames ctx.tnames a),
hangDSingle "with quantity" !(prettyQty sg.qty)])
[hangDSingle "while checking" !(prettyTerm names s),
hangDSingle "has type" !(prettyTerm names a),
hangDSingle "with quantity" !(prettyQConst sg.qconst)])
(prettyErrorNoLoc err)|]
WhileCheckingTy ctx a k err =>
[|vappendBlank
(inTContext ctx . sep =<< sequence
[hangDSingle "while checking" !(prettyTerm ctx.dnames ctx.tnames a),
[hangDSingle "while checking" !(prettyTerm ctx.names a),
pure $ text $ isTypeInUniverse k])
(prettyErrorNoLoc err)|]
@ -409,27 +370,27 @@ parameters {opts : LayoutOpts} (showContext : Bool)
[|vappendBlank
(inTContext ctx . sep =<< sequence
[hangDSingle "while inferring the type of"
!(prettyElim ctx.dnames ctx.tnames e),
hangDSingle "with quantity" !(prettyQty sg.qty)])
!(prettyElim ctx.names e),
hangDSingle "with quantity" !(prettyQConst sg.qconst)])
(prettyErrorNoLoc err)|]
WhileComparingT ctx mode sg a s t err =>
let names = ctx.names0 in
[|vappendBlank
(inEContext ctx . sep =<< sequence
[hangDSingle "while checking that" !(prettyTerm [<] ctx.tnames s),
hangDSingle (text "is \{prettyMode mode}")
!(prettyTerm [<] ctx.tnames t),
hangDSingle "at type" !(prettyTerm [<] ctx.tnames a),
hangDSingle "with quantity" !(prettyQty sg.qty)])
[hangDSingle "while checking that" !(prettyTerm names s),
hangDSingle (text "is \{prettyMode mode}") !(prettyTerm names t),
hangDSingle "at type" !(prettyTerm names a),
hangDSingle "with quantity" !(prettyQConst sg.qconst)])
(prettyErrorNoLoc err)|]
WhileComparingE ctx mode sg e f err =>
let names = ctx.names0 in
[|vappendBlank
(inEContext ctx . sep =<< sequence
[hangDSingle "while checking that" !(prettyElim [<] ctx.tnames e),
hangDSingle (text "is \{prettyMode mode}")
!(prettyElim [<] ctx.tnames f),
hangDSingle "with quantity" !(prettyQty sg.qty)])
[hangDSingle "while checking that" !(prettyElim names e),
hangDSingle (text "is \{prettyMode mode}") !(prettyElim names f),
hangDSingle "with quantity" !(prettyQConst sg.qconst)])
(prettyErrorNoLoc err)|]
where

51
lib/Quox/Untyped/Syntax.idr
View file

@ -255,49 +255,66 @@ USubst : Nat -> Nat -> Type
USubst = Subst Term
public export FromVar Term where fromVarLoc = B
public export %inline
FromVarR Term where fromVarR = B
public export %inline
FromVar Term where fromVar = B; fromVarSame _ _ = Refl
public export
CanSubstSelf Term where
s // th = case s of
export
CanSubstSelf Term
substTerm : Term from -> Lazy (USubst from to) -> Term to
substTerm s th = case s of
F x loc =>
F x loc
B i loc =>
getLoc th i loc
get th i loc
Lam x body loc =>
Lam x (assert_total $ body // push x.loc th) loc
Lam x (assert_total substTerm body $ push x.loc th) loc
App fun arg loc =>
App (fun // th) (arg // th) loc
App (substTerm fun th) (substTerm arg th) loc
Pair fst snd loc =>
Pair (fst // th) (snd // th) loc
Pair (substTerm fst th) (substTerm snd th) loc
Fst pair loc =>
Fst (pair // th) loc
Fst (substTerm pair th) loc
Snd pair loc =>
Snd (pair // th) loc
Snd (substTerm pair th) loc
Tag tag loc =>
Tag tag loc
CaseEnum tag cases loc =>
CaseEnum (tag // th) (map (assert_total mapSnd (// th)) cases) loc
CaseEnum (substTerm tag th)
(map (mapSnd (\b => assert_total substTerm b th)) cases) loc
Absurd loc =>
Absurd loc
Nat n loc =>
Nat n loc
Succ nat loc =>
Succ (nat // th) loc
Succ (substTerm nat th) loc
CaseNat nat zer suc loc =>
CaseNat (nat // th) (zer // th) (assert_total substSuc suc th) loc
CaseNat (substTerm nat th)
(substTerm zer th)
(assert_total substSuc suc th) loc
Str s loc =>
Str s loc
Let u x rhs body loc =>
Let u x (rhs // th) (assert_total $ body // push x.loc th) loc
Let u x (substTerm rhs th)
(assert_total substTerm body $ push x.loc th) loc
Erased loc =>
Erased loc
where
substSuc : forall from, to.
CaseNatSuc from -> USubst from to -> CaseNatSuc to
substSuc (NSRec x ih t) th = NSRec x ih $ t // pushN 2 x.loc th
substSuc (NSNonrec x t) th = NSNonrec x $ t // push x.loc th
CaseNatSuc from -> Lazy (USubst from to) -> CaseNatSuc to
substSuc (NSRec x ih t) th = NSRec x ih $ substTerm t $ pushN 2 x.loc th
substSuc (NSNonrec x t) th = NSNonrec x $ substTerm t $ push x.loc th
export
CanSubstSelfR Term where (//?) = substTerm
export
CanSubstSelf Term where (//) = substTerm; substSame _ _ = Refl
public export
subN : SnocVect s (Term n) -> Term (s + n) -> Term n

26
lib/Quox/Var.idr
View file

@ -138,21 +138,25 @@ export
weakIsSpec p i = toNatInj $ trans (weakCorrect p i) (sym $ weakSpecCorrect p i)
||| inject a variable (with a source location) into some kind of term. in this
||| case, the scope size may be needed at run time
public export
interface FromVar f where %inline fromVarLoc : Var n -> Loc -> f n
interface FromVarR f where
%inline fromVarR : {n : Nat} -> Var n -> Loc -> f n
||| inject a variable (with a source location) into some kind of term, without
||| needing the scope size
public export
interface FromVarR f => FromVar f where
%inline fromVar : Var n -> Loc -> f n
0 fromVarSame : (i : Var n) -> (l : Loc) -> fromVarR i l === fromVar i l
public export FromVar Var where fromVarLoc x _ = x
public export
FromVarR Var where fromVarR x _ = x
export
tabulateV : {0 tm : Nat -> Type} -> (forall n. Var n -> tm n) ->
(n : Nat) -> Vect n (tm n)
tabulateV f 0 = []
tabulateV f (S n) = f VZ :: tabulateV (f . VS) n
export
allVars : (n : Nat) -> Vect n (Var n)
allVars n = tabulateV id n
public export
FromVar Var where fromVar x _ = x; fromVarSame _ _ = Refl
public export

189
lib/Quox/Whnf/Coercion.idr
View file

@ -9,140 +9,147 @@ import Quox.Whnf.TypeCase
private
coeScoped : {s : Nat} -> DScopeTerm d n -> Dim d -> Dim d -> Loc ->
ScopeTermN s d n -> ScopeTermN s d n
coeScoped ty p q loc (S names (N body)) =
S names $ N $ E $ Coe ty p q body loc
coeScoped ty p q loc (S names (Y body)) =
ST names $ E $ Coe (weakDS s ty) p q body loc
coeScoped : {s, q : Nat} -> DScopeTerm q d n -> Dim d -> Dim d -> Loc ->
ScopeTermN s q d n -> ScopeTermN s q d n
coeScoped ty p p' loc (S names (N body)) =
S names $ N $ E $ Coe ty p p' body loc
coeScoped ty p p' loc (S names (Y body)) =
ST names $ E $ Coe (weakDS s ty) p p' body loc
where
weakDS : (by : Nat) -> DScopeTerm d n -> DScopeTerm d (by + n)
weakDS : (by : Nat) -> DScopeTerm q d n -> DScopeTerm q d (by + n)
weakDS by (S names (Y body)) = S names $ Y $ weakT by body
weakDS by (S names (N body)) = S names $ N $ weakT by body
parameters {auto _ : CanWhnf Term Interface.isRedexT}
{auto _ : CanWhnf Elim Interface.isRedexE}
(defs : Definitions) (ctx : WhnfContext d n) (sg : SQty)
||| reduce a function application `App (Coe ty p q val) s loc`
(defs : Definitions) (ctx : WhnfContext q d n) (sg : SQty)
||| reduce a function application `App (Coe ty p p' val) s loc`
export covering
piCoe : (ty : DScopeTerm d n) -> (p, q : Dim d) ->
(val, s : Term d n) -> Loc ->
Eff Whnf (Subset (Elim d n) (No . isRedexE defs ctx sg))
piCoe sty@(S [< i] ty) p q val s loc = do
-- (coe [i ⇒ π.(x : A) → B] @p @q t) s ⇝
-- coe [i ⇒ B[𝒔‹i›/x] @p @q ((t ∷ (π.(x : A) → B)‹p/i›) 𝒔‹p›)
-- where 𝒔‹j› ≔ coe [i ⇒ A] @q @j s
piCoe : (ty : DScopeTerm q d n) -> (p, p' : Dim d) ->
(val, s : Term q d n) -> Loc ->
Eff Whnf (Subset (Elim q d n) (No . isRedexE defs ctx sg))
piCoe sty@(S [< i] ty) p p' val s loc = do
-- (coe [i ⇒ π.(x : A) → B] @p @p' t) s ⇝
-- coe [i ⇒ B[𝒔‹i›/x] @p @p' ((t ∷ (π.(x : A) → B)‹p/i›) 𝒔‹p›)
-- where 𝒔‹j› ≔ coe [i ⇒ A] @p' @j s
--
-- type-case is used to expose A,B if the type is neutral
let ctx1 = extendDim i ctx
Element ty tynf <- whnf defs ctx1 SZero $ getTerm ty
(arg, res) <- tycasePi defs ctx1 ty
let s0 = CoeT i arg q p s s.loc
let Val q = ctx.qtyLen
s0 = CoeT i arg p' p s s.loc
body = E $ App (Ann val (ty // one p) val.loc) (E s0) loc
s1 = CoeT i (arg // (BV 0 i.loc ::: shift 2)) (weakD 1 q) (BV 0 i.loc)
s1 = CoeT i (arg // (BV 0 i.loc ::: shift 2))
(weakD 1 p') (BV 0 i.loc)
(s // shift 1) s.loc
whnf defs ctx sg $ CoeT i (sub1 res s1) p q body loc
whnf defs ctx sg $ CoeT i (sub1 res s1) p p' body loc
||| reduce a pair elimination `CasePair pi (Coe ty p q val) ret body loc`
||| reduce a pair elimination `CasePair pi (Coe ty p p' val) ret body loc`
export covering
sigCoe : (qty : Qty) ->
(ty : DScopeTerm d n) -> (p, q : Dim d) -> (val : Term d n) ->
(ret : ScopeTerm d n) -> (body : ScopeTermN 2 d n) -> Loc ->
Eff Whnf (Subset (Elim d n) (No . isRedexE defs ctx sg))
sigCoe qty sty@(S [< i] ty) p q val ret body loc = do
-- caseπ (coe [i ⇒ (x : A) × B] @p @q s) return z ⇒ C of { (a, b) ⇒ e }
sigCoe : (qty : Qty q) ->
(ty : DScopeTerm q d n) -> (p, p' : Dim d) -> (val : Term q d n) ->
(ret : ScopeTerm q d n) -> (body : ScopeTermN 2 q d n) -> Loc ->
Eff Whnf (Subset (Elim q d n) (No . isRedexE defs ctx sg))
sigCoe qty sty@(S [< i] ty) p p' val ret body loc = do
-- caseπ (coe [i ⇒ (x : A) × B] @p @p' s) return z ⇒ C of { (a, b) ⇒ e }
-- ⇝
-- caseπ s ∷ ((x : A) × B)‹p/i› return z ⇒ C
-- of { (a, b) ⇒
-- e[(coe [i ⇒ A] @p @q a)/a,
-- (coe [i ⇒ B[(coe [j ⇒ A‹j/i›] @p @i a)/x]] @p @q b)/b] }
-- e[(coe [i ⇒ A] @p @p' a)/a,
-- (coe [i ⇒ B[(coe [j ⇒ A‹j/i›] @p @i a)/x]] @p @p' b)/b] }
--
-- type-case is used to expose A,B if the type is neutral
let ctx1 = extendDim i ctx
Element ty tynf <- whnf defs ctx1 SZero $ getTerm ty
(tfst, tsnd) <- tycaseSig defs ctx1 ty
let [< x, y] = body.names
a' = CoeT i (weakT 2 tfst) p q (BVT 1 x.loc) x.loc
let Val q = ctx.qtyLen
[< x, y] = body.names
a' = CoeT i (weakT 2 tfst) p p' (BVT 1 x.loc) x.loc
tsnd' = tsnd.term //
(CoeT i (weakT 2 $ tfst // (B VZ tsnd.loc ::: shift 2))
(weakD 1 p) (B VZ i.loc) (BVT 1 tsnd.loc) y.loc ::: shift 2)
b' = CoeT i tsnd' p q (BVT 0 y.loc) y.loc
b' = CoeT i tsnd' p p' (BVT 0 y.loc) y.loc
whnf defs ctx sg $ CasePair qty (Ann val (ty // one p) val.loc) ret
(ST body.names $ body.term // (a' ::: b' ::: shift 2)) loc
||| reduce a pair projection `Fst (Coe ty p q val) loc`
||| reduce a pair projection `Fst (Coe ty p p' val) loc`
export covering
fstCoe : (ty : DScopeTerm d n) -> (p, q : Dim d) -> (val : Term d n) ->
Loc -> Eff Whnf (Subset (Elim d n) (No . isRedexE defs ctx sg))
fstCoe sty@(S [< i] ty) p q val loc = do
-- fst (coe (𝑖 ⇒ (x : A) × B) @p @q s)
fstCoe : (ty : DScopeTerm q d n) -> (p, p' : Dim d) -> (val : Term q d n) ->
Loc -> Eff Whnf (Subset (Elim q d n) (No . isRedexE defs ctx sg))
fstCoe sty@(S [< i] ty) p p' val loc = do
-- fst (coe (𝑖 ⇒ (x : A) × B) @p @p' s)
-- ⇝
-- coe (𝑖 ⇒ A) @p @q (fst (s ∷ (x : A‹p/𝑖›) × B‹p/𝑖›))
-- coe (𝑖 ⇒ A) @p @p' (fst (s ∷ (x : A‹p/𝑖›) × B‹p/𝑖›))
--
-- type-case is used to expose A,B if the type is neutral
let ctx1 = extendDim i ctx
Element ty tynf <- whnf defs ctx1 SZero $ getTerm ty
(tfst, _) <- tycaseSig defs ctx1 ty
let Val q = ctx.qtyLen
whnf defs ctx sg $
Coe (ST [< i] tfst) p q
Coe (ST [< i] tfst) p p'
(E (Fst (Ann val (ty // one p) val.loc) val.loc)) loc
||| reduce a pair projection `Snd (Coe ty p q val) loc`
export covering
sndCoe : (ty : DScopeTerm d n) -> (p, q : Dim d) -> (val : Term d n) ->
Loc -> Eff Whnf (Subset (Elim d n) (No . isRedexE defs ctx sg))
sndCoe sty@(S [< i] ty) p q val loc = do
-- snd (coe (𝑖 ⇒ (x : A) × B) @p @q s)
sndCoe : (ty : DScopeTerm q d n) -> (p, p' : Dim d) -> (val : Term q d n) ->
Loc -> Eff Whnf (Subset (Elim q d n) (No . isRedexE defs ctx sg))
sndCoe sty@(S [< i] ty) p p' val loc = do
-- snd (coe (𝑖 ⇒ (x : A) × B) @p @p' s)
-- ⇝
-- coe (𝑖 ⇒ B[coe (𝑗 ⇒ A‹𝑗/𝑖›) @p @𝑖 (fst (s ∷ (x : A) × B))/x]) @p @q
-- coe (𝑖 ⇒ B[coe (𝑗 ⇒ A‹𝑗/𝑖›) @p @𝑖 (fst (s ∷ (x : A) × B))/x]) @p @p'
-- (snd (s ∷ (x : A‹p/𝑖›) × B‹p/𝑖›))
--
-- type-case is used to expose A,B if the type is neutral
let ctx1 = extendDim i ctx
Element ty tynf <- whnf defs ctx1 SZero $ getTerm ty
(tfst, tsnd) <- tycaseSig defs ctx1 ty
let Val q = ctx.qtyLen
whnf defs ctx sg $
Coe (ST [< i] $ sub1 tsnd $
Coe (ST [< !(fresh i)] $ tfst // (BV 0 i.loc ::: shift 2))
(weakD 1 p) (BV 0 loc)
(E (Fst (Ann (dweakT 1 val) ty val.loc) val.loc)) loc)
p q
p p'
(E (Snd (Ann val (ty // one p) val.loc) val.loc))
loc
||| reduce a dimension application `DApp (Coe ty p q val) r loc`
export covering
eqCoe : (ty : DScopeTerm d n) -> (p, q : Dim d) -> (val : Term d n) ->
eqCoe : (ty : DScopeTerm q d n) -> (p, p' : Dim d) -> (val : Term q d n) ->
(r : Dim d) -> Loc ->
Eff Whnf (Subset (Elim d n) (No . isRedexE defs ctx sg))
eqCoe sty@(S [< j] ty) p q val r loc = do
-- (coe [j ⇒ Eq [i ⇒ A] L R] @p @q eq) @r
Eff Whnf (Subset (Elim q d n) (No . isRedexE defs ctx sg))
eqCoe sty@(S [< j] ty) p p' val r loc = do
-- (coe [j ⇒ Eq [i ⇒ A] L R] @p @p' eq) @r
-- ⇝
-- comp [j ⇒ A‹r/i›] @p @q ((eq ∷ (Eq [i ⇒ A] L R)‹p/j›) @r)
-- comp [j ⇒ A‹r/i›] @p @p' ((eq ∷ (Eq [i ⇒ A] L R)‹p/j›) @r)
-- @r { 0 j ⇒ L; 1 j ⇒ R }
let ctx1 = extendDim j ctx
Element ty tynf <- whnf defs ctx1 SZero $ getTerm ty
(a0, a1, a, s, t) <- tycaseEq defs ctx1 ty
let a' = dsub1 a (weakD 1 r)
let Val q = ctx.qtyLen
a' = dsub1 a (weakD 1 r)
val' = E $ DApp (Ann val (ty // one p) val.loc) r loc
whnf defs ctx sg $ CompH j a' p q val' r j s j t loc
whnf defs ctx sg $ CompH j a' p p' val' r j s j t loc
||| reduce a pair elimination `CaseBox pi (Coe ty p q val) ret body`
export covering
boxCoe : (qty : Qty) ->
(ty : DScopeTerm d n) -> (p, q : Dim d) -> (val : Term d n) ->
(ret : ScopeTerm d n) -> (body : ScopeTerm d n) -> Loc ->
Eff Whnf (Subset (Elim d n) (No . isRedexE defs ctx sg))
boxCoe qty sty@(S [< i] ty) p q val ret body loc = do
-- caseπ (coe [i ⇒ [ρ. A]] @p @q s) return z ⇒ C of { [a] ⇒ e }
boxCoe : (qty : Qty q) ->
(ty : DScopeTerm q d n) -> (p, p' : Dim d) -> (val : Term q d n) ->
(ret : ScopeTerm q d n) -> (body : ScopeTerm q d n) -> Loc ->
Eff Whnf (Subset (Elim q d n) (No . isRedexE defs ctx sg))
boxCoe qty sty@(S [< i] ty) p p' val ret body loc = do
-- caseπ (coe [i ⇒ [ρ. A]] @p @p' s) return z ⇒ C of { [a] ⇒ e }
-- ⇝
-- caseπ s ∷ [ρ. A]‹p/i› return z ⇒ C of { [a] ⇒ e[(coe [i ⇒ A] p q a)/a] }
-- caseπ s ∷ [ρ. A]‹p/i› return z ⇒ C of { [a] ⇒ e[(coe [i ⇒ A] p p' a)/a] }
let ctx1 = extendDim i ctx
Val q = ctx.qtyLen
Element ty tynf <- whnf defs ctx1 SZero $ getTerm ty
ta <- tycaseBOX defs ctx1 ty
let xloc = body.name.loc
let a' = CoeT i (weakT 1 ta) p q (BVT 0 xloc) xloc
let a' = CoeT i (weakT 1 ta) p p' (BVT 0 xloc) xloc
whnf defs ctx sg $ CaseBox qty (Ann val (ty // one p) val.loc) ret
(ST body.names $ body.term // (a' ::: shift 1)) loc
@ -150,14 +157,14 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
-- new params block to call the above functions at different `n`
parameters {auto _ : CanWhnf Term Interface.isRedexT}
{auto _ : CanWhnf Elim Interface.isRedexE}
(defs : Definitions) (ctx : WhnfContext d n) (sg : SQty)
(defs : Definitions) (ctx : WhnfContext q d n) (sg : SQty)
||| pushes a coercion inside a whnf-ed term
export covering
pushCoe : BindName ->
(ty : Term (S d) n) -> (p, q : Dim d) -> (s : Term d n) -> Loc ->
(0 pc : So (canPushCoe sg ty s)) =>
Eff Whnf (NonRedex Elim d n defs ctx sg)
pushCoe i ty p q s loc =
(ty : Term q (S d) n) -> (p, p' : Dim d) -> (s : Term q d n) ->
Loc -> (0 pc : So (canPushCoe sg ty s)) =>
Eff Whnf (NonRedex Elim q d n defs ctx sg)
pushCoe i ty p p' s loc =
case ty of
-- (coe ★ᵢ @_ @_ s) ⇝ (s ∷ ★ᵢ)
TYPE l tyLoc =>
@ -169,40 +176,40 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
-- η expand, then simplify the Coe/App in the body
--
-- (coe (𝑖 ⇒ π.(x : A) → B) @p @q s)
-- (coe (𝑖 ⇒ π.(x : A) → B) @p @p' s)
-- ⇝
-- (λ y ⇒ (coe (𝑖 ⇒ π.(x : A) → B) @p @q s) y) ∷ (π.(x : A) → B)‹q/𝑖›
-- ⇝ ‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾
-- (λ y ⇒ ⋯) ∷ (π.(x : A) → B)‹q/𝑖› -- see `piCoe`
-- (λ y ⇒ (coe (𝑖 ⇒ π.(x : A) → B) @p @p' s) y) ∷ (π.(x : A) → B)‹p'/𝑖›
-- ⇝ ‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾
-- (λ y ⇒ ⋯) ∷ (π.(x : A) → B)‹p'/𝑖› -- see `piCoe`
--
-- do the piCoe step here because otherwise equality checking keeps
-- doing the η forever
Pi {arg, res = S [< x] _, _} => do
let ctx' = extendTy x (arg // one p) ctx
body <- piCoe defs ctx' sg
(weakDS 1 $ SY [< i] ty) p q (weakT 1 s) (BVT 0 loc) loc
(weakDS 1 $ SY [< i] ty) p p' (weakT 1 s) (BVT 0 loc) loc
whnf defs ctx sg $
Ann (LamY x (E body.fst) loc) (ty // one q) loc
Ann (LamY x (E body.fst) loc) (ty // one p') loc
-- no η!!!
-- push into a pair constructor, otherwise still stuck
--
-- s̃‹𝑘› ≔ coe (𝑗 ⇒ A‹𝑗/𝑖›) @p @𝑘 s
-- -----------------------------------------------
-- (coe (𝑖 ⇒ (x : A) × B) @p @q (s, t))
-- (coe (𝑖 ⇒ (x : A) × B) @p @p' (s, t))
-- ⇝
-- (s̃‹q›, coe (𝑖 ⇒ B[s̃‹𝑖›/x]) @p @q t)
-- ∷ ((x : A) × B)‹q/𝑖›
-- (s̃‹p'›, coe (𝑖 ⇒ B[s̃‹𝑖›/x]) @p @p' t)
-- ∷ ((x : A) × B)‹p'/𝑖›
Sig tfst tsnd tyLoc => do
let Pair fst snd sLoc = s
fst' = CoeT i tfst p q fst fst.loc
let Val q = ctx.qtyLen
Pair fst snd sLoc = s
fst' = CoeT i tfst p p' fst fst.loc
fstInSnd =
CoeT !(fresh i)
(tfst // (BV 0 loc ::: shift 2))
(weakD 1 p) (BV 0 loc) (dweakT 1 fst) fst.loc
snd' = CoeT i (sub1 tsnd fstInSnd) p q snd snd.loc
snd' = CoeT i (sub1 tsnd fstInSnd) p p' snd snd.loc
whnf defs ctx sg $
Ann (Pair (E fst') (E snd') sLoc) (ty // one q) loc
Ann (Pair (E fst') (E snd') sLoc) (ty // one p') loc
-- (coe {𝐚̄} @_ @_ s) ⇝ (s ∷ {𝐚̄})
Enum cases tyLoc =>
@ -210,21 +217,21 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
-- η expand/simplify, same as for Π
--
-- (coe (𝑖 ⇒ Eq (𝑗 ⇒ A) l r) @p @q s)
-- (coe (𝑖 ⇒ Eq (𝑗 ⇒ A) l r) @p @p' s)
-- ⇝
-- (δ 𝑘 ⇒ (coe (𝑖 ⇒ Eq (𝑗 ⇒ A) l r) @p @q s) @𝑘) ∷ (Eq (𝑗 ⇒ A) l r)‹q/𝑖›
-- ⇝ ‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾
-- (δ 𝑘 ⇒ ⋯) ∷ (Eq (𝑗 ⇒ A) l r)‹q/𝑖› -- see `eqCoe`
-- (δ 𝑘 ⇒ (coe (𝑖 ⇒ Eq (𝑗 ⇒ A) l r) @p @p' s) @𝑘) ∷ (Eq (𝑗 ⇒ A) l r)‹p'/𝑖›
-- ⇝ ‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾
-- (δ 𝑘 ⇒ ⋯) ∷ (Eq (𝑗 ⇒ A) l r)‹p'/𝑖› -- see `eqCoe`
--
-- do the eqCoe step here because otherwise equality checking keeps
-- doing the η forever
Eq {ty = S [< j] _, _} => do
let ctx' = extendDim j ctx
body <- eqCoe defs ctx' sg
(dweakDS 1 $ S [< i] $ Y ty) (weakD 1 p) (weakD 1 q)
(dweakDS 1 $ S [< i] $ Y ty) (weakD 1 p) (weakD 1 p')
(dweakT 1 s) (BV 0 loc) loc
whnf defs ctx sg $
Ann (DLamY i (E body.fst) loc) (ty // one q) loc
Ann (DLamY i (E body.fst) loc) (ty // one p') loc
-- (coe ℕ @_ @_ s) ⇝ (s ∷ ℕ)
NAT tyLoc =>
@ -236,17 +243,17 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
-- η expand/simplify
--
-- (coe (𝑖 ⇒ [π.A]) @p @q s)
-- (coe (𝑖 ⇒ [π.A]) @p @p' s)
-- ⇝
-- [case coe (𝑖 ⇒ [π.A]) @p @q s return A‹q/𝑖› of {[x] ⇒ x}]
-- [case coe (𝑖 ⇒ [π.A]) @p @p' s return A‹p'/𝑖› of {[x] ⇒ x}]
-- ⇝
-- [case1 s ∷ [π.A]‹p/𝑖› ⋯] ∷ [π.A]‹q/𝑖› -- see `boxCoe`
-- [case1 s ∷ [π.A]‹p/𝑖› ⋯] ∷ [π.A]‹p'/𝑖› -- see `boxCoe`
--
-- do the eqCoe step here because otherwise equality checking keeps
-- do the boxCoe step here because otherwise equality checking keeps
-- doing the η forever
BOX qty inner tyLoc => do
body <- boxCoe defs ctx sg qty
(SY [< i] ty) p q s
(SN $ inner // one q)
(SY [< i] ty) p p' s
(SN $ inner // one p')
(SY [< !(mnb "inner" loc)] (BVT 0 loc)) loc
whnf defs ctx sg $ Ann (Box (E body.fst) loc) (ty // one q) loc
whnf defs ctx sg $ Ann (Box (E body.fst) loc) (ty // one p') loc

64
lib/Quox/Whnf/ComputeElimType.idr
View file

@ -15,46 +15,44 @@ export covering
computeElimType :
CanWhnf Term Interface.isRedexT =>
CanWhnf Elim Interface.isRedexE =>
(defs : Definitions) -> (ctx : WhnfContext d n) -> (0 sg : SQty) ->
(e : Elim d n) -> (0 ne : No (isRedexE defs ctx sg e)) =>
Eff Whnf (Term d n)
(defs : Definitions) -> (ctx : WhnfContext q d n) -> (0 sg : SQty) ->
(e : Elim q d n) -> (0 ne : No (isRedexE defs ctx sg e)) =>
Eff Whnf (Term q d n)
||| computes a type and then reduces it to whnf
export covering
computeWhnfElimType0 :
CanWhnf Term Interface.isRedexT =>
CanWhnf Elim Interface.isRedexE =>
(defs : Definitions) -> (ctx : WhnfContext d n) -> (0 sg : SQty) ->
(e : Elim d n) -> (0 ne : No (isRedexE defs ctx sg e)) =>
Eff Whnf (Term d n)
(defs : Definitions) -> (ctx : WhnfContext q d n) -> (0 sg : SQty) ->
(e : Elim q d n) -> (0 ne : No (isRedexE defs ctx sg e)) =>
Eff Whnf (Term q d n)
private covering
computeElimTypeNoLog, computeWhnfElimType0NoLog :
CanWhnf Term Interface.isRedexT =>
CanWhnf Elim Interface.isRedexE =>
(defs : Definitions) -> WhnfContext d n -> (0 sg : SQty) ->
(e : Elim d n) -> (0 ne : No (isRedexE defs ctx sg e)) =>
Eff Whnf (Term d n)
(defs : Definitions) -> WhnfContext q d n -> (0 sg : SQty) ->
(e : Elim q d n) -> (0 ne : No (isRedexE defs ctx sg e)) =>
Eff Whnf (Term q d n)
computeElimTypeNoLog defs ctx sg e =
case e of
F x u loc => do
let Just def = lookup x defs
| Nothing => throw $ NotInScope loc x
pure $ def.typeWithAt ctx.dimLen ctx.termLen u
let polyTy = def.typeWithAt ctx.dimLen ctx.termLen u
Val q = ctx.qtyLen
pure $ polyTy.type // ?freeQSubst
B i _ =>
pure (ctx.tctx !! i).type
B i _ => pure (ctx.tctx !! i).type
App f s loc =>
case !(computeWhnfElimType0NoLog defs ctx sg f {ne = noOr1 ne}) of
Pi {arg, res, _} => pure $ sub1 res $ Ann s arg loc
ty => throw $ ExpectedPi loc ctx.names ty
CasePair {pair, ret, _} =>
pure $ sub1 ret pair
Fst pair loc =>
case !(computeWhnfElimType0NoLog defs ctx sg pair {ne = noOr1 ne}) of
Sig {fst, _} => pure fst
@ -65,46 +63,34 @@ computeElimTypeNoLog defs ctx sg e =
Sig {snd, _} => pure $ sub1 snd $ Fst pair loc
ty => throw $ ExpectedSig loc ctx.names ty
CaseEnum {tag, ret, _} =>
pure $ sub1 ret tag
CaseNat {nat, ret, _} =>
pure $ sub1 ret nat
CaseBox {box, ret, _} =>
pure $ sub1 ret box
CasePair {pair, ret, _} => pure $ sub1 ret pair
CaseEnum {tag, ret, _} => pure $ sub1 ret tag
CaseNat {nat, ret, _} => pure $ sub1 ret nat
CaseBox {box, ret, _} => pure $ sub1 ret box
DApp {fun = f, arg = p, loc} =>
case !(computeWhnfElimType0NoLog defs ctx sg f {ne = noOr1 ne}) of
Eq {ty, _} => pure $ dsub1 ty p
t => throw $ ExpectedEq loc ctx.names t
Ann {ty, _} =>
pure ty
Coe {ty, q, _} =>
pure $ dsub1 ty q
Comp {ty, _} =>
pure ty
TypeCase {ret, _} =>
pure ret
Ann {ty, _} => pure ty
Coe {ty, p', _} => pure $ dsub1 ty p'
Comp {ty, _} => pure ty
TypeCase {ret, _} => pure ret
computeElimType defs ctx sg e {ne} = do
let Val n = ctx.termLen
sayMany "whnf" e.loc
[90 :> "computeElimType",
95 :> hsep ["ctx =", runPretty $ prettyWhnfContext ctx],
90 :> hsep ["e =", runPretty $ prettyElim ctx.dnames ctx.tnames e]]
90 :> hsep ["e =", runPretty $ prettyElim ctx.names e]]
res <- computeElimTypeNoLog defs ctx sg e {ne}
say "whnf" 91 e.loc $
hsep ["computeElimType ⇝",
runPretty $ prettyTerm ctx.dnames ctx.tnames res]
hsep ["computeElimType ⇝", runPretty $ prettyTerm ctx.names res]
pure res
computeWhnfElimType0 defs ctx sg e =
computeElimType defs ctx sg e >>= whnf0 defs ctx SZero
whnf0 defs ctx SZero !(computeElimType defs ctx sg e)
computeWhnfElimType0NoLog defs ctx sg e {ne} =
computeElimTypeNoLog defs ctx sg e {ne} >>= whnf0 defs ctx SZero
whnf0 defs ctx SZero !(computeElimTypeNoLog defs ctx sg e {ne})

36
lib/Quox/Whnf/Interface.idr
View file

@ -20,14 +20,15 @@ Whnf = [Except Error, NameGen, Log]
public export
0 RedexTest : TermLike -> Type
RedexTest tm =
{0 d, n : Nat} -> Definitions -> WhnfContext d n -> SQty -> tm d n -> Bool
{0 q, d, n : Nat} ->
Definitions -> WhnfContext q d n -> SQty -> tm q d n -> Bool
public export
interface CanWhnf (0 tm : TermLike) (0 isRedex : RedexTest tm) | tm
where
whnf, whnfNoLog :
(defs : Definitions) -> (ctx : WhnfContext d n) -> (q : SQty) ->
tm d n -> Eff Whnf (Subset (tm d n) (No . isRedex defs ctx q))
(defs : Definitions) -> (ctx : WhnfContext q d n) -> (sg : SQty) ->
tm q d n -> Eff Whnf (Subset (tm q d n) (No . isRedex defs ctx sg))
-- having isRedex be part of the class header, and needing to be explicitly
-- quantified on every use since idris can't infer its type, is a little ugly.
-- but none of the alternatives i've thought of so far work. e.g. in some
@ -36,26 +37,27 @@ where
public export %inline
whnf0, whnfNoLog0 :
{0 isRedex : RedexTest tm} -> CanWhnf tm isRedex =>
Definitions -> WhnfContext d n -> SQty -> tm d n -> Eff Whnf (tm d n)
Definitions -> WhnfContext q d n -> SQty -> tm q d n -> Eff Whnf (tm q d n)
whnf0 defs ctx q t = fst <$> whnf defs ctx q t
whnfNoLog0 defs ctx q t = fst <$> whnfNoLog defs ctx q t
public export
0 IsRedex, NotRedex : {isRedex : RedexTest tm} -> CanWhnf tm isRedex =>
Definitions -> WhnfContext d n -> SQty -> Pred (tm d n)
Definitions -> WhnfContext q d n -> SQty ->
Pred (tm q d n)
IsRedex defs ctx q = So . isRedex defs ctx q
NotRedex defs ctx q = No . isRedex defs ctx q
public export
0 NonRedex : (tm : TermLike) -> {isRedex : RedexTest tm} ->
CanWhnf tm isRedex => (d, n : Nat) ->
Definitions -> WhnfContext d n -> SQty -> Type
NonRedex tm d n defs ctx q = Subset (tm d n) (NotRedex defs ctx q)
CanWhnf tm isRedex => (q, d, n : Nat) ->
Definitions -> WhnfContext q d n -> SQty -> Type
NonRedex tm q d n defs ctx sg = Subset (tm q d n) (NotRedex defs ctx sg)
public export %inline
nred : {0 isRedex : RedexTest tm} -> (0 _ : CanWhnf tm isRedex) =>
(t : tm d n) -> (0 nr : NotRedex defs ctx q t) =>
NonRedex tm d n defs ctx q
(t : tm q d n) -> (0 nr : NotRedex defs ctx sg t) =>
NonRedex tm q d n defs ctx sg
nred t = Element t nr
@ -97,7 +99,7 @@ isNatHead _ = False
||| a natural constant, with or without an annotation
public export %inline
isNatConst : Term d n -> Bool
isNatConst : Term {} -> Bool
isNatConst (Nat {}) = True
isNatConst (E (Ann (Nat {}) _ _)) = True
isNatConst _ = False
@ -145,6 +147,7 @@ isTyCon (Let {}) = False
isTyCon (E {}) = False
isTyCon (CloT {}) = False
isTyCon (DCloT {}) = False
isTyCon (QCloT {}) = False
||| a syntactic type, or a neutral
public export %inline
@ -195,6 +198,7 @@ canPushCoe sg (Let {}) _ = False
canPushCoe sg (E {}) _ = False
canPushCoe sg (CloT {}) _ = False
canPushCoe sg (DCloT {}) _ = False
canPushCoe sg (QCloT {}) _ = False
mutual
@ -238,15 +242,16 @@ mutual
isRedexE defs ctx sg (Ann {tm, ty, _}) =
isE tm || isRedexT defs ctx sg tm || isRedexT defs ctx SZero ty
isRedexE defs ctx sg (Coe {ty = S _ (N _), _}) = True
isRedexE defs ctx sg (Coe {ty = S [< i] (Y ty), p, q, val, _}) =
isRedexE defs ctx sg (Coe {ty = S [< i] (Y ty), p, p', val, _}) =
isRedexT defs (extendDim i ctx) SZero ty ||
canPushCoe sg ty val || isYes (p `decEqv` q)
isRedexE defs ctx sg (Comp {ty, p, q, r, _}) =
isYes (p `decEqv` q) || isK r
canPushCoe sg ty val || isYes (p `decEqv` p')
isRedexE defs ctx sg (Comp {ty, p, p', r, _}) =
isYes (p `decEqv` p') || isK r
isRedexE defs ctx sg (TypeCase {ty, ret, _}) =
isRedexE defs ctx sg ty || isRedexT defs ctx sg ret || isAnnTyCon ty
isRedexE _ _ _ (CloE {}) = True
isRedexE _ _ _ (DCloE {}) = True
isRedexE _ _ _ (QCloE {}) = True
||| a reducible term
|||
@ -260,6 +265,7 @@ mutual
isRedexT : RedexTest Term
isRedexT _ _ _ (CloT {}) = True
isRedexT _ _ _ (DCloT {}) = True
isRedexT _ _ _ (QCloT {}) = True
isRedexT _ _ _ (Let {}) = True
isRedexT defs ctx sg (E {e, _}) = isAnn e || isRedexE defs ctx sg e
isRedexT _ _ _ (Succ p {}) = isNatConst p

82
lib/Quox/Whnf/Main.idr
View file

@ -19,19 +19,19 @@ export covering CanWhnf Elim Interface.isRedexE
private %inline
whnfDefault :
{0 isRedex : RedexTest tm} ->
(CanWhnf tm isRedex, Located2 tm) =>
(CanWhnf tm isRedex, Located3 tm) =>
String ->
(forall d, n. WhnfContext d n -> tm d n -> Eff Pretty LogDoc) ->
(forall d, n. WhnfContext q d n -> tm q d n -> Eff Pretty LogDoc) ->
(defs : Definitions) ->
(ctx : WhnfContext d n) ->
(ctx : WhnfContext q d n) ->
(sg : SQty) ->
(s : tm d n) ->
Eff Whnf (Subset (tm d n) (No . isRedex defs ctx sg))
(s : tm q d n) ->
Eff Whnf (Subset (tm q d n) (No . isRedex defs ctx sg))
whnfDefault name ppr defs ctx sg s = do
sayMany "whnf" s.loc
[10 :> "whnf",
95 :> hsep ["ctx =", runPretty $ prettyWhnfContext ctx],
95 :> hsep ["sg =", runPretty $ prettyQty sg.qty],
95 :> hsep ["sg =", runPretty $ prettyQConst sg.qconst],
10 :> hsep [text name, "=", runPretty $ ppr ctx s]]
res <- whnfNoLog defs ctx sg s
say "whnf" 11 s.loc $ hsep ["whnf ⇝", runPretty $ ppr ctx res.fst]
@ -39,10 +39,10 @@ whnfDefault name ppr defs ctx sg s = do
covering
CanWhnf Elim Interface.isRedexE where
whnf = whnfDefault "e" $ \ctx, e => prettyElim ctx.dnames ctx.tnames e
whnf = whnfDefault "e" $ \ctx, e => prettyElim ctx.names e
whnfNoLog defs ctx sg (F x u loc) with (lookupElim0 x u defs) proof eq
_ | Just y = whnf defs ctx sg $ setLoc loc $ injElim ctx y
_ | Just y = whnf defs ctx sg $ setLoc loc $ ?whnfFreeQSubst
_ | Nothing = pure $ Element (F x u loc) $ rewrite eq in Ah
whnfNoLog defs ctx sg (B i loc) with (ctx.tctx !! i) proof eq1
@ -186,8 +186,8 @@ CanWhnf Elim Interface.isRedexE where
whnf defs ctx sg $
Ann (endsOr (setLoc appLoc l) (setLoc appLoc r) (dsub1 body p) p)
(dsub1 ty p) appLoc
Coe ty p' q' val _ =>
eqCoe defs ctx sg ty p' q' val p appLoc
Coe ty r r' val _ =>
eqCoe defs ctx sg ty r r' val p appLoc
Right ndlh => case p of
K e _ => do
Eq {l, r, ty, _} <- computeWhnfElimType0 defs ctx sg f
@ -206,36 +206,37 @@ CanWhnf Elim Interface.isRedexE where
Element a anf <- whnf defs ctx SZero a
pure $ Element (Ann s a annLoc) (ne `orNo` snf `orNo` anf)
whnfNoLog defs ctx sg (Coe sty p q val coeLoc) =
whnfNoLog defs ctx sg (Coe sty p p' val coeLoc) = do
-- 𝑖 ∉ fv(A)
-- -------------------------------
-- coe (𝑖 ⇒ A) @p @q s ⇝ s ∷ A
-- coe (𝑖 ⇒ A) @p @p' s ⇝ s ∷ A
--
-- [fixme] needs a real equality check between A‹0/𝑖› and A‹1/𝑖›
case dsqueeze sty {f = Term} of
let Val q = ctx.qtyLen
case dsqueeze sty {f = Term q} of
([< i], Left ty) =>
case p `decEqv` q of
case p `decEqv` p' of
-- coe (𝑖 ⇒ A) @p @p s ⇝ (s ∷ A‹p/𝑖›)
Yes _ => whnf defs ctx sg $ Ann val (dsub1 sty p) coeLoc
No npq => do
Element ty tynf <- whnf defs (extendDim i ctx) SZero ty
case nchoose $ canPushCoe sg ty val of
Left pc => pushCoe defs ctx sg i ty p q val coeLoc
Right npc => pure $ Element (Coe (SY [< i] ty) p q val coeLoc)
Left pc => pushCoe defs ctx sg i ty p p' val coeLoc
Right npc => pure $ Element (Coe (SY [< i] ty) p p' val coeLoc)
(tynf `orNo` npc `orNo` notYesNo npq)
(_, Right ty) =>
whnf defs ctx sg $ Ann val ty coeLoc
whnfNoLog defs ctx sg (Comp ty p q val r zero one compLoc) =
case p `decEqv` q of
whnfNoLog defs ctx sg (Comp ty p p' val r zero one compLoc) =
case p `decEqv` p' of
-- comp [A] @p @p s @r { ⋯ } ⇝ s ∷ A
Yes y => whnf defs ctx sg $ Ann val ty compLoc
No npq => case r of
-- comp [A] @p @q s @0 { 0 𝑗 ⇒ t₀; ⋯ } ⇝ t₀‹q/𝑗› ∷ A
K Zero _ => whnf defs ctx sg $ Ann (dsub1 zero q) ty compLoc
-- comp [A] @p @q s @1 { 1 𝑗 ⇒ t₁; ⋯ } ⇝ t₁‹q/𝑗› ∷ A
K One _ => whnf defs ctx sg $ Ann (dsub1 one q) ty compLoc
B {} => pure $ Element (Comp ty p q val r zero one compLoc)
-- comp [A] @p @p' s @0 { 0 𝑗 ⇒ t₀; ⋯ } ⇝ t₀‹p'/𝑗› ∷ A
K Zero _ => whnf defs ctx sg $ Ann (dsub1 zero p') ty compLoc
-- comp [A] @p @p' s @1 { 1 𝑗 ⇒ t₁; ⋯ } ⇝ t₁‹p'/𝑗› ∷ A
K One _ => whnf defs ctx sg $ Ann (dsub1 one p') ty compLoc
B {} => pure $ Element (Comp ty p p' val r zero one compLoc)
(notYesNo npq `orNo` Ah)
whnfNoLog defs ctx sg (TypeCase ty ret arms def tcLoc) =
@ -248,17 +249,23 @@ CanWhnf Elim Interface.isRedexE where
reduceTypeCase defs ctx ty u ret arms def tcLoc
Right nt => pure $ Element (TypeCase ty ret arms def tcLoc)
(tynf `orNo` retnf `orNo` nt)
No _ =>
throw $ ClashQ tcLoc sg.qty Zero
No _ => do
let Val q = ctx.qtyLen
throw $ ClashQ tcLoc ctx.qnames (toQty tcLoc sg) (zero tcLoc)
whnfNoLog defs ctx sg (CloE (Sub el th)) =
whnfNoLog defs ctx sg $ pushSubstsWith' id th el
whnfNoLog defs ctx sg (DCloE (Sub el th)) =
whnfNoLog defs ctx sg $ pushSubstsWith' th id el
whnfNoLog defs ctx sg (CloE (Sub el th)) = do
let Val q = ctx.qtyLen
whnfNoLog defs ctx sg $ pushSubstsWith' id id th el
whnfNoLog defs ctx sg (DCloE (Sub el th)) = do
let Val q = ctx.qtyLen
whnfNoLog defs ctx sg $ pushSubstsWith' id th id el
whnfNoLog defs ctx sg (QCloE (SubR el th)) = do
let Val q = ctx.qtyLen
whnfNoLog defs ctx sg $ pushSubstsWith' th id id el
covering
CanWhnf Term Interface.isRedexT where
whnf = whnfDefault "e" $ \ctx, s => prettyTerm ctx.dnames ctx.tnames s
whnf = whnfDefault "e" $ \ctx, s => prettyTerm ctx.names s
whnfNoLog _ _ _ t@(TYPE {}) = pure $ nred t
whnfNoLog _ _ _ t@(IOState {}) = pure $ nred t
@ -294,7 +301,14 @@ CanWhnf Term Interface.isRedexT where
Left _ => let Ann {tm, _} = e in pure $ Element tm $ noOr1 $ noOr2 enf
Right na => pure $ Element (E e) $ na `orNo` enf
whnfNoLog defs ctx sg (CloT (Sub tm th)) =
whnfNoLog defs ctx sg $ pushSubstsWith' id th tm
whnfNoLog defs ctx sg (DCloT (Sub tm th)) =
whnfNoLog defs ctx sg $ pushSubstsWith' th id tm
whnfNoLog defs ctx sg (CloT (Sub tm th)) = do
let Val q = ctx.qtyLen
whnfNoLog defs ctx sg $ pushSubstsWith' id id th tm
whnfNoLog defs ctx sg (DCloT (Sub tm th)) = do
let Val q = ctx.qtyLen
whnfNoLog defs ctx sg $ pushSubstsWith' id th id tm
whnfNoLog defs ctx sg (QCloT (SubR tm th)) = do
let Val q = ctx.qtyLen
whnfNoLog defs ctx sg $ pushSubstsWith' th id id tm

64
lib/Quox/Whnf/TypeCase.idr
View file

@ -8,42 +8,43 @@ import Data.SnocVect
private
tycaseRhs : (k : TyConKind) -> TypeCaseArms d n ->
Maybe (ScopeTermN (arity k) d n)
tycaseRhs : (k : TyConKind) -> TypeCaseArms q d n ->
Maybe (ScopeTermN (arity k) q d n)
tycaseRhs k arms = lookupPrecise k arms
private
tycaseRhsDef : Term d n -> (k : TyConKind) -> TypeCaseArms d n ->
ScopeTermN (arity k) d n
tycaseRhsDef : (def : Term q d n) -> (k : TyConKind) -> TypeCaseArms q d n ->
ScopeTermN (arity k) q d n
tycaseRhsDef def k arms = fromMaybe (SN def) $ tycaseRhs k arms
private
tycaseRhs0 : (k : TyConKind) -> TypeCaseArms d n ->
(0 eq : arity k = 0) => Maybe (Term d n)
tycaseRhs0 : (k : TyConKind) -> TypeCaseArms q d n ->
(0 eq : arity k = 0) => Maybe (Term q d n)
tycaseRhs0 k arms = map (.term0) $ rewrite sym eq in tycaseRhs k arms
private
tycaseRhsDef0 : Term d n -> (k : TyConKind) -> TypeCaseArms d n ->
(0 eq : arity k = 0) => Term d n
tycaseRhsDef0 : (def : Term q d n) -> (k : TyConKind) -> TypeCaseArms q d n ->
(0 eq : arity k = 0) => Term q d n
tycaseRhsDef0 def k arms = fromMaybe def $ tycaseRhs0 k arms
parameters {auto _ : CanWhnf Term Interface.isRedexT}
{auto _ : CanWhnf Elim Interface.isRedexE}
(defs : Definitions) (ctx : WhnfContext d n)
(defs : Definitions) (ctx : WhnfContext q d n)
||| for π.(x : A) → B, returns (A, B);
||| for an elim returns a pair of type-cases that will reduce to that;
||| for other intro forms error
export covering
tycasePi : (t : Term d n) -> (0 tnf : No (isRedexT defs ctx SZero t)) =>
Eff Whnf (Term d n, ScopeTerm d n)
tycasePi : (t : Term q d n) -> (0 tnf : No (isRedexT defs ctx SZero t)) =>
Eff Whnf (Term q d n, ScopeTerm q d n)
tycasePi (Pi {arg, res, _}) = pure (arg, res)
tycasePi (E e) {tnf} = do
ty <- computeElimType defs ctx SZero e {ne = noOr2 tnf}
let loc = e.loc
let Val q = ctx.qtyLen
loc = e.loc
narg = mnb "Arg" loc; nret = mnb "Ret" loc
arg = E $ typeCase1Y e ty KPi [< !narg, !nret] (BVT 1 loc) loc
res' = typeCase1Y e (Arr Zero arg ty loc) KPi [< !narg, !nret]
res' = typeCase1Y e (Arr (zero loc) arg ty loc) KPi [< !narg, !nret]
(BVT 0 loc) loc
res = ST [< !narg] $ E $ App (weakE 1 res') (BVT 0 loc) loc
pure (arg, res)
@ -53,15 +54,16 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
||| for an elim returns a pair of type-cases that will reduce to that;
||| for other intro forms error
export covering
tycaseSig : (t : Term d n) -> (0 tnf : No (isRedexT defs ctx SZero t)) =>
Eff Whnf (Term d n, ScopeTerm d n)
tycaseSig : (t : Term q d n) -> (0 tnf : No (isRedexT defs ctx SZero t)) =>
Eff Whnf (Term q d n, ScopeTerm q d n)
tycaseSig (Sig {fst, snd, _}) = pure (fst, snd)
tycaseSig (E e) {tnf} = do
ty <- computeElimType defs ctx SZero e {ne = noOr2 tnf}
let loc = e.loc
let Val q = ctx.qtyLen
loc = e.loc
nfst = mnb "Fst" loc; nsnd = mnb "Snd" loc
fst = E $ typeCase1Y e ty KSig [< !nfst, !nsnd] (BVT 1 loc) loc
snd' = typeCase1Y e (Arr Zero fst ty loc) KSig [< !nfst, !nsnd]
snd' = typeCase1Y e (Arr (zero loc) fst ty loc) KSig [< !nfst, !nsnd]
(BVT 0 loc) loc
snd = ST [< !nfst] $ E $ App (weakE 1 snd') (BVT 0 loc) loc
pure (fst, snd)
@ -71,8 +73,8 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
||| for an elim returns a type-case that will reduce to that;
||| for other intro forms error
export covering
tycaseBOX : (t : Term d n) -> (0 tnf : No (isRedexT defs ctx SZero t)) =>
Eff Whnf (Term d n)
tycaseBOX : (t : Term q d n) -> (0 tnf : No (isRedexT defs ctx SZero t)) =>
Eff Whnf (Term q d n)
tycaseBOX (BOX {ty, _}) = pure ty
tycaseBOX (E e) {tnf} = do
ty <- computeElimType defs ctx SZero e {ne = noOr2 tnf}
@ -83,12 +85,14 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
||| for an elim returns five type-cases that will reduce to that;
||| for other intro forms error
export covering
tycaseEq : (t : Term d n) -> (0 tnf : No (isRedexT defs ctx SZero t)) =>
Eff Whnf (Term d n, Term d n, DScopeTerm d n, Term d n, Term d n)
tycaseEq : (t : Term q d n) -> (0 tnf : No (isRedexT defs ctx SZero t)) =>
Eff Whnf (Term q d n, Term q d n, DScopeTerm q d n,
Term q d n, Term q d n)
tycaseEq (Eq {ty, l, r, _}) = pure (ty.zero, ty.one, ty, l, r)
tycaseEq (E e) {tnf} = do
ty <- computeElimType defs ctx SZero e {ne = noOr2 tnf}
let loc = e.loc
let Val q = ctx.qtyLen
loc = e.loc
names = traverse' (\x => mnb x loc) [< "A0", "A1", "A", "L", "R"]
a0 = E $ typeCase1Y e ty KEq !names (BVT 4 loc) loc
a1 = E $ typeCase1Y e ty KEq !names (BVT 3 loc) loc
@ -104,10 +108,10 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
||| `reduceTypeCase A i Q arms def _` reduces an expression
||| `type-case A ∷ ★ᵢ return Q of { arms; _ ⇒ def }`
export covering
reduceTypeCase : (ty : Term d n) -> (u : Universe) -> (ret : Term d n) ->
(arms : TypeCaseArms d n) -> (def : Term d n) ->
reduceTypeCase : (ty : Term q d n) -> (u : Universe) -> (ret : Term q d n) ->
(arms : TypeCaseArms q d n) -> (def : Term q d n) ->
(0 _ : So (isTyCon ty)) => Loc ->
Eff Whnf (Subset (Elim d n) (No . isRedexE defs ctx SZero))
Eff Whnf (Subset (Elim q d n) (No . isRedexE defs ctx SZero))
reduceTypeCase ty u ret arms def loc = case ty of
-- (type-case ★ᵢ ∷ _ return Q of { ★ ⇒ s; ⋯ }) ⇝ s ∷ Q
TYPE {} =>
@ -120,9 +124,10 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
-- (type-case π.(x : A) → B ∷ ★ᵢ return Q of { (a → b) ⇒ s; ⋯ }) ⇝
-- s[(A ∷ ★ᵢ)/a, ((λ x ⇒ B) ∷ 0.A → ★ᵢ)/b] ∷ Q
Pi {arg, res, loc = piLoc, _} =>
let arg' = Ann arg (TYPE u arg.loc) arg.loc
let Val q = ctx.qtyLen
arg' = Ann arg (TYPE u arg.loc) arg.loc
res' = Ann (Lam res res.loc)
(Arr Zero arg (TYPE u arg.loc) arg.loc) res.loc
(Arr (zero loc) arg (TYPE u arg.loc) arg.loc) res.loc
in
whnf defs ctx SZero $
Ann (subN (tycaseRhsDef def KPi arms) [< arg', res']) ret loc
@ -130,9 +135,10 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
-- (type-case (x : A) × B ∷ ★ᵢ return Q of { (a × b) ⇒ s; ⋯ }) ⇝
-- s[(A ∷ ★ᵢ)/a, ((λ x ⇒ B) ∷ 0.A → ★ᵢ)/b] ∷ Q
Sig {fst, snd, loc = sigLoc, _} =>
let fst' = Ann fst (TYPE u fst.loc) fst.loc
let Val q = ctx.qtyLen
fst' = Ann fst (TYPE u fst.loc) fst.loc
snd' = Ann (Lam snd snd.loc)
(Arr Zero fst (TYPE u fst.loc) fst.loc) snd.loc
(Arr (zero loc) fst (TYPE u fst.loc) fst.loc) snd.loc
in
whnf defs ctx SZero $
Ann (subN (tycaseRhsDef def KSig arms) [< fst', snd']) ret loc

2
lib/quox-lib.ipkg
View file

@ -21,6 +21,8 @@ modules =
Quox.No,
Quox.Log,
Quox.Loc,
Quox.Semiring,
Quox.Polynomial,
Quox.Var,
Quox.Scoped,
Quox.OPE,

37
tests/Tests/FreeVars.idr
View file

@ -26,6 +26,15 @@ ToInfo Failure where
("expected", show f.expected),
("got", show f.got)]
private
testFreeVars1 : {d : Nat} -> HasFreeVars f =>
(f d -> String) -> f d -> FreeVars' d -> Test
testFreeVars1 lbl tm dims =
test (lbl tm) $ do
let dims = FV dims; dims' = fv tm
unless (dims == dims') $ Left $ Fail Dim dims dims'
Right ()
private
testFreeVars : {d, n : Nat} -> (HasFreeVars (f d), HasFreeDVars f) =>
(f d n -> String) -> f d n -> FreeVars' d -> FreeVars' n -> Test
@ -45,6 +54,22 @@ private
prettyWith : (a -> Eff Pretty Doc80) -> a -> String
prettyWith f = trim . render _ . runPretty . f
parameters {d : Nat} (ds : BContext d)
private
withContext1 : Doc80 -> Eff Pretty Doc80
withContext1 doc =
if null ds then pure $ hsep ["⊢", doc]
else pure $ sep [hsep [!(ctx1 ds), "⊢"], doc]
where
ctx1 : forall k. BContext k -> Eff Pretty Doc80
ctx1 [<] = pure "·"
ctx1 ctx = fillSeparateTight !commaD . toList' <$>
traverse' (pure . prettyBind') ctx
private
testFreeVarsD : Dim d -> FreeVars' d -> Test
testFreeVarsD = testFreeVars1 $ prettyWith $ withContext1 <=< prettyDim ds
parameters {d, n : Nat} (ds : BContext d) (ts : BContext n)
private
withContext : Doc80 -> Eff Pretty Doc80
@ -67,7 +92,13 @@ parameters {d, n : Nat} (ds : BContext d) (ts : BContext n)
export
tests : Test
tests = "free variables" :- [
tests = "free variables (fv/fdv)" :- [
testFreeVarsD [<] (^K Zero) [<],
testFreeVarsD [<"i", "j"] (^K Zero) [<False, False],
testFreeVarsD [<"i", "j"] (^BV 0) [<False, True],
testFreeVarsD [<"i", "j"] (^BV 1) [<True, False],
testFreeVarsD [<"i", "j", "k", "l"] (^BV 2) [<False, True, False, False],
testFreeVarsT [<] [<] (^TYPE 0) [<] [<],
testFreeVarsT [<"i", "j"] [<] (^TYPE 0) [<False, False] [<],
testFreeVarsT [<] [<"x", "y"] (^TYPE 0) [<] [<False, False],
@ -98,6 +129,10 @@ tests = "free variables" :- [
testFreeVarsT [<"i","j"] [<] (^DLamY "k" (E $ ^DApp (^F "eq" 0) (^BV 0)))
[<False,False] [<],
testFreeVarsT [<"i","j"] [<] (^DLamY "k" (E $ ^DApp (^F "eq" 0) (^BV 2)))
[<True,False] [<],
testFreeVarsT [<"i","j"] [<] (^DLamY "i" (E $ ^DApp (^F "eq" 0) (^BV 0)))
[<False,False] [<],
testFreeVarsT [<"i","j"] [<] (^DLamN (E $ ^DApp (^F "eq" 0) (^BV 0)))
[<False,True] [<],

8
tests/Tests/Qty.idr Normal file
View file

@ -0,0 +1,8 @@
module Tests.Qty
import TAP
import Quox.Syntax.Qty
import PrettyExtra