--------------------------------------------------------------------------------
-- This is part of Agda Inference Systems 

open import Agda.Builtin.Equality
open import Data.Product
open import Data.Sum
open import Data.Vec using (Vec; fromList; length) renaming (lookup to get)
open import Data.Fin using (Fin)
open import Level
open import Relation.Unary using (_βŠ†_)

module is-lib.InfSys.Base {𝓁} where

  record MetaRule {𝓁c 𝓁p : Level} (U : Set 𝓁) : Set (𝓁 βŠ” suc 𝓁c βŠ” suc 𝓁p) where 
    field 
      Ctx : Set 𝓁c
      Pos : Ctx β†’ Set 𝓁p 
      prems : (c : Ctx) β†’ Pos c β†’ U
      conclu : Ctx β†’ U 

    addSideCond : βˆ€{𝓁'} β†’ (U β†’ Set 𝓁') β†’ MetaRule {𝓁c βŠ” 𝓁'} U
    (addSideCond P) .Ctx = Σ[ c ∈ Ctx ] P (conclu c)
    (addSideCond P) .Pos (c , _) = Pos c
    (addSideCond P) .prems (c , _) p = prems c p
    (addSideCond P) .conclu (c , _) = conclu c

    RF[_] : βˆ€{𝓁'} β†’ (U β†’ Set 𝓁') β†’ (U β†’ Set _)
    RF[_] P u = Ξ£[ c ∈ Ctx ] (u ≑ conclu c Γ— (βˆ€ p β†’ P (prems c p)))

    RClosed : βˆ€{𝓁'} β†’ (U β†’ Set 𝓁') β†’ Set _
    RClosed P = βˆ€ c β†’ (βˆ€ p β†’ P (prems c p)) β†’ P (conclu c)

  {- Finitary Rule -}

  record FinMetaRule {𝓁c n} (U : Set 𝓁) : Set (𝓁 βŠ” suc 𝓁c) where
    field
      Ctx : Set 𝓁c
      comp : Ctx β†’ Vec U n Γ— U

    from : MetaRule {𝓁c} {zero} U
    from .MetaRule.Ctx = Ctx
    from .MetaRule.Pos = Ξ» _ β†’ Fin n
    from .MetaRule.prems c n = get (proj₁ (comp c)) n
    from .MetaRule.conclu c = projβ‚‚ (comp c)

  open MetaRule

  record IS {𝓁c 𝓁p 𝓁n : Level} (U : Set 𝓁) : Set (𝓁 βŠ” suc 𝓁c βŠ” suc 𝓁p βŠ” suc 𝓁n) where
    field
      Names : Set 𝓁n            
      rules : Names β†’ MetaRule {𝓁c} {𝓁p} U 

    ISF[_] : βˆ€{𝓁'} β†’ (U β†’ Set 𝓁') β†’ (U β†’ Set _)
    ISF[_] P u = Σ[ rn ∈ Names ] RF[ rules rn ] P u

    ISClosed : βˆ€{𝓁'} β†’ (U β†’ Set 𝓁') β†’ Set _
    ISClosed P = βˆ€ rn β†’ RClosed (rules rn) P

  open IS

  _βˆͺ_ : βˆ€{𝓁c 𝓁p 𝓁n 𝓁n'}{U : Set 𝓁} β†’ IS {𝓁c} {𝓁p} {𝓁n} U β†’ IS {_} {_} {𝓁n'} U β†’ IS {_} {_} {𝓁n βŠ” 𝓁n'} U
  (is1 βˆͺ is2) .Names = (is1 .Names) ⊎ (is2 .Names)
  (is1 βˆͺ is2) .rules = [ is1 .rules , is2 .rules ]

  _βŠ“_ : βˆ€{𝓁c 𝓁p 𝓁n 𝓁'}{U : Set 𝓁} β†’ IS {𝓁c} {𝓁p} {𝓁n} U β†’ (U β†’ Set 𝓁') β†’ IS {𝓁c βŠ” 𝓁'} {_} {_} U
  (is βŠ“ P) .Names = is .Names
  (is βŠ“ P) .rules rn = addSideCond (is .rules rn) P

  {- Properties -}

  -- closed implies prefix
  closedβ‡’prefix : βˆ€{𝓁c 𝓁p}{U : Set 𝓁} β†’ (m : MetaRule {𝓁c} {𝓁p} U) β†’ βˆ€{𝓁'}{P : U β†’ Set 𝓁'} β†’ RClosed m {𝓁'} P β†’ RF[ m ] P βŠ† P
  closed⇒prefix _ cl (_ , refl , pr) = cl _ pr

  -- prefix implies closed
  prefixβ‡’closed : βˆ€{𝓁c 𝓁p}{U : Set 𝓁} β†’ (m : MetaRule {𝓁c} {𝓁p} U) β†’ βˆ€{𝓁'}{P : U β†’ Set 𝓁'} β†’ (RF[ m ] P βŠ† P) β†’ RClosed m {𝓁'} P
  prefix⇒closed _ prf c pr = prf (c , refl , pr)