{-# LANGUAGE DataKinds                  #-}
{-# LANGUAGE TypeFamilies               #-}
{-# LANGUAGE DerivingStrategies         #-}
{-# LANGUAGE GADTs                      #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE InstanceSigs               #-}
{-# LANGUAGE KindSignatures             #-}
{-# LANGUAGE LambdaCase                 #-}
{-# LANGUAGE LiberalTypeSynonyms        #-}
{-# LANGUAGE OverloadedStrings          #-}
{-# LANGUAGE RankNTypes                 #-}
{-# LANGUAGE ScopedTypeVariables        #-}
{-# LANGUAGE StandaloneDeriving         #-}
{-# LANGUAGE TemplateHaskell            #-}
{-# LANGUAGE TypeApplications           #-}
-- | Foil implementation of the \(\lambda\Pi\)-calculus (with pairs)
-- using Template Haskell and "Generics.Kind" to reduce boilerplate.
--
-- Template Haskell helpers __generate__ the following:
--
-- 1. Scope-safe AST, generated from a raw definition. See 'FoilTerm', 'FoilScopedTerm', and 'FoilPattern'.
-- 2. Conversion between scope-safe and raw term representation (the latter is generated via BNFC), see 'toFoilTerm'' and 'fromFoilTerm''.
-- 3. Helper functions for patterns. See 'extendScopeFoilPattern'' and 'withRefreshedFoilPattern''.
--
-- The following is provided via kind-polymophic generics (see "Generics.Kind"):
--
-- 1. 'Sinkable' instance for 'FoilTerm''.
-- 2. 'CoSinkable' instance for 'FoilPattern'', giving access to 'extendScopePattern' and 'withRefreshedPattern' (among other utilities).
--
-- The following is implemented __manually__ in this module:
--
-- 1. Correct capture-avoiding substitution (see 'substitute').
-- 2. Computation of weak head normal form (WHNF), see 'whnf'.
-- 3. Entry point, gluing everything together. See 'defaultMain'.
--
-- The following is __not implemented__:
--
-- 1. \(\alpha\)-equivalence checks and \(\alpha\)-normalization helpers.
--
-- This implementation supports (nested) patterns for pairs.
module Language.LambdaPi.Impl.FoilTH where


import           Control.Monad.Foil
import           Control.Monad.Foil.TH
import qualified Data.Map                        as Map
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           Generics.Kind.TH
import           System.Exit                     (exitFailure)

-- * Generated code

-- ** Scope-safe AST
mkFoilData ''Raw.Term' ''Raw.VarIdent ''Raw.ScopedTerm' ''Raw.Pattern'
-- mkInstancesFoil ''Raw.Term' ''Raw.VarIdent ''Raw.ScopedTerm' ''Raw.Pattern'

deriveGenericK ''FoilTerm'
deriveGenericK ''FoilScopedTerm'
deriveGenericK ''FoilPattern'
instance SinkableK (FoilTerm' a)
instance SinkableK (FoilScopedTerm' a)
instance SinkableK (FoilPattern' a)
instance HasNameBinders (FoilPattern' a)

instance Sinkable (FoilTerm' a)
instance CoSinkable (FoilPattern' a)

-- ** Conversion from raw to scope-safe AST
mkToFoil ''Raw.Term' ''Raw.VarIdent ''Raw.ScopedTerm' ''Raw.Pattern'

-- ** Conversion from scope-safe to raw AST
mkFromFoil ''Raw.Term' ''Raw.VarIdent ''Raw.ScopedTerm' ''Raw.Pattern'

type FoilTerm = FoilTerm' Raw.BNFC'Position
type FoilPattern = FoilPattern' Raw.BNFC'Position

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

instance InjectName (FoilTerm' a) where
  injectName :: forall (n :: S). Name n -> FoilTerm' a n
injectName = a -> Name n -> FoilTerm' a n
forall a (n :: S). a -> Name n -> FoilTerm' a n
FoilVar (String -> a
forall a. HasCallStack => String -> a
error String
"undefined location")

-- * User-defined

-- ** Substitution

-- | Perform substitution in a \(\lambda\Pi\)-term.
substitute :: Distinct o => Scope o -> Substitution FoilTerm i o -> FoilTerm i -> FoilTerm o
substitute :: forall (o :: S) (i :: S).
Distinct o =>
Scope o -> Substitution FoilTerm i o -> FoilTerm i -> FoilTerm o
substitute Scope o
scope Substitution FoilTerm i o
subst = \case
    FoilVar BNFC'Position
_loc Name i
name -> Substitution FoilTerm i o -> Name i -> FoilTerm o
forall (e :: S -> *) (i :: S) (o :: S).
InjectName e =>
Substitution e i o -> Name i -> e o
lookupSubst Substitution FoilTerm i o
subst Name i
name
    FoilApp BNFC'Position
loc FoilTerm i
f FoilTerm i
x -> BNFC'Position -> FoilTerm o -> FoilTerm o -> FoilTerm o
forall a (n :: S).
a -> FoilTerm' a n -> FoilTerm' a n -> FoilTerm' a n
FoilApp BNFC'Position
loc (Scope o -> Substitution FoilTerm i o -> FoilTerm i -> FoilTerm o
forall (o :: S) (i :: S).
Distinct o =>
Scope o -> Substitution FoilTerm i o -> FoilTerm i -> FoilTerm o
substitute Scope o
scope Substitution FoilTerm i o
subst FoilTerm i
f) (Scope o -> Substitution FoilTerm i o -> FoilTerm i -> FoilTerm o
forall (o :: S) (i :: S).
Distinct o =>
Scope o -> Substitution FoilTerm i o -> FoilTerm i -> FoilTerm o
substitute Scope o
scope Substitution FoilTerm i o
subst FoilTerm i
x)
    FoilLam BNFC'Position
loc1 FoilPattern' BNFC'Position i l
pattern (FoilAScopedTerm BNFC'Position
loc2 FoilTerm' BNFC'Position l
body) -> Scope o
-> FoilPattern' BNFC'Position i l
-> (forall {o' :: S}.
    DExt o o' =>
    (Substitution FoilTerm i o -> Substitution FoilTerm l o')
    -> FoilPattern' BNFC'Position o o' -> FoilTerm o)
-> FoilTerm 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 FoilPattern' BNFC'Position i l
pattern ((forall {o' :: S}.
  DExt o o' =>
  (Substitution FoilTerm i o -> Substitution FoilTerm l o')
  -> FoilPattern' BNFC'Position o o' -> FoilTerm o)
 -> FoilTerm o)
-> (forall {o' :: S}.
    DExt o o' =>
    (Substitution FoilTerm i o -> Substitution FoilTerm l o')
    -> FoilPattern' BNFC'Position o o' -> FoilTerm o)
-> FoilTerm o
forall a b. (a -> b) -> a -> b
$ \Substitution FoilTerm i o -> Substitution FoilTerm l o'
extendSubst FoilPattern' BNFC'Position o o'
pattern' ->
      let subst' :: Substitution FoilTerm l o'
subst' = Substitution FoilTerm i o -> Substitution FoilTerm l o'
extendSubst Substitution FoilTerm i o
subst
          scope' :: Scope o'
scope' = FoilPattern' BNFC'Position 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 FoilPattern' BNFC'Position o o'
pattern' Scope o
scope
          body' :: FoilTerm o'
body' = Scope o'
-> Substitution FoilTerm l o'
-> FoilTerm' BNFC'Position l
-> FoilTerm o'
forall (o :: S) (i :: S).
Distinct o =>
Scope o -> Substitution FoilTerm i o -> FoilTerm i -> FoilTerm o
substitute Scope o'
scope' Substitution FoilTerm l o'
subst' FoilTerm' BNFC'Position l
body
       in BNFC'Position
-> FoilPattern' BNFC'Position o o'
-> FoilScopedTerm' BNFC'Position o'
-> FoilTerm o
forall a (n :: S) (n2 :: S).
a -> FoilPattern' a n n2 -> FoilScopedTerm' a n2 -> FoilTerm' a n
FoilLam BNFC'Position
loc1 FoilPattern' BNFC'Position o o'
pattern' (BNFC'Position -> FoilTerm o' -> FoilScopedTerm' BNFC'Position o'
forall a (n :: S). a -> FoilTerm' a n -> FoilScopedTerm' a n
FoilAScopedTerm BNFC'Position
loc2 FoilTerm o'
body')
    FoilPi BNFC'Position
loc1 FoilPattern' BNFC'Position i l
pattern FoilTerm i
a (FoilAScopedTerm BNFC'Position
loc2 FoilTerm' BNFC'Position l
b) -> Scope o
-> FoilPattern' BNFC'Position i l
-> (forall {o' :: S}.
    DExt o o' =>
    (Substitution FoilTerm i o -> Substitution FoilTerm l o')
    -> FoilPattern' BNFC'Position o o' -> FoilTerm o)
-> FoilTerm 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 FoilPattern' BNFC'Position i l
pattern ((forall {o' :: S}.
  DExt o o' =>
  (Substitution FoilTerm i o -> Substitution FoilTerm l o')
  -> FoilPattern' BNFC'Position o o' -> FoilTerm o)
 -> FoilTerm o)
-> (forall {o' :: S}.
    DExt o o' =>
    (Substitution FoilTerm i o -> Substitution FoilTerm l o')
    -> FoilPattern' BNFC'Position o o' -> FoilTerm o)
-> FoilTerm o
forall a b. (a -> b) -> a -> b
$ \Substitution FoilTerm i o -> Substitution FoilTerm l o'
extendSubst FoilPattern' BNFC'Position o o'
pattern' ->
      let subst' :: Substitution FoilTerm l o'
subst' = Substitution FoilTerm i o -> Substitution FoilTerm l o'
extendSubst Substitution FoilTerm i o
subst
          scope' :: Scope o'
scope' = FoilPattern' BNFC'Position 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 FoilPattern' BNFC'Position o o'
pattern' Scope o
scope
          a' :: FoilTerm o
a' = Scope o -> Substitution FoilTerm i o -> FoilTerm i -> FoilTerm o
forall (o :: S) (i :: S).
Distinct o =>
Scope o -> Substitution FoilTerm i o -> FoilTerm i -> FoilTerm o
substitute Scope o
scope Substitution FoilTerm i o
subst FoilTerm i
a
          b' :: FoilTerm o'
b' = Scope o'
-> Substitution FoilTerm l o'
-> FoilTerm' BNFC'Position l
-> FoilTerm o'
forall (o :: S) (i :: S).
Distinct o =>
Scope o -> Substitution FoilTerm i o -> FoilTerm i -> FoilTerm o
substitute Scope o'
scope' Substitution FoilTerm l o'
subst' FoilTerm' BNFC'Position l
b
       in BNFC'Position
-> FoilPattern' BNFC'Position o o'
-> FoilTerm o
-> FoilScopedTerm' BNFC'Position o'
-> FoilTerm o
forall a (n :: S) (n2 :: S).
a
-> FoilPattern' a n n2
-> FoilTerm' a n
-> FoilScopedTerm' a n2
-> FoilTerm' a n
FoilPi BNFC'Position
loc1 FoilPattern' BNFC'Position o o'
pattern' FoilTerm o
a' (BNFC'Position -> FoilTerm o' -> FoilScopedTerm' BNFC'Position o'
forall a (n :: S). a -> FoilTerm' a n -> FoilScopedTerm' a n
FoilAScopedTerm BNFC'Position
loc2 FoilTerm o'
b')
    FoilPair BNFC'Position
loc FoilTerm i
l FoilTerm i
r -> BNFC'Position -> FoilTerm o -> FoilTerm o -> FoilTerm o
forall a (n :: S).
a -> FoilTerm' a n -> FoilTerm' a n -> FoilTerm' a n
FoilPair BNFC'Position
loc (Scope o -> Substitution FoilTerm i o -> FoilTerm i -> FoilTerm o
forall (o :: S) (i :: S).
Distinct o =>
Scope o -> Substitution FoilTerm i o -> FoilTerm i -> FoilTerm o
substitute Scope o
scope Substitution FoilTerm i o
subst FoilTerm i
l) (Scope o -> Substitution FoilTerm i o -> FoilTerm i -> FoilTerm o
forall (o :: S) (i :: S).
Distinct o =>
Scope o -> Substitution FoilTerm i o -> FoilTerm i -> FoilTerm o
substitute Scope o
scope Substitution FoilTerm i o
subst FoilTerm i
r)
    FoilFirst BNFC'Position
loc FoilTerm i
t -> BNFC'Position -> FoilTerm o -> FoilTerm o
forall a (n :: S). a -> FoilTerm' a n -> FoilTerm' a n
FoilFirst BNFC'Position
loc (Scope o -> Substitution FoilTerm i o -> FoilTerm i -> FoilTerm o
forall (o :: S) (i :: S).
Distinct o =>
Scope o -> Substitution FoilTerm i o -> FoilTerm i -> FoilTerm o
substitute Scope o
scope Substitution FoilTerm i o
subst FoilTerm i
t)
    FoilSecond BNFC'Position
loc FoilTerm i
t -> BNFC'Position -> FoilTerm o -> FoilTerm o
forall a (n :: S). a -> FoilTerm' a n -> FoilTerm' a n
FoilSecond BNFC'Position
loc (Scope o -> Substitution FoilTerm i o -> FoilTerm i -> FoilTerm o
forall (o :: S) (i :: S).
Distinct o =>
Scope o -> Substitution FoilTerm i o -> FoilTerm i -> FoilTerm o
substitute Scope o
scope Substitution FoilTerm i o
subst FoilTerm i
t)
    FoilProduct BNFC'Position
loc FoilTerm i
l FoilTerm i
r -> BNFC'Position -> FoilTerm o -> FoilTerm o -> FoilTerm o
forall a (n :: S).
a -> FoilTerm' a n -> FoilTerm' a n -> FoilTerm' a n
FoilProduct BNFC'Position
loc (Scope o -> Substitution FoilTerm i o -> FoilTerm i -> FoilTerm o
forall (o :: S) (i :: S).
Distinct o =>
Scope o -> Substitution FoilTerm i o -> FoilTerm i -> FoilTerm o
substitute Scope o
scope Substitution FoilTerm i o
subst FoilTerm i
l) (Scope o -> Substitution FoilTerm i o -> FoilTerm i -> FoilTerm o
forall (o :: S) (i :: S).
Distinct o =>
Scope o -> Substitution FoilTerm i o -> FoilTerm i -> FoilTerm o
substitute Scope o
scope Substitution FoilTerm i o
subst FoilTerm i
r)
    FoilUniverse BNFC'Position
loc -> BNFC'Position -> FoilTerm o
forall a (n :: S). a -> FoilTerm' a n
FoilUniverse BNFC'Position
loc

-- ** Computation

-- | Match a pattern against an expression.
matchPattern :: FoilPattern n l -> FoilTerm n -> Substitution FoilTerm l n
matchPattern :: forall (n :: S) (l :: S).
FoilPattern n l -> FoilTerm n -> Substitution FoilTerm l n
matchPattern FoilPattern n l
pattern FoilTerm n
expr = FoilPattern n l
-> FoilTerm n
-> Substitution FoilTerm n n
-> Substitution FoilTerm l n
forall (i :: S) (l :: S) (n :: S).
FoilPattern i l
-> FoilTerm n
-> Substitution FoilTerm i n
-> Substitution FoilTerm l n
go FoilPattern n l
pattern FoilTerm n
expr Substitution FoilTerm n n
forall (e :: S -> *) (i :: S). InjectName e => Substitution e i i
identitySubst
  where
    go :: FoilPattern i l -> FoilTerm n -> Substitution FoilTerm i n -> Substitution FoilTerm l n
    go :: forall (i :: S) (l :: S) (n :: S).
FoilPattern i l
-> FoilTerm n
-> Substitution FoilTerm i n
-> Substitution FoilTerm l n
go FoilPatternWildcard{} FoilTerm n
_   = Substitution FoilTerm i n -> Substitution FoilTerm i n
Substitution FoilTerm i n -> Substitution FoilTerm l n
forall a. a -> a
id
    go (FoilPatternVar BNFC'Position
_loc NameBinder i l
x) FoilTerm n
e    = \Substitution FoilTerm i n
subst -> Substitution FoilTerm i n
-> NameBinder i l -> FoilTerm n -> Substitution FoilTerm 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 FoilTerm i n
subst NameBinder i l
x FoilTerm n
e
    go (FoilPatternPair BNFC'Position
loc FoilPattern' BNFC'Position i n2
l FoilPattern' BNFC'Position n2 l
r) FoilTerm n
e = FoilPattern' BNFC'Position n2 l
-> FoilTerm n
-> Substitution FoilTerm n2 n
-> Substitution FoilTerm l n
forall (i :: S) (l :: S) (n :: S).
FoilPattern i l
-> FoilTerm n
-> Substitution FoilTerm i n
-> Substitution FoilTerm l n
go FoilPattern' BNFC'Position n2 l
r (BNFC'Position -> FoilTerm n -> FoilTerm n
forall a (n :: S). a -> FoilTerm' a n -> FoilTerm' a n
FoilSecond BNFC'Position
loc FoilTerm n
e) (Substitution FoilTerm n2 n -> Substitution FoilTerm l n)
-> (Substitution FoilTerm i n -> Substitution FoilTerm n2 n)
-> Substitution FoilTerm i n
-> Substitution FoilTerm l n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FoilPattern' BNFC'Position i n2
-> FoilTerm n
-> Substitution FoilTerm i n
-> Substitution FoilTerm n2 n
forall (i :: S) (l :: S) (n :: S).
FoilPattern i l
-> FoilTerm n
-> Substitution FoilTerm i n
-> Substitution FoilTerm l n
go FoilPattern' BNFC'Position i n2
l (BNFC'Position -> FoilTerm n -> FoilTerm n
forall a (n :: S). a -> FoilTerm' a n -> FoilTerm' a n
FoilFirst BNFC'Position
loc FoilTerm n
e)

-- | Compute weak head normal form (WHNF).
whnf :: Distinct n => Scope n -> FoilTerm n -> FoilTerm n
whnf :: forall (n :: S). Distinct n => Scope n -> FoilTerm n -> FoilTerm n
whnf Scope n
scope = \case
  FoilApp BNFC'Position
loc FoilTerm n
f FoilTerm n
arg ->
    case Scope n -> FoilTerm n -> FoilTerm n
forall (n :: S). Distinct n => Scope n -> FoilTerm n -> FoilTerm n
whnf Scope n
scope FoilTerm n
f of
      FoilLam BNFC'Position
_loc FoilPattern' BNFC'Position n l
pat (FoilAScopedTerm BNFC'Position
_loc' FoilTerm' BNFC'Position l
body) ->
        let subst :: Substitution FoilTerm l n
subst = FoilPattern' BNFC'Position n l
-> FoilTerm n -> Substitution FoilTerm l n
forall (n :: S) (l :: S).
FoilPattern n l -> FoilTerm n -> Substitution FoilTerm l n
matchPattern FoilPattern' BNFC'Position n l
pat FoilTerm n
arg
         in Scope n -> FoilTerm n -> FoilTerm n
forall (n :: S). Distinct n => Scope n -> FoilTerm n -> FoilTerm n
whnf Scope n
scope (Scope n
-> Substitution FoilTerm l n
-> FoilTerm' BNFC'Position l
-> FoilTerm n
forall (o :: S) (i :: S).
Distinct o =>
Scope o -> Substitution FoilTerm i o -> FoilTerm i -> FoilTerm o
substitute Scope n
scope Substitution FoilTerm l n
subst FoilTerm' BNFC'Position l
body)
      FoilTerm n
f' -> BNFC'Position -> FoilTerm n -> FoilTerm n -> FoilTerm n
forall a (n :: S).
a -> FoilTerm' a n -> FoilTerm' a n -> FoilTerm' a n
FoilApp BNFC'Position
loc FoilTerm n
f' FoilTerm n
arg
  FoilFirst BNFC'Position
loc FoilTerm n
t ->
    case Scope n -> FoilTerm n -> FoilTerm n
forall (n :: S). Distinct n => Scope n -> FoilTerm n -> FoilTerm n
whnf Scope n
scope FoilTerm n
t of
      FoilPair BNFC'Position
_loc FoilTerm n
l FoilTerm n
_r -> Scope n -> FoilTerm n -> FoilTerm n
forall (n :: S). Distinct n => Scope n -> FoilTerm n -> FoilTerm n
whnf Scope n
scope FoilTerm n
l
      FoilTerm n
t'                 -> BNFC'Position -> FoilTerm n -> FoilTerm n
forall a (n :: S). a -> FoilTerm' a n -> FoilTerm' a n
FoilFirst BNFC'Position
loc FoilTerm n
t'
  FoilSecond BNFC'Position
loc FoilTerm n
t ->
    case Scope n -> FoilTerm n -> FoilTerm n
forall (n :: S). Distinct n => Scope n -> FoilTerm n -> FoilTerm n
whnf Scope n
scope FoilTerm n
t of
      FoilPair BNFC'Position
_loc FoilTerm n
_l FoilTerm n
r -> Scope n -> FoilTerm n -> FoilTerm n
forall (n :: S). Distinct n => Scope n -> FoilTerm n -> FoilTerm n
whnf Scope n
scope FoilTerm n
r
      FoilTerm n
t'                 -> BNFC'Position -> FoilTerm n -> FoilTerm n
forall a (n :: S). a -> FoilTerm' a n -> FoilTerm' a n
FoilSecond BNFC'Position
loc FoilTerm n
t'
  FoilTerm n
t -> FoilTerm n
t

-- ** 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 -> String -> String
forall a. [a] -> [a] -> [a]
++ FoilTerm 'VoidS -> String
printFoilTerm (Scope 'VoidS -> FoilTerm 'VoidS -> FoilTerm 'VoidS
forall (n :: S). Distinct n => Scope n -> FoilTerm n -> FoilTerm n
whnf Scope 'VoidS
emptyScope (Scope 'VoidS
-> Map VarIdent (Name 'VoidS) -> Term -> FoilTerm 'VoidS
forall (n :: S) a.
Distinct n =>
Scope n -> Map VarIdent (Name n) -> Term' a -> FoilTerm' a 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
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

-- ** Pretty-printing

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