-- | Several functions for stripping annotations from types and terms.

module Hydra.Strip where

import qualified Hydra.Core as Core
import Data.Int
import Data.List as L
import Data.Map as M
import Data.Set as S

-- | Strip all annotations from a term, including first-class type annotations
fullyStripTerm :: (Core.Term -> Core.Term)
fullyStripTerm :: Term -> Term
fullyStripTerm Term
t = ((\Term
x -> case Term
x of
  Core.TermAnnotated AnnotatedTerm
v266 -> (Term -> Term
fullyStripTerm (AnnotatedTerm -> Term
Core.annotatedTermSubject AnnotatedTerm
v266))
  Core.TermTyped TypedTerm
v267 -> (Term -> Term
fullyStripTerm (TypedTerm -> Term
Core.typedTermTerm TypedTerm
v267))
  Term
_ -> Term
t) Term
t)

-- | Strip all annotations from a term
stripTerm :: (Core.Term -> Core.Term)
stripTerm :: Term -> Term
stripTerm Term
t = ((\Term
x -> case Term
x of
  Core.TermAnnotated AnnotatedTerm
v268 -> (Term -> Term
stripTerm (AnnotatedTerm -> Term
Core.annotatedTermSubject AnnotatedTerm
v268))
  Term
_ -> Term
t) Term
t)

-- | Strip all annotations from a term
stripType :: (Core.Type -> Core.Type)
stripType :: Type -> Type
stripType Type
t = ((\Type
x -> case Type
x of
  Core.TypeAnnotated AnnotatedType
v269 -> (Type -> Type
stripType (AnnotatedType -> Type
Core.annotatedTypeSubject AnnotatedType
v269))
  Type
_ -> Type
t) Type
t)

-- | Strip any top-level type lambdas from a type, extracting the (possibly nested) type body
stripTypeParameters :: (Core.Type -> Core.Type)
stripTypeParameters :: Type -> Type
stripTypeParameters Type
t = ((\Type
x -> case Type
x of
  Core.TypeLambda LambdaType
v270 -> (Type -> Type
stripTypeParameters (LambdaType -> Type
Core.lambdaTypeBody LambdaType
v270))
  Type
_ -> Type
t) (Type -> Type
stripType Type
t))