module Hydra.Sources.Tier1.Strip where

-- Standard Tier-1 imports
import           Prelude hiding ((++))
import qualified Data.List                 as L
import qualified Data.Map                  as M
import qualified Data.Set                  as S
import qualified Data.Maybe                as Y
import           Hydra.Dsl.Base            as Base
import qualified Hydra.Dsl.Core            as Core
import qualified Hydra.Dsl.Graph           as Graph
import qualified Hydra.Dsl.Lib.Equality    as Equality
import qualified Hydra.Dsl.Lib.Flows       as Flows
import qualified Hydra.Dsl.Lib.Io          as Io
import qualified Hydra.Dsl.Lib.Lists       as Lists
import qualified Hydra.Dsl.Lib.Literals    as Literals
import qualified Hydra.Dsl.Lib.Logic       as Logic
import qualified Hydra.Dsl.Lib.Maps        as Maps
import qualified Hydra.Dsl.Lib.Math        as Math
import qualified Hydra.Dsl.Lib.Optionals   as Optionals
import qualified Hydra.Dsl.Lib.Sets        as Sets
import           Hydra.Dsl.Lib.Strings     as Strings
import qualified Hydra.Dsl.Module          as Module
import qualified Hydra.Dsl.Terms           as Terms
import qualified Hydra.Dsl.Types           as Types
import           Hydra.Sources.Tier0.All


stripDefinition :: String -> Datum a -> Definition a
stripDefinition :: forall a. String -> Datum a -> Definition a
stripDefinition = Module -> String -> Datum a -> Definition a
forall a. Module -> String -> Datum a -> Definition a
definitionInModule Module
hydraStripModule

hydraStripModule :: Module
hydraStripModule :: Module
hydraStripModule = Namespace
-> [Element] -> [Module] -> [Module] -> Maybe String -> Module
Module (String -> Namespace
Namespace String
"hydra/strip") [Element]
elements [] [Module]
tier0Modules (Maybe String -> Module) -> Maybe String -> Module
forall a b. (a -> b) -> a -> b
$
    String -> Maybe String
forall a. a -> Maybe a
Just String
"Several functions for stripping annotations from types and terms."
  where
   elements :: [Element]
elements = [
     Definition (Term -> Term) -> Element
forall a. Definition a -> Element
el Definition (Term -> Term)
fullyStripTermDef,
     Definition (Term -> Term) -> Element
forall a. Definition a -> Element
el Definition (Term -> Term)
stripTermDef,
     Definition (Type -> Type) -> Element
forall a. Definition a -> Element
el Definition (Type -> Type)
stripTypeDef,
     Definition (Type -> Type) -> Element
forall a. Definition a -> Element
el Definition (Type -> Type)
stripTypeParametersDef]

fullyStripTermDef :: Definition (Term -> Term)
fullyStripTermDef :: Definition (Term -> Term)
fullyStripTermDef = String -> Datum (Term -> Term) -> Definition (Term -> Term)
forall a. String -> Datum a -> Definition a
stripDefinition String
"fullyStripTerm" (Datum (Term -> Term) -> Definition (Term -> Term))
-> Datum (Term -> Term) -> Definition (Term -> Term)
forall a b. (a -> b) -> a -> b
$
    String -> Datum (Term -> Term) -> Datum (Term -> Term)
forall a. String -> Datum a -> Datum a
doc String
"Strip all annotations from a term, including first-class type annotations" (Datum (Term -> Term) -> Datum (Term -> Term))
-> Datum (Term -> Term) -> Datum (Term -> Term)
forall a b. (a -> b) -> a -> b
$
    Type -> Type -> Datum (Term -> Term) -> Datum (Term -> Term)
forall a. Type -> Type -> Datum a -> Datum a
function Type
termT Type
termT (Datum (Term -> Term) -> Datum (Term -> Term))
-> Datum (Term -> Term) -> Datum (Term -> Term)
forall a b. (a -> b) -> a -> b
$
      String -> Datum Any -> Datum (Term -> Term)
forall x a b. String -> Datum x -> Datum (a -> b)
lambda String
"t" (Name -> Maybe (Datum Any) -> [Field] -> Datum (Any -> Any)
forall b u. Name -> Maybe (Datum b) -> [Field] -> Datum (u -> b)
match Name
_Term (Datum Any -> Maybe (Datum Any)
forall a. a -> Maybe a
Just (Datum Any -> Maybe (Datum Any)) -> Datum Any -> Maybe (Datum Any)
forall a b. (a -> b) -> a -> b
$ String -> Datum Any
forall a. String -> Datum a
var String
"t") [
        Name -> Case Any
forall a. Name -> Case a
Case Name
_Term_annotated Case Any -> Datum (Any -> Term) -> Field
forall a b. Case a -> Datum (a -> b) -> Field
--> Definition (Term -> Term) -> Datum (Term -> Term)
forall a. Definition a -> Datum a
ref Definition (Term -> Term)
fullyStripTermDef Datum (Term -> Term) -> Datum (Any -> Term) -> Datum (Any -> Term)
forall b c a. Datum (b -> c) -> Datum (a -> b) -> Datum (a -> c)
<.> (Name -> Name -> Datum (Any -> Term)
forall a b. Name -> Name -> Datum (a -> b)
project Name
_AnnotatedTerm Name
_AnnotatedTerm_subject),
        Name -> Case Any
forall a. Name -> Case a
Case Name
_Term_typed Case Any -> Datum (Any -> Term) -> Field
forall a b. Case a -> Datum (a -> b) -> Field
--> Definition (Term -> Term) -> Datum (Term -> Term)
forall a. Definition a -> Datum a
ref Definition (Term -> Term)
fullyStripTermDef Datum (Term -> Term) -> Datum (Any -> Term) -> Datum (Any -> Term)
forall b c a. Datum (b -> c) -> Datum (a -> b) -> Datum (a -> c)
<.> (Name -> Name -> Datum (Any -> Term)
forall a b. Name -> Name -> Datum (a -> b)
project Name
_TypedTerm Name
_TypedTerm_term)
        ] Datum (Any -> Any) -> Datum Any -> Datum Any
forall a b. Datum (a -> b) -> Datum a -> Datum b
@@ (String -> Datum Any
forall a. String -> Datum a
var String
"t"))

stripTermDef :: Definition (Term -> Term)
stripTermDef :: Definition (Term -> Term)
stripTermDef = String -> Datum (Term -> Term) -> Definition (Term -> Term)
forall a. String -> Datum a -> Definition a
stripDefinition String
"stripTerm" (Datum (Term -> Term) -> Definition (Term -> Term))
-> Datum (Term -> Term) -> Definition (Term -> Term)
forall a b. (a -> b) -> a -> b
$
    String -> Datum (Term -> Term) -> Datum (Term -> Term)
forall a. String -> Datum a -> Datum a
doc String
"Strip all annotations from a term" (Datum (Term -> Term) -> Datum (Term -> Term))
-> Datum (Term -> Term) -> Datum (Term -> Term)
forall a b. (a -> b) -> a -> b
$
    Type -> Type -> Datum (Term -> Term) -> Datum (Term -> Term)
forall a. Type -> Type -> Datum a -> Datum a
function Type
termT Type
termT (Datum (Term -> Term) -> Datum (Term -> Term))
-> Datum (Term -> Term) -> Datum (Term -> Term)
forall a b. (a -> b) -> a -> b
$
      String -> Datum Any -> Datum (Term -> Term)
forall x a b. String -> Datum x -> Datum (a -> b)
lambda String
"t" (Name -> Maybe (Datum Any) -> [Field] -> Datum (Any -> Any)
forall b u. Name -> Maybe (Datum b) -> [Field] -> Datum (u -> b)
match Name
_Term (Datum Any -> Maybe (Datum Any)
forall a. a -> Maybe a
Just (Datum Any -> Maybe (Datum Any)) -> Datum Any -> Maybe (Datum Any)
forall a b. (a -> b) -> a -> b
$ String -> Datum Any
forall a. String -> Datum a
var String
"t") [
        Name -> Case Any
forall a. Name -> Case a
Case Name
_Term_annotated Case Any -> Datum (Any -> Term) -> Field
forall a b. Case a -> Datum (a -> b) -> Field
--> Definition (Term -> Term) -> Datum (Term -> Term)
forall a. Definition a -> Datum a
ref Definition (Term -> Term)
stripTermDef Datum (Term -> Term) -> Datum (Any -> Term) -> Datum (Any -> Term)
forall b c a. Datum (b -> c) -> Datum (a -> b) -> Datum (a -> c)
<.> (Name -> Name -> Datum (Any -> Term)
forall a b. Name -> Name -> Datum (a -> b)
project Name
_AnnotatedTerm Name
_AnnotatedTerm_subject)
        ] Datum (Any -> Any) -> Datum Any -> Datum Any
forall a b. Datum (a -> b) -> Datum a -> Datum b
@@ (String -> Datum Any
forall a. String -> Datum a
var String
"t"))

stripTypeDef :: Definition (Type -> Type)
stripTypeDef :: Definition (Type -> Type)
stripTypeDef = String -> Datum (Type -> Type) -> Definition (Type -> Type)
forall a. String -> Datum a -> Definition a
stripDefinition String
"stripType" (Datum (Type -> Type) -> Definition (Type -> Type))
-> Datum (Type -> Type) -> Definition (Type -> Type)
forall a b. (a -> b) -> a -> b
$
    String -> Datum (Type -> Type) -> Datum (Type -> Type)
forall a. String -> Datum a -> Datum a
doc String
"Strip all annotations from a term" (Datum (Type -> Type) -> Datum (Type -> Type))
-> Datum (Type -> Type) -> Datum (Type -> Type)
forall a b. (a -> b) -> a -> b
$
    Type -> Type -> Datum (Type -> Type) -> Datum (Type -> Type)
forall a. Type -> Type -> Datum a -> Datum a
function Type
typeT Type
typeT (Datum (Type -> Type) -> Datum (Type -> Type))
-> Datum (Type -> Type) -> Datum (Type -> Type)
forall a b. (a -> b) -> a -> b
$
      String -> Datum Any -> Datum (Type -> Type)
forall x a b. String -> Datum x -> Datum (a -> b)
lambda String
"t" (Name -> Maybe (Datum Any) -> [Field] -> Datum (Any -> Any)
forall b u. Name -> Maybe (Datum b) -> [Field] -> Datum (u -> b)
match Name
_Type (Datum Any -> Maybe (Datum Any)
forall a. a -> Maybe a
Just (Datum Any -> Maybe (Datum Any)) -> Datum Any -> Maybe (Datum Any)
forall a b. (a -> b) -> a -> b
$ String -> Datum Any
forall a. String -> Datum a
var String
"t") [
        Name -> Case Any
forall a. Name -> Case a
Case Name
_Type_annotated Case Any -> Datum (Any -> Type) -> Field
forall a b. Case a -> Datum (a -> b) -> Field
--> Definition (Type -> Type) -> Datum (Type -> Type)
forall a. Definition a -> Datum a
ref Definition (Type -> Type)
stripTypeDef Datum (Type -> Type) -> Datum (Any -> Type) -> Datum (Any -> Type)
forall b c a. Datum (b -> c) -> Datum (a -> b) -> Datum (a -> c)
<.> (Name -> Name -> Datum (Any -> Type)
forall a b. Name -> Name -> Datum (a -> b)
project Name
_AnnotatedType Name
_AnnotatedType_subject)
        ] Datum (Any -> Any) -> Datum Any -> Datum Any
forall a b. Datum (a -> b) -> Datum a -> Datum b
@@ (String -> Datum Any
forall a. String -> Datum a
var String
"t"))

stripTypeParametersDef :: Definition (Type -> Type)
stripTypeParametersDef :: Definition (Type -> Type)
stripTypeParametersDef = String -> Datum (Type -> Type) -> Definition (Type -> Type)
forall a. String -> Datum a -> Definition a
stripDefinition String
"stripTypeParameters" (Datum (Type -> Type) -> Definition (Type -> Type))
-> Datum (Type -> Type) -> Definition (Type -> Type)
forall a b. (a -> b) -> a -> b
$
    String -> Datum (Type -> Type) -> Datum (Type -> Type)
forall a. String -> Datum a -> Datum a
doc String
"Strip any top-level type lambdas from a type, extracting the (possibly nested) type body" (Datum (Type -> Type) -> Datum (Type -> Type))
-> Datum (Type -> Type) -> Datum (Type -> Type)
forall a b. (a -> b) -> a -> b
$
    Type -> Type -> Datum (Type -> Type) -> Datum (Type -> Type)
forall a. Type -> Type -> Datum a -> Datum a
function Type
typeT Type
typeT (Datum (Type -> Type) -> Datum (Type -> Type))
-> Datum (Type -> Type) -> Datum (Type -> Type)
forall a b. (a -> b) -> a -> b
$
      String -> Datum Any -> Datum (Type -> Type)
forall x a b. String -> Datum x -> Datum (a -> b)
lambda String
"t" (Datum Any -> Datum (Type -> Type))
-> Datum Any -> Datum (Type -> Type)
forall a b. (a -> b) -> a -> b
$ Name -> Maybe (Datum Any) -> [Field] -> Datum (Type -> Any)
forall b u. Name -> Maybe (Datum b) -> [Field] -> Datum (u -> b)
match Name
_Type (Datum Any -> Maybe (Datum Any)
forall a. a -> Maybe a
Just (Datum Any -> Maybe (Datum Any)) -> Datum Any -> Maybe (Datum Any)
forall a b. (a -> b) -> a -> b
$ String -> Datum Any
forall a. String -> Datum a
var String
"t") [
        Name -> Case Any
forall a. Name -> Case a
Case Name
_Type_lambda Case Any -> Datum (Any -> Any) -> Field
forall a b. Case a -> Datum (a -> b) -> Field
--> String -> Datum Type -> Datum (Any -> Any)
forall x a b. String -> Datum x -> Datum (a -> b)
lambda String
"lt" (Definition (Type -> Type) -> Datum (Type -> Type)
forall a. Definition a -> Datum a
ref Definition (Type -> Type)
stripTypeParametersDef Datum (Type -> Type) -> Datum Type -> Datum Type
forall a b. Datum (a -> b) -> Datum a -> Datum b
@@ (Name -> Name -> Datum (Any -> Type)
forall a b. Name -> Name -> Datum (a -> b)
project Name
_LambdaType Name
_LambdaType_body Datum (Any -> Type) -> Datum Any -> Datum Type
forall a b. Datum (a -> b) -> Datum a -> Datum b
@@ String -> Datum Any
forall a. String -> Datum a
var String
"lt"))
        ] Datum (Type -> Any) -> Datum Type -> Datum Any
forall a b. Datum (a -> b) -> Datum a -> Datum b
@@ (Definition (Type -> Type) -> Datum (Type -> Type)
forall a. Definition a -> Datum a
ref Definition (Type -> Type)
stripTypeDef Datum (Type -> Type) -> Datum Type -> Datum Type
forall a b. Datum (a -> b) -> Datum a -> Datum b
@@ String -> Datum Type
forall a. String -> Datum a
var String
"t")