{-# LANGUAGE FlexibleInstances   #-}
{-# LANGUAGE LambdaCase          #-}
{-# LANGUAGE ScopedTypeVariables #-}

module Telomare.Resolver where

import Codec.Binary.UTF8.String (encode)
import Control.Comonad.Cofree (Cofree (..))
import Control.Comonad.Trans.Cofree (CofreeF)
import qualified Control.Comonad.Trans.Cofree as C
import Control.Lens.Combinators (transform)
import Control.Monad ((<=<))
import qualified Control.Monad.State as State
import Crypto.Hash (Digest, SHA256, hash)
import Data.Bifunctor (Bifunctor (first), bimap)
import qualified Data.ByteArray as BA
import Data.ByteString (ByteString)
import qualified Data.ByteString as BS
import Data.Char (ord)
import qualified Data.Foldable as F
import Data.Functor.Foldable (Base, Corecursive (ana, apo), Recursive (cata))
import Data.List (delete, elem, elemIndex, zip4)
import qualified Data.Map as Map
import Data.Map.Strict (Map, fromList, keys)
import Data.Set (Set, (\\))
import qualified Data.Set as Set
import Debug.Trace (trace, traceShow, traceShowId)
import PrettyPrint (TypeDebugInfo (..), prettyPrint, showTypeDebugInfo)
import Telomare
import Telomare.Parser (AnnotatedUPT, TelomareParser, parseWithPrelude)
import Text.Megaparsec (errorBundlePretty, runParser)

debug :: Bool
debug :: Bool
debug = Bool
False

debugTrace :: String -> a -> a
debugTrace :: forall a. String -> a -> a
debugTrace String
s a
x = if Bool
debug then forall a. String -> a -> a
trace String
s a
x else a
x

type VarList = [String]

-- |Int to ParserTerm
i2t :: LocTag -> Int -> Cofree (ParserTermF l v) LocTag
i2t :: forall l v. LocTag -> Int -> Cofree (ParserTermF l v) LocTag
i2t LocTag
anno = forall t a. Corecursive t => (a -> Base t a) -> a -> t
ana forall l v. Int -> CofreeF (ParserTermF l v) LocTag Int
coalg where
  coalg :: Int -> CofreeF (ParserTermF l v) LocTag Int
  coalg :: forall l v. Int -> CofreeF (ParserTermF l v) LocTag Int
coalg Int
0 = LocTag
anno forall (f :: * -> *) a b. a -> f b -> CofreeF f a b
C.:< forall l v r. ParserTermF l v r
TZeroF
  coalg Int
n = LocTag
anno forall (f :: * -> *) a b. a -> f b -> CofreeF f a b
C.:< forall l v r. r -> r -> ParserTermF l v r
TPairF (Int
nforall a. Num a => a -> a -> a
-Int
1) Int
0

-- |List of Int's to ParserTerm
ints2t :: LocTag ->  [Int] -> Cofree (ParserTermF l v) LocTag
ints2t :: forall l v. LocTag -> [Int] -> Cofree (ParserTermF l v) LocTag
ints2t LocTag
anno = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((\Cofree (ParserTermF l v) LocTag
x Cofree (ParserTermF l v) LocTag
y -> LocTag
anno forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall l v r. r -> r -> ParserTermF l v r
TPairF Cofree (ParserTermF l v) LocTag
x Cofree (ParserTermF l v) LocTag
y) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall l v. LocTag -> Int -> Cofree (ParserTermF l v) LocTag
i2t LocTag
anno) (LocTag
anno forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall l v r. ParserTermF l v r
TZeroF)

-- |String to ParserTerm
s2t :: LocTag -> String -> Cofree (ParserTermF l v) LocTag
s2t :: forall l v. LocTag -> String -> Cofree (ParserTermF l v) LocTag
s2t LocTag
anno = forall l v. LocTag -> [Int] -> Cofree (ParserTermF l v) LocTag
ints2t LocTag
anno forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Char -> Int
ord

-- |Int to Church encoding
{-
i2c :: LocTag -> Int -> Term1
i2c anno x = anno :< TLamF (Closed "f") (anno :< TLamF (Open "x") (inner x))
  where inner :: Int -> Term1
        inner = apo coalg
        coalg :: Int -> Base Term1 (Either Term1 Int)
        coalg 0 = anno C.:< TVarF "x"
        coalg n = anno C.:< TAppF (Left . (anno :<) . TVarF $ "f") (Right $ n - 1)
-}

instance MonadFail (Either String) where
  fail :: forall a. String -> Either String a
fail = forall a b. a -> Either a b
Left

-- | Finds all PatternInt leaves returning "directions" to these leaves through pairs
-- in the form of a combination of RightUP and LeftUP from the root
-- e.g. PatternPair (PatternVar "x") (PatternPair (PatternInt 0) (PatternVar "y"))
--      will return [LeftUP . RightUP]
findInts :: LocTag -> Pattern -> [AnnotatedUPT -> AnnotatedUPT]
findInts :: LocTag -> Pattern -> [AnnotatedUPT -> AnnotatedUPT]
findInts LocTag
anno = forall t a. Recursive t => (Base t a -> a) -> t -> a
cata Base Pattern [AnnotatedUPT -> AnnotatedUPT]
-> [AnnotatedUPT -> AnnotatedUPT]
alg where
  alg :: Base Pattern [AnnotatedUPT -> AnnotatedUPT]
      -> [AnnotatedUPT -> AnnotatedUPT]
  alg :: Base Pattern [AnnotatedUPT -> AnnotatedUPT]
-> [AnnotatedUPT -> AnnotatedUPT]
alg = \case
    PatternPairF [AnnotatedUPT -> AnnotatedUPT]
x [AnnotatedUPT -> AnnotatedUPT]
y -> ((forall b c a. (b -> c) -> (a -> b) -> a -> c
. (LocTag
anno forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< ) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall r. r -> UnprocessedParsedTermF r
LeftUPF) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [AnnotatedUPT -> AnnotatedUPT]
x) forall a. Semigroup a => a -> a -> a
<> ((forall b c a. (b -> c) -> (a -> b) -> a -> c
. (LocTag
anno forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< ) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall r. r -> UnprocessedParsedTermF r
RightUPF) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [AnnotatedUPT -> AnnotatedUPT]
y)
    PatternIntF Int
x    -> [forall a. a -> a
id]
    Base Pattern [AnnotatedUPT -> AnnotatedUPT]
_                -> []

-- | Finds all PatternString leaves returning "directions" to these leaves through pairs
-- in the form of a combination of RightUP and LeftUP from the root
-- e.g. PatternPair (PatternVar "x") (PatternPair (PatternString "Hello, world!") (PatternVar "y"))
--      will return [LeftUP . RightUP]
findStrings :: LocTag -> Pattern -> [AnnotatedUPT -> AnnotatedUPT]
findStrings :: LocTag -> Pattern -> [AnnotatedUPT -> AnnotatedUPT]
findStrings LocTag
anno = forall t a. Recursive t => (Base t a -> a) -> t -> a
cata Base Pattern [AnnotatedUPT -> AnnotatedUPT]
-> [AnnotatedUPT -> AnnotatedUPT]
alg where
  alg :: Base Pattern [AnnotatedUPT -> AnnotatedUPT]
      -> [AnnotatedUPT -> AnnotatedUPT]
  alg :: Base Pattern [AnnotatedUPT -> AnnotatedUPT]
-> [AnnotatedUPT -> AnnotatedUPT]
alg = \case
    PatternPairF [AnnotatedUPT -> AnnotatedUPT]
x [AnnotatedUPT -> AnnotatedUPT]
y -> ((forall b c a. (b -> c) -> (a -> b) -> a -> c
. (LocTag
anno forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< ) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall r. r -> UnprocessedParsedTermF r
LeftUPF) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [AnnotatedUPT -> AnnotatedUPT]
x) forall a. Semigroup a => a -> a -> a
<> ((forall b c a. (b -> c) -> (a -> b) -> a -> c
. (LocTag
anno forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< ) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall r. r -> UnprocessedParsedTermF r
RightUPF) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [AnnotatedUPT -> AnnotatedUPT]
y)
    PatternStringF String
x -> [forall a. a -> a
id]
    Base Pattern [AnnotatedUPT -> AnnotatedUPT]
_                -> []

fitPatternVarsToCasedUPT :: Pattern -> AnnotatedUPT -> AnnotatedUPT
fitPatternVarsToCasedUPT :: Pattern -> AnnotatedUPT -> AnnotatedUPT
fitPatternVarsToCasedUPT Pattern
p aupt :: AnnotatedUPT
aupt@(LocTag
anno :< UnprocessedParsedTermF AnnotatedUPT
_) = Map String AnnotatedUPT -> AnnotatedUPT -> AnnotatedUPT
applyVars2UPT Map String AnnotatedUPT
varsOnUPT forall a b. (a -> b) -> a -> b
$ LocTag -> Pattern -> AnnotatedUPT
pattern2UPT LocTag
anno Pattern
p where
  varsOnUPT :: Map String AnnotatedUPT
  varsOnUPT :: Map String AnnotatedUPT
varsOnUPT = (forall a b. (a -> b) -> a -> b
$ AnnotatedUPT
aupt) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> LocTag -> Pattern -> Map String (AnnotatedUPT -> AnnotatedUPT)
findPatternVars LocTag
anno Pattern
p
  applyVars2UPT :: Map String AnnotatedUPT
                -> AnnotatedUPT
                -> AnnotatedUPT
  applyVars2UPT :: Map String AnnotatedUPT -> AnnotatedUPT -> AnnotatedUPT
applyVars2UPT Map String AnnotatedUPT
m = \case
    LocTag
anno :< LamUPF String
str AnnotatedUPT
x ->
      case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup String
str Map String AnnotatedUPT
m of
        Just AnnotatedUPT
a  -> LocTag
anno forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall r. r -> r -> UnprocessedParsedTermF r
AppUPF (LocTag
anno forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall r. String -> r -> UnprocessedParsedTermF r
LamUPF String
str (Map String AnnotatedUPT -> AnnotatedUPT -> AnnotatedUPT
applyVars2UPT Map String AnnotatedUPT
m AnnotatedUPT
x)) AnnotatedUPT
a
        Maybe AnnotatedUPT
Nothing -> LocTag
anno forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall r. String -> r -> UnprocessedParsedTermF r
LamUPF String
str AnnotatedUPT
x
    AnnotatedUPT
x -> AnnotatedUPT
x

-- |Collect all free variable names in a `AnnotatedUPT` expresion
varsUPT :: UnprocessedParsedTerm -> Set String
varsUPT :: UnprocessedParsedTerm -> Set String
varsUPT = forall t a. Recursive t => (Base t a -> a) -> t -> a
cata Base UnprocessedParsedTerm (Set String) -> Set String
alg where
  alg :: Base UnprocessedParsedTerm (Set String) -> Set String
  alg :: Base UnprocessedParsedTerm (Set String) -> Set String
alg (VarUPF String
n)     = forall a. a -> Set a
Set.singleton String
n
  alg (LamUPF String
str Set String
x) = String -> Set String -> Set String
del String
str Set String
x
  alg Base UnprocessedParsedTerm (Set String)
e              = forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
F.fold Base UnprocessedParsedTerm (Set String)
e
  del :: String -> Set String -> Set String
  del :: String -> Set String -> Set String
del String
n Set String
x = if forall a. Ord a => a -> Set a -> Bool
Set.member String
n Set String
x then forall a. Ord a => a -> Set a -> Set a
Set.delete String
n Set String
x else Set String
x

mkLambda4FreeVarUPs :: AnnotatedUPT -> AnnotatedUPT
mkLambda4FreeVarUPs :: AnnotatedUPT -> AnnotatedUPT
mkLambda4FreeVarUPs aupt :: AnnotatedUPT
aupt@(LocTag
anno :< UnprocessedParsedTermF AnnotatedUPT
_) = forall a anno. Recursive a => anno -> a -> Cofree (Base a) anno
tag LocTag
anno forall a b. (a -> b) -> a -> b
$ UnprocessedParsedTerm -> [String] -> UnprocessedParsedTerm
go UnprocessedParsedTerm
upt [String]
freeVars where
  upt :: UnprocessedParsedTerm
upt = forall a anno. Corecursive a => Cofree (Base a) anno -> a
forget AnnotatedUPT
aupt
  freeVars :: [String]
freeVars = forall a. Set a -> [a]
Set.toList forall b c a. (b -> c) -> (a -> b) -> a -> c
. UnprocessedParsedTerm -> Set String
varsUPT forall a b. (a -> b) -> a -> b
$ UnprocessedParsedTerm
upt
  go :: UnprocessedParsedTerm -> [String] -> UnprocessedParsedTerm
  go :: UnprocessedParsedTerm -> [String] -> UnprocessedParsedTerm
go UnprocessedParsedTerm
x = \case
    []     -> UnprocessedParsedTerm
x
    (String
y:[String]
ys) -> String -> UnprocessedParsedTerm -> UnprocessedParsedTerm
LamUP String
y forall a b. (a -> b) -> a -> b
$ UnprocessedParsedTerm -> [String] -> UnprocessedParsedTerm
go UnprocessedParsedTerm
x [String]
ys

findPatternVars :: LocTag -> Pattern -> Map String (AnnotatedUPT -> AnnotatedUPT)
findPatternVars :: LocTag -> Pattern -> Map String (AnnotatedUPT -> AnnotatedUPT)
findPatternVars LocTag
anno = forall t a. Recursive t => (Base t a -> a) -> t -> a
cata Base Pattern (Map String (AnnotatedUPT -> AnnotatedUPT))
-> Map String (AnnotatedUPT -> AnnotatedUPT)
alg where
  alg :: Base Pattern (Map String (AnnotatedUPT -> AnnotatedUPT))
      -> Map String (AnnotatedUPT -> AnnotatedUPT)
  alg :: Base Pattern (Map String (AnnotatedUPT -> AnnotatedUPT))
-> Map String (AnnotatedUPT -> AnnotatedUPT)
alg = \case
    PatternPairF Map String (AnnotatedUPT -> AnnotatedUPT)
x Map String (AnnotatedUPT -> AnnotatedUPT)
y -> ((forall b c a. (b -> c) -> (a -> b) -> a -> c
. (LocTag
anno forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< )forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall r. r -> UnprocessedParsedTermF r
LeftUPF) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map String (AnnotatedUPT -> AnnotatedUPT)
x) forall a. Semigroup a => a -> a -> a
<> ((forall b c a. (b -> c) -> (a -> b) -> a -> c
. (LocTag
anno forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< )forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall r. r -> UnprocessedParsedTermF r
RightUPF) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map String (AnnotatedUPT -> AnnotatedUPT)
y)
    PatternVarF String
str  -> forall k a. k -> a -> Map k a
Map.singleton String
str forall a. a -> a
id
    Base Pattern (Map String (AnnotatedUPT -> AnnotatedUPT))
_                -> forall k a. Map k a
Map.empty

-- TODO: Annotate without so much fuzz
pairStructureCheck :: Pattern -> UnprocessedParsedTerm -> UnprocessedParsedTerm
pairStructureCheck :: Pattern -> UnprocessedParsedTerm -> UnprocessedParsedTerm
pairStructureCheck Pattern
p UnprocessedParsedTerm
upt =
  UnprocessedParsedTerm
-> UnprocessedParsedTerm -> UnprocessedParsedTerm
AppUP (UnprocessedParsedTerm
-> UnprocessedParsedTerm -> UnprocessedParsedTerm
AppUP (UnprocessedParsedTerm
-> UnprocessedParsedTerm -> UnprocessedParsedTerm
AppUP (String -> UnprocessedParsedTerm
VarUP String
"foldl")
                      (String -> UnprocessedParsedTerm
VarUP String
"and"))
               (Int -> UnprocessedParsedTerm
IntUP Int
1))
        ([UnprocessedParsedTerm] -> UnprocessedParsedTerm
ListUP forall a b. (a -> b) -> a -> b
$ (forall a b. (a -> b) -> a -> b
$ UnprocessedParsedTerm
upt) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Pattern -> [UnprocessedParsedTerm -> UnprocessedParsedTerm]
pairRoute2Dirs Pattern
p)

pairRoute2Dirs :: Pattern -> [UnprocessedParsedTerm -> UnprocessedParsedTerm]
pairRoute2Dirs :: Pattern -> [UnprocessedParsedTerm -> UnprocessedParsedTerm]
pairRoute2Dirs = forall t a. Recursive t => (Base t a -> a) -> t -> a
cata Base Pattern [UnprocessedParsedTerm -> UnprocessedParsedTerm]
-> [UnprocessedParsedTerm -> UnprocessedParsedTerm]
alg where
  alg :: Base Pattern [UnprocessedParsedTerm -> UnprocessedParsedTerm]
      -> [UnprocessedParsedTerm -> UnprocessedParsedTerm]
  alg :: Base Pattern [UnprocessedParsedTerm -> UnprocessedParsedTerm]
-> [UnprocessedParsedTerm -> UnprocessedParsedTerm]
alg = \case
    PatternPairF [UnprocessedParsedTerm -> UnprocessedParsedTerm]
x [UnprocessedParsedTerm -> UnprocessedParsedTerm]
y -> [forall a. a -> a
id] forall a. Semigroup a => a -> a -> a
<> ((forall b c a. (b -> c) -> (a -> b) -> a -> c
. UnprocessedParsedTerm -> UnprocessedParsedTerm
LeftUP) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [UnprocessedParsedTerm -> UnprocessedParsedTerm]
x) forall a. Semigroup a => a -> a -> a
<> ((forall b c a. (b -> c) -> (a -> b) -> a -> c
. UnprocessedParsedTerm -> UnprocessedParsedTerm
RightUP) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [UnprocessedParsedTerm -> UnprocessedParsedTerm]
y)
    Base Pattern [UnprocessedParsedTerm -> UnprocessedParsedTerm]
_                -> []

pattern2UPT :: LocTag -> Pattern -> AnnotatedUPT
pattern2UPT :: LocTag -> Pattern -> AnnotatedUPT
pattern2UPT LocTag
anno = forall a anno. Recursive a => anno -> a -> Cofree (Base a) anno
tag LocTag
anno forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t a. Recursive t => (Base t a -> a) -> t -> a
cata Base Pattern UnprocessedParsedTerm -> UnprocessedParsedTerm
alg where
  alg :: Base Pattern UnprocessedParsedTerm -> UnprocessedParsedTerm
  alg :: Base Pattern UnprocessedParsedTerm -> UnprocessedParsedTerm
alg = \case
    PatternPairF UnprocessedParsedTerm
x UnprocessedParsedTerm
y   -> UnprocessedParsedTerm
-> UnprocessedParsedTerm -> UnprocessedParsedTerm
PairUP UnprocessedParsedTerm
x UnprocessedParsedTerm
y
    PatternIntF Int
i      -> Int -> UnprocessedParsedTerm
IntUP Int
i
    PatternStringF String
str -> String -> UnprocessedParsedTerm
StringUP String
str
    PatternVarF String
str    -> Int -> UnprocessedParsedTerm
IntUP Int
0
    Base Pattern UnprocessedParsedTerm
PatternF UnprocessedParsedTerm
PatternIgnoreF     -> Int -> UnprocessedParsedTerm
IntUP Int
0
      -- Note that "__ignore" is a special variable name and not accessible to users because
      -- parsing of VarUPs doesn't allow variable names to start with `_`

mkCaseAlternative :: AnnotatedUPT -- ^ UPT to be cased
                  -> AnnotatedUPT -- ^ Case result to be made lambda and applied
                  -> Pattern -- ^ Pattern
                  -> AnnotatedUPT -- ^ case result as a lambda applied to the appropirate part of the UPT to be cased
mkCaseAlternative :: AnnotatedUPT -> AnnotatedUPT -> Pattern -> AnnotatedUPT
mkCaseAlternative casedUPT :: AnnotatedUPT
casedUPT@(LocTag
anno :< UnprocessedParsedTermF AnnotatedUPT
_) AnnotatedUPT
caseResult Pattern
p = Map String AnnotatedUPT -> AnnotatedUPT -> AnnotatedUPT
appVars2ResultLambdaAlts Map String AnnotatedUPT
patternVarsOnUPT forall b c a. (b -> c) -> (a -> b) -> a -> c
. AnnotatedUPT -> [String] -> AnnotatedUPT
makeLambdas AnnotatedUPT
caseResult forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a. Map k a -> [k]
keys forall a b. (a -> b) -> a -> b
$ Map String AnnotatedUPT
patternVarsOnUPT where
  patternVarsOnUPT :: Map String AnnotatedUPT
  patternVarsOnUPT :: Map String AnnotatedUPT
patternVarsOnUPT = (forall a b. (a -> b) -> a -> b
$ AnnotatedUPT
casedUPT) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> LocTag -> Pattern -> Map String (AnnotatedUPT -> AnnotatedUPT)
findPatternVars LocTag
anno Pattern
p
  appVars2ResultLambdaAlts :: Map String AnnotatedUPT
                           -> AnnotatedUPT -- ^ case result as lambda
                           -> AnnotatedUPT
  appVars2ResultLambdaAlts :: Map String AnnotatedUPT -> AnnotatedUPT -> AnnotatedUPT
appVars2ResultLambdaAlts Map String AnnotatedUPT
m = \case
    lam :: AnnotatedUPT
lam@(LocTag
_ :< LamUPF String
varName AnnotatedUPT
upt) ->
      case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup String
varName Map String AnnotatedUPT
m of
        Maybe AnnotatedUPT
Nothing -> AnnotatedUPT
lam
        Just AnnotatedUPT
x -> LocTag
anno forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall r. r -> r -> UnprocessedParsedTermF r
AppUPF (LocTag
anno forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall r. String -> r -> UnprocessedParsedTermF r
LamUPF String
varName (Map String AnnotatedUPT -> AnnotatedUPT -> AnnotatedUPT
appVars2ResultLambdaAlts (forall k a. Ord k => k -> Map k a -> Map k a
Map.delete String
varName Map String AnnotatedUPT
m) AnnotatedUPT
upt)) AnnotatedUPT
x
    AnnotatedUPT
x -> AnnotatedUPT
x
  makeLambdas :: AnnotatedUPT
              -> [String]
              -> AnnotatedUPT
  makeLambdas :: AnnotatedUPT -> [String] -> AnnotatedUPT
makeLambdas aupt :: AnnotatedUPT
aupt@(LocTag
anno' :< UnprocessedParsedTermF AnnotatedUPT
_) = \case
    []     -> AnnotatedUPT
aupt
    (String
x:[String]
xs) -> LocTag
anno' forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall r. String -> r -> UnprocessedParsedTermF r
LamUPF String
x (AnnotatedUPT -> [String] -> AnnotatedUPT
makeLambdas AnnotatedUPT
aupt [String]
xs)

case2annidatedIfs :: AnnotatedUPT -- ^ Term to be pattern matched
                  -> [Pattern] -- ^ All patterns in a case expression
                  -> [AnnotatedUPT] -- ^ Int leaves as ListUPs on UPT
                  -> [AnnotatedUPT] -- ^ Int leaves as ListUPs on pattern
                  -> [AnnotatedUPT] -- ^ String leaves as ListUPs on UPT
                  -> [AnnotatedUPT] -- ^ String leaves as ListUPs on pattern
                  -> [AnnotatedUPT] -- ^ Case's alternatives
                  -> AnnotatedUPT
case2annidatedIfs :: AnnotatedUPT
-> [Pattern]
-> [AnnotatedUPT]
-> [AnnotatedUPT]
-> [AnnotatedUPT]
-> [AnnotatedUPT]
-> [AnnotatedUPT]
-> AnnotatedUPT
case2annidatedIfs (LocTag
anno :< UnprocessedParsedTermF AnnotatedUPT
_) [] [] [] [] [] [] = forall a anno. Recursive a => anno -> a -> Cofree (Base a) anno
tag LocTag
anno forall a b. (a -> b) -> a -> b
$
  UnprocessedParsedTerm
-> UnprocessedParsedTerm
-> UnprocessedParsedTerm
-> UnprocessedParsedTerm
ITEUP (Int -> UnprocessedParsedTerm
IntUP Int
1)
        (UnprocessedParsedTerm
-> UnprocessedParsedTerm -> UnprocessedParsedTerm
AppUP (String -> UnprocessedParsedTerm
VarUP String
"abort") forall a b. (a -> b) -> a -> b
$ String -> UnprocessedParsedTerm
StringUP String
"Non-exhaustive patterns in case")
        (Int -> UnprocessedParsedTerm
IntUP Int
0)
case2annidatedIfs AnnotatedUPT
x (Pattern
aPattern:[Pattern]
as) ((LocTag
_ :< ListUPF []) : [AnnotatedUPT]
bs) ((LocTag
_ :< ListUPF []) :[AnnotatedUPT]
cs) (AnnotatedUPT
dirs2StringOnUPT:[AnnotatedUPT]
ds) (AnnotatedUPT
dirs2StringOnPattern:[AnnotatedUPT]
es) (resultAlternative :: AnnotatedUPT
resultAlternative@(LocTag
anno :< UnprocessedParsedTermF AnnotatedUPT
_):[AnnotatedUPT]
fs) =
  forall a anno. Recursive a => anno -> a -> Cofree (Base a) anno
tag LocTag
anno forall a b. (a -> b) -> a -> b
$
    UnprocessedParsedTerm
-> UnprocessedParsedTerm
-> UnprocessedParsedTerm
-> UnprocessedParsedTerm
ITEUP (UnprocessedParsedTerm
-> UnprocessedParsedTerm -> UnprocessedParsedTerm
AppUP (UnprocessedParsedTerm
-> UnprocessedParsedTerm -> UnprocessedParsedTerm
AppUP (String -> UnprocessedParsedTerm
VarUP String
"and")
                        (UnprocessedParsedTerm
-> UnprocessedParsedTerm -> UnprocessedParsedTerm
AppUP (UnprocessedParsedTerm
-> UnprocessedParsedTerm -> UnprocessedParsedTerm
AppUP (String -> UnprocessedParsedTerm
VarUP String
"listEqual") (forall a anno. Corecursive a => Cofree (Base a) anno -> a
forget AnnotatedUPT
dirs2StringOnUPT)) (forall a anno. Corecursive a => Cofree (Base a) anno -> a
forget AnnotatedUPT
dirs2StringOnPattern)))
                 (Pattern -> UnprocessedParsedTerm -> UnprocessedParsedTerm
pairStructureCheck Pattern
aPattern (forall a anno. Corecursive a => Cofree (Base a) anno -> a
forget AnnotatedUPT
x)))
          (forall a anno. Corecursive a => Cofree (Base a) anno -> a
forget forall a b. (a -> b) -> a -> b
$ AnnotatedUPT -> AnnotatedUPT -> Pattern -> AnnotatedUPT
mkCaseAlternative AnnotatedUPT
x AnnotatedUPT
resultAlternative Pattern
aPattern)
          (forall a anno. Corecursive a => Cofree (Base a) anno -> a
forget forall a b. (a -> b) -> a -> b
$ AnnotatedUPT
-> [Pattern]
-> [AnnotatedUPT]
-> [AnnotatedUPT]
-> [AnnotatedUPT]
-> [AnnotatedUPT]
-> [AnnotatedUPT]
-> AnnotatedUPT
case2annidatedIfs AnnotatedUPT
x [Pattern]
as [AnnotatedUPT]
bs [AnnotatedUPT]
cs [AnnotatedUPT]
ds [AnnotatedUPT]
es [AnnotatedUPT]
fs)
case2annidatedIfs AnnotatedUPT
x (Pattern
aPattern:[Pattern]
as) (AnnotatedUPT
dirs2IntOnUPT:[AnnotatedUPT]
bs) (AnnotatedUPT
dirs2IntOnPattern:[AnnotatedUPT]
cs) ((LocTag
_ :< ListUPF []) : [AnnotatedUPT]
ds) ((LocTag
_ :< ListUPF []) : [AnnotatedUPT]
es) (resultAlternative :: AnnotatedUPT
resultAlternative@(LocTag
anno :< UnprocessedParsedTermF AnnotatedUPT
_):[AnnotatedUPT]
fs) =
  forall a anno. Recursive a => anno -> a -> Cofree (Base a) anno
tag LocTag
anno forall a b. (a -> b) -> a -> b
$
    UnprocessedParsedTerm
-> UnprocessedParsedTerm
-> UnprocessedParsedTerm
-> UnprocessedParsedTerm
ITEUP (UnprocessedParsedTerm
-> UnprocessedParsedTerm -> UnprocessedParsedTerm
AppUP (UnprocessedParsedTerm
-> UnprocessedParsedTerm -> UnprocessedParsedTerm
AppUP (String -> UnprocessedParsedTerm
VarUP String
"and")
                        (UnprocessedParsedTerm
-> UnprocessedParsedTerm -> UnprocessedParsedTerm
AppUP (UnprocessedParsedTerm
-> UnprocessedParsedTerm -> UnprocessedParsedTerm
AppUP (String -> UnprocessedParsedTerm
VarUP String
"listEqual") (forall a anno. Corecursive a => Cofree (Base a) anno -> a
forget AnnotatedUPT
dirs2IntOnUPT)) (forall a anno. Corecursive a => Cofree (Base a) anno -> a
forget AnnotatedUPT
dirs2IntOnPattern)))
                 (Pattern -> UnprocessedParsedTerm -> UnprocessedParsedTerm
pairStructureCheck Pattern
aPattern (forall a anno. Corecursive a => Cofree (Base a) anno -> a
forget AnnotatedUPT
x)))
          (forall a anno. Corecursive a => Cofree (Base a) anno -> a
forget forall a b. (a -> b) -> a -> b
$ AnnotatedUPT -> AnnotatedUPT -> Pattern -> AnnotatedUPT
mkCaseAlternative AnnotatedUPT
x AnnotatedUPT
resultAlternative Pattern
aPattern)
          (forall a anno. Corecursive a => Cofree (Base a) anno -> a
forget forall a b. (a -> b) -> a -> b
$ AnnotatedUPT
-> [Pattern]
-> [AnnotatedUPT]
-> [AnnotatedUPT]
-> [AnnotatedUPT]
-> [AnnotatedUPT]
-> [AnnotatedUPT]
-> AnnotatedUPT
case2annidatedIfs AnnotatedUPT
x [Pattern]
as [AnnotatedUPT]
bs [AnnotatedUPT]
cs [AnnotatedUPT]
ds [AnnotatedUPT]
es [AnnotatedUPT]
fs)
case2annidatedIfs AnnotatedUPT
x (Pattern
aPattern:[Pattern]
as) (AnnotatedUPT
dirs2IntOnUPT:[AnnotatedUPT]
bs) (AnnotatedUPT
dirs2IntOnPattern:[AnnotatedUPT]
cs) (AnnotatedUPT
dirs2StringOnUPT:[AnnotatedUPT]
ds) (AnnotatedUPT
dirs2StringOnPattern:[AnnotatedUPT]
es) (resultAlternative :: AnnotatedUPT
resultAlternative@(LocTag
anno :< UnprocessedParsedTermF AnnotatedUPT
_):[AnnotatedUPT]
fs) =
  forall a anno. Recursive a => anno -> a -> Cofree (Base a) anno
tag LocTag
anno forall a b. (a -> b) -> a -> b
$
    UnprocessedParsedTerm
-> UnprocessedParsedTerm
-> UnprocessedParsedTerm
-> UnprocessedParsedTerm
ITEUP (UnprocessedParsedTerm
-> UnprocessedParsedTerm -> UnprocessedParsedTerm
AppUP (UnprocessedParsedTerm
-> UnprocessedParsedTerm -> UnprocessedParsedTerm
AppUP (UnprocessedParsedTerm
-> UnprocessedParsedTerm -> UnprocessedParsedTerm
AppUP (String -> UnprocessedParsedTerm
VarUP String
"foldl")
                                (String -> UnprocessedParsedTerm
VarUP String
"and"))
                        (Int -> UnprocessedParsedTerm
IntUP Int
1))
                 ([UnprocessedParsedTerm] -> UnprocessedParsedTerm
ListUP [ UnprocessedParsedTerm
-> UnprocessedParsedTerm -> UnprocessedParsedTerm
AppUP (UnprocessedParsedTerm
-> UnprocessedParsedTerm -> UnprocessedParsedTerm
AppUP (String -> UnprocessedParsedTerm
VarUP String
"listEqual") (forall a anno. Corecursive a => Cofree (Base a) anno -> a
forget AnnotatedUPT
dirs2IntOnUPT)) (forall a anno. Corecursive a => Cofree (Base a) anno -> a
forget AnnotatedUPT
dirs2IntOnPattern)
                         , UnprocessedParsedTerm
-> UnprocessedParsedTerm -> UnprocessedParsedTerm
AppUP (UnprocessedParsedTerm
-> UnprocessedParsedTerm -> UnprocessedParsedTerm
AppUP (String -> UnprocessedParsedTerm
VarUP String
"listEqual") (forall a anno. Corecursive a => Cofree (Base a) anno -> a
forget AnnotatedUPT
dirs2StringOnUPT)) (forall a anno. Corecursive a => Cofree (Base a) anno -> a
forget AnnotatedUPT
dirs2StringOnPattern)
                         , Pattern -> UnprocessedParsedTerm -> UnprocessedParsedTerm
pairStructureCheck Pattern
aPattern (forall a anno. Corecursive a => Cofree (Base a) anno -> a
forget AnnotatedUPT
x)
                         ]))
          (forall a anno. Corecursive a => Cofree (Base a) anno -> a
forget forall a b. (a -> b) -> a -> b
$ AnnotatedUPT -> AnnotatedUPT -> Pattern -> AnnotatedUPT
mkCaseAlternative AnnotatedUPT
x AnnotatedUPT
resultAlternative Pattern
aPattern)
          (forall a anno. Corecursive a => Cofree (Base a) anno -> a
forget forall a b. (a -> b) -> a -> b
$ AnnotatedUPT
-> [Pattern]
-> [AnnotatedUPT]
-> [AnnotatedUPT]
-> [AnnotatedUPT]
-> [AnnotatedUPT]
-> [AnnotatedUPT]
-> AnnotatedUPT
case2annidatedIfs AnnotatedUPT
x [Pattern]
as [AnnotatedUPT]
bs [AnnotatedUPT]
cs [AnnotatedUPT]
ds [AnnotatedUPT]
es [AnnotatedUPT]
fs)
case2annidatedIfs AnnotatedUPT
_ [Pattern]
_ [AnnotatedUPT]
_ [AnnotatedUPT]
_ [AnnotatedUPT]
_ [AnnotatedUPT]
_ [AnnotatedUPT]
_ = forall a. HasCallStack => String -> a
error String
"case2annidatedIfs: lists don't match in size"

removeCaseUPs :: AnnotatedUPT -> AnnotatedUPT
removeCaseUPs :: AnnotatedUPT -> AnnotatedUPT
removeCaseUPs = forall a. Plated a => (a -> a) -> a -> a
transform AnnotatedUPT -> AnnotatedUPT
go where
  go :: AnnotatedUPT -> AnnotatedUPT
  go :: AnnotatedUPT -> AnnotatedUPT
go = \case
    LocTag
anno :< CaseUPF AnnotatedUPT
x [(Pattern, AnnotatedUPT)]
ls ->
      let duplicate :: b -> (b, b)
duplicate b
x = (b
x,b
x)
          pairApplyList :: ([a -> a], a) -> [a]
          pairApplyList :: forall a. ([a -> a], a) -> [a]
pairApplyList ([a -> a], a)
x = (forall a b. (a -> b) -> a -> b
$ forall a b. (a, b) -> b
snd ([a -> a], a)
x) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a b. (a, b) -> a
fst ([a -> a], a)
x
          patterns :: [Pattern]
patterns = forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Pattern, AnnotatedUPT)]
ls
          resultCaseAlts :: [AnnotatedUPT]
resultCaseAlts = forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Pattern, AnnotatedUPT)]
ls
          dirs2LeavesOnUPT :: (Pattern -> [AnnotatedUPT -> AnnotatedUPT])
                           -> [AnnotatedUPT]
          dirs2LeavesOnUPT :: (Pattern -> [AnnotatedUPT -> AnnotatedUPT]) -> [AnnotatedUPT]
dirs2LeavesOnUPT Pattern -> [AnnotatedUPT -> AnnotatedUPT]
f = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\[AnnotatedUPT]
y -> LocTag
anno forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall r. [r] -> UnprocessedParsedTermF r
ListUPF [AnnotatedUPT]
y) forall a b. (a -> b) -> a -> b
$ ((forall a b. (a -> b) -> a -> b
$ AnnotatedUPT
x) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Pattern -> [AnnotatedUPT -> AnnotatedUPT]
f forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Pattern]
patterns
          dirs2LeavesOnPattern :: (Pattern -> [AnnotatedUPT -> AnnotatedUPT])
                               -> [AnnotatedUPT]
          dirs2LeavesOnPattern :: (Pattern -> [AnnotatedUPT -> AnnotatedUPT]) -> [AnnotatedUPT]
dirs2LeavesOnPattern Pattern -> [AnnotatedUPT -> AnnotatedUPT]
f = (\[AnnotatedUPT]
a -> LocTag
anno forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall r. [r] -> UnprocessedParsedTermF r
ListUPF [AnnotatedUPT]
a) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall a. ([a -> a], a) -> [a]
pairApplyList forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap Pattern -> [AnnotatedUPT -> AnnotatedUPT]
f (LocTag -> Pattern -> AnnotatedUPT
pattern2UPT LocTag
anno) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {b}. b -> (b, b)
duplicate forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Pattern]
patterns))
      in AnnotatedUPT
-> [Pattern]
-> [AnnotatedUPT]
-> [AnnotatedUPT]
-> [AnnotatedUPT]
-> [AnnotatedUPT]
-> [AnnotatedUPT]
-> AnnotatedUPT
case2annidatedIfs AnnotatedUPT
x
                           [Pattern]
patterns
                           ((Pattern -> [AnnotatedUPT -> AnnotatedUPT]) -> [AnnotatedUPT]
dirs2LeavesOnUPT (LocTag -> Pattern -> [AnnotatedUPT -> AnnotatedUPT]
findInts LocTag
anno))
                           ((Pattern -> [AnnotatedUPT -> AnnotatedUPT]) -> [AnnotatedUPT]
dirs2LeavesOnPattern forall a b. (a -> b) -> a -> b
$ LocTag -> Pattern -> [AnnotatedUPT -> AnnotatedUPT]
findInts LocTag
anno)
                           ((Pattern -> [AnnotatedUPT -> AnnotatedUPT]) -> [AnnotatedUPT]
dirs2LeavesOnUPT forall a b. (a -> b) -> a -> b
$ LocTag -> Pattern -> [AnnotatedUPT -> AnnotatedUPT]
findStrings LocTag
anno)
                           ((Pattern -> [AnnotatedUPT -> AnnotatedUPT]) -> [AnnotatedUPT]
dirs2LeavesOnPattern forall a b. (a -> b) -> a -> b
$ LocTag -> Pattern -> [AnnotatedUPT -> AnnotatedUPT]
findStrings LocTag
anno)
                           [AnnotatedUPT]
resultCaseAlts
    AnnotatedUPT
x -> AnnotatedUPT
x

debruijinize :: MonadFail m => VarList -> Term1 -> m Term2
debruijinize :: forall (m :: * -> *). MonadFail m => [String] -> Term1 -> m Term2
debruijinize [String]
vl = \case
  all :: Term1
all@(LocTag
anno :< ParserTermF String String Term1
TZeroF) -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ LocTag
anno forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall l v r. ParserTermF l v r
TZeroF
  (LocTag
anno :< TPairF Term1
a Term1
b) -> (\Term2
x Term2
y -> LocTag
anno forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall l v r. r -> r -> ParserTermF l v r
TPairF Term2
x Term2
y) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). MonadFail m => [String] -> Term1 -> m Term2
debruijinize [String]
vl Term1
a forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (m :: * -> *). MonadFail m => [String] -> Term1 -> m Term2
debruijinize [String]
vl Term1
b
  (LocTag
anno :< TVarF String
n) -> case forall a. Eq a => a -> [a] -> Maybe Int
elemIndex String
n [String]
vl of
               Just Int
i  -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ LocTag
anno forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall l v r. v -> ParserTermF l v r
TVarF Int
i
               Maybe Int
Nothing -> forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String
"undefined identifier " forall a. Semigroup a => a -> a -> a
<> String
n)
  (LocTag
anno :< TAppF Term1
i Term1
c) -> (\Term2
x Term2
y -> LocTag
anno forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall l v r. r -> r -> ParserTermF l v r
TAppF Term2
x Term2
y) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). MonadFail m => [String] -> Term1 -> m Term2
debruijinize [String]
vl Term1
i forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (m :: * -> *). MonadFail m => [String] -> Term1 -> m Term2
debruijinize [String]
vl Term1
c
  (LocTag
anno :< TCheckF Term1
c Term1
tc) -> (\Term2
x Term2
y -> LocTag
anno forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall l v r. r -> r -> ParserTermF l v r
TCheckF Term2
x Term2
y) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). MonadFail m => [String] -> Term1 -> m Term2
debruijinize [String]
vl Term1
c forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (m :: * -> *). MonadFail m => [String] -> Term1 -> m Term2
debruijinize [String]
vl Term1
tc
  (LocTag
anno :< TITEF Term1
i Term1
t Term1
e) -> (\Term2
x Term2
y Term2
z -> LocTag
anno forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall l v r. r -> r -> r -> ParserTermF l v r
TITEF Term2
x Term2
y Term2
z) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). MonadFail m => [String] -> Term1 -> m Term2
debruijinize [String]
vl Term1
i
                                                           forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (m :: * -> *). MonadFail m => [String] -> Term1 -> m Term2
debruijinize [String]
vl Term1
t
                                                           forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (m :: * -> *). MonadFail m => [String] -> Term1 -> m Term2
debruijinize [String]
vl Term1
e
  (LocTag
anno :< TLeftF Term1
x) -> (\Term2
y -> LocTag
anno forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall l v r. r -> ParserTermF l v r
TLeftF Term2
y) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). MonadFail m => [String] -> Term1 -> m Term2
debruijinize [String]
vl Term1
x
  (LocTag
anno :< TRightF Term1
x) -> (\Term2
y -> LocTag
anno forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall l v r. r -> ParserTermF l v r
TRightF Term2
y) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). MonadFail m => [String] -> Term1 -> m Term2
debruijinize [String]
vl Term1
x
  (LocTag
anno :< TTraceF Term1
x) -> (\Term2
y -> LocTag
anno forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall l v r. r -> ParserTermF l v r
TTraceF Term2
y) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). MonadFail m => [String] -> Term1 -> m Term2
debruijinize [String]
vl Term1
x
  (LocTag
anno :< THashF Term1
x) -> (\Term2
y -> LocTag
anno forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall l v r. r -> ParserTermF l v r
THashF Term2
y) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). MonadFail m => [String] -> Term1 -> m Term2
debruijinize [String]
vl Term1
x
  (LocTag
anno :< TLamF (Open String
n) Term1
x) -> (\Term2
y -> LocTag
anno forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall l v r. LamType l -> r -> ParserTermF l v r
TLamF (forall l. l -> LamType l
Open ()) Term2
y) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). MonadFail m => [String] -> Term1 -> m Term2
debruijinize (String
n forall a. a -> [a] -> [a]
: [String]
vl) Term1
x
  (LocTag
anno :< TLamF (Closed String
n) Term1
x) -> (\Term2
y -> LocTag
anno forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall l v r. LamType l -> r -> ParserTermF l v r
TLamF (forall l. l -> LamType l
Closed ()) Term2
y) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). MonadFail m => [String] -> Term1 -> m Term2
debruijinize (String
n forall a. a -> [a] -> [a]
: [String]
vl) Term1
x
  (LocTag
anno :< TChurchF Int
n) -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ LocTag
anno forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall l v r. Int -> ParserTermF l v r
TChurchF Int
n
  (LocTag
anno :< TLimitedRecursionF Term1
t Term1
r Term1
b) -> (\Term2
x Term2
y Term2
z -> LocTag
anno forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall l v r. r -> r -> r -> ParserTermF l v r
TLimitedRecursionF Term2
x Term2
y Term2
z) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). MonadFail m => [String] -> Term1 -> m Term2
debruijinize [String]
vl Term1
t forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (m :: * -> *). MonadFail m => [String] -> Term1 -> m Term2
debruijinize [String]
vl Term1
r forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (m :: * -> *). MonadFail m => [String] -> Term1 -> m Term2
debruijinize [String]
vl Term1
b

rewriteOuterTag :: anno -> Cofree a anno -> Cofree a anno
rewriteOuterTag :: forall anno (a :: * -> *). anno -> Cofree a anno -> Cofree a anno
rewriteOuterTag anno
anno (anno
_ :< a (Cofree a anno)
x) = anno
anno forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< a (Cofree a anno)
x

splitExpr' :: Term2 -> BreakState' RecursionPieceFrag UnsizedRecursionToken
splitExpr' :: Term2 -> BreakState' RecursionPieceFrag UnsizedRecursionToken
splitExpr' = \case
  (LocTag
anno :< ParserTermF () Int Term2
TZeroF) -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (LocTag
anno forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall a r. FragExprF a r
ZeroFragF)
  (LocTag
anno :< TPairF Term2
a Term2
b) -> forall anno (a :: * -> *). anno -> Cofree a anno -> Cofree a anno
rewriteOuterTag LocTag
anno forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a b. BreakState' a b -> BreakState' a b -> BreakState' a b
pairF (Term2 -> BreakState' RecursionPieceFrag UnsizedRecursionToken
splitExpr' Term2
a) (Term2 -> BreakState' RecursionPieceFrag UnsizedRecursionToken
splitExpr' Term2
b)
  (LocTag
anno :< TVarF Int
n) -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a anno. Recursive a => anno -> a -> Cofree (Base a) anno
tag LocTag
anno forall a b. (a -> b) -> a -> b
$ forall a. Int -> FragExpr a
varNF Int
n
  (LocTag
anno :< TAppF Term2
c Term2
i) ->
    forall anno (a :: * -> *). anno -> Cofree a anno -> Cofree a anno
rewriteOuterTag LocTag
anno forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a b.
(Show a, Enum b, Show b) =>
BreakState' a b -> BreakState' a b -> BreakState' a b
appF (Term2 -> BreakState' RecursionPieceFrag UnsizedRecursionToken
splitExpr' Term2
c) (Term2 -> BreakState' RecursionPieceFrag UnsizedRecursionToken
splitExpr' Term2
i)
  (LocTag
anno :< TCheckF Term2
tc Term2
c) ->
    let performTC :: BreakState' RecursionPieceFrag UnsizedRecursionToken
performTC = forall a b. Show a => BreakState' a b -> BreakState' a b
deferF ((\BreakState' RecursionPieceFrag UnsizedRecursionToken
ia -> forall a b. BreakState' a b -> BreakState' a b
setEnvF (forall a b. BreakState' a b -> BreakState' a b -> BreakState' a b
pairF (forall a b. BreakState' a b -> BreakState' a b
setEnvF (forall a b. BreakState' a b -> BreakState' a b -> BreakState' a b
pairF (forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a anno. Recursive a => anno -> a -> Cofree (Base a) anno
tag LocTag
anno forall a. FragExpr a
AbortFrag) BreakState' RecursionPieceFrag UnsizedRecursionToken
ia))
                                                   (forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a anno. Recursive a => anno -> a -> Cofree (Base a) anno
tag LocTag
anno forall a b. (a -> b) -> a -> b
$ forall a. FragExpr a -> FragExpr a
RightFrag forall a. FragExpr a
EnvFrag))) forall a b. (a -> b) -> a -> b
$ forall a b.
(Show a, Enum b, Show b) =>
BreakState' a b -> BreakState' a b -> BreakState' a b
appF (forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a anno. Recursive a => anno -> a -> Cofree (Base a) anno
tag LocTag
anno forall a b. (a -> b) -> a -> b
$ forall a. FragExpr a -> FragExpr a
LeftFrag forall a. FragExpr a
EnvFrag)
                                                                                                  (forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a anno. Recursive a => anno -> a -> Cofree (Base a) anno
tag LocTag
anno forall a b. (a -> b) -> a -> b
$ forall a. FragExpr a -> FragExpr a
RightFrag forall a. FragExpr a
EnvFrag))
    in forall anno (a :: * -> *). anno -> Cofree a anno -> Cofree a anno
rewriteOuterTag LocTag
anno forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a b. BreakState' a b -> BreakState' a b
setEnvF (forall a b. BreakState' a b -> BreakState' a b -> BreakState' a b
pairF BreakState' RecursionPieceFrag UnsizedRecursionToken
performTC (forall a b. BreakState' a b -> BreakState' a b -> BreakState' a b
pairF (Term2 -> BreakState' RecursionPieceFrag UnsizedRecursionToken
splitExpr' Term2
tc) (Term2 -> BreakState' RecursionPieceFrag UnsizedRecursionToken
splitExpr' Term2
c)))
  (LocTag
anno :< TITEF Term2
i Term2
t Term2
e) -> forall anno (a :: * -> *). anno -> Cofree a anno -> Cofree a anno
rewriteOuterTag LocTag
anno forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a b. BreakState' a b -> BreakState' a b
setEnvF (forall a b. BreakState' a b -> BreakState' a b -> BreakState' a b
pairF (forall a b. BreakState' a b -> BreakState' a b -> BreakState' a b
gateF (Term2 -> BreakState' RecursionPieceFrag UnsizedRecursionToken
splitExpr' Term2
e) (Term2 -> BreakState' RecursionPieceFrag UnsizedRecursionToken
splitExpr' Term2
t)) (Term2 -> BreakState' RecursionPieceFrag UnsizedRecursionToken
splitExpr' Term2
i))
  (LocTag
anno :< TLeftF Term2
x) -> (LocTag
anno forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:<) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a r. r -> FragExprF a r
LeftFragF forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term2 -> BreakState' RecursionPieceFrag UnsizedRecursionToken
splitExpr' Term2
x
  (LocTag
anno :< TRightF Term2
x) -> (LocTag
anno forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:<) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a r. r -> FragExprF a r
RightFragF forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term2 -> BreakState' RecursionPieceFrag UnsizedRecursionToken
splitExpr' Term2
x
  (LocTag
anno :< TTraceF Term2
x) -> forall anno (a :: * -> *). anno -> Cofree a anno -> Cofree a anno
rewriteOuterTag LocTag
anno forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a b. BreakState' a b -> BreakState' a b
setEnvF (forall a b. BreakState' a b -> BreakState' a b -> BreakState' a b
pairF (forall a b. Show a => BreakState' a b -> BreakState' a b
deferF (forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a anno. Recursive a => anno -> a -> Cofree (Base a) anno
tag LocTag
anno forall a b. (a -> b) -> a -> b
$ forall a. FragExpr a
TraceFrag)) (Term2 -> BreakState' RecursionPieceFrag UnsizedRecursionToken
splitExpr' Term2
x))
  (LocTag
anno :< TLamF (Open ()) Term2
x) -> forall anno (a :: * -> *). anno -> Cofree a anno -> Cofree a anno
rewriteOuterTag LocTag
anno forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a b. (Show a, Enum b) => BreakState' a b -> BreakState' a b
lamF (Term2 -> BreakState' RecursionPieceFrag UnsizedRecursionToken
splitExpr' Term2
x)
  (LocTag
anno :< TLamF (Closed ()) Term2
x) -> forall anno (a :: * -> *). anno -> Cofree a anno -> Cofree a anno
rewriteOuterTag LocTag
anno forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a b. (Show a, Enum b) => BreakState' a b -> BreakState' a b
clamF (Term2 -> BreakState' RecursionPieceFrag UnsizedRecursionToken
splitExpr' Term2
x)
  (LocTag
anno :< TChurchF Int
n) -> forall a b. (Show a, Enum b) => LocTag -> Int -> BreakState' a b
i2cF LocTag
anno Int
n
  (LocTag
anno :< TLimitedRecursionF Term2
t Term2
r Term2
b) ->
    forall anno (a :: * -> *). anno -> Cofree a anno -> Cofree a anno
rewriteOuterTag LocTag
anno forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall b a. (Enum b, Show b) => BreakState a b b
nextBreakToken forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>=
      (\UnsizedRecursionToken
x -> UnsizedRecursionToken
-> BreakState' RecursionPieceFrag UnsizedRecursionToken
-> BreakState' RecursionPieceFrag UnsizedRecursionToken
-> BreakState' RecursionPieceFrag UnsizedRecursionToken
-> BreakState' RecursionPieceFrag UnsizedRecursionToken
unsizedRecursionWrapper UnsizedRecursionToken
x (Term2 -> BreakState' RecursionPieceFrag UnsizedRecursionToken
splitExpr' Term2
t) (Term2 -> BreakState' RecursionPieceFrag UnsizedRecursionToken
splitExpr' Term2
r) (Term2 -> BreakState' RecursionPieceFrag UnsizedRecursionToken
splitExpr' Term2
b)))

newtype FragExprUR' =
  FragExprUR' { FragExprUR' -> FragExpr (RecursionSimulationPieces FragExprUR')
unFragExprUR' :: FragExpr (RecursionSimulationPieces FragExprUR')
              }
  deriving (FragExprUR' -> FragExprUR' -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: FragExprUR' -> FragExprUR' -> Bool
$c/= :: FragExprUR' -> FragExprUR' -> Bool
== :: FragExprUR' -> FragExprUR' -> Bool
$c== :: FragExprUR' -> FragExprUR' -> Bool
Eq, Int -> FragExprUR' -> ShowS
[FragExprUR'] -> ShowS
FragExprUR' -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [FragExprUR'] -> ShowS
$cshowList :: [FragExprUR'] -> ShowS
show :: FragExprUR' -> String
$cshow :: FragExprUR' -> String
showsPrec :: Int -> FragExprUR' -> ShowS
$cshowsPrec :: Int -> FragExprUR' -> ShowS
Show)

newtype Term3' = Term3' (Map FragIndex FragExprUR') deriving (Term3' -> Term3' -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Term3' -> Term3' -> Bool
$c/= :: Term3' -> Term3' -> Bool
== :: Term3' -> Term3' -> Bool
$c== :: Term3' -> Term3' -> Bool
Eq, Int -> Term3' -> ShowS
[Term3'] -> ShowS
Term3' -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Term3'] -> ShowS
$cshowList :: [Term3'] -> ShowS
show :: Term3' -> String
$cshow :: Term3' -> String
showsPrec :: Int -> Term3' -> ShowS
$cshowsPrec :: Int -> Term3' -> ShowS
Show)

splitExpr :: Term2 -> Term3
splitExpr :: Term2 -> Term3
splitExpr Term2
t = let (Cofree (FragExprF RecursionPieceFrag) LocTag
bf, (UnsizedRecursionToken
_,FragIndex
_,Map FragIndex (Cofree (FragExprF RecursionPieceFrag) LocTag)
m)) = forall s a. State s a -> s -> (a, s)
State.runState (Term2 -> BreakState' RecursionPieceFrag UnsizedRecursionToken
splitExpr' Term2
t) (forall a. Enum a => Int -> a
toEnum Int
0, Int -> FragIndex
FragIndex Int
1, forall k a. Map k a
Map.empty)
              in Map FragIndex FragExprUR -> Term3
Term3 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b k. (a -> b) -> Map k a -> Map k b
Map.map Cofree (FragExprF RecursionPieceFrag) LocTag -> FragExprUR
FragExprUR forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (Int -> FragIndex
FragIndex Int
0) Cofree (FragExprF RecursionPieceFrag) LocTag
bf Map FragIndex (Cofree (FragExprF RecursionPieceFrag) LocTag)
m


-- |`makeLambda ps vl t1` makes a `TLam` around `t1` with `vl` as arguments.
-- Automatic recognition of Close or Open type of `TLam`.
makeLambda :: [(String, AnnotatedUPT)] -- ^Bindings
           -> String                            -- ^Variable name
           -> Term1                             -- ^Lambda body
           -> Term1
makeLambda :: [(String, AnnotatedUPT)] -> String -> Term1 -> Term1
makeLambda [(String, AnnotatedUPT)]
bindings String
str term1 :: Term1
term1@(LocTag
anno :< ParserTermF String String Term1
_) =
  if Set String
unbound forall a. Eq a => a -> a -> Bool
== forall a. Set a
Set.empty then LocTag
anno forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall l v r. LamType l -> r -> ParserTermF l v r
TLamF (forall l. l -> LamType l
Closed String
str) Term1
term1 else LocTag
anno forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall l v r. LamType l -> r -> ParserTermF l v r
TLamF (forall l. l -> LamType l
Open String
str) Term1
term1
  where bindings' :: Set String
bindings' = forall a. Ord a => [a] -> Set a
Set.fromList forall a b. (a -> b) -> a -> b
$ forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(String, AnnotatedUPT)]
bindings
        v :: Set String
v = Term1 -> Set String
varsTerm1 Term1
term1
        unbound :: Set String
unbound = (Set String
v forall a. Ord a => Set a -> Set a -> Set a
\\ Set String
bindings') forall a. Ord a => Set a -> Set a -> Set a
\\ forall a. a -> Set a
Set.singleton String
str

-- |Transformation from `AnnotatedUPT` to `Term1` validating and inlining `VarUP`s
validateVariables :: [(String, AnnotatedUPT)] -- ^ Prelude
                  -> AnnotatedUPT
                  -> Either String Term1
validateVariables :: [(String, AnnotatedUPT)] -> AnnotatedUPT -> Either String Term1
validateVariables [(String, AnnotatedUPT)]
prelude AnnotatedUPT
term =
  let validateWithEnvironment :: AnnotatedUPT
                              -> State.StateT (Map String Term1) (Either String) Term1
      validateWithEnvironment :: AnnotatedUPT -> StateT (Map String Term1) (Either String) Term1
validateWithEnvironment = \case
        LocTag
anno :< LamUPF String
v AnnotatedUPT
x -> do
          Map String Term1
oldState <- forall s (m :: * -> *). MonadState s m => m s
State.get
          forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
State.modify (forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert String
v (LocTag
anno forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall l v r. v -> ParserTermF l v r
TVarF String
v))
          Term1
result <- AnnotatedUPT -> StateT (Map String Term1) (Either String) Term1
validateWithEnvironment AnnotatedUPT
x
          forall s (m :: * -> *). MonadState s m => s -> m ()
State.put Map String Term1
oldState
          forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ [(String, AnnotatedUPT)] -> String -> Term1 -> Term1
makeLambda [(String, AnnotatedUPT)]
prelude String
v Term1
result
        LocTag
anno :< VarUPF String
n -> do
          Map String Term1
definitionsMap <- forall s (m :: * -> *). MonadState s m => m s
State.get
          case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup String
n Map String Term1
definitionsMap of
            Just Term1
v -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Term1
v
            Maybe Term1
_      -> forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
State.lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. a -> Either a b
Left  forall a b. (a -> b) -> a -> b
$ String
"No definition found for " forall a. Semigroup a => a -> a -> a
<> String
n
        LocTag
anno :< LetUPF [(String, AnnotatedUPT)]
preludeMap AnnotatedUPT
inner -> do
          Map String Term1
oldPrelude <- forall s (m :: * -> *). MonadState s m => m s
State.get
          let addBinding :: (String, AnnotatedUPT)
-> StateT (Map String Term1) (Either String) ()
addBinding (String
k,AnnotatedUPT
v) = do
                Term1
newTerm <- AnnotatedUPT -> StateT (Map String Term1) (Either String) Term1
validateWithEnvironment AnnotatedUPT
v
                forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
State.modify (forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert String
k Term1
newTerm)
          forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (String, AnnotatedUPT)
-> StateT (Map String Term1) (Either String) ()
addBinding [(String, AnnotatedUPT)]
preludeMap
          Term1
result <- AnnotatedUPT -> StateT (Map String Term1) (Either String) Term1
validateWithEnvironment AnnotatedUPT
inner
          forall s (m :: * -> *). MonadState s m => s -> m ()
State.put Map String Term1
oldPrelude
          forall (f :: * -> *) a. Applicative f => a -> f a
pure Term1
result
        LocTag
anno :< ITEUPF AnnotatedUPT
i AnnotatedUPT
t AnnotatedUPT
e -> (\Term1
a Term1
b Term1
c -> LocTag
anno forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall l v r. r -> r -> r -> ParserTermF l v r
TITEF Term1
a Term1
b Term1
c) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> AnnotatedUPT -> StateT (Map String Term1) (Either String) Term1
validateWithEnvironment AnnotatedUPT
i
                                                                forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> AnnotatedUPT -> StateT (Map String Term1) (Either String) Term1
validateWithEnvironment AnnotatedUPT
t
                                                                forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> AnnotatedUPT -> StateT (Map String Term1) (Either String) Term1
validateWithEnvironment AnnotatedUPT
e
        LocTag
anno :< IntUPF Int
x -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall l v. LocTag -> Int -> Cofree (ParserTermF l v) LocTag
i2t LocTag
anno Int
x
        LocTag
anno :< StringUPF String
s -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall l v. LocTag -> String -> Cofree (ParserTermF l v) LocTag
s2t LocTag
anno String
s
        LocTag
anno :< PairUPF AnnotatedUPT
a AnnotatedUPT
b -> (\Term1
x Term1
y -> LocTag
anno forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall l v r. r -> r -> ParserTermF l v r
TPairF Term1
x Term1
y) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> AnnotatedUPT -> StateT (Map String Term1) (Either String) Term1
validateWithEnvironment AnnotatedUPT
a
                                                            forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> AnnotatedUPT -> StateT (Map String Term1) (Either String) Term1
validateWithEnvironment AnnotatedUPT
b
        LocTag
anno :< ListUPF [AnnotatedUPT]
l -> forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\Term1
x Term1
y -> LocTag
anno forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall l v r. r -> r -> ParserTermF l v r
TPairF Term1
x Term1
y) (LocTag
anno forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall l v r. ParserTermF l v r
TZeroF) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM AnnotatedUPT -> StateT (Map String Term1) (Either String) Term1
validateWithEnvironment [AnnotatedUPT]
l
        LocTag
anno :< AppUPF AnnotatedUPT
f AnnotatedUPT
x -> (\Term1
a Term1
b -> LocTag
anno forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall l v r. r -> r -> ParserTermF l v r
TAppF Term1
a Term1
b) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> AnnotatedUPT -> StateT (Map String Term1) (Either String) Term1
validateWithEnvironment AnnotatedUPT
f
                                                          forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> AnnotatedUPT -> StateT (Map String Term1) (Either String) Term1
validateWithEnvironment AnnotatedUPT
x
        LocTag
anno :< UnsizedRecursionUPF AnnotatedUPT
t AnnotatedUPT
r AnnotatedUPT
b ->
          (\Term1
x Term1
y Term1
z -> LocTag
anno forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall l v r. r -> r -> r -> ParserTermF l v r
TLimitedRecursionF Term1
x Term1
y Term1
z) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> AnnotatedUPT -> StateT (Map String Term1) (Either String) Term1
validateWithEnvironment AnnotatedUPT
t
                                                       forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> AnnotatedUPT -> StateT (Map String Term1) (Either String) Term1
validateWithEnvironment AnnotatedUPT
r
                                                       forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> AnnotatedUPT -> StateT (Map String Term1) (Either String) Term1
validateWithEnvironment AnnotatedUPT
b
        -- anno :< ChurchUPF n -> pure $ i2c anno n
        LocTag
anno :< ChurchUPF Int
n -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ LocTag
anno forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall l v r. Int -> ParserTermF l v r
TChurchF Int
n
        LocTag
anno :< LeftUPF AnnotatedUPT
x -> (\Term1
y -> LocTag
anno forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall l v r. r -> ParserTermF l v r
TLeftF Term1
y) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> AnnotatedUPT -> StateT (Map String Term1) (Either String) Term1
validateWithEnvironment AnnotatedUPT
x
        LocTag
anno :< RightUPF AnnotatedUPT
x -> (\Term1
y -> LocTag
anno forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall l v r. r -> ParserTermF l v r
TRightF Term1
y) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> AnnotatedUPT -> StateT (Map String Term1) (Either String) Term1
validateWithEnvironment AnnotatedUPT
x
        LocTag
anno :< TraceUPF AnnotatedUPT
x -> (\Term1
y -> LocTag
anno forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall l v r. r -> ParserTermF l v r
TTraceF Term1
y) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> AnnotatedUPT -> StateT (Map String Term1) (Either String) Term1
validateWithEnvironment AnnotatedUPT
x
        LocTag
anno :< CheckUPF AnnotatedUPT
cf AnnotatedUPT
x -> (\Term1
y Term1
y'-> LocTag
anno forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall l v r. r -> r -> ParserTermF l v r
TCheckF Term1
y Term1
y') forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> AnnotatedUPT -> StateT (Map String Term1) (Either String) Term1
validateWithEnvironment AnnotatedUPT
cf forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> AnnotatedUPT -> StateT (Map String Term1) (Either String) Term1
validateWithEnvironment AnnotatedUPT
x
        LocTag
anno :< HashUPF AnnotatedUPT
x -> (\Term1
y -> LocTag
anno forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall l v r. r -> ParserTermF l v r
THashF Term1
y) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> AnnotatedUPT -> StateT (Map String Term1) (Either String) Term1
validateWithEnvironment AnnotatedUPT
x
  in forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
State.evalStateT (AnnotatedUPT -> StateT (Map String Term1) (Either String) Term1
validateWithEnvironment AnnotatedUPT
term) forall k a. Map k a
Map.empty

-- |Collect all free variable names in a `Term1` expresion
varsTerm1 :: Term1 -> Set String
varsTerm1 :: Term1 -> Set String
varsTerm1 = forall t a. Recursive t => (Base t a -> a) -> t -> a
cata forall a.
CofreeF (ParserTermF String String) a (Set String) -> Set String
alg where
  alg :: CofreeF (ParserTermF String String) a (Set String) -> Set String
  alg :: forall a.
CofreeF (ParserTermF String String) a (Set String) -> Set String
alg (a
_ C.:< (TVarF String
n))          = forall a. a -> Set a
Set.singleton String
n
  alg (a
_ C.:< TLamF (Open String
n) Set String
x)   = String -> Set String -> Set String
del String
n Set String
x
  alg (a
_ C.:< TLamF (Closed String
n) Set String
x) = String -> Set String -> Set String
del String
n Set String
x
  alg CofreeF (ParserTermF String String) a (Set String)
e                           = forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
F.fold CofreeF (ParserTermF String String) a (Set String)
e
  del :: String -> Set String -> Set String
  del :: String -> Set String -> Set String
del String
n Set String
x = if forall a. Ord a => a -> Set a -> Bool
Set.member String
n Set String
x then forall a. Ord a => a -> Set a -> Set a
Set.delete String
n Set String
x else Set String
x

optimizeBuiltinFunctions :: AnnotatedUPT -> AnnotatedUPT
optimizeBuiltinFunctions :: AnnotatedUPT -> AnnotatedUPT
optimizeBuiltinFunctions = forall a. Plated a => (a -> a) -> a -> a
transform forall {a}.
Cofree UnprocessedParsedTermF a -> Cofree UnprocessedParsedTermF a
optimize where
  optimize :: Cofree UnprocessedParsedTermF a -> Cofree UnprocessedParsedTermF a
optimize = \case
    twoApp :: Cofree UnprocessedParsedTermF a
twoApp@(a
anno0 :< AppUPF (a
_ :< AppUPF (a
_ :< UnprocessedParsedTermF (Cofree UnprocessedParsedTermF a)
f) Cofree UnprocessedParsedTermF a
x) Cofree UnprocessedParsedTermF a
y) ->
      case UnprocessedParsedTermF (Cofree UnprocessedParsedTermF a)
f of
        VarUPF String
"pair" -> a
anno0 forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall r. r -> r -> UnprocessedParsedTermF r
PairUPF Cofree UnprocessedParsedTermF a
x Cofree UnprocessedParsedTermF a
y
        VarUPF String
"app"  -> a
anno0 forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall r. r -> r -> UnprocessedParsedTermF r
AppUPF Cofree UnprocessedParsedTermF a
x Cofree UnprocessedParsedTermF a
y
        UnprocessedParsedTermF (Cofree UnprocessedParsedTermF a)
_             -> Cofree UnprocessedParsedTermF a
twoApp
    oneApp :: Cofree UnprocessedParsedTermF a
oneApp@(a
anno0 :< AppUPF (a
anno1 :< UnprocessedParsedTermF (Cofree UnprocessedParsedTermF a)
f) Cofree UnprocessedParsedTermF a
x) ->
      case UnprocessedParsedTermF (Cofree UnprocessedParsedTermF a)
f of
        VarUPF String
"left"  -> a
anno0 forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall r. r -> UnprocessedParsedTermF r
LeftUPF Cofree UnprocessedParsedTermF a
x
        VarUPF String
"right" -> a
anno0 forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall r. r -> UnprocessedParsedTermF r
RightUPF Cofree UnprocessedParsedTermF a
x
        VarUPF String
"trace" -> a
anno0 forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall r. r -> UnprocessedParsedTermF r
TraceUPF Cofree UnprocessedParsedTermF a
x
        VarUPF String
"pair"  -> a
anno0 forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall r. String -> r -> UnprocessedParsedTermF r
LamUPF String
"y" (a
anno1 forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall r. r -> r -> UnprocessedParsedTermF r
PairUPF Cofree UnprocessedParsedTermF a
x (a
anno1 forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall r. String -> UnprocessedParsedTermF r
VarUPF String
"y"))
        VarUPF String
"app"   -> a
anno0 forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall r. String -> r -> UnprocessedParsedTermF r
LamUPF String
"y" (a
anno1 forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall r. r -> r -> UnprocessedParsedTermF r
AppUPF Cofree UnprocessedParsedTermF a
x (a
anno1 forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall r. String -> UnprocessedParsedTermF r
VarUPF String
"y"))
        UnprocessedParsedTermF (Cofree UnprocessedParsedTermF a)
_             -> Cofree UnprocessedParsedTermF a
oneApp
        -- VarUP "check" TODO
    Cofree UnprocessedParsedTermF a
x -> Cofree UnprocessedParsedTermF a
x

-- |Process an `Term2` to have all `HashUP` replaced by a unique number.
-- The unique number is constructed by doing a SHA1 hash of the Term2 and
-- adding one for all consecutive HashUP's.
generateAllHashes :: Term2 -> Term2
generateAllHashes :: Term2 -> Term2
generateAllHashes x :: Term2
x@(LocTag
anno :< ParserTermF () Int Term2
_) = forall a. Plated a => (a -> a) -> a -> a
transform Term2 -> Term2
interm Term2
x where
  hash' :: ByteString -> Digest SHA256
  hash' :: ByteString -> Digest SHA256
hash' = forall ba a.
(ByteArrayAccess ba, HashAlgorithm a) =>
ba -> Digest a
hash
  term2Hash :: Term2 -> ByteString
  term2Hash :: Term2 -> ByteString
term2Hash = [Word8] -> ByteString
BS.pack forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. ByteArrayAccess a => a -> [Word8]
BA.unpack forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> Digest SHA256
hash' forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Word8] -> ByteString
BS.pack forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> [Word8]
encode forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String
show forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a anno. Corecursive a => Cofree (Base a) anno -> a
forget :: Cofree (ParserTermF () Int) LocTag -> ParserTerm () Int)
  bs2Term2 :: ByteString -> Term2
  bs2Term2 :: ByteString -> Term2
bs2Term2 ByteString
bs = forall l v. LocTag -> [Int] -> Cofree (ParserTermF l v) LocTag
ints2t LocTag
anno forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Int -> [a] -> [a]
drop Int
24 forall a b. (a -> b) -> a -> b
$ forall a. Num a => Integer -> a
fromInteger forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Integral a => a -> Integer
toInteger forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ByteString -> [Word8]
BS.unpack ByteString
bs
  interm :: Term2 -> Term2
  interm :: Term2 -> Term2
interm = \case
    (LocTag
anno :< THashF Term2
term1) -> ByteString -> Term2
bs2Term2 forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term2 -> ByteString
term2Hash forall a b. (a -> b) -> a -> b
$ Term2
term1
    Term2
x                      -> Term2
x

addBuiltins :: AnnotatedUPT -> AnnotatedUPT
addBuiltins :: AnnotatedUPT -> AnnotatedUPT
addBuiltins AnnotatedUPT
aupt = LocTag
DummyLoc forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall r. [(String, r)] -> r -> UnprocessedParsedTermF r
LetUPF
  [ (String
"zero", LocTag
DummyLoc forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall r. Int -> UnprocessedParsedTermF r
IntUPF Int
0)
  , (String
"left", LocTag
DummyLoc forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall r. String -> r -> UnprocessedParsedTermF r
LamUPF String
"x" (LocTag
DummyLoc forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall r. r -> UnprocessedParsedTermF r
LeftUPF (LocTag
DummyLoc forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall r. String -> UnprocessedParsedTermF r
VarUPF String
"x")))
  , (String
"right", LocTag
DummyLoc forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall r. String -> r -> UnprocessedParsedTermF r
LamUPF String
"x" (LocTag
DummyLoc forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall r. r -> UnprocessedParsedTermF r
RightUPF (LocTag
DummyLoc forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall r. String -> UnprocessedParsedTermF r
VarUPF String
"x")))
  , (String
"trace", LocTag
DummyLoc forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall r. String -> r -> UnprocessedParsedTermF r
LamUPF String
"x" (LocTag
DummyLoc forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall r. r -> UnprocessedParsedTermF r
TraceUPF (LocTag
DummyLoc forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall r. String -> UnprocessedParsedTermF r
VarUPF String
"x")))
  , (String
"pair", LocTag
DummyLoc forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall r. String -> r -> UnprocessedParsedTermF r
LamUPF String
"x" (LocTag
DummyLoc forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall r. String -> r -> UnprocessedParsedTermF r
LamUPF String
"y" (LocTag
DummyLoc forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall r. r -> r -> UnprocessedParsedTermF r
PairUPF (LocTag
DummyLoc forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall r. String -> UnprocessedParsedTermF r
VarUPF String
"x") (LocTag
DummyLoc forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall r. String -> UnprocessedParsedTermF r
VarUPF String
"y"))))
  , (String
"app", LocTag
DummyLoc forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall r. String -> r -> UnprocessedParsedTermF r
LamUPF String
"x" (LocTag
DummyLoc forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall r. String -> r -> UnprocessedParsedTermF r
LamUPF String
"y" (LocTag
DummyLoc forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall r. r -> r -> UnprocessedParsedTermF r
AppUPF (LocTag
DummyLoc forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall r. String -> UnprocessedParsedTermF r
VarUPF String
"x") (LocTag
DummyLoc forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall r. String -> UnprocessedParsedTermF r
VarUPF String
"y"))))
  ]
  AnnotatedUPT
aupt

-- |Process an `AnnotatedUPT` to a `Term3` with failing capability.
process :: [(String, AnnotatedUPT)] -- ^Prelude
        -> AnnotatedUPT
        -> Either String Term3
process :: [(String, AnnotatedUPT)] -> AnnotatedUPT -> Either String Term3
process [(String, AnnotatedUPT)]
prelude AnnotatedUPT
upt = (\Term3
dt -> forall a. String -> a -> a
debugTrace (String
"Resolver process term:\n" forall a. Semigroup a => a -> a -> a
<> forall p. PrettyPrintable p => p -> String
prettyPrint Term3
dt) Term3
dt) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term2 -> Term3
splitExpr forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(String, AnnotatedUPT)] -> AnnotatedUPT -> Either String Term2
process2Term2 [(String, AnnotatedUPT)]
prelude AnnotatedUPT
upt

process2Term2 :: [(String, AnnotatedUPT)] -- ^Prelude
              -> AnnotatedUPT
              -> Either String Term2
process2Term2 :: [(String, AnnotatedUPT)] -> AnnotatedUPT -> Either String Term2
process2Term2 [(String, AnnotatedUPT)]
prelude = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Term2 -> Term2
generateAllHashes
                      forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *). MonadFail m => [String] -> Term1 -> m Term2
debruijinize [] forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< [(String, AnnotatedUPT)] -> AnnotatedUPT -> Either String Term1
validateVariables [(String, AnnotatedUPT)]
prelude
                      forall b c a. (b -> c) -> (a -> b) -> a -> c
. AnnotatedUPT -> AnnotatedUPT
removeCaseUPs
                      forall b c a. (b -> c) -> (a -> b) -> a -> c
. AnnotatedUPT -> AnnotatedUPT
optimizeBuiltinFunctions
                      forall b c a. (b -> c) -> (a -> b) -> a -> c
. AnnotatedUPT -> AnnotatedUPT
addBuiltins

-- |Helper function to compile to Term2
runTelomareParser2Term2 :: TelomareParser AnnotatedUPT -- ^Parser to run
                        -> [(String, AnnotatedUPT)]    -- ^Prelude
                        -> String                               -- ^Raw string to be parsed
                        -> Either String Term2                  -- ^Error on Left
runTelomareParser2Term2 :: TelomareParser AnnotatedUPT
-> [(String, AnnotatedUPT)] -> String -> Either String Term2
runTelomareParser2Term2 TelomareParser AnnotatedUPT
parser [(String, AnnotatedUPT)]
prelude String
str =
  forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first forall s e.
(VisualStream s, TraversableStream s, ShowErrorComponent e) =>
ParseErrorBundle s e -> String
errorBundlePretty (forall e s a.
Parsec e s a -> String -> s -> Either (ParseErrorBundle s e) a
runParser TelomareParser AnnotatedUPT
parser String
"" String
str) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= [(String, AnnotatedUPT)] -> AnnotatedUPT -> Either String Term2
process2Term2 [(String, AnnotatedUPT)]
prelude

parseMain :: [(String, AnnotatedUPT)] -- ^Prelude: [(VariableName, BindedUPT)]
          -> String                            -- ^Raw string to be parserd.
          -> Either String Term3               -- ^Error on Left.
parseMain :: [(String, AnnotatedUPT)] -> String -> Either String Term3
parseMain [(String, AnnotatedUPT)]
prelude String
s = [(String, AnnotatedUPT)] -> String -> Either String AnnotatedUPT
parseWithPrelude [(String, AnnotatedUPT)]
prelude String
s forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= [(String, AnnotatedUPT)] -> AnnotatedUPT -> Either String Term3
process [(String, AnnotatedUPT)]
prelude