module Calculi.Lambda (
LambdaTerm(..)
, UntypedLambdaExpr
, freeVars
, NotKnownErr(..)
, LetDeclr
, unlet
, letsDependency
, letsDependency'
) where
import Data.Bifunctor.TH
import Data.Either.Combinators
import Data.Either (lefts, partitionEithers)
import Data.Generics (Data(..))
import Data.Graph.Inductive
import Data.Graph.Inductive.Helper
import qualified Data.Map as Map
import Data.Maybe
import Data.Random.Generics
import Data.Semigroup
import qualified Data.Set as Set
import Test.QuickCheck
data LambdaTerm c v t =
Variable v
| Constant c
| Apply (LambdaTerm c v t) (LambdaTerm c v t)
| Lambda (v, t) (LambdaTerm c v t)
deriving (Eq, Ord, Show, Data)
deriveBifunctor ''LambdaTerm
deriveBifoldable ''LambdaTerm
deriveBitraversable ''LambdaTerm
instance (Arbitrary c, Data c,
Arbitrary v, Data v,
Arbitrary t, Data t) => Arbitrary (LambdaTerm c v t) where
arbitrary = sized generatorSR
type LetDeclr c v t = ((v, t), LambdaTerm c v t)
type UntypedLambdaExpr c v = LambdaTerm c v ()
data NotKnownErr c v t =
UnknownType t
| UnknownVariable v
| UnknownConstant c
deriving (Eq, Ord, Show)
letsDependency :: (DynGraph gr, Ord c, Ord v, Ord t) => [LetDeclr c v t] -> gr (LetDeclr c v t) ()
letsDependency = snd . letsDependency'
letsDependency' :: forall gr c v t. (DynGraph gr, Ord c, Ord v, Ord t)
=> [LetDeclr c v t]
-> (NodeMap (LetDeclr c v t), gr (LetDeclr c v t) ())
letsDependency' lets =
let
declrs = fst . fst <$> lets
declrsSet = Set.fromList declrs
declrMap :: Map.Map v (LetDeclr c v t)
declrMap = Map.fromList $ zip declrs lets
dependsOf :: LetDeclr c v t -> Set.Set v
dependsOf = Set.intersection declrsSet . freeVars . snd
inwardNodes :: LetDeclr c v t -> [LetDeclr c v t]
inwardNodes declr =
fromMaybe [] (sequence $ (`Map.lookup` declrMap) <$> Set.toList (dependsOf declr))
inwardEdges :: LetDeclr c v t -> [(LetDeclr c v t, LetDeclr c v t, ())]
inwardEdges declr = (\inward -> (inward, declr, ())) <$> inwardNodes declr
in snd . run empty $ insMapEdgesM (concat $ inwardEdges <$> lets)
unlet :: forall c v t. (Ord c, Ord v, Ord t)
=> [LetDeclr c v t]
-> LambdaTerm c v t
-> Either [[LetDeclr c v t]]
(LambdaTerm c v t)
unlet lets expr =
let
depends :: Gr (LetDeclr c v t) () = letsDependency lets
tsorted = topsortWithCycles depends
(cycles, lets') = partitionEithers tsorted
unlet' (declr, body) lexpr = Lambda declr lexpr `Apply` body
in if null cycles then Right (foldr unlet' expr lets') else Left cycles
freeVars :: Ord v => LambdaTerm c v t -> Set.Set v
freeVars = \case
Variable v -> Set.singleton v
Constant _ -> Set.empty
Apply fun arg ->
freeVars fun <> freeVars arg
Lambda (v, _) expr ->
Set.delete v (freeVars expr)