-- | 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
v309 -> (Term -> Term
fullyStripTerm (AnnotatedTerm -> Term
Core.annotatedTermSubject AnnotatedTerm
v309))
  Core.TermTyped TypedTerm
v310 -> (Term -> Term
fullyStripTerm (TypedTerm -> Term
Core.typedTermTerm TypedTerm
v310))
  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
v311 -> (Term -> Term
stripTerm (AnnotatedTerm -> Term
Core.annotatedTermSubject AnnotatedTerm
v311))
  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
v312 -> (Type -> Type
stripType (AnnotatedType -> Type
Core.annotatedTypeSubject AnnotatedType
v312))
  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
v313 -> (Type -> Type
stripTypeParameters (LambdaType -> Type
Core.lambdaTypeBody LambdaType
v313))
  Type
_ -> Type
t) (Type -> Type
stripType Type
t))