ModuleAgda-2.8.0.2Haskell2010

Agda.TypeChecking.With

9 values

PackageAgda-2.8.0.2
Exports9
LanguageHaskell2010
LicenceMIT
SourceWith.hs

valuesplitTelForWith

:: Telescope
Δ context of types and with-arguments.
-> Type
Δ ⊢ t type of rhs.
-> List1 (Arg (Term, EqualityView))
Δ ⊢ vs : as with arguments and their types. Output:
-> (Telescope, Telescope, Permutation, Type, List1 (Arg (Term, EqualityView)))
(Δ₁,Δ₂,π,t',vtys') where
Δ₁
part of context needed for with arguments and their types.
Δ₂
part of context not needed for with arguments and their types.
π
permutation from Δ to Δ₁Δ₂ as returned by
splitTelescope
.
Δ₁Δ₂ ⊢ t'
type of rhs under
π
Δ₁ ⊢ vtys'
with-arguments and their types under
π
.

Split pattern variables according to with-expressions.

valuewithFunctionType

:: Telescope
Δ₁ context for types of with-expressions.
-> List1 (Arg (Term, EqualityView))
Δ₁,Δ₂ ⊢ vs : raise Δ₂ as with and rewrite-expressions and their type.
-> Telescope
Δ₁ ⊢ Δ₂ context extension to type with-expressions.
-> Type
Δ₁,Δ₂ ⊢ b type of rhs.
-> Boundary
Δ₁,Δ₂ ⊢ [(i,(u0,u1))] : b boundary of rhs.
-> TCM (Type, (Nat1, Nat))
Δ₁ → wtel → Δ₂′ → b′ such that [vs/wtel]wtel = as and [vs/wtel]Δ₂′ = Δ₂ and [vs/wtel]b′ = b. Plus the final number of with-arguments and the number of visible ones.

Abstract with-expressions vs to generate type for with-helper function.

Each EqualityType, coming from a rewrite, will turn into 2 abstractions.

valuecountWithArgs :: (Functor f, Foldable f) => f EqualityView -> Nat1

Count the number of arguments introduced into the type of the with-function.

valuecountWithPats

:: (Functor f, Foldable f)
=> f (Arg (Term, EqualityView))
-> Nat1

Count the number of with-patterns in the with-clause that need to be transformed to regular patterns in the **current round** of with-abstraction (important for nested with).

valuewithArguments :: List1 (Arg (Term, EqualityView)) -> TCM (List1 (Arg Term))

From a list of with and rewrite expressions and their types, compute the list of final with expressions (after expanding the rewrites).

valuebuildWithFunction

:: [Name]
Names of the module parameters of the parent function.
-> QName
Name of the parent function.
-> QName
Name of the with-function.
-> Type
Types of the parent function.
-> Telescope
Context of parent patterns.
-> [NamedArg DeBruijnPattern]
Parent patterns.
-> Nat
Number of module parameters in parent patterns
-> Substitution
Substitution from parent lhs to with function lhs
-> Permutation
Final permutation.
-> Nat
Number of needed vars.
-> Nat
Number of with expressions.
-> List1 SpineClause
With-clauses.
-> TCM (List1 SpineClause)
With-clauses flattened wrt. parent patterns.

Compute the clauses for the with-function given the original patterns.

valuestripWithClausePatterns

:: [Name]
cxtNames names of the module parameters of the parent function
-> QName
parent name of the parent function.
-> QName
f name of with-function.
-> Type
t top-level type of the original function.
-> Telescope
Δ context of patterns of parent function.
-> [NamedArg DeBruijnPattern]
qs internal patterns for original function.
-> Nat
npars number of module parameters in qs.
-> Permutation
π permutation taking vars(qs) to support(Δ).
-> [NamedArg Pattern]
ps patterns in with clause (eliminating type t).
-> TCM ([ProblemEq], [NamedArg Pattern])
ps' patterns for with function (presumably of type Δ).

stripWithClausePatterns cxtNames parent f t Δ qs np π ps = ps'

Example:

  record Stream (A : Set) : Set where
    coinductive
    constructor delay
    field       force : A × Stream A

  record SEq (s t : Stream A) : Set where
    coinductive
    field
      ~force : let a , as = force s
                   b , bs = force t
               in  a ≡ b × SEq as bs

  test : (s : Nat × Stream Nat) (t : Stream Nat) → SEq (delay s) t → SEq t (delay s)
  ~force (test (a     , as) t p) with force t
  ~force (test (suc n , as) t p) | b , bs = ?

With function:

  f : (t : Stream Nat) (w : Nat × Stream Nat) (a : Nat) (as : Stream Nat)
      (p : SEq (delay (a , as)) t) → (fst w ≡ a) × SEq (snd w) as

  Δ  = t a as p   -- reorder to bring with-relevant (= needed) vars first
  π  = a as t p → Δ
  qs = (a     , as) t p ~force
  ps = (suc n , as) t p ~force
  ps' = (suc n) as t p

Resulting with-function clause is:

  f t (b , bs) (suc n) as t p

Note: stripWithClausePatterns factors ps through qs, thus

  ps = qs[ps']

where [..] is to be understood as substitution. The projection patterns have vanished from ps' (as they are already in qs).

valuewithDisplayForm

:: QName
The name of parent function.
-> QName
The name of the with-function.
-> Telescope
Δ₁ The arguments of the with function before the with expressions.
-> Telescope
Δ₂ The arguments of the with function after the with expressions.
-> Nat
n The number of with expressions.
-> [NamedArg DeBruijnPattern]
qs The parent patterns.
-> Permutation
perm Permutation to split into needed and unneeded vars.
-> Permutation
lhsPerm Permutation reordering the variables in parent patterns.
-> TCM DisplayForm

Construct the display form for a with function. It will display applications of the with function as applications to the original function. For instance,

    aux a b c

    f (suc a) (suc b) | c

valuepatsToElims :: [NamedArg DeBruijnPattern] -> [Elim' DisplayTerm]