module Hydra.Impl.Haskell.Dsl.Base (
  module Hydra.Impl.Haskell.Dsl.Base,
  module Hydra.Impl.Haskell.Dsl.PhantomLiterals,
  Standard.coreContext,
) where

import Hydra.All
import Hydra.Meta
import Hydra.CoreEncoding
import Hydra.Impl.Haskell.Dsl.PhantomLiterals
import qualified Hydra.Impl.Haskell.Dsl.Standard as Standard
import qualified Hydra.Impl.Haskell.Dsl.Terms as Terms
import qualified Hydra.Impl.Haskell.Dsl.Types as Types
import Hydra.Impl.Haskell.Sources.Core
import Hydra.Types.Inference
import qualified Hydra.Impl.Haskell.Dsl.Lib.Strings as Strings

import Prelude hiding ((++))

import qualified Data.Map as M
import qualified Data.Set as S


el :: Definition a -> Element Meta
el :: forall a. Definition a -> Element Meta
el (Definition Name
name (Datum Term Meta
term)) = forall m. Name -> Term m -> Term m -> Element m
Element Name
name (forall m. Type m -> Term m
encodeType forall {m}. Type m
dummyType) Term Meta
term
  where
    dummyType :: Type m
dummyType = forall m. RowType m -> Type m
TypeRecord (forall m. Name -> Maybe Name -> [FieldType m] -> RowType m
RowType (String -> Name
Name String
"PreInferencePlaceholder") forall a. Maybe a
Nothing [])

infixr 0 >:
(>:) :: String -> Datum a -> Fld a
String
n >: :: forall a. String -> Datum a -> Fld a
>: Datum a
d = forall a. Field Meta -> Fld a
Fld forall a b. (a -> b) -> a -> b
$ forall m. FieldName -> Term m -> Field m
Field (String -> FieldName
FieldName String
n) (forall a. Datum a -> Term Meta
unDatum Datum a
d)

(<.>) :: Datum (b -> c) -> Datum (a -> b) -> Datum (a -> c)
Datum (b -> c)
f <.> :: forall b c a. Datum (b -> c) -> Datum (a -> b) -> Datum (a -> c)
<.> Datum (a -> b)
g = forall b c a. Datum (b -> c) -> Datum (a -> b) -> Datum (a -> c)
compose Datum (b -> c)
f Datum (a -> b)
g

($$) :: Datum (a -> b) -> Datum a -> Datum b
Datum (a -> b)
f $$ :: forall a b. Datum (a -> b) -> Datum a -> Datum b
$$ Datum a
x = forall a b. Datum (a -> b) -> Datum a -> Datum b
apply Datum (a -> b)
f Datum a
x

(@@) :: Datum (a -> b) -> Datum a -> Datum b
Datum (a -> b)
f @@ :: forall a b. Datum (a -> b) -> Datum a -> Datum b
@@ Datum a
x = forall a b. Datum (a -> b) -> Datum a -> Datum b
apply Datum (a -> b)
f Datum a
x

infixr 0 @->
(@->) :: a -> b -> (a, b)
a
x @-> :: forall a b. a -> b -> (a, b)
@-> b
y = (a
x, b
y)

infixr 0 -->
(-->) :: Case a -> Datum (a -> b) -> Field Meta
Case a
c --> :: forall a b. Case a -> Datum (a -> b) -> Field Meta
--> Datum (a -> b)
t = forall a b. Case a -> Datum (a -> b) -> Field Meta
caseField Case a
c Datum (a -> b)
t

(++) :: Datum String -> Datum String -> Datum String
Datum String
l ++ :: Datum String -> Datum String -> Datum String
++ Datum String
r = Datum ([String] -> String)
Strings.cat forall a b. Datum (a -> b) -> Datum a -> Datum b
@@ forall a. [Datum a] -> Datum [a]
list [Datum String
l, Datum String
r]

apply :: Datum (a -> b) -> Datum a -> Datum b
apply :: forall a b. Datum (a -> b) -> Datum a -> Datum b
apply (Datum Term Meta
lhs) (Datum Term Meta
rhs) = forall a. Term Meta -> Datum a
Datum forall a b. (a -> b) -> a -> b
$ forall m. Term m -> Term m -> Term m
Terms.apply Term Meta
lhs Term Meta
rhs

apply2 :: Datum (a -> b -> c) -> Datum a -> Datum b -> Datum c
apply2 :: forall a b c. Datum (a -> b -> c) -> Datum a -> Datum b -> Datum c
apply2 (Datum Term Meta
f) (Datum Term Meta
a1) (Datum Term Meta
a2) = forall a. Term Meta -> Datum a
Datum forall a b. (a -> b) -> a -> b
$ forall m. Term m -> Term m -> Term m
Terms.apply (forall m. Term m -> Term m -> Term m
Terms.apply Term Meta
f Term Meta
a1) Term Meta
a2

caseField :: Case a -> Datum (a -> b) -> Field Meta
caseField :: forall a b. Case a -> Datum (a -> b) -> Field Meta
caseField (Case FieldName
fname) (Datum Term Meta
f) = forall m. FieldName -> Term m -> Field m
Field FieldName
fname Term Meta
f

compareTo :: Datum a -> Datum (a -> Bool)
compareTo :: forall a. Datum a -> Datum (a -> Bool)
compareTo (Datum Term Meta
term) = forall a. Term Meta -> Datum a
Datum forall a b. (a -> b) -> a -> b
$ forall m. Term m -> Term m
Terms.compareTo Term Meta
term

compose :: Datum (b -> c) -> Datum (a -> b) -> Datum (a -> c)
compose :: forall b c a. Datum (b -> c) -> Datum (a -> b) -> Datum (a -> c)
compose (Datum Term Meta
f) (Datum Term Meta
g) = forall a. Term Meta -> Datum a
Datum forall a b. (a -> b) -> a -> b
$ forall m. String -> Term m -> Term m
Terms.lambda String
"x1" forall a b. (a -> b) -> a -> b
$ forall m. Term m -> Term m -> Term m
Terms.apply Term Meta
f (forall m. Term m -> Term m -> Term m
Terms.apply Term Meta
g forall a b. (a -> b) -> a -> b
$ forall m. String -> Term m
Terms.variable String
"x1")

constant :: Datum a -> Datum (b -> a)
constant :: forall a b. Datum a -> Datum (b -> a)
constant (Datum Term Meta
term) = forall a. Term Meta -> Datum a
Datum forall a b. (a -> b) -> a -> b
$ forall m. String -> Term m -> Term m
Terms.lambda String
"_" Term Meta
term

denom :: Name -> Datum (a -> b)
denom :: forall a b. Name -> Datum (a -> b)
denom = forall a. Term Meta -> Datum a
Datum forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall m. Name -> Term m
Terms.eliminateNominal

delta :: Datum (Reference a -> a)
delta :: forall a. Datum (Reference a -> a)
delta = forall a. Term Meta -> Datum a
Datum forall m. Term m
Terms.delta

doc :: String -> Datum a -> Datum a
doc :: forall a. String -> Datum a -> Datum a
doc String
s (Datum Term Meta
term) = forall a. Term Meta -> Datum a
Datum forall a b. (a -> b) -> a -> b
$ Context Meta -> Maybe String -> Term Meta -> Term Meta
setTermDescription Context Meta
Standard.coreContext (forall a. a -> Maybe a
Just String
s) Term Meta
term

element :: Definition a -> Datum (Reference a)
element :: forall a. Definition a -> Datum (Reference a)
element (Definition Name
name Datum a
_) = forall a. Term Meta -> Datum a
Datum forall a b. (a -> b) -> a -> b
$ forall m. Name -> Term m
Terms.element Name
name

field :: FieldName -> Datum a -> Field Meta
field :: forall a. FieldName -> Datum a -> Field Meta
field FieldName
fname (Datum Term Meta
val) = forall m. FieldName -> Term m -> Field m
Field FieldName
fname Term Meta
val

function :: Type Meta -> Type Meta -> Datum a -> Datum a
function :: forall a. Type Meta -> Type Meta -> Datum a -> Datum a
function Type Meta
dom Type Meta
cod = forall a. Type Meta -> Datum a -> Datum a
typed (forall m. Type m -> Type m -> Type m
Types.function Type Meta
dom Type Meta
cod)

functionN :: [Type Meta] -> Type Meta -> Datum a -> Datum a
functionN :: forall a. [Type Meta] -> Type Meta -> Datum a -> Datum a
functionN [Type Meta]
doms Type Meta
cod = forall a. Type Meta -> Datum a -> Datum a
typed forall a b. (a -> b) -> a -> b
$ forall m. [Type m] -> Type m -> Type m
Types.functionN [Type Meta]
doms Type Meta
cod

lambda :: String -> Datum x -> Datum (a -> b)
lambda :: forall x a b. String -> Datum x -> Datum (a -> b)
lambda String
v (Datum Term Meta
body) = forall a. Term Meta -> Datum a
Datum forall a b. (a -> b) -> a -> b
$ forall m. String -> Term m -> Term m
Terms.lambda String
v Term Meta
body

--letTerm :: Var a -> Datum a -> Datum b -> Datum b
--letTerm (Var k) (Datum v) (Datum env) = Datum $ Terms.letTerm (Variable k) v env

list :: [Datum a] -> Datum [a]
list :: forall a. [Datum a] -> Datum [a]
list [Datum a]
els = forall a. Term Meta -> Datum a
Datum forall a b. (a -> b) -> a -> b
$ forall m. [Term m] -> Term m
Terms.list (forall a. Datum a -> Term Meta
unDatum forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Datum a]
els)

map :: M.Map (Datum a) (Datum b) -> Datum (M.Map a b)
map :: forall a b. Map (Datum a) (Datum b) -> Datum (Map a b)
map = forall a. Term Meta -> Datum a
Datum forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall m. Map (Term m) (Term m) -> Term m
Terms.map forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a. Ord k => [(k, a)] -> Map k a
M.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall {a} {a}. (Datum a, Datum a) -> (Term Meta, Term Meta)
fromDatum forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a. Map k a -> [(k, a)]
M.toList
  where
    fromDatum :: (Datum a, Datum a) -> (Term Meta, Term Meta)
fromDatum (Datum Term Meta
k, Datum Term Meta
v) = (Term Meta
k, Term Meta
v)

matchData :: Name -> [(FieldName, Datum (x -> b))] -> Datum (a -> b)
matchData :: forall x b a.
Name -> [(FieldName, Datum (x -> b))] -> Datum (a -> b)
matchData Name
name [(FieldName, Datum (x -> b))]
pairs = forall a. Term Meta -> Datum a
Datum forall a b. (a -> b) -> a -> b
$ forall m. Name -> [Field m] -> Term m
Terms.cases Name
name (forall {a}. (FieldName, Datum a) -> Field Meta
toField forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(FieldName, Datum (x -> b))]
pairs)
  where
    toField :: (FieldName, Datum a) -> Field Meta
toField (FieldName
fname, Datum Term Meta
term) = forall m. FieldName -> Term m -> Field m
Field FieldName
fname Term Meta
term

matchOpt :: Datum b -> Datum (a -> b) -> Datum (Maybe a -> b)
matchOpt :: forall b a. Datum b -> Datum (a -> b) -> Datum (Maybe a -> b)
matchOpt (Datum Term Meta
n) (Datum Term Meta
j) = forall a. Term Meta -> Datum a
Datum forall a b. (a -> b) -> a -> b
$ forall m. Term m -> Term m -> Term m
Terms.matchOptional Term Meta
n Term Meta
j

match :: Name -> Type Meta -> [Field Meta] -> Datum (u -> b)
match :: forall u b. Name -> Type Meta -> [Field Meta] -> Datum (u -> b)
match Name
name Type Meta
cod [Field Meta]
fields = forall a. Type Meta -> Type Meta -> Datum a -> Datum a
function (forall m. Name -> Type m
Types.nominal Name
name) Type Meta
cod forall a b. (a -> b) -> a -> b
$ forall a. Term Meta -> Datum a
Datum forall a b. (a -> b) -> a -> b
$ forall m. Name -> [Field m] -> Term m
Terms.cases Name
name [Field Meta]
fields

matchToEnum :: Name -> Name -> [(FieldName, FieldName)] -> Datum (a -> b)
matchToEnum :: forall a b.
Name -> Name -> [(FieldName, FieldName)] -> Datum (a -> b)
matchToEnum Name
domName Name
codName [(FieldName, FieldName)]
pairs = forall x b a.
Name -> [(FieldName, Datum (x -> b))] -> Datum (a -> b)
matchData Name
domName (forall {a} {b} {a}. (a, FieldName) -> (a, Datum (b -> a))
toCase forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(FieldName, FieldName)]
pairs)
  where
    toCase :: (a, FieldName) -> (a, Datum (b -> a))
toCase (a
fromName, FieldName
toName) = (a
fromName, forall a b. Datum a -> Datum (b -> a)
constant forall a b. (a -> b) -> a -> b
$ forall a. Name -> FieldName -> Datum a
unitVariant Name
codName FieldName
toName)

matchToUnion :: Name -> Name -> [(FieldName, Field Meta)] -> Datum (a -> b)
matchToUnion :: forall a b.
Name -> Name -> [(FieldName, Field Meta)] -> Datum (a -> b)
matchToUnion Name
domName Name
codName [(FieldName, Field Meta)]
pairs = forall x b a.
Name -> [(FieldName, Datum (x -> b))] -> Datum (a -> b)
matchData Name
domName (forall {a} {b} {a}. (a, Field Meta) -> (a, Datum (b -> a))
toCase forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(FieldName, Field Meta)]
pairs)
  where
    toCase :: (a, Field Meta) -> (a, Datum (b -> a))
toCase (a
fromName, Field Meta
fld) = (a
fromName, forall a b. Datum a -> Datum (b -> a)
constant forall a b. (a -> b) -> a -> b
$ forall a. Term Meta -> Datum a
Datum forall a b. (a -> b) -> a -> b
$ forall m. Name -> Field m -> Term m
Terms.union Name
codName Field Meta
fld)

-- Note: the phantom types provide no guarantee of type safety in this case
nom :: Name -> Datum a -> Datum b
nom :: forall a b. Name -> Datum a -> Datum b
nom Name
name (Datum Term Meta
term) = forall a. Term Meta -> Datum a
Datum forall a b. (a -> b) -> a -> b
$ forall m. Name -> Term m -> Term m
Terms.nominal Name
name Term Meta
term

opt :: Maybe (Datum a) -> Datum (Maybe a)
opt :: forall a. Maybe (Datum a) -> Datum (Maybe a)
opt Maybe (Datum a)
mc = forall a. Term Meta -> Datum a
Datum forall a b. (a -> b) -> a -> b
$ forall m. Maybe (Term m) -> Term m
Terms.optional (forall a. Datum a -> Term Meta
unDatum forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (Datum a)
mc)

primitive :: Name -> Datum a
primitive :: forall a. Name -> Datum a
primitive = forall a. Term Meta -> Datum a
Datum forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall m. Name -> Term m
Terms.primitive

project :: Name -> Type Meta -> FieldName -> Datum (a -> b)
project :: forall a b. Name -> Type Meta -> FieldName -> Datum (a -> b)
project Name
name Type Meta
cod FieldName
fname = forall a. Term Meta -> Datum a
Datum forall a b. (a -> b) -> a -> b
$ forall m. Name -> FieldName -> Term m
Terms.projection Name
name FieldName
fname

record :: Name -> [Fld a] -> Datum a
record :: forall a. Name -> [Fld a] -> Datum a
record Name
name [Fld a]
fields = forall a. Term Meta -> Datum a
Datum forall a b. (a -> b) -> a -> b
$ forall m. Name -> [Field m] -> Term m
Terms.record Name
name (forall a. Fld a -> Field Meta
unFld forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Fld a]
fields)

ref :: Definition a -> Datum a
ref :: forall a. Definition a -> Datum a
ref (Definition Name
name Datum a
_) = forall a. Term Meta -> Datum a
Datum (forall m. Term m -> Term m -> Term m
Terms.apply forall m. Term m
Terms.delta forall a b. (a -> b) -> a -> b
$ forall m. Name -> Term m
Terms.element Name
name) 

set :: S.Set (Datum a) -> Datum (S.Set a)
set :: forall a. Set (Datum a) -> Datum (Set a)
set = forall a. Term Meta -> Datum a
Datum forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall m. Set (Term m) -> Term m
Terms.set forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Ord a => [a] -> Set a
S.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Datum a -> Term Meta
unDatum forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Set a -> [a]
S.toList

typed :: Type Meta -> Datum a -> Datum a
typed :: forall a. Type Meta -> Datum a -> Datum a
typed Type Meta
t (Datum Term Meta
term) = forall a. Term Meta -> Datum a
Datum forall a b. (a -> b) -> a -> b
$ Context Meta -> Maybe (Type Meta) -> Term Meta -> Term Meta
setTermType Context Meta
Standard.coreContext (forall a. a -> Maybe a
Just Type Meta
t) Term Meta
term

union :: Name -> FieldName -> Datum a -> Datum b
union :: forall a b. Name -> FieldName -> Datum a -> Datum b
union Name
name FieldName
fname (Datum Term Meta
term) = forall a. Term Meta -> Datum a
Datum forall a b. (a -> b) -> a -> b
$ forall m. Name -> Field m -> Term m
Terms.union Name
name (forall m. FieldName -> Term m -> Field m
Field FieldName
fname Term Meta
term)

union2 :: Name -> FieldName -> Datum (a -> b)
union2 :: forall a b. Name -> FieldName -> Datum (a -> b)
union2 Name
name FieldName
fname = forall x a b. String -> Datum x -> Datum (a -> b)
lambda String
"x2" forall a b. (a -> b) -> a -> b
$ forall a. Type Meta -> Datum a -> Datum a
typed (forall m. Name -> Type m
Types.nominal Name
name) forall a b. (a -> b) -> a -> b
$ forall a b. Name -> FieldName -> Datum a -> Datum b
union Name
name FieldName
fname forall a b. (a -> b) -> a -> b
$ forall a. String -> Datum a
var String
"x2"

unit :: Datum a
unit :: forall a. Datum a
unit = forall a. Term Meta -> Datum a
Datum forall m. Term m
Terms.unit

unitVariant :: Name -> FieldName -> Datum a
unitVariant :: forall a. Name -> FieldName -> Datum a
unitVariant Name
name FieldName
fname = forall a. Type Meta -> Datum a -> Datum a
typed (forall m. Name -> Type m
Types.nominal Name
name) forall a b. (a -> b) -> a -> b
$ forall a. Term Meta -> Datum a
Datum forall a b. (a -> b) -> a -> b
$ forall m. Name -> Field m -> Term m
Terms.union Name
name forall a b. (a -> b) -> a -> b
$ forall m. FieldName -> Term m -> Field m
Field FieldName
fname forall m. Term m
Terms.unit

var :: String -> Datum a
var :: forall a. String -> Datum a
var String
v = forall a. Term Meta -> Datum a
Datum forall a b. (a -> b) -> a -> b
$ forall m. String -> Term m
Terms.variable String
v

variant :: Name -> FieldName -> Datum a -> Datum b
variant :: forall a b. Name -> FieldName -> Datum a -> Datum b
variant Name
name FieldName
fname (Datum Term Meta
term) = forall a. Type Meta -> Datum a -> Datum a
typed (forall m. Name -> Type m
Types.nominal Name
name) forall a b. (a -> b) -> a -> b
$ forall a. Term Meta -> Datum a
Datum forall a b. (a -> b) -> a -> b
$ forall m. Name -> Field m -> Term m
Terms.union Name
name forall a b. (a -> b) -> a -> b
$ forall m. FieldName -> Term m -> Field m
Field FieldName
fname Term Meta
term