{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ImportQualifiedPost #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}

module Constrained.Core where

import Control.Applicative
import Data.Function
import Data.Set (Set)
import Data.Set qualified as Set
import Data.Typeable

import Constrained.List

-- Variables --------------------------------------------------------------

data Var a = Var {forall a. Var a -> Int
nameOf :: Int, forall a. Var a -> String
nameHint :: String}

instance Ord (Var a) where
  compare :: Var a -> Var a -> Ordering
compare = forall a. Ord a => a -> a -> Ordering
compare forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` forall a. Var a -> Int
nameOf

instance Eq (Var a) where
  == :: Var a -> Var a -> Bool
(==) = forall a. Eq a => a -> a -> Bool
(==) forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` forall a. Var a -> Int
nameOf

instance Show (Var a) where
  show :: Var a -> String
show Var a
v = forall a. Var a -> String
nameHint Var a
v forall a. [a] -> [a] -> [a]
++ String
"_" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a. Var a -> Int
nameOf Var a
v)

eqVar :: forall a a'. (Typeable a, Typeable a') => Var a -> Var a' -> Maybe (a :~: a')
eqVar :: forall a a'.
(Typeable a, Typeable a') =>
Var a -> Var a' -> Maybe (a :~: a')
eqVar Var a
v Var a'
v' | forall a. Var a -> Int
nameOf Var a
v forall a. Eq a => a -> a -> Bool
== forall a. Var a -> Int
nameOf Var a'
v' = forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT @a @a'
eqVar Var a
_ Var a'
_ = forall a. Maybe a
Nothing

-- Variable renaming ------------------------------------------------------

class Rename a where
  rename :: Typeable x => Var x -> Var x -> a -> a

instance Typeable a => Rename (Var a) where
  rename :: forall x. Typeable x => Var x -> Var x -> Var a -> Var a
rename Var x
v Var x
v' Var a
v''
    | Just x :~: a
Refl <- forall a a'.
(Typeable a, Typeable a') =>
Var a -> Var a' -> Maybe (a :~: a')
eqVar Var x
v Var a
v'' = Var x
v'
    | Bool
otherwise = Var a
v''

instance Rename () where
  rename :: forall x. Typeable x => Var x -> Var x -> () -> ()
rename Var x
_ Var x
_ ()
_ = ()

instance (Rename a, Rename b) => Rename (a, b) where
  rename :: forall x. Typeable x => Var x -> Var x -> (a, b) -> (a, b)
rename Var x
x Var x
x' (a
a, b
b) = (forall a x. (Rename a, Typeable x) => Var x -> Var x -> a -> a
rename Var x
x Var x
x' a
a, forall a x. (Rename a, Typeable x) => Var x -> Var x -> a -> a
rename Var x
x Var x
x' b
b)

instance {-# OVERLAPPABLE #-} (Functor t, Rename a) => Rename (t a) where
  rename :: forall x. Typeable x => Var x -> Var x -> t a -> t a
rename Var x
v Var x
v'
    | Var x
v forall a. Eq a => a -> a -> Bool
== Var x
v' = forall a. a -> a
id
    | Bool
otherwise = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a x. (Rename a, Typeable x) => Var x -> Var x -> a -> a
rename Var x
v Var x
v')

instance (Ord a, Rename a) => Rename (Set a) where
  rename :: forall x. Typeable x => Var x -> Var x -> Set a -> Set a
rename Var x
v Var x
v'
    | Var x
v forall a. Eq a => a -> a -> Bool
== Var x
v' = forall a. a -> a
id
    | Bool
otherwise = forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (forall a x. (Rename a, Typeable x) => Var x -> Var x -> a -> a
rename Var x
v Var x
v')

instance (forall a. Rename (f a)) => Rename (List f as) where
  rename :: forall x. Typeable x => Var x -> Var x -> List f as -> List f as
rename Var x
v Var x
v' = forall {k} (f :: k -> *) (g :: k -> *) (as :: [k]).
(forall (a :: k). f a -> g a) -> List f as -> List g as
mapList (forall a x. (Rename a, Typeable x) => Var x -> Var x -> a -> a
rename Var x
v Var x
v')

freshVar :: Var a -> Set Int -> Var a
freshVar :: forall a. Var a -> Set Int -> Var a
freshVar (Var Int
n String
nh) Set Int
ns
  | forall a. Ord a => a -> Set a -> Bool
Set.member Int
n Set Int
ns = forall a. Int -> String -> Var a
Var (Int
1 forall a. Num a => a -> a -> a
+ forall a. Set a -> a
Set.findMax Set Int
ns) String
nh
  | Bool
otherwise = forall a. Int -> String -> Var a
Var Int
n String
nh

freshen :: (Typeable a, Rename t) => Var a -> t -> Set Int -> (Var a, t)
freshen :: forall a t.
(Typeable a, Rename t) =>
Var a -> t -> Set Int -> (Var a, t)
freshen Var a
v t
t Set Int
nms
  | forall a. Var a -> Int
nameOf Var a
v forall a. Ord a => a -> Set a -> Bool
`Set.member` Set Int
nms = let v' :: Var a
v' = forall a. Var a -> Set Int -> Var a
freshVar Var a
v Set Int
nms in (Var a
v', forall a x. (Rename a, Typeable x) => Var x -> Var x -> a -> a
rename Var a
v Var a
v' t
t)
  | Bool
otherwise = (Var a
v, t
t)

-- Values -----------------------------------------------------------------

data Value a where
  Value :: Show a => !a -> Value a

deriving instance Eq a => Eq (Value a)
deriving instance Ord a => Ord (Value a)
instance Show (Value a) where
  showsPrec :: Int -> Value a -> ShowS
showsPrec Int
p (Value a
a) = forall a. Show a => Int -> a -> ShowS
showsPrec Int
p a
a

unValue :: Value a -> a
unValue :: forall a. Value a -> a
unValue (Value a
v) = a
v

-- Cruft ------------------------------------------------------------------

data Evidence c where
  Evidence :: c => Evidence c

unionWithMaybe :: (a -> a -> a) -> Maybe a -> Maybe a -> Maybe a
unionWithMaybe :: forall a. (a -> a -> a) -> Maybe a -> Maybe a -> Maybe a
unionWithMaybe a -> a -> a
f Maybe a
ma Maybe a
ma' = (a -> a -> a
f forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe a
ma forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Maybe a
ma') forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Maybe a
ma forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Maybe a
ma'