module Quox.Syntax.Term.Base import public Quox.Syntax.Var 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 public export data ScopedBody : Nat -> (Nat -> Type) -> Nat -> Type where Y : (body : f (s + n)) -> ScopedBody s f n N : (body : f n) -> ScopedBody s f n %name ScopedBody body export %inline %hint EqScopedBody : (forall n. Eq (f n)) => Eq (ScopedBody s f n) EqScopedBody = deriveEq export %inline %hint ShowScopedBody : (forall n. Show (f n)) => Show (ScopedBody s f n) ShowScopedBody = deriveShow ||| a scoped term with names public export record Scoped (s : Nat) (f : Nat -> Type) (n : Nat) where constructor S names : BContext s body : ScopedBody s f n %name Scoped body export %inline (forall n. Eq (f n)) => Eq (Scoped s f n) where s == t = s.body == t.body export %inline %hint ShowScoped : (forall n. Show (f n)) => Show (Scoped s f n) ShowScoped = deriveShow 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 F : (x : Name) -> (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 ||| 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 -> (loc : Loc) -> Term d n FT x loc = E $ F x 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 (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 _) = F x 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 (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)