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

some syntax stuff

Browse source
This commit is contained in:
rhiannon morris 2021-07-20 22:05:19 +02:00
parent aff0748d82
commit e1c22b664c
12 changed files with 1278 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
quox.ipkg
View file

@ -9,4 +9,4 @@ executable = quox
main = Quox
sourcedir = "src"
depends = base
depends = base, contrib

19
src/Quox.idr
View file

@ -1,4 +1,21 @@
module Quox
import public Quox.Syntax.Term
import public Quox.Pretty
import Data.Nat
import Data.Vect
export
tm : Term 1 2
tm =
(Pi Zero One "a" (BVT 0) (E (F "F" :@@ [BVT 0, FT "w"]))
`DCloT` (DOne ::: id))
`CloT` (F "y" ::: TYPE (U 1) :# TYPE (U 2) ::: id)
main : IO Unit
main = putStrLn ":qtuwu:"
main = do
prettyTerm tm
prettyTerm $ pushSubstsT tm
putStrLn ":qtuwu:"

98
src/Quox/Ctx.idr Normal file
View file

@ -0,0 +1,98 @@
module Quox.Ctx
import Data.Nat
import Data.Fin
import Data.SnocList
import Data.DPair
%default total
public export
data Ctx : Nat -> (Nat -> Type) -> Type where
Lin : Ctx 0 f
(:<) : Ctx n f -> f n -> Ctx (S n) f
%name Ctx ctx
public export
0 Ctx' : Nat -> Type -> Type
Ctx' n a = Ctx n (\_ => a)
public export
toSList : Ctx n f -> SnocList (Exists f)
toSList [<] = [<]
toSList (ctx :< x) = toSList ctx :< Evidence _ x
public export
toSList' : Ctx' n a -> SnocList a
toSList' ctx = map (.snd) $ toSList ctx
public export
fromSList' : (xs : SnocList a) -> Ctx' (length xs) a
fromSList' [<] = [<]
fromSList' (sx :< x) = fromSList' sx :< x
public export
0 Weaken : (Nat -> Type) -> Type
Weaken f = forall n. (by : Nat) -> (1 x : f n) -> f (by + n)
public export
interface Weak f where weakN : Weaken f
public export
weak : Weak f => (1 x : f n) -> f (S n)
weak = weakN 1
public export
lookBy : Weaken f -> Ctx n f -> (1 _ : Fin n) -> f n
lookBy w = go 0 where
go : forall n. (by : Nat) -> Ctx n f -> (1 _ : Fin n) -> f (by + n)
go by (ctx :< x) (FZ {k}) =
rewrite sym $ plusSuccRightSucc by k in w (S by) x
go by (ctx :< x) (FS {k} i) =
rewrite sym $ plusSuccRightSucc by k in go (S by) ctx i
public export
look : Weak f => Ctx n f -> (1 _ : Fin n) -> f n
look = lookBy weakN
infixl 9 !!
public export
(!!) : Ctx' n a -> (1 _ : Fin n) -> a
(!!) = lookBy (\_, x => x)
public export
map : (forall n. f n -> g n) -> (1 _ : Ctx n f) -> Ctx n g
map f [<] = [<]
map f (ctx :< x) = map f ctx :< f x
public export
(forall n. Eq (f n)) => Eq (Ctx n f) where
[<] == [<] = True
(ctx1 :< x) == (ctx2 :< y) = ctx1 == ctx2 && x == y
public export
(forall n. Ord (f n)) => Ord (Ctx n f) where
compare [<] [<] = EQ
compare (ctx1 :< x) (ctx2 :< y) = compare ctx1 ctx2 <+> compare x y
||| like `Exists` but only shows the second part
private
data ShowWrapper : (Nat -> Type) -> Type where
SW : f n -> ShowWrapper f
private
(forall n. Show (f n)) => Show (ShowWrapper f) where
showPrec d (SW x) = showPrec d x
export
(forall n. Show (f n)) => Show (Ctx n f) where
show = show . map (\x => SW {f} x.snd) . toSList

52
src/Quox/Name.idr Normal file
View file

@ -0,0 +1,52 @@
module Quox.Name
import public Data.SnocList
%default total
public export
data BaseName =
UN String -- user-given name
private 0 BRepr : Type
BRepr = String
private %inline brepr : BaseName -> BRepr
brepr (UN x) = x
export Eq BaseName where (==) = (==) `on` brepr
export Ord BaseName where compare = compare `on` brepr
export
baseStr : BaseName -> String
baseStr (UN x) = x
export
FromString BaseName where
fromString = UN
public export
record Name where
constructor MakeName
mods : SnocList String
base : BaseName
private 0 Repr : Type
Repr = (SnocList String, BRepr)
private %inline repr : Name -> Repr
repr x = (x.mods, brepr x.base)
export Eq Name where (==) = (==) `on` repr
export Ord Name where compare = compare `on` repr
export
FromString Name where
fromString x = MakeName [<] (fromString x)
export
toDots : Name -> String
toDots x = fastConcat $ cast $ map (<+> ".") x.mods :< baseStr x.base

200
src/Quox/Pretty.idr Normal file
View file

@ -0,0 +1,200 @@
module Quox.Pretty
import Quox.Name
import public Text.PrettyPrint.Prettyprinter.Doc
import Text.PrettyPrint.Prettyprinter.Render.String
import Text.PrettyPrint.Prettyprinter.Render.Terminal
import public Data.String
import Data.DPair
import public Control.Monad.Identity
import public Control.Monad.Reader
%default total
public export
data HL
= Delim
| TVar
| TVarErr
| Dim
| DVar
| DVarErr
| Qty
| Free
| Syntax
private 0 HLRepr : Type
HLRepr = Nat
private %inline hlRepr : HL -> Nat
hlRepr Delim = 0
hlRepr TVar = 1
hlRepr TVarErr = 2
hlRepr Dim = 3
hlRepr DVar = 4
hlRepr DVarErr = 5
hlRepr Qty = 6
hlRepr Free = 7
hlRepr Syntax = 8
export Eq HL where (==) = (==) `on` hlRepr
export Ord HL where compare = compare `on` hlRepr
public export
data PPrec
= Outer
| Ann -- right of "::"
| AnnL -- left of "::"
-- ...
| App -- term/dimension application
| SApp -- substitution application
| Arg
private 0 PrecRepr : Type
PrecRepr = Nat
private %inline precRepr : PPrec -> PrecRepr
precRepr Outer = 0
precRepr Ann = 1
precRepr AnnL = 2
-- ...
precRepr App = 98
precRepr SApp = 99
precRepr Arg = 100
export Eq PPrec where (==) = (==) `on` precRepr
export Ord PPrec where compare = compare `on` precRepr
export %inline
hl : HL -> Doc HL -> Doc HL
hl = annotate
export %inline
hl' : HL -> Doc HL -> Doc HL
hl' h = hl h . unAnnotate
export %inline
hlF : Functor f => HL -> f (Doc HL) -> f (Doc HL)
hlF = map . hl
export %inline
hlF' : Functor f => HL -> f (Doc HL) -> f (Doc HL)
hlF' = map . hl'
export
parens : Doc HL -> Doc HL
parens doc = hl Delim "(" <+> doc <+> hl Delim ")"
export
parensIf : Bool -> Doc HL -> Doc HL
parensIf True = parens
parensIf False = id
public export
record PrettyEnv where
constructor MakePrettyEnv
||| names of bound dimension variables
dnames : List Name
||| names of bound term variables
tnames : List Name
||| use non-ascii characters for syntax
unicode : Bool
||| surrounding precedence level
prec : PPrec
public export
0 M : Type -> Type
M = Reader PrettyEnv
export
ifUnicode : (uni, asc : Lazy a) -> M a
ifUnicode uni asc = if unicode !ask then [|uni|] else [|asc|]
export
parensIfM : PPrec -> Doc HL -> M (Doc HL)
parensIfM d doc = pure $ parensIf (prec !ask > d) doc
export
withPrec : PPrec -> M a -> M a
withPrec d = local {prec := d}
public export data BinderSort = T | D
export
under : BinderSort -> Name -> M a -> M a
under s x = local $
{prec := Outer} .
(case s of T => {tnames $= (x ::)}; D => {dnames $= (x ::)})
public export
interface PrettyHL a where
prettyM : a -> M (Doc HL)
public export %inline
pretty0M : PrettyHL a => a -> M (Doc HL)
pretty0M = local {prec := Outer} . prettyM
public export %inline
pretty0 : PrettyHL a => {default True unicode : Bool} -> a -> Doc HL
pretty0 x {unicode} =
let env = MakePrettyEnv {dnames = [], tnames = [], unicode, prec = Outer} in
runReader env $ prettyM x
export
(forall a. PrettyHL (f a)) => PrettyHL (Exists f) where
prettyM x = prettyM x.snd
export
PrettyHL a => PrettyHL (Subset a b) where
prettyM x = prettyM x.fst
export PrettyHL BaseName where prettyM = pure . pretty . baseStr
export PrettyHL Name where prettyM = pure . pretty . toDots
export
prettyStr : PrettyHL a => {default True unicode : Bool} -> a -> String
prettyStr {unicode} =
renderString .
layoutSmart (MkLayoutOptions (AvailablePerLine 80 0.8)) .
pretty0 {unicode}
export
termHL : HL -> AnsiStyle
termHL Delim = color BrightBlack
termHL TVar = color BrightYellow
termHL TVarErr = color BrightYellow <+> underline
termHL Dim = color BrightGreen <+> bold
termHL DVar = color BrightGreen
termHL DVarErr = color BrightGreen <+> underline
termHL Qty = color BrightMagenta <+> bold
termHL Free = color BrightWhite
termHL Syntax = color BrightBlue
export
prettyTerm : {default True color, unicode : Bool} -> PrettyHL a => a -> IO Unit
prettyTerm x {color, unicode} =
let reann = if color then map termHL else unAnnotate in
Terminal.putDoc $ reann $ pretty0 x {unicode}
infixr 6 <//>
export %inline
(<//>) : Doc a -> Doc a -> Doc a
a <//> b = sep [a, b]
infixr 6 </>
export %inline
(</>) : Doc a -> Doc a -> Doc a
a </> b = cat [a, b]

50
src/Quox/Syntax/Dim.idr Normal file
View file

@ -0,0 +1,50 @@
module Quox.Syntax.Dim
import Quox.Syntax.Var
import Quox.Syntax.Subst
import Quox.Pretty
%default total
public export
data Dim : Nat -> Type where
DZero, DOne : Dim d
DBound : Var d -> Dim d
%name Dim.Dim p, q
private DRepr : Type
DRepr = Nat
private %inline drepr : Dim n -> DRepr
drepr d = case d of DZero => 0; DOne => 1; DBound i => 2 + i.nat
export Eq (Dim n) where (==) = (==) `on` drepr
export Ord (Dim n) where compare = compare `on` drepr
export
PrettyHL (Dim n) where
prettyM DZero = hl Dim <$> ifUnicode "𝟬" "0"
prettyM DOne = hl Dim <$> ifUnicode "𝟭" "1"
prettyM (DBound i) = prettyVar DVar DVarErr (!ask).dnames i
public export
0 DSubst : Nat -> Nat -> Type
DSubst = Subst Dim
export %inline
prettyDSubst : DSubst from to -> Pretty.M (Doc HL)
prettyDSubst th =
prettySubstM prettyM (dnames !ask) DVar
!(ifUnicode "⟨" "<") !(ifUnicode "⟩" ">") th
export FromVar Dim where fromVar = DBound
export
CanSubst Dim Dim where
DZero // _ = DZero
DOne // _ = DOne
DBound i // th = th !! i

54
src/Quox/Syntax/Qty.idr Normal file
View file

@ -0,0 +1,54 @@
module Quox.Syntax.Qty
import Quox.Pretty
import Data.Fin
public export
data Qty = Zero | One | Many
%name Qty.Qty pi, rh
private Repr : Type
Repr = Fin 3
private %inline repr : Qty -> Repr
repr pi = case pi of Zero => 0; One => 1; Many => 2
export Eq Qty where (==) = (==) `on` repr
export Ord Qty where compare = compare `on` repr
export
PrettyHL Qty where
prettyM pi = hl Qty <$>
case pi of
Zero => ifUnicode "𝟬" "0"
One => ifUnicode "𝟭" "1"
Many => ifUnicode "𝛚" "*"
export %inline
prettyQtyBinds : List Qty -> M (Doc HL)
prettyQtyBinds =
map (align . sep) .
traverse (\pi => [|pretty0M pi <++> pure (hl Delim "|")|])
public export
(+) : Qty -> Qty -> Qty
Zero + rh = rh
pi + Zero = pi
_ + _ = Many
public export
(*) : Qty -> Qty -> Qty
Zero * _ = Zero
_ * Zero = Zero
One * rh = rh
pi * One = pi
Many * Many = Many
infix 6 <=.
public export
(<=.) : Qty -> Qty -> Bool
pi <=. rh = rh == Many || pi == rh

174
src/Quox/Syntax/Shift.idr Normal file
View file

@ -0,0 +1,174 @@
module Quox.Syntax.Shift
import public Quox.Syntax.Var
import Quox.Pretty
import Data.Nat
import Data.So
%default total
||| represents the difference between a smaller scope and a larger one.
public export
data Shift : (0 from, to : Nat) -> Type where
SZ : Shift from from
SS : Shift from to -> Shift from (S to)
%name Shift by, bz
%builtin Natural Shift
public export
(.nat) : Shift from to -> Nat
(SZ).nat = Z
(SS by).nat = S by.nat
%transform "Shift.(.nat)" Shift.(.nat) = believe_me
public export Cast (Shift from to) Nat where cast = (.nat)
export Eq (Shift from to) where (==) = (==) `on` (.nat)
export Ord (Shift from to) where compare = compare `on` (.nat)
||| shift equivalence, ignoring indices
public export
data Eqv : Shift from1 to1 -> Shift from2 to2 -> Type where
EqSZ : SZ `Eqv` SZ
EqSS : by `Eqv` bz -> SS by `Eqv` SS bz
%name Eqv e
||| two equivalent shifts are equal if they have the same indices.
export
0 fromEqv : by `Eqv` bz -> by = bz
fromEqv EqSZ = Refl
fromEqv (EqSS e) = cong SS $ fromEqv e
||| two equal shifts are equivalent.
export
0 toEqv : by = bz -> by `Eqv` bz
toEqv Refl {by = SZ} = EqSZ
toEqv Refl {by = (SS by)} = EqSS $ toEqv Refl {by}
public export
0 shiftDiff : (by : Shift from to) -> to = by.nat + from
shiftDiff SZ = Refl
shiftDiff (SS by) = cong S $ shiftDiff by
export
0 shiftVarLT : (by : Shift from to) -> (i : Var from) ->
by.nat + i.nat `LT` to
shiftVarLT by i =
rewrite plusSuccRightSucc by.nat i.nat in
transitive {rel=LTE}
(plusLteMonotoneLeft by.nat (S i.nat) from (toNatLT i))
(replace {p=(\n => LTE n to)} (shiftDiff by) $ reflexive {rel=LTE})
public export
fromNat : (by : Nat) -> Shift from (by + from)
fromNat Z = SZ
fromNat (S by) = SS $ fromNat by
%transform "Shift.fromNat" Shift.fromNat x = believe_me x
export
0 fromToNat : (by : Shift from to) -> by `Eqv` fromNat by.nat {from}
fromToNat SZ = EqSZ
fromToNat (SS by) = EqSS $ fromToNat by
export
0 toFromNat : (from, by : Nat) -> by = (fromNat by {from}).nat
toFromNat from 0 = Refl
toFromNat from (S k) = cong S $ toFromNat from k
export
0 toNatInj' : (by : Shift from1 to1) -> (bz : Shift from2 to2) ->
by.nat = bz.nat -> by `Eqv` bz
toNatInj' SZ SZ prf = EqSZ
toNatInj' (SS by) (SS bz) prf = EqSS $ toNatInj' by bz $ succInjective _ _ prf
toNatInj' (SS by) SZ Refl impossible
export
0 toNatInj : (by, bz : Shift from to) -> by.nat = bz.nat -> by = bz
toNatInj by bz e = fromEqv $ toNatInj' by bz e
public export
shift : Shift from to -> Var from -> Var to
shift SZ i = i
shift (SS by) i = VS $ shift by i
private
shiftViaNat' : (by : Shift from to) -> (i : Var from) ->
(0 p : by.nat + i.nat `LT` to) -> Var to
shiftViaNat' by i p = V $ by.nat + i.nat
private
shiftViaNat : Shift from to -> Var from -> Var to
shiftViaNat by i = shiftViaNat' by i $ shiftVarLT by i
private
0 shiftViaNatCorrect : (by : Shift from to) -> (i : Var from) ->
(0 p : by.nat + i.nat `LT` to) ->
shiftViaNat' by i p = shift by i
shiftViaNatCorrect SZ i (LTESucc p) = fromToNat i _
shiftViaNatCorrect (SS by) i (LTESucc p) = cong VS $ shiftViaNatCorrect by i p
%transform "Shift.shift" shift = shiftViaNat
infixl 9 .
public export
(.) : Shift from mid -> Shift mid to -> Shift from to
by . SZ = by
by . SS bz = SS $ by . bz
private
0 compNatProof : (by : Shift from mid) -> (bz : Shift mid to) ->
to = by.nat + bz.nat + from
compNatProof by bz =
shiftDiff bz >>>
cong (bz.nat +) (shiftDiff by) >>>
plusAssociative bz.nat by.nat from >>>
cong (+ from) (plusCommutative bz.nat by.nat)
where
infixr 0 >>>
0 (>>>) : a = b -> b = c -> a = c
x >>> y = trans x y
private
compViaNat' : (by : Shift from mid) -> (bz : Shift mid to) ->
Shift from (by.nat + bz.nat + from)
compViaNat' by bz = fromNat $ by.nat + bz.nat
private
compViaNat : (by : Shift from mid) -> (bz : Shift mid to) -> Shift from to
compViaNat by bz = rewrite compNatProof by bz in compViaNat' by bz
private
0 compViaNatCorrect : (by : Shift from mid) -> (bz : Shift mid to) ->
by . bz `Eqv` compViaNat' by bz
compViaNatCorrect by SZ =
rewrite plusZeroRightNeutral by.nat in fromToNat by
compViaNatCorrect by (SS bz) =
rewrite sym $ plusSuccRightSucc by.nat bz.nat in
EqSS $ compViaNatCorrect by bz
%transform "Shift.(.)" Shift.(.) = compViaNat
||| `prettyShift bnd unicode prec by` pretty-prints the shift `by`, with the
||| following arguments:
|||
||| * `by : Shift from to`
||| * `bnd : HL` is the highlight used for bound variables of this kind
||| * `unicode : Bool` is whether to use unicode characters in the output
||| * `prec : PPrec` is the surrounding precedence level
export
prettyShift : (bnd : HL) -> Shift from to -> Pretty.M (Doc HL)
prettyShift bnd by =
parensIfM Outer $ hsep $
[hl bnd !(ifUnicode "𝑖" "i"), hl Delim !(ifUnicode "≔" ":="),
hl bnd $ !(ifUnicode "𝑖+" "i+") <+> pretty by.nat]
||| prints using the `TVar` highlight for variables
export PrettyHL (Shift from to) where prettyM = prettyShift TVar

121
src/Quox/Syntax/Subst.idr Normal file
View file

@ -0,0 +1,121 @@
module Quox.Syntax.Subst
import Quox.Syntax.Shift
import Quox.Syntax.Var
import Quox.Name
import Quox.Pretty
import Data.List
%default total
infixr 5 :::
public export
data Subst : (Nat -> Type) -> Nat -> Nat -> Type where
Shift : Shift from to -> Subst env from to
(:::) : (t : Lazy (env to)) -> Subst env from to -> Subst env (S from) to
%name Subst th, ph, ps
private
Repr : (Nat -> Type) -> Nat -> Type
Repr f to = (List (f to), Nat)
private
repr : Subst f from to -> Repr f to
repr (Shift by) = ([], by.nat)
repr (t ::: th) = let (ts, i) = repr th in (t::ts, i)
export Eq (f to) => Eq (Subst f from to) where (==) = (==) `on` repr
export Ord (f to) => Ord (Subst f from to) where compare = compare `on` repr
infixl 8 //
public export
interface FromVar env => CanSubst env term where
(//) : term from -> Subst env from to -> term to
public export
0 CanSubst1 : (Nat -> Type) -> Type
CanSubst1 f = CanSubst f f
infixl 8 !!
public export
(!!) : FromVar term => Subst term from to -> Var from -> term to
(Shift by) !! i = fromVar $ shift by i
(t ::: th) !! VZ = t
(t ::: th) !! (VS i) = th !! i
public export
CanSubst Var Var where
i // Shift by = shift by i
VZ // (t ::: th) = t
VS i // (t ::: th) = i // th
public export %inline
shift : (by : Nat) -> Subst env from (by + from)
shift by = Shift $ fromNat by
infixl 9 .
public export
(.) : CanSubst1 f => Subst f from mid -> Subst f mid to -> Subst f from to
Shift SZ . ph = ph
Shift (SS by) . Shift bz = Shift $ SS by . bz
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
public export
map : (f to -> g to) -> Subst f from to -> Subst g from to
map f (Shift by) = Shift by
map f (t ::: th) = f t ::: map f th
public export %inline
push : CanSubst1 f => Subst f from to -> Subst f (S from) (S to)
push th = fromVar VZ ::: (th . shift 1)
||| `prettySubst pr bnd op cl unicode th` pretty-prints the substitution `th`,
||| with the following arguments:
|||
||| * `th : Subst f from to`
||| * `pr : (unicode : Bool) -> f to -> m (Doc HL)` prints a single element
||| * `names : List Name` is a list of known bound var names
||| * `bnd : HL` is the highlight to use for bound variables being subsituted
||| * `op, cl : Doc HL` are the opening and closing brackets
||| * `unicode : Bool` is whether to use unicode characters in the output
||| (also passed into `pr`)
export
prettySubstM : (pr : f to -> Pretty.M (Doc HL)) ->
(names : List Name) ->
(bnd : HL) -> (op, cl : Doc HL) ->
Subst f from to -> Pretty.M (Doc HL)
prettySubstM pr names bnd op cl th =
encloseSep (hl Delim op) (hl Delim cl) (hl Delim "; ") <$>
withPrec Outer (go 0 th)
where
go1 : Nat -> f to -> Pretty.M (Doc HL)
go1 i t = pure $ hang 2 $ sep
[hsep [!(prettyVar' bnd bnd names i),
hl Delim !(ifUnicode "≔" ":=")],
!(pr t)]
go : forall from. Nat -> Subst f from to -> Pretty.M (List (Doc HL))
go _ (Shift SZ) = pure []
go _ (Shift by) = [|pure (prettyShift bnd by)|]
go i (t ::: th) = [|go1 i t :: go (S i) th|]
||| prints with [square brackets] and the `TVar` highlight for variables
export
PrettyHL (f to) => PrettyHL (Subst f from to) where
prettyM th = prettySubstM prettyM (tnames !ask) TVar "[" "]" th

340
src/Quox/Syntax/Term.idr Normal file
View file

@ -0,0 +1,340 @@
module Quox.Syntax.Term
import public Quox.Ctx
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 Quox.Pretty
import public Data.DPair
import Data.List
import Data.Maybe
import Data.Nat
import public Data.So
import Data.String
%default total
infixl 8 :#
infixl 9 :@
mutual
public export
0 TSubst : Nat -> Nat -> Nat -> Type
TSubst d = Subst (Elim d)
||| 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 : (qty, qtm : Qty) -> (x : Name) ->
(a : Term d n) -> (b : Term d (S n)) -> Term d n
||| function term
Lam : (x : Name) -> (t : Term d (S n)) -> Term d n
||| elimination
E : (e : Elim d n) -> Term d n
||| term closure/suspended substitution
CloT : (s : Term d from) -> (th : Lazy (TSubst d from to)) -> Term d to
||| dimension closure/suspended substitution
DCloT : (s : 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
(:@) : (f : Elim d n) -> (s : Term d n) -> Elim d n
||| type-annotated term
(:#) : (s, a : Term d n) -> Elim d n
||| term closure/suspended substitution
CloE : (e : Elim d from) -> (th : Lazy (TSubst d from to)) -> Elim d to
||| dimension closure/suspended substitution
DCloE : (e : Elim dfrom n) -> (th : Lazy (DSubst dfrom dto)) -> Elim dto n
%name Term s, t, r
%name Elim e, f
||| 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) -> {auto 0 p : LT i n} -> Elim d n
BV i = B $ V i
||| same as `BV` but as a term
public export %inline
BVT : (i : Nat) -> {auto 0 p : LT i n} -> Term d n
BVT i = E $ BV i
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
private
getArgs' : Elim d n -> List (Term d n) -> (Elim d n, List (Term d n))
getArgs' (f :@ s) args = getArgs' f (s :: args)
getArgs' f args = (f, args)
||| 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 -> (Elim d n, List (Term d n))
getArgs e = getArgs' e []
private %inline typeD : Doc HL
typeD = hl Syntax "Type"
private %inline arrowD : Pretty.M (Doc HL)
arrowD = hlF Syntax $ ifUnicode "→" "->"
private %inline lamD : Pretty.M (Doc HL)
lamD = hlF Syntax $ ifUnicode "λ" "fun"
private %inline annD : Pretty.M (Doc HL)
annD = hlF Syntax $ ifUnicode "⦂" "::"
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 qty qtm x s t) =
parensIfM Outer $ hang 2 $
!(prettyBinder [qty, qtm] 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 (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
prettyTSubst : TSubst d from to -> Pretty.M (Doc HL)
prettyTSubst s = prettySubstM prettyM (tnames !ask) TVar "[" "]" s
export covering
prettyBinder : List Qty -> Name -> Term d n -> Pretty.M (Doc HL)
prettyBinder pis x a =
pure $ parens $ hang 2 $
!(prettyQtyBinds pis) <//>
hsep [hl TVar !(prettyM x), 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 = CloE e $ assert_total $ ph . th
e // Shift SZ = e
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 // Shift SZ = s
s // th = CloT s th
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
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
||| true if an elimination has a closure or dimension closure at the top level
public export %inline
isCloE : Elim d n -> Bool
isCloE (CloE _ _) = True
isCloE (DCloE _ _) = True
isCloE _ = False
||| 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
isCloT : Term d n -> Bool
isCloT (CloT _ _) = True
isCloT (DCloT _ _) = True
isCloT (E e) = isCloE e
isCloT _ = False
||| an elimination which is not a top level closure
public export 0 NotCloElim : Nat -> Nat -> Type
NotCloElim d n = Subset (Elim d n) $ So . not . isCloE
||| a term which is not a top level closure
public export 0 NotCloTerm : Nat -> Nat -> Type
NotCloTerm d n = Subset (Term d n) $ So . not . isCloT
mutual
export
pushSubstsT : Term d n -> NotCloTerm d n
pushSubstsT s = pushSubstsT' id id s
export
pushSubstsE : Elim d n -> NotCloElim d n
pushSubstsE e = pushSubstsE' id id e
private
pushSubstsT' : DSubst dfrom dto -> TSubst dto from to ->
Term dfrom from -> NotCloTerm dto to
pushSubstsT' th ph (TYPE l) =
Element (TYPE l) Oh
pushSubstsT' th ph (Pi qty qtm x a b) =
Element (Pi qty qtm x (subs a th ph) (subs b th (push ph))) Oh
pushSubstsT' th ph (Lam x t) =
Element (Lam x $ subs t th $ push ph) Oh
pushSubstsT' th ph (E e) =
case pushSubstsE' th ph e of Element e' prf => Element (E e') prf
pushSubstsT' th ph (CloT s ps) =
pushSubstsT' th (comp' th ps ph) s
pushSubstsT' th ph (DCloT s ps) =
pushSubstsT' (ps . th) ph s
private
pushSubstsE' : DSubst dfrom dto -> TSubst dto from to ->
Elim dfrom from -> NotCloElim dto to
pushSubstsE' th ph (F x) =
Element (F x) Oh
pushSubstsE' th ph (B i) =
assert_total pushSubstsE $ ph !! i
pushSubstsE' th ph (f :@ s) =
Element (subs f th ph :@ subs s th ph) Oh
pushSubstsE' th ph (s :# a) =
Element (subs s th ph :# subs a th ph) Oh
pushSubstsE' th ph (CloE e ps) =
pushSubstsE' th (comp' th ps ph) e
pushSubstsE' th ph (DCloE e ps) =
pushSubstsE' (ps . th) ph e
||| `(λx. t ⦂ (x: A) → B) s >>> (t ⦂ B)[x ≔ (s ⦂ A)`
export
betaLam1 : Alternative f => Elim d n -> f (Elim d n)
betaLam1 ((Lam {t, _} :# Pi {a, b, _}) :@ s) =
pure $ (t :# b) // (s :# a ::: id)
betaLam1 _ = empty
||| `(e ⦂ A) >>> e` [if `e` is an elim]
export
upsilon1 : Alternative f => Elim d n -> f (Elim d n)
upsilon1 (E e :# _) = pure e
upsilon1 _ = empty
public export
step : Alternative f => Elim d n -> f (Elim d n)
step e = betaLam1 e <|> upsilon1 e
public export
step' : Elim d n -> Elim d n
step' e = fromMaybe e $ step e

28
src/Quox/Syntax/Universe.idr Normal file
View file

@ -0,0 +1,28 @@
module Quox.Syntax.Universe
import Quox.Pretty
import Data.Fin
%default total
||| `UAny` doesn't show up in programs, but when checking something is
||| just some type (e.g. in a signature) it's checked against `Star UAny`
public export
data Universe = U Nat | UAny
%name Universe l
private Repr : Type
Repr = (Fin 2, Nat)
private %inline repr : Universe -> Repr
repr u = case u of U i => (0, i); UAny => (1, 0)
export Eq Universe where (==) = (==) `on` repr
export Ord Universe where compare = compare `on` repr
export
PrettyHL Universe where
prettyM UAny = pure $ hl Delim "_"
prettyM (U l) = pure $ hl Free $ pretty l

142
src/Quox/Syntax/Var.idr Normal file
View file

@ -0,0 +1,142 @@
module Quox.Syntax.Var
import Quox.Name
import Data.Nat
import Data.Maybe
import Data.List
import Quox.Pretty
%default total
public export
data Var : Nat -> Type where
VZ : Var (S n)
VS : Var n -> Var (S n)
%name Var i, j
%builtin Natural Var
public export
(.nat) : Var n -> Nat
(VZ).nat = 0
(VS i).nat = S i.nat
%transform "Var.(.nat)" Var.(.nat) i = believe_me i
public export Cast (Var n) Nat where cast n = n.nat
export Eq (Var n) where i == j = i.nat == j.nat
export Ord (Var n) where compare i j = compare i.nat j.nat
export Show (Var n) where showPrec d i = showCon d "V" $ showArg i.nat
private
prettyIndex : Nat -> Pretty.M (Doc a)
prettyIndex i =
ifUnicode (pretty $ pack $ map sup $ unpack $ show i) (":" <+> pretty i)
where
sup : Char -> Char
sup c = case c of
'0' => '⁰'; '1' => '¹'; '2' => '²'; '3' => '³'; '4' => '⁴'
'5' => '⁵'; '6' => '⁶'; '7' => '⁷'; '8' => '⁸'; '9' => '⁹'; _ => c
||| `prettyVar hlok hlerr names i` pretty prints the de Bruijn index `i`.
|||
||| If it is within the bounds of `names`, then it uses the name at that index,
||| highlighted as `hlok`. Otherwise it is just printed as a number highlighted
||| as `hlerr`.
export
prettyVar' : HL -> HL -> List Name -> Nat -> Pretty.M (Doc HL)
prettyVar' hlok hlerr names i =
case inBounds i names of
Yes _ => hlF' hlok [|prettyM (index i names) <+> prettyIndex i|]
No _ => pure $ hl hlerr $ pretty i
export %inline
prettyVar : HL -> HL -> List Name -> Var n -> Pretty.M (Doc HL)
prettyVar hlok hlerr names i = prettyVar' hlok hlerr names i.nat
public export
fromNatWith : (i : Nat) -> (0 p : i `LT` n) -> Var n
fromNatWith Z (LTESucc _) = VZ
fromNatWith (S i) (LTESucc p) = VS $ fromNatWith i p
%transform "Var.fromNatWith" fromNatWith i p = believe_me i
public export %inline
V : (i : Nat) -> {auto 0 p : i `LT` n} -> Var n
V i {p} = fromNatWith i p
public export %inline
tryFromNat : Alternative f => (n : Nat) -> Nat -> f (Var n)
tryFromNat n i =
case i `isLT` n of
Yes p => pure $ fromNatWith i p
No _ => empty
export
0 toNatLT : (i : Var n) -> i.nat `LT` n
toNatLT VZ = LTESucc LTEZero
toNatLT (VS i) = LTESucc $ toNatLT i
export
0 toNatInj : {i, j : Var n} -> i.nat = j.nat -> i = j
toNatInj {i = VZ} {j = VZ} Refl = Refl
toNatInj {i = VZ} {j = (VS i)} Refl impossible
toNatInj {i = (VS i)} {j = VZ} Refl impossible
toNatInj {i = (VS i)} {j = (VS j)} prf =
cong VS $ toNatInj $ succInjective _ _ prf
export
0 fromToNat : (i : Var n) -> (p : i.nat `LT` n) -> fromNatWith i.nat p = i
fromToNat VZ (LTESucc p) = Refl
fromToNat (VS i) (LTESucc p) = rewrite fromToNat i p in Refl
export
0 toFromNat : (i : Nat) -> (p : i `LT` n) -> (fromNatWith i p).nat = i
toFromNat 0 (LTESucc x) = Refl
toFromNat (S k) (LTESucc x) = cong S $ toFromNat k x
public export
(.int) : Var n -> Integer
i.int = natToInteger i.nat
%builtin NaturalToInteger Var.(.int)
public export Cast (Var n) Integer where cast i = i.int
-- not using %transform like other things because weakSpec requires the proof
-- to be relevant. but since only `LTESucc` is ever possible that seems
-- to be a bug?
export
weak : (0 p : m `LTE` n) -> Var m -> Var n
weak p i = fromNatWith i.nat $ transitive (toNatLT i) p {rel=LTE}
public export
0 weakSpec : m `LTE` n -> Var m -> Var n
weakSpec LTEZero _ impossible
weakSpec (LTESucc p) VZ = VZ
weakSpec (LTESucc p) (VS i) = VS $ weakSpec p i
export
0 weakSpecCorrect : (p : m `LTE` n) -> (i : Var m) -> (weakSpec p i).nat = i.nat
weakSpecCorrect LTEZero _ impossible
weakSpecCorrect (LTESucc x) VZ = Refl
weakSpecCorrect (LTESucc x) (VS i) = cong S $ weakSpecCorrect x i
export
0 weakCorrect : (p : m `LTE` n) -> (i : Var m) -> (weak p i).nat = i.nat
weakCorrect LTEZero _ impossible
weakCorrect (LTESucc p) VZ = Refl
weakCorrect (LTESucc p) (VS i) = cong S $ weakCorrect p i
export
0 weakIsSpec : (p : m `LTE` n) -> (i : Var m) -> weak p i = weakSpec p i
weakIsSpec p i = toNatInj $ trans (weakCorrect p i) (sym $ weakSpecCorrect p i)
public export
interface FromVar f where %inline fromVar : Var n -> f n
public export FromVar Var where fromVar = id