#lang scheme
(require redex mzlib/list)

; Dans cette version ⊥ devient un operateur n-aire

; les element neutres et absorbant de ⊕ qui sont les booleens t et f sont implantes
; Les operateurs ⊕ et ⊥ sont n-aires
; L'odre lexicographique est implante
(define-language Process-lang
  [n variable bool b e (¬ n)] ; node
  [bool t f] ; boolean
  [e variable (¬ e)] ; event
  [b variable (¬ b)] ; condition
  [on ⊕ ⊥]  ; n-nary operators
  [o2 ≺]  ; binary operators
; process  
 [P variable (⊕ Q ... )] 
  [Q variable P n] 
  [C-P (⊕ C-P P) (⊕ P C-P) hole]
; Conflicts  
 [X variable (⊥ Y ... )] 
  [Y variable X n ] 
  [C-X (⊥ C-X P) (⊥ P C-X) hole]  
; Expression  
  [E variable (on F ...) (b o2 e) (P o2 X)]
  [F variable E P ]
  [C-E (on C-E E) (on E C-E) (E o2 C-E) (C-E o2 E) hole]
)

(define Process-red
  (reduction-relation
   Process-lang
;-----------------------------------------------------------------------
; ⊕ 
; Flatten, idempotency, neutral element 
   ; Conflicts in W  
    (--> (in-hole C-E (⊥ e ...)) (in-hole C-E (ƒ (⊥ e ... )))  "Fn⊥" )
    (--> (in-hole C-P (⊕ Q ... )) (in-hole C-P (ƒ (⊕ Q ... )))  "FIN⊕" )
    (--> (in-hole C-P (⊥ (⊕ Q_1 ... t Q_2 ...  ))) (in-hole C-P (ƒ (⊕ Q_1 ... Q_2 ... )))  "FIN⊕E" )
; Absorbing element
    (--> (in-hole C-P (⊕ Q_1 ... f Q_2 ... )) (in-hole C-P f)  "A⊕" )
; Falsification
    (--> (in-hole C-E (⊕ Q_1 ... e_1 Q_2 ... (¬ e_1) Q_4 ...  )) (in-hole C-E f)  "F⊕" )
    (--> (in-hole C-E (⊕ Q_1 ... (¬ e_1) Q_2 ... e_1 Q_4 ...  )) (in-hole C-E f)  "F⊕C" ) 
    (--> (in-hole C-E (⊥ P_0 ... (⊕ Q_1 ... e_1 Q_2 ... (¬ e_1) Q_4 ...  ) P_1 ...)) (in-hole C-E (⊥ P_0 ... P_1 ...))  "F1⊕" )
    (--> (in-hole C-E (⊥ P_0 ... (⊕ Q_1 ... (¬ e_1) Q_2 ... e_1 Q_4 ...  )P_1 ...)) (in-hole C-E (⊥ P_0 ... P_1 ...))  "F2⊕C" ) 

          
;-----------------------------------------------------------------------
; ⊥ 
; Flatten, idempotency, neutral element 
    (--> (in-hole C-X (⊥ X ... )) (in-hole C-X (ƒ (⊥  X ... )))  "FIN⊥" )
    
;-----------------------------------------------------------------------
; Canonical Form
; Flatten, idempotency, neutral element 
    (--> (in-hole C-E (⊥ (⊕ Q ...) ...)) (in-hole C-E  (ƒ ((⊕ Q ... ) ...)))  "FIN⊥⊕" )    
     
;-----------------------------------------------------------------------
; ≺ : Causality
; Direct conflict between 2 events  
  
   (--> (in-hole C-E (⊕ E_1 ... b E_3 ... (b ≺  n) E_4 ...))
       (in-hole C-E (⊕ n E_1 ... E_3 ...  E_4 ...))"Caus_0")
   
   
; OK : fire an event with multiples causes   
;   (--> (in-hole C-E (⊕ b_1  ... E_1 ... ((⊕ b_2 ...) ≺ n) E_2 ...))
;       (in-hole C-E   (fireTrans (term (b_1  ...)) (term (E_1 ...))(term (b_2 ...)) (term n) (term (E_2 ...)))"Caus_1"))
   
  
;    (--> (in-hole C-E (⊕ E_1 ... E_2 E_3 ...(E_2 ≺ (⊥ n_1 n_2)) E_4 ...))
;       (in-hole C-E (⊕ E_1 ... E_3 ... (⊥ (⊕ E_2 n_1) (⊕ E_2 n_2)) E_4 ...))"Caus_conf")
;-----------------------------------------------------------------------
; Conflicts
; Direct conflict between 2 events  
   (--> (in-hole C-E (⊕ E_1 ... (⊥ e_0 e_1) E_2 ...))
       (in-hole C-E (⊕ E_1 ... (⊥ (⊕ (¬ e_0) e_1) (⊕ e_0 (¬ e_1))) E_2 ...))"2C")

;-----------------------------------------------------------------------
; Distributivities   
; Distributivity of ⊕ over ⊥ (2 terms)
   (--> (in-hole C-E (⊕ F_1 ... (⊥ F_2 F_3))) 
        (in-hole C-E (⊥ (⊕ F_1 ... F_2) (⊕ F_1 ... F_3) )) "⊕→⊥1") 
; Distributivity of ⊕ over ⊥ (2 terms) commute
   (--> (in-hole C-E (⊕ (⊥ F_2 F_3) F_1 ... )) 
        (in-hole C-E (⊥ (⊕ F_1 ... F_2) (⊕ F_1 ... F_3) )) "⊕→⊥1C") 
   
; Distributivity of ⊕ over ⊥
   (--> (in-hole C-E (⊕ F_1 ... (⊥ F_2 F_3 F_4))) 
        (in-hole C-E (⊥ (⊕ F_1 ... F_2) (⊕ F_1 ... F_3) (⊕ F_1 ... F_4) )) "E⊕→⊥2") ; ⊕ over ⊥   
   
; Distributivity of ⊕ over ⊥ (>3 terms)
   (--> (in-hole C-E (⊕ F_1 ... (⊥ F_2 F_3 F_4 ...))) 
        (in-hole C-E (⊥ (⊕ F_1 ... F_2) (⊕ F_1 ... F_3) (⊕ F_1 ...(⊥ F_4 ...) ))) "⊕→⊥2") 
; Distributivity of ⊕ over ⊥ (>3 terms and anywhere in the process
   (--> (in-hole C-E (⊥ (⊕ F_1 ...) ... (⊕ F_2 ... (⊥ F_3 F_4 F_5 ...)) (⊕ F_6 ...) ...)) 
         (in-hole C-E (⊥ (⊕ F_1 ...) ...(⊕ F_2 ... F_3) (⊕ F_2 ... F_4) (⊕ F_2 ...(⊥ F_5 ...)) (⊕ F_6 ...) ...)) "⊕→⊥3") 
; Falsification
    (--> (in-hole C-E (⊕ F_1 ... e_1 F__2 ... (¬ e_1) F__4 ...  )) (in-hole C-P f)  "F⊕E" )
    (--> (in-hole C-E (⊕ F__1 ... (¬ e_1) F__2 ... e_1 F__4 ...  )) (in-hole C-P f)  "F⊕CE" ) 
    (--> (in-hole C-E (⊥ E_0 ... (⊕ F__1 ... e_1 F__2 ... (¬ e_1) F__4 ...  ) E_1 ...)) (in-hole C-E (⊥ E_0 ... E_1 ...))  "F1⊕E" )
    (--> (in-hole C-E (⊥ E_0 ... (⊕ F__1 ... (¬ e_1) F__2 ... e_1 F__4 ...  ) E_1 ...)) (in-hole C-E (⊥ E_0 ... E_1 ...))  "F2⊕CE" ) 
)) 

;-----------------------------------------------------------------------
; META FUNCTION
; ƒ flatten n-arry list member, applies idempotency and neutral element :
(define-metafunction Process-lang
  [(ƒ (⊕ Q ... )) ,(remove* (list 't) (remove-duplicates (cons '⊕ (flatten1 (term (Q ...)))))) ]
  [(ƒ (⊕ F ... )) ,(remove* (list 't) (remove-duplicates (cons '⊕ (flatten1 (term (F ...)))))) ]
  [(ƒ (⊥ e ... )) ,(lproc (term (e ...) )) ] 
  [(ƒ (⊥ X ... )) ,(remove* (list 't) (remove-duplicates (cons '⊥ (flatten2 (term (X ...)))))) ]
  [(ƒ ((⊕ Q ... ) ...)) ,(remove* (list 'f) (remove-duplicates (cons '⊥ (flatten3 (term ((Q ...) ...))))))]   
  [(ƒ ((⊕ Q_1 ... Q_2 ... ) ...)) ,(remove* (list 'f) (remove-duplicates (cons '⊥ (flatten3 (append (term ((Q_1 ...) ...))(term ((Q_2 ...) ...)))))))]
;  [(ƒ (⊕ b_1  ... E_1 ... ((⊕ b_2 ...) ≺ n) E_2 ...)) ,(fireTrans (term (b_1  ...)) (term (E_1 ...))(term (b_2 ...)) (term n) (term (E_2 ...)))]
 
)
;-----------------------------------------------------------------------
; Auxiliary function
; Critarion of sort
(define (symbol<? e1 e2)
  (cond 
    [(and (list? e1) (symbol? e2))  (string<? (symbol->string (cadr e1)) (symbol->string e2)) ]
    [(and (symbol? e1) (list? e2))  (string<? (symbol->string e1) (symbol->string (cadr e2))) ]
    [(and (list? e1) (list? e2))  (string<? (symbol->string (cadr e1)) (symbol->string (cadr e2))) ]
    [else (string<? (symbol->string e1) (symbol->string e2))]))

; Sort a list of node n with lexicographic order
(define (symbol-sort l)
  (quicksort l symbol<?))

; Suppress every sublist which is the prefix of a subllistr of the list list : ex (PrefixSuppress ((a b) (a b c)) --> (a b c)
(define (PrefixSuppress list)
  (cond
    [(< (length list) 2) empty]
    [(= (length list) 2) (if (not (Prefix? (first list) (cdr list))) (second list) empty)]
    [else (if (not (Prefix? (first list) (cdr list)))
                   (cons (first list ) (PrefixSuppress (cdr list))) 
                   (PrefixSuppress (cdr list)))]
 ))

; Return #t if e is a prefix of l
(define (Prefix? e l)
  (cond
    [(symbol? e) (and (equal? e (caar l)))]
    [(list? e) (for/or ([s l]) (⊆ e s)) ]))

; Return #t if l1 ⊆ l2
(define (⊆ l1 l2)
  (cond 
    [(<= (length l1) (length l2)) (for/and ([e1 l1][e2 l2]) (equal? e1 e2))]
    [else (for/and ([e2 l2][e1 l1]) (equal? e2 e1))]))

; Sort a list composed of sub list from the lower to the greater length
(define (LengthOrder l)
  (cond
    [(< (length l) 2) list]
    [else (quicksort l (lambda(x y) (< (length x) (length y))) )]
 ))

; Supress the multiple occurrences of on
(define (sup on l)  
  (filter (lambda (x) (not (equal? on x) ))  l))

; Restablish the parenthesis over a ¬ e --> (¬ e) 
(define (neg l)
  (cond 
    [(empty? l) empty]
    [(equal? (car l) '¬) (cons (list (car l) (second l)) (neg (cddr l)))  ]
    [else (cons (car l) (neg (cdr l)))]
  ))
;----------------------------------------------------------
; Flatten, suppress ⊕, and sort in lexicographical order.
(define (flatten1 l) (symbol-sort (neg (sup '⊕ (flatten l)))))
; Flatten, suppress ⊕, and sort in lexicographical order.
(define (flatten2 l) (neg (sup '⊥ (flattenb l))))
; Flatten, suppress ⊕, and sort in lexicographical order.
(define (flattenb l) 
  (cond
    [(empty? l) empty]
    [(list? (car l)) (if (equal? (second (car l)) '⊥) 
                         (cons (car l) (flattenb (cdr l)))
                         (append (car l) (flattenb (cdr l))))]
    [else (cons (car l) (flattenb (cdr l)))]
 ))
; Flatten, suppress ⊕, and sort in lexicographical order.
(define (flatten3 l) 
 (for/list ([e l])
   (cons '⊕ (remove-duplicates-all (flatten1 e)))))

(define (remove-duplicates-all l)
  (remove-duplicate-sublist (remove-duplicates l)))
  
(define (remove-duplicate-sublist l)
 (cond
  [(empty? l) empty]  
  [(list? (member (car l) (cdr l))) (remove-duplicate-sublist (cdr l))]
  [else (cons (car l) (remove-duplicate-sublist (reverse (cdr l))))]
))


;(define (E↓e e E))

(define (fireTrans p E1  Pre Post E2)
  (if (⊆ Pre p) (list* p E1 Post E2) (list* p E1 Pre Post E2)))
  
  
(include "conflits.rkt")
; test of functions


(include "testRedex.rkt")