{-# LANGUAGE CPP #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE TypeSynonymInstances, FlexibleInstances #-}

{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

-- | Substitution and weak head evaluation

module Substitute where

import Internal

import Impossible
#include "undefined.h"

-- | Substitutions are lists of terms.

type Subst = [Term]

-- | Weakening substitution @Γ.Δ ⊢ wkS |Δ| : Γ@

wkS :: Int -> Subst
wkS :: Int -> Subst
wkS Int
n = (Int -> Term) -> [Int] -> Subst
forall a b. (a -> b) -> [a] -> [b]
map (Index -> Term
Var (Index -> Term) -> (Int -> Index) -> Int -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Index
Index) [Int
n,Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1..]

-- | Identity substitution @Γ ⊢ idS : Γ@.

idS :: Subst
idS :: Subst
idS = Int -> Subst
wkS Int
0

-- | Composing substitution
--   @
--      Γ₁ ⊢ τ : Γ₂    Γ₂ ⊢ σ : Γ₃
--      -------------------------
--      Γ₁ ⊢ compS τ σ : Γ₃
--   @

compS :: Subst -> Subst -> Subst
compS :: Subst -> Subst -> Subst
compS = Subst -> Subst -> Subst
forall a. Substitute a => Subst -> a -> a
subst

-- | Extending a substitution
--   @
--      Γ ⊢ σ : Δ    Δ ⊢ T    Γ ⊢ t : Tσ
--      --------------------------------
--      Γ ⊢ consS t σ : Δ.T
--   @

consS :: Term -> Subst -> Subst
consS :: Term -> Subst -> Subst
consS = (:)

-- | Lifting a substitution under a binder.
--   @
--      Γ ⊢ σ : Δ      Δ ⊢ T
--      --------------------
--      Γ.Tσ ⊢ liftS σ : Δ.T
--   @

liftS :: Subst -> Subst
liftS :: Subst -> Subst
liftS Subst
s = Term -> Subst -> Subst
consS (Index -> Term
Var Index
0) (Subst -> Subst) -> Subst -> Subst
forall a b. (a -> b) -> a -> b
$ Subst -> Subst
weakS Subst
s

-- | Weakening a substitution.
--
--   @
--     Γ ⊢ σ : Δ    Γ ⊢ T
--     ------------------
--     Γ.T ⊢ weakS σ : Δ
--   @

weakS :: Subst -> Subst
weakS :: Subst -> Subst
weakS = Subst -> Subst -> Subst
compS (Int -> Subst
wkS Int
1)

-- | Looking up an entry in a substitution.

lookupS :: Subst -> Index -> Term
lookupS :: Subst -> Index -> Term
lookupS Subst
s Index
i =  Subst
s Subst -> Int -> Term
forall a. [a] -> Int -> a
!! Index -> Int
dbIndex Index
i

-- | Substitution for various syntactic categories.

class Substitute a where
  subst :: Subst -> a -> a

instance Substitute a => Substitute [a] where
  subst :: Subst -> [a] -> [a]
subst Subst
s = (a -> a) -> [a] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map (Subst -> a -> a
forall a. Substitute a => Subst -> a -> a
subst Subst
s)

instance Substitute a => Substitute (Dom a) where
  subst :: Subst -> Dom a -> Dom a
subst Subst
s = (a -> a) -> Dom a -> Dom a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Subst -> a -> a
forall a. Substitute a => Subst -> a -> a
subst Subst
s)

instance Substitute a => Substitute (Arg a) where
  subst :: Subst -> Arg a -> Arg a
subst Subst
s = (a -> a) -> Arg a -> Arg a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Subst -> a -> a
forall a. Substitute a => Subst -> a -> a
subst Subst
s)

instance Substitute a => Substitute (Elim' a) where
  subst :: Subst -> Elim' a -> Elim' a
subst Subst
s = (a -> a) -> Elim' a -> Elim' a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Subst -> a -> a
forall a. Substitute a => Subst -> a -> a
subst Subst
s)

instance Substitute Term where
  subst :: Subst -> Term -> Term
subst Subst
s = \case
    Type Term
l  -> Term -> Term
Type (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Subst -> Term -> Term
forall a. Substitute a => Subst -> a -> a
subst Subst
s Term
l
    Term
Size    -> Term
Size
    Nat Term
a   -> Term -> Term
Nat (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Subst -> Term -> Term
forall a. Substitute a => Subst -> a -> a
subst Subst
s Term
a
    Zero Arg Term
a  -> Arg Term -> Term
Zero (Arg Term -> Term) -> Arg Term -> Term
forall a b. (a -> b) -> a -> b
$ Subst -> Arg Term -> Arg Term
forall a. Substitute a => Subst -> a -> a
subst Subst
s Arg Term
a
    Suc Arg Term
a Term
t -> Arg Term -> Term -> Term
Suc (Subst -> Arg Term -> Arg Term
forall a. Substitute a => Subst -> a -> a
subst Subst
s Arg Term
a) (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Subst -> Term -> Term
forall a. Substitute a => Subst -> a -> a
subst Subst
s Term
t
    Term
Infty   -> Term
Infty
    Pi Dom Term
u Abs Term
t  -> Dom Term -> Abs Term -> Term
Pi (Subst -> Dom Term -> Dom Term
forall a. Substitute a => Subst -> a -> a
subst Subst
s Dom Term
u) (Abs Term -> Term) -> Abs Term -> Term
forall a b. (a -> b) -> a -> b
$ Subst -> Abs Term -> Abs Term
forall a. Substitute a => Subst -> a -> a
subst Subst
s Abs Term
t
    Lam ArgInfo
r Abs Term
t -> ArgInfo -> Abs Term -> Term
Lam ArgInfo
r (Abs Term -> Term) -> Abs Term -> Term
forall a b. (a -> b) -> a -> b
$ Subst -> Abs Term -> Abs Term
forall a. Substitute a => Subst -> a -> a
subst Subst
s Abs Term
t
    Var Index
i   -> Subst -> Index -> Term
lookupS Subst
s Index
i
    Def Id
f   -> Id -> Term
Def Id
f
    App Term
t Elim
u -> Term -> Elim -> Term
App (Subst -> Term -> Term
forall a. Substitute a => Subst -> a -> a
subst Subst
s Term
t) (Subst -> Elim -> Elim
forall a. Substitute a => Subst -> a -> a
subst Subst
s Elim
u)

instance Substitute (Abs Term) where
  subst :: Subst -> Abs Term -> Abs Term
subst Subst
s (Abs   Id
x Term
t) = Id -> Term -> Abs Term
forall a. Id -> a -> Abs a
Abs   Id
x (Term -> Abs Term) -> Term -> Abs Term
forall a b. (a -> b) -> a -> b
$ Subst -> Term -> Term
forall a. Substitute a => Subst -> a -> a
subst (Subst -> Subst
liftS Subst
s) Term
t
  subst Subst
s (NoAbs Id
x Term
t) = Id -> Term -> Abs Term
forall a. Id -> a -> Abs a
NoAbs Id
x (Term -> Abs Term) -> Term -> Abs Term
forall a b. (a -> b) -> a -> b
$ Subst -> Term -> Term
forall a. Substitute a => Subst -> a -> a
subst Subst
s Term
t

raise :: Substitute a => Int -> a -> a
raise :: Int -> a -> a
raise Int
n = Subst -> a -> a
forall a. Substitute a => Subst -> a -> a
subst (Int -> Subst
wkS Int
n)


-- | Construct the type of the functional for fix.
--
--   @fixType t = .(i : Size) -> ((x : Nat i) -> T i x) -> (x : Nat (i + 1)) -> T (i + 1) x

fixType :: Term -> Term
fixType :: Term -> Term
fixType Term
t =
  Dom Term -> Abs Term -> Term
Pi (ArgInfo -> Term -> Dom Term
forall a. ArgInfo -> a -> Dom a
Dom ArgInfo
Irrelevant Term
Size) (Abs Term -> Term) -> Abs Term -> Term
forall a b. (a -> b) -> a -> b
$ Id -> Term -> Abs Term
forall a. Id -> a -> Abs a
Abs Id
"i" (Term -> Abs Term) -> Term -> Abs Term
forall a b. (a -> b) -> a -> b
$
    Dom Term -> Abs Term -> Term
Pi (ArgInfo -> Term -> Dom Term
forall a. ArgInfo -> a -> Dom a
Dom ArgInfo
Relevant (Term -> Dom Term) -> Term -> Dom Term
forall a b. (a -> b) -> a -> b
$ Term -> Term
f (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Index -> Term
Var Index
0) (Abs Term -> Term) -> Abs Term -> Term
forall a b. (a -> b) -> a -> b
$ Id -> Term -> Abs Term
forall a. Id -> a -> Abs a
NoAbs Id
"_" (Term -> Abs Term) -> Term -> Abs Term
forall a b. (a -> b) -> a -> b
$
      Term -> Term
f (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Term -> Term
sSuc (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Index -> Term
Var Index
0
  where
  f :: Term -> Term
f Term
a = Dom Term -> Abs Term -> Term
Pi (ArgInfo -> Term -> Dom Term
forall a. ArgInfo -> a -> Dom a
Dom ArgInfo
Relevant (Term -> Term
Nat Term
a)) (Abs Term -> Term) -> Abs Term -> Term
forall a b. (a -> b) -> a -> b
$ Id -> Term -> Abs Term
forall a. Id -> a -> Abs a
Abs Id
"x" (Term -> Abs Term) -> Term -> Abs Term
forall a b. (a -> b) -> a -> b
$
          Int -> Term -> Term
forall a. Substitute a => Int -> a -> a
raise Int
2 Term
t
            Term -> Elim -> Term
`App` Arg Term -> Elim
forall a. Arg a -> Elim' a
Apply (ArgInfo -> Term -> Arg Term
forall a. ArgInfo -> a -> Arg a
Arg ArgInfo
ShapeIrr (Term -> Arg Term) -> Term -> Arg Term
forall a b. (a -> b) -> a -> b
$ Int -> Term -> Term
forall a. Substitute a => Int -> a -> a
raise Int
1 Term
a)
            Term -> Elim -> Term
`App` Arg Term -> Elim
forall a. Arg a -> Elim' a
Apply (ArgInfo -> Term -> Arg Term
forall a. ArgInfo -> a -> Arg a
Arg ArgInfo
Relevant (Term -> Arg Term) -> Term -> Arg Term
forall a b. (a -> b) -> a -> b
$ Index -> Term
Var Index
0)