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 -> TTerm a -> TElement a
stripDefinition :: forall a. String -> TTerm a -> TElement a
stripDefinition = Module -> String -> TTerm a -> TElement a
forall a. Module -> String -> TTerm a -> TElement 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 = [
     TElement (Term -> Term) -> Element
forall a. TElement a -> Element
el TElement (Term -> Term)
fullyStripTermDef,
     TElement (Term -> Term) -> Element
forall a. TElement a -> Element
el TElement (Term -> Term)
stripTermDef,
     TElement (Type -> Type) -> Element
forall a. TElement a -> Element
el TElement (Type -> Type)
stripTypeDef,
     TElement (Type -> Type) -> Element
forall a. TElement a -> Element
el TElement (Type -> Type)
stripTypeParametersDef]

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

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

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

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