{-# OPTIONS --termination-depth=2 #-}
module Unif where
open import Relation.Nullary.Decidable using (⌊_⌋)
open import Data.Bool                  using (Bool; true; false; _∨_; _∧_; if_then_else_)
open import Data.Empty                 using (⊥; ⊥-elim)
open import Data.Unit                  using (⊤; tt)
open import Data.Nat                   using (ℕ; suc; pred; _+_; _∸_; _≟_; zero)
open import Data.Maybe                 using (Maybe; nothing; just; from-just; From-just)
open import Data.Product               using (_×_; _,_; proj₁; proj₂; ∃)
open import Ty                         using (Var; Con; _⇒_; 𝕋; 𝕋𝕋; 𝕋𝕋s; 𝕍ar; numVarsL; 
                                              numConstructorsLP; numConstructors; _≟t_; invCon)
open import Subst_list                 using (Subs; emptySubs; insert; apply; applyL; 
                                              _∘s_; _≟s_; _≺_; lemmaS0; comm_apply)
open import Data.List                  using (List; []; _∷_; filter; map; sum)
open import Data.List.All as All       using (All; []; _∷_)
open import Function                   using (_∘_; case_of_)

open import Relation.Nullary           using (yes; no)
open import Relation.Binary            using (Decidable)
open import Relation.Binary.PropositionalEquality using (cong; _≡_; _≢_; refl; sym)
open Relation.Binary.PropositionalEquality.≡-Reasoning using (begin_; _≡⟨_⟩_; _∎)
open import Function using (_$_)
import Algebra.FunctionProperties as P; open P (_≡_ {A = ℕ})
open import Data.Sum using (_⊎_ ; inj₁; inj₂)

occurs : 𝕍ar → 𝕋 → Bool
occurs ν (Var ν') = ⌊ ν' ≟ ν ⌋ 
occurs _ (Con _)  = false
occurs ν (ta ⇒ tb) = occurs ν ta ∨ occurs ν tb

data Unif2 : (s : Subs) → (τ₁ : 𝕋) → (τ₂ : 𝕋) → Set where
  unif2 :  ∀ s τ₁ τ₂ → (apply s τ₁ ≡ apply s τ₂) → Unif2 s τ₁ τ₂

comm_unif2 : ∀ s τ₁ τ₂ → (apply s τ₁ ≡ apply s τ₂) → (apply s τ₂ ≡ apply s τ₁)
comm_unif2 s τ₁ τ₂ = sym 

comm_unif2' : ∀ {s} {τ₁} {τ₂} → Unif2 s τ₁ τ₂ → Unif2 s τ₂ τ₁
comm_unif2' (unif2 s τ₁ τ₂ p) = unif2 s τ₂ τ₁ (sym p)

mgu2 : (τ₁ : 𝕋) (τ₂ : 𝕋) → Maybe (∃ (\s₀ → Unif2 s₀ τ₁ τ₂ × (∀ {s} → Unif2 s τ₁ τ₂ → s₀ ≺ s)))
mgu2 (Con c)   (Var v) = {!!} 
{-
case mgu2 (Var v) (Con c) of λ
   { nothing → nothing ; 
     (just (s , _ , p₁)) → ? 
-}
mgu2 (Con _)   (_ ⇒ _)                 = nothing
mgu2 (Con c)   (Con c') with c ≟ c' 
mgu2 (Con c)   (Con .c) | yes refl     = just (emptySubs , unif2 [] (Con c) (Con c) refl , (λ {s} _ → s , refl))
mgu2 (Con c)   (Con c') | no _         = nothing
mgu2 (_ ⇒ _)   (Con _)                 = nothing 
mgu2 (τ₁ ⇒ τ₂) (Var v) with mgu2 (Var v) (τ₁ ⇒ τ₂)
mgu2 (τ₁ ⇒ τ₂) (Var v) | nothing = nothing 
mgu2 (τ₁ ⇒ τ₂) (Var v) | just (s₀ , p ) = just (s₀ , ({!!} , (λ x → {!!} , {!!}))) -- Agda bug1: auto gives nothing
mgu2 (τ₁ ⇒ τ₂) (τ₁' ⇒ τ₂') with mgu2 τ₁ τ₁'
mgu2 (τ₁ ⇒ τ₂) (τ₁' ⇒ τ₂') | nothing = nothing
mgu2 (τ₁ ⇒ τ₂) (τ₁' ⇒ τ₂') | just (s₀ , p₀ , p) with mgu2 (apply s₀ τ₂) (apply s₀ τ₂')
mgu2 (τ₁ ⇒ τ₂) (τ₁' ⇒ τ₂') | just (s₀ , p₀ , p) | nothing               = nothing
mgu2 (τ₁ ⇒ τ₂) (τ₁' ⇒ τ₂') | just (s₀ , p₀ , p) | just (s₀' , p₀' , p') = {!!} 
mgu2 (Var v₁)  (Var v₂) with v₁ ≟ v₂
mgu2 (Var v₁)  (Var .v₁) | yes refl = just (emptySubs , unif2 [] (Var v₁) (Var v₁) refl , (λ {x} x' → x , refl))
mgu2 (Var v₁)  (Var v₂)  | no _     = just (insert v₁ (Var v₂) emptySubs , {!!} , (λ x → {!!} , {!!}))
mgu2 (Var v) τ with occurs v τ
... | true                         = nothing 
... | false                        = just (insert v τ emptySubs , {!!} , (λ x → {!!} , {!!}))