{-# LANGUAGE ConstraintKinds #-}
-- | Interpreter to duplicate the representation of an expression
-- in order to evaluate it with different interpreters.
--
-- NOTE: this is a more verbose, less clear,
-- and maybe less efficient alternative
-- to maintaining the universal polymorphism of @term@ at parsing time
-- as done with 'TermO';
-- it is mainly here for the sake of curiosity.
module Language.Symantic.Interpreting.Dup where

import Data.Proxy

-- | Interpreter's data.
data DupI term1 term2 a
 =   DupI
 {   dupI_1 :: term1 a
 ,   dupI_2 :: term2 a
 }

dupI0
 :: (cl r, cl s)
 => Proxy cl
 -> (forall term. cl term => term a)
 -> DupI r s a
dupI0 _cl f = f `DupI` f

dupI1
 :: (cl r, cl s)
 => Proxy cl
 -> (forall term. cl term => term a -> term b)
 -> DupI r s a
 -> DupI r s b
dupI1 _cl f (a1 `DupI` a2) =
	f a1 `DupI` f a2

dupI2
 :: (cl r, cl s)
 => Proxy cl
 -> (forall term. cl term => term a -> term b -> term c)
 -> DupI r s a
 -> DupI r s b
 -> DupI r s c
dupI2 _cl f (a1 `DupI` a2) (b1 `DupI` b2) =
	f a1 b1 `DupI` f a2 b2

dupI3
 :: (cl r, cl s)
 => Proxy cl
 -> (forall term. cl term => term a -> term b -> term c -> term d)
 -> DupI r s a
 -> DupI r s b
 -> DupI r s c
 -> DupI r s d
dupI3 _cl f (a1 `DupI` a2) (b1 `DupI` b2) (c1 `DupI` c2) =
	f a1 b1 c1 `DupI` f a2 b2 c2