------------------------------------------------------------------------
-- Some definitions that are re-exported from Definition.Untyped but
-- do not depend on that module's module parameter
------------------------------------------------------------------------

module Definition.Untyped.NotParametrised where

open import Tools.Bool
open import Tools.Fin
open import Tools.Function
open import Tools.Level
open import Tools.List
open import Tools.Nat
open import Tools.PropositionalEquality
open import Tools.Vec

private variable
  a       : Level
  Ξ± l m n : Nat
  𝕋 π•Œ     : Set a
  P Q     : Nat β†’ Set _

------------------------------------------------------------------------
-- Definitions related to terms

-- Typing contexts (length indexed snoc-lists, isomorphic to lists).
-- Terms added to the context are well scoped in the sense that it cannot
-- contain more unbound variables than can be looked up in the context.

infixl 24 _βˆ™_

data Con (A : Nat β†’ Set a) : Nat β†’ Set a where
  Ξ΅   :                             Con A 0        -- Empty context.
  _βˆ™_ : {n : Nat} β†’ Con A n β†’ A n β†’ Con A (1+ n)   -- Context extension.

private variable
  Ξ“ : Con _ _

-- Empty-conΒ Ξ“ holds if Ξ“ is empty.

data Empty-con {P : Nat β†’ Set a} : Con P n β†’ Set a where
  Ξ΅ : Empty-con Ξ΅

-- A variant of Empty-con.

infix 4 _or-empty_

data _or-empty_ {P : Nat β†’ Set a} (A : Set a) : Con P n β†’ Set a where
  possibly-nonempty : ⦃ ok : A ⦄ β†’ A or-empty Ξ“
  Ξ΅                 : A or-empty Ξ΅

-- Representation of sub terms using a list of binding levels

infixr 5 _βˆ·β‚œ_

data GenTs (A : Nat β†’ Set a) : Nat β†’ List Nat β†’ Set a where
  []   : {n : Nat} β†’ GenTs A n []
  _βˆ·β‚œ_ : {n b : Nat} {bs : List Nat}
         (t : A (b + n)) (ts : GenTs A n bs) β†’ GenTs A n (b ∷ bs)

-- Sigma and Unit types have two modes, allowing either projections
-- and Ξ·-equality (strong) or elimination by prodrec/unitrec (weak).
--
-- Note that one can optionally enable Ξ·-equality for weak unit types,
-- see Definition.Typed.Variant.Type-variant.Ξ·-for-UnitΚ·.
data Strength : Set where
  𝕀 𝕨 : Strength

-- Ξ - or Ξ£-types.

data BinderMode : Set where
  BMΞ  : BinderMode
  BMΞ£ : (s : Strength) β†’ BinderMode

-- The function dropΒ k removes the last k entries from contexts.

drop : βˆ€ k β†’ Con P (k + n) β†’ Con P n
drop 0      Ξ“       = Ξ“
drop (1+ k) (Ξ“ βˆ™ _) = drop k Ξ“

-- A map function for contexts.

map-Con : (βˆ€ {n} β†’ P n β†’ Q n) β†’ Con P n β†’ Con Q n
map-Con _ Ξ΅       = Ξ΅
map-Con f (Ξ“ βˆ™ A) = map-Con f Ξ“ βˆ™ f A

------------------------------------------------------------------------
-- Weakening

-- In the following we define untyped weakenings Ξ· : Wk.
-- The typed form could be written Ξ· : Ξ“ ≀ Ξ” with the intention
-- that Ξ· transport a term t living in context Ξ” to a context Ξ“
-- that can bind additional variables (which cannot appear in t).
-- Thus, if Ξ” ⊒ t : A and Ξ· : Ξ“ ≀ Ξ” then Ξ“ ⊒ wk Ξ· t : wk Ξ· A.
--
-- Even though Ξ“ is "larger" than Ξ” we write Ξ“ ≀ Ξ” to be conformant
-- with subtyping A ≀ B.  With subtyping, relation Ξ“ ≀ Ξ” could be defined as
-- ``for all x ∈ dom(Ξ”) have Ξ“(x) ≀ Ξ”(x)'' (in the sense of subtyping)
-- and this would be the natural extension of weakenings.

data Wk : Nat β†’ Nat β†’ Set where
  id    : {n : Nat}   β†’ Wk n n                    -- Ξ· : Ξ“ ≀ Ξ“.
  step  : {n m : Nat} β†’ Wk m n β†’ Wk (1+ m) n      -- If Ξ· : Ξ“ ≀ Ξ” then step Ξ· : Ξ“βˆ™A ≀ Ξ”.
  lift  : {n m : Nat} β†’ Wk m n β†’ Wk (1+ m) (1+ n) -- If Ξ· : Ξ“ ≀ Ξ” then lift Ξ· : Ξ“βˆ™A ≀ Ξ”βˆ™A.

-- Composition of weakening.
-- If Ξ· : Ξ“ ≀ Ξ” and Ξ·β€² : Ξ” ≀ Ξ¦ then Ξ· β€’ Ξ·β€² : Ξ“ ≀ Ξ¦.

infixl 30 _β€’_

_β€’_                :  {l m n : Nat} β†’ Wk l m β†’ Wk m n β†’ Wk l n
id      β€’ Ξ·β€²       =  Ξ·β€²
step Ξ·  β€’ Ξ·β€²       =  step  (Ξ· β€’ Ξ·β€²)
lift Ξ·  β€’ id       =  lift  Ξ·
lift Ξ·  β€’ step Ξ·β€²  =  step  (Ξ· β€’ Ξ·β€²)
lift Ξ·  β€’ lift Ξ·β€²  =  lift  (Ξ· β€’ Ξ·β€²)

liftn : {k m : Nat} β†’ Wk k m β†’ (n : Nat) β†’ Wk (n + k) (n + m)
liftn ρ 0 = ρ
liftn ρ (1+ n) = lift (liftn ρ n)

stepn : {k m : Nat} (ρ : Wk k m) β†’ (n : Nat) β†’ Wk (n + k) m
stepn ρ 0 = ρ
stepn ρ (1+ n) = step (stepn ρ n)

-- The weakening step-atΒ x inserts a fresh variable at position x.

step-at : Fin n β†’ Wk n (pred n)
step-at x0                  = step id
step-at (_+1 {n = 0}    ())
step-at (_+1 {n = 1+ _} x)  = lift (step-at x)

-- A variant of step-at without lift constructors in the result.

step-atβ€² : (x : Fin n) β†’ Wk (n ∸ toβ„• x) (pred n ∸ toβ„• x)
step-atβ€² x0                  = step id
step-atβ€² (_+1 {n = 0}    ())
step-atβ€² (_+1 {n = 1+ _} x)  = step-atβ€² x

-- Weakening of variables.
-- If Ξ· : Ξ“ ≀ Ξ” and x ∈ dom(Ξ”) then wkVar Ξ· x ∈ dom(Ξ“).

wkVar : {m n : Nat} (ρ : Wk m n) (x : Fin n) β†’ Fin m
wkVar id x            = x
wkVar (step ρ) x      = (wkVar ρ x) +1
wkVar (lift ρ) x0     = x0
wkVar (lift ρ) (x +1) = (wkVar ρ x) +1

-- A weakening for closed terms.

wkβ‚€ : Wk n 0
wkβ‚€ {n = 0}    = id
wkβ‚€ {n = 1+ n} = step wkβ‚€

------------------------------------------------------------------------
-- Universe levels

-- Universe levels.

data Universe-level : Set where
  0ᡘ+_ : Nat β†’ Universe-level
  Ο‰α΅˜ : Universe-level

0ᡘ : Universe-level
0ᡘ = 0ᡘ+ 0

1ᡘ : Universe-level
1ᡘ = 0ᡘ+ 1

-- The maximum of two universe levels.

infixl 6 _βŠ”α΅˜_

_βŠ”α΅˜_ : (_ _ : Universe-level) β†’ Universe-level
(0ᡘ+ m) βŠ”α΅˜ (0ᡘ+ n) = 0ᡘ+ (m Tools.Nat.βŠ” n)
(0ᡘ+ m) βŠ”α΅˜ Ο‰α΅˜      = Ο‰α΅˜
Ο‰α΅˜      βŠ”α΅˜ n       = Ο‰α΅˜

-- Ordering of universe levels.

infix 4 _β‰€α΅˜_

data _β‰€α΅˜_ : Universe-level β†’ Universe-level β†’ Set where
  β‰€α΅˜-fin : βˆ€ {l lβ€²} β†’ l ≀′ lβ€² β†’ 0ᡘ+ l β‰€α΅˜ 0ᡘ+ lβ€²
  β‰€α΅˜-Ο‰α΅˜  : βˆ€ {l} β†’ l β‰€α΅˜ Ο‰α΅˜

β‰€α΅˜-refl : βˆ€ {l} β†’ l β‰€α΅˜ l
β‰€α΅˜-refl {0ᡘ+ x} = β‰€α΅˜-fin ≀′-refl
β‰€α΅˜-refl {(Ο‰α΅˜)} = β‰€α΅˜-Ο‰α΅˜

-- Strict ordering of universe levels.

infix 4 _<ᡘ_

data _<ᡘ_ : Universe-level β†’ Universe-level β†’ Set where
  <ᡘ-fin : βˆ€ {l lβ€²} β†’ l <β€² lβ€² β†’ 0ᡘ+ l <ᡘ 0ᡘ+ lβ€²
  <ᡘ-Ο‰α΅˜  : βˆ€ {l} β†’ 0ᡘ+ l <ᡘ Ο‰α΅˜

0ᡘ<ᡘ1ᡘ : 0ᡘ <ᡘ 1ᡘ
0ᡘ<ᡘ1ᡘ = <ᡘ-fin ≀′-refl

------------------------------------------------------------------------
-- Level-support

-- If Level is a type, is it small?

data Level-small : Set where
  small not-small : Level-small

-- Is Level a type, and in that case is the type small?

data Level-support : Set where
  -- Only level literals are allowed. Level is not a type.
  only-literals : Level-support
  -- Level is a type.
  level-type : Level-small β†’ Level-support

private variable
  sm sm₁ smβ‚‚ : Level-small

-- An ordering relation for Level-small.

infix 4 _≀LSm_

data _≀LSm_ : Level-small β†’ Level-small β†’ Set where
  not-small≀  : not-small ≀LSm sm
  small≀small : small     ≀LSm small

-- An ordering relation for Level-support.

data _≀LS_ : Level-support β†’ Level-support β†’ Set where
  only-literals≀ : only-literals ≀LS only-literals
  level-type     : sm₁ ≀LSm smβ‚‚ β†’ level-type sm₁ ≀LS level-type smβ‚‚

------------------------------------------------------------------------
-- Definition contexts

-- Unfolding vectors. The value true stands for "unfold".

Unfolding : Nat β†’ Set
Unfolding = Vec Bool

pattern _⁰ Ο† = false ∷ Ο†
pattern _ΒΉ Ο† = true  ∷ Ο†

opaque

  -- Merging of unfolding vectors.

  infixl 5 _βŠ”α΅’_

  _βŠ”α΅’_ : Unfolding n β†’ Unfolding n β†’ Unfolding n
  _βŠ”α΅’_ = zipWith _∨_

opaque

  -- A vector for unfolding everything.

  ones : Unfolding n
  ones = replicate _ true

opaque

  -- A vector for unfolding nothing.

  zeros : Unfolding n
  zeros = replicate _ false

-- Opacity.

data Opacity (n : Nat) : Set where
  -- Opaque, with the given unfolding clause.
  opa : Unfolding n β†’ Opacity n
  -- Transparent.
  tra : Opacity n

-- Definition contexts.

infixl 24 _βˆ™βŸ¨_⟩[_∷_] _βˆ™βŸ¨_⟩! _βˆ™!

data DCon (𝕋 : Set a) : Nat β†’ Set a where
  Ξ΅          : DCon 𝕋 0
  _βˆ™βŸ¨_⟩[_∷_] : DCon 𝕋 n β†’ Opacity n β†’ 𝕋 β†’ 𝕋 β†’ DCon 𝕋 (1+ n)

pattern _βˆ™βŸ¨_⟩! βˆ‡ Ο‰ = βˆ‡ βˆ™βŸ¨ Ο‰ ⟩[ _ ∷ _ ]
pattern _βˆ™! βˆ‡      = βˆ‡ βˆ™βŸ¨ _ ⟩!

private variable
  βˆ‡ : DCon _ _
  Ο‰ : Opacity _
  Ο† : Unfolding _

-- The type Ξ±Β β†¦βˆ·Β AΒ βˆˆΒ βˆ‡ means that Ξ± has type A in βˆ‡.

data _β†¦βˆ·_∈_ {𝕋 : Set a} : Nat β†’ 𝕋 β†’ DCon 𝕋 n β†’ Set a where
  here  : βˆ€ {A t} {βˆ‡ : DCon 𝕋 n} β†’ n β†¦βˆ· A ∈ βˆ‡ βˆ™βŸ¨ Ο‰ ⟩[ t ∷ A ]
  there : βˆ€ {A B u} β†’ Ξ± β†¦βˆ· A ∈ βˆ‡ β†’ Ξ± β†¦βˆ· A ∈ βˆ‡ βˆ™βŸ¨ Ο‰ ⟩[ u ∷ B ]

-- The type α ↦ t ∷ AΒ βˆˆΒ βˆ‡ means that Ξ± is (transparently) equal to t
-- of type A in βˆ‡.

data _↦_∷_∈_ {𝕋 : Set a} : Nat β†’ 𝕋 β†’ 𝕋 β†’ DCon 𝕋 n β†’ Set a where
  here  : βˆ€ {A t} {βˆ‡ : DCon 𝕋 n}      β†’ n ↦ t ∷ A ∈ βˆ‡ βˆ™βŸ¨ tra ⟩[ t ∷ A ]
  there : βˆ€ {A B t u} β†’ Ξ± ↦ t ∷ A ∈ βˆ‡ β†’ Ξ± ↦ t ∷ A ∈ βˆ‡ βˆ™βŸ¨ Ο‰   ⟩[ u ∷ B ]

-- The type Ξ±Β β†¦βŠ˜βˆ·Β AΒ βˆˆΒ βˆ‡ means that Ξ± is an opaque definition of type A
-- in βˆ‡.

data _β†¦βŠ˜βˆ·_∈_ {𝕋 : Set a} : Nat β†’ 𝕋 β†’ DCon 𝕋 n β†’ Set a where
  here  : βˆ€ {A t} {βˆ‡ : DCon 𝕋 n}  β†’ n β†¦βŠ˜βˆ· A ∈ βˆ‡ βˆ™βŸ¨ opa Ο† ⟩[ t ∷ A ]
  there : βˆ€ {A B u} β†’ Ξ± β†¦βŠ˜βˆ· A ∈ βˆ‡ β†’ Ξ± β†¦βŠ˜βˆ· A ∈ βˆ‡ βˆ™βŸ¨ Ο‰     ⟩[ u ∷ B ]

-- Glassification.

glassify : {𝕋 : Set a} β†’ DCon 𝕋 n β†’ DCon 𝕋 n
glassify Ξ΅                       = Ξ΅
glassify (βˆ‡ βˆ™βŸ¨ Ο‰ ⟩[ t ∷ A ]) = glassify βˆ‡ βˆ™βŸ¨ tra ⟩[ t ∷ A ]

-- A definition context is transparent if it is equal to its own
-- "glassification".

Transparent : {𝕋 : Set a} β†’ DCon 𝕋 n β†’ Set a
Transparent βˆ‡ = βˆ‡ ≑ glassify βˆ‡

-- Definition context extensions.

data DExt (𝕋 : Set a) : Nat β†’ Nat β†’ Set a where
  id   : n ≑ m β†’ DExt 𝕋 m n
  step : DExt 𝕋 m n β†’ Opacity m β†’ 𝕋 β†’ 𝕋 β†’ DExt 𝕋 (1+ m) n

pattern idᡉ         = id refl
pattern step₁ Ο‰ A t = step idᡉ Ο‰ A t

opaque

  -- Turns a definition context into a definition context extension.

  as-DExt : DCon 𝕋 n β†’ DExt 𝕋 n 0
  as-DExt Ξ΅                   = idᡉ
  as-DExt (βˆ‡ βˆ™βŸ¨ Ο‰ ⟩[ t ∷ A ]) = step (as-DExt βˆ‡) Ο‰ A t

opaque

  infixl 24 _α΅ˆβ€’_

  -- Appends a definition context extension to a definition context.

  _α΅ˆβ€’_ : DCon 𝕋 m β†’ DExt 𝕋 n m β†’ DCon 𝕋 n
  βˆ‡ α΅ˆβ€’ id eq        = subst (DCon _) eq βˆ‡
  βˆ‡ α΅ˆβ€’ step ΞΎ Ο‰ A t = (βˆ‡ α΅ˆβ€’ ΞΎ) βˆ™βŸ¨ Ο‰ ⟩[ t ∷ A ]

-- Concatenation of definition context extensions.

_β€’α΅ˆ_ : {𝕋 : Set a} β†’ DExt 𝕋 m n β†’ DExt 𝕋 n l β†’ DExt 𝕋 m l
id eq         β€’α΅ˆ ΞΎ = subst (flip (DExt _) _) eq ΞΎ
step ΞΎβ€² Ο‰ A t β€’α΅ˆ ΞΎ = step (ΞΎβ€² β€’α΅ˆ ΞΎ) Ο‰ A t

opaque

  -- Glassification for DExt.

  glassifyᡉ : DExt 𝕋 m n β†’ DExt 𝕋 m n
  glassifyᡉ (id eq)        = id eq
  glassifyᡉ (step ΞΎ _ A t) = step (glassifyᡉ ΞΎ) tra A t

-- A map function for definition contexts.

map-DCon : (𝕋 β†’ π•Œ) β†’ DCon 𝕋 n β†’ DCon π•Œ n
map-DCon _ Ξ΅                   = Ξ΅
map-DCon f (βˆ‡ βˆ™βŸ¨ Ο‰ ⟩[ t ∷ A ]) =
  map-DCon f βˆ‡ βˆ™βŸ¨ Ο‰ ⟩[ f t ∷ f A ]

------------------------------------------------------------------------
-- Context pairs

-- Pairs of definition contexts and variable contexts.

infix 5 _Β»_

record Context-pair (P : Nat β†’ Set a) (m n : Nat) : Set a where
  constructor _Β»_
  field
    -- The definition context.
    defs : DCon (P 0) m
    -- The variable context.
    vars : Con P n

open Context-pair public

-- A variant of Con._βˆ™_ for Context-pair.

infixl 24 _Β»βˆ™_

_Β»βˆ™_ : Context-pair P m n β†’ P n β†’ Context-pair P m (1+ n)
(βˆ‡ Β» Ξ“) Β»βˆ™ A = βˆ‡ Β» Ξ“ βˆ™ A

-- A map function for context pairs.

map-Cons : (βˆ€ {n} β†’ P n β†’ Q n) β†’ Context-pair P m n β†’ Context-pair Q m n
map-Cons f (βˆ‡ Β» Ξ“) = map-DCon f βˆ‡ Β» map-Con f Ξ“