Idea for guanxi terms with logical variables, mrsop style

mrsopLogicTerms.hs

-- -*- eval: (med/hp '(pretty-show generics-mrsop singletons)) -*-

{-# LANGUAGE TypeApplications        #-}
{-# LANGUAGE RankNTypes              #-}
{-# LANGUAGE FlexibleContexts        #-}
{-# LANGUAGE FlexibleInstances       #-}
{-# LANGUAGE GADTs                   #-}
{-# LANGUAGE TypeOperators           #-}
{-# LANGUAGE DataKinds               #-}
{-# LANGUAGE PolyKinds               #-}
{-# LANGUAGE ScopedTypeVariables     #-}
{-# LANGUAGE FunctionalDependencies  #-}
{-# LANGUAGE TemplateHaskell         #-}
{-# LANGUAGE LambdaCase              #-}
{-# LANGUAGE PatternSynonyms         #-}
{-# LANGUAGE UndecidableInstances    #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}

{-# OPTIONS_GHC -Wno-unticked-promoted-constructors #-}
{-# OPTIONS_GHC -Wno-orphans #-}

module Mrsop where

import Generics.MRSOP.Base
import Generics.MRSOP.Opaque
import Generics.MRSOP.Util
import Generics.MRSOP.TH

-- import Data.Functor.Const
-- import Data.Functor.Product
-- import Data.Functor.Sum
import Data.Kind

import Data.Singletons

data Foo
  = FooI Int
  | FooR String Foo
  deriving (Show)

deriveFamily ([t|Foo|])

data Prolog :: [[[Atom Kon]]] -> Atom Kon -> *  where
  Var  :: Int     -> Prolog codes at
  Con  :: Singl k -> Prolog codes (K k)
  Term :: (IsNat n , IsNat i)
       => Constr (Lkup i codes) n
       -> NP (Prolog codes) (Lkup n (Lkup i codes))
       -> Prolog codes (I i)

-- Riscriviamo gli esempi allora:
pex1, pex2, pex3, pex4 :: Prolog CodesFoo (I Z)
pex1 = Var 1                                              -- pura variabile
pex2 = Term CZ (Con (SInt 10) :* NP0)                     -- un costruttore e payload
pex3 = Term CZ (Var 2 :* NP0)                             -- un costruttore e variabile
pex4 = Term (CS CZ) (Con (SString "hey") :* Var 2 :* NP0) -- Un costruttore ricorsivo e variabili all'interno

--------------------------------------------------------------------------------
-- Now, for unification
--------------------------------------------------------------------------------

-- A substitution component is a pair of a term and a replacement symbol
data SubstComponent index = SC (Prolog CodesFoo index) Int

-- Let's do an example of a subcomponent
exSC1 :: SubstComponent (I Z)
exSC1 = SC (Term CZ ((Con (SInt 2)) :* NP0)) 1

-- Now for the entire substitution, which is a list of SubstComponent
data SomeSubstComponent :: Type where
  SomeSubstComponent :: Sing s -> SubstComponent s -> SomeSubstComponent

type Substitution = [SomeSubstComponent]

substitute :: SubstComponent j -> Prolog CodesFoo j -> Prolog CodesFoo j
substitute (SC s i) (Var j)    = if i == j then s else Var j
substitute (SC s i) (Con a)    = Con a
substitute (SC s i) (Term a b) = undefined

unifier :: Prolog CodesFoo (I Z) -> Prolog CodesFoo (I Z) -> Int
unifier = undefined