{-# LANGUAGE BlockArguments        #-}
{-# LANGUAGE ConstraintKinds       #-}
{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE EmptyCase             #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE KindSignatures        #-}
{-# LANGUAGE LambdaCase            #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes            #-}
{-# LANGUAGE ScopedTypeVariables   #-}
{-# LANGUAGE TypeApplications      #-}
{-# LANGUAGE UndecidableInstances  #-}
-- | Foil implementation of the \(\lambda\Pi\)-calculus (with pairs).
--
-- The following is implemented __manually__ in this module:
--
-- 1. Scope-safe AST for \(\lambda\Pi\)-terms.
-- 2. Correct capture-avoiding substitution (see 'substitute').
-- 3. Conversion between scope-safe and raw term representation (the latter is generated via BNFC), see 'toFoilTerm' and 'fromFoilTerm'.
-- 4. Helper functions for patterns. See 'extendScopePattern' and 'withRefreshedPattern'.
-- 5. \(\alpha\)-equivalence checks ('alphaEquiv' and 'alphaEquivRefreshed') and \(\alpha\)-normalization helpers ('refreshExpr').
-- 6. Computation of weak head normal form (WHNF) and normal form (NF), see 'whnf' and 'nf'.
-- 7. Entry point, gluing everything together. See 'defaultMain'.
--
-- This implementation supports (nested) patterns for pairs.
--
-- This is a baseline implementation, see other examples for partial automation:
--
-- 1. "Language.LambdaPi.Impl.FreeFoil" allows to reuse generalized substitution and \(\alpha\)-equivalence (and, in theory, more complicated algorithms).
-- 2. "Language.LambdaPi.Impl.FoilTH" works well with patterns and generates conversion functions and helpers for patterns.
-- 3. "Language.LambdaPi.Impl.FreeFoilTH" combines the benefits of the above, when it is possible to generate the signature automatically.
module Language.LambdaPi.Impl.Foil where

import           Control.Monad.Foil
import           Control.Monad.Foil.Relative
import           Data.Coerce                     (coerce)
import           Data.Map                        (Map)
import qualified Data.Map                        as Map
import           Data.String
import qualified Language.LambdaPi.Syntax.Abs    as Raw
import           Language.LambdaPi.Syntax.Layout (resolveLayout)
import           Language.LambdaPi.Syntax.Lex    (tokens)
import           Language.LambdaPi.Syntax.Par    (pProgram, pTerm)
import           Language.LambdaPi.Syntax.Print  (printTree)
import           System.Exit                     (exitFailure)

-- $setup
-- >>> :set -XOverloadedStrings
-- >>> :set -XDataKinds
-- >>> import Control.Monad.Foil

-- * Scope-safe AST

-- | Type of scope-safe \(\lambda\Pi\)-terms with pairs.
data Expr n where
  -- | Variables: \(x\)
  VarE  :: Name n -> Expr n

  -- | Application: \((t_1 \; t_2)\)
  AppE  :: Expr n -> Expr n -> Expr n
  -- | Abstraction (with patterns): \(\lambda p. t\)
  LamE  :: Pattern n l -> Expr l -> Expr n
  -- | \(\prod\)-types (with patterns): \(\prod_{p : T_1} T_2\)
  PiE   :: Pattern n l -> Expr n -> Expr l -> Expr n

  -- | Pair of terms: \(\langle t_1, t_2 \rangle\)
  PairE :: Expr n -> Expr n -> Expr n
  -- | First projection: \(\pi_1(t)\)
  FirstE :: Expr n -> Expr n
  -- | Second projection: \(\pi_2(t)\)
  SecondE :: Expr n -> Expr n
  -- | Product type (non-dependent): \(T_1 \times T_2\)
  ProductE :: Expr n -> Expr n -> Expr n

  -- | Universe (type of types): \(\mathcal{U}\)
  UniverseE :: Expr n

instance Show (Expr VoidS) where
  show :: Expr 'VoidS -> String
show = Term -> String
forall a. Print a => a -> String
printTree (Term -> String) -> (Expr 'VoidS -> Term) -> Expr 'VoidS -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr 'VoidS -> Term
forall (n :: S). Expr n -> Term
fromFoilTerm'

instance IsString (Expr VoidS) where
  fromString :: String -> Expr 'VoidS
fromString String
input =
    case [Token] -> Err Term
pTerm (String -> [Token]
tokens String
input) of
      Left String
err -> String -> Expr 'VoidS
forall a. HasCallStack => String -> a
error (String
"could not parse λΠ-term: " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
input String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"\n  " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
err)
      Right Term
term -> Term -> Expr 'VoidS
toFoilTermClosed Term
term

-- | Patterns.
data Pattern n l where
  -- | Wildcard pattern: \(_\)
  PatternWildcard :: Pattern n n
  -- | Variable pattern: \(x\)
  PatternVar :: NameBinder n l -> Pattern n l
  -- | Pair pattern: \((p_1, p_2)\)
  PatternPair :: Pattern n i -> Pattern i l -> Pattern n l

instance CoSinkable Pattern where
  coSinkabilityProof :: forall (n :: S) (n' :: S) (l :: S) r.
(Name n -> Name n')
-> Pattern n l
-> (forall (l' :: S). (Name l -> Name l') -> Pattern n' l' -> r)
-> r
coSinkabilityProof Name n -> Name n'
rename Pattern n l
pattern forall (l' :: S). (Name l -> Name l') -> Pattern n' l' -> r
cont =
    case Pattern n l
pattern of
      Pattern n l
PatternWildcard ->
        (Name l -> Name n') -> Pattern n' n' -> r
forall (l' :: S). (Name l -> Name l') -> Pattern n' l' -> r
cont Name n -> Name n'
Name l -> Name n'
rename Pattern n' n'
forall (n :: S). Pattern n n
PatternWildcard
      PatternVar NameBinder n l
x ->
        (Name n -> Name n')
-> NameBinder n l
-> (forall {l' :: S}. (Name l -> Name l') -> NameBinder n' l' -> r)
-> r
forall (n :: S) (n' :: S) (l :: S) r.
(Name n -> Name n')
-> NameBinder n l
-> (forall (l' :: S). (Name l -> Name l') -> NameBinder n' l' -> r)
-> r
forall (pattern :: S -> S -> *) (n :: S) (n' :: S) (l :: S) r.
CoSinkable pattern =>
(Name n -> Name n')
-> pattern n l
-> (forall (l' :: S). (Name l -> Name l') -> pattern n' l' -> r)
-> r
coSinkabilityProof Name n -> Name n'
rename NameBinder n l
x ((forall {l' :: S}. (Name l -> Name l') -> NameBinder n' l' -> r)
 -> r)
-> (forall {l' :: S}. (Name l -> Name l') -> NameBinder n' l' -> r)
-> r
forall a b. (a -> b) -> a -> b
$ \Name l -> Name l'
rename' NameBinder n' l'
x' ->
          (Name l -> Name l') -> Pattern n' l' -> r
forall (l' :: S). (Name l -> Name l') -> Pattern n' l' -> r
cont Name l -> Name l'
rename' (NameBinder n' l' -> Pattern n' l'
forall (n :: S) (l :: S). NameBinder n l -> Pattern n l
PatternVar NameBinder n' l'
x')
      PatternPair Pattern n i
l Pattern i l
r ->
        (Name n -> Name n')
-> Pattern n i
-> (forall {l' :: S}. (Name i -> Name l') -> Pattern n' l' -> r)
-> r
forall (n :: S) (n' :: S) (l :: S) r.
(Name n -> Name n')
-> Pattern n l
-> (forall (l' :: S). (Name l -> Name l') -> Pattern n' l' -> r)
-> r
forall (pattern :: S -> S -> *) (n :: S) (n' :: S) (l :: S) r.
CoSinkable pattern =>
(Name n -> Name n')
-> pattern n l
-> (forall (l' :: S). (Name l -> Name l') -> pattern n' l' -> r)
-> r
coSinkabilityProof Name n -> Name n'
rename Pattern n i
l ((forall {l' :: S}. (Name i -> Name l') -> Pattern n' l' -> r)
 -> r)
-> (forall {l' :: S}. (Name i -> Name l') -> Pattern n' l' -> r)
-> r
forall a b. (a -> b) -> a -> b
$ \Name i -> Name l'
rename' Pattern n' l'
l' ->
          (Name i -> Name l')
-> Pattern i l
-> (forall {l' :: S}. (Name l -> Name l') -> Pattern l' l' -> r)
-> r
forall (n :: S) (n' :: S) (l :: S) r.
(Name n -> Name n')
-> Pattern n l
-> (forall (l' :: S). (Name l -> Name l') -> Pattern n' l' -> r)
-> r
forall (pattern :: S -> S -> *) (n :: S) (n' :: S) (l :: S) r.
CoSinkable pattern =>
(Name n -> Name n')
-> pattern n l
-> (forall (l' :: S). (Name l -> Name l') -> pattern n' l' -> r)
-> r
coSinkabilityProof Name i -> Name l'
rename' Pattern i l
r ((forall {l' :: S}. (Name l -> Name l') -> Pattern l' l' -> r)
 -> r)
-> (forall {l' :: S}. (Name l -> Name l') -> Pattern l' l' -> r)
-> r
forall a b. (a -> b) -> a -> b
$ \Name l -> Name l'
rename'' Pattern l' l'
r' ->
            (Name l -> Name l') -> Pattern n' l' -> r
forall (l' :: S). (Name l -> Name l') -> Pattern n' l' -> r
cont Name l -> Name l'
rename'' (Pattern n' l' -> Pattern l' l' -> Pattern n' l'
forall (n :: S) (l :: S) (l :: S).
Pattern n l -> Pattern l l -> Pattern n l
PatternPair Pattern n' l'
l' Pattern l' l'
r')

  withPattern :: forall (o :: S) (f :: S -> S -> S -> S -> *) (n :: S) (l :: S) r.
Distinct o =>
(forall (x :: S) (y :: S) (z :: S) r'.
 Distinct z =>
 Scope z
 -> NameBinder x y
 -> (forall (z' :: S).
     DExt z z' =>
     f x y z z' -> NameBinder z z' -> r')
 -> r')
-> (forall (x :: S) (z :: S) (z' :: S). DExt z z' => f x x z z')
-> (forall (x :: S) (y :: S) (y' :: S) (z :: S) (z' :: S)
           (z'' :: S).
    (DExt z z', DExt z' z'') =>
    f x y z z' -> f y y' z' z'' -> f x y' z z'')
-> Scope o
-> Pattern n l
-> (forall (o' :: S). DExt o o' => f n l o o' -> Pattern o o' -> r)
-> r
withPattern forall (x :: S) (y :: S) (z :: S) r'.
Distinct z =>
Scope z
-> NameBinder x y
-> (forall (z' :: S).
    DExt z z' =>
    f x y z z' -> NameBinder z z' -> r')
-> r'
withNameBinder forall (x :: S) (z :: S) (z' :: S). DExt z z' => f x x z z'
id' forall (x :: S) (y :: S) (y' :: S) (z :: S) (z' :: S) (z'' :: S).
(DExt z z', DExt z' z'') =>
f x y z z' -> f y y' z' z'' -> f x y' z z''
combine Scope o
scope Pattern n l
pattern forall (o' :: S). DExt o o' => f n l o o' -> Pattern o o' -> r
cont =
    case Pattern n l
pattern of
      Pattern n l
PatternWildcard -> f n l o o -> Pattern o o -> r
forall (o' :: S). DExt o o' => f n l o o' -> Pattern o o' -> r
cont f n l o o
f l l o o
forall (x :: S) (z :: S) (z' :: S). DExt z z' => f x x z z'
id' Pattern o o
forall (n :: S). Pattern n n
PatternWildcard
      PatternVar NameBinder n l
x    -> Scope o
-> NameBinder n l
-> (forall {z' :: S}.
    DExt o z' =>
    f n l o z' -> NameBinder o z' -> r)
-> r
forall (x :: S) (y :: S) (z :: S) r'.
Distinct z =>
Scope z
-> NameBinder x y
-> (forall (z' :: S).
    DExt z z' =>
    f x y z z' -> NameBinder z z' -> r')
-> r'
withNameBinder Scope o
scope NameBinder n l
x ((forall {z' :: S}.
  DExt o z' =>
  f n l o z' -> NameBinder o z' -> r)
 -> r)
-> (forall {z' :: S}.
    DExt o z' =>
    f n l o z' -> NameBinder o z' -> r)
-> r
forall a b. (a -> b) -> a -> b
$ \f n l o z'
f NameBinder o z'
x' ->
        f n l o z' -> Pattern o z' -> r
forall (o' :: S). DExt o o' => f n l o o' -> Pattern o o' -> r
cont f n l o z'
f (NameBinder o z' -> Pattern o z'
forall (n :: S) (l :: S). NameBinder n l -> Pattern n l
PatternVar NameBinder o z'
x')
      PatternPair Pattern n i
l Pattern i l
r -> (forall (x :: S) (y :: S) (z :: S) r'.
 Distinct z =>
 Scope z
 -> NameBinder x y
 -> (forall (z' :: S).
     DExt z z' =>
     f x y z z' -> NameBinder z z' -> r')
 -> r')
-> (forall (x :: S) (z :: S) (z' :: S). DExt z z' => f x x z z')
-> (forall (x :: S) (y :: S) (y' :: S) (z :: S) (z' :: S)
           (z'' :: S).
    (DExt z z', DExt z' z'') =>
    f x y z z' -> f y y' z' z'' -> f x y' z z'')
-> Scope o
-> Pattern n i
-> (forall {o' :: S}. DExt o o' => f n i o o' -> Pattern o o' -> r)
-> r
forall (o :: S) (f :: S -> S -> S -> S -> *) (n :: S) (l :: S) r.
Distinct o =>
(forall (x :: S) (y :: S) (z :: S) r'.
 Distinct z =>
 Scope z
 -> NameBinder x y
 -> (forall (z' :: S).
     DExt z z' =>
     f x y z z' -> NameBinder z z' -> r')
 -> r')
-> (forall (x :: S) (z :: S) (z' :: S). DExt z z' => f x x z z')
-> (forall (x :: S) (y :: S) (y' :: S) (z :: S) (z' :: S)
           (z'' :: S).
    (DExt z z', DExt z' z'') =>
    f x y z z' -> f y y' z' z'' -> f x y' z z'')
-> Scope o
-> Pattern n l
-> (forall (o' :: S). DExt o o' => f n l o o' -> Pattern o o' -> r)
-> r
forall (pattern :: S -> S -> *) (o :: S)
       (f :: S -> S -> S -> S -> *) (n :: S) (l :: S) r.
(CoSinkable pattern, Distinct o) =>
(forall (x :: S) (y :: S) (z :: S) r'.
 Distinct z =>
 Scope z
 -> NameBinder x y
 -> (forall (z' :: S).
     DExt z z' =>
     f x y z z' -> NameBinder z z' -> r')
 -> r')
-> (forall (x :: S) (z :: S) (z' :: S). DExt z z' => f x x z z')
-> (forall (x :: S) (y :: S) (y' :: S) (z :: S) (z' :: S)
           (z'' :: S).
    (DExt z z', DExt z' z'') =>
    f x y z z' -> f y y' z' z'' -> f x y' z z'')
-> Scope o
-> pattern n l
-> (forall (o' :: S). DExt o o' => f n l o o' -> pattern o o' -> r)
-> r
withPattern Scope z
-> NameBinder x y
-> (forall (z' :: S).
    DExt z z' =>
    f x y z z' -> NameBinder z z' -> r')
-> r'
forall (x :: S) (y :: S) (z :: S) r'.
Distinct z =>
Scope z
-> NameBinder x y
-> (forall (z' :: S).
    DExt z z' =>
    f x y z z' -> NameBinder z z' -> r')
-> r'
withNameBinder f x x z z'
forall (x :: S) (z :: S) (z' :: S). DExt z z' => f x x z z'
id' f x y z z' -> f y y' z' z'' -> f x y' z z''
forall (x :: S) (y :: S) (y' :: S) (z :: S) (z' :: S) (z'' :: S).
(DExt z z', DExt z' z'') =>
f x y z z' -> f y y' z' z'' -> f x y' z z''
combine Scope o
scope Pattern n i
l ((forall {o' :: S}. DExt o o' => f n i o o' -> Pattern o o' -> r)
 -> r)
-> (forall {o' :: S}. DExt o o' => f n i o o' -> Pattern o o' -> r)
-> r
forall a b. (a -> b) -> a -> b
$ \f n i o o'
fl Pattern o o'
l' ->
        let scope' :: Scope o'
scope' = Pattern o o' -> Scope o -> Scope o'
forall (n :: S) (pattern :: S -> S -> *) (l :: S).
(Distinct n, CoSinkable pattern) =>
pattern n l -> Scope n -> Scope l
extendScopePattern Pattern o o'
l' Scope o
scope
        in (forall (x :: S) (y :: S) (z :: S) r'.
 Distinct z =>
 Scope z
 -> NameBinder x y
 -> (forall (z' :: S).
     DExt z z' =>
     f x y z z' -> NameBinder z z' -> r')
 -> r')
-> (forall (x :: S) (z :: S) (z' :: S). DExt z z' => f x x z z')
-> (forall (x :: S) (y :: S) (y' :: S) (z :: S) (z' :: S)
           (z'' :: S).
    (DExt z z', DExt z' z'') =>
    f x y z z' -> f y y' z' z'' -> f x y' z z'')
-> Scope o'
-> Pattern i l
-> (forall {o' :: S}.
    DExt o' o' =>
    f i l o' o' -> Pattern o' o' -> r)
-> r
forall (o :: S) (f :: S -> S -> S -> S -> *) (n :: S) (l :: S) r.
Distinct o =>
(forall (x :: S) (y :: S) (z :: S) r'.
 Distinct z =>
 Scope z
 -> NameBinder x y
 -> (forall (z' :: S).
     DExt z z' =>
     f x y z z' -> NameBinder z z' -> r')
 -> r')
-> (forall (x :: S) (z :: S) (z' :: S). DExt z z' => f x x z z')
-> (forall (x :: S) (y :: S) (y' :: S) (z :: S) (z' :: S)
           (z'' :: S).
    (DExt z z', DExt z' z'') =>
    f x y z z' -> f y y' z' z'' -> f x y' z z'')
-> Scope o
-> Pattern n l
-> (forall (o' :: S). DExt o o' => f n l o o' -> Pattern o o' -> r)
-> r
forall (pattern :: S -> S -> *) (o :: S)
       (f :: S -> S -> S -> S -> *) (n :: S) (l :: S) r.
(CoSinkable pattern, Distinct o) =>
(forall (x :: S) (y :: S) (z :: S) r'.
 Distinct z =>
 Scope z
 -> NameBinder x y
 -> (forall (z' :: S).
     DExt z z' =>
     f x y z z' -> NameBinder z z' -> r')
 -> r')
-> (forall (x :: S) (z :: S) (z' :: S). DExt z z' => f x x z z')
-> (forall (x :: S) (y :: S) (y' :: S) (z :: S) (z' :: S)
           (z'' :: S).
    (DExt z z', DExt z' z'') =>
    f x y z z' -> f y y' z' z'' -> f x y' z z'')
-> Scope o
-> pattern n l
-> (forall (o' :: S). DExt o o' => f n l o o' -> pattern o o' -> r)
-> r
withPattern Scope z
-> NameBinder x y
-> (forall (z' :: S).
    DExt z z' =>
    f x y z z' -> NameBinder z z' -> r')
-> r'
forall (x :: S) (y :: S) (z :: S) r'.
Distinct z =>
Scope z
-> NameBinder x y
-> (forall (z' :: S).
    DExt z z' =>
    f x y z z' -> NameBinder z z' -> r')
-> r'
withNameBinder f x x z z'
forall (x :: S) (z :: S) (z' :: S). DExt z z' => f x x z z'
id' f x y z z' -> f y y' z' z'' -> f x y' z z''
forall (x :: S) (y :: S) (y' :: S) (z :: S) (z' :: S) (z'' :: S).
(DExt z z', DExt z' z'') =>
f x y z z' -> f y y' z' z'' -> f x y' z z''
combine Scope o'
scope' Pattern i l
r ((forall {o' :: S}.
  DExt o' o' =>
  f i l o' o' -> Pattern o' o' -> r)
 -> r)
-> (forall {o' :: S}.
    DExt o' o' =>
    f i l o' o' -> Pattern o' o' -> r)
-> r
forall a b. (a -> b) -> a -> b
$ \f i l o' o'
fr Pattern o' o'
r' ->
              f n l o o' -> Pattern o o' -> r
forall (o' :: S). DExt o o' => f n l o o' -> Pattern o o' -> r
cont (f n i o o' -> f i l o' o' -> f n l o o'
forall (x :: S) (y :: S) (y' :: S) (z :: S) (z' :: S) (z'' :: S).
(DExt z z', DExt z' z'') =>
f x y z z' -> f y y' z' z'' -> f x y' z z''
combine f n i o o'
fl f i l o' o'
fr) (Pattern o o' -> Pattern o' o' -> Pattern o o'
forall (n :: S) (l :: S) (l :: S).
Pattern n l -> Pattern l l -> Pattern n l
PatternPair Pattern o o'
l' Pattern o' o'
r')

instance UnifiablePattern Pattern where
  unifyPatterns :: forall (n :: S) (l :: S) (r :: S).
Distinct n =>
Pattern n l -> Pattern n r -> UnifyNameBinders Pattern n l r
unifyPatterns Pattern n l
PatternWildcard Pattern n r
PatternWildcard = NameBinders n l -> UnifyNameBinders Pattern n l l
forall (n :: S) (l :: S) (pattern :: S -> S -> *).
NameBinders n l -> UnifyNameBinders pattern n l l
SameNameBinders NameBinders n n
NameBinders n l
forall (n :: S). NameBinders n n
emptyNameBinders
  unifyPatterns (PatternVar NameBinder n l
x) (PatternVar NameBinder n r
x') = NameBinder n l -> NameBinder n r -> UnifyNameBinders Pattern n l r
forall (i :: S) (l :: S) (r :: S) (pattern :: S -> S -> *).
Distinct i =>
NameBinder i l -> NameBinder i r -> UnifyNameBinders pattern i l r
unifyNameBinders NameBinder n l
x NameBinder n r
x'
  unifyPatterns (PatternPair Pattern n i
l Pattern i l
r) (PatternPair Pattern n i
l' Pattern i r
r') = case (Pattern n i -> DistinctEvidence i
forall (n :: S) (pattern :: S -> S -> *) (l :: S).
(Distinct n, CoSinkable pattern) =>
pattern n l -> DistinctEvidence l
assertDistinct Pattern n i
l, Pattern n i -> DistinctEvidence i
forall (n :: S) (pattern :: S -> S -> *) (l :: S).
(Distinct n, CoSinkable pattern) =>
pattern n l -> DistinctEvidence l
assertDistinct Pattern n i
l') of
    (DistinctEvidence i
Distinct, DistinctEvidence i
Distinct) -> Pattern n i -> Pattern n i -> UnifyNameBinders Pattern n i i
forall (n :: S) (l :: S) (r :: S).
Distinct n =>
Pattern n l -> Pattern n r -> UnifyNameBinders Pattern n l r
forall (pattern :: S -> S -> *) (n :: S) (l :: S) (r :: S).
(UnifiablePattern pattern, Distinct n) =>
pattern n l -> pattern n r -> UnifyNameBinders pattern n l r
unifyPatterns Pattern n i
l Pattern n i
l' UnifyNameBinders Pattern n i i
-> (Pattern i l, Pattern i r) -> UnifyNameBinders Pattern n l r
forall (pattern :: S -> S -> *) (l :: S) (l' :: S) (n :: S)
       (r :: S) (r' :: S).
(UnifiablePattern pattern, Distinct l, Distinct l') =>
UnifyNameBinders pattern n l l'
-> (pattern l r, pattern l' r') -> UnifyNameBinders pattern n r r'
`andThenUnifyPatterns` (Pattern i l
r, Pattern i r
r')
  unifyPatterns Pattern n l
_ Pattern n r
_ = UnifyNameBinders Pattern n l r
forall (pattern :: S -> S -> *) (n :: S) (l :: S) (r :: S).
UnifyNameBinders pattern n l r
NotUnifiable

instance InjectName Expr where
  injectName :: forall (n :: S). Name n -> Expr n
injectName = Name n -> Expr n
forall (n :: S). Name n -> Expr n
VarE

instance RelMonad Name Expr where
  rreturn :: forall (n :: S). Name n -> Expr n
rreturn = Name a -> Expr a
forall (n :: S). Name n -> Expr n
VarE
  rbind :: forall (b :: S) (a :: S).
Distinct b =>
Scope b -> Expr a -> (Name a -> Expr b) -> Expr b
rbind Scope b
scope Expr a
e Name a -> Expr b
subst = case Expr a
e of
    VarE Name a
name -> Name a -> Expr b
subst Name a
name
    AppE Expr a
f Expr a
x -> Expr b -> Expr b -> Expr b
forall (n :: S). Expr n -> Expr n -> Expr n
AppE (Scope b -> Expr a -> (Name a -> Expr b) -> Expr b
forall (b :: S) (a :: S).
Distinct b =>
Scope b -> Expr a -> (Name a -> Expr b) -> Expr b
forall (f :: S -> *) (m :: S -> *) (b :: S) (a :: S).
(RelMonad f m, Distinct b) =>
Scope b -> m a -> (f a -> m b) -> m b
rbind Scope b
scope Expr a
f Name a -> Expr b
subst) (Scope b -> Expr a -> (Name a -> Expr b) -> Expr b
forall (b :: S) (a :: S).
Distinct b =>
Scope b -> Expr a -> (Name a -> Expr b) -> Expr b
forall (f :: S -> *) (m :: S -> *) (b :: S) (a :: S).
(RelMonad f m, Distinct b) =>
Scope b -> m a -> (f a -> m b) -> m b
rbind Scope b
scope Expr a
x Name a -> Expr b
subst)
    LamE Pattern a l
pattern Expr l
body -> Scope b
-> Pattern a l
-> (forall {o' :: S}.
    DExt b o' =>
    ((Name a -> Expr b) -> Name l -> Expr o')
    -> Pattern b o' -> Expr b)
-> Expr b
forall (pattern :: S -> S -> *) (o :: S) (e :: S -> *) (n :: S)
       (l :: S) r.
(CoSinkable pattern, Distinct o, InjectName e, Sinkable e) =>
Scope o
-> pattern n l
-> (forall (o' :: S).
    DExt o o' =>
    ((Name n -> e o) -> Name l -> e o') -> pattern o o' -> r)
-> r
withRefreshedPattern' Scope b
scope Pattern a l
pattern ((forall {o' :: S}.
  DExt b o' =>
  ((Name a -> Expr b) -> Name l -> Expr o')
  -> Pattern b o' -> Expr b)
 -> Expr b)
-> (forall {o' :: S}.
    DExt b o' =>
    ((Name a -> Expr b) -> Name l -> Expr o')
    -> Pattern b o' -> Expr b)
-> Expr b
forall a b. (a -> b) -> a -> b
$ \(Name a -> Expr b) -> Name l -> Expr o'
extendSubst Pattern b o'
pattern' ->
      let subst' :: Name l -> Expr o'
subst' = (Name a -> Expr b) -> Name l -> Expr o'
extendSubst Name a -> Expr b
subst
          scope' :: Scope o'
scope' = Pattern b o' -> Scope b -> Scope o'
forall (n :: S) (pattern :: S -> S -> *) (l :: S).
(Distinct n, CoSinkable pattern) =>
pattern n l -> Scope n -> Scope l
extendScopePattern Pattern b o'
pattern' Scope b
scope
          body' :: Expr o'
body' = Scope o' -> Expr l -> (Name l -> Expr o') -> Expr o'
forall (b :: S) (a :: S).
Distinct b =>
Scope b -> Expr a -> (Name a -> Expr b) -> Expr b
forall (f :: S -> *) (m :: S -> *) (b :: S) (a :: S).
(RelMonad f m, Distinct b) =>
Scope b -> m a -> (f a -> m b) -> m b
rbind Scope o'
scope' Expr l
body Name l -> Expr o'
subst'
      in Pattern b o' -> Expr o' -> Expr b
forall (n :: S) (l :: S). Pattern n l -> Expr l -> Expr n
LamE Pattern b o'
pattern' Expr o'
body'
    PiE Pattern a l
pattern Expr a
a Expr l
b -> Scope b
-> Pattern a l
-> (forall {o' :: S}.
    DExt b o' =>
    ((Name a -> Expr b) -> Name l -> Expr o')
    -> Pattern b o' -> Expr b)
-> Expr b
forall (pattern :: S -> S -> *) (o :: S) (e :: S -> *) (n :: S)
       (l :: S) r.
(CoSinkable pattern, Distinct o, InjectName e, Sinkable e) =>
Scope o
-> pattern n l
-> (forall (o' :: S).
    DExt o o' =>
    ((Name n -> e o) -> Name l -> e o') -> pattern o o' -> r)
-> r
withRefreshedPattern' Scope b
scope Pattern a l
pattern ((forall {o' :: S}.
  DExt b o' =>
  ((Name a -> Expr b) -> Name l -> Expr o')
  -> Pattern b o' -> Expr b)
 -> Expr b)
-> (forall {o' :: S}.
    DExt b o' =>
    ((Name a -> Expr b) -> Name l -> Expr o')
    -> Pattern b o' -> Expr b)
-> Expr b
forall a b. (a -> b) -> a -> b
$ \(Name a -> Expr b) -> Name l -> Expr o'
extendSubst Pattern b o'
pattern' ->
      let subst' :: Name l -> Expr o'
subst' = (Name a -> Expr b) -> Name l -> Expr o'
extendSubst Name a -> Expr b
subst
          scope' :: Scope o'
scope' = Pattern b o' -> Scope b -> Scope o'
forall (n :: S) (pattern :: S -> S -> *) (l :: S).
(Distinct n, CoSinkable pattern) =>
pattern n l -> Scope n -> Scope l
extendScopePattern Pattern b o'
pattern' Scope b
scope
          a' :: Expr b
a' = Scope b -> Expr a -> (Name a -> Expr b) -> Expr b
forall (b :: S) (a :: S).
Distinct b =>
Scope b -> Expr a -> (Name a -> Expr b) -> Expr b
forall (f :: S -> *) (m :: S -> *) (b :: S) (a :: S).
(RelMonad f m, Distinct b) =>
Scope b -> m a -> (f a -> m b) -> m b
rbind Scope b
scope Expr a
a Name a -> Expr b
subst
          b' :: Expr o'
b' = Scope o' -> Expr l -> (Name l -> Expr o') -> Expr o'
forall (b :: S) (a :: S).
Distinct b =>
Scope b -> Expr a -> (Name a -> Expr b) -> Expr b
forall (f :: S -> *) (m :: S -> *) (b :: S) (a :: S).
(RelMonad f m, Distinct b) =>
Scope b -> m a -> (f a -> m b) -> m b
rbind Scope o'
scope' Expr l
b Name l -> Expr o'
subst'
       in Pattern b o' -> Expr b -> Expr o' -> Expr b
forall (n :: S) (l :: S). Pattern n l -> Expr n -> Expr l -> Expr n
PiE Pattern b o'
pattern' Expr b
a' Expr o'
b'
    PairE Expr a
l Expr a
r -> Expr b -> Expr b -> Expr b
forall (n :: S). Expr n -> Expr n -> Expr n
PairE (Scope b -> Expr a -> (Name a -> Expr b) -> Expr b
forall (b :: S) (a :: S).
Distinct b =>
Scope b -> Expr a -> (Name a -> Expr b) -> Expr b
forall (f :: S -> *) (m :: S -> *) (b :: S) (a :: S).
(RelMonad f m, Distinct b) =>
Scope b -> m a -> (f a -> m b) -> m b
rbind Scope b
scope Expr a
l Name a -> Expr b
subst) (Scope b -> Expr a -> (Name a -> Expr b) -> Expr b
forall (b :: S) (a :: S).
Distinct b =>
Scope b -> Expr a -> (Name a -> Expr b) -> Expr b
forall (f :: S -> *) (m :: S -> *) (b :: S) (a :: S).
(RelMonad f m, Distinct b) =>
Scope b -> m a -> (f a -> m b) -> m b
rbind Scope b
scope Expr a
r Name a -> Expr b
subst)
    FirstE Expr a
t -> Expr b -> Expr b
forall (n :: S). Expr n -> Expr n
FirstE (Scope b -> Expr a -> (Name a -> Expr b) -> Expr b
forall (b :: S) (a :: S).
Distinct b =>
Scope b -> Expr a -> (Name a -> Expr b) -> Expr b
forall (f :: S -> *) (m :: S -> *) (b :: S) (a :: S).
(RelMonad f m, Distinct b) =>
Scope b -> m a -> (f a -> m b) -> m b
rbind Scope b
scope Expr a
t Name a -> Expr b
subst)
    SecondE Expr a
t -> Expr b -> Expr b
forall (n :: S). Expr n -> Expr n
SecondE (Scope b -> Expr a -> (Name a -> Expr b) -> Expr b
forall (b :: S) (a :: S).
Distinct b =>
Scope b -> Expr a -> (Name a -> Expr b) -> Expr b
forall (f :: S -> *) (m :: S -> *) (b :: S) (a :: S).
(RelMonad f m, Distinct b) =>
Scope b -> m a -> (f a -> m b) -> m b
rbind Scope b
scope Expr a
t Name a -> Expr b
subst)
    ProductE Expr a
l Expr a
r -> Expr b -> Expr b -> Expr b
forall (n :: S). Expr n -> Expr n -> Expr n
ProductE (Scope b -> Expr a -> (Name a -> Expr b) -> Expr b
forall (b :: S) (a :: S).
Distinct b =>
Scope b -> Expr a -> (Name a -> Expr b) -> Expr b
forall (f :: S -> *) (m :: S -> *) (b :: S) (a :: S).
(RelMonad f m, Distinct b) =>
Scope b -> m a -> (f a -> m b) -> m b
rbind Scope b
scope Expr a
l Name a -> Expr b
subst) (Scope b -> Expr a -> (Name a -> Expr b) -> Expr b
forall (b :: S) (a :: S).
Distinct b =>
Scope b -> Expr a -> (Name a -> Expr b) -> Expr b
forall (f :: S -> *) (m :: S -> *) (b :: S) (a :: S).
(RelMonad f m, Distinct b) =>
Scope b -> m a -> (f a -> m b) -> m b
rbind Scope b
scope Expr a
r Name a -> Expr b
subst)
    Expr a
UniverseE -> Expr b
forall (n :: S). Expr n
UniverseE

-- * Pretty-printing

-- | Default way to print a name using its internal 'Id'.
ppName :: Name n -> String
ppName :: forall (n :: S). Name n -> String
ppName Name n
name = String
"x" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Int -> String
forall a. Show a => a -> String
show (Name n -> Int
forall (l :: S). Name l -> Int
nameId Name n
name)

-- | Pretty-print a \(\lambda\Pi\)-term directly (without converting to raw term).
--
-- >>> ppExpr identity
-- "\955x0. x0"
-- >>> ppExpr (churchN 2)
-- "\955x0. \955x1. x0 (x0 (x1))"
ppExpr :: Expr n -> String
ppExpr :: forall (n :: S). Expr n -> String
ppExpr = \case
  VarE Name n
name     -> Name n -> String
forall (n :: S). Name n -> String
ppName Name n
name
  AppE Expr n
e1 Expr n
e2    -> Expr n -> String
forall (n :: S). Expr n -> String
ppExpr Expr n
e1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" (" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr n -> String
forall (n :: S). Expr n -> String
ppExpr Expr n
e2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
  LamE Pattern n l
pat Expr l
body -> String
"λ" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Pattern n l -> String
forall (n :: S) (l :: S). Pattern n l -> String
ppPattern Pattern n l
pat String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
". " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr l -> String
forall (n :: S). Expr n -> String
ppExpr Expr l
body
  PiE Pattern n l
pat Expr n
a Expr l
b -> String
"Π" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Pattern n l -> String
forall (n :: S) (l :: S). Pattern n l -> String
ppPattern Pattern n l
pat String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" : " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr n -> String
forall (n :: S). Expr n -> String
ppExpr Expr n
a String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"), " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr l -> String
forall (n :: S). Expr n -> String
ppExpr Expr l
b
  PairE Expr n
l Expr n
r -> String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr n -> String
forall (n :: S). Expr n -> String
ppExpr Expr n
l String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"," String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr n -> String
forall (n :: S). Expr n -> String
ppExpr Expr n
r String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
  FirstE Expr n
t -> String
"π₁(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr n -> String
forall (n :: S). Expr n -> String
ppExpr Expr n
t String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
  SecondE Expr n
t -> String
"π₂(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr n -> String
forall (n :: S). Expr n -> String
ppExpr Expr n
t String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
  ProductE Expr n
l Expr n
r -> String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr n -> String
forall (n :: S). Expr n -> String
ppExpr Expr n
l String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" × " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr n -> String
forall (n :: S). Expr n -> String
ppExpr Expr n
r String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
  Expr n
UniverseE -> String
"𝕌"

-- | Pretty-print a pattern in a \(\lambda\Pi\)-term (without converting to raw pattern)..
ppPattern :: Pattern n l -> String
ppPattern :: forall (n :: S) (l :: S). Pattern n l -> String
ppPattern = \case
  Pattern n l
PatternWildcard -> String
"_"
  PatternVar NameBinder n l
x -> Name l -> String
forall (n :: S). Name n -> String
ppName (NameBinder n l -> Name l
forall (n :: S) (l :: S). NameBinder n l -> Name l
nameOf NameBinder n l
x)
  PatternPair Pattern n i
l Pattern i l
r -> String
"(" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Pattern n i -> String
forall (n :: S) (l :: S). Pattern n l -> String
ppPattern Pattern n i
l String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"," String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Pattern i l -> String
forall (n :: S) (l :: S). Pattern n l -> String
ppPattern Pattern i l
r String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
")"

-- | Pretty-print a /closed/ scode-safe \(\lambda\Pi\)-term
-- using BNFC-generated printer (via 'Raw.Term').
printExpr :: Expr VoidS -> String
printExpr :: Expr 'VoidS -> String
printExpr = Term -> String
forall a. Print a => a -> String
printTree (Term -> String) -> (Expr 'VoidS -> Term) -> Expr 'VoidS -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [VarIdent] -> Expr 'VoidS -> Term
fromFoilTermClosed
  [ String -> VarIdent
Raw.VarIdent (String
"x" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Integer -> String
forall a. Show a => a -> String
show Integer
i) | Integer
i <- [Integer
1 :: Integer ..] ]

instance Sinkable Expr where
  sinkabilityProof :: forall (n :: S) (l :: S). (Name n -> Name l) -> Expr n -> Expr l
sinkabilityProof Name n -> Name l
rename (VarE Name n
v) = Name l -> Expr l
forall (n :: S). Name n -> Expr n
VarE (Name n -> Name l
rename Name n
v)
  sinkabilityProof Name n -> Name l
rename (AppE Expr n
f Expr n
e) = Expr l -> Expr l -> Expr l
forall (n :: S). Expr n -> Expr n -> Expr n
AppE ((Name n -> Name l) -> Expr n -> Expr l
forall (n :: S) (l :: S). (Name n -> Name l) -> Expr n -> Expr l
forall (e :: S -> *) (n :: S) (l :: S).
Sinkable e =>
(Name n -> Name l) -> e n -> e l
sinkabilityProof Name n -> Name l
rename Expr n
f) ((Name n -> Name l) -> Expr n -> Expr l
forall (n :: S) (l :: S). (Name n -> Name l) -> Expr n -> Expr l
forall (e :: S -> *) (n :: S) (l :: S).
Sinkable e =>
(Name n -> Name l) -> e n -> e l
sinkabilityProof Name n -> Name l
rename Expr n
e)
  sinkabilityProof Name n -> Name l
rename (LamE Pattern n l
pat Expr l
body) = (Name n -> Name l)
-> Pattern n l
-> (forall {l' :: S}.
    (Name l -> Name l') -> Pattern l l' -> Expr l)
-> Expr l
forall (pattern :: S -> S -> *) (n :: S) (n' :: S) (l :: S) r.
CoSinkable pattern =>
(Name n -> Name n')
-> pattern n l
-> (forall (l' :: S). (Name l -> Name l') -> pattern n' l' -> r)
-> r
extendRenaming Name n -> Name l
rename Pattern n l
pat ((forall {l' :: S}. (Name l -> Name l') -> Pattern l l' -> Expr l)
 -> Expr l)
-> (forall {l' :: S}.
    (Name l -> Name l') -> Pattern l l' -> Expr l)
-> Expr l
forall a b. (a -> b) -> a -> b
$ \Name l -> Name l'
rename' Pattern l l'
pat' ->
    Pattern l l' -> Expr l' -> Expr l
forall (n :: S) (l :: S). Pattern n l -> Expr l -> Expr n
LamE Pattern l l'
pat' ((Name l -> Name l') -> Expr l -> Expr l'
forall (n :: S) (l :: S). (Name n -> Name l) -> Expr n -> Expr l
forall (e :: S -> *) (n :: S) (l :: S).
Sinkable e =>
(Name n -> Name l) -> e n -> e l
sinkabilityProof Name l -> Name l'
rename' Expr l
body)
  sinkabilityProof Name n -> Name l
rename (PiE Pattern n l
pat Expr n
a Expr l
b) =
    (Name n -> Name l)
-> Pattern n l
-> (forall {l' :: S}.
    (Name l -> Name l') -> Pattern l l' -> Expr l)
-> Expr l
forall (pattern :: S -> S -> *) (n :: S) (n' :: S) (l :: S) r.
CoSinkable pattern =>
(Name n -> Name n')
-> pattern n l
-> (forall (l' :: S). (Name l -> Name l') -> pattern n' l' -> r)
-> r
extendRenaming Name n -> Name l
rename Pattern n l
pat ((forall {l' :: S}. (Name l -> Name l') -> Pattern l l' -> Expr l)
 -> Expr l)
-> (forall {l' :: S}.
    (Name l -> Name l') -> Pattern l l' -> Expr l)
-> Expr l
forall a b. (a -> b) -> a -> b
$ \Name l -> Name l'
rename' Pattern l l'
pat' ->
      Pattern l l' -> Expr l -> Expr l' -> Expr l
forall (n :: S) (l :: S). Pattern n l -> Expr n -> Expr l -> Expr n
PiE Pattern l l'
pat' ((Name n -> Name l) -> Expr n -> Expr l
forall (n :: S) (l :: S). (Name n -> Name l) -> Expr n -> Expr l
forall (e :: S -> *) (n :: S) (l :: S).
Sinkable e =>
(Name n -> Name l) -> e n -> e l
sinkabilityProof Name n -> Name l
rename Expr n
a) ((Name l -> Name l') -> Expr l -> Expr l'
forall (n :: S) (l :: S). (Name n -> Name l) -> Expr n -> Expr l
forall (e :: S -> *) (n :: S) (l :: S).
Sinkable e =>
(Name n -> Name l) -> e n -> e l
sinkabilityProof Name l -> Name l'
rename' Expr l
b)
  sinkabilityProof Name n -> Name l
rename (PairE Expr n
l Expr n
r) = Expr l -> Expr l -> Expr l
forall (n :: S). Expr n -> Expr n -> Expr n
PairE ((Name n -> Name l) -> Expr n -> Expr l
forall (n :: S) (l :: S). (Name n -> Name l) -> Expr n -> Expr l
forall (e :: S -> *) (n :: S) (l :: S).
Sinkable e =>
(Name n -> Name l) -> e n -> e l
sinkabilityProof Name n -> Name l
rename Expr n
l) ((Name n -> Name l) -> Expr n -> Expr l
forall (n :: S) (l :: S). (Name n -> Name l) -> Expr n -> Expr l
forall (e :: S -> *) (n :: S) (l :: S).
Sinkable e =>
(Name n -> Name l) -> e n -> e l
sinkabilityProof Name n -> Name l
rename Expr n
r)
  sinkabilityProof Name n -> Name l
rename (FirstE Expr n
t) = Expr l -> Expr l
forall (n :: S). Expr n -> Expr n
FirstE ((Name n -> Name l) -> Expr n -> Expr l
forall (n :: S) (l :: S). (Name n -> Name l) -> Expr n -> Expr l
forall (e :: S -> *) (n :: S) (l :: S).
Sinkable e =>
(Name n -> Name l) -> e n -> e l
sinkabilityProof Name n -> Name l
rename Expr n
t)
  sinkabilityProof Name n -> Name l
rename (SecondE Expr n
t) = Expr l -> Expr l
forall (n :: S). Expr n -> Expr n
SecondE ((Name n -> Name l) -> Expr n -> Expr l
forall (n :: S) (l :: S). (Name n -> Name l) -> Expr n -> Expr l
forall (e :: S -> *) (n :: S) (l :: S).
Sinkable e =>
(Name n -> Name l) -> e n -> e l
sinkabilityProof Name n -> Name l
rename Expr n
t)
  sinkabilityProof Name n -> Name l
rename (ProductE Expr n
l Expr n
r) = Expr l -> Expr l -> Expr l
forall (n :: S). Expr n -> Expr n -> Expr n
ProductE ((Name n -> Name l) -> Expr n -> Expr l
forall (n :: S) (l :: S). (Name n -> Name l) -> Expr n -> Expr l
forall (e :: S -> *) (n :: S) (l :: S).
Sinkable e =>
(Name n -> Name l) -> e n -> e l
sinkabilityProof Name n -> Name l
rename Expr n
l) ((Name n -> Name l) -> Expr n -> Expr l
forall (n :: S) (l :: S). (Name n -> Name l) -> Expr n -> Expr l
forall (e :: S -> *) (n :: S) (l :: S).
Sinkable e =>
(Name n -> Name l) -> e n -> e l
sinkabilityProof Name n -> Name l
rename Expr n
r)
  sinkabilityProof Name n -> Name l
_ Expr n
UniverseE = Expr l
forall (n :: S). Expr n
UniverseE

-- * Substitution

-- | Perform substitution in a \(\lambda\Pi\)-term.
substitute :: Distinct o => Scope o -> Substitution Expr i o -> Expr i -> Expr o
substitute :: forall (o :: S) (i :: S).
Distinct o =>
Scope o -> Substitution Expr i o -> Expr i -> Expr o
substitute Scope o
scope Substitution Expr i o
subst = \case
    VarE Name i
name -> Substitution Expr i o -> Name i -> Expr o
forall (e :: S -> *) (i :: S) (o :: S).
InjectName e =>
Substitution e i o -> Name i -> e o
lookupSubst Substitution Expr i o
subst Name i
name
    AppE Expr i
f Expr i
x -> Expr o -> Expr o -> Expr o
forall (n :: S). Expr n -> Expr n -> Expr n
AppE (Scope o -> Substitution Expr i o -> Expr i -> Expr o
forall (o :: S) (i :: S).
Distinct o =>
Scope o -> Substitution Expr i o -> Expr i -> Expr o
substitute Scope o
scope Substitution Expr i o
subst Expr i
f) (Scope o -> Substitution Expr i o -> Expr i -> Expr o
forall (o :: S) (i :: S).
Distinct o =>
Scope o -> Substitution Expr i o -> Expr i -> Expr o
substitute Scope o
scope Substitution Expr i o
subst Expr i
x)
    LamE Pattern i l
pattern Expr l
body -> Scope o
-> Pattern i l
-> (forall {o' :: S}.
    DExt o o' =>
    (Substitution Expr i o -> Substitution Expr l o')
    -> Pattern o o' -> Expr o)
-> Expr o
forall (o :: S) (pattern :: S -> S -> *) (e :: S -> *) (n :: S)
       (l :: S) r.
(Distinct o, CoSinkable pattern, Sinkable e, InjectName e) =>
Scope o
-> pattern n l
-> (forall (o' :: S).
    DExt o o' =>
    (Substitution e n o -> Substitution e l o') -> pattern o o' -> r)
-> r
withRefreshedPattern Scope o
scope Pattern i l
pattern ((forall {o' :: S}.
  DExt o o' =>
  (Substitution Expr i o -> Substitution Expr l o')
  -> Pattern o o' -> Expr o)
 -> Expr o)
-> (forall {o' :: S}.
    DExt o o' =>
    (Substitution Expr i o -> Substitution Expr l o')
    -> Pattern o o' -> Expr o)
-> Expr o
forall a b. (a -> b) -> a -> b
$ \Substitution Expr i o -> Substitution Expr l o'
extendSubst Pattern o o'
pattern' ->
      let subst' :: Substitution Expr l o'
subst' = Substitution Expr i o -> Substitution Expr l o'
extendSubst Substitution Expr i o
subst
          scope' :: Scope o'
scope' = Pattern o o' -> Scope o -> Scope o'
forall (n :: S) (pattern :: S -> S -> *) (l :: S).
(Distinct n, CoSinkable pattern) =>
pattern n l -> Scope n -> Scope l
extendScopePattern Pattern o o'
pattern' Scope o
scope
          body' :: Expr o'
body' = Scope o' -> Substitution Expr l o' -> Expr l -> Expr o'
forall (o :: S) (i :: S).
Distinct o =>
Scope o -> Substitution Expr i o -> Expr i -> Expr o
substitute Scope o'
scope' Substitution Expr l o'
subst' Expr l
body
       in Pattern o o' -> Expr o' -> Expr o
forall (n :: S) (l :: S). Pattern n l -> Expr l -> Expr n
LamE Pattern o o'
pattern' Expr o'
body'
    PiE Pattern i l
pattern Expr i
a Expr l
b -> Scope o
-> Pattern i l
-> (forall {o' :: S}.
    DExt o o' =>
    (Substitution Expr i o -> Substitution Expr l o')
    -> Pattern o o' -> Expr o)
-> Expr o
forall (o :: S) (pattern :: S -> S -> *) (e :: S -> *) (n :: S)
       (l :: S) r.
(Distinct o, CoSinkable pattern, Sinkable e, InjectName e) =>
Scope o
-> pattern n l
-> (forall (o' :: S).
    DExt o o' =>
    (Substitution e n o -> Substitution e l o') -> pattern o o' -> r)
-> r
withRefreshedPattern Scope o
scope Pattern i l
pattern ((forall {o' :: S}.
  DExt o o' =>
  (Substitution Expr i o -> Substitution Expr l o')
  -> Pattern o o' -> Expr o)
 -> Expr o)
-> (forall {o' :: S}.
    DExt o o' =>
    (Substitution Expr i o -> Substitution Expr l o')
    -> Pattern o o' -> Expr o)
-> Expr o
forall a b. (a -> b) -> a -> b
$ \Substitution Expr i o -> Substitution Expr l o'
extendSubst Pattern o o'
pattern' ->
      let subst' :: Substitution Expr l o'
subst' = Substitution Expr i o -> Substitution Expr l o'
extendSubst Substitution Expr i o
subst
          scope' :: Scope o'
scope' = Pattern o o' -> Scope o -> Scope o'
forall (n :: S) (pattern :: S -> S -> *) (l :: S).
(Distinct n, CoSinkable pattern) =>
pattern n l -> Scope n -> Scope l
extendScopePattern Pattern o o'
pattern' Scope o
scope
          a' :: Expr o
a' = Scope o -> Substitution Expr i o -> Expr i -> Expr o
forall (o :: S) (i :: S).
Distinct o =>
Scope o -> Substitution Expr i o -> Expr i -> Expr o
substitute Scope o
scope Substitution Expr i o
subst Expr i
a
          b' :: Expr o'
b' = Scope o' -> Substitution Expr l o' -> Expr l -> Expr o'
forall (o :: S) (i :: S).
Distinct o =>
Scope o -> Substitution Expr i o -> Expr i -> Expr o
substitute Scope o'
scope' Substitution Expr l o'
subst' Expr l
b
       in Pattern o o' -> Expr o -> Expr o' -> Expr o
forall (n :: S) (l :: S). Pattern n l -> Expr n -> Expr l -> Expr n
PiE Pattern o o'
pattern' Expr o
a' Expr o'
b'
    PairE Expr i
l Expr i
r -> Expr o -> Expr o -> Expr o
forall (n :: S). Expr n -> Expr n -> Expr n
PairE (Scope o -> Substitution Expr i o -> Expr i -> Expr o
forall (o :: S) (i :: S).
Distinct o =>
Scope o -> Substitution Expr i o -> Expr i -> Expr o
substitute Scope o
scope Substitution Expr i o
subst Expr i
l) (Scope o -> Substitution Expr i o -> Expr i -> Expr o
forall (o :: S) (i :: S).
Distinct o =>
Scope o -> Substitution Expr i o -> Expr i -> Expr o
substitute Scope o
scope Substitution Expr i o
subst Expr i
r)
    FirstE Expr i
t -> Expr o -> Expr o
forall (n :: S). Expr n -> Expr n
FirstE (Scope o -> Substitution Expr i o -> Expr i -> Expr o
forall (o :: S) (i :: S).
Distinct o =>
Scope o -> Substitution Expr i o -> Expr i -> Expr o
substitute Scope o
scope Substitution Expr i o
subst Expr i
t)
    SecondE Expr i
t -> Expr o -> Expr o
forall (n :: S). Expr n -> Expr n
SecondE (Scope o -> Substitution Expr i o -> Expr i -> Expr o
forall (o :: S) (i :: S).
Distinct o =>
Scope o -> Substitution Expr i o -> Expr i -> Expr o
substitute Scope o
scope Substitution Expr i o
subst Expr i
t)
    ProductE Expr i
l Expr i
r -> Expr o -> Expr o -> Expr o
forall (n :: S). Expr n -> Expr n -> Expr n
ProductE (Scope o -> Substitution Expr i o -> Expr i -> Expr o
forall (o :: S) (i :: S).
Distinct o =>
Scope o -> Substitution Expr i o -> Expr i -> Expr o
substitute Scope o
scope Substitution Expr i o
subst Expr i
l) (Scope o -> Substitution Expr i o -> Expr i -> Expr o
forall (o :: S) (i :: S).
Distinct o =>
Scope o -> Substitution Expr i o -> Expr i -> Expr o
substitute Scope o
scope Substitution Expr i o
subst Expr i
r)
    Expr i
UniverseE -> Expr o
forall (n :: S). Expr n
UniverseE

-- | Perform substitution in a \(\lambda\Pi\)-term
-- and normalize binders in the process.
substituteRefresh :: Distinct o => Scope o -> Substitution Expr i o -> Expr i -> Expr o
substituteRefresh :: forall (o :: S) (i :: S).
Distinct o =>
Scope o -> Substitution Expr i o -> Expr i -> Expr o
substituteRefresh Scope o
scope Substitution Expr i o
subst = \case
    VarE Name i
name -> Substitution Expr i o -> Name i -> Expr o
forall (e :: S -> *) (i :: S) (o :: S).
InjectName e =>
Substitution e i o -> Name i -> e o
lookupSubst Substitution Expr i o
subst Name i
name
    AppE Expr i
f Expr i
x -> Expr o -> Expr o -> Expr o
forall (n :: S). Expr n -> Expr n -> Expr n
AppE (Scope o -> Substitution Expr i o -> Expr i -> Expr o
forall (o :: S) (i :: S).
Distinct o =>
Scope o -> Substitution Expr i o -> Expr i -> Expr o
substituteRefresh Scope o
scope Substitution Expr i o
subst Expr i
f) (Scope o -> Substitution Expr i o -> Expr i -> Expr o
forall (o :: S) (i :: S).
Distinct o =>
Scope o -> Substitution Expr i o -> Expr i -> Expr o
substituteRefresh Scope o
scope Substitution Expr i o
subst Expr i
x)
    LamE Pattern i l
pattern Expr l
body -> Scope o
-> Pattern i l
-> (forall {o' :: S}.
    DExt o o' =>
    (Substitution Expr i o -> Substitution Expr l o')
    -> Pattern o o' -> Expr o)
-> Expr o
forall (o :: S) (pattern :: S -> S -> *) (e :: S -> *) (n :: S)
       (l :: S) r.
(Distinct o, CoSinkable pattern, Sinkable e, InjectName e) =>
Scope o
-> pattern n l
-> (forall (o' :: S).
    DExt o o' =>
    (Substitution e n o -> Substitution e l o') -> pattern o o' -> r)
-> r
withFreshPattern Scope o
scope Pattern i l
pattern ((forall {o' :: S}.
  DExt o o' =>
  (Substitution Expr i o -> Substitution Expr l o')
  -> Pattern o o' -> Expr o)
 -> Expr o)
-> (forall {o' :: S}.
    DExt o o' =>
    (Substitution Expr i o -> Substitution Expr l o')
    -> Pattern o o' -> Expr o)
-> Expr o
forall a b. (a -> b) -> a -> b
$ \Substitution Expr i o -> Substitution Expr l o'
extendSubst Pattern o o'
pattern' ->
      let subst' :: Substitution Expr l o'
subst' = Substitution Expr i o -> Substitution Expr l o'
extendSubst Substitution Expr i o
subst
          scope' :: Scope o'
scope' = Pattern o o' -> Scope o -> Scope o'
forall (n :: S) (pattern :: S -> S -> *) (l :: S).
(Distinct n, CoSinkable pattern) =>
pattern n l -> Scope n -> Scope l
extendScopePattern Pattern o o'
pattern' Scope o
scope
          body' :: Expr o'
body' = Scope o' -> Substitution Expr l o' -> Expr l -> Expr o'
forall (o :: S) (i :: S).
Distinct o =>
Scope o -> Substitution Expr i o -> Expr i -> Expr o
substituteRefresh Scope o'
scope' Substitution Expr l o'
subst' Expr l
body
       in Pattern o o' -> Expr o' -> Expr o
forall (n :: S) (l :: S). Pattern n l -> Expr l -> Expr n
LamE Pattern o o'
pattern' Expr o'
body'
    PiE Pattern i l
pattern Expr i
a Expr l
b -> Scope o
-> Pattern i l
-> (forall {o' :: S}.
    DExt o o' =>
    (Substitution Expr i o -> Substitution Expr l o')
    -> Pattern o o' -> Expr o)
-> Expr o
forall (o :: S) (pattern :: S -> S -> *) (e :: S -> *) (n :: S)
       (l :: S) r.
(Distinct o, CoSinkable pattern, Sinkable e, InjectName e) =>
Scope o
-> pattern n l
-> (forall (o' :: S).
    DExt o o' =>
    (Substitution e n o -> Substitution e l o') -> pattern o o' -> r)
-> r
withFreshPattern Scope o
scope Pattern i l
pattern ((forall {o' :: S}.
  DExt o o' =>
  (Substitution Expr i o -> Substitution Expr l o')
  -> Pattern o o' -> Expr o)
 -> Expr o)
-> (forall {o' :: S}.
    DExt o o' =>
    (Substitution Expr i o -> Substitution Expr l o')
    -> Pattern o o' -> Expr o)
-> Expr o
forall a b. (a -> b) -> a -> b
$ \Substitution Expr i o -> Substitution Expr l o'
extendSubst Pattern o o'
pattern' ->
      let subst' :: Substitution Expr l o'
subst' = Substitution Expr i o -> Substitution Expr l o'
extendSubst Substitution Expr i o
subst
          scope' :: Scope o'
scope' = Pattern o o' -> Scope o -> Scope o'
forall (n :: S) (pattern :: S -> S -> *) (l :: S).
(Distinct n, CoSinkable pattern) =>
pattern n l -> Scope n -> Scope l
extendScopePattern Pattern o o'
pattern' Scope o
scope
          a' :: Expr o
a' = Scope o -> Substitution Expr i o -> Expr i -> Expr o
forall (o :: S) (i :: S).
Distinct o =>
Scope o -> Substitution Expr i o -> Expr i -> Expr o
substituteRefresh Scope o
scope Substitution Expr i o
subst Expr i
a
          b' :: Expr o'
b' = Scope o' -> Substitution Expr l o' -> Expr l -> Expr o'
forall (o :: S) (i :: S).
Distinct o =>
Scope o -> Substitution Expr i o -> Expr i -> Expr o
substituteRefresh Scope o'
scope' Substitution Expr l o'
subst' Expr l
b
       in Pattern o o' -> Expr o -> Expr o' -> Expr o
forall (n :: S) (l :: S). Pattern n l -> Expr n -> Expr l -> Expr n
PiE Pattern o o'
pattern' Expr o
a' Expr o'
b'
    PairE Expr i
l Expr i
r -> Expr o -> Expr o -> Expr o
forall (n :: S). Expr n -> Expr n -> Expr n
PairE (Scope o -> Substitution Expr i o -> Expr i -> Expr o
forall (o :: S) (i :: S).
Distinct o =>
Scope o -> Substitution Expr i o -> Expr i -> Expr o
substituteRefresh Scope o
scope Substitution Expr i o
subst Expr i
l) (Scope o -> Substitution Expr i o -> Expr i -> Expr o
forall (o :: S) (i :: S).
Distinct o =>
Scope o -> Substitution Expr i o -> Expr i -> Expr o
substituteRefresh Scope o
scope Substitution Expr i o
subst Expr i
r)
    FirstE Expr i
t -> Expr o -> Expr o
forall (n :: S). Expr n -> Expr n
FirstE (Scope o -> Substitution Expr i o -> Expr i -> Expr o
forall (o :: S) (i :: S).
Distinct o =>
Scope o -> Substitution Expr i o -> Expr i -> Expr o
substituteRefresh Scope o
scope Substitution Expr i o
subst Expr i
t)
    SecondE Expr i
t -> Expr o -> Expr o
forall (n :: S). Expr n -> Expr n
SecondE (Scope o -> Substitution Expr i o -> Expr i -> Expr o
forall (o :: S) (i :: S).
Distinct o =>
Scope o -> Substitution Expr i o -> Expr i -> Expr o
substituteRefresh Scope o
scope Substitution Expr i o
subst Expr i
t)
    ProductE Expr i
l Expr i
r -> Expr o -> Expr o -> Expr o
forall (n :: S). Expr n -> Expr n -> Expr n
ProductE (Scope o -> Substitution Expr i o -> Expr i -> Expr o
forall (o :: S) (i :: S).
Distinct o =>
Scope o -> Substitution Expr i o -> Expr i -> Expr o
substituteRefresh Scope o
scope Substitution Expr i o
subst Expr i
l) (Scope o -> Substitution Expr i o -> Expr i -> Expr o
forall (o :: S) (i :: S).
Distinct o =>
Scope o -> Substitution Expr i o -> Expr i -> Expr o
substituteRefresh Scope o
scope Substitution Expr i o
subst Expr i
r)
    Expr i
UniverseE -> Expr o
forall (n :: S). Expr n
UniverseE

-- * Conversion

-- ** From raw to foil

-- | Convert a raw pattern into a scope-safe one.
toFoilPattern
  :: Distinct n
  => Scope n                    -- ^ Outer scope (outside of pattern binding).
  -> Map Raw.VarIdent (Name n)  -- ^ Mapping for variable names (to be extended with pattern).
  -> Raw.Pattern                -- ^ Raw pattern.
  -> (forall l. DExt n l => Pattern n l -> Map Raw.VarIdent (Name l) -> r)
  -- ^ A continuation, accepting a scope-safe pattern and an updated variable mapping.
  -> r
toFoilPattern :: forall (n :: S) r.
Distinct n =>
Scope n
-> Map VarIdent (Name n)
-> Pattern
-> (forall (l :: S).
    DExt n l =>
    Pattern n l -> Map VarIdent (Name l) -> r)
-> r
toFoilPattern Scope n
scope Map VarIdent (Name n)
env Pattern
pattern forall (l :: S).
DExt n l =>
Pattern n l -> Map VarIdent (Name l) -> r
cont =
  case Pattern
pattern of
    Raw.PatternWildcard BNFC'Position
_loc -> Pattern n n -> Map VarIdent (Name n) -> r
forall (l :: S).
DExt n l =>
Pattern n l -> Map VarIdent (Name l) -> r
cont Pattern n n
forall (n :: S). Pattern n n
PatternWildcard Map VarIdent (Name n)
env
    Raw.PatternVar BNFC'Position
_loc VarIdent
x -> Scope n -> (forall {l :: S}. DExt n l => NameBinder n l -> r) -> r
forall (n :: S) r.
Distinct n =>
Scope n -> (forall (l :: S). DExt n l => NameBinder n l -> r) -> r
withFresh Scope n
scope ((forall {l :: S}. DExt n l => NameBinder n l -> r) -> r)
-> (forall {l :: S}. DExt n l => NameBinder n l -> r) -> r
forall a b. (a -> b) -> a -> b
$ \NameBinder n l
binder ->
      Pattern n l -> Map VarIdent (Name l) -> r
forall (l :: S).
DExt n l =>
Pattern n l -> Map VarIdent (Name l) -> r
cont (NameBinder n l -> Pattern n l
forall (n :: S) (l :: S). NameBinder n l -> Pattern n l
PatternVar NameBinder n l
binder) (VarIdent
-> Name l -> Map VarIdent (Name l) -> Map VarIdent (Name l)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert VarIdent
x (NameBinder n l -> Name l
forall (n :: S) (l :: S). NameBinder n l -> Name l
nameOf NameBinder n l
binder) (Name n -> Name l
forall (e :: S -> *) (n :: S) (l :: S).
(Sinkable e, DExt n l) =>
e n -> e l
sink (Name n -> Name l)
-> Map VarIdent (Name n) -> Map VarIdent (Name l)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map VarIdent (Name n)
env))
    Raw.PatternPair BNFC'Position
_loc Pattern
l Pattern
r ->
      Scope n
-> Map VarIdent (Name n)
-> Pattern
-> (forall (l :: S).
    DExt n l =>
    Pattern n l -> Map VarIdent (Name l) -> r)
-> r
forall (n :: S) r.
Distinct n =>
Scope n
-> Map VarIdent (Name n)
-> Pattern
-> (forall (l :: S).
    DExt n l =>
    Pattern n l -> Map VarIdent (Name l) -> r)
-> r
toFoilPattern Scope n
scope Map VarIdent (Name n)
env Pattern
l ((forall (l :: S).
  DExt n l =>
  Pattern n l -> Map VarIdent (Name l) -> r)
 -> r)
-> (forall (l :: S).
    DExt n l =>
    Pattern n l -> Map VarIdent (Name l) -> r)
-> r
forall a b. (a -> b) -> a -> b
$ \Pattern n l
l' Map VarIdent (Name l)
env' ->
        let scope' :: Scope l
scope' = Pattern n l -> Scope n -> Scope l
forall (n :: S) (pattern :: S -> S -> *) (l :: S).
(Distinct n, CoSinkable pattern) =>
pattern n l -> Scope n -> Scope l
extendScopePattern Pattern n l
l' Scope n
scope
         in Scope l
-> Map VarIdent (Name l)
-> Pattern
-> (forall {l :: S}.
    DExt l l =>
    Pattern l l -> Map VarIdent (Name l) -> r)
-> r
forall (n :: S) r.
Distinct n =>
Scope n
-> Map VarIdent (Name n)
-> Pattern
-> (forall (l :: S).
    DExt n l =>
    Pattern n l -> Map VarIdent (Name l) -> r)
-> r
toFoilPattern Scope l
scope' Map VarIdent (Name l)
env' Pattern
r ((forall {l :: S}.
  DExt l l =>
  Pattern l l -> Map VarIdent (Name l) -> r)
 -> r)
-> (forall {l :: S}.
    DExt l l =>
    Pattern l l -> Map VarIdent (Name l) -> r)
-> r
forall a b. (a -> b) -> a -> b
$ \Pattern l l
r' Map VarIdent (Name l)
env'' ->
              Pattern n l -> Map VarIdent (Name l) -> r
forall (l :: S).
DExt n l =>
Pattern n l -> Map VarIdent (Name l) -> r
cont (Pattern n l -> Pattern l l -> Pattern n l
forall (n :: S) (l :: S) (l :: S).
Pattern n l -> Pattern l l -> Pattern n l
PatternPair Pattern n l
l' Pattern l l
r') Map VarIdent (Name l)
env''

-- | Convert a raw term into a scope-safe \(\lambda\Pi\)-term.
toFoilTerm
  :: Distinct n
  => Scope n                    -- ^ Target scope.
  -> Map Raw.VarIdent (Name n)  -- ^ Mapping for variable names (to be extended with pattern).
  -> Raw.Term                   -- ^ A raw term.
  -> Expr n
toFoilTerm :: forall (n :: S).
Distinct n =>
Scope n -> Map VarIdent (Name n) -> Term -> Expr n
toFoilTerm Scope n
scope Map VarIdent (Name n)
env = \case
  Raw.Var BNFC'Position
_loc VarIdent
x ->
    case VarIdent -> Map VarIdent (Name n) -> Maybe (Name n)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup VarIdent
x Map VarIdent (Name n)
env of
      Just Name n
name -> Name n -> Expr n
forall (n :: S). Name n -> Expr n
VarE Name n
name
      Maybe (Name n)
Nothing   -> String -> Expr n
forall a. HasCallStack => String -> a
error (String -> Expr n) -> String -> Expr n
forall a b. (a -> b) -> a -> b
$ String
"unknown free variable: " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> VarIdent -> String
forall a. Show a => a -> String
show VarIdent
x

  Raw.App BNFC'Position
_loc Term
t1 Term
t2 ->
    Expr n -> Expr n -> Expr n
forall (n :: S). Expr n -> Expr n -> Expr n
AppE (Scope n -> Map VarIdent (Name n) -> Term -> Expr n
forall (n :: S).
Distinct n =>
Scope n -> Map VarIdent (Name n) -> Term -> Expr n
toFoilTerm Scope n
scope Map VarIdent (Name n)
env Term
t1) (Scope n -> Map VarIdent (Name n) -> Term -> Expr n
forall (n :: S).
Distinct n =>
Scope n -> Map VarIdent (Name n) -> Term -> Expr n
toFoilTerm Scope n
scope Map VarIdent (Name n)
env Term
t2)

  Raw.Lam BNFC'Position
_loc Pattern
pattern (Raw.AScopedTerm BNFC'Position
_loc' Term
body) ->
    Scope n
-> Map VarIdent (Name n)
-> Pattern
-> (forall {l :: S}.
    DExt n l =>
    Pattern n l -> Map VarIdent (Name l) -> Expr n)
-> Expr n
forall (n :: S) r.
Distinct n =>
Scope n
-> Map VarIdent (Name n)
-> Pattern
-> (forall (l :: S).
    DExt n l =>
    Pattern n l -> Map VarIdent (Name l) -> r)
-> r
toFoilPattern Scope n
scope Map VarIdent (Name n)
env Pattern
pattern ((forall {l :: S}.
  DExt n l =>
  Pattern n l -> Map VarIdent (Name l) -> Expr n)
 -> Expr n)
-> (forall {l :: S}.
    DExt n l =>
    Pattern n l -> Map VarIdent (Name l) -> Expr n)
-> Expr n
forall a b. (a -> b) -> a -> b
$ \Pattern n l
pattern' Map VarIdent (Name l)
env' ->
      let scope' :: Scope l
scope' = Pattern n l -> Scope n -> Scope l
forall (n :: S) (pattern :: S -> S -> *) (l :: S).
(Distinct n, CoSinkable pattern) =>
pattern n l -> Scope n -> Scope l
extendScopePattern Pattern n l
pattern' Scope n
scope
       in Pattern n l -> Expr l -> Expr n
forall (n :: S) (l :: S). Pattern n l -> Expr l -> Expr n
LamE Pattern n l
pattern' (Scope l -> Map VarIdent (Name l) -> Term -> Expr l
forall (n :: S).
Distinct n =>
Scope n -> Map VarIdent (Name n) -> Term -> Expr n
toFoilTerm Scope l
scope' Map VarIdent (Name l)
env' Term
body)

  Raw.Pi BNFC'Position
_loc Pattern
pattern Term
a (Raw.AScopedTerm BNFC'Position
_loc' Term
b) ->
    Scope n
-> Map VarIdent (Name n)
-> Pattern
-> (forall {l :: S}.
    DExt n l =>
    Pattern n l -> Map VarIdent (Name l) -> Expr n)
-> Expr n
forall (n :: S) r.
Distinct n =>
Scope n
-> Map VarIdent (Name n)
-> Pattern
-> (forall (l :: S).
    DExt n l =>
    Pattern n l -> Map VarIdent (Name l) -> r)
-> r
toFoilPattern Scope n
scope Map VarIdent (Name n)
env Pattern
pattern ((forall {l :: S}.
  DExt n l =>
  Pattern n l -> Map VarIdent (Name l) -> Expr n)
 -> Expr n)
-> (forall {l :: S}.
    DExt n l =>
    Pattern n l -> Map VarIdent (Name l) -> Expr n)
-> Expr n
forall a b. (a -> b) -> a -> b
$ \Pattern n l
pattern' Map VarIdent (Name l)
env' ->
      let scope' :: Scope l
scope' = Pattern n l -> Scope n -> Scope l
forall (n :: S) (pattern :: S -> S -> *) (l :: S).
(Distinct n, CoSinkable pattern) =>
pattern n l -> Scope n -> Scope l
extendScopePattern Pattern n l
pattern' Scope n
scope
       in Pattern n l -> Expr n -> Expr l -> Expr n
forall (n :: S) (l :: S). Pattern n l -> Expr n -> Expr l -> Expr n
PiE Pattern n l
pattern' (Scope n -> Map VarIdent (Name n) -> Term -> Expr n
forall (n :: S).
Distinct n =>
Scope n -> Map VarIdent (Name n) -> Term -> Expr n
toFoilTerm Scope n
scope Map VarIdent (Name n)
env Term
a) (Scope l -> Map VarIdent (Name l) -> Term -> Expr l
forall (n :: S).
Distinct n =>
Scope n -> Map VarIdent (Name n) -> Term -> Expr n
toFoilTerm Scope l
scope' Map VarIdent (Name l)
env' Term
b)

  Raw.Pair BNFC'Position
_loc Term
t1 Term
t2 ->
    Expr n -> Expr n -> Expr n
forall (n :: S). Expr n -> Expr n -> Expr n
PairE (Scope n -> Map VarIdent (Name n) -> Term -> Expr n
forall (n :: S).
Distinct n =>
Scope n -> Map VarIdent (Name n) -> Term -> Expr n
toFoilTerm Scope n
scope Map VarIdent (Name n)
env Term
t1) (Scope n -> Map VarIdent (Name n) -> Term -> Expr n
forall (n :: S).
Distinct n =>
Scope n -> Map VarIdent (Name n) -> Term -> Expr n
toFoilTerm Scope n
scope Map VarIdent (Name n)
env Term
t2)
  Raw.First BNFC'Position
_loc Term
t ->
    Expr n -> Expr n
forall (n :: S). Expr n -> Expr n
FirstE (Scope n -> Map VarIdent (Name n) -> Term -> Expr n
forall (n :: S).
Distinct n =>
Scope n -> Map VarIdent (Name n) -> Term -> Expr n
toFoilTerm Scope n
scope Map VarIdent (Name n)
env Term
t)
  Raw.Second BNFC'Position
_loc Term
t ->
    Expr n -> Expr n
forall (n :: S). Expr n -> Expr n
SecondE (Scope n -> Map VarIdent (Name n) -> Term -> Expr n
forall (n :: S).
Distinct n =>
Scope n -> Map VarIdent (Name n) -> Term -> Expr n
toFoilTerm Scope n
scope Map VarIdent (Name n)
env Term
t)

  Raw.Product BNFC'Position
_loc Term
t1 Term
t2 ->
    Expr n -> Expr n -> Expr n
forall (n :: S). Expr n -> Expr n -> Expr n
ProductE (Scope n -> Map VarIdent (Name n) -> Term -> Expr n
forall (n :: S).
Distinct n =>
Scope n -> Map VarIdent (Name n) -> Term -> Expr n
toFoilTerm Scope n
scope Map VarIdent (Name n)
env Term
t1) (Scope n -> Map VarIdent (Name n) -> Term -> Expr n
forall (n :: S).
Distinct n =>
Scope n -> Map VarIdent (Name n) -> Term -> Expr n
toFoilTerm Scope n
scope Map VarIdent (Name n)
env Term
t2)

  Raw.Universe BNFC'Position
_loc -> Expr n
forall (n :: S). Expr n
UniverseE

-- | Convert a raw term into a closed scope-safe term.
toFoilTermClosed :: Raw.Term -> Expr VoidS
toFoilTermClosed :: Term -> Expr 'VoidS
toFoilTermClosed = Scope 'VoidS -> Map VarIdent (Name 'VoidS) -> Term -> Expr 'VoidS
forall (n :: S).
Distinct n =>
Scope n -> Map VarIdent (Name n) -> Term -> Expr n
toFoilTerm Scope 'VoidS
emptyScope Map VarIdent (Name 'VoidS)
forall k a. Map k a
Map.empty

-- ** From foil to raw

-- | Convert a scope-safe pattern into a raw pattern.
fromFoilPattern
  :: [Raw.VarIdent]         -- ^ A stream of fresh variable identifiers.
  -> NameMap n Raw.VarIdent -- ^ A /total/ mapping for names in scope @n@.
  -> Pattern n l            -- ^ A scope-safe pattern that extends scope @n@ into scope @l@.
  -> ([Raw.VarIdent] -> NameMap l Raw.VarIdent -> Raw.Pattern -> r)
    -- ^ A continutation, accepting (smaller) stream of fresh variable identifiers, a mapping for the inner scope, and a raw pattern.
  -> r
fromFoilPattern :: forall (n :: S) (l :: S) r.
[VarIdent]
-> NameMap n VarIdent
-> Pattern n l
-> ([VarIdent] -> NameMap l VarIdent -> Pattern -> r)
-> r
fromFoilPattern [VarIdent]
freshVars NameMap n VarIdent
env Pattern n l
pattern [VarIdent] -> NameMap l VarIdent -> Pattern -> r
cont =
  case Pattern n l
pattern of
    Pattern n l
PatternWildcard -> [VarIdent] -> NameMap l VarIdent -> Pattern -> r
cont [VarIdent]
freshVars NameMap n VarIdent
NameMap l VarIdent
env (BNFC'Position -> Pattern
forall a. a -> Pattern' a
Raw.PatternWildcard BNFC'Position
forall {a}. a
loc)
    PatternVar NameBinder n l
z ->
      case [VarIdent]
freshVars of
        []   -> String -> r
forall a. HasCallStack => String -> a
error String
"not enough fresh variables!"
        VarIdent
x:[VarIdent]
xs -> [VarIdent] -> NameMap l VarIdent -> Pattern -> r
cont [VarIdent]
xs (NameBinder n l
-> VarIdent -> NameMap n VarIdent -> NameMap l VarIdent
forall (n :: S) (l :: S) a.
NameBinder n l -> a -> NameMap n a -> NameMap l a
addNameBinder NameBinder n l
z VarIdent
x NameMap n VarIdent
env) (BNFC'Position -> VarIdent -> Pattern
forall a. a -> VarIdent -> Pattern' a
Raw.PatternVar BNFC'Position
forall {a}. a
loc VarIdent
x)
    PatternPair Pattern n i
l Pattern i l
r ->
      [VarIdent]
-> NameMap n VarIdent
-> Pattern n i
-> ([VarIdent] -> NameMap i VarIdent -> Pattern -> r)
-> r
forall (n :: S) (l :: S) r.
[VarIdent]
-> NameMap n VarIdent
-> Pattern n l
-> ([VarIdent] -> NameMap l VarIdent -> Pattern -> r)
-> r
fromFoilPattern [VarIdent]
freshVars NameMap n VarIdent
env Pattern n i
l (([VarIdent] -> NameMap i VarIdent -> Pattern -> r) -> r)
-> ([VarIdent] -> NameMap i VarIdent -> Pattern -> r) -> r
forall a b. (a -> b) -> a -> b
$ \[VarIdent]
freshVars' NameMap i VarIdent
env' Pattern
l' ->
        [VarIdent]
-> NameMap i VarIdent
-> Pattern i l
-> ([VarIdent] -> NameMap l VarIdent -> Pattern -> r)
-> r
forall (n :: S) (l :: S) r.
[VarIdent]
-> NameMap n VarIdent
-> Pattern n l
-> ([VarIdent] -> NameMap l VarIdent -> Pattern -> r)
-> r
fromFoilPattern [VarIdent]
freshVars' NameMap i VarIdent
env' Pattern i l
r (([VarIdent] -> NameMap l VarIdent -> Pattern -> r) -> r)
-> ([VarIdent] -> NameMap l VarIdent -> Pattern -> r) -> r
forall a b. (a -> b) -> a -> b
$ \[VarIdent]
freshVars'' NameMap l VarIdent
env'' Pattern
r' ->
          [VarIdent] -> NameMap l VarIdent -> Pattern -> r
cont [VarIdent]
freshVars'' NameMap l VarIdent
env'' (BNFC'Position -> Pattern -> Pattern -> Pattern
forall a. a -> Pattern' a -> Pattern' a -> Pattern' a
Raw.PatternPair BNFC'Position
forall {a}. a
loc Pattern
l' Pattern
r')
    where
      loc :: a
loc = String -> a
forall a. HasCallStack => String -> a
error String
"location information is lost when converting from AST"

-- | Convert a scope-safe term into a raw term.
fromFoilTerm
  :: [Raw.VarIdent]         -- ^ A stream of fresh variable identifiers.
  -> NameMap n Raw.VarIdent -- ^ A /total/ mapping for names in scope @n@.
  -> Expr n                 -- ^ A scope safe term in scope @n@.
  -> Raw.Term
fromFoilTerm :: forall (n :: S). [VarIdent] -> NameMap n VarIdent -> Expr n -> Term
fromFoilTerm [VarIdent]
freshVars NameMap n VarIdent
env = \case
  VarE Name n
name -> BNFC'Position -> VarIdent -> Term
forall a. a -> VarIdent -> Term' a
Raw.Var BNFC'Position
forall {a}. a
loc (Name n -> NameMap n VarIdent -> VarIdent
forall (n :: S) a. Name n -> NameMap n a -> a
lookupName Name n
name NameMap n VarIdent
env)
  AppE Expr n
t1 Expr n
t2 -> BNFC'Position -> Term -> Term -> Term
forall a. a -> Term' a -> Term' a -> Term' a
Raw.App BNFC'Position
forall {a}. a
loc ([VarIdent] -> NameMap n VarIdent -> Expr n -> Term
forall (n :: S). [VarIdent] -> NameMap n VarIdent -> Expr n -> Term
fromFoilTerm [VarIdent]
freshVars NameMap n VarIdent
env Expr n
t1) ([VarIdent] -> NameMap n VarIdent -> Expr n -> Term
forall (n :: S). [VarIdent] -> NameMap n VarIdent -> Expr n -> Term
fromFoilTerm [VarIdent]
freshVars NameMap n VarIdent
env Expr n
t2)
  LamE Pattern n l
pattern Expr l
body ->
    [VarIdent]
-> NameMap n VarIdent
-> Pattern n l
-> ([VarIdent] -> NameMap l VarIdent -> Pattern -> Term)
-> Term
forall (n :: S) (l :: S) r.
[VarIdent]
-> NameMap n VarIdent
-> Pattern n l
-> ([VarIdent] -> NameMap l VarIdent -> Pattern -> r)
-> r
fromFoilPattern [VarIdent]
freshVars NameMap n VarIdent
env Pattern n l
pattern (([VarIdent] -> NameMap l VarIdent -> Pattern -> Term) -> Term)
-> ([VarIdent] -> NameMap l VarIdent -> Pattern -> Term) -> Term
forall a b. (a -> b) -> a -> b
$ \[VarIdent]
freshVars' NameMap l VarIdent
env' Pattern
pattern' ->
      BNFC'Position -> Pattern -> ScopedTerm' BNFC'Position -> Term
forall a. a -> Pattern' a -> ScopedTerm' a -> Term' a
Raw.Lam BNFC'Position
forall {a}. a
loc Pattern
pattern' (BNFC'Position -> Term -> ScopedTerm' BNFC'Position
forall a. a -> Term' a -> ScopedTerm' a
Raw.AScopedTerm BNFC'Position
forall {a}. a
loc ([VarIdent] -> NameMap l VarIdent -> Expr l -> Term
forall (n :: S). [VarIdent] -> NameMap n VarIdent -> Expr n -> Term
fromFoilTerm [VarIdent]
freshVars' NameMap l VarIdent
env' Expr l
body))
  PiE Pattern n l
pattern Expr n
a Expr l
b ->
    [VarIdent]
-> NameMap n VarIdent
-> Pattern n l
-> ([VarIdent] -> NameMap l VarIdent -> Pattern -> Term)
-> Term
forall (n :: S) (l :: S) r.
[VarIdent]
-> NameMap n VarIdent
-> Pattern n l
-> ([VarIdent] -> NameMap l VarIdent -> Pattern -> r)
-> r
fromFoilPattern [VarIdent]
freshVars NameMap n VarIdent
env Pattern n l
pattern (([VarIdent] -> NameMap l VarIdent -> Pattern -> Term) -> Term)
-> ([VarIdent] -> NameMap l VarIdent -> Pattern -> Term) -> Term
forall a b. (a -> b) -> a -> b
$ \[VarIdent]
freshVars' NameMap l VarIdent
env' Pattern
pattern' ->
      BNFC'Position
-> Pattern -> Term -> ScopedTerm' BNFC'Position -> Term
forall a. a -> Pattern' a -> Term' a -> ScopedTerm' a -> Term' a
Raw.Pi BNFC'Position
forall {a}. a
loc Pattern
pattern' ([VarIdent] -> NameMap n VarIdent -> Expr n -> Term
forall (n :: S). [VarIdent] -> NameMap n VarIdent -> Expr n -> Term
fromFoilTerm [VarIdent]
freshVars NameMap n VarIdent
env Expr n
a) (BNFC'Position -> Term -> ScopedTerm' BNFC'Position
forall a. a -> Term' a -> ScopedTerm' a
Raw.AScopedTerm BNFC'Position
forall {a}. a
loc ([VarIdent] -> NameMap l VarIdent -> Expr l -> Term
forall (n :: S). [VarIdent] -> NameMap n VarIdent -> Expr n -> Term
fromFoilTerm [VarIdent]
freshVars' NameMap l VarIdent
env' Expr l
b))
  PairE Expr n
t1 Expr n
t2 -> BNFC'Position -> Term -> Term -> Term
forall a. a -> Term' a -> Term' a -> Term' a
Raw.Pair BNFC'Position
forall {a}. a
loc ([VarIdent] -> NameMap n VarIdent -> Expr n -> Term
forall (n :: S). [VarIdent] -> NameMap n VarIdent -> Expr n -> Term
fromFoilTerm [VarIdent]
freshVars NameMap n VarIdent
env Expr n
t1) ([VarIdent] -> NameMap n VarIdent -> Expr n -> Term
forall (n :: S). [VarIdent] -> NameMap n VarIdent -> Expr n -> Term
fromFoilTerm [VarIdent]
freshVars NameMap n VarIdent
env Expr n
t2)
  FirstE Expr n
t -> BNFC'Position -> Term -> Term
forall a. a -> Term' a -> Term' a
Raw.First BNFC'Position
forall {a}. a
loc ([VarIdent] -> NameMap n VarIdent -> Expr n -> Term
forall (n :: S). [VarIdent] -> NameMap n VarIdent -> Expr n -> Term
fromFoilTerm [VarIdent]
freshVars NameMap n VarIdent
env Expr n
t)
  SecondE Expr n
t -> BNFC'Position -> Term -> Term
forall a. a -> Term' a -> Term' a
Raw.Second BNFC'Position
forall {a}. a
loc ([VarIdent] -> NameMap n VarIdent -> Expr n -> Term
forall (n :: S). [VarIdent] -> NameMap n VarIdent -> Expr n -> Term
fromFoilTerm [VarIdent]
freshVars NameMap n VarIdent
env Expr n
t)
  ProductE Expr n
t1 Expr n
t2 -> BNFC'Position -> Term -> Term -> Term
forall a. a -> Term' a -> Term' a -> Term' a
Raw.Product BNFC'Position
forall {a}. a
loc ([VarIdent] -> NameMap n VarIdent -> Expr n -> Term
forall (n :: S). [VarIdent] -> NameMap n VarIdent -> Expr n -> Term
fromFoilTerm [VarIdent]
freshVars NameMap n VarIdent
env Expr n
t1) ([VarIdent] -> NameMap n VarIdent -> Expr n -> Term
forall (n :: S). [VarIdent] -> NameMap n VarIdent -> Expr n -> Term
fromFoilTerm [VarIdent]
freshVars NameMap n VarIdent
env Expr n
t2)
  Expr n
UniverseE -> BNFC'Position -> Term
forall a. a -> Term' a
Raw.Universe BNFC'Position
forall {a}. a
loc
  where
    loc :: a
loc = String -> a
forall a. HasCallStack => String -> a
error String
"location information is lost when converting from AST"

-- | Convert a /closed/ scope-safe term into a raw term.
fromFoilTermClosed
  :: [Raw.VarIdent]   -- ^ A stream of fresh variable identifiers.
  -> Expr VoidS       -- ^ A scope safe term in scope @n@.
  -> Raw.Term
fromFoilTermClosed :: [VarIdent] -> Expr 'VoidS -> Term
fromFoilTermClosed [VarIdent]
freshVars = [VarIdent] -> NameMap 'VoidS VarIdent -> Expr 'VoidS -> Term
forall (n :: S). [VarIdent] -> NameMap n VarIdent -> Expr n -> Term
fromFoilTerm [VarIdent]
freshVars NameMap 'VoidS VarIdent
forall a. NameMap 'VoidS a
emptyNameMap

-- | Convert a scope-safe pattern into a raw pattern converting raw
-- identifiers directly into 'Raw.VarIdent'
fromFoilPattern'
  :: Pattern n l  -- ^ A scope-safe pattern that extends scope @n@ into scope @l@.
  -> Raw.Pattern
fromFoilPattern' :: forall (n :: S) (l :: S). Pattern n l -> Pattern
fromFoilPattern' Pattern n l
pattern =
  case Pattern n l
pattern of
    Pattern n l
PatternWildcard -> BNFC'Position -> Pattern
forall a. a -> Pattern' a
Raw.PatternWildcard BNFC'Position
forall {a}. a
loc
    PatternVar NameBinder n l
z -> BNFC'Position -> VarIdent -> Pattern
forall a. a -> VarIdent -> Pattern' a
Raw.PatternVar BNFC'Position
forall {a}. a
loc (NameBinder n l -> VarIdent
forall {n :: S} {l :: S}. NameBinder n l -> VarIdent
binderToVarIdent NameBinder n l
z)
    PatternPair Pattern n i
l Pattern i l
r ->
      let l' :: Pattern
l' = Pattern n i -> Pattern
forall (n :: S) (l :: S). Pattern n l -> Pattern
fromFoilPattern' Pattern n i
l
          r' :: Pattern
r' = Pattern i l -> Pattern
forall (n :: S) (l :: S). Pattern n l -> Pattern
fromFoilPattern' Pattern i l
r
       in BNFC'Position -> Pattern -> Pattern -> Pattern
forall a. a -> Pattern' a -> Pattern' a -> Pattern' a
Raw.PatternPair BNFC'Position
forall {a}. a
loc Pattern
l' Pattern
r'
    where
      loc :: a
loc = String -> a
forall a. HasCallStack => String -> a
error String
"location information is lost when converting from AST"
      binderToVarIdent :: NameBinder n l -> VarIdent
binderToVarIdent NameBinder n l
binder = String -> VarIdent
Raw.VarIdent (String
"x" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (Name l -> Int
forall (l :: S). Name l -> Int
nameId (NameBinder n l -> Name l
forall (n :: S) (l :: S). NameBinder n l -> Name l
nameOf NameBinder n l
binder)))

-- | Convert a scope-safe term into a raw term converting raw
-- identifiers directly into 'Raw.VarIdent'.
fromFoilTerm'
  :: Expr n                 -- ^ A scope safe term in scope @n@.
  -> Raw.Term
fromFoilTerm' :: forall (n :: S). Expr n -> Term
fromFoilTerm' = \case
  VarE Name n
name -> BNFC'Position -> VarIdent -> Term
forall a. a -> VarIdent -> Term' a
Raw.Var BNFC'Position
forall {a}. a
loc (Name n -> VarIdent
forall {l :: S}. Name l -> VarIdent
nameToVarIdent Name n
name)
  AppE Expr n
t1 Expr n
t2 -> BNFC'Position -> Term -> Term -> Term
forall a. a -> Term' a -> Term' a -> Term' a
Raw.App BNFC'Position
forall {a}. a
loc (Expr n -> Term
forall (n :: S). Expr n -> Term
fromFoilTerm' Expr n
t1) (Expr n -> Term
forall (n :: S). Expr n -> Term
fromFoilTerm' Expr n
t2)
  LamE Pattern n l
pattern Expr l
body ->
    BNFC'Position -> Pattern -> ScopedTerm' BNFC'Position -> Term
forall a. a -> Pattern' a -> ScopedTerm' a -> Term' a
Raw.Lam BNFC'Position
forall {a}. a
loc (Pattern n l -> Pattern
forall (n :: S) (l :: S). Pattern n l -> Pattern
fromFoilPattern' Pattern n l
pattern) (BNFC'Position -> Term -> ScopedTerm' BNFC'Position
forall a. a -> Term' a -> ScopedTerm' a
Raw.AScopedTerm BNFC'Position
forall {a}. a
loc (Expr l -> Term
forall (n :: S). Expr n -> Term
fromFoilTerm' Expr l
body))
  PiE Pattern n l
pattern Expr n
a Expr l
b ->
    BNFC'Position
-> Pattern -> Term -> ScopedTerm' BNFC'Position -> Term
forall a. a -> Pattern' a -> Term' a -> ScopedTerm' a -> Term' a
Raw.Pi BNFC'Position
forall {a}. a
loc (Pattern n l -> Pattern
forall (n :: S) (l :: S). Pattern n l -> Pattern
fromFoilPattern' Pattern n l
pattern) (Expr n -> Term
forall (n :: S). Expr n -> Term
fromFoilTerm' Expr n
a) (BNFC'Position -> Term -> ScopedTerm' BNFC'Position
forall a. a -> Term' a -> ScopedTerm' a
Raw.AScopedTerm BNFC'Position
forall {a}. a
loc (Expr l -> Term
forall (n :: S). Expr n -> Term
fromFoilTerm' Expr l
b))
  PairE Expr n
t1 Expr n
t2 -> BNFC'Position -> Term -> Term -> Term
forall a. a -> Term' a -> Term' a -> Term' a
Raw.Pair BNFC'Position
forall {a}. a
loc (Expr n -> Term
forall (n :: S). Expr n -> Term
fromFoilTerm' Expr n
t1) (Expr n -> Term
forall (n :: S). Expr n -> Term
fromFoilTerm' Expr n
t2)
  FirstE Expr n
t -> BNFC'Position -> Term -> Term
forall a. a -> Term' a -> Term' a
Raw.First BNFC'Position
forall {a}. a
loc (Expr n -> Term
forall (n :: S). Expr n -> Term
fromFoilTerm' Expr n
t)
  SecondE Expr n
t -> BNFC'Position -> Term -> Term
forall a. a -> Term' a -> Term' a
Raw.Second BNFC'Position
forall {a}. a
loc (Expr n -> Term
forall (n :: S). Expr n -> Term
fromFoilTerm' Expr n
t)
  ProductE Expr n
t1 Expr n
t2 -> BNFC'Position -> Term -> Term -> Term
forall a. a -> Term' a -> Term' a -> Term' a
Raw.Product BNFC'Position
forall {a}. a
loc (Expr n -> Term
forall (n :: S). Expr n -> Term
fromFoilTerm' Expr n
t1) (Expr n -> Term
forall (n :: S). Expr n -> Term
fromFoilTerm' Expr n
t2)
  Expr n
UniverseE -> BNFC'Position -> Term
forall a. a -> Term' a
Raw.Universe BNFC'Position
forall {a}. a
loc
  where
    loc :: a
loc = String -> a
forall a. HasCallStack => String -> a
error String
"location information is lost when converting from AST"
    nameToVarIdent :: Name l -> VarIdent
nameToVarIdent Name l
name = String -> VarIdent
Raw.VarIdent (String
"x" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (Name l -> Int
forall (l :: S). Name l -> Int
nameId Name l
name))

-- * Evaluation

-- | Match a pattern against an expression.
matchPattern :: Pattern n l -> Expr n -> Substitution Expr l n
matchPattern :: forall (n :: S) (l :: S).
Pattern n l -> Expr n -> Substitution Expr l n
matchPattern Pattern n l
pattern Expr n
expr = Pattern n l
-> Expr n -> Substitution Expr n n -> Substitution Expr l n
forall (i :: S) (l :: S) (n :: S).
Pattern i l
-> Expr n -> Substitution Expr i n -> Substitution Expr l n
go Pattern n l
pattern Expr n
expr Substitution Expr n n
forall (e :: S -> *) (i :: S). InjectName e => Substitution e i i
identitySubst
  where
    go :: Pattern i l -> Expr n -> Substitution Expr i n -> Substitution Expr l n
    go :: forall (i :: S) (l :: S) (n :: S).
Pattern i l
-> Expr n -> Substitution Expr i n -> Substitution Expr l n
go Pattern i l
PatternWildcard Expr n
_   = Substitution Expr i n -> Substitution Expr i n
Substitution Expr i n -> Substitution Expr l n
forall a. a -> a
id
    go (PatternVar NameBinder i l
x) Expr n
e    = \Substitution Expr i n
subst -> Substitution Expr i n
-> NameBinder i l -> Expr n -> Substitution Expr l n
forall (e :: S -> *) (i :: S) (o :: S) (i' :: S).
Substitution e i o -> NameBinder i i' -> e o -> Substitution e i' o
addSubst Substitution Expr i n
subst NameBinder i l
x Expr n
e
    go (PatternPair Pattern i i
l Pattern i l
r) Expr n
e = Pattern i l
-> Expr n -> Substitution Expr i n -> Substitution Expr l n
forall (i :: S) (l :: S) (n :: S).
Pattern i l
-> Expr n -> Substitution Expr i n -> Substitution Expr l n
go Pattern i l
r (Expr n -> Expr n
forall (n :: S). Expr n -> Expr n
SecondE Expr n
e) (Substitution Expr i n -> Substitution Expr l n)
-> (Substitution Expr i n -> Substitution Expr i n)
-> Substitution Expr i n
-> Substitution Expr l n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Pattern i i
-> Expr n -> Substitution Expr i n -> Substitution Expr i n
forall (i :: S) (l :: S) (n :: S).
Pattern i l
-> Expr n -> Substitution Expr i n -> Substitution Expr l n
go Pattern i i
l (Expr n -> Expr n
forall (n :: S). Expr n -> Expr n
FirstE Expr n
e)

-- | Compute weak head normal form (WHNF).
--
-- >>> whnf emptyScope "(λx.(λ_.x)(λy.x))(λy.λz.z)"
-- λ x0 . λ x1 . x1
--
-- >>> whnf emptyScope "(λs.λz.s(s(z)))(λs.λz.s(s(z)))"
-- λ x1 . (λ x0 . λ x1 . x0 (x0 x1)) ((λ x0 . λ x1 . x0 (x0 x1)) x1)
--
-- Note that during computation bound variables can become unordered
-- in the sense that binders may easily repeat or decrease. For example,
-- in the following expression, inner binder has lower index that the outer one:
--
-- >>> whnf emptyScope "(λx.λy.x)(λx.x)"
-- λ x1 . λ x0 . x0
--
-- At the same time, without substitution, we get regular, increasing binder indices:
--
-- >>> "λx.λy.y" :: Expr VoidS
-- λ x0 . λ x1 . x1
--
-- To compare terms for \(\alpha\)-equivalence, we may use 'alphaEquiv':
--
-- >>> alphaEquiv emptyScope (whnf emptyScope "(λx.λy.x)(λx.x)") "λx.λy.y"
-- True
--
-- We may also normalize binders using 'refreshExpr':
--
-- >>> refreshExpr emptyScope (whnf emptyScope "(λx.λy.x)(λx.x)")
-- λ x0 . λ x1 . x1
whnf :: Distinct n => Scope n -> Expr n -> Expr n
whnf :: forall (n :: S). Distinct n => Scope n -> Expr n -> Expr n
whnf Scope n
scope = \case
  AppE Expr n
f Expr n
arg ->
    case Scope n -> Expr n -> Expr n
forall (n :: S). Distinct n => Scope n -> Expr n -> Expr n
whnf Scope n
scope Expr n
f of
      LamE Pattern n l
pat Expr l
body ->
        let subst :: Substitution Expr l n
subst = Pattern n l -> Expr n -> Substitution Expr l n
forall (n :: S) (l :: S).
Pattern n l -> Expr n -> Substitution Expr l n
matchPattern Pattern n l
pat Expr n
arg
         in Scope n -> Expr n -> Expr n
forall (n :: S). Distinct n => Scope n -> Expr n -> Expr n
whnf Scope n
scope (Scope n -> Substitution Expr l n -> Expr l -> Expr n
forall (o :: S) (i :: S).
Distinct o =>
Scope o -> Substitution Expr i o -> Expr i -> Expr o
substitute Scope n
scope Substitution Expr l n
subst Expr l
body)
      Expr n
f' -> Expr n -> Expr n -> Expr n
forall (n :: S). Expr n -> Expr n -> Expr n
AppE Expr n
f' Expr n
arg
  FirstE Expr n
t ->
    case Scope n -> Expr n -> Expr n
forall (n :: S). Distinct n => Scope n -> Expr n -> Expr n
whnf Scope n
scope Expr n
t of
      PairE Expr n
l Expr n
_r -> Scope n -> Expr n -> Expr n
forall (n :: S). Distinct n => Scope n -> Expr n -> Expr n
whnf Scope n
scope Expr n
l
      Expr n
t'         -> Expr n -> Expr n
forall (n :: S). Expr n -> Expr n
FirstE Expr n
t'
  SecondE Expr n
t ->
    case Scope n -> Expr n -> Expr n
forall (n :: S). Distinct n => Scope n -> Expr n -> Expr n
whnf Scope n
scope Expr n
t of
      PairE Expr n
_l Expr n
r -> Scope n -> Expr n -> Expr n
forall (n :: S). Distinct n => Scope n -> Expr n -> Expr n
whnf Scope n
scope Expr n
r
      Expr n
t'         -> Expr n -> Expr n
forall (n :: S). Expr n -> Expr n
SecondE Expr n
t'
  Expr n
t -> Expr n
t

-- * \(\alpha\)-equivalence

-- | Normalize all binder identifiers in an expression.
refreshExpr :: Distinct n => Scope n -> Expr n -> Expr n
refreshExpr :: forall (n :: S). Distinct n => Scope n -> Expr n -> Expr n
refreshExpr Scope n
scope = Scope n -> Substitution Expr n n -> Expr n -> Expr n
forall (o :: S) (i :: S).
Distinct o =>
Scope o -> Substitution Expr i o -> Expr i -> Expr o
substituteRefresh Scope n
scope Substitution Expr n n
forall (e :: S -> *) (i :: S). InjectName e => Substitution e i i
identitySubst

-- | \(\alpha\)-equivalence check for two terms in one scope
-- via normalization of bound identifiers (via 'refreshExpr').
--
-- This function may perform some unnecessary
-- changes of bound variables when the binders are the same on both sides.
alphaEquivRefreshed :: Distinct n => Scope n -> Expr n -> Expr n -> Bool
alphaEquivRefreshed :: forall (n :: S). Distinct n => Scope n -> Expr n -> Expr n -> Bool
alphaEquivRefreshed Scope n
scope Expr n
e1 Expr n
e2 =
  Scope n -> Expr n -> Expr n
forall (n :: S). Distinct n => Scope n -> Expr n -> Expr n
refreshExpr Scope n
scope Expr n
e1 Expr n -> Expr n -> Bool
forall (n :: S) (l :: S). Expr n -> Expr l -> Bool
`unsafeEqExpr` Scope n -> Expr n -> Expr n
forall (n :: S). Distinct n => Scope n -> Expr n -> Expr n
refreshExpr Scope n
scope Expr n
e2

-- | Unsafely check for equality of two 'Pattern's.
--
-- This __does not__ include \(\alpha\)-equivalence!
unsafeEqPattern :: Pattern n l -> Pattern n' l' -> Bool
unsafeEqPattern :: forall (n :: S) (l :: S) (n' :: S) (l' :: S).
Pattern n l -> Pattern n' l' -> Bool
unsafeEqPattern Pattern n l
PatternWildcard Pattern n' l'
PatternWildcard = Bool
True
unsafeEqPattern (PatternVar NameBinder n l
x) (PatternVar NameBinder n' l'
x')   = NameBinder n l
x NameBinder n l -> NameBinder n l -> Bool
forall a. Eq a => a -> a -> Bool
== NameBinder n' l' -> NameBinder n l
forall a b. Coercible a b => a -> b
coerce NameBinder n' l'
x'
unsafeEqPattern (PatternPair Pattern n i
l Pattern i l
r) (PatternPair Pattern n' i
l' Pattern i l'
r') =
  Pattern n i -> Pattern n' i -> Bool
forall (n :: S) (l :: S) (n' :: S) (l' :: S).
Pattern n l -> Pattern n' l' -> Bool
unsafeEqPattern Pattern n i
l Pattern n' i
l' Bool -> Bool -> Bool
&& Pattern i l -> Pattern i l' -> Bool
forall (n :: S) (l :: S) (n' :: S) (l' :: S).
Pattern n l -> Pattern n' l' -> Bool
unsafeEqPattern Pattern i l
r Pattern i l'
r'
unsafeEqPattern Pattern n l
_ Pattern n' l'
_ = Bool
False

-- | Unsafely check for equality of two 'Expr's.
--
-- This __does not__ include \(\alpha\)-equivalence!
unsafeEqExpr :: Expr n -> Expr l -> Bool
unsafeEqExpr :: forall (n :: S) (l :: S). Expr n -> Expr l -> Bool
unsafeEqExpr Expr n
e1 Expr l
e2 = case (Expr n
e1, Expr l
e2) of
  (VarE Name n
x, VarE Name l
x')            -> Name n
x Name n -> Name n -> Bool
forall a. Eq a => a -> a -> Bool
== Name l -> Name n
forall a b. Coercible a b => a -> b
coerce Name l
x'
  (AppE Expr n
t1 Expr n
t2, AppE Expr l
t1' Expr l
t2')   -> Expr n -> Expr l -> Bool
forall (n :: S) (l :: S). Expr n -> Expr l -> Bool
unsafeEqExpr Expr n
t1 Expr l
t1' Bool -> Bool -> Bool
&& Expr n -> Expr l -> Bool
forall (n :: S) (l :: S). Expr n -> Expr l -> Bool
unsafeEqExpr Expr n
t2 Expr l
t2'
  (LamE Pattern n l
x Expr l
body, LamE Pattern l l
x' Expr l
body') -> Pattern n l -> Pattern l l -> Bool
forall (n :: S) (l :: S) (n' :: S) (l' :: S).
Pattern n l -> Pattern n' l' -> Bool
unsafeEqPattern Pattern n l
x Pattern l l
x' Bool -> Bool -> Bool
&& Expr l -> Expr l -> Bool
forall (n :: S) (l :: S). Expr n -> Expr l -> Bool
unsafeEqExpr Expr l
body Expr l
body'
  (PiE Pattern n l
x Expr n
a Expr l
b, PiE Pattern l l
x' Expr l
a' Expr l
b') -> Pattern n l -> Pattern l l -> Bool
forall (n :: S) (l :: S) (n' :: S) (l' :: S).
Pattern n l -> Pattern n' l' -> Bool
unsafeEqPattern Pattern n l
x Pattern l l
x' Bool -> Bool -> Bool
&& Expr n -> Expr l -> Bool
forall (n :: S) (l :: S). Expr n -> Expr l -> Bool
unsafeEqExpr Expr n
a Expr l
a' Bool -> Bool -> Bool
&& Expr l -> Expr l -> Bool
forall (n :: S) (l :: S). Expr n -> Expr l -> Bool
unsafeEqExpr Expr l
b Expr l
b'
  (PairE Expr n
l Expr n
r, PairE Expr l
l' Expr l
r') -> Expr n -> Expr l -> Bool
forall (n :: S) (l :: S). Expr n -> Expr l -> Bool
unsafeEqExpr Expr n
l Expr l
l' Bool -> Bool -> Bool
&& Expr n -> Expr l -> Bool
forall (n :: S) (l :: S). Expr n -> Expr l -> Bool
unsafeEqExpr Expr n
r Expr l
r'
  (FirstE Expr n
t, FirstE Expr l
t') -> Expr n -> Expr l -> Bool
forall (n :: S) (l :: S). Expr n -> Expr l -> Bool
unsafeEqExpr Expr n
t Expr l
t'
  (SecondE Expr n
t, SecondE Expr l
t') -> Expr n -> Expr l -> Bool
forall (n :: S) (l :: S). Expr n -> Expr l -> Bool
unsafeEqExpr Expr n
t Expr l
t'
  (ProductE Expr n
l Expr n
r, ProductE Expr l
l' Expr l
r') -> Expr n -> Expr l -> Bool
forall (n :: S) (l :: S). Expr n -> Expr l -> Bool
unsafeEqExpr Expr n
l Expr l
l' Bool -> Bool -> Bool
&& Expr n -> Expr l -> Bool
forall (n :: S) (l :: S). Expr n -> Expr l -> Bool
unsafeEqExpr Expr n
r Expr l
r'
  (Expr n
UniverseE, Expr l
UniverseE) -> Bool
True
  (Expr n, Expr l)
_ -> Bool
False

-- | \(\alpha\)-equivalence check for two terms in one scope
-- via unification of bound variables (via 'unifyNameBinders').
--
-- Compared to 'alphaEquivRefreshed', this function might skip unnecessary
-- changes of bound variables when both binders in two matching scoped terms coincide.
alphaEquiv :: Distinct n => Scope n -> Expr n -> Expr n -> Bool
alphaEquiv :: forall (n :: S). Distinct n => Scope n -> Expr n -> Expr n -> Bool
alphaEquiv Scope n
scope Expr n
e1 Expr n
e2 = case (Expr n
e1, Expr n
e2) of
  (VarE Name n
x, VarE Name n
x') -> Name n
x Name n -> Name n -> Bool
forall a. Eq a => a -> a -> Bool
== Name n -> Name n
forall a b. Coercible a b => a -> b
coerce Name n
x'
  (AppE Expr n
t1 Expr n
t2, AppE Expr n
t1' Expr n
t2') -> Scope n -> Expr n -> Expr n -> Bool
forall (n :: S). Distinct n => Scope n -> Expr n -> Expr n -> Bool
alphaEquiv Scope n
scope Expr n
t1 Expr n
t1' Bool -> Bool -> Bool
&& Scope n -> Expr n -> Expr n -> Bool
forall (n :: S). Distinct n => Scope n -> Expr n -> Expr n -> Bool
alphaEquiv Scope n
scope Expr n
t2 Expr n
t2'
  (LamE Pattern n l
x Expr l
body, LamE Pattern n l
x' Expr l
body') -> case Pattern n l -> Pattern n l -> UnifyNameBinders Pattern n l l
forall (n :: S) (l :: S) (r :: S).
Distinct n =>
Pattern n l -> Pattern n r -> UnifyNameBinders Pattern n l r
forall (pattern :: S -> S -> *) (n :: S) (l :: S) (r :: S).
(UnifiablePattern pattern, Distinct n) =>
pattern n l -> pattern n r -> UnifyNameBinders pattern n l r
unifyPatterns Pattern n l
x Pattern n l
x' of
    SameNameBinders NameBinders n l
z    -> case NameBinders n l -> DistinctEvidence l
forall (n :: S) (pattern :: S -> S -> *) (l :: S).
(Distinct n, CoSinkable pattern) =>
pattern n l -> DistinctEvidence l
assertDistinct NameBinders n l
z of
      DistinctEvidence l
Distinct -> Scope l -> Expr l -> Expr l -> Bool
forall (n :: S). Distinct n => Scope n -> Expr n -> Expr n -> Bool
alphaEquiv (NameBinders n l -> Scope n -> Scope l
forall (n :: S) (pattern :: S -> S -> *) (l :: S).
(Distinct n, CoSinkable pattern) =>
pattern n l -> Scope n -> Scope l
extendScopePattern NameBinders n l
z Scope n
scope) Expr l
body Expr l
Expr l
body'
    RenameLeftNameBinder NameBinders n l
z NameBinder n l -> NameBinder n l
renameL -> case NameBinders n l -> DistinctEvidence l
forall (n :: S) (pattern :: S -> S -> *) (l :: S).
(Distinct n, CoSinkable pattern) =>
pattern n l -> DistinctEvidence l
assertDistinct NameBinders n l
z of
      DistinctEvidence l
Distinct ->
        let scope' :: Scope l
scope' = NameBinders n l -> Scope n -> Scope l
forall (n :: S) (pattern :: S -> S -> *) (l :: S).
(Distinct n, CoSinkable pattern) =>
pattern n l -> Scope n -> Scope l
extendScopePattern NameBinders n l
z Scope n
scope
        in Scope l -> Expr l -> Expr l -> Bool
forall (n :: S). Distinct n => Scope n -> Expr n -> Expr n -> Bool
alphaEquiv Scope l
scope' (Scope l -> (Name l -> Name l) -> Expr l -> Expr l
forall (f :: S -> *) (m :: S -> *) (b :: S) (a :: S).
(RelMonad f m, Distinct b) =>
Scope b -> (f a -> f b) -> m a -> m b
liftRM Scope l
scope' ((NameBinder n l -> NameBinder n l) -> Name l -> Name l
forall (n :: S) (l :: S) (l' :: S).
(NameBinder n l -> NameBinder n l') -> Name l -> Name l'
fromNameBinderRenaming NameBinder n l -> NameBinder n l
renameL) Expr l
body) Expr l
body'
    RenameRightNameBinder NameBinders n l
z NameBinder n l -> NameBinder n l
renameR -> case NameBinders n l -> DistinctEvidence l
forall (n :: S) (pattern :: S -> S -> *) (l :: S).
(Distinct n, CoSinkable pattern) =>
pattern n l -> DistinctEvidence l
assertDistinct NameBinders n l
z of
      DistinctEvidence l
Distinct ->
        let scope' :: Scope l
scope' = NameBinders n l -> Scope n -> Scope l
forall (n :: S) (pattern :: S -> S -> *) (l :: S).
(Distinct n, CoSinkable pattern) =>
pattern n l -> Scope n -> Scope l
extendScopePattern NameBinders n l
z Scope n
scope
        in Scope l -> Expr l -> Expr l -> Bool
forall (n :: S). Distinct n => Scope n -> Expr n -> Expr n -> Bool
alphaEquiv Scope l
scope' Expr l
body (Scope l -> (Name l -> Name l) -> Expr l -> Expr l
forall (f :: S -> *) (m :: S -> *) (b :: S) (a :: S).
(RelMonad f m, Distinct b) =>
Scope b -> (f a -> f b) -> m a -> m b
liftRM Scope l
scope' ((NameBinder n l -> NameBinder n l) -> Name l -> Name l
forall (n :: S) (l :: S) (l' :: S).
(NameBinder n l -> NameBinder n l') -> Name l -> Name l'
fromNameBinderRenaming NameBinder n l -> NameBinder n l
renameR) Expr l
body')
    RenameBothBinders NameBinders n lr
z NameBinder n l -> NameBinder n lr
renameL NameBinder n l -> NameBinder n lr
renameR -> case NameBinders n lr -> DistinctEvidence lr
forall (n :: S) (pattern :: S -> S -> *) (l :: S).
(Distinct n, CoSinkable pattern) =>
pattern n l -> DistinctEvidence l
assertDistinct NameBinders n lr
z of
      DistinctEvidence lr
Distinct ->
        let scope' :: Scope lr
scope' = NameBinders n lr -> Scope n -> Scope lr
forall (n :: S) (pattern :: S -> S -> *) (l :: S).
(Distinct n, CoSinkable pattern) =>
pattern n l -> Scope n -> Scope l
extendScopePattern NameBinders n lr
z Scope n
scope
        in Scope lr -> Expr lr -> Expr lr -> Bool
forall (n :: S). Distinct n => Scope n -> Expr n -> Expr n -> Bool
alphaEquiv Scope lr
scope' (Scope lr -> (Name l -> Name lr) -> Expr l -> Expr lr
forall (f :: S -> *) (m :: S -> *) (b :: S) (a :: S).
(RelMonad f m, Distinct b) =>
Scope b -> (f a -> f b) -> m a -> m b
liftRM Scope lr
scope' ((NameBinder n l -> NameBinder n lr) -> Name l -> Name lr
forall (n :: S) (l :: S) (l' :: S).
(NameBinder n l -> NameBinder n l') -> Name l -> Name l'
fromNameBinderRenaming NameBinder n l -> NameBinder n lr
renameL) Expr l
body) (Scope lr -> (Name l -> Name lr) -> Expr l -> Expr lr
forall (f :: S -> *) (m :: S -> *) (b :: S) (a :: S).
(RelMonad f m, Distinct b) =>
Scope b -> (f a -> f b) -> m a -> m b
liftRM Scope lr
scope' ((NameBinder n l -> NameBinder n lr) -> Name l -> Name lr
forall (n :: S) (l :: S) (l' :: S).
(NameBinder n l -> NameBinder n l') -> Name l -> Name l'
fromNameBinderRenaming NameBinder n l -> NameBinder n lr
renameR) Expr l
body')
    UnifyNameBinders Pattern n l l
NotUnifiable -> Bool
False
  (PiE Pattern n l
x Expr n
a Expr l
b, PiE Pattern n l
x' Expr n
a' Expr l
b') -> Scope n -> Expr n -> Expr n -> Bool
forall (n :: S). Distinct n => Scope n -> Expr n -> Expr n -> Bool
alphaEquiv Scope n
scope Expr n
a Expr n
a' Bool -> Bool -> Bool
&& case Pattern n l -> Pattern n l -> UnifyNameBinders Pattern n l l
forall (n :: S) (l :: S) (r :: S).
Distinct n =>
Pattern n l -> Pattern n r -> UnifyNameBinders Pattern n l r
forall (pattern :: S -> S -> *) (n :: S) (l :: S) (r :: S).
(UnifiablePattern pattern, Distinct n) =>
pattern n l -> pattern n r -> UnifyNameBinders pattern n l r
unifyPatterns Pattern n l
x Pattern n l
x' of
    SameNameBinders NameBinders n l
z    -> case NameBinders n l -> DistinctEvidence l
forall (n :: S) (pattern :: S -> S -> *) (l :: S).
(Distinct n, CoSinkable pattern) =>
pattern n l -> DistinctEvidence l
assertDistinct NameBinders n l
z of DistinctEvidence l
Distinct -> Scope l -> Expr l -> Expr l -> Bool
forall (n :: S). Distinct n => Scope n -> Expr n -> Expr n -> Bool
alphaEquiv (NameBinders n l -> Scope n -> Scope l
forall (n :: S) (pattern :: S -> S -> *) (l :: S).
(Distinct n, CoSinkable pattern) =>
pattern n l -> Scope n -> Scope l
extendScopePattern NameBinders n l
z Scope n
scope) Expr l
b Expr l
Expr l
b'
    RenameLeftNameBinder NameBinders n l
z NameBinder n l -> NameBinder n l
renameL -> case NameBinders n l -> DistinctEvidence l
forall (n :: S) (pattern :: S -> S -> *) (l :: S).
(Distinct n, CoSinkable pattern) =>
pattern n l -> DistinctEvidence l
assertDistinct NameBinders n l
z of
      DistinctEvidence l
Distinct ->
        let scope' :: Scope l
scope' = NameBinders n l -> Scope n -> Scope l
forall (n :: S) (pattern :: S -> S -> *) (l :: S).
(Distinct n, CoSinkable pattern) =>
pattern n l -> Scope n -> Scope l
extendScopePattern NameBinders n l
z Scope n
scope
        in Scope l -> Expr l -> Expr l -> Bool
forall (n :: S). Distinct n => Scope n -> Expr n -> Expr n -> Bool
alphaEquiv Scope l
scope' (Scope l -> (Name l -> Name l) -> Expr l -> Expr l
forall (f :: S -> *) (m :: S -> *) (b :: S) (a :: S).
(RelMonad f m, Distinct b) =>
Scope b -> (f a -> f b) -> m a -> m b
liftRM Scope l
scope' ((NameBinder n l -> NameBinder n l) -> Name l -> Name l
forall (n :: S) (l :: S) (l' :: S).
(NameBinder n l -> NameBinder n l') -> Name l -> Name l'
fromNameBinderRenaming NameBinder n l -> NameBinder n l
renameL) Expr l
b) Expr l
b'
    RenameRightNameBinder NameBinders n l
z NameBinder n l -> NameBinder n l
renameR -> case NameBinders n l -> DistinctEvidence l
forall (n :: S) (pattern :: S -> S -> *) (l :: S).
(Distinct n, CoSinkable pattern) =>
pattern n l -> DistinctEvidence l
assertDistinct NameBinders n l
z of
      DistinctEvidence l
Distinct ->
        let scope' :: Scope l
scope' = NameBinders n l -> Scope n -> Scope l
forall (n :: S) (pattern :: S -> S -> *) (l :: S).
(Distinct n, CoSinkable pattern) =>
pattern n l -> Scope n -> Scope l
extendScopePattern NameBinders n l
z Scope n
scope
        in Scope l -> Expr l -> Expr l -> Bool
forall (n :: S). Distinct n => Scope n -> Expr n -> Expr n -> Bool
alphaEquiv Scope l
scope' Expr l
b (Scope l -> (Name l -> Name l) -> Expr l -> Expr l
forall (f :: S -> *) (m :: S -> *) (b :: S) (a :: S).
(RelMonad f m, Distinct b) =>
Scope b -> (f a -> f b) -> m a -> m b
liftRM Scope l
scope' ((NameBinder n l -> NameBinder n l) -> Name l -> Name l
forall (n :: S) (l :: S) (l' :: S).
(NameBinder n l -> NameBinder n l') -> Name l -> Name l'
fromNameBinderRenaming NameBinder n l -> NameBinder n l
renameR) Expr l
b')
    RenameBothBinders NameBinders n lr
z NameBinder n l -> NameBinder n lr
renameL NameBinder n l -> NameBinder n lr
renameR -> case NameBinders n lr -> DistinctEvidence lr
forall (n :: S) (pattern :: S -> S -> *) (l :: S).
(Distinct n, CoSinkable pattern) =>
pattern n l -> DistinctEvidence l
assertDistinct NameBinders n lr
z of
      DistinctEvidence lr
Distinct ->
        let scope' :: Scope lr
scope' = NameBinders n lr -> Scope n -> Scope lr
forall (n :: S) (pattern :: S -> S -> *) (l :: S).
(Distinct n, CoSinkable pattern) =>
pattern n l -> Scope n -> Scope l
extendScopePattern NameBinders n lr
z Scope n
scope
        in Scope lr -> Expr lr -> Expr lr -> Bool
forall (n :: S). Distinct n => Scope n -> Expr n -> Expr n -> Bool
alphaEquiv Scope lr
scope' (Scope lr -> (Name l -> Name lr) -> Expr l -> Expr lr
forall (f :: S -> *) (m :: S -> *) (b :: S) (a :: S).
(RelMonad f m, Distinct b) =>
Scope b -> (f a -> f b) -> m a -> m b
liftRM Scope lr
scope' ((NameBinder n l -> NameBinder n lr) -> Name l -> Name lr
forall (n :: S) (l :: S) (l' :: S).
(NameBinder n l -> NameBinder n l') -> Name l -> Name l'
fromNameBinderRenaming NameBinder n l -> NameBinder n lr
renameL) Expr l
b) (Scope lr -> (Name l -> Name lr) -> Expr l -> Expr lr
forall (f :: S -> *) (m :: S -> *) (b :: S) (a :: S).
(RelMonad f m, Distinct b) =>
Scope b -> (f a -> f b) -> m a -> m b
liftRM Scope lr
scope' ((NameBinder n l -> NameBinder n lr) -> Name l -> Name lr
forall (n :: S) (l :: S) (l' :: S).
(NameBinder n l -> NameBinder n l') -> Name l -> Name l'
fromNameBinderRenaming NameBinder n l -> NameBinder n lr
renameR) Expr l
b')
    UnifyNameBinders Pattern n l l
NotUnifiable -> Bool
False
  (PairE Expr n
l Expr n
r, PairE Expr n
l' Expr n
r') -> Scope n -> Expr n -> Expr n -> Bool
forall (n :: S). Distinct n => Scope n -> Expr n -> Expr n -> Bool
alphaEquiv Scope n
scope Expr n
l Expr n
l' Bool -> Bool -> Bool
&& Scope n -> Expr n -> Expr n -> Bool
forall (n :: S). Distinct n => Scope n -> Expr n -> Expr n -> Bool
alphaEquiv Scope n
scope Expr n
r Expr n
r'
  (FirstE Expr n
t, FirstE Expr n
t') -> Scope n -> Expr n -> Expr n -> Bool
forall (n :: S). Distinct n => Scope n -> Expr n -> Expr n -> Bool
alphaEquiv Scope n
scope Expr n
t Expr n
t'
  (SecondE Expr n
t, SecondE Expr n
t') -> Scope n -> Expr n -> Expr n -> Bool
forall (n :: S). Distinct n => Scope n -> Expr n -> Expr n -> Bool
alphaEquiv Scope n
scope Expr n
t Expr n
t'
  (ProductE Expr n
l Expr n
r, ProductE Expr n
l' Expr n
r') -> Scope n -> Expr n -> Expr n -> Bool
forall (n :: S). Distinct n => Scope n -> Expr n -> Expr n -> Bool
alphaEquiv Scope n
scope Expr n
l Expr n
l' Bool -> Bool -> Bool
&& Scope n -> Expr n -> Expr n -> Bool
forall (n :: S). Distinct n => Scope n -> Expr n -> Expr n -> Bool
alphaEquiv Scope n
scope Expr n
r Expr n
r'
  (Expr n
UniverseE, Expr n
UniverseE) -> Bool
True
  (Expr n, Expr n)
_ -> Bool
False

-- * Interpreter

-- | Interpret a \(\lambda\Pi\) command.
interpretCommand :: Raw.Command -> IO ()
interpretCommand :: Command -> IO ()
interpretCommand (Raw.CommandCompute BNFC'Position
_loc Term
term Term
_type) =
  String -> IO ()
putStrLn (String
"  ↦ " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr 'VoidS -> String
printExpr (Scope 'VoidS -> Expr 'VoidS -> Expr 'VoidS
forall (n :: S). Distinct n => Scope n -> Expr n -> Expr n
whnf Scope 'VoidS
emptyScope (Scope 'VoidS -> Map VarIdent (Name 'VoidS) -> Term -> Expr 'VoidS
forall (n :: S).
Distinct n =>
Scope n -> Map VarIdent (Name n) -> Term -> Expr n
toFoilTerm Scope 'VoidS
emptyScope Map VarIdent (Name 'VoidS)
forall k a. Map k a
Map.empty Term
term)))
-- #TODO: add typeCheck
interpretCommand (Raw.CommandCheck BNFC'Position
_loc Term
_term Term
_type) =
  String -> IO ()
putStrLn String
"Not yet implemented"

-- | Interpret a \(\lambda\Pi\) program.
interpretProgram :: Raw.Program -> IO ()
interpretProgram :: Program -> IO ()
interpretProgram (Raw.AProgram BNFC'Position
_loc [Command]
typedTerms) = (Command -> IO ()) -> [Command] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Command -> IO ()
interpretCommand [Command]
typedTerms

-- | Default interpreter program.
-- Reads a \(\lambda\Pi\) program from the standard input and runs the commands.
defaultMain :: IO ()
defaultMain :: IO ()
defaultMain = do
  String
input <- IO String
getContents
  case [Token] -> Err Program
pProgram (Bool -> [Token] -> [Token]
resolveLayout Bool
True (String -> [Token]
tokens String
input)) of
    Left String
err -> do
      String -> IO ()
putStrLn String
err
      IO ()
forall a. IO a
exitFailure
    Right Program
program -> Program -> IO ()
interpretProgram Program
program

-- * Example terms

-- | A helper for constructing \(\lambda\)-abstractions.
lam :: Distinct n => Scope n -> (forall l. DExt n l => Scope l -> NameBinder n l -> Expr l) -> Expr n
lam :: forall (n :: S).
Distinct n =>
Scope n
-> (forall (l :: S).
    DExt n l =>
    Scope l -> NameBinder n l -> Expr l)
-> Expr n
lam Scope n
scope forall (l :: S). DExt n l => Scope l -> NameBinder n l -> Expr l
mkBody = Scope n
-> (forall {l :: S}. DExt n l => NameBinder n l -> Expr n)
-> Expr n
forall (n :: S) r.
Distinct n =>
Scope n -> (forall (l :: S). DExt n l => NameBinder n l -> r) -> r
withFresh Scope n
scope ((forall {l :: S}. DExt n l => NameBinder n l -> Expr n) -> Expr n)
-> (forall {l :: S}. DExt n l => NameBinder n l -> Expr n)
-> Expr n
forall a b. (a -> b) -> a -> b
$ \NameBinder n l
x ->
  let scope' :: Scope l
scope' = NameBinder n l -> Scope n -> Scope l
forall (n :: S) (l :: S). NameBinder n l -> Scope n -> Scope l
extendScope NameBinder n l
x Scope n
scope
   in Pattern n l -> Expr l -> Expr n
forall (n :: S) (l :: S). Pattern n l -> Expr l -> Expr n
LamE (NameBinder n l -> Pattern n l
forall (n :: S) (l :: S). NameBinder n l -> Pattern n l
PatternVar NameBinder n l
x) (Scope l -> NameBinder n l -> Expr l
forall (l :: S). DExt n l => Scope l -> NameBinder n l -> Expr l
mkBody Scope l
scope' NameBinder n l
x)

-- | An identity function as a \(\lambda\)-term:
--
-- >>> identity
-- λ x0 . x0
identity :: Expr VoidS
identity :: Expr 'VoidS
identity = Scope 'VoidS
-> (forall {l :: S}.
    DExt 'VoidS l =>
    Scope l -> NameBinder 'VoidS l -> Expr l)
-> Expr 'VoidS
forall (n :: S).
Distinct n =>
Scope n
-> (forall (l :: S).
    DExt n l =>
    Scope l -> NameBinder n l -> Expr l)
-> Expr n
lam Scope 'VoidS
emptyScope ((forall {l :: S}.
  DExt 'VoidS l =>
  Scope l -> NameBinder 'VoidS l -> Expr l)
 -> Expr 'VoidS)
-> (forall {l :: S}.
    DExt 'VoidS l =>
    Scope l -> NameBinder 'VoidS l -> Expr l)
-> Expr 'VoidS
forall a b. (a -> b) -> a -> b
$ \Scope l
_ NameBinder 'VoidS l
nx ->
  Name l -> Expr l
forall (n :: S). Name n -> Expr n
VarE (NameBinder 'VoidS l -> Name l
forall (n :: S) (l :: S). NameBinder n l -> Name l
nameOf NameBinder 'VoidS l
nx)

-- | Church-encoding of a natural number \(n\).
--
-- >>> churchN 0
-- λ x0 . λ x1 . x1
--
-- >>> churchN 3
-- λ x0 . λ x1 . x0 (x0 (x0 x1))
churchN :: Int -> Expr VoidS
churchN :: Int -> Expr 'VoidS
churchN Int
n =
  Scope 'VoidS
-> (forall {l :: S}.
    DExt 'VoidS l =>
    Scope l -> NameBinder 'VoidS l -> Expr l)
-> Expr 'VoidS
forall (n :: S).
Distinct n =>
Scope n
-> (forall (l :: S).
    DExt n l =>
    Scope l -> NameBinder n l -> Expr l)
-> Expr n
lam Scope 'VoidS
emptyScope ((forall {l :: S}.
  DExt 'VoidS l =>
  Scope l -> NameBinder 'VoidS l -> Expr l)
 -> Expr 'VoidS)
-> (forall {l :: S}.
    DExt 'VoidS l =>
    Scope l -> NameBinder 'VoidS l -> Expr l)
-> Expr 'VoidS
forall a b. (a -> b) -> a -> b
$ \Scope l
sx NameBinder 'VoidS l
nx ->
    Scope l
-> (forall {l :: S}.
    DExt l l =>
    Scope l -> NameBinder l l -> Expr l)
-> Expr l
forall (n :: S).
Distinct n =>
Scope n
-> (forall (l :: S).
    DExt n l =>
    Scope l -> NameBinder n l -> Expr l)
-> Expr n
lam Scope l
sx ((forall {l :: S}. DExt l l => Scope l -> NameBinder l l -> Expr l)
 -> Expr l)
-> (forall {l :: S}.
    DExt l l =>
    Scope l -> NameBinder l l -> Expr l)
-> Expr l
forall a b. (a -> b) -> a -> b
$ \Scope l
_sxy NameBinder l l
ny ->
      let x :: Expr l
x = Expr l -> Expr l
forall (e :: S -> *) (n :: S) (l :: S).
(Sinkable e, DExt n l) =>
e n -> e l
sink (Name l -> Expr l
forall (n :: S). Name n -> Expr n
VarE (NameBinder 'VoidS l -> Name l
forall (n :: S) (l :: S). NameBinder n l -> Name l
nameOf NameBinder 'VoidS l
nx))
          y :: Expr l
y = Name l -> Expr l
forall (n :: S). Name n -> Expr n
VarE (NameBinder l l -> Name l
forall (n :: S) (l :: S). NameBinder n l -> Name l
nameOf NameBinder l l
ny)
       in (Expr l -> Expr l) -> Expr l -> [Expr l]
forall a. (a -> a) -> a -> [a]
iterate (Expr l -> Expr l -> Expr l
forall (n :: S). Expr n -> Expr n -> Expr n
AppE Expr l
x) Expr l
y [Expr l] -> Int -> Expr l
forall a. HasCallStack => [a] -> Int -> a
!! Int
n