{-# OPTIONS --without-K --safe #-}

open import Algebra.Bundles using (Group)

module Algebra.Group.Reasoning.Reflection {g₁ gβ‚‚} (𝓖 : Group g₁ gβ‚‚) where

open Group 𝓖

open import Algebra.Group.Symmetric 𝓖
open import Algebra.Group.Symmetric.Equality 𝓖
open import Algebra.Group.Symmetric.Inclusion 𝓖
open import Algebra.Group.Symmetric.PartialEquality 𝓖 using (_≣'_; peq)
open import Algebra.Morphism.Group

open import Function

open import Tactic.Homomorphism.Group public

open import Data.Bool    as Bool    using (Bool; _∨_; if_then_else_)
open import Data.Maybe   as Maybe   using (Maybe; just; nothing; maybe)
open import Data.List    as List    using (List; _∷_; [])
open import Data.Nat     as β„•       using (β„•; suc; zero)
open import Data.Product as Product using (_Γ—_; _,_)

open import Agda.Builtin.Reflection
open import Reflection.TypeChecking.MonadSyntax
open import Reflection.Argument
open import Reflection.Term using (getName; _β‹―βŸ…βˆ·βŸ†_)

begin-helper : βˆ€ {g h} β†’ ⟦ g ⟧ ≣ ⟦ h ⟧ β†’ g β‰ˆ h
begin-helper {g} {h} p = ⟦⟧-injective p

begin-helper2 : βˆ€ {g h} β†’ g ≣' h β†’ g ≣ h
begin-helper2 p .eq = peq p

constructBackSoln : Term β†’ Term β†’ Term β†’ Term β†’ Term
constructBackSoln f eq lhs rhs =
  let domgrp = quote GroupMorphism.from-group ⟨ def ⟩ f ⟨∷⟩ [] in
  let grp = quote GroupMorphism.to-group ⟨ def ⟩ f ⟨∷⟩ [] in
  quote begin-helper ⟨ def ⟩ domgrp ⟨∷⟩
  (quote Group.trans ⟨ def ⟩ grp ⟨∷⟩
    (quote Group.trans ⟨ def ⟩ grp ⟨∷⟩
      (quote proof ⟨ def ⟩ f ⟨∷⟩ buildExpr lhs ⟨∷⟩ [])
      ⟨∷⟩
      (quote begin-helper2 ⟨ def ⟩ domgrp ⟨∷⟩ eq ⟨∷⟩ [])
      ⟨∷⟩ []
    )
    ⟨∷⟩
    (quote Group.sym ⟨ def ⟩ grp ⟨∷⟩
        (quote proof ⟨ def ⟩ f ⟨∷⟩ buildExpr rhs ⟨∷⟩ []) ⟨∷⟩ [])
    ⟨∷⟩
    []) ⟨∷⟩ []


begin-macro : Term β†’ Term β†’ Term β†’ TC _
begin-macro f proof hole = do
  hole' ← inferType hole >>= normalise
  just (lhs , rhs) ← returnTC (getArgs hole')
    where nothing β†’ typeError (termErr hole' ∷ [])
  let soln = constructBackSoln f proof lhs rhs
  unify hole soln

macro
  begin⟨_⟩_ : Term β†’ Term β†’ Term β†’ TC _
  begin⟨_⟩_ = begin-macro