module temporal-logic  where

open import Level renaming ( suc to succ ; zero to Zero )
open import Data.Nat
open import Data.List
open import Data.Maybe
-- open import Data.Bool using ( Bool ; true ; false ; _∧_ ) renaming ( not to negate )
open import  Relation.Binary.PropositionalEquality hiding ( [_] )
open import Relation.Nullary -- using (not_; Dec; yes; no)
open import Data.Empty

open import logic
open import automaton

open Automaton 


open import nat
open import Data.Nat.Properties

data LTTL ( V : Set )  : Set where
    s :  V → LTTL V
    ○ :  LTTL V → LTTL V
    □ :  LTTL V → LTTL V
    ⋄ :  LTTL V → LTTL V
    _U_  :  LTTL V → LTTL  V → LTTL  V
    t-not :  LTTL V → LTTL  V
    _t\/_ :  LTTL V → LTTL  V → LTTL  V
    _t/\_ :  LTTL V → LTTL  V → LTTL  V

{-# TERMINATING #-}
M1 : { V : Set } → (ℕ → V → Bool) → ℕ →  LTTL V  → Set
M1 σ i (s x) = σ i x ≡ true
M1 σ i (○ x) = M1 σ (suc i) x  
M1 σ i (□ p) = (j : ℕ) → i ≤ j → M1  σ j p
M1 σ i (⋄ p) = ¬ ( M1 σ i (□ (t-not p) ))
M1 σ i (p U q) = ¬ ( ( j : ℕ) → i ≤ j → ¬ (M1 σ j q ∧ (( k : ℕ) → i ≤ k → k < j → M1 σ j p )) )
M1 σ i (t-not p) = ¬ ( M1 σ i p )
M1 σ i (p t\/ p₁) = M1 σ i p ∧ M1 σ i p₁ 
M1 σ i (p t/\ p₁) = M1 σ i p ∨ M1 σ i p₁ 

data LITL ( V : Set )  : Set where
    iv :  V → LITL V
    i○ :  LITL V → LITL V
    _&_  :  LITL V → LITL  V → LITL  V
    i-not :  LITL V → LITL  V
    _i\/_ :  LITL V → LITL  V → LITL  V
    _i/\_ :  LITL V → LITL  V → LITL  V

open import Relation.Binary.Definitions
open import Data.Unit using ( tt ; ⊤ )

{-# TERMINATING #-}
MI : { V : Set } → (ℕ → V → Bool) → (i j : ℕ) → i ≤ j  →  LITL V  → Set
MI σ i j lt (iv x) = σ i x ≡ true
MI σ i j lt (i○ x) with <-cmp i j
... | tri< a ¬b ¬c = MI σ (suc i) j a x
... | tri≈ ¬a b ¬c = ⊤
... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> lt c)
MI σ i j lt (p & q) = ¬ ( ( k : ℕ) → (i<k : i ≤ k) → (k<j : k ≤ j) → ¬ ( MI σ i k i<k p ∧ MI σ k j k<j p))
MI σ i j lt (i-not p) = ¬ ( MI σ i j lt p )
MI σ i j lt (p i\/ p₁) = MI σ i j lt p ∧ MI σ i j lt p₁ 
MI σ i j lt (p i/\ p₁) = MI σ i j lt p ∨ MI σ i j lt p₁ 

data QBool ( V : Set )  : Set where
    qb :  Bool → QBool V
    qv :  V → QBool V
    exists :  V → QBool V → QBool V
    b-not :  QBool V → QBool  V
    _b\/_ :  QBool V → QBool  V → QBool  V
    _b/\_ :  QBool V → QBool  V → QBool  V

{-# TERMINATING #-}
SQ1 : { V : Set } → ((x y : V) → Dec ( x ≡ y))   → QBool V → V  → Bool → QBool V
SQ1 {V} dec (qb x) v t = qb x
SQ1 {V} dec (qv x) v t with dec x v
... | yes _ = qb t
... | no _ = qv x
SQ1 {V} dec (exists x p) v t = SQ1 dec (SQ1 dec p x true) v t b\/  SQ1 dec (SQ1 dec p x false) v t
SQ1 {V} dec (b-not p) v t = b-not (SQ1 dec p v t )
SQ1 {V} dec (p b\/ p₁) v t =  SQ1 dec p v t b\/  SQ1 dec p₁ v t
SQ1 {V} dec (p b/\ p₁) v t = SQ1 dec p v t b/\  SQ1 dec p₁ v t

{-# TERMINATING #-}
MQ : { V : Set } → (V → Bool) → ((x y : V) → Dec ( x ≡ y))   → QBool V → Bool
MQ {V} val dec (qb x) = x
MQ {V} val dec (qv x) = val x
MQ {V} val dec (exists x p) =  MQ val dec ( SQ1 dec p x true b\/ SQ1 dec p x false )
MQ {V} val dec (b-not p) = not ( MQ val dec p )
MQ {V} val dec (p b\/ p₁) = MQ val dec p \/ MQ val dec p₁ 
MQ {V} val dec (p b/\ p₁) = MQ val dec p /\ MQ val dec p₁ 

data QPTL ( V : Set )  : Set where
    qt :  Bool → QPTL V
    qs :  V → QPTL V
    q○ :  QPTL V → QPTL V
    q□ :  QPTL V → QPTL V
    q⋄ :  QPTL V → QPTL V
    q-exists :  V → QPTL V → QPTL V
    q-not :  QPTL V → QPTL  V
    _q\/_ :  QPTL V → QPTL  V → QPTL  V
    _q/\_ :  QPTL V → QPTL  V → QPTL  V

--
--  ∃ p ( <> p → ? )
--


{-# TERMINATING #-}
SQP1 : { V : Set } → ((x y : V) → Dec ( x ≡ y))   → QPTL V → V  → Bool → QPTL V
SQP1 {V} dec (qt x) v t = qt x
SQP1 {V} dec (qs x) v t with dec x v
... | yes _  = qt t
... | no  _  = qs x
SQP1 {V} dec (q-exists x p) v t = SQP1 dec (SQP1 dec p x true) v t q\/  SQP1 dec (SQP1 dec p x false) v t
SQP1 {V} dec (q○ p) v t = q○ p
SQP1 {V} dec (q□ p) v t = SQP1 {V} dec p v t q/\ q□ p
SQP1 {V} dec (q⋄ p) v t = q-not ( SQP1 dec (q□ (q-not p)) v t)
SQP1 {V} dec (q-not p) v t = q-not ( SQP1 dec p v t )
SQP1 {V} dec (p q\/ p₁) v t = SQP1 {V} dec  p v t q\/ SQP1 {V} dec  p₁ v t 
SQP1 {V} dec (p q/\ p₁) v t = SQP1 {V} dec  p v t q/\ SQP1 {V} dec  p₁ v t 

{-# TERMINATING #-}
MQPTL : { V : Set } → (ℕ → V → Bool) → ℕ → ((x y : V) → Dec ( x ≡ y))     →  QPTL V  → Set
MQPTL σ i dec (qt x) = x ≡ true
MQPTL σ i dec (qs x) = σ i x ≡ true
MQPTL σ i dec (q○ x) = MQPTL σ (suc i) dec x  
MQPTL σ i dec (q□ p) = (j : ℕ) → i ≤ j → MQPTL  σ j dec p
MQPTL σ i dec (q⋄ p) = ¬ ( MQPTL σ i dec (q□ (q-not p) ))
MQPTL σ i dec (q-not p) = ¬ ( MQPTL σ i dec p )
MQPTL σ i dec (q-exists x p) = MQPTL σ i dec ( SQP1 dec p x true q\/  (SQP1 dec p x false)) 
MQPTL σ i dec (p q\/ p₁) = MQPTL σ i dec p ∧ MQPTL σ i dec p₁ 
MQPTL σ i dec (p q/\ p₁) = MQPTL σ i dec p ∨ MQPTL σ i dec p₁