content: {-# LANGUAGE DerivingVia #-}
  {-# LANGUAGE DeriveGeneric #-}
  {-# LANGUAGE DeriveAnyClass #-}
  {-# LANGUAGE FlexibleContexts #-}
  {-# LANGUAGE FlexibleInstances #-}
  {-# LANGUAGE GeneralizedNewtypeDeriving #-}
  {-# LANGUAGE OverloadedStrings #-}
  {-# LANGUAGE TupleSections #-}
  {-# LANGUAGE TypeFamilies #-}
  module Syntax where
  
  import           Prelude hiding (id)
  import           SortContext (Context,Sort,Signature)
  import qualified SortContext as I
  
  import           Control.Monad.Except
  import           Control.Monad.Writer (Writer, tell, runWriter)
  import           Control.Monad.State
  import           Control.DeepSeq
  
  import           Data.ATerm
  import           Data.Constructor
  import           Data.HashMap.Lazy (HashMap)
  import qualified Data.HashMap.Lazy as M
  import           Data.HashSet (HashSet)
  import qualified Data.HashSet as H
  import           Data.Hashable
  import           Data.List (intercalate)
  import           Data.Set (Set)
  import qualified Data.Set as S
  import           Data.String (IsString(..))
  import           Data.Text (Text,pack,unpack)
  import qualified Data.Text as T
  import           Data.Lens(Prism')
  import qualified Data.Lens as L
  import           Data.Label
  import           Data.Empty
  import           Data.Order
  
  import           GHC.Generics(Generic)
  import           GHC.Exts(IsList(..))
  
  import           Text.Read (readMaybe)
  import           Test.QuickCheck (Arbitrary(..),Gen)
  import qualified Test.QuickCheck as Q
  
  import           Prettyprinter
  import           Text.Printf
  
  -- | Expressions for the Stratego core language are called strategies.
  data Strat
    = Fail Label
    | Id Label
    | Seq Strat Strat Label
    | GuardedChoice Strat Strat Strat Label
    | One Strat Label
    | Some Strat Label
    | All Strat Label
    | Match TermPattern Label
    | Build TermPattern Label
    | Scope [TermVar] Strat Label
    | Let [(StratVar,Strategy)] Strat Label
    | Call StratVar [Strat] [TermVar] Label
    | Prim StratVar [Strat] [TermVar] Label
    | Apply Strat Strat Label
    deriving stock (Generic)
    deriving PreOrd via Discrete Strat
    deriving anyclass NFData
  
  type LStrat = State Label Strat
  
  fail :: MonadState Label m => m Strat
  fail = Fail <$> fresh
  
  id :: MonadState Label m => m Strat
  id = Id <$> fresh
  
  seq :: MonadState Label m => m Strat -> m Strat -> m Strat
  seq e1 e2 = Seq <$> e1 <*> e2 <*> fresh
  
  guardedChoice :: MonadState Label m => m Strat -> m Strat -> m Strat -> m Strat
  guardedChoice e1 e2 e3 = GuardedChoice <$> e1 <*> e2 <*> e3 <*> fresh
  
  leftChoice :: MonadState Label m => m Strat -> m Strat -> m Strat
  leftChoice f = guardedChoice f id
  
  one :: MonadState Label m => m Strat -> m Strat
  one e = One <$> e <*> fresh
  
  some :: MonadState Label m => m Strat -> m Strat
  some e = Some <$> e <*> fresh
  
  all :: MonadState Label m => m Strat -> m Strat
  all e = All <$> e <*> fresh
  
  match :: MonadState Label m => TermPattern -> m Strat
  match pat = Match pat <$> fresh
  
  build :: MonadState Label m => TermPattern -> m Strat
  build pat = Build pat <$> fresh
  
  scope :: MonadState Label m => [TermVar] -> m Strat -> m Strat
  scope vars body = Scope vars <$> body <*> fresh
  
  let_ :: MonadState Label m => [(StratVar,m Strategy)] -> m Strat -> m Strat
  let_ binds body = Let <$> sequence [ (var,) <$> strat | (var,strat) <- binds ] <*> body <*> fresh
  
  call :: MonadState Label m => StratVar -> [m Strat] -> [TermVar] -> m Strat
  call sv ss tvs = Call <$> pure sv <*> sequence ss <*> pure tvs <*> fresh
  
  prim :: MonadState Label m => StratVar -> [m Strat] -> [TermVar] -> m Strat
  prim sv ss tvs = Prim <$> pure sv <*> sequence ss <*> pure tvs <*> fresh
  
  -- | Pattern to match and build terms.
  data TermPattern
    = As TermVar TermPattern
    | Cons Constructor [TermPattern]
    | Explode TermPattern TermPattern
    | Var TermVar
    | StringLiteral Text
    | NumberLiteral Int
    deriving stock (Eq,Generic)
    deriving anyclass (NFData,Hashable)
  
  -- | Stratego source code is organized in modules consisting of a
  -- signature describing possible shapes of terms and named strategies.
  data Module = Module Context Strategies
    deriving stock (Show,Eq)
  
  type Strategies = HashMap StratVar Strategy
  
  -- | A named strategy takes two kinds of arguments, arguments that
  -- refer to other named strategies and arguments that refer to terms.
  -- Additionally, a strategy takes and input term and eventually
  -- produces an output term.
  data Strategy = Strategy { strategyStratArguments :: [StratVar]
                           , strategyTermArguments :: [TermVar]
                           , strategyBody :: Strat
                           , strategyLabel :: Label
                           }
    deriving stock (Generic)
    deriving anyclass (NFData)
  
  instance Show Strategy where
    show strat = printf "%s:%s" (show (strategyLabel strat)) (show (strategyBody strat))
  
  instance HasLabel Strategy where
    label = strategyLabel
  
  instance Eq Strategy where
    s1 == s2 = label s1 == label s2
  
  instance Pretty Strategy where pretty = viaShow
  instance Pretty Strat where pretty = viaShow
  
  strategy :: MonadState Label m => [StratVar] -> [TermVar] -> m Strat -> m Strategy
  strategy svs tvs body = Strategy svs tvs <$> body <*> fresh
  
  -- data Closure = Closure Strategy StratEnv
  --   deriving stock (Eq,Generic)
  --   deriving PreOrd via Discrete Closure
  --   deriving anyclass (NFData,Hashable)
  
  type StratEnv = HashMap StratVar Strategy
  type LStratEnv = State Label StratEnv
  
  instance IsEmpty LStratEnv where
    empty = return empty
  
  stratEnv :: MonadState Label m => [(StratVar,m Strategy)] -> m StratEnv
  stratEnv l = M.fromList <$> sequence [ (sv,) <$> strat | (sv,strat) <- l ]
  
  filterStratEnv :: HashSet StratVar -> StratEnv -> StratEnv
  filterStratEnv vars = M.filterWithKey (\var _ -> var `H.member` vars)
  
  newtype TermVar = TermVar Text   deriving newtype (Eq,Ord,Hashable,NFData)
  newtype StratVar = StratVar Text deriving newtype (Eq,Ord,IsString,Hashable,NFData)
  
  liftStrategyScopes :: Strategy -> Strategy
  liftStrategyScopes (Strategy svs tvs s l) = Strategy svs tvs (liftStratScopes s l) l
  
  liftStratScopes :: Strat -> Label -> Strat
  liftStratScopes s l =
    let (s', vs) = runWriter (liftScopes s) in
    if length vs == S.size (S.fromList vs)
      then if null vs
        then s'
        else Scope vs s' l
      else error $ "found duplicate scope vars " ++ show vs
  
  liftScopes :: Strat -> Writer [TermVar] Strat
  liftScopes strat = case strat of
    Id l -> return (Id l)
    Fail l -> return (Fail l)
    Seq s1 s2 l -> do
      s1' <- liftScopes s1
      s2' <- liftScopes s2
      return $ Seq s1' s2' l
    GuardedChoice s1 s2 s3 l -> do
      s1' <- liftScopes s1
      s2' <- liftScopes s2
      s3' <- liftScopes s3
      return $ GuardedChoice s1' s2' s3' l
    One s l -> One <$> liftScopes s <*> pure l
    Some s l -> Some <$> liftScopes s <*> pure l
    All s l -> All <$> liftScopes s <*> pure l
    Scope xs s _ -> do
      tell xs
      liftScopes s
    Match f l -> return $ Match f l
    Build f l -> return $ Build f l
    Let bnds body l -> do
      let bnds' = map (\(v,s) -> (v,liftStrategyScopes s)) bnds
      body' <- liftScopes body
      return $ Let bnds' body' l
    Call f ss ts l -> do
      let ss' = map (\s -> liftStratScopes s l) ss
      return $ Call f ss' ts l
    Prim f ss ts l -> do
      let ss' = map (\s -> liftStratScopes s l) ss
      return $ Prim f ss' ts l
    Apply cll body l -> Apply <$> liftScopes cll <*> liftScopes body <*> pure l
  
  -- instance Monoid TermVarSet where
  --   mempty = TermVarSet mempty
  --   mappend (TermVarSet s1) (TermVarSet s2) =
  --     if S.null (S.intersection s1 s2)
  --       then TermVarSet $ S.union s1 s2
  --       else error $ "non-unique scope vars " ++ show (s1,s2)
  
  moduleStratEnv :: Module -> StratEnv
  moduleStratEnv (Module _ senv) = M.fromList [ (var,strat) | (var,strat) <- M.toList senv ]
  
  signature :: Module -> Context
  signature (Module sig _) = sig
  
  linear :: TermPattern -> Bool
  linear p = S.size (termVars p :: Set TermVar) == length (termVars p :: [TermVar])
  
  parseModule :: (MonadError String m, MonadState Label m) => ATerm -> m Module
  parseModule t = case t of
    ATerm "Specification" [List [sig, ATerm "Strategies" [List strats]]] ->
      Module <$> parseSignature sig <*> (M.fromList <$> traverse parseStrategy strats)
    _ -> throwError $ "unexpected input while parsing module from aterm: " ++ show t
  
  parseSignature :: MonadError String m => ATerm -> m Context
  parseSignature s = case s of
    ATerm "Signature" [List sig] -> parseConstructors sig I.empty
    _ -> throwError $ "unexpected input while parsing signature from aterm: " ++ show s
    where
      parseConstructors :: MonadError String m => [ATerm] -> Context -> m Context
      parseConstructors ts sig = case ts of
        ATerm "Constructors" [List constrs]:rest -> do
          sig' <- foldM parseDeclaration sig constrs
          parseConstructors rest sig'
        [] -> return sig
        _ -> throwError $ "unexpected input while parsing signature from aterm: " ++ show ts
  
  parseDeclaration :: MonadError String m => Context -> ATerm -> m Context
  parseDeclaration sig t
    | containsSortVar t = return sig
    | otherwise = case t of
        ATerm "OpDecl" [String con, body] -> do
          typ <- parseFun body
          return $ I.insertSignature (Constructor con) typ sig
        ATerm "OpDeclInj" [f@(ATerm "FunType" [_, ATerm "ConstType" [ATerm "SortTuple" _]])] ->
          parseDeclaration sig $ ATerm "OpDecl" [String "", f]
        ATerm "OpDeclInj" [ATerm "FunType" [List[ty1], ty2]] ->
          I.insertSubtype <$> parseSort ty1 <*> parseSort ty2 <*> pure sig
        ATerm "OpDeclInj" [ATerm "ConstType" _] ->
          return sig
        _ -> throwError $ "unexpected input while parsing declaration from aterm: " ++ show t  
    where
      containsSortVar :: ATerm -> Bool
      containsSortVar (ATerm "SortVar" _) = True
      containsSortVar (ATerm _ ts) = any containsSortVar ts
      containsSortVar (List ts) = any containsSortVar ts
      containsSortVar _ = False
  
  parseFun :: MonadError String m => ATerm -> m Signature
  parseFun t = case t of
    ATerm "ConstType" [res] -> I.Signature [] <$> parseSort res
    ATerm "FunType" [List args,res] -> I.Signature <$> traverse parseSort args <*> parseSort res
    _ -> throwError $ "unexpected input while parsing function type from aterm: " ++ show t
  
  parseSort :: MonadError String m => ATerm -> m Sort
  parseSort t = case t of
    ATerm "ConstType" [res] -> parseSort res
    ATerm "SortNoArgs" [String "String"] -> return I.Lexical
    ATerm "SortNoArgs" [String "Int"] -> return I.Numerical
    ATerm "SortNoArgs" [String sortName] -> return $ I.Sort (I.SortId sortName)
    ATerm "Sort" [String "String", List []] -> return I.Lexical
    ATerm "Sort" [String "Int", List []] -> return I.Numerical
    ATerm "Sort" [String sortName, List []] -> return $ I.Sort (I.SortId sortName)
    ATerm "Sort" [String "List", List [s]] -> I.List <$> parseSort s
    ATerm "Sort" [String "List", List ss] -> I.List . I.Tuple <$> traverse parseSort ss
    ATerm "Sort" [String "Option", List [s]] -> I.Option <$> parseSort s
    ATerm "Sort" [String "Option", List ss] -> I.Option . I.Tuple <$> traverse parseSort ss
    ATerm "SortTuple" [List args] -> I.Tuple <$> traverse parseSort args
    _ -> throwError $ "unexpected input while parsing sort from aterm: " ++ show t
  
  parseStrategy :: (MonadError String m, MonadState Label m) => ATerm -> m (StratVar,Strategy)
  parseStrategy strat = case strat of
    ATerm "SDefT" [String name, List stratVars, List ts, body] -> do
      svs <- parseStratVars stratVars
      tvs <- parseTermVars ts
      str <- strategy svs tvs (parseStrat body)
      return (StratVar name, liftStrategyScopes str)
    ATerm "ExtSDef" [String name, List ts, List stratVars] -> do
      svs <- parseStratVars stratVars
      tvs <- parseTermVars ts
      str <- strategy svs tvs id
      return (StratVar name, liftStrategyScopes str)
    _ -> throwError $ "unexpected input while parsing strategy from aterm: " ++ show strat
  
  parseStratVars :: MonadError String m => [ATerm] -> m [StratVar]
  parseStratVars vars =
    forM vars $ \var -> case var of
      ATerm "VarDec" [String name, _] -> return $ StratVar name
      ATerm _ [String x] -> return $ StratVar x
      _ -> throwError $ "unexpected input while parsing strategy variables from aterm: " ++ show var
  
  parseTermVar :: MonadError String m => ATerm -> m TermVar
  parseTermVar var = case var of 
    ATerm "VarDec" [String name, _] -> return $ TermVar name
    ATerm "Var" [String name] -> return $ TermVar name
    ATerm "Wld" [] -> return $ TermVar "_"
    ATerm "Str" [String ""] -> return $ TermVar "_"
    String name -> return $ TermVar name
    _ -> throwError $ "unexpected input while parsing term variables from aterm: " ++ show var
  
  parseTermVars :: MonadError String m => [ATerm] -> m [TermVar]
  parseTermVars = traverse parseTermVar
  
  parseStrat :: (MonadError String m, MonadState Label m) => ATerm -> m Strat
  parseStrat t = case t of
    ATerm "Id" [] -> Id <$> fresh
    ATerm "Fail" [] -> Fail <$> fresh
    ATerm "Seq" [e1, e2] -> Seq <$> parseStrat e1 <*> parseStrat e2 <*> fresh
    ATerm "GuardedLChoice" [e1, e2, e3] -> GuardedChoice <$> parseStrat e1 <*> parseStrat e2 <*> parseStrat e3 <*> fresh
    ATerm "All" [e] -> All <$> parseStrat e <*> fresh
    ATerm "Some" [e] -> Some <$> parseStrat e <*> fresh
    ATerm "One" [e] -> One <$> parseStrat e <*> fresh
    ATerm "Match" [tp] -> Match <$> parseTermPattern tp <*> fresh
    ATerm "Build" [tp] -> Build <$> parseTermPattern tp <*> fresh
    ATerm "Scope" [List vars, e] -> Scope <$> parseTermVars vars <*> parseStrat e <*> fresh
    ATerm "Let" [List strats, body] ->
      Let <$> traverse parseStrategy strats <*> parseStrat body <*> fresh
    ATerm "CallT" [ATerm "SVar" [String svar], List stratArgs, List termArgs] ->
      Call (StratVar svar) <$> traverse parseStrat stratArgs <*> parseTermVars termArgs <*> fresh
    ATerm "PrimT" [String svar, List stratArgs, List termArgs] ->
      Prim (StratVar svar) <$> traverse parseStrat stratArgs <*> parseTermVars termArgs <*> fresh
    _ -> throwError $ "unexpected input while parsing strategy from aterm: " ++ show t
  
  parseTermPattern :: MonadError String m => ATerm -> m TermPattern
  parseTermPattern p = case p of
    ATerm "Anno" [p1,_] -> parseTermPattern p1 -- Ignore annotations
    ATerm "As" [v@(ATerm "Var" _), p1] -> As <$> parseTermVar v <*> parseTermPattern p1
    ATerm "Op" [String con, List subterms] ->
      Cons (Constructor con) <$> traverse parseTermPattern subterms
    ATerm "Str" [String str] -> return $ StringLiteral str
    ATerm "Var" _ -> Var <$> parseTermVar p
    ATerm "Wld" _ -> Var <$> parseTermVar p
    ATerm "Explode" [p1,p2] -> Explode <$> parseTermPattern p1 <*> parseTermPattern p2
    ATerm "Int" [i] -> NumberLiteral <$> parseInt i
    _ -> throwError $ "unexpected input while parsing term pattern from aterm: " ++ show p
  
  
  parseInt :: MonadError String m => ATerm -> m Int
  parseInt s = case s of
    String t -> case readMaybe (T.unpack t) of
      Just i -> return i
      Nothing -> throwError $ "could not parse integer literal from text: " ++ show t
    _ -> throwError $ "unexpected input while parsing integer literal from aterm: " ++ show s
  
  instance Arbitrary TermVar where
    arbitrary = TermVar . T.singleton <$> Q.choose ('a','z')
  
  instance Show TermVar where
    show (TermVar x) = unpack x
  
  instance IsString TermVar where
    fromString = TermVar . pack
  
  instance Pretty TermVar where
    pretty (TermVar x) = pretty x
  
  instance IsString TermPattern where
    fromString = Var . fromString
  
  instance Show TermPattern where
    show (As v t) = show v ++ "@(" ++ show t ++ ")"
    show (Cons c ts) = show c ++ if null ts then "" else show ts
    show (Var x) = show x
    show (Explode f xs) = show f ++ "#(" ++ show xs ++ ")"
    show (StringLiteral s) = show s
    show (NumberLiteral n) = show n
  
  -- instance IsString Strat where
  --   fromString s = Call (fromString s) [] [] 
  
  instance HasLabel Strat where
    label x = case x of
      Fail l -> l
      Id l -> l
      Seq _ _ l -> l
      GuardedChoice _ _ _ l -> l
      One _ l -> l
      Some _ l -> l
      All _ l -> l
      Match _ l -> l
      Build _ l -> l
      Scope _ _ l -> l
      Call _ _ _ l -> l
      Let _ _ l -> l
      Prim _ _ _ l -> l
      Apply _ _ l -> l
  
  instance Eq Strat where
    s1 == s2 = label s1 == label s2
  
  instance Hashable Strat where
    hashWithSalt s x = s `hashWithSalt` label x
  
  instance Show Strat where
    showsPrec d s0 = case s0 of
      Fail _ ->
        showString "fail"
      Id _ ->
        showString "id"
      Seq s1 s2 _ ->
        showParen (d > seq_prec)
          $ showsPrec seq_prec s1
          . showString "; "
          . showsPrec seq_prec s2
      GuardedChoice s1 s2 s3 _ ->
        showParen (d > choice_prec)
          $ showsPrec (choice_prec+1) s1
          . showString " < "
          . showsPrec (choice_prec+1) s2
          . showString " + "
          . showsPrec (choice_prec+1) s3
      One s _ ->
        showParen (d > app_prec)
          $ showString "one "
          . showsPrec (app_prec+1) s
      Some s _ ->
        showParen (d > app_prec)
          $ showString "some "
          . showsPrec (app_prec+1) s
      All s _ ->
        showParen (d > app_prec)
          $ showString "all "
          . showsPrec (app_prec+1) s
      Match t _ ->
        showString "?"
          . showsPrec (app_prec+1) t
      Build t _ ->
        showString "!"
          . showsPrec (app_prec+1) t
      Scope vars s _ ->
        showString "{ "
        . showString (intercalate "," (map show vars))
        . showString ": "
        . shows s
        . showString " }"
      Call (StratVar f) ss ts _ ->
       showString (unpack f)
       . showString "("
       . showString (intercalate "," (map show ss))
       . showString "|"
       . showString (intercalate "," (map show ts))
       . showString ")"
      Apply cll body _ ->
        showString "Call: "
        . showsPrec d cll
        . showString " -> "
        . showString "Callee: "
        . showsPrec d body
      Prim (StratVar f) ss ts _ ->
       showString (unpack f)
       . showString "("
       . showString (intercalate "," (map show ss))
       . showString "|"
       . showString (intercalate "," (map show ts))
       . showString ")"
      Let ss body _ ->
       showString "let "
       . showString (intercalate "," (map show ss))
       . showString " in "
       . shows body
       . showString " end"
      where
        app_prec = 10
        seq_prec = 9
        choice_prec = 8
  
  instance Hashable Strategy where
    hashWithSalt s strat = s `hashWithSalt` strategyLabel strat
  
  instance Show StratVar where
    show (StratVar x) = unpack x
  
  instance Pretty StratVar where
    pretty (StratVar x) = pretty x
  
  instance Num TermPattern where
    t1 + t2 = Cons "Add" [t1,t2]
    t1 - t2 = Cons "Sub" [t1,t2]
    t1 * t2 = Cons "Mul" [t1,t2]
    abs t = Cons "Abs" [t]
    signum t = Cons "Signum" [t]
    fromInteger = NumberLiteral . fromIntegral
  
  instance Arbitrary TermPattern where
    arbitrary = do
      h <- Q.choose (0,7)
      w <- Q.choose (0,4)
      arbitraryTermPattern h w Q.arbitrary
  
  arbitraryTermPattern :: Int -> Int -> Gen TermVar -> Gen TermPattern
  arbitraryTermPattern h w var
    | h == 0 =
        Q.oneof
          [ Cons <$> Q.arbitrary <*> pure []
          , StringLiteral <$> arbitraryLetter
          , NumberLiteral <$> Q.choose (0,9)
          , Var <$> var
          ]
    | otherwise = do
        w' <- Q.choose (0,w)
        Q.oneof
          [ do
            c <- Q.arbitrary
            fmap (Cons c) $ Q.vectorOf w' $ do
              h' <- Q.choose (0,h-1)
              arbitraryTermPattern h' w var
          -- , Explode <$> arbitraryStringPattern
          --           <*> arbitraryListPattern w'
          ]
  
    -- where
    --   arbitraryStringPattern :: Gen TermPattern
    --   arbitraryStringPattern =
    --     oneof
    --       [ Var <$> var
    --       , StringLiteral <$> arbitraryLetter
    --       ]
  
    --   arbitraryListPattern :: Int -> Gen TermPattern
    --   arbitraryListPattern len =
    --     if len == 0
    --       then return $ Cons "Nil" []
    --       else do
    --         h' <- choose (0,h-1)
    --         tp <- arbitraryTermPattern h' w var
    --         tl <- arbitraryListPattern (len-1)
    --         return $ Cons "Cons" [tp,tl]
  
  class TermVars s where
    termVars :: (IsList (f TermVar), Item (f TermVar) ~ TermVar, Monoid (f TermVar)) => s -> f TermVar
  
  instance TermVars Module where
    termVars (Module _ strats) = termVars strats
  
  instance (TermVars x,TermVars y) => TermVars (HashMap x y) where
    termVars = termVars . M.toList
  
  -- instance TermVars env => TermVars (Closure Strategy env) where
  --   termVars (Closure s env) = termVars s <> termVars env
  
  instance TermVars Strat where
    termVars s = case s of
      Fail _ -> mempty
      Id _ -> mempty
      Seq s1 s2 _ -> termVars s1 <> termVars s2
      GuardedChoice s1 s2 s3 _ -> termVars s1 <> termVars s2 <> termVars s3
      One s1 _ -> termVars s1
      Some s1 _ -> termVars s1
      All s1 _ -> termVars s1
      Match p _ -> termVars p
      Build p _ -> termVars p
      Scope vs s1 _ -> termVars vs <> termVars s1
      Let strats s1 _ -> termVars strats <> termVars s1
      Call _ _ vs _ -> termVars vs
      Prim _ _ vs _ -> termVars vs
      Apply _ body _ -> termVars body
  
  instance TermVars StratVar where
    termVars _ = mempty
  
  instance TermVars Strategy where
    termVars strat = termVars (strategyTermArguments strat) <> termVars (strategyBody strat)
  
  instance TermVars TermPattern where
    termVars t = case t of
      As v p -> termVars v <> termVars p
      Cons _ ts -> termVars ts
      Explode f l -> termVars f <> termVars l
      Var x -> termVars x
      _ -> mempty
  
  instance TermVars x => TermVars [x] where
    termVars l = mconcat $ termVars <$> l
  
  instance (TermVars x, TermVars y) => TermVars (x,y) where
    termVars (x,y) = termVars x <> termVars y
  
  instance TermVars TermVar where
    termVars "_" = mempty
    termVars x = fromList [x]
  
  stratCall :: Prism' (tenv,(senv,(Strat,term))) ((Strat,senv),(term,tenv))
  stratCall = L.prism' (\((strat,senv),(term,tenv)) -> (tenv,(senv,(strat,term))))
                  (\(tenv,(senv,(strat,term))) -> case strat of
                     Call {} -> Just ((strat,senv),(term,tenv))
                     _ -> Nothing)
  {-# INLINE stratCall #-}
  
  stratApply :: Prism' (tenv,(senv,(Strat,term))) ((Strat, senv),(term,tenv))
  stratApply = L.prism' (\((strat,senv),(term,tenv)) -> (tenv,(senv,(strat,term))))
                  (\(tenv,(senv,(strat,term))) -> case strat of
                     Apply {} -> Just ((strat,senv),(term,tenv))
                     _ -> Nothing)
  {-# INLINE stratApply #-}
  