open import Data.Product
open import Relation.Binary.Construct.Closure.ReflexiveTransitive
open import Relation.Binary

open import Stoughton.Var

module ParallelReduction (๐’ž : Set) {๐’ฑ : Set} (var : Enum ๐’ฑ) where

  open import Stoughton.Syntax ๐’ž ๐’ฑ (Enum._โ‰Ÿ_ var)  
  open import Stoughton.Substitution ๐’ž var      
  open import Beta ๐’ž var  
  open import BetaReduction ๐’ž var
  
  private
    _โ‰Ÿ_ = Enum._โ‰Ÿ_ var
  
  infixl 3 _โ‡‰_
  data _โ‡‰_ : ฮ› โ†’ ฮ› โ†’ Set where
    โ‡‰c : {k : ๐’ž} โ†’ c k โ‡‰ c k
    โ‡‰v : {x : ๐’ฑ} โ†’ v x โ‡‰ v x
    โ‡‰ฮป : โˆ€ {x A A' M M'} โ†’ A โ‡‰ A' โ†’ M โ‡‰ M' โ†’ ฮป[ x โˆถ A ] M โ‡‰ ฮป[ x โˆถ A' ] M'
    โ‡‰ฮ  : {x : ๐’ฑ}{A A' M M' : ฮ›} โ†’ A โ‡‰ A' โ†’ M โ‡‰ M' โ†’ ฮ [ x โˆถ A ] M โ‡‰ ฮ [ x โˆถ A' ] M'    
    โ‡‰ยท : {M M' N N' : ฮ›} โ†’ M โ‡‰ M' โ†’ N โ‡‰ N' โ†’ M ยท N โ‡‰ M' ยท N'
    โ‡‰ฮฒ : {x : ๐’ฑ}{A M M' N N' : ฮ›} โ†’ M โ‡‰ M' โ†’ N โ‡‰ N' โ†’ (ฮป[ x โˆถ A ] M) ยท N โ‡‰ M' [ x := N' ]

  โ‡‰ฯ : Reflexive _โ‡‰_
  โ‡‰ฯ {c k} = โ‡‰c 
  โ‡‰ฯ {v x} = โ‡‰v
  โ‡‰ฯ {M ยท N} = โ‡‰ยท โ‡‰ฯ โ‡‰ฯ
  โ‡‰ฯ {ฮป[ x โˆถ A ] M} = โ‡‰ฮป โ‡‰ฯ โ‡‰ฯ
  โ‡‰ฯ {ฮ [ x โˆถ A ] M} = โ‡‰ฮ  โ‡‰ฯ โ‡‰ฯ

  manyStepBetaContainsPar :  _โ‡‰_ โ‡’ _โ†’ฮฒ*โ‚€_
  manyStepBetaContainsPar โ‡‰c           = ฮต  
  manyStepBetaContainsPar โ‡‰v           = ฮต
  manyStepBetaContainsPar (โ‡‰ฮป Aโ‡‰B Mโ‡‰N) = abs-star-ty (manyStepBetaContainsPar Aโ‡‰B) โ—…โ—… abs-star (manyStepBetaContainsPar Mโ‡‰N)
  manyStepBetaContainsPar (โ‡‰ฮ  Aโ‡‰B Mโ‡‰N) =
    pi-star-ty (manyStepBetaContainsPar Aโ‡‰B) โ—…โ—… pi-star (manyStepBetaContainsPar Mโ‡‰N)
  manyStepBetaContainsPar (โ‡‰ยท {M} {M'} {N} {N'} Mโ‡‰M' Nโ‡‰N') =
    app-star-l (manyStepBetaContainsPar Mโ‡‰M') โ—…โ—… app-star-r (manyStepBetaContainsPar Nโ‡‰N')
  manyStepBetaContainsPar (โ‡‰ฮฒ {x} {A} {M} {M'} {N} {N'} Mโ‡‰M' Nโ‡‰N') =
    app-star-l (abs-star (manyStepBetaContainsPar Mโ‡‰M')) โ—…โ—… app-star-r (manyStepBetaContainsPar Nโ‡‰N') โ—…โ—… โ†’cxt ฮฒ โ—… ฮต

  manyStepBetaContainsStarPar : Star _โ‡‰_ โ‡’ _โ†’ฮฒ*โ‚€_
  manyStepBetaContainsStarPar ฮต = ฮต
  manyStepBetaContainsStarPar (Mโ‡‰N โ—… Nโ‡‰*P) = manyStepBetaContainsPar Mโ‡‰N โ—…โ—… manyStepBetaContainsStarPar Nโ‡‰*P

  parContainsOneStep : _โ†’ฮฒ_ โ‡’ _โ‡‰_
  parContainsOneStep (โ†’cxt ฮฒ) = โ‡‰ฮฒ โ‡‰ฯ โ‡‰ฯ
  parContainsOneStep (โ†’ฮปR Mโ†’N) = โ‡‰ฮป โ‡‰ฯ (parContainsOneStep Mโ†’N)
  parContainsOneStep (โ†’ฮ R Mโ†’N) = โ‡‰ฮ  โ‡‰ฯ (parContainsOneStep Mโ†’N)
  parContainsOneStep (โ†’ฮปL Mโ†’N) = โ‡‰ฮป (parContainsOneStep Mโ†’N) โ‡‰ฯ
  parContainsOneStep (โ†’ฮ L Mโ†’N) = โ‡‰ฮ  (parContainsOneStep Mโ†’N) โ‡‰ฯ  
  parContainsOneStep (โ†’ยทR Mโ†’N) = โ‡‰ยท โ‡‰ฯ (parContainsOneStep Mโ†’N)
  parContainsOneStep (โ†’ยทL Mโ†’N) = โ‡‰ยท (parContainsOneStep Mโ†’N) โ‡‰ฯ 

  starParContainsManyStep : _โ†’ฮฒ*โ‚€_ โ‡’ Star _โ‡‰_
  starParContainsManyStep ฮต = ฮต
  starParContainsManyStep (Mโ†’N โ—… Nโ†’*P) = parContainsOneStep Mโ†’N โ—… starParContainsManyStep Nโ†’*P

  manyStepBetaEqualsStarPar : _โ†’ฮฒ*โ‚€_ โ‡” Star _โ‡‰_
  manyStepBetaEqualsStarPar = starParContainsManyStep , manyStepBetaContainsStarPar