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

448 lines
13 KiB
Idris
Raw Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

module Quox.Syntax.Term.Base
import public Quox.Var
import public Quox.Scoped
import public Quox.Syntax.Shift
import public Quox.Syntax.Subst
import public Quox.Syntax.Qty
import public Quox.Syntax.Dim
import public Quox.Syntax.Term.TyConKind
import public Quox.Name
import public Quox.Loc
import public Quox.Context
import Quox.Pretty
import public Data.DPair
import Data.List
import Data.Maybe
import Data.Nat
import public Data.So
import Data.String
import public Data.SortedMap
import public Data.SortedMap.Dependent
import public Data.SortedSet
import Derive.Prelude
%default total
%language ElabReflection
%hide TT.Name
public export
TermLike : Type
TermLike = Nat -> Nat -> Type
public export
TSubstLike : Type
TSubstLike = Nat -> Nat -> Nat -> Type
public export
Universe : Type
Universe = Nat
public export
TagVal : Type
TagVal = String
infixl 8 :#
infixl 9 :@, :%
mutual
public export
TSubst : TSubstLike
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) -> (loc : Loc) -> Term d n
||| function type
Pi : (qty : Qty) -> (arg : Term d n) ->
(res : ScopeTerm d n) -> (loc : Loc) -> Term d n
||| function term
Lam : (body : ScopeTerm d n) -> (loc : Loc) -> Term d n
||| pair type
Sig : (fst : Term d n) -> (snd : ScopeTerm d n) -> (loc : Loc) -> Term d n
||| pair value
Pair : (fst, snd : Term d n) -> (loc : Loc) -> Term d n
||| enumeration type
Enum : (cases : SortedSet TagVal) -> (loc : Loc) -> Term d n
||| enumeration value
Tag : (tag : TagVal) -> (loc : Loc) -> Term d n
||| equality type
Eq : (ty : DScopeTerm d n) -> (l, r : Term d n) -> (loc : Loc) -> Term d n
||| equality term
DLam : (body : DScopeTerm d n) -> (loc : Loc) -> Term d n
||| natural numbers (temporary until 𝐖 gets added)
Nat : (loc : Loc) -> Term d n
-- [todo] can these be elims?
Zero : (loc : Loc) -> Term d n
Succ : (p : Term d n) -> (loc : Loc) -> Term 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
||| elimination
E : (e : Elim d n) -> Term d n
||| term closure/suspended substitution
CloT : WithSubst (Term d) (Elim d) n -> Term d n
||| dimension closure/suspended substitution
DCloT : WithSubst (\d => Term d n) Dim d -> Term 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
||| 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
||| bound variable
B : (i : Var n) -> (loc : Loc) -> Elim d n
||| term application
App : (fun : Elim d n) -> (arg : Term d n) -> (loc : Loc) -> Elim d n
||| pair destruction
|||
||| `CasePair 𝜋 𝑒 ([𝑟], 𝐴) ([𝑥, 𝑦], 𝑡)` is
||| `𝐜𝐚𝐬𝐞 𝜋 · 𝑒 𝐫𝐞𝐭𝐮𝐫𝐧 𝑟𝐴 𝐨𝐟 { (𝑥, 𝑦) ⇒ 𝑡 }`
CasePair : (qty : Qty) -> (pair : Elim d n) ->
(ret : ScopeTerm d n) ->
(body : ScopeTermN 2 d n) ->
(loc : Loc) ->
Elim d n
||| first element of a pair. only works in non-linear contexts.
Fst : (pair : Elim d n) -> (loc : Loc) -> Elim d n
||| second element of a pair. only works in non-linear contexts.
Snd : (pair : Elim d n) -> (loc : Loc) -> Elim d n
||| enum matching
CaseEnum : (qty : Qty) -> (tag : Elim d n) ->
(ret : ScopeTerm d n) ->
(arms : CaseEnumArms d n) ->
(loc : Loc) ->
Elim 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) ->
(loc : Loc) ->
Elim d n
||| unboxing
CaseBox : (qty : Qty) -> (box : Elim d n) ->
(ret : ScopeTerm d n) ->
(body : ScopeTerm d n) ->
(loc : Loc) ->
Elim d n
||| dim application
DApp : (fun : Elim d n) -> (arg : Dim d) -> (loc : Loc) -> Elim d n
||| type-annotated term
Ann : (tm, ty : Term d n) -> (loc : Loc) -> Elim 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
||| "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
||| 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) ->
(loc : Loc) ->
Elim d n
||| term closure/suspended substitution
CloE : WithSubst (Elim d) (Elim d) n -> Elim d n
||| dimension closure/suspended substitution
DCloE : WithSubst (\d => Elim d n) Dim d -> Elim d n
%name Elim e, f
public export
CaseEnumArms : TermLike
CaseEnumArms d n = SortedMap TagVal (Term d n)
public export
TypeCaseArms : TermLike
TypeCaseArms d n = SortedDMap TyConKind (\k => TypeCaseArmBody k d n)
public export
TypeCaseArm : TermLike
TypeCaseArm d n = (k ** TypeCaseArmBody k d n)
public export
TypeCaseArmBody : TyConKind -> TermLike
TypeCaseArmBody k = ScopeTermN (arity k)
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
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
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
||| scope which ignores all its binders
public export %inline
SN : {s : Nat} -> f n -> Scoped s f n
SN = S (replicate s $ BN Unused noLoc) . N
||| scope which uses its binders
public export %inline
SY : BContext s -> f (s + n) -> Scoped s f n
SY ns = S ns . Y
public export %inline
name : Scoped 1 f n -> BindName
name (S [< x] _) = x
public export %inline
(.name) : Scoped 1 f n -> BindName
s.name = name s
||| 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, 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, body, loc} = Lam {body = SY [< x] body, loc}
public export %inline
LamN : (body : Term d n) -> (loc : Loc) -> Term 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, 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, 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, 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, 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, body, loc} = DLam {body = SY [< i] body, loc}
public export %inline
DLamN : (body : Term d n) -> (loc : Loc) -> Term 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, 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 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 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 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 loc = E $ BV i loc
public export
makeNat : Nat -> Loc -> Term d n
makeNat 0 loc = Zero loc
makeNat (S k) loc = Succ (makeNat k loc) loc
public export %inline
enum : List TagVal -> Loc -> Term 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 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) ->
(loc : Loc) ->
{default (Nat loc) def : Term d n} ->
Elim d n
typeCase1Y ty ret k ns body loc = typeCase ty ret [(k ** SY ns body)] def loc
export
Located (Elim d n) where
(F _ _ loc).loc = loc
(B _ loc).loc = loc
(App _ _ loc).loc = loc
(CasePair _ _ _ _ loc).loc = loc
(Fst _ loc).loc = loc
(Snd _ loc).loc = loc
(CaseEnum _ _ _ _ loc).loc = loc
(CaseNat _ _ _ _ _ _ loc).loc = loc
(CaseBox _ _ _ _ loc).loc = loc
(DApp _ _ loc).loc = loc
(Ann _ _ loc).loc = loc
(Coe _ _ _ _ loc).loc = loc
(Comp _ _ _ _ _ _ _ loc).loc = loc
(TypeCase _ _ _ _ loc).loc = loc
(CloE (Sub e _)).loc = e.loc
(DCloE (Sub e _)).loc = e.loc
export
Located (Term d n) where
(TYPE _ loc).loc = loc
(Pi _ _ _ loc).loc = loc
(Lam _ loc).loc = loc
(Sig _ _ loc).loc = loc
(Pair _ _ loc).loc = loc
(Enum _ loc).loc = loc
(Tag _ loc).loc = loc
(Eq _ _ _ loc).loc = loc
(DLam _ loc).loc = loc
(Nat loc).loc = loc
(Zero loc).loc = loc
(Succ _ loc).loc = loc
(BOX _ _ loc).loc = loc
(Box _ loc).loc = loc
(E e).loc = e.loc
(CloT (Sub t _)).loc = t.loc
(DCloT (Sub t _)).loc = t.loc
export
Located1 f => Located (ScopedBody s f n) where
(Y t).loc = t.loc
(N t).loc = t.loc
export
Located1 f => Located (Scoped s f n) where
t.loc = t.body.loc
export
Relocatable (Elim 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
setLoc loc (CasePair qty pair ret body _) =
CasePair qty pair ret body loc
setLoc loc (Fst pair _) = Fst pair loc
setLoc loc (Snd pair _) = Fst pair loc
setLoc loc (CaseEnum qty tag ret arms _) =
CaseEnum qty tag ret arms loc
setLoc loc (CaseNat qty qtyIH nat ret zero succ _) =
CaseNat qty qtyIH nat ret zero succ loc
setLoc loc (CaseBox qty box ret body _) =
CaseBox qty box ret body loc
setLoc loc (DApp fun arg _) =
DApp fun arg loc
setLoc loc (Ann tm ty _) =
Ann tm ty loc
setLoc loc (Coe ty p q val _) =
Coe ty p q val loc
setLoc loc (Comp ty p q val r zero one _) =
Comp ty p q val r zero one loc
setLoc loc (TypeCase ty ret arms def _) =
TypeCase ty ret arms def loc
setLoc loc (CloE (Sub term subst)) =
CloE $ Sub (setLoc loc term) subst
setLoc loc (DCloE (Sub term subst)) =
DCloE $ Sub (setLoc loc term) subst
export
Relocatable (Term d n) where
setLoc loc (TYPE l _) = TYPE l loc
setLoc loc (Pi qty arg res _) = Pi qty arg res loc
setLoc loc (Lam body _) = Lam body loc
setLoc loc (Sig fst snd _) = Sig fst snd loc
setLoc loc (Pair fst snd _) = Pair fst snd loc
setLoc loc (Enum cases _) = Enum cases loc
setLoc loc (Tag tag _) = Tag tag loc
setLoc loc (Eq ty l r _) = Eq ty l r loc
setLoc loc (DLam body _) = DLam body loc
setLoc loc (Nat _) = Nat loc
setLoc loc (Zero _) = Zero loc
setLoc loc (Succ p _) = Succ p loc
setLoc loc (BOX qty ty _) = BOX qty ty loc
setLoc loc (Box val _) = Box val loc
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
export
Relocatable1 f => Relocatable (ScopedBody s f n) where
setLoc loc (Y body) = Y $ setLoc loc body
setLoc loc (N body) = N $ setLoc loc body
export
Relocatable1 f => Relocatable (Scoped s f n) where
setLoc loc (S names body) = S (setLoc loc <$> names) (setLoc loc body)