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

typechecker stuff

Browse source
This commit is contained in:
rhiannon morris 2022-04-24 00:21:30 +02:00
parent b433957eec
commit 5ea7880e38
17 changed files with 1021 additions and 750 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Quox.idr
View file

@ -5,7 +5,7 @@ import public Quox.Syntax
import public Quox.Equal import public Quox.Equal
import public Quox.Error import public Quox.Error
import public Quox.Pretty import public Quox.Pretty
-- import public Quox.Typechecker import public Quox.Typechecker
import Data.Nat import Data.Nat
import Data.Vect import Data.Vect

17
src/Quox/Context.idr
View file

@ -2,7 +2,7 @@ module Quox.Context
import Quox.Syntax.Shift import Quox.Syntax.Shift
import Quox.Pretty import Quox.Pretty
import Quox.NatExtra import public Quox.NatExtra
import Data.DPair import Data.DPair
import Data.Nat import Data.Nat
@ -36,6 +36,10 @@ Context' : (a : Type) -> (len : Nat) -> Type
Context' a = Context (\_ => a) Context' a = Context (\_ => a)
public export
tail : Context tm (S n) -> Context tm n
tail (tel :< _) = tel
export export
toSnocList : Telescope tm _ _ -> SnocList (Exists tm) toSnocList : Telescope tm _ _ -> SnocList (Exists tm)
toSnocList [<] = [<] toSnocList [<] = [<]
@ -158,6 +162,17 @@ teleLte' [<] = LTERefl
teleLte' (tel :< _) = LTESuccR (teleLte' tel) teleLte' (tel :< _) = LTESuccR (teleLte' tel)
export
tabulate : ((n : Nat) -> tm n) ->
(from, to : Nat) -> from `LTE'` to => Telescope tm from to
tabulate f from from @{LTERefl} = [<]
tabulate f from (S to) @{LTESuccR _} = tabulate f from to :< f to
export
tabulate0 : ((n : Nat) -> tm n) -> (n : Nat) -> Context tm n
tabulate0 f n = tabulate f 0 n
export export
pure : from `LTE'` to => a -> Telescope' a from to pure : from `LTE'` to => a -> Telescope' a from to
pure @{LTERefl} x = [<] pure @{LTERefl} x = [<]

176
src/Quox/Equal.idr
View file

@ -1,121 +1,161 @@
module Quox.Equal module Quox.Equal
import public Quox.Syntax import public Quox.Syntax
import public Quox.Reduce
import Quox.Error import Quox.Error
%default total %default total
public export
data Mode = Equal | Sub
public export public export
data Error data Error
= Clash SomeTerm SomeTerm = ClashT Mode (Term d n) (Term d n)
| ClashU Universe Universe | ClashU Mode Universe Universe
| ClashQ Qty Qty | ClashQ Qty Qty
private %inline private %inline
clashT' : Term d n -> Term d n -> Error ClashE : Mode -> Elim d n -> Elim d n -> Error
clashT' = Clash `on` some2 ClashE mode = ClashT mode `on` E
private %inline
clashE' : Elim d n -> Elim d n -> Error
clashE' = clashT' `on` E
parameters {auto _ : MonadThrow Error m} parameters {auto _ : MonadThrow Error m}
private %inline private %inline
clashT : Term d n -> Term d n -> m a clashT : Mode -> Term d n -> Term d n -> m a
clashT = throw .: clashT' clashT mode = throw .: ClashT mode
private %inline private %inline
clashE : Elim d n -> Elim d n -> m a clashE : Mode -> Elim d n -> Elim d n -> m a
clashE = clashT `on` E clashE mode = throw .: ClashE mode
private %inline
eq : Eq a => (a -> a -> Error) -> a -> a -> m ()
eq err a b = unless (a == b) $ throw $ err a b
mutual mutual
private covering private covering
equalTN' : (s, t : Term 0 n) -> compareTN' : Mode ->
(s, t : Term 0 n) ->
(0 _ : NotRedexT s) -> (0 _ : NotRedexT t) -> m () (0 _ : NotRedexT s) -> (0 _ : NotRedexT t) -> m ()
equalTN' (TYPE k) (TYPE l) _ _ = compareTN' mode (TYPE k) (TYPE l) _ _ =
eq ClashU k l case mode of
equalTN' s@(TYPE _) t _ _ = clashT s t Equal => unless (k == l) $ throw $ ClashU Equal k l
Sub => unless (k <= l) $ throw $ ClashU Sub k l
compareTN' mode s@(TYPE _) t _ _ = clashT mode s t
equalTN' (Pi qtm1 qty1 _ arg1 res1) (Pi qtm2 qty2 _ arg2 res2) _ _ = do compareTN' mode (Pi qtm1 qty1 _ arg1 res1)
eq ClashQ qtm1 qtm2 (Pi qtm2 qty2 _ arg2 res2) _ _ = do
eq ClashQ qty1 qty2 -- [todo] these should probably always be ==, right..?
equalT0 arg1 arg2 unless (qtm1 == qtm2) $ throw $ ClashQ qtm1 qtm2
equalTS0 res1 res2 unless (qty1 == qty2) $ throw $ ClashQ qty1 qty2
equalTN' s@(Pi {}) t _ _ = clashT s t compareT0 mode arg2 arg1 -- reversed for contravariant Sub
compareTS0 mode res1 res2
compareTN' mode s@(Pi {}) t _ _ = clashT mode s t
-- [todo] eta -- [todo] eta
equalTN' (Lam _ body1) (Lam _ body2) _ _ = compareTN' _ (Lam _ body1) (Lam _ body2) _ _ =
equalTS0 body1 body2 compareTS0 Equal body1 body2
equalTN' s@(Lam {}) t _ _ = clashT s t compareTN' mode s@(Lam {}) t _ _ = clashT mode s t
equalTN' (E e) (E f) ps pt = equalE0 e f compareTN' mode (E e) (E f) ps pt = compareE0 mode e f
equalTN' s@(E _) t _ _ = clashT s t compareTN' mode s@(E _) t _ _ = clashT mode s t
equalTN' (CloT {}) _ ps _ = void $ ps IsCloT compareTN' _ (CloT {}) _ ps _ = void $ ps IsCloT
equalTN' (DCloT {}) _ ps _ = void $ ps IsDCloT compareTN' _ (DCloT {}) _ ps _ = void $ ps IsDCloT
private covering private covering
equalEN' : (e, f : Elim 0 n) -> compareEN' : Mode ->
(e, f : Elim 0 n) ->
(0 _ : NotRedexE e) -> (0 _ : NotRedexE f) -> m () (0 _ : NotRedexE e) -> (0 _ : NotRedexE f) -> m ()
equalEN' (F x) (F y) _ _ = do compareEN' mode e@(F x) f@(F y) _ _ =
eq (clashE' `on` F {d = 0, n = 0}) x y unless (x == y) $ clashE mode e f
equalEN' e@(F _) f _ _ = clashE e f compareEN' mode e@(F _) f _ _ = clashE mode e f
equalEN' (B i) (B j) _ _ = do compareEN' mode e@(B i) f@(B j) _ _ =
eq (clashE' `on` B {d = 0}) i j unless (i == j) $ clashE mode e f
equalEN' e@(B _) f _ _ = clashE e f compareEN' mode e@(B _) f _ _ = clashE mode e f
equalEN' (fun1 :@ arg1) (fun2 :@ arg2) _ _ = do -- [todo] tracking variance of functions? maybe???
equalE0 fun1 fun2 -- probably not
equalT0 arg1 arg2 compareEN' _ (fun1 :@ arg1) (fun2 :@ arg2) _ _ = do
equalEN' e@(_ :@ _) f _ _ = clashE e f compareE0 Equal fun1 fun2
compareT0 Equal arg1 arg2
compareEN' mode e@(_ :@ _) f _ _ = clashE mode e f
equalEN' (tm1 :# ty1) (tm2 :# ty2) _ _ = do -- [todo] is always checking the types are equal correct?
equalT0 tm1 tm2 compareEN' mode (tm1 :# ty1) (tm2 :# ty2) _ _ = do
equalT0 ty1 ty2 compareT0 mode tm1 tm2
equalEN' e@(_ :# _) f _ _ = clashE e f compareT0 Equal ty1 ty2
compareEN' mode e@(_ :# _) f _ _ = clashE mode e f
equalEN' (CloE {}) _ pe _ = void $ pe IsCloE compareEN' _ (CloE {}) _ pe _ = void $ pe IsCloE
equalEN' (DCloE {}) _ pe _ = void $ pe IsDCloE compareEN' _ (DCloE {}) _ pe _ = void $ pe IsDCloE
private covering %inline private covering %inline
equalTN : NonRedexTerm 0 n -> NonRedexTerm 0 n -> m () compareTN : Mode -> NonRedexTerm 0 n -> NonRedexTerm 0 n -> m ()
equalTN s t = equalTN' s.fst t.fst s.snd t.snd compareTN mode s t = compareTN' mode s.fst t.fst s.snd t.snd
private covering %inline private covering %inline
equalEN : NonRedexElim 0 n -> NonRedexElim 0 n -> m () compareEN : Mode -> NonRedexElim 0 n -> NonRedexElim 0 n -> m ()
equalEN e f = equalEN' e.fst f.fst e.snd f.snd compareEN mode e f = compareEN' mode e.fst f.fst e.snd f.snd
export covering %inline export covering %inline
equalT : DimEq d -> Term d n -> Term d n -> m () compareT : Mode -> DimEq d -> Term d n -> Term d n -> m ()
equalT eqs s t = compareT mode eqs s t =
for_ (splits eqs) $ \th => (s /// th) `equalT0` (t /// th) for_ (splits eqs) $ \th => compareT0 mode (s /// th) (t /// th)
export covering %inline export covering %inline
equalE : DimEq d -> Elim d n -> Elim d n -> m () compareE : Mode -> DimEq d -> Elim d n -> Elim d n -> m ()
equalE eqs e f = compareE mode eqs e f =
for_ (splits eqs) $ \th => (e /// th) `equalE0` (f /// th) for_ (splits eqs) $ \th => compareE0 mode (e /// th) (f /// th)
export covering %inline export covering %inline
equalT0 : Term 0 n -> Term 0 n -> m () compareT0 : Mode -> Term 0 n -> Term 0 n -> m ()
equalT0 s t = whnfT s `equalTN` whnfT t compareT0 mode s t = compareTN mode (whnfT s) (whnfT t)
export covering %inline export covering %inline
equalE0 : Elim 0 n -> Elim 0 n -> m () compareE0 : Mode -> Elim 0 n -> Elim 0 n -> m ()
equalE0 e f = whnfE e `equalEN` whnfE f compareE0 mode e f = compareEN mode (whnfE e) (whnfE f)
export covering %inline export covering %inline
equalTS0 : ScopeTerm 0 n -> ScopeTerm 0 n -> m () compareTS0 : Mode -> ScopeTerm 0 n -> ScopeTerm 0 n -> m ()
equalTS0 (TUnused body1) (TUnused body2) = equalT0 body1 body2 compareTS0 mode (TUnused body1) (TUnused body2) =
equalTS0 body1 body2 = compareT0 mode body1 body2
fromScopeTerm body1 `equalT0` fromScopeTerm body2 compareTS0 mode body1 body2 =
compareT0 mode (fromScopeTerm body1) (fromScopeTerm body2)
export covering %inline
equalTWith : DimEq d -> Term d n -> Term d n -> m ()
equalTWith = compareT Equal
export covering %inline
equalEWith : DimEq d -> Elim d n -> Elim d n -> m ()
equalEWith = compareE Equal
export covering %inline
subTWith : DimEq d -> Term d n -> Term d n -> m ()
subTWith = compareT Sub
export covering %inline
subEWith : DimEq d -> Elim d n -> Elim d n -> m ()
subEWith = compareE Sub
export covering %inline
equalT : {d : Nat} -> Term d n -> Term d n -> m ()
equalT = equalTWith DimEq.new
export covering %inline
equalE : {d : Nat} -> Elim d n -> Elim d n -> m ()
equalE = equalEWith DimEq.new
export covering %inline
subT : {d : Nat} -> Term d n -> Term d n -> m ()
subT = subTWith DimEq.new
export covering %inline
subE : {d : Nat} -> Elim d n -> Elim d n -> m ()
subE = subEWith DimEq.new

5
src/Quox/Error.idr
View file

@ -183,6 +183,11 @@ interface MonadThrow err m1 => MonadCatch err m1 m2 | err, m1 where
public export public export
interface (Monad m1, Monad m2) => MonadEmbed m1 m2 where embed : m1 a -> m2 a interface (Monad m1, Monad m2) => MonadEmbed m1 m2 where embed : m1 a -> m2 a
public export
MonadThrows : (errs : List Type) -> (m : Type -> Type) -> Type
MonadThrows [] m = Monad m
MonadThrows (ty :: tys) m = (MonadThrow ty m, MonadThrows tys m)
export %inline export %inline
implementation implementation

6
src/Quox/NatExtra.idr
View file

@ -20,9 +20,9 @@ lteSucc' LTERefl = LTERefl
lteSucc' (LTESuccR p) = LTESuccR $ lteSucc' p lteSucc' (LTESuccR p) = LTESuccR $ lteSucc' p
public export public export
fromLTE : {n : Nat} -> LTE m n -> LTE' m n fromLte : {n : Nat} -> LTE m n -> LTE' m n
fromLTE LTEZero = lteZero' fromLte LTEZero = lteZero'
fromLTE (LTESucc p) = lteSucc' $ fromLTE p fromLte (LTESucc p) = lteSucc' $ fromLte p
public export public export
toLte : {n : Nat} -> m `LTE'` n -> m `LTE` n toLte : {n : Nat} -> m `LTE'` n -> m `LTE` n

2
src/Quox/OPE.idr
View file

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

121
src/Quox/Reduce.idr Normal file
View file

@ -0,0 +1,121 @@
module Quox.Reduce
import public Quox.Syntax
public export
data IsRedexT : Term d n -> Type where
IsUpsilon : IsRedexT $ E (_ :# _)
IsCloT : IsRedexT $ CloT {}
IsDCloT : IsRedexT $ DCloT {}
public export %inline
NotRedexT : Term d n -> Type
NotRedexT = Not . IsRedexT
public export
data IsRedexE : Elim d n -> Type where
IsBetaLam : IsRedexE $ (Lam {} :# Pi {}) :@ _
IsCloE : IsRedexE $ CloE {}
IsDCloE : IsRedexE $ DCloE {}
public export %inline
NotRedexE : Elim d n -> Type
NotRedexE = Not . IsRedexE
export %inline
isRedexT : (t : Term d n) -> Dec (IsRedexT t)
isRedexT (E (_ :# _)) = Yes IsUpsilon
isRedexT (CloT {}) = Yes IsCloT
isRedexT (DCloT {}) = Yes IsDCloT
isRedexT (TYPE _) = No $ \x => case x of {}
isRedexT (Pi {}) = No $ \x => case x of {}
isRedexT (Lam {}) = No $ \x => case x of {}
isRedexT (E (F _)) = No $ \x => case x of {}
isRedexT (E (B _)) = No $ \x => case x of {}
isRedexT (E (_ :@ _)) = No $ \x => case x of {}
isRedexT (E (CloE {})) = No $ \x => case x of {}
isRedexT (E (DCloE {})) = No $ \x => case x of {}
export %inline
isRedexE : (e : Elim d n) -> Dec (IsRedexE e)
isRedexE ((Lam {} :# Pi {}) :@ _) = Yes IsBetaLam
isRedexE (CloE {}) = Yes IsCloE
isRedexE (DCloE {}) = Yes IsDCloE
isRedexE (F x) = No $ \x => case x of {}
isRedexE (B i) = No $ \x => case x of {}
isRedexE (F _ :@ _) = No $ \x => case x of {}
isRedexE (B _ :@ _) = No $ \x => case x of {}
isRedexE (_ :@ _ :@ _) = No $ \x => case x of {}
isRedexE ((TYPE _ :# _) :@ _) = No $ \x => case x of {}
isRedexE ((Pi {} :# _) :@ _) = No $ \x => case x of {}
isRedexE ((Lam {} :# TYPE _) :@ _) = No $ \x => case x of {}
isRedexE ((Lam {} :# Lam {}) :@ _) = No $ \x => case x of {}
isRedexE ((Lam {} :# E _) :@ _) = No $ \x => case x of {}
isRedexE ((Lam {} :# CloT {}) :@ _) = No $ \x => case x of {}
isRedexE ((Lam {} :# DCloT {}) :@ _) = No $ \x => case x of {}
isRedexE ((E _ :# _) :@ _) = No $ \x => case x of {}
isRedexE ((CloT {} :# _) :@ _) = No $ \x => case x of {}
isRedexE ((DCloT {} :# _) :@ _) = No $ \x => case x of {}
isRedexE (CloE {} :@ _) = No $ \x => case x of {}
isRedexE (DCloE {} :@ _) = No $ \x => case x of {}
isRedexE (_ :# _) = No $ \x => case x of {}
public export %inline
RedexTerm : Nat -> Nat -> Type
RedexTerm d n = Subset (Term d n) IsRedexT
public export %inline
NonRedexTerm : Nat -> Nat -> Type
NonRedexTerm d n = Subset (Term d n) NotRedexT
public export %inline
RedexElim : Nat -> Nat -> Type
RedexElim d n = Subset (Elim d n) IsRedexE
public export %inline
NonRedexElim : Nat -> Nat -> Type
NonRedexElim d n = Subset (Elim d n) NotRedexE
||| substitute a term with annotation for the bound variable of a `ScopeTerm`
export %inline
substScope : (arg, argTy : Term d n) -> (body : ScopeTerm d n) -> Term d n
substScope arg argTy (TUsed body) = body // one (arg :# argTy)
substScope arg argTy (TUnused body) = body
export %inline
stepT' : (s : Term d n) -> IsRedexT s -> Term d n
stepT' (E (s :# _)) IsUpsilon = s
stepT' (CloT s th) IsCloT = pushSubstsTWith' id th s
stepT' (DCloT s th) IsDCloT = pushSubstsTWith' th id s
export %inline
stepT : (s : Term d n) -> Either (NotRedexT s) (Term d n)
stepT s = case isRedexT s of Yes y => Right $ stepT' s y; No n => Left n
export %inline
stepE' : (e : Elim d n) -> IsRedexE e -> Elim d n
stepE' ((Lam {body, _} :# Pi {arg, res, _}) :@ s) IsBetaLam =
substScope s arg body :# substScope s arg res
stepE' (CloE e th) IsCloE = pushSubstsEWith' id th e
stepE' (DCloE e th) IsDCloE = pushSubstsEWith' th id e
export %inline
stepE : (e : Elim d n) -> Either (NotRedexE e) (Elim d n)
stepE e = case isRedexE e of Yes y => Right $ stepE' e y; No n => Left n
export covering
whnfT : Term d n -> NonRedexTerm d n
whnfT s = case stepT s of
Right s' => whnfT s'
Left done => Element s done
export covering
whnfE : Elim d n -> NonRedexElim d n
whnfE e = case stepE e of
Right e' => whnfE e'
Left done => Element e done

16
src/Quox/Syntax/DimEq.idr
View file

@ -33,13 +33,13 @@ zeroEq : DimEq 0
zeroEq = C [<] zeroEq = C [<]
export export
new' : (d : Nat) -> DimEq' d new' : {d : Nat} -> DimEq' d
new' 0 = [<] new' {d = 0} = [<]
new' (S d) = new' d :< Nothing new' {d = S d} = new' :< Nothing
export %inline export %inline
new : (d : Nat) -> DimEq d new : {d : Nat} -> DimEq d
new d = C (new' d) new = C new'
private %inline private %inline
@ -147,16 +147,16 @@ splits (C eqs) = splits' eqs
private private
0 newGetShift : (d : Nat) -> (i : Var d) -> (by : Shift d d') -> 0 newGetShift : (d : Nat) -> (i : Var d) -> (by : Shift d d') ->
getShift' by (new' d) i = Nothing getShift' by (new' {d}) i = Nothing
newGetShift (S d) VZ by = Refl newGetShift (S d) VZ by = Refl
newGetShift (S d) (VS i) by = newGetShift d i (drop1 by) newGetShift (S d) (VS i) by = newGetShift d i (drop1 by)
export export
0 newGet' : (d : Nat) -> (i : Var d) -> get' (new' d) i = Nothing 0 newGet' : (d : Nat) -> (i : Var d) -> get' (new' {d}) i = Nothing
newGet' d i = newGetShift d i SZ newGet' d i = newGetShift d i SZ
export export
0 newGet : (d : Nat) -> (p : Dim d) -> get (new' d) p = p 0 newGet : (d : Nat) -> (p : Dim d) -> get (new' {d}) p = p
newGet d (K e) = Refl newGet d (K e) = Refl
newGet d (B i) = rewrite newGet' d i in Refl newGet d (B i) = rewrite newGet' d i in Refl

17
src/Quox/Syntax/Shift.idr
View file

@ -71,6 +71,10 @@ fromNat Z = SZ
fromNat (S by) = SS $ fromNat by fromNat (S by) = SS $ fromNat by
%transform "Shift.fromNat" Shift.fromNat x = believe_me x %transform "Shift.fromNat" Shift.fromNat x = believe_me x
public export
fromNat0 : (by : Nat) -> Shift 0 by
fromNat0 by = rewrite sym $ plusZeroRightNeutral by in fromNat by
export export
0 fromToNat : (by : Shift from to) -> by `Eqv` fromNat by.nat {from} 0 fromToNat : (by : Shift from to) -> by `Eqv` fromNat by.nat {from}
fromToNat SZ = EqSZ fromToNat SZ = EqSZ
@ -96,6 +100,19 @@ export %inline
Injective Shift.(.nat) where injective eq = irrelevantEq $ toNatInj eq Injective Shift.(.nat) where injective eq = irrelevantEq $ toNatInj eq
public export
ssDown : Shift (S from) to -> Shift from to
ssDown SZ = SS SZ
ssDown (SS by) = SS (ssDown by)
export
0 ssDownEqv : (by : Shift (S from) to) -> ssDown by `Eqv` SS by
ssDownEqv SZ = EqSS EqSZ
ssDownEqv (SS by) = EqSS $ ssDownEqv by
%transform "Shift.ssDown" ssDown by = believe_me (SS by)
public export public export
shift : Shift from to -> Var from -> Var to shift : Shift from to -> Var from -> Var to
shift SZ i = i shift SZ i = i

669
src/Quox/Syntax/Term.idr
View file

@ -1,666 +1,7 @@
module Quox.Syntax.Term module Quox.Syntax.Term
import public Quox.Syntax.Var import public Quox.Syntax.Term.Base
import public Quox.Syntax.Shift import public Quox.Syntax.Term.Split
import public Quox.Syntax.Subst import public Quox.Syntax.Term.Subst
import public Quox.Syntax.Universe import public Quox.Syntax.Term.Reduce
import public Quox.Syntax.Qty import public Quox.Syntax.Term.Pretty
import public Quox.Syntax.Dim
import public Quox.Name
import public Quox.OPE
import Quox.Pretty
import public Data.DPair
import Data.List
import Data.Maybe
import Data.Nat
import public Data.So
import Data.String
import Data.Vect
%default total
infixl 8 :#
infixl 9 :@
mutual
public export
TSubst : Nat -> Nat -> Nat -> Type
TSubst d = Subst (\n => Elim d n)
||| first argument `d` is dimension scope size, second `n` is term scope size
public export
data Term : (d, n : Nat) -> Type where
||| type of types
TYPE : (l : Universe) -> Term d n
||| function type
Pi : (qtm, qty : Qty) -> (x : Name) ->
(arg : Term d n) -> (res : ScopeTerm d n) -> Term d n
||| function term
Lam : (x : Name) -> (body : ScopeTerm d n) -> Term d n
||| elimination
E : (e : Elim d n) -> Term d n
||| term closure/suspended substitution
CloT : (tm : Term d from) -> (th : Lazy (TSubst d from to)) -> Term d to
||| dimension closure/suspended substitution
DCloT : (tm : Term dfrom n) -> (th : Lazy (DSubst dfrom dto)) -> Term dto n
||| first argument `d` is dimension scope size, second `n` is term scope size
public export
data Elim : (d, n : Nat) -> Type where
||| free variable
F : (x : Name) -> Elim d n
||| bound variable
B : (i : Var n) -> Elim d n
||| term application
(:@) : (fun : Elim d n) -> (arg : Term d n) -> Elim d n
||| type-annotated term
(:#) : (tm, ty : Term d n) -> Elim d n
||| term closure/suspended substitution
CloE : (el : Elim d from) -> (th : Lazy (TSubst d from to)) -> Elim d to
||| dimension closure/suspended substitution
DCloE : (el : Elim dfrom n) -> (th : Lazy (DSubst dfrom dto)) -> Elim dto n
||| a scope with one more bound variable
public export
data ScopeTerm : (d, n : Nat) -> Type where
||| variable is used
TUsed : (body : Term d (S n)) -> ScopeTerm d n
||| variable is unused
TUnused : (body : Term d n) -> ScopeTerm d n
||| a scope with one more bound dimension variable
public export
data DScopeTerm : (d, n : Nat) -> Type where
||| variable is used
DUsed : (body : Term (S d) n) -> DScopeTerm d n
||| variable is unused
DUnused : (body : Term d n) -> DScopeTerm d n
%name Term s, t, r
%name Elim e, f
%name ScopeTerm body
%name DScopeTerm body
export
fromDScopeTerm : DScopeTerm d n -> Term (S d) n
fromDScopeTerm (DUsed body) = body
fromDScopeTerm (DUnused body) = body `DCloT` shift 1
export
fromScopeTerm : ScopeTerm d n -> Term d (S n)
fromScopeTerm (TUsed body) = body
fromScopeTerm (TUnused body) = body `CloT` shift 1
||| same as `F` but as a term
public export %inline
FT : Name -> Term d n
FT = E . F
||| 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) => Elim d n
BV i = B $ V i
||| same as `BV` but as a term
public export %inline
BVT : (i : Nat) -> (0 _ : LT i n) => Term d n
BVT i = E $ BV i
public export %inline
isLam : Term d n -> Bool
isLam (Lam {}) = True
isLam _ = False
public export
NotLam : Term d n -> Type
NotLam = So . not . isLam
public export %inline
isApp : Elim d n -> Bool
isApp ((:@) {}) = True
isApp _ = False
public export
NotApp : Elim d n -> Type
NotApp = So . not . isApp
infixl 9 :@@
||| apply multiple arguments at once
public export %inline
(:@@) : Elim d n -> List (Term d n) -> Elim d n
f :@@ ss = foldl (:@) f ss
public export
record GetArgs (d, n : Nat) where
constructor GotArgs
fun : Elim d n
args : List (Term d n)
0 notApp : NotApp fun
private
getArgs' : Elim d n -> List (Term d n) -> GetArgs d n
getArgs' fun args with (choose $ isApp fun)
getArgs' (f :@ a) args | Left yes = getArgs' f (a :: args)
_ | Right no = GotArgs {fun, args, notApp = no}
||| splits an application into its head and arguments. if it's not an
||| application then the list is just empty
export %inline
getArgs : Elim d n -> GetArgs d n
getArgs e = getArgs' e []
infixr 1 :\\
public export
(:\\) : Vect m Name -> Term d (m + n) -> Term d n
[] :\\ t = t
x :: xs :\\ t = let t' = replace {p = Term _} (plusSuccRightSucc {}) t in
Lam x $ TUsed $ xs :\\ t'
public export
record GetLams (d, n : Nat) where
constructor GotLams
names : Vect lams Name
body : Term d rest
0 eq : lams + n = rest
0 notLam : NotLam body
public export
getLams : Term d n -> GetLams d n
getLams s with (choose $ isLam s)
getLams s@(Lam x body) | Left yes =
let inner = getLams $ assert_smaller s $ fromScopeTerm body in
GotLams {names = x :: inner.names,
body = inner.body,
eq = plusSuccRightSucc {} `trans` inner.eq,
notLam = inner.notLam}
_ | Right no = GotLams {names = [], body = s, eq = Refl, notLam = no}
parameters {auto _ : Pretty.HasEnv m}
private %inline arrowD : m (Doc HL)
arrowD = hlF Syntax $ ifUnicode "→" "->"
private %inline lamD : m (Doc HL)
lamD = hlF Syntax $ ifUnicode "λ" "fun"
private %inline annD : m (Doc HL)
annD = hlF Syntax $ ifUnicode "⦂" "::"
private %inline typeD : Doc HL
typeD = hl Syntax "Type"
private %inline colonD : Doc HL
colonD = hl Syntax ":"
mutual
export covering
PrettyHL (Term d n) where
prettyM (TYPE l) =
parensIfM App $ typeD <//> !(withPrec Arg $ prettyM l)
prettyM (Pi qtm qty x s t) =
parensIfM Outer $ hang 2 $
!(prettyBinder [qtm, qty] x s) <++> !arrowD
<//> !(under T x $ prettyM t)
prettyM (Lam x t) =
parensIfM Outer $
sep [!lamD, hl TVar !(prettyM x), !arrowD]
<//> !(under T x $ prettyM t)
prettyM (E e) =
prettyM e
prettyM (CloT s th) =
parensIfM SApp . hang 2 =<<
[|withPrec SApp (prettyM s) </> prettyTSubst th|]
prettyM (DCloT s th) =
parensIfM SApp . hang 2 =<<
[|withPrec SApp (prettyM s) </> prettyDSubst th|]
export covering
PrettyHL (Elim d n) where
prettyM (F x) =
hl' Free <$> prettyM x
prettyM (B i) =
prettyVar TVar TVarErr (!ask).tnames i
prettyM (e :@ s) =
let GotArgs f args _ = getArgs' e [s] in
parensIfM App =<< withPrec Arg
[|prettyM f <//> (align . sep <$> traverse prettyM args)|]
prettyM (s :# a) =
parensIfM Ann $ hang 2 $
!(withPrec AnnL $ prettyM s) <++> !annD
<//> !(withPrec Ann $ prettyM a)
prettyM (CloE e th) =
parensIfM SApp . hang 2 =<<
[|withPrec SApp (prettyM e) </> prettyTSubst th|]
prettyM (DCloE e th) =
parensIfM SApp . hang 2 =<<
[|withPrec SApp (prettyM e) </> prettyDSubst th|]
export covering
PrettyHL (ScopeTerm d n) where
prettyM body = prettyM $ fromScopeTerm body
export covering
prettyTSubst : Pretty.HasEnv m => TSubst d from to -> m (Doc HL)
prettyTSubst s = prettySubstM prettyM (!ask).tnames TVar "[" "]" s
export covering
prettyBinder : Pretty.HasEnv m => List Qty -> Name -> Term d n -> m (Doc HL)
prettyBinder pis x a =
pure $ parens $ hang 2 $
hsep [hl TVar !(prettyM x),
sep [!(prettyQtyBinds pis),
hsep [colonD, !(withPrec Outer $ prettyM a)]]]
export FromVar (Elim d) where fromVar = B
export FromVar (Term d) where fromVar = E . fromVar
||| does the minimal reasonable work:
||| - deletes the closure around a free name since it doesn't do anything
||| - deletes an identity substitution
||| - composes (lazily) with an existing top-level closure
||| - immediately looks up a bound variable
||| - otherwise, wraps in a new closure
export
CanSubst (Elim d) (Elim d) where
F x // _ = F x
B i // th = th !! i
CloE e ph // th = assert_total CloE e $ ph . th
e // th = case force th of
Shift SZ => e
th => CloE e th
||| 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 closure
||| - goes inside `E` in case it is a simple variable or something
||| - otherwise, wraps in a new closure
export
CanSubst (Elim d) (Term d) where
TYPE l // _ = TYPE l
E e // th = E $ e // th
CloT s ph // th = CloT s $ ph . th
s // th = case force th of
Shift SZ => s
th => CloT s th
export
CanSubst (Elim d) (ScopeTerm d) where
TUsed body // th = TUsed $ body // push th
TUnused body // th = TUnused $ body // th
export CanSubst Var (Term d) where s // th = s // map (B {d}) th
export CanSubst Var (Elim d) where e // th = e // map (B {d}) th
export CanSubst Var (ScopeTerm d) where s // th = s // map (B {d}) th
export CanShift (Term d) where s // by = s // Shift by {env = Elim d}
export CanShift (Elim d) where e // by = e // Shift by {env = Elim d}
export CanShift (ScopeTerm d) where s // by = s // Shift by {env = Elim d}
infixl 8 ///
mutual
namespace Term
||| applies a dimension substitution with the same behaviour as `(//)`
||| above
export
(///) : Term dfrom n -> DSubst dfrom dto -> Term dto n
TYPE l /// _ = TYPE l
E e /// th = E $ e /// th
DCloT s ph /// th = DCloT s $ ph . th
s /// Shift SZ = s
s /// th = DCloT s th
||| applies a term and dimension substitution
public export %inline
subs : Term dfrom from -> DSubst dfrom dto -> TSubst dto from to ->
Term dto to
subs s th ph = s /// th // ph
namespace Elim
||| applies a dimension substitution with the same behaviour as `(//)`
||| above
export
(///) : Elim dfrom n -> DSubst dfrom dto -> Elim dto n
F x /// _ = F x
B i /// _ = B i
DCloE e ph /// th = DCloE e $ ph . th
e /// Shift SZ = e
e /// th = DCloE e th
||| applies a term and dimension substitution
public export %inline
subs : Elim dfrom from -> DSubst dfrom dto -> TSubst dto from to ->
Elim dto to
subs e th ph = e /// th // ph
namespace ScopeTerm
||| applies a dimension substitution with the same behaviour as `(//)`
||| above
export
(///) : ScopeTerm dfrom n -> DSubst dfrom dto -> ScopeTerm dto n
TUsed body /// th = TUsed $ body /// th
TUnused body /// th = TUnused $ body /// th
||| applies a term and dimension substitution
public export %inline
subs : ScopeTerm dfrom from -> DSubst dfrom dto -> TSubst dto from to ->
ScopeTerm dto to
subs body th ph = body /// th // ph
private %inline
comp' : DSubst dfrom dto -> TSubst dfrom from mid -> TSubst dto mid to ->
TSubst dto from to
comp' th ps ph = map (/// th) ps . ph
mutual
||| true if a term has a closure or dimension closure at the top level,
||| or is `E` applied to such an elimination
public export %inline
topCloT : Term d n -> Bool
topCloT (CloT _ _) = True
topCloT (DCloT _ _) = True
topCloT (E e) = topCloE e
topCloT _ = False
||| true if an elimination has a closure or dimension closure at the top level
public export %inline
topCloE : Elim d n -> Bool
topCloE (CloE _ _) = True
topCloE (DCloE _ _) = True
topCloE _ = False
public export IsNotCloT : Term d n -> Type
IsNotCloT = So . not . topCloT
||| a term which is not a top level closure
public export NotCloTerm : Nat -> Nat -> Type
NotCloTerm d n = Subset (Term d n) IsNotCloT
public export IsNotCloE : Elim d n -> Type
IsNotCloE = So . not . topCloE
||| an elimination which is not a top level closure
public export NotCloElim : Nat -> Nat -> Type
NotCloElim d n = Subset (Elim d n) IsNotCloE
public export %inline
ncloT : (t : Term d n) -> (0 _ : IsNotCloT t) => NotCloTerm d n
ncloT t @{p} = Element t p
public export %inline
ncloE : (t : Elim d n) -> (0 _ : IsNotCloE t) => NotCloElim d n
ncloE e @{p} = Element e p
mutual
||| if the input term has any top-level closures, push them under one layer of
||| syntax
export %inline
pushSubstsT : Term d n -> NotCloTerm d n
pushSubstsT s = pushSubstsTWith id id s
||| if the input elimination has any top-level closures, push them under one
||| layer of syntax
export %inline
pushSubstsE : Elim d n -> NotCloElim d n
pushSubstsE e = pushSubstsEWith id id e
export
pushSubstsTWith : DSubst dfrom dto -> TSubst dto from to ->
Term dfrom from -> NotCloTerm dto to
pushSubstsTWith th ph (TYPE l) =
ncloT $ TYPE l
pushSubstsTWith th ph (Pi qtm qty x a body) =
ncloT $ Pi qtm qty x (subs a th ph) (subs body th ph)
pushSubstsTWith th ph (Lam x body) =
ncloT $ Lam x $ subs body th ph
pushSubstsTWith th ph (E e) =
let Element e _ = pushSubstsEWith th ph e in ncloT $ E e
pushSubstsTWith th ph (CloT s ps) =
pushSubstsTWith th (comp' th ps ph) s
pushSubstsTWith th ph (DCloT s ps) =
pushSubstsTWith (ps . th) ph s
export
pushSubstsEWith : DSubst dfrom dto -> TSubst dto from to ->
Elim dfrom from -> NotCloElim dto to
pushSubstsEWith th ph (F x) =
ncloE $ F x
pushSubstsEWith th ph (B i) =
assert_total pushSubstsE $ ph !! i
pushSubstsEWith th ph (f :@ s) =
ncloE $ subs f th ph :@ subs s th ph
pushSubstsEWith th ph (s :# a) =
ncloE $ subs s th ph :# subs a th ph
pushSubstsEWith th ph (CloE e ps) =
pushSubstsEWith th (comp' th ps ph) e
pushSubstsEWith th ph (DCloE e ps) =
pushSubstsEWith (ps . th) ph e
parameters (th : DSubst dfrom dto) (ph : TSubst dto from to)
public export %inline
pushSubstsTWith' : Term dfrom from -> Term dto to
pushSubstsTWith' s = (pushSubstsTWith th ph s).fst
public export %inline
pushSubstsEWith' : Elim dfrom from -> Elim dto to
pushSubstsEWith' e = (pushSubstsEWith th ph e).fst
public export %inline
pushSubstsT' : Term d n -> Term d n
pushSubstsT' s = (pushSubstsT s).fst
public export %inline
pushSubstsE' : Elim d n -> Elim d n
pushSubstsE' e = (pushSubstsE e).fst
mutual
-- tightening a term/elim also causes substitutions to be pushed through.
-- this is because otherwise a variable in an unused part of the subst
-- would cause it to incorrectly fail
export covering
Tighten (Term d) where
tighten p (TYPE l) =
pure $ TYPE l
tighten p (Pi qtm qty x arg res) =
Pi qtm qty x <$> tighten p arg
<*> tighten p res
tighten p (Lam x body) =
Lam x <$> tighten p body
tighten p (E e) =
E <$> tighten p e
tighten p (CloT tm th) =
tighten p $ pushSubstsTWith' id th tm
tighten p (DCloT tm th) =
tighten p $ pushSubstsTWith' th id tm
export covering
Tighten (Elim d) where
tighten p (F x) =
pure $ F x
tighten p (B i) =
B <$> tighten p i
tighten p (fun :@ arg) =
[|tighten p fun :@ tighten p arg|]
tighten p (tm :# ty) =
[|tighten p tm :# tighten p ty|]
tighten p (CloE el th) =
tighten p $ pushSubstsEWith' id th el
tighten p (DCloE el th) =
tighten p $ pushSubstsEWith' th id el
export covering
Tighten (ScopeTerm d) where
tighten p (TUsed body) = TUsed <$> tighten (Keep p) body
tighten p (TUnused body) = TUnused <$> tighten p body
public export
data IsRedexT : Term d n -> Type where
IsUpsilon : IsRedexT $ E (_ :# _)
IsCloT : IsRedexT $ CloT {}
IsDCloT : IsRedexT $ DCloT {}
public export %inline
NotRedexT : Term d n -> Type
NotRedexT = Not . IsRedexT
public export
data IsRedexE : Elim d n -> Type where
IsBetaLam : IsRedexE $ (Lam {} :# Pi {}) :@ _
IsCloE : IsRedexE $ CloE {}
IsDCloE : IsRedexE $ DCloE {}
public export %inline
NotRedexE : Elim d n -> Type
NotRedexE = Not . IsRedexE
export %inline
isRedexT : (t : Term d n) -> Dec (IsRedexT t)
isRedexT (E (_ :# _)) = Yes IsUpsilon
isRedexT (CloT {}) = Yes IsCloT
isRedexT (DCloT {}) = Yes IsDCloT
isRedexT (TYPE _) = No $ \x => case x of {}
isRedexT (Pi {}) = No $ \x => case x of {}
isRedexT (Lam {}) = No $ \x => case x of {}
isRedexT (E (F _)) = No $ \x => case x of {}
isRedexT (E (B _)) = No $ \x => case x of {}
isRedexT (E (_ :@ _)) = No $ \x => case x of {}
isRedexT (E (CloE {})) = No $ \x => case x of {}
isRedexT (E (DCloE {})) = No $ \x => case x of {}
export %inline
isRedexE : (e : Elim d n) -> Dec (IsRedexE e)
isRedexE ((Lam {} :# Pi {}) :@ _) = Yes IsBetaLam
isRedexE (CloE {}) = Yes IsCloE
isRedexE (DCloE {}) = Yes IsDCloE
isRedexE (F x) = No $ \x => case x of {}
isRedexE (B i) = No $ \x => case x of {}
isRedexE (F _ :@ _) = No $ \x => case x of {}
isRedexE (B _ :@ _) = No $ \x => case x of {}
isRedexE (_ :@ _ :@ _) = No $ \x => case x of {}
isRedexE ((TYPE _ :# _) :@ _) = No $ \x => case x of {}
isRedexE ((Pi {} :# _) :@ _) = No $ \x => case x of {}
isRedexE ((Lam {} :# TYPE _) :@ _) = No $ \x => case x of {}
isRedexE ((Lam {} :# Lam {}) :@ _) = No $ \x => case x of {}
isRedexE ((Lam {} :# E _) :@ _) = No $ \x => case x of {}
isRedexE ((Lam {} :# CloT {}) :@ _) = No $ \x => case x of {}
isRedexE ((Lam {} :# DCloT {}) :@ _) = No $ \x => case x of {}
isRedexE ((E _ :# _) :@ _) = No $ \x => case x of {}
isRedexE ((CloT {} :# _) :@ _) = No $ \x => case x of {}
isRedexE ((DCloT {} :# _) :@ _) = No $ \x => case x of {}
isRedexE (CloE {} :@ _) = No $ \x => case x of {}
isRedexE (DCloE {} :@ _) = No $ \x => case x of {}
isRedexE (_ :# _) = No $ \x => case x of {}
public export %inline
RedexTerm : Nat -> Nat -> Type
RedexTerm d n = Subset (Term d n) IsRedexT
public export %inline
NonRedexTerm : Nat -> Nat -> Type
NonRedexTerm d n = Subset (Term d n) NotRedexT
public export %inline
RedexElim : Nat -> Nat -> Type
RedexElim d n = Subset (Elim d n) IsRedexE
public export %inline
NonRedexElim : Nat -> Nat -> Type
NonRedexElim d n = Subset (Elim d n) NotRedexE
||| substitute a term with annotation for the bound variable of a `ScopeTerm`
public export %inline
substScope : (arg, argTy : Term d n) -> (body : ScopeTerm d n) -> Term d n
substScope arg argTy (TUsed body) = body // one (arg :# argTy)
substScope arg argTy (TUnused body) = body
public export %inline
stepT' : (s : Term d n) -> IsRedexT s -> Term d n
stepT' (E (s :# _)) IsUpsilon = s
stepT' (CloT s th) IsCloT = pushSubstsTWith' id th s
stepT' (DCloT s th) IsDCloT = pushSubstsTWith' th id s
public export %inline
stepT : (s : Term d n) -> Either (NotRedexT s) (Term d n)
stepT s = case isRedexT s of Yes y => Right $ stepT' s y; No n => Left n
public export %inline
stepE' : (e : Elim d n) -> IsRedexE e -> Elim d n
stepE' ((Lam {body, _} :# Pi {arg, res, _}) :@ s) IsBetaLam =
substScope s arg body :# substScope s arg res
stepE' (CloE e th) IsCloE = pushSubstsEWith' id th e
stepE' (DCloE e th) IsDCloE = pushSubstsEWith' th id e
public export %inline
stepE : (e : Elim d n) -> Either (NotRedexE e) (Elim d n)
stepE e = case isRedexE e of Yes y => Right $ stepE' e y; No n => Left n
public export
whnfT : Term d n -> NonRedexTerm d n
whnfT s = case stepT s of
Right s' => whnfT $ assert_smaller s s'
Left done => Element s done
public export
whnfE : Elim d n -> NonRedexElim d n
whnfE e = case stepE e of
Right e' => whnfE $ assert_smaller e e'
Left done => Element e done
public export
Exists2 : (ty1 -> ty2 -> Type) -> Type
Exists2 t = Exists $ Exists . t
public export %inline
some : {0 f : a -> Type} -> f x -> Exists f
some p = Evidence _ p
public export %inline
some2 : {0 f : a -> b -> Type} -> f x y -> Exists2 f
some2 p = some $ some p
||| A term of some unknown scope sizes.
public export
SomeTerm : Type
SomeTerm = Exists2 Term
||| An elimination of some unknown scope sizes.
public export
SomeElim : Type
SomeElim = Exists2 Elim
||| A dimension of some unknown scope size.
public export
SomeDim : Type
SomeDim = Exists Dim

106
src/Quox/Syntax/Term/Base.idr Normal file
View file

@ -0,0 +1,106 @@
module Quox.Syntax.Term.Base
import public Quox.Syntax.Var
import public Quox.Syntax.Shift
import public Quox.Syntax.Subst
import public Quox.Syntax.Universe
import public Quox.Syntax.Qty
import public Quox.Syntax.Dim
import public Quox.Name
import public Quox.OPE
import Quox.Pretty
import public Data.DPair
import Data.List
import Data.Maybe
import Data.Nat
import public Data.So
import Data.String
import Data.Vect
%default total
infixl 8 :#
infixl 9 :@
mutual
public export
TSubst : Nat -> Nat -> Nat -> Type
TSubst d = Subst (\n => Elim d n)
||| first argument `d` is dimension scope size, second `n` is term scope size
public export
data Term : (d, n : Nat) -> Type where
||| type of types
TYPE : (l : Universe) -> Term d n
||| function type
Pi : (qtm, qty : Qty) -> (x : Name) ->
(arg : Term d n) -> (res : ScopeTerm d n) -> Term d n
||| function term
Lam : (x : Name) -> (body : ScopeTerm d n) -> Term d n
||| elimination
E : (e : Elim d n) -> Term d n
||| term closure/suspended substitution
CloT : (tm : Term d from) -> (th : Lazy (TSubst d from to)) -> Term d to
||| dimension closure/suspended substitution
DCloT : (tm : Term dfrom n) -> (th : Lazy (DSubst dfrom dto)) -> Term dto n
||| first argument `d` is dimension scope size, second `n` is term scope size
public export
data Elim : (d, n : Nat) -> Type where
||| free variable
F : (x : Name) -> Elim d n
||| bound variable
B : (i : Var n) -> Elim d n
||| term application
(:@) : (fun : Elim d n) -> (arg : Term d n) -> Elim d n
||| type-annotated term
(:#) : (tm, ty : Term d n) -> Elim d n
||| term closure/suspended substitution
CloE : (el : Elim d from) -> (th : Lazy (TSubst d from to)) -> Elim d to
||| dimension closure/suspended substitution
DCloE : (el : Elim dfrom n) -> (th : Lazy (DSubst dfrom dto)) -> Elim dto n
||| a scope with one more bound variable
public export
data ScopeTerm : (d, n : Nat) -> Type where
||| variable is used
TUsed : (body : Term d (S n)) -> ScopeTerm d n
||| variable is unused
TUnused : (body : Term d n) -> ScopeTerm d n
||| a scope with one more bound dimension variable
public export
data DScopeTerm : (d, n : Nat) -> Type where
||| variable is used
DUsed : (body : Term (S d) n) -> DScopeTerm d n
||| variable is unused
DUnused : (body : Term d n) -> DScopeTerm d n
%name Term s, t, r
%name Elim e, f
%name ScopeTerm body
%name DScopeTerm body
||| same as `F` but as a term
public export %inline
FT : Name -> Term d n
FT = E . F
||| 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) => Elim d n
BV i = B $ V i
||| same as `BV` but as a term
public export %inline
BVT : (i : Nat) -> (0 _ : LT i n) => Term d n
BVT i = E $ BV i

85
src/Quox/Syntax/Term/Pretty.idr Normal file
View file

@ -0,0 +1,85 @@
module Quox.Syntax.Term.Pretty
import Quox.Syntax.Term.Base
import Quox.Syntax.Term.Split
import Quox.Syntax.Term.Subst
import Quox.Pretty
import Data.Vect
parameters {auto _ : Pretty.HasEnv m}
private %inline arrowD : m (Doc HL)
arrowD = hlF Syntax $ ifUnicode "→" "->"
private %inline lamD : m (Doc HL)
lamD = hlF Syntax $ ifUnicode "λ" "fun"
private %inline annD : m (Doc HL)
annD = hlF Syntax $ ifUnicode "⦂" "::"
private %inline typeD : Doc HL
typeD = hl Syntax "Type"
private %inline colonD : Doc HL
colonD = hl Syntax ":"
mutual
export covering
PrettyHL (Term d n) where
prettyM (TYPE l) =
parensIfM App $ typeD <//> !(withPrec Arg $ prettyM l)
prettyM (Pi qtm qty x s t) =
parensIfM Outer $ hang 2 $
!(prettyBinder [qtm, qty] x s) <++> !arrowD
<//> !(under T x $ prettyM t)
prettyM (Lam x t) =
parensIfM Outer $
sep [!lamD, hl TVar !(prettyM x), !arrowD]
<//> !(under T x $ prettyM t)
prettyM (E e) =
prettyM e
prettyM (CloT s th) =
parensIfM SApp . hang 2 =<<
[|withPrec SApp (prettyM s) </> prettyTSubst th|]
prettyM (DCloT s th) =
parensIfM SApp . hang 2 =<<
[|withPrec SApp (prettyM s) </> prettyDSubst th|]
export covering
PrettyHL (Elim d n) where
prettyM (F x) =
hl' Free <$> prettyM x
prettyM (B i) =
prettyVar TVar TVarErr (!ask).tnames i
prettyM (e :@ s) =
let GotArgs f args _ = getArgs' e [s] in
parensIfM App =<< withPrec Arg
[|prettyM f <//> (align . sep <$> traverse prettyM args)|]
prettyM (s :# a) =
parensIfM Ann $ hang 2 $
!(withPrec AnnL $ prettyM s) <++> !annD
<//> !(withPrec Ann $ prettyM a)
prettyM (CloE e th) =
parensIfM SApp . hang 2 =<<
[|withPrec SApp (prettyM e) </> prettyTSubst th|]
prettyM (DCloE e th) =
parensIfM SApp . hang 2 =<<
[|withPrec SApp (prettyM e) </> prettyDSubst th|]
export covering
PrettyHL (ScopeTerm d n) where
prettyM body = prettyM $ fromScopeTerm body
export covering
prettyTSubst : Pretty.HasEnv m => TSubst d from to -> m (Doc HL)
prettyTSubst s = prettySubstM prettyM (!ask).tnames TVar "[" "]" s
export covering
prettyBinder : Pretty.HasEnv m => List Qty -> Name -> Term d n -> m (Doc HL)
prettyBinder pis x a =
pure $ parens $ hang 2 $
hsep [hl TVar !(prettyM x),
sep [!(prettyQtyBinds pis),
hsep [colonD, !(withPrec Outer $ prettyM a)]]]

163
src/Quox/Syntax/Term/Reduce.idr Normal file
View file

@ -0,0 +1,163 @@
module Quox.Syntax.Term.Reduce
import Quox.Syntax.Term.Base
import Quox.Syntax.Term.Subst
mutual
||| true if a term has a closure or dimension closure at the top level,
||| or is `E` applied to such an elimination
public export %inline
topCloT : Term d n -> Bool
topCloT (CloT _ _) = True
topCloT (DCloT _ _) = True
topCloT (E e) = topCloE e
topCloT _ = False
||| true if an elimination has a closure or dimension closure at the top level
public export %inline
topCloE : Elim d n -> Bool
topCloE (CloE _ _) = True
topCloE (DCloE _ _) = True
topCloE _ = False
public export IsNotCloT : Term d n -> Type
IsNotCloT = So . not . topCloT
||| a term which is not a top level closure
public export NotCloTerm : Nat -> Nat -> Type
NotCloTerm d n = Subset (Term d n) IsNotCloT
public export IsNotCloE : Elim d n -> Type
IsNotCloE = So . not . topCloE
||| an elimination which is not a top level closure
public export NotCloElim : Nat -> Nat -> Type
NotCloElim d n = Subset (Elim d n) IsNotCloE
public export %inline
ncloT : (t : Term d n) -> (0 _ : IsNotCloT t) => NotCloTerm d n
ncloT t @{p} = Element t p
public export %inline
ncloE : (t : Elim d n) -> (0 _ : IsNotCloE t) => NotCloElim d n
ncloE e @{p} = Element e p
mutual
||| if the input term has any top-level closures, push them under one layer of
||| syntax
export %inline
pushSubstsT : Term d n -> NotCloTerm d n
pushSubstsT s = pushSubstsTWith id id s
||| if the input elimination has any top-level closures, push them under one
||| layer of syntax
export %inline
pushSubstsE : Elim d n -> NotCloElim d n
pushSubstsE e = pushSubstsEWith id id e
export
pushSubstsTWith : DSubst dfrom dto -> TSubst dto from to ->
Term dfrom from -> NotCloTerm dto to
pushSubstsTWith th ph (TYPE l) =
ncloT $ TYPE l
pushSubstsTWith th ph (Pi qtm qty x a body) =
ncloT $ Pi qtm qty x (subs a th ph) (subs body th ph)
pushSubstsTWith th ph (Lam x body) =
ncloT $ Lam x $ subs body th ph
pushSubstsTWith th ph (E e) =
let Element e _ = pushSubstsEWith th ph e in ncloT $ E e
pushSubstsTWith th ph (CloT s ps) =
pushSubstsTWith th (comp' th ps ph) s
pushSubstsTWith th ph (DCloT s ps) =
pushSubstsTWith (ps . th) ph s
export
pushSubstsEWith : DSubst dfrom dto -> TSubst dto from to ->
Elim dfrom from -> NotCloElim dto to
pushSubstsEWith th ph (F x) =
ncloE $ F x
pushSubstsEWith th ph (B i) =
assert_total pushSubstsE $ ph !! i
pushSubstsEWith th ph (f :@ s) =
ncloE $ subs f th ph :@ subs s th ph
pushSubstsEWith th ph (s :# a) =
ncloE $ subs s th ph :# subs a th ph
pushSubstsEWith th ph (CloE e ps) =
pushSubstsEWith th (comp' th ps ph) e
pushSubstsEWith th ph (DCloE e ps) =
pushSubstsEWith (ps . th) ph e
parameters (th : DSubst dfrom dto) (ph : TSubst dto from to)
public export %inline
pushSubstsTWith' : Term dfrom from -> Term dto to
pushSubstsTWith' s = (pushSubstsTWith th ph s).fst
public export %inline
pushSubstsEWith' : Elim dfrom from -> Elim dto to
pushSubstsEWith' e = (pushSubstsEWith th ph e).fst
public export %inline
pushSubstsT' : Term d n -> Term d n
pushSubstsT' s = (pushSubstsT s).fst
public export %inline
pushSubstsE' : Elim d n -> Elim d n
pushSubstsE' e = (pushSubstsE e).fst
mutual
-- tightening a term/elim also causes substitutions to be pushed through.
-- this is because otherwise a variable in an unused part of the subst
-- would cause it to incorrectly fail
export covering
Tighten (Term d) where
tighten p (TYPE l) =
pure $ TYPE l
tighten p (Pi qtm qty x arg res) =
Pi qtm qty x <$> tighten p arg
<*> tighten p res
tighten p (Lam x body) =
Lam x <$> tighten p body
tighten p (E e) =
E <$> tighten p e
tighten p (CloT tm th) =
tighten p $ pushSubstsTWith' id th tm
tighten p (DCloT tm th) =
tighten p $ pushSubstsTWith' th id tm
export covering
Tighten (Elim d) where
tighten p (F x) =
pure $ F x
tighten p (B i) =
B <$> tighten p i
tighten p (fun :@ arg) =
[|tighten p fun :@ tighten p arg|]
tighten p (tm :# ty) =
[|tighten p tm :# tighten p ty|]
tighten p (CloE el th) =
tighten p $ pushSubstsEWith' id th el
tighten p (DCloE el th) =
tighten p $ pushSubstsEWith' th id el
export covering
Tighten (ScopeTerm d) where
tighten p (TUsed body) = TUsed <$> tighten (Keep p) body
tighten p (TUnused body) = TUnused <$> tighten p body
public export %inline
weakT : Term d n -> Term d (S n)
weakT t = t //. shift 1
public export %inline
weakE : Elim d n -> Elim d (S n)
weakE t = t //. shift 1

82
src/Quox/Syntax/Term/Split.idr Normal file
View file

@ -0,0 +1,82 @@
module Quox.Syntax.Term.Split
import Quox.Syntax.Term.Base
import Quox.Syntax.Term.Subst
import Data.So
import Data.Vect
%default total
public export %inline
isLam : Term d n -> Bool
isLam (Lam {}) = True
isLam _ = False
public export
NotLam : Term d n -> Type
NotLam = So . not . isLam
public export %inline
isApp : Elim d n -> Bool
isApp ((:@) {}) = True
isApp _ = False
public export
NotApp : Elim d n -> Type
NotApp = So . not . isApp
infixl 9 :@@
||| apply multiple arguments at once
public export %inline
(:@@) : Elim d n -> List (Term d n) -> Elim d n
f :@@ ss = foldl (:@) f ss
public export
record GetArgs (d, n : Nat) where
constructor GotArgs
fun : Elim d n
args : List (Term d n)
0 notApp : NotApp fun
export
getArgs' : Elim d n -> List (Term d n) -> GetArgs d n
getArgs' fun args with (choose $ isApp fun)
getArgs' (f :@ a) args | Left yes = getArgs' f (a :: args)
_ | Right no = GotArgs {fun, args, notApp = no}
||| splits an application into its head and arguments. if it's not an
||| application then the list is just empty
export %inline
getArgs : Elim d n -> GetArgs d n
getArgs e = getArgs' e []
infixr 1 :\\
public export
(:\\) : Vect m Name -> Term d (m + n) -> Term d n
[] :\\ t = t
x :: xs :\\ t = let t' = replace {p = Term _} (plusSuccRightSucc {}) t in
Lam x $ TUsed $ xs :\\ t'
public export
record GetLams (d, n : Nat) where
constructor GotLams
names : Vect lams Name
body : Term d rest
0 eq : lams + n = rest
0 notLam : NotLam body
public export
getLams : Term d n -> GetLams d n
getLams s with (choose $ isLam s)
getLams s@(Lam x body) | Left yes =
let inner = getLams $ assert_smaller s $ fromScopeTerm body in
GotLams {names = x :: inner.names,
body = inner.body,
eq = plusSuccRightSucc {} `trans` inner.eq,
notLam = inner.notLam}
_ | Right no = GotLams {names = [], body = s, eq = Refl, notLam = no}

133
src/Quox/Syntax/Term/Subst.idr Normal file
View file

@ -0,0 +1,133 @@
module Quox.Syntax.Term.Subst
import Quox.Syntax.Term.Base
export FromVar (Elim d) where fromVar = B
export FromVar (Term d) where fromVar = E . fromVar
||| does the minimal reasonable work:
||| - deletes the closure around a free name since it doesn't do anything
||| - deletes an identity substitution
||| - composes (lazily) with an existing top-level closure
||| - immediately looks up a bound variable
||| - otherwise, wraps in a new closure
export
CanSubst (Elim d) (Elim d) where
F x // _ = F x
B i // th = th !! i
CloE e ph // th = assert_total CloE e $ ph . th
e // th = case force th of
Shift SZ => e
th => CloE e th
||| 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 closure
||| - goes inside `E` in case it is a simple variable or something
||| - otherwise, wraps in a new closure
export
CanSubst (Elim d) (Term d) where
TYPE l // _ = TYPE l
E e // th = E $ e // th
CloT s ph // th = CloT s $ ph . th
s // th = case force th of
Shift SZ => s
th => CloT s th
export
CanSubst (Elim d) (ScopeTerm d) where
TUsed body // th = TUsed $ body // push th
TUnused body // th = TUnused $ body // th
export CanSubst Var (Term d) where s // th = s // map (B {d}) th
export CanSubst Var (Elim d) where e // th = e // map (B {d}) th
export CanSubst Var (ScopeTerm d) where s // th = s // map (B {d}) th
infixl 8 //., ///
mutual
namespace Term
||| applies a term substitution with a less ambiguous type
export
(//.) : Term d from -> TSubst d from to -> Term d to
t //. th = t // th
||| applies a dimension substitution with the same behaviour as `(//)`
||| above
export
(///) : Term dfrom n -> DSubst dfrom dto -> Term dto n
TYPE l /// _ = TYPE l
E e /// th = E $ e /// th
DCloT s ph /// th = DCloT s $ ph . th
s /// Shift SZ = s
s /// th = DCloT s th
||| applies a term and dimension substitution
public export %inline
subs : Term dfrom from -> DSubst dfrom dto -> TSubst dto from to ->
Term dto to
subs s th ph = s /// th // ph
namespace Elim
||| applies a term substitution with a less ambiguous type
export
(//.) : Elim d from -> TSubst d from to -> Elim d to
e //. th = e // th
||| applies a dimension substitution with the same behaviour as `(//)`
||| above
export
(///) : Elim dfrom n -> DSubst dfrom dto -> Elim dto n
F x /// _ = F x
B i /// _ = B i
DCloE e ph /// th = DCloE e $ ph . th
e /// Shift SZ = e
e /// th = DCloE e th
||| applies a term and dimension substitution
public export %inline
subs : Elim dfrom from -> DSubst dfrom dto -> TSubst dto from to ->
Elim dto to
subs e th ph = e /// th // ph
namespace ScopeTerm
||| applies a term substitution with a less ambiguous type
export
(//.) : ScopeTerm d from -> TSubst d from to -> ScopeTerm d to
body //. th = body // th
||| applies a dimension substitution with the same behaviour as `(//)`
||| above
export
(///) : ScopeTerm dfrom n -> DSubst dfrom dto -> ScopeTerm dto n
TUsed body /// th = TUsed $ body /// th
TUnused body /// th = TUnused $ body /// th
||| applies a term and dimension substitution
public export %inline
subs : ScopeTerm dfrom from -> DSubst dfrom dto -> TSubst dto from to ->
ScopeTerm dto to
subs body th ph = body /// th // ph
export CanShift (Term d) where s // by = s //. Shift by
export CanShift (Elim d) where e // by = e //. Shift by
export CanShift (ScopeTerm d) where s // by = s //. Shift by
export %inline
comp' : DSubst dfrom dto -> TSubst dfrom from mid -> TSubst dto mid to ->
TSubst dto from to
comp' th ps ph = map (/// th) ps . ph
export
fromDScopeTerm : DScopeTerm d n -> Term (S d) n
fromDScopeTerm (DUsed body) = body
fromDScopeTerm (DUnused body) = body /// shift 1
export
fromScopeTerm : ScopeTerm d n -> Term d (S n)
fromScopeTerm (TUsed body) = body
fromScopeTerm (TUnused body) = body //. shift 1

142
src/Quox/Typechecker.idr Normal file
View file

@ -0,0 +1,142 @@
module Quox.Typechecker
import public Quox.Syntax
import public Quox.Typing
import Quox.Error
%default total
private covering %inline
expectTYPE : MonadThrow Typing.Error m => Term d n -> m Universe
expectTYPE s =
case (whnfT s).fst of
TYPE l => pure l
_ => throw $ ExpectedTYPE s
private covering %inline
expectPi : MonadThrow Typing.Error m => Term d n ->
m (Qty, Qty, Term d n, ScopeTerm d n)
expectPi ty =
case (whnfT ty).fst of
Pi qtm qty _ arg res => pure (qtm, qty, arg, res)
_ => throw $ ExpectedPi ty
private %inline
expectEqualQ : MonadThrow Equal.Error m =>
(expect, actual : Qty) -> m ()
expectEqualQ pi rh = unless (pi == rh) $ throw $ ClashQ pi rh
private %inline
popQ : MonadThrow Equal.Error m => Qty -> QOutput (S n) -> m (QOutput n)
popQ pi (qctx :< rh) = expectEqualQ pi rh $> qctx
private %inline
tail : TyContext d (S n) -> TyContext d n
tail = {tctx $= tail, qctx $= tail}
private %inline
weakI : InferResult d n -> InferResult d (S n)
weakI = {type $= weakT, tmout $= (:< zero), tyout $= (:< zero)}
private
lookupBound : {n : Nat} -> Var n -> TyContext d n -> InferResult d n
lookupBound VZ (MkTyContext {tctx = _ :< ty, qctx = _ :< tyout, _}) =
InfRes {type = weakT ty, tmout = zero :< one, tyout = tyout :< zero}
lookupBound (VS i) ctx =
weakI $ lookupBound i (tail ctx)
mutual
-- [todo] it seems like the options here for dealing with substitutions are
-- to either push them or parametrise the whole typechecker over ambient
-- substitutions. both of them seem like the same amount of work for the
-- computer but pushing is less work for the me
export covering %inline
check : MonadThrows [Typing.Error, Equal.Error] m => {d, n : Nat} ->
(ctx : TyContext d n) -> (subj : Term d n) -> (ty : Term d n) ->
m (CheckResult n)
check ctx subj ty = check' ctx (pushSubstsT subj) ty
export covering %inline
infer : MonadThrows [Typing.Error, Equal.Error] m => {d, n : Nat} ->
(ctx : TyContext d n) -> (subj : Elim d n) ->
m (InferResult d n)
infer ctx subj = infer' ctx (pushSubstsE subj)
export covering
check' : MonadThrows [Typing.Error, Equal.Error] m => {d, n : Nat} ->
(ctx : TyContext d n) ->
(subj : NotCloTerm d n) -> (ty : Term d n) ->
m (CheckResult n)
check' ctx (Element (TYPE l) _) ty = do
l' <- expectTYPE ty
unless (l < l') $ throw $ BadUniverse l l'
pure $ ChkRes {tmout = zero, tyout = zero}
-- [todo] factor this stuff out
check' ctx (Element (Pi qtm qty x arg (TUsed res)) _) ty = do
l <- expectTYPE ty
argty <- check ctx arg (TYPE l)
resty <- check (extendTy arg argty.tmout ctx) res (TYPE l)
res'tmout <- popQ qty resty.tmout
pure $ ChkRes {tmout = argty.tmout + res'tmout, tyout = zero}
check' ctx (Element (Pi qtm qty x arg (TUnused res)) _) ty = do
ignore $ expectTYPE ty
argty <- check ctx arg ty
resty <- check ctx res ty
expectEqualQ qty zero
pure $ ChkRes {tmout = argty.tmout + resty.tmout, tyout = zero}
check' ctx (Element (Lam x body) _) ty = do
(qtm, qty, arg, res) <- expectPi ty
-- [todo] do this properly?
let body = fromScopeTerm body; res = fromScopeTerm res
argres <- check ctx arg (TYPE UAny)
let ctx' = extendTy arg argres.tmout ctx
bodyres <- check ctx' body res
tmout <- popQ qtm bodyres.tmout
tyout <- popQ qty bodyres.tyout
pure $ ChkRes {tmout, tyout = argres.tmout + tyout}
check' ctx (Element (E e) _) ty = do
infres <- infer ctx e
tyres <- check ctx ty (TYPE UAny)
infres.type `subT` ty
pure $ ChkRes {tmout = infres.tmout, tyout = tyres.tmout}
export covering
infer' : MonadThrows [Typing.Error, Equal.Error] m => {d, n : Nat} ->
(ctx : TyContext d n) -> (subj : NotCloElim d n) ->
m (InferResult d n)
infer' ctx (Element (F x) _) =
case lookup x ctx.globals of
Just g => pure $ InfRes {type = g.type, tmout = zero, tyout = zero}
Nothing => throw $ NotInScope x
infer' ctx (Element (B i) _) = pure $ lookupBound i ctx
infer' ctx (Element (fun :@ arg) _) = do
funres <- infer ctx fun
(qtm, qty, argty, resty) <- expectPi funres.type
let resty = fromScopeTerm resty
argres <- check ctx arg argty
let ctx' = extendTy argty argres.tyout ctx
resres <- check ctx' resty (TYPE UAny)
res'tyout <- popQ qty resres.tmout
let type = resty //. (arg :# argty ::: id)
pure $ InfRes {type,
tmout = funres.tmout + qtm * argres.tmout,
tyout = res'tyout + qty * argres.tmout}
infer' ctx (Element (tm :# ty) _) = do
ignore $ check ctx ty (TYPE UAny)
res <- check ctx tm ty
pure $ InfRes {type = ty, tmout = res.tmout, tyout = res.tyout}

23
src/Quox/Typing.idr
View file

@ -2,9 +2,10 @@ module Quox.Typing
import public Quox.Syntax import public Quox.Syntax
import public Quox.Context import public Quox.Context
import public Quox.Equal
import Data.Nat import Data.Nat
import Data.SortedMap import public Data.SortedMap
import Control.Monad.Reader import Control.Monad.Reader
import Control.Monad.State import Control.Monad.State
@ -83,3 +84,23 @@ namespace QOutput
export export
zero : {n : Nat} -> QOutput n zero : {n : Nat} -> QOutput n
zero = pure Zero zero = pure Zero
public export
record CheckResult n where
constructor ChkRes
tmout, tyout : QOutput n
public export
record InferResult d n where
constructor InfRes
type : Term d n
tmout, tyout : QOutput n
public export
data Error
= NotInScope Name
| ExpectedTYPE (Term d n)
| ExpectedPi (Term d n)
| BadUniverse Universe Universe