Univ.idr

module Univ

import Decidable.Equality

-- Weapon, which can have "attack power" to evaluate its damage potential
interface IsWeapon a where
  getAttack : a -> Int

-- Kitchen tool, which can have "quality" to evaluate its usefulness and durability
interface IsKitchen a where
  getQuality : a -> Int

-- Knife, for now we're only concerned with its weight
record Knife where
  constructor MkKnife
  weight : Int

-- Knife is a weapon, and we assume its attack power is related to its weight
[impWeaponKnife] IsWeapon Knife where
  getAttack (MkKnife w) = w * 10

-- Knife is a kitchen tool, and we assume its quality is related to its weight
[impKitchenKnife] IsKitchen Knife where
  getQuality (MkKnife w) = w * 5

data TypeUniverse
  = Weapon
  | Kitchen
  | Both TypeUniverse TypeUniverse

DecEq TypeUniverse where
  decEq Weapon Weapon = Yes Refl
  decEq Kitchen Kitchen = Yes Refl
  decEq Kitchen Weapon = No (\x => case x of {})
  decEq Kitchen (Both _ _) = No (\x => case x of {})
  decEq Weapon Kitchen = No (\x => case x of {})
  decEq Weapon (Both _ _) = No (\x => case x of {})
  decEq (Both _ _) Kitchen = No (\x => case x of {})
  decEq (Both _ _) Weapon = No (\x => case x of {})
  decEq (Both a b) (Both a' b') with (decEq a a') | (decEq b b')
    decEq (Both a b) (Both a b) | Yes Refl | Yes Refl = Yes Refl
    decEq (Both a b) (Both a' b') | No p1 | _ = No (\Refl => p1 Refl)
    decEq (Both a b) (Both a' b') | Yes p1 | No p2 = No (\Refl => p2 Refl)

InterpretConstraints : TypeUniverse -> (Type -> Type)
InterpretConstraints Weapon = IsWeapon
InterpretConstraints Kitchen = IsKitchen
InterpretConstraints (Both a b) = \x => (InterpretConstraints a x, InterpretConstraints b x)



-- Question: Can we implement this?

-- ctrToType : (t : Type) -> GenericContainer -> Maybe t
-- Answer: for the general case, no we cannot. However, because we are working with a `GenericCOntainer` we have access to a bit
-- more information than if we were given just a generic `Type`. First we're going to start by writing a more simple interpreter for types

record RealWeapon where
  constructor MkRealWeapon
  power : Int

InterpretType : TypeUniverse -> Type
InterpretType Weapon = RealWeapon
InterpretType Kitchen = Knife
InterpretType (Both a b) = Pair (InterpretType a) (InterpretType b)

-- Then we are going to modify the generic container such that it only contains values from our type universe:
-- let's put aside the interface things for now

record GenericContainer where
  constructor MkGen
  kind : TypeUniverse
  value : InterpretType kind
  constraints : InterpretConstraints kind (InterpretType kind)

-- now we're going to implement a way to extract knives out of a container:
ctrToKnife : GenericContainer -> Maybe Knife
ctrToKnife (MkGen Weapon value _) = Nothing
ctrToKnife (MkGen Kitchen value _) = Just value
ctrToKnife (MkGen (Both x y) (v1, v2) _) = Nothing -- here we return nothing but we could also return the first knife we find:
-- ctrToKnife (MkGen (Both x y) (v1, v2)) = ctrToKnife (MkGen x v1) <|> ctrToKnife (MkGen y v2)

-- We can implement a generic version of this:
ctrToType : (t : TypeUniverse) -> GenericContainer -> Maybe (InterpretType t)
ctrToType t (MkGen kind value _) with (decEq t kind)
  ctrToType t (MkGen t value _) | (Yes Refl) = Just value
  ctrToType t (MkGen kind value _) | (No contra) = Nothing

-- We can now implement a function that extracts the value and the container and operates on it if we find it
opCtrByType : (t : TypeUniverse) -> (InterpretType t -> GenericContainer) -> GenericContainer -> GenericContainer
opCtrByType univ op cont = maybe cont op (ctrToType univ cont)

-- We can reuse our interpreter for constraints to operate on anything by bringing the constraints into scope, we just need to extract
-- the constraints first
ctrToConstr : (t : TypeUniverse) -> GenericContainer -> Maybe (InterpretConstraints t (InterpretType t))
ctrToConstr t (MkGen kind _ cstr) with (decEq t kind)
  ctrToConstr t (MkGen t _ cstr) | (Yes Refl) = Just cstr
  ctrToConstr t (MkGen kind _ cstr) | (No contra) = Nothing

-- Then we can use the same technique as `opCtrByType` to operate on the data with the added constraint.
opCtrByConstraint : (t : TypeUniverse) -> ((i : InterpretConstraints t (InterpretType t)) => InterpretType t -> GenericContainer) -> GenericContainer -> GenericContainer
opCtrByConstraint t op cont = maybe cont (\x => op {i = fst x} (snd x))
    (pure MkPair <*> ctrToConstr t cont <*> ctrToType t cont)