{-# OPTIONS --allow-unsolved-metas #-}

open import Relation.Binary using (Decidable)
open import Relation.Binary.PropositionalEquality using (_≡_)

module dtres

  {{ Α : Set }} -- Alpha, type-level constants
  {{ C : Set }} -- C, term-level constants

  {{ Var : Set }} -- term variables
  {{ decEqVar : Decidable (_≡_ {A = Var}) }}

  {{ Κ : Set }} -- proof term symbols
  
  where


import SyntaxRew
open SyntaxRew 
  {{ Α }} -- Alpha, type-level constants
  {{ C }} -- C, term-level constants

  {{ Var }} -- term variables
  {{ decEqVar }}

  {{ Κ }} -- proof term symbols
  using (Sig ; Prog ; Ctx ; PT ; Go ; go ; inMT ; · )


import BigSem
open BigSem
  {{ Α }} -- Alpha, type-level constants
  {{ C }} -- C, term-level constants

  {{ Var }} -- term variables
  {{ decEqVar }}

  {{ Κ }} -- proof term symbols
  using ( _+_⟶_∷_ )


import SmlSem
open SmlSem --{{Α}} {{C}} {{T}} {{K}} {{Var}} {{UVar}} 
  {{ Α }}    -- type level constants
  {{ C }}    -- term level constants

  {{ Var }}  -- variables
  {{ decEqVar }}

  {{ Κ }}     -- proof term constants
  using ( _+_⊢_∣_~>_∣_ ; ∀gen )

import LogRel.Gen
open LogRel.Gen
  {{ Α }}    -- type level constants
  {{ C }}    -- term level constants

  {{ Var }}  -- variables
  {{ decEqVar }}

  {{ Κ }}     -- proof term constants
  using ( log-gen )

import Fundamental
open Fundamental
  {{ Α }} -- Alpha, type-level constants
  {{ C }} -- C, term-level constants

  {{ Var }} -- term variables
  {{ decEqVar }}

  {{ Κ }} -- proof term symbols
  using ( fundamental )


import Escape
open Escape
  {{ Α }} -- Alpha, type-level constants
  {{ C }} -- C, term-level constants

  {{ Var }} -- term variables
  {{ decEqVar }}

  {{ Κ }} -- proof term symbols
  using ( escape )

{-

soundness of sml w.r.t big

-}


sound : {S : Sig} {P : Prog} {Γ : Ctx} {e : PT} {G : Go} →
  S + P ⊢ Γ ∣ (go G) ~> · ∣ (inMT e) →
  S + P ⟶  e ∷ G

sound sml = escape (fundamental sml)


{-

generalised soundness of sml w.r.t. big

-}

gensound : {S : Sig} {P : Prog} {Γ Γ' : Ctx} {e : PT} {G : Go} →
  S + P ⊢ Γ ∣ (go G) ~> Γ' ∣ (inMT e) →
  S + P ⟶  e ∷ (∀gen Γ' G)


gensound sml = escape (log-gen (fundamental sml))