{-# LANGUAGE DataKinds         #-}
{-# LANGUAGE KindSignatures    #-}
{-# LANGUAGE TypeFamilies      #-}
{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs             #-}
{-# LANGUAGE LambdaCase        #-}
{-# LANGUAGE PatternSynonyms   #-}
{-# LANGUAGE TemplateHaskell   #-}
{-# LANGUAGE TypeOperators     #-}
-- | Free foil implementation of the \(\lambda\Pi\)-calculus (with pairs).
--
-- Free foil provides __general__ definitions or implementations for the following:
--
-- 1. Freely generated (from a simple signature) scope-safe AST.
-- 2. Correct capture-avoiding substitution (see 'substitute').
-- 3. Correct \(\alpha\)-equivalence checks (see 'alphaEquiv' and 'alphaEquivRefreshed') as well as \(\alpha\)-normalization (see 'refreshAST').
-- 4. Conversion helpers (see 'convertToAST' and 'convertFromAST').
--
-- The following is implemented __manually__ in this module:
--
-- 1. Convenient pattern synonyms.
-- 2. 'ZipMatch' instances (enabling general \(\alpha\)-equivalence).
-- 3. Conversion between scope-safe and raw term representation (the latter is generated via BNFC), see 'toLambdaPi' and 'fromLambdaPi'.
-- 4. Computation of weak head normal form (WHNF), see 'whnf'.
-- 5. Entry point, gluing everything together. See 'defaultMain'.
--
-- __Note:__ free foil does not (easily) support patterns at the moment,
-- so only wildcard patterns and variable patterns are handled in this implementation.
--
-- See "Language.LambdaPi.Impl.FreeFoilTH" for a variation of this with more automation via Template Haskell.
module Language.LambdaPi.Impl.FreeFoil where

import qualified Control.Monad.Foil              as Foil
import           Control.Monad.Free.Foil
import           Data.Bifunctor.Sum
import           Data.Bifunctor.TH
import           Data.Map                        (Map)
import qualified Data.Map                        as Map
import           Data.ZipMatchK
import           Data.String                     (IsString (..))
import           Generics.Kind.TH                (deriveGenericK)
import qualified Language.LambdaPi.Syntax.Abs    as Raw
import qualified Language.LambdaPi.Syntax.Layout as Raw
import qualified Language.LambdaPi.Syntax.Lex    as Raw
import qualified Language.LambdaPi.Syntax.Par    as Raw
import qualified Language.LambdaPi.Syntax.Print  as Raw
import           System.Exit                     (exitFailure)
import Data.ZipMatchK.Bifunctor ()

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

-- | The signature 'Bifunctor' for the \(\lambda\Pi\).
data LambdaPiF scope term
  = AppF term term        -- ^ Application: \((t_1 \; t_2)\)
  | LamF scope            -- ^ Abstraction: \(\lambda x. t\)
  | PiF term scope        -- ^ Dependent function type: \(\prod_{x : T_1} T_2\)
  | UniverseF             -- ^ Universe (type of types): \(\mathcal{U}\)
  deriving (LambdaPiF scope term -> LambdaPiF scope term -> Bool
(LambdaPiF scope term -> LambdaPiF scope term -> Bool)
-> (LambdaPiF scope term -> LambdaPiF scope term -> Bool)
-> Eq (LambdaPiF scope term)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall scope term.
(Eq term, Eq scope) =>
LambdaPiF scope term -> LambdaPiF scope term -> Bool
$c== :: forall scope term.
(Eq term, Eq scope) =>
LambdaPiF scope term -> LambdaPiF scope term -> Bool
== :: LambdaPiF scope term -> LambdaPiF scope term -> Bool
$c/= :: forall scope term.
(Eq term, Eq scope) =>
LambdaPiF scope term -> LambdaPiF scope term -> Bool
/= :: LambdaPiF scope term -> LambdaPiF scope term -> Bool
Eq, Int -> LambdaPiF scope term -> ShowS
[LambdaPiF scope term] -> ShowS
LambdaPiF scope term -> String
(Int -> LambdaPiF scope term -> ShowS)
-> (LambdaPiF scope term -> String)
-> ([LambdaPiF scope term] -> ShowS)
-> Show (LambdaPiF scope term)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall scope term.
(Show term, Show scope) =>
Int -> LambdaPiF scope term -> ShowS
forall scope term.
(Show term, Show scope) =>
[LambdaPiF scope term] -> ShowS
forall scope term.
(Show term, Show scope) =>
LambdaPiF scope term -> String
$cshowsPrec :: forall scope term.
(Show term, Show scope) =>
Int -> LambdaPiF scope term -> ShowS
showsPrec :: Int -> LambdaPiF scope term -> ShowS
$cshow :: forall scope term.
(Show term, Show scope) =>
LambdaPiF scope term -> String
show :: LambdaPiF scope term -> String
$cshowList :: forall scope term.
(Show term, Show scope) =>
[LambdaPiF scope term] -> ShowS
showList :: [LambdaPiF scope term] -> ShowS
Show, (forall a b. (a -> b) -> LambdaPiF scope a -> LambdaPiF scope b)
-> (forall a b. a -> LambdaPiF scope b -> LambdaPiF scope a)
-> Functor (LambdaPiF scope)
forall a b. a -> LambdaPiF scope b -> LambdaPiF scope a
forall a b. (a -> b) -> LambdaPiF scope a -> LambdaPiF scope b
forall scope a b. a -> LambdaPiF scope b -> LambdaPiF scope a
forall scope a b.
(a -> b) -> LambdaPiF scope a -> LambdaPiF scope b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall scope a b.
(a -> b) -> LambdaPiF scope a -> LambdaPiF scope b
fmap :: forall a b. (a -> b) -> LambdaPiF scope a -> LambdaPiF scope b
$c<$ :: forall scope a b. a -> LambdaPiF scope b -> LambdaPiF scope a
<$ :: forall a b. a -> LambdaPiF scope b -> LambdaPiF scope a
Functor, (forall m. Monoid m => LambdaPiF scope m -> m)
-> (forall m a. Monoid m => (a -> m) -> LambdaPiF scope a -> m)
-> (forall m a. Monoid m => (a -> m) -> LambdaPiF scope a -> m)
-> (forall a b. (a -> b -> b) -> b -> LambdaPiF scope a -> b)
-> (forall a b. (a -> b -> b) -> b -> LambdaPiF scope a -> b)
-> (forall b a. (b -> a -> b) -> b -> LambdaPiF scope a -> b)
-> (forall b a. (b -> a -> b) -> b -> LambdaPiF scope a -> b)
-> (forall a. (a -> a -> a) -> LambdaPiF scope a -> a)
-> (forall a. (a -> a -> a) -> LambdaPiF scope a -> a)
-> (forall a. LambdaPiF scope a -> [a])
-> (forall a. LambdaPiF scope a -> Bool)
-> (forall a. LambdaPiF scope a -> Int)
-> (forall a. Eq a => a -> LambdaPiF scope a -> Bool)
-> (forall a. Ord a => LambdaPiF scope a -> a)
-> (forall a. Ord a => LambdaPiF scope a -> a)
-> (forall a. Num a => LambdaPiF scope a -> a)
-> (forall a. Num a => LambdaPiF scope a -> a)
-> Foldable (LambdaPiF scope)
forall a. Eq a => a -> LambdaPiF scope a -> Bool
forall a. Num a => LambdaPiF scope a -> a
forall a. Ord a => LambdaPiF scope a -> a
forall m. Monoid m => LambdaPiF scope m -> m
forall a. LambdaPiF scope a -> Bool
forall a. LambdaPiF scope a -> Int
forall a. LambdaPiF scope a -> [a]
forall a. (a -> a -> a) -> LambdaPiF scope a -> a
forall scope a. Eq a => a -> LambdaPiF scope a -> Bool
forall scope a. Num a => LambdaPiF scope a -> a
forall scope a. Ord a => LambdaPiF scope a -> a
forall scope m. Monoid m => LambdaPiF scope m -> m
forall m a. Monoid m => (a -> m) -> LambdaPiF scope a -> m
forall scope a. LambdaPiF scope a -> Bool
forall scope a. LambdaPiF scope a -> Int
forall scope a. LambdaPiF scope a -> [a]
forall b a. (b -> a -> b) -> b -> LambdaPiF scope a -> b
forall a b. (a -> b -> b) -> b -> LambdaPiF scope a -> b
forall scope a. (a -> a -> a) -> LambdaPiF scope a -> a
forall scope m a. Monoid m => (a -> m) -> LambdaPiF scope a -> m
forall scope b a. (b -> a -> b) -> b -> LambdaPiF scope a -> b
forall scope a b. (a -> b -> b) -> b -> LambdaPiF scope a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
$cfold :: forall scope m. Monoid m => LambdaPiF scope m -> m
fold :: forall m. Monoid m => LambdaPiF scope m -> m
$cfoldMap :: forall scope m a. Monoid m => (a -> m) -> LambdaPiF scope a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> LambdaPiF scope a -> m
$cfoldMap' :: forall scope m a. Monoid m => (a -> m) -> LambdaPiF scope a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> LambdaPiF scope a -> m
$cfoldr :: forall scope a b. (a -> b -> b) -> b -> LambdaPiF scope a -> b
foldr :: forall a b. (a -> b -> b) -> b -> LambdaPiF scope a -> b
$cfoldr' :: forall scope a b. (a -> b -> b) -> b -> LambdaPiF scope a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> LambdaPiF scope a -> b
$cfoldl :: forall scope b a. (b -> a -> b) -> b -> LambdaPiF scope a -> b
foldl :: forall b a. (b -> a -> b) -> b -> LambdaPiF scope a -> b
$cfoldl' :: forall scope b a. (b -> a -> b) -> b -> LambdaPiF scope a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> LambdaPiF scope a -> b
$cfoldr1 :: forall scope a. (a -> a -> a) -> LambdaPiF scope a -> a
foldr1 :: forall a. (a -> a -> a) -> LambdaPiF scope a -> a
$cfoldl1 :: forall scope a. (a -> a -> a) -> LambdaPiF scope a -> a
foldl1 :: forall a. (a -> a -> a) -> LambdaPiF scope a -> a
$ctoList :: forall scope a. LambdaPiF scope a -> [a]
toList :: forall a. LambdaPiF scope a -> [a]
$cnull :: forall scope a. LambdaPiF scope a -> Bool
null :: forall a. LambdaPiF scope a -> Bool
$clength :: forall scope a. LambdaPiF scope a -> Int
length :: forall a. LambdaPiF scope a -> Int
$celem :: forall scope a. Eq a => a -> LambdaPiF scope a -> Bool
elem :: forall a. Eq a => a -> LambdaPiF scope a -> Bool
$cmaximum :: forall scope a. Ord a => LambdaPiF scope a -> a
maximum :: forall a. Ord a => LambdaPiF scope a -> a
$cminimum :: forall scope a. Ord a => LambdaPiF scope a -> a
minimum :: forall a. Ord a => LambdaPiF scope a -> a
$csum :: forall scope a. Num a => LambdaPiF scope a -> a
sum :: forall a. Num a => LambdaPiF scope a -> a
$cproduct :: forall scope a. Num a => LambdaPiF scope a -> a
product :: forall a. Num a => LambdaPiF scope a -> a
Foldable, Functor (LambdaPiF scope)
Foldable (LambdaPiF scope)
(Functor (LambdaPiF scope), Foldable (LambdaPiF scope)) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> LambdaPiF scope a -> f (LambdaPiF scope b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    LambdaPiF scope (f a) -> f (LambdaPiF scope a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> LambdaPiF scope a -> m (LambdaPiF scope b))
-> (forall (m :: * -> *) a.
    Monad m =>
    LambdaPiF scope (m a) -> m (LambdaPiF scope a))
-> Traversable (LambdaPiF scope)
forall scope. Functor (LambdaPiF scope)
forall scope. Foldable (LambdaPiF scope)
forall scope (m :: * -> *) a.
Monad m =>
LambdaPiF scope (m a) -> m (LambdaPiF scope a)
forall scope (f :: * -> *) a.
Applicative f =>
LambdaPiF scope (f a) -> f (LambdaPiF scope a)
forall scope (m :: * -> *) a b.
Monad m =>
(a -> m b) -> LambdaPiF scope a -> m (LambdaPiF scope b)
forall scope (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> LambdaPiF scope a -> f (LambdaPiF scope b)
forall (t :: * -> *).
(Functor t, Foldable t) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a.
Monad m =>
LambdaPiF scope (m a) -> m (LambdaPiF scope a)
forall (f :: * -> *) a.
Applicative f =>
LambdaPiF scope (f a) -> f (LambdaPiF scope a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> LambdaPiF scope a -> m (LambdaPiF scope b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> LambdaPiF scope a -> f (LambdaPiF scope b)
$ctraverse :: forall scope (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> LambdaPiF scope a -> f (LambdaPiF scope b)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> LambdaPiF scope a -> f (LambdaPiF scope b)
$csequenceA :: forall scope (f :: * -> *) a.
Applicative f =>
LambdaPiF scope (f a) -> f (LambdaPiF scope a)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
LambdaPiF scope (f a) -> f (LambdaPiF scope a)
$cmapM :: forall scope (m :: * -> *) a b.
Monad m =>
(a -> m b) -> LambdaPiF scope a -> m (LambdaPiF scope b)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> LambdaPiF scope a -> m (LambdaPiF scope b)
$csequence :: forall scope (m :: * -> *) a.
Monad m =>
LambdaPiF scope (m a) -> m (LambdaPiF scope a)
sequence :: forall (m :: * -> *) a.
Monad m =>
LambdaPiF scope (m a) -> m (LambdaPiF scope a)
Traversable)
deriveBifunctor ''LambdaPiF
deriveBifoldable ''LambdaPiF
deriveBitraversable ''LambdaPiF
deriveGenericK ''LambdaPiF
instance ZipMatchK LambdaPiF

-- | The signature 'Bifunctor' for pairs.
data PairF scope term
  = PairF term term       -- ^ Pair: \(\langle t_1, t_2 \rangle\)
  | FirstF term           -- ^ First projection: \(\pi_1(t)\)
  | SecondF term          -- ^ Second projection: \(\pi_2(t)\)
  | ProductF term term    -- ^ Product type (non-dependent): \(T_1 \times T_2\)
  deriving (PairF scope term -> PairF scope term -> Bool
(PairF scope term -> PairF scope term -> Bool)
-> (PairF scope term -> PairF scope term -> Bool)
-> Eq (PairF scope term)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall scope term.
Eq term =>
PairF scope term -> PairF scope term -> Bool
$c== :: forall scope term.
Eq term =>
PairF scope term -> PairF scope term -> Bool
== :: PairF scope term -> PairF scope term -> Bool
$c/= :: forall scope term.
Eq term =>
PairF scope term -> PairF scope term -> Bool
/= :: PairF scope term -> PairF scope term -> Bool
Eq, Int -> PairF scope term -> ShowS
[PairF scope term] -> ShowS
PairF scope term -> String
(Int -> PairF scope term -> ShowS)
-> (PairF scope term -> String)
-> ([PairF scope term] -> ShowS)
-> Show (PairF scope term)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall scope term. Show term => Int -> PairF scope term -> ShowS
forall scope term. Show term => [PairF scope term] -> ShowS
forall scope term. Show term => PairF scope term -> String
$cshowsPrec :: forall scope term. Show term => Int -> PairF scope term -> ShowS
showsPrec :: Int -> PairF scope term -> ShowS
$cshow :: forall scope term. Show term => PairF scope term -> String
show :: PairF scope term -> String
$cshowList :: forall scope term. Show term => [PairF scope term] -> ShowS
showList :: [PairF scope term] -> ShowS
Show, (forall a b. (a -> b) -> PairF scope a -> PairF scope b)
-> (forall a b. a -> PairF scope b -> PairF scope a)
-> Functor (PairF scope)
forall a b. a -> PairF scope b -> PairF scope a
forall a b. (a -> b) -> PairF scope a -> PairF scope b
forall scope a b. a -> PairF scope b -> PairF scope a
forall scope a b. (a -> b) -> PairF scope a -> PairF scope b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall scope a b. (a -> b) -> PairF scope a -> PairF scope b
fmap :: forall a b. (a -> b) -> PairF scope a -> PairF scope b
$c<$ :: forall scope a b. a -> PairF scope b -> PairF scope a
<$ :: forall a b. a -> PairF scope b -> PairF scope a
Functor, (forall m. Monoid m => PairF scope m -> m)
-> (forall m a. Monoid m => (a -> m) -> PairF scope a -> m)
-> (forall m a. Monoid m => (a -> m) -> PairF scope a -> m)
-> (forall a b. (a -> b -> b) -> b -> PairF scope a -> b)
-> (forall a b. (a -> b -> b) -> b -> PairF scope a -> b)
-> (forall b a. (b -> a -> b) -> b -> PairF scope a -> b)
-> (forall b a. (b -> a -> b) -> b -> PairF scope a -> b)
-> (forall a. (a -> a -> a) -> PairF scope a -> a)
-> (forall a. (a -> a -> a) -> PairF scope a -> a)
-> (forall a. PairF scope a -> [a])
-> (forall a. PairF scope a -> Bool)
-> (forall a. PairF scope a -> Int)
-> (forall a. Eq a => a -> PairF scope a -> Bool)
-> (forall a. Ord a => PairF scope a -> a)
-> (forall a. Ord a => PairF scope a -> a)
-> (forall a. Num a => PairF scope a -> a)
-> (forall a. Num a => PairF scope a -> a)
-> Foldable (PairF scope)
forall a. Eq a => a -> PairF scope a -> Bool
forall a. Num a => PairF scope a -> a
forall a. Ord a => PairF scope a -> a
forall m. Monoid m => PairF scope m -> m
forall a. PairF scope a -> Bool
forall a. PairF scope a -> Int
forall a. PairF scope a -> [a]
forall a. (a -> a -> a) -> PairF scope a -> a
forall scope a. Eq a => a -> PairF scope a -> Bool
forall scope a. Num a => PairF scope a -> a
forall scope a. Ord a => PairF scope a -> a
forall scope m. Monoid m => PairF scope m -> m
forall m a. Monoid m => (a -> m) -> PairF scope a -> m
forall scope a. PairF scope a -> Bool
forall scope a. PairF scope a -> Int
forall scope a. PairF scope a -> [a]
forall b a. (b -> a -> b) -> b -> PairF scope a -> b
forall a b. (a -> b -> b) -> b -> PairF scope a -> b
forall scope a. (a -> a -> a) -> PairF scope a -> a
forall scope m a. Monoid m => (a -> m) -> PairF scope a -> m
forall scope b a. (b -> a -> b) -> b -> PairF scope a -> b
forall scope a b. (a -> b -> b) -> b -> PairF scope a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
$cfold :: forall scope m. Monoid m => PairF scope m -> m
fold :: forall m. Monoid m => PairF scope m -> m
$cfoldMap :: forall scope m a. Monoid m => (a -> m) -> PairF scope a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> PairF scope a -> m
$cfoldMap' :: forall scope m a. Monoid m => (a -> m) -> PairF scope a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> PairF scope a -> m
$cfoldr :: forall scope a b. (a -> b -> b) -> b -> PairF scope a -> b
foldr :: forall a b. (a -> b -> b) -> b -> PairF scope a -> b
$cfoldr' :: forall scope a b. (a -> b -> b) -> b -> PairF scope a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> PairF scope a -> b
$cfoldl :: forall scope b a. (b -> a -> b) -> b -> PairF scope a -> b
foldl :: forall b a. (b -> a -> b) -> b -> PairF scope a -> b
$cfoldl' :: forall scope b a. (b -> a -> b) -> b -> PairF scope a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> PairF scope a -> b
$cfoldr1 :: forall scope a. (a -> a -> a) -> PairF scope a -> a
foldr1 :: forall a. (a -> a -> a) -> PairF scope a -> a
$cfoldl1 :: forall scope a. (a -> a -> a) -> PairF scope a -> a
foldl1 :: forall a. (a -> a -> a) -> PairF scope a -> a
$ctoList :: forall scope a. PairF scope a -> [a]
toList :: forall a. PairF scope a -> [a]
$cnull :: forall scope a. PairF scope a -> Bool
null :: forall a. PairF scope a -> Bool
$clength :: forall scope a. PairF scope a -> Int
length :: forall a. PairF scope a -> Int
$celem :: forall scope a. Eq a => a -> PairF scope a -> Bool
elem :: forall a. Eq a => a -> PairF scope a -> Bool
$cmaximum :: forall scope a. Ord a => PairF scope a -> a
maximum :: forall a. Ord a => PairF scope a -> a
$cminimum :: forall scope a. Ord a => PairF scope a -> a
minimum :: forall a. Ord a => PairF scope a -> a
$csum :: forall scope a. Num a => PairF scope a -> a
sum :: forall a. Num a => PairF scope a -> a
$cproduct :: forall scope a. Num a => PairF scope a -> a
product :: forall a. Num a => PairF scope a -> a
Foldable, Functor (PairF scope)
Foldable (PairF scope)
(Functor (PairF scope), Foldable (PairF scope)) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> PairF scope a -> f (PairF scope b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    PairF scope (f a) -> f (PairF scope a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> PairF scope a -> m (PairF scope b))
-> (forall (m :: * -> *) a.
    Monad m =>
    PairF scope (m a) -> m (PairF scope a))
-> Traversable (PairF scope)
forall scope. Functor (PairF scope)
forall scope. Foldable (PairF scope)
forall scope (m :: * -> *) a.
Monad m =>
PairF scope (m a) -> m (PairF scope a)
forall scope (f :: * -> *) a.
Applicative f =>
PairF scope (f a) -> f (PairF scope a)
forall scope (m :: * -> *) a b.
Monad m =>
(a -> m b) -> PairF scope a -> m (PairF scope b)
forall scope (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> PairF scope a -> f (PairF scope b)
forall (t :: * -> *).
(Functor t, Foldable t) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a.
Monad m =>
PairF scope (m a) -> m (PairF scope a)
forall (f :: * -> *) a.
Applicative f =>
PairF scope (f a) -> f (PairF scope a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> PairF scope a -> m (PairF scope b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> PairF scope a -> f (PairF scope b)
$ctraverse :: forall scope (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> PairF scope a -> f (PairF scope b)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> PairF scope a -> f (PairF scope b)
$csequenceA :: forall scope (f :: * -> *) a.
Applicative f =>
PairF scope (f a) -> f (PairF scope a)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
PairF scope (f a) -> f (PairF scope a)
$cmapM :: forall scope (m :: * -> *) a b.
Monad m =>
(a -> m b) -> PairF scope a -> m (PairF scope b)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> PairF scope a -> m (PairF scope b)
$csequence :: forall scope (m :: * -> *) a.
Monad m =>
PairF scope (m a) -> m (PairF scope a)
sequence :: forall (m :: * -> *) a.
Monad m =>
PairF scope (m a) -> m (PairF scope a)
Traversable)
deriveBifunctor ''PairF
deriveBifoldable ''PairF
deriveBitraversable ''PairF
deriveGenericK ''PairF
instance ZipMatchK PairF

-- | Sum of signature bifunctors.
type (:+:) = Sum

-- | \(\lambda\Pi\)-terms in scope @n@, freely generated from the sum of signatures 'LambdaPiF' and t'PairF'.
type LambdaPi n = AST Foil.NameBinder (LambdaPiF :+: PairF) n

pattern App :: LambdaPi n -> LambdaPi n -> LambdaPi n
pattern $mApp :: forall {r} {n :: S}.
LambdaPi n -> (LambdaPi n -> LambdaPi n -> r) -> ((# #) -> r) -> r
$bApp :: forall (n :: S). LambdaPi n -> LambdaPi n -> LambdaPi n
App fun arg = Node (L2 (AppF fun arg))

pattern Lam :: Foil.NameBinder n l -> LambdaPi l -> LambdaPi n
pattern $mLam :: forall {r} {n :: S}.
LambdaPi n
-> (forall {l :: S}. NameBinder n l -> LambdaPi l -> r)
-> ((# #) -> r)
-> r
$bLam :: forall (n :: S) (l :: S).
NameBinder n l -> LambdaPi l -> LambdaPi n
Lam binder body = Node (L2 (LamF (ScopedAST binder body)))

pattern Pi :: Foil.NameBinder n l -> LambdaPi n -> LambdaPi l -> LambdaPi n
pattern $mPi :: forall {r} {n :: S}.
LambdaPi n
-> (forall {l :: S}.
    NameBinder n l -> LambdaPi n -> LambdaPi l -> r)
-> ((# #) -> r)
-> r
$bPi :: forall (n :: S) (l :: S).
NameBinder n l -> LambdaPi n -> LambdaPi l -> LambdaPi n
Pi binder a b = Node (L2 (PiF a (ScopedAST binder b)))

pattern Pair :: LambdaPi n -> LambdaPi n -> LambdaPi n
pattern $mPair :: forall {r} {n :: S}.
LambdaPi n -> (LambdaPi n -> LambdaPi n -> r) -> ((# #) -> r) -> r
$bPair :: forall (n :: S). LambdaPi n -> LambdaPi n -> LambdaPi n
Pair l r = Node (R2 (PairF l r))

pattern First :: LambdaPi n -> LambdaPi n
pattern $mFirst :: forall {r} {n :: S}.
LambdaPi n -> (LambdaPi n -> r) -> ((# #) -> r) -> r
$bFirst :: forall (n :: S). LambdaPi n -> LambdaPi n
First t = Node (R2 (FirstF t))

pattern Second :: LambdaPi n -> LambdaPi n
pattern $mSecond :: forall {r} {n :: S}.
LambdaPi n -> (LambdaPi n -> r) -> ((# #) -> r) -> r
$bSecond :: forall (n :: S). LambdaPi n -> LambdaPi n
Second t = Node (R2 (SecondF t))

pattern Product :: LambdaPi n -> LambdaPi n -> LambdaPi n
pattern $mProduct :: forall {r} {n :: S}.
LambdaPi n -> (LambdaPi n -> LambdaPi n -> r) -> ((# #) -> r) -> r
$bProduct :: forall (n :: S). LambdaPi n -> LambdaPi n -> LambdaPi n
Product l r = Node (R2 (ProductF l r))

pattern Universe :: LambdaPi n
pattern $mUniverse :: forall {r} {n :: S}.
LambdaPi n -> ((# #) -> r) -> ((# #) -> r) -> r
$bUniverse :: forall (n :: S). LambdaPi n
Universe = Node (L2 UniverseF)

{-# COMPLETE Var, App, Lam, Pi, Pair, First, Second, Product, Universe #-}

-- | \(\lambda\Pi\)-terms are pretty-printed using BNFC-generated printer via 'Raw.Term'.
instance Show (LambdaPi Foil.VoidS) where
  show :: LambdaPi 'VoidS -> String
show = LambdaPi 'VoidS -> String
ppLambdaPi

-- | \(\lambda\Pi\)-terms can be (unsafely) parsed from a 'String' via 'Raw.Term'.
instance IsString (LambdaPi Foil.VoidS) where
  fromString :: String -> LambdaPi 'VoidS
fromString String
input =
    case [Token] -> Err Term
Raw.pTerm (String -> [Token]
Raw.tokens String
input) of
      Left String
err -> String -> LambdaPi '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 -> LambdaPi 'VoidS
toLambdaPiClosed Term
term

-- | Compute weak head normal form (WHNF) of a \(\lambda\Pi\)-term.
--
-- >>> whnf Foil.emptyScope "(λx.(λ_.x)(λy.x))(λy.λz.z)"
-- λ x0 . λ x1 . x1
--
-- >>> whnf Foil.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 Foil.emptyScope "(λx.λy.x)(λx.x)"
-- λ x1 . λ x0 . x0
--
-- At the same time, without substitution, we get regular, increasing binder indices:
--
-- >>> "λx.λy.y" :: LambdaPi Foil.VoidS
-- λ x0 . λ x1 . x1
--
-- To compare terms for \(\alpha\)-equivalence, we may use 'alphaEquiv':
--
-- >>> alphaEquiv Foil.emptyScope (whnf Foil.emptyScope "(λx.λy.x)(λx.x)") "λx.λy.y"
-- True
--
-- We may also normalize binders using 'refreshAST':
--
-- >>> refreshAST Foil.emptyScope (whnf Foil.emptyScope "(λx.λy.x)(λx.x)")
-- λ x0 . λ x1 . x1
whnf :: Foil.Distinct n => Foil.Scope n -> LambdaPi n -> LambdaPi n
whnf :: forall (n :: S). Distinct n => Scope n -> LambdaPi n -> LambdaPi n
whnf Scope n
scope = \case
  App LambdaPi n
fun LambdaPi n
arg ->
    case Scope n -> LambdaPi n -> LambdaPi n
forall (n :: S). Distinct n => Scope n -> LambdaPi n -> LambdaPi n
whnf Scope n
scope LambdaPi n
fun of
      Lam NameBinder n l
binder LambdaPi l
body ->
        let subst :: Substitution (AST NameBinder (LambdaPiF :+: PairF)) l n
subst = Substitution (AST NameBinder (LambdaPiF :+: PairF)) n n
-> NameBinder n l
-> LambdaPi n
-> Substitution (AST NameBinder (LambdaPiF :+: PairF)) l n
forall (e :: S -> *) (i :: S) (o :: S) (i' :: S).
Substitution e i o -> NameBinder i i' -> e o -> Substitution e i' o
Foil.addSubst Substitution (AST NameBinder (LambdaPiF :+: PairF)) n n
forall (e :: S -> *) (i :: S). InjectName e => Substitution e i i
Foil.identitySubst NameBinder n l
binder LambdaPi n
arg
        in Scope n -> LambdaPi n -> LambdaPi n
forall (n :: S). Distinct n => Scope n -> LambdaPi n -> LambdaPi n
whnf Scope n
scope (Scope n
-> Substitution (AST NameBinder (LambdaPiF :+: PairF)) l n
-> LambdaPi l
-> LambdaPi n
forall (sig :: * -> * -> *) (o :: S) (binder :: S -> S -> *)
       (i :: S).
(Bifunctor sig, Distinct o, CoSinkable binder, SinkableK binder) =>
Scope o
-> Substitution (AST binder sig) i o
-> AST binder sig i
-> AST binder sig o
substitute Scope n
scope Substitution (AST NameBinder (LambdaPiF :+: PairF)) l n
subst LambdaPi l
body)
      LambdaPi n
fun' -> LambdaPi n -> LambdaPi n -> LambdaPi n
forall (n :: S). LambdaPi n -> LambdaPi n -> LambdaPi n
App LambdaPi n
fun' LambdaPi n
arg
  First LambdaPi n
t ->
    case Scope n -> LambdaPi n -> LambdaPi n
forall (n :: S). Distinct n => Scope n -> LambdaPi n -> LambdaPi n
whnf Scope n
scope LambdaPi n
t of
      Pair LambdaPi n
l LambdaPi n
_r -> Scope n -> LambdaPi n -> LambdaPi n
forall (n :: S). Distinct n => Scope n -> LambdaPi n -> LambdaPi n
whnf Scope n
scope LambdaPi n
l
      LambdaPi n
t'        -> LambdaPi n -> LambdaPi n
forall (n :: S). LambdaPi n -> LambdaPi n
First LambdaPi n
t'
  Second LambdaPi n
t ->
    case Scope n -> LambdaPi n -> LambdaPi n
forall (n :: S). Distinct n => Scope n -> LambdaPi n -> LambdaPi n
whnf Scope n
scope LambdaPi n
t of
      Pair LambdaPi n
_l LambdaPi n
r -> Scope n -> LambdaPi n -> LambdaPi n
forall (n :: S). Distinct n => Scope n -> LambdaPi n -> LambdaPi n
whnf Scope n
scope LambdaPi n
r
      LambdaPi n
t'        -> LambdaPi n -> LambdaPi n
forall (n :: S). LambdaPi n -> LambdaPi n
Second LambdaPi n
t'
  LambdaPi n
t -> LambdaPi n
t

-- | Convert a raw \(\lambda\)-abstraction into a scope-safe \(\lambda\Pi\)-term.
toLambdaPiLam
  :: Foil.Distinct n
  => Foil.Scope n                   -- ^ Target scope of the \(\lambda\Pi\)-term.
  -> Map Raw.VarIdent (Foil.Name n) -- ^ Mapping for the free variables in the raw term.
  -> Raw.Pattern                    -- ^ Raw pattern (argument) of the \(\lambda\)-abstraction.
  -> Raw.ScopedTerm                 -- ^ Raw body of the \(\lambda\)-abstraction.
  -> LambdaPi n
toLambdaPiLam :: forall (n :: S).
Distinct n =>
Scope n
-> Map VarIdent (Name n) -> Pattern -> ScopedTerm -> LambdaPi n
toLambdaPiLam Scope n
scope Map VarIdent (Name n)
env Pattern
pat (Raw.AScopedTerm BNFC'Position
_loc Term
body) =
  case Pattern
pat of
    Raw.PatternWildcard BNFC'Position
_loc -> Scope n
-> (forall {l :: S}. DExt n l => NameBinder n l -> LambdaPi n)
-> LambdaPi n
forall (n :: S) r.
Distinct n =>
Scope n -> (forall (l :: S). DExt n l => NameBinder n l -> r) -> r
Foil.withFresh Scope n
scope ((forall {l :: S}. DExt n l => NameBinder n l -> LambdaPi n)
 -> LambdaPi n)
-> (forall {l :: S}. DExt n l => NameBinder n l -> LambdaPi n)
-> LambdaPi n
forall a b. (a -> b) -> a -> b
$ \NameBinder n l
binder ->
      let scope' :: Scope l
scope' = NameBinder n l -> Scope n -> Scope l
forall (n :: S) (l :: S). NameBinder n l -> Scope n -> Scope l
Foil.extendScope NameBinder n l
binder Scope n
scope
       in NameBinder n l -> LambdaPi l -> LambdaPi n
forall (n :: S) (l :: S).
NameBinder n l -> LambdaPi l -> LambdaPi n
Lam NameBinder n l
binder (Scope l -> Map VarIdent (Name l) -> Term -> LambdaPi l
forall (n :: S).
Distinct n =>
Scope n -> Map VarIdent (Name n) -> Term -> LambdaPi n
toLambdaPi Scope l
scope' (Name n -> Name l
forall (e :: S -> *) (n :: S) (l :: S).
(Sinkable e, DExt n l) =>
e n -> e l
Foil.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) Term
body)

    Raw.PatternVar BNFC'Position
_loc VarIdent
x -> Scope n
-> (forall {l :: S}. DExt n l => NameBinder n l -> LambdaPi n)
-> LambdaPi n
forall (n :: S) r.
Distinct n =>
Scope n -> (forall (l :: S). DExt n l => NameBinder n l -> r) -> r
Foil.withFresh Scope n
scope ((forall {l :: S}. DExt n l => NameBinder n l -> LambdaPi n)
 -> LambdaPi n)
-> (forall {l :: S}. DExt n l => NameBinder n l -> LambdaPi n)
-> LambdaPi n
forall a b. (a -> b) -> a -> b
$ \NameBinder n l
binder ->
      let scope' :: Scope l
scope' = NameBinder n l -> Scope n -> Scope l
forall (n :: S) (l :: S). NameBinder n l -> Scope n -> Scope l
Foil.extendScope NameBinder n l
binder Scope n
scope
          env' :: Map VarIdent (Name l)
env' = 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
Foil.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
Foil.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)
       in NameBinder n l -> LambdaPi l -> LambdaPi n
forall (n :: S) (l :: S).
NameBinder n l -> LambdaPi l -> LambdaPi n
Lam NameBinder n l
binder (Scope l -> Map VarIdent (Name l) -> Term -> LambdaPi l
forall (n :: S).
Distinct n =>
Scope n -> Map VarIdent (Name n) -> Term -> LambdaPi n
toLambdaPi Scope l
scope' Map VarIdent (Name l)
env' Term
body)

    Raw.PatternPair{} -> String -> LambdaPi n
forall a. HasCallStack => String -> a
error String
"pattern pairs are not supported in the FreeFoil example"

-- | Convert a raw \(\Pi\)-type into a scope-safe \(\lambda\Pi\)-term.
toLambdaPiPi
  :: Foil.Distinct n
  => Foil.Scope n                   -- ^ Target scope of the \(\lambda\Pi\)-term.
  -> Map Raw.VarIdent (Foil.Name n) -- ^ Mapping for the free variables in the raw term.
  -> Raw.Pattern                    -- ^ Raw argument pattern of the \(\Pi\)-type.
  -> Raw.Term                       -- ^ Raw argument type of the \(\Pi\)-type.
  -> Raw.ScopedTerm                 -- ^ Raw body (result type family) of the \(\Pi\)-type.
  -> LambdaPi n
toLambdaPiPi :: forall (n :: S).
Distinct n =>
Scope n
-> Map VarIdent (Name n)
-> Pattern
-> Term
-> ScopedTerm
-> LambdaPi n
toLambdaPiPi Scope n
scope Map VarIdent (Name n)
env Pattern
pat Term
a (Raw.AScopedTerm BNFC'Position
_loc Term
b) =
  case Pattern
pat of
    Raw.PatternWildcard BNFC'Position
_loc -> Scope n
-> (forall {l :: S}. DExt n l => NameBinder n l -> LambdaPi n)
-> LambdaPi n
forall (n :: S) r.
Distinct n =>
Scope n -> (forall (l :: S). DExt n l => NameBinder n l -> r) -> r
Foil.withFresh Scope n
scope ((forall {l :: S}. DExt n l => NameBinder n l -> LambdaPi n)
 -> LambdaPi n)
-> (forall {l :: S}. DExt n l => NameBinder n l -> LambdaPi n)
-> LambdaPi n
forall a b. (a -> b) -> a -> b
$ \NameBinder n l
binder ->
      let scope' :: Scope l
scope' = NameBinder n l -> Scope n -> Scope l
forall (n :: S) (l :: S). NameBinder n l -> Scope n -> Scope l
Foil.extendScope NameBinder n l
binder Scope n
scope
       in NameBinder n l -> LambdaPi n -> LambdaPi l -> LambdaPi n
forall (n :: S) (l :: S).
NameBinder n l -> LambdaPi n -> LambdaPi l -> LambdaPi n
Pi NameBinder n l
binder (Scope n -> Map VarIdent (Name n) -> Term -> LambdaPi n
forall (n :: S).
Distinct n =>
Scope n -> Map VarIdent (Name n) -> Term -> LambdaPi n
toLambdaPi Scope n
scope Map VarIdent (Name n)
env Term
a) (Scope l -> Map VarIdent (Name l) -> Term -> LambdaPi l
forall (n :: S).
Distinct n =>
Scope n -> Map VarIdent (Name n) -> Term -> LambdaPi n
toLambdaPi Scope l
scope' (Name n -> Name l
forall (e :: S -> *) (n :: S) (l :: S).
(Sinkable e, DExt n l) =>
e n -> e l
Foil.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) Term
b)

    Raw.PatternVar BNFC'Position
_loc VarIdent
x -> Scope n
-> (forall {l :: S}. DExt n l => NameBinder n l -> LambdaPi n)
-> LambdaPi n
forall (n :: S) r.
Distinct n =>
Scope n -> (forall (l :: S). DExt n l => NameBinder n l -> r) -> r
Foil.withFresh Scope n
scope ((forall {l :: S}. DExt n l => NameBinder n l -> LambdaPi n)
 -> LambdaPi n)
-> (forall {l :: S}. DExt n l => NameBinder n l -> LambdaPi n)
-> LambdaPi n
forall a b. (a -> b) -> a -> b
$ \NameBinder n l
binder ->
      let scope' :: Scope l
scope' = NameBinder n l -> Scope n -> Scope l
forall (n :: S) (l :: S). NameBinder n l -> Scope n -> Scope l
Foil.extendScope NameBinder n l
binder Scope n
scope
          env' :: Map VarIdent (Name l)
env' = 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
Foil.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
Foil.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)
       in NameBinder n l -> LambdaPi n -> LambdaPi l -> LambdaPi n
forall (n :: S) (l :: S).
NameBinder n l -> LambdaPi n -> LambdaPi l -> LambdaPi n
Pi NameBinder n l
binder (Scope n -> Map VarIdent (Name n) -> Term -> LambdaPi n
forall (n :: S).
Distinct n =>
Scope n -> Map VarIdent (Name n) -> Term -> LambdaPi n
toLambdaPi Scope n
scope Map VarIdent (Name n)
env Term
a) (Scope l -> Map VarIdent (Name l) -> Term -> LambdaPi l
forall (n :: S).
Distinct n =>
Scope n -> Map VarIdent (Name n) -> Term -> LambdaPi n
toLambdaPi Scope l
scope' Map VarIdent (Name l)
env' Term
b)

    Raw.PatternPair{} -> String -> LambdaPi n
forall a. HasCallStack => String -> a
error String
"pattern pairs are not supported in the FreeFoil example"

-- | Convert a raw expression into a scope-safe \(\lambda\Pi\)-term.
toLambdaPi
  :: Foil.Distinct n
  => Foil.Scope n                   -- ^ Target scope of the \(\lambda\Pi\)-term.
  -> Map Raw.VarIdent (Foil.Name n) -- ^ Mapping for the free variables in the raw term.
  -> Raw.Term                       -- ^ Raw expression or type.
  -> LambdaPi n
toLambdaPi :: forall (n :: S).
Distinct n =>
Scope n -> Map VarIdent (Name n) -> Term -> LambdaPi n
toLambdaPi 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 -> LambdaPi n
forall (n :: S) (binder :: S -> S -> *) (sig :: * -> * -> *).
Name n -> AST binder sig n
Var Name n
name
      Maybe (Name n)
Nothing   -> String -> LambdaPi n
forall a. HasCallStack => String -> a
error (String
"unbound variable: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ VarIdent -> String
forall a. Print a => a -> String
Raw.printTree VarIdent
x)

  Raw.App BNFC'Position
_loc Term
fun Term
arg ->
    LambdaPi n -> LambdaPi n -> LambdaPi n
forall (n :: S). LambdaPi n -> LambdaPi n -> LambdaPi n
App (Scope n -> Map VarIdent (Name n) -> Term -> LambdaPi n
forall (n :: S).
Distinct n =>
Scope n -> Map VarIdent (Name n) -> Term -> LambdaPi n
toLambdaPi Scope n
scope Map VarIdent (Name n)
env Term
fun) (Scope n -> Map VarIdent (Name n) -> Term -> LambdaPi n
forall (n :: S).
Distinct n =>
Scope n -> Map VarIdent (Name n) -> Term -> LambdaPi n
toLambdaPi Scope n
scope Map VarIdent (Name n)
env Term
arg)

  Raw.Lam BNFC'Position
_loc Pattern
pat ScopedTerm
body -> Scope n
-> Map VarIdent (Name n) -> Pattern -> ScopedTerm -> LambdaPi n
forall (n :: S).
Distinct n =>
Scope n
-> Map VarIdent (Name n) -> Pattern -> ScopedTerm -> LambdaPi n
toLambdaPiLam Scope n
scope Map VarIdent (Name n)
env Pattern
pat ScopedTerm
body
  Raw.Pi BNFC'Position
_loc Pattern
pat Term
a ScopedTerm
b -> Scope n
-> Map VarIdent (Name n)
-> Pattern
-> Term
-> ScopedTerm
-> LambdaPi n
forall (n :: S).
Distinct n =>
Scope n
-> Map VarIdent (Name n)
-> Pattern
-> Term
-> ScopedTerm
-> LambdaPi n
toLambdaPiPi Scope n
scope Map VarIdent (Name n)
env Pattern
pat Term
a ScopedTerm
b

  Raw.Pair BNFC'Position
_loc Term
l Term
r -> LambdaPi n -> LambdaPi n -> LambdaPi n
forall (n :: S). LambdaPi n -> LambdaPi n -> LambdaPi n
Pair (Scope n -> Map VarIdent (Name n) -> Term -> LambdaPi n
forall (n :: S).
Distinct n =>
Scope n -> Map VarIdent (Name n) -> Term -> LambdaPi n
toLambdaPi Scope n
scope Map VarIdent (Name n)
env Term
l) (Scope n -> Map VarIdent (Name n) -> Term -> LambdaPi n
forall (n :: S).
Distinct n =>
Scope n -> Map VarIdent (Name n) -> Term -> LambdaPi n
toLambdaPi Scope n
scope Map VarIdent (Name n)
env Term
r)
  Raw.First BNFC'Position
_loc Term
t -> LambdaPi n -> LambdaPi n
forall (n :: S). LambdaPi n -> LambdaPi n
First (Scope n -> Map VarIdent (Name n) -> Term -> LambdaPi n
forall (n :: S).
Distinct n =>
Scope n -> Map VarIdent (Name n) -> Term -> LambdaPi n
toLambdaPi Scope n
scope Map VarIdent (Name n)
env Term
t)
  Raw.Second BNFC'Position
_loc Term
t -> LambdaPi n -> LambdaPi n
forall (n :: S). LambdaPi n -> LambdaPi n
Second (Scope n -> Map VarIdent (Name n) -> Term -> LambdaPi n
forall (n :: S).
Distinct n =>
Scope n -> Map VarIdent (Name n) -> Term -> LambdaPi n
toLambdaPi Scope n
scope Map VarIdent (Name n)
env Term
t)
  Raw.Product BNFC'Position
_loc Term
l Term
r -> LambdaPi n -> LambdaPi n -> LambdaPi n
forall (n :: S). LambdaPi n -> LambdaPi n -> LambdaPi n
Product (Scope n -> Map VarIdent (Name n) -> Term -> LambdaPi n
forall (n :: S).
Distinct n =>
Scope n -> Map VarIdent (Name n) -> Term -> LambdaPi n
toLambdaPi Scope n
scope Map VarIdent (Name n)
env Term
l) (Scope n -> Map VarIdent (Name n) -> Term -> LambdaPi n
forall (n :: S).
Distinct n =>
Scope n -> Map VarIdent (Name n) -> Term -> LambdaPi n
toLambdaPi Scope n
scope Map VarIdent (Name n)
env Term
r)

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

-- | Convert a raw expression into a /closed/ scope-safe \(\lambda\Pi\)-term.
toLambdaPiClosed :: Raw.Term -> LambdaPi Foil.VoidS
toLambdaPiClosed :: Term -> LambdaPi 'VoidS
toLambdaPiClosed = Scope 'VoidS
-> Map VarIdent (Name 'VoidS) -> Term -> LambdaPi 'VoidS
forall (n :: S).
Distinct n =>
Scope n -> Map VarIdent (Name n) -> Term -> LambdaPi n
toLambdaPi Scope 'VoidS
Foil.emptyScope Map VarIdent (Name 'VoidS)
forall k a. Map k a
Map.empty

-- | Convert back from a scope-safe \(\lambda\Pi\)-term into a raw expression or type.
fromLambdaPi
  :: [Raw.VarIdent]               -- ^ Stream of fresh raw identifiers.
  -> Foil.NameMap n Raw.VarIdent  -- ^ A /total/ map for all names in scope @n@.
  -> LambdaPi n                   -- ^ A scope-safe \(\lambda\Pi\)-term.
  -> Raw.Term
fromLambdaPi :: forall (n :: S).
[VarIdent] -> NameMap n VarIdent -> LambdaPi n -> Term
fromLambdaPi [VarIdent]
freshVars NameMap n VarIdent
env = \case
  Var 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
Foil.lookupName Name n
name NameMap n VarIdent
env)
  App LambdaPi n
fun LambdaPi n
arg -> 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 -> LambdaPi n -> Term
forall (n :: S).
[VarIdent] -> NameMap n VarIdent -> LambdaPi n -> Term
fromLambdaPi [VarIdent]
freshVars NameMap n VarIdent
env LambdaPi n
fun) ([VarIdent] -> NameMap n VarIdent -> LambdaPi n -> Term
forall (n :: S).
[VarIdent] -> NameMap n VarIdent -> LambdaPi n -> Term
fromLambdaPi [VarIdent]
freshVars NameMap n VarIdent
env LambdaPi n
arg)
  Lam NameBinder n l
binder LambdaPi l
body ->
    case [VarIdent]
freshVars of
      [] -> String -> Term
forall a. HasCallStack => String -> a
error String
"not enough fresh variables"
      VarIdent
x:[VarIdent]
freshVars' ->
        let env' :: NameMap l VarIdent
env' = 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
Foil.addNameBinder NameBinder n l
binder VarIdent
x NameMap n VarIdent
env
         in BNFC'Position -> Pattern -> ScopedTerm -> Term
forall a. a -> Pattern' a -> ScopedTerm' a -> Term' a
Raw.Lam BNFC'Position
forall {a}. a
loc (BNFC'Position -> VarIdent -> Pattern
forall a. a -> VarIdent -> Pattern' a
Raw.PatternVar BNFC'Position
forall {a}. a
loc VarIdent
x) (BNFC'Position -> Term -> ScopedTerm
forall a. a -> Term' a -> ScopedTerm' a
Raw.AScopedTerm BNFC'Position
forall {a}. a
loc ([VarIdent] -> NameMap l VarIdent -> LambdaPi l -> Term
forall (n :: S).
[VarIdent] -> NameMap n VarIdent -> LambdaPi n -> Term
fromLambdaPi [VarIdent]
freshVars' NameMap l VarIdent
env' LambdaPi l
body))
  Pi NameBinder n l
binder LambdaPi n
a LambdaPi l
b ->
    case [VarIdent]
freshVars of
      [] -> String -> Term
forall a. HasCallStack => String -> a
error String
"not enough fresh variables"
      VarIdent
x:[VarIdent]
freshVars' ->
        let env' :: NameMap l VarIdent
env' = 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
Foil.addNameBinder NameBinder n l
binder VarIdent
x NameMap n VarIdent
env
         in BNFC'Position -> Pattern -> Term -> ScopedTerm -> Term
forall a. a -> Pattern' a -> Term' a -> ScopedTerm' a -> Term' a
Raw.Pi BNFC'Position
forall {a}. a
loc (BNFC'Position -> VarIdent -> Pattern
forall a. a -> VarIdent -> Pattern' a
Raw.PatternVar BNFC'Position
forall {a}. a
loc VarIdent
x) ([VarIdent] -> NameMap n VarIdent -> LambdaPi n -> Term
forall (n :: S).
[VarIdent] -> NameMap n VarIdent -> LambdaPi n -> Term
fromLambdaPi [VarIdent]
freshVars NameMap n VarIdent
env LambdaPi n
a) (BNFC'Position -> Term -> ScopedTerm
forall a. a -> Term' a -> ScopedTerm' a
Raw.AScopedTerm BNFC'Position
forall {a}. a
loc ([VarIdent] -> NameMap l VarIdent -> LambdaPi l -> Term
forall (n :: S).
[VarIdent] -> NameMap n VarIdent -> LambdaPi n -> Term
fromLambdaPi [VarIdent]
freshVars' NameMap l VarIdent
env' LambdaPi l
b))
  Pair LambdaPi n
l LambdaPi n
r -> 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 -> LambdaPi n -> Term
forall (n :: S).
[VarIdent] -> NameMap n VarIdent -> LambdaPi n -> Term
fromLambdaPi [VarIdent]
freshVars NameMap n VarIdent
env LambdaPi n
l) ([VarIdent] -> NameMap n VarIdent -> LambdaPi n -> Term
forall (n :: S).
[VarIdent] -> NameMap n VarIdent -> LambdaPi n -> Term
fromLambdaPi [VarIdent]
freshVars NameMap n VarIdent
env LambdaPi n
r)
  First LambdaPi 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 -> LambdaPi n -> Term
forall (n :: S).
[VarIdent] -> NameMap n VarIdent -> LambdaPi n -> Term
fromLambdaPi [VarIdent]
freshVars NameMap n VarIdent
env LambdaPi n
t)
  Second LambdaPi 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 -> LambdaPi n -> Term
forall (n :: S).
[VarIdent] -> NameMap n VarIdent -> LambdaPi n -> Term
fromLambdaPi [VarIdent]
freshVars NameMap n VarIdent
env LambdaPi n
t)
  Product LambdaPi n
l LambdaPi n
r -> 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 -> LambdaPi n -> Term
forall (n :: S).
[VarIdent] -> NameMap n VarIdent -> LambdaPi n -> Term
fromLambdaPi [VarIdent]
freshVars NameMap n VarIdent
env LambdaPi n
l) ([VarIdent] -> NameMap n VarIdent -> LambdaPi n -> Term
forall (n :: S).
[VarIdent] -> NameMap n VarIdent -> LambdaPi n -> Term
fromLambdaPi [VarIdent]
freshVars NameMap n VarIdent
env LambdaPi n
r)
  LambdaPi n
Universe -> 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
"no location info available when converting from an AST"

-- | Convert back from a scope-safe \(\lambda\Pi\)-term into a raw expression or type.
--
-- In contrast to 'fromLambdaPi', this function uses the raw foil identifiers (integers)
-- to generate names for the variables. This makes them transparent when printing.
fromLambdaPi'
  :: LambdaPi n                   -- ^ A scope-safe \(\lambda\Pi\)-term.
  -> Raw.Term
fromLambdaPi' :: forall (n :: S). LambdaPi n -> Term
fromLambdaPi' = \case
  Var 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
ppName Name n
name)
  App LambdaPi n
fun LambdaPi n
arg -> BNFC'Position -> Term -> Term -> Term
forall a. a -> Term' a -> Term' a -> Term' a
Raw.App BNFC'Position
forall {a}. a
loc (LambdaPi n -> Term
forall (n :: S). LambdaPi n -> Term
fromLambdaPi' LambdaPi n
fun) (LambdaPi n -> Term
forall (n :: S). LambdaPi n -> Term
fromLambdaPi' LambdaPi n
arg)
  Lam NameBinder n l
binder LambdaPi l
body ->
    let x :: VarIdent
x = Name l -> VarIdent
forall {l :: S}. Name l -> VarIdent
ppName (NameBinder n l -> Name l
forall (n :: S) (l :: S). NameBinder n l -> Name l
Foil.nameOf NameBinder n l
binder)
     in BNFC'Position -> Pattern -> ScopedTerm -> Term
forall a. a -> Pattern' a -> ScopedTerm' a -> Term' a
Raw.Lam BNFC'Position
forall {a}. a
loc (BNFC'Position -> VarIdent -> Pattern
forall a. a -> VarIdent -> Pattern' a
Raw.PatternVar BNFC'Position
forall {a}. a
loc VarIdent
x) (BNFC'Position -> Term -> ScopedTerm
forall a. a -> Term' a -> ScopedTerm' a
Raw.AScopedTerm BNFC'Position
forall {a}. a
loc (LambdaPi l -> Term
forall (n :: S). LambdaPi n -> Term
fromLambdaPi' LambdaPi l
body))
  Pi NameBinder n l
binder LambdaPi n
a LambdaPi l
b ->
    let x :: VarIdent
x = Name l -> VarIdent
forall {l :: S}. Name l -> VarIdent
ppName (NameBinder n l -> Name l
forall (n :: S) (l :: S). NameBinder n l -> Name l
Foil.nameOf NameBinder n l
binder)
     in BNFC'Position -> Pattern -> Term -> ScopedTerm -> Term
forall a. a -> Pattern' a -> Term' a -> ScopedTerm' a -> Term' a
Raw.Pi BNFC'Position
forall {a}. a
loc (BNFC'Position -> VarIdent -> Pattern
forall a. a -> VarIdent -> Pattern' a
Raw.PatternVar BNFC'Position
forall {a}. a
loc VarIdent
x) (LambdaPi n -> Term
forall (n :: S). LambdaPi n -> Term
fromLambdaPi' LambdaPi n
a) (BNFC'Position -> Term -> ScopedTerm
forall a. a -> Term' a -> ScopedTerm' a
Raw.AScopedTerm BNFC'Position
forall {a}. a
loc (LambdaPi l -> Term
forall (n :: S). LambdaPi n -> Term
fromLambdaPi' LambdaPi l
b))
  Pair LambdaPi n
l LambdaPi n
r -> BNFC'Position -> Term -> Term -> Term
forall a. a -> Term' a -> Term' a -> Term' a
Raw.Pair BNFC'Position
forall {a}. a
loc (LambdaPi n -> Term
forall (n :: S). LambdaPi n -> Term
fromLambdaPi' LambdaPi n
l) (LambdaPi n -> Term
forall (n :: S). LambdaPi n -> Term
fromLambdaPi' LambdaPi n
r)
  First LambdaPi n
t -> BNFC'Position -> Term -> Term
forall a. a -> Term' a -> Term' a
Raw.First BNFC'Position
forall {a}. a
loc (LambdaPi n -> Term
forall (n :: S). LambdaPi n -> Term
fromLambdaPi' LambdaPi n
t)
  Second LambdaPi n
t -> BNFC'Position -> Term -> Term
forall a. a -> Term' a -> Term' a
Raw.Second BNFC'Position
forall {a}. a
loc (LambdaPi n -> Term
forall (n :: S). LambdaPi n -> Term
fromLambdaPi' LambdaPi n
t)
  Product LambdaPi n
l LambdaPi n
r -> BNFC'Position -> Term -> Term -> Term
forall a. a -> Term' a -> Term' a -> Term' a
Raw.Product BNFC'Position
forall {a}. a
loc (LambdaPi n -> Term
forall (n :: S). LambdaPi n -> Term
fromLambdaPi' LambdaPi n
l) (LambdaPi n -> Term
forall (n :: S). LambdaPi n -> Term
fromLambdaPi' LambdaPi n
r)
  LambdaPi n
Universe -> 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
"no location info available when converting from an AST"
    ppName :: Name l -> VarIdent
ppName 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
Foil.nameId Name l
name))

-- | Pretty-print a /closed/ \(\lambda\Pi\)-term.
ppLambdaPi :: LambdaPi Foil.VoidS -> String
ppLambdaPi :: LambdaPi 'VoidS -> String
ppLambdaPi = Term -> String
forall a. Print a => a -> String
Raw.printTree (Term -> String)
-> (LambdaPi 'VoidS -> Term) -> LambdaPi 'VoidS -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LambdaPi 'VoidS -> Term
forall (n :: S). LambdaPi n -> Term
fromLambdaPi'

-- | 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]
++ LambdaPi 'VoidS -> String
ppLambdaPi (Scope 'VoidS -> LambdaPi 'VoidS -> LambdaPi 'VoidS
forall (n :: S). Distinct n => Scope n -> LambdaPi n -> LambdaPi n
whnf Scope 'VoidS
Foil.emptyScope (Scope 'VoidS
-> Map VarIdent (Name 'VoidS) -> Term -> LambdaPi 'VoidS
forall (n :: S).
Distinct n =>
Scope n -> Map VarIdent (Name n) -> Term -> LambdaPi n
toLambdaPi Scope 'VoidS
Foil.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
"check is 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

-- | A \(\lambda\Pi\) interpreter implemented via the free foil.
defaultMain :: IO ()
defaultMain :: IO ()
defaultMain = do
  String
input <- IO String
getContents
  case [Token] -> Err Program
Raw.pProgram (Bool -> [Token] -> [Token]
Raw.resolveLayout Bool
True (String -> [Token]
Raw.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