mirror of
https://github.com/anoma/juvix.git
synced 2024-12-24 07:57:58 +03:00
Added some syntax revision and initial version of term substitution.
This commit is contained in:
Jonathan Prieto-Cubides
parent
88bf127a75
commit
a832b67041
@ -1,6 +1,9 @@
|
||||
-- Core syntax splits terms in two categories:
|
||||
-- CheckableTerm as the ones we must check.
|
||||
-- InferableTerm as the ones we can infer.
|
||||
{-
|
||||
This module exposes the Internal syntax. A term is either checkable or
|
||||
inferable. As the name indicates, a term of type CheckableTerm is a
|
||||
term we must check. Similarly, a term of type InferableTerm, it is a
|
||||
term we can infer.
|
||||
-}
|
||||
module MiniJuvix.Syntax.Core where
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
@ -8,7 +11,7 @@ module MiniJuvix.Syntax.Core where
|
||||
open import Haskell.Prelude
|
||||
open import Agda.Builtin.Equality
|
||||
|
||||
-- Language extensions
|
||||
-- Haskell language extensions
|
||||
{-# FOREIGN AGDA2HS
|
||||
{-# LANGUAGE LambdaCase #-}
|
||||
{-# LANGUAGE FlexibleInstances #-}
|
||||
@ -24,10 +27,16 @@ data Quantity : Set where
|
||||
-- Being relevant for a term is to have non zero quantity.
|
||||
data Relevance : Set where
|
||||
Relevant : Relevance -- terms to compute.
|
||||
Irrelevant : Relevance -- terms to contemplate (for type formers).
|
||||
Irrelevant : Relevance -- terms to contemplate (for type formation).
|
||||
{-# COMPILE AGDA2HS Relevance #-}
|
||||
|
||||
relevancy : Quantity → Relevance
|
||||
relevancy Zero = Irrelevant
|
||||
relevancy One = Relevant
|
||||
relevancy Many = Relevant
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
Name : Set
|
||||
Name = String
|
||||
{-# COMPILE AGDA2HS Name #-}
|
||||
@ -37,18 +46,19 @@ BName = String
|
||||
{-# COMPILE AGDA2HS BName #-}
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
data Term : Set where
|
||||
ToCheck : Term -- terms with a type checkable.
|
||||
ToInfer : Term -- terms that which types can be inferred.
|
||||
{-# COMPILE AGDA2HS Term #-}
|
||||
|
||||
|
||||
{-
|
||||
Following [Dunfield and Krishnaswami, 2019] and the
|
||||
Pfenning principle: "If the rule is an introduction rule, make the
|
||||
principal judgement "checking", and if the rule is an elimination
|
||||
rule, make the principal judgement "synthesising." Glossary:
|
||||
{-
|
||||
Core syntax follows the pattern design for bidirectional typing
|
||||
algorithmgs in [Dunfield and Krishnaswami, 2019]. Pfenning's principle
|
||||
is one of such criterion and stated as follows.
|
||||
|
||||
1. If the rule is an introduction rule, make the principal judgement
|
||||
"checking", and
|
||||
2. if the rule is an elimination rule, make the principal judgement
|
||||
"synthesising".
|
||||
|
||||
Jargon:
|
||||
- Principal connective of a rule:
|
||||
- for an introduction rule is the connective that is being
|
||||
introduced.
|
||||
@ -66,116 +76,95 @@ data CheckableTerm : Set
|
||||
data InferableTerm : Set
|
||||
|
||||
data CheckableTerm where
|
||||
-- Universe types.
|
||||
{- Universe types.
|
||||
See the typing rule Univ⇐.
|
||||
-}
|
||||
UniverseType : CheckableTerm
|
||||
-- Dependent function types.
|
||||
-- (λ x. t) : Π[ x :ρ S ] P x
|
||||
Lam : BName → CheckableTerm → CheckableTerm
|
||||
{- Dependent function types.
|
||||
See the typing rules →F⇐ and →I⇐.
|
||||
1. (Π[ x :ρ S ] P x) : U
|
||||
2. (λ x. t) : Π[ x :ρ S ] P x
|
||||
-}
|
||||
PiType : Quantity → BName → CheckableTerm → CheckableTerm → CheckableTerm
|
||||
-- (Π[ x :ρ S ] P x) : U
|
||||
-- Dependent tensor product types.
|
||||
-- (M , N) : S ⊗ T
|
||||
TensorIntro : CheckableTerm → CheckableTerm → CheckableTerm
|
||||
-- * S ⊗ T : U
|
||||
Lam : BName → CheckableTerm → CheckableTerm
|
||||
{- Dependent tensor product types.
|
||||
See the typing rules ⊗-F-⇐, ⊗-I₀⇐, and ⊗-I₁⇐.
|
||||
1. * S ⊗ T : U
|
||||
2. (M , N) : S ⊗ T
|
||||
-}
|
||||
TensorType : Quantity → BName → CheckableTerm → CheckableTerm → CheckableTerm
|
||||
-- Unit types.
|
||||
-- ⋆ : 𝟙
|
||||
Unit : CheckableTerm
|
||||
-- 𝟙 : U
|
||||
TensorIntro : CheckableTerm → CheckableTerm → CheckableTerm
|
||||
{- Unit types.
|
||||
See the typing rule 1-F-⇐ and 1-I-⇐.
|
||||
1. 𝟙 : U
|
||||
2. ⋆ : 𝟙
|
||||
-}
|
||||
UnitType : CheckableTerm
|
||||
-- Disjoint sum types.
|
||||
Inl : CheckableTerm → CheckableTerm
|
||||
-- inl x : S + T
|
||||
Inr : CheckableTerm → CheckableTerm
|
||||
-- inr x : S + T
|
||||
Unit : CheckableTerm
|
||||
{- Disjoint sum types.
|
||||
See the typing rules
|
||||
1. S + T : U
|
||||
2. inl x : S + T
|
||||
3. inr x : S + T
|
||||
-}
|
||||
SumType : CheckableTerm → CheckableTerm → CheckableTerm
|
||||
-- S + T : U
|
||||
-- Inferrable terms are clearly checkable.
|
||||
Inl : CheckableTerm → CheckableTerm
|
||||
Inr : CheckableTerm → CheckableTerm
|
||||
-- Inferrable terms are clearly checkable, see typing rule Inf⇐.
|
||||
Inferred : InferableTerm → CheckableTerm
|
||||
|
||||
{-# COMPILE AGDA2HS CheckableTerm #-}
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Type-inferable terms (a.k.a terms that synthesise)
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
data InferableTerm where
|
||||
Ann : CheckableTerm → CheckableTerm → InferableTerm
|
||||
-- | Variables, typing rule Var⇒.
|
||||
Bound : Nat → InferableTerm
|
||||
Free : Name → InferableTerm
|
||||
-- | eliminator.
|
||||
-- | Annotations, typing rule Ann⇒.
|
||||
{- Maybe, I want to have the rules here like this:
|
||||
|
||||
OΓ ⊢ S ⇐0 𝕌 Γ ⊢ M ⇐0 𝕌
|
||||
────────────────────────────── Ann⇒
|
||||
Γ ⊢ (M : S) ⇒ S
|
||||
-}
|
||||
Ann : CheckableTerm → CheckableTerm → InferableTerm
|
||||
-- | Application (eliminator).
|
||||
App : InferableTerm → CheckableTerm → InferableTerm
|
||||
-- | Dependent Tensor product eliminator.
|
||||
-- | Dependent Tensor product eliminator. See section 2.1.3 in Atkey 2018.
|
||||
-- let z@(u, v) = M in N :^q (a ⊗ b))
|
||||
TensorTypeElim
|
||||
: Quantity -- ^ Multiplicity of the eliminated pair.
|
||||
→ BName -- ^ Name of the variable binding the pair in the type
|
||||
-- annotation of the result of elimination.
|
||||
→ BName -- ^ Name of the variable binding the first element.
|
||||
→ BName -- ^ Name of the variable binding the second element.
|
||||
→ InferableTerm -- ^ The eliminated pair.
|
||||
→ CheckableTerm -- ^ Result of the elimination.
|
||||
→ CheckableTerm -- ^ Type annotation of the result of elimination.
|
||||
: Quantity -- q is the multiplicity of the eliminated pair.
|
||||
→ BName -- z is the name of the variable binding the pair in the
|
||||
-- type annotation of the result of elimination.
|
||||
→ BName -- u is the name of the variable binding the first element.
|
||||
→ BName -- v is the name of the variable binding the second element.
|
||||
→ InferableTerm -- (u,v) is the eliminated pair.
|
||||
→ CheckableTerm -- Result of the elimination.
|
||||
→ CheckableTerm -- Type annotation of the result of elimination.
|
||||
→ InferableTerm
|
||||
-- | Sum type eliminator.
|
||||
SumTypeElim -- Case
|
||||
: Quantity -- ^ Multiplicity of the sum contents.
|
||||
→ BName -- ^ Name of the variable binding the sum in the type
|
||||
-- annotation of the result of elimination.
|
||||
→ InferableTerm -- ^ The eliminated sum.
|
||||
→ BName -- ^ Name of the variable binding the left element.
|
||||
→ CheckableTerm -- ^ Result of the elimination in case the sum contains the left
|
||||
-- element.
|
||||
→ BName -- ^ Name of the variable binding the right element.
|
||||
→ CheckableTerm -- ^ Result of the elimination in case the sum contains the right
|
||||
-- element.
|
||||
→ CheckableTerm -- ^ Type annotation of the result of the elimination.
|
||||
-- | Sum type eliminator (a.k.a. case)
|
||||
-- let (z : S + T) in (case z of {(inl u) ↦ r1; (inr v) ↦ r2} :^q T)
|
||||
SumTypeElim -- Case
|
||||
: Quantity -- Multiplicity of the sum contents.
|
||||
→ BName -- Name of the variable binding the sum in the type
|
||||
-- annotation of the result of elimination.
|
||||
→ InferableTerm -- The eliminated sum.
|
||||
→ BName -- u is the name of the variable binding the left element.
|
||||
→ CheckableTerm -- r1 is the result of the elimination in case the sum contains
|
||||
-- the left element.
|
||||
→ BName -- v is the name of the variable binding the right element.
|
||||
→ CheckableTerm -- r2 is the result of the elimination in case the sum contains
|
||||
-- the right element.
|
||||
→ CheckableTerm -- Type annotation of the result of the elimination.
|
||||
→ InferableTerm
|
||||
{-# COMPILE AGDA2HS InferableTerm #-}
|
||||
|
||||
-- | Substitution on type-synthesising terms.
|
||||
substInferableTerm
|
||||
: Nat -- ^ bound variable x (Bruijn)
|
||||
-> InferableTerm -- inferable term N
|
||||
-> InferableTerm -- inferable term M
|
||||
-> InferableTerm -- N[x := M]
|
||||
substInferableTerm v i1 i2 = Bound 0
|
||||
{-# COMPILE AGDA2HS substInferableTerm #-}
|
||||
|
||||
-- | Substitution on type-checkable terms.
|
||||
checkableSubst
|
||||
: Nat -- ^ bound variable x (Bruijn)
|
||||
-> InferableTerm -- inferable term N
|
||||
-> CheckableTerm -- checkable term M
|
||||
-> CheckableTerm -- N[x := M]
|
||||
checkableSubst v i c = Unit
|
||||
{-# COMPILE AGDA2HS checkableSubst #-}
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Type checking
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
-- type Resource = Map.Map Name Usage
|
||||
|
||||
-- mergeUsages :: (Ord k, Semiring v) => Map.Map k v -> Map.Map k v -> Map.Map k v
|
||||
|
||||
-- -- | Synthesise the type of a term and check that context has appropriate
|
||||
-- -- resources available for the term.
|
||||
-- synthesise :: (ValueEnv, Context) -> Usage -> ITerm -> Result Type
|
||||
-- synthesise = P.undefined
|
||||
|
||||
-- -- | Synthesise the type of a term.
|
||||
-- synthType :: Relevance -> ITerm -> TypeJudgment (Usage, Type)
|
||||
-- synthType = P.undefined
|
||||
|
||||
-- -- | Type-check a term.
|
||||
-- checkType :: Relevance -> CTerm -> Type -> TypeJudgment Usage
|
||||
-- checkType = P.undefined
|
||||
|
||||
-- -- | Type-check a dependent type.
|
||||
-- checkTypeDep
|
||||
-- :: Relevance -> BindingName -> CTerm -> CTerm -> CTerm -> TypeJudgment Usage
|
||||
-- checkTypeDep = P.undefined
|
||||
|
||||
-- -- | Type-check an atomic type (a.k.a. types that denote a particular
|
||||
-- -- set, e.g. 1, Z, N).
|
||||
-- checkTypeAtom :: Relevance -> CTerm -> TypeJudgment Usage
|
||||
-- checkTypeAtom = P.undefined
|
||||
|
||||
-- checkTypeErased :: CTerm -> Type -> TypeJudgment ()
|
||||
-- checkTypeErased = P.undefined
|
||||
data Term : Set where
|
||||
Checkable : CheckableTerm → Term -- terms with a type checkable.
|
||||
Inferable : InferableTerm → Term -- terms that which types can be inferred.
|
||||
|
||||
{-# COMPILE AGDA2HS Term #-}
|
||||
@ -16,35 +16,27 @@ type Name = String
|
||||
|
||||
type BName = String
|
||||
|
||||
data Term = ToCheck
|
||||
| ToInfer
|
||||
|
||||
data CheckableTerm = UniverseType
|
||||
| Lam BName CheckableTerm
|
||||
| PiType Quantity BName CheckableTerm CheckableTerm
|
||||
| TensorIntro CheckableTerm CheckableTerm
|
||||
| Lam BName CheckableTerm
|
||||
| TensorType Quantity BName CheckableTerm CheckableTerm
|
||||
| Unit
|
||||
| TensorIntro CheckableTerm CheckableTerm
|
||||
| UnitType
|
||||
| Unit
|
||||
| SumType CheckableTerm CheckableTerm
|
||||
| Inl CheckableTerm
|
||||
| Inr CheckableTerm
|
||||
| SumType CheckableTerm CheckableTerm
|
||||
| Inferred InferableTerm
|
||||
|
||||
data InferableTerm = Ann CheckableTerm CheckableTerm
|
||||
| Bound Natural
|
||||
data InferableTerm = Bound Natural
|
||||
| Free Name
|
||||
| Ann CheckableTerm CheckableTerm
|
||||
| App InferableTerm CheckableTerm
|
||||
| TensorTypeElim Quantity BName BName BName InferableTerm
|
||||
CheckableTerm CheckableTerm
|
||||
| SumTypeElim Quantity BName InferableTerm BName CheckableTerm
|
||||
BName CheckableTerm CheckableTerm
|
||||
|
||||
substInferableTerm ::
|
||||
Natural -> InferableTerm -> InferableTerm -> InferableTerm
|
||||
substInferableTerm v i1 i2 = Bound 0
|
||||
|
||||
checkableSubst ::
|
||||
Natural -> InferableTerm -> CheckableTerm -> CheckableTerm
|
||||
checkableSubst v i c = Unit
|
||||
data Term = Checkable CheckableTerm
|
||||
| Inferable InferableTerm
|
||||
|
||||
|
||||
@ -7,20 +7,94 @@ open import Agda.Builtin.Equality
|
||||
|
||||
open import MiniJuvix.Syntax.Core
|
||||
|
||||
-- Language extensions
|
||||
{-# FOREIGN AGDA2HS
|
||||
{-# LANGUAGE LambdaCase #-}
|
||||
{-# LANGUAGE FlexibleInstances #-}
|
||||
#-}
|
||||
|
||||
{-# FOREIGN AGDA2HS
|
||||
import qualified MiniJuvix.Syntax.Core as Core
|
||||
#-}
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
-- What is a value? it's simply a term that contains an answer, i.e. a
|
||||
-- term that does no longer reduce.
|
||||
|
||||
data Value : Set where
|
||||
Universe : Value
|
||||
-- TODO: Obviously there is more stuff I need to add here to cover
|
||||
-- all the possible values.
|
||||
|
||||
{-# COMPILE AGDA2HS Value #-}
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Substitution.
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
substCheckableTerm
|
||||
: CheckableTerm -- Term N
|
||||
→ Nat -- Bound variable x
|
||||
-> InferableTerm -- M
|
||||
-> CheckableTerm -- N[x := M]
|
||||
|
||||
substInferableTerm
|
||||
: InferableTerm -- Term N
|
||||
→ Nat -- bound variable x (Bruijn)
|
||||
-> InferableTerm -- inferable term M
|
||||
-> InferableTerm -- N[x := M]
|
||||
|
||||
substCheckableTerm UniverseType x m = UniverseType
|
||||
substCheckableTerm (PiType q y a b) x m
|
||||
= PiType q y
|
||||
(substCheckableTerm a x m)
|
||||
(substCheckableTerm b (x + 1) m)
|
||||
substCheckableTerm (Lam y n) x m
|
||||
= Lam y (substCheckableTerm n (x + 1) m)
|
||||
substCheckableTerm (TensorType q y s t) x m
|
||||
= TensorType q y
|
||||
(substCheckableTerm s x m)
|
||||
(substCheckableTerm t (x + 1) m)
|
||||
substCheckableTerm (TensorIntro p1 p2) x m
|
||||
= TensorIntro
|
||||
(substCheckableTerm p1 x m)
|
||||
(substCheckableTerm p2 x m)
|
||||
substCheckableTerm UnitType x m = UnitType
|
||||
substCheckableTerm Unit x m = Unit
|
||||
substCheckableTerm (SumType a b) x m
|
||||
= SumType
|
||||
(substCheckableTerm a x m)
|
||||
(substCheckableTerm b x m)
|
||||
substCheckableTerm (Inl n) x m = Inl (substCheckableTerm n x m)
|
||||
substCheckableTerm (Inr n) x m = Inr (substCheckableTerm n x m)
|
||||
substCheckableTerm (Inferred n) x m
|
||||
= Inferred (substInferableTerm n x m)
|
||||
{-# COMPILE AGDA2HS substCheckableTerm #-}
|
||||
|
||||
-- Variable substitution.
|
||||
substInferableTerm (Bound y) x m = if x == y then m else Bound y
|
||||
substInferableTerm (Free y) x m = Free y
|
||||
-- we subst. checkable parts.
|
||||
substInferableTerm (Ann y a) x m
|
||||
= Ann (substCheckableTerm y x m)
|
||||
(substCheckableTerm a x m)
|
||||
substInferableTerm (App f t) x m
|
||||
= App (substInferableTerm f x m)
|
||||
(substCheckableTerm t x m)
|
||||
substInferableTerm (TensorTypeElim q z u v n a b) x m
|
||||
= TensorTypeElim q z u v
|
||||
(substInferableTerm n x m)
|
||||
(substCheckableTerm a (x + 2) m)
|
||||
(substCheckableTerm b (x + 1) m)
|
||||
substInferableTerm (SumTypeElim q z esum u r1 v r2 ann) x m
|
||||
= SumTypeElim q z
|
||||
(substInferableTerm esum x m)
|
||||
u (substCheckableTerm r1 (x + 1) m)
|
||||
v (substCheckableTerm r2 (x + 1) m)
|
||||
(substCheckableTerm ann (x + 1) m)
|
||||
{-# COMPILE AGDA2HS substInferableTerm #-}
|
||||
|
||||
{-- Substitution, denoted by (N[x := M]) is defined by mutual
|
||||
recursion and by induction on N, and replace all the ocurrences of
|
||||
'x' by M in the term N. Recall that N is a term of type either
|
||||
CheckableTerm or InferableTerm.
|
||||
-}
|
||||
|
||||
substTerm : Term → Nat → InferableTerm → Term
|
||||
substTerm (Checkable n) x m = Checkable (substCheckableTerm n x m)
|
||||
substTerm (Inferable n) x m = Inferable (substInferableTerm n x m)
|
||||
@ -1,9 +1,50 @@
|
||||
{-# LANGUAGE LambdaCase #-}
|
||||
{-# LANGUAGE FlexibleInstances #-}
|
||||
|
||||
module MiniJuvix.Syntax.Eval where
|
||||
|
||||
import Numeric.Natural (Natural)
|
||||
|
||||
import qualified MiniJuvix.Syntax.Core as Core
|
||||
|
||||
data Value = Universe
|
||||
|
||||
substCheckableTerm ::
|
||||
CheckableTerm -> Natural -> InferableTerm -> CheckableTerm
|
||||
substCheckableTerm UniverseType x m = UniverseType
|
||||
substCheckableTerm (PiType q y a b) x m
|
||||
= PiType q y (substCheckableTerm a x m)
|
||||
(substCheckableTerm b (x + 1) m)
|
||||
substCheckableTerm (Lam y n) x m
|
||||
= Lam y (substCheckableTerm n (x + 1) m)
|
||||
substCheckableTerm (TensorType q y s t) x m
|
||||
= TensorType q y (substCheckableTerm s x m)
|
||||
(substCheckableTerm t (x + 1) m)
|
||||
substCheckableTerm (TensorIntro p1 p2) x m
|
||||
= TensorIntro (substCheckableTerm p1 x m)
|
||||
(substCheckableTerm p2 x m)
|
||||
substCheckableTerm UnitType x m = UnitType
|
||||
substCheckableTerm Unit x m = Unit
|
||||
substCheckableTerm (SumType a b) x m
|
||||
= SumType (substCheckableTerm a x m) (substCheckableTerm b x m)
|
||||
substCheckableTerm (Inl n) x m = Inl (substCheckableTerm n x m)
|
||||
substCheckableTerm (Inr n) x m = Inr (substCheckableTerm n x m)
|
||||
substCheckableTerm (Inferred n) x m
|
||||
= Inferred (substInferableTerm n x m)
|
||||
|
||||
substInferableTerm ::
|
||||
InferableTerm -> Natural -> InferableTerm -> InferableTerm
|
||||
substInferableTerm (Bound y) x m = if x == y then m else Bound y
|
||||
substInferableTerm (Free y) x m = Free y
|
||||
substInferableTerm (Ann y a) x m
|
||||
= Ann (substCheckableTerm y x m) (substCheckableTerm a x m)
|
||||
substInferableTerm (App f t) x m
|
||||
= App (substInferableTerm f x m) (substCheckableTerm t x m)
|
||||
substInferableTerm (TensorTypeElim q z u v n a b) x m
|
||||
= TensorTypeElim q z u v (substInferableTerm n x m)
|
||||
(substCheckableTerm a (x + 2) m)
|
||||
(substCheckableTerm b (x + 1) m)
|
||||
substInferableTerm (SumTypeElim q z esum u r1 v r2 ann) x m
|
||||
= SumTypeElim q z (substInferableTerm esum x m) u
|
||||
(substCheckableTerm r1 (x + 1) m)
|
||||
v
|
||||
(substCheckableTerm r2 (x + 1) m)
|
||||
(substCheckableTerm ann (x + 1) m)
|
||||
|
||||
|
||||
Loading…
Reference in New Issue
Block a user