switch syntax to codb
This commit is contained in:
parent
92870fe716
commit
9e702dd03d
1 changed files with 272 additions and 347 deletions
|
|
@ -1,5 +1,6 @@
|
||||||
module Quox.Syntax.Term.Base
|
module Quox.Syntax.Term.Base
|
||||||
|
|
||||||
|
import public Quox.Thin
|
||||||
import public Quox.Syntax.Var
|
import public Quox.Syntax.Var
|
||||||
import public Quox.Syntax.Shift
|
import public Quox.Syntax.Shift
|
||||||
import public Quox.Syntax.Subst
|
import public Quox.Syntax.Subst
|
||||||
|
|
@ -18,9 +19,6 @@ import Data.Maybe
|
||||||
import Data.Nat
|
import Data.Nat
|
||||||
import public Data.So
|
import public Data.So
|
||||||
import Data.String
|
import Data.String
|
||||||
import public Data.SortedMap
|
|
||||||
import public Data.SortedMap.Dependent
|
|
||||||
import public Data.SortedSet
|
|
||||||
import Derive.Prelude
|
import Derive.Prelude
|
||||||
|
|
||||||
%default total
|
%default total
|
||||||
|
|
@ -46,345 +44,301 @@ TagVal : Type
|
||||||
TagVal = String
|
TagVal = String
|
||||||
|
|
||||||
|
|
||||||
|
||| type-checkable terms, which consists of types and constructor forms.
|
||||||
|
|||
|
||||||
|
||| first argument `d` is dimension scope size; second `n` is term scope size
|
||||||
public export
|
public export
|
||||||
data ScopedBody : Nat -> (Nat -> Type) -> Nat -> Type where
|
data Term : (d, n : Nat) -> Type
|
||||||
Y : (body : f (s + n)) -> ScopedBody s f n
|
%name Term s, t, r
|
||||||
N : (body : f n) -> ScopedBody s f n
|
|
||||||
%name ScopedBody body
|
|
||||||
|
|
||||||
export %inline %hint
|
||| inferrable terms, which consists of elimination forms like application and
|
||||||
EqScopedBody : (forall n. Eq (f n)) => Eq (ScopedBody s f n)
|
||| `case` (as well as other terms with an annotation)
|
||||||
EqScopedBody = deriveEq
|
|||
|
||||||
|
||| first argument `d` is dimension scope size; second `n` is term scope size
|
||||||
export %inline %hint
|
|
||||||
ShowScopedBody : (forall n. Show (f n)) => Show (ScopedBody s f n)
|
|
||||||
ShowScopedBody = deriveShow
|
|
||||||
|
|
||||||
||| a scoped term with names
|
|
||||||
public export
|
public export
|
||||||
record Scoped (s : Nat) (f : Nat -> Type) (n : Nat) where
|
data Elim : (d, n : Nat) -> Type
|
||||||
constructor S
|
%name Elim e, f
|
||||||
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 :#
|
public export
|
||||||
infixl 9 :@, :%
|
ScopeTermN : Nat -> TermLike
|
||||||
mutual
|
ScopeTermN s d n = ScopedN s (\n => Term d n) n
|
||||||
public export
|
|
||||||
TSubst : TSubstLike
|
|
||||||
TSubst d = Subst $ \n => Elim d n
|
|
||||||
|
|
||||||
||| first argument `d` is dimension scope size;
|
public export
|
||||||
||| second `n` is term scope size
|
DScopeTermN : Nat -> TermLike
|
||||||
public export
|
DScopeTermN s d n = ScopedN s (\d => Term d n) d
|
||||||
data Term : (d, n : Nat) -> Type where
|
|
||||||
||| type of types
|
|
||||||
TYPE : (l : Universe) -> (loc : Loc) -> Term d n
|
|
||||||
|
|
||||||
||| function type
|
public export
|
||||||
Pi : (qty : Qty) -> (arg : Term d n) ->
|
ScopeTerm : TermLike
|
||||||
(res : ScopeTerm d n) -> (loc : Loc) -> Term d n
|
ScopeTerm = ScopeTermN 1
|
||||||
||| function term
|
|
||||||
Lam : (body : ScopeTerm d n) -> (loc : Loc) -> Term d n
|
|
||||||
|
|
||||||
||| pair type
|
public export
|
||||||
Sig : (fst : Term d n) -> (snd : ScopeTerm d n) -> (loc : Loc) -> Term d n
|
DScopeTerm : TermLike
|
||||||
||| pair value
|
DScopeTerm = DScopeTermN 1
|
||||||
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
|
|
||||||
|
|
||||||
||| 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
|
public export
|
||||||
ScopeTermN, DScopeTermN : Nat -> TermLike
|
TermT : TermLike
|
||||||
ScopeTermN s d n = Scoped s (Term d) n
|
TermT = Thinned2 (\d, n => Term d n)
|
||||||
DScopeTermN s d n = Scoped s (\d => Term d n) d
|
|
||||||
|
|
||||||
public export
|
public export
|
||||||
ScopeTerm, DScopeTerm : TermLike
|
ElimT : TermLike
|
||||||
ScopeTerm = ScopeTermN 1
|
ElimT = Thinned2 (\d, n => Elim d n)
|
||||||
DScopeTerm = DScopeTermN 1
|
|
||||||
|
|
||||||
mutual
|
|
||||||
export %hint
|
|
||||||
EqTerm : Eq (Term d n)
|
|
||||||
EqTerm = assert_total {a = Eq (Term d n)} deriveEq
|
|
||||||
|
|
||||||
export %hint
|
public export
|
||||||
EqElim : Eq (Elim d n)
|
DimArg : TermLike
|
||||||
EqElim = assert_total {a = Eq (Elim d n)} deriveEq
|
DimArg d n = Dim d
|
||||||
|
|
||||||
mutual
|
|
||||||
export %hint
|
|
||||||
ShowTerm : Show (Term d n)
|
|
||||||
ShowTerm = assert_total {a = Show (Term d n)} deriveShow
|
|
||||||
|
|
||||||
export %hint
|
data Term where
|
||||||
ShowElim : Show (Elim d n)
|
||| type of types
|
||||||
ShowElim = assert_total {a = Show (Elim d n)} deriveShow
|
TYPE : (l : Universe) -> (loc : Loc) -> Term 0 0
|
||||||
|
|
||||||
||| scope which ignores all its binders
|
||| function type
|
||||||
public export %inline
|
Pi : Qty -> Subterms [Term, ScopeTerm] d n -> Loc -> Term d n
|
||||||
SN : {s : Nat} -> f n -> Scoped s f n
|
||| function value
|
||||||
SN = S (replicate s $ BN Unused noLoc) . N
|
Lam : ScopeTerm d n -> Loc -> Term d n
|
||||||
|
|
||||||
||| scope which uses its binders
|
||| pair type
|
||||||
public export %inline
|
Sig : Subterms [Term, ScopeTerm] d n -> Loc -> Term d n
|
||||||
SY : BContext s -> f (s + n) -> Scoped s f n
|
||| pair value
|
||||||
SY ns = S ns . Y
|
Pair : Subterms [Term, Term] d n -> Loc -> Term d n
|
||||||
|
|
||||||
public export %inline
|
||| enum type
|
||||||
name : Scoped 1 f n -> BindName
|
Enum : List TagVal -> Loc -> Term 0 0
|
||||||
name (S [< x] _) = x
|
||| enum value
|
||||||
|
Tag : TagVal -> Loc -> Term 0 0
|
||||||
|
|
||||||
public export %inline
|
||| equality type
|
||||||
(.name) : Scoped 1 f n -> BindName
|
Eq : Subterms [DScopeTerm, Term, Term] d n -> Loc -> Term d n
|
||||||
s.name = name s
|
||| equality value
|
||||||
|
DLam : DScopeTerm d n -> Loc -> Term d n
|
||||||
|
|
||||||
||| more convenient Pi
|
||| natural numbers (temporary until 𝐖 gets added)
|
||||||
public export %inline
|
Nat : Loc -> Term 0 0
|
||||||
PiY : (qty : Qty) -> (x : BindName) ->
|
Zero : Loc -> Term 0 0
|
||||||
(arg : Term d n) -> (res : Term d (S n)) -> (loc : Loc) -> Term d n
|
Succ : Term d n -> Loc -> Term 0 0
|
||||||
PiY {qty, x, arg, res, loc} = Pi {qty, arg, res = SY [< x] res, loc}
|
|
||||||
|
|
||||||
||| more convenient Lam
|
||| package a value with a quantity
|
||||||
public export %inline
|
||| e.g. a value of [ω. A], when unpacked, can be used ω times,
|
||||||
LamY : (x : BindName) -> (body : Term d (S n)) -> (loc : Loc) -> Term d n
|
||| even if the box itself is linear
|
||||||
LamY {x, body, loc} = Lam {body = SY [< x] body, loc}
|
BOX : Qty -> Term d n -> Loc -> Term d n
|
||||||
|
Box : Term d n -> Loc -> Term d n
|
||||||
|
|
||||||
public export %inline
|
E : Elim d n -> Term d n
|
||||||
LamN : (body : Term d n) -> (loc : Loc) -> Term d n
|
|
||||||
LamN {body, loc} = Lam {body = SN body, loc}
|
|
||||||
|
|
||||||
||| non dependent function type
|
||| term closure/suspended substitution
|
||||||
public export %inline
|
CloT : WithSubst (Term d) (Elim d) n -> Term d n
|
||||||
Arr : (qty : Qty) -> (arg, res : Term d n) -> (loc : Loc) -> Term d n
|
||| dimension closure/suspended substitution
|
||||||
Arr {qty, arg, res, loc} = Pi {qty, arg, res = SN res, loc}
|
DCloT : WithSubst (\d => Term d n) Dim d -> Term d n
|
||||||
|
|
||||||
||| more convenient Sig
|
||| first argument `d` is dimension scope size, second `n` is term scope size
|
||||||
public export %inline
|
public export
|
||||||
SigY : (x : BindName) -> (fst : Term d n) ->
|
data Elim where
|
||||||
(snd : Term d (S n)) -> (loc : Loc) -> Term d n
|
||| free variable, possibly with a displacement (see @crude, or @mugen for a
|
||||||
SigY {x, fst, snd, loc} = Sig {fst, snd = SY [< x] snd, loc}
|
||| more abstract and formalised take)
|
||||||
|
|||
|
||||||
|
||| e.g. if f : ★₀ → ★₁, then f¹ : ★₁ → ★₂
|
||||||
|
F : Name -> Universe -> Loc -> Elim 0 0
|
||||||
|
||| bound variable
|
||||||
|
B : Loc -> Elim 0 1
|
||||||
|
|
||||||
||| non dependent pair type
|
||| term application
|
||||||
public export %inline
|
App : Subterms [Elim, Term] d n -> Loc -> Elim d n
|
||||||
And : (fst, snd : Term d n) -> (loc : Loc) -> Term d n
|
|
||||||
And {fst, snd, loc} = Sig {fst, snd = SN snd, loc}
|
|
||||||
|
|
||||||
||| more convenient Eq
|
||| pair match
|
||||||
public export %inline
|
||| - the subterms are, in order: [head, return type, body]
|
||||||
EqY : (i : BindName) -> (ty : Term (S d) n) ->
|
||| - the quantity is that of the head, and since pairs only have one
|
||||||
(l, r : Term d n) -> (loc : Loc) -> Term d n
|
||| constructor, can be 0
|
||||||
EqY {i, ty, l, r, loc} = Eq {ty = SY [< i] ty, l, r, loc}
|
CasePair : Qty -> Subterms [Elim, ScopeTerm, ScopeTermN 2] d n ->
|
||||||
|
Loc -> Elim d n
|
||||||
|
|
||||||
||| more convenient DLam
|
||| enum match
|
||||||
public export %inline
|
CaseEnum : Qty -> (arms : List TagVal) ->
|
||||||
DLamY : (i : BindName) -> (body : Term (S d) n) -> (loc : Loc) -> Term d n
|
Subterms (Elim :: ScopeTerm :: (Term <$ arms)) d n ->
|
||||||
DLamY {i, body, loc} = DLam {body = SY [< i] body, loc}
|
Loc -> Elim d n
|
||||||
|
|
||||||
public export %inline
|
||| nat match
|
||||||
DLamN : (body : Term d n) -> (loc : Loc) -> Term d n
|
CaseNat : Qty -> Qty ->
|
||||||
DLamN {body, loc} = DLam {body = SN body, loc}
|
Subterms [Elim, ScopeTerm, Term, ScopeTermN 2] d n ->
|
||||||
|
Loc -> Elim d n
|
||||||
|
|
||||||
|
||| box match
|
||||||
|
CaseBox : Qty -> Subterms [Elim, ScopeTerm, ScopeTerm] d n -> Loc -> Elim d n
|
||||||
|
|
||||||
|
||| dim application
|
||||||
|
DApp : Subterms [Elim, DimArg] d n -> Loc -> Elim d n
|
||||||
|
|
||||||
|
||| type-annotated term
|
||||||
|
Ann : Subterms [Term, Term] d n -> Loc -> Elim d n
|
||||||
|
|
||||||
|
||| coerce a value along a type equality, or show its coherence
|
||||||
|
||| [@xtt; §2.1.1]
|
||||||
|
Coe : Subterms [DScopeTerm, DimArg, DimArg, Term] d n ->
|
||||||
|
Loc -> Elim d n
|
||||||
|
|
||||||
|
||| "generalised composition" [@xtt; §2.1.2]
|
||||||
|
Comp : Subterms [Term, DimArg, DimArg, Term,
|
||||||
|
DimArg, DScopeTerm, DScopeTerm] d n ->
|
||||||
|
Loc -> Elim d n
|
||||||
|
|
||||||
|
||| match on types. needed for b.s. of coercions [@xtt; §2.2]
|
||||||
|
TypeCase : Subterms [Elim, Term, -- head, type
|
||||||
|
Term, -- ★
|
||||||
|
ScopeTermN 2, -- pi
|
||||||
|
ScopeTermN 2, -- sig
|
||||||
|
Term, -- enum
|
||||||
|
ScopeTermN 5, -- eq
|
||||||
|
Term, -- nat
|
||||||
|
ScopeTerm -- box
|
||||||
|
] d n -> 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
|
||||||
|
|
||||||
|
|
||||||
|
-- this kills the idris ☹
|
||||||
|
-- export %hint
|
||||||
|
-- EqTerm : Eq (Term d n)
|
||||||
|
|
||||||
|
-- export %hint
|
||||||
|
-- EqElim : Eq (Elim d n)
|
||||||
|
|
||||||
|
-- EqTerm = deriveEq
|
||||||
|
-- EqElim = 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}
|
||||||
|
|
||||||
||| 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
|
||| same as `F` but as a term
|
||||||
public export %inline
|
public export %inline
|
||||||
FT : Name -> Universe -> Loc -> Term d n
|
FT : Name -> Universe -> Loc -> Term 0 0
|
||||||
FT x u loc = E $ F x u loc
|
FT x u loc = E $ F x u loc
|
||||||
|
|
||||||
||| abbreviation for a bound variable like `BV 4` instead of
|
||| abbreviation for a bound variable like `BV 4` instead of
|
||||||
||| `B (VS (VS (VS (VS VZ))))`
|
||| `B (VS (VS (VS (VS VZ))))`
|
||||||
public export %inline
|
public export %inline
|
||||||
BV : (i : Nat) -> (0 _ : LT i n) => (loc : Loc) -> Elim d n
|
BV : (i : Fin n) -> (loc : Loc) -> ElimT d n
|
||||||
BV i loc = B (V i) loc
|
BV i loc = Th2 zero (one' i) $ B loc
|
||||||
|
|
||||||
||| same as `BV` but as a term
|
||| same as `BV` but as a term
|
||||||
public export %inline
|
public export %inline
|
||||||
BVT : (i : Nat) -> (0 _ : LT i n) => (loc : Loc) -> Term d n
|
BVT : (i : Fin n) -> (loc : Loc) -> TermT d n
|
||||||
BVT i loc = E $ BV i loc
|
BVT i loc = Th2 zero (one' i) $ E $ B loc
|
||||||
|
|
||||||
public export
|
public export
|
||||||
makeNat : Nat -> Loc -> Term d n
|
makeNat : Nat -> Loc -> Term 0 0
|
||||||
makeNat 0 loc = Zero loc
|
makeNat 0 loc = Zero loc
|
||||||
makeNat (S k) loc = Succ (makeNat k loc) 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
|
export
|
||||||
Located (Elim d n) where
|
Located (Elim d n) where
|
||||||
(F _ _ loc).loc = loc
|
(F _ _ loc).loc = loc
|
||||||
(B _ loc).loc = loc
|
(B loc).loc = loc
|
||||||
(App _ _ loc).loc = loc
|
(App _ loc).loc = loc
|
||||||
(CasePair _ _ _ _ loc).loc = loc
|
(CasePair _ _ loc).loc = loc
|
||||||
(CaseEnum _ _ _ _ loc).loc = loc
|
(CaseEnum _ _ _ loc).loc = loc
|
||||||
(CaseNat _ _ _ _ _ _ loc).loc = loc
|
(CaseNat _ _ _ loc).loc = loc
|
||||||
(CaseBox _ _ _ _ loc).loc = loc
|
(CaseBox _ _ loc).loc = loc
|
||||||
(DApp _ _ loc).loc = loc
|
(DApp _ loc).loc = loc
|
||||||
(Ann _ _ loc).loc = loc
|
(Ann _ loc).loc = loc
|
||||||
(Coe _ _ _ _ loc).loc = loc
|
(Coe _ loc).loc = loc
|
||||||
(Comp _ _ _ _ _ _ _ loc).loc = loc
|
(Comp _ loc).loc = loc
|
||||||
(TypeCase _ _ _ _ loc).loc = loc
|
(TypeCase _ loc).loc = loc
|
||||||
(CloE (Sub e _)).loc = e.loc
|
(CloE (Sub e _)).loc = e.loc
|
||||||
(DCloE (Sub e _)).loc = e.loc
|
(DCloE (Sub e _)).loc = e.loc
|
||||||
|
|
||||||
export
|
export
|
||||||
Located (Term d n) where
|
Located (Term d n) where
|
||||||
(TYPE _ loc).loc = loc
|
(TYPE _ loc).loc = loc
|
||||||
(Pi _ _ _ loc).loc = loc
|
(Pi _ _ loc).loc = loc
|
||||||
(Lam _ loc).loc = loc
|
(Lam _ loc).loc = loc
|
||||||
(Sig _ _ loc).loc = loc
|
(Sig _ loc).loc = loc
|
||||||
(Pair _ _ loc).loc = loc
|
(Pair _ loc).loc = loc
|
||||||
(Enum _ loc).loc = loc
|
(Enum _ loc).loc = loc
|
||||||
(Tag _ loc).loc = loc
|
(Tag _ loc).loc = loc
|
||||||
(Eq _ _ _ loc).loc = loc
|
(Eq _ loc).loc = loc
|
||||||
(DLam _ loc).loc = loc
|
(DLam _ loc).loc = loc
|
||||||
(Nat loc).loc = loc
|
(Nat loc).loc = loc
|
||||||
(Zero loc).loc = loc
|
(Zero loc).loc = loc
|
||||||
|
|
@ -395,69 +349,40 @@ Located (Term d n) where
|
||||||
(CloT (Sub t _)).loc = t.loc
|
(CloT (Sub t _)).loc = t.loc
|
||||||
(DCloT (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
|
export
|
||||||
Relocatable (Elim d n) where
|
Relocatable (Elim d n) where
|
||||||
setLoc loc (F x u _) = F x u loc
|
setLoc loc (F x u _) = F x u loc
|
||||||
setLoc loc (B i _) = B i loc
|
setLoc loc (B _) = B loc
|
||||||
setLoc loc (App fun arg _) = App fun arg loc
|
setLoc loc (App ts _) = App ts loc
|
||||||
setLoc loc (CasePair qty pair ret body _) =
|
setLoc loc (CasePair qty ts _) = CasePair qty ts loc
|
||||||
CasePair qty pair ret body loc
|
setLoc loc (CaseEnum qty arms ts _) = CaseEnum qty arms ts loc
|
||||||
setLoc loc (CaseEnum qty tag ret arms _) =
|
setLoc loc (CaseNat qty qtyIH ts _) = CaseNat qty qtyIH ts loc
|
||||||
CaseEnum qty tag ret arms loc
|
setLoc loc (CaseBox qty ts _) = CaseBox qty ts loc
|
||||||
setLoc loc (CaseNat qty qtyIH nat ret zero succ _) =
|
setLoc loc (DApp ts _) = DApp ts loc
|
||||||
CaseNat qty qtyIH nat ret zero succ loc
|
setLoc loc (Ann ts _) = Ann ts loc
|
||||||
setLoc loc (CaseBox qty box ret body _) =
|
setLoc loc (Coe ts _) = Coe ts loc
|
||||||
CaseBox qty box ret body loc
|
setLoc loc (Comp ts _) = Comp ts loc
|
||||||
setLoc loc (DApp fun arg _) =
|
setLoc loc (TypeCase ts _) = TypeCase ts loc
|
||||||
DApp fun arg loc
|
setLoc loc (CloE (Sub term subst)) = CloE $ Sub (setLoc loc term) subst
|
||||||
setLoc loc (Ann tm ty _) =
|
setLoc loc (DCloE (Sub term subst)) = DCloE $ Sub (setLoc loc term) subst
|
||||||
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
|
export
|
||||||
Relocatable (Term d n) where
|
Relocatable (Term d n) where
|
||||||
setLoc loc (TYPE l _) = TYPE l loc
|
setLoc loc (TYPE l _) = TYPE l loc
|
||||||
setLoc loc (Pi qty arg res _) = Pi qty arg res loc
|
setLoc loc (Pi qty ts _) = Pi qty ts loc
|
||||||
setLoc loc (Lam body _) = Lam body loc
|
setLoc loc (Lam body _) = Lam body loc
|
||||||
setLoc loc (Sig fst snd _) = Sig fst snd loc
|
setLoc loc (Sig ts _) = Sig ts loc
|
||||||
setLoc loc (Pair fst snd _) = Pair fst snd loc
|
setLoc loc (Pair ts _) = Pair ts loc
|
||||||
setLoc loc (Enum cases _) = Enum cases loc
|
setLoc loc (Enum cases _) = Enum cases loc
|
||||||
setLoc loc (Tag tag _) = Tag tag loc
|
setLoc loc (Tag tag _) = Tag tag loc
|
||||||
setLoc loc (Eq ty l r _) = Eq ty l r loc
|
setLoc loc (Eq ts _) = Eq ts loc
|
||||||
setLoc loc (DLam body _) = DLam body loc
|
setLoc loc (DLam body _) = DLam body loc
|
||||||
setLoc loc (Nat _) = Nat loc
|
setLoc loc (Nat _) = Nat loc
|
||||||
setLoc loc (Zero _) = Zero loc
|
setLoc loc (Zero _) = Zero loc
|
||||||
setLoc loc (Succ p _) = Succ p loc
|
setLoc loc (Succ p _) = Succ p loc
|
||||||
setLoc loc (BOX qty ty _) = BOX qty ty loc
|
setLoc loc (BOX qty ty _) = BOX qty ty loc
|
||||||
setLoc loc (Box val _) = Box val loc
|
setLoc loc (Box val _) = Box val loc
|
||||||
setLoc loc (E e) = E $ setLoc loc e
|
setLoc loc (E e) = E $ setLoc loc e
|
||||||
setLoc loc (CloT (Sub term subst)) = CloT $ Sub (setLoc loc term) subst
|
setLoc loc (CloT (Sub term subst)) = CloT $ Sub (setLoc loc term) subst
|
||||||
setLoc loc (DCloT (Sub term subst)) = DCloT $ Sub (setLoc loc term) subst
|
setLoc loc (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)
|
|
||||||
|
|
|
||||||
Loading…
Reference in a new issue